Package org.smtlib.solvers

Class Solver_z3_4_3_2

java.lang.Object
org.smtlib.AbstractSolver
org.smtlib.solvers.Solver_z3_4_3
org.smtlib.solvers.Solver_z3_4_3_2
All Implemented Interfaces:
ISolver
public class Solver_z3_4_3_2 extends Solver_z3_4_3
This is a special handler for Z3 4.3.2, as opposed to other revisions of Z3 4.3.
See Also:

  • Constructor Details

    • Solver_z3_4_3_2

      public Solver_z3_4_3_2(SMT.Configuration smtConfig, String executable)

    • Solver_z3_4_3_2

      public Solver_z3_4_3_2(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

    • name

      protected String name()
      Description copied from class: Solver_z3_4_3
      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.
      Overrides:
      name in class Solver_z3_4_3

    • set_option_impl

      protected IResponse 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. SMT-LIB answers unsupported there, as z3 4.3.1 does. The error is parsable, but the z3-4.3 adapters aim to be as close to conforming as they can, so it is reported as unsupported. Only errors matching (?s)line \d+ column \d+: unknown parameter .* are converted; any other set-option error (a bad value, for example) passes through.
      Overrides:
      set_option_impl in class Solver_z3_4_3

    • sendScriptText

      protected String sendScriptText(boolean listen, String... text) throws IOException
      Corrects a non-conformance of z3 4.3.2: run with smtlib2_compliant=true, as this adapter runs it, a check-sat of a problem with quantifiers, before any push, makes z3 parse its built-in pattern database (111 commands) with print-success on, so a "success" line per command precedes the result. Those lines are read and dropped here. They all come before the result, so none is left for a later command. (Not passing smtlib2_compliant=true would avoid them, but changes many other responses away from SMT-LIB.)
      Overrides:
      sendScriptText in class AbstractSolver
      Throws:
      IOException