From a7158772adbcb43c3748b6d357e05097e5fcc237 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 13 Mar 2020 15:12:46 -0700
Subject: [PATCH] move to scoped intervals for memory management

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/dd/pdd_interval.h        | 26 ++++++++++++--------------
 src/math/interval/dep_intervals.h |  4 ++++
 src/math/lp/nla_core.cpp          | 10 +++++-----
 3 files changed, 21 insertions(+), 19 deletions(-)

diff --git a/src/math/dd/pdd_interval.h b/src/math/dd/pdd_interval.h
index fd796b6a1..2972e0086 100644
--- a/src/math/dd/pdd_interval.h
+++ b/src/math/dd/pdd_interval.h
@@ -31,35 +31,33 @@ class pdd_interval {
 public:
     
     pdd_interval(reslimit& lim): m_dep_intervals(lim) {}
-    
+
+    dep_intervals& m() { return m_dep_intervals; }
+
     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;
+    void get_interval(pdd const& p, scoped_dep_interval& ret) {
         if (p.is_val()) {
-            m_dep_intervals.set_interval_for_scalar(k, p.val());
-            return k;
+            m_dep_intervals.set_interval_for_scalar(ret.get(), p.val());
+            return;
         }
         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;
+        scoped_dep_interval hi(m()), lo(m()), t(m());
+        get_interval<wd>(p.hi(), hi);
+        get_interval<wd>(p.lo(), lo);
         if (deps) {
             interval_deps_combine_rule combine_rule;
             m_dep_intervals.mul(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;
+            m_dep_intervals.add(t, lo, ret, combine_rule);
+            m_dep_intervals.combine_deps(t, lo, combine_rule, ret);
         } else {
             m_dep_intervals.mul(hi, a, t);
-            m_dep_intervals.add(t, la, ret);
-            return ret;                
+            m_dep_intervals.add(t, lo, ret);
         }
     }
 	// f meant to be called when the separation happens
diff --git a/src/math/interval/dep_intervals.h b/src/math/interval/dep_intervals.h
index 34bcad9e8..973cadb4b 100644
--- a/src/math/interval/dep_intervals.h
+++ b/src/math/interval/dep_intervals.h
@@ -296,6 +296,8 @@ public:
     }
 
     void reset() { m_dep_manager.reset(); }
+
+    void del(interval& i) { m_imanager.del(i); }
     
     template <enum with_deps_t wd> interval intersect(const interval& a, const interval& b) const {
         interval i;
@@ -363,3 +365,5 @@ public:
         copy_upper_bound<wd>(b, i);
     }
 };
+
+typedef _scoped_interval<dep_intervals> scoped_dep_interval;
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 6f4a4993c..fdd019567 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1494,16 +1494,16 @@ bool core::check_pdd_eq(const dd::solver::equation* e) {
             else m_intervals.set_var_interval<dd::w_dep::without_deps>(j, a);
             return a;
         };
-    auto i = eval.get_interval<dd::w_dep::without_deps>(e->poly());    
-    dep_intervals di(m_reslim);
-    if (!di.separated_from_zero(i))
+    scoped_dep_interval i(eval.m()), i_wd(eval.m());
+    eval.get_interval<dd::w_dep::without_deps>(e->poly(), i);    
+    if (!eval.m().separated_from_zero(i))
         return false;
-    auto i_wd = eval.get_interval<dd::w_dep::with_deps>(e->poly());  
+    eval.get_interval<dd::w_dep::with_deps>(e->poly(), i_wd);  
     std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
                                                          add_empty_lemma();
                                                          current_expl().add(e);
                                                      };
-    if (di.check_interval_for_conflict_on_zero(i_wd, e->dep(), f)) {
+    if (eval.m().check_interval_for_conflict_on_zero(i_wd, e->dep(), f)) {
         lp_settings().stats().m_grobner_conflicts++;
         return true;
     }