diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/expr/node.h | 5 | ||||
| -rw-r--r-- | src/util/output.h | 29 |
2 files changed, 21 insertions, 13 deletions
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 <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 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 <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; |