From b6d90a64dab39e1b4f9ccf16a5462ee446940ef4 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sat, 21 May 2016 18:07:37 +0100
Subject: [PATCH] fpa rewriter tidy up
---
src/ast/rewriter/fpa_rewriter.cpp | 10 ----------
src/ast/rewriter/fpa_rewriter.h | 1 -
2 files changed, 11 deletions(-)
diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp
index 19b8c3909..b4ae744d3 100644
--- a/src/ast/rewriter/fpa_rewriter.cpp
+++ b/src/ast/rewriter/fpa_rewriter.cpp
@@ -109,8 +109,6 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
st = BR_FAILED;
break;
-
-
default:
NOT_IMPLEMENTED_YET();
}
@@ -892,7 +890,6 @@ br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) {
return BR_FAILED;
}
-
br_status fpa_rewriter::mk_bvwrap(expr * arg, expr_ref & result) {
if (is_app_of(arg, m_util.get_family_id(), OP_FPA_FP)) {
bv_util bu(m());
@@ -923,10 +920,3 @@ br_status fpa_rewriter::mk_bvwrap(expr * arg, expr_ref & result) {
return BR_FAILED;
}
-
-//br_status fpa_rewriter::mk_bvunwrap(expr * arg, expr_ref & result) {
-// if (is_app_of(arg, m_util.get_family_id(), OP_FPA_INTERNAL_BVWRAP))
-// result = to_app(arg)->get_arg(0);
-//
-// return BR_FAILED;
-//}
diff --git a/src/ast/rewriter/fpa_rewriter.h b/src/ast/rewriter/fpa_rewriter.h
index f42d7c719..10f4ab4aa 100644
--- a/src/ast/rewriter/fpa_rewriter.h
+++ b/src/ast/rewriter/fpa_rewriter.h
@@ -91,7 +91,6 @@ public:
br_status mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result);
br_status mk_bvwrap(expr * arg, expr_ref & result);
- br_status mk_bvunwrap(expr * arg, expr_ref & result);
};
#endif