Remove antlr_tracing.h (#7608)

This PR removes the long obsolete antlr_tracing.h. The file contains an ugly hack to make lexer tracing work for ANTLR 3.2. It has been obsolete since ANTLR 3.3 (April 2011). Note that the code is only enabled with -DCVC5_TRACE_ANTLR, a flag that is never used.

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 */