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

Description

Based on http://github.com/goldfirere/video-resources/blob/main/2022-08-12-java/Haskell.hs

Synopsis

- data Orangutan
  - = Merah
  - | Ofallo
  - | Quirrel
  - | Shamir
- data Handler
  - = Dolly
  - | Eva
  - | Francine
  - | Gracie
- data Location
  - = Ambalat
  - | Basahan
  - | Kendisi
  - | Tarakan
- type SOrangutan = SBV Orangutan
- sShamir :: SBV Orangutan
- sQuirrel :: SBV Orangutan
- sOfallo :: SBV Orangutan
- sMerah :: SBV Orangutan
- type SHandler = SBV Handler
- sGracie :: SBV Handler
- sFrancine :: SBV Handler
- sEva :: SBV Handler
- sDolly :: SBV Handler
- type SLocation = SBV Location
- sTarakan :: SBV Location
- sKendisi :: SBV Location
- sBasahan :: SBV Location
- sAmbalat :: SBV Location
- data Assignment = MkAssignment {
  - orangutan :: SOrangutan
  - handler :: SHandler
  - location :: SLocation
  - age :: SInteger
  }
- mkSym :: Orangutan -> Symbolic Assignment
- puzzle :: ConstraintSet

# Documentation

    >>> -- For doctest purposes only:
    >>> import Data.SBV

data Orangutan Source #

Orangutans in the puzzle.

Constructors

Merah |
Ofallo |
Quirrel |
Shamir |

#### Instances

Instances details

Data Orangutan Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

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

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

toConstr :: Orangutan -> Constr Source #

dataTypeOf :: Orangutan -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Bounded Orangutan Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Orangutans Methods minBound :: Orangutan Source # maxBound :: Orangutan Source #
Enum Orangutan Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

succ :: Orangutan -> Orangutan Source #

pred :: Orangutan -> Orangutan Source #

toEnum :: Int -> Orangutan Source #

fromEnum :: Orangutan -> Int Source #

enumFrom :: Orangutan -> [Orangutan] Source #

enumFromThen :: Orangutan -> Orangutan -> [Orangutan] Source #

enumFromTo :: Orangutan -> Orangutan -> [Orangutan] Source #

enumFromThenTo :: Orangutan -> Orangutan -> Orangutan -> [Orangutan] Source #

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

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

compare :: Orangutan -> Orangutan -> Ordering Source #

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

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

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

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

max :: Orangutan -> Orangutan -> Orangutan Source #

min :: Orangutan -> Orangutan -> Orangutan Source #

SymVal Orangutan Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

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

literal :: Orangutan -> SBV Orangutan Source #

fromCV :: CV -> Orangutan Source #

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

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

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

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

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

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

unliteral :: SBV Orangutan -> Maybe Orangutan Source #

isConcrete :: SBV Orangutan -> Bool Source #

isSymbolic :: SBV Orangutan -> Bool Source #

HasKind Orangutan Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

kindOf :: Orangutan -> Kind Source #

hasSign :: Orangutan -> Bool Source #

intSizeOf :: Orangutan -> Int Source #

isBoolean :: Orangutan -> Bool Source #

isBounded :: Orangutan -> Bool Source #

isReal :: Orangutan -> Bool Source #

isFloat :: Orangutan -> Bool Source #

isDouble :: Orangutan -> Bool Source #

isRational :: Orangutan -> Bool Source #

isFP :: Orangutan -> Bool Source #

isUnbounded :: Orangutan -> Bool Source #

isUserSort :: Orangutan -> Bool Source #

isChar :: Orangutan -> Bool Source #

isString :: Orangutan -> Bool Source #

isList :: Orangutan -> Bool Source #

isSet :: Orangutan -> Bool Source #

isTuple :: Orangutan -> Bool Source #

isMaybe :: Orangutan -> Bool Source #

isEither :: Orangutan -> Bool Source #

showType :: Orangutan -> String Source #

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

data Handler Source #

Handlers for each orangutan.

Constructors

Dolly |
Eva |
Francine |
Gracie |

#### Instances

Instances details

Data Handler Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

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

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

toConstr :: Handler -> Constr Source #

dataTypeOf :: Handler -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Read Handler Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Orangutans Methods readsPrec :: Int -> ReadS Handler Source # readList :: ReadS [Handler] Source # readPrec :: ReadPrec Handler Source # readListPrec :: ReadPrec [Handler] Source #
Show Handler Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Orangutans Methods showsPrec :: Int -> Handler -> ShowS Source # show :: Handler -> String Source # showList :: [Handler] -> ShowS Source #
Eq Handler Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Orangutans Methods (==) :: Handler -> Handler -> Bool Source # (/=) :: Handler -> Handler -> Bool Source #
Ord Handler Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Orangutans Methods compare :: Handler -> Handler -> Ordering Source # (<) :: Handler -> Handler -> Bool Source # (<=) :: Handler -> Handler -> Bool Source # (>) :: Handler -> Handler -> Bool Source # (>=) :: Handler -> Handler -> Bool Source # max :: Handler -> Handler -> Handler Source # min :: Handler -> Handler -> Handler Source #
SymVal Handler Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

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

literal :: Handler -> SBV Handler Source #

fromCV :: CV -> Handler Source #

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

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

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

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

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

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

unliteral :: SBV Handler -> Maybe Handler Source #

isConcrete :: SBV Handler -> Bool Source #

isSymbolic :: SBV Handler -> Bool Source #

HasKind Handler Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

kindOf :: Handler -> Kind Source #

hasSign :: Handler -> Bool Source #

intSizeOf :: Handler -> Int Source #

isBoolean :: Handler -> Bool Source #

isBounded :: Handler -> Bool Source #

isReal :: Handler -> Bool Source #

isFloat :: Handler -> Bool Source #

isDouble :: Handler -> Bool Source #

isRational :: Handler -> Bool Source #

isFP :: Handler -> Bool Source #

isUnbounded :: Handler -> Bool Source #

isUserSort :: Handler -> Bool Source #

isChar :: Handler -> Bool Source #

isString :: Handler -> Bool Source #

isList :: Handler -> Bool Source #

isSet :: Handler -> Bool Source #

isTuple :: Handler -> Bool Source #

isMaybe :: Handler -> Bool Source #

isEither :: Handler -> Bool Source #

showType :: Handler -> String Source #

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

data Location Source #

Location for each orangutan.

Constructors

Ambalat |
Basahan |
Kendisi |
Tarakan |

#### Instances

Instances details

Data Location Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

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

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

toConstr :: Location -> Constr Source #

dataTypeOf :: Location -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

compare :: Location -> Location -> Ordering Source #

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

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

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

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

max :: Location -> Location -> Location Source #

min :: Location -> Location -> Location Source #

SymVal Location Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

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

literal :: Location -> SBV Location Source #

fromCV :: CV -> Location Source #

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

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

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

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

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

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

unliteral :: SBV Location -> Maybe Location Source #

isConcrete :: SBV Location -> Bool Source #

isSymbolic :: SBV Location -> Bool Source #

HasKind Location Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

kindOf :: Location -> Kind Source #

hasSign :: Location -> Bool Source #

intSizeOf :: Location -> Int Source #

isBoolean :: Location -> Bool Source #

isBounded :: Location -> Bool Source #

isReal :: Location -> Bool Source #

isFloat :: Location -> Bool Source #

isDouble :: Location -> Bool Source #

isRational :: Location -> Bool Source #

isFP :: Location -> Bool Source #

isUnbounded :: Location -> Bool Source #

isUserSort :: Location -> Bool Source #

isChar :: Location -> Bool Source #

isString :: Location -> Bool Source #

isList :: Location -> Bool Source #

isSet :: Location -> Bool Source #

isTuple :: Location -> Bool Source #

isMaybe :: Location -> Bool Source #

isEither :: Location -> Bool Source #

showType :: Location -> String Source #

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

type SOrangutan = SBV Orangutan Source #

Symbolic version of the type `Orangutan`.

sShamir :: SBV Orangutan Source #

Symbolic version of the constructor `Shamir`.

sQuirrel :: SBV Orangutan Source #

Symbolic version of the constructor `Quirrel`.

sOfallo :: SBV Orangutan Source #

Symbolic version of the constructor `Ofallo`.

sMerah :: SBV Orangutan Source #

Symbolic version of the constructor `Merah`.

type SHandler = SBV Handler Source #

Symbolic version of the type `Handler`.

sGracie :: SBV Handler Source #

Symbolic version of the constructor `Gracie`.

sFrancine :: SBV Handler Source #

Symbolic version of the constructor `Francine`.

sEva :: SBV Handler Source #

Symbolic version of the constructor `Eva`.

sDolly :: SBV Handler Source #

Symbolic version of the constructor `Dolly`.

type SLocation = SBV Location Source #

Symbolic version of the type `Location`.

sTarakan :: SBV Location Source #

Symbolic version of the constructor `Tarakan`.

sKendisi :: SBV Location Source #

Symbolic version of the constructor `Kendisi`.

sBasahan :: SBV Location Source #

Symbolic version of the constructor `Basahan`.

sAmbalat :: SBV Location Source #

Symbolic version of the constructor `Ambalat`.

data Assignment Source #

An assignment is solution to the puzzle

Constructors

MkAssignment |

Fields

- orangutan :: SOrangutan
- handler :: SHandler
- location :: SLocation
- age :: SInteger

#### Instances

Instances details

Generic Assignment Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Orangutans Associated Types type Rep Assignment :: Type -> Type Source # Methods from :: Assignment -> Rep Assignment x Source # to :: Rep Assignment x -> Assignment Source #
Mergeable Assignment Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Orangutans Methods symbolicMerge :: Bool -> SBool -> Assignment -> Assignment -> Assignment Source # select :: (Ord b, SymVal b, Num b) => [Assignment] -> Assignment -> SBV b -> Assignment Source #
type Rep Assignment Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

type Rep Assignment = D1 ('MetaData "Assignment" "Documentation.SBV.Examples.Puzzles.Orangutans" "sbv-10.2-Gi6nXbGJVKyDE1oJouGknK" 'False) (C1 ('MetaCons "MkAssignment" 'PrefixI 'True) ((S1 ('MetaSel ('Just "orangutan") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SOrangutan) :*: S1 ('MetaSel ('Just "handler") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SHandler)) :*: (S1 ('MetaSel ('Just "location") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SLocation) :*: S1 ('MetaSel ('Just "age") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SInteger))))

mkSym :: Orangutan -> Symbolic Assignment Source #

Create a symbolic assignment, using symbolic fields.

puzzle :: ConstraintSet Source #

We get:

    >>> allSat puzzle
    Solution #1:
      Merah.handler    =   Gracie :: Handler
      Merah.location   =  Tarakan :: Location
      Merah.age        =       10 :: Integer
      Ofallo.handler   =      Eva :: Handler
      Ofallo.location  =  Kendisi :: Location
      Ofallo.age       =       13 :: Integer
      Quirrel.handler  =    Dolly :: Handler
      Quirrel.location =  Basahan :: Location
      Quirrel.age      =        4 :: Integer
      Shamir.handler   = Francine :: Handler
      Shamir.location  =  Ambalat :: Location
      Shamir.age       =        7 :: Integer
    This is the only solution.