-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Puzzles.Orangutans
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Based on <http://github.com/goldfirere/video-resources/blob/main/2022-08-12-java/Haskell.hs>
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE DeriveGeneric       #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE TemplateHaskell     #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE OverloadedRecordDot #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Puzzles.Orangutans where

import Data.SBV
import GHC.Generics (Generic)

-- $setup
-- >>> -- For doctest purposes only:
-- >>> import Data.SBV

-- | Orangutans in the puzzle.
data Orangutan = Merah   | Ofallo  | Quirrel  | Shamir   deriving (Int -> Orangutan
Orangutan -> Int
Orangutan -> [Orangutan]
Orangutan -> Orangutan
Orangutan -> Orangutan -> [Orangutan]
Orangutan -> Orangutan -> Orangutan -> [Orangutan]
(Orangutan -> Orangutan)
-> (Orangutan -> Orangutan)
-> (Int -> Orangutan)
-> (Orangutan -> Int)
-> (Orangutan -> [Orangutan])
-> (Orangutan -> Orangutan -> [Orangutan])
-> (Orangutan -> Orangutan -> [Orangutan])
-> (Orangutan -> Orangutan -> Orangutan -> [Orangutan])
-> Enum Orangutan
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Orangutan -> Orangutan
succ :: Orangutan -> Orangutan
$cpred :: Orangutan -> Orangutan
pred :: Orangutan -> Orangutan
$ctoEnum :: Int -> Orangutan
toEnum :: Int -> Orangutan
$cfromEnum :: Orangutan -> Int
fromEnum :: Orangutan -> Int
$cenumFrom :: Orangutan -> [Orangutan]
enumFrom :: Orangutan -> [Orangutan]
$cenumFromThen :: Orangutan -> Orangutan -> [Orangutan]
enumFromThen :: Orangutan -> Orangutan -> [Orangutan]
$cenumFromTo :: Orangutan -> Orangutan -> [Orangutan]
enumFromTo :: Orangutan -> Orangutan -> [Orangutan]
$cenumFromThenTo :: Orangutan -> Orangutan -> Orangutan -> [Orangutan]
enumFromThenTo :: Orangutan -> Orangutan -> Orangutan -> [Orangutan]
Enum, Orangutan
Orangutan -> Orangutan -> Bounded Orangutan
forall a. a -> a -> Bounded a
$cminBound :: Orangutan
minBound :: Orangutan
$cmaxBound :: Orangutan
maxBound :: Orangutan
Bounded)

-- | Handlers for each orangutan.
data Handler   = Dolly   | Eva     | Francine | Gracie

-- | Location for each orangutan.
data Location  = Ambalat | Basahan | Kendisi  | Tarakan

mkSymbolicEnumeration ''Orangutan
mkSymbolicEnumeration ''Handler
mkSymbolicEnumeration ''Location

-- | An assignment is solution to the puzzle
data Assignment = MkAssignment { Assignment -> SBV Orangutan
orangutan :: SOrangutan
                               , Assignment -> SHandler
handler   :: SHandler
                               , Assignment -> SLocation
location  :: SLocation
                               , Assignment -> SInteger
age       :: SInteger
                               }
                               deriving ((forall x. Assignment -> Rep Assignment x)
-> (forall x. Rep Assignment x -> Assignment) -> Generic Assignment
forall x. Rep Assignment x -> Assignment
forall x. Assignment -> Rep Assignment x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Assignment -> Rep Assignment x
from :: forall x. Assignment -> Rep Assignment x
$cto :: forall x. Rep Assignment x -> Assignment
to :: forall x. Rep Assignment x -> Assignment
Generic, Bool -> SBool -> Assignment -> Assignment -> Assignment
(Bool -> SBool -> Assignment -> Assignment -> Assignment)
-> (forall b.
    (Ord b, SymVal b, Num b) =>
    [Assignment] -> Assignment -> SBV b -> Assignment)
-> Mergeable Assignment
forall b.
(Ord b, SymVal b, Num b) =>
[Assignment] -> Assignment -> SBV b -> Assignment
forall a.
(Bool -> SBool -> a -> a -> a)
-> (forall b. (Ord b, SymVal b, Num b) => [a] -> a -> SBV b -> a)
-> Mergeable a
$csymbolicMerge :: Bool -> SBool -> Assignment -> Assignment -> Assignment
symbolicMerge :: Bool -> SBool -> Assignment -> Assignment -> Assignment
$cselect :: forall b.
(Ord b, SymVal b, Num b) =>
[Assignment] -> Assignment -> SBV b -> Assignment
select :: forall b.
(Ord b, SymVal b, Num b) =>
[Assignment] -> Assignment -> SBV b -> Assignment
Mergeable)

-- | Create a symbolic assignment, using symbolic fields.
mkSym :: Orangutan -> Symbolic Assignment
mkSym :: Orangutan -> Symbolic Assignment
mkSym Orangutan
o = do let h :: String
h = Orangutan -> String
forall a. Show a => a -> String
show Orangutan
o String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
".handler"
                 l :: String
l = Orangutan -> String
forall a. Show a => a -> String
show Orangutan
o String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
".location"
                 a :: String
a = Orangutan -> String
forall a. Show a => a -> String
show Orangutan
o String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
".age"
             Assignment
s <- SBV Orangutan -> SHandler -> SLocation -> SInteger -> Assignment
MkAssignment (Orangutan -> SBV Orangutan
forall a. SymVal a => a -> SBV a
literal Orangutan
o) (SHandler -> SLocation -> SInteger -> Assignment)
-> SymbolicT IO SHandler
-> SymbolicT IO (SLocation -> SInteger -> Assignment)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> SymbolicT IO SHandler
forall a. SymVal a => String -> Symbolic (SBV a)
free String
h SymbolicT IO (SLocation -> SInteger -> Assignment)
-> SymbolicT IO SLocation -> SymbolicT IO (SInteger -> Assignment)
forall a b.
SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> SymbolicT IO SLocation
forall a. SymVal a => String -> Symbolic (SBV a)
free String
l SymbolicT IO (SInteger -> Assignment)
-> SymbolicT IO SInteger -> Symbolic Assignment
forall a b.
SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> SymbolicT IO SInteger
forall a. SymVal a => String -> Symbolic (SBV a)
free String
a
             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
$ Assignment
s.age SInteger -> [SInteger] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [SInteger
4, SInteger
7, SInteger
10, SInteger
13]
             Assignment -> Symbolic Assignment
forall a. a -> SymbolicT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Assignment
s

-- | We get:
--
-- >>> allSat puzzle
-- Solution #1:
--   Merah.handler    =   Gracie :: Handler
--   Merah.location   =  Tarakan :: Location
--   Merah.age        =       10 :: Integer
--   Ofallo.handler   =      Eva :: Handler
--   Ofallo.location  =  Kendisi :: Location
--   Ofallo.age       =       13 :: Integer
--   Quirrel.handler  =    Dolly :: Handler
--   Quirrel.location =  Basahan :: Location
--   Quirrel.age      =        4 :: Integer
--   Shamir.handler   = Francine :: Handler
--   Shamir.location  =  Ambalat :: Location
--   Shamir.age       =        7 :: Integer
-- This is the only solution.
puzzle :: ConstraintSet
puzzle :: SymbolicT IO ()
puzzle = do
   solution :: [Assignment]
solution@[Assignment
_merah, Assignment
ofallo, Assignment
quirrel, Assignment
shamir] <- (Orangutan -> Symbolic Assignment)
-> [Orangutan] -> SymbolicT IO [Assignment]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Orangutan -> Symbolic Assignment
mkSym [Orangutan
forall a. Bounded a => a
minBound .. Orangutan
forall a. Bounded a => a
maxBound]

   let find :: (Assignment -> SBool) -> Assignment
find Assignment -> SBool
f = (Assignment -> Assignment -> Assignment)
-> [Assignment] -> Assignment
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\Assignment
a1 Assignment
a2 -> SBool -> Assignment -> Assignment -> Assignment
forall a. Mergeable a => SBool -> a -> a -> a
ite (Assignment -> SBool
f Assignment
a1) Assignment
a1 Assignment
a2) [Assignment]
solution

   -- 0. All are different in terms of handlers, locations, and ages
   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
$ [SHandler] -> SBool
forall a. EqSymbolic a => [a] -> SBool
distinct ((Assignment -> SHandler) -> [Assignment] -> [SHandler]
forall a b. (a -> b) -> [a] -> [b]
map (.handler)  [Assignment]
solution)
   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
$ [SLocation] -> SBool
forall a. EqSymbolic a => [a] -> SBool
distinct ((Assignment -> SLocation) -> [Assignment] -> [SLocation]
forall a b. (a -> b) -> [a] -> [b]
map (.location) [Assignment]
solution)
   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] -> SBool
forall a. EqSymbolic a => [a] -> SBool
distinct ((Assignment -> SInteger) -> [Assignment] -> [SInteger]
forall a b. (a -> b) -> [a] -> [b]
map (.age)      [Assignment]
solution)

   -- 1. Shamir is 7 years old.
   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
$ Assignment
shamir.age SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
7

   -- 2. Shamir came from Ambalat.
   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
$ Assignment
shamir.location SLocation -> SLocation -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SLocation
sAmbalat

   -- 3. Quirrel is younger than the ape that was found in Tarakan.
   let tarakan :: Assignment
tarakan = (Assignment -> SBool) -> Assignment
find (\Assignment
a -> Assignment
a.location SLocation -> SLocation -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SLocation
sTarakan)
   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
$ Assignment
quirrel.age SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< Assignment
tarakan.age

   -- 4. Of Ofallo and the ape that was found in Tarakan, one is cared for by Gracie and the other is 13 years old.
   let clue4 :: r -> r -> SBool
clue4 r
a1 r
a2 = r
a1.handler SHandler -> SHandler -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SHandler
sGracie SBool -> SBool -> SBool
.&& r
a2.age a -> a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== a
13
   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
$ Assignment -> Assignment -> SBool
forall {a} {r} {r}.
(EqSymbolic a, HasField "handler" r SHandler, HasField "age" r a,
 Num a) =>
r -> r -> SBool
clue4 Assignment
ofallo Assignment
tarakan SBool -> SBool -> SBool
.|| Assignment -> Assignment -> SBool
forall {a} {r} {r}.
(EqSymbolic a, HasField "handler" r SHandler, HasField "age" r a,
 Num a) =>
r -> r -> SBool
clue4 Assignment
tarakan Assignment
ofallo
   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
$ SBV Orangutan
sOfallo SBV Orangutan -> SBV Orangutan -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= Assignment
tarakan.orangutan

   -- 5. The animal that was found in Ambalat is either the 10-year-old or the animal Francine works with.
   let ambalat :: Assignment
ambalat = (Assignment -> SBool) -> Assignment
find (\Assignment
a -> Assignment
a.location SLocation -> SLocation -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SLocation
sAmbalat)
   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
$ Assignment
ambalat.age SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
10 SBool -> SBool -> SBool
.|| Assignment
ambalat.handler SHandler -> SHandler -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SHandler
sFrancine

   -- 6. Ofallo isn't 10 years old.
   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
$ Assignment
ofallo.age SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
10

   -- 7. The ape that was found in Kendisi is older than the ape Dolly works with.
   let kendisi :: Assignment
kendisi = (Assignment -> SBool) -> Assignment
find (\Assignment
a -> Assignment
a.location SLocation -> SLocation -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SLocation
sKendisi)
   let dolly :: Assignment
dolly   = (Assignment -> SBool) -> Assignment
find (\Assignment
a -> Assignment
a.handler  SHandler -> SHandler -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SHandler
sDolly)
   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
$ Assignment
kendisi.age SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> Assignment
dolly.age