Make the strategy cost structure explicit#3904
Open
unp1 wants to merge 8 commits into
Open
Conversation
Introduce CostBand (ncore, the shared cross-theory cost-band vocabulary) and FOLCost (FOL-theory-internal ordering constants), and convert FOLStrategy's cost literals to them - byte-identical by construction. Deferred: RAP + Model-Search node-for-node verification (holding proof runs for a benchmark). Checkpoint before the Integer conversion so the two theory changes stay separable for bisection if verification later flags a mismatch. Created with AI tooling support
…hmeticCosts Convert IntegerStrategy's ~50 cost literals to the shared CostBand ladder (anchors) and to per-sub-theory holders in IntegerArithmeticCosts (PolynomialCost / LinearEquationCost / LinearInequationCost / NonlinearArithmeticCost / DivModCost), grouped to anticipate a future split of the strategy. Byte-identical by construction; the old IN_EQ_SIMP_NON_LIN_COST / POLY_DIVISION_COST fields move into the holders. Deferred: RAP + Model-Search node-for-node verification (holding proof runs for a benchmark). Checkpoint after FOL (21a475ebb9) so the two theory conversions stay bisectable. Created with AI tooling support
Byte-identical. Shared-ladder anchors -> CostBand (block/loop contracts BLOCK_CONTRACT, loopInvariant LOOP_INVARIANT, concrete_java REWRITE, simplify_java SIMPLIFY, simplify_prog_subset EXECUTE). SE-internal nudges -> SymExCost (PROGRAM_STEP and its throwing/under-quantifier variants, method expand pair, LOOP_SCOPE_EXPAND, MERGE_RULE + MERGE_POINT_SKIP delta, MODAL_TAUTOLOGY, BOX_DIAMOND_CONV, SPLIT_IF, the 42 loop-contract tie-break). EXECUTE reserved for genuine program-execution rules (merge is not one); modal_tautology named separately from SUBST. Enabled-gates (longConst(0)) and the findDepth scale left raw. Created with AI tooling support
Byte-identical. String theory splits into an eager side (negatives, named in StringCost: INTEGER_TO_STRING, REPLACE_INLINE, CHAR_TO_INT_LITERAL, BELOW_MODALITY_PENALTY; plus stringsSimplify -> CostBand.NORMALIZE) and a lazy unfold ladder (positives) anchored to CostBand.DEFER.at(delta), so each defOps*/ strings* rule reads as "defer, by this much". instantiate default longConst(0) left raw; stringsConcatNotBothLiterals stays inftyConst. Created with AI tooling support
Byte-identical; RAP verification pending (deferred to resume). Band uses verified against the band docs: simplify_literals -> ELIMINATE, query_axiom -> SOLVE, partialInvAxiom -> DEFER_STRONG, information_flow_contract_appl (1000000 sentinel) -> LAST_RESORT. The pull-out-select ladder -> HeapSelectCost (its own holder, pre-staging a future heap/select module; carries a comment on the apply_equations ~-5700 cross-theory coupling). Remaining axiom/observer/ comprehension/induction nudges -> JavaCardDLCost, named by meaning not by value coincidence (JAVA_INTEGER_SEMANTICS/COMPREHENSION_SIMPLIFY != NORMALIZE, AUTO_INDUCTION != TYPE). QueryExpandCost tuples, branch count, and enabled-gates left raw. Created with AI tooling support
Byte-identical consolidation after the five theory conversions: - New CombinationCost holder for costs whose meaning spans strategies, with two documented admission mechanisms: (1) conflict-dispatched rule sets (ORDERED_REWRITING for apply_equations - the demodulation cost, guarded by term/monomial-ordering decrease at all four call sites; CNF_CONVERSION for apply_equations_andOr, shared deliberately by FOL's conjNormalForm), and (2) cost-sum couplings (APPLY_SELECT_EQ_EFFECTIVE = tuned sum of the dual- tagged applyEq taclet; HeapSelectCost.APPLY_SELECT_EQ is now derived from it, turning the old "about -5700" comment into checked arithmetic). FOLCost.APPLY_EQUATIONS/CNF_ORDERING and LinearEquationCost.APPLY_EQUATIONS/ APPLY_EQ_AND_OR are removed in favour of the shared constants. - JavaCardDL holders grouped per theory into JavaCardDLCosts.java (JavaCardDLCost + HeapSelectCost, Integer-style one file per theory). - Below-scope penalty names aligned: StringCost.BELOW_MODALITY (matching DivModCost.BELOW_MODALITY), SymExCost.PROGRAM_STEP_BELOW_QUANTIFIER. A sweep over all taclets and rule-set bindings verified completeness: exactly the three conflict-dispatched rule sets exist (order_terms, apply_equations, apply_equations_andOr, all FOL/Integer), and the only tuned cost-sum coupling is the applyEq taclet covered above. Created with AI tooling support
Pure cosmetic (byte-identical, no cost value changes): - Rename LinearEquationCost.APPLY_EQ -> APPLY_EQ_MONOMIAL_TIEBREAK (it is a small rider delta on CombinationCost.ORDERED_REWRITING via the dual-tagged apply_eq_monomials taclet, not a standalone "cost 1"); javadoc clarified. - Static-wildcard-import the theory-local cost holders in the single-holder strategies (FOLCost, SymExCost, StringCost, JavaCardDLCost+HeapSelectCost) so call sites read as bare names; the qualifier was pure redundancy there and forced spotless line wraps. CostBand and CombinationCost stay qualified (the prefix signals the shared ladder / a cross-theory cost). IntegerStrategy stays fully qualified: its 5 sub-holders' prefixes say which arithmetic layer. Created with AI tooling support
unp1
changed the title
unp1
added
Strategy
🛠 Maintenance
unp1
force-pushed
the
bubel/strategy-cost-cleanup
branch
from
8489846 to
2839edc
Compare
- cost() and at(delta) return the cost as a constant strategy Feature (ConstFeature over NumberRuleAppCost - exactly what longConst produced), so call sites lose the redundant wrapper: longConst(CostBand.DEFER.at(500)) becomes CostBand.DEFER.at(500), and bindRuleSet sites switch transparently to the Feature overload. The raw number stays available via value(); no code needed it. Behaviour unchanged (runAllProofs 674/674). - Document the deliberate relation between the layers: theory-local constants are absolute values on the same cost line, not anchored to a band, so retuning a tier moves exactly the rules placed on it. Point CostBand's javadoc at a real theory holder (was a stale IntegerCost reference), and note in IntegerArithmeticCosts why the file is not named "IntegerCosts" (would read as an integer-valued RuleAppCost type).
unp1
force-pushed
the
bubel/strategy-cost-cleanup
branch
from
2839edc to
04dc4d1
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Intended Change
This PR is a precursor to a careful refactoring of cost values assigned to rules.
It does not change any computed costs and is identical to current main. Its goal is too make
the current cost structure visible and to allow follow up PRs to consolidate them systematically.
The PR makes the cost structure explicit by naming the costs and organizing them in
three layers (for a detailed explanation see https://keyproject.github.io/key-docs/devel/StrategyCosts/) :
CostBand: cost bands express cost tiers for categories that are cross theorylike (
CLOSE,REWRITE,SUBST, …,DEFER,LAST_RESORT) withcost()andat(delta)for fine ordering within a tier. Each tier documents its meaning and, where present, hard ordering constraints (e.g.BLOCK_CONTRACTmust stay cheaper thanREWRITEand allsymbolic-execution rules).
CombinationCost(new,key.core): costs whose meaning spans theories,with the two admission mechanisms documented — (1) rule sets that more than
one strategy assigns a cost to (conflict-dispatched by
ModularJavaDLStrategy;ORDERED_REWRITINGforapply_equations,CNF_CONVERSIONforapply_equations_andOr), and (2) taclets whose rulesets belong to different strategies, so the tuned quantity is the sum
(
APPLY_SELECT_EQ_EFFECTIVEfor theapplyEqtaclet; the heap-side constantis derived from it, turning a previously comment-only "≈ −5700" coupling into
checked arithmetic). A taclet/rule-set sweep verified these are the only such
cases.
key.core):FOLCost, the integer-arithmeticholders (
PolynomialCost,LinearEquationCost,LinearInequationCost,NonlinearArithmeticCost,DivModCost— grouped anticipating a future splitof the integer strategy),
SymExCost,StringCost,JavaCardDLCostandHeapSelectCost(the pull-out-select pipeline, kept separate to pre-stage afuture heap/select module). Constants are named for what they achieve;
related values are expressed as arithmetic on their sibling
(
MERGE_POINT_SKIP = MERGE_RULE - 1000). Theory-local constants aredeliberately absolute (not anchored to a band): retuning a band moves exactly
the rules placed on it.
The five strategies (
FOLStrategy,IntegerStrategy,SymExStrategy,StringStrategy,JavaCardDLStrategy) are converted to this vocabulary;theory-local constants are imported statically so call sites read as bare
names, while
CostBand/CombinationCoststay qualified as a signal that ashared level is involved.
The commits are per-theory checkpoints (FOL, Integer, SymEx, String,
JavaCardDL, then consolidation and readability) and each compiles and passes
runAllProofs (to check that all proofs stay identical to current main) on its own.
Type of pull request
Ensuring quality
equals the literal it replaces, verified per theory.
runAllProofsafter each theory checkpoint and after the consolidationand readability steps: 674/674 proofs, 0 failures.
the unmodified strategies: identical proofs (same node counts on all
compared proofs).
band, holder and constant; cross-references between the layers).
developer-guide page "Strategy Costs and the Cost-Band Ladder"
(https://keyproject.github.io/key-docs/devel/StrategyCosts/) is pushed to
key-docs together with this PR; the page carries an open-PR notice
referencing this pull request, and this PR and the page reference each other.
Additional information and contact(s)
This PR is deliberately value-preserving. Follow-up PRs (independent of each
other, based on this one) will normalize individual values where the assessment
found them accidental — e.g. the relative order of goal closure and
loop-invariant application, the
Long.MIN_VALUE/-20000sentinel extremes,and near-duplicate levels — each gated by its own runAllProofs and
node-for-node comparison.
PR created with AI tooling support
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.