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

{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell     #-}
{-# LANGUAGE TypeApplications    #-}

{-# OPTIONS_GHC -Wall -Werror #-}

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.
mkSymbolic [''Color]

-- | Nationalities of the occupants
data Nationality = Briton | Dane | Swede | Norwegian | German
                 deriving Int -> Nationality -> String -> String
[Nationality] -> String -> String
Nationality -> String
(Int -> Nationality -> String -> String)
-> (Nationality -> String)
-> ([Nationality] -> String -> String)
-> Show Nationality
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Nationality -> String -> String
showsPrec :: Int -> Nationality -> String -> String
$cshow :: Nationality -> String
show :: Nationality -> String
$cshowList :: [Nationality] -> String -> String
showList :: [Nationality] -> String -> String
Show

-- | Make 'Nationality' a symbolic value.
mkSymbolic [''Nationality]

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

-- | Make 'Beverage' a symbolic value.
mkSymbolic [''Beverage]

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

-- | Make 'Pet' a symbolic value.
mkSymbolic [''Pet]

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

-- | Make 'Sport' a symbolic value.
mkSymbolic [''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