mirror of
https://github.com/Z3Prover/z3
synced 2025-04-05 17:14:07 +00:00
parent
2ae476416c
commit
4601d1d664
|
@ -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);
|
||||
}
|
||||
|
|
|
@ -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); }
|
||||
|
|
|
@ -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.
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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";
|
||||
}
|
||||
}
|
||||
};
|
||||
|
|
|
@ -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());
|
||||
|
|
Loading…
Reference in a new issue