From 5428d0bb0f08808612b4a8e5b53e84002659ee8c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 17 Aug 2019 18:59:26 -0700 Subject: [PATCH] rewrite horner scheme on top of nex_expr as a pointer Signed-off-by: Lev Nachmanson --- src/math/lp/cross_nested.h | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h index 50f70b6f4..787c931e0 100644 --- a/src/math/lp/cross_nested.h +++ b/src/math/lp/cross_nested.h @@ -215,13 +215,16 @@ public: nex* extract_common_factor(nex* e, const vector> & occurences) { nex_sum* c = to_sum(e); - TRACE("nla_cn", tout << "c=" << *c << "\n";); + TRACE("nla_cn", tout << "c=" << *c << "\n"; tout << "occs:"; dump_occurences(tout, occurences) << "\n";); unsigned size = c->children().size(); + bool have_factor = false; for(const auto & p : occurences) { - if (p.second.m_occs < size) { - return nullptr; + if (p.second.m_occs == size) { + have_factor = true; + break; } } + if (have_factor == false) return nullptr; nex_mul* f = mk_mul(); for(const auto & p : occurences) { // randomize here: todo if (p.second.m_occs == size) { @@ -255,8 +258,10 @@ public: bool proceed_with_common_factor(nex*& c, vector& front, const vector> & occurences) { TRACE("nla_cn", tout << "c=" << *c << "\n";); nex* f = extract_common_factor(c, occurences); - if (f == nullptr) + if (f == nullptr) { + TRACE("nla_cn", tout << "no common factor\n"; ); return false; + } nex* c_over_f = mk_div(c, f); to_sum(c_over_f)->simplify();