mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
commit
4fda2adec8
|
@ -45,7 +45,7 @@ def init_project_def():
|
|||
# Simplifier module will be deleted in the future.
|
||||
# It has been replaced with rewriter module.
|
||||
add_lib('simplifier', ['rewriter'], 'ast/simplifier')
|
||||
add_lib('fpa', ['ast', 'util', 'simplifier'], 'ast/fpa')
|
||||
add_lib('fpa', ['ast', 'util', 'simplifier', 'model'], 'ast/fpa')
|
||||
add_lib('macros', ['simplifier'], 'ast/macros')
|
||||
add_lib('pattern', ['normal_forms', 'smt2parser', 'simplifier'], 'ast/pattern')
|
||||
add_lib('bit_blaster', ['rewriter', 'simplifier'], 'ast/rewriter/bit_blaster')
|
||||
|
|
543
src/ast/fpa/bv2fpa_converter.cpp
Normal file
543
src/ast/fpa/bv2fpa_converter.cpp
Normal file
|
@ -0,0 +1,543 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
bv2fpa_converter.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Model conversion for fpa2bv_converter
|
||||
|
||||
Author:
|
||||
|
||||
Christoph (cwinter) 2016-10-15
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#include<math.h>
|
||||
|
||||
#include"ast_smt2_pp.h"
|
||||
#include"well_sorted.h"
|
||||
#include"th_rewriter.h"
|
||||
#include"fpa_rewriter.h"
|
||||
|
||||
#include"bv2fpa_converter.h"
|
||||
|
||||
|
||||
bv2fpa_converter::bv2fpa_converter(ast_manager & 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);
|
||||
}
|
||||
}
|
||||
|
||||
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);
|
||||
}
|
||||
}
|
||||
|
||||
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();
|
||||
|
||||
expr_ref res(m);
|
||||
mpf fp_val;
|
||||
|
||||
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;
|
||||
|
||||
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);
|
||||
|
||||
// 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());
|
||||
|
||||
m_fpa_util.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), exp_z, sig_z);
|
||||
|
||||
mpzm.del(sig_z);
|
||||
|
||||
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);
|
||||
|
||||
return res;
|
||||
}
|
||||
|
||||
expr_ref bv2fpa_converter::convert_bv2fp(model_core * mc, sort * s, app * 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 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);
|
||||
|
||||
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;
|
||||
|
||||
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;
|
||||
}
|
||||
|
||||
expr_ref bv2fpa_converter::convert_bv2rm(model_core * mc, app * 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))
|
||||
res = convert_bv2rm(eval_v);
|
||||
else
|
||||
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 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());
|
||||
}
|
||||
|
||||
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);
|
||||
|
||||
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());
|
||||
|
||||
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;
|
||||
}
|
||||
|
||||
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();
|
||||
|
||||
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);
|
||||
|
||||
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);
|
||||
}
|
||||
|
||||
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);
|
||||
}
|
||||
|
||||
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());
|
||||
|
||||
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);
|
||||
v0 = mc->get_const_interp(a0->get_decl());
|
||||
v1 = mc->get_const_interp(a1->get_decl());
|
||||
v2 = mc->get_const_interp(a2->get_decl());
|
||||
|
||||
if (!v0) v0 = m_bv_util.mk_numeral(0, 1);
|
||||
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);
|
||||
|
||||
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());
|
||||
#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());
|
||||
#endif
|
||||
|
||||
if (!sgn && !sig && !exp)
|
||||
continue;
|
||||
|
||||
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;);
|
||||
}
|
||||
}
|
||||
|
||||
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());
|
||||
}
|
||||
}
|
||||
|
||||
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;
|
||||
|
||||
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());
|
||||
|
||||
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);
|
||||
|
||||
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);
|
||||
|
||||
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 << ")";
|
||||
}
|
||||
|
||||
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;
|
||||
}
|
||||
|
||||
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;
|
||||
});
|
||||
|
||||
}
|
74
src/ast/fpa/bv2fpa_converter.h
Normal file
74
src/ast/fpa/bv2fpa_converter.h
Normal file
|
@ -0,0 +1,74 @@
|
|||
/*++
|
||||
Copyright (c) 2016 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
bv2fpa_converter.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Model conversion for fpa2bv_converter
|
||||
|
||||
Author:
|
||||
|
||||
Christoph (cwinter) 2016-10-15
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef BV2FPA_CONVERTER_H_
|
||||
#define BV2FPA_CONVERTER_H_
|
||||
|
||||
#include"fpa_decl_plugin.h"
|
||||
#include"bv_decl_plugin.h"
|
||||
#include"th_rewriter.h"
|
||||
#include"model_core.h"
|
||||
#include"fpa2bv_converter.h"
|
||||
|
||||
|
||||
class bv2fpa_converter {
|
||||
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;
|
||||
|
||||
public:
|
||||
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);
|
||||
|
||||
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);
|
||||
|
||||
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) {}
|
||||
};
|
||||
|
||||
array_model convert_array_func_interp(model_core * mc, func_decl * f, func_decl * bv_f);
|
||||
};
|
||||
|
||||
#endif
|
|
@ -23,6 +23,7 @@ Notes:
|
|||
#include"th_rewriter.h"
|
||||
|
||||
#include"fpa2bv_converter.h"
|
||||
#include"fpa_rewriter.h"
|
||||
|
||||
#define BVULT(X,Y,R) { expr_ref bvult_eq(m), bvult_not(m); m_simp.mk_eq(X, Y, bvult_eq); m_simp.mk_not(bvult_eq, bvult_not); expr_ref t(m); t = m_bv_util.mk_ule(X,Y); m_simp.mk_and(t, bvult_not, R); }
|
||||
|
||||
|
@ -32,7 +33,6 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
|
|||
m_util(m),
|
||||
m_bv_util(m),
|
||||
m_arith_util(m),
|
||||
m_array_util(m),
|
||||
m_dt_util(m),
|
||||
m_seq_util(m),
|
||||
m_mpf_manager(m_util.fm()),
|
||||
|
@ -165,7 +165,6 @@ void fpa2bv_converter::mk_numeral(sort * s, mpf const & v, expr_ref & result) {
|
|||
result = m_util.mk_fp(bv_sgn, biased_exp, bv_sig);
|
||||
TRACE("fpa2bv_dbg", tout << "value of [" << sign << " " << m_mpz_manager.to_string(sig) << " " << exp << "] is "
|
||||
<< mk_ismt2_pp(result, m) << std::endl;);
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -2772,6 +2771,7 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
|
|||
|
||||
expr_ref unspec(m);
|
||||
unspec = mk_to_real_unspecified(ebits, sbits);
|
||||
|
||||
result = m.mk_ite(x_is_zero, zero, res);
|
||||
result = m.mk_ite(x_is_inf, unspec, result);
|
||||
result = m.mk_ite(x_is_nan, unspec, result);
|
||||
|
@ -3073,50 +3073,95 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
|
|||
m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits),
|
||||
m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2),
|
||||
m_bv_util.mk_numeral(1, 1))));
|
||||
else
|
||||
nanv = mk_to_ieee_bv_unspecified(ebits, sbits);
|
||||
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);
|
||||
}
|
||||
|
||||
expr_ref sgn_e_s(m);
|
||||
sgn_e_s = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s);
|
||||
m_simp.mk_ite(x_is_nan, nanv, sgn_e_s, result);
|
||||
|
||||
TRACE("fpa2bv_to_ieee_bv", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
|
||||
SASSERT(is_well_sorted(m, result));
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
SASSERT(num == 0);
|
||||
unsigned ebits = f->get_parameter(0).get_int();
|
||||
unsigned sbits = f->get_parameter(1).get_int();
|
||||
|
||||
if (m_hi_fp_unspecified) {
|
||||
result = m_bv_util.mk_concat(m_bv_util.mk_concat(
|
||||
m_bv_util.mk_numeral(0, 1),
|
||||
m_bv_util.mk_numeral(-1, ebits)),
|
||||
m_bv_util.mk_numeral(1, sbits-1));
|
||||
}
|
||||
else {
|
||||
func_decl * fd;
|
||||
if (m_uf2bvuf.find(f, fd))
|
||||
result = m.mk_const(fd);
|
||||
else {
|
||||
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);
|
||||
|
||||
expr_ref exp_bv(m), exp_all_ones(m);
|
||||
exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result);
|
||||
exp_all_ones = m.mk_eq(exp_bv, m_bv_util.mk_numeral(-1, ebits));
|
||||
m_extra_assertions.push_back(exp_all_ones);
|
||||
|
||||
expr_ref sig_bv(m), sig_is_non_zero(m);
|
||||
sig_bv = m_bv_util.mk_extract(sbits-2, 0, result);
|
||||
sig_is_non_zero = m.mk_not(m.mk_eq(sig_bv, m_bv_util.mk_numeral(0, sbits-1)));
|
||||
m_extra_assertions.push_back(sig_is_non_zero);
|
||||
}
|
||||
}
|
||||
|
||||
TRACE("fpa2bv_to_ieee_bv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
|
||||
SASSERT(is_well_sorted(m, result));
|
||||
}
|
||||
|
||||
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)));
|
||||
else
|
||||
c1 = m.mk_or(x_is_nan, x_is_inf);
|
||||
v1 = mk_to_ubv_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
|
||||
|
@ -3226,7 +3271,8 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
|
|||
dbg_decouple("fpa2bv_to_bv_rnd", rnd);
|
||||
|
||||
expr_ref unspec(m);
|
||||
unspec = mk_to_ubv_unspecified(ebits, sbits, bv_sz);
|
||||
unspec = is_signed ? mk_to_sbv_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);
|
||||
|
@ -3247,101 +3293,89 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
|
|||
mk_to_bv(f, num, args, true, result);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_to_ubv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
SASSERT(num == 0);
|
||||
unsigned ebits = f->get_parameter(0).get_int();
|
||||
unsigned sbits = f->get_parameter(1).get_int();
|
||||
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);
|
||||
}
|
||||
|
||||
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 result(m);
|
||||
if (m_hi_fp_unspecified)
|
||||
result = m_bv_util.mk_numeral(0, width);
|
||||
else {
|
||||
app_ref unspec(m);
|
||||
unspec = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width);
|
||||
func_decl * unspec_fd = unspec->get_decl();
|
||||
func_decl * fd;
|
||||
if (!m_uf2bvuf.find(unspec_fd, fd)) {
|
||||
app_ref bvc(m);
|
||||
bvc = m.mk_fresh_const(0, unspec_fd->get_range());
|
||||
fd = bvc->get_decl();
|
||||
m_uf2bvuf.insert(unspec_fd, fd);
|
||||
m.inc_ref(unspec_fd);
|
||||
m.inc_ref(fd);
|
||||
}
|
||||
result = m.mk_const(fd);
|
||||
}
|
||||
return result;
|
||||
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 ebits = f->get_parameter(0).get_int();
|
||||
unsigned sbits = f->get_parameter(1).get_int();
|
||||
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);
|
||||
}
|
||||
|
||||
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 result(m);
|
||||
if (m_hi_fp_unspecified)
|
||||
result = m_bv_util.mk_numeral(0, width);
|
||||
else {
|
||||
app_ref unspec(m);
|
||||
unspec = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width);
|
||||
func_decl * unspec_fd = unspec->get_decl();
|
||||
func_decl * fd;
|
||||
if (!m_uf2bvuf.find(unspec_fd, fd)) {
|
||||
app_ref bvc(m);
|
||||
bvc = m.mk_fresh_const(0, unspec_fd->get_range());
|
||||
fd = bvc->get_decl();
|
||||
m_uf2bvuf.insert(unspec_fd, fd);
|
||||
m.inc_ref(unspec_fd);
|
||||
m.inc_ref(fd);
|
||||
}
|
||||
result = m.mk_const(fd);
|
||||
}
|
||||
return result;
|
||||
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 fpa2bv_converter::mk_to_real_unspecified(unsigned ebits, unsigned sbits) {
|
||||
expr_ref result(m);
|
||||
void fpa2bv_converter::mk_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
if (m_hi_fp_unspecified)
|
||||
result = m_arith_util.mk_numeral(rational(0), false);
|
||||
else {
|
||||
app_ref unspec(m);
|
||||
unspec = m_util.mk_internal_to_real_unspecified(ebits, sbits);
|
||||
func_decl * unspec_fd = unspec->get_decl();
|
||||
func_decl * fd;
|
||||
if (!m_uf2bvuf.find(unspec_fd, fd)) {
|
||||
app_ref bvc(m);
|
||||
bvc = m.mk_fresh_const(0, unspec_fd->get_range());
|
||||
fd = bvc->get_decl();
|
||||
m_uf2bvuf.insert(unspec_fd, fd);
|
||||
m.inc_ref(unspec_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);
|
||||
result = unspec;
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
expr_ref fpa2bv_converter::mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits) {
|
||||
expr_ref result(m);
|
||||
|
||||
app_ref unspec(m);
|
||||
unspec = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits);
|
||||
func_decl * unspec_fd = unspec->get_decl();
|
||||
func_decl * fd;
|
||||
if (!m_uf2bvuf.find(unspec_fd, fd)) {
|
||||
app_ref bvc(m);
|
||||
bvc = m.mk_fresh_const(0, unspec_fd->get_range());
|
||||
fd = bvc->get_decl();
|
||||
m_uf2bvuf.insert(unspec_fd, fd);
|
||||
m.inc_ref(unspec_fd);
|
||||
m.inc_ref(fd);
|
||||
}
|
||||
result = m.mk_const(fd);
|
||||
|
||||
app_ref mask(m), extra(m), result_and_mask(m);
|
||||
mask = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 1),
|
||||
m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits),
|
||||
m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2),
|
||||
m_bv_util.mk_numeral(1, 1))));
|
||||
expr * args[2] = { result, mask };
|
||||
result_and_mask = m.mk_app(m_bv_util.get_fid(), OP_BAND, 2, args);
|
||||
extra = m.mk_eq(result_and_mask, mask);
|
||||
m_extra_assertions.push_back(extra);
|
||||
|
||||
return result;
|
||||
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;
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
|
|
|
@ -43,7 +43,6 @@ protected:
|
|||
fpa_util m_util;
|
||||
bv_util m_bv_util;
|
||||
arith_util m_arith_util;
|
||||
array_util m_array_util;
|
||||
datatype_util m_dt_util;
|
||||
seq_util m_seq_util;
|
||||
mpf_manager & m_mpf_manager;
|
||||
|
@ -57,6 +56,7 @@ protected:
|
|||
special_t m_min_max_specials;
|
||||
|
||||
friend class fpa2bv_model_converter;
|
||||
friend class bv2fpa_converter;
|
||||
|
||||
public:
|
||||
fpa2bv_converter(ast_manager & m);
|
||||
|
@ -71,9 +71,9 @@ public:
|
|||
bool is_rm(expr * e) { return is_app(e) && m_util.is_rm(e); }
|
||||
bool is_rm(sort * s) { return m_util.is_rm(s); }
|
||||
bool is_float_family(func_decl * f) { return f->get_family_id() == m_util.get_family_id(); }
|
||||
|
||||
|
||||
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_ref & sgn, expr_ref & exp, expr_ref & sig) const;
|
||||
|
||||
|
@ -133,12 +133,16 @@ public:
|
|||
void mk_to_fp_signed(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result);
|
||||
void mk_to_fp_real_int(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
|
||||
void mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_to_ubv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_to_sbv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
|
||||
void set_unspecified_fp_hi(bool v) { m_hi_fp_unspecified = v; }
|
||||
|
||||
|
@ -149,16 +153,11 @@ public:
|
|||
void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
|
||||
expr_ref mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
|
||||
expr_ref mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
|
||||
expr_ref mk_to_real_unspecified(unsigned ebits, unsigned sbits);
|
||||
expr_ref mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits);
|
||||
|
||||
void reset(void);
|
||||
|
||||
void dbg_decouple(const char * prefix, expr_ref & e);
|
||||
expr_ref_vector m_extra_assertions;
|
||||
|
||||
|
||||
special_t const & get_min_max_specials() const { return m_min_max_specials; };
|
||||
const2bv_t const & get_const2bv() const { return m_const2bv; };
|
||||
const2bv_t const & get_rm_const2bv() const { return m_rm_const2bv; };
|
||||
|
@ -227,6 +226,10 @@ private:
|
|||
void mk_round_to_integral(sort * s, expr_ref & rm, expr_ref & x, expr_ref & result);
|
||||
|
||||
void mk_to_fp_float(sort * s, expr * rm, expr * x, expr_ref & result);
|
||||
|
||||
expr_ref mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
|
||||
expr_ref mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
|
||||
expr_ref mk_to_real_unspecified(unsigned ebits, unsigned sbits);
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
@ -143,9 +143,13 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
|
|||
case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: m_conv.mk_to_ubv_unspecified(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: m_conv.mk_to_sbv_unspecified(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: m_conv.mk_to_real_unspecified(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: m_conv.mk_to_ieee_bv_unspecified(f, num, args, result); return BR_DONE;
|
||||
|
||||
case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_REWRITE_FULL;
|
||||
case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_REWRITE_FULL;
|
||||
|
@ -157,12 +161,8 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
|
|||
|
||||
case OP_FPA_INTERNAL_BVWRAP:
|
||||
case OP_FPA_INTERNAL_BV2RM:
|
||||
|
||||
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
|
||||
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
|
||||
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
|
||||
case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED:
|
||||
return BR_FAILED;
|
||||
|
||||
default:
|
||||
TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";
|
||||
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
|
||||
|
|
|
@ -665,14 +665,14 @@ func_decl * fpa_decl_plugin::mk_to_real(decl_kind k, unsigned num_parameters, pa
|
|||
func_decl * fpa_decl_plugin::mk_to_ieee_bv(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 to_ieee_bv");
|
||||
m_manager->raise_exception("invalid number of arguments to fp.to_ieee_bv");
|
||||
if (!is_float_sort(domain[0]))
|
||||
m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort");
|
||||
|
||||
unsigned float_sz = domain[0]->get_parameter(0).get_int() + domain[0]->get_parameter(1).get_int();
|
||||
parameter ps[] = { parameter(float_sz) };
|
||||
sort * bv_srt = m_bv_plugin->mk_sort(BV_SORT, 1, ps);
|
||||
symbol name("to_ieee_bv");
|
||||
symbol name("fp.to_ieee_bv");
|
||||
return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k));
|
||||
}
|
||||
|
||||
|
@ -758,15 +758,15 @@ func_decl * fpa_decl_plugin::mk_internal_to_ieee_bv_unspecified(
|
|||
decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range) {
|
||||
if (arity != 0)
|
||||
m_manager->raise_exception("invalid number of arguments to to_ieee_bv_unspecified; expecting none");
|
||||
m_manager->raise_exception("invalid number of arguments to fp.to_ieee_bv_unspecified; expecting none");
|
||||
if (num_parameters != 2)
|
||||
m_manager->raise_exception("invalid number of parameters to to_ieee_bv_unspecified; expecting 2");
|
||||
m_manager->raise_exception("invalid number of parameters to fp.to_ieee_bv_unspecified; expecting 2");
|
||||
if (!parameters[0].is_int() || !parameters[1].is_int())
|
||||
m_manager->raise_exception("invalid parameters type provided to to_ieee_bv_unspecified; expecting 2 integers");
|
||||
m_manager->raise_exception("invalid parameters type provided to fp.to_ieee_bv_unspecified; expecting 2 integers");
|
||||
|
||||
parameter width_p[1] = { parameter(parameters[0].get_int() + parameters[1].get_int()) };
|
||||
sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, width_p);
|
||||
return m_manager->mk_func_decl(symbol("to_ieee_bv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
|
||||
return m_manager->mk_func_decl(symbol("fp.to_ieee_bv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
|
||||
}
|
||||
|
||||
|
||||
|
@ -915,7 +915,8 @@ void fpa_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
|
|||
op_names.push_back(builtin_name("to_fp_unsigned", OP_FPA_TO_FP_UNSIGNED));
|
||||
|
||||
/* Extensions */
|
||||
op_names.push_back(builtin_name("to_ieee_bv", OP_FPA_TO_IEEE_BV));
|
||||
op_names.push_back(builtin_name("to_ieee_bv", OP_FPA_TO_IEEE_BV));
|
||||
op_names.push_back(builtin_name("fp.to_ieee_bv", OP_FPA_TO_IEEE_BV));
|
||||
}
|
||||
|
||||
void fpa_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {
|
||||
|
|
|
@ -259,7 +259,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 * e) const { return is_app_of(e, m_fid, OP_FPA_FP); }
|
||||
unsigned get_ebits(sort * s) const;
|
||||
unsigned get_sbits(sort * s) const;
|
||||
|
||||
|
@ -294,13 +294,13 @@ public:
|
|||
bool is_pzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pzero(v); }
|
||||
bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nzero(v); }
|
||||
|
||||
app * mk_fp(expr * sgn, expr * exp, expr * sig) {
|
||||
app * mk_fp(expr * sgn, expr * exp, expr * sig) {
|
||||
SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1);
|
||||
SASSERT(m_bv_util.is_bv(exp));
|
||||
SASSERT(m_bv_util.is_bv(sig));
|
||||
return m().mk_app(m_fid, OP_FPA_FP, sgn, exp, sig);
|
||||
SASSERT(m_bv_util.is_bv(sig));
|
||||
return m().mk_app(m_fid, OP_FPA_FP, sgn, exp, sig);
|
||||
}
|
||||
|
||||
|
||||
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);
|
||||
|
@ -377,28 +377,28 @@ public:
|
|||
app * mk_internal_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits);
|
||||
app * mk_internal_to_real_unspecified(unsigned ebits, unsigned sbits);
|
||||
|
||||
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_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_bvwrap(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVWRAP); }
|
||||
bool is_bvwrap(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BVWRAP; }
|
||||
bool is_bv2rm(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BV2RM); }
|
||||
bool is_bv2rm(func_decl const * 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); }
|
||||
bool is_max_interpreted(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_I); }
|
||||
bool is_max_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED); }
|
||||
bool is_to_ubv_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED); }
|
||||
bool is_to_sbv_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED); }
|
||||
bool is_to_ieee_bv_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED); }
|
||||
bool is_to_real_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED); }
|
||||
bool is_min_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_I); }
|
||||
bool is_min_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED); }
|
||||
bool is_max_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_I); }
|
||||
bool is_max_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED); }
|
||||
bool is_to_ubv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED); }
|
||||
bool is_to_sbv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED); }
|
||||
bool is_to_ieee_bv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED); }
|
||||
bool is_to_real_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED); }
|
||||
|
||||
bool is_min_interpreted(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_I; }
|
||||
bool is_min_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_UNSPECIFIED; }
|
||||
bool is_max_interpreted(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_I; }
|
||||
bool is_max_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_UNSPECIFIED; }
|
||||
bool is_to_ubv_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED; }
|
||||
bool is_to_sbv_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED; }
|
||||
bool is_to_ieee_bv_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED; }
|
||||
bool is_to_real_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED; }
|
||||
bool is_min_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_I; }
|
||||
bool is_min_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_UNSPECIFIED; }
|
||||
bool is_max_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_I; }
|
||||
bool is_max_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_UNSPECIFIED; }
|
||||
bool is_to_ubv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED; }
|
||||
bool is_to_sbv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED; }
|
||||
bool is_to_ieee_bv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED; }
|
||||
bool is_to_real_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED; }
|
||||
|
||||
bool contains_floats(ast * a);
|
||||
};
|
||||
|
|
|
@ -18,11 +18,12 @@ Notes:
|
|||
--*/
|
||||
#include"fpa_rewriter.h"
|
||||
#include"fpa_rewriter_params.hpp"
|
||||
#include"ast_smt2_pp.h"
|
||||
|
||||
fpa_rewriter::fpa_rewriter(ast_manager & m, params_ref const & p) :
|
||||
m_util(m),
|
||||
m_fm(m_util.fm()),
|
||||
m_hi_fp_unspecified(true) {
|
||||
m_hi_fp_unspecified(false) {
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
|
@ -98,7 +99,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
case OP_FPA_INTERNAL_MIN_UNSPECIFIED:
|
||||
case OP_FPA_INTERNAL_MAX_UNSPECIFIED:
|
||||
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_BV2RM: SASSERT(num_args == 1); st = mk_bv2rm(args[0], result); break;
|
||||
|
||||
|
@ -117,34 +118,40 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
|
||||
br_status fpa_rewriter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width, expr_ref & result) {
|
||||
bv_util bu(m());
|
||||
if (m_hi_fp_unspecified)
|
||||
if (m_hi_fp_unspecified) {
|
||||
// The "hardware interpretation" is 0.
|
||||
result = bu.mk_numeral(0, width);
|
||||
else
|
||||
return BR_DONE;
|
||||
}
|
||||
else {
|
||||
result = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width);
|
||||
|
||||
return BR_DONE;
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
}
|
||||
|
||||
br_status fpa_rewriter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width, expr_ref & result) {
|
||||
bv_util bu(m());
|
||||
if (m_hi_fp_unspecified)
|
||||
if (m_hi_fp_unspecified) {
|
||||
// The "hardware interpretation" is 0.
|
||||
result = bu.mk_numeral(0, width);
|
||||
else
|
||||
return BR_DONE;
|
||||
}
|
||||
else {
|
||||
result = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width);
|
||||
|
||||
return BR_DONE;
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
}
|
||||
|
||||
br_status fpa_rewriter::mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result) {
|
||||
if (m_hi_fp_unspecified)
|
||||
if (m_hi_fp_unspecified) {
|
||||
// The "hardware interpretation" is 0.
|
||||
result = m_util.au().mk_numeral(rational(0), false);
|
||||
else
|
||||
return BR_DONE;
|
||||
}
|
||||
else {
|
||||
result = m_util.mk_internal_to_real_unspecified(ebits, sbits);
|
||||
|
||||
return BR_DONE;
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
}
|
||||
|
||||
br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
|
||||
|
@ -776,10 +783,8 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_
|
|||
m_util.is_numeral(arg2, v)) {
|
||||
const mpf & x = v.get();
|
||||
|
||||
if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v)) {
|
||||
mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
|
||||
return BR_REWRITE_FULL;
|
||||
}
|
||||
if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v))
|
||||
return mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
|
||||
|
||||
bv_util bu(m());
|
||||
scoped_mpq q(m_fm.mpq_manager());
|
||||
|
@ -789,11 +794,13 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_
|
|||
rational ul, ll;
|
||||
ul = m_fm.m_powers2.m1(bv_sz);
|
||||
ll = rational(0);
|
||||
if (r >= ll && r <= ul)
|
||||
if (r >= ll && r <= ul) {
|
||||
result = bu.mk_numeral(r, bv_sz);
|
||||
return BR_DONE;
|
||||
}
|
||||
else
|
||||
mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
|
||||
return BR_DONE;
|
||||
return mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
|
||||
|
||||
}
|
||||
|
||||
return BR_FAILED;
|
||||
|
@ -810,10 +817,8 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
|
|||
m_util.is_numeral(arg2, v)) {
|
||||
const mpf & x = v.get();
|
||||
|
||||
if (m_fm.is_nan(v) || m_fm.is_inf(v)) {
|
||||
mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
|
||||
return BR_REWRITE_FULL;
|
||||
}
|
||||
if (m_fm.is_nan(v) || m_fm.is_inf(v))
|
||||
return mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
|
||||
|
||||
bv_util bu(m());
|
||||
scoped_mpq q(m_fm.mpq_manager());
|
||||
|
@ -823,46 +828,42 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
|
|||
rational ul, ll;
|
||||
ul = m_fm.m_powers2.m1(bv_sz - 1);
|
||||
ll = - m_fm.m_powers2(bv_sz - 1);
|
||||
if (r >= ll && r <= ul)
|
||||
if (r >= ll && r <= ul) {
|
||||
result = bu.mk_numeral(r, bv_sz);
|
||||
return BR_DONE;
|
||||
}
|
||||
else
|
||||
mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
|
||||
return BR_DONE;
|
||||
return mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
|
||||
}
|
||||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result) {
|
||||
TRACE("fp_rewriter", tout << "to_ieee_bv of " << mk_ismt2_pp(arg, m()) << std::endl;);
|
||||
scoped_mpf v(m_fm);
|
||||
|
||||
if (m_util.is_numeral(arg, v)) {
|
||||
TRACE("fp_rewriter", tout << "to_ieee_bv numeral: " << m_fm.to_string(v) << std::endl;);
|
||||
bv_util bu(m());
|
||||
const mpf & x = v.get();
|
||||
|
||||
if (m_fm.is_nan(v)) {
|
||||
if (m_hi_fp_unspecified) {
|
||||
result = bu.mk_concat(bu.mk_numeral(0, 1),
|
||||
bu.mk_concat(bu.mk_numeral(-1, x.get_ebits()),
|
||||
bu.mk_concat(bu.mk_numeral(0, x.get_sbits() - 2),
|
||||
bu.mk_numeral(1, 1))));
|
||||
expr * args[4] = { bu.mk_numeral(0, 1),
|
||||
bu.mk_numeral(-1, x.get_ebits()),
|
||||
bu.mk_numeral(0, x.get_sbits() - 2),
|
||||
bu.mk_numeral(1, 1) };
|
||||
result = bu.mk_concat(4, args);
|
||||
}
|
||||
else {
|
||||
app_ref unspec(m()), mask(m()), extra(m());
|
||||
unspec = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits());
|
||||
mask = bu.mk_concat(bu.mk_numeral(0, 1),
|
||||
bu.mk_concat(bu.mk_numeral(-1, x.get_ebits()),
|
||||
bu.mk_concat(bu.mk_numeral(0, x.get_sbits() - 2),
|
||||
bu.mk_numeral(1, 1))));
|
||||
expr * args[2] = { unspec, mask };
|
||||
result = m().mk_app(bu.get_fid(), OP_BOR, 2, args);
|
||||
}
|
||||
return BR_REWRITE_FULL;
|
||||
else
|
||||
result = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits());
|
||||
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
else {
|
||||
scoped_mpz rz(m_fm.mpq_manager());
|
||||
m_fm.to_ieee_bv_mpz(v, rz);
|
||||
|
||||
result = bu.mk_numeral(rational(rz), x.get_ebits() + x.get_sbits());
|
||||
return BR_DONE;
|
||||
}
|
||||
|
|
|
@ -1,5 +1,5 @@
|
|||
def_module_params(module_name='rewriter',
|
||||
class_name='fpa_rewriter_params',
|
||||
export=True,
|
||||
params=(("hi_fp_unspecified", BOOL, True, "use the 'hardware interpretation' for unspecified values in fp.to_ubv, fp.to_sbv, and fp.to_real"),
|
||||
params=(("hi_fp_unspecified", BOOL, False, "use the 'hardware interpretation' for unspecified values in fp.to_ubv, fp.to_sbv, fp.to_real, and fp.to_ieee_bv"),
|
||||
))
|
||||
|
|
|
@ -87,3 +87,19 @@ void model_core::register_decl(func_decl * d, func_interp * fi) {
|
|||
}
|
||||
}
|
||||
|
||||
void model_core::unregister_decl(func_decl * d) {
|
||||
decl2expr::obj_map_entry * ec = m_interp.find_core(d);
|
||||
if (ec && ec->get_data().m_value != 0) {
|
||||
m_manager.dec_ref(ec->get_data().m_key);
|
||||
m_manager.dec_ref(ec->get_data().m_value);
|
||||
m_interp.remove(d);
|
||||
return;
|
||||
}
|
||||
|
||||
decl2finterp::obj_map_entry * ef = m_finterp.find_core(d);
|
||||
if (ef && ef->get_data().m_value != 0) {
|
||||
m_manager.dec_ref(ef->get_data().m_key);
|
||||
dealloc(ef->get_data().m_value);
|
||||
m_finterp.remove(d);
|
||||
}
|
||||
}
|
|
@ -60,6 +60,7 @@ public:
|
|||
|
||||
void register_decl(func_decl * d, expr * v);
|
||||
void register_decl(func_decl * f, func_interp * fi);
|
||||
void unregister_decl(func_decl * d);
|
||||
|
||||
virtual expr * get_some_value(sort * s) = 0;
|
||||
|
||||
|
|
|
@ -21,6 +21,7 @@ Revision History:
|
|||
#include"theory_fpa.h"
|
||||
#include"theory_bv.h"
|
||||
#include"smt_model_generator.h"
|
||||
#include"bv2fpa_converter.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
|
@ -83,15 +84,15 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
theory_fpa::theory_fpa(ast_manager & m) :
|
||||
theory(m.mk_family_id("fpa")),
|
||||
m_converter(m, this),
|
||||
m_rw(m, m_converter, params_ref()),
|
||||
m_th_rw(m),
|
||||
m_trail_stack(*this),
|
||||
m_fpa_util(m_converter.fu()),
|
||||
m_bv_util(m_converter.bu()),
|
||||
m_arith_util(m_converter.au()),
|
||||
theory_fpa::theory_fpa(ast_manager & m) :
|
||||
theory(m.mk_family_id("fpa")),
|
||||
m_converter(m, this),
|
||||
m_rw(m, m_converter, params_ref()),
|
||||
m_th_rw(m),
|
||||
m_trail_stack(*this),
|
||||
m_fpa_util(m_converter.fu()),
|
||||
m_bv_util(m_converter.bu()),
|
||||
m_arith_util(m_converter.au()),
|
||||
m_is_initialized(false)
|
||||
{
|
||||
params_ref p;
|
||||
|
@ -116,15 +117,15 @@ namespace smt {
|
|||
|
||||
SASSERT(m_trail_stack.get_num_scopes() == 0);
|
||||
SASSERT(m_conversions.empty());
|
||||
SASSERT(m_is_added_to_model.empty());
|
||||
}
|
||||
SASSERT(m_is_added_to_model.empty());
|
||||
}
|
||||
void theory_fpa::init(context * ctx) {
|
||||
smt::theory::init(ctx);
|
||||
m_is_initialized = true;
|
||||
}
|
||||
|
||||
app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
|
||||
TRACE("t_fpa_detail",
|
||||
TRACE("t_fpa_detail",
|
||||
ast_manager & m = m_th.get_manager();
|
||||
for (unsigned i = 0; i < values.size(); i++)
|
||||
tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
|
||||
|
@ -201,7 +202,7 @@ namespace smt {
|
|||
app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
|
||||
SASSERT(values.size() == 1);
|
||||
|
||||
TRACE("t_fpa_detail",
|
||||
TRACE("t_fpa_detail",
|
||||
ast_manager & m = m_th.get_manager();
|
||||
for (unsigned i = 0; i < values.size(); i++)
|
||||
tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
|
||||
|
@ -235,12 +236,12 @@ namespace smt {
|
|||
app_ref res(m);
|
||||
|
||||
if (m_fpa_util.is_fp(e)) {
|
||||
expr * cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) };
|
||||
expr * cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) };
|
||||
res = m_bv_util.mk_concat(3, cargs);
|
||||
m_th_rw((expr_ref&)res);
|
||||
}
|
||||
else {
|
||||
sort * es = m.get_sort(e);
|
||||
sort * es = m.get_sort(e);
|
||||
|
||||
sort_ref bv_srt(m);
|
||||
if (m_converter.is_rm(es))
|
||||
|
@ -264,7 +265,7 @@ namespace smt {
|
|||
SASSERT(!m_fpa_util.is_fp(e));
|
||||
SASSERT(m_bv_util.is_bv(e));
|
||||
SASSERT(m_fpa_util.is_float(s) || m_fpa_util.is_rm(s));
|
||||
ast_manager & m = get_manager();
|
||||
ast_manager & m = get_manager();
|
||||
app_ref res(m);
|
||||
|
||||
unsigned bv_sz = m_bv_util.get_bv_size(e);
|
||||
|
@ -285,7 +286,7 @@ namespace smt {
|
|||
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, e),
|
||||
m_bv_util.mk_extract(sbits - 2, 0, e));
|
||||
}
|
||||
|
||||
|
||||
return res;
|
||||
}
|
||||
|
||||
|
@ -312,7 +313,7 @@ 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 (m_fpa_util.is_rm(e)) {
|
||||
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);
|
||||
|
@ -329,7 +330,7 @@ namespace smt {
|
|||
}
|
||||
else
|
||||
UNREACHABLE();
|
||||
|
||||
|
||||
return res;
|
||||
}
|
||||
|
||||
|
@ -362,7 +363,7 @@ 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
|
||||
else
|
||||
res = convert_conversion_term(e);
|
||||
|
||||
TRACE("t_fpa_detail", tout << "converted; caching:" << std::endl;
|
||||
|
@ -448,7 +449,7 @@ namespace smt {
|
|||
TRACE("t_fpa_internalize", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";);
|
||||
SASSERT(term->get_family_id() == get_family_id());
|
||||
SASSERT(!get_context().e_internalized(term));
|
||||
|
||||
|
||||
ast_manager & m = get_manager();
|
||||
context & ctx = get_context();
|
||||
|
||||
|
@ -494,7 +495,7 @@ namespace smt {
|
|||
SASSERT(n->get_owner()->get_decl()->get_range() == s);
|
||||
|
||||
ast_manager & m = get_manager();
|
||||
context & ctx = get_context();
|
||||
context & ctx = get_context();
|
||||
app_ref owner(n->get_owner(), m);
|
||||
|
||||
if (!is_attached_to_var(n)) {
|
||||
|
@ -510,7 +511,7 @@ namespace smt {
|
|||
assert_cnstr(valid);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
if (!ctx.relevancy())
|
||||
relevant_eh(owner);
|
||||
}
|
||||
|
@ -600,7 +601,7 @@ namespace smt {
|
|||
xe_eq_ye = m.mk_eq(xe, ye);
|
||||
not_xe_eq_ye = m.mk_not(xe_eq_ye);
|
||||
c_eq_iff = m.mk_iff(not_xe_eq_ye, c);
|
||||
assert_cnstr(c_eq_iff);
|
||||
assert_cnstr(c_eq_iff);
|
||||
assert_cnstr(mk_side_conditions());
|
||||
|
||||
return;
|
||||
|
@ -689,10 +690,10 @@ namespace smt {
|
|||
pop_scope_eh(m_trail_stack.get_num_scopes());
|
||||
m_converter.reset();
|
||||
m_rw.reset();
|
||||
m_th_rw.reset();
|
||||
m_trail_stack.pop_scope(m_trail_stack.get_num_scopes());
|
||||
m_th_rw.reset();
|
||||
m_trail_stack.pop_scope(m_trail_stack.get_num_scopes());
|
||||
if (m_factory) {
|
||||
dealloc(m_factory);
|
||||
dealloc(m_factory);
|
||||
m_factory = 0;
|
||||
}
|
||||
ast_manager & m = get_manager();
|
||||
|
@ -712,20 +713,6 @@ namespace smt {
|
|||
ast_manager & m = get_manager();
|
||||
m_factory = alloc(fpa_value_factory, m, get_family_id());
|
||||
mg.register_factory(m_factory);
|
||||
|
||||
fpa2bv_converter::uf2bvuf_t const & uf2bvuf = m_converter.get_uf2bvuf();
|
||||
for (fpa2bv_converter::uf2bvuf_t::iterator it = uf2bvuf.begin();
|
||||
it != uf2bvuf.end();
|
||||
it++) {
|
||||
mg.hide(it->m_value);
|
||||
}
|
||||
fpa2bv_converter::special_t const & specials = m_converter.get_min_max_specials();
|
||||
for (fpa2bv_converter::special_t::iterator it = specials.begin();
|
||||
it != specials.end();
|
||||
it++) {
|
||||
mg.hide(it->m_value.first->get_decl());
|
||||
mg.hide(it->m_value.second->get_decl());
|
||||
}
|
||||
}
|
||||
|
||||
model_value_proc * theory_fpa::mk_value(enode * n, model_generator & mg) {
|
||||
|
@ -811,7 +798,33 @@ namespace smt {
|
|||
return res;
|
||||
}
|
||||
|
||||
void theory_fpa::finalize_model(model_generator & mg) {}
|
||||
void theory_fpa::finalize_model(model_generator & mg) {
|
||||
ast_manager & m = get_manager();
|
||||
proto_model & mdl = mg.get_model();
|
||||
proto_model new_model(m);
|
||||
|
||||
bv2fpa_converter bv2fp(m, m_converter);
|
||||
|
||||
obj_hashtable<func_decl> seen;
|
||||
bv2fp.convert_min_max_specials(&mdl, &new_model, seen);
|
||||
bv2fp.convert_uf2bvuf(&mdl, &new_model, seen);
|
||||
|
||||
for (obj_hashtable<func_decl>::iterator it = seen.begin();
|
||||
it != seen.end();
|
||||
it++)
|
||||
mdl.unregister_decl(*it);
|
||||
|
||||
for (unsigned i = 0; i < new_model.get_num_constants(); i++) {
|
||||
func_decl * f = new_model.get_constant(i);
|
||||
mdl.register_decl(f, new_model.get_const_interp(f));
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < new_model.get_num_functions(); i++) {
|
||||
func_decl * f = new_model.get_function(i);
|
||||
func_interp * fi = new_model.get_func_interp(f)->copy();
|
||||
mdl.register_decl(f, fi);
|
||||
}
|
||||
}
|
||||
|
||||
void theory_fpa::display(std::ostream & out) const
|
||||
{
|
||||
|
@ -862,8 +875,8 @@ namespace smt {
|
|||
}
|
||||
|
||||
bool theory_fpa::include_func_interp(func_decl * f) {
|
||||
TRACE("t_fpa", tout << "f = " << mk_ismt2_pp(f, get_manager()) << std::endl;);
|
||||
|
||||
TRACE("t_fpa", tout << "f = " << mk_ismt2_pp(f, get_manager()) << std::endl;);
|
||||
|
||||
if (f->get_family_id() == get_family_id()) {
|
||||
bool include =
|
||||
m_fpa_util.is_min_unspecified(f) ||
|
||||
|
|
|
@ -22,448 +22,54 @@ Notes:
|
|||
|
||||
void fpa2bv_model_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) << ")";
|
||||
}
|
||||
m_bv2fp->display(out);
|
||||
out << ")";
|
||||
}
|
||||
|
||||
model_converter * fpa2bv_model_converter::translate(ast_translation & translator) {
|
||||
fpa2bv_model_converter * res = alloc(fpa2bv_model_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);
|
||||
}
|
||||
fpa2bv_model_converter * res = alloc(fpa2bv_model_converter, translator.to());
|
||||
res->m_bv2fp = m_bv2fp->translate(translator);
|
||||
return res;
|
||||
}
|
||||
|
||||
expr_ref fpa2bv_model_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();
|
||||
void fpa2bv_model_converter::convert(model_core * mc, model * float_mdl) {
|
||||
obj_hashtable<func_decl> seen;
|
||||
m_bv2fp->convert_consts(mc, float_mdl, seen);
|
||||
m_bv2fp->convert_rm_consts(mc, float_mdl, seen);
|
||||
m_bv2fp->convert_min_max_specials(mc, float_mdl, seen);
|
||||
m_bv2fp->convert_uf2bvuf(mc, float_mdl, seen);
|
||||
|
||||
expr_ref res(m);
|
||||
mpf fp_val;
|
||||
// Keep all the non-float constants.
|
||||
unsigned sz = mc->get_num_constants();
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
{
|
||||
func_decl * c = mc->get_constant(i);
|
||||
if (!seen.contains(c))
|
||||
float_mdl->register_decl(c, mc->get_const_interp(c));
|
||||
}
|
||||
|
||||
unsigned ebits = m_fpa_util.get_ebits(s);
|
||||
unsigned sbits = m_fpa_util.get_sbits(s);
|
||||
// And keep everything else
|
||||
sz = mc->get_num_functions();
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
{
|
||||
func_decl * f = mc->get_function(i);
|
||||
if (!seen.contains(f))
|
||||
{
|
||||
TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl;);
|
||||
func_interp * val = mc->get_func_interp(f)->copy();
|
||||
float_mdl->register_decl(f, val);
|
||||
}
|
||||
}
|
||||
|
||||
unsigned sgn_sz = 1;
|
||||
unsigned exp_sz = ebits;
|
||||
unsigned sig_sz = sbits - 1;
|
||||
|
||||
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);
|
||||
|
||||
// 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());
|
||||
|
||||
m_fpa_util.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), exp_z, sig_z);
|
||||
|
||||
mpzm.del(sig_z);
|
||||
|
||||
res = m_fpa_util.mk_value(fp_val);
|
||||
|
||||
TRACE("fpa2bv_mc", 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;
|
||||
sz = mc->get_num_uninterpreted_sorts();
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
{
|
||||
sort * s = mc->get_uninterpreted_sort(i);
|
||||
ptr_vector<expr> u = mc->get_universe(s);
|
||||
float_mdl->register_usort(s, u.size(), u.c_ptr());
|
||||
}
|
||||
}
|
||||
|
||||
expr_ref fpa2bv_model_converter::convert_bv2fp(model * bv_mdl, 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 sgn(m), exp(m), sig(m);
|
||||
sgn = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv);
|
||||
exp = m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv);
|
||||
sig = m_bv_util.mk_extract(sbits - 2, 0, bv);
|
||||
|
||||
expr_ref v_sgn(m), v_exp(m), v_sig(m);
|
||||
bv_mdl->eval(sgn, v_sgn);
|
||||
bv_mdl->eval(exp, v_exp);
|
||||
bv_mdl->eval(sig, v_sig);
|
||||
|
||||
return convert_bv2fp(s, v_sgn, v_exp, v_sig);
|
||||
}
|
||||
|
||||
expr_ref fpa2bv_model_converter::convert_bv2rm(expr * bv_rm) {
|
||||
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();
|
||||
}
|
||||
}
|
||||
|
||||
return res;
|
||||
}
|
||||
|
||||
expr_ref fpa2bv_model_converter::convert_bv2rm(model * bv_mdl, expr * val) {
|
||||
expr_ref res(m);
|
||||
expr_ref eval_v(m);
|
||||
|
||||
if (val && bv_mdl->eval(val, eval_v, true))
|
||||
res = convert_bv2rm(eval_v);
|
||||
|
||||
return res;
|
||||
}
|
||||
|
||||
expr_ref fpa2bv_model_converter::rebuild_floats(model * bv_mdl, sort * s, expr * e) {
|
||||
expr_ref result(m);
|
||||
TRACE("fpa2bv_mc", tout << "rebuild floats in " << mk_ismt2_pp(s, m) << " for " << mk_ismt2_pp(e, m) << std::endl;);
|
||||
|
||||
if (m_fpa_util.is_float(s)) {
|
||||
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(bv_mdl, s, e);
|
||||
}
|
||||
}
|
||||
else if (m_fpa_util.is_rm(s)) {
|
||||
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(bv_mdl, 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(bv_mdl, a->get_decl()->get_domain()[i], a->get_arg(i)));
|
||||
result = m.mk_app(a->get_decl(), new_args.size(), new_args.c_ptr());
|
||||
}
|
||||
|
||||
return result;
|
||||
}
|
||||
|
||||
fpa2bv_model_converter::array_model fpa2bv_model_converter::convert_array_func_interp(func_decl * f, func_decl * bv_f, model * bv_mdl) {
|
||||
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;
|
||||
|
||||
expr_ref as_arr_mdl(m);
|
||||
as_arr_mdl = bv_mdl->get_const_interp(bv_f);
|
||||
if (as_arr_mdl == 0) return am;
|
||||
TRACE("fpa2bv_mc", 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));
|
||||
|
||||
am.new_float_fd = m.mk_fresh_func_decl(arity, array_domain.c_ptr(), rng);
|
||||
am.new_float_fi = convert_func_interp(am.new_float_fd, bv_f, bv_mdl);
|
||||
am.bv_fd = bv_f;
|
||||
am.result = arr_util.mk_as_array(f->get_range(), am.new_float_fd);
|
||||
return am;
|
||||
}
|
||||
|
||||
func_interp * fpa2bv_model_converter::convert_func_interp(func_decl * f, func_decl * bv_f, model * bv_mdl) {
|
||||
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 = bv_mdl->get_func_interp(bv_f);
|
||||
|
||||
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 j = 0; j < arity; j++) {
|
||||
sort * ft_dj = dmn[j];
|
||||
expr * bv_aj = bv_args[j];
|
||||
ai = rebuild_floats(bv_mdl, ft_dj, 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(bv_mdl, rng, bv_fres);
|
||||
m_th_rw(ft_fres);
|
||||
result->insert_new_entry(new_args.c_ptr(), ft_fres);
|
||||
}
|
||||
|
||||
expr_ref bv_els(m), ft_els(m);
|
||||
bv_els = bv_fi->get_else();
|
||||
ft_els = rebuild_floats(bv_mdl, rng, bv_els);
|
||||
m_th_rw(ft_els);
|
||||
result->set_else(ft_els);
|
||||
}
|
||||
|
||||
return result;
|
||||
}
|
||||
|
||||
void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
|
||||
TRACE("fpa2bv_mc", tout << "BV Model: " << std::endl;
|
||||
for (unsigned i = 0; i < bv_mdl->get_num_constants(); i++)
|
||||
tout << bv_mdl->get_constant(i)->get_name() << " --> " <<
|
||||
mk_ismt2_pp(bv_mdl->get_const_interp(bv_mdl->get_constant(i)), m) << std::endl;
|
||||
for (unsigned i = 0; i < bv_mdl->get_num_functions(); i++) {
|
||||
func_decl * f = bv_mdl->get_function(i);
|
||||
tout << f->get_name() << "(...) := " << std::endl;
|
||||
func_interp * fi = bv_mdl->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;
|
||||
});
|
||||
|
||||
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;
|
||||
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);
|
||||
bv_mdl->eval(it->m_value.first, pn, true);
|
||||
bv_mdl->eval(it->m_value.second, np, true);
|
||||
seen.insert(it->m_value.first->get_decl());
|
||||
seen.insert(it->m_value.second->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);
|
||||
|
||||
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);
|
||||
|
||||
float_mdl->register_decl(f, flt_fi);
|
||||
TRACE("fpa2bv_mc", tout << "fp.min/fp.max special: " << std::endl <<
|
||||
mk_ismt2_pp(f, m) << " == " << mk_ismt2_pp(flt_fi->get_interp(), m) << std::endl;);
|
||||
}
|
||||
|
||||
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);
|
||||
|
||||
expr_ref sgn(m), sig(m), exp(m);
|
||||
bv_mdl->eval(val->get_arg(0), sgn, true);
|
||||
bv_mdl->eval(val->get_arg(1), exp, true);
|
||||
bv_mdl->eval(val->get_arg(2), sig, true);
|
||||
|
||||
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());
|
||||
#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());
|
||||
#endif
|
||||
|
||||
if (!sgn && !sig && !exp)
|
||||
continue;
|
||||
|
||||
expr_ref cv(m);
|
||||
cv = convert_bv2fp(var->get_range(), sgn, exp, sig);
|
||||
float_mdl->register_decl(var, cv);
|
||||
|
||||
TRACE("fpa2bv_mc", tout << var->get_name() << " == " << mk_ismt2_pp(cv, m) << std::endl;);
|
||||
}
|
||||
|
||||
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(bv_mdl, bvval);
|
||||
TRACE("fpa2bv_mc", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << ")" << std::endl;);
|
||||
float_mdl->register_decl(var, fv);
|
||||
seen.insert(to_app(bvval)->get_decl());
|
||||
}
|
||||
|
||||
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(f, it->m_value, bv_mdl);
|
||||
if (am.new_float_fd) float_mdl->register_decl(am.new_float_fd, am.new_float_fi);
|
||||
if (am.result) float_mdl->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 val(m);
|
||||
bv_mdl->eval(it->m_value, val);
|
||||
if (val) float_mdl->register_decl(f, val);
|
||||
}
|
||||
}
|
||||
else {
|
||||
func_interp * fmv = convert_func_interp(f, it->m_value, bv_mdl);
|
||||
if (fmv) float_mdl->register_decl(f, fmv);
|
||||
}
|
||||
}
|
||||
|
||||
// Keep all the non-float constants.
|
||||
unsigned sz = bv_mdl->get_num_constants();
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
{
|
||||
func_decl * c = bv_mdl->get_constant(i);
|
||||
if (!seen.contains(c))
|
||||
float_mdl->register_decl(c, bv_mdl->get_const_interp(c));
|
||||
}
|
||||
|
||||
// And keep everything else
|
||||
sz = bv_mdl->get_num_functions();
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
{
|
||||
func_decl * f = bv_mdl->get_function(i);
|
||||
if (!seen.contains(f))
|
||||
{
|
||||
TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl;);
|
||||
func_interp * val = bv_mdl->get_func_interp(f)->copy();
|
||||
float_mdl->register_decl(f, val);
|
||||
}
|
||||
}
|
||||
|
||||
sz = bv_mdl->get_num_uninterpreted_sorts();
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
{
|
||||
sort * s = bv_mdl->get_uninterpreted_sort(i);
|
||||
ptr_vector<expr> u = bv_mdl->get_universe(s);
|
||||
float_mdl->register_usort(s, u.size(), u.c_ptr());
|
||||
}
|
||||
}
|
||||
|
||||
model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv) {
|
||||
model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter & conv) {
|
||||
return alloc(fpa2bv_model_converter, m, conv);
|
||||
}
|
||||
|
|
|
@ -19,79 +19,29 @@ Notes:
|
|||
#ifndef FPA2BV_MODEL_CONVERTER_H_
|
||||
#define FPA2BV_MODEL_CONVERTER_H_
|
||||
|
||||
#include"th_rewriter.h"
|
||||
#include"fpa2bv_converter.h"
|
||||
#include"model_converter.h"
|
||||
#include"bv2fpa_converter.h"
|
||||
|
||||
class fpa2bv_model_converter : public model_converter {
|
||||
ast_manager & m;
|
||||
fpa_util m_fpa_util;
|
||||
bv_util m_bv_util;
|
||||
th_rewriter m_th_rw;
|
||||
bv2fpa_converter * m_bv2fp;
|
||||
|
||||
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:
|
||||
fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & 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);
|
||||
}
|
||||
fpa2bv_model_converter(ast_manager & m, fpa2bv_converter & conv) :
|
||||
m(m) {
|
||||
m_bv2fp = alloc(bv2fpa_converter, m, conv);
|
||||
}
|
||||
|
||||
virtual ~fpa2bv_model_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);
|
||||
}
|
||||
if (m_bv2fp) dealloc(m_bv2fp);
|
||||
m_bv2fp = 0;
|
||||
}
|
||||
|
||||
virtual void operator()(model_ref & md, unsigned goal_idx) {
|
||||
SASSERT(goal_idx == 0);
|
||||
model * new_model = alloc(model, m);
|
||||
obj_hashtable<func_decl> bits;
|
||||
convert(md.get(), new_model);
|
||||
convert(md.get(), new_model);
|
||||
md = new_model;
|
||||
}
|
||||
|
||||
|
@ -106,32 +56,12 @@ public:
|
|||
protected:
|
||||
fpa2bv_model_converter(ast_manager & m) :
|
||||
m(m),
|
||||
m_fpa_util(m),
|
||||
m_bv_util(m),
|
||||
m_th_rw(m) {}
|
||||
m_bv2fp(0) {}
|
||||
|
||||
void convert(model * bv_mdl, model * float_mdl);
|
||||
expr_ref convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig);
|
||||
expr_ref convert_bv2fp(model * bv_mdl, sort * s, expr * bv);
|
||||
expr_ref convert_bv2rm(expr * eval_v);
|
||||
expr_ref convert_bv2rm(model * bv_mdl, expr * val);
|
||||
|
||||
func_interp * convert_func_interp(func_decl * f, func_decl * bv_f, model * bv_mdl);
|
||||
expr_ref rebuild_floats(model * bv_mdl, sort * s, expr * 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) {}
|
||||
};
|
||||
|
||||
array_model convert_array_func_interp(func_decl * f, func_decl * bv_f, model * bv_mdl);
|
||||
void convert(model_core * mc, model * float_mdl);
|
||||
};
|
||||
|
||||
|
||||
model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv);
|
||||
model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter & conv);
|
||||
|
||||
#endif
|
||||
|
|
Loading…
Reference in a new issue