sbv-10.9: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.Puzzles.Newspaper

Description

Solution to the following puzzle (found at http://hugopeters.me/posts/15) which contains 10 questions:

a. What is sum of all integer answers?
b. How many boolean answers are true?
c. Is a the largest number?
d. How many integers are equal to me?
e. Are all integers positive?
f. What is the average of all integers?
g. Is d strictly larger than b?
h. What is a / h?
i. Is f equal to d - b - h * d?
j. What is the answer to this question?

Note that j is ambiguous: It can be a boolean or an integer. We use the solver to decide what its type should be, so that all the other answers are consistent with that decision.

Synopsis

Documentation

puzzle :: Symbolic () Source #

Encoding of the constraints.

solvePuzzle :: IO () Source #

Print all solutions to the problem. We have:

>>> solvePuzzle
Solution #1:
  a =         144 :: Integer
  b =           2 :: Integer
  c =        True :: Bool
  d =           2 :: Integer
  e =       False :: Bool
  f =          24 :: Integer
  g =       False :: Bool
  h =         -12 :: Integer
  i =        True :: Bool
  j = Right (-16) :: Either Bool Integer
This is the only solution.