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

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

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

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

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

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

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

Make Color a symbolic value.

sBlue :: SBV Color

sYellow :: SBV Color

sWhite :: SBV Color

sGreen :: SBV Color

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

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

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

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

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

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

Make Nationality a symbolic value.

sGerman :: SBV Nationality

sNorwegian :: SBV Nationality

sSwede :: SBV Nationality

sDane :: SBV Nationality

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

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

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

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

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

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

Make Beverage a symbolic value.

sWater :: SBV Beverage

sBeer :: SBV Beverage

sMilk :: SBV Beverage

sCoffee :: SBV Beverage

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

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

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

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

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

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

Make Pet a symbolic value.

sFish :: SBV Pet

sBird :: SBV Pet

sCat :: SBV Pet

sHorse :: SBV Pet

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

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

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

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

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

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

Make Sport a symbolic value.

sTennis :: SBV Sport

sHockey :: SBV Sport

sVolleyball :: SBV Sport

sBaseball :: SBV Sport

sFootball :: SBV 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! 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!