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

data Color
- = Red
- | Green
- | White
- | Yellow
- | Blue
type SColor = SBV Color
sBlue :: SBV Color
sYellow :: SBV Color
sWhite :: SBV Color
sGreen :: SBV Color
sRed :: SBV Color
data Nationality
- = Briton
- | Dane
- | Swede
- | Norwegian
- | German
type SNationality = SBV Nationality
sGerman :: SBV Nationality
sNorwegian :: SBV Nationality
sSwede :: SBV Nationality
sDane :: SBV Nationality
sBriton :: SBV Nationality
data Beverage
- = Tea
- | Coffee
- | Milk
- | Beer
- | Water
type SBeverage = SBV Beverage
sWater :: SBV Beverage
sBeer :: SBV Beverage
sMilk :: SBV Beverage
sCoffee :: SBV Beverage
sTea :: SBV Beverage
data Pet
- = Dog
- | Horse
- | Cat
- | Bird
- | Fish
type SPet = SBV Pet
sFish :: SBV Pet
sBird :: SBV Pet
sCat :: SBV Pet
sHorse :: SBV Pet
sDog :: SBV Pet
data Sport
- = Football
- | Baseball
- | Volleyball
- | Hockey
- | Tennis
type SSport = SBV Sport
sTennis :: SBV Sport
sHockey :: SBV Sport
sVolleyball :: SBV Sport
sBaseball :: SBV Sport
sFootball :: SBV Sport
fishOwner :: IO ()

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 # isFP :: Color -> Bool Source # isUnbounded :: Color -> Bool Source # isUserSort :: 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 => VarContext -> 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 #
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 #

type SColor = SBV Color Source #

Make Color a symbolic value.

sBlue :: SBV Color Source #

sYellow :: SBV Color Source #

sWhite :: SBV Color Source #

sGreen :: SBV Color Source #

sRed :: SBV Color 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 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 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 Methods kindOf :: Nationality -> Kind Source # hasSign :: Nationality -> Bool Source # intSizeOf :: Nationality -> Int Source # isBoolean :: Nationality -> Bool Source # isBounded :: Nationality -> Bool Source # isReal :: Nationality -> Bool Source # isFloat :: Nationality -> Bool Source # isDouble :: Nationality -> Bool Source # isFP :: Nationality -> Bool Source # isUnbounded :: Nationality -> Bool Source # isUserSort :: Nationality -> Bool Source # isChar :: Nationality -> Bool Source # isString :: Nationality -> Bool Source # isList :: Nationality -> Bool Source # isSet :: Nationality -> Bool Source # isTuple :: Nationality -> Bool Source # isMaybe :: Nationality -> Bool Source # isEither :: Nationality -> Bool Source # showType :: Nationality -> String Source #
SymVal Nationality Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Nationality) Source # literal :: Nationality -> SBV Nationality Source # fromCV :: CV -> Nationality Source # isConcretely :: SBV Nationality -> (Nationality -> Bool) -> Bool Source # forall :: MonadSymbolic m => String -> m (SBV Nationality) Source # forall_ :: MonadSymbolic m => m (SBV Nationality) Source # mkForallVars :: MonadSymbolic m => Int -> m [SBV Nationality] Source # exists :: MonadSymbolic m => String -> m (SBV Nationality) Source # exists_ :: MonadSymbolic m => m (SBV Nationality) Source # mkExistVars :: MonadSymbolic m => Int -> m [SBV Nationality] Source # free :: MonadSymbolic m => String -> m (SBV Nationality) Source # free_ :: MonadSymbolic m => m (SBV Nationality) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV Nationality] Source # symbolic :: MonadSymbolic m => String -> m (SBV Nationality) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV Nationality] Source # unliteral :: SBV Nationality -> Maybe Nationality Source # isConcrete :: SBV Nationality -> Bool Source # isSymbolic :: SBV Nationality -> Bool Source #
SatModel Nationality Source #
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 #

type SNationality = SBV Nationality Source #

Make Nationality a symbolic value.

sGerman :: SBV Nationality Source #

sNorwegian :: SBV Nationality Source #

sSwede :: SBV Nationality Source #

sDane :: SBV Nationality Source #

sBriton :: SBV Nationality 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 Methods kindOf :: Beverage -> Kind Source # hasSign :: Beverage -> Bool Source # intSizeOf :: Beverage -> Int Source # isBoolean :: Beverage -> Bool Source # isBounded :: Beverage -> Bool Source # isReal :: Beverage -> Bool Source # isFloat :: Beverage -> Bool Source # isDouble :: Beverage -> Bool Source # isFP :: Beverage -> Bool Source # isUnbounded :: Beverage -> Bool Source # isUserSort :: Beverage -> Bool Source # isChar :: Beverage -> Bool Source # isString :: Beverage -> Bool Source # isList :: Beverage -> Bool Source # isSet :: Beverage -> Bool Source # isTuple :: Beverage -> Bool Source # isMaybe :: Beverage -> Bool Source # isEither :: Beverage -> Bool Source # showType :: Beverage -> String Source #
SymVal Beverage Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Beverage) Source # literal :: Beverage -> SBV Beverage Source # fromCV :: CV -> Beverage Source # isConcretely :: SBV Beverage -> (Beverage -> Bool) -> Bool Source # forall :: MonadSymbolic m => String -> m (SBV Beverage) Source # forall_ :: MonadSymbolic m => m (SBV Beverage) Source # mkForallVars :: MonadSymbolic m => Int -> m [SBV Beverage] Source # exists :: MonadSymbolic m => String -> m (SBV Beverage) Source # exists_ :: MonadSymbolic m => m (SBV Beverage) Source # mkExistVars :: MonadSymbolic m => Int -> m [SBV Beverage] Source # free :: MonadSymbolic m => String -> m (SBV Beverage) Source # free_ :: MonadSymbolic m => m (SBV Beverage) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV Beverage] Source # symbolic :: MonadSymbolic m => String -> m (SBV Beverage) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV Beverage] Source # unliteral :: SBV Beverage -> Maybe Beverage Source # isConcrete :: SBV Beverage -> Bool Source # isSymbolic :: SBV Beverage -> Bool Source #
SatModel Beverage Source #
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 #

type SBeverage = SBV Beverage Source #

Make Beverage a symbolic value.

sWater :: SBV Beverage Source #

sBeer :: SBV Beverage Source #

sMilk :: SBV Beverage Source #

sCoffee :: SBV Beverage Source #

sTea :: SBV Beverage 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 # isFP :: Pet -> Bool Source # isUnbounded :: Pet -> Bool Source # isUserSort :: 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 => VarContext -> 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 #
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 #

type SPet = SBV Pet Source #

Make Pet a symbolic value.

sFish :: SBV Pet Source #

sBird :: SBV Pet Source #

sCat :: SBV Pet Source #

sHorse :: SBV Pet Source #

sDog :: SBV Pet Source #

data Sport Source #

Sports they engage in

Constructors

Football
Baseball
Volleyball
Hockey
Tennis

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 # isFP :: Sport -> Bool Source # isUnbounded :: Sport -> Bool Source # isUserSort :: 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 => VarContext -> 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 #
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 #

type SSport = SBV Sport Source #

Make Sport a symbolic value.

sTennis :: SBV Sport Source #

sHockey :: SBV Sport Source #

sVolleyball :: SBV Sport Source #

sBaseball :: SBV Sport Source #

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