SMT-LIB Logics (Version 1)

Note. The theories below are superseded by those defined in Version 2 of SMT-LIB. They are listed here for historical purposes. Their use is deprecated.

Click on the logic's name to see its declaration in SMT-LIB format.

AUFLIA:

Closed linear formulas over the theory of integer arrays with free sort, function and predicate symbols.

AUFLIRA:

Closed linear formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value.

AUFNIRA:

Closed formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value.

LIA:

Closed linear formulas over linear integer arithmetic.

LRA:

Closed linear formulas in linear real arithmetic.

QF_A:

Closed quantifier-free formulas over the theory of arrays without extensionality.

QF_AUFBV:

Closed quantifier-free formulas over the theory of bitvectors and bitvector arrays with free function and predicate symbols.

QF_AUFLIA:

Closed quantifier-free and linear formulas over the theory of integer arrays with free sort, function and predicate symbols.

QF_AX:

Closed quantifier-free formulas over the theory of arrays with extensionality.

QF_BV:

Closed quantifier-free formulas over the theory of fixed-size bitvectors.

QF_IDL:

Difference Logic over the integers. In essence, Boolean combinations of inequations of the form x - y < b where x and y are integer variables and b is an integer constant.

QF_LIA:

Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables.

QF_LRA:

Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables.

QF_NIA:

Unquantified non-linear integer arithmetic. In essence, Boolean combinations of inequations between polynomials over integer variables, with at least one non-linear polynomial.

QF_RDL:

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.

QF_UF:

Unquantified formulas built over a signature of uninterpreted sort, function and predicate symbols.

QF_UFIDL:

Difference Logic over the integers (in essence) but with uninterpreted sort, function, and predicate symbols.

QF_UFBV:

Unquantified formulas over bitvectors with uninterpreted function and predicate symbols.

QF_UFBV[32] (now deprecated):

Unquantified formulas over bit vectors of size up to 32 bits, with uninterpreted function, and predicate symbols. This logic remains for historical purposes. The preferred logic for current use is now one of QF_BV or QF_UFBV.

QF_UFLIA:

Unquantified linear integer arithmetic with uninterpreted sort, function, and predicate symbols.

QF_UFLRA:

Unquantified linear real arithmetic with uninterpreted sort, function, and predicate symbols.

QF_UFNRA:

Unquantified non-linear real arithmetic with uninterpreted sort, function, and predicate symbols.

UFNIA:

Non-linear integer arithmetic with uninterpreted sort, function, and predicate symbols.