ensure that timeouts are distinguished from other cancel events #848

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/api_context.cpp

@@ -142,7 +142,7 @@ namespace api {
         #pragma omp critical (set_interruptable)
         {
             if (m_interruptable)
-                (*m_interruptable)();
+                (*m_interruptable)(API_INTERRUPT_EH_CALLER);
             m_limit.cancel();
             m().limit().cancel();
         }

src/api/api_solver.cpp

@@ -296,10 +296,14 @@ extern "C" {
                 result = to_solver_ref(s)->check_sat(num_assumptions, _assumptions);
             }
             catch (z3_exception & ex) {
+                to_solver_ref(s)->set_reason_unknown(eh);
                 mk_c(c)->handle_exception(ex);
                 return Z3_L_UNDEF;
             }
         }
+        if (result == l_undef) {
+            to_solver_ref(s)->set_reason_unknown(eh);
+        }
         return static_cast<Z3_lbool>(result);
     }
     
@@ -466,10 +470,14 @@ extern "C" {
                 result = to_solver_ref(s)->get_consequences(_assumptions, _variables, _consequences);
             }
             catch (z3_exception & ex) {
+                to_solver_ref(s)->set_reason_unknown(eh);
                 mk_c(c)->handle_exception(ex);
                 return Z3_L_UNDEF;
             }
         }
+        if (result == l_undef) {
+            to_solver_ref(s)->set_reason_unknown(eh);
+        }
         for (unsigned i = 0; i < _consequences.size(); ++i) {
             to_ast_vector_ref(consequences).push_back(_consequences[i].get());
         }

src/solver/check_sat_result.cpp

@@ -18,6 +18,24 @@ Notes:
 --*/
 #include "solver/check_sat_result.h"
 
+void check_sat_result::set_reason_unknown(event_handler& eh) {
+    switch (eh.caller_id()) {
+    case UNSET_EH_CALLER: break;
+    case CTRL_C_EH_CALLER:
+        set_reason_unknown("interrupted from keyboard");
+        break;
+    case TIMEOUT_EH_CALLER:
+        set_reason_unknown("timeout");
+        break;
+    case RESLIMIT_EH_CALLER:
+        set_reason_unknown("max. resource limit exceeded");
+        break;
+    case API_INTERRUPT_EH_CALLER:
+        set_reason_unknown("interrupted");
+        break;
+    }
+}
+
 simple_check_sat_result::simple_check_sat_result(ast_manager & m):
     m_core(m),
     m_proof(m) {

src/solver/check_sat_result.h

@@ -22,6 +22,7 @@ Notes:
 #include "model/model.h"
 #include "util/lbool.h"
 #include "util/statistics.h"
+#include "util/event_handler.h"
 
 /**
    \brief Abstract interface for the result of a (check-sat) like command.
@@ -57,6 +58,7 @@ public:
     virtual proof * get_proof() = 0;
     virtual std::string reason_unknown() const = 0;
     virtual void set_reason_unknown(char const* msg) = 0;
+    void set_reason_unknown(event_handler& eh);
     virtual void get_labels(svector<symbol> & r) = 0;
     virtual ast_manager& get_manager() const = 0;
 

src/solver/combined_solver.cpp

@@ -89,8 +89,8 @@ private:
                 m_solver->get_manager().limit().dec_cancel();
             }
         }
-        virtual void operator()() {
+        virtual void operator()(event_handler_caller_t caller_id) {
-            m_canceled = true;
+            m_canceled = true;            
             m_solver->get_manager().limit().inc_cancel();
         }
     };

src/util/cancel_eh.h

@@ -31,10 +31,14 @@ class cancel_eh : public event_handler {
 public:
     cancel_eh(T & o): m_canceled(false), m_obj(o) {}
     ~cancel_eh() { if (m_canceled) m_obj.dec_cancel(); }
-    virtual void operator()() { 
+    virtual void operator()(event_handler_caller_t caller_id) {
-        m_canceled = true;
+        if (!m_canceled) {
-        m_obj.inc_cancel(); 
+            m_caller_id = caller_id;
+            m_canceled = true;
+            m_obj.inc_cancel(); 
+        }
     }
+    bool canceled() const { return m_canceled; }
 };
 
 #endif

src/util/event_handler.h

@@ -19,10 +19,22 @@ Revision History:
 #ifndef EVENT_HANDLER_H_
 #define EVENT_HANDLER_H_
 
+enum event_handler_caller_t {
+    UNSET_EH_CALLER,
+    CTRL_C_EH_CALLER,
+    TIMEOUT_EH_CALLER,
+    RESLIMIT_EH_CALLER,
+    API_INTERRUPT_EH_CALLER
+};
+
 class event_handler {
+protected:
+    event_handler_caller_t m_caller_id;
 public:
+    event_handler(): m_caller_id(UNSET_EH_CALLER) {}
     virtual ~event_handler() {}
-    virtual void operator()() = 0;
+    virtual void operator()(event_handler_caller_t caller_id) = 0;
+    event_handler_caller_t caller_id() const { return m_caller_id; }
 };
 
 #endif

src/util/scoped_ctrl_c.cpp

@@ -24,7 +24,7 @@ scoped_ctrl_c * scoped_ctrl_c::g_obj = 0;
 
 void scoped_ctrl_c::on_ctrl_c(int) {
     if (g_obj->m_first) {
-        g_obj->m_cancel_eh();
+        g_obj->m_cancel_eh(CTRL_C_EH_CALLER);
         if (g_obj->m_once) {
             g_obj->m_first = false;
             signal(SIGINT, on_ctrl_c); // re-install the handler

src/util/scoped_timer.cpp

@@ -85,7 +85,7 @@ struct scoped_timer::imp {
             obj->m_first = false;
         }
         else {
-            obj->m_eh->operator()();
+            obj->m_eh->operator()(TIMEOUT_EH_CALLER);
         }
     }
 #elif defined(__APPLE__) && defined(__MACH__)

src/util/timeout.cpp

@@ -32,10 +32,11 @@ void (* g_on_timeout)() = 0;
 
 class g_timeout_eh : public event_handler {
 public:
-    void operator()() {
+    void operator()(event_handler_caller_t caller_id) {
         #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)