Uses of Interface
org.smtlib.IResponse

Packages that use IResponse

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.sexpr	This package is a concrete implementation of a particular concrete syntax for the abstract SMT-LIB semantics.
org.smtlib.solvers	This package implements various instances of org.smtlib.ISolver, which are specific solvers that wrap and interact with various off-the-shelf SMT solvers currently available.

Uses of IResponse in org.smtlib

Subinterfaces of IResponse in org.smtlib

Modifier and Type	Interface	Description
interface	IAttributeValue	This interface represents the general class of attribute values; that is, it is the super-interface of any class that may be an attribute value; in the abstract syntax it has no particular structure, though it does include true, false, string literals, numerals, and various pre-defined constants.
interface	IExpr	This interface represents the functionality for any class implementing an SMT-LIB term or formula
static interface	IExpr.IAsIdentifier	This interface represents SMT-LIB identifiers that are sort qualifiers on function ids
static interface	IExpr.IAttribute<TT extends IAttributeValue>	This interface represents an SMT-LIB attribute-value pair; the value may be null (keyword-only attribute).
static interface	IExpr.IAttributedExpr	This interface represents an SMT-LIB expression with attributes.
static interface	IExpr.IBinaryLiteral	This interface represents SMT-LIB binary literals
static interface	IExpr.IDecimal	This interface represents non-negative decimal numbers of arbitrary size (i.e.
static interface	IExpr.IError	This interface represents an error, e.g.
static interface	IExpr.IExists	This interface represents an SMT-LIB quantified exists expression
static interface	IExpr.IFcnExpr	This interface represents SMT-LIB expressions that are a function identifier applied to one or more arguments.
static interface	IExpr.IForall	This interface represents an SMT-LIB quantified forall expression
static interface	IExpr.IHexLiteral	This interface represents SMT-LIB hex literals
static interface	IExpr.IIdentifier	This interface represents SMT-LIB identifiers (either ids or parameterized ids)
static interface	IExpr.IIndex	Marker interface for the index types in a parameterized identifier: INumeral and ISymbol, plus IHexLiteral, which the Strings theory's (_ char H) uses, and IBinaryLiteral, which no theory uses but which is parsed so that a solver reports it; each theory decides which kinds it accepts.
static interface	IExpr.ILambda	This interface represents an SMT-LIB lambda expression: (lambda (sorted_var+) term).
static interface	IExpr.ILet	This interface represents an SMT-LIB let-expression
static interface	IExpr.ILiteral	This interface represents all literal (explicit constant) expressions.
static interface	IExpr.IMatch	This interface represents an SMT-LIB 2.7 match expression.
static interface	IExpr.INumeral	This interface represents non-negative integers of arbitrary size.
static interface	IExpr.IParameterizedIdentifier	This interface represents SMT-LIB parameterized identifiers
static interface	IExpr.IPatternTerms	This interface represents the value of a :pattern attribute: a list of terms (a multi-pattern), written in the concrete syntax as ( t1 ... tn ).
static interface	IExpr.IQualifiedIdentifier	This interface represents SMT-LIB identifiers for function ids (either ids or parameterized ids or as-type identifiers)
static interface	IExpr.IStringLiteral	This interface represents SMT-LIB string literals
static interface	IExpr.ISymbol	This interface represents SMT-LIB ids; equal ids have equal (using .equals) values of value().
static interface	IResponse.IAssertionsResponse	Response type for get-assertions, carrying the list of currently asserted formulae.
static interface	IResponse.IAssignmentResponse	Response type for get-assignment, carrying a list of name-Boolean pairs.
static interface	IResponse.IAttributeList	Response type for get-info, carrying a list of attribute key-value pairs.
static interface	IResponse.IError	The interface for error responses
static interface	IResponse.IProofResponse	Response type for get-proof.
static interface	IResponse.IUnsatAssumptionsResponse	Response type for get-unsat-assumptions, carrying the assumptions (terms, e.g.
static interface	IResponse.IUnsatCoreResponse	Response type for get-unsat-core, carrying the names of the formulae in the unsat core.
static interface	IResponse.IValueResponse	Response type for get-value, carrying a list of expression-value pairs.

Classes in org.smtlib that implement IResponse

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

Fields in org.smtlib declared as IResponse

Modifier and Type	Field	Description
protected IResponse	AbstractSolver.checkSatStatus	The response to the most recent check-sat or check-sat-assuming, or null if there is none.
IResponse	SMT.checkSatStatus	The last check-sat status seen during execution; null if no check-sat has been executed yet.
IResponse	SMT.lastResponse	The response from the most recently executed command; used to export results in interactive mode.

Fields in org.smtlib with type parameters of type IResponse

Modifier and Type	Field	Description
List<IResponse>	TypeChecker.result	Compilation of errors

Methods in org.smtlib that return IResponse

Modifier and Type	Method	Description
IResponse	AbstractSolver.assertExpr(IExpr sexpr)
IResponse	ISolver.assertExpr(IExpr expr)	Adds the given expression to the current assertion-stack frame.
IResponse	AbstractSolver.check_sat()
IResponse	ISolver.check_sat()	Checks whether the current assertion set is satisfiable under the current logic.
IResponse	AbstractSolver.check_sat_assuming(IExpr... exprs)
IResponse	ISolver.check_sat_assuming(IExpr... exprs)	Checks satisfiability under the current assertion set plus the given propositional assumptions.
protected IResponse	AbstractSolver.checkImmediateExit(IResponse result)	Called with each response parsed from the solver.
IResponse	AbstractSolver.checkPrintSuccess(SMT.Configuration smtConfig, IExpr.IKeyword key, IAttributeValue value)	Answers a set-option of :print-success locally (it is never sent), else returns null
IResponse	AbstractSolver.checkSatStatus()
IResponse	ISolver.checkSatStatus()	Returns the result of the most recent check-sat or check-sat-assuming, or null if none has been issued since the last push/pop/assert/declare/define.
protected IResponse	AbstractSolver.checkShape(AbstractSolver.Shape shape, String sent, String text, IResponse r)	r, if it has the given shape; else the error for a response out of step with the command sent, whose raw response was text
protected IResponse	AbstractSolver.checkStatus()	The response to the most recent check command, or null if there is none or the solver has accepted a command that changes the assertion stack since (after reading the responses to the pipelined commands): sat or unknown in SMT-LIB's sat mode, unsat in its unsat mode
IResponse	IResponse.IFactory.continued_execution()
IResponse	AbstractSolver.declare_const(ICommand.Ideclare_const cmd)
IResponse	ISolver.declare_const(ICommand.Ideclare_const cmd)	Declares a new uninterpreted constant; returns success or an SMT error response
IResponse	AbstractSolver.declare_datatype(ICommand.Ideclare_datatype cmd)
IResponse	ISolver.declare_datatype(ICommand.Ideclare_datatype cmd)	Declares a new datatype sort; returns success or an SMT error response
IResponse	AbstractSolver.declare_datatypes(ICommand.Ideclare_datatypes cmd)
IResponse	ISolver.declare_datatypes(ICommand.Ideclare_datatypes cmd)	Declares mutually recursive datatype sorts; returns success or an SMT error response
IResponse	AbstractSolver.declare_fun(ICommand.Ideclare_fun cmd)
IResponse	ISolver.declare_fun(ICommand.Ideclare_fun cmd)	Declares a new uninterpreted function (or constant); returns success or an SMT error response
IResponse	AbstractSolver.declare_sort(ICommand.Ideclare_sort cmd)
IResponse	ISolver.declare_sort(ICommand.Ideclare_sort cmd)	Declares a new uninterpreted sort; returns success or an SMT error response
IResponse	AbstractSolver.declare_sort_parameter(ICommand.Ideclare_sort_parameter cmd)
IResponse	ISolver.declare_sort_parameter(ICommand.Ideclare_sort_parameter cmd)	Declares a new sort parameter (polymorphic sort variable); returns success or an SMT error response
IResponse	AbstractSolver.define_const(ICommand.Idefine_const cmd)
IResponse	ISolver.define_const(ICommand.Idefine_const cmd)	Defines a named constant — syntactic sugar for define-fun with no parameters; returns success or an SMT error response
IResponse	AbstractSolver.define_fun(ICommand.Idefine_fun cmd)
IResponse	ISolver.define_fun(ICommand.Idefine_fun cmd)	Defines a named function or constant; returns success or an SMT error response
IResponse	AbstractSolver.define_fun_rec(ICommand.Idefine_fun_rec cmd)
IResponse	ISolver.define_fun_rec(ICommand.Idefine_fun_rec cmd)	Defines a named recursive function; returns success or an SMT error response
IResponse	AbstractSolver.define_funs_rec(ICommand.Idefine_funs_rec cmd)
IResponse	ISolver.define_funs_rec(ICommand.Idefine_funs_rec cmd)	Defines a group of mutually recursive functions; returns success or an SMT error response
IResponse	AbstractSolver.define_sort(ICommand.Idefine_sort cmd)
IResponse	ISolver.define_sort(ICommand.Idefine_sort cmd)	Defines a sort abbreviation; returns success or an SMT error response
IResponse	AbstractSolver.echo(IExpr.IStringLiteral arg)
IResponse	ISolver.echo(IExpr.IStringLiteral arg)	Echoes the argument string back to the output channel.
IResponse	IResponse.IFactory.empty()
IResponse	AbstractSolver.execute(ICommand cmd)	Once the solver process has exited, every command but exit (and a comment, which has no response) answers AbstractSolver.exitedResponse(), including those an adapter answers itself or checks with its own queries
IResponse	ICommand.execute(ISolver solver)	Executes the command on the given solver; presumes that the command type-checked successfully.
IResponse	ICommand.IScript.execute(ISolver solver)
default IResponse	ISolver.execute(ICommand command)	Executes the command on this solver
IResponse	AbstractSolver.executePipelined(List<ICommand> commands)	Executes the commands in order, as a script does: returns the first error, or else the last command's response.
IResponse	AbstractSolver.exit()
IResponse	ISolver.exit()	Terminates the solver; no further commands are permitted.
IResponse	AbstractSolver.exitedResponse()	The response to any command once the solver process has exited: timeout if its whole-run time limit ended it, else the error AbstractSolver.SOLVER_EXITED; null while the process runs (or has not been started)
IResponse	AbstractSolver.get_assertions()
IResponse	ISolver.get_assertions()	Returns the list of formulae in the current assertion set, in the order they were asserted.
IResponse	AbstractSolver.get_assignment()
IResponse	ISolver.get_assignment()	Returns the truth-value assignments for all named Boolean formulae in the current model.
IResponse	AbstractSolver.get_info(IExpr.IKeyword option)
IResponse	ISolver.get_info(IExpr.IKeyword option)	Returns the value of the named info item.
IResponse	AbstractSolver.get_model()
IResponse	ISolver.get_model()	Returns a satisfying model for the current assertion set.
IResponse	AbstractSolver.get_option(IExpr.IKeyword option)
IResponse	ISolver.get_option(IExpr.IKeyword option)	Returns the current value of the named option.
IResponse	IResponse.IFactory.get_option_response(IAttributeValue v)
IResponse	AbstractSolver.get_proof()
IResponse	ISolver.get_proof()	Returns a proof of unsatisfiability for the current assertion set.
IResponse	AbstractSolver.get_unsat_assumptions()
IResponse	ISolver.get_unsat_assumptions()	Returns the subset of check-sat-assuming assumptions that caused the result to be unsat.
IResponse	AbstractSolver.get_unsat_core()
IResponse	ISolver.get_unsat_core()	Returns the named formulae that form an unsatisfiable core of the current assertion set.
IResponse	AbstractSolver.get_value(IExpr... terms)
IResponse	ISolver.get_value(IExpr... terms)	Returns the values of the given expressions in the current satisfying model.
IResponse	IResponse.IFactory.immediate_exit()
IResponse	IResponse.IFactory.incomplete()
IResponse	Utils.loadLogic(String logicName, SymbolTable symTable, IPos pos)	Finds and loads a logic into the given symbol table
IResponse	Utils.loadLogic(ILogic logicExpr, SymbolTable symTable)
IResponse	Utils.loadTheory(String theoryName, SymbolTable symTable)	Loads a theory into the given symbol table.
IResponse	Utils.loadTheory(ITheory theory, SymbolTable symTable)
IResponse	IResponse.IFactory.memout()
protected IResponse	AbstractSolver.modelResponse(IResponse r)	The get-model response r, without the leading symbol model if it has one: z3 4.3 to 4.7 and yices2 2.6.5 (with --smt2-model-format) answer (model (define-fun ...) ...), where SMT-LIB has the plain list ((define-fun ...) ...).
IResponse	IResponse.IFactory.numericLiteral(int value)
protected IResponse	AbstractSolver.parseResponse(String response)	Parses the solver's raw response text.
IResponse	AbstractSolver.pop(int number)
IResponse	ISolver.pop(int number)	Removes the given number of assertion-stack frames from the solver state.
protected IResponse	AbstractSolver.proofResponse(IResponse r)	Wraps a parsed get-proof answer as an IProofResponse; anything else (an error, unsupported) is returned unchanged.
IResponse	AbstractSolver.push(int number)
IResponse	ISolver.push(int number)	Adds the given number of empty assertion-stack frames to the solver state.
protected IResponse	AbstractSolver.recordChange(AbstractSolver.StackChange kind, IResponse response)	Records the response to a command of the given kind that changes the assertion stack, and returns it.
protected IResponse	AbstractSolver.requireNoChangeSinceCheck(String commandName, Set<AbstractSolver.StackChange> answeredAfter)	Returns an error response if, since a check command, the solver has accepted a command of one of the given kinds (after which the solver wrongly keeps answering the get- commands about that check, which SMT-LIB's assert mode makes errors), else null
protected IResponse	AbstractSolver.requireOptionEnabled(String commandName, String option)	Returns an error response if the given option has not been enabled (per AbstractSolver.get_option(IKeyword)), else null.
protected IResponse	AbstractSolver.requireSatOrUnknown(String commandName)	Returns an error response unless AbstractSolver.checkStatus() is sat or unknown, else null.
protected IResponse	AbstractSolver.requireUnsat(String commandName, String afterWhat)	Returns an error response unless AbstractSolver.checkStatus() is unsat, else null.
IResponse	AbstractSolver.reset()
IResponse	ISolver.reset()	Resets the solver to the initial state, clearing all assertions, declarations, and options.
IResponse	AbstractSolver.reset_assertions()
IResponse	ISolver.reset_assertions()	Removes asserted formulae (but not global declarations when :global-declarations is true).
IResponse	AbstractSolver.Pending.response()	The response read for the command, or null if not yet read
IResponse	IResponse.IFactory.sat()
protected IResponse	AbstractSolver.sendChange(AbstractSolver.StackChange kind, ICommand cmd)	Sends a command that changes the assertion stack, recording it (see recordChange)
protected IResponse	AbstractSolver.sendCommand(ICommand cmd)	Translates the given command and sends it to the solver process, returning the parsed response.
protected IResponse	AbstractSolver.sendExitCommand()	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.
protected IResponse	AbstractSolver.sendFailure(Exception e, IResponse otherwise)	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
protected IResponse	AbstractSolver.sendFailure(String text, Exception e)	As AbstractSolver.sendFailure(Exception, IResponse), with an error giving text and e otherwise
IResponse	AbstractSolver.sendPipelined(ICommand cmd)	Executes a command for which AbstractSolver.pipelines(ICommand) is true, sending it to the solver without waiting for the response.
protected IResponse	AbstractSolver.sendSeed()	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.
IResponse	AbstractSolver.set_info(IExpr.IKeyword key, IAttributeValue value)
IResponse	ISolver.set_info(IExpr.IKeyword key, IAttributeValue value)	Annotates the problem with an info attribute (e.g.
IResponse	AbstractSolver.set_logic(String logicName, IPos pos)	A set-logic the solver accepts ends sat or unsat mode; one it rejects (as SMT-LIB requires outside start mode) changes nothing.
IResponse	ISolver.set_logic(String logicName, IPos pos)	Sets the logic the solver should use.
IResponse	AbstractSolver.set_option(IExpr.IKeyword key, IAttributeValue value)
IResponse	ISolver.set_option(IExpr.IKeyword option, IAttributeValue value)	Sets an SMT-LIB option.
protected IResponse	AbstractSolver.set_option_impl(IExpr.IKeyword key, IAttributeValue value)	Override in subclasses to handle solver-specific options.
IResponse	AbstractSolver.start()
IResponse	ISolver.start()	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.
IResponse	IResponse.IFactory.stringLiteral(String value)	The argument has no SMT-LIB escapes and no enclosing quotes
IResponse	IResponse.IFactory.success()
IResponse	AbstractSolver.successOrEmpty(SMT.Configuration smtConfig)
protected IResponse	AbstractSolver.timeLimitResponse(String rawResponse)	Returns responseFactory.timeout(), recording that the solver has ended, if the raw response reports that the solver's whole-run time limit ended it; otherwise null.
protected IResponse	AbstractSolver.timeLimitResponseAfterExit()	For when a send has found the solver process gone: the timeout response if the process left this solver's report that its whole-run time limit ended it unread (that limit runs on the wall clock, so it can end the solver between commands, and its report then answers no command), or if it ended once that limit had passed; otherwise null
IResponse	IResponse.IFactory.timeout()	The response when the solver's whole-run time limit (SMT.Configuration#timeoutTotal) ended it, normalized across solvers (z3 answers 'timeout' and exits; cvc5 reports the timeout on stderr and aborts); every later command to that solver gets the same response.
IResponse	IResponse.IFactory.unknown()
IResponse	IResponse.IFactory.unsat()
IResponse	IResponse.IFactory.unsupported()

Methods in org.smtlib that return types with arguments of type IResponse

Modifier and Type	Method	Description
static List<IResponse>	TypeChecker.check(SymbolTable symTable, IExpr expr)	The main entry point for type-checking an IExpr (expected to be a Bool)
static List<IResponse>	TypeChecker.checkAssertion(SymbolTable symTable, IExpr expr)	The main entry point for type-checking an assert expression (expected to be a Bool); unlike TypeChecker.check(SymbolTable,IExpr), this checks the expression within a pushed scope that is merged into the enclosing scope on success (or popped on error).
static List<IResponse>	TypeChecker.checkFcn(SymbolTable symTable, IExpr.IIdentifier id, List<IExpr.IDeclaration> params, ISort result, IExpr expr)
static List<IResponse>	TypeChecker.checkFcn(SymbolTable symTable, IExpr.IIdentifier id, List<ISort> sorts, ISort result, IPos pos)
static List<IResponse>	TypeChecker.checkFcnRec(SymbolTable symTable, boolean global, IExpr.ISymbol id, List<IExpr.IDeclaration> params, ISort result, IExpr expr)	Type-checks a define-fun-rec command: verifies the symbol is new, validates sorts, pre-adds the function to the symbol table so the body may call it recursively, then checks the body expression.
static List<IResponse>	TypeChecker.checkFcnsRec(SymbolTable symTable, boolean global, List<IExpr.IFunctionDeclaration> decls, List<IExpr> bodies)	Type-checks a define-funs-rec command: for each declaration verifies the symbol is new and sorts are valid, pre-adds all functions to the symbol table for mutual recursion, then checks each body expression.
static List<IResponse>	TypeChecker.checkSortAbbreviation(SymbolTable symTable, IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
static List<IResponse>	TypeChecker.checkTerm(SymbolTable symTable, IExpr expr)	Type-checks a term of any sort (e.g.
static List<IResponse>	TypeChecker.validate(SMT.Configuration smtConfig, ICommand cmd)	Validates non-syntactic well-formedness of a command (user IDs, duplicate names, list sizes).
static List<IResponse>	TypeChecker.validateDatatypeNames(SymbolTable symTable, SMT.Configuration smtConfig, List<IExpr.ISortDeclaration> sortDecls, List<ISort.IDatatype> datatypes)	Checks that constructor and selector names introduced by a datatype group are not already defined (neither in the symbol table nor duplicated within the group).

Methods in org.smtlib with parameters of type IResponse

Modifier and Type	Method	Description
protected IResponse	AbstractSolver.checkImmediateExit(IResponse result)	Called with each response parsed from the solver.
protected IResponse	AbstractSolver.checkShape(AbstractSolver.Shape shape, String sent, String text, IResponse r)	r, if it has the given shape; else the error for a response out of step with the command sent, whose raw response was text
protected boolean	AbstractSolver.errorStopsSolver(IResponse error)	Whether, after the given error response, the solver stops processing input (whether or not its process actually exits).
void	Log.IListener.logOut(IResponse result)	Called when a response is logged to the normal output (it is expected that a line termination will be added); the argument is converted to text using the defaultPrinter in the smt configuration.
void	Log.logOut(IResponse r)	Prints the argument on the regular output stream and to any listeners
void	Log.StandardListener.logOut(IResponse response)	Writes the given response to the out stream, adding line termination
protected IResponse	AbstractSolver.modelResponse(IResponse r)	The get-model response r, without the leading symbol model if it has one: z3 4.3 to 4.7 and yices2 2.6.5 (with --smt2-model-format) answer (model (define-fun ...) ...), where SMT-LIB has the plain list ((define-fun ...) ...).
protected IResponse	AbstractSolver.proofResponse(IResponse r)	Wraps a parsed get-proof answer as an IProofResponse; anything else (an error, unsupported) is returned unchanged.
protected IResponse	AbstractSolver.recordChange(AbstractSolver.StackChange kind, IResponse response)	Records the response to a command of the given kind that changes the assertion stack, and returns it.
protected IResponse	AbstractSolver.sendFailure(Exception e, IResponse otherwise)	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
T	IVisitor.TreeVisitor.visit(IResponse e)
T	IVisitor.visit(IResponse e)
ISort	TypeChecker.visit(IResponse e)

Uses of IResponse in org.smtlib.command

Methods in org.smtlib.command that return IResponse

Modifier and Type	Method	Description
IResponse	C_assert.execute(ISolver solver)
IResponse	C_check_sat_assuming.execute(ISolver solver)
IResponse	C_check_sat.execute(ISolver solver)
IResponse	C_comment.execute(ISolver solver)
IResponse	C_declare_const.execute(ISolver solver)
IResponse	C_declare_datatype.execute(ISolver solver)
IResponse	C_declare_datatypes.execute(ISolver solver)
IResponse	C_declare_fun.execute(ISolver solver)
IResponse	C_declare_sort_parameter.execute(ISolver solver)
IResponse	C_declare_sort.execute(ISolver solver)
IResponse	C_define_const.execute(ISolver solver)
IResponse	C_define_fun_rec.execute(ISolver solver)
IResponse	C_define_fun.execute(ISolver solver)
IResponse	C_define_funs_rec.execute(ISolver solver)
IResponse	C_define_sort.execute(ISolver solver)
IResponse	C_echo.execute(ISolver solver)
IResponse	C_exit.execute(ISolver solver)
IResponse	C_get_assertions.execute(ISolver solver)
IResponse	C_get_assignment.execute(ISolver solver)
IResponse	C_get_info.execute(ISolver solver)
IResponse	C_get_model.execute(ISolver solver)
IResponse	C_get_option.execute(ISolver solver)
IResponse	C_get_proof.execute(ISolver solver)
IResponse	C_get_unsat_assumptions.execute(ISolver solver)
IResponse	C_get_unsat_core.execute(ISolver solver)
IResponse	C_get_value.execute(ISolver solver)
IResponse	C_pop.execute(ISolver solver)
IResponse	C_push.execute(ISolver solver)
IResponse	C_reset_assertions.execute(ISolver solver)
IResponse	C_reset.execute(ISolver solver)
IResponse	C_set_info.execute(ISolver solver)
IResponse	C_set_logic.execute(ISolver solver)
IResponse	C_set_option.execute(ISolver solver)

Uses of IResponse in org.smtlib.ext

Methods in org.smtlib.ext that return IResponse

Modifier and Type	Method	Description
IResponse	C_exec.execute(ISolver solver)	Executes the command, which executes the script
IResponse	C_what.execute(ISolver solver)

Uses of IResponse in org.smtlib.impl

Classes in org.smtlib.impl that implement IResponse

Modifier and Type	Class	Description
static class	Pos.AbstractExpr	A Printable that also implements IExpr, additionally holding the sort computed for the expression by the type checker (null if not yet, or never, computed).
static class	Response.AssertionsResponse	Implements the IResponse.IAssertionsResponse interface
static class	Response.AssignmentResponse	Implements the IResponse.IAssignmentResponse interface
static class	Response.Error	Implements the IResponse.IError interface
static class	Response.ProofResponse	Implements the IResponse.IProofResponse interface
static class	Response.Seq	Implementation of IAttributeList: a list of attributes returned by get-info.
static class	Response.UnsatAssumptionsResponse	Implements the IResponse.IUnsatAssumptionsResponse interface
static class	Response.UnsatCoreResponse	Implements the IResponse.IUnsatCoreResponse interface
static class	Response.ValueResponse	Implements the IResponse.IValueResponse interface
class	SMTExpr	This class defines a number of subclasses that implement the SMT-LIB abstract AST; they are used by commands and expressions.
static class	SMTExpr.AsIdentifier	This class represents an SMT as-identifier AST
static class	SMTExpr.Attribute<TT extends IAttributeValue>	Represents an SMT-LIB attribute: a keyword optionally paired with a value.
static class	SMTExpr.AttributedExpr	Represents an SMT-LIB attributed expression ((! expr attrs...)).
static class	SMTExpr.BinaryLiteral	Represents an SMT-LIB binary literal (e.g.
static class	SMTExpr.Decimal	This class represents an SMT Decimal literal expression or syntax token
static class	SMTExpr.Error	Represents an expression-level error node inserted during parsing to allow error recovery.
static class	SMTExpr.Exists	Represents an SMT-LIB existential quantifier expression.
static class	SMTExpr.FcnExpr	Represents a function-application expression: a qualified identifier applied to a list of argument expressions.
static class	SMTExpr.Forall	Represents an SMT-LIB universal quantifier expression.
static class	SMTExpr.HexLiteral	Represents an SMT-LIB hex literal (e.g.
static class	SMTExpr.Lambda	Represents an SMT-LIB lambda expression (SMT-LIB 2.7ff, HO-Core theory).
static class	SMTExpr.Let	Represents an SMT-LIB let expression: a list of bindings and a body expression.
static class	SMTExpr.Literal<T>	Abstract base class for all literal value AST nodes; holds the typed value and provides a shared implementation.
static class	SMTExpr.Match	Represents an SMT-LIB 2.7 match expression: an expression matched against a list of cases.
static class	SMTExpr.Numeral	This class represents an SMT Numeral expression or syntax token
static class	SMTExpr.ParameterizedIdentifier	This class represents an SMT parameterized-identifier AST (e.g.
static class	SMTExpr.PatternTerms	Represents the value of a :pattern attribute: a list of trigger terms.
static class	SMTExpr.StringLiteral	This class represents an SMT String literal expression or syntax token
static class	SMTExpr.Symbol	This class represents an SMT Symbol

Methods in org.smtlib.impl that return IResponse

Modifier and Type	Method	Description
IResponse	Response.Factory.continued_execution()
IResponse	Response.Factory.empty()
IResponse	Script.execute(ISolver solver)	Executes the current list
IResponse	Response.Factory.get_option_response(IAttributeValue v)
IResponse	Response.Factory.immediate_exit()
IResponse	Response.Factory.incomplete()
IResponse	Response.Factory.memout()
IResponse	Response.Factory.sat()
IResponse	Response.Factory.success()
IResponse	Response.Factory.timeout()
IResponse	Response.Factory.unknown()
IResponse	Response.Factory.unsat()
IResponse	Response.Factory.unsupported()

Uses of IResponse in org.smtlib.sexpr

Subinterfaces of IResponse in org.smtlib.sexpr

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

Classes in org.smtlib.sexpr that implement IResponse

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

Methods in org.smtlib.sexpr that return IResponse

Modifier and Type	Method	Description
IResponse	Parser.parseResponse(String response)

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

Modifier and Type	Method	Description
Void	Printer.visit(IResponse e)

Uses of IResponse in org.smtlib.solvers

Fields in org.smtlib.solvers declared as IResponse

Modifier and Type	Field	Description
protected IResponse	Solver_test.checkSatStatus	Internal state variable - set to sat, unsat, unknown when check-sat is run and then to null whenever an additional push, pop, assert, declare- or define- command is executed.

Methods in org.smtlib.solvers that return IResponse

Modifier and Type	Method	Description
IResponse	Solver_bitwuzla.assertExpr(IExpr sexpr)
IResponse	Solver_simplify.assertExpr(IExpr expr)
IResponse	Solver_test.assertExpr(IExpr expr)
IResponse	Solver_z3_4_3.assertExpr(IExpr sexpr)
IResponse	Solver_bitwuzla.check_sat()
IResponse	Solver_simplify.check_sat()
IResponse	Solver_test.check_sat()
IResponse	Solver_z3_4_3.check_sat()
IResponse	Solver_z3_recent.check_sat()
IResponse	Solver_bitwuzla.check_sat_assuming(IExpr... exprs)
IResponse	Solver_simplify.check_sat_assuming(IExpr... exprs)	check-sat-assuming postdates Simplify by well over a decade (added in SMT-LIB 2.6; Simplify's protocol has no concept of it), and this class has no override for it -- without one, it silently inherits Solver_test's stub (this class's superclass, the type-check-only pseudo-solver), which never talks to the real Simplify process at all and just echoes back whatever :status a script happened to declare (or "unknown" if none), regardless of whether the assumed literals are actually satisfiable.
IResponse	Solver_test.check_sat_assuming(IExpr... exprs)
IResponse	Solver_z3_4_3.check_sat_assuming(IExpr... exprs)	z3 4.3 answers unsupported for check-sat-assuming, so it is sent as z3's legacy (check-sat a1 ...
IResponse	Solver_z3_recent.check_sat_assuming(IExpr... exprs)
IResponse	Solver_test.checkSatStatus()
IResponse	Solver_simplify.declare_const(ICommand.Ideclare_const cmd)	See Solver_test.declare_const(ICommand.Ideclare_const).
IResponse	Solver_test.declare_const(ICommand.Ideclare_const cmd)
IResponse	Solver_z3_4_3.declare_const(ICommand.Ideclare_const cmd)
IResponse	Solver_bitwuzla.declare_datatype(ICommand.Ideclare_datatype cmd)	Not sent: Bitwuzla exits on it (see above)
IResponse	Solver_simplify.declare_datatype(ICommand.Ideclare_datatype cmd)	Datatypes postdate Simplify (added in SMT-LIB 2.6) and its untyped translation (see the class javadoc: "Simplify has no type definitions") has no way to express a datatype's constructors/selectors.
IResponse	Solver_test.declare_datatype(ICommand.Ideclare_datatype cmd)
IResponse	Solver_bitwuzla.declare_datatypes(ICommand.Ideclare_datatypes cmd)	Not sent: Bitwuzla exits on it (see above)
IResponse	Solver_simplify.declare_datatypes(ICommand.Ideclare_datatypes cmd)	See Solver_simplify.declare_datatype(org.smtlib.ICommand.Ideclare_datatype).
IResponse	Solver_test.declare_datatypes(ICommand.Ideclare_datatypes cmd)
IResponse	Solver_simplify.declare_fun(ICommand.Ideclare_fun cmd)
IResponse	Solver_test.declare_fun(ICommand.Ideclare_fun cmd)
IResponse	Solver_z3_4_3.declare_fun(ICommand.Ideclare_fun cmd)
IResponse	Solver_simplify.declare_sort(ICommand.Ideclare_sort cmd)	See Solver_test.declare_sort(ICommand.Ideclare_sort).
IResponse	Solver_test.declare_sort(ICommand.Ideclare_sort cmd)
IResponse	Solver_z3_4_3.declare_sort(ICommand.Ideclare_sort cmd)
IResponse	Solver_bitwuzla.declare_sort_parameter(ICommand.Ideclare_sort_parameter cmd)	Not sent: Bitwuzla exits on it (see above)
IResponse	Solver_simplify.declare_sort_parameter(ICommand.Ideclare_sort_parameter cmd)	See Solver_test.declare_sort_parameter(ICommand.Ideclare_sort_parameter).
IResponse	Solver_test.declare_sort_parameter(ICommand.Ideclare_sort_parameter cmd)
IResponse	Solver_simplify.define_const(ICommand.Idefine_const cmd)	See Solver_test.define_const(ICommand.Idefine_const).
IResponse	Solver_test.define_const(ICommand.Idefine_const cmd)
IResponse	Solver_simplify.define_fun(ICommand.Idefine_fun cmd)
IResponse	Solver_test.define_fun(ICommand.Idefine_fun cmd)
IResponse	Solver_z3_4_3.define_fun(ICommand.Idefine_fun cmd)
IResponse	Solver_bitwuzla.define_fun_rec(ICommand.Idefine_fun_rec cmd)	Not sent: Bitwuzla exits on it (see above)
IResponse	Solver_simplify.define_fun_rec(ICommand.Idefine_fun_rec cmd)	Recursive function definitions postdate Simplify (added in SMT-LIB 2.6) and its axiom-based translation (see Solver_simplify.define_fun(org.smtlib.ICommand.Idefine_fun)/Solver_simplify.declare_fun(org.smtlib.ICommand.Ideclare_fun)) has no way to express recursion.
IResponse	Solver_test.define_fun_rec(ICommand.Idefine_fun_rec cmd)
IResponse	Solver_bitwuzla.define_funs_rec(ICommand.Idefine_funs_rec cmd)	Not sent: Bitwuzla exits on it (see above)
IResponse	Solver_simplify.define_funs_rec(ICommand.Idefine_funs_rec cmd)	See Solver_simplify.define_fun_rec(org.smtlib.ICommand.Idefine_fun_rec).
IResponse	Solver_test.define_funs_rec(ICommand.Idefine_funs_rec cmd)
IResponse	Solver_simplify.define_sort(ICommand.Idefine_sort cmd)	See Solver_test.define_sort(ICommand.Idefine_sort).
IResponse	Solver_test.define_sort(ICommand.Idefine_sort cmd)
IResponse	Solver_z3_4_3.define_sort(ICommand.Idefine_sort cmd)
IResponse	Solver_simplify.echo(IExpr.IStringLiteral arg)
IResponse	Solver_test.echo(IExpr.IStringLiteral arg)
IResponse	Solver_yices2.echo(IExpr.IStringLiteral arg)	yices2 writes echo's text unquoted, so where it ends cannot be found (#136); the response to echo is its argument
IResponse	Solver_z3_4_3.echo(IExpr.IStringLiteral arg)	z3 4.3 writes echo's text unquoted, so where it ends cannot be found (#136); the response to echo is its argument
IResponse	Solver_z3_4_5.echo(IExpr.IStringLiteral arg)
IResponse	Solver_test.execute(ICommand cmd)	Once exited, every command but exit (and a comment) answers as a process-based solver's would
IResponse	Solver_altergo.exit()	Alt-Ergo is silent for exit, as for any successful command, but no echo can follow it, since the process ends; so success is answered once the process has ended.
IResponse	Solver_simplify.exit()
IResponse	Solver_test.exit()
IResponse	Solver_z3_4_3.exit()
IResponse	Solver_altergo.get_assertions()	Alt-Ergo ignores get-assertions, writing nothing; answered unsupported without sending it
IResponse	Solver_bitwuzla.get_assertions()	See Solver_bitwuzla.get_proof(): Bitwuzla rejects get-assertions the same way.
IResponse	Solver_cvc5.get_assertions()	cvc5 answers get-assertions with :produce-assertions off
IResponse	Solver_simplify.get_assertions()	See Solver_test.get_assertions().
IResponse	Solver_test.get_assertions()
IResponse	Solver_z3_4_3.get_assertions()	Not a correction: this adapter sends commands by its own means (z3 4.3 itself reports get-assertions without :produce-assertions, which set_option_impl sends as :interactive-mode)
IResponse	Solver_altergo.get_assignment()	Alt-Ergo answers get-assignment in assert mode after a check.
IResponse	Solver_bitwuzla.get_assignment()	See Solver_bitwuzla.get_proof(): Bitwuzla rejects get-assignment the same way.
IResponse	Solver_cvc5.get_assignment()	cvc5 answers get-assignment with :produce-assignments off (if :produce-models is on), and in assert mode after a check
IResponse	Solver_simplify.get_assignment()	See Solver_test.get_assignment().
IResponse	Solver_smtinterpol.get_assignment()	SMTInterpol answers get-assignment after unsat, and in assert mode after a check
IResponse	Solver_test.get_assignment()
IResponse	Solver_yices2.get_assignment()	yices2 answers get-assignment with :produce-assignments off, and in assert mode after a check
IResponse	Solver_z3_4_3.get_assignment()	z3 4.3 answers get-assignment (with ()) when :produce-assignments is not enabled, which SMT-LIB makes an error
IResponse	Solver_z3_recent.get_assignment()	z3 answers get-assignment with :produce-assignments off, and in assert mode after a check
IResponse	Solver_bitwuzla.get_info(IExpr.IKeyword key)	Answered entirely client-side (never forwarded -- see class comment point 1).
IResponse	Solver_simplify.get_info(IExpr.IKeyword key)	Simplify has no get-info; answered here
IResponse	Solver_test.get_info(IExpr.IKeyword key)
IResponse	Solver_yices2.get_info(IExpr.IKeyword key)	yices2 answers get-info :status with the last set-info :status value, but with (error "no info for :status") when none was set; SMT-LIB requires unsupported for a flag the solver does not support.
IResponse	Solver_z3_4_3.get_info(IExpr.IKeyword key)	Not a correction: this adapter sends commands by its own means, so it scrubs run-dependent values for testing itself, as AbstractSolver.get_info does
IResponse	Solver_z3_recent.get_info(IExpr.IKeyword key)	z3 reports a query stopped by its per-query time limit, -t:, with :reason-unknown "canceled" in incremental mode (after a push; checked with z3 4.16.0 and 5.1.0, while 4.8.12 and 4.12.6 give up first, as incomplete), and in every mode in 4.6 and 4.7; one-shot queries in newer versions, and other solvers such as cvc5, report "timeout".
IResponse	Solver_altergo.get_model()	Alt-Ergo answers get-model in assert mode after a check
IResponse	Solver_bitwuzla.get_model()	With :produce-models on, Bitwuzla writes nothing for get-model unless its last check returned sat (and crashes if a reset came since); after an assert, push, pop or reset-assertions, or with the option set after the check, it writes an ordinary error.
IResponse	Solver_cvc5.get_model()	cvc5 answers get-model in assert mode after a check
IResponse	Solver_simplify.get_model()	See Solver_test.get_model().
IResponse	Solver_smtinterpol.get_model()	SMTInterpol answers get-model with :produce-models off, and in assert mode after a check
IResponse	Solver_test.get_model()
IResponse	Solver_yices2.get_model()	yices2 answers get-model with :produce-models off, and in assert mode after a check
IResponse	Solver_z3_4_3.get_model()	The :produce-models check corrects z3 4.3 answering get-model with that option at its (non-standard) default of true; z3 4.3 itself reports get-model when no model is available
IResponse	Solver_z3_recent.get_model()	z3 answers get-model in assert mode after a check
IResponse	Solver_altergo.get_option(IExpr.IKeyword key)	Alt-Ergo ignores get-option, writing nothing; answered from the values set (see set_option_impl) and the SMT-LIB defaults
IResponse	Solver_bitwuzla.get_option(IExpr.IKeyword key)	Answered entirely client-side (never forwarded -- see class comment point 1): from whatever this run has set via Solver_bitwuzla.set_option_impl(org.smtlib.IExpr.IKeyword, org.smtlib.IAttributeValue), falling back to the standard SMT-LIB default for any option never set, and "unsupported" for anything not a recognized standard option at all (matching what a compliant solver would say about an option it doesn't have).
IResponse	Solver_cvc5.get_option(IExpr.IKeyword option)	See the class Javadoc: wraps a bare-symbol answer for a string-typed option (Utils.stringOptions -- currently just :regular-output-channel and :diagnostic-output-channel) into a proper SMT-LIB string literal with the same text, working around cvc5 answering those two with an unquoted symbol instead.
IResponse	Solver_simplify.get_option(IExpr.IKeyword key)	Simplify has no get-option; answered from the values kept by set_option
IResponse	Solver_test.get_option(IExpr.IKeyword key)
IResponse	Solver_z3_4_3.get_option(IExpr.IKeyword key)	Sent to the solver, except where z3 4.3's answer does not conform: it defaults :produce-models to true (SMT-LIB: false), writes the channel names unquoted, knows :produce-assertions only as :interactive-mode (see set_option_impl), and answers unsupported, not the default value, for a standard option it lacks
IResponse	Solver_altergo.get_proof()	Alt-Ergo writes nothing for get-proof (it ignores it); answered unsupported without sending it
IResponse	Solver_bitwuzla.get_proof()	Bitwuzla rejects get-proof as an unsupported command and exits (class comment point 1); a conforming solver without proofs answers unsupported.
IResponse	Solver_cvc5.get_proof()	cvc5 answers get-proof in assert mode after a check
IResponse	Solver_simplify.get_proof()	See Solver_test.get_proof().
IResponse	Solver_smtinterpol.get_proof()	SMTInterpol answers get-proof after sat, and in assert mode after a check
IResponse	Solver_test.get_proof()
IResponse	Solver_z3_4_3.get_proof()	z3 4.3 itself reports get-proof without :produce-proofs or when no proof is available; the checks here only give the same messages as the other adapters
IResponse	Solver_z3_recent.get_proof()	z3 answers get-proof in assert mode after a check
IResponse	Solver_altergo.get_unsat_assumptions()	Alt-Ergo ignores get-unsat-assumptions, writing nothing; answered unsupported without sending it
IResponse	Solver_bitwuzla.get_unsat_assumptions()	Bitwuzla writes nothing for get-unsat-assumptions unless its last check returned unsat; then it writes a fragment and an error if the option is off or was set after the check, or an assert, push, pop, reset-assertions or reset came since.
IResponse	Solver_cvc5.get_unsat_assumptions()	cvc5 aborts on get-unsat-assumptions in assert mode after a check
IResponse	Solver_simplify.get_unsat_assumptions()	See Solver_test.get_unsat_assumptions().
IResponse	Solver_smtinterpol.get_unsat_assumptions()	SMTInterpol answers get-unsat-assumptions in assert mode after a check
IResponse	Solver_test.get_unsat_assumptions()
IResponse	Solver_yices2.get_unsat_assumptions()	yices2 answers get-unsat-assumptions, wrongly, in assert mode after a check
IResponse	Solver_z3_recent.get_unsat_assumptions()	z3 answers get-unsat-assumptions in assert mode after a check
IResponse	Solver_altergo.get_unsat_core()	Alt-Ergo ignores get-unsat-core, writing nothing (with --sat-solver Tableaux it writes a non-SMT-LIB core after check-sat instead); answered unsupported without sending it
IResponse	Solver_bitwuzla.get_unsat_core()	With :produce-unsat-cores on, Bitwuzla writes nothing for get-unsat-core unless its last check returned unsat, and a fragment and an error if an assert, push, pop, reset-assertions or reset came since or the option was set after the check.
IResponse	Solver_cvc5.get_unsat_core()	cvc5 answers get-unsat-core in assert mode after a check
IResponse	Solver_simplify.get_unsat_core()	See Solver_test.get_unsat_core().
IResponse	Solver_smtinterpol.get_unsat_core()	SMTInterpol answers get-unsat-core in assert mode after a check
IResponse	Solver_test.get_unsat_core()
IResponse	Solver_yices2.get_unsat_core()	yices2 answers get-unsat-core in assert mode after a check
IResponse	Solver_z3_4_3.get_unsat_core()	z3 4.3 itself reports get-unsat-core without :produce-unsat-cores or when no core is available; the checks here only give the same messages as the other adapters
IResponse	Solver_z3_recent.get_unsat_core()	z3 answers get-unsat-core in assert mode after a check
IResponse	Solver_altergo.get_value(IExpr... terms)	Alt-Ergo ignores get-value, writing nothing; answered unsupported without sending it
IResponse	Solver_bitwuzla.get_value(IExpr... terms)	With :produce-models on, Bitwuzla writes nothing for get-value unless its last check returned sat, and a fragment and an error if an assert, push, pop or reset-assertions came since or the option was set after the check.
IResponse	Solver_cvc5.get_value(IExpr... terms)	cvc5 answers get-value in assert mode after a check
IResponse	Solver_simplify.get_value(IExpr... terms)	See Solver_test.get_value(IExpr...).
IResponse	Solver_smtinterpol.get_value(IExpr... terms)	SMTInterpol answers get-value with :produce-models off, and in assert mode after a check
IResponse	Solver_test.get_value(IExpr... terms)
IResponse	Solver_yices2.get_value(IExpr... terms)	yices2 answers get-value with :produce-models off, and in assert mode after a check
IResponse	Solver_z3_4_3.get_value(IExpr... terms)	See get_model: z3 4.3 defaults :produce-models to true
IResponse	Solver_z3_recent.get_value(IExpr... terms)	z3 answers get-value in assert mode after a check
protected IResponse	Solver_bitwuzla.parseResponse(String response)
protected IResponse	Solver_z3_4_3.parseResponse(String response)	Every command this adapter sends directly to the process ends here, so the solver's report that its whole-run limit ended it is recognized for all of them (see AbstractSolver#timeLimitResponse).
IResponse	Solver_bitwuzla.pop(int number)
IResponse	Solver_simplify.pop(int number)
IResponse	Solver_test.pop(int number)
IResponse	Solver_z3_4_3.pop(int number)
IResponse	Solver_bitwuzla.push(int number)
IResponse	Solver_simplify.push(int number)
IResponse	Solver_test.push(int number)
IResponse	Solver_z3_4_3.push(int number)
IResponse	Solver_bitwuzla.reset()	Bitwuzla's reset restores its option defaults, so the values get_option answers from are dropped too (except the output channels, which are jSMTLIB's own and stay redirected).
IResponse	Solver_cvc5.reset()
IResponse	Solver_simplify.reset()	Transplanted from Solver_test.reset(): this class has no real process operation to ask for a reset (Simplify's protocol has no such concept), so this remains an entirely local, client-side reset exactly as it was as an inherited Solver_test method -- it does not, and did not before this restructuring, reset any BG_PUSH state already accumulated in the real Simplify process itself.
IResponse	Solver_test.reset()
IResponse	Solver_z3_4_3.reset()
IResponse	Solver_z3_recent.reset()
IResponse	Solver_altergo.reset_assertions()	Alt-Ergo ignores reset-assertions, writing nothing and keeping the assertions; answered unsupported without sending it
IResponse	Solver_bitwuzla.reset_assertions()
IResponse	Solver_simplify.reset_assertions()	Transplanted from Solver_test.reset_assertions().
IResponse	Solver_test.reset_assertions()
IResponse	Solver_z3_4_3.reset_assertions()	z3-4.3 predates reset-assertions (added in SMT-LIB 2.5), and turns out to already handle that gracefully on its own: sent the literal, unrecognized command text, its SMT2 front-end replies with the literal token "unsupported" -- confirmed directly against a real z3-4.3.1 binary -- rather than erroring or crashing.
IResponse	Solver_z3_4_3.sendCommand(String cmd)
IResponse	Solver_z3_4_3.sendCommand(ICommand cmd)
IResponse	Solver_simplify.set_info(IExpr.IKeyword key, IAttributeValue value)	See Solver_test.set_info(IKeyword,IAttributeValue).
IResponse	Solver_test.set_info(IExpr.IKeyword key, IAttributeValue value)
IResponse	Solver_bitwuzla.set_logic(String logicName, IPos pos)	Bitwuzla (0.9.1) accepts a second set-logic, which SMT-LIB forbids outside start mode, so that is reported here (--relax allows it).
IResponse	Solver_simplify.set_logic(String logicName, IPos pos)
IResponse	Solver_test.set_logic(String logicName, IPos pos)
IResponse	Solver_z3_4_3.set_logic(String logicName, IPos pos)
IResponse	Solver_simplify.set_option(IExpr.IKeyword option, IAttributeValue value)	Simplify has no set-option; options are kept here, and the :produce- options answer unsupported since Simplify cannot produce models, proofs or cores
IResponse	Solver_test.set_option(IExpr.IKeyword key, IAttributeValue value)
protected IResponse	Solver_altergo.set_option_impl(IExpr.IKeyword key, IAttributeValue value)	Sent to Alt-Ergo, and kept here for get_option when Alt-Ergo accepts it
protected IResponse	Solver_bitwuzla.set_option_impl(IExpr.IKeyword key, IAttributeValue value)	Sent to bitwuzla, and also kept here for get_option, which bitwuzla does not support
protected IResponse	Solver_cvc5.set_option_impl(IExpr.IKeyword key, IAttributeValue value)
protected IResponse	Solver_z3_4_3_2.set_option_impl(IExpr.IKeyword key, IAttributeValue value)	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.
protected IResponse	Solver_z3_4_3.set_option_impl(IExpr.IKeyword key, IAttributeValue value)	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.
IResponse	Solver_altergo.start()
IResponse	Solver_bitwuzla.start()
IResponse	Solver_cvc5.start()
IResponse	Solver_simplify.start()
IResponse	Solver_smt.start()
IResponse	Solver_smtinterpol.start()
IResponse	Solver_test.start()
IResponse	Solver_yices2.start()
IResponse	Solver_z3_4_3.start()
IResponse	Solver_z3_recent.start()

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

Modifier and Type	Method	Description
protected boolean	Solver_cvc5.errorStopsSolver(IResponse error)	cvc5 carries on after most errors (e.g.
String	Solver_simplify.Translator.visit(IResponse e)