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

Documentation.SBV.Examples.Puzzles.U2Bridge

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

Instances
 Source # Instance details Methods Source # Instance details Methodsgfoldl :: (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 #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 # Source # Instance details Methods(<) :: U2Member -> U2Member -> Bool #(>) :: U2Member -> U2Member -> Bool # Source # Instance details Methods Source # Instance details MethodsshowList :: [U2Member] -> ShowS # Source # Instance details Methods Source # Instance details MethodsisConcretely :: SBV U2Member -> (U2Member -> Bool) -> Bool Source #forall :: MonadSymbolic m => String -> m (SBV U2Member) Source #forall_ :: MonadSymbolic m => m (SBV U2Member) Source #mkForallVars :: MonadSymbolic m => Int -> m [SBV U2Member] Source #exists :: MonadSymbolic m => String -> m (SBV U2Member) Source #exists_ :: MonadSymbolic m => m (SBV U2Member) Source #mkExistVars :: MonadSymbolic m => Int -> m [SBV U2Member] Source #free :: MonadSymbolic m => String -> m (SBV U2Member) Source #free_ :: MonadSymbolic m => m (SBV U2Member) Source #mkFreeVars :: MonadSymbolic m => Int -> m [SBV U2Member] Source #symbolic :: MonadSymbolic m => String -> m (SBV U2Member) Source #symbolics :: MonadSymbolic m => [String] -> m [SBV U2Member] Source # Source # Make U2Member a symbolic value. Instance details MethodsparseCVs :: [CV] -> Maybe (U2Member, [CV]) Source #cvtModel :: (U2Member -> Maybe b) -> Maybe (U2Member, [CV]) -> Maybe (b, [CV]) Source # Source # Instance details MethodssexprToVal :: SExpr -> Maybe U2Member Source #

Symbolic shorthand for a U2Member

Shorthands for symbolic versions of the members

Shorthands for symbolic versions of the members

Shorthands for symbolic versions of the members

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

Crossing times for each member of the band

The symbolic variant.. The duplication is unfortunate.

data Location Source #

Location of the flash

Constructors

 Here There
Instances
 Source # Instance details Methods Source # Instance details Methodsgfoldl :: (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 #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 # Source # Instance details Methods(<) :: Location -> Location -> Bool #(>) :: Location -> Location -> Bool # Source # Instance details Methods Source # Instance details MethodsshowList :: [Location] -> ShowS # Source # Instance details Methods Source # Instance details MethodsisConcretely :: SBV Location -> (Location -> Bool) -> Bool Source #forall :: MonadSymbolic m => String -> m (SBV Location) Source #forall_ :: MonadSymbolic m => m (SBV Location) Source #mkForallVars :: MonadSymbolic m => Int -> m [SBV Location] Source #exists :: MonadSymbolic m => String -> m (SBV Location) Source #exists_ :: MonadSymbolic m => m (SBV Location) Source #mkExistVars :: MonadSymbolic m => Int -> m [SBV Location] Source #free :: MonadSymbolic m => String -> m (SBV Location) Source #free_ :: MonadSymbolic m => m (SBV Location) Source #mkFreeVars :: MonadSymbolic m => Int -> m [SBV Location] Source #symbolic :: MonadSymbolic m => String -> m (SBV Location) Source #symbolics :: MonadSymbolic m => [String] -> m [SBV Location] Source # Source # Make Location a symbolic value. Instance details MethodsparseCVs :: [CV] -> Maybe (Location, [CV]) Source #cvtModel :: (Location -> Maybe b) -> Maybe (Location, [CV]) -> Maybe (b, [CV]) Source # Source # Instance details MethodssexprToVal :: SExpr -> Maybe Location Source #

Symbolic variant of Location

Shorthands for symbolic versions of locations

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 Fieldstime :: STimeelapsed timeflash :: SLocationlocation of the flashlBono :: SLocationlocation of BonolEdge :: SLocationlocation of EdgelAdam :: SLocationlocation of AdamlLarry :: SLocationlocation of Larry
Instances
 Source # Instance details Associated Typestype Rep Status :: Type -> Type # Methodsfrom :: Status -> Rep Status x #to :: Rep Status x -> Status # Source # Instance details Methodsselect :: (Ord b, SymVal 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 MethodssymbolicMerge :: Bool -> SBool -> Move a -> Move a -> Move a Source #select :: (Ord b, SymVal b, Num b) => [Move a] -> Move a -> SBV b -> Move a Source # type Rep Status Source # Instance details type Rep Status = D1 (MetaData "Status" "Documentation.SBV.Examples.Puzzles.U2Bridge" "sbv-8.1-KJ81LMQmRNq7C7R4pcgIua" False) (C1 (MetaCons "Status" PrefixI True) ((S1 (MetaSel (Just "time") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 STime) :*: (S1 (MetaSel (Just "flash") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 SLocation) :*: S1 (MetaSel (Just "lBono") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 SLocation))) :*: (S1 (MetaSel (Just "lEdge") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 SLocation) :*: (S1 (MetaSel (Just "lAdam") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 SLocation) :*: S1 (MetaSel (Just "lLarry") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 SLocation)))))

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

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

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