sbv-2.7: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Stability experimental erkokl@gmail.com None

Data.SBV.Examples.Puzzles.U2Bridge

Description

The famous U2 bridge crossing puzzle: http://www.brainj.net/puzzle.php?id=u2

Synopsis

# Modeling the puzzle

data U2Member Source

U2 band members

Constructors

Instances

 Enum U2Member Show U2Member SatModel U2Member

type Time = SWord32Source

Model time using 32 bits

Each member gets an 8-bit id

Bono's ID

Edge's ID

Larry's ID

Is this a valid person?

Crossing times for each member of the band

type Location = SBoolSource

Location of the flash

We represent this side of the bridge as `here`, and arbitrarily as `false`

We represent other side of the bridge as `there`, and arbitrarily as `true`

data Status Source

The status of the puzzle after each move

Constructors

 Status Fieldstime :: Timeelapsed time flash :: Locationlocation of the flash lBono :: Locationlocation of Bono lEdge :: Locationlocation of Edge lAdam :: Locationlocation of Adam lLarry :: Locationlocation of Larry

Instances

 Mergeable Status Mergeable a => Mergeable (Move a)

Start configuration, time elapsed is 0 and everybody is `here`

type Move a = State Status aSource

A puzzle move is modeled as a state-transformer

peek :: (Status -> a) -> Move aSource

Read the state via an accessor function

Given an arbitrary member, return his location

Transferring the flash to the other side

Transferring a person to the other side

Increment the time, when only one person crosses

Increment the time, when two people cross together

whenS :: SBool -> Move () -> Move ()Source

Symbolic version of `when`

move1 :: SU2Member -> Move ()Source

Move one member, remembering to take the flash

Move two members, again with the flash

# 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

Run a sequence of given actions.

# Recognizing valid solutions

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

See if there is a solution that has precisely `n` steps

solveU2 :: IO ()Source

Solve the U2-bridge crossing puzzle, starting by testing solutions with increasing number of steps, until we find one. We have:

````>>> ````solveU2
```Checking 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 <-- Edge
14 <-- Bono
15 --> Edge, Bono
Total time: 17
Solution #2:
0 --> Edge, Bono
2 <-- Bono