mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
preparations for dealing with #2596
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
5bdcc737ec
commit
cc26d49060
|
|
@ -51,7 +51,8 @@ bv2fpa_converter::bv2fpa_converter(ast_manager & m, fpa2bv_converter & conv) :
|
|||
for (auto const& kv : conv.m_uf2bvuf) {
|
||||
m_uf2bvuf.insert(kv.m_key, kv.m_value);
|
||||
m.inc_ref(kv.m_key);
|
||||
m.inc_ref(kv.m_value);
|
||||
m.inc_ref(kv.m_value.first);
|
||||
m.inc_ref(kv.m_value.second);
|
||||
}
|
||||
for (auto const& kv : conv.m_min_max_ufs) {
|
||||
m_specials.insert(kv.m_key, kv.m_value);
|
||||
|
|
@ -64,12 +65,18 @@ bv2fpa_converter::bv2fpa_converter(ast_manager & m, fpa2bv_converter & conv) :
|
|||
bv2fpa_converter::~bv2fpa_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);
|
||||
for (auto const& kv : m_uf2bvuf) {
|
||||
m.dec_ref(kv.m_key);
|
||||
m.dec_ref(kv.m_value.first);
|
||||
m.dec_ref(kv.m_value.second);
|
||||
}
|
||||
for (auto const& kv : m_specials) {
|
||||
m.dec_ref(kv.m_key);
|
||||
m.dec_ref(kv.m_value.first);
|
||||
m.dec_ref(kv.m_value.second);
|
||||
}
|
||||
m_uf2bvuf.reset();
|
||||
m_specials.reset();
|
||||
}
|
||||
|
||||
expr_ref bv2fpa_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig) {
|
||||
|
|
@ -115,19 +122,19 @@ expr_ref bv2fpa_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp, expr
|
|||
return res;
|
||||
}
|
||||
|
||||
expr_ref bv2fpa_converter::convert_bv2fp(model_core * mc, sort * s, app * bv) {
|
||||
expr_ref bv2fpa_converter::convert_bv2fp(model_core * mc, sort * s, expr * bv) {
|
||||
SASSERT(m_bv_util.is_bv(bv));
|
||||
|
||||
unsigned ebits = m_fpa_util.get_ebits(s);
|
||||
unsigned sbits = m_fpa_util.get_sbits(s);
|
||||
unsigned bv_sz = sbits + ebits;
|
||||
|
||||
expr_ref bv_num(m);
|
||||
if (m_bv_util.is_numeral(bv))
|
||||
bv_num = bv;
|
||||
else if (!mc->eval(bv->get_decl(), bv_num))
|
||||
bv_num = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(bv));
|
||||
|
||||
expr_ref bv_num(bv, m);
|
||||
if (!m_bv_util.is_numeral(bv) && is_app(bv)) {
|
||||
if (!mc->eval(to_app(bv)->get_decl(), bv_num)) {
|
||||
bv_num = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(bv));
|
||||
}
|
||||
}
|
||||
expr_ref sgn(m), exp(m), sig(m);
|
||||
sgn = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv_num);
|
||||
exp = m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv_num);
|
||||
|
|
@ -156,27 +163,33 @@ expr_ref bv2fpa_converter::convert_bv2rm(expr * bv_rm) {
|
|||
default: res = m_fpa_util.mk_round_toward_zero();
|
||||
}
|
||||
}
|
||||
else {
|
||||
std::cout << expr_ref(bv_rm, m) << " not converted\n";
|
||||
}
|
||||
|
||||
return res;
|
||||
}
|
||||
|
||||
expr_ref bv2fpa_converter::convert_bv2rm(model_core * mc, app * val) {
|
||||
expr_ref bv2fpa_converter::convert_bv2rm(model_core * mc, expr * val) {
|
||||
expr_ref res(m);
|
||||
|
||||
if (val) {
|
||||
expr_ref eval_v(m);
|
||||
if (m_bv_util.is_numeral(val))
|
||||
res = convert_bv2rm(val);
|
||||
else if (mc->eval(val->get_decl(), eval_v))
|
||||
else if (is_app(val) && mc->eval(to_app(val)->get_decl(), eval_v))
|
||||
res = convert_bv2rm(eval_v);
|
||||
else
|
||||
else {
|
||||
// BUG: doesn't work for parametric definition
|
||||
// needs to be an ite expression.
|
||||
res = m_fpa_util.mk_round_toward_zero();
|
||||
}
|
||||
}
|
||||
|
||||
return res;
|
||||
}
|
||||
|
||||
expr_ref bv2fpa_converter::rebuild_floats(model_core * mc, sort * s, app * e) {
|
||||
expr_ref bv2fpa_converter::rebuild_floats(model_core * mc, sort * s, expr * e) {
|
||||
expr_ref result(m);
|
||||
TRACE("bv2fpa", tout << "rebuild floats in " << mk_ismt2_pp(s, m) << " for ";
|
||||
if (e) tout << mk_ismt2_pp(e, m);
|
||||
|
|
@ -206,11 +219,15 @@ expr_ref bv2fpa_converter::rebuild_floats(model_core * mc, sort * s, app * e) {
|
|||
else if (is_app(e)) {
|
||||
app * a = to_app(e);
|
||||
expr_ref_vector new_args(m);
|
||||
for (unsigned i = 0; i < a->get_num_args(); i++)
|
||||
new_args.push_back(rebuild_floats(mc, a->get_decl()->get_domain()[i], to_app(a->get_arg(i))));
|
||||
for (expr* arg : *a) {
|
||||
new_args.push_back(rebuild_floats(mc, m.get_sort(arg), arg));
|
||||
}
|
||||
result = m.mk_app(a->get_decl(), new_args.size(), new_args.c_ptr());
|
||||
}
|
||||
|
||||
else if (is_var(e)) {
|
||||
result = e;
|
||||
}
|
||||
SASSERT(!result || m.get_sort(result) == s);
|
||||
return result;
|
||||
}
|
||||
|
||||
|
|
@ -288,8 +305,8 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
|
|||
}
|
||||
|
||||
app_ref bv_els(m);
|
||||
bv_els = (app*)bv_fi->get_else();
|
||||
if (bv_els != 0) {
|
||||
bv_els = to_app(bv_fi->get_else());
|
||||
if (bv_els != nullptr) {
|
||||
expr_ref ft_els = rebuild_floats(mc, rng, bv_els);
|
||||
m_th_rw(ft_els);
|
||||
result->set_else(ft_els);
|
||||
|
|
@ -414,14 +431,16 @@ void bv2fpa_converter::convert_min_max_specials(model_core * mc, model_core * ta
|
|||
|
||||
void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen) {
|
||||
for (auto const& kv : m_uf2bvuf) {
|
||||
seen.insert(kv.m_value);
|
||||
|
||||
func_decl * f = kv.m_key;
|
||||
func_decl* f_uf = kv.m_value.first;
|
||||
expr* f_def = kv.m_value.second;
|
||||
seen.insert(f_uf);
|
||||
|
||||
if (f->get_arity() == 0)
|
||||
{
|
||||
array_util au(m);
|
||||
if (au.is_array(f->get_range())) {
|
||||
array_model am = convert_array_func_interp(mc, f, kv.m_value);
|
||||
array_model am = convert_array_func_interp(mc, f, f_uf);
|
||||
if (am.new_float_fd) target_model->register_decl(am.new_float_fd, am.new_float_fi);
|
||||
if (am.result) target_model->register_decl(f, am.result);
|
||||
if (am.bv_fd) seen.insert(am.bv_fd);
|
||||
|
|
@ -430,12 +449,23 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode
|
|||
// Just keep.
|
||||
SASSERT(!m_fpa_util.is_float(f->get_range()) && !m_fpa_util.is_rm(f->get_range()));
|
||||
expr_ref val(m);
|
||||
if (mc->eval(kv.m_value, val))
|
||||
if (mc->eval(f_uf, val))
|
||||
target_model->register_decl(f, val);
|
||||
}
|
||||
}
|
||||
else if (f->get_family_id() == m_fpa_util.get_fid()) {
|
||||
|
||||
if (f_def) {
|
||||
func_interp* fi = alloc(func_interp, m, f->get_arity());
|
||||
expr_ref def = rebuild_floats(mc, f->get_range(), to_app(f_def));
|
||||
fi->set_else(def);
|
||||
SASSERT(m.get_sort(def) == f->get_range());
|
||||
target_model->register_decl(f, fi);
|
||||
func_interp* fj = mc->get_func_interp(f_uf);
|
||||
if (fj) {
|
||||
target_model->register_decl(f_uf, fj->copy());
|
||||
}
|
||||
continue;
|
||||
}
|
||||
// kv.m_value contains the model for the unspecified cases of kv.m_key.
|
||||
// TBD: instead of mapping the interpretation of f to just the graph for the
|
||||
// uninterpreted case, map it to a condition, ite, that filters out the
|
||||
|
|
@ -446,7 +476,7 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode
|
|||
// }
|
||||
|
||||
|
||||
target_model->register_decl(f, convert_func_interp(mc, f, kv.m_value));
|
||||
target_model->register_decl(f, convert_func_interp(mc, f, f_uf));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -468,7 +498,7 @@ void bv2fpa_converter::display(std::ostream & out) {
|
|||
const symbol & n = kv.m_key->get_name();
|
||||
out << "\n (" << n << " ";
|
||||
unsigned indent = n.size() + 4;
|
||||
out << mk_ismt2_pp(kv.m_value, m, indent) << ")";
|
||||
out << mk_ismt2_pp(kv.m_value.first, m, indent) << ")";
|
||||
}
|
||||
for (auto const& kv : m_specials) {
|
||||
const symbol & n = kv.m_key->get_name();
|
||||
|
|
@ -497,10 +527,12 @@ bv2fpa_converter * bv2fpa_converter::translate(ast_translation & translator) {
|
|||
}
|
||||
for (auto const& kv : m_uf2bvuf) {
|
||||
func_decl * k = translator(kv.m_key);
|
||||
func_decl * v = translator(kv.m_value);
|
||||
res->m_uf2bvuf.insert(k, v);
|
||||
func_decl * v = translator(kv.m_value.first);
|
||||
expr* d = translator(kv.m_value.second);
|
||||
res->m_uf2bvuf.insert(k, std::make_pair(v, d));
|
||||
translator.to().inc_ref(k);
|
||||
translator.to().inc_ref(v);
|
||||
translator.to().inc_ref(d);
|
||||
}
|
||||
for (auto const& kv : m_specials) {
|
||||
func_decl * k = translator(kv.m_key);
|
||||
|
|
|
|||
|
|
@ -34,7 +34,7 @@ class bv2fpa_converter {
|
|||
|
||||
obj_map<func_decl, expr*> m_const2bv;
|
||||
obj_map<func_decl, expr*> m_rm_const2bv;
|
||||
obj_map<func_decl, func_decl*> m_uf2bvuf;
|
||||
obj_map<func_decl, std::pair<func_decl*, expr*>> m_uf2bvuf;
|
||||
obj_map<func_decl, std::pair<app*, app*> > m_specials;
|
||||
|
||||
public:
|
||||
|
|
@ -46,9 +46,9 @@ public:
|
|||
bv2fpa_converter * translate(ast_translation & translator);
|
||||
|
||||
expr_ref convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig);
|
||||
expr_ref convert_bv2fp(model_core * mc, sort * s, app * bv);
|
||||
expr_ref convert_bv2fp(model_core * mc, sort * s, expr * bv);
|
||||
expr_ref convert_bv2rm(expr * eval_v);
|
||||
expr_ref convert_bv2rm(model_core * mc, app * val);
|
||||
expr_ref convert_bv2rm(model_core * mc, expr * val);
|
||||
|
||||
void convert_consts(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen);
|
||||
void convert_rm_consts(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen);
|
||||
|
|
@ -56,7 +56,7 @@ public:
|
|||
void convert_uf2bvuf(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen);
|
||||
|
||||
func_interp * convert_func_interp(model_core * mc, func_decl * f, func_decl * bv_f);
|
||||
expr_ref rebuild_floats(model_core * mc, sort * s, app * e);
|
||||
expr_ref rebuild_floats(model_core * mc, sort * s, expr * e);
|
||||
|
||||
class array_model {
|
||||
public:
|
||||
|
|
@ -70,4 +70,4 @@ public:
|
|||
array_model convert_array_func_interp(model_core * mc, func_decl * f, func_decl * bv_f);
|
||||
};
|
||||
|
||||
#endif
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -93,8 +93,8 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
|
|||
|
||||
void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) {
|
||||
if (m_util.is_fp(t) && m_util.is_fp(f)) {
|
||||
expr *t_sgn, *t_sig, *t_exp;
|
||||
expr *f_sgn, *f_sig, *f_exp;
|
||||
expr_ref t_sgn(m), t_sig(m), t_exp(m);
|
||||
expr_ref f_sgn(m), f_sig(m), f_exp(m);
|
||||
split_fp(t, t_sgn, t_exp, t_sig);
|
||||
split_fp(f, f_sgn, f_exp, f_sig);
|
||||
|
||||
|
|
@ -695,7 +695,7 @@ void fpa2bv_converter::mk_neg(func_decl * f, unsigned num, expr * const * args,
|
|||
}
|
||||
|
||||
void fpa2bv_converter::mk_neg(sort * srt, expr_ref & x, expr_ref & result) {
|
||||
expr * sgn, *sig, *e;
|
||||
expr_ref sgn(m), sig(m), e(m);
|
||||
split_fp(x, sgn, e, sig);
|
||||
expr_ref c(m), nsgn(m);
|
||||
mk_is_nan(x, c);
|
||||
|
|
@ -1075,8 +1075,8 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r
|
|||
// exp(x) < exp(y) -> x
|
||||
unsigned ebits = m_util.get_ebits(s);
|
||||
unsigned sbits = m_util.get_sbits(s);
|
||||
expr * x_sgn, *x_sig, *x_exp;
|
||||
expr * y_sgn, *y_sig, *y_exp;
|
||||
expr_ref x_sgn(m), x_sig(m), x_exp(m);
|
||||
expr_ref y_sgn(m), y_sig(m), y_exp(m);
|
||||
split_fp(x, x_sgn, x_exp, x_sig);
|
||||
split_fp(y, y_sgn, y_exp, y_sig);
|
||||
expr_ref one_ebits(m), y_exp_m1(m), xe_lt_yem1(m), ye_neq_zero(m);
|
||||
|
|
@ -1214,7 +1214,7 @@ void fpa2bv_converter::mk_abs(func_decl * f, unsigned num, expr * const * args,
|
|||
}
|
||||
|
||||
void fpa2bv_converter::mk_abs(sort * s, expr_ref & x, expr_ref & result) {
|
||||
expr * sgn, *sig, *exp;
|
||||
expr_ref sgn(m), sig(m), exp(m);
|
||||
split_fp(x, sgn, exp, sig);
|
||||
result = m_util.mk_fp(m_bv_util.mk_numeral(0, 1), exp, sig);
|
||||
}
|
||||
|
|
@ -1224,8 +1224,8 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
|
|||
|
||||
expr * x = args[0], * y = args[1];
|
||||
|
||||
expr * x_sgn, *x_sig, *x_exp;
|
||||
expr * y_sgn, *y_sig, *y_exp;
|
||||
expr_ref x_sgn(m), x_sig(m), x_exp(m);
|
||||
expr_ref y_sgn(m), y_sig(m), y_exp(m);
|
||||
split_fp(x, x_sgn, x_exp, x_sig);
|
||||
split_fp(y, y_sgn, y_exp, y_sig);
|
||||
|
||||
|
|
@ -1269,8 +1269,8 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args,
|
|||
|
||||
expr * x = args[0], *y = args[1];
|
||||
|
||||
expr * x_sgn, *x_sig, *x_exp;
|
||||
expr * y_sgn, *y_sig, *y_exp;
|
||||
expr_ref x_sgn(m), x_sig(m), x_exp(m);
|
||||
expr_ref y_sgn(m), y_sig(m), y_exp(m);
|
||||
split_fp(x, x_sgn, x_exp, x_sig);
|
||||
split_fp(y, y_sgn, y_exp, y_sig);
|
||||
|
||||
|
|
@ -2150,8 +2150,8 @@ void fpa2bv_converter::mk_float_eq(sort * s, expr_ref & x, expr_ref & y, expr_re
|
|||
mk_is_zero(y, y_is_zero);
|
||||
m_simp.mk_and(x_is_zero, y_is_zero, c2);
|
||||
|
||||
expr * x_sgn, * x_sig, * x_exp;
|
||||
expr * y_sgn, * y_sig, * y_exp;
|
||||
expr_ref x_sgn(m), x_sig(m), x_exp(m);
|
||||
expr_ref y_sgn(m), y_sig(m), y_exp(m);
|
||||
split_fp(x, x_sgn, x_exp, x_sig);
|
||||
split_fp(y, y_sgn, y_exp, y_sig);
|
||||
|
||||
|
|
@ -2189,8 +2189,8 @@ void fpa2bv_converter::mk_float_lt(sort * s, expr_ref & x, expr_ref & y, expr_re
|
|||
mk_is_zero(y, y_is_zero);
|
||||
m_simp.mk_and(x_is_zero, y_is_zero, c2);
|
||||
|
||||
expr * x_sgn, * x_sig, * x_exp;
|
||||
expr * y_sgn, * y_sig, * y_exp;
|
||||
expr_ref x_sgn(m), x_sig(m), x_exp(m);
|
||||
expr_ref y_sgn(m), y_sig(m), y_exp(m);
|
||||
split_fp(x, x_sgn, x_exp, x_sig);
|
||||
split_fp(y, y_sgn, y_exp, y_sig);
|
||||
|
||||
|
|
@ -3140,7 +3140,7 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
|
|||
void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
SASSERT(num == 1);
|
||||
expr_ref x(m), x_is_nan(m);
|
||||
expr * sgn, * s, * e;
|
||||
expr_ref sgn(m), s(m), e(m);
|
||||
x = args[0];
|
||||
split_fp(x, sgn, e, s);
|
||||
mk_is_nan(x, x_is_nan);
|
||||
|
|
@ -3201,6 +3201,30 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
|
|||
sort * xs = m.get_sort(x);
|
||||
sort * bv_srt = f->get_range();
|
||||
|
||||
#if 0
|
||||
// for this to work, the following is required:
|
||||
// 1. split_fp should succeed even if the argument does not satisfy is_fp
|
||||
// we would need functions to access the sgn, exp and sig fields
|
||||
// 2. an inverse of bv2rm, here called rm2bv.
|
||||
expr_ref arg1(m), arg2(m), _rm(m);
|
||||
|
||||
var_subst vsubst(m, false);
|
||||
expr* def = get_bv_def(f);
|
||||
if (def) {
|
||||
result = vsubst(def, 2, args);
|
||||
return;
|
||||
}
|
||||
arg1 = m.mk_var(0, m.get_sort(args[0]));
|
||||
arg2 = m.mk_var(1, m.get_sort(args[1]));
|
||||
_rm = m_util.mk_rm2bv(arg1);
|
||||
rm = _rm;
|
||||
x = arg2;
|
||||
#endif
|
||||
|
||||
expr_ref sgn(m), sig(m), exp(m), lz(m);
|
||||
unpack(x, sgn, sig, exp, lz, true);
|
||||
|
||||
|
||||
unsigned ebits = m_util.get_ebits(xs);
|
||||
unsigned sbits = m_util.get_sbits(xs);
|
||||
unsigned bv_sz = (unsigned)f->get_parameter(0).get_int();
|
||||
|
|
@ -3230,8 +3254,6 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
|
|||
dbg_decouple("fpa2bv_to_bv_c2", c2);
|
||||
|
||||
// Otherwise...
|
||||
expr_ref sgn(m), sig(m), exp(m), lz(m);
|
||||
unpack(x, sgn, sig, exp, lz, true);
|
||||
|
||||
dbg_decouple("fpa2bv_to_bv_sgn", sgn);
|
||||
dbg_decouple("fpa2bv_to_bv_sig", sig);
|
||||
|
|
@ -3348,6 +3370,10 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
|
|||
result = m.mk_ite(c2, v2, result);
|
||||
result = m.mk_ite(c1, v1, result);
|
||||
|
||||
#if 0
|
||||
set_bv_def(f, result);
|
||||
result = vsubst(result, 2, args);
|
||||
#endif
|
||||
SASSERT(is_well_sorted(m, result));
|
||||
}
|
||||
|
||||
|
|
@ -3416,34 +3442,23 @@ void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, e
|
|||
TRACE("fpa2bv_mk_fp", tout << "mk_fp result = " << mk_ismt2_pp(result, m) << std::endl;);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const {
|
||||
SASSERT(m_util.is_fp(e));
|
||||
SASSERT(to_app(e)->get_num_args() == 3);
|
||||
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_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const {
|
||||
SASSERT(m_util.is_fp(e));
|
||||
SASSERT(to_app(e)->get_num_args() == 3);
|
||||
expr *e_sgn, *e_sig, *e_exp;
|
||||
split_fp(e, e_sgn, e_exp, e_sig);
|
||||
expr* e_sgn = nullptr, *e_exp = nullptr, *e_sig = nullptr;
|
||||
VERIFY(m_util.is_fp(e, e_sgn, e_exp, e_sig));
|
||||
sgn = e_sgn;
|
||||
exp = e_exp;
|
||||
sig = e_sig;
|
||||
}
|
||||
|
||||
void fpa2bv_converter::join_fp(expr * e, expr_ref & res) {
|
||||
SASSERT(m_util.is_fp(e));
|
||||
SASSERT(to_app(e)->get_num_args() == 3);
|
||||
expr *sgn, *exp, *sig;
|
||||
expr_ref sgn(m), exp(m), sig(m);
|
||||
split_fp(e, sgn, exp, sig);
|
||||
res = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, exp), sig);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) {
|
||||
expr * sgn, * sig, * exp;
|
||||
expr_ref sgn(m), sig(m), exp(m);
|
||||
split_fp(e, sgn, exp, sig);
|
||||
|
||||
// exp == 1^n , sig != 0
|
||||
|
|
@ -3458,7 +3473,7 @@ void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) {
|
|||
}
|
||||
|
||||
void fpa2bv_converter::mk_is_inf(expr * e, expr_ref & result) {
|
||||
expr * sgn, * sig, * exp;
|
||||
expr_ref sgn(m), sig(m), exp(m);
|
||||
split_fp(e, sgn, exp, sig);
|
||||
expr_ref eq1(m), eq2(m), top_exp(m), zero(m);
|
||||
mk_top_exp(m_bv_util.get_bv_size(exp), top_exp);
|
||||
|
|
@ -3501,7 +3516,7 @@ void fpa2bv_converter::mk_is_neg(expr * e, expr_ref & result) {
|
|||
}
|
||||
|
||||
void fpa2bv_converter::mk_is_zero(expr * e, expr_ref & result) {
|
||||
expr * sgn, * sig, * exp;
|
||||
expr_ref sgn(m), sig(m), exp(m);
|
||||
split_fp(e, sgn, exp, sig);
|
||||
expr_ref eq1(m), eq2(m), bot_exp(m), zero(m);
|
||||
mk_bot_exp(m_bv_util.get_bv_size(exp), bot_exp);
|
||||
|
|
@ -3512,7 +3527,7 @@ void fpa2bv_converter::mk_is_zero(expr * e, expr_ref & result) {
|
|||
}
|
||||
|
||||
void fpa2bv_converter::mk_is_nzero(expr * e, expr_ref & result) {
|
||||
expr * sgn, * sig, * exp;
|
||||
expr_ref sgn(m), sig(m), exp(m);
|
||||
split_fp(e, sgn, exp, sig);
|
||||
expr_ref e_is_zero(m), eq(m), one_1(m);
|
||||
mk_is_zero(e, e_is_zero);
|
||||
|
|
@ -3522,7 +3537,7 @@ void fpa2bv_converter::mk_is_nzero(expr * e, expr_ref & result) {
|
|||
}
|
||||
|
||||
void fpa2bv_converter::mk_is_pzero(expr * e, expr_ref & result) {
|
||||
expr * sgn, * sig, * exp;
|
||||
expr_ref sgn(m), sig(m), exp(m);
|
||||
split_fp(e, sgn, exp, sig);
|
||||
expr_ref e_is_zero(m), eq(m), nil_1(m);
|
||||
mk_is_zero(e, e_is_zero);
|
||||
|
|
@ -3532,7 +3547,7 @@ void fpa2bv_converter::mk_is_pzero(expr * e, expr_ref & result) {
|
|||
}
|
||||
|
||||
void fpa2bv_converter::mk_is_denormal(expr * e, expr_ref & result) {
|
||||
expr * sgn, *sig, *exp;
|
||||
expr_ref sgn(m), sig(m), exp(m);
|
||||
split_fp(e, sgn, exp, sig);
|
||||
|
||||
expr_ref zero(m), zexp(m), is_zero(m), n_is_zero(m);
|
||||
|
|
@ -3545,7 +3560,7 @@ void fpa2bv_converter::mk_is_denormal(expr * e, expr_ref & result) {
|
|||
}
|
||||
|
||||
void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) {
|
||||
expr * sgn, * sig, * exp;
|
||||
expr_ref sgn(m), sig(m), exp(m);
|
||||
split_fp(e, sgn, exp, sig);
|
||||
|
||||
expr_ref is_special(m), is_denormal(m), p(m), is_zero(m);
|
||||
|
|
@ -3779,7 +3794,7 @@ void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
|
|||
// CMW: This works only for quantifier-free formulas.
|
||||
if (m_util.is_fp(e)) {
|
||||
expr_ref new_bv(m);
|
||||
expr *e_sgn, *e_sig, *e_exp;
|
||||
expr_ref e_sgn(m), e_sig(m), e_exp(m);
|
||||
split_fp(e, e_sgn, e_exp, e_sig);
|
||||
unsigned ebits = m_bv_util.get_bv_size(e_exp);
|
||||
unsigned sbits = m_bv_util.get_bv_size(e_sig) + 1;
|
||||
|
|
@ -4173,24 +4188,52 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
|
|||
void fpa2bv_converter::reset() {
|
||||
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);
|
||||
for (auto const& kv : m_uf2bvuf) {
|
||||
m.dec_ref(kv.m_key);
|
||||
m.dec_ref(kv.m_value.first);
|
||||
m.dec_ref(kv.m_value.second);
|
||||
}
|
||||
for (auto const& kv : m_min_max_ufs) {
|
||||
m.dec_ref(kv.m_key);
|
||||
m.dec_ref(kv.m_value.first);
|
||||
m.dec_ref(kv.m_value.second);
|
||||
}
|
||||
m_uf2bvuf.reset();
|
||||
m_min_max_ufs.reset();
|
||||
m_extra_assertions.reset();
|
||||
}
|
||||
|
||||
func_decl * fpa2bv_converter::mk_bv_uf(func_decl * f, sort * const * domain, sort * range) {
|
||||
func_decl * res;
|
||||
std::pair<func_decl*, expr*> res;
|
||||
if (!m_uf2bvuf.find(f, res)) {
|
||||
res = m.mk_fresh_func_decl(nullptr, f->get_arity(), domain, range);
|
||||
m_uf2bvuf.insert(f, res);
|
||||
res.first = m.mk_fresh_func_decl(nullptr, f->get_arity(), domain, range);
|
||||
res.second = nullptr;
|
||||
m.inc_ref(f);
|
||||
m.inc_ref(res);
|
||||
TRACE("fpa2bv", tout << "New UF func_decl: " << std::endl << mk_ismt2_pp(res, m) << std::endl;);
|
||||
m.inc_ref(res.first);
|
||||
m_uf2bvuf.insert(f, res);
|
||||
TRACE("fpa2bv", tout << "New UF func_decl: " << res.first->get_id() << std::endl << mk_ismt2_pp(res.first, m) << std::endl;);
|
||||
}
|
||||
return res;
|
||||
return res.first;
|
||||
}
|
||||
|
||||
expr* fpa2bv_converter::get_bv_def(func_decl* f) {
|
||||
std::pair<func_decl*, expr*> res(nullptr, nullptr);
|
||||
m_uf2bvuf.find(f, res);
|
||||
TRACE("fpa2bv", tout << "get_bv_def " << mk_ismt2_pp(res.first, m) << " " << res.second << std::endl;);
|
||||
return res.second;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief expand the definition of bit-vector function f
|
||||
as an expression of what is defined and what is not
|
||||
defined.
|
||||
*/
|
||||
void fpa2bv_converter::set_bv_def(func_decl* f, expr* def) {
|
||||
auto res = m_uf2bvuf[f];
|
||||
SASSERT(res.first);
|
||||
SASSERT(!res.second);
|
||||
res.second = def;
|
||||
m.inc_ref(def);
|
||||
m_uf2bvuf.insert(f, res);
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -35,7 +35,7 @@ class fpa2bv_converter {
|
|||
public:
|
||||
typedef obj_map<func_decl, std::pair<app *, app *> > special_t;
|
||||
typedef obj_map<func_decl, expr*> const2bv_t;
|
||||
typedef obj_map<func_decl, func_decl*> uf2bvuf_t;
|
||||
typedef obj_map<func_decl, std::pair<func_decl*, expr*> > uf2bvuf_t;
|
||||
|
||||
protected:
|
||||
ast_manager & m;
|
||||
|
|
@ -74,7 +74,7 @@ public:
|
|||
|
||||
void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
|
||||
void split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const;
|
||||
// void split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const;
|
||||
void split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const;
|
||||
void join_fp(expr * e, expr_ref & res);
|
||||
|
||||
|
|
@ -219,6 +219,9 @@ private:
|
|||
void mk_to_fp_float(sort * s, expr * rm, expr * x, expr_ref & result);
|
||||
|
||||
func_decl * mk_bv_uf(func_decl * f, sort * const * domain, sort * range);
|
||||
void set_bv_def(func_decl * f, expr* def);
|
||||
expr* get_bv_def(func_decl * f);
|
||||
|
||||
expr_ref nan_wrap(expr * n);
|
||||
|
||||
expr_ref extra_quantify(expr * e);
|
||||
|
|
|
|||
|
|
@ -226,7 +226,7 @@ public:
|
|||
bool is_rm(sort * s) const { return is_sort_of(s, m_fid, ROUNDING_MODE_SORT); }
|
||||
bool is_float(expr * e) const { return is_float(m_manager.get_sort(e)); }
|
||||
bool is_rm(expr * e) const { return is_rm(m_manager.get_sort(e)); }
|
||||
bool is_fp(expr * e) const { return is_app_of(e, m_fid, OP_FPA_FP); }
|
||||
bool is_fp(expr const * e) const { return is_app_of(e, m_fid, OP_FPA_FP); }
|
||||
unsigned get_ebits(sort * s) const;
|
||||
unsigned get_sbits(sort * s) const;
|
||||
|
||||
|
|
@ -357,6 +357,8 @@ public:
|
|||
bool is_to_ieee_bv(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_IEEE_BV; }
|
||||
|
||||
bool contains_floats(ast * a);
|
||||
|
||||
MATCH_TERNARY(is_fp);
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -87,7 +87,7 @@ class fpa2bv_tactic : public tactic {
|
|||
// Inject auxiliary lemmas that fix e to the one and only NaN value,
|
||||
// that is (= e (fp #b0 #b1...1 #b0...01)), so that the value propagation
|
||||
// has a value to propagate.
|
||||
expr * sgn, *sig, *exp;
|
||||
expr_ref sgn(m), sig(m), exp(m);
|
||||
m_conv.split_fp(new_curr, sgn, exp, sig);
|
||||
result.back()->assert_expr(m.mk_eq(sgn, m_conv.bu().mk_numeral(0, 1)));
|
||||
result.back()->assert_expr(m.mk_eq(exp, m_conv.bu().mk_bv_neg(m_conv.bu().mk_numeral(1, m_conv.bu().get_bv_size(exp)))));
|
||||
|
|
|
|||
Loading…
Reference in a new issue