mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-27 03:41:29 +00:00
Code Activity

merge

Browse source
This commit is contained in:
Ilana Shapiro 2025-08-14 17:06:46 -07:00
commit 4362f2d8cb
3 changed files with 14 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/params/CMakeLists.txt
View file

@ -21,6 +21,7 @@ z3_add_component(params
bv_rewriter_params.pyg
fpa_rewriter_params.pyg
fpa2bv_rewriter_params.pyg
smt_parallel_params.pyg
pattern_inference_params_helper.pyg
poly_rewriter_params.pyg
rewriter_params.pyg

7
src/params/smt_parallel_params.pyg Normal file
View file

@ -0,0 +1,7 @@
def_module_params('smt_parallel',
export=True,
description='Experimental parameters for parallel solving',
params=(
('share_units', BOOL, True, 'share units'),
('share_conflicts', BOOL, True, 'share conflicts'),
))

9
src/smt/smt_parallel.cpp
View file

@ -23,6 +23,7 @@ Author:
#include "ast/ast_translation.h"
#include "smt/smt_parallel.h"
#include "smt/smt_lookahead.h"
#include "params/smt_parallel_params.hpp"
#ifdef SINGLE_THREAD
@ -99,12 +100,14 @@ namespace smt {
b.report_assumption_used(l2g, e); // report assumptions used in unsat core, so they can be used in final core
IF_VERBOSE(1, verbose_stream() << "Worker " << id << " found unsat cube\n");
b.collect_clause(l2g, id, mk_not(mk_and(unsat_core)));
if (smt_parallel_params(p.ctx.m_params).share_conflicts())
b.collect_clause(l2g, id, mk_not(mk_and(unsat_core)));
break;
}
}
}
share_units(l2g);
if (smt_parallel_params(p.ctx.m_params).share_units())
share_units(l2g);
}
}
@ -124,6 +127,7 @@ namespace smt {
void parallel::worker::share_units(ast_translation& l2g) {
// Collect new units learned locally by this worker and send to batch manager
ctx->pop_to_base_lvl();
unsigned sz = ctx->assigned_literals().size();
for (unsigned j = m_num_shared_units; j < sz; ++j) { // iterate only over new literals since last sync
literal lit = ctx->assigned_literals()[j];
@ -340,7 +344,6 @@ namespace smt {
// currenly, the code just implements the greedy strategy
void parallel::batch_manager::return_cubes(ast_translation& l2g, vector<expr_ref_vector>const& C_worker, expr_ref_vector const& A_worker) {
std::scoped_lock lock(mux);
auto atom_in_cube = [&](expr_ref_vector const& cube, expr* atom) {
return any_of(cube, [&](expr* e) { return e == atom || (m.is_not(e, e) && e == atom); });
};