From 7a977f0106fe0ae07c90d1566a8a75e2d430f2f9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 Aug 2017 14:54:54 -0700 Subject: [PATCH] ensure that timeouts are distinguished from other cancel events #848 Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 2 +- src/api/api_solver.cpp | 8 ++++++++ src/solver/check_sat_result.cpp | 18 ++++++++++++++++++ src/solver/check_sat_result.h | 2 ++ src/solver/combined_solver.cpp | 4 ++-- src/util/cancel_eh.h | 10 +++++++--- src/util/event_handler.h | 14 +++++++++++++- src/util/scoped_ctrl_c.cpp | 2 +- src/util/scoped_timer.cpp | 2 +- src/util/timeout.cpp | 3 ++- 10 files changed, 55 insertions(+), 10 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 210e0a1d4..c99d3f0c8 100644 --- a/src/api/api_context.cpp +++ b/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(); } diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 7fd6d08fe..3a81080ed 100644 --- a/src/api/api_solver.cpp +++ b/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(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()); } diff --git a/src/solver/check_sat_result.cpp b/src/solver/check_sat_result.cpp index 5a7733071..f1bedfc08 100644 --- a/src/solver/check_sat_result.cpp +++ b/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) { diff --git a/src/solver/check_sat_result.h b/src/solver/check_sat_result.h index 3079433b5..38720a5e9 100644 --- a/src/solver/check_sat_result.h +++ b/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 & r) = 0; virtual ast_manager& get_manager() const = 0; diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 744ac494a..8f37224ad 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -89,8 +89,8 @@ private: m_solver->get_manager().limit().dec_cancel(); } } - virtual void operator()() { - m_canceled = true; + virtual void operator()(event_handler_caller_t caller_id) { + m_canceled = true; m_solver->get_manager().limit().inc_cancel(); } }; diff --git a/src/util/cancel_eh.h b/src/util/cancel_eh.h index 4347a5b52..59f11b3f3 100644 --- a/src/util/cancel_eh.h +++ b/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()() { - m_canceled = true; - m_obj.inc_cancel(); + virtual void operator()(event_handler_caller_t caller_id) { + if (!m_canceled) { + m_caller_id = caller_id; + m_canceled = true; + m_obj.inc_cancel(); + } } + bool canceled() const { return m_canceled; } }; #endif diff --git a/src/util/event_handler.h b/src/util/event_handler.h index 4b13f9c48..2a951c3ce 100644 --- a/src/util/event_handler.h +++ b/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 diff --git a/src/util/scoped_ctrl_c.cpp b/src/util/scoped_ctrl_c.cpp index 739eca295..1cb3a03c4 100644 --- a/src/util/scoped_ctrl_c.cpp +++ b/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 diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index 741523291..825b251c9 100644 --- a/src/util/scoped_timer.cpp +++ b/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__) diff --git a/src/util/timeout.cpp b/src/util/timeout.cpp index a82d1ec25..67995c2aa 100644 --- a/src/util/timeout.cpp +++ b/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)