revamp ac plugin and plugin propagation

Author: NikolajBjorner

src/ast/euf/euf_ac_plugin.cpp

@@ -36,46 +36,28 @@ namespace euf {
 
     class ac_plugin : public plugin {
 
+        struct stats {
+            unsigned m_num_superpositions = 0;// number of superpositions
+        };
+
         // enode structure for AC equivalences
         struct node {
-            enode* n;        // associated enode
-            node* root;      // path compressed root
-            node* next;      // next in equivalence class
-            justification j; // justification for equality
-            node* target = nullptr;    // justified next
+            enode* n;                  // associated enode
             unsigned_vector shared;    // shared occurrences
             unsigned_vector eqs;       // equality occurrences
+            bool is_zero = false;
 
-            unsigned id() const { return root->n->get_id(); }
+            unsigned id() const { return n->get_id(); }
             static node* mk(region& r, enode* n);
         };
 
-        class equiv {
-            node& n;
-        public:
-            class iterator {
-                node* m_first;
-                node* m_last;
-            public:
-                iterator(node* n, node* m) : m_first(n), m_last(m) {}
-                node* operator*() { return m_first; }
-                iterator& operator++() { if (!m_last) m_last = m_first; m_first = m_first->next; return *this; }
-                iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; }
-                bool operator!=(iterator const& other) const { return m_last != other.m_last || m_first != other.m_first; }
-            };
-            equiv(node& _n) :n(_n) {}
-            equiv(node* _n) :n(*_n) {}
-            iterator begin() const { return iterator(&n, nullptr); }
-            iterator end() const { return iterator(&n, &n); }
-        };
-
         struct bloom {
             uint64_t m_tick = 0;
             uint64_t m_filter = 0;
         };
 
         enum eq_status {
-            processed, to_simplify, is_dead
+            processed, to_simplify, is_reducing_eq, is_dead
         };
 
         // represent equalities added by merge_eh and by superposition
@@ -150,6 +132,10 @@ namespace euf {
         tracked_uint_set         m_shared_todo;
         uint64_t                 m_tick = 1;
         symbol                   m_name;
+        unsigned                 m_fuel = 0;
+        unsigned                 m_fuel_inc = 3;
+        stats                    m_stats;
+        mutable symbol           m_superposition_stats, m_eqs_stats;
 
 
 
@@ -163,7 +149,6 @@ namespace euf {
             is_add_eq,
             is_add_monomial,
             is_add_node,
-            is_merge_node,
             is_update_eq,
             is_add_shared_index,
             is_add_eq_index,
@@ -200,14 +185,35 @@ namespace euf {
         bool can_be_subset(monomial_t& subset, ptr_vector<node> const& m, bloom& b);
         bool are_equal(ptr_vector<node> const& a, ptr_vector<node> const& b);
         bool are_equal(monomial_t& a, monomial_t& b);
+        bool are_equal(eq const& a, eq const& b)  {
+            return are_equal(monomial(a.l), monomial(b.l)) && are_equal(monomial(a.r), monomial(b.r));
+        }
+        bool well_formed(eq const& e) const;
+        bool is_reducing(eq const& e) const;
+        void forward_reduce(unsigned eq_id);
+        void forward_reduce(eq const& src, unsigned dst);
+        bool forward_reduce_monomial(eq const& eq, monomial_t& m);
+        void backward_subsume_new_eqs();
+        bool is_backward_subsumed(unsigned dst_eq);
         bool backward_subsumes(unsigned src_eq, unsigned dst_eq);
         bool forward_subsumes(unsigned src_eq, unsigned dst_eq);
 
-        void init_equation(eq const& e);
+        enode_vector m_units;
+        enode* get_unit(enode* n) const {
+            for (auto u : m_units) {
+                if (u->get_sort() == n->get_sort())
+                    return u;
+            }
+            UNREACHABLE();
+            return nullptr;
+        }
+        
+        bool init_equation(eq const& e);
         bool orient_equation(eq& e);
         void set_status(unsigned eq_id, eq_status s);
         unsigned pick_next_eq();
 
+        unsigned_vector m_new_eqs;
         void forward_simplify(unsigned eq_id, unsigned using_eq);
         bool backward_simplify(unsigned eq_id, unsigned using_eq);
         bool superpose(unsigned src_eq, unsigned dst_eq);
@@ -249,6 +255,7 @@ namespace euf {
 
         bool is_to_simplify(unsigned eq) const { return m_eqs[eq].status == eq_status::to_simplify; }
         bool is_processed(unsigned eq) const { return m_eqs[eq].status == eq_status::processed; }
+        bool is_reducing(unsigned eq) const { return m_eqs[eq].status == eq_status::is_reducing_eq; }
         bool is_alive(unsigned eq) const { return m_eqs[eq].status != eq_status::is_dead; }
 
         justification justify_rewrite(unsigned eq1, unsigned eq2);
@@ -279,6 +286,10 @@ namespace euf {
         ac_plugin(egraph& g, func_decl* f);
 
         void set_injective() { m_is_injective = true; }
+
+        void add_unit(enode*);
+
+        void add_zero(enode*);
 
         theory_id get_id() const override { return m_fid; }
 
@@ -294,6 +305,8 @@ namespace euf {
 
         std::ostream& display(std::ostream& out) const override;
 
+        void collect_statistics(statistics& st) const override;
+
         void set_undo(std::function<void(void)> u) { m_undo_notify = u; }
 
         struct eq_pp {

src/ast/euf/euf_ac_plugin.h

@@ -31,6 +31,25 @@ namespace euf {
         std::function<void(void)> umul = [&]() { m_undo.push_back(undo_t::undo_mul); };
         m_mul.set_undo(umul);
         m_add.set_injective();
+        auto e = a.mk_int(0);
+        auto n = g.find(e) ? g.find(e) : g.mk(e, 0, 0, nullptr);
+        m_add.add_unit(n);
+        m_mul.add_zero(n);
+
+        e = a.mk_real(0);
+        n = g.find(e) ? g.find(e) : g.mk(e, 0, 0, nullptr);
+        m_add.add_unit(n);
+        m_mul.add_zero(n);
+
+        e = a.mk_int(1);
+        n = g.find(e) ? g.find(e) : g.mk(e, 0, 0, nullptr);
+        m_mul.add_unit(n);
+
+        e = a.mk_real(1);
+        n = g.find(e) ? g.find(e) : g.mk(e, 0, 0, nullptr);
+        m_mul.add_unit(n);
+
+
     }    
 
     void arith_plugin::register_node(enode* n) {

src/ast/euf/euf_arith_plugin.cpp

@@ -46,6 +46,11 @@ namespace euf {
         void propagate() override;
 
         std::ostream& display(std::ostream& out) const override;
+
+        void collect_statistics(statistics& st) const override {
+            m_add.collect_statistics(st);
+            m_mul.collect_statistics(st);
+        }
 
     };
 }

src/ast/euf/euf_arith_plugin.h

@@ -117,6 +117,7 @@ namespace euf {
 
     enode* egraph::mk(expr* f, unsigned generation, unsigned num_args, enode *const* args) {
         SASSERT(!find(f));
+        TRACE(euf, tout << "mk: " << mk_bounded_pp(f, m) << " generation: " << generation << " num_args: " << num_args << "\n";);
         force_push();
         enode *n = mk_enode(f, generation, num_args, args);
 
@@ -157,6 +158,21 @@ namespace euf {
     }
 
     void egraph::propagate_plugins() {
+        if (m_plugins.empty())
+            return;
+        if (m_plugin_qhead < m_new_th_eqs.size())
+            m_updates.push_back(update_record(m_plugin_qhead, update_record::plugin_qhead()));
+
+        for (; m_plugin_qhead < m_new_th_eqs.size(); ++m_plugin_qhead) {
+            auto const& eq = m_new_th_eqs[m_plugin_qhead];
+            auto* p = get_plugin(eq.id());
+            if (!p)
+                continue;
+            if (eq.is_eq()) 
+                p->merge_eh(eq.child(), eq.root());            
+            else 
+                p->diseq_eh(eq.eq());
+        }
         for (auto* p : m_plugins)
             if (p)
                 p->propagate();        
@@ -167,23 +183,18 @@ namespace euf {
         m_new_th_eqs.push_back(th_eq(id, v1, v2, c, r));
         m_updates.push_back(update_record(update_record::new_th_eq()));
         ++m_stats.m_num_th_eqs;
-        auto* p = get_plugin(id);
-        if (p)
-            p->merge_eh(c, r);
     }
 
     void egraph::add_th_diseq(theory_id id, theory_var v1, theory_var v2, enode* eq) {
         if (!th_propagates_diseqs(id))
             return;
         TRACE(euf_verbose, tout << "eq: " << v1 << " != " << v2 << "\n";);
-        m_new_th_eqs.push_back(th_eq(id, v1, v2, eq->get_expr()));
+        m_new_th_eqs.push_back(th_eq(id, v1, v2, eq));
         m_updates.push_back(update_record(update_record::new_th_eq()));
-        auto* p = get_plugin(id);
-        if (p)
-            p->diseq_eh(eq);
+
         ++m_stats.m_num_th_diseqs;
     }
-
+    
     void egraph::add_literal(enode* n, enode* ante) {
         TRACE(euf, tout << "propagate " << bpp(n) << " " << bpp(ante) << "\n");
         if (!m_on_propagate_literal)
@@ -447,6 +458,9 @@ namespace euf {
             case update_record::tag_t::is_new_th_eq_qhead:
                 m_new_th_eqs_qhead = p.qhead;
                 break;
+            case update_record::tag_t::is_plugin_qhead:
+                m_plugin_qhead = p.qhead;
+                break;
             case update_record::tag_t::is_inconsistent:
                 m_inconsistent = p.m_inconsistent;
                 break;
@@ -546,16 +560,18 @@ namespace euf {
     void egraph::remove_parents(enode* r) {
         TRACE(euf_verbose, tout << bpp(r) << "\n");
         SASSERT(all_of(enode_parents(r), [&](enode* p) { return !p->is_marked1(); }));
+        TRACE(euf, tout << "remove_parents " << bpp(r) << "\n");
         for (enode* p : enode_parents(r)) {
             if (p->is_marked1())
                 continue;
             if (p->cgc_enabled()) {
                 if (!p->is_cgr())
                     continue;
+                TRACE(euf, tout << "removing " << m_table.contains_ptr(p) << " " << bpp(p) << "\n");
                 SASSERT(m_table.contains_ptr(p));
                 p->mark1();
                 erase_from_table(p);
-                CTRACE(euf_verbose, m_table.contains_ptr(p), tout << bpp(p) << "\n"; display(tout));
+                CTRACE(euf, m_table.contains_ptr(p), tout << bpp(p) << "\n"; display(tout));
                 SASSERT(!m_table.contains_ptr(p));
             }
             else if (p->is_equality())
@@ -564,15 +580,16 @@ namespace euf {
     }
 
     void egraph::reinsert_parents(enode* r1, enode* r2) {
+        TRACE(euf, tout << "reinsert_parents " << bpp(r1) << " " << bpp(r2) << "\n";);
         for (enode* p : enode_parents(r1)) {
             if (!p->is_marked1())
                 continue;
             p->unmark1();
-            TRACE(euf_verbose, tout << "reinsert " << bpp(r1) << " " << bpp(r2) << " " << bpp(p) << " " << p->cgc_enabled() << "\n";);
+            TRACE(euf, tout << "reinsert " << bpp(r1) << " " << bpp(r2) << " " << bpp(p) << " " << p->cgc_enabled() << "\n";);
             if (p->cgc_enabled()) {
                 auto [p_other, comm] = insert_table(p);
                 SASSERT(m_table.contains_ptr(p) == (p_other == p));
-                CTRACE(euf_verbose, p_other != p, tout << "reinsert " << bpp(p) << " == " << bpp(p_other) << " " << p->value() << " " << p_other->value() << "\n");
+                CTRACE(euf, p_other != p, tout << "reinsert " << bpp(p) << " == " << bpp(p_other) << " " << p->value() << " " << p_other->value() << "\n");
                 if (p_other != p) 
                     m_to_merge.push_back(to_merge(p_other, p, comm));                
                 else
@@ -957,6 +974,9 @@ namespace euf {
         st.update("euf propagations theory eqs", m_stats.m_num_th_eqs);
         st.update("euf propagations theory diseqs", m_stats.m_num_th_diseqs);
         st.update("euf propagations literal", m_stats.m_num_lits);
+        for (auto p : m_plugins) 
+            if (p) 
+                p->collect_statistics(st);                   
     }
 
     void egraph::copy_from(egraph const& src, std::function<void*(void*)>& copy_justification) {

src/ast/euf/euf_egraph.cpp

@@ -58,7 +58,7 @@ namespace euf {
         theory_var m_v2;
         union {            
             enode* m_child;
-            expr* m_eq;
+            enode* m_eq;
         };
         enode* m_root;
     public:
@@ -68,10 +68,10 @@ namespace euf {
         theory_var v2() const { return m_v2; }
         enode* child() const { SASSERT(is_eq()); return m_child; }
         enode* root() const { SASSERT(is_eq()); return m_root; }
-        expr* eq() const { SASSERT(!is_eq()); return m_eq; }
+        enode* eq() const { SASSERT(!is_eq()); return m_eq; }
         th_eq(theory_id id, theory_var v1, theory_var v2, enode* c, enode* r) :
             m_id(id), m_v1(v1), m_v2(v2), m_child(c), m_root(r) {}
-        th_eq(theory_id id, theory_var v1, theory_var v2, expr* eq) :
+        th_eq(theory_id id, theory_var v1, theory_var v2, enode* eq) :
             m_id(id), m_v1(v1), m_v2(v2), m_eq(eq), m_root(nullptr) {}
     };
 
@@ -116,6 +116,7 @@ namespace euf {
             struct replace_th_var {};
             struct new_th_eq {};
             struct new_th_eq_qhead {};
+            struct plugin_qhead {};
             struct inconsistent {};
             struct value_assignment {};
             struct lbl_hash {};
@@ -125,7 +126,7 @@ namespace euf {
             struct plugin_undo {};
             enum class tag_t { is_set_parent, is_add_node, is_toggle_cgc, is_toggle_merge_tf, is_update_children,
                     is_add_th_var, is_replace_th_var, is_new_th_eq,
-                    is_lbl_hash, is_new_th_eq_qhead,
+                    is_lbl_hash, is_new_th_eq_qhead, is_plugin_qhead,
                     is_inconsistent, is_value_assignment, is_lbl_set, is_set_relevant,
                     is_plugin_undo };
             tag_t  tag;
@@ -158,6 +159,8 @@ namespace euf {
                 tag(tag_t::is_new_th_eq), r1(nullptr), n1(nullptr), r2_num_parents(0) {}
             update_record(unsigned qh, new_th_eq_qhead):
                 tag(tag_t::is_new_th_eq_qhead), r1(nullptr), n1(nullptr), qhead(qh) {}
+            update_record(unsigned qh, plugin_qhead) :
+                tag(tag_t::is_plugin_qhead), r1(nullptr), n1(nullptr), qhead(qh) {}
             update_record(bool inc, inconsistent) :
                 tag(tag_t::is_inconsistent), r1(nullptr), n1(nullptr), m_inconsistent(inc) {}
             update_record(enode* n, value_assignment) :
@@ -196,6 +199,7 @@ namespace euf {
         enode                  *m_n2 = nullptr;
         justification          m_justification;
         unsigned               m_new_th_eqs_qhead = 0;
+        unsigned               m_plugin_qhead = 0;
         svector<th_eq>         m_new_th_eqs;
         bool_vector            m_th_propagates_diseqs;
         enode_vector           m_todo;

src/ast/euf/euf_egraph.h

@@ -35,7 +35,7 @@ namespace euf {
     void plugin::push_merge(enode* a, enode* b) {
         if (a->get_root() == b->get_root())
             return; // already merged
-        TRACE(plugin, tout << g.bpp(a) << " == " << g.bpp(b) << "\n");
+        TRACE(plugin, tout << "push-merge " << g.bpp(a) << " == " << g.bpp(b) << "\n");
         g.push_merge(a, b, justification::axiom(get_id()));
     }
 

src/ast/euf/euf_plugin.cpp

@@ -19,6 +19,7 @@ Module Name:
 
 #pragma once
 
+#include "util/statistics.h"
 #include "ast/euf/euf_enode.h"
 #include "ast/euf/euf_justification.h"
 
@@ -53,6 +54,8 @@ namespace euf {
         virtual void undo() = 0;
 
         virtual std::ostream& display(std::ostream& out) const = 0;
+
+        virtual void collect_statistics(statistics& st) const {}
 
     };
 }