From 2a02d042598a48a271d0b35fb968c9569facf961 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 23 Jul 2019 17:22:37 -0700 Subject: [PATCH] fixes in the interval processing in horner Signed-off-by: Lev Nachmanson --- src/math/lp/horner.cpp | 74 ++++++++++++++++++----------------- src/math/lp/horner.h | 6 +-- src/math/lp/nla_intervals.cpp | 3 +- src/math/lp/nla_intervals.h | 17 ++------ 4 files changed, 45 insertions(+), 55 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index e084dfa5f..012002ac9 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -39,9 +39,9 @@ bool horner::row_is_interesting(const T& row) const { } void horner::lemmas_on_expr(nex& e) { - TRACE("nla_cn", tout << "e = " << e << "\n";); + TRACE("nla_horner", tout << "e = " << e << "\n";); cross_nested cn(e, [this](const nex& n) { - TRACE("nla_cn", tout << "callback n = " << n << "\n";); + TRACE("nla_horner", tout << "callback n = " << n << "\n";); auto i = interval_of_expr(n); m_intervals.check_interval_for_conflict_on_zero(i);} ); cn.run(); @@ -83,7 +83,7 @@ nex horner::nexvar(lpvar j) const { } template nex horner::create_sum_from_row(const T& row) { - TRACE("nla_cn", tout << "row="; m_core->print_term(row, tout) << "\n";); + TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";); SASSERT(row.size() > 1); nex e(expr_type::SUM); for (const auto &p : row) { @@ -104,91 +104,93 @@ void horner::set_interval_for_scalar(interv& a, const rational& v) { interv horner::interval_of_expr(const nex& e) { - TRACE("nla_cn_details", tout << e.type() << " e=" << e << std::endl;); + TRACE("nla_horner_details", tout << e.type() << " e=" << e << std::endl;); interv a; switch (e.type()) { case expr_type::SCALAR: set_interval_for_scalar(a, e.value()); return a; case expr_type::SUM: - return interval_of_sum(e.children()); + return interval_of_sum(e); case expr_type::MUL: - return interval_of_mul(e.children()); + return interval_of_mul(e); case expr_type::VAR: set_var_interval(e.var(), a); return a; default: - TRACE("nla_cn_details", tout << e.type() << "\n";); + TRACE("nla_horner_details", tout << e.type() << "\n";); SASSERT(false); return interv(); } } -template -interv horner::interval_of_mul(const V& es) { +interv horner::interval_of_mul(const nex& e) { + SASSERT(e.is_mul()); + auto & es = e.children(); SASSERT(es.size()); + TRACE("nla_horner_details", tout << "e=" << e << "\n";); interv a = interval_of_expr(es[0]); - // std::cout << "a" << std::endl; - TRACE("nla_cn_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); tout << "\n";); + TRACE("nla_horner_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); ); for (unsigned k = 1; k < es.size(); k++) { interv b = interval_of_expr(es[k]); interv c; interval_deps deps; m_intervals.mul(a, b, c, deps); - m_intervals.set(a, c); + TRACE("nla_horner_details", tout << "c = "; m_intervals.display(tout, c); tout << "\n";); m_intervals.add_deps(a, b, deps, a); - TRACE("nla_cn_details", tout << "es["<< k << "] = " << es[k] << std::endl << "a = "; m_intervals.display(tout, a); tout << "\n";); + m_intervals.set(a, c); + TRACE("nla_horner_details", tout << "es[" << k << "]=" << es[k] << ", a = "; m_intervals.display(tout, a); ); if (m_intervals.is_zero(a)) { - TRACE("nla_cn_details", tout << "got zero\n"; ); + TRACE("nla_horner_details", tout << "got zero\n"; ); break; } } - TRACE("nla_cn_details", - for (const auto &e : es) { - tout << "("<< e << ")"; - } - tout << " interv a = "; - m_intervals.display(tout, a) << "\n";); + TRACE("nla_horner_details", tout << "e=" << e << "\n"; + tout << " interv = "; m_intervals.display(tout, a);); return a; } -template -interv horner::interval_of_sum(const V& es) { +interv horner::interval_of_sum(const nex& e) { + TRACE("nla_horner_details", tout << "e=" << e << "\n";); + SASSERT(e.is_sum()); + auto & es = e.children(); interv a = interval_of_expr(es[0]); - TRACE("nla_cn_details", tout << "es[0]= " << es[0] << "\n"; m_intervals.display(tout, a) << "\n";); if (m_intervals.is_inf(a)) { + TRACE("nla_horner_details", tout << "e=" << e << "\n"; + tout << " interv = "; m_intervals.display(tout, a);); return a; } for (unsigned k = 1; k < es.size(); k++) { - TRACE("nla_cn_details", tout << "es[" << k << "]= " << es[k] << "\n";); + TRACE("nla_horner_details_sum", tout << "es[" << k << "]= " << es[k] << "\n";); interv b = interval_of_expr(es[k]); if (m_intervals.is_inf(b)) { - TRACE("nla_cn_details", tout << "got inf\n";); + TRACE("nla_horner_details", tout << "got inf\n";); return b; } interv c; interval_deps deps; - TRACE("nla_cn_details", tout << "a = "; m_intervals.display(tout, a) << "\nb = "; m_intervals.display(tout, b) << "\n";); + TRACE("nla_horner_details_sum", tout << "a = "; m_intervals.display(tout, a) << "\nb = "; m_intervals.display(tout, b) << "\n";); m_intervals.add(a, b, c, deps); - TRACE("nla_cn_details", tout << "c = "; m_intervals.display(tout, c); tout << "\n";); - m_intervals.set(a, c); - TRACE("nla_cn_details", tout << "a = "; m_intervals.display(tout, a); tout << "\n";); - + TRACE("nla_horner_details", tout << "c = "; m_intervals.display(tout, c); tout << "\n";); m_intervals.add_deps(a, b, deps, a); - TRACE("nla_cn_details", tout << "final a with deps = "; m_intervals.display(tout, a); tout << "\n";); + m_intervals.set(a, c); + TRACE("nla_horner_details_sum", tout << "a = "; m_intervals.display(tout, a); tout << "\n";); + + // m_intervals.add_deps(a, b, deps, a); + TRACE("nla_horner_details", tout << "final a with deps = "; m_intervals.display(tout, a); tout << "\n";); if (m_intervals.is_inf(a)) { - TRACE("nla_cn_details", tout << "got infinity\n";); + TRACE("nla_horner_details", tout << "got infinity\n";); return a; } } + TRACE("nla_horner_details", tout << "e=" << e << "\n"; + tout << " interv = "; m_intervals.display(tout, a);); return a; } // 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_details", tout << "v = "; print_var(v, tout) << "\n"; m_intervals.display(tout, b)<< '\n';); - + m_intervals.set_var_interval_with_deps(v, b); + TRACE("nla_horner_details", tout << "v = "; print_var(v, tout) << "\n"; m_intervals.display(tout, b);); } } diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index a74978c5e..e45a92512 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -41,10 +41,8 @@ public: intervals::interval interval_of_expr(const nex& e); nex nexvar(lpvar j) const; - template // V is a vector of expressions - intervals::interval interval_of_sum(const V&); - template // V is a vector of expressions - intervals::interval interval_of_mul(const V&); + intervals::interval interval_of_sum(const nex&); + intervals::interval interval_of_mul(const nex&); void set_interval_for_scalar(intervals::interval&, const rational&); void set_var_interval(lpvar j, intervals::interval&); std::set get_vars_of_expr(const nex &) const; diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 045a52eac..e2baa8f44 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -94,10 +94,9 @@ std::ostream& intervals::display(std::ostream& out, const interval& i) const { m_dep_manager.linearize(i.m_upper_dep, expl); { lp::explanation e(expl); - out << "\n)\nupper constraints (\n"; + out << "upper constraints\n"; m_core->print_explanation(e, out); } - out << ")\n"; return out; } diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index fe6107e13..2c2865bd7 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -75,12 +75,11 @@ class intervals : common { void add_deps(interval const& a, interval const& b, interval_deps const& deps, interval& i) const { - ci_dependency* lo = mk_dependency(a, b, deps.m_lower_deps); - ci_dependency* hi = mk_dependency(a, b, deps.m_upper_deps); - i.m_lower_dep = lo; - i.m_upper_dep = hi; + i.m_lower_dep = mk_dependency(a, b, deps.m_lower_deps); + i.m_upper_dep = mk_dependency(a, b, deps.m_upper_deps); } - + + // Should be NOOPs for precise mpq types. // For imprecise types (e.g., floats) it should set the rounding mode. void round_to_minus_inf() {} @@ -149,13 +148,7 @@ public: typedef interval_manager::interval interval; private: void set_var_interval(lpvar v, interval & b) const; - - void set_var_interval_signs(lpvar v, interval & b) const; - - void set_var_interval_deps(lpvar v, interval & b) const; - ci_dependency* mk_dep(lp::constraint_index ci) const; - lp::lar_solver& ls(); const lp::lar_solver& ls() const; public: @@ -167,8 +160,6 @@ public: m_imanager(lim, im_config(m_num_manager, m_dep_manager)) {} interval mul(const svector&) const; - interval mul_signs(const svector&) const; - interval mul_signs_with_deps(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_explanations(const svector &, std::ostream&) const;