mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 09:35:32 +00:00
FPA: bugfixes for UF in model converter for fpa2bv.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger
parent
8f60a936d2
commit
121e83b6b7
3 changed files with 80 additions and 21 deletions
|
|
@ -2403,6 +2403,25 @@ 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, 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, func_decl_triple>::iterator it = m_uf23bvuf.begin();
|
||||
it != m_uf23bvuf.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.f_sgn, m, indent) << " ; " <<
|
||||
mk_ismt2_pp(it->m_value.f_sig, m, indent) << " ; " <<
|
||||
mk_ismt2_pp(it->m_value.f_exp, m, indent) << " ; " <<
|
||||
")";
|
||||
}
|
||||
out << ")" << std::endl;
|
||||
}
|
||||
|
||||
|
|
@ -2523,6 +2542,20 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
|
|||
}
|
||||
}
|
||||
|
||||
for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
|
||||
it != m_uf2bvuf.end();
|
||||
it++)
|
||||
seen.insert(it->m_value);
|
||||
|
||||
for (obj_map<func_decl, func_decl_triple>::iterator it = m_uf23bvuf.begin();
|
||||
it != m_uf23bvuf.end();
|
||||
it++)
|
||||
{
|
||||
seen.insert(it->m_value.f_sgn);
|
||||
seen.insert(it->m_value.f_sig);
|
||||
seen.insert(it->m_value.f_exp);
|
||||
}
|
||||
|
||||
fu.fm().del(fp_val);
|
||||
|
||||
// Keep all the non-float constants.
|
||||
|
|
@ -2530,7 +2563,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
|
|||
for (unsigned i = 0; i < sz; i++)
|
||||
{
|
||||
func_decl * c = bv_mdl->get_constant(i);
|
||||
if (!seen.contains(c))
|
||||
if (!seen.contains(c))
|
||||
float_mdl->register_decl(c, bv_mdl->get_const_interp(c));
|
||||
}
|
||||
|
||||
|
|
@ -2539,7 +2572,8 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
|
|||
for (unsigned i = 0; i < sz; i++)
|
||||
{
|
||||
func_decl * c = bv_mdl->get_function(i);
|
||||
float_mdl->register_decl(c, bv_mdl->get_const_interp(c));
|
||||
if (!seen.contains(c))
|
||||
float_mdl->register_decl(c, bv_mdl->get_const_interp(c));
|
||||
}
|
||||
|
||||
sz = bv_mdl->get_num_uninterpreted_sorts();
|
||||
|
|
@ -2553,6 +2587,8 @@ 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) {
|
||||
return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv);
|
||||
obj_map<func_decl, expr*> const & rm_const2bv,
|
||||
obj_map<func_decl, func_decl*> const & uf2bvuf,
|
||||
obj_map<func_decl, func_decl_triple> const & uf23bvuf) {
|
||||
return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf, uf23bvuf);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -31,20 +31,7 @@ typedef enum { BV_RM_TIES_TO_AWAY=0, BV_RM_TIES_TO_EVEN=1, BV_RM_TO_NEGATIVE=2,
|
|||
|
||||
class fpa2bv_model_converter;
|
||||
|
||||
class fpa2bv_converter {
|
||||
ast_manager & m;
|
||||
basic_simplifier_plugin m_simp;
|
||||
float_util m_util;
|
||||
mpf_manager & m_mpf_manager;
|
||||
unsynch_mpz_manager & m_mpz_manager;
|
||||
bv_util m_bv_util;
|
||||
float_decl_plugin * m_plugin;
|
||||
|
||||
obj_map<func_decl, expr*> m_const2bv;
|
||||
obj_map<func_decl, expr*> m_rm_const2bv;
|
||||
obj_map<func_decl, func_decl*> m_uf2bvuf;
|
||||
|
||||
struct func_decl_triple {
|
||||
struct func_decl_triple {
|
||||
func_decl_triple () { f_sgn = 0; f_sig = 0; f_exp = 0; }
|
||||
func_decl_triple (func_decl * sgn, func_decl * sig, func_decl * exp)
|
||||
{
|
||||
|
|
@ -56,6 +43,19 @@ class fpa2bv_converter {
|
|||
func_decl * f_sig;
|
||||
func_decl * f_exp;
|
||||
};
|
||||
|
||||
class fpa2bv_converter {
|
||||
ast_manager & m;
|
||||
basic_simplifier_plugin m_simp;
|
||||
float_util m_util;
|
||||
mpf_manager & m_mpf_manager;
|
||||
unsynch_mpz_manager & m_mpz_manager;
|
||||
bv_util m_bv_util;
|
||||
float_decl_plugin * m_plugin;
|
||||
|
||||
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, func_decl_triple> m_uf23bvuf;
|
||||
|
||||
public:
|
||||
|
|
@ -122,6 +122,8 @@ public:
|
|||
|
||||
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_map<func_decl, func_decl_triple> const & uf23bvuf() const { return m_uf23bvuf; }
|
||||
|
||||
void dbg_decouple(const char * prefix, expr_ref & e);
|
||||
expr_ref_vector extra_assertions;
|
||||
|
|
@ -166,10 +168,14 @@ class fpa2bv_model_converter : public model_converter {
|
|||
ast_manager & m;
|
||||
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, func_decl_triple> m_uf23bvuf;
|
||||
|
||||
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, expr*> const & rm_const2bv,
|
||||
obj_map<func_decl, func_decl*> const & uf2bvuf,
|
||||
obj_map<func_decl, func_decl_triple> const & uf23bvuf) :
|
||||
m(m) {
|
||||
// Just create a copy?
|
||||
for (obj_map<func_decl, expr*>::iterator it = const2bv.begin();
|
||||
|
|
@ -188,6 +194,21 @@ public:
|
|||
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();
|
||||
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, func_decl_triple>::iterator it = uf23bvuf.begin();
|
||||
it != uf23bvuf.end();
|
||||
it++)
|
||||
{
|
||||
m_uf23bvuf.insert(it->m_key, it->m_value);
|
||||
m.inc_ref(it->m_key);
|
||||
}
|
||||
}
|
||||
|
||||
virtual ~fpa2bv_model_converter() {
|
||||
|
|
@ -220,6 +241,8 @@ 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, expr*> const & rm_const2bv,
|
||||
obj_map<func_decl, func_decl*> const & uf2bvuf,
|
||||
obj_map<func_decl, func_decl_triple> const & uf23bvuf);
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -90,7 +90,7 @@ class fpa2bv_tactic : public tactic {
|
|||
}
|
||||
|
||||
if (g->models_enabled())
|
||||
mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv());
|
||||
mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv(), m_conv.uf2bvuf(), m_conv.uf23bvuf());
|
||||
|
||||
g->inc_depth();
|
||||
result.push_back(g.get());
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue