Skip to content

Commit

Permalink
Fix for partially interpreted floating-point functions. Relates to #2596
Browse files Browse the repository at this point in the history 
, #2631.
  • Loading branch information
@wintersteiger
wintersteiger committed Oct 28, 2019
1 parent 1d4f8c0 commit 2308d8a
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);

This comment has been minimized.

Sign in to view

Copy link
@nunoplopes

nunoplopes Oct 28, 2019

Collaborator

Hi @wintersteiger , thanks a lot for the fix! I'm testing it now.
Just one question: could we make this NaN case defined as well? AFAIU, the goal of fpa_to_ieee is to produce an exact BV representation of the FP value. If we leave NaN uninterpreted here, then fpa_to_ieee may yield any value for FP NaN, including BV values that don't correspond to NaN. This semantics is not good (not for my usage, at least). Since otherwise there's no way to produce a BV that corresponds to a NaN (I know there are many; I just need one).
Thanks!

This comment has been minimized.

Sign in to view

Copy link
@wintersteiger

wintersteiger Oct 28, 2019

Author Contributor

This has been added for somebody else's use-case a long time ago, so we'd break theirs. The goal was not to produce a single interpretation for all cases, but a single bit-vector encoded according to IEEE754, which the SMT standard doesn't make easy. We do have the hi_fp_unspecified option, which would fix all unspecified behavior to whatever my preferred value was at the time that I implemented it.

This comment has been minimized.

Sign in to view

Copy link
@nunoplopes

nunoplopes Nov 3, 2019

Collaborator

Thanks! I'm testing this now.
}
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 2308d8a

Please sign in to comment.