Package org.smtlib

Interface ISort

All Superinterfaces:
INode, IPos.IPosable
All Known Subinterfaces:
ISort.IApplication, ISort.IFcnSort, ISort.IParameter
All Known Implementing Classes:
Sort, Sort.Application, Sort.FcnSort, Sort.Parameter
public interface ISort extends INode, IPos.IPosable
The interface for an SMT-LIB concept of a Sort. Two kinds of things are modeled here.

First, a definition of a Sort, modeled by ISort.IDefinition. There are these kinds of definitions:

  • an ISort.IFamily, which defines a new sort symbol of a given arity
  • an ISort.IAbbreviation, which defines a (possibly parameterized) abbreviation for a sort expression.
  • an ISort.IParameter, which defines a sort name used as a parameter in an abbreviation definition
  • an ISort.IDatatype - a datatype sort
  • The ISort.ErrorDefinition class, which is used as a definition place holder for ill-formed definitions, to avoid excessive redundant errors
Second, Sort expressions themselves, modeled by ISort:
  • A ISort.IApplication, which is the application of an IDefinition to the appropriate number (possibly 0) of Sort expressions
  • A ISort.IParameter, which is a simple symbol designating the parameter of a parameterized abbreviation
  • A ISort.IFcnSort, an expression designating a function sort.

  • Nested Class Summary

    Nested Classes
    Modifier and Type
    Interface
    Description
    static interface 
    ISort.IAbbreviation
    This interface represents a new Sort symbol designating an abbreviation for a (possibly parameterized) sort expression.
    static interface 
    ISort.IApplication
    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.
    static interface 
    ISort.IDatatype
    The interface for a datatype declaration (used in declare-datatype and declare-datatypes).
    static interface 
    ISort.IDefinition
    A super-interface for definitions of new sort ids.
    static interface 
    ISort.IErrorDefinition
    Represents an erroneous sort definition; by having an actual IDefinition, redundant cascading errors are suppressed.
    static interface 
    ISort.IFactory
    The interface for a Sort-creating factory.
    static interface 
    ISort.IFamily
    This interface represents a new Sort symbol designating either a new Sort (if the arity is 0) or a new parameterized Sort family (if the arity is greater than 0); each new symbol has a (new) name and a non-negative arity.
    static interface 
    ISort.IFcnSort
    An interface to represent the Sort of a function; this is not something that can be written as a sort expression in SMT-LIB, but it is convenient to be able to represent the sorts of function ids uniformly with the sorts of other ids.
    static interface 
    ISort.IParameter
    The interface for a sort parameter, as used in sort abbreviations (including in the defining expression).

  • Method Summary

    Modifier and Type
    Method
    Description
    boolean
    equals(Object o)
    Structural equality after expansion of abbreviations (an alias and its literal expansion are equal), but without any substitution of free parameters.
    boolean
    equalsNoExpand(ISort sort)
    Raw structural comparison, deliberately without abbreviation expansion or parameter substitution -- so a user-defined alias and its expansion, which equals(Object) treats as equal, are NOT equal here.
    ISort
    expand()
    Expands all abbreviations
    boolean
    isBool()
    Returns true if the receiver designates the Bool pre-defined Sort.
    ISort
    substitute(Map<ISort.IParameter,ISort> map)
    Returns a new sort with any parameters substituted

    Methods inherited from interface org.smtlib.INode

    accept

    Methods inherited from interface org.smtlib.IPos.IPosable

    pos, setPos

  • Method Details

    • equals

      boolean equals(Object o)
      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.
      Overrides:
      equals in class Object
      See Also:

    • isBool

      boolean isBool()
      Returns true if the receiver designates the Bool pre-defined Sort.

    • expand

      ISort expand()
      Expands all abbreviations

    • substitute

      ISort substitute(Map<ISort.IParameter,ISort> map)
      Returns a new sort with any parameters substituted

    • equalsNoExpand

      boolean equalsNoExpand(ISort sort)
      Raw structural comparison, deliberately without abbreviation expansion or parameter substitution -- so a user-defined alias and its expansion, which equals(Object) treats as equal, are NOT equal here. Used internally as 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.