public final class SortDependingFunction extends Function
Modifier and Type | Class and Description |
---|---|
private static class |
SortDependingFunction.SortDependingFunctionTemplate |
Modifier and Type | Field and Description |
---|---|
private Sort |
sortDependingOn |
private SortDependingFunction.SortDependingFunctionTemplate |
template |
Modifier | Constructor and Description |
---|---|
private |
SortDependingFunction(SortDependingFunction.SortDependingFunctionTemplate template,
Sort sortDependingOn) |
Modifier and Type | Method and Description |
---|---|
static SortDependingFunction |
createFirstInstance(GenericSort sortDependingOn,
Name kind,
Sort sort,
Sort[] argSorts,
boolean unique) |
static SortDependingFunction |
getFirstInstance(Name kind,
TermServices services) |
SortDependingFunction |
getInstanceFor(Sort sort,
TermServices services)
returns the variant for the given sort
|
Name |
getKind() |
Sort |
getSortDependingOn() |
private static ImmutableArray<Sort> |
instantiateArgSorts(SortDependingFunction.SortDependingFunctionTemplate template,
Sort sortDependingOn) |
private static Name |
instantiateName(Name kind,
Sort sortDependingOn) |
private static Sort |
instantiateResultSort(SortDependingFunction.SortDependingFunctionTemplate template,
Sort sortDependingOn) |
boolean |
isSimilar(SortDependingFunction p) |
isSkolemConstant, isUnique, proofToString, rename, 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 SortDependingFunction.SortDependingFunctionTemplate template
private final Sort sortDependingOn
private SortDependingFunction(SortDependingFunction.SortDependingFunctionTemplate template, Sort sortDependingOn)
private static Sort instantiateResultSort(SortDependingFunction.SortDependingFunctionTemplate template, Sort sortDependingOn)
private static ImmutableArray<Sort> instantiateArgSorts(SortDependingFunction.SortDependingFunctionTemplate template, Sort sortDependingOn)
public static SortDependingFunction createFirstInstance(GenericSort sortDependingOn, Name kind, Sort sort, Sort[] argSorts, boolean unique)
public static SortDependingFunction getFirstInstance(Name kind, TermServices services)
public SortDependingFunction getInstanceFor(Sort sort, TermServices services)
sort
- the Sort
for which to retrieve the corresponding
variant of this functionservices
- the Services
public Sort getSortDependingOn()
public boolean isSimilar(SortDependingFunction p)
public Name getKind()