sbv-10.9: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.Puzzles.Orangutans

Description

Synopsis

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 #

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

toConstr :: Orangutan -> Constr #

dataTypeOf :: Orangutan -> DataType #

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

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

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

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

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

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

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

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

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

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

Bounded Orangutan Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Enum Orangutan Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Read Orangutan Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Show Orangutan Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Eq Orangutan Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Ord Orangutan Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

SymVal Orangutan Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

HasKind Orangutan Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

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 #

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

toConstr :: Handler -> Constr #

dataTypeOf :: Handler -> DataType #

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

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

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

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

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

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

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

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

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

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

Read Handler Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Show Handler Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Eq Handler Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

(==) :: Handler -> Handler -> Bool #

(/=) :: Handler -> Handler -> Bool #

Ord Handler Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

SymVal Handler Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

HasKind Handler Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

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 #

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

toConstr :: Location -> Constr #

dataTypeOf :: Location -> DataType #

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

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

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

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

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

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

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

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

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

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

Read Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Show Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Eq Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Ord Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

SymVal Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

HasKind Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

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.

sMerah :: SBV Orangutan Source #

Symbolic version of the constructor Merah.

sOfallo :: SBV Orangutan Source #

Symbolic version of the constructor Ofallo.

sQuirrel :: SBV Orangutan Source #

Symbolic version of the constructor Quirrel.

sShamir :: SBV Orangutan Source #

Symbolic version of the constructor Shamir.

type SHandler = SBV Handler Source #

Symbolic version of the type Handler.

sDolly :: SBV Handler Source #

Symbolic version of the constructor Dolly.

sEva :: SBV Handler Source #

Symbolic version of the constructor Eva.

sFrancine :: SBV Handler Source #

Symbolic version of the constructor Francine.

sGracie :: SBV Handler Source #

Symbolic version of the constructor Gracie.

type SLocation = SBV Location Source #

Symbolic version of the type Location.

sAmbalat :: SBV Location Source #

Symbolic version of the constructor Ambalat.

sBasahan :: SBV Location Source #

Symbolic version of the constructor Basahan.

sKendisi :: SBV Location Source #

Symbolic version of the constructor Kendisi.

sTarakan :: SBV Location Source #

Symbolic version of the constructor Tarakan.

data Assignment Source #

An assignment is solution to the puzzle

Instances

Instances details
Generic Assignment Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Associated Types

type Rep Assignment 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

type Rep Assignment = D1 ('MetaData "Assignment" "Documentation.SBV.Examples.Puzzles.Orangutans" "sbv-10.9-inplace" '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))))
Mergeable Assignment Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

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.9-inplace" '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.