mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
FPA: improved error messages for to_fp
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
d1cb2566e4
commit
7a15c41c47
|
@ -499,8 +499,19 @@ func_decl * float_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, pa
|
|||
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();
|
||||
else {
|
||||
m_manager->raise_exception("Unexpected argument combination for (_ to_fp eb sb). Supported argument combinations are: "
|
||||
"((_ BitVec 1) (_ BitVec eb) (_ BitVec sb-1)),"
|
||||
"(_ BitVec (eb+sb)),"
|
||||
"(Real),"
|
||||
"(RoundingMode (_ BitVec (eb+sb))),"
|
||||
"(RoundingMode (_ FloatingPoint eb' sb')),"
|
||||
"(RoundingMode Real Int), and"
|
||||
"(RoundingMode Real)."
|
||||
);
|
||||
}
|
||||
|
||||
return 0;
|
||||
}
|
||||
|
||||
func_decl * float_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
|
|
|
@ -239,6 +239,7 @@ public:
|
|||
app * mk_value(mpf const & v) { return m_plugin->mk_value(v); }
|
||||
bool is_value(expr * n) { return m_plugin->is_value(n); }
|
||||
bool is_value(expr * n, mpf & v) { return m_plugin->is_value(n, v); }
|
||||
bool is_rm_value(expr * n) { return m_plugin->is_rm_value(n); }
|
||||
bool is_rm_value(expr * n, mpf_rounding_mode & v) { return m_plugin->is_rm_value(n, v); }
|
||||
|
||||
app * mk_pzero(unsigned ebits, unsigned sbits);
|
||||
|
@ -254,8 +255,7 @@ public:
|
|||
bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_nzero(v); }
|
||||
|
||||
bool is_to_float(expr * n) { return is_app_of(n, m_fid, OP_FLOAT_TO_FP); }
|
||||
|
||||
app * mk_to_float(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_TO_FP, arg1, arg2); }
|
||||
|
||||
app * mk_add(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_ADD, arg1, arg2, arg3); }
|
||||
app * mk_mul(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_MUL, arg1, arg2, arg3); }
|
||||
app * mk_sub(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_SUB, arg1, arg2, arg3); }
|
||||
|
|
Loading…
Reference in a new issue