From ecba7b3cde4c1125ac1db63b7b7d63b299051b4a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Oct 2019 21:47:43 -0700 Subject: [PATCH] fix #1006 Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 33 +++++++++++++++++++++++++++++++-- src/api/api_solver.h | 14 +++++++++++--- src/api/z3_api.h | 12 ++++++++++++ 3 files changed, 54 insertions(+), 5 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index df77c5ed7..a26fff388 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -103,13 +103,23 @@ extern "C" { m_out.flush(); } - - solver2smt2_pp::solver2smt2_pp(ast_manager& m, char const* file): m_pp_util(m), m_out(file), m_tracked(m) { + solver2smt2_pp::solver2smt2_pp(ast_manager& m, char const* file): + m_pp_util(m), m_out(file), m_tracked(m) { if (!m_out) { throw default_exception("could not open " + std::string(file) + " for output"); } } + void Z3_solver_ref::set_eh(event_handler* eh) { + std::lock_guard lock(m_mux); + m_eh = eh; + } + + void Z3_solver_ref::set_cancel() { + std::lock_guard lock(m_mux); + if (m_eh) (*m_eh)(API_INTERRUPT_EH_CALLER); + } + void Z3_solver_ref::assert_expr(expr * e) { if (m_pp) m_pp->assert_expr(e); m_solver->assert_expr(e); @@ -386,6 +396,10 @@ extern "C" { Z3_CATCH; } + void Z3_API Z3_solver_interrupt(Z3_context c, Z3_solver s) { + to_solver(s)->set_cancel(); + } + void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n) { Z3_TRY; LOG_Z3_solver_pop(c, s, n); @@ -538,6 +552,7 @@ extern "C" { unsigned rlimit = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", true); cancel_eh eh(mk_c(c)->m().limit()); + to_solver(s)->set_eh(&eh); api::context::set_interruptable si(*(mk_c(c)), eh); lbool result; { @@ -550,12 +565,16 @@ extern "C" { } catch (z3_exception & ex) { to_solver_ref(s)->set_reason_unknown(eh); + to_solver(s)->set_eh(nullptr); if (!mk_c(c)->m().canceled()) { mk_c(c)->handle_exception(ex); } return Z3_L_UNDEF; } + catch (...) { + } } + to_solver(s)->set_eh(nullptr); if (result == l_undef) { to_solver_ref(s)->set_reason_unknown(eh); } @@ -730,6 +749,7 @@ extern "C" { unsigned rlimit = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", true); cancel_eh eh(mk_c(c)->m().limit()); + to_solver(s)->set_eh(&eh); api::context::set_interruptable si(*(mk_c(c)), eh); { scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); @@ -740,12 +760,16 @@ extern "C" { result = to_solver_ref(s)->get_consequences(_assumptions, _variables, _consequences); } catch (z3_exception & ex) { + to_solver(s)->set_eh(nullptr); to_solver_ref(s)->set_reason_unknown(eh); _assumptions.finalize(); _consequences.finalize(); _variables.finalize(); mk_c(c)->handle_exception(ex); return Z3_L_UNDEF; } + catch (...) { + } } + to_solver(s)->set_eh(nullptr); if (result == l_undef) { to_solver_ref(s)->set_reason_unknown(eh); } @@ -773,6 +797,7 @@ extern "C" { unsigned rlimit = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", true); cancel_eh eh(mk_c(c)->m().limit()); + to_solver(s)->set_eh(&eh); api::context::set_interruptable si(*(mk_c(c)), eh); { scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); @@ -782,10 +807,14 @@ extern "C" { result.append(to_solver_ref(s)->cube(vars, cutoff)); } catch (z3_exception & ex) { + to_solver(s)->set_eh(nullptr); mk_c(c)->handle_exception(ex); return nullptr; } + catch (...) { + } } + to_solver(s)->set_eh(nullptr); Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); mk_c(c)->save_object(v); for (expr* e : result) { diff --git a/src/api/api_solver.h b/src/api/api_solver.h index a49cb6706..519859cca 100644 --- a/src/api/api_solver.h +++ b/src/api/api_solver.h @@ -22,10 +22,11 @@ Revision History: #include "solver/solver.h" struct solver2smt2_pp { - ast_pp_util m_pp_util; - std::ofstream m_out; + ast_pp_util m_pp_util; + std::ofstream m_out; expr_ref_vector m_tracked; unsigned_vector m_tracked_lim; + solver2smt2_pp(ast_manager& m, char const* file); void assert_expr(expr* e); void assert_expr(expr* e, expr* t); @@ -34,6 +35,7 @@ struct solver2smt2_pp { void reset(); void check(unsigned n, expr* const* asms); void get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& variables); + }; struct Z3_solver_ref : public api::object { @@ -42,12 +44,18 @@ struct Z3_solver_ref : public api::object { params_ref m_params; symbol m_logic; scoped_ptr m_pp; + std::mutex m_mux; + event_handler* m_eh; + Z3_solver_ref(api::context& c, solver_factory * f): - api::object(c), m_solver_factory(f), m_solver(nullptr), m_logic(symbol::null) {} + api::object(c), m_solver_factory(f), m_solver(nullptr), m_logic(symbol::null), m_eh(nullptr) {} ~Z3_solver_ref() override {} void assert_expr(expr* e); void assert_expr(expr* e, expr* t); + void set_eh(event_handler* eh); + void set_cancel(); + }; inline Z3_solver_ref * to_solver(Z3_solver s) { return reinterpret_cast(s); } diff --git a/src/api/z3_api.h b/src/api/z3_api.h index ed3f4b50d..2209851fe 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6332,6 +6332,18 @@ extern "C" { */ void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s); + /** + \brief Solver local interrupt. + Normally you should use Z3_interrupt to cancel solvers because only + one solver is enabled concurrently per context. + However, per GitHub issue #1006, there are use cases where + it is more convenient to cancel a specific solver. Solvers + that are not selected for interrupts are left alone. + + def_API('Z3_solver_interrupt', VOID, (_in(CONTEXT), _in(SOLVER))) + */ + void Z3_API Z3_solver_interrupt(Z3_context c, Z3_solver s); + /** \brief Create a backtracking point.