#5778

reprogram flush, mark clauses during reinit as non-redundant.
Z3Prover · Apr 25, 2022 · 489459a · 489459a
1 parent 0b453a4
commit 489459a
Show file tree

Hide file tree

Showing 3 changed files with 39 additions and 29 deletions.
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
@@ -614,7 +614,7 @@ namespace euf {
             if (si.is_bool_op(e)) 
                 lit = literal(replay.m[e], false);
             else 
-                lit = si.internalize(e, true);
+                lit = si.internalize(e, false);
             VERIFY(lit.var() == v);     
             if (!m_egraph.find(e) && (!m.is_iff(e) && !m.is_or(e) && !m.is_and(e) && !m.is_not(e))) {
                 ptr_buffer<euf::enode> args;

diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
@@ -610,42 +610,51 @@ namespace q {
         return ctx.get_config().m_ematching && propagate(false);
     }
 
+    void ematch::propagate(clause& c, bool flush, bool& propagated) {
+        ptr_buffer<binding> to_remove;
+        binding* b = c.m_bindings;
+        if (!b)
+            return;
+
+        do {                
+            if (propagate(true, b->m_nodes, b->m_max_generation, c, propagated)) 
+                to_remove.push_back(b);
+            else if (flush) {
+                instantiate(*b);
+                to_remove.push_back(b);
+                propagated = true;
+            }
+            b = b->next();
+        } 
+        while (b != c.m_bindings);
+
+        for (auto* b : to_remove) {
+            SASSERT(binding::contains(c.m_bindings, b));
+            binding::remove_from(c.m_bindings, b);
+            binding::detach(b);
+            ctx.push(insert_binding(ctx, c, b));
+        }
+    }
+
+
     bool ematch::propagate(bool flush) {
         m_mam->propagate();
         bool propagated = flush_prop_queue();
         if (!flush && m_qhead >= m_clause_queue.size())
             return m_inst_queue.propagate() || propagated;
-        ctx.push(value_trail<unsigned>(m_qhead));
-        ptr_buffer<binding> to_remove;
-        unsigned qhead = flush ? 0 : m_qhead;
-        for (; qhead < m_clause_queue.size() && m.inc(); ++qhead) {
-            unsigned idx = m_clause_queue[qhead];
-            clause& c = *m_clauses[idx];
-            binding* b = c.m_bindings;
-            if (!b)
-                continue;
 
-            do {                
-                if (propagate(true, b->m_nodes, b->m_max_generation, c, propagated)) 
-                    to_remove.push_back(b);
-                else if (flush) {
-                    instantiate(*b);
-                    to_remove.push_back(b);
-                    propagated = true;
-                }
-                b = b->next();
-            } 
-            while (b != c.m_bindings);
-
-            for (auto* b : to_remove) {
-                SASSERT(binding::contains(c.m_bindings, b));
-                binding::remove_from(c.m_bindings, b);
-                binding::detach(b);
-                ctx.push(insert_binding(ctx, c, b));
+        if (flush) {
+            for (auto* c : m_clauses)
+                propagate(*c, flush, propagated);
+        }
+        else {
+            ctx.push(value_trail<unsigned>(m_qhead));
+            for (; m_qhead < m_clause_queue.size() && m.inc(); ++m_qhead) {
+                unsigned idx = m_clause_queue[m_qhead];
+                clause& c = *m_clauses[idx];
+                propagate(c, flush, propagated);
             }
-            to_remove.reset();
         }
-        m_qhead = std::max(m_qhead, qhead);
         m_clause_in_queue.reset();
         m_node_in_queue.reset();
         m_in_queue_set = true;

diff --git a/src/sat/smt/q_ematch.h b/src/sat/smt/q_ematch.h
@@ -121,6 +121,7 @@ namespace q {
         void propagate(bool is_conflict, unsigned idx, sat::ext_justification_idx j_idx);
 
         bool propagate(bool flush);
+        void propagate(clause& c, bool flush, bool& propagated);
 
         expr_ref_vector m_new_defs;
         proof_ref_vector m_new_proofs;