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

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

Data.SBV.Examples.Puzzles.Euler185

Description

A solution to Project Euler problem #185: http://projecteuler.net/index.php?section=problems&id=185

Synopsis

- guesses :: [(String, SWord8)]
- euler185 :: Symbolic SBool
- solveEuler185 :: IO ()

# Documentation

guesses :: [(String, SWord8)] Source

The given guesses and the correct digit counts, encoded as a simple list.

euler185 :: Symbolic SBool Source

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.

solveEuler185 :: IO () Source

Print out the solution nicely. We have:

    >>> solveEuler185
    4640261571849533
    Number of solutions: 1