{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Puzzles.Coins where
import Data.SBV
type Coin = SWord16
mkCoin :: Int -> Symbolic Coin
mkCoin :: Int -> Symbolic Coin
mkCoin i :: Int
i = do Coin
c <- String -> Symbolic Coin
forall a. SymVal a => String -> Symbolic (SBV a)
exists (String -> Symbolic Coin) -> String -> Symbolic Coin
forall a b. (a -> b) -> a -> b
$ 'c' Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
i
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ (Coin -> SBool) -> [Coin] -> SBool
forall a. (a -> SBool) -> [a] -> SBool
sAny (Coin -> Coin -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Coin
c) [1, 5, 10, 25, 50, 100]
Coin -> Symbolic Coin
forall (m :: * -> *) a. Monad m => a -> m a
return Coin
c
combinations :: [a] -> [[a]]
combinations :: [a] -> [[a]]
combinations coins :: [a]
coins = [[[a]]] -> [[a]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Int -> [a] -> [[a]]
forall t a. (Eq t, Num t) => t -> [a] -> [[a]]
combs Int
i [a]
coins | Int
i <- [1 .. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
coins]]
where combs :: t -> [a] -> [[a]]
combs 0 _ = [[]]
combs _ [] = []
combs k :: t
k (x :: a
x:xs :: [a]
xs) = ([a] -> [a]) -> [[a]] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:) (t -> [a] -> [[a]]
combs (t
kt -> t -> t
forall a. Num a => a -> a -> a
-1) [a]
xs) [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ t -> [a] -> [[a]]
combs t
k [a]
xs
c1 :: [Coin] -> SBool
c1 :: [Coin] -> SBool
c1 xs :: [Coin]
xs = [Coin] -> Coin
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Coin]
xs Coin -> Coin -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= 100
c2 :: [Coin] -> SBool
c2 :: [Coin] -> SBool
c2 xs :: [Coin]
xs = [Coin] -> Coin
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Coin]
xs Coin -> Coin -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= 50
c3 :: [Coin] -> SBool
c3 :: [Coin] -> SBool
c3 xs :: [Coin]
xs = [Coin] -> Coin
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Coin]
xs Coin -> Coin -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= 25
c4 :: [Coin] -> SBool
c4 :: [Coin] -> SBool
c4 xs :: [Coin]
xs = [Coin] -> Coin
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Coin]
xs Coin -> Coin -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= 10
c5 :: [Coin] -> SBool
c5 :: [Coin] -> SBool
c5 xs :: [Coin]
xs = [Coin] -> Coin
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Coin]
xs Coin -> Coin -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= 5
c6 :: [Coin] -> SBool
c6 :: [Coin] -> SBool
c6 xs :: [Coin]
xs = [Coin] -> Coin
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Coin -> Coin) -> [Coin] -> [Coin]
forall a b. (a -> b) -> [a] -> [b]
map Coin -> Coin
forall a. (Mergeable a, EqSymbolic a, Num a) => a -> a
val [Coin]
xs) Coin -> Coin -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= 95
where val :: a -> a
val x :: a
x = SBool -> a -> a -> a
forall a. Mergeable a => SBool -> a -> a -> a
ite (a
x a -> a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== 50) 0 a
x
puzzle :: IO SatResult
puzzle :: IO SatResult
puzzle = SymbolicT IO SBool -> IO SatResult
forall a. Provable a => a -> IO SatResult
sat (SymbolicT IO SBool -> IO SatResult)
-> SymbolicT IO SBool -> IO SatResult
forall a b. (a -> b) -> a -> b
$ do
[Coin]
cs <- (Int -> Symbolic Coin) -> [Int] -> SymbolicT IO [Coin]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Int -> Symbolic Coin
mkCoin [1..6]
(SBool -> SymbolicT IO ()) -> [SBool] -> SymbolicT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain [[Coin] -> SBool
c [Coin]
s | [Coin]
s <- [Coin] -> [[Coin]]
forall a. [a] -> [[a]]
combinations [Coin]
cs, [Coin] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Coin]
s Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 2, [Coin] -> SBool
c <- [[Coin] -> SBool
c1, [Coin] -> SBool
c2, [Coin] -> SBool
c3, [Coin] -> SBool
c4, [Coin] -> SBool
c5, [Coin] -> SBool
c6]]
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ [SBool] -> SBool
sAnd ([SBool] -> SBool) -> [SBool] -> SBool
forall a b. (a -> b) -> a -> b
$ (Coin -> Coin -> SBool) -> [Coin] -> [Coin] -> [SBool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Coin -> Coin -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
(.>=) [Coin]
cs ([Coin] -> [Coin]
forall a. [a] -> [a]
tail [Coin]
cs)
SBool -> SymbolicT IO SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ [Coin] -> Coin
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Coin]
cs Coin -> Coin -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== 115