misc fixes to grobner state (#109)

* fixes to use list bookkeeping

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

* fix reset logic

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

* fix non-termination bug in simplifier

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

* missing reset of values

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

* add configuration to throttle memory usage

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

* fix misc. invariant violations

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

* multiple linear constraints seem to be violated

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

src/math/grobner/pdd_grobner.cpp

@@ -127,7 +127,7 @@ namespace dd {
 
     void grobner::saturate() {
         simplify();
-        if (is_tuned()) tuned_init();
+        tuned_init();
         TRACE("grobner", display(tout););
         try {
             while (!done() && step()) {
@@ -138,46 +138,37 @@ namespace dd {
             DEBUG_CODE(invariant(););
         }
         catch (pdd_manager::mem_out) {
-            IF_VERBOSE(1, verbose_stream() << "mem-out\n");
+            m_watch.reset();
+            IF_VERBOSE(2, verbose_stream() << "mem-out\n");
             // don't reduce further
         }
     }
 
     bool grobner::step() {
         m_stats.m_compute_steps++;
-        return is_tuned() ? tuned_step() : basic_step();
+        return tuned_step();
     }
 
-    bool grobner::basic_step() {
+    void grobner::scoped_process::done() {
-        return basic_step(pick_next());
+        pdd p = e->poly();
+        SASSERT(!p.is_val());
+        if (p.hi().is_val()) {
+            g.push_equation(solved, e);
+        }
+        else {
+            g.push_equation(processed, e);
+        }
+        e = nullptr;
     }
 
     grobner::scoped_process::~scoped_process() {
         if (e) {
             pdd p = e->poly();
             SASSERT(!p.is_val());
-            if (p.hi().is_val()) {
+            g.push_equation(processed, e);            
-                g.push_equation(solved, e);
-            }
-            else {
-                g.push_equation(processed, e);
-            }
         }
     }
 
-    bool grobner::basic_step(equation* e) {
-        if (!e) return false;
-        scoped_process sd(*this, e);
-        equation& eq = *e;
-        TRACE("grobner", display(tout << "eq = ", eq); display(tout););
-        SASSERT(eq.state() == to_simplify);
-        if (!simplify_using(eq, m_processed)) return false;
-        if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; }
-        if (check_conflict(eq)) { sd.e = nullptr; return false; }
-        if (!simplify_using(m_processed, eq)) return false;
-        superpose(eq);
-        return simplify_using(m_to_simplify, eq);
-    }
     
     grobner::equation* grobner::pick_next() {
         equation* eq = nullptr;
@@ -206,6 +197,7 @@ namespace dd {
         }
         catch (pdd_manager::mem_out) {
             // done reduce
+            DEBUG_CODE(invariant(););
         }
     }
 
@@ -217,6 +209,7 @@ namespace dd {
 
     bool grobner::simplify_linear_step(bool binary) {
         TRACE("grobner", tout << "binary " << binary << "\n";);
+        IF_VERBOSE(2, verbose_stream() << "binary " << binary << "\n");
         equation_vector linear;
         for (equation* e : m_to_simplify) {
             pdd p = e->poly();
@@ -241,7 +234,11 @@ namespace dd {
         std::stable_sort(linear.begin(), linear.end(), ctv);
         equation_vector trivial;
         unsigned j = 0;
+        bool has_conflict = false;
         for (equation* src : linear) {
+            if (has_conflict) {
+                break;
+            }
             unsigned v = src->poly().var();
             equation_vector const& uses = use_list[v];
             TRACE("grobner", 
@@ -268,7 +265,7 @@ namespace dd {
                 else if (is_conflict(dst)) {
                     pop_equation(dst);
                     set_conflict(dst);
-                    return true;
+                    has_conflict = true;
                 }
                 else if (changed_leading_term) {
                     pop_equation(dst);
@@ -282,16 +279,18 @@ namespace dd {
                 linear[j++] = src;              
             }
         }
-        linear.shrink(j);      
+        if (!has_conflict) {
-        for (equation* src : linear) {
+            linear.shrink(j);      
-            pop_equation(src);
+            for (equation* src : linear) {
-            push_equation(solved, src);
+                pop_equation(src);
+                push_equation(solved, src);
+            }
         }
         for (equation* e : trivial) {
             del_equation(e);
         }
         DEBUG_CODE(invariant(););
-        return j > 0;
+        return j > 0 || has_conflict;
     }
 
     /**
@@ -302,6 +301,7 @@ namespace dd {
      */
     bool grobner::simplify_cc_step() {
         TRACE("grobner", tout << "cc\n";);
+        IF_VERBOSE(2, verbose_stream() << "cc\n");
         u_map<equation*> los;
         bool reduced = false;
         unsigned j = 0;
@@ -335,6 +335,7 @@ namespace dd {
     */
     bool grobner::simplify_leaf_step() {
         TRACE("grobner", tout << "leaf\n";);
+        IF_VERBOSE(2, verbose_stream() << "leaf\n");
         use_list_t use_list = get_use_list();
         equation_vector leaves;
         for (unsigned i = 0; i < m_to_simplify.size(); ++i) {
@@ -377,6 +378,7 @@ namespace dd {
     */
     bool grobner::simplify_elim_pure_step() {
         TRACE("grobner", tout << "pure\n";);
+        IF_VERBOSE(2, verbose_stream() << "pure\n");
         use_list_t use_list = get_use_list();        
         unsigned j = 0;
         for (equation* e : m_to_simplify) {
@@ -507,7 +509,7 @@ namespace dd {
     /*
       Use a set of equations to simplify eq
     */
-    bool grobner::simplify_using(equation& eq, equation_vector const& eqs) {
+    void grobner::simplify_using(equation& eq, equation_vector const& eqs) {
         bool simplified, changed_leading_term;
         do {
             simplified = false;
@@ -523,19 +525,36 @@ namespace dd {
         while (simplified && !eq.poly().is_val());
 
         TRACE("grobner", display(tout << "simplification result: ", eq););
-
-        return !done();
     }
 
     /*
       Use the given equation to simplify equations in set
     */
-    bool grobner::simplify_using(equation_vector& set, equation const& eq) {
+    void grobner::simplify_using(equation_vector& set, equation const& eq) {
-        unsigned j = 0, sz = set.size();
+        
-        for (unsigned i = 0; i < sz; ++i) {
+        struct scoped_update {
-            equation& target = *set[i];
+            equation_vector& set;
+            unsigned i, j, sz;
+            scoped_update(equation_vector& set): set(set), i(0), j(0), sz(set.size()) {}
+            void nextj() {
+                set[j] = set[i];
+                set[i]->set_index(j++);
+            }
+            ~scoped_update() {                
+                for (; i < sz; ++i) {
+                    nextj();
+                }
+                set.shrink(j);
+            }
+        };
+
+        scoped_update sr(set);
+        for (; sr.i < sr.sz; ++sr.i) {
+            equation& target = *set[sr.i];
             bool changed_leading_term = false;
-            bool simplified = !done() && try_simplify_using(target, eq, changed_leading_term); 
+            bool simplified = true;
+            simplified = !done() && try_simplify_using(target, eq, changed_leading_term); 
+            
             if (simplified && is_trivial(target)) {
                 retire(&target);
             }
@@ -551,12 +570,9 @@ namespace dd {
                 }
             }
             else {
-                set[j] = set[i];
+                sr.nextj();
-                target.set_index(j++);                
             } 
         }
-        set.shrink(j);
-        return !done();
     }    
 
     /*
@@ -571,7 +587,11 @@ namespace dd {
         m_stats.m_simplified++;
         pdd t = src.poly();
         pdd r = dst.poly().reduce(t);
-        if (r == dst.poly() || is_too_complex(r)) {
+        if (r == dst.poly()){
+            return false;
+        }
+        if (is_too_complex(r)) {
+            m_too_complex = true;
             return false;
         }
         TRACE("grobner", 
@@ -608,10 +628,14 @@ namespace dd {
     void grobner::superpose(equation const& eq1, equation const& eq2) {
         TRACE("grobner_d", display(tout << "eq1=", eq1); display(tout << "eq2=", eq2););
         pdd r(m);
-        if (m.try_spoly(eq1.poly(), eq2.poly(), r) && 
+        if (m.try_spoly(eq1.poly(), eq2.poly(), r) && !r.is_zero()) {
-            !r.is_zero() && !is_too_complex(r)) {
+            if (is_too_complex(r)) {
-            m_stats.m_superposed++;
+                m_too_complex = true;
-            add(r, m_dep_manager.mk_join(eq1.dep(), eq2.dep()));
+            }
+            else {
+                m_stats.m_superposed++;
+                add(r, m_dep_manager.mk_join(eq1.dep(), eq2.dep()));
+            }
         }
     }
 
@@ -622,13 +646,17 @@ namespace dd {
         equation& eq = *e;
         SASSERT(!m_watch[eq.poly().var()].contains(e));
         SASSERT(eq.state() == to_simplify);
-        if (!simplify_using(eq, m_processed)) return false;
+        simplify_using(eq, m_processed);
         if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; }
         if (check_conflict(eq)) { sd.e = nullptr; return false; }
-        if (!simplify_using(m_processed, eq)) return false;
+        m_too_complex = false;
+        simplify_using(m_processed, eq);
+        if (done()) return false;
         TRACE("grobner", display(tout << "eq = ", eq););
         superpose(eq);
         simplify_watch(eq);
+        if (done()) return false;
+        if (!m_too_complex) sd.done();
         return true;
     }
 
@@ -648,7 +676,6 @@ namespace dd {
 
     void grobner::add_to_watch(equation& eq) {
         SASSERT(eq.state() == to_simplify);
-        SASSERT(is_tuned());
         pdd const& p = eq.poly();
         if (!p.is_val()) {
             m_watch[p.var()].push_back(&eq);
@@ -785,6 +812,8 @@ namespace dd {
     }
 
     void grobner::push_equation(eq_state st, equation& eq) {
+        SASSERT(st != to_simplify || !eq.poly().is_val());
+        SASSERT(st != processed || !eq.poly().is_val());
         eq.set_state(st);
         equation_vector& v = get_queue(eq);
         eq.set_index(v.size());

src/math/lp/int_set.h

@@ -19,7 +19,6 @@ Revision History:
 --*/
 #pragma once
 #include "util/vector.h"
-#include "math/lp/indexed_vector.h"
 #include <ostream>
 namespace lp {
 // serves at a set of non-negative integers smaller than the set size

src/math/lp/nla_core.cpp

@@ -22,6 +22,7 @@ Revision History:
 #include "math/lp/nex.h"
 #include "math/grobner/pdd_grobner.h"
 #include "math/dd/pdd_interval.h"
+#include "math/dd/pdd_eval.h"
 namespace nla {
 
 core::core(lp::lar_solver& s, reslimit & lim) :
@@ -1419,7 +1420,18 @@ void core::run_pdd_grobner() {
     for (unsigned i : m_rows) {
         add_row_to_pdd_grobner(m_lar_solver.A_r().m_rows[i]);
     }
-
+#if 0
+    IF_VERBOSE(2, m_pdd_grobner.display(verbose_stream()));
+    dd::pdd_eval eval(m_pdd_manager);
+    eval.var2val() = [&](unsigned j){ return val(j); };
+    for (auto* e : m_pdd_grobner.equations()) {
+        dd::pdd p = e->poly();
+        rational v = eval(p);
+        if (p.is_linear() && !eval(p).is_zero()) {
+            IF_VERBOSE(0, verbose_stream() << "violated linear constraint " << p << "\n");
+        }
+    }
+#endif
    
     // configure grobner
     // TBD: move this code somewhere self-contained, and tune it.
@@ -1449,9 +1461,36 @@ void core::run_pdd_grobner() {
     }
     else {
         IF_VERBOSE(2, verbose_stream() << "grobner miss\n");
+        IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream()));
     }
 }
 
+std::ostream& core::diagnose_pdd_miss(std::ostream& out) {
+
+    // m_pdd_grobner.display(out);
+
+    dd::pdd_eval eval(m_pdd_manager);
+    eval.var2val() = [&](unsigned j){ return val(j); };
+    for (auto* e : m_pdd_grobner.equations()) {
+        dd::pdd p = e->poly();
+        rational v = eval(p);
+        if (!v.is_zero()) {
+            out << p << " := " << v << "\n";
+        }
+    }  
+  
+    for (unsigned j = 0; j < m_lar_solver.column_count(); ++j) {
+        if (m_lar_solver.column_has_lower_bound(j) || m_lar_solver.column_has_upper_bound(j)) {
+            out << j << ": [";
+                if (m_lar_solver.column_has_lower_bound(j)) out << m_lar_solver.get_lower_bound(j);
+                out << "..";
+                if (m_lar_solver.column_has_upper_bound(j)) out << m_lar_solver.get_upper_bound(j);
+                out << "]\n";
+        }
+    }              
+    return out;
+}
+
 bool core::check_pdd_eq(const dd::grobner::equation* e) {
     dd::pdd_interval eval(m_pdd_manager, m_reslim);
     eval.var2interval() =
@@ -1620,15 +1659,27 @@ void core::set_active_vars_weights(nex_creator& nc) {
 
 void core::set_level2var_for_pdd_grobner() {
     unsigned n = m_lar_solver.column_count();
-    unsigned_vector sorted_vars(n);
+    unsigned_vector sorted_vars(n), weighted_vars(n);
-    for (unsigned j = 0; j < n; j++)
+    for (unsigned j = 0; j < n; j++) {
         sorted_vars[j] = j;
-    // sort that the larger weights are in beginning
+        weighted_vars[j] = get_var_weight(j);
-    std::sort(sorted_vars.begin(), sorted_vars.end(), [this](unsigned a, unsigned b) {
+    }
-                                                      unsigned wa = get_var_weight(a);
+#if 1
-                                                      unsigned wb = get_var_weight(b);
+    // potential update to weights
+    for (unsigned j = 0; j < n; j++) {
+        if (is_monic_var(j) && m_to_refine.contains(j)) {
+            for (lpvar k : m_emons[j].vars()) {
+                weighted_vars[k] += 6;
+            }
+        }
+    }
+#endif
+
+    std::sort(sorted_vars.begin(), sorted_vars.end(), [&](unsigned a, unsigned b) {
+                                                      unsigned wa = weighted_vars[a];
+                                                      unsigned wb = weighted_vars[b];
                                                       return wa < wb || (wa == wb && a < b); });
-    
+
     unsigned_vector l2v(n);
     for (unsigned j = 0; j < n; j++)
         l2v[j] = sorted_vars[j];
@@ -1658,8 +1709,9 @@ unsigned core::get_var_weight(lpvar j) const {
     }
     if (is_monic_var(j)) {
         k++;
-        if (m_to_refine.contains(j))
+        if (m_to_refine.contains(j)) {
             k++;
+        }
     }
     return k;
 }

src/math/lp/nla_core.h

@@ -220,6 +220,7 @@ public:
     std::ostream& print_product_with_vars(const T& m, std::ostream& out) const;
     std::ostream& print_monic_with_vars(const monic& m, std::ostream& out) const;
     std::ostream& print_explanation(const lp::explanation& exp, std::ostream& out) const;
+    std::ostream& diagnose_pdd_miss(std::ostream& out);
     template <typename T>
     void trace_print_rms(const T& p, std::ostream& out);
     void trace_print_monic_and_factorization(const monic& rm, const factorization& f, std::ostream& out) const;