summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp6
-rw-r--r--src/theory/shared_term_manager.cpp6
-rw-r--r--src/util/output.cpp34
-rw-r--r--src/util/output.h125
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback