All Classes and Interfaces
Class
Description
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).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.The kinds of response a command has besides an error or unsupported (#149)
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)
Implements the assert command
Implements the check-sat command
Implements the check-sat-assuming command
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.Implements the declare-const command (syntactic sugar for declare-fun with no argument sorts)
Implements the declare-datatype command
Implements the declare-datatypes command
Implements the declare-fun command
Implements the declare-sort command
Implements the declare-sort-parameter command
Implements the define-const command: syntactic sugar for define-fun with no parameters
Implements the define-fun command
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.Implements the define-funs-rec command
Implements the define-sort command
Implements the echo command
Implements the non-standard exec command
Implements the exit command
Implements the get-assertions command
Implements the get-assignment command
Implements the get-info command.
Implements the get-model command
Implements the get-option command
Implements the get-proof command
Implements the get-unsat-assumptions command
Implements the get-unsat-core command
Implements the get-value command
Implements the pop command
Implements the push command
Implements the reset command
Implements the reset-assertions command
Implements the set-info command
Implements the set-logic command.
Implements the set-option command
Implements the non-standard what command.
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.
This interface is used to create prompters.
This class implements a CharSequence that obtains its characters from a Reader.
This class implements a CharSequence that obtains its characters from a ServerSocket.
This abstract class is the base class for all commands within this implementation.
Common base for the difference logics QF_IDL and QF_RDL.
The Driver class is a client that can send commands to the SMT application acting as a server.
Implements a factory for SMT-LIB expressions using the standard concrete syntax.
This is the factory for classes that are part of this particular concrete representation
of SMT-LIB syntax: Parser, Printer, Source for parsers.
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.
This interface is the generic interface to command classes, providing functionality
to type-check the command and to execute it.
Interface for the SMT-LIB
assert command.Interface for the SMT-LIB
check-sat command.Interface for the SMT-LIB
check-sat-assuming command.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).Interface for the SMT-LIB
declare-const command.Interface for the SMT-LIB
declare-datatype command.Interface for the SMT-LIB
declare-datatypes command.Interface for the SMT-LIB
declare-fun command.Interface for the SMT-LIB
declare-sort command.Interface for the SMT-LIB
declare-sort-parameter command.Interface for the SMT-LIB
define-const command.Interface for the SMT-LIB
define-fun command.Interface for the SMT-LIB
define-fun-rec command.Interface for the SMT-LIB
define-funs-rec command.Interface for the SMT-LIB
define-sort command.Interface for the SMT-LIB
echo command.Interface for the SMT-LIB
exit command.This is the interface to be used by a concrete ICommand factory.
This interface defines classes that implement techniques for mapping a command name to a class
that implements that command.
Interface for the SMT-LIB
get-assertions command.Interface for the SMT-LIB
get-assignment command.Interface for the SMT-LIB
get-info command.Interface for the SMT-LIB
get-model command (non-standard extension).Interface for the SMT-LIB
get-option command.Interface for the SMT-LIB
get-proof command.Interface for the SMT-LIB
get-unsat-assumptions command.Interface for the SMT-LIB
get-unsat-core command.Interface for the SMT-LIB
get-value command.Interface for the SMT-LIB
pop command.Interface for the SMT-LIB
push command.Interface for the SMT-LIB
reset command.Interface for the SMT-LIB
reset-assertions command.Interface to be implemented by all objects representing SMT-LIB scripts.
Interface for the SMT-LIB
set-info command.Interface for the SMT-LIB
set-logic command.Interface for the SMT-LIB
set-option command.Interface for the SMT-LIB
exec command (non-standard extension).This interface represents the functionality for any class implementing an SMT-LIB term or formula
This interface represents SMT-LIB identifiers that are sort qualifiers on function ids
This interface represents an SMT-LIB attribute-value pair; the value may be null (keyword-only attribute).
This interface represents an SMT-LIB expression with attributes.
This interface represents SMT-LIB binary literals
This interface represents a binding of a parameter and an expression
A constructor declaration within a datatype; pairs a constructor name with its selectors.
This interface represents non-negative decimal numbers of arbitrary size
(i.e.
This interface represents a declaration of a parameter and its sort
This interface represents an error, e.g.
This interface represents an SMT-LIB quantified exists expression
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.
This interface represents SMT-LIB expressions that are a function identifier applied to one or more arguments.
This interface represents an SMT-LIB quantified forall expression
A function declaration: a name, a parameter list (sorted variables), and a result sort;
used in the header list of define-funs-rec.
This interface represents SMT-LIB hex literals
This interface represents SMT-LIB identifiers (either ids or parameterized ids)
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.
This interface represents SMT-LIB attribute and infoflag names.
This interface represents an SMT-LIB lambda expression:
(lambda (sorted_var+) term).This interface represents an SMT-LIB let-expression
This interface represents all literal (explicit constant) expressions.
This interface represents an SMT-LIB 2.7 match expression.
This interface represents one case in a match expression: a pattern and its body.
This interface represents non-negative integers of arbitrary size.
This interface represents SMT-LIB parameterized identifiers
This interface represents a match pattern: either a bare symbol (variable/nullary-constructor)
or a constructor applied to zero or more variable symbols.
This interface represents the value of a
:pattern attribute: a list of terms
(a multi-pattern), written in the concrete syntax as ( t1 ... tn ).This interface represents SMT-LIB identifiers for function ids (either ids or parameterized ids
or as-type identifiers)
A selector declaration within a constructor; pairs a selector name with its result sort.
Pairs a sort name with its arity; used in declare-datatype and declare-datatypes.
This interface represents SMT-LIB string literals
This interface represents SMT-LIB ids; equal ids have equal (using .equals) values
of value().
This interface represents the functionality of an SMT-LIB language - the combination of one or more theories and various restrictions
on the permitted expressions.
An interface to indicate AST classes that are also lexical tokens in the
concrete syntax.
This interface represents a definition of an SMT_LIB logic
This interface is defined and implemented as a marker that
the accept method is available and to ensure that
subtypes implement the accept method.
This is the interface to a parser for SMT-LIB.
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.
Functional interface for a lambda that parses one element from a Parser.
The interface for the parser/printer factory
An exception thrown if parsing is to be aborted.
An exception to be thrown if there is an unrecoverable problem scanning the syntax
This is an interface that supplies information about a range in textual position within
a source of characters.
This interface identifies classes that can have their position set
An interface for printers to concrete syntax; factories are shared with Parsers
in IParser.IFactory.
This interface represents responses that can be received from SMT-LIB commands.
Response type for get-assertions, carrying the list of currently asserted formulae.
Response type for get-assignment, carrying a list of name-Boolean pairs.
Response type for get-info, carrying a list of attribute key-value pairs.
The interface for error responses
The factory interface for creating the standard IResponse singleton and structured instances.
An interface for simple pairs of objects; used to represent value/assignment response items
Response type for get-proof.
Response type for get-unsat-assumptions, carrying the assumptions (terms, e.g.
Response type for get-unsat-core, carrying the names of the formulae in the unsat core.
Response type for get-value, carrying a list of expression-value pairs.
This interface represents S-expressions as used in SMT-LIB;
they are used as values for attributes in the standard concrete
syntax.
Represents a sequence of S-expressions
Represents a single S-expression token
This is the interface to be implemented by any solver adapter;
there is a method for each SMT-LIB command.
Thrown by
SMT.Configuration.createSolver(java.lang.String, java.lang.String) when a solver adapter cannot be
resolved, constructed, or fails to launch.The interface for an SMT-LIB concept of a Sort.
This interface represents a new Sort symbol designating an
abbreviation for a (possibly parameterized) sort expression.
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.
The interface for a datatype declaration (used in declare-datatype and declare-datatypes).
A super-interface for definitions of new sort ids.
Represents an erroneous sort definition; by having an actual IDefinition,
redundant cascading errors are suppressed.
The interface for a Sort-creating factory.
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.
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.
The interface for a sort parameter, as used in sort abbreviations
(including in the defining expression).
This interface represents sources of characters.
This interface represents a definition of an SMT-LIB theory
This is a visitor interface for visitors over IExpr ASTs.
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.
An Exception class to use if there is a problem during execution of an
IVisitor (e.g.
Interface for the SMT-LIB
what command (non-standard extension).Converts character sequences (from ISource) into tokens, presuming the standard SMT-LIBv2 concrete syntax.
An interface used for punctuation tokens that can be retrieved from the parser input.
This class is used as a collection point for all output.
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.
Output whose content is not yet known, e.g.
Common base for this package's per-logic syntactic-restriction classes (QF_IDL, LRA,
QF_UF, etc).
This logic does not allow uninterpreted functions or nonlinear arithmetic terms
Parses the standard SMT-LIB concrete syntax to produce ASTs of objects that
are instances of the org.smtlib.* interfaces.
Represents a range of characters in a source - used to indicate the location of errors
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).
An implementation of IPosable, holding an instance of Pos,
that can be used as a base class if necessary
A Posable that also implements INode, with toString() delegating to Printer.
An implementation of the ISource interface
This class writes out SMT-LIB ASTs as concrete S-expression syntax; aside from white space
between tokens it should simply reverse what the Parser class does.
Functional interface for the argument-printing lambda passed to
Printer.printCommand(org.smtlib.ICommand, org.smtlib.sexpr.Printer.PrintArgs).This logic does not allow quantifiers or uninterpreted functions
This logic does not allow quantifiers; all array terms have sort (Array (_ BitVec i) (_ BitVec j))
Not an official SMT-LIB logic -- see QF_FP.smt2's own :notes: a jSMTLIB-invented
convenience logic for exercising the FloatingPoint theory in this project's own test
suite without needing the broad ALL logic.
QF_IDL atoms (QF_IDL.smt2): (op x y), (op (- x y) n) and (op (- x y) (- n)), with x, y
free constants of sort Int and n a numeral.
QF_RDL atoms (QF_RDL.smt2): (op x y), (op (- x y) c), (op (- (+ x ...
Quantifier-free, with uninterpreted functions and sorts permitted -- identical
restrictions to QF_UF, all inherited from it (the bit-vector vs.
This class holds subclasses that are implementations of the various IResponse interfaces.
Implements the IResponse.IAssertionsResponse interface
Implements the IResponse.IAssignmentResponse interface
Implements the IResponse.IError interface
Implements the IResponse.IFactory interface
Implements the IResponse.IPair interface
Implements the IResponse.IProofResponse interface
Implementation of IAttributeList: a list of attributes returned by get-info.
Implements the IResponse.IUnsatAssumptionsResponse interface
Implements the IResponse.IUnsatCoreResponse interface
Implements the IResponse.IValueResponse interface
This class implements the IScript interface, representing SMT-LIB command scripts
This is the root class for S-expressions in the concrete syntax
The class corresponding to sequences of S-expressions
Represents a single S-expression token with intrinsic type T
This is the main class for the SMT-LIB tool.
The configuration object holds the values of all of the current options (e.g.
Enumeration of the supported SMT-LIB versions, in declaration order from oldest to newest.
Marker interface for configuration objects; reserved for future extension.
This class is used to turn internal bugs that we do not want to try
to recover into exceptions that can be reported
This class is a prompter used when more data is needed from a data source
This class defines a number of subclasses that implement the SMT-LIB abstract AST;
they are used by commands and expressions.
This class represents an SMT as-identifier AST
Represents an SMT-LIB attribute: a keyword optionally paired with a value.
Represents an SMT-LIB attributed expression (
(! expr attrs...)).Represents an SMT-LIB binary literal (e.g.
Represents a let-binding: a symbol bound to an expression.
Represents a constructor declaration within a datatype, consisting of a name and a list of selectors.
Represents a datatype body: a list of constructors and (for parametric forms) a list of sort parameter symbols.
This class represents an SMT Decimal literal expression or syntax token
Represents a sorted variable declaration (parameter name and its sort), used in forall/exists/define-fun.
Represents an expression-level error node inserted during parsing to allow error recovery.
Represents an SMT-LIB existential quantifier expression.
Represents a function-application expression: a qualified identifier applied to a list of argument expressions.
Represents an SMT-LIB universal quantifier expression.
Represents a function declaration header (name, sorted parameters, result sort), used in define-funs-rec.
Represents an SMT-LIB hex literal (e.g.
This class represents an SMT Keyword syntax token
Represents an SMT-LIB lambda expression (SMT-LIB 2.7ff, HO-Core theory).
Represents an SMT-LIB let expression: a list of bindings and a body expression.
Abstract base class for all literal value AST nodes; holds the typed value and provides a shared implementation.
Represents an SMT-LIB 2.7 match expression: an expression matched against a list of cases.
Represents a single case in a match expression: a pattern and its result body.
This class represents an SMT Numeral expression or syntax token
This class represents an SMT parameterized-identifier AST (e.g.
Represents a match pattern: a constructor name applied to zero or more variable symbols.
Represents the value of a
:pattern attribute: a list of trigger terms.Represents a selector declaration within a datatype constructor.
Represents a sort declaration (symbol and arity) used in declare-datatype and declare-datatypes.
This class represents an SMT String literal expression or syntax token
This class represents an SMT Symbol
The adapter for Alt-Ergo (developed against 2.6.3 on Linux), run as
alt-ergo --input smtlib2
--output smtlib2, reading the script from standard input.This class is an adapter for Bitwuzla (bit-vectors, floating-point, arrays and
uninterpreted functions -- no arithmetic logics, no datatypes).
This class is an adapter for cvc5, on the assumption that it is (or should be) a
fully SMT-LIB compliant solver: it is a concrete, silent inheritor of
AbstractSolver — only the startup command line (cvc5 needs --incremental
to accept push/pop at all, and --quiet to suppress informational stderr
chatter that would otherwise fool SolverProcess's stdout/stderr-preference
heuristic) and Solver_cvc5.start() (process lifecycle) are overridden.The adapter that drives the Simplify solver.
This class is an adapter that takes the SMT-LIB ASTs and translates them into SMT
commands over a solver process speaking plain SMT-LIB, for a solver assumed to be
fully SMT-LIB compliant.
This class is an adapter for SMTInterpol (a Java SMT solver launched as
java -jar smtinterpol-VERSION.jar, not a native executable): it is a concrete,
silent inheritor of AbstractSolver -- the base launch command is declared in
jsmtlib.properties via org.smtlib.solver_smtinterpol-2.5.command (see SMT.startSolver's
%exec% placeholder substitution), so only the conditional timeout flag and
Solver_smtinterpol.start()/AbstractSolver.exit() (process lifecycle) are handled here, besides the
get- command checks below.This class is a Solver implementation that simply type-checks formulae and checks that
commands are used correctly; it does not do any proving.
This class is an adapter that takes the SMT-LIB ASTs and translates them into yices2 commands
yices2 2.6.5: by default it answers get-model in yices's own model format, not SMT-LIB's; with
--smt2-model-format it answers
(model (define-fun ...) ...), whose wrapper
AbstractSolver#modelResponse removes.This class is an adapter that takes the SMT-LIB ASTs and translates them into Z3 commands
This is a special handler for Z3 4.3.2, as opposed to other revisions of Z3 4.3.
z3 4.5.0: as recent z3, except that it writes echo's text unquoted even with SMTLIB2_COMPLIANT
(4.6 and later quote it), so where it ends cannot be found (#136), the response to echo is its
argument; and it rejects every check-sat-assuming (see translate)
This class is an adapter for recent z3 versions (empirically verified against 4.8.12 and
4.10.2), on the assumption that they are (or should be) fully SMT-LIB compliant: it is a
concrete, silent inheritor of
AbstractSolver -- only the startup command line and
Solver_z3_recent.start()/AbstractSolver.exit() (process lifecycle) are overridden.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.The capabilities that can be queried;
SolverCapabilities.Capability.token is the name used in the propertiesThe answer to a query; UNKNOWN means the solver's entry does not record the capability
This class implements launching, writing to, and reading responses from a
launched process (in particular, solver processes).
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()).
Wraps an exception thrown because of a failure in the prover
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.
For internal use only (public so that the tests can reach it); not part of the API.
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 oneThis class implements the abstract ISort interface
Implements a Sort abbreviation (parameterized definition, possibly with no parameters)
Represents a sort expression consisting of a sort symbol or sort abbreviation symbol applied to a
corresponding number of sort arguments
A placeholder sort definition used when a sort declaration is ill-formed, to suppress cascading errors.
Represents a new sort symbol, with a given identifier and arity
Represents the class of the sort of a function symbol.
Represents a Sort parameter, such as in either the parameter list or the expression of a Sort abbreviation
This class manages a symbol table used for storing definitions and looking up ids in expressions.
An object that holds all the information about the defined symbol (or aliased definition).
An iterator over all of the Symbols in the symbol scope stack from the top-most scope
on down.
This class is a visitor that type-checks a formula
Constants and reserved-word sets specific to the S-expression concrete syntax.
A class of static utility methods and constants for the SMT-LIB package.
A checked exception used internally to propagate SMT-LIB errors that carry an IResponse.IError.
Provides the release version string for jSMTLIB, read from the
org.smtlib.resources.version
resource bundle.