From a88f81bc28bc93561a48cb47a8d00dfd6d2599d0 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Mon, 30 Mar 2026 19:11:13 +0200 Subject: [PATCH] test: use DFS ordering for subgoals in mvcgen (#13193) This PR switches the mvcgen worklist from BFS (queue) to DFS (stack) ordering for subgoal processing. With the new do elaborator, `if`-without-`else` generates asymmetric bind depth between branches (`pure () >>= cont` is optimized to just `cont` in the else branch). This caused BFS-based VC numbering to depend on elaborator internals, swapping vc10/vc11 in test cases. DFS ordering follows the syntactic program structure more naturally and is robust to such bind-depth asymmetries. --------- Co-authored-by: Claude Opus 4.6 --- tests/bench/mvcgen/sym/cases/Cases/GetThrowSet.lean | 1 + tests/bench/mvcgen/sym/lib/VCGen.lean | 9 ++++----- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/bench/mvcgen/sym/cases/Cases/GetThrowSet.lean b/tests/bench/mvcgen/sym/cases/Cases/GetThrowSet.lean index 1229e9b730..3fb60fd78e 100644 --- a/tests/bench/mvcgen/sym/cases/Cases/GetThrowSet.lean +++ b/tests/bench/mvcgen/sym/cases/Cases/GetThrowSet.lean @@ -6,6 +6,7 @@ open Lean Meta Elab Tactic Sym Std Do SpecAttr namespace GetThrowSet set_option mvcgen.warning false +set_option backward.do.legacy false -- exercises asymmetric bind depth from new do elaborator abbrev M := ExceptT String <| StateM Nat diff --git a/tests/bench/mvcgen/sym/lib/VCGen.lean b/tests/bench/mvcgen/sym/lib/VCGen.lean index 286e0b212b..fdaa387343 100644 --- a/tests/bench/mvcgen/sym/lib/VCGen.lean +++ b/tests/bench/mvcgen/sym/lib/VCGen.lean @@ -876,11 +876,10 @@ meta def emitVC (goal : Grind.Goal) : VCGenM Unit := do meta def work (goal : Grind.Goal) : VCGenM Unit := do let mvarId ← preprocessMVar goal.mvarId let goal := { goal with mvarId } - let mut worklist := Std.Queue.empty.enqueue goal + let mut worklist := #[goal] repeat do - let some (goal, worklist') := worklist.dequeue? | break - let mut goal := goal - worklist := worklist' + let mut some goal := worklist.back? | break + worklist := worklist.pop let res ← solve goal.mvarId match res with | .noEntailment .. | .noProgramFoundInTarget .. => @@ -896,7 +895,7 @@ meta def work (goal : Grind.Goal) : VCGenM Unit := do -- to share E-graph context before forking. if subgoals.length > 1 then goal ← (← read).preTac.processHypotheses goal - worklist := worklist.enqueueAll (subgoals.map ({ goal with mvarId := · })) + worklist := worklist ++ (subgoals |>.map ({ goal with mvarId := · }) |>.reverse) public structure Result where invariants : Array MVarId