From 4601d1d66493c7fad1fce472188bd3c505c8e453 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 24 Jan 2023 03:37:09 -0800 Subject: [PATCH] fix #6550 Signed-off-by: Nikolaj Bjorner --- src/api/api_arith.cpp | 4 ++-- src/api/c++/z3++.h | 4 ++-- src/api/z3_api.h | 4 ++-- src/ast/rewriter/arith_rewriter.cpp | 2 +- src/smt/theory_bv.cpp | 2 +- src/smt/theory_fpa.cpp | 11 ++++------- src/smt/theory_lra.cpp | 4 ++-- 7 files changed, 14 insertions(+), 17 deletions(-) diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp index 9671dbc26..c0d599de7 100644 --- a/src/api/api_arith.cpp +++ b/src/api/api_arith.cpp @@ -48,7 +48,7 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } - Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den) { + Z3_ast Z3_API Z3_mk_real(Z3_context c, int64_t num, int64_t den) { Z3_TRY; LOG_Z3_mk_real(c, num, den); RESET_ERROR_CODE(); @@ -57,7 +57,7 @@ extern "C" { RETURN_Z3(nullptr); } sort* s = mk_c(c)->m().mk_sort(mk_c(c)->get_arith_fid(), REAL_SORT); - ast* a = mk_c(c)->mk_numeral_core(rational(num, den), s); + ast* a = mk_c(c)->mk_numeral_core(rational(num, rational::i64())/rational(den, rational::i64()), s); RETURN_Z3(of_ast(a)); Z3_CATCH_RETURN(nullptr); } diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index ec7b451fa..9d4ddcfb4 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -400,11 +400,11 @@ namespace z3 { expr int_val(uint64_t n); expr int_val(char const * n); - expr real_val(int n, int d); expr real_val(int n); expr real_val(unsigned n); expr real_val(int64_t n); expr real_val(uint64_t n); + expr real_val(int64_t n, int64_t d); expr real_val(char const * n); expr bv_val(int n, unsigned sz); @@ -3630,7 +3630,7 @@ namespace z3 { inline expr context::int_val(uint64_t n) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); } inline expr context::int_val(char const * n) { Z3_ast r = Z3_mk_numeral(m_ctx, n, int_sort()); check_error(); return expr(*this, r); } - inline expr context::real_val(int n, int d) { Z3_ast r = Z3_mk_real(m_ctx, n, d); check_error(); return expr(*this, r); } + inline expr context::real_val(int64_t n, int64_t d) { Z3_ast r = Z3_mk_real(m_ctx, n, d); check_error(); return expr(*this, r); } inline expr context::real_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); } inline expr context::real_val(unsigned n) { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); } inline expr context::real_val(int64_t n) { Z3_ast r = Z3_mk_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); } diff --git a/src/api/z3_api.h b/src/api/z3_api.h index ffa0d8665..fd85dd781 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -3419,9 +3419,9 @@ extern "C" { \sa Z3_mk_int \sa Z3_mk_unsigned_int - def_API('Z3_mk_real', AST, (_in(CONTEXT), _in(INT), _in(INT))) + def_API('Z3_mk_real', AST, (_in(CONTEXT), _in(INT64), _in(INT64))) */ - Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den); + Z3_ast Z3_API Z3_mk_real(Z3_context c, int64_t num, int64_t den); /** \brief Create a numeral of an int, bit-vector, or finite-domain sort. diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 15456d41e..7cade3bfa 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1321,7 +1321,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res bool is_num_y = m_util.is_numeral(arg2, y); auto ensure_real = [&](expr* e) { return m_util.is_int(e) ? m_util.mk_to_real(e) : e; }; - TRACE("arith", tout << mk_pp(arg1, m) << " " << mk_pp(arg2, m) << "\n";); + TRACE("arith", tout << mk_bounded_pp(arg1, m) << " " << mk_bounded_pp(arg2, m) << "\n";); if (is_num_x && x.is_one()) { result = m_util.mk_numeral(x, false); return BR_DONE; diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 62b7a2a20..b3a6e77ff 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -1379,7 +1379,7 @@ namespace smt { } void theory_bv::relevant_eh(app * n) { - TRACE("arith", tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_pp(n, m) << "\n";); + TRACE("arith", tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_bounded_pp(n, m) << "\n";); TRACE("bv", tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_pp(n, m) << "\n";); if (m.is_bool(n)) { bool_var v = ctx.get_bool_var(n); diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index ee547b22d..d63ff93cd 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -650,8 +650,7 @@ namespace smt { theory_var v = n->get_th_var(get_family_id()); if (v != -1) { if (first) out << "fpa theory variables:" << std::endl; - out << v << " -> " << - mk_ismt2_pp(n->get_expr(), m) << std::endl; + out << v << " -> " << enode_pp(n, ctx) << "\n"; first = false; } } @@ -661,22 +660,20 @@ namespace smt { out << "bv theory variables:" << std::endl; for (enode * n : ctx.enodes()) { theory_var v = n->get_th_var(m_bv_util.get_family_id()); - if (v != -1) out << v << " -> " << - mk_ismt2_pp(n->get_expr(), m) << std::endl; + if (v != -1) out << v << " -> " << enode_pp(n, ctx) << "\n"; } out << "arith theory variables:" << std::endl; for (enode* n : ctx.enodes()) { theory_var v = n->get_th_var(m_arith_util.get_family_id()); - if (v != -1) out << v << " -> " << - mk_ismt2_pp(n->get_expr(), m) << std::endl; + if (v != -1) out << v << " -> " << enode_pp(n, ctx) << "\n"; } out << "equivalence classes:\n"; for (enode * n : ctx.enodes()) { expr * e = n->get_expr(); expr * r = n->get_root()->get_expr(); - out << r->get_id() << " --> " << mk_ismt2_pp(e, m) << std::endl; + out << r->get_id() << " --> " << enode_pp(n, ctx) << "\n"; } } }; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index df5f12313..01282a53b 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1004,7 +1004,7 @@ public: } void assign_eh(bool_var v, bool is_true) { - TRACE("arith", tout << mk_pp(ctx().bool_var2expr(v), m) << " " << (literal(v, !is_true)) << "\n";); + TRACE("arith", tout << mk_bounded_pp(ctx().bool_var2expr(v), m) << " " << (literal(v, !is_true)) << "\n";); m_asserted_atoms.push_back(delayed_atom(v, is_true)); } @@ -1049,7 +1049,7 @@ public: } void apply_sort_cnstr(enode* n, sort*) { - TRACE("arith", tout << "sort constraint: " << pp(n, m) << "\n";); + TRACE("arith", tout << "sort constraint: " << enode_pp(n, ctx()) << "\n";); #if 0 if (!th.is_attached_to_var(n)) { mk_var(n->get_owner());