mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Tabs

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-10-18 13:18:59 +01:00
parent edaec81aa2
commit 5ac3bb04ee
3 changed files with 531 additions and 531 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

826
src/ast/fpa/bv2fpa_converter.cpp
View file

@ -1,17 +1,17 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Copyright (c) 2012 Microsoft Corporation
Module Name:
bv2fpa_converter.cpp
bv2fpa_converter.cpp
Abstract:
Model conversion for fpa2bv_converter
Model conversion for fpa2bv_converter
Author:
Christoph (cwinter) 2016-10-15
Christoph (cwinter) 2016-10-15
Notes:
@ -27,299 +27,299 @@ Notes:
bv2fpa_converter::bv2fpa_converter(ast_manager & m) :
m(m),
m_fpa_util(m),
m_bv_util(m),
m_th_rw(m) {
m(m),
m_fpa_util(m),
m_bv_util(m),
m_th_rw(m) {
}
bv2fpa_converter::bv2fpa_converter(ast_manager & m, fpa2bv_converter & conv) :
m(m),
m_fpa_util(m),
m_bv_util(m),
m_th_rw(m) {
for (obj_map<func_decl, expr*>::iterator it = conv.m_const2bv.begin();
it != conv.m_const2bv.end();
it++)
{
m_const2bv.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
}
for (obj_map<func_decl, expr*>::iterator it = conv.m_rm_const2bv.begin();
it != conv.m_rm_const2bv.end();
it++)
{
m_rm_const2bv.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
}
for (obj_map<func_decl, func_decl*>::iterator it = conv.m_uf2bvuf.begin();
it != conv.m_uf2bvuf.end();
it++)
{
m_uf2bvuf.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
}
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = conv.m_min_max_specials.begin();
it != conv.m_min_max_specials.end();
it++) {
m_specials.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value.first);
m.inc_ref(it->m_value.second);
}
m(m),
m_fpa_util(m),
m_bv_util(m),
m_th_rw(m) {
for (obj_map<func_decl, expr*>::iterator it = conv.m_const2bv.begin();
it != conv.m_const2bv.end();
it++)
{
m_const2bv.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
}
for (obj_map<func_decl, expr*>::iterator it = conv.m_rm_const2bv.begin();
it != conv.m_rm_const2bv.end();
it++)
{
m_rm_const2bv.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
}
for (obj_map<func_decl, func_decl*>::iterator it = conv.m_uf2bvuf.begin();
it != conv.m_uf2bvuf.end();
it++)
{
m_uf2bvuf.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
}
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = conv.m_min_max_specials.begin();
it != conv.m_min_max_specials.end();
it++) {
m_specials.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value.first);
m.inc_ref(it->m_value.second);
}
}
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 (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.end();
it++) {
m.dec_ref(it->m_key);
m.dec_ref(it->m_value.first);
m.dec_ref(it->m_value.second);
}
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 (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.end();
it++) {
m.dec_ref(it->m_key);
m.dec_ref(it->m_value.first);
m.dec_ref(it->m_value.second);
}
}
expr_ref bv2fpa_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig) {
unsynch_mpz_manager & mpzm = m_fpa_util.fm().mpz_manager();
unsynch_mpq_manager & mpqm = m_fpa_util.fm().mpq_manager();
unsynch_mpz_manager & mpzm = m_fpa_util.fm().mpz_manager();
unsynch_mpq_manager & mpqm = m_fpa_util.fm().mpq_manager();
expr_ref res(m);
mpf fp_val;
expr_ref res(m);
mpf fp_val;
unsigned ebits = m_fpa_util.get_ebits(s);
unsigned sbits = m_fpa_util.get_sbits(s);
unsigned ebits = m_fpa_util.get_ebits(s);
unsigned sbits = m_fpa_util.get_sbits(s);
unsigned sgn_sz = 1;
unsigned exp_sz = ebits;
unsigned sig_sz = sbits - 1;
unsigned sgn_sz = 1;
unsigned exp_sz = ebits;
unsigned sig_sz = sbits - 1;
rational sgn_q(0), sig_q(0), exp_q(0);
rational sgn_q(0), sig_q(0), exp_q(0);
if (sgn) m_bv_util.is_numeral(sgn, sgn_q, sgn_sz);
if (exp) m_bv_util.is_numeral(exp, exp_q, exp_sz);
if (sig) m_bv_util.is_numeral(sig, sig_q, sig_sz);
if (sgn) m_bv_util.is_numeral(sgn, sgn_q, sgn_sz);
if (exp) m_bv_util.is_numeral(exp, exp_q, exp_sz);
if (sig) m_bv_util.is_numeral(sig, sig_q, sig_sz);
// un-bias exponent
rational exp_unbiased_q;
exp_unbiased_q = exp_q - m_fpa_util.fm().m_powers2.m1(ebits - 1);
// un-bias exponent
rational exp_unbiased_q;
exp_unbiased_q = exp_q - m_fpa_util.fm().m_powers2.m1(ebits - 1);
mpz sig_z; mpf_exp_t exp_z;
mpzm.set(sig_z, sig_q.to_mpq().numerator());
exp_z = mpzm.get_int64(exp_unbiased_q.to_mpq().numerator());
mpz sig_z; mpf_exp_t exp_z;
mpzm.set(sig_z, sig_q.to_mpq().numerator());
exp_z = mpzm.get_int64(exp_unbiased_q.to_mpq().numerator());
m_fpa_util.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), exp_z, sig_z);
m_fpa_util.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), exp_z, sig_z);
mpzm.del(sig_z);
mpzm.del(sig_z);
res = m_fpa_util.mk_value(fp_val);
res = m_fpa_util.mk_value(fp_val);
TRACE("bv2fpa", tout << "[" << mk_ismt2_pp(sgn, m) <<
" " << mk_ismt2_pp(exp, m) <<
" " << mk_ismt2_pp(sig, m) << "] == " <<
mk_ismt2_pp(res, m) << std::endl;);
m_fpa_util.fm().del(fp_val);
TRACE("bv2fpa", tout << "[" << mk_ismt2_pp(sgn, m) <<
" " << mk_ismt2_pp(exp, m) <<
" " << mk_ismt2_pp(sig, m) << "] == " <<
mk_ismt2_pp(res, m) << std::endl;);
m_fpa_util.fm().del(fp_val);
return res;
return res;
}
expr_ref bv2fpa_converter::convert_bv2fp(model_core * mc, sort * s, app * bv) {
SASSERT(m_bv_util.is_bv(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;
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(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 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);
sig = m_bv_util.mk_extract(sbits - 2, 0, bv_num);
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);
sig = m_bv_util.mk_extract(sbits - 2, 0, bv_num);
expr_ref v_sgn(m), v_exp(m), v_sig(m);
m_th_rw(sgn, v_sgn);
m_th_rw(exp, v_exp);
m_th_rw(sig, v_sig);
expr_ref v_sgn(m), v_exp(m), v_sig(m);
m_th_rw(sgn, v_sgn);
m_th_rw(exp, v_exp);
m_th_rw(sig, v_sig);
return convert_bv2fp(s, v_sgn, v_exp, v_sig);
return convert_bv2fp(s, v_sgn, v_exp, v_sig);
}
expr_ref bv2fpa_converter::convert_bv2rm(expr * bv_rm) {
expr_ref res(m);
rational bv_val(0);
unsigned sz = 0;
expr_ref res(m);
rational bv_val(0);
unsigned sz = 0;
if (m_bv_util.is_numeral(bv_rm, bv_val, sz)) {
SASSERT(bv_val.is_uint64());
switch (bv_val.get_uint64()) {
case BV_RM_TIES_TO_AWAY: res = m_fpa_util.mk_round_nearest_ties_to_away(); break;
case BV_RM_TIES_TO_EVEN: res = m_fpa_util.mk_round_nearest_ties_to_even(); break;
case BV_RM_TO_NEGATIVE: res = m_fpa_util.mk_round_toward_negative(); break;
case BV_RM_TO_POSITIVE: res = m_fpa_util.mk_round_toward_positive(); break;
case BV_RM_TO_ZERO:
default: res = m_fpa_util.mk_round_toward_zero();
}
}
if (m_bv_util.is_numeral(bv_rm, bv_val, sz)) {
SASSERT(bv_val.is_uint64());
switch (bv_val.get_uint64()) {
case BV_RM_TIES_TO_AWAY: res = m_fpa_util.mk_round_nearest_ties_to_away(); break;
case BV_RM_TIES_TO_EVEN: res = m_fpa_util.mk_round_nearest_ties_to_even(); break;
case BV_RM_TO_NEGATIVE: res = m_fpa_util.mk_round_toward_negative(); break;
case BV_RM_TO_POSITIVE: res = m_fpa_util.mk_round_toward_positive(); break;
case BV_RM_TO_ZERO:
default: res = m_fpa_util.mk_round_toward_zero();
}
}
return res;
return res;
}
expr_ref bv2fpa_converter::convert_bv2rm(model_core * mc, app * val) {
expr_ref res(m);
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))
res = convert_bv2rm(eval_v);
else
res = m_fpa_util.mk_round_toward_zero();
}
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))
res = convert_bv2rm(eval_v);
else
res = m_fpa_util.mk_round_toward_zero();
}
return res;
return res;
}
expr_ref bv2fpa_converter::rebuild_floats(model_core * mc, sort * s, app * 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);
else tout << "nil";
tout << std::endl; );
expr_ref result(m);
TRACE("bv2fpa", tout << "rebuild floats in " << mk_ismt2_pp(s, m) << " for ";
if (e) tout << mk_ismt2_pp(e, m);
else tout << "nil";
tout << std::endl; );
if (m_fpa_util.is_float(s)) {
if (e == 0)
result = m_fpa_util.mk_pzero(s);
else if (m_fpa_util.is_numeral(e))
result = e;
else {
SASSERT(m_bv_util.is_bv(e) && m_bv_util.get_bv_size(e) == (m_fpa_util.get_ebits(s) + m_fpa_util.get_sbits(s)));
result = convert_bv2fp(mc, s, e);
}
}
else if (m_fpa_util.is_rm(s)) {
if (e == 0)
result = m_fpa_util.mk_round_toward_zero();
else if (m_fpa_util.is_rm_numeral(e))
result = e;
else {
SASSERT(m_bv_util.is_bv(e) && m_bv_util.get_bv_size(e) == 3);
result = convert_bv2rm(mc, 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))));
result = m.mk_app(a->get_decl(), new_args.size(), new_args.c_ptr());
}
if (m_fpa_util.is_float(s)) {
if (e == 0)
result = m_fpa_util.mk_pzero(s);
else if (m_fpa_util.is_numeral(e))
result = e;
else {
SASSERT(m_bv_util.is_bv(e) && m_bv_util.get_bv_size(e) == (m_fpa_util.get_ebits(s) + m_fpa_util.get_sbits(s)));
result = convert_bv2fp(mc, s, e);
}
}
else if (m_fpa_util.is_rm(s)) {
if (e == 0)
result = m_fpa_util.mk_round_toward_zero();
else if (m_fpa_util.is_rm_numeral(e))
result = e;
else {
SASSERT(m_bv_util.is_bv(e) && m_bv_util.get_bv_size(e) == 3);
result = convert_bv2rm(mc, 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))));
result = m.mk_app(a->get_decl(), new_args.size(), new_args.c_ptr());
}
return result;
return result;
}
bv2fpa_converter::array_model bv2fpa_converter::convert_array_func_interp(model_core * mc, func_decl * f, func_decl * bv_f) {
SASSERT(f->get_arity() == 0);
array_util arr_util(m);
SASSERT(f->get_arity() == 0);
array_util arr_util(m);
array_model am(m);
sort_ref_vector array_domain(m);
unsigned arity = f->get_range()->get_num_parameters()-1;
array_model am(m);
sort_ref_vector array_domain(m);
unsigned arity = f->get_range()->get_num_parameters()-1;
expr_ref as_arr_mdl(m);
as_arr_mdl = mc->get_const_interp(bv_f);
if (as_arr_mdl == 0) return am;
TRACE("bv2fpa", tout << "arity=0 func_interp for " << mk_ismt2_pp(f, m) << " := " << mk_ismt2_pp(as_arr_mdl, m) << std::endl;);
SASSERT(arr_util.is_as_array(as_arr_mdl));
for (unsigned i = 0; i < arity; i++)
array_domain.push_back(to_sort(f->get_range()->get_parameter(i).get_ast()));
sort * rng = to_sort(f->get_range()->get_parameter(arity).get_ast());
expr_ref as_arr_mdl(m);
as_arr_mdl = mc->get_const_interp(bv_f);
if (as_arr_mdl == 0) return am;
TRACE("bv2fpa", tout << "arity=0 func_interp for " << mk_ismt2_pp(f, m) << " := " << mk_ismt2_pp(as_arr_mdl, m) << std::endl;);
SASSERT(arr_util.is_as_array(as_arr_mdl));
for (unsigned i = 0; i < arity; i++)
array_domain.push_back(to_sort(f->get_range()->get_parameter(i).get_ast()));
sort * rng = to_sort(f->get_range()->get_parameter(arity).get_ast());
bv_f = arr_util.get_as_array_func_decl(to_app(as_arr_mdl));
bv_f = arr_util.get_as_array_func_decl(to_app(as_arr_mdl));
am.new_float_fd = m.mk_fresh_func_decl(arity, array_domain.c_ptr(), rng);
am.new_float_fi = convert_func_interp(mc, am.new_float_fd, bv_f);
am.bv_fd = bv_f;
am.result = arr_util.mk_as_array(f->get_range(), am.new_float_fd);
return am;
am.new_float_fd = m.mk_fresh_func_decl(arity, array_domain.c_ptr(), rng);
am.new_float_fi = convert_func_interp(mc, am.new_float_fd, bv_f);
am.bv_fd = bv_f;
am.result = arr_util.mk_as_array(f->get_range(), am.new_float_fd);
return am;
}
func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl * f, func_decl * bv_f) {
SASSERT(f->get_arity() > 0);
func_interp * result = 0;
sort * rng = f->get_range();
sort * const * dmn = f->get_domain();
SASSERT(f->get_arity() > 0);
func_interp * result = 0;
sort * rng = f->get_range();
sort * const * dmn = f->get_domain();
unsigned arity = bv_f->get_arity();
func_interp * bv_fi = mc->get_func_interp(bv_f);
unsigned arity = bv_f->get_arity();
func_interp * bv_fi = mc->get_func_interp(bv_f);
if (bv_fi != 0) {
fpa_rewriter rw(m);
expr_ref ai(m);
result = alloc(func_interp, m, arity);
if (bv_fi != 0) {
fpa_rewriter rw(m);
expr_ref ai(m);
result = alloc(func_interp, m, arity);
for (unsigned i = 0; i < bv_fi->num_entries(); i++) {
func_entry const * bv_fe = bv_fi->get_entry(i);
expr * const * bv_args = bv_fe->get_args();
expr_ref_buffer new_args(m);
for (unsigned i = 0; i < bv_fi->num_entries(); i++) {
func_entry const * bv_fe = bv_fi->get_entry(i);
expr * const * bv_args = bv_fe->get_args();
expr_ref_buffer new_args(m);
for (unsigned j = 0; j < arity; j++) {
sort * ft_dj = dmn[j];
expr * bv_aj = bv_args[j];
ai = rebuild_floats(mc, ft_dj, to_app(bv_aj));
m_th_rw(ai);
new_args.push_back(ai);
}
for (unsigned j = 0; j < arity; j++) {
sort * ft_dj = dmn[j];
expr * bv_aj = bv_args[j];
ai = rebuild_floats(mc, ft_dj, to_app(bv_aj));
m_th_rw(ai);
new_args.push_back(ai);
}
expr_ref bv_fres(m), ft_fres(m);
bv_fres = bv_fe->get_result();
ft_fres = rebuild_floats(mc, rng, to_app(bv_fres));
m_th_rw(ft_fres);
result->insert_new_entry(new_args.c_ptr(), ft_fres);
}
expr_ref bv_fres(m), ft_fres(m);
bv_fres = bv_fe->get_result();
ft_fres = rebuild_floats(mc, rng, to_app(bv_fres));
m_th_rw(ft_fres);
result->insert_new_entry(new_args.c_ptr(), ft_fres);
}
app_ref bv_els(m);
expr_ref ft_els(m);
bv_els = (app*)bv_fi->get_else();
ft_els = rebuild_floats(mc, rng, bv_els);
m_th_rw(ft_els);
result->set_else(ft_els);
}
app_ref bv_els(m);
expr_ref ft_els(m);
bv_els = (app*)bv_fi->get_else();
ft_els = rebuild_floats(mc, rng, bv_els);
m_th_rw(ft_els);
result->set_else(ft_els);
}
return result;
return result;
}
void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen) {
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
it != m_const2bv.end();
it++)
{
func_decl * var = it->m_key;
app * val = to_app(it->m_value);
SASSERT(m_fpa_util.is_float(var->get_range()));
SASSERT(var->get_range()->get_num_parameters() == 2);
unsigned ebits = m_fpa_util.get_ebits(var->get_range());
unsigned sbits = m_fpa_util.get_sbits(var->get_range());
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
it != m_const2bv.end();
it++)
{
func_decl * var = it->m_key;
app * val = to_app(it->m_value);
SASSERT(m_fpa_util.is_float(var->get_range()));
SASSERT(var->get_range()->get_num_parameters() == 2);
unsigned ebits = m_fpa_util.get_ebits(var->get_range());
unsigned sbits = m_fpa_util.get_sbits(var->get_range());
app * a0 = to_app(val->get_arg(0));
app * a1 = to_app(val->get_arg(1));
app * a2 = to_app(val->get_arg(2));
app * a0 = to_app(val->get_arg(0));
app * a1 = to_app(val->get_arg(1));
app * a2 = to_app(val->get_arg(2));
expr_ref v0(m), v1(m), v2(m);
expr_ref v0(m), v1(m), v2(m);
#ifdef Z3DEBUG
v0 = mc->get_const_interp(a0->get_decl());
v1 = mc->get_const_interp(a1->get_decl());
v2 = mc->get_const_interp(a2->get_decl());
v0 = mc->get_const_interp(a0->get_decl());
v1 = mc->get_const_interp(a1->get_decl());
v2 = mc->get_const_interp(a2->get_decl());
#else
expr * bv = mc->get_const_interp(to_app(to_app(a0)->get_arg(0))->get_decl());
unsigned bv_sz = m_bv_util.get_bv_size(bv);
@ -332,220 +332,220 @@ void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model
if (!v1) v1 = m_bv_util.mk_numeral(0, ebits);
if (!v2) v2 = m_bv_util.mk_numeral(0, sbits-1);
expr_ref sgn(m), exp(m), sig(m);
m_th_rw(v0, sgn);
m_th_rw(v1, exp);
m_th_rw(v2, sig);
expr_ref sgn(m), exp(m), sig(m);
m_th_rw(v0, sgn);
m_th_rw(v1, exp);
m_th_rw(v2, sig);
SASSERT(val->is_app_of(m_fpa_util.get_family_id(), OP_FPA_FP));
SASSERT(val->is_app_of(m_fpa_util.get_family_id(), OP_FPA_FP));
#ifdef Z3DEBUG
SASSERT(to_app(val->get_arg(0))->get_decl()->get_arity() == 0);
SASSERT(to_app(val->get_arg(1))->get_decl()->get_arity() == 0);
SASSERT(to_app(val->get_arg(2))->get_decl()->get_arity() == 0);
seen.insert(to_app(val->get_arg(0))->get_decl());
seen.insert(to_app(val->get_arg(1))->get_decl());
seen.insert(to_app(val->get_arg(2))->get_decl());
SASSERT(to_app(val->get_arg(0))->get_decl()->get_arity() == 0);
SASSERT(to_app(val->get_arg(1))->get_decl()->get_arity() == 0);
SASSERT(to_app(val->get_arg(2))->get_decl()->get_arity() == 0);
seen.insert(to_app(val->get_arg(0))->get_decl());
seen.insert(to_app(val->get_arg(1))->get_decl());
seen.insert(to_app(val->get_arg(2))->get_decl());
#else
SASSERT(a->get_arg(0)->get_kind() == OP_EXTRACT);
SASSERT(to_app(a->get_arg(0))->get_arg(0)->get_kind() == OP_EXTRACT);
seen.insert(to_app(to_app(val->get_arg(0))->get_arg(0))->get_decl());
SASSERT(a->get_arg(0)->get_kind() == OP_EXTRACT);
SASSERT(to_app(a->get_arg(0))->get_arg(0)->get_kind() == OP_EXTRACT);
seen.insert(to_app(to_app(val->get_arg(0))->get_arg(0))->get_decl());
#endif
if (!sgn && !sig && !exp)
continue;
if (!sgn && !sig && !exp)
continue;
expr_ref cv(m);
cv = convert_bv2fp(var->get_range(), sgn, exp, sig);
target_model->register_decl(var, cv);
expr_ref cv(m);
cv = convert_bv2fp(var->get_range(), sgn, exp, sig);
target_model->register_decl(var, cv);
TRACE("bv2fpa", tout << var->get_name() << " == " << mk_ismt2_pp(cv, m) << std::endl;);
}
TRACE("bv2fpa", tout << var->get_name() << " == " << mk_ismt2_pp(cv, m) << std::endl;);
}
}
void bv2fpa_converter::convert_rm_consts(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen) {
for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
it != m_rm_const2bv.end();
it++)
{
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_bv2rm(val));
expr * bvval = to_app(val)->get_arg(0);
expr_ref fv(m);
fv = convert_bv2rm(mc, to_app(bvval));
TRACE("bv2fpa", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << ")" << std::endl;);
target_model->register_decl(var, fv);
seen.insert(to_app(bvval)->get_decl());
}
for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
it != m_rm_const2bv.end();
it++)
{
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_bv2rm(val));
expr * bvval = to_app(val)->get_arg(0);
expr_ref fv(m);
fv = convert_bv2rm(mc, to_app(bvval));
TRACE("bv2fpa", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << ")" << std::endl;);
target_model->register_decl(var, fv);
seen.insert(to_app(bvval)->get_decl());
}
}
void bv2fpa_converter::convert_min_max_specials(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen) {
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.end();
it++) {
func_decl * f = it->m_key;
app * pn_cnst = it->m_value.first;
app * np_cnst = it->m_value.second;
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.end();
it++) {
func_decl * f = it->m_key;
app * pn_cnst = it->m_value.first;
app * np_cnst = it->m_value.second;
expr_ref pzero(m), nzero(m);
pzero = m_fpa_util.mk_pzero(f->get_range());
nzero = m_fpa_util.mk_nzero(f->get_range());
expr_ref pzero(m), nzero(m);
pzero = m_fpa_util.mk_pzero(f->get_range());
nzero = m_fpa_util.mk_nzero(f->get_range());
expr_ref pn(m), np(m);
if (!mc->eval(pn_cnst->get_decl(), pn)) pn = pzero;
if (!mc->eval(np_cnst->get_decl(), np)) np = pzero;
seen.insert(pn_cnst->get_decl());
seen.insert(np_cnst->get_decl());
expr_ref pn(m), np(m);
if (!mc->eval(pn_cnst->get_decl(), pn)) pn = pzero;
if (!mc->eval(np_cnst->get_decl(), np)) np = pzero;
seen.insert(pn_cnst->get_decl());
seen.insert(np_cnst->get_decl());
rational pn_num, np_num;
unsigned bv_sz;
m_bv_util.is_numeral(pn, pn_num, bv_sz);
m_bv_util.is_numeral(np, np_num, bv_sz);
rational pn_num, np_num;
unsigned bv_sz;
m_bv_util.is_numeral(pn, pn_num, bv_sz);
m_bv_util.is_numeral(np, np_num, bv_sz);
func_interp * flt_fi = alloc(func_interp, m, f->get_arity());
expr * pn_args[2] = { pzero, nzero };
if (pn != np) flt_fi->insert_new_entry(pn_args, (pn_num.is_one() ? nzero : pzero));
flt_fi->set_else(np_num.is_one() ? nzero : pzero);
func_interp * flt_fi = alloc(func_interp, m, f->get_arity());
expr * pn_args[2] = { pzero, nzero };
if (pn != np) flt_fi->insert_new_entry(pn_args, (pn_num.is_one() ? nzero : pzero));
flt_fi->set_else(np_num.is_one() ? nzero : pzero);
target_model->register_decl(f, flt_fi);
TRACE("bv2fpa", tout << "fp.min/fp.max special: " << std::endl <<
mk_ismt2_pp(f, m) << " == " << mk_ismt2_pp(flt_fi->get_interp(), m) << std::endl;);
}
target_model->register_decl(f, flt_fi);
TRACE("bv2fpa", tout << "fp.min/fp.max special: " << std::endl <<
mk_ismt2_pp(f, m) << " == " << mk_ismt2_pp(flt_fi->get_interp(), m) << std::endl;);
}
}
void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen) {
for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
it != m_uf2bvuf.end();
it++) {
seen.insert(it->m_value);
for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
it != m_uf2bvuf.end();
it++) {
seen.insert(it->m_value);
func_decl * f = it->m_key;
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, it->m_value);
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);
}
else {
// Just keep.
SASSERT(!m_fpa_util.is_float(f->get_range()) && !m_fpa_util.is_rm(f->get_range()));
expr_ref var(m), val(m);
if (mc->eval(it->m_value, val))
target_model->register_decl(f, val);
}
}
else {
func_interp * fmv = convert_func_interp(mc, f, it->m_value);
if (fmv) target_model->register_decl(f, fmv);
}
}
func_decl * f = it->m_key;
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, it->m_value);
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);
}
else {
// Just keep.
SASSERT(!m_fpa_util.is_float(f->get_range()) && !m_fpa_util.is_rm(f->get_range()));
expr_ref var(m), val(m);
if (mc->eval(it->m_value, val))
target_model->register_decl(f, val);
}
}
else {
func_interp * fmv = convert_func_interp(mc, f, it->m_value);
if (fmv) target_model->register_decl(f, fmv);
}
}
}
void bv2fpa_converter::display(std::ostream & out) {
out << "(fpa2bv-model-converter";
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
it != m_const2bv.end();
it++) {
const symbol & n = it->m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value, m, indent) << ")";
}
for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
it != m_rm_const2bv.end();
it++) {
const symbol & n = it->m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value, m, indent) << ")";
}
for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
it != m_uf2bvuf.end();
it++) {
const symbol & n = it->m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value, m, indent) << ")";
}
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.end();
it++) {
const symbol & n = it->m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value.first, m, indent) << "; " <<
mk_ismt2_pp(it->m_value.second, m, indent) << ")";
}
out << ")";
out << "(fpa2bv-model-converter";
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
it != m_const2bv.end();
it++) {
const symbol & n = it->m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value, m, indent) << ")";
}
for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
it != m_rm_const2bv.end();
it++) {
const symbol & n = it->m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value, m, indent) << ")";
}
for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
it != m_uf2bvuf.end();
it++) {
const symbol & n = it->m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value, m, indent) << ")";
}
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.end();
it++) {
const symbol & n = it->m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value.first, m, indent) << "; " <<
mk_ismt2_pp(it->m_value.second, m, indent) << ")";
}
out << ")";
}
bv2fpa_converter * bv2fpa_converter::translate(ast_translation & translator) {
bv2fpa_converter * res = alloc(bv2fpa_converter, translator.to());
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
it != m_const2bv.end();
it++)
{
func_decl * k = translator(it->m_key);
expr * v = translator(it->m_value);
res->m_const2bv.insert(k, v);
translator.to().inc_ref(k);
translator.to().inc_ref(v);
}
for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
it != m_rm_const2bv.end();
it++)
{
func_decl * k = translator(it->m_key);
expr * v = translator(it->m_value);
res->m_rm_const2bv.insert(k, v);
translator.to().inc_ref(k);
translator.to().inc_ref(v);
}
for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
it != m_uf2bvuf.end();
it++) {
func_decl * k = translator(it->m_key);
func_decl * v = translator(it->m_value);
res->m_uf2bvuf.insert(k, v);
translator.to().inc_ref(k);
translator.to().inc_ref(v);
}
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.end();
it++) {
func_decl * k = translator(it->m_key);
app * v1 = translator(it->m_value.first);
app * v2 = translator(it->m_value.second);
res->m_specials.insert(k, std::pair<app*, app*>(v1, v2));
translator.to().inc_ref(k);
translator.to().inc_ref(v1);
translator.to().inc_ref(v2);
}
return res;
bv2fpa_converter * res = alloc(bv2fpa_converter, translator.to());
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
it != m_const2bv.end();
it++)
{
func_decl * k = translator(it->m_key);
expr * v = translator(it->m_value);
res->m_const2bv.insert(k, v);
translator.to().inc_ref(k);
translator.to().inc_ref(v);
}
for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
it != m_rm_const2bv.end();
it++)
{
func_decl * k = translator(it->m_key);
expr * v = translator(it->m_value);
res->m_rm_const2bv.insert(k, v);
translator.to().inc_ref(k);
translator.to().inc_ref(v);
}
for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
it != m_uf2bvuf.end();
it++) {
func_decl * k = translator(it->m_key);
func_decl * v = translator(it->m_value);
res->m_uf2bvuf.insert(k, v);
translator.to().inc_ref(k);
translator.to().inc_ref(v);
}
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.end();
it++) {
func_decl * k = translator(it->m_key);
app * v1 = translator(it->m_value.first);
app * v2 = translator(it->m_value.second);
res->m_specials.insert(k, std::pair<app*, app*>(v1, v2));
translator.to().inc_ref(k);
translator.to().inc_ref(v1);
translator.to().inc_ref(v2);
}
return res;
}
void bv2fpa_converter::convert(model_core * mc, model_core * float_mdl) {
TRACE("bv2fpa", tout << "BV Model: " << std::endl;
for (unsigned i = 0; i < mc->get_num_constants(); i++)
tout << mc->get_constant(i)->get_name() << " --> " <<
mk_ismt2_pp(mc->get_const_interp(mc->get_constant(i)), m) << std::endl;
for (unsigned i = 0; i < mc->get_num_functions(); i++) {
func_decl * f = mc->get_function(i);
tout << f->get_name() << "(...) := " << std::endl;
func_interp * fi = mc->get_func_interp(f);
for (unsigned j = 0; j < fi->num_entries(); j++) {
func_entry const * fe = fi->get_entry(j);
for (unsigned k = 0; k < f->get_arity(); k++) {
tout << mk_ismt2_pp(fe->get_arg(k), m) << " ";
}
tout << "--> " << mk_ismt2_pp(fe->get_result(), m) << std::endl;
}
tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl;
});
TRACE("bv2fpa", tout << "BV Model: " << std::endl;
for (unsigned i = 0; i < mc->get_num_constants(); i++)
tout << mc->get_constant(i)->get_name() << " --> " <<
mk_ismt2_pp(mc->get_const_interp(mc->get_constant(i)), m) << std::endl;
for (unsigned i = 0; i < mc->get_num_functions(); i++) {
func_decl * f = mc->get_function(i);
tout << f->get_name() << "(...) := " << std::endl;
func_interp * fi = mc->get_func_interp(f);
for (unsigned j = 0; j < fi->num_entries(); j++) {
func_entry const * fe = fi->get_entry(j);
for (unsigned k = 0; k < f->get_arity(); k++) {
tout << mk_ismt2_pp(fe->get_arg(k), m) << " ";
}
tout << "--> " << mk_ismt2_pp(fe->get_result(), m) << std::endl;
}
tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl;
});
}

74
src/ast/fpa/bv2fpa_converter.h
View file

@ -1,17 +1,17 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Copyright (c) 2016 Microsoft Corporation
Module Name:
bv2fpa_converter.h
bv2fpa_converter.h
Abstract:
Model conversion for fpa2bv_converter
Model conversion for fpa2bv_converter
Author:
Christoph (cwinter) 2016-10-15
Christoph (cwinter) 2016-10-15
Notes:
@ -27,48 +27,48 @@ Notes:
class bv2fpa_converter {
ast_manager & m;
fpa_util m_fpa_util;
bv_util m_bv_util;
th_rewriter m_th_rw;
ast_manager & m;
fpa_util m_fpa_util;
bv_util m_bv_util;
th_rewriter m_th_rw;
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<app*, app*> > m_specials;
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<app*, app*> > m_specials;
public:
bv2fpa_converter(ast_manager & m);
bv2fpa_converter(ast_manager & m, fpa2bv_converter & conv);
virtual ~bv2fpa_converter();
bv2fpa_converter(ast_manager & m);
bv2fpa_converter(ast_manager & m, fpa2bv_converter & conv);
virtual ~bv2fpa_converter();
void display(std::ostream & out);
bv2fpa_converter * translate(ast_translation & translator);
void display(std::ostream & out);
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_bv2rm(expr * eval_v);
expr_ref convert_bv2rm(model_core * mc, app * val);
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_bv2rm(expr * eval_v);
expr_ref convert_bv2rm(model_core * mc, app * val);
void convert(model_core * mc, model_core * float_mdl);
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);
void convert_min_max_specials(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen);
void convert_uf2bvuf(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen);
void convert(model_core * mc, model_core * float_mdl);
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);
void convert_min_max_specials(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen);
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);
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);
class array_model {
public:
func_decl * new_float_fd;
func_interp * new_float_fi;
func_decl * bv_fd;
expr_ref result;
array_model(ast_manager & m) : new_float_fd(0), new_float_fi(0), bv_fd(0), result(m) {}
};
class array_model {
public:
func_decl * new_float_fd;
func_interp * new_float_fi;
func_decl * bv_fd;
expr_ref result;
array_model(ast_manager & m) : new_float_fd(0), new_float_fi(0), bv_fd(0), result(m) {}
};
array_model convert_array_func_interp(model_core * mc, func_decl * f, func_decl * bv_f);
array_model convert_array_func_interp(model_core * mc, func_decl * f, func_decl * bv_f);
};
#endif

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

@ -3074,9 +3074,9 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2),
m_bv_util.mk_numeral(1, 1))));
else {
app_ref unspec(m);
unspec = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits);
mk_to_ieee_bv_unspecified(unspec->get_decl(), 0, 0, nanv);
app_ref unspec(m);
unspec = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits);
mk_to_ieee_bv_unspecified(unspec->get_decl(), 0, 0, nanv);
}
expr_ref sgn_e_s(m);
@ -3126,42 +3126,42 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex
}
void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result) {
TRACE("fpa2bv_to_bv", for (unsigned i = 0; i < num; i++)
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
TRACE("fpa2bv_to_bv", for (unsigned i = 0; i < num; i++)
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
SASSERT(num == 2);
SASSERT(m_util.is_bv2rm(args[0]));
SASSERT(m_util.is_float(args[1]));
SASSERT(num == 2);
SASSERT(m_util.is_bv2rm(args[0]));
SASSERT(m_util.is_float(args[1]));
expr * rm = to_app(args[0])->get_arg(0);
expr * x = args[1];
sort * xs = m.get_sort(x);
sort * bv_srt = f->get_range();
expr * rm = to_app(args[0])->get_arg(0);
expr * x = args[1];
sort * xs = m.get_sort(x);
sort * bv_srt = f->get_range();
unsigned ebits = m_util.get_ebits(xs);
unsigned sbits = m_util.get_sbits(xs);
unsigned bv_sz = (unsigned)f->get_parameter(0).get_int();
unsigned ebits = m_util.get_ebits(xs);
unsigned sbits = m_util.get_sbits(xs);
unsigned bv_sz = (unsigned)f->get_parameter(0).get_int();
expr_ref bv0(m), bv1(m);
bv1 = m_bv_util.mk_numeral(1, 1);
expr_ref bv0(m), bv1(m);
bv1 = m_bv_util.mk_numeral(1, 1);
expr_ref x_is_nan(m), x_is_inf(m), x_is_zero(m), x_is_neg(m), x_is_nzero(m);
mk_is_nan(x, x_is_nan);
mk_is_inf(x, x_is_inf);
mk_is_zero(x, x_is_zero);
mk_is_neg(x, x_is_neg);
mk_is_nzero(x, x_is_nzero);
expr_ref x_is_nan(m), x_is_inf(m), x_is_zero(m), x_is_neg(m), x_is_nzero(m);
mk_is_nan(x, x_is_nan);
mk_is_inf(x, x_is_inf);
mk_is_zero(x, x_is_zero);
mk_is_neg(x, x_is_neg);
mk_is_nzero(x, x_is_nzero);
// NaN, Inf, or negative (except -0) -> unspecified
expr_ref c1(m), v1(m);
if (!is_signed) {
c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero)));
v1 = mk_to_ubv_unspecified(ebits, sbits, bv_sz);
}
else {
c1 = m.mk_or(x_is_nan, x_is_inf);
v1 = mk_to_sbv_unspecified(ebits, sbits, bv_sz);
}
// NaN, Inf, or negative (except -0) -> unspecified
expr_ref c1(m), v1(m);
if (!is_signed) {
c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero)));
v1 = mk_to_ubv_unspecified(ebits, sbits, bv_sz);
}
else {
c1 = m.mk_or(x_is_nan, x_is_inf);
v1 = mk_to_sbv_unspecified(ebits, sbits, bv_sz);
}
dbg_decouple("fpa2bv_to_bv_c1", c1);
// +-Zero -> 0
@ -3272,7 +3272,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
expr_ref unspec(m);
unspec = is_signed ? mk_to_sbv_unspecified(ebits, sbits, bv_sz) :
mk_to_ubv_unspecified(ebits, sbits, bv_sz);
mk_to_ubv_unspecified(ebits, sbits, bv_sz);
result = m.mk_ite(rnd_has_overflown, unspec, rnd);
result = m.mk_ite(c_in_limits, result, unspec);
result = m.mk_ite(c2, v2, result);
@ -3294,61 +3294,61 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
}
void fpa2bv_converter::mk_to_ubv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 0);
unsigned width = m_bv_util.get_bv_size(f->get_range());
SASSERT(num == 0);
unsigned width = m_bv_util.get_bv_size(f->get_range());
if (m_hi_fp_unspecified)
result = m_bv_util.mk_numeral(0, width);
else {
func_decl * fd;
if (!m_uf2bvuf.find(f, fd)) {
fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range());
m_uf2bvuf.insert(f, fd);
m.inc_ref(f);
m.inc_ref(fd);
}
result = m.mk_const(fd);
}
if (m_hi_fp_unspecified)
result = m_bv_util.mk_numeral(0, width);
else {
func_decl * fd;
if (!m_uf2bvuf.find(f, fd)) {
fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range());
m_uf2bvuf.insert(f, fd);
m.inc_ref(f);
m.inc_ref(fd);
}
result = m.mk_const(fd);
}
TRACE("fpa2bv_to_ubv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
SASSERT(is_well_sorted(m, result));
TRACE("fpa2bv_to_ubv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
SASSERT(is_well_sorted(m, result));
}
expr_ref fpa2bv_converter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width) {
expr_ref res(m);
app_ref u(m);
u = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width);
mk_to_sbv_unspecified(u->get_decl(), 0, 0, res);
return res;
expr_ref res(m);
app_ref u(m);
u = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width);
mk_to_sbv_unspecified(u->get_decl(), 0, 0, res);
return res;
}
void fpa2bv_converter::mk_to_sbv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 0);
unsigned width = m_bv_util.get_bv_size(f->get_range());
SASSERT(num == 0);
unsigned width = m_bv_util.get_bv_size(f->get_range());
if (m_hi_fp_unspecified)
result = m_bv_util.mk_numeral(0, width);
else {
func_decl * fd;
if (!m_uf2bvuf.find(f, fd)) {
fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range());
m_uf2bvuf.insert(f, fd);
m.inc_ref(f);
m.inc_ref(fd);
}
result = m.mk_const(fd);
}
if (m_hi_fp_unspecified)
result = m_bv_util.mk_numeral(0, width);
else {
func_decl * fd;
if (!m_uf2bvuf.find(f, fd)) {
fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range());
m_uf2bvuf.insert(f, fd);
m.inc_ref(f);
m.inc_ref(fd);
}
result = m.mk_const(fd);
}
TRACE("fpa2bv_to_sbv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
SASSERT(is_well_sorted(m, result));
TRACE("fpa2bv_to_sbv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
SASSERT(is_well_sorted(m, result));
}
expr_ref fpa2bv_converter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width) {
expr_ref res(m);
app_ref u(m);
u = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width);
mk_to_sbv_unspecified(u->get_decl(), 0, 0, res);
return res;
expr_ref res(m);
app_ref u(m);
u = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width);
mk_to_sbv_unspecified(u->get_decl(), 0, 0, res);
return res;
}
void fpa2bv_converter::mk_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
@ -3367,11 +3367,11 @@ void fpa2bv_converter::mk_to_real_unspecified(func_decl * f, unsigned num, expr
}
expr_ref fpa2bv_converter::mk_to_real_unspecified(unsigned ebits, unsigned sbits) {
expr_ref res(m);
app_ref u(m);
u = m_util.mk_internal_to_real_unspecified(ebits, sbits);
mk_to_real_unspecified(u->get_decl(), 0, 0, res);
return res;
expr_ref res(m);
app_ref u(m);
u = m_util.mk_internal_to_real_unspecified(ebits, sbits);
mk_to_real_unspecified(u->get_decl(), 0, 0, res);
return res;
}
void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {