mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
capture i by value
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
27971e3f68
commit
7f74382863
|
@ -1300,13 +1300,12 @@ namespace sat {
|
|||
}
|
||||
};
|
||||
|
||||
vector<std::thread> threads;
|
||||
vector<std::thread> threads(num_threads);
|
||||
for (int i = 0; i < num_threads; ++i) {
|
||||
int id = i;
|
||||
threads.push_back(std::thread([&]() { worker_thread(id); }));
|
||||
threads[i] = std::thread([&, i]() { worker_thread(i); });
|
||||
}
|
||||
for (int i = 0; i < num_threads; ++i) {
|
||||
threads[i].join();
|
||||
for (auto & th : threads) {
|
||||
th.join();
|
||||
}
|
||||
|
||||
if (IS_AUX_SOLVER(finished_id)) {
|
||||
|
|
|
@ -59,7 +59,7 @@ public:
|
|||
}
|
||||
|
||||
~smt_tactic() override {
|
||||
SASSERT(m_ctx == 0);
|
||||
SASSERT(m_ctx == nullptr);
|
||||
}
|
||||
|
||||
smt_params & fparams() {
|
||||
|
@ -132,7 +132,6 @@ public:
|
|||
new_ctx->set_progress_callback(o.m_callback);
|
||||
}
|
||||
o.m_ctx = new_ctx;
|
||||
|
||||
}
|
||||
|
||||
~scoped_init_ctx() {
|
||||
|
@ -208,7 +207,7 @@ public:
|
|||
m_ctx->collect_statistics(m_stats);
|
||||
throw;
|
||||
}
|
||||
SASSERT(m_ctx);
|
||||
SASSERT(m_ctx);
|
||||
m_ctx->collect_statistics(m_stats);
|
||||
proof * pr = m_ctx->get_proof();
|
||||
TRACE("smt_tactic", tout << r << " " << pr << "\n";);
|
||||
|
|
|
@ -370,9 +370,13 @@ enum par_exception_kind {
|
|||
|
||||
class par_tactical : public or_else_tactical {
|
||||
|
||||
std::string ex_msg;
|
||||
unsigned error_code;
|
||||
|
||||
public:
|
||||
par_tactical(unsigned num, tactic * const * ts):or_else_tactical(num, ts) {}
|
||||
par_tactical(unsigned num, tactic * const * ts):or_else_tactical(num, ts) {
|
||||
error_code = 0;
|
||||
}
|
||||
~par_tactical() override {}
|
||||
|
||||
|
||||
|
@ -404,19 +408,15 @@ public:
|
|||
|
||||
unsigned finished_id = UINT_MAX;
|
||||
par_exception_kind ex_kind = DEFAULT_EX;
|
||||
std::string ex_msg;
|
||||
unsigned error_code = 0;
|
||||
std::mutex mux;
|
||||
int num_threads = static_cast<int>(sz);
|
||||
|
||||
auto worker_thread = [&](int i) {
|
||||
goal_ref_buffer _result;
|
||||
|
||||
std::mutex mux;
|
||||
|
||||
auto worker_thread = [&](unsigned i) {
|
||||
goal_ref_buffer _result;
|
||||
goal_ref in_copy = in_copies[i];
|
||||
tactic & t = *(ts.get(i));
|
||||
|
||||
try {
|
||||
// IF_VERBOSE(0, verbose_stream() << "start\n");
|
||||
t(in_copy, _result);
|
||||
bool first = false;
|
||||
{
|
||||
|
@ -428,11 +428,11 @@ public:
|
|||
}
|
||||
if (first) {
|
||||
for (unsigned j = 0; j < sz; j++) {
|
||||
if (static_cast<unsigned>(i) != j) {
|
||||
if (i != j) {
|
||||
managers[j]->limit().cancel();
|
||||
}
|
||||
}
|
||||
IF_VERBOSE(0, verbose_stream() << "first\n");
|
||||
|
||||
ast_translation translator(*(managers[i]), m, false);
|
||||
for (goal* g : _result) {
|
||||
result.push_back(g->translate(translator));
|
||||
|
@ -461,13 +461,13 @@ public:
|
|||
}
|
||||
};
|
||||
|
||||
scoped_ptr_vector<std::thread> threads;
|
||||
for (int i = 0; i < num_threads; ++i) {
|
||||
int id = i;
|
||||
threads.push_back(alloc(std::thread, [&]() { worker_thread(id); }));
|
||||
vector<std::thread> threads(sz);
|
||||
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
threads[i] = std::thread([&, i]() { worker_thread(i); });
|
||||
}
|
||||
for (int i = 0; i < num_threads; ++i) {
|
||||
threads[i]->join();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
threads[i].join();
|
||||
}
|
||||
|
||||
if (finished_id == UINT_MAX) {
|
||||
|
@ -562,7 +562,7 @@ public:
|
|||
std::string ex_msg;
|
||||
std::mutex mux;
|
||||
|
||||
auto worker_thread = [&](int i) {
|
||||
auto worker_thread = [&](unsigned i) {
|
||||
ast_manager & new_m = *(managers[i]);
|
||||
goal_ref new_g = g_copies[i];
|
||||
|
||||
|
@ -663,13 +663,11 @@ public:
|
|||
}
|
||||
};
|
||||
|
||||
std::vector<std::thread> threads;
|
||||
int num_threads = static_cast<int>(r1_size);
|
||||
for (int i = 0; i < num_threads; ++i) {
|
||||
int id = i;
|
||||
threads.emplace_back([&]() { worker_thread(id); });
|
||||
vector<std::thread> threads(r1_size);
|
||||
for (unsigned i = 0; i < r1_size; ++i) {
|
||||
threads[i] = std::thread([&, i]() { worker_thread(i); });
|
||||
}
|
||||
for (int i = 0; i < num_threads; ++i) {
|
||||
for (unsigned i = 0; i < r1_size; ++i) {
|
||||
threads[i].join();
|
||||
}
|
||||
|
||||
|
|
|
@ -20,6 +20,8 @@ Revision History:
|
|||
#include "util/common_msgs.h"
|
||||
|
||||
|
||||
static std::mutex g_rlimit_mux;
|
||||
|
||||
reslimit::reslimit():
|
||||
m_cancel(0),
|
||||
m_suspend(false),
|
||||
|
@ -70,34 +72,34 @@ char const* reslimit::get_cancel_msg() const {
|
|||
}
|
||||
|
||||
void reslimit::push_child(reslimit* r) {
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
std::lock_guard<std::mutex> lock(g_rlimit_mux);
|
||||
m_children.push_back(r);
|
||||
}
|
||||
|
||||
void reslimit::pop_child() {
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
std::lock_guard<std::mutex> lock(g_rlimit_mux);
|
||||
m_children.pop_back();
|
||||
}
|
||||
|
||||
void reslimit::cancel() {
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
std::lock_guard<std::mutex> lock(g_rlimit_mux);
|
||||
set_cancel(m_cancel+1);
|
||||
}
|
||||
|
||||
|
||||
void reslimit::reset_cancel() {
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
std::lock_guard<std::mutex> lock(g_rlimit_mux);
|
||||
set_cancel(0);
|
||||
}
|
||||
|
||||
void reslimit::inc_cancel() {
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
std::lock_guard<std::mutex> lock(g_rlimit_mux);
|
||||
set_cancel(m_cancel+1);
|
||||
}
|
||||
|
||||
|
||||
void reslimit::dec_cancel() {
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
std::lock_guard<std::mutex> lock(g_rlimit_mux);
|
||||
if (m_cancel > 0) {
|
||||
set_cancel(m_cancel-1);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue