Uses of Interface
org.smtlib.ILogic

Packages that use ILogic

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.
org.smtlib.sexpr	This package is a concrete implementation of a particular concrete syntax for the abstract SMT-LIB semantics.
org.smtlib.solvers	This package implements various instances of org.smtlib.ISolver, which are specific solvers that wrap and interact with various off-the-shelf SMT solvers currently available.

Uses of ILogic in org.smtlib

Fields in org.smtlib declared as ILogic

Modifier and Type	Field	Description
ILogic	SymbolTable.logicInUse	The logic that is being used - this value is used to check that expressions, etc., conform to the language restrictions of the current logic.

Methods in org.smtlib that return ILogic

Modifier and Type	Method	Description
ILogic	Utils.findLogic(String name, IPos pos)	Reads a logic file, parses it, validates the name, and checks the version.
ILogic	IParser.parseLogic()	Parse an SMT-LIB logic; return null and log an error response if there is no valid logic definition

Methods in org.smtlib with parameters of type ILogic

Modifier and Type	Method	Description
IResponse	Utils.loadLogic(ILogic logicExpr, SymbolTable symTable)
T	IVisitor.TreeVisitor.visit(ILogic s)
T	IVisitor.visit(ILogic s)
ISort	TypeChecker.visit(ILogic s)

Uses of ILogic in org.smtlib.impl

Classes in org.smtlib.impl that implement ILogic

Modifier and Type	Class	Description
static class	SMTExpr.Logic

Uses of ILogic in org.smtlib.logic

Classes in org.smtlib.logic that implement ILogic

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

Uses of ILogic in org.smtlib.sexpr

Methods in org.smtlib.sexpr that return ILogic

Modifier and Type	Method	Description
ILogic	Parser.parseLogic()	Parses a logic definition (including beginning and ending parentheses, returning null with error messages if it fails; only part of the checking of the contents is performed in this call (the rest is done in loadLogic).

Methods in org.smtlib.sexpr with parameters of type ILogic

Modifier and Type	Method	Description
Void	Printer.visit(ILogic s)

Uses of ILogic in org.smtlib.solvers

Methods in org.smtlib.solvers with parameters of type ILogic

Modifier and Type	Method	Description
String	Solver_simplify.Translator.visit(ILogic s)