16 files changed, 15 insertions, 154 deletions
diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index d7491f8ca..d79d7b22c 100644
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -18,7 +18,6 @@ set(libcvc4parser_src_files
   antlr_line_buffered_input.cpp
   antlr_line_buffered_input.h
   antlr_tracing.h
-  antlr_undefines.h
   bounded_token_buffer.cpp
   bounded_token_buffer.h
   bounded_token_factory.cpp
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index fe80d0322..a2885d1b6 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -15,11 +15,8 @@
  **/
 
 #include "parser/antlr_input.h"
-// We rely on the inclusion of #include <antlr3.h> in "parser/antlr_input.h".
-// This is avoid having to undefine the symbols in <antlr3.h>.
-// See the documentation in "parser/antlr_undefines.h" for more
-// details.
 
+#include <antlr3.h>
 #include <limits.h>
 #include <stdint.h>
 
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 5598dd359..576b693e8 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -17,14 +17,9 @@
 #ifndef __CVC4__PARSER__ANTLR_INPUT_H
 #define __CVC4__PARSER__ANTLR_INPUT_H
 
-// These headers must be included first. See the documentation
-// in parser/antlr_undefines.h for an explanation.
-// Also while unusual this must also be within the #ifdef guard.
-#include <antlr3.h>
-#include "parser/antlr_undefines.h"
-
 #include "cvc4parser_private.h"
 
+#include <antlr3.h>
 #include <iostream>
 #include <sstream>
 #include <stdexcept>
diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp
index 0f746cfbb..91ced0f41 100644
--- a/src/parser/antlr_input_imports.cpp
+++ b/src/parser/antlr_input_imports.cpp
@@ -51,11 +51,7 @@
 
 
 
-// These headers must be the first two included.
-// See the documentation in "parser/antlr_undefines.h" for more details.
 #include <antlr3.h>
-#include "parser/antlr_undefines.h"
-
 #include <sstream>
 
 #include "parser/antlr_input.h"
diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp
index a2ca0de78..356663559 100644
--- a/src/parser/antlr_line_buffered_input.cpp
+++ b/src/parser/antlr_line_buffered_input.cpp
@@ -28,14 +28,9 @@
  ** are not split across multiple lines).
  **/
 
-// We rely on the inclusion of #include <antlr3.h> in
-//   "parser/antlr_line_buffered_input.h".
-// This is avoid having to undefine the symbols in <antlr3.h>.
-// See the documentation in "parser/antlr_undefines.h" for more
-// details.
-
 #include "parser/antlr_line_buffered_input.h"
 
+#include <antlr3.h>
 #include <iostream>
 #include <string>
 #include <cassert>
diff --git a/src/parser/antlr_line_buffered_input.h b/src/parser/antlr_line_buffered_input.h
index 8253a9c3f..c33566e22 100644
--- a/src/parser/antlr_line_buffered_input.h
+++ b/src/parser/antlr_line_buffered_input.h
@@ -20,16 +20,12 @@
  ** achieve that and stores the lines received so far in a LineBuffer.
  **/
 
-// These headers should be the first two included.
-// See the documentation in "parser/antlr_undefines.h" for more details.
-#include <antlr3.h>
-#include "parser/antlr_undefines.h"
-
 #include "cvc4parser_private.h"
 
 #ifndef __CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H
 #define __CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H
 
+#include <antlr3.h>
 #include <istream>
 
 #include "parser/line_buffer.h"
diff --git a/src/parser/antlr_undefines.h b/src/parser/antlr_undefines.h
deleted file mode 100644
index 20df6dbc7..000000000
--- a/src/parser/antlr_undefines.h
+++ /dev/null
@@ -1,69 +0,0 @@
-/*********************                                                        */
-/*! \file antlr_undefines.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 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.\endverbatim
- **
- ** \brief Every usage undefines standard autotools macro names.
- **
- ** This header is very sensitive and it should be understood *in full* before
- ** it is used or *moved* in position relative to other headers.
- **
- ** Including this header runs #undef on the following identifiers:
- ** - PACKAGE_BUGREPORT,
- ** - PACKAGE_NAME
- ** - PACKAGE_STRING
- ** - PACKAGE_TARNAME
- ** - PACKAGE_VERSION
- **
- ** This is to solves a problem caused by antlr and cvc4 both defining these
- ** symbols. This has to do with both packages using autotools in a slightly
- ** dicey way. This was reported by us a long time ago, but most versions
- ** of libantlr are quite old (3.2).
- ** http://www.antlr3.org/pipermail/antlr-interest/2010-March/037859.html
- **
- ** The source of both of these two definitions are given below.
- **
- ** From antlr, the autogenerated antlr lexers and parsers include antlr3.h.
- ** The chain of inclusions is:
- **  Lang{Lexer,Parser}.h -> <antlr3.h> -> <antlr3config.h> -> <antlr3defs.h>
- **
- ** where Lang is in {Smt1,Smt2,Tptp,Cvc}.
- **
- ** From CVC4, the parsers use Debug("...") and other features from
- ** "base/output.h". This is a cvc4_private_library.h header file. This means
- ** the files is usable while building the driver and parsers, but is otherwise
- ** conceptually the same as a cvc4_private.h header. (If that sounds sketchy,
- ** it is sure is! [See src/DESIGN.txt for more details].)
- ** The include chain is then
- **  "base/output.h" -> "cvc4_private_library.h" -> "cvc4_private.h" ->
- **     "cvc4autoconfig.h".
- ** The file cvc4autoconfig.h is autogenerated by autotools and can be found in
- **   builds/<arch>/<target>/cvc4autoconfig.h
- **
- ** Thus a working solution is to include this header immediately after all
- ** locations of #include <antlr3.h>. This includes all autogenerated files.
- ** This potentially has to be repeated so this header should not be guarded.
- **
- ** To ensure that we do not remove cvc4's versions and use antlr's by mistake
- ** #include <antlr3.h> needs to proceed any other includes like
- ** #include "cvc4parser_private.h".
- **
- ** It is worth noting that future version of antlr can both not define these
- ** macros and may generate different code. This is at best a stop gap
- ** solution.
- **
- ** Every location this header is included needs to be documented.
- ** When in doubt do not move this header!
- **/
-
-#undef PACKAGE_BUGREPORT
-#undef PACKAGE_NAME
-#undef PACKAGE_STRING
-#undef PACKAGE_TARNAME
-#undef PACKAGE_VERSION
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 1a4541939..3eddf438f 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -495,10 +495,6 @@ Expr addNots(ExprManager* em, size_t n, Expr e) {
 
 @lexer::includes {
 
-// This should come immediately after #include <antlr3.h> in the generated
-// files. See the documentation in "parser/antlr_undefines.h" for more details.
-#include "parser/antlr_undefines.h"
-
 /** This suppresses warnings about the redefinition of token symbols between different
   * parsers. The redefinitions should be harmless as long as no client: (a) #include's
   * the lexer headers for two grammars AND (b) uses the token symbol definitions. */
@@ -523,10 +519,6 @@ Expr addNots(ExprManager* em, size_t n, Expr e) {
 
 @parser::includes {
 
-// This should come immediately after #include <antlr3.h> in the generated
-// files. See the documentation in "parser/antlr_undefines.h" for more details.
-#include "parser/antlr_undefines.h"
-
 #include <cassert>
 #include <memory>
 #include <stdint.h>
diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
index 4efe23ac5..17a670f40 100644
--- a/src/parser/cvc/cvc_input.cpp
+++ b/src/parser/cvc/cvc_input.cpp
@@ -14,13 +14,10 @@
  ** [[ Add file-specific comments here ]]
  **/
 
-// These headers should be the first two included.
-// See the documentation in "parser/antlr_undefines.h" for more details.
-#include <antlr3.h>
-#include "parser/antlr_undefines.h"
-
 #include "parser/cvc/cvc_input.h"
 
+#include <antlr3.h>
+
 #include "expr/expr_manager.h"
 #include "parser/antlr_input.h"
 #include "parser/parser_exception.h"
diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g
index 1127bd2df..455da3b42 100644
--- a/src/parser/smt1/Smt1.g
+++ b/src/parser/smt1/Smt1.g
@@ -41,10 +41,6 @@ options {
 
 @lexer::includes {
 
-// This should come immediately after #include <antlr3.h> in the generated
-// files. See the documentation in "parser/antlr_undefines.h" for more details.
-#include "parser/antlr_undefines.h"
-
 /** This suppresses warnings about the redefinition of token symbols between
   * different parsers. The redefinitions should be harmless as long as no
   * client: (a) #include's the lexer headers for two grammars AND (b) uses the
@@ -67,10 +63,6 @@ options {
 
 @parser::includes {
 
-// This should come immediately after #include <antlr3.h> in the generated
-// files. See the documentation in "parser/antlr_undefines.h" for more details.
-#include "parser/antlr_undefines.h"
-
 #include <algorithm>
 #include <memory>
 #include <stdint.h>
diff --git a/src/parser/smt1/smt1_input.cpp b/src/parser/smt1/smt1_input.cpp
index a04dff844..0a8118711 100644
--- a/src/parser/smt1/smt1_input.cpp
+++ b/src/parser/smt1/smt1_input.cpp
@@ -14,13 +14,10 @@
  ** [[ Add file-specific comments here ]]
  **/
 
-// These headers must be the first two included.
-// See the documentation in "parser/antlr_undefines.h" for more details.
-#include <antlr3.h>
-#include "parser/antlr_undefines.h"
-
 #include "parser/smt1/smt1_input.h"
 
+#include <antlr3.h>
+
 #include "expr/expr_manager.h"
 #include "parser/input.h"
 #include "parser/parser.h"
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index b8b05f7dd..d9b0f622b 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -41,10 +41,6 @@ options {
 
 @lexer::includes {
 
-// This should come immediately after #include <antlr3.h> in the generated
-// files. See the documentation in "parser/antlr_undefines.h" for more details.
-#include "parser/antlr_undefines.h"
-
 /** This suppresses warnings about the redefinition of token symbols between
   * different parsers. The redefinitions should be harmless as long as no
   * client: (a) #include's the lexer headers for two grammars AND (b) uses the
@@ -81,10 +77,6 @@ using namespace CVC4::parser;
 
 @parser::includes {
 
-// This should come immediately after #include <antlr3.h> in the generated
-// files. See the documentation in "parser/antlr_undefines.h" for more details.
-#include "parser/antlr_undefines.h"
-
 #include <memory>
 
 #include "parser/parser.h"
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index 44d251370..e8b52ee34 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -14,14 +14,10 @@
  ** [[ Add file-specific comments here ]]
  **/
 
-// These headers should be the first two included.
-// See the documentation in "parser/antlr_undefines.h" for more details.
-#include <antlr3.h>
-#include "parser/antlr_undefines.h"
-
-
 #include "parser/smt2/smt2_input.h"
 
+#include <antlr3.h>
+
 #include "expr/expr_manager.h"
 #include "parser/input.h"
 #include "parser/parser.h"
diff --git a/src/parser/smt2/sygus_input.cpp b/src/parser/smt2/sygus_input.cpp
index 8ba5fdd10..00760bffc 100644
--- a/src/parser/smt2/sygus_input.cpp
+++ b/src/parser/smt2/sygus_input.cpp
@@ -14,14 +14,10 @@
  ** [[ Add file-specific comments here ]]
  **/
 
-// These headers should be the first two included.
-// See the documentation in "parser/antlr_undefines.h" for more details.
-#include <antlr3.h>
-#include "parser/antlr_undefines.h"
-
-
 #include "parser/smt2/sygus_input.h"
 
+#include <antlr3.h>
+
 #include "expr/expr_manager.h"
 #include "parser/input.h"
 #include "parser/parser.h"
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index be155c425..54e9b0b4a 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -42,10 +42,6 @@ options {
 
 @lexer::includes {
 
-// This should come immediately after #include <antlr3.h> in the generated
-// files. See the documentation in "parser/antlr_undefines.h" for more details.
-#include "parser/antlr_undefines.h"
-
 /** This suppresses warnings about the redefinition of token symbols between
   * different parsers. The redefinitions should be harmless as long as no
   * client: (a) #include's the lexer headers for two grammars AND (b) uses the
@@ -89,10 +85,6 @@ using namespace CVC4::parser;
 
 @parser::includes {
 
-// This should come immediately after #include <antlr3.h> in the generated
-// files. See the documentation in "parser/antlr_undefines.h" for more details.
-#include "parser/antlr_undefines.h"
-
 #include <memory>
 
 #include "smt/command.h"
diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp
index 78a465aca..126b28735 100644
--- a/src/parser/tptp/tptp_input.cpp
+++ b/src/parser/tptp/tptp_input.cpp
@@ -14,13 +14,11 @@
  ** [[ Add file-specific comments here ]]
  **/
 
-// These headers should be the first two included.
-// See the documentation in "parser/antlr_undefines.h" for more details.
-#include <antlr3.h>
-#include "parser/antlr_undefines.h"
-
 
 #include "parser/tptp/tptp_input.h"
+
+#include <antlr3.h>
+
 #include "expr/expr_manager.h"
 #include "parser/input.h"
 #include "parser/parser.h"