From: Morgan Deters Date: Wed, 5 Oct 2011 19:03:23 +0000 (+0000) Subject: minor visibility fixes X-Git-Tag: cvc5-1.0.0~8424 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9bdf1355af20c4dd2b97ea9bc5f34cc20fbdde0f;p=cvc5.git minor visibility fixes --- diff --git a/src/expr/node.h b/src/expr/node.h index 0f4b55d4a..9d852f195 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -52,6 +52,11 @@ class NodeManager; template 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 const& t) CVC4_PUBLIC; +template <> CVC4ostream& CVC4ostream::operator<<(NodeTemplate 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 da1efe68a..8a90ef136 100644 --- 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 - 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 +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 d_tags;