diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-03-30 03:59:05 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-03-30 03:59:05 +0000 |
commit | 10cabf82a20258da80be53eb6d23b1a536e82eb5 (patch) | |
tree | d8262298ed5fba5a3c51681cc5739551747f7a90 /src | |
parent | d35d086268fa2a3d9b3c387157e4c54f1b967e0e (diff) |
Add Valuation::getSatValue() so that theories can access the current
(propositional) assignment for theory atoms.
Fixed Debug/Trace as discussed in bug ticket #252 and on the mailing list.
This implementation leads to some compiler warnings in production builds,
but these will be corrected in coming days. There appears to be a small
speedup in the parser as a result of this fix:
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=1902&reference_id=1886&p=5
Cleaned up a few CD Boolean attribute things.
Various small fixes to coding guidelines / test coverage.
This commit:
* Resolves bug 252 (tracing not disabled in production builds)
* Resolves bug 254 (implement CDAttrHash<>::BitIterator::find())
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/attribute_internals.h | 73 | ||||
-rw-r--r-- | src/lib/clock_gettime.h | 4 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 8 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 6 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 5 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 11 | ||||
-rw-r--r-- | src/theory/theory_traits_template.h | 25 | ||||
-rw-r--r-- | src/theory/valuation.cpp | 10 | ||||
-rw-r--r-- | src/theory/valuation.h | 12 | ||||
-rw-r--r-- | src/util/output.cpp | 120 | ||||
-rw-r--r-- | src/util/output.h | 298 |
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 */ |