From 96f10b8c1cb83f3434bc12cf03560a6d2d2953ce Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 Aug 2020 19:00:58 -0700 Subject: [PATCH] user propagator Signed-off-by: Nikolaj Bjorner --- scripts/update_api.py | 2 +- src/api/api_context.cpp | 2 + src/api/api_solver.cpp | 18 +++-- src/api/python/z3/z3.py | 106 +++++++++++++++++++++-------- src/api/z3_api.h | 6 +- src/cmd_context/context_params.cpp | 15 +--- src/cmd_context/context_params.h | 31 +++++---- src/smt/smt_context.cpp | 26 +++++-- src/smt/smt_context.h | 10 +-- src/smt/smt_kernel.cpp | 16 ++--- src/smt/smt_kernel.h | 6 +- src/smt/smt_solver.cpp | 2 +- src/smt/user_propagator.cpp | 28 +++++--- src/smt/user_propagator.h | 56 +++++++++------ src/solver/solver.h | 22 +++--- 15 files changed, 219 insertions(+), 127 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 665b3f01e9a..db1bf9db500 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1843,7 +1843,7 @@ def _to_pystr(s): push_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p) pop_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint) -fresh_eh_type = ctypes.CFUNCTYPE(ctypes.c_void_p, ctypes.c_void_p) +fresh_eh_type = ctypes.CFUNCTYPE(ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p) fixed_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint, ctypes.c_void_p) final_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 48882827609..f113744b495 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -116,6 +116,8 @@ namespace api { DEBUG_CODE(warning_msg("Uncollected memory: %d: %s", kv.m_key, typeid(*val).name());); dealloc(val); } + if (m_params.owns_manager()) + m_manager.detach(); } context::set_interruptable::set_interruptable(context & ctx, event_handler & i): diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 8c1dbe4e348..08de8ec388f 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -896,9 +896,15 @@ extern "C" { Z3_TRY; RESET_ERROR_CODE(); init_solver(c, s); - std::function _push = push_eh; - std::function _pop = pop_eh; - std::function _fresh = fresh_eh; + solver::push_eh_t _push = push_eh; + solver::pop_eh_t _pop = pop_eh; + solver::fresh_eh_t _fresh = [&](void * user_ctx, ast_manager& m, void*& _ctx) { + context_params params; + params.set_foreign_manager(&m); + auto* ctx = reinterpret_cast(alloc(api::context, ¶ms, false)); + _ctx = ctx; + return fresh_eh(user_ctx, ctx); + }; to_solver_ref(s)->user_propagate_init(user_context, _push, _pop, _fresh); Z3_CATCH; } @@ -955,11 +961,11 @@ extern "C" { Z3_CATCH_RETURN(0); } - void Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback s, unsigned sz, unsigned const* ids, Z3_ast conseq) { + void Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback s, unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, Z3_ast conseq) { Z3_TRY; - LOG_Z3_solver_propagate_consequence(c, s, sz, ids, conseq); + LOG_Z3_solver_propagate_consequence(c, s, num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, conseq); RESET_ERROR_CODE(); - reinterpret_cast(s)->propagate(sz, ids, to_expr(conseq)); + reinterpret_cast(s)->propagate(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, to_expr(conseq)); Z3_CATCH; } diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index eb40dff95bf..910d89573be 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -10506,30 +10506,39 @@ def TransitiveClosure(f): class PropClosures: -# import thread def __init__(self): self.bases = {} -# self.lock = thread.Lock() + self.lock = None + + def set_threaded(): + if self.lock is None: + import threading + self.lock = threading.thread.Lock() def get(self, ctx): -# self.lock.acquire() + if self.lock: self.lock.acquire() r = self.bases[ctx] -# self.lock.release() + if self.lock: self.lock.release() return r def set(self, ctx, r): -# self.lock.acquire() + if self.lock: self.lock.acquire() self.bases[ctx] = r -# self.lock.release() + if self.lock: self.lock.release() def insert(self, r): -# self.lock.acquire() + if self.lock: self.lock.acquire() id = len(self.bases) + 3 self.bases[id] = r -# self.lock.release() + if self.lock: self.lock.release() return id -_prop_closures = PropClosures() +_prop_closures = None + +def ensure_prop_closures(): + global _prop_closures + if _prop_closures is None: + _prop_closures = PropClosures() def user_prop_push(ctx): _prop_closures.get(ctx).push(); @@ -10537,9 +10546,10 @@ def user_prop_push(ctx): def user_prop_pop(ctx, num_scopes): _prop_closures.get(ctx).pop(num_scopes) -def user_prop_fresh(ctx): - prop = _prop_closures.get(ctx) - new_prop = UsePropagateBase(None, prop.ctx) +def user_prop_fresh(id, ctx): + prop = _prop_closures.get(id) + _prop_closures.set_threaded() + new_prop = UsePropagateBase(None, ctx) _prop_closures.set(new_prop.id, new_prop.fresh()) return ctypes.c_void_p(new_prop.id) @@ -10577,66 +10587,104 @@ def user_prop_diseq(ctx, cb, x, y): class UserPropagateBase: + # + # Either solver is set or ctx is set. + # Propagators that are created throuh callbacks + # to "fresh" inherit the context of that is supplied + # as argument to the callback. + # This context should not be deleted. It is owned by the solver. + # def __init__(self, s, ctx = None): + assert s is None or ctx is None + ensure_prop_closures() self.solver = s - self.ctx = s.ctx if s is not None else ctx + self._ctx = None self.cb = None self.id = _prop_closures.insert(self) self.fixed = None self.final = None self.eq = None self.diseq = None + if ctx: + self._ctx = Context() + Z3_del_context(self._ctx.ctx) + self._ctx.ctx = ctx + self._ctx.eh = Z3_set_error_handler(ctx, z3_error_handler) + Z3_set_ast_print_mode(ctx, Z3_PRINT_SMTLIB2_COMPLIANT) if s: - Z3_solver_propagate_init(s.ctx.ref(), + Z3_solver_propagate_init(self.ctx_ref(), s.solver, ctypes.c_void_p(self.id), _user_prop_push, _user_prop_pop, _user_prop_fresh) - + + def __del__(self): + if self._ctx: + self._ctx.ctx = None + + def ctx(self): + if self._ctx: + return self._ctx + else: + return self.solver.ctx + def ctx_ref(self): + return self.ctx().ref() + def add_fixed(self, fixed): assert not self.fixed - Z3_solver_propagate_fixed(self.ctx.ref(), self.solver.solver, _user_prop_fixed) + assert not self._ctx + Z3_solver_propagate_fixed(self.ctx_ref(), self.solver.solver, _user_prop_fixed) self.fixed = fixed def add_final(self, final): assert not self.final - Z3_solver_propagate_final(self.ctx.ref(), self.solver.solver, _user_prop_final) + assert not self._ctx + Z3_solver_propagate_final(self.ctx_ref(), self.solver.solver, _user_prop_final) self.final = final def add_eq(self, eq): assert not self.eq - Z3_solver_propagate_eq(self.ctx.ref(), self.solver.solver, _user_prop_eq) + assert not self._ctx + Z3_solver_propagate_eq(self.ctx_ref(), self.solver.solver, _user_prop_eq) self.eq = eq def add_diseq(self, diseq): assert not self.diseq - Z3_solver_propagate_diseq(self.ctx.ref(), self.solver.solver, _user_prop_diseq) + assert not self._ctx + Z3_solver_propagate_diseq(self.ctx_ref(), self.solver.solver, _user_prop_diseq) self.diseq = diseq def push(self): - raise Z3Exception("push has not been overwritten") + raise Z3Exception("push needs to be overwritten") def pop(self, num_scopes): - raise Z3Exception("pop has not been overwritten") + raise Z3Exception("pop needs to be overwritten") def fresh(self): - raise Z3Exception("fresh has not been overwritten") + raise Z3Exception("fresh needs to be overwritten") def add(self, e): assert self.solver - return Z3_solver_propagate_register(self.ctx.ref(), self.solver.solver, e.ast) + assert not self._ctx + return Z3_solver_propagate_register(self.ctx_ref(), self.solver.solver, e.ast) # # Propagation can only be invoked as during a fixed-callback. # - def propagate(self, ids, e): - sz = len(ids) - _ids = (ctypes.c_uint * sz)() - for i in range(sz): + def propagate(self, e, ids, eqs = []): + num_fixed = len(ids) + _ids = (ctypes.c_uint * num_fixed)() + for i in range(num_fixed): _ids[i] = ids[i] - Z3_solver_propagate_consequence(self.ctx.ref(), ctypes.c_void_p(self.cb), sz, _ids, e.ast) + num_eqs = len(eqs) + _lhs = (ctypes.c_uint * num_eqs)() + _rhs = (ctypes.c_uint * num_eqs)() + for i in range(num_eqs): + _lhs[i] = eqs[i][0] + _rhs[i] = eqs[i][1] + Z3_solver_propagate_consequence(self.ctx_ref(), ctypes.c_void_p(self.cb), num_fixed, _ids, num_eqs, _lhs, _rhs, e.ast) def conflict(self, ids): - self.propagate(ids, BoolVal(False, self.ctx)) + self.propagate(ids, BoolVal(False, self.ctx_ref())) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 0d15adba58d..fbe7eb40f8d 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1420,7 +1420,7 @@ typedef void Z3_error_handler(Z3_context c, Z3_error_code e); */ typedef void Z3_push_eh(void* ctx); typedef void Z3_pop_eh(void* ctx, unsigned num_scopes); -typedef void* Z3_fresh_eh(void* ctx); +typedef void* Z3_fresh_eh(void* ctx, Z3_context new_context); typedef void Z3_fixed_eh(void* ctx, Z3_solver_callback cb, unsigned id, Z3_ast value); typedef void Z3_eq_eh(void* ctx, Z3_solver_callback cb, unsigned x, unsigned y); typedef void Z3_final_eh(void* ctx, Z3_solver_callback cb); @@ -6586,10 +6586,10 @@ extern "C" { The callback adds a propagation consequence based on the fixed values of the \c ids. - def_API('Z3_solver_propagate_consequence', VOID, (_in(CONTEXT), _in(SOLVER_CALLBACK), _in(UINT), _in_array(2, UINT), _in(AST))) + def_API('Z3_solver_propagate_consequence', VOID, (_in(CONTEXT), _in(SOLVER_CALLBACK), _in(UINT), _in_array(2, UINT), _in(UINT), _in_array(4, UINT), _in_array(4, UINT), _in(AST))) */ - void Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback, unsigned sz, unsigned const* ids, Z3_ast conseq); + void Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback, unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, Z3_ast conseq); /** \brief Check whether the assertions in a given solver are consistent or not. diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp index 6289d33c5cf..7f022f5336c 100644 --- a/src/cmd_context/context_params.cpp +++ b/src/cmd_context/context_params.cpp @@ -24,19 +24,6 @@ Module Name: #include "solver/solver.h" context_params::context_params() { - m_unsat_core = false; - m_model = true; - m_model_validate = false; - m_dump_models = false; - m_auto_config = true; - m_proof = false; - m_trace = false; - m_debug_ref_count = false; - m_smtlib2_compliant = false; - m_well_sorted_check = false; - m_timeout = UINT_MAX; - m_rlimit = 0; - m_statistics = false; updt_params(); } @@ -204,6 +191,8 @@ void context_params::get_solver_params(ast_manager const & m, params_ref & p, bo } ast_manager * context_params::mk_ast_manager() { + if (m_manager) + return m_manager; ast_manager * r = alloc(ast_manager, m_proof ? PGM_ENABLED : PGM_DISABLED, m_trace ? m_trace_file_name.c_str() : nullptr); diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h index 50332ff9bc5..acf72f82348 100644 --- a/src/cmd_context/context_params.h +++ b/src/cmd_context/context_params.h @@ -26,24 +26,24 @@ class context_params { void set_bool(bool & opt, char const * param, char const * value); void set_uint(unsigned & opt, char const * param, char const * value); - unsigned m_rlimit; + unsigned m_rlimit { 0 }; + ast_manager* m_manager { nullptr }; public: - bool m_auto_config; - bool m_proof; + bool m_auto_config { true }; + bool m_proof { false }; std::string m_dot_proof_file; - bool m_interpolants; - bool m_debug_ref_count; - bool m_trace; + bool m_debug_ref_count { false }; + bool m_trace { false }; std::string m_trace_file_name; - bool m_well_sorted_check; - bool m_model; - bool m_model_validate; - bool m_dump_models; - bool m_unsat_core; - bool m_smtlib2_compliant; // it must be here because it enable/disable the use of coercions in the ast_manager. - unsigned m_timeout; - bool m_statistics; + bool m_well_sorted_check { false }; + bool m_model { true }; + bool m_model_validate { false }; + bool m_dump_models { false }; + bool m_unsat_core { false }; + bool m_smtlib2_compliant { false }; // it must be here because it enable/disable the use of coercions in the ast_manager. + unsigned m_timeout { UINT_MAX } ; + bool m_statistics { false }; unsigned rlimit() const { return m_rlimit; } context_params(); @@ -74,6 +74,9 @@ class context_params { \brief Create an AST manager using this configuration. */ ast_manager * mk_ast_manager(); + + void set_foreign_manager(ast_manager* m) { m_manager = m; } + bool owns_manager() const { return m_manager != nullptr; } }; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index a354e150741..a215fb6ef69 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -183,13 +183,14 @@ namespace smt { dst_ctx.setup_context(dst_ctx.m_fparams.m_auto_config); dst_ctx.internalize_assertions(); + + dst_ctx.copy_user_propagator(src_ctx); TRACE("smt_context", src_ctx.display(tout); dst_ctx.display(tout);); } - context::~context() { flush(); m_asserted_formulas.finalize(); @@ -205,6 +206,19 @@ namespace smt { } } + void context::copy_user_propagator(context& src_ctx) { + if (!src_ctx.m_user_propagator) + return; + ast_translation tr(src_ctx.m, m, false); + auto* p = get_theory(m.mk_family_id("user_propagator")); + m_user_propagator = reinterpret_cast(p); + SASSERT(m_user_propagator); + for (unsigned i = 0; i < src_ctx.m_user_propagator->get_num_vars(); ++i) { + app* e = src_ctx.m_user_propagator->get_expr(i); + m_user_propagator->add_expr(tr(e)); + } + } + context * context::mk_fresh(symbol const * l, smt_params * p, params_ref const& pa) { context * new_ctx = alloc(context, m, p ? *p : m_fparams, pa); new_ctx->m_is_auxiliary = true; @@ -2950,10 +2964,10 @@ namespace smt { } void context::user_propagate_init( - void* ctx, - std::function& push_eh, - std::function& pop_eh, - std::function& fresh_eh) { + void* ctx, + solver::push_eh_t& push_eh, + solver::pop_eh_t& pop_eh, + solver::fresh_eh_t& fresh_eh) { setup_context(m_fparams.m_auto_config); m_user_propagator = alloc(user_propagator, *this); m_user_propagator->add(ctx, push_eh, pop_eh, fresh_eh); @@ -2963,7 +2977,7 @@ namespace smt { } bool context::watches_fixed(enode* n) const { - return m_user_propagator && n->get_th_var(m_user_propagator->get_family_id()) != null_theory_var; + return m_user_propagator && m_user_propagator->has_fixed() && n->get_th_var(m_user_propagator->get_family_id()) != null_theory_var; } void context::assign_fixed(enode* n, expr* val, unsigned sz, literal const* explain) { diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 8f6d0a6a698..3b566b905d7 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1573,6 +1573,8 @@ namespace smt { void log_stats(); + void copy_user_propagator(context& src); + public: context(ast_manager & m, smt_params & fp, params_ref const & p = params_ref()); @@ -1688,10 +1690,10 @@ namespace smt { * user-propagator */ void user_propagate_init( - void* ctx, - std::function& push_eh, - std::function& pop_eh, - std::function& fresh_eh); + void* ctx, + solver::push_eh_t& push_eh, + solver::pop_eh_t& pop_eh, + solver::fresh_eh_t& fresh_eh); void user_propagate_register_final(solver::final_eh_t& final_eh) { if (!m_user_propagator) diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index 9d69631427c..4d4cf800028 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -234,10 +234,10 @@ namespace smt { } void user_propagate_init( - void* ctx, - std::function& push_eh, - std::function& pop_eh, - std::function& fresh_eh) { + void* ctx, + solver::push_eh_t& push_eh, + solver::pop_eh_t& pop_eh, + solver::fresh_eh_t& fresh_eh) { m_kernel.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); } @@ -474,10 +474,10 @@ namespace smt { } void kernel::user_propagate_init( - void* ctx, - std::function& push_eh, - std::function& pop_eh, - std::function& fresh_eh) { + void* ctx, + solver::push_eh_t& push_eh, + solver::pop_eh_t& pop_eh, + solver::fresh_eh_t& fresh_eh) { m_imp->user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); } diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index c3a6d180e90..2590b488e37 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -290,9 +290,9 @@ namespace smt { */ void user_propagate_init( void* ctx, - std::function& push_eh, - std::function& pop_eh, - std::function& fresh_eh); + solver::push_eh_t& push_eh, + solver::pop_eh_t& pop_eh, + solver::fresh_eh_t& fresh_eh); void user_propagate_register_fixed(solver::fixed_eh_t& fixed_eh); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 42854b811ee..0b380f04d33 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -212,7 +212,7 @@ namespace { void* ctx, std::function& push_eh, std::function& pop_eh, - std::function& fresh_eh) override { + solver::fresh_eh_t& fresh_eh) override { m_context.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); } diff --git a/src/smt/user_propagator.cpp b/src/smt/user_propagator.cpp index 2bd4b284430..2f13f5ee08b 100644 --- a/src/smt/user_propagator.cpp +++ b/src/smt/user_propagator.cpp @@ -23,11 +23,13 @@ Module Name: using namespace smt; user_propagator::user_propagator(context& ctx): - theory(ctx, ctx.get_manager().mk_family_id("user_propagator")), - m_qhead(0), - m_num_scopes(0) + theory(ctx, ctx.get_manager().mk_family_id("user_propagator")) {} +user_propagator::~user_propagator() { + dealloc(m_api_context); +} + void user_propagator::force_push() { for (; m_num_scopes > 0; --m_num_scopes) { theory::push_scope_eh(); @@ -36,9 +38,6 @@ void user_propagator::force_push() { } } -// TODO: check type of 'e', either Bool or Bit-vector. -// - unsigned user_propagator::add_expr(expr* e) { force_push(); enode* n = ensure_enode(e); @@ -49,13 +48,13 @@ unsigned user_propagator::add_expr(expr* e) { return v; } -void user_propagator::propagate(unsigned sz, unsigned const* ids, expr* conseq) { - m_prop.push_back(prop_info(sz, ids, expr_ref(conseq, m))); +void user_propagator::propagate(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr* conseq) { + m_prop.push_back(prop_info(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, expr_ref(conseq, m))); } theory * user_propagator::mk_fresh(context * new_ctx) { auto* th = alloc(user_propagator, *new_ctx); - void* ctx = m_fresh_eh(m_user_context); + void* ctx = m_fresh_eh(m_user_context, new_ctx->get_manager(), th->m_api_context); th->add(ctx, m_push_eh, m_pop_eh, m_fresh_eh); if ((bool)m_fixed_eh) th->register_fixed(m_fixed_eh); if ((bool)m_final_eh) th->register_final(m_final_eh); @@ -110,9 +109,12 @@ void user_propagator::propagate() { justification* js; while (qhead < m_prop.size() && !ctx.inconsistent()) { auto const& prop = m_prop[qhead]; - m_lits.reset(); + m_lits.reset(); + eqs.reset(); for (unsigned id : prop.m_ids) m_lits.append(m_id2justification[id]); + for (auto const& p : prop.m_eqs) + eqs.push_back(enode_pair(get_enode(p.first), get_enode(p.second))); if (m.is_false(prop.m_conseq)) { js = ctx.mk_justification( ext_theory_conflict_justification( @@ -126,10 +128,16 @@ void user_propagator::propagate() { get_id(), ctx.get_region(), m_lits.size(), m_lits.c_ptr(), eqs.size(), eqs.c_ptr(), lit)); ctx.assign(lit, js); } + ++m_stats.m_num_propagations; ++qhead; } ctx.push_trail(value_trail(m_qhead)); m_qhead = qhead; } +void user_propagator::collect_statistics(::statistics & st) const { + st.update("user-propagations", m_stats.m_num_propagations); + st.update("user-watched", get_num_vars()); +} + diff --git a/src/smt/user_propagator.h b/src/smt/user_propagator.h index 409891b864c..08a48f41637 100644 --- a/src/smt/user_propagator.h +++ b/src/smt/user_propagator.h @@ -29,45 +29,59 @@ Module Name: namespace smt { class user_propagator : public theory, public solver::propagate_callback { - void* m_user_context; - std::function m_push_eh; - std::function m_pop_eh; - std::function m_fresh_eh; - solver::final_eh_t m_final_eh; - solver::fixed_eh_t m_fixed_eh; - solver::eq_eh_t m_eq_eh; - solver::eq_eh_t m_diseq_eh; struct prop_info { unsigned_vector m_ids; expr_ref m_conseq; - prop_info(unsigned sz, unsigned const* ids, expr_ref const& c): - m_ids(sz, ids), + svector> m_eqs; + prop_info(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr_ref const& c): + m_ids(num_fixed, fixed_ids), m_conseq(c) - {} + { + for (unsigned i = 0; i < num_eqs; ++i) + m_eqs.push_back(std::make_pair(eq_lhs[i], eq_rhs[i])); + } }; - unsigned m_qhead; + + struct stats { + unsigned m_num_propagations; + stats() { reset(); } + void reset() { memset(this, 0, sizeof(*this)); } + }; + + void* m_user_context; + solver::push_eh_t m_push_eh; + solver::pop_eh_t m_pop_eh; + solver::fresh_eh_t m_fresh_eh; + solver::final_eh_t m_final_eh; + solver::fixed_eh_t m_fixed_eh; + solver::eq_eh_t m_eq_eh; + solver::eq_eh_t m_diseq_eh; + void* m_api_context { nullptr }; + + unsigned m_qhead { 0 }; vector m_prop; unsigned_vector m_prop_lim; vector m_id2justification; - unsigned m_num_scopes; + unsigned m_num_scopes { 0 }; literal_vector m_lits; + stats m_stats; void force_push(); public: user_propagator(context& ctx); - ~user_propagator() override {} + ~user_propagator() override; /* * \brief initial setup for user propagator. */ void add( - void* ctx, - std::function& push_eh, - std::function& pop_eh, - std::function& fresh_eh) { + void* ctx, + solver::push_eh_t& push_eh, + solver::pop_eh_t& pop_eh, + solver::fresh_eh_t& fresh_eh) { m_user_context = ctx; m_push_eh = push_eh; m_pop_eh = pop_eh; @@ -81,7 +95,9 @@ namespace smt { void register_eq(solver::eq_eh_t& eq_eh) { m_eq_eh = eq_eh; } void register_diseq(solver::eq_eh_t& diseq_eh) { m_diseq_eh = diseq_eh; } - void propagate(unsigned sz, unsigned const* ids, expr* conseq) override; + bool has_fixed() const { return (bool)m_fixed_eh; } + + void propagate(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* lhs, unsigned const* rhs, expr* conseq) override; void new_fixed_eh(theory_var v, expr* value, unsigned num_lits, literal const* jlits); @@ -99,7 +115,7 @@ namespace smt { void push_scope_eh() override; void pop_scope_eh(unsigned num_scopes) override; void restart_eh() override {} - void collect_statistics(::statistics & st) const override {} + void collect_statistics(::statistics & st) const override; model_value_proc * mk_value(enode * n, model_generator & mg) override { return nullptr; } void init_model(model_generator & m) override {} bool include_func_interp(func_decl* f) override { return false; } diff --git a/src/solver/solver.h b/src/solver/solver.h index 2fe01498638..1f8d700ae53 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -239,22 +239,26 @@ class solver : public check_sat_result { virtual expr_ref get_implied_upper_bound(expr* e) = 0; - virtual void user_propagate_init( - void* ctx, - std::function& push_eh, - std::function& pop_eh, - std::function& fresh_eh) { - throw default_exception("user-propagators are only supported on the SMT solver"); - } - class propagate_callback { public: - virtual void propagate(unsigned sz, unsigned const* ids, expr* conseq) = 0; + virtual void propagate(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr* conseq) = 0; }; 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; + + virtual void user_propagate_init( + void* ctx, + push_eh_t& push_eh, + pop_eh_t& pop_eh, + fresh_eh_t& fresh_eh) { + throw default_exception("user-propagators are only supported on the SMT solver"); + } + virtual void user_propagate_register_fixed(fixed_eh_t& fixed_eh) { throw default_exception("user-propagators are only supported on the SMT solver");