change user propagation to apply scheme similar to theory_recfun

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Dec 1, 2021 · 4daba29 · 4daba29
1 parent 3c1aedf
commit 4daba29
Showing 1 changed file with 23 additions and 9 deletions.
diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
@@ -53,7 +53,7 @@ void theory_user_propagator::propagate_cb(
     unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, 
     expr* conseq) {
     CTRACE("user_propagate", ctx.lit_internalized(conseq) && ctx.get_assignment(ctx.get_literal(conseq)) == l_true,
-           tout << "redundant consequence: " << mk_pp(conseq, m) << " relevant " << ctx.is_relevant(ctx.get_literal(conseq)) << "\n");
+           tout << "redundant consequence: " << mk_pp(conseq, m) << "\n");
     if (ctx.lit_internalized(conseq) && ctx.get_assignment(ctx.get_literal(conseq)) == l_true) 
         return;
     m_prop.push_back(prop_info(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, expr_ref(conseq, m)));
@@ -130,10 +130,10 @@ void theory_user_propagator::propagate() {
         for (auto const& p : prop.m_eqs)
             m_eqs.push_back(enode_pair(get_enode(p.first), get_enode(p.second)));
         DEBUG_CODE(for (auto const& p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root()););
-	    DEBUG_CODE(for (unsigned id : prop.m_ids) VERIFY(m_fixed.contains(id)););
-	    DEBUG_CODE(for (literal lit : m_lits) VERIFY(ctx.get_assignment(lit) == l_true););
+        DEBUG_CODE(for (unsigned id : prop.m_ids) VERIFY(m_fixed.contains(id)););
+        DEBUG_CODE(for (literal lit : m_lits) VERIFY(ctx.get_assignment(lit) == l_true););
 
-        TRACE("user_propagate", tout << "propagating: " << prop.m_conseq << "\n");
+        TRACE("user_propagate", tout << "propagating #" << prop.m_conseq->get_id() << ": " << prop.m_conseq << "\n");
 
         if (m.is_false(prop.m_conseq)) {
             js = ctx.mk_justification(
@@ -142,11 +142,25 @@ void theory_user_propagator::propagate() {
             ctx.set_conflict(js);
         }
         else {
-            literal lit = mk_literal(prop.m_conseq);
-            js = ctx.mk_justification(
-                ext_theory_propagation_justification(
-                    get_id(), ctx.get_region(), m_lits.size(), m_lits.data(), m_eqs.size(), m_eqs.data(), lit));
-            ctx.assign(lit, js);
+            for (auto& lit : m_lits)
+                lit.neg();
+            for (auto const& [a,b] : m_eqs)
+                m_lits.push_back(~mk_eq(a->get_expr(), b->get_expr(), false));
+            literal lit;
+            if (has_quantifiers(prop.m_conseq)) {
+                expr_ref fn(m.mk_fresh_const("user-conseq", m.mk_bool_sort()), m);
+                expr_ref eq(m.mk_eq(fn, prop.m_conseq), m);
+                ctx.assert_expr(eq);
+                ctx.internalize_assertions();
+                lit = mk_literal(fn);
+            }
+            else {
+                lit = mk_literal(prop.m_conseq);
+            }
+            ctx.mark_as_relevant(lit);
+            m_lits.push_back(lit);
+            ctx.mk_th_axiom(get_id(), m_lits);
+            TRACE("user_propagate", ctx.display(tout););
         }
         ++m_stats.m_num_propagations;
         ++qhead;