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

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-05-22 17:03:37 -07:00
parent c725fe7698 218e47f34b
commit cb6d008da8
11 changed files with 230 additions and 313 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/datatype_decl_plugin.h
View file

@ -109,7 +109,7 @@ public:
parameters[o] - (int) m - number of constructors
parameters[o+1] - (int) k_1 - offset for constructor definition
...
parameters[o+m] - (int) k_m - offset ofr constructor definition
parameters[o+m] - (int) k_m - offset for constructor definition
for each offset k_i at parameters[o+s] for some s in 0..m-1
parameters[k_i] - (symbol) name of the constructor

320
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;
@ -103,7 +103,7 @@ void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) {
m_simp.mk_ite(c, t_sig, f_sig, s);
m_simp.mk_ite(c, t_exp, f_exp, e);
mk_fp(sgn, e, s, result);
result = m_util.mk_fp(sgn, e, s);
}
void fpa2bv_converter::mk_distinct(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
@ -152,7 +152,7 @@ void fpa2bv_converter::mk_numeral(func_decl * f, unsigned num, expr * const * ar
mk_bias(e, biased_exp);
mk_fp(bv_sgn, biased_exp, bv_sig, result);
result = m_util.mk_fp(bv_sgn, biased_exp, bv_sig);
TRACE("fpa2bv_dbg", tout << "value of [" << sign << " " << m_mpz_manager.to_string(sig) << " " << exp << "] is "
<< mk_ismt2_pp(result, m) << std::endl;);
@ -199,7 +199,7 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
SASSERT(m_bv_util.get_bv_size(e) == ebits);
#endif
mk_fp(sgn, e, s, result);
result = m_util.mk_fp(sgn, e, s);
m_const2bv.insert(f, result);
m.inc_ref(f);
@ -218,7 +218,7 @@ void fpa2bv_converter::mk_var(unsigned base_inx, sort * srt, expr_ref & result)
s = m.mk_var(base_inx+1, m_bv_util.mk_sort(sbits-1));
e = m.mk_var(base_inx+2, m_bv_util.mk_sort(ebits));
mk_fp(sgn, e, s, result);
result = m_util.mk_fp(sgn, e, s);
}
void fpa2bv_converter::mk_function_output(sort * rng, func_decl * fbv, expr * const * new_args, expr_ref & result) {
@ -229,176 +229,68 @@ void fpa2bv_converter::mk_function_output(sort * rng, func_decl * fbv, expr * co
app_ref na(m);
na = m.mk_app(fbv, fbv->get_arity(), new_args);
mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, na),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, na),
m_bv_util.mk_extract(sbits - 2, 0, na),
result);
result = m_util.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, na),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, na),
m_bv_util.mk_extract(sbits - 2, 0, na));
}
else if (m_util.is_rm(rng)) {
app_ref na(m);
na = m.mk_app(fbv, fbv->get_arity(), new_args);
mk_rm(na, result);
result = m_util.mk_rm(na);
}
else
result = m.mk_app(fbv, fbv->get_arity(), new_args);
}
sort_ref fpa2bv_converter::replace_float_sorts(sort * s) {
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;
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);
}
else
new_params.push_back(pi);
}
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());
func_decl * fpa2bv_converter::get_bv_uf(func_decl * f, sort * bv_rng, unsigned arity) {
func_decl * res;
if (!m_uf2bvuf.find(f, res)) {
res = m.mk_fresh_func_decl(f->get_name(), symbol("bv"), arity, f->get_domain(), bv_rng);
m_uf2bvuf.insert(f, res);
m.inc_ref(f);
m.inc_ref(res);
TRACE("fpa2bv", tout << "New UF func_decl: " << std::endl << mk_ismt2_pp(res, m) << std::endl;);
}
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);
sort_ref_buffer new_domain(m);
for (unsigned i = 0; i < f->get_arity(); i++) {
sort * di = f->get_domain()[i];
new_domain.push_back(replace_float_sorts(di));
}
func_decl * fd;
if (m_uf2bvuf.find(f, fd))
res = fd;
else {
sort_ref new_range(m);
new_range = replace_float_sorts(f->get_range());
if (f->get_family_id() == null_family_id) {
res = m.mk_fresh_func_decl(f->get_name(), symbol("bv"), new_domain.size(), new_domain.c_ptr(), new_range);
TRACE("fpa2bv", tout << "New UF func_decl: " << std::endl << mk_ismt2_pp(res, m) << std::endl;);
m_uf2bvuf.insert(f, res);
m.inc_ref(f);
m.inc_ref(res);
}
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;);
res = m.mk_func_decl(f->get_family_id(), f->get_decl_kind(),
f->get_num_parameters(), f->get_parameters(),
new_domain.size(), new_domain.c_ptr(), new_range);
TRACE("fpa2bv", tout << "New IF func_decl: " << mk_ismt2_pp(res, m) << std::endl;);
}
}
return res;
}
expr_ref fpa2bv_converter::replace_float_arg(expr * a) {
expr_ref na(m);
switch (a->get_kind()) {
case AST_APP:
if (m_util.is_float(a)) {
SASSERT(m_util.is_fp(a));
expr * sgn, *exp, *sig;
split_fp(a, sgn, exp, sig);
expr * args[3] = { sgn, exp, sig };
na = m_bv_util.mk_concat(3, args);
}
else if (is_rm(a)) {
SASSERT(m_util.is_rm_bvwrap(a));
na = to_app(a)->get_arg(0);
}
else if (m.is_value(a))
na = a;
else {
sort_ref ns(m);
app_ref ar(m);
ar = to_app(a);
func_decl * f = to_app(ar)->get_decl();
func_decl_ref rf(m);
rf = replace_function(f);
na = m.mk_app(rf, ar->get_num_args(), ar->get_args());
}
break;
case AST_VAR:
na = m.mk_var(to_var(a)->get_idx(), replace_float_sorts(m.get_sort(a)));
break;
case AST_QUANTIFIER: {
quantifier * q = to_quantifier(a);
sort * const * srts = q->get_decl_sorts();
vector<sort*> new_sorts;
for (unsigned i = 0; q->get_num_decls(); i++) {
sort_ref ns(m);
ns = replace_float_sorts(q->get_decl_sort(i));
new_sorts.push_back(ns);
}
na = m.mk_quantifier(q->is_forall(),
q->get_num_decls(), new_sorts.c_ptr(),
q->get_decl_names(), q->get_expr(),
q->get_weight(), q->get_qid(), q->get_skid(),
q->get_num_patterns(), q->get_patterns(),
q->get_num_no_patterns(), q->get_no_patterns());
break;
}
case AST_SORT:
case AST_FUNC_DECL:
default:
UNREACHABLE();
}
TRACE("fpa2bv", tout << "arg replaced: " << mk_ismt2_pp(a, m) << " --> " << mk_ismt2_pp(na, m) << std::endl; );
return na;
}
void fpa2bv_converter::mk_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result)
{
TRACE("fpa2bv", tout << "UF: " << mk_ismt2_pp(f, m) << std::endl; );
SASSERT(f->get_arity() == num);
expr_ref_buffer new_args(m);
for (unsigned i = 0; i < num; i++)
new_args.push_back(replace_float_arg(args[i]));
TRACE("fpa2bv", tout << "UF bv-args:";
for (unsigned i = 0; i < num; i++)
tout << " " << mk_ismt2_pp(new_args[i], m);
tout << std::endl; );
func_decl_ref rf(m);
rf = replace_function(f);
mk_function_output(f->get_range(), rf, new_args.c_ptr(), result);
expr_ref fapp(m), feq(m);
sort_ref rng(m);
app_ref bv_app(m), flt_app(m);
rng = f->get_range();
fapp = m.mk_app(f, num, args);
if (m_util.is_float(rng)) {
sort_ref bv_rng(m);
expr_ref new_eq(m);
unsigned ebits = m_util.get_ebits(rng);
unsigned sbits = m_util.get_sbits(rng);
unsigned bv_sz = ebits+sbits;
bv_rng = m_bv_util.mk_sort(bv_sz);
func_decl * bv_f = get_bv_uf(f, bv_rng, num);
bv_app = m.mk_app(bv_f, num, args);
flt_app = m_util.mk_fp(m_bv_util.mk_extract(bv_sz-1, bv_sz-1, bv_app),
m_bv_util.mk_extract(sbits+ebits-2, sbits-1, bv_app),
m_bv_util.mk_extract(sbits-2, 0, bv_app));
new_eq = m.mk_eq(fapp, flt_app);
m_extra_assertions.push_back(new_eq);
result = flt_app;
}
else if (m_util.is_rm(rng)) {
sort_ref bv_rng(m);
expr_ref new_eq(m);
bv_rng = m_bv_util.mk_sort(3);
func_decl * bv_f = get_bv_uf(f, bv_rng, num);
bv_app = m.mk_app(bv_f, num, args);
flt_app = m_util.mk_rm(bv_app);
new_eq = m.mk_eq(fapp, flt_app);
m_extra_assertions.push_back(new_eq);
result = flt_app;
}
else
result = fapp;
TRACE("fpa2bv", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl; );
SASSERT(is_well_sorted(m, result));
@ -423,7 +315,7 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
#endif
, m_bv_util.mk_sort(3));
mk_rm(bv3, result);
result = m_util.mk_rm(bv3);
m_rm_const2bv.insert(f, result);
m.inc_ref(f);
m.inc_ref(result);
@ -444,10 +336,7 @@ void fpa2bv_converter::mk_pinf(sort * s, expr_ref & result) {
unsigned ebits = m_util.get_ebits(s);
expr_ref top_exp(m);
mk_top_exp(ebits, top_exp);
mk_fp(m_bv_util.mk_numeral(0, 1),
top_exp,
m_bv_util.mk_numeral(0, sbits-1),
result);
result = m_util.mk_fp(m_bv_util.mk_numeral(0, 1), top_exp, m_bv_util.mk_numeral(0, sbits-1));
}
void fpa2bv_converter::mk_ninf(func_decl * f, expr_ref & result) {
@ -460,10 +349,7 @@ void fpa2bv_converter::mk_ninf(sort * s, expr_ref & result) {
unsigned ebits = m_util.get_ebits(s);
expr_ref top_exp(m);
mk_top_exp(ebits, top_exp);
mk_fp(m_bv_util.mk_numeral(1, 1),
top_exp,
m_bv_util.mk_numeral(0, sbits-1),
result);
result = m_util.mk_fp(m_bv_util.mk_numeral(1, 1), top_exp, m_bv_util.mk_numeral(0, sbits-1));
}
void fpa2bv_converter::mk_nan(func_decl * f, expr_ref & result) {
@ -476,10 +362,7 @@ void fpa2bv_converter::mk_nan(sort * s, expr_ref & result) {
unsigned ebits = m_util.get_ebits(s);
expr_ref top_exp(m);
mk_top_exp(ebits, top_exp);
mk_fp(m_bv_util.mk_numeral(0, 1),
top_exp,
m_bv_util.mk_numeral(1, sbits - 1),
result);
result = m_util.mk_fp(m_bv_util.mk_numeral(0, 1), top_exp, m_bv_util.mk_numeral(1, sbits - 1));
}
void fpa2bv_converter::mk_nzero(func_decl * f, expr_ref & result) {
@ -492,10 +375,7 @@ void fpa2bv_converter::mk_nzero(sort * s, expr_ref & result) {
unsigned ebits = m_util.get_ebits(s);
expr_ref bot_exp(m);
mk_bot_exp(ebits, bot_exp);
mk_fp(m_bv_util.mk_numeral(1, 1),
bot_exp,
m_bv_util.mk_numeral(0, sbits - 1),
result);
result = m_util.mk_fp(m_bv_util.mk_numeral(1, 1), bot_exp, m_bv_util.mk_numeral(0, sbits - 1));
}
void fpa2bv_converter::mk_pzero(func_decl * f, expr_ref & result) {
@ -508,10 +388,7 @@ void fpa2bv_converter::mk_pzero(sort * s, expr_ref & result) {
unsigned ebits = m_util.get_ebits(s);
expr_ref bot_exp(m);
mk_bot_exp(ebits, bot_exp);
mk_fp(m_bv_util.mk_numeral(0, 1),
bot_exp,
m_bv_util.mk_numeral(0, sbits-1),
result);
result = m_util.mk_fp(m_bv_util.mk_numeral(0, 1), bot_exp, m_bv_util.mk_numeral(0, sbits-1));
}
void fpa2bv_converter::mk_zero(sort * s, expr_ref & sgn, expr_ref & result) {
@ -530,10 +407,7 @@ void fpa2bv_converter::mk_one(sort * s, expr_ref & sign, expr_ref & result) {
SASSERT(is_float(s));
unsigned sbits = m_util.get_sbits(s);
unsigned ebits = m_util.get_ebits(s);
mk_fp(sign,
m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1), ebits),
m_bv_util.mk_numeral(0, sbits-1),
result);
result = m_util.mk_fp(sign, m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1), ebits), m_bv_util.mk_numeral(0, sbits-1));
}
void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits,
@ -813,7 +687,7 @@ void fpa2bv_converter::mk_neg(sort * srt, expr_ref & x, expr_ref & result) {
nsgn = m_bv_util.mk_bv_not(sgn);
expr_ref r_sgn(m);
m_simp.mk_ite(c, sgn, nsgn, r_sgn);
mk_fp(r_sgn, e, sig, result);
result = m_util.mk_fp(r_sgn, e, sig);
}
void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
@ -1230,7 +1104,7 @@ void fpa2bv_converter::mk_abs(func_decl * f, unsigned num, expr * const * args,
SASSERT(num == 1);
expr * sgn, * s, * e;
split_fp(args[0], sgn, e, s);
mk_fp(m_bv_util.mk_numeral(0, 1), e, s, result);
result = m_util.mk_fp(m_bv_util.mk_numeral(0, 1), e, s);
}
void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
@ -1301,14 +1175,8 @@ expr_ref fpa2bv_converter::mk_min_unspecified(func_decl * f, expr * x, expr * y)
}
expr_ref pn(m), np(m);
mk_fp(decls.first,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
pn);
mk_fp(decls.second,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
np);
pn = m_util.mk_fp(decls.first, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1));
np = m_util.mk_fp(decls.second, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1));
expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m);
mk_is_pzero(x, x_is_pzero);
@ -1388,14 +1256,8 @@ expr_ref fpa2bv_converter::mk_max_unspecified(func_decl * f, expr * x, expr * y)
}
expr_ref pn(m), np(m);
mk_fp(decls.first,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
pn);
mk_fp(decls.second,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
np);
pn = m_util.mk_fp(decls.first, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1));
np = m_util.mk_fp(decls.second, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1));
expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m);
mk_is_pzero(x, x_is_pzero);
@ -2286,10 +2148,9 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
int sz = m_bv_util.get_bv_size(bv);
SASSERT((unsigned)sz == to_sbits + to_ebits);
mk_fp(m_bv_util.mk_extract(sz - 1, sz - 1, bv),
m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv),
m_bv_util.mk_extract(sz - to_ebits - 2, 0, bv),
result);
result = m_util.mk_fp(m_bv_util.mk_extract(sz - 1, sz - 1, bv),
m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv),
m_bv_util.mk_extract(sz - to_ebits - 2, 0, bv));
}
else if (num == 2 &&
m_util.is_rm(args[0]) &&
@ -2318,7 +2179,7 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
SASSERT(m_bv_util.get_bv_size(args[0]) == 1);
SASSERT(m_util.get_ebits(f->get_range()) == m_bv_util.get_bv_size(args[1]));
SASSERT(m_util.get_sbits(f->get_range()) == m_bv_util.get_bv_size(args[2])+1);
mk_fp(args[0], args[1], args[2], result);
result = m_util.mk_fp(args[0], args[1], args[2]);
}
else if (num == 3 &&
m_util.is_rm(args[0]) &&
@ -2545,7 +2406,7 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v), ebits);
mk_bias(unbiased_exp, exp);
mk_fp(sgn, exp, sig, result);
result = m_util.mk_fp(sgn, exp, sig);
}
}
else if (m_util.au().is_numeral(x)) {
@ -2578,32 +2439,32 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
sig = m_bv_util.mk_numeral(m_util.fm().sig(v_nta), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nta), ebits);
mk_bias(unbiased_exp, exp);
mk_fp(sgn, exp, sig, v1);
v1 = m_util.mk_fp(sgn, exp, sig);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nte)) ? 1 : 0, 1);
sig = m_bv_util.mk_numeral(m_util.fm().sig(v_nte), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nte), ebits);
mk_bias(unbiased_exp, exp);
mk_fp(sgn, exp, sig, v2);
v2 = m_util.mk_fp(sgn, exp, sig);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1);
sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits);
mk_bias(unbiased_exp, exp);
mk_fp(sgn, exp, sig, v3);
v3 = m_util.mk_fp(sgn, exp, sig);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tn)) ? 1 : 0, 1);
sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tn), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tn), ebits);
mk_bias(unbiased_exp, exp);
mk_fp(sgn, exp, sig, v4);
v4 = m_util.mk_fp(sgn, exp, sig);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1);
sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits);
mk_bias(unbiased_exp, exp);
mk_fp(sgn, exp, sig, result);
result = m_util.mk_fp(sgn, exp, sig);
mk_ite(rm_tn, v4, result, result);
mk_ite(rm_tp, v3, result, result);
mk_ite(rm_nte, v2, result, result);
@ -3344,27 +3205,14 @@ expr_ref fpa2bv_converter::mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sb
return result;
}
void fpa2bv_converter::mk_rm(expr * bv3, expr_ref & result) {
SASSERT(m_bv_util.is_bv(bv3) && m_bv_util.get_bv_size(bv3) == 3);
result = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_RM_BVWRAP, 0, 0, 1, &bv3, m_util.mk_rm_sort());
}
void fpa2bv_converter::mk_fp(expr * sign, expr * exponent, expr * significand, expr_ref & result) {
SASSERT(m_bv_util.is_bv(sign) && m_bv_util.get_bv_size(sign) == 1);
SASSERT(m_bv_util.is_bv(significand));
SASSERT(m_bv_util.is_bv(exponent));
result = m.mk_app(m_util.get_family_id(), OP_FPA_FP, sign, exponent, significand);
}
void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 3);
SASSERT(m_bv_util.get_bv_size(args[0]) == 1);
SASSERT(m_util.get_sbits(f->get_range()) == m_bv_util.get_bv_size(args[2]) + 1);
SASSERT(m_util.get_ebits(f->get_range()) == m_bv_util.get_bv_size(args[1]));
mk_fp(args[0], args[1], args[2], result);
result = m_util.mk_fp(args[0], args[1], args[2]);
TRACE("fpa2bv_mk_fp", tout << "mk_fp result = " << mk_ismt2_pp(result, m) << std::endl;);
}
void fpa2bv_converter::split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const {
SASSERT(m_util.is_fp(e));
SASSERT(to_app(e)->get_num_args() == 3);
@ -3711,7 +3559,7 @@ void fpa2bv_converter::mk_rounding_mode(decl_kind k, expr_ref & result)
default: UNREACHABLE();
}
mk_rm(result, result);
result = m_util.mk_rm(result);
}
void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
@ -4109,7 +3957,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
SASSERT(m_bv_util.get_bv_size(res_exp) == ebits);
SASSERT(is_well_sorted(m, res_exp));
mk_fp(res_sgn, res_exp, res_sig, result);
result = m_util.mk_fp(res_sgn, res_exp, res_sig);
TRACE("fpa2bv_round", tout << "ROUND = " << mk_ismt2_pp(result, m) << std::endl; );
}

20
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;
@ -40,7 +48,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<func_decl, func_decl*> m_uf2bvuf;
obj_map<func_decl, std::pair<app *, app *> > m_specials;
@ -59,12 +67,9 @@ public:
bool is_rm(expr * e) { return is_app(e) && m_util.is_rm(e); }
bool is_rm(sort * s) { return m_util.is_rm(s); }
bool is_float_family(func_decl * f) { return f->get_family_id() == m_util.get_family_id(); }
void mk_rm(expr * bv3, expr_ref & result);
void mk_fp(expr * sign, expr * exponent, expr * significand, expr_ref & result);
void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const;
void split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const;
@ -145,7 +150,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);
@ -190,6 +195,7 @@ protected:
func_decl_ref replace_function(func_decl * f);
expr_ref replace_float_arg(expr * a);
void mk_function_output(sort * rng, func_decl * fbv, expr * const * new_args, expr_ref & result);
func_decl * get_bv_uf(func_decl * f, sort * bv_rng, unsigned arity);
private:
void mk_nan(sort * s, expr_ref & result);

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

@ -56,7 +56,10 @@ bool fpa2bv_rewriter_cfg::max_steps_exceeded(unsigned num_steps) const {
br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
TRACE("fpa2bv_rw", tout << "APP: " << f->get_name() << std::endl; );
TRACE("fpa2bv_rw", tout << "func: " << f->get_name() << std::endl;
tout << "args: " << std::endl;
for (unsigned i = 0; i < num; i++)
tout << mk_ismt2_pp(args[i], m()) << std::endl;);
if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_float(f->get_range())) {
m_conv.mk_const(f, result);
@ -71,7 +74,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 +86,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 +103,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,19 +169,11 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
NOT_IMPLEMENTED_YET();
}
}
else {
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) {
m_conv.mk_function(f, num, args, result);
return BR_DONE;
}
m_conv.mk_function(f, num, args, result);
return BR_DONE;
}
return BR_FAILED;
@ -249,17 +244,15 @@ 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));
new_exp = m_conv.fu().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));
}
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;
}

17
src/ast/fpa_decl_plugin.h
View file

@ -294,7 +294,18 @@ public:
bool is_pzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pzero(v); }
bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nzero(v); }
app * mk_fp(expr * sgn, expr * exp, expr * sig) { return m().mk_app(m_fid, OP_FPA_FP, sgn, exp, sig); }
app * mk_fp(expr * sgn, expr * exp, expr * sig) {
SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1);
SASSERT(m_bv_util.is_bv(exp));
SASSERT(m_bv_util.is_bv(sig));
return m().mk_app(m_fid, OP_FPA_FP, sgn, exp, sig);
}
app * mk_rm(expr * bv3) {
SASSERT(m_bv_util.is_bv(bv3) && m_bv_util.get_bv_size(bv3) == 3);
return m().mk_app(m_fid, OP_FPA_INTERNAL_RM_BVWRAP, 0, 0, 1, &bv3, mk_rm_sort());
}
app * mk_to_fp(sort * s, expr * bv_t) {
SASSERT(is_float(s) && s->get_num_parameters() == 2);
return m().mk_app(m_fid, OP_FPA_TO_FP, 2, s->get_parameters(), 1, &bv_t);
@ -370,7 +381,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

10
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -109,8 +109,6 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
st = BR_FAILED;
break;
default:
NOT_IMPLEMENTED_YET();
}
@ -892,7 +890,6 @@ br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) {
return BR_FAILED;
}
br_status fpa_rewriter::mk_bvwrap(expr * arg, expr_ref & result) {
if (is_app_of(arg, m_util.get_family_id(), OP_FPA_FP)) {
bv_util bu(m());
@ -923,10 +920,3 @@ br_status fpa_rewriter::mk_bvwrap(expr * arg, expr_ref & result) {
return BR_FAILED;
}
//br_status fpa_rewriter::mk_bvunwrap(expr * arg, expr_ref & result) {
// if (is_app_of(arg, m_util.get_family_id(), OP_FPA_INTERNAL_BVWRAP))
// result = to_app(arg)->get_arg(0);
//
// return BR_FAILED;
//}

1
src/ast/rewriter/fpa_rewriter.h
View file

@ -91,7 +91,6 @@ public:
br_status mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result);
br_status mk_bvwrap(expr * arg, expr_ref & result);
br_status mk_bvunwrap(expr * arg, expr_ref & result);
};
#endif

34
src/smt/theory_fpa.cpp
View file

@ -54,10 +54,9 @@ namespace smt {
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);
m_th.m_converter.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),
result);
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);
@ -76,7 +75,7 @@ namespace smt {
SASSERT(is_rm(f->get_range()));
expr_ref bv(m);
bv = m_th.wrap(m.mk_const(f));
mk_rm(bv, result);
result = m_util.mk_rm(bv);
m_rm_const2bv.insert(f, result);
m.inc_ref(f);
m.inc_ref(result);
@ -84,8 +83,8 @@ namespace smt {
}
void theory_fpa::fpa2bv_converter_wrapped::mk_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
return fpa2bv_converter::mk_function(f, num, args, result);
TRACE("t_fpa", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl; );
// Note: this introduces new UFs that should be filtered afterwards.
return fpa2bv_converter::mk_function(f, num, args, result);
}
expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_min_unspecified(func_decl * f, expr * x, expr * y) {
@ -100,10 +99,9 @@ namespace smt {
expr_ref a(m), wrapped(m);
a = m.mk_app(w, x, y);
wrapped = m_th.wrap(a);
m_th.m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, wrapped),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, wrapped),
m_bv_util.mk_extract(sbits - 2, 0, wrapped),
res);
res = m_util.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, wrapped),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, wrapped),
m_bv_util.mk_extract(sbits - 2, 0, wrapped));
expr_ref sc(m);
m_th.m_converter.mk_is_zero(res, sc);
@ -123,10 +121,9 @@ namespace smt {
expr_ref a(m), wrapped(m);
a = m.mk_app(w, x, y);
wrapped = m_th.wrap(a);
m_th.m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, wrapped),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, wrapped),
m_bv_util.mk_extract(sbits - 2, 0, wrapped),
res);
res = m_util.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, wrapped),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, wrapped),
m_bv_util.mk_extract(sbits - 2, 0, wrapped));
expr_ref sc(m);
m_th.m_converter.mk_is_zero(res, sc);
@ -320,8 +317,7 @@ namespace smt {
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));
ast_manager & m = get_manager();
sort * bv_srt = m.get_sort(e);
ast_manager & m = get_manager();
app_ref res(m);
unsigned bv_sz = m_bv_util.get_bv_size(e);
@ -380,7 +376,7 @@ namespace smt {
SASSERT(m_fpa_util.is_rm_bvwrap(e_conv));
expr_ref bv_rm(m);
m_th_rw(to_app(e_conv)->get_arg(0), bv_rm);
m_converter.mk_rm(bv_rm, res);
res = m_fpa_util.mk_rm(bv_rm);
}
else if (m_fpa_util.is_float(e)) {
SASSERT(m_fpa_util.is_fp(e_conv));
@ -389,7 +385,7 @@ namespace smt {
m_th_rw(sgn);
m_th_rw(exp);
m_th_rw(sig);
m_converter.mk_fp(sgn, exp, sig, res);
res = m_fpa_util.mk_fp(sgn, exp, sig);
}
else
UNREACHABLE();

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

@ -55,6 +55,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) {
@ -197,16 +198,25 @@ expr_ref fpa2bv_model_converter::convert_bv2rm(model * bv_mdl, expr * val) {
expr_ref fpa2bv_model_converter::rebuild_floats(model * bv_mdl, sort * s, expr * e) {
expr_ref result(m);
TRACE("fpa2bv_mc", tout << "rebuild floats in " << mk_ismt2_pp(s, m) << " for " << mk_ismt2_pp(e, m) << std::endl;);
if (m_fpa_util.is_float(s)) {
SASSERT(m_bv_util.is_bv(e));
result = convert_bv2fp(bv_mdl, s, e);
if (m_fpa_util.is_numeral(e)) {
result = e;
}
else {
SASSERT(m_bv_util.is_bv(e) && m_bv_util.get_bv_size(e) == (m_fpa_util.get_ebits(s) + m_fpa_util.get_sbits(s)));
result = convert_bv2fp(bv_mdl, s, e);
}
}
else if (m_fpa_util.is_rm(s)) {
SASSERT(m_bv_util.get_bv_size(e) == 3);
result = convert_bv2rm(bv_mdl, e);
if (m_fpa_util.is_rm_numeral(e)) {
result = e;
}
else {
SASSERT(m_bv_util.is_bv(e) && m_bv_util.get_bv_size(e) == 3);
result = convert_bv2rm(bv_mdl, e);
}
}
else if (is_app(e)) {
app * a = to_app(e);
@ -229,6 +239,7 @@ fpa2bv_model_converter::array_model fpa2bv_model_converter::convert_array_func_i
expr_ref as_arr_mdl(m);
as_arr_mdl = bv_mdl->get_const_interp(bv_f);
if (as_arr_mdl == 0) return am;
TRACE("fpa2bv_mc", tout << "arity=0 func_interp for " << mk_ismt2_pp(f, m) << " := " << mk_ismt2_pp(as_arr_mdl, m) << std::endl;);
SASSERT(arr_util.is_as_array(as_arr_mdl));
for (unsigned i = 0; i < arity; i++)
@ -410,9 +421,10 @@ 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);
float_mdl->register_decl(f, val);
if (val) float_mdl->register_decl(f, val);
}
}
else {

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

@ -118,15 +118,14 @@ protected:
func_interp * convert_func_interp(func_decl * f, func_decl * bv_f, model * bv_mdl);
expr_ref rebuild_floats(model * bv_mdl, sort * s, expr * e);
class array_model {
public:
func_decl * new_float_fd;
func_interp * new_float_fi;
func_decl * bv_fd;
expr_ref result;
array_model(ast_manager & m) : result(m) {}
array_model(ast_manager & m) : new_float_fd(0), new_float_fi(0), bv_fd(0), result(m) {}
};
array_model convert_array_func_interp(func_decl * f, func_decl * bv_f, model * bv_mdl);