Package org.smtlib

Interface ISort.IParameter

All Superinterfaces:

INode, IPos.IPosable, ISort, ISort.IDefinition

All Known Implementing Classes:

Sort.Parameter

Enclosing interface:

ISort

public static interface ISort.IParameter
extends ISort, ISort.IDefinition

The interface for a sort parameter, as used in sort abbreviations (including in the defining expression).

Nested Class Summary

Nested classes/interfaces inherited from interface org.smtlib.ISort

ISort.IAbbreviation, ISort.IApplication, ISort.IDatatype, ISort.IDefinition, ISort.IErrorDefinition, ISort.IFactory, ISort.IFamily, ISort.IFcnSort, ISort.IParameter

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 ISort.equals(Object) treats as equal, are NOT equal here.
IExpr.ISymbol	symbol()	The symbol that names the parameter

Methods inherited from interface org.smtlib.INode

accept

Methods inherited from interface org.smtlib.IPos.IPosable

pos, setPos

Methods inherited from interface org.smtlib.ISort

expand, isBool, substitute

Methods inherited from interface org.smtlib.ISort.IDefinition

eval, identifier, intArity

Method Details

symbol

IExpr.ISymbol symbol()

The symbol that names the parameter

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:

• ISort.equalsNoExpand(ISort)

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