mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

Portability fixes

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-09-15 21:13:47 +01:00
parent 05447d612a
commit 65697eb277
3 changed files with 32 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -2582,7 +2582,7 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
unsigned ebits = m_util.get_ebits(s); unsigned ebits = m_util.get_ebits(s);
unsigned sbits = m_util.get_sbits(s); unsigned sbits = m_util.get_sbits(s);
if (m_bv_util.is_numeral(bv_rm) && m_util.arith_util().is_numeral(x)) { if (m_bv_util.is_numeral(bv_rm) && m_util.au().is_numeral(x)) {
rational tmp_rat; unsigned sz; rational tmp_rat; unsigned sz;
m_bv_util.is_numeral(to_expr(bv_rm), tmp_rat, sz); m_bv_util.is_numeral(to_expr(bv_rm), tmp_rat, sz);
SASSERT(tmp_rat.is_int32()); SASSERT(tmp_rat.is_int32());
@ -2600,7 +2600,7 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
rational q; rational q;
bool is_int; bool is_int;
m_util.arith_util().is_numeral(x, q, is_int); m_util.au().is_numeral(x, q, is_int);
if (q.is_zero()) if (q.is_zero())
return mk_pzero(f, result); return mk_pzero(f, result);
@ -2617,12 +2617,12 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
result = m_util.mk_fp(sgn, exp, sig); result = m_util.mk_fp(sgn, exp, sig);
} }
} }
else if (m_util.arith_util().is_numeral(x)) { else if (m_util.au().is_numeral(x)) {
rational q; rational q;
bool is_int; bool is_int;
m_util.arith_util().is_numeral(x, q, is_int); m_util.au().is_numeral(x, q, is_int);
if (m_util.arith_util().is_zero(x)) if (m_util.au().is_zero(x))
mk_pzero(f, result); mk_pzero(f, result);
else { else {
expr_ref rm_nta(m), rm_nte(m), rm_tp(m), rm_tn(m), rm_tz(m); expr_ref rm_nta(m), rm_nte(m), rm_tp(m), rm_tn(m), rm_tz(m);
@ -3317,7 +3317,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
last = m_bv_util.mk_extract(big_sig_sz-(bv_sz+3), big_sig_sz-(bv_sz+3), big_sig_shifted); last = m_bv_util.mk_extract(big_sig_sz-(bv_sz+3), big_sig_sz-(bv_sz+3), big_sig_shifted);
round = m_bv_util.mk_extract(big_sig_sz-(bv_sz+4), big_sig_sz-(bv_sz+4), big_sig_shifted); round = m_bv_util.mk_extract(big_sig_sz-(bv_sz+4), big_sig_sz-(bv_sz+4), big_sig_shifted);
stickies = m_bv_util.mk_extract(big_sig_sz-(bv_sz+5), 0, big_sig_shifted); stickies = m_bv_util.mk_extract(big_sig_sz-(bv_sz+5), 0, big_sig_shifted);
sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, stickies); sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, stickies.get());
dbg_decouple("fpa2bv_to_bv_big_sig_shifted", big_sig_shifted); dbg_decouple("fpa2bv_to_bv_big_sig_shifted", big_sig_shifted);
dbg_decouple("fpa2bv_to_bv_int_part", int_part); dbg_decouple("fpa2bv_to_bv_int_part", int_part);
dbg_decouple("fpa2bv_to_bv_last", last); dbg_decouple("fpa2bv_to_bv_last", last);

4
src/ast/fpa_decl_plugin.h
View file

@ -221,8 +221,8 @@ public:
mpf_manager & fm() const { return m_plugin->fm(); } mpf_manager & fm() const { return m_plugin->fm(); }
family_id get_fid() const { return m_fid; } family_id get_fid() const { return m_fid; }
family_id get_family_id() const { return m_fid; } family_id get_family_id() const { return m_fid; }
arith_util & arith_util() { return m_a_util; } arith_util & au() { return m_a_util; }
bv_util & bv_util() { return m_bv_util; } bv_util & bu() { return m_bv_util; }
fpa_decl_plugin & plugin() { return *m_plugin; } fpa_decl_plugin & plugin() { return *m_plugin; }
sort * mk_float_sort(unsigned ebits, unsigned sbits); sort * mk_float_sort(unsigned ebits, unsigned sbits);

48
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -121,7 +121,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
unsigned sbits = f->get_parameter(1).get_int(); unsigned sbits = f->get_parameter(1).get_int();
if (num_args == 1) { if (num_args == 1) {
if (m_util.bv_util().is_numeral(args[0], r1, bvs1)) { if (m_util.bu().is_numeral(args[0], r1, bvs1)) {
// BV -> float // BV -> float
SASSERT(bvs1 == sbits + ebits); SASSERT(bvs1 == sbits + ebits);
unsynch_mpz_manager & mpzm = m_fm.mpz_manager(); unsynch_mpz_manager & mpzm = m_fm.mpz_manager();
@ -162,7 +162,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
if (!m_util.is_rm_numeral(args[0], rmv)) if (!m_util.is_rm_numeral(args[0], rmv))
return BR_FAILED; return BR_FAILED;
if (m_util.arith_util().is_numeral(args[1], r1)) { if (m_util.au().is_numeral(args[1], r1)) {
// rm + real -> float // rm + real -> float
TRACE("fp_rewriter", tout << "r: " << r1 << std::endl;); TRACE("fp_rewriter", tout << "r: " << r1 << std::endl;);
scoped_mpf v(m_fm); scoped_mpf v(m_fm);
@ -180,10 +180,10 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
// TRACE("fp_rewriter", tout << "result: " << result << std::endl; ); // TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
return BR_DONE; return BR_DONE;
} }
else if (m_util.bv_util().is_numeral(args[1], r1, bvs1)) { else if (m_util.bu().is_numeral(args[1], r1, bvs1)) {
// rm + signed bv -> float // rm + signed bv -> float
TRACE("fp_rewriter", tout << "r1: " << r1 << std::endl;); TRACE("fp_rewriter", tout << "r1: " << r1 << std::endl;);
r1 = m_util.bv_util().norm(r1, bvs1, true); r1 = m_util.bu().norm(r1, bvs1, true);
TRACE("fp_rewriter", tout << "r1 norm: " << r1 << std::endl;); TRACE("fp_rewriter", tout << "r1 norm: " << r1 << std::endl;);
m_fm.set(v, ebits, sbits, rmv, r1.to_mpq()); m_fm.set(v, ebits, sbits, rmv, r1.to_mpq());
result = m_util.mk_value(v); result = m_util.mk_value(v);
@ -192,12 +192,12 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
} }
else if (num_args == 3) { else if (num_args == 3) {
if (m_util.is_rm_numeral(args[0], rmv) && if (m_util.is_rm_numeral(args[0], rmv) &&
m_util.arith_util().is_real(args[1]) && m_util.au().is_real(args[1]) &&
m_util.arith_util().is_int(args[2])) { m_util.au().is_int(args[2])) {
// rm + real + int -> float // rm + real + int -> float
if (!m_util.is_rm_numeral(args[0], rmv) || if (!m_util.is_rm_numeral(args[0], rmv) ||
!m_util.arith_util().is_numeral(args[1], r1) || !m_util.au().is_numeral(args[1], r1) ||
!m_util.arith_util().is_numeral(args[2], r2)) !m_util.au().is_numeral(args[2], r2))
return BR_FAILED; return BR_FAILED;
TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";); TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";);
@ -206,12 +206,12 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
return BR_DONE; return BR_DONE;
} }
else if (m_util.is_rm_numeral(args[0], rmv) && else if (m_util.is_rm_numeral(args[0], rmv) &&
m_util.arith_util().is_int(args[1]) && m_util.au().is_int(args[1]) &&
m_util.arith_util().is_real(args[2])) { m_util.au().is_real(args[2])) {
// rm + int + real -> float // rm + int + real -> float
if (!m_util.is_rm_numeral(args[0], rmv) || if (!m_util.is_rm_numeral(args[0], rmv) ||
!m_util.arith_util().is_numeral(args[1], r1) || !m_util.au().is_numeral(args[1], r1) ||
!m_util.arith_util().is_numeral(args[2], r2)) !m_util.au().is_numeral(args[2], r2))
return BR_FAILED; return BR_FAILED;
TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";); TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";);
@ -219,9 +219,9 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
result = m_util.mk_value(v); result = m_util.mk_value(v);
return BR_DONE; return BR_DONE;
} }
else if (m_util.bv_util().is_numeral(args[0], r1, bvs1) && else if (m_util.bu().is_numeral(args[0], r1, bvs1) &&
m_util.bv_util().is_numeral(args[1], r2, bvs2) && m_util.bu().is_numeral(args[1], r2, bvs2) &&
m_util.bv_util().is_numeral(args[2], r3, bvs3)) { m_util.bu().is_numeral(args[2], r3, bvs3)) {
// 3 BV -> float // 3 BV -> float
SASSERT(m_fm.mpz_manager().is_one(r2.to_mpq().denominator())); SASSERT(m_fm.mpz_manager().is_one(r2.to_mpq().denominator()));
SASSERT(m_fm.mpz_manager().is_one(r3.to_mpq().denominator())); SASSERT(m_fm.mpz_manager().is_one(r3.to_mpq().denominator()));
@ -251,7 +251,7 @@ br_status fpa_rewriter::mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg
unsigned bvs; unsigned bvs;
if (m_util.is_rm_numeral(arg1, rmv) && if (m_util.is_rm_numeral(arg1, rmv) &&
m_util.bv_util().is_numeral(arg2, r, bvs)) { m_util.bu().is_numeral(arg2, r, bvs)) {
scoped_mpf v(m_fm); scoped_mpf v(m_fm);
m_fm.set(v, ebits, sbits, rmv, r.to_mpq()); m_fm.set(v, ebits, sbits, rmv, r.to_mpq());
result = m_util.mk_value(v); result = m_util.mk_value(v);
@ -722,7 +722,7 @@ br_status fpa_rewriter::mk_bv2rm(expr * arg, expr_ref & result) {
rational bv_val; rational bv_val;
unsigned sz = 0; unsigned sz = 0;
if (m_util.bv_util().is_numeral(arg, bv_val, sz)) { if (m_util.bu().is_numeral(arg, bv_val, sz)) {
SASSERT(bv_val.is_uint64()); SASSERT(bv_val.is_uint64());
switch (bv_val.get_uint64()) { switch (bv_val.get_uint64()) {
case BV_RM_TIES_TO_AWAY: result = m_util.mk_round_nearest_ties_to_away(); break; case BV_RM_TIES_TO_AWAY: result = m_util.mk_round_nearest_ties_to_away(); break;
@ -744,9 +744,9 @@ br_status fpa_rewriter::mk_fp(expr * sgn, expr * exp, expr * sig, expr_ref & res
rational rsgn, rexp, rsig; rational rsgn, rexp, rsig;
unsigned bvsz_sgn, bvsz_exp, bvsz_sig; unsigned bvsz_sgn, bvsz_exp, bvsz_sig;
if (m_util.bv_util().is_numeral(sgn, rsgn, bvsz_sgn) && if (m_util.bu().is_numeral(sgn, rsgn, bvsz_sgn) &&
m_util.bv_util().is_numeral(sig, rsig, bvsz_sig) && m_util.bu().is_numeral(sig, rsig, bvsz_sig) &&
m_util.bv_util().is_numeral(exp, rexp, bvsz_exp)) { m_util.bu().is_numeral(exp, rexp, bvsz_exp)) {
SASSERT(mpzm.is_one(rexp.to_mpq().denominator())); SASSERT(mpzm.is_one(rexp.to_mpq().denominator()));
SASSERT(mpzm.is_one(rsig.to_mpq().denominator())); SASSERT(mpzm.is_one(rsig.to_mpq().denominator()));
scoped_mpf v(m_fm); scoped_mpf v(m_fm);
@ -804,8 +804,8 @@ br_status fpa_rewriter::mk_to_bv(func_decl * f, expr * arg1, expr * arg2, bool i
br_status fpa_rewriter::mk_to_bv_unspecified(func_decl * f, expr_ref & result) { br_status fpa_rewriter::mk_to_bv_unspecified(func_decl * f, expr_ref & result) {
if (m_hi_fp_unspecified) { if (m_hi_fp_unspecified) {
unsigned bv_sz = m_util.bv_util().get_bv_size(f->get_range()); unsigned bv_sz = m_util.bu().get_bv_size(f->get_range());
result = m_util.bv_util().mk_numeral(0, bv_sz); result = m_util.bu().mk_numeral(0, bv_sz);
return BR_DONE; return BR_DONE;
} }
else else
@ -856,14 +856,14 @@ br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) {
if (m_util.is_numeral(arg, v)) { if (m_util.is_numeral(arg, v)) {
if (m_fm.is_nan(v) || m_fm.is_inf(v)) { if (m_fm.is_nan(v) || m_fm.is_inf(v)) {
if (m_hi_fp_unspecified) { if (m_hi_fp_unspecified) {
result = m_util.arith_util().mk_numeral(rational(0), false); result = m_util.au().mk_numeral(rational(0), false);
return BR_DONE; return BR_DONE;
} }
} }
else { else {
scoped_mpq r(m_fm.mpq_manager()); scoped_mpq r(m_fm.mpq_manager());
m_fm.to_rational(v, r); m_fm.to_rational(v, r);
result = m_util.arith_util().mk_numeral(r.get(), false); result = m_util.au().mk_numeral(r.get(), false);
return BR_DONE; return BR_DONE;
} }
} }