mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

make it easier to debug parallel

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-10 07:09:04 +02:00
parent 3e6ff768a5
commit 34f878fb97
1 changed files with 10 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/solver/parallel_tactic.cpp
View file

@ -503,7 +503,10 @@ private:
cube.append(s.split_cubes(1)); cube.append(s.split_cubes(1));
SASSERT(cube.size() <= 1); SASSERT(cube.size() <= 1);
IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :split-cube " << cube.size() << ")\n";); IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :split-cube " << cube.size() << ")\n";);
{
// std::lock_guard<std::mutex> lock(m_mutex);
if (!s.cubes().empty()) m_queue.add_task(s.clone()); if (!s.cubes().empty()) m_queue.add_task(s.clone());
}
if (!cube.empty()) { if (!cube.empty()) {
s.assert_cube(cube.get(0).cube()); s.assert_cube(cube.get(0).cube());
vars.reset(); vars.reset();
@ -612,7 +615,11 @@ private:
if (cubes.empty()) return; if (cubes.empty()) return;
add_branches(cubes.size()); add_branches(cubes.size());
s.set_cubes(cubes); s.set_cubes(cubes);
solver_state* s1 = s.clone(); solver_state* s1 = nullptr;
{
// std::lock_guard<std::mutex> lock(m_mutex);
s1 = s.clone();
}
s1->inc_width(width); s1->inc_width(width);
m_queue.add_task(s1); m_queue.add_task(s1);
} }