From 73e63e1ad9e2f079987e7a934ddf40d6ca156072 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 17 Jun 2019 17:06:32 -0700
Subject: [PATCH] fix a bug in nla_intervals

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nla_intervals.cpp | 21 +++++++++++++++++++--
 src/math/lp/nla_intervals.h   |  6 ++++--
 src/smt/smt_context_pp.cpp    |  1 +
 3 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
index 5a519c9b1..52a3cd375 100644
--- a/src/math/lp/nla_intervals.cpp
+++ b/src/math/lp/nla_intervals.cpp
@@ -37,7 +37,8 @@ void intervals::get_lemma_for_zero_interval(monomial const& m) {
     interval signs_a = mul_signs_with_deps(m.vars());
     add_empty_lemma();
     svector<lp::constraint_index> expl;
-    m_dep_manager.linearize(signs_a.m_lower_dep, expl); 
+    m_dep_manager.linearize(signs_a.m_lower_dep, expl);
+    TRACE("nla_solver", print_vector(expl, tout) << "\n";);
     _().current_expl().add_expl(expl);
     mk_ineq(m.var(), llc::EQ);
     TRACE("nla_solver", _().print_lemma(tout); );
@@ -90,7 +91,7 @@ bool intervals::get_lemma_for_upper(const monomial& m, const interval& a) {
 bool intervals::get_lemma(monomial const& m) {
     interval  b, c, d;
     interval a = mul(m.vars());
-    if (m_config.is_zero(a)) {
+    if (m_imanager.is_zero(a)) {
         get_lemma_for_zero_interval(m);
         return true;
     }
@@ -206,6 +207,22 @@ lp::impq intervals::get_lower_bound_of_monomial(lpvar j) const {
     return r;
 }
 
+std::ostream& intervals::display(std::ostream& out, const interval& i) const {
+    if (m_imanager.lower_is_inf(i)) {
+        out << "(-oo";
+    } else {
+        out << (m_imanager.lower_is_open(i)? "(":"[") << rational(m_imanager.lower(i));        
+    }
+    out << ",";
+    if (m_imanager.upper_is_inf(i)) {
+        out << "oo)";
+    } else {
+        out << rational(m_imanager.upper(i)) << (m_imanager.lower_is_open(i)? ")":"]");         
+    }
+    return out;
+}
+
+
 intervals::interval intervals::mul(const svector<lpvar>& vars) const {
     interval a;
     m_imanager.set(a, mpq(1));
diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h
index 9012212ba..a720183f9 100644
--- a/src/math/lp/nla_intervals.h
+++ b/src/math/lp/nla_intervals.h
@@ -145,8 +145,9 @@ class intervals : common {
     mutable interval_manager<im_config> m_imanager;
     region                      m_region;
 
+public:
     typedef interval_manager<im_config>::interval interval;
-
+private:
     void set_var_interval(lpvar v, interval & b) const;
 
     void set_var_interval_signs(lpvar v, interval & b) const;
@@ -184,6 +185,7 @@ public:
     void push();
     void pop(unsigned k);
     void init();
-    
+    std::ostream& display(std::ostream& out, const intervals::interval& i) const;
 };
+
 } // end of namespace nla
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index 02ad786dd..077051e95 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -493,6 +493,7 @@ namespace smt {
         TRACE("lemma", tout << strm.str() << "\n";);
         display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic);
         out.close();
+
         return m_lemma_id;
     }