From 1915812f84cf41a5f232eedf2a695a54d055aa88 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 29 Jul 2019 20:32:00 -0700
Subject: [PATCH] add a test for intervals

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

diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
index 9a59c016b..e9d13bbbf 100644
--- a/src/math/lp/nla_intervals.cpp
+++ b/src/math/lp/nla_intervals.cpp
@@ -4,6 +4,31 @@
 #include "util/mpq.h"
 
 namespace nla {
+void intervals::test_inf() {
+    interval a; // [1, inf)
+    m_config.set_lower(a, rational(1));
+    m_config.set_lower_is_open(a, false);
+    m_config.set_upper_is_inf(a, true);
+    a.m_lower_dep = mk_dep(1);
+
+    interval b; // [-1,-1]
+    m_config.set_lower(b, rational(-1));
+    m_config.set_lower_is_open(b, false);
+    m_config.set_upper(b, rational(-1));
+    m_config.set_upper_is_open(b, false);
+ 
+    b.m_lower_dep = mk_dep(2);
+    b.m_upper_dep = mk_dep(4);
+    
+    interval_deps_combine_rule comb_rule;
+    interval c;
+    mul(a, b, c, comb_rule);
+    TRACE("nla_horner_test", tout << "c before combine_deps() "; display(tout, c););
+    combine_deps(a, b, comb_rule, c);
+    SASSERT(lower_is_inf(c));
+    SASSERT(!dep_in_upper1(comb_rule.m_lower_combine));
+
+}
 void intervals::set_var_interval_with_deps(lpvar v, interval& b) {
     lp::constraint_index ci;
     rational val;
diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h
index 5581bdce1..0563a29b1 100644
--- a/src/math/lp/nla_intervals.h
+++ b/src/math/lp/nla_intervals.h
@@ -159,7 +159,10 @@ public:
         m_dep_manager(m_val_manager, m_alloc),
         m_config(m_num_manager, m_dep_manager),
         m_imanager(lim, im_config(m_num_manager, m_dep_manager))
-    {}
+    {
+        test_inf();
+    }
+    void test_inf();
     interval mul(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;