Express properties about Haskell programs and automatically prove them using SMT solvers.
$ ghci ghci> :m Data.SBV ghci> prove $ \x -> x `shiftL` 2 .== 4 * (x::SWord8) Q.E.D. ghci> prove $ \x -> x `shiftL` 2 .== 2 * (x::SWord8) Falsifiable. Counter-example: s0 = 32 :: Word8
prove establishes theorem-hood, while
sat finds any satisfying model. All satisfying models can be computed using
allSat. SBV can also perform static assertion checks, such as absence of division-by-0, and other user given properties. Furthermore, SBV can perform
optimization, minimizing/maximizing arithmetic goals for their optimal values.
SBV also allows for an incremental mode: Users are given a handle to the SMT solver as their programs execute, and they can issue SMTLib commands
programmatically, query values, and direct the interaction using a high-level typed API. The incremental mode also allows for creation of constraints
based on the current model, and access to internals of SMT solvers for advanced users. See the
query commands for details.
SBV library provides support for dealing with symbolic values in Haskell. It introduces the types:
SBool: Symbolic Booleans (bits).
SWord64: Symbolic Words (unsigned).
SInt64: Symbolic Ints (signed).
SInteger: Symbolic unbounded integers (signed).
SReal: Symbolic infinite precision algebraic reals (signed).
SFloat: IEEE-754 single precision floating point number. (
SDouble: IEEE-754 double precision floating point number. (
SChar: Symbolic characters. (Currently Latin-1, but will be unicode in the future.)
SString: Symbolic strings.
SInt4as needed. (In a future version of SBV, we plan to support these automatically.)
The user can construct ordinary Haskell programs using these types, which behave like ordinary Haskell values when used concretely. However, when used with symbolic arguments, functions built out of these types can also be:
satfunction with existentials),
The SBV library uses third-party SMT solvers via the standard SMT-Lib interface. The following solvers are supported:
Most functions have two variants: For instance
proveWith. The former uses the default solver, which is currently Z3.
The latter expects you to pass it a configuration that picks the solver. The valid values are
See versions for a listing of the versions of these tools SBV has been tested with. Please report if you see any discrepancies!
Other SMT solvers can be used with SBV as well, with a relatively easy hook-up mechanism. Please do get in touch if you plan to use SBV with any other solver.
SBV also allows for running multiple solvers at the same time, either picking the result of the first to complete, or getting results from all. See
satWithAll functions. The function
sbvAvailableSolvers can be used to query the available solvers at run-time.
The following people reported bugs, provided comments/feedback, or contributed to the development of SBV in various ways: Ara Adkins, Kanishka Azimi, Reid Barton, Ian Blumenfeld, Martin Brain, Joel Burget, Ian Calvert, Oliver Charles, Christian Conkle, Matthew Danish, Iavor Diatchki, Robert Dockins, Thomas DuBuisson, Trevor Elliott, John Erickson, Adam Foltzer, Joshua Gancher, Remy Goldschmidt, Brad Hardy, Tom Hawkins, Greg Horn, Brian Huffman, Joe Leslie-Hurd, Georges-Axel Jaloyan, Anders Kaseorg, Tom Sydney Kerckhove, Piërre van de Laar, Brett Letner, Georgy Lukyanov, John Matthews, Philipp Meyer, Jan Path, Matt Peddie, Matthew Pickering, Lee Pike, Gleb Popov, Rohit Ramesh, Geoffrey Ramseyer, Stephan Renatus, Dan Rosén, Brian Schroeder, Eric Seidel, Austin Seipp, Andrés Sicard-Ramírez, Don Stewart, Josef Svenningsson, Daniel Wagner, Sean Weaver, Nis Wegmann, and Jared Ziegler. Thanks!