From b6618892d80355ef219c4c652206dff43833fdc4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 22 Mar 2020 11:02:24 -0700 Subject: [PATCH] fix #3469 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith.h | 16 ++++++++-------- src/smt/theory_arith_nl.h | 36 ++++++++++++++++++------------------ 2 files changed, 26 insertions(+), 26 deletions(-) diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index ee1b99312..29603db81 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -1000,20 +1000,20 @@ namespace smt { bool is_mixed_real_integer(row const & r) const; bool is_integer(row const & r) const; typedef std::pair coeff_expr; - bool get_polynomial_info(sbuffer const & p, sbuffer & vars); - expr * p2expr(sbuffer & p); + bool get_polynomial_info(buffer const & p, sbuffer & vars); + expr * p2expr(buffer & p); expr * power(expr * var, unsigned power); expr * mk_nary_mul(unsigned sz, expr * const * args, bool is_int); expr * mk_nary_add(unsigned sz, expr * const * args, bool is_int); expr * mk_nary_add(unsigned sz, expr * const * args); void display_nested_form(std::ostream & out, expr * p); unsigned get_degree_of(expr * m, expr * var); - unsigned get_min_degree(sbuffer & p, expr * var); + unsigned get_min_degree(buffer & 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(unsigned depth, sbuffer & p, expr * var); - expr * cross_nested(unsigned depth, sbuffer & p, expr * var); - bool is_cross_nested_consistent(sbuffer & p); + bool in_monovariate_monomials(buffer & p, expr * var, unsigned & i1, rational & c1, unsigned & n1, unsigned & i2, rational & c2, unsigned & n2); + expr * horner(unsigned depth, buffer & p, expr * var); + expr * cross_nested(unsigned depth, buffer & p, expr * var); + bool is_cross_nested_consistent(buffer & p); bool is_cross_nested_consistent(row const & r); bool is_cross_nested_consistent(svector const & nl_cluster); rational get_value(theory_var v, bool & computed_epsilon); @@ -1149,7 +1149,7 @@ namespace smt { void display_bounds_in_smtlib(std::ostream & out) const; void display_bounds_in_smtlib() const; void display_nl_monomials(std::ostream & out) const; - void display_coeff_exprs(std::ostream & out, sbuffer const & p) const; + void display_coeff_exprs(std::ostream & out, buffer const & p) const; void display_interval(std::ostream& out, interval const& i); void display_deps(std::ostream& out, v_dependency* dep); diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 1e4bc1b96..fe23240d2 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -1202,9 +1202,9 @@ bool theory_arith::is_integer(row const & r) const { } template -void theory_arith::display_coeff_exprs(std::ostream & out, sbuffer const & p) const { - typename sbuffer::const_iterator it = p.begin(); - typename sbuffer::const_iterator end = p.end(); +void theory_arith::display_coeff_exprs(std::ostream & out, buffer const & p) const { + typename buffer::const_iterator it = p.begin(); + typename buffer::const_iterator end = p.end(); for (bool first = true; it != end; ++it) { if (first) first = false; @@ -1220,7 +1220,7 @@ void theory_arith::display_coeff_exprs(std::ostream & out, sbuffer -bool theory_arith::get_polynomial_info(sbuffer const & p, sbuffer & varinfo) { +bool theory_arith::get_polynomial_info(buffer const & p, sbuffer & varinfo) { context & ctx = get_context(); varinfo.reset(); m_var2num_occs.reset(); @@ -1262,7 +1262,7 @@ bool theory_arith::get_polynomial_info(sbuffer const & p, sbuff \brief Convert p into an expression. */ template -expr * theory_arith::p2expr(sbuffer & p) { +expr * theory_arith::p2expr(buffer & p) { SASSERT(!p.empty()); TRACE("p2expr_bug", display_coeff_exprs(tout, p);); ptr_buffer args; @@ -1308,7 +1308,7 @@ expr * theory_arith::power(expr * var, unsigned power) { The arguments i1 and i2 contain the position in p of the two monomials. */ template -bool theory_arith::in_monovariate_monomials(sbuffer & p, expr * var, +bool theory_arith::in_monovariate_monomials(buffer & p, expr * var, unsigned & i1, rational & c1, unsigned & n1, unsigned & i2, rational & c2, unsigned & n2) { int idx = 0; #define SET_RESULT(POWER) { \ @@ -1328,8 +1328,8 @@ bool theory_arith::in_monovariate_monomials(sbuffer & p, expr * return false; \ } - typename sbuffer::const_iterator it = p.begin(); - typename sbuffer::const_iterator end = p.end(); + typename buffer::const_iterator it = p.begin(); + typename buffer::const_iterator end = p.end(); for (unsigned i = 0; it != end; ++it, ++i) { expr * m = it->second; if (is_pure_monomial(m)) { @@ -1418,13 +1418,13 @@ unsigned theory_arith::get_degree_of(expr * m, expr * var) { \brief Return the minimal degree of var in the polynomial p. */ template -unsigned theory_arith::get_min_degree(sbuffer & p, expr * var) { +unsigned theory_arith::get_min_degree(buffer & p, expr * var) { SASSERT(!p.empty()); SASSERT(var != 0); // get monomial where the degree of var is min. unsigned d = UINT_MAX; // min. degree of var - sbuffer::const_iterator it = p.begin(); - sbuffer::const_iterator end = p.end(); + buffer::const_iterator it = p.begin(); + buffer::const_iterator end = p.end(); for (; it != end; ++it) { expr * m = it->second; d = std::min(d, get_degree_of(m, var)); @@ -1475,7 +1475,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(unsigned depth, sbuffer & p, expr * var) { +expr * theory_arith::horner(unsigned depth, buffer & p, expr * var) { SASSERT(!p.empty()); SASSERT(var != 0); unsigned d = get_min_degree(p, var); @@ -1483,8 +1483,8 @@ expr * theory_arith::horner(unsigned depth, sbuffer & p, expr * for (unsigned i = 0; i < p.size(); i++) { if (i > 0) tout << " + "; tout << p[i].first << "*" << mk_pp(p[i].second, get_manager()); } tout << "\n"; tout << "var: " << mk_pp(var, get_manager()) << "\n"; tout << "min_degree: " << d << "\n";); - sbuffer e; // monomials/x^d where var occurs with degree d - sbuffer r; // rest + buffer e; // monomials/x^d where var occurs with degree d + buffer r; // rest for (auto const& kv : p) { expr * m = kv.second; expr * f = factor(m, var, d); @@ -1521,7 +1521,7 @@ expr * theory_arith::horner(unsigned depth, sbuffer & p, expr * If var != 0, then it is used for performing the horner extension */ template - expr * theory_arith::cross_nested(unsigned depth, sbuffer & p, expr * var) { + expr * theory_arith::cross_nested(unsigned depth, buffer & p, expr * var) { TRACE("non_linear", tout << "p.size: " << p.size() << "\n";); if (var == nullptr) { sbuffer varinfo; @@ -1588,7 +1588,7 @@ template new_expr = b.is_one() ? rhs2 : m_util.mk_mul(m_util.mk_numeral(b, m_util.is_int(var)), rhs2); m_nl_new_exprs.push_back(new_expr); TRACE("non_linear", tout << "new_expr:\n"; display_nested_form(tout, new_expr); tout << "\n";); - sbuffer rest; + buffer rest; unsigned sz = p.size(); for (unsigned i = 0; i < sz; i++) { if (i != i1 && i != i2) @@ -1612,7 +1612,7 @@ template bounds. The polynomial is converted into an equivalent cross nested form. */ template -bool theory_arith::is_cross_nested_consistent(sbuffer & p) { +bool theory_arith::is_cross_nested_consistent(buffer & p) { sbuffer varinfo; if (!get_polynomial_info(p, varinfo)) return true; @@ -1706,7 +1706,7 @@ bool theory_arith::is_cross_nested_consistent(row const & r) { c = r.get_denominators_lcm().to_rational(); TRACE("non_linear", tout << "check problematic row:\n"; display_row(tout, r); display_row(tout, r, false);); - sbuffer p; + buffer p; for (auto & col : r) { if (!col.is_dead()) { p.push_back(coeff_expr(col.m_coeff.to_rational() * c, var2expr(col.m_var)));