start porting grobner basis functionality

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/lp/horner.cpp

@@ -45,7 +45,7 @@ bool horner::row_is_interesting(const T& row) const {
         return false;
     }
     SASSERT(row_has_monomial_to_refine(row));
-    m_row_var_set.clear();
+    c().clear_row_var_set();
     for (const auto& p : row) {
         lpvar j = p.var();
         if (!c().is_monomial_var(j))
@@ -53,11 +53,11 @@ bool horner::row_is_interesting(const T& row) const {
         auto & m = c().emons()[j];
         
         for (lpvar k : m.vars()) {
-            if (m_row_var_set.contains(k))
+            if (c().row_var_set_contains(k))
                 return true;
         }
         for (lpvar k : m.vars()) {
-            m_row_var_set.insert(k);
+            c().insert_to_row_var_set(k);
         }
     }
     return false;
@@ -113,7 +113,7 @@ void horner::horner_lemmas() {
         for (auto & s : matrix.m_columns[j])
             rows_to_check.insert(s.var());
     }
-    m_row_var_set.resize(c().m_lar_solver.number_of_vars());
+    c().prepare_row_var_set();
     svector<unsigned> rows;
     for (unsigned i : rows_to_check) {
         if (row_is_interesting(matrix.m_rows[i]))

src/math/lp/horner.h

@@ -32,7 +32,6 @@ class core;
 class horner : common {
     intervals             m_intervals;
     nex_sum               m_row_sum;
-    mutable lp::int_set   m_row_var_set;
 public:
     typedef intervals::interval interv;
     horner(core *core);

src/math/lp/lar_solver.h

@@ -636,6 +636,7 @@ public:
     void update_delta_for_terms(const impq & delta, unsigned j, const vector<unsigned>&);
     void fill_vars_to_terms(vector<vector<unsigned>> & vars_to_terms);
     unsigned column_count() const { return A_r().column_count(); }
+    unsigned row_count() const { return A_r().row_count(); }
     const vector<unsigned> & r_basis() const { return m_mpq_lar_core_solver.r_basis(); }
     const vector<unsigned> & r_nbasis() const { return m_mpq_lar_core_solver.r_nbasis(); }
     bool get_equality_and_right_side_for_term_on_current_x(unsigned i, mpq &rs, constraint_index& ci, bool &upper_bound) const;

src/math/lp/lp_settings.h

@@ -110,6 +110,8 @@ struct stats {
     unsigned m_horner_calls;
     unsigned m_horner_conflicts;
     unsigned m_cross_nested_forms;
+    unsigned m_grobner_calls;
+    unsigned m_grobner_conflicts;
     stats() { reset(); }
     void reset() { memset(this, 0, sizeof(*this)); }
 };

src/math/lp/nla_core.h

@@ -93,14 +93,31 @@ public:
 private:
     emonomials               m_emons;
     svector<lpvar>           m_add_buffer;
+    mutable lp::int_set      m_row_var_set;
 public:
-    reslimit                   m_reslim;
+    reslimit                 m_reslim;
+
+    
+    const lp::int_set&  row_var_set () const { return m_row_var_set;}
+    bool row_var_set_contains(unsigned j) const { return m_row_var_set.contains(j); }
+
+    void insert_to_row_var_set(unsigned j) const { m_row_var_set.insert(j); }    
+
+    void clear_row_var_set() const {
+        m_row_var_set.clear();
+    }
+
+    void prepare_row_var_set() const {
+        m_row_var_set.clear();
+        m_row_var_set.resize(m_lar_solver.number_of_vars());
+    }
+    
     reslimit &               reslim() { return m_reslim; }  
     emonomials& emons() { return m_emons; }
     const emonomials& emons() const { return m_emons; }
     // constructor
     core(lp::lar_solver& s, reslimit &);
-
+   
     bool compare_holds(const rational& ls, llc cmp, const rational& rs) const;
     
     rational value(const lp::lar_term& r) const;

src/math/lp/nla_grobner.cpp

@@ -0,0 +1,104 @@
+/*++
+  Copyright (c) 2017 Microsoft Corporation
+
+  Module Name:
+
+  <name>
+
+  Abstract:
+
+  <abstract>
+
+  Author:
+  Nikolaj Bjorner (nbjorner)
+  Lev Nachmanson (levnach)
+
+  Revision History:
+
+
+  --*/
+#include "math/lp/nla_grobner.h"
+#include "math/lp/nla_core.h"
+#include "math/lp/factorization_factory_imp.h"
+namespace nla {
+nla_grobner::nla_grobner(core *c) : common(c) {}
+
+void nla_grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue<lpvar> & q) {
+    SASSERT(m_active_vars.contains(j) == false);
+    const auto& matrix = c().m_lar_solver.A_r();
+    m_active_vars.insert(j);
+    for (auto & s : matrix.m_columns[j]) {
+        unsigned row = s.var();
+        if (m_rows.contains(row)) continue;
+        m_rows.insert(row);
+        for (auto& rc : matrix.m_rows[row]) {
+            if (m_active_vars.contains(rc.var()))
+                continue;
+            q.push(rc.var());
+        }
+    }
+
+    if (!c().is_monomial_var(j))
+        return;
+
+    const monomial& m = c().emons()[j];
+    for (auto fcn : factorization_factory_imp(m, c())) {
+        for (const factor& fc: fcn) {
+            lpvar j = var(fc);
+            if (! m_active_vars.contains(j))
+                add_var_and_its_factors_to_q_and_collect_new_rows(j, q);
+        }
+    }            
+}
+    
+
+void nla_grobner::find_rows() {
+    prepare_rows_and_active_vars();
+    std::queue<lpvar> q;
+    for (lpvar j : c().m_to_refine) {        
+        TRACE("nla_grobner", c().print_monomial(c().emons()[j], tout) << "\n";);
+        q.push(j);
+    }
+
+    while (!q.empty()) {
+        unsigned j = q.front();        
+        q.pop();
+        if (m_active_vars.contains(j))
+            continue;
+        add_var_and_its_factors_to_q_and_collect_new_rows(j, q);
+    }
+    
+
+}
+
+void nla_grobner::prepare_rows_and_active_vars() {
+    m_rows.clear();
+    m_rows.resize(c().m_lar_solver.row_count());
+    m_active_vars.clear();
+    m_active_vars.resize(c().m_lar_solver.column_count());
+}
+
+void nla_grobner::grobner_lemmas() {
+    c().lp_settings().st().m_grobner_calls++;
+    if (c().lp_settings().st().m_grobner_calls == 2)
+        SASSERT(false);
+
+
+    find_rows();
+
+    TRACE("nla_grobner",
+          {
+              const auto& matrix = c().m_lar_solver.A_r();
+          tout << "rows = " << m_rows.size() << "\n";
+          for (unsigned k : m_rows) {
+              c().print_term(matrix.m_rows[k], tout) << "\n";
+          }
+          tout << "the matrix =\n";
+          
+          for (const auto & r : matrix.m_rows) {
+              c().print_term(r, tout) << "\n";
+          }
+          }
+          );
+}
+} // end of nla namespace

src/math/lp/nla_grobner.h

@@ -0,0 +1,38 @@
+/*++
+  Copyright (c) 2017 Microsoft Corporation
+
+  Module Name:
+
+  <name>
+
+  Abstract:
+
+  <abstract>
+
+  Author:
+  Nikolaj Bjorner (nbjorner)
+  Lev Nachmanson (levnach)
+
+  Revision History:
+
+
+  --*/
+#pragma once
+
+#include "math/lp/nla_common.h"
+#include "math/lp/nex.h"
+namespace nla {
+class core;
+
+class nla_grobner : common {
+    lp::int_set m_rows;
+    lp::int_set m_active_vars;
+public:
+    nla_grobner(core *core);
+    void grobner_lemmas();
+private:
+    void find_rows();
+    void prepare_rows_and_active_vars();
+    void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j,  std::queue<lpvar>& q);
+}; // end of grobner
+}

src/smt/theory_lra.cpp

@@ -3791,6 +3791,8 @@ public:
         st.update("horner-calls", lp().settings().st().m_horner_calls);
         st.update("horner-conflicts", lp().settings().st().m_horner_conflicts);
         st.update("horner-cross-nested-forms", lp().settings().st().m_cross_nested_forms);
+        st.update("grobner-calls", lp().settings().st().m_grobner_calls);
+        st.update("grobner-conflicts", lp().settings().st().m_grobner_conflicts);
         st.update("nla-explanations", m_stats.m_nla_explanations);
         st.update("nla-lemmas", m_stats.m_nla_lemmas);
     }