sbv: Symbolic bit vectors: Bit-precise verification and automatic C-code generation.

SBV: Symbolic Bit Vectors in Haskell
====================================

Express properties about bit-precise Haskell programs and automatically prove
them using SMT solvers.

```haskell
        $ ghci -XScopedTypeVariables
        Prelude> :m Data.SBV
        Prelude Data.SBV> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x
        Q.E.D.
        Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x
        Falsifiable. Counter-example:
          x = 128 :: SWord8
```

The function `prove` has the following type:
    
```haskell
        prove :: Provable a => a -> IO ThmResult
```

The class `Provable` 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 (`sat` and `allSat`) are also provided.
In addition, functions using the SBV library can be compiled to C automatically.

Resources
=========
The sbv library is hosted at [http://github.com/LeventErkok/sbv](http://github.com/LeventErkok/sbv).

The hackage site
[http://hackage.haskell.org/package/sbv](http://hackage.haskell.org/package/sbv) is the best place
for details on the API and the example use cases.

Comments, bug reports, and patches are always welcome.

Overview
========
The Haskell sbv library provides support for dealing with Symbolic Bit Vectors
in Haskell. It introduces the types:

  - `SBool`: Symbolic Booleans (bits)
  - `SWord8`, `SWord16`, `SWord32`, `SWord64`: Symbolic Words (unsigned)
  - `SInt8`,  `SInt16`,  `SInt32`,  `SInt64`: Symbolic Ints (signed)
  - `SInteger`: Symbolic unbounded integers (signed)
  - Arrays of symbolic values
  - Symbolic polynomials over GF(2^n ), polynomial arithmetic, and CRCs
  - Uninterpreted constants and functions over symbolic values, with user
    defined SMT-Lib axioms

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 `Num`, `Bits`, (custom versions of) `Eq` and `Ord`, along with several
other custom classes for simplifying bit-precise programming with symbolic values. The
framework takes full advantage of Haskell's type inference to avoid many common mistakes.

Furthermore, functions built out of these types can also be:

  - proven correct via an external SMT solver (the `prove` function)
  - checked for satisfiability (the `sat`, and `allSat` functions)
  - used in synthesis (the `sat` function with existentials)
  - optimized with respect to cost functions (the 'optimize', 'maximize', and 'minimize' functions)
  - quick-checked
  - used in concrete test case generation (the 'genTest' function)

If a predicate is not valid, `prove` will return a counterexample: An 
assignment to inputs such that the predicate fails. The `sat` function will
return a satisfying assignment, if there is one. The `allSat` function returns
all satisfying assignments, lazily.

The SBV library can also compile Haskell functions that manipulate symbolic
values directly to C, rendering them as straight-line C programs.

Use of SMT solvers
==================
The sbv library uses third-party SMT solvers via the standard SMT-Lib interface: 
[http://goedel.cs.uiowa.edu/smtlib/](http://goedel.cs.uiowa.edu/smtlib/)

The SBV library is designed to work with any SMT-Lib compliant SMT-solver, although integration with
individual solvers require some library work.
Currently, we fully support the [Yices](http://yices.csl.sri.com) SMT solver from SRI,
and the [Z3](http://research.microsoft.com/en-us/um/redmond/projects/z3/)
SMT solver from Microsoft.
Both solvers are available for Windows, Linux, and Mac OSX.

Prerequisites
=============
You **should** [download](http://yices.csl.sri.com/download-yices2.shtml)
and install Yices (version 2.X) on your machine, and
make sure the "yices" executable is in your path before using the sbv library,
as it is the current default solver. Alternatively, you can specify the location
of yices executable in the environment variable `SBV_YICES` and the options to yices
in `SBV_YICES_OPTIONS`. The default for the latter is `"-m -f"`.

SBV can also use Microsoft's Z3 SMT solver as a
backend [(download)](http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html).
The environment variables `SBV_Z3` and `SBV_Z3_OPTIONS` can be used for choosing executable location
and custom options.  The default for the latter is `"/in /smt2"` on Windows and `"-in -smt2"`
on Mac and Linux. You should download Z3 version 3.2 or later.

Examples
=========
Please see the files under the
[Examples](http://github.com/LeventErkok/sbv/tree/master/Data/SBV/Examples)
directory for a number of interesting applications and use cases. Amongst others,
it contains solvers for Sudoku and N-Queens puzzles as mandatory SMT solver examples in
the Puzzles directory.

Installation
============
The sbv library is cabalized. Assuming you have cabal/ghc installed, it should merely
be a matter of running 
     
         cabal install sbv
	 
Please see [INSTALL](http://github.com/LeventErkok/sbv/tree/master/INSTALL) for installation details.

Once the installation is done, you can run the executable `SBVUnitTests` which will
execute the regression test suite for sbv on your machine to ensure all is well.

Copyright, License
==================
The sbv library is distributed with the BSD3 license. See [COPYRIGHT](http://github.com/LeventErkok/sbv/tree/master/COPYRIGHT) for
details. The [LICENSE](http://github.com/LeventErkok/sbv/tree/master/LICENSE) file contains
the [BSD3](http://en.wikipedia.org/wiki/BSD_licenses) verbiage.

Thanks
======
The following people reported bugs, provided comments/feedback, or contributed to the development of SBV in various ways:
Ian Blumenfeld, Ian Calvert, Iavor Diatchki, Tom Hawkins, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson,
and Nis Wegmann.