diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp index 2b76d99f7..79508a4f6 100644 --- a/src/muz/rel/dl_instruction.cpp +++ b/src/muz/rel/dl_instruction.cpp @@ -41,7 +41,6 @@ namespace datalog { execution_context::~execution_context() { reset(); - dealloc(m_stopwatch); } void execution_context::reset() { @@ -104,15 +103,15 @@ namespace datalog { m_timelimit_ms = time_in_ms; if (!m_stopwatch) { m_stopwatch = alloc(stopwatch); + } else { + m_stopwatch->stop(); + m_stopwatch->reset(); } - m_stopwatch->stop(); - m_stopwatch->reset(); m_stopwatch->start(); } void execution_context::reset_timelimit() { - if (m_stopwatch) { - m_stopwatch->stop(); - } + dealloc(m_stopwatch); + m_stopwatch = nullptr; m_timelimit_ms = 0; } diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 7c3ebb688..cdb90e2a0 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -515,7 +515,6 @@ namespace sat { reinit(); DEBUG_CODE(verify_slack();); timer timer; - timer.start(); unsigned step = 0, total_flips = 0, tries = 0; for (tries = 1; !m_unsat_stack.empty() && m_limit.inc(); ++tries) { diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 4a0397cee..3669f801e 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -27,6 +27,9 @@ Revision History: #include "util/trace.h" #include "util/max_cliques.h" #include "util/gparams.h" +#ifdef _MSC_VER +# include +#endif // define to update glue during propagation #define UPDATE_GLUE diff --git a/src/shell/main.cpp b/src/shell/main.cpp index b036628b1..260cf8a79 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -115,6 +115,7 @@ void display_usage() { } void parse_cmd_line_args(int argc, char ** argv) { + long timeout = 0; int i = 1; char * eq_pos = nullptr; while (i < argc) { @@ -216,8 +217,7 @@ void parse_cmd_line_args(int argc, char ** argv) { else if (strcmp(opt_name, "T") == 0) { if (!opt_arg) error("option argument (-T:timeout) is missing."); - long tm = strtol(opt_arg, nullptr, 10); - set_timeout(tm * 1000); + timeout = strtol(opt_arg, nullptr, 10); } else if (strcmp(opt_name, "t") == 0) { if (!opt_arg) @@ -292,6 +292,9 @@ void parse_cmd_line_args(int argc, char ** argv) { } i++; } + + if (timeout) + set_timeout(timeout * 1000); } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 86b3374fc..ecb69b418 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3496,7 +3496,6 @@ namespace smt { m_case_split_queue ->init_search_eh(); m_next_progress_sample = 0; TRACE("literal_occ", display_literal_num_occs(tout);); - m_timer.start(); } void context::end_search() { diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index b6abb785f..5b1f336d1 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -56,7 +56,6 @@ z3_add_component(util symbol.cpp timeit.cpp timeout.cpp - timer.cpp trace.cpp util.cpp warning.cpp diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index e3b96fa15..58416289a 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -26,39 +26,33 @@ Revision History: struct scoped_timer::imp { - event_handler * m_eh; +private: std::thread m_thread; std::timed_mutex m_mutex; - unsigned m_ms; - static void* thread_func(imp * st) { - auto end = std::chrono::steady_clock::now() + std::chrono::milliseconds(st->m_ms); + static void thread_func(unsigned ms, event_handler * eh, std::timed_mutex * mutex) { + auto end = std::chrono::steady_clock::now() + std::chrono::milliseconds(ms); - while (!st->m_mutex.try_lock_until(end)) { - if (std::chrono::steady_clock::now() > end) { - st->m_eh->operator()(TIMEOUT_EH_CALLER); - return nullptr; - } + while (!mutex->try_lock_until(end)) { + if (std::chrono::steady_clock::now() >= end) { + eh->operator()(TIMEOUT_EH_CALLER); + return; + } } - st->m_mutex.unlock(); - return nullptr; + mutex->unlock(); } - imp(unsigned ms, event_handler * eh): - m_eh(eh), m_ms(ms) { +public: + imp(unsigned ms, event_handler * eh) { m_mutex.lock(); - m_thread = std::thread(thread_func, this); + m_thread = std::thread(thread_func, ms, eh, &m_mutex); } ~imp() { m_mutex.unlock(); - while (!m_thread.joinable()) { - std::this_thread::yield(); - } m_thread.join(); } - }; scoped_timer::scoped_timer(unsigned ms, event_handler * eh) { @@ -69,6 +63,5 @@ scoped_timer::scoped_timer(unsigned ms, event_handler * eh) { } scoped_timer::~scoped_timer() { - if (m_imp) - dealloc(m_imp); + dealloc(m_imp); } diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index a11a87484..1135c893e 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -20,171 +20,60 @@ Revision History: #ifndef STOPWATCH_H_ #define STOPWATCH_H_ -#if defined(_WINDOWS) || defined(_CYGWIN) || defined(_MINGW) - -// Does this redefinition work? - -#include +#include "util/debug.h" +#include class stopwatch { -private: - LARGE_INTEGER m_elapsed; - LARGE_INTEGER m_last_start_time; - LARGE_INTEGER m_last_stop_time; - LARGE_INTEGER m_frequency; + typedef decltype(std::chrono::steady_clock::now()) clock_t; + typedef decltype(std::chrono::steady_clock::now() - std::chrono::steady_clock::now()) duration_t; + + clock_t m_start; + duration_t m_elapsed; +#if Z3DEBUG + bool m_running = false; +#endif + + // FIXME: just use auto with VS 2015+ + static clock_t get() { + return std::chrono::steady_clock::now(); + } public: stopwatch() { - QueryPerformanceFrequency(&m_frequency); - reset(); + reset(); } - ~stopwatch() {}; - - void add (const stopwatch &s) {/* TODO */} - - void reset() { m_elapsed.QuadPart = 0; } - - void start() { - QueryPerformanceCounter(&m_last_start_time); - } - - void stop() { - QueryPerformanceCounter(&m_last_stop_time); - m_elapsed.QuadPart += m_last_stop_time.QuadPart - m_last_start_time.QuadPart; + void add(const stopwatch &s) { + m_elapsed += s.m_elapsed; } - double get_seconds() const { - return static_cast(m_elapsed.QuadPart / static_cast(m_frequency.QuadPart)) ; + void reset() { + m_elapsed = duration_t::zero(); + DEBUG_CODE(m_running = false;); + } + + void start() { + SASSERT(!m_running); + DEBUG_CODE(m_running = true;); + m_start = get(); + } + + void stop() { + SASSERT(m_running); + DEBUG_CODE(m_running = false;); + m_elapsed += get() - m_start; + } + + double get_seconds() const { + return std::chrono::duration_cast(m_elapsed).count() / 1000.0; } double get_current_seconds() const { - LARGE_INTEGER t; - QueryPerformanceCounter(&t); - return static_cast( (t.QuadPart - m_last_start_time.QuadPart) / static_cast(m_frequency.QuadPart)); + return std::chrono::duration_cast(get() - m_start).count() / 1000.0; } }; -#undef max -#undef min - - -#elif defined(__APPLE__) && defined (__MACH__) // macOS - -#include -#include - -class stopwatch { - unsigned long long m_time; // elapsed time in ns - bool m_running; - clock_serv_t m_host_clock; - mach_timespec_t m_start; - -public: - stopwatch():m_time(0), m_running(false) { - host_get_clock_service(mach_host_self(), SYSTEM_CLOCK, &m_host_clock); - } - - ~stopwatch() {} - - void add (const stopwatch &s) {m_time += s.m_time;} - - void reset() { - m_time = 0ull; - } - - void start() { - if (!m_running) { - clock_get_time(m_host_clock, &m_start); - m_running = true; - } - } - - void stop() { - if (m_running) { - mach_timespec_t _stop; - clock_get_time(m_host_clock, &_stop); - m_time += (_stop.tv_sec - m_start.tv_sec) * 1000000000ull; - m_time += (_stop.tv_nsec - m_start.tv_nsec); - m_running = false; - } - } - - double get_seconds() const { - if (m_running) { - const_cast(this)->stop(); - /* update m_time */ - const_cast(this)->start(); - } - return static_cast(m_time)/static_cast(1000000000ull); - } - - double get_current_seconds() const { - return get_seconds(); - } -}; - - -#else // Linux - -#include - -#ifndef CLOCK_PROCESS_CPUTIME_ID -/* BSD */ -# define CLOCK_PROCESS_CPUTIME_ID CLOCK_MONOTONIC -#endif - -class stopwatch { - unsigned long long m_time; // elapsed time in ns - bool m_running; - struct timespec m_start; - -public: - stopwatch():m_time(0), m_running(false) { - } - - ~stopwatch() {} - - void add (const stopwatch &s) {m_time += s.m_time;} - - void reset() { - m_time = 0ull; - } - - void start() { - if (!m_running) { - clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &m_start); - m_running = true; - } - } - - void stop() { - if (m_running) { - struct timespec _stop; - clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &_stop); - m_time += (_stop.tv_sec - m_start.tv_sec) * 1000000000ull; - if (m_time != 0 || _stop.tv_nsec >= m_start.tv_nsec) - m_time += (_stop.tv_nsec - m_start.tv_nsec); - m_running = false; - } - } - - double get_seconds() const { - if (m_running) { - const_cast(this)->stop(); - /* update m_time */ - const_cast(this)->start(); - } - return static_cast(m_time)/static_cast(1000000000ull); - } - - double get_current_seconds() const { - return get_seconds(); - } -}; - -#endif struct scoped_watch { stopwatch &m_sw; diff --git a/src/util/timeout.cpp b/src/util/timeout.cpp index ad02a747d..1a92ae867 100644 --- a/src/util/timeout.cpp +++ b/src/util/timeout.cpp @@ -19,7 +19,6 @@ Revision History: --*/ #include -#include "util/z3_omp.h" #include "util/util.h" #include "util/timeout.h" #include "util/error_codes.h" @@ -34,26 +33,21 @@ namespace { class g_timeout_eh : public event_handler { public: void operator()(event_handler_caller_t caller_id) override { - #pragma omp critical (g_timeout_cs) - { - std::cout << "timeout\n"; - m_caller_id = caller_id; - if (g_on_timeout) - g_on_timeout(); - if (g_timeout) - delete g_timeout; - g_timeout = nullptr; - throw z3_error(ERR_TIMEOUT); - } + std::cout << "timeout\n"; + m_caller_id = caller_id; + if (g_on_timeout) + g_on_timeout(); + throw z3_error(ERR_TIMEOUT); } }; } -void set_timeout(long ms) { - if (g_timeout) - delete g_timeout; +static g_timeout_eh eh; - g_timeout = new scoped_timer(ms, new g_timeout_eh()); +void set_timeout(long ms) { + SASSERT(!g_timeout); + // this is leaked, but since it's only used in the shell, it's ok + g_timeout = new scoped_timer(ms, &eh); } void register_on_timeout_proc(void (*proc)()) { diff --git a/src/util/timer.cpp b/src/util/timer.cpp deleted file mode 100644 index 2d80b732c..000000000 --- a/src/util/timer.cpp +++ /dev/null @@ -1,40 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - timer.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2009-01-06. - -Revision History: - ---*/ -#include "util/util.h" -#include "util/memory_manager.h" -#include "util/stopwatch.h" -#include "util/timer.h" - -timer::timer(){ - m_watch = alloc(stopwatch); - start(); -} - -timer::~timer() { - dealloc(m_watch); -} - -void timer::start() { - m_watch->start(); -} - -double timer::get_seconds() { - return m_watch->get_current_seconds(); -} - diff --git a/src/util/timer.h b/src/util/timer.h index b4a69f8bf..e2ddb55e7 100644 --- a/src/util/timer.h +++ b/src/util/timer.h @@ -19,21 +19,29 @@ Revision History: #ifndef TIMER_H_ #define TIMER_H_ -class stopwatch; +#include "util/stopwatch.h" /** - \brief Wrapper for the stopwatch class. It hides windows.h dependency. + \brief Wrapper for the stopwatch class. */ class timer { - stopwatch * m_watch; + stopwatch m_watch; public: - timer(); - ~timer(); - void start(); - double get_seconds(); - bool timeout(unsigned secs) { return secs > 0 && secs != UINT_MAX && get_seconds() > secs; } - bool ms_timeout(unsigned ms) { return ms > 0 && ms != UINT_MAX && get_seconds() * 1000 > ms; } + timer() { + m_watch.start(); + } + + double get_seconds() const { + return m_watch.get_current_seconds(); + } + + bool timeout(unsigned secs) const { + return secs != 0 && secs != UINT_MAX && get_seconds() > secs; + } + + bool ms_timeout(unsigned ms) const { + return ms != 0 && ms != UINT_MAX && get_seconds() * 1000 > ms; + } }; #endif /* TIMER_H_ */ -