From 4a87ca8b924ae7f5cc7e52d1addf432b5ec8e276 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sun, 3 Nov 2019 11:34:22 -0800 Subject: [PATCH] remove m_lc field from equation Signed-off-by: Lev Nachmanson --- src/math/lp/nla_grobner.cpp | 22 ++-------------------- src/math/lp/nla_grobner.h | 6 ++---- src/smt/theory_arith_nl.h | 2 +- 3 files changed, 5 insertions(+), 25 deletions(-) diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 79d5d6dab..fbcaf2e98 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -27,21 +27,6 @@ nla_grobner::nla_grobner(core *c, intervals *s) m_dep_manager(m_val_manager, m_alloc), m_changed_leading_term(false) {} -// Scan the grobner basis eqs for equations of the form x - k = 0 or x = 0 is found, and x is not fixed, -// then assert bounds for x, and continue -bool nla_grobner::scan_for_linear(ptr_vector& eqs) { - bool result = false; - for (nla_grobner::equation* eq : eqs) { - if (!eq->is_linear_combination()) { - TRACE("non_linear", tout << "processing new equality:\n"; display_equation(tout, *eq);); - TRACE("non_linear_bug", tout << "processing new equality:\n"; display_equation(tout, *eq);); - if (internalize_gb_eq(eq)) - result = true; - } - } - return result; -} - bool nla_grobner::internalize_gb_eq(equation* ) { NOT_IMPLEMENTED_YET(); return false; @@ -735,7 +720,7 @@ bool nla_grobner::done() const { || canceled() || - m_reported > 0 // 10 + m_reported > 10 || m_conflict) { TRACE("grobner", tout << "done()\n";); @@ -766,9 +751,7 @@ void nla_grobner::update_statistics(){ bool nla_grobner::push_calculation_forward(ptr_vector& eqs, unsigned & next_weight) { - return scan_for_linear(eqs) - && - (!m_nl_gb_exhausted) && + return (!m_nl_gb_exhausted) && try_to_modify_eqs(eqs, next_weight); } @@ -837,7 +820,6 @@ void nla_grobner::init_equation(equation* eq, nex*e, ci_dependency * dep) { unsigned bidx = m_equations_to_delete.size(); eq->m_bidx = bidx; eq->dep() = dep; - eq->m_lc = true; eq->exp() = e; m_equations_to_delete.push_back(eq); SASSERT(m_equations_to_delete[eq->m_bidx] == eq); diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index bae8a492a..ca73becbb 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -39,8 +39,8 @@ struct grobner_stats { class nla_grobner : common { class equation { - unsigned m_bidx:31; //!< position at m_equations_to_delete - unsigned m_lc:1; //!< true if equation if a linear combination of the input equations. + unsigned m_bidx; //!< position at m_equations_to_delete + nex * m_expr; // simplified expressionted monomials ci_dependency * m_dep; //!< justification for the equality public: @@ -71,7 +71,6 @@ class nla_grobner : common { ci_dependency * dep() const { return m_dep; } ci_dependency *& dep() { return m_dep; } unsigned hash() const { return m_bidx; } - bool is_linear_combination() const { return m_lc; } friend class nla_grobner; }; @@ -101,7 +100,6 @@ public: void grobner_lemmas(); ~nla_grobner(); private: - bool scan_for_linear(ptr_vector& eqs); void find_nl_cluster(); void prepare_rows_and_active_vars(); void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue& q); diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 7c5abcf3d..903968cb8 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -2292,7 +2292,7 @@ bool theory_arith::try_to_modify_eqs(ptr_vector& eqs, gr template bool theory_arith::scan_for_linear(ptr_vector& eqs, grobner& gb) { bool result = false; - if (m_params.m_nl_arith_gb_eqs) { + if (m_params.m_nl_arith_gb_eqs) { // m_nl_arith_gb_eqs is false by default for (grobner::equation* eq : eqs) { if (!eq->is_linear_combination()) { TRACE("non_linear", tout << "processing new equality:\n"; gb.display_equation(tout, *eq););