-----------------------------------------------------------------------------
-- |
-- 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. [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. Provable 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Int -> SymbolicT IO [Count]
forall a. SymVal a => Int -> Symbolic [SBV a]
mkExistVars 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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [a] -> Int -> a
!! Int
9)
                     String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."
{-# ANN counts ("HLint: ignore Use head" :: String) #-}