mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2015-05-20 10:41:50 -07:00
commit cd8f82ebc2
3 changed files with 7 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3132,14 +3132,16 @@ void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) {
expr * sgn, * sig, * exp;
split_fp(e, sgn, exp, sig);
expr_ref is_special(m), is_denormal(m), p(m);
expr_ref is_special(m), is_denormal(m), p(m), is_zero(m);
mk_is_denormal(e, is_denormal);
mk_is_zero(e, is_zero);
unsigned ebits = m_bv_util.get_bv_size(exp);
p = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits), ebits);
m_simp.mk_eq(exp, p, is_special);
expr_ref or_ex(m);
m_simp.mk_or(is_special, is_denormal, or_ex);
m_simp.mk_or(is_zero, or_ex, or_ex);
m_simp.mk_not(or_ex, result);
}
@ -3351,7 +3353,7 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result)
void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
#ifdef Z3DEBUG
// return;
return;
// CMW: This works only for quantifier-free formulas.
expr_ref new_e(m);
new_e = m.mk_fresh_const(prefix, m.get_sort(e));

4
src/ast/fpa_decl_plugin.cpp
View file

@ -289,7 +289,7 @@ func_decl * fpa_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_param
func_decl * fpa_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
if (arity != 2)
if (arity < 2)
m_manager->raise_exception("invalid number of arguments to floating point relation");
if (domain[0] != domain[1] || !is_float_sort(domain[0]))
m_manager->raise_exception("sort mismatch, expected equal FloatingPoint sorts as arguments");
@ -306,7 +306,7 @@ func_decl * fpa_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_parameter
}
func_decl_info finfo(m_family_id, k);
finfo.set_chainable(true);
return m_manager->mk_func_decl(name, arity, domain, m_manager->mk_bool_sort(), finfo);
return m_manager->mk_func_decl(name, domain[0], domain[1], m_manager->mk_bool_sort(), finfo);
}
func_decl * fpa_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,