port Grobner, add fixed var dependencies to create_sum_from_row()

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

src/math/lp/horner.cpp

@@ -81,7 +81,7 @@ bool horner::check_cross_nested_expr(const nex* n) {
     }
     auto interv_wd = interval_of_expr_with_deps(n, 1);
     TRACE("nla_horner", tout << "conflict: interv_wd = "; m_intervals.display(tout, interv_wd ) << *n << "\n";);
-    m_intervals.check_interval_for_conflict_on_zero(interv_wd, m_fixed_var_deps);
+    m_intervals.check_interval_for_conflict_on_zero(interv_wd, m_fixed_var_constraints_for_row);
     m_intervals.reset(); // clean the memory allocated by the interval bound dependencies
     return true;
 }
@@ -94,7 +94,10 @@ bool horner::lemmas_on_row(const T& row) {
         [this]() { return c().random(); }, m_nex_creator);
 
     SASSERT (row_is_interesting(row));
-    create_sum_from_row(row, cn.get_nex_creator(), m_row_sum, m_fixed_var_deps);    
+    c().clear_and_resize_active_var_set();
+    m_fixed_var_constraints_for_row.clear();
+    create_sum_from_row(row, cn.get_nex_creator(), m_row_sum, m_fixed_var_constraints_for_row);
+    set_active_vars_weights(); // without this call the comparisons will be incorrect
     nex* e =  m_nex_creator.simplify(&m_row_sum);
     if (!e->is_sum())
         return false;
@@ -108,7 +111,6 @@ void horner::horner_lemmas() {
         return;
     }
     c().lp_settings().stats().m_horner_calls++;
-    set_active_vars_weights();
     const auto& matrix = c().m_lar_solver.A_r();
     // choose only rows that depend on m_to_refine variables
     std::set<unsigned> rows_to_check; // we need it to be determenistic: cannot work with the unordered_set
@@ -116,7 +118,7 @@ void horner::horner_lemmas() {
         for (auto & s : matrix.m_columns[j])
             rows_to_check.insert(s.var());
     }
-    c().prepare_active_var_set();
+    c().clear_and_resize_active_var_set();
     svector<unsigned> rows;
     for (unsigned i : rows_to_check) {
         if (row_is_interesting(matrix.m_rows[i]))

src/math/lp/horner.h

@@ -30,9 +30,9 @@ class core;
 
 
 class horner : common {
-    intervals             m_intervals;
+    intervals                                                     m_intervals;
-    nex_sum               m_row_sum;
+    nex_sum                                                       m_row_sum;
-    ci_dependency*        m_fixed_var_deps;
+    svector<lp::constraint_index>                                 m_fixed_var_constraints_for_row;
 public:
     typedef intervals::interval interv;
     horner(core *core);

src/math/lp/lar_core_solver.h

@@ -799,7 +799,7 @@ public:
             ( m_column_types()[j] == column_type::boxed &&
               m_r_solver.m_lower_bounds[j] == m_r_solver.m_upper_bounds[j]);
     }
-
+    
     const impq & lower_bound(unsigned j) const {
         lp_assert(m_column_types()[j] == column_type::fixed ||
                     m_column_types()[j] == column_type::boxed ||

src/math/lp/nex_creator.cpp

@@ -357,6 +357,9 @@ nex * nex_creator::simplify_mul(nex_mul *e) {
     simplify_children_of_mul(e->children(), coeff);
     if (e->size() == 1 && (*e)[0].pow() == 1 && coeff.is_one()) 
         return (*e)[0].e();
+    
+    if (e->size() == 0 || e->coeff().is_zero())
+        return mk_scalar(e->coeff());
     TRACE("nla_cn_details", tout << *e << "\n";);
     SASSERT(is_simplified(e));
     return e;
@@ -540,7 +543,10 @@ void nex_creator::simplify_children_of_sum(ptr_vector<nex> & children) {
         } else if (is_zero_scalar(e)) {
             skipped ++;
             continue;
-        } else {
+        } else if (e->is_mul() && to_mul(e)->coeff().is_zero() ) {
+            skipped ++;
+            continue;
+        }else {
             unsigned offset = to_promote.size() + skipped;
             if (offset) {
                 children[j - offset] = e;

src/math/lp/nla_common.cpp

@@ -122,7 +122,9 @@ unsigned common::random() {
     return c().random();
 }
 
-nex * common::nexvar(lpvar j, nex_creator& cn) {
+// it also inserts variables into m_active_vars
+// and updates fixed_var_deps
+nex * common::nexvar(lpvar j, nex_creator& cn,  svector<lp::constraint_index> & fixed_vars_constraints) {
     // todo: consider deepen the recursion
     if (!c().is_monic_var(j)) {
         c().insert_to_active_var_set(j);
@@ -138,15 +140,30 @@ nex * common::nexvar(lpvar j, nex_creator& cn) {
     return e;
 }
 
-nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) {
+nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn,
-    // todo: consider deepen the recursion
+                     svector<lp::constraint_index> & fixed_vars_constraints) {
     if (!c().is_monic_var(j)) {
+        if (c().var_is_fixed(j)) {
+            lp::constraint_index lc,uc;
+            c().m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
+            fixed_vars_constraints.push_back(lc);
+            fixed_vars_constraints.push_back(uc);
+            return cn.mk_scalar(c().m_lar_solver.get_lower_bound(j).x);
+        } 
         c().insert_to_active_var_set(j);
         return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(j));
     }
     const monic& m = c().emons()[j];
     nex_mul * e = cn.mk_mul(cn.mk_scalar(coeff));
     for (lpvar k : m.vars()) {
+        if (c().var_is_fixed(j)) {
+            lp::constraint_index lc,uc;
+            c().m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
+            fixed_vars_constraints.push_back(lc);
+            fixed_vars_constraints.push_back(uc);
+            e->coeff() *=  c().m_lar_solver.get_lower_bound(j).x;
+            continue;
+        }  
         c().insert_to_active_var_set(j);
         e->add_child(cn.mk_var(k));
         CTRACE("nla_horner", c().is_monic_var(k), c().print_var(k, tout) << "\n";);
@@ -155,21 +172,24 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) {
 }
 
 
-template <typename T> void common::create_sum_from_row(const T& row, nex_creator& cn, nex_sum& sum, ci_dependency*& fixed_var_deps) {
+template <typename T> void common::create_sum_from_row(const T& row, nex_creator& cn,
+                                                       nex_sum& sum,
+                                                       svector<lp::constraint_index> & fixed_vars_constraints) {
+
     TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";);
 
-    fixed_var_deps = nullptr;
-    
     SASSERT(row.size() > 1);
     sum.children().clear();
     for (const auto &p : row) {
-        if (p.coeff().is_one())
+        if (p.coeff().is_one()) {
-            sum.add_child(nexvar(p.var(), cn));
+            nex* e = nexvar(p.var(), cn, fixed_vars_constraints);
-        else {           
+            sum.add_child(e);
-            sum.add_child(nexvar(p.coeff(), p.var(), cn));
+        } else {
+            nex* e = nexvar(p.coeff(), p.var(), cn, fixed_vars_constraints);
+            sum.add_child(e);
         }
     }
-   }
+}
 
 void common::set_active_vars_weights() {
     m_nex_creator.set_number_of_vars(c().m_lar_solver.column_count());
@@ -206,5 +226,6 @@ var_weight common::get_var_weight(lpvar j) const {
 
 
 }
-template void nla::common::create_sum_from_row<old_vector<lp::row_cell<rational>, true, unsigned int> >(old_vector<lp::row_cell<rational>, true, unsigned int> const&, nla::nex_creator&, nla::nex_sum&, ci_dependency*&);
+template void nla::common::create_sum_from_row<old_vector<lp::row_cell<rational>, true, unsigned int> >(old_vector<lp::row_cell<rational>, true, unsigned int> const&, nla::nex_creator&, nla::nex_sum&, svector<lp::constraint_index>&);  
+
 

src/math/lp/nla_common.h

@@ -117,10 +117,11 @@ struct common {
     typedef dependency_manager<ci_dependency_config> ci_dependency_manager;
 
     typedef ci_dependency_manager::dependency ci_dependency;
-    nex* nexvar(lpvar j, nex_creator& );
+    nex* nexvar(lpvar j, nex_creator&, svector<lp::constraint_index> & fixed_vars_constraints);
-    nex* nexvar(const rational& coeff, lpvar j, nex_creator&);
+    nex* nexvar(const rational& coeff, lpvar j, nex_creator&, svector<lp::constraint_index> & fixed_vars_constraints);
     template <typename T>
-    void create_sum_from_row(const T&, nex_creator&, nex_sum&, ci_dependency*&);
+    void create_sum_from_row(const T&, nex_creator&, nex_sum&,
+                             svector<lp::constraint_index> & fixed_vars_constraints);
     void set_active_vars_weights();
     var_weight get_var_weight(lpvar) const;
 };

src/math/lp/nla_core.h

@@ -107,7 +107,7 @@ public:
         m_active_var_set.clear();
     }
 
-    void prepare_active_var_set() const {
+    void clear_and_resize_active_var_set() const {
         m_active_var_set.clear();
         m_active_var_set.resize(m_lar_solver.number_of_vars());
     }

src/math/lp/nla_grobner.cpp

@@ -99,8 +99,7 @@ void nla_grobner::find_nl_cluster() {
 void nla_grobner::prepare_rows_and_active_vars() {
     m_rows.clear();
     m_rows.resize(c().m_lar_solver.row_count());
-    m_active_vars.clear();
+    c().clear_and_resize_active_var_set();
-    m_active_vars.resize(c().m_lar_solver.column_count());
 }
 
 void nla_grobner::display(std::ostream & out) {
@@ -171,16 +170,23 @@ nex * nla_grobner::mk_monomial_in_row(rational coeff, lpvar j, ci_dependency * &
     */
 }
 
+common::ci_dependency* nla_grobner::dep_from_vector(svector<lp::constraint_index> & cs) {
+    ci_dependency * d = nullptr;
+    for (auto c : cs)
+        d = m_dep_manager.mk_join(d, m_dep_manager.mk_leaf(c));
+    return d;
+}
 
 void nla_grobner::add_row(unsigned i) {    
     const auto& row = c().m_lar_solver.A_r().m_rows[i];    
     TRACE("nla_grobner", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout););
     nex_sum * ns = m_nex_creator.mk_sum();
-    ci_dependency * dep;
+
-    create_sum_from_row(row, m_nex_creator, *ns, dep);
+    svector<lp::constraint_index> fixed_vars_constraints;
+    create_sum_from_row(row, m_nex_creator, *ns, fixed_vars_constraints);
     TRACE("nla_grobner", tout << "ns = " << *ns << "\n";);
-    m_tmp_var_set.clear();
+    m_tmp_var_set.clear();    
-    assert_eq_0(ns, dep);
+    assert_eq_0(ns, dep_from_vector(fixed_vars_constraints));
 }
 
 void nla_grobner::simplify_equations_to_process() {
@@ -191,7 +197,7 @@ void nla_grobner::simplify_equations_to_process() {
 
 void nla_grobner::init() {
     find_nl_cluster();
-    c().prepare_active_var_set();
+    c().clear_and_resize_active_var_set();
     for (unsigned i : m_rows) {
         add_row(i);
     }

src/math/lp/nla_grobner.h

@@ -165,5 +165,6 @@ bool simplify_processed_with_eq(equation*);
     void insert_to_process(equation *eq) { m_to_process.insert(eq); }
     void simplify_equations_to_process();
     const nex_mul * get_highest_monomial(const nex * e) const;
+    ci_dependency* dep_from_vector( svector<lp::constraint_index> & fixed_vars_constraints);
 }; // end of grobner
 }

src/math/lp/nla_intervals.cpp

@@ -103,32 +103,35 @@ bool intervals::separated_from_zero_on_upper(const interval& i) const {
 }
 
 
-bool intervals::check_interval_for_conflict_on_zero(const interval & i, ci_dependency * fixed_var_deps) {
+bool intervals::check_interval_for_conflict_on_zero(const interval & i, const svector<lp::constraint_index>& cs) {
-    return check_interval_for_conflict_on_zero_lower(i, fixed_var_deps) || check_interval_for_conflict_on_zero_upper(i, fixed_var_deps);
+    return check_interval_for_conflict_on_zero_lower(i, cs) || check_interval_for_conflict_on_zero_upper(i, cs);
 }
 
-bool intervals::check_interval_for_conflict_on_zero_upper(const interval & i, ci_dependency* fixed_var_deps) {
+bool intervals::check_interval_for_conflict_on_zero_upper(
+    const interval & i,
+    const svector<lp::constraint_index>& fixed_vars_constraints) {
     if (!separated_from_zero_on_upper(i))
         return false;
         
      add_empty_lemma();
      svector<lp::constraint_index> expl;
-     if (fixed_var_deps)
+     for (auto c : fixed_vars_constraints) {
-         m_dep_manager.linearize(fixed_var_deps, expl); 
+         expl.push_back(c);
-         
+     }
      m_dep_manager.linearize(i.m_upper_dep, expl); 
      _().current_expl().add_expl(expl);
      TRACE("nla_solver", print_lemma(tout););
      return true;
 }
 
-bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i, ci_dependency* fixed_var_deps) {
+bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i,  const svector<lp::constraint_index>& fixed_vars_constraints) {
     if (!separated_from_zero_on_lower(i))
         return false;
      add_empty_lemma();
      svector<lp::constraint_index> expl;
-     if (fixed_var_deps)
+     for (auto c : fixed_vars_constraints) {
-         m_dep_manager.linearize(fixed_var_deps, expl); 
+         expl.push_back(c);
+     }
 
      m_dep_manager.linearize(i.m_lower_dep, expl); 
      _().current_expl().add_expl(expl);

src/math/lp/nla_intervals.h

@@ -156,6 +156,9 @@ public:
         m_config(m_num_manager, m_dep_manager),
         m_imanager(lim, im_config(m_num_manager, m_dep_manager))
     {}
+    ci_dependency* mk_join(ci_dependency* a, ci_dependency* b) { return m_dep_manager.mk_join(a, b);}
+    ci_dependency* mk_leaf(lp::constraint_index ci) { return m_dep_manager.mk_leaf(ci);}
+    
     interval mul(const svector<lpvar>&) const;
     void get_explanation_of_upper_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const;
     void get_explanation_of_lower_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const;
@@ -425,9 +428,9 @@ public:
         return separated_from_zero_on_upper(i) ||
             separated_from_zero_on_lower(i);            
         }
-    bool check_interval_for_conflict_on_zero(const interval & i, ci_dependency*);
+    bool check_interval_for_conflict_on_zero(const interval & i, const svector<lp::constraint_index>&);
-    bool check_interval_for_conflict_on_zero_lower(const interval & i, ci_dependency*);
+    bool check_interval_for_conflict_on_zero_lower(const interval & i, const svector<lp::constraint_index>&);
-    bool check_interval_for_conflict_on_zero_upper(const interval & i, ci_dependency*);
+    bool check_interval_for_conflict_on_zero_upper(const interval & i, const svector<lp::constraint_index>&);
     mpq const & lower(interval const & a) const { return m_config.lower(a); }
     mpq const & upper(interval const & a) const { return m_config.upper(a); }
     inline