4 files changed, 0 insertions, 99 deletions
diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index 4fd2993ed..bfa577304 100644
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -27,7 +27,6 @@ set(libcvc5parser_src_files
   antlr_input_imports.cpp
   antlr_line_buffered_input.cpp
   antlr_line_buffered_input.h
-  antlr_tracing.h
   bounded_token_buffer.cpp
   bounded_token_buffer.h
   bounded_token_factory.cpp
diff --git a/src/parser/antlr_tracing.h b/src/parser/antlr_tracing.h
deleted file mode 100644
index e9d1d0758..000000000
--- a/src/parser/antlr_tracing.h
+++ /dev/null
@@ -1,92 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Morgan Deters, Mathias Preiner, Aina Niemetz
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * [[ Add one-line brief description here ]]
- *
- * [[ Add lengthier description here ]]
- * \todo document this file
- */
-
-#ifndef CVC5__PARSER__ANTLR_TRACING_H
-#define CVC5__PARSER__ANTLR_TRACING_H
-
-// only enable the hack with -DCVC5_TRACE_ANTLR
-#ifdef CVC5_TRACE_ANTLR
-
-#include <iostream>
-#include <string>
-
-#include "base/output.h"
-
-/* The ANTLR lexer generator, as of v3.2, puts Java trace commands
- * into our beautiful generated C lexer!  How awful!  This is clearly
- * a bug (the parser generator traces with printf()), but we have to
- * do something about it.  Basically, the things look like this:
- *
- *   System.out.println("something"+somethingElse+"another thing");
- *
- * What to do to make this C++?!  Alas, you cannot
- * "#define System.out.println", because it has dots in it.
- * So we do the following.  Sigh.
- *
- * This is all C++, and the generated lexer/parser is C++, but that's
- * ok here, we use the C++ compiler anyway!  Plus, this is only code
- * for **debugging** lexers and parsers.
- */
-
-/** A "System" object, just like in Java! */
-static struct __Cvc5System
-{
-  /**
-   * Helper class just to handle arbitrary string concatenation
-   * with Java syntax.  In C++ you cannot do "char*" + "char*",
-   * so instead we fool the type system into calling
-   * JavaPrinter::operator+() for each item successively.
-   */
-  struct JavaPrinter {
-    template <class T>
-    JavaPrinter operator+(const T& t) const {
-      CVC5Message() << t;
-      return JavaPrinter();
-    }
-  };/* struct JavaPrinter */
-
-  /** A "System.out" object, just like in Java! */
-  struct {
-    /**
-     * By the time println() is called, we've completely
-     * evaluated (and thus printed) its entire argument, thanks
-     * to the call-by-value semantics of C.  All that's left to
-     * do is print the newline.
-     */
-    void println(JavaPrinter) { CVC5Message() << std::endl; }
-  } out;
-} System;
-
-// Now define println(): this kicks off the successive operator+() calls
-// Also define "failed" because ANTLR 3.3 uses "failed" improperly.
-// These are highly dependent on the bugs in a particular ANTLR release.
-// These seem to work with ANTLR 3.3 as of 4/23/2011.  A different trick
-// works with ANTLR 3.2.  EXPECT LOTS OF COMPILER WARNINGS.
-#define println(x)                   \
-  println(({                         \
-    int failed = 0;                  \
-    __Cvc5System::JavaPrinter() + x; \
-  }))
-#undef ANTLR3_FPRINTF
-#define ANTLR3_FPRINTF(args...) {int failed=0;fprintf(args);}
-#undef ANTLR3_PRINTF
-#define ANTLR3_PRINTF(args...) {int failed=0;printf(args);}
-
-#endif /* CVC5_TRACE_ANTLR */
-
-#endif /* CVC5__PARSER__ANTLR_TRACING_H */
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index e60494b7d..4b4b7c10b 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -59,8 +59,6 @@ options {
 #  define ANTLR3_INLINE_INPUT_8BIT
 #endif /* CVC5_COMPETITION_MODE && !CVC5_SMTCOMP_APPLICATION_TRACK */
 
-#include "parser/antlr_tracing.h"
-
 }/* @lexer::includes */
 
 @lexer::postinclude {
@@ -79,7 +77,6 @@ using namespace cvc5::parser;
 #include <memory>
 
 #include "base/check.h"
-#include "parser/antlr_tracing.h"
 #include "parser/parse_op.h"
 #include "parser/parser.h"
 #include "smt/command.h"
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index feaf876f7..9ef04c348 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -58,8 +58,6 @@ options {
  */
 #define ANTLR3_INLINE_INPUT_ASCII
 
-#include "parser/antlr_tracing.h"
-
 }/* @lexer::includes */
 
 @lexer::postinclude {
@@ -92,7 +90,6 @@ using namespace cvc5::parser;
 #include "parser/parse_op.h"
 #include "parser/parser.h"
 #include "parser/tptp/tptp.h"
-#include "parser/antlr_tracing.h"
 
 }/* @parser::includes */