mirror of
https://github.com/Z3Prover/z3
synced 2025-04-29 03:45:51 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
Nikolaj Bjorner
commit
f78c769b3b
7 changed files with 141 additions and 117 deletions
|
|
@ -36,10 +36,6 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
|
|||
m_mpf_manager(m_util.fm()),
|
||||
m_mpz_manager(m_mpf_manager.mpz_manager()),
|
||||
m_hi_fp_unspecified(true),
|
||||
m_min_pn_zeros(0, m),
|
||||
m_min_np_zeros(0, m),
|
||||
m_max_pn_zeros(0, m),
|
||||
m_max_np_zeros(0, m),
|
||||
m_extra_assertions(m) {
|
||||
m_plugin = static_cast<fpa_decl_plugin*>(m.get_plugin(m.mk_family_id("fpa")));
|
||||
}
|
||||
|
|
@ -1154,22 +1150,22 @@ expr_ref fpa2bv_converter::mk_min_unspecified(func_decl * f, expr * x, expr * y)
|
|||
// The hardware interpretation is -0.0.
|
||||
mk_nzero(f, res);
|
||||
else {
|
||||
if (m_min_pn_zeros == 0) {
|
||||
m_min_pn_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
|
||||
m_decls_to_hide.insert_if_not_there(m_min_pn_zeros->get_decl());
|
||||
}
|
||||
|
||||
if (m_min_np_zeros == 0) {
|
||||
m_min_np_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
|
||||
m_decls_to_hide.insert_if_not_there(m_min_np_zeros->get_decl());
|
||||
std::pair<app*, app*> decls(0, 0);
|
||||
if (!m_specials.find(f, decls)) {
|
||||
decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
|
||||
decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
|
||||
m_specials.insert(f, decls);
|
||||
m.inc_ref(f);
|
||||
m.inc_ref(decls.first);
|
||||
m.inc_ref(decls.second);
|
||||
}
|
||||
|
||||
expr_ref pn(m), np(m);
|
||||
mk_fp(m_min_pn_zeros,
|
||||
mk_fp(decls.first,
|
||||
m_bv_util.mk_numeral(0, ebits),
|
||||
m_bv_util.mk_numeral(0, sbits - 1),
|
||||
pn);
|
||||
mk_fp(m_min_np_zeros,
|
||||
mk_fp(decls.second,
|
||||
m_bv_util.mk_numeral(0, ebits),
|
||||
m_bv_util.mk_numeral(0, sbits - 1),
|
||||
np);
|
||||
|
|
@ -1243,22 +1239,22 @@ expr_ref fpa2bv_converter::mk_max_unspecified(func_decl * f, expr * x, expr * y)
|
|||
// The hardware interpretation is +0.0.
|
||||
mk_pzero(f, res);
|
||||
else {
|
||||
if (m_max_pn_zeros == 0) {
|
||||
m_max_pn_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
|
||||
m_decls_to_hide.insert_if_not_there(m_max_pn_zeros->get_decl());
|
||||
}
|
||||
|
||||
if (m_max_np_zeros == 0) {
|
||||
m_max_np_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
|
||||
m_decls_to_hide.insert_if_not_there(m_max_np_zeros->get_decl());
|
||||
std::pair<app*, app*> decls(0, 0);
|
||||
if (!m_specials.find(f, decls)) {
|
||||
decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
|
||||
decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
|
||||
m_specials.insert(f, decls);
|
||||
m.inc_ref(f);
|
||||
m.inc_ref(decls.first);
|
||||
m.inc_ref(decls.second);
|
||||
}
|
||||
|
||||
expr_ref pn(m), np(m);
|
||||
mk_fp(m_max_pn_zeros,
|
||||
mk_fp(decls.first,
|
||||
m_bv_util.mk_numeral(0, ebits),
|
||||
m_bv_util.mk_numeral(0, sbits - 1),
|
||||
pn);
|
||||
mk_fp(m_max_np_zeros,
|
||||
mk_fp(decls.second,
|
||||
m_bv_util.mk_numeral(0, ebits),
|
||||
m_bv_util.mk_numeral(0, sbits - 1),
|
||||
np);
|
||||
|
|
@ -3839,14 +3835,16 @@ void fpa2bv_converter::round(sort * s, expr_ref & bv_rm, expr_ref & sgn, expr_re
|
|||
TRACE("fpa2bv_round", tout << "ROUND = " << mk_ismt2_pp(result, m) << std::endl; );
|
||||
}
|
||||
|
||||
|
||||
void fpa2bv_converter::reset(void) {
|
||||
dec_ref_map_key_values(m, m_const2bv);
|
||||
dec_ref_map_key_values(m, m_rm_const2bv);
|
||||
dec_ref_map_key_values(m, m_uf2bvuf);
|
||||
m_min_np_zeros = 0;
|
||||
m_min_pn_zeros = 0;
|
||||
m_max_np_zeros = 0;
|
||||
m_max_pn_zeros = 0;
|
||||
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);
|
||||
}
|
||||
m_extra_assertions.reset();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -35,8 +35,8 @@ struct func_decl_triple {
|
|||
f_exp = exp;
|
||||
}
|
||||
func_decl * f_sgn;
|
||||
func_decl * f_sig;
|
||||
func_decl * f_exp;
|
||||
func_decl * f_sig;
|
||||
func_decl * f_exp;
|
||||
};
|
||||
|
||||
class fpa2bv_converter {
|
||||
|
|
@ -47,22 +47,20 @@ protected:
|
|||
bv_util m_bv_util;
|
||||
arith_util m_arith_util;
|
||||
mpf_manager & m_mpf_manager;
|
||||
unsynch_mpz_manager & m_mpz_manager;
|
||||
unsynch_mpz_manager & m_mpz_manager;
|
||||
fpa_decl_plugin * m_plugin;
|
||||
bool m_hi_fp_unspecified;
|
||||
|
||||
obj_map<func_decl, expr*> m_const2bv;
|
||||
obj_map<func_decl, expr*> m_rm_const2bv;
|
||||
obj_map<func_decl, func_decl*> m_uf2bvuf;
|
||||
obj_hashtable<func_decl> m_decls_to_hide;
|
||||
|
||||
app_ref m_min_pn_zeros;
|
||||
app_ref m_min_np_zeros;
|
||||
app_ref m_max_pn_zeros;
|
||||
app_ref m_max_np_zeros;
|
||||
|
||||
obj_map<func_decl, std::pair<app *, app *> > m_specials;
|
||||
|
||||
friend class fpa2bv_model_converter;
|
||||
|
||||
public:
|
||||
fpa2bv_converter(ast_manager & m);
|
||||
fpa2bv_converter(ast_manager & m);
|
||||
~fpa2bv_converter();
|
||||
|
||||
fpa_util & fu() { return m_util; }
|
||||
|
|
@ -83,7 +81,7 @@ public:
|
|||
void split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const;
|
||||
void split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const;
|
||||
|
||||
void mk_eq(expr * a, expr * b, expr_ref & result);
|
||||
void mk_eq(expr * a, expr * b, expr_ref & result);
|
||||
void mk_ite(expr * c, expr * t, expr * f, expr_ref & result);
|
||||
void mk_distinct(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
|
||||
|
|
@ -98,7 +96,7 @@ public:
|
|||
void mk_ninf(func_decl * f, expr_ref & result);
|
||||
void mk_nan(func_decl * f, expr_ref & result);
|
||||
void mk_nzero(func_decl *f, expr_ref & result);
|
||||
void mk_pzero(func_decl *f, expr_ref & result);
|
||||
void mk_pzero(func_decl *f, expr_ref & result);
|
||||
|
||||
void mk_add(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_sub(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
|
|
@ -106,7 +104,7 @@ public:
|
|||
void mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_div(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_rem(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_abs(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_abs(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_round_to_integral(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
|
|
@ -125,10 +123,10 @@ public:
|
|||
void mk_is_nan(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
|
||||
void mk_to_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result);
|
||||
void mk_to_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result);
|
||||
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);
|
||||
|
|
@ -137,7 +135,7 @@ public:
|
|||
|
||||
void mk_to_ubv(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_real(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 set_unspecified_fp_hi(bool v) { m_hi_fp_unspecified = v; }
|
||||
|
||||
|
|
@ -145,7 +143,7 @@ public:
|
|||
void mk_min_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
virtual expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y);
|
||||
|
||||
void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
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);
|
||||
virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y);
|
||||
|
||||
|
|
@ -153,11 +151,6 @@ public:
|
|||
expr_ref mk_to_sbv_unspecified(unsigned width);
|
||||
expr_ref mk_to_real_unspecified();
|
||||
|
||||
obj_map<func_decl, expr*> const & const2bv() const { return m_const2bv; }
|
||||
obj_map<func_decl, expr*> const & rm_const2bv() const { return m_rm_const2bv; }
|
||||
obj_map<func_decl, func_decl*> const & uf2bvuf() const { return m_uf2bvuf; }
|
||||
obj_hashtable<func_decl> const & decls_to_hide() const { return m_decls_to_hide; }
|
||||
|
||||
void reset(void);
|
||||
|
||||
void dbg_decouple(const char * prefix, expr_ref & e);
|
||||
|
|
@ -191,7 +184,7 @@ protected:
|
|||
void mk_unbias(expr * e, expr_ref & result);
|
||||
|
||||
void unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & lz, bool normalize);
|
||||
void round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & result);
|
||||
void round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & result);
|
||||
expr_ref mk_rounding_decision(expr * rm, expr * sgn, expr * last, expr * round, expr * sticky);
|
||||
|
||||
void add_core(unsigned sbits, unsigned ebits,
|
||||
|
|
|
|||
|
|
@ -439,7 +439,7 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
|
|||
if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
|
||||
if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) {
|
||||
result = m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, arg1, arg2);
|
||||
return BR_DONE;
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
else {
|
||||
scoped_mpf r(m_fm);
|
||||
|
|
@ -474,7 +474,7 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
|
|||
if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
|
||||
if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) {
|
||||
result = m().mk_app(get_fid(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, arg1, arg2);
|
||||
return BR_DONE;
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
else {
|
||||
scoped_mpf r(m_fm);
|
||||
|
|
|
|||
|
|
@ -737,10 +737,11 @@ namespace smt {
|
|||
|
||||
expr_ref converted(m);
|
||||
converted = m.mk_and(convert(e), mk_side_conditions());
|
||||
if (is_true)
|
||||
assert_cnstr(m.mk_implies(e, converted));
|
||||
else
|
||||
assert_cnstr(m.mk_implies(m.mk_not(e), m.mk_not(converted)));
|
||||
|
||||
expr_ref cnstr(m);
|
||||
cnstr = (is_true) ? m.mk_implies(e, converted) : m.mk_implies(converted, e);
|
||||
m_th_rw(cnstr);
|
||||
assert_cnstr(cnstr);
|
||||
}
|
||||
|
||||
void theory_fpa::relevant_eh(app * n) {
|
||||
|
|
|
|||
|
|
@ -45,6 +45,15 @@ void fpa2bv_model_converter::display(std::ostream & out) {
|
|||
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 << ")" << std::endl;
|
||||
}
|
||||
|
||||
|
|
@ -79,12 +88,16 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator
|
|||
translator.to().inc_ref(k);
|
||||
translator.to().inc_ref(v);
|
||||
}
|
||||
for (obj_hashtable<func_decl>::iterator it = m_decls_to_hide.begin();
|
||||
it != m_decls_to_hide.end();
|
||||
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
|
||||
it != m_specials.end();
|
||||
it++) {
|
||||
func_decl * k = translator(*it);
|
||||
res->m_decls_to_hide.insert(k);
|
||||
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;
|
||||
}
|
||||
|
|
@ -217,10 +230,34 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
|
|||
|
||||
obj_hashtable<func_decl> seen;
|
||||
|
||||
for (obj_hashtable<func_decl>::iterator it = m_decls_to_hide.begin();
|
||||
it != m_decls_to_hide.end();
|
||||
it++)
|
||||
seen.insert(*it);
|
||||
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 = fu.mk_pzero(f->get_range());
|
||||
nzero = fu.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;
|
||||
bu.is_numeral(pn, pn_num, bv_sz);
|
||||
bu.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();
|
||||
|
|
@ -362,10 +399,6 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
|
|||
}
|
||||
}
|
||||
|
||||
model_converter * mk_fpa2bv_model_converter(ast_manager & m,
|
||||
obj_map<func_decl, expr*> const & const2bv,
|
||||
obj_map<func_decl, expr*> const & rm_const2bv,
|
||||
obj_map<func_decl, func_decl*> const & uf2bvuf,
|
||||
obj_hashtable<func_decl> const & decls_to_hide) {
|
||||
return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf, decls_to_hide);
|
||||
model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv) {
|
||||
return alloc(fpa2bv_model_converter, m, conv);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -27,44 +27,41 @@ class fpa2bv_model_converter : public model_converter {
|
|||
obj_map<func_decl, expr*> m_const2bv;
|
||||
obj_map<func_decl, expr*> m_rm_const2bv;
|
||||
obj_map<func_decl, func_decl*> m_uf2bvuf;
|
||||
obj_hashtable<func_decl> m_decls_to_hide;
|
||||
obj_map<func_decl, std::pair<app*, app*> > m_specials;
|
||||
|
||||
public:
|
||||
fpa2bv_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bv,
|
||||
obj_map<func_decl, expr*> const & rm_const2bv,
|
||||
obj_map<func_decl, func_decl*> const & uf2bvuf,
|
||||
obj_hashtable<func_decl> const & decls_to_hide) :
|
||||
m(m) {
|
||||
for (obj_map<func_decl, expr*>::iterator it = const2bv.begin();
|
||||
it != const2bv.end();
|
||||
fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv) : m(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 = rm_const2bv.begin();
|
||||
it != rm_const2bv.end();
|
||||
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 = uf2bvuf.begin();
|
||||
it != uf2bvuf.end();
|
||||
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_hashtable<func_decl>::iterator it = decls_to_hide.begin();
|
||||
it != decls_to_hide.end();
|
||||
it++)
|
||||
{
|
||||
m_decls_to_hide.insert(*it);
|
||||
m.inc_ref(*it);
|
||||
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = conv.m_specials.begin();
|
||||
it != conv.m_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);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -72,7 +69,13 @@ public:
|
|||
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);
|
||||
dec_ref_collection_values(m, m_decls_to_hide);
|
||||
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);
|
||||
}
|
||||
}
|
||||
|
||||
virtual void operator()(model_ref & md, unsigned goal_idx) {
|
||||
|
|
@ -92,7 +95,7 @@ public:
|
|||
virtual model_converter * translate(ast_translation & translator);
|
||||
|
||||
protected:
|
||||
fpa2bv_model_converter(ast_manager & m) : m(m) { }
|
||||
fpa2bv_model_converter(ast_manager & m) : m(m){ }
|
||||
|
||||
void convert(model * bv_mdl, model * float_mdl);
|
||||
expr_ref convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig) const;
|
||||
|
|
@ -102,10 +105,6 @@ protected:
|
|||
};
|
||||
|
||||
|
||||
model_converter * mk_fpa2bv_model_converter(ast_manager & m,
|
||||
obj_map<func_decl, expr*> const & const2bv,
|
||||
obj_map<func_decl, expr*> const & rm_const2bv,
|
||||
obj_map<func_decl, func_decl*> const & uf2bvuf,
|
||||
obj_hashtable<func_decl> const & decls_to_hide);
|
||||
model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv);
|
||||
|
||||
#endif
|
||||
|
|
@ -43,26 +43,26 @@ class fpa2bv_tactic : public tactic {
|
|||
}
|
||||
|
||||
void updt_params(params_ref const & p) {
|
||||
m_rw.cfg().updt_params(p);
|
||||
m_rw.cfg().updt_params(p);
|
||||
}
|
||||
|
||||
|
||||
void set_cancel(bool f) {
|
||||
m_rw.set_cancel(f);
|
||||
}
|
||||
|
||||
virtual void operator()(goal_ref const & g,
|
||||
goal_ref_buffer & result,
|
||||
model_converter_ref & mc,
|
||||
virtual void operator()(goal_ref const & g,
|
||||
goal_ref_buffer & result,
|
||||
model_converter_ref & mc,
|
||||
proof_converter_ref & pc,
|
||||
expr_dependency_ref & core) {
|
||||
SASSERT(g->is_well_sorted());
|
||||
m_proofs_enabled = g->proofs_enabled();
|
||||
m_produce_models = g->models_enabled();
|
||||
m_produce_unsat_cores = g->unsat_core_enabled();
|
||||
|
||||
|
||||
mc = 0; pc = 0; core = 0; result.reset();
|
||||
tactic_report report("fpa2bv", *g);
|
||||
m_rw.reset();
|
||||
m_rw.reset();
|
||||
|
||||
TRACE("fpa2bv", tout << "BEFORE: " << std::endl; g->display(tout););
|
||||
|
||||
|
|
@ -70,7 +70,7 @@ class fpa2bv_tactic : public tactic {
|
|||
result.push_back(g.get());
|
||||
return;
|
||||
}
|
||||
|
||||
|
||||
m_num_steps = 0;
|
||||
expr_ref new_curr(m);
|
||||
proof_ref new_pr(m);
|
||||
|
|
@ -91,7 +91,7 @@ class fpa2bv_tactic : public tactic {
|
|||
const app * a = to_app(new_curr.get());
|
||||
if (a->get_family_id() == m_conv.fu().get_family_id() &&
|
||||
a->get_decl_kind() == OP_FPA_IS_NAN) {
|
||||
// Inject auxiliary lemmas that fix e to the one and only NaN value,
|
||||
// Inject auxiliary lemmas that fix e to the one and only NaN value,
|
||||
// that is (= e (fp #b0 #b1...1 #b0...01)), so that the value propagation
|
||||
// has a value to propagate.
|
||||
expr * sgn, *sig, *exp;
|
||||
|
|
@ -104,8 +104,8 @@ class fpa2bv_tactic : public tactic {
|
|||
}
|
||||
}
|
||||
|
||||
if (g->models_enabled())
|
||||
mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv(), m_conv.uf2bvuf(), m_conv.decls_to_hide());
|
||||
if (g->models_enabled())
|
||||
mc = mk_fpa2bv_model_converter(m, m_conv);
|
||||
|
||||
g->inc_depth();
|
||||
result.push_back(g.get());
|
||||
|
|
@ -114,7 +114,7 @@ class fpa2bv_tactic : public tactic {
|
|||
result.back()->assert_expr(m_conv.m_extra_assertions[i].get());
|
||||
|
||||
SASSERT(g->is_well_sorted());
|
||||
TRACE("fpa2bv", tout << "AFTER: " << std::endl; g->display(tout);
|
||||
TRACE("fpa2bv", tout << "AFTER: " << std::endl; g->display(tout);
|
||||
if (mc) mc->display(tout); tout << std::endl; );
|
||||
}
|
||||
};
|
||||
|
|
@ -141,12 +141,12 @@ public:
|
|||
m_imp->updt_params(p);
|
||||
}
|
||||
|
||||
virtual void collect_param_descrs(param_descrs & r) {
|
||||
virtual void collect_param_descrs(param_descrs & r) {
|
||||
}
|
||||
|
||||
virtual void operator()(goal_ref const & in,
|
||||
goal_ref_buffer & result,
|
||||
model_converter_ref & mc,
|
||||
virtual void operator()(goal_ref const & in,
|
||||
goal_ref_buffer & result,
|
||||
model_converter_ref & mc,
|
||||
proof_converter_ref & pc,
|
||||
expr_dependency_ref & core) {
|
||||
try {
|
||||
|
|
@ -156,8 +156,8 @@ public:
|
|||
throw tactic_exception(ex.msg());
|
||||
}
|
||||
}
|
||||
|
||||
virtual void cleanup() {
|
||||
|
||||
virtual void cleanup() {
|
||||
imp * d = alloc(imp, m_imp->m, m_params);
|
||||
#pragma omp critical (tactic_cancel)
|
||||
{
|
||||
|
|
@ -173,6 +173,6 @@ protected:
|
|||
}
|
||||
};
|
||||
|
||||
tactic * mk_fpa2bv_tactic(ast_manager & m, params_ref const & p) {
|
||||
tactic * mk_fpa2bv_tactic(ast_manager & m, params_ref const & p) {
|
||||
return clean(alloc(fpa2bv_tactic, m, p));
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue