From 4daa841116f5543ff2617a27ea01adccf380fa09 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 15 Oct 2019 10:24:50 -0700
Subject: [PATCH] calculate power of intervals with depenencies

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

diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index 75ca015f6..c0d54301b 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -148,8 +148,10 @@ interv horner::power_with_deps(const interv& a, unsigned n) {
     interv b;
     interval_deps_combine_rule combine_rule;
     m_intervals.power(a, n, b, combine_rule);
+    m_intervals.combine_deps(a, combine_rule, b);
     TRACE("nla_horner_details", tout << "power of "; m_intervals.display(tout, a) << " = ";
-          m_intervals.display(tout, b) << "\n";);
+          m_intervals.display(tout, b) << "\n"; );
+    
     return b; 
 }
 
diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h
index a72de66ee..ca72734c5 100644
--- a/src/math/lp/nla_intervals.h
+++ b/src/math/lp/nla_intervals.h
@@ -60,6 +60,12 @@ class intervals : common {
             i.m_upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_upper_combine);
         }
 
+        void add_deps(interval const& a,
+                      interval_deps_combine_rule const& deps, interval& i) const {
+            i.m_lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, deps.m_lower_combine);
+            i.m_upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, deps.m_upper_combine);
+        }
+
         
         // Should be NOOPs for precise mpq types.
         // For imprecise types (e.g., floats) it should set the rounding mode.
@@ -114,6 +120,18 @@ class intervals : common {
             }
             return dep;
         }
+
+        ci_dependency* mk_dependency(interval const& a, deps_combine_rule bd) const {
+            ci_dependency* dep = nullptr;
+            if (dep_in_lower1(bd)) {
+                dep = m_dep_manager.mk_join(dep, a.m_lower_dep);
+            }
+            if (dep_in_upper1(bd)) {
+                dep = m_dep_manager.mk_join(dep, a.m_upper_dep);
+            }
+            return dep;
+        }
+
     };
 
     region                              m_alloc;
@@ -197,6 +215,11 @@ public:
         m_config.add_deps(a, b, deps, i);
     }
 
+    void combine_deps(interval const& a, interval_deps_combine_rule const& deps, interval& i) const {
+        SASSERT(&a != &i);
+        m_config.add_deps(a, deps, i);
+    }
+
     void power(interval const & a, unsigned n, interval & b, interval_deps_combine_rule & b_deps) {
         m_imanager.power(a, n, b, b_deps);
     }