minor visibility fixes

diff --git a/src/expr/node.h b/src/expr/node.h
index 0f4b55d4a848a3c8e24a607add0a754330abf2ca..9d852f195e3481421557808084dc828ea9d59a84 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -52,6 +52,11 @@ class NodeManager;
 template <bool ref_count>
 class NodeTemplate;
 
+// For some reason these are instantiated with different visibility in different modules??
+// Fix by making their instantiations explicit, here.
+template <> CVC4ostream& CVC4ostream::operator<<(NodeTemplate<false> const& t) CVC4_PUBLIC;
+template <> CVC4ostream& CVC4ostream::operator<<(NodeTemplate<true> const& t) CVC4_PUBLIC;
+
 /**
  * Exception thrown during the type-checking phase, it can be
  * thrown by node.getType().

diff --git a/src/util/output.h b/src/util/output.h
index da1efe68a578a156580d963c33936d5c65b6e54b..8a90ef136c839cb24ac309c5735b4ec6f6e51581 100644 (file)
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -112,19 +112,7 @@ public:
   operator std::ostream&() { return isConnected() ? *d_os : null_os; }
 
   template <class T>
-  CVC4ostream& operator<<(T const& t) {
-    if(d_os != NULL) {
-      if(d_firstColumn) {
-        d_firstColumn = false;
-        long indent = d_os->iword(s_indentIosIndex);
-        for(long i = 0; i < indent; ++ i) {
-          d_os = &(*d_os << s_tab);
-        }
-      }
-      d_os = &(*d_os << t);
-    }
-    return *this;
-  }
+  CVC4ostream& operator<<(T const& t) CVC4_PUBLIC;
 
   // support manipulators, endl, etc..
   CVC4ostream& operator<<(std::ostream& (*pf)(std::ostream&)) {
@@ -164,6 +152,21 @@ inline CVC4ostream& pop(CVC4ostream& stream) {
   return stream;
 }
 
+template <class T>
+CVC4ostream& CVC4ostream::operator<<(T const& t) {
+  if(d_os != NULL) {
+    if(d_firstColumn) {
+      d_firstColumn = false;
+      long indent = d_os->iword(s_indentIosIndex);
+      for(long i = 0; i < indent; ++i) {
+        d_os = &(*d_os << s_tab);
+      }
+    }
+    d_os = &(*d_os << t);
+  }
+  return *this;
+}
+
 /** The debug output class */
 class CVC4_PUBLIC DebugC {
   std::set<std::string> d_tags;