Package org.smtlib

package 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. For a tool that encapsulates this functionality as an Eclipse plug-in, see the companion package org.smtlib.plugin.

Related Packages

Package	Description
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.

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.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.
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.
CharSequenceReader	This class implements a CharSequence that obtains its characters from a Reader.
CharSequenceSocket	This class implements a CharSequence that obtains its characters from a ServerSocket.
Driver	The Driver class is a client that can send commands to the SMT application acting as a server.
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<TT extends IAttributeValue>	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.AbortInputException	An exception to be thrown if parsing is to be intentionally aborted (and restarted, ignoring any tokens since the last successful call to the parser.
IParser.ElementParser<T>	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.
IParser.SyntaxException	An exception to be thrown if there is an unrecoverable problem scanning the syntax
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<T1,T2>	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<T>	This is a visitor interface for visitors over IExpr ASTs.
IVisitor.TreeVisitor<T>	This class is an implementation of IVisitor meant for further derivation: each visitor is implemented to visit its children without doing anything else; the default return value is null.
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	This is the main class for the SMT-LIB tool.
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.
SMT.InternalException	This class is used to turn internal bugs that we do not want to try to recover into exceptions that can be reported
SMT.Prompter	This class is a prompter used when more data is needed from a data source
SolverCapabilities	Whether a solver supports a capability, as recorded per solver name in jsmtlib.properties (#157): org.smtlib.solver_<name>.capabilities=strings,-proofs,... -- a name records a supported capability, a -name an unsupported one.
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.NoResponseException	Thrown when a command gets literally no response from the solver -- either because the process was already confirmed dead before this command was even written (the pre-write liveness check in send()), or because its output stream closed while listening without ever producing anything on either stream (the forced-EOF check in listen()).
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	For internal use only (public so that the tests can reach it); not part of the API.
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	This class is a visitor that type-checks a formula
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.
Version	Provides the release version string for jSMTLIB, read from the org.smtlib.resources.version resource bundle.