Skip to content

Commit 04dc4d1

Browse files
unp1unp1
committed
CostBand: cost()/at() return a constant Feature; document layer relation
- cost() and at(delta) return the cost as a constant strategy Feature (ConstFeature over NumberRuleAppCost - exactly what longConst produced), so call sites lose the redundant wrapper: longConst(CostBand.DEFER.at(500)) becomes CostBand.DEFER.at(500), and bindRuleSet sites switch transparently to the Feature overload. The raw number stays available via value(); no code needed it. Behaviour unchanged (runAllProofs 674/674). - Document the deliberate relation between the layers: theory-local constants are absolute values on the same cost line, not anchored to a band, so retuning a tier moves exactly the rules placed on it. Point CostBand's javadoc at a real theory holder (was a stale IntegerCost reference), and note in IntegerArithmeticCosts why the file is not named "IntegerCosts" (would read as an integer-valued RuleAppCost type).
1 parent bae1d24 commit 04dc4d1

7 files changed

Lines changed: 86 additions & 68 deletions

File tree

‎key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java‎

Lines changed: 27 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -85,7 +85,7 @@ public FOLStrategy(Proof proof, StrategyProperties strategyProperties) {
8585

8686
private Feature setUpGlobalF(RuleSetDispatchFeature d) {
8787
final Feature oneStepSimplificationF =
88-
oneStepSimplificationFeature(longConst(CostBand.REWRITE.cost()));
88+
oneStepSimplificationFeature(CostBand.REWRITE.cost());
8989
return add(d, oneStepSimplificationF);
9090
}
9191

@@ -107,7 +107,7 @@ private RuleSetDispatchFeature setupCostComputationF() {
107107
FindDepthFeature.getInstance();
108108

109109
bindRuleSet(d, "concrete",
110-
add(longConst(CostBand.REWRITE.cost()),
110+
add(CostBand.REWRITE.cost(),
111111
ScaleFeature.createScaled(findDepthFeature, 10.0)));
112112
bindRuleSet(d, "simplify", CostBand.SIMPLIFY.cost());
113113
bindRuleSet(d, "simplify_enlarging", CostBand.ENLARGE.cost());
@@ -123,51 +123,51 @@ private RuleSetDispatchFeature setupCostComputationF() {
123123
not(contains(AssumptionProjection.create(0), FocusProjection.INSTANCE))));
124124

125125
bindRuleSet(d, "update_elim",
126-
add(longConst(CostBand.ELIMINATE.cost()),
126+
add(CostBand.ELIMINATE.cost(),
127127
ScaleFeature.createScaled(findDepthFeature, 10.0)));
128128
bindRuleSet(d, "update_apply_on_update",
129-
add(longConst(CostBand.DECOMPOSE.cost()),
129+
add(CostBand.DECOMPOSE.cost(),
130130
ScaleFeature.createScaled(findDepthFeature, 10.0)));
131131
bindRuleSet(d, "update_join", CostBand.SIMPLIFY.at(-100));
132132
bindRuleSet(d, "update_apply", CostBand.SIMPLIFY.cost());
133133

134134
setupSplitting(d);
135135

136136
bindRuleSet(d, "gamma", add(not(isInstantiated("t")),
137-
ifZero(allowQuantifierSplitting(), longConst(CostBand.DEFAULT.cost()),
138-
longConst(CostBand.DEFAULT.at(50)))));
137+
ifZero(allowQuantifierSplitting(), CostBand.DEFAULT.cost(),
138+
CostBand.DEFAULT.at(50))));
139139
bindRuleSet(d, "gamma_destructive", inftyConst());
140140

141141
bindRuleSet(d, "triggered",
142-
add(not(isTriggerVariableInstantiated()), longConst(CostBand.DEFER.cost())));
142+
add(not(isTriggerVariableInstantiated()), CostBand.DEFER.cost()));
143143

144144
bindRuleSet(d, "comprehension_split",
145145
add(applyTF(FocusFormulaProjection.INSTANCE, ff.notContainsExecutable),
146-
ifZero(allowQuantifierSplitting(), longConst(CostBand.DEFER.at(2000)),
147-
longConst(CostBand.DEFER.at(4500)))));
146+
ifZero(allowQuantifierSplitting(), CostBand.DEFER.at(2000),
147+
CostBand.DEFER.at(4500))));
148148

149149
setupReplaceKnown(d);
150150

151151
setupEquationReasoning(d);
152152

153153
bindRuleSet(d, "order_terms",
154154
add(termSmallerThan("commEqLeft", "commEqRight"),
155-
longConst(CostBand.NORMALIZE.cost())));
155+
CostBand.NORMALIZE.cost()));
156156

157157
bindRuleSet(d, "simplify_instanceof_static",
158-
add(EqNonDuplicateAppFeature.INSTANCE, longConst(CostBand.PREFER.cost())));
158+
add(EqNonDuplicateAppFeature.INSTANCE, CostBand.PREFER.cost()));
159159

160-
bindRuleSet(d, "evaluate_instanceof", longConst(CostBand.PREFER.cost()));
160+
bindRuleSet(d, "evaluate_instanceof", CostBand.PREFER.cost());
161161

162162
bindRuleSet(d, "instanceof_to_exists", TopLevelFindFeature.ANTEC);
163163

164164
bindRuleSet(d, "try_apply_subst",
165-
add(EqNonDuplicateAppFeature.INSTANCE, longConst(CostBand.SUBST.cost())));
165+
add(EqNonDuplicateAppFeature.INSTANCE, CostBand.SUBST.cost()));
166166

167167
// delete cast
168168
bindRuleSet(d, "cast_deletion",
169169
ifZero(implicitCastNecessary(instOf("castedTerm")),
170-
longConst(CostBand.NORMALIZE.cost()),
170+
CostBand.NORMALIZE.cost(),
171171
inftyConst()));
172172

173173
bindRuleSet(d, "type_hierarchy_def", CostBand.TYPE.at(-500));
@@ -291,13 +291,13 @@ public Name name() {
291291

292292
protected void setupFormulaNormalisation(RuleSetDispatchFeature d) {
293293
bindRuleSet(d, "negationNormalForm", add(BelowBinderFeature.getInstance(),
294-
longConst(CostBand.PREFER.cost()),
294+
CostBand.PREFER.cost(),
295295
ScaleFeature.createScaled(FindDepthFeature.getInstance(), 10.0)));
296296

297297
bindRuleSet(d, "moveQuantToLeft",
298-
add(quantifiersMightSplit() ? longConst(CostBand.DEFAULT.cost())
298+
add(quantifiersMightSplit() ? CostBand.DEFAULT.cost()
299299
: applyTF(FocusFormulaProjection.INSTANCE, ff.quantifiedPureLitConjDisj),
300-
longConst(CostBand.PREFER.at(-50))));
300+
CostBand.PREFER.at(-50)));
301301

302302
bindRuleSet(d, "conjNormalForm",
303303
ifZero(
@@ -307,7 +307,7 @@ protected void setupFormulaNormalisation(RuleSetDispatchFeature d) {
307307
ScaleFeature.createScaled(FindDepthFeature.getInstance(), 20)),
308308
inftyConst()));
309309

310-
bindRuleSet(d, "setEqualityBlastingRight", longConst(CostBand.DEFAULT.at(-100)));
310+
bindRuleSet(d, "setEqualityBlastingRight", CostBand.DEFAULT.at(-100));
311311

312312

313313

@@ -411,13 +411,13 @@ private void setupQuantifierInstantiation(RuleSetDispatchFeature d) {
411411
: ff.notContainsExecutable)),
412412
forEach(varInst, HeuristicInstantiation.INSTANCE,
413413
add(instantiate("t", varInst), branchPrediction,
414-
longConst(CostBand.DEFAULT.at(10))))));
414+
CostBand.DEFAULT.at(10)))));
415415
final TermBuffer splitInst = new TermBuffer();
416416

417417
bindRuleSet(d, "triggered",
418418
SumFeature.createSum(forEach(splitInst, TriggeredInstantiations.create(true),
419-
add(instantiateTriggeredVariable(splitInst), longConst(CostBand.DEFER.cost()))),
420-
longConst(CostBand.DEFER.at(1000))));
419+
add(instantiateTriggeredVariable(splitInst), CostBand.DEFER.cost())),
420+
CostBand.DEFER.at(1000)));
421421

422422
} else {
423423
bindRuleSet(d, "gamma", inftyConst());
@@ -432,7 +432,7 @@ private void setupQuantifierInstantiationApproval(RuleSetDispatchFeature d) {
432432
bindRuleSet(d, "gamma", add(isInstantiated("t"),
433433
not(sum(varInst, HeuristicInstantiation.INSTANCE, not(eq(instOf("t"), varInst)))),
434434
InstantiationCostScalerFeature.create(InstantiationCost.create(instOf("t")),
435-
longConst(CostBand.DEFAULT.cost()))));
435+
CostBand.DEFAULT.cost())));
436436

437437
final TermBuffer splitInst = new TermBuffer();
438438
bindRuleSet(d, "triggered",
@@ -462,7 +462,7 @@ protected Feature notBelowQuantifier() {
462462
private void setupReplaceKnown(RuleSetDispatchFeature d) {
463463
final Feature commonF =
464464
add(ifZero(MatchedAssumesFeature.INSTANCE, DiffFindAndIfFeature.INSTANCE),
465-
longConst(CostBand.NORMALIZE.cost()),
465+
CostBand.NORMALIZE.cost(),
466466
add(DiffFindAndReplacewithFeature.INSTANCE,
467467
ScaleFeature.createScaled(CountMaxDPathFeature.INSTANCE, 10.0)));
468468

@@ -490,10 +490,10 @@ protected void setupSplitting(RuleSetDispatchFeature d) {
490490
sum(subFor, AllowedCutPositionsGenerator.INSTANCE, not(applyTF(subFor, ff.cutAllowed)));
491491
bindRuleSet(d, "beta",
492492
SumFeature.createSum(noCutsAllowed,
493-
ifZero(PurePosDPathFeature.INSTANCE, longConst(CostBand.PREFER.at(300))),
493+
ifZero(PurePosDPathFeature.INSTANCE, CostBand.PREFER.at(300)),
494494
ScaleFeature.createScaled(CountPosDPathFeature.INSTANCE, -3.0),
495495
ScaleFeature.createScaled(CountMaxDPathFeature.INSTANCE, 10.0),
496-
longConst(CostBand.DEFAULT.at(20))));
496+
CostBand.DEFAULT.at(20)));
497497
TermBuffer superF = new TermBuffer();
498498
final ProjectionToTerm<Goal> splitCondition = sub(FocusProjection.INSTANCE, 0);
499499
bindRuleSet(d, "split_cond", add(// do not split over formulas containing auxiliary
@@ -509,7 +509,7 @@ protected void setupSplitting(RuleSetDispatchFeature d) {
509509
sum(superF, SuperTermGenerator.upwards(any(), getServices()),
510510
applyTF(superF, not(ff.elemUpdate))),
511511
ifZero(applyTF(FocusProjection.INSTANCE, ContainsExecutableCodeTermFeature.PROGRAMS),
512-
longConst(CostBand.DEFAULT.at(-100)), longConst(CostBand.DEFAULT.at(25)))));
512+
CostBand.DEFAULT.at(-100), CostBand.DEFAULT.at(25))));
513513
ProjectionToTerm<Goal> cutFormula = instOf("cutFormula");
514514
Feature countOccurrencesInSeq =
515515
ScaleFeature.createAffine(countOccurrences(cutFormula), -10, 10);
@@ -531,7 +531,7 @@ protected void setupSplitting(RuleSetDispatchFeature d) {
531531
applyTF(FocusFormulaProjection.INSTANCE,
532532
ff.quantifiedClauseSet),
533533
ifZero(allowQuantifierSplitting(),
534-
longConst(CostBand.DEFAULT.cost()),
534+
CostBand.DEFAULT.cost(),
535535
longConst(CUT_DIRECT_STANDARD))))));
536536
}
537537

‎key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerArithmeticCosts.java‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,10 @@
1010
* holder is meant to move with its sub-strategy. Cross-theory levels stay in
1111
* {@link org.key_project.prover.strategy.costbased.CostBand}; only the arithmetic-internal ordering
1212
* lives here. All values are byte-identical to the literals they replace.
13+
*
14+
* The file is named after the integer-arithmetic *theory*; a plain "IntegerCost(s)" would suggest
15+
* an integer-valued cost type (an implementation of RuleAppCost) rather than a holder of cost
16+
* constants.
1317
*/
1418

1519
/** Polynomial normal-form canonicalisation (Buchberger normalisation) — the "basic" substrate. */

‎key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -158,7 +158,7 @@ private RuleSetDispatchFeature setupCostComputationF() {
158158
bindRuleSet(d, "order_terms",
159159
add(applyTF("commEqRight", tf.monomial), applyTF("commEqLeft", tf.polynomial),
160160
monSmallerThan("commEqLeft", "commEqRight", numbers),
161-
longConst(CostBand.NORMALIZE.cost())));
161+
CostBand.NORMALIZE.cost()));
162162

163163
final TermBuffer equation = new TermBuffer();
164164
final TermBuffer left = new TermBuffer();
@@ -402,7 +402,7 @@ private void setupDivModDivision(RuleSetDispatchFeature d) {
402402
add(NotInScopeOfModalityFeature.INSTANCE, ifZero(isReduciblePolyE,
403403
// try again later
404404
longConst(-DivModCost.POLY_DIVISION)))))),
405-
longConst(CostBand.DEFAULT.at(100))));
405+
CostBand.DEFAULT.at(100)));
406406

407407
}
408408

@@ -576,7 +576,7 @@ private void setupInEqSimp(RuleSetDispatchFeature d, IntegerLDT numbers) {
576576
// category "handling of non-linear inequations"
577577

578578
if (arithNonLinInferences()) {
579-
setupMultiplyInequations(d, longConst(CostBand.DEFAULT.at(100)));
579+
setupMultiplyInequations(d, CostBand.DEFAULT.at(100));
580580

581581
bindRuleSet(d, "inEqSimp_split_eq",
582582
add(TopLevelFindFeature.SUCC, longConst(NonlinearArithmeticCost.SPLIT_EQ)));
@@ -699,9 +699,9 @@ private void setupMultiplyInequations(RuleSetDispatchFeature d, Feature notAllow
699699
ifZero(MatchedAssumesFeature.INSTANCE,
700700
SumFeature.createSum(
701701
applyTF("multFacLeft", tf.nonNegMonomial),
702-
ifZero(applyTF("multRight", tf.literal), longConst(CostBand.DEFAULT.at(-100))),
702+
ifZero(applyTF("multRight", tf.literal), CostBand.DEFAULT.at(-100)),
703703
ifZero(applyTF("multFacRight", tf.literal),
704-
longConst(CostBand.DEFAULT.at(-100)),
704+
CostBand.DEFAULT.at(-100),
705705
applyTF("multFacRight", tf.polynomial)),
706706
/*
707707
* ifZero ( applyTF ( "multRight", tf.literal ), longConst ( -100 ), applyTF (
@@ -710,8 +710,8 @@ private void setupMultiplyInequations(RuleSetDispatchFeature d, Feature notAllow
710710
*/
711711
not(TermSmallerThanFeature.create(FocusProjection.create(0),
712712
AssumptionProjection.create(0))),
713-
ifZero(exactlyBounded, longConst(CostBand.DEFAULT.cost()),
714-
ifZero(totallyBounded, longConst(CostBand.DEFAULT.at(100)), notAllowedF))
713+
ifZero(exactlyBounded, CostBand.DEFAULT.cost(),
714+
ifZero(totallyBounded, CostBand.DEFAULT.at(100), notAllowedF))
715715
/*
716716
* ifZero ( partiallyBounded, longConst ( 400 ), notAllowedF ) ) ),
717717
*/
@@ -850,9 +850,9 @@ private void setupInEqCaseDistinctions(RuleSetDispatchFeature d) {
850850
forEach(rootInf, RootsGenerator.create(intRel, getServices()),
851851
add(instantiate("cutFormula", rootInf),
852852
ifZero(applyTF(rootInf, op(Junctor.OR)),
853-
longConst(CostBand.DEFAULT.at(50))),
853+
CostBand.DEFAULT.at(50)),
854854
ifZero(applyTF(rootInf, op(Junctor.AND)),
855-
longConst(CostBand.DEFAULT.at(20))))),
855+
CostBand.DEFAULT.at(20)))),
856856
longConst(NonlinearArithmeticCost.MULTIPLY)));
857857

858858
// noinspection unchecked

‎key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -192,7 +192,7 @@ private RuleSetDispatchFeature setupCostComputationF() {
192192
bindRuleSet(d, "simplify_literals",
193193
// ifZero ( ConstraintStrengthenFeatureUC.create(proof),
194194
// longConst ( 0 ),
195-
longConst(CostBand.ELIMINATE.cost()));
195+
CostBand.ELIMINATE.cost());
196196

197197
bindRuleSet(d, "nonDuplicateAppCheckEq", EqNonDuplicateAppFeature.INSTANCE);
198198

@@ -219,7 +219,7 @@ private RuleSetDispatchFeature setupCostComputationF() {
219219
strategyProperties.getProperty(StrategyProperties.QUERYAXIOM_OPTIONS_KEY);
220220
switch (queryAxProp) {
221221
case StrategyProperties.QUERYAXIOM_ON ->
222-
bindRuleSet(d, "query_axiom", longConst(CostBand.SOLVE.cost()));
222+
bindRuleSet(d, "query_axiom", CostBand.SOLVE.cost());
223223
case StrategyProperties.QUERYAXIOM_OFF -> bindRuleSet(d, "query_axiom", inftyConst());
224224
default -> throw new RuntimeException("Unexpected strategy property " + queryAxProp);
225225
}
@@ -237,7 +237,7 @@ private RuleSetDispatchFeature setupCostComputationF() {
237237
// partial inv axiom
238238
bindRuleSet(d, "partialInvAxiom",
239239
add(NonDuplicateAppModPositionFeature.INSTANCE,
240-
longConst(CostBand.DEFER_STRONG.cost())));
240+
CostBand.DEFER_STRONG.cost()));
241241

242242
// inReachableState
243243
bindRuleSet(d, "inReachableStateImplication",
@@ -268,7 +268,7 @@ private RuleSetDispatchFeature setupCostComputationF() {
268268
bindRuleSet(d, "auto_induction_lemma", inftyConst());
269269
}
270270

271-
bindRuleSet(d, "information_flow_contract_appl", longConst(CostBand.LAST_RESORT.cost()));
271+
bindRuleSet(d, "information_flow_contract_appl", CostBand.LAST_RESORT.cost());
272272

273273
if (strategyProperties.contains(StrategyProperties.AUTO_INDUCTION_ON)
274274
|| strategyProperties.contains(StrategyProperties.AUTO_INDUCTION_LEMMA_ON)) {

‎key.core/src/main/java/de/uka/ilkd/key/strategy/StringStrategy.java‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -104,20 +104,20 @@ private void setUpStringNormalisation(RuleSetDispatchFeature d) {
104104
bindRuleSet(d, "defOpsSeqEquality",
105105
add(NonDuplicateAppModPositionFeature.INSTANCE,
106106
ifZero(add(applyTF("left", seqLiteral), applyTF("right", seqLiteral)),
107-
longConst(CostBand.DEFER.at(500)), inftyConst()),
107+
CostBand.DEFER.at(500), inftyConst()),
108108
belowModOpPenality));
109109

110110
bindRuleSet(d, "defOpsConcat",
111111
add(NonDuplicateAppModPositionFeature.INSTANCE,
112112
ifZero(
113113
or(applyTF("leftStr", not(seqLiteral)), applyTF("rightStr", not(seqLiteral))),
114-
longConst(CostBand.DEFER.at(500))
114+
CostBand.DEFER.at(500)
115115
// concat is often introduced for construction purposes,
116116
// we do not want to use its definition right at the
117117
// beginning
118118
), belowModOpPenality));
119119

120-
bindRuleSet(d, "stringsSimplify", longConst(CostBand.NORMALIZE.cost()));
120+
bindRuleSet(d, "stringsSimplify", CostBand.NORMALIZE.cost());
121121

122122
final TermFeature charOrIntLiteral = or(tf.charLiteral, tf.literal,
123123
or(add(OperatorClassTF.create(ParametricFunctionInstance.class), // XXX:
@@ -131,36 +131,36 @@ private void setUpStringNormalisation(RuleSetDispatchFeature d) {
131131

132132
bindRuleSet(d, "defOpsReplace", add(NonDuplicateAppModPositionFeature.INSTANCE,
133133
ifZero(or(applyTF("str", not(seqLiteral)), applyTF("searchChar", not(charOrIntLiteral)),
134-
applyTF("replChar", not(charOrIntLiteral))), longConst(CostBand.DEFER.cost()),
134+
applyTF("replChar", not(charOrIntLiteral))), CostBand.DEFER.cost(),
135135
inftyConst()),
136136
belowModOpPenality));
137137

138138
bindRuleSet(d, "stringsReduceSubstring",
139-
add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(CostBand.DEFER.at(-400))));
139+
add(NonDuplicateAppModPositionFeature.INSTANCE, CostBand.DEFER.at(-400)));
140140

141-
bindRuleSet(d, "defOpsStartsEndsWith", longConst(CostBand.DEFER.at(-250)));
141+
bindRuleSet(d, "defOpsStartsEndsWith", CostBand.DEFER.at(-250));
142142

143143
bindRuleSet(d, "stringsConcatNotBothLiterals",
144144
ifZero(MatchedAssumesFeature.INSTANCE, ifZero(
145145
add(applyTF(instOf("leftStr"), seqLiteral),
146146
applyTF(instOf("rightStr"), seqLiteral)),
147147
inftyConst()), inftyConst()));
148148

149-
bindRuleSet(d, "stringsReduceConcat", longConst(CostBand.DEFER.at(-400)));
149+
bindRuleSet(d, "stringsReduceConcat", CostBand.DEFER.at(-400));
150150

151151
bindRuleSet(d, "stringsReduceOrMoveOutsideConcat",
152-
ifZero(NonDuplicateAppModPositionFeature.INSTANCE, longConst(CostBand.DEFER.at(300)),
152+
ifZero(NonDuplicateAppModPositionFeature.INSTANCE, CostBand.DEFER.at(300),
153153
inftyConst()));
154154

155155
bindRuleSet(d, "stringsMoveReplaceInside",
156-
ifZero(NonDuplicateAppModPositionFeature.INSTANCE, longConst(CostBand.DEFER.at(-100)),
156+
ifZero(NonDuplicateAppModPositionFeature.INSTANCE, CostBand.DEFER.at(-100),
157157
inftyConst()));
158158

159159

160-
bindRuleSet(d, "stringsExpandDefNormalOp", longConst(CostBand.DEFER.cost()));
160+
bindRuleSet(d, "stringsExpandDefNormalOp", CostBand.DEFER.cost());
161161

162162
bindRuleSet(d, "stringsContainsDefInline", SumFeature
163-
.createSum(EqNonDuplicateAppFeature.INSTANCE, longConst(CostBand.DEFER.at(500))));
163+
.createSum(EqNonDuplicateAppFeature.INSTANCE, CostBand.DEFER.at(500)));
164164
}
165165

166166
@Override

0 commit comments

Comments
 (0)