mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-10 04:12:24 +00:00
Code Activity

[code-simplifier] Simplify backbone/parallel code from PR #9343 (#9357)

Browse source 
* Initial plan

* Simplify backbone and parallel code paths from PR #9343

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/5bcd7f31-c5cc-4d1f-9ef1-6647950bab25

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-04-23 16:17:42 +02:00 • committed by GitHub
parent 99f64b80fa
commit f37f87422a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 12 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/smt_parallel.cpp
View file

@ -675,14 +675,7 @@ namespace smt {
LOG_BB_WORKER(1, " RESULT: " << r << " FOR CANDIDATE: " << mk_bounded_pp(bb_candidate, m, 3) << "\n");
if (r == l_false) {
auto core = ctx->unsat_core();
if (core.size() == 1) {
return true;
}
}
return false;
return r == l_false && ctx->unsat_core().size() == 1;
}
void parallel::worker::share_units() {
@ -1315,8 +1308,7 @@ namespace smt {
m_batch_manager.initialize(num_global_bb_threads);
// Launch threads
vector<std::thread> threads;
threads.resize(total_threads);
vector<std::thread> threads(total_threads);
unsigned thread_idx = 0;
for (auto* w : m_workers)
threads[thread_idx++] = std::thread([&, w]() { w->run(); });

3
src/smt/smt_parallel.h
View file

@ -234,8 +234,9 @@ namespace smt {
void share_units();
void update_max_thread_conflicts() {
// allow for backoff scheme of conflicts within the thread for cube timeouts.
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.
}
void simplify();
bb_candidates find_backbone_candidates(unsigned k = 10);

10
src/util/search_tree.h
View file

@ -32,9 +32,9 @@ Author:
--*/
#pragma once
#include "util/util.h"
#include "util/vector.h"
#pragma once
namespace search_tree {
@ -100,7 +100,11 @@ namespace search_tree {
for (unsigned i = 0; i < indent; ++i)
out << " ";
Config::display_literal(out, m_literal);
out << (get_status() == status::open ? " (o)" : get_status() == status::closed ? " (c)" : " (a)");
switch (get_status()) {
case status::open: out << " (o)"; break;
case status::closed: out << " (c)"; break;
case status::active: out << " (a)"; break;
}
out << "\n";
if (m_left)
m_left->display(out, indent + 2);
@ -528,6 +532,7 @@ namespace search_tree {
find_nonclosed_nodes_with_literal_rec(m_root.get(), lit, out);
}
private:
void find_nonclosed_nodes_with_literal_rec(node<Config>* n, literal const& lit, ptr_vector<node<Config>>& out) {
if (!n)
return;
@ -539,6 +544,7 @@ namespace search_tree {
find_nonclosed_nodes_with_literal_rec(n->right(), lit, out);
}
public:
void dec_active_workers(node<Config>* n) {
if (!n)
return;