From ee4da1affd04f31313886c665ab3b157be764e0c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 10 Jul 2019 16:22:28 -0700 Subject: [PATCH] work on horner Signed-off-by: Lev Nachmanson --- src/math/lp/horner.cpp | 80 ++++++++++++++++++++--------------- src/math/lp/horner.h | 6 +-- src/math/lp/lp_utils.h | 6 +++ src/math/lp/nla_intervals.cpp | 4 +- src/math/lp/nla_solver.h | 2 +- 5 files changed, 57 insertions(+), 41 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index c4199fa49..b94d73bd8 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -21,7 +21,6 @@ #include "math/lp/horner.h" #include "math/lp/nla_core.h" #include "math/lp/lp_utils.h" - namespace nla { typedef nla_expr nex; typedef intervals::interval interv; @@ -39,48 +38,59 @@ bool horner::row_is_interesting(const T& row) const { } void horner::lemmas_on_expr(nex& e) { + TRACE("nla_cn", tout << "e = " << e << "\n";); vector front; front.push_back(&e); cross_nested_of_expr(e, front); } -void horner::cross_nested_of_expr(nex& e, vector front) { - TRACE("nla_cn", tout << "e = " << e << ", front has " << front.size() << "\n";); - while (!front.empty()) { - nex& c = *front.back(); - front.pop_back(); - cross_nested_of_expr_on_front_elem(e, c, front); - } - TRACE("nla_cn", tout << "empty front: e=" << "\n";); - +nex* pop_back(vector& front) { + nex* c = front.back(); + front.pop_back(); + return c; } -void horner::cross_nested_of_expr_on_front_elem(nex& e, nex& c, vector front) { - TRACE("nla_cn", tout << "e=" << e << "\nc=" << c << "\n";); - SASSERT(c.is_sum()); - auto occurences = get_mult_occurences(c); - if (occurences.empty() && front.empty()) { - TRACE("nla_cn", tout << "empty front: e=" << e << "\n";); - auto i = interval_of_expr(e); - m_intervals.check_interval_for_conflict_on_zero(i); +void horner::cross_nested_of_expr(nex& e, vector& front) { + TRACE("nla_cn", tout << "e = " << e << ", front:"; print_vector_of_ptrs(front, tout) << "\n";); + while (!front.empty()) { + nex* c = pop_back(front); + cross_nested_of_expr_on_front_elem(e, c, front); + } +} + +void horner::cross_nested_of_expr_on_front_elem(nex& e, nex* c, vector& front) { + SASSERT(c->is_sum()); + vector occurences = get_mult_occurences(*c); + TRACE("nla_cn", tout << "e=" << e << "\nc=" << *c << "\noccurences="; print_vector(occurences, tout) << "\nfront:"; print_vector_of_ptrs(front, tout) << "\n";); + + if (occurences.empty()) { + if(front.empty()) { + TRACE("nla_cn", tout << "empty front: e=" << e << "\n";); + auto i = interval_of_expr(e); + m_intervals.check_interval_for_conflict_on_zero(i); + } else { + nex* c = pop_back(front); + cross_nested_of_expr_on_front_elem(e, c, front); + } } else { - nex copy_of_c = c; + TRACE("nla_cn", tout << "save c=" << *c << "front:"; print_vector_of_ptrs(front, tout) << "\n";); + nex copy_of_c = *c; for(lpvar j : occurences) { cross_nested_of_expr_on_sum_and_var(e, c, j, front); - c = copy_of_c; + *c = copy_of_c; + TRACE("nla_cn", tout << "restore c=" << *c << ", e=" << e << "\n";); } } TRACE("nla_cn", tout << "exit\n";); } // e is the global expression, c is the sub expressiond which is going to changed from sum to the cross nested form -void horner::cross_nested_of_expr_on_sum_and_var(nex& e, nex& c, lpvar j, vector front) { - TRACE("nla_cn", tout << "e=" << e << "\nc=" << c << "\nj = v" << j << "\n";); - split_with_var(c, j, front); - TRACE("nla_cn", tout << "after split c=" << c << "\n";); +void horner::cross_nested_of_expr_on_sum_and_var(nex& e, nex* c, lpvar j, vector& front) { + TRACE("nla_cn", tout << "e=" << e << "\nc=" << *c << "\nj = v" << j << "\nfront="; print_vector_of_ptrs(front, tout) << "\n";); + split_with_var(*c, j, front); + TRACE("nla_cn", tout << "after split c=" << *c << "\nfront="; print_vector_of_ptrs(front, tout) << "\n";); do { - nex& c = *front.back(); - front.pop_back(); - cross_nested_of_expr_on_front_elem(e, c, front); + nex* n = pop_back(front); + cross_nested_of_expr_on_front_elem(e, n, front); } while (!front.empty()); } @@ -166,7 +176,7 @@ vector horner::get_mult_occurences(const nex& e) const { SASSERT(false); } } - TRACE("nla_cn", + TRACE("nla_cn_details", tout << "{"; for(auto p: occurences) { tout << "(v" << p.first << "->" << p.second << ")"; @@ -181,7 +191,7 @@ vector horner::get_mult_occurences(const nex& e) const { } void horner::split_with_var(nex& e, lpvar j, vector & front) { - TRACE("nla_cn", tout << "e = " << e << ", j = v" << j << "\n";); + TRACE("nla_cn_details", tout << "e = " << e << ", j = v" << j << "\n";); if (!e.is_sum()) return; nex a, b; @@ -193,7 +203,7 @@ void horner::split_with_var(nex& e, lpvar j, vector & front) { } } a.type() = expr_type::SUM; - TRACE("nla_cn", tout << "a = " << a << "\n";); + TRACE("nla_cn_details", tout << "a = " << a << "\n";); SASSERT(a.children().size() >= 2); if (b.children().size() == 1) { @@ -210,20 +220,20 @@ void horner::split_with_var(nex& e, lpvar j, vector & front) { e.add_child(a); if (a.size() > 1) { front.push_back(&e.children().back()); - TRACE("nla_cn", tout << "push to front " << e.children().back() << "\n";); + TRACE("nla_cn_details", tout << "push to front " << e.children().back() << "\n";); } } else { - TRACE("nla_cn", tout << "b = " << b << "\n";); + TRACE("nla_cn_details", tout << "b = " << b << "\n";); e = nex::sum(nex::mul(nex::var(j), a), b); if (a.is_sum()) { front.push_back(&(e.children()[0].children()[1])); - TRACE("nla_cn", tout << "push to front " << e.children()[0].children()[1] << "\n";); + TRACE("nla_cn_details", tout << "push to front " << e.children()[0].children()[1] << "\n";); } if (b.is_sum()) { front.push_back(&(e.children()[1])); - TRACE("nla_cn", tout << "push to front " << e.children()[1] << "\n";); -} + TRACE("nla_cn_details", tout << "push to front " << e.children()[1] << "\n";); + } } } diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index 58bb517e4..d02f2ccf0 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -50,8 +50,8 @@ public: void set_interval_for_scalar(intervals::interval&, const rational&); std::set get_vars_of_expr(const nex &) const; void lemmas_on_expr(nex &); - void cross_nested_of_expr(nex& , vector front); - void cross_nested_of_expr_on_front_elem(nex& , nex&, vector front); - void cross_nested_of_expr_on_sum_and_var(nex& , nex&, lpvar, vector front); + void cross_nested_of_expr(nex& , vector& front); + void cross_nested_of_expr_on_front_elem(nex& , nex*, vector& front); + void cross_nested_of_expr_on_sum_and_var(nex& , nex*, lpvar, vector& front); }; // end of horner } diff --git a/src/math/lp/lp_utils.h b/src/math/lp/lp_utils.h index f0e9fe5af..cef119168 100644 --- a/src/math/lp/lp_utils.h +++ b/src/math/lp/lp_utils.h @@ -29,6 +29,12 @@ std::ostream& print_vector(const C & t, std::ostream & out) { out << p << " "; return out; } +template +std::ostream& print_vector_of_ptrs(const C & t, std::ostream & out) { + for (const auto & p : t) + out << (*p) << ", "; + return out; +} template bool contains(const C & collection, const D & key) { diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index a51e878e7..5b4b0ed3a 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -90,7 +90,7 @@ bool intervals::check_interval_for_conflict_on_zero_upper(const interval & i) { svector expl; m_dep_manager.linearize(i.m_upper_dep, expl); _().current_expl().add_expl(expl); - TRACE("nla_cn", print_lemma(tout);); + TRACE("nla_cn_lemmas", print_lemma(tout);); return true; } @@ -105,7 +105,7 @@ bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i) { svector expl; m_dep_manager.linearize(i.m_lower_dep, expl); _().current_expl().add_expl(expl); - TRACE("nla_cn", print_lemma(tout);); + TRACE("nla_cn_lemmas", print_lemma(tout);); return true; } diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index 1c3705533..62d77c7e5 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -31,8 +31,8 @@ namespace nla { // nonlinear integer incremental linear solver class solver { - core* m_core; reslimit m_res_limit; + core* m_core; public: void add_monomial(lpvar v, unsigned sz, lpvar const* vs);