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

pfor

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-06-03 20:35:13 -07:00 committed by Nuno Lopes
parent 59330b3855
commit 1f84381c4c
2 changed files with 24 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/sat/sat_solver.cpp
View file

@ -1243,6 +1243,8 @@ namespace sat {
unsigned error_code = 0;
lbool result = l_undef;
bool canceled = false;
std::mutex mux;
auto worker_thread = [&](int i) {
try {
lbool r = l_undef;
@ -1259,8 +1261,8 @@ namespace sat {
r = check(num_lits, lits);
}
bool first = false;
#pragma omp critical (par_solver)
{
std::lock_guard<std::mutex> lock(mux);
if (finished_id == -1) {
finished_id = i;
first = true;

25
src/tactic/tactical.cpp
View file

@ -405,9 +405,9 @@ public:
std::string ex_msg;
unsigned error_code = 0;
std::mutex mux;
int num_threads = static_cast<int>(sz);
#pragma omp parallel for
for (int i = 0; i < static_cast<int>(sz); i++) {
auto worker_thread = [&](int i) {
goal_ref_buffer _result;
goal_ref in_copy = in_copies[i];
@ -455,7 +455,16 @@ public:
ex_msg = z3_ex.msg();
}
}
};
vector<std::thread> threads;
for (int i = 0; i < num_threads; ++i) {
threads.push_back(std::thread([&]() { worker_thread(i); }));
}
for (int i = 0; i < num_threads; ++i) {
threads[i].join();
}
if (finished_id == UINT_MAX) {
switch (ex_kind) {
case ERROR_EX: throw z3_error(error_code);
@ -548,8 +557,7 @@ public:
std::string ex_msg;
std::mutex mux;
#pragma omp parallel for
for (int i = 0; i < static_cast<int>(r1_size); i++) {
auto worker_thread = [&](int i) {
ast_manager & new_m = *(managers[i]);
goal_ref new_g = g_copies[i];
@ -648,6 +656,15 @@ public:
}
}
}
};
vector<std::thread> threads;
int num_threads = static_cast<int>(r1_size);
for (int i = 0; i < num_threads; ++i) {
threads.push_back(std::thread([&]() { worker_thread(i); }));
}
for (int i = 0; i < num_threads; ++i) {
threads[i].join();
}
if (failed) {