public class Function extends AbstractSortedOperator
Modifier and Type | Field and Description |
---|---|
private boolean |
skolemConstant |
private boolean |
unique |
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,
boolean isRigid) |
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,
ImmutableArray<Sort> argSorts,
ImmutableArray<java.lang.Boolean> whereToBind,
boolean unique,
boolean isRigid,
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 |
---|---|
boolean |
isSkolemConstant() |
boolean |
isUnique()
Indicates whether the function or predicate symbol has the "uniqueness"
property.
|
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() |
additionalValidTopLevel, additionalValidTopLevel2, argSort, argSorts, sort, sort
arity, bindVarsAt, isRigid, name, validTopLevel, whereToBind
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
arity, bindVarsAt, isRigid, validTopLevel
private final boolean unique
private final boolean skolemConstant
Function(Name name, Sort sort, ImmutableArray<Sort> argSorts, ImmutableArray<java.lang.Boolean> whereToBind, boolean unique, boolean isRigid, boolean isSkolemConstant)
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)
Function(Name name, Sort sort, ImmutableArray<Sort> argSorts, boolean isRigid)
public Function(Name name, Sort sort, ImmutableArray<Sort> argSorts)
public final boolean isUnique()
public final boolean isSkolemConstant()
public final java.lang.String toString()
toString
in class AbstractOperator
public final java.lang.String proofToString()