Data.SBV.Program.Examples

These examples can from GHCi by importing this module. To get a human-readable pseudocode for the solution use

ghci> Right res <- someExample
ghci> putStrLn $ writePseudocode res

Reset most significant set bit

paperRunningExampleSpec :: SimpleSpec Word8

A running example from the original paper. The function should reset the least significant set bit of a 8-byte word: >>> 0001 0010 -> 0000 0010

paperRunningExample :: IO (Either SynthesisError (Program Location (SimpleComponent Word8)))

Quadratic equation

quadEquExampleSpec :: SimpleSpec Int32

Synthesizes a formula for the quadratic equation \(x^2 - 2x + 1 = 0\)

quadEquExample :: IO (Either SynthesisError (Program Location (SimpleComponent Int32)))

Transform boolean formula into NAND-only expression

nandifyExample

Arguments

:: Int

Amount of NAND components available

-> SimpleSpec Bool

Specification of the desired function

-> IO (Either SynthesisError (Program Location (SimpleComponent Bool)))

Reimplement arbitrary boolean formula with only NAND components. Example usage:

nandifyExample 2 (SimpleSpec 2 $ [i1, i2] o -> o .== (i1 .&& i2))