Package org.smtlib.solvers

Class Solver_bitwuzla

java.lang.Object
org.smtlib.AbstractSolver
org.smtlib.solvers.Solver_bitwuzla
All Implemented Interfaces:
ISolver
public class Solver_bitwuzla extends AbstractSolver implements ISolver
This class is an adapter for Bitwuzla (bit-vectors, floating-point, arrays and uninterpreted functions -- no arithmetic logics, no datatypes). It is a concrete, silent inheritor of AbstractSolver apart from a handful of real, empirically confirmed (against 0.9.1) protocol gaps:

1) Bitwuzla has no get-info, get-option, get-assertions, get-assignment or get-proof at all -- each is rejected with [error] <stdin>:L:C: unsupported command '...' and, critically, that rejection KILLS the process (see point 2), so these are answered entirely client-side and never forwarded. get_option(org.smtlib.IExpr.IKeyword) therefore tracks values itself (via the inherited options map, falling back to smtConfig.utils.defaults) rather than relying on AbstractSolver's default of asking the solver.

2) Unlike cvc5/yices2 (which die only after some errors), Bitwuzla's process exits immediately after essentially ANY error -- an unsupported command, an unsupported logic, a sort mismatch in an assertion, etc. -- not just protocol violations. selfReportsImmediateExit() is therefore true, and :error-behavior is reported (via the hardcoded get_info(org.smtlib.IExpr.IKeyword)) as immediate-exit, which is simply the truth for this solver, not a workaround.

3) Bitwuzla's own error text for a genuine semantic error (e.g. [error] <stdin>:3:14: expected terms of same sort ...) is not SMT-LIB (error "...") syntax -- the leading [ is not valid s-expression syntax at all, and feeding it to the standard parser doesn't just fail to parse cleanly, it throws a raw ClassCastException out of the lexer (a LexError token reaching code that assumes an IError) instead of the IParser.ParserException that AbstractSolver.parseResponse(java.lang.String) already knows how to turn into a clean error response. parseResponse(java.lang.String) widens that catch locally so a non-conforming response produces an ordinary error IResponse instead of crashing the whole run.

4) With its :produce-* option on, Bitwuzla writes nothing at all, or the start of a list followed by an error on standard error, for get-model, get-value, get-unsat-core and get-unsat-assumptions when it has no answer (e.g. get-value after unknown, or get-unsat-core after an assert that followed unsat); it writes nothing or a fragment for get-unsat-assumptions whenever that option is off. The adapter answers those cases with an error itself, tracking Bitwuzla's own state (see lastCheck).

  • Field Details

    • cmds

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

  • Constructor Details

    • Solver_bitwuzla

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

    • Solver_bitwuzla

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

    • selfReportsImmediateExit

      protected boolean selfReportsImmediateExit()
      Description copied from class: AbstractSolver
      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 AbstractSolver.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.
      Overrides:
      selfReportsImmediateExit 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:

    • parseResponse

      protected IResponse parseResponse(String response)
      Description copied from class: AbstractSolver
      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.
      Overrides:
      parseResponse in class AbstractSolver

    • isTimeLimitResponse

      protected boolean isTimeLimitResponse(String rawResponse)
      When its whole-run limit (--time-limit) ends it, Bitwuzla writes unknown -- as the answer to a running check-sat, or unprompted while idle -- and exits with code 0 (checked with 0.9.1). An unknown for any other reason (e.g. the per-query limit) leaves it running, so an unknown is the whole-run limit only if the process then exits.
      Overrides:
      isTimeLimitResponse in class AbstractSolver

    • isFlatResponse

      protected boolean isFlatResponse(String response)
      Bitwuzla writes its errors as "[error] ..." lines (class comment point 3), so for the get- commands that parse a list reply such a line goes to parseResponse(java.lang.String), not the list parser.
      Overrides:
      isFlatResponse in class AbstractSolver

    • 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

    • reportsEarlierLines

      protected boolean reportsEarlierLines()
      Description copied from class: AbstractSolver
      Whether the solver's messages name lines of earlier commands (see AbstractSolver.earlierSourceLine(int))
      Overrides:
      reportsEarlierLines in class AbstractSolver

    • set_option_impl

      protected IResponse set_option_impl(IExpr.IKeyword key, IAttributeValue value)
      Sent to bitwuzla, and also kept here for get_option, which bitwuzla does not support
      Overrides:
      set_option_impl in class AbstractSolver

    • get_option

      public IResponse get_option(IExpr.IKeyword key)
      Answered entirely client-side (never forwarded -- see class comment point 1): from whatever this run has set via set_option_impl(org.smtlib.IExpr.IKeyword, org.smtlib.IAttributeValue), falling back to the standard SMT-LIB default for any option never set, and "unsupported" for anything not a recognized standard option at all (matching what a compliant solver would say about an option it doesn't have).
      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:

    • get_info

      public IResponse get_info(IExpr.IKeyword key)
      Answered entirely client-side (never forwarded -- see class comment point 1). :version/:authors are fixed to the 0.9.1 build this adapter was written and tested against; if jsmtlib.properties is ever pointed at a different Bitwuzla build, update these to match.
      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:

    • get_proof

      public IResponse get_proof()
      Bitwuzla rejects get-proof as an unsupported command and exits (class comment point 1); a conforming solver without proofs answers unsupported.
      Specified by:
      get_proof in interface ISolver
      Overrides:
      get_proof in class AbstractSolver
      Returns:
      a proof, unsupported, or an SMT error response
      See Also:

    • get_assignment

      public IResponse get_assignment()
      See get_proof(): Bitwuzla rejects get-assignment the same way.
      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_assertions

      public IResponse get_assertions()
      See get_proof(): Bitwuzla rejects get-assertions the same way.
      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:

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

    • declare_datatype

      public IResponse declare_datatype(ICommand.Ideclare_datatype cmd)
      Not sent: Bitwuzla exits on it (see above)
      Specified by:
      declare_datatype in interface ISolver
      Overrides:
      declare_datatype in class AbstractSolver

    • declare_datatypes

      public IResponse declare_datatypes(ICommand.Ideclare_datatypes cmd)
      Not sent: Bitwuzla exits on it (see above)
      Specified by:
      declare_datatypes in interface ISolver
      Overrides:
      declare_datatypes in class AbstractSolver

    • define_fun_rec

      public IResponse define_fun_rec(ICommand.Idefine_fun_rec cmd)
      Not sent: Bitwuzla exits on it (see above)
      Specified by:
      define_fun_rec in interface ISolver
      Overrides:
      define_fun_rec in class AbstractSolver
      See Also:

    • define_funs_rec

      public IResponse define_funs_rec(ICommand.Idefine_funs_rec cmd)
      Not sent: Bitwuzla exits on it (see above)
      Specified by:
      define_funs_rec in interface ISolver
      Overrides:
      define_funs_rec in class AbstractSolver
      See Also:

    • declare_sort_parameter

      public IResponse declare_sort_parameter(ICommand.Ideclare_sort_parameter cmd)
      Not sent: Bitwuzla exits on it (see above)
      Specified by:
      declare_sort_parameter in interface ISolver
      Overrides:
      declare_sort_parameter in class AbstractSolver
      See Also:

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

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

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

    • 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
      Overrides:
      reset_assertions in class AbstractSolver
      Returns:
      success or an SMT error response
      See Also:

    • reset

      public IResponse reset()
      Bitwuzla's reset restores its option defaults, so the values get_option answers from are dropped too (except the output channels, which are jSMTLIB's own and stay redirected).
      Specified by:
      reset in interface ISolver
      Overrides:
      reset in class AbstractSolver
      Returns:
      success or an SMT error response
      See Also:

    • set_logic

      public IResponse set_logic(String logicName, IPos pos)
      Bitwuzla (0.9.1) accepts a second set-logic, which SMT-LIB forbids outside start mode, so that is reported here (--relax allows it). After one it accepts, it still answers the get- commands about its last check, so that check is dropped here, as for reset.
      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:

    • get_model

      public IResponse get_model()
      With :produce-models on, Bitwuzla writes nothing for get-model unless its last check returned sat (and crashes if a reset came since); after an assert, push, pop or reset-assertions, or with the option set after the check, it writes an ordinary error. Bitwuzla also answers it in assert mode, after a declare or define following the 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)
      With :produce-models on, Bitwuzla writes nothing for get-value unless its last check returned sat, and a fragment and an error if an assert, push, pop or reset-assertions came since or the option was set after the check. Bitwuzla also answers it in assert mode, after a declare or define following the 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_unsat_core

      public IResponse get_unsat_core()
      With :produce-unsat-cores on, Bitwuzla writes nothing for get-unsat-core unless its last check returned unsat, and a fragment and an error if an assert, push, pop, reset-assertions or reset came since or the option was set after the check. Bitwuzla also answers it in assert mode, after a declare or define following the 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()
      Bitwuzla writes nothing for get-unsat-assumptions unless its last check returned unsat; then it writes a fragment and an error if the option is off or was set after the check, or an assert, push, pop, reset-assertions or reset came since. Bitwuzla also answers it in assert mode, after a declare or define following the 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: