From 7a15c41c473152ffd6d83e48133c3dd30b3e67be Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 28 Dec 2014 13:40:36 +0000 Subject: [PATCH] FPA: improved error messages for to_fp Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.cpp | 15 +++++++++++++-- src/ast/float_decl_plugin.h | 4 ++-- 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index d775523ec..846d6ddb7 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -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, diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index e4bf633a5..01daab8e3 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -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); }