From 1d217595c80cc89c556a18421277f18c62fdd809 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 24 Dec 2019 18:08:03 -0800
Subject: [PATCH] add pdd_interval to evaluate intervals of pdd expressions

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/dd/pdd_interval.h        | 72 +++++++++++++++++++++++++++++++
 src/math/interval/dep_intervals.h |  1 -
 src/math/interval/interval.h      |  3 ++
 src/test/pdd.cpp                  |  1 +
 4 files changed, 76 insertions(+), 1 deletion(-)
 create mode 100644 src/math/dd/pdd_interval.h

diff --git a/src/math/dd/pdd_interval.h b/src/math/dd/pdd_interval.h
new file mode 100644
index 000000000..9849b3f48
--- /dev/null
+++ b/src/math/dd/pdd_interval.h
@@ -0,0 +1,72 @@
+/*++
+Copyright (c) 2019 Microsoft Corporation
+
+Module Name:
+
+    dd_pdd.cpp
+
+Abstract:
+
+    Poly DD package 
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2019-12-24
+    Lev Nachmanson (levnach) 2019-12-24
+
+Revision History:
+
+--*/
+#include "math/dd/dd_pdd.h"
+#include "math/interval/dep_intervals.h"
+
+namespace dd {
+typedef dep_intervals::interval interval;
+typedef dep_intervals::with_deps_t w_dep;
+// calculates the interval of a pdd expression based on the given intervals of the variables
+class pdd_interval {
+    pdd_manager&  m;
+    dep_intervals m_dep_intervals;
+    std::function<interval (unsigned, bool)> m_var2interval;
+    
+public:
+    
+    pdd_interval(pdd_manager& m, reslimit& lim): m(m), m_dep_intervals(lim) {}
+    
+    std::function<interval (unsigned, bool)>& var2interval() { return m_var2interval; } // setter
+    const std::function<interval (unsigned, bool)>& var2interval() const { return m_var2interval; } // getter
+
+    template <w_dep wd>
+    interval get_interval(pdd const& p) {
+        interval k;
+        if (p.is_val()) {
+            m_dep_intervals.set_interval_for_scalar(k, p.val());
+            return k;
+        }
+        bool deps = (wd == w_dep::with_deps);
+        interval a = m_var2interval(p.var(), deps);
+        interval hi = get_interval<wd>(p.hi());
+        interval la = get_interval<wd>(p.lo());
+        interval t;
+        interval ret;
+        if (deps) {
+            interval_deps_combine_rule combine_rule;
+            m_dep_intervals.add(hi, a, t, combine_rule);
+            m_dep_intervals.combine_deps(hi, a, combine_rule, t); 
+            combine_rule.reset();
+            m_dep_intervals.add(t, la, ret, combine_rule);
+            m_dep_intervals.combine_deps(t, la, combine_rule, ret);
+            return ret;
+        } else {
+            m_dep_intervals.mul(hi, a, t);
+            m_dep_intervals.add(t, la, ret);
+            return ret;                
+        }
+    }
+
+    bool separated_from_zero(pdd const& p, u_dependency*& dep) {
+        return m_dep_intervals.check_interval_for_conflict_on_zero((*this)(p), dep);
+    }
+
+};
+}
diff --git a/src/math/interval/dep_intervals.h b/src/math/interval/dep_intervals.h
index 4b1357656..d0c0343be 100644
--- a/src/math/interval/dep_intervals.h
+++ b/src/math/interval/dep_intervals.h
@@ -332,5 +332,4 @@ public:
 
         copy_upper_bound<wd>(b, i);
     }
-
 };
diff --git a/src/math/interval/interval.h b/src/math/interval/interval.h
index 0b11569a4..566c852b8 100644
--- a/src/math/interval/interval.h
+++ b/src/math/interval/interval.h
@@ -107,6 +107,9 @@ inline deps_combine_rule dep1_to_dep2(deps_combine_rule d) {
 struct interval_deps_combine_rule {
     deps_combine_rule m_lower_combine;
     deps_combine_rule m_upper_combine;
+    void reset() {
+        m_lower_combine = m_upper_combine = 0;
+    }
 };
 
 template<typename C>
diff --git a/src/test/pdd.cpp b/src/test/pdd.cpp
index 4620bff7b..0efb4cae8 100644
--- a/src/test/pdd.cpp
+++ b/src/test/pdd.cpp
@@ -1,5 +1,6 @@
 #include "math/dd/dd_pdd.h"
 #include "math/dd/pdd_eval.h"
+#include "math/dd/pdd_interval.h"
 
 namespace dd {
 static void test1() {