From a888e79696ef3e29d456724b3981bd71f72390c0 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 2 Oct 2019 17:14:34 -0700
Subject: [PATCH] fix nex simplification

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

diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp
index 3d729a41a..21151abfc 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -61,15 +61,15 @@ nex * nex_creator::mk_div(const nex* a, lpvar j) {
     return mk_mul(bv);
 }
 
-bool nex_creator::eat_scalar_pow(nex_scalar *& r, nex_pow& p) {
+bool nex_creator::eat_scalar_pow(nex_scalar *& r, nex_pow& p, unsigned pow) {
     if (!p.e()->is_scalar())
         return false;
     nex_scalar *pe = to_scalar(p.e());
     if (r == nullptr) {
         r = pe;
-        r->value() = r->value().expt(p.pow());                
+        r->value() = r->value().expt(p.pow()*pow);                
     } else {
-        r->value() *= pe->value().expt(p.pow());
+        r->value() *= pe->value().expt(p.pow()*pow);
     }
     return true;
 }
@@ -82,7 +82,7 @@ void nex_creator::simplify_children_of_mul(vector<nex_pow> & children) {
     int skipped = 0;
     for(unsigned j = 0; j < children.size(); j++) {        
         nex_pow& p = children[j];
-        if (eat_scalar_pow(r, p)) {
+        if (eat_scalar_pow(r, p, 1)) {
             skipped++;
             continue;
         }
@@ -101,8 +101,10 @@ void nex_creator::simplify_children_of_mul(vector<nex_pow> & children) {
     children.shrink(children.size() - to_promote.size() - skipped);
 
     for (nex_pow & p : to_promote) {
+        TRACE("nla_cn_details", tout << p << "\n";);
         for (nex_pow& pp : to_mul(p.e())->children()) {
-            if (!eat_scalar_pow(r, pp))
+            TRACE("nla_cn_details", tout << pp << "\n";);
+            if (!eat_scalar_pow(r, pp, p.pow()))
                 children.push_back(nex_pow(pp.e(), pp.pow() * p.pow()));            
         }
     }
diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h
index 997457578..fee027e8c 100644
--- a/src/math/lp/nex_creator.h
+++ b/src/math/lp/nex_creator.h
@@ -224,7 +224,7 @@ public:
 
     void simplify_children_of_sum(ptr_vector<nex> & children);
     
-    bool eat_scalar_pow(nex_scalar *& r, nex_pow& p);
+    bool eat_scalar_pow(nex_scalar *& r, nex_pow& p, unsigned);
     void simplify_children_of_mul(vector<nex_pow> & children, lt_on_vars lt, std::function<nex_scalar*()> mk_scalar);
 
     bool lt(const nex* a, const nex* b) const;    
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index 824e802da..f88d2cf4f 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -83,8 +83,8 @@ void test_simplify() {
         [](unsigned) { return false; },
         []() { return 1; } // for random
                     );
-    // enable_trace("nla_cn");
-    // enable_trace("nla_cn_details");
+    enable_trace("nla_cn");
+    enable_trace("nla_cn_details");
     //    enable_trace("nla_cn_details_");
     enable_trace("nla_test");
     
@@ -99,6 +99,14 @@ void test_simplify() {
     auto a_plus_bc = r.mk_sum(a, bc);
     auto simp_a_plus_bc = r.simplify(a_plus_bc);
     SASSERT(to_sum(simp_a_plus_bc)->size() > 1);
+    auto three_ab = r.mk_mul(r.mk_scalar(rational(3)), a, b);
+    auto three_ab_square = r.mk_mul();
+    three_ab_square->add_child_in_power(three_ab, 3);
+    TRACE("nla_test", tout << "before simplify " << *three_ab_square << "\n";);
+    three_ab_square = to_mul(r.simplify(three_ab_square));
+    TRACE("nla_test", tout << *three_ab_square << "\n";);
+    nex_scalar * s = to_scalar(three_ab_square->children()[0].e());
+    SASSERT(s->value() == rational(27));
     auto m = r.mk_mul(); m->add_child_in_power(c, 2);
     TRACE("nla_test_", tout << "m = " << *m << "\n";); 
     auto n = r.mk_mul(a);