diff options
Diffstat (limited to 'src/theory/fp/fp_word_blaster.h')
| -rw-r--r-- | src/theory/fp/fp_word_blaster.h | 18 |
1 files changed, 0 insertions, 18 deletions
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 |