From cef9726f0070b21d25ccb8670b5ef7854cb18ca9 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 18 Jul 2019 11:05:12 -0700
Subject: [PATCH] fixes in nla_expr operators and delete m_reported

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/cross_nested.h |  8 +-------
 src/math/lp/nla_expr.h     | 15 ++++++++++++++-
 src/test/lp/lp.cpp         | 12 +++++-------
 3 files changed, 20 insertions(+), 15 deletions(-)

diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h
index eee3928f6..959664de8 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -25,7 +25,6 @@ class cross_nested {
     typedef nla_expr<rational> nex;
     nex& m_e;
     std::function<void (const nex&)> m_call_on_result;
-    std::set<nex> m_reported;
 public:
     cross_nested(nex &e, std::function<void (const nex&)> call_on_result): m_e(e), m_call_on_result(call_on_result) {}
 
@@ -105,12 +104,7 @@ public:
                 auto e_to_report = m_e;
                 e_to_report.simplify();
                 e_to_report.sort();
-                if (m_reported.find(e_to_report) == m_reported.end()) {
-                    m_reported.insert(e_to_report);
-                    m_call_on_result(e_to_report);
-                } else {
-                    TRACE("nla_cn", tout << "do not report " << e_to_report << "\n";);
-                }
+                m_call_on_result(e_to_report);
             } else {
                 nex* c = pop_back(front);
                 cross_nested_of_expr_on_front_elem(c, front);     
diff --git a/src/math/lp/nla_expr.h b/src/math/lp/nla_expr.h
index 3e598cd68..146214c1e 100644
--- a/src/math/lp/nla_expr.h
+++ b/src/math/lp/nla_expr.h
@@ -396,6 +396,11 @@ public:
 
     
     nla_expr& operator/=(const nla_expr& b) {
+        TRACE("nla_cn_details", tout << *this <<", " << b << "\n";);
+        if (b.is_var()) {
+            *this = (*this) / b.var();
+            return *this;
+        }
         SASSERT(b.is_mul());
         if (is_sum()) {
             for (auto & e : children()) {
@@ -403,6 +408,10 @@ public:
             }
             return *this;
         }
+        if (is_var()) {
+            *this = scalar(T(1));
+            return *this;
+        }
         SASSERT(is_mul());
         auto powers = b.get_powers_from_mul();
         unsigned i = 0, k = 0;
@@ -496,6 +505,7 @@ nla_expr<T> operator*(const nla_expr<T>& a, const nla_expr<T>& b) {
 
 template <typename T> 
 nla_expr<T> operator/(const nla_expr<T>& a, lpvar j) {
+    TRACE("nla_cn_details", tout << "a=" << a << ", v" << j << "\n";);
     SASSERT((a.is_mul() && a.contains(j)) || (a.is_var() && a.var() == j));
     if (a.is_var())
         return nla_expr<T>::scalar(T(1));
@@ -514,8 +524,11 @@ nla_expr<T> operator/(const nla_expr<T>& a, lpvar j) {
     }
     if (b.children().size() > 1) {
         b.type() = expr_type::MUL;
+    } else if (b.children().size() == 1) {
+        auto t = b.children()[0];
+        b = t;        
     } else {
-        b = b.children()[0];
+        b = nla_expr<T>::scalar(T(1));
     }
     return b;
 }
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index 485dab113..6d1a8e10d 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -71,11 +71,6 @@ void test_cn_on_expr(horner::nex t) {
     TRACE("nla_cn", tout << "t=" << t << '\n';);
     cross_nested cn(t, [](const horner::nex& n) {
                            TRACE("nla_cn", tout << n << "\n";);
-                           auto nn = n;
-                           nn.simplify();                               
-                           nn.sort();
-                           TRACE("nla_cn", tout << "ordered version\n" << nn << "\n______________________\n";);
-                           
                        } );
     cn.run();
 }
@@ -87,9 +82,12 @@ void test_cn() {
     enable_trace("nla_cn_cn");
     nex a = nex::var(0), b = nex::var(1), c = nex::var(2), d = nex::var(3), e = nex::var(4);
     
+    test_cn_on_expr(a*b*d + a*b*c + c*b*d + a*c*d);
+    test_cn_on_expr(a*b*b*d*d + a*b*b*c*d + c*b*b*d);
+    TRACE("nla_cn", tout << "done\n";);
     test_cn_on_expr(a*b*d + a*b*c + c*b*d);
-    // nex t = a*a*d + a*b*c*d + a*a*c*c*d + a*d*d + e*a*e + e*a*c + e*d;
-    // test_cn_on_expr(t);
+    nex t = a*a*d + a*b*c*d + a*a*c*c*d + a*d*d + e*a*e + e*a*c + e*d;
+    test_cn_on_expr(t);
 }
 
 } // end of namespace nla