    -----------------------------------------------------------------------------
    -- |
    -- 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 = [ ("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)
              ]

    -- | 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 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

    -- | 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
    $ "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])