public class StaticFeatureCollection extends 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(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(String schemaVar,
TermFeature tf)
Invoke the term feature
tf on the term that instantiation of
schemaVar . |
protected static Feature |
atomSmallerThan(String smaller,
String bigger,
IntegerLDT numbers) |
protected static Feature |
blockContractFeature(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(String schemaVar)
Create a projection of taclet applications to the instantiation of the
schema variables
schemaVar . |
protected static ProjectionToTerm |
instOfNonStrict(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(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(String smaller,
String bigger,
IntegerLDT numbers) |
protected static Feature |
longConst(long a) |
protected static TermFeature |
longTermConst(long a) |
protected static Feature |
loopInvFeature(Feature cost) |
protected static Feature |
methodSpecFeature(Feature cost) |
protected static Feature |
monSmallerThan(String smaller,
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 Feature |
setupJoinRule() |
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(String smaller,
String bigger) |
protected static Feature setupJoinRule()
protected static Feature sequentContainsNoPrograms()
protected static Feature countOccurrences(ProjectionToTerm cutFormula)
protected static Feature monSmallerThan(String smaller, String bigger, IntegerLDT numbers)
protected static Feature atomSmallerThan(String smaller, String bigger, IntegerLDT numbers)
protected static Feature literalsSmallerThan(String smaller, 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(String schemaVar)
schemaVar
. If schemaVar
is not
instantiated for a particular taclet app, an error will be raisedprotected static ProjectionToTerm instOfNonStrict(String schemaVar)
schemaVar
. The projection will be partial
and undefined for those taclet applications that do not instantiate
schemaVar
protected 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 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(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 appprotected static Feature applyTFNonStrict(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 appprotected 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 raisedprotected 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 returnedprotected 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)