From a86d4b0675f2abe33c3d17012f5c6a847f297b71 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 10 Dec 2019 17:10:02 -1000 Subject: [PATCH] add dependencies for row in grobner Signed-off-by: Lev Nachmanson --- src/math/lp/horner.cpp | 2 +- src/math/lp/nla_common.cpp | 29 ++++++++++++++++------- src/math/lp/nla_common.h | 2 +- src/math/lp/nla_grobner.cpp | 15 ++++++------ src/math/lp/nla_intervals.cpp | 44 ++++++++++++++++++----------------- src/math/lp/nla_intervals.h | 1 + 6 files changed, 55 insertions(+), 38 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index c6cf24048..ba9ca5aef 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -78,7 +78,7 @@ bool horner::lemmas_on_row(const T& row) { SASSERT (row_is_interesting(row)); c().clear_and_resize_active_var_set(); - create_sum_from_row(row, cn.get_nex_creator(), m_row_sum, m_fixed_as_scalars); + create_sum_from_row(row, cn.get_nex_creator(), m_row_sum, m_fixed_as_scalars, nullptr); set_active_vars_weights(); // without this call the comparisons will be incorrect nex* e = m_nex_creator.simplify(&m_row_sum); TRACE("nla_horner", tout << "e = " << * e << "\n";); diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp index fd629d6d6..a5473f8f1 100644 --- a/src/math/lp/nla_common.cpp +++ b/src/math/lp/nla_common.cpp @@ -159,20 +159,33 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixe } -template void common::create_sum_from_row(const T& row, - nex_creator& cn, - nex_sum& sum, bool fixed_as_scalars) { +template common::ci_dependency* common::create_sum_from_row(const T& row, + nex_creator& cn, + nex_sum& sum, + bool fixed_as_scalars, + ci_dependency_manager* dep_manager + ) { TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";); - + ci_dependency * dep = nullptr; SASSERT(row.size() > 1); sum.children().clear(); for (const auto &p : row) { nex* e = nexvar(p.coeff(), p.var(), cn, fixed_as_scalars); - if (e) - sum.add_child(e); + if (!e) + continue; + unsigned lc, uc; + if (dep_manager) { + c().m_lar_solver.get_bound_constraint_witnesses_for_column(p.var(), lc, uc); + if (lc + 1) + dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(lc)); + if (uc + 1) + dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(uc)); + sum.add_child(e); + } } - TRACE("nla_horner", tout << "sum =" << sum << "\n";); + TRACE("nla_grobner", tout << "sum =" << sum << "\ndep="; m_intervals->print_dependencies(dep, tout);); + return dep; } template @@ -242,6 +255,6 @@ var_weight common::get_var_weight(lpvar j) const { } -template void nla::common::create_sum_from_row, true, unsigned int> >(old_vector, true, unsigned int> const&, nla::nex_creator&, nla::nex_sum&, bool); +template nla::common::ci_dependency* nla::common::create_sum_from_row, true, unsigned int> >(old_vector, true, unsigned int> const&, nla::nex_creator&, nla::nex_sum&, bool, ci_dependency_manager*); template dependency_manager::dependency* nla::common::get_fixed_vars_dep_from_row, true, unsigned int> >(old_vector, true, unsigned int> const&, dependency_manager&); diff --git a/src/math/lp/nla_common.h b/src/math/lp/nla_common.h index f2f3bb046..634c2baf7 100644 --- a/src/math/lp/nla_common.h +++ b/src/math/lp/nla_common.h @@ -122,7 +122,7 @@ struct common { // nex* nexvar(lpvar j, nex_creator&, svector & fixed_vars_constraints); nex* nexvar(const rational& coeff, lpvar j, nex_creator&, bool); template - void create_sum_from_row(const T&, nex_creator&, nex_sum&, bool); + ci_dependency* create_sum_from_row(const T&, nex_creator&, nex_sum&, bool, ci_dependency_manager*); template ci_dependency* get_fixed_vars_dep_from_row(const T&, ci_dependency_manager& dep_manager); void set_active_vars_weights(); diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 010ef94eb..d1bf7cafd 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -129,11 +129,10 @@ void nla_grobner::add_row(unsigned i) { } ); nex_sum * ns = m_nex_creator.mk_sum(); - create_sum_from_row(row, m_nex_creator, *ns, m_look_for_fixed_vars_in_rows); + ci_dependency* dep = create_sum_from_row(row, m_nex_creator, *ns, m_look_for_fixed_vars_in_rows, &m_dep_manager); nex* e = m_nex_creator.simplify(ns); TRACE("grobner", tout << "e = " << *e << "\n";); - m_tmp_var_set.clear(); - assert_eq_0(e, m_look_for_fixed_vars_in_rows? get_fixed_vars_dep_from_row(row, m_dep_manager) : nullptr); + assert_eq_0(e, dep); } void nla_grobner::simplify_equations_in_m_to_simplify() { @@ -144,7 +143,6 @@ void nla_grobner::simplify_equations_in_m_to_simplify() { void nla_grobner::init() { m_reported = 0; - m_conflict = false; del_equations(0); SASSERT(m_equations_to_delete.size() == 0); m_to_superpose.reset(); @@ -566,8 +564,7 @@ void nla_grobner::superpose(equation * eq1, equation * eq2) { void nla_grobner::register_report() { m_reported++; - if (c().current_lemma().expl().size() == 0) - m_conflict = true; + m_conflict = true; } // Let a be the greatest common divider of ab and bc, // then ab/a is stored in b, and ac/a is stored in c @@ -833,10 +830,12 @@ std::unordered_set nla_grobner::get_vars_of_expr_with_opening_terms(const void nla_grobner::assert_eq_0(nex* e, ci_dependency * dep) { if (e == nullptr || is_zero_scalar(e)) return; + m_tmp_var_set.clear(); equation * eq = alloc(equation); init_equation(eq, e, dep); TRACE("grobner", display_equation(tout, *eq); + tout << "\nvars\n"; for (unsigned j : get_vars_of_expr_with_opening_terms(e)) { tout << "("; c().print_var(j, tout) << ")\n"; @@ -866,7 +865,9 @@ std::ostream& nla_grobner::display_dependency(std::ostream& out, ci_dependency* out << "constraints\n"; m_core->print_explanation(e, out); out << "\n"; - } + } else { + out << "no deps\n"; + } } return out; diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 16e610918..fffab5637 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -244,9 +244,24 @@ intervals::interv intervals::interval_of_mul(const nex_mul* e) { return a; } +std::ostream & intervals::print_dependencies(ci_dependency* deps , std::ostream& out) const { + svector expl; + m_dep_manager.linearize(deps, expl); + { + lp::explanation e(expl); + if (!expl.empty()) { + m_core->print_explanation(e, out); + expl.clear(); + } else { + out << "\nno constraints\n"; + } + } + return out; +} + // return true iff the interval of n is does not contain 0 bool intervals::check_nex(const nex* n, ci_dependency* initial_deps) { - TRACE("nla_grobner", tout << "cross-nested n = " << *n << ", n->type() == " << n->type() << "\n";); + TRACE("nla_grobner", tout << "n = " << *n << "\n";); m_core->lp_settings().stats().m_cross_nested_forms++; auto i = interval_of_expr(n, 1); @@ -256,7 +271,7 @@ bool intervals::check_nex(const nex* n, ci_dependency* initial_deps) { return false; } auto interv_wd = interval_of_expr_with_deps(n, 1); - TRACE("nla_grobner", tout << "conflict: interv_wd = "; display(tout, interv_wd ) << *n << "\n";); + TRACE("nla_grobner", tout << "conflict: interv_wd = "; display(tout, interv_wd ) << *n << "\n, initial deps\n"; print_dependencies(initial_deps, tout);); check_interval_for_conflict_on_zero(interv_wd, initial_deps); reset(); // clean the memory allocated by the interval bound dependencies return true; @@ -615,26 +630,13 @@ std::ostream& intervals::display(std::ostream& out, const interval& i) const { out << rational(m_imanager.upper(i)) << (m_imanager.upper_is_open(i)? ")":"]"); } svector expl; - m_dep_manager.linearize(i.m_lower_dep, expl); - { - lp::explanation e(expl); - if (!expl.empty()) { - out << "\nlower constraints\n"; - m_core->print_explanation(e, out); - expl.clear(); - } else { - out << "\nno lower constraints\n"; - } + if (i.m_lower_dep) { + out << "\nlower deps\n"; + print_dependencies(i.m_lower_dep, out); } - m_dep_manager.linearize(i.m_upper_dep, expl); - { - lp::explanation e(expl); - if (!expl.empty()) { - out << "upper constraints\n"; - m_core->print_explanation(e, out); - }else { - out << "no upper constraints\n"; - } + if (i.m_upper_dep) { + out << "\nupper deps\n"; + print_dependencies(i.m_upper_dep, out); } return out; } diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 0e3325a69..7ec40d093 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -167,6 +167,7 @@ public: interval mul(const svector&) const; void get_explanation_of_upper_bound_for_monomial(lpvar j, svector& expl) const; void get_explanation_of_lower_bound_for_monomial(lpvar j, svector& expl) const; + std::ostream & print_dependencies(ci_dependency* , std::ostream&) const; std::ostream& print_explanations(const svector &, std::ostream&) const; std::ostream& display(std::ostream& out, const intervals::interval& i) const; void set_lower(interval & a, rational const & n) const { m_config.set_lower(a, n.to_mpq()); }