public abstract class StaticFeatureCollection
extends java.lang.Object
Constructor and Description |
---|
StaticFeatureCollection() |
Modifier and Type | Method and Description |
---|---|
protected static Feature |
add(Feature... features) |
protected static Feature |
add(Feature a,
Feature b) |
protected static Feature |
add(Feature a,
Feature b,
Feature c) |
protected static TermFeature |
add(TermFeature a,
TermFeature b) |
protected static TermFeature |
add(TermFeature a,
TermFeature b,
TermFeature c) |
protected static TermFeature |
any() |
protected static Feature |
applyTF(ProjectionToTerm term,
TermFeature tf)
Evaluate the term feature
tf for the term described by the projection
term . |
protected static Feature |
applyTF(java.lang.String schemaVar,
TermFeature tf)
Invoke the term feature
tf on the term that instantiation of
schemaVar . |
protected static Feature |
applyTFNonStrict(ProjectionToTerm term,
TermFeature tf)
Evaluate the term feature
tf for the term described by the projection
term . |
protected static Feature |
applyTFNonStrict(java.lang.String schemaVar,
TermFeature tf)
Invoke the term feature
tf on the term that instantiation of
schemaVar . |
protected static Feature |
atomSmallerThan(java.lang.String smaller,
java.lang.String bigger,
IntegerLDT numbers) |
protected static Feature |
blockContractExternalFeature(Feature cost) |
protected static Feature |
blockContractInternalFeature(Feature cost) |
protected static RuleAppCost |
c(long p) |
protected static Feature |
contains(ProjectionToTerm bigTerm,
ProjectionToTerm searchedTerm) |
protected static Feature |
countOccurrences(ProjectionToTerm cutFormula) |
protected static Feature |
eq(Feature a,
Feature b) |
protected static Feature |
eq(ProjectionToTerm t1,
ProjectionToTerm t2) |
protected static TermFeature |
eq(TermBuffer t) |
protected static TermFeature |
extendsTrans(Sort s) |
protected static Feature |
ifZero(Feature cond,
Feature thenFeature) |
protected static Feature |
ifZero(Feature cond,
Feature thenFeature,
Feature elseFeature) |
protected static TermFeature |
ifZero(TermFeature cond,
TermFeature thenFeature) |
protected static TermFeature |
ifZero(TermFeature cond,
TermFeature thenFeature,
TermFeature elseFeature) |
protected static Feature |
implicitCastNecessary(ProjectionToTerm s1) |
private static RuleAppCost |
infty() |
protected static Feature |
inftyConst() |
protected static TermFeature |
inftyTermConst() |
protected static ProjectionToTerm |
instOf(java.lang.String schemaVar)
Create a projection of taclet applications to the instantiation of the schema variables
schemaVar . |
protected static ProjectionToTerm |
instOfNonStrict(java.lang.String schemaVar)
Create a projection of taclet applications to the instantiation of the schema variables
schemaVar . |
protected static ProjectionToTerm |
instOfTriggerVariable()
Create a projection of taclet applications to the instantiation of the trigger variable of a
taclet.
|
protected static Feature |
isInstantiated(java.lang.String schemaVar) |
protected static Feature |
isSubSortFeature(ProjectionToTerm s1,
ProjectionToTerm s2) |
protected static Feature |
isTriggerVariableInstantiated() |
protected static Feature |
leq(Feature a,
Feature b) |
protected static Feature |
less(Feature a,
Feature b) |
protected static Feature |
let(TermBuffer x,
ProjectionToTerm value,
Feature body) |
protected static Feature |
literalsSmallerThan(java.lang.String smaller,
java.lang.String bigger,
IntegerLDT numbers) |
protected static Feature |
longConst(long a) |
protected static TermFeature |
longTermConst(long a) |
protected static Feature |
loopContractApplyHead(Feature cost) |
protected static Feature |
loopContractExternalFeature(Feature cost) |
protected static Feature |
loopContractInternalFeature(Feature cost) |
protected static Feature |
loopInvFeature(Feature costStdInv,
Feature costLoopScopeInv) |
protected static Feature |
mergeRuleFeature(Feature cost) |
protected static Feature |
methodSpecFeature(Feature cost) |
protected static Feature |
monSmallerThan(java.lang.String smaller,
java.lang.String bigger,
IntegerLDT numbers) |
protected static Feature |
not(Feature f) |
protected static TermFeature |
not(TermFeature f) |
protected static TermFeature |
op(Operator op) |
protected static TermFeature |
opSub(Operator op,
TermFeature sub0) |
protected static TermFeature |
opSub(Operator op,
TermFeature sub0,
TermFeature sub1) |
protected static ProjectionToTerm |
opTerm(Operator op,
ProjectionToTerm subTerm) |
protected static ProjectionToTerm |
opTerm(Operator op,
ProjectionToTerm[] subTerms) |
protected static ProjectionToTerm |
opTerm(Operator op,
ProjectionToTerm subTerm0,
ProjectionToTerm subTerm1) |
protected static Feature |
or(Feature... features) |
protected static Feature |
or(Feature a,
Feature b) |
protected static Feature |
or(Feature a,
Feature b,
Feature c) |
protected static TermFeature |
or(TermFeature a,
TermFeature b) |
protected static TermFeature |
or(TermFeature a,
TermFeature b,
TermFeature c) |
protected static Feature |
println(ProjectionToTerm t) |
protected static Feature |
querySpecFeature(Feature cost) |
protected static TermFeature |
rec(TermFeature cond,
TermFeature summand) |
protected static Feature |
sequentContainsNoPrograms() |
protected static ProjectionToTerm |
sub(ProjectionToTerm t,
int index) |
protected static TermFeature |
sub(TermFeature sub0) |
protected static TermFeature |
sub(TermFeature sub0,
TermFeature sub1) |
protected static ProjectionToTerm |
subAt(ProjectionToTerm t,
PosInTerm pit) |
protected static Feature |
sum(TermBuffer x,
TermGenerator gen,
Feature body) |
protected static Feature |
termSmallerThan(java.lang.String smaller,
java.lang.String bigger) |
protected static Feature loopInvFeature(Feature costStdInv, Feature costLoopScopeInv)
protected static Feature blockContractInternalFeature(Feature cost)
cost
- The specified cost.BlockContractInternalRule
with the specified cost.protected static Feature blockContractExternalFeature(Feature cost)
cost
- The specified cost.BlockContractExternalRule
with the specified cost.protected static Feature loopContractInternalFeature(Feature cost)
cost
- The specified cost.LoopContractInternalRule
with the specified cost.protected static Feature loopContractExternalFeature(Feature cost)
cost
- The specified cost.LoopContractExternalRule
with the specified cost.protected static Feature loopContractApplyHead(Feature cost)
cost
- The specified cost.LoopApplyHeadRule
with the specified cost.protected static Feature sequentContainsNoPrograms()
protected static Feature countOccurrences(ProjectionToTerm cutFormula)
protected static Feature termSmallerThan(java.lang.String smaller, java.lang.String bigger)
protected static Feature monSmallerThan(java.lang.String smaller, java.lang.String bigger, IntegerLDT numbers)
protected static Feature atomSmallerThan(java.lang.String smaller, java.lang.String bigger, IntegerLDT numbers)
protected static Feature literalsSmallerThan(java.lang.String smaller, java.lang.String bigger, IntegerLDT numbers)
protected static Feature longConst(long a)
protected static Feature inftyConst()
protected static TermFeature any()
protected static TermFeature longTermConst(long a)
protected static TermFeature inftyTermConst()
protected static TermFeature add(TermFeature a, TermFeature b)
protected static TermFeature add(TermFeature a, TermFeature b, TermFeature c)
protected static TermFeature or(TermFeature a, TermFeature b)
protected static TermFeature or(TermFeature a, TermFeature b, TermFeature c)
protected static TermFeature ifZero(TermFeature cond, TermFeature thenFeature)
protected static TermFeature ifZero(TermFeature cond, TermFeature thenFeature, TermFeature elseFeature)
protected static TermFeature not(TermFeature f)
protected static RuleAppCost c(long p)
private static RuleAppCost infty()
protected static ProjectionToTerm instOfTriggerVariable()
protected static ProjectionToTerm instOf(java.lang.String schemaVar)
schemaVar
. If schemaVar
is not instantiated for a particular taclet
app, an error will be raisedschemaVar
- schema variableprotected static ProjectionToTerm instOfNonStrict(java.lang.String schemaVar)
schemaVar
. The projection will be partial and undefined for those taclet
applications that do not instantiate schemaVar
schemaVar
- schema variableprotected static ProjectionToTerm subAt(ProjectionToTerm t, PosInTerm pit)
protected static ProjectionToTerm sub(ProjectionToTerm t, int index)
protected static ProjectionToTerm opTerm(Operator op, ProjectionToTerm[] subTerms)
protected static ProjectionToTerm opTerm(Operator op, ProjectionToTerm subTerm)
protected static ProjectionToTerm opTerm(Operator op, ProjectionToTerm subTerm0, ProjectionToTerm subTerm1)
protected static Feature isInstantiated(java.lang.String schemaVar)
protected static Feature isTriggerVariableInstantiated()
protected static TermFeature op(Operator op)
protected static TermFeature rec(TermFeature cond, TermFeature summand)
protected static TermFeature sub(TermFeature sub0)
protected static TermFeature sub(TermFeature sub0, TermFeature sub1)
protected static TermFeature opSub(Operator op, TermFeature sub0)
protected static TermFeature opSub(Operator op, TermFeature sub0, TermFeature sub1)
protected static TermFeature eq(TermBuffer t)
protected static Feature eq(ProjectionToTerm t1, ProjectionToTerm t2)
protected static Feature contains(ProjectionToTerm bigTerm, ProjectionToTerm searchedTerm)
protected static Feature println(ProjectionToTerm t)
protected static TermFeature extendsTrans(Sort s)
protected static Feature applyTF(java.lang.String schemaVar, TermFeature tf)
tf
on the term that instantiation of
schemaVar
. This is the strict/safe version that raises an error of
schemaVar
is not instantiated for a particular taclet appschemaVar
- schema variabletf
- term featureprotected static Feature applyTFNonStrict(java.lang.String schemaVar, TermFeature tf)
tf
on the term that instantiation of
schemaVar
. This is the non-strict/unsafe version that simply returns zero if
schemaVar
is not instantiated for a particular taclet appschemaVar
- schema variabletf
- term featureprotected static Feature applyTF(ProjectionToTerm term, TermFeature tf)
tf
for the term described by the projection
term
. If term
is undefined for a particular rule app, an exception
is raisedterm
- term describing the projectiontf
- term featureprotected static Feature applyTFNonStrict(ProjectionToTerm term, TermFeature tf)
tf
for the term described by the projection
term
. If term
is undefined for a particular rule app, zero is
returnedterm
- term describing the projectiontf
- term featureprotected static Feature sum(TermBuffer x, TermGenerator gen, Feature body)
protected static Feature let(TermBuffer x, ProjectionToTerm value, Feature body)
protected static Feature isSubSortFeature(ProjectionToTerm s1, ProjectionToTerm s2)
protected static Feature implicitCastNecessary(ProjectionToTerm s1)