From: Mathias Preiner Date: Sat, 20 Oct 2018 21:53:19 +0000 (-0700) Subject: Remove antlr_undefines.h. (#2664) X-Git-Tag: cvc5-1.0.0~4393 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0b515de430771d9bdc15fc29d41b391f1cc7c1fd;p=cvc5.git 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 cfbd1a1c2..84575d610 100644 --- 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 ce8aeb5da..1c9fdf605 100644 --- 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 a00cee856..f154e5c90 100644 --- 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 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 in "parser/antlr_input.h". -// This is avoid having to undefine the symbols in . -// See the documentation in "parser/antlr_undefines.h" for more -// details. +#include #include #include 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 -#include "parser/antlr_undefines.h" - #include "cvc4parser_private.h" +#include #include #include #include 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 -#include "parser/antlr_undefines.h" - #include #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 in -// "parser/antlr_line_buffered_input.h". -// This is avoid having to undefine the symbols in . -// See the documentation in "parser/antlr_undefines.h" for more -// details. - #include "parser/antlr_line_buffered_input.h" +#include #include #include #include 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 -#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 #include #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 -> -> -> - ** - ** 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///cvc4autoconfig.h - ** - ** Thus a working solution is to include this header immediately after all - ** locations of #include . 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 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 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 in the generated -// files. See the documentation in "parser/antlr_undefines.h" for more details. -#include "parser/antlr_undefines.h" - #include #include #include 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 -#include "parser/antlr_undefines.h" - #include "parser/cvc/cvc_input.h" +#include + #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 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 in the generated -// files. See the documentation in "parser/antlr_undefines.h" for more details. -#include "parser/antlr_undefines.h" - #include #include #include 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 -#include "parser/antlr_undefines.h" - #include "parser/smt1/smt1_input.h" +#include + #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 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 in the generated -// files. See the documentation in "parser/antlr_undefines.h" for more details. -#include "parser/antlr_undefines.h" - #include #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 -#include "parser/antlr_undefines.h" - - #include "parser/smt2/smt2_input.h" +#include + #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 -#include "parser/antlr_undefines.h" - - #include "parser/smt2/sygus_input.h" +#include + #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 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 in the generated -// files. See the documentation in "parser/antlr_undefines.h" for more details. -#include "parser/antlr_undefines.h" - #include #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 -#include "parser/antlr_undefines.h" - #include "parser/tptp/tptp_input.h" + +#include + #include "expr/expr_manager.h" #include "parser/input.h" #include "parser/parser.h"