From b075d3923e44c0013785f14845c282141e0d1623 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 22 Aug 2019 18:18:54 -0700 Subject: [PATCH] separate calculations on intervals on one with dependencies and one without Signed-off-by: Lev Nachmanson --- src/math/lp/horner.cpp | 199 ++++++++++++++++++++++++++++------ src/math/lp/horner.h | 21 ++-- src/math/lp/nla_intervals.cpp | 64 +++++++++-- src/math/lp/nla_intervals.h | 126 +++++++++++++++++++-- 4 files changed, 356 insertions(+), 54 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 0435de5bf..8e614f3e9 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -66,19 +66,28 @@ bool horner::lemmas_on_expr(cross_nested& cn) { } +bool horner::check_cross_nested_expr(const nex* n) { + TRACE("nla_horner", tout << "cross-nested n = " << *n << "\n";); + c().lp_settings().st().m_cross_nested_forms++; + + auto i = interval_of_expr(n); + 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 id = interval_of_expr_with_deps(n); + TRACE("nla_horner", tout << "conflict: id = "; m_intervals.display(tout, id ) << *n << "\n";); + m_intervals.check_interval_for_conflict_on_zero(id); + 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) { - TRACE("nla_horner", tout << "cross-nested n = " << *n << "\n";); - auto i = interval_of_expr(n); - TRACE("nla_horner", tout << "callback n = " << *n << "\ni="; m_intervals.display(tout, i) << "\n";); - - bool conflict = m_intervals.check_interval_for_conflict_on_zero(i); - c().lp_settings().st().m_cross_nested_forms++; - m_intervals.reset(); // clean the memory allocated by the interval bound dependencies - return conflict; - }, - [this](unsigned j) { return c().var_is_fixed(j); } + cross_nested cn( + [this](const nex* n) { return check_cross_nested_expr(n); }, + [this](unsigned j) { return c().var_is_fixed(j); } ); SASSERT (row_is_interesting(row)); @@ -167,6 +176,26 @@ void horner::set_interval_for_scalar(interv& a, const rational& v) { m_intervals.set_upper_is_inf(a, false); } +interv horner::interval_of_expr_with_deps(const nex* e) { + interv a; + switch (e->type()) { + case expr_type::SCALAR: + set_interval_for_scalar(a, to_scalar(e)->value()); + return a; + case expr_type::SUM: + return interval_of_sum_with_deps(to_sum(e)); + case expr_type::MUL: + return interval_of_mul_with_deps(to_mul(e)); + case expr_type::VAR: + set_var_interval_with_deps(to_var(e)->var(), a); + return a; + default: + TRACE("nla_horner_details", tout << e->type() << "\n";); + SASSERT(false); + return interv(); + } +} + interv horner::interval_of_expr(const nex* e) { interv a; switch (e->type()) { @@ -188,6 +217,37 @@ interv horner::interval_of_expr(const nex* e) { } +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); + 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()); + auto & es = to_mul(e)->children(); + interv a = interval_of_expr_with_deps(es[0]); + 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_with_deps(es[k]); + TRACE("nla_horner_details", tout << "es[" << k << "] "<< *es[k] << ", "; m_intervals.display(tout, b); ); + interv c; + interval_deps_combine_rule comb_rule; + m_intervals.mul(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) { const nex * zero_interval_child = get_zero_interval_child(e); if (zero_interval_child) { @@ -200,10 +260,10 @@ interv horner::interval_of_mul(const nex_mul* e) { SASSERT(e->is_mul()); auto & es = to_mul(e)->children(); interv a = interval_of_expr(es[0]); - TRACE("nla_horner_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); ); + 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]); - TRACE("nla_horner_details", tout << "es[" << k << "] "<< es[k] << ", "; m_intervals.display(tout, b); ); + TRACE("nla_horner_details", tout << "es[" << k << "] "<< *es[k] << ", "; m_intervals.display(tout, b); ); interv c; interval_deps_combine_rule comb_rule; m_intervals.mul(a, b, c, comb_rule); @@ -211,7 +271,7 @@ interv horner::interval_of_mul(const nex_mul* e) { 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); + 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"; @@ -219,8 +279,9 @@ interv horner::interval_of_mul(const nex_mul* e) { return a; } + void horner::add_mul_to_vector(const nex_mul* e, vector> &v) { - TRACE("nla_horner_details", tout << e << "\n";); + TRACE("nla_horner_details", tout << *e << "\n";); SASSERT(e->size() > 0); if (e->size() == 1) { add_linear_to_vector(*(e->children().begin()), v); @@ -246,7 +307,7 @@ void horner::add_mul_to_vector(const nex_mul* e, vector> &v) { - TRACE("nla_horner_details", tout << e << "\n";); + TRACE("nla_horner_details", tout << *e << "\n";); switch (e->type()) { case expr_type::MUL: add_mul_to_vector(to_mul(e), v); @@ -261,7 +322,7 @@ void horner::add_linear_to_vector(const nex* e, vector> v; b = rational(0); @@ -364,7 +425,31 @@ lpvar horner::find_term_column(const lp::lar_term & norm_t, rational& a) const { return -1; } -interv horner::interval_of_sum_no_terms(const nex_sum* e) { +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]); + 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]); + 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(); @@ -372,23 +457,23 @@ interv horner::interval_of_sum_no_terms(const nex_sum* e) { auto & es = e->children(); interv a = interval_of_expr(es[0]); for (unsigned k = 1; k < es.size(); k++) { - TRACE("nla_horner_details_sum", tout << "es[" << k << "]= " << es[k] << "\n";); + TRACE("nla_horner_details_sum", tout << "es[" << k << "]= " << *es[k] << "\n";); interv b = interval_of_expr(es[k]); 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); - TRACE("nla_horner_details_sum", tout << es[k] << ", "; + 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"; + TRACE("nla_horner_details", tout << "e=" << *e << "\n"; tout << " interv = "; m_intervals.display(tout, a);); return a; } -bool horner::interval_from_term(const nex* e, interv & i) const { +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; @@ -401,28 +486,75 @@ bool horner::interval_from_term(const nex* e, interv & i) const { if (j + 1 == 0) return false; - set_var_interval(j, i); + set_var_interval_with_deps(j, i); interv bi; - m_intervals.mul(a, i, bi); + m_intervals.mul_with_deps(a, i, bi); m_intervals.add(b, bi); - m_intervals.set(i, 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);); + 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(a, i, bi, 22); + 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) { - TRACE("nla_horner_details", tout << "e=" << e << "\n";); - interv i_e = interval_of_sum_no_terms(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)) { - interv r = m_intervals.intersect(i_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 @@ -435,11 +567,16 @@ interv horner::interval_of_sum(const nex_sum* e) { } // sets the dependencies also -void horner::set_var_interval(lpvar v, interv& b) const{ +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 957e2921a..957169e2c 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -42,15 +42,22 @@ public: template bool row_is_interesting(const T&) const; template void create_sum_from_row(const T&, cross_nested&); + intervals::interval interval_of_expr_with_deps(const nex* e); intervals::interval interval_of_expr(const nex* e); - - nex* nexvar(lpvar j, cross_nested& cn) const; - nex* nexvar(const rational& coeff, lpvar j, cross_nested& cn) const; intervals::interval interval_of_sum(const nex_sum*); - intervals::interval interval_of_sum_no_terms(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; + + + nex* nexvar(lpvar j, cross_nested& cn) const; + nex* nexvar(const rational& coeff, lpvar j, cross_nested& cn) 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&); template // T has an iterator of (coeff(), var()) @@ -59,12 +66,12 @@ public: 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_to_vector(const nex_mul*, vector> &); - bool interval_from_term(const nex* e, interv&) const; + 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 has_inf_interval(const nex* ) const; bool mul_has_inf_interval(const nex_mul* ) const; + bool check_cross_nested_expr(const nex*); }; // end of horner } diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index b9e32944d..74c351ac6 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -32,6 +32,30 @@ void intervals::set_var_interval_with_deps(lpvar v, interval& b) const { } } +void intervals::set_var_interval(lpvar v, interval& b) const { + 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); + } + else { + m_config.set_lower_is_open(b, true); + m_config.set_lower_is_inf(b, true); + } + 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); + } + else { + m_config.set_upper_is_open(b, true); + m_config.set_upper_is_inf(b, true); + } +} + void intervals::set_zero_interval_with_explanation(interval& i, const lp::explanation& exp) const { auto val = rational(0); m_config.set_lower(i, val); @@ -43,22 +67,50 @@ void intervals::set_zero_interval_with_explanation(interval& i, const lp::explan i.m_lower_dep = i.m_upper_dep = mk_dep(exp); } +void intervals::set_zero_interval(interval& i) const { + auto val = rational(0); + m_config.set_lower(i, val); + m_config.set_lower_is_open(i, false); + m_config.set_lower_is_inf(i, false); + m_config.set_upper(i, val); + m_config.set_upper_is_open(i, false); + m_config.set_upper_is_inf(i, false); +} + void intervals::set_zero_interval_deps_for_mult(interval& a) { a.m_lower_dep = m_dep_manager.mk_join(a.m_lower_dep, a.m_upper_dep); a.m_upper_dep = a.m_lower_dep; } -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::separated_from_zero_on_lower(const interval& i) const { + if (lower_is_inf(i)) + return false; + 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; + return true; } -bool intervals::check_interval_for_conflict_on_zero_upper(const interval & i) { +bool intervals::separated_from_zero_on_upper(const interval& i) const { if (upper_is_inf(i)) return false; if (unsynch_mpq_manager::is_pos(upper(i))) return false; if (unsynch_mpq_manager::is_zero(upper(i)) && !m_config.upper_is_open(i)) return false; + return true; +} + + +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) { + if (!separated_from_zero_on_upper(i)) + return false; + add_empty_lemma(); svector expl; m_dep_manager.linearize(i.m_upper_dep, expl); @@ -68,11 +120,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_neg(lower(i))) - return false; - if (unsynch_mpq_manager::is_zero(lower(i)) && !m_config.lower_is_open(i)) + if (!separated_from_zero_on_lower(i)) return false; add_empty_lemma(); svector expl; diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 962653451..2b9e5bf40 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -145,7 +145,6 @@ class intervals : common { public: typedef interval_manager::interval interval; private: - void set_var_interval(lpvar v, interval & b) const; ci_dependency* mk_dep(lp::constraint_index ci) const; ci_dependency* mk_dep(lp::explanation const &) const; lp::lar_solver& ls(); @@ -170,7 +169,9 @@ public: void set_upper_is_open(interval & a, bool strict) { m_config.set_upper_is_open(a, strict); } void set_upper_is_inf(interval & a, bool inf) { m_config.set_upper_is_inf(a, inf); } bool is_zero(const interval& a) const { return m_config.is_zero(a); } - void mul(const rational& r, const interval& a, interval& b) const { + void set_var_interval(lpvar v, interval & b) const; + + void mul_with_deps(const rational& r, const interval& a, interval& b) const { m_imanager.mul(r.to_mpq(), a, b); if (r.is_pos()) { b.m_lower_dep = a.m_lower_dep; @@ -182,6 +183,10 @@ public: } } + void mul(const rational& r, const interval& a, interval& b, int foo) const { + m_imanager.mul(r.to_mpq(), a, b); + } + void add(const rational& r, interval& a) const { if (!a.m_lower_inf) { m_config.set_lower(a, a.m_lower + r); @@ -194,11 +199,16 @@ public: void mul(const interval& a, const interval& b, interval& c) { m_imanager.mul(a, b, c); } void add(const interval& a, const interval& b, interval& c) { m_imanager.add(a, b, c); } void add(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.add(a, b, c, deps); } - void set(interval& a, const interval& b) const { + void set_with_deps(interval& a, const interval& b) const { m_imanager.set(a, b); a.m_lower_dep = b.m_lower_dep; a.m_upper_dep = b.m_upper_dep; } + + void set(interval& a, const interval& b, int fooo) const { + m_imanager.set(a, b); + } + void mul(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.mul(a, b, c, deps); } void combine_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const { SASSERT(&a != &i && &b != &i); @@ -238,7 +248,40 @@ public: copy_lower_bound(b, i); } - void copy_upper_bound(const interval& a, interval & i) const { + void update_lower_for_intersection_with_deps(const interval& a, const interval& b, interval & i) const { + if (a.m_lower_inf) { + if (b.m_lower_inf) + return; + copy_lower_bound_with_deps(b, i); + return; + } + + if (b.m_lower_inf) { + SASSERT(!a.m_lower_inf); + copy_lower_bound_with_deps(a, i); + return; + } + + if (m_num_manager.lt(a.m_lower, b.m_lower)) { + copy_lower_bound_with_deps(b, i); + return; + } + + if (m_num_manager.gt(a.m_lower, b.m_lower)) { + copy_lower_bound_with_deps(a, i); + return; + } + + SASSERT(m_num_manager.eq(a.m_lower, b.m_lower)); + if (a.m_lower_open) { // we might consider to look at b.m_lower_open too here + copy_lower_bound_with_deps(a, i); + return; + } + + copy_lower_bound_with_deps(b, i); + } + + void copy_upper_bound_with_deps(const interval& a, interval & i) const { SASSERT(a.m_upper_inf == false); i.m_upper_inf = false; m_config.set_upper(i, a.m_upper); @@ -246,14 +289,62 @@ public: i.m_upper_open = a.m_upper_open; } - void copy_lower_bound(const interval& a, interval & i) const { - SASSERT(a.m_lower_open == false); + void copy_upper_bound(const interval& a, interval & i) const { + SASSERT(a.m_upper_inf == false); + i.m_upper_inf = false; + m_config.set_upper(i, a.m_upper); + i.m_upper_open = a.m_upper_open; + } + + void copy_lower_bound_with_deps(const interval& a, interval & i) const { + SASSERT(a.m_lower_inf == false); i.m_lower_inf = false; m_config.set_lower(i, a.m_lower); i.m_lower_dep = a.m_lower_dep; i.m_lower_open = a.m_lower_open; } + + void copy_lower_bound(const interval& a, interval & i) const { + SASSERT(a.m_lower_inf == false); + i.m_lower_inf = false; + m_config.set_lower(i, a.m_lower); + i.m_lower_open = a.m_lower_open; + } + + void update_upper_for_intersection_with_deps(const interval& a, const interval& b, interval & i) const { + if (a.m_upper_inf) { + if (b.m_upper_inf) + return; + copy_upper_bound_with_deps(b, i); + return; + } + + if (b.m_upper_inf) { + SASSERT(!a.m_upper_inf); + copy_upper_bound_with_deps(a, i); + return; + } + + if (m_num_manager.gt(a.m_upper, b.m_upper)) { + copy_upper_bound_with_deps(b, i); + return; + } + + if (m_num_manager.lt(a.m_upper, b.m_upper)) { + copy_upper_bound_with_deps(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_with_deps(a, i); + return; + } + + copy_upper_bound_with_deps(b, i); + } + void update_upper_for_intersection(const interval& a, const interval& b, interval & i) const { if (a.m_upper_inf) { if (b.m_upper_inf) @@ -286,8 +377,19 @@ public: copy_upper_bound(b, i); } + - interval intersect(const interval& a, const interval& b) const { + interval intersect_with_deps(const interval& a, const interval& b) const { + interval i; + TRACE("nla_interval_compare", tout << "a="; display(tout, a) << "\nb="; display(tout, b);); + update_lower_for_intersection_with_deps(a, b, i); + TRACE("nla_interval_compare", tout << "i="; display(tout, i) << "\n";); + update_upper_for_intersection_with_deps(a, b, i); + TRACE("nla_interval_compare", tout << "i="; display(tout, i) << "\n";); + return i; + } + + interval intersect(const interval& a, const interval& b, int foo) const { interval i; TRACE("nla_interval_compare", tout << "a="; display(tout, a) << "\nb="; display(tout, b);); update_lower_for_intersection(a, b, i); @@ -296,18 +398,26 @@ public: TRACE("nla_interval_compare", tout << "i="; display(tout, i) << "\n";); return i; } - + 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); } void set_var_interval_with_deps(lpvar, interval &) const; void set_zero_interval_deps_for_mult(interval&); void set_zero_interval_with_explanation(interval& , const lp::explanation& exp) const; + void set_zero_interval(interval&) const; bool is_inf(const interval& i) const { return m_config.is_inf(i); } + bool separated_from_zero_on_lower(const interval&) const; + bool separated_from_zero_on_upper(const interval&) const; + inline bool separated_from_zero(const interval& i) const { + return separated_from_zero_on_upper(i) || + separated_from_zero_on_lower(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); } mpq const & upper(interval const & a) const { return m_config.upper(a); } + inline bool is_empty(interval const & a) const { if (a.m_lower_inf || a.m_upper_inf) return false;