From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 8 Dec 2021 02:51:40 +0000 (-0800)
Subject: FP: Remove static call to Rewriter. (#7765)
X-Git-Tag: cvc5-1.0.0~706
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c02de2447c0eb52a60aa32c9a4c97c530f529c13;p=cvc5.git

FP: Remove static call to Rewriter. (#7765)
---

diff --git a/src/theory/fp/fp_word_blaster.h b/src/theory/fp/fp_word_blaster.h
index f9ec4fd4e..f7c7f26be 100644
--- a/src/theory/fp/fp_word_blaster.h
+++ b/src/theory/fp/fp_word_blaster.h
@@ -34,15 +34,6 @@
 #include "util/floatingpoint_size.h"
 #include "util/hash.h"
 
-#ifdef CVC5_SYM_SYMBOLIC_EVAL
-// This allows debugging of the cvc5 symbolic back-end.
-// By enabling this and disabling constant folding in the rewriter,
-// SMT files that have operations on constants will be evaluated
-// during the encoding step, which means that the expressions
-// generated by the symbolic back-end can be debugged with gdb.
-#include "theory/rewriter.h"
-#endif
-
 namespace cvc5 {
 namespace theory {
 namespace fp {
@@ -100,16 +91,7 @@ typedef traits::bwt bwt;
 class nodeWrapper : public Node
 {
  protected:
-/* CVC5_SYM_SYMBOLIC_EVAL is for debugging cvc5 symbolic back-end issues.
- * Enable this and disabling constant folding will mean that operations
- * that are input with constant args are 'folded' using the symbolic encoding
- * allowing them to be traced via GDB.
- */
-#ifdef CVC5_SYM_SYMBOLIC_EVAL
-  nodeWrapper(const Node& n) : Node(theory::Rewriter::rewrite(n)) {}
-#else
   nodeWrapper(const Node& n) : Node(n) {}
-#endif
 };
 
 class symbolicProposition : public nodeWrapper