From d5f574ffc5db147520cb4b2eaf554bed4c454b34 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 11 Oct 2019 17:36:30 -0700
Subject: [PATCH] fixes in nex order

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nex_creator.cpp | 50 ++++++++++++++++++++++---------------
 src/math/lp/nex_creator.h   |  3 ++-
 src/test/lp/lp.cpp          |  4 +--
 3 files changed, 34 insertions(+), 23 deletions(-)

diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp
index cd9ecccb5..8375e2a8b 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -115,29 +115,17 @@ void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational&
     TRACE("nla_cn_details", print_vector(children, tout););    
 }
 
-bool nex_creator::less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const {
-    SASSERT(is_simplified(a));
-    SASSERT(is_simplified(b));
-    unsigned a_deg = a->get_degree();
-    unsigned b_deg = b->get_degree();
-    if (a_deg > b_deg)
-        return true;
-    if (a_deg < b_deg)
-        return false;
+bool nex_creator::less_than_on_mul_mul_same_degree_iterate(const nex_mul* a, const nex_mul* b) const {
+    bool inside_a_p = false; // inside_a_p is true means we still compare the old position of it_a
+    bool inside_b_p = false; // inside_b_p is true means we still compare the old position of it_b
+    const nex* ae = nullptr;
+    const nex* be = nullptr;
     auto it_a  = a->begin();
     auto it_b  = b->begin();
     auto a_end = a->end();
     auto b_end = b->end();
     unsigned a_pow, b_pow;
-    bool inside_a_p = false; // inside_a_p is true means we still compare the old position of it_a
-    bool inside_b_p = false; // inside_b_p is true means we still compare the old position of it_b
-    const nex* ae = nullptr;
-    const nex *be = nullptr;
-    if (it_a == a_end) {
-        return it_b != b_end;
-    }
-    if (it_b == b_end)
-        return false;
+
     for (; ;) {
         if (!inside_a_p) {
             ae = it_a->e();
@@ -185,6 +173,28 @@ bool nex_creator::less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const
     }
     TRACE("nla_cn_details", tout << "a = " << *a << " >= b = " << *b << "\n";);
     return false;
+    
+}
+
+bool nex_creator::less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_mul* b) const {
+    SASSERT(a->get_degree() == b->get_degree());
+    SASSERT(a->size() && b->size());
+    return less_than_on_mul_mul_same_degree_iterate(a, b);    
+}
+
+bool nex_creator::less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const {
+    SASSERT(is_simplified(a) && is_simplified(b));
+    unsigned a_deg = a->get_degree();
+    unsigned b_deg = b->get_degree();
+    bool ret;
+    if (a_deg > b_deg) {
+        ret = true;
+    } else if (a_deg < b_deg) {
+        ret = false;
+    } else {
+        ret = less_than_on_mul_mul_same_degree(a, b);
+    }
+    return ret;
 
 }
 
@@ -752,8 +762,8 @@ bool nex_creator::equal(const nex* a, const nex* b) {
     }
     nex * ca = cn.canonize(a);
     nex * cb = cn.canonize(b);
-    TRACE("nla_cn_test", tout << "a = " << *a << ", canonized a = " << *ca << "\n";);
-    TRACE("nla_cn_test", tout << "b = " << *b << ", canonized b = " << *cb << "\n";);
+    TRACE("nla_cn_details", tout << "a = " << *a << ", canonized a = " << *ca << "\n";);
+    TRACE("nla_cn_details", tout << "b = " << *b << ", canonized b = " << *cb << "\n";);
     return !(cn.lt(ca, cb) || cn.lt(cb, ca));
 }
 #endif
diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h
index ab0b825fe..dbf47c0d4 100644
--- a/src/math/lp/nex_creator.h
+++ b/src/math/lp/nex_creator.h
@@ -95,7 +95,6 @@ public:
     
     void simplify_children_of_mul(vector<nex_pow> & children, rational&);
 
-
     nex * clone(const nex* a) {        
         switch (a->type()) {
         case expr_type::VAR: {
@@ -253,6 +252,8 @@ public:
 
     bool lt(const nex* a, const nex* b) const;    
     bool less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const;
+    bool less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_mul* b) const;
+    bool less_than_on_mul_mul_same_degree_iterate(const nex_mul* a, const nex_mul* b) const;
     bool less_than_on_var_nex(const nex_var* a, const nex* b) const;
     bool less_than_on_mul_nex(const nex_mul* a, const nex* b) const;
     bool less_than_on_sum_sum(const nex_sum* a, const nex_sum* b) const;
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index f32bc1766..8c13d2c10 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -184,9 +184,9 @@ void test_cn_shorter() {
     bcg->add_child(min_1);
     nex* abcd = cr.mk_mul(a, b, c, d);
     nex* eae = cr.mk_mul(e, a, e);
-    nex* eac = cr.mk_mul(e, a, c);
+    nex* three_eac = cr.mk_mul(e, a, c); to_mul(three_eac)->coeff() = rational(3);
     nex* _6aad = cr.mk_mul(cr.mk_scalar(rational(6)), a, a, d);
-    clone = to_sum(cr.clone(cr.mk_sum(_6aad, abcd, eae, eac)));
+    clone = to_sum(cr.clone(cr.mk_sum(_6aad, abcd, eae, three_eac)));
     clone = to_sum(cr.simplify(clone));
     TRACE("nla_test", tout << "clone = " << *clone << "\n";);
     //    test_cn_on_expr(cr.mk_sum(aad,  abcd, aaccd, add, eae, eac, ed), cn);