Package org.smtlib.command

Class C_set_option

java.lang.Object
org.smtlib.impl.Pos.Posable
org.smtlib.impl.Pos.Printable
org.smtlib.impl.Command
org.smtlib.command.C_set_option
All Implemented Interfaces:
ICommand, ICommand.Iset_option, INode, IPos.IPosable
public class C_set_option extends Command implements ICommand.Iset_option
Implements the set-option command

  • Field Details

  • Constructor Details

  • Method Details

    • commandName

      public String commandName()
      The command name
      Specified by:
      commandName in interface ICommand
      Specified by:
      commandName in class Command

    • option

      public IExpr.IKeyword option()
      The keyword for the option to set
      Specified by:
      option in interface ICommand.Iset_option

    • value

      public IAttributeValue value()
      The new value of the option being set
      Specified by:
      value in interface ICommand.Iset_option

    • parse

      public static C_set_option parse(Parser p) throws IParser.ParserException
      Creates a command instance by parsing the concrete S-expression syntax
      Throws:
      IParser.ParserException

    • execute

      public IResponse execute(ISolver solver)
      Description copied from interface: ICommand
      Executes the command on the given solver; presumes that the command type-checked successfully.
      Specified by:
      execute in interface ICommand
      Parameters:
      solver - the instance of the solver to use (note that solvers have state)
      Returns:
      the result of the command

    • checkOptionType

      public IResponse.IError checkOptionType(SMT.Configuration smtConfig, IExpr.IKeyword keyword, IAttributeValue t)
      This method checks that the value for the given keyword has the correct type, when the keyword is used as the key for an SMT-LIB option. Called eagerly from parse() above, unlike most other commands (e.g. C_declare_fun's non-standard extensions, C_define_fun's result-sort check -- see issue #40), which defer semantic validation to type-checking/execute time. That's deliberate here, not an inconsistency to remove: unlike commands whose semantics are checked uniformly regardless of solver (TypeChecker.validate()'s job), no real solver adapter validates option-value types at all -- they forward set-option straight to the real process (see AbstractSolver#set_option) -- so parse time is the only point that would otherwise ever be reached for every solver alike. It is not, however, the *only* layer: Solver_test.set_option() and AbstractSolver#checkPrintSuccess() both separately validate :print-success's value too, since smtConfig.commandFactory.set_option(key,value) can construct and execute a C_set_option directly, bypassing this parse-time check entirely (see issue #41) -- AbstractSolver#set_option_impl() itself calls exactly that factory method.
      Parameters:
      keyword - the keyword controlling the type
      t - the value being tested
      Returns:
      null or an error response

    • accept

      public <T> T accept(IVisitor<T> v) throws IVisitor.VisitorException
      Description copied from interface: INode
      The accept method corresponding to IVisitor, to be implemented in each subclass as { return v.visit(this); }
      Specified by:
      accept in interface INode
      Type Parameters:
      T - the return type desired from the visit methods
      Parameters:
      v - the visitor class
      Returns:
      the value returned by the visit method
      Throws:
      IVisitor.VisitorException