Package org.smtlib

Interface ISolver

All Known Implementing Classes:
AbstractSolver, Solver_altergo, Solver_bitwuzla, Solver_cvc5, Solver_simplify, Solver_smt, Solver_smtinterpol, Solver_test, Solver_yices2, Solver_yices2_2_6, Solver_z3_4_3, Solver_z3_4_3_2, Solver_z3_4_5, Solver_z3_recent
public interface ISolver
This is the interface to be implemented by any solver adapter; there is a method for each SMT-LIB command.

SMT.startSolver(org.smtlib.SMT.Configuration, java.lang.String, java.lang.String), which is how every adapter actually gets instantiated, constructs one via reflection rather than a fixed factory method or hardcoded switch -- a contract not stated anywhere near this interface or AbstractSolver until now. Concretely, it looks up (on whatever concrete class jsmtlib.properties names for the requested solver, via its .adapter entry) a public constructor with exactly one of these two signatures:

  • (SMT.Configuration, String) -- used when the properties entry gives a single .exec value (a bare executable path/name); that resolved executable is passed as the String.
  • (SMT.Configuration, String[]) -- used when the properties entry gives a .command array instead (a full argv, e.g. for a launcher like "java,-jar,%exec%,-q"); the resolved command array is passed as-is.
A new adapter class must expose whichever of the two matches how it's configured (or both, if it should support either) -- reflection fails with a bare NoSuchMethodException at solver-startup time otherwise, not at compile time.

  • Method Details

    • smt

      SMT.Configuration smt()
      Returns the configuration object with which the solver is initialized

    • checkSatStatus

      IResponse checkSatStatus()
      Returns the result of the most recent check-sat or check-sat-assuming, or null if none has been issued since the last push/pop/assert/declare/define.

    • solverName

      String solverName()
      A public, user-readable name for the solver adapter class

    • start

      IResponse start()
      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.
      Returns:
      success or an SMT error response

    • reset

      IResponse reset()
      Resets the solver to the initial state, clearing all assertions, declarations, and options.
      Returns:
      success or an SMT error response

    • reset_assertions

      IResponse reset_assertions()
      Removes asserted formulae (but not global declarations when :global-declarations is true).
      Returns:
      success or an SMT error response

    • exit

      IResponse exit()
      Terminates the solver; no further commands are permitted.
      Returns:
      success or an SMT error response

    • forceExit

      void forceExit()
      Terminates the solver forcibly without sending commands (e.g. by killing the process).

    • echo

      IResponse echo(IExpr.IStringLiteral arg)
      Echoes the argument string back to the output channel.
      Returns:
      the argument as an IResponse

    • setSourceLine

      default void setSourceLine(int line)
      Tells the solver the line of the user's source on which the command about to be executed starts (counted from 1), or 0 if it has none, so that the line numbers in the solver's messages can be given as lines of that source

    • execute

      default IResponse execute(ICommand command)
      Executes the command on this solver

    • comment

      void comment(String comment)
      Passes comment text to the solver (for logging/tracing); the argument is the comment body without the leading semicolon.

    • set_logic

      IResponse set_logic(String logicName, IPos pos)
      Sets the logic the solver should use.
      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

    • push

      IResponse push(int number)
      Adds the given number of empty assertion-stack frames to the solver state.
      Parameters:
      number - non-negative number of frames to push
      Returns:
      success or an SMT error response

    • pop

      IResponse pop(int number)
      Removes the given number of assertion-stack frames from the solver state.
      Parameters:
      number - non-negative number of frames to pop
      Returns:
      success or an SMT error response

    • assertExpr

      IResponse assertExpr(IExpr expr)
      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.
      Returns:
      success or an SMT error response

    • check_sat

      IResponse check_sat()
      Checks whether the current assertion set is satisfiable under the current logic.
      Returns:
      sat, unsat, unknown, or an SMT error response

    • check_sat_assuming

      IResponse check_sat_assuming(IExpr... exprs)
      Checks satisfiability under the current assertion set plus the given propositional assumptions.
      Returns:
      sat, unsat, unknown, or an SMT error response

    • declare_const

      IResponse declare_const(ICommand.Ideclare_const cmd)
      Declares a new uninterpreted constant; returns success or an SMT error response

    • declare_datatype

      IResponse declare_datatype(ICommand.Ideclare_datatype cmd)
      Declares a new datatype sort; returns success or an SMT error response

    • declare_datatypes

      IResponse declare_datatypes(ICommand.Ideclare_datatypes cmd)
      Declares mutually recursive datatype sorts; returns success or an SMT error response

    • declare_fun

      IResponse declare_fun(ICommand.Ideclare_fun cmd)
      Declares a new uninterpreted function (or constant); returns success or an SMT error response

    • declare_sort

      IResponse declare_sort(ICommand.Ideclare_sort cmd)
      Declares a new uninterpreted sort; returns success or an SMT error response

    • declare_sort_parameter

      IResponse declare_sort_parameter(ICommand.Ideclare_sort_parameter cmd)
      Declares a new sort parameter (polymorphic sort variable); returns success or an SMT error response

    • define_const

      IResponse define_const(ICommand.Idefine_const cmd)
      Defines a named constant — syntactic sugar for define-fun with no parameters; returns success or an SMT error response

    • define_fun

      IResponse define_fun(ICommand.Idefine_fun cmd)
      Defines a named function or constant; returns success or an SMT error response

    • define_fun_rec

      IResponse define_fun_rec(ICommand.Idefine_fun_rec cmd)
      Defines a named recursive function; returns success or an SMT error response

    • define_funs_rec

      IResponse define_funs_rec(ICommand.Idefine_funs_rec cmd)
      Defines a group of mutually recursive functions; returns success or an SMT error response

    • define_sort

      IResponse define_sort(ICommand.Idefine_sort cmd)
      Defines a sort abbreviation; returns success or an SMT error response

    • set_option

      IResponse set_option(IExpr.IKeyword option, IAttributeValue value)
      Sets an SMT-LIB option.
      Parameters:
      option - the keyword naming the option
      value - the value to set
      Returns:
      success, unsupported, or an SMT error response

    • set_info

      IResponse set_info(IExpr.IKeyword key, IAttributeValue value)
      Annotates the problem with an info attribute (e.g. :status sat).
      Parameters:
      key - the info keyword
      value - the attribute value
      Returns:
      success, unsupported, or an SMT error response

    • get_assertions

      IResponse get_assertions()
      Returns the list of formulae in the current assertion set, in the order they were asserted. Requires :produce-assertions to be enabled; returns an error if it is not. SMT-LIB does not stipulate the order of the terms in the returned list.
      Returns:
      a sequence of asserted terms, unsupported, or an SMT error response

    • get_proof

      IResponse get_proof()
      Returns a proof of unsatisfiability for the current assertion set. Requires :produce-proofs to be enabled; returns an error if it is not.
      Returns:
      a proof, unsupported, or an SMT error response

    • get_model

      IResponse get_model()
      Returns a satisfying model for the current assertion set. Requires :produce-models to be enabled and the last check-sat to have returned sat; returns an error if these preconditions are not met.
      Returns:
      a model, unsupported, or an SMT error response

    • get_unsat_assumptions

      IResponse get_unsat_assumptions()
      Returns the subset of check-sat-assuming assumptions that caused the result to be unsat. Requires :produce-unsat-assumptions to be enabled; returns an error if it is not.
      Returns:
      a list of assumption literals, unsupported, or an SMT error response

    • get_unsat_core

      IResponse get_unsat_core()
      Returns the named formulae that form an unsatisfiable core of the current assertion set. Requires :produce-unsat-cores to be enabled; returns an error if it is not.
      Returns:
      a list of formula names, unsupported, or an SMT error response

    • get_value

      IResponse get_value(IExpr... terms)
      Returns the values of the given expressions in the current satisfying model. Requires :produce-models to be enabled and the last check-sat to have returned sat; returns an error if these preconditions are not met.
      Parameters:
      terms - expressions to evaluate
      Returns:
      a list of term–value pairs, unsupported, or an SMT error response

    • get_assignment

      IResponse get_assignment()
      Returns the truth-value assignments for all named Boolean formulae in the current model. Requires :produce-assignments to be enabled and the last check-sat to have returned sat; returns an error if these preconditions are not met.
      Returns:
      a list of name–Boolean pairs, unsupported, or an SMT error response

    • get_option

      IResponse get_option(IExpr.IKeyword option)
      Returns the current value of the named option.
      Parameters:
      option - the keyword naming the option
      Returns:
      the option value, or unsupported, or an SMT error response

    • get_info

      IResponse get_info(IExpr.IKeyword option)
      Returns the value of the named info item.
      Parameters:
      option - the info keyword
      Returns:
      the info value, or unsupported, or an SMT error response