Remove antlr_undefines.h. (#2664)

Is not required anymore since we don't use autotools anymore.

diff --git a/cmake/ConfigureCVC4.cmake b/cmake/ConfigureCVC4.cmake
index cfbd1a1c2b88787301367bfee8c3cb387973f2bc..84575d6109688496f2f64a6e2b92919c2055bbe7 100644 (file)
--- a/cmake/ConfigureCVC4.cmake
+++ b/cmake/ConfigureCVC4.cmake
@@ -80,4 +80,4 @@ set(CVC4_CLN_IMP ${CVC4_USE_CLN_IMP})
 # Defined if using the GMP multi-precision arithmetic library.
 set(CVC4_GMP_IMP ${CVC4_USE_GMP_IMP})
 # Define the full name of this package.
-set(PACKAGE_NAME "${PROJECT_NAME}")
+set(CVC4_PACKAGE_NAME "${PROJECT_NAME}")

diff --git a/cvc4autoconfig.h.in b/cvc4autoconfig.h.in
index ce8aeb5dad18367b083f9bedad1bcce5985c28fc..1c9fdf60526f9c15d147a3c41401cd4b8429a900 100644 (file)
--- a/cvc4autoconfig.h.in
+++ b/cvc4autoconfig.h.in
@@ -17,7 +17,7 @@
 #define CVC4_RELEASE_STRING "@CVC4_RELEASE_STRING@"
 
 /* Full name of this package. */
-#define PACKAGE_NAME "@PACKAGE_NAME@"
+#define CVC4_PACKAGE_NAME "@CVC4_PACKAGE_NAME@"
 
 /* Define to 1 if CVC4 is built with (optional) GPLed library dependencies. */
 #cmakedefine01 CVC4_GPL_DEPS

diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index a00cee856c557eb09704ec59f558b004dba65f3d..f154e5c90ce5f814f99c7e74976c51e137a9a35c 100644 (file)
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -39,7 +39,7 @@ using namespace std;
 namespace CVC4 {
 
 string Configuration::getName() {
-  return PACKAGE_NAME;
+  return CVC4_PACKAGE_NAME;
 }
 
 bool Configuration::isDebugBuild() {
@@ -89,7 +89,7 @@ bool Configuration::isCompetitionBuild() {
 }
 
 string Configuration::getPackageName() {
-  return PACKAGE_NAME;
+  return CVC4_PACKAGE_NAME;
 }
 
 string Configuration::getVersionString() {

diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index d7491f8caefdbe8de027c99346c55521302c8c7d..d79d7b22c8b0ec7b69eb5534bb2df4611723db45 100644 (file)
--- 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 fe80d032228e452da321cbdfbdffa33223424965..a2885d1b6fa3abb1c67b79c5ae5ac6d62af90a06 100644 (file)
--- 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 5598dd359e73d7562df4e25d79b97c7349e826e7..576b693e8c936bb24971ffe24c1e6756c8a536f3 100644 (file)
--- 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 0f746cfbb633c29d285d026ac03d394afa8a8c4e..91ced0f4171e6a3653386270353ccd5d0d7f8aa3 100644 (file)
--- 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 a2ca0de7816e1d8c43cd612e6c4b88c7118a7d79..35666355921bda732a32333c589b6626a9f53b13 100644 (file)
--- 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 8253a9c3fc7820b95a871b7d1a5508b4a06f2cb4..c33566e229cddf5e245a2173fcb9210f787233c2 100644 (file)
--- 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 (file)
index 20df6db..0000000
--- 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 1a4541939ce1c1a9c6a061dd4b2b0aafb554dbf4..3eddf438f866f277c453347f39ae42ebe99147f9 100644 (file)
--- 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 4efe23ac51182ee7a68a96f20d1a23977d8d3281..17a670f40b11a0266098d9c52038f205a7817bb0 100644 (file)
--- 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 1127bd2df258c7a87bc1eac609a556b2a0c8653f..455da3b42a3a4820cdb711675ede05ffecab7cd5 100644 (file)
--- 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 a04dff844c250ebfcd83918ca6c065977dbc3a67..0a81187117b7e13c4525847ce3e83907bc75c8ad 100644 (file)
--- 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 b8b05f7dd2638b82ed31d6a731cda4ec13952a82..d9b0f622be794d0fcd7d4cff7bd29e0087856be3 100644 (file)
--- 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 44d251370ce408fa9bbd950207925757d7b5633c..e8b52ee34dc3f249a57ee5c67ac5c3f3cee60431 100644 (file)
--- 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 8ba5fdd10df03e035eaec8d4eb59310dc873308a..00760bffcb9c313a782cb1d1dd863fb40f2dcbfc 100644 (file)
--- 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 be155c42544f029cfbee6a660c1b09d94d3d331f..54e9b0b4a17af3314001ed4552acc504f4a047bc 100644 (file)
--- 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 78a465aca60451fcdfaa707498b10750b823f0c5..126b28735a18b1c599d6401d76a20c2d04eddab3 100644 (file)
--- 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"