sbv-0.9.13: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers.





The famous U2 bridge crossing puzzle:


Modeling the puzzle

data U2Member Source

U2 band members



type Time = SWord32Source

Model time using 32 bits

type SU2Member = SWord8Source

Each member gets an 8-bit id

bono :: SU2MemberSource

Bono's ID

edge :: SU2MemberSource

Edge's ID

adam :: SU2MemberSource

Adam's ID

larry :: SU2MemberSource

Larry's ID

isU2Member :: SU2Member -> SBoolSource

Is this a valid person?

crossTime :: SU2Member -> TimeSource

Crossing times for each member of the band

type Location = SBoolSource

Location of the flash

here :: LocationSource

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

there :: LocationSource

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

data Status Source

The status of the puzzle after each move




time :: Time

elapsed time

flash :: Location

location of the flash

lBono :: Location

location of Bono

lEdge :: Location

location of Edge

lAdam :: Location

location of Adam

lLarry :: Location

location of Larry


start :: StatusSource

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

whereIs :: SU2Member -> Move SBoolSource

Given an arbitrary member, return his location

xferFlash :: Move ()Source

Transferring the flash to the other side

xferPerson :: SU2Member -> Move ()Source

Transferring a person to the other side

bumpTime1 :: SU2Member -> Move ()Source

Increment the time, when only one person crosses

bumpTime2 :: SU2Member -> SU2Member -> Move ()Source

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

move2 :: SU2Member -> SU2Member -> Move ()Source

Move two members, again with the flash


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 :: Actions -> Move [Status]Source

Run a sequence of given actions.

Recognizing valid solutions

isValid :: Actions -> SBoolSource

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

solveN :: Int -> IO BoolSource

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
 4 --> Larry, Adam
14 <-- Bono
15 --> Edge, Bono
Total time: 17
Solution #2: 
 0 --> Edge, Bono
 2 <-- Bono
 3 --> Larry, Adam
13 <-- Edge
15 --> Edge, Bono
Total time: 17
Found: 2 solutions with 5 moves.

Finding the all 2 possible solutions to the puzzle.