mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

smt_parallel: keep preprocessing for quantified formulas so MBQI can solve

Browse source 
The parallel SMT worker contexts disable preprocessing
(`m_preprocess = false`) so that units/clauses exchanged between workers
refer to a stable, shared atom set. This is fine for the quantifier-free
cubing the parallel solver was designed for, but it breaks quantifier
reasoning: MBQI relies on preprocessing (macro/quantifier simplification
and trigger setup). With preprocessing disabled, a worker running MBQI on
a satisfiable quantified formula can spin indefinitely and never find a
model that the sequential solver dispatches immediately.

Concretely, on `iss-3268/bug-1.smt2` (a satisfiable quantified array
formula that sets `smt.threads 4`) the sequential solver returns `sat` in
0.04s (64 conflicts), while every parallel worker fails to find a model
even with an effectively unbounded per-cube conflict budget, so the run
hits the wall-clock timeout.

Gate preprocessing on `ctx->has_quantifiers()` in the three worker
constructors (CDCL worker, core-minimizer worker, backbones worker):
keep it disabled for quantifier-free problems (unchanged behavior for the
cubing use case) and enable it when quantifiers are present so MBQI works.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-07-03 05:52:36 -07:00 • committed by GitHub
parent f15584cdae
commit 46a45dee04
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 18 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/smt/smt_parallel.cpp
View file

@ -626,7 +626,12 @@ namespace smt {
ctx->set_logic(p.ctx.m_setup.get_logic());
context::copy(p.ctx, *ctx, true);
ctx->pop_to_base_lvl();
ctx->get_fparams().m_preprocess = false; // avoid preprocessing lemmas that are exchanged
// Disable preprocessing so units/clauses exchanged between workers refer to a
// stable shared atom set, but keep it enabled for quantified formulas: MBQI
// relies on preprocessing (macro/quantifier simplification, trigger setup) and
// without it a satisfiable quantified formula can spin without ever finding a
// model the sequential solver dispatches immediately.
ctx->get_fparams().m_preprocess = ctx->has_quantifiers();
}
void parallel::core_minimizer_worker::cancel() {
@ -866,7 +871,12 @@ namespace smt {
ctx->pop_to_base_lvl();
m_shared_units_prefix = ctx->assigned_literals().size();
m_num_initial_atoms = ctx->get_num_bool_vars();
ctx->get_fparams().m_preprocess = false; // avoid preprocessing lemmas that are exchanged
// Disable preprocessing so units/clauses exchanged between workers refer to a
// stable shared atom set, but keep it enabled for quantified formulas: MBQI
// relies on preprocessing (macro/quantifier simplification, trigger setup) and
// without it a satisfiable quantified formula can spin without ever finding a
// model the sequential solver dispatches immediately.
ctx->get_fparams().m_preprocess = ctx->has_quantifiers();
parallel_params pp(p.ctx.m_params);
m_config.m_inprocessing = false;
@ -901,7 +911,12 @@ namespace smt {
ctx->pop_to_base_lvl();
m_shared_units_prefix = ctx->assigned_literals().size();
m_num_initial_atoms = ctx->get_num_bool_vars();
ctx->get_fparams().m_preprocess = false; // avoid preprocessing lemmas that are exchanged
// Disable preprocessing so units/clauses exchanged between workers refer to a
// stable shared atom set, but keep it enabled for quantified formulas: MBQI
// relies on preprocessing (macro/quantifier simplification, trigger setup) and
// without it a satisfiable quantified formula can spin without ever finding a
// model the sequential solver dispatches immediately.
ctx->get_fparams().m_preprocess = ctx->has_quantifiers();
m_use_failed_literal_test = false;
}