reduce simplification

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

src/math/dd/dd_pdd.cpp

@@ -70,7 +70,7 @@ namespace dd {
     pdd pdd_manager::zero() { return pdd(zero_pdd, this); }
     pdd pdd_manager::one() { return pdd(one_pdd, this); }
     
-    pdd pdd_manager::mk_or(pdd const& p, pdd const& q) { return p*q + p + q; }
+    pdd pdd_manager::mk_or(pdd const& p, pdd const& q) { return p + q - (p*q); }
 
     pdd_manager::PDD pdd_manager::apply(PDD arg1, PDD arg2, pdd_op op) {
         bool first = true;
@@ -448,6 +448,19 @@ namespace dd {
         return is_linear(p.root); 
     }
 
+    /*
+      Determine whether p is a binary polynomials 
+      of the form v1, x*v1 + v2, or x*v1 + y*v2 + v3
+      where v1, v2 are values.      
+     */
+    bool pdd_manager::is_binary(PDD p) {
+        return is_val(p) || (is_val(hi(p)) && (is_val(lo(p)) || (is_val(hi(lo(p))) && is_val(lo(lo(p))))));
+    }
+
+    bool pdd_manager::is_binary(pdd const& p) { 
+        return is_binary(p.root); 
+    }
+
     void pdd_manager::push(PDD b) {
         m_pdd_stack.push_back(b);
     }

src/math/dd/dd_pdd.h

@@ -252,6 +252,9 @@ namespace dd {
         bool is_linear(PDD p);
         bool is_linear(pdd const& p);
 
+        bool is_binary(PDD p);
+        bool is_binary(pdd const& p);
+
         // create an spoly r if leading monomials of a and b overlap
         bool try_spoly(pdd const& a, pdd const& b, pdd& r);
 
@@ -287,7 +290,10 @@ namespace dd {
         bool is_val() const { return m.is_val(root); }
         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); }
 
+        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); }
@@ -315,7 +321,10 @@ 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, pdd const& b) { return r + (-b); }
+    inline pdd operator-(int x, pdd const& b) { return rational(x) - b; }
     inline pdd operator-(pdd const& b, int x) { return b + (-rational(x)); }
+
     inline pdd& operator*=(pdd & p, pdd const& q) { p = p * q; return p; }
     inline pdd& operator|=(pdd & p, pdd const& q) { p = p | q; return p; }
     inline pdd& operator-=(pdd & p, pdd const& q) { p = p - q; return p; }

src/math/grobner/pdd_grobner.cpp

@@ -184,20 +184,14 @@ namespace dd {
         return eq;
     }
 
-    grobner::equation* grobner::pick_linear() {
-        equation* eq = nullptr;
-        for (auto* curr : m_to_simplify) {
-            if (!eq || (curr->poly().is_linear() && is_simpler(*curr, *eq))) {
-                eq = curr;
-            }
-        }
-        if (eq) pop_equation(eq);
-        return eq;
-    }
-
     void grobner::simplify() {
         try {
-            while (simplify_linear_step(true) || simplify_linear_step(false) /*|| simplify_cc_step() */ || simplify_elim_step()) {
+            while (simplify_linear_step(true) || 
+                   simplify_elim_pure_step() ||
+                   simplify_linear_step(false) || 
+                   simplify_cc_step() ||  
+                   /*simplify_elim_dual_step() ||*/
+                false) {
                 DEBUG_CODE(invariant(););
                 TRACE("grobner", display(tout););
             }
@@ -217,41 +211,62 @@ namespace dd {
         equation_vector linear;
         for (equation* e : m_to_simplify) {
             pdd p = e->poly();
-            if (p.is_linear()) {
+            if (p.is_linear() && (!binary || p.is_binary())) {
-                if (!binary || p.lo().is_val() || p.lo().lo().is_val()) {
+                linear.push_back(e);
-                    linear.push_back(e);
-                }
             }
         }
+        return simplify_linear_step(linear);
+    }
+
+    /**
+       \brief simplify linear equations by using top variable as solution.
+       The linear equation is moved to set of solved equations.
+    */
+    bool grobner::simplify_linear_step(equation_vector& linear) {
         if (linear.empty()) return false;
         use_list_t use_list = get_use_list();
         compare_top_var ctv;
         std::stable_sort(linear.begin(), linear.end(), ctv);
+        equation_vector trivial;
+        unsigned j = 0;
         for (equation* src : linear) {
             equation_vector const& uses = use_list[src->poly().var()];
             bool changed_leading_term;
+            bool all_reduced = true;
             for (equation* dst : uses) {
-                if (src == dst) {
+                if (src == dst || is_trivial(*dst)) {
                     continue;                    
                 }
+                if (!src->poly().is_binary() && !dst->poly().is_linear()) {
+                    all_reduced = false;
+                    continue;
+                }
                 simplify_using(*dst, *src, changed_leading_term);
                 if (check_conflict(*dst)) {
                     return false;
                 }
                 if (is_trivial(*dst)) {
-                    SASSERT(false);
+                    trivial.push_back(dst);
                 }
-                if (changed_leading_term) {
+                else if (changed_leading_term) {
                     pop_equation(dst);
                     push_equation(to_simplify, dst);
                 }
-            }            
+            }          
+            if (all_reduced) {
+                linear[j++] = src;              
+            }
         } 
+        linear.shrink(j);      
         for (equation* src : linear) {
             pop_equation(src);
             push_equation(solved, src);
         }
-        return true;
+        for (equation* e : trivial) {
+            del_equation(e);
+        }
+        DEBUG_CODE(invariant(););
+        return j > 0;
     }
 
     /**
@@ -269,7 +284,8 @@ namespace dd {
             pdd p = eq1->poly();
             auto* e = los.insert_if_not_there2(p.lo().index(), eq1);
             equation* eq2 = e->get_data().m_value;
-            if (eq2 != eq1 && p.hi().is_val() && !p.lo().is_val()) {
+            pdd q = eq2->poly();
+            if (eq2 != eq1 && (p.hi().is_val() || q.hi().is_val()) && !p.lo().is_val()) {
                 *eq1 = p - eq2->poly();
                 *eq1 = m_dep_manager.mk_join(eq1->dep(), eq2->dep());
                 reduced = true;
@@ -290,9 +306,8 @@ namespace dd {
 
     /**
        \brief treat equations as processed if top variable occurs only once.
-       reduce equations where top variable occurs only twice and linear in one of the occurrences.       
+    */
-     */
+    bool grobner::simplify_elim_pure_step() {
-    bool grobner::simplify_elim_step() {
         use_list_t use_list = get_use_list();        
         unsigned j = 0;
         for (equation* e : m_to_simplify) {
@@ -309,7 +324,16 @@ namespace dd {
             m_to_simplify.shrink(j);
             return true;
         }
-        j = 0;
+        return false;
+    }
+
+    /**
+       \brief 
+       reduce equations where top variable occurs only twice and linear in one of the occurrences.       
+     */
+    bool grobner::simplify_elim_dual_step() {
+        use_list_t use_list = get_use_list();        
+        unsigned j = 0;
         for (unsigned i = 0; i < m_to_simplify.size(); ++i) {
             equation* e = m_to_simplify[i];            
             pdd p = e->poly();
@@ -653,9 +677,9 @@ namespace dd {
         return m_to_simplify;
     }
 
-    void grobner::del_equation(equation& eq) {
+    void grobner::del_equation(equation* eq) {
         pop_equation(eq);
-        retire(&eq);
+        retire(eq);
     }
 
     void grobner::pop_equation(equation& eq) {

src/math/grobner/pdd_grobner.h

@@ -121,7 +121,6 @@ private:
     bool basic_step();
     bool basic_step(equation* e);
     equation* pick_next();
-    equation* pick_linear();
     bool canceled();
     bool done();
     void superpose(equation const& eq1, equation const& eq2);
@@ -151,7 +150,8 @@ private:
     bool simplify_to_simplify(equation const& eq);
     void add_to_watch(equation& eq);
 
-    void del_equation(equation& eq);    
+    void del_equation(equation& eq) { del_equation(&eq); }    
+    void del_equation(equation* eq);    
     equation_vector& get_queue(equation const& eq);
     void retire(equation* eq) { dealloc(eq); }
     void pop_equation(equation& eq);
@@ -161,13 +161,15 @@ private:
 
     struct compare_top_var;
     bool simplify_linear_step(bool binary);
+    bool simplify_linear_step(equation_vector& linear);
     typedef vector<equation_vector> use_list_t;
     use_list_t get_use_list();
     void add_to_use(equation* e, use_list_t& use_list);
     void remove_from_use(equation* e, use_list_t& use_list);
 
     bool simplify_cc_step();
-    bool simplify_elim_step();
+    bool simplify_elim_pure_step();
+    bool simplify_elim_dual_step();
 
     void invariant() const;
     struct scoped_process {

src/test/pdd_grobner.cpp

@@ -81,21 +81,26 @@ namespace dd {
         if (m.is_and(e)) {
             pdd r = p.one();
             for (expr* arg : *e) r *= p.mk_var(id2var[arg->get_id()]);
-            q = v1 + r;
+            q = v1 - r;
         }
         else if (m.is_or(e)) {
             pdd r = p.zero();
             for (expr* arg : *e) r |= p.mk_var(id2var[arg->get_id()]);
-            q = v1 + r;
+            q = v1 - r;
         }
         else if (m.is_not(e, a)) {
             pdd v2 = p.mk_var(id2var[a->get_id()]);
-            q = v1 + v2 + 1;
+            q = v1 + v2 - 1;
         }
         else if (m.is_eq(e, a, b)) {
             pdd v2 = p.mk_var(id2var[a->get_id()]);
             pdd v3 = p.mk_var(id2var[b->get_id()]);
-            q = v1 + v2 + v3 + 1;
+            // v1 = (v2 = v3)
+            // 111, 100 = 0
+            // 001, 010 = 0
+            // 000, 011 = 1
+            // 110, 101 = 1
+            q = v1 - v2 - v3 + 1 + 2*v2*v3 - 2*v1*v2*v3;
         }
         else if (is_uninterp_const(e)) {
             return;
@@ -121,34 +126,34 @@ namespace dd {
         }
     }
 
-    void test_simplify(expr_ref_vector& fmls) {
+    void test_simplify(expr_ref_vector& fmls, bool use_mod2) {
         ast_manager& m = fmls.get_manager();
         unsigned_vector id2var;
 
         collect_id2var(id2var, fmls);
         pdd_manager p(id2var.size());
-        p.set_mod2_semantics();
+        if (use_mod2) p.set_mod2_semantics();
         grobner g(m.limit(), p);
 
         for (expr* e : subterms(fmls)) {
             add_def(id2var, to_app(e), m, p, g);
         }
         for (expr* e : fmls) {
-            g.add(p.mk_var(id2var[e->get_id()]) + 1);
+            g.add(1 - p.mk_var(id2var[e->get_id()]));
         }
         g.display(std::cout);
         g.simplify();
         g.display(std::cout);
-        g.saturate();
+        //g.saturate();
-        g.display(std::cout);
+        //g.display(std::cout);
     }
 
     void test2() {
         ast_manager m;
         reg_decl_plugins(m);
         bv_util bv(m);
-        expr_ref x(m.mk_const("x", bv.mk_sort(3)), m);
+        expr_ref x(m.mk_const("x", bv.mk_sort(4)), m);
-        expr_ref y(m.mk_const("y", bv.mk_sort(3)), m);
+        expr_ref y(m.mk_const("y", bv.mk_sort(4)), m);
         expr_ref xy(bv.mk_bv_mul(x, y), m);
         expr_ref yx(bv.mk_bv_mul(y, x), m);
         expr_ref eq(m.mk_not(m.mk_eq(xy,yx)), m);
@@ -163,7 +168,8 @@ namespace dd {
         for (unsigned i = 0; i < g->size(); ++i) {
             fmls.push_back(g->form(i));        
         }
-        test_simplify(fmls);
+        test_simplify(fmls, true);
+        test_simplify(fmls, false);
         
     }
 }