From d0d7813b9b2c7e39207115fe869a8c9164274ef9 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 6 Sep 2019 16:59:01 -0700
Subject: [PATCH] port grobner

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nla_grobner.cpp | 78 ++++++++++++++++++++++++++-----------
 src/math/lp/nla_grobner.h   | 23 +++++++++--
 2 files changed, 76 insertions(+), 25 deletions(-)

diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 6d12c8a15..3b9260620 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -50,9 +50,41 @@ void nla_grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std
         }
     }            
 }
-    
 
-void nla_grobner::find_rows() {
+var_weight nla_grobner::get_var_weight(lpvar j) const {
+    var_weight k;
+    switch (c().m_lar_solver.get_column_type(j)) {
+        
+    case lp::column_type::fixed:
+        k = var_weight::FIXED;
+        break;
+    case lp::column_type::boxed:
+        k = var_weight::BOUNDED;
+        break;
+    case lp::column_type::lower_bound:
+    case lp::column_type::upper_bound:
+        k = var_weight::NOT_FREE;
+    case lp::column_type::free_column:
+        k = var_weight::FREE;
+        break;
+    default:
+        UNREACHABLE();
+        break;
+    }
+    if (c().is_monomial_var(j)) {
+        return (var_weight)((int)k + 1);
+    }
+    return k;
+}
+
+void nla_grobner::set_active_vars_weights() {
+    m_active_vars_weights.resize(c().m_lar_solver.column_count());
+    for (lpvar j : m_active_vars) {
+        m_active_vars_weights[j] = get_var_weight(j);
+    }
+}
+
+void nla_grobner::find_nl_cluster() {
     prepare_rows_and_active_vars();
     std::queue<lpvar> q;
     for (lpvar j : c().m_to_refine) {        
@@ -67,8 +99,8 @@ void nla_grobner::find_rows() {
             continue;
         add_var_and_its_factors_to_q_and_collect_new_rows(j, q);
     }
-    
-
+    set_active_vars_weights();
+    TRACE("nla_grobner", display(tout););
 }
 
 void nla_grobner::prepare_rows_and_active_vars() {
@@ -78,25 +110,27 @@ void nla_grobner::prepare_rows_and_active_vars() {
     m_active_vars.resize(c().m_lar_solver.column_count());
 }
 
-void nla_grobner::grobner_lemmas() {
-    c().lp_settings().st().m_grobner_calls++;
-
-    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";
+void nla_grobner::display(std::ostream & out) {
+    const auto& matrix = c().m_lar_solver.A_r();
+    out << "rows = " << m_rows.size() << "\n";
+    for (unsigned k : m_rows) {
+        c().print_term(matrix.m_rows[k], out) << "\n";
+    }
+    out << "the matrix =\n";
           
-          for (const auto & r : matrix.m_rows) {
-              c().print_term(r, tout) << std::endl;
-          }
-          }
-          );
+    for (const auto & r : matrix.m_rows) {
+        c().print_term(r, out) << std::endl;
+    }
+}
+
+void nla_grobner::init() {
+    find_nl_cluster();
+}
+
+void nla_grobner::grobner_lemmas() {
+    c().lp_settings().st().m_grobner_calls++;    
+    init();
+
     SASSERT(false);
 }
 } // end of nla namespace
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index 23e20aaf9..d6cb74e36 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -24,15 +24,32 @@
 namespace nla {
 class core;
 
+enum class var_weight {
+        FIXED = 0,
+            QUOTED_FIXED =  1,
+            BOUNDED    =    2,
+            QUOTED_BOUNDED = 3,
+            NOT_FREE      =  4,
+            QUOTED_NOT_FREE = 5,
+            FREE          =   6,
+            QUOTED_FREE    = 7,
+            MAX_DEFAULT_WEIGHT = 7
+            };
+
 class nla_grobner : common {
-    lp::int_set m_rows;
-    lp::int_set m_active_vars;
+    lp::int_set         m_rows;
+    lp::int_set         m_active_vars;
+    svector<var_weight> m_active_vars_weights;
 public:
     nla_grobner(core *core);
     void grobner_lemmas();
 private:
-    void find_rows();
+    void find_nl_cluster();
     void prepare_rows_and_active_vars();
     void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j,  std::queue<lpvar>& q);
+    void display(std::ostream&);
+    void set_active_vars_weights();
+    void init();
+    var_weight get_var_weight(lpvar) const;
 }; // end of grobner
 }