mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
SINGLE_THREAD: do not use pthread if possible (#4382)
This commit is contained in:
parent
5fe0eeda63
commit
3b0c40044f
|
@ -16,18 +16,18 @@ Revision History:
|
|||
|
||||
--*/
|
||||
#include<fstream>
|
||||
#include<mutex>
|
||||
#include "api/z3.h"
|
||||
#include "api/api_log_macros.h"
|
||||
#include "util/util.h"
|
||||
#include "util/z3_version.h"
|
||||
#include "util/mutex.h"
|
||||
|
||||
std::ostream * g_z3_log = nullptr;
|
||||
std::atomic<bool> g_z3_log_enabled;
|
||||
|
||||
#ifdef Z3_LOG_SYNC
|
||||
static std::mutex g_log_mux;
|
||||
#define SCOPED_LOCK() std::lock_guard<std::mutex> lock(g_log_mux)
|
||||
static mutex g_log_mux;
|
||||
#define SCOPED_LOCK() lock_guard lock(g_log_mux)
|
||||
#else
|
||||
#define SCOPED_LOCK() {}
|
||||
#endif
|
||||
|
|
|
@ -129,7 +129,7 @@ namespace sat {
|
|||
if (s.get_config().m_num_threads == 1 || s.m_par_syncing_clauses) return;
|
||||
flet<bool> _disable_sync_clause(s.m_par_syncing_clauses, true);
|
||||
{
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
lock_guard lock(m_mux);
|
||||
if (limit < m_units.size()) {
|
||||
// this might repeat some literals.
|
||||
out.append(m_units.size() - limit, m_units.c_ptr() + limit);
|
||||
|
@ -150,7 +150,7 @@ namespace sat {
|
|||
flet<bool> _disable_sync_clause(s.m_par_syncing_clauses, true);
|
||||
IF_VERBOSE(3, verbose_stream() << s.m_par_id << ": share " << l1 << " " << l2 << "\n";);
|
||||
{
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
lock_guard lock(m_mux);
|
||||
m_pool.begin_add_vector(s.m_par_id, 2);
|
||||
m_pool.add_vector_elem(l1.index());
|
||||
m_pool.add_vector_elem(l2.index());
|
||||
|
@ -164,7 +164,7 @@ namespace sat {
|
|||
unsigned n = c.size();
|
||||
unsigned owner = s.m_par_id;
|
||||
IF_VERBOSE(3, verbose_stream() << owner << ": share " << c << "\n";);
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
lock_guard lock(m_mux);
|
||||
m_pool.begin_add_vector(owner, n);
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
m_pool.add_vector_elem(c[i].index());
|
||||
|
@ -175,7 +175,7 @@ namespace sat {
|
|||
void parallel::get_clauses(solver& s) {
|
||||
if (s.m_par_syncing_clauses) return;
|
||||
flet<bool> _disable_sync_clause(s.m_par_syncing_clauses, true);
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
lock_guard lock(m_mux);
|
||||
_get_clauses(s);
|
||||
}
|
||||
|
||||
|
@ -227,12 +227,12 @@ namespace sat {
|
|||
}
|
||||
|
||||
void parallel::from_solver(solver& s) {
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
lock_guard lock(m_mux);
|
||||
_from_solver(s);
|
||||
}
|
||||
|
||||
bool parallel::to_solver(solver& s) {
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
lock_guard lock(m_mux);
|
||||
return _to_solver(s);
|
||||
}
|
||||
|
||||
|
@ -254,19 +254,19 @@ namespace sat {
|
|||
}
|
||||
|
||||
bool parallel::from_solver(i_local_search& s) {
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
lock_guard lock(m_mux);
|
||||
return _from_solver(s);
|
||||
}
|
||||
|
||||
void parallel::to_solver(i_local_search& s) {
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
lock_guard lock(m_mux);
|
||||
_to_solver(s);
|
||||
}
|
||||
|
||||
bool parallel::copy_solver(solver& s) {
|
||||
bool copied = false;
|
||||
{
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
lock_guard lock(m_mux);
|
||||
m_consumer_ready = true;
|
||||
if (m_solver_copy && s.m_clauses.size() > m_solver_copy->m_clauses.size()) {
|
||||
s.copy(*m_solver_copy, true);
|
||||
|
|
|
@ -24,7 +24,7 @@ Revision History:
|
|||
#include "util/map.h"
|
||||
#include "util/rlimit.h"
|
||||
#include "util/scoped_ptr_vector.h"
|
||||
#include <mutex>
|
||||
#include "util/mutex.h"
|
||||
|
||||
namespace sat {
|
||||
|
||||
|
@ -62,7 +62,7 @@ namespace sat {
|
|||
index_set m_unit_set;
|
||||
literal_vector m_lits;
|
||||
vector_pool m_pool;
|
||||
std::mutex m_mux;
|
||||
mutex m_mux;
|
||||
|
||||
// for exchange with local search:
|
||||
unsigned m_num_clauses;
|
||||
|
|
Loading…
Reference in a new issue