Package org.smtlib.solvers

Class Solver_z3_4_3

java.lang.Object

org.smtlib.AbstractSolver

org.smtlib.solvers.Solver_z3_4_3

All Implemented Interfaces:

ISolver

Direct Known Subclasses:

Solver_z3_4_3_2

public class Solver_z3_4_3
extends AbstractSolver
implements ISolver

This class is an adapter that takes the SMT-LIB ASTs and translates them into Z3 commands

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
class	Solver_z3_4_3.Translator

Nested classes/interfaces inherited from class org.smtlib.AbstractSolver

AbstractSolver.Pending, AbstractSolver.Shape, AbstractSolver.StackChange

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

ISolver.CreationException

Field Summary

Fields

Modifier and Type	Field	Description
protected String[]	cmds	The command-line arguments for launching the Z3 solver
protected String[]	cmds_mac
protected String[]	cmds_unix
protected String[]	cmds_win
protected boolean	logicSet	Set to true once a set-logic command has been executed.
protected Parser	responseParser	The parser that parses responses from the solver

Fields inherited from class org.smtlib.AbstractSolver

checkSatStatus, END_WAIT_MILLIS, endedByTimeLimit, isMac, isWindows, linesOffset, options, printSuccess, printSuccessResponse, smtConfig, SOLVER_EXITED, solverProcess

Constructor Summary

Constructors

Constructor	Description
Solver_z3_4_3(SMT.Configuration smtConfig, String executable)	Creates an instance of the Z3 solver
Solver_z3_4_3(SMT.Configuration smtConfig, String[] command)	Creates an instance of the Z3 solver

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)	z3 4.3 answers unsupported for check-sat-assuming, so it is sent as z3's legacy (check-sat a1 ...
IResponse	declare_const(ICommand.Ideclare_const cmd)	Declares a new uninterpreted constant; 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	define_fun(ICommand.Idefine_fun cmd)	Defines a named function or constant; 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
IResponse	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	exit()	Terminates the solver; no further commands are permitted.
void	forceExit()	Terminates the solver forcibly without sending commands (e.g.
IResponse	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	get_assignment()	z3 4.3 answers get-assignment (with ()) when :produce-assignments is not enabled, which SMT-LIB makes an error
IResponse	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	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	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	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	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	get_value(IExpr... terms)	See get_model: z3 4.3 defaults :produce-models to true
protected boolean	isTimeLimitResponse(String rawResponse)	z3 answers 'timeout' (instead of a result) when its whole-run limit, -T, ends it, and then exits
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 String	name()	The solver's display name for diagnostic logging.
protected IResponse	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).
boolean	pipelines(ICommand cmd)	Never pipelined: this adapter sends and corrects commands by its own means
IResponse	pop(int number)	Removes the given number of assertion-stack frames from the solver state.
IResponse	push(int number)	Adds the given number of empty assertion-stack frames to the solver state.
IResponse	reset()	Resets the solver to the initial state, clearing all assertions, declarations, and options.
IResponse	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	sendCommand(String cmd)
IResponse	sendCommand(ICommand cmd)	Translates the given command and sends it to the solver process, returning the parsed response.
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.
protected IResponse	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	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.
protected String	translate(INode sexpr)	Translates an S-expression into Z3 syntax
protected List<IExpr>	unsatCoreElements(List<IExpr> reply)	Drops the assumptions z3 4.3 adds to the unsat core after check-sat-assuming

Methods inherited from class org.smtlib.AbstractSolver

checkImmediateExit, checkPrintSuccess, checkSatStatus, checkShape, checkStatus, comment, correctResponse, declare_datatype, declare_datatypes, declare_sort_parameter, define_const, define_fun_rec, define_funs_rec, earlierSourceLine, errorStopsSolver, execute, executePipelined, exitedResponse, finishPipelined, get_unsat_assumptions, hasPending, inSatMode, interrupt, inUnsatMode, isFlatResponse, logSolverDiagnostics, modelResponse, nextSolverLine, normalizeForTesting, outOfStep, proofResponse, readPipelined, recordChange, reportsEarlierLines, reportSeedIgnored, requireNoChangeSinceCheck, requireOptionEnabled, requireSatOrUnknown, requireUnsat, responseEnd, selfReportsImmediateExit, sendChange, sendExitCommand, sendFailure, sendFailure, sendPipelined, sendScriptText, sendSeed, set_info, set_option, setSourceLine, shapeOf, smt, solverName, solverPrintsSuccess, successOrEmpty, timeLimitResponse, timeLimitResponseAfterExit, unsatAssumptionsElements, withSourceLines

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.smtlib.ISolver

checkSatStatus, comment, declare_datatype, declare_datatypes, declare_sort_parameter, define_const, define_fun_rec, define_funs_rec, execute, get_unsat_assumptions, set_info, set_option, setSourceLine, smt, solverName

Field Details

cmds

protected String[] cmds

The command-line arguments for launching the Z3 solver

cmds_win

protected String[] cmds_win

cmds_mac

protected String[] cmds_mac

cmds_unix

protected String[] cmds_unix

responseParser

protected Parser responseParser

The parser that parses responses from the solver

logicSet

protected boolean logicSet

Set to true once a set-logic command has been executed. z3 4.3 accepts declarations, definitions, assert, push, pop and check-sat before set-logic, which SMT-LIB forbids, so those commands check this flag and report the error themselves.

Constructor Details

Solver_z3_4_3

public Solver_z3_4_3(SMT.Configuration smtConfig,
 String executable)

Creates an instance of the Z3 solver

Solver_z3_4_3

public Solver_z3_4_3(SMT.Configuration smtConfig,
 String[] command)

Creates an instance of the Z3 solver

Method Details

name

protected String name()

The solver's display name for diagnostic logging. A real, overridable method rather than a field -- a field here would be hidden, not overridden, by a subclass's own same-named field (Java fields aren't polymorphic), silently binding start()'s reference to this class's value regardless of which subclass is actually running. See issue #51.

lineNumberPatterns

protected List<Pattern> lineNumberPatterns()

Description copied from class: AbstractSolver

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

Overrides:

lineNumberPatterns in class AbstractSolver

isTimeLimitResponse

protected boolean isTimeLimitResponse(String rawResponse)

z3 answers 'timeout' (instead of a result) when its whole-run limit, -T, ends it, and then exits

Overrides:

isTimeLimitResponse in class AbstractSolver

pipelines

public boolean pipelines(ICommand cmd)

Never pipelined: this adapter sends and corrects commands by its own means

Overrides:

pipelines in class AbstractSolver

sendCommand

public IResponse sendCommand(ICommand cmd)

Description copied from class: AbstractSolver

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.

Overrides:

sendCommand in class AbstractSolver

sendCommand

public IResponse sendCommand(String cmd)

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

Overrides:

start in class AbstractSolver

Returns:

success or an SMT error response

See Also:

• ISolver.start()

exit

public IResponse exit()

Description copied from interface: ISolver

Terminates the solver; no further commands are permitted.

Specified by:

exit in interface ISolver

Overrides:

exit in class AbstractSolver

Returns:

success or an SMT error response

See Also:

• ISolver.exit()

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

Overrides:

forceExit in class AbstractSolver

translate

protected String translate(INode sexpr)
                    throws IVisitor.VisitorException

Translates an S-expression into Z3 syntax

Overrides:

translate in class AbstractSolver

Throws:

IVisitor.VisitorException

parseResponse

protected IResponse 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). A command sent directly after that finds the process gone and gets an error; sendCommand returns the timeout response.

Overrides:

parseResponse in class AbstractSolver

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

Overrides:

assertExpr in class AbstractSolver

Returns:

success or an SMT error response

See Also:

• ISolver.assertExpr(IExpr)

get_assertions

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

Specified by:

get_assertions in interface ISolver

Overrides:

get_assertions in class AbstractSolver

Returns:

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

See Also:

• ISolver.get_assertions()

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

Overrides:

check_sat in class AbstractSolver

Returns:

sat, unsat, unknown, or an SMT error response

See Also:

• ISolver.check_sat()

check_sat_assuming

public IResponse 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 ... an), which checks under the same assumptions; it is padded with spaces so z3's error columns match the check-sat-assuming text (see translate and Solver_z3_recent.legacyCheckSat). Its unsat core then includes the assumptions, which unsatCoreElements drops. Like check-sat, it is accepted before set-logic, which SMT-LIB forbids, so that is reported here.

Specified by:

check_sat_assuming in interface ISolver

Overrides:

check_sat_assuming in class AbstractSolver

Returns:

sat, unsat, unknown, or an SMT error response

See Also:

• ISolver.check_sat_assuming(IExpr...)

unsatCoreElements

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

Drops the assumptions z3 4.3 adds to the unsat core after check-sat-assuming

Overrides:

unsatCoreElements in class AbstractSolver

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

Overrides:

reset in class AbstractSolver

Returns:

success or an SMT error response

See Also:

• ISolver.reset()

reset_assertions

public IResponse 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. That's the correct, honest answer for a solver that genuinely can't do this, so there is nothing for the adapter to improve on here: a from-jSMTLIB pop-to-base simulation was tried and reverted -- it silently claimed success while only partially honoring the contract (it can only clear pushed-frame state, not declarations, and per issue #53 discussion, non-global declarations are also supposed to be cleared by reset-assertions, which this adapter has no way to do without locally tracking every declaration), and it desynced the linesOffset bookkeeping used to translate Z3's own reported error positions back to the script's real line numbers, corrupting later error messages. See issue #53.

Specified by:

reset_assertions in interface ISolver

Overrides:

reset_assertions in class AbstractSolver

Returns:

success or an SMT error response

See Also:

• ISolver.reset_assertions()

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

Overrides:

pop in class AbstractSolver

Parameters:

number - non-negative number of frames to pop

Returns:

success or an SMT error response

See Also:

• ISolver.pop(int)

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

Overrides:

push in class AbstractSolver

Parameters:

number - non-negative number of frames to push

Returns:

success or an SMT error response

See Also:

• ISolver.push(int)

set_logic

public IResponse set_logic(String logicName,
 IPos pos)

Description copied from class: AbstractSolver

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

Overrides:

set_logic in class AbstractSolver

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)

set_option_impl

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

Overrides:

set_option_impl in class AbstractSolver

get_option

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

Specified by:

get_option in interface ISolver

Overrides:

get_option in class AbstractSolver

Parameters:

key - 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 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

Specified by:

get_info in interface ISolver

Overrides:

get_info in class AbstractSolver

Parameters:

key - the info keyword

Returns:

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

See Also:

• ISolver.get_info(IExpr.IKeyword)

echo

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

Specified by:

echo in interface ISolver

Overrides:

echo in class AbstractSolver

Returns:

the argument as an IResponse

get_model

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

Specified by:

get_model in interface ISolver

Overrides:

get_model in class AbstractSolver

Returns:

a model, unsupported, or an SMT error response

See Also:

• ISolver.get_model()

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

Overrides:

declare_const in class AbstractSolver

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

Overrides:

declare_fun in class AbstractSolver

See Also:

• ISolver.declare_fun(ICommand.Ideclare_fun)

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

Overrides:

define_fun in class AbstractSolver

See Also:

• ISolver.define_fun(ICommand.Idefine_fun)

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

Overrides:

declare_sort in class AbstractSolver

See Also:

• ISolver.declare_sort(ICommand.Ideclare_sort)

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

Overrides:

define_sort in class AbstractSolver

See Also:

• ISolver.define_sort(ICommand.Idefine_sort)

get_proof

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

Specified by:

get_proof in interface ISolver

Overrides:

get_proof in class AbstractSolver

Returns:

a proof, unsupported, or an SMT error response

See Also:

• ISolver.get_proof()

get_unsat_core

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

Specified by:

get_unsat_core in interface ISolver

Overrides:

get_unsat_core in class AbstractSolver

Returns:

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

See Also:

• ISolver.get_unsat_core()

get_assignment

public IResponse get_assignment()

z3 4.3 answers get-assignment (with ()) when :produce-assignments is not enabled, which SMT-LIB makes an error

Specified by:

get_assignment in interface ISolver

Overrides:

get_assignment in class AbstractSolver

Returns:

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

See Also:

• ISolver.get_assignment()

get_value

public IResponse get_value(IExpr... terms)

See get_model: z3 4.3 defaults :produce-models to true

Specified by:

get_value in interface ISolver

Overrides:

get_value in class AbstractSolver

Parameters:

terms - expressions to evaluate

Returns:

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

See Also:

• ISolver.get_value(IExpr...)