sbv-13.1: 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

data Orangutan Source #

Orangutans in the puzzle.

Constructors

Merah 
Ofallo 
Quirrel 
Shamir 

Instances

Instances details
Arbitrary Orangutan Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Bounded Orangutan Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Enum Orangutan Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Show 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

EnumSymbolic 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 #

OrdSymbolic (SBV Orangutan) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

HasInductionSchema (Forall ta Orangutan -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

inductionSchema :: (Forall ta Orangutan -> SBool) -> ProofObj Source #

SymVal extraT => HasInductionSchema (Forall ta Orangutan -> Forall extraS extraT -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

inductionSchema :: (Forall ta Orangutan -> Forall extraS extraT -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta Orangutan -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

inductionSchema :: (Forall ta Orangutan -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta Orangutan -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

inductionSchema :: (Forall ta Orangutan -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta Orangutan -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

inductionSchema :: (Forall ta Orangutan -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta Orangutan -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

inductionSchema :: (Forall ta Orangutan -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

data Handler Source #

Handlers for each orangutan.

Constructors

Dolly 
Eva 
Francine 
Gracie 

Instances

Instances details
Arbitrary 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

EnumSymbolic 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 #

OrdSymbolic (SBV Handler) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

HasInductionSchema (Forall ta Handler -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

inductionSchema :: (Forall ta Handler -> SBool) -> ProofObj Source #

SymVal extraT => HasInductionSchema (Forall ta Handler -> Forall extraS extraT -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

inductionSchema :: (Forall ta Handler -> Forall extraS extraT -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta Handler -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

inductionSchema :: (Forall ta Handler -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta Handler -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

inductionSchema :: (Forall ta Handler -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta Handler -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

inductionSchema :: (Forall ta Handler -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta Handler -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

inductionSchema :: (Forall ta Handler -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

data Location Source #

Location for each orangutan.

Constructors

Ambalat 
Basahan 
Kendisi 
Tarakan 

Instances

Instances details
Arbitrary 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

EnumSymbolic 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 #

OrdSymbolic (SBV Location) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

HasInductionSchema (Forall ta Location -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

inductionSchema :: (Forall ta Location -> SBool) -> ProofObj Source #

SymVal extraT => HasInductionSchema (Forall ta Location -> Forall extraS extraT -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

inductionSchema :: (Forall ta Location -> Forall extraS extraT -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta Location -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

inductionSchema :: (Forall ta Location -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta Location -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

inductionSchema :: (Forall ta Location -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta Location -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

inductionSchema :: (Forall ta Location -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta Location -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Orangutans

Methods

inductionSchema :: (Forall ta Location -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

cv2Orangutan :: String -> [CV] -> Orangutan Source #

Conversion from SMT values to Orangutan values.

_undefiner_Orangutan :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

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.

isMerah :: SBV Orangutan -> SBool Source #

Field recognizer predicate.

isOfallo :: SBV Orangutan -> SBool Source #

Field recognizer predicate.

isQuirrel :: SBV Orangutan -> SBool Source #

Field recognizer predicate.

isShamir :: SBV Orangutan -> SBool Source #

Field recognizer predicate.

sCaseOrangutan :: Mergeable result => SBV Orangutan -> result -> result -> result -> result -> result Source #

Case analyzer for the type Orangutan.

cv2Handler :: String -> [CV] -> Handler Source #

Conversion from SMT values to Handler values.

_undefiner_Handler :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

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.

isDolly :: SBV Handler -> SBool Source #

Field recognizer predicate.

isEva :: SBV Handler -> SBool Source #

Field recognizer predicate.

isFrancine :: SBV Handler -> SBool Source #

Field recognizer predicate.

isGracie :: SBV Handler -> SBool Source #

Field recognizer predicate.

sCaseHandler :: Mergeable result => SBV Handler -> result -> result -> result -> result -> result Source #

Case analyzer for the type Handler.

cv2Location :: String -> [CV] -> Location Source #

Conversion from SMT values to Location values.

_undefiner_Location :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

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.

isAmbalat :: SBV Location -> SBool Source #

Field recognizer predicate.

isBasahan :: SBV Location -> SBool Source #

Field recognizer predicate.

isKendisi :: SBV Location -> SBool Source #

Field recognizer predicate.

isTarakan :: SBV Location -> SBool Source #

Field recognizer predicate.

sCaseLocation :: Mergeable result => SBV Location -> result -> result -> result -> result -> result Source #

Case analyzer for the type Location.

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-13.1-FRMD1KCFPWQ3DbBy4ZdTdB" '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-13.1-FRMD1KCFPWQ3DbBy4ZdTdB" '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.