mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

try with std::vector and ptr_vectors

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-06-04 04:10:55 -07:00 • committed by Nuno Lopes
parent e4e60bff26
commit 9f3089b098
3 changed files with 34 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

60
src/api/api_log.cpp
View file

@ -24,7 +24,13 @@ Revision History:
std::ostream * g_z3_log = nullptr; std::ostream * g_z3_log = nullptr;
bool g_z3_log_enabled = false; bool g_z3_log_enabled = false;
#ifdef Z3_LOG_SYNC
static std::mutex g_log_mux; static std::mutex g_log_mux;
#define SCOPED_LOCK() std::lock_guard<std::mutex> lock(g_log_mux)
#else
#define SCOPED_LOCK() {}
#endif
extern "C" { extern "C" {
void Z3_close_log_unsafe(void) { void Z3_close_log_unsafe(void) {
@ -38,26 +44,20 @@ extern "C" {
bool Z3_API Z3_open_log(Z3_string filename) { bool Z3_API Z3_open_log(Z3_string filename) {
bool res = true; bool res = true;
#ifdef Z3_LOG_SYNC SCOPED_LOCK();
std::lock_guard<std::mutex> lock(g_log_mux); if (g_z3_log != nullptr)
{ Z3_close_log_unsafe();
#endif g_z3_log = alloc(std::ofstream, filename);
if (g_z3_log != nullptr) if (g_z3_log->bad() || g_z3_log->fail()) {
Z3_close_log_unsafe(); dealloc(g_z3_log);
g_z3_log = alloc(std::ofstream, filename); g_z3_log = nullptr;
if (g_z3_log->bad() || g_z3_log->fail()) { res = false;
dealloc(g_z3_log); }
g_z3_log = nullptr; else {
res = false; *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << " " << __DATE__ << "\"\n";
} g_z3_log->flush();
else { g_z3_log_enabled = true;
*g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << " " << __DATE__ << "\"\n";
g_z3_log->flush();
g_z3_log_enabled = true;
}
#ifdef Z3_LOG_SYNC
} }
#endif
return res; return res;
} }
@ -65,27 +65,15 @@ extern "C" {
void Z3_API Z3_append_log(Z3_string str) { void Z3_API Z3_append_log(Z3_string str) {
if (g_z3_log == nullptr) if (g_z3_log == nullptr)
return; return;
#ifdef Z3_LOG_SYNC SCOPED_LOCK();
std::lock_guard<std::mutex> lock(g_log_mux); if (g_z3_log != nullptr)
{ _Z3_append_log(static_cast<char const *>(str));
#endif
if (g_z3_log != nullptr)
_Z3_append_log(static_cast<char const *>(str));
#ifdef Z3_LOG_SYNC
}
#endif
} }
void Z3_API Z3_close_log(void) { void Z3_API Z3_close_log(void) {
if (g_z3_log != nullptr) { if (g_z3_log != nullptr) {
#ifdef Z3_LOG_SYNC SCOPED_LOCK();
std::lock_guard<std::mutex> lock(g_log_mux); Z3_close_log_unsafe();
{
#endif
Z3_close_log_unsafe();
#ifdef Z3_LOG_SYNC
}
#endif
} }
} }
} }

3
src/sat/sat_solver.cpp
View file

@ -1302,7 +1302,8 @@ namespace sat {
vector<std::thread> threads; vector<std::thread> threads;
for (int i = 0; i < num_threads; ++i) { for (int i = 0; i < num_threads; ++i) {
threads.push_back(std::thread([&]() { worker_thread(i); })); int id = i;
threads.push_back(std::thread([&]() { worker_thread(id); }));
} }
for (int i = 0; i < num_threads; ++i) { for (int i = 0; i < num_threads; ++i) {
threads[i].join(); threads[i].join();

13
src/tactic/tactical.cpp
View file

@ -22,6 +22,7 @@ Notes:
#include "util/scoped_ptr_vector.h" #include "util/scoped_ptr_vector.h"
#include "tactic/tactical.h" #include "tactic/tactical.h"
#include <thread> #include <thread>
#include <vector>
class binary_tactical : public tactic { class binary_tactical : public tactic {
protected: protected:
@ -458,12 +459,13 @@ public:
} }
}; };
vector<std::thread> threads; scoped_ptr_vector<std::thread> threads;
for (int i = 0; i < num_threads; ++i) { for (int i = 0; i < num_threads; ++i) {
threads.push_back(std::thread([&]() { worker_thread(i); })); int id = i;
threads.push_back(alloc(std::thread, [&]() { worker_thread(id); }));
} }
for (int i = 0; i < num_threads; ++i) { for (int i = 0; i < num_threads; ++i) {
threads[i].join(); threads[i]->join();
} }
if (finished_id == UINT_MAX) { if (finished_id == UINT_MAX) {
@ -659,10 +661,11 @@ public:
} }
}; };
vector<std::thread> threads; std::vector<std::thread> threads;
int num_threads = static_cast<int>(r1_size); int num_threads = static_cast<int>(r1_size);
for (int i = 0; i < num_threads; ++i) { for (int i = 0; i < num_threads; ++i) {
threads.push_back(std::thread([&]() { worker_thread(i); })); int id = i;
threads.emplace_back([&]() { worker_thread(id); });
} }
for (int i = 0; i < num_threads; ++i) { for (int i = 0; i < num_threads; ++i) {
threads[i].join(); threads[i].join();