Package org.smtlib.solvers

Class Solver_test

java.lang.Object
org.smtlib.solvers.Solver_test
All Implemented Interfaces:
ISolver
public class Solver_test extends Object implements ISolver
This class is a Solver implementation that simply type-checks formulae and checks that commands are used correctly; it does not do any proving.

  • Field Details

    • smtConfig

      protected SMT.Configuration smtConfig
      A reference to the configuration used by this SMT instance.

    • symTable

      public SymbolTable symTable
      The symbol table used by this solver

    • assertionSetStack

      protected List<List<IExpr>> assertionSetStack
      The solver's assertion set stack, one frame per push level, top first. Once the logic is set it always has at least one frame: start() and reset() add the base frame and pop() cannot remove it. The base frame holds the assertions made outside any push. Declarations live in symTable, which has one more frame: each frame here pairs with the symTable frame of the same level (the base frame with its primary frame), and symTable's bottom, background frame holds the logic's symbols and the global declarations.

    • logicSet

      protected String logicSet
      Internal state variable - set non-null once the logic is set.

    • checkSatStatus

      protected IResponse checkSatStatus
      Internal state variable - set to sat, unsat, unknown when check-sat is run and then to null whenever an additional push, pop, assert, declare- or define- command is executed. This is used in checking those commands that depend on the above set of conditions.

    • options

      protected Map<String,IAttributeValue> options
      The data structure that maintains the current values of options and info items for this solver.

  • Constructor Details

    • Solver_test

      public Solver_test(SMT.Configuration smtConfig, String exec)
      Constructor for an instance of this test solver class; the second argument is ignored - it is present just for uniformity with other solvers, for which that argument is a path to the relevant executable. This constructor is called by reflection, upon knowing the name of the solver ("test").
      Parameters:
      smtConfig - a reference to the configuration instance in use
      exec - the executable for the solver, ignored for the case of this test solver

  • Method Details

    • solverName

      public String solverName()
      Description copied from interface: ISolver
      A public, user-readable name for the solver adapter class
      Specified by:
      solverName in interface ISolver

    • smt

      public SMT.Configuration smt()
      Returns the reference to the configuration currently in use.
      Specified by:
      smt in interface ISolver

    • checkSatStatus

      public IResponse checkSatStatus()
      Description copied from interface: ISolver
      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.
      Specified by:
      checkSatStatus in interface ISolver

    • 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
      Returns:
      success or an SMT error response

    • 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
      Returns:
      success or an SMT error response

    • comment

      public void comment(String comment)
      Description copied from interface: ISolver
      Passes comment text to the solver (for logging/tracing); the argument is the comment body without the leading semicolon.
      Specified by:
      comment in interface ISolver

    • 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
      Returns:
      success or an SMT error response

    • execute

      public IResponse execute(ICommand cmd)
      Once exited, every command but exit (and a comment) answers as a process-based solver's would
      Specified by:
      execute in interface ISolver

    • exit

      public IResponse exit()
      Description copied from interface: ISolver
      Terminates the solver; no further commands are permitted.
      Specified by:
      exit in interface ISolver
      Returns:
      success or an SMT error response

    • forceExit

      public void forceExit()
      Description copied from interface: ISolver
      Terminates the solver forcibly without sending commands (e.g. by killing the process).
      Specified by:
      forceExit in interface ISolver

    • echo

      public IResponse echo(IExpr.IStringLiteral arg)
      Description copied from interface: ISolver
      Echoes the argument string back to the output channel.
      Specified by:
      echo in interface ISolver
      Returns:
      the argument as an IResponse

    • assertExpr

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

    • get_assertions

      public IResponse get_assertions()
      Description copied from interface: ISolver
      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.
      Specified by:
      get_assertions in interface ISolver
      Returns:
      a sequence of asserted terms, unsupported, or an SMT error response

    • 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
      Returns:
      sat, unsat, unknown, or an SMT error response

    • 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
      Returns:
      sat, unsat, unknown, or an SMT error response

    • get_value

      public IResponse get_value(IExpr... terms)
      Description copied from interface: ISolver
      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.
      Specified by:
      get_value in interface ISolver
      Parameters:
      terms - expressions to evaluate
      Returns:
      a list of term–value pairs, unsupported, or an SMT error response

    • get_assignment

      public IResponse get_assignment()
      Description copied from interface: ISolver
      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.
      Specified by:
      get_assignment in interface ISolver
      Returns:
      a list of name–Boolean pairs, unsupported, or an SMT error response

    • get_proof

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

    • get_model

      public IResponse get_model()
      Description copied from interface: ISolver
      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.
      Specified by:
      get_model in interface ISolver
      Returns:
      a model, unsupported, or an SMT error response

    • get_unsat_assumptions

      public IResponse get_unsat_assumptions()
      Description copied from interface: ISolver
      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.
      Specified by:
      get_unsat_assumptions in interface ISolver
      Returns:
      a list of assumption literals, unsupported, or an SMT error response

    • get_unsat_core

      public IResponse get_unsat_core()
      Description copied from interface: ISolver
      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.
      Specified by:
      get_unsat_core in interface ISolver
      Returns:
      a list of formula names, unsupported, or an SMT error response

    • 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
      Parameters:
      number - non-negative number of frames to pop
      Returns:
      success or an SMT error response

    • 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
      Parameters:
      number - non-negative number of frames to push
      Returns:
      success or an SMT error response

    • set_logic

      public IResponse set_logic(String logicName, IPos pos)
      Description copied from interface: ISolver
      Sets the logic the solver should use.
      Specified by:
      set_logic in interface ISolver
      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

    • set_option

      public IResponse set_option(IExpr.IKeyword key, IAttributeValue value)
      Description copied from interface: ISolver
      Sets an SMT-LIB option.
      Specified by:
      set_option in interface ISolver
      Parameters:
      key - the keyword naming the option
      value - the value to set
      Returns:
      success, unsupported, or an SMT error response

    • get_option

      public IResponse get_option(IExpr.IKeyword key)
      Description copied from interface: ISolver
      Returns the current value of the named option.
      Specified by:
      get_option in interface ISolver
      Parameters:
      key - the keyword naming the option
      Returns:
      the option value, or unsupported, or an SMT error response

    • set_info

      public IResponse set_info(IExpr.IKeyword key, IAttributeValue value)
      Description copied from interface: ISolver
      Annotates the problem with an info attribute (e.g. :status sat).
      Specified by:
      set_info in interface ISolver
      Parameters:
      key - the info keyword
      value - the attribute value
      Returns:
      success, unsupported, or an SMT error response

    • get_info

      public IResponse get_info(IExpr.IKeyword key)
      Description copied from interface: ISolver
      Returns the value of the named info item.
      Specified by:
      get_info in interface ISolver
      Parameters:
      key - the info keyword
      Returns:
      the info value, or unsupported, or an SMT error response

    • encode

      protected String encode(IExpr.IIdentifier id)

    • declare_const

      public IResponse declare_const(ICommand.Ideclare_const cmd)
      Description copied from interface: ISolver
      Declares a new uninterpreted constant; returns success or an SMT error response
      Specified by:
      declare_const in interface ISolver

    • declare_fun

      public IResponse declare_fun(ICommand.Ideclare_fun cmd)
      Description copied from interface: ISolver
      Declares a new uninterpreted function (or constant); returns success or an SMT error response
      Specified by:
      declare_fun in interface ISolver

    • define_const

      public IResponse define_const(ICommand.Idefine_const cmd)
      Description copied from interface: ISolver
      Defines a named constant — syntactic sugar for define-fun with no parameters; returns success or an SMT error response
      Specified by:
      define_const in interface ISolver

    • define_fun

      public IResponse define_fun(ICommand.Idefine_fun cmd)
      Description copied from interface: ISolver
      Defines a named function or constant; returns success or an SMT error response
      Specified by:
      define_fun in interface ISolver

    • define_fun_rec

      public IResponse define_fun_rec(ICommand.Idefine_fun_rec cmd)
      Description copied from interface: ISolver
      Defines a named recursive function; returns success or an SMT error response
      Specified by:
      define_fun_rec in interface ISolver

    • define_funs_rec

      public IResponse define_funs_rec(ICommand.Idefine_funs_rec cmd)
      Description copied from interface: ISolver
      Defines a group of mutually recursive functions; returns success or an SMT error response
      Specified by:
      define_funs_rec in interface ISolver

    • declare_sort

      public IResponse declare_sort(ICommand.Ideclare_sort cmd)
      Description copied from interface: ISolver
      Declares a new uninterpreted sort; returns success or an SMT error response
      Specified by:
      declare_sort in interface ISolver

    • declare_sort_parameter

      public IResponse declare_sort_parameter(ICommand.Ideclare_sort_parameter cmd)
      Description copied from interface: ISolver
      Declares a new sort parameter (polymorphic sort variable); returns success or an SMT error response
      Specified by:
      declare_sort_parameter in interface ISolver

    • define_sort

      public IResponse define_sort(ICommand.Idefine_sort cmd)
      Description copied from interface: ISolver
      Defines a sort abbreviation; returns success or an SMT error response
      Specified by:
      define_sort in interface ISolver

    • declare_datatype

      public IResponse declare_datatype(ICommand.Ideclare_datatype cmd)
      Description copied from interface: ISolver
      Declares a new datatype sort; returns success or an SMT error response
      Specified by:
      declare_datatype in interface ISolver

    • declare_datatypes

      public IResponse declare_datatypes(ICommand.Ideclare_datatypes cmd)
      Description copied from interface: ISolver
      Declares mutually recursive datatype sorts; returns success or an SMT error response
      Specified by:
      declare_datatypes in interface ISolver