remove separate to_add_literal queue

Z3Prover · Nov 29, 2023 · d469c10 · d469c10
1 parent e972eb3
commit d469c10
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 17 deletions.
diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
@@ -88,7 +88,7 @@ namespace euf {
 
     void egraph::queue_literal(enode* p, enode* ante) {
         if (m_on_propagate_literal)
-            m_to_add_literal.push_back({ p, ante });
+            m_to_merge.push_back({ p, ante });
     }
 
     void egraph::force_push() {
@@ -352,7 +352,6 @@ namespace euf {
         if (num_scopes <= m_num_scopes) {
             m_num_scopes -= num_scopes;
             m_to_merge.reset();
-            m_to_add_literal.reset();
             return;
         }
         num_scopes -= m_num_scopes;
@@ -435,7 +434,6 @@ namespace euf {
         m_scopes.shrink(old_lim);        
         m_region.pop_scope(num_scopes);  
         m_to_merge.reset();
-        m_to_add_literal.reset();
 
         SASSERT(m_new_th_eqs_qhead <= m_new_th_eqs.size());
 
@@ -588,14 +586,16 @@ namespace euf {
         unsigned j = 0;
         for (unsigned i = 0; i < m_to_merge.size() && m.limit().inc() && !inconsistent(); ++i) {
             auto const& w = m_to_merge[i];
-            merge(w.a, w.b, justification::congruence(w.commutativity, m_congruence_timestamp++));                
-            for (; j < m_to_add_literal.size() && m.limit().inc() && !inconsistent(); ++j) {
-                auto const& [p, ante] = m_to_add_literal[j];
-                add_literal(p, ante);
-            }
+            switch (w.t) {
+            case to_merge_plain:
+                merge(w.a, w.b, justification::congruence(w.commutativity(), m_congruence_timestamp++));
+                break;
+            case to_add_literal:
+                add_literal(w.a, w.b);
+                break;
+            }                
         }
         m_to_merge.reset();
-        m_to_add_literal.reset();
         return 
             (m_new_th_eqs_qhead < m_new_th_eqs.size()) ||
             inconsistent();

diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h
@@ -84,15 +84,13 @@ namespace euf {
 
         typedef ptr_vector<trail> trail_stack;
 
+        enum to_merge_t { to_merge_plain, to_merge_comm, to_add_literal };
         struct to_merge {
             enode* a, * b;
-            bool commutativity;
-            to_merge(enode* a, enode* b, bool c) : a(a), b(b), commutativity(c) {}
-        };
-
-        struct to_add_literal {
-            enode* p, *ante;
-            to_add_literal(enode* p, enode* ante) : p(p), ante(ante) {}
+            to_merge_t t;
+            bool commutativity() const { return t == to_merge_comm; }
+            to_merge(enode* a, enode* b, bool c) : a(a), b(b), t(c ? to_merge_comm : to_merge_comm) {}
+            to_merge(enode* p, enode* ante): a(p), b(ante), t(to_add_literal) {}
         };
 
         struct stats {
@@ -167,7 +165,6 @@ namespace euf {
         };
         ast_manager&           m;
         svector<to_merge>      m_to_merge;
-        svector<to_add_literal>   m_to_add_literal;
         etable                 m_table;
         region                 m_region;
         svector<update_record> m_updates;