Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.Puzzles.Fish

Description

Solves the following logic puzzle:

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
data Nationality
- = Briton
- | Dane
- | Swede
- | Norwegian
- | German
data Beverage
- = Tea
- | Coffee
- | Milk
- | Beer
- | Water
data Pet
- = Dog
- | Horse
- | Cat
- | Bird
- | Fish
data Sport
- = Football
- | Baseball
- | Volleyball
- | Hockey
- | Tennis
fishOwner :: IO ()

Documentation

data Color #

Colors of houses

Constructors

Red
Green
White
Yellow
Blue

Instances

Eq Color #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods (==) :: Color -> Color -> Bool # (/=) :: Color -> Color -> Bool #
Data Color #
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 :: (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 #
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 #
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 #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods showsPrec :: Int -> Color -> ShowS # show :: Color -> String # showList :: [Color] -> ShowS #
HasKind Color #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods kindOf :: Color -> Kind # hasSign :: Color -> Bool # intSizeOf :: Color -> Int # isBoolean :: Color -> Bool # isBounded :: Color -> Bool # isReal :: Color -> Bool # isFloat :: Color -> Bool # isDouble :: Color -> Bool # isInteger :: Color -> Bool # isUninterpreted :: Color -> Bool # isChar :: Color -> Bool # isString :: Color -> Bool # isList :: Color -> Bool # showType :: Color -> String #
SymWord Color #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods forall :: String -> Symbolic (SBV Color) # forall_ :: Symbolic (SBV Color) # mkForallVars :: Int -> Symbolic [SBV Color] # exists :: String -> Symbolic (SBV Color) # exists_ :: Symbolic (SBV Color) # mkExistVars :: Int -> Symbolic [SBV Color] # free :: String -> Symbolic (SBV Color) # free_ :: Symbolic (SBV Color) # mkFreeVars :: Int -> Symbolic [SBV Color] # symbolic :: String -> Symbolic (SBV Color) # symbolics :: [String] -> Symbolic [SBV Color] # literal :: Color -> SBV Color # unliteral :: SBV Color -> Maybe Color # fromCW :: CW -> Color # isConcrete :: SBV Color -> Bool # isSymbolic :: SBV Color -> Bool # isConcretely :: SBV Color -> (Color -> Bool) -> Bool # mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Color) #
SatModel Color #	Make `Color` a symbolic value.
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods parseCWs :: [CW] -> Maybe (Color, [CW]) # cvtModel :: (Color -> Maybe b) -> Maybe (Color, [CW]) -> Maybe (b, [CW]) #
SMTValue Color #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods sexprToVal :: SExpr -> Maybe Color #

data Nationality #

Nationalities of the occupants

Constructors

Briton
Dane
Swede
Norwegian
German

Instances

Eq Nationality #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods (==) :: Nationality -> Nationality -> Bool # (/=) :: Nationality -> Nationality -> Bool #
Data Nationality #
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 :: (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 #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods compare :: Nationality -> Nationality -> Ordering # (<) :: Nationality -> Nationality -> Bool # (<=) :: Nationality -> Nationality -> Bool # (>) :: Nationality -> Nationality -> Bool # (>=) :: Nationality -> Nationality -> Bool # max :: Nationality -> Nationality -> Nationality # min :: Nationality -> Nationality -> Nationality #
Read Nationality #
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 #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods showsPrec :: Int -> Nationality -> ShowS # show :: Nationality -> String # showList :: [Nationality] -> ShowS #
HasKind Nationality #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods kindOf :: Nationality -> Kind # hasSign :: Nationality -> Bool # intSizeOf :: Nationality -> Int # isBoolean :: Nationality -> Bool # isBounded :: Nationality -> Bool # isReal :: Nationality -> Bool # isFloat :: Nationality -> Bool # isDouble :: Nationality -> Bool # isInteger :: Nationality -> Bool # isUninterpreted :: Nationality -> Bool # isChar :: Nationality -> Bool # isString :: Nationality -> Bool # isList :: Nationality -> Bool # showType :: Nationality -> String #
SymWord Nationality #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods forall :: String -> Symbolic (SBV Nationality) # forall_ :: Symbolic (SBV Nationality) # mkForallVars :: Int -> Symbolic [SBV Nationality] # exists :: String -> Symbolic (SBV Nationality) # exists_ :: Symbolic (SBV Nationality) # mkExistVars :: Int -> Symbolic [SBV Nationality] # free :: String -> Symbolic (SBV Nationality) # free_ :: Symbolic (SBV Nationality) # mkFreeVars :: Int -> Symbolic [SBV Nationality] # symbolic :: String -> Symbolic (SBV Nationality) # symbolics :: [String] -> Symbolic [SBV Nationality] # literal :: Nationality -> SBV Nationality # unliteral :: SBV Nationality -> Maybe Nationality # fromCW :: CW -> Nationality # isConcrete :: SBV Nationality -> Bool # isSymbolic :: SBV Nationality -> Bool # isConcretely :: SBV Nationality -> (Nationality -> Bool) -> Bool # mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Nationality) #
SatModel Nationality #	Make `Nationality` a symbolic value.
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods parseCWs :: [CW] -> Maybe (Nationality, [CW]) # cvtModel :: (Nationality -> Maybe b) -> Maybe (Nationality, [CW]) -> Maybe (b, [CW]) #
SMTValue Nationality #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods sexprToVal :: SExpr -> Maybe Nationality #

data Beverage #

Beverage choices

Constructors

Tea
Coffee
Milk
Beer
Water

Instances

Eq Beverage #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods (==) :: Beverage -> Beverage -> Bool # (/=) :: Beverage -> Beverage -> Bool #
Data Beverage #
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 :: (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 #
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 #
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 #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods showsPrec :: Int -> Beverage -> ShowS # show :: Beverage -> String # showList :: [Beverage] -> ShowS #
HasKind Beverage #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods kindOf :: Beverage -> Kind # hasSign :: Beverage -> Bool # intSizeOf :: Beverage -> Int # isBoolean :: Beverage -> Bool # isBounded :: Beverage -> Bool # isReal :: Beverage -> Bool # isFloat :: Beverage -> Bool # isDouble :: Beverage -> Bool # isInteger :: Beverage -> Bool # isUninterpreted :: Beverage -> Bool # isChar :: Beverage -> Bool # isString :: Beverage -> Bool # isList :: Beverage -> Bool # showType :: Beverage -> String #
SymWord Beverage #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods forall :: String -> Symbolic (SBV Beverage) # forall_ :: Symbolic (SBV Beverage) # mkForallVars :: Int -> Symbolic [SBV Beverage] # exists :: String -> Symbolic (SBV Beverage) # exists_ :: Symbolic (SBV Beverage) # mkExistVars :: Int -> Symbolic [SBV Beverage] # free :: String -> Symbolic (SBV Beverage) # free_ :: Symbolic (SBV Beverage) # mkFreeVars :: Int -> Symbolic [SBV Beverage] # symbolic :: String -> Symbolic (SBV Beverage) # symbolics :: [String] -> Symbolic [SBV Beverage] # literal :: Beverage -> SBV Beverage # unliteral :: SBV Beverage -> Maybe Beverage # fromCW :: CW -> Beverage # isConcrete :: SBV Beverage -> Bool # isSymbolic :: SBV Beverage -> Bool # isConcretely :: SBV Beverage -> (Beverage -> Bool) -> Bool # mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Beverage) #
SatModel Beverage #	Make `Beverage` a symbolic value.
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods parseCWs :: [CW] -> Maybe (Beverage, [CW]) # cvtModel :: (Beverage -> Maybe b) -> Maybe (Beverage, [CW]) -> Maybe (b, [CW]) #
SMTValue Beverage #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods sexprToVal :: SExpr -> Maybe Beverage #

data Pet #

Pets they keep

Constructors

Dog
Horse
Cat
Bird
Fish

Instances

Eq Pet #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods (==) :: Pet -> Pet -> Bool # (/=) :: Pet -> Pet -> Bool #
Data Pet #
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 :: (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 #
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 #
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 #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods showsPrec :: Int -> Pet -> ShowS # show :: Pet -> String # showList :: [Pet] -> ShowS #
HasKind Pet #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods kindOf :: Pet -> Kind # hasSign :: Pet -> Bool # intSizeOf :: Pet -> Int # isBoolean :: Pet -> Bool # isBounded :: Pet -> Bool # isReal :: Pet -> Bool # isFloat :: Pet -> Bool # isDouble :: Pet -> Bool # isInteger :: Pet -> Bool # isUninterpreted :: Pet -> Bool # isChar :: Pet -> Bool # isString :: Pet -> Bool # isList :: Pet -> Bool # showType :: Pet -> String #
SymWord Pet #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods forall :: String -> Symbolic (SBV Pet) # forall_ :: Symbolic (SBV Pet) # mkForallVars :: Int -> Symbolic [SBV Pet] # exists :: String -> Symbolic (SBV Pet) # exists_ :: Symbolic (SBV Pet) # mkExistVars :: Int -> Symbolic [SBV Pet] # free :: String -> Symbolic (SBV Pet) # free_ :: Symbolic (SBV Pet) # mkFreeVars :: Int -> Symbolic [SBV Pet] # symbolic :: String -> Symbolic (SBV Pet) # symbolics :: [String] -> Symbolic [SBV Pet] # literal :: Pet -> SBV Pet # unliteral :: SBV Pet -> Maybe Pet # fromCW :: CW -> Pet # isConcrete :: SBV Pet -> Bool # isSymbolic :: SBV Pet -> Bool # isConcretely :: SBV Pet -> (Pet -> Bool) -> Bool # mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Pet) #
SatModel Pet #	Make `Pet` a symbolic value.
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods parseCWs :: [CW] -> Maybe (Pet, [CW]) # cvtModel :: (Pet -> Maybe b) -> Maybe (Pet, [CW]) -> Maybe (b, [CW]) #
SMTValue Pet #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods sexprToVal :: SExpr -> Maybe Pet #

data Sport #

Sports they engage in

Constructors

Football
Baseball
Volleyball
Hockey
Tennis

Instances

Eq Sport #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods (==) :: Sport -> Sport -> Bool # (/=) :: Sport -> Sport -> Bool #
Data Sport #
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 :: (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 #
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 #
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 #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods showsPrec :: Int -> Sport -> ShowS # show :: Sport -> String # showList :: [Sport] -> ShowS #
HasKind Sport #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods kindOf :: Sport -> Kind # hasSign :: Sport -> Bool # intSizeOf :: Sport -> Int # isBoolean :: Sport -> Bool # isBounded :: Sport -> Bool # isReal :: Sport -> Bool # isFloat :: Sport -> Bool # isDouble :: Sport -> Bool # isInteger :: Sport -> Bool # isUninterpreted :: Sport -> Bool # isChar :: Sport -> Bool # isString :: Sport -> Bool # isList :: Sport -> Bool # showType :: Sport -> String #
SymWord Sport #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods forall :: String -> Symbolic (SBV Sport) # forall_ :: Symbolic (SBV Sport) # mkForallVars :: Int -> Symbolic [SBV Sport] # exists :: String -> Symbolic (SBV Sport) # exists_ :: Symbolic (SBV Sport) # mkExistVars :: Int -> Symbolic [SBV Sport] # free :: String -> Symbolic (SBV Sport) # free_ :: Symbolic (SBV Sport) # mkFreeVars :: Int -> Symbolic [SBV Sport] # symbolic :: String -> Symbolic (SBV Sport) # symbolics :: [String] -> Symbolic [SBV Sport] # literal :: Sport -> SBV Sport # unliteral :: SBV Sport -> Maybe Sport # fromCW :: CW -> Sport # isConcrete :: SBV Sport -> Bool # isSymbolic :: SBV Sport -> Bool # isConcretely :: SBV Sport -> (Sport -> Bool) -> Bool # mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Sport) #
SatModel Sport #	Make `Sport` a symbolic value.
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods parseCWs :: [CW] -> Maybe (Sport, [CW]) # cvtModel :: (Sport -> Maybe b) -> Maybe (Sport, [CW]) -> Maybe (b, [CW]) #
SMTValue Sport #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods sexprToVal :: SExpr -> Maybe Sport #

fishOwner :: IO () #

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!