diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 99d332724..948064af6 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -883,8 +883,8 @@ extern "C" { Z3_TRY; RESET_ERROR_CODE(); init_solver(c, s); - user_propagator::push_eh_t _push = push_eh; - user_propagator::pop_eh_t _pop = pop_eh; + user_propagator::push_eh_t _push = (void(*)(void*,user_propagator::callback*)) push_eh; + user_propagator::pop_eh_t _pop = (void(*)(void*,user_propagator::callback*,unsigned)) pop_eh; user_propagator::fresh_eh_t _fresh = [=](void * user_ctx, ast_manager& m, user_propagator::context_obj*& _ctx) { ast_context_params params; params.set_foreign_manager(&m); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 4d60de433..101fa04a3 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -3964,18 +3964,23 @@ namespace z3 { } }; - static void push_eh(void* p) { + static void push_eh(void* _p, Z3_solver_callback cb) { + user_propagator_base* p = static_cast(_p); + scoped_cb _cb(p, cb); static_cast(p)->push(); } - static void pop_eh(void* p, unsigned num_scopes) { - static_cast(p)->pop(num_scopes); + static void pop_eh(void* _p, Z3_solver_callback cb, unsigned num_scopes) { + user_propagator_base* p = static_cast(_p); + scoped_cb _cb(p, cb); + static_cast(_p)->pop(num_scopes); } - static void* fresh_eh(void* p, Z3_context ctx) { + static void* fresh_eh(void* _p, Z3_context ctx) { + user_propagator_base* p = static_cast(_p); context* c = new context(ctx); - static_cast(p)->subcontexts.push_back(c); - return static_cast(p)->fresh(*c); + p->subcontexts.push_back(c); + return p->fresh(*c); } static void fixed_eh(void* _p, Z3_solver_callback cb, Z3_ast _var, Z3_ast _value) { diff --git a/src/api/z3_api.h b/src/api/z3_api.h index d7dd0a332..8a610bc6d 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1434,8 +1434,8 @@ Z3_DECLARE_CLOSURE(Z3_error_handler, void, (Z3_context c, Z3_error_code e)); /** \brief callback functions for user propagator. */ -Z3_DECLARE_CLOSURE(Z3_push_eh, void, (void* ctx)); -Z3_DECLARE_CLOSURE(Z3_pop_eh, void, (void* ctx, unsigned num_scopes)); +Z3_DECLARE_CLOSURE(Z3_push_eh, void, (void* ctx, Z3_solver_callback cb)); +Z3_DECLARE_CLOSURE(Z3_pop_eh, void, (void* ctx, Z3_solver_callback cb, unsigned num_scopes)); Z3_DECLARE_CLOSURE(Z3_fresh_eh, void*, (void* ctx, Z3_context new_context)); Z3_DECLARE_CLOSURE(Z3_fixed_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast t, Z3_ast value)); Z3_DECLARE_CLOSURE(Z3_eq_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast s, Z3_ast t)); diff --git a/src/sat/smt/user_solver.cpp b/src/sat/smt/user_solver.cpp index 6b3eb6718..d24af253e 100644 --- a/src/sat/smt/user_solver.cpp +++ b/src/sat/smt/user_solver.cpp @@ -88,7 +88,7 @@ namespace user_solver { void solver::push_core() { th_euf_solver::push_core(); m_prop_lim.push_back(m_prop.size()); - m_push_eh(m_user_context); + m_push_eh(m_user_context, this); } void solver::pop_core(unsigned num_scopes) { @@ -96,7 +96,7 @@ namespace user_solver { unsigned old_sz = m_prop_lim.size() - num_scopes; m_prop.shrink(m_prop_lim[old_sz]); m_prop_lim.shrink(old_sz); - m_pop_eh(m_user_context, num_scopes); + m_pop_eh(m_user_context, this, num_scopes); } void solver::propagate_consequence(prop_info const& prop) { diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index 7c53aa8eb..daded32c7 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -25,6 +25,7 @@ using namespace smt; theory_user_propagator::theory_user_propagator(context& ctx): theory(ctx, ctx.get_manager().mk_family_id(user_propagator::plugin::name())), m_var2expr(ctx.get_manager()), + m_push_popping(false), m_to_add(ctx.get_manager()) {} @@ -38,7 +39,7 @@ void theory_user_propagator::force_push() { theory::push_scope_eh(); m_prop_lim.push_back(m_prop.size()); m_to_add_lim.push_back(m_to_add.size()); - m_push_eh(m_user_context); + m_push_eh(m_user_context, this); } } @@ -122,7 +123,8 @@ final_check_status theory_user_propagator::final_check_eh() { if (!(bool)m_final_eh) return FC_DONE; force_push(); - unsigned sz = m_prop.size(); + unsigned sz1 = m_prop.size(); + unsigned sz2 = m_expr2var.size(); try { m_final_eh(m_user_context, this); } @@ -130,7 +132,8 @@ final_check_status theory_user_propagator::final_check_eh() { throw default_exception("Exception thrown in \"final\"-callback"); } propagate(); - bool done = (sz == m_prop.size()) && !ctx.inconsistent(); + // check if it became inconsistent or something new was propagated/registered + bool done = !can_propagate() && !ctx.inconsistent(); return done ? FC_DONE : FC_CONTINUE; } @@ -169,11 +172,11 @@ void theory_user_propagator::pop_scope_eh(unsigned num_scopes) { old_sz = m_to_add_lim.size() - num_scopes; m_to_add.shrink(m_to_add_lim[old_sz]); m_to_add_lim.shrink(old_sz); - m_pop_eh(m_user_context, num_scopes); + m_pop_eh(m_user_context, this, num_scopes); } bool theory_user_propagator::can_propagate() { - return m_qhead < m_prop.size() || !m_to_add.empty(); + return m_qhead < m_prop.size() || m_to_add_qhead < m_to_add.size(); } void theory_user_propagator::propagate_consequence(prop_info const& prop) { diff --git a/src/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h index 07270ffe6..02a027762 100644 --- a/src/tactic/user_propagator_base.h +++ b/src/tactic/user_propagator_base.h @@ -17,13 +17,13 @@ namespace user_propagator { virtual ~context_obj() = default; }; - typedef std::function final_eh_t; - typedef std::function fixed_eh_t; - typedef std::function eq_eh_t; + typedef std::function final_eh_t; + typedef std::function fixed_eh_t; + typedef std::function eq_eh_t; typedef std::function fresh_eh_t; - typedef std::function push_eh_t; - typedef std::function pop_eh_t; - typedef std::function created_eh_t; + typedef std::function push_eh_t; + typedef std::function pop_eh_t; + typedef std::function created_eh_t; class plugin : public decl_plugin {