SMT Logics

The following table lists the names of all the official SMT-LIB logics at http://smt-lib.org (as of January 2015) and indicates whether Yices supports them. Currently, Yices supports most quantifier-free SMT-LIB logics. Nonlinear real arithmetic is supported by using the MCSAT solver of Yices.

Logic name Description Supported
ALIA Arrays, Linear Integer Arithmetic, Quantifiers No
AUFLIA Arrays, Uninterpreted Functions, Linear Integer Arithmetic, Quantifiers No
AUFLIRA Arrays, Uninterpreted Functions, Mixed Linear Arithmetic, Quantifiers No
AUFNIRA Arrays, Uninterpreted Functions, Mixed Nonlinear Arithmetic, Quantifiers No
LIA Linear Integer Arithmetic, Quantifiers No
LRA Linear Real Arithmetic, Quantifiers No
NIA Nonlinear Integer Arithmetic, Quantifiers No
NRA Nonlinear Real Arithmetic, Quantifiers No
QF_ABV Arrays and Bitvectors Yes
QF_ALIA Arrays and Linear Integer Arithmetic Yes
QF_AUFBV Arrays, Uninterpreted Functions, and Bitvectors Yes
QF_AUFLIA Arrays, Uninterpreted Functions, and Linear Integer Arithmetic Yes
QF_AX Arrays (with extensionality) Yes
QF_BV Bitvectors Yes
QF_IDL Integer Difference Logic Yes
QF_LIA Linear Integer Arithmetic Yes
QF_LRA Linear Real Arithmetic Yes
QF_NIA Nonlinear Integer Arithmetic Yes
QF_NIRA Mixed Nonlinear Arithmetic Yes
QF_NRA Nonlinear Real Arithmetic Yes
QF_RDL Real Difference Logic Yes
QF_UF Uninterpreted Functions Yes
QF_UFBV Uninterpreted Functions and Bitvectors Yes
QF_UFIDL Uninterpreted Functions and Integer Difference Logic Yes
QF_UFLIA Uninterpreted Functions and Linear Integer Arithmetic Yes
QF_UFLRA Uninterpreted Functions and Linear Real Arithmetic Yes
QF_UFNIA Uninterpreted Functions and Nonlinear Integer Arithmetic Yes
QF_UFNIRA Uninterpreted Functions and Mixed Nonlinear Arithmetic Yes
QF_UFNRA Uninterpreted Functions and Nonlinear Real Arithmetic Yes
UFLRA Uninterpreted Functions, Linear Real Arithmetic, Quantifiers No
UFNIA Uninterpreted Functions, Nonlinear Integer Arithmetic, Quantifiers No

Yices also recognizes and supports some logic names that are not officially part of SMT-LIB.

Logic name Description
QF_ALRA Arrays and Linear Real Arithmetic
QF_ALIRA Arrays and Mixed Linear Arithmetic
QF_AUF Arrays and Uninterpreted Functions
QF_AUFLRA Arrays, Uninterpreted Functions, Linear Real Arithmetic
QF_AUFLIRA Arrays, Uninterpreted Functions, Mixed Linear Arithmetic
QF_LIRA Mixed Linear Arithmetic
QF_UFLIRA Uninterpreted Functions and Mixed Linear Arithmetic
QF_UFRDL Uninterpreted Functions and Real Difference Logic