src/parser/antlr_undefines.h

   1 /*********************                                                        */
   2 /*! \file antlr_undefines.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Every usage undefines standard autotools macro names.
  13  **
  14  ** This header is very sensitive and it should be understood *in full* before
  15  ** it is used or *moved* in position relative to other headers.
  16  **
  17  ** Including this header runs #undef on the following identifiers:
  18  ** - PACKAGE_BUGREPORT,
  19  ** - PACKAGE_NAME
  20  ** - PACKAGE_STRING
  21  ** - PACKAGE_TARNAME
  22  ** - PACKAGE_VERSION
  23  **
  24  ** This is to solves a problem caused by antlr and cvc4 both defining these
  25  ** symbols. This has to do with both packages using autotools in a slightly
  26  ** dicey way. This was reported by us a long time ago, but most versions
  27  ** of libantlr are quite old (3.2).
  28  ** http://www.antlr3.org/pipermail/antlr-interest/2010-March/037859.html
  29  **
  30  ** The source of both of these two definitions are given below.
  31  **
  32  ** From antlr, the autogenerated antlr lexers and parsers include antlr3.h.
  33  ** The chain of inclusions is:
  34  **  Lang{Lexer,Parser}.h -> <antlr3.h> -> <antlr3config.h> -> <antlr3defs.h>
  35  **
  36  ** where Lang is in {Smt1,Smt2,Tptp,Cvc}.
  37  **
  38  ** From CVC4, the parsers use Debug("...") and other features from
  39  ** "base/output.h". This is a cvc4_private_library.h header file. This means
  40  ** the files is usable while building the driver and parsers, but is otherwise
  41  ** conceptually the same as a cvc4_private.h header. (If that sounds sketchy,
  42  ** it is sure is! [See src/DESIGN.txt for more details].)
  43  ** The include chain is then
  44  **  "base/output.h" -> "cvc4_private_library.h" -> "cvc4_private.h" ->
  45  **     "cvc4autoconfig.h".
  46  ** The file cvc4autoconfig.h is autogenerated by autotools and can be found in
  47  **   builds/<arch>/<target>/cvc4autoconfig.h
  48  **
  49  ** Thus a working solution is to include this header immediately after all
  50  ** locations of #include <antlr3.h>. This includes all autogenerated files.
  51  ** This potentially has to be repeated so this header should not be guarded.
  52  **
  53  ** To ensure that we do not remove cvc4's versions and use antlr's by mistake
  54  ** #include <antlr3.h> needs to proceed any other includes like
  55  ** #include "cvc4parser_private.h".
  56  **
  57  ** It is worth noting that future version of antlr can both not define these
  58  ** macros and may generate different code. This is at best a stop gap
  59  ** solution.
  60  **
  61  ** Every location this header is included needs to be documented.
  62  ** When in doubt do not move this header!
  63  **/
  64
  65 #undef PACKAGE_BUGREPORT
  66 #undef PACKAGE_NAME
  67 #undef PACKAGE_STRING
  68 #undef PACKAGE_TARNAME
  69 #undef PACKAGE_VERSION