/*********************                                                        */
/*! \file antlr_undefines.h
 ** \verbatim
 ** Top contributors (to current version):
 **   Tim King
 ** This file is part of the CVC4 project.
 ** Copyright (c) 2009-2016 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