Skip to content

Commit

Permalink
Fix for partially interpreted floating-point functions. Relates to Z3…
Browse files Browse the repository at this point in the history 
…Prover#2596, Z3Prover#2631.
  • Loading branch information
@wintersteiger
wintersteiger committed Oct 28, 2019
1 parent d00dc40 commit db1d2bb
Show file tree
Hide file tree
Showing 7 changed files with 118 additions and 86 deletions.
80 changes: 39 additions & 41 deletions src/ast/fpa/bv2fpa_converter.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,11 +51,10 @@ bv2fpa_converter::bv2fpa_converter(ast_manager & m, fpa2bv_converter & conv) :
for (auto const& kv : conv.m_uf2bvuf) {
m_uf2bvuf.insert(kv.m_key, kv.m_value);
m.inc_ref(kv.m_key);
m.inc_ref(kv.m_value.first);
m.inc_ref(kv.m_value.second);
m.inc_ref(kv.m_value);
}
for (auto const& kv : conv.m_min_max_ufs) {
m_specials.insert(kv.m_key, kv.m_value);
m_min_max_specials.insert(kv.m_key, kv.m_value);
m.inc_ref(kv.m_key);
m.inc_ref(kv.m_value.first);
m.inc_ref(kv.m_value.second);
Expand All @@ -67,16 +66,15 @@ bv2fpa_converter::~bv2fpa_converter() {
dec_ref_map_key_values(m, m_rm_const2bv);
for (auto const& kv : m_uf2bvuf) {
m.dec_ref(kv.m_key);
m.dec_ref(kv.m_value.first);
m.dec_ref(kv.m_value.second);
m.dec_ref(kv.m_value);
}
for (auto const& kv : m_specials) {
for (auto const& kv : m_min_max_specials) {
m.dec_ref(kv.m_key);
m.dec_ref(kv.m_value.first);
m.dec_ref(kv.m_value.second);
}
m_uf2bvuf.reset();
m_specials.reset();
m_min_max_specials.reset();
}

expr_ref bv2fpa_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig) {
Expand Down Expand Up @@ -191,7 +189,7 @@ expr_ref bv2fpa_converter::convert_bv2rm(model_core * mc, expr * val) {

expr_ref bv2fpa_converter::rebuild_floats(model_core * mc, sort * s, expr * e) {
expr_ref result(m);
TRACE("bv2fpa", tout << "rebuild floats in " << mk_ismt2_pp(s, m) << " for ";
TRACE("bv2fpa_rebuild", tout << "rebuild floats in " << mk_ismt2_pp(s, m) << " for ";
if (e) tout << mk_ismt2_pp(e, m);
else tout << "nil";
tout << std::endl; );
Expand Down Expand Up @@ -288,13 +286,23 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
expr_ref ft_fres = rebuild_floats(mc, rng, to_app(bv_fres));
m_th_rw(ft_fres);
TRACE("bv2fpa",
tout << "func_interp entry #" << i << ":" << std::endl;
tout << "(" << bv_f->get_name();
for (unsigned i = 0; i < bv_f->get_arity(); i++)
tout << " " << mk_ismt2_pp(bv_args[i], m);
tout << ") = " << mk_ismt2_pp(bv_fres, m) << std::endl;
tout << " --> " << std::endl;
tout << "(" << f->get_name();
for (unsigned i = 0; i < new_args.size(); i++)
tout << mk_ismt2_pp(bv_args[i], m) << " == " <<
mk_ismt2_pp(new_args[i], m) << std::endl;
tout << mk_ismt2_pp(bv_fres, m) << " == " << mk_ismt2_pp(ft_fres, m) << std::endl;);
tout << " " << mk_ismt2_pp(new_args[i], m);
tout << ") = " << mk_ismt2_pp(ft_fres, m) << std::endl;);
func_entry * fe = result->get_entry(new_args.c_ptr());
if (fe == nullptr)
result->insert_new_entry(new_args.c_ptr(), ft_fres);
if (fe == nullptr) {
// Avoid over-specification of a partially interpreted theory function
if (f->get_family_id() != m_fpa_util.get_family_id() ||
m_fpa_util.is_considered_uninterpreted(f, new_args.size(), new_args.c_ptr()))
result->insert_new_entry(new_args.c_ptr(), ft_fres);
}
else {
// The BV model may have multiple equivalent entries using different
// representations of NaN. We can only keep one and we check that
Expand All @@ -309,6 +317,7 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
if (bv_els) {
expr_ref ft_els = rebuild_floats(mc, rng, bv_els);
m_th_rw(ft_els);
TRACE("bv2fpa", tout << "else=" << mk_ismt2_pp(ft_els, m) << std::endl;);
result->set_else(ft_els);
}
}
Expand Down Expand Up @@ -398,7 +407,7 @@ void bv2fpa_converter::convert_rm_consts(model_core * mc, model_core * target_mo
}

void bv2fpa_converter::convert_min_max_specials(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen) {
for (auto const& kv : m_specials) {
for (auto const& kv : m_min_max_specials) {
func_decl * f = kv.m_key;
app * pn_cnst = kv.m_value.first;
app * np_cnst = kv.m_value.second;
Expand Down Expand Up @@ -432,8 +441,7 @@ void bv2fpa_converter::convert_min_max_specials(model_core * mc, model_core * ta
void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen) {
for (auto const& kv : m_uf2bvuf) {
func_decl * f = kv.m_key;
func_decl* f_uf = kv.m_value.first;
expr* f_def = kv.m_value.second;
func_decl * f_uf = kv.m_value;
seen.insert(f_uf);

if (f->get_arity() == 0)
Expand All @@ -454,29 +462,22 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode
}
}
else if (f->get_family_id() == m_fpa_util.get_fid()) {
if (f_def) {
func_interp* fi = alloc(func_interp, m, f->get_arity());
expr_ref def = rebuild_floats(mc, f->get_range(), to_app(f_def));
fi->set_else(def);
SASSERT(m.get_sort(def) == f->get_range());
target_model->register_decl(f, fi);
func_interp* fj = mc->get_func_interp(f_uf);
if (fj) {
target_model->register_decl(f_uf, fj->copy());
}
continue;
}

// kv.m_value contains the model for the unspecified cases of kv.m_key in terms of bit-vectors.
// convert_func_interp rebuilds a func_interp on floats.

// f is a floating point function: f(x,y) : Float
// f_uf is a bit-vector function: f_uf(xB,yB) : BitVec
// then there is f_def: f_Bv(xB, yB) := if(range(xB),.., f_uf(xB,yB))
// f(x,y) := to_float(if(range(to_bv(x)), ... f_uf(to_bv(xB), to_bv(yB)))) - not practical
// := if(range_fp(x), ...., to_float(f_uf(...)) - approach

target_model->register_decl(f, convert_func_interp(mc, f, f_uf));
// := if(range_fp(x), ...., to_float(f_uf(...)) - approach (via fpa_util::is_considered_uninterpreted)

func_interp *fi = convert_func_interp(mc, f, f_uf);
if (fi->num_entries() > 0 || fi->get_else() != nullptr)
target_model->register_decl(f, fi);
}
}

TRACE("bv2fpa", tout << "Target model: " << *target_model; );
}

void bv2fpa_converter::display(std::ostream & out) {
Expand All @@ -496,9 +497,9 @@ void bv2fpa_converter::display(std::ostream & out) {
const symbol & n = kv.m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(kv.m_value.first, m, indent) << ")";
out << mk_ismt2_pp(kv.m_value, m, indent) << ")";
}
for (auto const& kv : m_specials) {
for (auto const& kv : m_min_max_specials) {
const symbol & n = kv.m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
Expand All @@ -525,22 +526,19 @@ bv2fpa_converter * bv2fpa_converter::translate(ast_translation & translator) {
}
for (auto const& kv : m_uf2bvuf) {
func_decl * k = translator(kv.m_key);
func_decl * v = translator(kv.m_value.first);
expr* d = translator(kv.m_value.second);
res->m_uf2bvuf.insert(k, std::make_pair(v, d));
func_decl * v = translator(kv.m_value);
res->m_uf2bvuf.insert(k, v);
translator.to().inc_ref(k);
translator.to().inc_ref(v);
translator.to().inc_ref(d);
}
for (auto const& kv : m_specials) {
for (auto const& kv : m_min_max_specials) {
func_decl * k = translator(kv.m_key);
app * v1 = translator(kv.m_value.first);
app * v2 = translator(kv.m_value.second);
res->m_specials.insert(k, std::pair<app*, app*>(v1, v2));
res->m_min_max_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;
}

4 changes: 2 additions & 2 deletions src/ast/fpa/bv2fpa_converter.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,8 @@ class bv2fpa_converter {

obj_map<func_decl, expr*> m_const2bv;
obj_map<func_decl, expr*> m_rm_const2bv;
obj_map<func_decl, std::pair<func_decl*, expr*>> m_uf2bvuf;
obj_map<func_decl, std::pair<app*, app*> > m_specials;
obj_map<func_decl, func_decl*> m_uf2bvuf;
obj_map<func_decl, std::pair<app*, app*> > m_min_max_specials;

public:
bv2fpa_converter(ast_manager & m);
Expand Down
37 changes: 6 additions & 31 deletions src/ast/fpa/fpa2bv_converter.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3203,7 +3203,6 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args

expr_ref sgn(m), sig(m), exp(m), lz(m);
unpack(x, sgn, sig, exp, lz, true);


unsigned ebits = m_util.get_ebits(xs);
unsigned sbits = m_util.get_sbits(xs);
Expand Down Expand Up @@ -4166,8 +4165,7 @@ void fpa2bv_converter::reset() {
dec_ref_map_key_values(m, m_rm_const2bv);
for (auto const& kv : m_uf2bvuf) {
m.dec_ref(kv.m_key);
m.dec_ref(kv.m_value.first);
m.dec_ref(kv.m_value.second);
m.dec_ref(kv.m_value);
}
for (auto const& kv : m_min_max_ufs) {
m.dec_ref(kv.m_key);
Expand All @@ -4180,36 +4178,13 @@ void fpa2bv_converter::reset() {
}

func_decl * fpa2bv_converter::mk_bv_uf(func_decl * f, sort * const * domain, sort * range) {
std::pair<func_decl*, expr*> res;
func_decl* res;
if (!m_uf2bvuf.find(f, res)) {
res.first = m.mk_fresh_func_decl(nullptr, f->get_arity(), domain, range);
res.second = nullptr;
res = m.mk_fresh_func_decl(nullptr, f->get_arity(), domain, range);
m.inc_ref(f);
m.inc_ref(res.first);
m.inc_ref(res);
m_uf2bvuf.insert(f, res);
TRACE("fpa2bv", tout << "New UF func_decl: " << res.first->get_id() << std::endl << mk_ismt2_pp(res.first, m) << std::endl;);
TRACE("fpa2bv", tout << "New UF func_decl: " << res->get_id() << std::endl << mk_ismt2_pp(res, m) << std::endl;);
}
return res.first;
}

expr* fpa2bv_converter::get_bv_def(func_decl* f) {
std::pair<func_decl*, expr*> res(nullptr, nullptr);
m_uf2bvuf.find(f, res);
TRACE("fpa2bv", tout << "get_bv_def " << mk_ismt2_pp(res.first, m) << " " << res.second << std::endl;);
return res.second;
}

/**
\brief expand the definition of bit-vector function f
as an expression of what is defined and what is not
defined.
*/
void fpa2bv_converter::set_bv_def(func_decl* f, expr* def) {
auto res = m_uf2bvuf[f];
SASSERT(res.first);
SASSERT(!res.second);
res.second = def;
m.inc_ref(def);
m_uf2bvuf.insert(f, res);

return res;
}
4 changes: 1 addition & 3 deletions src/ast/fpa/fpa2bv_converter.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ class fpa2bv_converter {
public:
typedef obj_map<func_decl, std::pair<app *, app *> > special_t;
typedef obj_map<func_decl, expr*> const2bv_t;
typedef obj_map<func_decl, std::pair<func_decl*, expr*> > uf2bvuf_t;
typedef obj_map<func_decl, func_decl*> uf2bvuf_t;

protected:
ast_manager & m;
Expand Down Expand Up @@ -219,8 +219,6 @@ class fpa2bv_converter {
void mk_to_fp_float(sort * s, expr * rm, expr * x, expr_ref & result);

func_decl * mk_bv_uf(func_decl * f, sort * const * domain, sort * range);
void set_bv_def(func_decl * f, expr* def);
expr* get_bv_def(func_decl * f);

expr_ref nan_wrap(expr * n);

Expand Down
46 changes: 46 additions & 0 deletions src/ast/fpa_decl_plugin.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ Revision History:
#include "ast/fpa_decl_plugin.h"
#include "ast/arith_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
#include "ast/ast_smt2_pp.h"

fpa_decl_plugin::fpa_decl_plugin():
m_values(m_fm),
Expand Down Expand Up @@ -68,6 +69,10 @@ void fpa_decl_plugin::recycled_id(unsigned id) {
m_fm.del(m_values[id]);
}

bool fpa_decl_plugin::is_considered_uninterpreted(func_decl * f) {
return false;
}

func_decl * fpa_decl_plugin::mk_numeral_decl(mpf const & v) {
sort * s = mk_float_sort(v.get_ebits(), v.get_sbits());
func_decl * r = nullptr;
Expand Down Expand Up @@ -1044,3 +1049,44 @@ bool fpa_util::contains_floats(ast * a) {

return false;
}

bool fpa_util::is_considered_uninterpreted(func_decl * f, unsigned n, expr* const* args) {
TRACE("fpa_util", expr_ref t(m().mk_app(f, n, args), m()); tout << mk_ismt2_pp(t, m()) << std::endl; );

family_id ffid = plugin().get_family_id();
if (f->get_family_id() != ffid)
return false;

if (is_decl_of(f, ffid, OP_FPA_TO_IEEE_BV)) {
SASSERT(n == 1);
expr* x = args[0];
return is_nan(x);
}
else if (is_decl_of(f, ffid, OP_FPA_TO_SBV) ||
is_decl_of(f, ffid, OP_FPA_TO_UBV)) {
SASSERT(n == 2);
SASSERT(f->get_num_parameters() == 1);
bool is_signed = f->get_decl_kind() == OP_FPA_TO_SBV;
expr* rm = args[0];
expr* x = args[1];
unsigned bv_sz = f->get_parameter(0).get_int();
mpf_rounding_mode rmv;
mpf v;
if (!is_rm_numeral(rm, rmv) || !is_numeral(x, v)) return false;
if (is_nan(x) || is_inf(x)) return true;
unsynch_mpq_manager& mpqm = plugin().fm().mpq_manager();
scoped_mpq r(mpqm);
plugin().fm().to_sbv_mpq(rmv, v, r);
if (is_signed)
return mpqm.bitsize(r) >= bv_sz;
else
return mpqm.is_neg(r) || mpqm.bitsize(r) > bv_sz;
}
else if (is_decl_of(f, ffid, OP_FPA_TO_REAL)) {
SASSERT(n == 1);
expr* x = args[0];
return is_nan(x) || is_inf(x);
}

return plugin().is_considered_uninterpreted(f);
}
6 changes: 4 additions & 2 deletions src/ast/fpa_decl_plugin.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -163,8 +163,6 @@ class fpa_decl_plugin : public decl_plugin {
unsigned mk_id(mpf const & v);
void recycled_id(unsigned id);

bool is_considered_uninterpreted(func_decl * f) override { return false; }

public:
fpa_decl_plugin();

Expand Down Expand Up @@ -199,6 +197,8 @@ class fpa_decl_plugin : public decl_plugin {

void del(parameter const & p) override;
parameter translate(parameter const & p, decl_plugin & target) override;

bool is_considered_uninterpreted(func_decl * f) override;
};

class fpa_util {
Expand Down Expand Up @@ -358,6 +358,8 @@ class fpa_util {

bool contains_floats(ast * a);

bool is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args);

MATCH_TERNARY(is_fp);
};

Expand Down
Loading

0 comments on commit db1d2bb

Please sign in to comment.