{-# 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)
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)
data Handler = Dolly | Eva | Francine | Gracie
data Location = Ambalat | Basahan | Kendisi | Tarakan
mkSymbolicEnumeration ''Orangutan
mkSymbolicEnumeration ''Handler
mkSymbolicEnumeration ''Location
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)
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
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
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)
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
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
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
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
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
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
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