Add (speculate ...): test an instantiation hypothesis in one scope

[kiranandcode]

Implements the solver side of plans/speculative_probe.md: a caller tries one hypothesis about quantifier instantiation in the current user context, checks, and reads back what the hypothesis did. The push/pop around it is the fork; nothing of it survives the pop.

Commands

(speculate :instantiate <qid> ((<var> "<term>")+))        ; instantiate once at these terms
(speculate :trigger <qid> ((<var> <sort>)+) ("<term>"+))  ; one more trigger, matched every round
(speculate :block <qid> "<fingerprint>")                  ; refuse instances that fit a shape
(speculate :observe)                                      ; change nothing, watch for loops
; each takes [:loop-threshold <n>]
(get-info :speculation)

Terms are string literals, each parsed on its own (the import-instantiations lambdas became shared tryParseString/unquoteString helpers). A term naming an undeclared symbol fails the command with (error "speculate: cannot parse ...") and the session goes on; nothing is left active. The outer syntax is a command like any other: malformed, it is a parse error, as (assert) would be, so a driver must spell it exactly and pass only the terms through as strings.

The reply lists each hypothesis with a status (applied, rejected, mismatch, unusable, no-quantifier, pending: no round of the scope has reached e-matching yet), a reason, the instances it made (in original form), and for :trigger the formula with the pattern as its only one (:materialized). It also lists loops, see below. A hypothesis's counts and lists cover every check of its scope so far (:quantifiers counts distinct formulas); :rounds and :loops cover the last check.

Design, and where it departs from the plan

• New file theory/quantifiers/speculation.{h,cpp}, owned by Instantiate. Hypotheses, the per-formula "applied" set and the speculative triggers are all user-context-dependent (CDList, CDHashSet). The triggers are owned by that CDList, not a TriggerDatabase, so a pop frees them along with the formulas they hold. A ContextNotifyObj clears the qid and depth caches on pop. Keeping popped nodes alive shifts later node ids, and with them the search; that resource drift was seen in the nl-frontier work.
• New InferenceId::QUANTIFIERS_INST_LLM_DIRECTED. Directed instances and speculative-trigger matches carry it (Trigger::setInferenceId), so a leaked one is easy to find.
• The directed instance skips the SAT-context entailment filter, as replay does: it is offered once per user context, so skipping it after one branch would lose it. A speculative trigger's matches come back every round like any trigger's, so they are filtered and can be blocked like any trigger's; the funnel tells the two apart by Speculation::isDirecting, set only while the directed instance is added, not by the inference id.
• A directed term sees the top-level substitutions before it is rewritten, so a variable preprocessing eliminated ((= a b)), or a define-fun application, means what it did in the input. :instances shows the term after substitution.
• Where hypotheses are applied. QuantifiersEngine::applySpeculation runs at the start of QEFFORT_STANDARD, the effort e-matching runs at, ahead of that round's strategies. Its lemmas stay pending while the strategies run and are sent with theirs, so a speculative trigger is matched in the same round as the formulas' own triggers, as the :materialized formula's would be. The ordinary path counts the round, so --inst-max-rounds bounds a speculative trigger that feeds itself. Directed instances run once per formula; triggers match every round. Conflict-based instantiation still runs first, so a check it closes never applies the hypotheses (status pending). In replay-only mode no strategy runs, and the hypotheses apply before the replay-only return.
• Terms given through the API must be closed. speculateInstantiation rejects a term with free variables; speculateTrigger requires bound variables and a pattern whose free variables are among them. The SMT-LIB parser cannot produce either.
• Blocks sit at the top of the funnel. They are tested against the bindings and the instance of the trigger that matched, both in original form. A fingerprint is an s-expression whose holes _, _n and #n match any term (repeated names must match equal terms), written in the vocabulary of :matching-loops' :step; a leaf constant matches the text the printer gives it, (- 1) and (/ 1 2) included. The directed instance of an :instantiate hypothesis is never refused. A check in which a block refused an instance answers unknown, not sat (new IncompleteId::QUANTIFIERS_SPECULATIVE_BLOCK): its model may violate the formulas the block kept from being instantiated.
• The loop signal is not a re-entry count per fingerprint. For a general instantiation there is no fingerprint to count, and relying on the instantiation graph would need launch flags. While any hypothesis is active (:observe included), each check records, per quantified formula, the rounds in which its deepest instantiating term got deeper than in any earlier round. A formula with at least :loop-threshold such rises (default 5) is reported as a loop. Comparing an :observe check with a hypothesis check tells whether the hypothesis introduced one.
• d_recordedInst is not used. As Add (get-info :matching-loops): self-feeding quantifiers of the last check #3 and Record the instantiation graph: --inst-graph and (get-instantiation-graph) #4 found, it only holds CEGQI's recorded instances.
• Which instances closed the goal is not reported. That needs full proofs. The reply lists the instances the hypothesis made, and the Verus side establishes a close by checking with and without the hypothesis.

Testing

• Sixteen regressions, regress0/quantifiers/speculate-*.smt2. They cover scoping (the scope after a probe is unknown again and nothing is active), mismatches, unusable patterns, unknown qids, parse errors, a loop observed and then cut by a block, a block that stops a proof, a block refusing a speculative trigger's match, --inst-max-rounds stopping a self-feeding speculative trigger (speculate-rounds), a block under --finite-model-find answering unknown (speculate-block-model), directed terms through an eliminated variable and a define-fun (speculate-instantiate-subst), constant fingerprints (speculate-block-const), the report before any check and after a nested pop (speculate-report), a self-feeding speculative trigger that no longer keeps an ordinary trigger from closing the goal in the same round (speculate-trigger-round, --no-cbqi, next to the :materialized formula), and a check closed by conflict-based instantiation leaving the hypothesis pending (speculate-pending). From the fourth round: a formula found by its :qid after variable elimination (speculate-varelim), the rejected reasons (speculate-rejected), an indexed-operator fingerprint (speculate-block-indexed) and a logic without quantifiers (speculate-qf). From the fifth round: integer terms for real variables (speculate-instantiate-real). The dump tester runs on all sixteen.
• API unit test TestApiBlackSolver.speculate: the four Solver::speculate* functions, a directed instance closing a goal, the report before and after the pop, and the argument errors, including a directed term and a pattern with a free variable.
• With an assertions build (unrestricted --assertions), after the third review change and the merge of main (Add (get-info :branch-profile) for counterfactual twins #11, Clear pending quantifier lemmas when a check is interrupted #15): all regress0/regress1 quantifier and nl regressions plus pending_lemmas_after_interrupt, 718/718; api_solver_black 131/131; git clang-format clean.
• After the fourth round (da4b2b0073), same build type: all of regress0, 2730/2730, and the regress1 quantifier, nl and proof regressions, 363/363, every tester included; api_solver_black 131/131. Neutrality of the rewriter change, over the 710 regress0–regress2 quantifier and nl files against the build just before it: every verdict is identical; resource::resourceUnitsUsed differs on 5. Two vary from run to run on the new build (quant-wf-int-ind 877/878, ufdt-solve-model-built 1162/1163). Three move by a fixed amount over five runs, each with a :qid in its input (issue5373-2 1213 to 1216, issue6638-sygus-inst 2197 to 2206, cee-event-wrong-sat 11711 to 11729), consistent with a formula that keeps its name being a different node.
• Neutrality: rerun after the first review change over the 429 regress0/regress1 quantifier files against a local build of the same base (c893833): every verdict is identical; resource::resourceUnitsUsed is equal on 426 files. The 3 others (ho-seu-sygus-inst, ufdt-solve-model-built, infer-arith-trigger-eq) vary from run to run on the base build itself (e.g. 55815/61099, 1162/1163, 134702/134722/135177), and the branch build lands on the same values. The second review change touches only code that runs while a hypothesis is active (the round count sits in the speculation branch, hasBlocked is false without a block, the substitution applies to directed terms only). So does the third: applySpeculation is called only while a hypothesis is active, and the replay-only branch is unchanged without one.

Review changes

• instantiate.cpp, speculation.{h,cpp}: the entailment skip and the block exemption applied to every QUANTIFIERS_INST_LLM_DIRECTED instantiation, so a speculative trigger's matches were neither filtered as entailed nor refused by a block, unlike the real trigger the probe stands for. Both now key off Speculation::isDirecting(); isBlocked lost its InferenceId parameter.
• speculate-trigger.smt2: one more scope with a :trigger and a :block on the same formula; the match is refused each round it is offered.

Second round, from probing the branch:

• quantifiers_engine.cpp: the speculation branch returned before d_numInstRoundsLemma++ and notifyEndRound(), so --inst-max-rounds never counted its rounds and a self-feeding speculative trigger ran until a resource limit (seen: over 90 s with --inst-max-rounds=12). The round now counts.
• instantiate.cpp, incomplete_id.{h,cpp}: a block refuses as a duplicate would be refused and nothing marked the check incomplete, so --finite-model-find answered sat on an unsat query. checkComplete now reports QUANTIFIERS_SPECULATIVE_BLOCK.
• speculation.cpp: directed terms were only rewritten; an eliminated variable or a define-fun term gave an unrelated instance that still reported applied. They now go through the top-level substitutions.
• speculation.{h,cpp}, solver_engine.cpp: constant fingerprints match; :quantifiers, :bodies and :materialized no longer repeat after a nested pop; the report before any check shows the default threshold, not 0.
• Tests: five regressions and the API unit test above.

Third round:

• quantifiers_engine.{h,cpp}: a round whose lemmas came from a hypothesis returned before any strategy ran, so a speculative trigger that feeds itself kept every other formula from being instantiated. A query the :materialized formula proves unsat at once ran until killed (30 s), or answered unknown under --inst-max-rounds=20. Hypotheses now apply inside the strategy loop, see Design.
• speculation.{h,cpp}: no-quantifier was inferred from rounds > 0; a check can now end before a round reaches e-matching, so it needs the hypothesis to have been applied (d_considered), and is pending otherwise.
• cvc5.cpp: speculateInstantiation accepted a term with a free variable, which reached TheoryEngine::lemma (Check failure !expr::hasFreeVar); speculateTrigger now also checks its variables and pattern.
• speculation.cpp: dropped a local copy of quoteString (util/smt2_quote_string.h has it); the unit test uses TermManager::mkConst.

Fourth round:

• quantifiers_rewriter.cpp: when a rewrite changes a formula's variables (variable elimination, prenexing), the rewriter dropped the whole pattern list, and the :qid with it, so every hypothesis about such a formula reported no-quantifier. The patterns still go, since they may mention a variable that is gone, but a :qid attribute stays. No other attribute does: some (fun-def, sygus, the prenex id) mark the formula for a procedure whose shape the rewrite need not keep. A pattern list holding only a :qid is what (! body :qid q) already gives, so no rewrite or strategy meets a new shape; proof reconstruction of variable elimination already declines formulas with a pattern list. New regression speculate-varelim. Its two formulas have different bodies: an alpha-equivalent formula is registered once whatever its :qid (--quant-alpha-equiv), so the second one's :qid finds nothing. That is base behaviour, now documented on speculateInstantiation.
• solver_engine.cpp: speculate in a logic without quantifiers was a fatal error that ended the session; it is now recoverable, like a term that does not parse (speculate-qf).
• speculation.cpp: a variable named twice, in :instantiate or :trigger, is an error (the first term used to win silently); a directed instance that simplifies to true is rejected with that reason, not "a lemma already sent" (speculate-rejected, which also covers "made already"); a fingerprint application may be headed by an indexed operator such as (_ extract 3 0) (speculate-block-indexed).
• commands.{h,cpp}, smt2_cmd_parser.cpp: SpeculateCommand keeps each term as the input spelled it and prints that, so a command whose term failed to parse dumps as it was read. The dump tester now runs on every speculate-* regression.

Fifth round:

• speculation.cpp: an integer term for a real variable was a mismatch ("the term for y has sort Int, and y has sort Real"), so "5" could not stand for 5.0. It now means its real, as in an SMT-LIB term; a real term for an integer variable is still a mismatch (speculate-instantiate-real).

• cvc5.h, speculation.h: miniscoping still drops the :qid. A formula without a :pattern that it splits, such as (forall ((x Int) (y Int)) (or (P x) (R y))), gives no-quantifier; --miniscope-quant=off keeps it whole. This is documented, not changed. The proof rules rebuild a miniscoped formula's parts without attributes (QUANT_MINISCOPE_AND and the others), so parts that kept the name would no longer match their elaboration. The parts would also all carry one name, which the reports that key by :qid would merge. A formula with a :pattern is not split, and Verus gives every quantifier one.

• speculation.{h,cpp}: dropped d_envRef, which duplicated EnvObj::d_env.

• The fourth round's :qid change is visible in output, beyond the verdicts and resource units above. A formula the rewriter changed now keeps its name in every report that names formulas. Before, --dump-instantiations printed the rewritten formula, (get-info :inst-pressure) reported it as quant_0 :named false, and the instantiation graph as _. Now all three print the :qid. The same holds for the formula's num-instantiations, :matching-loops and :branch-profile rows. --check-proofs still passes on such a formula, with no trust step.

• After the fifth round (cb8ffefd41), same build type: the regress0/regress1 quantifier regressions, 445/445, every tester included; api_solver_black 131/131; git clang-format clean. The fifth-round code runs only while a hypothesis is active (the integer-to-real conversion sits in the directed-instance path), so the neutrality sweep above still applies.

• Verus against this build, on two trees: Verus main (da8fa532e), and verus#36 merged with main at 88e6566 (the Final preparations for arithmetic for building with libc++. cvc5/cvc5#33 merge that main has since taken conflicts with verus#36 in resident.rs, so that tree stops short of it). The resident harness cannot turn the in-session (get-info :version) check off, so the build ran behind a test-only wrapper that rewrites its version answer to the pinned 1.3.5.dev+main@79e8830; the solver is otherwise unchanged. Main: air 212/212 (with this cvc5 as VERUS_CVC5_PATH), rust_verify --lib 42/42, rust_verify_test --test resident --include-ignored 50/50, --test difficulty 3/3; the same counts as with the pinned release. verus#36: air 214/214, rust_verify --lib 46/46, resident 52/52, difficulty 3/3; with the pinned release, resident is 50/52, the two failures being the speculate tests (resident_speculate_probes_and_leaves_the_session_unchanged, resident_speculate_reads_terms_at_the_goal), which need this PR.

Overlap

Merged with main after #11, #12, #13 and #15. The #11 merge had two conflicts: isValidGetInfoFlag accepts both speculation and branch-profile, and Instantiate::presolve takes #11's pressure carry before Speculation::presolve(). This branch also adds an IncompleteId.

The Verus resident speculate request (BasisResearch/verus#36) and the MCP speculative_probe tool (BasisResearch/verus-tools-mcp#36) use this. verus#36 reads :instances, which for a directed term now shows it after substitution. Its AIR doc for pending ("no instantiation round ran") should now read "no round reached e-matching". After the fourth round, a formula whose variable the rewriter eliminated is found by its :qid, so no-quantifier there now means the :qid is absent, belongs to an alpha-equivalent duplicate, or names a formula without a :pattern that miniscoping split.

The named reports change what AIR reads for formulas the rewriter changed; none of its parsers needs a change. parse_provenance_lines takes (instantiations <atom> ...) only, and sent a formula printed in full to unparsed, so provenance used to drop these formulas' instances; it now counts them under their :qid. The :inst-pressure and :branch-profile rows that were named: false, quant_<n>, now carry their :qid and map to source; twin.rs keys rows by (qid, named), so a twin comparing runs of cvc5 from before and after this change would see these rows move. The instantiation graph's _unnamed_<i> nodes become named ones.

🤖 Generated with Claude Code