summaryrefslogtreecommitdiff
path: root/src/util/output.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2009-12-17 18:48:39 +0000
committerMorgan Deters <mdeters@gmail.com>2009-12-17 18:48:39 +0000
commit7eb18a6c4b0ec6fcf4b6474d22307baa04f8f515 (patch)
tree8621e2e60756ec6770bc949877eef808e7e99d55 /src/util/output.h
parent3b06265b82d48074b3b733d655efd6dab6481150 (diff)
+ test infrastructure fixes
+ regenerate configure script + add CVC4::Message output class + add some IllegalArgument() assertion things + rename NodeManager::mkExpr() to mkNode()
Diffstat (limited to 'src/util/output.h')
-rw-r--r--src/util/output.h18
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback