(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())
# 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,
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";
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';
** 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
}
};/* 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
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;
- /**
- * 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.
}
/**
- * 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();
** 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
** 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
/*! \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
}
/* 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;
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]));
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){
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;
** 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
}
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);
/*! \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
d_propEngine = propEngine;
}
+ /**
+ * 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).
*/
-/*
- * 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}
** 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
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 */
** 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
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 */
** 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
#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 */
** \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
/** 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 {
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() {
}
};/* 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;
}
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()) {
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 */
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 */
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 */
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 */
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 */
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()) {
}
}
- 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 */
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 {
#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 */
test9.cvc \
test11.cvc \
uf20-03.cvc \
+ uf20-03.tim.cvc \
wiki.01.cvc \
wiki.02.cvc \
wiki.03.cvc \
--- /dev/null
+% 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
** \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
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
// 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
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
// 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");
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");
** 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
}
+ 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
#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 */
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 */
# 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("");
projects / cvc5.git / commitdiff