From b6a99d515bf007ba987133c712393538653e818c Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 12 Jul 2019 14:20:21 -0700
Subject: [PATCH] work on horner form

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

diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index df875bf48..f44397b9a 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -189,5 +189,4 @@ void horner::set_var_interval(lpvar v, interv& b) {
     
 }
 }
- 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 0a1e1eb77..f4b2a30eb 100644
--- a/src/math/lp/horner.h
+++ b/src/math/lp/horner.h
@@ -44,6 +44,7 @@ public:
     intervals::interval interval_of_sum(const vector<nex>&);
     intervals::interval interval_of_mul(const vector<nex>&);
     void set_interval_for_scalar(intervals::interval&, const rational&);
+    void set_var_interval(lpvar j, intervals::interval&);
     std::set<lpvar> get_vars_of_expr(const nex &) const;
     void lemmas_on_expr(nex &);
 }; // end of horner
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index 07a997351..840317496 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -56,6 +56,7 @@
 #include "math/lp/lp_bound_propagator.h"
 #include "math/lp/nla_solver.h"
 #include "math/lp/horner.h"
+#include "math/lp/cross_nested.h"
 namespace nla {
 void test_order_lemma();
 void test_monotone_lemma();
@@ -73,9 +74,11 @@ void test_cn() {
     nex a = nex::var(0), b = nex::var(1), c = nex::var(2), d = nex::var(3), e = nex::var(4);
     nex t = a*a*d + a*b*c*d + a*c*c*d + e*a*e + e*a*c + e*d;
     TRACE("nla_cn", tout << "t=" << t << '\n';);
+    cross_nested cn(t, [](const nex& n) { std::cout << n << "\n"; } );
+    cn.run();
 }
 
-}
+} // end of namespace nla
 
 namespace lp {
 unsigned seed = 1;