From 5f2720562bbf22e1c99bf0d6fedbfcf5fc06eb20 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 31 Jan 2020 17:04:03 -0800 Subject: [PATCH] adding threads to smt core Signed-off-by: Nikolaj Bjorner --- src/smt/CMakeLists.txt | 1 + src/smt/params/smt_params.cpp | 2 ++ src/smt/params/smt_params.h | 2 ++ src/smt/params/smt_params_helper.pyg | 1 + src/smt/smt_context.cpp | 14 +++++++++++++- src/smt/smt_context.h | 17 +++++++++++------ src/smt/smt_context_pp.cpp | 1 + src/util/mpn.cpp | 5 +---- src/util/mpn.h | 2 +- src/util/mpz.cpp | 23 ++++++++++++++++++----- src/util/mpz.h | 22 +++++++++++++++++----- 11 files changed, 68 insertions(+), 22 deletions(-) diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index 778890cb7..e08b55e30 100644 --- a/src/smt/CMakeLists.txt +++ b/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 diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index f89830aee..ed2e13749 100644 --- a/src/smt/params/smt_params.cpp +++ b/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); diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 0acbf164a..c2fca2c10 100644 --- a/src/smt/params/smt_params.h +++ b/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), diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 27b348042..afc1f61e2 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/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'), diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index f9a6e59f0..6bb8c1c50 100644 --- a/src/smt/smt_context.cpp +++ b/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";); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 0b78bc887..b2826e2de 100644 --- a/src/smt/smt_context.h +++ b/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 { - return m_searching; - } + void set_par(unsigned idx, parallel* p) { m_par = p; m_par_index = idx; } + + 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 const & get_activity_vector() const { return m_activity; diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 6c7b6f905..aaa249b2a 100644 --- a/src/smt/smt_context_pp.cpp +++ b/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); diff --git a/src/util/mpn.cpp b/src/util/mpn.cpp index 7142fbad1..d0615f31d 100644 --- a/src/util/mpn.cpp +++ b/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; } diff --git a/src/util/mpn.h b/src/util/mpn.h index f871adda1..10e3476b2 100644 --- a/src/util/mpn.h +++ b/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, diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 729c5af0e..a66add988 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -187,9 +187,16 @@ mpz_manager::~mpz_manager() { template mpz_cell * mpz_manager::allocate(unsigned capacity) { SASSERT(capacity >= m_init_cell_capacity); - MPZ_BEGIN_CRITICAL(); - mpz_cell * cell = reinterpret_cast(m_allocator.allocate(cell_size(capacity))); - MPZ_END_CRITICAL(); +#ifdef SINGLE_THREAD + mpz_cell * cell = reinterpret_cast(m_allocator.allocate(cell_size(capacity))); +#else +#if SYNC + mpz_cell * cell = reinterpret_cast(m_allocator.allocate(cell_size(capacity))); +#else + mpz_cell * cell = reinterpret_cast(memory::allocate(cell_size(capacity))); + +#endif +#endif cell->m_capacity = capacity; return cell; } @@ -197,9 +204,15 @@ mpz_cell * mpz_manager::allocate(unsigned capacity) { template void mpz_manager::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 } } diff --git a/src/util/mpz.h b/src/util/mpz.h index 4c927b206..1ce325174 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -196,9 +196,15 @@ class mpz_manager { mutable mpz_t m_int64_min; mpz_t * allocate() { - MPZ_BEGIN_CRITICAL(); - mpz_t * cell = reinterpret_cast(m_allocator.allocate(sizeof(mpz_t))); - MPZ_END_CRITICAL(); +#ifdef SINGLE_THREAD + mpz_t * cell = reinterpret_cast(m_allocator.allocate(sizeof(mpz_t))); +#else +#if SYNC + mpz_t * cell = reinterpret_cast(memory::allocate(sizeof(mpz_t))); +#else + mpz_t * cell = reinterpret_cast(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 } }