Documentation.SBV.Examples.Puzzles.Fish

Author : Levent Erkok License : BSD3 Maintainer: [e-mail] Stability : experimental

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?

Documentation

data Color

Colors of houses

Constructors

Red

Green

White

Yellow

Blue

Instances

Eq Color

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

Data Color

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

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

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

readsPrec :: Int -> ReadS Color

readList :: ReadS [Color]

readPrec :: ReadPrec Color

readListPrec :: ReadPrec [Color]

Show Color

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

showsPrec :: Int -> Color -> ShowS

show :: Color -> String

showList :: [Color] -> ShowS

HasKind Color

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

isTuple :: Color -> Bool

showType :: Color -> String

SymVal Color

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

literal :: Color -> SBV Color

fromCV :: CV -> Color

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

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

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

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

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

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

mkExistVars :: MonadSymbolic m => Int -> m [SBV Color]

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

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

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

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

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

unliteral :: SBV Color -> Maybe Color

isConcrete :: SBV Color -> Bool

isSymbolic :: SBV Color -> Bool

SatModel Color

Make Color a symbolic value.

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

parseCVs :: [CV] -> Maybe (Color, [CV])

cvtModel :: (Color -> Maybe b) -> Maybe (Color, [CV]) -> Maybe (b, [CV])

SMTValue Color

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

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

Data Nationality

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

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

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

readsPrec :: Int -> ReadS Nationality

readList :: ReadS [Nationality]

readPrec :: ReadPrec Nationality

readListPrec :: ReadPrec [Nationality]

Show Nationality

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

showsPrec :: Int -> Nationality -> ShowS

show :: Nationality -> String

showList :: [Nationality] -> ShowS

HasKind Nationality

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

isTuple :: Nationality -> Bool

showType :: Nationality -> String

SymVal Nationality

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV Nationality)

literal :: Nationality -> SBV Nationality

fromCV :: CV -> Nationality

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

forall :: MonadSymbolic m => String -> m (SBV Nationality)

forall_ :: MonadSymbolic m => m (SBV Nationality)

mkForallVars :: MonadSymbolic m => Int -> m [SBV Nationality]

exists :: MonadSymbolic m => String -> m (SBV Nationality)

exists_ :: MonadSymbolic m => m (SBV Nationality)

mkExistVars :: MonadSymbolic m => Int -> m [SBV Nationality]

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

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

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

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

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

unliteral :: SBV Nationality -> Maybe Nationality

isConcrete :: SBV Nationality -> Bool

isSymbolic :: SBV Nationality -> Bool

SatModel Nationality

Make Nationality a symbolic value.

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

parseCVs :: [CV] -> Maybe (Nationality, [CV])

cvtModel :: (Nationality -> Maybe b) -> Maybe (Nationality, [CV]) -> Maybe (b, [CV])

SMTValue Nationality

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

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

Data Beverage

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

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

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

readsPrec :: Int -> ReadS Beverage

readList :: ReadS [Beverage]

readPrec :: ReadPrec Beverage

readListPrec :: ReadPrec [Beverage]

Show Beverage

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

showsPrec :: Int -> Beverage -> ShowS

show :: Beverage -> String

showList :: [Beverage] -> ShowS

HasKind Beverage

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

isTuple :: Beverage -> Bool

showType :: Beverage -> String

SymVal Beverage

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV Beverage)

literal :: Beverage -> SBV Beverage

fromCV :: CV -> Beverage

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

forall :: MonadSymbolic m => String -> m (SBV Beverage)

forall_ :: MonadSymbolic m => m (SBV Beverage)

mkForallVars :: MonadSymbolic m => Int -> m [SBV Beverage]

exists :: MonadSymbolic m => String -> m (SBV Beverage)

exists_ :: MonadSymbolic m => m (SBV Beverage)

mkExistVars :: MonadSymbolic m => Int -> m [SBV Beverage]

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

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

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

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

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

unliteral :: SBV Beverage -> Maybe Beverage

isConcrete :: SBV Beverage -> Bool

isSymbolic :: SBV Beverage -> Bool

SatModel Beverage

Make Beverage a symbolic value.

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

parseCVs :: [CV] -> Maybe (Beverage, [CV])

cvtModel :: (Beverage -> Maybe b) -> Maybe (Beverage, [CV]) -> Maybe (b, [CV])

SMTValue Beverage

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

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

Data Pet

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

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

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

readsPrec :: Int -> ReadS Pet

readList :: ReadS [Pet]

readPrec :: ReadPrec Pet

readListPrec :: ReadPrec [Pet]

Show Pet

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

showsPrec :: Int -> Pet -> ShowS

show :: Pet -> String

showList :: [Pet] -> ShowS

HasKind Pet

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

isTuple :: Pet -> Bool

showType :: Pet -> String

SymVal Pet

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

literal :: Pet -> SBV Pet

fromCV :: CV -> Pet

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

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

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

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

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

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

mkExistVars :: MonadSymbolic m => Int -> m [SBV Pet]

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

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

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

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

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

unliteral :: SBV Pet -> Maybe Pet

isConcrete :: SBV Pet -> Bool

isSymbolic :: SBV Pet -> Bool

SatModel Pet

Make Pet a symbolic value.

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

parseCVs :: [CV] -> Maybe (Pet, [CV])

cvtModel :: (Pet -> Maybe b) -> Maybe (Pet, [CV]) -> Maybe (b, [CV])

SMTValue Pet

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

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

Data Sport

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

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

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

readsPrec :: Int -> ReadS Sport

readList :: ReadS [Sport]

readPrec :: ReadPrec Sport

readListPrec :: ReadPrec [Sport]

Show Sport

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

showsPrec :: Int -> Sport -> ShowS

show :: Sport -> String

showList :: [Sport] -> ShowS

HasKind Sport

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

isTuple :: Sport -> Bool

showType :: Sport -> String

SymVal Sport

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

literal :: Sport -> SBV Sport

fromCV :: CV -> Sport

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

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

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

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

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

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

mkExistVars :: MonadSymbolic m => Int -> m [SBV Sport]

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

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

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

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

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

unliteral :: SBV Sport -> Maybe Sport

isConcrete :: SBV Sport -> Bool

isSymbolic :: SBV Sport -> Bool

SatModel Sport

Make Sport a symbolic value.

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

parseCVs :: [CV] -> Maybe (Sport, [CV])

cvtModel :: (Sport -> Maybe b) -> Maybe (Sport, [CV]) -> Maybe (b, [CV])

SMTValue Sport

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!