port updates to egraph from poly

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Author: NikolajBjorner

src/ast/euf/euf_ac_plugin.cpp

@@ -109,7 +109,7 @@ namespace euf {
         m_shared_nodes.setx(n->get_id(), true, false);
         sort(monomial(m));
         m_shared_todo.insert(m_shared.size());
-        m_shared.push_back({ n, m, justification::axiom() });
+        m_shared.push_back({ n, m, justification::axiom(get_id()) });
         push_undo(is_register_shared);
     }
 

src/ast/euf/euf_ac_plugin.h

@@ -137,7 +137,7 @@ namespace euf {
             }
         };
 
-        unsigned                 m_fid = 0;
+        theory_id                m_fid = 0;
         unsigned                 m_op = null_decl_kind;
         func_decl*               m_decl = nullptr;
         vector<eq>               m_eqs;
@@ -273,7 +273,7 @@ namespace euf {
 
         ~ac_plugin() override {}
 
-        unsigned get_id() const override { return m_fid; }
+        theory_id get_id() const override { return m_fid; }
 
         void register_node(enode* n) override;
 

src/ast/euf/euf_arith_plugin.h

@@ -35,7 +35,7 @@ namespace euf {
 
         ~arith_plugin() override {}
 
-        unsigned get_id() const override { return a.get_family_id(); }
+        theory_id get_id() const override { return a.get_family_id(); }
 
         void register_node(enode* n) override;
 

src/ast/euf/euf_bv_plugin.cpp

@@ -161,20 +161,27 @@ namespace euf {
     void bv_plugin::propagate_values(enode* x) {
         if (!is_value(x))
             return;
-        
+
+        auto val_x = get_value(x);
         enode* a, * b;
-        for (enode* p : enode_parents(x))
-            if (is_concat(p, a, b) && is_value(a) && is_value(b) && !is_value(p))
+        unsigned lo, hi;
+        for (enode* p : enode_parents(x)) {
+            if (is_concat(p, a, b) && is_value(a) && is_value(b))
                 push_merge(mk_concat(a->get_interpreted(), b->get_interpreted()), mk_value_concat(a, b));
-        
+
+            if (is_extract(p, lo, hi)) {
+                auto val_p = mod2k(machine_div2k(val_x, lo), hi - lo + 1);
+                auto ix = x->get_interpreted();
+                auto ex = mk(bv.mk_extract(hi, lo, ix->get_expr()), 1, &ix);
+                push_merge(ex, mk_value(val_p, width(p)));
+            }
+        }
+
         for (enode* sib : enode_class(x)) {
             if (is_concat(sib, a, b)) {
-                if (!is_value(a) || !is_value(b)) {
-                    auto val = get_value(x);
-                    auto val_a = machine_div2k(val, width(b));
-                    auto val_b = mod2k(val, width(b));
-                    push_merge(mk_concat(mk_value(val_a, width(a)), mk_value(val_b, width(b))), x->get_interpreted());
-                }
+                auto val_a = machine_div2k(val_x, width(b));
+                auto val_b = mod2k(val_x, width(b));
+                push_merge(mk_concat(mk_value(val_a, width(a)), mk_value(val_b, width(b))), x->get_interpreted());
             }
         }
     }
@@ -198,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))
@@ -212,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)) {
@@ -230,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 {
@@ -432,13 +445,14 @@ namespace euf {
                         delta += width(arg);
                     }
                 }
-            }
-            for (auto p : euf::enode_parents(n->get_root())) {
-                if (bv.is_extract(p->get_expr(), lo, hi, e)) {
-                    SASSERT(g.find(e)->get_root() == n->get_root());
-                    m_todo.push_back({ p, offset + lo });
+                for (auto p : euf::enode_parents(sib)) {
+                    if (bv.is_extract(p->get_expr(), lo, hi, e)) {
+                        SASSERT(g.find(e)->get_root() == n->get_root());
+                        m_todo.push_back({ p, offset + lo });
+                    }
                 }
             }
+
         }
         clear_offsets();
     }
@@ -462,17 +476,17 @@ namespace euf {
                     auto child = g.find(e);
                     m_todo.push_back({ child, offset + lo });
                 }
-            }
-            for (auto p : euf::enode_parents(n->get_root())) {
-                if (bv.is_concat(p->get_expr())) {
-                    unsigned delta = 0;
-                    for (unsigned j = p->num_args(); j-- > 0; ) {
-                        auto arg = p->get_arg(j);
-                        if (arg->get_root() == n->get_root()) 
-                            m_todo.push_back({ p, offset + delta });
-                        delta += width(arg);                   
+                for (auto p : euf::enode_parents(sib)) {
+                    if (bv.is_concat(p->get_expr())) {
+                        unsigned delta = 0;
+                        for (unsigned j = p->num_args(); j-- > 0; ) {
+                            auto arg = p->get_arg(j);
+                            if (arg->get_root() == n->get_root())
+                                m_todo.push_back({ p, offset + delta });
+                            delta += width(arg);
+                        }
                     }
-                }
+                }            
             }
         }
         clear_offsets();
@@ -511,6 +525,9 @@ namespace euf {
                     m_offsets.reserve(n->get_root_id() + 1);
                     m_offsets[n->get_root_id()].reset();
                 }
+                for (auto const& off : m_offsets) {
+                    SASSERT(off.empty());
+                }
                 m_jtodo.reset();
                 return;
             }
@@ -521,20 +538,27 @@ namespace euf {
                     just.push_back({ n, sib, j });
                     for (unsigned j = sib->num_args(); j-- > 0; ) {
                         auto arg = sib->get_arg(j);
-                        m_jtodo.push_back({ arg, offset + delta, j2 });
+                        m_jtodo.push_back({ arg, offs + delta, j2 });
                         delta += width(arg);
                     }
                 }
-            }
-            for (auto p : euf::enode_parents(n->get_root())) {
-                if (bv.is_extract(p->get_expr(), lo, hi, e)) {
-                    SASSERT(g.find(e)->get_root() == n->get_root());
-                    unsigned j2 = just.size();
-                    just.push_back({ g.find(e), n, j});
-                    m_jtodo.push_back({ p, offset + lo, j2});
+                for (auto p : euf::enode_parents(sib)) {
+                    if (bv.is_extract(p->get_expr(), lo, hi, e)) {
+                        SASSERT(g.find(e)->get_root() == n->get_root());
+                        unsigned j2 = just.size();
+                        just.push_back({ g.find(e), n, j });
+                        m_jtodo.push_back({ p, offs + lo, j2 });
+                    }
                 }
             }
+
         }
+        IF_VERBOSE(0,
+            g.display(verbose_stream());
+            verbose_stream() << g.bpp(a) << " offset " << offset << " " << g.bpp(b) << "\n";
+            for (auto const& [n, offset, j] : m_jtodo) 
+                verbose_stream() << g.bpp(n) << " offset " << offset << " " << g.bpp(n->get_root()) << "\n";            
+        );
         UNREACHABLE();
     }
 

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);
 
@@ -96,7 +97,7 @@ namespace euf {
 
         ~bv_plugin() override {}
 
-        unsigned get_id() const override { return bv.get_family_id(); }
+        theory_id get_id() const override { return bv.get_family_id(); }
 
         void register_node(enode* n) override;
 

src/ast/euf/euf_enode.cpp

@@ -135,7 +135,7 @@ namespace euf {
         enode* prev = this;
         justification js = m_justification;
         prev->m_target = nullptr;
-        prev->m_justification = justification::axiom();
+        prev->m_justification = justification::axiom(null_theory_id);
         while (curr != nullptr) {
             enode* new_curr = curr->m_target;
             justification new_js = curr->m_justification;

src/ast/euf/euf_enode.h

@@ -36,10 +36,6 @@ namespace euf {
     typedef std::pair<enode*,bool> enode_bool_pair;
     typedef svector<enode_bool_pair> enode_bool_pair_vector;
     typedef id_var_list<> th_var_list;
-    typedef int theory_var;
-    typedef int theory_id;
-    const theory_var null_theory_var = -1;
-    const theory_id null_theory_id = -1;
 
     class enode {
         expr*         m_expr = nullptr;

src/ast/euf/euf_justification.h

@@ -28,6 +28,11 @@ namespace euf {
 
     class enode;
 
+    typedef int theory_var;
+    typedef int theory_id;
+    const theory_var null_theory_var = -1;
+    const theory_id null_theory_id = -1;
+
     class justification {
     public:
         typedef stacked_dependency_manager<justification>             dependency_manager;
@@ -42,6 +47,7 @@ namespace euf {
         };
         kind_t m_kind;
         union {
+            int    m_theory_id;
             bool   m_comm;
             enode* m_n1;
         };
@@ -76,19 +82,27 @@ namespace euf {
             m_n2(n2)
         {}
 
+        justification(int theory_id):
+            m_kind(kind_t::axiom_t),
+            m_theory_id(theory_id),
+            m_external(nullptr)
+        {}
+
     public:
+
         justification():
             m_kind(kind_t::axiom_t),
-            m_comm(false),
+            m_theory_id(null_theory_id),
             m_external(nullptr)
         {}
 
-        static justification axiom() { return justification(); }
+        static justification axiom(int theory_id) { return justification(theory_id); }
         static justification congruence(bool c, uint64_t ts) { return justification(c, ts); }
         static justification external(void* ext) { return justification(ext); }
         static justification dependent(dependency* d) { return justification(d, 1); }
         static justification equality(enode* a, enode* b) { return justification(a, b); }
 
+        bool   is_axiom() const { return m_kind == kind_t::axiom_t; }
         bool   is_external() const { return m_kind == kind_t::external_t; }
         bool   is_congruence() const { return m_kind == kind_t::congruence_t; }
         bool   is_commutative() const { return m_comm; }
@@ -98,6 +112,7 @@ namespace euf {
         enode* lhs() const { SASSERT(is_equality()); return m_n1; }
         enode* rhs() const { SASSERT(is_equality()); return m_n2; }
         uint64_t timestamp() const { SASSERT(is_congruence()); return m_timestamp; }
+        theory_id get_theory_id() const { SASSERT(is_axiom()); return m_theory_id; }
         template <typename T>
         T*  ext() const { SASSERT(is_external()); return static_cast<T*>(m_external); }            
 
@@ -106,15 +121,15 @@ namespace euf {
             case kind_t::external_t:
                 return external(copy_justification(m_external));
             case kind_t::axiom_t:
-                return axiom();
+                return axiom(m_theory_id);
             case kind_t::congruence_t:
                 return congruence(m_comm, m_timestamp);
             case kind_t::dependent_t:
                 NOT_IMPLEMENTED_YET();
                 return dependent(m_dependency);
             default:
                 UNREACHABLE();
-                return axiom();
+                return axiom(-1);
             }
         }
 

src/ast/euf/euf_plugin.cpp

@@ -26,12 +26,13 @@ namespace euf {
     }
 
     void plugin::push_merge(enode* a, enode* b, justification j) {
+        TRACE("euf", tout << "push-merge " << g.bpp(a) << " == " << g.bpp(b) << " " << j << "\n");
         g.push_merge(a, b, j);
     }
 
     void plugin::push_merge(enode* a, enode* b) {
         TRACE("plugin", tout << g.bpp(a) << " == " << g.bpp(b) << "\n");
-        g.push_merge(a, b, justification::axiom());
+        g.push_merge(a, b, justification::axiom(get_id()));
     }
 
     enode* plugin::mk(expr* e, unsigned n, enode* const* args) {

src/ast/euf/euf_plugin.h

@@ -40,7 +40,7 @@ namespace euf {
 
         virtual ~plugin() {}
 
-        virtual unsigned get_id() const = 0;
+        virtual theory_id get_id() const = 0;
 
         virtual void register_node(enode* n) = 0;
 

src/ast/euf/euf_specrel_plugin.h

@@ -37,7 +37,7 @@ namespace euf {
 
         ~specrel_plugin() override {}
 
-        unsigned get_id() const override { return sp.get_family_id(); }
+        theory_id get_id() const override { return sp.get_family_id(); }
 
         void register_node(enode* n) override;