-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
--   
@package sbv
@version 3.2


-- | Low level functions to access the SBV infrastructure, for developers
--   who want to build further tools on top of SBV. End-users of the
--   library should not need to use this module.
module Data.SBV.Internals

-- | Result of running a symbolic computation
data Result

-- | Different means of running a symbolic piece of code
data SBVRunMode

-- | Symbolic simulation mode, for proof purposes. Bool is True if it's a
--   sat instance. SMTConfig is used for <tt>sBranch</tt> calls.
Proof :: (Bool, Maybe SMTConfig) -> SBVRunMode

-- | Code generation mode
CodeGen :: SBVRunMode

-- | Concrete simulation mode. The StdGen is for the pConstrain acceptance
--   in cross runs
Concrete :: StdGen -> SBVRunMode

-- | Run a symbolic computation in Proof mode and return a <a>Result</a>.
--   The boolean argument indicates if this is a sat instance or not.
runSymbolic :: (Bool, Maybe SMTConfig) -> Symbolic a -> IO Result

-- | Run a symbolic computation, and return a extra value paired up with
--   the <a>Result</a>
runSymbolic' :: SBVRunMode -> Symbolic a -> IO (a, Result)

-- | The <a>Symbolic</a> value. Either a constant (<tt>Left</tt>) or a
--   symbolic value (<tt>Right Cached</tt>). Note that caching is essential
--   for making sure sharing is preserved. The parameter <tt>a</tt> is
--   phantom, but is extremely important in keeping the user interface
--   strongly typed.
data SBV a
SBV :: !Kind -> !(Either CW (Cached SW)) -> SBV a

-- | Explicit sharing combinator. The SBV library has internal
--   caching/hash-consing mechanisms built in, based on Andy Gill's
--   type-safe obervable sharing technique (see:
--   <a>http://ittc.ku.edu/~andygill/paper.php?label=DSLExtract09</a>).
--   However, there might be times where being explicit on the sharing can
--   help, especially in experimental code. The <a>slet</a> combinator
--   ensures that its first argument is computed once and passed on to its
--   continuation, explicitly indicating the intent of sharing. Most use
--   cases of the SBV library should simply use Haskell's <tt>let</tt>
--   construct for this purpose.
slet :: (HasKind a, HasKind b) => SBV a -> (SBV a -> SBV b) -> SBV b

-- | <a>CW</a> represents a concrete word of a fixed size: Endianness is
--   mostly irrelevant (see the <tt>FromBits</tt> class). For signed words,
--   the most significant digit is considered to be the sign.
data CW
CW :: !Kind -> !CWVal -> CW
cwKind :: CW -> !Kind
cwVal :: CW -> !CWVal

-- | Kind of symbolic value
data Kind
KBool :: Kind
KBounded :: Bool -> Int -> Kind
KUnbounded :: Kind
KReal :: Kind
KUninterpreted :: String -> Kind
KFloat :: Kind
KDouble :: Kind

-- | A constant value
data CWVal

-- | algebraic real
CWAlgReal :: AlgReal -> CWVal

-- | bit-vector/unbounded integer
CWInteger :: Integer -> CWVal

-- | float
CWFloat :: Float -> CWVal

-- | double
CWDouble :: Double -> CWVal

-- | value of an uninterpreted kind
CWUninterpreted :: String -> CWVal

-- | Algebraic reals. Note that the representation is left abstract. We
--   represent rational results explicitly, while the roots-of-polynomials
--   are represented implicitly by their defining equation
data AlgReal
AlgRational :: Bool -> Rational -> AlgReal
AlgPolyRoot :: (Integer, Polynomial) -> (Maybe String) -> AlgReal

-- | Create a constant word from an integral
mkConstCW :: Integral a => Kind -> a -> CW

-- | Generate a finite symbolic bitvector, named
genVar :: (Random a, SymWord a) => Maybe Quantifier -> Kind -> String -> Symbolic (SBV a)

-- | Generate a finite symbolic bitvector, unnamed
genVar_ :: (Random a, SymWord a) => Maybe Quantifier -> Kind -> Symbolic (SBV a)

-- | Lower level version of <a>compileToC</a>, producing a
--   <a>CgPgmBundle</a>
compileToC' :: String -> SBVCodeGen () -> IO CgPgmBundle

-- | Lower level version of <a>compileToCLib</a>, producing a
--   <a>CgPgmBundle</a>
compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO CgPgmBundle

-- | Representation of a collection of generated programs.
data CgPgmBundle
CgPgmBundle :: (Maybe Int, Maybe CgSRealType) -> [(FilePath, (CgPgmKind, [Doc]))] -> CgPgmBundle

-- | Different kinds of "files" we can produce. Currently this is quite
--   <a>C</a> specific.
data CgPgmKind
CgMakefile :: [String] -> CgPgmKind
CgHeader :: [Doc] -> CgPgmKind
CgSource :: CgPgmKind
CgDriver :: CgPgmKind


-- | (The sbv library is hosted at
--   <a>http://github.com/LeventErkok/sbv</a>. Comments, bug reports, and
--   patches are always welcome.)
--   
--   SBV: SMT Based Verification
--   
--   Express properties about Haskell programs and automatically prove them
--   using SMT solvers.
--   
--   <pre>
--   &gt;&gt;&gt; prove $ \x -&gt; x `shiftL` 2 .== 4 * (x :: SWord8)
--   Q.E.D.
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; prove $ forAll ["x"] $ \x -&gt; x `shiftL` 2 .== (x :: SWord8)
--   Falsifiable. Counter-example:
--     x = 51 :: SWord8
--   </pre>
--   
--   The function <a>prove</a> has the following type:
--   
--   <pre>
--   <a>prove</a> :: <a>Provable</a> a =&gt; a -&gt; <a>IO</a> <a>ThmResult</a>
--   </pre>
--   
--   The class <a>Provable</a> comes with instances for n-ary predicates,
--   for arbitrary n. The predicates are just regular Haskell functions
--   over symbolic signed and unsigned bit-vectors. Functions for checking
--   satisfiability (<a>sat</a> and <a>allSat</a>) are also provided.
--   
--   In particular, the sbv library introduces the types:
--   
--   <ul>
--   <li><a>SBool</a>: Symbolic Booleans (bits).</li>
--   <li><a>SWord8</a>, <a>SWord16</a>, <a>SWord32</a>, <a>SWord64</a>:
--   Symbolic Words (unsigned).</li>
--   <li><a>SInt8</a>, <a>SInt16</a>, <a>SInt32</a>, <a>SInt64</a>:
--   Symbolic Ints (signed).</li>
--   <li><a>SInteger</a>: Unbounded signed integers.</li>
--   <li><a>SReal</a>: Algebraic-real numbers</li>
--   <li><a>SFloat</a>: IEEE-754 single-precision floating point
--   values</li>
--   <li><a>SDouble</a>: IEEE-754 double-precision floating point
--   values</li>
--   <li><a>SArray</a>, <a>SFunArray</a>: Flat arrays of symbolic
--   values.</li>
--   <li>Symbolic polynomials over GF(2^n), polynomial arithmetic, and
--   CRCs.</li>
--   <li>Uninterpreted constants and functions over symbolic values, with
--   user defined SMT-Lib axioms.</li>
--   <li>Uninterpreted sorts, and proofs over such sorts, potentially with
--   axioms.</li>
--   </ul>
--   
--   The user can construct ordinary Haskell programs using these types,
--   which behave very similar to their concrete counterparts. In
--   particular these types belong to the standard classes <a>Num</a>,
--   <a>Bits</a>, custom versions of <a>Eq</a> (<a>EqSymbolic</a>) and
--   <a>Ord</a> (<a>OrdSymbolic</a>), along with several other custom
--   classes for simplifying programming with symbolic values. The
--   framework takes full advantage of Haskell's type inference to avoid
--   many common mistakes.
--   
--   Furthermore, predicates (i.e., functions that return <a>SBool</a>)
--   built out of these types can also be:
--   
--   <ul>
--   <li>proven correct via an external SMT solver (the <a>prove</a>
--   function)</li>
--   <li>checked for satisfiability (the <a>sat</a>, <a>allSat</a>
--   functions)</li>
--   <li>used in synthesis (the <a>sat</a> function with existentials)</li>
--   <li>quick-checked</li>
--   </ul>
--   
--   If a predicate is not valid, <a>prove</a> will return a
--   counterexample: An assignment to inputs such that the predicate fails.
--   The <a>sat</a> function will return a satisfying assignment, if there
--   is one. The <a>allSat</a> function returns all satisfying assignments,
--   lazily.
--   
--   The sbv library uses third-party SMT solvers via the standard SMT-Lib
--   interface: <a>http://goedel.cs.uiowa.edu/smtlib/</a>.
--   
--   The SBV library is designed to work with any SMT-Lib compliant
--   SMT-solver. Currently, we support the following SMT-Solvers out-of-the
--   box:
--   
--   <ul>
--   <li>Z3 from Microsoft:
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/</a></li>
--   <li>Yices from SRI: <a>http://yices.csl.sri.com/</a></li>
--   <li>CVC4 from New York University and University of Iowa:
--   <a>http://cvc4.cs.nyu.edu/</a></li>
--   <li>Boolector from Johannes Kepler University:
--   <a>http://fmv.jku.at/boolector/</a></li>
--   <li>MathSAT from Fondazione Bruno Kessler and DISI-University of
--   Trento: <a>http://mathsat.fbk.eu/</a></li>
--   </ul>
--   
--   SBV also allows calling these solvers in parallel, either getting
--   results from multiple solvers or returning the fastest one. (See
--   <a>proveWithAll</a>, <a>proveWithAny</a>, etc.)
--   
--   Support for other compliant solvers can be added relatively easily,
--   please get in touch if there is a solver you'd like to see included.
module Data.SBV

-- | A symbolic boolean/bit
type SBool = SBV Bool

-- | 8-bit unsigned symbolic value
type SWord8 = SBV Word8

-- | 16-bit unsigned symbolic value
type SWord16 = SBV Word16

-- | 32-bit unsigned symbolic value
type SWord32 = SBV Word32

-- | 64-bit unsigned symbolic value
type SWord64 = SBV Word64

-- | 8-bit signed symbolic value, 2's complement representation
type SInt8 = SBV Int8

-- | 16-bit signed symbolic value, 2's complement representation
type SInt16 = SBV Int16

-- | 32-bit signed symbolic value, 2's complement representation
type SInt32 = SBV Int32

-- | 64-bit signed symbolic value, 2's complement representation
type SInt64 = SBV Int64

-- | Infinite precision signed symbolic value
type SInteger = SBV Integer

-- | IEEE-754 single-precision floating point numbers
type SFloat = SBV Float

-- | IEEE-754 double-precision floating point numbers
type SDouble = SBV Double

-- | Rounding mode to be used for the IEEE floating-point operations. Note
--   that Haskell's default is <a>RoundNearestTiesToEven</a>. If you use a
--   different rounding mode, then the counter-examples you get may not
--   match what you observe in Haskell.
data RoundingMode

-- | Round to nearest representable floating point value. If precisely at
--   half-way, pick the even number. (In this context, <i>even</i> means
--   the lowest-order bit is zero.)
RoundNearestTiesToEven :: RoundingMode

-- | Round to nearest representable floating point value. If precisely at
--   half-way, pick the number further away from 0. (That is, for positive
--   values, pick the greater; for negative values, pick the smaller.)
RoundNearestTiesToAway :: RoundingMode

-- | Round towards positive infinity. (Also known as rounding-up or
--   ceiling.)
RoundTowardPositive :: RoundingMode

-- | Round towards negative infinity. (Also known as rounding-down or
--   floor.)
RoundTowardNegative :: RoundingMode

-- | Round towards zero. (Also known as truncation.)
RoundTowardZero :: RoundingMode

-- | Not-A-Number for <a>Double</a> and <a>Float</a>. Surprisingly, Haskell
--   Prelude doesn't have this value defined, so we provide it here.
nan :: Floating a => a

-- | Infinity for <a>Double</a> and <a>Float</a>. Surprisingly, Haskell
--   Prelude doesn't have this value defined, so we provide it here.
infinity :: Floating a => a

-- | Symbolic variant of Not-A-Number. This value will inhabit both
--   <a>SDouble</a> and <a>SFloat</a>.
sNaN :: (Floating a, SymWord a) => SBV a

-- | Symbolic variant of infinity. This value will inhabit both
--   <a>SDouble</a> and <a>SFloat</a>.
sInfinity :: (Floating a, SymWord a) => SBV a

-- | Fused-multiply add. <tt>fusedMA a b c = a * b + c</tt>, for double and
--   floating point values. Note that a <a>fusedMA</a> call will *never* be
--   concrete, even if all the arguments are constants; since we cannot
--   guarantee the precision requirements, which is the whole reason why
--   <a>fusedMA</a> exists in the first place. (NB. <a>fusedMA</a> only
--   rounds once, even though it does two operations, and hence the extra
--   precision.)
fusedMA :: (SymWord a, Floating a) => SBV a -> SBV a -> SBV a -> SBV a

-- | Note that the floating point value NaN does not compare equal to
--   itself, so we need a special recognizer for that. Haskell provides the
--   isNaN predicate with the <a>RealFrac</a> class, which unfortunately is
--   not currently implementable for symbolic cases. (Requires
--   trigonometric functions etc.) Thus, we provide this recognizer
--   separately. Note that the definition simply tests equality against
--   itself, which fails for NaN. Who said equality for floating point was
--   reflexive?
isSNaN :: (Floating a, SymWord a) => SBV a -> SBool

-- | We call a FP number FPPoint if it is neither NaN, nor +/- infinity.
isFPPoint :: (Floating a, SymWord a) => SBV a -> SBool

-- | Infinite precision symbolic algebraic real value
type SReal = SBV AlgReal

-- | Algebraic reals. Note that the representation is left abstract. We
--   represent rational results explicitly, while the roots-of-polynomials
--   are represented implicitly by their defining equation
data AlgReal

-- | Promote an SInteger to an SReal
toSReal :: SInteger -> SReal

-- | Declare an <a>SBool</a>
sBool :: String -> Symbolic SBool

-- | Declare an <a>SWord8</a>
sWord8 :: String -> Symbolic SWord8

-- | Declare an <a>SWord16</a>
sWord16 :: String -> Symbolic SWord16

-- | Declare an <a>SWord32</a>
sWord32 :: String -> Symbolic SWord32

-- | Declare an <a>SWord64</a>
sWord64 :: String -> Symbolic SWord64

-- | Declare an <a>SInt8</a>
sInt8 :: String -> Symbolic SInt8

-- | Declare an <a>SInt16</a>
sInt16 :: String -> Symbolic SInt16

-- | Declare an <a>SInt32</a>
sInt32 :: String -> Symbolic SInt32

-- | Declare an <a>SInt64</a>
sInt64 :: String -> Symbolic SInt64

-- | Declare an <a>SInteger</a>
sInteger :: String -> Symbolic SInteger

-- | Declare an <a>SReal</a>
sReal :: String -> Symbolic SReal

-- | Declare an <a>SFloat</a>
sFloat :: String -> Symbolic SFloat

-- | Declare an <a>SDouble</a>
sDouble :: String -> Symbolic SDouble

-- | Declare a list of <a>SBool</a>s
sBools :: [String] -> Symbolic [SBool]

-- | Declare a list of <a>SWord8</a>s
sWord8s :: [String] -> Symbolic [SWord8]

-- | Declare a list of <a>SWord16</a>s
sWord16s :: [String] -> Symbolic [SWord16]

-- | Declare a list of <a>SWord32</a>s
sWord32s :: [String] -> Symbolic [SWord32]

-- | Declare a list of <a>SWord64</a>s
sWord64s :: [String] -> Symbolic [SWord64]

-- | Declare a list of <a>SInt8</a>s
sInt8s :: [String] -> Symbolic [SInt8]

-- | Declare a list of <a>SInt16</a>s
sInt16s :: [String] -> Symbolic [SInt16]

-- | Declare a list of <a>SInt32</a>s
sInt32s :: [String] -> Symbolic [SInt32]

-- | Declare a list of <a>SInt64</a>s
sInt64s :: [String] -> Symbolic [SInt64]

-- | Declare a list of <a>SInteger</a>s
sIntegers :: [String] -> Symbolic [SInteger]

-- | Declare a list of <a>SReal</a>s
sReals :: [String] -> Symbolic [SReal]

-- | Declare a list of <a>SFloat</a>s
sFloats :: [String] -> Symbolic [SFloat]

-- | Declare a list of <a>SDouble</a>s
sDoubles :: [String] -> Symbolic [SDouble]

-- | The <a>Symbolic</a> value. Either a constant (<tt>Left</tt>) or a
--   symbolic value (<tt>Right Cached</tt>). Note that caching is essential
--   for making sure sharing is preserved. The parameter <tt>a</tt> is
--   phantom, but is extremely important in keeping the user interface
--   strongly typed.
data SBV a

-- | Flat arrays of symbolic values An <tt>array a b</tt> is an array
--   indexed by the type <tt><a>SBV</a> a</tt>, with elements of type
--   <tt><a>SBV</a> b</tt> If an initial value is not provided in
--   <a>newArray_</a> and <a>newArray</a> methods, then the elements are
--   left unspecified, i.e., the solver is free to choose any value. This
--   is the right thing to do if arrays are used as inputs to functions to
--   be verified, typically.
--   
--   While it's certainly possible for user to create instances of
--   <a>SymArray</a>, the <a>SArray</a> and <a>SFunArray</a> instances
--   already provided should cover most use cases in practice. (There are
--   some differences between these models, however, see the corresponding
--   declaration.)
--   
--   Minimal complete definition: All methods are required, no defaults.
class SymArray array
newArray_ :: (SymArray array, HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (array a b)
newArray :: (SymArray array, HasKind a, HasKind b) => String -> Maybe (SBV b) -> Symbolic (array a b)
readArray :: SymArray array => array a b -> SBV a -> SBV b
resetArray :: (SymArray array, SymWord b) => array a b -> SBV b -> array a b
writeArray :: (SymArray array, SymWord b) => array a b -> SBV a -> SBV b -> array a b
mergeArrays :: (SymArray array, SymWord b) => SBV Bool -> array a b -> array a b -> array a b

-- | Arrays implemented in terms of SMT-arrays:
--   <a>http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2</a>
--   
--   <ul>
--   <li>Maps directly to SMT-lib arrays</li>
--   <li>Reading from an unintialized value is OK and yields an
--   uninterpreted result</li>
--   <li>Can check for equality of these arrays</li>
--   <li>Cannot quick-check theorems using <tt>SArray</tt> values</li>
--   <li>Typically slower as it heavily relies on SMT-solving for the array
--   theory</li>
--   </ul>
data SArray a b

-- | Arrays implemented internally as functions
--   
--   <ul>
--   <li>Internally handled by the library and not mapped to
--   SMT-Lib<ul><li>Reading an uninitialized value is considered an error
--   (will throw exception)</li><li>Cannot check for equality (internally
--   represented as functions)</li><li>Can quick-check</li><li>Typically
--   faster as it gets compiled away during translation</li></ul></li>
--   </ul>
data SFunArray a b

-- | Lift a function to an array. Useful for creating arrays in a pure
--   context. (Otherwise use <a>newArray</a>.)
mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b

-- | A symbolic tree containing values of type e, indexed by elements of
--   type i. Note that these are full-trees, and their their shapes remain
--   constant. There is no API provided that can change the shape of the
--   tree. These structures are useful when dealing with data-structures
--   that are indexed with symbolic values where access time is important.
--   <a>STree</a> structures provide logarithmic time reads and writes.
type STree i e = STreeInternal (SBV i) (SBV e)

-- | Reading a value. We bit-blast the index and descend down the full tree
--   according to bit-values.
readSTree :: (Num i, Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e

-- | Writing a value, similar to how reads are done. The important thing is
--   that the tree representation keeps updates to a minimum.
writeSTree :: (Mergeable (SBV e), Num i, Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e -> STree i e

-- | Construct the fully balanced initial tree using the given values.
mkSTree :: HasKind i => [SBV e] -> STree i e

-- | Replacement for <a>testBit</a>. Since <a>testBit</a> requires a
--   <a>Bool</a> to be returned, we cannot implement it for symbolic words.
--   Index 0 is the least-significant bit.
sbvTestBit :: (Num a, Bits a, SymWord a) => SBV a -> Int -> SBool

-- | Replacement for <a>popCount</a>. Since <a>popCount</a> returns an
--   <a>Int</a>, we cannot implement it for symbolic words. Here, we return
--   an <a>SWord8</a>, which can overflow when used on quantities that have
--   more than 255 bits. Currently, that's only the <a>SInteger</a> type
--   that SBV supports, all other types are safe. Even with
--   <a>SInteger</a>, this will only overflow if there are at least
--   256-bits set in the number, and the smallest such number is 2^256-1,
--   which is a pretty darn big number to worry about for practical
--   purposes. In any case, we do not support <a>sbvPopCount</a> for
--   unbounded symbolic integers, as the only possible implementation
--   wouldn't symbolically terminate. So the only overflow issue is with
--   really-really large concrete <a>SInteger</a> values.
sbvPopCount :: (Num a, Bits a, SymWord a) => SBV a -> SWord8

-- | Generalization of <a>shiftL</a>, when the shift-amount is symbolic.
--   Since Haskell's <a>shiftL</a> only takes an <a>Int</a> as the shift
--   amount, it cannot be used when we have a symbolic amount to shift
--   with. The shift amount must be an unsigned quantity.
sbvShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a

-- | Generalization of <a>shiftR</a>, when the shift-amount is symbolic.
--   Since Haskell's <a>shiftR</a> only takes an <a>Int</a> as the shift
--   amount, it cannot be used when we have a symbolic amount to shift
--   with. The shift amount must be an unsigned quantity.
--   
--   NB. If the shiftee is signed, then this is an arithmetic shift;
--   otherwise it's logical, following the usual Haskell convention. See
--   <a>sbvSignedShiftArithRight</a> for a variant that explicitly uses the
--   msb as the sign bit, even for unsigned underlying types.
sbvShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a

-- | Arithmetic shift-right with a symbolic unsigned shift amount. This is
--   equivalent to <a>sbvShiftRight</a> when the argument is signed.
--   However, if the argument is unsigned, then it explicitly treats its
--   msb as a sign-bit, and uses it as the bit that gets shifted in. Useful
--   when using the underlying unsigned bit representation to implement
--   custom signed operations. Note that there is no direct Haskell
--   analogue of this function.
sbvSignedShiftArithRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a

-- | Generalization of <a>setBit</a> based on a symbolic boolean. Note that
--   <a>setBit</a> and <a>clearBit</a> are still available on Symbolic
--   words, this operation comes handy when the condition to set/clear
--   happens to be symbolic.
setBitTo :: (Num a, Bits a, SymWord a) => SBV a -> Int -> SBool -> SBV a

-- | Returns 1 if the boolean is true, otherwise 0.
oneIf :: (Num a, SymWord a) => SBool -> SBV a

-- | Least significant bit of a word, always stored at index 0.
lsb :: (Num a, Bits a, SymWord a) => SBV a -> SBool

-- | Most significant bit of a word, always stored at the last position.
msb :: (Num a, Bits a, SymWord a) => SBV a -> SBool

-- | Returns (symbolic) true if all the elements of the given list are the
--   same.
allEqual :: EqSymbolic a => [a] -> SBool

-- | Returns (symbolic) true if all the elements of the given list are
--   different.
allDifferent :: EqSymbolic a => [a] -> SBool

-- | Returns (symbolic) true if the argument is in range
inRange :: OrdSymbolic a => a -> (a, a) -> SBool

-- | Symbolic membership test
sElem :: EqSymbolic a => a -> [a] -> SBool

-- | Full adder. Returns the carry-out from the addition.
--   
--   N.B. Only works for unsigned types. Signed arguments will be rejected.
fullAdder :: SIntegral a => SBV a -> SBV a -> (SBool, SBV a)

-- | Full multiplier: Returns both the high-order and the low-order bits in
--   a tuple, thus fully accounting for the overflow.
--   
--   N.B. Only works for unsigned types. Signed arguments will be rejected.
--   
--   N.B. The higher-order bits are determined using a simple shift-add
--   multiplier, thus involving bit-blasting. It'd be naive to expect SMT
--   solvers to deal efficiently with properties involving this function,
--   at least with the current state of the art.
fullMultiplier :: SIntegral a => SBV a -> SBV a -> (SBV a, SBV a)

-- | Big-endian blasting of a word into its bits. Also see the
--   <tt>FromBits</tt> class.
blastBE :: (Num a, Bits a, SymWord a) => SBV a -> [SBool]

-- | Little-endian blasting of a word into its bits. Also see the
--   <tt>FromBits</tt> class.
blastLE :: (Num a, Bits a, SymWord a) => SBV a -> [SBool]

-- | Unblasting a value from symbolic-bits. The bits can be given
--   little-endian or big-endian. For a signed number in little-endian, we
--   assume the very last bit is the sign digit. This is a bit awkward, but
--   it is more consistent with the "reverse" view of little-big-endian
--   representations
--   
--   Minimal complete definition: <a>fromBitsLE</a>
class FromBits a where fromBitsBE = fromBitsLE . reverse
fromBitsLE, fromBitsBE :: FromBits a => [SBool] -> a

-- | Splitting an <tt>a</tt> into two <tt>b</tt>'s and joining back.
--   Intuitively, <tt>a</tt> is a larger bit-size word than <tt>b</tt>,
--   typically double. The <a>extend</a> operation captures embedding of a
--   <tt>b</tt> value into an <tt>a</tt> without changing its semantic
--   value.
--   
--   Minimal complete definition: All, no defaults.
class Splittable a b | b -> a
split :: Splittable a b => a -> (b, b)
(#) :: Splittable a b => b -> b -> a
extend :: Splittable a b => b -> a

-- | Sign casting a value into another. This essentially means forgetting
--   the sign bit and reinterpreting the bits accordingly when converting a
--   signed value to an unsigned one. Similarly, when an unsigned quantity
--   is converted to a signed one, the most significant bit is interpreted
--   as the sign. We only define instances when the source and target types
--   are precisely the same size. The idea is that <a>signCast</a> and
--   <a>unsignCast</a> must form an isomorphism pair between the types
--   <tt>a</tt> and <tt>b</tt>, i.e., we expect the following two
--   properties to hold:
--   
--   <pre>
--   signCast . unsignCast = id
--   unsingCast . signCast = id
--   </pre>
--   
--   Note that one naive way to implement both these operations is simply
--   to compute <tt>fromBitsLE . blastLE</tt>, i.e., first get all the bits
--   of the word and then reconstruct in the target type. While this is
--   semantically correct, it generates a lot of code (both during proofs
--   via SMT-Lib, and when compiled to C). The goal of this class is to
--   avoid that cost, so these operations can be compiled very efficiently,
--   they will essentially become no-op's.
--   
--   Minimal complete definition: All, no defaults.
class SignCast a b | a -> b, b -> a
signCast :: SignCast a b => a -> b
unsignCast :: SignCast a b => b -> a

-- | Implements polynomial addition, multiplication, division, and modulus
--   operations over GF(2^n). NB. Similar to <a>sQuotRem</a>, division by
--   <tt>0</tt> is interpreted as follows:
--   
--   <pre>
--   x <a>pDivMod</a> 0 = (0, x)
--   </pre>
--   
--   for all <tt>x</tt> (including <tt>0</tt>)
--   
--   Minimal complete definition: <a>pMult</a>, <a>pDivMod</a>,
--   <a>showPolynomial</a>
class (Num a, Bits a) => Polynomial a where polynomial = foldr (flip setBit) 0 pAdd = xor pDiv x y = fst (pDivMod x y) pMod x y = snd (pDivMod x y) showPoly = showPolynomial False
polynomial :: Polynomial a => [Int] -> a
pAdd :: Polynomial a => a -> a -> a
pMult :: Polynomial a => (a, a, [Int]) -> a
pDiv :: Polynomial a => a -> a -> a
pMod :: Polynomial a => a -> a -> a
pDivMod :: Polynomial a => a -> a -> (a, a)
showPoly :: Polynomial a => a -> String
showPolynomial :: Polynomial a => Bool -> a -> String

-- | Compute CRCs over bit-vectors. The call <tt>crcBV n m p</tt> computes
--   the CRC of the message <tt>m</tt> with respect to polynomial
--   <tt>p</tt>. The inputs are assumed to be blasted big-endian. The
--   number <tt>n</tt> specifies how many bits of CRC is needed. Note that
--   <tt>n</tt> is actually the degree of the polynomial <tt>p</tt>, and
--   thus it seems redundant to pass it in. However, in a typical proof
--   context, the polynomial can be symbolic, so we cannot compute the
--   degree easily. While this can be worked-around by generating code that
--   accounts for all possible degrees, the resulting code would be
--   unnecessarily big and complicated, and much harder to reason with.
--   (Also note that a CRC is just the remainder from the polynomial
--   division, but this routine is much faster in practice.)
--   
--   NB. The <tt>n</tt>th bit of the polynomial <tt>p</tt> <i>must</i> be
--   set for the CRC to be computed correctly. Note that the polynomial
--   argument <tt>p</tt> will not even have this bit present most of the
--   time, as it will typically contain bits <tt>0</tt> through
--   <tt>n-1</tt> as usual in the CRC literature. The higher order
--   <tt>n</tt>th bit is simply assumed to be set, as it does not make
--   sense to use a polynomial of a lesser degree. This is usually not a
--   problem since CRC polynomials are designed and expressed this way.
--   
--   NB. The literature on CRC's has many variants on how CRC's are
--   computed. We follow the painless guide
--   (<a>http://www.ross.net/crc/download/crc_v3.txt</a>) and compute the
--   CRC as follows:
--   
--   <ul>
--   <li>Extend the message <tt>m</tt> by adding <tt>n</tt> 0 bits on the
--   right<ul><li>Divide the polynomial thus obtained by the
--   <tt>p</tt></li><li>The remainder is the CRC value.</li></ul></li>
--   </ul>
--   
--   There are many variants on final XOR's, reversed polynomials etc., so
--   it is essential to double check you use the correct <i>algorithm</i>.
crcBV :: Int -> [SBool] -> [SBool] -> [SBool]

-- | Compute CRC's over polynomials, i.e., symbolic words. The first
--   <a>Int</a> argument plays the same role as the one in the <a>crcBV</a>
--   function.
crc :: (FromBits (SBV a), FromBits (SBV b), Num a, Num b, Bits a, Bits b, SymWord a, SymWord b) => Int -> SBV a -> SBV b -> SBV b

-- | Symbolic conditionals are modeled by the <a>Mergeable</a> class,
--   describing how to merge the results of an if-then-else call with a
--   symbolic test. SBV provides all basic types as instances of this
--   class, so users only need to declare instances for custom data-types
--   of their programs as needed.
--   
--   The function <a>select</a> is a total-indexing function out of a list
--   of choices with a default value, simulating array/list indexing. It's
--   an n-way generalization of the <a>ite</a> function.
--   
--   Minimal complete definition: <a>symbolicMerge</a>
class Mergeable a where select xs err ind | isReal ind = error "SBV.select: unsupported real valued select/index expression" | True = walk xs ind err where walk [] _ acc = acc walk (e : es) i acc = walk es (i - 1) (ite (i .== 0) e acc)
symbolicMerge :: Mergeable a => Bool -> SBool -> a -> a -> a
select :: (Mergeable a, SymWord b, Num b) => [a] -> a -> SBV b -> a

-- | If-then-else. This is by definition <a>symbolicMerge</a> with both
--   branches forced. This is typically the desired behavior, but also see
--   <a>iteLazy</a> should you need more laziness.
ite :: Mergeable a => SBool -> a -> a -> a

-- | A Lazy version of ite, which does not force its arguments. This might
--   cause issues for symbolic simulation with large thunks around, so use
--   with care.
iteLazy :: Mergeable a => SBool -> a -> a -> a

-- | Branch on a condition, much like <a>ite</a>. The exception is that SBV
--   will check to make sure if the test condition is feasible by making an
--   external call to the SMT solver. Note that this can be expensive, thus
--   we shall use a time-out value (<a>sBranchTimeOut</a>). There might be
--   zero, one, or two such external calls per <a>sBranch</a> call:
--   
--   <ul>
--   <li>If condition is statically known to be True/False: 0 calls</li>
--   <li>In this case, we simply constant fold..<ul><li>If condition is
--   determined to be unsatisfiable : 1 call</li><li>In this case, we know
--   then-branch is infeasible, so just take the else-branch</li><li>If
--   condition is determined to be satisfable : 2 calls</li><li>In this
--   case, we know then-branch is feasible, but we still have to check if
--   the else-branch is</li></ul></li>
--   </ul>
--   
--   In summary, <a>sBranch</a> calls can be expensive, but they can help
--   with the so-called symbolic-termination problem. See
--   <a>Data.SBV.Examples.Misc.SBranch</a> for an example.
sBranch :: Mergeable a => SBool -> a -> a -> a

-- | Symbolic assert. Check that the given boolean condition is always true
--   in the given path. Otherwise symbolic simulation will stop with a
--   run-time error.
sAssert :: Mergeable a => String -> SBool -> a -> a

-- | Symbolic assert with a programmable continuation. Check that the given
--   boolean condition is always true in the given path. Otherwise symbolic
--   simulation will transfer the failing model to the given continuation.
--   The continuation takes the <tt>SMTConfig</tt>, and a possible model:
--   If it receives <tt>Nothing</tt>, then it means that the condition
--   fails for all assignments to inputs. Otherwise, it'll receive
--   <tt>Just</tt> a dictionary that maps the input variables to the
--   appropriate <tt>CW</tt> values that exhibit the failure. Note that the
--   continuation has no option but to display the result in some fashion
--   and call error, due to its restricted type.
sAssertCont :: Mergeable a => String -> (forall b. SMTConfig -> Maybe (Map String CW) -> b) -> SBool -> a -> a

-- | Symbolic Equality. Note that we can't use Haskell's <a>Eq</a> class
--   since Haskell insists on returning Bool Comparing symbolic values will
--   necessarily return a symbolic value.
--   
--   Minimal complete definition: <a>.==</a>
class EqSymbolic a where x ./= y = bnot (x .== y)
(.==, ./=) :: EqSymbolic a => a -> a -> SBool

-- | Symbolic Comparisons. Similar to <a>Eq</a>, we cannot implement
--   Haskell's <a>Ord</a> class since there is no way to return an
--   <a>Ordering</a> value from a symbolic comparison. Furthermore,
--   <a>OrdSymbolic</a> requires <a>Mergeable</a> to implement
--   if-then-else, for the benefit of implementing symbolic versions of
--   <a>max</a> and <a>min</a> functions.
--   
--   Minimal complete definition: <a>.&lt;</a>
class (Mergeable a, EqSymbolic a) => OrdSymbolic a where a .<= b = a .< b ||| a .== b a .> b = b .< a a .>= b = b .<= a a `smin` b = ite (a .<= b) a b a `smax` b = ite (a .<= b) b a
(.<, .>=, .>, .<=) :: OrdSymbolic a => a -> a -> SBool
smin, smax :: OrdSymbolic a => a -> a -> a

-- | Symbolic Numbers. This is a simple class that simply incorporates all
--   number like base types together, simplifying writing polymorphic
--   type-signatures that work for all symbolic numbers, such as
--   <a>SWord8</a>, <a>SInt8</a> etc. For instance, we can write a generic
--   list-minimum function as follows:
--   
--   <pre>
--   mm :: SIntegral a =&gt; [SBV a] -&gt; SBV a
--   mm = foldr1 (a b -&gt; ite (a .&lt;= b) a b)
--   </pre>
--   
--   It is similar to the standard <a>Integral</a> class, except ranging
--   over symbolic instances.
class (SymWord a, Num a, Bits a) => SIntegral a

-- | The <a>SDivisible</a> class captures the essence of division.
--   Unfortunately we cannot use Haskell's <a>Integral</a> class since the
--   <a>Real</a> and <a>Enum</a> superclasses are not implementable for
--   symbolic bit-vectors. However, <a>quotRem</a> and <a>divMod</a> makes
--   perfect sense, and the <a>SDivisible</a> class captures this
--   operation. One issue is how division by 0 behaves. The verification
--   technology requires total functions, and there are several design
--   choices here. We follow Isabelle/HOL approach of assigning the value 0
--   for division by 0. Therefore, we impose the following law:
--   
--   <tt> x <a>sQuotRem</a> 0 = (0, x) </tt> <tt> x <a>sDivMod</a> 0 = (0,
--   x) </tt>
--   
--   Note that our instances implement this law even when <tt>x</tt> is
--   <tt>0</tt> itself.
--   
--   NB. <a>quot</a> truncates toward zero, while <a>div</a> truncates
--   toward negative infinity.
--   
--   Minimal complete definition: <a>sQuotRem</a>, <a>sDivMod</a>
class SDivisible a where x `sQuot` y = fst $ x `sQuotRem` y x `sRem` y = snd $ x `sQuotRem` y x `sDiv` y = fst $ x `sDivMod` y x `sMod` y = snd $ x `sDivMod` y
sQuotRem :: SDivisible a => a -> a -> (a, a)
sDivMod :: SDivisible a => a -> a -> (a, a)
sQuot :: SDivisible a => a -> a -> a
sRem :: SDivisible a => a -> a -> a
sDiv :: SDivisible a => a -> a -> a
sMod :: SDivisible a => a -> a -> a

-- | The <a>Boolean</a> class: a generalization of Haskell's <a>Bool</a>
--   type Haskell <a>Bool</a> and SBV's <tt>SBool</tt> are instances of
--   this class, unifying the treatment of boolean values.
--   
--   Minimal complete definition: <a>true</a>, <a>bnot</a>,
--   <a>&amp;&amp;&amp;</a> However, it's advisable to define <a>false</a>,
--   and <a>|||</a> as well (typically), for clarity.
class Boolean b where false = bnot true a ||| b = bnot (bnot a &&& bnot b) a ~& b = bnot (a &&& b) a ~| b = bnot (a ||| b) a <+> b = (a &&& bnot b) ||| (bnot a &&& b) a <=> b = (a &&& b) ||| (bnot a &&& bnot b) a ==> b = bnot a ||| b fromBool True = true fromBool False = false
true :: Boolean b => b
false :: Boolean b => b
bnot :: Boolean b => b -> b
(&&&) :: Boolean b => b -> b -> b
(|||) :: Boolean b => b -> b -> b
(~&) :: Boolean b => b -> b -> b
(~|) :: Boolean b => b -> b -> b
(<+>) :: Boolean b => b -> b -> b
(==>) :: Boolean b => b -> b -> b
(<=>) :: Boolean b => b -> b -> b
fromBool :: Boolean b => Bool -> b

-- | Generalization of <a>and</a>
bAnd :: Boolean b => [b] -> b

-- | Generalization of <a>or</a>
bOr :: Boolean b => [b] -> b

-- | Generalization of <a>any</a>
bAny :: Boolean b => (a -> b) -> [a] -> b

-- | Generalization of <a>all</a>
bAll :: Boolean b => (a -> b) -> [a] -> b

-- | PrettyNum class captures printing of numbers in hex and binary
--   formats; also supporting negative numbers.
--   
--   Minimal complete definition: <a>hexS</a> and <a>binS</a>
class PrettyNum a
hexS :: PrettyNum a => a -> String
binS :: PrettyNum a => a -> String
hex :: PrettyNum a => a -> String
bin :: PrettyNum a => a -> String

-- | A more convenient interface for reading binary numbers, also supports
--   negative numbers
readBin :: Num a => String -> a

-- | Uninterpreted constants and functions. An uninterpreted constant is a
--   value that is indexed by its name. The only property the prover
--   assumes about these values are that they are equivalent to themselves;
--   i.e., (for functions) they return the same results when applied to
--   same arguments. We support uninterpreted-functions as a general means
--   of black-box'ing operations that are <i>irrelevant</i> for the
--   purposes of the proof; i.e., when the proofs can be performed without
--   any knowledge about the function itself.
--   
--   Minimal complete definition: <a>sbvUninterpret</a>. However, most
--   instances in practice are already provided by SBV, so end-users should
--   not need to define their own instances.
class Uninterpreted a where uninterpret = sbvUninterpret Nothing cgUninterpret nm code v = sbvUninterpret (Just (code, v)) nm
uninterpret :: Uninterpreted a => String -> a
cgUninterpret :: Uninterpreted a => String -> [String] -> a -> a
sbvUninterpret :: Uninterpreted a => Maybe ([String], a) -> String -> a

-- | Add a user specified axiom to the generated SMT-Lib file. The first
--   argument is a mere string, use for commenting purposes. The second
--   argument is intended to hold the multiple-lines of the axiom text as
--   expressed in SMT-Lib notation. Note that we perform no checks on the
--   axiom itself, to see whether it's actually well-formed or is sensical
--   by any means. A separate formalization of SMT-Lib would be very useful
--   here.
addAxiom :: String -> [String] -> Symbolic ()

-- | A predicate is a symbolic program that returns a (symbolic) boolean
--   value. For all intents and purposes, it can be treated as an n-ary
--   function from symbolic-values to a boolean. The <a>Symbolic</a> monad
--   captures the underlying representation, and can/should be ignored by
--   the users of the library, unless you are building further utilities on
--   top of SBV itself. Instead, simply use the <a>Predicate</a> type when
--   necessary.
type Predicate = Symbolic SBool

-- | A type <tt>a</tt> is provable if we can turn it into a predicate. Note
--   that a predicate can be made from a curried function of arbitrary
--   arity, where each element is either a symbolic type or up-to a 7-tuple
--   of symbolic-types. So predicates can be constructed from almost
--   arbitrary Haskell functions that have arbitrary shapes. (See the
--   instance declarations below.)
class Provable a
forAll_ :: Provable a => a -> Predicate
forAll :: Provable a => [String] -> a -> Predicate
forSome_ :: Provable a => a -> Predicate
forSome :: Provable a => [String] -> a -> Predicate

-- | Equality as a proof method. Allows for very concise construction of
--   equivalence proofs, which is very typical in bit-precise proofs.
class Equality a
(===) :: Equality a => a -> a -> IO ThmResult

-- | Prove a predicate, equivalent to <tt><a>proveWith</a>
--   <a>defaultSMTCfg</a></tt>
prove :: Provable a => a -> IO ThmResult

-- | Proves the predicate using the given SMT-solver
proveWith :: Provable a => SMTConfig -> a -> IO ThmResult

-- | Checks theoremhood within the given optional time limit of <tt>i</tt>
--   seconds. Returns <tt>Nothing</tt> if times out, or the result wrapped
--   in a <tt>Just</tt> otherwise.
isTheorem :: Provable a => Maybe Int -> a -> IO (Maybe Bool)

-- | Check whether a given property is a theorem, with an optional time out
--   and the given solver. Returns <tt>Nothing</tt> if times out, or the
--   result wrapped in a <tt>Just</tt> otherwise.
isTheoremWith :: Provable a => SMTConfig -> Maybe Int -> a -> IO (Maybe Bool)

-- | Find a satisfying assignment for a predicate, equivalent to
--   <tt><a>satWith</a> <a>defaultSMTCfg</a></tt>
sat :: Provable a => a -> IO SatResult

-- | Find a satisfying assignment using the given SMT-solver
satWith :: Provable a => SMTConfig -> a -> IO SatResult

-- | Checks satisfiability within the given optional time limit of
--   <tt>i</tt> seconds. Returns <tt>Nothing</tt> if times out, or the
--   result wrapped in a <tt>Just</tt> otherwise.
isSatisfiable :: Provable a => Maybe Int -> a -> IO (Maybe Bool)

-- | Check whether a given property is satisfiable, with an optional time
--   out and the given solver. Returns <tt>Nothing</tt> if times out, or
--   the result wrapped in a <tt>Just</tt> otherwise.
isSatisfiableWith :: Provable a => SMTConfig -> Maybe Int -> a -> IO (Maybe Bool)

-- | Return all satisfying assignments for a predicate, equivalent to
--   <tt><a>allSatWith</a> <a>defaultSMTCfg</a></tt>. Satisfying
--   assignments are constructed lazily, so they will be available as
--   returned by the solver and on demand.
--   
--   NB. Uninterpreted constant/function values and counter-examples for
--   array values are ignored for the purposes of <tt><a>allSat</a></tt>.
--   That is, only the satisfying assignments modulo uninterpreted
--   functions and array inputs will be returned. This is due to the
--   limitation of not having a robust means of getting a function
--   counter-example back from the SMT solver.
allSat :: Provable a => a -> IO AllSatResult

-- | Find all satisfying assignments using the given SMT-solver
allSatWith :: Provable a => SMTConfig -> a -> IO AllSatResult

-- | Form the symbolic conjunction of a given list of boolean conditions.
--   Useful in expressing problems with constraints, like the following:
--   
--   <pre>
--   do [x, y, z] &lt;- sIntegers ["x", "y", "z"]
--      solve [x .&gt; 5, y + z .&lt; x]
--   </pre>
solve :: [SBool] -> Symbolic SBool

-- | Adding arbitrary constraints. When adding constraints, one has to be
--   careful about making sure they are not inconsistent. The function
--   <a>isVacuous</a> can be use for this purpose. Here is an example.
--   Consider the following predicate:
--   
--   <pre>
--   &gt;&gt;&gt; let pred = do { x &lt;- forall "x"; constrain $ x .&lt; x; return $ x .&gt;= (5 :: SWord8) }
--   </pre>
--   
--   This predicate asserts that all 8-bit values are larger than 5,
--   subject to the constraint that the values considered satisfy <tt>x
--   .&lt; x</tt>, i.e., they are less than themselves. Since there are no
--   values that satisfy this constraint, the proof will pass vacuously:
--   
--   <pre>
--   &gt;&gt;&gt; prove pred
--   Q.E.D.
--   </pre>
--   
--   We can use <a>isVacuous</a> to make sure to see that the pass was
--   vacuous:
--   
--   <pre>
--   &gt;&gt;&gt; isVacuous pred
--   True
--   </pre>
--   
--   While the above example is trivial, things can get complicated if
--   there are multiple constraints with non-straightforward relations; so
--   if constraints are used one should make sure to check the predicate is
--   not vacuously true. Here's an example that is not vacuous:
--   
--   <pre>
--   &gt;&gt;&gt; let pred' = do { x &lt;- forall "x"; constrain $ x .&gt; 6; return $ x .&gt;= (5 :: SWord8) }
--   </pre>
--   
--   This time the proof passes as expected:
--   
--   <pre>
--   &gt;&gt;&gt; prove pred'
--   Q.E.D.
--   </pre>
--   
--   And the proof is not vacuous:
--   
--   <pre>
--   &gt;&gt;&gt; isVacuous pred'
--   False
--   </pre>
constrain :: SBool -> Symbolic ()

-- | Adding a probabilistic constraint. The <a>Double</a> argument is the
--   probability threshold. Probabilistic constraints are useful for
--   <tt>genTest</tt> and <tt>quickCheck</tt> calls where we restrict our
--   attention to <i>interesting</i> parts of the input domain.
pConstrain :: Double -> SBool -> Symbolic ()

-- | Check if the given constraints are satisfiable, equivalent to
--   <tt><a>isVacuousWith</a> <a>defaultSMTCfg</a></tt>. See the function
--   <tt>constrain</tt> for an example use of <a>isVacuous</a>.
isVacuous :: Provable a => a -> IO Bool

-- | Determine if the constraints are vacuous using the given SMT-solver
isVacuousWith :: Provable a => SMTConfig -> a -> IO Bool

-- | Prove a property with multiple solvers, running them in separate
--   threads. The results will be returned in the order produced.
proveWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, ThmResult)]

-- | Prove a property with multiple solvers, running them in separate
--   threads. Only the result of the first one to finish will be returned,
--   remaining threads will be killed.
proveWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, ThmResult)

-- | Find a satisfying assignment to a property with multiple solvers,
--   running them in separate threads. The results will be returned in the
--   order produced.
satWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, SatResult)]

-- | Find a satisfying assignment to a property with multiple solvers,
--   running them in separate threads. Only the result of the first one to
--   finish will be returned, remaining threads will be killed.
satWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, SatResult)

-- | Find all satisfying assignments to a property with multiple solvers,
--   running them in separate threads. Only the result of the first one to
--   finish will be returned, remaining threads will be killed.
allSatWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, AllSatResult)]

-- | Find all satisfying assignments to a property with multiple solvers,
--   running them in separate threads. Only the result of the first one to
--   finish will be returned, remaining threads will be killed.
allSatWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, AllSatResult)

-- | Minimizes a cost function with respect to a constraint. Examples:
--   
--   <pre>
--   &gt;&gt;&gt; minimize Quantified sum 3 (bAll (.&gt; (10 :: SInteger)))
--   Just [11,11,11]
--   </pre>
minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])

-- | Maximizes a cost function with respect to a constraint. Examples:
--   
--   <pre>
--   &gt;&gt;&gt; maximize Quantified sum 3 (bAll (.&lt; (10 :: SInteger)))
--   Just [9,9,9]
--   </pre>
maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])

-- | Variant of <a>optimizeWith</a> using the default solver. See
--   <a>optimizeWith</a> for parameter descriptions.
optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])

-- | Variant of <a>minimize</a> allowing the use of a user specified
--   solver. See <a>optimizeWith</a> for parameter descriptions.
minimizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])

-- | Variant of <a>maximize</a> allowing the use of a user specified
--   solver. See <a>optimizeWith</a> for parameter descriptions.
maximizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])

-- | Symbolic optimization. Generalization on <a>minimize</a> and
--   <a>maximize</a> that allows arbitrary cost functions and comparisons.
optimizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])

-- | Given a symbolic computation that produces a value, compute the
--   expected value that value would take if this computation is run with
--   its free variables drawn from uniform distributions of its respective
--   values, satisfying the given constraints specified by
--   <tt>constrain</tt> and <tt>pConstrain</tt> calls. This is equivalent
--   to calling <a>expectedValueWith</a> the following parameters: verbose,
--   warm-up round count of <tt>10000</tt>, no maximum iteration count, and
--   with convergence margin <tt>0.0001</tt>.
expectedValue :: Outputtable a => Symbolic a -> IO [Double]

-- | Generalized version of <a>expectedValue</a>, allowing the user to
--   specify the warm-up count and the convergence factor. Maximum
--   iteration count can also be specified, at which point convergence
--   won't be sought. The boolean controls verbosity.
expectedValueWith :: Outputtable a => Bool -> Int -> Maybe Int -> Double -> Symbolic a -> IO [Double]

-- | A <tt>prove</tt> call results in a <a>ThmResult</a>
newtype ThmResult
ThmResult :: SMTResult -> ThmResult

-- | A <tt>sat</tt> call results in a <a>SatResult</a> The reason for
--   having a separate <a>SatResult</a> is to have a more meaningful
--   <a>Show</a> instance.
newtype SatResult
SatResult :: SMTResult -> SatResult

-- | An <tt>allSat</tt> call results in a <a>AllSatResult</a>. The boolean
--   says whether we should warn the user about prefix-existentials.
newtype AllSatResult
AllSatResult :: (Bool, [SMTResult]) -> AllSatResult

-- | The result of an SMT solver call. Each constructor is tagged with the
--   <a>SMTConfig</a> that created it so that further tools can inspect it
--   and build layers of results, if needed. For ordinary uses of the
--   library, this type should not be needed, instead use the accessor
--   functions on it. (Custom Show instances and model extractors.)
data SMTResult

-- | Unsatisfiable
Unsatisfiable :: SMTConfig -> SMTResult

-- | Satisfiable with model
Satisfiable :: SMTConfig -> SMTModel -> SMTResult

-- | Prover returned unknown, with a potential (possibly bogus) model
Unknown :: SMTConfig -> SMTModel -> SMTResult

-- | Prover errored out
ProofError :: SMTConfig -> [String] -> SMTResult

-- | Computation timed out (see the <tt>timeout</tt> combinator)
TimeOut :: SMTConfig -> SMTResult

-- | Instances of <a>SatModel</a> can be automatically extracted from
--   models returned by the solvers. The idea is that the sbv
--   infrastructure provides a stream of <tt>CW'</tt>s (constant-words)
--   coming from the solver, and the type <tt>a</tt> is interpreted based
--   on these constants. Many typical instances are already provided, so
--   new instances can be declared with relative ease.
--   
--   Minimum complete definition: <a>parseCWs</a>
class SatModel a where cvtModel f x = x >>= \ (a, r) -> f a >>= \ b -> return (b, r)
parseCWs :: SatModel a => [CW] -> Maybe (a, [CW])
cvtModel :: SatModel a => (a -> Maybe b) -> Maybe (a, [CW]) -> Maybe (b, [CW])

-- | Various SMT results that we can extract models out of.
class Modelable a where getModelValue v r = fromCW `fmap` (v `lookup` getModelDictionary r) getModelUninterpretedValue v r = case v `lookup` getModelDictionary r of { Just (CW _ (CWUninterpreted s)) -> Just s _ -> Nothing } extractModel a = case getModel a of { Right (_, b) -> Just b _ -> Nothing }
modelExists :: Modelable a => a -> Bool
getModel :: (Modelable a, SatModel b) => a -> Either String (Bool, b)
getModelDictionary :: Modelable a => a -> Map String CW
getModelValue :: (Modelable a, SymWord b) => String -> a -> Maybe b
getModelUninterpretedValue :: Modelable a => String -> a -> Maybe String
extractModel :: (Modelable a, SatModel b) => a -> Maybe b

-- | Given an <tt>allSat</tt> call, we typically want to iterate over it
--   and print the results in sequence. The <a>displayModels</a> function
--   automates this task by calling <tt>disp</tt> on each result,
--   consecutively. The first <a>Int</a> argument to <tt>disp</tt> 'is the
--   current model number. The second argument is a tuple, where the first
--   element indicates whether the model is alleged (i.e., if the solver is
--   not sure, returing Unknown)
displayModels :: SatModel a => (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int

-- | Return all the models from an <tt>allSat</tt> call, similar to
--   <a>extractModel</a> but is suitable for the case of multiple results.
extractModels :: SatModel a => AllSatResult -> [a]

-- | Get dictionaries from an all-sat call. Similar to
--   <a>getModelDictionary</a>.
getModelDictionaries :: AllSatResult -> [Map String CW]

-- | Extract value of a variable from an all-sat call. Similar to
--   <a>getModelValue</a>.
getModelValues :: SymWord b => String -> AllSatResult -> [Maybe b]

-- | Extract value of an uninterpreted variable from an all-sat call.
--   Similar to <a>getModelUninterpretedValue</a>.
getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String]

-- | Solver configuration. See also <tt>z3</tt>, <tt>yices</tt>,
--   <tt>cvc4</tt>, <tt>boolector</tt>, <tt>mathSAT</tt>, etc. which are
--   instantiations of this type for those solvers, with reasonable
--   defaults. In particular, custom configuration can be created by
--   varying those values. (Such as <tt>z3{verbose=True}</tt>.)
--   
--   Most fields are self explanatory. The notion of precision for printing
--   algebraic reals stems from the fact that such values does not
--   necessarily have finite decimal representations, and hence we have to
--   stop printing at some depth. It is important to emphasize that such
--   values always have infinite precision internally. The issue is merely
--   with how we print such an infinite precision value on the screen. The
--   field <a>printRealPrec</a> controls the printing precision, by
--   specifying the number of digits after the decimal point. The default
--   value is 16, but it can be set to any positive integer.
--   
--   When printing, SBV will add the suffix <tt>...</tt> at the and of a
--   real-value, if the given bound is not sufficient to represent the
--   real-value exactly. Otherwise, the number will be written out in
--   standard decimal notation. Note that SBV will always print the whole
--   value if it is precise (i.e., if it fits in a finite number of
--   digits), regardless of the precision limit. The limit only applies if
--   the representation of the real value is not finite, i.e., if it is not
--   rational.
data SMTConfig
SMTConfig :: Bool -> Bool -> Maybe Int -> Maybe Int -> Int -> Int -> [String] -> String -> Maybe FilePath -> Bool -> SMTSolver -> RoundingMode -> Maybe Logic -> SMTConfig

-- | Debug mode
verbose :: SMTConfig -> Bool

-- | Print timing information on how long different phases took
--   (construction, solving, etc.)
timing :: SMTConfig -> Bool

-- | How much time to give to the solver for each call of <tt>sBranch</tt>
--   check. (In seconds. Default: No limit.)
sBranchTimeOut :: SMTConfig -> Maybe Int

-- | How much time to give to the solver. (In seconds. Default: No limit.)
timeOut :: SMTConfig -> Maybe Int

-- | Print integral literals in this base (2, 8, 10, and 16 are supported.)
printBase :: SMTConfig -> Int

-- | Print algebraic real values with this precision. (SReal, default: 16)
printRealPrec :: SMTConfig -> Int

-- | Additional lines of script to give to the solver (user specified)
solverTweaks :: SMTConfig -> [String]

-- | Usually "(check-sat)". However, users might tweak it based on solver
--   characteristics.
satCmd :: SMTConfig -> String

-- | If Just, the generated SMT script will be put in this file (for
--   debugging purposes mostly)
smtFile :: SMTConfig -> Maybe FilePath

-- | If True, we'll treat the solver as using SMTLib2 input format.
--   Otherwise, SMTLib1
useSMTLib2 :: SMTConfig -> Bool

-- | The actual SMT solver.
solver :: SMTConfig -> SMTSolver

-- | Rounding mode to use for floating-point conversions
roundingMode :: SMTConfig -> RoundingMode

-- | If Nothing, pick automatically. Otherwise, either use the given one,
--   or use the custom string.
useLogic :: SMTConfig -> Maybe Logic

-- | SMT-Lib logics. If left unspecified SBV will pick the logic based on
--   what it determines is needed. However, the user can override this
--   choice using the <a>useLogic</a> parameter to the configuration. This
--   is especially handy if one is experimenting with custom logics that
--   might be supported on new solvers.
data SMTLibLogic

-- | Formulas over the theory of linear integer arithmetic and arrays
--   extended with free sort and function symbols but restricted to arrays
--   with integer indices and values
AUFLIA :: SMTLibLogic

-- | Linear formulas with free sort and function symbols over one- and
--   two-dimentional arrays of integer index and real value
AUFLIRA :: SMTLibLogic

-- | Formulas with free function and predicate symbols over a theory of
--   arrays of arrays of integer index and real value
AUFNIRA :: SMTLibLogic

-- | Linear formulas in linear real arithmetic
LRA :: SMTLibLogic

-- | Linear real arithmetic with uninterpreted sort and function symbols.
UFLRA :: SMTLibLogic

-- | Non-linear integer arithmetic with uninterpreted sort and function
--   symbols.
UFNIA :: SMTLibLogic

-- | Quantifier-free formulas over the theory of bitvectors and bitvector
--   arrays
QF_ABV :: SMTLibLogic

-- | Quantifier-free formulas over the theory of bitvectors and bitvector
--   arrays extended with free sort and function symbols
QF_AUFBV :: SMTLibLogic

-- | Quantifier-free linear formulas over the theory of integer arrays
--   extended with free sort and function symbols
QF_AUFLIA :: SMTLibLogic

-- | Quantifier-free formulas over the theory of arrays with extensionality
QF_AX :: SMTLibLogic

-- | Quantifier-free formulas over the theory of fixed-size bitvectors
QF_BV :: SMTLibLogic

-- | Difference Logic over the integers. Boolean combinations of
--   inequations of the form x - y &lt; b where x and y are integer
--   variables and b is an integer constant
QF_IDL :: SMTLibLogic

-- | Unquantified linear integer arithmetic. In essence, Boolean
--   combinations of inequations between linear polynomials over integer
--   variables
QF_LIA :: SMTLibLogic

-- | Unquantified linear real arithmetic. In essence, Boolean combinations
--   of inequations between linear polynomials over real variables.
QF_LRA :: SMTLibLogic

-- | Quantifier-free integer arithmetic.
QF_NIA :: SMTLibLogic

-- | Quantifier-free real arithmetic.
QF_NRA :: SMTLibLogic

-- | Difference Logic over the reals. In essence, Boolean combinations of
--   inequations of the form x - y &lt; b where x and y are real variables
--   and b is a rational constant.
QF_RDL :: SMTLibLogic

-- | Unquantified formulas built over a signature of uninterpreted (i.e.,
--   free) sort and function symbols.
QF_UF :: SMTLibLogic

-- | Unquantified formulas over bitvectors with uninterpreted sort function
--   and symbols.
QF_UFBV :: SMTLibLogic

-- | Difference Logic over the integers (in essence) but with uninterpreted
--   sort and function symbols.
QF_UFIDL :: SMTLibLogic

-- | Unquantified linear integer arithmetic with uninterpreted sort and
--   function symbols.
QF_UFLIA :: SMTLibLogic

-- | Unquantified linear real arithmetic with uninterpreted sort and
--   function symbols.
QF_UFLRA :: SMTLibLogic

-- | Unquantified non-linear real arithmetic with uninterpreted sort and
--   function symbols.
QF_UFNRA :: SMTLibLogic

-- | Quantifier-free formulas over the theory of floating point numbers,
--   arrays, and bit-vectors
QF_FPABV :: SMTLibLogic

-- | Quantifier-free formulas over the theory of floating point numbers
QF_FPA :: SMTLibLogic

-- | Chosen logic for the solver
data Logic

-- | Use one of the logics as defined by the standard
PredefinedLogic :: SMTLibLogic -> Logic

-- | Use this name for the logic
CustomLogic :: String -> Logic

-- | Optimizer configuration. Note that iterative and quantified approaches
--   are in general not interchangeable. For instance, iterative solutions
--   will loop infinitely when there is no optimal value, but quantified
--   solutions can handle such problems. Of course, quantified problems are
--   harder for SMT solvers, naturally.
data OptimizeOpts

-- | Iteratively search. if True, it will be reporting progress
Iterative :: Bool -> OptimizeOpts

-- | Use quantifiers
Quantified :: OptimizeOpts

-- | Solvers that SBV is aware of
data Solver
Z3 :: Solver
Yices :: Solver
Boolector :: Solver
CVC4 :: Solver
MathSAT :: Solver

-- | An SMT solver
data SMTSolver
SMTSolver :: Solver -> String -> [String] -> SMTEngine -> (ExitCode -> ExitCode) -> SolverCapabilities -> SMTSolver

-- | The solver in use
name :: SMTSolver -> Solver

-- | The path to its executable
executable :: SMTSolver -> String

-- | Options to provide to the solver
options :: SMTSolver -> [String]

-- | The solver engine, responsible for interpreting solver output
engine :: SMTSolver -> SMTEngine

-- | Should we re-interpret exit codes. Most solvers behave rationally,
--   i.e., id will do. Some (like CVC4) don't.
xformExitCode :: SMTSolver -> ExitCode -> ExitCode

-- | Various capabilities of the solver
capabilities :: SMTSolver -> SolverCapabilities

-- | Default configuration for the Boolector SMT solver
boolector :: SMTConfig

-- | Default configuration for the CVC4 SMT Solver.
cvc4 :: SMTConfig

-- | Default configuration for the Yices SMT Solver.
yices :: SMTConfig

-- | Default configuration for the Z3 SMT solver
z3 :: SMTConfig

-- | Default configuration for the MathSAT SMT solver
mathSAT :: SMTConfig

-- | The default configs corresponding to supported SMT solvers
defaultSolverConfig :: Solver -> SMTConfig

-- | The currently active solver, obtained by importing <a>Data.SBV</a>. To
--   have other solvers <i>current</i>, import one of the bridge modules
--   <a>Data.SBV.Bridge.CVC4</a>, <a>Data.SBV.Bridge.Yices</a>, or
--   <a>Data.SBV.Bridge.Z3</a> directly.
sbvCurrentSolver :: SMTConfig

-- | The default solver used by SBV. This is currently set to z3.
defaultSMTCfg :: SMTConfig

-- | Check whether the given solver is installed and is ready to go. This
--   call does a simple call to the solver to ensure all is well.
sbvCheckSolverInstallation :: SMTConfig -> IO Bool

-- | Return the known available solver configs, installed on your machine.
sbvAvailableSolvers :: IO [SMTConfig]

-- | A Symbolic computation. Represented by a reader monad carrying the
--   state of the computation, layered on top of IO for creating unique
--   references to hold onto intermediate results.
data Symbolic a

-- | Mark an interim result as an output. Useful when constructing Symbolic
--   programs that return multiple values, or when the result is
--   programmatically computed.
output :: Outputtable a => a -> Symbolic a

-- | A <a>SymWord</a> is a potential symbolic bitvector that can be created
--   instances of to be fed to a symbolic program. Note that these methods
--   are typically not needed in casual uses with <tt>prove</tt>,
--   <tt>sat</tt>, <tt>allSat</tt> etc, as default instances automatically
--   provide the necessary bits.
class (HasKind a, Ord a) => SymWord a where forall = mkSymWord (Just ALL) . Just forall_ = mkSymWord (Just ALL) Nothing exists = mkSymWord (Just EX) . Just exists_ = mkSymWord (Just EX) Nothing free = mkSymWord Nothing . Just free_ = mkSymWord Nothing Nothing mkForallVars n = mapM (const forall_) [1 .. n] mkExistVars n = mapM (const exists_) [1 .. n] mkFreeVars n = mapM (const free_) [1 .. n] symbolic = free symbolics = mapM symbolic unliteral (SBV _ (Left c)) = Just $ fromCW c unliteral _ = Nothing isConcrete (SBV _ (Left _)) = True isConcrete _ = False isSymbolic = not . isConcrete isConcretely s p | Just i <- unliteral s = p i | True = False mbMaxBound = Nothing mbMinBound = Nothing literal x = error $ "Cannot create symbolic literals for kind: " ++ show (kindOf x) fromCW cw = error $ "Cannot convert CW " ++ show cw ++ " to kind " ++ show (kindOf (undefined :: a)) mkSymWord mbQ mbNm = do { let sortName = tyconUQname . dataTypeName . dataTypeOf $ (undefined :: a); st <- ask; let k = KUninterpreted sortName; liftIO $ registerKind st k; let q = case (mbQ, runMode st) of { (Just x, _) -> x (Nothing, Proof (True, _)) -> EX (Nothing, Proof (False, _)) -> ALL (Nothing, Concrete {}) -> error $ "SBV: Uninterpreted sort " ++ sortName ++ " can not be used in concrete simulation mode." (Nothing, CodeGen) -> error $ "SBV: Uninterpreted sort " ++ sortName ++ " can not be used in code-generation mode." }; ctr <- liftIO $ incCtr st; let sw = SW k (NodeId ctr) nm = maybe ('s' : show ctr) id mbNm; liftIO $ modifyIORef (rinps st) ((q, (sw, nm)) :); return $ SBV k $ Right $ cache (const (return sw)) }
forall :: SymWord a => String -> Symbolic (SBV a)
forall_ :: SymWord a => Symbolic (SBV a)
mkForallVars :: SymWord a => Int -> Symbolic [SBV a]
exists :: SymWord a => String -> Symbolic (SBV a)
exists_ :: SymWord a => Symbolic (SBV a)
mkExistVars :: SymWord a => Int -> Symbolic [SBV a]
free :: SymWord a => String -> Symbolic (SBV a)
free_ :: SymWord a => Symbolic (SBV a)
mkFreeVars :: SymWord a => Int -> Symbolic [SBV a]
symbolic :: SymWord a => String -> Symbolic (SBV a)
symbolics :: SymWord a => [String] -> Symbolic [SBV a]
literal :: SymWord a => a -> SBV a
unliteral :: SymWord a => SBV a -> Maybe a
fromCW :: SymWord a => CW -> a
isConcrete :: SymWord a => SBV a -> Bool
isSymbolic :: SymWord a => SBV a -> Bool
isConcretely :: SymWord a => SBV a -> (a -> Bool) -> Bool
mbMaxBound, mbMinBound :: SymWord a => Maybe a
mkSymWord :: SymWord a => Maybe Quantifier -> Maybe String -> Symbolic (SBV a)

-- | Compiles to SMT-Lib and returns the resulting program as a string.
--   Useful for saving the result to a file for off-line analysis, for
--   instance if you have an SMT solver that's not natively supported
--   out-of-the box by the SBV library. It takes two booleans:
--   
--   <ul>
--   <li>smtLib2: If <a>True</a>, will generate SMT-Lib2 output, otherwise
--   SMT-Lib1 output<ul><li>isSat : If <a>True</a>, will translate it as a
--   SAT query, i.e., in the positive. If <a>False</a>, will translate as a
--   PROVE query, i.e., it will negate the result. (In this case, the
--   check-sat call to the SMT solver will produce UNSAT if the input is a
--   theorem, as usual.)</li></ul></li>
--   </ul>
compileToSMTLib :: Provable a => Bool -> Bool -> a -> IO String

-- | Create both SMT-Lib1 and SMT-Lib2 benchmarks. The first argument is
--   the basename of the file, SMT-Lib1 version will be written with suffix
--   ".smt1" and SMT-Lib2 version will be written with suffix ".smt2". The
--   <a>Bool</a> argument controls whether this is a SAT instance, i.e.,
--   translate the query directly, or a PROVE instance, i.e., translate the
--   negated query. (See the second boolean argument to
--   <a>compileToSMTLib</a> for details.)
generateSMTBenchmarks :: Provable a => Bool -> FilePath -> a -> IO ()

-- | Generate a set of concrete test values from a symbolic program. The
--   output can be rendered as test vectors in different languages as
--   necessary. Use the function <a>output</a> call to indicate what fields
--   should be in the test result. (Also see <tt>constrain</tt> and
--   <tt>pConstrain</tt> for filtering acceptable test values.)
genTest :: Outputtable a => Int -> Symbolic a -> IO TestVectors

-- | Retrieve the test vectors for further processing. This function is
--   useful in cases where <a>renderTest</a> is not sufficient and custom
--   output (or further preprocessing) is needed.
getTestValues :: TestVectors -> [([CW], [CW])]

-- | Type of test vectors (abstract)
data TestVectors

-- | Test output style
data TestStyle

-- | As a Haskell value with given name
Haskell :: String -> TestStyle

-- | As a C array of structs with given name
C :: String -> TestStyle

-- | As a Forte/Verilog value with given name. If the boolean is True then
--   vectors are blasted big-endian, otherwise little-endian The indices
--   are the split points on bit-vectors for input and output values
Forte :: String -> Bool -> ([Int], [Int]) -> TestStyle

-- | Render the test as a Haskell value with the given name <tt>n</tt>.
renderTest :: TestStyle -> TestVectors -> String

-- | <a>CW</a> represents a concrete word of a fixed size: Endianness is
--   mostly irrelevant (see the <tt>FromBits</tt> class). For signed words,
--   the most significant digit is considered to be the sign.
data CW
CW :: !Kind -> !CWVal -> CW
cwKind :: CW -> !Kind
cwVal :: CW -> !CWVal

-- | A class for capturing values that have a sign and a size (finite or
--   infinite) minimal complete definition: kindOf. This class can be
--   automatically derived for data-types that have a <a>Data</a> instance;
--   this is useful for creating uninterpreted sorts.
class HasKind a where hasSign x = case kindOf x of { KBool -> False KBounded b _ -> b KUnbounded -> True KReal -> True KFloat -> True KDouble -> True KUninterpreted {} -> False } intSizeOf x = case kindOf x of { KBool -> error "SBV.HasKind.intSizeOf((S)Bool)" KBounded _ s -> s KUnbounded -> error "SBV.HasKind.intSizeOf((S)Integer)" KReal -> error "SBV.HasKind.intSizeOf((S)Real)" KFloat -> error "SBV.HasKind.intSizeOf((S)Float)" KDouble -> error "SBV.HasKind.intSizeOf((S)Double)" KUninterpreted s -> error $ "SBV.HasKind.intSizeOf: Uninterpreted sort: " ++ s } isBoolean x | KBool {} <- kindOf x = True | True = False isBounded x | KBounded {} <- kindOf x = True | True = False isReal x | KReal {} <- kindOf x = True | True = False isFloat x | KFloat {} <- kindOf x = True | True = False isDouble x | KDouble {} <- kindOf x = True | True = False isInteger x | KUnbounded {} <- kindOf x = True | True = False isUninterpreted x | KUninterpreted {} <- kindOf x = True | True = False showType = show . kindOf kindOf = KUninterpreted . tyconUQname . dataTypeName . dataTypeOf
kindOf :: HasKind a => a -> Kind
hasSign :: HasKind a => a -> Bool
intSizeOf :: HasKind a => a -> Int
isBoolean :: HasKind a => a -> Bool
isBounded :: HasKind a => a -> Bool
isReal :: HasKind a => a -> Bool
isFloat :: HasKind a => a -> Bool
isDouble :: HasKind a => a -> Bool
isInteger :: HasKind a => a -> Bool
isUninterpreted :: HasKind a => a -> Bool
showType :: HasKind a => a -> String

-- | Kind of symbolic value
data Kind
KBool :: Kind
KBounded :: Bool -> Int -> Kind
KUnbounded :: Kind
KReal :: Kind
KUninterpreted :: String -> Kind
KFloat :: Kind
KDouble :: Kind

-- | Convert a CW to a Haskell boolean (NB. Assumes input is well-kinded)
cwToBool :: CW -> Bool

-- | The code-generation monad. Allows for precise layout of input values
--   reference parameters (for returning composite values in languages such
--   as C), and return values.
data SBVCodeGen a

-- | Sets RTC (run-time-checks) for index-out-of-bounds, shift-with-large
--   value etc. on/off. Default: <a>False</a>.
cgPerformRTCs :: Bool -> SBVCodeGen ()

-- | Sets driver program run time values, useful for generating programs
--   with fixed drivers for testing. Default: None, i.e., use random
--   values.
cgSetDriverValues :: [Integer] -> SBVCodeGen ()

-- | Should we generate a driver program? Default: <a>True</a>. When a
--   library is generated, it will have a driver if any of the contituent
--   functions has a driver. (See <tt>compileToCLib</tt>.)
cgGenerateDriver :: Bool -> SBVCodeGen ()

-- | Should we generate a Makefile? Default: <a>True</a>.
cgGenerateMakefile :: Bool -> SBVCodeGen ()

-- | Creates an atomic input in the generated code.
cgInput :: SymWord a => String -> SBVCodeGen (SBV a)

-- | Creates an array input in the generated code.
cgInputArr :: SymWord a => Int -> String -> SBVCodeGen [SBV a]

-- | Creates an atomic output in the generated code.
cgOutput :: SymWord a => String -> SBV a -> SBVCodeGen ()

-- | Creates an array output in the generated code.
cgOutputArr :: SymWord a => String -> [SBV a] -> SBVCodeGen ()

-- | Creates a returned (unnamed) value in the generated code.
cgReturn :: SymWord a => SBV a -> SBVCodeGen ()

-- | Creates a returned (unnamed) array value in the generated code.
cgReturnArr :: SymWord a => [SBV a] -> SBVCodeGen ()

-- | Adds the given lines to the header file generated, useful for
--   generating programs with uninterpreted functions.
cgAddPrototype :: [String] -> SBVCodeGen ()

-- | Adds the given lines to the program file generated, useful for
--   generating programs with uninterpreted functions.
cgAddDecl :: [String] -> SBVCodeGen ()

-- | Adds the given words to the compiler options in the generated
--   Makefile, useful for linking extra stuff in.
cgAddLDFlags :: [String] -> SBVCodeGen ()

-- | Sets number of bits to be used for representing the <a>SInteger</a>
--   type in the generated C code. The argument must be one of <tt>8</tt>,
--   <tt>16</tt>, <tt>32</tt>, or <tt>64</tt>. Note that this is
--   essentially unsafe as the semantics of unbounded Haskell integers
--   becomes reduced to the corresponding bit size, as typical in most C
--   implementations.
cgIntegerSize :: Int -> SBVCodeGen ()

-- | Sets the C type to be used for representing the <a>SReal</a> type in
--   the generated C code. The setting can be one of C's <tt>"float"</tt>,
--   <tt>"double"</tt>, or <tt>"long double"</tt>, types, depending on the
--   precision needed. Note that this is essentially unsafe as the
--   semantics of infinite precision SReal values becomes reduced to the
--   corresponding floating point type in C, and hence it is subject to
--   rounding errors.
cgSRealType :: CgSRealType -> SBVCodeGen ()

-- | Possible mappings for the <a>SReal</a> type when translated to C. Used
--   in conjunction with the function <a>cgSRealType</a>. Note that the
--   particular characteristics of the mapped types depend on the platform
--   and the compiler used for compiling the generated C program. See
--   <a>http://en.wikipedia.org/wiki/C_data_types</a> for details.
data CgSRealType

-- | <pre>
--   float
--   </pre>
CgFloat :: CgSRealType

-- | <pre>
--   double
--   </pre>
CgDouble :: CgSRealType

-- | <pre>
--   long double
--   </pre>
CgLongDouble :: CgSRealType

-- | Given a symbolic computation, render it as an equivalent collection of
--   files that make up a C program:
--   
--   <ul>
--   <li>The first argument is the directory name under which the files
--   will be saved. To save files in the current directory pass
--   <tt><a>Just</a> "."</tt>. Use <a>Nothing</a> for printing to
--   stdout.</li>
--   <li>The second argument is the name of the C function to
--   generate.</li>
--   <li>The final argument is the function to be compiled.</li>
--   </ul>
--   
--   Compilation will also generate a <tt>Makefile</tt>, a header file, and
--   a driver (test) program, etc.
compileToC :: Maybe FilePath -> String -> SBVCodeGen () -> IO ()

-- | Create code to generate a library archive (.a) from given symbolic
--   functions. Useful when generating code from multiple functions that
--   work together as a library.
--   
--   <ul>
--   <li>The first argument is the directory name under which the files
--   will be saved. To save files in the current directory pass
--   <tt><a>Just</a> "."</tt>. Use <a>Nothing</a> for printing to
--   stdout.</li>
--   <li>The second argument is the name of the archive to generate.</li>
--   <li>The third argument is the list of functions to include, in the
--   form of function-name/code pairs, similar to the second and third
--   arguments of <a>compileToC</a>, except in a list.</li>
--   </ul>
compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen ())] -> IO ()
instance [overlap ok] (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z)
instance [overlap ok] (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z)
instance [overlap ok] (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z)
instance [overlap ok] (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z)
instance [overlap ok] (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z)
instance [overlap ok] (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z)
instance [overlap ok] (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z)
instance [overlap ok] (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z)
instance [overlap ok] (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z)
instance [overlap ok] (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z)
instance [overlap ok] (SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z)
instance [overlap ok] (SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z)
instance [overlap ok] (SymWord a, EqSymbolic z) => Equality (SBV a -> z)


-- | Interface to the Boolector SMT solver. Import this module if you want
--   to use the Boolector SMT prover as your backend solver. Also see:
--   
--   <ul>
--   
--   <li><a>Data.SBV.Bridge.Yices</a><ul><li><a>Data.SBV.Bridge.Z3</a></li><li><a>Data.SBV.Bridge.CVC4</a></li><li><a>Data.SBV.Bridge.MathSAT</a></li></ul></li>
--   </ul>
module Data.SBV.Bridge.Boolector

-- | Current solver instance, pointing to cvc4.
sbvCurrentSolver :: SMTConfig

-- | Prove theorems, using the CVC4 SMT solver
prove :: Provable a => a -> IO ThmResult

-- | Find satisfying solutions, using the CVC4 SMT solver
sat :: Provable a => a -> IO SatResult

-- | Find all satisfying solutions, using the CVC4 SMT solver
allSat :: Provable a => a -> IO AllSatResult

-- | Check vacuity of the explicit constraints introduced by calls to the
--   <a>constrain</a> function, using the CVC4 SMT solver
isVacuous :: Provable a => a -> IO Bool

-- | Check if the statement is a theorem, with an optional time-out in
--   seconds, using the CVC4 SMT solver
isTheorem :: Provable a => Maybe Int -> a -> IO (Maybe Bool)

-- | Check if the statement is satisfiable, with an optional time-out in
--   seconds, using the CVC4 SMT solver
isSatisfiable :: Provable a => Maybe Int -> a -> IO (Maybe Bool)

-- | Optimize cost functions, using the CVC4 SMT solver
optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])

-- | Minimize cost functions, using the CVC4 SMT solver
minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])

-- | Maximize cost functions, using the CVC4 SMT solver
maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])


-- | Interface to the CVC4 SMT solver. Import this module if you want to
--   use the CVC4 SMT prover as your backend solver. Also see:
--   
--   <ul>
--   
--   <li><a>Data.SBV.Bridge.Yices</a><ul><li><a>Data.SBV.Bridge.Z3</a></li><li><a>Data.SBV.Bridge.Boolector</a></li><li><a>Data.SBV.Bridge.MathSAT</a></li></ul></li>
--   </ul>
module Data.SBV.Bridge.CVC4

-- | Current solver instance, pointing to cvc4.
sbvCurrentSolver :: SMTConfig

-- | Prove theorems, using the CVC4 SMT solver
prove :: Provable a => a -> IO ThmResult

-- | Find satisfying solutions, using the CVC4 SMT solver
sat :: Provable a => a -> IO SatResult

-- | Find all satisfying solutions, using the CVC4 SMT solver
allSat :: Provable a => a -> IO AllSatResult

-- | Check vacuity of the explicit constraints introduced by calls to the
--   <a>constrain</a> function, using the CVC4 SMT solver
isVacuous :: Provable a => a -> IO Bool

-- | Check if the statement is a theorem, with an optional time-out in
--   seconds, using the CVC4 SMT solver
isTheorem :: Provable a => Maybe Int -> a -> IO (Maybe Bool)

-- | Check if the statement is satisfiable, with an optional time-out in
--   seconds, using the CVC4 SMT solver
isSatisfiable :: Provable a => Maybe Int -> a -> IO (Maybe Bool)

-- | Optimize cost functions, using the CVC4 SMT solver
optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])

-- | Minimize cost functions, using the CVC4 SMT solver
minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])

-- | Maximize cost functions, using the CVC4 SMT solver
maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])


-- | Interface to the MathSAT SMT solver. Import this module if you want to
--   use the MathSAT SMT prover as your backend solver. Also see:
--   
--   <ul>
--   
--   <li><a>Data.SBV.Bridge.Yices</a><ul><li><a>Data.SBV.Bridge.Z3</a></li><li><a>Data.SBV.Bridge.CVC4</a></li><li><a>Data.SBV.Bridge.Boolector</a></li></ul></li>
--   </ul>
module Data.SBV.Bridge.MathSAT

-- | Current solver instance, pointing to cvc4.
sbvCurrentSolver :: SMTConfig

-- | Prove theorems, using the CVC4 SMT solver
prove :: Provable a => a -> IO ThmResult

-- | Find satisfying solutions, using the CVC4 SMT solver
sat :: Provable a => a -> IO SatResult

-- | Find all satisfying solutions, using the CVC4 SMT solver
allSat :: Provable a => a -> IO AllSatResult

-- | Check vacuity of the explicit constraints introduced by calls to the
--   <a>constrain</a> function, using the CVC4 SMT solver
isVacuous :: Provable a => a -> IO Bool

-- | Check if the statement is a theorem, with an optional time-out in
--   seconds, using the CVC4 SMT solver
isTheorem :: Provable a => Maybe Int -> a -> IO (Maybe Bool)

-- | Check if the statement is satisfiable, with an optional time-out in
--   seconds, using the CVC4 SMT solver
isSatisfiable :: Provable a => Maybe Int -> a -> IO (Maybe Bool)

-- | Optimize cost functions, using the CVC4 SMT solver
optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])

-- | Minimize cost functions, using the CVC4 SMT solver
minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])

-- | Maximize cost functions, using the CVC4 SMT solver
maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])


-- | Interface to the Yices SMT solver. Import this module if you want to
--   use the Yices SMT prover as your backend solver. Also see:
--   
--   <ul>
--   
--   <li><a>Data.SBV.Bridge.Boolector</a><ul><li><a>Data.SBV.Bridge.CVC4</a></li><li><a>Data.SBV.Bridge.Z3</a></li><li><a>Data.SBV.Bridge.MathSAT</a></li></ul></li>
--   </ul>
module Data.SBV.Bridge.Yices

-- | Current solver instance, pointing to yices.
sbvCurrentSolver :: SMTConfig

-- | Prove theorems, using the Yices SMT solver
prove :: Provable a => a -> IO ThmResult

-- | Find satisfying solutions, using the Yices SMT solver
sat :: Provable a => a -> IO SatResult

-- | Find all satisfying solutions, using the Yices SMT solver
allSat :: Provable a => a -> IO AllSatResult

-- | Check vacuity of the explicit constraints introduced by calls to the
--   <a>constrain</a> function, using the Yices SMT solver
isVacuous :: Provable a => a -> IO Bool

-- | Check if the statement is a theorem, with an optional time-out in
--   seconds, using the Yices SMT solver
isTheorem :: Provable a => Maybe Int -> a -> IO (Maybe Bool)

-- | Check if the statement is satisfiable, with an optional time-out in
--   seconds, using the Yices SMT solver
isSatisfiable :: Provable a => Maybe Int -> a -> IO (Maybe Bool)

-- | Optimize cost functions, using the Yices SMT solver
optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])

-- | Minimize cost functions, using the Yices SMT solver
minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])

-- | Maximize cost functions, using the Yices SMT solver
maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])


-- | Interface to the Z3 SMT solver. Import this module if you want to use
--   the Z3 SMT prover as your backend solver. Also see:
--   
--   <ul>
--   
--   <li><a>Data.SBV.Bridge.Boolector</a><ul><li><a>Data.SBV.Bridge.CVC4</a></li><li><a>Data.SBV.Bridge.Yices</a></li><li><a>Data.SBV.Bridge.MathSAT</a></li></ul></li>
--   </ul>
module Data.SBV.Bridge.Z3

-- | Current solver instance, pointing to z3.
sbvCurrentSolver :: SMTConfig

-- | Prove theorems, using the Z3 SMT solver
prove :: Provable a => a -> IO ThmResult

-- | Find satisfying solutions, using the Z3 SMT solver
sat :: Provable a => a -> IO SatResult

-- | Find all satisfying solutions, using the Z3 SMT solver
allSat :: Provable a => a -> IO AllSatResult

-- | Check vacuity of the explicit constraints introduced by calls to the
--   <a>constrain</a> function, using the Z3 SMT solver
isVacuous :: Provable a => a -> IO Bool

-- | Check if the statement is a theorem, with an optional time-out in
--   seconds, using the Z3 SMT solver
isTheorem :: Provable a => Maybe Int -> a -> IO (Maybe Bool)

-- | Check if the statement is satisfiable, with an optional time-out in
--   seconds, using the Z3 SMT solver
isSatisfiable :: Provable a => Maybe Int -> a -> IO (Maybe Bool)

-- | Optimize cost functions, using the Z3 SMT solver
optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])

-- | Minimize cost functions, using the Z3 SMT solver
minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])

-- | Maximize cost functions, using the Z3 SMT solver
maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])


-- | Checks the correctness of a few tricks from the large collection found
--   in: <a>http://graphics.stanford.edu/~seander/bithacks.html</a>
module Data.SBV.Examples.BitPrecise.BitTricks

-- | Formalizes
--   <a>http://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax</a>
fastMinCorrect :: SInt32 -> SInt32 -> SBool

-- | Formalizes
--   <a>http://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax</a>
fastMaxCorrect :: SInt32 -> SInt32 -> SBool

-- | Formalizes
--   <a>http://graphics.stanford.edu/~seander/bithacks.html#DetectOppositeSigns</a>
oppositeSignsCorrect :: SInt32 -> SInt32 -> SBool

-- | Formalizes
--   <a>http://graphics.stanford.edu/~seander/bithacks.html#ConditionalSetOrClearBitsWithoutBranching</a>
conditionalSetClearCorrect :: SBool -> SWord32 -> SWord32 -> SBool

-- | Formalizes
--   <a>http://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2</a>
powerOfTwoCorrect :: SWord32 -> SBool

-- | Collection of queries
queries :: IO ()


-- | An encoding and correctness proof of Legato's multiplier in Haskell.
--   Bill Legato came up with an interesting way to multiply two 8-bit
--   numbers on Mostek, as described here:
--   <a>http://www.cs.utexas.edu/~moore/acl2/workshop-2004/contrib/legato/Weakest-Preconditions-Report.pdf</a>
--   
--   Here's Legato's algorithm, as coded in Mostek assembly:
--   
--   <pre>
--   step1 :       LDX #8         ; load X immediate with the integer 8 
--   step2 :       LDA #0         ; load A immediate with the integer 0 
--   step3 : LOOP  ROR F1         ; rotate F1 right circular through C 
--   step4 :       BCC ZCOEF      ; branch to ZCOEF if C = 0 
--   step5 :       CLC            ; set C to 0 
--   step6 :       ADC F2         ; set A to A+F2+C and C to the carry 
--   step7 : ZCOEF ROR A          ; rotate A right circular through C 
--   step8 :       ROR LOW        ; rotate LOW right circular through C 
--   step9 :       DEX            ; set X to X-1 
--   step10:       BNE LOOP       ; branch to LOOP if Z = 0 
--   </pre>
--   
--   This program came to be known as the Legato's challenge in the
--   community, where the challenge was to prove that it indeed does
--   perform multiplication. This file formalizes the Mostek architecture
--   in Haskell and proves that Legato's algorithm is indeed correct.
module Data.SBV.Examples.BitPrecise.Legato

-- | The memory is addressed by 32-bit words.
type Address = SWord32

-- | We model only two registers of Mostek that is used in the above
--   algorithm, can add more.
data Register
RegX :: Register
RegA :: Register

-- | The carry flag (<a>FlagC</a>) and the zero flag (<a>FlagZ</a>)
data Flag
FlagC :: Flag
FlagZ :: Flag

-- | Mostek was an 8-bit machine.
type Value = SWord8

-- | Convenient synonym for symbolic machine bits.
type Bit = SBool

-- | Register bank
type Registers = Array Register Value

-- | Flag bank
type Flags = Array Flag Bit

-- | The memory maps 32-bit words to 8-bit words. (The <a>Model</a>
--   data-type is defined later, depending on the verification model used.)
type Memory = Model Word32 Word8

-- | Abstraction of the machine: The CPU consists of memory, registers, and
--   flags. Unlike traditional hardware, we assume the program is stored in
--   some other memory area that we need not model. (No self modifying
--   programs!)
data Mostek
Mostek :: Memory -> Registers -> Flags -> Mostek
memory :: Mostek -> Memory
registers :: Mostek -> Registers
flags :: Mostek -> Flags

-- | Given a machine state, compute a value out of it
type Extract a = Mostek -> a

-- | Programs are essentially state transformers (on the machine state)
type Program = Mostek -> Mostek

-- | <a>Mergeable</a> instance of <a>Mostek</a> simply pushes the merging
--   into record fields.

-- | Get the value of a given register
getReg :: Register -> Extract Value

-- | Set the value of a given register
setReg :: Register -> Value -> Program

-- | Get the value of a flag
getFlag :: Flag -> Extract Bit

-- | Set the value of a flag
setFlag :: Flag -> Bit -> Program

-- | Read memory
peek :: Address -> Extract Value

-- | Write to memory
poke :: Address -> Value -> Program

-- | Checking overflow. In Legato's multipler the <tt>ADC</tt> instruction
--   needs to see if the expression x + y + c overflowed, as checked by
--   this function. Note that we verify the correctness of this check
--   separately below in <a>checkOverflowCorrect</a>.
checkOverflow :: SWord8 -> SWord8 -> SBool -> SBool

-- | Correctness theorem for our <a>checkOverflow</a> implementation.
--   
--   We have:
--   
--   <pre>
--   &gt;&gt;&gt; checkOverflowCorrect
--   Q.E.D.
--   </pre>
checkOverflowCorrect :: IO ThmResult

-- | An instruction is modeled as a <a>Program</a> transformer. We model
--   mostek programs in direct continuation passing style.
type Instruction = Program -> Program

-- | LDX: Set register <tt>X</tt> to value <tt>v</tt>
ldx :: Value -> Instruction

-- | LDA: Set register <tt>A</tt> to value <tt>v</tt>
lda :: Value -> Instruction

-- | CLC: Clear the carry flag
clc :: Instruction

-- | ROR, memory version: Rotate the value at memory location <tt>a</tt> to
--   the right by 1 bit, using the carry flag as a transfer position. That
--   is, the final bit of the memory location becomes the new carry and the
--   carry moves over to the first bit. This very instruction is one of the
--   reasons why Legato's multiplier is quite hard to understand and is
--   typically presented as a verification challenge.
rorM :: Address -> Instruction

-- | ROR, register version: Same as <a>rorM</a>, except through register
--   <tt>r</tt>.
rorR :: Register -> Instruction

-- | BCC: branch to label <tt>l</tt> if the carry flag is false
bcc :: Program -> Instruction

-- | ADC: Increment the value of register <tt>A</tt> by the value of memory
--   contents at address <tt>a</tt>, using the carry-bit as the carry-in
--   for the addition.
adc :: Address -> Instruction

-- | DEX: Decrement the value of register <tt>X</tt>
dex :: Instruction

-- | BNE: Branch if the zero-flag is false
bne :: Program -> Instruction

-- | The <a>end</a> combinator "stops" our program, providing the final
--   continuation that does nothing.
end :: Program

-- | Parameterized by the addresses of locations of the factors
--   (<tt>F1</tt> and <tt>F2</tt>), the following program multiplies them,
--   storing the low-byte of the result in the memory location
--   <tt>lowAddr</tt>, and the high-byte in register <tt>A</tt>. The
--   implementation is a direct transliteration of Legato's algorithm given
--   at the top, using our notation.
legato :: Address -> Address -> Address -> Program

-- | Given address/value pairs for F1 and F2, and the location of where the
--   low-byte of the result should go, <tt>runLegato</tt> takes an
--   arbitrary machine state <tt>m</tt> and returns the high and low bytes
--   of the multiplication.
runLegato :: (Address, Value) -> (Address, Value) -> Address -> Mostek -> (Value, Value)

-- | Helper synonym for capturing relevant bits of Mostek
type InitVals = (Value, Value, Value, Bit, Bit)

-- | Create an instance of the Mostek machine, initialized by the memory
--   and the relevant values of the registers and the flags
initMachine :: Memory -> InitVals -> Mostek

-- | The correctness theorem. For all possible memory configurations, the
--   factors (<tt>x</tt> and <tt>y</tt> below), the location of the
--   low-byte result and the initial-values of registers and the flags,
--   this function will return True only if running Legato's algorithm does
--   indeed compute the product of <tt>x</tt> and <tt>y</tt> correctly.
legatoIsCorrect :: Memory -> (Address, Value) -> (Address, Value) -> Address -> InitVals -> SBool

-- | Choose the appropriate array model to be used for modeling the memory.
--   (See <a>Memory</a>.) The <a>SFunArray</a> is the function based model.
--   <a>SArray</a> is the SMT-Lib array's based model.
type Model = SFunArray

-- | The correctness theorem. On a decent MacBook Pro, this proof takes
--   about 3 minutes with the <a>SFunArray</a> memory model and about 30
--   minutes with the <a>SArray</a> model, using yices as the SMT solver
correctnessTheorem :: IO ThmResult

-- | Generate a C program that implements Legato's algorithm automatically.
legatoInC :: IO ()
instance Eq Register
instance Ord Register
instance Ix Register
instance Bounded Register
instance Enum Register
instance Eq Flag
instance Ord Flag
instance Ix Flag
instance Bounded Flag
instance Enum Flag
instance Mergeable Mostek


-- | Symbolic implementation of merge-sort and its correctness.
module Data.SBV.Examples.BitPrecise.MergeSort

-- | Element type of lists we'd like to sort. For simplicity, we'll just
--   use <a>SWord8</a> here, but we can pick any symbolic type.
type E = SWord8

-- | Merging two given sorted lists, preserving the order.
merge :: [E] -> [E] -> [E]

-- | Simple merge-sort implementation. We simply divide the input list in
--   two two halves so long as it has at least two elements, sort each half
--   on its own, and then merge.
mergeSort :: [E] -> [E]

-- | Check whether a given sequence is non-decreasing.
nonDecreasing :: [E] -> SBool

-- | Check whether two given sequences are permutations. We simply check
--   that each sequence is a subset of the other, when considered as a set.
--   The check is slightly complicated for the need to account for possibly
--   duplicated elements.
isPermutationOf :: [E] -> [E] -> SBool

-- | Asserting correctness of merge-sort for a list of the given size. Note
--   that we can only check correctness for fixed-size lists. Also, the
--   proof will get more and more complicated for the backend SMT solver as
--   <tt>n</tt> increases. A value around 5 or 6 should be fairly easy to
--   prove. For instance, we have:
--   
--   <pre>
--   &gt;&gt;&gt; correctness 5
--   Q.E.D.
--   </pre>
correctness :: Int -> IO ThmResult

-- | Generate C code for merge-sorting an array of size <tt>n</tt>. Again,
--   we're restricted to fixed size inputs. While the output is not how one
--   would code merge sort in C by hand, it's a faithful rendering of all
--   the operations merge-sort would do as described by it's Haskell
--   counterpart.
codeGen :: Int -> IO ()


-- | The PrefixSum algorithm over power-lists and proof of the
--   Ladner-Fischer implementation. See
--   <a>http://www.cs.utexas.edu/users/psp/powerlist.pdf</a> and
--   <a>http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf</a>.
module Data.SBV.Examples.BitPrecise.PrefixSum

-- | A poor man's representation of powerlists and basic operations on
--   them: <a>http://www.cs.utexas.edu/users/psp/powerlist.pdf</a>. We
--   merely represent power-lists by ordinary lists.
type PowerList a = [a]

-- | The tie operator, concatenation.
tiePL :: PowerList a -> PowerList a -> PowerList a

-- | The zip operator, zips the power-lists of the same size, returns a
--   powerlist of double the size.
zipPL :: PowerList a -> PowerList a -> PowerList a

-- | Inverse of zipping.
unzipPL :: PowerList a -> (PowerList a, PowerList a)

-- | Reference prefix sum (<tt>ps</tt>) is simply Haskell's <tt>scanl1</tt>
--   function.
ps :: (a, a -> a -> a) -> PowerList a -> PowerList a

-- | The Ladner-Fischer (<tt>lf</tt>) implementation of prefix-sum. See
--   <a>http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf</a>
--   or pg. 16 of <a>http://www.cs.utexas.edu/users/psp/powerlist.pdf</a>.
lf :: (a, a -> a -> a) -> PowerList a -> PowerList a

-- | Correctness theorem, for a powerlist of given size, an associative
--   operator, and its left-unit element.
flIsCorrect :: Int -> (forall a. (OrdSymbolic a, Num a, Bits a) => (a, a -> a -> a)) -> Symbolic SBool

-- | Proves Ladner-Fischer is equivalent to reference specification for
--   addition. <tt>0</tt> is the left-unit element, and we use a power-list
--   of size <tt>8</tt>.
thm1 :: IO ThmResult

-- | Proves Ladner-Fischer is equivalent to reference specification for the
--   function <tt>max</tt>. <tt>0</tt> is the left-unit element, and we use
--   a power-list of size <tt>16</tt>.
thm2 :: IO ThmResult

-- | Try proving correctness for an arbitrary operator. This proof will
--   <i>not</i> go through since the SMT solver does not know that the
--   operator associative and has the given left-unit element. We have:
--   
--   <pre>
--   &gt;&gt;&gt; thm3
--   Falsifiable. Counter-example:
--     s0 = 0 :: SWord32
--     s1 = 0 :: SWord32
--     s2 = 0 :: SWord32
--     s3 = 0 :: SWord32
--     s4 = 1073741824 :: SWord32
--     s5 = 0 :: SWord32
--     s6 = 0 :: SWord32
--     s7 = 0 :: SWord32
--     -- uninterpreted: u
--          u  = 0
--     -- uninterpreted: flOp
--          flOp 0          0          = 2147483648
--          flOp 0          1073741824 = 3221225472
--          flOp 2147483648 0          = 3221225472
--          flOp 2147483648 1073741824 = 1073741824
--          flOp _          _          = 0
--   </pre>
--   
--   You can verify that the function <tt>flOp</tt> is indeed not
--   associative:
--   
--   <pre>
--   ghci&gt; flOp 3221225472 (flOp 2147483648 1073741824)
--   0
--   ghci&gt; flOp (flOp 3221225472 2147483648) 1073741824
--   3221225472
--   </pre>
--   
--   Also, the unit <tt>0</tt> is clearly not a left-unit for
--   <tt>flOp</tt>, as the last equation for <tt>flOp</tt> will simply map
--   many elements to <tt>0</tt>. (NB. We need to use yices for this proof
--   as the uninterpreted function examples are only supported through the
--   yices interface currently.)
thm3 :: IO ThmResult

-- | Generate an instance of the prefix-sum problem for an arbitrary
--   operator, by telling the SMT solver the necessary axioms for
--   associativity and left-unit. The first argument states how wide the
--   power list should be.
genPrefixSumInstance :: Int -> Symbolic SBool

-- | Prove the generic problem for powerlists of given sizes. Note that
--   this will only work for Yices-1. This is due to the fact that Yices-2
--   follows the SMT-Lib standard and does not accept bit-vector problems
--   with quantified axioms in them, while Yices-1 did allow for that. The
--   crux of the problem is that there are no SMT-Lib logics that combine
--   BV's and quantifiers, see:
--   <a>http://goedel.cs.uiowa.edu/smtlib/logics.html</a>. So we are stuck
--   until new powerful logics are added to SMT-Lib.
--   
--   Here, we explicitly tell SBV to use Yices-1 that did not have that
--   limitation. Tweak the executable location accordingly below for your
--   platform..
--   
--   We have:
--   
--   <pre>
--   &gt;&gt;&gt; prefixSum 2
--   Q.E.D.
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; prefixSum 4
--   Q.E.D.
--   </pre>
--   
--   Note that these proofs tend to run long. Also, Yices ran out of memory
--   and crashed on my box when I tried for size <tt>8</tt>, after running
--   for about 2.5 minutes..
prefixSum :: Int -> IO ThmResult

-- | Old version of Yices that supports quantified axioms in SMT-Lib1
yices1029 :: SMTConfig

-- | Another old version of yices, suitable for the non-axiom based problem
yicesSMT09 :: SMTConfig

-- | A symbolic trace can help illustrate the action of Ladner-Fischer.
--   This generator produces the actions of Ladner-Fischer for addition,
--   showing how the computation proceeds:
--   
--   <pre>
--   &gt;&gt;&gt; ladnerFischerTrace 8
--   INPUTS
--     s0 :: SWord8
--     s1 :: SWord8
--     s2 :: SWord8
--     s3 :: SWord8
--     s4 :: SWord8
--     s5 :: SWord8
--     s6 :: SWord8
--     s7 :: SWord8
--   CONSTANTS
--     s_2 = False
--     s_1 = True
--   TABLES
--   ARRAYS
--   UNINTERPRETED CONSTANTS
--   USER GIVEN CODE SEGMENTS
--   AXIOMS
--   DEFINE
--     s8 :: SWord8 = s0 + s1
--     s9 :: SWord8 = s2 + s8
--     s10 :: SWord8 = s2 + s3
--     s11 :: SWord8 = s8 + s10
--     s12 :: SWord8 = s4 + s11
--     s13 :: SWord8 = s4 + s5
--     s14 :: SWord8 = s11 + s13
--     s15 :: SWord8 = s6 + s14
--     s16 :: SWord8 = s6 + s7
--     s17 :: SWord8 = s13 + s16
--     s18 :: SWord8 = s11 + s17
--   CONSTRAINTS
--   OUTPUTS
--     s0
--     s8
--     s9
--     s11
--     s12
--     s14
--     s15
--     s18
--   </pre>
ladnerFischerTrace :: Int -> IO ()

-- | Trace generator for the reference spec. It clearly demonstrates that
--   the reference implementation fewer operations, but is not
--   parallelizable at all:
--   
--   <pre>
--   &gt;&gt;&gt; scanlTrace 8
--   INPUTS
--     s0 :: SWord8
--     s1 :: SWord8
--     s2 :: SWord8
--     s3 :: SWord8
--     s4 :: SWord8
--     s5 :: SWord8
--     s6 :: SWord8
--     s7 :: SWord8
--   CONSTANTS
--     s_2 = False
--     s_1 = True
--   TABLES
--   ARRAYS
--   UNINTERPRETED CONSTANTS
--   USER GIVEN CODE SEGMENTS
--   AXIOMS
--   DEFINE
--     s8 :: SWord8 = s0 + s1
--     s9 :: SWord8 = s2 + s8
--     s10 :: SWord8 = s3 + s9
--     s11 :: SWord8 = s4 + s10
--     s12 :: SWord8 = s5 + s11
--     s13 :: SWord8 = s6 + s12
--     s14 :: SWord8 = s7 + s13
--   CONSTRAINTS
--   OUTPUTS
--     s0
--     s8
--     s9
--     s10
--     s11
--     s12
--     s13
--     s14
--   </pre>
scanlTrace :: Int -> IO ()


-- | Simple code generation example.
module Data.SBV.Examples.CodeGeneration.AddSub

-- | Simple function that returns add/sum of args
addSub :: SWord8 -> SWord8 -> (SWord8, SWord8)

-- | Generate C code for addSub. Here's the output showing the generated C
--   code:
--   
--   <pre>
--   &gt;&gt;&gt; genAddSub
--   == BEGIN: "Makefile" ================
--   # Makefile for addSub. Automatically generated by SBV. Do not edit!
--   
--   # include any user-defined .mk file in the current directory.
--   -include *.mk
--   
--   CC=gcc
--   CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
--   
--   all: addSub_driver
--   
--   addSub.o: addSub.c addSub.h
--   	${CC} ${CCFLAGS} -c $&lt; -o $@
--   
--   addSub_driver.o: addSub_driver.c
--   	${CC} ${CCFLAGS} -c $&lt; -o $@
--   
--   addSub_driver: addSub.o addSub_driver.o
--   	${CC} ${CCFLAGS} $^ -o $@
--   
--   clean:
--   	rm -f *.o
--   
--   veryclean: clean
--   	rm -f addSub_driver
--   == END: "Makefile" ==================
--   == BEGIN: "addSub.h" ================
--   /* Header file for addSub. Automatically generated by SBV. Do not edit! */
--   
--   #ifndef __addSub__HEADER_INCLUDED__
--   #define __addSub__HEADER_INCLUDED__
--   
--   #include &lt;inttypes.h&gt;
--   #include &lt;stdint.h&gt;
--   #include &lt;stdbool.h&gt;
--   #include &lt;math.h&gt;
--   
--   /* The boolean type */
--   typedef bool SBool;
--   
--   /* The float type */
--   typedef float SFloat;
--   
--   /* The double type */
--   typedef double SDouble;
--   
--   /* Unsigned bit-vectors */
--   typedef uint8_t  SWord8 ;
--   typedef uint16_t SWord16;
--   typedef uint32_t SWord32;
--   typedef uint64_t SWord64;
--   
--   /* Signed bit-vectors */
--   typedef int8_t  SInt8 ;
--   typedef int16_t SInt16;
--   typedef int32_t SInt32;
--   typedef int64_t SInt64;
--   
--   /* Entry point prototype: */
--   void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,
--               SWord8 *dif);
--   
--   #endif /* __addSub__HEADER_INCLUDED__ */
--   == END: "addSub.h" ==================
--   == BEGIN: "addSub_driver.c" ================
--   /* Example driver program for addSub. */
--   /* Automatically generated by SBV. Edit as you see fit! */
--   
--   #include &lt;inttypes.h&gt;
--   #include &lt;stdint.h&gt;
--   #include &lt;stdbool.h&gt;
--   #include &lt;math.h&gt;
--   #include &lt;stdio.h&gt;
--   #include "addSub.h"
--   
--   int main(void)
--   {
--     SWord8 sum;
--     SWord8 dif;
--   
--     addSub(132, 241, &amp;sum, &amp;dif);
--   
--     printf("addSub(132, 241, &amp;sum, &amp;dif) -&gt;\n");
--     printf("  sum = %"PRIu8"\n", sum);
--     printf("  dif = %"PRIu8"\n", dif);
--   
--     return 0;
--   }
--   == END: "addSub_driver.c" ==================
--   == BEGIN: "addSub.c" ================
--   /* File: "addSub.c". Automatically generated by SBV. Do not edit! */
--   
--   #include &lt;inttypes.h&gt;
--   #include &lt;stdint.h&gt;
--   #include &lt;stdbool.h&gt;
--   #include &lt;math.h&gt;
--   #include "addSub.h"
--   
--   void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,
--               SWord8 *dif)
--   {
--     const SWord8 s0 = x;
--     const SWord8 s1 = y;
--     const SWord8 s2 = s0 + s1;
--     const SWord8 s3 = s0 - s1;
--   
--     *sum = s2;
--     *dif = s3;
--   }
--   == END: "addSub.c" ==================
--   </pre>
genAddSub :: IO ()


-- | Computing the CRC symbolically, using the USB polynomial. We also
--   generating C code for it as well. This example demonstrates the use of
--   the <a>crcBV</a> function, along with how CRC's can be computed
--   mathematically using polynomial division. While the results are the
--   same (i.e., proven equivalent, see <a>crcGood</a> below), the internal
--   CRC implementation generates much better code, compare <a>cg1</a> vs
--   <a>cg2</a> below.
module Data.SBV.Examples.CodeGeneration.CRC_USB5

-- | The USB CRC polynomial: <tt>x^5 + x^2 + 1</tt>. Although this
--   polynomial needs just 6 bits to represent (5 if higher order bit is
--   implicitly assumed to be set), we'll simply use a 16 bit number for
--   its representation to keep things simple for code generation purposes.
usb5 :: SWord16

-- | Given an 11 bit message, compute the CRC of it using the USB
--   polynomial, which is 5 bits, and then append it to the msg to get a
--   16-bit word. Again, the incoming 11-bits is represented as a 16-bit
--   word, with 5 highest bits essentially ignored for input purposes.
crcUSB :: SWord16 -> SWord16

-- | Alternate method for computing the CRC, <i>mathematically</i>. We
--   shift the number to the left by 5, and then compute the remainder from
--   the polynomial division by the USB polynomial. The result is then
--   appended to the end of the message.
crcUSB' :: SWord16 -> SWord16

-- | Prove that the custom <a>crcBV</a> function is equivalent to the
--   mathematical definition of CRC's for 11 bit messages. We have:
--   
--   <pre>
--   &gt;&gt;&gt; crcGood
--   Q.E.D.
--   </pre>
crcGood :: IO ThmResult

-- | Generate a C function to compute the USB CRC, using the internal CRC
--   function.
cg1 :: IO ()

-- | Generate a C function to compute the USB CRC, using the mathematical
--   definition of the CRCs. Whule this version generates functionally
--   eqivalent C code, it's less efficient; it has about 30% more code. So,
--   the above version is preferable for code generation purposes.
cg2 :: IO ()


-- | Computing Fibonacci numbers and generating C code. Inspired by Lee
--   Pike's original implementation, modified for inclusion in the package.
--   It illustrates symbolic termination issues one can have when working
--   with recursive algorithms and how to deal with such, eventually
--   generating good C code.
module Data.SBV.Examples.CodeGeneration.Fibonacci

-- | This is a naive implementation of fibonacci, and will work fine
--   (albeit slow) for concrete inputs:
--   
--   <pre>
--   &gt;&gt;&gt; map fib0 [0..6]
--   [0 :: SWord64,1 :: SWord64,1 :: SWord64,2 :: SWord64,3 :: SWord64,5 :: SWord64,8 :: SWord64]
--   </pre>
--   
--   However, it is not suitable for doing proofs or generating code, as it
--   is not symbolically terminating when it is called with a symbolic
--   value <tt>n</tt>. When we recursively call <tt>fib0</tt> on
--   <tt>n-1</tt> (or <tt>n-2</tt>), the test against <tt>0</tt> will
--   always explore both branches since the result will be symbolic, hence
--   will not terminate. (An integrated theorem prover can establish
--   termination after a certain number of unrollings, but this would be
--   quite expensive to implement, and would be impractical.)
fib0 :: SWord64 -> SWord64

-- | The recursion-depth limited version of fibonacci. Limiting the maximum
--   number to be 20, we can say:
--   
--   <pre>
--   &gt;&gt;&gt; map (fib1 20) [0..6]
--   [0 :: SWord64,1 :: SWord64,1 :: SWord64,2 :: SWord64,3 :: SWord64,5 :: SWord64,8 :: SWord64]
--   </pre>
--   
--   The function will work correctly, so long as the index we query is at
--   most <tt>top</tt>, and otherwise will return the value at
--   <tt>top</tt>. Note that we also use accumulating parameters here for
--   efficiency, although this is orthogonal to the termination concern.
--   
--   A note on modular arithmetic: The 64-bit word we use to represent the
--   values will of course eventually overflow, beware! Fibonacci is a fast
--   growing function..
fib1 :: SWord64 -> SWord64 -> SWord64

-- | We can generate code for <a>fib1</a> using the <a>genFib1</a> action.
--   Note that the generated code will grow larger as we pick larger values
--   of <tt>top</tt>, but only linearly, thanks to the accumulating
--   parameter trick used by <a>fib1</a>. The following is an excerpt from
--   the code generated for the call <tt>genFib1 10</tt>, where the code
--   will work correctly for indexes up to 10:
--   
--   <pre>
--   SWord64 fib1(const SWord64 x)
--   {
--     const SWord64 s0 = x;
--     const SBool   s2 = s0 == 0x0000000000000000ULL;
--     const SBool   s4 = s0 == 0x0000000000000001ULL;
--     const SBool   s6 = s0 == 0x0000000000000002ULL;
--     const SBool   s8 = s0 == 0x0000000000000003ULL;
--     const SBool   s10 = s0 == 0x0000000000000004ULL;
--     const SBool   s12 = s0 == 0x0000000000000005ULL;
--     const SBool   s14 = s0 == 0x0000000000000006ULL;
--     const SBool   s17 = s0 == 0x0000000000000007ULL;
--     const SBool   s19 = s0 == 0x0000000000000008ULL;
--     const SBool   s22 = s0 == 0x0000000000000009ULL;
--     const SWord64 s25 = s22 ? 0x0000000000000022ULL : 0x0000000000000037ULL;
--     const SWord64 s26 = s19 ? 0x0000000000000015ULL : s25;
--     const SWord64 s27 = s17 ? 0x000000000000000dULL : s26;
--     const SWord64 s28 = s14 ? 0x0000000000000008ULL : s27;
--     const SWord64 s29 = s12 ? 0x0000000000000005ULL : s28;
--     const SWord64 s30 = s10 ? 0x0000000000000003ULL : s29;
--     const SWord64 s31 = s8 ? 0x0000000000000002ULL : s30;
--     const SWord64 s32 = s6 ? 0x0000000000000001ULL : s31;
--     const SWord64 s33 = s4 ? 0x0000000000000001ULL : s32;
--     const SWord64 s34 = s2 ? 0x0000000000000000ULL : s33;
--     
--     return s34;
--   }
--   </pre>
genFib1 :: SWord64 -> IO ()

-- | Compute the fibonacci numbers statically at <i>code-generation</i>
--   time and put them in a table, accessed by the <a>select</a> call.
fib2 :: SWord64 -> SWord64 -> SWord64

-- | Once we have <a>fib2</a>, we can generate the C code
--   straightforwardly. Below is an excerpt from the code that SBV
--   generates for the call <tt>genFib2 64</tt>. Note that this code is a
--   constant-time look-up table implementation of fibonacci, with no
--   run-time overhead. The index can be made arbitrarily large, naturally.
--   (Note that this function returns <tt>0</tt> if the index is larger
--   than 64, as specified by the call to <a>select</a> with default
--   <tt>0</tt>.)
--   
--   <pre>
--   SWord64 fibLookup(const SWord64 x)
--   {
--     const SWord64 s0 = x;
--     static const SWord64 table0[] = {
--         0x0000000000000000ULL, 0x0000000000000001ULL,
--         0x0000000000000001ULL, 0x0000000000000002ULL,
--         0x0000000000000003ULL, 0x0000000000000005ULL,
--         0x0000000000000008ULL, 0x000000000000000dULL,
--         0x0000000000000015ULL, 0x0000000000000022ULL,
--         0x0000000000000037ULL, 0x0000000000000059ULL,
--         0x0000000000000090ULL, 0x00000000000000e9ULL,
--         0x0000000000000179ULL, 0x0000000000000262ULL,
--         0x00000000000003dbULL, 0x000000000000063dULL,
--         0x0000000000000a18ULL, 0x0000000000001055ULL,
--         0x0000000000001a6dULL, 0x0000000000002ac2ULL,
--         0x000000000000452fULL, 0x0000000000006ff1ULL,
--         0x000000000000b520ULL, 0x0000000000012511ULL,
--         0x000000000001da31ULL, 0x000000000002ff42ULL,
--         0x000000000004d973ULL, 0x000000000007d8b5ULL,
--         0x00000000000cb228ULL, 0x0000000000148addULL,
--         0x0000000000213d05ULL, 0x000000000035c7e2ULL,
--         0x00000000005704e7ULL, 0x00000000008cccc9ULL,
--         0x0000000000e3d1b0ULL, 0x0000000001709e79ULL,
--         0x0000000002547029ULL, 0x0000000003c50ea2ULL,
--         0x0000000006197ecbULL, 0x0000000009de8d6dULL,
--         0x000000000ff80c38ULL, 0x0000000019d699a5ULL,
--         0x0000000029cea5ddULL, 0x0000000043a53f82ULL,
--         0x000000006d73e55fULL, 0x00000000b11924e1ULL,
--         0x000000011e8d0a40ULL, 0x00000001cfa62f21ULL,
--         0x00000002ee333961ULL, 0x00000004bdd96882ULL,
--         0x00000007ac0ca1e3ULL, 0x0000000c69e60a65ULL,
--         0x0000001415f2ac48ULL, 0x000000207fd8b6adULL,
--         0x0000003495cb62f5ULL, 0x0000005515a419a2ULL,
--         0x00000089ab6f7c97ULL, 0x000000dec1139639ULL,
--         0x000001686c8312d0ULL, 0x000002472d96a909ULL,
--         0x000003af9a19bbd9ULL, 0x000005f6c7b064e2ULL, 0x000009a661ca20bbULL
--     };
--     const SWord64 s65 = s0 &gt;= 65 ? 0x0000000000000000ULL : table0[s0];
--     
--     return s65;
--   }
--   </pre>
genFib2 :: SWord64 -> IO ()


-- | Computing GCD symbolically, and generating C code for it. This example
--   illustrates symbolic termination related issues when programming with
--   SBV, when the termination of a recursive algorithm crucially depends
--   on the value of a symbolic variable. The technique we use is to
--   statically enforce termination by using a recursion depth counter.
module Data.SBV.Examples.CodeGeneration.GCD

-- | The symbolic GCD algorithm, over two 8-bit numbers. We define <tt>sgcd
--   a 0</tt> to be <tt>a</tt> for all <tt>a</tt>, which implies <tt>sgcd 0
--   0 = 0</tt>. Note that this is essentially Euclid's algorithm, except
--   with a recursion depth counter. We need the depth counter since the
--   algorithm is not <i>symbolically terminating</i>, as we don't have a
--   means of determining that the second argument (<tt>b</tt>) will
--   eventually reach 0 in a symbolic context. Hence we stop after 12
--   iterations. Why 12? We've empirically determined that this algorithm
--   will recurse at most 12 times for arbitrary 8-bit numbers. Of course,
--   this is a claim that we shall prove below.
sgcd :: SWord8 -> SWord8 -> SWord8

-- | We have:
--   
--   <pre>
--   &gt;&gt;&gt; prove sgcdIsCorrect
--   Q.E.D.
--   </pre>
sgcdIsCorrect :: SWord8 -> SWord8 -> SWord8 -> SBool

-- | This call will generate the required C files. The following is the
--   function body generated for <a>sgcd</a>. (We are not showing the
--   generated header, <tt>Makefile</tt>, and the driver programs for
--   brevity.) Note that the generated function is a constant time
--   algorithm for GCD. It is not necessarily fastest, but it will take
--   precisely the same amount of time for all values of <tt>x</tt> and
--   <tt>y</tt>.
--   
--   <pre>
--   /* File: "sgcd.c". Automatically generated by SBV. Do not edit! */
--   
--   #include &lt;inttypes.h&gt;
--   #include &lt;stdint.h&gt;
--   #include &lt;stdbool.h&gt;
--   #include "sgcd.h"
--   
--   SWord8 sgcd(const SWord8 x, const SWord8 y)
--   {
--     const SWord8 s0 = x;
--     const SWord8 s1 = y;
--     const SBool  s3 = s1 == 0;
--     const SWord8 s4 = (s1 == 0) ? s0 : (s0 % s1);
--     const SWord8 s5 = s3 ? s0 : s4;
--     const SBool  s6 = 0 == s5;
--     const SWord8 s7 = (s5 == 0) ? s1 : (s1 % s5);
--     const SWord8 s8 = s6 ? s1 : s7;
--     const SBool  s9 = 0 == s8;
--     const SWord8 s10 = (s8 == 0) ? s5 : (s5 % s8);
--     const SWord8 s11 = s9 ? s5 : s10;
--     const SBool  s12 = 0 == s11;
--     const SWord8 s13 = (s11 == 0) ? s8 : (s8 % s11);
--     const SWord8 s14 = s12 ? s8 : s13;
--     const SBool  s15 = 0 == s14;
--     const SWord8 s16 = (s14 == 0) ? s11 : (s11 % s14);
--     const SWord8 s17 = s15 ? s11 : s16;
--     const SBool  s18 = 0 == s17;
--     const SWord8 s19 = (s17 == 0) ? s14 : (s14 % s17);
--     const SWord8 s20 = s18 ? s14 : s19;
--     const SBool  s21 = 0 == s20;
--     const SWord8 s22 = (s20 == 0) ? s17 : (s17 % s20);
--     const SWord8 s23 = s21 ? s17 : s22;
--     const SBool  s24 = 0 == s23;
--     const SWord8 s25 = (s23 == 0) ? s20 : (s20 % s23);
--     const SWord8 s26 = s24 ? s20 : s25;
--     const SBool  s27 = 0 == s26;
--     const SWord8 s28 = (s26 == 0) ? s23 : (s23 % s26);
--     const SWord8 s29 = s27 ? s23 : s28;
--     const SBool  s30 = 0 == s29;
--     const SWord8 s31 = (s29 == 0) ? s26 : (s26 % s29);
--     const SWord8 s32 = s30 ? s26 : s31;
--     const SBool  s33 = 0 == s32;
--     const SWord8 s34 = (s32 == 0) ? s29 : (s29 % s32);
--     const SWord8 s35 = s33 ? s29 : s34;
--     const SBool  s36 = 0 == s35;
--     const SWord8 s37 = s36 ? s32 : s35;
--     const SWord8 s38 = s33 ? s29 : s37;
--     const SWord8 s39 = s30 ? s26 : s38;
--     const SWord8 s40 = s27 ? s23 : s39;
--     const SWord8 s41 = s24 ? s20 : s40;
--     const SWord8 s42 = s21 ? s17 : s41;
--     const SWord8 s43 = s18 ? s14 : s42;
--     const SWord8 s44 = s15 ? s11 : s43;
--     const SWord8 s45 = s12 ? s8 : s44;
--     const SWord8 s46 = s9 ? s5 : s45;
--     const SWord8 s47 = s6 ? s1 : s46;
--     const SWord8 s48 = s3 ? s0 : s47;
--     
--     return s48;
--   }
--   </pre>
genGCDInC :: IO ()


-- | Computing population-counts (number of set bits) and autimatically
--   generating C code.
module Data.SBV.Examples.CodeGeneration.PopulationCount

-- | Given a 64-bit quantity, the simplest (and obvious) way to count the
--   number of bits that are set in it is to simply walk through all the
--   bits and add 1 to a running count. This is slow, as it requires 64
--   iterations, but is simple and easy to convince yourself that it is
--   correct. For instance:
--   
--   <pre>
--   &gt;&gt;&gt; popCountSlow 0x0123456789ABCDEF
--   32 :: SWord8
--   </pre>
popCountSlow :: SWord64 -> SWord8

-- | Faster version. This is essentially the same algorithm, except we go 8
--   bits at a time instead of one by one, by using a precomputed table of
--   population-count values for each byte. This algorithm <i>loops</i>
--   only 8 times, and hence is at least 8 times more efficient.
popCountFast :: SWord64 -> SWord8

-- | Look-up table, containing population counts for all possible 8-bit
--   value, from 0 to 255. Note that we do not "hard-code" the values, but
--   merely use the slow version to compute them.
pop8 :: [SWord8]

-- | States the correctness of faster population-count algorithm, with
--   respect to the reference slow version. (We use yices here as it's
--   quite fast for this problem. Z3 seems to take much longer.) We have:
--   
--   <pre>
--   &gt;&gt;&gt; proveWith yices fastPopCountIsCorrect
--   Q.E.D.
--   </pre>
fastPopCountIsCorrect :: SWord64 -> SBool

-- | Not only we can prove that faster version is correct, but we can also
--   automatically generate C code to compute population-counts for us.
--   This action will generate all the C files that you will need,
--   including a driver program for test purposes.
--   
--   Below is the generated header file for <a>popCountFast</a>:
--   
--   <pre>
--   &gt;&gt;&gt; genPopCountInC
--   == BEGIN: "Makefile" ================
--   # Makefile for popCount. Automatically generated by SBV. Do not edit!
--   
--   # include any user-defined .mk file in the current directory.
--   -include *.mk
--   
--   CC=gcc
--   CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
--   
--   all: popCount_driver
--   
--   popCount.o: popCount.c popCount.h
--   	${CC} ${CCFLAGS} -c $&lt; -o $@
--   
--   popCount_driver.o: popCount_driver.c
--   	${CC} ${CCFLAGS} -c $&lt; -o $@
--   
--   popCount_driver: popCount.o popCount_driver.o
--   	${CC} ${CCFLAGS} $^ -o $@
--   
--   clean:
--   	rm -f *.o
--   
--   veryclean: clean
--   	rm -f popCount_driver
--   == END: "Makefile" ==================
--   == BEGIN: "popCount.h" ================
--   /* Header file for popCount. Automatically generated by SBV. Do not edit! */
--   
--   #ifndef __popCount__HEADER_INCLUDED__
--   #define __popCount__HEADER_INCLUDED__
--   
--   #include &lt;inttypes.h&gt;
--   #include &lt;stdint.h&gt;
--   #include &lt;stdbool.h&gt;
--   #include &lt;math.h&gt;
--   
--   /* The boolean type */
--   typedef bool SBool;
--   
--   /* The float type */
--   typedef float SFloat;
--   
--   /* The double type */
--   typedef double SDouble;
--   
--   /* Unsigned bit-vectors */
--   typedef uint8_t  SWord8 ;
--   typedef uint16_t SWord16;
--   typedef uint32_t SWord32;
--   typedef uint64_t SWord64;
--   
--   /* Signed bit-vectors */
--   typedef int8_t  SInt8 ;
--   typedef int16_t SInt16;
--   typedef int32_t SInt32;
--   typedef int64_t SInt64;
--   
--   /* Entry point prototype: */
--   SWord8 popCount(const SWord64 x);
--   
--   #endif /* __popCount__HEADER_INCLUDED__ */
--   == END: "popCount.h" ==================
--   == BEGIN: "popCount_driver.c" ================
--   /* Example driver program for popCount. */
--   /* Automatically generated by SBV. Edit as you see fit! */
--   
--   #include &lt;inttypes.h&gt;
--   #include &lt;stdint.h&gt;
--   #include &lt;stdbool.h&gt;
--   #include &lt;math.h&gt;
--   #include &lt;stdio.h&gt;
--   #include "popCount.h"
--   
--   int main(void)
--   {
--     const SWord8 __result = popCount(0x1b02e143e4f0e0e5ULL);
--   
--     printf("popCount(0x1b02e143e4f0e0e5ULL) = %"PRIu8"\n", __result);
--   
--     return 0;
--   }
--   == END: "popCount_driver.c" ==================
--   == BEGIN: "popCount.c" ================
--   /* File: "popCount.c". Automatically generated by SBV. Do not edit! */
--   
--   #include &lt;inttypes.h&gt;
--   #include &lt;stdint.h&gt;
--   #include &lt;stdbool.h&gt;
--   #include &lt;math.h&gt;
--   #include "popCount.h"
--   
--   SWord8 popCount(const SWord64 x)
--   {
--     const SWord64 s0 = x;
--     static const SWord8 table0[] = {
--         0, 1, 1, 2, 1, 2, 2, 3, 1, 2, 2, 3, 2, 3, 3, 4, 1, 2, 2, 3, 2, 3,
--         3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4,
--         3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 1, 2,
--         2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5,
--         3, 4, 4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5,
--         5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 1, 2, 2, 3,
--         2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4,
--         4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6,
--         3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 2, 3, 3, 4, 3, 4,
--         4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6,
--         5, 6, 6, 7, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 4, 5,
--         5, 6, 5, 6, 6, 7, 5, 6, 6, 7, 6, 7, 7, 8
--     };
--     const SWord64 s11 = s0 &amp; 0x00000000000000ffULL;
--     const SWord8  s12 = table0[s11];
--     const SWord64 s13 = s0 &gt;&gt; 8;
--     const SWord64 s14 = 0x00000000000000ffULL &amp; s13;
--     const SWord8  s15 = table0[s14];
--     const SWord8  s16 = s12 + s15;
--     const SWord64 s17 = s13 &gt;&gt; 8;
--     const SWord64 s18 = 0x00000000000000ffULL &amp; s17;
--     const SWord8  s19 = table0[s18];
--     const SWord8  s20 = s16 + s19;
--     const SWord64 s21 = s17 &gt;&gt; 8;
--     const SWord64 s22 = 0x00000000000000ffULL &amp; s21;
--     const SWord8  s23 = table0[s22];
--     const SWord8  s24 = s20 + s23;
--     const SWord64 s25 = s21 &gt;&gt; 8;
--     const SWord64 s26 = 0x00000000000000ffULL &amp; s25;
--     const SWord8  s27 = table0[s26];
--     const SWord8  s28 = s24 + s27;
--     const SWord64 s29 = s25 &gt;&gt; 8;
--     const SWord64 s30 = 0x00000000000000ffULL &amp; s29;
--     const SWord8  s31 = table0[s30];
--     const SWord8  s32 = s28 + s31;
--     const SWord64 s33 = s29 &gt;&gt; 8;
--     const SWord64 s34 = 0x00000000000000ffULL &amp; s33;
--     const SWord8  s35 = table0[s34];
--     const SWord8  s36 = s32 + s35;
--     const SWord64 s37 = s33 &gt;&gt; 8;
--     const SWord64 s38 = 0x00000000000000ffULL &amp; s37;
--     const SWord8  s39 = table0[s38];
--     const SWord8  s40 = s36 + s39;
--   
--     return s40;
--   }
--   == END: "popCount.c" ==================
--   </pre>
genPopCountInC :: IO ()


-- | Demonstrates the use of uninterpreted functions for the purposes of
--   code generation. This facility is important when we want to take
--   advantage of native libraries in the target platform, or when we'd
--   like to hand-generate code for certain functions for various purposes,
--   such as efficiency, or reliability.
module Data.SBV.Examples.CodeGeneration.Uninterpreted

-- | A definition of shiftLeft that can deal with variable length shifts.
--   (Note that the ``shiftL`` method from the <a>Bits</a> class requires
--   an <a>Int</a> shift amount.) Unfortunately, this'll generate rather
--   clumsy C code due to the use of tables etc., so we uninterpret it for
--   code generation purposes using the <a>cgUninterpret</a> function.
shiftLeft :: SWord32 -> SWord32 -> SWord32

-- | Test function that uses shiftLeft defined above. When used as a normal
--   Haskell function or in verification the definition is fully used,
--   i.e., no uninterpretation happens. To wit, we have:
--   
--   <pre>
--   &gt;&gt;&gt; tstShiftLeft 3 4 5
--   224 :: SWord32
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; prove $ \x y -&gt; tstShiftLeft x y 0 .== x + y
--   Q.E.D.
--   </pre>
tstShiftLeft :: SWord32 -> SWord32 -> SWord32 -> SWord32

-- | Generate C code for "tstShiftLeft". In this case, SBV will *use* the
--   user given definition verbatim, instead of generating code for it.
--   (Also see the functions <a>cgAddDecl</a>, <a>cgAddLDFlags</a>, and
--   <a>cgAddPrototype</a>.)
genCCode :: IO ()


-- | An implementation of AES (Advanced Encryption Standard), using SBV.
--   For details on AES, see FIPS-197:
--   <a>http://csrc.nist.gov/publications/fips/fips197/fips-197.pdf</a>.
--   
--   We do a T-box implementation, which leads to good C code as we can
--   take advantage of look-up tables. Note that we make virtually no
--   attempt to optimize our Haskell code. The concern here is not with
--   getting Haskell running fast at all. The idea is to program the T-Box
--   implementation as naturally and clearly as possible in Haskell, and
--   have SBV's code-generator generate fast C code automatically.
--   Therefore, we merely use ordinary Haskell lists as our
--   data-structures, and do not bother with any unboxing or strictness
--   annotations. Thus, we achieve the separation of concerns: Correctness
--   via clairty and simplicity and proofs on the Haskell side, performance
--   by relying on SBV's code generator. If necessary, the generated code
--   can be FFI'd back into Haskell to complete the loop.
--   
--   All 3 valid key sizes (128, 192, and 256) as required by the FIPS-197
--   standard are supported.
module Data.SBV.Examples.Crypto.AES

-- | An element of the Galois Field 2^8, which are essentially polynomials
--   with maximum degree 7. They are conveniently represented as values
--   between 0 and 255.
type GF28 = SWord8

-- | Multiplication in GF(2^8). This is simple polynomial multipliation,
--   followed by the irreducible polynomial <tt>x^8+x^4+x^3+x^1+1</tt>. We
--   simply use the <a>pMult</a> function exported by SBV to do the
--   operation.
gf28Mult :: GF28 -> GF28 -> GF28

-- | Exponentiation by a constant in GF(2^8). The implementation uses the
--   usual square-and-multiply trick to speed up the computation.
gf28Pow :: GF28 -> Int -> GF28

-- | Computing inverses in GF(2^8). By the mathematical properties of
--   GF(2^8) and the particular irreducible polynomial used
--   <tt>x^8+x^5+x^3+x^1+1</tt>, it turns out that raising to the 254 power
--   gives us the multiplicative inverse. Of course, we can prove this
--   using SBV:
--   
--   <pre>
--   &gt;&gt;&gt; prove $ \x -&gt; x ./= 0 ==&gt; x `gf28Mult` gf28Inverse x .== 1
--   Q.E.D.
--   </pre>
--   
--   Note that we exclude <tt>0</tt> in our theorem, as it does not have a
--   multiplicative inverse.
gf28Inverse :: GF28 -> GF28

-- | AES state. The state consists of four 32-bit words, each of which is
--   in turn treated as four GF28's, i.e., 4 bytes. The T-Box
--   implementation keeps the four-bytes together for efficient
--   representation.
type State = [SWord32]

-- | The key, which can be 128, 192, or 256 bits. Represented as a sequence
--   of 32-bit words.
type Key = [SWord32]

-- | The key schedule. AES executes in rounds, and it treats first and last
--   round keys slightly differently than the middle ones. We reflect that
--   choice by being explicit about it in our type. The length of the
--   middle list of keys depends on the key-size, which in turn determines
--   the number of rounds.
type KS = (Key, [Key], Key)

-- | Conversion from 32-bit words to 4 constituent bytes.
toBytes :: SWord32 -> [GF28]

-- | Conversion from 4 bytes, back to a 32-bit row, inverse of
--   <a>toBytes</a> above. We have the following simple theorems stating
--   this relationship formally:
--   
--   <pre>
--   &gt;&gt;&gt; prove $ \a b c d -&gt; toBytes (fromBytes [a, b, c, d]) .== [a, b, c, d]
--   Q.E.D.
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; prove $ \r -&gt; fromBytes (toBytes r) .== r
--   Q.E.D.
--   </pre>
fromBytes :: [GF28] -> SWord32

-- | Rotating a state row by a fixed amount to the right.
rotR :: [GF28] -> Int -> [GF28]

-- | Definition of round-constants, as specified in Section 5.2 of the AES
--   standard.
roundConstants :: [GF28]

-- | The <tt>InvMixColumns</tt> transformation, as described in Section
--   5.3.3 of the standard. Note that this transformation is only used
--   explicitly during key-expansion in the T-Box implementation of AES.
invMixColumns :: State -> State

-- | Key expansion. Starting with the given key, returns an infinite
--   sequence of words, as described by the AES standard, Section 5.2,
--   Figure 11.
keyExpansion :: Int -> Key -> [Key]

-- | The values of the AES S-box table. Note that we describe the S-box
--   programmatically using the mathematical construction given in Section
--   5.1.1 of the standard. However, the code-generation will turn this
--   into a mere look-up table, as it is just a constant table, all
--   computation being done at "compile-time".
sboxTable :: [GF28]

-- | The sbox transformation. We simply select from the sbox table. Note
--   that we are obliged to give a default value (here <tt>0</tt>) to be
--   used if the index is out-of-bounds as required by SBV's <a>select</a>
--   function. However, that will never happen since the table has all 256
--   elements in it.
sbox :: GF28 -> GF28

-- | The values of the inverse S-box table. Again, the construction is
--   programmatic.
unSBoxTable :: [GF28]

-- | The inverse s-box transformation.
unSBox :: GF28 -> GF28

-- | Prove that the <a>sbox</a> and <a>unSBox</a> are inverses. We have:
--   
--   <pre>
--   &gt;&gt;&gt; prove sboxInverseCorrect
--   Q.E.D.
--   </pre>
sboxInverseCorrect :: GF28 -> SBool

-- | Adding the round-key to the current state. We simply exploit the fact
--   that addition is just xor in implementing this transformation.
addRoundKey :: Key -> State -> State

-- | T-box table generation function for encryption
t0Func :: GF28 -> [GF28]

-- | First look-up table used in encryption
t0 :: GF28 -> SWord32

-- | Second look-up table used in encryption
t1 :: GF28 -> SWord32

-- | Third look-up table used in encryption
t2 :: GF28 -> SWord32

-- | Fourth look-up table used in encryption
t3 :: GF28 -> SWord32

-- | T-box table generating function for decryption
u0Func :: GF28 -> [GF28]

-- | First look-up table used in decryption
u0 :: GF28 -> SWord32

-- | Second look-up table used in decryption
u1 :: GF28 -> SWord32

-- | Third look-up table used in decryption
u2 :: GF28 -> SWord32

-- | Fourth look-up table used in decryption
u3 :: GF28 -> SWord32

-- | Generic round function. Given the function to perform one round, a
--   key-schedule, and a starting state, it performs the AES rounds.
doRounds :: (Bool -> State -> Key -> State) -> KS -> State -> State

-- | One encryption round. The first argument indicates whether this is the
--   final round or not, in which case the construction is slightly
--   different.
aesRound :: Bool -> State -> Key -> State

-- | One decryption round. Similar to the encryption round, the first
--   argument indicates whether this is the final round or not.
aesInvRound :: Bool -> State -> Key -> State

-- | Key schedule. Given a 128, 192, or 256 bit key, expand it to get
--   key-schedules for encryption and decryption. The key is given as a
--   sequence of 32-bit words. (4 elements for 128-bits, 6 for 192, and 8
--   for 256.)
aesKeySchedule :: Key -> (KS, KS)

-- | Block encryption. The first argument is the plain-text, which must
--   have precisely 4 elements, for a total of 128-bits of input. The
--   second argument is the key-schedule to be used, obtained by a call to
--   <a>aesKeySchedule</a>. The output will always have 4 32-bit words,
--   which is the cipher-text.
aesEncrypt :: [SWord32] -> KS -> [SWord32]

-- | Block decryption. The arguments are the same as in <a>aesEncrypt</a>,
--   except the first argument is the cipher-text and the output is the
--   corresponding plain-text.
aesDecrypt :: [SWord32] -> KS -> [SWord32]

-- | 128-bit encryption test, from Appendix C.1 of the AES standard:
--   
--   <pre>
--   &gt;&gt;&gt; map hex t128Enc
--   ["69c4e0d8","6a7b0430","d8cdb780","70b4c55a"]
--   </pre>
t128Enc :: [SWord32]

-- | 128-bit decryption test, from Appendix C.1 of the AES standard:
--   
--   <pre>
--   &gt;&gt;&gt; map hex t128Dec
--   ["00112233","44556677","8899aabb","ccddeeff"]
--   </pre>
t128Dec :: [SWord32]

-- | 192-bit encryption test, from Appendix C.2 of the AES standard:
--   
--   <pre>
--   &gt;&gt;&gt; map hex t192Enc
--   ["dda97ca4","864cdfe0","6eaf70a0","ec0d7191"]
--   </pre>
t192Enc :: [SWord32]

-- | 192-bit decryption test, from Appendix C.2 of the AES standard:
--   
--   <pre>
--   &gt;&gt;&gt; map hex t192Dec
--   ["00112233","44556677","8899aabb","ccddeeff"]
--   </pre>
t192Dec :: [SWord32]

-- | 256-bit encryption, from Appendix C.3 of the AES standard:
--   
--   <pre>
--   &gt;&gt;&gt; map hex t256Enc
--   ["8ea2b7ca","516745bf","eafc4990","4b496089"]
--   </pre>
t256Enc :: [SWord32]

-- | 256-bit decryption, from Appendix C.3 of the AES standard:
--   
--   <pre>
--   &gt;&gt;&gt; map hex t256Dec
--   ["00112233","44556677","8899aabb","ccddeeff"]
--   </pre>
t256Dec :: [SWord32]

-- | Correctness theorem for 128-bit AES. Ideally, we would run:
--   
--   <pre>
--   prove aes128IsCorrect
--   </pre>
--   
--   to get a proof automatically. Unfortunately, while SBV will
--   successfully generate the proof obligation for this theorem and ship
--   it to the SMT solver, it would be naive to expect the SMT-solver to
--   finish that proof in any reasonable time with the currently available
--   SMT solving technologies. Instead, we can issue:
--   
--   <pre>
--   quickCheck aes128IsCorrect
--   </pre>
--   
--   and get some degree of confidence in our code. Similar predicates can
--   be easily constructed for 192, and 256 bit cases as well.
aes128IsCorrect :: (SWord32, SWord32, SWord32, SWord32) -> (SWord32, SWord32, SWord32, SWord32) -> SBool

-- | Code generation for 128-bit AES encryption.
--   
--   The following sample from the generated code-lines show how T-Boxes
--   are rendered as C arrays:
--   
--   <pre>
--   static const SWord32 table1[] = {
--       0xc66363a5UL, 0xf87c7c84UL, 0xee777799UL, 0xf67b7b8dUL,
--       0xfff2f20dUL, 0xd66b6bbdUL, 0xde6f6fb1UL, 0x91c5c554UL,
--       0x60303050UL, 0x02010103UL, 0xce6767a9UL, 0x562b2b7dUL,
--       0xe7fefe19UL, 0xb5d7d762UL, 0x4dababe6UL, 0xec76769aUL,
--       ...
--       }
--   </pre>
--   
--   The generated program has 5 tables (one sbox table, and 4-Tboxes), all
--   converted to fast C arrays. Here is a sample of the generated
--   straightline C-code:
--   
--   <pre>
--   const SWord8  s1915 = (SWord8) s1912;
--   const SWord8  s1916 = table0[s1915];
--   const SWord16 s1917 = (((SWord16) s1914) &lt;&lt; 8) | ((SWord16) s1916);
--   const SWord32 s1918 = (((SWord32) s1911) &lt;&lt; 16) | ((SWord32) s1917);
--   const SWord32 s1919 = s1844 ^ s1918;
--   const SWord32 s1920 = s1903 ^ s1919;
--   </pre>
--   
--   The GNU C-compiler does a fine job of optimizing this straightline
--   code to generate a fairly efficient C implementation.
cgAES128BlockEncrypt :: IO ()

-- | Components of the AES-128 implementation that the library is generated
--   from
aes128LibComponents :: [(String, SBVCodeGen ())]

-- | Generate a C library, containing functions for performing 128-bit
--   enc<i>dec</i>key-expansion. A note on performance: In a very rough
--   speed test, the generated code was able to do 6.3 million block
--   encryptions per second on a decent MacBook Pro. On the same machine,
--   OpenSSL reports 8.2 million block encryptions per second. So, the
--   generated code is about 25% slower as compared to the highly optimized
--   OpenSSL implementation. (Note that the speed test was done somewhat
--   simplistically, so these numbers should be considered very rough
--   estimates.)
cgAES128Library :: IO ()


-- | An implementation of RC4 (AKA Rivest Cipher 4 or Alleged RC4/ARC4),
--   using SBV. For information on RC4, see:
--   <a>http://en.wikipedia.org/wiki/RC4</a>.
--   
--   We make no effort to optimize the code, and instead focus on a clear
--   implementation. In fact, the RC4 algorithm relies on in-place update
--   of its state heavily for efficiency, and is therefore unsuitable for a
--   purely functional implementation.
module Data.SBV.Examples.Crypto.RC4

-- | RC4 State contains 256 8-bit values. We use the symbolically
--   accessible full-binary type <a>STree</a> to represent the state, since
--   RC4 needs access to the array via a symbolic index and it's important
--   to minimize access time.
type S = STree Word8 Word8

-- | Construct the fully balanced initial tree, where the leaves are simply
--   the numbers <tt>0</tt> through <tt>255</tt>.
initS :: S

-- | The key is a stream of <a>Word8</a> values.
type Key = [SWord8]

-- | Represents the current state of the RC4 stream: it is the <tt>S</tt>
--   array along with the <tt>i</tt> and <tt>j</tt> index values used by
--   the PRGA.
type RC4 = (S, SWord8, SWord8)

-- | Swaps two elements in the RC4 array.
swap :: SWord8 -> SWord8 -> S -> S

-- | Implements the PRGA used in RC4. We return the new state and the next
--   key value generated.
prga :: RC4 -> (SWord8, RC4)

-- | Constructs the state to be used by the PRGA using the given key.
initRC4 :: Key -> S

-- | The key-schedule. Note that this function returns an infinite list.
keySchedule :: Key -> [SWord8]

-- | Generate a key-schedule from a given key-string.
keyScheduleString :: String -> [SWord8]

-- | RC4 encryption. We generate key-words and xor it with the input. The
--   following test-vectors are from Wikipedia
--   <a>http://en.wikipedia.org/wiki/RC4</a>:
--   
--   <pre>
--   &gt;&gt;&gt; concatMap hex $ encrypt "Key" "Plaintext"
--   "bbf316e8d940af0ad3"
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; concatMap hex $ encrypt "Wiki" "pedia"
--   "1021bf0420"
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; concatMap hex $ encrypt "Secret" "Attack at dawn"
--   "45a01f645fc35b383552544b9bf5"
--   </pre>
encrypt :: String -> String -> [SWord8]

-- | RC4 decryption. Essentially the same as decryption. For the above test
--   vectors we have:
--   
--   <pre>
--   &gt;&gt;&gt; decrypt "Key" [0xbb, 0xf3, 0x16, 0xe8, 0xd9, 0x40, 0xaf, 0x0a, 0xd3]
--   "Plaintext"
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; decrypt "Wiki" [0x10, 0x21, 0xbf, 0x04, 0x20]
--   "pedia"
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; decrypt "Secret" [0x45, 0xa0, 0x1f, 0x64, 0x5f, 0xc3, 0x5b, 0x38, 0x35, 0x52, 0x54, 0x4b, 0x9b, 0xf5]
--   "Attack at dawn"
--   </pre>
decrypt :: String -> [SWord8] -> String

-- | Prove that round-trip encryption/decryption leaves the plain-text
--   unchanged. The theorem is stated parametrically over key and
--   plain-text sizes. The expression performs the proof for a 40-bit key
--   (5 bytes) and 40-bit plaintext (again 5 bytes).
--   
--   Note that this theorem is trivial to prove, since it is essentially
--   establishing xor'in the same value twice leaves a word unchanged
--   (i.e., <tt>x <a>xor</a> y <a>xor</a> y = x</tt>). However, the proof
--   takes quite a while to complete, as it gives rise to a fairly large
--   symbolic trace.
rc4IsCorrect :: IO ThmResult


-- | This program demonstrates the use of the existentials and the QBVF
--   (quantified bit-vector solver). We generate CRC polynomials of degree
--   16 that can be used for messages of size 48-bits. The query finds all
--   such polynomials that have hamming distance is at least 4. That is, if
--   the CRC can't tell two different 48-bit messages apart, then they must
--   differ in at least 4 bits.
module Data.SBV.Examples.Existentials.CRCPolynomial

-- | SBV doesn't support 48 bit words natively. So, we represent them as a
--   tuple, 32 high-bits and 16 low-bits.
type SWord48 = (SWord32, SWord16)

-- | Compute the 16 bit CRC of a 48 bit message, using the given polynomial
crc_48_16 :: SWord48 -> SWord16 -> [SBool]

-- | Count the differing bits in the message and the corresponding CRC
diffCount :: (SWord48, [SBool]) -> (SWord48, [SBool]) -> SWord8

-- | Given a hamming distance value <tt>hd</tt>, <a>crcGood</a> returns
--   <tt>true</tt> if the 16 bit polynomial can distinguish all messages
--   that has at most <tt>hd</tt> different bits. Note that we express this
--   conversely: If the <tt>sent</tt> and <tt>received</tt> messages are
--   different, then it must be the case that that must differ from each
--   other (including CRCs), in more than <tt>hd</tt> bits.
crcGood :: SWord8 -> SWord16 -> SWord48 -> SWord48 -> SBool

-- | Generate good CRC polynomials for 48-bit words, given the hamming
--   distance <tt>hd</tt>.
genPoly :: SWord8 -> IO ()

-- | Find and display all degree 16 polynomials with hamming distance at
--   least 4, for 48 bit messages.
--   
--   When run, this function prints:
--   
--   <pre>
--   Polynomial #1. x^16 + x^2 + x + 1
--   Polynomial #2. x^16 + x^15 + x^2 + 1
--   Polynomial #3. x^16 + x^15 + x^14 + 1
--   Polynomial #4. x^16 + x^15 + x^2 + x + 1
--   Polynomial #5. x^16 + x^14 + x + 1
--   ...
--   
--   </pre>
--   
--   Note that different runs can produce different results, depending on
--   the random numbers used by the solver, solver version, etc. (Also, the
--   solver will take some time to generate these results. On my machine,
--   the first five polynomials were generated in about 5 minutes.)
findHD4Polynomials :: IO ()


-- | Finding minimal natural number solutions to linear Diophantine
--   equations, using explicit quantification.
module Data.SBV.Examples.Existentials.Diophantine

-- | For a homogeneous problem, the solution is any linear combination of
--   the resulting vectors. For a non-homogeneous problem, the solution is
--   any linear combination of the vectors in the second component plus one
--   of the vectors in the first component.
data Solution
Homogeneous :: [[Integer]] -> Solution
NonHomogeneous :: [[Integer]] -> [[Integer]] -> Solution

-- | ldn: Solve a (L)inear (D)iophantine equation, returning minimal
--   solutions over (N)aturals. The input is given as a rows of equations,
--   with rhs values separated into a tuple.
ldn :: [([Integer], Integer)] -> IO Solution

-- | Find the basis solution. By definition, the basis has all non-trivial
--   (i.e., non-0) solutions that cannot be written as the sum of two other
--   solutions. We use the mathematically equivalent statement that a
--   solution is in the basis if it's least according to the lexicographic
--   order using the ordinary less-than relation. (NB. We explicitly tell
--   z3 to use the logic AUFLIA for this problem, as the BV solver that is
--   chosen automatically has a performance issue. See:
--   <a>https://z3.codeplex.com/workitem/88.)</a>
basis :: [[SInteger]] -> IO [[Integer]]

-- | Solve the equation:
--   
--   <pre>
--   2x + y - z = 2
--   </pre>
--   
--   We have:
--   
--   <pre>
--   &gt;&gt;&gt; test
--   NonHomogeneous [[0,2,0],[1,0,0]] [[1,0,2],[0,1,1]]
--   </pre>
--   
--   which means that the solutions are of the form:
--   
--   <pre>
--   (1, 0, 0) + k (0, 1, 1) + k' (1, 0, 2) = (1+k', k, k+2k')
--   </pre>
--   
--   OR
--   
--   <pre>
--   (0, 2, 0) + k (0, 1, 1) + k' (1, 0, 2) = (k', 2+k, k+2k')
--   </pre>
--   
--   for arbitrary <tt>k</tt>, <tt>k'</tt>. It's easy to see that these are
--   really solutions to the equation given. It's harder to see that they
--   cover all possibilities, but a moments thought reveals that is indeed
--   the case.
test :: IO Solution

-- | A puzzle: Five sailors and a monkey escape from a naufrage and reach
--   an island with coconuts. Before dawn, they gather a few of them and
--   decide to sleep first and share the next day. At night, however, one
--   of them awakes, counts the nuts, makes five parts, gives the remaining
--   nut to the monkey, saves his share away, and sleeps. All other sailors
--   do the same, one by one. When they all wake up in the morning, they
--   again make 5 shares, and give the last remaining nut to the monkey.
--   How many nuts were there at the beginning?
--   
--   We can model this as a series of diophantine equations:
--   
--   <pre>
--     x_0 = 5 x_1 + 1
--   4 x_1 = 5 x_2 + 1
--   4 x_2 = 5 x_3 + 1
--   4 x_3 = 5 x_4 + 1
--   4 x_4 = 5 x_5 + 1
--   4 x_5 = 5 x_6 + 1
--   </pre>
--   
--   We need to solve for x_0, over the naturals. We have:
--   
--   <pre>
--   &gt;&gt;&gt; sailors
--   [15621,3124,2499,1999,1599,1279,1023]
--   </pre>
--   
--   That is:
--   
--   <pre>
--   * There was a total of 15621 coconuts
--   * 1st sailor: 15621 = 3124*5+1, leaving 15621-3124-1 = 12496
--   * 2nd sailor: 12496 = 2499*5+1, leaving 12496-2499-1 =  9996
--   * 3rd sailor:  9996 = 1999*5+1, leaving  9996-1999-1 =  7996
--   * 4th sailor:  7996 = 1599*5+1, leaving  7996-1599-1 =  6396
--   * 5th sailor:  6396 = 1279*5+1, leaving  6396-1279-1 =  5116
--   * In the morning, they had: 5116 = 1023*5+1.
--   </pre>
--   
--   Note that this is the minimum solution, that is, we are guaranteed
--   that there's no solution with less number of coconuts. In fact, any
--   member of <tt>[15625*k-4 | k &lt;- [1..]]</tt> is a solution, i.e., so
--   are <tt>31246</tt>, <tt>46871</tt>, <tt>62496</tt>, <tt>78121</tt>,
--   etc.
sailors :: IO [Integer]
instance Show Solution


-- | Several examples involving IEEE-754 floating point numbers, i.e.,
--   single precision <a>Float</a> (<a>SFloat</a>) and double precision
--   <a>Double</a> (<a>SDouble</a>) types.
--   
--   Note that arithmetic with floating point is full of surprises; due to
--   precision issues associativity of arithmetic operations typically do
--   not hold. Also, the presence of <tt>NaN</tt> is always something to
--   look out for.
module Data.SBV.Examples.Misc.Floating

-- | Prove that floating point addition is not associative. We have:
--   
--   <pre>
--   &gt;&gt;&gt; prove assocPlus
--   Falsifiable. Counter-example:
--     s0 = -Infinity :: SFloat
--     s1 = Infinity :: SFloat
--     s2 = -9.403955e-38 :: SFloat
--   </pre>
--   
--   Indeed:
--   
--   <pre>
--   &gt;&gt;&gt; let i = 1/0 :: Float
--   
--   &gt;&gt;&gt; ((-i) + i) + (-9.403955e-38) :: Float
--   NaN
--   
--   &gt;&gt;&gt; (-i) + (i + (-9.403955e-38)) :: Float
--   NaN
--   </pre>
--   
--   But keep in mind that <tt>NaN</tt> does not equal itself in the
--   floating point world! We have:
--   
--   <pre>
--   &gt;&gt;&gt; let nan = 0/0 :: Float in nan == nan
--   False
--   </pre>
assocPlus :: SFloat -> SFloat -> SFloat -> SBool

-- | Prove that addition is not associative, even if we ignore
--   <tt>NaN</tt>/<tt>Infinity</tt> values. To do this, we use the
--   predicate <a>isFPPoint</a>, which is true of a floating point number
--   (<a>SFloat</a> or <a>SDouble</a>) if it is neither <tt>NaN</tt> nor
--   <tt>Infinity</tt>. (That is, it's a representable point in the
--   real-number line.)
--   
--   We have:
--   
--   <pre>
--   &gt;&gt;&gt; assocPlusRegular
--   Falsifiable. Counter-example:
--     x = 1.5775295e-30 :: SFloat
--     y = 1.92593e-34 :: SFloat
--     z = -2.1521e-41 :: SFloat
--   </pre>
--   
--   Indeed, we have:
--   
--   <pre>
--   &gt;&gt;&gt; (1.5775295e-30 + 1.92593e-34) + (-2.1521e-41) :: Float
--   1.5777222e-30
--   
--   &gt;&gt;&gt; 1.5775295e-30 + (1.92593e-34 + (-2.1521e-41)) :: Float
--   1.577722e-30
--   </pre>
--   
--   Note the loss of precision in the second expression.
assocPlusRegular :: IO ThmResult

-- | Demonstrate that <tt>a+b = a</tt> does not necessarily mean <tt>b</tt>
--   is <tt>0</tt> in the floating point world, even when we disallow the
--   obvious solution when <tt>a</tt> and <tt>b</tt> are <tt>Infinity.</tt>
--   We have:
--   
--   <pre>
--   &gt;&gt;&gt; nonZeroAddition
--   Falsifiable. Counter-example:
--     a = -4.0 :: SFloat
--     b = 4.5918e-41 :: SFloat
--   </pre>
--   
--   Indeed, we have:
--   
--   <pre>
--   &gt;&gt;&gt; -4.0 + 4.5918e-41 == (-4.0 :: Float)
--   True
--   </pre>
--   
--   But:
--   
--   <pre>
--   &gt;&gt;&gt; 4.5918e-41 == (0 :: Float)
--   False
--   </pre>
nonZeroAddition :: IO ThmResult

-- | The last example illustrates that <tt>a * (1/a)</tt> does not
--   necessarily equal <tt>1</tt>. Again, we protect against division by
--   <tt>0</tt> and <tt>NaN</tt>/<tt>Infinity</tt>.
--   
--   We have:
--   
--   <pre>
--   &gt;&gt;&gt; multInverse
--   Falsifiable. Counter-example:
--     a = 1.3625818045773776e-308 :: SDouble
--   </pre>
--   
--   Indeed, we have:
--   
--   <pre>
--   &gt;&gt;&gt; let a = 1.3625818045773776e-308 :: Double
--   
--   &gt;&gt;&gt; a * (1/a)
--   0.9999999999999999
--   </pre>
multInverse :: IO ThmResult


-- | Illustrates the use of <a>sBranch</a>, as a means of dealing with
--   certain cases of the symbolic-termination problem.
module Data.SBV.Examples.Misc.SBranch

-- | A fast implementation of population-count. Note that SBV already
--   provides this functionality via <a>sbvPopCount</a>, using simple
--   expansion and counting algorithm. <a>sbvPopCount</a> is linear in the
--   size of the input, i.e., a 32-bit word would take 32 additions. This
--   implementation here is <i>faster</i> in the sense that it takes as
--   many additions as there are set-bits in the given word.
--   
--   Of course, the issue is that this definition is recursive, and the
--   usual definition via <a>ite</a> would never symbolically terminate:
--   Recursion is done on the input argument: In each recursive call, we
--   <i>reduce</i> the value <tt>n</tt> to <tt>n .&amp;. (n-1)</tt>. This
--   eliminates one set-bit in the input. However, this claim is far from
--   obvious. By the use of <a>sBranch</a> we tell SBV to call the SMT
--   solver in each test to ensure we only evaluate the branches we need,
--   thus avoiding the symbolic-termination issue. In a sense, the SMT
--   solvers proves that the implementation terminates for all valid
--   inputs.
--   
--   Note that replacing <a>sBranch</a> in this implementation with
--   <a>ite</a> would cause symbolic-termination to loop forever. Of
--   course, this does <i>not</i> mean that <a>sBranch</a> is fast: It is
--   costly to make external calls to the solver for each branch, so use
--   with care.
bitCount :: SWord32 -> SWord8

-- | Prove that the <a>bitCount</a> function implemented here is equivalent
--   to the internal "slower" implementation. We have:
--   
--   <pre>
--   &gt;&gt;&gt; prop
--   Q.E.D.
--   </pre>
prop :: IO ThmResult

-- | Illustrates the use of path-conditions in avoiding infeasible paths in
--   symbolic simulation. If we used <a>ite</a> instead of <a>sBranch</a>
--   in the else-branch of the implementation of <a>path</a> symbolic
--   simulation would have encountered the <a>error</a> call, and hence
--   would have failed. But <a>sBranch</a> keeps track of the path
--   condition, and can successfully determine that this path will never be
--   taken, and hence avoids the problem. Note that we can freely mix/match
--   <a>ite</a> and <a>sBranch</a> calls; path conditions will be tracked
--   in both cases. In fact, use of <a>ite</a> is advisable if we know for
--   a fact that both branches are feasible, as it avoids the external
--   call. <a>sBranch</a> will have the same result, albeit it'll cost
--   more.
path :: SWord8 -> SWord8

-- | Prove that <a>path</a> always produces either <tt>10</tt> or
--   <tt>20</tt>, i.e., symbolic simulation will not fail due to the
--   <a>error</a> call. We have:
--   
--   <pre>
--   &gt;&gt;&gt; pathCheck
--   Q.E.D.
--   </pre>
--   
--   Were we to use <a>ite</a> instead of <a>sBranch</a> in the
--   implementation of <a>path</a>, this expression would have caused an
--   exception to be raised at symbolic simulation time.
pathCheck :: IO ThmResult


-- | Demonstrates use of programmatic model extraction. When programming
--   with SBV, we typically use <a>sat</a>/<a>allSat</a> calls to compute
--   models automatically. In more advanced uses, however, the user might
--   want to use programmable extraction features to do fancier
--   programming. We demonstrate some of these utilities here.
module Data.SBV.Examples.Misc.ModelExtract

-- | A simple function to generate a new integer value, that is not in the
--   given set of values. We also require the value to be non-negative
outside :: [Integer] -> IO SatResult

-- | We now use "outside" repeatedly to generate 10 integers, such that we
--   not only disallow previously generated elements, but also any value
--   that differs from previous solutions by less than 5. Here, we use the
--   <a>getModelValue</a> function. We could have also extracted the
--   dictionary via <a>getModelDictionary</a> and did fancier programming
--   as well, as necessary. We have:
--   
--   <pre>
--   &gt;&gt;&gt; genVals
--   [45,40,35,30,25,20,15,10,5,0]
--   </pre>
genVals :: IO [Integer]


-- | Simple usage of polynomials over GF(2^n), using Rijndael's finite
--   field:
--   <a>http://en.wikipedia.org/wiki/Finite_field_arithmetic#Rijndael.27s_finite_field</a>
--   
--   The functions available are:
--   
--   <ul>
--   <li><i><i>pMult</i></i> GF(2^n) Multiplication</li>
--   <li><i><i>pDiv</i></i> GF(2^n) Division</li>
--   <li><i><i>pMod</i></i> GF(2^n) Modulus</li>
--   <li><i><i>pDivMod</i></i> GF(2^n) Division/Modulus, packed
--   together</li>
--   </ul>
--   
--   Note that addition in GF(2^n) is simply <a>xor</a>, so no custom
--   function is provided.
module Data.SBV.Examples.Polynomials.Polynomials

-- | Helper synonym for representing GF(2^8); which are merely 8-bit
--   unsigned words. Largest term in such a polynomial has degree 7.
type GF28 = SWord8

-- | Multiplication in Rijndael's field; usual polynomial multiplication
--   followed by reduction by the irreducible polynomial. The irreducible
--   used by Rijndael's field is the polynomial <tt>x^8 + x^4 + x^3 + x +
--   1</tt>, which we write by giving it's <i>exponents</i> in SBV. See:
--   <a>http://en.wikipedia.org/wiki/Finite_field_arithmetic#Rijndael.27s_finite_field</a>.
--   Note that the irreducible itself is not in GF28! It has a degree of 8.
--   
--   NB. You can use the <a>showPoly</a> function to print polynomials
--   nicely, as a mathematician would write.
gfMult :: GF28 -> GF28 -> GF28

-- | States that the unit polynomial <tt>1</tt>, is the unit element
multUnit :: GF28 -> SBool

-- | States that multiplication is commutative
multComm :: GF28 -> GF28 -> SBool

-- | States that multiplication is associative, note that associativity
--   proofs are notoriously hard for SAT/SMT solvers
multAssoc :: GF28 -> GF28 -> GF28 -> SBool

-- | States that the usual multiplication rule holds over GF(2^n)
--   polynomials Checks:
--   
--   <pre>
--   if (a, b) = x <a>pDivMod</a> y then x = y <a>pMult</a> a + b
--   </pre>
--   
--   being careful about <tt>y = 0</tt>. When divisor is 0, then quotient
--   is defined to be 0 and the remainder is the numerator. (Note that
--   addition is simply <a>xor</a> in GF(2^8).)
polyDivMod :: GF28 -> GF28 -> SBool

-- | Queries
testGF28 :: IO ()


-- | Solves the following puzzle:
--   
--   <pre>
--   You and a friend pass by a standard coin operated vending machine and you decide to get a candy bar.
--   The price is US $0.95, but after checking your pockets you only have a dollar (US $1) and the machine
--   only takes coins. You turn to your friend and have this conversation:
--     you: Hey, do you have change for a dollar?
--     friend: Let's see. I have 6 US coins but, although they add up to a US $1.15, I can't break a dollar.
--     you: Huh? Can you make change for half a dollar?
--     friend: No.
--     you: How about a quarter?
--     friend: Nope, and before you ask I cant make change for a dime or nickel either.
--     you: Really? and these six coins are all US government coins currently in production? 
--     friend: Yes.
--     you: Well can you just put your coins into the vending machine and buy me a candy bar, and I'll pay you back?
--     friend: Sorry, I would like to but I cant with the coins I have.
--   What coins are your friend holding?
--   </pre>
--   
--   To be fair, the problem has no solution <i>mathematically</i>. But
--   there is a solution when one takes into account that vending machines
--   typically do not take the 50 cent coins!
module Data.SBV.Examples.Puzzles.Coins

-- | We will represent coins with 16-bit words (more than enough precision
--   for coins).
type Coin = SWord16

-- | Create a coin. The argument Int argument just used for naming the
--   coin. Note that we constrain the value to be one of the valid U.S.
--   coin values as we create it.
mkCoin :: Int -> Symbolic Coin

-- | Return all combinations of a sequence of values.
combinations :: [a] -> [[a]]

-- | Constraint 1: Cannot make change for a dollar.
c1 :: [Coin] -> SBool

-- | Constraint 2: Cannot make change for half a dollar.
c2 :: [Coin] -> SBool

-- | Constraint 3: Cannot make change for a quarter.
c3 :: [Coin] -> SBool

-- | Constraint 4: Cannot make change for a dime.
c4 :: [Coin] -> SBool

-- | Constraint 5: Cannot make change for a nickel
c5 :: [Coin] -> SBool

-- | Constraint 6: Cannot buy the candy either. Here's where we need to
--   have the extra knowledge that the vending machines do not take 50 cent
--   coins.
c6 :: [Coin] -> SBool

-- | Solve the puzzle. We have:
--   
--   <pre>
--   &gt;&gt;&gt; puzzle
--   Satisfiable. Model:
--     c1 = 50 :: SWord16
--     c2 = 25 :: SWord16
--     c3 = 10 :: SWord16
--     c4 = 10 :: SWord16
--     c5 = 10 :: SWord16
--     c6 = 10 :: SWord16
--   </pre>
--   
--   i.e., your friend has 4 dimes, a quarter, and a half dollar.
puzzle :: IO SatResult


-- | Consider the sentence:
--   
--   <pre>
--   In this sentence, the number of occurrences of 0 is _, of 1 is _, of 2 is _,
--   of 3 is _, of 4 is _, of 5 is _, of 6 is _, of 7 is _, of 8 is _, and of 9 is _.
--   </pre>
--   
--   The puzzle is to fill the blanks with numbers, such that the sentence
--   will be correct. There are precisely two solutions to this puzzle,
--   both of which are found by SBV successfully.
--   
--   References:
--   
--   <ul>
--   <li>Douglas Hofstadter, Metamagical Themes, pg.
--   27.<ul><li><a>http://www.lboro.ac.uk/departments/ma/gallery/selfref/index.html</a></li></ul></li>
--   </ul>
module Data.SBV.Examples.Puzzles.Counts

-- | We will assume each number can be represented by an 8-bit word, i.e.,
--   can be at most 128.
type Count = SWord8

-- | Given a number, increment the count array depending on the digits of
--   the number
count :: Count -> [Count] -> [Count]

-- | Encoding of the puzzle. The solution is a sequence of 10 numbers for
--   the occurrences of the digits such that if we count each digit, we
--   find these numbers.
puzzle :: [Count] -> SBool

-- | Finds all two known solutions to this puzzle. We have:
--   
--   <pre>
--   &gt;&gt;&gt; counts
--   Solution #1
--   In this sentence, the number of occurrences of 0 is 1, of 1 is 11, of 2 is 2, of 3 is 1, of 4 is 1, of 5 is 1, of 6 is 1, of 7 is 1, of 8 is 1, of 9 is 1.
--   Solution #2
--   In this sentence, the number of occurrences of 0 is 1, of 1 is 7, of 2 is 3, of 3 is 2, of 4 is 1, of 5 is 1, of 6 is 1, of 7 is 2, of 8 is 1, of 9 is 1.
--   Found: 2 solution(s).
--   </pre>
counts :: IO ()


-- | 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?
module Data.SBV.Examples.Puzzles.DogCatMouse

-- | Prints the only solution:
--   
--   <pre>
--   &gt;&gt;&gt; puzzle
--   Solution #1:
--     dog = 3 :: SInteger
--     cat = 41 :: SInteger
--     mouse = 56 :: SInteger
--   This is the only solution.
--   </pre>
puzzle :: IO AllSatResult


-- | A solution to Project Euler problem #185:
--   <a>http://projecteuler.net/index.php?section=problems&amp;id=185</a>
module Data.SBV.Examples.Puzzles.Euler185

-- | The given guesses and the correct digit counts, encoded as a simple
--   list.
guesses :: [(String, SWord8)]

-- | 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.
euler185 :: Symbolic SBool

-- | Print out the solution nicely. We have:
--   
--   <pre>
--   &gt;&gt;&gt; solveEuler185
--   4640261571849533
--   Number of solutions: 1
--   </pre>
solveEuler185 :: IO ()


-- | Solves the magic-square puzzle. An NxN magic square is one where all
--   entries are filled with numbers from 1 to NxN such that sums of all
--   rows, columns and diagonals is the same.
module Data.SBV.Examples.Puzzles.MagicSquare

-- | Use 32-bit words for elements.
type Elem = SWord32

-- | A row is a list of elements
type Row = [Elem]

-- | The puzzle board is a list of rows
type Board = [Row]

-- | Checks that all elements in a list are within bounds
check :: Elem -> Elem -> [Elem] -> SBool

-- | Get the diagonal of a square matrix
diag :: [[a]] -> [a]

-- | Test if a given board is a magic square
isMagic :: Board -> SBool

-- | Group a list of elements in the sublists of length <tt>i</tt>
chunk :: Int -> [a] -> [[a]]

-- | Given <tt>n</tt>, magic <tt>n</tt> prints all solutions to the
--   <tt>nxn</tt> magic square problem
magic :: Int -> IO ()


-- | Solves the NQueens puzzle:
--   <a>http://en.wikipedia.org/wiki/Eight_queens_puzzle</a>
module Data.SBV.Examples.Puzzles.NQueens

-- | A solution is a sequence of row-numbers where queens should be placed
type Solution = [SWord8]

-- | Checks that a given solution of <tt>n</tt>-queens is valid, i.e., no
--   queen captures any other.
isValid :: Int -> Solution -> SBool

-- | Given <tt>n</tt>, it solves the <tt>n-queens</tt> puzzle, printing all
--   possible solutions.
nQueens :: Int -> IO ()


-- | The Sudoku solver, quintessential SMT solver example!
module Data.SBV.Examples.Puzzles.Sudoku

-- | A row is a sequence of 8-bit words, too large indeed for representing
--   1-9, but does not harm
type Row = [SWord8]

-- | A Sudoku board is a sequence of 9 rows
type Board = [Row]

-- | Given a series of elements, make sure they are all different and they
--   all are numbers between 1 and 9
check :: [SWord8] -> SBool

-- | Given a full Sudoku board, check that it is valid
valid :: Board -> SBool

-- | A puzzle is a pair: First is the number of missing elements, second is
--   a function that given that many elements returns the final board.
type Puzzle = (Int, [SWord8] -> Board)

-- | Solve a given puzzle and print the results
sudoku :: Puzzle -> IO ()

-- | Helper function to display results nicely, not really needed, but
--   helps presentation
dispSolution :: Puzzle -> (Bool, [Word8]) -> IO ()

-- | Find all solutions to a puzzle
solveAll :: Puzzle -> IO ()

-- | Find an arbitrary good board
puzzle0 :: Puzzle

-- | A random puzzle, found on the internet..
puzzle1 :: Puzzle

-- | Another random puzzle, found on the internet..
puzzle2 :: Puzzle

-- | Another random puzzle, found on the internet..
puzzle3 :: Puzzle

-- | According to the web, this is the toughest sudoku puzzle ever.. It
--   even has a name: Al Escargot:
--   <a>http://zonkedyak.blogspot.com/2006/11/worlds-hardest-sudoku-puzzle-al.html</a>
puzzle4 :: Puzzle

-- | This one has been called diabolical, apparently
puzzle5 :: Puzzle

-- | The following is nefarious according to
--   <a>http://haskell.org/haskellwiki/Sudoku</a>
puzzle6 :: Puzzle

-- | Solve them all, this takes a fraction of a second to run for each case
allPuzzles :: IO ()


-- | The famous U2 bridge crossing puzzle:
--   <a>http://www.brainj.net/puzzle.php?id=u2</a>
module Data.SBV.Examples.Puzzles.U2Bridge

-- | U2 band members
data U2Member
Bono :: U2Member
Edge :: U2Member
Adam :: U2Member
Larry :: U2Member

-- | Model time using 32 bits
type Time = SWord32

-- | Each member gets an 8-bit id
type SU2Member = SWord8

-- | Bono's ID
bono :: SU2Member

-- | Edge's ID
edge :: SU2Member

-- | Adam's ID
adam :: SU2Member

-- | Larry's ID
larry :: SU2Member

-- | Is this a valid person?
isU2Member :: SU2Member -> SBool

-- | Crossing times for each member of the band
crossTime :: SU2Member -> Time

-- | Location of the flash
type Location = SBool

-- | We represent this side of the bridge as <a>here</a>, and arbitrarily
--   as <a>false</a>
here :: Location

-- | We represent other side of the bridge as <a>there</a>, and arbitrarily
--   as <a>true</a>
there :: Location

-- | The status of the puzzle after each move
data Status
Status :: Time -> Location -> Location -> Location -> Location -> Location -> Status

-- | elapsed time
time :: Status -> Time

-- | location of the flash
flash :: Status -> Location

-- | location of Bono
lBono :: Status -> Location

-- | location of Edge
lEdge :: Status -> Location

-- | location of Adam
lAdam :: Status -> Location

-- | location of Larry
lLarry :: Status -> Location

-- | Start configuration, time elapsed is 0 and everybody is <a>here</a>
start :: Status

-- | Mergeable instance for <a>Status</a> simply walks down the structure
--   fields and merges them.

-- | A puzzle move is modeled as a state-transformer
type Move a = State Status a

-- | Mergeable instance for <a>Move</a> simply pushes the merging the data
--   after run of each branch starting from the same state.

-- | Read the state via an accessor function
peek :: (Status -> a) -> Move a

-- | Given an arbitrary member, return his location
whereIs :: SU2Member -> Move SBool

-- | Transferring the flash to the other side
xferFlash :: Move ()

-- | Transferring a person to the other side
xferPerson :: SU2Member -> Move ()

-- | Increment the time, when only one person crosses
bumpTime1 :: SU2Member -> Move ()

-- | Increment the time, when two people cross together
bumpTime2 :: SU2Member -> SU2Member -> Move ()

-- | Symbolic version of <tt>when</tt>
whenS :: SBool -> Move () -> Move ()

-- | Move one member, remembering to take the flash
move1 :: SU2Member -> Move ()

-- | Move two members, again with the flash
move2 :: SU2Member -> SU2Member -> Move ()

-- | A move action is a sequence of triples. The first component is
--   symbolically True if only one member crosses. (In this case the third
--   element of the triple is irrelevant.) If the first component is
--   (symbolically) False, then both members move together
type Actions = [(SBool, SU2Member, SU2Member)]

-- | Run a sequence of given actions.
run :: Actions -> Move [Status]

-- | Check if a given sequence of actions is valid, i.e., they must all
--   cross the bridge according to the rules and in less than 17 seconds
isValid :: Actions -> SBool

-- | The SatModel instance makes it easy to build models, mapping words to
--   U2 members in the way we designated.

-- | See if there is a solution that has precisely <tt>n</tt> steps
solveN :: Int -> IO Bool

-- | Solve the U2-bridge crossing puzzle, starting by testing solutions
--   with increasing number of steps, until we find one. We have:
--   
--   <pre>
--   &gt;&gt;&gt; solveU2
--   Checking for solutions with 1 move.
--   Checking for solutions with 2 moves.
--   Checking for solutions with 3 moves.
--   Checking for solutions with 4 moves.
--   Checking for solutions with 5 moves.
--   Solution #1: 
--    0 --&gt; Edge, Bono
--    2 &lt;-- Edge
--    4 --&gt; Larry, Adam
--   14 &lt;-- Bono
--   15 --&gt; Edge, Bono
--   Total time: 17
--   Solution #2: 
--    0 --&gt; Edge, Bono
--    2 &lt;-- Bono
--    3 --&gt; Larry, Adam
--   13 &lt;-- Edge
--   15 --&gt; Edge, Bono
--   Total time: 17
--   Found: 2 solutions with 5 moves.
--   </pre>
--   
--   Finding all possible solutions to the puzzle.
solveU2 :: IO ()
instance Show U2Member
instance Enum U2Member
instance SatModel U2Member
instance Mergeable a => Mergeable (Move a)
instance Mergeable Status


-- | Formalizes and proves the following theorem, about arithmetic,
--   uninterpreted functions, and arrays. (For reference, see
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3/fmcad06-slides.pdf</a>
--   slide number 24):
--   
--   <pre>
--   x + 2 = y  implies  f (read (write (a, x, 3), y - 2)) = f (y - x + 1)
--   </pre>
--   
--   We interpret the types as follows (other interpretations certainly
--   possible):
--   
--   <ul>
--   <li><i><i>x</i></i> <a>SWord32</a> (32-bit unsigned
--   address)<ul><li><i><i>y</i></i> <a>SWord32</a> (32-bit unsigned
--   address)</li><li><i><i>a</i></i> An array, indexed by 32-bit
--   addresses, returning 32-bit unsigned integers</li><li><i><i>f</i></i>
--   An uninterpreted function of type <tt><a>SWord32</a> -&gt;
--   <a>SWord64</a></tt></li></ul></li>
--   </ul>
--   
--   The function <tt>read</tt> and <tt>write</tt> are usual array
--   operations.
module Data.SBV.Examples.Uninterpreted.AUF

-- | The array type, takes symbolic 32-bit unsigned indexes and stores
--   32-bit unsigned symbolic values. These are functional arrays where
--   reading before writing a cell throws an exception.
type A = SFunArray Word32 Word32

-- | Uninterpreted function in the theorem
f :: SWord32 -> SWord64

-- | Correctness theorem. We state it for all values of <tt>x</tt>,
--   <tt>y</tt>, and the array <tt>a</tt>. We also take an arbitrary
--   initializer for the array.
thm1 :: SWord32 -> SWord32 -> A -> SWord32 -> SBool

-- | Prints Q.E.D. when run, as expected
--   
--   <pre>
--   &gt;&gt;&gt; proveThm1
--   Q.E.D.
--   </pre>
proveThm1 :: IO ()

-- | This version directly uses SMT-arrays and hence does not need an
--   initializer. Reading an element before writing to it returns an
--   arbitrary value.
type B = SArray Word32 Word32

-- | Same as <a>thm1</a>, except we don't need an initializer with the
--   <a>SArray</a> model.
thm2 :: SWord32 -> SWord32 -> B -> SBool

-- | Prints Q.E.D. when run, as expected:
--   
--   <pre>
--   &gt;&gt;&gt; proveThm2
--   Q.E.D.
--   </pre>
proveThm2 :: IO ()


-- | Demonstrates uninterpreted sorts and how they can be used for
--   deduction. This example is inspired by the discussion at
--   <a>http://stackoverflow.com/questions/10635783/using-axioms-for-deductions-in-z3</a>,
--   essentially showing how to show the required deduction using SBV.
module Data.SBV.Examples.Uninterpreted.Deduce

-- | The uninterpreted sort <a>B</a>, corresponding to the carrier.
data B
B :: B

-- | Default instance declaration for <a>SymWord</a>

-- | Default instance declaration for <a>HasKind</a>

-- | Handy shortcut for the type of symbolic values over <a>B</a>
type SB = SBV B

-- | Uninterpreted logical connective <a>and</a>
and :: SB -> SB -> SB

-- | Uninterpreted logical connective <a>or</a>
or :: SB -> SB -> SB

-- | Uninterpreted logical connective <a>not</a>
not :: SB -> SB

-- | Distributivity of OR over AND, as an axiom in terms of the
--   uninterpreted functions we have introduced. Note how variables range
--   over the uninterpreted sort <a>B</a>.
ax1 :: [String]

-- | One of De Morgan's laws, again as an axiom in terms of our
--   uninterpeted logical connectives.
ax2 :: [String]

-- | Double negation axiom, similar to the above.
ax3 :: [String]

-- | Proves the equivalence <tt>NOT (p OR (q AND r)) == (NOT p AND NOT q)
--   OR (NOT p AND NOT r)</tt>, following from the axioms we have specified
--   above. We have:
--   
--   <pre>
--   &gt;&gt;&gt; test
--   Q.E.D.
--   </pre>
test :: IO ThmResult
instance Typeable B
instance Eq B
instance Ord B
instance Data B
instance HasKind B
instance SymWord B


-- | Demonstrates function counter-examples
module Data.SBV.Examples.Uninterpreted.Function

-- | An uninterpreted function
f :: SWord8 -> SWord8 -> SWord16

-- | Asserts that <tt>f x z == f (y+2) z</tt> whenever <tt>x == y+2</tt>.
--   Naturally correct:
--   
--   <pre>
--   &gt;&gt;&gt; prove thmGood
--   Q.E.D.
--   </pre>
thmGood :: SWord8 -> SWord8 -> SWord8 -> SBool

-- | Asserts that <tt>f</tt> is commutative; which is not necessarily true!
--   Indeed, the SMT solver returns a counter-example function that is not
--   commutative. (Note that we have to use Yices as Z3 function
--   counterexamples are not yet supported by sbv.) We have:
--   
--   <pre>
--   &gt;&gt;&gt; proveWith yicesSMT09 $ forAll ["x", "y"] thmBad
--   Falsifiable. Counter-example:
--     x = 0 :: SWord8
--     y = 128 :: SWord8
--     -- uninterpreted: f
--          f 128 0 = 32768
--          f _   _ = 0
--   </pre>
--   
--   Note how the counterexample function <tt>f</tt> returned by Yices
--   violates commutativity; thus providing evidence that the asserted
--   theorem is not valid.
thmBad :: SWord8 -> SWord8 -> SBool

-- | Old version of Yices, which supports nice output for uninterpreted
--   functions.
yicesSMT09 :: SMTConfig


-- | Proves (instances of) Shannon's expansion theorem and other relevant
--   facts. See: <a>http://en.wikipedia.org/wiki/Shannon's_expansion</a>
module Data.SBV.Examples.Uninterpreted.Shannon

-- | A ternary boolean function
type Ternary = SBool -> SBool -> SBool -> SBool

-- | A binary boolean function
type Binary = SBool -> SBool -> SBool

-- | Positive Shannon cofactor of a boolean function, with respect to its
--   first argument
pos :: (SBool -> a) -> a

-- | Negative Shannon cofactor of a boolean function, with respect to its
--   first argument
neg :: (SBool -> a) -> a

-- | Shannon's expansion over the first argument of a function. We have:
--   
--   <pre>
--   &gt;&gt;&gt; shannon
--   Q.E.D.
--   </pre>
shannon :: IO ThmResult

-- | Alternative form of Shannon's expansion over the first argument of a
--   function. We have:
--   
--   <pre>
--   &gt;&gt;&gt; shannon2
--   Q.E.D.
--   </pre>
shannon2 :: IO ThmResult

-- | Computing the derivative of a boolean function (boolean difference).
--   Defined as exclusive-or of Shannon cofactors with respect to that
--   variable.
derivative :: Ternary -> Binary

-- | The no-wiggle theorem: If the derivative of a function with respect to
--   a variable is constant False, then that variable does not "wiggle" the
--   function; i.e., any changes to it won't affect the result of the
--   function. In fact, we have an equivalence: The variable only changes
--   the result of the function iff the derivative with respect to it is
--   not False:
--   
--   <pre>
--   &gt;&gt;&gt; noWiggle
--   Q.E.D.
--   </pre>
noWiggle :: IO ThmResult

-- | Universal quantification of a boolean function with respect to a
--   variable. Simply defined as the conjunction of the Shannon cofactors.
universal :: Ternary -> Binary

-- | Show that universal quantification is really meaningful: That is, if
--   the universal quantification with respect to a variable is True, then
--   both cofactors are true for those arguments. Of course, this is a
--   trivial theorem if you think about it for a moment, or you can just
--   let SBV prove it for you:
--   
--   <pre>
--   &gt;&gt;&gt; univOK
--   Q.E.D.
--   </pre>
univOK :: IO ThmResult

-- | Existential quantification of a boolean function with respect to a
--   variable. Simply defined as the conjunction of the Shannon cofactors.
existential :: Ternary -> Binary

-- | Show that existential quantification is really meaningful: That is, if
--   the existential quantification with respect to a variable is True,
--   then one of the cofactors must be true for those arguments. Again,
--   this is a trivial theorem if you think about it for a moment, but we
--   will just let SBV prove it:
--   
--   <pre>
--   &gt;&gt;&gt; existsOK
--   Q.E.D.
--   </pre>
existsOK :: IO ThmResult


-- | Demonstrates uninterpreted sorts, together with axioms.
module Data.SBV.Examples.Uninterpreted.Sort

-- | A new data-type that we expect to use in an uninterpreted fashion in
--   the backend SMT solver. Note the custom <tt>deriving</tt> clause,
--   which takes care of most of the boilerplate.
data Q
Q :: Q

-- | We need <a>SymWord</a> and <a>HasKind</a> instances, but default
--   definitions are always sufficient for uninterpreted sorts, so all we
--   do is to declare them as such. Note that, starting with GHC 7.6.1, we
--   will be able to simply derive these classes as well. (See
--   <a>http://hackage.haskell.org/trac/ghc/ticket/5462</a>.)

-- | <a>HasKind</a> instance is again straightforward, no specific
--   implementation needed.

-- | Declare an uninterpreted function that works over Q's
f :: SBV Q -> SBV Q

-- | A satisfiable example, stating that there is an element of the domain
--   <a>Q</a> such that <a>f</a> returns a different element. Note that
--   this is valid only when the domain <a>Q</a> has at least two elements.
--   We have:
--   
--   <pre>
--   &gt;&gt;&gt; t1
--   Satisfiable. Model:
--     x = Q!val!0 :: Q
--   </pre>
t1 :: IO SatResult

-- | This is a variant on the first example, except we also add an axiom
--   for the sort, stating that the domain <a>Q</a> has only one element.
--   In this case the problem naturally becomes unsat. We have:
--   
--   <pre>
--   &gt;&gt;&gt; t2
--   Unsatisfiable
--   </pre>
t2 :: IO SatResult
instance Typeable Q
instance Eq Q
instance Ord Q
instance Data Q
instance HasKind Q
instance SymWord Q


-- | Demonstrates uninterpreted sorts and how all-sat behaves for them.
--   Thanks to Eric Seidel for the idea.
module Data.SBV.Examples.Uninterpreted.UISortAllSat

-- | A "list-like" data type, but one we plan to uninterpret at the SMT
--   level. The actual shape is really immaterial for us, but could be used
--   as a proxy to generate test cases or explore data-space in some other
--   part of a program. Note that we neither rely on the shape of this
--   data, nor need the actual constructors.
data L
Nil :: L
Cons :: Int -> L -> L

-- | Declare instances to make <a>L</a> a usable uninterpreted sort. First
--   we need the <a>SymWord</a> instance, with the default definition
--   sufficing.

-- | Similarly, <a>HasKind</a>s default implementation is sufficient.

-- | An uninterpreted "classify" function. Really, we only care about the
--   fact that such a function exists, not what it does.
classify :: SBV L -> SInteger

-- | Formulate a query that essentially asserts a cardinality constraint on
--   the uninterpreted sort <a>L</a>. The goal is to say there are
--   precisely 3 such things, as it might be the case. We manage this by
--   declaring four elements, and asserting that for a free variable of
--   this sort, the shape of the data matches one of these three instances.
--   That is, we assert that all the instances of the data <a>L</a> can be
--   classified into 3 equivalence classes. Then, allSat returns all the
--   possible instances, which of course are all uninterpreted.
--   
--   As expected, we have:
--   
--   <pre>
--   &gt;&gt;&gt; genLs
--   Solution #1:
--     l = L!val!0 :: L
--     l0 = L!val!0 :: L
--     l1 = L!val!1 :: L
--     l2 = L!val!2 :: L
--   Solution #2:
--     l = L!val!2 :: L
--     l0 = L!val!0 :: L
--     l1 = L!val!1 :: L
--     l2 = L!val!2 :: L
--   Solution #3:
--     l = L!val!1 :: L
--     l0 = L!val!0 :: L
--     l1 = L!val!1 :: L
--     l2 = L!val!2 :: L
--   Found 3 different solutions.
--   </pre>
genLs :: IO AllSatResult
instance Typeable L
instance Eq L
instance Ord L
instance Data L
instance HasKind L
instance SymWord L