From 519bbc5af1bea8101a02d60fcc4c6ccde813734e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 16 Dec 2019 13:46:57 -1000 Subject: [PATCH] reshaffle the template definitions from nla_interval.h to nla_interval.cpp Signed-off-by: Lev Nachmanson --- src/math/lp/nla_core.h | 2 + src/math/lp/nla_intervals.cpp | 206 ++++++++++++++++++++++++++++++++++ src/math/lp/nla_intervals.h | 201 ++------------------------------- 3 files changed, 216 insertions(+), 193 deletions(-) diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index fcab27135..f5bd8d6d9 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -30,6 +30,8 @@ #include "math/lp/nex.h" #include "math/lp/horner.h" #include "math/lp/nla_grobner.h" +#include "math/lp/nla_intervals.h" + namespace nla { template diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 5d32ce680..7cdf9cb2e 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -5,6 +5,8 @@ namespace nla { +typedef intervals::interval interv; +typedef enum intervals::with_deps_t e_with_deps; void intervals::set_interval_for_scalar(interv& a, const rational& v) { set_lower(a, v); @@ -292,6 +294,210 @@ std::ostream& intervals::display(std::ostream& out, const interval& i) const { return out; } +template +void intervals::set_var_interval(lpvar v, interval& b) const { + TRACE("nla_intervals_details", m_core->print_var(v, tout) << "\n";); + lp::constraint_index ci; + rational val; + bool is_strict; + if (ls().has_lower_bound(v, ci, val, is_strict)) { + m_config.set_lower(b, val); + m_config.set_lower_is_open(b, is_strict); + m_config.set_lower_is_inf(b, false); + if (wd == with_deps) b.m_lower_dep = mk_dep(ci); + } + else { + m_config.set_lower_is_open(b, true); + m_config.set_lower_is_inf(b, true); + if (wd == with_deps) b.m_lower_dep = nullptr; + } + if (ls().has_upper_bound(v, ci, val, is_strict)) { + m_config.set_upper(b, val); + m_config.set_upper_is_open(b, is_strict); + m_config.set_upper_is_inf(b, false); + if (wd == with_deps) b.m_upper_dep = mk_dep(ci); + } + else { + m_config.set_upper_is_open(b, true); + m_config.set_upper_is_inf(b, true); + if (wd == with_deps) b.m_upper_dep = nullptr; + } +} + +template +bool intervals::interval_from_term(const nex& e, interv& i) const { + rational a, b; + lp::lar_term norm_t = expression_to_normalized_term(&e.to_sum(), a, b); + lp::explanation exp; + if (m_core->explain_by_equiv(norm_t, exp)) { + set_zero_interval(i); + TRACE("nla_intervals", tout << "explain_by_equiv\n";); + return true; + } + lpvar j = find_term_column(norm_t, a); + if (j + 1 == 0) + return false; + + set_var_interval(j, i); + interv bi; + mul(a, i, bi); + add(b, bi); + set(i, bi); + + TRACE("nla_intervals", + m_core->m_lar_solver.print_column_info(j, tout) << "\n"; + tout << "a=" << a << ", b=" << b << "\n"; + tout << e << ", interval = "; display(tout, i);); + return true; +} + +template +interv intervals::interval_of_sum_no_term(const nex_sum& e) { + const nex* inf_e = get_inf_interval_child(e); + if (inf_e) { + return interv(); + } + interv a = interval_of_expr(e[0], 1); + for (unsigned k = 1; k < e.size(); k++) { + TRACE("nla_intervals_details_sum", tout << "e[" << k << "]= " << *e[k] << "\n";); + interv b = interval_of_expr(e[k], 1); + interv c; + + TRACE("nla_intervals_details_sum", tout << "a = "; display(tout, a) << "\nb = "; display(tout, b) << "\n";); + if (wd == with_deps) { + interval_deps_combine_rule combine_rule; + add(a, b, c, combine_rule); + combine_deps(a, b, combine_rule, c); + } + else { + add(a, b, c); + } + set(a, c); + TRACE("nla_intervals_details_sum", tout << *e[k] << ", "; + display(tout, a); tout << "\n";); + } + TRACE("nla_intervals_details", tout << "e=" << e << "\n"; + tout << " interv = "; display(tout, a);); + return a; +} + +template +void intervals::update_upper_for_intersection(const interval& a, const interval& b, interval& i) const { + if (a.m_upper_inf) { + if (b.m_upper_inf) + return; + copy_upper_bound(b, i); + return; + } + if (b.m_upper_inf) { + SASSERT(!a.m_upper_inf); + copy_upper_bound(a, i); + return; + } + if (m_num_manager.gt(a.m_upper, b.m_upper)) { + copy_upper_bound(b, i); + return; + } + if (m_num_manager.lt(a.m_upper, b.m_upper)) { + copy_upper_bound(a, i); + return; + } + SASSERT(m_num_manager.eq(a.m_upper, b.m_upper)); + if (a.m_upper_open) { // we might consider to look at b.m_upper_open too here + copy_upper_bound(a, i); + return; + } + + copy_upper_bound(b, i); +} + +template +interv intervals::interval_of_sum(const nex_sum& e) { + TRACE("nla_intervals_details", tout << "e=" << e << "\n";); + interv i_e = interval_of_sum_no_term(e); + if (e.is_a_linear_term()) { + SASSERT(e.is_sum() && e.size() > 1); + interv i_from_term; + if (interval_from_term(e, i_from_term)) { + interv r = intersect(i_e, i_from_term); + TRACE("nla_intervals_details", tout << "intersection="; display(tout, r) << "\n";); + if (is_empty(r)) { + SASSERT(false); // not implemented + } + return r; + + } + } + return i_e; +} + +template +interv intervals::interval_of_mul(const nex_mul& e) { + TRACE("nla_intervals_details", tout << "e = " << e << "\n";); + const nex* zero_interval_child = get_zero_interval_child(e); + if (zero_interval_child) { + interv a = interval_of_expr(zero_interval_child, 1); + set_zero_interval_deps_for_mult(a); + TRACE("nla_intervals_details", tout << "zero_interval_child = " << *zero_interval_child << std::endl << "a = "; display(tout, a); ); + return a; + } + + interv a; + set_interval_for_scalar(a, e.coeff()); + TRACE("nla_intervals_details", tout << "a = "; display(tout, a); ); + for (const auto& ep : e) { + interv b = interval_of_expr(ep.e(), ep.pow()); + TRACE("nla_intervals_details", tout << "ep = " << ep << ", "; display(tout, b); ); + interv c; + interval_deps_combine_rule comb_rule; + mul_two_intervals(a, b, c, comb_rule); + TRACE("nla_intervals_details", tout << "c before combine_deps() "; display(tout, c);); + combine_deps(a, b, comb_rule, c); + TRACE("nla_intervals_details", tout << "a "; display(tout, a);); + TRACE("nla_intervals_details", tout << "c "; display(tout, c);); + set(a, c); + TRACE("nla_intervals_details", tout << "part mult "; display(tout, a);); + } + TRACE("nla_intervals_details", tout << "e=" << e << "\n"; + tout << " return "; display(tout, a);); + return a; +} + +template +interv intervals::interval_of_expr(const nex* e, unsigned p) { + interv a; + switch (e->type()) { + case expr_type::SCALAR: + set_interval_for_scalar(a, to_scalar(e)->value()); + if (p != 1) { + return power(a, p); + } + return a; + case expr_type::SUM: { + interv b = interval_of_sum(e->to_sum()); + if (p != 1) + return power(b, p); + return b; + } + case expr_type::MUL: { + interv b = interval_of_mul(e->to_mul()); + if (p != 1) + return power(b, p); + return b; + } + case expr_type::VAR: + set_var_interval(e->to_var().var(), a); + if (p != 1) + return power(a, p);; + return a; + default: + TRACE("nla_intervals_details", tout << e->type() << "\n";); + UNREACHABLE(); + return interval(); + } +} + + lp::lar_solver& intervals::ls() { return m_core->m_lar_solver; } const lp::lar_solver& intervals::ls() const { return m_core->m_lar_solver; } diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 881e38ad4..82d07b104 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -25,7 +25,6 @@ #include "math/interval/interval.h" #include "util/dependency.h" - namespace nla { class core; @@ -297,66 +296,11 @@ public: } template - void set_var_interval(lpvar v, interval& b) const { - TRACE("nla_intervals_details", m_core->print_var(v, tout) << "\n";); - lp::constraint_index ci; - rational val; - bool is_strict; - if (ls().has_lower_bound(v, ci, val, is_strict)) { - m_config.set_lower(b, val); - m_config.set_lower_is_open(b, is_strict); - m_config.set_lower_is_inf(b, false); - if (wd == with_deps) b.m_lower_dep = mk_dep(ci); - } - else { - m_config.set_lower_is_open(b, true); - m_config.set_lower_is_inf(b, true); - if (wd == with_deps) b.m_lower_dep = nullptr; - } - if (ls().has_upper_bound(v, ci, val, is_strict)) { - m_config.set_upper(b, val); - m_config.set_upper_is_open(b, is_strict); - m_config.set_upper_is_inf(b, false); - if (wd == with_deps) b.m_upper_dep = mk_dep(ci); - } - else { - m_config.set_upper_is_open(b, true); - m_config.set_upper_is_inf(b, true); - if (wd == with_deps) b.m_upper_dep = nullptr; - } - } - + void set_var_interval(lpvar v, interval& b) const; template - void update_upper_for_intersection(const interval& a, const interval& b, interval& i) const { - if (a.m_upper_inf) { - if (b.m_upper_inf) - return; - copy_upper_bound(b, i); - return; - } - if (b.m_upper_inf) { - SASSERT(!a.m_upper_inf); - copy_upper_bound(a, i); - return; - } - if (m_num_manager.gt(a.m_upper, b.m_upper)) { - copy_upper_bound(b, i); - return; - } - if (m_num_manager.lt(a.m_upper, b.m_upper)) { - copy_upper_bound(a, i); - return; - } - SASSERT(m_num_manager.eq(a.m_upper, b.m_upper)); - if (a.m_upper_open) { // we might consider to look at b.m_upper_open too here - copy_upper_bound(a, i); - return; - } - - copy_upper_bound(b, i); - } - + void update_upper_for_intersection(const interval& a, const interval& b, interval& i) const; + template interval intersect(const interval& a, const interval& b) const { interval i; @@ -369,148 +313,19 @@ public: } template - bool interval_from_term(const nex& e, interval& i) const { - rational a, b; - lp::lar_term norm_t = expression_to_normalized_term(&e.to_sum(), a, b); - lp::explanation exp; - if (m_core->explain_by_equiv(norm_t, exp)) { - set_zero_interval(i); - TRACE("nla_intervals", tout << "explain_by_equiv\n";); - return true; - } - lpvar j = find_term_column(norm_t, a); - if (j + 1 == 0) - return false; - - set_var_interval(j, i); - interv bi; - mul(a, i, bi); - add(b, bi); - set(i, bi); - - TRACE("nla_intervals", - m_core->m_lar_solver.print_column_info(j, tout) << "\n"; - tout << "a=" << a << ", b=" << b << "\n"; - tout << e << ", interval = "; display(tout, i);); - return true; - } + bool interval_from_term(const nex& e, interval& i) const; template - interval interval_of_sum_no_term(const nex_sum& e) { - const nex* inf_e = get_inf_interval_child(e); - if (inf_e) { - return interv(); - } - interv a = interval_of_expr(e[0], 1); - for (unsigned k = 1; k < e.size(); k++) { - TRACE("nla_intervals_details_sum", tout << "e[" << k << "]= " << *e[k] << "\n";); - interv b = interval_of_expr(e[k], 1); - interv c; - - TRACE("nla_intervals_details_sum", tout << "a = "; display(tout, a) << "\nb = "; display(tout, b) << "\n";); - if (wd == with_deps) { - interval_deps_combine_rule combine_rule; - add(a, b, c, combine_rule); - combine_deps(a, b, combine_rule, c); - } - else { - add(a, b, c); - } - set(a, c); - TRACE("nla_intervals_details_sum", tout << *e[k] << ", "; - display(tout, a); tout << "\n";); - } - TRACE("nla_intervals_details", tout << "e=" << e << "\n"; - tout << " interv = "; display(tout, a);); - return a; - } + interval interval_of_sum_no_term(const nex_sum& e); template - interval interval_of_sum(const nex_sum& e) { - TRACE("nla_intervals_details", tout << "e=" << e << "\n";); - interv i_e = interval_of_sum_no_term(e); - if (e.is_a_linear_term()) { - SASSERT(e.is_sum() && e.size() > 1); - interv i_from_term; - if (interval_from_term(e, i_from_term)) { - interv r = intersect(i_e, i_from_term); - TRACE("nla_intervals_details", tout << "intersection="; display(tout, r) << "\n";); - if (is_empty(r)) { - SASSERT(false); // not implemented - } - return r; - - } - } - return i_e; - } + interval interval_of_sum(const nex_sum& e); template - interval interval_of_mul(const nex_mul& e) { - TRACE("nla_intervals_details", tout << "e = " << e << "\n";); - const nex* zero_interval_child = get_zero_interval_child(e); - if (zero_interval_child) { - interv a = interval_of_expr(zero_interval_child, 1); - set_zero_interval_deps_for_mult(a); - TRACE("nla_intervals_details", tout << "zero_interval_child = " << *zero_interval_child << std::endl << "a = "; display(tout, a); ); - return a; - } - - interv a; - set_interval_for_scalar(a, e.coeff()); - TRACE("nla_intervals_details", tout << "a = "; display(tout, a); ); - for (const auto& ep : e) { - interv b = interval_of_expr(ep.e(), ep.pow()); - TRACE("nla_intervals_details", tout << "ep = " << ep << ", "; display(tout, b); ); - interv c; - interval_deps_combine_rule comb_rule; - mul_two_intervals(a, b, c, comb_rule); - TRACE("nla_intervals_details", tout << "c before combine_deps() "; display(tout, c);); - combine_deps(a, b, comb_rule, c); - TRACE("nla_intervals_details", tout << "a "; display(tout, a);); - TRACE("nla_intervals_details", tout << "c "; display(tout, c);); - set(a, c); - TRACE("nla_intervals_details", tout << "part mult "; display(tout, a);); - } - TRACE("nla_intervals_details", tout << "e=" << e << "\n"; - tout << " return "; display(tout, a);); - return a; - } + interval interval_of_mul(const nex_mul& e); template - interval interval_of_expr(const nex* e, unsigned p) { - interv a; - switch (e->type()) { - case expr_type::SCALAR: - set_interval_for_scalar(a, to_scalar(e)->value()); - if (p != 1) { - return power(a, p); - } - return a; - case expr_type::SUM: { - interv b = interval_of_sum(e->to_sum()); - if (p != 1) - return power(b, p); - return b; - } - case expr_type::MUL: { - interv b = interval_of_mul(e->to_mul()); - if (p != 1) - return power(b, p); - return b; - } - case expr_type::VAR: - set_var_interval(e->to_var().var(), a); - if (p != 1) - return power(a, p);; - return a; - default: - TRACE("nla_intervals_details", tout << e->type() << "\n";); - UNREACHABLE(); - return interval(); - } - } - + interval interval_of_expr(const nex* e, unsigned p); bool upper_is_inf(const interval& a) const { return m_config.upper_is_inf(a); } bool lower_is_inf(const interval& a) const { return m_config.lower_is_inf(a); }