mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-09 17:31:57 +00:00
Code Activity

try per thread tree

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-09 18:57:35 -07:00
parent 9bab5ce7b7
commit 37c9534d04
2 changed files with 55 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

48
src/smt/smt_parallel2.cpp
View file

@ -73,10 +73,15 @@ namespace smt {
while (true) {
collect_shared_clauses(m_g2l);
#if 0
if (!b.get_cube(m_g2l, id, cube, node)) {
LOG_WORKER(1, " no more cubes\n");
return;
}
#else
if (!get_cube(cube, node))
return;
#endif
check_cube_start:
LOG_WORKER(1, " CUBE SIZE IN MAIN LOOP: " << cube.size() << "\n");
@ -97,7 +102,11 @@ namespace smt {
auto atom = get_split_atom();
if (!atom)
goto check_cube_start;
#if 0
b.split(m_l2g, id, node, atom);
#else
split(node, atom);
#endif
break;
}
case l_true: {
@ -126,7 +135,11 @@ namespace smt {
b.report_assumption_used(m_l2g, e); // report assumptions used in unsat core, so they can be used in final core
LOG_WORKER(1, " found unsat cube\n");
#if 0
b.backtrack(m_l2g, unsat_core, node);
#else
backtrack(unsat_core, node);
#endif
break;
}
}
@ -135,10 +148,43 @@ namespace smt {
}
}
bool parallel2::worker::get_cube(expr_ref_vector& cube, node*& n) {
node* t = m_search_tree.activate_node(n);
cube.reset();
if (!t) {
b.set_unsat(m_l2g, cube);
return false;
}
n = t;
while (t) {
if (cube_config::literal_is_null(t->get_literal()))
break;
cube.push_back(t->get_literal());
t = t->parent();
}
return true;
}
void parallel2::worker::backtrack(expr_ref_vector const& core, node* n) {
vector<expr_ref> core_copy;
for (auto c : core)
core_copy.push_back(expr_ref(c, m));
m_search_tree.backtrack(n, core_copy);
//LOG_WORKER(1, m_search_tree.display(verbose_stream() << bounded_pp_exprs(core) << "\n"););
}
void parallel2::worker::split(node* n, expr* atom) {
expr_ref lit(atom, m), nlit(m);
nlit = mk_not(m, lit);
IF_VERBOSE(1, verbose_stream() << "Batch manager splitting on literal: " << mk_bounded_pp(lit, m, 3) << "\n");
m_search_tree.split(n, lit, nlit);
}
parallel2::worker::worker(unsigned id, parallel2& p, expr_ref_vector const& _asms):
id(id), p(p), b(p.m_batch_manager), m_smt_params(p.ctx.get_fparams()), asms(m),
m_g2l(p.ctx.m, m),
m_l2g(m, p.ctx.m) {
m_l2g(m, p.ctx.m),
m_search_tree(expr_ref(m)) {
for (auto e : _asms)
asms.push_back(m_g2l(e));
LOG_WORKER(1, " created with " << asms.size() << " assumptions\n");

7
src/smt/smt_parallel2.h
View file

@ -64,6 +64,7 @@ namespace smt {
unsigned m_num_cubes = 0;
};
ast_manager& m;
parallel2& p;
std::mutex mux;
@ -135,6 +136,8 @@ namespace smt {
bool m_cubetree = false;
};
using node = search_tree::node<cube_config>;
unsigned id; // unique identifier for the worker
parallel2& p;
batch_manager& b;
@ -145,6 +148,7 @@ namespace smt {
random_gen m_rand;
scoped_ptr<context> ctx;
ast_translation m_g2l, m_l2g;
search_tree::tree<cube_config> m_search_tree;
unsigned m_num_shared_units = 0;
unsigned m_num_initial_atoms = 0;
@ -159,6 +163,9 @@ namespace smt {
m_config.m_threads_max_conflicts = (unsigned)(m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts);
} // allow for backoff scheme of conflicts within the thread for cube timeouts.
bool get_cube(expr_ref_vector& cube, node*& n);
void backtrack(expr_ref_vector const& core, node* n);
void split(node* n, expr* atom);
public:
worker(unsigned id, parallel2& p, expr_ref_vector const& _asms);