Remove output.h from public space, to avoid clashes with symbols defined in users...

Specifically, output.h was moved to CVC4's "private-library" rules, which means that it's
not installed on users' machines, and public headers should not include it.

Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 601c251d9d2dd765adf99c3e8a7ada44c375825e..1ac277667934492eb02cd35c64b29a74f6a144d3 100644 (file)
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -25,6 +25,7 @@
 #include "util/hash.h"
 #include "util/subrange_bound.h"
 #include "util/predicate.h"
+#include "util/output.h"
 
 #include "parser/parser.h"
 #include "parser/parser_builder.h"

diff --git a/src/include/cvc4_private_library.h b/src/include/cvc4_private_library.h
index b04160a818bbb4f9c876622c1db3d3e817a76ea8..f7fd1b60750ec3cfa817d46ccc9ea25cdd61421e 100644 (file)
--- a/src/include/cvc4_private_library.h
+++ b/src/include/cvc4_private_library.h
@@ -19,7 +19,7 @@
 #ifndef __CVC4_PRIVATE_LIBRARY_H
 #define __CVC4_PRIVATE_LIBRARY_H
 
-#if ! (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) || defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST) || defined(__BUILDING_CVC4DRIVER))
+#if ! (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) || defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST) || defined(__BUILDING_CVC4COMPATLIB) || defined(__BUILDING_CVC4DRIVER))
 #  warning A "private library" CVC4 header was included when not building the library, driver, or private unit test code.
 #endif /* ! (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST || __BUILDING_CVC4PARSERLIB || __BUILDING_CVC4PARSERLIB_UNIT_TEST || __BUILDING_CVC4DRIVER) */
 

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 5c9f8af218fa78a3d6aa068cab9739326b40ff07..a8099ca30d78229b8067d3ee753f3bdf250f9fa7 100644 (file)
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -33,6 +33,7 @@
 #include "parser/parser_builder.h"
 #include "options/options.h"
 #include "util/language.h"
+#include "util/output.h"
 
 #include <string.h>
 #include <cassert>

diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 3b7d53be8b6ca54b4689f9647c6aa73f25830f6c..8763e8451e3f40c42b36a32625bd64f6a25d9fc0 100644 (file)
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -14,12 +14,21 @@
  ** Base for ANTLR parser classes.
  **/
 
+#include <antlr3.h>
+
+// ANTLR3 headers define these in our space :(
+// undef them so that we don't get multiple-definition warnings
+#undef PACKAGE_BUGREPORT
+#undef PACKAGE_NAME
+#undef PACKAGE_STRING
+#undef PACKAGE_TARNAME
+#undef PACKAGE_VERSION
+
 #include "cvc4parser_private.h"
 
 #ifndef __CVC4__PARSER__ANTLR_INPUT_H
 #define __CVC4__PARSER__ANTLR_INPUT_H
 
-#include <antlr3.h>
 #include <iostream>
 #include <sstream>
 #include <stdexcept>
@@ -34,6 +43,7 @@
 #include "util/bitvector.h"
 #include "util/integer.h"
 #include "util/rational.h"
+#include "util/output.h"
 
 namespace CVC4 {
 

diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp
index c2f73d988831da11bd5514ed53c51082dee73a61..a59fb35316e8dec013ee176a5049f17303035a93 100644 (file)
--- a/src/parser/antlr_line_buffered_input.cpp
+++ b/src/parser/antlr_line_buffered_input.cpp
@@ -16,6 +16,15 @@
  **/
 
 #include <antlr3.h>
+
+// ANTLR3 headers define these in our space :(
+// undef them so that we don't get multiple-definition warnings
+#undef PACKAGE_BUGREPORT
+#undef PACKAGE_NAME
+#undef PACKAGE_STRING
+#undef PACKAGE_TARNAME
+#undef PACKAGE_VERSION
+
 #include <iostream>
 #include <string>
 #include <cassert>

diff --git a/src/util/datatype.h b/src/util/datatype.h
index 3da441f1f606693a61adf86f89053977e5a1e46b..c46c10c973c88dfe74471754170094a9d4d0a1a6 100644 (file)
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -33,7 +33,6 @@ namespace CVC4 {
 
 #include "expr/expr.h"
 #include "expr/type.h"
-#include "util/output.h"
 #include "util/hash.h"
 #include "util/exception.h"
 

diff --git a/src/util/dump.h b/src/util/dump.h
index 2ef6010e3718cb5d2a43b0dfb160e2cfdfd13dcb..0bde68d762323254753dedbf25afd80185118620 100644 (file)
--- a/src/util/dump.h
+++ b/src/util/dump.h
@@ -19,7 +19,6 @@
 #ifndef __CVC4__DUMP_H
 #define __CVC4__DUMP_H
 
-#include "util/output.h"
 #include "expr/command.h"
 
 namespace CVC4 {

diff --git a/src/util/output.h b/src/util/output.h
index 263d5a14475f5edaa76cb803b487dc256e1ac2ba..7394f24abd8b48a7427c46f1eb467994139a3c36 100644 (file)
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -14,7 +14,7 @@
  ** Output utility classes and functions.
  **/
 
-#include "cvc4_public.h"
+#include "cvc4_private_library.h"
 
 #ifndef __CVC4__OUTPUT_H
 #define __CVC4__OUTPUT_H

diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index c66b5cb1f847d1ae895d0479a6abc31250ec2c19..7f6385d36f8942faf02b4c63bbffbe2edb6470b3 100644 (file)
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -342,7 +342,7 @@ public:
   void testIsConst() {
     /* bool isConst() const; */
 
-    Debug.on("isConst");
+    //Debug.on("isConst");
 
     TS_ASSERT(!a_bool->isConst());
     TS_ASSERT(!b_bool->isConst());

diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h
index 2441b7b0d503a48c50311e6c9299e7f5c50c3d2a..3c2609e3eb6f513291c76c91b4152b6842e21723 100644 (file)
--- a/test/unit/expr/type_cardinality_public.h
+++ b/test/unit/expr/type_cardinality_public.h
@@ -200,7 +200,7 @@ public:
   }
 
   void testBitvectors() {
-    Debug.on("bvcard");
+    //Debug.on("bvcard");
     TS_ASSERT( d_em->mkBitVectorType(0).getCardinality().compare(0) == Cardinality::EQUAL );
     Cardinality lastCard = 0;
     for(unsigned i = 1; i <= 65; ++i) {