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

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

data Action
- = Initial
- | FillBig
- | FillSmall
- | EmptyBig
- | EmptySmall
- | BigToSmall
- | SmallToBig
cv2Action :: String -> [CV] -> Action
_undefiner_Action :: a
type SAction = SBV Action
sInitial :: SBV Action
sFillBig :: SBV Action
sFillSmall :: SBV Action
sEmptyBig :: SBV Action
sEmptySmall :: SBV Action
sBigToSmall :: SBV Action
sSmallToBig :: SBV Action
isInitial :: SBV Action -> SBool
isFillBig :: SBV Action -> SBool
isFillSmall :: SBV Action -> SBool
isEmptyBig :: SBV Action -> SBool
isEmptySmall :: SBV Action -> SBool
isBigToSmall :: SBV Action -> SBool
isSmallToBig :: SBV Action -> SBool
sCaseAction :: Mergeable result => SBV Action -> result -> result -> result -> result -> result -> result -> result -> result
data State a b = State {
- big :: a
- small :: a
- action :: b
}
type SState = State SInteger SAction
type CState = State Integer Action
dieHard :: IO ()

Documentation

data Action Source #

Possible actions

Constructors

Initial
FillBig
FillSmall
EmptyBig
EmptySmall
BigToSmall
SmallToBig

Instances

Instances details

Arbitrary Action Source #

Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

arbitrary :: Gen Action #

shrink :: Action -> [Action] #

Show Action Source #

Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

showsPrec :: Int -> Action -> ShowS #

show :: Action -> String #

showList :: [Action] -> ShowS #

SymVal Action Source #

Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

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

mkSymValInit :: State -> SBV Action -> IO () Source #

literal :: Action -> SBV Action Source #

fromCV :: CV -> Action Source #

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

minMaxBound :: Maybe (Action, Action) 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 #

unlitCV :: SBV Action -> Maybe (Kind, CVal) 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 #

isADT :: Action -> Bool Source #

isChar :: Action -> Bool Source #

isString :: Action -> Bool Source #

isList :: Action -> Bool Source #

isSet :: Action -> Bool Source #

isTuple :: Action -> Bool Source #

isArray :: Action -> Bool Source #

isRoundingMode :: Action -> Bool Source #

isUninterpreted :: Action -> Bool Source #

showType :: Action -> String Source #

EnumSymbolic Action Source #

Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

succ :: SBV Action -> SBV Action Source #

pred :: SBV Action -> SBV Action Source #

toEnum :: SInteger -> SBV Action Source #

fromEnum :: SBV Action -> SInteger Source #

enumFrom :: SBV Action -> SList Action Source #

enumFromThen :: SBV Action -> SBV Action -> SList Action Source #

enumFromTo :: SBV Action -> SBV Action -> SList Action Source #

enumFromThenTo :: SBV Action -> SBV Action -> SBV Action -> SList Action 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 #

OrdSymbolic (SBV Action) Source #

Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

(.<) :: SBV Action -> SBV Action -> SBool Source #

(.<=) :: SBV Action -> SBV Action -> SBool Source #

(.>) :: SBV Action -> SBV Action -> SBool Source #

(.>=) :: SBV Action -> SBV Action -> SBool Source #

smin :: SBV Action -> SBV Action -> SBV Action Source #

smax :: SBV Action -> SBV Action -> SBV Action Source #

inRange :: SBV Action -> (SBV Action, SBV Action) -> SBool Source #

HasInductionSchema (Forall ta Action -> SBool) Source #

Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

inductionSchema :: (Forall ta Action -> SBool) -> ProofObj Source #

SymVal extraT => HasInductionSchema (Forall ta Action -> Forall extraS extraT -> SBool) Source #

Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

inductionSchema :: (Forall ta Action -> Forall extraS extraT -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta Action -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source #

Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

inductionSchema :: (Forall ta Action -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta Action -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source #

Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

inductionSchema :: (Forall ta Action -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta Action -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source #

Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

inductionSchema :: (Forall ta Action -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta Action -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source #

Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

Methods

inductionSchema :: (Forall ta Action -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

type QueryResult SState Source #

Instance details

Defined in Documentation.SBV.Examples.Puzzles.DieHard

type QueryResult SState = CState

cv2Action :: String -> [CV] -> Action Source #

Conversion from SMT values to Action values.

_undefiner_Action :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

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.

isInitial :: SBV Action -> SBool Source #

Field recognizer predicate.

isFillBig :: SBV Action -> SBool Source #

Field recognizer predicate.

isFillSmall :: SBV Action -> SBool Source #

Field recognizer predicate.

isEmptyBig :: SBV Action -> SBool Source #

Field recognizer predicate.

isEmptySmall :: SBV Action -> SBool Source #

Field recognizer predicate.

isBigToSmall :: SBV Action -> SBool Source #

Field recognizer predicate.

isSmallToBig :: SBV Action -> SBool Source #

Field recognizer predicate.

sCaseAction :: Mergeable result => SBV Action -> result -> result -> result -> result -> result -> result -> result -> result Source #

Case analyzer for the type Action.

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 big :: a small :: a action :: b

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)