resolve

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

src/math/dd/dd_pdd.cpp

@@ -461,6 +461,30 @@ namespace dd {
         return is_binary(p.root); 
     }
 
+    /*
+      \brief determine if v occurs as a leaf variable.
+     */
+    bool pdd_manager::var_is_leaf(PDD p, unsigned v) {
+        init_mark();
+        m_todo.push_back(p);
+        while (!m_todo.empty()) {
+            PDD r = m_todo.back();
+            m_todo.pop_back();
+            if (is_val(r) || is_marked(r)) continue;
+            set_mark(r);
+            if (var(r) == v) {
+                if (!is_val(lo(r)) || !is_val(hi(r))) {
+                    m_todo.reset();
+                    return false;
+                }
+                continue;
+            }
+            if (!is_marked(lo(r))) m_todo.push_back(lo(r));
+            if (!is_marked(hi(r))) m_todo.push_back(hi(r));
+        }
+        return true;
+    }
+
     void pdd_manager::push(PDD b) {
         m_pdd_stack.push_back(b);
     }

src/math/dd/dd_pdd.h

@@ -203,6 +203,8 @@ namespace dd {
         unsigned dag_size(pdd const& p);
         unsigned degree(pdd const& p);
 
+        bool var_is_leaf(PDD p, unsigned v);
+
         bool is_reachable(PDD p);
         void compute_reachable(svector<bool>& reachable);
         void try_gc();
@@ -291,9 +293,9 @@ namespace dd {
         bool is_zero() const { return m.is_zero(root); }
         bool is_linear() const { return m.is_linear(root); }
         bool is_binary() const { return m.is_binary(root); }
+        bool var_is_leaf(unsigned v) const { return m.var_is_leaf(root, v); }
 
         pdd minus() const { return m.minus(*this); }
-        pdd operator-() const { return m.minus(*this); }
         pdd operator+(pdd const& other) const { return m.add(*this, other); }
         pdd operator-(pdd const& other) const { return m.sub(*this, other); }
         pdd operator*(pdd const& other) const { return m.mul(*this, other); }
@@ -317,11 +319,11 @@ namespace dd {
     inline pdd operator*(int x, pdd const& b) { return b * rational(x); }
     inline pdd operator*(pdd const& b, int x) { return b * rational(x); }
 
-    inline pdd operator+(rational const& r, const pdd& b) { return b + r; }
+    inline pdd operator+(rational const& r, pdd const& b) { return b + r; }
     inline pdd operator+(int x, pdd const& b) { return b + rational(x); }
     inline pdd operator+(pdd const& b, int x) { return b + rational(x); }
 
-    inline pdd operator-(rational const& r, pdd const& b) { return r + (-b); }
+    inline pdd operator-(rational const& r, pdd const& b) { return r + b.minus(); }
     inline pdd operator-(int x, pdd const& b) { return rational(x) - b; }
     inline pdd operator-(pdd const& b, int x) { return b + (-rational(x)); }
 

src/math/grobner/pdd_grobner.cpp

@@ -190,6 +190,7 @@ namespace dd {
                    simplify_elim_pure_step() ||
                    simplify_linear_step(false) || 
                    simplify_cc_step() || 
+                   simplify_leaf_step() ||
                    /*simplify_elim_dual_step() ||*/
                 false) {
                 DEBUG_CODE(invariant(););
@@ -304,6 +305,43 @@ namespace dd {
         return reduced;
     }
 
+    /**
+       \brief remove ax+b from p if x occurs as a leaf in p and a is a constant.
+    */
+    bool grobner::simplify_leaf_step() {
+        use_list_t use_list = get_use_list();
+        bool reduced = false;
+        equation_vector leaves;
+        for (unsigned i = 0; i < m_to_simplify.size(); ++i) {
+            equation* e = m_to_simplify[i];
+            pdd p = e->poly();
+            if (!p.hi().is_val()) {
+                continue;
+            }
+            leaves.reset();
+            for (equation* e2 : use_list[p.var()]) {
+                if (e != e2 && e2->poly().var_is_leaf(p.var())) {
+                    leaves.push_back(e2);
+                }
+            }
+            for (equation* e2 : leaves) {
+                bool changed_leading_term;
+                remove_from_use(e2, use_list);
+                simplify_using(*e2, *e, changed_leading_term);
+                add_to_use(e2, use_list);
+                if (check_conflict(*e2)) {
+                    return false;
+                }
+                else if (changed_leading_term) {
+                    pop_equation(e2);
+                    push_equation(to_simplify, e2);
+                }
+                reduced = true;
+            }
+        }
+        return reduced;
+    }
+
     /**
        \brief treat equations as processed if top variable occurs only once.
     */
@@ -334,12 +372,13 @@ namespace dd {
     bool grobner::simplify_elim_dual_step() {
         use_list_t use_list = get_use_list();        
         unsigned j = 0;
+        bool reduced = false;
         for (unsigned i = 0; i < m_to_simplify.size(); ++i) {
             equation* e = m_to_simplify[i];            
             pdd p = e->poly();
             // check that e is linear in top variable.
             if (e->state() != to_simplify) {
-                // this was moved before this pass
+                reduced = true;
             }
             else if (!done() && !is_trivial(*e) && p.hi().is_val() && use_list[p.var()].size() == 2) {
                 for (equation* e2 : use_list[p.var()]) {
@@ -351,9 +390,8 @@ namespace dd {
                     if (check_conflict(*e2)) { 
                         break;
                     }
-                    if (is_trivial(*e2)) {
+                    // when e2 is trivial, leading term is changed
-                        break;
+                    SASSERT(!is_trivial(*e2) || changed_leading_term);
-                    }
                     if (changed_leading_term) {
                         pop_equation(e2);
                         push_equation(to_simplify, e2);
@@ -361,6 +399,7 @@ namespace dd {
                     add_to_use(e2, use_list);
                     break;
                 }
+                reduced = true;
                 push_equation(solved, e);
             }
             else {
@@ -368,7 +407,7 @@ namespace dd {
                 e->set_index(j++);
             }
         }
-        if (j != m_to_simplify.size()) {
+        if (reduced) {
             // clean up elements in m_to_simplify 
             // they may have moved.
             m_to_simplify.shrink(j);

src/math/grobner/pdd_grobner.h

@@ -170,6 +170,7 @@ private:
     bool simplify_cc_step();
     bool simplify_elim_pure_step();
     bool simplify_elim_dual_step();
+    bool simplify_leaf_step();
 
     void invariant() const;
     struct scoped_process {