From e35ce0bb0a8f2dd270633ee74a22a8cf7eab7335 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 7 Jul 2026 06:36:20 +0200 Subject: [PATCH] Enable bounded cross-multiplication of inequations in DefOps Created with AI tooling support --- .../uka/ilkd/key/settings/ViewSettings.java | 4 +- .../ilkd/key/strategy/IntegerStrategy.java | 89 +++++++++++++++++-- .../key/strategy/IntegerStrategyFactory.java | 5 +- .../ModularJavaDLStrategyFactory.java | 5 +- .../integer/integerSimplificationRules.key | 12 +-- .../DefOpsCrossMultiplicationTest.java | 68 ++++++++++++++ .../de/uka/ilkd/key/nparser/taclets.old.txt | 8 +- .../uka/ilkd/key/strategy/crossMultDefOps.key | 12 +++ 8 files changed, 182 insertions(+), 21 deletions(-) create mode 100644 key.core/src/test/java/de/uka/ilkd/key/strategy/DefOpsCrossMultiplicationTest.java create mode 100644 key.core/src/test/resources/de/uka/ilkd/key/strategy/crossMultDefOps.key diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java index 1d72f2a17c8..ec9f9128d88 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java @@ -35,8 +35,8 @@ public class ViewSettings extends AbstractPropertiesSettings { private static final String CLUTTER_RULESETS_DEFAULT = "notHumanReadable,obsolete," + "pullOutQuantifierAll,inEqSimp_commute,inEqSimp_expand,pullOutQuantifierEx," - + "inEqSimp_nonLin_divide,inEqSimp_special_nonLin,inEqSimp_nonLin,polySimp_normalise," - + "polySimp_directEquations"; + + "inEqSimp_nonLin_divide,inEqSimp_special_nonLin,inEqSimp_nonLin,inEqSimp_nonLin_multiply," + + "polySimp_normalise,polySimp_directEquations"; /** * default max number of displayed tooltip lines is 40 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 85da5d6c654..60ac803b4f0 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 @@ -106,6 +106,17 @@ private RuleSetDispatchFeature setupInstantiationF() { setupInstantiationWithoutRetry(d); setupInEqSimpInstantiation(d); + // The multiply_2_inEq* taclets used to receive their instantiation cost from the + // inEqSimp_nonLin rule set (bound in setupArithPrimaryCategories above). Now that + // they only carry inEqSimp_nonLin_multiply, bind that rule set here explicitly. + // Both Model Search and DefOps must complete cross-multiplication candidates (the + // \assumes clause is matched during instantiation), so both get the finite stock + // cost; Basic keeps them uninstantiated at infinity. Model Search stays + // byte-identical because this reproduces the value inEqSimp_nonLin gave it. + bindRuleSet(d, "inEqSimp_nonLin_multiply", + arithNonLinInferences() || arithDefOps() ? longConst(IN_EQ_SIMP_NON_LIN_COST) + : inftyConst()); + disableInstantiate(); return d; } @@ -114,8 +125,17 @@ private RuleSetDispatchFeature setupApprovalDispatcher() { final RuleSetDispatchFeature d = new RuleSetDispatchFeature(); final IntegerLDT numbers = getServices().getTypeConverter().getIntegerLDT(); - if (arithNonLinInferences()) { - setupMultiplyInequations(d, inftyConst()); + if (arithNonLinInferences() || arithDefOps()) { + // The InEquationMultFeature bounding enforced here is what prevents + // cross-multiplication from running in circles: only products that are + // bounded by the left side of an inequation already present in the + // sequent are approved, so the derivable monomials are capped. In + // DefOps mode the check is stricter (exact match only) to avoid the + // saturation blow-up acceptable for Model Search. + // baseCost is zero on the approval dispatcher: approval only distinguishes + // finite (approved) from infinite (rejected), so the base cost is irrelevant + // here and left out to keep the approval decision identical to stock. + setupMultiplyInequations(d, longConst(0), inftyConst(), !arithNonLinInferences()); } // these taclets are not supposed to be applied with metavariable // instantiations @@ -256,6 +276,11 @@ private void setupArithPrimaryCategories(RuleSetDispatchFeature d) { } else { bindRuleSet(d, "inEqSimp_nonLin", inftyConst()); } + // Cross-multiplication of inequations is now driven exclusively through the + // inEqSimp_nonLin_multiply rule set (the multiply_2_inEq* taclets no longer + // carry inEqSimp_nonLin). This keeps inEqSimp_nonLin at its stock cost so that + // splitEquationSucc and DefOps proofs that never cross-multiply stay on their + // stock search path. See setupInEqSimp for the per-mode binding. // polynomial division, simplification of fractions and mods bindRuleSet(d, "polyDivision", POLY_DIVISION_COST); @@ -574,11 +599,39 @@ private void setupInEqSimp(RuleSetDispatchFeature d, IntegerLDT numbers) { // category "handling of non-linear inequations" if (arithNonLinInferences()) { - setupMultiplyInequations(d, longConst(100)); + setupMultiplyInequations(d, longConst(IN_EQ_SIMP_NON_LIN_COST), longConst(100), false); bindRuleSet(d, "inEqSimp_split_eq", add(TopLevelFindFeature.SUCC, longConst(-100))); bindRuleSet(d, "inEqSimp_signCases", not(isInstantiated("signCasesLeft"))); + } else if (arithDefOps()) { + // DefOps also cross-multiplies inequations, but - unlike Model Search - does + // no equation splitting, case distinctions or cuts, and only multiplies when + // the product exactly matches the left side of an inequation already in the + // sequent (onlyExactlyBounded, enforced at approval). This terminates: the + // monomial ordering is degree-graded, so products (which equal an existing + // left side) and all monomials of the resulting right side stay within the + // degree of the existing left sides - a finite monomial universe. DefOps + // proofs without integer inequations enqueue no multiply candidates and keep + // their stock search path. + // + // Note: inEqSimp_split_eq and inEqSimp_signCases are deliberately NOT bound + // here. Since the multiply_2_inEq* taclets no longer carry inEqSimp_nonLin, + // that rule set keeps its stock (infinite) DefOps cost, which already switches + // splitEquationSucc off exactly as in stock DefOps. + // + // notAllowed is finite (not infinity): an app whose \assumes is not yet matched + // takes this branch, and needs a finite cost to survive long enough for the + // assumes-completion machinery to match it and re-evaluate as exactly bounded. + // Non-exactly-bounded apps are ultimately rejected by the approval dispatcher. + // The value matches the Model Search convention above; raising it does not + // measurably reduce the (inherent) reordering of arithmetic proofs. + setupMultiplyInequations(d, longConst(IN_EQ_SIMP_NON_LIN_COST), longConst(100), true); + } else { + // Basic arithmetic: cross-multiplication is off. inEqSimp_nonLin used to be + // the off-switch via the (now removed) tag on the multiply taclets, so the + // multiply rule set must be pinned to infinity explicitly. + bindRuleSet(d, "inEqSimp_nonLin_multiply", inftyConst()); } // category "normalisation of formulas" @@ -662,7 +715,31 @@ public void setContent(Term term, MutableState mState) {} } - private void setupMultiplyInequations(RuleSetDispatchFeature d, Feature notAllowedF) { + /** + * Sets up the cost/approval features for the cross-multiplication of inequations + * (rule set inEqSimp_nonLin_multiply). + * + *

+ * The multiply_2_inEq* taclets used to carry the inEqSimp_nonLin rule set in addition to + * inEqSimp_nonLin_multiply, which contributed the base cost {@link #IN_EQ_SIMP_NON_LIN_COST} + * and, in DefOps mode, the infinite off-switch. They no longer do; the base cost is therefore + * passed in explicitly via {@code baseCost} so that inEqSimp_nonLin can keep its stock cost + * and DefOps proofs that never cross-multiply stay on their stock path. + *

+ * + * @param d the dispatcher to bind the features to + * @param baseCost cost added unconditionally (previously supplied by the inEqSimp_nonLin + * rule set); zero for the approval dispatcher, {@link #IN_EQ_SIMP_NON_LIN_COST} for + * the cost dispatcher + * @param notAllowedF the costs in case the multiplication is not allowed + * @param onlyExactlyBounded if true, only products that exactly match the left side of + * an inequation already present in the sequent are allowed (used in DefOps mode: + * multiplication strictly directed at existing goal monomials); if false, products + * that are merely subsumed by an existing left side are admitted as well (Model + * Search: more speculative saturation) + */ + private void setupMultiplyInequations(RuleSetDispatchFeature d, Feature baseCost, + Feature notAllowedF, boolean onlyExactlyBounded) { final TermBuffer intRel = new TermBuffer(); /* @@ -691,6 +768,7 @@ private void setupMultiplyInequations(RuleSetDispatchFeature d, Feature notAllow // perfect, because it is not possible to distinguish between the // re-cost-computation delay and the normal costs for a rule application bindRuleSet(d, "inEqSimp_nonLin_multiply", add( + baseCost, applyTF("multLeft", tf.nonNegMonomial), applyTF("multRight", tf.polynomial), ifZero(MatchedAssumesFeature.INSTANCE, @@ -707,7 +785,8 @@ private void setupMultiplyInequations(RuleSetDispatchFeature d, Feature notAllow not(TermSmallerThanFeature.create(FocusProjection.create(0), AssumptionProjection.create(0))), ifZero(exactlyBounded, longConst(0), - ifZero(totallyBounded, longConst(100), notAllowedF)) + onlyExactlyBounded ? notAllowedF + : ifZero(totallyBounded, longConst(100), notAllowedF)) /* * ifZero ( partiallyBounded, longConst ( 400 ), notAllowedF ) ) ), */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategyFactory.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategyFactory.java index 3f85df875ae..74b76686dac 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategyFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategyFactory.java @@ -24,7 +24,10 @@ public class IntegerStrategyFactory implements StrategyFactory {
  • /, %, jdiv, jmod, ...
    • \
  • int_RANGE, short_MIN, ...
    • \
  • inInt, inByte, ...
    • \ -
  • addJint, mulJshort, ...
    • """; +
  • addJint, mulJshort, ...
    • \ + In addition, inequations are multiplied with each other
    \ + where the product is bounded by an existing inequation
    \ + (restricted such that termination is guaranteed)."""; public static final String TOOL_TIP_ARITHMETIC_MODEL_SEARCH = """ \ Support for non-linear inequations and model search.
    In addition, this performs:\ diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/ModularJavaDLStrategyFactory.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/ModularJavaDLStrategyFactory.java index a356f1b00e2..a570a021a21 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/ModularJavaDLStrategyFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/ModularJavaDLStrategyFactory.java @@ -49,7 +49,10 @@ public class ModularJavaDLStrategyFactory implements StrategyFactory { + "
  • /, %, jdiv, jmod, ...
    • " + "
  • int_RANGE, short_MIN, ...
    • " + "
  • inInt, inByte, ...
    • " - + "
  • addJint, mulJshort, ...
    • " + "" + ""; + + "
  • addJint, mulJshort, ...
    • " + "" + + "In addition, inequations are multiplied with each other
    " + + "where the product is bounded by an existing inequation
    " + + "(restricted such that termination is guaranteed)." + ""; public static final String TOOL_TIP_ARITHMETIC_MODEL_SEARCH = "" + "Support for non-linear inequations and model search.
    " + "In addition, this performs:" + "