From cc5971ceaf7cdcf400e60f6b039d3620e5848e6f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Feb 2020 10:50:54 -0800 Subject: [PATCH] fix #2936 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith.h | 4 ++-- src/smt/theory_arith_nl.h | 40 ++++++++++++++++++++++++--------------- 2 files changed, 27 insertions(+), 17 deletions(-) diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 41bb3753e..dc30c99a0 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -1011,8 +1011,8 @@ namespace smt { unsigned get_min_degree(sbuffer & p, expr * var); expr * factor(expr * m, expr * var, unsigned d); bool in_monovariate_monomials(sbuffer & p, expr * var, unsigned & i1, rational & c1, unsigned & n1, unsigned & i2, rational & c2, unsigned & n2); - expr * horner(sbuffer & p, expr * var); - expr * cross_nested(sbuffer & p, expr * var); + expr * horner(unsigned depth, sbuffer & p, expr * var); + expr * cross_nested(unsigned depth, sbuffer & p, expr * var); bool is_cross_nested_consistent(sbuffer & p); bool is_cross_nested_consistent(row const & r); bool is_cross_nested_consistent(svector const & nl_cluster); diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 6c8a88ceb..79337f4fe 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -209,10 +209,12 @@ expr * theory_arith::get_monomial_body(expr * m) const { template rational theory_arith::get_monomial_coeff(expr * m) const { SASSERT(m_util.is_mul(m)); - rational r; - if (m_util.is_numeral(to_app(m)->get_arg(0), r)) - return r; - return rational(1); + rational result(1), r; + for (expr* arg : *to_app(m)) { + if (m_util.is_numeral(arg, r)) + result *= r; + } + return result; } /** @@ -222,11 +224,14 @@ template unsigned theory_arith::get_num_vars_in_monomial(expr * m) const { SASSERT(m_util.is_mul(m)); m = get_monomial_body(m); - SASSERT(!m_util.is_numeral(m)); + if (m_util.is_numeral(m)) + return 0; if (m_util.is_mul(m)) { unsigned num_vars = 0; expr * var = nullptr; for (expr * curr : *to_app(m)) { + if (m_util.is_numeral(curr)) + continue; if (var != curr) { num_vars++; var = curr; @@ -252,7 +257,10 @@ typename theory_arith::var_power_pair theory_arith::get_var_and_degree expr * var = nullptr; unsigned power = 0; for (expr * arg : *to_app(m)) { - if (var == nullptr) { + if (m_util.is_numeral(arg)) { + continue; + } + else if (var == nullptr) { var = arg; power = 1; } @@ -1465,7 +1473,7 @@ expr * theory_arith::factor(expr * m, expr * var, unsigned d) { \brief Return the horner extension of p with respect to var. */ template -expr * theory_arith::horner(sbuffer & p, expr * var) { +expr * theory_arith::horner(unsigned depth, sbuffer & p, expr * var) { SASSERT(!p.empty()); SASSERT(var != 0); unsigned d = get_min_degree(p, var); @@ -1486,9 +1494,9 @@ expr * theory_arith::horner(sbuffer & p, expr * var) { r.push_back(coeff_expr(kv.first, f)); } } - expr * s = cross_nested(e, nullptr); + expr * s = cross_nested(depth + 1, e, nullptr); if (!r.empty()) { - expr * q = horner(r, var); + expr * q = horner(depth + 1, r, var); // TODO: improve here s = m_util.mk_add(q, s); } @@ -1511,12 +1519,12 @@ expr * theory_arith::horner(sbuffer & p, expr * var) { If var != 0, then it is used for performing the horner extension */ template -expr * theory_arith::cross_nested(sbuffer & p, expr * var) { + expr * theory_arith::cross_nested(unsigned depth, sbuffer & p, expr * var) { TRACE("non_linear", tout << "p.size: " << p.size() << "\n";); if (var == nullptr) { sbuffer varinfo; if (!get_polynomial_info(p, varinfo)) - return nullptr; + return p2expr(p); if (varinfo.empty()) return p2expr(p); unsigned max = 0; @@ -1527,6 +1535,8 @@ expr * theory_arith::cross_nested(sbuffer & p, expr * var) { } } } + if (depth > 20) + return p2expr(p); SASSERT(var != nullptr); unsigned i1 = UINT_MAX; unsigned i2 = UINT_MAX; @@ -1546,7 +1556,7 @@ expr * theory_arith::cross_nested(sbuffer & p, expr * var) { tout << "i2: " << i2 << "\n"; tout << "b: " << b << "\n"; tout << "nm: " << nm << "\n";); - if (n == nm) return horner(p, var); + if (n == nm) return horner(depth, p, var); SASSERT(n != nm); expr * new_expr = nullptr; if (nm < n) { @@ -1585,14 +1595,14 @@ expr * theory_arith::cross_nested(sbuffer & p, expr * var) { if (rest.empty()) return new_expr; TRACE("non_linear", tout << "rest size: " << rest.size() << ", i1: " << i1 << ", i2: " << i2 << "\n";); - expr * h = cross_nested(rest, nullptr); + expr * h = cross_nested(depth + 1, rest, nullptr); expr * r = m_util.mk_add(new_expr, h); m_nl_new_exprs.push_back(r); return r; } } } - return horner(p, var); + return horner(depth, p, var); } /** @@ -1614,7 +1624,7 @@ bool theory_arith::is_cross_nested_consistent(sbuffer & p) { for (auto const& kv : varinfo) { m_nl_new_exprs.reset(); expr * var = kv.first; - expr * cn = cross_nested(p, var); + expr * cn = cross_nested(0, p, var); // Remark: cn may not be well-sorted because, since a row may contain mixed integer/real monomials. // This is not really a problem, since evaluate_as_interval will work even if cn is not well-sorted. if (!cn)