mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

remove remaining _NO_OMP_

Browse source
This commit is contained in:
Nuno Lopes 2019-06-05 10:07:16 +01:00
parent 37882f5afa
commit 9b375150eb
11 changed files with 39 additions and 71 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/util/mpff.cpp
View file

@ -376,7 +376,7 @@ void mpff_manager::set(mpff & n, unsynch_mpz_manager & m, mpz const & v) {
set_core(n, m, v); set_core(n, m, v);
} }
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
void mpff_manager::set(mpff & n, synch_mpz_manager & m, mpz const & v) { void mpff_manager::set(mpff & n, synch_mpz_manager & m, mpz const & v) {
set_core(n, m, v); set_core(n, m, v);
} }
@ -399,7 +399,7 @@ void mpff_manager::set(mpff & n, unsynch_mpq_manager & m, mpq const & v) {
set_core(n, m, v); set_core(n, m, v);
} }
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
void mpff_manager::set(mpff & n, synch_mpq_manager & m, mpq const & v) { void mpff_manager::set(mpff & n, synch_mpq_manager & m, mpq const & v) {
set_core(n, m, v); set_core(n, m, v);
} }
@ -1081,7 +1081,7 @@ void mpff_manager::significand(mpff const & n, unsynch_mpz_manager & m, mpz & t)
significand_core(n, m, t); significand_core(n, m, t);
} }
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
void mpff_manager::significand(mpff const & n, synch_mpz_manager & m, mpz & t) { void mpff_manager::significand(mpff const & n, synch_mpz_manager & m, mpz & t) {
significand_core(n, m, t); significand_core(n, m, t);
} }
@ -1115,7 +1115,7 @@ void mpff_manager::to_mpz(mpff const & n, unsynch_mpz_manager & m, mpz & t) {
to_mpz_core(n, m, t); to_mpz_core(n, m, t);
} }
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
void mpff_manager::to_mpz(mpff const & n, synch_mpz_manager & m, mpz & t) { void mpff_manager::to_mpz(mpff const & n, synch_mpz_manager & m, mpz & t) {
to_mpz_core(n, m, t); to_mpz_core(n, m, t);
} }
@ -1162,7 +1162,7 @@ void mpff_manager::to_mpq(mpff const & n, unsynch_mpq_manager & m, mpq & t) {
to_mpq_core(n, m, t); to_mpq_core(n, m, t);
} }
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
void mpff_manager::to_mpq(mpff const & n, synch_mpq_manager & m, mpq & t) { void mpff_manager::to_mpq(mpff const & n, synch_mpq_manager & m, mpq & t) {
to_mpq_core(n, m, t); to_mpq_core(n, m, t);
} }

10
src/util/mpff.h
View file

@ -58,7 +58,7 @@ class mpz;
class mpq; class mpq;
template<bool SYNCH> class mpz_manager; template<bool SYNCH> class mpz_manager;
template<bool SYNCH> class mpq_manager; template<bool SYNCH> class mpq_manager;
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
typedef mpz_manager<true> synch_mpz_manager; typedef mpz_manager<true> synch_mpz_manager;
typedef mpq_manager<true> synch_mpq_manager; typedef mpq_manager<true> synch_mpq_manager;
#else #else
@ -218,7 +218,7 @@ public:
\brief Return the significand as a mpz numeral. \brief Return the significand as a mpz numeral.
*/ */
void significand(mpff const & n, unsynch_mpz_manager & m, mpz & r); void significand(mpff const & n, unsynch_mpz_manager & m, mpz & r);
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
void significand(mpff const & n, synch_mpz_manager & m, mpz & r); void significand(mpff const & n, synch_mpz_manager & m, mpz & r);
#endif #endif
@ -386,7 +386,7 @@ public:
void set(mpff & n, mpff const & v); void set(mpff & n, mpff const & v);
void set(mpff & n, unsynch_mpz_manager & m, mpz const & v); void set(mpff & n, unsynch_mpz_manager & m, mpz const & v);
void set(mpff & n, unsynch_mpq_manager & m, mpq const & v); void set(mpff & n, unsynch_mpq_manager & m, mpq const & v);
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
void set(mpff & n, synch_mpq_manager & m, mpq const & v); void set(mpff & n, synch_mpq_manager & m, mpq const & v);
void set(mpff & n, synch_mpz_manager & m, mpz const & v); void set(mpff & n, synch_mpz_manager & m, mpz const & v);
#endif #endif
@ -429,7 +429,7 @@ public:
*/ */
void to_mpz(mpff const & n, unsynch_mpz_manager & m, mpz & t); void to_mpz(mpff const & n, unsynch_mpz_manager & m, mpz & t);
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
/** /**
\brief Convert n into a mpz numeral. \brief Convert n into a mpz numeral.
@ -447,7 +447,7 @@ public:
*/ */
void to_mpq(mpff const & n, unsynch_mpq_manager & m, mpq & t); void to_mpq(mpff const & n, unsynch_mpq_manager & m, mpq & t);
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
/** /**
\brief Convert n into a mpq numeral. \brief Convert n into a mpq numeral.

8
src/util/mpfx.cpp
View file

@ -272,7 +272,7 @@ void mpfx_manager::set(mpfx & n, unsynch_mpz_manager & m, mpz const & v) {
set_core(n, m, v); set_core(n, m, v);
} }
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
void mpfx_manager::set(mpfx & n, synch_mpz_manager & m, mpz const & v) { void mpfx_manager::set(mpfx & n, synch_mpz_manager & m, mpz const & v) {
set_core(n, m, v); set_core(n, m, v);
} }
@ -311,7 +311,7 @@ void mpfx_manager::set(mpfx & n, unsynch_mpq_manager & m, mpq const & v) {
set_core(n, m, v); set_core(n, m, v);
} }
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
void mpfx_manager::set(mpfx & n, synch_mpq_manager & m, mpq const & v) { void mpfx_manager::set(mpfx & n, synch_mpq_manager & m, mpq const & v) {
set_core(n, m, v); set_core(n, m, v);
} }
@ -718,7 +718,7 @@ void mpfx_manager::to_mpz(mpfx const & n, unsynch_mpz_manager & m, mpz & t) {
to_mpz_core(n, m, t); to_mpz_core(n, m, t);
} }
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
void mpfx_manager::to_mpz(mpfx const & n, synch_mpz_manager & m, mpz & t) { void mpfx_manager::to_mpz(mpfx const & n, synch_mpz_manager & m, mpz & t) {
to_mpz_core(n, m, t); to_mpz_core(n, m, t);
} }
@ -744,7 +744,7 @@ void mpfx_manager::to_mpq(mpfx const & n, unsynch_mpq_manager & m, mpq & t) {
to_mpq_core(n, m, t); to_mpq_core(n, m, t);
} }
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
void mpfx_manager::to_mpq(mpfx const & n, synch_mpq_manager & m, mpq & t) { void mpfx_manager::to_mpq(mpfx const & n, synch_mpq_manager & m, mpq & t) {
to_mpq_core(n, m, t); to_mpq_core(n, m, t);
} }

8
src/util/mpfx.h
View file

@ -51,7 +51,7 @@ class mpz;
class mpq; class mpq;
template<bool SYNCH> class mpz_manager; template<bool SYNCH> class mpz_manager;
template<bool SYNCH> class mpq_manager; template<bool SYNCH> class mpq_manager;
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
typedef mpz_manager<true> synch_mpz_manager; typedef mpz_manager<true> synch_mpz_manager;
typedef mpq_manager<true> synch_mpq_manager; typedef mpq_manager<true> synch_mpq_manager;
#else #else
@ -318,7 +318,7 @@ public:
void set(mpfx & n, mpfx const & v); void set(mpfx & n, mpfx const & v);
void set(mpfx & n, unsynch_mpz_manager & m, mpz const & v); void set(mpfx & n, unsynch_mpz_manager & m, mpz const & v);
void set(mpfx & n, unsynch_mpq_manager & m, mpq const & v); void set(mpfx & n, unsynch_mpq_manager & m, mpq const & v);
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
void set(mpfx & n, synch_mpz_manager & m, mpz const & v); void set(mpfx & n, synch_mpz_manager & m, mpz const & v);
void set(mpfx & n, synch_mpq_manager & m, mpq const & v); void set(mpfx & n, synch_mpq_manager & m, mpq const & v);
#endif #endif
@ -366,7 +366,7 @@ public:
*/ */
void to_mpz(mpfx const & n, unsynch_mpz_manager & m, mpz & t); void to_mpz(mpfx const & n, unsynch_mpz_manager & m, mpz & t);
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
/** /**
\brief Convert n into a mpz numeral. \brief Convert n into a mpz numeral.
@ -380,7 +380,7 @@ public:
*/ */
void to_mpq(mpfx const & n, unsynch_mpq_manager & m, mpq & t); void to_mpq(mpfx const & n, unsynch_mpq_manager & m, mpq & t);
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
/** /**
\brief Convert n into a mpq numeral. \brief Convert n into a mpq numeral.
*/ */

2
src/util/mpq.cpp
View file

@ -428,7 +428,7 @@ void mpq_manager<SYNCH>::rat_sub(mpq const & a, mpq const & b, mpq & c) {
} }
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
template class mpq_manager<true>; template class mpq_manager<true>;
#endif #endif
template class mpq_manager<false>; template class mpq_manager<false>;

2
src/util/mpq.h
View file

@ -816,7 +816,7 @@ public:
bool is_even(mpq const & a) { return is_int(a) && is_even(a.m_num); } bool is_even(mpq const & a) { return is_int(a) && is_even(a.m_num); }
}; };
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
typedef mpq_manager<true> synch_mpq_manager; typedef mpq_manager<true> synch_mpq_manager;
#else #else
typedef mpq_manager<false> synch_mpq_manager; typedef mpq_manager<false> synch_mpq_manager;

2
src/util/mpq_inf.cpp
View file

@ -39,7 +39,7 @@ std::string mpq_inf_manager<SYNCH>::to_string(mpq_inf const & a) {
} }
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
template class mpq_inf_manager<true>; template class mpq_inf_manager<true>;
#endif #endif
template class mpq_inf_manager<false>; template class mpq_inf_manager<false>;

2
src/util/mpq_inf.h
View file

@ -279,7 +279,7 @@ public:
mpq_manager<SYNCH>& get_mpq_manager() { return m; } mpq_manager<SYNCH>& get_mpq_manager() { return m; }
}; };
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
typedef mpq_inf_manager<true> synch_mpq_inf_manager; typedef mpq_inf_manager<true> synch_mpq_inf_manager;
#else #else
typedef mpq_inf_manager<false> synch_mpq_inf_manager; typedef mpq_inf_manager<false> synch_mpq_inf_manager;

2
src/util/mpz.cpp
View file

@ -2466,7 +2466,7 @@ bool mpz_manager<SYNCH>::divides(mpz const & a, mpz const & b) {
return r; return r;
} }
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
template class mpz_manager<true>; template class mpz_manager<true>;
#endif #endif
template class mpz_manager<false>; template class mpz_manager<false>;

21
src/util/util.cpp
View file

@ -17,15 +17,16 @@ Revision History:
--*/ --*/
#ifdef _WINDOWS
#include <windows.h>
#endif
#include <thread>
#include "util/util.h" #include "util/util.h"
#ifndef SINGLE_THREAD
#include <mutex>
#include <thread>
static std::mutex g_verbose_mux; static std::mutex g_verbose_mux;
void verbose_lock() { g_verbose_mux.lock(); } void verbose_lock() { g_verbose_mux.lock(); }
void verbose_unlock() { g_verbose_mux.unlock(); } void verbose_unlock() { g_verbose_mux.unlock(); }
#endif
static unsigned g_verbosity_level = 0; static unsigned g_verbosity_level = 0;
@ -43,23 +44,13 @@ void set_verbose_stream(std::ostream& str) {
g_verbose_stream = &str; g_verbose_stream = &str;
} }
#ifndef _NO_OMP_ #ifndef SINGLE_THREAD
#ifdef _WINDOWS
static int g_thread_id = 0;
#else
static std::thread::id g_thread_id = std::this_thread::get_id(); static std::thread::id g_thread_id = std::this_thread::get_id();
#endif
static bool g_is_threaded = false; static bool g_is_threaded = false;
bool is_threaded() { bool is_threaded() {
if (g_is_threaded) return true; if (g_is_threaded) return true;
#ifdef _WINDOWS
int thid = GetCurrentThreadId();
g_is_threaded = g_thread_id != thid && g_thread_id != 0;
g_thread_id = thid;
#else
g_is_threaded = std::this_thread::get_id() != g_thread_id; g_is_threaded = std::this_thread::get_id() != g_thread_id;
#endif
return g_is_threaded; return g_is_threaded;
} }
#endif #endif

43
src/util/util.h
View file

@ -16,15 +16,13 @@ Author:
Revision History: Revision History:
--*/ --*/
#ifndef UTIL_H_ #pragma once
#define UTIL_H_
#include "util/debug.h" #include "util/debug.h"
#include "util/memory_manager.h" #include "util/memory_manager.h"
#include<iostream> #include<iostream>
#include<climits> #include<climits>
#include<limits> #include<limits>
#include<mutex>
#include<stdint.h> #include<stdint.h>
#ifndef SIZE_MAX #ifndef SIZE_MAX
@ -47,14 +45,10 @@ static_assert(sizeof(int64_t) == 8, "64 bits");
#endif #endif
#ifdef _WINDOWS #ifdef _WINDOWS
#define SSCANF sscanf_s
// #define SPRINTF sprintf_s
#define SPRINTF_D(_buffer_, _i_) sprintf_s(_buffer_, Z3_ARRAYSIZE(_buffer_), "%d", _i_) #define SPRINTF_D(_buffer_, _i_) sprintf_s(_buffer_, Z3_ARRAYSIZE(_buffer_), "%d", _i_)
#define SPRINTF_U(_buffer_, _u_) sprintf_s(_buffer_, Z3_ARRAYSIZE(_buffer_), "%u", _u_) #define SPRINTF_U(_buffer_, _u_) sprintf_s(_buffer_, Z3_ARRAYSIZE(_buffer_), "%u", _u_)
#define _Exit exit #define _Exit exit
#else #else
#define SSCANF sscanf
// #define SPRINTF sprintf
#define SPRINTF_D(_buffer_, _i_) sprintf(_buffer_, "%d", _i_) #define SPRINTF_D(_buffer_, _i_) sprintf(_buffer_, "%d", _i_)
#define SPRINTF_U(_buffer_, _u_) sprintf(_buffer_, "%u", _u_) #define SPRINTF_U(_buffer_, _u_) sprintf(_buffer_, "%u", _u_)
#endif #endif
@ -174,8 +168,11 @@ void set_verbosity_level(unsigned lvl);
unsigned get_verbosity_level(); unsigned get_verbosity_level();
std::ostream& verbose_stream(); std::ostream& verbose_stream();
void set_verbose_stream(std::ostream& str); void set_verbose_stream(std::ostream& str);
#ifdef SINGLE_THREAD
# define is_threaded() false
#else
bool is_threaded(); bool is_threaded();
#endif
#define IF_VERBOSE(LVL, CODE) { \ #define IF_VERBOSE(LVL, CODE) { \
@ -189,6 +186,9 @@ bool is_threaded();
} } ((void) 0) } } ((void) 0)
#ifdef SINGLE_THREAD
#define LOCK_CODE(CODE) CODE;
#else
void verbose_lock(); void verbose_lock();
void verbose_unlock(); void verbose_unlock();
@ -197,7 +197,8 @@ void verbose_unlock();
verbose_lock(); \ verbose_lock(); \
CODE; \ CODE; \
verbose_unlock(); \ verbose_unlock(); \
} \ }
#endif
template<typename T> template<typename T>
struct default_eq { struct default_eq {
@ -280,20 +281,6 @@ inline std::ostream & operator<<(std::ostream & out, std::pair<T1, T2> const & p
return out; return out;
} }
template<typename IT>
bool has_duplicates(const IT & begin, const IT & end) {
for (IT it1 = begin; it1 != end; ++it1) {
IT it2 = it1;
++it2;
for (; it2 != end; ++it2) {
if (*it1 == *it2) {
return true;
}
}
}
return false;
}
#ifndef _WINDOWS #ifndef _WINDOWS
#ifndef __declspec #ifndef __declspec
#define __declspec(X) #define __declspec(X)
@ -364,12 +351,6 @@ void shuffle(unsigned sz, T * array, random_gen & gen) {
} }
} }
#ifdef _EXTERNAL_RELEASE
#define INTERNAL_CODE(CODE) ((void) 0)
#else
#define INTERNAL_CODE(CODE) { CODE } ((void) 0)
#endif
void fatal_error(int error_code); void fatal_error(int error_code);
void set_fatal_error_handler(void (*pfn)(int error_code)); void set_fatal_error_handler(void (*pfn)(int error_code));
@ -408,7 +389,3 @@ inline size_t megabytes_to_bytes(unsigned mb) {
r = SIZE_MAX; r = SIZE_MAX;
return r; return r;
} }
#endif /* UTIL_H_ */