From 7885fbe789e4327ae7135d026b5e58ed1708315b Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 7 Jul 2026 21:24:31 +0200 Subject: [PATCH 01/10] Step 2 (checkpoint): FOLStrategy costs via CostBand + FOLCost Introduce CostBand (ncore, the shared cross-theory cost-band vocabulary) and FOLCost (FOL-theory-internal ordering constants), and convert FOLStrategy's cost literals to them - byte-identical by construction. Deferred: RAP + Model-Search node-for-node verification (holding proof runs for a benchmark). Checkpoint before the Integer conversion so the two theory changes stay separable for bisection if verification later flags a mismatch. Created with AI tooling support # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java --- .../de/uka/ilkd/key/strategy/FOLCost.java | 63 +++++++++ .../de/uka/ilkd/key/strategy/FOLStrategy.java | 128 ++++++++++-------- .../prover/strategy/costbased/CostBand.java | 98 ++++++++++++++ 3 files changed, 235 insertions(+), 54 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/strategy/FOLCost.java create mode 100644 key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/CostBand.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLCost.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLCost.java new file mode 100644 index 00000000000..af0c819f56d --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLCost.java @@ -0,0 +1,63 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.strategy; + +/** + * FOL-theory-internal ordering costs, used by {@link FOLStrategy}. These are the fine, within-FOL + * ordering values that are reused across FOLStrategy's normalisation / splitting / + * equation methods and therefore deserve a name of their own; genuinely one-off nudges are written + * directly as {@code CostBand..at(delta)} at the call site instead. + * + *

+ * Values are byte-identical to the literals they replace. They position FOL rules within the shared + * {@link org.key_project.prover.strategy.costbased.CostBand} ladder, so changing one shifts the + * cross-theory search — verify with a full runAllProofs and a Model-Search node-for-node comparison + * (as for {@code CostBand}). + *

+ */ +final class FOLCost { + private FOLCost() {} + + /** + * Base cost of applying an equation (applyEq / apply_equations). Deliberately its own band — + * not {@code EXECUTE}, which is reserved for symbolic execution. + */ + static final long APPLY_EQUATIONS = -4000; + + /** + * Distribution / swapping of quantifiers ({@code distrQuantifier}, {@code swapQuantifiers}). + */ + static final long QUANTIFIER_DISTRIBUTION = -300; + + /** + * Restructuring of CNF clauses by associativity / distribution ({@code cnf_orAssoc}, + * {@code cnf_andAssoc}, {@code cnf_dist}); the small {@code ± delta} at the call sites orders + * these among themselves. + */ + static final long CNF_RESTRUCTURE = -35; + + /** + * Ordering of formula-normalisation steps in the boolean/CNF area, at one shared priority: + * {@code conjNormalForm} (CNF conversion) and {@code apply_equations_andOr} (contextual + * equation application inside and/or). + */ + static final long CNF_ORDERING = -150; + + /** + * Defer {@code replace_known_right} when its target is in the consequent of an implication or + * inside an equivalence, so the connective is decomposed first (which makes the antecedent + * available as a known-true fact). Deliberately not applied to + * {@code replace_known_left}, whose antecedent-true facts stay valid across the decomposition. + */ + static final long REPLACE_KNOWN_UNDER_CONNECTIVE = 100; + + /** Standard cost of a direct cut ({@code cut_direct}). */ + static final long CUT_DIRECT_STANDARD = 100; + + /** Preferred direction of the {@code pullOutQuantifier*} rules. */ + static final long PULL_OUT_QUANTIFIER = -20; + + /** Dispreferred direction of the {@code pullOutQuantifier*} rules. */ + static final long PULL_OUT_QUANTIFIER_REVERSE = -40; +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java index c4cda4a412e..a8bccf5aebc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java @@ -31,6 +31,7 @@ import org.key_project.prover.rules.RuleApp; import org.key_project.prover.rules.RuleSet; import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.prover.strategy.costbased.CostBand; import org.key_project.prover.strategy.costbased.MutableState; import org.key_project.prover.strategy.costbased.RuleAppCost; import org.key_project.prover.strategy.costbased.TopRuleAppCost; @@ -82,7 +83,7 @@ public FOLStrategy(Proof proof, StrategyProperties strategyProperties) { private Feature setUpGlobalF(RuleSetDispatchFeature d) { final Feature oneStepSimplificationF = - oneStepSimplificationFeature(longConst(-11000)); + oneStepSimplificationFeature(longConst(CostBand.REWRITE.cost())); return add(d, oneStepSimplificationF); } @@ -95,20 +96,20 @@ private Feature oneStepSimplificationFeature(Feature cost) { private RuleSetDispatchFeature setupCostComputationF() { final RuleSetDispatchFeature d = new RuleSetDispatchFeature(); - bindRuleSet(d, "closure", -15000); - bindRuleSet(d, "alpha", -7000); - bindRuleSet(d, "delta", -6000); - bindRuleSet(d, "simplify_boolean", -200); + bindRuleSet(d, "closure", CostBand.CLOSE.cost()); + bindRuleSet(d, "alpha", CostBand.DECOMPOSE.cost()); + bindRuleSet(d, "delta", CostBand.TYPE.cost()); + bindRuleSet(d, "simplify_boolean", CostBand.PREFER.at(300)); final Feature findDepthFeature = FindDepthFeature.getInstance(); bindRuleSet(d, "concrete", - add(longConst(-11000), + add(longConst(CostBand.REWRITE.cost()), ScaleFeature.createScaled(findDepthFeature, 10.0))); - bindRuleSet(d, "simplify", -4500); - bindRuleSet(d, "simplify_enlarging", -2000); - bindRuleSet(d, "simplify_ENLARGING", -1900); + bindRuleSet(d, "simplify", CostBand.SIMPLIFY.cost()); + bindRuleSet(d, "simplify_enlarging", CostBand.ENLARGE.cost()); + bindRuleSet(d, "simplify_ENLARGING", CostBand.ENLARGE.at(100)); // always give infinite cost to obsolete rules bindRuleSet(d, "obsolete", inftyConst()); @@ -120,46 +121,54 @@ private RuleSetDispatchFeature setupCostComputationF() { not(contains(AssumptionProjection.create(0), FocusProjection.INSTANCE)))); bindRuleSet(d, "update_elim", - add(longConst(-8000), ScaleFeature.createScaled(findDepthFeature, 10.0))); + add(longConst(CostBand.ELIMINATE.cost()), + ScaleFeature.createScaled(findDepthFeature, 10.0))); bindRuleSet(d, "update_apply_on_update", - add(longConst(-7000), ScaleFeature.createScaled(findDepthFeature, 10.0))); - bindRuleSet(d, "update_join", -4600); - bindRuleSet(d, "update_apply", -4500); + add(longConst(CostBand.DECOMPOSE.cost()), + ScaleFeature.createScaled(findDepthFeature, 10.0))); + bindRuleSet(d, "update_join", CostBand.SIMPLIFY.at(-100)); + bindRuleSet(d, "update_apply", CostBand.SIMPLIFY.cost()); setupSplitting(d); bindRuleSet(d, "gamma", add(not(isInstantiated("t")), - ifZero(allowQuantifierSplitting(), longConst(0), longConst(50)))); + ifZero(allowQuantifierSplitting(), longConst(CostBand.DEFAULT.cost()), + longConst(CostBand.DEFAULT.at(50))))); bindRuleSet(d, "gamma_destructive", inftyConst()); - bindRuleSet(d, "triggered", add(not(isTriggerVariableInstantiated()), longConst(500))); + bindRuleSet(d, "triggered", + add(not(isTriggerVariableInstantiated()), longConst(CostBand.DEFER.cost()))); bindRuleSet(d, "comprehension_split", add(applyTF(FocusFormulaProjection.INSTANCE, ff.notContainsExecutable), - ifZero(allowQuantifierSplitting(), longConst(2500), longConst(5000)))); + ifZero(allowQuantifierSplitting(), longConst(CostBand.DEFER.at(2000)), + longConst(CostBand.DEFER.at(4500))))); setupReplaceKnown(d); setupEquationReasoning(d); bindRuleSet(d, "order_terms", - add(termSmallerThan("commEqLeft", "commEqRight"), longConst(-5000))); + add(termSmallerThan("commEqLeft", "commEqRight"), + longConst(CostBand.NORMALIZE.cost()))); bindRuleSet(d, "simplify_instanceof_static", - add(EqNonDuplicateAppFeature.INSTANCE, longConst(-500))); + add(EqNonDuplicateAppFeature.INSTANCE, longConst(CostBand.PREFER.cost()))); - bindRuleSet(d, "evaluate_instanceof", longConst(-500)); + bindRuleSet(d, "evaluate_instanceof", longConst(CostBand.PREFER.cost())); bindRuleSet(d, "instanceof_to_exists", TopLevelFindFeature.ANTEC); bindRuleSet(d, "try_apply_subst", - add(EqNonDuplicateAppFeature.INSTANCE, longConst(-10000))); + add(EqNonDuplicateAppFeature.INSTANCE, longConst(CostBand.SUBST.cost()))); // delete cast bindRuleSet(d, "cast_deletion", - ifZero(implicitCastNecessary(instOf("castedTerm")), longConst(-5000), inftyConst())); + ifZero(implicitCastNecessary(instOf("castedTerm")), + longConst(CostBand.NORMALIZE.cost()), + inftyConst())); - bindRuleSet(d, "type_hierarchy_def", -6500); + bindRuleSet(d, "type_hierarchy_def", CostBand.TYPE.at(-500)); bindRuleSet(d, "cut", not(isInstantiated("cutFormula"))); @@ -280,28 +289,28 @@ public Name name() { protected void setupFormulaNormalisation(RuleSetDispatchFeature d) { bindRuleSet(d, "negationNormalForm", add(BelowBinderFeature.getInstance(), - longConst(-500), + longConst(CostBand.PREFER.cost()), ScaleFeature.createScaled(FindDepthFeature.getInstance(), 10.0))); bindRuleSet(d, "moveQuantToLeft", - add(quantifiersMightSplit() ? longConst(0) + add(quantifiersMightSplit() ? longConst(CostBand.DEFAULT.cost()) : applyTF(FocusFormulaProjection.INSTANCE, ff.quantifiedPureLitConjDisj), - longConst(-550))); + longConst(CostBand.PREFER.at(-50)))); bindRuleSet(d, "conjNormalForm", ifZero( add(or(FocusInAntecFeature.getInstance(), notBelowQuantifier()), NotInScopeOfModalityFeature.INSTANCE), - add(longConst(-150), + add(longConst(FOLCost.CNF_ORDERING), ScaleFeature.createScaled(FindDepthFeature.getInstance(), 20)), inftyConst())); - bindRuleSet(d, "setEqualityBlastingRight", longConst(-100)); + bindRuleSet(d, "setEqualityBlastingRight", longConst(CostBand.DEFAULT.at(-100))); - bindRuleSet(d, "elimQuantifier", -1000); - bindRuleSet(d, "elimQuantifierWithCast", 50); + bindRuleSet(d, "elimQuantifier", CostBand.PREFER.at(-500)); + bindRuleSet(d, "elimQuantifierWithCast", CostBand.DEFAULT.at(50)); final TermBuffer left = new TermBuffer(); final TermBuffer right = new TermBuffer(); @@ -309,7 +318,7 @@ protected void setupFormulaNormalisation(RuleSetDispatchFeature d) { add(let(left, instOf("applyEqLeft"), let(right, instOf("applyEqRight"), TermSmallerThanFeature.create(right, left))), - longConst(-150))); + longConst(FOLCost.CNF_ORDERING))); bindRuleSet(d, "distrQuantifier", add(or( @@ -321,28 +330,30 @@ protected void setupFormulaNormalisation(RuleSetDispatchFeature d) { ifZero(FocusInAntecFeature.getInstance(), applyTF(FocusProjection.INSTANCE, sub(ff.andF)), applyTF(FocusProjection.INSTANCE, sub(ff.orF))))), - longConst(-300))); + longConst(FOLCost.QUANTIFIER_DISTRIBUTION))); bindRuleSet(d, "swapQuantifiers", add(applyTF(FocusProjection.INSTANCE, add(ff.quantifiedClauseSet, EliminableQuantifierTF.INSTANCE, sub(not(EliminableQuantifierTF.INSTANCE)))), - longConst(-300))); + longConst(FOLCost.QUANTIFIER_DISTRIBUTION))); // category "conjunctive normal form" bindRuleSet(d, "cnf_orAssoc", SumFeature.createSum(applyTF("assoc0", ff.clause), - applyTF("assoc1", ff.clause), applyTF("assoc2", ff.literal), longConst(-80))); + applyTF("assoc1", ff.clause), applyTF("assoc2", ff.literal), + longConst(FOLCost.CNF_RESTRUCTURE - 45))); bindRuleSet(d, "cnf_andAssoc", SumFeature.createSum(applyTF("assoc0", ff.clauseSet), - applyTF("assoc1", ff.clauseSet), applyTF("assoc2", ff.clause), longConst(-10))); + applyTF("assoc1", ff.clauseSet), applyTF("assoc2", ff.clause), + longConst(FOLCost.CNF_RESTRUCTURE + 25))); bindRuleSet(d, "cnf_dist", SumFeature.createSum(applyTF("distRight0", ff.clauseSet), applyTF("distRight1", ff.clauseSet), ifZero(applyTF("distLeft", ff.clause), - longConst(-15), applyTF("distLeft", ff.clauseSet)), - longConst(-35))); + longConst(FOLCost.CNF_RESTRUCTURE + 20), applyTF("distLeft", ff.clauseSet)), + longConst(FOLCost.CNF_RESTRUCTURE))); final TermBuffer superFor = new TermBuffer(); final Feature onlyBelowQuanAndOr = @@ -364,13 +375,16 @@ EliminableQuantifierTF.INSTANCE, sub(not(EliminableQuantifierTF.INSTANCE)))), add(isBelow(OperatorClassTF.create(Quantifier.class)), onlyBelowQuanAndOr, applyTF( FocusProjection.create(0), sub(ff.quantifiedClauseSet, ff.quantifiedClauseSet))); - bindRuleSet(d, "pullOutQuantifierUnifying", -20); + bindRuleSet(d, "pullOutQuantifierUnifying", FOLCost.PULL_OUT_QUANTIFIER); bindRuleSet(d, "pullOutQuantifierAll", add(pullOutQuantifierAllowed, - ifZero(FocusInAntecFeature.getInstance(), longConst(-20), longConst(-40)))); + ifZero(FocusInAntecFeature.getInstance(), longConst(FOLCost.PULL_OUT_QUANTIFIER), + longConst(FOLCost.PULL_OUT_QUANTIFIER_REVERSE)))); bindRuleSet(d, "pullOutQuantifierEx", add(pullOutQuantifierAllowed, - ifZero(FocusInAntecFeature.getInstance(), longConst(-40), longConst(-20)))); + ifZero(FocusInAntecFeature.getInstance(), + longConst(FOLCost.PULL_OUT_QUANTIFIER_REVERSE), + longConst(FOLCost.PULL_OUT_QUANTIFIER)))); } // ////////////////////////////////////////////////////////////////////////// @@ -396,17 +410,18 @@ private void setupQuantifierInstantiation(RuleSetDispatchFeature d) { : ff.notContainsExecutable)), forEach(varInst, HeuristicInstantiation.forOption(classicTriggers()), add(instantiate("t", varInst), - add(branchPrediction, longConst(10), + add(branchPrediction, + longConst(CostBand.DEFAULT.at(10), // orders candidates of one predicted-cost band by their // connection to the sequent instead of formula position InstantiationTieBreakFeature.create(varInst, - triggersOption())))))); + triggersOption()))))))); final TermBuffer splitInst = new TermBuffer(); bindRuleSet(d, "triggered", SumFeature.createSum(forEach(splitInst, TriggeredInstantiations.create(true), - add(instantiateTriggeredVariable(splitInst), longConst(500))), - longConst(1500))); + add(instantiateTriggeredVariable(splitInst), longConst(CostBand.DEFER.cost()))), + longConst(CostBand.DEFER.at(1000)))); } else { bindRuleSet(d, "gamma", inftyConst()); @@ -423,7 +438,7 @@ private void setupQuantifierInstantiationApproval(RuleSetDispatchFeature d) { not(eq(instOf("t"), varInst)))), InstantiationCostScalerFeature.create( InstantiationCost.create(instOf("t"), classicTriggers()), - longConst(0)))); + longConst(CostBand.DEFAULT.cost())))); final TermBuffer splitInst = new TermBuffer(); bindRuleSet(d, "triggered", @@ -453,15 +468,18 @@ protected Feature notBelowQuantifier() { private void setupReplaceKnown(RuleSetDispatchFeature d) { final Feature commonF = add(ifZero(MatchedAssumesFeature.INSTANCE, DiffFindAndIfFeature.INSTANCE), - longConst(-5000), + longConst(CostBand.NORMALIZE.cost()), add(DiffFindAndReplacewithFeature.INSTANCE, ScaleFeature.createScaled(CountMaxDPathFeature.INSTANCE, 10.0))); bindRuleSet(d, "replace_known_left", commonF); bindRuleSet(d, "replace_known_right", - add(commonF, ifZero(directlyBelowSymbolAtIndex(Junctor.IMP, 1), longConst(100), - ifZero(directlyBelowSymbolAtIndex(Equality.EQV, -1), longConst(100))))); + add(commonF, + ifZero(directlyBelowSymbolAtIndex(Junctor.IMP, 1), + longConst(FOLCost.REPLACE_KNOWN_UNDER_CONNECTIVE), + ifZero(directlyBelowSymbolAtIndex(Equality.EQV, -1), + longConst(FOLCost.REPLACE_KNOWN_UNDER_CONNECTIVE))))); } // ////////////////////////////////////////////////////////////////////////// @@ -478,9 +496,10 @@ protected void setupSplitting(RuleSetDispatchFeature d) { sum(subFor, AllowedCutPositionsGenerator.INSTANCE, not(applyTF(subFor, ff.cutAllowed))); bindRuleSet(d, "beta", SumFeature.createSum(noCutsAllowed, - ifZero(PurePosDPathFeature.INSTANCE, longConst(-200)), + ifZero(PurePosDPathFeature.INSTANCE, longConst(CostBand.PREFER.at(300))), ScaleFeature.createScaled(CountPosDPathFeature.INSTANCE, -3.0), - ScaleFeature.createScaled(CountMaxDPathFeature.INSTANCE, 10.0), longConst(20))); + ScaleFeature.createScaled(CountMaxDPathFeature.INSTANCE, 10.0), + longConst(CostBand.DEFAULT.at(20)))); TermBuffer superF = new TermBuffer(); final ProjectionToTerm splitCondition = sub(FocusProjection.INSTANCE, 0); bindRuleSet(d, "split_cond", add(// do not split over formulas containing auxiliary @@ -496,7 +515,7 @@ protected void setupSplitting(RuleSetDispatchFeature d) { sum(superF, SuperTermGenerator.upwards(any(), getServices()), applyTF(superF, not(ff.elemUpdate))), ifZero(applyTF(FocusProjection.INSTANCE, ContainsExecutableCodeTermFeature.PROGRAMS), - longConst(-100), longConst(25)))); + longConst(CostBand.DEFAULT.at(-100)), longConst(CostBand.DEFAULT.at(25))))); ProjectionToTerm cutFormula = instOf("cutFormula"); Feature countOccurrencesInSeq = ScaleFeature.createAffine(countOccurrences(cutFormula), -10, 10); @@ -512,13 +531,14 @@ protected void setupSplitting(RuleSetDispatchFeature d) { // auxiliary variables rec(any(), not(selectSkolemConstantTermFeature())))), countOccurrencesInSeq, // standard costs - longConst(100)), + longConst(FOLCost.CUT_DIRECT_STANDARD)), SumFeature // check for cuts below quantifiers .createSum(applyTF(cutFormula, ff.cutAllowedBelowQuantifier), applyTF(FocusFormulaProjection.INSTANCE, ff.quantifiedClauseSet), - ifZero(allowQuantifierSplitting(), longConst(0), - longConst(100)))))); + ifZero(allowQuantifierSplitting(), + longConst(CostBand.DEFAULT.cost()), + longConst(FOLCost.CUT_DIRECT_STANDARD)))))); } private void setupSplittingApproval(RuleSetDispatchFeature d) { @@ -567,7 +587,7 @@ private void setupEquationReasoning(RuleSetDispatchFeature d) { let(left, sub(equation, 0), let(right, sub(equation, 1), TermSmallerThanFeature.create(right, left))))))), - longConst(-4000))); + longConst(FOLCost.APPLY_EQUATIONS))); bindRuleSet(d, "insert_eq_nonrigid", applyTF(FocusProjection.create(0), IsNonRigidTermFeature.INSTANCE)); diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/CostBand.java b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/CostBand.java new file mode 100644 index 00000000000..dfbe711c025 --- /dev/null +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/CostBand.java @@ -0,0 +1,98 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.prover.strategy.costbased; + +/** + * The shared, cross-theory priority ladder for the cost-based strategies. + * + *

+ * Rule costs from every component strategy (theory) are summed per rule and the globally + * cheapest applicable rule is applied, so a band's absolute value fixes its priority + * against every other theory — in practice the theories interleave at almost every + * step. A band is therefore combination-relevant. The fine ordering of rules within a + * band is expressed as {@code TIER.at(delta)} with a small delta; ordering that is internal to a + * single theory lives in that theory (e.g. {@code IntegerCost} for the integer (in)equality and + * division solver steps), not here. + *

+ * + *

+ * Care when changing: altering a band's value, or its order relative to other bands, + * shifts the cross-theory search of all proofs — always re-verify with a full + * runAllProofs and a Model-Search node-for-node comparison. Respect the hard ordering + * constraints noted on individual bands (notably {@link #BLOCK_CONTRACT}). + *

+ */ +public enum CostBand { + /** + * Apply a block/loop contract instead of executing the block. MUST stay more eager (smaller) + * than {@link #REWRITE} and every symbolic-execution program rule, otherwise the block starts + * to execute instead of being contracted. Value is the current sentinel; step 3 normalizes it + * to a modest value between {@link #CLOSE} and {@link #REWRITE}. + */ + BLOCK_CONTRACT(Long.MIN_VALUE), + /** + * Apply a loop invariant instead of unrolling. Only needs to beat loop-unrolling / method + * expansion when enabled. (Currently above {@link #CLOSE}; step 3 flips it below CLOSE.) + */ + LOOP_INVARIANT(-20_000), + /** + * Close the goal. Most eager of the ordinary bands: eager closure is completeness-neutral + * (no free-variable calculus), so closing may always take precedence. + */ + CLOSE(-15_000), + /** One-Step-Simplification and decidable ground rewrites (rule set {@code concrete}). */ + REWRITE(-11_000), + /** Force a pending substitution / eager equality ({@code try_apply_subst}). */ + SUBST(-10_000), + /** Eliminate updates and literals. */ + ELIMINATE(-8_000), + /** Non-splitting sequent decomposition (alpha rules, update-apply-on-update). */ + DECOMPOSE(-7_000), + /** Type reasoning (delta rules, type hierarchy). */ + TYPE(-6_000), + /** Canonicalize / order / commute terms. */ + NORMALIZE(-5_000), + /** Safe, size-reducing definitional simplification and symbolic-execution steps. */ + SIMPLIFY(-4_500), + /** Symbolic-execution program step / state merge. */ + EXECUTE(-4_000), + /** Solve direct (in)equations; apply query axioms. */ + SOLVE(-3_000), + /** Useful but size-increasing simplification (e.g. comprehension / map unfolding). */ + ENLARGE(-2_000), + /** Minor local structural preference. */ + PREFER(-500), + /** + * The default cost. A taclet whose rule sets carry no explicit feature in a strategy already + * contributes 0 (the dispatcher sums only the bound rule sets), so binding a rule set to + * DEFAULT is a deliberate "no strategic bias — apply in due (age) order", cost-identical to + * leaving it unbound. + */ + DEFAULT(0), + /** Defer: lazy definitional unfolding, applied only when needed. */ + DEFER(500), + /** Strongly defer. */ + DEFER_STRONG(10_000), + /** Finite last resort — reachable, but only when nothing else applies (soft infinity). */ + LAST_RESORT(1_000_000); + + private final long base; + + CostBand(long base) { + this.base = base; + } + + /** The band's cost. */ + public long cost() { + return base; + } + + /** + * The band's cost shifted by a small theory-internal ordering delta. Use only for fine + * ordering within the band; larger, cross-theory steps deserve their own band. + */ + public long at(long delta) { + return base + delta; + } +} From 0bc232d90a5cabf0b5fa08e0450f364837b10b4c Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 7 Jul 2026 22:59:13 +0200 Subject: [PATCH 02/10] Step 2 (checkpoint): IntegerStrategy costs via CostBand + IntegerArithmeticCosts Convert IntegerStrategy's ~50 cost literals to the shared CostBand ladder (anchors) and to per-sub-theory holders in IntegerArithmeticCosts (PolynomialCost / LinearEquationCost / LinearInequationCost / NonlinearArithmeticCost / DivModCost), grouped to anticipate a future split of the strategy. Byte-identical by construction; the old IN_EQ_SIMP_NON_LIN_COST / POLY_DIVISION_COST fields move into the holders. Deferred: RAP + Model-Search node-for-node verification (holding proof runs for a benchmark). Checkpoint after FOL (21a475ebb9) so the two theory conversions stay bisectable. Created with AI tooling support --- .../key/strategy/IntegerArithmeticCosts.java | 125 ++++++++++++++++ .../ilkd/key/strategy/IntegerStrategy.java | 139 ++++++++++-------- 2 files changed, 200 insertions(+), 64 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerArithmeticCosts.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerArithmeticCosts.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerArithmeticCosts.java new file mode 100644 index 00000000000..1c34f5b58b0 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerArithmeticCosts.java @@ -0,0 +1,125 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.strategy; + +/* + * Theory-internal cost constants for the integer arithmetic strategy, grouped by the arithmetic + * sub-theory they belong to. The grouping deliberately anticipates a future split of + * IntegerStrategy into separate sub-strategies (polynomial / linear / non-linear / div-mod): each + * holder is meant to move with its sub-strategy. Cross-theory levels stay in + * {@link org.key_project.prover.strategy.costbased.CostBand}; only the arithmetic-internal ordering + * lives here. All values are byte-identical to the literals they replace. + */ + +/** Polynomial normal-form canonicalisation (Buchberger normalisation) — the "basic" substrate. */ +final class PolynomialCost { + private PolynomialCost() {} + + /** elimSubNeg, homo, pullOutFactor, elimOneLeft/Right. */ + static final long EXPAND = -120; + static final long MUL_ORDER = -100; + static final long MUL_ASSOC = -80; + static final long ADD_ORDER = -60; + static final long ADD_ASSOC = -10; + /** polySimp_dist base; the distLeft sub-case is {@code DISTRIBUTE + 20}. */ + static final long DISTRIBUTE = -35; + static final long PULLOUT_GCD = -2250; +} + + +/** + * Polynomial equation solving (Gaussian / Gröbner). These {@code polySimp_*} rule sets + * live + * here rather than in {@link PolynomialCost} on purpose: they do not just canonicalise a term, they + * derive from and apply equations, so they belong to the "linear" (solving) layer next to + * {@link LinearInequationCost}. + */ +final class LinearEquationCost { + private LinearEquationCost() {} + + /** + * The general {@code apply_equations} rule set (applyEq / applyEqReverse), used to reduce + * polynomials. Distinct from {@link #APPLY_EQ}, which is the monomial-specialised polySimp + * variant. Its own band, not {@code EXECUTE} (reserved for symbolic execution). + *

+ * Step-3 idea: test whether the specialised {@link #APPLY_EQ} is needed at all, or should just + * be a small delta that prefers these original {@code apply_equations} rules. + *

+ */ + static final long APPLY_EQUATIONS = -4000; + static final long APPLY_EQ_AND_OR = -150; + /** polySimp_balance, polySimp_normalise. */ + static final long BALANCE = -30; + /** + * polySimp_applyEq — the monomial-coefficient-specialised equation application. The rigid + * variant polySimp_applyEqRigid is written {@code APPLY_EQ + 1} at the call site; that +1 is + * only an (uninteresting) tie-break between the two rules, a step-3 candidate to flatten to a + * single cost. + */ + static final long APPLY_EQ = 1; +} + + +/** Linear inequation solving — the Omega / Fourier-Motzkin machinery ({@code inEqSimp_*}). */ +final class LinearInequationCost { + private LinearInequationCost() {} + + static final long PROPAGATION = -2400; + static final long SATURATE = -1900; + /** General GCD normalisation of inequations — confluent, hence safe to apply eagerly. */ + static final long PULLOUT_GCD_CONFLUENT = -2150; + static final long FOR_NORMALISATION = -1100; + static final long MOVE_LEFT = -90; + static final long MAKE_NON_STRICT = -80; + static final long CONTRAD = -60; + static final long COMMUTE = -40; + static final long STRENGTHEN = -30; + static final long ANTISYMM = -20; + /** + * Faster antecedent-specialised GCD pull-out, but not confluent (the result can depend + * on application order), hence pinned near baseline so it fires only opportunistically — in + * contrast to the eager {@link #PULLOUT_GCD_CONFLUENT}. + */ + static final long PULLOUT_GCD_ANTEC_NONCONFLUENT = -10; +} + + +/** Non-linear arithmetic — cross-multiplication, sign cases, root inferences (Model Search). */ +final class NonlinearArithmeticCost { + private NonlinearArithmeticCost() {} + + /** + * inEqSimp_nonLin (cross-multiplication) base; case-distinction offsets are + * {@code MULTIPLY + n}. + */ + static final long MULTIPLY = 1000; + /** + * Divide an inequation by a factor of known sign/bound to bound the quotient (the + * {@code divide_inEq*} taclets) — the inverse of cross-multiplication. Kept clearly more eager + * than {@link #MULTIPLY}, since dividing/reducing is safer and more productive than + * multiplying. + */ + static final long DIVIDE_INEQUATION = -1400; + static final long SPLIT_EQ = -100; +} + + +/** Division / modulo and DefOps expansion ({@code polyDivision}, {@code defOps_*}). */ +final class DivModCost { + private DivModCost() {} + + static final long POLY_DIVISION = -2250; + static final long EXPAND_MODULO = -600; + /** extra cost for defOps_div/jdiv applied below a modality. */ + static final long BELOW_MODALITY = 200; + static final long EXPAND_RANGES = -8000; + static final long MOD_HOMO_EQ = -5000; + static final long EXPAND_NUMERIC_OP = -500; + /** defOps_jdiv_inline for a literal numerator (eager, concrete division). */ + static final long INLINE = -5000; + /** literal-only division / modulo (defOps_mod, off-mode jdiv_inline). */ + static final long MOD = -4000; + /** modulo expansion for a polynomial (non-literal) modulus (defOps_mod). */ + static final long MOD_EXPAND = -3500; +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java index 4896a823ea5..02a3f9ef118 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java @@ -26,6 +26,7 @@ import org.key_project.prover.rules.RuleApp; import org.key_project.prover.rules.RuleSet; import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.prover.strategy.costbased.CostBand; import org.key_project.prover.strategy.costbased.MutableState; import org.key_project.prover.strategy.costbased.RuleAppCost; import org.key_project.prover.strategy.costbased.TopRuleAppCost; @@ -205,7 +206,8 @@ private RuleSetDispatchFeature setupCostComputationF() { bindRuleSet(d, "order_terms", add(applyTF("commEqRight", tf.monomial), applyTF("commEqLeft", tf.polynomial), - monSmallerThan("commEqLeft", "commEqRight", numbers), longConst(-5000))); + monSmallerThan("commEqLeft", "commEqRight", numbers), + longConst(CostBand.NORMALIZE.cost()))); final TermBuffer equation = new TermBuffer(); final TermBuffer left = new TermBuffer(); @@ -228,7 +230,7 @@ private RuleSetDispatchFeature setupCostComputationF() { applyTF(right, tf.polynomial), MonomialsSmallerThanFeature.create(right, left, numbers)))))))), - longConst(-4000))); + longConst(LinearEquationCost.APPLY_EQUATIONS))); final TermBuffer l = new TermBuffer(); final TermBuffer r = new TermBuffer(); @@ -237,7 +239,7 @@ private RuleSetDispatchFeature setupCostComputationF() { let(r, instOf("applyEqRight"), add(applyTF(l, tf.nonNegOrNonCoeffMonomial), applyTF(r, tf.polynomial), MonomialsSmallerThanFeature.create(r, l, numbers)))), - longConst(-150))); + longConst(LinearEquationCost.APPLY_EQ_AND_OR))); // For taclets that need instantiation, but where the instantiation is // deterministic and does not have to be repeated at a later point, we @@ -270,79 +272,80 @@ private void setupArithPrimaryCategories(RuleSetDispatchFeature d) { // Buchberger's algorithmus for handling polynomial equations over // the integers - bindRuleSet(d, "polySimp_expand", -4500); - bindRuleSet(d, "polySimp_directEquations", -3000); - bindRuleSet(d, "polySimp_pullOutGcd", -2250); - bindRuleSet(d, "polySimp_leftNonUnit", -2000); - bindRuleSet(d, "polySimp_saturate", 0); + bindRuleSet(d, "polySimp_expand", CostBand.SIMPLIFY.cost()); + bindRuleSet(d, "polySimp_directEquations", CostBand.SOLVE.cost()); + bindRuleSet(d, "polySimp_pullOutGcd", PolynomialCost.PULLOUT_GCD); + bindRuleSet(d, "polySimp_leftNonUnit", CostBand.ENLARGE.cost()); + bindRuleSet(d, "polySimp_saturate", CostBand.DEFAULT.cost()); // Omega test for handling linear arithmetic and inequalities over the // integers; cross-multiplication + case distinctions for nonlinear // inequalities - bindRuleSet(d, "inEqSimp_expand", -4400); - bindRuleSet(d, "inEqSimp_directInEquations", -2900); - bindRuleSet(d, "inEqSimp_propagation", -2400); - bindRuleSet(d, "inEqSimp_pullOutGcd", -2150); - bindRuleSet(d, "inEqSimp_saturate", -1900); - bindRuleSet(d, "inEqSimp_forNormalisation", -1100); - bindRuleSet(d, "inEqSimp_special_nonLin", -1400); + bindRuleSet(d, "inEqSimp_expand", CostBand.SIMPLIFY.at(100)); + bindRuleSet(d, "inEqSimp_directInEquations", CostBand.SOLVE.at(100)); + bindRuleSet(d, "inEqSimp_propagation", LinearInequationCost.PROPAGATION); + bindRuleSet(d, "inEqSimp_pullOutGcd", LinearInequationCost.PULLOUT_GCD_CONFLUENT); + bindRuleSet(d, "inEqSimp_saturate", LinearInequationCost.SATURATE); + bindRuleSet(d, "inEqSimp_forNormalisation", LinearInequationCost.FOR_NORMALISATION); + bindRuleSet(d, "inEqSimp_special_nonLin", NonlinearArithmeticCost.DIVIDE_INEQUATION); if (arith == ArithTreatment.MODEL_SEARCH) { - bindRuleSet(d, "inEqSimp_nonLin", IN_EQ_SIMP_NON_LIN_COST); + bindRuleSet(d, "inEqSimp_nonLin", NonlinearArithmeticCost.MULTIPLY); } else { bindRuleSet(d, "inEqSimp_nonLin", inftyConst()); } - bindRuleSet(d, "polyDivision", POLY_DIVISION_COST); + bindRuleSet(d, "polyDivision", DivModCost.POLY_DIVISION); } private void setupPolySimp(RuleSetDispatchFeature d, IntegerLDT numbers) { // category "expansion" (normalising polynomial terms) - bindRuleSet(d, "polySimp_elimSubNeg", longConst(-120)); + bindRuleSet(d, "polySimp_elimSubNeg", longConst(PolynomialCost.EXPAND)); bindRuleSet(d, "polySimp_homo", add(applyTF("homoRight", add(not(tf.zeroLiteral), tf.polynomial)), or(applyTF("homoLeft", or(tf.addF, tf.negMonomial)), not(monSmallerThan("homoRight", "homoLeft", numbers))), - longConst(-120))); + longConst(PolynomialCost.EXPAND))); bindRuleSet(d, "polySimp_pullOutFactor", add(applyTFNonStrict("pullOutLeft", tf.literal), - applyTFNonStrict("pullOutRight", tf.literal), longConst(-120))); + applyTFNonStrict("pullOutRight", tf.literal), longConst(PolynomialCost.EXPAND))); - bindRuleSet(d, "polySimp_elimOneLeft", -120); + bindRuleSet(d, "polySimp_elimOneLeft", PolynomialCost.EXPAND); - bindRuleSet(d, "polySimp_elimOneRight", -120); + bindRuleSet(d, "polySimp_elimOneRight", PolynomialCost.EXPAND); bindRuleSet(d, "polySimp_mulOrder", add(applyTF("commRight", tf.monomial), or( applyTF("commLeft", tf.addF), add(applyTF("commLeft", tf.atom), atomSmallerThan("commLeft", "commRight", numbers))), - longConst(-100))); + longConst(PolynomialCost.MUL_ORDER))); bindRuleSet(d, "polySimp_mulAssoc", SumFeature.createSum(applyTF("mulAssocMono0", tf.monomial), applyTF("mulAssocMono1", tf.monomial), applyTF("mulAssocAtom", tf.atom), - longConst(-80))); + longConst(PolynomialCost.MUL_ASSOC))); bindRuleSet(d, "polySimp_addOrder", SumFeature.createSum(applyTF("commLeft", tf.monomial), applyTF("commRight", tf.polynomial), - monSmallerThan("commRight", "commLeft", numbers), longConst(-60))); + monSmallerThan("commRight", "commLeft", numbers), + longConst(PolynomialCost.ADD_ORDER))); bindRuleSet(d, "polySimp_addAssoc", SumFeature.createSum(applyTF("addAssocPoly0", tf.polynomial), applyTF("addAssocPoly1", tf.polynomial), applyTF("addAssocMono", tf.monomial), - longConst(-10))); + longConst(PolynomialCost.ADD_ASSOC))); bindRuleSet(d, "polySimp_dist", SumFeature.createSum(applyTF("distSummand0", tf.polynomial), applyTF("distSummand1", tf.polynomial), - ifZero(applyTF("distCoeff", tf.monomial), longConst(-15), + ifZero(applyTF("distCoeff", tf.monomial), longConst(PolynomialCost.DISTRIBUTE + 20), applyTF("distCoeff", tf.polynomial)), applyTF("distSummand0", tf.polynomial), - applyTF("distSummand1", tf.polynomial), longConst(-35))); + applyTF("distSummand1", tf.polynomial), longConst(PolynomialCost.DISTRIBUTE))); // category "direct equations" @@ -355,10 +358,10 @@ private void setupPolySimp(RuleSetDispatchFeature d, IntegerLDT numbers) { ifZero(isInstantiated("sepNegMono"), add(applyTF("sepNegMono", tf.negMonomial), monSmallerThan("sepResidue", "sepNegMono", numbers))), - longConst(-30))); + longConst(LinearEquationCost.BALANCE))); bindRuleSet(d, "polySimp_normalise", add(applyTF("invertRight", tf.zeroLiteral), - applyTF("invertLeft", tf.negMonomial), longConst(-30))); + applyTF("invertLeft", tf.negMonomial), longConst(LinearEquationCost.BALANCE))); // application of equations: some specialised rules that handle // monomials and their coefficients properly @@ -381,13 +384,15 @@ private void setupPolySimp(RuleSetDispatchFeature d, IntegerLDT numbers) { ifZero(MatchedAssumesFeature.INSTANCE, let(focus, FocusProjection.create(0), let(eqLeft, sub(AssumptionProjection.create(0), 0), validEqApplication)))); - bindRuleSet(d, "polySimp_applyEq", add(eqMonomialFeature, longConst(1))); + bindRuleSet(d, "polySimp_applyEq", + add(eqMonomialFeature, longConst(LinearEquationCost.APPLY_EQ))); - bindRuleSet(d, "polySimp_applyEqRigid", add(eqMonomialFeature, longConst(2))); + bindRuleSet(d, "polySimp_applyEqRigid", + add(eqMonomialFeature, longConst(LinearEquationCost.APPLY_EQ + 1))); // bindRuleSet(d, "defOps_expandModulo", - add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(-600))); + add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(DivModCost.EXPAND_MODULO))); // category "saturate" @@ -435,8 +440,8 @@ private void setupDivModDivision(RuleSetDispatchFeature d) { // no possible division has been found so far add(NotInScopeOfModalityFeature.INSTANCE, ifZero(isReduciblePolyE, // try again later - longConst(-POLY_DIVISION_COST)))))), - longConst(100))); + longConst(-DivModCost.POLY_DIVISION)))))), + longConst(CostBand.DEFAULT.at(100)))); } @@ -527,14 +532,15 @@ private void setupInEqSimp(RuleSetDispatchFeature d, IntegerLDT numbers) { // category "expansion" (normalising inequations) - bindRuleSet(d, "inEqSimp_moveLeft", -90); + bindRuleSet(d, "inEqSimp_moveLeft", LinearInequationCost.MOVE_LEFT); - bindRuleSet(d, "inEqSimp_makeNonStrict", -80); + bindRuleSet(d, "inEqSimp_makeNonStrict", LinearInequationCost.MAKE_NON_STRICT); bindRuleSet(d, "inEqSimp_commute", SumFeature.createSum(applyTF("commRight", tf.monomial), applyTF("commLeft", tf.polynomial), - monSmallerThan("commLeft", "commRight", numbers), longConst(-40))); + monSmallerThan("commLeft", "commRight", numbers), + longConst(LinearInequationCost.COMMUTE))); // this is copied from "polySimp_homo" bindRuleSet(d, "inEqSimp_homo", @@ -559,7 +565,7 @@ private void setupInEqSimp(RuleSetDispatchFeature d, IntegerLDT numbers) { // category "saturate" - bindRuleSet(d, "inEqSimp_antiSymm", longConst(-20)); + bindRuleSet(d, "inEqSimp_antiSymm", longConst(LinearInequationCost.ANTISYMM)); bindRuleSet(d, "inEqSimp_exactShadow", SumFeature.createSum(applyTF("esLeft", tf.nonCoeffMonomial), @@ -590,9 +596,9 @@ private void setupInEqSimp(RuleSetDispatchFeature d, IntegerLDT numbers) { SumFeature.createSum(applyTF("contradRightSmaller", tf.polynomial), applyTF("contradRightBigger", tf.polynomial), PolynomialValuesCmpFeature .lt(instOf("contradRightSmaller"), instOf("contradRightBigger")))), - longConst(-60))); + longConst(LinearInequationCost.CONTRAD))); - bindRuleSet(d, "inEqSimp_strengthen", longConst(-30)); + bindRuleSet(d, "inEqSimp_strengthen", longConst(LinearInequationCost.STRENGTHEN)); bindRuleSet(d, "inEqSimp_subsumption", add(applyTF("subsumLeft", tf.monomial), @@ -609,10 +615,11 @@ private void setupInEqSimp(RuleSetDispatchFeature d, IntegerLDT numbers) { // category "handling of non-linear inequations" if (arith == ArithTreatment.MODEL_SEARCH) { - setupMultiplyInequations(d, longConst(IN_EQ_SIMP_NON_LIN_COST), longConst(100), - AT_COST); + setupMultiplyInequations(d, longConst(IN_EQ_SIMP_NON_LIN_COST), longConst(CostBand.DEFAULT.at(100), + AT_COST)); - bindRuleSet(d, "inEqSimp_split_eq", add(TopLevelFindFeature.SUCC, longConst(-100))); + bindRuleSet(d, "inEqSimp_split_eq", + add(TopLevelFindFeature.SUCC, longConst(NonlinearArithmeticCost.SPLIT_EQ))); bindRuleSet(d, "inEqSimp_signCases", not(isInstantiated("signCasesLeft"))); } else if (arith == ArithTreatment.DEF_OPS) { @@ -780,8 +787,9 @@ private void setupMultiplyInequations(RuleSetDispatchFeature d, Feature baseCost ifZero(MatchedAssumesFeature.INSTANCE, SumFeature.createSum( applyTF("multFacLeft", tf.nonNegMonomial), - ifZero(applyTF("multRight", tf.literal), longConst(-100)), - ifZero(applyTF("multFacRight", tf.literal), longConst(-100), + ifZero(applyTF("multRight", tf.literal), longConst(CostBand.DEFAULT.at(-100))), + ifZero(applyTF("multFacRight", tf.literal), + longConst(CostBand.DEFAULT.at(-100)), applyTF("multFacRight", tf.polynomial)), /* * ifZero ( applyTF ( "multRight", tf.literal ), longConst ( -100 ), applyTF ( @@ -800,9 +808,9 @@ private void setupMultiplyInequations(RuleSetDispatchFeature d, Feature baseCost ? ifZero(BranchMultiplicationCountFeature.atMost("multiply_2_inEq", BRANCH_MULT_CAP), longConst(0), notAllowedF) : longConst(0), - ifZero(exactlyBounded, longConst(0), + ifZero(exactlyBounded, longConst(CostBand.DEFAULT.cost()), onlyExactlyBounded ? notAllowedF - : ifZero(totallyBounded, longConst(100), notAllowedF)) + : ifZero(totallyBounded, longConst(CostBand.DEFAULT.at(100)), notAllowedF)) /* * ifZero ( partiallyBounded, longConst ( 400 ), notAllowedF ) ) ), */ @@ -839,7 +847,8 @@ private void setupInEqSimpInstantiationWithoutRetry(RuleSetDispatchFeature d) { setupPullOutGcd(d, "inEqSimp_pullOutGcd_geq", true); // more efficient (but not confluent) versions for the antecedent - bindRuleSet(d, "inEqSimp_pullOutGcd_antec", -10); + bindRuleSet(d, "inEqSimp_pullOutGcd_antec", + LinearInequationCost.PULLOUT_GCD_ANTEC_NONCONFLUENT); // category "handling of non-linear inequations" @@ -917,7 +926,7 @@ private void setupInEqCaseDistinctions(RuleSetDispatchFeature d) { forEach(atom, SubtermGenerator.leftTraverse(sub(intRel, 0), tf.mulF), SumFeature.createSum(applyTF(atom, add(tf.atom, not(tf.literal))), allowPosNegCaseDistinction(atom), instantiate("signCasesLeft", atom), - longConst(IN_EQ_SIMP_NON_LIN_COST + 200) + longConst(NonlinearArithmeticCost.MULTIPLY + 200) // , // applyTF ( atom, rec ( any (), // longTermConst ( 5 ) ) ) @@ -929,7 +938,7 @@ private void setupInEqCaseDistinctions(RuleSetDispatchFeature d) { SumFeature.createSum( applyTF(intRel, add(or(tf.geqF, tf.leqF), sub(tf.atom, tf.literal))), instantiate("cutFormula", opTerm(tf.eq, sub(intRel, 0), sub(intRel, 1))), - longConst(IN_EQ_SIMP_NON_LIN_COST + 300) + longConst(NonlinearArithmeticCost.MULTIPLY + 300) // , // applyTF ( sub ( intRel, 0 ), // rec ( any (), longTermConst ( 5 ) ) ) @@ -939,9 +948,11 @@ private void setupInEqCaseDistinctions(RuleSetDispatchFeature d) { add(isRootInferenceProducer(intRel), forEach(rootInf, RootsGenerator.create(intRel, getServices()), add(instantiate("cutFormula", rootInf), - ifZero(applyTF(rootInf, op(Junctor.OR)), longConst(50)), - ifZero(applyTF(rootInf, op(Junctor.AND)), longConst(20)))), - longConst(IN_EQ_SIMP_NON_LIN_COST))); + ifZero(applyTF(rootInf, op(Junctor.OR)), + longConst(CostBand.DEFAULT.at(50))), + ifZero(applyTF(rootInf, op(Junctor.AND)), + longConst(CostBand.DEFAULT.at(20))))), + longConst(NonlinearArithmeticCost.MULTIPLY))); // noinspection unchecked bindRuleSet(d, "cut", oneOf(new Feature[] { strengthening, rootInferences })); @@ -1017,32 +1028,32 @@ private void setupDefOpsPrimaryCategories(RuleSetDispatchFeature d) { applyTF("divNum", tf.polynomial), applyTF("divDenom", tf.polynomial), applyTF("divNum", tf.notContainsDivMod), applyTF("divDenom", tf.notContainsDivMod), - ifZero(isBelow(ff.modalOperator), longConst(200)))); + ifZero(isBelow(ff.modalOperator), longConst(DivModCost.BELOW_MODALITY)))); bindRuleSet(d, "defOps_jdiv", SumFeature.createSum(NonDuplicateAppModPositionFeature.INSTANCE, applyTF("divNum", tf.polynomial), applyTF("divDenom", tf.polynomial), applyTF("divNum", tf.notContainsDivMod), applyTF("divDenom", tf.notContainsDivMod), - ifZero(isBelow(ff.modalOperator), longConst(200)))); + ifZero(isBelow(ff.modalOperator), longConst(DivModCost.BELOW_MODALITY)))); bindRuleSet(d, "defOps_jdiv_inline", add(applyTF("divNum", tf.literal), - applyTF("divDenom", tf.polynomial), longConst(-5000))); + applyTF("divDenom", tf.polynomial), longConst(DivModCost.INLINE))); setupDefOpsExpandMod(d); - bindRuleSet(d, "defOps_expandRanges", -8000); - bindRuleSet(d, "defOps_expandJNumericOp", -500); - bindRuleSet(d, "defOps_modHomoEq", -5000); + bindRuleSet(d, "defOps_expandRanges", DivModCost.EXPAND_RANGES); + bindRuleSet(d, "defOps_expandJNumericOp", DivModCost.EXPAND_NUMERIC_OP); + bindRuleSet(d, "defOps_modHomoEq", DivModCost.MOD_HOMO_EQ); } else { bindRuleSet(d, "defOps_div", inftyConst()); bindRuleSet(d, "defOps_jdiv", inftyConst()); bindRuleSet(d, "defOps_jdiv_inline", add(applyTF("divNum", tf.literal), - applyTF("divDenom", tf.literal), longConst(-4000))); + applyTF("divDenom", tf.literal), longConst(DivModCost.MOD))); bindRuleSet(d, "defOps_mod", add(applyTF("divNum", tf.literal), - applyTF("divDenom", tf.literal), longConst(-4000))); + applyTF("divDenom", tf.literal), longConst(DivModCost.MOD))); bindRuleSet(d, "defOps_expandRanges", inftyConst()); bindRuleSet(d, "defOps_expandJNumericOp", inftyConst()); @@ -1066,13 +1077,13 @@ private void setupDefOpsExpandMod(RuleSetDispatchFeature d) { bindRuleSet(d, "defOps_mod", ifZero(add(applyTF("divNum", tf.literal), applyTF("divDenom", tf.literal)), - longConst(-4000), + longConst(DivModCost.MOD), SumFeature.createSum(applyTF("divNum", tf.polynomial), applyTF("divDenom", tf.polynomial), ifZero(isBelow(ff.modalOperator), exSubsumedModulus, or(add(applyTF("divNum", tf.notContainsDivMod), applyTF("divDenom", tf.notContainsDivMod)), exSubsumedModulus)), - longConst(-3500)))); + longConst(DivModCost.MOD_EXPAND)))); } /** From 3a66fc374786dda58a0d69b5541a5824c6c996ec Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Wed, 8 Jul 2026 18:36:08 +0200 Subject: [PATCH 03/10] Step 2 (checkpoint): SymExStrategy costs via CostBand + SymExCost Byte-identical. Shared-ladder anchors -> CostBand (block/loop contracts BLOCK_CONTRACT, loopInvariant LOOP_INVARIANT, concrete_java REWRITE, simplify_java SIMPLIFY, simplify_prog_subset EXECUTE). SE-internal nudges -> SymExCost (PROGRAM_STEP and its throwing/under-quantifier variants, method expand pair, LOOP_SCOPE_EXPAND, MERGE_RULE + MERGE_POINT_SKIP delta, MODAL_TAUTOLOGY, BOX_DIAMOND_CONV, SPLIT_IF, the 42 loop-contract tie-break). EXECUTE reserved for genuine program-execution rules (merge is not one); modal_tautology named separately from SUBST. Enabled-gates (longConst(0)) and the findDepth scale left raw. Created with AI tooling support --- .../de/uka/ilkd/key/strategy/SymExCost.java | 87 +++++++++++++++++++ .../uka/ilkd/key/strategy/SymExStrategy.java | 60 +++++++------ 2 files changed, 122 insertions(+), 25 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/strategy/SymExCost.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExCost.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExCost.java new file mode 100644 index 00000000000..6130f1d88e4 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExCost.java @@ -0,0 +1,87 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.strategy; + +/** + * Symbolic-execution-internal ordering costs, used by {@link SymExStrategy}. These are the fine, + * within-SE ordering values that deserve a speaking name of their own; the coarse priorities that + * place SE rules relative to the other theories are written as + * {@code CostBand..cost()/at(delta)} at the call site instead (e.g. block/loop contracts + * {@code BLOCK_CONTRACT}, {@code loopInvariant} {@code LOOP_INVARIANT}, {@code concrete_java} + * {@code REWRITE}). + * + *

+ * Values are byte-identical to the literals they replace. Changing one reorders symbolic execution; + * verify with a full runAllProofs (as for + * {@link org.key_project.prover.strategy.costbased.CostBand}). + *

+ */ +final class SymExCost { + private SymExCost() {} + + /** + * A cheap concrete program step: {@code simplify_expression}, {@code execute*Assignment} and + * the ordinary {@code simplify_prog} case — "advance the program by one small step". + */ + static final long PROGRAM_STEP = -100; + + /** + * {@code simplify_prog} step that would raise a tracked runtime exception + * (NullPointer/ArrayIndexOutOfBounds/…): pushed back so the non-exceptional path is explored + * first. + */ + static final long THROWING_PROGRAM_STEP = 500; + + /** {@code simplify_prog} step underneath a quantifier / non-atom: mildly dispreferred. */ + static final long PROGRAM_STEP_UNDER_QUANTIFIER = 200; + + /** Method-body expansion in METHOD_EXPAND mode. */ + static final long METHOD_EXPAND = 100; + + /** + * Method-body expansion in METHOD_CONTRACT mode: raised (from {@link #METHOD_EXPAND}) so that + * contract application is preferred over expanding the body. + */ + static final long METHOD_EXPAND_REPRESSED = 2000; + + /** Preference offset of the method-contract feature ({@code methodSpec}). */ + static final long METHOD_CONTRACT_PREFERENCE = -20; + + /** {@code loop_scope_expand} when that loop treatment is selected. */ + static final long LOOP_SCOPE_EXPAND = 1000; + + /** + * Tie-break so that in BLOCK_CONTRACT_EXTERNAL mode the external loop contract is applied in + * preference to the internal one when both match; any small positive value would do. + *

+ * TODO: this delta should be anchored to the external loop contract cost rather than standing + * alone (deferred to the step-3 band normalization); kept byte-identical for now. + *

+ */ + static final long LOOP_CONTRACT_INTERNAL_TIEBREAK = 42; + + /** + * The merge rule ({@code MergeRule}), applied eagerly. NOT the EXECUTE band: that is reserved + * for genuine program-execution rules, and a branch merge is not one. + */ + static final long MERGE_RULE = -4000; + + /** + * Deleting a merge point in MPS_SKIP mode: a delta below {@link #MERGE_RULE} so the skip is + * preferred over performing a merge. + */ + static final long MERGE_POINT_SKIP = MERGE_RULE - 1000; + + /** + * Closing a modal tautology ({@code modal_tautology}). A distinct concept from a substitution; + * it merely shares the numeric level of {@code CostBand.SUBST} and so gets its own name. + */ + static final long MODAL_TAUTOLOGY = -10000; + + /** Prefer converting a box/diamond modality towards the antecedent-polarity program. */ + static final long BOX_DIAMOND_CONV = -1000; + + /** Mildly defer {@code split_if} so straight-line simplification runs first. */ + static final long SPLIT_IF = 50; +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExStrategy.java index baa90455843..b72933ba9b9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExStrategy.java @@ -21,6 +21,7 @@ import org.key_project.prover.rules.RuleApp; import org.key_project.prover.rules.RuleSet; import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.prover.strategy.costbased.CostBand; import org.key_project.prover.strategy.costbased.MutableState; import org.key_project.prover.strategy.costbased.NumberRuleAppCost; import org.key_project.prover.strategy.costbased.RuleAppCost; @@ -91,7 +92,7 @@ private Feature setupGlobalF(Feature dispatcher) { strategyProperties.getProperty(StrategyProperties.METHOD_OPTIONS_KEY); switch (methProp) { case StrategyProperties.METHOD_CONTRACT -> - methodSpecF = methodSpecFeature(longConst(-20)); + methodSpecF = methodSpecFeature(longConst(SymExCost.METHOD_CONTRACT_PREFERENCE)); case StrategyProperties.METHOD_EXPAND, StrategyProperties.METHOD_NONE -> methodSpecF = methodSpecFeature(inftyConst()); default -> { @@ -114,15 +115,20 @@ private Feature setupGlobalF(Feature dispatcher) { final String blockProperty = strategyProperties.getProperty(StrategyProperties.BLOCK_OPTIONS_KEY); if (blockProperty.equals(StrategyProperties.BLOCK_CONTRACT_INTERNAL)) { - blockFeature = blockContractInternalFeature(longConst(Long.MIN_VALUE)); - loopBlockFeature = loopContractInternalFeature(longConst(Long.MIN_VALUE)); - loopBlockApplyHeadFeature = loopContractApplyHead(longConst(Long.MIN_VALUE)); + blockFeature = blockContractInternalFeature(longConst(CostBand.BLOCK_CONTRACT.cost())); + loopBlockFeature = + loopContractInternalFeature(longConst(CostBand.BLOCK_CONTRACT.cost())); + loopBlockApplyHeadFeature = + loopContractApplyHead(longConst(CostBand.BLOCK_CONTRACT.cost())); } else if (blockProperty.equals(StrategyProperties.BLOCK_CONTRACT_EXTERNAL)) { - blockFeature = blockContractExternalFeature(longConst(Long.MIN_VALUE)); + blockFeature = blockContractExternalFeature(longConst(CostBand.BLOCK_CONTRACT.cost())); loopBlockFeature = - SumFeature.createSum(loopContractExternalFeature(longConst(Long.MIN_VALUE)), - loopContractInternalFeature(longConst(42))); - loopBlockApplyHeadFeature = loopContractApplyHead(longConst(Long.MIN_VALUE)); + SumFeature.createSum( + loopContractExternalFeature(longConst(CostBand.BLOCK_CONTRACT.cost())), + loopContractInternalFeature( + longConst(SymExCost.LOOP_CONTRACT_INTERNAL_TIEBREAK))); + loopBlockApplyHeadFeature = + loopContractApplyHead(longConst(CostBand.BLOCK_CONTRACT.cost())); } else { blockFeature = blockContractInternalFeature(inftyConst()); loopBlockFeature = loopContractExternalFeature(inftyConst()); @@ -133,7 +139,7 @@ private Feature setupGlobalF(Feature dispatcher) { final String mpsProperty = strategyProperties.getProperty(StrategyProperties.MPS_OPTIONS_KEY); if (mpsProperty.equals(StrategyProperties.MPS_MERGE)) { - mergeRuleF = mergeRuleFeature(longConst(-4000)); + mergeRuleF = mergeRuleFeature(longConst(SymExCost.MERGE_RULE)); } else { mergeRuleF = mergeRuleFeature(inftyConst()); } @@ -151,26 +157,28 @@ private RuleSetDispatchFeature setupCostComputationF() { bindRuleSet(d, "simplify_prog", ifZero(ThrownExceptionFeature.create(exceptionsWithPenalty, getServices()), - longConst(500), - ifZero(isBelow(add(ff.forF, not(ff.atom))), longConst(200), longConst(-100)))); + longConst(SymExCost.THROWING_PROGRAM_STEP), + ifZero(isBelow(add(ff.forF, not(ff.atom))), + longConst(SymExCost.PROGRAM_STEP_UNDER_QUANTIFIER), + longConst(SymExCost.PROGRAM_STEP)))); - bindRuleSet(d, "simplify_prog_subset", longConst(-4000)); + bindRuleSet(d, "simplify_prog_subset", longConst(CostBand.EXECUTE.cost())); - bindRuleSet(d, "simplify_expression", -100); + bindRuleSet(d, "simplify_expression", SymExCost.PROGRAM_STEP); - bindRuleSet(d, "simplify_java", -4500); + bindRuleSet(d, "simplify_java", CostBand.SIMPLIFY.cost()); - bindRuleSet(d, "executeIntegerAssignment", -100); - bindRuleSet(d, "executeDoubleAssignment", -100); + bindRuleSet(d, "executeIntegerAssignment", SymExCost.PROGRAM_STEP); + bindRuleSet(d, "executeDoubleAssignment", SymExCost.PROGRAM_STEP); final Feature findDepthFeature = FindDepthFeature.getInstance(); bindRuleSet(d, "concrete_java", - add(longConst(-11000), + add(longConst(CostBand.REWRITE.cost()), ScaleFeature.createScaled(findDepthFeature, 10.0))); // taclets for special invariant handling - bindRuleSet(d, "loopInvariant", -20000); + bindRuleSet(d, "loopInvariant", CostBand.LOOP_INVARIANT.cost()); boolean useLoopExpand = strategyProperties.getProperty(StrategyProperties.LOOP_OPTIONS_KEY) .equals(StrategyProperties.LOOP_EXPAND); @@ -183,7 +191,8 @@ private RuleSetDispatchFeature setupCostComputationF() { bindRuleSet(d, "loop_expand", useLoopExpand ? longConst(0) : inftyConst()); bindRuleSet(d, "loop_scope_inv_taclet", useLoopInvTaclets ? longConst(0) : inftyConst()); - bindRuleSet(d, "loop_scope_expand", useLoopScopeExpand ? longConst(1000) : inftyConst()); + bindRuleSet(d, "loop_scope_expand", + useLoopScopeExpand ? longConst(SymExCost.LOOP_SCOPE_EXPAND) : inftyConst()); final String methProp = @@ -196,9 +205,9 @@ private RuleSetDispatchFeature setupCostComputationF() { * is disabled. The original cost was 200 and is now increased to 2000 in order to * repress method expansion stronger when method treatment by contracts is chosen. */ - bindRuleSet(d, "method_expand", longConst(2000)); + bindRuleSet(d, "method_expand", longConst(SymExCost.METHOD_EXPAND_REPRESSED)); case StrategyProperties.METHOD_EXPAND -> - bindRuleSet(d, "method_expand", longConst(100)); + bindRuleSet(d, "method_expand", longConst(SymExCost.METHOD_EXPAND)); case StrategyProperties.METHOD_NONE -> bindRuleSet(d, "method_expand", inftyConst()); default -> throw new RuntimeException("Unexpected strategy property " + methProp); } @@ -227,12 +236,13 @@ private RuleSetDispatchFeature setupCostComputationF() { mState); } }); - case StrategyProperties.MPS_SKIP -> bindRuleSet(d, "merge_point", longConst(-5000)); + case StrategyProperties.MPS_SKIP -> + bindRuleSet(d, "merge_point", longConst(SymExCost.MERGE_POINT_SKIP)); case StrategyProperties.MPS_NONE -> bindRuleSet(d, "merge_point", inftyConst()); default -> throw new RuntimeException("Unexpected strategy property " + mpsProp); } - bindRuleSet(d, "modal_tautology", longConst(-10000)); + bindRuleSet(d, "modal_tautology", longConst(SymExCost.MODAL_TAUTOLOGY)); if (programsToRight) { bindRuleSet(d, "boxDiamondConv", @@ -240,7 +250,7 @@ private RuleSetDispatchFeature setupCostComputationF() { new FindPrefixRestrictionFeature( FindPrefixRestrictionFeature.PositionModifier.ALLOW_UPDATE_AS_PARENT, FindPrefixRestrictionFeature.PrefixChecker.ANTEC_POLARITY), - longConst(-1000))); + longConst(SymExCost.BOX_DIAMOND_CONV))); } else { bindRuleSet(d, "boxDiamondConv", inftyConst()); } @@ -251,7 +261,7 @@ private RuleSetDispatchFeature setupCostComputationF() { final TermBuffer superFor = new TermBuffer(); bindRuleSet(d, "split_if", add(sum(superFor, SuperTermGenerator.upwards(any(), getServices()), - applyTF(superFor, not(ff.program))), longConst(50))); + applyTF(superFor, not(ff.program))), longConst(SymExCost.SPLIT_IF))); return d; } From 167ed2f16d7197d5890114260508bea0d921e5da Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Thu, 9 Jul 2026 08:48:56 +0200 Subject: [PATCH 04/10] Step 2 (checkpoint): StringStrategy costs via CostBand + StringCost Byte-identical. String theory splits into an eager side (negatives, named in StringCost: INTEGER_TO_STRING, REPLACE_INLINE, CHAR_TO_INT_LITERAL, BELOW_MODALITY_PENALTY; plus stringsSimplify -> CostBand.NORMALIZE) and a lazy unfold ladder (positives) anchored to CostBand.DEFER.at(delta), so each defOps*/ strings* rule reads as "defer, by this much". instantiate default longConst(0) left raw; stringsConcatNotBothLiterals stays inftyConst. Created with AI tooling support --- .../de/uka/ilkd/key/strategy/StringCost.java | 42 +++++++++++++++++++ .../uka/ilkd/key/strategy/StringStrategy.java | 36 +++++++++------- 2 files changed, 63 insertions(+), 15 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/strategy/StringCost.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/StringCost.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/StringCost.java new file mode 100644 index 00000000000..ffdf87545dc --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/StringCost.java @@ -0,0 +1,42 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.strategy; + +/** + * String/sequence-theory-internal ordering costs, used by {@link StringStrategy}. + * + *

+ * The theory splits into an eager side (negative costs: normalisations done early, named + * here) and a lazy unfold ladder (positive costs: unfolding of string definitions is + * deferred so it happens only when needed). The ladder is anchored to + * {@code CostBand.DEFER.at(delta)} at the call sites, so each rule reads as "defer, by this much". + *

+ * + *

+ * Values are byte-identical to the literals they replace; changing one reorders string reasoning + * (verify with a full runAllProofs, as for + * {@link org.key_project.prover.strategy.costbased.CostBand}). + *

+ */ +final class StringCost { + private StringCost() {} + + /** Translate an integer to its string representation ({@code integerToString}): very eager. */ + static final long INTEGER_TO_STRING = -10000; + + /** + * Inline a {@code replace} when string, search- and replace-char are all literals + * ({@code defOpsReplaceInline}): eager, closed-form. + */ + static final long REPLACE_INLINE = -2500; + + /** Convert a char literal to an int literal (outside string functions). */ + static final long CHAR_TO_INT_LITERAL = -100; + + /** + * Extra penalty for unfolding a string definition below a modal operator: postpone it until + * the program has been symbolically executed. Shared by the {@code defOps*} rules. + */ + static final long BELOW_MODALITY_PENALTY = 500; +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/StringStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/StringStrategy.java index 1f8270ac099..bd6acb68815 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/StringStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/StringStrategy.java @@ -20,6 +20,7 @@ import org.key_project.prover.rules.RuleApp; import org.key_project.prover.rules.RuleSet; import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.prover.strategy.costbased.CostBand; import org.key_project.prover.strategy.costbased.MutableState; import org.key_project.prover.strategy.costbased.RuleAppCost; import org.key_project.prover.strategy.costbased.feature.Feature; @@ -70,7 +71,7 @@ private RuleSetDispatchFeature setupCostComputationF() { private void setUpStringNormalisation(RuleSetDispatchFeature d) { // translates an integer into its string representation - bindRuleSet(d, "integerToString", -10000); + bindRuleSet(d, "integerToString", StringCost.INTEGER_TO_STRING); // do not convert char to int when inside a string function // feature used to recognize if one is inside a string literal @@ -84,7 +85,7 @@ private void setUpStringNormalisation(RuleSetDispatchFeature d) { or(op(charListLDT.getClReplace()), op(charListLDT.getClLastIndexOfChar())))); bindRuleSet(d, "charLiteral_to_intLiteral", - ifZero(isBelow(keepChar), inftyConst(), longConst(-100))); + ifZero(isBelow(keepChar), inftyConst(), longConst(StringCost.CHAR_TO_INT_LITERAL))); // establish normalform @@ -95,25 +96,26 @@ private void setUpStringNormalisation(RuleSetDispatchFeature d) { final TermFeature seqLiteral = rec(anyLiteral, or(op(seqLDT.getSeqConcat()), or(op(seqLDT.getSeqSingleton()), or(anyLiteral, inftyTermConst())))); - Feature belowModOpPenality = ifZero(isBelow(ff.modalOperator), longConst(500)); + Feature belowModOpPenality = + ifZero(isBelow(ff.modalOperator), longConst(StringCost.BELOW_MODALITY_PENALTY)); bindRuleSet(d, "defOpsSeqEquality", add(NonDuplicateAppModPositionFeature.INSTANCE, ifZero(add(applyTF("left", seqLiteral), applyTF("right", seqLiteral)), - longConst(1000), inftyConst()), + longConst(CostBand.DEFER.at(500)), inftyConst()), belowModOpPenality)); bindRuleSet(d, "defOpsConcat", add(NonDuplicateAppModPositionFeature.INSTANCE, ifZero( or(applyTF("leftStr", not(seqLiteral)), applyTF("rightStr", not(seqLiteral))), - longConst(1000) + longConst(CostBand.DEFER.at(500)) // concat is often introduced for construction purposes, // we do not want to use its definition right at the // beginning ), belowModOpPenality)); - bindRuleSet(d, "stringsSimplify", longConst(-5000)); + bindRuleSet(d, "stringsSimplify", longConst(CostBand.NORMALIZE.cost())); final TermFeature charOrIntLiteral = or(tf.charLiteral, tf.literal, or(add(OperatorClassTF.create(ParametricFunctionInstance.class), // XXX: @@ -122,17 +124,19 @@ private void setUpStringNormalisation(RuleSetDispatchFeature d) { bindRuleSet(d, "defOpsReplaceInline", ifZero(add(applyTF("str", seqLiteral), applyTF("searchChar", charOrIntLiteral), - applyTF("replChar", charOrIntLiteral)), longConst(-2500), inftyConst())); + applyTF("replChar", charOrIntLiteral)), longConst(StringCost.REPLACE_INLINE), + inftyConst())); bindRuleSet(d, "defOpsReplace", add(NonDuplicateAppModPositionFeature.INSTANCE, ifZero(or(applyTF("str", not(seqLiteral)), applyTF("searchChar", not(charOrIntLiteral)), - applyTF("replChar", not(charOrIntLiteral))), longConst(500), inftyConst()), + applyTF("replChar", not(charOrIntLiteral))), longConst(CostBand.DEFER.cost()), + inftyConst()), belowModOpPenality)); bindRuleSet(d, "stringsReduceSubstring", - add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(100))); + add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(CostBand.DEFER.at(-400)))); - bindRuleSet(d, "defOpsStartsEndsWith", longConst(250)); + bindRuleSet(d, "defOpsStartsEndsWith", longConst(CostBand.DEFER.at(-250))); bindRuleSet(d, "stringsConcatNotBothLiterals", ifZero(MatchedAssumesFeature.INSTANCE, ifZero( @@ -140,19 +144,21 @@ private void setUpStringNormalisation(RuleSetDispatchFeature d) { applyTF(instOf("rightStr"), seqLiteral)), inftyConst()), inftyConst())); - bindRuleSet(d, "stringsReduceConcat", longConst(100)); + bindRuleSet(d, "stringsReduceConcat", longConst(CostBand.DEFER.at(-400))); bindRuleSet(d, "stringsReduceOrMoveOutsideConcat", - ifZero(NonDuplicateAppModPositionFeature.INSTANCE, longConst(800), inftyConst())); + ifZero(NonDuplicateAppModPositionFeature.INSTANCE, longConst(CostBand.DEFER.at(300)), + inftyConst())); bindRuleSet(d, "stringsMoveReplaceInside", - ifZero(NonDuplicateAppModPositionFeature.INSTANCE, longConst(400), inftyConst())); + ifZero(NonDuplicateAppModPositionFeature.INSTANCE, longConst(CostBand.DEFER.at(-100)), + inftyConst())); - bindRuleSet(d, "stringsExpandDefNormalOp", longConst(500)); + bindRuleSet(d, "stringsExpandDefNormalOp", longConst(CostBand.DEFER.cost())); bindRuleSet(d, "stringsContainsDefInline", SumFeature - .createSum(EqNonDuplicateAppFeature.INSTANCE, longConst(1000))); + .createSum(EqNonDuplicateAppFeature.INSTANCE, longConst(CostBand.DEFER.at(500)))); } @Override From 091391c5f80ea2b013f788e0829a1c8765d52520 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 10 Jul 2026 07:48:53 +0200 Subject: [PATCH 05/10] Step 2 (checkpoint): JavaCardDLStrategy costs via CostBand + holders Byte-identical; RAP verification pending (deferred to resume). Band uses verified against the band docs: simplify_literals -> ELIMINATE, query_axiom -> SOLVE, partialInvAxiom -> DEFER_STRONG, information_flow_contract_appl (1000000 sentinel) -> LAST_RESORT. The pull-out-select ladder -> HeapSelectCost (its own holder, pre-staging a future heap/select module; carries a comment on the apply_equations ~-5700 cross-theory coupling). Remaining axiom/observer/ comprehension/induction nudges -> JavaCardDLCost, named by meaning not by value coincidence (JAVA_INTEGER_SEMANTICS/COMPREHENSION_SIMPLIFY != NORMALIZE, AUTO_INDUCTION != TYPE). QueryExpandCost tuples, branch count, and enabled-gates left raw. Created with AI tooling support --- .../uka/ilkd/key/strategy/HeapSelectCost.java | 50 +++++++++++++ .../uka/ilkd/key/strategy/JavaCardDLCost.java | 73 +++++++++++++++++++ .../ilkd/key/strategy/JavaCardDLStrategy.java | 66 ++++++++++------- 3 files changed, 163 insertions(+), 26 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/strategy/HeapSelectCost.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLCost.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/HeapSelectCost.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/HeapSelectCost.java new file mode 100644 index 00000000000..92551b1bf48 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/HeapSelectCost.java @@ -0,0 +1,50 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.strategy; + +/** + * Costs of the pull-out-select heap simplification pipeline, used by {@link JavaCardDLStrategy}. + * This is the coherent heap/select cluster that is a candidate to be promoted into its own + * component strategy later; it is kept in a dedicated holder to pre-stage that split. + * + *

+ * Combination-relevant, not purely local: this ladder is tuned relative to the + * FOL/Integer {@code apply_equations} cost. In particular {@link #APPLY_SELECT_EQ} is chosen so + * that, together with the cost of {@code apply_equations}, the effective cost of replacing a select + * comes out at about −5700 (see the inline comment at {@code apply_select_eq}). Keep that coupling + * in mind when changing either side. + *

+ * + *

+ * Values are byte-identical to the literals they replace; verify changes with a full runAllProofs + * (as for {@link org.key_project.prover.strategy.costbased.CostBand}). + *

+ */ +final class HeapSelectCost { + private HeapSelectCost() {} + + /** {@code pull_out_select} when the focus select sits below an update (pull it out harder). */ + static final long PULL_OUT_SELECT_BELOW_UPDATE = -4200; + + /** {@code pull_out_select} otherwise. */ + static final long PULL_OUT_SELECT = -1900; + + /** + * {@code apply_select_eq}: replace a not-yet-simplified select by the skolem constant of its + * pull-out. Tuned so that with {@code apply_equations} the effective cost is about −5700. + */ + static final long APPLY_SELECT_EQ = -1700; + + /** {@code simplify_select}: simplify the select term in the pulled-out equation. */ + static final long SIMPLIFY_SELECT = -5600; + + /** {@code apply_auxiliary_eq}: replace the skolem constant by its computed value. */ + static final long APPLY_AUXILIARY_EQ = -5500; + + /** {@code hide_auxiliary_eq}: hide the auxiliary equation once the constant is replaced. */ + static final long HIDE_AUXILIARY_EQ = -5400; + + /** {@code hide_auxiliary_eq_const}: same, for the constant-valued case. */ + static final long HIDE_AUXILIARY_EQ_CONST = -500; +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLCost.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLCost.java new file mode 100644 index 00000000000..13621bec686 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLCost.java @@ -0,0 +1,73 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.strategy; + +/** + * JavaCardDL-theory-internal ordering costs, used by {@link JavaCardDLStrategy} (the axiom / + * observer / comprehension / induction reasoning; the heap/select pipeline has its own + * {@link HeapSelectCost}). + * + *

+ * Values are byte-identical to the literals they replace. Names are chosen by meaning, not + * by numeric coincidence with a {@link org.key_project.prover.strategy.costbased.CostBand} tier — + * e.g. {@link #AUTO_INDUCTION} shares −6500 with the FOL type-hierarchy rule but is not type + * reasoning, and {@link #JAVA_INTEGER_SEMANTICS} / {@link #COMPREHENSION_SIMPLIFY} share −5000 with + * NORMALIZE but are a definitional expansion / a simplify-like step. Verify changes with a full + * runAllProofs. + *

+ */ +final class JavaCardDLCost { + private JavaCardDLCost() {} + + /** + * Insert the java integer operator definitions ({@code javaIntegerSemantics}) once no program + * is left / on a single branch: a definitional expansion, not a canonicalization. + */ + static final long JAVA_INTEGER_SEMANTICS = -5000; + + /** Loc-set CNF commutation ({@code cnf_setComm}). */ + static final long LOCSET_CNF_COMMUTE = -800; + + /** Apply a class axiom ({@code classAxiom}). */ + static final long CLASS_AXIOM = -250; + + /** {@code inReachableStateImplication}. */ + static final long IN_REACHABLE_STATE = 100; + + /** + * Limit an observer symbol ({@code limitObserver}); must have better priority than classAxiom. + */ + static final long LIMIT_OBSERVER = -200; + + /** Dependency-contract application ({@code UseDependencyContractRule} / dependency feature). */ + static final long DEPENDENCY_CONTRACT = 250; + + // Comprehensions form a simplify/enlarge-style pair (cf. simplify / simplify_ENLARGING). The + // ENLARGE band doc even names "comprehension / map unfolding" — a step-3 candidate to normalize + // COMPREHENSION_SIMPLIFY -> SIMPLIFY and COMPREHENSION_ENLARGE -> ENLARGE. Byte-identical here. + /** Ordinary comprehension handling ({@code comprehensions}). */ + static final long COMPREHENSION = -50; + /** Cheap, simplify-like comprehension application ({@code comprehensions_low_costs}). */ + static final long COMPREHENSION_SIMPLIFY = -5000; + /** Expensive, enlarge-like comprehension application ({@code comprehensions_high_costs}). */ + static final long COMPREHENSION_ENLARGE = 10000; + + /** + * Auto-induction ({@code auto_induction}); must be applied like a delta rule. NOT the TYPE band + * despite sharing −6500 with the FOL type-hierarchy rule. + */ + static final long AUTO_INDUCTION = -6500; + + /** + * Auto-induction lemma ({@code auto_induction_lemma}); a beta rule with higher-than-usual + * priority. + */ + static final long AUTO_INDUCTION_LEMMA = -300; + + /** User taclets set to low priority: applied late. */ + static final long USER_TACLET_LOW_PRIORITY = 10000; + + /** User taclets set to high priority: mildly preferred. */ + static final long USER_TACLET_HIGH_PRIORITY = -50; +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java index d3a856e7572..acb162ccc67 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java @@ -27,6 +27,7 @@ import org.key_project.prover.rules.RuleApp; import org.key_project.prover.rules.RuleSet; import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.prover.strategy.costbased.CostBand; import org.key_project.prover.strategy.costbased.MutableState; import org.key_project.prover.strategy.costbased.RuleAppCost; import org.key_project.prover.strategy.costbased.TopRuleAppCost; @@ -133,7 +134,8 @@ protected Feature setupGlobalF(@NonNull Feature dispatcher) { final SetRuleFilter depFilter = new SetRuleFilter(); depFilter.addRuleToSet(UseDependencyContractRule.INSTANCE); if (depProp.equals(StrategyProperties.DEP_ON)) { - depSpecF = ConditionalFeature.createConditional(depFilter, longConst(250)); + depSpecF = ConditionalFeature.createConditional(depFilter, + longConst(JavaCardDLCost.DEPENDENCY_CONTRACT)); } else { depSpecF = ConditionalFeature.createConditional(depFilter, inftyConst()); } @@ -183,8 +185,10 @@ private RuleSetDispatchFeature setupCostComputationF() { bindRuleSet(d, "simplify_heap_high_costs", inftyConst()); bindRuleSet(d, "javaIntegerSemantics", - ifZero(sequentContainsNoPrograms(), longConst(-5000), ifZero( - leq(CountBranchFeature.INSTANCE, longConst(1)), longConst(-5000), inftyConst()))); + ifZero(sequentContainsNoPrograms(), longConst(JavaCardDLCost.JAVA_INTEGER_SEMANTICS), + ifZero( + leq(CountBranchFeature.INSTANCE, longConst(1)), + longConst(JavaCardDLCost.JAVA_INTEGER_SEMANTICS), inftyConst()))); setupSelectSimplification(d); @@ -201,7 +205,8 @@ private RuleSetDispatchFeature setupCostComputationF() { bindRuleSet(d, "cnf_setComm", add(SetsSmallerThanFeature.create(instOf("commRight"), instOf("commLeft"), locSetLDT), - NotInScopeOfModalityFeature.INSTANCE, longConst(-800))); + NotInScopeOfModalityFeature.INSTANCE, + longConst(JavaCardDLCost.LOCSET_CNF_COMMUTE))); } else { bindRuleSet(d, "cnf_setComm", inftyConst()); } @@ -209,19 +214,22 @@ private RuleSetDispatchFeature setupCostComputationF() { bindRuleSet(d, "simplify_literals", // ifZero ( ConstraintStrengthenFeatureUC.create(proof), // longConst ( 0 ), - longConst(-8000)); + longConst(CostBand.ELIMINATE.cost())); bindRuleSet(d, "nonDuplicateAppCheckEq", EqNonDuplicateAppFeature.INSTANCE); // TODO: rename rule set? bindRuleSet(d, "comprehensions", - add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(-50))); + add(NonDuplicateAppModPositionFeature.INSTANCE, + longConst(JavaCardDLCost.COMPREHENSION))); bindRuleSet(d, "comprehensions_high_costs", - add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(10000))); + add(NonDuplicateAppModPositionFeature.INSTANCE, + longConst(JavaCardDLCost.COMPREHENSION_ENLARGE))); bindRuleSet(d, "comprehensions_low_costs", - add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(-5000))); + add(NonDuplicateAppModPositionFeature.INSTANCE, + longConst(JavaCardDLCost.COMPREHENSION_SIMPLIFY))); // features influenced by the strategy options /* @@ -233,13 +241,13 @@ private RuleSetDispatchFeature setupCostComputationF() { strategyProperties.getProperty(StrategyProperties.QUERYAXIOM_OPTIONS_KEY); switch (queryAxProp) { case StrategyProperties.QUERYAXIOM_ON -> - bindRuleSet(d, "query_axiom", longConst(-3000)); + bindRuleSet(d, "query_axiom", longConst(CostBand.SOLVE.cost())); case StrategyProperties.QUERYAXIOM_OFF -> bindRuleSet(d, "query_axiom", inftyConst()); default -> throw new RuntimeException("Unexpected strategy property " + queryAxProp); } if (classAxiomApplicationEnabled()) { - bindRuleSet(d, "classAxiom", longConst(-250)); + bindRuleSet(d, "classAxiom", longConst(JavaCardDLCost.CLASS_AXIOM)); } else { bindRuleSet(d, "classAxiom", inftyConst()); } @@ -250,15 +258,18 @@ private RuleSetDispatchFeature setupCostComputationF() { // partial inv axiom bindRuleSet(d, "partialInvAxiom", - add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(10000))); + add(NonDuplicateAppModPositionFeature.INSTANCE, + longConst(CostBand.DEFER_STRONG.cost()))); // inReachableState bindRuleSet(d, "inReachableStateImplication", - add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(100))); + add(NonDuplicateAppModPositionFeature.INSTANCE, + longConst(JavaCardDLCost.IN_REACHABLE_STATE))); // limit observer (must have better priority than "classAxiom") bindRuleSet(d, "limitObserver", - add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(-200))); + add(NonDuplicateAppModPositionFeature.INSTANCE, + longConst(JavaCardDLCost.LIMIT_OBSERVER))); setupUserTaclets(d); @@ -266,7 +277,7 @@ private RuleSetDispatchFeature setupCostComputationF() { // chrisg: The following rule, if active, must be applied delta rules. if (autoInductionEnabled()) { - bindRuleSet(d, "auto_induction", -6500); // chrisg + bindRuleSet(d, "auto_induction", JavaCardDLCost.AUTO_INDUCTION); // chrisg } else { bindRuleSet(d, "auto_induction", inftyConst()); // chrisg } @@ -274,12 +285,12 @@ private RuleSetDispatchFeature setupCostComputationF() { // chrisg: The following rule is a beta rule that, if active, must have // a higher priority than other beta rules. if (autoInductionLemmaEnabled()) { - bindRuleSet(d, "auto_induction_lemma", -300); + bindRuleSet(d, "auto_induction_lemma", JavaCardDLCost.AUTO_INDUCTION_LEMMA); } else { bindRuleSet(d, "auto_induction_lemma", inftyConst()); } - bindRuleSet(d, "information_flow_contract_appl", longConst(1000000)); + bindRuleSet(d, "information_flow_contract_appl", longConst(CostBand.LAST_RESORT.cost())); if (strategyProperties.contains(StrategyProperties.AUTO_INDUCTION_ON) || strategyProperties.contains(StrategyProperties.AUTO_INDUCTION_LEMMA_ON)) { @@ -301,8 +312,9 @@ private void setupSelectSimplification(final RuleSetDispatchFeature d) { // function symbol) add(applyTF("h", not(or(PrimitiveHeapTermFeature.create(heapLDT), anonHeapTermFeature()))), - ifZero(applyTF(FocusFormulaProjection.INSTANCE, ff.update), longConst(-4200), - longConst(-1900)), + ifZero(applyTF(FocusFormulaProjection.INSTANCE, ff.update), + longConst(HeapSelectCost.PULL_OUT_SELECT_BELOW_UPDATE), + longConst(HeapSelectCost.PULL_OUT_SELECT)), NonDuplicateAppModPositionFeature.INSTANCE)); bindRuleSet(d, "apply_select_eq", // replace non-simplified select by the skolem constant @@ -312,7 +324,7 @@ private void setupSelectSimplification(final RuleSetDispatchFeature d) { ifZero(applyTF("s", not(rec(any(), SimplifiedSelectTermFeature.create(heapLDT)))), // together with the costs of apply_equations the // resulting costs are about -5700 - longConst(-1700))); + longConst(HeapSelectCost.APPLY_SELECT_EQ))); bindRuleSet(d, "simplify_select", // simplify_select term in pulled out equation (right hand // side has to be a skolem constant which has been @@ -322,12 +334,12 @@ private void setupSelectSimplification(final RuleSetDispatchFeature d) { add(isSelectSkolemConstantTerm("sk"), applyTF(sub(FocusProjection.INSTANCE, 0), not(SimplifiedSelectTermFeature.create(heapLDT))), - longConst(-5600))); + longConst(HeapSelectCost.SIMPLIFY_SELECT))); bindRuleSet(d, "simplify_select_concrete", longConst(-6000)); bindRuleSet(d, "simplify_select_elim_store", longConst(-7000)); bindRuleSet(d, "apply_auxiliary_eq", // replace a skolem constant by its computed value - add(isSelectSkolemConstantTerm("t1"), longConst(-5500))); + add(isSelectSkolemConstantTerm("t1"), longConst(HeapSelectCost.APPLY_AUXILIARY_EQ))); // hide an auxiliary equation once the skolem constant has been replaced by its value final Feature hideReplacedAuxiliaryEq = add(isSelectSkolemConstantTerm("auxiliarySK"), applyTF("result", @@ -338,7 +350,7 @@ private void setupSelectSimplification(final RuleSetDispatchFeature d) { final int pullOutHeapBound = getHeapSizeBound(); bindRuleSet(d, "hide_auxiliary_eq", pullOutHeapBound <= 0 ? add(hideReplacedAuxiliaryEq, longConst(-5400)) - : ifZero(hideReplacedAuxiliaryEq, longConst(-5400), + : ifZero(hideReplacedAuxiliaryEq, longConst(HeapSelectCost.HIDE_AUXILIARY_EQ), ifZero(isTermAPulledOutHeap(), ifZero(isSkolemConstantUsedElsewhereInSequent(), longConst(-5400), longConst(HIDE_DEFERRAL_COST)), @@ -346,7 +358,8 @@ private void setupSelectSimplification(final RuleSetDispatchFeature d) { bindRuleSet(d, "hide_auxiliary_eq_const", // hide an auxiliary equation once the skolem constant has been replaced by its // value - add(isSelectSkolemConstantTerm("auxiliarySK"), longConst(-500))); + add(isSelectSkolemConstantTerm("auxiliarySK"), + longConst(HeapSelectCost.HIDE_AUXILIARY_EQ_CONST))); } private void setupUserTaclets(RuleSetDispatchFeature d) { @@ -354,9 +367,9 @@ private void setupUserTaclets(RuleSetDispatchFeature d) { final String userTacletsProbs = strategyProperties.getProperty(StrategyProperties.userTacletsOptionsKey(i)); if (StrategyProperties.USER_TACLETS_LOW.equals(userTacletsProbs)) { - bindRuleSet(d, "userTaclets" + i, 10000); + bindRuleSet(d, "userTaclets" + i, JavaCardDLCost.USER_TACLET_LOW_PRIORITY); } else if (StrategyProperties.USER_TACLETS_HIGH.equals(userTacletsProbs)) { - bindRuleSet(d, "userTaclets" + i, -50); + bindRuleSet(d, "userTaclets" + i, JavaCardDLCost.USER_TACLET_HIGH_PRIORITY); } else { bindRuleSet(d, "userTaclets" + i, inftyConst()); } @@ -480,7 +493,8 @@ protected Feature setupApprovalF() { depFilter.addRuleToSet(UseDependencyContractRule.INSTANCE); if (depProp.equals(StrategyProperties.DEP_ON)) { depSpecF = ConditionalFeature.createConditional(depFilter, - ifZero(new DependencyContractFeature(), longConst(250), inftyConst())); + ifZero(new DependencyContractFeature(), + longConst(JavaCardDLCost.DEPENDENCY_CONTRACT), inftyConst())); } else { depSpecF = ConditionalFeature.createConditional(depFilter, inftyConst()); } From c841740cbb1a431ac1470571b63d28435fdab6e3 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 10 Jul 2026 09:08:01 +0200 Subject: [PATCH 06/10] Step 2 (consolidation): CombinationCost + naming/structure alignment Byte-identical consolidation after the five theory conversions: - New CombinationCost holder for costs whose meaning spans strategies, with two documented admission mechanisms: (1) conflict-dispatched rule sets (ORDERED_REWRITING for apply_equations - the demodulation cost, guarded by term/monomial-ordering decrease at all four call sites; CNF_CONVERSION for apply_equations_andOr, shared deliberately by FOL's conjNormalForm), and (2) cost-sum couplings (APPLY_SELECT_EQ_EFFECTIVE = tuned sum of the dual- tagged applyEq taclet; HeapSelectCost.APPLY_SELECT_EQ is now derived from it, turning the old "about -5700" comment into checked arithmetic). FOLCost.APPLY_EQUATIONS/CNF_ORDERING and LinearEquationCost.APPLY_EQUATIONS/ APPLY_EQ_AND_OR are removed in favour of the shared constants. - JavaCardDL holders grouped per theory into JavaCardDLCosts.java (JavaCardDLCost + HeapSelectCost, Integer-style one file per theory). - Below-scope penalty names aligned: StringCost.BELOW_MODALITY (matching DivModCost.BELOW_MODALITY), SymExCost.PROGRAM_STEP_BELOW_QUANTIFIER. A sweep over all taclets and rule-set bindings verified completeness: exactly the three conflict-dispatched rule sets exist (order_terms, apply_equations, apply_equations_andOr, all FOL/Integer), and the only tuned cost-sum coupling is the applyEq taclet covered above. Created with AI tooling support --- .../ilkd/key/strategy/CombinationCost.java | 67 +++++++++++++++++++ .../de/uka/ilkd/key/strategy/FOLCost.java | 17 +---- .../de/uka/ilkd/key/strategy/FOLStrategy.java | 6 +- .../uka/ilkd/key/strategy/HeapSelectCost.java | 50 -------------- .../key/strategy/IntegerArithmeticCosts.java | 26 +++---- .../ilkd/key/strategy/IntegerStrategy.java | 4 +- ...vaCardDLCost.java => JavaCardDLCosts.java} | 58 ++++++++++++++++ .../ilkd/key/strategy/JavaCardDLStrategy.java | 4 +- .../de/uka/ilkd/key/strategy/StringCost.java | 2 +- .../uka/ilkd/key/strategy/StringStrategy.java | 2 +- .../de/uka/ilkd/key/strategy/SymExCost.java | 2 +- .../uka/ilkd/key/strategy/SymExStrategy.java | 2 +- 12 files changed, 150 insertions(+), 90 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/strategy/CombinationCost.java delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/strategy/HeapSelectCost.java rename key.core/src/main/java/de/uka/ilkd/key/strategy/{JavaCardDLCost.java => JavaCardDLCosts.java} (54%) diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/CombinationCost.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/CombinationCost.java new file mode 100644 index 00000000000..8906ec57a60 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/CombinationCost.java @@ -0,0 +1,67 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.strategy; + +/** + * Costs whose meaning spans more than one component strategy — the theory-combination + * constants, as opposed to the theory-internal holders ({@link FOLCost}, the integer holders, + * {@link SymExCost}, {@link StringCost}, {@link JavaCardDLCost}, {@link HeapSelectCost}). + * + *

+ * A constant is admitted here through one of two mechanisms: + *

+ *
    + *
  1. Conflict-dispatched rule sets: the same rule set is bound by two strategies, and + * {@link ModularJavaDLStrategy}#resolveConflict dispatches between the two bindings by the focus + * term (integer-typed focus → Integer half, otherwise FOL half). The two bindings are two halves of + * ONE combination decision, so their base costs must agree. Currently: {@code apply_equations} and + * {@code apply_equations_andOr} (the third conflict case, {@code order_terms}, needs no constant + * here — both halves anchor it at {@code CostBand.NORMALIZE}).
    2. + *
  2. Cost-sum couplings: one taclet carries rule sets owned by different + * strategies, so the dispatch sums their contributions and the tuned quantity is the sum, not + * either summand (e.g. the {@code applyEq} taclet, see {@link #APPLY_SELECT_EQ_EFFECTIVE}).
    3. + *
+ * + *

+ * A theory-local rule may also reference a constant here when sharing the level is the documented + * intent (e.g. {@code conjNormalForm} at {@link #CNF_CONVERSION}), so that retuning the + * combination level moves the coupled rule with it. + *

+ * + *

+ * Values are byte-identical to the literals they replace; verify changes with a full runAllProofs + * (as for {@link org.key_project.prover.strategy.costbased.CostBand}). + *

+ */ +final class CombinationCost { + private CombinationCost() {} + + /** + * Demodulation: use an oriented equation as a rewrite rule, only in the decreasing direction + * of the reduction ordering (see the {@code TermSmallerThanFeature} / + * {@code MonomialsSmallerThanFeature} guards at the call sites; right ≺ left). The FOL half + * instantiates this with the generic term ordering, the Integer half with the monomial + * ordering. The orientation step itself ({@code order_terms}) sits at + * {@code CostBand.NORMALIZE}. Deliberately its own level — not {@code EXECUTE}, which + * is reserved for symbolic execution. + */ + static final long ORDERED_REWRITING = -4000; + + /** + * Priority at which CNF conversion runs: {@code conjNormalForm} (associativity, commutation, + * distribution, if-then-else expansion — the fine ordering among these comes from the + * {@code cnf_*} co-rule-sets, {@link FOLCost#CNF_RESTRUCTURE}) and ordered rewriting within + * and/or clause contexts ({@code apply_equations_andOr}, conflict-dispatched). + */ + static final long CNF_CONVERSION = -150; + + /** + * Effective cost of replacing a select term via the {@code applyEq} taclet: the taclet carries + * BOTH {@code apply_equations} (FOL/Integer, {@link #ORDERED_REWRITING}) and + * {@code apply_select_eq} (JavaCardDL, {@link HeapSelectCost#APPLY_SELECT_EQ}), so the + * dispatch sums the two contributions. This constant is the tuned target of that sum; + * {@link HeapSelectCost#APPLY_SELECT_EQ} is derived from it. + */ + static final long APPLY_SELECT_EQ_EFFECTIVE = -5700; +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLCost.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLCost.java index af0c819f56d..1cd7907686f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLCost.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLCost.java @@ -19,12 +19,6 @@ final class FOLCost { private FOLCost() {} - /** - * Base cost of applying an equation (applyEq / apply_equations). Deliberately its own band — - * not {@code EXECUTE}, which is reserved for symbolic execution. - */ - static final long APPLY_EQUATIONS = -4000; - /** * Distribution / swapping of quantifiers ({@code distrQuantifier}, {@code swapQuantifiers}). */ @@ -33,17 +27,12 @@ private FOLCost() {} /** * Restructuring of CNF clauses by associativity / distribution ({@code cnf_orAssoc}, * {@code cnf_andAssoc}, {@code cnf_dist}); the small {@code ± delta} at the call sites orders - * these among themselves. + * these among themselves. These are the fine deltas summed on top of the + * {@link CombinationCost#CNF_CONVERSION} level via the dual rule-set tags of the + * {@code conjNormalForm} taclets. */ static final long CNF_RESTRUCTURE = -35; - /** - * Ordering of formula-normalisation steps in the boolean/CNF area, at one shared priority: - * {@code conjNormalForm} (CNF conversion) and {@code apply_equations_andOr} (contextual - * equation application inside and/or). - */ - static final long CNF_ORDERING = -150; - /** * Defer {@code replace_known_right} when its target is in the consequent of an implication or * inside an equivalence, so the connective is decomposed first (which makes the antecedent diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java index a8bccf5aebc..506fddef19c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java @@ -301,7 +301,7 @@ protected void setupFormulaNormalisation(RuleSetDispatchFeature d) { ifZero( add(or(FocusInAntecFeature.getInstance(), notBelowQuantifier()), NotInScopeOfModalityFeature.INSTANCE), - add(longConst(FOLCost.CNF_ORDERING), + add(longConst(CombinationCost.CNF_CONVERSION), ScaleFeature.createScaled(FindDepthFeature.getInstance(), 20)), inftyConst())); @@ -318,7 +318,7 @@ protected void setupFormulaNormalisation(RuleSetDispatchFeature d) { add(let(left, instOf("applyEqLeft"), let(right, instOf("applyEqRight"), TermSmallerThanFeature.create(right, left))), - longConst(FOLCost.CNF_ORDERING))); + longConst(CombinationCost.CNF_CONVERSION))); bindRuleSet(d, "distrQuantifier", add(or( @@ -587,7 +587,7 @@ private void setupEquationReasoning(RuleSetDispatchFeature d) { let(left, sub(equation, 0), let(right, sub(equation, 1), TermSmallerThanFeature.create(right, left))))))), - longConst(FOLCost.APPLY_EQUATIONS))); + longConst(CombinationCost.ORDERED_REWRITING))); bindRuleSet(d, "insert_eq_nonrigid", applyTF(FocusProjection.create(0), IsNonRigidTermFeature.INSTANCE)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/HeapSelectCost.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/HeapSelectCost.java deleted file mode 100644 index 92551b1bf48..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/HeapSelectCost.java +++ /dev/null @@ -1,50 +0,0 @@ -/* This file is part of KeY - https://key-project.org - * KeY is licensed under the GNU General Public License Version 2 - * SPDX-License-Identifier: GPL-2.0-only */ -package de.uka.ilkd.key.strategy; - -/** - * Costs of the pull-out-select heap simplification pipeline, used by {@link JavaCardDLStrategy}. - * This is the coherent heap/select cluster that is a candidate to be promoted into its own - * component strategy later; it is kept in a dedicated holder to pre-stage that split. - * - *

- * Combination-relevant, not purely local: this ladder is tuned relative to the - * FOL/Integer {@code apply_equations} cost. In particular {@link #APPLY_SELECT_EQ} is chosen so - * that, together with the cost of {@code apply_equations}, the effective cost of replacing a select - * comes out at about −5700 (see the inline comment at {@code apply_select_eq}). Keep that coupling - * in mind when changing either side. - *

- * - *

- * Values are byte-identical to the literals they replace; verify changes with a full runAllProofs - * (as for {@link org.key_project.prover.strategy.costbased.CostBand}). - *

- */ -final class HeapSelectCost { - private HeapSelectCost() {} - - /** {@code pull_out_select} when the focus select sits below an update (pull it out harder). */ - static final long PULL_OUT_SELECT_BELOW_UPDATE = -4200; - - /** {@code pull_out_select} otherwise. */ - static final long PULL_OUT_SELECT = -1900; - - /** - * {@code apply_select_eq}: replace a not-yet-simplified select by the skolem constant of its - * pull-out. Tuned so that with {@code apply_equations} the effective cost is about −5700. - */ - static final long APPLY_SELECT_EQ = -1700; - - /** {@code simplify_select}: simplify the select term in the pulled-out equation. */ - static final long SIMPLIFY_SELECT = -5600; - - /** {@code apply_auxiliary_eq}: replace the skolem constant by its computed value. */ - static final long APPLY_AUXILIARY_EQ = -5500; - - /** {@code hide_auxiliary_eq}: hide the auxiliary equation once the constant is replaced. */ - static final long HIDE_AUXILIARY_EQ = -5400; - - /** {@code hide_auxiliary_eq_const}: same, for the constant-valued case. */ - static final long HIDE_AUXILIARY_EQ_CONST = -500; -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerArithmeticCosts.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerArithmeticCosts.java index 1c34f5b58b0..679634e1f6b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerArithmeticCosts.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerArithmeticCosts.java @@ -38,24 +38,20 @@ private PolynomialCost() {} final class LinearEquationCost { private LinearEquationCost() {} - /** - * The general {@code apply_equations} rule set (applyEq / applyEqReverse), used to reduce - * polynomials. Distinct from {@link #APPLY_EQ}, which is the monomial-specialised polySimp - * variant. Its own band, not {@code EXECUTE} (reserved for symbolic execution). - *

- * Step-3 idea: test whether the specialised {@link #APPLY_EQ} is needed at all, or should just - * be a small delta that prefers these original {@code apply_equations} rules. - *

- */ - static final long APPLY_EQUATIONS = -4000; - static final long APPLY_EQ_AND_OR = -150; + // The base costs of apply_equations / apply_equations_andOr are combination-shared with + // FOLStrategy (conflict-dispatched; the Integer halves use the monomial ordering as + // demodulation guard): see CombinationCost.ORDERED_REWRITING and + // CombinationCost.CNF_CONVERSION. + /** polySimp_balance, polySimp_normalise. */ static final long BALANCE = -30; /** - * polySimp_applyEq — the monomial-coefficient-specialised equation application. The rigid - * variant polySimp_applyEqRigid is written {@code APPLY_EQ + 1} at the call site; that +1 is - * only an (uninteresting) tie-break between the two rules, a step-3 candidate to flatten to a - * single cost. + * polySimp_applyEq — the monomial-coefficient-specialised equation application (the general + * demodulation cost is {@link CombinationCost#ORDERED_REWRITING}). The rigid variant + * polySimp_applyEqRigid is written {@code APPLY_EQ + 1} at the call site; that +1 is only an + * (uninteresting) tie-break between the two rules, a step-3 candidate to flatten to a single + * cost. Step-3 idea: test whether this specialised variant is needed at all, or should just be + * a small delta preferring the original {@code apply_equations} rules. */ static final long APPLY_EQ = 1; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java index 02a3f9ef118..d0e2177e587 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java @@ -230,7 +230,7 @@ private RuleSetDispatchFeature setupCostComputationF() { applyTF(right, tf.polynomial), MonomialsSmallerThanFeature.create(right, left, numbers)))))))), - longConst(LinearEquationCost.APPLY_EQUATIONS))); + longConst(CombinationCost.ORDERED_REWRITING))); final TermBuffer l = new TermBuffer(); final TermBuffer r = new TermBuffer(); @@ -239,7 +239,7 @@ private RuleSetDispatchFeature setupCostComputationF() { let(r, instOf("applyEqRight"), add(applyTF(l, tf.nonNegOrNonCoeffMonomial), applyTF(r, tf.polynomial), MonomialsSmallerThanFeature.create(r, l, numbers)))), - longConst(LinearEquationCost.APPLY_EQ_AND_OR))); + longConst(CombinationCost.CNF_CONVERSION))); // For taclets that need instantiation, but where the instantiation is // deterministic and does not have to be repeated at a later point, we diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLCost.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLCosts.java similarity index 54% rename from key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLCost.java rename to key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLCosts.java index 13621bec686..78a371093ef 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLCost.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLCosts.java @@ -3,6 +3,14 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.strategy; +/* + * Theory-internal cost constants for the JavaCardDL strategy, grouped per sub-area + * (Integer-style, one file per theory): JavaCardDLCost for the axiom / observer / + * comprehension / induction reasoning, HeapSelectCost for the pull-out-select pipeline + * (a future component strategy of its own; it is kept as a separate holder to pre-stage + * that split and moves with it). + */ + /** * JavaCardDL-theory-internal ordering costs, used by {@link JavaCardDLStrategy} (the axiom / * observer / comprehension / induction reasoning; the heap/select pipeline has its own @@ -71,3 +79,53 @@ private JavaCardDLCost() {} /** User taclets set to high priority: mildly preferred. */ static final long USER_TACLET_HIGH_PRIORITY = -50; } + + +/** + * Costs of the pull-out-select heap simplification pipeline, used by {@link JavaCardDLStrategy}. + * This is the coherent heap/select cluster that is a candidate to be promoted into its own + * component strategy later; it is kept in a dedicated holder to pre-stage that split. + * + *

+ * Combination-relevant, not purely local: this ladder is tuned relative to the + * demodulation cost {@link CombinationCost#ORDERED_REWRITING}: {@link #APPLY_SELECT_EQ} is the + * JavaCardDL-side remainder of the tuned sum {@link CombinationCost#APPLY_SELECT_EQ_EFFECTIVE} + * (the {@code applyEq} taclet carries both rule sets, so the dispatch sums the contributions). + *

+ * + *

+ * Values are byte-identical to the literals they replace; verify changes with a full runAllProofs + * (as for {@link org.key_project.prover.strategy.costbased.CostBand}). + *

+ */ +final class HeapSelectCost { + private HeapSelectCost() {} + + /** {@code pull_out_select} when the focus select sits below an update (pull it out harder). */ + static final long PULL_OUT_SELECT_BELOW_UPDATE = -4200; + + /** {@code pull_out_select} otherwise. */ + static final long PULL_OUT_SELECT = -1900; + + /** + * {@code apply_select_eq}: replace a not-yet-simplified select by the skolem constant of its + * pull-out. The {@code applyEq} taclet carries both {@code apply_equations} and + * {@code apply_select_eq}, so the effective cost is the SUM of the two bindings; the tuned + * quantity is {@link CombinationCost#APPLY_SELECT_EQ_EFFECTIVE} and this constant is the + * JavaCardDL-side remainder (currently −1700). + */ + static final long APPLY_SELECT_EQ = + CombinationCost.APPLY_SELECT_EQ_EFFECTIVE - CombinationCost.ORDERED_REWRITING; + + /** {@code simplify_select}: simplify the select term in the pulled-out equation. */ + static final long SIMPLIFY_SELECT = -5600; + + /** {@code apply_auxiliary_eq}: replace the skolem constant by its computed value. */ + static final long APPLY_AUXILIARY_EQ = -5500; + + /** {@code hide_auxiliary_eq}: hide the auxiliary equation once the constant is replaced. */ + static final long HIDE_AUXILIARY_EQ = -5400; + + /** {@code hide_auxiliary_eq_const}: same, for the constant-valued case. */ + static final long HIDE_AUXILIARY_EQ_CONST = -500; +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java index acb162ccc67..515adc60a4c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java @@ -322,8 +322,8 @@ private void setupSelectSimplification(final RuleSetDispatchFeature d) { // needs to be not simplified yet; additional restrictions // in isApproved() ifZero(applyTF("s", not(rec(any(), SimplifiedSelectTermFeature.create(heapLDT)))), - // together with the costs of apply_equations the - // resulting costs are about -5700 + // the applyEq taclet also carries apply_equations, so the dispatch sums the + // bindings; the tuned sum is CombinationCost.APPLY_SELECT_EQ_EFFECTIVE longConst(HeapSelectCost.APPLY_SELECT_EQ))); bindRuleSet(d, "simplify_select", // simplify_select term in pulled out equation (right hand diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/StringCost.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/StringCost.java index ffdf87545dc..953080d5f42 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/StringCost.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/StringCost.java @@ -38,5 +38,5 @@ private StringCost() {} * Extra penalty for unfolding a string definition below a modal operator: postpone it until * the program has been symbolically executed. Shared by the {@code defOps*} rules. */ - static final long BELOW_MODALITY_PENALTY = 500; + static final long BELOW_MODALITY = 500; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/StringStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/StringStrategy.java index bd6acb68815..5a2bc6fe493 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/StringStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/StringStrategy.java @@ -97,7 +97,7 @@ private void setUpStringNormalisation(RuleSetDispatchFeature d) { or(op(seqLDT.getSeqSingleton()), or(anyLiteral, inftyTermConst())))); Feature belowModOpPenality = - ifZero(isBelow(ff.modalOperator), longConst(StringCost.BELOW_MODALITY_PENALTY)); + ifZero(isBelow(ff.modalOperator), longConst(StringCost.BELOW_MODALITY)); bindRuleSet(d, "defOpsSeqEquality", add(NonDuplicateAppModPositionFeature.INSTANCE, diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExCost.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExCost.java index 6130f1d88e4..798fdde2cef 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExCost.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExCost.java @@ -34,7 +34,7 @@ private SymExCost() {} static final long THROWING_PROGRAM_STEP = 500; /** {@code simplify_prog} step underneath a quantifier / non-atom: mildly dispreferred. */ - static final long PROGRAM_STEP_UNDER_QUANTIFIER = 200; + static final long PROGRAM_STEP_BELOW_QUANTIFIER = 200; /** Method-body expansion in METHOD_EXPAND mode. */ static final long METHOD_EXPAND = 100; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExStrategy.java index b72933ba9b9..b944d73cea4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExStrategy.java @@ -159,7 +159,7 @@ private RuleSetDispatchFeature setupCostComputationF() { ifZero(ThrownExceptionFeature.create(exceptionsWithPenalty, getServices()), longConst(SymExCost.THROWING_PROGRAM_STEP), ifZero(isBelow(add(ff.forF, not(ff.atom))), - longConst(SymExCost.PROGRAM_STEP_UNDER_QUANTIFIER), + longConst(SymExCost.PROGRAM_STEP_BELOW_QUANTIFIER), longConst(SymExCost.PROGRAM_STEP)))); bindRuleSet(d, "simplify_prog_subset", longConst(CostBand.EXECUTE.cost())); From c2beb4bd55a6a51e8976e00816eda4b9b41a2964 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 10 Jul 2026 11:24:31 +0200 Subject: [PATCH 07/10] Step 2 (readability): static-import theory-local costs; APPLY_EQ rename Pure cosmetic (byte-identical, no cost value changes): - Rename LinearEquationCost.APPLY_EQ -> APPLY_EQ_MONOMIAL_TIEBREAK (it is a small rider delta on CombinationCost.ORDERED_REWRITING via the dual-tagged apply_eq_monomials taclet, not a standalone "cost 1"); javadoc clarified. - Static-wildcard-import the theory-local cost holders in the single-holder strategies (FOLCost, SymExCost, StringCost, JavaCardDLCost+HeapSelectCost) so call sites read as bare names; the qualifier was pure redundancy there and forced spotless line wraps. CostBand and CombinationCost stay qualified (the prefix signals the shared ladder / a cross-theory cost). IntegerStrategy stays fully qualified: its 5 sub-holders' prefixes say which arithmetic layer. Created with AI tooling support --- .../de/uka/ilkd/key/strategy/FOLStrategy.java | 32 +++++++------ .../key/strategy/IntegerArithmeticCosts.java | 15 +++--- .../ilkd/key/strategy/IntegerStrategy.java | 4 +- .../ilkd/key/strategy/JavaCardDLStrategy.java | 47 ++++++++++--------- .../uka/ilkd/key/strategy/StringStrategy.java | 10 ++-- .../uka/ilkd/key/strategy/SymExStrategy.java | 34 +++++++------- 6 files changed, 76 insertions(+), 66 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java index 506fddef19c..9960d7c9446 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java @@ -43,6 +43,8 @@ import org.jspecify.annotations.NonNull; +import static de.uka.ilkd.key.strategy.FOLCost.*; + /// Strategy for general FOL rules. This does not consider other /// theories like integers or Java-specific functions. /// @@ -330,30 +332,30 @@ protected void setupFormulaNormalisation(RuleSetDispatchFeature d) { ifZero(FocusInAntecFeature.getInstance(), applyTF(FocusProjection.INSTANCE, sub(ff.andF)), applyTF(FocusProjection.INSTANCE, sub(ff.orF))))), - longConst(FOLCost.QUANTIFIER_DISTRIBUTION))); + longConst(QUANTIFIER_DISTRIBUTION))); bindRuleSet(d, "swapQuantifiers", add(applyTF(FocusProjection.INSTANCE, add(ff.quantifiedClauseSet, EliminableQuantifierTF.INSTANCE, sub(not(EliminableQuantifierTF.INSTANCE)))), - longConst(FOLCost.QUANTIFIER_DISTRIBUTION))); + longConst(QUANTIFIER_DISTRIBUTION))); // category "conjunctive normal form" bindRuleSet(d, "cnf_orAssoc", SumFeature.createSum(applyTF("assoc0", ff.clause), applyTF("assoc1", ff.clause), applyTF("assoc2", ff.literal), - longConst(FOLCost.CNF_RESTRUCTURE - 45))); + longConst(CNF_RESTRUCTURE - 45))); bindRuleSet(d, "cnf_andAssoc", SumFeature.createSum(applyTF("assoc0", ff.clauseSet), applyTF("assoc1", ff.clauseSet), applyTF("assoc2", ff.clause), - longConst(FOLCost.CNF_RESTRUCTURE + 25))); + longConst(CNF_RESTRUCTURE + 25))); bindRuleSet(d, "cnf_dist", SumFeature.createSum(applyTF("distRight0", ff.clauseSet), applyTF("distRight1", ff.clauseSet), ifZero(applyTF("distLeft", ff.clause), - longConst(FOLCost.CNF_RESTRUCTURE + 20), applyTF("distLeft", ff.clauseSet)), - longConst(FOLCost.CNF_RESTRUCTURE))); + longConst(CNF_RESTRUCTURE + 20), applyTF("distLeft", ff.clauseSet)), + longConst(CNF_RESTRUCTURE))); final TermBuffer superFor = new TermBuffer(); final Feature onlyBelowQuanAndOr = @@ -375,16 +377,16 @@ EliminableQuantifierTF.INSTANCE, sub(not(EliminableQuantifierTF.INSTANCE)))), add(isBelow(OperatorClassTF.create(Quantifier.class)), onlyBelowQuanAndOr, applyTF( FocusProjection.create(0), sub(ff.quantifiedClauseSet, ff.quantifiedClauseSet))); - bindRuleSet(d, "pullOutQuantifierUnifying", FOLCost.PULL_OUT_QUANTIFIER); + bindRuleSet(d, "pullOutQuantifierUnifying", PULL_OUT_QUANTIFIER); bindRuleSet(d, "pullOutQuantifierAll", add(pullOutQuantifierAllowed, - ifZero(FocusInAntecFeature.getInstance(), longConst(FOLCost.PULL_OUT_QUANTIFIER), - longConst(FOLCost.PULL_OUT_QUANTIFIER_REVERSE)))); + ifZero(FocusInAntecFeature.getInstance(), longConst(PULL_OUT_QUANTIFIER), + longConst(PULL_OUT_QUANTIFIER_REVERSE)))); bindRuleSet(d, "pullOutQuantifierEx", add(pullOutQuantifierAllowed, ifZero(FocusInAntecFeature.getInstance(), - longConst(FOLCost.PULL_OUT_QUANTIFIER_REVERSE), - longConst(FOLCost.PULL_OUT_QUANTIFIER)))); + longConst(PULL_OUT_QUANTIFIER_REVERSE), + longConst(PULL_OUT_QUANTIFIER)))); } // ////////////////////////////////////////////////////////////////////////// @@ -477,9 +479,9 @@ private void setupReplaceKnown(RuleSetDispatchFeature d) { bindRuleSet(d, "replace_known_right", add(commonF, ifZero(directlyBelowSymbolAtIndex(Junctor.IMP, 1), - longConst(FOLCost.REPLACE_KNOWN_UNDER_CONNECTIVE), + longConst(REPLACE_KNOWN_UNDER_CONNECTIVE), ifZero(directlyBelowSymbolAtIndex(Equality.EQV, -1), - longConst(FOLCost.REPLACE_KNOWN_UNDER_CONNECTIVE))))); + longConst(REPLACE_KNOWN_UNDER_CONNECTIVE))))); } // ////////////////////////////////////////////////////////////////////////// @@ -531,14 +533,14 @@ protected void setupSplitting(RuleSetDispatchFeature d) { // auxiliary variables rec(any(), not(selectSkolemConstantTermFeature())))), countOccurrencesInSeq, // standard costs - longConst(FOLCost.CUT_DIRECT_STANDARD)), + longConst(CUT_DIRECT_STANDARD)), SumFeature // check for cuts below quantifiers .createSum(applyTF(cutFormula, ff.cutAllowedBelowQuantifier), applyTF(FocusFormulaProjection.INSTANCE, ff.quantifiedClauseSet), ifZero(allowQuantifierSplitting(), longConst(CostBand.DEFAULT.cost()), - longConst(FOLCost.CUT_DIRECT_STANDARD)))))); + longConst(CUT_DIRECT_STANDARD)))))); } private void setupSplittingApproval(RuleSetDispatchFeature d) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerArithmeticCosts.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerArithmeticCosts.java index 679634e1f6b..fb572e7c594 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerArithmeticCosts.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerArithmeticCosts.java @@ -46,14 +46,15 @@ private LinearEquationCost() {} /** polySimp_balance, polySimp_normalise. */ static final long BALANCE = -30; /** - * polySimp_applyEq — the monomial-coefficient-specialised equation application (the general - * demodulation cost is {@link CombinationCost#ORDERED_REWRITING}). The rigid variant - * polySimp_applyEqRigid is written {@code APPLY_EQ + 1} at the call site; that +1 is only an - * (uninteresting) tie-break between the two rules, a step-3 candidate to flatten to a single - * cost. Step-3 idea: test whether this specialised variant is needed at all, or should just be - * a small delta preferring the original {@code apply_equations} rules. + * polySimp_applyEq — a small tie-break rider on top of the general demodulation cost + * {@link CombinationCost#ORDERED_REWRITING} (the {@code apply_eq_monomials} taclet carries both + * rule sets, so the effective cost is their sum). The rigid variant polySimp_applyEqRigid is + * written {@code APPLY_EQ_MONOMIAL_TIEBREAK + 1} at the call site; that +1 is only an + * (uninteresting) tie-break between the two rules, a step-3 candidate to flatten. Step-3 idea: + * test whether this specialised variant is needed at all, or should just be a small delta + * preferring the original {@code apply_equations} rules. */ - static final long APPLY_EQ = 1; + static final long APPLY_EQ_MONOMIAL_TIEBREAK = 1; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java index d0e2177e587..3d4eaa6bc00 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java @@ -385,10 +385,10 @@ private void setupPolySimp(RuleSetDispatchFeature d, IntegerLDT numbers) { let(eqLeft, sub(AssumptionProjection.create(0), 0), validEqApplication)))); bindRuleSet(d, "polySimp_applyEq", - add(eqMonomialFeature, longConst(LinearEquationCost.APPLY_EQ))); + add(eqMonomialFeature, longConst(LinearEquationCost.APPLY_EQ_MONOMIAL_TIEBREAK))); bindRuleSet(d, "polySimp_applyEqRigid", - add(eqMonomialFeature, longConst(LinearEquationCost.APPLY_EQ + 1))); + add(eqMonomialFeature, longConst(LinearEquationCost.APPLY_EQ_MONOMIAL_TIEBREAK + 1))); // bindRuleSet(d, "defOps_expandModulo", diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java index 515adc60a4c..82d7e9186e6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java @@ -39,6 +39,9 @@ import org.jspecify.annotations.NonNull; +import static de.uka.ilkd.key.strategy.HeapSelectCost.*; +import static de.uka.ilkd.key.strategy.JavaCardDLCost.*; + /// This strategy is the catch-all for Java related features that are either /// cross-cutting or one of the features that do not fit well into any other /// strategy. @@ -135,7 +138,7 @@ protected Feature setupGlobalF(@NonNull Feature dispatcher) { depFilter.addRuleToSet(UseDependencyContractRule.INSTANCE); if (depProp.equals(StrategyProperties.DEP_ON)) { depSpecF = ConditionalFeature.createConditional(depFilter, - longConst(JavaCardDLCost.DEPENDENCY_CONTRACT)); + longConst(DEPENDENCY_CONTRACT)); } else { depSpecF = ConditionalFeature.createConditional(depFilter, inftyConst()); } @@ -185,10 +188,10 @@ private RuleSetDispatchFeature setupCostComputationF() { bindRuleSet(d, "simplify_heap_high_costs", inftyConst()); bindRuleSet(d, "javaIntegerSemantics", - ifZero(sequentContainsNoPrograms(), longConst(JavaCardDLCost.JAVA_INTEGER_SEMANTICS), + ifZero(sequentContainsNoPrograms(), longConst(JAVA_INTEGER_SEMANTICS), ifZero( leq(CountBranchFeature.INSTANCE, longConst(1)), - longConst(JavaCardDLCost.JAVA_INTEGER_SEMANTICS), inftyConst()))); + longConst(JAVA_INTEGER_SEMANTICS), inftyConst()))); setupSelectSimplification(d); @@ -206,7 +209,7 @@ private RuleSetDispatchFeature setupCostComputationF() { add(SetsSmallerThanFeature.create(instOf("commRight"), instOf("commLeft"), locSetLDT), NotInScopeOfModalityFeature.INSTANCE, - longConst(JavaCardDLCost.LOCSET_CNF_COMMUTE))); + longConst(LOCSET_CNF_COMMUTE))); } else { bindRuleSet(d, "cnf_setComm", inftyConst()); } @@ -221,15 +224,15 @@ private RuleSetDispatchFeature setupCostComputationF() { // TODO: rename rule set? bindRuleSet(d, "comprehensions", add(NonDuplicateAppModPositionFeature.INSTANCE, - longConst(JavaCardDLCost.COMPREHENSION))); + longConst(COMPREHENSION))); bindRuleSet(d, "comprehensions_high_costs", add(NonDuplicateAppModPositionFeature.INSTANCE, - longConst(JavaCardDLCost.COMPREHENSION_ENLARGE))); + longConst(COMPREHENSION_ENLARGE))); bindRuleSet(d, "comprehensions_low_costs", add(NonDuplicateAppModPositionFeature.INSTANCE, - longConst(JavaCardDLCost.COMPREHENSION_SIMPLIFY))); + longConst(COMPREHENSION_SIMPLIFY))); // features influenced by the strategy options /* @@ -247,7 +250,7 @@ private RuleSetDispatchFeature setupCostComputationF() { } if (classAxiomApplicationEnabled()) { - bindRuleSet(d, "classAxiom", longConst(JavaCardDLCost.CLASS_AXIOM)); + bindRuleSet(d, "classAxiom", longConst(CLASS_AXIOM)); } else { bindRuleSet(d, "classAxiom", inftyConst()); } @@ -264,12 +267,12 @@ private RuleSetDispatchFeature setupCostComputationF() { // inReachableState bindRuleSet(d, "inReachableStateImplication", add(NonDuplicateAppModPositionFeature.INSTANCE, - longConst(JavaCardDLCost.IN_REACHABLE_STATE))); + longConst(IN_REACHABLE_STATE))); // limit observer (must have better priority than "classAxiom") bindRuleSet(d, "limitObserver", add(NonDuplicateAppModPositionFeature.INSTANCE, - longConst(JavaCardDLCost.LIMIT_OBSERVER))); + longConst(LIMIT_OBSERVER))); setupUserTaclets(d); @@ -277,7 +280,7 @@ private RuleSetDispatchFeature setupCostComputationF() { // chrisg: The following rule, if active, must be applied delta rules. if (autoInductionEnabled()) { - bindRuleSet(d, "auto_induction", JavaCardDLCost.AUTO_INDUCTION); // chrisg + bindRuleSet(d, "auto_induction", AUTO_INDUCTION); // chrisg } else { bindRuleSet(d, "auto_induction", inftyConst()); // chrisg } @@ -285,7 +288,7 @@ private RuleSetDispatchFeature setupCostComputationF() { // chrisg: The following rule is a beta rule that, if active, must have // a higher priority than other beta rules. if (autoInductionLemmaEnabled()) { - bindRuleSet(d, "auto_induction_lemma", JavaCardDLCost.AUTO_INDUCTION_LEMMA); + bindRuleSet(d, "auto_induction_lemma", AUTO_INDUCTION_LEMMA); } else { bindRuleSet(d, "auto_induction_lemma", inftyConst()); } @@ -313,8 +316,8 @@ private void setupSelectSimplification(final RuleSetDispatchFeature d) { add(applyTF("h", not(or(PrimitiveHeapTermFeature.create(heapLDT), anonHeapTermFeature()))), ifZero(applyTF(FocusFormulaProjection.INSTANCE, ff.update), - longConst(HeapSelectCost.PULL_OUT_SELECT_BELOW_UPDATE), - longConst(HeapSelectCost.PULL_OUT_SELECT)), + longConst(PULL_OUT_SELECT_BELOW_UPDATE), + longConst(PULL_OUT_SELECT)), NonDuplicateAppModPositionFeature.INSTANCE)); bindRuleSet(d, "apply_select_eq", // replace non-simplified select by the skolem constant @@ -324,7 +327,7 @@ private void setupSelectSimplification(final RuleSetDispatchFeature d) { ifZero(applyTF("s", not(rec(any(), SimplifiedSelectTermFeature.create(heapLDT)))), // the applyEq taclet also carries apply_equations, so the dispatch sums the // bindings; the tuned sum is CombinationCost.APPLY_SELECT_EQ_EFFECTIVE - longConst(HeapSelectCost.APPLY_SELECT_EQ))); + longConst(APPLY_SELECT_EQ))); bindRuleSet(d, "simplify_select", // simplify_select term in pulled out equation (right hand // side has to be a skolem constant which has been @@ -334,12 +337,12 @@ private void setupSelectSimplification(final RuleSetDispatchFeature d) { add(isSelectSkolemConstantTerm("sk"), applyTF(sub(FocusProjection.INSTANCE, 0), not(SimplifiedSelectTermFeature.create(heapLDT))), - longConst(HeapSelectCost.SIMPLIFY_SELECT))); + longConst(SIMPLIFY_SELECT))); bindRuleSet(d, "simplify_select_concrete", longConst(-6000)); bindRuleSet(d, "simplify_select_elim_store", longConst(-7000)); bindRuleSet(d, "apply_auxiliary_eq", // replace a skolem constant by its computed value - add(isSelectSkolemConstantTerm("t1"), longConst(HeapSelectCost.APPLY_AUXILIARY_EQ))); + add(isSelectSkolemConstantTerm("t1"), longConst(APPLY_AUXILIARY_EQ))); // hide an auxiliary equation once the skolem constant has been replaced by its value final Feature hideReplacedAuxiliaryEq = add(isSelectSkolemConstantTerm("auxiliarySK"), applyTF("result", @@ -350,7 +353,7 @@ private void setupSelectSimplification(final RuleSetDispatchFeature d) { final int pullOutHeapBound = getHeapSizeBound(); bindRuleSet(d, "hide_auxiliary_eq", pullOutHeapBound <= 0 ? add(hideReplacedAuxiliaryEq, longConst(-5400)) - : ifZero(hideReplacedAuxiliaryEq, longConst(HeapSelectCost.HIDE_AUXILIARY_EQ), + : ifZero(hideReplacedAuxiliaryEq, longConst(HIDE_AUXILIARY_EQ), ifZero(isTermAPulledOutHeap(), ifZero(isSkolemConstantUsedElsewhereInSequent(), longConst(-5400), longConst(HIDE_DEFERRAL_COST)), @@ -359,7 +362,7 @@ private void setupSelectSimplification(final RuleSetDispatchFeature d) { // hide an auxiliary equation once the skolem constant has been replaced by its // value add(isSelectSkolemConstantTerm("auxiliarySK"), - longConst(HeapSelectCost.HIDE_AUXILIARY_EQ_CONST))); + longConst(HIDE_AUXILIARY_EQ_CONST))); } private void setupUserTaclets(RuleSetDispatchFeature d) { @@ -367,9 +370,9 @@ private void setupUserTaclets(RuleSetDispatchFeature d) { final String userTacletsProbs = strategyProperties.getProperty(StrategyProperties.userTacletsOptionsKey(i)); if (StrategyProperties.USER_TACLETS_LOW.equals(userTacletsProbs)) { - bindRuleSet(d, "userTaclets" + i, JavaCardDLCost.USER_TACLET_LOW_PRIORITY); + bindRuleSet(d, "userTaclets" + i, USER_TACLET_LOW_PRIORITY); } else if (StrategyProperties.USER_TACLETS_HIGH.equals(userTacletsProbs)) { - bindRuleSet(d, "userTaclets" + i, JavaCardDLCost.USER_TACLET_HIGH_PRIORITY); + bindRuleSet(d, "userTaclets" + i, USER_TACLET_HIGH_PRIORITY); } else { bindRuleSet(d, "userTaclets" + i, inftyConst()); } @@ -494,7 +497,7 @@ protected Feature setupApprovalF() { if (depProp.equals(StrategyProperties.DEP_ON)) { depSpecF = ConditionalFeature.createConditional(depFilter, ifZero(new DependencyContractFeature(), - longConst(JavaCardDLCost.DEPENDENCY_CONTRACT), inftyConst())); + longConst(DEPENDENCY_CONTRACT), inftyConst())); } else { depSpecF = ConditionalFeature.createConditional(depFilter, inftyConst()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/StringStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/StringStrategy.java index 5a2bc6fe493..339637ac505 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/StringStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/StringStrategy.java @@ -30,6 +30,8 @@ import org.jspecify.annotations.NonNull; +import static de.uka.ilkd.key.strategy.StringCost.*; + /// Strategy for string related rules. /// /// Do not create directly; use [StringStrategyFactory] instead. @@ -71,7 +73,7 @@ private RuleSetDispatchFeature setupCostComputationF() { private void setUpStringNormalisation(RuleSetDispatchFeature d) { // translates an integer into its string representation - bindRuleSet(d, "integerToString", StringCost.INTEGER_TO_STRING); + bindRuleSet(d, "integerToString", INTEGER_TO_STRING); // do not convert char to int when inside a string function // feature used to recognize if one is inside a string literal @@ -85,7 +87,7 @@ private void setUpStringNormalisation(RuleSetDispatchFeature d) { or(op(charListLDT.getClReplace()), op(charListLDT.getClLastIndexOfChar())))); bindRuleSet(d, "charLiteral_to_intLiteral", - ifZero(isBelow(keepChar), inftyConst(), longConst(StringCost.CHAR_TO_INT_LITERAL))); + ifZero(isBelow(keepChar), inftyConst(), longConst(CHAR_TO_INT_LITERAL))); // establish normalform @@ -97,7 +99,7 @@ private void setUpStringNormalisation(RuleSetDispatchFeature d) { or(op(seqLDT.getSeqSingleton()), or(anyLiteral, inftyTermConst())))); Feature belowModOpPenality = - ifZero(isBelow(ff.modalOperator), longConst(StringCost.BELOW_MODALITY)); + ifZero(isBelow(ff.modalOperator), longConst(BELOW_MODALITY)); bindRuleSet(d, "defOpsSeqEquality", add(NonDuplicateAppModPositionFeature.INSTANCE, @@ -124,7 +126,7 @@ private void setUpStringNormalisation(RuleSetDispatchFeature d) { bindRuleSet(d, "defOpsReplaceInline", ifZero(add(applyTF("str", seqLiteral), applyTF("searchChar", charOrIntLiteral), - applyTF("replChar", charOrIntLiteral)), longConst(StringCost.REPLACE_INLINE), + applyTF("replChar", charOrIntLiteral)), longConst(REPLACE_INLINE), inftyConst())); bindRuleSet(d, "defOpsReplace", add(NonDuplicateAppModPositionFeature.INSTANCE, diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExStrategy.java index b944d73cea4..fbdcdf353e6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExStrategy.java @@ -32,6 +32,8 @@ import org.jspecify.annotations.NonNull; +import static de.uka.ilkd.key.strategy.SymExCost.*; + /// Strategy for symbolic execution rules. /// /// Do not create directly. Use [SymExStrategyFactory] instead. @@ -92,7 +94,7 @@ private Feature setupGlobalF(Feature dispatcher) { strategyProperties.getProperty(StrategyProperties.METHOD_OPTIONS_KEY); switch (methProp) { case StrategyProperties.METHOD_CONTRACT -> - methodSpecF = methodSpecFeature(longConst(SymExCost.METHOD_CONTRACT_PREFERENCE)); + methodSpecF = methodSpecFeature(longConst(METHOD_CONTRACT_PREFERENCE)); case StrategyProperties.METHOD_EXPAND, StrategyProperties.METHOD_NONE -> methodSpecF = methodSpecFeature(inftyConst()); default -> { @@ -126,7 +128,7 @@ private Feature setupGlobalF(Feature dispatcher) { SumFeature.createSum( loopContractExternalFeature(longConst(CostBand.BLOCK_CONTRACT.cost())), loopContractInternalFeature( - longConst(SymExCost.LOOP_CONTRACT_INTERNAL_TIEBREAK))); + longConst(LOOP_CONTRACT_INTERNAL_TIEBREAK))); loopBlockApplyHeadFeature = loopContractApplyHead(longConst(CostBand.BLOCK_CONTRACT.cost())); } else { @@ -139,7 +141,7 @@ private Feature setupGlobalF(Feature dispatcher) { final String mpsProperty = strategyProperties.getProperty(StrategyProperties.MPS_OPTIONS_KEY); if (mpsProperty.equals(StrategyProperties.MPS_MERGE)) { - mergeRuleF = mergeRuleFeature(longConst(SymExCost.MERGE_RULE)); + mergeRuleF = mergeRuleFeature(longConst(MERGE_RULE)); } else { mergeRuleF = mergeRuleFeature(inftyConst()); } @@ -157,19 +159,19 @@ private RuleSetDispatchFeature setupCostComputationF() { bindRuleSet(d, "simplify_prog", ifZero(ThrownExceptionFeature.create(exceptionsWithPenalty, getServices()), - longConst(SymExCost.THROWING_PROGRAM_STEP), + longConst(THROWING_PROGRAM_STEP), ifZero(isBelow(add(ff.forF, not(ff.atom))), - longConst(SymExCost.PROGRAM_STEP_BELOW_QUANTIFIER), - longConst(SymExCost.PROGRAM_STEP)))); + longConst(PROGRAM_STEP_BELOW_QUANTIFIER), + longConst(PROGRAM_STEP)))); bindRuleSet(d, "simplify_prog_subset", longConst(CostBand.EXECUTE.cost())); - bindRuleSet(d, "simplify_expression", SymExCost.PROGRAM_STEP); + bindRuleSet(d, "simplify_expression", PROGRAM_STEP); bindRuleSet(d, "simplify_java", CostBand.SIMPLIFY.cost()); - bindRuleSet(d, "executeIntegerAssignment", SymExCost.PROGRAM_STEP); - bindRuleSet(d, "executeDoubleAssignment", SymExCost.PROGRAM_STEP); + bindRuleSet(d, "executeIntegerAssignment", PROGRAM_STEP); + bindRuleSet(d, "executeDoubleAssignment", PROGRAM_STEP); final Feature findDepthFeature = FindDepthFeature.getInstance(); @@ -192,7 +194,7 @@ private RuleSetDispatchFeature setupCostComputationF() { bindRuleSet(d, "loop_expand", useLoopExpand ? longConst(0) : inftyConst()); bindRuleSet(d, "loop_scope_inv_taclet", useLoopInvTaclets ? longConst(0) : inftyConst()); bindRuleSet(d, "loop_scope_expand", - useLoopScopeExpand ? longConst(SymExCost.LOOP_SCOPE_EXPAND) : inftyConst()); + useLoopScopeExpand ? longConst(LOOP_SCOPE_EXPAND) : inftyConst()); final String methProp = @@ -205,9 +207,9 @@ private RuleSetDispatchFeature setupCostComputationF() { * is disabled. The original cost was 200 and is now increased to 2000 in order to * repress method expansion stronger when method treatment by contracts is chosen. */ - bindRuleSet(d, "method_expand", longConst(SymExCost.METHOD_EXPAND_REPRESSED)); + bindRuleSet(d, "method_expand", longConst(METHOD_EXPAND_REPRESSED)); case StrategyProperties.METHOD_EXPAND -> - bindRuleSet(d, "method_expand", longConst(SymExCost.METHOD_EXPAND)); + bindRuleSet(d, "method_expand", longConst(METHOD_EXPAND)); case StrategyProperties.METHOD_NONE -> bindRuleSet(d, "method_expand", inftyConst()); default -> throw new RuntimeException("Unexpected strategy property " + methProp); } @@ -237,12 +239,12 @@ private RuleSetDispatchFeature setupCostComputationF() { } }); case StrategyProperties.MPS_SKIP -> - bindRuleSet(d, "merge_point", longConst(SymExCost.MERGE_POINT_SKIP)); + bindRuleSet(d, "merge_point", longConst(MERGE_POINT_SKIP)); case StrategyProperties.MPS_NONE -> bindRuleSet(d, "merge_point", inftyConst()); default -> throw new RuntimeException("Unexpected strategy property " + mpsProp); } - bindRuleSet(d, "modal_tautology", longConst(SymExCost.MODAL_TAUTOLOGY)); + bindRuleSet(d, "modal_tautology", longConst(MODAL_TAUTOLOGY)); if (programsToRight) { bindRuleSet(d, "boxDiamondConv", @@ -250,7 +252,7 @@ private RuleSetDispatchFeature setupCostComputationF() { new FindPrefixRestrictionFeature( FindPrefixRestrictionFeature.PositionModifier.ALLOW_UPDATE_AS_PARENT, FindPrefixRestrictionFeature.PrefixChecker.ANTEC_POLARITY), - longConst(SymExCost.BOX_DIAMOND_CONV))); + longConst(BOX_DIAMOND_CONV))); } else { bindRuleSet(d, "boxDiamondConv", inftyConst()); } @@ -261,7 +263,7 @@ private RuleSetDispatchFeature setupCostComputationF() { final TermBuffer superFor = new TermBuffer(); bindRuleSet(d, "split_if", add(sum(superFor, SuperTermGenerator.upwards(any(), getServices()), - applyTF(superFor, not(ff.program))), longConst(SymExCost.SPLIT_IF))); + applyTF(superFor, not(ff.program))), longConst(SPLIT_IF))); return d; } From 51a0458cb24dd4a19cb24319c3ea142b5587e650 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 10 Jul 2026 12:02:05 +0200 Subject: [PATCH 08/10] 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). --- .../de/uka/ilkd/key/strategy/FOLStrategy.java | 56 +++++++++---------- .../key/strategy/IntegerArithmeticCosts.java | 4 ++ .../ilkd/key/strategy/IntegerStrategy.java | 16 +++--- .../ilkd/key/strategy/JavaCardDLStrategy.java | 8 +-- .../uka/ilkd/key/strategy/StringStrategy.java | 22 ++++---- .../uka/ilkd/key/strategy/SymExStrategy.java | 16 +++--- .../prover/strategy/costbased/CostBand.java | 32 ++++++++--- 7 files changed, 86 insertions(+), 68 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java index 9960d7c9446..4d007d76b9f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java @@ -85,7 +85,7 @@ public FOLStrategy(Proof proof, StrategyProperties strategyProperties) { private Feature setUpGlobalF(RuleSetDispatchFeature d) { final Feature oneStepSimplificationF = - oneStepSimplificationFeature(longConst(CostBand.REWRITE.cost())); + oneStepSimplificationFeature(CostBand.REWRITE.cost()); return add(d, oneStepSimplificationF); } @@ -107,7 +107,7 @@ private RuleSetDispatchFeature setupCostComputationF() { FindDepthFeature.getInstance(); bindRuleSet(d, "concrete", - add(longConst(CostBand.REWRITE.cost()), + add(CostBand.REWRITE.cost(), ScaleFeature.createScaled(findDepthFeature, 10.0))); bindRuleSet(d, "simplify", CostBand.SIMPLIFY.cost()); bindRuleSet(d, "simplify_enlarging", CostBand.ENLARGE.cost()); @@ -123,10 +123,10 @@ private RuleSetDispatchFeature setupCostComputationF() { not(contains(AssumptionProjection.create(0), FocusProjection.INSTANCE)))); bindRuleSet(d, "update_elim", - add(longConst(CostBand.ELIMINATE.cost()), + add(CostBand.ELIMINATE.cost(), ScaleFeature.createScaled(findDepthFeature, 10.0))); bindRuleSet(d, "update_apply_on_update", - add(longConst(CostBand.DECOMPOSE.cost()), + add(CostBand.DECOMPOSE.cost(), ScaleFeature.createScaled(findDepthFeature, 10.0))); bindRuleSet(d, "update_join", CostBand.SIMPLIFY.at(-100)); bindRuleSet(d, "update_apply", CostBand.SIMPLIFY.cost()); @@ -134,17 +134,17 @@ private RuleSetDispatchFeature setupCostComputationF() { setupSplitting(d); bindRuleSet(d, "gamma", add(not(isInstantiated("t")), - ifZero(allowQuantifierSplitting(), longConst(CostBand.DEFAULT.cost()), - longConst(CostBand.DEFAULT.at(50))))); + ifZero(allowQuantifierSplitting(), CostBand.DEFAULT.cost(), + CostBand.DEFAULT.at(50)))); bindRuleSet(d, "gamma_destructive", inftyConst()); bindRuleSet(d, "triggered", - add(not(isTriggerVariableInstantiated()), longConst(CostBand.DEFER.cost()))); + add(not(isTriggerVariableInstantiated()), CostBand.DEFER.cost())); bindRuleSet(d, "comprehension_split", add(applyTF(FocusFormulaProjection.INSTANCE, ff.notContainsExecutable), - ifZero(allowQuantifierSplitting(), longConst(CostBand.DEFER.at(2000)), - longConst(CostBand.DEFER.at(4500))))); + ifZero(allowQuantifierSplitting(), CostBand.DEFER.at(2000), + CostBand.DEFER.at(4500)))); setupReplaceKnown(d); @@ -152,22 +152,22 @@ private RuleSetDispatchFeature setupCostComputationF() { bindRuleSet(d, "order_terms", add(termSmallerThan("commEqLeft", "commEqRight"), - longConst(CostBand.NORMALIZE.cost()))); + CostBand.NORMALIZE.cost())); bindRuleSet(d, "simplify_instanceof_static", - add(EqNonDuplicateAppFeature.INSTANCE, longConst(CostBand.PREFER.cost()))); + add(EqNonDuplicateAppFeature.INSTANCE, CostBand.PREFER.cost())); - bindRuleSet(d, "evaluate_instanceof", longConst(CostBand.PREFER.cost())); + bindRuleSet(d, "evaluate_instanceof", CostBand.PREFER.cost()); bindRuleSet(d, "instanceof_to_exists", TopLevelFindFeature.ANTEC); bindRuleSet(d, "try_apply_subst", - add(EqNonDuplicateAppFeature.INSTANCE, longConst(CostBand.SUBST.cost()))); + add(EqNonDuplicateAppFeature.INSTANCE, CostBand.SUBST.cost())); // delete cast bindRuleSet(d, "cast_deletion", ifZero(implicitCastNecessary(instOf("castedTerm")), - longConst(CostBand.NORMALIZE.cost()), + CostBand.NORMALIZE.cost(), inftyConst())); bindRuleSet(d, "type_hierarchy_def", CostBand.TYPE.at(-500)); @@ -291,13 +291,13 @@ public Name name() { protected void setupFormulaNormalisation(RuleSetDispatchFeature d) { bindRuleSet(d, "negationNormalForm", add(BelowBinderFeature.getInstance(), - longConst(CostBand.PREFER.cost()), + CostBand.PREFER.cost(), ScaleFeature.createScaled(FindDepthFeature.getInstance(), 10.0))); bindRuleSet(d, "moveQuantToLeft", - add(quantifiersMightSplit() ? longConst(CostBand.DEFAULT.cost()) + add(quantifiersMightSplit() ? CostBand.DEFAULT.cost() : applyTF(FocusFormulaProjection.INSTANCE, ff.quantifiedPureLitConjDisj), - longConst(CostBand.PREFER.at(-50)))); + CostBand.PREFER.at(-50))); bindRuleSet(d, "conjNormalForm", ifZero( @@ -307,7 +307,7 @@ protected void setupFormulaNormalisation(RuleSetDispatchFeature d) { ScaleFeature.createScaled(FindDepthFeature.getInstance(), 20)), inftyConst())); - bindRuleSet(d, "setEqualityBlastingRight", longConst(CostBand.DEFAULT.at(-100))); + bindRuleSet(d, "setEqualityBlastingRight", CostBand.DEFAULT.at(-100)); @@ -413,17 +413,17 @@ private void setupQuantifierInstantiation(RuleSetDispatchFeature d) { forEach(varInst, HeuristicInstantiation.forOption(classicTriggers()), add(instantiate("t", varInst), add(branchPrediction, - longConst(CostBand.DEFAULT.at(10), + CostBand.DEFAULT.at(10), // orders candidates of one predicted-cost band by their // connection to the sequent instead of formula position InstantiationTieBreakFeature.create(varInst, - triggersOption()))))))); + triggersOption())))))); final TermBuffer splitInst = new TermBuffer(); bindRuleSet(d, "triggered", SumFeature.createSum(forEach(splitInst, TriggeredInstantiations.create(true), - add(instantiateTriggeredVariable(splitInst), longConst(CostBand.DEFER.cost()))), - longConst(CostBand.DEFER.at(1000)))); + add(instantiateTriggeredVariable(splitInst), CostBand.DEFER.cost())), + CostBand.DEFER.at(1000))); } else { bindRuleSet(d, "gamma", inftyConst()); @@ -440,7 +440,7 @@ private void setupQuantifierInstantiationApproval(RuleSetDispatchFeature d) { not(eq(instOf("t"), varInst)))), InstantiationCostScalerFeature.create( InstantiationCost.create(instOf("t"), classicTriggers()), - longConst(CostBand.DEFAULT.cost())))); + CostBand.DEFAULT.cost()))); final TermBuffer splitInst = new TermBuffer(); bindRuleSet(d, "triggered", @@ -470,7 +470,7 @@ protected Feature notBelowQuantifier() { private void setupReplaceKnown(RuleSetDispatchFeature d) { final Feature commonF = add(ifZero(MatchedAssumesFeature.INSTANCE, DiffFindAndIfFeature.INSTANCE), - longConst(CostBand.NORMALIZE.cost()), + CostBand.NORMALIZE.cost(), add(DiffFindAndReplacewithFeature.INSTANCE, ScaleFeature.createScaled(CountMaxDPathFeature.INSTANCE, 10.0))); @@ -498,10 +498,10 @@ protected void setupSplitting(RuleSetDispatchFeature d) { sum(subFor, AllowedCutPositionsGenerator.INSTANCE, not(applyTF(subFor, ff.cutAllowed))); bindRuleSet(d, "beta", SumFeature.createSum(noCutsAllowed, - ifZero(PurePosDPathFeature.INSTANCE, longConst(CostBand.PREFER.at(300))), + ifZero(PurePosDPathFeature.INSTANCE, CostBand.PREFER.at(300)), ScaleFeature.createScaled(CountPosDPathFeature.INSTANCE, -3.0), ScaleFeature.createScaled(CountMaxDPathFeature.INSTANCE, 10.0), - longConst(CostBand.DEFAULT.at(20)))); + CostBand.DEFAULT.at(20))); TermBuffer superF = new TermBuffer(); final ProjectionToTerm splitCondition = sub(FocusProjection.INSTANCE, 0); bindRuleSet(d, "split_cond", add(// do not split over formulas containing auxiliary @@ -517,7 +517,7 @@ protected void setupSplitting(RuleSetDispatchFeature d) { sum(superF, SuperTermGenerator.upwards(any(), getServices()), applyTF(superF, not(ff.elemUpdate))), ifZero(applyTF(FocusProjection.INSTANCE, ContainsExecutableCodeTermFeature.PROGRAMS), - longConst(CostBand.DEFAULT.at(-100)), longConst(CostBand.DEFAULT.at(25))))); + CostBand.DEFAULT.at(-100), CostBand.DEFAULT.at(25)))); ProjectionToTerm cutFormula = instOf("cutFormula"); Feature countOccurrencesInSeq = ScaleFeature.createAffine(countOccurrences(cutFormula), -10, 10); @@ -539,7 +539,7 @@ protected void setupSplitting(RuleSetDispatchFeature d) { applyTF(FocusFormulaProjection.INSTANCE, ff.quantifiedClauseSet), ifZero(allowQuantifierSplitting(), - longConst(CostBand.DEFAULT.cost()), + CostBand.DEFAULT.cost(), longConst(CUT_DIRECT_STANDARD)))))); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerArithmeticCosts.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerArithmeticCosts.java index fb572e7c594..527151c6a3e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerArithmeticCosts.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerArithmeticCosts.java @@ -10,6 +10,10 @@ * holder is meant to move with its sub-strategy. Cross-theory levels stay in * {@link org.key_project.prover.strategy.costbased.CostBand}; only the arithmetic-internal ordering * lives here. All values are byte-identical to the literals they replace. + * + * The file is named after the integer-arithmetic *theory*; a plain "IntegerCost(s)" would suggest + * an integer-valued cost type (an implementation of RuleAppCost) rather than a holder of cost + * constants. */ /** Polynomial normal-form canonicalisation (Buchberger normalisation) — the "basic" substrate. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java index 3d4eaa6bc00..6fd7bdf60bf 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java @@ -207,7 +207,7 @@ private RuleSetDispatchFeature setupCostComputationF() { bindRuleSet(d, "order_terms", add(applyTF("commEqRight", tf.monomial), applyTF("commEqLeft", tf.polynomial), monSmallerThan("commEqLeft", "commEqRight", numbers), - longConst(CostBand.NORMALIZE.cost()))); + CostBand.NORMALIZE.cost())); final TermBuffer equation = new TermBuffer(); final TermBuffer left = new TermBuffer(); @@ -441,7 +441,7 @@ private void setupDivModDivision(RuleSetDispatchFeature d) { add(NotInScopeOfModalityFeature.INSTANCE, ifZero(isReduciblePolyE, // try again later longConst(-DivModCost.POLY_DIVISION)))))), - longConst(CostBand.DEFAULT.at(100)))); + CostBand.DEFAULT.at(100))); } @@ -787,9 +787,9 @@ private void setupMultiplyInequations(RuleSetDispatchFeature d, Feature baseCost ifZero(MatchedAssumesFeature.INSTANCE, SumFeature.createSum( applyTF("multFacLeft", tf.nonNegMonomial), - ifZero(applyTF("multRight", tf.literal), longConst(CostBand.DEFAULT.at(-100))), + ifZero(applyTF("multRight", tf.literal), CostBand.DEFAULT.at(-100)), ifZero(applyTF("multFacRight", tf.literal), - longConst(CostBand.DEFAULT.at(-100)), + CostBand.DEFAULT.at(-100), applyTF("multFacRight", tf.polynomial)), /* * ifZero ( applyTF ( "multRight", tf.literal ), longConst ( -100 ), applyTF ( @@ -808,9 +808,9 @@ private void setupMultiplyInequations(RuleSetDispatchFeature d, Feature baseCost ? ifZero(BranchMultiplicationCountFeature.atMost("multiply_2_inEq", BRANCH_MULT_CAP), longConst(0), notAllowedF) : longConst(0), - ifZero(exactlyBounded, longConst(CostBand.DEFAULT.cost()), + ifZero(exactlyBounded, CostBand.DEFAULT.cost(), onlyExactlyBounded ? notAllowedF - : ifZero(totallyBounded, longConst(CostBand.DEFAULT.at(100)), notAllowedF)) + : ifZero(totallyBounded, CostBand.DEFAULT.at(100), notAllowedF)) /* * ifZero ( partiallyBounded, longConst ( 400 ), notAllowedF ) ) ), */ @@ -949,9 +949,9 @@ private void setupInEqCaseDistinctions(RuleSetDispatchFeature d) { forEach(rootInf, RootsGenerator.create(intRel, getServices()), add(instantiate("cutFormula", rootInf), ifZero(applyTF(rootInf, op(Junctor.OR)), - longConst(CostBand.DEFAULT.at(50))), + CostBand.DEFAULT.at(50)), ifZero(applyTF(rootInf, op(Junctor.AND)), - longConst(CostBand.DEFAULT.at(20))))), + CostBand.DEFAULT.at(20)))), longConst(NonlinearArithmeticCost.MULTIPLY))); // noinspection unchecked diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java index 82d7e9186e6..8674af6982f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java @@ -217,7 +217,7 @@ private RuleSetDispatchFeature setupCostComputationF() { bindRuleSet(d, "simplify_literals", // ifZero ( ConstraintStrengthenFeatureUC.create(proof), // longConst ( 0 ), - longConst(CostBand.ELIMINATE.cost())); + CostBand.ELIMINATE.cost()); bindRuleSet(d, "nonDuplicateAppCheckEq", EqNonDuplicateAppFeature.INSTANCE); @@ -244,7 +244,7 @@ private RuleSetDispatchFeature setupCostComputationF() { strategyProperties.getProperty(StrategyProperties.QUERYAXIOM_OPTIONS_KEY); switch (queryAxProp) { case StrategyProperties.QUERYAXIOM_ON -> - bindRuleSet(d, "query_axiom", longConst(CostBand.SOLVE.cost())); + bindRuleSet(d, "query_axiom", CostBand.SOLVE.cost()); case StrategyProperties.QUERYAXIOM_OFF -> bindRuleSet(d, "query_axiom", inftyConst()); default -> throw new RuntimeException("Unexpected strategy property " + queryAxProp); } @@ -262,7 +262,7 @@ private RuleSetDispatchFeature setupCostComputationF() { // partial inv axiom bindRuleSet(d, "partialInvAxiom", add(NonDuplicateAppModPositionFeature.INSTANCE, - longConst(CostBand.DEFER_STRONG.cost()))); + CostBand.DEFER_STRONG.cost())); // inReachableState bindRuleSet(d, "inReachableStateImplication", @@ -293,7 +293,7 @@ private RuleSetDispatchFeature setupCostComputationF() { bindRuleSet(d, "auto_induction_lemma", inftyConst()); } - bindRuleSet(d, "information_flow_contract_appl", longConst(CostBand.LAST_RESORT.cost())); + bindRuleSet(d, "information_flow_contract_appl", CostBand.LAST_RESORT.cost()); if (strategyProperties.contains(StrategyProperties.AUTO_INDUCTION_ON) || strategyProperties.contains(StrategyProperties.AUTO_INDUCTION_LEMMA_ON)) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/StringStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/StringStrategy.java index 339637ac505..207e5b1a996 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/StringStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/StringStrategy.java @@ -104,20 +104,20 @@ private void setUpStringNormalisation(RuleSetDispatchFeature d) { bindRuleSet(d, "defOpsSeqEquality", add(NonDuplicateAppModPositionFeature.INSTANCE, ifZero(add(applyTF("left", seqLiteral), applyTF("right", seqLiteral)), - longConst(CostBand.DEFER.at(500)), inftyConst()), + CostBand.DEFER.at(500), inftyConst()), belowModOpPenality)); bindRuleSet(d, "defOpsConcat", add(NonDuplicateAppModPositionFeature.INSTANCE, ifZero( or(applyTF("leftStr", not(seqLiteral)), applyTF("rightStr", not(seqLiteral))), - longConst(CostBand.DEFER.at(500)) + CostBand.DEFER.at(500) // concat is often introduced for construction purposes, // we do not want to use its definition right at the // beginning ), belowModOpPenality)); - bindRuleSet(d, "stringsSimplify", longConst(CostBand.NORMALIZE.cost())); + bindRuleSet(d, "stringsSimplify", CostBand.NORMALIZE.cost()); final TermFeature charOrIntLiteral = or(tf.charLiteral, tf.literal, or(add(OperatorClassTF.create(ParametricFunctionInstance.class), // XXX: @@ -131,14 +131,14 @@ private void setUpStringNormalisation(RuleSetDispatchFeature d) { bindRuleSet(d, "defOpsReplace", add(NonDuplicateAppModPositionFeature.INSTANCE, ifZero(or(applyTF("str", not(seqLiteral)), applyTF("searchChar", not(charOrIntLiteral)), - applyTF("replChar", not(charOrIntLiteral))), longConst(CostBand.DEFER.cost()), + applyTF("replChar", not(charOrIntLiteral))), CostBand.DEFER.cost(), inftyConst()), belowModOpPenality)); bindRuleSet(d, "stringsReduceSubstring", - add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(CostBand.DEFER.at(-400)))); + add(NonDuplicateAppModPositionFeature.INSTANCE, CostBand.DEFER.at(-400))); - bindRuleSet(d, "defOpsStartsEndsWith", longConst(CostBand.DEFER.at(-250))); + bindRuleSet(d, "defOpsStartsEndsWith", CostBand.DEFER.at(-250)); bindRuleSet(d, "stringsConcatNotBothLiterals", ifZero(MatchedAssumesFeature.INSTANCE, ifZero( @@ -146,21 +146,21 @@ private void setUpStringNormalisation(RuleSetDispatchFeature d) { applyTF(instOf("rightStr"), seqLiteral)), inftyConst()), inftyConst())); - bindRuleSet(d, "stringsReduceConcat", longConst(CostBand.DEFER.at(-400))); + bindRuleSet(d, "stringsReduceConcat", CostBand.DEFER.at(-400)); bindRuleSet(d, "stringsReduceOrMoveOutsideConcat", - ifZero(NonDuplicateAppModPositionFeature.INSTANCE, longConst(CostBand.DEFER.at(300)), + ifZero(NonDuplicateAppModPositionFeature.INSTANCE, CostBand.DEFER.at(300), inftyConst())); bindRuleSet(d, "stringsMoveReplaceInside", - ifZero(NonDuplicateAppModPositionFeature.INSTANCE, longConst(CostBand.DEFER.at(-100)), + ifZero(NonDuplicateAppModPositionFeature.INSTANCE, CostBand.DEFER.at(-100), inftyConst())); - bindRuleSet(d, "stringsExpandDefNormalOp", longConst(CostBand.DEFER.cost())); + bindRuleSet(d, "stringsExpandDefNormalOp", CostBand.DEFER.cost()); bindRuleSet(d, "stringsContainsDefInline", SumFeature - .createSum(EqNonDuplicateAppFeature.INSTANCE, longConst(CostBand.DEFER.at(500)))); + .createSum(EqNonDuplicateAppFeature.INSTANCE, CostBand.DEFER.at(500))); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExStrategy.java index fbdcdf353e6..d782ad55aac 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExStrategy.java @@ -117,20 +117,20 @@ private Feature setupGlobalF(Feature dispatcher) { final String blockProperty = strategyProperties.getProperty(StrategyProperties.BLOCK_OPTIONS_KEY); if (blockProperty.equals(StrategyProperties.BLOCK_CONTRACT_INTERNAL)) { - blockFeature = blockContractInternalFeature(longConst(CostBand.BLOCK_CONTRACT.cost())); + blockFeature = blockContractInternalFeature(CostBand.BLOCK_CONTRACT.cost()); loopBlockFeature = - loopContractInternalFeature(longConst(CostBand.BLOCK_CONTRACT.cost())); + loopContractInternalFeature(CostBand.BLOCK_CONTRACT.cost()); loopBlockApplyHeadFeature = - loopContractApplyHead(longConst(CostBand.BLOCK_CONTRACT.cost())); + loopContractApplyHead(CostBand.BLOCK_CONTRACT.cost()); } else if (blockProperty.equals(StrategyProperties.BLOCK_CONTRACT_EXTERNAL)) { - blockFeature = blockContractExternalFeature(longConst(CostBand.BLOCK_CONTRACT.cost())); + blockFeature = blockContractExternalFeature(CostBand.BLOCK_CONTRACT.cost()); loopBlockFeature = SumFeature.createSum( - loopContractExternalFeature(longConst(CostBand.BLOCK_CONTRACT.cost())), + loopContractExternalFeature(CostBand.BLOCK_CONTRACT.cost()), loopContractInternalFeature( longConst(LOOP_CONTRACT_INTERNAL_TIEBREAK))); loopBlockApplyHeadFeature = - loopContractApplyHead(longConst(CostBand.BLOCK_CONTRACT.cost())); + loopContractApplyHead(CostBand.BLOCK_CONTRACT.cost()); } else { blockFeature = blockContractInternalFeature(inftyConst()); loopBlockFeature = loopContractExternalFeature(inftyConst()); @@ -164,7 +164,7 @@ private RuleSetDispatchFeature setupCostComputationF() { longConst(PROGRAM_STEP_BELOW_QUANTIFIER), longConst(PROGRAM_STEP)))); - bindRuleSet(d, "simplify_prog_subset", longConst(CostBand.EXECUTE.cost())); + bindRuleSet(d, "simplify_prog_subset", CostBand.EXECUTE.cost()); bindRuleSet(d, "simplify_expression", PROGRAM_STEP); @@ -176,7 +176,7 @@ private RuleSetDispatchFeature setupCostComputationF() { final Feature findDepthFeature = FindDepthFeature.getInstance(); bindRuleSet(d, "concrete_java", - add(longConst(CostBand.REWRITE.cost()), + add(CostBand.REWRITE.cost(), ScaleFeature.createScaled(findDepthFeature, 10.0))); // taclets for special invariant handling diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/CostBand.java b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/CostBand.java index dfbe711c025..36f535485a6 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/CostBand.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/CostBand.java @@ -3,6 +3,9 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.prover.strategy.costbased; +import org.key_project.prover.strategy.costbased.feature.ConstFeature; +import org.key_project.prover.strategy.costbased.feature.Feature; + /** * The shared, cross-theory priority ladder for the cost-based strategies. * @@ -12,8 +15,11 @@ * against every other theory — in practice the theories interleave at almost every * step. A band is therefore combination-relevant. The fine ordering of rules within a * band is expressed as {@code TIER.at(delta)} with a small delta; ordering that is internal to a - * single theory lives in that theory (e.g. {@code IntegerCost} for the integer (in)equality and - * division solver steps), not here. + * single theory lives in that theory's cost holder (e.g. {@code LinearInequationCost} for the + * integer inequation solver steps), not here. Theory-local constants are deliberately + * absolute values on the same cost line, not anchored to a band: they order the theory's + * own steps among each other and are unaffected when a tier is retuned — retuning a band moves + * exactly those rules that were deliberately placed on it. *

* *

@@ -78,21 +84,29 @@ public enum CostBand { LAST_RESORT(1_000_000); private final long base; + private final Feature costFeature; CostBand(long base) { this.base = base; + this.costFeature = ConstFeature.createConst(NumberRuleAppCost.create(base)); } - /** The band's cost. */ - public long cost() { - return base; + /** The band's cost, as a constant strategy {@link Feature} (ready to use in feature terms). */ + public Feature cost() { + return costFeature; } /** - * The band's cost shifted by a small theory-internal ordering delta. Use only for fine - * ordering within the band; larger, cross-theory steps deserve their own band. + * The band's cost shifted by a small theory-internal ordering delta, as a constant strategy + * {@link Feature}. Use only for fine ordering within the band; larger, cross-theory steps + * deserve their own band. */ - public long at(long delta) { - return base + delta; + public Feature at(long delta) { + return ConstFeature.createConst(NumberRuleAppCost.create(base + delta)); + } + + /** The band's raw cost value. */ + public long value() { + return base; } } From d1476294445d63ce38c1ae249c4f35d6dde0425c Mon Sep 17 00:00:00 2001 From: Drodt Date: Mon, 17 Aug 2026 08:31:27 +0200 Subject: [PATCH 09/10] Fix compilation error and move SymEx specific constants to SymExCost --- .../de/uka/ilkd/key/strategy/FOLStrategy.java | 2 +- .../uka/ilkd/key/strategy/IntegerStrategy.java | 5 +++-- .../de/uka/ilkd/key/strategy/SymExCost.java | 17 +++++++++++++++++ .../de/uka/ilkd/key/strategy/SymExStrategy.java | 14 +++++++------- .../prover/strategy/costbased/CostBand.java | 14 +------------- 5 files changed, 29 insertions(+), 23 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java index 4d007d76b9f..796cfa8b09a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java @@ -413,7 +413,7 @@ private void setupQuantifierInstantiation(RuleSetDispatchFeature d) { forEach(varInst, HeuristicInstantiation.forOption(classicTriggers()), add(instantiate("t", varInst), add(branchPrediction, - CostBand.DEFAULT.at(10), + CostBand.DEFAULT.at(10), // orders candidates of one predicted-cost band by their // connection to the sequent instead of formula position InstantiationTieBreakFeature.create(varInst, diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java index 6fd7bdf60bf..f070759d05f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java @@ -615,8 +615,9 @@ private void setupInEqSimp(RuleSetDispatchFeature d, IntegerLDT numbers) { // category "handling of non-linear inequations" if (arith == ArithTreatment.MODEL_SEARCH) { - setupMultiplyInequations(d, longConst(IN_EQ_SIMP_NON_LIN_COST), longConst(CostBand.DEFAULT.at(100), - AT_COST)); + setupMultiplyInequations(d, longConst(IN_EQ_SIMP_NON_LIN_COST), + CostBand.DEFAULT.at(100), + AT_COST); bindRuleSet(d, "inEqSimp_split_eq", add(TopLevelFindFeature.SUCC, longConst(NonlinearArithmeticCost.SPLIT_EQ))); diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExCost.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExCost.java index 798fdde2cef..d7691d47825 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExCost.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExCost.java @@ -20,6 +20,23 @@ final class SymExCost { private SymExCost() {} + /** + * Apply a block/loop contract instead of executing the block. MUST stay more eager (smaller) + * than {@link org.key_project.prover.strategy.costbased.CostBand#REWRITE} and every + * symbolic-execution program rule, otherwise the block starts + * to execute instead of being contracted. Value is the current sentinel; step 3 normalizes it + * to a modest value between {@link org.key_project.prover.strategy.costbased.CostBand#CLOSE} + * and {@link org.key_project.prover.strategy.costbased.CostBand#REWRITE}. + */ + static final long BLOCK_CONTRACT = Long.MIN_VALUE; + /** + * Apply a loop invariant instead of unrolling. Only needs to beat loop-unrolling / method + * expansion when enabled. (Currently above + * {@link org.key_project.prover.strategy.costbased.CostBand#CLOSE}; step 3 flips it below + * CLOSE.) + */ + static final long LOOP_INVARIANT = -20_000; + /** * A cheap concrete program step: {@code simplify_expression}, {@code execute*Assignment} and * the ordinary {@code simplify_prog} case — "advance the program by one small step". diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExStrategy.java index d782ad55aac..1511ae3ef29 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExStrategy.java @@ -117,20 +117,20 @@ private Feature setupGlobalF(Feature dispatcher) { final String blockProperty = strategyProperties.getProperty(StrategyProperties.BLOCK_OPTIONS_KEY); if (blockProperty.equals(StrategyProperties.BLOCK_CONTRACT_INTERNAL)) { - blockFeature = blockContractInternalFeature(CostBand.BLOCK_CONTRACT.cost()); + blockFeature = blockContractInternalFeature(longConst(BLOCK_CONTRACT)); loopBlockFeature = - loopContractInternalFeature(CostBand.BLOCK_CONTRACT.cost()); + loopContractInternalFeature(longConst(BLOCK_CONTRACT)); loopBlockApplyHeadFeature = - loopContractApplyHead(CostBand.BLOCK_CONTRACT.cost()); + loopContractApplyHead(longConst(BLOCK_CONTRACT)); } else if (blockProperty.equals(StrategyProperties.BLOCK_CONTRACT_EXTERNAL)) { - blockFeature = blockContractExternalFeature(CostBand.BLOCK_CONTRACT.cost()); + blockFeature = blockContractExternalFeature(longConst(BLOCK_CONTRACT)); loopBlockFeature = SumFeature.createSum( - loopContractExternalFeature(CostBand.BLOCK_CONTRACT.cost()), + loopContractExternalFeature(longConst(BLOCK_CONTRACT)), loopContractInternalFeature( longConst(LOOP_CONTRACT_INTERNAL_TIEBREAK))); loopBlockApplyHeadFeature = - loopContractApplyHead(CostBand.BLOCK_CONTRACT.cost()); + loopContractApplyHead(longConst(BLOCK_CONTRACT)); } else { blockFeature = blockContractInternalFeature(inftyConst()); loopBlockFeature = loopContractExternalFeature(inftyConst()); @@ -180,7 +180,7 @@ private RuleSetDispatchFeature setupCostComputationF() { ScaleFeature.createScaled(findDepthFeature, 10.0))); // taclets for special invariant handling - bindRuleSet(d, "loopInvariant", CostBand.LOOP_INVARIANT.cost()); + bindRuleSet(d, "loopInvariant", longConst(LOOP_INVARIANT)); boolean useLoopExpand = strategyProperties.getProperty(StrategyProperties.LOOP_OPTIONS_KEY) .equals(StrategyProperties.LOOP_EXPAND); diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/CostBand.java b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/CostBand.java index 36f535485a6..63bc0686467 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/CostBand.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/CostBand.java @@ -26,22 +26,10 @@ * Care when changing: altering a band's value, or its order relative to other bands, * shifts the cross-theory search of all proofs — always re-verify with a full * runAllProofs and a Model-Search node-for-node comparison. Respect the hard ordering - * constraints noted on individual bands (notably {@link #BLOCK_CONTRACT}). + * constraints noted on individual bands. *

*/ public enum CostBand { - /** - * Apply a block/loop contract instead of executing the block. MUST stay more eager (smaller) - * than {@link #REWRITE} and every symbolic-execution program rule, otherwise the block starts - * to execute instead of being contracted. Value is the current sentinel; step 3 normalizes it - * to a modest value between {@link #CLOSE} and {@link #REWRITE}. - */ - BLOCK_CONTRACT(Long.MIN_VALUE), - /** - * Apply a loop invariant instead of unrolling. Only needs to beat loop-unrolling / method - * expansion when enabled. (Currently above {@link #CLOSE}; step 3 flips it below CLOSE.) - */ - LOOP_INVARIANT(-20_000), /** * Close the goal. Most eager of the ordinary bands: eager closure is completeness-neutral * (no free-variable calculus), so closing may always take precedence. From a1139a157d873b81da4fc0b56df5e88acbec1894 Mon Sep 17 00:00:00 2001 From: Drodt Date: Mon, 17 Aug 2026 10:12:28 +0200 Subject: [PATCH 10/10] Integrate set into new structure --- .../de/uka/ilkd/key/strategy/JavaCardDLCosts.java | 3 --- .../java/de/uka/ilkd/key/strategy/SetCosts.java | 14 ++++++++++++++ .../java/de/uka/ilkd/key/strategy/SetStrategy.java | 12 ++++++++---- 3 files changed, 22 insertions(+), 7 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/strategy/SetCosts.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLCosts.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLCosts.java index 78a371093ef..9e978ea3c89 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLCosts.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLCosts.java @@ -34,9 +34,6 @@ private JavaCardDLCost() {} */ static final long JAVA_INTEGER_SEMANTICS = -5000; - /** Loc-set CNF commutation ({@code cnf_setComm}). */ - static final long LOCSET_CNF_COMMUTE = -800; - /** Apply a class axiom ({@code classAxiom}). */ static final long CLASS_AXIOM = -250; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/SetCosts.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/SetCosts.java new file mode 100644 index 00000000000..c0132bd13da --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/SetCosts.java @@ -0,0 +1,14 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.strategy; + +public final class SetCosts { + private SetCosts() {} + + /// Set commutation (`setComm`). + static final long COMMUTE = -800; + + /// Set distribution (`setDist`). + static final long DIST = -2000; +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/SetStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/SetStrategy.java index e4adec94f3e..a67f2b7642c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/SetStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/SetStrategy.java @@ -19,6 +19,7 @@ import org.key_project.prover.rules.RuleApp; import org.key_project.prover.rules.RuleSet; import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.prover.strategy.costbased.CostBand; import org.key_project.prover.strategy.costbased.MutableState; import org.key_project.prover.strategy.costbased.RuleAppCost; import org.key_project.prover.strategy.costbased.feature.Feature; @@ -27,6 +28,9 @@ import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; +import static de.uka.ilkd.key.strategy.SetCosts.COMMUTE; +import static de.uka.ilkd.key.strategy.SetCosts.DIST; + /// Strategy for the sort generic theory of sets. /// Do not create directly; use [SetStrategyFactory] instead. public class SetStrategy extends AbstractFeatureStrategy implements ComponentStrategy { @@ -49,7 +53,7 @@ public SetStrategy(Proof proof, StrategyProperties strategyProperties) { private RuleSetDispatchFeature setupCostComputationF() { final RuleSetDispatchFeature d = new RuleSetDispatchFeature(); - bindRuleSet(d, "setEqualityBlastingRight", longConst(-90)); + bindRuleSet(d, "setEqualityBlastingRight", CostBand.DEFAULT.at(-90)); // Distribution duplicates the distributed set, so it is allowed only // where a resulting set is known to collapse. @@ -57,8 +61,8 @@ private RuleSetDispatchFeature setupCostComputationF() { final Feature operandCollapses = or(applyTF("distributedSet", collapses), applyTF("unionLeft", collapses), applyTF("unionRight", collapses)); bindRuleSet(d, "setDist", - add(ifZero(MatchedAssumesFeature.INSTANCE, operandCollapses, longConst(0)), - longConst(-2000))); + add(ifZero(MatchedAssumesFeature.INSTANCE, operandCollapses, CostBand.DEFAULT.cost()), + longConst(DIST))); bindRuleSet(d, "setAssoc", longConst(-850)); @@ -68,7 +72,7 @@ private RuleSetDispatchFeature setupCostComputationF() { add(applyTF("commLeft", not(or(stf.unionF, stf.intersectF))), applyTF("commRight", not(or(stf.unionF, stf.intersectF))), SetsSmallerThanFeature.create(instOf("commRight"), instOf("commLeft"), stf), - longConst(-800))); + longConst(COMMUTE))); return d; }