{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Puzzles.Newspaper where
import Data.SBV
import Data.SBV.Either
puzzle :: Symbolic ()
puzzle :: Symbolic ()
puzzle = do
SInteger
a <- String -> Symbolic SInteger
sInteger String
"a"
SInteger
b <- String -> Symbolic SInteger
sInteger String
"b"
SBool
c <- String -> Symbolic SBool
sBool String
"c"
SInteger
d <- String -> Symbolic SInteger
sInteger String
"d"
SBool
e <- String -> Symbolic SBool
sBool String
"e"
SInteger
f <- String -> Symbolic SInteger
sInteger String
"f"
SBool
g <- String -> Symbolic SBool
sBool String
"g"
SInteger
h <- String -> Symbolic SInteger
sInteger String
"h"
SBool
i <- String -> Symbolic SBool
sBool String
"i"
SEither Bool Integer
j <- String -> Symbolic (SEither Bool Integer)
forall a b.
(SymVal a, SymVal b) =>
String -> Symbolic (SEither a b)
sEither String
"j"
SBool
jIsInt <- String -> Symbolic SBool
sBool String
"jIsInt"
let ints :: Bool -> [SInteger]
ints Bool
intj = [SInteger
a, SInteger
b, SInteger
d, SInteger
f, SInteger
h] [SInteger] -> [SInteger] -> [SInteger]
forall a. [a] -> [a] -> [a]
++ [SEither Bool Integer -> SInteger
forall a b. (SymVal a, SymVal b) => SEither a b -> SBV b
fromRight SEither Bool Integer
j | Bool
intj]
bools :: Bool -> [SBool]
bools Bool
intj = [SBool
c, SBool
e, SBool
g, SBool
i] [SBool] -> [SBool] -> [SBool]
forall a. [a] -> [a] -> [a]
++ [SEither Bool Integer -> SBool
forall a b. (SymVal a, SymVal b) => SEither a b -> SBV a
fromLeft SEither Bool Integer
j | Bool -> Bool
not Bool
intj]
choice :: (Bool -> a) -> a
choice Bool -> a
fn = SBool -> a -> a -> a
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
jIsInt (Bool -> a
fn Bool
True) (Bool -> a
fn Bool
False)
SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (Bool -> SInteger) -> SInteger
forall {a}. Mergeable a => (Bool -> a) -> a
choice ([SInteger] -> SInteger
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([SInteger] -> SInteger)
-> (Bool -> [SInteger]) -> Bool -> SInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> [SInteger]
ints)
SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SInteger
b SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (Bool -> SInteger) -> SInteger
forall {a}. Mergeable a => (Bool -> a) -> a
choice ([SInteger] -> SInteger
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([SInteger] -> SInteger)
-> (Bool -> [SInteger]) -> Bool -> SInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SBool -> SInteger) -> [SBool] -> [SInteger]
forall a b. (a -> b) -> [a] -> [b]
map SBool -> SInteger
forall a. (Ord a, Num a, SymVal a) => SBool -> SBV a
oneIf ([SBool] -> [SInteger]) -> (Bool -> [SBool]) -> Bool -> [SInteger]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> [SBool]
bools)
SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SBool
c SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (Bool -> SInteger) -> SInteger
forall {a}. Mergeable a => (Bool -> a) -> a
choice ((SInteger -> SInteger -> SInteger) -> [SInteger] -> SInteger
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 SInteger -> SInteger -> SInteger
forall a. OrdSymbolic a => a -> a -> a
smax ([SInteger] -> SInteger)
-> (Bool -> [SInteger]) -> Bool -> SInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> [SInteger]
ints))
SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SInteger
d SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (Bool -> SInteger) -> SInteger
forall {a}. Mergeable a => (Bool -> a) -> a
choice ([SInteger] -> SInteger
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([SInteger] -> SInteger)
-> (Bool -> [SInteger]) -> Bool -> SInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SInteger -> SInteger) -> [SInteger] -> [SInteger]
forall a b. (a -> b) -> [a] -> [b]
map (SBool -> SInteger
forall a. (Ord a, Num a, SymVal a) => SBool -> SBV a
oneIf (SBool -> SInteger) -> (SInteger -> SBool) -> SInteger -> SInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SInteger
d SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.==)) ([SInteger] -> [SInteger])
-> (Bool -> [SInteger]) -> Bool -> [SInteger]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> [SInteger]
ints)
SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SBool
e SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (Bool -> SBool) -> SBool
forall {a}. Mergeable a => (Bool -> a) -> a
choice ((SInteger -> SBool) -> [SInteger] -> SBool
forall a. (a -> SBool) -> [a] -> SBool
sAll (SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0) ([SInteger] -> SBool) -> (Bool -> [SInteger]) -> Bool -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> [SInteger]
ints)
SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SInteger
f SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (Bool -> SInteger) -> SInteger
forall {a}. Mergeable a => (Bool -> a) -> a
choice (Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal (Integer -> SInteger) -> (Bool -> Integer) -> Bool -> SInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> (Bool -> Int) -> Bool -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SInteger] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([SInteger] -> Int) -> (Bool -> [SInteger]) -> Bool -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> [SInteger]
ints) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (Bool -> SInteger) -> SInteger
forall {a}. Mergeable a => (Bool -> a) -> a
choice ([SInteger] -> SInteger
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([SInteger] -> SInteger)
-> (Bool -> [SInteger]) -> Bool -> SInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> [SInteger]
ints)
SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SBool
g SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SInteger
d SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
b)
SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SInteger
h SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
h SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
a
SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SBool
i SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SInteger
f SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
d SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
b SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
h SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
d)
SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
jIsInt (SEither Bool Integer -> SBool
forall a b. (SymVal a, SymVal b) => SEither a b -> SBool
isRight SEither Bool Integer
j) (SEither Bool Integer -> SBool
forall a b. (SymVal a, SymVal b) => SEither a b -> SBool
isLeft SEither Bool Integer
j)
solvePuzzle :: IO ()
solvePuzzle :: IO ()
solvePuzzle = 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
=<< SMTConfig -> Symbolic () -> IO AllSatResult
forall a. Satisfiable a => SMTConfig -> a -> IO AllSatResult
allSatWith SMTConfig
z3{isNonModelVar = (== "jIsInt")} Symbolic ()
puzzle