sbv-8.7: 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.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

Documentation

data Color Source #

Colors of houses

Constructors

Red 
Green 
White 
Yellow 
Blue 

Instances

Instances details
Eq Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

(==) :: Color -> Color -> Bool

(/=) :: Color -> Color -> Bool

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

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

toConstr :: Color -> Constr

dataTypeOf :: Color -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

compare :: Color -> Color -> Ordering

(<) :: Color -> Color -> Bool

(<=) :: Color -> Color -> Bool

(>) :: Color -> Color -> Bool

(>=) :: Color -> Color -> Bool

max :: Color -> Color -> Color

min :: Color -> Color -> Color

Read Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

readsPrec :: Int -> ReadS Color

readList :: ReadS [Color]

readPrec :: ReadPrec Color

readListPrec :: ReadPrec [Color]

Show Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

showsPrec :: Int -> Color -> ShowS

show :: Color -> String

showList :: [Color] -> ShowS

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 #

isUnbounded :: Color -> Bool Source #

isUninterpreted :: 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 #

SymVal Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

literal :: Color -> SBV Color Source #

fromCV :: CV -> Color Source #

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

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

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

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

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

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

mkExistVars :: MonadSymbolic m => Int -> m [SBV Color] 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 #

SatModel Color Source #

Make Color a symbolic value.

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 #

data Nationality Source #

Nationalities of the occupants

Constructors

Briton 
Dane 
Swede 
Norwegian 
German 

Instances

Instances details
Eq Nationality Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

(/=) :: Nationality -> Nationality -> Bool

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

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

toConstr :: Nationality -> Constr

dataTypeOf :: Nationality -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Nationality Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Read Nationality Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

readsPrec :: Int -> ReadS Nationality

readList :: ReadS [Nationality]

readPrec :: ReadPrec Nationality

readListPrec :: ReadPrec [Nationality]

Show Nationality Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

showsPrec :: Int -> Nationality -> ShowS

show :: Nationality -> String

showList :: [Nationality] -> ShowS

HasKind Nationality Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SymVal Nationality Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SatModel Nationality Source #

Make Nationality a symbolic value.

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 #

data Beverage Source #

Beverage choices

Constructors

Tea 
Coffee 
Milk 
Beer 
Water 

Instances

Instances details
Eq Beverage Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

(/=) :: Beverage -> Beverage -> Bool

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

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

toConstr :: Beverage -> Constr

dataTypeOf :: Beverage -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Beverage Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

compare :: Beverage -> Beverage -> Ordering

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

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

(>) :: Beverage -> Beverage -> Bool

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

max :: Beverage -> Beverage -> Beverage

min :: Beverage -> Beverage -> Beverage

Read Beverage Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

readsPrec :: Int -> ReadS Beverage

readList :: ReadS [Beverage]

readPrec :: ReadPrec Beverage

readListPrec :: ReadPrec [Beverage]

Show Beverage Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

showsPrec :: Int -> Beverage -> ShowS

show :: Beverage -> String

showList :: [Beverage] -> ShowS

HasKind Beverage Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SymVal Beverage Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SatModel Beverage Source #

Make Beverage a symbolic value.

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 #

data Pet Source #

Pets they keep

Constructors

Dog 
Horse 
Cat 
Bird 
Fish 

Instances

Instances details
Eq Pet Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

(==) :: Pet -> Pet -> Bool

(/=) :: Pet -> Pet -> Bool

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

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

toConstr :: Pet -> Constr

dataTypeOf :: Pet -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Pet Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

compare :: Pet -> Pet -> Ordering

(<) :: Pet -> Pet -> Bool

(<=) :: Pet -> Pet -> Bool

(>) :: Pet -> Pet -> Bool

(>=) :: Pet -> Pet -> Bool

max :: Pet -> Pet -> Pet

min :: Pet -> Pet -> Pet

Read Pet Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

readsPrec :: Int -> ReadS Pet

readList :: ReadS [Pet]

readPrec :: ReadPrec Pet

readListPrec :: ReadPrec [Pet]

Show Pet Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

showsPrec :: Int -> Pet -> ShowS

show :: Pet -> String

showList :: [Pet] -> ShowS

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 #

isUnbounded :: Pet -> Bool Source #

isUninterpreted :: 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 #

SymVal Pet Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

literal :: Pet -> SBV Pet Source #

fromCV :: CV -> Pet Source #

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

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

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

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

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

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

mkExistVars :: MonadSymbolic m => Int -> m [SBV Pet] 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 #

SatModel Pet Source #

Make Pet a symbolic value.

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 #

data Sport Source #

Sports they engage in

Instances

Instances details
Eq Sport Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

(==) :: Sport -> Sport -> Bool

(/=) :: Sport -> Sport -> Bool

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

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

toConstr :: Sport -> Constr

dataTypeOf :: Sport -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Sport Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

compare :: Sport -> Sport -> Ordering

(<) :: Sport -> Sport -> Bool

(<=) :: Sport -> Sport -> Bool

(>) :: Sport -> Sport -> Bool

(>=) :: Sport -> Sport -> Bool

max :: Sport -> Sport -> Sport

min :: Sport -> Sport -> Sport

Read Sport Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

readsPrec :: Int -> ReadS Sport

readList :: ReadS [Sport]

readPrec :: ReadPrec Sport

readListPrec :: ReadPrec [Sport]

Show Sport Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

showsPrec :: Int -> Sport -> ShowS

show :: Sport -> String

showList :: [Sport] -> ShowS

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 #

isUnbounded :: Sport -> Bool Source #

isUninterpreted :: 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 #

SymVal Sport Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

literal :: Sport -> SBV Sport Source #

fromCV :: CV -> Sport Source #

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

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

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

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

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

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

mkExistVars :: MonadSymbolic m => Int -> m [SBV Sport] 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 #

SatModel Sport Source #

Make Sport a symbolic value.

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 #

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 satTrackUFs configuration to indicate that the uninterpreted function changes do not matter for generating different values. All we care is that the fishOwner changes!