mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

FPA: bug and leak fixes

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-12-14 19:09:17 +00:00
parent 4e913bb18c
commit f11ee40c38
7 changed files with 142 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

75
src/ast/float_decl_plugin.cpp
View file

@ -457,22 +457,47 @@ func_decl * float_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, pa
sort * fp = mk_float_sort(ebits, sbits);
symbol name("to_fp");
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
}
else {
// 1 Real -> 1 FP
if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()))
m_manager->raise_exception("expecting two integer parameters to to_fp");
if (arity != 2 && arity != 3)
m_manager->raise_exception("invalid number of arguments to to_fp operator");
if (arity == 3 && domain[2] != m_int_sort)
m_manager->raise_exception("sort mismatch, expected third argument of Int sort");
if (domain[1] != m_real_sort)
m_manager->raise_exception("sort mismatch, expected second argument of Real sort");
}
else if (arity == 3 &&
is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) &&
is_sort_of(domain[1], m_arith_fid, REAL_SORT) &&
is_sort_of(domain[2], m_arith_fid, INT_SORT))
{
// Rounding + 1 Real + 1 Int -> 1 FP
if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()))
m_manager->raise_exception("expecting two integer parameters to to_fp");
sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
symbol name("to_fp");
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
}
else if (arity == 1 &&
is_sort_of(domain[0], m_arith_fid, REAL_SORT))
{
// 1 Real -> 1 FP
if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()))
m_manager->raise_exception("expecting two integer parameters to to_fp");
if (domain[1] != m_real_sort)
m_manager->raise_exception("sort mismatch, expected one argument of Real sort");
sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
symbol name("to_fp");
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
}
else if (arity == 2 &&
is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) &&
is_sort_of(domain[1], m_arith_fid, REAL_SORT))
{
// Rounding + 1 Real -> 1 FP
if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()))
m_manager->raise_exception("expecting two integer parameters to to_fp");
sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
symbol name("to_fp");
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
}
else
NOT_IMPLEMENTED_YET();
}
func_decl * float_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters,
@ -759,6 +784,32 @@ bool float_decl_plugin::is_value(app * e) const {
}
}
bool float_decl_plugin::is_unique_value(app* e) const {
if (e->get_family_id() != m_family_id)
return false;
switch (e->get_decl_kind()) {
case OP_FLOAT_RM_NEAREST_TIES_TO_EVEN:
case OP_FLOAT_RM_NEAREST_TIES_TO_AWAY:
case OP_FLOAT_RM_TOWARD_POSITIVE:
case OP_FLOAT_RM_TOWARD_NEGATIVE:
case OP_FLOAT_RM_TOWARD_ZERO:
return true;
case OP_FLOAT_PLUS_INF: /* No; +oo == fp(#b0 #b11 #b00) */
case OP_FLOAT_MINUS_INF: /* Nol -oo == fp #b1 #b11 #b00) */
case OP_FLOAT_PLUS_ZERO: /* No; +zero == fp #b0 #b00 #b000) */
case OP_FLOAT_MINUS_ZERO: /* No; -zero == fp #b1 #b00 #b000) */
case OP_FLOAT_NAN: /* No; NaN == (fp #b0 #b111111 #b0000001) */
case OP_FLOAT_VALUE: /* above */
return false;
case OP_FLOAT_FP:
return m_manager->is_unique_value(e->get_arg(0)) &&
m_manager->is_unique_value(e->get_arg(1)) &&
m_manager->is_unique_value(e->get_arg(2));
default:
return false;
}
}
float_util::float_util(ast_manager & m):
m_manager(m),
m_fid(m.mk_family_id("float")),

2
src/ast/float_decl_plugin.h
View file

@ -170,7 +170,7 @@ public:
virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
virtual expr * get_some_value(sort * s);
virtual bool is_value(app* e) const;
virtual bool is_unique_value(app* e) const { return is_value(e); }
virtual bool is_unique_value(app* e) const;
mpf_manager & fm() { return m_fm; }
func_decl * mk_value_decl(mpf const & v);

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

@ -1870,6 +1870,12 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
// Just keep it here, as there will be something else that uses it.
mk_triple(args[0], args[1], args[2], result);
}
else if (num == 2 &&
m_bv_util.is_bv(args[0]) &&
m_bv_util.is_bv(args[1]))
{
mk_to_fp_signed(f, num, args, result);
}
else if (num == 3 &&
m_bv_util.is_bv(args[0]) &&
m_arith_util.is_numeral(args[1]) &&
@ -2143,6 +2149,50 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
SASSERT(is_well_sorted(m, result));
}
void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
TRACE("fpa2bv_to_fp_signed", for (unsigned i = 0; i < num; i++)
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
// This is meant to be a conversion from signed bitvector to float:
// ; from signed machine integer, represented as a 2's complement bit vector
// ((_ to_fp eb sb) RoundingMode(_ BitVec m) (_ FloatingPoint eb sb))
// Semantics:
//((_ to_fp eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb)):
// Let b in[[(_ BitVec m)]] and let n be the signed integer represented by b (in 2's complement format).
// [[(_ to_fp eb sb)]](r, b) = +/ -infinity if n is too large / too small to be represented as a finite
// number of [[(_ FloatingPoint eb sb)]]; [[(_ to_fp eb sb)]](r, x) = y otherwise, where y is the finite
// number such that [[fp.to_real]](y) is closest to n according to rounding mode r.
NOT_IMPLEMENTED_YET();
SASSERT(m_util.is_float(f->get_range()));
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
unsigned sz = sbits + ebits;
SASSERT(m_bv_util.get_bv_size(args[0]) == 3);
SASSERT(m_bv_util.get_bv_size(args[1]) == sz);
expr_ref rm(m), x(m);
rm = args[0];
x = args[1];
expr_ref sgn(m), sig(m), exp(m);
sgn = m_bv_util.mk_extract(sz - 1, sz - 1, x);
sig = m_bv_util.mk_extract(sz - ebits - 2, 0, x);
exp = m_bv_util.mk_extract(sz - 2, sz - ebits - 1, x);
round(f->get_range(), rm, sgn, sig, exp, result);
}
void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
TRACE("fpa2bv_to_fp_unsigned", for (unsigned i = 0; i < num; i++)
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
NOT_IMPLEMENTED_YET();
}
void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1);
expr * sgn, * s, * e;

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

@ -121,11 +121,13 @@ public:
void mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_fp_signed(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result);

19
src/ast/rewriter/float_rewriter.cpp
View file

@ -37,6 +37,7 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
SASSERT(f->get_family_id() == get_fid());
switch (f->get_decl_kind()) {
case OP_FLOAT_TO_FP: st = mk_to_fp(f, num_args, args, result); break;
case OP_FLOAT_TO_FP_UNSIGNED: st = mk_to_fp_unsigned(f, num_args, args, result); break;
case OP_FLOAT_ADD: SASSERT(num_args == 3); st = mk_add(args[0], args[1], args[2], result); break;
case OP_FLOAT_SUB: SASSERT(num_args == 3); st = mk_sub(args[0], args[1], args[2], result); break;
case OP_FLOAT_NEG: SASSERT(num_args == 1); st = mk_neg(args[0], result); break;
@ -86,10 +87,10 @@ br_status float_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * cons
return BR_FAILED;
rational q;
mpf q_mpf;
scoped_mpf q_mpf(m_util.fm());
if (m_util.au().is_numeral(args[1], q)) {
TRACE("fp_rewriter", tout << "q: " << q << std::endl; );
mpf v;
scoped_mpf v(m_util.fm());
m_util.fm().set(v, ebits, sbits, rm, q.to_mpq());
result = m_util.mk_value(v);
m_util.fm().del(v);
@ -98,7 +99,7 @@ br_status float_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * cons
}
else if (m_util.is_value(args[1], q_mpf)) {
TRACE("fp_rewriter", tout << "q: " << m_util.fm().to_string(q_mpf) << std::endl; );
mpf v;
scoped_mpf v(m_util.fm());
m_util.fm().set(v, ebits, sbits, rm, q_mpf);
result = m_util.mk_value(v);
m_util.fm().del(v);
@ -126,7 +127,7 @@ br_status float_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * cons
return BR_FAILED;
TRACE("fp_rewriter", tout << "q: " << q << ", e: " << e << "\n";);
mpf v;
scoped_mpf v(m_util.fm());
m_util.fm().set(v, ebits, sbits, rm, q.to_mpq(), e.to_mpq().numerator());
result = m_util.mk_value(v);
m_util.fm().del(v);
@ -137,6 +138,16 @@ br_status float_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * cons
}
}
br_status float_rewriter::mk_to_fp_unsigned(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(f->get_num_parameters() == 2);
SASSERT(f->get_parameter(0).is_int());
SASSERT(f->get_parameter(1).is_int());
unsigned ebits = f->get_parameter(0).get_int();
unsigned sbits = f->get_parameter(1).get_int();
return BR_FAILED;
}
br_status float_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
mpf_rounding_mode rm;
if (m_util.is_rm_value(arg1, rm)) {

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

@ -75,6 +75,7 @@ public:
br_status mk_to_ieee_bv(expr * arg1, expr_ref & result);
br_status mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_to_fp_unsigned(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result);

11
src/smt/theory_fpa.cpp
View file

@ -336,10 +336,13 @@ namespace smt {
<< mk_ismt2_pp(e_exp, m) << "]\n";);
rational sgn_r(0), sig_r(0), exp_r(0);
bv_th->get_fixed_value(e_sgn, sgn_r); // OK to fail
bv_th->get_fixed_value(e_sig, sig_r); // OK to fail
bv_th->get_fixed_value(e_exp, exp_r); // OK to fail
if (ctx.e_internalized(bv_sgn) && ctx.get_enode(bv_sgn)->get_num_th_vars() > 0)
bv_th->get_fixed_value(e_sgn, sgn_r); // OK to fail
if (ctx.e_internalized(bv_sig) && ctx.get_enode(bv_sig)->get_num_th_vars() > 0)
bv_th->get_fixed_value(e_sig, sig_r); // OK to fail
if (ctx.e_internalized(bv_exp) && ctx.get_enode(bv_exp)->get_num_th_vars() > 0)
bv_th->get_fixed_value(e_exp, exp_r); // OK to fail
TRACE("t_fpa", tout << "bv model: [" << sgn_r.to_string() << " "
<< sig_r.to_string() << " "