Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
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

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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Rabbit # toConstr :: Rabbit -> Constr # dataTypeOf :: Rabbit -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Rabbit) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Rabbit) # gmapT :: (forall b. Data b => b -> b) -> Rabbit -> Rabbit # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Rabbit -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Rabbit -> r # gmapQ :: (forall d. Data d => d -> u) -> Rabbit -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Rabbit -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Rabbit -> m Rabbit # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Rabbit -> m Rabbit # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Rabbit -> m Rabbit #
Read Rabbit Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Rabbits Methods readsPrec :: Int -> ReadS Rabbit # readList :: ReadS [Rabbit] # readPrec :: ReadPrec Rabbit # readListPrec :: ReadPrec [Rabbit] #
Show Rabbit Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Rabbits Methods showsPrec :: Int -> Rabbit -> ShowS # show :: Rabbit -> String # showList :: [Rabbit] -> ShowS #
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.