From 9b375150ebdb0bcb04ae3a606774080c36dcac6a Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 5 Jun 2019 10:07:16 +0100 Subject: [PATCH] remove remaining _NO_OMP_ --- src/util/mpff.cpp | 10 +++++----- src/util/mpff.h | 10 +++++----- src/util/mpfx.cpp | 8 ++++---- src/util/mpfx.h | 8 ++++---- src/util/mpq.cpp | 2 +- src/util/mpq.h | 2 +- src/util/mpq_inf.cpp | 2 +- src/util/mpq_inf.h | 2 +- src/util/mpz.cpp | 2 +- src/util/util.cpp | 21 ++++++--------------- src/util/util.h | 43 ++++++++++--------------------------------- 11 files changed, 39 insertions(+), 71 deletions(-) diff --git a/src/util/mpff.cpp b/src/util/mpff.cpp index 8ca2e983f..a46757059 100644 --- a/src/util/mpff.cpp +++ b/src/util/mpff.cpp @@ -376,7 +376,7 @@ void mpff_manager::set(mpff & n, unsynch_mpz_manager & m, mpz const & 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) { 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); } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD void mpff_manager::set(mpff & n, synch_mpq_manager & m, mpq const & 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); } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD void mpff_manager::significand(mpff const & n, synch_mpz_manager & m, mpz & 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); } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD void mpff_manager::to_mpz(mpff const & n, synch_mpz_manager & m, mpz & 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); } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD void mpff_manager::to_mpq(mpff const & n, synch_mpq_manager & m, mpq & t) { to_mpq_core(n, m, t); } diff --git a/src/util/mpff.h b/src/util/mpff.h index 6f1e9d23c..c7d14bac4 100644 --- a/src/util/mpff.h +++ b/src/util/mpff.h @@ -58,7 +58,7 @@ class mpz; class mpq; template class mpz_manager; template class mpq_manager; -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD typedef mpz_manager synch_mpz_manager; typedef mpq_manager synch_mpq_manager; #else @@ -218,7 +218,7 @@ public: \brief Return the significand as a mpz numeral. */ 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); #endif @@ -386,7 +386,7 @@ public: void set(mpff & n, mpff const & v); void set(mpff & n, unsynch_mpz_manager & m, mpz 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_mpz_manager & m, mpz const & v); #endif @@ -429,7 +429,7 @@ public: */ 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. @@ -447,7 +447,7 @@ public: */ 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. diff --git a/src/util/mpfx.cpp b/src/util/mpfx.cpp index 8ed16ec68..4769ab24a 100644 --- a/src/util/mpfx.cpp +++ b/src/util/mpfx.cpp @@ -272,7 +272,7 @@ void mpfx_manager::set(mpfx & n, unsynch_mpz_manager & m, mpz const & 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) { 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); } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD void mpfx_manager::set(mpfx & n, synch_mpq_manager & m, mpq const & 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); } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD void mpfx_manager::to_mpz(mpfx const & n, synch_mpz_manager & m, mpz & 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); } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD void mpfx_manager::to_mpq(mpfx const & n, synch_mpq_manager & m, mpq & t) { to_mpq_core(n, m, t); } diff --git a/src/util/mpfx.h b/src/util/mpfx.h index 6de3f251b..ddaf6f89a 100644 --- a/src/util/mpfx.h +++ b/src/util/mpfx.h @@ -51,7 +51,7 @@ class mpz; class mpq; template class mpz_manager; template class mpq_manager; -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD typedef mpz_manager synch_mpz_manager; typedef mpq_manager synch_mpq_manager; #else @@ -318,7 +318,7 @@ public: void set(mpfx & n, mpfx const & v); void set(mpfx & n, unsynch_mpz_manager & m, mpz 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_mpq_manager & m, mpq const & v); #endif @@ -366,7 +366,7 @@ public: */ 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. @@ -380,7 +380,7 @@ public: */ 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. */ diff --git a/src/util/mpq.cpp b/src/util/mpq.cpp index b126f4c5d..e3f7292e4 100644 --- a/src/util/mpq.cpp +++ b/src/util/mpq.cpp @@ -428,7 +428,7 @@ void mpq_manager::rat_sub(mpq const & a, mpq const & b, mpq & c) { } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD template class mpq_manager; #endif template class mpq_manager; diff --git a/src/util/mpq.h b/src/util/mpq.h index 20802f786..ac96b8b7c 100644 --- a/src/util/mpq.h +++ b/src/util/mpq.h @@ -816,7 +816,7 @@ public: bool is_even(mpq const & a) { return is_int(a) && is_even(a.m_num); } }; -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD typedef mpq_manager synch_mpq_manager; #else typedef mpq_manager synch_mpq_manager; diff --git a/src/util/mpq_inf.cpp b/src/util/mpq_inf.cpp index 69de425cf..f8d5ff4f0 100644 --- a/src/util/mpq_inf.cpp +++ b/src/util/mpq_inf.cpp @@ -39,7 +39,7 @@ std::string mpq_inf_manager::to_string(mpq_inf const & a) { } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD template class mpq_inf_manager; #endif template class mpq_inf_manager; diff --git a/src/util/mpq_inf.h b/src/util/mpq_inf.h index c7bd261e6..69ad655df 100644 --- a/src/util/mpq_inf.h +++ b/src/util/mpq_inf.h @@ -279,7 +279,7 @@ public: mpq_manager& get_mpq_manager() { return m; } }; -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD typedef mpq_inf_manager synch_mpq_inf_manager; #else typedef mpq_inf_manager synch_mpq_inf_manager; diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 73697512d..cda4b599a 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -2466,7 +2466,7 @@ bool mpz_manager::divides(mpz const & a, mpz const & b) { return r; } -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD template class mpz_manager; #endif template class mpz_manager; diff --git a/src/util/util.cpp b/src/util/util.cpp index 4b5489dc2..714c947a9 100644 --- a/src/util/util.cpp +++ b/src/util/util.cpp @@ -17,15 +17,16 @@ Revision History: --*/ -#ifdef _WINDOWS -#include -#endif -#include #include "util/util.h" +#ifndef SINGLE_THREAD +#include +#include + static std::mutex g_verbose_mux; void verbose_lock() { g_verbose_mux.lock(); } void verbose_unlock() { g_verbose_mux.unlock(); } +#endif static unsigned g_verbosity_level = 0; @@ -43,23 +44,13 @@ void set_verbose_stream(std::ostream& str) { g_verbose_stream = &str; } -#ifndef _NO_OMP_ -#ifdef _WINDOWS -static int g_thread_id = 0; -#else +#ifndef SINGLE_THREAD static std::thread::id g_thread_id = std::this_thread::get_id(); -#endif static bool g_is_threaded = false; bool is_threaded() { 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; -#endif return g_is_threaded; } #endif diff --git a/src/util/util.h b/src/util/util.h index 39ca45701..5860382c6 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -16,15 +16,13 @@ Author: Revision History: --*/ -#ifndef UTIL_H_ -#define UTIL_H_ +#pragma once #include "util/debug.h" #include "util/memory_manager.h" #include #include #include -#include #include #ifndef SIZE_MAX @@ -47,14 +45,10 @@ static_assert(sizeof(int64_t) == 8, "64 bits"); #endif #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_U(_buffer_, _u_) sprintf_s(_buffer_, Z3_ARRAYSIZE(_buffer_), "%u", _u_) #define _Exit exit #else -#define SSCANF sscanf -// #define SPRINTF sprintf #define SPRINTF_D(_buffer_, _i_) sprintf(_buffer_, "%d", _i_) #define SPRINTF_U(_buffer_, _u_) sprintf(_buffer_, "%u", _u_) #endif @@ -174,8 +168,11 @@ void set_verbosity_level(unsigned lvl); unsigned get_verbosity_level(); std::ostream& verbose_stream(); void set_verbose_stream(std::ostream& str); +#ifdef SINGLE_THREAD +# define is_threaded() false +#else bool is_threaded(); - +#endif #define IF_VERBOSE(LVL, CODE) { \ @@ -189,6 +186,9 @@ bool is_threaded(); } } ((void) 0) +#ifdef SINGLE_THREAD +#define LOCK_CODE(CODE) CODE; +#else void verbose_lock(); void verbose_unlock(); @@ -197,7 +197,8 @@ void verbose_unlock(); verbose_lock(); \ CODE; \ verbose_unlock(); \ - } \ + } +#endif template struct default_eq { @@ -280,20 +281,6 @@ inline std::ostream & operator<<(std::ostream & out, std::pair const & p return out; } -template -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 __declspec #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 set_fatal_error_handler(void (*pfn)(int error_code)); @@ -408,7 +389,3 @@ inline size_t megabytes_to_bytes(unsigned mb) { r = SIZE_MAX; return r; } - - -#endif /* UTIL_H_ */ -