From 9262908ebb7bdb4875a4316fdb607754ad9e72be Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 3 Jun 2019 19:50:25 -0700 Subject: [PATCH 01/68] mux Signed-off-by: Nikolaj Bjorner --- CMakeLists.txt | 38 --------- ...z3_append_linker_flag_list_to_target.cmake | 2 +- src/api/api_context.cpp | 26 +++--- src/api/api_context.h | 2 + src/api/api_log.cpp | 8 +- src/ast/rewriter/der.cpp | 7 +- src/cmd_context/echo_tactic.cpp | 22 ++---- src/sat/sat_parallel.cpp | 38 ++++----- src/sat/sat_parallel.h | 1 + src/sat/sat_solver.cpp | 12 --- src/shell/lp_frontend.cpp | 13 ++- src/shell/opt_frontend.cpp | 9 ++- src/shell/smtlib_frontend.cpp | 14 ++-- src/smt/smt_kernel.cpp | 7 +- src/solver/parallel_tactic.cpp | 2 +- src/tactic/tactical.cpp | 27 +++---- src/util/cooperate.cpp | 32 +++----- src/util/gparams.cpp | 79 +++++++++---------- src/util/memory_manager.cpp | 29 +++---- src/util/mpn.cpp | 2 - src/util/mpn.h | 10 +-- src/util/mpz.cpp | 4 - src/util/mpz.h | 12 +-- src/util/prime_generator.cpp | 5 +- src/util/rational.cpp | 5 +- src/util/rlimit.cpp | 42 ++++------ src/util/symbol.cpp | 8 +- src/util/util.cpp | 4 + src/util/util.h | 34 +++----- src/util/z3_omp.h | 38 --------- 30 files changed, 191 insertions(+), 341 deletions(-) delete mode 100644 src/util/z3_omp.h diff --git a/CMakeLists.txt b/CMakeLists.txt index fb0fc6a87..fca5520ab 100644 --- a/CMakeLists.txt +++ b/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() diff --git a/cmake/z3_append_linker_flag_list_to_target.cmake b/cmake/z3_append_linker_flag_list_to_target.cmake index 3eb1e2d34..6e1378270 100644 --- a/cmake/z3_append_linker_flag_list_to_target.cmake +++ b/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") diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 7fbbd965e..3b946bd21 100644 --- a/src/api/api_context.cpp +++ b/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) - { - SASSERT(m_ctx.m_interruptable == 0); - m_ctx.m_interruptable = &i; - } + std::lock_guard lock(ctx.m_mux); + SASSERT(m_ctx.m_interruptable == 0); + m_ctx.m_interruptable = &i; } context::set_interruptable::~set_interruptable() { - #pragma omp critical (set_interruptable) - { - m_ctx.m_interruptable = nullptr; - } + std::lock_guard lock(m_ctx.m_mux); + m_ctx.m_interruptable = nullptr; } void context::interrupt() { - #pragma omp critical (set_interruptable) - { - if (m_interruptable) - (*m_interruptable)(API_INTERRUPT_EH_CALLER); - m_limit.cancel(); - m().limit().cancel(); - } + std::lock_guard lock(m_mux); + if (m_interruptable) + (*m_interruptable)(API_INTERRUPT_EH_CALLER); + m_limit.cancel(); + m().limit().cancel(); } void context::set_error_code(Z3_error_code err, char const* opt_msg) { diff --git a/src/api/api_context.h b/src/api/api_context.h index 917d3f0af..ff239438a 100644 --- a/src/api/api_context.h +++ b/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 namespace smtlib { class parser; @@ -79,6 +80,7 @@ namespace api { scoped_ptr m_manager; scoped_ptr m_cmd; add_plugins m_plugins; + std::mutex m_mux; arith_util m_arith_util; bv_util m_bv_util; diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp index d338407bf..d6dccc670 100644 --- a/src/api/api_log.cpp +++ b/src/api/api_log.cpp @@ -16,6 +16,7 @@ Revision History: --*/ #include +#include #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 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 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 lock(g_log_mux); { #endif Z3_close_log_unsafe(); diff --git a/src/ast/rewriter/der.cpp b/src/ast/rewriter/der.cpp index c95c07f63..196750a46 100644 --- a/src/ast/rewriter/der.cpp +++ b/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() { diff --git a/src/cmd_context/echo_tactic.cpp b/src/cmd_context/echo_tactic.cpp index 1ea556bef..d722b9351 100644 --- a/src/cmd_context/echo_tactic.cpp +++ b/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() << std::endl; - } + m_ctx.regular_stream() << m_msg; + 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 << " "; - m_ctx.diagnostic_stream() << val; - if (m_newline) - m_ctx.diagnostic_stream() << std::endl; - } + if (m_msg) + m_ctx.diagnostic_stream() << m_msg << " "; + m_ctx.diagnostic_stream() << val; + if (m_newline) + m_ctx.diagnostic_stream() << std::endl; skip_tactic::operator()(in, result); } }; diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp index 77a5f973d..c66552ac5 100644 --- a/src/sat/sat_parallel.cpp +++ b/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 _disable_sync_clause(s.m_par_syncing_clauses, true); - #pragma omp critical (par_solver) { + std::lock_guard 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 _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 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) - { - m_pool.begin_add_vector(owner, n); - for (unsigned i = 0; i < n; ++i) { - m_pool.add_vector_elem(c[i].index()); - } - m_pool.end_add_vector(); + std::lock_guard lock(m_mux); + m_pool.begin_add_vector(owner, n); + for (unsigned i = 0; i < n; ++i) { + m_pool.add_vector_elem(c[i].index()); } + m_pool.end_add_vector(); } void parallel::get_clauses(solver& s) { if (s.m_par_syncing_clauses) return; flet _disable_sync_clause(s.m_par_syncing_clauses, true); - #pragma omp critical (par_solver) - { - _get_clauses(s); - } + std::lock_guard lock(m_mux); + _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) - { - _set_phase(s); - } + std::lock_guard lock(m_mux); + _set_phase(s); } void parallel::get_phase(solver& s) { - #pragma omp critical (par_solver) - { - _get_phase(s); - } + std::lock_guard lock(m_mux); + _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 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 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); diff --git a/src/sat/sat_parallel.h b/src/sat/sat_parallel.h index afb148ed4..22dbfc490 100644 --- a/src/sat/sat_parallel.h +++ b/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 m_phase; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 9241c4eaa..81f1793a9 100644 --- a/src/sat/sat_solver.cpp +++ b/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) { diff --git a/src/shell/lp_frontend.cpp b/src/shell/lp_frontend.cpp index 718f59854..96284230d 100644 --- a/src/shell/lp_frontend.cpp +++ b/src/shell/lp_frontend.cpp @@ -17,6 +17,8 @@ Author: #include "util/gparams.h" #include +static std::mutex display_stats_mux; + static lp::lp_solver* 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 lock(display_stats_mux); display_statistics(); } raise(SIGINT); } static void on_timeout() { - #pragma omp critical (g_display_stats) - { - display_statistics(); - exit(0); - } + std::lock_guard lock(display_stats_mux); + display_statistics(); + 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); diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp index afa7b79c5..e9e294eb9 100644 --- a/src/shell/opt_frontend.cpp +++ b/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 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 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 lock(display_stats_mux); display_statistics(); register_on_timeout_proc(nullptr); g_opt = nullptr; diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp index 0f156bced..ca0cbfaab 100644 --- a/src/shell/smtlib_frontend.cpp +++ b/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) - { - display_statistics(); - exit(0); - } + std::lock_guard lock(display_stats_mux); + display_statistics(); + exit(0); } static void STD_CALL on_ctrl_c(int) { signal (SIGINT, SIG_DFL); - #pragma omp critical (g_display_stats) { + std::lock_guard 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 lock(display_stats_mux); display_statistics(); g_cmd_context = nullptr; } diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index 323efeb12..9c8e08d3d 100644 --- a/src/smt/smt_kernel.cpp +++ b/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() { diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index 053a584c1..1dbb5c090 100644 --- a/src/solver/parallel_tactic.cpp +++ b/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; diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 00ea59869..9d64fa373 100644 --- a/src/tactic/tactical.cpp +++ b/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 = true; -#else - use_seq = 0 != omp_in_parallel(); -#endif + use_seq = false; 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(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 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 = true; -#else - use_seq = 0 != omp_in_parallel(); -#endif + use_seq = false; 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(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 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 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 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 lock(mux); if (!found_solution) { failed = false; found_solution = true; diff --git a/src/util/cooperate.cpp b/src/util/cooperate.cpp index df8f67968..029ac2b87 100644 --- a/src/util/cooperate.cpp +++ b/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 +#include 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; - omp_unset_nest_lock(&(g_lock.m_lock)); + g_lock.m_owner_thread = std::thread::id(); + 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) - { - omp_set_nest_lock(&(g_lock.m_lock)); - TRACE("cooperate_detail", tout << task << ", tid: " << tid << "\n";); - CTRACE("cooperate", g_lock.m_task != task, tout << "moving to task: " << task << "\n";); - g_lock.m_owner_thread = tid; - } + std::this_thread::yield(); + g_lock.m_lock.lock(); + TRACE("cooperate_detail", tout << task << ", tid: " << tid << "\n";); + CTRACE("cooperate", g_lock.m_task != task, tout << "moving to task: " << task << "\n";); + g_lock.m_owner_thread = tid; } -#endif diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index ea9b3603c..06cc67211 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -19,6 +19,9 @@ Notes: #include "util/gparams.h" #include "util/dictionary.h" #include "util/trace.h" +#include + +static std::mutex gparams_mux; extern void gparams_register_modules(); @@ -110,14 +113,12 @@ public: } void reset() { - #pragma omp critical (gparams) - { - m_params.reset(); - for (auto & kv : m_module_params) { - dealloc(kv.m_value); - } - m_module_params.reset(); + std::lock_guard lock(gparams_mux); + m_params.reset(); + for (auto & kv : m_module_params) { + dealloc(kv.m_value); } + 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 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 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 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 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) - { - for (auto & kv : get_module_param_descrs()) { - out << "[module] " << kv.m_key; - char const * descr = nullptr; - if (get_module_descrs().find(kv.m_key, descr)) { - out << ", description: " << descr; - } - out << "\n"; + std::lock_guard lock(gparams_mux); + for (auto & kv : get_module_param_descrs()) { + out << "[module] " << kv.m_key; + char const * descr = nullptr; + if (get_module_descrs().find(kv.m_key, descr)) { + out << ", description: " << descr; } + out << "\n"; } } void display_module(std::ostream & out, symbol const & module_name) { bool error = false; std::string error_msg; - #pragma omp critical (gparams) - { - try { - param_descrs * d = nullptr; - if (!get_module_param_descrs().find(module_name, d)) { - std::stringstream strm; - strm << "unknown module '" << module_name << "'"; - 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); + std::lock_guard lock(gparams_mux); + try { + param_descrs * d = nullptr; + if (!get_module_param_descrs().find(module_name, d)) { + std::stringstream strm; + strm << "unknown module '" << module_name << "'"; + throw exception(strm.str()); } - catch (z3_exception & ex) { - // Exception cannot cross critical section boundaries. - error = true; - error_msg = ex.msg(); + 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) { + // 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 lock(gparams_mux); try { symbol m, p; normalize(name, m, p); diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 6ef94e880..e1a763567 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -7,10 +7,10 @@ Copyright (c) 2015 Microsoft Corporation #include #include #include +#include #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 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 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 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; - #pragma omp critical (z3_memory_manager) - { - r = g_memory_watermark < g_memory_alloc_size; - } - return r; + std::lock_guard lock(g_memory_mux); + return g_memory_watermark < g_memory_alloc_size; } // 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 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 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 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(p) - 1; size_t sz = *sz_p; void * real_p = reinterpret_cast(sz_p); - #pragma omp critical (z3_memory_manager) { + std::lock_guard 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 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(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 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) diff --git a/src/util/mpn.cpp b/src/util/mpn.cpp index 25445bc89..7142fbad1 100644 --- a/src/util/mpn.cpp +++ b/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, diff --git a/src/util/mpn.h b/src/util/mpn.h index bae972b0c..63d3f771c 100644 --- a/src/util/mpn.h +++ b/src/util/mpn.h @@ -20,18 +20,16 @@ Revision History: #define MPN_H_ #include +#include #include "util/util.h" #include "util/buffer.h" -#include "util/z3_omp.h" typedef unsigned int mpn_digit; class mpn_manager { -#ifndef _NO_OMP_ - omp_nest_lock_t m_lock; -#endif -#define MPN_BEGIN_CRITICAL() omp_set_nest_lock(&m_lock); -#define MPN_END_CRITICAL() omp_unset_nest_lock(&m_lock); + std::recursive_mutex m_lock; +#define MPN_BEGIN_CRITICAL() m_lock.lock(); +#define MPN_END_CRITICAL() m_lock.unlock(); public: mpn_manager(); diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 1e74c2e9e..73697512d 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -139,8 +139,6 @@ uint64_t u64_gcd(uint64_t u, uint64_t v) { template mpz_manager::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::~mpz_manager() { mpz_clear(m_int64_max); mpz_clear(m_int64_min); #endif - if (SYNCH) - omp_destroy_nest_lock(&m_lock); } #ifndef _MP_GMP diff --git a/src/util/mpz.h b/src/util/mpz.h index 0faf13d18..a8916fc64 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -20,12 +20,12 @@ Revision History: #define MPZ_H_ #include +#include #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 class mpz_manager { mutable small_object_allocator m_allocator; - mutable omp_nest_lock_t m_lock; -#define MPZ_BEGIN_CRITICAL() if (SYNCH) omp_set_nest_lock(&m_lock); -#define MPZ_END_CRITICAL() if (SYNCH) omp_unset_nest_lock(&m_lock); + mutable std::recursive_mutex m_lock; +#define MPZ_BEGIN_CRITICAL() if (SYNCH) m_lock.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 & digits); }; -#ifndef _NO_OMP_ typedef mpz_manager synch_mpz_manager; -#else -typedef mpz_manager synch_mpz_manager; -#endif typedef mpz_manager unsynch_mpz_manager; typedef _scoped_numeral scoped_mpz; diff --git a/src/util/prime_generator.cpp b/src/util/prime_generator.cpp index 9d3936edf..6e17cddb7 100644 --- a/src/util/prime_generator.cpp +++ b/src/util/prime_generator.cpp @@ -17,6 +17,7 @@ Notes: --*/ #include "util/prime_generator.h" +#include #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 lock(g_prime_iterator); { r = (*m_generator)(idx); } diff --git a/src/util/rational.cpp b/src/util/rational.cpp index e8c2d52d1..3acb40422 100644 --- a/src/util/rational.cpp +++ b/src/util/rational.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include +#include #include "util/util.h" #include "util/rational.h" #ifdef _WINDOWS @@ -42,9 +43,11 @@ static void mk_power_up_to(vector & 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 lock(g_powers_of_two); { if (k >= m_powers_of_two.size()) mk_power_up_to(m_powers_of_two, k+1); diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index e3afd0d92..52816316b 100644 --- a/src/util/rlimit.cpp +++ b/src/util/rlimit.cpp @@ -18,6 +18,10 @@ Revision History: --*/ #include "util/rlimit.h" #include "util/common_msgs.h" +#include + +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) - { - m_children.push_back(r); - } + std::lock_guard lock(g_reslimit_cancel); + m_children.push_back(r); } void reslimit::pop_child() { - #pragma omp critical (reslimit_cancel) - { - m_children.pop_back(); - } + std::lock_guard lock(g_reslimit_cancel); + m_children.pop_back(); } void reslimit::cancel() { - #pragma omp critical (reslimit_cancel) - { - set_cancel(m_cancel+1); - } + std::lock_guard lock(g_reslimit_cancel); + set_cancel(m_cancel+1); } void reslimit::reset_cancel() { - #pragma omp critical (reslimit_cancel) - { - set_cancel(0); - } + std::lock_guard lock(g_reslimit_cancel); + set_cancel(0); } void reslimit::inc_cancel() { - #pragma omp critical (reslimit_cancel) - { - set_cancel(m_cancel+1); - } + std::lock_guard lock(g_reslimit_cancel); + set_cancel(m_cancel+1); } void reslimit::dec_cancel() { - #pragma omp critical (reslimit_cancel) - { - if (m_cancel > 0) { - set_cancel(m_cancel-1); - } + std::lock_guard lock(g_reslimit_cancel); + if (m_cancel > 0) { + set_cancel(m_cancel-1); } } diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp index 3f0e7c967..418f96569 100644 --- a/src/util/symbol.cpp +++ b/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 +#include + +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 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; } }; diff --git a/src/util/util.cpp b/src/util/util.cpp index 4fb361475..4b5489dc2 100644 --- a/src/util/util.cpp +++ b/src/util/util.cpp @@ -23,6 +23,10 @@ Revision History: #include #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) { diff --git a/src/util/util.h b/src/util/util.h index 9bc4f8a41..39ca45701 100644 --- a/src/util/util.h +++ b/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 #include #include +#include #include #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_ -#define LOCK_CODE(CODE) CODE; -#else -#define LOCK_CODE(CODE) \ - { \ - PRAGMA_LOCK \ - { \ - CODE; \ - } \ - } -#endif +void verbose_lock(); +void verbose_unlock(); + +#define LOCK_CODE(CODE) \ + { \ + verbose_lock(); \ + CODE; \ + verbose_unlock(); \ + } \ template struct default_eq { diff --git a/src/util/z3_omp.h b/src/util/z3_omp.h deleted file mode 100644 index 6c618192e..000000000 --- a/src/util/z3_omp.h +++ /dev/null @@ -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 -#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 From 59330b3855cff459a5561d8249ad8ad9891123d0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 3 Jun 2019 20:20:36 -0700 Subject: [PATCH 02/68] pfor Signed-off-by: Nikolaj Bjorner --- src/sat/sat_parallel.cpp | 4 ++-- src/sat/sat_parallel.h | 5 +++-- src/sat/sat_solver.cpp | 11 +++++++++-- src/util/rlimit.cpp | 15 ++++++--------- src/util/rlimit.h | 3 +++ 5 files changed, 23 insertions(+), 15 deletions(-) diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp index c66552ac5..71fed841b 100644 --- a/src/sat/sat_parallel.cpp +++ b/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()); diff --git a/src/sat/sat_parallel.h b/src/sat/sat_parallel.h index 22dbfc490..29b821b00 100644 --- a/src/sat/sat_parallel.h +++ b/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 m_limits; + scoped_ptr_vector m_limits; ptr_vector 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); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 81f1793a9..0a41959ef 100644 --- a/src/sat/sat_solver.cpp +++ b/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 - for (int i = 0; i < num_threads; ++i) { + auto worker_thread = [&](int 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 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)) { diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index 52816316b..69b1cd11c 100644 --- a/src/util/rlimit.cpp +++ b/src/util/rlimit.cpp @@ -18,9 +18,6 @@ Revision History: --*/ #include "util/rlimit.h" #include "util/common_msgs.h" -#include - -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 lock(g_reslimit_cancel); + std::lock_guard lock(m_mux); m_children.push_back(r); } void reslimit::pop_child() { - std::lock_guard lock(g_reslimit_cancel); + std::lock_guard lock(m_mux); m_children.pop_back(); } void reslimit::cancel() { - std::lock_guard lock(g_reslimit_cancel); + std::lock_guard lock(m_mux); set_cancel(m_cancel+1); } void reslimit::reset_cancel() { - std::lock_guard lock(g_reslimit_cancel); + std::lock_guard lock(m_mux); set_cancel(0); } void reslimit::inc_cancel() { - std::lock_guard lock(g_reslimit_cancel); + std::lock_guard lock(m_mux); set_cancel(m_cancel+1); } void reslimit::dec_cancel() { - std::lock_guard lock(g_reslimit_cancel); + std::lock_guard lock(m_mux); if (m_cancel > 0) { set_cancel(m_cancel-1); } diff --git a/src/util/rlimit.h b/src/util/rlimit.h index 77fab7b6b..aa57df78a 100644 --- a/src/util/rlimit.h +++ b/src/util/rlimit.h @@ -19,6 +19,7 @@ Revision History: #ifndef RLIMIT_H_ #define RLIMIT_H_ +#include #include "util/vector.h" class reslimit { @@ -28,12 +29,14 @@ class reslimit { uint64_t m_limit; svector m_limits; ptr_vector 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); From 1f84381c4c6434480c3d0be3d5d3756bcf2e5dd1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 3 Jun 2019 20:35:13 -0700 Subject: [PATCH 03/68] pfor Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 4 +++- src/tactic/tactical.cpp | 25 +++++++++++++++++++++---- 2 files changed, 24 insertions(+), 5 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 0a41959ef..b58fbf6fc 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1243,6 +1243,8 @@ namespace sat { unsigned error_code = 0; lbool result = l_undef; bool canceled = false; + std::mutex mux; + auto worker_thread = [&](int i) { try { lbool r = l_undef; @@ -1259,8 +1261,8 @@ namespace sat { r = check(num_lits, lits); } bool first = false; - #pragma omp critical (par_solver) { + std::lock_guard lock(mux); if (finished_id == -1) { finished_id = i; first = true; diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 9d64fa373..ab5ff4eab 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -405,9 +405,9 @@ public: std::string ex_msg; unsigned error_code = 0; std::mutex mux; + int num_threads = static_cast(sz); - #pragma omp parallel for - for (int i = 0; i < static_cast(sz); i++) { + auto worker_thread = [&](int i) { goal_ref_buffer _result; goal_ref in_copy = in_copies[i]; @@ -455,7 +455,16 @@ public: ex_msg = z3_ex.msg(); } } + }; + + vector 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 (finished_id == UINT_MAX) { switch (ex_kind) { case ERROR_EX: throw z3_error(error_code); @@ -548,8 +557,7 @@ public: std::string ex_msg; std::mutex mux; - #pragma omp parallel for - for (int i = 0; i < static_cast(r1_size); i++) { + auto worker_thread = [&](int i) { ast_manager & new_m = *(managers[i]); goal_ref new_g = g_copies[i]; @@ -648,6 +656,15 @@ public: } } } + }; + + vector threads; + int num_threads = static_cast(r1_size); + 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 (failed) { From f5511b41747770658aa36a59b7f2306d2a89d99a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jun 2019 02:44:59 -0700 Subject: [PATCH 04/68] missing include Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index b58fbf6fc..969a00e8a 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -19,6 +19,7 @@ Revision History: #include +#include #include "sat/sat_solver.h" #include "sat/sat_integrity_checker.h" #include "sat/sat_lookahead.h" From e4e60bff26c0dfc11c7e2fd0fe6a237527482f14 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jun 2019 02:58:32 -0700 Subject: [PATCH 05/68] include thread in tactical Signed-off-by: Nikolaj Bjorner --- src/tactic/tactical.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index ab5ff4eab..45e768198 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -21,6 +21,7 @@ Notes: #include "util/cooperate.h" #include "util/scoped_ptr_vector.h" #include "tactic/tactical.h" +#include class binary_tactical : public tactic { protected: From 9f3089b098363babae1192f8c821225d58338af0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jun 2019 04:10:55 -0700 Subject: [PATCH 06/68] try with std::vector and ptr_vectors Signed-off-by: Nikolaj Bjorner --- src/api/api_log.cpp | 60 +++++++++++++++++------------------------ src/sat/sat_solver.cpp | 3 ++- src/tactic/tactical.cpp | 13 +++++---- 3 files changed, 34 insertions(+), 42 deletions(-) diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp index d6dccc670..5f2d8f8af 100644 --- a/src/api/api_log.cpp +++ b/src/api/api_log.cpp @@ -24,7 +24,13 @@ Revision History: std::ostream * g_z3_log = nullptr; bool g_z3_log_enabled = false; + +#ifdef Z3_LOG_SYNC static std::mutex g_log_mux; +#define SCOPED_LOCK() std::lock_guard lock(g_log_mux) +#else +#define SCOPED_LOCK() {} +#endif extern "C" { void Z3_close_log_unsafe(void) { @@ -38,26 +44,20 @@ extern "C" { bool Z3_API Z3_open_log(Z3_string filename) { bool res = true; -#ifdef Z3_LOG_SYNC - std::lock_guard lock(g_log_mux); - { -#endif - if (g_z3_log != nullptr) - Z3_close_log_unsafe(); - g_z3_log = alloc(std::ofstream, filename); - if (g_z3_log->bad() || g_z3_log->fail()) { - dealloc(g_z3_log); - g_z3_log = nullptr; - res = false; - } - else { - *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << " " << __DATE__ << "\"\n"; - g_z3_log->flush(); - g_z3_log_enabled = true; - } -#ifdef Z3_LOG_SYNC + SCOPED_LOCK(); + if (g_z3_log != nullptr) + Z3_close_log_unsafe(); + g_z3_log = alloc(std::ofstream, filename); + if (g_z3_log->bad() || g_z3_log->fail()) { + dealloc(g_z3_log); + g_z3_log = nullptr; + res = false; + } + else { + *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << " " << __DATE__ << "\"\n"; + g_z3_log->flush(); + g_z3_log_enabled = true; } -#endif return res; } @@ -65,27 +65,15 @@ extern "C" { void Z3_API Z3_append_log(Z3_string str) { if (g_z3_log == nullptr) return; -#ifdef Z3_LOG_SYNC - std::lock_guard lock(g_log_mux); - { -#endif - if (g_z3_log != nullptr) - _Z3_append_log(static_cast(str)); -#ifdef Z3_LOG_SYNC - } -#endif + SCOPED_LOCK(); + if (g_z3_log != nullptr) + _Z3_append_log(static_cast(str)); } void Z3_API Z3_close_log(void) { if (g_z3_log != nullptr) { -#ifdef Z3_LOG_SYNC - std::lock_guard lock(g_log_mux); - { -#endif - Z3_close_log_unsafe(); -#ifdef Z3_LOG_SYNC - } -#endif + SCOPED_LOCK(); + Z3_close_log_unsafe(); } } } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 969a00e8a..604ec67c5 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1302,7 +1302,8 @@ namespace sat { vector threads; for (int i = 0; i < num_threads; ++i) { - threads.push_back(std::thread([&]() { worker_thread(i); })); + int id = i; + threads.push_back(std::thread([&]() { worker_thread(id); })); } for (int i = 0; i < num_threads; ++i) { threads[i].join(); diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 45e768198..82ecb819e 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -22,6 +22,7 @@ Notes: #include "util/scoped_ptr_vector.h" #include "tactic/tactical.h" #include +#include class binary_tactical : public tactic { protected: @@ -458,12 +459,13 @@ public: } }; - vector threads; + scoped_ptr_vector threads; for (int i = 0; i < num_threads; ++i) { - threads.push_back(std::thread([&]() { worker_thread(i); })); + int id = i; + threads.push_back(alloc(std::thread, [&]() { worker_thread(id); })); } for (int i = 0; i < num_threads; ++i) { - threads[i].join(); + threads[i]->join(); } if (finished_id == UINT_MAX) { @@ -659,10 +661,11 @@ public: } }; - vector threads; + std::vector threads; int num_threads = static_cast(r1_size); for (int i = 0; i < num_threads; ++i) { - threads.push_back(std::thread([&]() { worker_thread(i); })); + int id = i; + threads.emplace_back([&]() { worker_thread(id); }); } for (int i = 0; i < num_threads; ++i) { threads[i].join(); From 27971e3f68c70933302c48f7c89159d228034ef7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jun 2019 04:36:48 -0700 Subject: [PATCH 07/68] exception behavior in C++11 threads? Signed-off-by: Nikolaj Bjorner --- src/smt/tactic/smt_tactic.cpp | 1 + src/tactic/tactical.cpp | 2 ++ 2 files changed, 3 insertions(+) diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index dea1a6c0b..5445d6089 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -208,6 +208,7 @@ public: m_ctx->collect_statistics(m_stats); throw; } + SASSERT(m_ctx); m_ctx->collect_statistics(m_stats); proof * pr = m_ctx->get_proof(); TRACE("smt_tactic", tout << r << " " << pr << "\n";); diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 82ecb819e..063f3dbe1 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -416,6 +416,7 @@ public: tactic & t = *(ts.get(i)); try { + // IF_VERBOSE(0, verbose_stream() << "start\n"); t(in_copy, _result); bool first = false; { @@ -431,6 +432,7 @@ public: managers[j]->limit().cancel(); } } + IF_VERBOSE(0, verbose_stream() << "first\n"); ast_translation translator(*(managers[i]), m, false); for (goal* g : _result) { result.push_back(g->translate(translator)); From 7f74382863f3b7897fe80eea7167ff11402ef217 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jun 2019 12:42:35 -0700 Subject: [PATCH 08/68] capture i by value Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 9 +++---- src/smt/tactic/smt_tactic.cpp | 5 ++-- src/tactic/tactical.cpp | 46 +++++++++++++++++------------------ src/util/rlimit.cpp | 14 ++++++----- 4 files changed, 36 insertions(+), 38 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 604ec67c5..8a5da7531 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1300,13 +1300,12 @@ namespace sat { } }; - vector threads; + vector threads(num_threads); for (int i = 0; i < num_threads; ++i) { - int id = i; - threads.push_back(std::thread([&]() { worker_thread(id); })); + threads[i] = std::thread([&, i]() { worker_thread(i); }); } - for (int i = 0; i < num_threads; ++i) { - threads[i].join(); + for (auto & th : threads) { + th.join(); } if (IS_AUX_SOLVER(finished_id)) { diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 5445d6089..0796471b1 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -59,7 +59,7 @@ public: } ~smt_tactic() override { - SASSERT(m_ctx == 0); + SASSERT(m_ctx == nullptr); } smt_params & fparams() { @@ -132,7 +132,6 @@ public: new_ctx->set_progress_callback(o.m_callback); } o.m_ctx = new_ctx; - } ~scoped_init_ctx() { @@ -208,7 +207,7 @@ public: m_ctx->collect_statistics(m_stats); throw; } - SASSERT(m_ctx); + SASSERT(m_ctx); m_ctx->collect_statistics(m_stats); proof * pr = m_ctx->get_proof(); TRACE("smt_tactic", tout << r << " " << pr << "\n";); diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 063f3dbe1..ea89c6642 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -370,9 +370,13 @@ enum par_exception_kind { class par_tactical : public or_else_tactical { + std::string ex_msg; + unsigned error_code; public: - par_tactical(unsigned num, tactic * const * ts):or_else_tactical(num, ts) {} + par_tactical(unsigned num, tactic * const * ts):or_else_tactical(num, ts) { + error_code = 0; + } ~par_tactical() override {} @@ -404,19 +408,15 @@ public: unsigned finished_id = UINT_MAX; par_exception_kind ex_kind = DEFAULT_EX; - std::string ex_msg; - unsigned error_code = 0; - std::mutex mux; - int num_threads = static_cast(sz); - auto worker_thread = [&](int i) { - goal_ref_buffer _result; - + std::mutex mux; + + auto worker_thread = [&](unsigned i) { + goal_ref_buffer _result; goal_ref in_copy = in_copies[i]; tactic & t = *(ts.get(i)); try { - // IF_VERBOSE(0, verbose_stream() << "start\n"); t(in_copy, _result); bool first = false; { @@ -428,11 +428,11 @@ public: } if (first) { for (unsigned j = 0; j < sz; j++) { - if (static_cast(i) != j) { + if (i != j) { managers[j]->limit().cancel(); } } - IF_VERBOSE(0, verbose_stream() << "first\n"); + ast_translation translator(*(managers[i]), m, false); for (goal* g : _result) { result.push_back(g->translate(translator)); @@ -461,13 +461,13 @@ public: } }; - scoped_ptr_vector threads; - for (int i = 0; i < num_threads; ++i) { - int id = i; - threads.push_back(alloc(std::thread, [&]() { worker_thread(id); })); + vector threads(sz); + + for (unsigned i = 0; i < sz; ++i) { + threads[i] = std::thread([&, i]() { worker_thread(i); }); } - for (int i = 0; i < num_threads; ++i) { - threads[i]->join(); + for (unsigned i = 0; i < sz; ++i) { + threads[i].join(); } if (finished_id == UINT_MAX) { @@ -562,7 +562,7 @@ public: std::string ex_msg; std::mutex mux; - auto worker_thread = [&](int i) { + auto worker_thread = [&](unsigned i) { ast_manager & new_m = *(managers[i]); goal_ref new_g = g_copies[i]; @@ -663,13 +663,11 @@ public: } }; - std::vector threads; - int num_threads = static_cast(r1_size); - for (int i = 0; i < num_threads; ++i) { - int id = i; - threads.emplace_back([&]() { worker_thread(id); }); + vector threads(r1_size); + for (unsigned i = 0; i < r1_size; ++i) { + threads[i] = std::thread([&, i]() { worker_thread(i); }); } - for (int i = 0; i < num_threads; ++i) { + for (unsigned i = 0; i < r1_size; ++i) { threads[i].join(); } diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index 69b1cd11c..b99b09102 100644 --- a/src/util/rlimit.cpp +++ b/src/util/rlimit.cpp @@ -20,6 +20,8 @@ Revision History: #include "util/common_msgs.h" +static std::mutex g_rlimit_mux; + reslimit::reslimit(): m_cancel(0), m_suspend(false), @@ -70,34 +72,34 @@ char const* reslimit::get_cancel_msg() const { } void reslimit::push_child(reslimit* r) { - std::lock_guard lock(m_mux); + std::lock_guard lock(g_rlimit_mux); m_children.push_back(r); } void reslimit::pop_child() { - std::lock_guard lock(m_mux); + std::lock_guard lock(g_rlimit_mux); m_children.pop_back(); } void reslimit::cancel() { - std::lock_guard lock(m_mux); + std::lock_guard lock(g_rlimit_mux); set_cancel(m_cancel+1); } void reslimit::reset_cancel() { - std::lock_guard lock(m_mux); + std::lock_guard lock(g_rlimit_mux); set_cancel(0); } void reslimit::inc_cancel() { - std::lock_guard lock(m_mux); + std::lock_guard lock(g_rlimit_mux); set_cancel(m_cancel+1); } void reslimit::dec_cancel() { - std::lock_guard lock(m_mux); + std::lock_guard lock(g_rlimit_mux); if (m_cancel > 0) { set_cancel(m_cancel-1); } From 8f2cc6c03d94b6975278f9ab12fcdad699f8d3d3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jun 2019 12:50:45 -0700 Subject: [PATCH 09/68] updated dist cmd wrapper Signed-off-by: Nikolaj Bjorner --- scripts/mk_win_dist.cmd | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/scripts/mk_win_dist.cmd b/scripts/mk_win_dist.cmd index 22ee71e17..bbb25d727 100644 --- a/scripts/mk_win_dist.cmd +++ b/scripts/mk_win_dist.cmd @@ -1,4 +1,10 @@ call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat" -python scripts\mk_win_dist.py +python scripts\mk_win_dist.py --x64-only + +call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars86.bat" + +python scripts\mk_win_dist.py --x86-only + + From 35b36168a3327dc533c68dcb04793554bebed025 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jun 2019 12:55:30 -0700 Subject: [PATCH 10/68] fix to 32 Signed-off-by: Nikolaj Bjorner --- scripts/mk_win_dist.cmd | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_win_dist.cmd b/scripts/mk_win_dist.cmd index bbb25d727..de402000b 100644 --- a/scripts/mk_win_dist.cmd +++ b/scripts/mk_win_dist.cmd @@ -2,7 +2,7 @@ call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliar python scripts\mk_win_dist.py --x64-only -call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars86.bat" +call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars32.bat" python scripts\mk_win_dist.py --x86-only From f379a3f8b3b7386d8bd16cd73935fadef9152f9c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jun 2019 13:44:56 -0700 Subject: [PATCH 11/68] refer to z3.snk Signed-off-by: Nikolaj Bjorner --- scripts/mk_win_dist.cmd | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/scripts/mk_win_dist.cmd b/scripts/mk_win_dist.cmd index de402000b..cf3c19a9a 100644 --- a/scripts/mk_win_dist.cmd +++ b/scripts/mk_win_dist.cmd @@ -1,10 +1,11 @@ call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat" -python scripts\mk_win_dist.py --x64-only +python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk --githash call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars32.bat" -python scripts\mk_win_dist.py --x86-only +python scripts\mk_win_dist.py --x86-only --dotnet-key=$(Agent.TempDirectory)\z3.snk --githash + From c83c3a5fd76ae429d980981c7c18c0679359fd65 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jun 2019 22:45:17 +0200 Subject: [PATCH 12/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index 05815b31f..fcf06c023 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -8,6 +8,9 @@ steps: inputs: version: 2.1.300 +- task: DownloadSecureFile@1 + inputs: + secureFile: 'z3.snk' - task: BatchScript@1 displayName: 'run windist' From 3fd1a13dea6de7301502484038c0f2576c55a9ae Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jun 2019 13:49:44 -0700 Subject: [PATCH 13/68] show output Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index eda7ac6fb..d3637b0b4 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -136,7 +136,7 @@ def git_hash(): raise MKException("Failed to retrieve git hash") ls = r.split(' ') if len(ls) != 2: - raise MKException("Unexpected git output") + raise MKException("Unexpected git output " + r) return ls[0] def is_windows(): From 721bb0d3149f8840275bc5436de3a64f0df17df5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jun 2019 13:52:08 -0700 Subject: [PATCH 14/68] remove githash Signed-off-by: Nikolaj Bjorner --- scripts/mk_win_dist.cmd | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/mk_win_dist.cmd b/scripts/mk_win_dist.cmd index cf3c19a9a..d6400f3e9 100644 --- a/scripts/mk_win_dist.cmd +++ b/scripts/mk_win_dist.cmd @@ -1,10 +1,10 @@ call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat" -python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk --githash +python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars32.bat" -python scripts\mk_win_dist.py --x86-only --dotnet-key=$(Agent.TempDirectory)\z3.snk --githash +python scripts\mk_win_dist.py --x86-only --dotnet-key=$(Agent.TempDirectory)\z3.snk From 1c89fd32b59143c6fc3da2746f3dc2cabf02f0aa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jun 2019 13:56:36 -0700 Subject: [PATCH 15/68] remove reference to omp in legacy build Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 50 +++++----------------------------------------- 1 file changed, 5 insertions(+), 45 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index d3637b0b4..61d5fd1a2 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -110,7 +110,6 @@ GPROF=False GIT_HASH=False GIT_DESCRIBE=False SLOW_OPTIMIZE=False -USE_OMP=True LOG_SYNC=False GUARD_CF=False ALWAYS_DYNAMIC_BASE=False @@ -272,24 +271,6 @@ def test_gmp(cc): return exec_compiler_cmd([cc, CPPFLAGS, 'tstgmp.cpp', LDFLAGS, '-lgmp']) == 0 -def test_openmp(cc): - if not USE_OMP: - return False - if is_verbose(): - print("Testing OpenMP...") - t = TempFile('tstomp.cpp') - t.add('#include\nint main() { return omp_in_parallel() ? 1 : 0; }\n') - t.commit() - if IS_WINDOWS: - r = exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '/openmp']) == 0 - try: - rmf('tstomp.obj') - rmf('tstomp.exe') - except: - pass - return r - else: - return exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '-fopenmp']) == 0 def test_fpmath(cc): global FPMATH_FLAGS @@ -664,7 +645,6 @@ def display_help(exit_code): if not IS_WINDOWS: print(" -g, --gmp use GMP.") print(" --gprof enable gprof") - print(" --noomp disable OpenMP and all features that require it.") print(" --log-sync synchronize access to API log files to enable multi-thread API logging.") print("") print("Some influential environment variables:") @@ -692,14 +672,14 @@ def display_help(exit_code): def parse_options(): global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM global DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, JS_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED, ESRP_SIGN - global LINUX_X64, SLOW_OPTIMIZE, USE_OMP, LOG_SYNC + global LINUX_X64, SLOW_OPTIMIZE, LOG_SYNC global GUARD_CF, ALWAYS_DYNAMIC_BASE try: options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:df:sxhmcvtnp:gj', ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf', 'trace', 'dotnet', 'dotnet-key=', 'esrp', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', 'js', - 'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python', 'staticbin', 'log-sync']) + 'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'pypkgdir=', 'python', 'staticbin', 'log-sync']) except: print("ERROR: Invalid command line option") display_help(1) @@ -763,8 +743,6 @@ def parse_options(): ML_ENABLED = True elif opt == "--js": JS_ENABLED = True - elif opt in ('', '--noomp'): - USE_OMP = False elif opt in ('', '--log-sync'): LOG_SYNC = True elif opt in ('--python'): @@ -2426,7 +2404,7 @@ def mk_config(): if ONLY_MAKEFILES: return config = open(os.path.join(BUILD_DIR, 'config.mk'), 'w') - global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, HAS_OMP, LOG_SYNC + global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, LOG_SYNC if IS_WINDOWS: config.write( 'CC=cl\n' @@ -2446,12 +2424,7 @@ def mk_config(): 'OS_DEFINES=/D _WINDOWS\n') extra_opt = '' link_extra_opt = '' - HAS_OMP = test_openmp('cl') - if HAS_OMP: - extra_opt = ' /openmp' - else: - extra_opt = ' /D_NO_OMP_' - if HAS_OMP and LOG_SYNC: + if LOG_SYNC: extra_opt = '%s /DZ3_LOG_SYNC' % extra_opt if GIT_HASH: extra_opt = ' %s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH) @@ -2515,7 +2488,6 @@ def mk_config(): # End of Windows VS config.mk if is_verbose(): print('64-bit: %s' % is64()) - print('OpenMP: %s' % HAS_OMP) if is_java_enabled(): print('JNI Bindings: %s' % JNI_HOME) print('Java Compiler: %s' % JAVAC) @@ -2551,14 +2523,7 @@ def mk_config(): CXXFLAGS = '%s -fvisibility=hidden -c' % CXXFLAGS FPMATH = test_fpmath(CXX) CXXFLAGS = '%s %s' % (CXXFLAGS, FPMATH_FLAGS) - HAS_OMP = test_openmp(CXX) - if HAS_OMP: - CXXFLAGS = '%s -fopenmp' % CXXFLAGS - LDFLAGS = '%s -fopenmp' % LDFLAGS - SLIBEXTRAFLAGS = '%s -fopenmp' % SLIBEXTRAFLAGS - else: - CXXFLAGS = '%s -D_NO_OMP_' % CXXFLAGS - if HAS_OMP and LOG_SYNC: + if LOG_SYNC: CXXFLAGS = '%s -DZ3_LOG_SYNC' % CXXFLAGS if DEBUG_MODE: CXXFLAGS = '%s -g -Wall' % CXXFLAGS @@ -2661,7 +2626,6 @@ def mk_config(): print('MinGW32 cross: %s' % (is_cygwin_mingw())) print('Archive Tool: %s' % AR) print('Arithmetic: %s' % ARITH) - print('OpenMP: %s' % HAS_OMP) print('Prefix: %s' % PREFIX) print('64-bit: %s' % is64()) print('FP math: %s' % FPMATH) @@ -3166,10 +3130,6 @@ def mk_vs_proj_cl_compile(f, name, components, debug): f.write(' MultiThreadedDebugDLL\n') else: f.write(' MultiThreadedDLL\n') - if USE_OMP: - f.write(' true\n') - else: - f.write(' false\n') f.write(' ProgramDatabase\n') f.write(' ') deps = find_all_deps(name, components) From 3f7a2105d924a15f96a9e5625369704e17e127c4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 00:40:53 +0200 Subject: [PATCH 16/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index fcf06c023..8c34b71b4 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -3,6 +3,9 @@ pool: steps: + +- script: git clone https://github.com/z3prover/bin bin + - task: DotNetCoreInstaller@0 displayName: 'Use .NET Core sdk 2.1' inputs: @@ -17,4 +20,11 @@ steps: inputs: filename: 'scripts/mk_win_dist.cmd' +- script: xcopy dist\z3-4.8.6-x86-win\*.zip bin\nightly\* /y +- script: xcopy dist\z3-4.8.6-x64-win\*.zip bin\nightly\* /y +- script: cd bin\nightly +- script: git add *.zip +- script: git commit -s -a +- script: git push + From 8d769569641c8a63576aec81c6599737d167d6ea Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 04:36:39 +0200 Subject: [PATCH 17/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index 8c34b71b4..f52880426 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -15,11 +15,14 @@ steps: inputs: secureFile: 'z3.snk' +- script: dir + - task: BatchScript@1 displayName: 'run windist' inputs: filename: 'scripts/mk_win_dist.cmd' +- script: dir - script: xcopy dist\z3-4.8.6-x86-win\*.zip bin\nightly\* /y - script: xcopy dist\z3-4.8.6-x64-win\*.zip bin\nightly\* /y - script: cd bin\nightly From 73c6759b689ad0f7b4c78d4988633d630752914d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 04:40:43 +0200 Subject: [PATCH 18/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index f52880426..31e540be4 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -17,10 +17,13 @@ steps: - script: dir -- task: BatchScript@1 - displayName: 'run windist' - inputs: - filename: 'scripts/mk_win_dist.cmd' +- script: "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat" + +- script: python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk + +- script: "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars32.bat" + +- script: python scripts\mk_win_dist.py --x86-only --dotnet-key=$(Agent.TempDirectory)\z3.snk - script: dir - script: xcopy dist\z3-4.8.6-x86-win\*.zip bin\nightly\* /y From 3f6360df935e513207c1ca831bfc86f4fe191205 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 05:28:14 +0200 Subject: [PATCH 19/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index 31e540be4..a83f5d0b4 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -21,11 +21,12 @@ steps: - script: python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk -- script: "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars32.bat" +#- script: "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars32.bat" -- script: python scripts\mk_win_dist.py --x86-only --dotnet-key=$(Agent.TempDirectory)\z3.snk +#- script: python scripts\mk_win_dist.py --x86-only --dotnet-key=$(Agent.TempDirectory)\z3.snk - script: dir +- script: dir dist - script: xcopy dist\z3-4.8.6-x86-win\*.zip bin\nightly\* /y - script: xcopy dist\z3-4.8.6-x64-win\*.zip bin\nightly\* /y - script: cd bin\nightly From 1996f8447c5fdada2ba94d1618d792e8b09eb973 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 05:33:23 +0200 Subject: [PATCH 20/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index a83f5d0b4..4735a7b03 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -21,9 +21,9 @@ steps: - script: python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk -#- script: "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars32.bat" +# - script: "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars32.bat" -#- script: python scripts\mk_win_dist.py --x86-only --dotnet-key=$(Agent.TempDirectory)\z3.snk +# - script: python scripts\mk_win_dist.py --x86-only --dotnet-key=$(Agent.TempDirectory)\z3.snk - script: dir - script: dir dist From 980f9fc57e452639387fd74c5699d9c345a924d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 05:35:14 +0200 Subject: [PATCH 21/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index 4735a7b03..a24d1491d 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -21,9 +21,9 @@ steps: - script: python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk -# - script: "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars32.bat" +- script: "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars32.bat" -# - script: python scripts\mk_win_dist.py --x86-only --dotnet-key=$(Agent.TempDirectory)\z3.snk +- script: python scripts\mk_win_dist.py --x86-only --dotnet-key=$(Agent.TempDirectory)\z3.snk - script: dir - script: dir dist From ab33150f8dd73bf376dbdf06e518612fce309ea4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 05:36:16 +0200 Subject: [PATCH 22/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index a24d1491d..291d34fe2 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -17,13 +17,13 @@ steps: - script: dir -- script: "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat" +- script: "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Enterprise\\VC\\Auxiliary\\Build\\vcvars64.bat" - script: python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk -- script: "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars32.bat" +# - script: "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Enterprise\\VC\\Auxiliary\\Build\\vcvars32.bat" -- script: python scripts\mk_win_dist.py --x86-only --dotnet-key=$(Agent.TempDirectory)\z3.snk +# - script: python scripts\mk_win_dist.py --x86-only --dotnet-key=$(Agent.TempDirectory)\z3.snk - script: dir - script: dir dist From 0086ac88bf0a09255299592490a13d073313159b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 05:44:01 +0200 Subject: [PATCH 23/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index 291d34fe2..722670f97 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -17,11 +17,11 @@ steps: - script: dir -- script: "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Enterprise\\VC\\Auxiliary\\Build\\vcvars64.bat" +- script: "C:\\Program\ Files\ (x86)\\Microsoft\ Visual\ Studio\\2017\\Enterprise\\VC\\Auxiliary\\Build\\vcvars64.bat" - script: python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk -# - script: "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Enterprise\\VC\\Auxiliary\\Build\\vcvars32.bat" +# - script: "C:\\Program\ Files\ (x86)\\Microsoft\ Visual\ Studio\\2017\\Enterprise\\VC\\Auxiliary\\Build\\vcvars32.bat" # - script: python scripts\mk_win_dist.py --x86-only --dotnet-key=$(Agent.TempDirectory)\z3.snk From d3265314f3633519e59c5f4963edd8d17b7718dd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 06:01:34 +0200 Subject: [PATCH 24/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index 722670f97..4575cfe99 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -17,7 +17,7 @@ steps: - script: dir -- script: "C:\\Program\ Files\ (x86)\\Microsoft\ Visual\ Studio\\2017\\Enterprise\\VC\\Auxiliary\\Build\\vcvars64.bat" +- script: call "C:\\Program\ Files\ (x86)\\Microsoft\ Visual\ Studio\\2017\\Enterprise\\VC\\Auxiliary\\Build\\vcvars64.bat" - script: python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk From b7f9d96c2dcf0d224cb058d94fc1147110838722 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 06:05:32 +0200 Subject: [PATCH 25/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index 4575cfe99..226d180af 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -4,7 +4,7 @@ pool: steps: -- script: git clone https://github.com/z3prover/bin bin +# - script: git clone https://github.com/z3prover/bin bin - task: DotNetCoreInstaller@0 displayName: 'Use .NET Core sdk 2.1' @@ -17,7 +17,8 @@ steps: - script: dir -- script: call "C:\\Program\ Files\ (x86)\\Microsoft\ Visual\ Studio\\2017\\Enterprise\\VC\\Auxiliary\\Build\\vcvars64.bat" +- script: 'C:\Program\ Files\ (x86)\\Microsoft\ Visual\ Studio\\2017\\Enterprise\\VC\\Auxiliary\\Build\\vcvars64.bat' + - script: python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk From d520891043a21d530a9d1b921f3ce8ae77a02679 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 06:07:22 +0200 Subject: [PATCH 26/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index 226d180af..117c77247 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -17,7 +17,7 @@ steps: - script: dir -- script: 'C:\Program\ Files\ (x86)\\Microsoft\ Visual\ Studio\\2017\\Enterprise\\VC\\Auxiliary\\Build\\vcvars64.bat' +- script: 'C:\\Program\ Files\ (x86)\\Microsoft\ Visual\ Studio\\2017\\Enterprise\\VC\\Auxiliary\\Build\\vcvars64.bat' - script: python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk From 84fb0e5d5b7475a41ac184bdfcc4e78f4275e977 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 06:10:44 +0200 Subject: [PATCH 27/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index 117c77247..d849a0a17 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -17,7 +17,7 @@ steps: - script: dir -- script: 'C:\\Program\ Files\ (x86)\\Microsoft\ Visual\ Studio\\2017\\Enterprise\\VC\\Auxiliary\\Build\\vcvars64.bat' +- script: 'C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat' - script: python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk From eda1e1bc8e9c83173cc6eee5e2a4148910aa5736 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 06:12:39 +0200 Subject: [PATCH 28/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index d849a0a17..f72346ba5 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -6,18 +6,18 @@ steps: # - script: git clone https://github.com/z3prover/bin bin -- task: DotNetCoreInstaller@0 - displayName: 'Use .NET Core sdk 2.1' - inputs: - version: 2.1.300 +#- task: DotNetCoreInstaller@0 +# displayName: 'Use .NET Core sdk 2.1' +# inputs: +# version: 2.1.300 -- task: DownloadSecureFile@1 - inputs: - secureFile: 'z3.snk' +# - task: DownloadSecureFile@1 +# inputs: +# secureFile: 'z3.snk' - script: dir -- script: 'C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat' +- script: '"C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat"' - script: python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk From 451e70afee4b2208c09d2f4d30aca7f7a59395c8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 06:15:28 +0200 Subject: [PATCH 29/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index f72346ba5..f54d8a2de 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -4,25 +4,24 @@ pool: steps: -# - script: git clone https://github.com/z3prover/bin bin +- script: git clone https://github.com/z3prover/bin bin -#- task: DotNetCoreInstaller@0 -# displayName: 'Use .NET Core sdk 2.1' -# inputs: -# version: 2.1.300 +- task: DotNetCoreInstaller@0 + displayName: 'Use .NET Core sdk 2.1' + inputs: + version: 2.1.300 -# - task: DownloadSecureFile@1 -# inputs: -# secureFile: 'z3.snk' +- task: DownloadSecureFile@1 + inputs: + secureFile: 'z3.snk' - script: dir - script: '"C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat"' - - script: python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk -# - script: "C:\\Program\ Files\ (x86)\\Microsoft\ Visual\ Studio\\2017\\Enterprise\\VC\\Auxiliary\\Build\\vcvars32.bat" +# - script: '"C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars32.bat"' # - script: python scripts\mk_win_dist.py --x86-only --dotnet-key=$(Agent.TempDirectory)\z3.snk From f9c0ab5496201f6e0c082212b16d16b140250b27 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 06:25:13 +0200 Subject: [PATCH 30/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index f54d8a2de..5a6c9232e 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -17,9 +17,7 @@ steps: - script: dir -- script: '"C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat"' - -- script: python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk +- script: '"C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat"' & python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk # - script: '"C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars32.bat"' From 6d17bcc5f7e8d13a57dadf9ad94f02f4b0c8ab72 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 06:25:44 +0200 Subject: [PATCH 31/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index 5a6c9232e..5ebb7b84f 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -17,7 +17,7 @@ steps: - script: dir -- script: '"C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat"' & python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk +- script: '"C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat"' \& python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk # - script: '"C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars32.bat"' From 3087ac458acf98bdc2f9d156ff3380b3a87ecd7d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 06:29:46 +0200 Subject: [PATCH 32/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index 5ebb7b84f..765138537 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -17,7 +17,9 @@ steps: - script: dir -- script: '"C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat"' \& python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk +- script: | + '"C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat"' + python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk # - script: '"C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars32.bat"' From 6a0708fc8e14bd51b5ff5f0f25b49925fb1fa3b0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 06:33:58 +0200 Subject: [PATCH 33/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index 765138537..fb8d5e6c1 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -17,9 +17,10 @@ steps: - script: dir -- script: | - '"C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat"' - python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk +- script: scripts\mk_win_dist.cmd + +# '"C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat"' +# python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk # - script: '"C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars32.bat"' From 37882f5aface20e787b80ef80eb4667abd624462 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 5 Jun 2019 09:31:45 +0100 Subject: [PATCH 34/68] fix race condition in cooperate --- src/util/cooperate.cpp | 31 ++++++++++++------------------- src/util/cooperate.h | 7 ++----- 2 files changed, 14 insertions(+), 24 deletions(-) diff --git a/src/util/cooperate.cpp b/src/util/cooperate.cpp index 029ac2b87..fa9ac7986 100644 --- a/src/util/cooperate.cpp +++ b/src/util/cooperate.cpp @@ -17,24 +17,17 @@ Notes: --*/ +#ifndef SINGLE_THREAD + #include "util/cooperate.h" #include "util/trace.h" #include "util/debug.h" -#include +#include #include +#include -struct cooperation_lock { - std::recursive_mutex m_lock; - char const * m_task; - std::thread::id m_owner_thread; - cooperation_lock() { - m_task = nullptr; - } - ~cooperation_lock() { - } -}; - -static cooperation_lock g_lock; +static std::mutex lock; +static std::atomic owner_thread; bool cooperation_ctx::g_cooperate = false; @@ -42,17 +35,17 @@ void cooperation_ctx::checkpoint(char const * task) { SASSERT(cooperation_ctx::enabled()); std::thread::id tid = std::this_thread::get_id(); - if (g_lock.m_owner_thread == tid) { - g_lock.m_owner_thread = std::thread::id(); - g_lock.m_lock.unlock(); + if (owner_thread == tid) { + owner_thread = std::thread::id(); + lock.unlock(); } // this critical section is used to force the owner thread to give a chance to // another thread to get the lock std::this_thread::yield(); - g_lock.m_lock.lock(); + lock.lock(); TRACE("cooperate_detail", tout << task << ", tid: " << tid << "\n";); - CTRACE("cooperate", g_lock.m_task != task, tout << "moving to task: " << task << "\n";); - g_lock.m_owner_thread = tid; + owner_thread = tid; } +#endif diff --git a/src/util/cooperate.h b/src/util/cooperate.h index 6220c4c51..7e75a50c3 100644 --- a/src/util/cooperate.h +++ b/src/util/cooperate.h @@ -16,10 +16,9 @@ Author: Notes: --*/ -#ifndef COOPERATE_H_ -#define COOPERATE_H_ +#pragma once -#ifndef _NO_OMP_ +#ifndef SINGLE_THREAD class cooperation_ctx { static bool g_cooperate; @@ -35,5 +34,3 @@ inline void cooperate(char const * task) { #else inline void cooperate(char const *) {} #endif - -#endif From 9b375150ebdb0bcb04ae3a606774080c36dcac6a Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 5 Jun 2019 10:07:16 +0100 Subject: [PATCH 35/68] 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_ */ - From a53ff6f21c8243385ff577511fe8bee6a37e9dc0 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 5 Jun 2019 12:11:27 +0100 Subject: [PATCH 36/68] turn locks into no-ops when compiled with -DSINGLE_THREAD --- src/api/api_context.cpp | 6 +++--- src/api/api_context.h | 4 ++-- src/sat/sat_parallel.cpp | 4 ++-- src/sat/sat_parallel.h | 5 +++-- src/smt/asserted_formulas.cpp | 5 +---- src/smt/theory_array_bapa.cpp | 1 - src/util/gparams.cpp | 20 ++++++++++---------- src/util/memory_manager.cpp | 34 +++++++++++++--------------------- src/util/mpn.h | 9 +++++++-- src/util/mpz.h | 15 ++++++++++++--- src/util/mutex.h | 35 +++++++++++++++++++++++++++++++++++ src/util/prime_generator.cpp | 7 +++---- src/util/rational.cpp | 9 +++------ src/util/rlimit.cpp | 15 ++++++++------- src/util/rlimit.h | 9 +-------- src/util/symbol.cpp | 6 +++--- src/util/z3_exception.cpp | 1 - 17 files changed, 106 insertions(+), 79 deletions(-) create mode 100644 src/util/mutex.h diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 3b946bd21..abc02fc68 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -119,18 +119,18 @@ namespace api { context::set_interruptable::set_interruptable(context & ctx, event_handler & i): m_ctx(ctx) { - std::lock_guard lock(ctx.m_mux); + lock_guard lock(ctx.m_mux); SASSERT(m_ctx.m_interruptable == 0); m_ctx.m_interruptable = &i; } context::set_interruptable::~set_interruptable() { - std::lock_guard lock(m_ctx.m_mux); + lock_guard lock(m_ctx.m_mux); m_ctx.m_interruptable = nullptr; } void context::interrupt() { - std::lock_guard lock(m_mux); + lock_guard lock(m_mux); if (m_interruptable) (*m_interruptable)(API_INTERRUPT_EH_CALLER); m_limit.cancel(); diff --git a/src/api/api_context.h b/src/api/api_context.h index ff239438a..8d240f3de 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -42,7 +42,7 @@ Revision History: #include "ast/rewriter/seq_rewriter.h" #include "smt/smt_solver.h" #include "solver/solver.h" -#include +#include "util/mutex.h" namespace smtlib { class parser; @@ -80,7 +80,7 @@ namespace api { scoped_ptr m_manager; scoped_ptr m_cmd; add_plugins m_plugins; - std::mutex m_mux; + mutex m_mux; arith_util m_arith_util; bv_util m_bv_util; diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp index 71fed841b..c66552ac5 100644 --- a/src/sat/sat_parallel.cpp +++ b/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(alloc(reslimit)); + m_limits.push_back(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()); diff --git a/src/sat/sat_parallel.h b/src/sat/sat_parallel.h index 29b821b00..a55cc17da 100644 --- a/src/sat/sat_parallel.h +++ b/src/sat/sat_parallel.h @@ -24,6 +24,7 @@ Revision History: #include "util/map.h" #include "util/rlimit.h" #include "util/scoped_ptr_vector.h" +#include namespace sat { @@ -70,7 +71,7 @@ namespace sat { bool m_consumer_ready; scoped_limits m_scoped_rlimit; - scoped_ptr_vector m_limits; + vector m_limits; ptr_vector m_solvers; public: @@ -88,7 +89,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); diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 26d8df0ab..b1e89f72e 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -435,12 +435,9 @@ void asserted_formulas::commit(unsigned new_qhead) { TRACE("asserted_formulas", tout << "commit " << new_qhead << "\n";); m_macro_manager.mark_forbidden(new_qhead - m_qhead, m_formulas.c_ptr() + m_qhead); m_expr2depth.reset(); - bool new_sub = false; for (unsigned i = m_qhead; i < new_qhead; ++i) { justified_expr const& j = m_formulas[i]; - if (update_substitution(j.get_fml(), j.get_proof())) { - new_sub = true; - } + update_substitution(j.get_fml(), j.get_proof()); } m_qhead = new_qhead; } diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp index 6d790b68d..ab53a0ca9 100644 --- a/src/smt/theory_array_bapa.cpp +++ b/src/smt/theory_array_bapa.cpp @@ -321,7 +321,6 @@ namespace smt { sz_info& i = *kv.m_value; if (is_leaf(&i) && (i.m_literal == null_literal || !is_true(i.m_literal))) { rational value; - expr* set = k->get_arg(0); expr* sz = k->get_arg(1); if (!m_arith_value.get_value(sz, value)) { return l_undef; diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 06cc67211..0983189da 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -19,9 +19,9 @@ Notes: #include "util/gparams.h" #include "util/dictionary.h" #include "util/trace.h" -#include +#include "util/mutex.h" -static std::mutex gparams_mux; +static mutex gparams_mux; extern void gparams_register_modules(); @@ -113,7 +113,7 @@ public: } void reset() { - std::lock_guard lock(gparams_mux); + lock_guard lock(gparams_mux); m_params.reset(); for (auto & kv : m_module_params) { dealloc(kv.m_value); @@ -329,7 +329,7 @@ public: bool error = false; std::string error_msg; { - std::lock_guard lock(gparams_mux); + lock_guard lock(gparams_mux); try { symbol m, p; normalize(name, m, p); @@ -381,7 +381,7 @@ public: bool error = false; std::string error_msg; { - std::lock_guard lock(gparams_mux); + lock_guard lock(gparams_mux); try { symbol m, p; normalize(name, m, p); @@ -428,7 +428,7 @@ public: params_ref result; params_ref * ps = nullptr; { - std::lock_guard lock(gparams_mux); + lock_guard lock(gparams_mux); if (m_module_params.find(module_name, ps)) { result.copy(*ps); } @@ -448,7 +448,7 @@ public: void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) { { - std::lock_guard lock(gparams_mux); + lock_guard lock(gparams_mux); out << "Global parameters\n"; get_param_descrs().display(out, indent + 4, smt2_style, include_descr); out << "\n"; @@ -470,7 +470,7 @@ public: } void display_modules(std::ostream & out) { - std::lock_guard lock(gparams_mux); + lock_guard lock(gparams_mux); for (auto & kv : get_module_param_descrs()) { out << "[module] " << kv.m_key; char const * descr = nullptr; @@ -484,7 +484,7 @@ public: void display_module(std::ostream & out, symbol const & module_name) { bool error = false; std::string error_msg; - std::lock_guard lock(gparams_mux); + lock_guard lock(gparams_mux); try { param_descrs * d = nullptr; if (!get_module_param_descrs().find(module_name, d)) { @@ -513,7 +513,7 @@ public: bool error = false; std::string error_msg; { - std::lock_guard lock(gparams_mux); + lock_guard lock(gparams_mux); try { symbol m, p; normalize(name, m, p); diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index e1a763567..ffb664b6e 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -7,7 +7,7 @@ Copyright (c) 2015 Microsoft Corporation #include #include #include -#include +#include "util/mutex.h" #include "util/trace.h" #include "util/memory_manager.h" #include "util/error_codes.h" @@ -35,8 +35,8 @@ 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 mutex g_memory_mux; +static atomic g_memory_out_of_memory(false); static bool g_memory_initialized = false; static long long g_memory_alloc_size = 0; static long long g_memory_max_size = 0; @@ -55,10 +55,7 @@ void memory::exit_when_out_of_memory(bool flag, char const * msg) { } static void throw_out_of_memory() { - { - std::lock_guard lock(g_memory_mux); - g_memory_out_of_memory = true; - } + g_memory_out_of_memory = true; if (g_exit_when_out_of_memory) { std::cerr << g_out_of_memory_msg << "\n"; @@ -92,7 +89,7 @@ mem_usage_report g_info; void memory::initialize(size_t max_size) { bool initialize = false; { - std::lock_guard lock(g_memory_mux); + lock_guard 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,12 +113,7 @@ void memory::initialize(size_t max_size) { } bool memory::is_out_of_memory() { - bool r = false; - { - std::lock_guard lock(g_memory_mux); - r = g_memory_out_of_memory; - } - return r; + return g_memory_out_of_memory; } void memory::set_high_watermark(size_t watermark) { @@ -132,7 +124,7 @@ void memory::set_high_watermark(size_t watermark) { bool memory::above_high_watermark() { if (g_memory_watermark == 0) return false; - std::lock_guard lock(g_memory_mux); + lock_guard lock(g_memory_mux); return g_memory_watermark < g_memory_alloc_size; } @@ -161,7 +153,7 @@ void memory::finalize() { unsigned long long memory::get_allocation_size() { long long r; { - std::lock_guard lock(g_memory_mux); + lock_guard lock(g_memory_mux); r = g_memory_alloc_size; } if (r < 0) @@ -172,7 +164,7 @@ unsigned long long memory::get_allocation_size() { unsigned long long memory::get_max_used_memory() { unsigned long long r; { - std::lock_guard lock(g_memory_mux); + lock_guard lock(g_memory_mux); r = g_memory_max_used_size; } return r; @@ -256,7 +248,7 @@ static void synchronize_counters(bool allocating) { bool out_of_mem = false; bool counts_exceeded = false; { - std::lock_guard lock(g_memory_mux); + lock_guard 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) @@ -337,7 +329,7 @@ void memory::deallocate(void * p) { size_t sz = *sz_p; void * real_p = reinterpret_cast(sz_p); { - std::lock_guard lock(g_memory_mux); + lock_guard lock(g_memory_mux); g_memory_alloc_size -= sz; } free(real_p); @@ -347,7 +339,7 @@ void * memory::allocate(size_t s) { s = s + sizeof(size_t); // we allocate an extra field! bool out_of_mem = false, counts_exceeded = false; { - std::lock_guard lock(g_memory_mux); + lock_guard lock(g_memory_mux); g_memory_alloc_size += s; g_memory_alloc_count += 1; if (g_memory_alloc_size > g_memory_max_used_size) @@ -377,7 +369,7 @@ void* memory::reallocate(void *p, size_t s) { s = s + sizeof(size_t); // we allocate an extra field! bool out_of_mem = false, counts_exceeded = false; { - std::lock_guard lock(g_memory_mux); + lock_guard 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) diff --git a/src/util/mpn.h b/src/util/mpn.h index 63d3f771c..f871adda1 100644 --- a/src/util/mpn.h +++ b/src/util/mpn.h @@ -27,9 +27,14 @@ Revision History: typedef unsigned int mpn_digit; class mpn_manager { +#ifndef SINGLE_THREAD std::recursive_mutex m_lock; -#define MPN_BEGIN_CRITICAL() m_lock.lock(); -#define MPN_END_CRITICAL() m_lock.unlock(); +#define MPN_BEGIN_CRITICAL() m_lock.lock() +#define MPN_END_CRITICAL() m_lock.unlock() +#else +#define MPN_BEGIN_CRITICAL() {} +#define MPN_END_CRITICAL() {} +#endif public: mpn_manager(); diff --git a/src/util/mpz.h b/src/util/mpz.h index a8916fc64..4c927b206 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -135,9 +135,14 @@ inline void swap(mpz & m1, mpz & m2) { m1.swap(m2); } template class mpz_manager { mutable small_object_allocator m_allocator; - mutable std::recursive_mutex m_lock; -#define MPZ_BEGIN_CRITICAL() if (SYNCH) m_lock.lock(); -#define MPZ_END_CRITICAL() if (SYNCH) m_lock.unlock(); +#ifndef SINGLE_THREAD + mutable std::recursive_mutex m_lock; +#define MPZ_BEGIN_CRITICAL() if (SYNCH) m_lock.lock() +#define MPZ_END_CRITICAL() if (SYNCH) m_lock.unlock() +#else +#define MPZ_BEGIN_CRITICAL() {} +#define MPZ_END_CRITICAL() {} +#endif mutable mpn_manager m_mpn_manager; #ifndef _MP_GMP @@ -702,7 +707,11 @@ public: bool decompose(mpz const & n, svector & digits); }; +#ifndef SINGLE_THREAD typedef mpz_manager synch_mpz_manager; +#else +typedef mpz_manager synch_mpz_manager; +#endif typedef mpz_manager unsynch_mpz_manager; typedef _scoped_numeral scoped_mpz; diff --git a/src/util/mutex.h b/src/util/mutex.h new file mode 100644 index 000000000..36d06f9a2 --- /dev/null +++ b/src/util/mutex.h @@ -0,0 +1,35 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + mutex.h + +Abstract: + + Auxiliary macros for mutual exclusion + +--*/ +#pragma once + +#ifdef SINGLE_THREAD + +template using atomic = T; + +struct mutex { + void lock() {} + void unlock() {} +}; + +struct lock_guard { + lock_guard(mutex &) {} +}; + +#else +#include +#include + +template using atomic = std::atomic; +typedef std::mutex mutex; +typedef std::lock_guard lock_guard; +#endif diff --git a/src/util/prime_generator.cpp b/src/util/prime_generator.cpp index 6e17cddb7..c659403ca 100644 --- a/src/util/prime_generator.cpp +++ b/src/util/prime_generator.cpp @@ -17,7 +17,7 @@ Notes: --*/ #include "util/prime_generator.h" -#include +#include "util/mutex.h" #define PRIME_LIST_MAX_SIZE 1<<20 @@ -110,7 +110,7 @@ prime_iterator::prime_iterator(prime_generator * g):m_idx(0) { } } -static std::mutex g_prime_iterator; +static mutex g_prime_iterator; uint64_t prime_iterator::next() { unsigned idx = m_idx; @@ -120,7 +120,7 @@ uint64_t prime_iterator::next() { } else { uint64_t r; - std::lock_guard lock(g_prime_iterator); + lock_guard lock(g_prime_iterator); { r = (*m_generator)(idx); } @@ -131,4 +131,3 @@ uint64_t prime_iterator::next() { void prime_iterator::finalize() { g_prime_generator.finalize(); } - diff --git a/src/util/rational.cpp b/src/util/rational.cpp index 3acb40422..5e5ebe9e0 100644 --- a/src/util/rational.cpp +++ b/src/util/rational.cpp @@ -17,12 +17,9 @@ Revision History: --*/ #include -#include +#include "util/mutex.h" #include "util/util.h" #include "util/rational.h" -#ifdef _WINDOWS -#include -#endif synch_mpq_manager * rational::g_mpq_manager = nullptr; rational rational::m_zero; @@ -43,11 +40,11 @@ static void mk_power_up_to(vector & pws, unsigned n) { } } -static std::mutex g_powers_of_two; +static mutex g_powers_of_two; rational rational::power_of_two(unsigned k) { rational result; - std::lock_guard lock(g_powers_of_two); + lock_guard lock(g_powers_of_two); { if (k >= m_powers_of_two.size()) mk_power_up_to(m_powers_of_two, k+1); diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index b99b09102..94e1ab970 100644 --- a/src/util/rlimit.cpp +++ b/src/util/rlimit.cpp @@ -18,9 +18,10 @@ Revision History: --*/ #include "util/rlimit.h" #include "util/common_msgs.h" +#include "util/mutex.h" -static std::mutex g_rlimit_mux; +static mutex g_rlimit_mux; reslimit::reslimit(): m_cancel(0), @@ -72,34 +73,34 @@ char const* reslimit::get_cancel_msg() const { } void reslimit::push_child(reslimit* r) { - std::lock_guard lock(g_rlimit_mux); + lock_guard lock(g_rlimit_mux); m_children.push_back(r); } void reslimit::pop_child() { - std::lock_guard lock(g_rlimit_mux); + lock_guard lock(g_rlimit_mux); m_children.pop_back(); } void reslimit::cancel() { - std::lock_guard lock(g_rlimit_mux); + lock_guard lock(g_rlimit_mux); set_cancel(m_cancel+1); } void reslimit::reset_cancel() { - std::lock_guard lock(g_rlimit_mux); + lock_guard lock(g_rlimit_mux); set_cancel(0); } void reslimit::inc_cancel() { - std::lock_guard lock(g_rlimit_mux); + lock_guard lock(g_rlimit_mux); set_cancel(m_cancel+1); } void reslimit::dec_cancel() { - std::lock_guard lock(g_rlimit_mux); + lock_guard lock(g_rlimit_mux); if (m_cancel > 0) { set_cancel(m_cancel-1); } diff --git a/src/util/rlimit.h b/src/util/rlimit.h index aa57df78a..c118a1093 100644 --- a/src/util/rlimit.h +++ b/src/util/rlimit.h @@ -16,10 +16,8 @@ Author: Revision History: --*/ -#ifndef RLIMIT_H_ -#define RLIMIT_H_ +#pragma once -#include #include "util/vector.h" class reslimit { @@ -29,14 +27,12 @@ class reslimit { uint64_t m_limit; svector m_limits; ptr_vector 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); @@ -91,6 +87,3 @@ struct scoped_limits { ~scoped_limits() { for (unsigned i = 0; i < m_sz; ++i) m_limit.pop_child(); } void push_child(reslimit* lim) { m_limit.push_child(lim); ++m_sz; } }; - - -#endif diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp index 418f96569..36ea344fa 100644 --- a/src/util/symbol.cpp +++ b/src/util/symbol.cpp @@ -17,13 +17,13 @@ Revision History: --*/ #include "util/symbol.h" +#include "util/mutex.h" #include "util/str_hashtable.h" #include "util/region.h" #include "util/string_buffer.h" #include -#include -static std::mutex g_symbol_lock; +static mutex g_symbol_lock; symbol symbol::m_dummy(TAG(void*, nullptr, 2)); const symbol symbol::null; @@ -38,7 +38,7 @@ public: char const * get_str(char const * d) { const char * result; - std::lock_guard lock(g_symbol_lock); + lock_guard lock(g_symbol_lock); str_hashtable::entry * e; if (m_table.insert_if_not_there_core(d, e)) { // new entry diff --git a/src/util/z3_exception.cpp b/src/util/z3_exception.cpp index 585313024..6b9e16a5d 100644 --- a/src/util/z3_exception.cpp +++ b/src/util/z3_exception.cpp @@ -16,7 +16,6 @@ Author: Notes: --*/ -#include #include #include #include "util/z3_exception.h" From cd3b807e2c8a7a82d97590549118c5ac946608d3 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 5 Jun 2019 15:18:27 +0100 Subject: [PATCH 37/68] add --single-threaded to old configure system --- scripts/mk_util.py | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 61d5fd1a2..8aaec3360 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -111,6 +111,7 @@ GIT_HASH=False GIT_DESCRIBE=False SLOW_OPTIMIZE=False LOG_SYNC=False +SINGLE_THREADED=False GUARD_CF=False ALWAYS_DYNAMIC_BASE=False @@ -646,6 +647,7 @@ def display_help(exit_code): print(" -g, --gmp use GMP.") print(" --gprof enable gprof") print(" --log-sync synchronize access to API log files to enable multi-thread API logging.") + print(" --single-threaded non-thread-safe build") print("") print("Some influential environment variables:") if not IS_WINDOWS: @@ -672,14 +674,14 @@ def display_help(exit_code): def parse_options(): global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM global DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, JS_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED, ESRP_SIGN - global LINUX_X64, SLOW_OPTIMIZE, LOG_SYNC + global LINUX_X64, SLOW_OPTIMIZE, LOG_SYNC, SINGLE_THREADED global GUARD_CF, ALWAYS_DYNAMIC_BASE try: options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:df:sxhmcvtnp:gj', ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf', 'trace', 'dotnet', 'dotnet-key=', 'esrp', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', 'js', - 'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'pypkgdir=', 'python', 'staticbin', 'log-sync']) + 'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'pypkgdir=', 'python', 'staticbin', 'log-sync', 'single-threaded']) except: print("ERROR: Invalid command line option") display_help(1) @@ -745,6 +747,8 @@ def parse_options(): JS_ENABLED = True elif opt in ('', '--log-sync'): LOG_SYNC = True + elif opt == '--single-threaded': + SINGLE_THREADED = True elif opt in ('--python'): PYTHON_ENABLED = True PYTHON_INSTALL_ENABLED = True @@ -2404,7 +2408,7 @@ def mk_config(): if ONLY_MAKEFILES: return config = open(os.path.join(BUILD_DIR, 'config.mk'), 'w') - global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, LOG_SYNC + global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, LOG_SYNC, SINGLE_THREADED if IS_WINDOWS: config.write( 'CC=cl\n' @@ -2426,6 +2430,8 @@ def mk_config(): link_extra_opt = '' if LOG_SYNC: extra_opt = '%s /DZ3_LOG_SYNC' % extra_opt + if SINGLE_THREADED: + extra_opt = '%s /DSINGLE_THREAD' % extra_opt if GIT_HASH: extra_opt = ' %s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH) if GUARD_CF: @@ -2525,6 +2531,8 @@ def mk_config(): CXXFLAGS = '%s %s' % (CXXFLAGS, FPMATH_FLAGS) if LOG_SYNC: CXXFLAGS = '%s -DZ3_LOG_SYNC' % CXXFLAGS + if SINGLE_THREADED: + CXXFLAGS = '%s -DSINGLE_THREAD' % CXXFLAGS if DEBUG_MODE: CXXFLAGS = '%s -g -Wall' % CXXFLAGS EXAMP_DEBUG_FLAG = '-g' From 6e6e7d51a14fd8bad80fd2a88b58751be55b534e Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 5 Jun 2019 15:44:25 +0100 Subject: [PATCH 38/68] cmake: addd SINGLE_THREADED option --- CMakeLists.txt | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index fca5520ab..5c82c1c00 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -287,6 +287,20 @@ else() message(STATUS "Not using API_LOG_SYNC") endif() +################################################################################ +# Thread safe or not? +################################################################################ +option(SINGLE_THREADED + "Non-thread-safe build" + OFF +) +if (SINGLE_THREADED) + list(APPEND Z3_COMPONENT_CXX_DEFINES "-DSINGLE_THREAD") + message(STATUS "Non-thread-safe build") +else() + message(STATUS "Thread-safe build") +endif() + ################################################################################ # FP math ################################################################################ From 15f645da66b0581f8d8b76d0ac5a746dcd827fee Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 09:48:15 -0700 Subject: [PATCH 39/68] debug options Signed-off-by: Nikolaj Bjorner --- scripts/mk_win_dist.py | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index c685f4bd8..e4a0c0542 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -89,6 +89,7 @@ def parse_options(): 'x86-only', 'x64-only' ]) + print(options) for opt, arg in options: if opt in ('-b', '--build'): if arg == 'src': From 8b187e4c0aac0a9a845fb6e5eae969a7cb573cbe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 19:40:02 +0200 Subject: [PATCH 40/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index fb8d5e6c1..3d9efea03 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -16,20 +16,10 @@ steps: secureFile: 'z3.snk' - script: dir - - script: scripts\mk_win_dist.cmd - -# '"C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat"' -# python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk - -# - script: '"C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars32.bat"' - -# - script: python scripts\mk_win_dist.py --x86-only --dotnet-key=$(Agent.TempDirectory)\z3.snk - - script: dir - script: dir dist -- script: xcopy dist\z3-4.8.6-x86-win\*.zip bin\nightly\* /y -- script: xcopy dist\z3-4.8.6-x64-win\*.zip bin\nightly\* /y +- script: xcopy dist\*.zip bin\nightly\* /y - script: cd bin\nightly - script: git add *.zip - script: git commit -s -a From cdad6f3f977cd32c77909073ddba935e4ae2ae37 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 20:14:35 +0200 Subject: [PATCH 41/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index 3d9efea03..f45225f88 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -15,14 +15,7 @@ steps: inputs: secureFile: 'z3.snk' -- script: dir - script: scripts\mk_win_dist.cmd -- script: dir -- script: dir dist -- script: xcopy dist\*.zip bin\nightly\* /y -- script: cd bin\nightly -- script: git add *.zip -- script: git commit -s -a -- script: git push + From 2d95e8de546cdf3414be8b24e406aa610c2f477d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 11:17:09 -0700 Subject: [PATCH 42/68] update cmd Signed-off-by: Nikolaj Bjorner --- scripts/mk_win_dist.cmd | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/scripts/mk_win_dist.cmd b/scripts/mk_win_dist.cmd index d6400f3e9..c959b134c 100644 --- a/scripts/mk_win_dist.cmd +++ b/scripts/mk_win_dist.cmd @@ -6,6 +6,18 @@ call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliar python scripts\mk_win_dist.py --x86-only --dotnet-key=$(Agent.TempDirectory)\z3.snk +<<<<<<< HEAD +xcopy dist\*.zip bin\nightly\* /y + +cd bin\nightly + +git add *.zip + +git commit -s -a -m "nightly Windows" + +git push +======= +>>>>>>> cdad6f3f977cd32c77909073ddba935e4ae2ae37 From 5c9c76055ebf61b3a551095ccd64376eafb1f05f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 13:19:37 -0700 Subject: [PATCH 43/68] merge Signed-off-by: Nikolaj Bjorner --- scripts/mk_win_dist.cmd | 5 ----- 1 file changed, 5 deletions(-) diff --git a/scripts/mk_win_dist.cmd b/scripts/mk_win_dist.cmd index c959b134c..66b9747ed 100644 --- a/scripts/mk_win_dist.cmd +++ b/scripts/mk_win_dist.cmd @@ -6,7 +6,6 @@ call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliar python scripts\mk_win_dist.py --x86-only --dotnet-key=$(Agent.TempDirectory)\z3.snk -<<<<<<< HEAD xcopy dist\*.zip bin\nightly\* /y cd bin\nightly @@ -16,8 +15,4 @@ git add *.zip git commit -s -a -m "nightly Windows" git push -======= - - ->>>>>>> cdad6f3f977cd32c77909073ddba935e4ae2ae37 From 9b412a1f3dfb10a967a31c01cb65db0292d7db6e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 13:55:51 -0700 Subject: [PATCH 44/68] configure git identity Signed-off-by: Nikolaj Bjorner --- scripts/mk_win_dist.cmd | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/scripts/mk_win_dist.cmd b/scripts/mk_win_dist.cmd index 66b9747ed..bbe7de5ae 100644 --- a/scripts/mk_win_dist.cmd +++ b/scripts/mk_win_dist.cmd @@ -1,3 +1,7 @@ +git config --global user.email "nbjorner@microsoft.com" + +git config --global user.name "Nikolaj Bjorner" + call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat" python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk From d4c9b20dad9ad2d03c57474672d7342886023c58 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 13:56:55 -0700 Subject: [PATCH 45/68] test Signed-off-by: Nikolaj Bjorner --- scripts/mk_win_dist.cmd | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/scripts/mk_win_dist.cmd b/scripts/mk_win_dist.cmd index bbe7de5ae..250f1a3c1 100644 --- a/scripts/mk_win_dist.cmd +++ b/scripts/mk_win_dist.cmd @@ -2,6 +2,19 @@ git config --global user.email "nbjorner@microsoft.com" git config --global user.name "Nikolaj Bjorner" +echo "test" > bin\nightly\ping.txt + +cd bin\nightly + +git add ping.txt + +git commit -s -a -m "test" + +git push + +goto :EOF + + call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat" python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk From 39dcd1b3201efba18d4580bd52f6e2d88970edc4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 23:57:31 +0200 Subject: [PATCH 46/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index f45225f88..a6053b6f7 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -17,5 +17,15 @@ steps: - script: scripts\mk_win_dist.cmd - +- task: GitHubRelease@0 + inputs: + repositoryName: '$(Build.Repository.Name)' + action: 'edit' + target: '$(Build.SourceVersion)' + tag: 'nightly' + title: 'nightly' + releaseNotesSource: 'input' + releaseNotes: 'nightly build' + isDraft: true + isPreRelease: true From 0714f800d5f74f6a5b2fc4500a986095f558821c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Jun 2019 00:07:55 +0200 Subject: [PATCH 47/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 28 +++++++++++++++------------- 1 file changed, 15 insertions(+), 13 deletions(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index a6053b6f7..5a2f5f35a 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -1,24 +1,13 @@ pool: vmImage: "vs2017-win2016" - steps: -- script: git clone https://github.com/z3prover/bin bin - -- task: DotNetCoreInstaller@0 - displayName: 'Use .NET Core sdk 2.1' - inputs: - version: 2.1.300 - -- task: DownloadSecureFile@1 - inputs: - secureFile: 'z3.snk' - -- script: scripts\mk_win_dist.cmd +- script: echo "test" > $(Build.ArtifactStagingDirectory)/ping.txt - task: GitHubRelease@0 inputs: + gitHubConnection: Z3GitHub repositoryName: '$(Build.Repository.Name)' action: 'edit' target: '$(Build.SourceVersion)' @@ -29,3 +18,16 @@ steps: isDraft: true isPreRelease: true +# - script: git clone https://github.com/z3prover/bin bin + +# - task: DotNetCoreInstaller@0 +# displayName: 'Use .NET Core sdk 2.1' +# inputs: +# version: 2.1.300 + +# - task: DownloadSecureFile@1 +# inputs: +# secureFile: 'z3.snk' + +# - script: scripts\mk_win_dist.cmd + From 4307c28d171cad821b0b6af4cffa0bb85836de6d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Jun 2019 00:11:40 +0200 Subject: [PATCH 48/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index 5a2f5f35a..201d291fa 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -8,7 +8,7 @@ steps: - task: GitHubRelease@0 inputs: gitHubConnection: Z3GitHub - repositoryName: '$(Build.Repository.Name)' + repositoryName: 'Z3Prover/bin' action: 'edit' target: '$(Build.SourceVersion)' tag: 'nightly' From 77ba793f3b06a3833fd863a01eb15ecfbd4bcce7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Jun 2019 00:27:38 +0200 Subject: [PATCH 49/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index 201d291fa..08e181bad 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -11,7 +11,7 @@ steps: repositoryName: 'Z3Prover/bin' action: 'edit' target: '$(Build.SourceVersion)' - tag: 'nightly' + tag: 'Git tag' title: 'nightly' releaseNotesSource: 'input' releaseNotes: 'nightly build' From 7ecf2f1136679a61987a1a9ee95140fde1826d2c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Jun 2019 00:29:43 +0200 Subject: [PATCH 50/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index 08e181bad..22feff8da 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -11,7 +11,8 @@ steps: repositoryName: 'Z3Prover/bin' action: 'edit' target: '$(Build.SourceVersion)' - tag: 'Git tag' + tagSource: 'auto' + tag: '1.0' title: 'nightly' releaseNotesSource: 'input' releaseNotes: 'nightly build' From 5341e24b5d544296daeefc2ba63a3aa284c30761 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Jun 2019 00:31:07 +0200 Subject: [PATCH 51/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index 22feff8da..ed399fed7 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -11,8 +11,8 @@ steps: repositoryName: 'Z3Prover/bin' action: 'edit' target: '$(Build.SourceVersion)' - tagSource: 'auto' - tag: '1.0' + tagSource: 'manual' + tag: 'nightly' title: 'nightly' releaseNotesSource: 'input' releaseNotes: 'nightly build' From 4a5155a73585e7ecd15ada818fc87d5909928274 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Jun 2019 00:32:32 +0200 Subject: [PATCH 52/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index ed399fed7..f0db50a9b 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -9,7 +9,7 @@ steps: inputs: gitHubConnection: Z3GitHub repositoryName: 'Z3Prover/bin' - action: 'edit' + action: 'create' target: '$(Build.SourceVersion)' tagSource: 'manual' tag: 'nightly' From e115a60ddf0927d3f5493a34e8ba8d9395fbdbe8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Jun 2019 00:34:12 +0200 Subject: [PATCH 53/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index f0db50a9b..29720b5ce 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -8,7 +8,7 @@ steps: - task: GitHubRelease@0 inputs: gitHubConnection: Z3GitHub - repositoryName: 'Z3Prover/bin' + repositoryName: 'Z3Prover/z3' action: 'create' target: '$(Build.SourceVersion)' tagSource: 'manual' From c9817ff74dca3c770ef2ee21f225a670a23629ec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Jun 2019 00:38:46 +0200 Subject: [PATCH 54/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index 29720b5ce..b84a7534f 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -12,7 +12,7 @@ steps: action: 'create' target: '$(Build.SourceVersion)' tagSource: 'manual' - tag: 'nightly' + tag: '$(Build.SourceVersion)' title: 'nightly' releaseNotesSource: 'input' releaseNotes: 'nightly build' From 19a64a6540b0ec6cc9f68d60cc68d5bc0234c292 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 15:51:07 -0700 Subject: [PATCH 55/68] update dist Signed-off-by: Nikolaj Bjorner --- scripts/mk_win_dist.cmd | 26 -------------------------- 1 file changed, 26 deletions(-) diff --git a/scripts/mk_win_dist.cmd b/scripts/mk_win_dist.cmd index 250f1a3c1..e3c24da2f 100644 --- a/scripts/mk_win_dist.cmd +++ b/scripts/mk_win_dist.cmd @@ -1,19 +1,3 @@ -git config --global user.email "nbjorner@microsoft.com" - -git config --global user.name "Nikolaj Bjorner" - -echo "test" > bin\nightly\ping.txt - -cd bin\nightly - -git add ping.txt - -git commit -s -a -m "test" - -git push - -goto :EOF - call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat" @@ -23,13 +7,3 @@ call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliar python scripts\mk_win_dist.py --x86-only --dotnet-key=$(Agent.TempDirectory)\z3.snk -xcopy dist\*.zip bin\nightly\* /y - -cd bin\nightly - -git add *.zip - -git commit -s -a -m "nightly Windows" - -git push - From 327321cce48a211fce8dc3512e32d018c8b7dc9e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Jun 2019 00:51:25 +0200 Subject: [PATCH 56/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index b84a7534f..c39b231fb 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -3,7 +3,18 @@ pool: steps: -- script: echo "test" > $(Build.ArtifactStagingDirectory)/ping.txt +- task: DotNetCoreInstaller@0 + displayName: 'Use .NET Core sdk 2.1' + inputs: + version: 2.1.300 + +- task: DownloadSecureFile@1 + inputs: + secureFile: 'z3.snk' + +- script: scripts\mk_win_dist.cmd + +- script: xcopy dist\*.zip $(Build.ArtifactStagingDirectory)/* /y - task: GitHubRelease@0 inputs: @@ -13,22 +24,12 @@ steps: target: '$(Build.SourceVersion)' tagSource: 'manual' tag: '$(Build.SourceVersion)' - title: 'nightly' + title: 'Nightly Windows' releaseNotesSource: 'input' releaseNotes: 'nightly build' isDraft: true isPreRelease: true -# - script: git clone https://github.com/z3prover/bin bin -# - task: DotNetCoreInstaller@0 -# displayName: 'Use .NET Core sdk 2.1' -# inputs: -# version: 2.1.300 -# - task: DownloadSecureFile@1 -# inputs: -# secureFile: 'z3.snk' - -# - script: scripts\mk_win_dist.cmd From a753c38c6f5c279f376a9aeeab9d31b4fd95de93 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Jun 2019 01:44:10 +0200 Subject: [PATCH 57/68] Update azure-pipeline.vs.yaml for Azure Pipelines --- scripts/azure-pipeline.vs.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/azure-pipeline.vs.yaml index c39b231fb..6ebecd3a9 100644 --- a/scripts/azure-pipeline.vs.yaml +++ b/scripts/azure-pipeline.vs.yaml @@ -14,7 +14,7 @@ steps: - script: scripts\mk_win_dist.cmd -- script: xcopy dist\*.zip $(Build.ArtifactStagingDirectory)/* /y +- script: xcopy dist\*.zip $(Build.ArtifactStagingDirectory)\* /y - task: GitHubRelease@0 inputs: From c8ce31a04bee5fe29d97604a88812ec04958847f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 17:22:13 -0700 Subject: [PATCH 58/68] rename nightly Signed-off-by: Nikolaj Bjorner --- scripts/{azure-pipeline.vs.yaml => nightly-windows.yaml} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename scripts/{azure-pipeline.vs.yaml => nightly-windows.yaml} (100%) diff --git a/scripts/azure-pipeline.vs.yaml b/scripts/nightly-windows.yaml similarity index 100% rename from scripts/azure-pipeline.vs.yaml rename to scripts/nightly-windows.yaml From 5687cda1012224c8da0b06de1afc1dd1fac191e5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 17:25:21 -0700 Subject: [PATCH 59/68] add ubuntu nightly Signed-off-by: Nikolaj Bjorner --- scripts/nightly-ubuntu.yaml | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 scripts/nightly-ubuntu.yaml diff --git a/scripts/nightly-ubuntu.yaml b/scripts/nightly-ubuntu.yaml new file mode 100644 index 000000000..6ebecd3a9 --- /dev/null +++ b/scripts/nightly-ubuntu.yaml @@ -0,0 +1,35 @@ +pool: + vmImage: "vs2017-win2016" + +steps: + +- task: DotNetCoreInstaller@0 + displayName: 'Use .NET Core sdk 2.1' + inputs: + version: 2.1.300 + +- task: DownloadSecureFile@1 + inputs: + secureFile: 'z3.snk' + +- script: scripts\mk_win_dist.cmd + +- script: xcopy dist\*.zip $(Build.ArtifactStagingDirectory)\* /y + +- task: GitHubRelease@0 + inputs: + gitHubConnection: Z3GitHub + repositoryName: 'Z3Prover/z3' + action: 'create' + target: '$(Build.SourceVersion)' + tagSource: 'manual' + tag: '$(Build.SourceVersion)' + title: 'Nightly Windows' + releaseNotesSource: 'input' + releaseNotes: 'nightly build' + isDraft: true + isPreRelease: true + + + + From ae93469e17cec9cd3e9df8f3880fdbbc509bac11 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Jun 2019 02:29:06 +0200 Subject: [PATCH 60/68] Set up CI with Azure Pipelines [skip ci] --- scripts/nightly-ubuntu.yaml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/scripts/nightly-ubuntu.yaml b/scripts/nightly-ubuntu.yaml index 6ebecd3a9..36ddfc47d 100644 --- a/scripts/nightly-ubuntu.yaml +++ b/scripts/nightly-ubuntu.yaml @@ -1,5 +1,5 @@ pool: - vmImage: "vs2017-win2016" + vmImage: "ubuntu-16.04" steps: @@ -12,9 +12,9 @@ steps: inputs: secureFile: 'z3.snk' -- script: scripts\mk_win_dist.cmd +- script: python scripts/mk_unix_dist.py --dotnet-key=$(Agent.TempDirectory)/z3.snk -- script: xcopy dist\*.zip $(Build.ArtifactStagingDirectory)\* /y +- script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/* - task: GitHubRelease@0 inputs: @@ -24,10 +24,10 @@ steps: target: '$(Build.SourceVersion)' tagSource: 'manual' tag: '$(Build.SourceVersion)' - title: 'Nightly Windows' + title: 'Nightly Ubuntu' releaseNotesSource: 'input' releaseNotes: 'nightly build' - isDraft: true + isDraft: false isPreRelease: true From 7c034827cbbbd6bf404fc84915486ad605efaed9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Jun 2019 04:15:43 +0200 Subject: [PATCH 61/68] Update nightly-ubuntu.yaml for Azure Pipelines --- scripts/nightly-ubuntu.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/nightly-ubuntu.yaml b/scripts/nightly-ubuntu.yaml index 36ddfc47d..0b2fbd35b 100644 --- a/scripts/nightly-ubuntu.yaml +++ b/scripts/nightly-ubuntu.yaml @@ -23,7 +23,7 @@ steps: action: 'create' target: '$(Build.SourceVersion)' tagSource: 'manual' - tag: '$(Build.SourceVersion)' + tag: 'Ubuntu$(Build.SourceVersion)' title: 'Nightly Ubuntu' releaseNotesSource: 'input' releaseNotes: 'nightly build' From 75b92df1d02b1134ac7010b90c1b0133fea6c9ff Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 19:40:24 -0700 Subject: [PATCH 62/68] change cp command Signed-off-by: Nikolaj Bjorner --- scripts/nightly-ubuntu.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/nightly-ubuntu.yaml b/scripts/nightly-ubuntu.yaml index 36ddfc47d..9caf6f402 100644 --- a/scripts/nightly-ubuntu.yaml +++ b/scripts/nightly-ubuntu.yaml @@ -14,7 +14,7 @@ steps: - script: python scripts/mk_unix_dist.py --dotnet-key=$(Agent.TempDirectory)/z3.snk -- script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/* +- script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/. - task: GitHubRelease@0 inputs: From dc452b92e1d5929e932eded7bfc0e9b98b9e5907 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 20:11:00 -0700 Subject: [PATCH 63/68] update tag Signed-off-by: Nikolaj Bjorner --- scripts/nightly-ubuntu.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/nightly-ubuntu.yaml b/scripts/nightly-ubuntu.yaml index 06eec7b00..142e5cdf7 100644 --- a/scripts/nightly-ubuntu.yaml +++ b/scripts/nightly-ubuntu.yaml @@ -23,7 +23,7 @@ steps: action: 'create' target: '$(Build.SourceVersion)' tagSource: 'manual' - tag: 'Ubuntu$(Build.SourceVersion)' + tag: 'NightlyUbuntu' title: 'Nightly Ubuntu' releaseNotesSource: 'input' releaseNotes: 'nightly build' From f0f37411a2ea16dd4d1f3c2e37755bd22a20e67d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 20:15:11 -0700 Subject: [PATCH 64/68] macos Signed-off-by: Nikolaj Bjorner --- scripts/nightly-macos.yaml | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 scripts/nightly-macos.yaml diff --git a/scripts/nightly-macos.yaml b/scripts/nightly-macos.yaml new file mode 100644 index 000000000..4c4a10112 --- /dev/null +++ b/scripts/nightly-macos.yaml @@ -0,0 +1,35 @@ +pool: + vmImage: "macOS-10.14" + +steps: + +- task: DotNetCoreInstaller@0 + displayName: 'Use .NET Core sdk 2.1' + inputs: + version: 2.1.300 + +- task: DownloadSecureFile@1 + inputs: + secureFile: 'z3.snk' + +- script: python scripts/mk_unix_dist.py --dotnet-key=$(Agent.TempDirectory)/z3.snk + +- script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/. + +- task: GitHubRelease@0 + inputs: + gitHubConnection: Z3GitHub + repositoryName: 'Z3Prover/z3' + action: 'create' + target: '$(Build.SourceVersion)' + tagSource: 'manual' + tag: 'NightlyMacOs' + title: 'Nightly MacOs' + releaseNotesSource: 'input' + releaseNotes: 'nightly build' + isDraft: false + isPreRelease: true + + + + From 7c1e935bc28148cda705f0bc8fcae54836217a8d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 22:17:09 -0700 Subject: [PATCH 65/68] rlimit mux Signed-off-by: Nikolaj Bjorner --- src/util/rlimit.cpp | 2 -- src/util/rlimit.h | 1 + 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index 94e1ab970..ac596a118 100644 --- a/src/util/rlimit.cpp +++ b/src/util/rlimit.cpp @@ -87,7 +87,6 @@ void reslimit::cancel() { set_cancel(m_cancel+1); } - void reslimit::reset_cancel() { lock_guard lock(g_rlimit_mux); set_cancel(0); @@ -98,7 +97,6 @@ void reslimit::inc_cancel() { set_cancel(m_cancel+1); } - void reslimit::dec_cancel() { lock_guard lock(g_rlimit_mux); if (m_cancel > 0) { diff --git a/src/util/rlimit.h b/src/util/rlimit.h index c118a1093..18124717a 100644 --- a/src/util/rlimit.h +++ b/src/util/rlimit.h @@ -20,6 +20,7 @@ Revision History: #include "util/vector.h" + class reslimit { volatile unsigned m_cancel; bool m_suspend; From 2d75bf9d124f21ca8369760f177525f6aae89dfb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 23:47:53 -0700 Subject: [PATCH 66/68] edit Signed-off-by: Nikolaj Bjorner --- scripts/nightly-macos.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/nightly-macos.yaml b/scripts/nightly-macos.yaml index 4c4a10112..37b7169df 100644 --- a/scripts/nightly-macos.yaml +++ b/scripts/nightly-macos.yaml @@ -20,7 +20,7 @@ steps: inputs: gitHubConnection: Z3GitHub repositoryName: 'Z3Prover/z3' - action: 'create' + action: 'edit' target: '$(Build.SourceVersion)' tagSource: 'manual' tag: 'NightlyMacOs' From 8f1325d5c5d7d810639009026a80a290579dae13 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Jun 2019 17:29:23 +0200 Subject: [PATCH 67/68] Update nightly-ubuntu.yaml for Azure Pipelines --- scripts/nightly-ubuntu.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/nightly-ubuntu.yaml b/scripts/nightly-ubuntu.yaml index 142e5cdf7..53fbc4b70 100644 --- a/scripts/nightly-ubuntu.yaml +++ b/scripts/nightly-ubuntu.yaml @@ -20,7 +20,7 @@ steps: inputs: gitHubConnection: Z3GitHub repositoryName: 'Z3Prover/z3' - action: 'create' + action: 'edit' target: '$(Build.SourceVersion)' tagSource: 'manual' tag: 'NightlyUbuntu' From 783f99889217a1c15de3ab168054618217e001f7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Jun 2019 17:31:18 +0200 Subject: [PATCH 68/68] Update nightly-windows.yaml for Azure Pipelines --- scripts/nightly-windows.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/nightly-windows.yaml b/scripts/nightly-windows.yaml index 6ebecd3a9..fccf6a877 100644 --- a/scripts/nightly-windows.yaml +++ b/scripts/nightly-windows.yaml @@ -20,10 +20,10 @@ steps: inputs: gitHubConnection: Z3GitHub repositoryName: 'Z3Prover/z3' - action: 'create' + action: 'edit' target: '$(Build.SourceVersion)' tagSource: 'manual' - tag: '$(Build.SourceVersion)' + tag: 'NightlyWindows' title: 'Nightly Windows' releaseNotesSource: 'input' releaseNotes: 'nightly build'