public abstract class AbstractBetaFeature extends java.lang.Object implements Feature
Modifier and Type | Class and Description |
---|---|
static class |
AbstractBetaFeature.TermInfo
Informations about a term as cached within "betaCandidates"
|
Constructor and Description |
---|
AbstractBetaFeature() |
Modifier and Type | Method and Description |
---|---|
static boolean |
alwaysReplace(Term p_t) |
RuleAppCost |
computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal)
Compute the cost of a RuleApp.
|
protected static boolean |
containsNegAtom(Term p_t,
boolean p_positive,
ServiceCaches caches) |
protected static boolean |
containsQuantifier(Term p_t,
ServiceCaches caches) |
protected abstract RuleAppCost |
doComputation(PosInOccurrence pos,
Term findTerm,
ServiceCaches caches) |
protected static boolean |
hasPurePosPath(Term p_t,
boolean p_positive,
ServiceCaches caches)
p_t contains a d-path consisting only of positive literals (as a formula
of the antecedent)
|
protected static boolean |
isBetaCandidate(Term p_t,
boolean p_inAntec,
ServiceCaches caches) |
protected static int |
maxDPath(Term p_t,
boolean p_positive,
ServiceCaches caches)
The length (number of literals) of the maximum d-path of the given
formula as a formula of the antecedent
|
protected static int |
maxPosPath(Term p_t,
boolean p_positive,
ServiceCaches caches)
The maximal number of positive literals occurring within a
d-path of "p_t" as a formula of the antecedent
|
protected static boolean hasPurePosPath(Term p_t, boolean p_positive, ServiceCaches caches)
caches
- TODOprotected static int maxPosPath(Term p_t, boolean p_positive, ServiceCaches caches)
caches
- TODOprotected static int maxDPath(Term p_t, boolean p_positive, ServiceCaches caches)
caches
- TODOprotected static boolean containsQuantifier(Term p_t, ServiceCaches caches)
caches
- TODOprotected static boolean containsNegAtom(Term p_t, boolean p_positive, ServiceCaches caches)
caches
- TODOpublic static boolean alwaysReplace(Term p_t)
protected static boolean isBetaCandidate(Term p_t, boolean p_inAntec, ServiceCaches caches)
caches
- TODOpublic RuleAppCost computeCost(RuleApp app, PosInOccurrence pos, Goal goal)
computeCost
in interface Feature
app
- the RuleApppos
- position where app
is to be appliedgoal
- the goal on which app
is to be appliedapp
protected abstract RuleAppCost doComputation(PosInOccurrence pos, Term findTerm, ServiceCaches caches)
Copyright © 2003-2019 The KeY-Project.