From: Morgan Deters Date: Tue, 3 May 2011 04:33:09 +0000 (+0000) Subject: output fixes for performance X-Git-Tag: cvc5-1.0.0~8558 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=12d31931b48b659b78f531e98dba9d449da0137b;p=cvc5.git output fixes for performance --- diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index af0024156..fce785cc7 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -688,8 +688,8 @@ mainCommand[CVC4::Command*& cmd] | ECHO_TOK ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) - { CVC4::Message() << s << std::endl; } - | { CVC4::Message() << std::endl; } + { Message() << s << std::endl; } + | { Message() << std::endl; } ) | INCLUDE_TOK diff --git a/src/util/output.h b/src/util/output.h index d3eb3a831..f21fc39e7 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -76,10 +76,11 @@ public: void pushIndent() { d_indent ++; } void popIndent() { if (d_indent > 0) -- d_indent; } - void flush() { + CVC4ostream& flush() { if(d_os != NULL) { d_os->flush(); } + return *this; } bool isConnected() { return d_os != NULL; } @@ -184,6 +185,8 @@ public: std::ostream& setStream(std::ostream& os) { d_os = &os; return os; } std::ostream& getStream() { return *d_os; } + + bool isOn() const { return d_os != &null_os; } };/* class WarningC */ /** The message output class */ @@ -199,6 +202,8 @@ public: std::ostream& setStream(std::ostream& os) { d_os = &os; return os; } std::ostream& getStream() { return *d_os; } + + bool isOn() const { return d_os != &null_os; } };/* class MessageC */ /** The notice output class */ @@ -214,6 +219,8 @@ public: std::ostream& setStream(std::ostream& os) { d_os = &os; return os; } std::ostream& getStream() { return *d_os; } + + bool isOn() const { return d_os != &null_os; } };/* class NoticeC */ /** The chat output class */ @@ -229,6 +236,8 @@ public: std::ostream& setStream(std::ostream& os) { d_os = &os; return os; } std::ostream& getStream() { return *d_os; } + + bool isOn() const { return d_os != &null_os; } };/* class ChatC */ /** The trace output class */ @@ -273,26 +282,33 @@ public: /** The debug output singleton */ extern DebugC DebugChannel CVC4_PUBLIC; #ifdef CVC4_DEBUG -# define Debug CVC4::DebugChannel +# define Debug ::CVC4::DebugChannel #else /* CVC4_DEBUG */ -# define Debug CVC4::__cvc4_true() ? CVC4::debugNullCvc4Stream : CVC4::DebugChannel +# define Debug ::CVC4::__cvc4_true() ? ::CVC4::debugNullCvc4Stream : ::CVC4::DebugChannel #endif /* CVC4_DEBUG */ /** The warning output singleton */ extern WarningC Warning CVC4_PUBLIC; +#define Warning() (! ::CVC4::Warning.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Warning() + /** The message output singleton */ extern MessageC Message CVC4_PUBLIC; +#define Message() (! ::CVC4::Message.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Message() + /** The notice output singleton */ extern NoticeC Notice CVC4_PUBLIC; +#define Notice() (! ::CVC4::Notice.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Notice() + /** The chat output singleton */ extern ChatC Chat CVC4_PUBLIC; +#define Chat() (! ::CVC4::Chat.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Chat() /** The trace output singleton */ extern TraceC TraceChannel CVC4_PUBLIC; #ifdef CVC4_TRACING -# define Trace CVC4::TraceChannel +# define Trace ::CVC4::TraceChannel #else /* CVC4_TRACING */ -# define Trace CVC4::__cvc4_true() ? CVC4::debugNullCvc4Stream : CVC4::TraceChannel +# define Trace ::CVC4::__cvc4_true() ? ::CVC4::debugNullCvc4Stream : ::CVC4::TraceChannel #endif /* CVC4_TRACING */ // Disallow e.g. !Debug("foo").isOn() forms @@ -432,33 +448,6 @@ extern NullDebugC Trace CVC4_PUBLIC; */ class CVC4_PUBLIC NullDebugC { public: -/* - NullDebugC() {} - NullDebugC(std::ostream* os) {} - - void operator()(const char* tag, const char*) {} - void operator()(const char* tag, std::string) {} - void operator()(std::string tag, const char*) {} - void operator()(std::string tag, std::string) {} - - int printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) {} - int printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) {} - - std::ostream& operator()(const char* tag) { return null_os; } - std::ostream& operator()(std::string tag) { return null_os; } - - void on (const char* tag) {} - void on (std::string tag) {} - void off(const char* tag) {} - void off(std::string tag) {} - - bool isOn(const char* tag) { return false; } - bool isOn(std::string tag) { return false; } - - void setStream(std::ostream& os) {} - std::ostream& getStream() { return null_os; } - -*/ operator bool() { return false; } operator CVC4ostream() { return CVC4ostream(); } operator std::ostream&() { return null_os; } @@ -471,6 +460,7 @@ public: * complain. */ class CVC4_PUBLIC NullC { public: +/* NullC() {} NullC(std::ostream* os) {} @@ -480,6 +470,10 @@ public: std::ostream& setStream(std::ostream& os) { return null_os; } std::ostream& getStream() { return null_os; } +*/ + operator bool() { return false; } + operator CVC4ostream() { return CVC4ostream(); } + operator std::ostream&() { return null_os; } };/* class NullC */ extern NullDebugC debugNullCvc4Stream CVC4_PUBLIC;