blob: 20df6dbc7c9cb73d032af30af2bff08df90baf29 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
|
/********************* */
/*! \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
|
