port Grobner

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

src/math/grobner/grobner.cpp

@@ -586,25 +586,20 @@ grobner::equation * grobner::copy_equation(equation const * eq) {
 // source 3f + k = 0, so f = -k/3
 // target 2fg + e = 0  
 // target is replaced by 2(-k/3)g + e = -2/3kg + e
-unsigned grobner::simplify_loop_on_target_monomials(equation const * source, equation * target, bool & result) {
+bool grobner::simplify_target_monomials(equation const * source, equation * target) {
     unsigned i          = 0;
     unsigned new_target_sz = 0;
-    unsigned sz         = target->m_monomials.size();
+    unsigned target_sz         = target->m_monomials.size();
     monomial const * LT = source->get_monomial(0); 
     m_tmp_monomials.reset();
-    for (; i < sz; i++) {
+    for (; i < target_sz; i++) {
         monomial * targ_i = target->m_monomials[i];
         if (divide_ignore_coeffs(targ_i, LT)) {
             if (i == 0)
                 m_changed_leading_term = true;
-            if (!result) {  // first time that source is being applied.
-                target->m_dep = m_dep_manager.mk_join(target->m_dep, source->m_dep);
-                result         = true;
-            }
-            rational coeff = - targ_i->m_coeff / (LT->m_coeff);
             if (!m_tmp_vars1.empty())
                 target->m_lc = false;
-            mul_append_skip_first(source, coeff, m_tmp_vars1);
+            mul_append_skip_first(source, - targ_i->m_coeff / (LT->m_coeff), m_tmp_vars1);
             del_monomial(targ_i);
         }
         else {
@@ -614,16 +609,20 @@ unsigned grobner::simplify_loop_on_target_monomials(equation const * source, equ
             new_target_sz++;
         }
     }
-    return new_target_sz;
+    if (new_target_sz < target_sz) {
+        target->m_monomials.shrink(new_target_sz);
+        target->m_monomials.append(m_tmp_monomials.size(), m_tmp_monomials.c_ptr());
+        simplify_eq(target);
+        TRACE("grobner", tout << "result: "; display_equation(tout, *target););
+        return true;
+    }
+    return false;
 }
 
 /**
    \brief Simplify the target equation using the source as a rewrite rule.
    Return 0 if target was not simplified.
 
-   LN. The rest of the comment seems to be incorrect: there is no m_scope_lvl
-   Return target if target was simplified
-   Return new_equation if source->m_scope_lvl > target->m_scope_lvl, moreover target is freezed, and new_equation contains the result.
 */
 grobner::equation * grobner::simplify_source_target(equation const * source, equation * target) {
     TRACE("grobner", tout << "simplifying: "; display_equation(tout, *target); tout << "using: "; display_equation(tout, *source););
@@ -632,18 +631,18 @@ grobner::equation * grobner::simplify_source_target(equation const * source, equ
     m_stats.m_simplify++;
     bool result = false;
     do {
-        unsigned target_new_size = simplify_loop_on_target_monomials(source, target, result);
+        if (simplify_target_monomials(source, target)) {
-        if (target_new_size < target->m_monomials.size()) {
+            result = true;
-            target->m_monomials.shrink(target_new_size);
-            target->m_monomials.append(m_tmp_monomials.size(), m_tmp_monomials.c_ptr());
-            simplify_eq(target);
         } else {
             break;
         }
-    }
+    }  while (!m_manager.canceled());
-    while (!m_manager.canceled());
     TRACE("grobner", tout << "result: "; display_equation(tout, *target););
-    return result ? target : nullptr;
+    if (result) {
+        target->m_dep = m_dep_manager.mk_join(target->m_dep, source->m_dep);
+        return target;
+    }
+    return nullptr;
 }
 
 /**

src/math/grobner/grobner.h

@@ -166,7 +166,7 @@ protected:
     equation * copy_equation(equation const * eq);
 
     equation * simplify_source_target(equation const * source, equation * target);
-    unsigned simplify_loop_on_target_monomials(equation const * source, equation * target, bool&);
+    bool simplify_target_monomials(equation const * source, equation * target);
 
     equation * simplify_using_processed(equation * eq);
 

src/math/lp/nla_grobner.cpp

@@ -200,7 +200,7 @@ void nla_grobner::init() {
 }
 
 bool nla_grobner::is_trivial(equation* eq) const {
-    return eq->m_exp->size() == 0;
+    return eq->m_expr->size() == 0;
 }
 
 bool nla_grobner::is_better_choice(equation * eq1, equation * eq2) {
@@ -210,7 +210,7 @@ bool nla_grobner::is_better_choice(equation * eq1, equation * eq2) {
         return true;
     if (is_trivial(eq2))
         return false;
-    return m_nex_creator.lt(eq1->m_exp, eq2->m_exp);
+    return m_nex_creator.lt(eq1->m_expr, eq2->m_expr);
 }
 
 void nla_grobner::del_equation(equation * eq) {
@@ -266,10 +266,15 @@ nla_grobner::equation* nla_grobner::simplify_using_processed(equation* eq) {
 
 }
 
+// source 3f + k = 0, so f = -k/3
+// target 2fg + e = 0  
+// target is replaced by 2(-k/3)g + e = -2/3kg + e
 unsigned nla_grobner::simplify_loop_on_target_monomials(equation const * source, equation * target, bool & result) {
+    TRACE("nla_grobner", tout << "source = " << *source->exp() << " , target = " << *target->exp() << "\n";);
     unsigned i          = 0;
-    unsigned n_sz = 0;
+    unsigned new_target_sz = 0;
-    unsigned sz         = target->m_exp->size();
+    unsigned sz         = target->exp()->size();
+    //if (source->exp()->is_sum() && target->exp()->is_su
     NOT_IMPLEMENTED_YET();
     /*
     monomial const * LT = source->get_monomial(0); 
@@ -300,7 +305,7 @@ unsigned nla_grobner::simplify_loop_on_target_monomials(equation const * source,
             target->m_monomials[n_sz++] = curr;
         }
         }*/
-    return n_sz;
+    return 1;
 }
 
 
@@ -312,7 +317,7 @@ nla_grobner::equation * nla_grobner::simplify_source_target(equation const * sou
     bool result = false;
     do {
         unsigned target_new_size = simplify_loop_on_target_monomials(source, target, result);
-        if (target_new_size < target->m_exp->size()) {
+        if (target_new_size < target->exp()->size()) {
             NOT_IMPLEMENTED_YET();
             /*
               target->m_monomials.shrink(target_new_size);
@@ -612,7 +617,7 @@ nla_grobner::equation * nla_grobner::simplify(equation const * source, equation
 }
 
 std::ostream& nla_grobner::display_equation(std::ostream & out, const equation & eq) {
-    out << "m_exp = " << *eq.m_exp << "\n";
+    out << "m_exp = " << *eq.exp() << "\n";
     out << "dep = "; display_dependency(out, eq.m_dep) << "\n";
     return out;
 }
@@ -635,7 +640,7 @@ void nla_grobner::init_equation(equation* eq, nex*e, ci_dependency * dep) {
     eq->m_bidx      = bidx;
     eq->m_dep       = dep;
     eq->m_lc        = true;
-    eq->m_exp =       e;
+    eq->exp()       = e;
     m_equations_to_delete.push_back(eq);
     SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
 }

src/math/lp/nla_grobner.h

@@ -41,15 +41,16 @@ class nla_grobner : common {
     class equation {
         unsigned                   m_bidx:31;       //!< position at m_equations_to_delete
         unsigned                   m_lc:1;          //!< true if equation if a linear combination of the input equations.
-        nex *                      m_exp;           //  simplified expressionted monomials
+        nex *                      m_expr;           //  simplified expressionted monomials
         ci_dependency *            m_dep;           //!< justification for the equality
         friend class nla_grobner;
         equation() {}
     public:
-        unsigned get_num_monomials() const { return m_exp->size(); }
+        unsigned get_num_monomials() const { return m_expr->size(); }
         nex_mul* const * get_monomial(unsigned idx) const { NOT_IMPLEMENTED_YET();
             return nullptr; }
-        nex* & exp() { return m_exp; }
+        nex* & exp() { return m_expr; }
+        const nex*  exp() const { return m_expr; }
         ci_dependency * get_dependency() const { return m_dep; }
         unsigned hash() const { return m_bidx; }
         bool is_linear_combination() const { return m_lc; }