Package org.smtlib.solvers

Class Solver_z3_4_5

java.lang.Object

org.smtlib.AbstractSolver

org.smtlib.solvers.Solver_z3_recent

org.smtlib.solvers.Solver_z3_4_5

All Implemented Interfaces:

ISolver

public class Solver_z3_4_5
extends Solver_z3_recent

z3 4.5.0: as recent z3, except that it writes echo's text unquoted even with SMTLIB2_COMPLIANT (4.6 and later quote it), so where it ends cannot be found (#136), the response to echo is its argument; and it rejects every check-sat-assuming (see translate)

Nested Class Summary

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 inherited from class org.smtlib.solvers.Solver_z3_recent

cmds, cmds_mac, cmds_unix, cmds_win, needsPrintSuccessPriming

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_5(SMT.Configuration smtConfig, String executable)
Solver_z3_4_5(SMT.Configuration smtConfig, String[] command)

Method Summary

Modifier and Type	Method	Description
protected Set<AbstractSolver.StackChange>	answeredAfter()	z3 4.5 reports the get- commands after a declare or define itself, except after declare-datatype(s) (probed 2026-10-29)
IResponse	echo(IExpr.IStringLiteral arg)	Echoes the argument string back to the output channel.
protected String	translate(INode node)	z3 4.5 rejects every check-sat-assuming ("invalid check-sat-assuming command, '(', expected", a parser bug), so it is sent as z3's legacy (check-sat a1 ...

Methods inherited from class org.smtlib.solvers.Solver_z3_recent

check_sat, check_sat_assuming, get_assignment, get_info, get_model, get_proof, get_unsat_assumptions, get_unsat_core, get_value, isTimeLimitResponse, lineNumberPatterns, reset, start, unsatAssumptionsElements, unsatCoreElements

Methods inherited from class org.smtlib.AbstractSolver

assertExpr, checkImmediateExit, checkPrintSuccess, checkSatStatus, checkShape, checkStatus, comment, correctResponse, declare_const, declare_datatype, declare_datatypes, declare_fun, declare_sort, declare_sort_parameter, define_const, define_fun, define_fun_rec, define_funs_rec, define_sort, earlierSourceLine, errorStopsSolver, execute, executePipelined, exit, exitedResponse, finishPipelined, forceExit, get_assertions, get_option, hasPending, inSatMode, interrupt, inUnsatMode, isFlatResponse, logSolverDiagnostics, modelResponse, nextSolverLine, normalizeForTesting, outOfStep, parseResponse, pipelines, pop, proofResponse, push, readPipelined, recordChange, reportsEarlierLines, reportSeedIgnored, requireNoChangeSinceCheck, requireOptionEnabled, requireSatOrUnknown, requireUnsat, reset_assertions, responseEnd, selfReportsImmediateExit, sendChange, sendCommand, sendExitCommand, sendFailure, sendFailure, sendPipelined, sendScriptText, sendSeed, set_info, set_logic, set_option, set_option_impl, setSourceLine, shapeOf, smt, solverName, solverPrintsSuccess, successOrEmpty, timeLimitResponse, timeLimitResponseAfterExit, 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

assertExpr, checkSatStatus, comment, declare_const, declare_datatype, declare_datatypes, declare_fun, declare_sort, declare_sort_parameter, define_const, define_fun, define_fun_rec, define_funs_rec, define_sort, execute, exit, forceExit, get_assertions, get_option, pop, push, reset_assertions, set_info, set_logic, set_option, setSourceLine, smt, solverName

Constructor Details

Solver_z3_4_5

public Solver_z3_4_5(SMT.Configuration smtConfig,
 String executable)

Solver_z3_4_5

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

Method Details

answeredAfter

protected Set<AbstractSolver.StackChange> answeredAfter()

z3 4.5 reports the get- commands after a declare or define itself, except after declare-datatype(s) (probed 2026-10-29)

Overrides:

answeredAfter in class Solver_z3_recent

translate

protected String translate(INode node)
                    throws IVisitor.VisitorException

z3 4.5 rejects every check-sat-assuming ("invalid check-sat-assuming command, '(', expected", a parser bug), so it is sent as z3's legacy (check-sat a1 ... an), which checks under the same assumptions, padded with spaces so z3's error columns match the check-sat-assuming text (see Solver_z3_recent.legacyCheckSat). Its unsat core then includes the assumptions, which Solver_z3_recent drops.

Overrides:

translate in class AbstractSolver

Throws:

IVisitor.VisitorException

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

Overrides:

echo in class AbstractSolver

Returns:

the argument as an IResponse