From 97ef190f4f84acaa75ba3543a76009fe65450365 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 9 Jul 2019 12:20:43 -0700 Subject: [PATCH] full recursion on horner, not finished Signed-off-by: Lev Nachmanson --- src/math/lp/horner.cpp | 188 ++++++++++++++++++++----------------- src/math/lp/horner.h | 37 ++++---- src/smt/smt_context_pp.cpp | 1 + 3 files changed, 118 insertions(+), 108 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 38e7461dd..e77053168 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -29,6 +29,8 @@ horner::horner(core * c) : common(c), m_intervals(c, c->reslim()) {} template bool horner::row_is_interesting(const T& row) const { + if (row.size() <= 1) + return false; for (const auto& p : row) { if (c().m_to_refine.contains(p.var())) return true; @@ -36,19 +38,53 @@ bool horner::row_is_interesting(const T& row) const { return false; } +void horner::lemmas_on_expr(nex& e) { + 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";); + if (front.empty()) { + auto i = interval_of_expr(e); + m_intervals.check_interval_for_conflict_on_zero(i); + } + nex & c = *(front.back()); + front.pop_back(); + TRACE("nla_cn", tout << "pop from front\n";); + 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()); + std::unordered_map occurences; + TRACE("nla_cn", tout << "c = " << c << "\n";); + get_occurences_map(c, occurences); + nex copy_of_c(c); + for(const auto & p : occurences) { + TRACE("nla_cn", tout << "v" << p.first << ", " << p.second << "\n";); + if (p.second < 2) + continue; + cross_nested_of_expr_on_sum_and_var(e, c, p.first, front); + c = copy_of_c; + } + 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); + cross_nested_of_expr(e, front); +} + template -void horner::lemma_on_row(const T& row) { +void horner::lemmas_on_row(const T& row) { if (!row_is_interesting(row)) return; - nex e = create_expr_from_row(row); - TRACE("nla_cn", tout << "cross nested e = " << e << std::endl; - for (lpvar j: get_vars_of_expr(e)) { - print_var(j, tout); - } - ); - interv a = interval_of_expr(e); - TRACE("nla_cn_details", tout << "interval a = "; m_intervals.display(tout, a) << "\n";); - check_interval_for_conflict(a, row); + nex e = create_sum_from_row(row); + lemmas_on_expr(e); } void horner::horner_lemmas() { @@ -57,15 +93,14 @@ void horner::horner_lemmas() { return; } - const auto& m = c().m_lar_solver.A_r(); - unsigned r = random(); - unsigned s = m.row_count(); - for (unsigned i = 0; i < s && !done() ; i++) { - lemma_on_row(m.m_rows[((i + r) % s)]); + const auto& matrix = c().m_lar_solver.A_r(); + for (unsigned i = 0; i < matrix.row_count(); i++) { + lemmas_on_row(matrix.m_rows[i]); } } nex horner::nexvar(lpvar j) const { + // todo: consider deepen the recursion if (!c().is_monomial_var(j)) return nex::var(j); const monomial& m = c().emons()[j]; @@ -100,48 +135,20 @@ void process_mul_occurences(const nex& e, std::unordered_set& seen, std:: } } -// return a valid j if some variable appears more than once -unsigned horner::random_most_occured_var(std::unordered_map& occurences) { - unsigned max = 0; - unsigned ret = -1; - unsigned n = 0; - for (const auto & p : occurences) { - if (p.second > max) { - n = 0; - max = p.second; - ret = p.first; - } else if (p.second == max) { - n++; - if (random() % n == 0) { - ret = p.first; - } - } - } - if (max <= 1) - return -1; - SASSERT(ret + 1); - return ret; -} - -// j -> the number of expressions j appears in +// j -> the number of expressions j appears in as a multiplier void horner::get_occurences_map(const nla_expr& e, std::unordered_map& occurences) const { - TRACE("nla_cn_details", tout << "e = " << e << std::endl;); SASSERT(e.type() == expr_type::SUM); for (const auto & ce : e.children()) { std::unordered_set seen; if (ce.type() == expr_type::MUL) { for (const auto & cce : ce.children()) { - if (cce.type() == expr_type::SCALAR) { - } else if (cce.type() == expr_type::VAR) { + if (cce.type() == expr_type::VAR) { process_var_occurences(cce.var(), seen, occurences); } else if (cce.type() == expr_type::MUL) { process_mul_occurences(cce, seen, occurences); } else { - TRACE("nla_cn_details", tout << "e = " << e << "\nce = " << ce << std::endl << - "ce type = " << ce.type() << std::endl;); - - SASSERT(false); // unexpected type + continue; } } } else if (ce.type() == expr_type::VAR) { @@ -152,12 +159,18 @@ void horner::get_occurences_map(const nla_expr& e, std::unordered_map< SASSERT(false); } } + TRACE("nla_cn_details", + tout << "{"; + for(auto p: occurences) { + tout << "(v" << p.first << "->" << p.second << ")"; + } + tout << "}" << std::endl;); } -nex horner::split_with_var(const nex& e, lpvar j) { - TRACE("nla_cn_details", tout << "e = " << e << ", j = v" << j << "\n";); +void horner::split_with_var(nex& e, lpvar j, vector & front) { + TRACE("nla_cn", tout << "e = " << e << ", j = v" << j << "\n";); if (!e.is_sum()) - return e; + return; nex a, b; for (const nex & ce: e.children()) { if ((ce.is_mul() && ce.contains(j)) || (ce.is_var() && ce.var() == j)) { @@ -166,32 +179,45 @@ nex horner::split_with_var(const nex& e, lpvar j) { b.add_child(ce); } } - if (a.children().size() == 1) - return e; - SASSERT(a.children().size()); a.type() = expr_type::SUM; + TRACE("nla_cn", tout << "a = " << a << "\n";); + SASSERT(a.children().size() >= 2); if (b.children().size() == 1) { nex t = b.children()[0]; b = t; } else if (b.children().size() > 1) { - b.type() = expr_type::SUM; + b.type() = expr_type::SUM; } if (b.is_undef()) { SASSERT(b.children().size() == 0); - nex r(expr_type::MUL); - r.add_child(nex::var(j)); - r.add_child(cross_nested_of_sum(a)); - return r; + e = nex(expr_type::MUL); + e.add_child(nex::var(j)); + 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";); + } + + } else { + TRACE("nla_cn", 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";); + } + 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 << "b = " << b << "\n";); - return nex::sum(nex::mul(cross_nested_of_sum(a), nex::var(j)), cross_nested_of_sum(b)); } -nex horner::cross_nested_of_sum(const nex& e) { +nex horner::cross_nested_of_sum(const nex& e, lpvar j) { if (!e.is_sum()) return e; + /* std::unordered_map occurences; get_occurences_map(e, occurences); lpvar j = random_most_occured_var(occurences); @@ -204,28 +230,22 @@ nex horner::cross_nested_of_sum(const nex& e) { tout << std::endl << "most occured = v" << j << std::endl;); nex ret = split_with_var(e, j); TRACE("nla_cn_details", tout << "ret =" << ret << "\n";); - return ret; + return ret;*/ + SASSERT(false); + return nex(); } -template nex horner::create_expr_from_row(const T& row) { +template nex horner::create_sum_from_row(const T& row) { TRACE("nla_cn", tout << "row="; m_core->print_term(row, tout) << "\n";); - nex e; - if (row.size() > 1) { - e.type() = expr_type::SUM; - for (const auto &p : row) { - e.add_child(nex::mul(p.coeff(), nexvar(p.var()))); - } - return cross_nested_of_sum(e); + SASSERT(row.size() > 1); + nex e(expr_type::SUM); + for (const auto &p : row) { + e.add_child(nex::mul(p.coeff(), nexvar(p.var()))); } - if (row.size() == 1) { - const auto &p = *row.begin(); - return nex::mul(p.coeff(), nexvar(p.var())); - } - SASSERT(false); return e; } -template -std::set horner::get_vars_of_expr(const nla_expr &e ) const { + +std::set horner::get_vars_of_expr(const nex &e ) const { std::set r; switch (e.type()) { case expr_type::SCALAR: @@ -249,8 +269,7 @@ std::set horner::get_vars_of_expr(const nla_expr &e ) const { } -template -void horner::set_interval_for_scalar(interv& a, const T& v) { +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); @@ -280,8 +299,8 @@ interv horner::interval_of_expr(const nex& e) { return interv(); } } -template -interv horner::interval_of_mul(const vector>& es) { + +interv horner::interval_of_mul(const vector& es) { interv a = interval_of_expr(es[0]); // std::cout << "a" << std::endl; TRACE("nla_cn_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); tout << "\n";); @@ -307,8 +326,7 @@ interv horner::interval_of_mul(const vector>& es) { return a; } -template -interv horner::interval_of_sum(const vector>& es) { +interv horner::interval_of_sum(const vector& es) { interv a = interval_of_expr(es[0]); TRACE("nla_cn_details", tout << "es[0]= " << es[0] << "\n"; m_intervals.display(tout, a) << "\n";); if (m_intervals.is_inf(a)) { @@ -346,10 +364,4 @@ void horner::set_var_interval(lpvar v, interv& b) { TRACE("nla_cn_details", tout << "v = "; print_var(v, tout) << "\n"; m_intervals.display(tout, b)<< '\n';); } -template -void horner::check_interval_for_conflict(const interv& i, const T& row) { - if (m_intervals.check_interval_for_conflict_on_zero(i)) { - TRACE("nla_cn", print_lemma(tout);); - } -} } diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index b4e52b21a..da8b0b7bb 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -27,35 +27,32 @@ namespace nla { class core; -class horner : common { +class horner : common { + typedef nla_expr nex; intervals m_intervals; public: horner(core *core); void horner_lemmas(); template // T has an iterator of (coeff(), var()) - void lemma_on_row(const T&); + void lemmas_on_row(const T&); template bool row_is_interesting(const T&) const; - template nla_expr create_expr_from_row(const T&); - intervals::interval interval_of_expr(const nla_expr& e); + template nex create_sum_from_row(const T&); + intervals::interval interval_of_expr(const nex& e); - template void check_interval_for_conflict(const intervals::interval&, const T&); - bool check_interval_for_conflict_lower_bound(const intervals::interval&); - bool check_interval_for_conflict_upper_bound(const intervals::interval&); - nla_expr nexvar(lpvar j) const; - nla_expr cross_nested_of_sum(const nla_expr&); - void get_occurences_map(const nla_expr& e, + nex nexvar(lpvar j) const; + nex cross_nested_of_sum(const nex&, lpvar); + void get_occurences_map(const nex& e, std::unordered_map& ) const; - unsigned random_most_occured_var(std::unordered_map& occurences); - nla_expr split_with_var(const nla_expr &, lpvar); + void split_with_var(nex &, lpvar, vector & front); void set_var_interval(lpvar j, intervals::interval&); - template - intervals::interval interval_of_sum(const vector>&); - template - intervals::interval interval_of_mul(const vector>&); - template - void set_interval_for_scalar(intervals::interval&, const T&); - template - std::set get_vars_of_expr(const nla_expr &) const; + intervals::interval interval_of_sum(const vector&); + intervals::interval interval_of_mul(const vector&); + 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); }; // end of horner } diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 077051e95..76dbfecba 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -451,6 +451,7 @@ namespace smt { std::ofstream out(strm.str()); TRACE("lemma", tout << strm.str() << "\n";); display_lemma_as_smt_problem(out, num_antecedents, antecedents, consequent, logic); + TRACE("non_linear", display_lemma_as_smt_problem(tout, num_antecedents, antecedents, consequent, logic);); out.close(); return m_lemma_id; }