Uses of Package
org.smtlib

Packages that use org.smtlib

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.

Classes in org.smtlib used by org.smtlib

Class	Description
AbstractSolver.Shape	The kinds of response a command has besides an error or unsupported (#149)
AbstractSolver.StackChange	The kinds of command that change the assertion stack: each returns a conforming solver to assert mode, where the get- commands about the last check are errors (declare-const is declare-fun, declare-datatypes is declare-datatype, define-funs-rec is define-fun-rec), as does a set-logic that a solver accepts after a check (SMT-LIB makes that an error, but --relax may allow it)
CharSequenceInfinite	This class implements a CharSequence that obtains its characters from a source of characters of unknown length; it also provides some functionality to retain the characters and compute line numbers.
CharSequenceInfinite.IPrompter	This interface is used to create prompters.
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.
ICommand	This interface is the generic interface to command classes, providing functionality to type-check the command and to execute it.
ICommand.Iassert	Interface for the SMT-LIB assert command.
ICommand.Icheck_sat	Interface for the SMT-LIB check-sat command.
ICommand.Icheck_sat_assuming	Interface for the SMT-LIB check-sat-assuming command.
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).
ICommand.Ideclare_const	Interface for the SMT-LIB declare-const command.
ICommand.Ideclare_datatype	Interface for the SMT-LIB declare-datatype command.
ICommand.Ideclare_datatypes	Interface for the SMT-LIB declare-datatypes command.
ICommand.Ideclare_fun	Interface for the SMT-LIB declare-fun command.
ICommand.Ideclare_sort	Interface for the SMT-LIB declare-sort command.
ICommand.Ideclare_sort_parameter	Interface for the SMT-LIB declare-sort-parameter command.
ICommand.Idefine_const	Interface for the SMT-LIB define-const command.
ICommand.Idefine_fun	Interface for the SMT-LIB define-fun command.
ICommand.Idefine_fun_rec	Interface for the SMT-LIB define-fun-rec command.
ICommand.Idefine_funs_rec	Interface for the SMT-LIB define-funs-rec command.
ICommand.Idefine_sort	Interface for the SMT-LIB define-sort command.
ICommand.Iecho	Interface for the SMT-LIB echo command.
ICommand.Iexit	Interface for the SMT-LIB exit command.
ICommand.IFactory	This is the interface to be used by a concrete ICommand factory.
ICommand.IFinder	This interface defines classes that implement techniques for mapping a command name to a class that implements that command.
ICommand.Iget_assertions	Interface for the SMT-LIB get-assertions command.
ICommand.Iget_assignment	Interface for the SMT-LIB get-assignment command.
ICommand.Iget_info	Interface for the SMT-LIB get-info command.
ICommand.Iget_model	Interface for the SMT-LIB get-model command (non-standard extension).
ICommand.Iget_option	Interface for the SMT-LIB get-option command.
ICommand.Iget_proof	Interface for the SMT-LIB get-proof command.
ICommand.Iget_unsat_assumptions	Interface for the SMT-LIB get-unsat-assumptions command.
ICommand.Iget_unsat_core	Interface for the SMT-LIB get-unsat-core command.
ICommand.Iget_value	Interface for the SMT-LIB get-value command.
ICommand.Ipop	Interface for the SMT-LIB pop command.
ICommand.Ipush	Interface for the SMT-LIB push command.
ICommand.Ireset	Interface for the SMT-LIB reset command.
ICommand.Ireset_assertions	Interface for the SMT-LIB reset-assertions command.
ICommand.IScript	Interface to be implemented by all objects representing SMT-LIB scripts.
ICommand.Iset_info	Interface for the SMT-LIB set-info command.
ICommand.Iset_logic	Interface for the SMT-LIB set-logic command.
ICommand.Iset_option	Interface for the SMT-LIB set-option command.
IExpr	This interface represents the functionality for any class implementing an SMT-LIB term or formula
IExpr.IAsIdentifier	This interface represents SMT-LIB identifiers that are sort qualifiers on function ids
IExpr.IAttribute	This interface represents an SMT-LIB attribute-value pair; the value may be null (keyword-only attribute).
IExpr.IAttributedExpr	This interface represents an SMT-LIB expression with attributes.
IExpr.IBinaryLiteral	This interface represents SMT-LIB binary literals
IExpr.IBinding	This interface represents a binding of a parameter and an expression
IExpr.IConstructor	A constructor declaration within a datatype; pairs a constructor name with its selectors.
IExpr.IDecimal	This interface represents non-negative decimal numbers of arbitrary size (i.e.
IExpr.IDeclaration	This interface represents a declaration of a parameter and its sort
IExpr.IError	This interface represents an error, e.g.
IExpr.IExists	This interface represents an SMT-LIB quantified exists expression
IExpr.IFactory	The interface defining the factory type for producing objects of various subtypes of IExpr; the IPos argument is an optional argument giving information about the textual position of an expression.
IExpr.IFcnExpr	This interface represents SMT-LIB expressions that are a function identifier applied to one or more arguments.
IExpr.IForall	This interface represents an SMT-LIB quantified forall expression
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.
IExpr.IHexLiteral	This interface represents SMT-LIB hex literals
IExpr.IIdentifier	This interface represents SMT-LIB identifiers (either ids or parameterized ids)
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.
IExpr.IKeyword	This interface represents SMT-LIB attribute and infoflag names.
IExpr.ILambda	This interface represents an SMT-LIB lambda expression: (lambda (sorted_var+) term).
IExpr.ILet	This interface represents an SMT-LIB let-expression
IExpr.ILiteral	This interface represents all literal (explicit constant) expressions.
IExpr.IMatch	This interface represents an SMT-LIB 2.7 match expression.
IExpr.IMatchCase	This interface represents one case in a match expression: a pattern and its body.
IExpr.INumeral	This interface represents non-negative integers of arbitrary size.
IExpr.IParameterizedIdentifier	This interface represents SMT-LIB parameterized identifiers
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.
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 ).
IExpr.IQualifiedIdentifier	This interface represents SMT-LIB identifiers for function ids (either ids or parameterized ids or as-type identifiers)
IExpr.ISelector	A selector declaration within a constructor; pairs a selector name with its result sort.
IExpr.ISortDeclaration	Pairs a sort name with its arity; used in declare-datatype and declare-datatypes.
IExpr.IStringLiteral	This interface represents SMT-LIB string literals
IExpr.ISymbol	This interface represents SMT-LIB ids; equal ids have equal (using .equals) values of value().
ILanguage	This interface represents the functionality of an SMT-LIB language - the combination of one or more theories and various restrictions on the permitted expressions.
ILogic	This interface represents a definition of an SMT_LIB logic
INode	This interface is defined and implemented as a marker that the accept method is available and to ensure that subtypes implement the accept method.
IParser	This is the interface to a parser for SMT-LIB.
IParser.IFactory	The interface for the parser/printer factory
IParser.ParserException	An exception thrown if parsing is to be aborted.
IPos	This is an interface that supplies information about a range in textual position within a source of characters.
IPos.IPosable	This interface identifies classes that can have their position set
IPrinter	An interface for printers to concrete syntax; factories are shared with Parsers in IParser.IFactory.
IResponse	This interface represents responses that can be received from SMT-LIB commands.
IResponse.IAssertionsResponse	Response type for get-assertions, carrying the list of currently asserted formulae.
IResponse.IAssignmentResponse	Response type for get-assignment, carrying a list of name-Boolean pairs.
IResponse.IAttributeList	Response type for get-info, carrying a list of attribute key-value pairs.
IResponse.IError	The interface for error responses
IResponse.IFactory	The factory interface for creating the standard IResponse singleton and structured instances.
IResponse.IPair	An interface for simple pairs of objects; used to represent value/assignment response items
IResponse.IProofResponse	Response type for get-proof.
IResponse.IUnsatAssumptionsResponse	Response type for get-unsat-assumptions, carrying the assumptions (terms, e.g.
IResponse.IUnsatCoreResponse	Response type for get-unsat-core, carrying the names of the formulae in the unsat core.
IResponse.IValueResponse	Response type for get-value, carrying a list of expression-value pairs.
ISolver	This is the interface to be implemented by any solver adapter; there is a method for each SMT-LIB command.
ISolver.CreationException	Thrown by SMT.Configuration.createSolver(java.lang.String, java.lang.String) when a solver adapter cannot be resolved, constructed, or fails to launch.
ISort	The interface for an SMT-LIB concept of a Sort.
ISort.IAbbreviation	This interface represents a new Sort symbol designating an abbreviation for a (possibly parameterized) sort expression.
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.
ISort.IDatatype	The interface for a datatype declaration (used in declare-datatype and declare-datatypes).
ISort.IDefinition	A super-interface for definitions of new sort ids.
ISort.IErrorDefinition	Represents an erroneous sort definition; by having an actual IDefinition, redundant cascading errors are suppressed.
ISort.IFactory	The interface for a Sort-creating factory.
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.
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.
ISort.IParameter	The interface for a sort parameter, as used in sort abbreviations (including in the defining expression).
ISource	This interface represents sources of characters.
ITheory	This interface represents a definition of an SMT-LIB theory
IVisitor	This is a visitor interface for visitors over IExpr ASTs.
IVisitor.VisitorException	An Exception class to use if there is a problem during execution of an IVisitor (e.g.
Log	This class is used as a collection point for all output.
Log.IListener	This is an interface to be implemented by any Object that wants to hear log messages; the Object must register itself by calling Log.addListener.
Log.IPendingOutput	Output whose content is not yet known, e.g.
SMT.Configuration	The configuration object holds the values of all of the current options (e.g.
SMT.Configuration.SMTLIB	Enumeration of the supported SMT-LIB versions, in declaration order from oldest to newest.
SMT.IConfiguration	Marker interface for configuration objects; reserved for future extension.
SolverCapabilities.Capability	The capabilities that can be queried; SolverCapabilities.Capability.token is the name used in the properties
SolverCapabilities.Support	The answer to a query; UNKNOWN means the solver's entry does not record the capability
SolverProcess	This class implements launching, writing to, and reading responses from a launched process (in particular, solver processes).
SolverProcess.ProverException	Wraps an exception thrown because of a failure in the prover
SolverProcess.StreamGobbler	Continuously drains one of the process's output streams (stdout or stderr) on a dedicated thread, so that a solver writing a large amount of text to one stream can never be blocked by the other stream's OS pipe buffer filling up while this process is busy reading elsewhere -- reading stdout and stderr sequentially in a single thread cannot make that guarantee.
SolverResolver.Resolution	The result of SolverResolver.resolve(java.util.Properties, java.lang.String, java.lang.String, java.lang.String, java.lang.String, java.util.function.Function<java.lang.String, java.lang.Class<?>>): the adapter class (and its name, for messages), and the executable, or the command array if the properties give one
SymbolTable	This class manages a symbol table used for storing definitions and looking up ids in expressions.
SymbolTable.Entry	An object that holds all the information about the defined symbol (or aliased definition).
SymbolTable.Iterator	An iterator over all of the Symbols in the symbol scope stack from the top-most scope on down.
TypeChecker.Variable
Utils	A class of static utility methods and constants for the SMT-LIB package.
Utils.SMTLIBException	A checked exception used internally to propagate SMT-LIB errors that carry an IResponse.IError.

Classes in org.smtlib used by org.smtlib.command

Class	Description
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.
ICommand	This interface is the generic interface to command classes, providing functionality to type-check the command and to execute it.
ICommand.Iassert	Interface for the SMT-LIB assert command.
ICommand.Icheck_sat	Interface for the SMT-LIB check-sat command.
ICommand.Icheck_sat_assuming	Interface for the SMT-LIB check-sat-assuming command.
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).
ICommand.Ideclare_const	Interface for the SMT-LIB declare-const command.
ICommand.Ideclare_datatype	Interface for the SMT-LIB declare-datatype command.
ICommand.Ideclare_datatypes	Interface for the SMT-LIB declare-datatypes command.
ICommand.Ideclare_fun	Interface for the SMT-LIB declare-fun command.
ICommand.Ideclare_sort	Interface for the SMT-LIB declare-sort command.
ICommand.Ideclare_sort_parameter	Interface for the SMT-LIB declare-sort-parameter command.
ICommand.Idefine_const	Interface for the SMT-LIB define-const command.
ICommand.Idefine_fun	Interface for the SMT-LIB define-fun command.
ICommand.Idefine_fun_rec	Interface for the SMT-LIB define-fun-rec command.
ICommand.Idefine_funs_rec	Interface for the SMT-LIB define-funs-rec command.
ICommand.Idefine_sort	Interface for the SMT-LIB define-sort command.
ICommand.Iecho	Interface for the SMT-LIB echo command.
ICommand.Iexit	Interface for the SMT-LIB exit command.
ICommand.Iget_assertions	Interface for the SMT-LIB get-assertions command.
ICommand.Iget_assignment	Interface for the SMT-LIB get-assignment command.
ICommand.Iget_info	Interface for the SMT-LIB get-info command.
ICommand.Iget_model	Interface for the SMT-LIB get-model command (non-standard extension).
ICommand.Iget_option	Interface for the SMT-LIB get-option command.
ICommand.Iget_proof	Interface for the SMT-LIB get-proof command.
ICommand.Iget_unsat_assumptions	Interface for the SMT-LIB get-unsat-assumptions command.
ICommand.Iget_unsat_core	Interface for the SMT-LIB get-unsat-core command.
ICommand.Iget_value	Interface for the SMT-LIB get-value command.
ICommand.Ipop	Interface for the SMT-LIB pop command.
ICommand.Ipush	Interface for the SMT-LIB push command.
ICommand.Ireset	Interface for the SMT-LIB reset command.
ICommand.Ireset_assertions	Interface for the SMT-LIB reset-assertions command.
ICommand.Iset_info	Interface for the SMT-LIB set-info command.
ICommand.Iset_logic	Interface for the SMT-LIB set-logic command.
ICommand.Iset_option	Interface for the SMT-LIB set-option command.
IExpr	This interface represents the functionality for any class implementing an SMT-LIB term or formula
IExpr.IAttribute	This interface represents an SMT-LIB attribute-value pair; the value may be null (keyword-only attribute).
IExpr.IDeclaration	This interface represents a declaration of a parameter and its sort
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.
IExpr.IKeyword	This interface represents SMT-LIB attribute and infoflag names.
IExpr.INumeral	This interface represents non-negative integers of arbitrary size.
IExpr.ISortDeclaration	Pairs a sort name with its arity; used in declare-datatype and declare-datatypes.
IExpr.IStringLiteral	This interface represents SMT-LIB string literals
IExpr.ISymbol	This interface represents SMT-LIB ids; equal ids have equal (using .equals) values of value().
INode	This interface is defined and implemented as a marker that the accept method is available and to ensure that subtypes implement the accept method.
IParser.ParserException	An exception thrown if parsing is to be aborted.
IPos.IPosable	This interface identifies classes that can have their position set
IResponse	This interface represents responses that can be received from SMT-LIB commands.
IResponse.IError	The interface for error responses
ISolver	This is the interface to be implemented by any solver adapter; there is a method for each SMT-LIB command.
ISort	The interface for an SMT-LIB concept of a Sort.
ISort.IDatatype	The interface for a datatype declaration (used in declare-datatype and declare-datatypes).
ISort.IParameter	The interface for a sort parameter, as used in sort abbreviations (including in the defining expression).
IVisitor	This is a visitor interface for visitors over IExpr ASTs.
IVisitor.VisitorException	An Exception class to use if there is a problem during execution of an IVisitor (e.g.
SMT.Configuration	The configuration object holds the values of all of the current options (e.g.

Classes in org.smtlib used by org.smtlib.ext

Class	Description
ICommand	This interface is the generic interface to command classes, providing functionality to type-check the command and to execute it.
ICommand.IScript	Interface to be implemented by all objects representing SMT-LIB scripts.
IExpr.IIdentifier	This interface represents SMT-LIB identifiers (either ids or parameterized ids)
INode	This interface is defined and implemented as a marker that the accept method is available and to ensure that subtypes implement the accept method.
IParser.ParserException	An exception thrown if parsing is to be aborted.
IPos.IPosable	This interface identifies classes that can have their position set
IResponse	This interface represents responses that can be received from SMT-LIB commands.
ISolver	This is the interface to be implemented by any solver adapter; there is a method for each SMT-LIB command.
IVisitor	This is a visitor interface for visitors over IExpr ASTs.
IVisitor.VisitorException	An Exception class to use if there is a problem during execution of an IVisitor (e.g.

Classes in org.smtlib used by org.smtlib.impl

Class	Description
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.
ICommand	This interface is the generic interface to command classes, providing functionality to type-check the command and to execute it.
ICommand.Iassert	Interface for the SMT-LIB assert command.
ICommand.Icheck_sat	Interface for the SMT-LIB check-sat command.
ICommand.Icheck_sat_assuming	Interface for the SMT-LIB check-sat-assuming command.
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).
ICommand.Ideclare_const	Interface for the SMT-LIB declare-const command.
ICommand.Ideclare_datatype	Interface for the SMT-LIB declare-datatype command.
ICommand.Ideclare_datatypes	Interface for the SMT-LIB declare-datatypes command.
ICommand.Ideclare_fun	Interface for the SMT-LIB declare-fun command.
ICommand.Ideclare_sort	Interface for the SMT-LIB declare-sort command.
ICommand.Ideclare_sort_parameter	Interface for the SMT-LIB declare-sort-parameter command.
ICommand.Idefine_const	Interface for the SMT-LIB define-const command.
ICommand.Idefine_fun	Interface for the SMT-LIB define-fun command.
ICommand.Idefine_fun_rec	Interface for the SMT-LIB define-fun-rec command.
ICommand.Idefine_funs_rec	Interface for the SMT-LIB define-funs-rec command.
ICommand.Idefine_sort	Interface for the SMT-LIB define-sort command.
ICommand.Iecho	Interface for the SMT-LIB echo command.
ICommand.Iexit	Interface for the SMT-LIB exit command.
ICommand.IFactory	This is the interface to be used by a concrete ICommand factory.
ICommand.Iget_assertions	Interface for the SMT-LIB get-assertions command.
ICommand.Iget_assignment	Interface for the SMT-LIB get-assignment command.
ICommand.Iget_info	Interface for the SMT-LIB get-info command.
ICommand.Iget_model	Interface for the SMT-LIB get-model command (non-standard extension).
ICommand.Iget_option	Interface for the SMT-LIB get-option command.
ICommand.Iget_proof	Interface for the SMT-LIB get-proof command.
ICommand.Iget_unsat_assumptions	Interface for the SMT-LIB get-unsat-assumptions command.
ICommand.Iget_unsat_core	Interface for the SMT-LIB get-unsat-core command.
ICommand.Iget_value	Interface for the SMT-LIB get-value command.
ICommand.Ipop	Interface for the SMT-LIB pop command.
ICommand.Ipush	Interface for the SMT-LIB push command.
ICommand.Ireset	Interface for the SMT-LIB reset command.
ICommand.Ireset_assertions	Interface for the SMT-LIB reset-assertions command.
ICommand.IScript	Interface to be implemented by all objects representing SMT-LIB scripts.
ICommand.Iset_info	Interface for the SMT-LIB set-info command.
ICommand.Iset_logic	Interface for the SMT-LIB set-logic command.
ICommand.Iset_option	Interface for the SMT-LIB set-option command.
IExpr	This interface represents the functionality for any class implementing an SMT-LIB term or formula
IExpr.IAsIdentifier	This interface represents SMT-LIB identifiers that are sort qualifiers on function ids
IExpr.IAttribute	This interface represents an SMT-LIB attribute-value pair; the value may be null (keyword-only attribute).
IExpr.IAttributedExpr	This interface represents an SMT-LIB expression with attributes.
IExpr.IBinaryLiteral	This interface represents SMT-LIB binary literals
IExpr.IBinding	This interface represents a binding of a parameter and an expression
IExpr.IConstructor	A constructor declaration within a datatype; pairs a constructor name with its selectors.
IExpr.IDecimal	This interface represents non-negative decimal numbers of arbitrary size (i.e.
IExpr.IDeclaration	This interface represents a declaration of a parameter and its sort
IExpr.IError	This interface represents an error, e.g.
IExpr.IExists	This interface represents an SMT-LIB quantified exists expression
IExpr.IFactory	The interface defining the factory type for producing objects of various subtypes of IExpr; the IPos argument is an optional argument giving information about the textual position of an expression.
IExpr.IFcnExpr	This interface represents SMT-LIB expressions that are a function identifier applied to one or more arguments.
IExpr.IForall	This interface represents an SMT-LIB quantified forall expression
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.
IExpr.IHexLiteral	This interface represents SMT-LIB hex literals
IExpr.IIdentifier	This interface represents SMT-LIB identifiers (either ids or parameterized ids)
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.
IExpr.IKeyword	This interface represents SMT-LIB attribute and infoflag names.
IExpr.ILambda	This interface represents an SMT-LIB lambda expression: (lambda (sorted_var+) term).
IExpr.ILet	This interface represents an SMT-LIB let-expression
IExpr.ILiteral	This interface represents all literal (explicit constant) expressions.
IExpr.IMatch	This interface represents an SMT-LIB 2.7 match expression.
IExpr.IMatchCase	This interface represents one case in a match expression: a pattern and its body.
IExpr.INumeral	This interface represents non-negative integers of arbitrary size.
IExpr.IParameterizedIdentifier	This interface represents SMT-LIB parameterized identifiers
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.
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 ).
IExpr.IQualifiedIdentifier	This interface represents SMT-LIB identifiers for function ids (either ids or parameterized ids or as-type identifiers)
IExpr.ISelector	A selector declaration within a constructor; pairs a selector name with its result sort.
IExpr.ISortDeclaration	Pairs a sort name with its arity; used in declare-datatype and declare-datatypes.
IExpr.IStringLiteral	This interface represents SMT-LIB string literals
IExpr.ISymbol	This interface represents SMT-LIB ids; equal ids have equal (using .equals) values of value().
ILanguage	This interface represents the functionality of an SMT-LIB language - the combination of one or more theories and various restrictions on the permitted expressions.
ILogic	This interface represents a definition of an SMT_LIB logic
INode	This interface is defined and implemented as a marker that the accept method is available and to ensure that subtypes implement the accept method.
IParser.ParserException	An exception thrown if parsing is to be aborted.
IPos	This is an interface that supplies information about a range in textual position within a source of characters.
IPos.IPosable	This interface identifies classes that can have their position set
IResponse	This interface represents responses that can be received from SMT-LIB commands.
IResponse.IAssertionsResponse	Response type for get-assertions, carrying the list of currently asserted formulae.
IResponse.IAssignmentResponse	Response type for get-assignment, carrying a list of name-Boolean pairs.
IResponse.IAttributeList	Response type for get-info, carrying a list of attribute key-value pairs.
IResponse.IError	The interface for error responses
IResponse.IFactory	The factory interface for creating the standard IResponse singleton and structured instances.
IResponse.IPair	An interface for simple pairs of objects; used to represent value/assignment response items
IResponse.IProofResponse	Response type for get-proof.
IResponse.IUnsatAssumptionsResponse	Response type for get-unsat-assumptions, carrying the assumptions (terms, e.g.
IResponse.IUnsatCoreResponse	Response type for get-unsat-core, carrying the names of the formulae in the unsat core.
IResponse.IValueResponse	Response type for get-value, carrying a list of expression-value pairs.
ISolver	This is the interface to be implemented by any solver adapter; there is a method for each SMT-LIB command.
ISort	The interface for an SMT-LIB concept of a Sort.
ISort.IAbbreviation	This interface represents a new Sort symbol designating an abbreviation for a (possibly parameterized) sort expression.
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.
ISort.IDatatype	The interface for a datatype declaration (used in declare-datatype and declare-datatypes).
ISort.IDefinition	A super-interface for definitions of new sort ids.
ISort.IErrorDefinition	Represents an erroneous sort definition; by having an actual IDefinition, redundant cascading errors are suppressed.
ISort.IFactory	The interface for a Sort-creating factory.
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.
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.
ISort.IParameter	The interface for a sort parameter, as used in sort abbreviations (including in the defining expression).
ISource	This interface represents sources of characters.
ITheory	This interface represents a definition of an SMT-LIB theory
IVisitor	This is a visitor interface for visitors over IExpr ASTs.
IVisitor.VisitorException	An Exception class to use if there is a problem during execution of an IVisitor (e.g.
SMT.Configuration	The configuration object holds the values of all of the current options (e.g.

Classes in org.smtlib used by org.smtlib.logic

Class	Description
IExpr	This interface represents the functionality for any class implementing an SMT-LIB term or formula
IExpr.IAttribute	This interface represents an SMT-LIB attribute-value pair; the value may be null (keyword-only attribute).
IExpr.IFcnExpr	This interface represents SMT-LIB expressions that are a function identifier applied to one or more arguments.
IExpr.IIdentifier	This interface represents SMT-LIB identifiers (either ids or parameterized ids)
IExpr.ISymbol	This interface represents SMT-LIB ids; equal ids have equal (using .equals) values of value().
ILanguage	This interface represents the functionality of an SMT-LIB language - the combination of one or more theories and various restrictions on the permitted expressions.
ILogic	This interface represents a definition of an SMT_LIB logic
INode	This interface is defined and implemented as a marker that the accept method is available and to ensure that subtypes implement the accept method.
IPos	This is an interface that supplies information about a range in textual position within a source of characters.
IPos.IPosable	This interface identifies classes that can have their position set
ISort	The interface for an SMT-LIB concept of a Sort.
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.
ISort.IParameter	The interface for a sort parameter, as used in sort abbreviations (including in the defining expression).
IVisitor.VisitorException	An Exception class to use if there is a problem during execution of an IVisitor (e.g.
SMT.Configuration	The configuration object holds the values of all of the current options (e.g.

Classes in org.smtlib used by org.smtlib.sexpr

Class	Description
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.
ICommand	This interface is the generic interface to command classes, providing functionality to type-check the command and to execute it.
ICommand.Iassert	Interface for the SMT-LIB assert command.
ICommand.Icheck_sat	Interface for the SMT-LIB check-sat command.
ICommand.Icheck_sat_assuming	Interface for the SMT-LIB check-sat-assuming command.
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).
ICommand.Ideclare_const	Interface for the SMT-LIB declare-const command.
ICommand.Ideclare_datatype	Interface for the SMT-LIB declare-datatype command.
ICommand.Ideclare_datatypes	Interface for the SMT-LIB declare-datatypes command.
ICommand.Ideclare_fun	Interface for the SMT-LIB declare-fun command.
ICommand.Ideclare_sort	Interface for the SMT-LIB declare-sort command.
ICommand.Ideclare_sort_parameter	Interface for the SMT-LIB declare-sort-parameter command.
ICommand.Idefine_const	Interface for the SMT-LIB define-const command.
ICommand.Idefine_fun	Interface for the SMT-LIB define-fun command.
ICommand.Idefine_fun_rec	Interface for the SMT-LIB define-fun-rec command.
ICommand.Idefine_funs_rec	Interface for the SMT-LIB define-funs-rec command.
ICommand.Idefine_sort	Interface for the SMT-LIB define-sort command.
ICommand.Iecho	Interface for the SMT-LIB echo command.
ICommand.Iexit	Interface for the SMT-LIB exit command.
ICommand.Iget_assertions	Interface for the SMT-LIB get-assertions command.
ICommand.Iget_assignment	Interface for the SMT-LIB get-assignment command.
ICommand.Iget_info	Interface for the SMT-LIB get-info command.
ICommand.Iget_model	Interface for the SMT-LIB get-model command (non-standard extension).
ICommand.Iget_option	Interface for the SMT-LIB get-option command.
ICommand.Iget_proof	Interface for the SMT-LIB get-proof command.
ICommand.Iget_unsat_assumptions	Interface for the SMT-LIB get-unsat-assumptions command.
ICommand.Iget_unsat_core	Interface for the SMT-LIB get-unsat-core command.
ICommand.Iget_value	Interface for the SMT-LIB get-value command.
ICommand.Ipop	Interface for the SMT-LIB pop command.
ICommand.Ipush	Interface for the SMT-LIB push command.
ICommand.Ireset	Interface for the SMT-LIB reset command.
ICommand.Ireset_assertions	Interface for the SMT-LIB reset-assertions command.
ICommand.IScript	Interface to be implemented by all objects representing SMT-LIB scripts.
ICommand.Iset_info	Interface for the SMT-LIB set-info command.
ICommand.Iset_logic	Interface for the SMT-LIB set-logic command.
ICommand.Iset_option	Interface for the SMT-LIB set-option command.
IExpr	This interface represents the functionality for any class implementing an SMT-LIB term or formula
IExpr.IAsIdentifier	This interface represents SMT-LIB identifiers that are sort qualifiers on function ids
IExpr.IAttribute	This interface represents an SMT-LIB attribute-value pair; the value may be null (keyword-only attribute).
IExpr.IAttributedExpr	This interface represents an SMT-LIB expression with attributes.
IExpr.IBinaryLiteral	This interface represents SMT-LIB binary literals
IExpr.IBinding	This interface represents a binding of a parameter and an expression
IExpr.IConstructor	A constructor declaration within a datatype; pairs a constructor name with its selectors.
IExpr.IDecimal	This interface represents non-negative decimal numbers of arbitrary size (i.e.
IExpr.IDeclaration	This interface represents a declaration of a parameter and its sort
IExpr.IError	This interface represents an error, e.g.
IExpr.IExists	This interface represents an SMT-LIB quantified exists expression
IExpr.IFactory	The interface defining the factory type for producing objects of various subtypes of IExpr; the IPos argument is an optional argument giving information about the textual position of an expression.
IExpr.IFcnExpr	This interface represents SMT-LIB expressions that are a function identifier applied to one or more arguments.
IExpr.IForall	This interface represents an SMT-LIB quantified forall expression
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.
IExpr.IHexLiteral	This interface represents SMT-LIB hex literals
IExpr.IIdentifier	This interface represents SMT-LIB identifiers (either ids or parameterized ids)
IExpr.IKeyword	This interface represents SMT-LIB attribute and infoflag names.
IExpr.ILambda	This interface represents an SMT-LIB lambda expression: (lambda (sorted_var+) term).
IExpr.ILet	This interface represents an SMT-LIB let-expression
IExpr.ILiteral	This interface represents all literal (explicit constant) expressions.
IExpr.IMatch	This interface represents an SMT-LIB 2.7 match expression.
IExpr.IMatchCase	This interface represents one case in a match expression: a pattern and its body.
IExpr.INumeral	This interface represents non-negative integers of arbitrary size.
IExpr.IParameterizedIdentifier	This interface represents SMT-LIB parameterized identifiers
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.
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 ).
IExpr.IQualifiedIdentifier	This interface represents SMT-LIB identifiers for function ids (either ids or parameterized ids or as-type identifiers)
IExpr.ISelector	A selector declaration within a constructor; pairs a selector name with its result sort.
IExpr.ISortDeclaration	Pairs a sort name with its arity; used in declare-datatype and declare-datatypes.
IExpr.IStringLiteral	This interface represents SMT-LIB string literals
IExpr.ISymbol	This interface represents SMT-LIB ids; equal ids have equal (using .equals) values of value().
ILogic	This interface represents a definition of an SMT_LIB logic
INode	This interface is defined and implemented as a marker that the accept method is available and to ensure that subtypes implement the accept method.
IParser	This is the interface to a parser for SMT-LIB.
IParser.ElementParser	Functional interface for a lambda that parses one element from a Parser.
IParser.IFactory	The interface for the parser/printer factory
IParser.ParserException	An exception thrown if parsing is to be aborted.
IPos	This is an interface that supplies information about a range in textual position within a source of characters.
IPos.IPosable	This interface identifies classes that can have their position set
IPrinter	An interface for printers to concrete syntax; factories are shared with Parsers in IParser.IFactory.
IResponse	This interface represents responses that can be received from SMT-LIB commands.
IResponse.IAssertionsResponse	Response type for get-assertions, carrying the list of currently asserted formulae.
IResponse.IAssignmentResponse	Response type for get-assignment, carrying a list of name-Boolean pairs.
IResponse.IAttributeList	Response type for get-info, carrying a list of attribute key-value pairs.
IResponse.IError	The interface for error responses
IResponse.IPair	An interface for simple pairs of objects; used to represent value/assignment response items
IResponse.IProofResponse	Response type for get-proof.
IResponse.IUnsatAssumptionsResponse	Response type for get-unsat-assumptions, carrying the assumptions (terms, e.g.
IResponse.IUnsatCoreResponse	Response type for get-unsat-core, carrying the names of the formulae in the unsat core.
IResponse.IValueResponse	Response type for get-value, carrying a list of expression-value pairs.
ISort	The interface for an SMT-LIB concept of a Sort.
ISort.IAbbreviation	This interface represents a new Sort symbol designating an abbreviation for a (possibly parameterized) sort expression.
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.
ISort.IDatatype	The interface for a datatype declaration (used in declare-datatype and declare-datatypes).
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.
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.
ISort.IParameter	The interface for a sort parameter, as used in sort abbreviations (including in the defining expression).
ISource	This interface represents sources of characters.
ITheory	This interface represents a definition of an SMT-LIB theory
IVisitor	This is a visitor interface for visitors over IExpr ASTs.
IVisitor.VisitorException	An Exception class to use if there is a problem during execution of an IVisitor (e.g.
SMT.Configuration	The configuration object holds the values of all of the current options (e.g.
SMT.Configuration.SMTLIB	Enumeration of the supported SMT-LIB versions, in declaration order from oldest to newest.

Classes in org.smtlib used by org.smtlib.solvers

Class	Description
AbstractSolver	This class implements the operations of the org.smtlib.ISolver interface that map directly onto a single translated command sent to the solver process, with the expected response of a fully SMT-LIB compliant solver (a flat success/error/sat/unsat/ unknown/unsupported, or a bare value/attribute-pair for get-option/get-info): the command is translated with AbstractSolver.translate(INode) and sent via AbstractSolver.sendCommand(ICommand).
AbstractSolver.StackChange	The kinds of command that change the assertion stack: each returns a conforming solver to assert mode, where the get- commands about the last check are errors (declare-const is declare-fun, declare-datatypes is declare-datatype, define-funs-rec is define-fun-rec), as does a set-logic that a solver accepts after a check (SMT-LIB makes that an error, but --relax may allow it)
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.
ICommand	This interface is the generic interface to command classes, providing functionality to type-check the command and to execute it.
ICommand.Ideclare_const	Interface for the SMT-LIB declare-const command.
ICommand.Ideclare_datatype	Interface for the SMT-LIB declare-datatype command.
ICommand.Ideclare_datatypes	Interface for the SMT-LIB declare-datatypes command.
ICommand.Ideclare_fun	Interface for the SMT-LIB declare-fun command.
ICommand.Ideclare_sort	Interface for the SMT-LIB declare-sort command.
ICommand.Ideclare_sort_parameter	Interface for the SMT-LIB declare-sort-parameter command.
ICommand.Idefine_const	Interface for the SMT-LIB define-const command.
ICommand.Idefine_fun	Interface for the SMT-LIB define-fun command.
ICommand.Idefine_fun_rec	Interface for the SMT-LIB define-fun-rec command.
ICommand.Idefine_funs_rec	Interface for the SMT-LIB define-funs-rec command.
ICommand.Idefine_sort	Interface for the SMT-LIB define-sort command.
ICommand.IScript	Interface to be implemented by all objects representing SMT-LIB scripts.
IExpr	This interface represents the functionality for any class implementing an SMT-LIB term or formula
IExpr.IAsIdentifier	This interface represents SMT-LIB identifiers that are sort qualifiers on function ids
IExpr.IAttribute	This interface represents an SMT-LIB attribute-value pair; the value may be null (keyword-only attribute).
IExpr.IAttributedExpr	This interface represents an SMT-LIB expression with attributes.
IExpr.IBinaryLiteral	This interface represents SMT-LIB binary literals
IExpr.IBinding	This interface represents a binding of a parameter and an expression
IExpr.IConstructor	A constructor declaration within a datatype; pairs a constructor name with its selectors.
IExpr.IDecimal	This interface represents non-negative decimal numbers of arbitrary size (i.e.
IExpr.IDeclaration	This interface represents a declaration of a parameter and its sort
IExpr.IError	This interface represents an error, e.g.
IExpr.IExists	This interface represents an SMT-LIB quantified exists expression
IExpr.IFcnExpr	This interface represents SMT-LIB expressions that are a function identifier applied to one or more arguments.
IExpr.IForall	This interface represents an SMT-LIB quantified forall expression
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.
IExpr.IHexLiteral	This interface represents SMT-LIB hex literals
IExpr.IIdentifier	This interface represents SMT-LIB identifiers (either ids or parameterized ids)
IExpr.IKeyword	This interface represents SMT-LIB attribute and infoflag names.
IExpr.ILambda	This interface represents an SMT-LIB lambda expression: (lambda (sorted_var+) term).
IExpr.ILet	This interface represents an SMT-LIB let-expression
IExpr.IMatch	This interface represents an SMT-LIB 2.7 match expression.
IExpr.IMatchCase	This interface represents one case in a match expression: a pattern and its body.
IExpr.INumeral	This interface represents non-negative integers of arbitrary size.
IExpr.IParameterizedIdentifier	This interface represents SMT-LIB parameterized identifiers
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.
IExpr.ISelector	A selector declaration within a constructor; pairs a selector name with its result sort.
IExpr.ISortDeclaration	Pairs a sort name with its arity; used in declare-datatype and declare-datatypes.
IExpr.IStringLiteral	This interface represents SMT-LIB string literals
IExpr.ISymbol	This interface represents SMT-LIB ids; equal ids have equal (using .equals) values of value().
ILogic	This interface represents a definition of an SMT_LIB logic
INode	This interface is defined and implemented as a marker that the accept method is available and to ensure that subtypes implement the accept method.
IPos	This is an interface that supplies information about a range in textual position within a source of characters.
IPrinter	An interface for printers to concrete syntax; factories are shared with Parsers in IParser.IFactory.
IResponse	This interface represents responses that can be received from SMT-LIB commands.
IResponse.IAssertionsResponse	Response type for get-assertions, carrying the list of currently asserted formulae.
IResponse.IAssignmentResponse	Response type for get-assignment, carrying a list of name-Boolean pairs.
IResponse.IAttributeList	Response type for get-info, carrying a list of attribute key-value pairs.
IResponse.IError	The interface for error responses
IResponse.IProofResponse	Response type for get-proof.
IResponse.IUnsatAssumptionsResponse	Response type for get-unsat-assumptions, carrying the assumptions (terms, e.g.
IResponse.IUnsatCoreResponse	Response type for get-unsat-core, carrying the names of the formulae in the unsat core.
IResponse.IValueResponse	Response type for get-value, carrying a list of expression-value pairs.
ISolver	This is the interface to be implemented by any solver adapter; there is a method for each SMT-LIB command.
ISort.IAbbreviation	This interface represents a new Sort symbol designating an abbreviation for a (possibly parameterized) sort expression.
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.
ISort.IDatatype	The interface for a datatype declaration (used in declare-datatype and declare-datatypes).
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.
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.
ISort.IParameter	The interface for a sort parameter, as used in sort abbreviations (including in the defining expression).
ITheory	This interface represents a definition of an SMT-LIB theory
IVisitor	This is a visitor interface for visitors over IExpr ASTs.
IVisitor.VisitorException	An Exception class to use if there is a problem during execution of an IVisitor (e.g.
SMT.Configuration	The configuration object holds the values of all of the current options (e.g.
SymbolTable	This class manages a symbol table used for storing definitions and looking up ids in expressions.