From 8e21342549cd6143768ecdf49269e169ddf31a4c Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 10 Jul 2019 19:18:24 -0700
Subject: [PATCH] work on horner

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

diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index fc7343591..51ca8e7f7 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -39,9 +39,9 @@ bool horner::row_is_interesting(const T& row) const {
 
 void horner::lemmas_on_expr(nex& e) {
     TRACE("nla_cn", tout << "e = " << e << "\n";);    
+    TRACE("nla_cn_cn", tout << "e = " << e << "\n";);    
     vector<nex*> front;
-    front.push_back(&e);
-    cross_nested_of_expr(e, front);
+    cross_nested_of_expr_on_front_elem(e, &e, front);
 }
 
 nex* pop_back(vector<nex*>& front) {
@@ -50,14 +50,6 @@ nex* pop_back(vector<nex*>& front) {
     return c;
 }
 
-void horner::cross_nested_of_expr(nex& e, vector<nex*>& front) {
-    TRACE("nla_cn", tout << "e = " << e << ", front:"; print_vector_of_ptrs(front, tout) << "\n";);
-    while (!front.empty()) {
-        nex* c = pop_back(front);
-        cross_nested_of_expr_on_front_elem(e, c, front);        
-    }
-}
-
 void horner::cross_nested_of_expr_on_front_elem(nex& e, nex* c, vector<nex*>& front) {
     SASSERT(c->is_sum());
     vector<lpvar> occurences = get_mult_occurences(*c);
@@ -65,7 +57,7 @@ void horner::cross_nested_of_expr_on_front_elem(nex& e, nex* c, vector<nex*>& fr
     
     if (occurences.empty()) {
         if(front.empty()) {
-            TRACE("nla_cn", tout << "got the cn form: e=" << e << "\n";);
+            TRACE("nla_cn_cn", tout << "got the cn form: e=" << e << "\n";);
             SASSERT(!can_be_cross_nested_more(e));
             auto i = interval_of_expr(e);
             m_intervals.check_interval_for_conflict_on_zero(i);
diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h
index a06cede00..b83a371d8 100644
--- a/src/math/lp/horner.h
+++ b/src/math/lp/horner.h
@@ -50,7 +50,6 @@ public:
     void set_interval_for_scalar(intervals::interval&, const rational&);
     std::set<lpvar> get_vars_of_expr(const nex &) const;
     void lemmas_on_expr(nex &);
-    void cross_nested_of_expr(nex& , vector<nex*>& front);
     void cross_nested_of_expr_on_front_elem(nex& , nex*, vector<nex*>& front);
     void cross_nested_of_expr_on_sum_and_var(nex& , nex*, lpvar, vector<nex*>& front);    
     bool can_be_cross_nested_more(const nex&) const;