-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Puzzles.Euler185
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- A solution to Project Euler problem #185: <http://projecteuler.net/index.php?section=problems&id=185>
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Puzzles.Euler185 where

import Data.Char (ord)
import Data.SBV

-- | The given guesses and the correct digit counts, encoded as a simple list.
guesses :: [(String, SWord8)]
guesses :: [(String, SWord8)]
guesses = [ (String
"5616185650518293", SWord8
2), (String
"3847439647293047", SWord8
1), (String
"5855462940810587", SWord8
3)
          , (String
"9742855507068353", SWord8
3), (String
"4296849643607543", SWord8
3), (String
"3174248439465858", SWord8
1)
          , (String
"4513559094146117", SWord8
2), (String
"7890971548908067", SWord8
3), (String
"8157356344118483", SWord8
1)
          , (String
"2615250744386899", SWord8
2), (String
"8690095851526254", SWord8
3), (String
"6375711915077050", SWord8
1)
          , (String
"6913859173121360", SWord8
1), (String
"6442889055042768", SWord8
2), (String
"2321386104303845", SWord8
0)
          , (String
"2326509471271448", SWord8
2), (String
"5251583379644322", SWord8
2), (String
"1748270476758276", SWord8
3)
          , (String
"4895722652190306", SWord8
1), (String
"3041631117224635", SWord8
3), (String
"1841236454324589", SWord8
3)
          , (String
"2659862637316867", SWord8
2)
          ]

-- | Encode the problem, note that we check digits are within 0-9 as
-- we use 8-bit words to represent them. Otherwise, the constraints are simply
-- generated by zipping the alleged solution with each guess, and making sure the
-- number of matching digits match what's given in the problem statement.
euler185 :: Symbolic SBool
euler185 :: Symbolic SBool
euler185 = do [SWord8]
soln <- Int -> Symbolic [SWord8]
forall a. SymVal a => Int -> Symbolic [SBV a]
mkExistVars Int
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 (String
b, 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 SWord8
x = (SWord8
x :: SWord8) SWord8 -> SWord8 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SWord8
0 SBool -> SBool -> SBool
.&& SWord8
x SWord8 -> SWord8 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SWord8
9
        eq :: a -> Char -> a
eq a
x 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 Char
'0')) a
1 a
0

-- | Print out the solution nicely. We have:
--
-- >>> solveEuler185
-- 4640261571849533
-- Number of solutions: 1
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
$ String
"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 p
_ (a
_, [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])