From e2702f3ae88f5c48a55f4473bb5c29184c182634 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 29 Jul 2019 18:07:38 -0700 Subject: [PATCH] fixes in assigning constraints to intervals Signed-off-by: Lev Nachmanson --- src/math/lp/cross_nested.h | 23 ++++++++++++++++++++--- src/math/lp/horner.cpp | 37 ++++++++++++++++++++++++++----------- src/math/lp/horner.h | 4 ++-- src/math/lp/nla_intervals.h | 7 ++++--- src/test/lp/lp.cpp | 4 +++- 5 files changed, 55 insertions(+), 20 deletions(-) diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h index 835f563bc..4b281efdc 100644 --- a/src/math/lp/cross_nested.h +++ b/src/math/lp/cross_nested.h @@ -24,9 +24,18 @@ namespace nla { class cross_nested { typedef nla_expr nex; nex& m_e; - std::function m_call_on_result; + std::function m_call_on_result; + std::function m_var_is_fixed; + bool m_done; public: - cross_nested(nex &e, std::function call_on_result): m_e(e), m_call_on_result(call_on_result) {} + cross_nested(nex &e, + std::function call_on_result, + std::function var_is_fixed): + m_e(e), + m_call_on_result(call_on_result), + m_var_is_fixed(var_is_fixed), + m_done(false) + {} void run() { vector front; @@ -123,7 +132,15 @@ public: for(auto& p : occurences) { SASSERT(p.second.m_occs > 1); lpvar j = p.first; + if (m_var_is_fixed(j)) { + // it does not make sense to explore fixed multupliers + // because the interval products do not become smaller + // after factoring those out + continue; + } explore_of_expr_on_sum_and_var(c, j, front); + if (m_done) + return; *c = copy_of_c; TRACE("nla_cn", tout << "restore c=" << *c << ", m_e=" << m_e << "\n";); restore_front(copy_of_front, front); @@ -151,7 +168,7 @@ public: if (occurences.empty()) { if(front.empty()) { TRACE("nla_cn", tout << "got the cn form: =" << m_e << "\n";); - m_call_on_result(m_e); + m_done = m_call_on_result(m_e); } else { nex* c = pop_back(front); explore_expr_on_front_elem(c, front); diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index d51b9e159..e8ce097b8 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -52,23 +52,29 @@ bool horner::row_is_interesting(const T& row) const { return false; } -void horner::lemmas_on_expr(nex& e) { - TRACE("nla_horner", tout << "e = " << e << "\n";); - cross_nested cn(e, [this](const nex& n) { +bool horner::lemmas_on_expr(nex& e) { + TRACE("nla_horner", tout << "e = " << e << "\n";); + bool conflict = false; + cross_nested cn(e, [this, & conflict](const nex& n) { auto i = interval_of_expr(n); TRACE("nla_horner", tout << "callback n = " << n << "\ni="; m_intervals.display(tout, i) << "\n";); - m_intervals.check_interval_for_conflict_on_zero(i);} ); + conflict = m_intervals.check_interval_for_conflict_on_zero(i); + return conflict; + }, + [this](unsigned j) { return c().var_is_fixed(j); } + ); cn.run(); + return conflict; } template -void horner::lemmas_on_row(const T& row) { +bool horner::lemmas_on_row(const T& row) { if (!row_is_interesting(row)) - return; + return false; nex e = create_sum_from_row(row); - lemmas_on_expr(e); + return lemmas_on_expr(e); } void horner::horner_lemmas() { @@ -84,8 +90,16 @@ void horner::horner_lemmas() { for (auto & s : matrix.m_columns[j]) rows_to_check.insert(s.var()); } - for (unsigned i : rows_to_check) { - lemmas_on_row(matrix.m_rows[i]); + svector rows; + for (unsigned i : rows_to_check) { + rows.push_back(i); + } + + unsigned r = c().random(); + unsigned sz = rows.size(); + for (unsigned i = 0; i < sz; i++) { + if (lemmas_on_row(matrix.m_rows[(i + r) % sz])) + break; } } @@ -145,7 +159,6 @@ interv horner::interval_of_expr(const nex& e) { interv horner::interval_of_mul(const nex& e) { SASSERT(e.is_mul()); auto & es = e.children(); - interval_deps_combine_rule comb_rule; interv a = interval_of_expr(es[0]); if (m_intervals.is_zero(a)) { m_intervals.set_zero_interval_deps_for_mult(a); @@ -161,9 +174,11 @@ interv horner::interval_of_mul(const nex& e) { TRACE("nla_horner_details", tout << "got zero\n"; ); return b; } - 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); + 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);); diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index e45a92512..a08852956 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -35,7 +35,7 @@ public: horner(core *core); void horner_lemmas(); template // T has an iterator of (coeff(), var()) - void lemmas_on_row(const T&); + bool lemmas_on_row(const T&); template bool row_is_interesting(const T&) const; template nex create_sum_from_row(const T&); intervals::interval interval_of_expr(const nex& e); @@ -46,6 +46,6 @@ public: 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; - void lemmas_on_expr(nex &); + bool lemmas_on_expr(nex &); }; // end of horner } diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index e60884fcb..5581bdce1 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -74,7 +74,8 @@ class intervals : common { }; - void add_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const { + void add_deps(interval const& a, interval const& b, + interval_deps_combine_rule const& deps, interval& i) const { i.m_lower_dep = mk_dependency(a, b, deps.m_lower_combine); i.m_upper_dep = mk_dependency(a, b, deps.m_upper_combine); } @@ -176,8 +177,8 @@ public: 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) { m_imanager.set(a, b); - a.m_lower_dep = b.m_lower_dep; - a.m_upper_dep = b.m_upper_dep; + a.m_lower_dep = lower_is_inf(a)? nullptr : b.m_lower_dep; + a.m_upper_dep = upper_is_inf(a)?nullptr : b.m_upper_dep; } 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 { diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 25cdd75c3..f25d10f40 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -72,7 +72,9 @@ void test_cn_on_expr(horner::nex t) { TRACE("nla_cn", tout << "t=" << t << '\n';); cross_nested cn(t, [](const horner::nex& n) { TRACE("nla_cn_test", tout << n << "\n";); - } ); + return false; + } , + [](unsigned) { return false; }); cn.run(); }