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

FPA: standard function names consistency, improved error messages, bugfixes.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-10-22 19:47:50 +01:00
parent 4304012971
commit 31a017e99e
7 changed files with 303 additions and 215 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -136,12 +136,13 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
unsigned sbits = m_util.get_sbits(srt);
expr_ref sgn(m), s(m), e(m);
sort_ref s_sgn(m), s_sig(m), s_exp(m);
s_sgn = m_bv_util.mk_sort(1);
s_sig = m_bv_util.mk_sort(sbits-1);
s_exp = m_bv_util.mk_sort(ebits);
#ifdef Z3DEBUG
sort_ref s_sgn(m), s_sig(m), s_exp(m);
s_sgn = m_bv_util.mk_sort(1);
s_sig = m_bv_util.mk_sort(sbits - 1);
s_exp = m_bv_util.mk_sort(ebits);
std::string p("fpa2bv");
std::string name = f->get_name().str();
@ -149,9 +150,17 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
s = m.mk_fresh_const((p + "_sig_" + name).c_str(), s_sig);
e = m.mk_fresh_const((p + "_exp_" + name).c_str(), s_exp);
#else
sgn = m.mk_fresh_const(0, s_sgn);
s = m.mk_fresh_const(0, s_sig);
e = m.mk_fresh_const(0, s_exp);
expr_ref bv(m);
unsigned bv_sz = 1 + ebits + (sbits - 1);
bv = m.mk_fresh_const(0, m_bv_util.mk_sort(bv_sz));
sgn = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv);
e = m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv);
s = m_bv_util.mk_extract(sbits - 2, 0, bv);
SASSERT(m_bv_util.get_bv_size(sgn) == 1);
SASSERT(m_bv_util.get_bv_size(s) == sbits-1);
SASSERT(m_bv_util.get_bv_size(e) == ebits);
#endif
mk_triple(sgn, s, e, result);
@ -595,12 +604,12 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args,
void fpa2bv_converter::mk_sub(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 3);
expr_ref t(m);
mk_uminus(f, 1, &args[2], t);
mk_neg(f, 1, &args[2], t);
expr * nargs[3] = { args[0], args[1], t };
mk_add(f, 3, nargs, result);
}
void fpa2bv_converter::mk_uminus(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
void fpa2bv_converter::mk_neg(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1);
expr * sgn, * s, * e;
split(args[0], sgn, s, e);
@ -906,7 +915,7 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
TRACE("fpa2bv_div", tout << "DIV = " << mk_ismt2_pp(result, m) << std::endl; );
}
void fpa2bv_converter::mk_remainder(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);
// Remainder is always exact, so there is no rounding mode.
@ -1114,7 +1123,7 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args,
mk_triple(r_sgn, r_sig, r_exp, result);
}
void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 4);
// fusedma means (x * y) + z
@ -1835,9 +1844,18 @@ void fpa2bv_converter::mk_is_subnormal(func_decl * f, unsigned num, expr * const
mk_is_denormal(args[0], result);
}
void fpa2bv_converter::mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
void fpa2bv_converter::mk_is_negative(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1);
mk_is_neg(args[0], result);
TRACE("fpa2bv_is_negative", tout << "result = " << mk_ismt2_pp(result, m) << std::endl;);
}
void fpa2bv_converter::mk_is_positive(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1);
expr_ref t1(m), t2(m);
mk_is_nan(args[0], t1);
mk_is_pos(args[0], t2);
result = m.mk_and(m.mk_not(t1), t2);
}
void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
@ -2123,7 +2141,7 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
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;
split(args[0], sgn, s, e);
split(args[0], sgn, s, e);
result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s);
}
@ -2132,19 +2150,55 @@ void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, e
mk_triple(args[0], args[2], args[1], result);
}
void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
NOT_IMPLEMENTED_YET();
}
void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);
SASSERT(f->get_num_parameters() == 1);
SASSERT(f->get_parameter(0).is_int());
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
int width = f->get_parameter(0).get_int();
expr * rm = args[0];
expr * x = args[1];
expr * sgn, *s, *e;
split(x, sgn, s, e);
NOT_IMPLEMENTED_YET();
}
void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);
SASSERT(f->get_num_parameters() == 1);
SASSERT(f->get_parameter(0).is_int());
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
int width = f->get_parameter(0).get_int();
expr * rm = args[0];
expr * x = args[1];
expr * sgn, *s, *e;
split(x, sgn, s, e);
NOT_IMPLEMENTED_YET();
}
void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1);
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
int width = f->get_parameter(0).get_int();
expr * rm = args[0];
expr * x = args[1];
expr * sgn, *s, *e;
split(x, sgn, s, e);
NOT_IMPLEMENTED_YET();
}

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

@ -94,14 +94,14 @@ public:
void mk_add(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_sub(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_uminus(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_neg(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_div(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_remainder(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_rem(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_abs(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_fusedma(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_round_to_integral(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
@ -114,7 +114,8 @@ public:
void mk_is_zero(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_nzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_pzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_negative(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_positive(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_nan(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result);

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

@ -65,8 +65,6 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
bool max_steps_exceeded(unsigned num_steps) const {
cooperate("fpa2bv");
if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
return num_steps > m_max_steps;
}
@ -117,17 +115,19 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
case OP_FLOAT_VALUE: m_conv.mk_value(f, num, args, result); return BR_DONE;
case OP_FLOAT_PLUS_INF: m_conv.mk_plus_inf(f, result); return BR_DONE;
case OP_FLOAT_MINUS_INF: m_conv.mk_minus_inf(f, result); return BR_DONE;
case OP_FLOAT_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE;
case OP_FLOAT_MINUS_ZERO: m_conv.mk_nzero(f, result); return BR_DONE;
case OP_FLOAT_NAN: m_conv.mk_nan(f, result); return BR_DONE;
case OP_FLOAT_ADD: m_conv.mk_add(f, num, args, result); return BR_DONE;
case OP_FLOAT_SUB: m_conv.mk_sub(f, num, args, result); return BR_DONE;
case OP_FLOAT_UMINUS: m_conv.mk_uminus(f, num, args, result); return BR_DONE;
case OP_FLOAT_NEG: m_conv.mk_neg(f, num, args, result); return BR_DONE;
case OP_FLOAT_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE;
case OP_FLOAT_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE;
case OP_FLOAT_REM: m_conv.mk_remainder(f, num, args, result); return BR_DONE;
case OP_FLOAT_REM: m_conv.mk_rem(f, num, args, result); return BR_DONE;
case OP_FLOAT_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE;
case OP_FLOAT_MIN: m_conv.mk_min(f, num, args, result); return BR_DONE;
case OP_FLOAT_MAX: m_conv.mk_max(f, num, args, result); return BR_DONE;
case OP_FLOAT_FUSED_MA: m_conv.mk_fusedma(f, num, args, result); return BR_DONE;
case OP_FLOAT_FMA: m_conv.mk_fma(f, num, args, result); return BR_DONE;
case OP_FLOAT_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE;
case OP_FLOAT_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE;
case OP_FLOAT_EQ: m_conv.mk_float_eq(f, num, args, result); return BR_DONE;
@ -142,18 +142,18 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
case OP_FLOAT_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_POSITIVE: m_conv.mk_is_positive(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_NEGATIVE: m_conv.mk_is_negative(f, num, args, result); return BR_DONE;
case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE;
case OP_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
case OP_FLOAT_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
case OP_FLOAT_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE;
case OP_FLOAT_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE;
case OP_FLOAT_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE;
case OP_FLOAT_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
case OP_FLOAT_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
default:
TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
throw tactic_exception("NYI");
NOT_IMPLEMENTED_YET();
}
}