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

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

Data.SBV.Examples.Puzzles.U2Bridge

Contents

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

Description

The famous U2 bridge crossing puzzle: http://www.brainj.net/puzzle.php?id=u2

Synopsis

- data U2Member
  - = Bono
  - | Edge
  - | Adam
  - | Larry
- type SU2Member = SBV U2Member
- bono :: SU2Member
- edge :: SU2Member
- adam :: SU2Member
- larry :: SU2Member
- type Time = Word32
- type STime = SBV Time
- crossTime :: U2Member -> Time
- sCrossTime :: SU2Member -> STime
- data Location
  - = Here
  - | There
- type SLocation = SBV Location
- here :: SLocation
- there :: SLocation
- 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 deriving mechanism.

Constructors

Bono |
Edge |
Adam |
Larry |

Instances

Eq U2Member Source |
Data U2Member Source |
Ord U2Member Source |
Read U2Member Source |
Show U2Member Source |
HasKind U2Member Source |
SymWord U2Member Source |
SatModel 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 |
Data Location Source |
Ord Location Source |
Read Location Source |
Show Location Source |
HasKind Location Source |
SymWord Location Source |
SatModel 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

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 Source |
Mergeable 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.
type Rep Status Source |

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.