user propagator fixes

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Aug 20, 2020 · ba4a218 · ba4a218
1 parent de65c61
commit ba4a218
Show file tree

Hide file tree

Showing 4 changed files with 22 additions and 11 deletions.
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
@@ -2880,6 +2880,7 @@ namespace smt {
         std::function<void(void*)>&                  push_eh,
         std::function<void(void*, unsigned)>&        pop_eh,
         std::function<void*(void*)>&                 fresh_eh) {
+        setup_context(m_fparams.m_auto_config);
         m_user_propagator = alloc(user_propagator, *this);
         m_user_propagator->add(ctx, fixed_eh, push_eh, pop_eh, fresh_eh);
         for (unsigned i = m_scopes.size(); i-- > 0; ) 

diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
@@ -795,7 +795,7 @@ namespace smt {
                 //   and a theory variable must be created for it.
                 enode * e = get_enode(n);
                 if (!th->is_attached_to_var(e))
-                    internalize_theory_term(n);
+                    th->internalize_term(n);
             }
             return;
         }

diff --git a/src/smt/user_propagator.cpp b/src/smt/user_propagator.cpp
@@ -49,6 +49,17 @@ unsigned user_propagator::add_expr(expr* e) {
     return v;
 }
 
+void user_propagator::add_propagation(unsigned sz, unsigned const* ids, expr* conseq) {
+    m_prop.push_back(prop_info(sz, ids, 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);
+    th->add(ctx, m_fixed_eh, m_push_eh, m_pop_eh, m_fresh_eh);
+    return th;
+}
+
 void user_propagator::new_fixed_eh(theory_var v, expr* value, unsigned num_lits, literal const* jlits) {
     force_push();
     m_id2justification.setx(v, literal_vector(num_lits, jlits), literal_vector());
@@ -77,6 +88,8 @@ bool user_propagator::can_propagate() {
 }
 
 void user_propagator::propagate() {
+    if (m_qhead == m_prop.size())
+        return;
     force_push();
     unsigned qhead = m_qhead;
     literal_vector lits;
@@ -86,7 +99,11 @@ void user_propagator::propagate() {
         auto const& prop = m_prop[qhead];
         lits.reset();        
         for (unsigned id : prop.m_ids) 
-            lits.append(m_id2justification[id]);
+            for (literal lit : m_id2justification[id]) {
+                if (ctx.get_assignment(lit) == l_false) 
+                    lit.neg();
+                lits.push_back(lit);
+            }
         if (m.is_false(prop.m_conseq)) {
             js = ctx.mk_justification(
                 ext_theory_conflict_justification(

diff --git a/src/smt/user_propagator.h b/src/smt/user_propagator.h
@@ -72,18 +72,11 @@ namespace smt {
 
         unsigned add_expr(expr* e);
 
-        void add_propagation(unsigned sz, unsigned const* ids, expr* conseq) {
-            m_prop.push_back(prop_info(sz, ids, expr_ref(conseq, m)));
-        }
+        void add_propagation(unsigned sz, unsigned const* ids, expr* conseq);
 
         void new_fixed_eh(theory_var v, expr* value, unsigned num_lits, literal const* jlits);
 
-        theory * mk_fresh(context * new_ctx) override { 
-            auto* th = alloc(user_propagator, *new_ctx); 
-            void* ctx = m_fresh_eh(m_user_context);
-            th->add(ctx, m_fixed_eh, m_push_eh, m_pop_eh, m_fresh_eh);
-            return th;
-        }
+        theory * mk_fresh(context * new_ctx) override;
         bool internalize_atom(app * atom, bool gate_ctx) override { UNREACHABLE(); return false; }
         bool internalize_term(app * term) override { UNREACHABLE(); return false; }
         void new_eq_eh(theory_var v1, theory_var v2) override { }