summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/expr/attribute_internals.h73
-rw-r--r--src/lib/clock_gettime.h4
-rw-r--r--src/main/interactive_shell.cpp8
-rw-r--r--src/prop/minisat/core/Solver.cc6
-rw-r--r--src/prop/prop_engine.cpp5
-rw-r--r--src/theory/theory_engine.h11
-rw-r--r--src/theory/theory_traits_template.h25
-rw-r--r--src/theory/valuation.cpp10
-rw-r--r--src/theory/valuation.h12
-rw-r--r--src/util/output.cpp120
-rw-r--r--src/util/output.h298
11 files changed, 244 insertions, 328 deletions
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index bd3e6eeba..1df8da63e 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): taking, dejan, cconway
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
@@ -445,44 +445,6 @@ class CDAttrHash<bool> :
};/* class CDAttrHash<bool>::BitAccessor */
/**
- * A (somewhat degenerate) iterator over boolean-valued attributes.
- * This iterator doesn't support anything except comparison and
- * dereference. It's intended just for the result of find() on the
- * table.
- */
- class BitIterator {
-
- super* d_map;
-
- std::pair<NodeValue* const, uint64_t>* d_entry;
-
- unsigned d_bit;
-
- public:
-
- BitIterator() :
- d_map(NULL),
- d_entry(NULL),
- d_bit(0) {
- }
-
- BitIterator(super& map, std::pair<NodeValue* const, uint64_t>& entry, unsigned bit) :
- d_map(&map),
- d_entry(&entry),
- d_bit(bit) {
- }
-
- std::pair<NodeValue* const, BitAccessor> operator*() {
- return std::make_pair(d_entry->first,
- BitAccessor(*d_map, d_entry->first, d_entry->second, d_bit));
- }
-
- bool operator==(const BitIterator& b) {
- return d_entry == b.d_entry && d_bit == b.d_bit;
- }
- };/* class CDAttrHash<bool>::BitIterator */
-
- /**
* A (somewhat degenerate) const_iterator over boolean-valued
* attributes. This const_iterator doesn't support anything except
* comparison and dereference. It's intended just for the result of
@@ -530,7 +492,7 @@ public:
typedef std::pair<const key_type, data_type> value_type;
/** an iterator type; see above for limitations */
- typedef BitIterator iterator;
+ typedef ConstBitIterator iterator;
/** a const_iterator type; see above for limitations */
typedef ConstBitIterator const_iterator;
@@ -538,28 +500,6 @@ public:
* Find the boolean value in the hash table. Returns something ==
* end() if not found.
*/
- /*BitIterator find(const std::pair<uint64_t, NodeValue*>& k) {
- super::iterator i = super::find(k.second);
- if(i == super::end()) {
- return BitIterator();
- }
- Debug.printf("cdboolattr",
- "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
- &(*i).second,
- (unsigned long long)((*i).second),
- unsigned(k.first));
- return BitIterator(*i, k.first);
- }*/
-
- /** The "off the end" iterator */
- BitIterator end() {
- return BitIterator();
- }
-
- /**
- * Find the boolean value in the hash table. Returns something ==
- * end() if not found.
- */
ConstBitIterator find(const std::pair<uint64_t, NodeValue*>& k) const {
super::const_iterator i = super::find(k.second);
if(i == super::end()) {
@@ -588,14 +528,19 @@ public:
}
/**
- * Delete all flags from the given node.
+ * Delete all flags from the given node. Simply calls superclass's
+ * obliterate(). Note this removes all attributes at all context
+ * levels for this NodeValue! This is important when the NodeValue
+ * is no longer referenced and is being collected, but otherwise
+ * it probably isn't useful to do this.
*/
void erase(NodeValue* nv) {
super::obliterate(nv);
}
/**
- * Clear the hash table.
+ * Clear the hash table. This simply exposes the protected superclass
+ * version of clear() to clients.
*/
void clear() {
super::clear();
diff --git a/src/lib/clock_gettime.h b/src/lib/clock_gettime.h
index e419e16b0..e158ff836 100644
--- a/src/lib/clock_gettime.h
+++ b/src/lib/clock_gettime.h
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
@@ -16,6 +16,8 @@
** Replacement for clock_gettime() for systems without it (like Mac OS X).
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__LIB__CLOCK_GETTIME_H
#define __CVC4__LIB__CLOCK_GETTIME_H
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index b2c8b8c1d..f99eef4a1 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -2,10 +2,10 @@
/*! \file interactive_shell.cpp
** \verbatim
** Original author: cconway
- ** Major contributors:
- ** Minor contributors (to current version):
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
@@ -98,7 +98,7 @@ Command* InteractiveShell::readCommand() {
}
/* Extract the newline delimiter from the stream too */
- int c = d_in.get();
+ int c CVC4_UNUSED = d_in.get();
Assert( c == '\n' );
// cout << "Next char is '" << (char)c << "'" << endl << flush;
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 6703a44be..4781fd8cf 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -266,7 +266,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type)
void Solver::attachClause(CRef cr) {
const Clause& c = ca[cr];
- CVC4::Debug("minisat") << "Solver::attachClause(" << c << ")" << std::endl;
+ Debug("minisat") << "Solver::attachClause(" << c << ")" << std::endl;
Assert(c.size() > 1);
watches[~c[0]].push(Watcher(cr, c[1]));
watches[~c[1]].push(Watcher(cr, c[0]));
@@ -276,7 +276,7 @@ void Solver::attachClause(CRef cr) {
void Solver::detachClause(CRef cr, bool strict) {
const Clause& c = ca[cr];
- CVC4::Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl;
+ Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl;
assert(c.size() > 1);
if (strict){
@@ -294,7 +294,7 @@ void Solver::detachClause(CRef cr, bool strict) {
void Solver::removeClause(CRef cr) {
Clause& c = ca[cr];
- CVC4::Debug("minisat") << "Solver::removeClause(" << c << ")" << std::endl;
+ Debug("minisat") << "Solver::removeClause(" << c << ")" << std::endl;
detachClause(cr);
// Don't leave pointers to free'd memory!
if (locked(c)) vardata[var(c[0])].reason = CRef_Undef;
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 4939ecb43..d64aadc96 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -5,7 +5,7 @@
** Major contributors: cconway, dejan
** Minor contributors (to current version): taking
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
@@ -137,8 +137,7 @@ Result PropEngine::checkSat() {
}
Node PropEngine::getValue(TNode node) {
- Assert(node.getKind() == kind::VARIABLE &&
- node.getType().isBoolean());
+ Assert(node.getType().isBoolean());
SatLiteralValue v = d_satSolver->value(d_cnfStream->getLiteral(node));
if(v == l_True) {
return NodeManager::currentNM()->mkConst(true);
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 787323495..b773a84ee 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -2,10 +2,10 @@
/*! \file theory_engine.h
** \verbatim
** Original author: mdeters
- ** Major contributors: dejan, taking
+ ** Major contributors: taking, dejan
** Minor contributors (to current version): cconway, barrett
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
@@ -191,6 +191,13 @@ public:
}
/**
+ * Get a pointer to the underlying propositional engine.
+ */
+ prop::PropEngine* getPropEngine() const {
+ return d_propEngine;
+ }
+
+ /**
* Return whether or not we are incomplete (in the current context).
*/
bool isIncomplete() {
diff --git a/src/theory/theory_traits_template.h b/src/theory/theory_traits_template.h
index 067fe55d0..c6541dbea 100644
--- a/src/theory/theory_traits_template.h
+++ b/src/theory/theory_traits_template.h
@@ -1,12 +1,25 @@
-/*
- * theory_traits_template.h
- *
- * Created on: Dec 23, 2010
- * Author: dejan
- */
+/********************* */
+/*! \file theory_traits_template.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
#pragma once
+#include "cvc4_private.h"
#include "theory/theory.h"
${theory_includes}
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 20d339b52..1f82f1404 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
@@ -27,5 +27,13 @@ Node Valuation::getValue(TNode n) {
return d_engine->getValue(n);
}
+Node Valuation::getSatValue(TNode n) {
+ if(n.getKind() == kind::NOT) {
+ return NodeManager::currentNM()->mkConst(! d_engine->getPropEngine()->getValue(n[0]).getConst<bool>());
+ } else {
+ return d_engine->getPropEngine()->getValue(n);
+ }
+}
+
}/* CVC4::theory namespace */
}/* CVC4 namespace */
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 2d38c29cd..94c2bc12f 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
@@ -40,6 +40,16 @@ public:
Node getValue(TNode n);
+ /**
+ * Get the current SAT assignment to the node n.
+ *
+ * This is only permitted if n is a theory atom that has an associated
+ * SAT literal (or its negation).
+ *
+ * @return Node::null() if no current assignment; otherwise true or false.
+ */
+ Node getSatValue(TNode n);
+
};/* class Valuation */
}/* CVC4::theory namespace */
diff --git a/src/util/output.cpp b/src/util/output.cpp
index 34a3af93e..080409ed8 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
@@ -34,109 +34,115 @@ NullC nullCvc4Stream CVC4_PUBLIC;
#ifndef CVC4_MUZZLE
-#ifdef CVC4_DEBUG
-DebugC Debug CVC4_PUBLIC (&cout);
-#else /* CVC4_DEBUG */
-NullDebugC Debug CVC4_PUBLIC;
-#endif /* CVC4_DEBUG */
-
+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);
+TraceC TraceChannel 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()) {
- // chop off output after 1024 bytes
- char buf[1024];
- va_list vl;
- va_start(vl, fmt);
- vsnprintf(buf, sizeof(buf), fmt, vl);
- va_end(vl);
- *d_os << buf;
+int DebugC::printf(const char* tag, const char* fmt, ...) {
+ if(d_tags.find(string(tag)) == d_tags.end()) {
+ return 0;
}
+
+ // chop off output after 1024 bytes
+ char buf[1024];
+ va_list vl;
+ va_start(vl, fmt);
+ int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+ va_end(vl);
+ *d_os << buf;
+ return retval;
}
-void DebugC::printf(std::string tag, const char* fmt, ...) {
- if(d_tags.find(tag) != d_tags.end()) {
- // chop off output after 1024 bytes
- char buf[1024];
- va_list vl;
- va_start(vl, fmt);
- vsnprintf(buf, sizeof(buf), fmt, vl);
- va_end(vl);
- *d_os << buf;
+int DebugC::printf(std::string tag, const char* fmt, ...) {
+ if(d_tags.find(tag) == d_tags.end()) {
+ return 0;
}
+
+ // chop off output after 1024 bytes
+ char buf[1024];
+ va_list vl;
+ va_start(vl, fmt);
+ int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+ va_end(vl);
+ *d_os << buf;
+ return retval;
}
-void WarningC::printf(const char* fmt, ...) {
+int WarningC::printf(const char* fmt, ...) {
// chop off output after 1024 bytes
char buf[1024];
va_list vl;
va_start(vl, fmt);
- vsnprintf(buf, sizeof(buf), fmt, vl);
+ int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
va_end(vl);
*d_os << buf;
+ return retval;
}
-void MessageC::printf(const char* fmt, ...) {
+int MessageC::printf(const char* fmt, ...) {
// chop off output after 1024 bytes
char buf[1024];
va_list vl;
va_start(vl, fmt);
- vsnprintf(buf, sizeof(buf), fmt, vl);
+ int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
va_end(vl);
*d_os << buf;
+ return retval;
}
-void NoticeC::printf(const char* fmt, ...) {
+int NoticeC::printf(const char* fmt, ...) {
// chop off output after 1024 bytes
char buf[1024];
va_list vl;
va_start(vl, fmt);
- vsnprintf(buf, sizeof(buf), fmt, vl);
+ int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
va_end(vl);
*d_os << buf;
+ return retval;
}
-void ChatC::printf(const char* fmt, ...) {
+int ChatC::printf(const char* fmt, ...) {
// chop off output after 1024 bytes
char buf[1024];
va_list vl;
va_start(vl, fmt);
- vsnprintf(buf, sizeof(buf), fmt, vl);
+ int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
va_end(vl);
*d_os << buf;
+ return retval;
}
-void TraceC::printf(const char* tag, const char* fmt, ...) {
- if(d_tags.find(string(tag)) != d_tags.end()) {
- // chop off output after 1024 bytes
- char buf[1024];
- va_list vl;
- va_start(vl, fmt);
- vsnprintf(buf, sizeof(buf), fmt, vl);
- va_end(vl);
- *d_os << buf;
+int TraceC::printf(const char* tag, const char* fmt, ...) {
+ if(d_tags.find(string(tag)) == d_tags.end()) {
+ return 0;
}
+
+ // chop off output after 1024 bytes
+ char buf[1024];
+ va_list vl;
+ va_start(vl, fmt);
+ int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+ va_end(vl);
+ *d_os << buf;
+ return retval;
}
-void TraceC::printf(std::string tag, const char* fmt, ...) {
- if(d_tags.find(tag) != d_tags.end()) {
- // chop off output after 1024 bytes
- char buf[1024];
- va_list vl;
- va_start(vl, fmt);
- vsnprintf(buf, sizeof(buf), fmt, vl);
- va_end(vl);
- *d_os << buf;
+int TraceC::printf(std::string tag, const char* fmt, ...) {
+ if(d_tags.find(tag) == d_tags.end()) {
+ return 0;
}
+
+ // chop off output after 1024 bytes
+ char buf[1024];
+ va_list vl;
+ va_start(vl, fmt);
+ int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+ va_end(vl);
+ *d_os << buf;
+ return retval;
}
#else /* ! CVC4_MUZZLE */
diff --git a/src/util/output.h b/src/util/output.h
index 9efb4110e..b205d1d37 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -3,9 +3,9 @@
** \verbatim
** Original author: mdeters
** Major contributors: none
- ** Minor contributors (to current version): cconway
+ ** Minor contributors (to current version): cconway, taking, dejan
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
@@ -58,78 +58,6 @@ 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 {
@@ -141,11 +69,11 @@ class CVC4_PUBLIC CVC4ostream {
public:
CVC4ostream() : d_os(NULL) {}
- CVC4ostream(std::ostream* os) : d_os(os), d_indent(0) {
+ explicit CVC4ostream(std::ostream* os) : d_os(os), d_indent(0) {
d_endl = &std::endl;
}
- void pushIndent() { d_indent ++; };
+ void pushIndent() { d_indent ++; }
void popIndent() { if (d_indent > 0) -- d_indent; }
void flush() {
@@ -195,14 +123,12 @@ public:
}
};/* class CVC4ostream */
-inline CVC4ostream& push(CVC4ostream& stream)
-{
+inline CVC4ostream& push(CVC4ostream& stream) {
stream.pushIndent();
return stream;
}
-inline CVC4ostream& pop(CVC4ostream& stream)
-{
+inline CVC4ostream& pop(CVC4ostream& stream) {
stream.popIndent();
return stream;
}
@@ -213,34 +139,10 @@ class CVC4_PUBLIC DebugC {
std::ostream* d_os;
public:
- DebugC(std::ostream* os) : d_os(os) {}
-
- void operator()(const char* tag, const char* s) {
- if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
- *d_os << s;
- }
- }
-
- void operator()(const char* tag, const std::string& s) {
- if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
- *d_os << s;
- }
- }
-
- void operator()(const std::string& tag, const char* s) {
- if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
- *d_os << s;
- }
- }
-
- void operator()(const std::string& tag, const std::string& s) {
- if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
- *d_os << s;
- }
- }
+ explicit DebugC(std::ostream* os) : d_os(os) {}
- 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)));
+ int printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
+ int printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
CVC4ostream operator()(const char* tag) {
if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
@@ -256,21 +158,16 @@ public:
return CVC4ostream();
}
}
- /**
- * The "Yeting option" - this allows use of Debug() without a tag
- * for temporary (file-only) debugging.
- */
- CVC4ostream operator()();
- void on (const char* tag) { d_tags.insert(std::string(tag)); }
- void on (std::string tag) { d_tags.insert(tag); }
- void off(const char* tag) { d_tags.erase (std::string(tag)); }
- void off(std::string tag) { d_tags.erase (tag); }
+ bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; }
+ bool on (std::string tag) { d_tags.insert(tag); return true; }
+ bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; }
+ bool off(std::string tag) { d_tags.erase (tag); return false; }
bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); }
bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
- void setStream(std::ostream& os) { d_os = &os; }
+ std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
std::ostream& getStream() { return *d_os; }
};/* class DebugC */
@@ -279,16 +176,13 @@ class CVC4_PUBLIC WarningC {
std::ostream* d_os;
public:
- WarningC(std::ostream* os) : d_os(os) {}
+ explicit WarningC(std::ostream* os) : d_os(os) {}
- void operator()(const char* s) { *d_os << s; }
- void operator()(std::string s) { *d_os << s; }
-
- void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+ int printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
CVC4ostream operator()() { return CVC4ostream(d_os); }
- void setStream(std::ostream& os) { d_os = &os; }
+ std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
std::ostream& getStream() { return *d_os; }
};/* class WarningC */
@@ -297,16 +191,13 @@ class CVC4_PUBLIC MessageC {
std::ostream* d_os;
public:
- MessageC(std::ostream* os) : d_os(os) {}
-
- void operator()(const char* s) { *d_os << s; }
- void operator()(std::string s) { *d_os << s; }
+ explicit MessageC(std::ostream* os) : d_os(os) {}
- void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+ int printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
CVC4ostream operator()() { return CVC4ostream(d_os); }
- void setStream(std::ostream& os) { d_os = &os; }
+ std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
std::ostream& getStream() { return *d_os; }
};/* class MessageC */
@@ -315,16 +206,13 @@ class CVC4_PUBLIC NoticeC {
std::ostream* d_os;
public:
- NoticeC(std::ostream* os) : d_os(os) {}
-
- void operator()(const char* s) { *d_os << s; }
- void operator()(std::string s) { *d_os << s; }
+ explicit NoticeC(std::ostream* os) : d_os(os) {}
- void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+ int printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
CVC4ostream operator()() { return CVC4ostream(d_os); }
- void setStream(std::ostream& os) { d_os = &os; }
+ std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
std::ostream& getStream() { return *d_os; }
};/* class NoticeC */
@@ -333,16 +221,13 @@ class CVC4_PUBLIC ChatC {
std::ostream* d_os;
public:
- ChatC(std::ostream* os) : d_os(os) {}
+ explicit ChatC(std::ostream* os) : d_os(os) {}
- void operator()(const char* s) { *d_os << s; }
- void operator()(std::string s) { *d_os << s; }
-
- void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+ int printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
CVC4ostream operator()() { return CVC4ostream(d_os); }
- void setStream(std::ostream& os) { d_os = &os; }
+ std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
std::ostream& getStream() { return *d_os; }
};/* class ChatC */
@@ -352,34 +237,10 @@ class CVC4_PUBLIC TraceC {
std::set<std::string> d_tags;
public:
- TraceC(std::ostream* os) : d_os(os) {}
-
- void operator()(const char* tag, const char* s) {
- if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
- *d_os << s;
- }
- }
-
- void operator()(const char* tag, const std::string& s) {
- if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
- *d_os << s;
- }
- }
+ explicit TraceC(std::ostream* os) : d_os(os) {}
- void operator()(const std::string& tag, const char* s) {
- if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
- *d_os << s;
- }
- }
-
- void operator()(const std::string& tag, const std::string& s) {
- if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
- *d_os << s;
- }
- }
-
- 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)));
+ int printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
+ int printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
CVC4ostream operator()(const char* tag) {
if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
@@ -397,23 +258,24 @@ public:
}
}
- void on (const char* tag) { d_tags.insert(std::string(tag)); };
- void on (std::string tag) { d_tags.insert(tag); };
- void off(const char* tag) { d_tags.erase (std::string(tag)); };
- void off(std::string tag) { d_tags.erase (tag); };
+ bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; }
+ bool on (std::string tag) { d_tags.insert(tag); return true; }
+ bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; }
+ bool off(std::string tag) { d_tags.erase (tag); return false; }
bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); }
bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
- void setStream(std::ostream& os) { d_os = &os; }
+ std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
std::ostream& getStream() { return *d_os; }
};/* class TraceC */
/** The debug output singleton */
+extern DebugC DebugChannel CVC4_PUBLIC;
#ifdef CVC4_DEBUG
-extern DebugC Debug CVC4_PUBLIC;
+# define Debug DebugChannel
#else /* CVC4_DEBUG */
-extern NullDebugC Debug CVC4_PUBLIC;
+# define Debug __cvc4_true() ? debugNullCvc4Stream : DebugChannel
#endif /* CVC4_DEBUG */
/** The warning output singleton */
@@ -426,12 +288,26 @@ extern NoticeC Notice CVC4_PUBLIC;
extern ChatC Chat CVC4_PUBLIC;
/** The trace output singleton */
+extern TraceC TraceChannel CVC4_PUBLIC;
#ifdef CVC4_TRACING
-extern TraceC Trace CVC4_PUBLIC;
+# define Trace TraceChannel
#else /* CVC4_TRACING */
-extern NullDebugC Trace CVC4_PUBLIC;
+# define Trace __cvc4_true() ? debugNullCvc4Stream : TraceChannel
#endif /* CVC4_TRACING */
+// Disallow e.g. !Debug("foo").isOn() forms
+// because the ! will apply before the ? .
+// If a compiler error has directed you here,
+// just parenthesize it e.g. !(Debug("foo").isOn())
+class __cvc4_true {
+ void operator!() CVC4_UNUSED;
+ void operator~() CVC4_UNUSED;
+ void operator-() CVC4_UNUSED;
+ void operator+() CVC4_UNUSED;
+public:
+ inline operator bool() { return true; }
+};/* __cvc4_true */
+
#ifdef CVC4_DEBUG
class CVC4_PUBLIC ScopedDebug {
@@ -549,15 +425,65 @@ extern NullDebugC Trace 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) {
-#if defined(CVC4_DEBUG) && !defined(CVC4_MUZZLE)
- return Debug.isOn(tag);
-#else /* CVC4_DEBUG && !CVC4_MUZZLE */
- return false;
-#endif /* CVC4_DEBUG && !CVC4_MUZZLE */
-}/* debugTagIsOn() */
+/**
+ * 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.
+ */
+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) {}
+
+ int printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) {}
+ int 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; }
+
+*/
+ 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; }
+};/* 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