diff options
| -rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 6 | ||||
| -rw-r--r-- | src/theory/shared_term_manager.cpp | 6 | ||||
| -rw-r--r-- | src/util/output.cpp | 34 | ||||
| -rw-r--r-- | src/util/output.h | 125 | ||||
| -rw-r--r-- | test/unit/parser/parser_black.h | 28 | ||||
| -rw-r--r-- | test/unit/util/output_black.h | 83 | ||||
| -rw-r--r-- | test/unit/util/stats_black.h | 3 |
7 files changed, 159 insertions, 126 deletions
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; i<possibleCons.size(); i++ ) { if( possibleCons[i] ){ - Assert( testerIndex==-1 ); + Assert( testerIndex==unsigned(-1) ); testerIndex = i; } } - Assert( testerIndex!=-1 ); + Assert( testerIndex!=unsigned(-1) ); assertionRep = NodeManager::currentNM()->mkNode( 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 <iostream> - #include "util/output.h" +#include <iostream> + 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 */ } }; |