mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

fp2bv refactoring

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-05-23 18:10:17 +01:00
parent 8370bb8986
commit 617e941015
10 changed files with 45 additions and 64 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_ast.cpp
View file

@ -1185,7 +1185,7 @@ extern "C" {
case OP_FPA_TO_IEEE_BV: return Z3_OP_FPA_TO_IEEE_BV;
case OP_FPA_INTERNAL_MIN_I: return Z3_OP_FPA_MIN_I;
case OP_FPA_INTERNAL_MAX_I: return Z3_OP_FPA_MAX_I;
case OP_FPA_INTERNAL_RM_BVWRAP:
case OP_FPA_INTERNAL_BV2RM:
case OP_FPA_INTERNAL_BVWRAP:
case OP_FPA_INTERNAL_MIN_UNSPECIFIED:
case OP_FPA_INTERNAL_MAX_UNSPECIFIED:

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

@ -79,7 +79,7 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
m_simp.mk_or(both_are_nan, both_the_same, result);
}
else if (is_rm(a) && is_rm(b)) {
SASSERT(m_util.is_rm_bvwrap(b) && m_util.is_rm_bvwrap(a));
SASSERT(m_util.is_bv2rm(b) && m_util.is_bv2rm(a));
TRACE("fpa2bv", tout << "mk_eq_rm a=" << mk_ismt2_pp(a, m) << std::endl;
tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;);
@ -236,7 +236,7 @@ void fpa2bv_converter::mk_function_output(sort * rng, func_decl * fbv, expr * co
else if (m_util.is_rm(rng)) {
app_ref na(m);
na = m.mk_app(fbv, fbv->get_arity(), new_args);
result = m_util.mk_rm(na);
result = m_util.mk_bv2rm(na);
}
else
result = m.mk_app(fbv, fbv->get_arity(), new_args);
@ -284,7 +284,7 @@ void fpa2bv_converter::mk_function(func_decl * f, unsigned num, expr * const * a
bv_rng = m_bv_util.mk_sort(3);
func_decl * bv_f = get_bv_uf(f, bv_rng, num);
bv_app = m.mk_app(bv_f, num, args);
flt_app = m_util.mk_rm(bv_app);
flt_app = m_util.mk_bv2rm(bv_app);
new_eq = m.mk_eq(fapp, flt_app);
m_extra_assertions.push_back(new_eq);
result = flt_app;
@ -315,7 +315,7 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
#endif
, m_bv_util.mk_sort(3));
result = m_util.mk_rm(bv3);
result = m_util.mk_bv2rm(bv3);
m_rm_const2bv.insert(f, result);
m.inc_ref(f);
m.inc_ref(result);
@ -522,7 +522,7 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits,
void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 3);
SASSERT(m_util.is_rm_bvwrap(args[0]));
SASSERT(m_util.is_bv2rm(args[0]));
expr_ref rm(m), x(m), y(m);
rm = to_app(args[0])->get_arg(0);
@ -692,7 +692,7 @@ void fpa2bv_converter::mk_neg(sort * srt, expr_ref & x, expr_ref & result) {
void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 3);
SASSERT(m_util.is_rm_bvwrap(args[0]));
SASSERT(m_util.is_bv2rm(args[0]));
expr_ref rm(m), x(m), y(m);
rm = to_app(args[0])->get_arg(0);
@ -842,7 +842,7 @@ void fpa2bv_converter::mk_mul(sort * s, expr_ref & rm, expr_ref & x, expr_ref &
void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 3);
SASSERT(m_util.is_rm_bvwrap(args[0]));
SASSERT(m_util.is_bv2rm(args[0]));
expr_ref rm(m), x(m), y(m);
rm = to_app(args[0])->get_arg(0);
x = args[1];
@ -1239,7 +1239,7 @@ void fpa2bv_converter::mk_max_i(func_decl * f, unsigned num, expr * const * args
void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 4);
SASSERT(m_util.is_rm_bvwrap(args[0]));
SASSERT(m_util.is_bv2rm(args[0]));
// fusedma means (x * y) + z
expr_ref rm(m), x(m), y(m), z(m);
@ -1557,7 +1557,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);
SASSERT(m_util.is_rm_bvwrap(args[0]));
SASSERT(m_util.is_bv2rm(args[0]));
expr_ref rm(m), x(m);
rm = to_app(args[0])->get_arg(0);
@ -1706,7 +1706,7 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args,
void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);
SASSERT(m_util.is_rm_bvwrap(args[0]));
SASSERT(m_util.is_bv2rm(args[0]));
expr_ref rm(m), x(m);
rm = to_app(args[0])->get_arg(0);
@ -2166,7 +2166,7 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result) {
SASSERT(m_util.is_rm_bvwrap(rm));
SASSERT(m_util.is_bv2rm(rm));
mk_to_fp_float(s, to_app(rm)->get_arg(0), x, result);
}
@ -2337,7 +2337,7 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
"x: " << mk_ismt2_pp(x, m) << std::endl;);
SASSERT(m_util.is_float(s));
SASSERT(au().is_real(x) || au().is_int(x));
SASSERT(m_util.is_rm_bvwrap(rm));
SASSERT(m_util.is_bv2rm(rm));
expr * bv_rm = to_app(rm)->get_arg(0);
unsigned ebits = m_util.get_ebits(s);
@ -2472,7 +2472,7 @@ void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * con
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
SASSERT(m_util.is_rm_bvwrap(args[0]));
SASSERT(m_util.is_bv2rm(args[0]));
expr * bv_rm = to_app(args[0])->get_arg(0);
rational e;
@ -2630,7 +2630,7 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
SASSERT(num == 2);
SASSERT(m_util.is_float(f->get_range()));
SASSERT(m_util.is_rm_bvwrap(args[0]));
SASSERT(m_util.is_bv2rm(args[0]));
SASSERT(m_bv_util.is_bv(args[1]));
expr_ref rm(m), x(m);
@ -2772,7 +2772,7 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
SASSERT(num == 2);
SASSERT(m_util.is_float(f->get_range()));
SASSERT(m_util.is_rm_bvwrap(args[0]));
SASSERT(m_util.is_bv2rm(args[0]));
SASSERT(m_bv_util.is_bv(args[1]));
expr_ref rm(m), x(m);
@ -2924,7 +2924,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
SASSERT(num == 2);
SASSERT(m_util.is_rm_bvwrap(args[0]));
SASSERT(m_util.is_bv2rm(args[0]));
SASSERT(m_util.is_float(args[1]));
expr * rm = to_app(args[0])->get_arg(0);
@ -3528,7 +3528,7 @@ void fpa2bv_converter::mk_rounding_mode(decl_kind k, expr_ref & result)
default: UNREACHABLE();
}
result = m_util.mk_rm(result);
result = m_util.mk_bv2rm(result);
}
void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {

2
src/ast/fpa/fpa2bv_rewriter.cpp
View file

@ -156,7 +156,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
case OP_FPA_INTERNAL_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_BVWRAP:
case OP_FPA_INTERNAL_RM_BVWRAP:
case OP_FPA_INTERNAL_BV2RM:
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:

6
src/ast/fpa_decl_plugin.cpp
View file

@ -676,7 +676,7 @@ func_decl * fpa_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameters,
return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k));
}
func_decl * fpa_decl_plugin::mk_internal_rm(decl_kind k, unsigned num_parameters, parameter const * parameters,
func_decl * fpa_decl_plugin::mk_internal_bv2rm(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
if (arity != 1)
m_manager->raise_exception("invalid number of arguments to internal_rm");
@ -837,8 +837,8 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
case OP_FPA_INTERNAL_BVWRAP:
return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range);
case OP_FPA_INTERNAL_RM_BVWRAP:
return mk_internal_rm(k, num_parameters, parameters, arity, domain, range);
case OP_FPA_INTERNAL_BV2RM:
return mk_internal_bv2rm(k, num_parameters, parameters, arity, domain, range);
case OP_FPA_INTERNAL_MIN_I:
case OP_FPA_INTERNAL_MAX_I:

19
src/ast/fpa_decl_plugin.h
View file

@ -88,7 +88,7 @@ enum fpa_op_kind {
/* Internal use only */
OP_FPA_INTERNAL_BVWRAP,
OP_FPA_INTERNAL_RM_BVWRAP, // Internal conversion from (_ BitVec 3) to RoundingMode
OP_FPA_INTERNAL_BV2RM,
OP_FPA_INTERNAL_MIN_I,
OP_FPA_INTERNAL_MAX_I,
@ -164,8 +164,8 @@ class fpa_decl_plugin : public decl_plugin {
func_decl * mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_rm(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_bv2rm(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_bv_unwrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
@ -301,11 +301,6 @@ public:
return m().mk_app(m_fid, OP_FPA_FP, sgn, exp, sig);
}
app * mk_rm(expr * bv3) {
SASSERT(m_bv_util.is_bv(bv3) && m_bv_util.get_bv_size(bv3) == 3);
return m().mk_app(m_fid, OP_FPA_INTERNAL_RM_BVWRAP, 0, 0, 1, &bv3, mk_rm_sort());
}
app * mk_to_fp(sort * s, expr * bv_t) {
SASSERT(is_float(s) && s->get_num_parameters() == 2);
return m().mk_app(m_fid, OP_FPA_TO_FP, 2, s->get_parameters(), 1, &bv_t);
@ -373,6 +368,10 @@ public:
app * mk_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FPA_TO_IEEE_BV, arg1); }
app * mk_bv2rm(expr * bv3) {
SASSERT(m_bv_util.is_bv(bv3) && m_bv_util.get_bv_size(bv3) == 3);
return m().mk_app(m_fid, OP_FPA_INTERNAL_BV2RM, 0, 0, 1, &bv3, mk_rm_sort());
}
app * mk_internal_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
app * mk_internal_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
app * mk_internal_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits);
@ -380,8 +379,8 @@ public:
bool is_bvwrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVWRAP); }
bool is_bvwrap(func_decl * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BVWRAP; }
bool is_rm_bvwrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_RM_BVWRAP); }
bool is_rm_bvwrap(func_decl * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_RM_BVWRAP; }
bool is_bv2rm(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BV2RM); }
bool is_bv2rm(func_decl * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BV2RM; }
bool is_min_interpreted(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_I); }
bool is_min_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED); }

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

@ -100,7 +100,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
SASSERT(num_args == 2); st = BR_FAILED; break;
case OP_FPA_INTERNAL_BVWRAP: SASSERT(num_args == 1); st = mk_bvwrap(args[0], result); break;
case OP_FPA_INTERNAL_RM_BVWRAP:SASSERT(num_args == 1); st = mk_rm(args[0], result); break;
case OP_FPA_INTERNAL_BV2RM: SASSERT(num_args == 1); st = mk_bv2rm(args[0], result); break;
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
@ -719,7 +719,7 @@ br_status fpa_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result)
return BR_FAILED;
}
br_status fpa_rewriter::mk_rm(expr * arg, expr_ref & result) {
br_status fpa_rewriter::mk_bv2rm(expr * arg, expr_ref & result) {
bv_util bu(m());
rational bv_val;
unsigned sz = 0;

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

@ -78,7 +78,7 @@ public:
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_rm(expr * arg, expr_ref & result);
br_status mk_bv2rm(expr * arg, expr_ref & result);
br_status mk_fp(expr * sgn, expr * exp, expr * sig, expr_ref & result);
br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);

35
src/smt/theory_fpa.cpp
View file

@ -75,7 +75,7 @@ namespace smt {
SASSERT(is_rm(f->get_range()));
expr_ref bv(m);
bv = m_th.wrap(m.mk_const(f));
result = m_util.mk_rm(bv);
result = m_util.mk_bv2rm(bv);
m_rm_const2bv.insert(f, result);
m.inc_ref(f);
m.inc_ref(result);
@ -339,18 +339,11 @@ namespace smt {
TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, get_manager()) << std::endl;
tout << "converted term: " << mk_ismt2_pp(e_conv, get_manager()) << std::endl;);
if (is_app(e_conv) && to_app(e_conv)->get_family_id() != get_family_id()) {
UNREACHABLE();
if (!m_fpa_util.is_float(e_conv) && !m_fpa_util.is_rm(e_conv))
m_th_rw(e_conv, res);
else
res = unwrap(wrap(e_conv), m.get_sort(e));
}
else if (m_fpa_util.is_rm(e)) {
SASSERT(m_fpa_util.is_rm_bvwrap(e_conv));
if (m_fpa_util.is_rm(e)) {
SASSERT(m_fpa_util.is_bv2rm(e_conv));
expr_ref bv_rm(m);
m_th_rw(to_app(e_conv)->get_arg(0), bv_rm);
res = m_fpa_util.mk_rm(bv_rm);
res = m_fpa_util.mk_bv2rm(bv_rm);
}
else if (m_fpa_util.is_float(e)) {
SASSERT(m_fpa_util.is_fp(e_conv));
@ -363,20 +356,14 @@ namespace smt {
}
else
UNREACHABLE();
SASSERT(res.get() != 0);
return res;
}
expr_ref theory_fpa::convert_conversion_term(expr * e) {
SASSERT(to_app(e)->get_family_id() == get_family_id());
/* This is for the conversion functions fp.to_* */
ast_manager & m = get_manager();
expr_ref res(m);
proof_ref pr(m);
SASSERT(m_arith_util.is_real(e) || m_bv_util.is_bv(e));
expr_ref res(get_manager());
m_rw(e, res);
m_th_rw(res, res);
return res;
@ -402,10 +389,8 @@ namespace smt {
res = convert_atom(e);
else if (m_fpa_util.is_float(e) || m_fpa_util.is_rm(e))
res = convert_term(e);
else if (m_arith_util.is_real(e) || m_bv_util.is_bv(e))
else
res = convert_conversion_term(e);
else
UNREACHABLE();
TRACE("t_fpa_detail", tout << "converted; caching:" << std::endl;
tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl <<
@ -514,7 +499,6 @@ namespace smt {
case OP_FPA_TO_SBV:
case OP_FPA_TO_REAL:
case OP_FPA_TO_IEEE_BV: {
expr_ref conv(m);
conv = convert(term);
assert_cnstr(m.mk_eq(term, conv));
@ -545,7 +529,7 @@ namespace smt {
if (m_fpa_util.is_rm(s)) {
// For every RM term, we need to make sure that it's
// associated bit-vector is within the valid range.
if (!m_fpa_util.is_rm_bvwrap(owner)) {
if (!m_fpa_util.is_bv2rm(owner)) {
expr_ref valid(m), limit(m);
limit = m_bv_util.mk_numeral(4, 3);
valid = m_bv_util.mk_ule(wrap(owner), limit);
@ -649,7 +633,6 @@ namespace smt {
void theory_fpa::pop_scope_eh(unsigned num_scopes) {
m_trail_stack.pop_scope(num_scopes);
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);
theory::pop_scope_eh(num_scopes);
}
@ -785,7 +768,7 @@ namespace smt {
mk_ismt2_pp(a2, m) << " eq. cls. #" << get_enode(a2)->get_root()->get_owner()->get_id() << std::endl;);
res = vp;
}
else if (m_fpa_util.is_rm_bvwrap(owner)) {
else if (m_fpa_util.is_bv2rm(owner)) {
SASSERT(to_app(owner)->get_num_args() == 1);
app_ref a0(m);
a0 = to_app(owner->get_arg(0));

3
src/smt/theory_fpa.h
View file

@ -144,8 +144,7 @@ namespace smt {
fpa_util & m_fpa_util;
bv_util & m_bv_util;
arith_util & m_arith_util;
obj_map<sort, func_decl*> m_wraps;
obj_map<sort, func_decl*> m_unwraps;
obj_map<sort, func_decl*> m_wraps;
obj_map<expr, expr*> m_conversions;
bool m_is_initialized;
obj_hashtable<func_decl> m_is_added_to_model;

2
src/tactic/fpa/fpa2bv_model_converter.cpp
View file

@ -395,7 +395,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
func_decl * var = it->m_key;
SASSERT(m_fpa_util.is_rm(var->get_range()));
expr * val = it->m_value;
SASSERT(m_fpa_util.is_rm_bvwrap(val));
SASSERT(m_fpa_util.is_bv2rm(val));
expr * bvval = to_app(val)->get_arg(0);
expr_ref fv(m);
fv = convert_bv2rm(bv_mdl, bvval);