mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2019-06-05 16:10:31 -07:00
commit fdfb9e4fd5
3 changed files with 20 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/python/z3/z3.py
View file

@ -9394,7 +9394,7 @@ def _mk_fp_unary_norm(f, a, ctx):
[a] = _coerce_fp_expr_list([a], ctx) [a] = _coerce_fp_expr_list([a], ctx)
if z3_debug(): if z3_debug():
_z3_assert(is_fp(a), "First argument must be a Z3 floating-point expression") _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): def _mk_fp_unary_pred(f, a, ctx):
ctx = _get_ctx(ctx) ctx = _get_ctx(ctx)

17
src/math/polynomial/upolynomial.cpp
View file

@ -832,7 +832,7 @@ namespace upolynomial {
set(sz2, p2, B); set(sz2, p2, B);
TRACE("upolynomial", tout << "sz1: " << sz1 << ", p1: " << p1 << ", sz2: " << sz2 << ", p2: " << p2 << "\nB.size(): " << B.size() << TRACE("upolynomial", tout << "sz1: " << sz1 << ", p1: " << p1 << ", sz2: " << sz2 << ", p2: " << p2 << "\nB.size(): " << B.size() <<
", B.c_ptr(): " << B.c_ptr() << "\n";); ", 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";); TRACE("upolynomial", tout << "A: "; display(tout, A); tout <<"\nB: "; display(tout, B); tout << "\n";);
if (B.empty()) { if (B.empty()) {
normalize(A); normalize(A);
@ -853,6 +853,7 @@ namespace upolynomial {
A.swap(B); A.swap(B);
B.swap(R); 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) { 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 // 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; bool displayed = false;
unsigned i = sz; unsigned i = sz;
scoped_numeral a(m()); scoped_numeral a(m());
@ -1142,6 +1143,7 @@ namespace upolynomial {
} }
if (!displayed) if (!displayed)
out << "0"; out << "0";
return out;
} }
static void display_smt2_mumeral(std::ostream & out, numeral_manager & m, mpz const & n) { 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 // 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) { if (sz == 0) {
out << "0"; out << "0";
return; return out;
} }
if (sz == 1) { if (sz == 1) {
display_smt2_mumeral(out, m(), p[0]); display_smt2_mumeral(out, m(), p[0]);
return; return out;
} }
unsigned non_zero_idx = UINT_MAX; unsigned non_zero_idx = UINT_MAX;
@ -1217,7 +1219,7 @@ namespace upolynomial {
display_smt2_monomial(out, m(), p[i], i, var_name); 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) { bool core_manager::eq(unsigned sz1, numeral const * p1, unsigned sz2, numeral const * p2) {
@ -3115,11 +3117,12 @@ namespace upolynomial {
return result; 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++) { for (unsigned i = 0; i < seq.size(); i++) {
display(out, seq.size(i), seq.coeffs(i), var_name); display(out, seq.size(i), seq.coeffs(i), var_name);
out << "\n"; out << "\n";
} }
return out;
} }
}; };

18
src/math/polynomial/upolynomial.h
View file

@ -460,13 +460,13 @@ namespace upolynomial {
bool eq(unsigned sz1, numeral const * p1, unsigned sz2, numeral const * p2); 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()); } 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; std::ostream& 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); } 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); }
void display_star(std::ostream & out, unsigned sz, numeral const * p) { display(out, sz, p, "x", true); } std::ostream& display_star(std::ostream & out, unsigned sz, numeral const * p) { return 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_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; std::ostream& 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, numeral_vector const & p, char const * var_name = "x") const {
return display_smt2(out, p.size(), p.c_ptr(), var_name); 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(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); } 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); 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); 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;
}; };
}; };