Package org.smtlib.solvers

Class Solver_cvc5

java.lang.Object
org.smtlib.AbstractSolver
org.smtlib.solvers.Solver_cvc5
All Implemented Interfaces:
ISolver
public class Solver_cvc5 extends AbstractSolver implements ISolver
This class is an adapter for cvc5, on the assumption that it is (or should be) a fully SMT-LIB compliant solver: it is a concrete, silent inheritor of AbstractSolver — only the startup command line (cvc5 needs --incremental to accept push/pop at all, and --quiet to suppress informational stderr chatter that would otherwise fool SolverProcess's stdout/stderr-preference heuristic) and start() (process lifecycle) are overridden. Empirically (against cvc5 1.3.2), none of the CVC4-era workarounds a previous version of this class used to need still apply: cvc5 handles Bool-sorted quantifiers natively (no translate() workaround needed), get-value/ get-option return clean standard-shaped responses (no Response.Seq workaround needed), and get-info/get-option round-trip through AbstractSolver's generic parseResponse without issue -- with one exception, get_option(org.smtlib.IExpr.IKeyword), described below.

One confirmed, patchable compliance gap: cvc5 answers (get-option :regular-output-channel)/(get-option :diagnostic-output-channel) with a bare, unquoted symbol (stdout/stderr) rather than the SMT-LIB string literal ("stdout"/"stderr") these two options are specified to hold -- confirmed against a real cvc5 1.3.2 process. get_option(org.smtlib.IExpr.IKeyword) wraps a bare-symbol answer for either option into a proper string literal with the same text.

One confirmed, non-workaroundable compliance gap: cvc5 self-reports (get-info :error-behavior) as immediate-exit (not continued-execution) and its process actually exits after a top-level parse error. Neither (set-option :error-behavior continued-execution) (rejected as unsupported) nor (set-info :error-behavior continued-execution) (silently accepted but with no actual effect — get-info still reports immediate-exit and the process still dies) can change this, so there's no way to ask for the other mode. selfReportsImmediateExit() tells AbstractSolver.sendCommand(ICommand, boolean) about this, so once cvc5 reports one real error, jSMTLIB pauses briefly before sending anything further, giving the process time to actually finish exiting (if it is going to) before the next command's liveness check runs.

  • Field Details

    • cmds

      protected String[] cmds
      The command-line arguments for launching the solver. --print-success turns on success replies from the very first command onward (confirmed: --interactive does NOT imply it by itself -- without --print-success, the first command gets no reply at all), so no priming (set-option :print-success true) is needed in start().

    • cmds_win

      protected String[] cmds_win

    • cmds_mac

      protected String[] cmds_mac

    • cmds_unix

      protected String[] cmds_unix

  • Constructor Details

    • Solver_cvc5

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

    • Solver_cvc5

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

    • 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

    • nextSolverLine

      protected int nextSolverLine()
      Description copied from class: AbstractSolver
      The solver line, as the solver numbers lines in its messages, on which the next text sent starts; overridden for a solver that does not number the lines of its whole input
      Overrides:
      nextSolverLine in class AbstractSolver

    • isTimeLimitResponse

      protected boolean isTimeLimitResponse(String rawResponse)
      cvc5 reports 'cvc5 interrupted by timeout.' on stderr, with no answer, when its whole-run limit, --tlimit, ends it, and then aborts (checked with cvc5 1.3.2)
      Overrides:
      isTimeLimitResponse in class AbstractSolver

    • errorStopsSolver

      protected boolean errorStopsSolver(IResponse error)
      cvc5 carries on after most errors (e.g. sort errors), but after a parse error it no longer processes input, and when run interactively it does not always exit either -- so it is stopped (see AbstractSolver.checkImmediateExit).
      Overrides:
      errorStopsSolver 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_option

      public IResponse get_option(IExpr.IKeyword option)
      See the class Javadoc: wraps a bare-symbol answer for a string-typed option (Utils.stringOptions -- currently just :regular-output-channel and :diagnostic-output-channel) into a proper SMT-LIB string literal with the same text, working around cvc5 answering those two with an unquoted symbol instead.
      Specified by:
      get_option in interface ISolver
      Overrides:
      get_option in class AbstractSolver
      Parameters:
      option - the keyword naming the option
      Returns:
      the option value, or unsupported, or an SMT error response
      See Also:

    • set_option_impl

      protected IResponse set_option_impl(IExpr.IKeyword key, IAttributeValue value)
      Description copied from class: AbstractSolver
      Override in subclasses to handle solver-specific options. Channel options are handled by set_option and never reach here. This default handles :print-success client-side (see AbstractSolver.checkPrintSuccess(org.smtlib.SMT.Configuration, org.smtlib.IExpr.IKeyword, org.smtlib.IAttributeValue)): the solver process is always left with :print-success true at the wire level (see start()/sendCommand()) -- without that, we'd get no acknowledgment at all for other commands once a script turns it off -- so it is answered entirely client-side, matching the local smtConfig.nosuccess flag, and is never itself forwarded to the solver process. A subclass that overrides set_option_impl for other reasons (e.g. to also track option values locally) needs its own checkPrintSuccess call, same as it always has -- this default is only reached by a subclass that doesn't override set_option_impl at all.
      Overrides:
      set_option_impl 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:

    • get_assertions

      public IResponse get_assertions()
      cvc5 answers get-assertions with :produce-assertions off
      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:

    • get_assignment

      public IResponse get_assignment()
      cvc5 answers get-assignment with :produce-assignments off (if :produce-models is on), 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()
      cvc5 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)
      cvc5 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()
      cvc5 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:

    • get_unsat_core

      public IResponse get_unsat_core()
      cvc5 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()
      cvc5 aborts on 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: