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

Description

A puzzle, attributed to Lewis Caroll:

- All rabbits, that are not greedy, are black
- No old rabbits are free from greediness
- Therefore: Some black rabbits are not old

What's implicit here is that there is a rabbit that must be not-greedy; which we add to our constraints.

Synopsis

- data Rabbit
- type SRabbit = SBV Rabbit
- greedy :: SRabbit -> SBool
- black :: SRabbit -> SBool
- old :: SRabbit -> SBool
- rabbits :: Predicate
- rabbitsAreOK :: IO ThmResult

# Documentation

data Rabbit Source #

A universe of rabbits

#### Instances

Instances details

Data Rabbit Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Rabbits

Methods

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

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

toConstr :: Rabbit -> Constr Source #

dataTypeOf :: Rabbit -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Rabbits

Methods

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

literal :: Rabbit -> SBV Rabbit Source #

fromCV :: CV -> Rabbit Source #

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

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

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

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

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

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

unliteral :: SBV Rabbit -> Maybe Rabbit Source #

isConcrete :: SBV Rabbit -> Bool Source #

isSymbolic :: SBV Rabbit -> Bool Source #

HasKind Rabbit Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Rabbits

Methods

kindOf :: Rabbit -> Kind Source #

hasSign :: Rabbit -> Bool Source #

intSizeOf :: Rabbit -> Int Source #

isBoolean :: Rabbit -> Bool Source #

isBounded :: Rabbit -> Bool Source #

isReal :: Rabbit -> Bool Source #

isFloat :: Rabbit -> Bool Source #

isDouble :: Rabbit -> Bool Source #

isRational :: Rabbit -> Bool Source #

isFP :: Rabbit -> Bool Source #

isUnbounded :: Rabbit -> Bool Source #

isUserSort :: Rabbit -> Bool Source #

isChar :: Rabbit -> Bool Source #

isString :: Rabbit -> Bool Source #

isList :: Rabbit -> Bool Source #

isSet :: Rabbit -> Bool Source #

isTuple :: Rabbit -> Bool Source #

isMaybe :: Rabbit -> Bool Source #

isEither :: Rabbit -> Bool Source #

showType :: Rabbit -> String Source #

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

type SRabbit = SBV Rabbit Source #

Symbolic version of the type `Rabbit`.

greedy :: SRabbit -> SBool Source #

Identify those rabbits that are greedy. Note that we leave the predicate uninterpreted.

black :: SRabbit -> SBool Source #

Identify those rabbits that are black. Note that we leave the predicate uninterpreted.

old :: SRabbit -> SBool Source #

Identify those rabbits that are old. Note that we leave the predicate uninterpreted.

rabbits :: Predicate Source #

Express the puzzle.

rabbitsAreOK :: IO ThmResult Source #

Prove the claim. We have:

    >>> rabbitsAreOK
    Q.E.D.