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.

diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index 4fd2993ed5922c2b1d5f3af5ad7257a59b9ca7b7..bfa577304d8e33f112cc6f994b21a7f420035c4f 100644 (file)
--- 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 (file)
index e9d1d07..0000000
--- 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 e60494b7dd00f592ca78408456b9fc982ae839b9..4b4b7c10bf0c7fff736e5b20f3c84dac2b892c07 100644 (file)
--- 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 feaf876f73db3d65f58a7342b0051c939c0747bb..9ef04c348eea3d53188a64d3dd1163fde2baa610 100644 (file)
--- 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 */