mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-14 09:56:15 +00:00
Code Activity

stack

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-12-02 09:00:51 -08:00
parent bfd61fec00
commit 41aa7d7b60
2 changed files with 6 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/api/api_context.cpp
View file

@ -87,8 +87,6 @@ namespace api {
m_error_code = Z3_OK; m_error_code = Z3_OK;
m_print_mode = Z3_PRINT_SMTLIB_FULL; m_print_mode = Z3_PRINT_SMTLIB_FULL;
m_interruptable = nullptr;
m_error_handler = &default_error_handler; m_error_handler = &default_error_handler;
m_bv_fid = m().mk_family_id("bv"); m_bv_fid = m().mk_family_id("bv");
@ -98,7 +96,7 @@ namespace api {
m_datalog_fid = m().mk_family_id("datalog_relation"); m_datalog_fid = m().mk_family_id("datalog_relation");
m_fpa_fid = m().mk_family_id("fpa"); m_fpa_fid = m().mk_family_id("fpa");
m_seq_fid = m().mk_family_id("seq"); m_seq_fid = m().mk_family_id("seq");
m_char_fid = m().mk_family_id("char"); m_char_fid = m().mk_family_id("char");
m_special_relations_fid = m().mk_family_id("specrels"); m_special_relations_fid = m().mk_family_id("specrels");
m_dt_plugin = static_cast<datatype_decl_plugin*>(m().get_plugin(m_dt_fid)); m_dt_plugin = static_cast<datatype_decl_plugin*>(m().get_plugin(m_dt_fid));
@ -120,19 +118,18 @@ namespace api {
context::set_interruptable::set_interruptable(context & ctx, event_handler & i): context::set_interruptable::set_interruptable(context & ctx, event_handler & i):
m_ctx(ctx) { m_ctx(ctx) {
lock_guard lock(ctx.m_mux); lock_guard lock(ctx.m_mux);
SASSERT(m_ctx.m_interruptable == 0); m_ctx.m_interruptable.push_back(& i);
m_ctx.m_interruptable = &i;
} }
context::set_interruptable::~set_interruptable() { context::set_interruptable::~set_interruptable() {
lock_guard lock(m_ctx.m_mux); lock_guard lock(m_ctx.m_mux);
m_ctx.m_interruptable = nullptr; m_ctx.m_interruptable.pop_back();
} }
void context::interrupt() { void context::interrupt() {
lock_guard lock(m_mux); lock_guard lock(m_mux);
if (m_interruptable) for (auto * eh : m_interruptable)
(*m_interruptable)(API_INTERRUPT_EH_CALLER); (*eh)(API_INTERRUPT_EH_CALLER);
m_limit.cancel(); m_limit.cancel();
m().limit().cancel(); m().limit().cancel();
} }

2
src/api/api_context.h
View file

@ -115,7 +115,7 @@ namespace api {
std::string m_exception_msg; // catch the message associated with a Z3 exception std::string m_exception_msg; // catch the message associated with a Z3 exception
Z3_ast_print_mode m_print_mode; Z3_ast_print_mode m_print_mode;
event_handler * m_interruptable; // Reference to an object that can be interrupted by Z3_interrupt ptr_vector<event_handler> m_interruptable; // Reference to an object that can be interrupted by Z3_interrupt
public: public:
// Scoped obj for setting m_interruptable // Scoped obj for setting m_interruptable