Q package:sbv
Monad for querying a solver.
A new data-type that we expect to use in an uninterpreted fashion in
the backend SMT solver.
Quantifier-free formulas over the theory of bitvectors and bitvector
arrays.
Quantifier-free formulas over the theory of bitvectors and bitvector
arrays extended with free sort and function symbols.
Quantifier-free linear formulas over the theory of integer arrays
extended with free sort and function symbols.
Quantifier-free formulas over the theory of arrays with
extensionality.
Quantifier-free formulas over the theory of fixed-size bitvectors.
Quantifier-free finite domains.
Quantifier-free formulas over the theory of floating point numbers.
Quantifier-free formulas over the theory of floating point numbers,
arrays, and bit-vectors.
Difference Logic over the integers. Boolean combinations of
inequations of the form x - y < b where x and y are integer
variables and b is an integer constant.
Unquantified linear integer arithmetic. In essence, Boolean
combinations of inequations between linear polynomials over integer
variables.
Unquantified linear real arithmetic. In essence, Boolean combinations
of inequations between linear polynomials over real variables.
Quantifier-free integer arithmetic.
Quantifier-free real arithmetic.
Difference Logic over the reals. In essence, Boolean combinations of
inequations of the form x - y < b where x and y are real variables
and b is a rational constant.
Quantifier-free formulas over the theory of strings.
Unquantified formulas built over a signature of uninterpreted (i.e.,
free) sort and function symbols.
Unquantified formulas over bitvectors with uninterpreted sort function
and symbols.
Difference Logic over the integers (in essence) but with uninterpreted
sort and function symbols.
Unquantified linear integer arithmetic with uninterpreted sort and
function symbols.
Unquantified linear real arithmetic with uninterpreted sort and
function symbols.
Unquantified non-linear real integer arithmetic with uninterpreted
sort and function symbols.