-----------------------------------------------------------------------------
-- |
-- 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 <- forall a. SymVal a => Int -> Symbolic [SBV a]
mkExistVars Int
16
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (a -> SBool) -> [a] -> SBool
sAll SWord8 -> SBool
digit [SWord8]
soln SBool -> SBool -> SBool
.&& [SBool] -> SBool
sAnd (forall a b. (a -> b) -> [a] -> [b]
map (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) = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {a} {a}.
(Mergeable a, EqSymbolic a, Num a, Num a) =>
a -> Char -> a
eq [a]
a String
b) forall a. EqSymbolic a => a -> a -> SBool
.== (SWord8
c :: SWord8)
        digit :: SWord8 -> SBool
digit SWord8
x = (SWord8
x :: SWord8) forall a. OrdSymbolic a => a -> a -> SBool
.>= SWord8
0 SBool -> SBool -> SBool
.&& SWord8
x forall a. OrdSymbolic a => a -> a -> SBool
.<= SWord8
9
        eq :: a -> Char -> a
eq a
x Char
y =  forall a. Mergeable a => SBool -> a -> a -> a
ite (a
x forall a. EqSymbolic a => a -> a -> SBool
.== forall a b. (Integral a, Num b) => a -> b
fromIntegral (Char -> Int
ord Char
y 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 <- forall a. Provable a => a -> IO AllSatResult
allSat Symbolic SBool
euler185
                   Int
cnt <- forall a.
SatModel a =>
([(Bool, a)] -> [(Bool, a)])
-> (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
displayModels forall a. a -> a
id forall {p} {a}. p -> (a, [Word8]) -> IO ()
disp AllSatResult
res
                   String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Number of solutions: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
cnt
   where disp :: p -> (a, [Word8]) -> IO ()
disp p
_ (a
_, [Word8]
ss) = String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a. Show a => a -> String
show ([Word8]
ss :: [Word8])