Package org.smtlib

Interface ISort.IApplication

All Superinterfaces:
INode, IPos.IPosable, ISort
All Known Implementing Classes:
Sort.Application
Enclosing interface:
ISort
public static interface ISort.IApplication extends ISort
The interface for a Sort expression that consists of either an arity 0 sort symbol or a positive-arity symbol with the appropriate number of arguments.

  • Method Details

    • family

      IExpr.IIdentifier family()
      The head identifier of the sort expression

    • param

      ISort param(int i)
      Returns the ith parameter

    • parameters

      List<ISort> parameters()
      Returns the list of parameters

    • definition

      ISort.IDefinition definition()
      The definition of the family identifier, valid after the sort expression has been type-checked.

    • definition

      ISort.IDefinition definition(ISort.IDefinition definition)
      Sets and returns the value of definition() for this object to the value that is the argument

    • parenthesized

      default boolean parenthesized()
      True if written in parentheses; (S), with no parameters, is not SMT-LIB but is parsed (with an error) so that type checking reports it as well

    • expand

      ISort expand()
      Expands any head abbreviations, if any; requires definition() to be defined
      Specified by:
      expand in interface ISort

    • equals

      boolean equals(Object o)
      Description copied from interface: ISort
      Structural equality after expansion of abbreviations (an alias and its literal expansion are equal), but without any substitution of free parameters. The general- purpose equality method -- use this unless a caller specifically needs a narrower comparison below.
      Specified by:
      equals in interface ISort
      Overrides:
      equals in class Object
      See Also:

    • equalsNoExpand

      boolean equalsNoExpand(ISort sort)
      Description copied from interface: ISort
      Raw structural comparison, deliberately without abbreviation expansion or parameter substitution -- so a user-defined alias and its expansion, which ISort.equals(Object) treats as equal, are NOT equal here. Used internally as ISort.equals(Object)'s own building block (expand both sides first, then compare structurally with this), and directly by any caller that specifically wants the literal, as-declared shape rather than the expanded one, e.g. Logic.checkArraySort(), which checks an array sort's declared shape against a fixed set of allowed sorts without expanding through an alias first.
      Specified by:
      equalsNoExpand in interface ISort