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_AUFBVLIA

Arrays, Uninterpreted Functions, Bitvectors and Linear Integer Arithmetic

QF_AUFLRA

Arrays, Uninterpreted Functions, Linear Real Arithmetic

QF_AUFLIRA

Arrays, Uninterpreted Functions, Mixed Linear Arithmetic

QF_BVLRA

Bitvectors, Linear Real Arithmetic

QF_LIRA

Mixed Linear Arithmetic

QF_UFBVLIA

Uninterpreted Functions, Bitvectors Linear Integer Arithmetic

QF_UFLIRA

Uninterpreted Functions and Mixed Linear Arithmetic

QF_UFRDL

Uninterpreted Functions and Real Difference Logic

Previous topic

Next topic

SMT Logics

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

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