| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Data.SBV.Program.Examples
Description
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
Synopsis
- paperRunningExampleSpec :: SimpleSpec Word8
- paperRunningExample :: IO (Either SynthesisError (Program Location (SimpleComponent Word8)))
- quadEquExampleSpec :: SimpleSpec Int32
- quadEquExample :: IO (Either SynthesisError (Program Location (SimpleComponent Int32)))
- nandifyExample :: Int -> SimpleSpec Bool -> IO (Either SynthesisError (Program Location (SimpleComponent Bool)))
Reset most significant set bit
paperRunningExampleSpec :: SimpleSpec Word8 Source #
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))) Source #
Quadratic equation
quadEquExampleSpec :: SimpleSpec Int32 Source #
Synthesizes a formula for the quadratic equation \(x^2 - 2x + 1 = 0\)
Transform boolean formula into NAND-only expression
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))