Package org.smtlib

Class AbstractSolver

java.lang.Object

org.smtlib.AbstractSolver

All Implemented Interfaces:

ISolver

Direct Known Subclasses:

Solver_altergo, Solver_bitwuzla, Solver_cvc5, Solver_simplify, Solver_smt, Solver_smtinterpol, Solver_z3_4_3, Solver_z3_recent

public class AbstractSolver
extends Object
implements ISolver

This class implements the operations of the org.smtlib.ISolver interface that map directly onto a single translated command sent to the solver process, with the expected response of a fully SMT-LIB compliant solver (a flat success/error/sat/unsat/ unknown/unsupported, or a bare value/attribute-pair for get-option/get-info): the command is translated with translate(INode) and sent via sendCommand(ICommand). get_assertions/get_value/get_assignment/get_unsat_core/ get_unsat_assumptions additionally reparse a non-flat response as the structured list they're actually specified to return (a (term value) pair list, a name list, etc. — see Parser.parseValueList() and its siblings), since parseResponse(String)'s generic parse only handles flat outcomes and just returns a raw s-expression for anything else. A subclass whose target solver deviates from strict SMT-LIB concrete syntax or response format overrides translate(INode) and/or parseResponse(String); a subclass whose target solver deviates in some other way overrides the individual ISolver method itself, same as before.

start() still throws UnsupportedOperationException, because AbstractSolver has no generic way to provide it: constructing the solver process and choosing its command line is inherently solver-specific, so every concrete adapter must override it. exit(), by contrast, has a working default (send the exit command tolerating a silent process exit, then tear down the process) that's generic enough to cover every solver seen so far; a subclass only overrides it when exiting needs solver-specific handling beyond that.

Thus this class can still be used as a base class for a solver adapter class that wants the convenience of not having to implement every operation at once (remove AbstractSolver as a base class and retain ISolver as an interface to check that all ISolver methods are indeed present in the derived class), while getting working default behavior for the operations that don't need solver-specific handling.

Author:

David Cok

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static final class	AbstractSolver.Pending	The response returned for a command sent by sendPipelined(ICommand) whose actual response has not yet been read; AbstractSolver.Pending.isReady() tells when it has (see readPipelined(boolean)), and AbstractSolver.Pending.response() then gives it.
protected static enum	AbstractSolver.Shape	The kinds of response a command has besides an error or unsupported (#149)
static enum	AbstractSolver.StackChange	The kinds of command that change the assertion stack: each returns a conforming solver to assert mode, where the get- commands about the last check are errors (declare-const is declare-fun, declare-datatypes is declare-datatype, define-funs-rec is define-fun-rec), as does a set-logic that a solver accepts after a check (SMT-LIB makes that an error, but --relax may allow it)

Nested classes/interfaces inherited from interface org.smtlib.ISolver

ISolver.CreationException

Field Summary

Fields

Modifier and Type	Field	Description
protected IResponse	checkSatStatus	The response to the most recent check-sat or check-sat-assuming, or null if there is none.
protected static final long	END_WAIT_MILLIS	How long (ms) to wait for the solver process to end, once a send has found it gone or ending
protected boolean	endedByTimeLimit	True once the solver's whole-run time limit (smtConfig.timeoutTotal) has ended it; every later command then gets responseFactory.timeout() (exit tolerates it), rather than an error about the process having exited.
protected static boolean	isMac
protected static boolean	isWindows
protected int	linesOffset	The correction to a line number the solver reports for the command whose response is being read: line N of the solver's input is shown as line N - linesOffset, the line of the user's source on which that command starts.
protected Map<String,IAttributeValue>	options	Map that keeps current values of options.
protected final IExpr.IKeyword	printSuccess
protected boolean	printSuccessResponse
protected SMT.Configuration	smtConfig	SMT configuration — set by each concrete subclass constructor.
static final String	SOLVER_EXITED	The error every command answers once the solver process has exited (other than by its whole-run time limit)
protected SolverProcess	solverProcess	The object that interacts with external processes

Constructor Summary

Constructors

Constructor	Description
AbstractSolver()

Method Summary

Modifier and Type	Method	Description
IResponse	assertExpr(IExpr sexpr)	Adds the given expression to the current assertion-stack frame.
IResponse	check_sat()	Checks whether the current assertion set is satisfiable under the current logic.
IResponse	check_sat_assuming(IExpr... exprs)	Checks satisfiability under the current assertion set plus the given propositional assumptions.
protected IResponse	checkImmediateExit(IResponse result)	Called with each response parsed from the solver.
IResponse	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	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	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	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
void	comment(String comment)	Forwards a standalone comment (its own C_comment pseudo-command -- see issue #42) to the solver process, uniformly for every solver adapter: a comment is legal SMT-LIB input (any conforming solver must silently ignore it), and the solver's log then shows the script's comments.
protected String	correctResponse(ICommand cmd, String response)	The solver's raw response to cmd (sent by sendCommand and waited for), corrected where the solver departs from SMT-LIB; an adapter overrides this to patch a specific non-conforming response
IResponse	declare_const(ICommand.Ideclare_const cmd)	Declares a new uninterpreted constant; returns success or an SMT error response
IResponse	declare_datatype(ICommand.Ideclare_datatype cmd)	Declares a new datatype sort; returns success or an SMT error response
IResponse	declare_datatypes(ICommand.Ideclare_datatypes cmd)	Declares mutually recursive datatype sorts; returns success or an SMT error response
IResponse	declare_fun(ICommand.Ideclare_fun cmd)	Declares a new uninterpreted function (or constant); returns success or an SMT error response
IResponse	declare_sort(ICommand.Ideclare_sort cmd)	Declares a new uninterpreted sort; returns success or an SMT error response
IResponse	declare_sort_parameter(ICommand.Ideclare_sort_parameter cmd)	Declares a new sort parameter (polymorphic sort variable); returns success or an SMT error response
IResponse	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	define_fun(ICommand.Idefine_fun cmd)	Defines a named function or constant; returns success or an SMT error response
IResponse	define_fun_rec(ICommand.Idefine_fun_rec cmd)	Defines a named recursive function; returns success or an SMT error response
IResponse	define_funs_rec(ICommand.Idefine_funs_rec cmd)	Defines a group of mutually recursive functions; returns success or an SMT error response
IResponse	define_sort(ICommand.Idefine_sort cmd)	Defines a sort abbreviation; returns success or an SMT error response
protected int	earlierSourceLine(int n)	The source line for line n of the solver's input, which may be that of an earlier command
IResponse	echo(IExpr.IStringLiteral arg)	Echoes the argument string back to the output channel.
protected boolean	errorStopsSolver(IResponse error)	Whether, after the given error response, the solver stops processing input (whether or not its process actually exits).
IResponse	execute(ICommand cmd)	Once the solver process has exited, every command but exit (and a comment, which has no response) answers exitedResponse(), including those an adapter answers itself or checks with its own queries
IResponse	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	exit()	Terminates the solver; no further commands are permitted.
IResponse	exitedResponse()	The response to any command once the solver process has exited: timeout if its whole-run time limit ended it, else the error SOLVER_EXITED; null while the process runs (or has not been started)
void	finishPipelined()	At the end of a pipelined run: waits briefly for output still arriving after the last response, and reports any as out of step
void	forceExit()	Terminates the solver forcibly without sending commands (e.g.
IResponse	get_assertions()	Returns the list of formulae in the current assertion set, in the order they were asserted.
IResponse	get_assignment()	Returns the truth-value assignments for all named Boolean formulae in the current model.
IResponse	get_info(IExpr.IKeyword option)	Returns the value of the named info item.
IResponse	get_model()	Returns a satisfying model for the current assertion set.
IResponse	get_option(IExpr.IKeyword option)	Returns the current value of the named option.
IResponse	get_proof()	Returns a proof of unsatisfiability for the current assertion set.
IResponse	get_unsat_assumptions()	Returns the subset of check-sat-assuming assumptions that caused the result to be unsat.
IResponse	get_unsat_core()	Returns the named formulae that form an unsatisfiable core of the current assertion set.
IResponse	get_value(IExpr... terms)	Returns the values of the given expressions in the current satisfying model.
boolean	hasPending()	Whether some pipelined command's response has not yet been read
protected boolean	inSatMode()	Whether the most recent check command was answered sat or unknown, with the assertion stack unchanged since: SMT-LIB's sat mode (false once the whole-run time limit has ended the solver)
void	interrupt()	Interrupts the command the solver is running (see SolverProcess.interrupt())
protected boolean	inUnsatMode()	Whether the most recent check command was answered unsat, with the assertion stack unchanged since: SMT-LIB's unsat mode (false once the whole-run time limit has ended the solver)
protected boolean	isFlatResponse(String response)	True if the given raw response text is a flat outcome (empty/success/unsupported/an (error ...) s-expression) rather than a structured list — used by the get_assertions/get_value/get_assignment/get_unsat_core/get_unsat_assumptions defaults below to decide whether to delegate to parseResponse(String) or reparse the response as the structured list they actually expect.
protected boolean	isTimeLimitResponse(String rawResponse)	Whether the raw response text is this solver's report that its whole-run time limit (smtConfig.timeoutTotal) ended it; consulted only when that limit is set.
protected List<Pattern>	lineNumberPatterns()	Patterns matching the line numbers in this solver's messages about the command answered: group 1 is the text before the number, group 2 the number, group 3 the text after it
protected void	logSolverDiagnostics()	Logs the standard-error text the solver wrote along with its replies (see SolverProcess.takeDiagnosticOutput), noting a whole-run time-limit report there: the reply stands, but the solver has ended
protected IResponse	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 int	nextSolverLine()	The solver line, as the solver numbers lines in its messages, on which the next text sent starts; overridden for a solver that does not number the lines of its whole input
protected static String	normalizeForTesting(String raw, IExpr.IKeyword infoflag)	Replaces known sources of non-deterministic content in a raw solver response with a fixed placeholder, so that --testing runs produce byte-for-byte reproducible output across machines and repeated runs.
boolean	outOfStep()	Whether pipelined responses have been found out of step with their commands (#149)
protected IResponse	parseResponse(String response)	Parses the solver's raw response text.
boolean	pipelines(ICommand cmd)	Whether sendPipelined(ICommand) may send the command without waiting for its response.
IResponse	pop(int number)	Removes the given number of assertion-stack frames from the solver state.
protected IResponse	proofResponse(IResponse r)	Wraps a parsed get-proof answer as an IProofResponse; anything else (an error, unsupported) is returned unchanged.
IResponse	push(int number)	Adds the given number of empty assertion-stack frames to the solver state.
void	readPipelined(boolean wait)	Reads what the solver has written for pipelined commands, matching each response to its command in order; with wait, until every pending command has its response (or the solver has stopped), else only what has already arrived.
protected IResponse	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 boolean	reportsEarlierLines()	Whether the solver's messages name lines of earlier commands (see earlierSourceLine(int))
protected void	reportSeedIgnored()	Reports that --seed, if given, is ignored, for an adapter whose solver has no random seed
protected IResponse	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	requireOptionEnabled(String commandName, String option)	Returns an error response if the given option has not been enabled (per get_option(IKeyword)), else null.
protected IResponse	requireSatOrUnknown(String commandName)	Returns an error response unless checkStatus() is sat or unknown, else null.
protected IResponse	requireUnsat(String commandName, String afterWhat)	Returns an error response unless checkStatus() is unsat, else null.
IResponse	reset()	Resets the solver to the initial state, clearing all assertions, declarations, and options.
IResponse	reset_assertions()	Removes asserted formulae (but not global declarations when :global-declarations is true).
static int	responseEnd(CharSequence s, int start)	The index just past the response that starts at start (an atom, a string literal, a quoted symbol, or one balanced S-expression), or -1 if that response is not yet complete
protected boolean	selfReportsImmediateExit()	Overridden by a subclass whose target solver's :error-behavior is immediate-exit (e.g.
protected IResponse	sendChange(AbstractSolver.StackChange kind, ICommand cmd)	Sends a command that changes the assertion stack, recording it (see recordChange)
protected IResponse	sendCommand(ICommand cmd)	Translates the given command and sends it to the solver process, returning the parsed response.
protected IResponse	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	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 SOLVER_EXITED; otherwise otherwise
protected IResponse	sendFailure(String text, Exception e)	As sendFailure(Exception, IResponse), with an error giving text and e otherwise
IResponse	sendPipelined(ICommand cmd)	Executes a command for which pipelines(ICommand) is true, sending it to the solver without waiting for the response.
protected String	sendScriptText(boolean listen, String... text)	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
protected IResponse	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	set_info(IExpr.IKeyword key, IAttributeValue value)	Annotates the problem with an info attribute (e.g.
IResponse	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	set_option(IExpr.IKeyword key, IAttributeValue value)	Sets an SMT-LIB option.
protected IResponse	set_option_impl(IExpr.IKeyword key, IAttributeValue value)	Override in subclasses to handle solver-specific options.
void	setSourceLine(int line)	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
protected static AbstractSolver.Shape	shapeOf(ICommand cmd)	The kind of response cmd has
SMT.Configuration	smt()	Returns the configuration object with which the solver is initialized
String	solverName()	A public, user-readable name for the solver adapter class
protected boolean	solverPrintsSuccess()	Whether the solver writes 'success' for a successful command, so that every command gets one response.
IResponse	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	successOrEmpty(SMT.Configuration smtConfig)
protected IResponse	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	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
protected String	translate(INode sexpr)	Translates an in-memory node into the text sent to the solver process.
protected List<IExpr>	unsatAssumptionsElements(List<IExpr> reply)	The elements of a get-unsat-assumptions reply that belong in the response (all of them); an adapter whose solver's reply holds others filters them out
protected List<IExpr>	unsatCoreElements(List<IExpr> reply)	The elements of a get-unsat-core reply that belong in the unsat core (all of them); an adapter whose solver's reply holds others filters them out
protected String	withSourceLines(String text)	The text with each line number lineNumberPatterns finds in it rewritten as a source line (see linesOffset)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Details

isWindows

protected static boolean isWindows

isMac

protected static boolean isMac

printSuccess

protected final IExpr.IKeyword printSuccess

printSuccessResponse

protected boolean printSuccessResponse

solverProcess

protected SolverProcess solverProcess

The object that interacts with external processes

linesOffset

protected int linesOffset

The correction to a line number the solver reports for the command whose response is being read: line N of the solver's input is shown as line N - linesOffset, the line of the user's source on which that command starts. The solver numbers the lines it receives, which are not the source's: jSMTLIB adds lines (a priming :print-success, a pipelining barrier, an adapter's own query), omits lines (blank lines, commands answered here) and sends each command on one line. So rather than tracking each such difference, linesOffset is set by sendScriptText(boolean, java.lang.String...) whenever text is sent for a command of the script, from the solver line that text starts on and the command's source line (see setSourceLine(int)). A command without a source line (one built through the API) counts as the line after the previous one. An adapter rewrites the line numbers in its solver's messages with withSourceLines(java.lang.String).

smtConfig

protected SMT.Configuration smtConfig

SMT configuration — set by each concrete subclass constructor.

options

protected Map<String,IAttributeValue> options

Map that keeps current values of options.

checkSatStatus

protected IResponse checkSatStatus

The response to the most recent check-sat or check-sat-assuming, or null if there is none. Whether the solver is still in the mode it set is given by checkStatus().

endedByTimeLimit

protected boolean endedByTimeLimit

True once the solver's whole-run time limit (smtConfig.timeoutTotal) has ended it; every later command then gets responseFactory.timeout() (exit tolerates it), rather than an error about the process having exited.

END_WAIT_MILLIS

protected static final long END_WAIT_MILLIS

How long (ms) to wait for the solver process to end, once a send has found it gone or ending

See Also:

• Constant Field Values

SOLVER_EXITED

public static final String SOLVER_EXITED

The error every command answers once the solver process has exited (other than by its whole-run time limit)

See Also:

• Constant Field Values

Constructor Details

AbstractSolver

public AbstractSolver()

Method Details

setSourceLine

public void setSourceLine(int line)

Description copied from interface: 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

Specified by:

setSourceLine in interface ISolver

nextSolverLine

protected int nextSolverLine()

The solver line, as the solver numbers lines in its messages, on which the next text sent starts; overridden for a solver that does not number the lines of its whole input

reportsEarlierLines

protected boolean reportsEarlierLines()

Whether the solver's messages name lines of earlier commands (see earlierSourceLine(int))

sendScriptText

protected String sendScriptText(boolean listen,
 String... text)
                         throws IOException

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

Throws:

IOException

logSolverDiagnostics

protected void logSolverDiagnostics()

Logs the standard-error text the solver wrote along with its replies (see SolverProcess.takeDiagnosticOutput), noting a whole-run time-limit report there: the reply stands, but the solver has ended

earlierSourceLine

protected int earlierSourceLine(int n)

The source line for line n of the solver's input, which may be that of an earlier command

lineNumberPatterns

protected List<Pattern> lineNumberPatterns()

Patterns matching the line numbers in this solver's messages about the command answered: group 1 is the text before the number, group 2 the number, group 3 the text after it

withSourceLines

protected String withSourceLines(String text)

The text with each line number lineNumberPatterns finds in it rewritten as a source line (see linesOffset)

selfReportsImmediateExit

protected boolean selfReportsImmediateExit()

Overridden by a subclass whose target solver's :error-behavior is immediate-exit (e.g. cvc5, yices2) rather than the SMT-LIB default of continued-execution -- such a solver's process may start exiting asynchronously right after it reports an error, and SolverProcess.send(boolean, String...)'s own process.isAlive() check can still read true for a brief window afterward (OS process-death bookkeeping lags the actual exit) -- see sendCommand(ICommand, boolean), which uses this to give a solver that just reported an error a moment to actually finish dying before the next command's liveness check runs, closing that race deterministically rather than guessing from the error's content whether the process will actually exit.

checkImmediateExit

protected IResponse checkImmediateExit(IResponse result)

Called with each response parsed from the solver. After an error response from a selfReportsImmediateExit() solver, gives its process a moment to finish exiting (see IMMEDIATE_EXIT_SETTLE_MILLIS). If the error is one after which the solver no longer processes input (errorStopsSolver(IResponse)) and the process is still alive, it is stopped, since a later command -- or exit() -- would otherwise wait forever for a reply. Only the OS process is stopped; the adapter is left as it is, so later commands answer that the solver process has exited and exit() cleans up normally.

errorStopsSolver

protected boolean errorStopsSolver(IResponse error)

Whether, after the given error response, the solver stops processing input (whether or not its process actually exits). False by default; see Solver_cvc5.

solverName

public String solverName()

Description copied from interface: ISolver

A public, user-readable name for the solver adapter class

Specified by:

solverName in interface ISolver

forceExit

public void forceExit()

Description copied from interface: ISolver

Terminates the solver forcibly without sending commands (e.g. by killing the process).

Specified by:

forceExit in interface ISolver

interrupt

public void interrupt()

Interrupts the command the solver is running (see SolverProcess.interrupt())

successOrEmpty

public IResponse successOrEmpty(SMT.Configuration smtConfig)

checkPrintSuccess

public IResponse checkPrintSuccess(SMT.Configuration smtConfig,
 IExpr.IKeyword key,
 IAttributeValue value)

Answers a set-option of :print-success locally (it is never sent), else returns null

translate

protected String translate(INode sexpr)
                    throws IVisitor.VisitorException

Translates an in-memory node into the text sent to the solver process. The base behavior assumes the solver is fully SMT-LIB compliant, so it is exactly what the default printer produces. Override in a subclass whose target solver deviates from strict SMT-LIB concrete syntax.

Throws:

IVisitor.VisitorException

parseResponse

protected IResponse parseResponse(String response)

Parses the solver's raw response text. The base behavior assumes the response is exactly standard SMT-LIB concrete syntax: success/sat/unsat/unknown/unsupported/ true/false, an (error "...") s-expression, a bare value (get-option), or a single (:keyword value) attribute pair (get-info). It does not build the richer structured IResponse subtypes that get_value/get_model/get_proof/ get_assertions/get_unsat_core/get_unsat_assumptions/get_assignment need, nor does it correct for any real solver's non-compliant quirks (e.g. legacy bit-vector literal syntax) — override in a subclass whose target solver needs either.

sendCommand

protected IResponse sendCommand(ICommand cmd)

Translates the given command and sends it to the solver process, returning the parsed response. This is the mechanism behind the default implementations below; a subclass may also call it directly to send a command built some other way.

sendExitCommand

protected IResponse 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. The tolerated result is "", which Parser.parseResponse("") already turns into a plain empty response -- the same outcome a real empty response (e.g. under :print-success false) already produces, so no separate response-construction case is needed here. A subclass's exit() should call this instead of sendCommand(commandFactory.exit()) directly.

normalizeForTesting

protected static String normalizeForTesting(String raw,
 IExpr.IKeyword infoflag)

Replaces known sources of non-deterministic content in a raw solver response with a fixed placeholder, so that --testing runs produce byte-for-byte reproducible output across machines and repeated runs. Deliberately a short, explicit list rather than a broad catch-all, so it can't silently mask an actual difference in solver output: elapsed-time figures (e.g. cvc5's :all-statistics response embeds these as bare, unquoted "NNNms" tokens, which aren't valid SMT-LIB syntax at all and would otherwise cascade into a wall of "Invalid token" parse errors that also differ every run), and, in a reply to get-info :all-statistics, every number: statistics are run-dependent by nature, and solvers name them as they please. Their names are kept.

isTimeLimitResponse

protected boolean isTimeLimitResponse(String rawResponse)

Whether the raw response text is this solver's report that its whole-run time limit (smtConfig.timeoutTotal) ended it; consulted only when that limit is set. Solvers report this in their own ways, so an adapter whose solver has such a limit overrides this; the default recognizes nothing.

timeLimitResponse

protected IResponse 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. For adapters that send commands by their own means.

timeLimitResponseAfterExit

protected IResponse 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

sendFailure

protected IResponse 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 SOLVER_EXITED; otherwise otherwise

sendFailure

protected IResponse sendFailure(String text,
 Exception e)

As sendFailure(Exception, IResponse), with an error giving text and e otherwise

exitedResponse

public IResponse exitedResponse()

The response to any command once the solver process has exited: timeout if its whole-run time limit ended it, else the error SOLVER_EXITED; null while the process runs (or has not been started)

execute

public IResponse execute(ICommand cmd)

Once the solver process has exited, every command but exit (and a comment, which has no response) answers exitedResponse(), including those an adapter answers itself or checks with its own queries

Specified by:

execute in interface ISolver

correctResponse

protected String correctResponse(ICommand cmd,
 String response)

The solver's raw response to cmd (sent by sendCommand and waited for), corrected where the solver departs from SMT-LIB; an adapter overrides this to patch a specific non-conforming response

pipelines

public boolean pipelines(ICommand cmd)

Whether sendPipelined(ICommand) may send the command without waiting for its response. True for the commands whose execution here sends the command (once) and has nothing to do with its response beyond returning it -- except check-sat, whose response becomes checkSatStatus when it is read. A subclass returns false for a command whose solver response needs correcting before it is compliant, or that it executes otherwise, and for all commands if it does not send them through sendCommand.

sendPipelined

public IResponse sendPipelined(ICommand cmd)

Executes a command for which pipelines(ICommand) is true, sending it to the solver without waiting for the response. Returns a AbstractSolver.Pending response if the command was sent, or the actual response if it was not (e.g. an error found before sending). Any other request to this solver first waits for the pending responses, but a caller must call readPipelined(boolean) with true itself before executing a command that is checked against an earlier response (such as get-value against check-sat).

executePipelined

public IResponse executePipelined(List<ICommand> commands)

Executes the commands in order, as a script does: returns the first error, or else the last command's response. Commands that pipelines(ICommand) allows are sent without waiting for their responses; check-sat, check-sat-assuming and every other command first wait for the pending responses, so that none is executed after an error. Used by IScript.execute when SMT.Configuration.pipeline is set.

hasPending

public boolean hasPending()

Whether some pipelined command's response has not yet been read

readPipelined

public void readPipelined(boolean wait)

Reads what the solver has written for pipelined commands, matching each response to its command in order; with wait, until every pending command has its response (or the solver has stopped), else only what has already arrived. Standard error is checked each time output is read. Which command its text belongs to is not known while the solver runs, so it is kept until either the solver stops, when it becomes the response of the first command without one (as listen() would return it), or every pending response has been read, when it is logged as diagnostic output.

finishPipelined

public void finishPipelined()

At the end of a pipelined run: waits briefly for output still arriving after the last response, and reports any as out of step

solverPrintsSuccess

protected boolean solverPrintsSuccess()

Whether the solver writes 'success' for a successful command, so that every command gets one response. True by default (the solver process is kept at :print-success true); an adapter whose solver does not (alt-ergo) returns false, and its responses are then matched by shape (see matchSilent), its commands being sent as when pipelining even when not (see sendCommand).

outOfStep

public boolean outOfStep()

Whether pipelined responses have been found out of step with their commands (#149)

shapeOf

protected static AbstractSolver.Shape shapeOf(ICommand cmd)

The kind of response cmd has

checkShape

protected IResponse 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

responseEnd

public static int responseEnd(CharSequence s,
 int start)

The index just past the response that starts at start (an atom, a string literal, a quoted symbol, or one balanced S-expression), or -1 if that response is not yet complete

start

public IResponse start()

Description copied from interface: 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.

Specified by:

start in interface ISolver

Returns:

success or an SMT error response

See Also:

• ISolver.start()

sendSeed

protected IResponse sendSeed()
                      throws IOException

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. Returns an error if the solver rejects it, else null.

Throws:

IOException

reportSeedIgnored

protected void reportSeedIgnored()

Reports that --seed, if given, is ignored, for an adapter whose solver has no random seed

exit

public IResponse exit()

Description copied from interface: ISolver

Terminates the solver; no further commands are permitted.

Specified by:

exit in interface ISolver

Returns:

success or an SMT error response

See Also:

• ISolver.exit()

echo

public IResponse echo(IExpr.IStringLiteral arg)

Description copied from interface: ISolver

Echoes the argument string back to the output channel.

Specified by:

echo in interface ISolver

Returns:

the argument as an IResponse

comment

public void comment(String comment)

Forwards a standalone comment (its own C_comment pseudo-command -- see issue #42) to the solver process, uniformly for every solver adapter: a comment is legal SMT-LIB input (any conforming solver must silently ignore it), and the solver's log then shows the script's comments. It has no response to wait for. A trailing, same-line comment never reaches here -- it's captured as Command.trailingText instead (see Parser.parseCommand()) and is never sent to a solver.

Specified by:

comment in interface ISolver

set_logic

public IResponse 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.

Specified by:

set_logic in interface ISolver

Parameters:

logicName - the name of the logic

pos - source position used only for error messages; may be null

Returns:

success or unsupported or an SMT error response

See Also:

• ISolver.set_logic(String,IPos)

reset

public IResponse reset()

Description copied from interface: ISolver

Resets the solver to the initial state, clearing all assertions, declarations, and options.

Specified by:

reset in interface ISolver

Returns:

success or an SMT error response

See Also:

• ISolver.reset()

reset_assertions

public IResponse reset_assertions()

Description copied from interface: ISolver

Removes asserted formulae (but not global declarations when :global-declarations is true).

Specified by:

reset_assertions in interface ISolver

Returns:

success or an SMT error response

See Also:

• ISolver.reset_assertions()

push

public IResponse push(int number)

Description copied from interface: ISolver

Adds the given number of empty assertion-stack frames to the solver state.

Specified by:

push in interface ISolver

Parameters:

number - non-negative number of frames to push

Returns:

success or an SMT error response

See Also:

• ISolver.push(int)

pop

public IResponse pop(int number)

Description copied from interface: ISolver

Removes the given number of assertion-stack frames from the solver state.

Specified by:

pop in interface ISolver

Parameters:

number - non-negative number of frames to pop

Returns:

success or an SMT error response

See Also:

• ISolver.pop(int)

assertExpr

public IResponse assertExpr(IExpr sexpr)

Description copied from interface: ISolver

Adds the given expression to the current assertion-stack frame. The SMT-LIB command name is assert; the Java method name differs to avoid the Java reserved word.

Specified by:

assertExpr in interface ISolver

Returns:

success or an SMT error response

See Also:

• ISolver.assertExpr(IExpr)

check_sat

public IResponse check_sat()

Description copied from interface: ISolver

Checks whether the current assertion set is satisfiable under the current logic.

Specified by:

check_sat in interface ISolver

Returns:

sat, unsat, unknown, or an SMT error response

See Also:

• ISolver.check_sat()

check_sat_assuming

public IResponse check_sat_assuming(IExpr... exprs)

Description copied from interface: ISolver

Checks satisfiability under the current assertion set plus the given propositional assumptions.

Specified by:

check_sat_assuming in interface ISolver

Returns:

sat, unsat, unknown, or an SMT error response

See Also:

• ISolver.check_sat_assuming(IExpr...)

define_const

public IResponse define_const(ICommand.Idefine_const cmd)

Description copied from interface: ISolver

Defines a named constant — syntactic sugar for define-fun with no parameters; returns success or an SMT error response

Specified by:

define_const in interface ISolver

See Also:

• ISolver.define_const(ICommand.Idefine_const)

define_fun

public IResponse define_fun(ICommand.Idefine_fun cmd)

Description copied from interface: ISolver

Defines a named function or constant; returns success or an SMT error response

Specified by:

define_fun in interface ISolver

See Also:

• ISolver.define_fun(ICommand.Idefine_fun)

define_fun_rec

public IResponse define_fun_rec(ICommand.Idefine_fun_rec cmd)

Description copied from interface: ISolver

Defines a named recursive function; returns success or an SMT error response

Specified by:

define_fun_rec in interface ISolver

See Also:

• ISolver.define_fun_rec(ICommand.Idefine_fun_rec)

define_funs_rec

public IResponse define_funs_rec(ICommand.Idefine_funs_rec cmd)

Description copied from interface: ISolver

Defines a group of mutually recursive functions; returns success or an SMT error response

Specified by:

define_funs_rec in interface ISolver

See Also:

• ISolver.define_funs_rec(ICommand.Idefine_funs_rec)

declare_const

public IResponse declare_const(ICommand.Ideclare_const cmd)

Description copied from interface: ISolver

Declares a new uninterpreted constant; returns success or an SMT error response

Specified by:

declare_const in interface ISolver

See Also:

• ISolver.declare_const(ICommand.Ideclare_const)

declare_fun

public IResponse declare_fun(ICommand.Ideclare_fun cmd)

Description copied from interface: ISolver

Declares a new uninterpreted function (or constant); returns success or an SMT error response

Specified by:

declare_fun in interface ISolver

See Also:

• ISolver.declare_fun(ICommand.Ideclare_fun)

define_sort

public IResponse define_sort(ICommand.Idefine_sort cmd)

Description copied from interface: ISolver

Defines a sort abbreviation; returns success or an SMT error response

Specified by:

define_sort in interface ISolver

See Also:

• ISolver.define_sort(ICommand.Idefine_sort)

declare_sort

public IResponse declare_sort(ICommand.Ideclare_sort cmd)

Description copied from interface: ISolver

Declares a new uninterpreted sort; returns success or an SMT error response

Specified by:

declare_sort in interface ISolver

See Also:

• ISolver.declare_sort(ICommand.Ideclare_sort)

declare_sort_parameter

public IResponse declare_sort_parameter(ICommand.Ideclare_sort_parameter cmd)

Description copied from interface: ISolver

Declares a new sort parameter (polymorphic sort variable); returns success or an SMT error response

Specified by:

declare_sort_parameter in interface ISolver

See Also:

• ISolver.declare_sort_parameter(ICommand.Ideclare_sort_parameter)

set_option

public IResponse set_option(IExpr.IKeyword key,
 IAttributeValue value)

Description copied from interface: ISolver

Sets an SMT-LIB option.

Specified by:

set_option in interface ISolver

Parameters:

key - the keyword naming the option

value - the value to set

Returns:

success, unsupported, or an SMT error response

See Also:

• The channel options are not sent: responses reach the user through jSMTLIB's own output, so it is jSMTLIB's output that they redirect.

set_option_impl

protected IResponse set_option_impl(IExpr.IKeyword key,
 IAttributeValue value)

Override in subclasses to handle solver-specific options. Channel options are handled by set_option and never reach here. This default handles :print-success client-side (see checkPrintSuccess(org.smtlib.SMT.Configuration, org.smtlib.IExpr.IKeyword, org.smtlib.IAttributeValue)): the solver process is always left with :print-success true at the wire level (see start()/sendCommand()) -- without that, we'd get no acknowledgment at all for other commands once a script turns it off -- so it is answered entirely client-side, matching the local smtConfig.nosuccess flag, and is never itself forwarded to the solver process. A subclass that overrides set_option_impl for other reasons (e.g. to also track option values locally) needs its own checkPrintSuccess call, same as it always has -- this default is only reached by a subclass that doesn't override set_option_impl at all.

set_info

public IResponse set_info(IExpr.IKeyword key,
 IAttributeValue value)

Description copied from interface: ISolver

Annotates the problem with an info attribute (e.g. :status sat).

Specified by:

set_info in interface ISolver

Parameters:

key - the info keyword

value - the attribute value

Returns:

success, unsupported, or an SMT error response

See Also:

• ISolver.set_info(IExpr.IKeyword, IExpr.IAttributeValue)

sendChange

protected IResponse sendChange(AbstractSolver.StackChange kind,
 ICommand cmd)

Sends a command that changes the assertion stack, recording it (see recordChange)

recordChange

protected IResponse recordChange(AbstractSolver.StackChange kind,
 IResponse response)

Records the response to a command of the given kind that changes the assertion stack, and returns it. The command counts as a change only once its response is known not to be an error: a command the solver rejects changes nothing.

checkStatus

protected IResponse 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

inSatMode

protected boolean inSatMode()

Whether the most recent check command was answered sat or unknown, with the assertion stack unchanged since: SMT-LIB's sat mode (false once the whole-run time limit has ended the solver)

inUnsatMode

protected boolean inUnsatMode()

Whether the most recent check command was answered unsat, with the assertion stack unchanged since: SMT-LIB's unsat mode (false once the whole-run time limit has ended the solver)

requireNoChangeSinceCheck

protected IResponse 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

requireOptionEnabled

protected IResponse requireOptionEnabled(String commandName,
 String option)

Returns an error response if the given option has not been enabled (per get_option(IKeyword)), else null.

requireSatOrUnknown

protected IResponse requireSatOrUnknown(String commandName)

Returns an error response unless checkStatus() is sat or unknown, else null.

requireUnsat

protected IResponse requireUnsat(String commandName,
 String afterWhat)

Returns an error response unless checkStatus() is unsat, else null.

isFlatResponse

protected boolean isFlatResponse(String response)

True if the given raw response text is a flat outcome (empty/success/unsupported/an (error ...) s-expression) rather than a structured list — used by the get_assertions/get_value/get_assignment/get_unsat_core/get_unsat_assumptions defaults below to decide whether to delegate to parseResponse(String) or reparse the response as the structured list they actually expect.

get_assertions

public IResponse get_assertions()

Description copied from interface: ISolver

Returns the list of formulae in the current assertion set, in the order they were asserted. Requires :produce-assertions to be enabled; returns an error if it is not. SMT-LIB does not stipulate the order of the terms in the returned list.

Specified by:

get_assertions in interface ISolver

Returns:

a sequence of asserted terms, unsupported, or an SMT error response

See Also:

• ISolver.get_assertions()

get_proof

public IResponse get_proof()

Description copied from interface: ISolver

Returns a proof of unsatisfiability for the current assertion set. Requires :produce-proofs to be enabled; returns an error if it is not.

Specified by:

get_proof in interface ISolver

Returns:

a proof, unsupported, or an SMT error response

See Also:

• ISolver.get_proof()

proofResponse

protected IResponse proofResponse(IResponse r)

Wraps a parsed get-proof answer as an IProofResponse; anything else (an error, unsupported) is returned unchanged.

get_model

public IResponse get_model()

Description copied from interface: ISolver

Returns a satisfying model for the current assertion set. Requires :produce-models to be enabled and the last check-sat to have returned sat; returns an error if these preconditions are not met.

Specified by:

get_model in interface ISolver

Returns:

a model, unsupported, or an SMT error response

See Also:

• ISolver.get_model()

modelResponse

protected IResponse 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 ...) ...). A conforming response, whose elements are all lists, is unchanged.

unsatCoreElements

protected List<IExpr> unsatCoreElements(List<IExpr> reply)

The elements of a get-unsat-core reply that belong in the unsat core (all of them); an adapter whose solver's reply holds others filters them out

unsatAssumptionsElements

protected List<IExpr> unsatAssumptionsElements(List<IExpr> reply)

The elements of a get-unsat-assumptions reply that belong in the response (all of them); an adapter whose solver's reply holds others filters them out

get_unsat_assumptions

public IResponse get_unsat_assumptions()

Description copied from interface: ISolver

Returns the subset of check-sat-assuming assumptions that caused the result to be unsat. Requires :produce-unsat-assumptions to be enabled; returns an error if it is not.

Specified by:

get_unsat_assumptions in interface ISolver

Returns:

a list of assumption literals, unsupported, or an SMT error response

See Also:

• ISolver.get_unsat_assumptions()

get_unsat_core

public IResponse get_unsat_core()

Description copied from interface: ISolver

Returns the named formulae that form an unsatisfiable core of the current assertion set. Requires :produce-unsat-cores to be enabled; returns an error if it is not.

Specified by:

get_unsat_core in interface ISolver

Returns:

a list of formula names, unsupported, or an SMT error response

See Also:

• ISolver.get_unsat_core()

get_value

public IResponse get_value(IExpr... terms)

Description copied from interface: ISolver

Returns the values of the given expressions in the current satisfying model. Requires :produce-models to be enabled and the last check-sat to have returned sat; returns an error if these preconditions are not met.

Specified by:

get_value in interface ISolver

Parameters:

terms - expressions to evaluate

Returns:

a list of term–value pairs, unsupported, or an SMT error response

See Also:

• ISolver.get_value(IExpr...)

get_assignment

public IResponse get_assignment()

Description copied from interface: ISolver

Returns the truth-value assignments for all named Boolean formulae in the current model. Requires :produce-assignments to be enabled and the last check-sat to have returned sat; returns an error if these preconditions are not met.

Specified by:

get_assignment in interface ISolver

Returns:

a list of name–Boolean pairs, unsupported, or an SMT error response

See Also:

• ISolver.get_assignment()

get_option

public IResponse get_option(IExpr.IKeyword option)

Description copied from interface: ISolver

Returns the current value of the named option.

Specified by:

get_option in interface ISolver

Parameters:

option - the keyword naming the option

Returns:

the option value, or unsupported, or an SMT error response

See Also:

• ISolver.get_option(IExpr.IKeyword)

get_info

public IResponse get_info(IExpr.IKeyword option)

Description copied from interface: ISolver

Returns the value of the named info item.

Specified by:

get_info in interface ISolver

Parameters:

option - the info keyword

Returns:

the info value, or unsupported, or an SMT error response

See Also:

• ISolver.get_info(IExpr.IKeyword)

smt

public SMT.Configuration smt()

Description copied from interface: ISolver

Returns the configuration object with which the solver is initialized

Specified by:

smt in interface ISolver

See Also:

• ISolver.smt()

checkSatStatus

public IResponse checkSatStatus()

Description copied from interface: ISolver

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.

Specified by:

checkSatStatus in interface ISolver

See Also:

• ISolver.checkSatStatus()

declare_datatype

public IResponse declare_datatype(ICommand.Ideclare_datatype cmd)

Description copied from interface: ISolver

Declares a new datatype sort; returns success or an SMT error response

Specified by:

declare_datatype in interface ISolver

declare_datatypes

public IResponse declare_datatypes(ICommand.Ideclare_datatypes cmd)

Description copied from interface: ISolver

Declares mutually recursive datatype sorts; returns success or an SMT error response

Specified by:

declare_datatypes in interface ISolver