Uses of Class
org.smtlib.impl.SMTExpr.Logic

Packages that use SMTExpr.Logic

Package	Description
org.smtlib.logic	This package contains implementations of classes that implement the constraints of individual logics.

Uses of SMTExpr.Logic in org.smtlib.logic

Subclasses of SMTExpr.Logic in org.smtlib.logic

Modifier and Type	Class	Description
class	ALL
class	AUFLIA
class	AUFLIRA
class	AUFNIRA
class	DifferenceLogic	Common base for the difference logics QF_IDL and QF_RDL.
class	LIA
class	Logic	Common base for this package's per-logic syntactic-restriction classes (QF_IDL, LRA, QF_UF, etc).
class	LRA	This logic does not allow uninterpreted functions or nonlinear arithmetic terms
class	QF_ABV	This logic does not allow quantifiers or uninterpreted functions
class	QF_AUFBV	This logic does not allow quantifiers; all array terms have sort (Array (_ BitVec i) (_ BitVec j))
class	QF_AUFLIA
class	QF_AX
class	QF_BV
class	QF_EIA
class	QF_FP	Not an official SMT-LIB logic -- see QF_FP.smt2's own :notes: a jSMTLIB-invented convenience logic for exercising the FloatingPoint theory in this project's own test suite without needing the broad ALL logic.
class	QF_IDL	QF_IDL atoms (QF_IDL.smt2): (op x y), (op (- x y) n) and (op (- x y) (- n)), with x, y free constants of sort Int and n a numeral.
class	QF_LIA
class	QF_LRA
class	QF_NIA
class	QF_NRA
class	QF_RDL	QF_RDL atoms (QF_RDL.smt2): (op x y), (op (- x y) c), (op (- (+ x ...
class	QF_UF
class	QF_UFBV	Quantifier-free, with uninterpreted functions and sorts permitted -- identical restrictions to QF_UF, all inherited from it (the bit-vector vs.
class	QF_UFIDL
class	QF_UFLIA
class	QF_UFLRA
class	QF_UFNRA
class	UFLRA
class	UFNIA