content: -----------------------------------------------------------------------------
  -- |
  -- 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 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 = do vs <- getModelValues "fishOwner" `fmap` allSatWith z3{allSatTrackUFs = False} 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
  