Package org.smtlib.logic

package org.smtlib.logic

This package contains implementations of classes that implement the constraints of individual logics. In particular the language restrictions are checked in these classes.

Related Packages

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.command	This package contains implementations of the SMT-LIB commands, implementing the interfaces defined in ICommand; these implementations are independent of the concrete syntax that might be used, except that each command object has methods that can parse or print representations of the command in the standard (or potentially other) concrete syntaxes.
org.smtlib.ext	This package contains commands that are extensions to SMT-LIB.
org.smtlib.impl	This package is an implementation of the interfaces defined in org.smtlib.
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.

Classes

Class	Description
ALL
AUFLIA
AUFLIRA
AUFNIRA
DifferenceLogic	Common base for the difference logics QF_IDL and QF_RDL.
LIA
Logic	Common base for this package's per-logic syntactic-restriction classes (QF_IDL, LRA, QF_UF, etc).
LRA	This logic does not allow uninterpreted functions or nonlinear arithmetic terms
QF_ABV	This logic does not allow quantifiers or uninterpreted functions
QF_AUFBV	This logic does not allow quantifiers; all array terms have sort (Array (_ BitVec i) (_ BitVec j))
QF_AUFLIA
QF_AX
QF_BV
QF_EIA
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.
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.
QF_LIA
QF_LRA
QF_NIA
QF_NRA
QF_RDL	QF_RDL atoms (QF_RDL.smt2): (op x y), (op (- x y) c), (op (- (+ x ...
QF_UF
QF_UFBV	Quantifier-free, with uninterpreted functions and sorts permitted -- identical restrictions to QF_UF, all inherited from it (the bit-vector vs.
QF_UFIDL
QF_UFLIA
QF_UFLRA
QF_UFNRA
UFLRA
UFNIA