add tuned implementation

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

src/math/dd/dd_pdd.cpp

@@ -362,6 +362,13 @@ namespace dd {
         }
     }
 
+    // a = s*x + t, where s is a constant, b = u*x + v, where u is a constant.
+    // since x is the maximal variable, it does not occur in t or v.
+    // thus, both a and b are linear in x
+    bool pdd_manager::spoly_is_invertible(pdd const& a, pdd const& b) {
+        return a.is_var() && b.is_var() && a.hi().is_val() && b.hi().is_val() && a.var() == b.var();
+    }
+
     /*
      * Compare leading monomials.
      * The pdd format makes lexicographic comparison easy: compare based on
@@ -609,6 +616,38 @@ namespace dd {
         return m_tree_size[p.root];
     }
 
+    unsigned_vector const& pdd_manager::free_vars(pdd const& p) { 
+        return free_vars_except(p, zero()); 
+    }
+
+    unsigned_vector const& pdd_manager::free_vars_except(pdd const& p, pdd const& q) {
+        init_mark();
+        m_free_vars.reset();
+        m_todo.push_back(q.root);
+        while (!m_todo.empty()) {
+            PDD r = m_todo.back();
+            m_todo.pop_back();
+            if (is_val(r) || is_marked(r)) continue;            
+            set_mark(r);            
+            set_mark(m_var2pdd[var(r)]);            
+            if (!is_marked(lo(r))) m_todo.push_back(lo(r));
+            if (!is_marked(hi(r))) m_todo.push_back(hi(r));
+        }
+        m_todo.push_back(p.root);
+        while (!m_todo.empty()) {
+            PDD r = m_todo.back();
+            m_todo.pop_back();
+            if (is_val(r) || is_marked(r)) continue;
+            PDD v = m_var2pdd[var(r)];
+            if (!is_marked(v)) m_free_vars.push_back(var(r));
+            set_mark(r);
+            set_mark(v);
+            if (!is_marked(lo(r))) m_todo.push_back(lo(r));
+            if (!is_marked(hi(r))) m_todo.push_back(hi(r));
+        }
+        return m_free_vars;
+    }
+
 
     void pdd_manager::alloc_free_nodes(unsigned n) {
         for (unsigned i = 0; i < n; ++i) {

src/math/dd/dd_pdd.h

@@ -148,6 +148,7 @@ namespace dd {
         bool                       m_is_new_node;
         unsigned                   m_max_num_pdd_nodes;
         bool                       m_mod2_semantics;
+        unsigned_vector            m_free_vars;
 
         PDD make_node(unsigned level, PDD l, PDD r);
         PDD insert_node(pdd_node const& n);
@@ -221,7 +222,7 @@ namespace dd {
 
         void set_mod2_semantics() { m_mod2_semantics = true; }
         void set_max_num_nodes(unsigned n) { m_max_num_pdd_nodes = n; }
-        void set_var_order(unsigned_vector const& levels);  // TBD: set variable order (m_var2level, m_level2var) before doing anything else.
+        void set_var_order(unsigned_vector const& levels);  // TBD: set variable order (m_var2level, m_level2var) before doing anything else.        
 
         pdd mk_var(unsigned i);
         pdd mk_val(rational const& r);
@@ -234,11 +235,19 @@ namespace dd {
         pdd mul(pdd const& a, pdd const& b);
         pdd mul(rational const& c, pdd const& b);
         pdd reduce(pdd const& a, pdd const& b);
+
+        // create an spoly r if leading monomials of a and b overlap
         bool try_spoly(pdd const& a, pdd const& b, pdd& r);
+
+        // true if b can be computed using a and the result of spoly
+        bool spoly_is_invertible(pdd const& a, pdd const& b);
         bool lt(pdd const& a, pdd const& b);
         bool different_leading_term(pdd const& a, pdd const& b);
         double tree_size(pdd const& p);
 
+        unsigned_vector const& free_vars(pdd const& p);
+        unsigned_vector const& free_vars_except(pdd const& p, pdd const& q);
+
         std::ostream& display(std::ostream& out);
         std::ostream& display(std::ostream& out, pdd const& b);
 
@@ -260,6 +269,7 @@ namespace dd {
         pdd hi() const { return pdd(m->hi(root), m); }
         unsigned var() const { return m->var(root); }
         rational const& val() const { SASSERT(is_val()); return m->val(root); }
+        bool is_var() const { return !m->is_val(root); }
         bool is_val() const { return m->is_val(root); }
         bool is_zero() const { return m->is_zero(root); }
 

src/math/grobner/pdd_grobner.cpp

@@ -92,6 +92,7 @@ namespace dd {
     }
 
     void grobner::saturate() {
+        if (is_tuned()) tuned_init();
         try {
             while (!done() && step()) {
                 TRACE("grobner", display(tout););
@@ -105,6 +106,15 @@ namespace dd {
 
     bool grobner::step() {
         m_stats.m_compute_steps++;
+        if (is_tuned()) {
+            return tuned_step();
+        }
+        else {
+            return basic_step();
+        }
+    }
+
+    bool grobner::basic_step() {
         equation* e = pick_next();
         if (!e) return false;
         equation& eq = *e;
@@ -132,9 +142,18 @@ namespace dd {
     }
 
     void grobner::superpose(equation const & eq) {
-        for (equation * target : m_processed) {
+        unsigned j = 0;
-            superpose(eq, *target);
+        for (equation* target : m_processed) {
+            if (superpose(eq, *target)) {
+                // remove from watch lists
+                retire(target); 
+            }
+            else {
+                target->set_index(j);
+                m_processed[j++] = target;
+            }
         }
+        m_processed.shrink(j);
     }
 
     /*
@@ -172,18 +191,15 @@ namespace dd {
             equation& target = *set[i];
             bool changed_leading_term = false;
             bool simplified = !done() && simplify_source_target(eq, target, changed_leading_term); 
-            if (simplified && (is_trivial(target) || is_too_complex(target))) {
+            if (simplified && is_trivial(target)) {
                 retire(&target);
             }
-            else if (simplified && !check_conflict(target) && changed_leading_term && target.is_processed()) {
+            else if (simplified && !check_conflict(target) && changed_leading_term) {
-                target.set_index(m_to_simplify.size());
+                push_equation(target, m_to_simplify);               
-                target.set_processed(false);
-                m_to_simplify.push_back(&target);                    
             }
             else {
-                set[j] = ⌖
+                set[j] = set[i];
-                target.set_index(j);
+                target.set_index(j++);                
-                ++j;
             } 
         }
         set.shrink(j);
@@ -198,14 +214,32 @@ namespace dd {
     bool grobner::simplify_source_target(equation const& source, equation& target, bool& changed_leading_term) {
         TRACE("grobner", tout << "simplifying: " << target.poly() << "\nusing: " << source.poly() << "\n";);
         m_stats.m_simplified++;
-        pdd r = source.poly().reduce(target.poly());
+        pdd t = target.poly();
-        if (r == source.poly()) {
+        pdd r = source.poly().reduce(t);
+        if (r == source.poly() || is_too_complex(r)) {
             return false;
         }
         changed_leading_term = target.is_processed() && m.different_leading_term(r, source.poly());
         target = r;
         target = m_dep_manager.mk_join(target.dep(), source.dep());
         update_stats_max_degree_and_size(target);
+        if (changed_leading_term) {
+            target.set_processed(false);
+        }
+        if (is_tuned()) {
+            if (r == t) {
+                // noop
+            }
+            else if (changed_leading_term) {
+                add_to_watch(target);
+            }
+            else if (target.is_processed()) {
+                add_diff_to_watch(target, t);
+            }
+            else {
+                add_to_watch(target);
+            }            
+        }
 
         TRACE("grobner", tout << "simplified " << target.poly() << "\n";);
         return true;
@@ -214,14 +248,104 @@ namespace dd {
     /*
        let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0
     */
-    void grobner::superpose(equation const& eq1, equation const& eq2) {
+    bool grobner::superpose(equation const& eq1, equation const& eq2) {
         TRACE("grobner_d", tout << "eq1="; display_equation(tout, eq1) << "eq2="; display_equation(tout, eq2););
         pdd r(m);
-        if (!m.try_spoly(eq1.poly(), eq2.poly(), r)) return;
+        if (!m.try_spoly(eq1.poly(), eq2.poly(), r)) return false;
         m_stats.m_superposed++;
-        if (r.is_zero()) return;
+        if (r.is_zero() || is_too_complex(r)) return false;
-        if (is_too_complex(r)) return;
         add(r, m_dep_manager.mk_join(eq1.dep(), eq2.dep()));
+        return is_tuned() && m.spoly_is_invertible(eq1.poly(), eq2.poly());
+    }
+
+    bool grobner::tuned_step() {
+        equation* e = tuned_pick_next();
+        if (!e) return false;
+        equation& eq = *e;
+        SASSERT(!eq.is_processed());
+        if (!simplify_watch(eq, true)) return false;
+        if (eliminate(eq)) return true;
+        if (check_conflict(eq)) return false;
+        if (!simplify_using(m_processed, eq)) return false;
+        TRACE("grobner", tout << "eq = "; display_equation(tout, eq););
+        superpose(eq);
+        eq.set_processed(true);
+        m_processed.push_back(e);
+        add_diff_to_watch(eq, m.zero());
+        return simplify_watch(eq, false);
+    }
+
+    void grobner::tuned_init() {
+        // TBD: extract free variables, order them, set pointer into variable list.
+        NOT_IMPLEMENTED_YET();
+        m_watch.reserve(m_vars.size());
+        for (equation* eq : m_to_simplify) add_to_watch(*eq);
+        SASSERT(m_processed.empty());
+    }
+
+    // watch top variable
+    void grobner::add_to_watch(equation& eq) {
+        SASSERT(!eq.is_processed());
+        pdd const& p = eq.poly();
+        if (is_tuned() && !p.is_val()) {
+            m_watch[p.var()].push_back(&eq);
+        }
+    }
+
+    // add all variables in q but not p into watch.
+    void grobner::add_diff_to_watch(equation& eq, pdd const& p) {
+        SASSERT(eq.is_processed());
+        pdd const& q = eq.poly();
+        if (is_tuned() && !q.is_val()) {
+            for (unsigned v : m.free_vars_except(q, p)) {
+                m_watch[v].push_back(&eq);
+            }
+        }
+    }
+
+    bool grobner::simplify_watch(equation const& eq, bool is_processed) {
+        unsigned v = m_vars[m_var];
+        auto& watch = m_watch[v];
+        unsigned j = 0;
+        for (equation* _target : watch) {
+            equation& target = *_target;
+            bool changed_leading_term = false;
+            bool simplified = !done() && simplify_source_target(eq, target, changed_leading_term);
+            if (simplified && is_trivial(target)) {
+                retire(&target);
+            }
+            else if (simplified && !check_conflict(target) && changed_leading_term) {
+                SASSERT(!target.is_processed());
+                pop_equation(target.idx(), m_processed);
+                push_equation(target, m_to_simplify);
+            }
+            else {
+                watch[++j] = _target;
+            }
+        }
+        watch.shrink(j);        
+        return false;
+    }
+
+    grobner::equation* grobner::tuned_pick_next() {
+        while (m_var < m_vars.size()) {
+            unsigned v = m_vars[m_var];
+            equation_vector const& watch = m_watch[v];
+            equation* eq = nullptr;
+            for (equation* curr : watch) {
+                pdd const& p = curr->poly();
+                if (!curr->is_processed() && !p.is_val() && p.var() == v) {
+                    if (!eq || is_simpler(*curr, *eq))
+                        eq = curr;
+                }
+            }
+            if (eq) {
+                pop_equation(eq->idx(), m_to_simplify);
+                return eq;
+            }
+            ++m_var;
+        }
+        return nullptr;
     }
 
     grobner::equation_vector const& grobner::equations() {
@@ -262,11 +386,18 @@ namespace dd {
     }
 
     void grobner::pop_equation(unsigned idx, equation_vector& v) {
-        equation* eq2 = v.back();
+        if (idx != v.size() - 1) {
-        eq2->set_index(idx);
+            equation* eq2 = v.back();
-        v[idx] = eq2;
+            eq2->set_index(idx);
+            v[idx] = eq2;
+        }
         v.pop_back();            
     }
+
+    void grobner::push_equation(equation& eq, equation_vector& v) {
+        eq.set_index(v.size());
+        v.push_back(&eq);
+    }
     
     void grobner::update_stats_max_degree_and_size(const equation& e) {
         m_stats.m_max_expr_size = std::max(m_stats.m_max_expr_size, e.poly().tree_size());

src/math/grobner/pdd_grobner.h

@@ -42,6 +42,12 @@ public:
     struct config {
         unsigned m_eqs_threshold;
         unsigned m_expr_size_limit;
+        enum { basic, tuned } m_algorithm;
+        config() :
+            m_eqs_threshold(UINT_MAX),
+            m_expr_size_limit(UINT_MAX),
+            m_algorithm(basic)
+        {}
     };
 
 private:
@@ -80,7 +86,7 @@ private:
     equation_vector                              m_to_simplify;
     mutable u_dependency_manager                 m_dep_manager;
     equation_vector                              m_all_eqs;
-    equation const*                              m_conflict;
+    equation const*                              m_conflict;   
 public:
     grobner(reslimit& lim, pdd_manager& m);
     ~grobner();
@@ -102,10 +108,11 @@ public:
 
 private:
     bool step();
+    bool basic_step();
     equation* pick_next();
     bool canceled();
     bool done();
-    void superpose(equation const& eq1, equation const& eq2);
+    bool superpose(equation const& eq1, equation const& eq2);
     void superpose(equation const& eq);
     bool simplify_source_target(equation const& source, equation& target, bool& changed_leading_term);
     bool simplify_using(equation_vector& set, equation const& eq);
@@ -119,13 +126,33 @@ private:
     bool is_too_complex(const equation& eq) const { return is_too_complex(eq.poly()); }
     bool is_too_complex(const pdd& p) const { return p.tree_size() > m_config.m_expr_size_limit;  }
 
+
+    // tuned implementation
+    vector<equation_vector> m_watch;           // watch list mapping variables to vector of equations where they occur (generally a subset)
+    unsigned                m_var;             // index into vars with current variable
+    unsigned_vector         m_vars;            // variables sorted by priority, higher priority first.
+
+    bool tuned_step();
+    void tuned_init();
+    equation* tuned_pick_next();
+    bool simplify_watch(equation const& eq, bool is_processed);
+    void add_to_watch(equation& eq);
+    void add_diff_to_watch(equation& eq, pdd const& p);
+
     void del_equation(equation& eq);    
-    void retire(equation* eq) { dealloc(eq); }
+    void retire(equation* eq) {
+        if (is_tuned())
+            for (auto v : m.free_vars(eq->poly())) m_watch[v].erase(eq);
+        dealloc(eq);
+    }
     void pop_equation(unsigned idx, equation_vector& v);
+    void push_equation(equation& eq, equation_vector& v);
 
     void invariant() const;
 
     void update_stats_max_degree_and_size(const equation& e);
+    bool is_tuned() const { return m_config.m_algorithm == config::tuned;  }
+    bool is_basic() const { return m_config.m_algorithm == config::basic; }
 };
 
 }