Uses of Interface
org.smtlib.INode

Packages that use INode

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.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 INode in org.smtlib

Subinterfaces of INode in org.smtlib

Modifier and Type	Interface	Description
interface	IAttributeValue	This interface represents the general class of attribute values; that is, it is the super-interface of any class that may be an attribute value; in the abstract syntax it has no particular structure, though it does include true, false, string literals, numerals, and various pre-defined constants.
interface	ICommand	This interface is the generic interface to command classes, providing functionality to type-check the command and to execute it.
static interface	ICommand.Iassert	Interface for the SMT-LIB assert command.
static interface	ICommand.Icheck_sat	Interface for the SMT-LIB check-sat command.
static interface	ICommand.Icheck_sat_assuming	Interface for the SMT-LIB check-sat-assuming command.
static interface	ICommand.Icomment	Interface for a comment pseudo-command: not part of the SMT-LIB command grammar itself, but modeled as a real, typed ICommand (see issue #115) so that every dispatch path -- execution, typed-visitor traversal, and printing -- treats it uniformly with every other command, rather than falling back on IVisitor's generic visit(ICommand) handling (a reflection-based lookup in Printer's case).
static interface	ICommand.Ideclare_const	Interface for the SMT-LIB declare-const command.
static interface	ICommand.Ideclare_datatype	Interface for the SMT-LIB declare-datatype command.
static interface	ICommand.Ideclare_datatypes	Interface for the SMT-LIB declare-datatypes command.
static interface	ICommand.Ideclare_fun	Interface for the SMT-LIB declare-fun command.
static interface	ICommand.Ideclare_sort	Interface for the SMT-LIB declare-sort command.
static interface	ICommand.Ideclare_sort_parameter	Interface for the SMT-LIB declare-sort-parameter command.
static interface	ICommand.Idefine_const	Interface for the SMT-LIB define-const command.
static interface	ICommand.Idefine_fun	Interface for the SMT-LIB define-fun command.
static interface	ICommand.Idefine_fun_rec	Interface for the SMT-LIB define-fun-rec command.
static interface	ICommand.Idefine_funs_rec	Interface for the SMT-LIB define-funs-rec command.
static interface	ICommand.Idefine_sort	Interface for the SMT-LIB define-sort command.
static interface	ICommand.Iecho	Interface for the SMT-LIB echo command.
static interface	ICommand.Iexit	Interface for the SMT-LIB exit command.
static interface	ICommand.Iget_assertions	Interface for the SMT-LIB get-assertions command.
static interface	ICommand.Iget_assignment	Interface for the SMT-LIB get-assignment command.
static interface	ICommand.Iget_info	Interface for the SMT-LIB get-info command.
static interface	ICommand.Iget_model	Interface for the SMT-LIB get-model command (non-standard extension).
static interface	ICommand.Iget_option	Interface for the SMT-LIB get-option command.
static interface	ICommand.Iget_proof	Interface for the SMT-LIB get-proof command.
static interface	ICommand.Iget_unsat_assumptions	Interface for the SMT-LIB get-unsat-assumptions command.
static interface	ICommand.Iget_unsat_core	Interface for the SMT-LIB get-unsat-core command.
static interface	ICommand.Iget_value	Interface for the SMT-LIB get-value command.
static interface	ICommand.Ipop	Interface for the SMT-LIB pop command.
static interface	ICommand.Ipush	Interface for the SMT-LIB push command.
static interface	ICommand.Ireset	Interface for the SMT-LIB reset command.
static interface	ICommand.Ireset_assertions	Interface for the SMT-LIB reset-assertions command.
static interface	ICommand.IScript	Interface to be implemented by all objects representing SMT-LIB scripts.
static interface	ICommand.Iset_info	Interface for the SMT-LIB set-info command.
static interface	ICommand.Iset_logic	Interface for the SMT-LIB set-logic command.
static interface	ICommand.Iset_option	Interface for the SMT-LIB set-option command.
interface	IExpr	This interface represents the functionality for any class implementing an SMT-LIB term or formula
static interface	IExpr.IAsIdentifier	This interface represents SMT-LIB identifiers that are sort qualifiers on function ids
static interface	IExpr.IAttribute<TT extends IAttributeValue>	This interface represents an SMT-LIB attribute-value pair; the value may be null (keyword-only attribute).
static interface	IExpr.IAttributedExpr	This interface represents an SMT-LIB expression with attributes.
static interface	IExpr.IBinaryLiteral	This interface represents SMT-LIB binary literals
static interface	IExpr.IBinding	This interface represents a binding of a parameter and an expression
static interface	IExpr.IConstructor	A constructor declaration within a datatype; pairs a constructor name with its selectors.
static interface	IExpr.IDecimal	This interface represents non-negative decimal numbers of arbitrary size (i.e.
static interface	IExpr.IDeclaration	This interface represents a declaration of a parameter and its sort
static interface	IExpr.IError	This interface represents an error, e.g.
static interface	IExpr.IExists	This interface represents an SMT-LIB quantified exists expression
static interface	IExpr.IFcnExpr	This interface represents SMT-LIB expressions that are a function identifier applied to one or more arguments.
static interface	IExpr.IForall	This interface represents an SMT-LIB quantified forall expression
static interface	IExpr.IFunctionDeclaration	A function declaration: a name, a parameter list (sorted variables), and a result sort; used in the header list of define-funs-rec.
static interface	IExpr.IHexLiteral	This interface represents SMT-LIB hex literals
static interface	IExpr.IIdentifier	This interface represents SMT-LIB identifiers (either ids or parameterized ids)
static interface	IExpr.IIndex	Marker interface for the index types in a parameterized identifier: INumeral and ISymbol, plus IHexLiteral, which the Strings theory's (_ char H) uses, and IBinaryLiteral, which no theory uses but which is parsed so that a solver reports it; each theory decides which kinds it accepts.
static interface	IExpr.IKeyword	This interface represents SMT-LIB attribute and infoflag names.
static interface	IExpr.ILambda	This interface represents an SMT-LIB lambda expression: (lambda (sorted_var+) term).
static interface	IExpr.ILet	This interface represents an SMT-LIB let-expression
static interface	IExpr.ILiteral	This interface represents all literal (explicit constant) expressions.
static interface	IExpr.IMatch	This interface represents an SMT-LIB 2.7 match expression.
static interface	IExpr.IMatchCase	This interface represents one case in a match expression: a pattern and its body.
static interface	IExpr.INumeral	This interface represents non-negative integers of arbitrary size.
static interface	IExpr.IParameterizedIdentifier	This interface represents SMT-LIB parameterized identifiers
static interface	IExpr.IPattern	This interface represents a match pattern: either a bare symbol (variable/nullary-constructor) or a constructor applied to zero or more variable symbols.
static interface	IExpr.IPatternTerms	This interface represents the value of a :pattern attribute: a list of terms (a multi-pattern), written in the concrete syntax as ( t1 ... tn ).
static interface	IExpr.IQualifiedIdentifier	This interface represents SMT-LIB identifiers for function ids (either ids or parameterized ids or as-type identifiers)
static interface	IExpr.ISelector	A selector declaration within a constructor; pairs a selector name with its result sort.
static interface	IExpr.ISortDeclaration	Pairs a sort name with its arity; used in declare-datatype and declare-datatypes.
static interface	IExpr.IStringLiteral	This interface represents SMT-LIB string literals
static interface	IExpr.ISymbol	This interface represents SMT-LIB ids; equal ids have equal (using .equals) values of value().
interface	ILogic	This interface represents a definition of an SMT_LIB logic
interface	IResponse	This interface represents responses that can be received from SMT-LIB commands.
static interface	IResponse.IAssertionsResponse	Response type for get-assertions, carrying the list of currently asserted formulae.
static interface	IResponse.IAssignmentResponse	Response type for get-assignment, carrying a list of name-Boolean pairs.
static interface	IResponse.IAttributeList	Response type for get-info, carrying a list of attribute key-value pairs.
static interface	IResponse.IError	The interface for error responses
static interface	IResponse.IProofResponse	Response type for get-proof.
static interface	IResponse.IUnsatAssumptionsResponse	Response type for get-unsat-assumptions, carrying the assumptions (terms, e.g.
static interface	IResponse.IUnsatCoreResponse	Response type for get-unsat-core, carrying the names of the formulae in the unsat core.
static interface	IResponse.IValueResponse	Response type for get-value, carrying a list of expression-value pairs.
interface	ISort	The interface for an SMT-LIB concept of a Sort.
static interface	ISort.IAbbreviation	This interface represents a new Sort symbol designating an abbreviation for a (possibly parameterized) sort expression.
static interface	ISort.IApplication	The interface for a Sort expression that consists of either an arity 0 sort symbol or a positive-arity symbol with the appropriate number of arguments.
static interface	ISort.IDatatype	The interface for a datatype declaration (used in declare-datatype and declare-datatypes).
static interface	ISort.IDefinition	A super-interface for definitions of new sort ids.
static interface	ISort.IErrorDefinition	Represents an erroneous sort definition; by having an actual IDefinition, redundant cascading errors are suppressed.
static interface	ISort.IFamily	This interface represents a new Sort symbol designating either a new Sort (if the arity is 0) or a new parameterized Sort family (if the arity is greater than 0); each new symbol has a (new) name and a non-negative arity.
static interface	ISort.IFcnSort	An interface to represent the Sort of a function; this is not something that can be written as a sort expression in SMT-LIB, but it is convenient to be able to represent the sorts of function ids uniformly with the sorts of other ids.
static interface	ISort.IParameter	The interface for a sort parameter, as used in sort abbreviations (including in the defining expression).
interface	ITheory	This interface represents a definition of an SMT-LIB theory

Classes in org.smtlib that implement INode

Modifier and Type	Class	Description
static final class	AbstractSolver.Pending	The response returned for a command sent by AbstractSolver.sendPipelined(ICommand) whose actual response has not yet been read; AbstractSolver.Pending.isReady() tells when it has (see AbstractSolver.readPipelined(boolean)), and AbstractSolver.Pending.response() then gives it.

Methods in org.smtlib with type parameters of type INode

Modifier and Type	Method	Description
<T extends INode> void	IPrinter.print(T expr)	Prints the argument to the receiver
<T extends INode> String	IPrinter.toString(T expr)	Returns the argument as a String using a Printer of the same type as the receiver, but does not modify the receiver.

Methods in org.smtlib with parameters of type INode

Modifier and Type	Method	Description
protected String	AbstractSolver.translate(INode sexpr)	Translates an in-memory node into the text sent to the solver process.

Uses of INode in org.smtlib.command

Classes in org.smtlib.command that implement INode

Modifier and Type	Class	Description
class	C_assert	Implements the assert command
class	C_check_sat	Implements the check-sat command
class	C_check_sat_assuming	Implements the check-sat-assuming command
class	C_comment	A synthetic pseudo-command representing a comment that appeared immediately before a real command in a script -- not part of the SMT-LIB command grammar itself, but modeled as a real, typed ICommand.Icomment (see issue #115) rather than a generic ICommand, so execution, typed-visitor traversal, and printing all dispatch to it the same way every other command does, with no reflection-based or generic-fallback special case.
class	C_declare_const	Implements the declare-const command (syntactic sugar for declare-fun with no argument sorts)
class	C_declare_datatype	Implements the declare-datatype command
class	C_declare_datatypes	Implements the declare-datatypes command
class	C_declare_fun	Implements the declare-fun command
class	C_declare_sort	Implements the declare-sort command
class	C_declare_sort_parameter	Implements the declare-sort-parameter command
class	C_define_const	Implements the define-const command: syntactic sugar for define-fun with no parameters
class	C_define_fun	Implements the define-fun command
class	C_define_fun_rec	Implements the define-fun-rec command (recursive function definition); syntactically identical to define-fun (see C_define_fun), differing only in the dispatch target -- shares that class's fields, accessors, and constructor.
class	C_define_funs_rec	Implements the define-funs-rec command
class	C_define_sort	Implements the define-sort command
class	C_echo	Implements the echo command
class	C_exit	Implements the exit command
class	C_get_assertions	Implements the get-assertions command
class	C_get_assignment	Implements the get-assignment command
class	C_get_info	Implements the get-info command.
class	C_get_model	Implements the get-model command
class	C_get_option	Implements the get-option command
class	C_get_proof	Implements the get-proof command
class	C_get_unsat_assumptions	Implements the get-unsat-assumptions command
class	C_get_unsat_core	Implements the get-unsat-core command
class	C_get_value	Implements the get-value command
class	C_pop	Implements the pop command
class	C_push	Implements the push command
class	C_reset	Implements the reset command
class	C_reset_assertions	Implements the reset-assertions command
class	C_set_info	Implements the set-info command
class	C_set_logic	Implements the set-logic command.
class	C_set_option	Implements the set-option command

Uses of INode in org.smtlib.ext

Subinterfaces of INode in org.smtlib.ext

Modifier and Type	Interface	Description
interface	Iexec	Interface for the SMT-LIB exec command (non-standard extension).
interface	Iwhat	Interface for the SMT-LIB what command (non-standard extension).

Classes in org.smtlib.ext that implement INode

Modifier and Type	Class	Description
class	C_exec	Implements the non-standard exec command
class	C_what	Implements the non-standard what command.

Uses of INode in org.smtlib.impl

Classes in org.smtlib.impl that implement INode

Modifier and Type	Class	Description
class	Command	This abstract class is the base class for all commands within this implementation.
static class	Pos.AbstractExpr	A Printable that also implements IExpr, additionally holding the sort computed for the expression by the type checker (null if not yet, or never, computed).
static class	Pos.Printable	A Posable that also implements INode, with toString() delegating to Printer.
static class	Response.AssertionsResponse	Implements the IResponse.IAssertionsResponse interface
static class	Response.AssignmentResponse	Implements the IResponse.IAssignmentResponse interface
static class	Response.Error	Implements the IResponse.IError interface
static class	Response.ProofResponse	Implements the IResponse.IProofResponse interface
static class	Response.Seq	Implementation of IAttributeList: a list of attributes returned by get-info.
static class	Response.UnsatAssumptionsResponse	Implements the IResponse.IUnsatAssumptionsResponse interface
static class	Response.UnsatCoreResponse	Implements the IResponse.IUnsatCoreResponse interface
static class	Response.ValueResponse	Implements the IResponse.IValueResponse interface
class	Script	This class implements the IScript interface, representing SMT-LIB command scripts
class	SMTExpr	This class defines a number of subclasses that implement the SMT-LIB abstract AST; they are used by commands and expressions.
static class	SMTExpr.AsIdentifier	This class represents an SMT as-identifier AST
static class	SMTExpr.Attribute<TT extends IAttributeValue>	Represents an SMT-LIB attribute: a keyword optionally paired with a value.
static class	SMTExpr.AttributedExpr	Represents an SMT-LIB attributed expression ((! expr attrs...)).
static class	SMTExpr.BinaryLiteral	Represents an SMT-LIB binary literal (e.g.
static class	SMTExpr.Binding	Represents a let-binding: a symbol bound to an expression.
static class	SMTExpr.Constructor	Represents a constructor declaration within a datatype, consisting of a name and a list of selectors.
static class	SMTExpr.Datatype	Represents a datatype body: a list of constructors and (for parametric forms) a list of sort parameter symbols.
static class	SMTExpr.Decimal	This class represents an SMT Decimal literal expression or syntax token
static class	SMTExpr.Declaration	Represents a sorted variable declaration (parameter name and its sort), used in forall/exists/define-fun.
static class	SMTExpr.Error	Represents an expression-level error node inserted during parsing to allow error recovery.
static class	SMTExpr.Exists	Represents an SMT-LIB existential quantifier expression.
static class	SMTExpr.FcnExpr	Represents a function-application expression: a qualified identifier applied to a list of argument expressions.
static class	SMTExpr.Forall	Represents an SMT-LIB universal quantifier expression.
static class	SMTExpr.FunctionDeclaration	Represents a function declaration header (name, sorted parameters, result sort), used in define-funs-rec.
static class	SMTExpr.HexLiteral	Represents an SMT-LIB hex literal (e.g.
static class	SMTExpr.Keyword	This class represents an SMT Keyword syntax token
static class	SMTExpr.Lambda	Represents an SMT-LIB lambda expression (SMT-LIB 2.7ff, HO-Core theory).
static class	SMTExpr.Let	Represents an SMT-LIB let expression: a list of bindings and a body expression.
static class	SMTExpr.Literal<T>	Abstract base class for all literal value AST nodes; holds the typed value and provides a shared implementation.
static class	SMTExpr.Logic
static class	SMTExpr.Match	Represents an SMT-LIB 2.7 match expression: an expression matched against a list of cases.
static class	SMTExpr.MatchCase	Represents a single case in a match expression: a pattern and its result body.
static class	SMTExpr.Numeral	This class represents an SMT Numeral expression or syntax token
static class	SMTExpr.ParameterizedIdentifier	This class represents an SMT parameterized-identifier AST (e.g.
static class	SMTExpr.Pattern	Represents a match pattern: a constructor name applied to zero or more variable symbols.
static class	SMTExpr.PatternTerms	Represents the value of a :pattern attribute: a list of trigger terms.
static class	SMTExpr.Selector	Represents a selector declaration within a datatype constructor.
static class	SMTExpr.SortDeclaration	Represents a sort declaration (symbol and arity) used in declare-datatype and declare-datatypes.
static class	SMTExpr.StringLiteral	This class represents an SMT String literal expression or syntax token
static class	SMTExpr.Symbol	This class represents an SMT Symbol
static class	SMTExpr.Theory
class	Sort	This class implements the abstract ISort interface
static class	Sort.Abbreviation	Implements a Sort abbreviation (parameterized definition, possibly with no parameters)
static class	Sort.Application	Represents a sort expression consisting of a sort symbol or sort abbreviation symbol applied to a corresponding number of sort arguments
static class	Sort.ErrorDefinition	A placeholder sort definition used when a sort declaration is ill-formed, to suppress cascading errors.
static class	Sort.Family	Represents a new sort symbol, with a given identifier and arity
static class	Sort.FcnSort	Represents the class of the sort of a function symbol.
static class	Sort.Parameter	Represents a Sort parameter, such as in either the parameter list or the expression of a Sort abbreviation

Uses of INode in org.smtlib.logic

Classes in org.smtlib.logic that implement INode

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 INode in org.smtlib.sexpr

Subinterfaces of INode in org.smtlib.sexpr

Modifier and Type	Interface	Description
interface	ISexpr	This interface represents S-expressions as used in SMT-LIB; they are used as values for attributes in the standard concrete syntax.
static interface	ISexpr.ISeq	Represents a sequence of S-expressions
static interface	ISexpr.IToken<T>	Represents a single S-expression token

Classes in org.smtlib.sexpr that implement INode

Modifier and Type	Class	Description
class	Sexpr	This is the root class for S-expressions in the concrete syntax
static class	Sexpr.Seq	The class corresponding to sequences of S-expressions
static class	Sexpr.Token<T>	Represents a single S-expression token with intrinsic type T

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

Modifier and Type	Method	Description
<T extends INode> void	Printer.print(T expr)	Prints the argument to the receiver
<T extends INode> String	Printer.toString(T expr)	Returns the argument as a String using a Printer of the same type as the receiver, but does not modify the receiver.
static <T extends INode> void	Printer.WithLines.write(SMT.Configuration smtConfig, PrintStream w, T e)	Writes the given expression to the given stream, following the given Configuration's rules.
static <T extends INode> void	Printer.WithLines.write(SMT.Configuration smtConfig, Writer w, T e)	Writes the given expression to the given writer, following the given Configuration's rules.
static <T extends INode> void	Printer.write(SMT.Configuration smtConfig, PrintStream w, T e)	Writes the given expression to the given stream, following the given Configuration's rules.
static <T extends INode> void	Printer.write(SMT.Configuration smtConfig, Writer w, T e)	Writes the given expression to the given writer, following the given Configuration's rules.
static <T extends INode> String	Printer.write(SMT.Configuration smtConfig, T e)	Writes the given expression and outputs as a String, following the given Configuration's rules (e.g.

Uses of INode in org.smtlib.solvers

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

Modifier and Type	Method	Description
<T extends INode> String	Printer.toString(T expr)
static <T extends INode> void	Printer.write(SMT.Configuration smtConfig, PrintStream w, T e)	Writes the given expression to the given stream, following the given Configuration's rules.
static <T extends INode> void	Printer.write(SMT.Configuration smtConfig, Writer w, T e)	Writes the given expression to the given writer, following the given Configuration's rules.
static <T extends INode> String	Printer.write(SMT.Configuration smtConfig, T e)	Writes the given expression and outputs as a String, following the given Configuration's rules.

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

Modifier and Type	Method	Description
protected String	Solver_smt.translate(INode sexpr)	Translates an S-expression into SMT syntax; this solver uses the standard S-expression concrete syntax except for a Bool-quantifier workaround (see Printer).
protected String	Solver_z3_4_3.translate(INode sexpr)	Translates an S-expression into Z3 syntax
protected String	Solver_z3_4_5.translate(INode node)	z3 4.5 rejects every check-sat-assuming ("invalid check-sat-assuming command, '(', expected", a parser bug), so it is sent as z3's legacy (check-sat a1 ...