Data.SBV.Examples.Puzzles.U2Bridge

The famous U2 bridge crossing puzzle: http://www.braingle.com/brainteasers/515/u2.html

Modeling the puzzle

data U2Member

U2 band members. We want to translate this to SMT-Lib as a data-type, and hence the call to mkSymbolicEnumeration.

Constructors

Bono

Edge

Adam

Larry

Instances

Eq U2Member

Methods

(==) :: U2Member -> U2Member -> Bool

(/=) :: U2Member -> U2Member -> Bool

Data U2Member

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> U2Member -> c U2Member

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c U2Member

toConstr :: U2Member -> Constr

dataTypeOf :: U2Member -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c U2Member)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c U2Member)

gmapT :: (forall b. Data b => b -> b) -> U2Member -> U2Member

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> U2Member -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> U2Member -> r

gmapQ :: (forall d. Data d => d -> u) -> U2Member -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> U2Member -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> U2Member -> m U2Member

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> U2Member -> m U2Member

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> U2Member -> m U2Member

Ord U2Member

Methods

compare :: U2Member -> U2Member -> Ordering

(<) :: U2Member -> U2Member -> Bool

(<=) :: U2Member -> U2Member -> Bool

(>) :: U2Member -> U2Member -> Bool

(>=) :: U2Member -> U2Member -> Bool

max :: U2Member -> U2Member -> U2Member

min :: U2Member -> U2Member -> U2Member

Read U2Member

Methods

readsPrec :: Int -> ReadS U2Member

readList :: ReadS [U2Member]

readPrec :: ReadPrec U2Member

readListPrec :: ReadPrec [U2Member]

Show U2Member

Methods

showsPrec :: Int -> U2Member -> ShowS

show :: U2Member -> String

showList :: [U2Member] -> ShowS

HasKind U2Member

Methods

kindOf :: U2Member -> Kind

hasSign :: U2Member -> Bool

intSizeOf :: U2Member -> Int

isBoolean :: U2Member -> Bool

isBounded :: U2Member -> Bool

isReal :: U2Member -> Bool

isFloat :: U2Member -> Bool

isDouble :: U2Member -> Bool

isInteger :: U2Member -> Bool

isUninterpreted :: U2Member -> Bool

showType :: U2Member -> String

SymWord U2Member

Methods

forall :: String -> Symbolic (SBV U2Member)

forall_ :: Symbolic (SBV U2Member)

mkForallVars :: Int -> Symbolic [SBV U2Member]

exists :: String -> Symbolic (SBV U2Member)

exists_ :: Symbolic (SBV U2Member)

mkExistVars :: Int -> Symbolic [SBV U2Member]

free :: String -> Symbolic (SBV U2Member)

free_ :: Symbolic (SBV U2Member)

mkFreeVars :: Int -> Symbolic [SBV U2Member]

symbolic :: String -> Symbolic (SBV U2Member)

symbolics :: [String] -> Symbolic [SBV U2Member]

literal :: U2Member -> SBV U2Member

unliteral :: SBV U2Member -> Maybe U2Member

fromCW :: CW -> U2Member

isConcrete :: SBV U2Member -> Bool

isSymbolic :: SBV U2Member -> Bool

isConcretely :: SBV U2Member -> (U2Member -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV U2Member)

SatModel U2Member

Make U2Member a symbolic value.

Methods

parseCWs :: [CW] -> Maybe (U2Member, [CW])

cvtModel :: (U2Member -> Maybe b) -> Maybe (U2Member, [CW]) -> Maybe (b, [CW])

SMTValue U2Member

Methods

sexprToVal :: SExpr -> Maybe U2Member

type SU2Member = SBV U2Member

Symbolic shorthand for a U2Member

bono :: SU2Member

Shorthands for symbolic versions of the members

edge :: SU2Member

Shorthands for symbolic versions of the members

adam :: SU2Member

Shorthands for symbolic versions of the members

larry :: SU2Member

Shorthands for symbolic versions of the members

type Time = Word32

Model time using 32 bits

type STime = SBV Time

Symbolic variant for time

crossTime :: U2Member -> Time

Crossing times for each member of the band

sCrossTime :: SU2Member -> STime

The symbolic variant.. The duplication is unfortunate.

data Location

Location of the flash

Constructors

Here

There

Instances

Eq Location

Methods

(==) :: Location -> Location -> Bool

(/=) :: Location -> Location -> Bool

Data Location

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Location -> c Location

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Location

toConstr :: Location -> Constr

dataTypeOf :: Location -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Location)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Location)

gmapT :: (forall b. Data b => b -> b) -> Location -> Location

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Location -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Location -> r

gmapQ :: (forall d. Data d => d -> u) -> Location -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Location -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Location -> m Location

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Location -> m Location

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Location -> m Location

Ord Location

Methods

compare :: Location -> Location -> Ordering

(<) :: Location -> Location -> Bool

(<=) :: Location -> Location -> Bool

(>) :: Location -> Location -> Bool

(>=) :: Location -> Location -> Bool

max :: Location -> Location -> Location

min :: Location -> Location -> Location

Read Location

Methods

readsPrec :: Int -> ReadS Location

readList :: ReadS [Location]

readPrec :: ReadPrec Location

readListPrec :: ReadPrec [Location]

Show Location

Methods

showsPrec :: Int -> Location -> ShowS

show :: Location -> String

showList :: [Location] -> ShowS

HasKind Location

Methods

kindOf :: Location -> Kind

hasSign :: Location -> Bool

intSizeOf :: Location -> Int

isBoolean :: Location -> Bool

isBounded :: Location -> Bool

isReal :: Location -> Bool

isFloat :: Location -> Bool

isDouble :: Location -> Bool

isInteger :: Location -> Bool

isUninterpreted :: Location -> Bool

showType :: Location -> String

SymWord Location

Methods

forall :: String -> Symbolic (SBV Location)

forall_ :: Symbolic (SBV Location)

mkForallVars :: Int -> Symbolic [SBV Location]

exists :: String -> Symbolic (SBV Location)

exists_ :: Symbolic (SBV Location)

mkExistVars :: Int -> Symbolic [SBV Location]

free :: String -> Symbolic (SBV Location)

free_ :: Symbolic (SBV Location)

mkFreeVars :: Int -> Symbolic [SBV Location]

symbolic :: String -> Symbolic (SBV Location)

symbolics :: [String] -> Symbolic [SBV Location]

literal :: Location -> SBV Location

unliteral :: SBV Location -> Maybe Location

fromCW :: CW -> Location

isConcrete :: SBV Location -> Bool

isSymbolic :: SBV Location -> Bool

isConcretely :: SBV Location -> (Location -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Location)

SatModel Location

Make Location a symbolic value.

Methods

parseCWs :: [CW] -> Maybe (Location, [CW])

cvtModel :: (Location -> Maybe b) -> Maybe (Location, [CW]) -> Maybe (b, [CW])

SMTValue Location

Methods

sexprToVal :: SExpr -> Maybe Location

type SLocation = SBV Location

Symbolic variant of Location

here :: SLocation

Shorthands for symbolic versions of locations

there :: SLocation

Shorthands for symbolic versions of locations

data Status

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

Fields

• time :: STime

  elapsed time

• flash :: SLocation

  location of the flash

• lBono :: SLocation

  location of Bono

• lEdge :: SLocation

  location of Edge

• lAdam :: SLocation

  location of Adam

• lLarry :: SLocation

  location of Larry

Instances

Generic Status

Associated Types

type Rep Status :: * -> *

Methods

from :: Status -> Rep Status x

to :: Rep Status x -> Status

Mergeable Status

Methods

symbolicMerge :: Bool -> SBool -> Status -> Status -> Status

select :: (SymWord b, Num b) => [Status] -> Status -> SBV b -> Status

Mergeable a => Mergeable (Move a)

Mergeable instance for Move simply pushes the merging the data after run of each branch starting from the same state.

Methods

symbolicMerge :: Bool -> SBool -> Move a -> Move a -> Move a

select :: (SymWord b, Num b) => [Move a] -> Move a -> SBV b -> Move a

type Rep Status

type Rep Status = D1 * (MetaData "Status" "Data.SBV.Examples.Puzzles.U2Bridge" "sbv-7.1-56ITrlqRjAjFzgs28xEVp3" False) (C1 * (MetaCons "Status" PrefixI True) ((:*:) * ((:*:) * (S1 * (MetaSel (Just Symbol "time") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * STime)) ((:*:) * (S1 * (MetaSel (Just Symbol "flash") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * SLocation)) (S1 * (MetaSel (Just Symbol "lBono") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * SLocation)))) ((:*:) * (S1 * (MetaSel (Just Symbol "lEdge") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * SLocation)) ((:*:) * (S1 * (MetaSel (Just Symbol "lAdam") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * SLocation)) (S1 * (MetaSel (Just Symbol "lLarry") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * SLocation))))))

start :: Status

Start configuration, time elapsed is 0 and everybody is here

type Move a = State Status a

A puzzle move is modeled as a state-transformer

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

Read the state via an accessor function

whereIs :: SU2Member -> Move SLocation

Given an arbitrary member, return his location

xferFlash :: Move ()

Transferring the flash to the other side

xferPerson :: SU2Member -> Move ()

Transferring a person to the other side

bumpTime1 :: SU2Member -> Move ()

Increment the time, when only one person crosses

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

Increment the time, when two people cross together

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

Symbolic version of when

move1 :: SU2Member -> Move ()

Move one member, remembering to take the flash

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

Move two members, again with the flash

Actions

type Actions = [(SBool, SU2Member, SU2Member)]

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]

Run a sequence of given actions.

Recognizing valid solutions

isValid :: Actions -> SBool

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 Bool

See if there is a solution that has precisely n steps

solveU2 :: IO ()

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 all possible solutions to the puzzle.