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

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.Puzzles.U2Bridge

Contents

- Modeling the puzzle
- Actions
- Recognizing valid solutions
- Solving the puzzle

Description

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

Synopsis

- data U2Member
  - = Bono
  - | Edge
  - | Adam
  - | Larry
- type SU2Member = SBV U2Member
- sLarry :: SBV U2Member
- sAdam :: SBV U2Member
- sEdge :: SBV U2Member
- sBono :: SBV U2Member
- type Time = Word32
- type STime = SBV Time
- crossTime :: U2Member -> Time
- sCrossTime :: SU2Member -> STime
- data Location
  - = Here
  - | There
- type SLocation = SBV Location
- sThere :: SBV Location
- sHere :: SBV Location
- data Status = Status {
  - time :: STime
  - flash :: SLocation
  - lBono :: SLocation
  - lEdge :: SLocation
  - lAdam :: SLocation
  - lLarry :: SLocation
  }
- start :: Status
- type Move a = State Status a
- peek :: (Status -> a) -> Move a
- whereIs :: SU2Member -> Move SLocation
- xferFlash :: Move ()
- xferPerson :: SU2Member -> Move ()
- bumpTime1 :: SU2Member -> Move ()
- bumpTime2 :: SU2Member -> SU2Member -> Move ()
- whenS :: SBool -> Move () -> Move ()
- move1 :: SU2Member -> Move ()
- move2 :: SU2Member -> SU2Member -> Move ()
- type Actions = [(SBool, SU2Member, SU2Member)]
- run :: Actions -> Move [Status]
- isValid :: Actions -> SBool
- solveN :: Int -> IO Bool
- solveU2 :: IO ()

# 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

Instances details

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

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

toConstr :: U2Member -> Constr Source #

dataTypeOf :: U2Member -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Read U2Member Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.U2Bridge Methods readsPrec :: Int -> ReadS U2Member Source # readList :: ReadS [U2Member] Source # readPrec :: ReadPrec U2Member Source # readListPrec :: ReadPrec [U2Member] Source #
Show U2Member Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.U2Bridge Methods showsPrec :: Int -> U2Member -> ShowS Source # show :: U2Member -> String Source # showList :: [U2Member] -> ShowS Source #
Eq U2Member Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.U2Bridge Methods (==) :: U2Member -> U2Member -> Bool Source # (/=) :: U2Member -> U2Member -> Bool Source #
Ord U2Member Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Methods

compare :: U2Member -> U2Member -> Ordering Source #

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

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

(>) :: U2Member -> U2Member -> Bool Source #

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

max :: U2Member -> U2Member -> U2Member Source #

min :: U2Member -> U2Member -> U2Member Source #

SymVal U2Member Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV U2Member) Source #

literal :: U2Member -> SBV U2Member Source #

fromCV :: CV -> U2Member Source #

isConcretely :: SBV U2Member -> (U2Member -> Bool) -> Bool 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 #

unliteral :: SBV U2Member -> Maybe U2Member Source #

isConcrete :: SBV U2Member -> Bool Source #

isSymbolic :: SBV U2Member -> Bool Source #

HasKind U2Member Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Methods

kindOf :: U2Member -> Kind Source #

hasSign :: U2Member -> Bool Source #

intSizeOf :: U2Member -> Int Source #

isBoolean :: U2Member -> Bool Source #

isBounded :: U2Member -> Bool Source #

isReal :: U2Member -> Bool Source #

isFloat :: U2Member -> Bool Source #

isDouble :: U2Member -> Bool Source #

isRational :: U2Member -> Bool Source #

isFP :: U2Member -> Bool Source #

isUnbounded :: U2Member -> Bool Source #

isUserSort :: U2Member -> Bool Source #

isChar :: U2Member -> Bool Source #

isString :: U2Member -> Bool Source #

isList :: U2Member -> Bool Source #

isSet :: U2Member -> Bool Source #

isTuple :: U2Member -> Bool Source #

isMaybe :: U2Member -> Bool Source #

isEither :: U2Member -> Bool Source #

showType :: U2Member -> String Source #

SatModel U2Member Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.U2Bridge Methods parseCVs :: [CV] -> Maybe (U2Member, [CV]) Source # cvtModel :: (U2Member -> Maybe b) -> Maybe (U2Member, [CV]) -> Maybe (b, [CV]) Source #

type SU2Member = SBV U2Member Source #

Symbolic version of the type `U2Member`.

sLarry :: SBV U2Member Source #

Symbolic version of the constructor `Larry`.

sAdam :: SBV U2Member Source #

Symbolic version of the constructor `Adam`.

sEdge :: SBV U2Member Source #

Symbolic version of the constructor `Edge`.

sBono :: SBV U2Member Source #

Symbolic version of the constructor `Bono`.

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

Instances details

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

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

toConstr :: Location -> Constr Source #

dataTypeOf :: Location -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Read Location Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.U2Bridge Methods readsPrec :: Int -> ReadS Location Source # readList :: ReadS [Location] Source # readPrec :: ReadPrec Location Source # readListPrec :: ReadPrec [Location] Source #
Show Location Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.U2Bridge Methods showsPrec :: Int -> Location -> ShowS Source # show :: Location -> String Source # showList :: [Location] -> ShowS Source #
Eq Location Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.U2Bridge Methods (==) :: Location -> Location -> Bool Source # (/=) :: Location -> Location -> Bool Source #
Ord Location Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Methods

compare :: Location -> Location -> Ordering Source #

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

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

(>) :: Location -> Location -> Bool Source #

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

max :: Location -> Location -> Location Source #

min :: Location -> Location -> Location Source #

SymVal Location Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Location) Source #

literal :: Location -> SBV Location Source #

fromCV :: CV -> Location Source #

isConcretely :: SBV Location -> (Location -> Bool) -> Bool 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 #

unliteral :: SBV Location -> Maybe Location Source #

isConcrete :: SBV Location -> Bool Source #

isSymbolic :: SBV Location -> Bool Source #

HasKind Location Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

Methods

kindOf :: Location -> Kind Source #

hasSign :: Location -> Bool Source #

intSizeOf :: Location -> Int Source #

isBoolean :: Location -> Bool Source #

isBounded :: Location -> Bool Source #

isReal :: Location -> Bool Source #

isFloat :: Location -> Bool Source #

isDouble :: Location -> Bool Source #

isRational :: Location -> Bool Source #

isFP :: Location -> Bool Source #

isUnbounded :: Location -> Bool Source #

isUserSort :: Location -> Bool Source #

isChar :: Location -> Bool Source #

isString :: Location -> Bool Source #

isList :: Location -> Bool Source #

isSet :: Location -> Bool Source #

isTuple :: Location -> Bool Source #

isMaybe :: Location -> Bool Source #

isEither :: Location -> Bool Source #

showType :: Location -> String Source #

SatModel Location Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.U2Bridge Methods parseCVs :: [CV] -> Maybe (Location, [CV]) Source # cvtModel :: (Location -> Maybe b) -> Maybe (Location, [CV]) -> Maybe (b, [CV]) Source #

type SLocation = SBV Location Source #

Symbolic version of the type `Location`.

sThere :: SBV Location Source #

Symbolic version of the constructor `There`.

sHere :: SBV Location Source #

Symbolic version of the constructor `Here`.

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

- 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

Instances details

Generic Status Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.U2Bridge Associated Types type Rep Status :: Type -> Type Source # Methods from :: Status -> Rep Status x Source # to :: Rep Status x -> Status Source #
Mergeable Status Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.U2Bridge Methods symbolicMerge :: Bool -> SBool -> Status -> Status -> Status Source # select :: (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 Defined in Documentation.SBV.Examples.Puzzles.U2Bridge Methods symbolicMerge :: 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

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

type Rep Status = D1 ('MetaData "Status" "Documentation.SBV.Examples.Puzzles.U2Bridge" "sbv-10.2-Gi6nXbGJVKyDE1oJouGknK" '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 :: 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.