introducing base namespace for user propagator

src/api/api_solver.cpp

@@ -866,7 +866,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-    class api_context_obj : public solver::context_obj {
+    class api_context_obj : public user_propagator::context_obj {
         api::context* c;
     public:
         api_context_obj(api::context* c):c(c) {}
@@ -883,9 +883,9 @@ extern "C" {
         Z3_TRY;
         RESET_ERROR_CODE();
         init_solver(c, s);
-        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, solver::context_obj*& _ctx) {
+        user_propagator::push_eh_t _push = push_eh;
+        user_propagator::pop_eh_t _pop = 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);
             auto* ctx = alloc(api::context, &params, false);
@@ -902,7 +902,7 @@ extern "C" {
         Z3_fixed_eh fixed_eh) {
         Z3_TRY;
         RESET_ERROR_CODE();
-        solver::fixed_eh_t _fixed = (void(*)(void*,solver::propagate_callback*,unsigned,expr*))fixed_eh; 
+        user_propagator::fixed_eh_t _fixed = (void(*)(void*,user_propagator::callback*,unsigned,expr*))fixed_eh;
         to_solver_ref(s)->user_propagate_register_fixed(_fixed);
         Z3_CATCH;        
     }
@@ -913,7 +913,7 @@ extern "C" {
         Z3_final_eh final_eh) {
         Z3_TRY;
         RESET_ERROR_CODE();
-        solver::final_eh_t _final = (bool(*)(void*,solver::propagate_callback*))final_eh;
+        user_propagator::final_eh_t _final = (bool(*)(void*,user_propagator::callback*))final_eh;
         to_solver_ref(s)->user_propagate_register_final(_final);
         Z3_CATCH;        
     }
@@ -924,7 +924,7 @@ extern "C" {
         Z3_eq_eh eq_eh) {
         Z3_TRY;
         RESET_ERROR_CODE();
-        solver::eq_eh_t _eq = (void(*)(void*,solver::propagate_callback*,unsigned,unsigned))eq_eh;
+        user_propagator::eq_eh_t _eq = (void(*)(void*,user_propagator::callback*,unsigned,unsigned))eq_eh;
         to_solver_ref(s)->user_propagate_register_eq(_eq);
         Z3_CATCH;        
     }
@@ -935,7 +935,7 @@ extern "C" {
         Z3_eq_eh    diseq_eh) {
         Z3_TRY;
         RESET_ERROR_CODE();
-        solver::eq_eh_t _diseq = (void(*)(void*,solver::propagate_callback*,unsigned,unsigned))diseq_eh;
+        user_propagator::eq_eh_t _diseq = (void(*)(void*,user_propagator::callback*,unsigned,unsigned))diseq_eh;
         to_solver_ref(s)->user_propagate_register_diseq(_diseq);
         Z3_CATCH;        
     }
@@ -952,7 +952,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_solver_propagate_consequence(c, s, num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, conseq);
         RESET_ERROR_CODE();
-        reinterpret_cast<solver::propagate_callback*>(s)->propagate_cb(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, to_expr(conseq));
+        reinterpret_cast<user_propagator::callback*>(s)->propagate_cb(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, to_expr(conseq));
         Z3_CATCH;        
     }
 

src/sat/sat_solver/inc_sat_solver.cpp

@@ -661,25 +661,25 @@ class inc_sat_solver : public solver {
 
     void user_propagate_init(
         void*                ctx, 
-        solver::push_eh_t&   push_eh,
-        solver::pop_eh_t&    pop_eh,
-        solver::fresh_eh_t&  fresh_eh) override {
+        user_propagator::push_eh_t&   push_eh,
+        user_propagator::pop_eh_t&    pop_eh,
+        user_propagator::fresh_eh_t&  fresh_eh) override {
         ensure_euf()->user_propagate_init(ctx, push_eh, pop_eh, fresh_eh);
     }
 
-    void user_propagate_register_fixed(solver::fixed_eh_t& fixed_eh) override {
+    void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) override {
         ensure_euf()->user_propagate_register_fixed(fixed_eh);
     }
 
-    void user_propagate_register_final(solver::final_eh_t& final_eh) override {
+    void user_propagate_register_final(user_propagator::final_eh_t& final_eh) override {
         ensure_euf()->user_propagate_register_final(final_eh);
     }
 
-    void user_propagate_register_eq(solver::eq_eh_t& eq_eh) override {
+    void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) override {
         ensure_euf()->user_propagate_register_eq(eq_eh);
     }
 
-    void user_propagate_register_diseq(solver::eq_eh_t& diseq_eh) override {
+    void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) override {
         ensure_euf()->user_propagate_register_diseq(diseq_eh);
     }
 
@@ -959,11 +959,11 @@ class inc_sat_solver : public solver {
         extract_asm2dep(asm2dep);
         sat::literal_vector const& core = m_solver.get_core();
         TRACE("sat",
-              for (auto kv : m_dep2asm) {
+              for (auto const& kv : m_dep2asm) {
                   tout << mk_pp(kv.m_key, m) << " |-> " << sat::literal(kv.m_value) << "\n";
               }
               tout << "asm2fml: ";
-              for (auto kv : asm2fml) {
+              for (auto const& kv : asm2fml) {
                   tout << mk_pp(kv.m_key, m) << " |-> " << mk_pp(kv.m_value, m) << "\n";
               }
               tout << "core: "; for (auto c : core) tout << c << " ";  tout << "\n";

src/sat/smt/euf_solver.cpp

@@ -295,7 +295,7 @@ namespace euf {
             return;
         bool sign = l.sign();   
         m_egraph.set_value(n, sign ? l_false : l_true);
-        for (auto th : enode_th_vars(n))
+        for (auto const& th : enode_th_vars(n))
             m_id2solver[th.get_id()]->asserted(l);
 
         size_t* c = to_ptr(l);
@@ -519,8 +519,7 @@ namespace euf {
 
     void solver::push() {
         si.push();
-        scope s;
-        s.m_var_lim = m_var_trail.size();
+        scope s(m_var_trail.size());
         m_scopes.push_back(s);
         m_trail.push_scope();
         for (auto* e : m_solvers)
@@ -994,9 +993,9 @@ namespace euf {
 
     void solver::user_propagate_init(
         void* ctx,
-        ::solver::push_eh_t& push_eh,
-        ::solver::pop_eh_t& pop_eh,
-        ::solver::fresh_eh_t& fresh_eh) {
+        user_propagator::push_eh_t& push_eh,
+        user_propagator::pop_eh_t& pop_eh,
+        user_propagator::fresh_eh_t& fresh_eh) {
         m_user_propagator = alloc(user_solver::solver, *this);
         m_user_propagator->add(ctx, push_eh, pop_eh, fresh_eh);
         for (unsigned i = m_scopes.size(); i-- > 0; )

src/sat/smt/euf_solver.h

@@ -72,6 +72,7 @@ namespace euf {
         };
         struct scope {
             unsigned m_var_lim;
+            scope(unsigned l) : m_var_lim(l) {}
         };
 
 
@@ -400,27 +401,27 @@ namespace euf {
         // user propagator
         void user_propagate_init(
             void* ctx,
-            ::solver::push_eh_t& push_eh,
-            ::solver::pop_eh_t& pop_eh,
-            ::solver::fresh_eh_t& fresh_eh);
+            user_propagator::push_eh_t& push_eh,
+            user_propagator::pop_eh_t& pop_eh,
+            user_propagator::fresh_eh_t& fresh_eh);
         bool watches_fixed(enode* n) const;
         void assign_fixed(enode* n, expr* val, unsigned sz, literal const* explain);
         void assign_fixed(enode* n, expr* val, literal_vector const& explain) { assign_fixed(n, val, explain.size(), explain.data()); }
         void assign_fixed(enode* n, expr* val, literal explain) { assign_fixed(n, val, 1, &explain); }
 
-        void user_propagate_register_final(::solver::final_eh_t& final_eh) {
+        void user_propagate_register_final(user_propagator::final_eh_t& final_eh) {
             check_for_user_propagator();
             m_user_propagator->register_final(final_eh);
         }
-        void user_propagate_register_fixed(::solver::fixed_eh_t& fixed_eh) {
+        void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) {
             check_for_user_propagator();
             m_user_propagator->register_fixed(fixed_eh);
         }
-        void user_propagate_register_eq(::solver::eq_eh_t& eq_eh) {
+        void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) {
             check_for_user_propagator();
             m_user_propagator->register_eq(eq_eh);
         }
-        void user_propagate_register_diseq(::solver::eq_eh_t& diseq_eh) {
+        void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) {
             check_for_user_propagator();
             m_user_propagator->register_diseq(diseq_eh);
         }

src/sat/smt/user_solver.h

@@ -21,11 +21,12 @@ Module Name:
 
 #include "sat/smt/sat_th.h"
 #include "solver/solver.h"
+#include "tactic/user_propagator_base.h"
 
 
 namespace user_solver {
 
-    class solver : public euf::th_euf_solver, public ::solver::propagate_callback {
+    class solver : public euf::th_euf_solver, public user_propagator::callback {
 
         struct prop_info {
             unsigned_vector m_ids;
@@ -47,15 +48,15 @@ namespace user_solver {
         };
 
         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;
-        ::solver::context_obj*   m_api_context { nullptr };
-        unsigned               m_qhead { 0 };
+        user_propagator::push_eh_t      m_push_eh;
+        user_propagator::pop_eh_t       m_pop_eh;
+        user_propagator::fresh_eh_t     m_fresh_eh;
+        user_propagator::final_eh_t     m_final_eh;
+        user_propagator::fixed_eh_t     m_fixed_eh;
+        user_propagator::eq_eh_t        m_eq_eh;
+        user_propagator::eq_eh_t        m_diseq_eh;
+        user_propagator::context_obj*   m_api_context = nullptr;
+        unsigned               m_qhead = 0;
         vector<prop_info>      m_prop;
         unsigned_vector        m_prop_lim;
         vector<sat::literal_vector> m_id2justification;
@@ -91,9 +92,9 @@ namespace user_solver {
          */
         void add(
             void*                 ctx, 
-            ::solver::push_eh_t&    push_eh,
-            ::solver::pop_eh_t&     pop_eh,
-            ::solver::fresh_eh_t&   fresh_eh) {
+            user_propagator::push_eh_t&    push_eh,
+            user_propagator::pop_eh_t&     pop_eh,
+            user_propagator::fresh_eh_t&   fresh_eh) {
             m_user_context = ctx;
             m_push_eh      = push_eh;
             m_pop_eh       = pop_eh;
@@ -102,10 +103,10 @@ namespace user_solver {
 
         unsigned add_expr(expr* e);
 
-        void register_final(::solver::final_eh_t& final_eh) { m_final_eh = final_eh; }
-        void register_fixed(::solver::fixed_eh_t& fixed_eh) { m_fixed_eh = fixed_eh; }
-        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 register_final(user_propagator::final_eh_t& final_eh) { m_final_eh = final_eh; }
+        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; }
 
         bool has_fixed() const { return (bool)m_fixed_eh; }
 

src/smt/smt_context.cpp

@@ -198,7 +198,7 @@ namespace smt {
             return;
         ast_translation tr(src_ctx.m, m, false);
         auto* p = get_theory(m.mk_family_id("user_propagator"));
-        m_user_propagator = reinterpret_cast<user_propagator*>(p);
+        m_user_propagator = reinterpret_cast<theory_user_propagator*>(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);
@@ -2886,11 +2886,11 @@ namespace smt {
 
     void context::user_propagate_init(
         void*                    ctx, 
-        solver::push_eh_t&       push_eh,
-        solver::pop_eh_t&        pop_eh,
-        solver::fresh_eh_t&      fresh_eh) {
+        user_propagator::push_eh_t&       push_eh,
+        user_propagator::pop_eh_t&        pop_eh,
+        user_propagator::fresh_eh_t&      fresh_eh) {
         setup_context(false);
-        m_user_propagator = alloc(user_propagator, *this);
+        m_user_propagator = alloc(theory_user_propagator, *this);
         m_user_propagator->add(ctx, push_eh, pop_eh, fresh_eh);
         for (unsigned i = m_scopes.size(); i-- > 0; ) 
             m_user_propagator->push_scope_eh();
@@ -3552,7 +3552,7 @@ namespace smt {
             parallel p(*this);
             return p(asms);
         }
-        lbool r;
+        lbool r = l_undef;
         do {
             pop_to_base_lvl();
             expr_ref_vector asms(m, num_assumptions, assumptions);
@@ -3573,7 +3573,7 @@ namespace smt {
         if (!check_preamble(true)) return l_undef;
         TRACE("before_search", display(tout););
         setup_context(false);
-        lbool r;
+        lbool r = l_undef;
         do {
             pop_to_base_lvl();
             expr_ref_vector asms(cube);

src/smt/smt_context.h

@@ -88,7 +88,7 @@ namespace smt {
         scoped_ptr<quantifier_manager>   m_qmanager;
         scoped_ptr<model_generator>      m_model_generator;
         scoped_ptr<relevancy_propagator> m_relevancy_propagator;
-        user_propagator*            m_user_propagator;
+        theory_user_propagator*          m_user_propagator;
         random_gen                  m_random;
         bool                        m_flushing; // (debug support) true when flushing
         mutable unsigned            m_lemma_id;
@@ -1695,29 +1695,29 @@ namespace smt {
          */
         void user_propagate_init(
             void*                 ctx, 
-            solver::push_eh_t&    push_eh,
-            solver::pop_eh_t&     pop_eh,
-            solver::fresh_eh_t&   fresh_eh);
+            user_propagator::push_eh_t&    push_eh,
+            user_propagator::pop_eh_t&     pop_eh,
+            user_propagator::fresh_eh_t&   fresh_eh);
 
-        void user_propagate_register_final(solver::final_eh_t& final_eh) {
+        void user_propagate_register_final(user_propagator::final_eh_t& final_eh) {
             if (!m_user_propagator) 
                 throw default_exception("user propagator must be initialized");
             m_user_propagator->register_final(final_eh);
         }
 
-        void user_propagate_register_fixed(solver::fixed_eh_t& fixed_eh) {
+        void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) {
             if (!m_user_propagator) 
                 throw default_exception("user propagator must be initialized");
             m_user_propagator->register_fixed(fixed_eh);
         }
 
-        void user_propagate_register_eq(solver::eq_eh_t& eq_eh) {
+        void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) {
             if (!m_user_propagator) 
                 throw default_exception("user propagator must be initialized");
             m_user_propagator->register_eq(eq_eh);
         }
 
-        void user_propagate_register_diseq(solver::eq_eh_t& diseq_eh) {
+        void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) {
             if (!m_user_propagator) 
                 throw default_exception("user propagator must be initialized");
             m_user_propagator->register_diseq(diseq_eh);