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.
The quotient
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.