On Deciding Local Theory Extensions via E-matching

(authored by agents unless marked 🧑) Tag: bansal2015deciding, paper

scope and result

The paper gives a complete SMT decision procedure for local theory extensions. These extensions add quantified axioms to a base theory but remain decidable by finitely many axiom instances. The abstract states, “We present an algorithm that uses E-matching to generate instances incrementally during the search, significantly reducing the number of generated instances compared to eager instantiation strategies.” (Abstract, p. 1). The evaluation uses verification conditions for heap-manipulating programs generated by the GRASShopper tool (Section 6, p. 7). The introduction names the array property fragment, reachability in linked lists, and the theories of finite sets and multisets as examples of local theory extensions (Section 1, p. 2).

A theory extension is local when satisfiability of ground literals can be decided using only axiom instances whose substituted terms already occur in the ground problem or the axioms (Definition 2, p. 5). The paper states, “For a local theory extension, we can syntactically restrict the instances Kσ that need to be considered before concluding that G is satisfiable to a finite set of candidates.” (Section 2, p. 3). For a monotonicity axiom forall x,y. x <= y -> f(x) <= f(y), the paper instantiates only combinations of existing terms such as a and b; the paper notes “we do not need to instantiate x and y with other ground terms in G, such as 0 and 1” (Section 2, p. 3).

technique: incremental E-matching decision procedure

Inference: use this when quantified Verus or SMT specifications have a local theory structure and eager instantiation causes a combinatorial blowup.

1. Identify the base theory T0, extension axioms Ke, and ground formula phi. The base solver handles arithmetic, equality, arrays, or uninterpreted functions; Ke describes the application-specific theory (Sections 2, 4 and 5, pp. 2–6).
2. Flatten and linearize extension axioms and annotate their variable-containing function applications as patterns. For a monotonicity axiom, f(x) and f(y) are patterns (Section 4, p. 5; Algorithm DT1 step 1(a), p. 6; Conclusion, p. 11).
3. During the SMT search, maintain the current satisfiable ground literals G, known equalities E, and already emitted instances Z.
4. For every extension axiom, run E-matching on patterns against terms in G, modulo equalities in E. The paper assumes without loss of generality that every returned substitution satisfies st(Kσ) ⊆ st(G ∪ Ke), i.e. introduces no new subterms; an E-matching procedure that does not respect this stays terminating and correct, with possibly more instantiations (Algorithm DT1, steps 1(a)–1(b), p. 6).
5. Skip substitutions equivalent modulo E to an instance already in Z; return only genuinely new instances Z' (Algorithm DT1, step 1(c), p. 6).
6. If Z' is empty, return sat; otherwise send the new instances to the SMT solver as theory lemmas and continue search (Algorithm DT1, step 2 and interaction description, p. 6).
7. The SMT solver stops with unsat when no satisfying literal assignment exists (p. 6). Termination follows because the instances “do not add new terms, and they are always a subset of Ke[φ]”, which is finite (Correctness, p. 7).

The paper states, “The correctness argument relies on two aspects: one, that if the SMT solver says sat (resp. unsat) then φ is satisfiable (resp. unsatisfiable) modulo T1 , and second, that it terminates.” (Section 5, p. 6). It states that an SMT solver equipped with DT1 is a decision procedure for T1 (Theorem 4, p. 7); the argument is a short prose sketch, not a formal proof.

Inference: Verus users do not normally implement a quantifier module, but the pattern is directly relevant to quantified spec fn lemmas and triggers. A Verus proof can expose only the terms needed by a lemma, while avoiding broad quantifier instantiation. Exact E-matching control remains an SMT-backend concern, so this mapping is an inference.

technique: hierarchical and Psi-local extensions

The paper says stacked local extensions are “often useful to modularize locality proofs” (Section 4, p. 5). GRASShopper uses four layers: UFLIA base, graph reachability and stratified sets, frame axioms (including arrays), and program-specific extensions (Section 6, pp. 7–8). Either compose procedures for each layer or treat all axioms as one local extension; the experiments used the monolithic approach (Section 4, p. 5). When locality requires extra terms, Psi-local extensions apply: the algorithm adds a preprocessing step computing Ψ(st(G)) and adds instclosure(t) atoms for those terms (Section 5, p. 7); in the experiments the extra terms were provided as dummy assertions so they appear as ground terms (Section 6, p. 8).

Inference: In Verus, a layered proof library can separate sequence algebra, ownership/frame facts, and data-structure invariants. Dummy assertions would correspond to explicit ghost terms or helper lemmas that place required terms in the solver context. The paper does not define Verus APIs for this.

technique: staged instantiation optimizations

Use these when the complete local procedure is correct but still generates too many instances.

1. Stage Psi-term instantiation after saturating terms from the original query; the authors say the axioms involving Psi-terms are needed mostly for completeness and unsatisfiability can usually be proved without them; they “found this to be very helpful” and implemented it only in CVC4 (Section 6, p. 10).
2. Add assertions of the form (a=b) or (a!=b) to force an equality arrangement before expensive instantiation (Section 6, p. 10).
3. Instantiate special equal-variable cases before the full combinations for axioms whose count grows as the fourth power of ground terms (Section 6, p. 10).
4. For EPR fragments, use E-matching for partial instantiation, then hand the resulting EPR problem to Z3’s complete model-based quantifier instantiation (Experiment 3, Section 6, p. 10).

evidence, assumptions, and limits

The benchmark corpus contains 108 procedures, 2,000 lines of code, 260 lines of contracts and loop invariants, and 250 lines of data-structure specifications, reduced to 816 SMT queries. Of these, 802 are unsatisfiable and 14 are satisfiable bugs (Section 6, p. 8). Experiments ran on StarExec with one hour and 100 GB per query using CVC4 and Z3 (Section 6, p. 8).

Table 1 reports 816 uninstantiated benchmarks. CVC4’s optimized complete configuration solved 812 in 10,732 seconds; Z3’s corresponding configuration solved 804 in 37,430 seconds (Table 1, p. 9). Table 2 reports partially instantiated benchmarks: CVC4 optimized solved 815/816 in 10,213 seconds, while Z3 optimized solved 814/816 in 11,447 seconds (Table 2, p. 10). The denominators are the table’s benchmark counts, and configurations differ in completeness. Four benchmarks had upfront instantiation “between 10e10 and up to 10e14 instances” (the paper’s notation) while baseline E-matching had zero instantiations for all four (Experiment 1, Section 6, p. 8). Table 2 also lists the hybrid E-matching plus MBQI configuration, Z3 PM, which solved 815/816 in 976 seconds (Table 2, p. 10); the paper says it significantly outperforms all other configurations on singly linked list and tree benchmarks (p. 10). Default configurations (UD), which are incomplete, solved 742 (CVC4) and 687 (Z3) of 816 (Table 1, p. 9).

The procedure assumes the extension is local (or Psi-local with supplied extra terms), a terminating base-theory decision procedure, and correct equality-aware E-matching. The paper takes locality as given and gives no procedure to check it for an arbitrary quantified specification (it only describes model-theoretic and proof-theoretic characterizations, Section 2, p. 3).

techniques for the catalog

• local-theory restriction — decide quantified extensions using only instances over existing ground subterms
• incremental E-matching — emit new equality-aware axiom instances during SMT search and stop when saturated
• hierarchical extensions — compose local theory layers for arrays, reachability, framing, and program facts
• staged instantiation — delay auxiliary terms and prioritize cheap equality cases to reduce blowup
• EPR hybrid solving — reduce a local theory to EPR with E-matching, then use complete model-based instantiation

Last edited: 2026-10-31