Package org.smtlib.impl

Class Sort.Parameter

java.lang.Object
org.smtlib.impl.Pos.Posable
org.smtlib.impl.Pos.Printable
org.smtlib.impl.Sort
org.smtlib.impl.Sort.Parameter
All Implemented Interfaces:
INode, IPos.IPosable, ISort, ISort.IDefinition, ISort.IParameter
Enclosing class:
Sort
public static class Sort.Parameter extends Sort implements ISort.IParameter
Represents a Sort parameter, such as in either the parameter list or the expression of a Sort abbreviation

  • Field Details

  • Constructor Details

    • Parameter

      public Parameter(IExpr.ISymbol symbol)
      Creates a sort parameter for the given symbol name.

  • Method Details

    • symbol

      public IExpr.ISymbol symbol()
      Description copied from interface: ISort.IParameter
      The symbol that names the parameter
      Specified by:
      symbol in interface ISort.IParameter

    • 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

    • expand

      public ISort expand()
      Description copied from interface: ISort
      Expands all abbreviations
      Specified by:
      expand in interface ISort

    • equals

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

    • hashCode

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

    • 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

    • identifier

      public IExpr.IIdentifier identifier()
      Description copied from interface: ISort.IDefinition
      The identifier for the sort symbol
      Specified by:
      identifier in interface ISort.IDefinition

    • eval

      public ISort eval(List<ISort> sorts)
      Description copied from interface: ISort.IDefinition
      A new sort expression that results from applying the sort symbol to a list of sort expressions
      Specified by:
      eval in interface ISort.IDefinition

    • intArity

      public int intArity()
      Description copied from interface: ISort.IDefinition
      The arity of the symbol
      Specified by:
      intArity in interface ISort.IDefinition