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

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.

10 files changed, 26 insertions, 7 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 601c251d9..1ac277667 100644
--- 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 b04160a81..f7fd1b607 100644
--- 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 5c9f8af21..a8099ca30 100644
--- 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 3b7d53be8..8763e8451 100644
--- 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 c2f73d988..a59fb3531 100644
--- 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 3da441f1f..c46c10c97 100644
--- 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 2ef6010e3..0bde68d76 100644
--- 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 263d5a144..7394f24ab 100644
--- 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 c66b5cb1f..7f6385d36 100644
--- 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 2441b7b0d..3c2609e3e 100644
--- 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) {