diff options
Diffstat (limited to 'src')
-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 |
4 files changed, 71 insertions, 100 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 */ |