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

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

-- | Nationalities of the occupants
data Nationality = Briton | Dane | Swede | Norwegian | German

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

-- | Beverage choices
data Beverage = Tea | Coffee | Milk | Beer | Water

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

-- | Pets they keep
data Pet = Dog | Horse | Cat | Bird | Fish

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

-- | Sports they engage in
data Sport = Football | Baseball | Volleyball | Hockey | Tennis

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

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

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

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

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

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