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.KnightsAndKnaves

Description

From Raymond Smullyan: On a fictional island, all inhabitants are either knights, who always tell the truth, or knaves, who always lie. John and Bill are residents of the island of knights and knaves. John and Bill make several utterances. Determine which one is a knave or a knight, depending on their answers.

Synopsis

- data Inhabitant
- type SInhabitant = SBV Inhabitant
- data Identity
  - = Knave
  - | Knight
- type SIdentity = SBV Identity
- sKnight :: SBV Identity
- sKnave :: SBV Identity
- data Statement
  - = Truth
  - | Falsity
- type SStatement = SBV Statement
- sFalsity :: SBV Statement
- sTruth :: SBV Statement
- john :: SInhabitant
- bill :: SInhabitant
- is :: SInhabitant -> SIdentity -> SStatement
- says :: SInhabitant -> SStatement -> SBool
- holds :: SStatement -> SBool
- and :: SStatement -> SStatement -> SStatement
- not :: SStatement -> SStatement
- iff :: SStatement -> SStatement -> SStatement
- puzzle :: IO ()

# Documentation

data Inhabitant Source #

Inhabitants of the island, as an uninterpreted sort

#### Instances

Instances details

Data Inhabitant Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Inhabitant -> c Inhabitant Source #

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

toConstr :: Inhabitant -> Constr Source #

dataTypeOf :: Inhabitant -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Read Inhabitant Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods readsPrec :: Int -> ReadS Inhabitant Source # readList :: ReadS [Inhabitant] Source # readPrec :: ReadPrec Inhabitant Source # readListPrec :: ReadPrec [Inhabitant] Source #
Show Inhabitant Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves Methods showsPrec :: Int -> Inhabitant -> ShowS Source # show :: Inhabitant -> String Source # showList :: [Inhabitant] -> ShowS Source #
SymVal Inhabitant Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves

Methods

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

literal :: Inhabitant -> SBV Inhabitant Source #

fromCV :: CV -> Inhabitant Source #

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

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

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

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

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

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

unliteral :: SBV Inhabitant -> Maybe Inhabitant Source #

isConcrete :: SBV Inhabitant -> Bool Source #

isSymbolic :: SBV Inhabitant -> Bool Source #

HasKind Inhabitant Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves

Methods

kindOf :: Inhabitant -> Kind Source #

hasSign :: Inhabitant -> Bool Source #

intSizeOf :: Inhabitant -> Int Source #

isBoolean :: Inhabitant -> Bool Source #

isBounded :: Inhabitant -> Bool Source #

isReal :: Inhabitant -> Bool Source #

isFloat :: Inhabitant -> Bool Source #

isDouble :: Inhabitant -> Bool Source #

isRational :: Inhabitant -> Bool Source #

isFP :: Inhabitant -> Bool Source #

isUnbounded :: Inhabitant -> Bool Source #

isUserSort :: Inhabitant -> Bool Source #

isChar :: Inhabitant -> Bool Source #

isString :: Inhabitant -> Bool Source #

isList :: Inhabitant -> Bool Source #

isSet :: Inhabitant -> Bool Source #

isTuple :: Inhabitant -> Bool Source #

isMaybe :: Inhabitant -> Bool Source #

isEither :: Inhabitant -> Bool Source #

showType :: Inhabitant -> String Source #

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

type SInhabitant = SBV Inhabitant Source #

Symbolic version of the type `Inhabitant`.

data Identity Source #

Each inhabitant is either a knave or a knight

Constructors

Knave |
Knight |

#### Instances

Instances details

Data Identity Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Identity -> c Identity Source #

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

toConstr :: Identity -> Constr Source #

dataTypeOf :: Identity -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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

Instance details

Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves

Methods

compare :: Identity -> Identity -> Ordering Source #

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

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

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

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

max :: Identity -> Identity -> Identity Source #

min :: Identity -> Identity -> Identity Source #

SymVal Identity Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves

Methods

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

literal :: Identity -> SBV Identity Source #

fromCV :: CV -> Identity Source #

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

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

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

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

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

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

unliteral :: SBV Identity -> Maybe Identity Source #

isConcrete :: SBV Identity -> Bool Source #

isSymbolic :: SBV Identity -> Bool Source #

HasKind Identity Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves

Methods

kindOf :: Identity -> Kind Source #

hasSign :: Identity -> Bool Source #

intSizeOf :: Identity -> Int Source #

isBoolean :: Identity -> Bool Source #

isBounded :: Identity -> Bool Source #

isReal :: Identity -> Bool Source #

isFloat :: Identity -> Bool Source #

isDouble :: Identity -> Bool Source #

isRational :: Identity -> Bool Source #

isFP :: Identity -> Bool Source #

isUnbounded :: Identity -> Bool Source #

isUserSort :: Identity -> Bool Source #

isChar :: Identity -> Bool Source #

isString :: Identity -> Bool Source #

isList :: Identity -> Bool Source #

isSet :: Identity -> Bool Source #

isTuple :: Identity -> Bool Source #

isMaybe :: Identity -> Bool Source #

isEither :: Identity -> Bool Source #

showType :: Identity -> String Source #

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

type SIdentity = SBV Identity Source #

Symbolic version of the type `Identity`.

sKnight :: SBV Identity Source #

Symbolic version of the constructor `Knight`.

sKnave :: SBV Identity Source #

Symbolic version of the constructor `Knave`.

data Statement Source #

Statements are utterances which are either true or false

Constructors

Truth |
Falsity |

#### Instances

Instances details

Data Statement Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Statement -> c Statement Source #

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

toConstr :: Statement -> Constr Source #

dataTypeOf :: Statement -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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

Instance details

Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves

Methods

compare :: Statement -> Statement -> Ordering Source #

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

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

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

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

max :: Statement -> Statement -> Statement Source #

min :: Statement -> Statement -> Statement Source #

SymVal Statement Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves

Methods

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

literal :: Statement -> SBV Statement Source #

fromCV :: CV -> Statement Source #

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

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

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

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

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

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

unliteral :: SBV Statement -> Maybe Statement Source #

isConcrete :: SBV Statement -> Bool Source #

isSymbolic :: SBV Statement -> Bool Source #

HasKind Statement Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.KnightsAndKnaves

Methods

kindOf :: Statement -> Kind Source #

hasSign :: Statement -> Bool Source #

intSizeOf :: Statement -> Int Source #

isBoolean :: Statement -> Bool Source #

isBounded :: Statement -> Bool Source #

isReal :: Statement -> Bool Source #

isFloat :: Statement -> Bool Source #

isDouble :: Statement -> Bool Source #

isRational :: Statement -> Bool Source #

isFP :: Statement -> Bool Source #

isUnbounded :: Statement -> Bool Source #

isUserSort :: Statement -> Bool Source #

isChar :: Statement -> Bool Source #

isString :: Statement -> Bool Source #

isList :: Statement -> Bool Source #

isSet :: Statement -> Bool Source #

isTuple :: Statement -> Bool Source #

isMaybe :: Statement -> Bool Source #

isEither :: Statement -> Bool Source #

showType :: Statement -> String Source #

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

type SStatement = SBV Statement Source #

Symbolic version of the type `Statement`.

sFalsity :: SBV Statement Source #

Symbolic version of the constructor `Falsity`.

sTruth :: SBV Statement Source #

Symbolic version of the constructor `Truth`.

john :: SInhabitant Source #

John is an inhabitant of the island.

bill :: SInhabitant Source #

Bill is an inhabitant of the island.

is :: SInhabitant -> SIdentity -> SStatement Source #

The connective `is` makes a statement about an inhabitant regarding his/her identity.

says :: SInhabitant -> SStatement -> SBool Source #

The connective `says` makes a predicate from what an inhabitant states

holds :: SStatement -> SBool Source #

The connective `holds` is will be true if the statement is true

and :: SStatement -> SStatement -> SStatement Source #

The connective `and` creates the conjunction of two statements

not :: SStatement -> SStatement Source #

The connective `not` negates a statement

iff :: SStatement -> SStatement -> SStatement Source #

The connective `iff` creates a statement that equates the truth values of its argument statements

puzzle :: IO () Source #

Encode Smullyan's puzzle. We have:

    >>> puzzle
    Question 1.
      John says, We are both knaves
        Then, John is: Knave
        And,  Bill is: Knight
    Question 2.
      John says If (and only if) Bill is a knave, then I am a knave.
      Bill says We are of different kinds.
        Then, John is: Knave
        And,  Bill is: Knight