Documentation.SBV.Examples.Puzzles.DieHard

Solves the die-hard riddle: In the movie Die Hard 3, the heroes must obtain exactly 4 gallons of water using a 5 gallon jug, a 3 gallon jug, and a water faucet. We use a bounded-model-checking style search to find a solution.

Documentation

data Action

Possible actions

Constructors

Initial

FillBig

FillSmall

EmptyBig

EmptySmall

BigToSmall

SmallToBig

Instances

Data Action

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

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

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

toConstr :: Action -> Constr

dataTypeOf :: Action -> DataType

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

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

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

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

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

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

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

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

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

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

Read Action

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

readsPrec :: Int -> ReadS Action

readList :: ReadS [Action]

readPrec :: ReadPrec Action

readListPrec :: ReadPrec [Action]

Show Action

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

showsPrec :: Int -> Action -> ShowS

show :: Action -> String

showList :: [Action] -> ShowS

Eq Action

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

(==) :: Action -> Action -> Bool

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

Ord Action

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

compare :: Action -> Action -> Ordering

(<) :: Action -> Action -> Bool

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

(>) :: Action -> Action -> Bool

(>=) :: Action -> Action -> Bool

max :: Action -> Action -> Action

min :: Action -> Action -> Action

SymVal Action

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Action)

literal :: Action -> SBV Action

fromCV :: CV -> Action

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

free :: MonadSymbolic m => String -> m (SBV Action)

free_ :: MonadSymbolic m => m (SBV Action)

mkFreeVars :: MonadSymbolic m => Int -> m [SBV Action]

symbolic :: MonadSymbolic m => String -> m (SBV Action)

symbolics :: MonadSymbolic m => [String] -> m [SBV Action]

unliteral :: SBV Action -> Maybe Action

isConcrete :: SBV Action -> Bool

isSymbolic :: SBV Action -> Bool

HasKind Action

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

kindOf :: Action -> Kind

hasSign :: Action -> Bool

intSizeOf :: Action -> Int

isBoolean :: Action -> Bool

isBounded :: Action -> Bool

isReal :: Action -> Bool

isFloat :: Action -> Bool

isDouble :: Action -> Bool

isRational :: Action -> Bool

isFP :: Action -> Bool

isUnbounded :: Action -> Bool

isUserSort :: Action -> Bool

isChar :: Action -> Bool

isString :: Action -> Bool

isList :: Action -> Bool

isSet :: Action -> Bool

isTuple :: Action -> Bool

isMaybe :: Action -> Bool

isEither :: Action -> Bool

isArray :: Action -> Bool

showType :: Action -> String

SatModel Action

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

parseCVs :: [CV] -> Maybe (Action, [CV])

cvtModel :: (Action -> Maybe b) -> Maybe (Action, [CV]) -> Maybe (b, [CV])

Queriable IO SState

Queriable instance needed for running bmc

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Associated Types

type QueryResult SState

Defined in Documentation.SBV.Examples.Puzzles.DieHard

type QueryResult SState = CState

Methods

create :: QueryT IO SState

project :: SState -> QueryT IO (QueryResult SState)

embed :: QueryResult SState -> QueryT IO SState

type QueryResult SState

Defined in Documentation.SBV.Examples.Puzzles.DieHard

type QueryResult SState = CState

type SAction = SBV Action

Symbolic version of the type Action.

sInitial :: SBV Action

Symbolic version of the constructor Initial.

sFillBig :: SBV Action

Symbolic version of the constructor FillBig.

sFillSmall :: SBV Action

Symbolic version of the constructor FillSmall.

sEmptyBig :: SBV Action

Symbolic version of the constructor EmptyBig.

sEmptySmall :: SBV Action

Symbolic version of the constructor EmptySmall.

sBigToSmall :: SBV Action

Symbolic version of the constructor BigToSmall.

sSmallToBig :: SBV Action

Symbolic version of the constructor SmallToBig.

data State a b

We represent the state with two quantities, the amount of water in each jug. The action is how we got into this state.

Constructors

State

Fields

• big :: a
• small :: a
• action :: b

Instances

Queriable IO SState

Queriable instance needed for running bmc

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Associated Types

type QueryResult SState

Defined in Documentation.SBV.Examples.Puzzles.DieHard

type QueryResult SState = CState

Methods

create :: QueryT IO SState

project :: SState -> QueryT IO (QueryResult SState)

embed :: QueryResult SState -> QueryT IO SState

(Show a, Show b) => Show (State a b)

Show instance

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

showsPrec :: Int -> State a b -> ShowS

show :: State a b -> String

showList :: [State a b] -> ShowS

type QueryResult SState

Defined in Documentation.SBV.Examples.Puzzles.DieHard

type QueryResult SState = CState

type SState = State SInteger SAction

Fully symbolic state

type CState = State Integer Action

Fully concrete state

dieHard :: IO ()

Solve the problem using a BMC search. We have:

>>> dieHard
BMC Cover: Iteration: 0
BMC Cover: Iteration: 1
BMC Cover: Iteration: 2
BMC Cover: Iteration: 3
BMC Cover: Iteration: 4
BMC Cover: Iteration: 5
BMC Cover: Iteration: 6
BMC Cover: Satisfying state found at iteration 6
Big: 0, Small: 0 (Initial)
Big: 5, Small: 0 (FillBig)
Big: 2, Small: 3 (BigToSmall)
Big: 2, Small: 0 (EmptySmall)
Big: 0, Small: 2 (BigToSmall)
Big: 5, Small: 2 (FillBig)
Big: 4, Small: 3 (BigToSmall)