memory throttling (#108)

* 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>

src/math/dd/dd_pdd.cpp

@@ -51,6 +51,7 @@ namespace dd {
         m_free_nodes.reset();
         m_pdd_stack.reset();
         m_values.reset();
+        m_free_values.reset();
         m_mpq_table.reset();        
         m_values.reset();
         m_free_values.reset();

src/math/grobner/pdd_grobner.cpp

@@ -133,10 +133,12 @@ namespace dd {
             while (!done() && step()) {
                 TRACE("grobner", display(tout););
                 DEBUG_CODE(invariant(););
+                IF_VERBOSE(3, display_statistics(verbose_stream()));
             }
             DEBUG_CODE(invariant(););
         }
         catch (pdd_manager::mem_out) {
+            IF_VERBOSE(1, verbose_stream() << "mem-out\n");
             // don't reduce further
         }
     }
@@ -752,6 +754,7 @@ namespace dd {
         return 
             m_to_simplify.size() + m_processed.size() >= m_config.m_eqs_threshold || 
             canceled() || 
+            m_stats.m_compute_steps > m_config.m_max_steps ||
             m_conflict != nullptr;
     }
 
@@ -794,11 +797,14 @@ namespace dd {
     }
     
     void grobner::collect_statistics(statistics& st) const {
-        st.update("steps", m_stats.m_compute_steps);
-        st.update("simplified", m_stats.m_simplified);
-        st.update("superposed", m_stats.m_superposed);
-        st.update("degree", m_stats.m_max_expr_degree);
-        st.update("size", m_stats.m_max_expr_size);
+        st.update("dd.solver.steps", m_stats.m_compute_steps);
+        st.update("dd.solver.simplified", m_stats.m_simplified);
+        st.update("dd.solver.superposed", m_stats.m_superposed);
+        st.update("dd.solver.processed", m_processed.size());
+        st.update("dd.solver.solved", m_solved.size());
+        st.update("dd.solver.to_simplify", m_to_simplify.size());
+        st.update("dd.solver.degree", m_stats.m_max_expr_degree);
+        st.update("dd.solver.size", m_stats.m_max_expr_size);
     }
             
     std::ostream& grobner::display(std::ostream & out, const equation & eq) const {
@@ -811,6 +817,10 @@ namespace dd {
         out << "solved\n"; for (auto e : m_solved) display(out, *e);
         out << "processed\n"; for (auto e : m_processed) display(out, *e);
         out << "to_simplify\n"; for (auto e : m_to_simplify) display(out, *e);
+        return display_statistics(out);
+    }
+
+    std::ostream& grobner::display_statistics(std::ostream& out) const {
         statistics st;
         collect_statistics(st);
         st.display(out);

src/math/lp/nla_core.cpp

@@ -1419,13 +1419,40 @@ void core::run_pdd_grobner() {
     for (unsigned i : m_rows) {
         add_row_to_pdd_grobner(m_lar_solver.A_r().m_rows[i]);
     }
+
+   
+    // configure grobner
+    // TBD: move this code somewhere self-contained, and tune it.
+    double tree_size = 100;
+    for (auto* e : m_pdd_grobner.equations()) {
+        tree_size = std::max(tree_size, e->poly().tree_size());
+    }
+    tree_size *= 10;
+    struct dd::grobner::config cfg;
+    cfg.m_expr_size_limit = (unsigned)tree_size;
+    cfg.m_eqs_threshold = m_pdd_grobner.equations().size()*5;
+    cfg.m_max_steps = m_pdd_grobner.equations().size();
+    m_pdd_grobner = cfg;
+
+    m_pdd_manager.set_max_num_nodes(10000); // or something proportional to the number of initial nodes.
+
     m_pdd_grobner.saturate();
+    bool conflict = false;
     for (auto eq : m_pdd_grobner.equations()) {
-        check_pdd_eq(eq);
+        if (check_pdd_eq(eq)) {
+            conflict = true;
+            break;
+        }
+    }
+    if (conflict) {
+        IF_VERBOSE(2, verbose_stream() << "grobner conflict\n");
+    }
+    else {
+        IF_VERBOSE(2, verbose_stream() << "grobner miss\n");
     }
 }
 
-void core::check_pdd_eq(const dd::grobner::equation* e) {
+bool core::check_pdd_eq(const dd::grobner::equation* e) {
     dd::pdd_interval eval(m_pdd_manager, m_reslim);
     eval.var2interval() =
         [this](lpvar j, bool deps) {
@@ -1437,7 +1464,7 @@ void core::check_pdd_eq(const dd::grobner::equation* e) {
     auto i = eval.get_interval<dd::w_dep::without_deps>(e->poly());    
     dep_intervals di(m_reslim);
     if (!di.separated_from_zero(i))
-        return;
+        return false;
     auto i_wd = eval.get_interval<dd::w_dep::with_deps>(e->poly());  
     std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
                                                          add_empty_lemma();
@@ -1445,10 +1472,10 @@ void core::check_pdd_eq(const dd::grobner::equation* e) {
                                                      };
     if (di.check_interval_for_conflict_on_zero(i_wd, e->dep(), f)) {
         lp_settings().stats().m_grobner_conflicts++;
-        IF_VERBOSE(2, verbose_stream() << "grobner conflict\n");
+        return true;
     }
     else {
-        IF_VERBOSE(2, verbose_stream() << "grobner miss\n");
+        return false;
     }
 }
 

src/math/lp/nla_core.h

@@ -401,7 +401,7 @@ public:
     void set_active_vars_weights(nex_creator&);
     unsigned get_var_weight(lpvar) const;
     void add_row_to_pdd_grobner(const vector<lp::row_cell<rational>> & row);    
-    void check_pdd_eq(const dd::grobner::equation*);
+    bool check_pdd_eq(const dd::grobner::equation*);
     dd::pdd pdd_expr(const rational& c, lpvar j, u_dependency*&);
     void set_level2var_for_pdd_grobner();
 };  // end of core