adding threads to smt core

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

src/smt/CMakeLists.txt

@@ -37,6 +37,7 @@ z3_add_component(smt
     smt_model_checker.cpp
     smt_model_finder.cpp
     smt_model_generator.cpp
+    smt_parallel.cpp
     smt_quantifier.cpp
     smt_quantifier_stat.cpp
     smt_quick_checker.cpp

src/smt/params/smt_params.cpp

@@ -38,6 +38,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
     m_max_conflicts = p.max_conflicts();
     m_restart_max   = p.restart_max();
+    m_threads       = p.threads();
     m_core_validate = p.core_validate();
     m_logic = _p.get_sym("logic", m_logic);
     m_string_solver = p.string_solver();
@@ -98,6 +99,7 @@ void smt_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_phase_caching_off);
     DISPLAY_PARAM(m_minimize_lemmas);
     DISPLAY_PARAM(m_max_conflicts);
+    DISPLAY_PARAM(m_threads);
     DISPLAY_PARAM(m_simplify_clauses);
     DISPLAY_PARAM(m_tick);
     DISPLAY_PARAM(m_display_features);

src/smt/params/smt_params.h

@@ -103,6 +103,7 @@ struct smt_params : public preprocessor_params,
     bool             m_minimize_lemmas;
     unsigned         m_max_conflicts;
     unsigned         m_restart_max;
+    unsigned         m_threads;
     bool             m_simplify_clauses;
     unsigned         m_tick;
     bool             m_display_features;
@@ -253,6 +254,7 @@ struct smt_params : public preprocessor_params,
         m_phase_caching_off(100),
         m_minimize_lemmas(true),
         m_max_conflicts(UINT_MAX),
+        m_threads(1),
         m_simplify_clauses(true),
         m_tick(1000),
         m_display_features(false),

src/smt/params/smt_params_helper.pyg

@@ -20,6 +20,7 @@ def_module_params(module_name='smt',
                           ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'),
                           ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'),
                           ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
+                          ('threads', UINT, 1, 'maximal number of parallel threads.'),
                           ('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
                           ('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),
                           ('mbqi.max_cexs_incr', UINT, 0, 'increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI'),

src/smt/smt_context.cpp

@@ -38,6 +38,7 @@ Revision History:
 #include "smt/smt_model_generator.h"
 #include "smt/smt_model_checker.h"
 #include "smt/smt_model_finder.h"
+#include "smt/smt_parallel.h"
 
 namespace smt {
 
@@ -63,6 +64,8 @@ namespace smt {
         m_e_internalized_stack(m),
         m_final_check_idx(0),
         m_is_auxiliary(false),
+        m_par(nullptr),
+        m_par_index(0),
         m_cg_table(m),
         m_is_diseq_tmp(nullptr),
         m_units_to_reassert(m),
@@ -3376,6 +3379,11 @@ namespace smt {
         SASSERT(!m_setup.already_configured());
         setup_context(m_fparams.m_auto_config);
 
+        if (m_fparams.m_threads > 1) {
+            parallel p(*this);
+            expr_ref_vector asms(m);
+            return p(asms);
+        }
 
         internalize_assertions();
         expr_ref_vector theory_assumptions(m);
@@ -3432,10 +3440,14 @@ namespace smt {
         if (!check_preamble(reset_cancel)) return l_undef;
         SASSERT(at_base_level());
         setup_context(false);
+        expr_ref_vector asms(m, num_assumptions, assumptions);
+        if (m_fparams.m_threads > 1) {            
+            parallel p(*this);
+            return p(asms);
+        }
         lbool r;
         do {
             pop_to_base_lvl();
-            expr_ref_vector asms(m, num_assumptions, assumptions);
             internalize_assertions();
             add_theory_assumptions(asms);                
             TRACE("unsat_core_bug", tout << asms << "\n";);        

src/smt/smt_context.h

@@ -69,6 +69,7 @@ namespace smt {
     class context {
         friend class model_generator;
         friend class lookahead;
+        friend class parallel;
     public:
         statistics                  m_stats;
 
@@ -82,6 +83,7 @@ namespace smt {
         ast_manager &               m;
         smt_params &                m_fparams;
         params_ref                  m_params;
+        ::statistics                m_aux_stats;
         setup                       m_setup;
         unsigned                    m_relevancy_lvl;
         timer                       m_timer;
@@ -110,6 +112,8 @@ namespace smt {
         unsigned                    m_final_check_idx; // circular counter used for implementing fairness
 
         bool                        m_is_auxiliary; // used to prevent unwanted information from being logged.
+        parallel*                   m_par;
+        unsigned                    m_par_index;
 
         // -----------------------------------
         //
@@ -409,13 +413,14 @@ namespace smt {
             return js.get_kind() == b_justification::JUSTIFICATION && js.get_justification()->get_from_theory() == th_id;
         }
 
-        int get_random_value() {
-            return m_random();
-        }
 
-        bool is_searching() const {
+        void set_par(unsigned idx, parallel* p) { m_par = p; m_par_index = idx; }
-            return m_searching;
+
-        }
+        void set_random_seed(unsigned s) { m_random.set_seed(s); }
+
+        int get_random_value() { return m_random(); }
+
+        bool is_searching() const { return m_searching; }
 
         svector<double> const & get_activity_vector() const {
             return m_activity;

src/smt/smt_context_pp.cpp

@@ -377,6 +377,7 @@ namespace smt {
     }
 
     void context::collect_statistics(::statistics & st) const {
+        st.copy(m_aux_stats);
         st.update("conflicts", m_stats.m_num_conflicts);
         st.update("decisions", m_stats.m_num_decisions);
         st.update("propagations", m_stats.m_num_propagations + m_stats.m_num_bin_propagations);

src/util/mpn.cpp

@@ -151,7 +151,6 @@ bool mpn_manager::div(mpn_digit const * numer, size_t const lnum,
                       mpn_digit const * denom, size_t const lden,
                       mpn_digit * quot,
                       mpn_digit * rem) {
-    MPN_BEGIN_CRITICAL();
     trace(numer, lnum, denom, lden, "/");
     bool res = false;    
 
@@ -160,7 +159,6 @@ bool mpn_manager::div(mpn_digit const * numer, size_t const lnum,
             quot[i] = 0;
         for (size_t i = 0; i < lden; i++)
             rem[i] = (i < lnum) ? numer[i] : 0;
-        MPN_END_CRITICAL();
         return false;
     }
 
@@ -170,7 +168,6 @@ bool mpn_manager::div(mpn_digit const * numer, size_t const lnum,
 
     if (all_zero) {
         UNREACHABLE();
-        MPN_END_CRITICAL();
         return res;
     }
 
@@ -186,6 +183,7 @@ bool mpn_manager::div(mpn_digit const * numer, size_t const lnum,
             rem[i] = (i < lnum) ? numer[i] : 0;       
     }        
     else  {
+        mpn_sbuffer u, v, t_ms, t_ab;
         size_t d = div_normalize(numer, lnum, denom, lden, u, v);
         if (lden == 1)
             res = div_1(u, v[0], quot);
@@ -214,7 +212,6 @@ bool mpn_manager::div(mpn_digit const * numer, size_t const lnum,
     SASSERT(ok);
 #endif
 
-    MPN_END_CRITICAL();
     return res;
 }
 

src/util/mpn.h

@@ -90,7 +90,7 @@ private:
     #endif
 
     static const mpn_digit zero;
-    mpn_sbuffer u, v, t_ms, t_ab;
+//    mpn_sbuffer u, v, t_ms, t_ab;
     void display_raw(std::ostream & out, mpn_digit const * a, size_t lng) const;
 
     size_t div_normalize(mpn_digit const * numer, size_t lnum,

src/util/mpz.cpp

@@ -187,9 +187,16 @@ mpz_manager<SYNCH>::~mpz_manager() {
 template<bool SYNCH>
 mpz_cell * mpz_manager<SYNCH>::allocate(unsigned capacity) {
     SASSERT(capacity >= m_init_cell_capacity);
-    MPZ_BEGIN_CRITICAL();
+#ifdef SINGLE_THREAD
     mpz_cell * cell = reinterpret_cast<mpz_cell*>(m_allocator.allocate(cell_size(capacity)));
-    MPZ_END_CRITICAL();
+#else
+#if SYNC
+    mpz_cell * cell = reinterpret_cast<mpz_cell*>(m_allocator.allocate(cell_size(capacity)));
+#else
+    mpz_cell * cell = reinterpret_cast<mpz_cell*>(memory::allocate(cell_size(capacity)));
+    
+#endif
+#endif
     cell->m_capacity = capacity;
     return cell;
 }
@@ -197,9 +204,15 @@ mpz_cell * mpz_manager<SYNCH>::allocate(unsigned capacity) {
 template<bool SYNCH>
 void mpz_manager<SYNCH>::deallocate(bool is_heap, mpz_cell * ptr) { 
     if (is_heap) {
-        MPZ_BEGIN_CRITICAL();
+#ifdef SINGLE_THREAD
         m_allocator.deallocate(cell_size(ptr->m_capacity), ptr); 
-        MPZ_END_CRITICAL();
+#else
+#if SYNC
+        m_allocator.deallocate(cell_size(ptr->m_capacity), ptr);        
+#else
+        memory::deallocate(ptr);
+#endif
+#endif
     }
 }
 

src/util/mpz.h

@@ -196,9 +196,15 @@ class mpz_manager {
     mutable mpz_t     m_int64_min;
 
     mpz_t * allocate() {        
-        MPZ_BEGIN_CRITICAL();
+#ifdef SINGLE_THREAD
         mpz_t * cell = reinterpret_cast<mpz_t*>(m_allocator.allocate(sizeof(mpz_t)));        
-        MPZ_END_CRITICAL();
+#else
+#if SYNC
+        mpz_t * cell = reinterpret_cast<mpz_t*>(memory::allocate(sizeof(mpz_t)));
+#else
+        mpz_t * cell = reinterpret_cast<mpz_t*>(m_allocator.allocate(sizeof(mpz_t)));        
+#endif
+#endif
         mpz_init(*cell);
         return cell;
     }
@@ -206,9 +212,15 @@ class mpz_manager {
     void deallocate(bool is_heap, mpz_t * ptr) { 
         mpz_clear(*ptr); 
         if (is_heap) {
-            MPZ_BEGIN_CRITICAL();
+#ifdef SINGLE_THREAD
             m_allocator.deallocate(sizeof(mpz_t), ptr); 
-            MPZ_END_CRITICAL();
+#else
+#if SYNC
+            memory::deallocate(ptr);
+#else
+            m_allocator.deallocate(sizeof(mpz_t), ptr); 
+#endif
+#endif
         }
     }