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

add mode for running smt_parallel with 1 thread (i.e. 1 thread with parallel framework overhead) for ablation

Browse source
This commit is contained in:
Ilana Shapiro 2026-07-11 23:41:24 -07:00
parent c383004968
commit 2456afc5bb
4 changed files with 16 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/params/smt_parallel_params.pyg
View file

@ -3,6 +3,7 @@ def_module_params('smt_parallel',
description='Experimental parameters for parallel solving',
params=(
('inprocessing', BOOL, False, 'integrate in-processing as a heuristic simplification'),
('force_enable', BOOL, False, 'force the SMT parallel architecture even when smt.threads is 1'),
('sls', BOOL, False, 'add sls-tactic as a separate worker thread outside the search tree parallelism'),
('num_global_bb_fl_threads', UINT, 0, 'run failed-literal backbone worker threads; default is 0 (off), supported values are 1 (negative mode only) or 2 (negative and positive mode)'),
('num_global_bb_batch_threads', UINT, 0, 'run Janota-style chunking backbone worker threads; default is 0 (off), supported values are 1 (negative mode only) or 2 (negative and positive mode)'),

12
src/smt/smt_context.cpp
View file

@ -32,6 +32,7 @@ Revision History:
#include "model/model_params.hpp"
#include "model/model.h"
#include "model/model_pp.h"
#include "params/smt_parallel_params.hpp"
#include "smt/smt_context.h"
#include "smt/smt_quick_checker.h"
#include "smt/uses_theory.h"
@ -3615,6 +3616,13 @@ namespace smt {
return m_model.get() != nullptr;
}
bool context::use_parallel_solver() const {
if (m.has_trace_stream() || m_par)
return false;
smt_parallel_params pp(m_params);
return m_fparams.m_threads > 1 || pp.force_enable();
}
/**
\brief Setup the logical context based on the current set of
asserted formulas and execute the check command.
@ -3628,7 +3636,7 @@ namespace smt {
SASSERT(!m_setup.already_configured());
setup_context(m_fparams.m_auto_config);
if (m_fparams.m_threads > 1 && !m.has_trace_stream()) {
if (use_parallel_solver()) {
parallel p(*this);
expr_ref_vector asms(m);
return p(asms);
@ -3695,7 +3703,7 @@ namespace smt {
SASSERT(at_base_level());
setup_context(false);
search_completion sc(*this);
if (m_fparams.m_threads > 1 && !m.has_trace_stream()) {
if (use_parallel_solver()) {
expr_ref_vector asms(m, num_assumptions, assumptions);
parallel p(*this);
return p(asms);

2
src/smt/smt_context.h
View file

@ -131,6 +131,7 @@ namespace smt {
bool m_is_auxiliary = false; // used to prevent unwanted information from being logged.
class parallel* m_par = nullptr;
unsigned m_par_index = 0;
bool use_parallel_solver() const;
bool m_internalizing_assertions = false;
lbool m_internal_completed = l_undef;
@ -1918,4 +1919,3 @@ namespace smt {
};

5
src/smt/smt_parallel.cpp
View file

@ -854,6 +854,7 @@ namespace smt {
LOG_WORKER(1, " created with " << asms.size() << " assumptions\n");
m_smt_params.m_random_seed += id; // ensure different random seed for each worker
ctx = alloc(context, m, m_smt_params, p.ctx.get_params());
ctx->m_par = &p;
ctx->set_logic(p.ctx.m_setup.get_logic());
context::copy(p.ctx, *ctx, true);
// don't share initial units
@ -1839,7 +1840,9 @@ namespace smt {
m_core_minimizer_worker = nullptr;
scoped_limits sl(m.limit());
flet<unsigned> _nt(ctx.m_fparams.m_threads, 1);
SASSERT(num_workers > 1);
if (num_workers == 0)
throw default_exception("smt.threads must be at least 1 in parallel mode");
SASSERT(num_workers > 1 || pp.force_enable());
for (unsigned i = 0; i < num_workers; ++i)
m_workers.push_back(alloc(worker, i, *this, asms));
for (auto w : m_workers)