mux

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

CMakeLists.txt

@@ -272,41 +272,6 @@ else()
   message(STATUS "Not using libgmp")
 endif()
 
-################################################################################
-# OpenMP support
-################################################################################
-find_package(OpenMP)
-if (OPENMP_FOUND)
-  set(USE_OPENMP_DEFAULT ON)
-else()
-  set(USE_OPENMP_DEFAULT OFF)
-endif()
-# By setting `USE_OPENMP` this way configuration will fail during the first
-# configure if the user explicitly passes `-DUSE_OPENMP=ON` and the compiler
-# does not support OpenMP. However if the option is not set explicitly during
-# the first configure OpenMP support will be automatically enabled/disabled
-# depending on whether OpenMP is available.
-option(USE_OPENMP "Use OpenMP" ${USE_OPENMP_DEFAULT})
-
-if (USE_OPENMP)
-  if (NOT OPENMP_FOUND)
-    message(FATAL_ERROR "USE_OPENMP is ON but your compiler does not support OpenMP")
-  endif()
-
-  list(APPEND Z3_COMPONENT_CXX_FLAGS ${OpenMP_CXX_FLAGS})
-  # GCC and Clang need to have additional flags passed to the linker.
-  # We can't do ``target_link_libraries(libz3 INTERFACE ${OpenMP_CXX_FLAGS})``
-  # because ``/openmp`` is interpreted as file name rather than a linker
-  # flag by MSVC and breaks the build
-  if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR
-      ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
-    list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS ${OpenMP_CXX_FLAGS})
-  endif()
-  message(STATUS "Using OpenMP")
-else()
-  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_NO_OMP_")
-  message(STATUS "Not using OpenMP")
-endif()
 
 ################################################################################
 # API Log sync
@@ -316,9 +281,6 @@ option(API_LOG_SYNC
   OFF
 )
 if (API_LOG_SYNC)
-  if (NOT USE_OPENMP)
-    message(FATAL_ERROR "API_LOG_SYNC feature requires OpenMP")
-  endif()
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-DZ3_LOG_SYNC")
   message(STATUS "Using API_LOG_SYNC")
 else()

cmake/z3_append_linker_flag_list_to_target.cmake

@@ -3,7 +3,7 @@
 # them to append them as strings to the ``LINK_FLAGS`` property of
 # the specified target.
 # E.g.
-# z3_append_linker_flag_list_to_target(mytarget "-fopenmp" "-static")
+# z3_append_linker_flag_list_to_target(mytarget "-static")
 function(z3_append_linker_flag_list_to_target target)
   if (NOT (TARGET "${target}"))
     message(FATAL_ERROR "Specified target \"${target}\" is not a target")

src/api/api_context.cpp

@@ -119,28 +119,22 @@ namespace api {
 
     context::set_interruptable::set_interruptable(context & ctx, event_handler & i):
         m_ctx(ctx) {
-        #pragma omp critical (set_interruptable) 
+        std::lock_guard<std::mutex> lock(ctx.m_mux);
-        {
+        SASSERT(m_ctx.m_interruptable == 0);
-            SASSERT(m_ctx.m_interruptable == 0);
+        m_ctx.m_interruptable = &i;        
-            m_ctx.m_interruptable = &i;
-        }
     }
 
     context::set_interruptable::~set_interruptable() {
-        #pragma omp critical (set_interruptable) 
+        std::lock_guard<std::mutex> lock(m_ctx.m_mux);
-        {
+        m_ctx.m_interruptable = nullptr;        
-            m_ctx.m_interruptable = nullptr;
-        }
     }
 
     void context::interrupt() {
-        #pragma omp critical (set_interruptable)
+        std::lock_guard<std::mutex> lock(m_mux);
-        {
+        if (m_interruptable)
-            if (m_interruptable)
+            (*m_interruptable)(API_INTERRUPT_EH_CALLER);
-                (*m_interruptable)(API_INTERRUPT_EH_CALLER);
+        m_limit.cancel();
-            m_limit.cancel();
+        m().limit().cancel();        
-            m().limit().cancel();
-        }
     }
     
     void context::set_error_code(Z3_error_code err, char const* opt_msg) {

src/api/api_context.h

@@ -42,6 +42,7 @@ Revision History:
 #include "ast/rewriter/seq_rewriter.h"
 #include "smt/smt_solver.h"
 #include "solver/solver.h"
+#include <mutex>
 
 namespace smtlib {
     class parser;
@@ -79,6 +80,7 @@ namespace api {
         scoped_ptr<ast_manager>    m_manager;
         scoped_ptr<cmd_context>    m_cmd;
         add_plugins                m_plugins;
+        std::mutex                 m_mux;
 
         arith_util                 m_arith_util;
         bv_util                    m_bv_util;

src/api/api_log.cpp

@@ -16,6 +16,7 @@ Revision History:
 
 --*/
 #include<fstream>
+#include<mutex>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "util/util.h"
@@ -23,6 +24,7 @@ Revision History:
 
 std::ostream * g_z3_log = nullptr;
 bool g_z3_log_enabled   = false;
+static std::mutex g_log_mux;
 
 extern "C" {
     void Z3_close_log_unsafe(void) {
@@ -37,7 +39,7 @@ extern "C" {
         bool res = true;
 
 #ifdef Z3_LOG_SYNC
-        #pragma omp critical (z3_log)
+        std::lock_guard<std::mutex> lock(g_log_mux);
         {
 #endif
             if (g_z3_log != nullptr)
@@ -64,7 +66,7 @@ extern "C" {
         if (g_z3_log == nullptr)
             return;
 #ifdef Z3_LOG_SYNC
-        #pragma omp critical (z3_log)
+        std::lock_guard<std::mutex> lock(g_log_mux);
         {
 #endif
             if (g_z3_log != nullptr)
@@ -77,7 +79,7 @@ extern "C" {
     void Z3_API Z3_close_log(void) {
         if (g_z3_log != nullptr) {
 #ifdef Z3_LOG_SYNC
-            #pragma omp critical (z3_log)
+            std::lock_guard<std::mutex> lock(g_log_mux);
             {
 #endif
                 Z3_close_log_unsafe();

src/ast/rewriter/der.cpp

@@ -436,11 +436,8 @@ void der_rewriter::operator()(expr * t, expr_ref & result, proof_ref & result_pr
 
 void der_rewriter::cleanup() {
     ast_manager & m = m_imp->m();
-    #pragma omp critical (th_rewriter)
+    dealloc(m_imp);
-    {
+    m_imp = alloc(imp, m);    
-        dealloc(m_imp);
-        m_imp = alloc(imp, m);
-    }
 }
 
 void der_rewriter::reset() {

src/cmd_context/echo_tactic.cpp

@@ -29,12 +29,9 @@ public:
     
     void operator()(goal_ref const & in, 
                     goal_ref_buffer & result) override {
-        #pragma omp critical (echo_tactic)
+        m_ctx.regular_stream() << m_msg;
-        {
+        if (m_newline)
-            m_ctx.regular_stream() << m_msg;
+            m_ctx.regular_stream() << std::endl;
-            if (m_newline)
-                m_ctx.regular_stream() << std::endl;
-        }
         skip_tactic::operator()(in, result);
     }
 };
@@ -61,14 +58,11 @@ public:
     void operator()(goal_ref const & in, 
                     goal_ref_buffer & result) override {
         double val = (*m_p)(*(in.get())).get_value();
-        #pragma omp critical (probe_value_tactic)
+        if (m_msg)
-        {
+            m_ctx.diagnostic_stream() << m_msg << " ";
-            if (m_msg)
+        m_ctx.diagnostic_stream() << val;
-                m_ctx.diagnostic_stream() << m_msg << " ";
+        if (m_newline)
-            m_ctx.diagnostic_stream() << val;
+            m_ctx.diagnostic_stream() << std::endl;
-            if (m_newline)
-                m_ctx.diagnostic_stream() << std::endl;
-        }
         skip_tactic::operator()(in, result);
     }
 };

src/sat/sat_parallel.cpp

@@ -129,8 +129,8 @@ namespace sat {
     void parallel::exchange(solver& s, literal_vector const& in, unsigned& limit, literal_vector& out) {
         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);
-        #pragma omp critical (par_solver)
         {
+            std::lock_guard<std::mutex> 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,8 +150,8 @@ 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);
         IF_VERBOSE(3, verbose_stream() << s.m_par_id << ": share " <<  l1 << " " << l2 << "\n";);
-        #pragma omp critical (par_solver)
         {
+            std::lock_guard<std::mutex> 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());            
@@ -165,23 +165,19 @@ namespace sat {
         unsigned n = c.size();
         unsigned owner = s.m_par_id;
         IF_VERBOSE(3, verbose_stream() << owner << ": share " <<  c << "\n";);
-        #pragma omp critical (par_solver)
+        std::lock_guard<std::mutex> lock(m_mux);
-        {
+        m_pool.begin_add_vector(owner, n);                
-            m_pool.begin_add_vector(owner, n);                
+        for (unsigned i = 0; i < n; ++i) {
-            for (unsigned i = 0; i < n; ++i) {
+            m_pool.add_vector_elem(c[i].index());
-                m_pool.add_vector_elem(c[i].index());
-            }
-            m_pool.end_add_vector();
         }
+        m_pool.end_add_vector();        
     }
 
     void parallel::get_clauses(solver& s) {
         if (s.m_par_syncing_clauses) return;
         flet<bool> _disable_sync_clause(s.m_par_syncing_clauses, true);
-        #pragma omp critical (par_solver)
+        std::lock_guard<std::mutex> lock(m_mux);
-        {
+        _get_clauses(s);        
-            _get_clauses(s);
-        }
     }
 
     void parallel::_get_clauses(solver& s) {
@@ -241,17 +237,13 @@ namespace sat {
     }
 
     void parallel::set_phase(solver& s) {
-        #pragma omp critical (par_solver)
+        std::lock_guard<std::mutex> lock(m_mux);
-        {
+        _set_phase(s);        
-            _set_phase(s);
-        }
     }
 
     void parallel::get_phase(solver& s) {
-        #pragma omp critical (par_solver)
+        std::lock_guard<std::mutex> lock(m_mux);
-        {
+        _get_phase(s);        
-            _get_phase(s);
-        }
     }
 
     void parallel::_get_phase(solver& s) {
@@ -269,8 +261,8 @@ namespace sat {
 
     bool parallel::get_phase(local_search& s) {
         bool copied = false;
-        #pragma omp critical (par_solver)
         {
+            std::lock_guard<std::mutex> lock(m_mux);
             m_consumer_ready = true;
             if (m_solver_copy && s.num_non_binary_clauses() > m_solver_copy->m_clauses.size()) {
                 copied = true;
@@ -288,8 +280,8 @@ namespace sat {
 
     bool parallel::copy_solver(solver& s) {
         bool copied = false;
-        #pragma omp critical (par_solver)
         {
+            std::lock_guard<std::mutex> 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);

src/sat/sat_parallel.h

@@ -60,6 +60,7 @@ namespace sat {
         index_set      m_unit_set;
         literal_vector m_lits;
         vector_pool    m_pool;
+        std::mutex     m_mux;
 
         // for exchange with local search:
         svector<lbool>     m_phase;

src/sat/sat_solver.cpp

@@ -1731,18 +1731,6 @@ namespace sat {
         }
 
         if (m_par) m_par->set_phase(*this);
-
-#if 0
-        static unsigned file_no = 0;
-        #pragma omp critical (print_sat)
-        {
-            ++file_no;
-            std::ostringstream ostrm;
-            ostrm << "s" << file_no << ".txt";
-            std::ofstream ous(ostrm.str());
-            display(ous);
-        }
-#endif
     }
 
     bool solver::set_root(literal l, literal r) {

src/shell/lp_frontend.cpp

@@ -17,6 +17,8 @@ Author:
 #include "util/gparams.h"
 #include <signal.h>
 
+static std::mutex display_stats_mux;
+
 static lp::lp_solver<double, double>* g_solver = nullptr;
 
 static void display_statistics() {
@@ -27,19 +29,17 @@ static void display_statistics() {
 
 static void STD_CALL on_ctrl_c(int) {
     signal (SIGINT, SIG_DFL);
-    #pragma omp critical (g_display_stats)
     {
+        std::lock_guard<std::mutex> lock(display_stats_mux);
         display_statistics();
     }
     raise(SIGINT);
 }
 
 static void on_timeout() {
-    #pragma omp critical (g_display_stats)
+    std::lock_guard<std::mutex> lock(display_stats_mux);
-    {
+    display_statistics();
-        display_statistics();
+    exit(0);    
-        exit(0);
-    }
 }
 
 struct front_end_resource_limit : public lp::lp_resource_limit {
@@ -92,7 +92,6 @@ void run_solver(lp_params & params, char const * mps_file_name) {
         solver->print_model(std::cout);
     }
 
-//    #pragma omp critical (g_display_stats)
     {
         display_statistics();
         register_on_timeout_proc(nullptr);

src/shell/opt_frontend.cpp

@@ -25,6 +25,7 @@ static bool g_first_interrupt = true;
 static opt::context* g_opt = nullptr;
 static double g_start_time = 0;
 static unsigned_vector g_handles;
+static std::mutex display_stats_mux;
 
 
 
@@ -68,8 +69,8 @@ static void STD_CALL on_ctrl_c(int) {
     }
     else {
         signal (SIGINT, SIG_DFL);
-        #pragma omp critical (g_display_stats) 
         {
+            std::lock_guard<std::mutex> lock(display_stats_mux);
             display_statistics();
         }
         raise(SIGINT);
@@ -77,11 +78,11 @@ static void STD_CALL on_ctrl_c(int) {
 }
 
 static void on_timeout() {
-    #pragma omp critical (g_display_stats) 
     {
+        std::lock_guard<std::mutex> lock(display_stats_mux);
         display_statistics();
-        exit(0);
     }
+    exit(0);
 }
 
 static unsigned parse_opt(std::istream& in, opt_format f) {
@@ -131,8 +132,8 @@ static unsigned parse_opt(std::istream& in, opt_format f) {
     catch (z3_exception & ex) {
         std::cerr << ex.msg() << "\n";
     }
-    #pragma omp critical (g_display_stats) 
     {
+        std::lock_guard<std::mutex> lock(display_stats_mux);
         display_statistics();
         register_on_timeout_proc(nullptr);
         g_opt = nullptr;

src/shell/smtlib_frontend.cpp

@@ -32,6 +32,8 @@ Revision History:
 #include "tactic/portfolio/smt_strategic_solver.h"
 #include "smt/smt_solver.h"
 
+static std::mutex display_stats_mux;
+
 extern bool g_display_statistics;
 static clock_t             g_start_time;
 static cmd_context *       g_cmd_context = nullptr;
@@ -49,17 +51,15 @@ static void display_statistics() {
 }
 
 static void on_timeout() {
-    #pragma omp critical (g_display_stats)
+    std::lock_guard<std::mutex> lock(display_stats_mux);
-    {
+    display_statistics();
-        display_statistics();
+    exit(0);    
-        exit(0);
-    }
 }
 
 static void STD_CALL on_ctrl_c(int) {
     signal (SIGINT, SIG_DFL);
-    #pragma omp critical (g_display_stats)
     {
+        std::lock_guard<std::mutex> lock(display_stats_mux);
         display_statistics();
     }
     raise(SIGINT);
@@ -98,8 +98,8 @@ unsigned read_smtlib2_commands(char const * file_name) {
     }
 
 
-    #pragma omp critical (g_display_stats)
     {
+        std::lock_guard<std::mutex> lock(display_stats_mux);
         display_statistics();
         g_cmd_context = nullptr;
     }

src/smt/smt_kernel.cpp

@@ -295,11 +295,8 @@ namespace smt {
         ast_manager & _m = m();
         smt_params & fps = m_imp->fparams();
         params_ref ps    = m_imp->params();
-        #pragma omp critical (smt_kernel)
+        m_imp->~imp();
-        {
+        m_imp = new (m_imp) imp(_m, fps, ps);        
-            m_imp->~imp();
-            m_imp = new (m_imp) imp(_m, fps, ps);
-        }
     }
 
     bool kernel::inconsistent() {

src/solver/parallel_tactic.cpp

@@ -337,7 +337,7 @@ private:
 
     void init() {
         parallel_params pp(m_params);
-        m_num_threads = std::min((unsigned)omp_get_num_procs(), pp.threads_max());
+        m_num_threads = std::min((unsigned) std::thread::hardware_concurrency(), pp.threads_max());
         m_progress = 0;
         m_has_undef = false;
         m_allsat = false;

src/tactic/tactical.cpp

@@ -20,7 +20,6 @@ Notes:
 #include "util/cancel_eh.h"
 #include "util/cooperate.h"
 #include "util/scoped_ptr_vector.h"
-#include "util/z3_omp.h"
 #include "tactic/tactical.h"
 
 class binary_tactical : public tactic {
@@ -378,11 +377,7 @@ public:
 
     void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         bool use_seq;
-#ifdef _NO_OMP_
+        use_seq = false;
-        use_seq = true;
-#else
-        use_seq = 0 != omp_in_parallel();
-#endif
         if (use_seq) {
             // execute tasks sequentially
             or_else_tactical::operator()(in, result);
@@ -409,7 +404,8 @@ public:
         par_exception_kind ex_kind = DEFAULT_EX;
         std::string        ex_msg;
         unsigned           error_code = 0;
-        
+        std::mutex         mux;
+
         #pragma omp parallel for
         for (int i = 0; i < static_cast<int>(sz); i++) {
             goal_ref_buffer     _result;
@@ -420,8 +416,8 @@ public:
             try {
                 t(in_copy, _result);
                 bool first = false;
-                #pragma omp critical (par_tactical)
                 {
+                    std::lock_guard<std::mutex> lock(mux);
                     if (finished_id == UINT_MAX) {
                         finished_id = i;
                         first = true;
@@ -499,11 +495,7 @@ public:
 
     void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         bool use_seq;
-#ifdef _NO_OMP_
+        use_seq = false;
-        use_seq = true;
-#else
-        use_seq = 0 != omp_in_parallel();
-#endif
         if (use_seq) {
             // execute tasks sequentially
             and_then_tactical::operator()(in, result);
@@ -554,6 +546,7 @@ public:
             par_exception_kind ex_kind = DEFAULT_EX;
             unsigned error_code = 0;
             std::string  ex_msg;
+            std::mutex mux;
 
             #pragma omp parallel for
             for (int i = 0; i < static_cast<int>(r1_size); i++) { 
@@ -568,8 +561,8 @@ public:
                     ts2[i]->operator()(new_g, r2);                  
                 }
                 catch (tactic_exception & ex) {
-                    #pragma omp critical (par_and_then_tactical)
                     {
+                        std::lock_guard<std::mutex> lock(mux);
                         if (!failed && !found_solution) {
                             curr_failed = true;
                             failed      = true;
@@ -579,8 +572,8 @@ public:
                     }
                 }
                 catch (z3_error & err) {
-                    #pragma omp critical (par_and_then_tactical)
                     {
+                        std::lock_guard<std::mutex> lock(mux);
                         if (!failed && !found_solution) {
                             curr_failed = true;
                             failed      = true;
@@ -590,8 +583,8 @@ public:
                     }                    
                 }
                 catch (z3_exception & z3_ex) {
-                    #pragma omp critical (par_and_then_tactical)
                     {
+                        std::lock_guard<std::mutex> lock(mux);
                         if (!failed && !found_solution) {
                             curr_failed = true;
                             failed      = true;
@@ -614,8 +607,8 @@ public:
                         if (is_decided_sat(r2)) {                                                          
                             // found solution... 
                             bool first = false;
-                            #pragma omp critical (par_and_then_tactical)
                             {
+                                std::lock_guard<std::mutex> lock(mux);
                                 if (!found_solution) {
                                     failed         = false;
                                     found_solution = true;

src/util/cooperate.cpp

@@ -17,24 +17,20 @@ Notes:
 
 --*/
 
-#ifndef _NO_OMP_
 #include "util/cooperate.h"
 #include "util/trace.h"
 #include "util/debug.h"
-#include "util/z3_omp.h"
+#include <thread>
+#include <mutex>
 
 struct cooperation_lock {
-    omp_nest_lock_t  m_lock;
+    std::recursive_mutex m_lock;
     char const *     m_task;
-    volatile int     m_owner_thread;
+    std::thread::id   m_owner_thread;
     cooperation_lock() {
-        omp_set_nested(1);
-        omp_init_nest_lock(&m_lock);
         m_task = nullptr;
-        m_owner_thread = -1;
     }
     ~cooperation_lock() {
-        omp_destroy_nest_lock(&m_lock);
     }
 };
 
@@ -45,20 +41,18 @@ bool cooperation_ctx::g_cooperate = false;
 void cooperation_ctx::checkpoint(char const * task) {
     SASSERT(cooperation_ctx::enabled());
 
-    int  tid      = omp_get_thread_num();
+    std::thread::id tid = std::this_thread::get_id();
     if (g_lock.m_owner_thread == tid) {
-        g_lock.m_owner_thread = -1;
+        g_lock.m_owner_thread = std::thread::id();
-        omp_unset_nest_lock(&(g_lock.m_lock));
+        g_lock.m_lock.unlock();
     }
+
     // this critical section is used to force the owner thread to give a chance to
     // another thread to get the lock
-    #pragma omp critical (z3_cooperate) 
+    std::this_thread::yield();
-    {
+    g_lock.m_lock.lock();
-        omp_set_nest_lock(&(g_lock.m_lock));
+    TRACE("cooperate_detail", tout << task << ", tid: " << tid << "\n";);
-        TRACE("cooperate_detail", tout << task << ", tid: " << tid << "\n";);
+    CTRACE("cooperate", g_lock.m_task != task, tout << "moving to task: " << task << "\n";);
-        CTRACE("cooperate", g_lock.m_task != task, tout << "moving to task: " << task << "\n";);
+    g_lock.m_owner_thread = tid;    
-        g_lock.m_owner_thread = tid;
-    }
 }
 
-#endif

src/util/gparams.cpp

@@ -19,6 +19,9 @@ Notes:
 #include "util/gparams.h"
 #include "util/dictionary.h"
 #include "util/trace.h"
+#include <mutex>
+
+static std::mutex gparams_mux;
 
 extern void gparams_register_modules();
 
@@ -110,14 +113,12 @@ public:
     }
 
     void reset() {
-        #pragma omp critical (gparams)
+        std::lock_guard<std::mutex> lock(gparams_mux);
-        {
+        m_params.reset();
-            m_params.reset();
+        for (auto & kv : m_module_params) {
-            for (auto & kv : m_module_params) {
+            dealloc(kv.m_value);
-                dealloc(kv.m_value);
-            }
-            m_module_params.reset();
         }
+        m_module_params.reset();        
     }
 
     // -----------------------------------------------
@@ -327,8 +328,8 @@ public:
     void set(char const * name, char const * value) {
         bool error = false;
         std::string error_msg;
-        #pragma omp critical (gparams)
         {
+            std::lock_guard<std::mutex> lock(gparams_mux);
             try {
                 symbol m, p;
                 normalize(name, m, p);
@@ -379,8 +380,8 @@ public:
         std::string r;
         bool error = false;
         std::string error_msg;
-        #pragma omp critical (gparams)
         {
+            std::lock_guard<std::mutex> lock(gparams_mux);
             try {
                 symbol m, p;
                 normalize(name, m, p);
@@ -426,8 +427,8 @@ public:
     params_ref get_module(symbol const & module_name) {
         params_ref result;
         params_ref * ps = nullptr;
-        #pragma omp critical (gparams)
         {
+            std::lock_guard<std::mutex> lock(gparams_mux);
             if (m_module_params.find(module_name, ps)) {
                 result.copy(*ps);
             }
@@ -446,8 +447,8 @@ public:
     // -----------------------------------------------
 
     void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) {
-        #pragma omp critical (gparams)
         {
+            std::lock_guard<std::mutex> lock(gparams_mux);
             out << "Global parameters\n";
             get_param_descrs().display(out, indent + 4, smt2_style, include_descr);
             out << "\n";
@@ -469,44 +470,40 @@ public:
     }
 
     void display_modules(std::ostream & out) {
-        #pragma omp critical (gparams)
+        std::lock_guard<std::mutex> lock(gparams_mux);
-        {
+        for (auto & kv : get_module_param_descrs()) {
-            for (auto & kv : get_module_param_descrs()) {
+            out << "[module] " << kv.m_key;
-                out << "[module] " << kv.m_key;
+            char const * descr = nullptr;
-                char const * descr = nullptr;
+            if (get_module_descrs().find(kv.m_key, descr)) {
-                if (get_module_descrs().find(kv.m_key, descr)) {
+                out << ", description: " << descr;
-                    out << ", description: " << descr;
-                }
-                out << "\n";
             }
+            out << "\n";
         }
     }
 
     void display_module(std::ostream & out, symbol const & module_name) {
         bool error = false;
         std::string error_msg;
-        #pragma omp critical (gparams)
+        std::lock_guard<std::mutex> lock(gparams_mux);
-        {
+        try {
-            try {
+            param_descrs * d = nullptr;
-                param_descrs * d = nullptr;
+            if (!get_module_param_descrs().find(module_name, d)) {
-                if (!get_module_param_descrs().find(module_name, d)) {
+                std::stringstream strm;
-                    std::stringstream strm;
+                strm << "unknown module '" << module_name << "'";                    
-                    strm << "unknown module '" << module_name << "'";                    
+                throw exception(strm.str());
-                    throw exception(strm.str());
-                }
-                out << "[module] " << module_name;
-                char const * descr = nullptr;
-                if (get_module_descrs().find(module_name, descr)) {
-                    out << ", description: " << descr;
-                }
-                out << "\n";
-                d->display(out, 4, false);
             }
-            catch (z3_exception & ex) {
+            out << "[module] " << module_name;
-                // Exception cannot cross critical section boundaries.
+            char const * descr = nullptr;
-                error = true;
+            if (get_module_descrs().find(module_name, descr)) {
-                error_msg = ex.msg();
+                out << ", description: " << descr;
             }
+            out << "\n";
+            d->display(out, 4, false);
+        }
+        catch (z3_exception & ex) {
+            // Exception cannot cross critical section boundaries.
+            error = true;
+            error_msg = ex.msg();
         }
         if (error)
             throw exception(std::move(error_msg));
@@ -515,8 +512,8 @@ public:
     void display_parameter(std::ostream & out, char const * name) {
         bool error = false;
         std::string error_msg;
-        #pragma omp critical (gparams)
         {
+            std::lock_guard<std::mutex> lock(gparams_mux);
             try {
                 symbol m, p;
                 normalize(name, m, p);

src/util/memory_manager.cpp

@@ -7,10 +7,10 @@ Copyright (c) 2015 Microsoft Corporation
 #include<iostream>
 #include<stdlib.h>
 #include<climits>
+#include<mutex>
 #include "util/trace.h"
 #include "util/memory_manager.h"
 #include "util/error_codes.h"
-#include "util/z3_omp.h"
 #include "util/debug.h"
 // The following two function are automatically generated by the mk_make.py script.
 // The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files.
@@ -35,6 +35,7 @@ out_of_memory_error::out_of_memory_error():z3_error(ERR_MEMOUT) {
 }
 
 
+static std::mutex g_memory_mux;
 static volatile bool g_memory_out_of_memory  = false;
 static bool       g_memory_initialized       = false;
 static long long  g_memory_alloc_size        = 0;
@@ -54,8 +55,8 @@ void memory::exit_when_out_of_memory(bool flag, char const * msg) {
 }
 
 static void throw_out_of_memory() {
-    #pragma omp critical (z3_memory_manager) 
     {
+        std::lock_guard<std::mutex> lock(g_memory_mux);
         g_memory_out_of_memory = true;
     }
 
@@ -90,8 +91,8 @@ mem_usage_report g_info;
 
 void memory::initialize(size_t max_size) {
     bool initialize = false;
-    #pragma omp critical (z3_memory_manager)
     {
+        std::lock_guard<std::mutex> lock(g_memory_mux);
         // only update the maximum size if max_size != UINT_MAX
         if (max_size != UINT_MAX) 
             g_memory_max_size       = max_size;
@@ -116,8 +117,8 @@ void memory::initialize(size_t max_size) {
 
 bool memory::is_out_of_memory() {
     bool r = false;
-    #pragma omp critical (z3_memory_manager) 
     {
+        std::lock_guard<std::mutex> lock(g_memory_mux);
         r = g_memory_out_of_memory;
     }
     return r;
@@ -131,12 +132,8 @@ void memory::set_high_watermark(size_t watermark) {
 bool memory::above_high_watermark() {
     if (g_memory_watermark == 0)
         return false;
-    bool r;
+    std::lock_guard<std::mutex> lock(g_memory_mux);
-    #pragma omp critical (z3_memory_manager) 
+    return g_memory_watermark < g_memory_alloc_size;
-    {
-        r = g_memory_watermark < g_memory_alloc_size;
-    }
-    return r;
 }
 
 // The following methods are only safe to invoke at 
@@ -163,8 +160,8 @@ void memory::finalize() {
 
 unsigned long long memory::get_allocation_size() {
     long long r;
-    #pragma omp critical (z3_memory_manager) 
     {
+        std::lock_guard<std::mutex> lock(g_memory_mux);
         r = g_memory_alloc_size;
     }
     if (r < 0)
@@ -174,8 +171,8 @@ unsigned long long memory::get_allocation_size() {
 
 unsigned long long memory::get_max_used_memory() {
     unsigned long long r;
-    #pragma omp critical (z3_memory_manager) 
     {
+        std::lock_guard<std::mutex> lock(g_memory_mux);
         r = g_memory_max_used_size;
     }
     return r;
@@ -258,8 +255,8 @@ static void synchronize_counters(bool allocating) {
 
     bool out_of_mem = false;
     bool counts_exceeded = false;
-    #pragma omp critical (z3_memory_manager) 
     {
+        std::lock_guard<std::mutex> lock(g_memory_mux);
         g_memory_alloc_size += g_memory_thread_alloc_size;
         g_memory_alloc_count += g_memory_thread_alloc_count;
         if (g_memory_alloc_size > g_memory_max_used_size)
@@ -339,8 +336,8 @@ void memory::deallocate(void * p) {
     size_t * sz_p  = reinterpret_cast<size_t*>(p) - 1;
     size_t sz      = *sz_p;
     void * real_p  = reinterpret_cast<void*>(sz_p);
-    #pragma omp critical (z3_memory_manager) 
     {
+        std::lock_guard<std::mutex> lock(g_memory_mux);
         g_memory_alloc_size -= sz;
     }
     free(real_p);
@@ -349,8 +346,8 @@ void memory::deallocate(void * p) {
 void * memory::allocate(size_t s) {
     s = s + sizeof(size_t); // we allocate an extra field!
     bool out_of_mem = false, counts_exceeded = false;
-    #pragma omp critical (z3_memory_manager) 
     {
+        std::lock_guard<std::mutex> lock(g_memory_mux);
         g_memory_alloc_size += s;
         g_memory_alloc_count += 1;
         if (g_memory_alloc_size > g_memory_max_used_size)
@@ -379,8 +376,8 @@ void* memory::reallocate(void *p, size_t s) {
     void * real_p  = reinterpret_cast<void*>(sz_p);
     s = s + sizeof(size_t); // we allocate an extra field!
     bool out_of_mem = false, counts_exceeded = false;
-    #pragma omp critical (z3_memory_manager)
     {
+        std::lock_guard<std::mutex> lock(g_memory_mux);
         g_memory_alloc_size += s - sz;
         g_memory_alloc_count += 1;
         if (g_memory_alloc_size > g_memory_max_used_size)

src/util/mpn.cpp

@@ -29,11 +29,9 @@ static_assert(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit), "size alignment
 const mpn_digit mpn_manager::zero = 0;
 
 mpn_manager::mpn_manager() {
-    omp_init_nest_lock(&m_lock);
 }
 
 mpn_manager::~mpn_manager() {
-    omp_destroy_nest_lock(&m_lock);
 }
 
 int mpn_manager::compare(mpn_digit const * a, size_t const lnga, 

src/util/mpn.h

@@ -20,18 +20,16 @@ Revision History:
 #define MPN_H_
 
 #include<ostream>
+#include<mutex>
 #include "util/util.h"
 #include "util/buffer.h"
-#include "util/z3_omp.h"
 
 typedef unsigned int mpn_digit;
 
 class mpn_manager {
-#ifndef _NO_OMP_
+    std::recursive_mutex m_lock;
-    omp_nest_lock_t m_lock;
+#define MPN_BEGIN_CRITICAL() m_lock.lock();
-#endif
+#define MPN_END_CRITICAL() m_lock.unlock();
-#define MPN_BEGIN_CRITICAL() omp_set_nest_lock(&m_lock);
-#define MPN_END_CRITICAL() omp_unset_nest_lock(&m_lock);
 
 public:
     mpn_manager();

src/util/mpz.cpp

@@ -139,8 +139,6 @@ uint64_t u64_gcd(uint64_t u, uint64_t v) {
 template<bool SYNCH>
 mpz_manager<SYNCH>::mpz_manager():
     m_allocator("mpz_manager") {
-    if (SYNCH)
-        omp_init_nest_lock(&m_lock);
 #ifndef _MP_GMP
     if (sizeof(digit_t) == sizeof(uint64_t)) {
         // 64-bit machine
@@ -197,8 +195,6 @@ mpz_manager<SYNCH>::~mpz_manager() {
     mpz_clear(m_int64_max);
     mpz_clear(m_int64_min);
 #endif
-    if (SYNCH)
-        omp_destroy_nest_lock(&m_lock);
 }
 
 #ifndef _MP_GMP

src/util/mpz.h

@@ -20,12 +20,12 @@ Revision History:
 #define MPZ_H_
 
 #include<string>
+#include<mutex>
 #include "util/util.h"
 #include "util/small_object_allocator.h"
 #include "util/trace.h"
 #include "util/scoped_numeral.h"
 #include "util/scoped_numeral_vector.h"
-#include "util/z3_omp.h"
 #include "util/mpn.h"
 
 unsigned u_gcd(unsigned u, unsigned v);
@@ -135,9 +135,9 @@ inline void swap(mpz & m1, mpz & m2) { m1.swap(m2); }
 template<bool SYNCH = true>
 class mpz_manager {
     mutable small_object_allocator  m_allocator;
-    mutable omp_nest_lock_t         m_lock;
+    mutable std::recursive_mutex         m_lock;
-#define MPZ_BEGIN_CRITICAL() if (SYNCH) omp_set_nest_lock(&m_lock);
+#define MPZ_BEGIN_CRITICAL() if (SYNCH) m_lock.lock();
-#define MPZ_END_CRITICAL()   if (SYNCH) omp_unset_nest_lock(&m_lock);
+#define MPZ_END_CRITICAL()   if (SYNCH) m_lock.unlock();
     mutable mpn_manager             m_mpn_manager;
 
 #ifndef _MP_GMP
@@ -702,11 +702,7 @@ public:
     bool decompose(mpz const & n, svector<digit_t> & digits);
 };
 
-#ifndef _NO_OMP_
 typedef mpz_manager<true> synch_mpz_manager;
-#else
-typedef mpz_manager<false> synch_mpz_manager;
-#endif
 typedef mpz_manager<false> unsynch_mpz_manager;
 
 typedef _scoped_numeral<unsynch_mpz_manager> scoped_mpz;

src/util/prime_generator.cpp

@@ -17,6 +17,7 @@ Notes:
 
 --*/
 #include "util/prime_generator.h"
+#include <mutex>
 
 #define PRIME_LIST_MAX_SIZE 1<<20
 
@@ -109,6 +110,8 @@ prime_iterator::prime_iterator(prime_generator * g):m_idx(0) {
     }
 }
 
+static std::mutex g_prime_iterator;
+
 uint64_t prime_iterator::next() {
     unsigned idx = m_idx;
     m_idx++;
@@ -117,7 +120,7 @@ uint64_t prime_iterator::next() {
     }
     else {
         uint64_t r;
-        #pragma omp critical (prime_iterator)
+        std::lock_guard<std::mutex> lock(g_prime_iterator);
         {
             r = (*m_generator)(idx);
         }

src/util/rational.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include<sstream>
+#include<mutex>
 #include "util/util.h"
 #include "util/rational.h"
 #ifdef _WINDOWS
@@ -42,9 +43,11 @@ static void mk_power_up_to(vector<rational> & pws, unsigned n) {
     }
 }
 
+static std::mutex g_powers_of_two;
+
 rational rational::power_of_two(unsigned k) {
     rational result;
-    #pragma omp critical (powers_of_two)
+    std::lock_guard<std::mutex> lock(g_powers_of_two);
     {
         if (k >= m_powers_of_two.size())
             mk_power_up_to(m_powers_of_two, k+1);

src/util/rlimit.cpp

@@ -18,6 +18,10 @@ Revision History:
 --*/
 #include "util/rlimit.h"
 #include "util/common_msgs.h"
+#include <mutex>
+
+static std::mutex g_reslimit_cancel;
+
 
 reslimit::reslimit():
     m_cancel(0),
@@ -69,48 +73,36 @@ char const* reslimit::get_cancel_msg() const {
 }
 
 void reslimit::push_child(reslimit* r) {
-    #pragma omp critical (reslimit_cancel)
+    std::lock_guard<std::mutex> lock(g_reslimit_cancel);
-    {
+    m_children.push_back(r);    
-        m_children.push_back(r);
-    }
 }
 
 void reslimit::pop_child() {
-    #pragma omp critical (reslimit_cancel)
+    std::lock_guard<std::mutex> lock(g_reslimit_cancel);
-    {
+    m_children.pop_back();    
-        m_children.pop_back();
-    }
 }
 
 void reslimit::cancel() {
-    #pragma omp critical (reslimit_cancel)
+    std::lock_guard<std::mutex> lock(g_reslimit_cancel);
-    {
+    set_cancel(m_cancel+1);    
-        set_cancel(m_cancel+1);
-    }
 }
 
 
 void reslimit::reset_cancel() {
-    #pragma omp critical (reslimit_cancel)
+    std::lock_guard<std::mutex> lock(g_reslimit_cancel);
-    {
+    set_cancel(0);    
-        set_cancel(0);
-    }
 }
 
 void reslimit::inc_cancel() {
-    #pragma omp critical (reslimit_cancel)
+    std::lock_guard<std::mutex> lock(g_reslimit_cancel);
-    {
+    set_cancel(m_cancel+1);    
-        set_cancel(m_cancel+1);
-    }
 }
 
 
 void reslimit::dec_cancel() {
-    #pragma omp critical (reslimit_cancel)
+    std::lock_guard<std::mutex> lock(g_reslimit_cancel);
-    {
+    if (m_cancel > 0) {
-        if (m_cancel > 0) {
+        set_cancel(m_cancel-1);
-            set_cancel(m_cancel-1);
-        }
     }
 }
 

src/util/symbol.cpp

@@ -20,8 +20,10 @@ Revision History:
 #include "util/str_hashtable.h"
 #include "util/region.h"
 #include "util/string_buffer.h"
-#include "util/z3_omp.h"
 #include <cstring>
+#include <mutex>
+
+static std::mutex g_symbol_lock;
 
 symbol symbol::m_dummy(TAG(void*, nullptr, 2));
 const symbol symbol::null;
@@ -36,8 +38,7 @@ public:
 
     char const * get_str(char const * d) {
         const char * result;
-        #pragma omp critical (cr_symbol) 
+        std::lock_guard<std::mutex> lock(g_symbol_lock);
-        {
         str_hashtable::entry * e;
         if (m_table.insert_if_not_there_core(d, e)) {
             // new entry
@@ -55,7 +56,6 @@ public:
             result = e->get_data();
         }
         SASSERT(m_table.contains(result));
-        }
         return result;
     }
 };

src/util/util.cpp

@@ -23,6 +23,10 @@ Revision History:
 #include <thread>
 #include "util/util.h"
 
+static std::mutex g_verbose_mux;
+void verbose_lock() { g_verbose_mux.lock(); }
+void verbose_unlock() { g_verbose_mux.unlock(); }
+
 static unsigned g_verbosity_level = 0;
 
 void set_verbosity_level(unsigned lvl) {

src/util/util.h

@@ -21,10 +21,10 @@ Revision History:
 
 #include "util/debug.h"
 #include "util/memory_manager.h"
-#include "util/z3_omp.h"
 #include<iostream>
 #include<climits>
 #include<limits>
+#include<mutex>
 #include<stdint.h>
 
 #ifndef SIZE_MAX
@@ -174,11 +174,8 @@ void set_verbosity_level(unsigned lvl);
 unsigned get_verbosity_level();
 std::ostream& verbose_stream();
 void set_verbose_stream(std::ostream& str);
-#ifdef _NO_OMP_
-# define is_threaded() false
-#else
 bool is_threaded();
-#endif
+
 
   
 #define IF_VERBOSE(LVL, CODE) {                                 \
@@ -191,25 +188,16 @@ bool is_threaded();
         }                                                       \
     } } ((void) 0)              
 
-#ifdef _MSC_VER
-#define DO_PRAGMA(x) __pragma(x)
-#define PRAGMA_LOCK __pragma(omp critical (verbose_lock))
-#else
-#define DO_PRAGMA(x) _Pragma(#x)
-#define PRAGMA_LOCK _Pragma("omp critical (verbose_lock)")
-#endif
 
-#ifdef _NO_OMP_
+void verbose_lock();
-#define LOCK_CODE(CODE) CODE;
+void verbose_unlock();
-#else
+
-#define LOCK_CODE(CODE)                         \
+#define LOCK_CODE(CODE)                                         \
-    {                                           \
+    {                                                           \
-        PRAGMA_LOCK   \
+        verbose_lock();                                         \
-            {                                   \
+        CODE;                                                   \
-                CODE;                           \
+        verbose_unlock();                                       \
-            }                                   \
+    }                                                           \
-    }                      
-#endif
 
 template<typename T>
 struct default_eq {

src/util/z3_omp.h

@@ -1,38 +0,0 @@
-/*++
-Copyright (c) 2012 Microsoft Corporation
-
-Module Name:
-
-    z3_omp.h
-
-Abstract:
-
-    Wrapper for OMP functions and data-structures
-
-Author:
-
-    Leonardo (leonardo) 2012-01-05
-
-Notes:
-
---*/
-#ifndef Z3_OMP_H_
-#define Z3_OMP_H_
-
-#ifndef _NO_OMP_
-#include<omp.h>
-#else
-#define omp_in_parallel() false
-#define omp_set_num_threads(SZ) ((void)0)
-#define omp_get_thread_num() 0
-#define omp_get_num_procs()  1
-#define omp_set_nested(V) ((void)0)
-#define omp_init_nest_lock(L) ((void) 0)
-#define omp_destroy_nest_lock(L) ((void) 0)
-#define omp_set_nest_lock(L) ((void) 0)
-#define omp_unset_nest_lock(L) ((void) 0)
-struct omp_nest_lock_t {
-};
-#endif
-
-#endif