sbv-0.9.5: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers.

Portabilityportable
Stabilityexperimental
Maintainererkokl@gmail.com

Data.SBV.Examples.Puzzles.DogCatMouse

Description

Puzzle: Spend exactly 100 dollars and buy exactly 100 animals. Dogs cost 15 dollars, cats cost 1 dollar, and mice cost 25 cents each. You have to buy at least one of each. How many of each should you buy?

Synopsis

Documentation

type Count = SWord16Source

Use 16-bit words to represent the counts, much larger than we actually need, but no harm.

puzzle :: Count -> Count -> Count -> SBoolSource

Codes the puzzle statement, more or less directly using SBV.

solve :: IO ()Source

prints the only solution:

     dog = 3 :: SWord16
     cat = 41 :: SWord16
     mouse = 56 :: SWord16