diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 1a6e9c43f..0c75edbf6 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -9394,7 +9394,7 @@ def _mk_fp_unary_norm(f, a, ctx): [a] = _coerce_fp_expr_list([a], ctx) if z3_debug(): _z3_assert(is_fp(a), "First argument must be a Z3 floating-point expression") - return FPRef(f(ctx.ref(), a.as_ast()), ctx) + return BoolRef(f(ctx.ref(), a.as_ast()), ctx) def _mk_fp_unary_pred(f, a, ctx): ctx = _get_ctx(ctx) diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp index 65dbf91f4..9c43d88ec 100644 --- a/src/math/polynomial/upolynomial.cpp +++ b/src/math/polynomial/upolynomial.cpp @@ -832,7 +832,7 @@ namespace upolynomial { set(sz2, p2, B); TRACE("upolynomial", tout << "sz1: " << sz1 << ", p1: " << p1 << ", sz2: " << sz2 << ", p2: " << p2 << "\nB.size(): " << B.size() << ", B.c_ptr(): " << B.c_ptr() << "\n";); - while (true) { + while (m_limit.inc()) { TRACE("upolynomial", tout << "A: "; display(tout, A); tout <<"\nB: "; display(tout, B); tout << "\n";); if (B.empty()) { normalize(A); @@ -853,6 +853,7 @@ namespace upolynomial { A.swap(B); B.swap(R); } + throw upolynomial_exception(Z3_CANCELED_MSG); } void core_manager::gcd(unsigned sz1, numeral const * p1, unsigned sz2, numeral const * p2, numeral_vector & buffer) { @@ -1106,7 +1107,7 @@ namespace upolynomial { } // Display p - void core_manager::display(std::ostream & out, unsigned sz, numeral const * p, char const * var_name, bool use_star) const { + std::ostream& core_manager::display(std::ostream & out, unsigned sz, numeral const * p, char const * var_name, bool use_star) const { bool displayed = false; unsigned i = sz; scoped_numeral a(m()); @@ -1142,6 +1143,7 @@ namespace upolynomial { } if (!displayed) out << "0"; + return out; } static void display_smt2_mumeral(std::ostream & out, numeral_manager & m, mpz const & n) { @@ -1183,15 +1185,15 @@ namespace upolynomial { } // Display p as an s-expression - void core_manager::display_smt2(std::ostream & out, unsigned sz, numeral const * p, char const * var_name) const { + std::ostream& core_manager::display_smt2(std::ostream & out, unsigned sz, numeral const * p, char const * var_name) const { if (sz == 0) { out << "0"; - return; + return out; } if (sz == 1) { display_smt2_mumeral(out, m(), p[0]); - return; + return out; } unsigned non_zero_idx = UINT_MAX; @@ -1217,7 +1219,7 @@ namespace upolynomial { display_smt2_monomial(out, m(), p[i], i, var_name); } } - out << ")"; + return out << ")"; } bool core_manager::eq(unsigned sz1, numeral const * p1, unsigned sz2, numeral const * p2) { @@ -3115,11 +3117,12 @@ namespace upolynomial { return result; } - void manager::display(std::ostream & out, upolynomial_sequence const & seq, char const * var_name) const { + std::ostream& manager::display(std::ostream & out, upolynomial_sequence const & seq, char const * var_name) const { for (unsigned i = 0; i < seq.size(); i++) { display(out, seq.size(i), seq.coeffs(i), var_name); out << "\n"; } + return out; } }; diff --git a/src/math/polynomial/upolynomial.h b/src/math/polynomial/upolynomial.h index ad6942ffb..52115ebc1 100644 --- a/src/math/polynomial/upolynomial.h +++ b/src/math/polynomial/upolynomial.h @@ -460,13 +460,13 @@ namespace upolynomial { bool eq(unsigned sz1, numeral const * p1, unsigned sz2, numeral const * p2); bool eq(numeral_vector const & p1, numeral_vector const & p2) { return eq(p1.size(), p1.c_ptr(), p2.size(), p2.c_ptr()); } - void display(std::ostream & out, unsigned sz, numeral const * p, char const * var_name = "x", bool use_star = false) const; - void display(std::ostream & out, numeral_vector const & p, char const * var_name = "x") const { display(out, p.size(), p.c_ptr(), var_name); } - void display_star(std::ostream & out, unsigned sz, numeral const * p) { display(out, sz, p, "x", true); } - void display_star(std::ostream & out, numeral_vector const & p) { display_star(out, p.size(), p.c_ptr()); } + std::ostream& display(std::ostream & out, unsigned sz, numeral const * p, char const * var_name = "x", bool use_star = false) const; + std::ostream& display(std::ostream & out, numeral_vector const & p, char const * var_name = "x") const { return display(out, p.size(), p.c_ptr(), var_name); } + std::ostream& display_star(std::ostream & out, unsigned sz, numeral const * p) { return display(out, sz, p, "x", true); } + std::ostream& display_star(std::ostream & out, numeral_vector const & p) { return display_star(out, p.size(), p.c_ptr()); } - void display_smt2(std::ostream & out, unsigned sz, numeral const * p, char const * var_name = "x") const; - void display_smt2(std::ostream & out, numeral_vector const & p, char const * var_name = "x") const { + std::ostream& display_smt2(std::ostream & out, unsigned sz, numeral const * p, char const * var_name = "x") const; + std::ostream& display_smt2(std::ostream & out, numeral_vector const & p, char const * var_name = "x") const { return display_smt2(out, p.size(), p.c_ptr(), var_name); } }; @@ -908,13 +908,13 @@ namespace upolynomial { bool factor(unsigned sz, numeral const * p, factors & r, factor_params const & params = factor_params()); bool factor(numeral_vector const & p, factors & r, factor_params const & params = factor_params()) { return factor(p.size(), p.c_ptr(), r, params); } - void display(std::ostream & out, unsigned sz, numeral const * p, char const * var_name = "x", bool use_star = false) const { + std::ostream& display(std::ostream & out, unsigned sz, numeral const * p, char const * var_name = "x", bool use_star = false) const { return core_manager::display(out, sz, p, var_name); } - void display(std::ostream & out, numeral_vector const & p, char const * var_name = "x") const { + std::ostream& display(std::ostream & out, numeral_vector const & p, char const * var_name = "x") const { return core_manager::display(out, p, var_name); } - void display(std::ostream & out, upolynomial_sequence const & seq, char const * var_name = "x") const; + std::ostream& display(std::ostream & out, upolynomial_sequence const & seq, char const * var_name = "x") const; }; };