{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Puzzles.Birthday where
import Data.SBV
data Month = May | Jun | Jul | Aug
data Day = D14 | D15 | D16 | D17 | D18 | D19
mkSymbolicEnumeration ''Month
mkSymbolicEnumeration ''Day
data Birthday = BD SMonth SDay
mkBirthday :: Symbolic Birthday
mkBirthday :: Symbolic Birthday
mkBirthday = do Birthday
b <- SMonth -> SDay -> Birthday
BD (SMonth -> SDay -> Birthday)
-> SymbolicT IO SMonth -> SymbolicT IO (SDay -> Birthday)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> SymbolicT IO SMonth
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"birthMonth" SymbolicT IO (SDay -> Birthday)
-> SymbolicT IO SDay -> Symbolic Birthday
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 SDay
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"birthDay"
SBool -> ConstraintSet
forall a. QuantifiedBool a => a -> ConstraintSet
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ Birthday -> SBool
valid Birthday
b
Birthday -> Symbolic Birthday
forall a. a -> SymbolicT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Birthday
b
valid :: Birthday -> SBool
valid :: Birthday -> SBool
valid (BD SMonth
m SDay
d) = (SMonth
m SMonth -> SMonth -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SMonth
sMay SBool -> SBool -> SBool
.=> SDay
d SDay -> [SDay] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [SDay
sD15, SDay
sD16, SDay
sD19])
SBool -> SBool -> SBool
.&& (SMonth
m SMonth -> SMonth -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SMonth
sJun SBool -> SBool -> SBool
.=> SDay
d SDay -> [SDay] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [SDay
sD17, SDay
sD18])
SBool -> SBool -> SBool
.&& (SMonth
m SMonth -> SMonth -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SMonth
sJul SBool -> SBool -> SBool
.=> SDay
d SDay -> [SDay] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [SDay
sD14, SDay
sD16])
SBool -> SBool -> SBool
.&& (SMonth
m SMonth -> SMonth -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SMonth
sAug SBool -> SBool -> SBool
.=> SDay
d SDay -> [SDay] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [SDay
sD14, SDay
sD15, SDay
sD17])
puzzle :: ConstraintSet
puzzle :: ConstraintSet
puzzle = do BD SMonth
birthMonth SDay
birthDay <- Symbolic Birthday
mkBirthday
let ok :: [Birthday] -> SBool
ok = (Birthday -> SBool) -> [Birthday] -> SBool
forall a. (a -> SBool) -> [a] -> SBool
sAll Birthday -> SBool
valid
qe :: a -> SBool
qe a
qb = a -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool a
qb
let a1 :: SMonth -> SBool
a1 SMonth
m = (Exists Any Day -> Exists Any Day -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
qe ((Exists Any Day -> Exists Any Day -> SBool) -> SBool)
-> (Exists Any Day -> Exists Any Day -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Exists SDay
d1) (Exists SDay
d2) -> [Birthday] -> SBool
ok [SMonth -> SDay -> Birthday
BD SMonth
m SDay
d1, SMonth -> SDay -> Birthday
BD SMonth
m SDay
d2] SBool -> SBool -> SBool
.&& SDay
d1 SDay -> SDay -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SDay
d2
SBool -> ConstraintSet
forall a. QuantifiedBool a => a -> ConstraintSet
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ SMonth -> SBool
a1 SMonth
birthMonth
let a2 :: SMonth -> SBool
a2 SMonth
m = (Forall Any Day -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
qe ((Forall Any Day -> SBool) -> SBool)
-> (Forall Any Day -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall SDay
d) -> [Birthday] -> SBool
ok [SMonth -> SDay -> Birthday
BD SMonth
m SDay
d] SBool -> SBool -> SBool
.=> (Exists Any Month -> Exists Any Month -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
qe (\(Exists SMonth
m1) (Exists SMonth
m2) -> [Birthday] -> SBool
ok [SMonth -> SDay -> Birthday
BD SMonth
m1 SDay
d, SMonth -> SDay -> Birthday
BD SMonth
m2 SDay
d] SBool -> SBool -> SBool
.&& SMonth
m1 SMonth -> SMonth -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SMonth
m2)
SBool -> ConstraintSet
forall a. QuantifiedBool a => a -> ConstraintSet
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ SMonth -> SBool
a2 SMonth
birthMonth
let b1 :: SDay -> SBool
b1 SDay
d = (Exists Any Month -> Exists Any Month -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
qe ((Exists Any Month -> Exists Any Month -> SBool) -> SBool)
-> (Exists Any Month -> Exists Any Month -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Exists SMonth
m1) (Exists SMonth
m2) -> [Birthday] -> SBool
ok [SMonth -> SDay -> Birthday
BD SMonth
m1 SDay
d, SMonth -> SDay -> Birthday
BD SMonth
m2 SDay
d] SBool -> SBool -> SBool
.&& SMonth
m1 SMonth -> SMonth -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SMonth
m2
SBool -> ConstraintSet
forall a. QuantifiedBool a => a -> ConstraintSet
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ SDay -> SBool
b1 SDay
birthDay
let b2p :: SMonth -> SDay -> SBool
b2p SMonth
m SDay
d = [Birthday] -> SBool
ok [SMonth -> SDay -> Birthday
BD SMonth
m SDay
d] SBool -> SBool -> SBool
.&& SMonth -> SBool
a1 SMonth
m SBool -> SBool -> SBool
.&& SMonth -> SBool
a2 SMonth
m
b2 :: SDay -> SBool
b2 SDay
d = (Forall Any Month -> Forall Any Month -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
qe ((Forall Any Month -> Forall Any Month -> SBool) -> SBool)
-> (Forall Any Month -> Forall Any Month -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall SMonth
m1) (Forall SMonth
m2) -> (SMonth -> SDay -> SBool
b2p SMonth
m1 SDay
d SBool -> SBool -> SBool
.&& SMonth -> SDay -> SBool
b2p SMonth
m2 SDay
d) SBool -> SBool -> SBool
.=> SMonth
m1 SMonth -> SMonth -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SMonth
m2
SBool -> ConstraintSet
forall a. QuantifiedBool a => a -> ConstraintSet
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ SDay -> SBool
b2 SDay
birthDay
let a3p :: SMonth -> SDay -> SBool
a3p SMonth
m SDay
d = [Birthday] -> SBool
ok [SMonth -> SDay -> Birthday
BD SMonth
m SDay
d] SBool -> SBool -> SBool
.&& SMonth -> SBool
a1 SMonth
m SBool -> SBool -> SBool
.&& SMonth -> SBool
a2 SMonth
m SBool -> SBool -> SBool
.&& SDay -> SBool
b1 SDay
d SBool -> SBool -> SBool
.&& SDay -> SBool
b2 SDay
d
a3 :: SMonth -> Forall nm Day -> Forall nm Day -> SBool
a3 SMonth
m = \(Forall SDay
d1) (Forall SDay
d2) -> (SMonth -> SDay -> SBool
a3p SMonth
m SDay
d1 SBool -> SBool -> SBool
.&& SMonth -> SDay -> SBool
a3p SMonth
m SDay
d2) SBool -> SBool -> SBool
.=> SDay
d1 SDay -> SDay -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SDay
d2
(Forall Any Day -> Forall Any Day -> SBool) -> ConstraintSet
forall a. QuantifiedBool a => a -> ConstraintSet
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain ((Forall Any Day -> Forall Any Day -> SBool) -> ConstraintSet)
-> (Forall Any Day -> Forall Any Day -> SBool) -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ SMonth -> Forall Any Day -> Forall Any Day -> SBool
forall {nm :: Symbol} {nm :: Symbol}.
SMonth -> Forall nm Day -> Forall nm Day -> SBool
a3 SMonth
birthMonth
cheryl :: IO ()
cheryl :: IO ()
cheryl = AllSatResult -> IO ()
forall a. Show a => a -> IO ()
print (AllSatResult -> IO ()) -> IO AllSatResult -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConstraintSet -> IO AllSatResult
forall a. Satisfiable a => a -> IO AllSatResult
allSat ConstraintSet
puzzle