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

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.Puzzles.U2Bridge

Contents

Description

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

Synopsis

Modeling the puzzle

data U2Member Source #

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 Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Data U2Member Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

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 Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Read U2Member Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Show U2Member Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

HasKind U2Member Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

SymWord U2Member Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

SatModel U2Member Source #

Make U2Member a symbolic value.

Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Methods

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

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

SMTValue U2Member Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Methods

sexprToVal :: SExpr -> Maybe U2Member Source #

type SU2Member = SBV U2Member Source #

Symbolic shorthand for a U2Member

bono :: SU2Member Source #

Shorthands for symbolic versions of the members

edge :: SU2Member Source #

Shorthands for symbolic versions of the members

adam :: SU2Member Source #

Shorthands for symbolic versions of the members

larry :: SU2Member Source #

Shorthands for symbolic versions of the members

type Time = Word32 Source #

Model time using 32 bits

type STime = SBV Time Source #

Symbolic variant for time

crossTime :: U2Member -> Time Source #

Crossing times for each member of the band

sCrossTime :: SU2Member -> STime Source #

The symbolic variant.. The duplication is unfortunate.

data Location Source #

Location of the flash

Constructors

Here 
There 
Instances
Eq Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Data Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

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 Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Read Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Show Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

HasKind Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

SymWord Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

SatModel Location Source #

Make Location a symbolic value.

Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Methods

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

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

SMTValue Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Methods

sexprToVal :: SExpr -> Maybe Location Source #

type SLocation = SBV Location Source #

Symbolic variant of Location

here :: SLocation Source #

Shorthands for symbolic versions of locations

there :: SLocation Source #

Shorthands for symbolic versions of locations

data Status Source #

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

Instances
Generic Status Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Associated Types

type Rep Status :: * -> * #

Methods

from :: Status -> Rep Status x #

to :: Rep Status x -> Status #

Mergeable Status Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Methods

symbolicMerge :: Bool -> SBool -> Status -> Status -> Status Source #

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

Mergeable a => Mergeable (Move a) Source #

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

Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Methods

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

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

type Rep Status Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

start :: Status Source #

Start configuration, time elapsed is 0 and everybody is here

type Move a = State Status a Source #

A puzzle move is modeled as a state-transformer

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

Read the state via an accessor function

whereIs :: SU2Member -> Move SLocation Source #

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

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

Run a sequence of given actions.

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

solveN :: Int -> IO Bool Source #

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 <-- 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.