mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Partial support for fpa2bv translation in complex types.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-05-21 18:08:48 +01:00
parent b6d90a64da
commit fe3f8466b6
7 changed files with 266 additions and 70 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

191
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -33,6 +33,9 @@ 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()),
m_mpz_manager(m_mpf_manager.mpz_manager()),
m_hi_fp_unspecified(true),
@ -46,11 +49,10 @@ fpa2bv_converter::~fpa2bv_converter() {
void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
if (is_float(a) && is_float(b)) {
SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FPA_FP));
SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_FP));
SASSERT(m_util.is_fp(a) && m_util.is_fp(b));
TRACE("fpa2bv", tout << "mk_eq a=" << mk_ismt2_pp(a, m) << std::endl;
tout << "mk_eq b=" << mk_ismt2_pp(b, m) << std::endl;);
tout << "mk_eq b=" << mk_ismt2_pp(b, m) << std::endl;);
expr_ref eq_sgn(m), eq_exp(m), eq_sig(m);
m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), eq_sgn);
@ -77,11 +79,10 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
m_simp.mk_or(both_are_nan, both_the_same, result);
}
else if (is_rm(a) && is_rm(b)) {
SASSERT(m_util.is_rm_bvwrap(b));
SASSERT(m_util.is_rm_bvwrap(a));
SASSERT(m_util.is_rm_bvwrap(b) && m_util.is_rm_bvwrap(a));
TRACE("fpa2bv", tout << "mk_eq_rm a=" << mk_ismt2_pp(a, m) << std::endl;
tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;);
tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;);
m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), result);
}
@ -90,8 +91,7 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
}
void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) {
SASSERT(is_app_of(t, m_plugin->get_family_id(), OP_FPA_FP));
SASSERT(is_app_of(f, m_plugin->get_family_id(), OP_FPA_FP));
SASSERT(m_util.is_fp(t) && m_util.is_fp(f));
expr *t_sgn, *t_sig, *t_exp;
expr *f_sgn, *f_sig, *f_exp;
@ -244,46 +244,119 @@ void fpa2bv_converter::mk_function_output(sort * rng, func_decl * fbv, expr * co
}
sort_ref fpa2bv_converter::replace_float_sorts(sort * s) {
sort_ref ns(m);
sort_ref ns(m);
if (m_util.is_float(s))
ns = m_bv_util.mk_sort(m_util.get_sbits(s) + m_util.get_ebits(s));
else if (m_util.is_rm(s))
ns = m_bv_util.mk_sort(3);
else
ns = s;
sort * found_sort;
if (m_subst_sorts.find(s, found_sort)) {
ns = found_sort;
}
else {
if (m_util.is_float(s))
ns = m_bv_util.mk_sort(m_util.get_sbits(s) + m_util.get_ebits(s));
else if (m_util.is_rm(s))
ns = m_bv_util.mk_sort(3);
else if (m_array_util.is_array(s)) {
SASSERT(s->get_num_parameters() > 0);
vector<parameter> new_params;
unsigned num_params = s->get_num_parameters();
for (unsigned i = 0; i < num_params; i++)
{
parameter const & pi = s->get_parameter(i);
if (pi.is_ast() && is_sort(pi.get_ast())) {
sort_ref nsrt(m);
nsrt = replace_float_sorts(to_sort(pi.get_ast()));
parameter np((ast*)nsrt);
new_params.push_back(np);
}
else
new_params.push_back(pi);
}
ns = m.mk_sort(s->get_family_id(), s->get_decl_kind(), new_params.size(), new_params.c_ptr());
}
else if (m_dt_util.is_datatype(s)) {
TRACE("fpa2bv", tout << "datatype:"; m_dt_util.display_datatype(s, tout); );
bool is_recursive = m_dt_util.is_recursive(s);
SASSERT(!is_recursive);
ptr_vector<func_decl> const * cs = m_dt_util.get_datatype_constructors(s);
ptr_vector<constructor_decl> new_css;
bool has_news = false;
for (unsigned i = 0; i < cs->size(); i++) {
func_decl * cf = cs->get(i);
func_decl * rf = m_dt_util.get_constructor_recognizer(cf);
ptr_vector<func_decl> new_rf;
ptr_vector<func_decl> const * cas = m_dt_util.get_constructor_accessors(cf);
ptr_vector<accessor_decl> new_cas;
for (unsigned j = 0; j < cas->size(); j++) {
func_decl * ca = cas->get(j);
sort * s1 = ca->get_range();
sort_ref s1r(m);
s1r = replace_float_sorts(s1);
if (ns->get_num_parameters() != 0) {
vector<parameter> new_params;
unsigned num_params = ns->get_num_parameters();
for (unsigned i = 0; i < num_params; i++)
{
parameter const & pi = ns->get_parameter(i);
if (pi.is_ast() && pi.get_ast()->get_kind() == AST_SORT) {
sort_ref nsrt(m);
nsrt = replace_float_sorts(to_sort(pi.get_ast()));
parameter np = parameter((ast*)nsrt);
new_params.push_back(np);
symbol name(ca->get_name());
if (s1r != s1) {
std::stringstream ss;
ss << name << "!fpa2bv";
name = symbol(ss.str().c_str());
has_news = true;
}
accessor_decl * ad = mk_accessor_decl(name, type_ref(s1r));
new_cas.push_back(ad);
}
constructor_decl * cd = 0;
symbol name(cf->get_name());
symbol rf_name(rf->get_name());
if (has_news) {
std::stringstream ss;
ss << name << "!fpa2bv";
name = symbol(ss.str().c_str());
std::stringstream ss2;
ss2 << rf_name << "!fpa2bv";
rf_name = symbol(ss2.str().c_str());
}
cd = mk_constructor_decl(name, rf_name, new_cas.size(), new_cas.c_ptr());
new_css.push_back(cd);
}
if (has_news) {
std::stringstream ss;
ss << s->get_name() << "!fpa2bv";
symbol name(ss.str().c_str());
datatype_decl * dtd = mk_datatype_decl(name, new_css.size(), new_css.c_ptr());
datatype_decl_plugin * dtp = static_cast<datatype_decl_plugin*>(m.get_plugin(m.mk_family_id("datatype")));
sort_ref_vector sorts(m);
bool is_ok = dtp->mk_datatypes(1, &dtd, sorts);
SASSERT(is_ok);
ns = sorts.get(0);
TRACE("fpa2bv", tout << "new datatype:"; m_dt_util.display_datatype(ns, tout); );
}
else
new_params.push_back(pi);
ns = s;
}
else if (m_seq_util.is_seq(s)) {
NOT_IMPLEMENTED_YET();
}
else
ns = s;
TRACE("fpa2bv", tout << "New sort params:";
for (unsigned i = 0; i < new_params.size(); i++)
tout << " " << new_params[i];
tout << std::endl;);
ns = m.mk_sort(ns->get_family_id(), ns->get_decl_kind(), new_params.size(), new_params.c_ptr());
if (ns != s) {
m_subst_sorts.insert(s, ns);
m.inc_ref(s);
m.inc_ref(ns);
}
}
SASSERT(ns != 0);
TRACE("fpa2bv", tout << "sorts replaced: " << mk_ismt2_pp(s, m) << " --> " << mk_ismt2_pp(ns, m) << std::endl; );
return ns;
}
func_decl_ref fpa2bv_converter::replace_function(func_decl * f) {
TRACE("fpa2bv", tout << "replacing: " << mk_ismt2_pp(f, m) << std::endl;);
func_decl_ref res(m);
func_decl_ref res(m);
sort_ref_buffer new_domain(m);
for (unsigned i = 0; i < f->get_arity(); i++) {
@ -308,18 +381,44 @@ func_decl_ref fpa2bv_converter::replace_function(func_decl * f) {
}
else
{
TRACE("fpa2bv", tout << "New domain:";
for (unsigned i = 0; i < new_domain.size(); i++)
tout << " " << mk_ismt2_pp(new_domain[i], m);
tout << std::endl;);
TRACE("fpa2bv", tout << "Old domain:" << std::endl;
for (unsigned i = 0; i < f->get_arity(); i++) {
if (m_dt_util.is_datatype(f->get_domain(i)))
m_dt_util.display_datatype(f->get_domain(i), tout);
else
tout << mk_ismt2_pp(f->get_domain(i), m);
tout << std::endl;
});
TRACE("fpa2bv", tout << "New domain:" << std::endl;
for (unsigned i = 0; i < new_domain.size(); i++) {
if (m_dt_util.is_datatype(new_domain[i]))
m_dt_util.display_datatype(new_domain[i], tout);
else
tout << mk_ismt2_pp(new_domain[i], m);
tout << std::endl;
});
vector<parameter> new_params;
for (unsigned i = 0; i < f->get_num_parameters(); i++) {
parameter const & pi = f->get_parameter(i);
if (pi.is_ast() && is_sort(pi.get_ast())) {
sort_ref ns(m);
ns = replace_float_sorts(to_sort(pi.get_ast()));
parameter np((ast*)ns);
new_params.push_back(np);
}
else
new_params.push_back(pi);
}
res = m.mk_func_decl(f->get_family_id(), f->get_decl_kind(),
f->get_num_parameters(), f->get_parameters(),
new_params.size(), new_params.c_ptr(),
new_domain.size(), new_domain.c_ptr(), new_range);
TRACE("fpa2bv", tout << "New IF func_decl: " << mk_ismt2_pp(res, m) << std::endl;);
TRACE("fpa2bv", tout << "IF func_decl: " << mk_ismt2_pp(res, m) << std::endl;);
}
}
return res;
}
@ -391,7 +490,8 @@ void fpa2bv_converter::mk_function(func_decl * f, unsigned num, expr * const * a
for (unsigned i = 0; i < num; i++)
new_args.push_back(replace_float_arg(args[i]));
TRACE("fpa2bv", tout << "UF bv-args:";
CTRACE("fpa2bv", num > 0, tout << "UF bv-args:";
for (unsigned i = 0; i < num; i++)
tout << " " << mk_ismt2_pp(new_args[i], m);
tout << std::endl; );
@ -400,7 +500,11 @@ void fpa2bv_converter::mk_function(func_decl * f, unsigned num, expr * const * a
rf = replace_function(f);
mk_function_output(f->get_range(), rf, new_args.c_ptr(), result);
TRACE("fpa2bv", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl; );
TRACE("fpa2bv", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl;
tout << "old: " << mk_ismt2_pp(f->get_range(), m) << std::endl;
tout << "new: " << mk_ismt2_pp(m.get_sort(result), m) << std::endl;
tout << "equal: " << (f->get_range() == m.get_sort(result)) << std::endl;);
SASSERT(is_well_sorted(m, result));
}
@ -4118,6 +4222,7 @@ 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);
dec_ref_map_key_values(m, m_subst_sorts);
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.end();
it++) {

11
src/ast/fpa/fpa2bv_converter.h
View file

@ -24,6 +24,11 @@ Notes:
#include"ref_util.h"
#include"fpa_decl_plugin.h"
#include"bv_decl_plugin.h"
#include"array_decl_plugin.h"
#include"datatype_decl_plugin.h"
#include"dl_decl_plugin.h"
#include"pb_decl_plugin.h"
#include"seq_decl_plugin.h"
#include"basic_simplifier_plugin.h"
class fpa2bv_converter {
@ -33,6 +38,9 @@ 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;
unsynch_mpz_manager & m_mpz_manager;
fpa_decl_plugin * m_plugin;
@ -41,6 +49,7 @@ protected:
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<sort, sort*> m_subst_sorts;
obj_map<func_decl, std::pair<app *, app *> > m_specials;
@ -145,7 +154,7 @@ public:
expr_ref_vector m_extra_assertions;
bool is_special(func_decl * f) { return m_specials.contains(f); }
bool is_uf2bvuf(func_decl * f) { return m_uf2bvuf.contains(f); }
bool is_uf2bvuf(func_decl * f) { return m_uf2bvuf.contains(f); }
protected:
void mk_one(func_decl *f, expr_ref & sign, expr_ref & result);

40
src/ast/fpa/fpa2bv_rewriter.cpp
View file

@ -71,7 +71,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
if (m().is_eq(f)) {
SASSERT(num == 2);
TRACE("fpa2bv_rw", tout << "(= " << mk_ismt2_pp(args[0], m()) << " " <<
mk_ismt2_pp(args[1], m()) << ")" << std::endl;);
mk_ismt2_pp(args[1], m()) << ")" << std::endl;);
SASSERT(m().get_sort(args[0]) == m().get_sort(args[1]));
sort * ds = f->get_domain()[0];
if (m_conv.is_float(ds)) {
@ -83,7 +83,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
return BR_DONE;
}
return BR_FAILED;
}
}
else if (m().is_ite(f)) {
SASSERT(num == 3);
if (m_conv.is_float(args[1])) {
@ -100,7 +100,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
}
return BR_FAILED;
}
if (m_conv.is_float_family(f)) {
switch (f->get_decl_kind()) {
case OP_FPA_RM_NEAREST_TIES_TO_AWAY:
@ -166,16 +166,9 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
NOT_IMPLEMENTED_YET();
}
}
else {
SASSERT(!m_conv.is_float_family(f));
bool is_float_uf = m_conv.is_float(f->get_range()) || m_conv.is_rm(f->get_range());
for (unsigned i = 0; i < f->get_arity(); i++) {
sort * di = f->get_domain()[i];
is_float_uf |= m_conv.is_float(di) || m_conv.is_rm(di);
}
if (is_float_uf) {
else if (f->get_arity() > 0 && !m_conv.is_float_family(f)) {
expr_ref q(m().mk_app(f, num, args), m());
if (m_conv.fu().contains_floats(q)) {
m_conv.mk_function(f, num, args, result);
return BR_DONE;
}
@ -249,17 +242,16 @@ bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & res
expr_ref new_exp(m());
sort * s = t->get_sort();
if (m_conv.is_float(s))
{
expr_ref new_var(m());
unsigned ebits = m_conv.fu().get_ebits(s);
unsigned sbits = m_conv.fu().get_sbits(s);
new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits));
m_conv.mk_fp(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var),
m_conv.bu().mk_extract(ebits - 1, 0, new_var),
m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var),
new_exp);
}
if (m_conv.is_float(s)) {
expr_ref new_var(m());
unsigned ebits = m_conv.fu().get_ebits(s);
unsigned sbits = m_conv.fu().get_sbits(s);
new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits));
m_conv.mk_fp(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var),
m_conv.bu().mk_extract(ebits - 1, 0, new_var),
m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var),
new_exp);
}
else
new_exp = m().mk_var(t->get_idx(), s);

63
src/ast/fpa_decl_plugin.cpp
View file

@ -691,7 +691,7 @@ func_decl * fpa_decl_plugin::mk_internal_rm(decl_kind k, unsigned num_parameters
}
func_decl * fpa_decl_plugin::mk_internal_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
unsigned arity, sort * const * domain, sort * range) {
if (arity != 1)
m_manager->raise_exception("invalid number of arguments to bv_wrap");
if (!is_float_sort(domain[0]) && !is_rm_sort(domain[0]))
@ -1076,3 +1076,64 @@ app * fpa_util::mk_internal_to_real_unspecified(unsigned ebits, unsigned sbits)
sort * range = m_a_util.mk_real();
return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED, 2, ps, 0, 0, range);
}
bool fpa_util::contains_floats(ast * a) {
switch (a->get_kind()) {
case AST_APP: {
app * aa = to_app(a);
if (contains_floats(aa->get_decl()))
return true;
else
for (unsigned i = 0; i < aa->get_num_args(); i++)
if (contains_floats(aa->get_arg(i)))
return true;
break;
}
case AST_VAR:
return contains_floats(to_var(a)->get_sort());
break;
case AST_QUANTIFIER: {
quantifier * q = to_quantifier(a);
for (unsigned i = 0; i < q->get_num_children(); i++)
if (contains_floats(q->get_child(i)))
return true;
for (unsigned i = 0; i < q->get_num_decls(); i++)
if (contains_floats(q->get_decl_sort(i)))
return true;
if (contains_floats(q->get_expr()))
return true;
break;
}
case AST_SORT: {
sort * s = to_sort(a);
if (is_float(s) || is_rm(s))
return true;
else {
for (unsigned i = 0; i < s->get_num_parameters(); i++) {
parameter const & pi = s->get_parameter(i);
if (pi.is_ast() && contains_floats(pi.get_ast()))
return true;
}
}
break;
}
case AST_FUNC_DECL: {
func_decl * f = to_func_decl(a);
for (unsigned i = 0; i < f->get_arity(); i++)
if (contains_floats(f->get_domain(i)))
return true;
if (contains_floats(f->get_range()))
return true;
for (unsigned i = 0; i < f->get_num_parameters(); i++) {
parameter const & pi = f->get_parameter(i);
if (pi.is_ast() && contains_floats(pi.get_ast()))
return true;
}
break;
}
default:
UNREACHABLE();
}
return false;
}

4
src/ast/fpa_decl_plugin.h
View file

@ -370,7 +370,9 @@ public:
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_rm_bvwrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_RM_BVWRAP); }
bool is_rm_bvwrap(func_decl * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_RM_BVWRAP; }
bool is_rm_bvwrap(func_decl * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_RM_BVWRAP; }
bool contains_floats(ast * a);
};
#endif

17
src/tactic/fpa/fpa2bv_model_converter.cpp
View file

@ -46,6 +46,12 @@ 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<sort, sort*>::iterator it = m_subst_sorts.begin();
it != m_subst_sorts.end();
it++) {
out << "\n " << mk_ismt2_pp(it->m_key, m) << " -> ";
out << mk_ismt2_pp(it->m_value, m);
}
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.end();
it++) {
@ -55,6 +61,7 @@ void fpa2bv_model_converter::display(std::ostream & out) {
out << mk_ismt2_pp(it->m_value.first, m, indent) << "; " <<
mk_ismt2_pp(it->m_value.second, m, indent) << ")";
}
out << ")";
}
model_converter * fpa2bv_model_converter::translate(ast_translation & translator) {
@ -88,6 +95,15 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator
translator.to().inc_ref(k);
translator.to().inc_ref(v);
}
for (obj_map<sort, sort*>::iterator it = m_subst_sorts.begin();
it != m_subst_sorts.end();
it++) {
sort * k = translator(it->m_key);
sort * v = translator(it->m_value);
res->m_subst_sorts.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++) {
@ -410,6 +426,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
}
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);

10
src/tactic/fpa/fpa2bv_model_converter.h
View file

@ -32,6 +32,7 @@ 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_map<sort, sort*> m_subst_sorts;
obj_map<func_decl, std::pair<app*, app*> > m_specials;
public:
@ -64,6 +65,14 @@ public:
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
}
for (obj_map<sort, sort*>::iterator it = conv.m_subst_sorts.begin();
it != conv.m_subst_sorts.end();
it++)
{
m_subst_sorts.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_specials.begin();
it != conv.m_specials.end();
it++) {
@ -78,6 +87,7 @@ 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_map_key_values(m, m_subst_sorts);
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
it != m_specials.end();
it++) {