port Grobner

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

src/math/lp/column_namer.h

@@ -25,12 +25,13 @@ class column_namer {
 public:
     virtual std::string get_variable_name(unsigned j) const = 0;
     template <typename T>
-    void print_row(const row_strip<T> & row, std::ostream & out) const {
+    std::ostream & print_row(const row_strip<T> & row, std::ostream & out) const {
         vector<std::pair<T, unsigned>> coeff;
         for (auto & p : row) {
             coeff.push_back(std::make_pair(p.coeff(), p.var()));
         }
         print_linear_combination_of_column_indices(coeff, out);
+        return out;
     }
     
     template <typename T>

src/math/lp/nex_creator.cpp

@@ -533,7 +533,7 @@ bool nex_creator::sum_is_simplified(const nex_sum* e) const {
     if (e->size() < 2)  return false;
     bool scalar = false;
     for (nex * ee : *e) {
-        TRACE("nla_cn", tout << "ee = " << *ee << "\n";);
+        TRACE("nla_cn_details", tout << "ee = " << *ee << "\n";);
         if (ee->is_sum()) {
             TRACE("nla_cn", tout << "not simplified e = " << *e << "\n"
                   << " has a child which is a sum " << *ee << "\n";);
@@ -854,7 +854,7 @@ void nex_creator::process_map_pair(nex *e, const rational& coeff, ptr_vector<nex
 
 bool nex_creator::is_simplified(const nex *e) const 
 {
-    TRACE("nla_cn", tout << "e = " << *e << "\n";);
+    TRACE("nla_cn_details", tout << "e = " << *e << "\n";);
     if (e->is_mul())
         return mul_is_simplified(to_mul(e));
     if (e->is_sum())

src/math/lp/nla_common.cpp

@@ -140,7 +140,7 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixe
     nex_mul * e = cn.mk_mul(cn.mk_scalar(coeff));
     for (lpvar k : m.vars()) {
         if (fixed_as_scalars && c().var_is_fixed(k)) {
-            auto & b = c().m_lar_solver.get_lower_bound(j).x;
+            auto & b = c().m_lar_solver.get_lower_bound(k).x;
             if (b.is_zero())
                 return nullptr;
             e->coeff() *=  b;
@@ -150,6 +150,7 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixe
         e->add_child(cn.mk_var(k));
         CTRACE("nla_horner", c().is_monic_var(k), c().print_var(k, tout) << "\n";);
     }
+    TRACE("nla_cn", tout << *e;);
     return e;
 }
 

src/math/lp/nla_grobner.cpp

@@ -140,8 +140,13 @@ common::ci_dependency* nla_grobner::dep_from_vector(svector<lp::constraint_index
 
 void nla_grobner::add_row(unsigned i) {    
     const auto& row = c().m_lar_solver.A_r().m_rows[i];    
-    TRACE("grobner", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout););
+    TRACE("grobner", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout) << '\n';
+          for (auto p : row) {
+              c().print_var(p.var(), tout) << "\n";
+          }
+          );
     nex_sum * ns = m_nex_creator.mk_sum();
+    
 
     svector<lp::constraint_index> fixed_vars_constraints;
     create_sum_from_row(row, m_nex_creator, *ns, true); // true to treat fixed vars as scalars
@@ -817,11 +822,14 @@ std::ostream& nla_grobner::display_equation(std::ostream & out, const equation &
 }
 
 void nla_grobner::assert_eq_0(nex* e, ci_dependency * dep) {
-    TRACE("grobner_e", tout << "e = " << *e << "\n";);
     if (e == nullptr || is_zero_scalar(e))
         return;
     equation * eq = alloc(equation);
     init_equation(eq, e, dep);
+    TRACE("grobner", display_equation(tout, *eq);
+    for (unsigned j : get_vars_of_expr(e)) {
+        c().print_var(j, tout) << "\n";
+    });
     insert_to_simplify(eq);
 }
 

src/math/lp/nla_grobner.h

@@ -147,9 +147,11 @@ private:
     
     std::ostream& display_dependency(std::ostream& out, ci_dependency*) const;
     void insert_to_simplify(equation *eq) {
+        SASSERT(!eq->exp()->is_scalar() || to_scalar(eq->exp())->value().is_zero());
         m_to_simplify.insert(eq);
     }
     void insert_to_superpose(equation *eq) {
+        SASSERT(!eq->exp()->is_scalar() || to_scalar(eq->exp())->value().is_zero());
         SASSERT(m_nex_creator.is_simplified(eq->exp()));
         m_to_superpose.insert(eq);
     }

src/smt/smt_context_pp.cpp

@@ -496,8 +496,6 @@ namespace smt {
 );
         display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic);
         out.close();
-        if (m_lemma_id==2559)
-            exit(1);
         return m_lemma_id;
     }