sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.Puzzles.Counts

Description

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

Synopsis

- type Count = SWord8
- count :: Count -> [Count] -> [Count]
- puzzle :: [Count] -> SBool
- counts :: IO ()

# Documentation

type Count = SWord8 Source #

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

count :: Count -> [Count] -> [Count] Source #

Given a number, increment the count array depending on the digits of the number

puzzle :: [Count] -> SBool Source #

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.

counts :: IO () Source #

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