summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/context/cdmap.h5
-rw-r--r--src/context/context.cpp59
-rw-r--r--src/context/context.h4
-rw-r--r--src/context/context_mm.cpp8
-rw-r--r--src/prop/prop_engine.cpp2
-rw-r--r--src/prop/sat.h17
-rw-r--r--src/theory/arith/arith_propagator.cpp2
-rw-r--r--src/theory/arith/theory_arith.cpp22
-rw-r--r--src/theory/theory_engine.cpp14
-rw-r--r--src/util/output.cpp34
-rw-r--r--src/util/output.h320
11 files changed, 273 insertions, 214 deletions
diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index b981628c5..45ff68a23 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -106,11 +106,6 @@ namespace context {
template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > class CDMap;
-template <class T, class U>
-inline std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) {
- return out << "[" << p.first << "," << p.second << "]";
-}
-
template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
class CDOmap : public ContextObj {
friend class CDMap<Key, Data, HashFcn>;
diff --git a/src/context/context.cpp b/src/context/context.cpp
index 994f644a7..0028aaad5 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -132,19 +132,15 @@ void Context::addNotifyObjPost(ContextNotifyObj* pCNO) {
void ContextObj::update() throw(AssertionException) {
- if(debugTagIsOn("context")) {
- Debug("context") << "before update(" << this << "):" << std::endl
- << *getContext() << std::endl;
- }
+ Debug("context") << "before update(" << this << "):" << std::endl
+ << *getContext() << std::endl;
// Call save() to save the information in the current object
ContextObj* pContextObjSaved = save(d_pScope->getCMM());
- if(debugTagIsOn("context")) {
- Debug("context") << "in update(" << this << ") with restore "
- << pContextObjSaved << ": waypoint 1" << std::endl
- << *getContext() << std::endl;
- }
+ Debug("context") << "in update(" << this << ") with restore "
+ << pContextObjSaved << ": waypoint 1" << std::endl
+ << *getContext() << std::endl;
// Check that base class data was saved
Assert( ( pContextObjSaved->d_pContextObjNext == d_pContextObjNext &&
@@ -173,11 +169,9 @@ void ContextObj::update() throw(AssertionException) {
Debug("context") << "in update(" << this
<< "): *prev() is now " << *prev() << std::endl;
- if(debugTagIsOn("context")) {
- Debug("context") << "in update(" << this << ") with restore "
- << pContextObjSaved << ": waypoint 3" << std::endl
- << *getContext() << std::endl;
- }
+ Debug("context") << "in update(" << this << ") with restore "
+ << pContextObjSaved << ": waypoint 3" << std::endl
+ << *getContext() << std::endl;
// Update Scope pointer to current top Scope
d_pScope = d_pScope->getContext()->getTopScope();
@@ -189,11 +183,9 @@ void ContextObj::update() throw(AssertionException) {
// Scope is popped.
d_pScope->addToChain(this);
- if(debugTagIsOn("context")) {
- Debug("context") << "after update(" << this << ") with restore "
- << pContextObjSaved << ":" << std::endl
- << *getContext() << std::endl;
- }
+ Debug("context") << "after update(" << this << ") with restore "
+ << pContextObjSaved << ":" << std::endl
+ << *getContext() << std::endl;
}
@@ -238,12 +230,11 @@ ContextObj* ContextObj::restoreAndContinue() throw(AssertionException) {
void ContextObj::destroy() throw(AssertionException) {
- if(debugTagIsOn("context")) {
- /* Context can be big and complicated, so we only want to process this output
- * if we're really going to use it. (Same goes below.) */
- Debug("context") << "before destroy " << this << " (level " << getLevel()
- << "):" << std::endl << *getContext() << std::endl;
- }
+ /* Context can be big and complicated, so we only want to process this output
+ * if we're really going to use it. (Same goes below.) */
+ Debug("context") << "before destroy " << this << " (level " << getLevel()
+ << "):" << std::endl << *getContext() << std::endl;
+
for(;;) {
// If valgrind reports invalid writes on the next few lines,
// here's a hint: make sure all classes derived from ContextObj in
@@ -256,18 +247,14 @@ void ContextObj::destroy() throw(AssertionException) {
if(d_pContextObjRestore == NULL) {
break;
}
- if(debugTagIsOn("context")) {
- Debug("context") << "in destroy " << this << ", restore object is "
- << d_pContextObjRestore << " at level "
- << d_pContextObjRestore->getLevel() << ":" << std::endl
- << *getContext() << std::endl;
- }
+ Debug("context") << "in destroy " << this << ", restore object is "
+ << d_pContextObjRestore << " at level "
+ << d_pContextObjRestore->getLevel() << ":" << std::endl
+ << *getContext() << std::endl;
restoreAndContinue();
}
- if(debugTagIsOn("context")) {
- Debug("context") << "after destroy " << this << ":" << std::endl
- << *getContext() << std::endl;
- }
+ Debug("context") << "after destroy " << this << ":" << std::endl
+ << *getContext() << std::endl;
}
@@ -318,7 +305,7 @@ ContextNotifyObj::~ContextNotifyObj() throw(AssertionException) {
std::ostream& operator<<(std::ostream& out,
const Context& context) throw(AssertionException) {
- const std::string separator(79, '-');
+ static const std::string separator(79, '-');
int level = context.d_scopeList.size() - 1;
typedef std::vector<Scope*>::const_reverse_iterator const_reverse_iterator;
diff --git a/src/context/context.h b/src/context/context.h
index 12d7c4673..1aa5fe44d 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -508,9 +508,7 @@ public:
* ContextMemoryManager as an argument.
*/
void deleteSelf() {
- if(debugTagIsOn("context")) {
- Debug("context") << "deleteSelf(" << this << ")" << std::endl;
- }
+ Debug("context") << "deleteSelf(" << this << ")" << std::endl;
this->~ContextObj();
::operator delete(this);
}
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp
index 6a277245e..5a1e52d66 100644
--- a/src/context/context_mm.cpp
+++ b/src/context/context_mm.cpp
@@ -88,11 +88,9 @@ void* ContextMemoryManager::newData(size_t size) {
AlwaysAssert(d_nextFree <= d_endChunk,
"Request is bigger than memory chunk size");
}
- if(debugTagIsOn("context")) {
- Debug("context") << "ContextMemoryManager::newData(" << size
- << ") returning " << res << " at level "
- << d_chunkList.size() << std::endl;
- }
+ Debug("context") << "ContextMemoryManager::newData(" << size
+ << ") returning " << res << " at level "
+ << d_chunkList.size() << std::endl;
return res;
}
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 7cccca177..c49d5f38a 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -122,7 +122,7 @@ Result PropEngine::checkSat() {
// Check the problem
bool result = d_satSolver->solve();
- if( result && debugTagIsOn("prop") ) {
+ if( result && Debug.isOn("prop") ) {
printSatisfyingAssignment();
}
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 9e09727e3..c58a198b3 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -237,7 +237,7 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
d_minisat->polarity_mode = minisat::SimpSolver::polarity_user;
// No random choices
- if(debugTagIsOn("no_rnd_decisions")){
+ if(Debug.isOn("no_rnd_decisions")){
d_minisat->random_var_freq = 0;
}
@@ -271,13 +271,15 @@ SatSolver::SatLiteralHashFunction::operator()(const SatLiteral& literal) const {
return hashSatLiteral(literal);
}
-inline std::ostream& operator <<(std::ostream& out, SatLiteral lit) {
- const char * s = (literalSign(lit)) ? "~" : " ";
- out << s << literalToVariable(lit);
+}/* CVC4::prop namespace */
+
+inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
+ const char * s = (prop::literalSign(lit)) ? "~" : " ";
+ out << s << prop::literalToVariable(lit);
return out;
}
-inline std::ostream& operator <<(std::ostream& out, const SatClause& clause) {
+inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& clause) {
out << "clause:";
for(int i = 0; i < clause.size(); ++i) {
out << " " << clause[i];
@@ -286,12 +288,11 @@ inline std::ostream& operator <<(std::ostream& out, const SatClause& clause) {
return out;
}
-inline std::ostream& operator <<(std::ostream& out, const SatLiteralValue& val) {
- out << stringOfLiteralValue(val);
+inline std::ostream& operator <<(std::ostream& out, prop::SatLiteralValue val) {
+ out << prop::stringOfLiteralValue(val);
return out;
}
-}/* CVC4::prop namespace */
}/* CVC4 namespace */
#endif /* __CVC4__PROP__SAT_H */
diff --git a/src/theory/arith/arith_propagator.cpp b/src/theory/arith/arith_propagator.cpp
index c5068c9fb..0f417bc41 100644
--- a/src/theory/arith/arith_propagator.cpp
+++ b/src/theory/arith/arith_propagator.cpp
@@ -122,7 +122,7 @@ std::vector<Node> ArithUnatePropagator::getImpliedLiterals(){
enqueueImpliedLiterals(assertion, impliedButNotAsserted);
}
- if(debugTagIsOn("arith::propagator")){
+ if(Debug.isOn("arith::propagator")){
for(std::vector<Node>::iterator i = impliedButNotAsserted.begin(),
endIter = impliedButNotAsserted.end(); i != endIter; ++i){
Node imp = *i;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 4d6a95eff..f11f38ab4 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -517,7 +517,7 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){
d_partialModel.setAssignment(x_i, v);
- if(debugTagIsOn("paranoid:check_tableau")){
+ if(Debug.isOn("paranoid:check_tableau")){
checkTableau();
}
}
@@ -562,7 +562,7 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
checkBasicVariable(x_j);
- if(debugTagIsOn("tableau")){
+ if(Debug.isOn("tableau")){
d_tableau.printTableau();
}
}
@@ -583,7 +583,7 @@ TNode TheoryArith::selectSmallestInconsistentVar(){
d_possiblyInconsistent.pop();
}
- if(debugTagIsOn("paranoid:variables")){
+ if(Debug.isOn("paranoid:variables")){
for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
basicIter != d_tableau.end();
++basicIter){
@@ -631,7 +631,7 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
static int iteratationNum = 0;
static const int EJECT_FREQUENCY = 10;
while(true){
- if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
+ if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
TNode x_i = selectSmallestInconsistentVar();
Debug("arith_update") << "selectSmallestInconsistentVar()=" << x_i << endl;
@@ -824,14 +824,14 @@ void TheoryArith::check(Effort level){
}
//TODO This must be done everytime for the time being
- if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
+ if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
Node possibleConflict = updateInconsistentVars();
if(possibleConflict != Node::null()){
d_partialModel.revertAssignmentChanges();
- if(debugTagIsOn("arith::print-conflict"))
+ if(Debug.isOn("arith::print-conflict"))
Debug("arith_conflict") << (possibleConflict) << std::endl;
d_out->conflict(possibleConflict);
@@ -840,12 +840,12 @@ void TheoryArith::check(Effort level){
}else{
d_partialModel.commitAssignmentChanges();
}
- if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
+ if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
Debug("arith") << "TheoryArith::check end" << std::endl;
- if(debugTagIsOn("arith::print_model")) {
+ if(Debug.isOn("arith::print_model")) {
Debug("arith::print_model") << "Model:" << endl;
for (unsigned i = 0; i < d_variables.size(); ++ i) {
@@ -856,7 +856,7 @@ void TheoryArith::check(Effort level){
Debug("arith::print_model") << endl;
}
}
- if(debugTagIsOn("arith::print_assertions")) {
+ if(Debug.isOn("arith::print_assertions")) {
Debug("arith::print_assertions") << "Assertions:" << endl;
for (unsigned i = 0; i < d_variables.size(); ++ i) {
Node x = d_variables[i];
@@ -874,8 +874,8 @@ void TheoryArith::check(Effort level){
/**
* This check is quite expensive.
- * It should be wrapped in a debugTagIsOn guard.
- * if(debugTagIsOn("paranoid:check_tableau")){
+ * It should be wrapped in a Debug.isOn() guard.
+ * if(Debug.isOn("paranoid:check_tableau")){
* checkTableau();
* }
*/
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 096c99c06..c4dc1c508 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -154,12 +154,10 @@ Node TheoryEngine::removeITEs(TNode node) {
nodeManager->mkNode(kind::EQUAL, skolem, node[2]));
nodeManager->setAttribute(node, theory::IteRewriteAttr(), skolem);
- if(debugTagIsOn("ite")){
- Debug("ite") << "removeITEs([" << node.getId() << "," << node << "])"
- << "->"
- << "["<<newAssertion.getId() << "," << newAssertion << "]"
- << endl;
- }
+ Debug("ite") << "removeITEs([" << node.getId() << "," << node << "])"
+ << "->"
+ << "["<<newAssertion.getId() << "," << newAssertion << "]"
+ << endl;
Node preprocessed = preprocess(newAssertion);
d_propEngine->assertFormula(preprocessed);
@@ -416,8 +414,8 @@ Node TheoryEngine::rewrite(TNode in, bool topLevel) {
* in the cache to make sure they are the same. This is
* especially necessary if a theory post-rewrites something into
* a term of another theory. */
- if(debugTagIsOn("extra-checking") &&
- !debugTagIsOn("$extra-checking:inside-rewrite")) {
+ if(Debug.isOn("extra-checking") &&
+ !Debug.isOn("$extra-checking:inside-rewrite")) {
ScopedDebug d("$extra-checking:inside-rewrite");
Node rewrittenAgain = rewrite(rse.d_node, rse.d_topLevel);
Assert(rewrittenAgain == rse.d_node,
diff --git a/src/util/output.cpp b/src/util/output.cpp
index 501ef52fd..8a0bdd298 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -33,12 +33,22 @@ NullC nullCvc4Stream CVC4_PUBLIC;
#ifndef CVC4_MUZZLE
-DebugC DebugOut(&cout);
-WarningC WarningOut(&cerr);
-MessageC MessageOut(&cout);
-NoticeC NoticeOut(&cout);
-ChatC ChatOut(&cout);
-TraceC TraceOut(&cout);
+#ifdef CVC4_DEBUG
+DebugC Debug CVC4_PUBLIC (&cout);
+#else /* CVC4_DEBUG */
+NullDebugC Debug CVC4_PUBLIC;
+#endif /* CVC4_DEBUG */
+
+WarningC Warning CVC4_PUBLIC (&cerr);
+MessageC Message CVC4_PUBLIC (&cout);
+NoticeC Notice CVC4_PUBLIC (&cout);
+ChatC Chat CVC4_PUBLIC (&cout);
+
+#ifdef CVC4_TRACING
+TraceC Trace CVC4_PUBLIC (&cout);
+#else /* CVC4_TRACING */
+NullDebugC Trace CVC4_PUBLIC;
+#endif /* CVC4_TRACING */
void DebugC::printf(const char* tag, const char* fmt, ...) {
if(d_tags.find(string(tag)) != d_tags.end()) {
@@ -128,6 +138,16 @@ void TraceC::printf(string tag, const char* fmt, ...) {
}
}
-#endif /* CVC4_MUZZLE */
+#else /* ! CVC4_MUZZLE */
+
+NullDebugC Debug CVC4_PUBLIC;
+NullC Warning CVC4_PUBLIC;
+NullC Warning CVC4_PUBLIC;
+NullC Message CVC4_PUBLIC;
+NullC Notice CVC4_PUBLIC;
+NullC Chat CVC4_PUBLIC;
+NullDebugC Trace CVC4_PUBLIC;
+
+#endif /* ! CVC4_MUZZLE */
}/* CVC4 namespace */
diff --git a/src/util/output.h b/src/util/output.h
index 851868c15..355d15760 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -29,6 +29,14 @@
namespace CVC4 {
+template <class T, class U>
+std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) CVC4_PUBLIC;
+
+template <class T, class U>
+std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) {
+ return out << "[" << p.first << "," << p.second << "]";
+}
+
/**
* A utility class to provide (essentially) a "/dev/null" streambuf.
* If debugging support is compiled in, but debugging for
@@ -36,7 +44,7 @@ namespace CVC4 {
* attached to a null_streambuf instance so that output is directed to
* the bit bucket.
*/
-class null_streambuf : public std::streambuf {
+class CVC4_PUBLIC null_streambuf : public std::streambuf {
public:
/* Overriding overflow() just ensures that EOF isn't returned on the
* stream. Perhaps this is not so critical, but recommended; this
@@ -50,12 +58,129 @@ extern null_streambuf null_sb;
/** A null output stream singleton */
extern std::ostream null_os CVC4_PUBLIC;
+class CVC4_PUBLIC NullCVC4ostream {
+public:
+ void flush() {}
+ bool isConnected() { return false; }
+ operator std::ostream&() { return null_os; }
+
+ template <class T>
+ NullCVC4ostream& operator<<(T const& t) { return *this; }
+
+ // support manipulators, endl, etc..
+ NullCVC4ostream& operator<<(std::ostream& (*pf)(std::ostream&)) { return *this; }
+ NullCVC4ostream& operator<<(std::ios& (*pf)(std::ios&)) { return *this; }
+ NullCVC4ostream& operator<<(std::ios_base& (*pf)(std::ios_base&)) { return *this; }
+};/* class NullCVC4ostream */
+
+/**
+ * Same shape as DebugC/TraceC, 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 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) {}
+
+ void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) {}
+ void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) {}
+
+ NullCVC4ostream operator()(const char* tag) { return NullCVC4ostream(); }
+ NullCVC4ostream operator()(std::string tag) { return NullCVC4ostream(); }
+
+ 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; }
+};/* 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) {}
+
+ void operator()(const char*) {}
+ void operator()(std::string) {}
+
+ void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) {}
+
+ NullCVC4ostream operator()() { return NullCVC4ostream(); }
+
+ void setStream(std::ostream& os) {}
+ std::ostream& getStream() { return null_os; }
+};/* class NullC */
+
+extern NullDebugC debugNullCvc4Stream CVC4_PUBLIC;
+extern NullC nullCvc4Stream CVC4_PUBLIC;
+
#ifndef CVC4_MUZZLE
+class CVC4_PUBLIC CVC4ostream {
+ std::ostream* d_os;
+public:
+ CVC4ostream() : d_os(NULL) {}
+ CVC4ostream(std::ostream* os) : d_os(os) {}
+
+ void flush() {
+ if(d_os != NULL) {
+ d_os->flush();
+ }
+ }
+
+ bool isConnected() { return d_os != NULL; }
+ operator std::ostream&() { return isConnected() ? *d_os : null_os; }
+
+ template <class T>
+ CVC4ostream& operator<<(T const& t) {
+ if(d_os != NULL) {
+ d_os = &(*d_os << t);
+ }
+ return *this;
+ }
+
+ // support manipulators, endl, etc..
+ CVC4ostream& operator<<(std::ostream& (*pf)(std::ostream&)) {
+ if(d_os != NULL) {
+ d_os = &(*d_os << pf);
+ }
+ return *this;
+ }
+ CVC4ostream& operator<<(std::ios& (*pf)(std::ios&)) {
+ if(d_os != NULL) {
+ d_os = &(*d_os << pf);
+ }
+ return *this;
+ }
+ CVC4ostream& operator<<(std::ios_base& (*pf)(std::ios_base&)) {
+ if(d_os != NULL) {
+ d_os = &(*d_os << pf);
+ }
+ return *this;
+ }
+
+};/* class CVC4ostream */
+
/** The debug output class */
class CVC4_PUBLIC DebugC {
std::set<std::string> d_tags;
- std::ostream *d_os;
+ std::ostream* d_os;
public:
DebugC(std::ostream* os) : d_os(os) {}
@@ -87,25 +212,25 @@ public:
void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
- std::ostream& operator()(const char* tag) {
+ CVC4ostream operator()(const char* tag) {
if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
- return *d_os;
+ return CVC4ostream(d_os);
} else {
- return null_os;
+ return CVC4ostream();
}
}
- std::ostream& operator()(std::string tag) {
+ CVC4ostream operator()(std::string tag) {
if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
- return *d_os;
+ return CVC4ostream(d_os);
} else {
- return null_os;
+ return CVC4ostream();
}
}
/**
* The "Yeting option" - this allows use of Debug() without a tag
* for temporary (file-only) debugging.
*/
- std::ostream& operator()();
+ CVC4ostream operator()();
void on (const char* tag) { d_tags.insert(std::string(tag)); }
void on (std::string tag) { d_tags.insert(tag); }
@@ -117,19 +242,11 @@ public:
void setStream(std::ostream& os) { d_os = &os; }
std::ostream& getStream() { return *d_os; }
-};/* class Debug */
-
-/** The debug output singleton */
-extern DebugC DebugOut CVC4_PUBLIC;
-#ifdef CVC4_DEBUG
-# define Debug DebugOut
-#else /* CVC4_DEBUG */
-# define Debug if(0) debugNullCvc4Stream
-#endif /* CVC4_DEBUG */
+};/* class DebugC */
/** The warning output class */
class CVC4_PUBLIC WarningC {
- std::ostream *d_os;
+ std::ostream* d_os;
public:
WarningC(std::ostream* os) : d_os(os) {}
@@ -139,19 +256,15 @@ public:
void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
- std::ostream& operator()() { return *d_os; }
+ CVC4ostream operator()() { return CVC4ostream(d_os); }
void setStream(std::ostream& os) { d_os = &os; }
std::ostream& getStream() { return *d_os; }
-};/* class Warning */
-
-/** The warning output singleton */
-extern WarningC WarningOut CVC4_PUBLIC;
-#define Warning WarningOut
+};/* class WarningC */
/** The message output class */
class CVC4_PUBLIC MessageC {
- std::ostream *d_os;
+ std::ostream* d_os;
public:
MessageC(std::ostream* os) : d_os(os) {}
@@ -161,19 +274,15 @@ public:
void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
- std::ostream& operator()() { return *d_os; }
+ CVC4ostream operator()() { return CVC4ostream(d_os); }
void setStream(std::ostream& os) { d_os = &os; }
std::ostream& getStream() { return *d_os; }
-};/* class Message */
-
-/** The message output singleton */
-extern MessageC MessageOut CVC4_PUBLIC;
-#define Message MessageOut
+};/* class MessageC */
/** The notice output class */
class CVC4_PUBLIC NoticeC {
- std::ostream *d_os;
+ std::ostream* d_os;
public:
NoticeC(std::ostream* os) : d_os(os) {}
@@ -183,19 +292,15 @@ public:
void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
- std::ostream& operator()() { return *d_os; }
+ CVC4ostream operator()() { return CVC4ostream(d_os); }
void setStream(std::ostream& os) { d_os = &os; }
std::ostream& getStream() { return *d_os; }
-};/* class Notice */
-
-/** The notice output singleton */
-extern NoticeC NoticeOut CVC4_PUBLIC;
-#define Notice NoticeOut
+};/* class NoticeC */
/** The chat output class */
class CVC4_PUBLIC ChatC {
- std::ostream *d_os;
+ std::ostream* d_os;
public:
ChatC(std::ostream* os) : d_os(os) {}
@@ -205,19 +310,15 @@ public:
void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
- std::ostream& operator()() { return *d_os; }
+ CVC4ostream operator()() { return CVC4ostream(d_os); }
void setStream(std::ostream& os) { d_os = &os; }
std::ostream& getStream() { return *d_os; }
-};/* class Chat */
-
-/** The chat output singleton */
-extern ChatC ChatOut CVC4_PUBLIC;
-#define Chat ChatOut
+};/* class ChatC */
/** The trace output class */
class CVC4_PUBLIC TraceC {
- std::ostream *d_os;
+ std::ostream* d_os;
std::set<std::string> d_tags;
public:
@@ -250,19 +351,19 @@ public:
void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
- std::ostream& operator()(const char* tag) {
+ CVC4ostream operator()(const char* tag) {
if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
- return *d_os;
+ return CVC4ostream(d_os);
} else {
- return null_os;
+ return CVC4ostream();
}
}
- std::ostream& operator()(std::string tag) {
+ CVC4ostream operator()(std::string tag) {
if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
- return *d_os;
+ return CVC4ostream(d_os);
} else {
- return null_os;
+ return CVC4ostream();
}
}
@@ -276,14 +377,29 @@ public:
void setStream(std::ostream& os) { d_os = &os; }
std::ostream& getStream() { return *d_os; }
-};/* class Trace */
+};/* class TraceC */
+
+/** The debug output singleton */
+#ifdef CVC4_DEBUG
+extern DebugC Debug CVC4_PUBLIC;
+#else /* CVC4_DEBUG */
+extern NullDebugC Debug CVC4_PUBLIC;
+#endif /* CVC4_DEBUG */
+
+/** The warning output singleton */
+extern WarningC Warning CVC4_PUBLIC;
+/** The message output singleton */
+extern MessageC Message CVC4_PUBLIC;
+/** The notice output singleton */
+extern NoticeC Notice CVC4_PUBLIC;
+/** The chat output singleton */
+extern ChatC Chat CVC4_PUBLIC;
/** The trace output singleton */
-extern TraceC TraceOut CVC4_PUBLIC;
#ifdef CVC4_TRACING
-# define Trace TraceOut
+extern TraceC Trace CVC4_PUBLIC;
#else /* CVC4_TRACING */
-# define Trace if(0) debugNullCvc4Stream
+extern NullDebugC Trace CVC4_PUBLIC;
#endif /* CVC4_TRACING */
#ifdef CVC4_DEBUG
@@ -296,11 +412,11 @@ public:
ScopedDebug(std::string tag, bool newSetting = true) :
d_tag(tag) {
- d_oldSetting = DebugOut.isOn(d_tag);
+ d_oldSetting = Debug.isOn(d_tag);
if(newSetting) {
- DebugOut.on(d_tag);
+ Debug.on(d_tag);
} else {
- DebugOut.off(d_tag);
+ Debug.off(d_tag);
}
}
@@ -382,13 +498,6 @@ public:
#else /* ! CVC4_MUZZLE */
-# define Debug if(0) debugNullCvc4Stream
-# define Warning if(0) nullCvc4Stream
-# define Message if(0) nullCvc4Stream
-# define Notice if(0) nullCvc4Stream
-# define Chat if(0) nullCvc4Stream
-# define Trace if(0) debugNullCvc4Stream
-
class CVC4_PUBLIC ScopedDebug {
public:
ScopedDebug(std::string tag, bool newSetting = true) {}
@@ -401,72 +510,25 @@ public:
ScopedTrace(const char* tag, bool newSetting = true) {}
};/* class ScopedTrace */
-#endif /* ! CVC4_MUZZLE */
-
-/**
- * Same shape as DebugC/TraceC, 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 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) {}
+extern NullDebugC Debug CVC4_PUBLIC;
+extern NullC Warning 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;
- void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) {}
- void 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; }
-};/* 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) {}
-
- void operator()(const char*) {}
- void operator()(std::string) {}
-
- void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) {}
-
- std::ostream& operator()() { return null_os; }
-
- void setStream(std::ostream& os) {}
- std::ostream& getStream() { return null_os; }
-};/* class NullC */
-
-extern NullDebugC debugNullCvc4Stream CVC4_PUBLIC;
-extern NullC nullCvc4Stream CVC4_PUBLIC;
+#endif /* ! CVC4_MUZZLE */
+// don't use debugTagIsOn() anymore, use Debug.isOn()
+inline bool debugTagIsOn(std::string tag) __attribute__((__deprecated__));
inline bool debugTagIsOn(std::string tag) {
-#ifdef CVC4_DEBUG
- return DebugOut.isOn(tag);
-#else
+#if defined(CVC4_DEBUG) && !defined(CVC4_MUZZLE)
+ return Debug.isOn(tag);
+#else /* CVC4_DEBUG && !CVC4_MUZZLE */
return false;
-#endif
-}
+#endif /* CVC4_DEBUG && !CVC4_MUZZLE */
+}/* debugTagIsOn() */
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback