From 0b1023c2c72b04f101ffe5ea120c469bdebdf47e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 3 Dec 2019 16:56:41 -0800 Subject: [PATCH] do not add row with free basic vars in grobner, more tracing Signed-off-by: Lev Nachmanson --- src/math/lp/lar_core_solver.h | 5 +++++ src/math/lp/lar_solver.cpp | 4 ++++ src/math/lp/lar_solver.h | 1 + src/math/lp/nla_common.cpp | 4 +++- src/math/lp/nla_core.cpp | 4 ++++ src/math/lp/nla_core.h | 1 + src/math/lp/nla_grobner.cpp | 14 ++++++++++++-- 7 files changed, 30 insertions(+), 3 deletions(-) diff --git a/src/math/lp/lar_core_solver.h b/src/math/lp/lar_core_solver.h index a4ede77e9..b248d28f4 100644 --- a/src/math/lp/lar_core_solver.h +++ b/src/math/lp/lar_core_solver.h @@ -799,6 +799,11 @@ public: ( m_column_types()[j] == column_type::boxed && m_r_solver.m_lower_bounds[j] == m_r_solver.m_upper_bounds[j]); } + + bool column_is_free(unsigned j) const { + return m_column_types()[j] == column_type::free_column; + } + const impq & lower_bound(unsigned j) const { lp_assert(m_column_types()[j] == column_type::fixed || diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index b0606a898..bc8a886ca 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1693,6 +1693,10 @@ bool lar_solver::column_is_fixed(unsigned j) const { return m_mpq_lar_core_solver.column_is_fixed(j); } +bool lar_solver::column_is_free(unsigned j) const { + return m_mpq_lar_core_solver.column_is_free(j); +} + // below is the initialization functionality of lar_solver bool lar_solver::strategy_is_undecided() const { diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index a14ba59f6..9b01a110c 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -151,6 +151,7 @@ public: bool is_term(var_index j) const; bool column_is_fixed(unsigned j) const; + bool column_is_free(unsigned j) const; public: // init region diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp index 7561607c2..78e826974 100644 --- a/src/math/lp/nla_common.cpp +++ b/src/math/lp/nla_common.cpp @@ -141,8 +141,10 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixe for (lpvar k : m.vars()) { if (fixed_as_scalars && c().var_is_fixed(k)) { auto & b = c().m_lar_solver.get_lower_bound(k).x; - if (b.is_zero()) + if (b.is_zero()) { + TRACE("nla_grobner", tout << "[" << k << "] is fixed to zero\n";); return nullptr; + } e->coeff() *= b; continue; } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 07aecf3e8..dc5b97e93 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -641,6 +641,10 @@ bool core:: var_is_fixed_to_val(lpvar j, const rational& v) const { bool core:: var_is_fixed(lpvar j) const { return m_lar_solver.column_is_fixed(j); } + +bool core:: var_is_free(lpvar j) const { + return m_lar_solver.column_is_free(j); +} std::ostream & core::print_ineq(const ineq & in, std::ostream & out) const { m_lar_solver.print_term_as_indices(in.m_term, out); diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 690f03b2b..1e910df52 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -287,6 +287,7 @@ public: bool var_is_fixed_to_val(lpvar j, const rational& v) const; bool var_is_fixed(lpvar j) const; + bool var_is_free(lpvar j) const; bool find_canonical_monic_of_vars(const svector& vars, lpvar & i) const; bool is_canonical_monic(lpvar) const; diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 3ec540496..40ab5b7ed 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -34,11 +34,19 @@ bool nla_grobner::internalize_gb_eq(equation* ) { void nla_grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue & q) { SASSERT(!c().active_var_set_contains(j)); + TRACE("grobner", tout << "j = " << j << ", "; c().print_var(j, tout) << "\n";); const auto& matrix = c().m_lar_solver.A_r(); c().insert_to_active_var_set(j); + const auto & core_slv = c().m_lar_solver.m_mpq_lar_core_solver; for (auto & s : matrix.m_columns[j]) { unsigned row = s.var(); if (m_rows.contains(row)) continue; + lpvar basic_in_row = core_slv.m_r_basis[row]; + if (c().var_is_free(basic_in_row)) { + TRACE("grobner", tout << "ignore the row " << row << " with the free basic var\n";); + continue; // mimic the behavior of the legacy solver + + } m_rows.insert(row); for (auto& rc : matrix.m_rows[row]) { if (c().active_var_set_contains(rc.var())) @@ -159,6 +167,7 @@ void nla_grobner::init() { find_nl_cluster(); c().clear_and_resize_active_var_set(); + TRACE("grobner", tout << "m_rows.size() = " << m_rows.size() << "\n";); for (unsigned i : m_rows) { add_row(i); } @@ -730,7 +739,7 @@ bool nla_grobner::done() const { || canceled() || - m_reported > 10 + m_reported > 100000 || m_conflict) { TRACE("grobner", tout << "done()\n";); @@ -776,7 +785,8 @@ bool nla_grobner::try_to_modify_eqs(ptr_vector& eqs, unsigned& next_we void nla_grobner::grobner_lemmas() { - c().lp_settings().stats().m_grobner_calls++; + c().lp_settings().stats().m_grobner_calls++; + init(); ptr_vector eqs;