mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

fix issues in par

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-02-06 13:38:07 -08:00
parent fe105d94a0
commit 4831c45ad8
2 changed files with 20 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/sat/sat_par.cpp
View file

@ -77,9 +77,14 @@ namespace sat {
bool par::vector_pool::get_vector(unsigned owner, unsigned& n, unsigned const*& ptr) { bool par::vector_pool::get_vector(unsigned owner, unsigned& n, unsigned const*& ptr) {
unsigned head = m_heads[owner]; unsigned head = m_heads[owner];
unsigned iterations = 0;
while (head != m_tail) { while (head != m_tail) {
++iterations;
if (head == 0 && m_tail >= m_size) {
break;
}
SASSERT(head < m_size); SASSERT(head < m_size);
IF_VERBOSE(3, verbose_stream() << owner << ": head: " << head << " tail: " << m_tail << "\n";); IF_VERBOSE((iterations > m_size ? 0 : 3), verbose_stream() << owner << ": head: " << head << " tail: " << m_tail << "\n";);
bool is_self = owner == get_owner(head); bool is_self = owner == get_owner(head);
next(m_heads[owner]); next(m_heads[owner]);
if (!is_self) { if (!is_self) {
@ -88,9 +93,6 @@ namespace sat {
return true; return true;
} }
head = m_heads[owner]; head = m_heads[owner];
if (head == 0 && m_tail >= m_size) {
break;
}
} }
return false; return false;
} }
@ -109,6 +111,8 @@ namespace sat {
symbol saved_phase = s.m_params.get_sym("phase", symbol("caching")); symbol saved_phase = s.m_params.get_sym("phase", symbol("caching"));
for (unsigned i = 0; i < num_extra_solvers; ++i) { for (unsigned i = 0; i < num_extra_solvers; ++i) {
m_limits.push_back(reslimit()); m_limits.push_back(reslimit());
}
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"));

12
src/sat/sat_solver.cpp
View file

@ -364,6 +364,11 @@ namespace sat {
} }
unsigned some_idx = c.size() >> 1; unsigned some_idx = c.size() >> 1;
literal block_lit = c[some_idx]; literal block_lit = c[some_idx];
if (m_watches.size() <= (~c[0]).index()) std::cout << c << "\n";
if (m_watches.size() <= (~c[1]).index()) std::cout << c << "\n";
if (m_watches[(~c[0]).index()].size() >= 20000) {
std::cout << m_par_id << ": " << c << "\n";
}
m_watches[(~c[0]).index()].push_back(watched(block_lit, cls_off)); m_watches[(~c[0]).index()].push_back(watched(block_lit, cls_off));
m_watches[(~c[1]).index()].push_back(watched(block_lit, cls_off)); m_watches[(~c[1]).index()].push_back(watched(block_lit, cls_off));
return reinit; return reinit;
@ -836,7 +841,8 @@ namespace sat {
int num_threads = static_cast<int>(m_config.m_num_parallel); int num_threads = static_cast<int>(m_config.m_num_parallel);
int num_extra_solvers = num_threads - 1; int num_extra_solvers = num_threads - 1;
sat::par par(*this); sat::par par(*this);
par.reserve(num_threads, 1 << 16); // par.reserve(num_threads, 1 << 16);
par.reserve(num_threads, 1 << 9);
par.init_solvers(*this, num_extra_solvers); par.init_solvers(*this, num_extra_solvers);
int finished_id = -1; int finished_id = -1;
std::string ex_msg; std::string ex_msg;
@ -877,11 +883,13 @@ namespace sat {
} }
} }
if (i != num_extra_solvers) { if (i != num_extra_solvers) {
canceled = rlimit().inc(); canceled = !rlimit().inc();
if (!canceled) {
rlimit().cancel(); rlimit().cancel();
} }
} }
} }
}
catch (z3_error & err) { catch (z3_error & err) {
error_code = err.error_code(); error_code = err.error_code();
ex_kind = ERROR_EX; ex_kind = ERROR_EX;