Package org.smtlib.solvers

Class Solver_z3_recent

java.lang.Object
org.smtlib.AbstractSolver
org.smtlib.solvers.Solver_z3_recent
All Implemented Interfaces:
ISolver
Direct Known Subclasses:
Solver_z3_4_5
public class Solver_z3_recent extends AbstractSolver implements ISolver
This class is an adapter for recent z3 versions (empirically verified against 4.8.12 and 4.10.2), on the assumption that they are (or should be) fully SMT-LIB compliant: it is a concrete, silent inheritor of AbstractSolver -- only the startup command line and start()/AbstractSolver.exit() (process lifecycle) are overridden. Empirically, none of the z3-4.3-era workarounds the old version-specific adapters needed (see the git history of the now-removed Solver_z3_4_5/4_6/4_7/4_8 classes) are needed any more: bitvector literals print in standard #b/#x form (no bv5[8]-style regex conversion needed), and errors come back as clean, well-formed (error "...") s-expressions that AbstractSolver's generic parseResponse handles without any massaging.

:print-success needs an explicit priming command on Linux specifically, same idea as Solver_z3_4_3: jSMTLIB's own protocol expects a response to every command it sends, and print-success false (the SMT-LIB-compliant default) means most commands legitimately produce none on their own. Confirmed via gdb-attaching to a hung z3 process on Linux CI that the very first real command produced no response at all -- z3 sitting in its own SMT2 scanner blocked reading stdin for more input, having silently consumed the command and moved on without acking it, which jSMTLIB has no way to distinguish from a solver that's simply slow, so it just waited forever. macOS/ Windows don't hit this and already have goldens reflecting an un-primed first response, so the priming command below is Linux-only rather than unconditional -- doing it everywhere would shift every line-numbered error message on every platform by one, not just the platform that actually needs it.

One confirmed compliance gap, not caused by this adapter: z3 defaults :produce-models to true rather than the spec's false, with no known CLI flag or startup option to change that -- scripts checking that default need a z3-specific golden reflecting it.

  • Field Details

    • cmds

      protected String[] cmds
      The command-line arguments for launching the solver.

    • cmds_win

      protected String[] cmds_win

    • cmds_mac

      protected String[] cmds_mac

    • cmds_unix

      protected String[] cmds_unix

    • needsPrintSuccessPriming

      protected final boolean needsPrintSuccessPriming
      True only on the platform where the print-success priming command below is needed (see the class javadoc)

  • Constructor Details

    • Solver_z3_recent

      public Solver_z3_recent(SMT.Configuration smtConfig, String executable)
      Creates an instance of the solver

    • Solver_z3_recent

      public Solver_z3_recent(SMT.Configuration smtConfig, String[] command)
      Launches the given command as is (a .command property, #147), without adding the flags the executable form adds

  • Method Details

    • 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

    • 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:

    • get_info

      public IResponse 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". jSMTLIB sets no other limit that cancels a query, so when the per-query limit is set, "canceled" is reported as "timeout" (OpenJML#1022).
      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:

    • isTimeLimitResponse

      protected boolean isTimeLimitResponse(String rawResponse)
      z3 answers 'timeout' (instead of a result) when its whole-run limit, -T:, ends it, and then exits (checked with z3 4.16.0 and 5.1.0)
      Overrides:
      isTimeLimitResponse in class AbstractSolver

    • answeredAfter

      protected Set<AbstractSolver.StackChange> answeredAfter()
      The kinds of command after which this z3 still answers the get- commands about the last check (probed 2026-10-29: z3 4.6 to 5.1 after every declare and define; 4.8 and later also after reset-assertions, which 4.6 and 4.7 report themselves). After assert, push or pop z3 reports the error itself.

    • get_assignment

      public IResponse get_assignment()
      z3 answers get-assignment with :produce-assignments off, and in assert mode after a check
      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:

    • get_model

      public IResponse get_model()
      z3 answers get-model in assert mode after a check
      Specified by:
      get_model in interface ISolver
      Overrides:
      get_model in class AbstractSolver
      Returns:
      a model, unsupported, or an SMT error response
      See Also:

    • get_value

      public IResponse get_value(IExpr... terms)
      z3 answers get-value in assert mode after a check
      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:

    • get_proof

      public IResponse get_proof()
      z3 answers get-proof in assert mode after a check
      Specified by:
      get_proof in interface ISolver
      Overrides:
      get_proof in class AbstractSolver
      Returns:
      a proof, unsupported, or an SMT error response
      See Also:

    • 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:

    • 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
      Overrides:
      check_sat_assuming in class AbstractSolver
      Returns:
      sat, unsat, unknown, or an SMT error response
      See Also:

    • 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:

    • unsatCoreElements

      protected List<IExpr> unsatCoreElements(List<IExpr> reply)
      Drops the assumptions z3 adds to the unsat core (see Assumptions)
      Overrides:
      unsatCoreElements in class AbstractSolver

    • unsatAssumptionsElements

      protected List<IExpr> unsatAssumptionsElements(List<IExpr> reply)
      Drops the labels z3 adds to the unsat assumptions (see Assumptions)
      Overrides:
      unsatAssumptionsElements in class AbstractSolver

    • get_unsat_core

      public IResponse get_unsat_core()
      z3 answers get-unsat-core in assert mode after a check
      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:

    • get_unsat_assumptions

      public IResponse get_unsat_assumptions()
      z3 answers get-unsat-assumptions in assert mode after a check
      Specified by:
      get_unsat_assumptions in interface ISolver
      Overrides:
      get_unsat_assumptions in class AbstractSolver
      Returns:
      a list of assumption literals, unsupported, or an SMT error response
      See Also: