-----------------------------------------------------------------------------
-- |
-- 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 <- String -> AllSatResult -> [Maybe Nationality]
forall b. SymVal b => String -> AllSatResult -> [Maybe b]
getModelValues String
"fishOwner" (AllSatResult -> [Maybe Nationality])
-> IO AllSatResult -> IO [Maybe Nationality]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` SMTConfig -> SymbolicT IO () -> IO AllSatResult
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)] -> 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 :: SBV Integer -> SBV Color
c = String -> SBV Integer -> SBV Color
forall a. Uninterpreted a => String -> a
uninterpret String
"color"
              n :: SBV Integer -> SBV Nationality
n = String -> SBV Integer -> SBV Nationality
forall a. Uninterpreted a => String -> a
uninterpret String
"nationality"
              b :: SBV Integer -> SBV Beverage
b = String -> SBV Integer -> SBV Beverage
forall a. Uninterpreted a => String -> a
uninterpret String
"beverage"
              p :: SBV Integer -> SBV Pet
p = String -> SBV Integer -> SBV Pet
forall a. Uninterpreted a => String -> a
uninterpret String
"pet"
              s :: SBV Integer -> SBV Sport
s = String -> SBV Integer -> SBV Sport
forall a. Uninterpreted 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 (m :: * -> *). SolverContext m => SBool -> m ()
constrain
              fact1 :: (SBV Integer -> SBool) -> SymbolicT IO ()
fact1 SBV Integer -> SBool
f = do SBV Integer
i <- Symbolic (SBV Integer)
forall a. SymVal a => Symbolic (SBV a)
free_
                           SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Integer
1 SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV Integer
i SBool -> SBool -> SBool
.&& SBV Integer
i SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= (SBV Integer
5 :: SInteger)
                           SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
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 <- Symbolic (SBV Integer)
forall a. SymVal a => Symbolic (SBV a)
free_
                           SBV Integer
j <- Symbolic (SBV Integer)
forall a. SymVal a => Symbolic (SBV a)
free_
                           SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Integer
1 SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV Integer
i SBool -> SBool -> SBool
.&& SBV Integer
i SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= (SBV Integer
5 :: SInteger)
                           SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Integer
1 SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV Integer
j SBool -> SBool -> SBool
.&& SBV Integer
j SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV Integer
5
                           SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV Integer
i SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBV Integer
j
                           SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
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 ((SBV Integer -> SBool) -> SymbolicT IO ())
-> (SBV Integer -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SBV Integer
i   -> SBV Integer -> SBV Nationality
n SBV Integer
i SBV Nationality -> Nationality -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Nationality
Briton     SBool -> SBool -> SBool
.&& SBV Integer -> SBV Color
c SBV Integer
i SBV Color -> Color -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Color
Red
          (SBV Integer -> SBool) -> SymbolicT IO ()
fact1 ((SBV Integer -> SBool) -> SymbolicT IO ())
-> (SBV Integer -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SBV Integer
i   -> SBV Integer -> SBV Nationality
n SBV Integer
i SBV Nationality -> Nationality -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Nationality
Swede      SBool -> SBool -> SBool
.&& SBV Integer -> SBV Pet
p SBV Integer
i SBV Pet -> Pet -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Pet
Dog
          (SBV Integer -> SBool) -> SymbolicT IO ()
fact1 ((SBV Integer -> SBool) -> SymbolicT IO ())
-> (SBV Integer -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SBV Integer
i   -> SBV Integer -> SBV Nationality
n SBV Integer
i SBV Nationality -> Nationality -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Nationality
Dane       SBool -> SBool -> SBool
.&& SBV Integer -> SBV Beverage
b SBV Integer
i SBV Beverage -> Beverage -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Beverage
Tea
          (SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ()
fact2 ((SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ())
-> (SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SBV Integer
i SBV Integer
j -> SBV Integer -> SBV Color
c SBV Integer
i SBV Color -> Color -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Color
Green      SBool -> SBool -> SBool
.&& SBV Integer -> SBV Color
c SBV Integer
j SBV Color -> Color -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Color
White    SBool -> SBool -> SBool
.&& SBV Integer
i SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
jSBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
-SBV Integer
1
          (SBV Integer -> SBool) -> SymbolicT IO ()
fact1 ((SBV Integer -> SBool) -> SymbolicT IO ())
-> (SBV Integer -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SBV Integer
i   -> SBV Integer -> SBV Color
c SBV Integer
i SBV Color -> Color -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Color
Green      SBool -> SBool -> SBool
.&& SBV Integer -> SBV Beverage
b SBV Integer
i SBV Beverage -> Beverage -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Beverage
Coffee
          (SBV Integer -> SBool) -> SymbolicT IO ()
fact1 ((SBV Integer -> SBool) -> SymbolicT IO ())
-> (SBV Integer -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SBV Integer
i   -> SBV Integer -> SBV Sport
s SBV Integer
i SBV Sport -> Sport -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Sport
Football   SBool -> SBool -> SBool
.&& SBV Integer -> SBV Pet
p SBV Integer
i SBV Pet -> Pet -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Pet
Bird
          (SBV Integer -> SBool) -> SymbolicT IO ()
fact1 ((SBV Integer -> SBool) -> SymbolicT IO ())
-> (SBV Integer -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SBV Integer
i   -> SBV Integer -> SBV Color
c SBV Integer
i SBV Color -> Color -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Color
Yellow     SBool -> SBool -> SBool
.&& SBV Integer -> SBV Sport
s SBV Integer
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
$         SBV Integer -> SBV Beverage
b SBV Integer
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
$         SBV Integer -> SBV Nationality
n SBV Integer
1 SBV Nationality -> Nationality -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Nationality
Norwegian
          (SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ()
fact2 ((SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ())
-> (SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SBV Integer
i SBV Integer
j -> SBV Integer -> SBV Sport
s SBV Integer
i SBV Sport -> Sport -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Sport
Volleyball SBool -> SBool -> SBool
.&& SBV Integer -> SBV Pet
p SBV Integer
j SBV Pet -> Pet -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Pet
Cat      SBool -> SBool -> SBool
.&& SBV Integer
i SBV Integer -> SBV Integer -> SBool
forall a. (EqSymbolic a, Num a) => a -> a -> SBool
`neighbor` SBV Integer
j
          (SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ()
fact2 ((SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ())
-> (SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SBV Integer
i SBV Integer
j -> SBV Integer -> SBV Pet
p SBV Integer
i SBV Pet -> Pet -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Pet
Horse      SBool -> SBool -> SBool
.&& SBV Integer -> SBV Sport
s SBV Integer
j SBV Sport -> Sport -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Sport
Baseball SBool -> SBool -> SBool
.&& SBV Integer
i SBV Integer -> SBV Integer -> SBool
forall a. (EqSymbolic a, Num a) => a -> a -> SBool
`neighbor` SBV Integer
j
          (SBV Integer -> SBool) -> SymbolicT IO ()
fact1 ((SBV Integer -> SBool) -> SymbolicT IO ())
-> (SBV Integer -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SBV Integer
i   -> SBV Integer -> SBV Sport
s SBV Integer
i SBV Sport -> Sport -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Sport
Tennis     SBool -> SBool -> SBool
.&& SBV Integer -> SBV Beverage
b SBV Integer
i SBV Beverage -> Beverage -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Beverage
Beer
          (SBV Integer -> SBool) -> SymbolicT IO ()
fact1 ((SBV Integer -> SBool) -> SymbolicT IO ())
-> (SBV Integer -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SBV Integer
i   -> SBV Integer -> SBV Nationality
n SBV Integer
i SBV Nationality -> Nationality -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Nationality
German     SBool -> SBool -> SBool
.&& SBV Integer -> SBV Sport
s SBV Integer
i SBV Sport -> Sport -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Sport
Hockey
          (SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ()
fact2 ((SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ())
-> (SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SBV Integer
i SBV Integer
j -> SBV Integer -> SBV Nationality
n SBV Integer
i SBV Nationality -> Nationality -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Nationality
Norwegian  SBool -> SBool -> SBool
.&& SBV Integer -> SBV Color
c SBV Integer
j SBV Color -> Color -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Color
Blue     SBool -> SBool -> SBool
.&& SBV Integer
i SBV Integer -> SBV Integer -> SBool
forall a. (EqSymbolic a, Num a) => a -> a -> SBool
`neighbor` SBV Integer
j
          (SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ()
fact2 ((SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ())
-> (SBV Integer -> SBV Integer -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \SBV Integer
i SBV Integer
j -> SBV Integer -> SBV Sport
s SBV Integer
i SBV Sport -> Sport -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Sport
Volleyball SBool -> SBool -> SBool
.&& SBV Integer -> SBV Beverage
b SBV Integer
j SBV Beverage -> Beverage -> SBool
forall a. SymVal a => SBV a -> a -> SBool
`is` Beverage
Water    SBool -> SBool -> SBool
.&& SBV Integer
i SBV Integer -> SBV Integer -> SBool
forall a. (EqSymbolic a, Num a) => a -> a -> SBool
`neighbor` SBV Integer
j

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