mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

move generic functionality for fpa

Browse source 
move generic functionality for fpa to converter/rewriter so it can be used outside of theory_fpa @wintersteiger
This commit is contained in:
Nikolaj Bjorner 2020-09-30 18:50:07 -07:00
parent 518296dbc1
commit 6708a764f5
6 changed files with 210 additions and 184 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -4254,3 +4254,107 @@ func_decl * fpa2bv_converter::mk_bv_uf(func_decl * f, sort * const * domain, sor
}
return res;
}
void fpa2bv_converter_wrapped::mk_const(func_decl* f, expr_ref& result) {
SASSERT(f->get_family_id() == null_family_id);
SASSERT(f->get_arity() == 0);
expr* r;
if (m_const2bv.find(f, r)) {
result = r;
}
else {
sort* s = f->get_range();
expr_ref bv(m);
bv = wrap(m.mk_const(f));
unsigned bv_sz = m_bv_util.get_bv_size(bv);
unsigned sbits = m_util.get_sbits(s);
SASSERT(bv_sz == m_util.get_ebits(s) + sbits);
result = m_util.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv),
m_bv_util.mk_extract(sbits - 2, 0, bv));
SASSERT(m_util.is_float(result));
m_const2bv.insert(f, result);
m.inc_ref(f);
m.inc_ref(result);
}
}
app_ref fpa2bv_converter_wrapped::wrap(expr* e) {
SASSERT(m_util.is_float(e) || m_util.is_rm(e));
SASSERT(!m_util.is_bvwrap(e));
app_ref res(m);
if (m_util.is_fp(e)) {
expr* cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) };
expr_ref tmp(m_bv_util.mk_concat(3, cargs), m);
m_rw(tmp);
res = to_app(tmp);
}
else {
sort* es = m.get_sort(e);
sort_ref bv_srt(m);
if (is_rm(es))
bv_srt = m_bv_util.mk_sort(3);
else {
SASSERT(m_converter.is_float(es));
unsigned ebits = m_util.get_ebits(es);
unsigned sbits = m_util.get_sbits(es);
bv_srt = m_bv_util.mk_sort(ebits + sbits);
}
func_decl_ref wrap_fd(m);
wrap_fd = m.mk_func_decl(m_util.get_family_id(), OP_FPA_BVWRAP, 0, nullptr, 1, &es, bv_srt);
res = m.mk_app(wrap_fd, e);
}
return res;
}
app_ref fpa2bv_converter_wrapped::unwrap(expr* e, sort* s) {
SASSERT(!m_util.is_fp(e));
SASSERT(m_bv_util.is_bv(e));
SASSERT(m_util.is_float(s) || m_util.is_rm(s));
app_ref res(m);
unsigned bv_sz = m_bv_util.get_bv_size(e);
if (m_util.is_rm(s)) {
SASSERT(bv_sz == 3);
res = m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3)), m_util.mk_round_nearest_ties_to_away(),
m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3)), m_util.mk_round_nearest_ties_to_even(),
m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TO_NEGATIVE, 3)), m_util.mk_round_toward_negative(),
m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)), m_util.mk_round_toward_positive(),
m_util.mk_round_toward_zero()))));
}
else {
SASSERT(m_util.is_float(s));
unsigned sbits = m_util.get_sbits(s);
SASSERT(bv_sz == m_util.get_ebits(s) + sbits);
res = m_util.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, e),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, e),
m_bv_util.mk_extract(sbits - 2, 0, e));
}
return res;
}
void fpa2bv_converter_wrapped::mk_rm_const(func_decl* f, expr_ref& result) {
SASSERT(f->get_family_id() == null_family_id);
SASSERT(f->get_arity() == 0);
expr* r;
if (m_rm_const2bv.find(f, r)) {
result = r;
}
else {
SASSERT(is_rm(f->get_range()));
expr_ref bv(m);
bv = wrap(m.mk_const(f));
result = m_util.mk_bv2rm(bv);
m_rm_const2bv.insert(f, result);
m.inc_ref(f);
m.inc_ref(result);
}
}

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

@ -29,6 +29,7 @@ Notes:
#include "ast/pb_decl_plugin.h"
#include "ast/seq_decl_plugin.h"
#include "ast/rewriter/bool_rewriter.h"
#include "ast/rewriter/th_rewriter.h"
class fpa2bv_converter {
public:
@ -39,7 +40,6 @@ public:
protected:
ast_manager & m;
bool_rewriter m_simp;
fpa_util m_util;
bv_util m_bv_util;
arith_util m_arith_util;
datatype_util m_dt_util;
@ -58,6 +58,8 @@ protected:
friend class bv2fpa_converter;
public:
fpa_util m_util;
fpa2bv_converter(ast_manager & m);
~fpa2bv_converter();
@ -224,3 +226,18 @@ private:
expr_ref extra_quantify(expr * e);
};
class fpa2bv_converter_wrapped : public fpa2bv_converter {
th_rewriter& m_rw;
public:
fpa2bv_converter_wrapped(ast_manager & m, th_rewriter& rw) :
fpa2bv_converter(m),
m_rw(rw) {}
virtual ~fpa2bv_converter_wrapped() {}
void mk_const(func_decl * f, expr_ref & result) override;
void mk_rm_const(func_decl * f, expr_ref & result) override;
app_ref wrap(expr * e);
app_ref unwrap(expr * e, sort * s);
};

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

@ -271,3 +271,77 @@ bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & res
}
template class rewriter_tpl<fpa2bv_rewriter_cfg>;
expr_ref fpa2bv_rewriter::convert_atom(th_rewriter& rw, expr * e) {
TRACE("t_fpa_detail", tout << "converting atom: " << mk_ismt2_pp(e, m) << std::endl;);
expr_ref res(m_cfg.m());
proof_ref pr(m_cfg.m());
(*this)(e, res);
rw(res, res);
SASSERT(is_app(res));
SASSERT(m.is_bool(res));
return res;
}
expr_ref fpa2bv_rewriter::convert_term(th_rewriter& rw, expr * e) {
SASSERT(m_fpa_util.is_rm(e) || m_fpa_util.is_float(e));
ast_manager& m = m_cfg.m();
expr_ref e_conv(m), res(m);
proof_ref pr(m);
(*this)(e, e_conv);
TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, m) << std::endl;
tout << "converted term: " << mk_ismt2_pp(e_conv, m) << std::endl;);
if (m_cfg.m_conv.m_util.is_rm(e)) {
SASSERT(m_cfg.m_conv.m_util.is_bv2rm(e_conv));
expr_ref bv_rm(m);
rw(to_app(e_conv)->get_arg(0), bv_rm);
res = m_cfg.m_conv.m_util.mk_bv2rm(bv_rm);
}
else if (m_cfg.m_conv.m_util.is_float(e)) {
SASSERT(m_cfg.m_conv.m_util.is_fp(e_conv));
expr_ref sgn(m), sig(m), exp(m);
m_cfg.m_conv.split_fp(e_conv, sgn, exp, sig);
rw(sgn);
rw(exp);
rw(sig);
res = m_cfg.m_conv.m_util.mk_fp(sgn, exp, sig);
}
else
UNREACHABLE();
return res;
}
expr_ref fpa2bv_rewriter::convert_conversion_term(th_rewriter& rw, expr * e) {
SASSERT(to_app(e)->get_family_id() == m_cfg.m_conv.m_util.get_family_id());
/* This is for the conversion functions fp.to_* */
expr_ref res(m_cfg.m());
(*this)(e, res);
rw(res, res);
return res;
}
expr_ref fpa2bv_rewriter::convert(th_rewriter& rw, expr * e) {
ast_manager& m = m_cfg.m();
expr_ref res(m);
TRACE("t_fpa", tout << "converting " << mk_ismt2_pp(e, m) << std::endl;);
if (m_cfg.m_conv.m_util.is_fp(e))
res = e;
else if (m.is_bool(e))
res = convert_atom(rw, e);
else if (m_cfg.m_conv.m_util.is_float(e) || m_cfg.m_conv.m_util.is_rm(e))
res = convert_term(rw, e);
else
res = convert_conversion_term(rw, e);
TRACE("t_fpa_detail", tout << "converted; caching:" << std::endl;
tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl <<
mk_ismt2_pp(res, m) << std::endl;);
return res;
}

5
src/ast/fpa/fpa2bv_rewriter.h
View file

@ -74,5 +74,10 @@ struct fpa2bv_rewriter : public rewriter_tpl<fpa2bv_rewriter_cfg> {
rewriter_tpl<fpa2bv_rewriter_cfg>(m, m.proofs_enabled(), m_cfg),
m_cfg(m, c, p) {
}
expr_ref convert_atom(th_rewriter& rw, expr * e);
expr_ref convert_term(th_rewriter& rw, expr * e);
expr_ref convert_conversion_term(th_rewriter& rw, expr * e);
expr_ref convert(th_rewriter& rw, expr * e);
};

175
src/smt/theory_fpa.cpp
View file

@ -42,53 +42,12 @@ namespace smt {
}
};
void theory_fpa::fpa2bv_converter_wrapped::mk_const(func_decl * f, expr_ref & result) {
SASSERT(f->get_family_id() == null_family_id);
SASSERT(f->get_arity() == 0);
expr * r;
if (m_const2bv.find(f, r)) {
result = r;
}
else {
sort * s = f->get_range();
expr_ref bv(m);
bv = m_th.wrap(m.mk_const(f));
unsigned bv_sz = m_th.m_bv_util.get_bv_size(bv);
unsigned sbits = m_th.m_fpa_util.get_sbits(s);
SASSERT(bv_sz == m_th.m_fpa_util.get_ebits(s) + sbits);
result = m_util.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv),
m_bv_util.mk_extract(sbits - 2, 0, bv));
SASSERT(m_th.m_fpa_util.is_float(result));
m_const2bv.insert(f, result);
m.inc_ref(f);
m.inc_ref(result);
}
}
void theory_fpa::fpa2bv_converter_wrapped::mk_rm_const(func_decl * f, expr_ref & result) {
SASSERT(f->get_family_id() == null_family_id);
SASSERT(f->get_arity() == 0);
expr * r;
if (m_rm_const2bv.find(f, r)) {
result = r;
}
else {
SASSERT(is_rm(f->get_range()));
expr_ref bv(m);
bv = m_th.wrap(m.mk_const(f));
result = m_util.mk_bv2rm(bv);
m_rm_const2bv.insert(f, result);
m.inc_ref(f);
m.inc_ref(result);
}
}
theory_fpa::theory_fpa(context& ctx) :
theory(ctx, ctx.get_manager().mk_family_id("fpa")),
m_converter(ctx.get_manager(), this),
m_rw(ctx.get_manager(), m_converter, params_ref()),
m_th_rw(ctx.get_manager()),
m_converter(ctx.get_manager(), m_th_rw),
m_rw(ctx.get_manager(), m_converter, params_ref()),
m_trail_stack(*this),
m_fpa_util(m_converter.fu()),
m_bv_util(m_converter.bu()),
@ -224,117 +183,6 @@ namespace smt {
return result;
}
app_ref theory_fpa::wrap(expr * e) {
SASSERT(m_fpa_util.is_float(e) || m_fpa_util.is_rm(e));
SASSERT(!m_fpa_util.is_bvwrap(e));
app_ref res(m);
if (m_fpa_util.is_fp(e)) {
expr * cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) };
expr_ref tmp(m_bv_util.mk_concat(3, cargs), m);
m_th_rw(tmp);
res = to_app(tmp);
}
else {
sort * es = m.get_sort(e);
sort_ref bv_srt(m);
if (m_converter.is_rm(es))
bv_srt = m_bv_util.mk_sort(3);
else {
SASSERT(m_converter.is_float(es));
unsigned ebits = m_fpa_util.get_ebits(es);
unsigned sbits = m_fpa_util.get_sbits(es);
bv_srt = m_bv_util.mk_sort(ebits + sbits);
}
func_decl_ref wrap_fd(m);
wrap_fd = m.mk_func_decl(get_family_id(), OP_FPA_BVWRAP, 0, nullptr, 1, &es, bv_srt);
res = m.mk_app(wrap_fd, e);
}
return res;
}
app_ref theory_fpa::unwrap(expr * e, sort * s) {
SASSERT(!m_fpa_util.is_fp(e));
SASSERT(m_bv_util.is_bv(e));
SASSERT(m_fpa_util.is_float(s) || m_fpa_util.is_rm(s));
app_ref res(m);
unsigned bv_sz = m_bv_util.get_bv_size(e);
if (m_fpa_util.is_rm(s)) {
SASSERT(bv_sz == 3);
res = m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3)), m_fpa_util.mk_round_nearest_ties_to_away(),
m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3)), m_fpa_util.mk_round_nearest_ties_to_even(),
m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TO_NEGATIVE, 3)), m_fpa_util.mk_round_toward_negative(),
m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)), m_fpa_util.mk_round_toward_positive(),
m_fpa_util.mk_round_toward_zero()))));
}
else {
SASSERT(m_fpa_util.is_float(s));
unsigned sbits = m_fpa_util.get_sbits(s);
SASSERT(bv_sz == m_fpa_util.get_ebits(s) + sbits);
res = m_fpa_util.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, e),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, e),
m_bv_util.mk_extract(sbits - 2, 0, e));
}
return res;
}
expr_ref theory_fpa::convert_atom(expr * e) {
TRACE("t_fpa_detail", tout << "converting atom: " << mk_ismt2_pp(e, m) << std::endl;);
expr_ref res(m);
proof_ref pr(m);
m_rw(e, res);
m_th_rw(res, res);
SASSERT(is_app(res));
SASSERT(m.is_bool(res));
return res;
}
expr_ref theory_fpa::convert_term(expr * e) {
SASSERT(m_fpa_util.is_rm(e) || m_fpa_util.is_float(e));
expr_ref e_conv(m), res(m);
proof_ref pr(m);
m_rw(e, e_conv);
TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, m) << std::endl;
tout << "converted term: " << mk_ismt2_pp(e_conv, m) << std::endl;);
if (m_fpa_util.is_rm(e)) {
SASSERT(m_fpa_util.is_bv2rm(e_conv));
expr_ref bv_rm(m);
m_th_rw(to_app(e_conv)->get_arg(0), bv_rm);
res = m_fpa_util.mk_bv2rm(bv_rm);
}
else if (m_fpa_util.is_float(e)) {
SASSERT(m_fpa_util.is_fp(e_conv));
expr_ref sgn(m), sig(m), exp(m);
m_converter.split_fp(e_conv, sgn, exp, sig);
m_th_rw(sgn);
m_th_rw(exp);
m_th_rw(sig);
res = m_fpa_util.mk_fp(sgn, exp, sig);
}
else
UNREACHABLE();
return res;
}
expr_ref theory_fpa::convert_conversion_term(expr * e) {
SASSERT(to_app(e)->get_family_id() == get_family_id());
/* This is for the conversion functions fp.to_* */
expr_ref res(m);
m_rw(e, res);
m_th_rw(res, res);
return res;
}
expr_ref theory_fpa::convert(expr * e)
{
@ -349,14 +197,7 @@ namespace smt {
mk_ismt2_pp(res, m) << std::endl;);
}
else {
if (m_fpa_util.is_fp(e))
res = e;
else if (m.is_bool(e))
res = convert_atom(e);
else if (m_fpa_util.is_float(e) || m_fpa_util.is_rm(e))
res = convert_term(e);
else
res = convert_conversion_term(e);
res = m_rw.convert(m_th_rw, e);
TRACE("t_fpa_detail", tout << "converted; caching:" << std::endl;
tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl <<
@ -421,7 +262,7 @@ namespace smt {
literal l(ctx.mk_bool_var(atom));
ctx.set_var_theory(l.var(), get_id());
expr_ref bv_atom(convert_atom(atom));
expr_ref bv_atom(m_rw.convert_atom(m_th_rw, atom));
expr_ref bv_atom_w_side_c(m), atom_eq(m);
bv_atom_w_side_c = m.mk_and(bv_atom, mk_side_conditions());
m_th_rw(bv_atom_w_side_c);
@ -486,7 +327,7 @@ namespace smt {
if (!m_fpa_util.is_bv2rm(owner)) {
expr_ref valid(m), limit(m);
limit = m_bv_util.mk_numeral(4, 3);
valid = m_bv_util.mk_ule(wrap(owner), limit);
valid = m_bv_util.mk_ule(m_converter.wrap(owner), limit);
assert_cnstr(valid);
}
}
@ -622,7 +463,7 @@ namespace smt {
if (m_fpa_util.is_float(n) || m_fpa_util.is_rm(n)) {
if (!m_fpa_util.is_fp(n)) {
expr_ref wrapped(m), c(m);
wrapped = wrap(n);
wrapped = m_converter.wrap(n);
mpf_rounding_mode rm;
scoped_mpf val(mpfm);
if (m_fpa_util.is_rm_numeral(n, rm)) {
@ -646,7 +487,7 @@ namespace smt {
}
else {
expr_ref wu(m);
wu = m.mk_eq(unwrap(wrapped, m.get_sort(n)), n);
wu = m.mk_eq(m_converter.unwrap(wrapped, m.get_sort(n)), n);
TRACE("t_fpa", tout << "w/u eq: " << std::endl << mk_ismt2_pp(wu, m) << std::endl;);
assert_cnstr(wu);
}
@ -736,7 +577,7 @@ namespace smt {
model_value_proc * res = nullptr;
app_ref wrapped(m);
wrapped = wrap(owner);
wrapped = m_converter.wrap(owner);
SASSERT(m_bv_util.is_bv(wrapped));
CTRACE("t_fpa_detail", !ctx.e_internalized(wrapped),

17
src/smt/theory_fpa.h
View file

@ -85,16 +85,6 @@ namespace smt {
protected:
typedef trail_stack<theory_fpa> th_trail_stack;
class fpa2bv_converter_wrapped : public fpa2bv_converter {
public:
theory_fpa & m_th;
fpa2bv_converter_wrapped(ast_manager & m, theory_fpa * th) :
fpa2bv_converter(m),
m_th(*th) {}
virtual ~fpa2bv_converter_wrapped() {}
void mk_const(func_decl * f, expr_ref & result) override;
void mk_rm_const(func_decl * f, expr_ref & result) override;
};
class fpa_value_proc : public model_value_proc {
protected:
@ -144,9 +134,9 @@ namespace smt {
};
protected:
th_rewriter m_th_rw;
fpa2bv_converter_wrapped m_converter;
fpa2bv_rewriter m_rw;
th_rewriter m_th_rw;
th_trail_stack m_trail_stack;
fpa_value_factory * m_factory;
fpa_util & m_fpa_util;
@ -184,15 +174,10 @@ namespace smt {
protected:
expr_ref mk_side_conditions();
expr_ref convert(expr * e);
expr_ref convert_atom(expr * e);
expr_ref convert_term(expr * e);
expr_ref convert_conversion_term(expr * e);
void attach_new_th_var(enode * n);
void assert_cnstr(expr * e);
app_ref wrap(expr * e);
app_ref unwrap(expr * e, sort * s);
enode* ensure_enode(expr* e);
enode* get_root(expr* a) { return ensure_enode(a)->get_root(); }