mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

fpa2bv: added reset(), adjustments for consistency

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-12-28 13:33:19 +00:00
parent 6ebeebde50
commit 55662bcf6b
2 changed files with 29 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -37,19 +37,7 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
}
fpa2bv_converter::~fpa2bv_converter() {
dec_ref_map_key_values(m, m_const2bv);
dec_ref_map_key_values(m, m_rm_const2bv);
dec_ref_map_key_values(m, m_uf2bvuf);
obj_map<func_decl, func_decl_triple>::iterator it = m_uf23bvuf.begin();
obj_map<func_decl, func_decl_triple>::iterator end = m_uf23bvuf.end();
for (; it != end; ++it) {
m.dec_ref(it->m_key);
m.dec_ref(it->m_value.f_sgn);
m.dec_ref(it->m_value.f_sig);
m.dec_ref(it->m_value.f_exp);
}
m_uf23bvuf.reset();
reset();
}
void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
@ -58,8 +46,8 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
expr_ref sgn(m), s(m), e(m);
m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), sgn);
m_simp.mk_eq(to_app(a)->get_arg(1), to_app(b)->get_arg(1), s);
m_simp.mk_eq(to_app(a)->get_arg(2), to_app(b)->get_arg(2), e);
m_simp.mk_eq(to_app(a)->get_arg(1), to_app(b)->get_arg(1), e);
m_simp.mk_eq(to_app(a)->get_arg(2), to_app(b)->get_arg(2), s);
// The SMT FPA theory asks for _one_ NaN value, but the bit-blasting
// has many, like IEEE754. This encoding of equality makes it look like
@ -2261,7 +2249,7 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
// The exponent is at most bv_sz, i.e., we need ld(bv_sz)+1 ebits.
// exp < bv_sz (+sign bit which is [0])
unsigned exp_worst_case_sz = (unsigned)((log(bv_sz) / log(2)) + 1);
unsigned exp_worst_case_sz = (unsigned)((log((double)bv_sz) / log((double)2)) + 1.0);
if (exp_sz < exp_worst_case_sz) {
// exp_sz < exp_worst_case_sz and exp >= 0.
@ -2473,9 +2461,9 @@ void fpa2bv_converter::split_triple(expr * e, expr * & sgn, expr * & sig, expr *
SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FLOAT_TO_FP));
SASSERT(to_app(e)->get_num_args() == 3);
sgn = to_app(e)->get_arg(0);
sig = to_app(e)->get_arg(2);
sgn = to_app(e)->get_arg(0);
exp = to_app(e)->get_arg(1);
sig = to_app(e)->get_arg(2);
}
void fpa2bv_converter::split_triple(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp) const {
@ -3140,3 +3128,22 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
TRACE("fpa2bv_round", tout << "ROUND = " << mk_ismt2_pp(result, m) << std::endl; );
}
void fpa2bv_converter::reset(void) {
dec_ref_map_key_values(m, m_const2bv);
dec_ref_map_key_values(m, m_rm_const2bv);
dec_ref_map_key_values(m, m_uf2bvuf);
obj_map<func_decl, func_decl_triple>::iterator it = m_uf23bvuf.begin();
obj_map<func_decl, func_decl_triple>::iterator end = m_uf23bvuf.end();
for (; it != end; ++it) {
m.dec_ref(it->m_key);
m.dec_ref(it->m_value.f_sgn);
m.dec_ref(it->m_value.f_sig);
m.dec_ref(it->m_value.f_exp);
}
m_uf23bvuf.reset();
m_extra_assertions.reset();
}

4
src/ast/fpa/fpa2bv_converter.h
View file

@ -63,6 +63,7 @@ public:
float_util & fu() { return m_util; }
bv_util & bu() { return m_bv_util; }
arith_util & au() { return m_arith_util; }
bool is_float(sort * s) { return m_util.is_float(s); }
bool is_float(expr * e) { return is_app(e) && m_util.is_float(to_app(e)->get_decl()->get_range()); }
@ -141,11 +142,14 @@ public:
obj_map<func_decl, func_decl*> const & uf2bvuf() const { return m_uf2bvuf; }
obj_map<func_decl, func_decl_triple> const & uf23bvuf() const { return m_uf23bvuf; }
void reset(void);
void dbg_decouple(const char * prefix, expr_ref & e);
expr_ref_vector m_extra_assertions;
void mk_internal_bvwrap(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_internal_bvunwrap(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
protected:
void mk_is_nan(expr * e, expr_ref & result);
void mk_is_inf(expr * e, expr_ref & result);