1 files changed, 18 insertions, 0 deletions
diff --git a/src/util/output.h b/src/util/output.h
index b6532b93a..43dfe8a40 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -91,6 +91,24 @@ public:
 
 extern WarningC Warning CVC4_PUBLIC;
 
+class CVC4_PUBLIC MessageC {
+  std::ostream *d_os;
+
+public:
+  MessageC(std::ostream* os) : d_os(os) {}
+
+  void operator()(const char* s) { *d_os << s; }
+  void operator()(std::string s) { *d_os << s; }
+
+  void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+
+  std::ostream& operator()() { return *d_os; }
+
+  void setStream(std::ostream& os) { d_os = &os; }
+};/* class Message */
+
+extern MessageC Message CVC4_PUBLIC;
+
 class CVC4_PUBLIC NoticeC {
   std::ostream *d_os;