From 2181c982e89109e8fd551a77f9a946972786ecf1 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 3 Jul 2019 14:30:36 -0700 Subject: [PATCH] progress with horner's heuristic Signed-off-by: Lev Nachmanson --- src/math/lp/horner.cpp | 60 ++++++++++++++++++++--------------- src/math/lp/horner.h | 8 +++-- src/math/lp/lar_solver.h | 7 +++- src/math/lp/nla_core.cpp | 10 +++++- src/math/lp/nla_core.h | 1 + src/math/lp/nla_intervals.cpp | 21 +++++++++--- src/math/lp/nla_intervals.h | 2 +- 7 files changed, 73 insertions(+), 36 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index dda8efb6a..f07f774ef 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -41,8 +41,9 @@ void horner::lemma_on_row(const T& row) { return; nex e = create_expr_from_row(row); TRACE("nla_cn", tout << "cross nested e = " << e << std::endl;); - intervals::interval inter = interval_of_expr(e); - check_interval_for_conflict(inter); + intervals::interval a = interval_of_expr(e); + TRACE("nla_cn", tout << "interval a = "; m_intervals.display(tout, a) << "\n";); + check_interval_for_conflict(a, row); } void horner::horner_lemmas() { @@ -120,7 +121,7 @@ unsigned horner::random_most_occured_var(std::unordered_map& oc // j -> the number of expressions j appears in void horner::get_occurences_map(const nla_expr& e, std::unordered_map& occurences) const { - TRACE("nla_cn", tout << "e = " << e << std::endl;); + TRACE("nla_cn_details", tout << "e = " << e << std::endl;); SASSERT(e.type() == expr_type::SUM); for (const auto & ce : e.children()) { std::unordered_set seen; @@ -183,7 +184,6 @@ nex horner::split_with_var(const nex& e, lpvar j) { } nex horner::cross_nested_of_sum(const nex& e) { - TRACE("nla_cn", ); if (!e.is_sum()) return e; std::unordered_map occurences; @@ -218,19 +218,22 @@ template nex horner::create_expr_from_row(const T& row) { return e; } +template +void horner::set_interval_for_scalar(interv& a, const T& v) { + m_intervals.set_lower(a, v); + m_intervals.set_upper(a, v); + m_intervals.set_lower_is_open(a, false); + m_intervals.set_lower_is_inf(a, false); + m_intervals.set_upper_is_open(a, false); + m_intervals.set_upper_is_inf(a, false); +} + intervals::interval horner::interval_of_expr(const nex& e) { - TRACE("nla_cn", tout << e.type() << " e=" << e << std::endl;); + TRACE("nla_cn_details", tout << e.type() << " e=" << e << std::endl;); interv a; switch (e.type()) { case expr_type::SCALAR: - m_intervals.set_lower(a, e.value()); - m_intervals.set_upper(a, e.value()); - m_intervals.set_lower_is_open(a, false); - m_intervals.set_lower_is_inf(a, false); - m_intervals.set_upper_is_open(a, false); - m_intervals.set_upper_is_inf(a, false); - - TRACE("nla_cn", tout << "e.value() = " << e.value() << "\n"; m_intervals.display(tout, a) << '\n';); + set_interval_for_scalar(a, e.value()); return a; case expr_type::SUM: return interval_of_sum(e.children()); @@ -238,7 +241,6 @@ intervals::interval horner::interval_of_expr(const nex& e) { return interval_of_mul(e.children()); case expr_type::VAR: set_var_interval(e.var(), a); - TRACE("nla_cn", tout << "a = "; m_intervals.display(tout, a) << "\n";); return a; default: TRACE("nla_cn", tout << e.type() << "\n";); @@ -250,14 +252,14 @@ template interv horner::interval_of_mul(const vector>& es) { interv a = interval_of_expr(es[0]); if (m_intervals.is_zero(a)) { - TRACE("nla_cn", tout << "got zero\n";); + TRACE("nla_cn", m_intervals.display(tout, a) << "\ngot zero for " << es[0] << "\n";); return a; } TRACE("nla_cn", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); tout << "\n";); for (unsigned k = 1; k < es.size(); k++) { interv b = interval_of_expr(es[k]); if (m_intervals.is_zero(b)) { - TRACE("nla_cn", tout << "got zero\n";); + TRACE("nla_cn", m_intervals.display(tout, b) << "\ngot zero for " << es[k] << "\n";); return b; } interv c; @@ -265,21 +267,24 @@ interv horner::interval_of_mul(const vector>& es) { m_intervals.mul(a, b, c, deps); m_intervals.set(a, c); m_intervals.add_deps(a, b, deps, a); - TRACE("nla_cn", tout << "a = "; m_intervals.display(tout, a); tout << "\n";); } + TRACE("nla_cn", + for (const auto &e : es) tout << e; + tout << " interv a = "; + m_intervals.display(tout, a) << "\n";); return a; } template interv horner::interval_of_sum(const vector>& es) { interv a = interval_of_expr(es[0]); - TRACE("nla_cn", tout << "es[0]= " << es[0] << "\n"; m_intervals.display(tout, a) << "\n";); + TRACE("nla_cn_details", tout << "es[0]= " << es[0] << "\n"; m_intervals.display(tout, a) << "\n";); if (m_intervals.is_inf(a)) { return a; } for (unsigned k = 1; k < es.size(); k++) { - TRACE("nla_cn", tout << "es[" << k << "]= " << es[k] << "\n";); + TRACE("nla_cn_details", tout << "es[" << k << "]= " << es[k] << "\n";); interv b = interval_of_expr(es[k]); if (m_intervals.is_inf(b)) { TRACE("nla_cn", tout << "got inf\n";); @@ -290,9 +295,9 @@ interv horner::interval_of_sum(const vector>& es) { m_intervals.add(a, b, c, deps); m_intervals.set(a, c); m_intervals.add_deps(a, b, deps, a); - TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";); + TRACE("nla_cn_details", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";); if (m_intervals.is_inf(a)) { - TRACE("nla_cn", tout << "got infinity\n";); + TRACE("nla_cn_details", tout << "got infinity\n";); return a; } } @@ -301,11 +306,16 @@ interv horner::interval_of_sum(const vector>& es) { // sets the dependencies also void horner::set_var_interval(lpvar v, interv& b) { m_intervals.set_var_interval_with_deps(v, b); - TRACE("nla_cn", tout << "v = "; print_var(v, tout); tout << "\n";); + + TRACE("nla_cn", tout << "v = "; print_var(v, tout) << "\n"; m_intervals.display(tout, b)<< '\n';); } - -void horner::check_interval_for_conflict(const intervals::interval& i) { - m_intervals.check_interval_for_conflict_on_zero(i); +template +void horner::check_interval_for_conflict(const intervals::interval& i, const T& row) { + if (m_intervals.check_interval_for_conflict_on_zero(i)) { + TRACE("nla_cn", print_lemma(tout);); + } else { + TRACE("nla_cn", tout << "no lemma\n";); + } } } diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index 5e88e5529..801f2687c 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -35,11 +35,11 @@ public: void horner_lemmas(); template // T has an iterator of (coeff(), var()) void lemma_on_row(const T&); - template - bool row_is_interesting(const T&) const; + template bool row_is_interesting(const T&) const; template nla_expr create_expr_from_row(const T&); intervals::interval interval_of_expr(const nla_expr& e); - void check_interval_for_conflict(const intervals::interval&); + + template void check_interval_for_conflict(const intervals::interval&, const T&); bool check_interval_for_conflict_lower_bound(const intervals::interval&); bool check_interval_for_conflict_upper_bound(const intervals::interval&); nla_expr nexvar(lpvar j) const; @@ -53,5 +53,7 @@ public: intervals::interval interval_of_sum(const vector>&); template intervals::interval interval_of_mul(const vector>&); + template + void set_interval_for_scalar(intervals::interval&, const T&); }; // end of horner } diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 74516db64..17f1d48ea 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -607,7 +607,12 @@ public: } std::ostream& print_column_info(unsigned j, std::ostream& out) const { - return m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out); + m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out); + if( !column_corresponds_to_term(j)) + return out; + const lar_term& t = * m_terms[m_var_register.local_to_external(j) - m_terms_start_index]; + print_term_as_indices(t, out) << "\n"; + return out; } bool has_int_var() const; diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 60e46757f..9f96a2e76 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -433,6 +433,14 @@ void core::mk_ineq(lp::lar_term& t, llc cmp, const rational& rs) { } } +void core::mk_ineq_no_expl_check(lp::lar_term& t, llc cmp, const rational& rs) { + TRACE("nla_solver_details", m_lar_solver.print_term_as_indices(t, tout << "t = ");); + m_lar_solver.subs_term_columns(t); + current_lemma().push_back(ineq(cmp, t, rs)); + CTRACE("nla_solver", ineq_holds(ineq(cmp, t, rs)), print_ineq(ineq(cmp, t, rs), tout) << "\n";); + SASSERT(!ineq_holds(ineq(cmp, t, rs))); +} + void core::mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs) { lp::lar_term t; t.add_coeff_var(a, j); @@ -1246,7 +1254,7 @@ lbool core:: inner_check(bool derived) { return l_false; } - TRACE("nla_cn", print_terms(tout);); + TRACE("nla_cn_details", print_terms(tout);); for (int search_level = 0; search_level < 3 && !done(); search_level++) { TRACE("nla_solver", tout << "derived = " << derived << ", search_level = " << search_level << "\n";); if (search_level == 0) { diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index bd0656303..04a1b7f91 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -201,6 +201,7 @@ public: void mk_ineq(lp::lar_term& t, llc cmp, const rational& rs); + void mk_ineq_no_expl_check(lp::lar_term& t, llc cmp, const rational& rs); void mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs); void mk_ineq(bool a, lpvar j, bool b, lpvar k, llc cmp, const rational& rs); void mk_ineq(bool a, lpvar j, bool b, lpvar k, llc cmp); diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 0fbf3607a..ed3abdced 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -75,10 +75,8 @@ void intervals::set_var_interval_with_deps(lpvar v, interval& b) { } } -void intervals::check_interval_for_conflict_on_zero(const interval & i) { - if (check_interval_for_conflict_on_zero_lower(i)) - return; - check_interval_for_conflict_on_zero_upper(i); +bool intervals::check_interval_for_conflict_on_zero(const interval & i) { + return check_interval_for_conflict_on_zero_lower(i) || check_interval_for_conflict_on_zero_upper(i); } bool intervals::check_interval_for_conflict_on_zero_upper(const interval & i) { @@ -98,7 +96,7 @@ bool intervals::check_interval_for_conflict_on_zero_upper(const interval & i) { bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i) { if (lower_is_inf(i)) return false; - if (unsynch_mpq_manager::is_pos(lower(i))) + if (unsynch_mpq_manager::is_neg(lower(i))) return false; if (unsynch_mpq_manager::is_zero(lower(i)) && !m_config.lower_is_open(i)) return false; @@ -126,6 +124,19 @@ std::ostream& intervals::display(std::ostream& out, const interval& i) const { } else { out << rational(m_imanager.upper(i)) << (m_imanager.lower_is_open(i)? ")":"]"); } + svector expl; + m_dep_manager.linearize(i.m_lower_dep, expl); + out << "\nlower constraints (\n"; + for (lp::constraint_index c: expl) + m_core->m_lar_solver.print_constraint_indices_only(c, out); + out << ")\n"; + expl.clear(); + m_dep_manager.linearize(i.m_upper_dep, expl); + out << "upper constraints (\n"; + for (lp::constraint_index c: expl) + m_core->m_lar_solver.print_constraint_indices_only(c, out); + out << ")\n"; + return out; } diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 8f606fffa..fe6107e13 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -193,7 +193,7 @@ public: bool lower_is_inf(const interval& a) const { return m_config.lower_is_inf(a); } void set_var_interval_with_deps(lpvar, interval &); bool is_inf(const interval& i) const { return m_config.is_inf(i); } - void check_interval_for_conflict_on_zero(const interval & i); + bool check_interval_for_conflict_on_zero(const interval & i); bool check_interval_for_conflict_on_zero_lower(const interval & i); bool check_interval_for_conflict_on_zero_upper(const interval & i); mpq const & lower(interval const & a) const { return m_config.lower(a); }