Package org.smtlib.impl

Class Sort.Application

java.lang.Object
org.smtlib.impl.Pos.Posable
org.smtlib.impl.Pos.Printable
org.smtlib.impl.Sort
org.smtlib.impl.Sort.Application
All Implemented Interfaces:
INode, IPos.IPosable, ISort, ISort.IApplication
Enclosing class:
Sort
public static class Sort.Application extends Sort implements ISort.IApplication
Represents a sort expression consisting of a sort symbol or sort abbreviation symbol applied to a corresponding number of sort arguments

  • Field Details

    • sortID

      protected IExpr.IIdentifier sortID

    • sortParameters

      protected List<ISort> sortParameters

    • definition

      protected ISort.IDefinition definition
      Reference to definition; filled in during type-checking

    • expanded

      protected ISort expanded
      Cached value for expanded()

    • emptyParentheses

      protected boolean emptyParentheses
      Whether the sort was written as (S), in parentheses with no parameters

  • Constructor Details

    • Application

      public Application(IExpr.IIdentifier sortID, List<ISort> sortParameters)
      Creates a sort application from a sort identifier and a list of sort arguments.

    • Application

      public Application(IExpr.IIdentifier sortID, List<ISort> sortParameters, boolean parenthesized)
      Creates a sort application that is written in parentheses even if it has no parameters, as (S)

    • Application

      public Application(IExpr.IIdentifier sortID, ISort... sortParameters)
      Creates a sort application from a sort identifier and a varargs array of sort arguments.

  • Method Details

    • parenthesized

      public boolean parenthesized()
      Description copied from interface: ISort.IApplication
      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
      Specified by:
      parenthesized in interface ISort.IApplication

    • family

      public IExpr.IIdentifier family()
      Description copied from interface: ISort.IApplication
      The head identifier of the sort expression
      Specified by:
      family in interface ISort.IApplication

    • param

      public ISort param(int i)
      Description copied from interface: ISort.IApplication
      Returns the ith parameter
      Specified by:
      param in interface ISort.IApplication

    • parameters

      public List<ISort> parameters()
      Description copied from interface: ISort.IApplication
      Returns the list of parameters
      Specified by:
      parameters in interface ISort.IApplication

    • definition

      public ISort.IDefinition definition()
      Description copied from interface: ISort.IApplication
      The definition of the family identifier, valid after the sort expression has been type-checked.
      Specified by:
      definition in interface ISort.IApplication

    • definition

      public ISort.IDefinition definition(ISort.IDefinition definition)
      Description copied from interface: ISort.IApplication
      Sets and returns the value of definition() for this object to the value that is the argument
      Specified by:
      definition in interface ISort.IApplication

    • expand

      public ISort expand()
      Description copied from interface: ISort.IApplication
      Expands any head abbreviations, if any; requires definition() to be defined
      Specified by:
      expand in interface ISort
      Specified by:
      expand in interface ISort.IApplication

    • equals

      public boolean equals(Object sort)
      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
      Specified by:
      equals in interface ISort.IApplication
      Overrides:
      equals in class Pos.Posable
      See Also:

    • equalsNoExpand

      public 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
      Specified by:
      equalsNoExpand in interface ISort.IApplication

    • hashCode

      public int hashCode()
      Overrides:
      hashCode in class Pos.Posable

    • substitute

      public ISort substitute(Map<ISort.IParameter,ISort> map)
      Description copied from interface: ISort
      Returns a new sort with any parameters substituted
      Specified by:
      substitute in interface ISort

    • 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