Package org.smtlib.impl

Class Sort.FcnSort

java.lang.Object
org.smtlib.impl.Pos.Posable
org.smtlib.impl.Pos.Printable
org.smtlib.impl.Sort
org.smtlib.impl.Sort.FcnSort
All Implemented Interfaces:
INode, IPos.IPosable, ISort, ISort.IFcnSort
Enclosing class:
Sort
public static class Sort.FcnSort extends Sort implements ISort.IFcnSort
Represents the class of the sort of a function symbol. This is not a sort that can be expressed in SMT-LIB sort grammar, except implicitly when function ids are defined in define-fun and declare-fun commands and in theory definitions.

  • Field Details

    • noargs

      protected static final ISort[] noargs

    • resultSort

      protected ISort resultSort

    • argSorts

      protected ISort[] argSorts

  • Constructor Details

    • FcnSort

      public FcnSort(ISort[] argSorts, ISort resultSort)
      Creates a function sort with the given argument sorts and result sort.

    • FcnSort

      public FcnSort(ISort resultSort)
      Creates a zero-argument (nullary) function sort with the given result sort.

  • Method Details

    • expand

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

    • resultSort

      public ISort resultSort()
      Specified by:
      resultSort in interface ISort.IFcnSort

    • argSorts

      public ISort[] argSorts()
      Specified by:
      argSorts in interface ISort.IFcnSort

    • 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
      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

    • 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