sbv-11.4: 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.DieHard

Description

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.

Synopsis

Documentation

data Action Source #

Possible actions

Constructors

Initial 
FillBig 
FillSmall 
EmptyBig 
EmptySmall 
BigToSmall 
SmallToBig 

Instances

Instances details
Data Action Source # 
Instance details

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

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

readsPrec :: Int -> ReadS Action #

readList :: ReadS [Action] #

readPrec :: ReadPrec Action #

readListPrec :: ReadPrec [Action] #

Show Action Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

showsPrec :: Int -> Action -> ShowS #

show :: Action -> String #

showList :: [Action] -> ShowS #

Eq Action Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

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

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

Ord Action Source # 
Instance details

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

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

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

literal :: Action -> SBV Action Source #

fromCV :: CV -> Action Source #

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

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

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

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

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

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

unliteral :: SBV Action -> Maybe Action Source #

isConcrete :: SBV Action -> Bool Source #

isSymbolic :: SBV Action -> Bool Source #

HasKind Action Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

kindOf :: Action -> Kind Source #

hasSign :: Action -> Bool Source #

intSizeOf :: Action -> Int Source #

isBoolean :: Action -> Bool Source #

isBounded :: Action -> Bool Source #

isReal :: Action -> Bool Source #

isFloat :: Action -> Bool Source #

isDouble :: Action -> Bool Source #

isRational :: Action -> Bool Source #

isFP :: Action -> Bool Source #

isUnbounded :: Action -> Bool Source #

isUserSort :: Action -> Bool Source #

isChar :: Action -> Bool Source #

isString :: Action -> Bool Source #

isList :: Action -> Bool Source #

isSet :: Action -> Bool Source #

isTuple :: Action -> Bool Source #

isMaybe :: Action -> Bool Source #

isEither :: Action -> Bool Source #

isArray :: Action -> Bool Source #

showType :: Action -> String Source #

SatModel Action Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

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

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

Queriable IO SState Source #

Queriable instance needed for running bmc

Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Associated Types

type QueryResult SState 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

type QueryResult SState = CState

Methods

create :: QueryT IO SState Source #

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

embed :: QueryResult SState -> QueryT IO SState Source #

type QueryResult SState Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

type QueryResult SState = CState

type SAction = SBV Action Source #

Symbolic version of the type Action.

sInitial :: SBV Action Source #

Symbolic version of the constructor Initial.

sFillBig :: SBV Action Source #

Symbolic version of the constructor FillBig.

sFillSmall :: SBV Action Source #

Symbolic version of the constructor FillSmall.

sEmptyBig :: SBV Action Source #

Symbolic version of the constructor EmptyBig.

sEmptySmall :: SBV Action Source #

Symbolic version of the constructor EmptySmall.

sBigToSmall :: SBV Action Source #

Symbolic version of the constructor BigToSmall.

sSmallToBig :: SBV Action Source #

Symbolic version of the constructor SmallToBig.

data State a b Source #

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

Instances

Instances details
Queriable IO SState Source #

Queriable instance needed for running bmc

Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Associated Types

type QueryResult SState 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

type QueryResult SState = CState

Methods

create :: QueryT IO SState Source #

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

embed :: QueryResult SState -> QueryT IO SState Source #

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

Show instance

Instance details

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

Defined in Documentation.SBV.Examples.Puzzles.DieHard

type QueryResult SState = CState

type SState = State SInteger SAction Source #

Fully symbolic state

type CState = State Integer Action Source #

Fully concrete state

dieHard :: IO () Source #

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)