mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-28 16:29:50 +00:00
Code Activity

add back statistics to smt-parallel

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-11-15 16:49:13 -08:00
parent 5690be8cfc
commit bd2ead977e
2 changed files with 14 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/smt_parallel.cpp
View file

@ -148,6 +148,7 @@ namespace smt {
void parallel::worker::share_units() { void parallel::worker::share_units() {
// Collect new units learned locally by this worker and send to batch manager // Collect new units learned locally by this worker and send to batch manager
ctx->pop_to_base_lvl(); ctx->pop_to_base_lvl();
unsigned sz = ctx->assigned_literals().size(); unsigned sz = ctx->assigned_literals().size();
for (unsigned j = m_num_shared_units; j < sz; ++j) { // iterate only over new literals since last sync for (unsigned j = m_num_shared_units; j < sz; ++j) { // iterate only over new literals since last sync
@ -156,7 +157,7 @@ namespace smt {
continue; continue;
if (m_config.m_share_units_initial_only && lit.var() >= m_num_initial_atoms) { if (m_config.m_share_units_initial_only && lit.var() >= m_num_initial_atoms) {
LOG_WORKER(2, " Skipping non-initial unit: " << lit.var() << "\n"); LOG_WORKER(4, " Skipping non-initial unit: " << lit.var() << "\n");
continue; // skip non-iniial atoms if configured to do so continue; // skip non-iniial atoms if configured to do so
} }
@ -285,6 +286,8 @@ namespace smt {
// node->get_status() == status::active // node->get_status() == status::active
// and depth is 'high' enough // and depth is 'high' enough
// then ignore split, and instead set the status of node to open. // then ignore split, and instead set the status of node to open.
++m_stats.m_num_cubes;
m_stats.m_max_cube_depth = std::max(m_stats.m_max_cube_depth, node->depth() + 1);
m_search_tree.split(node, lit, nlit); m_search_tree.split(node, lit, nlit);
} }
@ -303,7 +306,7 @@ namespace smt {
// 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) {
ctx->assert_expr(e); ctx->assert_expr(e);
LOG_WORKER(2, " asserting shared clause: " << mk_bounded_pp(e, m, 3) << "\n"); LOG_WORKER(4, " asserting shared clause: " << mk_bounded_pp(e, m, 3) << "\n");
} }
} }

9
src/util/search_tree.h
View file

@ -68,6 +68,15 @@ namespace search_tree {
node* left() const { return m_left; } node* left() const { return m_left; }
node* right() const { return m_right; } node* right() const { return m_right; }
node* parent() const { return m_parent; } node* parent() const { return m_parent; }
unsigned depth() const {
unsigned d = 0;
node* p = m_parent;
while (p) {
++d;
p = p->parent();
}
return d;
}
node* find_active_node() { node* find_active_node() {
if (m_status == status::active) if (m_status == status::active)