diff --git a/CMakeLists.txt b/CMakeLists.txt index cfd43571422..34f3caecdeb 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -254,6 +254,21 @@ else() message(STATUS "Thread-safe build") endif() + +################################################################################ +# Use polling based timeout. This avoids spawning threads for timer tasks +################################################################################ +option(Z3_POLLING_TIMER + "Use polling based timeout checks" + OFF +) +if (Z3_POLLING_TIMER) + list(APPEND Z3_COMPONENT_CXX_DEFINES "-DPOLLING_TIMER") + message(STATUS "Polling based timer") +endif() + + + ################################################################################ # FP math ################################################################################ diff --git a/README-CMake.md b/README-CMake.md index 9bfc2d9ef29..04773718614 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -310,6 +310,7 @@ The following useful options can be passed to CMake whilst configuring. * ``Z3_BUILD_TEST_EXECUTABLES`` - BOOL. If set to ``TRUE`` build the z3 test executables. Defaults to ``TRUE`` unless z3 is being built as a submodule in which case it defaults to ``FALSE``. * ``Z3_SAVE_CLANG_OPTIMIZATION_RECORDS`` - BOOL. If set to ``TRUE`` saves Clang optimization records by setting the compiler flag ``-fsave-optimization-record``. * ``Z3_SINGLE_THREADED`` - BOOL. If set to ``TRUE`` compiles Z3 for single threaded mode. +* ``Z3_POLLING_TIMER`` - BOOL. If set to ``TRUE`` compiles Z3 to use polling based timer instead of requiring a thread. This is useful for wasm builds and avoids spawning threads that interfere with how WASM is run. On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface. diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 6c826d478df..7b2ec6fbc9a 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -30,6 +30,7 @@ class LibError(Exception): IS_PYODIDE = 'PYODIDE_ROOT' in os.environ and os.environ.get('_PYTHON_HOST_PLATFORM', '').startswith('emscripten') + # determine where binaries are RELEASE_DIR = os.environ.get('PACKAGE_FROM_RELEASE', None) if RELEASE_DIR is None: @@ -133,7 +134,8 @@ def _configure_z3(): # Config options cmake_options = { # Config Options - 'Z3_SINGLE_THREADED' : IS_SINGLE_THREADED, + 'Z3_SINGLE_THREADED' : IS_SINGLE_THREADED, # avoid solving features that use threads + 'Z3_POLING_TIMER' : IS_SINGLE_THREADED, # avoid using timer threads 'Z3_BUILD_PYTHON_BINDINGS' : True, # Build Options 'CMAKE_BUILD_TYPE' : 'Release', diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 0f952e016d7..5257a70b539 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -20,6 +20,7 @@ Module Name: #include "cmd_context/cmd_context.h" #include "solver/combined_solver.h" #include "solver/tactic2solver.h" +#include "tactic/tactical.h" #include "tactic/smtlogics/qfbv_tactic.h" #include "tactic/smtlogics/qflia_tactic.h" #include "tactic/smtlogics/qfnia_tactic.h" @@ -67,27 +68,27 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const else if (logic=="QF_BV") return mk_qfbv_tactic(m, p); else if (logic=="QF_IDL") - return mk_qfidl_tactic(m, p); + return annotate_tactic("qfidl-tactic", mk_qfidl_tactic(m, p)); else if (logic=="QF_LIA") - return mk_qflia_tactic(m, p); + return annotate_tactic("qflia-tactic", mk_qflia_tactic(m, p)); else if (logic=="QF_LRA") - return mk_qflra_tactic(m, p); + return annotate_tactic("qflra-tactic", mk_qflra_tactic(m, p)); else if (logic=="QF_NIA") - return mk_qfnia_tactic(m, p); + return annotate_tactic("qfnia-tactic", mk_qfnia_tactic(m, p)); else if (logic=="QF_NRA") - return mk_qfnra_tactic(m, p); + return annotate_tactic("qfnra-tactic", mk_qfnra_tactic(m, p)); else if (logic=="QF_AUFLIA") - return mk_qfauflia_tactic(m, p); + return annotate_tactic("qfauflia-tactic", mk_qfauflia_tactic(m, p)); else if (logic=="QF_AUFBV") - return mk_qfaufbv_tactic(m, p); + return annotate_tactic("qfaufbv-tactic", mk_qfaufbv_tactic(m, p)); else if (logic=="QF_ABV") - return mk_qfaufbv_tactic(m, p); + return annotate_tactic("qfaufbv-tactic", mk_qfaufbv_tactic(m, p)); else if (logic=="QF_UFBV") - return mk_qfufbv_tactic(m, p); + return annotate_tactic("qfufbv-tactic", mk_qfufbv_tactic(m, p)); else if (logic=="AUFLIA") - return mk_auflia_tactic(m, p); + return annotate_tactic("auflia-tactic", mk_auflia_tactic(m, p)); else if (logic=="AUFLIRA") - return mk_auflira_tactic(m, p); + return annotate_tactic("auflira-tactic", mk_auflira_tactic(m, p)); else if (logic=="AUFNIRA") return mk_aufnira_tactic(m, p); else if (logic=="UFNIA") @@ -101,7 +102,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const else if (logic=="LIA") return mk_lia_tactic(m, p); else if (logic=="UFBV") - return mk_ufbv_tactic(m, p); + return annotate_tactic("ufbv", mk_ufbv_tactic(m, p)); else if (logic=="BV") return mk_ufbv_tactic(m, p); else if (logic=="QF_FP") diff --git a/src/util/cancel_eh.h b/src/util/cancel_eh.h index 5ccf31636e3..d609b957a6f 100644 --- a/src/util/cancel_eh.h +++ b/src/util/cancel_eh.h @@ -25,11 +25,12 @@ Revision History: */ template class cancel_eh : public event_handler { - bool m_canceled; + bool m_canceled = false; + bool m_auto_cancel = false; T & m_obj; public: - cancel_eh(T & o): m_canceled(false), m_obj(o) {} - ~cancel_eh() override { if (m_canceled) m_obj.dec_cancel(); } + cancel_eh(T & o): m_obj(o) {} + ~cancel_eh() override { if (m_canceled) m_obj.dec_cancel(); if (m_auto_cancel) m_obj.auto_cancel(); } void operator()(event_handler_caller_t caller_id) override { if (!m_canceled) { m_caller_id = caller_id; @@ -39,5 +40,7 @@ class cancel_eh : public event_handler { } bool canceled() const { return m_canceled; } void reset() { m_canceled = false; } + T& t() { return m_obj; } + void set_auto_cancel() { m_auto_cancel = true; } }; diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index ea2e68b311b..28656bc63f1 100644 --- a/src/util/rlimit.cpp +++ b/src/util/rlimit.cpp @@ -31,11 +31,7 @@ void finalize_rlimit() { DEALLOC_MUTEX(g_rlimit_mux); } -reslimit::reslimit(): - m_cancel(0), - m_suspend(false), - m_count(0), - m_limit(std::numeric_limits::max()) { +reslimit::reslimit() { } uint64_t reslimit::count() const { @@ -117,7 +113,7 @@ void reslimit::reset_cancel() { void reslimit::inc_cancel() { lock_guard lock(*g_rlimit_mux); - set_cancel(m_cancel+1); + set_cancel(m_cancel + 1); } void reslimit::dec_cancel() { @@ -133,3 +129,39 @@ void reslimit::set_cancel(unsigned f) { m_children[i]->set_cancel(f); } } + + + +#ifdef POLLING_TIMER +void reslimit::push_timeout(unsigned ms) { + m_num_timers++; + if (m_cancel > 0) { + ++m_cancel; + return; + } + if (m_timeout_ms != 0) { + double ms_taken = 1000 * m_timer.get_seconds(); + if (ms_taken > m_timeout_ms) + return; + if (m_timeout_ms - ms_taken < ms) + return; + } + m_timer = timer(); + m_timeout_ms = ms; +} + +void reslimit::inc_cancel(unsigned k) { + lock_guard lock(*g_rlimit_mux); + set_cancel(m_cancel + k); +} + +void reslimit::auto_cancel() { + --m_num_timers; + dec_cancel(); +} + +#else +void reslimit::auto_cancel() { + UNREACHABLE(); +} +#endif \ No newline at end of file diff --git a/src/util/rlimit.h b/src/util/rlimit.h index 59bd818a2cc..c8688e4e2bb 100644 --- a/src/util/rlimit.h +++ b/src/util/rlimit.h @@ -19,6 +19,7 @@ Revision History: #pragma once #include "util/vector.h" +#include "util/timer.h" #include void initialize_rlimit(); @@ -29,16 +30,38 @@ void finalize_rlimit(); */ class reslimit { - std::atomic m_cancel; - bool m_suspend; - uint64_t m_count; - uint64_t m_limit; - svector m_limits; - ptr_vector m_children; + std::atomic m_cancel = 0; + bool m_suspend = false; + uint64_t m_count = 0; + uint64_t m_limit = std::numeric_limits::max(); +#ifdef POLLING_TIMER + timer m_timer; + unsigned m_timeout_ms = 0; + unsigned m_num_timers = 0; +#endif + svector m_limits; + ptr_vector m_children; + void set_cancel(unsigned f); friend class scoped_suspend_rlimit; +#ifdef POLLING_TIMER + bool is_timeout() { return m_timer.ms_timeout(m_timeout_ms) && (inc_cancel(m_num_timers), pop_timeout(), true); } + void inc_cancel(unsigned k); +#else + inline bool is_timeout() { return false; } +#endif + +#ifdef POLLING_TIMER + + void pop_timeout() { + m_timeout_ms = 0; + } + + void push_timeout(unsigned ms); +#endif + public: reslimit(); void push(unsigned delta_limit); @@ -52,15 +75,21 @@ class reslimit { uint64_t count() const; void reset_count() { m_count = 0; } - bool suspended() const { return m_suspend; } - inline bool not_canceled() const { return (m_cancel == 0 && m_count <= m_limit) || m_suspend; } - inline bool is_canceled() const { return !not_canceled(); } +#ifdef POLLING_TIMER + void set_timeout(unsigned ms) { push_timeout(ms); } +#endif + bool suspended() const { return m_suspend; } + inline bool not_canceled() { + return m_suspend || (m_cancel == 0 && m_count <= m_limit && !is_timeout()); + } + inline bool is_canceled() { return !not_canceled(); } char const* get_cancel_msg() const; void cancel(); void reset_cancel(); void inc_cancel(); void dec_cancel(); + void auto_cancel(); }; class scoped_rlimit { diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index ce1b14a23bd..4a62b928059 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -22,6 +22,8 @@ Revision History: #include "util/scoped_timer.h" #include "util/mutex.h" #include "util/util.h" +#include "util/cancel_eh.h" +#include "util/rlimit.h" #include #include #include @@ -79,6 +81,14 @@ scoped_timer::scoped_timer(unsigned ms, event_handler * eh) { if (ms == 0 || ms == UINT_MAX) return; +#ifdef POLLING_TIMER + auto* r = dynamic_cast*>(eh); + if (r) { + r->t().set_timeout(ms); + r->set_auto_cancel(); + return; + } +#endif workers.lock(); if (available_workers.empty()) { // start new thead