Uses of Interface
org.smtlib.ILanguage

Packages that use ILanguage

Package	Description
org.smtlib	This package contains the main classes and abstract interfaces for this SMT-LIB tool; the tool provides a stand-alone SMT-LIB-compliant command-line application, an application that responds to SMT-LIB commands over a network port, and an SMT-LIB Java API.
org.smtlib.impl	This package is an implementation of the interfaces defined in org.smtlib.
org.smtlib.logic	This package contains implementations of classes that implement the constraints of individual logics.

Uses of ILanguage in org.smtlib

Subinterfaces of ILanguage in org.smtlib

Modifier and Type	Interface	Description
interface	ILogic	This interface represents a definition of an SMT_LIB logic

Uses of ILanguage in org.smtlib.impl

Classes in org.smtlib.impl that implement ILanguage

Modifier and Type	Class	Description
static class	SMTExpr.Logic

Uses of ILanguage in org.smtlib.logic

Classes in org.smtlib.logic that implement ILanguage

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