Package org.smtlib.command

Class C_declare_fun

java.lang.Object
org.smtlib.impl.Pos.Posable
org.smtlib.impl.Pos.Printable
org.smtlib.impl.Command
org.smtlib.command.C_declare_fun
All Implemented Interfaces:
ICommand, ICommand.Ideclare_fun, INode, IPos.IPosable
Direct Known Subclasses:
C_declare_const
public class C_declare_fun extends Command implements ICommand.Ideclare_fun
Implements the declare-fun command

  • Field Details

    • commandName

      public static final String commandName
      The command name
      See Also:

    • fcnName

      protected IExpr.ISymbol fcnName
      The name of the function being declared

    • argSorts

      protected List<ISort> argSorts
      The sorts of the arguments of the function being declared -- never null (every construction path, parser or direct, always supplies a real list, empty for a zero-argument function).

    • resultSort

      protected ISort resultSort
      The result sort of the function being declared

    • attributes

      protected List<IExpr.IAttribute<?>> attributes
      Any trailing attributes (see attributes()) -- never null, Collections.emptyList() if none (the common case: this is a non-standard extension, only meaningful at all under --relax). Unlike parameters, null-vs-empty draws no real distinction here: the concrete syntax has no way to write an explicit-but-empty attribute clause (attributes are a bare trailing sequence, not a bracketed list), so there is nothing for a null/non-null split to usefully encode -- it would just be an arbitrary implementation detail, not a meaningful state. See issue #42 point 2.

    • parameters

      protected List<ISort.IParameter> parameters
      The par-polymorphic parameters (see parameters()). Unlike attributes, null here is load-bearing, not just an empty-list stand-in: it distinguishes an ordinary declaration from the non-standard "(declare-fun par (params) (name sorts attrs))" form (SMT-LIB's declare-fun has no par production at all), and Solver_test.declare_fun(org.smtlib.ICommand.Ideclare_fun) branches on that distinction directly (e.g. requiring --relax only when this is non-null) -- collapsing it to Collections.emptyList() would erase real information (a par-polymorphic declaration's parameter list is never actually empty in practice -- the grammar requires param+ -- so there is no "empty par-form" state this could be confused with). Null for an ordinary declaration. See issue #42 point 2.

  • Constructor Details

    • C_declare_fun

      public C_declare_fun(IExpr.ISymbol symbol, List<ISort> argSorts, ISort resultSort)
      Constructs a command instance for an ordinary (non-attributed, non-par) declaration

    • C_declare_fun

      public C_declare_fun(IExpr.ISymbol symbol, List<ISort> argSorts, ISort resultSort, List<IExpr.IAttribute<?>> attributes)
      Constructs a command instance for an ordinary declaration, including any trailing attributes (see attributes()).

    • C_declare_fun

      public C_declare_fun(IExpr.ISymbol symbol, List<ISort> argSorts, ISort resultSort, List<IExpr.IAttribute<?>> attributes, List<ISort.IParameter> parameters)
      Constructs a command instance from all of its components, including the par-polymorphic parameters (see parameters()) for the "(declare-fun par ...)" form.

  • Method Details

    • commandName

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

    • symbol

      public IExpr.ISymbol symbol()
      Description copied from interface: ICommand.Ideclare_fun
      Returns the name of the function being declared.
      Specified by:
      symbol in interface ICommand.Ideclare_fun

    • argSorts

      public List<ISort> argSorts()
      Description copied from interface: ICommand.Ideclare_fun
      Returns the list of argument sorts.
      Specified by:
      argSorts in interface ICommand.Ideclare_fun

    • resultSort

      public ISort resultSort()
      Description copied from interface: ICommand.Ideclare_fun
      Returns the result sort.
      Specified by:
      resultSort in interface ICommand.Ideclare_fun

    • attributes

      public List<IExpr.IAttribute<?>> attributes()
      Description copied from interface: ICommand.Ideclare_fun
      Returns any trailing attributes given after the result sort -- an experimental, non-standard extension (SMT-LIB's declare-fun has no attribute* production); accepting one at all is unconditional at parse time, but the command is rejected at type-checking time unless --relax is set. Never null; empty if none were given -- unlike ICommand.Ideclare_fun.parameters(), null-vs-empty has no real distinction to encode here (the concrete syntax has no way to write an explicit-but-empty attribute clause).
      Specified by:
      attributes in interface ICommand.Ideclare_fun

    • parameters

      public List<ISort.IParameter> parameters()
      Description copied from interface: ICommand.Ideclare_fun
      Returns the par-polymorphic type parameters, for the experimental, non-standard "(declare-fun par (param+) (name sort+ attribute*))" form -- mirrors exactly the par_fun_symbol_decl shape a theory's own :funs entry uses. Accepting this form at all is unconditional at parse time, but the command is rejected at type-checking time unless --relax is set. Null for an ordinary (non-par) declare-fun -- this is load-bearing, not just an empty-list stand-in: Solver_test.declare_fun(org.smtlib.ICommand.Ideclare_fun) branches on null-vs-non-null directly to decide whether --relax is required, and a par-form's parameter list is never actually empty in practice (the grammar requires param+), so there is no "empty par-form" state this could be confused with.
      Specified by:
      parameters in interface ICommand.Ideclare_fun

    • parse

      public static C_declare_fun parse(Parser p) throws IParser.ParserException
      Parses the arguments of the command, producing a new command instance. Two non-standard extensions, both parsed unconditionally (whether either is actually accepted, rather than rejected with a specific message, is decided at type-checking time in Solver_test.declare_fun() -- see there): - A trailing attribute* after the result sort (e.g. :left-assoc), the same production a theory's own fun_symbol_decl can carry, so a user-declared function can opt into the same n-ary sugar handling SymbolTable.lookup() already applies to theory-declared ones. Standard SMT-LIB declare-fun has no such production. - "(declare-fun par (param+) (name sort+ attribute*))": a par-polymorphic declaration, detected by the literal reserved word "par" appearing where the function's own symbol normally goes (the same technique parseDatatype() already uses to detect datatype's own optional par form). The nested (name sort+ attribute*) is exactly the par_fun_symbol_decl shape a theory's own :funs entry uses (e.g. Core.smt2's (par (A) (= A A Bool :chainable))) -- reusing that shape verbatim, under the familiar declare-fun command name, rather than inventing a different, unrelated syntax or a wholly new top-level command name. SMT-LIB's declare-fun has no par form at all (par otherwise only appears in declare-datatype's own constructor lists).
      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

    • 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