-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Puzzles.Newspaper
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Solution to the following puzzle (found at <http://hugopeters.me/posts/15>)
-- which contains 10 questions:
--
-- @
-- a. What is sum of all integer answers?
-- b. How many boolean answers are true?
-- c. Is a the largest number?
-- d. How many integers are equal to me?
-- e. Are all integers positive?
-- f. What is the average of all integers?
-- g. Is d strictly larger than b?
-- h. What is a / h?
-- i. Is f equal to d - b - h * d?
-- j. What is the answer to this question?
-- @
--
-- Note that @j@ is ambiguous: It can be a boolean or an integer. We use
-- the solver to decide what its type should be, so that all the other
-- answers are consistent with that decision.
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Puzzles.Newspaper where

import Data.SBV
import Data.SBV.Either

-- | Encoding of the constraints.
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)

    -- a. What is sum of all integer answers?
    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)

    -- b. How many boolean answers are true?
    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)

    -- c. Is a the largest number?
    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))

    -- d. How many integers are equal to me?
    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)

    -- e. Are all integers positive?
    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)

    -- f. What is the average of all integers?
    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)

    -- g. is d strictly larger than 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
$ 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)

    -- h. what is a / h?
    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

    -- i. is f equal to d - b - h * 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
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)

    -- j. what is the answer to this question?
    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)

-- | Print all solutions to the problem. We have:
--
-- >>> solvePuzzle
-- Solution #1:
--   a =         144 :: Integer
--   b =           2 :: Integer
--   c =        True :: Bool
--   d =           2 :: Integer
--   e =       False :: Bool
--   f =          24 :: Integer
--   g =       False :: Bool
--   h =         -12 :: Integer
--   i =        True :: Bool
--   j = Right (-16) :: Either Bool Integer
-- This is the only solution.
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