put ensure concat on a list

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Jan 13, 2024 · 01c5a09 · 01c5a09
1 parent 477db7d
commit 01c5a09
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 2 deletions.
diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp
@@ -205,7 +205,9 @@ namespace euf {
         enode* arg_r = arg->get_root();       
         enode* n_r = n->get_root();
 
+        m_ensure_concat.reset();
         auto ensure_concat = [&](unsigned lo, unsigned mid, unsigned hi) {
+            // verbose_stream() << lo << " " << mid << " " << hi << "\n";
             TRACE("bv", tout << "ensure-concat " << lo << " " << mid << " " << hi << "\n");
             unsigned lo_, hi_;
             for (enode* p1 : enode_parents(n))
@@ -219,14 +221,14 @@ namespace euf {
             TRACE("bv", tout << "propagate-above " << g.bpp(b) << "\n");
             for (enode* sib : enode_class(b))
                 if (is_extract(sib, lo2, hi2) && sib->get_arg(0)->get_root() == arg_r && hi1 + 1 == lo2)
-                    ensure_concat(lo1, hi1, hi2);
+                    m_ensure_concat.push_back({lo1, hi1, hi2});
         };
 
         auto propagate_below = [&](enode* a) {
             TRACE("bv", tout << "propagate-below " << g.bpp(a) << "\n");
             for (enode* sib : enode_class(a))
                 if (is_extract(sib, lo2, hi2) && sib->get_arg(0)->get_root() == arg_r && hi2 + 1 == lo1)
-                    ensure_concat(lo2, hi2, hi1);
+                    m_ensure_concat.push_back({lo2, hi2, hi1});
         };
 
         for (enode* p : enode_parents(n)) {
@@ -237,6 +239,10 @@ namespace euf {
                     propagate_above(a);
             }
         }
+
+        for (auto [lo, mid, hi] : m_ensure_concat) 
+            ensure_concat(lo, mid, hi);
+
     }
 
     class bv_plugin::undo_split : public trail {

diff --git a/src/ast/euf/euf_bv_plugin.h b/src/ast/euf/euf_bv_plugin.h
@@ -72,6 +72,7 @@ namespace euf {
         bool unfold_width(enode* x, enode_vector& xs, enode* y, enode_vector& ys);
         bool unfold_sub(enode* x, enode_vector& xs);
         void merge(enode_vector& xs, enode_vector& ys, justification j);
+        svector<std::tuple<unsigned, unsigned, unsigned>> m_ensure_concat;
         void propagate_extract(enode* n);
         void propagate_values(enode* n);