From 7bac71476222d0234ca16d5e1833dc1972980f60 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 2 Jul 2019 12:52:25 -0700
Subject: [PATCH] save

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/horner.cpp      | 43 +++++++++++++++++++++++++++++--------
 src/math/lp/nla_intervals.h |  4 ++++
 2 files changed, 38 insertions(+), 9 deletions(-)

diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index 5f9ceb5c2..7d3042abf 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -235,9 +235,14 @@ intervals::interval horner::interval_of_expr(const nex& e) {
 template <typename T>
 interv horner::interval_of_mul(const vector<nla_expr<T>>& es) {
     interv a = interval_of_expr(es[0]);    
+    if (m_intervals.is_zero(a)) {
+        TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";);
+            return a;
+    }
     for (unsigned k = 1; k < es.size(); k++) {
         interv b = interval_of_expr(es[k]);
         if (m_intervals.is_zero(b)) {
+            TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, b); tout << "\n";);
             return b;
         }
         interv c;
@@ -245,29 +250,49 @@ interv horner::interval_of_mul(const vector<nla_expr<T>>& es) {
         m_intervals.mul(a, b, c, deps);
         m_intervals.set(a, c);
         m_intervals.add_deps(a, b, deps, a);
-        if (m_intervals.is_zero(a))
-            return a;
     }
+    TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";);
     return a;
 }
 
 template <typename T>
 interv horner::interval_of_sum(const vector<nla_expr<T>>& es) {
-    interv a = interval_of_expr(es[0]);    
-    for (unsigned k = 1; k < es.size(); k++) {
-        interv b = interval_of_expr(es[k]);
-        interv c;
-        m_intervals.add(a, b, c);
-        m_intervals.set(a, c);
+    TRACE("nla_cn", tout << "es[0]= "  << es[0] << "\n";);
+    interv a = interval_of_expr(es[0]);
+    TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";);
+    if (m_intervals.is_inf(a)) {
+        return a;
     }
+        
+    for (unsigned k = 1; k < es.size(); k++) {
+        TRACE("nla_cn", tout << "es[k]= "  << es[k] << "\n";);
+        interv b = interval_of_expr(es[k]);
+        TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";);
+        if (m_intervals.is_inf(b)) {
+            return a;
+        }
+        interv c;
+        interval_deps deps;
+        m_intervals.add(a, b, c, deps);
+        m_intervals.set(a, c);
+        m_intervals.add_deps(a, b, deps, a);
+        TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";);
+        if (m_intervals.is_inf(a)) {
+            return a;
+        }
+    }
+    TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";);
     return a;
 }
 // sets the dependencies also
 void horner::set_var_interval(lpvar v, interv& b) {
     m_intervals.set_var_interval_with_deps(v, b);
+    TRACE("nla_cn", tout << "v = "; print_var(v, tout); tout << "\n";);
+    
 }
 
-void horner::check_interval_for_conflict(const intervals::interval&) {
+void horner::check_interval_for_conflict(const intervals::interval& i) {
+    TRACE("nla_cn", tout << "interval = "; m_intervals.display(tout, i); );
     SASSERT(false);
 }
 }
diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h
index 086b5794e..9f37026f3 100644
--- a/src/math/lp/nla_intervals.h
+++ b/src/math/lp/nla_intervals.h
@@ -96,9 +96,11 @@ class intervals : common {
         bool upper_is_open(interval const & a) const { return a.m_upper_open; }
         bool lower_is_inf(interval const & a) const { return a.m_lower_inf; }
         bool upper_is_inf(interval const & a) const { return a.m_upper_inf; }
+        bool is_inf(interval const & a) const { return upper_is_inf(a) && lower_is_inf(a); }
         bool is_zero(interval const & a) const {
             return unsynch_mpq_manager::is_zero(a.m_lower)
                 && unsynch_mpq_manager::is_zero(a.m_upper); }
+
             
         // Setters
         void set_lower(interval & a, mpq const & n) const { m_manager.set(a.m_lower, n); }
@@ -178,11 +180,13 @@ public:
     bool is_zero(const interval& a) const { return m_config.is_zero(a); }
     void mul(const interval& a, const interval& b, interval& c) { m_imanager.mul(a, b, c); }
     void add(const interval& a, const interval& b, interval& c) { m_imanager.add(a, b, c); }
+    void add(const interval& a, const interval& b, interval& c, interval_deps& deps) { m_imanager.add(a, b, c, deps); }
     void set(interval& a, const interval& b) { m_imanager.set(a, b); }
     void mul(const interval& a, const interval& b, interval& c, interval_deps& deps) { m_imanager.mul(a, b, c, deps); }
     void add_deps(interval const& a, interval const& b, interval_deps const& deps, interval& i) const {
         m_config.add_deps(a, b, deps, i);
     }
     void set_var_interval_with_deps(lpvar, interval &);
+    bool is_inf(const interval& i) const { return m_config.is_inf(i); }
 }; // end of intervals
 } // end of namespace nla