| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Documentation.SBV.Examples.Puzzles.U2Bridge
Description
The famous U2 bridge crossing puzzle: http://www.braingle.com/brainteasers/515/u2.html
- data U2Member
- type SU2Member = SBV U2Member
- bono :: SU2Member
- edge :: SU2Member
- adam :: SU2Member
- larry :: SU2Member
- type Time = Word32
- type STime = SBV Time
- crossTime :: U2Member -> Time
- sCrossTime :: SU2Member -> STime
- data Location
- type SLocation = SBV Location
- here :: SLocation
- there :: SLocation
- data Status = Status {}
- start :: Status
- type Move a = State Status a
- peek :: (Status -> a) -> Move a
- whereIs :: SU2Member -> Move SLocation
- xferFlash :: Move ()
- xferPerson :: SU2Member -> Move ()
- bumpTime1 :: SU2Member -> Move ()
- bumpTime2 :: SU2Member -> SU2Member -> Move ()
- whenS :: SBool -> Move () -> Move ()
- move1 :: SU2Member -> Move ()
- move2 :: SU2Member -> SU2Member -> Move ()
- type Actions = [(SBool, SU2Member, SU2Member)]
- run :: Actions -> Move [Status]
- isValid :: Actions -> SBool
- solveN :: Int -> IO Bool
- solveU2 :: IO ()
Modeling the puzzle
U2 band members. We want to translate this to SMT-Lib as a data-type, and hence the call to mkSymbolicEnumeration.
sCrossTime :: SU2Member -> STime Source #
The symbolic variant.. The duplication is unfortunate.
Location of the flash
The status of the puzzle after each move
This type is equipped with an automatically derived Mergeable instance
because each field is Mergeable. A Generic instance must also be derived
for this to work, and the DeriveAnyClass language extension must be
enabled. The derived Mergeable instance simply walks down the structure
field by field and merges each one. An equivalent hand-written Mergeable
instance is provided in a comment below.
Constructors
| Status | |
xferPerson :: SU2Member -> Move () Source #
Transferring a person to the other side
bumpTime2 :: SU2Member -> SU2Member -> Move () Source #
Increment the time, when two people cross together
Actions
type Actions = [(SBool, SU2Member, SU2Member)] Source #
A move action is a sequence of triples. The first component is symbolically True if only one member crosses. (In this case the third element of the triple is irrelevant.) If the first component is (symbolically) False, then both members move together
Recognizing valid solutions
isValid :: Actions -> SBool Source #
Check if a given sequence of actions is valid, i.e., they must all cross the bridge according to the rules and in less than 17 seconds
Solving the puzzle
Solve the U2-bridge crossing puzzle, starting by testing solutions with increasing number of steps, until we find one. We have:
>>>solveU2Checking for solutions with 1 move. Checking for solutions with 2 moves. Checking for solutions with 3 moves. Checking for solutions with 4 moves. Checking for solutions with 5 moves. Solution #1: 0 --> Edge, Bono 2 <-- Bono 3 --> Larry, Adam 13 <-- Edge 15 --> Edge, Bono Total time: 17 Solution #2: 0 --> Edge, Bono 2 <-- Edge 4 --> Larry, Adam 14 <-- Bono 15 --> Edge, Bono Total time: 17 Found: 2 solutions with 5 moves.
Finding all possible solutions to the puzzle.