From 4206a75e7a1635d04bb69084404a75670e164b62 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 29 Jun 2010 22:42:40 +0000
Subject: add --default-expr-depth=N command line parameter, expose setdepth()
 to public interface

---
 src/util/output.h | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src/util/output.h')

diff --git a/src/util/output.h b/src/util/output.h
index f27ec24da..651f6b607 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -116,6 +116,7 @@ public:
   bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
 
   void setStream(std::ostream& os) { d_os = &os; }
+  std::ostream& getStream() { return *d_os; }
 };/* class Debug */
 
 /** The debug output singleton */
@@ -141,6 +142,7 @@ public:
   std::ostream& operator()() { return *d_os; }
 
   void setStream(std::ostream& os) { d_os = &os; }
+  std::ostream& getStream() { return *d_os; }
 };/* class Warning */
 
 /** The warning output singleton */
@@ -162,6 +164,7 @@ public:
   std::ostream& operator()() { return *d_os; }
 
   void setStream(std::ostream& os) { d_os = &os; }
+  std::ostream& getStream() { return *d_os; }
 };/* class Message */
 
 /** The message output singleton */
@@ -183,6 +186,7 @@ public:
   std::ostream& operator()() { return *d_os; }
 
   void setStream(std::ostream& os) { d_os = &os; }
+  std::ostream& getStream() { return *d_os; }
 };/* class Notice */
 
 /** The notice output singleton */
@@ -204,6 +208,7 @@ public:
   std::ostream& operator()() { return *d_os; }
 
   void setStream(std::ostream& os) { d_os = &os; }
+  std::ostream& getStream() { return *d_os; }
 };/* class Chat */
 
 /** The chat output singleton */
@@ -270,6 +275,7 @@ public:
   bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
 
   void setStream(std::ostream& os) { d_os = &os; }
+  std::ostream& getStream() { return *d_os; }
 };/* class Trace */
 
 /** The trace output singleton */
@@ -321,6 +327,7 @@ public:
   bool isOn(std::string tag) { return false; }
 
   void setStream(std::ostream& os) {}
+  std::ostream& getStream() { return null_os; }
 };/* class NullDebugC */
 
 /**
@@ -341,6 +348,7 @@ public:
   std::ostream& operator()() { return null_os; }
 
   void setStream(std::ostream& os) {}
+  std::ostream& getStream() { return null_os; }
 };/* class NullC */
 
 extern NullDebugC debugNullCvc4Stream CVC4_PUBLIC;
-- 
cgit v1.2.3