mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-01 13:39:28 +00:00
Code Activity

household cleanup

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-22 03:58:04 +03:00
parent e26f7b900c
commit f5c28a0b76
2 changed files with 10 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/smt/smt_parallel.cpp
View file

@ -72,7 +72,7 @@ namespace smt {
LOG_WORKER(1, " no more cubes\n");
return;
}
collect_shared_clauses(m_g2l);
collect_shared_clauses();
check_cube_start:
LOG_WORKER(1, " CUBE SIZE IN MAIN LOOP: " << cube.size() << "\n");
@ -129,13 +129,13 @@ namespace smt {
}
}
if (m_config.m_share_units)
share_units(m_l2g);
share_units();
}
}
parallel::worker::worker(unsigned id, parallel &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_search_tree(expr_ref(m)) {
m_l2g(m, p.ctx.m) {
for (auto e : _asms)
asms.push_back(m_g2l(e));
LOG_WORKER(1, " created with " << asms.size() << " assumptions\n");
@ -149,7 +149,7 @@ namespace smt {
m_num_initial_atoms = ctx->get_num_bool_vars();
}
void parallel::worker::share_units(ast_translation &l2g) {
void parallel::worker::share_units() {
// Collect new units learned locally by this worker and send to batch manager
ctx->pop_to_base_lvl();
unsigned sz = ctx->assigned_literals().size();
@ -169,7 +169,7 @@ namespace smt {
if (lit.sign())
e = m.mk_not(e); // negate if literal is negative
b.collect_clause(l2g, id, e);
b.collect_clause(m_l2g, id, e);
}
m_num_shared_units = sz;
}
@ -301,8 +301,8 @@ namespace smt {
}
}
void parallel::worker::collect_shared_clauses(ast_translation &g2l) {
expr_ref_vector new_clauses = b.return_shared_clauses(g2l, m_shared_clause_limit, id);
void parallel::worker::collect_shared_clauses() {
expr_ref_vector new_clauses = b.return_shared_clauses(m_g2l, m_shared_clause_limit, id);
// iterate over new clauses and assert them in the local context
for (expr *e : new_clauses) {
ctx->assert_expr(e);

7
src/smt/smt_parallel.h
View file

@ -11,7 +11,7 @@ Abstract:
Author:
Ilana 2025
Ilana Shapiro - 2025
Revision History:
@ -131,7 +131,6 @@ 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;
@ -140,7 +139,7 @@ namespace smt {
expr_ref get_split_atom();
lbool check_cube(expr_ref_vector const& cube);
void share_units(ast_translation& l2g);
void share_units();
void update_max_thread_conflicts() {
m_config.m_threads_max_conflicts = (unsigned)(m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts);
@ -152,7 +151,7 @@ namespace smt {
worker(unsigned id, parallel& p, expr_ref_vector const& _asms);
void run();
void collect_shared_clauses(ast_translation& g2l);
void collect_shared_clauses();
void cancel();
void collect_statistics(::statistics& st) const;