public abstract class AbstractSortedOperator extends java.lang.Object implements SortedOperator, Sorted
Modifier | Constructor and Description |
---|---|
protected |
AbstractSortedOperator(Name name,
ImmutableArray<Sort> argSorts,
Sort sort,
boolean isRigid) |
protected |
AbstractSortedOperator(Name name,
ImmutableArray<Sort> argSorts,
Sort sort,
ImmutableArray<java.lang.Boolean> whereToBind,
boolean isRigid) |
protected |
AbstractSortedOperator(Name name,
Sort[] argSorts,
Sort sort,
boolean isRigid) |
protected |
AbstractSortedOperator(Name name,
Sort[] argSorts,
Sort sort,
java.lang.Boolean[] whereToBind,
boolean isRigid) |
protected |
AbstractSortedOperator(Name name,
Sort sort,
boolean isRigid) |
Modifier and Type | Method and Description |
---|---|
protected void |
additionalValidTopLevel(Term term)
Allows subclasses to impose custom demands on what constitutes a
valid term using the operator represented by the subclass.
|
Sort |
argSort(int i) |
ImmutableArray<Sort> |
argSorts() |
int |
arity()
the arity of this operator
|
boolean |
bindVarsAt(int n)
Tells whether the operator binds variables at the n-th subterm.
|
boolean |
isRigid()
Tells whether the operator is rigid.
|
Name |
name()
returns the name of this element
|
Sort |
sort() |
Sort |
sort(ImmutableArray<Term> terms)
Determines the sort of the
Term if it would be created using this
Operator as top level operator and the given terms as sub terms. |
java.lang.String |
toString() |
void |
validTopLevelException(Term term)
Checks whether the top level structure of the given @link Term
is syntactically valid, given the assumption that the top level
operator of the term is the same as this Operator.
|
protected ImmutableArray<java.lang.Boolean> |
whereToBind() |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
arity, bindVarsAt, isRigid, validTopLevel, validTopLevelException
protected AbstractSortedOperator(Name name, ImmutableArray<Sort> argSorts, Sort sort, ImmutableArray<java.lang.Boolean> whereToBind, boolean isRigid)
protected AbstractSortedOperator(Name name, Sort[] argSorts, Sort sort, java.lang.Boolean[] whereToBind, boolean isRigid)
protected AbstractSortedOperator(Name name, ImmutableArray<Sort> argSorts, Sort sort, boolean isRigid)
protected AbstractSortedOperator(Name name, Sort[] argSorts, Sort sort, boolean isRigid)
public final Sort sort(ImmutableArray<Term> terms)
Operator
Term
if it would be created using this
Operator as top level operator and the given terms as sub terms. The
assumption that the constructed term would be allowed is not checked.protected final void additionalValidTopLevel(Term term)
public final Sort argSort(int i)
argSort
in interface SortedOperator
public final ImmutableArray<Sort> argSorts()
argSorts
in interface SortedOperator
public final Sort sort()
sort
in interface SortedOperator
sort
in interface Sorted
protected final ImmutableArray<java.lang.Boolean> whereToBind()
public final Name name()
Named
public final int arity()
Operator
public final boolean bindVarsAt(int n)
Operator
bindVarsAt
in interface Operator
public final boolean isRigid()
Operator
public void validTopLevelException(Term term) throws TermCreationException
Operator
validTopLevelException
in interface Operator
TermCreationException
- if a construction error was recognisepublic java.lang.String toString()
toString
in class java.lang.Object
Copyright © 2003-2019 The KeY-Project.