    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Puzzles.Counts
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Consider the sentence:
    --
    -- @
    --    In this sentence, the number of occurrences of 0 is _, of 1 is _, of 2 is _,
    --    of 3 is _, of 4 is _, of 5 is _, of 6 is _, of 7 is _, of 8 is _, and of 9 is _.
    -- @
    --
    -- The puzzle is to fill the blanks with numbers, such that the sentence
    -- will be correct. There are precisely two solutions to this puzzle, both of
    -- which are found by SBV successfully.
    --
    --  References:
    --
    --    * Douglas Hofstadter, Metamagical Themes, pg. 27.
    --
    --    * <http://mathcentral.uregina.ca/mp/archives/previous2002/dec02sol.html>
    --
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Puzzles.Counts where

    import Data.SBV
    import Data.List (sortOn)

    -- | We will assume each number can be represented by an 8-bit word, i.e., can be at most 128.
    type Count = SWord8

    -- | Given a number, increment the count array depending on the digits of the number
    count :: Count -> [Count] -> [Count]
    count :: Count -> [Count] -> [Count]
    count Count
    n [Count]
    cnts = SBool -> [Count] -> [Count] -> [Count]
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (Count
    n Count -> Count -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .< Count
    10)
                       (Count -> [Count] -> [Count]
    forall {c} {a}.
    (Mergeable c, Num c, Num a, Enum a, EqSymbolic a) =>
    a -> [c] -> [c]
    upd Count
    n [Count]
    cnts)                           -- only one digit
                       (SBool -> [Count] -> [Count] -> [Count]
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (Count
    n Count -> Count -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .< Count
    100)
                            (Count -> [Count] -> [Count]
    forall {c} {a}.
    (Mergeable c, Num c, Num a, Enum a, EqSymbolic a) =>
    a -> [c] -> [c]
    upd Count
    d1 (Count -> [Count] -> [Count]
    forall {c} {a}.
    (Mergeable c, Num c, Num a, Enum a, EqSymbolic a) =>
    a -> [c] -> [c]
    upd Count
    d2 [Count]
    cnts))            -- two digits
                            (Count -> [Count] -> [Count]
    forall {c} {a}.
    (Mergeable c, Num c, Num a, Enum a, EqSymbolic a) =>
    a -> [c] -> [c]
    upd Count
    d1 (Count -> [Count] -> [Count]
    forall {c} {a}.
    (Mergeable c, Num c, Num a, Enum a, EqSymbolic a) =>
    a -> [c] -> [c]
    upd Count
    d2 (Count -> [Count] -> [Count]
    forall {c} {a}.
    (Mergeable c, Num c, Num a, Enum a, EqSymbolic a) =>
    a -> [c] -> [c]
    upd Count
    d3 [Count]
    cnts))))  -- three digits
      where (Count
    r1, Count
    d1)   = Count
    n  Count -> Count -> (Count, Count)
    forall a. SDivisible a => a -> a -> (a, a)
    `sQuotRem` Count
    10
            (Count
    d3, Count
    d2)   = Count
    r1 Count -> Count -> (Count, Count)
    forall a. SDivisible a => a -> a -> (a, a)
    `sQuotRem` Count
    10
            upd :: a -> [c] -> [c]
    upd a
    d = (a -> c -> c) -> [a] -> [c] -> [c]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith a -> c -> c
    forall {a}. (Mergeable a, Num a) => a -> a -> a
    inc [a
    0..]
              where inc :: a -> a -> a
    inc a
    i a
    c = SBool -> a -> a -> a
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (a
    i a -> a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== a
    d) (a
    ca -> a -> a
    forall a. Num a => a -> a -> a
    +a
    1) a
    c

    -- | Encoding of the puzzle. The solution is a sequence of 10 numbers
    -- for the occurrences of the digits such that if we count each digit,
    -- we find these numbers.
    puzzle :: [Count] -> SBool
    puzzle :: [Count] -> SBool
    puzzle [Count]
    cnt = [Count]
    cnt [Count] -> [Count] -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== [[Count]] -> [Count]
    forall a. HasCallStack => [a] -> a
    last [[Count]]
    css
      where ones :: [Count]
    ones = Int -> Count -> [Count]
    forall a. Int -> a -> [a]
    replicate Int
    10 Count
    1  -- all digits occur once to start with
            css :: [[Count]]
    css  = [Count]
    ones [Count] -> [[Count]] -> [[Count]]
    forall a. a -> [a] -> [a]
    : (Count -> [Count] -> [Count]) -> [Count] -> [[Count]] -> [[Count]]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Count -> [Count] -> [Count]
    count [Count]
    cnt [[Count]]
    css

    -- | Finds all two known solutions to this puzzle. We have:
    --
    -- >>> counts
    -- Solution #1
    -- In this sentence, the number of occurrences of 0 is 1, of 1 is 11, of 2 is 2, of 3 is 1, of 4 is 1, of 5 is 1, of 6 is 1, of 7 is 1, of 8 is 1, of 9 is 1.
    -- Solution #2
    -- In this sentence, the number of occurrences of 0 is 1, of 1 is 7, of 2 is 3, of 3 is 2, of 4 is 1, of 5 is 1, of 6 is 1, of 7 is 2, of 8 is 1, of 9 is 1.
    -- Found: 2 solution(s).
    counts :: IO ()
    counts :: IO ()
    counts = do AllSatResult
    res <- SymbolicT IO SBool -> IO AllSatResult
    forall a. Satisfiable a => a -> IO AllSatResult
    allSat (SymbolicT IO SBool -> IO AllSatResult)
    -> SymbolicT IO SBool -> IO AllSatResult
    forall a b. (a -> b) -> a -> b
    $ [Count] -> SBool
    puzzle ([Count] -> SBool) -> SymbolicT IO [Count] -> SymbolicT IO SBool
    forall a b. (a -> b) -> SymbolicT IO a -> SymbolicT IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` Int -> SymbolicT IO [Count]
    forall a. SymVal a => Int -> Symbolic [SBV a]
    mkFreeVars Int
    10
                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]) -> String)
    -> [(Bool, [Word8])] -> [(Bool, [Word8])]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    sortOn (Bool, [Word8]) -> String
    forall a. Show a => a -> String
    show) Int -> (Bool, [Word8]) -> IO ()
    forall {a} {a}. Show a => a -> (a, [Word8]) -> IO ()
    disp AllSatResult
    res
                String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Found: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    cnt String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " solution(s)."
      where disp :: a -> (a, [Word8]) -> IO ()
    disp a
    n (a
    _, [Word8]
    s) = do String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Solution #" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    n
                               [Word8] -> IO ()
    dispSolution [Word8]
    s
            dispSolution :: [Word8] -> IO ()
            dispSolution :: [Word8] -> IO ()
    dispSolution [Word8]
    ns = String -> IO ()
    putStrLn String
    soln
              where soln :: String
    soln =  String
    "In this sentence, the number of occurrences"
                         String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++  String
    " of 0 is " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Word8 -> String
    forall a. Show a => a -> String
    show ([Word8]
    ns [Word8] -> Int -> Word8
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    0)
                         String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ", of 1 is " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Word8 -> String
    forall a. Show a => a -> String
    show ([Word8]
    ns [Word8] -> Int -> Word8
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    1)
                         String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ", of 2 is " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Word8 -> String
    forall a. Show a => a -> String
    show ([Word8]
    ns [Word8] -> Int -> Word8
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    2)
                         String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ", of 3 is " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Word8 -> String
    forall a. Show a => a -> String
    show ([Word8]
    ns [Word8] -> Int -> Word8
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    3)
                         String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ", of 4 is " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Word8 -> String
    forall a. Show a => a -> String
    show ([Word8]
    ns [Word8] -> Int -> Word8
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    4)
                         String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ", of 5 is " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Word8 -> String
    forall a. Show a => a -> String
    show ([Word8]
    ns [Word8] -> Int -> Word8
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    5)
                         String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ", of 6 is " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Word8 -> String
    forall a. Show a => a -> String
    show ([Word8]
    ns [Word8] -> Int -> Word8
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    6)
                         String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ", of 7 is " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Word8 -> String
    forall a. Show a => a -> String
    show ([Word8]
    ns [Word8] -> Int -> Word8
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    7)
                         String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ", of 8 is " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Word8 -> String
    forall a. Show a => a -> String
    show ([Word8]
    ns [Word8] -> Int -> Word8
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    8)
                         String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ", of 9 is " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Word8 -> String
    forall a. Show a => a -> String
    show ([Word8]
    ns [Word8] -> Int -> Word8
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    9)
                         String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "."
    {- HLint ignore counts "Use head" -}