From e62913999e5d81c1e9c57eccd1e900735c0a2b12 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 5 Dec 2019 16:19:17 -1000 Subject: [PATCH] in grobner optional treatment of fixed vars in rows, remove a field Signed-off-by: Lev Nachmanson --- src/math/lp/nla_common.cpp | 8 +++++--- src/math/lp/nla_grobner.cpp | 20 +++++++------------- src/math/lp/nla_grobner.h | 2 +- 3 files changed, 13 insertions(+), 17 deletions(-) diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp index 78e826974..fd629d6d6 100644 --- a/src/math/lp/nla_common.cpp +++ b/src/math/lp/nla_common.cpp @@ -129,8 +129,10 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixe if (!c().is_monic_var(j)) { if (fixed_as_scalars && c().var_is_fixed(j)) { auto & b = c().m_lar_solver.get_lower_bound(j).x; - if (b.is_zero()) + if (b.is_zero()) { + TRACE("nla_grobner", tout << "[" << j << "] is fixed to zero\n";); return nullptr; + } return cn.mk_scalar(coeff * b); } c().insert_to_active_var_set(j); @@ -150,9 +152,9 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixe } c().insert_to_active_var_set(k); e->add_child(cn.mk_var(k)); - CTRACE("nla_horner", c().is_monic_var(k), c().print_var(k, tout) << "\n";); + CTRACE("nla_grobner", c().is_monic_var(k), c().print_var(k, tout) << "\n";); } - TRACE("nla_cn", tout << *e;); + TRACE("nla_grobner", tout << *e;); return e; } diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 40ab5b7ed..f805a0b7c 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -25,7 +25,9 @@ nla_grobner::nla_grobner(core *c, intervals *s) : common(c, s), m_nl_gb_exhausted(false), m_dep_manager(m_val_manager, m_alloc), - m_changed_leading_term(false) {} + m_changed_leading_term(false), + m_look_for_fixed_vars_in_rows(false) +{} bool nla_grobner::internalize_gb_eq(equation* ) { NOT_IMPLEMENTED_YET(); @@ -139,14 +141,11 @@ void nla_grobner::add_row(unsigned i) { } ); nex_sum * ns = m_nex_creator.mk_sum(); - - - svector fixed_vars_constraints; - create_sum_from_row(row, m_nex_creator, *ns, true); // true to treat fixed vars as scalars + create_sum_from_row(row, m_nex_creator, *ns, m_look_for_fixed_vars_in_rows); nex* e = m_nex_creator.simplify(ns); TRACE("grobner", tout << "e = " << *e << "\n";); m_tmp_var_set.clear(); - assert_eq_0(e, get_fixed_vars_dep_from_row(row, m_dep_manager)); + assert_eq_0(e, m_look_for_fixed_vars_in_rows? get_fixed_vars_dep_from_row(row, m_dep_manager) : nullptr); } void nla_grobner::simplify_equations_to_process() { @@ -158,7 +157,6 @@ void nla_grobner::simplify_equations_to_process() { void nla_grobner::init() { m_reported = 0; m_conflict = false; - m_equations_to_unfreeze.clear(); del_equations(0); SASSERT(m_equations_to_delete.size() == 0); m_num_of_equations = 0; @@ -243,7 +241,6 @@ nla_grobner::equation* nla_grobner::simplify_using_processed(equation* eq) { TRACE("grobner", tout << "simplification result: "; display_equation(tout, *eq);); return result ? eq : nullptr; - } const nex* nla_grobner::get_highest_monomial(const nex* e) const { @@ -288,7 +285,7 @@ unsigned nla_grobner::find_divisible(nex_sum* targ_sum, for (unsigned j = 0; j < targ_sum->size(); j++) { auto t = (*targ_sum)[j]; if (divide_ignore_coeffs_check_only(t, high_mon)) { - TRACE("grobner", tout << "yes div: " << *targ_sum << " / " << *high_mon << "\n";); + TRACE("grobner", tout << "yes div: " << *t << " / " << *high_mon << "\n";); return j; } } @@ -461,7 +458,6 @@ nla_grobner::equation * nla_grobner::simplify_source_target(equation * source, e void nla_grobner::process_simplified_target(ptr_buffer& to_insert, equation* new_target, equation*& target, ptr_buffer& to_remove) { if (new_target != target) { - m_equations_to_unfreeze.push_back(target); to_remove.push_back(target); if (m_changed_leading_term) { insert_to_simplify(new_target); @@ -530,7 +526,6 @@ void nla_grobner::simplify_to_superpose(equation* eq) { for (equation* target : m_to_simplify) { equation * new_target = simplify_source_target(eq, target); if (new_target != nullptr && new_target != target) { - m_equations_to_unfreeze.push_back(target); to_insert.push_back(new_target); to_remove.push_back(target); target = new_target; @@ -695,7 +690,6 @@ bool nla_grobner::compute_basis_step() { equation * new_eq = simplify_using_processed(eq); if (new_eq != nullptr && eq != new_eq) { // equation was updated using non destructive updates - m_equations_to_unfreeze.push_back(eq); eq = new_eq; } if (canceled()) return false; @@ -882,7 +876,7 @@ std::ostream& nla_grobner::display_dependency(std::ostream& out, ci_dependency* { lp::explanation e(expl); if (!expl.empty()) { - out << "upper constraints\n"; + out << "constraints\n"; m_core->print_explanation(e, out); }else { out << "no constraints\n"; diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 11e48a299..23533445b 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -78,7 +78,6 @@ class nla_grobner : common { typedef ptr_vector equation_vector; // fields - equation_vector m_equations_to_unfreeze; equation_vector m_equations_to_delete; lp::int_set m_rows; unsigned m_num_of_equations; @@ -95,6 +94,7 @@ class nla_grobner : common { bool m_changed_leading_term; unsigned m_reported; bool m_conflict; + bool m_look_for_fixed_vars_in_rows; public: nla_grobner(core *core, intervals *); void grobner_lemmas();