Modifier and Type | Field and Description |
---|---|
static int |
ConsideredAsBigLiteral
If the literals in a query become greater than abs(ConsideredAsBigLiteral), then
this is interpreted as a "loop smell", i.e.
|
static RuleAppCost |
TOP_COST
Constant that represents the boolean value false
|
static RuleAppCost |
ZERO_COST
Constant that represents the boolean value true
|
Constructor and Description |
---|
QueryExpandCost(int baseCost,
int maxRepetitionsOnSameTerm,
int termAgeFactor,
boolean useExperimentalHeuristics) |
Modifier and Type | Method and Description |
---|---|
RuleAppCost |
computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal)
Evaluate the cost of a
RuleApp . |
int |
getMaxRepetitionsOnSameTerm() |
protected static boolean |
isStepCaseBranch(Goal goal)
This method determines whether the given goal belongs to a subtree of a
step case or body preserves case.
|
protected int |
queryExpandAlreadyAppliedAtPos(RuleApp app,
PosInOccurrence pos,
Goal goal)
The method checks if the same rule has been applied earlier on this branch
at the same position in the sequent.
|
public static final RuleAppCost ZERO_COST
public static final RuleAppCost TOP_COST
public static final int ConsideredAsBigLiteral
public QueryExpandCost(int baseCost, int maxRepetitionsOnSameTerm, int termAgeFactor, boolean useExperimentalHeuristics)
baseCost
- Should be set to 200. This was the cost before this class was introduced.maxRepetitionsOnSameTerm
- Search in the current branch if query expand
has been already applied on this term.
For each such application a penalty cost is added.
If this limit is exceeded the cost is set to TOP_COST,
i.e. the rule is not applied.termAgeFactor
- This factor (must be >= 0) sets the cost of older queries lower,
than that of younger queries (i.e. that occur later in proofs). The effect is a
breath-first search
on the expansion of queries.
In class QueryExpand
the time is stored, when queries can be
expanded for the first time.useExperimentalHeuristics
- Activates experimental, pattern-based heuristics.public RuleAppCost computeCost(RuleApp app, PosInOccurrence pos, Goal goal)
Feature
RuleApp
.computeCost
in interface Feature
app
- the RuleApppos
- position where app
is to be appliedgoal
- the goal on which app
is to be appliedRuleAppCost
object. TopRuleAppCost.INSTANCE
indicates that the rule shall not be applied at all (it is discarded by
the strategy).protected int queryExpandAlreadyAppliedAtPos(RuleApp app, PosInOccurrence pos, Goal goal)
app
- The rule application.pos
- The occurrence position.goal
- The goal.protected static boolean isStepCaseBranch(Goal goal)
goal
- the current proof goalpublic int getMaxRepetitionsOnSameTerm()
Copyright © 2003-2019 The KeY-Project.