From 8596fb2ae6310304b3cf6f46e6cf956630ce6f6b Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 2 Jan 2020 12:21:41 -0800
Subject: [PATCH] cleaner code in add row to gb

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nla_core.cpp | 19 +++++++++----------
 src/math/lp/nla_core.h   |  1 +
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index adcd47b8c..fa6f7c18a 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1536,14 +1536,17 @@ void core::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lp
     }            
 }
 
+const rational& core::val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep) {
+    unsigned lc, uc;
+    m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
+    dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(lc));
+    dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(uc));
+    return m_lar_solver.column_lower_bound(j).x;
+}
 
 dd::pdd core::pdd_expr(const rational& c, lpvar j, u_dependency*& dep) {
     if (var_is_fixed(j)) {
-        unsigned lc, uc;
-        m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
-        dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(lc));
-        dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(uc));
-        return m_pdd_manager.mk_val(c *  m_lar_solver.column_lower_bound(j).x);
+        return m_pdd_manager.mk_val(c * val_of_fixed_var_with_deps(j, dep));
     }
 
     if (!is_monic_var(j))
@@ -1554,11 +1557,7 @@ dd::pdd core::pdd_expr(const rational& c, lpvar j, u_dependency*& dep) {
     const monic& m = emons()[j];
     for (lpvar k : m.vars()) {
         if (var_is_fixed(k)) {
-            unsigned lc, uc;
-            r *= m_pdd_manager.mk_val(m_lar_solver.column_lower_bound(k).x);           
-            m_lar_solver.get_bound_constraint_witnesses_for_column(k, lc, uc);
-            dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(lc));
-            dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(uc));
+            r *= m_pdd_manager.mk_val(val_of_fixed_var_with_deps(k, dep));
         } else {
             r *= m_pdd_manager.mk_var(k);
         }
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index d905415b1..5cf3924f6 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -409,6 +409,7 @@ public:
     unsigned get_var_weight(lpvar) const;
     void add_row_to_pdd_grobner(const vector<lp::row_cell<rational>> & row);    
     bool check_pdd_eq(const dd::grobner::equation*);
+    const rational& val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep);
     dd::pdd pdd_expr(const rational& c, lpvar j, u_dependency*&);
     void set_level2var_for_pdd_grobner();
 };  // end of core