Merge branch 'master' of https://github.com/z3prover/z3

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) {
+        dealloc(m_stopwatch);
-            m_stopwatch->stop();
+        m_stopwatch = nullptr;
-        }
         m_timelimit_ms = 0;
     }
 

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) {

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 <xmmintrin.h>
+#endif
 
 // define to update glue during propagation
 #define UPDATE_GLUE

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);
+                timeout = strtol(opt_arg, nullptr, 10);
-                set_timeout(tm * 1000);
             }
             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);
 }
 
 

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() {

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

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) {
+    static void thread_func(unsigned ms, event_handler * eh, std::timed_mutex * mutex) {
-        auto end = std::chrono::steady_clock::now() + std::chrono::milliseconds(st->m_ms);
+        auto end = std::chrono::steady_clock::now() + std::chrono::milliseconds(ms);
 
-        while (!st->m_mutex.try_lock_until(end)) {
+        while (!mutex->try_lock_until(end)) {
-          if (std::chrono::steady_clock::now() > end) {
+            if (std::chrono::steady_clock::now() >= end) {
-            st->m_eh->operator()(TIMEOUT_EH_CALLER);
+                eh->operator()(TIMEOUT_EH_CALLER);
-            return nullptr;
+                return;
-          }
+            }
         }
 
-        st->m_mutex.unlock();
+        mutex->unlock();
-        return nullptr;
     }
 
-    imp(unsigned ms, event_handler * eh):
+public:
-        m_eh(eh), m_ms(ms) {
+    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);
 }

src/util/stopwatch.h

@@ -20,171 +20,60 @@ Revision History:
 #ifndef STOPWATCH_H_
 #define STOPWATCH_H_
 
-#if defined(_WINDOWS) || defined(_CYGWIN) || defined(_MINGW)
+#include "util/debug.h"
-
+#include <chrono>
-// Does this redefinition work?
-
-#include <windows.h>
 
 class stopwatch
 {
-private:
+    typedef decltype(std::chrono::steady_clock::now()) clock_t;
-    LARGE_INTEGER m_elapsed;
+    typedef decltype(std::chrono::steady_clock::now() - std::chrono::steady_clock::now()) duration_t;
-    LARGE_INTEGER m_last_start_time;
+
-    LARGE_INTEGER m_last_stop_time;
+    clock_t m_start;
-    LARGE_INTEGER m_frequency;
+    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) {
-    
+        m_elapsed += s.m_elapsed;
-    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;
     }
 
-    double get_seconds() const { 
+    void reset() {
-        return static_cast<double>(m_elapsed.QuadPart / static_cast<double>(m_frequency.QuadPart)) ;
+        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<std::chrono::milliseconds>(m_elapsed).count() / 1000.0;
     }
 
     double get_current_seconds() const {
-        LARGE_INTEGER t;
+        return std::chrono::duration_cast<std::chrono::milliseconds>(get() - m_start).count() / 1000.0;
-        QueryPerformanceCounter(&t);
-        return static_cast<double>( (t.QuadPart - m_last_start_time.QuadPart) / static_cast<double>(m_frequency.QuadPart)); 
     }
 };
 
-#undef max
-#undef min
-
-
-#elif defined(__APPLE__) && defined (__MACH__) // macOS
-
-#include<mach/mach.h>
-#include<mach/clock.h>
-
-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<stopwatch*>(this)->stop(); 
-            /* update m_time */ 
-            const_cast<stopwatch*>(this)->start();
-        }
-        return static_cast<double>(m_time)/static_cast<double>(1000000000ull); 
-    }
-
-    double get_current_seconds() const { 
-        return get_seconds(); 
-    }
-};
-
-
-#else // Linux 
-
-#include<ctime>
-
-#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<stopwatch*>(this)->stop(); 
-            /* update m_time */ 
-            const_cast<stopwatch*>(this)->start();
-        }
-        return static_cast<double>(m_time)/static_cast<double>(1000000000ull); 
-    }
-
-    double get_current_seconds() const { 
-    return get_seconds(); 
-    }
-};
-
-#endif
 
 struct scoped_watch {
     stopwatch &m_sw;

src/util/timeout.cpp

@@ -19,7 +19,6 @@ Revision History:
 
 --*/
 #include<iostream>
-#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;
-            std::cout << "timeout\n";
+        if (g_on_timeout)
-            m_caller_id = caller_id;
+            g_on_timeout();
-            if (g_on_timeout)
+        throw z3_error(ERR_TIMEOUT);
-                g_on_timeout();
-            if (g_timeout) 
-                delete g_timeout;
-            g_timeout = nullptr;
-            throw z3_error(ERR_TIMEOUT);
-        }
     }
 };
 }
 
-void set_timeout(long ms) {
+static g_timeout_eh eh;
-    if (g_timeout) 
-        delete g_timeout;
 
-    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)()) {

src/util/timer.cpp

@@ -1,40 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    timer.cpp
-
-Abstract:
-
-    <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();
-}
-

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() {
-    ~timer();
+        m_watch.start();
-    void start();
+    }
-    double get_seconds();
+
-    bool timeout(unsigned secs) { return secs > 0 && secs != UINT_MAX && get_seconds() > secs; }
+    double get_seconds() const {
-    bool ms_timeout(unsigned ms) { return ms > 0 && ms != UINT_MAX && get_seconds() * 1000 > ms; }
+        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_ */
-