public class Function extends AbstractSortedOperator
Constructor and Description |
---|
Function(Name name,
Sort sort) |
Function(Name name,
Sort sort,
boolean isSkolemConstant) |
Function(Name name,
Sort sort,
boolean isSkolemConstant,
Sort... argSorts) |
Function(Name name,
Sort sort,
ImmutableArray<Sort> argSorts) |
Function(Name name,
Sort sort,
ImmutableArray<Sort> argSorts,
ImmutableArray<java.lang.Boolean> whereToBind,
boolean unique) |
Function(Name name,
Sort sort,
ImmutableArray<Sort> argSorts,
ImmutableArray<java.lang.Boolean> whereToBind,
boolean unique,
boolean isSkolemConstant) |
Function(Name name,
Sort sort,
Sort... argSorts) |
Function(Name name,
Sort sort,
Sort[] argSorts,
java.lang.Boolean[] whereToBind,
boolean unique) |
Function(Name name,
Sort sort,
Sort[] argSorts,
java.lang.Boolean[] whereToBind,
boolean unique,
boolean isSkolemConstant) |
Modifier and Type | Method and Description |
---|---|
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.
|
boolean |
isSkolemConstant() |
boolean |
isUnique()
Indicates whether the function or predicate symbol has the "uniqueness"
property.
|
Name |
name()
returns the name of this element
|
java.lang.String |
proofToString()
Returns a parsable string representation of the declaration of this
function or predicate symbol.
|
Function |
rename(Name newName) |
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() |
additionalValidTopLevel, argSort, argSorts, sort, sort
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
arity, bindVarsAt, isRigid, validTopLevel, validTopLevelException
public Function(Name name, Sort sort, ImmutableArray<Sort> argSorts, ImmutableArray<java.lang.Boolean> whereToBind, boolean unique)
public Function(Name name, Sort sort, ImmutableArray<Sort> argSorts, ImmutableArray<java.lang.Boolean> whereToBind, boolean unique, boolean isSkolemConstant)
public Function(Name name, Sort sort, Sort[] argSorts, java.lang.Boolean[] whereToBind, boolean unique)
public Function(Name name, Sort sort, Sort[] argSorts, java.lang.Boolean[] whereToBind, boolean unique, boolean isSkolemConstant)
public Function(Name name, Sort sort, ImmutableArray<Sort> argSorts)
public final boolean isUnique()
public final boolean isSkolemConstant()
public final java.lang.String toString()
public final java.lang.String proofToString()
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 recogniseCopyright © 2003-2019 The KeY-Project.