From 9b3ebfdd2a2966467467f89e3a823c8451409d23 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 28 Oct 2019 16:47:53 -0700 Subject: [PATCH] move interval functionality from horner to intervals Signed-off-by: Lev Nachmanson --- src/math/lp/horner.cpp | 454 +--------------------------------- src/math/lp/horner.h | 20 -- src/math/lp/nla_intervals.cpp | 453 +++++++++++++++++++++++++++++++++ src/math/lp/nla_intervals.h | 23 ++ 4 files changed, 477 insertions(+), 473 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 2e4f1d911..1058987eb 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -69,28 +69,11 @@ bool horner::lemmas_on_expr(cross_nested& cn, nex_sum* e) { return cn.done(); } -bool horner::check_cross_nested_expr(const nex* n) { - TRACE("nla_horner", tout << "cross-nested n = " << *n << ", n->type() == " << n->type() << "\n";); - c().lp_settings().stats().m_cross_nested_forms++; - - auto i = interval_of_expr(n, 1); - TRACE("nla_horner", tout << "callback n = " << *n << "\ni="; m_intervals.display(tout, i) << "\n";); - if (!m_intervals.separated_from_zero(i)) { - m_intervals.reset(); - return false; - } - auto interv_wd = interval_of_expr_with_deps(n, 1); - TRACE("nla_horner", tout << "conflict: interv_wd = "; m_intervals.display(tout, interv_wd ) << *n << "\n";); - ci_dependency* dep = m_fixed_as_scalars? get_fixed_vars_dep_from_row(c().m_lar_solver.A_r().m_rows[m_row_index], m_intervals.dep_manager()) : nullptr; - m_intervals.check_interval_for_conflict_on_zero(interv_wd, dep); - m_intervals.reset(); // clean the memory allocated by the interval bound dependencies - return true; -} template bool horner::lemmas_on_row(const T& row) { cross_nested cn( - [this](const nex* n) { return check_cross_nested_expr(n); }, + [this](const nex* n) { return m_intervals.check_cross_nested_expr(n, m_fixed_as_scalars? get_fixed_vars_dep_from_row(c().m_lar_solver.A_r().m_rows[m_row_index], m_intervals.dep_manager()) : nullptr); }, [this](unsigned j) { return c().var_is_fixed(j); }, [this]() { return c().random(); }, m_nex_creator); @@ -140,444 +123,9 @@ void horner::horner_lemmas() { } -void horner::set_interval_for_scalar(interv& a, const rational& 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); -} - -interv horner::power_with_deps(const interv& a, unsigned n) { - interv b; - interval_deps_combine_rule combine_rule; - m_intervals.power(a, n, b, combine_rule); - m_intervals.combine_deps(a, combine_rule, b); - TRACE("nla_horner_details", tout << "power of "; m_intervals.display(tout, a) << " = "; - m_intervals.display(tout, b) << "\n"; ); - - return b; -} - -interv horner::interval_of_expr_with_deps(const nex* e, unsigned power) { - interv a; - switch (e->type()) { - case expr_type::SCALAR: - set_interval_for_scalar(a, to_scalar(e)->value()); - if (power != 1) { - return power_with_deps(a, power); - } - return a; - case expr_type::SUM: - { - interv b = interval_of_sum_with_deps(to_sum(e)); - if (power != 1) - return power_with_deps(b, power); - return b; - } - case expr_type::MUL: - { - interv b = interval_of_mul_with_deps(to_mul(e)); - if (power != 1) - return power_with_deps(b, power);; - return b; - } - case expr_type::VAR: - set_var_interval_with_deps(to_var(e)->var(), a); - if (power != 1) - return power_with_deps(a, power);; - return a; - default: - TRACE("nla_horner_details", tout << e->type() << "\n";); - SASSERT(false); - return interv(); - } -} - -interv horner::interval_of_expr(const nex* e, unsigned power) { - TRACE("nla_horner_details", tout << "e = " << *e << "\n";); - interv a; - switch (e->type()) { - case expr_type::SCALAR: - set_interval_for_scalar(a, to_scalar(e)->value()); - break; - case expr_type::SUM: - { - interv b = interval_of_sum(to_sum(e)); - if (power != 1) { - return power_with_deps(b, power);; - } - return b; - } - case expr_type::MUL: - { - interv b = interval_of_mul(to_mul(e)); - if (power != 1) { - return power_with_deps(b, power);; - } - return b; - } - case expr_type::VAR: - set_var_interval(to_var(e)->var(), a); - break; - default: - TRACE("nla_horner_details", tout << e->type() << "\n";); - SASSERT(false); - return interv(); - } - if (power != 1) { - return power_with_deps(a, power);; - } - return a; -} -interv horner::interval_of_mul_with_deps(const nex_mul* e) { - const nex * zero_interval_child = get_zero_interval_child(e); - if (zero_interval_child) { - interv a = interval_of_expr_with_deps(zero_interval_child, 1); - m_intervals.set_zero_interval_deps_for_mult(a); - TRACE("nla_horner_details", tout << "zero_interval_child = "<< *zero_interval_child << std::endl << "a = "; m_intervals.display(tout, a); ); - return a; - } - - SASSERT(e->is_mul()); - interv a; - set_interval_for_scalar(a, e->coeff()); - TRACE("nla_horner_details", tout << "a = "; m_intervals.display(tout, a); ); - for (const auto & ep : *e) { - interv b = interval_of_expr_with_deps(ep.e(), ep.pow()); - TRACE("nla_horner_details", tout << "ep = " << ep << ", "; m_intervals.display(tout, b); ); - interv c; - interval_deps_combine_rule comb_rule; - m_intervals.mul_two_intervals(a, b, c, comb_rule); - TRACE("nla_horner_details", tout << "c before combine_deps() "; m_intervals.display(tout, c);); - m_intervals.combine_deps(a, b, comb_rule, c); - TRACE("nla_horner_details", tout << "a "; m_intervals.display(tout, a);); - TRACE("nla_horner_details", tout << "c "; m_intervals.display(tout, c);); - m_intervals.set_with_deps(a, c); - TRACE("nla_horner_details", tout << "part mult "; m_intervals.display(tout, a);); - } - TRACE("nla_horner_details", tout << "e=" << *e << "\n"; - tout << " return "; m_intervals.display(tout, a);); - return a; -} -interv horner::interval_of_mul(const nex_mul* e) { - TRACE("nla_horner_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); - m_intervals.set_zero_interval_deps_for_mult(a); - TRACE("nla_horner_details", tout << "zero_interval_child = "<< *zero_interval_child << std::endl << "a = "; m_intervals.display(tout, a); ); - return a; - } - - interv a; - - set_interval_for_scalar(a, e->coeff()); - TRACE("nla_horner_details", tout << "a = "; m_intervals.display(tout, a); ); - for (const auto & ep : *e) { - interv b = interval_of_expr(ep.e(), ep.pow() ); - TRACE("nla_horner_details", tout << "ep = " << ep << ", "; m_intervals.display(tout, b); ); - interv c; - interval_deps_combine_rule comb_rule; - m_intervals.mul_two_intervals(a, b, c, comb_rule); - TRACE("nla_horner_details", tout << "c before combine_deps() "; m_intervals.display(tout, c);); - m_intervals.combine_deps(a, b, comb_rule, c); - TRACE("nla_horner_details", tout << "a "; m_intervals.display(tout, a);); - TRACE("nla_horner_details", tout << "c "; m_intervals.display(tout, c);); - m_intervals.set(a, c, 33); - TRACE("nla_horner_details", tout << "part mult "; m_intervals.display(tout, a);); - } - TRACE("nla_horner_details", tout << "e=" << *e << "\n"; - tout << " return "; m_intervals.display(tout, a);); - return a; -} - - -void horner::add_mul_of_degree_one_to_vector(const nex_mul* e, vector> &v) { - TRACE("nla_horner_details", tout << *e << "\n";); - SASSERT(e->size() == 1); - SASSERT((*e)[0].pow() == 1); - const nex *ev = (*e)[0].e(); - lpvar j = to_var(ev)->var(); - v.push_back(std::make_pair(e->coeff(), j)); -} - -void horner::add_linear_to_vector(const nex* e, vector> &v) { - TRACE("nla_horner_details", tout << *e << "\n";); - switch (e->type()) { - case expr_type::MUL: - add_mul_of_degree_one_to_vector(to_mul(e), v); - break; - case expr_type::VAR: - v.push_back(std::make_pair(rational(1), to_var(e)->var())); - break; - default: - SASSERT(!e->is_sum()); - // noop - } -} -// e = a * can_t + b -lp::lar_term horner::expression_to_normalized_term(const nex_sum* e, rational& a, rational& b) { - TRACE("nla_horner_details", tout << *e << "\n";); - lpvar smallest_j; - vector> v; - b = rational(0); - unsigned a_index; - for (const nex* c : e->children()) { - if (c->is_scalar()) { - b += to_scalar(c)->value(); - } else { - add_linear_to_vector(c, v); - if (v.empty()) - continue; - if (v.size() == 1 || smallest_j > v.back().second) { - smallest_j = v.back().second; - a_index = v.size() - 1; - } - } - } - TRACE("nla_horner_details", tout << "a_index = " << a_index << ", v="; print_vector(v, tout) << "\n";); - a = v[a_index].first; - lp::lar_term t; - - if (a.is_one()) { - for (unsigned k = 0; k < v.size(); k++) { - auto& p = v[k]; - t.add_coeff_var(p.first, p.second); - } - } else { - for (unsigned k = 0; k < v.size(); k++) { - auto& p = v[k]; - if (k != a_index) - t.add_coeff_var(p.first/a, p.second); - else - t.add_var(p.second); - } - } - TRACE("nla_horner_details", tout << a << "* ("; - lp::lar_solver::print_term_as_indices(t, tout) << ") + " << b << std::endl;); - SASSERT(t.is_normalized()); - return t; -} - -bool horner::mul_has_inf_interval(const nex_mul* e) const { - bool has_inf = false; - for (const auto & p : e->children()) { - const nex *c = p.e(); - if (!c->is_elementary()) - return false; - if (has_zero_interval(c)) - return false; - has_inf |= has_inf_interval(c); - } - return has_inf; -} - -bool horner::has_inf_interval(const nex* e) const { - if (e->is_var()) - return c().no_bounds(to_var(e)->var()); - if (e->is_mul()) { - return mul_has_inf_interval(to_mul(e)); - } - if (e->is_scalar()) - return false; - for (auto * c : to_sum(e)->children()) { - if (has_inf_interval(c)) - return true; - } - return false; -} - -bool horner::has_zero_interval(const nex* e) const { - SASSERT(!e->is_scalar() || !to_scalar(e)->value().is_zero()); - if (! e->is_var()) - return false; - return c().var_is_fixed_to_zero(to_var(e)->var()); -} - -const nex* horner::get_zero_interval_child(const nex_mul* e) const { - for (const auto & p : e->children()) { - const nex * c = p.e(); - if (has_zero_interval(c)) - return c; - } - return nullptr; -} - -const nex* horner::get_inf_interval_child(const nex_sum* e) const { - for (auto * c : e->children()) { - if (has_inf_interval(c)) - return c; - } - return nullptr; -} - -// we should have in the case of found a * m_terms[k] + b = e, -// where m_terms[k] corresponds to the returned lpvar -lpvar horner::find_term_column(const lp::lar_term & norm_t, rational& a) const { - std::pair a_j; - if (c().m_lar_solver.fetch_normalized_term_column(norm_t, a_j)) { - a /= a_j.first; - return a_j.second; - } - return -1; -} - -interv horner::interval_of_sum_no_term_with_deps(const nex_sum* e) { - const nex* inf_e = get_inf_interval_child(e); - if (inf_e) { - return interv(); - } - auto & es = e->children(); - interv a = interval_of_expr_with_deps(es[0], 1); - for (unsigned k = 1; k < es.size(); k++) { - TRACE("nla_horner_details_sum", tout << "es[" << k << "]= " << *es[k] << "\n";); - interv b = interval_of_expr_with_deps(es[k], 1); - interv c; - interval_deps_combine_rule combine_rule; - 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, combine_rule); - m_intervals.combine_deps(a, b, combine_rule, c); - m_intervals.set_with_deps(a, c); - TRACE("nla_horner_details_sum", tout << *es[k] << ", "; - m_intervals.display(tout, a); tout << "\n";); - } - TRACE("nla_horner_details", tout << "e=" << *e << "\n"; - tout << " interv = "; m_intervals.display(tout, a);); - return a; -} - -interv horner::interval_of_sum_no_term(const nex_sum* e) { - const nex* inf_e = get_inf_interval_child(e); - if (inf_e) { - return interv(); - } - auto & es = e->children(); - interv a = interval_of_expr(es[0], 1); - for (unsigned k = 1; k < es.size(); k++) { - TRACE("nla_horner_details_sum", tout << "es[" << k << "]= " << *es[k] << "\n";); - interv b = interval_of_expr(es[k], 1); - interv c; - interval_deps_combine_rule combine_rule; - 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, combine_rule); - m_intervals.combine_deps(a, b, combine_rule, c); - m_intervals.set(a, c, 22); - TRACE("nla_horner_details_sum", tout << *es[k] << ", "; - m_intervals.display(tout, a); tout << "\n";); - } - TRACE("nla_horner_details", tout << "e=" << *e << "\n"; - tout << " interv = "; m_intervals.display(tout, a);); - return a; -} - -bool horner::interval_from_term_with_deps(const nex* e, interv & i) const { - rational a, b; - lp::lar_term norm_t = expression_to_normalized_term(to_sum(e), a, b); - lp::explanation exp; - if (c().explain_by_equiv(norm_t, exp)) { - m_intervals.set_zero_interval_with_explanation(i, exp); - TRACE("nla_horner", tout << "explain_by_equiv\n";); - return true; - } - lpvar j = find_term_column(norm_t, a); - if (j + 1 == 0) - return false; - - set_var_interval_with_deps(j, i); - interv bi; - m_intervals.mul_with_deps(a, i, bi); - m_intervals.add(b, bi); - m_intervals.set_with_deps(i, bi); - - TRACE("nla_horner", - c().m_lar_solver.print_column_info(j, tout) << "\n"; - tout << "a=" << a << ", b=" << b << "\n"; - tout << *e << ", interval = "; m_intervals.display(tout, i);); - return true; -} - -bool horner::interval_from_term(const nex* e, interv & i) const { - rational a, b; - lp::lar_term norm_t = expression_to_normalized_term(to_sum(e), a, b); - lp::explanation exp; - if (c().explain_by_equiv(norm_t, exp)) { - m_intervals.set_zero_interval(i); - TRACE("nla_horner", 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; - m_intervals.mul_no_deps(a, i, bi); - m_intervals.add(b, bi); - m_intervals.set(i, bi, 44); - - TRACE("nla_horner", - c().m_lar_solver.print_column_info(j, tout) << "\n"; - tout << "a=" << a << ", b=" << b << "\n"; - tout << *e << ", interval = "; m_intervals.display(tout, i);); - return true; - -} - - -interv horner::interval_of_sum_with_deps(const nex_sum* e) { - TRACE("nla_horner_details", tout << "e=" << *e << "\n";); - interv i_e = interval_of_sum_no_term_with_deps(e); - if (e->is_a_linear_term()) { - SASSERT(e->is_sum() && e->size() > 1); - interv i_from_term ; - if (interval_from_term_with_deps(e, i_from_term)) { - interv r = m_intervals.intersect_with_deps(i_e, i_from_term); - TRACE("nla_horner_details", tout << "intersection="; m_intervals.display(tout, r) << "\n";); - if (m_intervals.is_empty(r)) { - SASSERT(false); // not implemented - } - return r; - - } - } - return i_e; -} - -interv horner::interval_of_sum(const nex_sum* e) { - interv i_e = interval_of_sum_no_term(e); - TRACE("nla_horner_details", tout << "e=" << *e << "\ni_e="; m_intervals.display(tout, i_e) << "\n";); - 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)) { - TRACE("nla_horner_details", tout << "i_from_term="; m_intervals.display(tout, i_from_term) << "\n";); - interv r = m_intervals.intersect(i_e, i_from_term, 44); - TRACE("nla_horner_details", tout << "intersection="; m_intervals.display(tout, r) << "\n";); - if (m_intervals.is_empty(r)) { - SASSERT(false); // not implemented - } - return r; - - } - } - return i_e; -} - -// sets the dependencies also -void horner::set_var_interval_with_deps(lpvar v, interv& b) const{ - m_intervals.set_var_interval_with_deps(v, b); - TRACE("nla_horner_details_var", tout << "v = "; print_var(v, tout) << "\n"; m_intervals.display(tout, b);); -} - -void horner::set_var_interval(lpvar v, interv& b) const{ - m_intervals.set_var_interval(v, b); - TRACE("nla_horner_details_var", 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 d3b24de35..371280d5f 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -41,35 +41,15 @@ public: template // T has an iterator of (coeff(), var()) bool lemmas_on_row(const T&); template bool row_is_interesting(const T&) const; - intervals::interval interval_of_expr_with_deps(const nex* e, unsigned power); - intervals::interval interval_of_expr(const nex* e, unsigned power); - intervals::interval interval_of_sum(const nex_sum*); - intervals::interval interval_of_sum_no_term(const nex_sum*); - intervals::interval interval_of_mul(const nex_mul*); - void set_interval_for_scalar(intervals::interval&, const rational&); - void set_var_interval(lpvar j, intervals::interval&) const; - bool interval_from_term(const nex* e, interv&) const; intervals::interval interval_of_sum_with_deps(const nex_sum*); intervals::interval interval_of_sum_no_term_with_deps(const nex_sum*); - intervals::interval interval_of_mul_with_deps(const nex_mul*); void set_var_interval_with_deps(lpvar j, intervals::interval&) const; bool lemmas_on_expr(cross_nested&, nex_sum*); template // T has an iterator of (coeff(), var()) bool row_has_monomial_to_refine(const T&) const; - lpvar find_term_column(const lp::lar_term &, rational & a) const; - static lp::lar_term expression_to_normalized_term(const nex_sum*, rational& a, rational & b); - static void add_linear_to_vector(const nex*, vector> &); - static void add_mul_of_degree_one_to_vector(const nex_mul*, vector> &); bool interval_from_term_with_deps(const nex* e, interv&) const; - const nex* get_zero_interval_child(const nex_mul*) const; - const nex* get_inf_interval_child(const nex_sum*) const; - bool has_zero_interval(const nex* ) const; - bool has_inf_interval(const nex* ) const; - bool mul_has_inf_interval(const nex_mul* ) const; - bool check_cross_nested_expr(const nex*); - interv power_with_deps(const interv& a, unsigned); }; // end of horner } diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 3f719dda9..73c3864c4 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -32,6 +32,459 @@ void intervals::set_var_interval_with_deps(lpvar v, interval& b) const { } } +void intervals::set_interval_for_scalar(interv& a, const rational& v) { + set_lower(a, v); + set_upper(a, v); + set_lower_is_open(a, false); + set_lower_is_inf(a, false); + set_upper_is_open(a, false); + set_upper_is_inf(a, false); +} + + + +intervals::interv intervals::power_with_deps(const interv& a, unsigned n) { + interv b; + interval_deps_combine_rule combine_rule; + power(a, n, b, combine_rule); + combine_deps(a, combine_rule, b); + TRACE("nla_horner_details", tout << "power of "; display(tout, a) << " = "; + display(tout, b) << "\n"; ); + + return b; +} + + +intervals::interv intervals::interval_of_expr_with_deps(const nex* e, unsigned power) { + interv a; + switch (e->type()) { + case expr_type::SCALAR: + set_interval_for_scalar(a, to_scalar(e)->value()); + if (power != 1) { + return power_with_deps(a, power); + } + return a; + case expr_type::SUM: + { + interv b = interval_of_sum_with_deps(to_sum(e)); + if (power != 1) + return power_with_deps(b, power); + return b; + } + case expr_type::MUL: + { + interv b = interval_of_mul_with_deps(to_mul(e)); + if (power != 1) + return power_with_deps(b, power);; + return b; + } + case expr_type::VAR: + set_var_interval_with_deps(to_var(e)->var(), a); + if (power != 1) + return power_with_deps(a, power);; + return a; + default: + TRACE("nla_intervals_details", tout << e->type() << "\n";); + SASSERT(false); + return interv(); + } +} + +intervals::interv intervals::interval_of_expr(const nex* e, unsigned power) { + TRACE("nla_intervals_details", tout << "e = " << *e << "\n";); + interv a; + switch (e->type()) { + case expr_type::SCALAR: + set_interval_for_scalar(a, to_scalar(e)->value()); + break; + case expr_type::SUM: + { + interv b = interval_of_sum(to_sum(e)); + if (power != 1) { + return power_with_deps(b, power);; + } + return b; + } + case expr_type::MUL: + { + interv b = interval_of_mul(to_mul(e)); + if (power != 1) { + return power_with_deps(b, power);; + } + return b; + } + case expr_type::VAR: + set_var_interval(to_var(e)->var(), a); + break; + default: + TRACE("nla_intervals_details", tout << e->type() << "\n";); + SASSERT(false); + return interv(); + } + if (power != 1) { + return power_with_deps(a, power);; + } + return a; +} + +const nex* intervals::get_inf_interval_child(const nex_sum* e) const { + for (auto * c : e->children()) { + if (has_inf_interval(c)) + return c; + } + return nullptr; +} + +bool intervals::mul_has_inf_interval(const nex_mul* e) const { + bool has_inf = false; + for (const auto & p : e->children()) { + const nex *c = p.e(); + if (!c->is_elementary()) + return false; + if (has_zero_interval(c)) + return false; + has_inf |= has_inf_interval(c); + } + return has_inf; +} + +bool intervals::has_inf_interval(const nex* e) const { + if (e->is_var()) + return m_core->no_bounds(to_var(e)->var()); + if (e->is_mul()) { + return mul_has_inf_interval(to_mul(e)); + } + if (e->is_scalar()) + return false; + for (auto * c : to_sum(e)->children()) { + if (has_inf_interval(c)) + return true; + } + return false; +} + +bool intervals::has_zero_interval(const nex* e) const { + SASSERT(!e->is_scalar() || !to_scalar(e)->value().is_zero()); + if (! e->is_var()) + return false; + return m_core->var_is_fixed_to_zero(to_var(e)->var()); +} + +const nex* intervals::get_zero_interval_child(const nex_mul* e) const { + for (const auto & p : e->children()) { + const nex * c = p.e(); + if (has_zero_interval(c)) + return c; + } + return nullptr; +} + + +intervals::interv intervals::interval_of_mul_with_deps(const nex_mul* e) { + const nex * zero_interval_child = get_zero_interval_child(e); + if (zero_interval_child) { + interv a = interval_of_expr_with_deps(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; + } + + SASSERT(e->is_mul()); + 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_with_deps(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_with_deps(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; +} + +intervals::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, 33); + 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; +} + + +bool intervals::check_cross_nested_expr(const nex* n, ci_dependency* initial_deps) { + TRACE("nla_intervals", tout << "cross-nested n = " << *n << ", n->type() == " << n->type() << "\n";); + m_core->lp_settings().stats().m_cross_nested_forms++; + + auto i = interval_of_expr(n, 1); + TRACE("nla_intervals", tout << "callback n = " << *n << "\ni="; display(tout, i) << "\n";); + if (!separated_from_zero(i)) { + reset(); + return false; + } + auto interv_wd = interval_of_expr_with_deps(n, 1); + TRACE("nla_intervals", tout << "conflict: interv_wd = "; display(tout, interv_wd ) << *n << "\n";); + check_interval_for_conflict_on_zero(interv_wd, initial_deps); + reset(); // clean the memory allocated by the interval bound dependencies + return true; +} + +intervals::interv intervals::interval_of_sum_no_term_with_deps(const nex_sum* e) { + const nex* inf_e = get_inf_interval_child(e); + if (inf_e) { + return interv(); + } + auto & es = e->children(); + interv a = interval_of_expr_with_deps(es[0], 1); + for (unsigned k = 1; k < es.size(); k++) { + TRACE("nla_intervals_details_sum", tout << "es[" << k << "]= " << *es[k] << "\n";); + interv b = interval_of_expr_with_deps(es[k], 1); + interv c; + interval_deps_combine_rule combine_rule; + TRACE("nla_intervals_details_sum", tout << "a = "; display(tout, a) << "\nb = "; display(tout, b) << "\n";); + add(a, b, c, combine_rule); + combine_deps(a, b, combine_rule, c); + set_with_deps(a, c); + TRACE("nla_intervals_details_sum", tout << *es[k] << ", "; + display(tout, a); tout << "\n";); + } + TRACE("nla_intervals_details", tout << "e=" << *e << "\n"; + tout << " interv = "; display(tout, a);); + return a; +} + +intervals::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(); + } + auto & es = e->children(); + interv a = interval_of_expr(es[0], 1); + for (unsigned k = 1; k < es.size(); k++) { + TRACE("nla_intervals_details_sum", tout << "es[" << k << "]= " << *es[k] << "\n";); + interv b = interval_of_expr(es[k], 1); + interv c; + interval_deps_combine_rule combine_rule; + TRACE("nla_intervals_details_sum", tout << "a = "; display(tout, a) << "\nb = "; display(tout, b) << "\n";); + add(a, b, c, combine_rule); + combine_deps(a, b, combine_rule, c); + set(a, c, 22); + TRACE("nla_intervals_details_sum", tout << *es[k] << ", "; + display(tout, a); tout << "\n";); + } + TRACE("nla_intervals_details", tout << "e=" << *e << "\n"; + tout << " interv = "; display(tout, a);); + return a; +} + +void intervals::add_mul_of_degree_one_to_vector(const nex_mul* e, vector> &v) { + TRACE("nla_horner_details", tout << *e << "\n";); + SASSERT(e->size() == 1); + SASSERT((*e)[0].pow() == 1); + const nex *ev = (*e)[0].e(); + lpvar j = to_var(ev)->var(); + v.push_back(std::make_pair(e->coeff(), j)); +} + +void intervals::add_linear_to_vector(const nex* e, vector> &v) { + TRACE("nla_horner_details", tout << *e << "\n";); + switch (e->type()) { + case expr_type::MUL: + add_mul_of_degree_one_to_vector(to_mul(e), v); + break; + case expr_type::VAR: + v.push_back(std::make_pair(rational(1), to_var(e)->var())); + break; + default: + SASSERT(!e->is_sum()); + // noop + } +} + +// e = a * can_t + b +lp::lar_term intervals::expression_to_normalized_term(const nex_sum* e, rational& a, rational& b) { + TRACE("nla_horner_details", tout << *e << "\n";); + lpvar smallest_j; + vector> v; + b = rational(0); + unsigned a_index; + for (const nex* c : e->children()) { + if (c->is_scalar()) { + b += to_scalar(c)->value(); + } else { + add_linear_to_vector(c, v); + if (v.empty()) + continue; + if (v.size() == 1 || smallest_j > v.back().second) { + smallest_j = v.back().second; + a_index = v.size() - 1; + } + } + } + TRACE("nla_horner_details", tout << "a_index = " << a_index << ", v="; print_vector(v, tout) << "\n";); + a = v[a_index].first; + lp::lar_term t; + + if (a.is_one()) { + for (unsigned k = 0; k < v.size(); k++) { + auto& p = v[k]; + t.add_coeff_var(p.first, p.second); + } + } else { + for (unsigned k = 0; k < v.size(); k++) { + auto& p = v[k]; + if (k != a_index) + t.add_coeff_var(p.first/a, p.second); + else + t.add_var(p.second); + } + } + TRACE("nla_horner_details", tout << a << "* ("; + lp::lar_solver::print_term_as_indices(t, tout) << ") + " << b << std::endl;); + SASSERT(t.is_normalized()); + return t; +} + + +// we should have in the case of found a * m_terms[k] + b = e, +// where m_terms[k] corresponds to the returned lpvar +lpvar intervals::find_term_column(const lp::lar_term & norm_t, rational& a) const { + std::pair a_j; + if (m_core->m_lar_solver.fetch_normalized_term_column(norm_t, a_j)) { + a /= a_j.first; + return a_j.second; + } + return -1; +} + + + +bool intervals::interval_from_term_with_deps(const nex* e, interv & i) const { + rational a, b; + lp::lar_term norm_t = expression_to_normalized_term(to_sum(e), a, b); + lp::explanation exp; + if (m_core->explain_by_equiv(norm_t, exp)) { + set_zero_interval_with_explanation(i, exp); + 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_with_deps(j, i); + interv bi; + mul_with_deps(a, i, bi); + add(b, bi); + set_with_deps(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 intervals::interval_from_term(const nex* e, interv & i) const { + rational a, b; + lp::lar_term norm_t = expression_to_normalized_term(to_sum(e), 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_no_deps(a, i, bi); + add(b, bi); + set(i, bi, 44); + + 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; + +} + + +intervals::interv intervals::interval_of_sum_with_deps(const nex_sum* e) { + TRACE("nla_intervals_details", tout << "e=" << *e << "\n";); + interv i_e = interval_of_sum_no_term_with_deps(e); + if (e->is_a_linear_term()) { + SASSERT(e->is_sum() && e->size() > 1); + interv i_from_term ; + if (interval_from_term_with_deps(e, i_from_term)) { + interv r = intersect_with_deps(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; +} + +intervals::interv intervals::interval_of_sum(const nex_sum* e) { + interv i_e = interval_of_sum_no_term(e); + TRACE("nla_intervals_details", tout << "e=" << *e << "\ni_e="; display(tout, i_e) << "\n";); + 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)) { + TRACE("nla_intervals_details", tout << "i_from_term="; display(tout, i_from_term) << "\n";); + interv r = intersect(i_e, i_from_term, 44); + TRACE("nla_intervals_details", tout << "intersection="; display(tout, r) << "\n";); + if (is_empty(r)) { + SASSERT(false); // not implemented + } + return r; + + } + } + return i_e; +} + + void intervals::set_var_interval(lpvar v, interval& b) const { lp::constraint_index ci; rational val; diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 34f9d884a..71906e03a 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -452,5 +452,28 @@ public: return false; } void reset() { m_alloc.reset(); } + bool check_cross_nested_expr(const nex*, ci_dependency*); + interval interval_of_expr_with_deps(const nex* e, unsigned power); + interval interval_of_expr(const nex* e, unsigned power); + interval interval_of_sum(const nex_sum*); + interval interval_of_sum_no_term(const nex_sum*); + interval interval_of_mul(const nex_mul*); + interval interval_of_sum_no_term_with_deps(const nex_sum* e); + bool interval_from_term_with_deps(const nex* e, interval & i) const; + bool interval_from_term(const nex* e, interval & i) const; + interval interval_of_sum_with_deps(const nex_sum* e); + typedef interval interv; + void set_interval_for_scalar(interv&, const rational&); + interv power_with_deps(const interv& a, unsigned); + interv interval_of_mul_with_deps(const nex_mul*); + const nex* get_zero_interval_child(const nex_mul*) const; + const nex* get_inf_interval_child(const nex_sum*) const; + bool has_zero_interval(const nex* ) const; + bool has_inf_interval(const nex* ) const; + bool mul_has_inf_interval(const nex_mul* ) const; + static lp::lar_term expression_to_normalized_term(const nex_sum*, rational& a, rational & b); + static void add_linear_to_vector(const nex*, vector> &); + static void add_mul_of_degree_one_to_vector(const nex_mul*, vector> &); + lpvar find_term_column(const lp::lar_term &, rational & a) const; }; // end of intervals } // end of namespace nla