From e9e1fb2f37c87734153e32d249fba3123c5b709d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 25 Jul 2023 10:06:11 -0700
Subject: [PATCH] separate out functions that call set_var_interval1/2 into
 functions for linker

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/nla_grobner.cpp | 24 ++++++++++++++----------
 src/math/lp/nla_grobner.h   |  1 +
 2 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index efe7c0fce..832f4f12c 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -275,16 +275,7 @@ namespace nla {
             return false;
 
         eval.var2intervals() = [&](lpvar j, bool deps, scoped_ptr_vector<scoped_dep_interval>& intervals) {
-            verbose_stream() << "get-intervals\n";
-            scoped_ptr<scoped_dep_interval> a = alloc(scoped_dep_interval, di);
-            scoped_ptr<scoped_dep_interval> b = alloc(scoped_dep_interval, di);
-            if (deps) c().m_intervals.set_var_interval1<dd::w_dep::with_deps>(j, *a);
-            else c().m_intervals.set_var_interval1<dd::w_dep::without_deps>(j, *a);
-            intervals.push_back(a.detach());
-            if (deps && c().m_intervals.set_var_interval2<dd::w_dep::with_deps>(j, *b))
-                intervals.push_back(b.detach());
-            if (!deps && c().m_intervals.set_var_interval2<dd::w_dep::without_deps>(j, *b))
-                intervals.push_back(b.detach());
+            var2intervals(j, deps, intervals);
         };
         // TODO - relax bound dependencies to weakest that admit within interval -mx, mx.
         eval.explain(lo, i, i_wd);
@@ -325,6 +316,19 @@ namespace nla {
         return true;
     }
 
+    void grobner::var2intervals(lpvar j, bool deps, scoped_ptr_vector<scoped_dep_interval>& intervals) {
+        auto& di = c().m_intervals.get_dep_intervals();
+        scoped_ptr<scoped_dep_interval> a = alloc(scoped_dep_interval, di);
+        scoped_ptr<scoped_dep_interval> b = alloc(scoped_dep_interval, di);
+        if (deps) c().m_intervals.set_var_interval1<dd::w_dep::with_deps>(j, *a);
+        else c().m_intervals.set_var_interval1<dd::w_dep::without_deps>(j, *a);
+        intervals.push_back(a.detach());
+        if (deps && c().m_intervals.set_var_interval2<dd::w_dep::with_deps>(j, *b))
+            intervals.push_back(b.detach());
+        if (!deps && c().m_intervals.set_var_interval2<dd::w_dep::without_deps>(j, *b))
+            intervals.push_back(b.detach());
+    }
+
 
     void grobner::add_dependencies(new_lemma& lemma, const dd::solver::equation& eq) {
         lp::explanation ex;
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index d0c4e51b1..ad92d6f53 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -46,6 +46,7 @@ namespace nla {
 
         bool propagate_gcd();
         bool propagate_gcd(const dd::solver::equation& eq);
+
         
         void add_dependencies(new_lemma& lemma, const dd::solver::equation& eq);