Quantifier and Heap Reasoning Improvements - #3961
Open
unp1 wants to merge 14 commits into
Open
Conversation
unp1
force-pushed
the
bubel/quantifier-shape-fallback
branch
from
August 12, 2026 10:34
63f3f22 to
ad12fe2
Compare
unp1
force-pushed
the
bubel/quantifier-shape-fallback
branch
5 times, most recently
from
August 20, 2026 20:35
ca5429c to
dc363c4
Compare
unp1
force-pushed
the
bubel/quantifier-shape-fallback
branch
from
August 21, 2026 11:12
dc363c4 to
cc9beac
Compare
Improves treatment of quantified formulas involving arrays with affine integer indexes. Trigger matching compares the structure of two terms, so a fact about b[srcStart + t] cannot be used on a term about a[x]: the witness x - srcStart occurs nowhere in the proof. Re-indexing therefore had to be written as a lemma and discharged by SMT. A theory can now solve a trigger subterm against the term it should match, through a new method on QuantifierTheorySupport. Integer arithmetic solves k*t + rest = s for t by exact division, for a pattern affine in one unbound variable. A wrong solution costs one instantiation, since instantiating a universal with any term is sound. (created with AI tooling support)
Applying a method contract anonymises the heap. A quantified formula from before the call has its triggers over the old heap, so trigger matching finds no instance and the property cannot be used afterwards. For an array read select(h,a,arr(i)) the heap theory now adds the trigger select(H,a,arr(i)) with a metavariable H for the heap, which matches the read over any heap. Such a trigger is matched by unification and by basic matching. An instantiation that basic matching gets by solving a subterm costs 10000 more, so it is tried after the ones from ordinary matches. The heap theory also supplies the array indices the formula writes as instance candidates, through a new method on QuantifierTheorySupport. Such an index is ground, so no trigger contains it, although instantiating with it collapses the read it is written to. AdjacencyStore.storeValidList, added here, needs this across its call to storeList. runAllProofs: 101 of 672 proofs change, 793103 against 803745 nodes. (created with AI tooling supported)
…alues then o != u Some heap simplification rules rely in their assumes on the fact that two objects are different, i.e., \assumes (==> o = u). this change makes it more likely for that formula to be actually present
Approval should only be called on taclets whose assumes clause has been matched.
…antiation QuantifierTheorySupport bundled two unrelated concerns: which subterms of a theory make a trigger, and what the theory answers about terms and literals. Trigger selection depends on the terms a profile builds, the answers about terms do not. TriggerSupport and TheoryReasoning now hold the two halves, and each caller takes the one it uses: TriggersSet and Instantiation the first, BasicMatching, Congruence and PredictCostProver the second. The list of theories moves from TriggersSet to Profile.getTheorySupports, so a profile over other terms registers its own. Instantiation reads its instance candidates from that list too, which retires the check for the classic treatment it did before: the classic list holds no heap support, so it yields no candidates. runAllProofs is node-identical, 675 proofs. (created with AI tooling support)
The theory modules move to theory, the metavariable and unification machinery to constraint, and the tie-break strategies to tiebreak. Pure moves and visibility adjustments; tests of moved package-private classes move along.
A theory answered two questions about a trigger candidate, rejectsAsTrigger and prefersEnclosingTrigger, and the selection consulted them at different points of its descent. The heap theory needed both to express one rule: the trigger for an array access is the read. Both hooks become one verdict, ACCEPTABLE, FORBIDDEN or PREFER_ENCLOSING, so a theory selects its triggers in one method and the descent interprets the verdict in one place. The created field is recognised by its function symbol instead of a name suffix. A uni-trigger carried three booleans, onlyUnify, matchByUnification and isElementOfMultitrigger, and the matcher was chosen by a two-condition test over the first two. The first two become the kind of the trigger, PATTERN, GENERALIZED, NEEDS_UNIFY or GENERALIZED_UNIFY, fixed at registration; the matching switches on the kind. The element flag is a role, not a matching mode, and stays a flag. Each clause is read once into a ClauseAnalysis value, literals stripped of negations and if-then-else expanded, and the descent returns a Search value, SATISFIED or OPEN, instead of a boolean that meant three things. runAllProofs is node-identical, 674 proofs, 792744 nodes. (created with AI tooling support)
Why an instance costs what it costs was encoded in which loop of addInstances found it, with the surcharge constants at the call sites. Every instance now carries an Origin, OWN_PATTERN, SOLVED_POSITION, THEORY_UNIFIED, THEORY_MATCHED or THEORY_DIRECT, and one method states the surcharge per origin. A trigger treatment becomes the set of origins it admits, next to its choice of theory supports; the predicate for basic matching of theory triggers becomes the admission of THEORY_MATCHED, and a treatment that admits no direct theory instances does not pay for the matrix walk that would find none. The instances of a sequent live in an InstanceTable that keeps cost and origin per instance. The table normalizes a cast-wrapped query in one place, comparing against the cast symbol; the three copies of the cast test by name in the cost lookup, the generation rank and the polarity count are gone, and the tie-break scorers receive the normalized instance. runAllProofs is node-identical, 674 proofs. (created with AI tooling support)
unp1
force-pushed
the
bubel/quantifier-shape-fallback
branch
from
August 21, 2026 18:58
07e26a4 to
1ba8242
Compare
Some clauses yield no trigger at all: every literal holding the quantified variable is forbidden, and what remains covers no variable. After the covering multi-triggers of a clause are built, the selection now asks each theory for fallback triggers if the clause got no covering trigger. A fallback is registered as theory-provided, its instances carry the FALLBACK origin, and only the most informed treatment admits them. The treatment decides at the instance, not at registration: the trigger set is cached per formula and shared by the non-classic treatments, so a set built under one treatment must serve the other. No theory offers fallback triggers yet, so this changes no proof. runAllProofs is node-identical, 674 proofs. (created with AI tooling support)
Comments across the package let terms and rules speak: a read said which access is meant, a wrapper said everything through its argument, a term was never named by the formula. Each such phrase now states its relation: a read determines the accessed array, a wrapper adds no information to its argument, a term does not occur in the formula. Comment change only. (created with AI tooling support)
Whether a clause had a covering trigger was read off the growth of the shared trigger collection, and which literal contributed what was not recorded at all. That encoding missed a trigger an earlier clause had already registered for the same term, and it left a theory asked for fallback triggers without any view of the literals. Selection now produces a ClauseTriggers value: per literal the covering triggers and the elements it yielded, and whether a covering multi-trigger was built. A clause is covered if the value says so. The derived triggers of a subterm are registered once and counted for every later literal that holds the subterm, classified against that literal's clause. fallbackTriggers receives the value, so a theory sees which literals yielded nothing. No theory offers fallback triggers yet, so no proof changes. (created with AI tooling support)
The fallback triggers were asked for every clause without a covering trigger. The instantiation binds the first quantified variable, and every covering trigger binds it, so a formula is instantiated exactly if some of its clauses is covered. A clause without a covering trigger next to one that covers is no gap, and asking there only added triggers to a formula that was never incomplete. The selection now collects the result of every clause and asks the theories only if none is covered, still clause by clause, so a theory keeps the clause's variables and literals in view. After the fallbacks of a clause are registered the cover search runs once more for it: a fallback that binds only some of the clause's universal variables is an element and can now combine into a covering multi-trigger. No clause of the formula had a cover before, so the second search finds only covers that use a fallback, and registers no cover twice. No theory offers fallback triggers yet, so no proof changes. (created with AI tooling support)
…hich to derive triggers (addresses issue #3972)
unp1
force-pushed
the
bubel/quantifier-shape-fallback
branch
from
August 21, 2026 19:05
1ba8242 to
5bf097e
Compare
unp1
enabled auto-merge
August 21, 2026 19:36
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.
Second of three of the last AI supported work
The following problem
can now be proven automatically.
It also makes inequality of objects explicit in the sequents enabling more heap simplification rules to be applied automatically. The added taclet has been proven sound and the proof has been added.
This PR also addresses issue Incompleteness of quantifier treatment #3972 using the reworked infrastructure of this PR.
Type of pull request
Ensuring quality
Additional information and contact(s)
Created with AI tooling support
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.