From 4e59976c2f4cef049ee5af4b32f87174fa590010 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 19 Aug 2019 14:09:41 -0700
Subject: [PATCH] make sure that the returned cross nested form is equal to the
 original

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/cross_nested.h | 22 +++++++++++++++++++---
 src/math/lp/nex.h          |  9 ++++++++-
 2 files changed, 27 insertions(+), 4 deletions(-)

diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h
index 9f7da6b3c..babb455dd 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -43,6 +43,9 @@ class cross_nested {
     std::unordered_map<lpvar, unsigned>   m_powers;
     ptr_vector<nex> m_allocated;
     ptr_vector<nex> m_b_split_vec;
+#ifdef Z3DEBUG
+    nex* m_e_clone;
+#endif
 public:
     cross_nested(std::function<bool (const nex*)> call_on_result,
                  std::function<bool (unsigned)> var_is_fixed):
@@ -53,7 +56,10 @@ public:
 
     void run(nex *e) {
         m_e = e;
-        
+#ifdef Z3DEBUG
+        m_e_clone = clone(m_e);
+        m_e_clone = normalize(m_e_clone);
+#endif
         vector<nex**> front;
         explore_expr_on_front_elem(&m_e, front);
     }
@@ -337,6 +343,13 @@ public:
             if(front.empty()) {
                 TRACE("nla_cn", tout << "got the cn form: =" << *m_e << "\n";);
                 m_done = m_call_on_result(m_e);
+#ifdef Z3DEBUG
+                nex *ce = clone(m_e);
+                TRACE("nla_cn", tout << "ce = " << *ce <<  "\n";);
+                nex *n = normalize(ce);
+                TRACE("nla_cn", tout << "n = " << *n << "\nm_e_clone=" << * m_e_clone << "\n";);
+                SASSERT(*n == *m_e_clone);
+#endif
             } else {
                 nex** f = pop_front(front);
                 explore_expr_on_front_elem(f, front);     
@@ -619,7 +632,9 @@ public:
                 if ((int)j != sum_j)
                     b->add_child(a->children()[j]);
             }
-        }        
+            b->simplify();
+        }
+        TRACE("nla_cn", tout << *r << "\n";); 
         return normalize_sum(r);
     }
 
@@ -635,8 +650,9 @@ public:
             r = normalize_sum(to_sum(a));
         }
         r->sort();
+        return r;
     }
-    #endif
+#endif
     
 };
 }
diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h
index 7ee473687..67da8168f 100644
--- a/src/math/lp/nex.h
+++ b/src/math/lp/nex.h
@@ -82,6 +82,9 @@ public:
 };
 #if Z3DEBUG
 bool operator<(const nex& a , const nex& b);
+inline bool operator ==(const nex& a , const nex& b) {
+    return ! (a < b || b < a) ;
+}
 #endif
 std::ostream& operator<<(std::ostream& out, const nex&);
 
@@ -133,6 +136,8 @@ static void promote_children_by_type(ptr_vector<nex> * children, expr_type t) {
             }
         }
     }
+
+    children->shrink(children->size() - to_promote.size());
     
     for (nex *e : to_promote) {
         for (nex *ee : *(e->children_ptr())) {
@@ -218,7 +223,9 @@ public:
     }
     
     void simplify() {
+        TRACE("nla_cn_details", tout << *this << "\n";);
         promote_children_by_type(&m_children, expr_type::MUL);
+        TRACE("nla_cn_details", tout << *this << "\n";);
     }
     #ifdef Z3DEBUG
     virtual void sort() {
@@ -377,7 +384,7 @@ inline bool operator<(const nex& a , const nex& b) {
         return to_mul(&a)->children() < to_mul(&b)->children();
     }
     case expr_type::SUM: {
-        return to_mul(&a)->children() < to_mul(&b)->children();
+        return to_sum(&a)->children() < to_sum(&b)->children();
     }
     default:
         SASSERT(false);