pfor

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

src/sat/sat_parallel.cpp

@@ -104,7 +104,7 @@ namespace sat {
         m_solvers.resize(num_extra_solvers);
         symbol saved_phase = s.m_params.get_sym("phase", symbol("caching"));
         for (unsigned i = 0; i < num_extra_solvers; ++i) {        
-            m_limits.push_back(reslimit());
+            m_limits.push_back(alloc(reslimit));
         }
         
         for (unsigned i = 0; i < num_extra_solvers; ++i) {
@@ -112,7 +112,7 @@ namespace sat {
             if (i == 1 + num_threads/2) {
                 s.m_params.set_sym("phase", symbol("random"));
             }                        
-            m_solvers[i] = alloc(sat::solver, s.m_params, m_limits[i]);
+            m_solvers[i] = alloc(sat::solver, s.m_params, *m_limits[i]);
             m_solvers[i]->copy(s, true);
             m_solvers[i]->set_par(this, i);
             push_child(m_solvers[i]->rlimit());            

src/sat/sat_parallel.h

@@ -23,6 +23,7 @@ Revision History:
 #include "util/hashtable.h"
 #include "util/map.h"
 #include "util/rlimit.h"
+#include "util/scoped_ptr_vector.h"
 
 namespace sat {
 
@@ -69,7 +70,7 @@ namespace sat {
         bool               m_consumer_ready;
 
         scoped_limits      m_scoped_rlimit;
-        vector<reslimit>   m_limits;
+        scoped_ptr_vector<reslimit> m_limits;
         ptr_vector<solver> m_solvers;
         
     public:
@@ -87,7 +88,7 @@ namespace sat {
 
         solver& get_solver(unsigned i) { return *m_solvers[i]; }
 
-        void cancel_solver(unsigned i) { m_limits[i].cancel(); }
+        void cancel_solver(unsigned i) { m_limits[i]->cancel(); }
 
         // exchange unit literals
         void exchange(solver& s, literal_vector const& in, unsigned& limit, literal_vector& out);

src/sat/sat_solver.cpp

@@ -1243,8 +1243,7 @@ namespace sat {
         unsigned error_code = 0;
         lbool result = l_undef;
         bool canceled = false;
-        #pragma omp parallel for
+        auto worker_thread = [&](int i) {
-        for (int i = 0; i < num_threads; ++i) {
             try {
                 lbool r = l_undef;
                 if (IS_AUX_SOLVER(i)) {
@@ -1296,6 +1295,14 @@ namespace sat {
                 ex_msg = ex.msg();
                 ex_kind = DEFAULT_EX;    
             }
+        };
+
+        vector<std::thread> threads;
+        for (int i = 0; i < num_threads; ++i) {
+            threads.push_back(std::thread([&]() { worker_thread(i); }));
+        }
+        for (int i = 0; i < num_threads; ++i) {
+            threads[i].join();
         }
         
         if (IS_AUX_SOLVER(finished_id)) {

src/util/rlimit.cpp

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

src/util/rlimit.h

@@ -19,6 +19,7 @@ Revision History:
 #ifndef RLIMIT_H_
 #define RLIMIT_H_
 
+#include <mutex>
 #include "util/vector.h"
 
 class reslimit {
@@ -28,12 +29,14 @@ class reslimit {
     uint64_t        m_limit;
     svector<uint64_t> m_limits;
     ptr_vector<reslimit> m_children;
+    std::mutex        m_mux;
 
     void set_cancel(unsigned f);
     friend class scoped_suspend_rlimit;
 
 public:
     reslimit();
+    ~reslimit() {}
     void push(unsigned delta_limit);
     void pop();
     void push_child(reslimit* r);