mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #6936

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-10-10 19:24:21 +09:00
parent 7afa4d0752
commit e8e636c3ec
2 changed files with 12 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/sat/sat_parallel.cpp
View file

@ -25,12 +25,7 @@ namespace sat {
void parallel::vector_pool::next(unsigned& index) { void parallel::vector_pool::next(unsigned& index) {
SASSERT(index < m_size); SASSERT(index < m_size);
unsigned n = index + 2 + get_length(index); unsigned n = index + 2 + get_length(index);
if (n >= m_size) { index = (n >= m_size) ? 0 : n;
index = 0;
}
else {
index = n;
}
} }
void parallel::vector_pool::reserve(unsigned num_threads, unsigned sz) { void parallel::vector_pool::reserve(unsigned num_threads, unsigned sz) {
@ -64,9 +59,8 @@ namespace sat {
} }
void parallel::vector_pool::end_add_vector() { void parallel::vector_pool::end_add_vector() {
if (m_tail >= m_size) { if (m_tail >= m_size)
m_tail = 0; m_tail = 0;
}
} }
@ -93,9 +87,9 @@ namespace sat {
parallel::parallel(solver& s): m_num_clauses(0), m_consumer_ready(false), m_scoped_rlimit(s.rlimit()) {} parallel::parallel(solver& s): m_num_clauses(0), m_consumer_ready(false), m_scoped_rlimit(s.rlimit()) {}
parallel::~parallel() { parallel::~parallel() {
for (unsigned i = 0; i < m_solvers.size(); ++i) { m_limits.reset();
dealloc(m_solvers[i]); for (auto* s : m_solvers)
} dealloc(s);
} }
void parallel::init_solvers(solver& s, unsigned num_extra_solvers) { void parallel::init_solvers(solver& s, unsigned num_extra_solvers) {
@ -106,9 +100,8 @@ namespace sat {
for (unsigned i = 0; i < num_extra_solvers; ++i) { for (unsigned i = 0; i < num_extra_solvers; ++i) {
s.m_params.set_uint("random_seed", s.m_rand()); s.m_params.set_uint("random_seed", s.m_rand());
if (i == 1 + num_threads/2) { if (i == 1 + num_threads/2)
s.m_params.set_sym("phase", symbol("random")); s.m_params.set_sym("phase", symbol("random"));
}
m_solvers[i] = alloc(sat::solver, s.m_params, m_limits[i]); m_solvers[i] = alloc(sat::solver, s.m_params, m_limits[i]);
m_solvers[i]->copy(s, true); m_solvers[i]->copy(s, true);
m_solvers[i]->set_par(this, i); m_solvers[i]->set_par(this, i);
@ -164,9 +157,8 @@ namespace sat {
IF_VERBOSE(3, verbose_stream() << owner << ": share " << c << "\n";); IF_VERBOSE(3, verbose_stream() << owner << ": share " << c << "\n";);
lock_guard lock(m_mux); lock_guard lock(m_mux);
m_pool.begin_add_vector(owner, n); m_pool.begin_add_vector(owner, n);
for (unsigned i = 0; i < n; ++i) { for (unsigned i = 0; i < n; ++i)
m_pool.add_vector_elem(c[i].index()); m_pool.add_vector_elem(c[i].index());
}
m_pool.end_add_vector(); m_pool.end_add_vector();
} }
@ -220,9 +212,8 @@ namespace sat {
if (m_priorities.empty()) if (m_priorities.empty())
return; return;
for (bool_var v = 0; v < m_priorities.size(); ++v) { for (bool_var v = 0; v < m_priorities.size(); ++v)
s.update_activity(v, m_priorities[v]); s.update_activity(v, m_priorities[v]);
}
s.m_activity_inc = 128; s.m_activity_inc = 128;
#endif #endif
} }

7
src/util/rlimit.h
View file

@ -91,8 +91,9 @@ public:
struct scoped_limits { struct scoped_limits {
reslimit& m_limit; reslimit& m_limit;
unsigned m_sz; unsigned m_sz = 0;
scoped_limits(reslimit& lim): m_limit(lim), m_sz(0) {} scoped_limits(reslimit& lim): m_limit(lim) {}
~scoped_limits() { for (unsigned i = 0; i < m_sz; ++i) m_limit.pop_child(); } ~scoped_limits() { reset(); }
void reset() { for (unsigned i = 0; i < m_sz; ++i) m_limit.pop_child(); m_sz = 0; }
void push_child(reslimit* lim) { m_limit.push_child(lim); ++m_sz; } void push_child(reslimit* lim) { m_limit.push_child(lim); ++m_sz; }
}; };