From f07d9a80c53c4b9f2f17449600b52f3ec5ed82cc Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 1 Oct 2019 11:18:25 -0700
Subject: [PATCH] fix nex simplification

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/cross_nested.h  |  1 +
 src/math/lp/nex.h           | 14 +++++++++++---
 src/math/lp/nex_creator.cpp | 16 +++++++++++-----
 src/math/lp/nex_creator.h   |  3 +--
 4 files changed, 24 insertions(+), 10 deletions(-)

diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h
index f6fa24dcc..dadede624 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -127,6 +127,7 @@ public:
         
         nex* c_over_f = m_nex_creator.mk_div(*c, f);
         c_over_f = m_nex_creator.simplify(c_over_f);
+        TRACE("nla_cn", tout << "c_over_f =" << *c_over_f << std::endl;);
         nex_mul* cm; 
         *c = cm = m_nex_creator.mk_mul(f, c_over_f);
         TRACE("nla_cn", tout << "common factor=" << *f << ", c=" << **c << "\ne = " << *m_e << "\n";);
diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h
index 18c9666ca..1ba5d1ea9 100644
--- a/src/math/lp/nex.h
+++ b/src/math/lp/nex.h
@@ -141,10 +141,18 @@ public:
     int& pow() { return m_power; }
     std::string to_string() const {
         std::stringstream s;
-        if (pow() == 1) {           
-            s <<"(" <<  *e() << ")";
+        if (pow() == 1) {
+            if (e()->is_elementary()) {
+                s << *e();
+            } else {
+                s <<"(" <<  *e() << ")";
+            }
         } else {
-            s << "(" << *e() << "^" << pow() << ")";
+            if (e()->is_elementary()){
+                s << "(" << *e() << "^" << pow() << ")";
+            } else {
+                s << "((" << *e() << ")^" << pow() << ")";
+            }
         }
         return s.str();
     }
diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp
index e2fbcbbff..f8ffb7369 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -464,7 +464,7 @@ void nex_creator::fill_map_with_children(std::map<nex*, rational, nex_lt> & m, p
         }
     }
     if (scalar && scalar->value().is_zero() == false) {
-        m[scalar] = rational();
+        m[scalar] = rational(scalar->value());
     }
     
 }
@@ -590,11 +590,17 @@ nex * nex_creator::mk_div(const nex* a, const nex* b) {
 }
 
 nex* nex_creator::simplify(nex* e) {
+    nex* es;
+    TRACE("nla_cn_details", tout << *e << std::endl;);
     if (e->is_mul())
-        return simplify_mul(to_mul(e));
-    if (e->is_sum())
-        return simplify_sum(to_sum(e));
-    return e;
+        es =  simplify_mul(to_mul(e));
+    else if (e->is_sum())
+        es =  simplify_sum(to_sum(e));
+    else
+        es = e;
+    TRACE("nla_cn_details", tout << "simplified = " << *es << std::endl;);
+    SASSERT(is_simplified(es));
+    return es;
 }
 
 bool nex_creator::is_simplified(const nex *e) const 
diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h
index 7e9806417..5845b1314 100644
--- a/src/math/lp/nex_creator.h
+++ b/src/math/lp/nex_creator.h
@@ -68,7 +68,6 @@ public:
     const svector<var_weight>& active_vars_weights() const { return m_active_vars_weights;}
 
     nex* simplify(nex* e);
-
     rational extract_coeff_from_mul(const nex_mul* m);
     rational extract_coeff(const nex*);
     
@@ -235,6 +234,6 @@ public:
     bool less_than_on_mul(const nex_mul* a, const nex_mul* b, bool skip_scalar) const;
     bool less_than_on_var_nex(const nex_var* a, const nex* b, bool skip_scalar) const;
     bool less_than_on_mul_nex(const nex_mul* a, const nex* b, bool skip_scalar) const;
-    void fill_map_with_children(std::map<nex*, rational, nex_lt> & m, ptr_vector<nex> & children);
+    void fill_map_with_children(std::map<nex*, rational, nex_lt> & m, ptr_vector<nex> & children);    
 };
 }