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
cv2Color :: String -> [CV] -> Color
_undefiner_Color :: a
type SColor = SBV Color
sRed :: SBV Color
sGreen :: SBV Color
sWhite :: SBV Color
sYellow :: SBV Color
sBlue :: SBV Color
isRed :: SBV Color -> SBool
isGreen :: SBV Color -> SBool
isWhite :: SBV Color -> SBool
isYellow :: SBV Color -> SBool
isBlue :: SBV Color -> SBool
sCaseColor :: Mergeable result => SBV Color -> result -> result -> result -> result -> result -> result
data Nationality
- = Briton
- | Dane
- | Swede
- | Norwegian
- | German
cv2Nationality :: String -> [CV] -> Nationality
_undefiner_Nationality :: a
type SNationality = SBV Nationality
sBriton :: SBV Nationality
sDane :: SBV Nationality
sSwede :: SBV Nationality
sNorwegian :: SBV Nationality
sGerman :: SBV Nationality
isBriton :: SBV Nationality -> SBool
isDane :: SBV Nationality -> SBool
isSwede :: SBV Nationality -> SBool
isNorwegian :: SBV Nationality -> SBool
isGerman :: SBV Nationality -> SBool
sCaseNationality :: Mergeable result => SBV Nationality -> result -> result -> result -> result -> result -> result
data Beverage
- = Tea
- | Coffee
- | Milk
- | Beer
- | Water
cv2Beverage :: String -> [CV] -> Beverage
_undefiner_Beverage :: a
type SBeverage = SBV Beverage
sTea :: SBV Beverage
sCoffee :: SBV Beverage
sMilk :: SBV Beverage
sBeer :: SBV Beverage
sWater :: SBV Beverage
isTea :: SBV Beverage -> SBool
isCoffee :: SBV Beverage -> SBool
isMilk :: SBV Beverage -> SBool
isBeer :: SBV Beverage -> SBool
isWater :: SBV Beverage -> SBool
sCaseBeverage :: Mergeable result => SBV Beverage -> result -> result -> result -> result -> result -> result
data Pet
- = Dog
- | Horse
- | Cat
- | Bird
- | Fish
cv2Pet :: String -> [CV] -> Pet
_undefiner_Pet :: a
type SPet = SBV Pet
sDog :: SBV Pet
sHorse :: SBV Pet
sCat :: SBV Pet
sBird :: SBV Pet
sFish :: SBV Pet
isDog :: SBV Pet -> SBool
isHorse :: SBV Pet -> SBool
isCat :: SBV Pet -> SBool
isBird :: SBV Pet -> SBool
isFish :: SBV Pet -> SBool
sCasePet :: Mergeable result => SBV Pet -> result -> result -> result -> result -> result -> result
data Sport
- = Football
- | Baseball
- | Volleyball
- | Hockey
- | Tennis
cv2Sport :: String -> [CV] -> Sport
_undefiner_Sport :: a
type SSport = SBV Sport
sFootball :: SBV Sport
sBaseball :: SBV Sport
sVolleyball :: SBV Sport
sHockey :: SBV Sport
sTennis :: SBV Sport
isFootball :: SBV Sport -> SBool
isBaseball :: SBV Sport -> SBool
isVolleyball :: SBV Sport -> SBool
isHockey :: SBV Sport -> SBool
isTennis :: SBV Sport -> SBool
sCaseSport :: Mergeable result => SBV Sport -> result -> result -> result -> result -> result -> result
fishOwner :: IO ()

Documentation

data Color Source #

Colors of houses

Constructors

Red
Green
White
Yellow
Blue

Instances

Instances details

Arbitrary Color Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods arbitrary :: Gen Color # shrink :: Color -> [Color] #
SymVal Color Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Color) Source # mkSymValInit :: State -> SBV Color -> IO () Source # literal :: Color -> SBV Color Source # fromCV :: CV -> Color Source # isConcretely :: SBV Color -> (Color -> Bool) -> Bool Source # minMaxBound :: Maybe (Color, 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 # unlitCV :: SBV Color -> Maybe (Kind, CVal) Source # isConcrete :: SBV Color -> Bool Source # isSymbolic :: SBV Color -> Bool Source #
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 # isRational :: Color -> Bool Source # isFP :: Color -> Bool Source # isUnbounded :: Color -> Bool Source # isADT :: Color -> Bool Source # isChar :: Color -> Bool Source # isString :: Color -> Bool Source # isList :: Color -> Bool Source # isSet :: Color -> Bool Source # isTuple :: Color -> Bool Source # isArray :: Color -> Bool Source # isRoundingMode :: Color -> Bool Source # isUninterpreted :: Color -> Bool Source # showType :: Color -> String Source #
EnumSymbolic Color Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods succ :: SBV Color -> SBV Color Source # pred :: SBV Color -> SBV Color Source # toEnum :: SInteger -> SBV Color Source # fromEnum :: SBV Color -> SInteger Source # enumFrom :: SBV Color -> SList Color Source # enumFromThen :: SBV Color -> SBV Color -> SList Color Source # enumFromTo :: SBV Color -> SBV Color -> SList Color Source # enumFromThenTo :: SBV Color -> SBV Color -> SBV Color -> SList Color 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 #
OrdSymbolic (SBV Color) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods (.<) :: SBV Color -> SBV Color -> SBool Source # (.<=) :: SBV Color -> SBV Color -> SBool Source # (.>) :: SBV Color -> SBV Color -> SBool Source # (.>=) :: SBV Color -> SBV Color -> SBool Source # smin :: SBV Color -> SBV Color -> SBV Color Source # smax :: SBV Color -> SBV Color -> SBV Color Source # inRange :: SBV Color -> (SBV Color, SBV Color) -> SBool Source #
HasInductionSchema (Forall ta Color -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Color -> SBool) -> ProofObj Source #
SymVal extraT => HasInductionSchema (Forall ta Color -> Forall extraS extraT -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Color -> Forall extraS extraT -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta Color -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Color -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta Color -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Color -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta Color -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Color -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta Color -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Color -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

cv2Color :: String -> [CV] -> Color Source #

Conversion from SMT values to Color values.

_undefiner_Color :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type SColor = SBV Color Source #

Symbolic version of the type Color.

sRed :: SBV Color Source #

Symbolic version of the constructor Red.

sGreen :: SBV Color Source #

Symbolic version of the constructor Green.

sWhite :: SBV Color Source #

Symbolic version of the constructor White.

sYellow :: SBV Color Source #

Symbolic version of the constructor Yellow.

sBlue :: SBV Color Source #

Symbolic version of the constructor Blue.

isRed :: SBV Color -> SBool Source #

Field recognizer predicate.

isGreen :: SBV Color -> SBool Source #

Field recognizer predicate.

isWhite :: SBV Color -> SBool Source #

Field recognizer predicate.

isYellow :: SBV Color -> SBool Source #

Field recognizer predicate.

isBlue :: SBV Color -> SBool Source #

Field recognizer predicate.

sCaseColor :: Mergeable result => SBV Color -> result -> result -> result -> result -> result -> result Source #

Case analyzer for the type Color.

data Nationality Source #

Nationalities of the occupants

Constructors

Briton
Dane
Swede
Norwegian
German

Instances

Instances details

Arbitrary Nationality Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods arbitrary :: Gen Nationality # shrink :: Nationality -> [Nationality] #
Show Nationality Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods showsPrec :: Int -> Nationality -> ShowS # show :: Nationality -> String # showList :: [Nationality] -> ShowS #
SymVal Nationality Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Nationality) Source # mkSymValInit :: State -> SBV Nationality -> IO () Source # literal :: Nationality -> SBV Nationality Source # fromCV :: CV -> Nationality Source # isConcretely :: SBV Nationality -> (Nationality -> Bool) -> Bool Source # minMaxBound :: Maybe (Nationality, 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 # unlitCV :: SBV Nationality -> Maybe (Kind, CVal) Source # isConcrete :: SBV Nationality -> Bool Source # isSymbolic :: SBV Nationality -> Bool Source #
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 # isRational :: Nationality -> Bool Source # isFP :: Nationality -> Bool Source # isUnbounded :: Nationality -> Bool Source # isADT :: Nationality -> Bool Source # isChar :: Nationality -> Bool Source # isString :: Nationality -> Bool Source # isList :: Nationality -> Bool Source # isSet :: Nationality -> Bool Source # isTuple :: Nationality -> Bool Source # isArray :: Nationality -> Bool Source # isRoundingMode :: Nationality -> Bool Source # isUninterpreted :: Nationality -> Bool Source # showType :: Nationality -> String Source #
EnumSymbolic Nationality Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods succ :: SBV Nationality -> SBV Nationality Source # pred :: SBV Nationality -> SBV Nationality Source # toEnum :: SInteger -> SBV Nationality Source # fromEnum :: SBV Nationality -> SInteger Source # enumFrom :: SBV Nationality -> SList Nationality Source # enumFromThen :: SBV Nationality -> SBV Nationality -> SList Nationality Source # enumFromTo :: SBV Nationality -> SBV Nationality -> SList Nationality Source # enumFromThenTo :: SBV Nationality -> SBV Nationality -> SBV Nationality -> SList Nationality 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 #
OrdSymbolic (SBV Nationality) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods (.<) :: SBV Nationality -> SBV Nationality -> SBool Source # (.<=) :: SBV Nationality -> SBV Nationality -> SBool Source # (.>) :: SBV Nationality -> SBV Nationality -> SBool Source # (.>=) :: SBV Nationality -> SBV Nationality -> SBool Source # smin :: SBV Nationality -> SBV Nationality -> SBV Nationality Source # smax :: SBV Nationality -> SBV Nationality -> SBV Nationality Source # inRange :: SBV Nationality -> (SBV Nationality, SBV Nationality) -> SBool Source #
HasInductionSchema (Forall ta Nationality -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Nationality -> SBool) -> ProofObj Source #
SymVal extraT => HasInductionSchema (Forall ta Nationality -> Forall extraS extraT -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Nationality -> Forall extraS extraT -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta Nationality -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Nationality -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta Nationality -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Nationality -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta Nationality -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Nationality -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta Nationality -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Nationality -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

cv2Nationality :: String -> [CV] -> Nationality Source #

Conversion from SMT values to Nationality values.

_undefiner_Nationality :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type SNationality = SBV Nationality Source #

Symbolic version of the type Nationality.

sBriton :: SBV Nationality Source #

Symbolic version of the constructor Briton.

sDane :: SBV Nationality Source #

Symbolic version of the constructor Dane.

sSwede :: SBV Nationality Source #

Symbolic version of the constructor Swede.

sNorwegian :: SBV Nationality Source #

Symbolic version of the constructor Norwegian.

sGerman :: SBV Nationality Source #

Symbolic version of the constructor German.

isBriton :: SBV Nationality -> SBool Source #

Field recognizer predicate.

isDane :: SBV Nationality -> SBool Source #

Field recognizer predicate.

isSwede :: SBV Nationality -> SBool Source #

Field recognizer predicate.

isNorwegian :: SBV Nationality -> SBool Source #

Field recognizer predicate.

isGerman :: SBV Nationality -> SBool Source #

Field recognizer predicate.

sCaseNationality :: Mergeable result => SBV Nationality -> result -> result -> result -> result -> result -> result Source #

Case analyzer for the type Nationality.

data Beverage Source #

Beverage choices

Constructors

Tea
Coffee
Milk
Beer
Water

Instances

Instances details

Arbitrary Beverage Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods arbitrary :: Gen Beverage # shrink :: Beverage -> [Beverage] #
SymVal Beverage Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Beverage) Source # mkSymValInit :: State -> SBV Beverage -> IO () Source # literal :: Beverage -> SBV Beverage Source # fromCV :: CV -> Beverage Source # isConcretely :: SBV Beverage -> (Beverage -> Bool) -> Bool Source # minMaxBound :: Maybe (Beverage, 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 # unlitCV :: SBV Beverage -> Maybe (Kind, CVal) Source # isConcrete :: SBV Beverage -> Bool Source # isSymbolic :: SBV Beverage -> Bool Source #
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 # isRational :: Beverage -> Bool Source # isFP :: Beverage -> Bool Source # isUnbounded :: Beverage -> Bool Source # isADT :: Beverage -> Bool Source # isChar :: Beverage -> Bool Source # isString :: Beverage -> Bool Source # isList :: Beverage -> Bool Source # isSet :: Beverage -> Bool Source # isTuple :: Beverage -> Bool Source # isArray :: Beverage -> Bool Source # isRoundingMode :: Beverage -> Bool Source # isUninterpreted :: Beverage -> Bool Source # showType :: Beverage -> String Source #
EnumSymbolic Beverage Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods succ :: SBV Beverage -> SBV Beverage Source # pred :: SBV Beverage -> SBV Beverage Source # toEnum :: SInteger -> SBV Beverage Source # fromEnum :: SBV Beverage -> SInteger Source # enumFrom :: SBV Beverage -> SList Beverage Source # enumFromThen :: SBV Beverage -> SBV Beverage -> SList Beverage Source # enumFromTo :: SBV Beverage -> SBV Beverage -> SList Beverage Source # enumFromThenTo :: SBV Beverage -> SBV Beverage -> SBV Beverage -> SList Beverage 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 #
OrdSymbolic (SBV Beverage) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods (.<) :: SBV Beverage -> SBV Beverage -> SBool Source # (.<=) :: SBV Beverage -> SBV Beverage -> SBool Source # (.>) :: SBV Beverage -> SBV Beverage -> SBool Source # (.>=) :: SBV Beverage -> SBV Beverage -> SBool Source # smin :: SBV Beverage -> SBV Beverage -> SBV Beverage Source # smax :: SBV Beverage -> SBV Beverage -> SBV Beverage Source # inRange :: SBV Beverage -> (SBV Beverage, SBV Beverage) -> SBool Source #
HasInductionSchema (Forall ta Beverage -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Beverage -> SBool) -> ProofObj Source #
SymVal extraT => HasInductionSchema (Forall ta Beverage -> Forall extraS extraT -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Beverage -> Forall extraS extraT -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta Beverage -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Beverage -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta Beverage -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Beverage -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta Beverage -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Beverage -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta Beverage -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Beverage -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

cv2Beverage :: String -> [CV] -> Beverage Source #

Conversion from SMT values to Beverage values.

_undefiner_Beverage :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type SBeverage = SBV Beverage Source #

Symbolic version of the type Beverage.

sTea :: SBV Beverage Source #

Symbolic version of the constructor Tea.

sCoffee :: SBV Beverage Source #

Symbolic version of the constructor Coffee.

sMilk :: SBV Beverage Source #

Symbolic version of the constructor Milk.

sBeer :: SBV Beverage Source #

Symbolic version of the constructor Beer.

sWater :: SBV Beverage Source #

Symbolic version of the constructor Water.

isTea :: SBV Beverage -> SBool Source #

Field recognizer predicate.

isCoffee :: SBV Beverage -> SBool Source #

Field recognizer predicate.

isMilk :: SBV Beverage -> SBool Source #

Field recognizer predicate.

isBeer :: SBV Beverage -> SBool Source #

Field recognizer predicate.

isWater :: SBV Beverage -> SBool Source #

Field recognizer predicate.

sCaseBeverage :: Mergeable result => SBV Beverage -> result -> result -> result -> result -> result -> result Source #

Case analyzer for the type Beverage.

data Pet Source #

Pets they keep

Constructors

Dog
Horse
Cat
Bird
Fish

Instances

Instances details

Arbitrary Pet Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods arbitrary :: Gen Pet # shrink :: Pet -> [Pet] #
SymVal Pet Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Pet) Source # mkSymValInit :: State -> SBV Pet -> IO () Source # literal :: Pet -> SBV Pet Source # fromCV :: CV -> Pet Source # isConcretely :: SBV Pet -> (Pet -> Bool) -> Bool Source # minMaxBound :: Maybe (Pet, 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 # unlitCV :: SBV Pet -> Maybe (Kind, CVal) Source # isConcrete :: SBV Pet -> Bool Source # isSymbolic :: SBV Pet -> Bool Source #
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 # isRational :: Pet -> Bool Source # isFP :: Pet -> Bool Source # isUnbounded :: Pet -> Bool Source # isADT :: Pet -> Bool Source # isChar :: Pet -> Bool Source # isString :: Pet -> Bool Source # isList :: Pet -> Bool Source # isSet :: Pet -> Bool Source # isTuple :: Pet -> Bool Source # isArray :: Pet -> Bool Source # isRoundingMode :: Pet -> Bool Source # isUninterpreted :: Pet -> Bool Source # showType :: Pet -> String Source #
EnumSymbolic Pet Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods succ :: SBV Pet -> SBV Pet Source # pred :: SBV Pet -> SBV Pet Source # toEnum :: SInteger -> SBV Pet Source # fromEnum :: SBV Pet -> SInteger Source # enumFrom :: SBV Pet -> SList Pet Source # enumFromThen :: SBV Pet -> SBV Pet -> SList Pet Source # enumFromTo :: SBV Pet -> SBV Pet -> SList Pet Source # enumFromThenTo :: SBV Pet -> SBV Pet -> SBV Pet -> SList Pet 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 #
OrdSymbolic (SBV Pet) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods (.<) :: SBV Pet -> SBV Pet -> SBool Source # (.<=) :: SBV Pet -> SBV Pet -> SBool Source # (.>) :: SBV Pet -> SBV Pet -> SBool Source # (.>=) :: SBV Pet -> SBV Pet -> SBool Source # smin :: SBV Pet -> SBV Pet -> SBV Pet Source # smax :: SBV Pet -> SBV Pet -> SBV Pet Source # inRange :: SBV Pet -> (SBV Pet, SBV Pet) -> SBool Source #
HasInductionSchema (Forall ta Pet -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Pet -> SBool) -> ProofObj Source #
SymVal extraT => HasInductionSchema (Forall ta Pet -> Forall extraS extraT -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Pet -> Forall extraS extraT -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta Pet -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Pet -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta Pet -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Pet -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta Pet -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Pet -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta Pet -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Pet -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

cv2Pet :: String -> [CV] -> Pet Source #

Conversion from SMT values to Pet values.

_undefiner_Pet :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type SPet = SBV Pet Source #

Symbolic version of the type Pet.

sDog :: SBV Pet Source #

Symbolic version of the constructor Dog.

sHorse :: SBV Pet Source #

Symbolic version of the constructor Horse.

sCat :: SBV Pet Source #

Symbolic version of the constructor Cat.

sBird :: SBV Pet Source #

Symbolic version of the constructor Bird.

sFish :: SBV Pet Source #

Symbolic version of the constructor Fish.

isDog :: SBV Pet -> SBool Source #

Field recognizer predicate.

isHorse :: SBV Pet -> SBool Source #

Field recognizer predicate.

isCat :: SBV Pet -> SBool Source #

Field recognizer predicate.

isBird :: SBV Pet -> SBool Source #

Field recognizer predicate.

isFish :: SBV Pet -> SBool Source #

Field recognizer predicate.

sCasePet :: Mergeable result => SBV Pet -> result -> result -> result -> result -> result -> result Source #

Case analyzer for the type Pet.

data Sport Source #

Sports they engage in

Constructors

Football
Baseball
Volleyball
Hockey
Tennis

Instances

Instances details

Arbitrary Sport Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods arbitrary :: Gen Sport # shrink :: Sport -> [Sport] #
SymVal Sport Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Sport) Source # mkSymValInit :: State -> SBV Sport -> IO () Source # literal :: Sport -> SBV Sport Source # fromCV :: CV -> Sport Source # isConcretely :: SBV Sport -> (Sport -> Bool) -> Bool Source # minMaxBound :: Maybe (Sport, 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 # unlitCV :: SBV Sport -> Maybe (Kind, CVal) Source # isConcrete :: SBV Sport -> Bool Source # isSymbolic :: SBV Sport -> Bool Source #
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 # isRational :: Sport -> Bool Source # isFP :: Sport -> Bool Source # isUnbounded :: Sport -> Bool Source # isADT :: Sport -> Bool Source # isChar :: Sport -> Bool Source # isString :: Sport -> Bool Source # isList :: Sport -> Bool Source # isSet :: Sport -> Bool Source # isTuple :: Sport -> Bool Source # isArray :: Sport -> Bool Source # isRoundingMode :: Sport -> Bool Source # isUninterpreted :: Sport -> Bool Source # showType :: Sport -> String Source #
EnumSymbolic Sport Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods succ :: SBV Sport -> SBV Sport Source # pred :: SBV Sport -> SBV Sport Source # toEnum :: SInteger -> SBV Sport Source # fromEnum :: SBV Sport -> SInteger Source # enumFrom :: SBV Sport -> SList Sport Source # enumFromThen :: SBV Sport -> SBV Sport -> SList Sport Source # enumFromTo :: SBV Sport -> SBV Sport -> SList Sport Source # enumFromThenTo :: SBV Sport -> SBV Sport -> SBV Sport -> SList Sport 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 #
OrdSymbolic (SBV Sport) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods (.<) :: SBV Sport -> SBV Sport -> SBool Source # (.<=) :: SBV Sport -> SBV Sport -> SBool Source # (.>) :: SBV Sport -> SBV Sport -> SBool Source # (.>=) :: SBV Sport -> SBV Sport -> SBool Source # smin :: SBV Sport -> SBV Sport -> SBV Sport Source # smax :: SBV Sport -> SBV Sport -> SBV Sport Source # inRange :: SBV Sport -> (SBV Sport, SBV Sport) -> SBool Source #
HasInductionSchema (Forall ta Sport -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Sport -> SBool) -> ProofObj Source #
SymVal extraT => HasInductionSchema (Forall ta Sport -> Forall extraS extraT -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Sport -> Forall extraS extraT -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta Sport -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Sport -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta Sport -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Sport -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta Sport -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Sport -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta Sport -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Fish Methods inductionSchema :: (Forall ta Sport -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

cv2Sport :: String -> [CV] -> Sport Source #

Conversion from SMT values to Sport values.

_undefiner_Sport :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type SSport = SBV Sport Source #

Symbolic version of the type Sport.

sFootball :: SBV Sport Source #

Symbolic version of the constructor Football.

sBaseball :: SBV Sport Source #

Symbolic version of the constructor Baseball.

sVolleyball :: SBV Sport Source #

Symbolic version of the constructor Volleyball.

sHockey :: SBV Sport Source #

Symbolic version of the constructor Hockey.

sTennis :: SBV Sport Source #

Symbolic version of the constructor Tennis.

isFootball :: SBV Sport -> SBool Source #

Field recognizer predicate.

isBaseball :: SBV Sport -> SBool Source #

Field recognizer predicate.

isVolleyball :: SBV Sport -> SBool Source #

Field recognizer predicate.

isHockey :: SBV Sport -> SBool Source #

Field recognizer predicate.

isTennis :: SBV Sport -> SBool Source #

Field recognizer predicate.

sCaseSport :: Mergeable result => SBV Sport -> result -> result -> result -> result -> result -> result Source #

Case analyzer for the type Sport.

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 allSatTrackUFs configuration to indicate that the uninterpreted function changes do not matter for generating different values. All we care is that the fishOwner changes!