diff options
| -rwxr-xr-x | contrib/update-copyright.pl | 26 | ||||
| -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 | ||||
| -rw-r--r-- | test/regress/regress0/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/uf20-03.tim.cvc | 117 | ||||
| -rw-r--r-- | test/unit/expr/attribute_white.h | 242 | ||||
| -rw-r--r-- | test/unit/util/output_black.h | 43 |
16 files changed, 536 insertions, 465 deletions
diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl index db3ac47da..93ec5e6f0 100755 --- a/contrib/update-copyright.pl +++ b/contrib/update-copyright.pl @@ -4,16 +4,19 @@ # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 # Copyright (c) 2009, 2010, 2011 The CVC4 Project # -# usage: update-copyright [ files/directories... ] +# usage: update-copyright [-m] [files/directories...] # # This script goes through a source directory rewriting the top bits of # source files to match a template (inline, below). For files with no # top comment, it adds a fresh one. # -# usage: contrib/update-copyright.pl [dirs...] -# if dirs... are unspecified, the script scans its own parent directory's -# "src" directory. Since it lives in contrib/ in the CVC4 source tree, -# that means src/ in the CVC4 source tree. +# if no files/directories are unspecified, the script scans its own +# parent directory's "src" directory. Since it lives in contrib/ in +# the CVC4 source tree, that means src/ in the CVC4 source tree. +# +# If -m is specified as the first argument, all files and directories +# are scanned, but only ones modifed in the current working directory +# are modified (i.e., those that have status M in "svn status"). # # It ignores any file/directory not starting with [a-zA-Z] # (so, this includes . and .., vi swaps, .svn meta-info, @@ -62,6 +65,14 @@ use Fcntl ':mode'; my $dir = $0; $dir =~ s,/[^/]+/*$,,; +# whether we ONLY process files with svn status "M" +my $modonly = 0; + +if($#ARGV >= 0 && $ARGV[0] eq '-m') { + $modonly = 1; + shift; +} + my @searchdirs = (); if($#ARGV == -1) { (chdir($dir."/..") && -f "src/include/cvc4_public.h") || die "can't find top-level source directory for CVC4"; @@ -112,8 +123,9 @@ while($#searchdirs >= 0) { sub handleFile { my ($srcdir, $file) = @_; - next if !($file =~ /\.(c|cc|cpp|C|h|hh|hpp|H|y|yy|ypp|Y|l|ll|lpp|L|g)$/); - next if ($srcdir.'/'.$file) =~ /$excluded_paths/; + return if !($file =~ /\.(c|cc|cpp|C|h|hh|hpp|H|y|yy|ypp|Y|l|ll|lpp|L|g)$/); + return if ($srcdir.'/'.$file) =~ /$excluded_paths/; + return if $modonly &&`svn status "$srcdir/$file" 2>/dev/null` !~ /^M/; print "$srcdir/$file..."; my $infile = $srcdir.'/'.$file; my $outfile = $srcdir.'/#'.$file.'.tmp'; 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 */ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index c732ffbb2..83291eb5a 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -52,6 +52,7 @@ CVC_TESTS = \ test9.cvc \ test11.cvc \ uf20-03.cvc \ + uf20-03.tim.cvc \ wiki.01.cvc \ wiki.02.cvc \ wiki.03.cvc \ diff --git a/test/regress/regress0/uf20-03.tim.cvc b/test/regress/regress0/uf20-03.tim.cvc new file mode 100644 index 000000000..f13bdcce5 --- /dev/null +++ b/test/regress/regress0/uf20-03.tim.cvc @@ -0,0 +1,117 @@ +% COMMAND-LINE: --uf=tim +% EXPECT: invalid +x_1 : BOOLEAN; +x_2 : BOOLEAN; +x_3 : BOOLEAN; +x_4 : BOOLEAN; +x_5 : BOOLEAN; +x_6 : BOOLEAN; +x_7 : BOOLEAN; +x_8 : BOOLEAN; +x_9 : BOOLEAN; +x_10 : BOOLEAN; +x_11 : BOOLEAN; +x_12 : BOOLEAN; +x_13 : BOOLEAN; +x_14 : BOOLEAN; +x_15 : BOOLEAN; +x_16 : BOOLEAN; +x_17 : BOOLEAN; +x_18 : BOOLEAN; +x_19 : BOOLEAN; +x_20 : BOOLEAN; +ASSERT NOT x_9 OR x_3 OR NOT x_15; +ASSERT NOT x_12 OR NOT x_4 OR NOT x_15; +ASSERT x_6 OR x_14 OR NOT x_17; +ASSERT x_10 OR x_16 OR x_11; +ASSERT NOT x_15 OR x_20 OR NOT x_7; +ASSERT NOT x_1 OR x_10 OR x_16; +ASSERT x_13 OR x_17 OR NOT x_7; +ASSERT NOT x_2 OR NOT x_14 OR NOT x_13; +ASSERT x_13 OR NOT x_6 OR x_15; +ASSERT NOT x_9 OR x_3 OR x_16; +ASSERT NOT x_20 OR NOT x_13 OR x_4; +ASSERT NOT x_7 OR x_15 OR NOT x_14; +ASSERT NOT x_15 OR NOT x_16 OR x_6; +ASSERT x_5 OR NOT x_18 OR x_20; +ASSERT NOT x_16 OR NOT x_19 OR x_7; +ASSERT x_20 OR NOT x_18 OR NOT x_2; +ASSERT x_10 OR NOT x_19 OR NOT x_14; +ASSERT x_16 OR NOT x_7 OR x_12; +ASSERT x_6 OR NOT x_5 OR NOT x_1; +ASSERT NOT x_9 OR x_11 OR x_15; +ASSERT x_19 OR NOT x_6 OR x_7; +ASSERT NOT x_11 OR x_17 OR NOT x_19; +ASSERT x_9 OR NOT x_16 OR x_6; +ASSERT x_15 OR NOT x_20 OR x_10; +ASSERT x_9 OR NOT x_1 OR NOT x_11; +ASSERT NOT x_8 OR NOT x_19 OR x_5; +ASSERT NOT x_19 OR x_11 OR x_20; +ASSERT NOT x_12 OR x_13 OR NOT x_3; +ASSERT NOT x_7 OR NOT x_17 OR NOT x_19; +ASSERT x_17 OR x_6 OR NOT x_11; +ASSERT NOT x_7 OR NOT x_17 OR x_10; +ASSERT NOT x_14 OR x_9 OR x_20; +ASSERT x_1 OR NOT x_18 OR NOT x_16; +ASSERT NOT x_2 OR NOT x_15 OR x_20; +ASSERT x_14 OR x_18 OR NOT x_1; +ASSERT NOT x_8 OR NOT x_4 OR x_1; +ASSERT x_13 OR x_3 OR NOT x_9; +ASSERT x_5 OR x_7 OR x_8; +ASSERT x_9 OR x_4 OR NOT x_20; +ASSERT NOT x_18 OR NOT x_15 OR NOT x_10; +ASSERT x_10 OR x_3 OR NOT x_20; +ASSERT x_20 OR NOT x_14 OR x_16; +ASSERT x_20 OR NOT x_3 OR NOT x_11; +ASSERT NOT x_12 OR x_19 OR NOT x_16; +ASSERT NOT x_3 OR x_5 OR x_10; +ASSERT x_8 OR x_13 OR NOT x_7; +ASSERT NOT x_2 OR NOT x_15 OR x_10; +ASSERT NOT x_3 OR x_9 OR x_16; +ASSERT NOT x_12 OR NOT x_16 OR NOT x_18; +ASSERT x_3 OR x_1 OR NOT x_12; +ASSERT NOT x_18 OR x_13 OR x_5; +ASSERT x_1 OR x_3 OR NOT x_19; +ASSERT NOT x_19 OR NOT x_5 OR x_6; +ASSERT NOT x_20 OR x_8 OR NOT x_2; +ASSERT x_17 OR NOT x_8 OR NOT x_13; +ASSERT x_7 OR NOT x_11 OR NOT x_12; +ASSERT NOT x_10 OR NOT x_14 OR NOT x_20; +ASSERT NOT x_1 OR x_16 OR NOT x_12; +ASSERT x_5 OR NOT x_3 OR x_9; +ASSERT NOT x_18 OR x_8 OR x_14; +ASSERT x_1 OR x_16 OR x_12; +ASSERT x_20 OR NOT x_1 OR NOT x_16; +ASSERT x_5 OR x_10 OR NOT x_13; +ASSERT x_9 OR NOT x_10 OR x_6; +ASSERT NOT x_12 OR x_10 OR NOT x_14; +ASSERT NOT x_13 OR x_1 OR x_4; +ASSERT NOT x_20 OR NOT x_7 OR x_3; +ASSERT x_12 OR x_1 OR NOT x_10; +ASSERT NOT x_1 OR NOT x_16 OR x_7; +ASSERT x_11 OR NOT x_6 OR NOT x_4; +ASSERT x_1 OR x_16 OR NOT x_20; +ASSERT x_9 OR x_7 OR x_15; +ASSERT NOT x_6 OR x_17 OR x_10; +ASSERT x_8 OR x_9 OR x_17; +ASSERT x_18 OR x_11 OR x_10; +ASSERT x_7 OR x_1 OR NOT x_8; +ASSERT NOT x_5 OR NOT x_12 OR x_18; +ASSERT NOT x_6 OR x_2 OR x_15; +ASSERT x_2 OR x_18 OR x_1; +ASSERT NOT x_7 OR NOT x_13 OR x_16; +ASSERT x_18 OR x_19 OR x_9; +ASSERT x_9 OR NOT x_14 OR x_18; +ASSERT x_14 OR x_12 OR NOT x_5; +ASSERT NOT x_13 OR NOT x_7 OR NOT x_14; +ASSERT NOT x_1 OR x_8 OR NOT x_16; +ASSERT NOT x_11 OR x_4 OR x_7; +ASSERT NOT x_4 OR x_20 OR x_5; +ASSERT NOT x_5 OR x_2 OR x_12; +ASSERT NOT x_5 OR x_13 OR NOT x_18; +ASSERT NOT x_18 OR x_9 OR x_1; +ASSERT x_10 OR NOT x_11 OR x_16; + + +QUERY FALSE; +% EXIT: 10 diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index 3dbee87eb..448933622 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): barrett, dejan, cconway + ** Minor contributors (to current version): cconway, 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 @@ -160,21 +160,21 @@ public: Node b = d_nm->mkVar(*d_booleanType); Node c = d_nm->mkVar(*d_booleanType); - Debug("cdboolattr", "get flag 1 on a (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("cdboolattr", "get flag 1 on b (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on b (should be F)\n"; TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("cdboolattr", "get flag 1 on c (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); d_ctxt->push(); // level 1 // test that all boolean flags are FALSE to start - Debug("cdboolattr", "get flag 1 on a (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("cdboolattr", "get flag 1 on b (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on b (should be F)\n"; TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("cdboolattr", "get flag 1 on c (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); // test that they all HAVE the boolean attributes @@ -184,96 +184,96 @@ public: // test two-arg version of hasAttribute() bool bb = false; - Debug("cdboolattr", "get flag 1 on a (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; TS_ASSERT(a.getAttribute(TestFlag1cd(), bb)); TS_ASSERT(! bb); - Debug("cdboolattr", "get flag 1 on b (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on b (should be F)\n"; TS_ASSERT(b.getAttribute(TestFlag1cd(), bb)); TS_ASSERT(! bb); - Debug("cdboolattr", "get flag 1 on c (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(c.getAttribute(TestFlag1cd(), bb)); TS_ASSERT(! bb); // setting boolean flags - Debug("cdboolattr", "set flag 1 on a to T\n"); + Debug("cdboolattr") << "set flag 1 on a to T\n"; a.setAttribute(TestFlag1cd(), true); - Debug("cdboolattr", "set flag 1 on b to F\n"); + Debug("cdboolattr") << "set flag 1 on b to F\n"; b.setAttribute(TestFlag1cd(), false); - Debug("cdboolattr", "set flag 1 on c to F\n"); + Debug("cdboolattr") << "set flag 1 on c to F\n"; c.setAttribute(TestFlag1cd(), false); - Debug("cdbootattr", "get flag 1 on a (should be T)\n"); + Debug("cdboolattr") << "get flag 1 on a (should be T)\n"; TS_ASSERT(a.getAttribute(TestFlag1cd())); - Debug("cdbootattr", "get flag 1 on b (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on b (should be F)\n"; TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("cdbootattr", "get flag 1 on c (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); d_ctxt->push(); // level 2 - Debug("cdbootattr", "get flag 1 on a (should be T)\n"); + Debug("cdboolattr") << "get flag 1 on a (should be T)\n"; TS_ASSERT(a.getAttribute(TestFlag1cd())); - Debug("cdbootattr", "get flag 1 on b (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on b (should be F)\n"; TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("cdbootattr", "get flag 1 on c (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); - Debug("cdbootattr", "set flag 1 on a to F\n"); + Debug("cdboolattr") << "set flag 1 on a to F\n"; a.setAttribute(TestFlag1cd(), false); - Debug("cdbootattr", "set flag 1 on b to T\n"); + Debug("cdboolattr") << "set flag 1 on b to T\n"; b.setAttribute(TestFlag1cd(), true); - Debug("cdbootattr", "get flag 1 on a (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("cdbootattr", "get flag 1 on b (should be T)\n"); + Debug("cdboolattr") << "get flag 1 on b (should be T)\n"; TS_ASSERT(b.getAttribute(TestFlag1cd())); - Debug("cdbootattr", "get flag 1 on c (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); d_ctxt->push(); // level 3 - Debug("cdbootattr", "get flag 1 on a (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("cdbootattr", "get flag 1 on b (should be T)\n"); + Debug("cdboolattr") << "get flag 1 on b (should be T)\n"; TS_ASSERT(b.getAttribute(TestFlag1cd())); - Debug("cdbootattr", "get flag 1 on c (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); - Debug("cdbootattr", "set flag 1 on c to T\n"); + Debug("cdboolattr") << "set flag 1 on c to T\n"; c.setAttribute(TestFlag1cd(), true); - Debug("cdbootattr", "get flag 1 on a (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("cdbootattr", "get flag 1 on b (should be T)\n"); + Debug("cdboolattr") << "get flag 1 on b (should be T)\n"; TS_ASSERT(b.getAttribute(TestFlag1cd())); - Debug("cdbootattr", "get flag 1 on c (should be T)\n"); + Debug("cdboolattr") << "get flag 1 on c (should be T)\n"; TS_ASSERT(c.getAttribute(TestFlag1cd())); d_ctxt->pop(); // level 2 - Debug("cdbootattr", "get flag 1 on a (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("cdbootattr", "get flag 1 on b (should be T)\n"); + Debug("cdboolattr") << "get flag 1 on b (should be T)\n"; TS_ASSERT(b.getAttribute(TestFlag1cd())); - Debug("cdbootattr", "get flag 1 on c (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); d_ctxt->pop(); // level 1 - Debug("cdbootattr", "get flag 1 on a (should be T)\n"); + Debug("cdboolattr") << "get flag 1 on a (should be T)\n"; TS_ASSERT(a.getAttribute(TestFlag1cd())); - Debug("cdbootattr", "get flag 1 on b (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on b (should be F)\n"; TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("cdbootattr", "get flag 1 on c (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); d_ctxt->pop(); // level 0 - Debug("cdbootattr", "get flag 1 on a (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("cdbootattr", "get flag 1 on b (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on b (should be F)\n"; TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("cdbootattr", "get flag 1 on c (should be F)\n"); + Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); #ifdef CVC4_ASSERTIONS @@ -294,49 +294,49 @@ public: c.setAttribute(VarNameAttr(), "c"); // test that all boolean flags are FALSE to start - Debug("boolattr", "get flag 1 on a (should be F)\n"); + Debug("boolattr") << "get flag 1 on a (should be F)\n"; TS_ASSERT(! a.getAttribute(TestFlag1())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); + Debug("boolattr") << "get flag 1 on b (should be F)\n"; TS_ASSERT(! b.getAttribute(TestFlag1())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); + Debug("boolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1())); - Debug("boolattr", "get flag 1 on unnamed (should be F)\n"); + Debug("boolattr") << "get flag 1 on unnamed (should be F)\n"; TS_ASSERT(! unnamed.getAttribute(TestFlag1())); - Debug("boolattr", "get flag 2 on a (should be F)\n"); + Debug("boolattr") << "get flag 2 on a (should be F)\n"; TS_ASSERT(! a.getAttribute(TestFlag2())); - Debug("boolattr", "get flag 2 on b (should be F)\n"); + Debug("boolattr") << "get flag 2 on b (should be F)\n"; TS_ASSERT(! b.getAttribute(TestFlag2())); - Debug("boolattr", "get flag 2 on c (should be F)\n"); + Debug("boolattr") << "get flag 2 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag2())); - Debug("boolattr", "get flag 2 on unnamed (should be F)\n"); + Debug("boolattr") << "get flag 2 on unnamed (should be F)\n"; TS_ASSERT(! unnamed.getAttribute(TestFlag2())); - Debug("boolattr", "get flag 3 on a (should be F)\n"); + Debug("boolattr") << "get flag 3 on a (should be F)\n"; TS_ASSERT(! a.getAttribute(TestFlag3())); - Debug("boolattr", "get flag 3 on b (should be F)\n"); + Debug("boolattr") << "get flag 3 on b (should be F)\n"; TS_ASSERT(! b.getAttribute(TestFlag3())); - Debug("boolattr", "get flag 3 on c (should be F)\n"); + Debug("boolattr") << "get flag 3 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag3())); - Debug("boolattr", "get flag 3 on unnamed (should be F)\n"); + Debug("boolattr") << "get flag 3 on unnamed (should be F)\n"; TS_ASSERT(! unnamed.getAttribute(TestFlag3())); - Debug("boolattr", "get flag 4 on a (should be F)\n"); + Debug("boolattr") << "get flag 4 on a (should be F)\n"; TS_ASSERT(! a.getAttribute(TestFlag4())); - Debug("boolattr", "get flag 4 on b (should be F)\n"); + Debug("boolattr") << "get flag 4 on b (should be F)\n"; TS_ASSERT(! b.getAttribute(TestFlag4())); - Debug("boolattr", "get flag 4 on c (should be F)\n"); + Debug("boolattr") << "get flag 4 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag4())); - Debug("boolattr", "get flag 4 on unnamed (should be F)\n"); + Debug("boolattr") << "get flag 4 on unnamed (should be F)\n"; TS_ASSERT(! unnamed.getAttribute(TestFlag4())); - Debug("boolattr", "get flag 5 on a (should be F)\n"); + Debug("boolattr") << "get flag 5 on a (should be F)\n"; TS_ASSERT(! a.getAttribute(TestFlag5())); - Debug("boolattr", "get flag 5 on b (should be F)\n"); + Debug("boolattr") << "get flag 5 on b (should be F)\n"; TS_ASSERT(! b.getAttribute(TestFlag5())); - Debug("boolattr", "get flag 5 on c (should be F)\n"); + Debug("boolattr") << "get flag 5 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag5())); - Debug("boolattr", "get flag 5 on unnamed (should be F)\n"); + Debug("boolattr") << "get flag 5 on unnamed (should be F)\n"; TS_ASSERT(! unnamed.getAttribute(TestFlag5())); // test that they all HAVE the boolean attributes @@ -367,115 +367,115 @@ public: // test two-arg version of hasAttribute() bool bb; - Debug("boolattr", "get flag 1 on a (should be F)\n"); + Debug("boolattr") << "get flag 1 on a (should be F)\n"; TS_ASSERT(a.getAttribute(TestFlag1(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 1 on b (should be F)\n"); + Debug("boolattr") << "get flag 1 on b (should be F)\n"; TS_ASSERT(b.getAttribute(TestFlag1(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 1 on c (should be F)\n"); + Debug("boolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(c.getAttribute(TestFlag1(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 1 on unnamed (should be F)\n"); + Debug("boolattr") << "get flag 1 on unnamed (should be F)\n"; TS_ASSERT(unnamed.getAttribute(TestFlag1(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 2 on a (should be F)\n"); + Debug("boolattr") << "get flag 2 on a (should be F)\n"; TS_ASSERT(a.getAttribute(TestFlag2(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 2 on b (should be F)\n"); + Debug("boolattr") << "get flag 2 on b (should be F)\n"; TS_ASSERT(b.getAttribute(TestFlag2(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 2 on c (should be F)\n"); + Debug("boolattr") << "get flag 2 on c (should be F)\n"; TS_ASSERT(c.getAttribute(TestFlag2(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 2 on unnamed (should be F)\n"); + Debug("boolattr") << "get flag 2 on unnamed (should be F)\n"; TS_ASSERT(unnamed.getAttribute(TestFlag2(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 3 on a (should be F)\n"); + Debug("boolattr") << "get flag 3 on a (should be F)\n"; TS_ASSERT(a.getAttribute(TestFlag3(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 3 on b (should be F)\n"); + Debug("boolattr") << "get flag 3 on b (should be F)\n"; TS_ASSERT(b.getAttribute(TestFlag3(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 3 on c (should be F)\n"); + Debug("boolattr") << "get flag 3 on c (should be F)\n"; TS_ASSERT(c.getAttribute(TestFlag3(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 3 on unnamed (should be F)\n"); + Debug("boolattr") << "get flag 3 on unnamed (should be F)\n"; TS_ASSERT(unnamed.getAttribute(TestFlag3(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 4 on a (should be F)\n"); + Debug("boolattr") << "get flag 4 on a (should be F)\n"; TS_ASSERT(a.getAttribute(TestFlag4(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 4 on b (should be F)\n"); + Debug("boolattr") << "get flag 4 on b (should be F)\n"; TS_ASSERT(b.getAttribute(TestFlag4(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 4 on c (should be F)\n"); + Debug("boolattr") << "get flag 4 on c (should be F)\n"; TS_ASSERT(c.getAttribute(TestFlag4(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 4 on unnamed (should be F)\n"); + Debug("boolattr") << "get flag 4 on unnamed (should be F)\n"; TS_ASSERT(unnamed.getAttribute(TestFlag4(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 5 on a (should be F)\n"); + Debug("boolattr") << "get flag 5 on a (should be F)\n"; TS_ASSERT(a.getAttribute(TestFlag5(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 5 on b (should be F)\n"); + Debug("boolattr") << "get flag 5 on b (should be F)\n"; TS_ASSERT(b.getAttribute(TestFlag5(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 5 on c (should be F)\n"); + Debug("boolattr") << "get flag 5 on c (should be F)\n"; TS_ASSERT(c.getAttribute(TestFlag5(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 5 on unnamed (should be F)\n"); + Debug("boolattr") << "get flag 5 on unnamed (should be F)\n"; TS_ASSERT(unnamed.getAttribute(TestFlag5(), bb)); TS_ASSERT(! bb); // setting boolean flags - Debug("boolattr", "set flag 1 on a to T\n"); + Debug("boolattr") << "set flag 1 on a to T\n"; a.setAttribute(TestFlag1(), true); - Debug("boolattr", "set flag 1 on b to F\n"); + Debug("boolattr") << "set flag 1 on b to F\n"; b.setAttribute(TestFlag1(), false); - Debug("boolattr", "set flag 1 on c to F\n"); + Debug("boolattr") << "set flag 1 on c to F\n"; c.setAttribute(TestFlag1(), false); - Debug("boolattr", "set flag 1 on unnamed to T\n"); + Debug("boolattr") << "set flag 1 on unnamed to T\n"; unnamed.setAttribute(TestFlag1(), true); - Debug("boolattr", "set flag 2 on a to F\n"); + Debug("boolattr") << "set flag 2 on a to F\n"; a.setAttribute(TestFlag2(), false); - Debug("boolattr", "set flag 2 on b to T\n"); + Debug("boolattr") << "set flag 2 on b to T\n"; b.setAttribute(TestFlag2(), true); - Debug("boolattr", "set flag 2 on c to T\n"); + Debug("boolattr") << "set flag 2 on c to T\n"; c.setAttribute(TestFlag2(), true); - Debug("boolattr", "set flag 2 on unnamed to F\n"); + Debug("boolattr") << "set flag 2 on unnamed to F\n"; unnamed.setAttribute(TestFlag2(), false); - Debug("boolattr", "set flag 3 on a to T\n"); + Debug("boolattr") << "set flag 3 on a to T\n"; a.setAttribute(TestFlag3(), true); - Debug("boolattr", "set flag 3 on b to T\n"); + Debug("boolattr") << "set flag 3 on b to T\n"; b.setAttribute(TestFlag3(), true); - Debug("boolattr", "set flag 3 on c to T\n"); + Debug("boolattr") << "set flag 3 on c to T\n"; c.setAttribute(TestFlag3(), true); - Debug("boolattr", "set flag 3 on unnamed to T\n"); + Debug("boolattr") << "set flag 3 on unnamed to T\n"; unnamed.setAttribute(TestFlag3(), true); - Debug("boolattr", "set flag 4 on a to T\n"); + Debug("boolattr") << "set flag 4 on a to T\n"; a.setAttribute(TestFlag4(), true); - Debug("boolattr", "set flag 4 on b to T\n"); + Debug("boolattr") << "set flag 4 on b to T\n"; b.setAttribute(TestFlag4(), true); - Debug("boolattr", "set flag 4 on c to T\n"); + Debug("boolattr") << "set flag 4 on c to T\n"; c.setAttribute(TestFlag4(), true); - Debug("boolattr", "set flag 4 on unnamed to T\n"); + Debug("boolattr") << "set flag 4 on unnamed to T\n"; unnamed.setAttribute(TestFlag4(), true); - Debug("boolattr", "set flag 5 on a to T\n"); + Debug("boolattr") << "set flag 5 on a to T\n"; a.setAttribute(TestFlag5(), true); - Debug("boolattr", "set flag 5 on b to T\n"); + Debug("boolattr") << "set flag 5 on b to T\n"; b.setAttribute(TestFlag5(), true); - Debug("boolattr", "set flag 5 on c to F\n"); + Debug("boolattr") << "set flag 5 on c to F\n"; c.setAttribute(TestFlag5(), false); - Debug("boolattr", "set flag 5 on unnamed to T\n"); + Debug("boolattr") << "set flag 5 on unnamed to T\n"; unnamed.setAttribute(TestFlag5(), true); TS_ASSERT(a.getAttribute(VarNameAttr()) == "a"); @@ -510,49 +510,49 @@ public: TS_ASSERT(! c.hasAttribute(TestStringAttr2())); TS_ASSERT(! unnamed.hasAttribute(TestStringAttr2())); - Debug("boolattr", "get flag 1 on a (should be T)\n"); + Debug("boolattr") << "get flag 1 on a (should be T)\n"; TS_ASSERT(a.getAttribute(TestFlag1())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); + Debug("boolattr") << "get flag 1 on b (should be F)\n"; TS_ASSERT(! b.getAttribute(TestFlag1())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); + Debug("boolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1())); - Debug("boolattr", "get flag 1 on unnamed (should be T)\n"); + Debug("boolattr") << "get flag 1 on unnamed (should be T)\n"; TS_ASSERT(unnamed.getAttribute(TestFlag1())); - Debug("boolattr", "get flag 2 on a (should be F)\n"); + Debug("boolattr") << "get flag 2 on a (should be F)\n"; TS_ASSERT(! a.getAttribute(TestFlag2())); - Debug("boolattr", "get flag 2 on b (should be T)\n"); + Debug("boolattr") << "get flag 2 on b (should be T)\n"; TS_ASSERT(b.getAttribute(TestFlag2())); - Debug("boolattr", "get flag 2 on c (should be T)\n"); + Debug("boolattr") << "get flag 2 on c (should be T)\n"; TS_ASSERT(c.getAttribute(TestFlag2())); - Debug("boolattr", "get flag 2 on unnamed (should be F)\n"); + Debug("boolattr") << "get flag 2 on unnamed (should be F)\n"; TS_ASSERT(! unnamed.getAttribute(TestFlag2())); - Debug("boolattr", "get flag 3 on a (should be T)\n"); + Debug("boolattr") << "get flag 3 on a (should be T)\n"; TS_ASSERT(a.getAttribute(TestFlag3())); - Debug("boolattr", "get flag 3 on b (should be T)\n"); + Debug("boolattr") << "get flag 3 on b (should be T)\n"; TS_ASSERT(b.getAttribute(TestFlag3())); - Debug("boolattr", "get flag 3 on c (should be T)\n"); + Debug("boolattr") << "get flag 3 on c (should be T)\n"; TS_ASSERT(c.getAttribute(TestFlag3())); - Debug("boolattr", "get flag 3 on unnamed (should be T)\n"); + Debug("boolattr") << "get flag 3 on unnamed (should be T)\n"; TS_ASSERT(unnamed.getAttribute(TestFlag3())); - Debug("boolattr", "get flag 4 on a (should be T)\n"); + Debug("boolattr") << "get flag 4 on a (should be T)\n"; TS_ASSERT(a.getAttribute(TestFlag4())); - Debug("boolattr", "get flag 4 on b (should be T)\n"); + Debug("boolattr") << "get flag 4 on b (should be T)\n"; TS_ASSERT(b.getAttribute(TestFlag4())); - Debug("boolattr", "get flag 4 on c (should be T)\n"); + Debug("boolattr") << "get flag 4 on c (should be T)\n"; TS_ASSERT(c.getAttribute(TestFlag4())); - Debug("boolattr", "get flag 4 on unnamed (should be T)\n"); + Debug("boolattr") << "get flag 4 on unnamed (should be T)\n"; TS_ASSERT(unnamed.getAttribute(TestFlag4())); - Debug("boolattr", "get flag 5 on a (should be T)\n"); + Debug("boolattr") << "get flag 5 on a (should be T)\n"; TS_ASSERT(a.getAttribute(TestFlag5())); - Debug("boolattr", "get flag 5 on b (should be T)\n"); + Debug("boolattr") << "get flag 5 on b (should be T)\n"; TS_ASSERT(b.getAttribute(TestFlag5())); - Debug("boolattr", "get flag 5 on c (should be F)\n"); + Debug("boolattr") << "get flag 5 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag5())); - Debug("boolattr", "get flag 5 on unnamed (should be T)\n"); + Debug("boolattr") << "get flag 5 on unnamed (should be T)\n"; TS_ASSERT(unnamed.getAttribute(TestFlag5())); a.setAttribute(TestStringAttr1(), "foo"); diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h index e6a040f7b..183d8f7f1 100644 --- a/test/unit/util/output_black.h +++ b/test/unit/util/output_black.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 @@ -219,6 +219,31 @@ public: } + static int expensiveFunction() { + // this represents an expensive function that should NOT be called + // when debugging/tracing is turned off + TS_FAIL("a function was evaluated under Debug() or Trace() when it should not have been"); + return 0; + } + + void testEvaluationOffWhenItsSupposedToBe() { + Trace.on("foo"); +#ifndef CVC4_TRACING + TS_ASSERT( !( Trace.isOn("foo") ) ); + Trace("foo") << expensiveFunction() << endl; +#else /* CVC4_TRACING */ + TS_ASSERT( Trace.isOn("foo") ); +#endif /* CVC4_TRACING */ + + Debug.on("foo"); +#ifndef CVC4_DEBUG + TS_ASSERT( !( Debug.isOn("foo") ) ); + Debug("foo") << expensiveFunction() << endl; +#else /* CVC4_DEBUG */ + TS_ASSERT( Debug.isOn("foo") ); +#endif /* CVC4_DEBUG */ + } + void testSimplePrint() { #ifdef CVC4_MUZZLE @@ -260,11 +285,11 @@ public: #else /* CVC4_MUZZLE */ Debug.off("yo"); - Debug("yo", "foobar"); + Debug("yo") << "foobar"; TS_ASSERT_EQUALS(d_debugStream.str(), string()); d_debugStream.str(""); Debug.on("yo"); - Debug("yo", "baz foo"); + Debug("yo") << "baz foo"; # ifdef CVC4_DEBUG TS_ASSERT_EQUALS(d_debugStream.str(), string("baz foo")); # else /* CVC4_DEBUG */ @@ -273,11 +298,11 @@ public: d_debugStream.str(""); Trace.off("yo"); - Trace("yo", "foobar"); + Trace("yo") << "foobar"; TS_ASSERT_EQUALS(d_traceStream.str(), string()); d_traceStream.str(""); Trace.on("yo"); - Trace("yo", "baz foo"); + Trace("yo") << "baz foo"; # ifdef CVC4_TRACING TS_ASSERT_EQUALS(d_traceStream.str(), string("baz foo")); # else /* CVC4_TRACING */ @@ -285,19 +310,19 @@ public: # endif /* CVC4_TRACING */ d_traceStream.str(""); - Warning("baz foo"); + Warning() << "baz foo"; TS_ASSERT_EQUALS(d_warningStream.str(), string("baz foo")); d_warningStream.str(""); - Chat("baz foo"); + Chat() << "baz foo"; TS_ASSERT_EQUALS(d_chatStream.str(), string("baz foo")); d_chatStream.str(""); - Message("baz foo"); + Message() << "baz foo"; TS_ASSERT_EQUALS(d_messageStream.str(), string("baz foo")); d_messageStream.str(""); - Notice("baz foo"); + Notice() << "baz foo"; TS_ASSERT_EQUALS(d_noticeStream.str(), string("baz foo")); d_noticeStream.str(""); |