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

Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.Puzzles.Euler185

Description

Author : Levent Erkok License : BSD3 Maintainer: erkokl@gmail.com Stability : experimental

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

Synopsis

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