Performance Series 2 (5/5): Faster quantifier-instantiation heuristic, plus code cleanup#3878
Open
unp1 wants to merge 7 commits into
Open
Performance Series 2 (5/5): Faster quantifier-instantiation heuristic, plus code cleanup#3878unp1 wants to merge 7 commits into
unp1 wants to merge 7 commits into
Conversation
unp1
changed the title
unp1
force-pushed
the
bubel/quantheur-cleanup
branch
from
e7b6156 to
67f45dc
Compare
Pin the current TriggersSet output for representative quantifier shapes (uni/multi/powerset, equality exclusion, negated implication guards, existential variables, conjunction clauses, and the no-outer-variable case) ahead of a rename/cleanup pass. A behavior-preservation net, not a claim the current output is ideal. Created with AI tooling support
The three-argument intersect computed all three sizes from set0, so the 'intersect the two smaller sets first' optimization never engaged. Use the respective set sizes. The three-way intersection is order-independent so the result is unchanged; the only caller (SplittableQuantifiedFormulaFeature) inspects just the result's emptiness/size. Created with AI tooling support
Rename for readability (triggers->elements, qvs->clauseVariables, setMultiSubstitution->combineElementSubstitutions, unifySubstitution->mergeIfCompatible, cryptic locals) and document the class. No behavior change. Created with AI tooling support
Rename uqvs->universalVariables and the matching helpers, and turn the cycle detection copied from EqualityConstraint into readable, documented containsCycle/reachesItself. No behavior change. Created with AI tooling support
Rename the trigger-discovery methods and locals (collectUniversalVariables, addMaximalUniTriggers, buildCoveringMultiTriggers, tryAddCoveringMultiTrigger, clauseVariables, ...), rename inner ClauseTrigger to ClauseTriggerFinder, document the multi-trigger powerset pruning, and fix smells (HashSet-declared LinkedHashSet, unused import, generic-array suppression). No behavior change. Created with AI tooling support
Substitution.applyWithoutCasts applied each variable in its own ClashFreeSubst pass -- one full traversal of the term per variable. As the substitution is ground, all variables can be replaced in a single shadow-aware traversal, keeping the per-variable path only as a fallback for the rare cast case. Behaviour-preserving; cuts substitution time roughly threefold on quantifier-heavy proofs. Created with AI tooling support
When estimating quantifier instantiation cost, PredictCostProver calls HandleArith.provedByArith for every literal/axiom pair. For a non-arithmetic literal it allocated a cache key, took the cache lock and ran formatArithTerm only to return the literal unproved -- and such literals dominate (~98% of calls even on arithmetic proofs). Both entry points now bail on a cheap arithmetic-shape check (>=, <=, plus = for the single-argument variant), exactly the condition under which the full prover would have returned the literal unchanged. Behaviour-preserving; cuts refinement time by roughly a third. Created with AI tooling support
unp1
force-pushed
the
bubel/quantheur-cleanup
branch
from
67f45dc to
9d2ba94
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
2 participants
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
Code-quality cleanup of the quantifier-instantiation heuristic plus two behaviour-preserving speed-ups: (1) trigger-set construction is clarified and now has characterization tests, and a dead set-size heuristic is fixed; (2) ground substitutions are applied in a single term traversal instead of one pass per variable (~3.6 -> 1); (3) the arithmetic prover is skipped for non-arithmetic literals, which dominate (~98% even on arithmetic proofs). Behaviour-preserving (identical proof node counts across runAllProofs).
Benchmark
Automode time, median of 3 runs, serial forks (
-PrapForks=1), isolateduser.homeper run; baseline = current main (8 representative proofs: 4 quantifier-heavy + 4 mixed). ArrayList.remove.1 is high-variance run-to-run — treat as noise. The gains concentrate on quantifier-heavy proofs (PUZ031p1, SYN550p1), as expected.Plan
Type of pull request
Ensuring quality
TestTriggersSetcharacterization tests).Additional information and contact(s)
Part of Performance Series 2 — see the overview (#3879) for the combined benchmark and series context.
Created with AI tooling support.
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.