mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-14 09:45:36 +00:00
Code Activity

Recalibrate the seq_monadic work budget for the interval-refinement product

Browse source 
The per-decide() work budget was set to 200000 when product enumeration was a
cartesian product over derivative cofactors.  The interval-refinement (ITE)
product that replaced it in #10455 turns that product into a sum: a cell
enumeration costs sum_i I_i + 1 pops instead of prod_i k_i combinations, so an
individual pop is now roughly an order of magnitude cheaper.  The budget was
never retuned, so it fires on goals the monadic path can now finish outright
and hands them to the legacy fallback instead.

split_membership_easy_sat_0019 is the clearest example: at 200000 it takes 3
budget bails, 8293 cofactor calls, 67 monadic checks and 35 legacy fallbacks;
at 1000000 it takes zero bails, 131 cofactor calls and a single monadic check.

Raise the budget to 1000000 and record the calibration in a comment.

Measured on the bench regexes corpus (ClemensRegex + MargusRegex, 1476 files,
10s timeout, smt.seq.regex_monadic=true), 200000 vs 1000000:

  decided           1377 -> 1383   (+6 gained, 0 lost)
  commonly decided  135.9s -> 105.8s   (-22.2%)
  sat/unsat contradictions: 0

The six newly decided goals are split_membership_medium sat_0014, sat_0049,
sat_0054, unsat_0023, unsat_0029 and unsat_0032.  Individual movers include
easy_unsat_0010 3682 -> 1316 ms, medium_sat_0026 2586 -> 328 ms and
easy_sat_0018 2299 -> 244 ms.

The same sweep over the nseq/Nielsen consumer (smt.nseq.monadic_split=true on
the c3 branch) is neutral: 1377 -> 1379 decided, -1.1% time, 0 contradictions.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
This commit is contained in:
Margus Veanes 2026-08-08 12:59:04 -07:00
parent 40953fa703
commit a9894be876
1 changed files with 6 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/rewriter/seq_monadic.cpp
View file

@ -721,7 +721,12 @@ lbool seq_monadic::decide(membership_vec const& memberships) {
m_rp_cache.maybe_reset(1u << 16);
reset_ivl_cache();
m_rw.get_derive().maybe_reset_cached_cofactors(1u << 16);
m_budget = 200000;
// Work budget for one decide() call, counted in search-node and product-pop
// units. Recalibrated from 200000 once the interval-refinement product
// replaced the cartesian one: a pop now costs roughly an order of magnitude
// less, so the old value bailed to the legacy fallback on goals the monadic
// path can finish outright.
m_budget = 1000000;
m_giveup = false;
lbool r = l_true; // empty conjunction is vacuously true
if (!memberships.empty() && !prepare(memberships))