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 new file mode 100644 index 00000000000..1cd7907686f --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLCost.java @@ -0,0 +1,52 @@ +/* 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() {} + + /** + * 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. 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; + + /** + * 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 df761fb94bb..2dc7bdb0162 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; @@ -42,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. /// @@ -82,7 +85,7 @@ public FOLStrategy(Proof proof, StrategyProperties strategyProperties) { private Feature setUpGlobalF(RuleSetDispatchFeature d) { final Feature oneStepSimplificationF = - oneStepSimplificationFeature(longConst(-11000)); + oneStepSimplificationFeature(CostBand.REWRITE.cost()); return add(d, oneStepSimplificationF); } @@ -95,20 +98,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(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 +123,54 @@ private RuleSetDispatchFeature setupCostComputationF() { not(contains(AssumptionProjection.create(0), FocusProjection.INSTANCE)))); bindRuleSet(d, "update_elim", - add(longConst(-8000), ScaleFeature.createScaled(findDepthFeature, 10.0))); + add(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(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(), CostBand.DEFAULT.cost(), + CostBand.DEFAULT.at(50)))); bindRuleSet(d, "gamma_destructive", inftyConst()); - bindRuleSet(d, "triggered", add(not(isTriggerVariableInstantiated()), longConst(500))); + bindRuleSet(d, "triggered", + add(not(isTriggerVariableInstantiated()), CostBand.DEFER.cost())); bindRuleSet(d, "comprehension_split", add(applyTF(FocusFormulaProjection.INSTANCE, ff.notContainsExecutable), - ifZero(allowQuantifierSplitting(), longConst(2500), longConst(5000)))); + ifZero(allowQuantifierSplitting(), CostBand.DEFER.at(2000), + CostBand.DEFER.at(4500)))); setupReplaceKnown(d); setupEquationReasoning(d); bindRuleSet(d, "order_terms", - add(termSmallerThan("commEqLeft", "commEqRight"), longConst(-5000))); + add(termSmallerThan("commEqLeft", "commEqRight"), + CostBand.NORMALIZE.cost())); bindRuleSet(d, "simplify_instanceof_static", - add(EqNonDuplicateAppFeature.INSTANCE, longConst(-500))); + add(EqNonDuplicateAppFeature.INSTANCE, CostBand.PREFER.cost())); - bindRuleSet(d, "evaluate_instanceof", longConst(-500)); + bindRuleSet(d, "evaluate_instanceof", CostBand.PREFER.cost()); bindRuleSet(d, "instanceof_to_exists", TopLevelFindFeature.ANTEC); bindRuleSet(d, "try_apply_subst", - add(EqNonDuplicateAppFeature.INSTANCE, longConst(-10000))); + add(EqNonDuplicateAppFeature.INSTANCE, CostBand.SUBST.cost())); // delete cast bindRuleSet(d, "cast_deletion", - ifZero(implicitCastNecessary(instOf("castedTerm")), longConst(-5000), inftyConst())); + ifZero(implicitCastNecessary(instOf("castedTerm")), + 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,24 +291,24 @@ public Name name() { protected void setupFormulaNormalisation(RuleSetDispatchFeature d) { bindRuleSet(d, "negationNormalForm", add(BelowBinderFeature.getInstance(), - longConst(-500), + CostBand.PREFER.cost(), ScaleFeature.createScaled(FindDepthFeature.getInstance(), 10.0))); bindRuleSet(d, "moveQuantToLeft", - add(quantifiersMightSplit() ? longConst(0) + add(quantifiersMightSplit() ? CostBand.DEFAULT.cost() : applyTF(FocusFormulaProjection.INSTANCE, ff.quantifiedPureLitConjDisj), - longConst(-550))); + CostBand.PREFER.at(-50))); bindRuleSet(d, "conjNormalForm", ifZero( add(or(FocusInAntecFeature.getInstance(), notBelowQuantifier()), NotInScopeOfModalityFeature.INSTANCE), - add(longConst(-150), + add(longConst(CombinationCost.CNF_CONVERSION), ScaleFeature.createScaled(FindDepthFeature.getInstance(), 20)), inftyConst())); - 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(); @@ -305,7 +316,7 @@ protected void setupFormulaNormalisation(RuleSetDispatchFeature d) { add(let(left, instOf("applyEqLeft"), let(right, instOf("applyEqRight"), TermSmallerThanFeature.create(right, left))), - longConst(-150))); + longConst(CombinationCost.CNF_CONVERSION))); bindRuleSet(d, "distrQuantifier", add(or( @@ -317,28 +328,30 @@ protected void setupFormulaNormalisation(RuleSetDispatchFeature d) { ifZero(FocusInAntecFeature.getInstance(), applyTF(FocusProjection.INSTANCE, sub(ff.andF)), applyTF(FocusProjection.INSTANCE, sub(ff.orF))))), - longConst(-300))); + longConst(QUANTIFIER_DISTRIBUTION))); bindRuleSet(d, "swapQuantifiers", add(applyTF(FocusProjection.INSTANCE, add(ff.quantifiedClauseSet, EliminableQuantifierTF.INSTANCE, sub(not(EliminableQuantifierTF.INSTANCE)))), - longConst(-300))); + 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(-80))); + applyTF("assoc1", ff.clause), applyTF("assoc2", ff.literal), + longConst(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(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(CNF_RESTRUCTURE + 20), applyTF("distLeft", ff.clauseSet)), + longConst(CNF_RESTRUCTURE))); final TermBuffer superFor = new TermBuffer(); final Feature onlyBelowQuanAndOr = @@ -360,13 +373,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", PULL_OUT_QUANTIFIER); bindRuleSet(d, "pullOutQuantifierAll", add(pullOutQuantifierAllowed, - ifZero(FocusInAntecFeature.getInstance(), longConst(-20), longConst(-40)))); + ifZero(FocusInAntecFeature.getInstance(), longConst(PULL_OUT_QUANTIFIER), + longConst(PULL_OUT_QUANTIFIER_REVERSE)))); bindRuleSet(d, "pullOutQuantifierEx", add(pullOutQuantifierAllowed, - ifZero(FocusInAntecFeature.getInstance(), longConst(-40), longConst(-20)))); + ifZero(FocusInAntecFeature.getInstance(), + longConst(PULL_OUT_QUANTIFIER_REVERSE), + longConst(PULL_OUT_QUANTIFIER)))); } // ////////////////////////////////////////////////////////////////////////// @@ -392,7 +408,8 @@ private void setupQuantifierInstantiation(RuleSetDispatchFeature d) { : ff.notContainsExecutable)), forEach(varInst, HeuristicInstantiation.forOption(classicTriggers()), add(instantiate("t", varInst), - add(branchPrediction, longConst(10), + add(branchPrediction, + CostBand.DEFAULT.at(10), // orders candidates of one predicted-cost band by their // connection to the sequent instead of formula position InstantiationTieBreakFeature.create(varInst, @@ -401,8 +418,8 @@ private void setupQuantifierInstantiation(RuleSetDispatchFeature d) { bindRuleSet(d, "triggered", SumFeature.createSum(forEach(splitInst, TriggeredInstantiations.create(true), - add(instantiateTriggeredVariable(splitInst), longConst(500))), - longConst(1500))); + add(instantiateTriggeredVariable(splitInst), CostBand.DEFER.cost())), + CostBand.DEFER.at(1000))); } else { bindRuleSet(d, "gamma", inftyConst()); @@ -419,7 +436,7 @@ private void setupQuantifierInstantiationApproval(RuleSetDispatchFeature d) { not(eq(instOf("t"), varInst)))), InstantiationCostScalerFeature.create( InstantiationCost.create(instOf("t"), classicTriggers()), - longConst(0)))); + CostBand.DEFAULT.cost()))); final TermBuffer splitInst = new TermBuffer(); bindRuleSet(d, "triggered", @@ -449,15 +466,18 @@ protected Feature notBelowQuantifier() { private void setupReplaceKnown(RuleSetDispatchFeature d) { final Feature commonF = add(ifZero(MatchedAssumesFeature.INSTANCE, DiffFindAndIfFeature.INSTANCE), - longConst(-5000), + 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(REPLACE_KNOWN_UNDER_CONNECTIVE), + ifZero(directlyBelowSymbolAtIndex(Equality.EQV, -1), + longConst(REPLACE_KNOWN_UNDER_CONNECTIVE))))); } // ////////////////////////////////////////////////////////////////////////// @@ -474,9 +494,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, CostBand.PREFER.at(300)), ScaleFeature.createScaled(CountPosDPathFeature.INSTANCE, -3.0), - ScaleFeature.createScaled(CountMaxDPathFeature.INSTANCE, 10.0), longConst(20))); + ScaleFeature.createScaled(CountMaxDPathFeature.INSTANCE, 10.0), + 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 @@ -492,7 +513,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)))); + CostBand.DEFAULT.at(-100), CostBand.DEFAULT.at(25)))); ProjectionToTerm cutFormula = instOf("cutFormula"); Feature countOccurrencesInSeq = ScaleFeature.createAffine(countOccurrences(cutFormula), -10, 10); @@ -508,13 +529,14 @@ protected void setupSplitting(RuleSetDispatchFeature d) { // auxiliary variables rec(any(), not(selectSkolemConstantTermFeature())))), countOccurrencesInSeq, // standard costs - longConst(100)), + longConst(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(), + CostBand.DEFAULT.cost(), + longConst(CUT_DIRECT_STANDARD)))))); } private void setupSplittingApproval(RuleSetDispatchFeature d) { @@ -563,7 +585,7 @@ private void setupEquationReasoning(RuleSetDispatchFeature d) { let(left, sub(equation, 0), let(right, sub(equation, 1), TermSmallerThanFeature.create(right, left))))))), - longConst(-4000))); + 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/IntegerArithmeticCosts.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerArithmeticCosts.java new file mode 100644 index 00000000000..527151c6a3e --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerArithmeticCosts.java @@ -0,0 +1,126 @@ +/* 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. + * + * 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. */ +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 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 — 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_MONOMIAL_TIEBREAK = 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 5c0458c1fcb..25956a439e1 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 @@ -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; @@ -206,7 +207,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), + CostBand.NORMALIZE.cost())); final TermBuffer equation = new TermBuffer(); final TermBuffer left = new TermBuffer(); @@ -229,7 +231,7 @@ private RuleSetDispatchFeature setupCostComputationF() { applyTF(right, tf.polynomial), MonomialsSmallerThanFeature.create(right, left, numbers)))))))), - longConst(-4000))); + longConst(CombinationCost.ORDERED_REWRITING))); final TermBuffer l = new TermBuffer(); final TermBuffer r = new TermBuffer(); @@ -238,7 +240,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(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 @@ -271,77 +273,78 @@ 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)), - longConst(-35))); + longConst(PolynomialCost.DISTRIBUTE))); // category "direct equations" @@ -354,10 +357,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 @@ -380,13 +383,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_MONOMIAL_TIEBREAK))); - bindRuleSet(d, "polySimp_applyEqRigid", add(eqMonomialFeature, longConst(2))); + bindRuleSet(d, "polySimp_applyEqRigid", + add(eqMonomialFeature, longConst(LinearEquationCost.APPLY_EQ_MONOMIAL_TIEBREAK + 1))); // bindRuleSet(d, "defOps_expandModulo", - add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(-600))); + add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(DivModCost.EXPAND_MODULO))); // category "saturate" @@ -434,8 +439,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)))))), + CostBand.DEFAULT.at(100))); } @@ -526,14 +531,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", @@ -558,7 +564,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), @@ -589,9 +595,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), @@ -608,10 +614,12 @@ 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), + setupMultiplyInequations(d, longConst(IN_EQ_SIMP_NON_LIN_COST), + 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) { @@ -782,8 +790,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), CostBand.DEFAULT.at(-100)), + ifZero(applyTF("multFacRight", tf.literal), + CostBand.DEFAULT.at(-100), applyTF("multFacRight", tf.polynomial)), /* * ifZero ( applyTF ( "multRight", tf.literal ), longConst ( -100 ), applyTF ( @@ -802,9 +811,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, CostBand.DEFAULT.cost(), onlyExactlyBounded ? notAllowedF - : ifZero(totallyBounded, longConst(100), notAllowedF)) + : ifZero(totallyBounded, CostBand.DEFAULT.at(100), notAllowedF)) /* * ifZero ( partiallyBounded, longConst ( 400 ), notAllowedF ) ) ), */ @@ -841,7 +850,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" @@ -919,7 +929,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 ) ) ) @@ -931,7 +941,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 ) ) ) @@ -941,9 +951,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)), + CostBand.DEFAULT.at(50)), + ifZero(applyTF(rootInf, op(Junctor.AND)), + CostBand.DEFAULT.at(20)))), + longConst(NonlinearArithmeticCost.MULTIPLY))); // noinspection unchecked bindRuleSet(d, "cut", oneOf(new Feature[] { strengthening, rootInferences })); @@ -1019,32 +1031,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()); @@ -1068,13 +1080,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)))); } /** 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 new file mode 100644 index 00000000000..9e978ea3c89 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLCosts.java @@ -0,0 +1,128 @@ +/* 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 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 + * {@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; + + /** 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; +} + + +/** + * 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 82875fa1ddf..2a4ab73d523 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 @@ -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; @@ -37,6 +38,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. @@ -132,7 +136,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(DEPENDENCY_CONTRACT)); } else { depSpecF = ConditionalFeature.createConditional(depFilter, inftyConst()); } @@ -182,8 +187,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(JAVA_INTEGER_SEMANTICS), + ifZero( + leq(CountBranchFeature.INSTANCE, longConst(1)), + longConst(JAVA_INTEGER_SEMANTICS), inftyConst()))); setupSelectSimplification(d); @@ -195,19 +202,22 @@ private RuleSetDispatchFeature setupCostComputationF() { bindRuleSet(d, "simplify_literals", // ifZero ( ConstraintStrengthenFeatureUC.create(proof), // longConst ( 0 ), - longConst(-8000)); + CostBand.ELIMINATE.cost()); bindRuleSet(d, "nonDuplicateAppCheckEq", EqNonDuplicateAppFeature.INSTANCE); // TODO: rename rule set? bindRuleSet(d, "comprehensions", - add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(-50))); + add(NonDuplicateAppModPositionFeature.INSTANCE, + longConst(COMPREHENSION))); bindRuleSet(d, "comprehensions_high_costs", - add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(10000))); + add(NonDuplicateAppModPositionFeature.INSTANCE, + longConst(COMPREHENSION_ENLARGE))); bindRuleSet(d, "comprehensions_low_costs", - add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(-5000))); + add(NonDuplicateAppModPositionFeature.INSTANCE, + longConst(COMPREHENSION_SIMPLIFY))); // features influenced by the strategy options /* @@ -219,13 +229,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", 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(CLASS_AXIOM)); } else { bindRuleSet(d, "classAxiom", inftyConst()); } @@ -236,15 +246,18 @@ private RuleSetDispatchFeature setupCostComputationF() { // partial inv axiom bindRuleSet(d, "partialInvAxiom", - add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(10000))); + add(NonDuplicateAppModPositionFeature.INSTANCE, + CostBand.DEFER_STRONG.cost())); // inReachableState bindRuleSet(d, "inReachableStateImplication", - add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(100))); + add(NonDuplicateAppModPositionFeature.INSTANCE, + longConst(IN_REACHABLE_STATE))); // limit observer (must have better priority than "classAxiom") bindRuleSet(d, "limitObserver", - add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(-200))); + add(NonDuplicateAppModPositionFeature.INSTANCE, + longConst(LIMIT_OBSERVER))); setupUserTaclets(d); @@ -252,7 +265,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", AUTO_INDUCTION); // chrisg } else { bindRuleSet(d, "auto_induction", inftyConst()); // chrisg } @@ -260,12 +273,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", AUTO_INDUCTION_LEMMA); } else { bindRuleSet(d, "auto_induction_lemma", inftyConst()); } - bindRuleSet(d, "information_flow_contract_appl", longConst(1000000)); + bindRuleSet(d, "information_flow_contract_appl", CostBand.LAST_RESORT.cost()); if (strategyProperties.contains(StrategyProperties.AUTO_INDUCTION_ON) || strategyProperties.contains(StrategyProperties.AUTO_INDUCTION_LEMMA_ON)) { @@ -287,8 +300,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(PULL_OUT_SELECT_BELOW_UPDATE), + longConst(PULL_OUT_SELECT)), NonDuplicateAppModPositionFeature.INSTANCE)); bindRuleSet(d, "apply_select_eq", // replace non-simplified select by the skolem constant @@ -296,9 +310,9 @@ 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 - longConst(-1700))); + // the applyEq taclet also carries apply_equations, so the dispatch sums the + // bindings; the tuned sum is CombinationCost.APPLY_SELECT_EQ_EFFECTIVE + 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 @@ -308,12 +322,12 @@ private void setupSelectSimplification(final RuleSetDispatchFeature d) { add(isSelectSkolemConstantTerm("sk"), applyTF(sub(FocusProjection.INSTANCE, 0), not(SimplifiedSelectTermFeature.create(heapLDT))), - longConst(-5600))); + 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(-5500))); + 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", @@ -324,7 +338,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(HIDE_AUXILIARY_EQ), ifZero(isTermAPulledOutHeap(), ifZero(isSkolemConstantUsedElsewhereInSequent(), longConst(-5400), longConst(HIDE_DEFERRAL_COST)), @@ -332,7 +346,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(HIDE_AUXILIARY_EQ_CONST))); } private void setupUserTaclets(RuleSetDispatchFeature d) { @@ -340,9 +355,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, USER_TACLET_LOW_PRIORITY); } else if (StrategyProperties.USER_TACLETS_HIGH.equals(userTacletsProbs)) { - bindRuleSet(d, "userTaclets" + i, -50); + bindRuleSet(d, "userTaclets" + i, USER_TACLET_HIGH_PRIORITY); } else { bindRuleSet(d, "userTaclets" + i, inftyConst()); } @@ -466,7 +481,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(DEPENDENCY_CONTRACT), inftyConst())); } else { depSpecF = ConditionalFeature.createConditional(depFilter, inftyConst()); } 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; } 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..953080d5f42 --- /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 = 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..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 @@ -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; @@ -29,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. @@ -70,7 +73,7 @@ private RuleSetDispatchFeature setupCostComputationF() { private void setUpStringNormalisation(RuleSetDispatchFeature d) { // translates an integer into its string representation - bindRuleSet(d, "integerToString", -10000); + 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 @@ -84,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(-100))); + ifZero(isBelow(keepChar), inftyConst(), longConst(CHAR_TO_INT_LITERAL))); // establish normalform @@ -95,25 +98,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(BELOW_MODALITY)); bindRuleSet(d, "defOpsSeqEquality", add(NonDuplicateAppModPositionFeature.INSTANCE, ifZero(add(applyTF("left", seqLiteral), applyTF("right", seqLiteral)), - longConst(1000), inftyConst()), + CostBand.DEFER.at(500), inftyConst()), belowModOpPenality)); bindRuleSet(d, "defOpsConcat", add(NonDuplicateAppModPositionFeature.INSTANCE, ifZero( or(applyTF("leftStr", not(seqLiteral)), applyTF("rightStr", not(seqLiteral))), - longConst(1000) + 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", CostBand.NORMALIZE.cost()); final TermFeature charOrIntLiteral = or(tf.charLiteral, tf.literal, or(add(OperatorClassTF.create(ParametricFunctionInstance.class), // XXX: @@ -122,17 +126,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(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))), CostBand.DEFER.cost(), + inftyConst()), belowModOpPenality)); bindRuleSet(d, "stringsReduceSubstring", - add(NonDuplicateAppModPositionFeature.INSTANCE, longConst(100))); + add(NonDuplicateAppModPositionFeature.INSTANCE, CostBand.DEFER.at(-400))); - bindRuleSet(d, "defOpsStartsEndsWith", longConst(250)); + bindRuleSet(d, "defOpsStartsEndsWith", CostBand.DEFER.at(-250)); bindRuleSet(d, "stringsConcatNotBothLiterals", ifZero(MatchedAssumesFeature.INSTANCE, ifZero( @@ -140,19 +146,21 @@ private void setUpStringNormalisation(RuleSetDispatchFeature d) { applyTF(instOf("rightStr"), seqLiteral)), inftyConst()), inftyConst())); - bindRuleSet(d, "stringsReduceConcat", longConst(100)); + bindRuleSet(d, "stringsReduceConcat", CostBand.DEFER.at(-400)); bindRuleSet(d, "stringsReduceOrMoveOutsideConcat", - ifZero(NonDuplicateAppModPositionFeature.INSTANCE, longConst(800), inftyConst())); + ifZero(NonDuplicateAppModPositionFeature.INSTANCE, CostBand.DEFER.at(300), + inftyConst())); bindRuleSet(d, "stringsMoveReplaceInside", - ifZero(NonDuplicateAppModPositionFeature.INSTANCE, longConst(400), inftyConst())); + ifZero(NonDuplicateAppModPositionFeature.INSTANCE, CostBand.DEFER.at(-100), + inftyConst())); - bindRuleSet(d, "stringsExpandDefNormalOp", longConst(500)); + bindRuleSet(d, "stringsExpandDefNormalOp", CostBand.DEFER.cost()); bindRuleSet(d, "stringsContainsDefInline", SumFeature - .createSum(EqNonDuplicateAppFeature.INSTANCE, longConst(1000))); + .createSum(EqNonDuplicateAppFeature.INSTANCE, CostBand.DEFER.at(500))); } @Override 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..d7691d47825 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/SymExCost.java @@ -0,0 +1,104 @@ +/* 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() {} + + /** + * 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". + */ + 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_BELOW_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..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 @@ -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; @@ -31,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. @@ -91,7 +94,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(METHOD_CONTRACT_PREFERENCE)); case StrategyProperties.METHOD_EXPAND, StrategyProperties.METHOD_NONE -> methodSpecF = methodSpecFeature(inftyConst()); default -> { @@ -114,15 +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(Long.MIN_VALUE)); - loopBlockFeature = loopContractInternalFeature(longConst(Long.MIN_VALUE)); - loopBlockApplyHeadFeature = loopContractApplyHead(longConst(Long.MIN_VALUE)); + blockFeature = blockContractInternalFeature(longConst(BLOCK_CONTRACT)); + loopBlockFeature = + loopContractInternalFeature(longConst(BLOCK_CONTRACT)); + loopBlockApplyHeadFeature = + loopContractApplyHead(longConst(BLOCK_CONTRACT)); } else if (blockProperty.equals(StrategyProperties.BLOCK_CONTRACT_EXTERNAL)) { - blockFeature = blockContractExternalFeature(longConst(Long.MIN_VALUE)); + blockFeature = blockContractExternalFeature(longConst(BLOCK_CONTRACT)); loopBlockFeature = - SumFeature.createSum(loopContractExternalFeature(longConst(Long.MIN_VALUE)), - loopContractInternalFeature(longConst(42))); - loopBlockApplyHeadFeature = loopContractApplyHead(longConst(Long.MIN_VALUE)); + SumFeature.createSum( + loopContractExternalFeature(longConst(BLOCK_CONTRACT)), + loopContractInternalFeature( + longConst(LOOP_CONTRACT_INTERNAL_TIEBREAK))); + loopBlockApplyHeadFeature = + loopContractApplyHead(longConst(BLOCK_CONTRACT)); } else { blockFeature = blockContractInternalFeature(inftyConst()); loopBlockFeature = loopContractExternalFeature(inftyConst()); @@ -133,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(-4000)); + mergeRuleF = mergeRuleFeature(longConst(MERGE_RULE)); } else { mergeRuleF = mergeRuleFeature(inftyConst()); } @@ -151,26 +159,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(THROWING_PROGRAM_STEP), + ifZero(isBelow(add(ff.forF, not(ff.atom))), + longConst(PROGRAM_STEP_BELOW_QUANTIFIER), + longConst(PROGRAM_STEP)))); - bindRuleSet(d, "simplify_prog_subset", longConst(-4000)); + bindRuleSet(d, "simplify_prog_subset", CostBand.EXECUTE.cost()); - bindRuleSet(d, "simplify_expression", -100); + bindRuleSet(d, "simplify_expression", 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", PROGRAM_STEP); + bindRuleSet(d, "executeDoubleAssignment", PROGRAM_STEP); final Feature findDepthFeature = FindDepthFeature.getInstance(); bindRuleSet(d, "concrete_java", - add(longConst(-11000), + add(CostBand.REWRITE.cost(), ScaleFeature.createScaled(findDepthFeature, 10.0))); // taclets for special invariant handling - bindRuleSet(d, "loopInvariant", -20000); + bindRuleSet(d, "loopInvariant", longConst(LOOP_INVARIANT)); boolean useLoopExpand = strategyProperties.getProperty(StrategyProperties.LOOP_OPTIONS_KEY) .equals(StrategyProperties.LOOP_EXPAND); @@ -183,7 +193,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(LOOP_SCOPE_EXPAND) : inftyConst()); final String methProp = @@ -196,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(2000)); + bindRuleSet(d, "method_expand", longConst(METHOD_EXPAND_REPRESSED)); case StrategyProperties.METHOD_EXPAND -> - bindRuleSet(d, "method_expand", longConst(100)); + bindRuleSet(d, "method_expand", longConst(METHOD_EXPAND)); case StrategyProperties.METHOD_NONE -> bindRuleSet(d, "method_expand", inftyConst()); default -> throw new RuntimeException("Unexpected strategy property " + methProp); } @@ -227,12 +238,13 @@ private RuleSetDispatchFeature setupCostComputationF() { mState); } }); - case StrategyProperties.MPS_SKIP -> bindRuleSet(d, "merge_point", longConst(-5000)); + case StrategyProperties.MPS_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(-10000)); + bindRuleSet(d, "modal_tautology", longConst(MODAL_TAUTOLOGY)); if (programsToRight) { bindRuleSet(d, "boxDiamondConv", @@ -240,7 +252,7 @@ private RuleSetDispatchFeature setupCostComputationF() { new FindPrefixRestrictionFeature( FindPrefixRestrictionFeature.PositionModifier.ALLOW_UPDATE_AS_PARENT, FindPrefixRestrictionFeature.PrefixChecker.ANTEC_POLARITY), - longConst(-1000))); + longConst(BOX_DIAMOND_CONV))); } else { bindRuleSet(d, "boxDiamondConv", inftyConst()); } @@ -251,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(50))); + applyTF(superFor, not(ff.program))), longConst(SPLIT_IF))); return d; } 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..63bc0686467 --- /dev/null +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/CostBand.java @@ -0,0 +1,100 @@ +/* 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; + +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. + * + *

+ * 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'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. + *

+ * + *

+ * 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. + *

+ */ +public enum CostBand { + /** + * 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; + private final Feature costFeature; + + CostBand(long base) { + this.base = base; + this.costFeature = ConstFeature.createConst(NumberRuleAppCost.create(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, as a constant strategy + * {@link Feature}. Use only for fine ordering within the band; larger, cross-theory steps + * deserve their own band. + */ + public Feature at(long delta) { + return ConstFeature.createConst(NumberRuleAppCost.create(base + delta)); + } + + /** The band's raw cost value. */ + public long value() { + return base; + } +}