Index

A B C D E F G H I J K L M N O P Q R S T U V W X Y Z 
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form

S

sameLineTrailingEnd - Variable in class org.smtlib.sexpr.Lexer
 
sameLineTrailingStart - Variable in class org.smtlib.sexpr.Lexer
 
sameLineTrailingText - Variable in class org.smtlib.sexpr.Lexer
Whitespace/comment text, if any, found between the previous token and the first line terminator after it -- i.e.
sameSort(ISort, ISort) - Static method in class org.smtlib.logic.Logic
Whether sort, with abbreviations expanded, is structurally the same as allowed
sat() - Method in class org.smtlib.impl.Response.Factory
 
sat() - Method in interface org.smtlib.IResponse.IFactory
 
SAT - Static variable in class org.smtlib.impl.Response
 
save(IExpr, ISort) - Method in class org.smtlib.TypeChecker
 
savedlp - Variable in class org.smtlib.sexpr.Parser
This field is used to communicate the beginning LP while parsing commands
SBV_TO_INT - Static variable in class org.smtlib.Utils
 
script - Variable in class org.smtlib.ext.C_exec
The command script to be run
script() - Method in class org.smtlib.ext.C_exec
Returns a reference to the command script to be run
script() - Method in interface org.smtlib.ext.Iexec
Returns the script to execute.
script() - Method in interface org.smtlib.ICommand.IFactory
Creates an empty script, with no filename and no commands, ready to have commands added via ICommand.IScript.add(ICommand).
script() - Method in class org.smtlib.impl.Factory
 
script(IExpr.IStringLiteral, List<ICommand>) - Method in interface org.smtlib.ICommand.IFactory
Creates a script object containing the given filename or the given set of commands.
script(IExpr.IStringLiteral, List<ICommand>) - Method in class org.smtlib.impl.Factory
 
Script - Class in org.smtlib.impl
This class implements the IScript interface, representing SMT-LIB command scripts
Script() - Constructor for class org.smtlib.impl.Script
Constructs a script with no commands
Script(IExpr.IStringLiteral, List<ICommand>) - Constructor for class org.smtlib.impl.Script
Constructs the script with the given list of commands, hijacking the list itself
second - Variable in class org.smtlib.impl.Response.Pair
 
second() - Method in class org.smtlib.impl.Response.Pair
 
second() - Method in interface org.smtlib.IResponse.IPair
 
seed - Variable in class org.smtlib.SMT.Configuration
If non-zero, a seed to pass to the solver to initialize its random number generator (--seed, non-negative)
SELECT - Static variable in class org.smtlib.Utils
 
selector(IExpr.ISymbol, ISort) - Method in interface org.smtlib.IExpr.IFactory
Creates a selector declaration.
selector(IExpr.ISymbol, ISort) - Method in class org.smtlib.impl.Factory
 
Selector(IExpr.ISymbol, ISort) - Constructor for class org.smtlib.impl.SMTExpr.Selector
Creates a selector with the given name and result sort.
selectors - Variable in class org.smtlib.impl.SMTExpr.Constructor
 
selectors() - Method in interface org.smtlib.IExpr.IConstructor
 
selectors() - Method in class org.smtlib.impl.SMTExpr.Constructor
 
selfReportsImmediateExit() - Method in class org.smtlib.AbstractSolver
Overridden by a subclass whose target solver's :error-behavior is immediate-exit (e.g.
selfReportsImmediateExit() - Method in class org.smtlib.solvers.Solver_bitwuzla
 
selfReportsImmediateExit() - Method in class org.smtlib.solvers.Solver_cvc5
 
selfReportsImmediateExit() - Method in class org.smtlib.solvers.Solver_yices2
yices2 self-reports (get-info :error-behavior) as immediate-exit and its process does exit after some (not all) errors -- see AbstractSolver#sendCommand(ICommand, boolean), which uses this to pause briefly after any error response, giving a genuinely-exiting process time to finish dying before the next command's liveness check runs.
send() - Method in class org.smtlib.Driver
Sends the options and commands to the port; returns the exit code corresponding to the response from the last command.
send(boolean, String...) - Method in class org.smtlib.SolverProcess
Sends all the given text arguments, then (if listen is true) listens for the designated end marker text
sendAndListen(String...) - Method in class org.smtlib.SolverProcess
Sends all the given text arguments, then listens for the designated end marker text
sendChange(AbstractSolver.StackChange, ICommand) - Method in class org.smtlib.AbstractSolver
Sends a command that changes the assertion stack, recording it (see recordChange)
sendCommand(String) - Method in class org.smtlib.solvers.Solver_z3_4_3
 
sendCommand(ICommand) - Method in class org.smtlib.AbstractSolver
Translates the given command and sends it to the solver process, returning the parsed response.
sendCommand(ICommand) - Method in class org.smtlib.solvers.Solver_z3_4_3
 
sendExitCommand() - Method in class org.smtlib.AbstractSolver
Sends the exit command, tolerating the solver producing literally no response (SolverProcess.NoResponseException) as a benign, expected outcome rather than an error -- many solvers legitimately print nothing before terminating in response to exit.
sendFailure(Exception, IResponse) - Method in class org.smtlib.AbstractSolver
The response to a command whose sending failed with e: if the solver process has exited (waiting briefly for that), timeout if its whole-run time limit ended it, else the error AbstractSolver.SOLVER_EXITED; otherwise otherwise
sendFailure(String, Exception) - Method in class org.smtlib.AbstractSolver
As AbstractSolver.sendFailure(Exception, IResponse), with an error giving text and e otherwise
sendNoListen(String...) - Method in class org.smtlib.SolverProcess
Sends all the given text arguments, but does not wait for a response
sendPipelined(ICommand) - Method in class org.smtlib.AbstractSolver
Executes a command for which AbstractSolver.pipelines(ICommand) is true, sending it to the solver without waiting for the response.
sendScriptText(boolean, String...) - Method in class org.smtlib.AbstractSolver
Sends text for the command being executed (not text the adapter adds of its own accord), first setting linesOffset for it; returns the response if listen is true, else null
sendScriptText(boolean, String...) - Method in class org.smtlib.solvers.Solver_z3_4_3_2
Corrects a non-conformance of z3 4.3.2: run with smtlib2_compliant=true, as this adapter runs it, a check-sat of a problem with quantifiers, before any push, makes z3 parse its built-in pattern database (111 commands) with print-success on, so a "success" line per command precedes the result.
sendSeed() - Method in class org.smtlib.AbstractSolver
Passes --seed, if given, as the standard :random-seed option, for an adapter whose solver uses that option; called from start(), while :print-success is true.
Seq() - Constructor for class org.smtlib.sexpr.Sexpr.Seq
 
Seq(List<IExpr.IAttribute<? extends IAttributeValue>>) - Constructor for class org.smtlib.impl.Response.Seq
 
Seq(List<ISexpr>) - Constructor for class org.smtlib.sexpr.Sexpr.Seq
 
Seq(IExpr.IAttribute<T>) - Constructor for class org.smtlib.impl.Response.Seq
 
serverSocket - Variable in class org.smtlib.CharSequenceSocket
The socket from which characters are read
set_info(IExpr.IKeyword, IAttributeValue) - Method in class org.smtlib.AbstractSolver
 
set_info(IExpr.IKeyword, IAttributeValue) - Method in interface org.smtlib.ICommand.IFactory
Creates a set-info command object.
set_info(IExpr.IKeyword, IAttributeValue) - Method in class org.smtlib.impl.Factory
 
set_info(IExpr.IKeyword, IAttributeValue) - Method in interface org.smtlib.ISolver
Annotates the problem with an info attribute (e.g.
set_info(IExpr.IKeyword, IAttributeValue) - Method in class org.smtlib.solvers.Solver_simplify
See Solver_test.set_info(IKeyword,IAttributeValue).
set_info(IExpr.IKeyword, IAttributeValue) - Method in class org.smtlib.solvers.Solver_test
 
set_logic(String, IPos) - Method in class org.smtlib.AbstractSolver
A set-logic the solver accepts ends sat or unsat mode; one it rejects (as SMT-LIB requires outside start mode) changes nothing.
set_logic(String, IPos) - Method in interface org.smtlib.ISolver
Sets the logic the solver should use.
set_logic(String, IPos) - Method in class org.smtlib.solvers.Solver_bitwuzla
Bitwuzla (0.9.1) accepts a second set-logic, which SMT-LIB forbids outside start mode, so that is reported here (--relax allows it).
set_logic(String, IPos) - Method in class org.smtlib.solvers.Solver_simplify
 
set_logic(String, IPos) - Method in class org.smtlib.solvers.Solver_test
 
set_logic(String, IPos) - Method in class org.smtlib.solvers.Solver_z3_4_3
 
set_logic(IExpr.ISymbol) - Method in interface org.smtlib.ICommand.IFactory
Creates a set-logic command object.
set_logic(IExpr.ISymbol) - Method in class org.smtlib.impl.Factory
 
SET_LOGIC - Enum constant in enum class org.smtlib.AbstractSolver.StackChange
 
set_option(IExpr.IKeyword, IAttributeValue) - Method in class org.smtlib.AbstractSolver
 
set_option(IExpr.IKeyword, IAttributeValue) - Method in interface org.smtlib.ICommand.IFactory
Creates a set-option command object.
set_option(IExpr.IKeyword, IAttributeValue) - Method in class org.smtlib.impl.Factory
 
set_option(IExpr.IKeyword, IAttributeValue) - Method in interface org.smtlib.ISolver
Sets an SMT-LIB option.
set_option(IExpr.IKeyword, IAttributeValue) - Method in class org.smtlib.solvers.Solver_simplify
Simplify has no set-option; options are kept here, and the :produce- options answer unsupported since Simplify cannot produce models, proofs or cores
set_option(IExpr.IKeyword, IAttributeValue) - Method in class org.smtlib.solvers.Solver_test
 
set_option_impl(IExpr.IKeyword, IAttributeValue) - Method in class org.smtlib.AbstractSolver
Override in subclasses to handle solver-specific options.
set_option_impl(IExpr.IKeyword, IAttributeValue) - Method in class org.smtlib.solvers.Solver_altergo
Sent to Alt-Ergo, and kept here for get_option when Alt-Ergo accepts it
set_option_impl(IExpr.IKeyword, IAttributeValue) - Method in class org.smtlib.solvers.Solver_bitwuzla
Sent to bitwuzla, and also kept here for get_option, which bitwuzla does not support
set_option_impl(IExpr.IKeyword, IAttributeValue) - Method in class org.smtlib.solvers.Solver_cvc5
 
set_option_impl(IExpr.IKeyword, IAttributeValue) - Method in class org.smtlib.solvers.Solver_z3_4_3_2
Corrects a non-conformance of z3 4.3.2: set-option of an option it does not know answers an error, (error "line L column C: unknown parameter 'foo'\nLegal parameters are:\n ..."), which names the option and then lists every parameter of its module, one per line.
set_option_impl(IExpr.IKeyword, IAttributeValue) - Method in class org.smtlib.solvers.Solver_z3_4_3
z3 4.3 accepts :interactive-mode, :produce-assertions and the other :produce- options after set-logic, which SMT-LIB forbids, so that is reported here; values are kept here for get_option.
setChannels(PrintStream, PrintStream) - Method in class org.smtlib.Log
Points both output channels at the given streams -- the one point through which every change to these two channels happens.
setCmd(String[]) - Method in class org.smtlib.SolverProcess
Enables changing the command-line; must be called prior to start()
setDiagnosticOutputChannel(String) - Method in class org.smtlib.Log
The Log.diag sibling of Log.setRegularOutputChannel(String).
setInfoKeywords - Static variable in class org.smtlib.Utils
The attributes the standard defines for set-info (any other is allowed, but not standard)
setPos(IPos) - Method in class org.smtlib.impl.Pos.Posable
 
setPos(IPos) - Method in interface org.smtlib.IPos.IPosable
Setting the textual position
setPos(IPos) - Method in exception class org.smtlib.IVisitor.VisitorException
 
setPos(T, IPos) - Method in class org.smtlib.impl.Response.Error
Setting the textual position of the command
setPos(T, IPos) - Static method in class org.smtlib.sexpr.Lexer
A static helper method that sets the position of an AST node, but returns the same type
setRegularOutputChannel(String) - Method in class org.smtlib.Log
Points the regular-output channel at "stdout", "stderr", or -- for any other value -- opens (in append mode) the file so named, per :regular-output-channel's SMT-LIB semantics.
setSort(ISort) - Method in interface org.smtlib.IExpr
Records the sort computed for this expression by the type checker.
setSort(ISort) - Method in class org.smtlib.impl.Pos.AbstractExpr
 
setSourceLine(int) - Method in class org.smtlib.AbstractSolver
 
setSourceLine(int) - Method in interface org.smtlib.ISolver
Tells the solver the line of the user's source on which the command about to be executed starts (counted from 1), or 0 if it has none, so that the line numbers in the solver's messages can be given as lines of that source
setTrailingText(String) - Method in class org.smtlib.impl.Command
Sets the text captured in Command.trailingText.
Sexpr - Class in org.smtlib.sexpr
This is the root class for S-expressions in the concrete syntax
Sexpr() - Constructor for class org.smtlib.sexpr.Sexpr
 
Sexpr.Seq - Class in org.smtlib.sexpr
The class corresponding to sequences of S-expressions
Sexpr.Token<T> - Class in org.smtlib.sexpr
Represents a single S-expression token with intrinsic type T
sexprs - Variable in class org.smtlib.sexpr.Sexpr.Seq
 
sexprs() - Method in interface org.smtlib.sexpr.ISexpr.ISeq
 
sexprs() - Method in class org.smtlib.sexpr.Sexpr.Seq
 
shadowsLogic(IExpr.ISymbol, boolean) - Method in class org.smtlib.TypeChecker
Reports a bound variable (sort parameter, if sort is true) with the name of a function (sort) symbol of the logic or its theories, which only --relax allows (SMT-LIB Remark 7); returns true if reported
shapeOf(ICommand) - Static method in class org.smtlib.AbstractSolver
The kind of response cmd has
shutdownThread - Variable in class org.smtlib.SolverProcess
 
SIGN_EXTEND - Static variable in class org.smtlib.Utils
 
sizeIncrease - Variable in class org.smtlib.CharSequenceInfinite
The amount by which to increase the internal char array when needed
sizeMultiple - Variable in class org.smtlib.CharSequenceInfinite
The factor by which to increase the size of the internal char array when needed
skipThroughEndOfLine - Static variable in class org.smtlib.sexpr.Lexer
A pattern to skip up to the end of the line
skipThruRP() - Method in class org.smtlib.sexpr.Lexer
Reads and discards tokens until an unmatched right parenthesis or end-of-data is read
SLASH - Static variable in class org.smtlib.Utils
 
smt() - Method in class org.smtlib.AbstractSolver
 
smt() - Method in interface org.smtlib.IParser
Returns the configuration with which the parser was instantiated.
smt() - Method in interface org.smtlib.ISolver
Returns the configuration object with which the solver is initialized
smt() - Method in class org.smtlib.sexpr.Parser
Returns a handle to the parent SMTConfig object, in order to see command-line options etc.
smt() - Method in class org.smtlib.solvers.Solver_test
Returns the reference to the configuration currently in use.
SMT - Class in org.smtlib
This is the main class for the SMT-LIB tool.
SMT() - Constructor for class org.smtlib.SMT
 
SMT.Configuration - Class in org.smtlib
The configuration object holds the values of all of the current options (e.g.
SMT.Configuration.SMTLIB - Enum Class in org.smtlib
Enumeration of the supported SMT-LIB versions, in declaration order from oldest to newest.
SMT.IConfiguration - Interface in org.smtlib
Marker interface for configuration objects; reserved for future extension.
SMT.InternalException - Exception Class in org.smtlib
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 - Class in org.smtlib
This class is a prompter used when more data is needed from a data source
smtConfig - Variable in class org.smtlib.AbstractSolver
SMT configuration — set by each concrete subclass constructor.
smtConfig - Variable in class org.smtlib.CharSequenceSocket
The configuration for this instance of SMT
smtConfig - Variable in class org.smtlib.impl.Factory
The configuration this factory's instances (e.g.
smtConfig - Variable in class org.smtlib.impl.SMTExpr.Logic
The configuration this logic instance is scoped to; see issue #22.
smtConfig - Variable in class org.smtlib.sexpr.Printer
The Configuration whose rules (e.g.
smtConfig - Variable in class org.smtlib.SMT.Prompter
 
smtConfig - Variable in class org.smtlib.SMT
The set of configuration settings for this instance of the SMT object
smtConfig - Variable in class org.smtlib.solvers.Solver_test
A reference to the configuration used by this SMT instance.
smtConfig - Variable in class org.smtlib.SymbolTable
A reference to the Configuration for this instance of SMT.
smtConfig - Variable in class org.smtlib.Utils
A reference to the configuration being used for this instance of Utils.
SMTExpr - Class in org.smtlib.impl
This class defines a number of subclasses that implement the SMT-LIB abstract AST; they are used by commands and expressions.
SMTExpr() - Constructor for class org.smtlib.impl.SMTExpr
 
SMTExpr.AsIdentifier - Class in org.smtlib.impl
This class represents an SMT as-identifier AST
SMTExpr.Attribute<TT> - Class in org.smtlib.impl
Represents an SMT-LIB attribute: a keyword optionally paired with a value.
SMTExpr.AttributedExpr - Class in org.smtlib.impl
Represents an SMT-LIB attributed expression ((! expr attrs...)).
SMTExpr.BinaryLiteral - Class in org.smtlib.impl
Represents an SMT-LIB binary literal (e.g.
SMTExpr.Binding - Class in org.smtlib.impl
Represents a let-binding: a symbol bound to an expression.
SMTExpr.Constructor - Class in org.smtlib.impl
Represents a constructor declaration within a datatype, consisting of a name and a list of selectors.
SMTExpr.Datatype - Class in org.smtlib.impl
Represents a datatype body: a list of constructors and (for parametric forms) a list of sort parameter symbols.
SMTExpr.Decimal - Class in org.smtlib.impl
This class represents an SMT Decimal literal expression or syntax token
SMTExpr.Declaration - Class in org.smtlib.impl
Represents a sorted variable declaration (parameter name and its sort), used in forall/exists/define-fun.
SMTExpr.Error - Class in org.smtlib.impl
Represents an expression-level error node inserted during parsing to allow error recovery.
SMTExpr.Exists - Class in org.smtlib.impl
Represents an SMT-LIB existential quantifier expression.
SMTExpr.FcnExpr - Class in org.smtlib.impl
Represents a function-application expression: a qualified identifier applied to a list of argument expressions.
SMTExpr.Forall - Class in org.smtlib.impl
Represents an SMT-LIB universal quantifier expression.
SMTExpr.FunctionDeclaration - Class in org.smtlib.impl
Represents a function declaration header (name, sorted parameters, result sort), used in define-funs-rec.
SMTExpr.HexLiteral - Class in org.smtlib.impl
Represents an SMT-LIB hex literal (e.g.
SMTExpr.Keyword - Class in org.smtlib.impl
This class represents an SMT Keyword syntax token
SMTExpr.Lambda - Class in org.smtlib.impl
Represents an SMT-LIB lambda expression (SMT-LIB 2.7ff, HO-Core theory).
SMTExpr.Let - Class in org.smtlib.impl
Represents an SMT-LIB let expression: a list of bindings and a body expression.
SMTExpr.Literal<T> - Class in org.smtlib.impl
Abstract base class for all literal value AST nodes; holds the typed value and provides a shared implementation.
SMTExpr.Logic - Class in org.smtlib.impl
 
SMTExpr.Match - Class in org.smtlib.impl
Represents an SMT-LIB 2.7 match expression: an expression matched against a list of cases.
SMTExpr.MatchCase - Class in org.smtlib.impl
Represents a single case in a match expression: a pattern and its result body.
SMTExpr.Numeral - Class in org.smtlib.impl
This class represents an SMT Numeral expression or syntax token
SMTExpr.ParameterizedIdentifier - Class in org.smtlib.impl
This class represents an SMT parameterized-identifier AST (e.g.
SMTExpr.Pattern - Class in org.smtlib.impl
Represents a match pattern: a constructor name applied to zero or more variable symbols.
SMTExpr.PatternTerms - Class in org.smtlib.impl
Represents the value of a :pattern attribute: a list of trigger terms.
SMTExpr.Selector - Class in org.smtlib.impl
Represents a selector declaration within a datatype constructor.
SMTExpr.SortDeclaration - Class in org.smtlib.impl
Represents a sort declaration (symbol and arity) used in declare-datatype and declare-datatypes.
SMTExpr.StringLiteral - Class in org.smtlib.impl
This class represents an SMT String literal expression or syntax token
SMTExpr.Symbol - Class in org.smtlib.impl
This class represents an SMT Symbol
SMTExpr.Theory - Class in org.smtlib.impl
 
smtFactory - Variable in class org.smtlib.SMT.Configuration
The factory to use to create IParser, IPos, ISource objects
smtlib - Variable in class org.smtlib.SMT.Configuration
The version of SMT-LIB to be supported; null means the default (most recent version)
SMTLIB_VERSION - Static variable in class org.smtlib.Utils
The string designating the smtlib attribute within a logic or theory
SMTLIBException(IResponse.IError) - Constructor for exception class org.smtlib.Utils.SMTLIBException
Creates an SMTLIBException wrapping the given error response.
solver - Variable in class org.smtlib.SMT
 
Solver_altergo - Class in org.smtlib.solvers
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.
Solver_altergo(SMT.Configuration, String) - Constructor for class org.smtlib.solvers.Solver_altergo
Creates an instance of the solver
Solver_altergo(SMT.Configuration, String[]) - Constructor for class org.smtlib.solvers.Solver_altergo
Launches the given command as is (a .command property, #147), without adding the flags the executable form adds
Solver_bitwuzla - Class in org.smtlib.solvers
This class is an adapter for Bitwuzla (bit-vectors, floating-point, arrays and uninterpreted functions -- no arithmetic logics, no datatypes).
Solver_bitwuzla(SMT.Configuration, String) - Constructor for class org.smtlib.solvers.Solver_bitwuzla
Creates an instance of the solver
Solver_bitwuzla(SMT.Configuration, String[]) - Constructor for class org.smtlib.solvers.Solver_bitwuzla
Launches the given command as is (a .command property, #147), without adding the flags the executable form adds
Solver_cvc5 - Class in org.smtlib.solvers
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.
Solver_cvc5(SMT.Configuration, String) - Constructor for class org.smtlib.solvers.Solver_cvc5
Creates an instance of the solver
Solver_cvc5(SMT.Configuration, String[]) - Constructor for class org.smtlib.solvers.Solver_cvc5
Launches the given command as is (a .command property, #147), without adding the flags the executable form adds
SOLVER_EXITED - Static variable in class org.smtlib.AbstractSolver
The error every command answers once the solver process has exited (other than by its whole-run time limit)
Solver_simplify - Class in org.smtlib.solvers
The adapter that drives the Simplify solver.
Solver_simplify(SMT.Configuration, String) - Constructor for class org.smtlib.solvers.Solver_simplify
Constructor with standard signature for invocation through reflection
Solver_simplify(SMT.Configuration, String[]) - Constructor for class org.smtlib.solvers.Solver_simplify
Launches the given command as is (a .command property, #147), without adding the flags the executable form adds
Solver_simplify.Translator - Class in org.smtlib.solvers
 
Solver_smt - Class in org.smtlib.solvers
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.
Solver_smt(SMT.Configuration, String) - Constructor for class org.smtlib.solvers.Solver_smt
Creates an instance of the adapter
Solver_smt(SMT.Configuration, String[]) - Constructor for class org.smtlib.solvers.Solver_smt
 
Solver_smtinterpol - Class in org.smtlib.solvers
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.
Solver_smtinterpol(SMT.Configuration, String[]) - Constructor for class org.smtlib.solvers.Solver_smtinterpol
Creates an instance of the solver.
Solver_test - Class in org.smtlib.solvers
This class is a Solver implementation that simply type-checks formulae and checks that commands are used correctly; it does not do any proving.
Solver_test(SMT.Configuration, String) - Constructor for class org.smtlib.solvers.Solver_test
Constructor for an instance of this test solver class; the second argument is ignored - it is present just for uniformity with other solvers, for which that argument is a path to the relevant executable.
Solver_yices2 - Class in org.smtlib.solvers
This class is an adapter that takes the SMT-LIB ASTs and translates them into yices2 commands
Solver_yices2(SMT.Configuration, String) - Constructor for class org.smtlib.solvers.Solver_yices2
Creates an instance of the yices2 solver
Solver_yices2(SMT.Configuration, String[]) - Constructor for class org.smtlib.solvers.Solver_yices2
Creates an instance of the yices2 solver
Solver_yices2_2_6 - Class in org.smtlib.solvers
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.
Solver_yices2_2_6(SMT.Configuration, String) - Constructor for class org.smtlib.solvers.Solver_yices2_2_6
 
Solver_yices2_2_6(SMT.Configuration, String[]) - Constructor for class org.smtlib.solvers.Solver_yices2_2_6
 
Solver_z3_4_3 - Class in org.smtlib.solvers
This class is an adapter that takes the SMT-LIB ASTs and translates them into Z3 commands
Solver_z3_4_3(SMT.Configuration, String) - Constructor for class org.smtlib.solvers.Solver_z3_4_3
Creates an instance of the Z3 solver
Solver_z3_4_3(SMT.Configuration, String[]) - Constructor for class org.smtlib.solvers.Solver_z3_4_3
Creates an instance of the Z3 solver
Solver_z3_4_3_2 - Class in org.smtlib.solvers
This is a special handler for Z3 4.3.2, as opposed to other revisions of Z3 4.3.
Solver_z3_4_3_2(SMT.Configuration, String) - Constructor for class org.smtlib.solvers.Solver_z3_4_3_2
 
Solver_z3_4_3_2(SMT.Configuration, String[]) - Constructor for class org.smtlib.solvers.Solver_z3_4_3_2
Launches the given command as is (a .command property, #147), without adding the flags the executable form adds
Solver_z3_4_3.Translator - Class in org.smtlib.solvers
 
Solver_z3_4_5 - Class in org.smtlib.solvers
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)
Solver_z3_4_5(SMT.Configuration, String) - Constructor for class org.smtlib.solvers.Solver_z3_4_5
 
Solver_z3_4_5(SMT.Configuration, String[]) - Constructor for class org.smtlib.solvers.Solver_z3_4_5
 
Solver_z3_recent - Class in org.smtlib.solvers
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.
Solver_z3_recent(SMT.Configuration, String) - Constructor for class org.smtlib.solvers.Solver_z3_recent
Creates an instance of the solver
Solver_z3_recent(SMT.Configuration, String[]) - Constructor for class org.smtlib.solvers.Solver_z3_recent
Launches the given command as is (a .command property, #147), without adding the flags the executable form adds
SolverCapabilities - Class in org.smtlib
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 - Enum Class in org.smtlib
The capabilities that can be queried; SolverCapabilities.Capability.token is the name used in the properties
SolverCapabilities.Support - Enum Class in org.smtlib
The answer to a query; UNKNOWN means the solver's entry does not record the capability
solvername - Variable in class org.smtlib.SMT.Configuration
The solver to use
solvername() - Method in record class org.smtlib.SolverResolver.Resolution
Returns the value of the solvername record component.
solverName() - Method in class org.smtlib.AbstractSolver
 
solverName() - Method in interface org.smtlib.ISolver
A public, user-readable name for the solver adapter class
solverName() - Method in class org.smtlib.solvers.Solver_test
 
solverPrintsSuccess() - Method in class org.smtlib.AbstractSolver
Whether the solver writes 'success' for a successful command, so that every command gets one response.
solverPrintsSuccess() - Method in class org.smtlib.solvers.Solver_altergo
Alt-Ergo writes nothing for a successful command and answers (set-option :print-success true) with unsupported; its commands are therefore sent as when pipelining, each followed by an echo that marks the end of its response
solverProcess - Variable in class org.smtlib.AbstractSolver
The object that interacts with external processes
SolverProcess - Class in org.smtlib
This class implements launching, writing to, and reading responses from a launched process (in particular, solver processes).
SolverProcess(String[], String, String) - Constructor for class org.smtlib.SolverProcess
Constructs a SolverProcess object, without actually starting the process as yet.
SolverProcess(String[], String, String, Charset) - Constructor for class org.smtlib.SolverProcess
As SolverProcess(String[], String, String), but explicitly setting the charset used to encode text sent to the process and decode text read back from it.
SolverProcess.NoResponseException - Exception Class in org.smtlib
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 - Exception Class in org.smtlib
Wraps an exception thrown because of a failure in the prover
SolverProcess.StreamGobbler - Class in org.smtlib
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 - Class in org.smtlib
For internal use only (public so that the tests can reach it); not part of the API.
SolverResolver.Resolution - Record Class in org.smtlib
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
solverVerbosity - Variable in class org.smtlib.SMT.Configuration
The verbosity level of the SMT solver
sort - Variable in class org.smtlib.impl.Pos.AbstractExpr
 
sort - Variable in class org.smtlib.impl.SMTExpr.Declaration
 
sort - Variable in class org.smtlib.impl.SMTExpr.FunctionDeclaration
 
sort - Variable in class org.smtlib.impl.SMTExpr.Selector
 
sort - Variable in class org.smtlib.SymbolTable.Entry
The Sort of the identifier
sort - Variable in class org.smtlib.TypeChecker.Variable
 
sort() - Method in interface org.smtlib.IExpr.IDeclaration
 
sort() - Method in interface org.smtlib.IExpr.IFunctionDeclaration
 
sort() - Method in interface org.smtlib.IExpr.ISelector
 
sort() - Method in interface org.smtlib.IExpr
The sort computed for this expression by the type checker, or null if not yet (or never) computed.
sort() - Method in class org.smtlib.impl.Pos.AbstractExpr
 
sort() - Method in class org.smtlib.impl.SMTExpr.Declaration
 
sort() - Method in class org.smtlib.impl.SMTExpr.FunctionDeclaration
 
sort() - Method in class org.smtlib.impl.SMTExpr.Selector
 
Sort - Class in org.smtlib.impl
This class implements the abstract ISort interface
Sort() - Constructor for class org.smtlib.impl.Sort
 
Sort.Abbreviation - Class in org.smtlib.impl
Implements a Sort abbreviation (parameterized definition, possibly with no parameters)
Sort.Application - Class in org.smtlib.impl
Represents a sort expression consisting of a sort symbol or sort abbreviation symbol applied to a corresponding number of sort arguments
Sort.ErrorDefinition - Class in org.smtlib.impl
A placeholder sort definition used when a sort declaration is ill-formed, to suppress cascading errors.
Sort.Family - Class in org.smtlib.impl
Represents a new sort symbol, with a given identifier and arity
Sort.FcnSort - Class in org.smtlib.impl
Represents the class of the sort of a function symbol.
Sort.Parameter - Class in org.smtlib.impl
Represents a Sort parameter, such as in either the parameter list or the expression of a Sort abbreviation
sortApp(String, ISort...) - Method in class org.smtlib.logic.Logic
Creates the sort expression name(params...), e.g.
sortDeclaration - Variable in class org.smtlib.command.C_declare_datatype
The sort declaration (symbol + arity derived from datatype body)
sortDeclaration() - Method in class org.smtlib.command.C_declare_datatype
 
sortDeclaration() - Method in interface org.smtlib.ICommand.Ideclare_datatype
Returns the sort declaration (name and arity).
sortDeclaration(IExpr.ISymbol, IExpr.INumeral) - Method in interface org.smtlib.IExpr.IFactory
Creates a sort declaration (symbol + arity) for use in declare-datatype(s).
sortDeclaration(IExpr.ISymbol, IExpr.INumeral) - Method in class org.smtlib.impl.Factory
 
SortDeclaration(IExpr.ISymbol, IExpr.INumeral) - Constructor for class org.smtlib.impl.SMTExpr.SortDeclaration
Creates a sort declaration for the given sort name and arity.
sortDeclarations - Variable in class org.smtlib.command.C_declare_datatypes
The sort declarations: (symbol arity) pairs
sortDeclarations() - Method in class org.smtlib.command.C_declare_datatypes
 
sortDeclarations() - Method in interface org.smtlib.ICommand.Ideclare_datatypes
Returns the list of sort declarations (names and arities).
sortExpression - Variable in class org.smtlib.impl.Sort.Abbreviation
 
sortExpression() - Method in class org.smtlib.impl.Sort.Abbreviation
 
sortExpression() - Method in interface org.smtlib.ISort.IAbbreviation
The sort expression that the abbreviation represents, presumably using the given parameters
sortFactory - Variable in class org.smtlib.SMT.Configuration
The factory to use to create ISort objects
sortID - Variable in class org.smtlib.impl.Sort.Application
 
sortName - Variable in class org.smtlib.command.C_define_sort
The name of the sort being defined
sortParameters - Variable in class org.smtlib.impl.Sort.Application
 
SORTS - Static variable in class org.smtlib.Utils
The attribute tag for defining sorts in a theory
sortSymbol - Variable in class org.smtlib.command.C_declare_sort_parameter
The new sort symbol
sortSymbol - Variable in class org.smtlib.command.C_declare_sort
The new sort symbol
sortSymbol() - Method in class org.smtlib.command.C_declare_sort_parameter
The sort symbol declared by this command
sortSymbol() - Method in class org.smtlib.command.C_declare_sort
The sort symbol declared by this command
sortSymbol() - Method in class org.smtlib.command.C_define_sort
Returns the name of the sort being defined.
sortSymbol() - Method in interface org.smtlib.ICommand.Ideclare_sort_parameter
Returns the name of the sort parameter being declared.
sortSymbol() - Method in interface org.smtlib.ICommand.Ideclare_sort
Returns the name of the sort being declared.
sortSymbol() - Method in interface org.smtlib.ICommand.Idefine_sort
Returns the name of the sort being defined.
source - Variable in class org.smtlib.impl.Pos
The source of text
source() - Method in class org.smtlib.impl.Pos
The source of text
source() - Method in interface org.smtlib.IPos
Returns the source object containing the characters
source() - Method in class org.smtlib.sexpr.Lexer
The source of input used in this lexer; typically a different lexer object will be used for each source (e.g.
Source(CharSequence, Object) - Constructor for class org.smtlib.impl.Pos.Source
Creates a Source from a character sequence
Source(SMT.Configuration, File) - Constructor for class org.smtlib.impl.Pos.Source
Creates a Source from a File; for these objects, the location is the file path (a String)
Source(SMT.Configuration, InputStream, Object) - Constructor for class org.smtlib.impl.Pos.Source
Creates a Source from a File
sourceLine(ICommand) - Static method in class org.smtlib.Utils
The line of its source on which the command starts (counted from 1), or 0 if it has no source position
StandardListener() - Constructor for class org.smtlib.Log.StandardListener
 
standardOut - Variable in class org.smtlib.SolverProcess
 
start - Variable in class org.smtlib.Driver
Whether to start a service process from this process
start() - Method in class org.smtlib.AbstractSolver
 
start() - Method in interface org.smtlib.ISolver
Starts the solver; this is not an SMT-LIB command, but it is convenient in some implementations to separate the starting and initialization from the construction of the solver instance.
start() - Method in class org.smtlib.solvers.Solver_altergo
 
start() - Method in class org.smtlib.solvers.Solver_bitwuzla
 
start() - Method in class org.smtlib.solvers.Solver_cvc5
 
start() - Method in class org.smtlib.solvers.Solver_simplify
 
start() - Method in class org.smtlib.solvers.Solver_smt
 
start() - Method in class org.smtlib.solvers.Solver_smtinterpol
 
start() - Method in class org.smtlib.solvers.Solver_test
 
start() - Method in class org.smtlib.solvers.Solver_yices2
 
start() - Method in class org.smtlib.solvers.Solver_z3_4_3
 
start() - Method in class org.smtlib.solvers.Solver_z3_recent
 
start(boolean) - Method in class org.smtlib.SolverProcess
Starts the process; if the argument is true, then also listens to its output until a prompt is read.
startModeOptions - Static variable in class org.smtlib.Utils
The standard options that may be set only in start mode, i.e.
startSolver(SMT.Configuration, String, String) - Method in class org.smtlib.SMT
Starts the solver with the given name and executable, preset according to the given configuration.
STATUS - Static variable in class org.smtlib.Utils
The string designating an info item
stderr - Variable in class org.smtlib.SMT.Configuration
The PrintStream that "stderr" resolves to for this instance.
STDERR - Static variable in class org.smtlib.Utils
The String for the stderr predefined string
stdout - Variable in class org.smtlib.SMT.Configuration
The PrintStream that "stdout" resolves to for this instance.
STDOUT - Static variable in class org.smtlib.Utils
The String for the stdout predefined string
stopIfRunning() - Method in class org.smtlib.SolverProcess
Stops the solver's OS process if it is still running, leaving this object as it is: later sends then fail as "Solver process has already exited", and SolverProcess.exit() cleans up.
STORE - Static variable in class org.smtlib.Utils
 
StreamGobbler(InputStream, Function<StringBuilder, Boolean>, Charset) - Constructor for class org.smtlib.SolverProcess.StreamGobbler
 
strictCommandExtensionPrefixes - Variable in class org.smtlib.SMT.Configuration
 
STRING - Static variable in class org.smtlib.sexpr.Utils
Concrete syntax for the special STRING token
stringLiteral(String) - Method in class org.smtlib.impl.Response.Factory
 
stringLiteral(String) - Method in interface org.smtlib.IResponse.IFactory
The argument has no SMT-LIB escapes and no enclosing quotes
StringLiteral(SMT.Configuration, String, boolean) - Constructor for class org.smtlib.impl.SMTExpr.StringLiteral
Creates a string literal.
stringOptions - Variable in class org.smtlib.Utils
The set of standard options with string values
STRINGS - Enum constant in enum class org.smtlib.SolverCapabilities.Capability
 
subSequence(int, int) - Method in class org.smtlib.CharSequenceInfinite
Returns a subsequence of this CharSequence, of length end-start.
substitute(Map<ISort.IParameter, ISort>) - Method in class org.smtlib.impl.Sort.Application
 
substitute(Map<ISort.IParameter, ISort>) - Method in class org.smtlib.impl.Sort.FcnSort
 
substitute(Map<ISort.IParameter, ISort>) - Method in class org.smtlib.impl.Sort.Parameter
 
substitute(Map<ISort.IParameter, ISort>) - Method in interface org.smtlib.ISort
Returns a new sort with any parameters substituted
success() - Method in class org.smtlib.impl.Response.Factory
 
success() - Method in interface org.smtlib.IResponse.IFactory
 
SUCCESS - Enum constant in enum class org.smtlib.AbstractSolver.Shape
success
SUCCESS - Static variable in class org.smtlib.impl.Response
 
successOrEmpty(SMT.Configuration) - Method in class org.smtlib.AbstractSolver
 
SUFFIX - Static variable in class org.smtlib.Utils
The suffix used for SMT-LIB files
supports(String, String) - Static method in class org.smtlib.SolverCapabilities
As SolverCapabilities.supports(String, Capability), with the capability given by its token or enum name
supports(String, SolverCapabilities.Capability) - Static method in class org.smtlib.SolverCapabilities
Whether the solver supports the capability, according to the merged jsmtlib.properties
supports(Properties, String, SolverCapabilities.Capability) - Static method in class org.smtlib.SolverCapabilities
Whether the solver supports the capability, according to the given properties
symbol - Variable in class org.smtlib.impl.SMTExpr.Constructor
 
symbol - Variable in class org.smtlib.impl.SMTExpr.FunctionDeclaration
 
symbol - Variable in class org.smtlib.impl.SMTExpr.Selector
 
symbol - Variable in class org.smtlib.impl.SMTExpr.SortDeclaration
 
symbol - Variable in class org.smtlib.impl.Sort.Parameter
 
symbol - Variable in class org.smtlib.TypeChecker.Variable
 
symbol() - Method in class org.smtlib.command.C_declare_fun
 
symbol() - Method in class org.smtlib.command.C_define_fun
The name of the function being defined
symbol() - Method in interface org.smtlib.ICommand.Ideclare_const
Returns the name of the constant being declared.
symbol() - Method in interface org.smtlib.ICommand.Ideclare_fun
Returns the name of the function being declared.
symbol() - Method in interface org.smtlib.ICommand.Idefine_fun_rec
Returns the name of the function being defined.
symbol() - Method in interface org.smtlib.ICommand.Idefine_fun
Returns the name of the function being defined.
symbol() - Method in interface org.smtlib.IExpr.IConstructor
 
symbol() - Method in interface org.smtlib.IExpr.IFunctionDeclaration
 
symbol() - Method in interface org.smtlib.IExpr.ISelector
 
symbol() - Method in interface org.smtlib.IExpr.ISortDeclaration
 
symbol() - Method in class org.smtlib.impl.SMTExpr.Constructor
 
symbol() - Method in class org.smtlib.impl.SMTExpr.FunctionDeclaration
 
symbol() - Method in class org.smtlib.impl.SMTExpr.Selector
 
symbol() - Method in class org.smtlib.impl.SMTExpr.SortDeclaration
 
symbol() - Method in class org.smtlib.impl.Sort.Parameter
 
symbol() - Method in interface org.smtlib.ISort.IParameter
The symbol that names the parameter
symbol(String) - Method in interface org.smtlib.IExpr.IFactory
Creates an ISymbol object from a canonical String representation of the symbol.
symbol(String) - Method in class org.smtlib.impl.Factory
 
Symbol(String) - Constructor for class org.smtlib.impl.SMTExpr.Symbol
The argument is a Symbol string, with or without enclosing bars; a lone or unmatched bar is kept in the value (and reported by the type checker)
symbols - Variable in class org.smtlib.impl.SMTExpr.Datatype
 
symbols() - Method in class org.smtlib.impl.SMTExpr.Datatype
 
symbols() - Method in interface org.smtlib.ISort.IDatatype
 
SymbolTable - Class in org.smtlib
This class manages a symbol table used for storing definitions and looking up ids in expressions.
SymbolTable(SMT.Configuration) - Constructor for class org.smtlib.SymbolTable
Constructs an empty symbol table
SymbolTable.Entry - Class in org.smtlib
An object that holds all the information about the defined symbol (or aliased definition).
SymbolTable.Iterator - Class in org.smtlib
An iterator over all of the Symbols in the symbol scope stack from the top-most scope on down.
symTable - Variable in class org.smtlib.solvers.Solver_simplify
The symbol table used for this class's own local type-checking simulation (see the class Javadoc) -- a straight copy of Solver_test's own field of the same name and visibility (public for C_what's sake, though that extension command no longer recognizes this class as a symbol-table-bearing solver now that it isn't a Solver_test -- see this session's own restructuring notes; no test exercises "what" against Simplify).
symTable - Variable in class org.smtlib.solvers.Solver_test
The symbol table used by this solver
SyntaxException(String, IPos) - Constructor for exception class org.smtlib.IParser.SyntaxException
Creates an exception from the given error message and problem location
A B C D E F G H I J K L M N O P Q R S T U V W X Y Z 
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form