fix nex order and cross_nested

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

src/math/lp/cross_nested.h

@@ -91,10 +91,7 @@ public:
         nex_mul* f = m_nex_creator.mk_mul();
         for(const auto & p : m_nex_creator.occurences_map()) { // randomize here: todo
             if (p.second.m_occs == size) {
-                unsigned pow = p.second.m_power;
+                f->add_child_in_power(m_nex_creator.mk_var(p.first), p.second.m_power);
-                while (pow --) {
-                    f->add_child(m_nex_creator.mk_var(p.first));
-                }
             }
         }
         return f;

src/math/lp/nex.h

@@ -202,6 +202,10 @@ public:
         return out;
     }
 
+    void add_child(const rational& r) {
+        m_coeff *= r;
+    }
+    
     void add_child(nex* e) {
         if (e->is_scalar()) {
             m_coeff *= to_scalar(e)->value();

src/math/lp/nex_creator.cpp

@@ -123,7 +123,7 @@ bool nex_creator::less_than_on_mul_mul_same_degree_iterate(const nex_mul* a, con
     auto a_end = a->end();
     auto b_end = b->end();
     unsigned a_pow, b_pow;
-    bool ret;
+    int ret = - 1;
     do {
         if (!inside_a_p) { a_pow = it_a->pow(); }
         if (!inside_b_p) { b_pow = it_b->pow(); }
@@ -141,14 +141,14 @@ bool nex_creator::less_than_on_mul_mul_same_degree_iterate(const nex_mul* a, con
             it_a++; it_b++;
             if (it_a == a_end) {
                 if (it_b != b_end) {
-                    ret = true;
+                    ret = false;
                     break;
                 }
                 SASSERT(it_a == a_end && it_b == b_end);
                 ret = a->coeff() < b->coeff();
                 break;
             }
-            if (it_b == b_end) {
+            if (it_b == b_end) { // it_a is not at the end
                 ret = false;
                 break;
             }
@@ -176,7 +176,8 @@ bool nex_creator::less_than_on_mul_mul_same_degree_iterate(const nex_mul* a, con
             inside_b_p = false;
         }
     } while (true);
-    
+    if (ret == -1)
+        ret = true;
     TRACE("nla_cn_details", tout << "a = " << *a << (ret == 1?" < ":" >= ") << *b << "\n";);
     return ret;
 }
@@ -193,9 +194,9 @@ bool nex_creator::less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const
     unsigned b_deg = b->get_degree();
     bool ret;
     if (a_deg > b_deg) {
-        ret = true;
-    } else if (a_deg < b_deg) {
         ret = false;
+    } else if (a_deg < b_deg) {
+        ret = true;
     } else {
         ret = less_than_on_mul_mul_same_degree(a, b);
     }

src/test/lp/lp.cpp

@@ -74,6 +74,38 @@ void test_cn_on_expr(nex_sum *t, cross_nested& cn) {
     cn.run(t);
 }
 
+void test_nex_order() {
+    enable_trace("nla_cn");
+    enable_trace("nla_cn_details");
+    // enable_trace("nla_cn_details_");
+    enable_trace("nla_test");
+    nex_creator r;
+    r.set_number_of_vars(3);
+    for (unsigned j = 0; j < r.get_number_of_vars(); j++)
+        r.set_var_weight(j, j);
+    nex_var* a = r.mk_var(0);
+    nex_var* b = r.mk_var(1);
+    nex_var* c = r.mk_var(2);
+    SASSERT(r.lt(a, b));
+    nex* ab = r.mk_mul(a, b);
+    nex* ba = r.mk_mul(b, a);
+    nex* ac = r.mk_mul(a, c);
+    SASSERT(r.lt(ab, ac));
+    SASSERT(!r.lt(ac, ab));
+    nex* _3ac = r.mk_mul(rational(3), a, c);
+    nex* _2ab = r.mk_mul(rational(2), a, b);
+    SASSERT(r.lt(ab, _3ac));
+    SASSERT(!r.lt(_3ac, ab));
+    SASSERT(r.lt(a, ab));
+    SASSERT(!r.lt(ab, a));
+    SASSERT(r.lt(_2ab, _3ac));
+    SASSERT(!r.lt(_3ac, _2ab));
+    nex* _2a = r.mk_mul(rational(2), a);
+    SASSERT(r.lt(_2a, _2ab));
+    SASSERT(!r.lt(_2ab, _2a));
+    SASSERT(nex_creator::equal(ab, ba));
+}
+
 void test_simplify() {
 #ifdef Z3DEBUG
     nex_creator r;
@@ -2101,6 +2133,7 @@ void test_replace_column() {
 
 
 void setup_args_parser(argument_parser & parser) {
+    parser.add_option_with_help_string("-nex_order", "test nex order");
     parser.add_option_with_help_string("-nla_cn", "test cross nornmal form");
     parser.add_option_with_help_string("-nla_sim", "test nex simplify");
     parser.add_option_with_help_string("-nla_blfmz_mf", "test_basic_lemma_for_mon_zero_from_factor_to_monomial");
@@ -3813,6 +3846,11 @@ void test_lp_local(int argn, char**argv) {
         return finalize(0);
     }
 
+    if (args_parser.option_is_used("-nex_order")) {
+        nla::test_nex_order();
+        return finalize(0);
+    }
+
     
     if (args_parser.option_is_used("-nla_order")) {
 #ifdef Z3DEBUG