From 2d5595eddc3a91b8a38f3fdd66cb43a02f64f3ce Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Sun, 9 Jun 2019 13:39:26 -0700
Subject: [PATCH] add trace statements

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nla_intervals.cpp | 11 ++++++++++-
 src/math/lp/nla_intervals.h   |  1 +
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
index 657c4064d..6f1ae1b41 100755
--- a/src/math/lp/nla_intervals.cpp
+++ b/src/math/lp/nla_intervals.cpp
@@ -239,13 +239,22 @@ lp::lar_solver& intervals::ls() { return m_core->m_lar_solver; }
 
 const lp::lar_solver& intervals::ls() const { return m_core->m_lar_solver; }
 
+std::ostream& intervals::print_explanations(const svector<lp::constraint_index> &expl , std::ostream& out) const {
+    out << "interv expl: ";
+    for (auto ci : expl)
+        m_core->m_lar_solver.print_constraint(ci, out) << "\n";
+    return out;
+}
+
 void intervals::get_explanation_of_upper_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const {
     interval a = mul_signs_with_deps(m_core->emons()[j].vars());
-    m_dep_manager.linearize(a.m_upper_dep, expl);    
+    m_dep_manager.linearize(a.m_upper_dep, expl);
+    TRACE("nla_intervals", print_explanations(expl, tout););
 }
 void intervals::get_explanation_of_lower_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const{
     interval a = mul_signs_with_deps(m_core->emons()[j].vars());
     m_dep_manager.linearize(a.m_lower_dep, expl);    
+    TRACE("nla_intervals", print_explanations(expl, tout););
     //    return m_intervals.get_explanation_of_lower_bound_for_monomial(j, expl ) 
 }
 }
diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h
index 0766181d8..a4a33241d 100755
--- a/src/math/lp/nla_intervals.h
+++ b/src/math/lp/nla_intervals.h
@@ -179,5 +179,6 @@ namespace nla {
         interval mul_signs_with_deps(const svector<lpvar>&) const;
         void get_explanation_of_upper_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const;
         void get_explanation_of_lower_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const;
+        std::ostream& print_explanations(const svector<lp::constraint_index> &, std::ostream&) const;
     };
 } // end of namespace nla