mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 17:01:55 +00:00
Code Activity

cleanup

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-19 19:32:54 -07:00
parent 7eb6ef3161
commit 6b66cbf547
1 changed files with 18 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

44
src/smt/smt_parallel.cpp
View file

@ -59,8 +59,6 @@ namespace smt {
#include <thread> #include <thread>
#define SHARE_SEARCH_TREE 1
#define LOG_WORKER(lvl, s) IF_VERBOSE(lvl, verbose_stream() << "Worker " << id << s) #define LOG_WORKER(lvl, s) IF_VERBOSE(lvl, verbose_stream() << "Worker " << id << s)
namespace smt { namespace smt {
@ -265,9 +263,8 @@ namespace smt {
vector<cube_config::literal> g_core; vector<cube_config::literal> g_core;
for (auto c : core) { for (auto c : core) {
expr_ref g_c(l2g(c), m); expr_ref g_c(l2g(c), m);
if (is_assumption(g_c)) if (!is_assumption(g_c))
continue; g_core.push_back(expr_ref(l2g(c), m));
g_core.push_back(expr_ref(l2g(c), m));
} }
m_search_tree.backtrack(node, g_core); m_search_tree.backtrack(node, g_core);
@ -308,9 +305,8 @@ namespace smt {
expr_ref_vector new_clauses = b.return_shared_clauses(g2l, m_shared_clause_limit, id); expr_ref_vector new_clauses = b.return_shared_clauses(g2l, m_shared_clause_limit, id);
// iterate over new clauses and assert them in the local context // iterate over new clauses and assert them in the local context
for (expr *e : new_clauses) { for (expr *e : new_clauses) {
expr_ref local_clause(e, g2l.to()); ctx->assert_expr(e);
ctx->assert_expr(local_clause); LOG_WORKER(2, " asserting shared clause: " << mk_bounded_pp(e, m, 3) << "\n");
LOG_WORKER(2, " asserting shared clause: " << mk_bounded_pp(local_clause, m, 3) << "\n");
} }
} }
@ -319,9 +315,8 @@ namespace smt {
std::scoped_lock lock(mux); std::scoped_lock lock(mux);
expr_ref_vector result(g2l.to()); expr_ref_vector result(g2l.to());
for (unsigned i = worker_limit; i < shared_clause_trail.size(); ++i) { for (unsigned i = worker_limit; i < shared_clause_trail.size(); ++i) {
if (shared_clause_trail[i].source_worker_id == worker_id) if (shared_clause_trail[i].source_worker_id != worker_id)
continue; // skip clauses from the requesting worker result.push_back(g2l(shared_clause_trail[i].clause.get()));
result.push_back(g2l(shared_clause_trail[i].clause.get()));
} }
worker_limit = shared_clause_trail.size(); // update the worker limit to the end of the current trail worker_limit = shared_clause_trail.size(); // update the worker limit to the end of the current trail
return result; return result;
@ -468,22 +463,19 @@ namespace smt {
node *t = m_search_tree.activate_node(n); node *t = m_search_tree.activate_node(n);
if (!t) if (!t)
t = m_search_tree.find_active_node(); t = m_search_tree.find_active_node();
if (t) { if (!t)
IF_VERBOSE(1, m_search_tree.display(verbose_stream()); verbose_stream() << "\n";); return false;
n = t; IF_VERBOSE(1, m_search_tree.display(verbose_stream()); verbose_stream() << "\n";);
while (t) { n = t;
if (cube_config::literal_is_null(t->get_literal())) while (t) {
break; if (cube_config::literal_is_null(t->get_literal()))
expr_ref lit(g2l.to()); break;
lit = g2l(t->get_literal().get()); expr_ref lit(g2l.to());
cube.push_back(lit); lit = g2l(t->get_literal().get());
t = t->parent(); cube.push_back(lit);
} t = t->parent();
// IF_VERBOSE(1, verbose_stream() << "got cube " << cube << " from " << " " << t->get_status() <<
// "\n";);
return true;
} }
return false; return true;
} }
void parallel::batch_manager::initialize() { void parallel::batch_manager::initialize() {