mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

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

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-10-30 06:31:22 -07:00
commit 4923b50c53
4 changed files with 137 additions and 136 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -33,7 +33,7 @@ void fpa_rewriter::updt_params(params_ref const & _p) {
fpa_rewriter_params p(_p); fpa_rewriter_params p(_p);
m_hi_fp_unspecified = p.hi_fp_unspecified(); m_hi_fp_unspecified = p.hi_fp_unspecified();
} }
void fpa_rewriter::get_param_descrs(param_descrs & r) { void fpa_rewriter::get_param_descrs(param_descrs & r) {
} }
@ -72,7 +72,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_FPA_SQRT: SASSERT(num_args == 2); st = mk_sqrt(args[0], args[1], result); break; case OP_FPA_SQRT: SASSERT(num_args == 2); st = mk_sqrt(args[0], args[1], result); break;
case OP_FPA_ROUND_TO_INTEGRAL: SASSERT(num_args == 2); st = mk_round_to_integral(args[0], args[1], result); break; case OP_FPA_ROUND_TO_INTEGRAL: SASSERT(num_args == 2); st = mk_round_to_integral(args[0], args[1], result); break;
case OP_FPA_EQ: SASSERT(num_args == 2); st = mk_float_eq(args[0], args[1], result); break; case OP_FPA_EQ: SASSERT(num_args == 2); st = mk_float_eq(args[0], args[1], result); break;
case OP_FPA_LT: SASSERT(num_args == 2); st = mk_lt(args[0], args[1], result); break; case OP_FPA_LT: SASSERT(num_args == 2); st = mk_lt(args[0], args[1], result); break;
case OP_FPA_GT: SASSERT(num_args == 2); st = mk_gt(args[0], args[1], result); break; case OP_FPA_GT: SASSERT(num_args == 2); st = mk_gt(args[0], args[1], result); break;
case OP_FPA_LE: SASSERT(num_args == 2); st = mk_le(args[0], args[1], result); break; case OP_FPA_LE: SASSERT(num_args == 2); st = mk_le(args[0], args[1], result); break;
@ -83,29 +83,29 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_FPA_IS_NORMAL: SASSERT(num_args == 1); st = mk_is_normal(args[0], result); break; case OP_FPA_IS_NORMAL: SASSERT(num_args == 1); st = mk_is_normal(args[0], result); break;
case OP_FPA_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break; case OP_FPA_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break;
case OP_FPA_IS_NEGATIVE: SASSERT(num_args == 1); st = mk_is_negative(args[0], result); break; case OP_FPA_IS_NEGATIVE: SASSERT(num_args == 1); st = mk_is_negative(args[0], result); break;
case OP_FPA_IS_POSITIVE: SASSERT(num_args == 1); st = mk_is_positive(args[0], result); break; case OP_FPA_IS_POSITIVE: SASSERT(num_args == 1); st = mk_is_positive(args[0], result); break;
case OP_FPA_FP: SASSERT(num_args == 3); st = mk_fp(args[0], args[1], args[2], result); break; case OP_FPA_FP: SASSERT(num_args == 3); st = mk_fp(args[0], args[1], args[2], result); break;
case OP_FPA_TO_FP: st = mk_to_fp(f, num_args, args, result); break; case OP_FPA_TO_FP: st = mk_to_fp(f, num_args, args, result); break;
case OP_FPA_TO_FP_UNSIGNED: SASSERT(num_args == 2); st = mk_to_fp_unsigned(f, args[0], args[1], result); break; case OP_FPA_TO_FP_UNSIGNED: SASSERT(num_args == 2); st = mk_to_fp_unsigned(f, args[0], args[1], result); break;
case OP_FPA_TO_UBV: SASSERT(num_args == 2); st = mk_to_ubv(f, args[0], args[1], result); break; case OP_FPA_TO_UBV: SASSERT(num_args == 2); st = mk_to_ubv(f, args[0], args[1], result); break;
case OP_FPA_TO_SBV: SASSERT(num_args == 2); st = mk_to_sbv(f, args[0], args[1], result); break; case OP_FPA_TO_SBV: SASSERT(num_args == 2); st = mk_to_sbv(f, args[0], args[1], result); break;
case OP_FPA_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(f, args[0], result); break; case OP_FPA_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(f, args[0], result); break;
case OP_FPA_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break; case OP_FPA_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break;
case OP_FPA_INTERNAL_MIN_I: case OP_FPA_INTERNAL_MIN_I:
case OP_FPA_INTERNAL_MAX_I: case OP_FPA_INTERNAL_MAX_I:
case OP_FPA_INTERNAL_MIN_UNSPECIFIED: case OP_FPA_INTERNAL_MIN_UNSPECIFIED:
case OP_FPA_INTERNAL_MAX_UNSPECIFIED: case OP_FPA_INTERNAL_MAX_UNSPECIFIED:
SASSERT(num_args == 2); st = BR_FAILED; break; SASSERT(num_args == 2); st = BR_FAILED; break;
case OP_FPA_INTERNAL_RM: case OP_FPA_INTERNAL_RM:
SASSERT(num_args == 1); st = mk_rm(args[0], result); break; SASSERT(num_args == 1); st = mk_rm(args[0], result); break;
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
SASSERT(num_args == 0); st = mk_to_ubv_unspecified(f, result); break; SASSERT(num_args == 0); st = mk_to_ubv_unspecified(f, result); break;
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
SASSERT(num_args == 0); st = mk_to_sbv_unspecified(f, result); break; SASSERT(num_args == 0); st = mk_to_sbv_unspecified(f, result); break;
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
SASSERT(num_args == 0); st = mk_to_real_unspecified(result); break; SASSERT(num_args == 0); st = mk_to_real_unspecified(result); break;
case OP_FPA_INTERNAL_BVWRAP: case OP_FPA_INTERNAL_BVWRAP:
@ -113,7 +113,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
st = BR_FAILED; st = BR_FAILED;
break; break;
default: default:
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
} }
return st; return st;
@ -171,7 +171,7 @@ br_status fpa_rewriter::mk_to_real_unspecified(expr_ref & result) {
else else
result = m_util.mk_internal_to_real_unspecified(); result = m_util.mk_internal_to_real_unspecified();
return BR_DONE; return BR_DONE;
} }
br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
@ -186,7 +186,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
unsigned ebits = f->get_parameter(0).get_int(); unsigned ebits = f->get_parameter(0).get_int();
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 (bu.is_numeral(args[0], r1, bvs1)) { if (bu.is_numeral(args[0], r1, bvs1)) {
// BV -> float // BV -> float
SASSERT(bvs1 == sbits + ebits); SASSERT(bvs1 == sbits + ebits);
@ -196,13 +196,13 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
const mpz & sm1 = m_fm.m_powers2(sbits - 1); const mpz & sm1 = m_fm.m_powers2(sbits - 1);
const mpz & em1 = m_fm.m_powers2(ebits); const mpz & em1 = m_fm.m_powers2(ebits);
scoped_mpq q(mpqm); scoped_mpq q(mpqm);
mpqm.set(q, r1.to_mpq()); mpqm.set(q, r1.to_mpq());
SASSERT(mpzm.is_one(q.get().denominator())); SASSERT(mpzm.is_one(q.get().denominator()));
scoped_mpz z(mpzm); scoped_mpz z(mpzm);
z = q.get().numerator(); z = q.get().numerator();
mpzm.rem(z, sm1, sig); mpzm.rem(z, sm1, sig);
mpzm.div(z, sm1, z); mpzm.div(z, sm1, z);
@ -214,7 +214,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
mpf_exp = m_fm.unbias_exp(ebits, mpf_exp); mpf_exp = m_fm.unbias_exp(ebits, mpf_exp);
m_fm.set(v, ebits, sbits, !mpzm.is_zero(z), sig, mpf_exp); m_fm.set(v, ebits, sbits, !mpzm.is_zero(z), sig, mpf_exp);
TRACE("fp_rewriter", TRACE("fp_rewriter",
tout << "sgn: " << !mpzm.is_zero(z) << std::endl; tout << "sgn: " << !mpzm.is_zero(z) << std::endl;
tout << "sig: " << mpzm.to_string(sig) << std::endl; tout << "sig: " << mpzm.to_string(sig) << std::endl;
tout << "exp: " << mpf_exp << std::endl; tout << "exp: " << mpf_exp << std::endl;
@ -227,9 +227,9 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
else if (num_args == 2) { else if (num_args == 2) {
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.au().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);
m_fm.set(v, ebits, sbits, rmv, r1.to_mpq()); m_fm.set(v, ebits, sbits, rmv, r1.to_mpq());
@ -246,7 +246,7 @@ 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 (bu.is_numeral(args[1], r1, bvs1)) { else if (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 = bu.norm(r1, bvs1, true); r1 = bu.norm(r1, bvs1, true);
@ -256,7 +256,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
return BR_DONE; return BR_DONE;
} }
} }
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.au().is_real(args[1]) && m_util.au().is_real(args[1]) &&
m_util.au().is_int(args[2])) { m_util.au().is_int(args[2])) {
@ -286,7 +286,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
TRACE("fp_rewriter", tout << "v = " << m_fm.to_string(v) << std::endl;); TRACE("fp_rewriter", tout << "v = " << m_fm.to_string(v) << std::endl;);
result = m_util.mk_value(v); result = m_util.mk_value(v);
return BR_DONE; return BR_DONE;
} }
} }
return BR_FAILED; return BR_FAILED;
@ -296,13 +296,13 @@ br_status fpa_rewriter::mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg
SASSERT(f->get_num_parameters() == 2); SASSERT(f->get_num_parameters() == 2);
SASSERT(f->get_parameter(0).is_int()); SASSERT(f->get_parameter(0).is_int());
SASSERT(f->get_parameter(1).is_int()); SASSERT(f->get_parameter(1).is_int());
bv_util bu(m()); bv_util bu(m());
unsigned ebits = f->get_parameter(0).get_int(); unsigned ebits = f->get_parameter(0).get_int();
unsigned sbits = f->get_parameter(1).get_int(); unsigned sbits = f->get_parameter(1).get_int();
mpf_rounding_mode rmv; mpf_rounding_mode rmv;
rational r; rational r;
unsigned bvs; unsigned bvs;
if (m_util.is_rm_numeral(arg1, rmv) && if (m_util.is_rm_numeral(arg1, rmv) &&
bu.is_numeral(arg2, r, bvs)) { bu.is_numeral(arg2, r, bvs)) {
scoped_mpf v(m_fm); scoped_mpf v(m_fm);
@ -314,7 +314,7 @@ br_status fpa_rewriter::mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg
return BR_FAILED; return BR_FAILED;
} }
br_status fpa_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { br_status fpa_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
mpf_rounding_mode rm; mpf_rounding_mode rm;
if (m_util.is_rm_numeral(arg1, rm)) { if (m_util.is_rm_numeral(arg1, rm)) {
scoped_mpf v2(m_fm), v3(m_fm); scoped_mpf v2(m_fm), v3(m_fm);
@ -335,7 +335,7 @@ br_status fpa_rewriter::mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref &
return BR_REWRITE2; return BR_REWRITE2;
} }
br_status fpa_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { br_status fpa_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
mpf_rounding_mode rm; mpf_rounding_mode rm;
if (m_util.is_rm_numeral(arg1, rm)) { if (m_util.is_rm_numeral(arg1, rm)) {
scoped_mpf v2(m_fm), v3(m_fm); scoped_mpf v2(m_fm), v3(m_fm);
@ -386,7 +386,7 @@ br_status fpa_rewriter::mk_neg(expr * arg1, expr_ref & result) {
result = to_app(arg1)->get_arg(0); result = to_app(arg1)->get_arg(0);
return BR_DONE; return BR_DONE;
} }
scoped_mpf v1(m_fm); scoped_mpf v1(m_fm);
if (m_util.is_numeral(arg1, v1)) { if (m_util.is_numeral(arg1, v1)) {
m_fm.neg(v1); m_fm.neg(v1);
@ -414,14 +414,14 @@ br_status fpa_rewriter::mk_abs(expr * arg1, expr_ref & result) {
result = arg1; result = arg1;
return BR_DONE; return BR_DONE;
} }
scoped_mpf v(m_fm); scoped_mpf v(m_fm);
if (m_util.is_numeral(arg1, v)) { if (m_util.is_numeral(arg1, v)) {
if (m_fm.is_neg(v)) m_fm.neg(v); if (m_fm.is_neg(v)) m_fm.neg(v);
result = m_util.mk_value(v); result = m_util.mk_value(v);
return BR_DONE; return BR_DONE;
} }
return BR_FAILED; return BR_FAILED;
} }
@ -434,7 +434,7 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
result = arg1; result = arg1;
return BR_DONE; return BR_DONE;
} }
scoped_mpf v1(m_fm), v2(m_fm); scoped_mpf v1(m_fm), v2(m_fm);
if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) { if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) {
@ -543,6 +543,7 @@ br_status fpa_rewriter::mk_round_to_integral(expr * arg1, expr * arg2, expr_ref
// This the floating point theory == // This the floating point theory ==
br_status fpa_rewriter::mk_float_eq(expr * arg1, expr * arg2, expr_ref & result) { br_status fpa_rewriter::mk_float_eq(expr * arg1, expr * arg2, expr_ref & result) {
scoped_mpf v1(m_fm), v2(m_fm); scoped_mpf v1(m_fm), v2(m_fm);
if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
result = (m_fm.eq(v1, v2)) ? m().mk_true() : m().mk_false(); result = (m_fm.eq(v1, v2)) ? m().mk_true() : m().mk_false();
return BR_DONE; return BR_DONE;
@ -745,22 +746,22 @@ br_status fpa_rewriter::mk_rm(expr * arg, expr_ref & result) {
case BV_RM_TO_ZERO: case BV_RM_TO_ZERO:
default: result = m_util.mk_round_toward_zero(); default: result = m_util.mk_round_toward_zero();
} }
return BR_DONE; return BR_DONE;
} }
return BR_FAILED; return BR_FAILED;
} }
br_status fpa_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { br_status fpa_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
unsynch_mpz_manager & mpzm = m_fm.mpz_manager(); unsynch_mpz_manager & mpzm = m_fm.mpz_manager();
bv_util bu(m()); bv_util bu(m());
rational r1, r2, r3; rational r1, r2, r3;
unsigned bvs1, bvs2, bvs3; unsigned bvs1, bvs2, bvs3;
if (bu.is_numeral(arg1, r1, bvs1) && if (bu.is_numeral(arg1, r1, bvs1) &&
bu.is_numeral(arg2, r2, bvs2) && bu.is_numeral(arg2, r2, bvs2) &&
bu.is_numeral(arg3, r3, bvs3)) { bu.is_numeral(arg3, r3, bvs3)) {
SASSERT(mpzm.is_one(r2.to_mpq().denominator())); SASSERT(mpzm.is_one(r2.to_mpq().denominator()));
SASSERT(mpzm.is_one(r3.to_mpq().denominator())); SASSERT(mpzm.is_one(r3.to_mpq().denominator()));
SASSERT(mpzm.is_int64(r3.to_mpq().numerator())); SASSERT(mpzm.is_int64(r3.to_mpq().numerator()));
@ -769,7 +770,7 @@ br_status fpa_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref &
m_fm.set(v, bvs2, bvs3 + 1, m_fm.set(v, bvs2, bvs3 + 1,
r1.is_one(), r1.is_one(),
r3.to_mpq().numerator(), r3.to_mpq().numerator(),
m_fm.unbias_exp(bvs2, biased_exp)); m_fm.unbias_exp(bvs2, biased_exp));
TRACE("fp_rewriter", tout << "simplified (fp ...) to " << m_fm.to_string(v) << std::endl;); TRACE("fp_rewriter", tout << "simplified (fp ...) to " << m_fm.to_string(v) << std::endl;);
result = m_util.mk_value(v); result = m_util.mk_value(v);
return BR_DONE; return BR_DONE;
@ -780,24 +781,24 @@ br_status fpa_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref &
br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) { br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) {
SASSERT(f->get_num_parameters() == 1); SASSERT(f->get_num_parameters() == 1);
SASSERT(f->get_parameter(0).is_int()); SASSERT(f->get_parameter(0).is_int());
int bv_sz = f->get_parameter(0).get_int(); int bv_sz = f->get_parameter(0).get_int();
mpf_rounding_mode rmv; mpf_rounding_mode rmv;
scoped_mpf v(m_fm); scoped_mpf v(m_fm);
if (m_util.is_rm_numeral(arg1, rmv) && if (m_util.is_rm_numeral(arg1, rmv) &&
m_util.is_numeral(arg2, v)) { m_util.is_numeral(arg2, v)) {
if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v)) { if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v)) {
mk_to_ubv_unspecified(f, result); mk_to_ubv_unspecified(f, result);
return BR_REWRITE_FULL; return BR_REWRITE_FULL;
} }
bv_util bu(m()); bv_util bu(m());
scoped_mpq q(m_fm.mpq_manager()); scoped_mpq q(m_fm.mpq_manager());
m_fm.to_sbv_mpq(rmv, v, q); m_fm.to_sbv_mpq(rmv, v, q);
rational r(q); rational r(q);
rational ul, ll; rational ul, ll;
ul = m_fm.m_powers2.m1(bv_sz); ul = m_fm.m_powers2.m1(bv_sz);
ll = rational(0); ll = rational(0);
@ -813,7 +814,7 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_
br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) { br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) {
SASSERT(f->get_num_parameters() == 1); SASSERT(f->get_num_parameters() == 1);
SASSERT(f->get_parameter(0).is_int()); SASSERT(f->get_parameter(0).is_int());
int bv_sz = f->get_parameter(0).get_int(); int bv_sz = f->get_parameter(0).get_int();
mpf_rounding_mode rmv; mpf_rounding_mode rmv;
scoped_mpf v(m_fm); scoped_mpf v(m_fm);
@ -829,8 +830,8 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
bv_util bu(m()); bv_util bu(m());
scoped_mpq q(m_fm.mpq_manager()); scoped_mpq q(m_fm.mpq_manager());
m_fm.to_sbv_mpq(rmv, v, q); m_fm.to_sbv_mpq(rmv, v, q);
rational r(q); rational r(q);
rational ul, ll; rational ul, ll;
ul = m_fm.m_powers2.m1(bv_sz - 1); ul = m_fm.m_powers2.m1(bv_sz - 1);
ll = - m_fm.m_powers2(bv_sz - 1); ll = - m_fm.m_powers2(bv_sz - 1);
@ -853,7 +854,7 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu
mk_to_ieee_bv_unspecified(f, result); mk_to_ieee_bv_unspecified(f, result);
return BR_REWRITE_FULL; return BR_REWRITE_FULL;
} }
bv_util bu(m()); bv_util bu(m());
scoped_mpz rz(m_fm.mpq_manager()); scoped_mpz rz(m_fm.mpq_manager());
m_fm.to_ieee_bv_mpz(v, rz); m_fm.to_ieee_bv_mpz(v, rz);
@ -866,7 +867,7 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu
br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) { br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) {
scoped_mpf v(m_fm); scoped_mpf v(m_fm);
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)) {
result = m_util.mk_internal_to_real_unspecified(); result = m_util.mk_internal_to_real_unspecified();

6
src/ast/rewriter/fpa_rewriter.h
View file

@ -39,13 +39,13 @@ public:
ast_manager & m() const { return m_util.m(); } ast_manager & m() const { return m_util.m(); }
family_id get_fid() const { return m_util.get_fid(); } family_id get_fid() const { return m_util.get_fid(); }
void updt_params(params_ref const & p); void updt_params(params_ref const & p);
static void get_param_descrs(param_descrs & r); static void get_param_descrs(param_descrs & r);
br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_eq_core(expr * arg1, expr * arg2, expr_ref & result); br_status mk_eq_core(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); br_status mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
br_status mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); br_status mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
br_status mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); br_status mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
@ -77,7 +77,7 @@ public:
br_status mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); br_status mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); br_status mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
br_status mk_rm(expr * arg, expr_ref & result); br_status mk_rm(expr * arg, expr_ref & result);
br_status mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); br_status mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result); br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result);

148
src/smt/theory_fpa.cpp
View file

@ -29,7 +29,7 @@ namespace smt {
obj_map<expr, expr*> & m_conversions; obj_map<expr, expr*> & m_conversions;
expr * m_e; expr * m_e;
public: public:
fpa2bv_conversion_trail_elem(ast_manager & m, obj_map<expr, expr*> & c, expr * e) : fpa2bv_conversion_trail_elem(ast_manager & m, obj_map<expr, expr*> & c, expr * e) :
m(m), m_conversions(c), m_e(e) {} m(m), m_conversions(c), m_e(e) {}
virtual ~fpa2bv_conversion_trail_elem() {} virtual ~fpa2bv_conversion_trail_elem() {}
virtual void undo(theory_fpa & th) { virtual void undo(theory_fpa & th) {
@ -63,7 +63,7 @@ namespace smt {
m.inc_ref(f); m.inc_ref(f);
m.inc_ref(result); m.inc_ref(result);
} }
} }
void theory_fpa::fpa2bv_converter_wrapped::mk_rm_const(func_decl * f, expr_ref & result) { void theory_fpa::fpa2bv_converter_wrapped::mk_rm_const(func_decl * f, expr_ref & result) {
SASSERT(f->get_family_id() == null_family_id); SASSERT(f->get_family_id() == null_family_id);
@ -89,12 +89,12 @@ namespace smt {
} }
expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_min_unspecified(func_decl * f, expr * x, expr * y) { expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_min_unspecified(func_decl * f, expr * x, expr * y) {
// The only cases in which min is unspecified for is when the arguments are +0.0 and -0.0. // The only cases in which min is unspecified for is when the arguments are +0.0 and -0.0.
unsigned ebits = m_util.get_ebits(f->get_range()); unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range());
unsigned bv_sz = ebits + sbits; unsigned bv_sz = ebits + sbits;
expr_ref res(m); expr_ref res(m);
expr * args[] = { x, y }; expr * args[] = { x, y };
func_decl * w = m.mk_func_decl(m_th.get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, 0, 0, 2, args, f->get_range()); func_decl * w = m.mk_func_decl(m_th.get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, 0, 0, 2, args, f->get_range());
expr_ref a(m), wrapped(m); expr_ref a(m), wrapped(m);
@ -110,7 +110,7 @@ namespace smt {
m_extra_assertions.push_back(sc); m_extra_assertions.push_back(sc);
return res; return res;
} }
expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_max_unspecified(func_decl * f, expr * x, expr * y) { expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_max_unspecified(func_decl * f, expr * x, expr * y) {
// The only cases in which max is unspecified for is when the arguments are +0.0 and -0.0. // The only cases in which max is unspecified for is when the arguments are +0.0 and -0.0.
unsigned ebits = m_util.get_ebits(f->get_range()); unsigned ebits = m_util.get_ebits(f->get_range());
@ -118,7 +118,7 @@ namespace smt {
unsigned bv_sz = ebits + sbits; unsigned bv_sz = ebits + sbits;
expr_ref res(m); expr_ref res(m);
expr * args[] = { x, y }; expr * args[] = { x, y };
func_decl * w = m.mk_func_decl(m_th.get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, 0, 0, 2, args, f->get_range()); func_decl * w = m.mk_func_decl(m_th.get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, 0, 0, 2, args, f->get_range());
expr_ref a(m), wrapped(m); expr_ref a(m), wrapped(m);
a = m.mk_app(w, x, y); a = m.mk_app(w, x, y);
@ -154,15 +154,15 @@ namespace smt {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
dec_ref_map_values(m, m_conversions); dec_ref_map_values(m, m_conversions);
dec_ref_map_values(m, m_wraps); dec_ref_map_values(m, m_wraps);
dec_ref_map_values(m, m_unwraps); dec_ref_map_values(m, m_unwraps);
} }
app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) { app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
ast_manager & m = m_th.get_manager(); ast_manager & m = m_th.get_manager();
TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++) TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++)
tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;); tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
mpf_manager & mpfm = m_fu.fm(); mpf_manager & mpfm = m_fu.fm();
unsynch_mpz_manager & mpzm = mpfm.mpz_manager(); unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
app * result; app * result;
@ -195,7 +195,7 @@ namespace smt {
mpzm.set(sig_z, all_z); mpzm.set(sig_z, all_z);
} }
else if (values.size() == 3) { else if (values.size() == 3) {
rational sgn_r(0), exp_r(0), sig_r(0); rational sgn_r(0), exp_r(0), sig_r(0);
bool r = m_bu.is_numeral(values[0], sgn_r, bv_sz); bool r = m_bu.is_numeral(values[0], sgn_r, bv_sz);
@ -204,7 +204,7 @@ namespace smt {
SASSERT(r && bv_sz == m_ebits); SASSERT(r && bv_sz == m_ebits);
r = m_bu.is_numeral(values[2], sig_r, bv_sz); r = m_bu.is_numeral(values[2], sig_r, bv_sz);
SASSERT(r && bv_sz == m_sbits - 1); SASSERT(r && bv_sz == m_sbits - 1);
SASSERT(mpzm.is_one(sgn_r.to_mpq().denominator())); SASSERT(mpzm.is_one(sgn_r.to_mpq().denominator()));
SASSERT(mpzm.is_one(exp_r.to_mpq().denominator())); SASSERT(mpzm.is_one(exp_r.to_mpq().denominator()));
SASSERT(mpzm.is_one(sig_r.to_mpq().denominator())); SASSERT(mpzm.is_one(sig_r.to_mpq().denominator()));
@ -228,25 +228,25 @@ namespace smt {
mpzm.to_string(exp_z) << "," << mpzm.to_string(exp_z) << "," <<
mpzm.to_string(sig_z) << "] --> " << mpzm.to_string(sig_z) << "] --> " <<
mk_ismt2_pp(result, m_th.get_manager()) << "\n";); mk_ismt2_pp(result, m_th.get_manager()) << "\n";);
return result; return result;
} }
app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) { app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
SASSERT(values.size() == 1); SASSERT(values.size() == 1);
ast_manager & m = m_th.get_manager(); ast_manager & m = m_th.get_manager();
TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++) TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++)
tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;); tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
app * result = 0; app * result = 0;
unsigned bv_sz; unsigned bv_sz;
rational val(0); rational val(0);
bool r = m_bu.is_numeral(values[0], val, bv_sz); bool r = m_bu.is_numeral(values[0], val, bv_sz);
SASSERT(r); SASSERT(r);
SASSERT(bv_sz == 3); SASSERT(bv_sz == 3);
switch (val.get_uint64()) switch (val.get_uint64())
{ {
case BV_RM_TIES_TO_AWAY: result = m_fu.mk_round_nearest_ties_to_away(); break; case BV_RM_TIES_TO_AWAY: result = m_fu.mk_round_nearest_ties_to_away(); break;
@ -257,7 +257,7 @@ namespace smt {
default: result = m_fu.mk_round_toward_zero(); default: result = m_fu.mk_round_toward_zero();
} }
TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value result: " << TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value result: " <<
mk_ismt2_pp(result, m_th.get_manager()) << "\n";); mk_ismt2_pp(result, m_th.get_manager()) << "\n";);
return result; return result;
@ -272,7 +272,7 @@ namespace smt {
if (!m_wraps.find(e_srt, w)) { if (!m_wraps.find(e_srt, w)) {
SASSERT(!m_wraps.contains(e_srt)); SASSERT(!m_wraps.contains(e_srt));
sort * bv_srt; sort * bv_srt;
if (m_converter.is_rm(e_srt)) if (m_converter.is_rm(e_srt))
bv_srt = m_bv_util.mk_sort(3); bv_srt = m_bv_util.mk_sort(3);
@ -280,9 +280,9 @@ namespace smt {
SASSERT(m_converter.is_float(e_srt)); SASSERT(m_converter.is_float(e_srt));
unsigned ebits = m_fpa_util.get_ebits(e_srt); unsigned ebits = m_fpa_util.get_ebits(e_srt);
unsigned sbits = m_fpa_util.get_sbits(e_srt); unsigned sbits = m_fpa_util.get_sbits(e_srt);
bv_srt = m_bv_util.mk_sort(ebits + sbits); bv_srt = m_bv_util.mk_sort(ebits + sbits);
} }
w = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVWRAP, 0, 0, 1, &e_srt, bv_srt); w = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVWRAP, 0, 0, 1, &e_srt, bv_srt);
m_wraps.insert(e_srt, w); m_wraps.insert(e_srt, w);
m.inc_ref(w); m.inc_ref(w);
@ -295,7 +295,7 @@ namespace smt {
app_ref theory_fpa::unwrap(expr * e, sort * s) { app_ref theory_fpa::unwrap(expr * e, sort * s) {
SASSERT(!m_fpa_util.is_unwrap(e)); SASSERT(!m_fpa_util.is_unwrap(e));
ast_manager & m = get_manager(); ast_manager & m = get_manager();
sort * bv_srt = m.get_sort(e); sort * bv_srt = m.get_sort(e);
func_decl *u; func_decl *u;
@ -311,7 +311,7 @@ namespace smt {
res = m.mk_app(u, e); res = m.mk_app(u, e);
return res; return res;
} }
expr_ref theory_fpa::convert_atom(expr * e) { expr_ref theory_fpa::convert_atom(expr * e) {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
TRACE("t_fpa_detail", tout << "converting atom: " << mk_ismt2_pp(e, get_manager()) << "\n";); TRACE("t_fpa_detail", tout << "converting atom: " << mk_ismt2_pp(e, get_manager()) << "\n";);
@ -320,7 +320,7 @@ namespace smt {
m_rw(e, res); m_rw(e, res);
m_th_rw(res, res); m_th_rw(res, res);
SASSERT(is_app(res)); SASSERT(is_app(res));
SASSERT(m.is_bool(res)); SASSERT(m.is_bool(res));
return res; return res;
} }
@ -331,12 +331,12 @@ namespace smt {
expr_ref e_conv(m), res(m); expr_ref e_conv(m), res(m);
proof_ref pr(m); proof_ref pr(m);
m_rw(e, e_conv); m_rw(e, e_conv);
if (is_app(e_conv) && to_app(e_conv)->get_family_id() != get_family_id()) { if (is_app(e_conv) && to_app(e_conv)->get_family_id() != get_family_id()) {
if (!m_fpa_util.is_float(e_conv)) if (!m_fpa_util.is_float(e_conv))
m_th_rw(e_conv, res); m_th_rw(e_conv, res);
else { else {
expr_ref bv(m); expr_ref bv(m);
bv = wrap(e_conv); bv = wrap(e_conv);
unsigned bv_sz = m_bv_util.get_bv_size(bv); unsigned bv_sz = m_bv_util.get_bv_size(bv);
unsigned ebits = m_fpa_util.get_ebits(m.get_sort(e_conv)); unsigned ebits = m_fpa_util.get_ebits(m.get_sort(e_conv));
@ -365,7 +365,7 @@ namespace smt {
m_converter.mk_fp(sgn, exp, sig, res); m_converter.mk_fp(sgn, exp, sig, res);
} }
else else
UNREACHABLE(); UNREACHABLE();
SASSERT(res.get() != 0); SASSERT(res.get() != 0);
return res; return res;
@ -426,7 +426,7 @@ namespace smt {
expr_ref theory_fpa::convert_conversion_term(expr * e) { expr_ref theory_fpa::convert_conversion_term(expr * e) {
/* This is for the conversion functions fp.to_* */ /* This is for the conversion functions fp.to_* */
ast_manager & m = get_manager(); ast_manager & m = get_manager();
expr_ref res(m); expr_ref res(m);
proof_ref pr(m); proof_ref pr(m);
@ -480,7 +480,7 @@ namespace smt {
else if (m_fpa_util.is_float(e) || m_fpa_util.is_rm(e)) else if (m_fpa_util.is_float(e) || m_fpa_util.is_rm(e))
res = convert_term(e); res = convert_term(e);
else if (m_arith_util.is_real(e) || m_bv_util.is_bv(e)) else if (m_arith_util.is_real(e) || m_bv_util.is_bv(e))
res = convert_conversion_term(e); res = convert_conversion_term(e);
else else
UNREACHABLE(); UNREACHABLE();
@ -492,7 +492,7 @@ namespace smt {
m.inc_ref(res); m.inc_ref(res);
m_trail_stack.push(fpa2bv_conversion_trail_elem(m, m_conversions, e)); m_trail_stack.push(fpa2bv_conversion_trail_elem(m, m_conversions, e));
} }
return res; return res;
} }
@ -501,7 +501,7 @@ namespace smt {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
context & ctx = get_context(); context & ctx = get_context();
simplifier & simp = ctx.get_simplifier(); simplifier & simp = ctx.get_simplifier();
expr_ref res(m), t(m); expr_ref res(m), t(m);
proof_ref t_pr(m); proof_ref t_pr(m);
res = m.mk_true(); res = m.mk_true();
@ -515,21 +515,21 @@ namespace smt {
m_converter.m_extra_assertions.reset(); m_converter.m_extra_assertions.reset();
m_th_rw(res); m_th_rw(res);
CTRACE("t_fpa", !m.is_true(res), tout << "side condition: " << mk_ismt2_pp(res, m) << "\n";); CTRACE("t_fpa", !m.is_true(res), tout << "side condition: " << mk_ismt2_pp(res, m) << "\n";);
return res; return res;
} }
void theory_fpa::assert_cnstr(expr * e) { void theory_fpa::assert_cnstr(expr * e) {
if (get_manager().is_true(e)) return; if (get_manager().is_true(e)) return;
TRACE("t_fpa_detail", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << "\n";); TRACE("t_fpa_detail", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << "\n";);
context & ctx = get_context(); context & ctx = get_context();
ctx.internalize(e, false); ctx.internalize(e, false);
literal lit(ctx.get_literal(e)); literal lit(ctx.get_literal(e));
ctx.mark_as_relevant(lit); ctx.mark_as_relevant(lit);
ctx.mk_th_axiom(get_id(), 1, &lit); ctx.mk_th_axiom(get_id(), 1, &lit);
TRACE("t_fpa_detail", tout << "done asserting " << mk_ismt2_pp(e, get_manager()) << "\n";); TRACE("t_fpa_detail", tout << "done asserting " << mk_ismt2_pp(e, get_manager()) << "\n";);
} }
void theory_fpa::attach_new_th_var(enode * n) { void theory_fpa::attach_new_th_var(enode * n) {
context & ctx = get_context(); context & ctx = get_context();
@ -556,10 +556,10 @@ namespace smt {
ctx.set_var_theory(l.var(), get_id()); ctx.set_var_theory(l.var(), get_id());
expr_ref bv_atom(m); expr_ref bv_atom(m);
bv_atom = convert_atom(atom); bv_atom = convert_atom(atom);
SASSERT(is_app(bv_atom) && m.is_bool(bv_atom)); SASSERT(is_app(bv_atom) && m.is_bool(bv_atom));
bv_atom = m.mk_and(bv_atom, mk_side_conditions()); bv_atom = m.mk_and(bv_atom, mk_side_conditions());
assert_cnstr(m.mk_iff(atom, bv_atom)); assert_cnstr(m.mk_iff(atom, bv_atom));
return true; return true;
} }
@ -569,29 +569,29 @@ namespace smt {
context & ctx = get_context(); context & ctx = get_context();
TRACE("t_fpa", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";); TRACE("t_fpa", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";);
SASSERT(term->get_family_id() == get_family_id()); SASSERT(term->get_family_id() == get_family_id());
SASSERT(!ctx.e_internalized(term)); SASSERT(!ctx.e_internalized(term));
unsigned num_args = term->get_num_args(); unsigned num_args = term->get_num_args();
for (unsigned i = 0; i < num_args; i++) for (unsigned i = 0; i < num_args; i++)
ctx.internalize(term->get_arg(i), false); ctx.internalize(term->get_arg(i), false);
enode * e = (ctx.e_internalized(term)) ? ctx.get_enode(term) : enode * e = (ctx.e_internalized(term)) ? ctx.get_enode(term) :
ctx.mk_enode(term, false, false, true); ctx.mk_enode(term, false, false, true);
if (is_attached_to_var(e)) if (is_attached_to_var(e))
return false; return false;
attach_new_th_var(e); attach_new_th_var(e);
// The conversion operators fp.to_* appear in non-FP constraints. // The conversion operators fp.to_* appear in non-FP constraints.
// The corresponding constraints will not be translated and added // The corresponding constraints will not be translated and added
// via convert(...) and assert_cnstr(...) in initialize_atom(...). // via convert(...) and assert_cnstr(...) in initialize_atom(...).
// Therefore, we translate and assert them here. // Therefore, we translate and assert them here.
fpa_op_kind k = (fpa_op_kind)term->get_decl_kind(); fpa_op_kind k = (fpa_op_kind)term->get_decl_kind();
switch (k) { switch (k) {
case OP_FPA_TO_UBV: case OP_FPA_TO_UBV:
case OP_FPA_TO_SBV: case OP_FPA_TO_SBV:
case OP_FPA_TO_REAL: case OP_FPA_TO_REAL:
case OP_FPA_TO_IEEE_BV: { case OP_FPA_TO_IEEE_BV: {
expr_ref conv(m); expr_ref conv(m);
conv = convert(term); conv = convert(term);
@ -599,32 +599,32 @@ namespace smt {
assert_cnstr(mk_side_conditions()); assert_cnstr(mk_side_conditions());
break; break;
} }
default: /* ignore */; default: /* ignore */;
} }
return true; return true;
} }
void theory_fpa::apply_sort_cnstr(enode * n, sort * s) { void theory_fpa::apply_sort_cnstr(enode * n, sort * s) {
TRACE("t_fpa", tout << "apply sort cnstr for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << "\n";); TRACE("t_fpa", tout << "apply sort cnstr for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << "\n";);
SASSERT(s->get_family_id() == get_family_id()); SASSERT(s->get_family_id() == get_family_id());
ast_manager & m = get_manager(); ast_manager & m = get_manager();
context & ctx = get_context(); context & ctx = get_context();
app_ref owner(m); app_ref owner(m);
owner = n->get_owner(); owner = n->get_owner();
SASSERT(owner->get_decl()->get_range() == s); SASSERT(owner->get_decl()->get_range() == s);
if ((m_fpa_util.is_float(s) || m_fpa_util.is_rm(s)) && if ((m_fpa_util.is_float(s) || m_fpa_util.is_rm(s)) &&
!is_attached_to_var(n)) { !is_attached_to_var(n)) {
attach_new_th_var(n); attach_new_th_var(n);
if (m_fpa_util.is_rm(s)) { if (m_fpa_util.is_rm(s)) {
// For every RM term, we need to make sure that it's // For every RM term, we need to make sure that it's
// associated bit-vector is within the valid range. // associated bit-vector is within the valid range.
if (!m_fpa_util.is_unwrap(owner)) { if (!m_fpa_util.is_unwrap(owner)) {
expr_ref valid(m), limit(m); expr_ref valid(m), limit(m);
limit = m_bv_util.mk_numeral(4, 3); limit = m_bv_util.mk_numeral(4, 3);
@ -638,7 +638,7 @@ namespace smt {
} }
} }
void theory_fpa::new_eq_eh(theory_var x, theory_var y) { void theory_fpa::new_eq_eh(theory_var x, theory_var y) {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
enode * e_x = get_enode(x); enode * e_x = get_enode(x);
enode * e_y = get_enode(y); enode * e_y = get_enode(y);
@ -646,7 +646,7 @@ namespace smt {
TRACE("t_fpa", tout << "new eq: " << x << " = " << y << std::endl;); TRACE("t_fpa", tout << "new eq: " << x << " = " << y << std::endl;);
TRACE("t_fpa_detail", tout << mk_ismt2_pp(e_x->get_owner(), m) << " = " << TRACE("t_fpa_detail", tout << mk_ismt2_pp(e_x->get_owner(), m) << " = " <<
mk_ismt2_pp(e_y->get_owner(), m) << std::endl;); mk_ismt2_pp(e_y->get_owner(), m) << std::endl;);
fpa_util & fu = m_fpa_util; fpa_util & fu = m_fpa_util;
expr_ref xe(m), ye(m); expr_ref xe(m), ye(m);
@ -664,13 +664,13 @@ namespace smt {
"yc = " << mk_ismt2_pp(yc, m) << std::endl;); "yc = " << mk_ismt2_pp(yc, m) << std::endl;);
expr_ref c(m); expr_ref c(m);
if ((fu.is_float(xe) && fu.is_float(ye)) || if ((fu.is_float(xe) && fu.is_float(ye)) ||
(fu.is_rm(xe) && fu.is_rm(ye))) (fu.is_rm(xe) && fu.is_rm(ye)))
m_converter.mk_eq(xc, yc, c); m_converter.mk_eq(xc, yc, c);
else else
c = m.mk_eq(xc, yc); c = m.mk_eq(xc, yc);
m_th_rw(c); m_th_rw(c);
assert_cnstr(m.mk_iff(m.mk_eq(xe, ye), c)); assert_cnstr(m.mk_iff(m.mk_eq(xe, ye), c));
assert_cnstr(mk_side_conditions()); assert_cnstr(mk_side_conditions());
@ -722,33 +722,33 @@ namespace smt {
m_trail_stack.push_scope(); m_trail_stack.push_scope();
} }
void theory_fpa::pop_scope_eh(unsigned num_scopes) { void theory_fpa::pop_scope_eh(unsigned num_scopes) {
m_trail_stack.pop_scope(num_scopes); m_trail_stack.pop_scope(num_scopes);
TRACE("t_fpa", tout << "pop " << num_scopes << "; now " << m_trail_stack.get_num_scopes() << "\n";); TRACE("t_fpa", tout << "pop " << num_scopes << "; now " << m_trail_stack.get_num_scopes() << "\n";);
// unsigned num_old_vars = get_old_num_vars(num_scopes); // unsigned num_old_vars = get_old_num_vars(num_scopes);
theory::pop_scope_eh(num_scopes); theory::pop_scope_eh(num_scopes);
} }
void theory_fpa::assign_eh(bool_var v, bool is_true) { void theory_fpa::assign_eh(bool_var v, bool is_true) {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
context & ctx = get_context(); context & ctx = get_context();
expr * e = ctx.bool_var2expr(v); expr * e = ctx.bool_var2expr(v);
TRACE("t_fpa", tout << "assign_eh for: " << v << " (" << is_true << "):\n" << mk_ismt2_pp(e, m) << "\n";); TRACE("t_fpa", tout << "assign_eh for: " << v << " (" << is_true << "):\n" << mk_ismt2_pp(e, m) << "\n";);
expr_ref converted(m); expr_ref converted(m);
converted = m.mk_and(convert(e), mk_side_conditions()); converted = m.mk_and(convert(e), mk_side_conditions());
if (is_true) if (is_true)
assert_cnstr(m.mk_implies(e, converted)); assert_cnstr(m.mk_implies(e, converted));
else else
assert_cnstr(m.mk_implies(m.mk_not(e), m.mk_not(converted))); assert_cnstr(m.mk_implies(m.mk_not(e), m.mk_not(converted)));
} }
void theory_fpa::relevant_eh(app * n) { void theory_fpa::relevant_eh(app * n) {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
TRACE("t_fpa", tout << "relevant_eh for: " << mk_ismt2_pp(n, m) << "\n";); TRACE("t_fpa", tout << "relevant_eh for: " << mk_ismt2_pp(n, m) << "\n";);
mpf_manager & mpfm = m_fpa_util.fm(); mpf_manager & mpfm = m_fpa_util.fm();
if (m_fpa_util.is_float(n) || m_fpa_util.is_rm(n)) { if (m_fpa_util.is_float(n) || m_fpa_util.is_rm(n)) {
if (!m_fpa_util.is_unwrap(n)) { if (!m_fpa_util.is_unwrap(n)) {
@ -757,7 +757,7 @@ namespace smt {
mpf_rounding_mode rm; mpf_rounding_mode rm;
scoped_mpf val(mpfm); scoped_mpf val(mpfm);
if (m_fpa_util.is_rm_numeral(n, rm)) { if (m_fpa_util.is_rm_numeral(n, rm)) {
c = m.mk_eq(wrapped, m_bv_util.mk_numeral(rm, 3)); c = m.mk_eq(wrapped, m_bv_util.mk_numeral(rm, 3));
assert_cnstr(c); assert_cnstr(c);
} }
else if (m_fpa_util.is_numeral(n, val)) { else if (m_fpa_util.is_numeral(n, val)) {
@ -772,7 +772,7 @@ namespace smt {
assert_cnstr(c); assert_cnstr(c);
} }
else { else {
c = m.mk_eq(unwrap(wrapped, m.get_sort(n)), n); c = m.mk_eq(unwrap(wrapped, m.get_sort(n)), n);
assert_cnstr(c); assert_cnstr(c);
} }
} }
@ -803,7 +803,7 @@ namespace smt {
final_check_status theory_fpa::final_check_eh() { final_check_status theory_fpa::final_check_eh() {
TRACE("t_fpa", tout << "final_check_eh\n";); TRACE("t_fpa", tout << "final_check_eh\n";);
SASSERT(m_converter.m_extra_assertions.empty()); SASSERT(m_converter.m_extra_assertions.empty());
return FC_DONE; return FC_DONE;
} }
void theory_fpa::init_model(model_generator & mg) { void theory_fpa::init_model(model_generator & mg) {
@ -813,7 +813,7 @@ namespace smt {
} }
model_value_proc * theory_fpa::mk_value(enode * n, model_generator & mg) { model_value_proc * theory_fpa::mk_value(enode * n, model_generator & mg) {
TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), get_manager()) <<
" (sort " << mk_ismt2_pp(get_manager().get_sort(n->get_owner()), get_manager()) << ")\n";); " (sort " << mk_ismt2_pp(get_manager().get_sort(n->get_owner()), get_manager()) << ")\n";);
ast_manager & m = get_manager(); ast_manager & m = get_manager();
@ -821,14 +821,14 @@ namespace smt {
app_ref owner(m); app_ref owner(m);
owner = n->get_owner(); owner = n->get_owner();
// If the owner is not internalized, it doesn't have an enode associated. // If the owner is not internalized, it doesn't have an enode associated.
SASSERT(ctx.e_internalized(owner)); SASSERT(ctx.e_internalized(owner));
if (m_fpa_util.is_rm_numeral(owner) || if (m_fpa_util.is_rm_numeral(owner) ||
m_fpa_util.is_numeral(owner)) { m_fpa_util.is_numeral(owner)) {
return alloc(expr_wrapper_proc, owner); return alloc(expr_wrapper_proc, owner);
} }
model_value_proc * res = 0; model_value_proc * res = 0;
app_ref wrapped(m); app_ref wrapped(m);
@ -849,7 +849,7 @@ namespace smt {
a2 = to_app(owner->get_arg(2)); a2 = to_app(owner->get_arg(2));
unsigned ebits = m_fpa_util.get_ebits(m.get_sort(owner)); unsigned ebits = m_fpa_util.get_ebits(m.get_sort(owner));
unsigned sbits = m_fpa_util.get_sbits(m.get_sort(owner)); unsigned sbits = m_fpa_util.get_sbits(m.get_sort(owner));
fpa_value_proc * vp = alloc(fpa_value_proc, this, ebits, sbits); fpa_value_proc * vp = alloc(fpa_value_proc, this, ebits, sbits);
vp->add_dependency(ctx.get_enode(a0)); vp->add_dependency(ctx.get_enode(a0));
vp->add_dependency(ctx.get_enode(a1)); vp->add_dependency(ctx.get_enode(a1));
vp->add_dependency(ctx.get_enode(a2)); vp->add_dependency(ctx.get_enode(a2));
@ -891,8 +891,8 @@ namespace smt {
{ {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
context & ctx = get_context(); context & ctx = get_context();
out << "fpa theory variables:" << std::endl; out << "fpa theory variables:" << std::endl;
ptr_vector<enode>::const_iterator it = ctx.begin_enodes(); ptr_vector<enode>::const_iterator it = ctx.begin_enodes();
ptr_vector<enode>::const_iterator end = ctx.end_enodes(); ptr_vector<enode>::const_iterator end = ctx.end_enodes();
for (; it != end; it++) { for (; it != end; it++) {
@ -907,7 +907,7 @@ namespace smt {
for (; it != end; it++) { for (; it != end; it++) {
theory_var v = (*it)->get_th_var(m_bv_util.get_family_id()); theory_var v = (*it)->get_th_var(m_bv_util.get_family_id());
if (v != -1) out << v << " -> " << if (v != -1) out << v << " -> " <<
mk_ismt2_pp((*it)->get_owner(), m) << std::endl; mk_ismt2_pp((*it)->get_owner(), m) << std::endl;
} }
out << "arith theory variables:" << std::endl; out << "arith theory variables:" << std::endl;

22
src/smt/theory_fpa.h
View file

@ -84,13 +84,13 @@ namespace smt {
virtual void mk_const(func_decl * f, expr_ref & result); virtual void mk_const(func_decl * f, expr_ref & result);
virtual void mk_rm_const(func_decl * f, expr_ref & result); virtual void mk_rm_const(func_decl * f, expr_ref & result);
virtual void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result); virtual void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
virtual expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y); virtual expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y);
virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y); virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y);
}; };
class fpa_value_proc : public model_value_proc { class fpa_value_proc : public model_value_proc {
protected: protected:
theory_fpa & m_th; theory_fpa & m_th;
ast_manager & m; ast_manager & m;
fpa_util & m_fu; fpa_util & m_fu;
@ -100,10 +100,10 @@ namespace smt {
unsigned m_sbits; unsigned m_sbits;
public: public:
fpa_value_proc(theory_fpa * th, unsigned ebits, unsigned sbits) : fpa_value_proc(theory_fpa * th, unsigned ebits, unsigned sbits) :
m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util), m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util),
m_ebits(ebits), m_sbits(sbits) {} m_ebits(ebits), m_sbits(sbits) {}
virtual ~fpa_value_proc() {} virtual ~fpa_value_proc() {}
void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); } void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
@ -123,7 +123,7 @@ namespace smt {
buffer<model_value_dependency> m_deps; buffer<model_value_dependency> m_deps;
public: public:
fpa_rm_value_proc(theory_fpa * th) : fpa_rm_value_proc(theory_fpa * th) :
m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util) {} m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util) {}
void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); } void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
@ -135,7 +135,7 @@ namespace smt {
virtual ~fpa_rm_value_proc() {} virtual ~fpa_rm_value_proc() {}
virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values); virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values);
}; };
protected: protected:
fpa2bv_converter_wrapped m_converter; fpa2bv_converter_wrapped m_converter;
fpa2bv_rewriter m_rw; fpa2bv_rewriter m_rw;
@ -159,10 +159,10 @@ namespace smt {
virtual void pop_scope_eh(unsigned num_scopes); virtual void pop_scope_eh(unsigned num_scopes);
virtual void reset_eh(); virtual void reset_eh();
virtual theory* mk_fresh(context*) { return alloc(theory_fpa, get_manager()); } virtual theory* mk_fresh(context*) { return alloc(theory_fpa, get_manager()); }
virtual char const * get_name() const { return "fpa"; } virtual char const * get_name() const { return "fpa"; }
virtual model_value_proc * mk_value(enode * n, model_generator & mg); virtual model_value_proc * mk_value(enode * n, model_generator & mg);
void assign_eh(bool_var v, bool is_true); void assign_eh(bool_var v, bool is_true);
virtual void relevant_eh(app * n); virtual void relevant_eh(app * n);
virtual void init_model(model_generator & m); virtual void init_model(model_generator & m);
@ -181,14 +181,14 @@ namespace smt {
expr_ref convert_term(expr * e); expr_ref convert_term(expr * e);
expr_ref convert_conversion_term(expr * e); expr_ref convert_conversion_term(expr * e);
expr_ref convert_unwrap(expr * e); expr_ref convert_unwrap(expr * e);
void add_trail(ast * a); void add_trail(ast * a);
void attach_new_th_var(enode * n); void attach_new_th_var(enode * n);
void assert_cnstr(expr * e); void assert_cnstr(expr * e);
app_ref wrap(expr * e); app_ref wrap(expr * e);
app_ref unwrap(expr * e, sort * s); app_ref unwrap(expr * e, sort * s);
}; };
}; };