adding user propagation to API

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/smt/smt_context.cpp

@@ -2878,7 +2878,7 @@ namespace smt {
         }
     }
 
-    void context::register_user_propagator(
+    void context::user_propagate_init(
         void* ctx, 
         std::function<void(void*, unsigned, expr*)>& fixed_eh,
         std::function<void(void*)>&                  push_eh,

src/smt/smt_context.h

@@ -1682,12 +1682,25 @@ namespace smt {
         /*
          * user-propagator
          */
-        void register_user_propagator(
+        void user_propagate_init(
             void* ctx, 
             std::function<void(void*, unsigned, expr*)>& fixed_eh,
             std::function<void(void*)>&                  push_eh,
             std::function<void(void*, unsigned)>&        pop_eh);
 
+        unsigned user_propagate_register(expr* e) {
+            if (!m_user_propagator) 
+                throw default_exception("user propagator must be initialized");
+            return m_user_propagator->add_expr(e);
+        }
+        
+        void user_propagate_consequence(unsigned sz, unsigned const* ids, expr* conseq) {
+            if (!m_user_propagator) 
+                throw default_exception("user propagator must be initialized");
+            m_user_propagator->add_propagation(sz, ids, conseq);
+        }
+
+
         bool watches_fixed(enode* n) const;
 
         void assign_fixed(enode* n, expr* val, unsigned sz, literal const* explain);

src/smt/smt_kernel.cpp

@@ -233,12 +233,20 @@ namespace smt {
             m_kernel.updt_params(p);
         }
 
-        void register_user_propagator(
+        void user_propagate_init(
             void* ctx, 
             std::function<void(void*, unsigned, expr*)>& fixed_eh,
             std::function<void(void*)>&                  push_eh,
             std::function<void(void*, unsigned)>&        pop_eh) {
-            m_kernel.register_user_propagator(ctx, fixed_eh, push_eh, pop_eh);
+            m_kernel.user_propagate_init(ctx, fixed_eh, push_eh, pop_eh);
+        }
+
+        unsigned user_propagate_register(expr* e) {
+            return m_kernel.user_propagate_register(e);
+        }
+        
+        void user_propagate_consequence(unsigned sz, unsigned const* ids, expr* conseq) {
+            m_kernel.user_propagate_consequence(sz, ids, conseq);
         }
     };
 
@@ -327,7 +335,6 @@ namespace smt {
         return m_imp->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);
     }
@@ -453,12 +460,20 @@ namespace smt {
         return m_imp->get_implied_upper_bound(e);
     }
 
-    void kernel::register_user_propagator(
+    void kernel::user_propagate_init(
         void* ctx, 
         std::function<void(void*, unsigned, expr*)>& fixed_eh,
         std::function<void(void*)>&                  push_eh,
         std::function<void(void*, unsigned)>&        pop_eh) {
-        m_imp->register_user_propagator(ctx, fixed_eh, push_eh, pop_eh);
+        m_imp->user_propagate_init(ctx, fixed_eh, push_eh, pop_eh);
+    }
+
+    unsigned kernel::user_propagate_register(expr* e) {
+        return m_imp->user_propagate_register(e);
+    }
+        
+    void kernel::user_propagate_consequence(unsigned sz, unsigned const* ids, expr* conseq) {
+        m_imp->user_propagate_consequence(sz, ids, conseq);
     }
 
 

src/smt/smt_kernel.h

@@ -285,14 +285,27 @@ namespace smt {
         static void collect_param_descrs(param_descrs & d);
 
         /**
-           \brief register a user-propagator "theory"
+           \brief initialize a user-propagator "theory"
         */
-        void register_user_propagator(
+        void user_propagate_init(
             void* ctx, 
             std::function<void(void*, unsigned, expr*)>& fixed_eh,
             std::function<void(void*)>&                  push_eh,
             std::function<void(void*, unsigned)>&        pop_eh);
 
+        /**
+           \brief register an expression to be tracked fro user propagation.
+        */
+        unsigned user_propagate_register(expr* e);
+
+
+        /**
+           \brief accept a user-propagation callback (issued during fixed_he).
+        */
+        
+        void user_propagate_consequence(unsigned sz, unsigned const* ids, expr* conseq);
+        
+
         /**
            \brief Return a reference to smt::context.
            This is a temporary hack to support user theories.

src/smt/smt_solver.cpp

@@ -208,14 +208,21 @@ namespace {
             return m_context.get_trail();
         }
 
-        void register_user_propagator(
+        void user_propagate_init(
             void* ctx, 
             std::function<void(void*, unsigned, expr*)>& fixed_eh,
             std::function<void(void*)>&                  push_eh,
             std::function<void(void*, unsigned)>&        pop_eh) override {
-            m_context.register_user_propagator(ctx, fixed_eh, push_eh, pop_eh);
+            m_context.user_propagate_init(ctx, fixed_eh, push_eh, pop_eh);
         }
 
+        unsigned user_propagate_register(expr* e) override { 
+            return m_context.user_propagate_register(e);
+        }
+
+        void user_propagate_consequence(unsigned sz, unsigned const* ids, expr* conseq) {
+            m_context.user_propagate_consequence(sz, ids, conseq);
+        }        
 
         struct scoped_minimize_core {
             smt_solver& s;