From f0740bdf607520ae1d687e45534421e7a7a5ce1e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 18 Dec 2021 10:56:42 -0800
Subject: [PATCH] move user propagte declare to context level

declaration of user propagate functions are declared at context level instead of at solver scope.
---
 src/api/api_solver.cpp                  |  13 +-
 src/api/z3_api.h                        |  14 +-
 src/sat/sat_solver/inc_sat_solver.cpp   |   4 +-
 src/sat/smt/euf_solver.h                |   2 +-
 src/smt/smt_context.h                   |   8 +-
 src/smt/smt_kernel.cpp                  | 302 ++++--------------------
 src/smt/smt_kernel.h                    |   4 +-
 src/smt/smt_solver.cpp                  |   8 +-
 src/smt/tactic/smt_tactic_core.cpp      |   8 +-
 src/smt/theory_user_propagator.cpp      |  12 +-
 src/smt/theory_user_propagator.h        |   1 -
 src/solver/tactic2solver.cpp            |   4 +-
 src/tactic/core/elim_uncnstr_tactic.cpp |   2 +-
 src/tactic/core/reduce_args_tactic.cpp  |   4 +-
 src/tactic/tactic.h                     |   2 +-
 src/tactic/tactical.cpp                 |  12 +-
 src/tactic/user_propagator_base.h       |  16 +-
 17 files changed, 92 insertions(+), 324 deletions(-)

diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 222fe7061..8e8360cd3 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -944,7 +944,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_solver_propagate_register(c, s, e);
         RESET_ERROR_CODE();
-        return to_solver_ref(s)->user_propagate_register(to_expr(e));
+        return to_solver_ref(s)->user_propagate_register_expr(to_expr(e));
         Z3_CATCH_RETURN(0);
     }
 
@@ -972,11 +972,16 @@ extern "C" {
         Z3_CATCH;
     }
 
-    Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_solver s, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range) {
+    Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range) {
         Z3_TRY;
-        LOG_Z3_solver_propagate_declare(c, s, name, n, domain, range);
+        LOG_Z3_solver_propagate_declare(c, name, n, domain, range);
         RESET_ERROR_CODE();
-        func_decl* f = to_solver_ref(s)->user_propagate_declare(to_symbol(name), n, to_sorts(domain), to_sort(range));
+        ast_manager& m = mk_c(c)->m();        
+        family_id fid = m.mk_family_id(user_propagator::plugin::name());
+        if (!m.has_plugin(fid)) 
+            m.register_plugin(fid, alloc(user_propagator::plugin));            
+        func_decl_info info(fid, user_propagator::plugin::kind_t::OP_USER_PROPAGATE);
+        func_decl* f = m.mk_func_decl(to_symbol(name), n, to_sorts(domain), to_sort(range), info);
         mk_c(c)->save_ast_trail(f);
         RETURN_Z3(of_func_decl(f));
         Z3_CATCH_RETURN(nullptr);
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 899a5e7d1..0ac70ee98 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -6679,17 +6679,21 @@ extern "C" {
 
     /**
     * \brief register a callback when a new expression with a registered function is used by the solver 
-    * The registered function appears at the top level and is created using \c Z3_solver_declare.
+    * The registered function appears at the top level and is created using \ref Z3_propagate_solver_declare.
     */
     void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh);
 
     /**
-      \brief Create a registered function. Expressions used by the solver \c s that uses the registered function
-      at top level cause the callback propagate_created to be invoked.
+        Create uninterpreted function declaration for the user propagator.
+        When expressions using the function are created by the solver invoke a callback
+        to \ref \Z3_solver_progate_created with arguments
+        1. context and callback solve
+        2. declared_expr: expression using function that was used as the top-level symbol
+        3. declared_id: a unique identifier (unique within the current scope) to track the expression.
      
-      def_API('Z3_solver_propagate_declare', FUNC_DECL, (_in(CONTEXT), _in(SOLVER), _in(SYMBOL), _in(UINT), _in_array(3, SORT), _in(SORT)))
+      def_API('Z3_solver_propagate_declare', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(SORT)))
     */
-    Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_solver s, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range);
+    Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range);
 
     /**
        \brief register an expression to propagate on with the solver.
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index ea81f0c4d..97a319382 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -683,8 +683,8 @@ public:
         ensure_euf()->user_propagate_register_diseq(diseq_eh);
     }
     
-    unsigned user_propagate_register(expr* e) override { 
-        return ensure_euf()->user_propagate_register(e);
+    unsigned user_propagate_register_expr(expr* e) override { 
+        return ensure_euf()->user_propagate_register_expr(e);
     }
 
 private:
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index d70206d11..384e15822 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -425,7 +425,7 @@ namespace euf {
             check_for_user_propagator();
             m_user_propagator->register_diseq(diseq_eh);
         }
-        unsigned user_propagate_register(expr* e) {
+        unsigned user_propagate_register_expr(expr* e) {
             check_for_user_propagator();
             return m_user_propagator->add_expr(e);
         }
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 85f59d26c..4a764e975 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1723,7 +1723,7 @@ namespace smt {
             m_user_propagator->register_diseq(diseq_eh);
         }
 
-        unsigned user_propagate_register(expr* e) {
+        unsigned user_propagate_register_expr(expr* e) {
             if (!m_user_propagator) 
                 throw default_exception("user propagator must be initialized");
             return m_user_propagator->add_expr(e);
@@ -1735,12 +1735,6 @@ namespace smt {
             m_user_propagator->register_created(r);
         }
 
-        func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) {
-            if (!m_user_propagator)
-                throw default_exception("user propagator must be initialized");
-            return m_user_propagator->declare(name, n, domain, range);
-        }
-        
         bool watches_fixed(enode* n) const;
 
         void assign_fixed(enode* n, expr* val, unsigned sz, literal const* explain);
diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp
index b26823291..fdfbbb97a 100644
--- a/src/smt/smt_kernel.cpp
+++ b/src/smt/smt_kernel.cpp
@@ -49,14 +49,6 @@ namespace smt {
             return m_kernel.get_manager();
         }
 
-        bool set_logic(symbol logic) {
-            return m_kernel.set_logic(logic);
-        }
-        
-        void set_progress_callback(progress_callback * callback) {
-            return m_kernel.set_progress_callback(callback);
-        }
-
         void display(std::ostream & out) const {
             // m_kernel.display(out); <<< for external users it is just junk
             // TODO: it will be replaced with assertion_stack.display
@@ -67,195 +59,7 @@ namespace smt {
                 out << "\n  " << mk_ismt2_pp(f, m(), 2);
             }
             out << ")";
-        }
-        
-        void assert_expr(expr * e) {
-            TRACE("smt_kernel", tout << "assert:\n" << mk_ismt2_pp(e, m()) << "\n";);
-            m_kernel.assert_expr(e);
-        }
-        
-        void assert_expr(expr * e, proof * pr) {
-            m_kernel.assert_expr(e, pr);
-        }
-
-        unsigned size() const {
-            return m_kernel.get_num_asserted_formulas();
-        }
-        
-        void get_formulas(ptr_vector<expr>& fmls) const {
-            m_kernel.get_asserted_formulas(fmls);
-        }
-
-        expr* get_formula(unsigned i) const {
-            return m_kernel.get_asserted_formula(i);
-        }
-        
-        void push() {
-            TRACE("smt_kernel", tout << "push()\n";);
-            m_kernel.push();
-        }
-
-        void pop(unsigned num_scopes) {
-            TRACE("smt_kernel", tout << "pop()\n";);
-            m_kernel.pop(num_scopes);
-        }
-        
-        unsigned get_scope_level() const {
-            return m_kernel.get_scope_level();
-        }
-
-        lbool setup_and_check() {
-            return m_kernel.setup_and_check();
-        }
-
-        bool inconsistent() {
-            return m_kernel.inconsistent();
-        }
-        
-        lbool check(unsigned num_assumptions, expr * const * assumptions) {
-            return m_kernel.check(num_assumptions, assumptions);
-        }
-
-        lbool check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clause) {
-            return m_kernel.check(cube, clause);
-        }        
-
-        lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed) {
-            return m_kernel.get_consequences(assumptions, vars, conseq, unfixed);
-        }
-
-        lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) {
-            return m_kernel.preferred_sat(asms, cores);
-        }
-
-        lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
-            return m_kernel.find_mutexes(vars, mutexes);
-        }
-        
-        void get_model(model_ref & m) {
-            m_kernel.get_model(m);
-        }
-
-        proof * get_proof() {
-            return m_kernel.get_proof();
-        }
-
-        unsigned get_unsat_core_size() const {
-            return m_kernel.get_unsat_core_size();
-        }
-        
-        expr * get_unsat_core_expr(unsigned idx) const {
-            return m_kernel.get_unsat_core_expr(idx);
-        }
-
-        void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) {
-            m_kernel.get_levels(vars, depth);
-        }
-
-        expr_ref_vector get_trail() {
-            return m_kernel.get_trail();
-        }
-        
-        failure last_failure() const {
-            return m_kernel.get_last_search_failure();
-        }
-        
-        std::string last_failure_as_string() const {
-            return m_kernel.last_failure_as_string();
-        }
-
-        void set_reason_unknown(char const* msg) {
-            m_kernel.set_reason_unknown(msg);
-        }
-
-        void get_assignments(expr_ref_vector & result) {
-            m_kernel.get_assignments(result);
-        }
-        
-        void get_relevant_labels(expr * cnstr, buffer<symbol> & result) {
-            m_kernel.get_relevant_labels(cnstr, result);
-        }
-        
-        void get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) {
-            m_kernel.get_relevant_labeled_literals(at_lbls, result);
-        }
-
-        void get_relevant_literals(expr_ref_vector & result) {
-            m_kernel.get_relevant_literals(result);
-        }
-        
-        void get_guessed_literals(expr_ref_vector & result) {
-            m_kernel.get_guessed_literals(result);
-        }
-
-        expr_ref next_cube() {
-            lookahead lh(m_kernel);
-            return lh.choose();
-        }
-
-        expr_ref_vector cubes(unsigned depth) {
-            lookahead lh(m_kernel);
-            return lh.choose_rec(depth);
-        }
-                
-        void collect_statistics(::statistics & st) const {
-            m_kernel.collect_statistics(st);
-        }
-
-        void reset_statistics() {
-        }
-
-        void display_statistics(std::ostream & out) const {
-            m_kernel.display_statistics(out);
-        }
-        
-        void display_istatistics(std::ostream & out) const {
-            m_kernel.display_istatistics(out);
-        }
-        
-        bool canceled() {
-            return m_kernel.get_cancel_flag();
-        }
-
-        void updt_params(params_ref const & p) {
-            m_kernel.updt_params(p);
-        }
-
-        void user_propagate_init(
-            void*                    ctx, 
-            user_propagator::push_eh_t&       push_eh,
-            user_propagator::pop_eh_t&        pop_eh,
-            user_propagator::fresh_eh_t&      fresh_eh) {
-            m_kernel.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh);
-        }
-
-        void user_propagate_register_final(user_propagator::final_eh_t& final_eh) {
-            m_kernel.user_propagate_register_final(final_eh);
-        }
-
-        void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) {
-            m_kernel.user_propagate_register_fixed(fixed_eh);
-        }
-        
-        void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) {
-            m_kernel.user_propagate_register_eq(eq_eh);
-        }
-        
-        void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) {
-            m_kernel.user_propagate_register_diseq(diseq_eh);
-        }
-
-        unsigned user_propagate_register(expr* e) {
-            return m_kernel.user_propagate_register(e);
-        }
-
-        void user_propagate_register_created(user_propagator::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) {
-            return m_kernel.user_propagate_declare(name, n, domain, range);
-        }
+        } 
         
     };
 
@@ -268,7 +72,7 @@ namespace smt {
     }
 
     ast_manager & kernel::m() const {
-        return m_imp->m();
+        return m_imp->m_kernel.get_manager();
     }
 
     void  kernel::copy(kernel& src, kernel& dst) {
@@ -276,45 +80,44 @@ namespace smt {
     }
 
     bool kernel::set_logic(symbol logic) {
-        return m_imp->set_logic(logic);
+        return m_imp->m_kernel.set_logic(logic);
     }
 
     void kernel::set_progress_callback(progress_callback * callback) {
-        m_imp->set_progress_callback(callback);
+        m_imp->m_kernel.set_progress_callback(callback);
     }
 
     void kernel::assert_expr(expr * e) {
-        m_imp->assert_expr(e);
+        m_imp->m_kernel.assert_expr(e);
     }
 
     void kernel::assert_expr(expr_ref_vector const& es) {
-        for (unsigned i = 0; i < es.size(); ++i) {
-            m_imp->assert_expr(es[i]);
-        }
+        for (unsigned i = 0; i < es.size(); ++i) 
+            m_imp->m_kernel.assert_expr(es[i]);
     }
 
     void kernel::assert_expr(expr * e, proof * pr) {
-        m_imp->assert_expr(e, pr);
+        m_imp->m_kernel.assert_expr(e, pr);
     }
 
     unsigned kernel::size() const {
-        return m_imp->size();
+        return m_imp->m_kernel.get_num_asserted_formulas();
     }
     
     expr* kernel::get_formula(unsigned i) const {
-        return m_imp->get_formula(i);
+        return m_imp->m_kernel.get_asserted_formula(i);
     }
 
     void kernel::push() {
-        m_imp->push();
+        m_imp->m_kernel.push();
     }
 
     void kernel::pop(unsigned num_scopes) {
-        m_imp->pop(num_scopes);
+        m_imp->m_kernel.pop(num_scopes);
     }
 
     unsigned kernel::get_scope_level() const {
-        return m_imp->get_scope_level();
+        return m_imp->m_kernel.get_scope_level();
     }
 
     void kernel::reset() {
@@ -326,89 +129,91 @@ namespace smt {
     }
 
     bool kernel::inconsistent() {
-        return m_imp->inconsistent();
+        return m_imp->m_kernel.inconsistent();
     }
 
     lbool kernel::setup_and_check() {
-        return m_imp->setup_and_check();
+        return m_imp->m_kernel.setup_and_check();
     }
 
     lbool kernel::check(unsigned num_assumptions, expr * const * assumptions) {
-        lbool r = m_imp->check(num_assumptions, assumptions);
+        lbool r = m_imp->m_kernel.check(num_assumptions, assumptions);
         TRACE("smt_kernel", tout << "check result: " << r << "\n";);
         return r;
     }
 
     lbool kernel::check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses) {
-        return m_imp->check(cube, clauses);
+        return m_imp->m_kernel.check(cube, clauses);
     }
 
     lbool kernel::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed) {
-        return m_imp->get_consequences(assumptions, vars, conseq, unfixed);
+        return m_imp->m_kernel.get_consequences(assumptions, vars, conseq, unfixed);
     }
 
     lbool kernel::preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) {
-        return m_imp->preferred_sat(asms, cores);
+        return m_imp->m_kernel.preferred_sat(asms, cores);
     }
 
     lbool kernel::find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
-        return m_imp->find_mutexes(vars, mutexes);
+        return m_imp->m_kernel.find_mutexes(vars, mutexes);
     }
 
     void kernel::get_model(model_ref & m) {
-        m_imp->get_model(m);
+        m_imp->m_kernel.get_model(m);
     }
 
     proof * kernel::get_proof() {
-        return m_imp->get_proof();
+        return m_imp->m_kernel.get_proof();
     }
 
     unsigned kernel::get_unsat_core_size() const {
-        return m_imp->get_unsat_core_size();
+        return m_imp->m_kernel.get_unsat_core_size();
     }
         
     expr * kernel::get_unsat_core_expr(unsigned idx) const {
-        return m_imp->get_unsat_core_expr(idx);
+        return m_imp->m_kernel.get_unsat_core_expr(idx);
     }
 
     failure kernel::last_failure() const {
-        return m_imp->last_failure();
+        return m_imp->m_kernel.get_last_search_failure();
     }
 
     std::string kernel::last_failure_as_string() const {
-        return m_imp->last_failure_as_string();
+        return m_imp->m_kernel.last_failure_as_string();
     }
 
     void kernel::set_reason_unknown(char const* msg) {
-        m_imp->set_reason_unknown(msg);
+        m_imp->m_kernel.set_reason_unknown(msg);
     }
 
     void kernel::get_assignments(expr_ref_vector & result) {
-        m_imp->get_assignments(result);
+        m_imp->m_kernel.get_assignments(result);
     }
         
     void kernel::get_relevant_labels(expr * cnstr, buffer<symbol> & result) {
-        m_imp->get_relevant_labels(cnstr, result);
+        m_imp->m_kernel.get_relevant_labels(cnstr, result);
     }
     
     void kernel::get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) {
-        m_imp->get_relevant_labeled_literals(at_lbls, result);
+        m_imp->m_kernel.get_relevant_labeled_literals(at_lbls, result);
     }
 
     void kernel::get_relevant_literals(expr_ref_vector & result) {
-        m_imp->get_relevant_literals(result);
+        m_imp->m_kernel.get_relevant_literals(result);
     }
 
     void kernel::get_guessed_literals(expr_ref_vector & result) {
-        m_imp->get_guessed_literals(result);
+        m_imp->m_kernel.get_guessed_literals(result);
     }
 
     expr_ref kernel::next_cube() {
-        return m_imp->next_cube();
+        lookahead lh(m_imp->m_kernel);
+        return lh.choose();
     }        
 
     expr_ref_vector kernel::cubes(unsigned depth) {
-        return m_imp->cubes(depth);
+        lookahead lh(m_imp->m_kernel);
+        return lh.choose_rec(depth);
     }        
 
     std::ostream& kernel::display(std::ostream & out) const {
@@ -417,27 +222,26 @@ namespace smt {
     }
 
     void kernel::collect_statistics(::statistics & st) const {
-        m_imp->collect_statistics(st);
+        m_imp->m_kernel.collect_statistics(st);
     }
         
     void kernel::reset_statistics() {
-        m_imp->reset_statistics();
     }
 
     void kernel::display_statistics(std::ostream & out) const {
-        m_imp->display_statistics(out);
+        m_imp->m_kernel.display_statistics(out);
     }
 
     void kernel::display_istatistics(std::ostream & out) const {
-        m_imp->display_istatistics(out);
+        m_imp->m_kernel.display_istatistics(out);
     }
 
     bool kernel::canceled() const {
-        return m_imp->canceled();
+        return m_imp->m_kernel.get_cancel_flag();
     }
 
     void kernel::updt_params(params_ref const & p) {
-        return m_imp->updt_params(p);
+        return m_imp->m_kernel.updt_params(p);
     }
 
     void kernel::collect_param_descrs(param_descrs & d) {
@@ -449,11 +253,11 @@ namespace smt {
     }
 
     void kernel::get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) {
-        m_imp->get_levels(vars, depth);
+        m_imp->m_kernel.get_levels(vars, depth);
     }
 
     expr_ref_vector kernel::get_trail() {
-        return m_imp->get_trail();
+        return m_imp->m_kernel.get_trail();
     }
 
     void kernel::user_propagate_init(
@@ -461,35 +265,31 @@ namespace smt {
         user_propagator::push_eh_t&   push_eh,
         user_propagator::pop_eh_t&    pop_eh,
         user_propagator::fresh_eh_t&  fresh_eh) {
-        m_imp->user_propagate_init(ctx, push_eh, pop_eh, fresh_eh);
+        m_imp->m_kernel.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh);
     }
 
     void kernel::user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) {
-        m_imp->user_propagate_register_fixed(fixed_eh);
+        m_imp->m_kernel.user_propagate_register_fixed(fixed_eh);
     }
     
     void kernel::user_propagate_register_final(user_propagator::final_eh_t& final_eh) {
-        m_imp->user_propagate_register_final(final_eh);
+        m_imp->m_kernel.user_propagate_register_final(final_eh);
     }
     
     void kernel::user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) {
-        m_imp->user_propagate_register_eq(eq_eh);
+        m_imp->m_kernel.user_propagate_register_eq(eq_eh);
     }
     
     void kernel::user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) {
-        m_imp->user_propagate_register_diseq(diseq_eh);
+        m_imp->m_kernel.user_propagate_register_diseq(diseq_eh);
     }
 
-    unsigned kernel::user_propagate_register(expr* e) {
-        return m_imp->user_propagate_register(e);
+    unsigned kernel::user_propagate_register_expr(expr* e) {
+        return m_imp->m_kernel.user_propagate_register_expr(e);
     }        
 
     void kernel::user_propagate_register_created(user_propagator::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) {
-        return m_imp->user_propagate_declare(name, n, domain, range);
+        m_imp->m_kernel.user_propagate_register_created(r);
     }
 
 };
\ No newline at end of file
diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h
index 0296c29a6..5c28d52fd 100644
--- a/src/smt/smt_kernel.h
+++ b/src/smt/smt_kernel.h
@@ -301,12 +301,10 @@ namespace smt {
         
         void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh);
 
-        unsigned user_propagate_register(expr* e);
+        unsigned user_propagate_register_expr(expr* e);
         
         void user_propagate_register_created(user_propagator::created_eh_t& r);
 
-        func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range);
-
         /**
            \brief Return a reference to smt::context.
            This is a temporary hack to support user theories.
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index fe4aec944..f9ab54327 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -236,18 +236,14 @@ namespace {
             m_context.user_propagate_register_diseq(diseq_eh);
         }
 
-        unsigned user_propagate_register(expr* e) override { 
-            return m_context.user_propagate_register(e);
+        unsigned user_propagate_register_expr(expr* e) override { 
+            return m_context.user_propagate_register_expr(e);
         }
 
         void user_propagate_register_created(user_propagator::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 d67e430e2..c99e50393 100644
--- a/src/smt/tactic/smt_tactic_core.cpp
+++ b/src/smt/tactic/smt_tactic_core.cpp
@@ -449,7 +449,7 @@ public:
 
         unsigned i = 0;
         for (expr* v : m_vars) {
-            unsigned j = m_ctx->user_propagate_register(v);
+            unsigned j = m_ctx->user_propagate_register_expr(v);
             m_var2internal.setx(i, j, 0);
             m_internal2var.setx(j, i, 0);
             ++i;
@@ -493,15 +493,11 @@ public:
         m_diseq_eh = diseq_eh;
     }
 
-    unsigned user_propagate_register(expr* e) override {
+    unsigned user_propagate_register_expr(expr* e) override {
         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::created_eh_t& created_eh) override {
         m_ctx->user_propagate_register_created(created_eh);
     }
diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
index ac7968d45..200d9b946 100644
--- a/src/smt/theory_user_propagator.cpp
+++ b/src/smt/theory_user_propagator.cpp
@@ -23,7 +23,7 @@ Author:
 using namespace smt;
 
 theory_user_propagator::theory_user_propagator(context& ctx):
-    theory(ctx, ctx.get_manager().mk_family_id("user_propagator"))
+    theory(ctx, ctx.get_manager().mk_family_id(user_propagator::plugin::name()))
 {}
 
 theory_user_propagator::~theory_user_propagator() {
@@ -173,16 +173,6 @@ void theory_user_propagator::propagate() {
     m_qhead = qhead;
 }
 
-func_decl* theory_user_propagator::declare(symbol const& name, unsigned n, sort* const* domain, sort* range) {
-    if (!m_created_eh)
-        throw default_exception("event handler for dynamic expressions has to be registered before functions can be created");
-    // ensure that declaration plugin is registered with m.
-    if (!m.has_plugin(get_id())) 
-        m.register_plugin(get_id(), alloc(user_propagator::plugin));
-    
-    func_decl_info info(get_id(), user_propagator::plugin::kind_t::OP_USER_PROPAGATE);
-    return m.mk_func_decl(name, n, domain, range, info);    
-}
 
 bool theory_user_propagator::internalize_atom(app* atom, bool gate_ctx) {
     return internalize_term(atom);
diff --git a/src/smt/theory_user_propagator.h b/src/smt/theory_user_propagator.h
index 0189b13cb..0589a87a5 100644
--- a/src/smt/theory_user_propagator.h
+++ b/src/smt/theory_user_propagator.h
@@ -97,7 +97,6 @@ namespace smt {
         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_created(user_propagator::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/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 94f7fb336..15c9cab82 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -108,8 +108,8 @@ public:
         m_tactic->user_propagate_register_diseq(diseq_eh);
     }
 
-    unsigned user_propagate_register(expr* e) override {
-        return m_tactic->user_propagate_register(e);
+    unsigned user_propagate_register_expr(expr* e) override {
+        return m_tactic->user_propagate_register_expr(e);
     }
 
     void user_propagate_clear() override {
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index a5cbea932..a9f5ffcf8 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -892,7 +892,7 @@ public:
         m_num_elim_apps = 0;
     }
 
-    unsigned user_propagate_register(expr* e) override { 
+    unsigned user_propagate_register_expr(expr* e) override { 
         m_nonvars.insert(e);
         return 0;
     }
diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp
index 436ee3272..607928f64 100644
--- a/src/tactic/core/reduce_args_tactic.cpp
+++ b/src/tactic/core/reduce_args_tactic.cpp
@@ -78,7 +78,7 @@ public:
     
     void operator()(goal_ref const & g, goal_ref_buffer & result) override;
     void cleanup() override;
-    unsigned user_propagate_register(expr* e) override;
+    unsigned user_propagate_register_expr(expr* e) override;
     void user_propagate_clear() override;
 };
 
@@ -502,7 +502,7 @@ void reduce_args_tactic::cleanup() {
     m_imp->m_vars.append(vars);
 }
 
-unsigned reduce_args_tactic::user_propagate_register(expr* e) {
+unsigned reduce_args_tactic::user_propagate_register_expr(expr* e) {
     m_imp->m_vars.push_back(e);
     return 0;
 }
diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h
index 4c4b9358d..437c7f804 100644
--- a/src/tactic/tactic.h
+++ b/src/tactic/tactic.h
@@ -85,7 +85,7 @@ public:
         throw default_exception("tactic does not support user propagation");
     }
 
-    unsigned user_propagate_register(expr* e) override { return 0; }
+    unsigned user_propagate_register_expr(expr* e) override { return 0; }
     virtual char const* name() const = 0;
 
 protected:
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index 07fc88b37..fca2f8481 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -190,9 +190,9 @@ public:
         m_t2->user_propagate_register_diseq(diseq_eh);
     }
 
-    unsigned user_propagate_register(expr* e) override {
-        m_t1->user_propagate_register(e);
-        return m_t2->user_propagate_register(e);
+    unsigned user_propagate_register_expr(expr* e) override {
+        m_t1->user_propagate_register_expr(e);
+        return m_t2->user_propagate_register_expr(e);
     }
 
     void user_propagate_clear() override {
@@ -204,10 +204,6 @@ public:
         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) {
@@ -833,7 +829,7 @@ public:
     void reset() override { m_t->reset(); }
     void set_logic(symbol const& l) override { m_t->set_logic(l); }    
     void set_progress_callback(progress_callback * callback) override { m_t->set_progress_callback(callback); }
-    unsigned user_propagate_register(expr* e) override { return m_t->user_propagate_register(e); }
+    unsigned user_propagate_register_expr(expr* e) override { return m_t->user_propagate_register_expr(e); }
     void user_propagate_clear() override { m_t->user_propagate_clear(); }
 
 protected:
diff --git a/src/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h
index db9ca88fd..534b9dbc0 100644
--- a/src/tactic/user_propagator_base.h
+++ b/src/tactic/user_propagator_base.h
@@ -29,6 +29,8 @@ namespace user_propagator {
     class plugin : public decl_plugin {
     public:
 
+        static symbol name() { return symbol("user_propagator"); }
+
         enum kind_t { OP_USER_PROPAGATE };
 
         virtual ~plugin() {}
@@ -79,19 +81,7 @@ namespace user_propagator {
             throw default_exception("user-propagators are only supported on the SMT solver");
         }
         
-        virtual unsigned user_propagate_register(expr* e) { 
-            throw default_exception("user-propagators are only supported on the SMT solver");
-        }
-
-        /**
-         * Create uninterpreted function for the user propagator.
-         * When expressions using the function are assigned values, generate a callback
-         * into a register_declared_eh(user_ctx, solver_ctx, declared_expr, declare_id) with arguments
-         * 1. context and callback context
-         * 2. declared_expr: expression using function that was declared at top.
-         * 3. declared_id: a unique identifier (unique within the current scope) to track the expression.
-         */
-        virtual func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) {
+        virtual unsigned user_propagate_register_expr(expr* e) { 
             throw default_exception("user-propagators are only supported on the SMT solver");
         }