create scalars for fixed variables in rows for grobner

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/lp/nla_common.cpp

@@ -123,8 +123,19 @@ unsigned common::random() {
 }
 
 // creates a nex expression for the coeff and var, 
-nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) {
+nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn,
+                     u_dependency*& dep,
+                     u_dependency_manager* dep_manager) {
     SASSERT(!coeff.is_zero());
+    unsigned lc, uc;
+    if (c().var_is_fixed(j)) {
+        if (dep_manager) {
+            c().m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
+            dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(lc));
+            dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(uc));
+        }
+        return cn.mk_scalar(c().m_lar_solver.column_lower_bound(j).x);
+    }
     if (!c().is_monic_var(j)) {
         c().insert_to_active_var_set(j);
         return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(j));
@@ -133,10 +144,19 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) {
     nex_creator::mul_factory mf(cn);
     mf *= coeff;
     for (lpvar k : m.vars()) {
+        if (c().var_is_fixed(j)) {
+            if (dep_manager) {
+                c().m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
+                dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(lc));
+                dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(uc));
+            }
+            mf *= c().m_lar_solver.column_lower_bound(j).x;
+        } else {
             c().insert_to_active_var_set(k);
             mf *= cn.mk_var(k);
             CTRACE("nla_grobner", c().is_monic_var(k), c().print_var(k, tout) << "\n";);
         }
+    }
     nex* e = mf.mk();
     TRACE("nla_grobner", tout << *e;);
     return e;
@@ -154,7 +174,7 @@ template <typename T> u_dependency* common::create_sum_from_row(const T& row,
     SASSERT(row.size() > 1);
     sum.reset();
     for (const auto &p : row) {
-        nex* e = nexvar(p.coeff(), p.var(), cn);
+        nex* e = nexvar(p.coeff(), p.var(), cn, dep, dep_manager);
         if (!e)
             continue;
         unsigned lc, uc;

src/math/lp/nla_common.h

@@ -116,7 +116,7 @@ struct common {
         typedef lp::constraint_index value;
     };
         
-    nex* nexvar(const rational& coeff, lpvar j, nex_creator&);
+    nex* nexvar(const rational& coeff, lpvar j, nex_creator&, u_dependency*&, u_dependency_manager*);
     template <typename T>
     u_dependency* create_sum_from_row(const T&, nex_creator&, nex_creator::sum_factory&, u_dependency_manager*);
     template <typename T>

src/math/lp/nla_core.cpp

@@ -1482,7 +1482,17 @@ void core::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lp
 }
 
 
-dd::pdd core::pdd_expr(const rational& c, lpvar j) {
+dd::pdd core::pdd_expr(const rational& c, lpvar j, u_dependency*& dep) {
+    unsigned lc, uc;
+    m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
+    if (lc != null_lpvar)
+        dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(lc));
+    if (uc != null_lpvar) 
+        dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(uc));
+    if (var_is_fixed(j)) {
+        return m_pdd_manager.mk_val(c *  m_lar_solver.column_lower_bound(j).x);
+    }
+
     if (!is_monic_var(j))
         return c * m_pdd_manager.mk_var(j);
 
@@ -1490,8 +1500,15 @@ dd::pdd core::pdd_expr(const rational& c, lpvar j) {
     dd::pdd r = m_pdd_manager.mk_val(c);
     const monic& m = emons()[j];
     for (lpvar k : m.vars()) {
+        if (var_is_fixed(k)) {
+            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));
+        } else {
             r *= m_pdd_manager.mk_var(k);
         }
+    }
     return r;
 }
 
@@ -1499,14 +1516,7 @@ void core::add_row_to_pdd_grobner(const vector<lp::row_cell<rational>> & row) {
     u_dependency *dep = nullptr;
     dd::pdd sum = m_pdd_manager.mk_val(rational(0));
     for (const auto &p : row) {
-        dd::pdd e = pdd_expr(p.coeff(), p.var());
+        sum  += pdd_expr(p.coeff(), p.var(), dep);
-        sum  +=  e; 
-        unsigned lc, uc;
-        m_lar_solver.get_bound_constraint_witnesses_for_column(p.var(), lc, uc);
-        if (lc != null_lpvar)
-            dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(lc));
-        if (uc != null_lpvar) 
-            dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(uc));                    
     }
     m_pdd_grobner.add(sum, dep);    
 }

src/math/lp/nla_core.h

@@ -402,7 +402,7 @@ public:
     unsigned get_var_weight(lpvar) const;
     void add_row_to_pdd_grobner(const vector<lp::row_cell<rational>> & row);    
     void check_pdd_eq(const dd::grobner::equation*);
-    dd::pdd pdd_expr(const rational& c, lpvar j);
+    dd::pdd pdd_expr(const rational& c, lpvar j, u_dependency*&);
     void set_level2var_for_pdd_grobner();
 };  // end of core
 

src/math/lp/nla_grobner.cpp

@@ -54,7 +54,7 @@ void grobner::check_eq(grobner_core::equation* target) {
                   c().print_var(j, tout);
               }
               tout << "\ntarget->expr() val = " << get_nex_val(target->expr(), [this](unsigned j) { return c().val(j); }) << "\n";);
-        m_reported++;       
+        c().lp_settings().stats().m_grobner_conflicts++;
     }
 }