From: Morgan Deters Date: Wed, 4 May 2011 00:21:34 +0000 (+0000) Subject: Stronger support for zero-performance-penalty output, and fixes and X-Git-Tag: cvc5-1.0.0~8557 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=691fbae1dad8689007686cf61b737da58a4c9427;p=cvc5.git Stronger support for zero-performance-penalty output, and fixes and simplifications for the "muzzled" (i.e. competition) design, which had been broken. Addition of some new unit test bits to ensure that nothing is ever called in muzzled builds, e.g. things like Warning() << expensiveFunction(); Also, fix some compiler warnings. --- diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 7b5319267..104992bd4 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -387,11 +387,11 @@ void TheoryDatatypes::addTester( Node assertion ){ unsigned int testerIndex = -1; for( unsigned int i=0; imkNode( APPLY_TESTER, Node::fromExpr( dt[testerIndex].getTester() ), tRep ); Node exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb; d_em.addNode( assertionRep, exp, Reason::idt_texhaust ); @@ -862,7 +862,7 @@ void TheoryDatatypes::collectTerms( Node n ) { if( n.getKind() == APPLY_CONSTRUCTOR ){ for( int i=0; i<(int)n.getNumChildren(); i++ ) { Debug("datatypes-cycles") << "Subterm " << n << " -> " << n[i] << endl; - bool result = d_cycle_check.addEdgeNode( n, n[i] ); + bool result CVC4_UNUSED = d_cycle_check.addEdgeNode( n, n[i] ); Assert( !result ); //this should not create any new cycles (relevant terms should have been recorded before) } }else{ diff --git a/src/theory/shared_term_manager.cpp b/src/theory/shared_term_manager.cpp index 8103a149a..03afa984e 100644 --- a/src/theory/shared_term_manager.cpp +++ b/src/theory/shared_term_manager.cpp @@ -67,7 +67,7 @@ void SharedTermManager::addTerm(TNode n, Theory* parent, Theory* child) { uint64_t bothTags = parentTag | childTag; // Create or update the SharedData for n - SharedData* pData; + SharedData* pData = NULL; if(n.getAttribute(SharedAttr(), pData)) { // The attribute already exists, just update it if necessary uint64_t tags = pData->getTheories(); @@ -121,8 +121,8 @@ void SharedTermManager::addEq(TNode eq, Theory* thReason) { TNode x = eq[0]; TNode y = eq[1]; - SharedData* pDataX; - SharedData* pDataY; + SharedData* pDataX = NULL; + SharedData* pDataY = NULL; // Grab the SharedData for each side of the equality, create if necessary if(!x.getAttribute(SharedAttr(), pDataX)) { diff --git a/src/util/output.cpp b/src/util/output.cpp index 080409ed8..88628481f 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -11,15 +11,15 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Output utility classes and functions. + ** \brief Output utility classes and functions ** ** Output utility classes and functions. **/ -#include - #include "util/output.h" +#include + using namespace std; namespace CVC4 { @@ -29,18 +29,19 @@ namespace CVC4 { null_streambuf null_sb; ostream null_os(&null_sb); -NullDebugC debugNullCvc4Stream CVC4_PUBLIC; NullC nullCvc4Stream CVC4_PUBLIC; -#ifndef CVC4_MUZZLE - DebugC DebugChannel CVC4_PUBLIC (&cout); -WarningC Warning CVC4_PUBLIC (&cerr); -MessageC Message CVC4_PUBLIC (&cout); -NoticeC Notice CVC4_PUBLIC (&cout); -ChatC Chat CVC4_PUBLIC (&cout); +WarningC WarningChannel CVC4_PUBLIC (&cerr); +MessageC MessageChannel CVC4_PUBLIC (&cout); +NoticeC NoticeChannel CVC4_PUBLIC (&cout); +ChatC ChatChannel CVC4_PUBLIC (&cout); TraceC TraceChannel CVC4_PUBLIC (&cout); +#ifndef CVC4_MUZZLE + +# ifdef CVC4_DEBUG + int DebugC::printf(const char* tag, const char* fmt, ...) { if(d_tags.find(string(tag)) == d_tags.end()) { return 0; @@ -71,6 +72,8 @@ int DebugC::printf(std::string tag, const char* fmt, ...) { return retval; } +# endif /* CVC4_DEBUG */ + int WarningC::printf(const char* fmt, ...) { // chop off output after 1024 bytes char buf[1024]; @@ -115,6 +118,8 @@ int ChatC::printf(const char* fmt, ...) { return retval; } +# ifdef CVC4_TRACING + int TraceC::printf(const char* tag, const char* fmt, ...) { if(d_tags.find(string(tag)) == d_tags.end()) { return 0; @@ -145,14 +150,7 @@ int TraceC::printf(std::string tag, const char* fmt, ...) { return retval; } -#else /* ! CVC4_MUZZLE */ - -NullDebugC Debug CVC4_PUBLIC; -NullC Warning CVC4_PUBLIC; -NullC Message CVC4_PUBLIC; -NullC Notice CVC4_PUBLIC; -NullC Chat CVC4_PUBLIC; -NullDebugC Trace CVC4_PUBLIC; +# endif /* CVC4_TRACING */ #endif /* ! CVC4_MUZZLE */ diff --git a/src/util/output.h b/src/util/output.h index f21fc39e7..b0e210c17 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Output utility classes and functions. + ** \brief Output utility classes and functions ** ** Output utility classes and functions. **/ @@ -58,8 +58,6 @@ extern null_streambuf null_sb; /** A null output stream singleton */ extern std::ostream null_os CVC4_PUBLIC; -#ifndef CVC4_MUZZLE - class CVC4_PUBLIC CVC4ostream { std::ostream* d_os; // Current indentation @@ -281,35 +279,57 @@ public: /** The debug output singleton */ extern DebugC DebugChannel CVC4_PUBLIC; -#ifdef CVC4_DEBUG -# define Debug ::CVC4::DebugChannel -#else /* CVC4_DEBUG */ -# 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() - +extern WarningC WarningChannel CVC4_PUBLIC; /** The message output singleton */ -extern MessageC Message CVC4_PUBLIC; -#define Message() (! ::CVC4::Message.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Message() - +extern MessageC MessageChannel CVC4_PUBLIC; /** The notice output singleton */ -extern NoticeC Notice CVC4_PUBLIC; -#define Notice() (! ::CVC4::Notice.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Notice() - +extern NoticeC NoticeChannel CVC4_PUBLIC; /** The chat output singleton */ -extern ChatC Chat CVC4_PUBLIC; -#define Chat() (! ::CVC4::Chat.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Chat() - +extern ChatC ChatChannel CVC4_PUBLIC; /** The trace output singleton */ extern TraceC TraceChannel CVC4_PUBLIC; -#ifdef CVC4_TRACING -# define Trace ::CVC4::TraceChannel -#else /* CVC4_TRACING */ -# define Trace ::CVC4::__cvc4_true() ? ::CVC4::debugNullCvc4Stream : ::CVC4::TraceChannel -#endif /* CVC4_TRACING */ + +#ifdef CVC4_MUZZLE + +# define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel +# define Warning ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel +# define Message ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel +# define Notice ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel +# define Chat ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel +# define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel + +inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; } +inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; } +inline int WarningC::printf(const char* fmt, ...) { return 0; } +inline int MessageC::printf(const char* fmt, ...) { return 0; } +inline int NoticeC::printf(const char* fmt, ...) { return 0; } +inline int ChatC::printf(const char* fmt, ...) { return 0; } +inline int TraceC::printf(const char* tag, const char* fmt, ...) { return 0; } +inline int TraceC::printf(std::string tag, const char* fmt, ...) { return 0; } + +#else /* CVC4_MUZZLE */ + +# ifdef CVC4_DEBUG +# define Debug ::CVC4::DebugChannel +# else /* CVC4_DEBUG */ +# define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel +inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; } +inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; } +# endif /* CVC4_DEBUG */ +# define Warning (! ::CVC4::WarningChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel +# define Message (! ::CVC4::MessageChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel +# define Notice (! ::CVC4::NoticeChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel +# define Chat (! ::CVC4::ChatChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel +# ifdef CVC4_TRACING +# define Trace ::CVC4::TraceChannel +# else /* CVC4_TRACING */ +# define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel +inline int TraceC::printf(const char* tag, const char* fmt, ...) { return 0; } +inline int TraceC::printf(std::string tag, const char* fmt, ...) { return 0; } +# endif /* CVC4_TRACING */ + +#endif /* CVC4_MUZZLE */ // Disallow e.g. !Debug("foo").isOn() forms // because the ! will apply before the ? . @@ -418,65 +438,18 @@ public: #endif /* CVC4_TRACING */ -#else /* ! CVC4_MUZZLE */ - -class CVC4_PUBLIC ScopedDebug { -public: - ScopedDebug(std::string tag, bool newSetting = true) {} - ScopedDebug(const char* tag, bool newSetting = true) {} -};/* class ScopedDebug */ - -class CVC4_PUBLIC ScopedTrace { -public: - ScopedTrace(std::string tag, bool newSetting = true) {} - ScopedTrace(const char* tag, bool newSetting = true) {} -};/* class ScopedTrace */ - -extern NullDebugC Debug CVC4_PUBLIC; -extern NullC Warning CVC4_PUBLIC; -extern NullC Message CVC4_PUBLIC; -extern NullC Notice CVC4_PUBLIC; -extern NullC Chat CVC4_PUBLIC; -extern NullDebugC Trace CVC4_PUBLIC; - -#endif /* ! CVC4_MUZZLE */ - /** - * Same shape as DebugC/TraceC, but does nothing; designed for - * compilation of non-debug/non-trace builds. None of these should ever be called - * in such builds, but we offer this to the compiler so it doesn't complain. + * Does nothing; designed for compilation of non-debug/non-trace + * builds. None of these should ever be called in such builds, but we + * offer this to the compiler so it doesn't complain. */ -class CVC4_PUBLIC NullDebugC { -public: - operator bool() { return false; } - operator CVC4ostream() { return CVC4ostream(); } - operator std::ostream&() { return null_os; } -};/* class NullDebugC */ - -/** - * Same shape as WarningC/etc., but does nothing; designed for - * compilation of muzzled builds. None of these should ever be called - * in muzzled builds, but we offer this to the compiler so it doesn't - * complain. */ class CVC4_PUBLIC NullC { public: -/* - NullC() {} - NullC(std::ostream* os) {} - - int printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) { return 0; } - - std::ostream& operator()() { return null_os; } - - 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; extern NullC nullCvc4Stream CVC4_PUBLIC; }/* CVC4 namespace */ diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 3a9dd4418..91af11561 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -190,9 +190,9 @@ protected: void tearDown() { delete d_exprManager; } -}; +};/* class ParserBlack */ -class Cvc4ParserTest : public CxxTest::TestSuite, public ParserBlack { +class Cvc4ParserTest : public CxxTest::TestSuite, public ParserBlack { typedef ParserBlack super; public: @@ -236,6 +236,8 @@ public: } void testBadCvc4Inputs() { +// competition builds don't do any checking +#ifndef CVC4_COMPETITION_MODE tryBadInput("ASSERT;"); // no args tryBadInput("QUERY"); tryBadInput("CHECKSAT"); @@ -256,6 +258,7 @@ public: tryBadInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list = nil | cons(car:INT,cdr:list) END;"); tryBadInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list2 = nil END;"); tryBadInput("DATATYPE tree = node(data:(list,list,ARRAY trex OF list)), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;"); +#endif /* ! CVC4_COMPETITION_MODE */ } void testGoodCvc4Exprs() { @@ -267,14 +270,17 @@ public: } void testBadCvc4Exprs() { +// competition builds don't do any checking +#ifndef CVC4_COMPETITION_MODE tryBadInput("a AND"); // wrong arity tryBadInput("AND(a,b)"); // not infix tryBadInput("(OR (AND a b) c)"); // not infix tryBadInput("a IMPLIES b"); // should be => tryBadInput("a NOT b"); // wrong arity, not infix tryBadInput("a and b"); // wrong case +#endif /* ! CVC4_COMPETITION_MODE */ } -}; +};/* class Cvc4ParserTest */ class SmtParserTest : public CxxTest::TestSuite, public ParserBlack { typedef ParserBlack super; @@ -304,11 +310,14 @@ public: } void testBadSmtInputs() { +// competition builds don't do any checking +#ifndef CVC4_COMPETITION_MODE tryBadInput("(benchmark foo)"); // empty benchmark is not OK tryBadInput("(benchmark bar :assumption)"); // no args tryBadInput("(benchmark bar :formula)"); tryBadInput("(benchmark baz :extrapreds ( (a) (a) ) )"); // double decl tryBadInput("(benchmark zub :extrasorts (a) :extrapreds (p a))"); // (p a) needs parens +#endif /* ! CVC4_COMPETITION_MODE */ } void testGoodSmtExprs() { @@ -325,6 +334,8 @@ public: } void testBadSmtExprs() { +// competition builds don't do any checking +#ifndef CVC4_COMPETITION_MODE tryBadExpr("(and)"); // wrong arity tryBadExpr("(and a b"); // no closing paren tryBadExpr("(a and b)"); // infix @@ -336,8 +347,9 @@ public: tryBadExpr("(a b)"); // using non-function as function tryBadExpr(".5"); // rational constants must have integer prefix tryBadExpr("1."); // rational constants must have fractional suffix +#endif /* ! CVC4_COMPETITION_MODE */ } -}; +};/* class SmtParserTest */ class Smt2ParserTest : public CxxTest::TestSuite, public ParserBlack { typedef ParserBlack super; @@ -381,6 +393,8 @@ public: } void testBadSmt2Inputs() { +// competition builds don't do any checking +#ifndef CVC4_COMPETITION_MODE tryBadInput("(assert)"); // no args tryBadInput("(set-info :notes |Symbols can't contain the | character|)"); tryBadInput("(set-logic QF_UF) (check-sat true)"); // shouldn't have an arg @@ -390,6 +404,7 @@ public: // strict mode tryBadInput("(assert true)", true); // no set-logic, core theory symbol "true" undefined tryBadInput("(declare-fun p Bool)", true); // core theory symbol "Bool" undefined +#endif /* ! CVC4_COMPETITION_MODE */ } void testGoodSmt2Exprs() { @@ -408,6 +423,8 @@ public: } void testBadSmt2Exprs() { +// competition builds don't do any checking +#ifndef CVC4_COMPETITION_MODE tryBadExpr("(and)"); // wrong arity tryBadExpr("(and a b"); // no closing paren tryBadExpr("(a and b)"); // infix @@ -430,5 +447,6 @@ public: tryBadExpr("(and a)", true); // no unary and's tryBadExpr("(or a)", true); // no unary or's tryBadExpr("(* 5 01)", true); // '01' is not a valid integer constant +#endif /* ! CVC4_COMPETITION_MODE */ } -}; +};/* class Smt2ParserTest */ diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h index 183d8f7f1..61b1f40d2 100644 --- a/test/unit/util/output_black.h +++ b/test/unit/util/output_black.h @@ -219,29 +219,72 @@ public: } - static int expensiveFunction() { + static int failure() { // this represents an expensive function that should NOT be called // when debugging/tracing is turned off - TS_FAIL("a function was evaluated under Debug() or Trace() when it should not have been"); + TS_FAIL("a function was evaluated under an output operation when it should not have been"); return 0; } - void testEvaluationOffWhenItsSupposedToBe() { + void testEvaluationOffWhenItIsSupposedToBe() { + Debug.on("foo"); +#ifndef CVC4_DEBUG + TS_ASSERT( !( Debug.isOn("foo") ) ); + Debug("foo") << failure() << endl; + Debug.printf("foo", "%d\n", failure()); +#else /* ! CVC4_DEBUG */ + TS_ASSERT( Debug.isOn("foo") ); +#endif /* ! CVC4_DEBUG */ + Debug.off("foo"); + //Debug("foo") << failure() << endl; + //Debug.printf("foo", "%d\n", failure()); + Trace.on("foo"); #ifndef CVC4_TRACING TS_ASSERT( !( Trace.isOn("foo") ) ); - Trace("foo") << expensiveFunction() << endl; -#else /* CVC4_TRACING */ + Trace("foo") << failure() << endl; + Trace.printf("foo", "%d\n", failure()); +#else /* ! CVC4_TRACING */ TS_ASSERT( Trace.isOn("foo") ); -#endif /* CVC4_TRACING */ +#endif /* ! CVC4_TRACING */ + Trace.off("foo"); + //Trace("foo") << failure() << endl; + //Trace.printf("foo", "%d\n", failure()); - Debug.on("foo"); -#ifndef CVC4_DEBUG +#ifdef CVC4_MUZZLE TS_ASSERT( !( Debug.isOn("foo") ) ); - Debug("foo") << expensiveFunction() << endl; -#else /* CVC4_DEBUG */ - TS_ASSERT( Debug.isOn("foo") ); -#endif /* CVC4_DEBUG */ + TS_ASSERT( !( Trace.isOn("foo") ) ); + TS_ASSERT( !( Warning.isOn() ) ); + TS_ASSERT( !( Message.isOn() ) ); + TS_ASSERT( !( Notice.isOn() ) ); + TS_ASSERT( !( Chat.isOn() ) ); + + cout << "debug" << std::endl; + Debug("foo") << failure() << endl; + cout << "trace" << std::endl; + Trace("foo") << failure() << endl; + cout << "warning" << std::endl; + Warning() << failure() << endl; + cout << "message" << std::endl; + Message() << failure() << endl; + cout << "notice" << std::endl; + Notice() << failure() << endl; + cout << "chat" << std::endl; + Chat() << failure() << endl; + + cout << "debug:printf" << std::endl; + Debug.printf("foo", "%d\n", failure()); + cout << "trace:printf" << std::endl; + Trace.printf("foo", "%d\n", failure()); + cout << "warning:printf" << std::endl; + Warning.printf("%d\n", failure()); + cout << "message:printf" << std::endl; + Message.printf("%d\n", failure()); + cout << "notice:printf" << std::endl; + Notice.printf("%d\n", failure()); + cout << "chat:printf" << std::endl; + Chat.printf("%d\n", failure()); +#endif /* CVC4_MUZZLE */ } void testSimplePrint() { @@ -249,36 +292,36 @@ public: #ifdef CVC4_MUZZLE Debug.off("yo"); - Debug("yo", "foobar"); + Debug("yo") << "foobar"; TS_ASSERT_EQUALS(d_debugStream.str(), string()); d_debugStream.str(""); Debug.on("yo"); - Debug("yo", "baz foo"); + Debug("yo") << "baz foo"; TS_ASSERT_EQUALS(d_debugStream.str(), string()); d_debugStream.str(""); Trace.off("yo"); - Trace("yo", "foobar"); + Trace("yo") << "foobar"; TS_ASSERT_EQUALS(d_traceStream.str(), string()); d_traceStream.str(""); Trace.on("yo"); - Trace("yo", "baz foo"); + Trace("yo") << "baz foo"; TS_ASSERT_EQUALS(d_traceStream.str(), string()); d_traceStream.str(""); - Warning("baz foo"); + Warning() << "baz foo"; TS_ASSERT_EQUALS(d_warningStream.str(), string()); d_warningStream.str(""); - Chat("baz foo"); + Chat() << "baz foo"; TS_ASSERT_EQUALS(d_chatStream.str(), string()); d_chatStream.str(""); - Message("baz foo"); + Message() << "baz foo"; TS_ASSERT_EQUALS(d_messageStream.str(), string()); d_messageStream.str(""); - Notice("baz foo"); + Notice() << "baz foo"; TS_ASSERT_EQUALS(d_noticeStream.str(), string()); d_noticeStream.str(""); diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h index e44a016e6..d32ef828c 100644 --- a/test/unit/util/stats_black.h +++ b/test/unit/util/stats_black.h @@ -30,7 +30,7 @@ class StatsBlack : public CxxTest::TestSuite { public: void testStats() { - +#ifdef CVC4_STATISTICS_ON // StatisticsRegistry //static void flushStatistics(std::ostream& out); @@ -99,6 +99,7 @@ public: TS_ASSERT_EQUALS(zero, sTimer.getData()); sTimer.stop(); TS_ASSERT_LESS_THAN(zero, sTimer.getData()); +#endif /* CVC4_STATISTICS_ON */ } };