-----------------------------------------------------------------------------
-- |
-- Module      :  Data.SBV.Examples.Puzzles.Fish
-- Copyright   :  (c) Levent Erkok
-- License     :  BSD3
-- Maintainer  :  erkokl@gmail.com
-- Stability   :  experimental
--
-- Solves the following logic puzzle:
--
--   - 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 TemplateHaskell     #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Data.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!
fishOwner :: IO ()
fishOwner = do vs <- getModelValues "fishOwner" `fmap` allSat puzzle
               case vs of
                 [Just (v::Nationality)] -> print v
                 []                      -> error "no solution"
                 _                       -> error "no unique solution"
 where puzzle = do

          let c = uninterpret "color"
              n = uninterpret "nationality"
              b = uninterpret "beverage"
              p = uninterpret "pet"
              s = uninterpret "sport"

          let i `neighbor` j = i .== j+1 ||| j .== i+1
              a `is`       v = a .== literal v

          let fact0   = constrain
              fact1 f = do i <- free_
                           constrain $ 1 .<= i &&& i .<= (5 :: SInteger)
                           constrain $ f i
              fact2 f = do i <- free_
                           j <- free_
                           constrain $ 1 .<= i &&& i .<= (5 :: SInteger)
                           constrain $ 1 .<= j &&& j .<= 5
                           constrain $ i ./= j
                           constrain $ f i j

          fact1 $ \i   -> n i `is` Briton     &&& c i `is` Red
          fact1 $ \i   -> n i `is` Swede      &&& p i `is` Dog
          fact1 $ \i   -> n i `is` Dane       &&& b i `is` Tea
          fact2 $ \i j -> c i `is` Green      &&& c j `is` White    &&& i .== j-1
          fact1 $ \i   -> c i `is` Green      &&& b i `is` Coffee
          fact1 $ \i   -> s i `is` Football   &&& p i `is` Bird
          fact1 $ \i   -> c i `is` Yellow     &&& s i `is` Baseball
          fact0 $         b 3 `is` Milk
          fact0 $         n 1 `is` Norwegian
          fact2 $ \i j -> s i `is` Volleyball &&& p j `is` Cat      &&& i `neighbor` j
          fact2 $ \i j -> p i `is` Horse      &&& s j `is` Baseball &&& i `neighbor` j
          fact1 $ \i   -> s i `is` Tennis     &&& b i `is` Beer
          fact1 $ \i   -> n i `is` German     &&& s i `is` Hockey
          fact2 $ \i j -> n i `is` Norwegian  &&& c j `is` Blue     &&& i `neighbor` j
          fact2 $ \i j -> s i `is` Volleyball &&& b j `is` Water    &&& i `neighbor` j

          ownsFish <- free "fishOwner"
          fact1 $ \i -> n i .== ownsFish &&& p i `is` Fish