Modifier and Type | Field and Description |
---|---|
private int |
baseCost |
static int |
ConsideredAsBigLiteral
If the literals in a query become greater than abs(ConsideredAsBigLiteral), then
this is interpreted as a "loop smell", i.e. the proof construction is in a loop
and produces big literals.
|
private int |
maxRepetitionsOnSameTerm |
private int |
termAgeFactor |
static RuleAppCost |
TOP_COST
Constant that represents the boolean value false
|
private boolean |
useExperimentalHeuristics |
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) |
private static int |
maxIntliteralInArgumentsTimesTwo(Term t,
IntegerLDT iLDT,
Services serv) |
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.
|
private static int |
sumOfAbsLiteralsTimesTwo(Term t,
IntegerLDT iLDT,
Services serv)
Absolute values of literal occurring in t a used for cost computation.
|
public static final RuleAppCost ZERO_COST
public static final RuleAppCost TOP_COST
public static final int ConsideredAsBigLiteral
private final int baseCost
private final int maxRepetitionsOnSameTerm
private final int termAgeFactor
private final boolean useExperimentalHeuristics
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).private static int maxIntliteralInArgumentsTimesTwo(Term t, IntegerLDT iLDT, Services serv)
t
- the query that is considered for the rule expand query.iLDT
- serv
- literalsToCost
private static int sumOfAbsLiteralsTimesTwo(Term t, IntegerLDT iLDT, Services serv)
t
- The term is expected to be an argument of the query.iLDT
- serv
- protected int queryExpandAlreadyAppliedAtPos(RuleApp app, PosInOccurrence pos, Goal goal)
protected static boolean isStepCaseBranch(Goal goal)
public int getMaxRepetitionsOnSameTerm()