diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index fe9fe2054..ba8005484 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1729,10 +1729,10 @@ namespace smt { return m_user_propagator->add_expr(e); } - void user_propagate_register_declared(user_propagator::register_created_eh_t& r) { + void user_propagate_register_created(user_propagator::register_created_eh_t& r) { if (!m_user_propagator) throw default_exception("user propagator must be initialized"); - m_user_propagator->register_declared(r); + m_user_propagator->register_created(r); } func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index 1e97fa465..13f7da7dc 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -249,8 +249,8 @@ namespace smt { return m_kernel.user_propagate_register(e); } - void user_propagate_register_declared(user_propagator::register_created_eh_t& r) { - m_kernel.user_propagate_register_declared(r); + void user_propagate_register_created(user_propagator::register_created_eh_t& r) { + m_kernel.user_propagate_register_created(r); } func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { @@ -305,7 +305,6 @@ namespace smt { return m_imp->get_formula(i); } - void kernel::push() { m_imp->push(); } @@ -485,8 +484,8 @@ namespace smt { return m_imp->user_propagate_register(e); } - void kernel::user_propagate_register_declared(user_propagator::register_created_eh_t& r) { - m_imp->user_propagate_register_declared(r); + void kernel::user_propagate_register_created(user_propagator::register_created_eh_t& r) { + m_imp->user_propagate_register_created(r); } func_decl* kernel::user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index 7af8f2fe6..e8fdbc648 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -303,7 +303,7 @@ namespace smt { unsigned user_propagate_register(expr* e); - void user_propagate_register_declared(user_propagator::register_created_eh_t& r); + void user_propagate_register_created(user_propagator::register_created_eh_t& r); func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 9352e33f4..a755fe5ae 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -241,6 +241,14 @@ namespace { return m_context.user_propagate_register(e); } + void user_propagate_register_created(user_propagator::register_created_eh_t& c) override { + m_context.user_propagate_register_created(c); + } + + func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { + return m_context.user_propagate_declare(name, n, domain, range); + } + struct scoped_minimize_core { smt_solver& s; expr_ref_vector m_assumptions; diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp index 5cbe469fd..93ce81976 100644 --- a/src/smt/tactic/smt_tactic_core.cpp +++ b/src/smt/tactic/smt_tactic_core.cpp @@ -319,15 +319,21 @@ public: user_propagator::final_eh_t m_final_eh; user_propagator::eq_eh_t m_eq_eh; user_propagator::eq_eh_t m_diseq_eh; + user_propagator::register_created_eh_t m_created_eh; + expr_ref_vector m_vars; unsigned_vector m_var2internal; unsigned_vector m_internal2var; + unsigned_vector m_limit; + + user_propagator::push_eh_t i_push_eh; + user_propagator::pop_eh_t i_pop_eh; user_propagator::fixed_eh_t i_fixed_eh; user_propagator::final_eh_t i_final_eh; user_propagator::eq_eh_t i_eq_eh; user_propagator::eq_eh_t i_diseq_eh; - + user_propagator::register_created_eh_t i_created_eh; struct callback : public user_propagator::callback { @@ -403,15 +409,43 @@ public: m_ctx->user_propagate_register_diseq(i_diseq_eh); } + void init_i_created_eh() { + if (!m_created_eh) + return; + i_created_eh = [this](void* ctx, user_propagator::callback* cb, expr* e, unsigned i) { + unsigned j = m_vars.size(); + m_vars.push_back(e); + m_internal2var.setx(i, j, 0); + m_var2internal.setx(j, i, 0); + }; + m_ctx->user_propagate_register_created(i_created_eh); + } + + void init_i_push_pop() { + i_push_eh = [this](void* ctx) { + m_limit.push_back(m_vars.size()); + m_push_eh(ctx); + }; + i_pop_eh = [this](void* ctx, unsigned n) { + unsigned old_sz = m_limit.size() - n; + unsigned num_vars = m_limit[old_sz]; + m_vars.shrink(num_vars); + m_limit.shrink(old_sz); + m_pop_eh(ctx, n); + }; + } + void user_propagate_delay_init() { if (!m_user_ctx) return; - m_ctx->user_propagate_init(m_user_ctx, m_push_eh, m_pop_eh, m_fresh_eh); + init_i_push_pop(); + m_ctx->user_propagate_init(m_user_ctx, i_push_eh, i_pop_eh, m_fresh_eh); init_i_fixed_eh(); init_i_final_eh(); init_i_eq_eh(); init_i_diseq_eh(); + init_i_created_eh(); unsigned i = 0; for (expr* v : m_vars) { @@ -463,6 +497,14 @@ public: m_vars.push_back(e); return m_vars.size() - 1; } + + func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) override { + return m_ctx->user_propagate_declare(name, n, domain, range); + } + + void user_propagate_register_created(user_propagator::register_created_eh_t& created_eh) override { + m_ctx->user_propagate_register_created(created_eh); + } }; static tactic * mk_seq_smt_tactic(ast_manager& m, params_ref const & p) { diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index 75983b490..ac7968d45 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -189,8 +189,12 @@ bool theory_user_propagator::internalize_atom(app* atom, bool gate_ctx) { } bool theory_user_propagator::internalize_term(app* term) { - NOT_IMPLEMENTED_YET(); - return false; + for (auto arg : *term) + ensure_enode(arg); + unsigned v = add_expr(term); + if (m_created_eh) + m_created_eh(m_user_context, this, term, v); + return true; } void theory_user_propagator::collect_statistics(::statistics & st) const { diff --git a/src/smt/theory_user_propagator.h b/src/smt/theory_user_propagator.h index 0c5cdeef8..a9b340d4a 100644 --- a/src/smt/theory_user_propagator.h +++ b/src/smt/theory_user_propagator.h @@ -96,7 +96,7 @@ namespace smt { void register_fixed(user_propagator::fixed_eh_t& fixed_eh) { m_fixed_eh = fixed_eh; } void register_eq(user_propagator::eq_eh_t& eq_eh) { m_eq_eh = eq_eh; } void register_diseq(user_propagator::eq_eh_t& diseq_eh) { m_diseq_eh = diseq_eh; } - void register_declared(user_propagator::register_created_eh_t& created_eh) { m_created_eh = created_eh; } + void register_created(user_propagator::register_created_eh_t& created_eh) { m_created_eh = created_eh; } func_decl* declare(symbol const& name, unsigned n, sort* const* domain, sort* range); bool has_fixed() const { return (bool)m_fixed_eh; } diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 19009aa44..171a8314d 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -200,6 +200,14 @@ public: m_t2->user_propagate_clear(); } + void user_propagate_register_created(user_propagator::register_created_eh_t& created_eh) override { + m_t2->user_propagate_register_created(created_eh); + } + + func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) override { + return m_t2->user_propagate_declare(name, n, domain, range); + } + }; tactic * and_then(tactic * t1, tactic * t2) {