    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.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>
    -----------------------------------------------------------------------------

    module Data.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 = [ ("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 = do soln <- mkExistVars 16
                  return $ bAll digit soln &&& bAnd (map (genConstr soln) guesses)
      where genConstr a (b, c) = sum (zipWith eq a b) .== (c :: SWord8)
            digit x = (x :: SWord8) .>= 0 &&& x .<= 9
            eq x y =  ite (x .== fromIntegral (ord y - ord '0')) 1 0

    -- | Print out the solution nicely. We have:
    --
    -- >>> solveEuler185
    -- 4640261571849533
    -- Number of solutions: 1
    solveEuler185 :: IO ()
    solveEuler185 = do res <- allSat euler185
                       cnt <- displayModels disp res
                       putStrLn $ "Number of solutions: " ++ show cnt
       where disp _ (_, ss) = putStrLn $ concatMap show (ss :: [Word8])