Documentation.SBV.Examples.Puzzles.Fish

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?

Documentation

data Color

Colors of houses

Constructors

Red

Green

White

Yellow

Blue

Instances

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

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

Eq Color

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

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

SymVal Color

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

literal :: Color -> SBV Color

fromCV :: CV -> Color

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

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

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

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

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

sbvExists_ :: 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

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

isRational :: Color -> Bool

isFP :: Color -> Bool

isUnbounded :: Color -> Bool

isUserSort :: Color -> Bool

isChar :: Color -> Bool

isString :: Color -> Bool

isList :: Color -> Bool

isSet :: Color -> Bool

isTuple :: Color -> Bool

isMaybe :: Color -> Bool

isEither :: Color -> Bool

showType :: Color -> String

SatModel Color

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

type SColor = SBV Color

Symbolic version of the type Color.

sBlue :: SBV Color

Symbolic version of the constructor Blue.

sYellow :: SBV Color

Symbolic version of the constructor Yellow.

sWhite :: SBV Color

Symbolic version of the constructor White.

sGreen :: SBV Color

Symbolic version of the constructor Green.

sRed :: SBV Color

Symbolic version of the constructor Red.

data Nationality

Nationalities of the occupants

Constructors

Briton

Dane

Swede

Norwegian

German

Instances

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

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

Eq Nationality

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

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

SymVal Nationality

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

literal :: Nationality -> SBV Nationality

fromCV :: CV -> Nationality

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

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

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

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

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

sbvExists_ :: 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

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

isRational :: Nationality -> Bool

isFP :: Nationality -> Bool

isUnbounded :: Nationality -> Bool

isUserSort :: Nationality -> Bool

isChar :: Nationality -> Bool

isString :: Nationality -> Bool

isList :: Nationality -> Bool

isSet :: Nationality -> Bool

isTuple :: Nationality -> Bool

isMaybe :: Nationality -> Bool

isEither :: Nationality -> Bool

showType :: Nationality -> String

SatModel Nationality

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

type SNationality = SBV Nationality

Symbolic version of the type Nationality.

sGerman :: SBV Nationality

Symbolic version of the constructor German.

sNorwegian :: SBV Nationality

Symbolic version of the constructor Norwegian.

sSwede :: SBV Nationality

Symbolic version of the constructor Swede.

sDane :: SBV Nationality

Symbolic version of the constructor Dane.

sBriton :: SBV Nationality

Symbolic version of the constructor Briton.

data Beverage

Beverage choices

Constructors

Tea

Coffee

Milk

Beer

Water

Instances

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

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

Eq Beverage

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

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

SymVal Beverage

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

literal :: Beverage -> SBV Beverage

fromCV :: CV -> Beverage

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

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

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

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

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

sbvExists_ :: 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

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

isRational :: Beverage -> Bool

isFP :: Beverage -> Bool

isUnbounded :: Beverage -> Bool

isUserSort :: Beverage -> Bool

isChar :: Beverage -> Bool

isString :: Beverage -> Bool

isList :: Beverage -> Bool

isSet :: Beverage -> Bool

isTuple :: Beverage -> Bool

isMaybe :: Beverage -> Bool

isEither :: Beverage -> Bool

showType :: Beverage -> String

SatModel Beverage

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

type SBeverage = SBV Beverage

Symbolic version of the type Beverage.

sWater :: SBV Beverage

Symbolic version of the constructor Water.

sBeer :: SBV Beverage

Symbolic version of the constructor Beer.

sMilk :: SBV Beverage

Symbolic version of the constructor Milk.

sCoffee :: SBV Beverage

Symbolic version of the constructor Coffee.

sTea :: SBV Beverage

Symbolic version of the constructor Tea.

data Pet

Pets they keep

Constructors

Dog

Horse

Cat

Bird

Fish

Instances

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

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

Eq Pet

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

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

SymVal Pet

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

literal :: Pet -> SBV Pet

fromCV :: CV -> Pet

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

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

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

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

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

sbvExists_ :: 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

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

isRational :: Pet -> Bool

isFP :: Pet -> Bool

isUnbounded :: Pet -> Bool

isUserSort :: Pet -> Bool

isChar :: Pet -> Bool

isString :: Pet -> Bool

isList :: Pet -> Bool

isSet :: Pet -> Bool

isTuple :: Pet -> Bool

isMaybe :: Pet -> Bool

isEither :: Pet -> Bool

showType :: Pet -> String

SatModel Pet

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

type SPet = SBV Pet

Symbolic version of the type Pet.

sFish :: SBV Pet

Symbolic version of the constructor Fish.

sBird :: SBV Pet

Symbolic version of the constructor Bird.

sCat :: SBV Pet

Symbolic version of the constructor Cat.

sHorse :: SBV Pet

Symbolic version of the constructor Horse.

sDog :: SBV Pet

Symbolic version of the constructor Dog.

data Sport

Sports they engage in

Constructors

Football

Baseball

Volleyball

Hockey

Tennis

Instances

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

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

Eq Sport

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

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

SymVal Sport

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

literal :: Sport -> SBV Sport

fromCV :: CV -> Sport

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

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

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

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

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

sbvExists_ :: 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

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

isRational :: Sport -> Bool

isFP :: Sport -> Bool

isUnbounded :: Sport -> Bool

isUserSort :: Sport -> Bool

isChar :: Sport -> Bool

isString :: Sport -> Bool

isList :: Sport -> Bool

isSet :: Sport -> Bool

isTuple :: Sport -> Bool

isMaybe :: Sport -> Bool

isEither :: Sport -> Bool

showType :: Sport -> String

SatModel Sport

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

type SSport = SBV Sport

Symbolic version of the type Sport.

sTennis :: SBV Sport

Symbolic version of the constructor Tennis.

sHockey :: SBV Sport

Symbolic version of the constructor Hockey.

sVolleyball :: SBV Sport

Symbolic version of the constructor Volleyball.

sBaseball :: SBV Sport

Symbolic version of the constructor Baseball.

sFootball :: SBV Sport

Symbolic version of the constructor Football.

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! 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!