From 63748206fea9d9d18380354790a7c4f7dad18b62 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 19 Aug 2019 10:53:40 -0700
Subject: [PATCH] add test routines to nla_expr

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/cross_nested.h | 35 +++++++++++++++++++++++++++++++++++
 src/test/lp/lp.cpp         |  6 ++++--
 2 files changed, 39 insertions(+), 2 deletions(-)

diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h
index 2fa1dd41d..a5fa4021b 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -556,6 +556,41 @@ public:
     }
 
     bool done() const { return m_done; }
+#if Z3DEBUG
+    nex *clone (nex * a) {
+        switch (a->type()) {
+        case expr_type::VAR: {
+            auto v = to_var(a);
+            return mk_var(v->var());
+        }
+            
+        case expr_type::SCALAR: {
+            auto v = to_scalar(a);
+            return mk_scalar(v->value());
+        }
+        case expr_type::MUL: {
+            auto m = to_mul(a);
+            auto r = mk_mul();
+            for (nex * e : m->children()) {
+                r->add_child(clone(e));
+            }
+            return r;
+        }
+        case expr_type::SUM: {
+            auto m = to_sum(a);
+            auto r = mk_sum();
+            for (nex * e : m->children()) {
+                r->add_child(clone(e));
+            }
+            return r;
+        }
+        default:
+            SASSERT(false);
+            break;
+        }
+        return nullptr;
+    }
+    #endif
     
 };
 }
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index d73c59a04..f0b9ef763 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -93,7 +93,7 @@ void test_cn() {
     nex_mul* bcg = cn.mk_mul(b, c, g);
     bcg->add_child(min_1);
     nex_sum* t = cn.mk_sum(bcd, bcg);
-    //    test_cn_on_expr(t, cn);
+    test_cn_on_expr(t, cn);
     nex* aad = cn.mk_mul(a, a, d);
     nex* abcd = cn.mk_mul(a, b, c, d);
     nex* aaccd = cn.mk_mul(a, a, c, c, d);
@@ -101,7 +101,9 @@ void test_cn() {
     nex* eae = cn.mk_mul(e, a, e);
     nex* eac = cn.mk_mul(e, a, c);
     nex* ed = cn.mk_mul(e, d);
-    nex* _6aad = cn.mk_mul(cn.mk_scalar(rational(6)), a, a, d); 
+    nex* _6aad = cn.mk_mul(cn.mk_scalar(rational(6)), a, a, d);
+    nex * clone = cn.clone(cn.mk_sum(_6aad, abcd, aaccd, add, eae, eac, ed));
+    TRACE("nla_cn", tout << "clone = " << *clone << "\n";);
     //    test_cn_on_expr(cn.mk_sum(aad,  abcd, aaccd, add, eae, eac, ed), cn);
     test_cn_on_expr(cn.mk_sum(_6aad, abcd, aaccd, add, eae, eac, ed), cn);
     // TRACE("nla_cn", tout << "done\n";);