updates to AC plugin, notes in BV plugin

src/ast/euf/euf_ac_plugin.cpp

@@ -41,6 +41,18 @@ More notes:
   Shared occurrences are rewritten modulo completion.
   When equal to a different shared occurrence, propagate equality.
 
+TODOs:
+- Establish / fix formal termination properties in the presence of union-find.
+  The formal interactions between union find and orienting the equations need to be established.  
+  - Union-find merges can change the orientation of an equation and break termination.
+  - For example, rules are currently not re-oriented if there is a merge. The rules could be re-oriented during propagation.
+- Elimination of redundant rules.
+  - superposition uses a stop-gap to avoid some steps. It should be revisited.
+- Efficiency of handling shared terms.
+  - The shared terms hash table is not incremental. 
+    It could be made incremental by updating it on every merge similar to how the egraph handles it.
+- V2 using multiplicities instead of repeated values in monomials.
+
 --*/
 
 #include "ast/euf/euf_ac_plugin.h"
@@ -49,11 +61,13 @@ More notes:
 namespace euf {
 
     ac_plugin::ac_plugin(egraph& g, unsigned fid, unsigned op):
-        plugin(g), m_fid(fid), m_op(op)
+        plugin(g), m_fid(fid), m_op(op),
+        m_dep_manager(get_region()),
+        m_hash(*this), m_eq(*this), m_monomial_table(m_hash, m_eq)
     {}
 
     void ac_plugin::register_node(enode* n) {
-        
+        // no-op
     }
 
     void ac_plugin::register_shared(enode* n) {
@@ -64,8 +78,9 @@ namespace euf {
             m_node_trail.push_back(arg);
             push_undo(is_add_shared);
         }
-        m_shared_trail.push_back(m);
-        m_shared_find.setx(m, m, 0);
+        sort(monomial(m));
+        m_shared.push_back({ n, m, justification::axiom() });
+        m_shared_todo.insert(m);
         push_undo(is_register_shared);
     }
 
@@ -91,7 +106,6 @@ namespace euf {
         }
         case is_add_monomial: {         
             m_monomials.pop_back();
-            m_monomial_enodes.pop_back();
             break;
         }
         case is_merge_node: {
@@ -117,17 +131,13 @@ namespace euf {
             break;
         }
         case is_register_shared: {
-            m_shared_trail.pop_back();
+            m_shared.pop_back();
             break;
         }
-        case is_join_justification: {
-            m_dep_manager.pop_scope(1);
-            break;
-        }
-        case is_update_shared_find: {
-            auto [id, old_id] = m_shared_find_trail.back();
-            m_shared_find[id] = old_id;
-            m_shared_find_trail.pop_back();
+        case is_update_shared: {
+            auto [id, s] = m_update_shared_trail.back();
+            m_shared[id] = s;
+            m_update_shared_trail.pop_back();
             break;
         }
         default:
@@ -135,7 +145,7 @@ namespace euf {
         }
     }
 
-    std::ostream& ac_plugin::display_monomial(std::ostream& out, ptr_vector<node> const& m) const {
+    std::ostream& ac_plugin::display_monomial(std::ostream& out, monomial_t const& m) const {
         for (auto n : m)
             out << g.bpp(n->n) << " ";
         return out;
@@ -216,8 +226,8 @@ namespace euf {
             return true;
         }
         else {
-            std::sort(ml.begin(), ml.end(), [&](node* a, node* b) { return a->root_id() < b->root_id(); });
-            std::sort(mr.begin(), mr.end(), [&](node* a, node* b) { return a->root_id() < b->root_id(); });
+            sort(ml);
+            sort(mr);
             for (unsigned i = ml.size(); i-- > 0;) {
                 if (ml[i] == mr[i])
                     continue;
@@ -229,6 +239,17 @@ namespace euf {
         }
     }
 
+    void ac_plugin::sort(monomial_t& m) {
+        std::sort(m.begin(), m.end(), [&](node* a, node* b) { return a->root_id() < b->root_id(); });
+    }
+
+    bool ac_plugin::is_sorted(monomial_t const& m) const {
+        for (unsigned i = m.size(); i-- > 1; ) 
+            if (m[i-1]->root_id() > m[i]->root_id())
+                return false;        
+        return true;
+    }
+
     void ac_plugin::merge(node* root, node* other, justification j) {
         for (auto n : equiv(other))
             n->root = root;
@@ -237,6 +258,8 @@ namespace euf {
             set_processed(eq_id, false);
         for (auto eq_id : other->rhs)
             set_processed(eq_id, false);
+        for (auto m : other->shared)
+            m_shared_todo.insert(m);
         root->shared.append(other->shared);
         root->lhs.append(other->lhs);
         root->rhs.append(other->rhs);
@@ -270,10 +293,9 @@ namespace euf {
         return to_monomial(n, ms);
     }
 
-    unsigned ac_plugin::to_monomial(enode* e, ptr_vector<node> const& ms) {
+    unsigned ac_plugin::to_monomial(enode* e, monomial_t const& ms) {
         unsigned id = m_monomials.size();
         m_monomials.push_back(ms);
-        m_monomial_enodes.push_back(e);
         push_undo(is_add_monomial);
         return id;
     }
@@ -502,7 +524,7 @@ namespace euf {
         m_backward_simplified = true;
     }
 
-    unsigned ac_plugin::rewrite(ptr_vector<node> const& src_r, ptr_vector<node> const& dst_r) {
+    unsigned ac_plugin::rewrite(monomial_t const& src_r, monomial_t const& dst_r) {
         // pre-condition: is-subset is invoked so that m_src_count is initialized.
         // pre-condition: m_dst_count is also initialized (once).
         m_src_r.reset();
@@ -519,7 +541,7 @@ namespace euf {
         return to_monomial(nullptr, m_src_r);
     }
 
-    bool ac_plugin::is_subset(ptr_vector<node> const& dst) {
+    bool ac_plugin::is_subset(monomial_t const& dst) {
         reset_ids_counts(m_src_ids, m_src_count);
         for (auto n : dst) {
             unsigned id = n->root_id();
@@ -620,32 +642,61 @@ namespace euf {
     // simple version based on propagating all shared
     // todo: version touching only newly processed shared, and maintaining incremental data-structures.
     //       - hash-tables for shared monomials similar to the ones used for euf_table.
-    //       -  m_shared_todo : tracked_uint_set set of monomials that have elements that can be simplified.
-    //          set is updated when nodes are merged, similar to updates of to_simplify
+    //         the tables have to be updated (and re-sorted) whenever a child changes root.
     // 
 
     void ac_plugin::propagate_shared() {
-        for (auto m : m_shared_trail)
-            simplify_shared(m);
-        // check for collisions, push_merge when there is a collision.
+        if (m_shared_todo.empty())
+            return;
+        while (!m_shared_todo.empty()) {
+            auto idx = *m_shared_todo.begin();
+            m_shared_todo.remove(idx);
+            if (idx < m_shared.size()) 
+                simplify_shared(idx, m_shared[idx]);
+        }
+        m_monomial_table.reset();
+        for (auto const& s1 : m_shared) {
+            shared s2;
+            if (m_monomial_table.find(s1.m, s2)) {
+                if (s2.n->get_root() != s1.n->get_root())
+                    push_merge(s1.n, s2.n, justification::dependent(m_dep_manager.mk_join(m_dep_manager.mk_leaf(s1.j), m_dep_manager.mk_leaf(s2.j))));
+            }
+            else 
+                m_monomial_table.insert(s1.m, s1);
+        }
     }
 
-    void ac_plugin::simplify_shared(unsigned monomial_id) {
-        unsigned m_id = monomial_id;
+    void ac_plugin::simplify_shared(unsigned idx, shared s) {
         bool change = true;
         while (change) {
             change = false;
-            auto const& m = monomial(m_shared_find[monomial_id]);
+            auto const& m = monomial(s.m);
             init_ids_counts(m, m_dst_ids, m_dst_count);
             init_overlap_iterator(UINT_MAX, m);
             for (auto eq : m_lhs_eqs) {
                 auto& src = m_eqs[eq];
                 if (!is_subset(monomial(src.l)))
                     continue;
-                m_shared_find_trail.push_back({ monomial_id, m_id });
-                m_id = rewrite(monomial(src.r), m);                
-                m_shared_find[monomial_id] = m_id;
-                push_undo(is_update_shared_find);
+                m_update_shared_trail.push_back({ idx, s });
+                push_undo(is_update_shared);
+                unsigned new_m = rewrite(monomial(src.r), m);
+                m_shared[idx].m = new_m;
+                m_shared[idx].j = justification::dependent(m_dep_manager.mk_join(m_dep_manager.mk_leaf(s.j), justify_equation(eq)));
+                
+                // update shared occurrences for members of the new monomial that are not already in the old monomial.
+                for (auto n : monomial(s.m))
+                    n->root->n->mark1();
+                for (auto n : monomial(new_m))
+                    if (!n->root->n->is_marked1()) {
+                        n->root->shared.push_back(s.m);
+                        m_shared_todo.insert(s.m);
+                        m_node_trail.push_back(n->root);
+                        push_undo(is_add_shared);
+                    }
+                for (auto n : monomial(s.m))
+                    n->root->n->unmark1();
+
+                s = m_shared[idx];
                 change = true;
                 break;
             }
@@ -653,19 +704,19 @@ namespace euf {
     }
 
     justification ac_plugin::justify_rewrite(unsigned eq1, unsigned eq2) {
-        auto const& e1 = m_eqs[eq1];
-        auto const& e2 = m_eqs[eq2];
-        auto* j = m_dep_manager.mk_join(m_dep_manager.mk_leaf(e1.j), m_dep_manager.mk_leaf(e2.j));        
-        j = justify_monomial(j, monomial(e1.l));
-        j = justify_monomial(j, monomial(e1.r));
-        j = justify_monomial(j, monomial(e2.l));
-        j = justify_monomial(j, monomial(e2.r));
-        m_dep_manager.push_scope();
-        push_undo(is_join_justification);
+        auto* j = m_dep_manager.mk_join(justify_equation(eq1), justify_equation(eq2));
         return justification::dependent(j);
     }
 
-    justification::dependency* ac_plugin::justify_monomial(justification::dependency* j, ptr_vector<node> const& m) {
+    justification::dependency* ac_plugin::justify_equation(unsigned eq) {
+        auto const& e = m_eqs[eq];
+        auto* j = m_dep_manager.mk_leaf(e.j);
+        j = justify_monomial(j, monomial(e.l));
+        j = justify_monomial(j, monomial(e.r));
+        return j;
+    }
+
+    justification::dependency* ac_plugin::justify_monomial(justification::dependency* j, monomial_t const& m) {
         for (auto n : m)
             if (n->root->n != n->n)
                 j = m_dep_manager.mk_join(j, m_dep_manager.mk_leaf(justification::equality(n->root->n, n->n)));

src/ast/euf/euf_ac_plugin.h

@@ -71,21 +71,64 @@ namespace euf {
             iterator end() const { return iterator(&n, &n); }
         };
 
+        // represent equalities added by merge_eh and by superposition
         struct eq {
-            unsigned l, r;   // refer to monomials
-            bool is_processed = false;
-            justification j;
+            unsigned l, r;              // refer to monomials
+            bool is_processed = false;  // true if the equality is in the processed set
+            justification j;            // justification for equality
+        };
+
+        // represent shared enodes that use the AC symbol.
+        struct shared {
+            enode* n;         // original shared enode
+            unsigned m;       // monomial index
+            justification j;  // justification for current simplification of monomial
+        };
+
+        using monomial_t = ptr_vector<node>;
+
+        struct monomial_hash {
+            ac_plugin& p;
+            monomial_hash(ac_plugin& p) :p(p) {}
+            unsigned operator()(unsigned i) const {
+                unsigned h = 0;
+                auto& m = p.monomial(i);
+                if (!p.is_sorted(m))
+                    p.sort(m);
+                for (auto* n : m)
+                    h = combine_hash(h, n->root_id());
+                return h;
+            }
+        };
+
+        struct monomial_eq {
+            ac_plugin& p;
+            monomial_eq(ac_plugin& p) :p(p) {}
+            bool operator()(unsigned i, unsigned j) const {
+                auto const& m1 = p.monomial(i);
+                auto const& m2 = p.monomial(j);
+                if (m1.size() != m2.size()) return false;
+                for (unsigned k = 0; k < m1.size(); ++k)
+                    if (m1[k]->root_id() != m2[k]->root_id())
+                        return false;
+                return true;
+            }
         };
 
         unsigned                 m_fid;
         unsigned                 m_op;
         vector<eq>               m_eqs;
         ptr_vector<node>         m_nodes;
-        vector<ptr_vector<node>> m_monomials;
-        enode_vector             m_monomial_enodes;
+        vector<monomial_t>       m_monomials;
+        svector<shared>          m_shared;
         justification::dependency_manager m_dep_manager;
         tracked_uint_set         m_to_simplify_todo;
-        unsigned_vector          m_shared_find;
+        tracked_uint_set         m_shared_todo;
+
+
+        monomial_hash m_hash;
+        monomial_eq   m_eq;
+        map<unsigned, shared, monomial_hash, monomial_eq> m_monomial_table;
         
 
         // backtrackable state
@@ -97,16 +140,17 @@ namespace euf {
             is_update_eq,
             is_add_shared,
             is_register_shared,
-            is_join_justification,
-            is_update_shared_find
+            is_update_shared
         };
         svector<undo_kind>       m_undo;
         ptr_vector<node>         m_node_trail;
-        unsigned_vector          m_monomial_trail, m_shared_trail;
-        svector<std::pair<unsigned, unsigned>> m_shared_find_trail;
+
+        svector<std::pair<unsigned, shared>> m_update_shared_trail;
         svector<std::tuple<node*, unsigned, unsigned, unsigned>> m_merge_trail;
         svector<std::pair<unsigned, eq>> m_update_eq_trail;
 
+
+
         node* mk_node(enode* n);
         void merge(node* r1, node* r2, justification j);
 
@@ -116,21 +160,22 @@ namespace euf {
         void push_undo(undo_kind k);
         enode_vector m_todo;
         unsigned to_monomial(enode* n);
-        unsigned to_monomial(enode* n, ptr_vector<node> const& ms);
-        ptr_vector<node> const& monomial(unsigned i) const { return m_monomials[i]; }
-        ptr_vector<node>& monomial(unsigned i) { return m_monomials[i]; }
+        unsigned to_monomial(enode* n, monomial_t const& ms);
+        monomial_t const& monomial(unsigned i) const { return m_monomials[i]; }
+        monomial_t& monomial(unsigned i) { return m_monomials[i]; }
+        void sort(monomial_t& monomial);
+        bool is_sorted(monomial_t const& monomial) const;
 
         void init_equation(eq const& e);
         bool orient_equation(eq& e);
         void set_processed(unsigned eq_id, bool f);
         unsigned pick_next_eq();
-        bool is_trivial(unsigned eq_id) const { throw default_exception("NYI"); }
 
         void forward_simplify(unsigned eq_id, unsigned using_eq);
         void backward_simplify(unsigned eq_id, unsigned using_eq);
         void superpose(unsigned src_eq, unsigned dst_eq);
 
-        ptr_vector<node> m_src_r, m_src_l, m_dst_r;
+        monomial_t m_src_r, m_src_l, m_dst_r;
         unsigned_vector m_src_ids, m_src_count, m_dst_ids, m_dst_count;
         unsigned_vector m_lhs_eqs;
         bool_vector m_eq_seen;
@@ -139,20 +184,21 @@ namespace euf {
         unsigned_vector const& forward_iterator(unsigned eq);
         unsigned_vector const& superpose_iterator(unsigned eq);
         unsigned_vector const& backward_iterator(unsigned eq);
-        void init_ids_counts(ptr_vector<node> const& monomial, unsigned_vector& ids, unsigned_vector& counts);
+        void init_ids_counts(monomial_t const& monomial, unsigned_vector& ids, unsigned_vector& counts);
         void reset_ids_counts(unsigned_vector& ids, unsigned_vector& counts);
-        void init_overlap_iterator(unsigned eq, ptr_vector<node> const& m);
-        bool is_subset(ptr_vector<node> const& dst);
-        unsigned rewrite(ptr_vector<node> const& src_r, ptr_vector<node> const& dst_r);
+        void init_overlap_iterator(unsigned eq, monomial_t const& m);
+        bool is_subset(monomial_t const& dst);
+        unsigned rewrite(monomial_t const& src_r, monomial_t const& dst_r);
 
         bool is_to_simplify(unsigned eq) const { return !m_eqs[eq].is_processed; }
         bool is_processed(unsigned eq) const { return m_eqs[eq].is_processed; }
 
         justification justify_rewrite(unsigned eq1, unsigned eq2);
+        justification::dependency* justify_equation(unsigned eq);
         justification::dependency* justify_monomial(justification::dependency* d, ptr_vector<node> const& m);
 
         void propagate_shared();
-        void simplify_shared(unsigned monomial_id);
+        void simplify_shared(unsigned idx, shared s);
 
         std::ostream& display_monomial(std::ostream& out, ptr_vector<node> const& m) const;
         std::ostream& display_equation(std::ostream& out, eq const& e) const;

src/ast/euf/euf_bv_plugin.cpp

@@ -64,6 +64,20 @@ Example:
    by (2) => x[I123] = (x1 (x2 x3))
    by (5) => x = x[I123]
 
+The formal properties of saturation have to be established.
+
+- Saturation does not complete with respect to associativity.
+Instead the claim is along the lines that the resulting E-graph can be used as a canonizer.
+If given a set of equations E that are saturated, and terms t1, t2 that are 
+both simplified with respect to left-associativity of concatentation, and t1, t2 belong to the E-graph,
+then t1 = t2 iff t1 ~ t2 in the E-graph.
+
+TODO: Is saturation for (7) overkill for the purpose of canonization?
+
+TODO: revisit re-entrancy during register_node. It can be called when creating internal extract terms.
+Instead of allowing re-entrancy we can accumulate nodes that are registered during recursive calls 
+and have the main call perform recursive slicing.
+
 --*/
 
 

src/ast/euf/euf_justification.h

@@ -30,8 +30,8 @@ namespace euf {
 
     class justification {
     public:
-        typedef scoped_dependency_manager<justification>             dependency_manager;
-        typedef scoped_dependency_manager<justification>::dependency dependency;
+        typedef stacked_dependency_manager<justification>             dependency_manager;
+        typedef stacked_dependency_manager<justification>::dependency dependency;
     private:
         enum class kind_t {
             axiom_t, 

src/util/dependency.h

@@ -361,4 +361,83 @@ typedef scoped_dependency_manager<void*>::dependency v_dependency;
 typedef scoped_dependency_manager<unsigned>             u_dependency_manager;
 typedef scoped_dependency_manager<unsigned>::dependency u_dependency;
 
+/**
+   \brief Version of the scoped-depenendcy-manager where region scopes are handled externally.
+*/
+template<typename Value>
+class stacked_dependency_manager {
 
+    class config {
+    public:
+        static const bool ref_count = true;
+
+        typedef Value value;
+
+        class value_manager {
+        public:
+            void inc_ref(value const& v) {
+            }
+
+            void dec_ref(value const& v) {
+            }
+        };
+
+        class allocator {
+            region&   m_region;
+        public:
+            allocator(region& r) : m_region(r) {}
+
+            void* allocate(size_t sz) { 
+                return m_region.allocate(sz);
+            }            
+
+            void deallocate(size_t sz, void* mem) {
+            }
+        };
+    };
+
+    typedef dependency_manager<config>       dep_manager;
+public:
+    typedef typename dep_manager::dependency dependency;
+    typedef Value value;
+
+private:
+    typename config::value_manager m_vmanager;
+    typename config::allocator     m_allocator;
+    dep_manager                    m_dep_manager;
+
+public:
+    stacked_dependency_manager(region& r) :
+        m_allocator(r),
+        m_dep_manager(m_vmanager, m_allocator) {
+    }
+
+    dependency* mk_empty() {
+        return m_dep_manager.mk_empty();
+    }
+
+    dependency* mk_leaf(value const& v) {
+        return m_dep_manager.mk_leaf(v);
+    }
+
+    dependency* mk_join(dependency* d1, dependency* d2) {
+        return m_dep_manager.mk_join(d1, d2);
+    }
+
+    bool contains(dependency* d, value const& v) {
+        return m_dep_manager.contains(d, v);
+    }
+
+    void linearize(dependency* d, vector<value, false>& vs) {
+        return m_dep_manager.linearize(d, vs);
+    }
+
+    static vector<value, false> const& s_linearize(dependency* d, vector<value, false>& vs) {
+        dep_manager::s_linearize(d, vs);
+        return vs;
+    }
+
+    void linearize(ptr_vector<dependency>& d, vector<value, false>& vs) {
+        return m_dep_manager.linearize(d, vs);
+    }
+};