-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Puzzles.Fish
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- 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?
------------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE TemplateHaskell     #-}

module Documentation.SBV.Examples.Puzzles.Fish where

import Data.SBV

-- | Colors of houses
data Color = Red | Green | White | Yellow | Blue
           deriving (Int -> Color
Color -> Int
Color -> [Color]
Color -> Color
Color -> Color -> [Color]
Color -> Color -> Color -> [Color]
(Color -> Color)
-> (Color -> Color)
-> (Int -> Color)
-> (Color -> Int)
-> (Color -> [Color])
-> (Color -> Color -> [Color])
-> (Color -> Color -> [Color])
-> (Color -> Color -> Color -> [Color])
-> Enum Color
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Color -> Color
succ :: Color -> Color
$cpred :: Color -> Color
pred :: Color -> Color
$ctoEnum :: Int -> Color
toEnum :: Int -> Color
$cfromEnum :: Color -> Int
fromEnum :: Color -> Int
$cenumFrom :: Color -> [Color]
enumFrom :: Color -> [Color]
$cenumFromThen :: Color -> Color -> [Color]
enumFromThen :: Color -> Color -> [Color]
$cenumFromTo :: Color -> Color -> [Color]
enumFromTo :: Color -> Color -> [Color]
$cenumFromThenTo :: Color -> Color -> Color -> [Color]
enumFromThenTo :: Color -> Color -> Color -> [Color]
Enum, Color
Color -> Color -> Bounded Color
forall a. a -> a -> Bounded a
$cminBound :: Color
minBound :: Color
$cmaxBound :: Color
maxBound :: Color
Bounded)

-- | Make 'Color' a symbolic value.
mkSymbolicEnumeration ''Color

-- | Nationalities of the occupants
data Nationality = Briton | Dane | Swede | Norwegian | German
                 deriving (Int -> Nationality
Nationality -> Int
Nationality -> [Nationality]
Nationality -> Nationality
Nationality -> Nationality -> [Nationality]
Nationality -> Nationality -> Nationality -> [Nationality]
(Nationality -> Nationality)
-> (Nationality -> Nationality)
-> (Int -> Nationality)
-> (Nationality -> Int)
-> (Nationality -> [Nationality])
-> (Nationality -> Nationality -> [Nationality])
-> (Nationality -> Nationality -> [Nationality])
-> (Nationality -> Nationality -> Nationality -> [Nationality])
-> Enum Nationality
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Nationality -> Nationality
succ :: Nationality -> Nationality
$cpred :: Nationality -> Nationality
pred :: Nationality -> Nationality
$ctoEnum :: Int -> Nationality
toEnum :: Int -> Nationality
$cfromEnum :: Nationality -> Int
fromEnum :: Nationality -> Int
$cenumFrom :: Nationality -> [Nationality]
enumFrom :: Nationality -> [Nationality]
$cenumFromThen :: Nationality -> Nationality -> [Nationality]
enumFromThen :: Nationality -> Nationality -> [Nationality]
$cenumFromTo :: Nationality -> Nationality -> [Nationality]
enumFromTo :: Nationality -> Nationality -> [Nationality]
$cenumFromThenTo :: Nationality -> Nationality -> Nationality -> [Nationality]
enumFromThenTo :: Nationality -> Nationality -> Nationality -> [Nationality]
Enum, Nationality
Nationality -> Nationality -> Bounded Nationality
forall a. a -> a -> Bounded a
$cminBound :: Nationality
minBound :: Nationality
$cmaxBound :: Nationality
maxBound :: Nationality
Bounded)

-- | Make 'Nationality' a symbolic value.
mkSymbolicEnumeration ''Nationality

-- | Beverage choices
data Beverage = Tea | Coffee | Milk | Beer | Water
              deriving (Int -> Beverage
Beverage -> Int
Beverage -> [Beverage]
Beverage -> Beverage
Beverage -> Beverage -> [Beverage]
Beverage -> Beverage -> Beverage -> [Beverage]
(Beverage -> Beverage)
-> (Beverage -> Beverage)
-> (Int -> Beverage)
-> (Beverage -> Int)
-> (Beverage -> [Beverage])
-> (Beverage -> Beverage -> [Beverage])
-> (Beverage -> Beverage -> [Beverage])
-> (Beverage -> Beverage -> Beverage -> [Beverage])
-> Enum Beverage
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Beverage -> Beverage
succ :: Beverage -> Beverage
$cpred :: Beverage -> Beverage
pred :: Beverage -> Beverage
$ctoEnum :: Int -> Beverage
toEnum :: Int -> Beverage
$cfromEnum :: Beverage -> Int
fromEnum :: Beverage -> Int
$cenumFrom :: Beverage -> [Beverage]
enumFrom :: Beverage -> [Beverage]
$cenumFromThen :: Beverage -> Beverage -> [Beverage]
enumFromThen :: Beverage -> Beverage -> [Beverage]
$cenumFromTo :: Beverage -> Beverage -> [Beverage]
enumFromTo :: Beverage -> Beverage -> [Beverage]
$cenumFromThenTo :: Beverage -> Beverage -> Beverage -> [Beverage]
enumFromThenTo :: Beverage -> Beverage -> Beverage -> [Beverage]
Enum, Beverage
Beverage -> Beverage -> Bounded Beverage
forall a. a -> a -> Bounded a
$cminBound :: Beverage
minBound :: Beverage
$cmaxBound :: Beverage
maxBound :: Beverage
Bounded)

-- | Make 'Beverage' a symbolic value.
mkSymbolicEnumeration ''Beverage

-- | Pets they keep
data Pet = Dog | Horse | Cat | Bird | Fish
         deriving (Int -> Pet
Pet -> Int
Pet -> [Pet]
Pet -> Pet
Pet -> Pet -> [Pet]
Pet -> Pet -> Pet -> [Pet]
(Pet -> Pet)
-> (Pet -> Pet)
-> (Int -> Pet)
-> (Pet -> Int)
-> (Pet -> [Pet])
-> (Pet -> Pet -> [Pet])
-> (Pet -> Pet -> [Pet])
-> (Pet -> Pet -> Pet -> [Pet])
-> Enum Pet
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Pet -> Pet
succ :: Pet -> Pet
$cpred :: Pet -> Pet
pred :: Pet -> Pet
$ctoEnum :: Int -> Pet
toEnum :: Int -> Pet
$cfromEnum :: Pet -> Int
fromEnum :: Pet -> Int
$cenumFrom :: Pet -> [Pet]
enumFrom :: Pet -> [Pet]
$cenumFromThen :: Pet -> Pet -> [Pet]
enumFromThen :: Pet -> Pet -> [Pet]
$cenumFromTo :: Pet -> Pet -> [Pet]
enumFromTo :: Pet -> Pet -> [Pet]
$cenumFromThenTo :: Pet -> Pet -> Pet -> [Pet]
enumFromThenTo :: Pet -> Pet -> Pet -> [Pet]
Enum, Pet
Pet -> Pet -> Bounded Pet
forall a. a -> a -> Bounded a
$cminBound :: Pet
minBound :: Pet
$cmaxBound :: Pet
maxBound :: Pet
Bounded)

-- | Make 'Pet' a symbolic value.
mkSymbolicEnumeration ''Pet

-- | Sports they engage in
data Sport = Football | Baseball | Volleyball | Hockey | Tennis
           deriving (Int -> Sport
Sport -> Int
Sport -> [Sport]
Sport -> Sport
Sport -> Sport -> [Sport]
Sport -> Sport -> Sport -> [Sport]
(Sport -> Sport)
-> (Sport -> Sport)
-> (Int -> Sport)
-> (Sport -> Int)
-> (Sport -> [Sport])
-> (Sport -> Sport -> [Sport])
-> (Sport -> Sport -> [Sport])
-> (Sport -> Sport -> Sport -> [Sport])
-> Enum Sport
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Sport -> Sport
succ :: Sport -> Sport
$cpred :: Sport -> Sport
pred :: Sport -> Sport
$ctoEnum :: Int -> Sport
toEnum :: Int -> Sport
$cfromEnum :: Sport -> Int
fromEnum :: Sport -> Int
$cenumFrom :: Sport -> [Sport]
enumFrom :: Sport -> [Sport]
$cenumFromThen :: Sport -> Sport -> [Sport]
enumFromThen :: Sport -> Sport -> [Sport]
$cenumFromTo :: Sport -> Sport -> [Sport]
enumFromTo :: Sport -> Sport -> [Sport]
$cenumFromThenTo :: Sport -> Sport -> Sport -> [Sport]
enumFromThenTo :: Sport -> Sport -> Sport -> [Sport]
Enum, Sport
Sport -> Sport -> Bounded Sport
forall a. a -> a -> Bounded a
$cminBound :: Sport
minBound :: Sport
$cmaxBound :: Sport
maxBound :: Sport
Bounded)

-- | Make 'Sport' a symbolic value.
mkSymbolicEnumeration ''Sport

-- | 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!
fishOwner :: IO ()
fishOwner :: IO ()
fishOwner = do [Maybe Nationality]
vs <- String -> AllSatResult -> [Maybe Nationality]
forall b. SymVal b => String -> AllSatResult -> [Maybe b]
getModelValues String
"fishOwner" (AllSatResult -> [Maybe Nationality])
-> IO AllSatResult -> IO [Maybe Nationality]
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` SMTConfig -> SymbolicT IO () -> IO AllSatResult
forall a. Satisfiable a => SMTConfig -> a -> IO AllSatResult
allSatWith SMTConfig
z3{allSatTrackUFs = False} SymbolicT IO ()
puzzle
               case [Maybe Nationality]
vs of
                 [Just (Nationality
v::Nationality)] -> Nationality -> IO ()
forall a. Show a => a -> IO ()
print Nationality
v
                 []                      -> String -> IO ()
forall a. HasCallStack => String -> a
error String
"no solution"
                 [Maybe Nationality]
_                       -> String -> IO ()
forall a. HasCallStack => String -> a
error String
"no unique solution"
 where puzzle :: SymbolicT IO ()
puzzle = do

          let c :: SInteger -> SBV Color
c = String -> SInteger -> SBV Color
forall a. SMTDefinable a => String -> a
uninterpret String
"color"
              n :: SInteger -> SBV Nationality
n = String -> SInteger -> SBV Nationality
forall a. SMTDefinable a => String -> a
uninterpret String
"nationality"
              b :: SInteger -> SBV Beverage
b = String -> SInteger -> SBV Beverage
forall a. SMTDefinable a => String -> a
uninterpret String
"beverage"
              p :: SInteger -> SBV Pet
p = String -> SInteger -> SBV Pet
forall a. SMTDefinable a => String -> a
uninterpret String
"pet"
              s :: SInteger -> SBV Sport
s = String -> SInteger -> SBV Sport
forall a. SMTDefinable a => String -> a
uninterpret String
"sport"

          let a
i neighbor :: a -> a -> SBool
`neighbor` a
j = a
i a -> a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== a
ja -> a -> a
forall a. Num a => a -> a -> a
+a
1 SBool -> SBool -> SBool
.|| a
j a -> a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== a
ia -> a -> a
forall a. Num a => a -> a -> a
+a
1
              SBV a
a is :: SBV a -> a -> SBool
`is`       a
v = SBV a
a SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
v

          let fact0 :: SBool -> SymbolicT IO ()
fact0   = SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain
              fact1 :: (SInteger -> a) -> SymbolicT IO ()
fact1 SInteger -> a
f = do SInteger
i <- Symbolic SInteger
forall a. SymVal a => Symbolic (SBV a)
free_
                           SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SInteger
1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
i SBool -> SBool -> SBool
.&& SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= (SInteger
5 :: SInteger)
                           a -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (a -> SymbolicT IO ()) -> a -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SInteger -> a
f SInteger
i
              fact2 :: (SInteger -> SInteger -> a) -> SymbolicT IO ()
fact2 SInteger -> SInteger -> a
f = do SInteger
i <- Symbolic SInteger
forall a. SymVal a => Symbolic (SBV a)
free_
                           SInteger
j <- Symbolic SInteger
forall a. SymVal a => Symbolic (SBV a)
free_
                           SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SInteger
1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
i SBool -> SBool -> SBool
.&& SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= (SInteger
5 :: SInteger)
                           SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SInteger
1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
j SBool -> SBool -> SBool
.&& SInteger
j SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
5
                           SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SInteger
i SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
j
                           a -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (a -> SymbolicT IO ()) -> a -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SInteger -> SInteger -> a
f SInteger
i SInteger
j

          (SInteger -> SBool) -> SymbolicT IO ()
forall {a}. QuantifiedBool a => (SInteger -> a) -> SymbolicT IO ()
fact1 ((SInteger -> SBool) -> SymbolicT IO ())
-> (SInteger -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SInteger
i   -> SInteger -> SBV Nationality
n SInteger
i SBV Nationality -> Nationality -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Nationality
Briton     SBool -> SBool -> SBool
.&& SInteger -> SBV Color
c SInteger
i SBV Color -> Color -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Color
Red
          (SInteger -> SBool) -> SymbolicT IO ()
forall {a}. QuantifiedBool a => (SInteger -> a) -> SymbolicT IO ()
fact1 ((SInteger -> SBool) -> SymbolicT IO ())
-> (SInteger -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SInteger
i   -> SInteger -> SBV Nationality
n SInteger
i SBV Nationality -> Nationality -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Nationality
Swede      SBool -> SBool -> SBool
.&& SInteger -> SBV Pet
p SInteger
i SBV Pet -> Pet -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Pet
Dog
          (SInteger -> SBool) -> SymbolicT IO ()
forall {a}. QuantifiedBool a => (SInteger -> a) -> SymbolicT IO ()
fact1 ((SInteger -> SBool) -> SymbolicT IO ())
-> (SInteger -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SInteger
i   -> SInteger -> SBV Nationality
n SInteger
i SBV Nationality -> Nationality -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Nationality
Dane       SBool -> SBool -> SBool
.&& SInteger -> SBV Beverage
b SInteger
i SBV Beverage -> Beverage -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Beverage
Tea
          (SInteger -> SInteger -> SBool) -> SymbolicT IO ()
forall {a}.
QuantifiedBool a =>
(SInteger -> SInteger -> a) -> SymbolicT IO ()
fact2 ((SInteger -> SInteger -> SBool) -> SymbolicT IO ())
-> (SInteger -> SInteger -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SInteger
i SInteger
j -> SInteger -> SBV Color
c SInteger
i SBV Color -> Color -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Color
Green      SBool -> SBool -> SBool
.&& SInteger -> SBV Color
c SInteger
j SBV Color -> Color -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Color
White    SBool -> SBool -> SBool
.&& SInteger
i SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
jSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1
          (SInteger -> SBool) -> SymbolicT IO ()
forall {a}. QuantifiedBool a => (SInteger -> a) -> SymbolicT IO ()
fact1 ((SInteger -> SBool) -> SymbolicT IO ())
-> (SInteger -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SInteger
i   -> SInteger -> SBV Color
c SInteger
i SBV Color -> Color -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Color
Green      SBool -> SBool -> SBool
.&& SInteger -> SBV Beverage
b SInteger
i SBV Beverage -> Beverage -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Beverage
Coffee
          (SInteger -> SBool) -> SymbolicT IO ()
forall {a}. QuantifiedBool a => (SInteger -> a) -> SymbolicT IO ()
fact1 ((SInteger -> SBool) -> SymbolicT IO ())
-> (SInteger -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SInteger
i   -> SInteger -> SBV Sport
s SInteger
i SBV Sport -> Sport -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Sport
Football   SBool -> SBool -> SBool
.&& SInteger -> SBV Pet
p SInteger
i SBV Pet -> Pet -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Pet
Bird
          (SInteger -> SBool) -> SymbolicT IO ()
forall {a}. QuantifiedBool a => (SInteger -> a) -> SymbolicT IO ()
fact1 ((SInteger -> SBool) -> SymbolicT IO ())
-> (SInteger -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SInteger
i   -> SInteger -> SBV Color
c SInteger
i SBV Color -> Color -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Color
Yellow     SBool -> SBool -> SBool
.&& SInteger -> SBV Sport
s SInteger
i SBV Sport -> Sport -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Sport
Baseball
          SBool -> SymbolicT IO ()
fact0 (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$         SInteger -> SBV Beverage
b SInteger
3 SBV Beverage -> Beverage -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Beverage
Milk
          SBool -> SymbolicT IO ()
fact0 (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$         SInteger -> SBV Nationality
n SInteger
1 SBV Nationality -> Nationality -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Nationality
Norwegian
          (SInteger -> SInteger -> SBool) -> SymbolicT IO ()
forall {a}.
QuantifiedBool a =>
(SInteger -> SInteger -> a) -> SymbolicT IO ()
fact2 ((SInteger -> SInteger -> SBool) -> SymbolicT IO ())
-> (SInteger -> SInteger -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SInteger
i SInteger
j -> SInteger -> SBV Sport
s SInteger
i SBV Sport -> Sport -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Sport
Volleyball SBool -> SBool -> SBool
.&& SInteger -> SBV Pet
p SInteger
j SBV Pet -> Pet -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Pet
Cat      SBool -> SBool -> SBool
.&& SInteger
i SInteger -> SInteger -> SBool
forall {a}. (EqSymbolic a, Num a) => a -> a -> SBool
`neighbor` SInteger
j
          (SInteger -> SInteger -> SBool) -> SymbolicT IO ()
forall {a}.
QuantifiedBool a =>
(SInteger -> SInteger -> a) -> SymbolicT IO ()
fact2 ((SInteger -> SInteger -> SBool) -> SymbolicT IO ())
-> (SInteger -> SInteger -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SInteger
i SInteger
j -> SInteger -> SBV Pet
p SInteger
i SBV Pet -> Pet -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Pet
Horse      SBool -> SBool -> SBool
.&& SInteger -> SBV Sport
s SInteger
j SBV Sport -> Sport -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Sport
Baseball SBool -> SBool -> SBool
.&& SInteger
i SInteger -> SInteger -> SBool
forall {a}. (EqSymbolic a, Num a) => a -> a -> SBool
`neighbor` SInteger
j
          (SInteger -> SBool) -> SymbolicT IO ()
forall {a}. QuantifiedBool a => (SInteger -> a) -> SymbolicT IO ()
fact1 ((SInteger -> SBool) -> SymbolicT IO ())
-> (SInteger -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SInteger
i   -> SInteger -> SBV Sport
s SInteger
i SBV Sport -> Sport -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Sport
Tennis     SBool -> SBool -> SBool
.&& SInteger -> SBV Beverage
b SInteger
i SBV Beverage -> Beverage -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Beverage
Beer
          (SInteger -> SBool) -> SymbolicT IO ()
forall {a}. QuantifiedBool a => (SInteger -> a) -> SymbolicT IO ()
fact1 ((SInteger -> SBool) -> SymbolicT IO ())
-> (SInteger -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SInteger
i   -> SInteger -> SBV Nationality
n SInteger
i SBV Nationality -> Nationality -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Nationality
German     SBool -> SBool -> SBool
.&& SInteger -> SBV Sport
s SInteger
i SBV Sport -> Sport -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Sport
Hockey
          (SInteger -> SInteger -> SBool) -> SymbolicT IO ()
forall {a}.
QuantifiedBool a =>
(SInteger -> SInteger -> a) -> SymbolicT IO ()
fact2 ((SInteger -> SInteger -> SBool) -> SymbolicT IO ())
-> (SInteger -> SInteger -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SInteger
i SInteger
j -> SInteger -> SBV Nationality
n SInteger
i SBV Nationality -> Nationality -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Nationality
Norwegian  SBool -> SBool -> SBool
.&& SInteger -> SBV Color
c SInteger
j SBV Color -> Color -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Color
Blue     SBool -> SBool -> SBool
.&& SInteger
i SInteger -> SInteger -> SBool
forall {a}. (EqSymbolic a, Num a) => a -> a -> SBool
`neighbor` SInteger
j
          (SInteger -> SInteger -> SBool) -> SymbolicT IO ()
forall {a}.
QuantifiedBool a =>
(SInteger -> SInteger -> a) -> SymbolicT IO ()
fact2 ((SInteger -> SInteger -> SBool) -> SymbolicT IO ())
-> (SInteger -> SInteger -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SInteger
i SInteger
j -> SInteger -> SBV Sport
s SInteger
i SBV Sport -> Sport -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Sport
Volleyball SBool -> SBool -> SBool
.&& SInteger -> SBV Beverage
b SInteger
j SBV Beverage -> Beverage -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Beverage
Water    SBool -> SBool -> SBool
.&& SInteger
i SInteger -> SInteger -> SBool
forall {a}. (EqSymbolic a, Num a) => a -> a -> SBool
`neighbor` SInteger
j

          SBV Nationality
ownsFish <- String -> Symbolic (SBV Nationality)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"fishOwner"
          (SInteger -> SBool) -> SymbolicT IO ()
forall {a}. QuantifiedBool a => (SInteger -> a) -> SymbolicT IO ()
fact1 ((SInteger -> SBool) -> SymbolicT IO ())
-> (SInteger -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SInteger
i -> SInteger -> SBV Nationality
n SInteger
i SBV Nationality -> SBV Nationality -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Nationality
ownsFish SBool -> SBool -> SBool
.&& SInteger -> SBV Pet
p SInteger
i SBV Pet -> Pet -> SBool
forall {a}. SymVal a => SBV a -> a -> SBool
`is` Pet
Fish