{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Puzzles.Euler185 where
import Data.Char (ord)
import Data.SBV
guesses :: [(String, SWord8)]
guesses :: [(String, SWord8)]
guesses = [ ("5616185650518293", 2), ("3847439647293047", 1), ("5855462940810587", 3)
, ("9742855507068353", 3), ("4296849643607543", 3), ("3174248439465858", 1)
, ("4513559094146117", 2), ("7890971548908067", 3), ("8157356344118483", 1)
, ("2615250744386899", 2), ("8690095851526254", 3), ("6375711915077050", 1)
, ("6913859173121360", 1), ("6442889055042768", 2), ("2321386104303845", 0)
, ("2326509471271448", 2), ("5251583379644322", 2), ("1748270476758276", 3)
, ("4895722652190306", 1), ("3041631117224635", 3), ("1841236454324589", 3)
, ("2659862637316867", 2)
]
euler185 :: Symbolic SBool
euler185 :: Symbolic SBool
euler185 = do [SWord8]
soln <- Int -> Symbolic [SWord8]
forall a. SymVal a => Int -> Symbolic [SBV a]
mkExistVars 16
SBool -> Symbolic SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> Symbolic SBool) -> SBool -> Symbolic SBool
forall a b. (a -> b) -> a -> b
$ (SWord8 -> SBool) -> [SWord8] -> SBool
forall a. (a -> SBool) -> [a] -> SBool
sAll SWord8 -> SBool
digit [SWord8]
soln SBool -> SBool -> SBool
.&& [SBool] -> SBool
sAnd (((String, SWord8) -> SBool) -> [(String, SWord8)] -> [SBool]
forall a b. (a -> b) -> [a] -> [b]
map ([SWord8] -> (String, SWord8) -> SBool
forall a. (EqSymbolic a, Num a) => [a] -> (String, SWord8) -> SBool
genConstr [SWord8]
soln) [(String, SWord8)]
guesses)
where genConstr :: [a] -> (String, SWord8) -> SBool
genConstr a :: [a]
a (b :: String
b, c :: SWord8
c) = [SWord8] -> SWord8
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((a -> Char -> SWord8) -> [a] -> String -> [SWord8]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> Char -> SWord8
forall a a.
(Mergeable a, EqSymbolic a, Num a, Num a) =>
a -> Char -> a
eq [a]
a String
b) SWord8 -> SWord8 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SWord8
c :: SWord8)
digit :: SWord8 -> SBool
digit x :: SWord8
x = (SWord8
x :: SWord8) SWord8 -> SWord8 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= 0 SBool -> SBool -> SBool
.&& SWord8
x SWord8 -> SWord8 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= 9
eq :: a -> Char -> a
eq x :: a
x y :: Char
y = 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
.== Int -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Char -> Int
ord Char
y Int -> Int -> Int
forall a. Num a => a -> a -> a
- Char -> Int
ord '0')) 1 0
solveEuler185 :: IO ()
solveEuler185 :: IO ()
solveEuler185 = do AllSatResult
res <- Symbolic SBool -> IO AllSatResult
forall a. Provable a => a -> IO AllSatResult
allSat Symbolic SBool
euler185
Int
cnt <- ([(Bool, [Word8])] -> [(Bool, [Word8])])
-> (Int -> (Bool, [Word8]) -> IO ()) -> AllSatResult -> IO Int
forall a.
SatModel a =>
([(Bool, a)] -> [(Bool, a)])
-> (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
displayModels [(Bool, [Word8])] -> [(Bool, [Word8])]
forall a. a -> a
id Int -> (Bool, [Word8]) -> IO ()
forall p a. p -> (a, [Word8]) -> IO ()
disp AllSatResult
res
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Number of solutions: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
cnt
where disp :: p -> (a, [Word8]) -> IO ()
disp _ (_, ss :: [Word8]
ss) = String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ (Word8 -> String) -> [Word8] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Word8 -> String
forall a. Show a => a -> String
show ([Word8]
ss :: [Word8])