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

Description

Solves the following logic puzzle, attributed to Albert Einstein:

- The Briton lives in the red house.
- The Swede keeps dogs as pets.
- The Dane drinks tea.
- The green house is left to the white house.
- The owner of the green house drinks coffee.
- The person who plays football rears birds.
- The owner of the yellow house plays baseball.
- The man living in the center house drinks milk.
- The Norwegian lives in the first house.
- The man who plays volleyball lives next to the one who keeps cats.
- The man who keeps the horse lives next to the one who plays baseball.
- The owner who plays tennis drinks beer.
- The German plays hockey.
- The Norwegian lives next to the blue house.
- The man who plays volleyball has a neighbor who drinks water.

Who owns the fish?

Synopsis

- data Color
  - = Red
  - | Green
  - | White
  - | Yellow
  - | Blue
- type SColor = SBV Color
- sBlue :: SBV Color
- sYellow :: SBV Color
- sWhite :: SBV Color
- sGreen :: SBV Color
- sRed :: SBV Color
- data Nationality
  - = Briton
  - | Dane
  - | Swede
  - | Norwegian
  - | German
- type SNationality = SBV Nationality
- sGerman :: SBV Nationality
- sNorwegian :: SBV Nationality
- sSwede :: SBV Nationality
- sDane :: SBV Nationality
- sBriton :: SBV Nationality
- data Beverage
  - = Tea
  - | Coffee
  - | Milk
  - | Beer
  - | Water
- type SBeverage = SBV Beverage
- sWater :: SBV Beverage
- sBeer :: SBV Beverage
- sMilk :: SBV Beverage
- sCoffee :: SBV Beverage
- sTea :: SBV Beverage
- data Pet
  - = Dog
  - | Horse
  - | Cat
  - | Bird
  - | Fish
- type SPet = SBV Pet
- sFish :: SBV Pet
- sBird :: SBV Pet
- sCat :: SBV Pet
- sHorse :: SBV Pet
- sDog :: SBV Pet
- data Sport
  - = Football
  - | Baseball
  - | Volleyball
  - | Hockey
  - | Tennis
- type SSport = SBV Sport
- sTennis :: SBV Sport
- sHockey :: SBV Sport
- sVolleyball :: SBV Sport
- sBaseball :: SBV Sport
- sFootball :: SBV Sport
- fishOwner :: IO ()

# Documentation

data Color Source #

Colors of houses

Constructors

Red |
Green |
White |
Yellow |
Blue |

#### Instances

Instances details

Data Color Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

toConstr :: Color -> Constr Source #

dataTypeOf :: Color -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

literal :: Color -> SBV Color Source #

fromCV :: CV -> Color Source #

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

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

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

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

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

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

unliteral :: SBV Color -> Maybe Color Source #

isConcrete :: SBV Color -> Bool Source #

isSymbolic :: SBV Color -> Bool Source #

HasKind Color Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

kindOf :: Color -> Kind Source #

hasSign :: Color -> Bool Source #

intSizeOf :: Color -> Int Source #

isBoolean :: Color -> Bool Source #

isBounded :: Color -> Bool Source #

isReal :: Color -> Bool Source #

isFloat :: Color -> Bool Source #

isDouble :: Color -> Bool Source #

isRational :: Color -> Bool Source #

isFP :: Color -> Bool Source #

isUnbounded :: Color -> Bool Source #

isUserSort :: Color -> Bool Source #

isChar :: Color -> Bool Source #

isString :: Color -> Bool Source #

isList :: Color -> Bool Source #

isSet :: Color -> Bool Source #

isTuple :: Color -> Bool Source #

isMaybe :: Color -> Bool Source #

isEither :: Color -> Bool Source #

showType :: Color -> String Source #

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

type SColor = SBV Color Source #

Symbolic version of the type `Color`.

sBlue :: SBV Color Source #

Symbolic version of the constructor `Blue`.

sYellow :: SBV Color Source #

Symbolic version of the constructor `Yellow`.

sWhite :: SBV Color Source #

Symbolic version of the constructor `White`.

sGreen :: SBV Color Source #

Symbolic version of the constructor `Green`.

sRed :: SBV Color Source #

Symbolic version of the constructor `Red`.

data Nationality Source #

Nationalities of the occupants

Constructors

Briton |
Dane |
Swede |
Norwegian |
German |

#### Instances

Instances details

Data Nationality Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

toConstr :: Nationality -> Constr Source #

dataTypeOf :: Nationality -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

compare :: Nationality -> Nationality -> Ordering Source #

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

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

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

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

max :: Nationality -> Nationality -> Nationality Source #

min :: Nationality -> Nationality -> Nationality Source #

SymVal Nationality Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

literal :: Nationality -> SBV Nationality Source #

fromCV :: CV -> Nationality Source #

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

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

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

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

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

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

unliteral :: SBV Nationality -> Maybe Nationality Source #

isConcrete :: SBV Nationality -> Bool Source #

isSymbolic :: SBV Nationality -> Bool Source #

HasKind Nationality Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

kindOf :: Nationality -> Kind Source #

hasSign :: Nationality -> Bool Source #

intSizeOf :: Nationality -> Int Source #

isBoolean :: Nationality -> Bool Source #

isBounded :: Nationality -> Bool Source #

isReal :: Nationality -> Bool Source #

isFloat :: Nationality -> Bool Source #

isDouble :: Nationality -> Bool Source #

isRational :: Nationality -> Bool Source #

isFP :: Nationality -> Bool Source #

isUnbounded :: Nationality -> Bool Source #

isUserSort :: Nationality -> Bool Source #

isChar :: Nationality -> Bool Source #

isString :: Nationality -> Bool Source #

isList :: Nationality -> Bool Source #

isSet :: Nationality -> Bool Source #

isTuple :: Nationality -> Bool Source #

isMaybe :: Nationality -> Bool Source #

isEither :: Nationality -> Bool Source #

showType :: Nationality -> String Source #

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

type SNationality = SBV Nationality Source #

Symbolic version of the type `Nationality`.

sGerman :: SBV Nationality Source #

Symbolic version of the constructor `German`.

sNorwegian :: SBV Nationality Source #

Symbolic version of the constructor `Norwegian`.

sSwede :: SBV Nationality Source #

Symbolic version of the constructor `Swede`.

sDane :: SBV Nationality Source #

Symbolic version of the constructor `Dane`.

sBriton :: SBV Nationality Source #

Symbolic version of the constructor `Briton`.

data Beverage Source #

Beverage choices

Constructors

Tea |
Coffee |
Milk |
Beer |
Water |

#### Instances

Instances details

Data Beverage Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

toConstr :: Beverage -> Constr Source #

dataTypeOf :: Beverage -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

compare :: Beverage -> Beverage -> Ordering Source #

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

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

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

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

max :: Beverage -> Beverage -> Beverage Source #

min :: Beverage -> Beverage -> Beverage Source #

SymVal Beverage Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

literal :: Beverage -> SBV Beverage Source #

fromCV :: CV -> Beverage Source #

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

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

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

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

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

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

unliteral :: SBV Beverage -> Maybe Beverage Source #

isConcrete :: SBV Beverage -> Bool Source #

isSymbolic :: SBV Beverage -> Bool Source #

HasKind Beverage Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

kindOf :: Beverage -> Kind Source #

hasSign :: Beverage -> Bool Source #

intSizeOf :: Beverage -> Int Source #

isBoolean :: Beverage -> Bool Source #

isBounded :: Beverage -> Bool Source #

isReal :: Beverage -> Bool Source #

isFloat :: Beverage -> Bool Source #

isDouble :: Beverage -> Bool Source #

isRational :: Beverage -> Bool Source #

isFP :: Beverage -> Bool Source #

isUnbounded :: Beverage -> Bool Source #

isUserSort :: Beverage -> Bool Source #

isChar :: Beverage -> Bool Source #

isString :: Beverage -> Bool Source #

isList :: Beverage -> Bool Source #

isSet :: Beverage -> Bool Source #

isTuple :: Beverage -> Bool Source #

isMaybe :: Beverage -> Bool Source #

isEither :: Beverage -> Bool Source #

showType :: Beverage -> String Source #

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

type SBeverage = SBV Beverage Source #

Symbolic version of the type `Beverage`.

sWater :: SBV Beverage Source #

Symbolic version of the constructor `Water`.

sBeer :: SBV Beverage Source #

Symbolic version of the constructor `Beer`.

sMilk :: SBV Beverage Source #

Symbolic version of the constructor `Milk`.

sCoffee :: SBV Beverage Source #

Symbolic version of the constructor `Coffee`.

sTea :: SBV Beverage Source #

Symbolic version of the constructor `Tea`.

data Pet Source #

Pets they keep

Constructors

Dog |
Horse |
Cat |
Bird |
Fish |

#### Instances

Instances details

Data Pet Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

toConstr :: Pet -> Constr Source #

dataTypeOf :: Pet -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

literal :: Pet -> SBV Pet Source #

fromCV :: CV -> Pet Source #

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

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

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

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

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

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

unliteral :: SBV Pet -> Maybe Pet Source #

isConcrete :: SBV Pet -> Bool Source #

isSymbolic :: SBV Pet -> Bool Source #

HasKind Pet Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

kindOf :: Pet -> Kind Source #

hasSign :: Pet -> Bool Source #

intSizeOf :: Pet -> Int Source #

isBoolean :: Pet -> Bool Source #

isBounded :: Pet -> Bool Source #

isReal :: Pet -> Bool Source #

isFloat :: Pet -> Bool Source #

isDouble :: Pet -> Bool Source #

isRational :: Pet -> Bool Source #

isFP :: Pet -> Bool Source #

isUnbounded :: Pet -> Bool Source #

isUserSort :: Pet -> Bool Source #

isChar :: Pet -> Bool Source #

isString :: Pet -> Bool Source #

isList :: Pet -> Bool Source #

isSet :: Pet -> Bool Source #

isTuple :: Pet -> Bool Source #

isMaybe :: Pet -> Bool Source #

isEither :: Pet -> Bool Source #

showType :: Pet -> String Source #

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

type SPet = SBV Pet Source #

Symbolic version of the type `Pet`.

sFish :: SBV Pet Source #

Symbolic version of the constructor `Fish`.

sBird :: SBV Pet Source #

Symbolic version of the constructor `Bird`.

sCat :: SBV Pet Source #

Symbolic version of the constructor `Cat`.

sHorse :: SBV Pet Source #

Symbolic version of the constructor `Horse`.

sDog :: SBV Pet Source #

Symbolic version of the constructor `Dog`.

data Sport Source #

Sports they engage in

Constructors

Football |
Baseball |
Volleyball |
Hockey |
Tennis |

#### Instances

Instances details

Data Sport Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

toConstr :: Sport -> Constr Source #

dataTypeOf :: Sport -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

literal :: Sport -> SBV Sport Source #

fromCV :: CV -> Sport Source #

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

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

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

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

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

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

unliteral :: SBV Sport -> Maybe Sport Source #

isConcrete :: SBV Sport -> Bool Source #

isSymbolic :: SBV Sport -> Bool Source #

HasKind Sport Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

kindOf :: Sport -> Kind Source #

hasSign :: Sport -> Bool Source #

intSizeOf :: Sport -> Int Source #

isBoolean :: Sport -> Bool Source #

isBounded :: Sport -> Bool Source #

isReal :: Sport -> Bool Source #

isFloat :: Sport -> Bool Source #

isDouble :: Sport -> Bool Source #

isRational :: Sport -> Bool Source #

isFP :: Sport -> Bool Source #

isUnbounded :: Sport -> Bool Source #

isUserSort :: Sport -> Bool Source #

isChar :: Sport -> Bool Source #

isString :: Sport -> Bool Source #

isList :: Sport -> Bool Source #

isSet :: Sport -> Bool Source #

isTuple :: Sport -> Bool Source #

isMaybe :: Sport -> Bool Source #

isEither :: Sport -> Bool Source #

showType :: Sport -> String Source #

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

type SSport = SBV Sport Source #

Symbolic version of the type `Sport`.

sTennis :: SBV Sport Source #

Symbolic version of the constructor `Tennis`.

sHockey :: SBV Sport Source #

Symbolic version of the constructor `Hockey`.

sVolleyball :: SBV Sport Source #

Symbolic version of the constructor `Volleyball`.

sBaseball :: SBV Sport Source #

Symbolic version of the constructor `Baseball`.

sFootball :: SBV Sport Source #

Symbolic version of the constructor `Football`.

fishOwner :: IO () Source #

We have:

    >>> fishOwner
    German

It's not hard to modify this program to grab the values of all the assignments, i.e., the full solution to the puzzle. We leave that as an exercise to the interested reader! NB. We use the `allSatTrackUFs` configuration to indicate that the uninterpreted function changes do not matter for generating different values. All we care is that the fishOwner changes!