node_manager.h \
expr_manager.h \
attribute.h \
- attribute.cpp \
@srcdir@/kind.h \
node.cpp \
node_builder.cpp \
+++ /dev/null
-/********************* -*- C++ -*- */
-/** attribute.cpp
- ** Original author: mdeters
- ** 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)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.
- **
- ** Node attributes.
- **/
-
-#include "expr/attribute.h"
-
-#include <string>
-
-using std::string;
-
-namespace CVC4 {
-namespace expr {
-namespace attr {
-
-unsigned BitAssignment::s_bit = 0;
-
-}/* CVC4::expr::attr namespace */
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
**
** An attribute structure looks like the following:
**
- ** struct VarName_attr {
+ ** struct VarNameAttr {
**
** // the value type for this attribute
** typedef std::string value_type;
** // an extra hash value (to avoid same-value-type collisions)
** enum { hash_value = 1 };
**
- ** // whether inclusion in the table keeps the (key) Node live or not
- ** static const bool hard_key = false;
- **
** // cleanup routine when the Node goes away
** static inline void cleanup(const std::string&) {
** }
namespace CVC4 {
namespace expr {
+// ATTRIBUTE HASH FUNCTIONS ====================================================
+
struct AttrHashFcn {
enum { LARGE_PRIME = 1 };
std::size_t operator()(const std::pair<unsigned, SoftNode>& p) const {
}
};
-/*
-template <class T>
-class AttrTable;
-
-template <>
-class AttrTable<bool> {
-public:
- class BitAccessor {
-
- uint64_t& d_word;
-
- unsigned d_bit;
-
- public:
-
- BitAccessor(uint64_t& word, unsigned bit) :
- d_word(word),
- d_bit(bit) {
- }
-
- BitAccessor& operator=(bool b) {
- if(b) {
- // set the bit
- d_word |= (1 << d_bit);
- } else {
- // clear the bit
- d_word &= ~(1 << d_bit);
- }
-
- return *this;
- }
- };
-
- // bool specialization
- //static AttrHash<uint64_t>* s_hash;
-
- //typedef AttrHash<SoftNode, uint64_t>::iterator iterator;
- //typedef AttrHash<SoftNode, uint64_t>::const_iterator const_iterator;
-
- template <class Attr>
- BitAccessor& find(Node e, const Attr&);
-
- template <class Attr>
- bool find(Node e, const Attr&) const;
-};
-
-template <>
-class AttrTable<uint64_t> {
-public:
- // int(egral) specialization
- //static AttrHash<uint64_t>* s_hash;
- typedef AttrHash<uint64_t>::iterator iterator;
- typedef AttrHash<uint64_t>::const_iterator const_iterator;
- uint64_t& find(TNode);
-};
-
-template <class T>
-class AttrTable<T*> {
-public:
- // pointer specialization
- //static AttrHash<void*>* s_hash;
- typedef AttrHash<void*>::iterator iterator;
- typedef AttrHash<void*>::const_iterator const_iterator;
-};
-
-template <>
-class AttrTable<Node> {
-public:
- // Node specialization
- //static AttrHash<SoftNode>* s_hash;
- typedef AttrHash<SoftNode>::iterator iterator;
- typedef AttrHash<SoftNode>::const_iterator const_iterator;
- Node find(TNode);
-};
-
-template <>
-class AttrTable<std::string> {
-public:
- // string specialization
- //static AttrHash<std::string>* s_hash;
- typedef AttrHash<std::string>::iterator iterator;
- typedef AttrHash<std::string>::const_iterator const_iterator;
- Node find(TNode);
-};
-
-*/
-
-/*
-template <class T>
-AttrHash<void*>* AttrTable<T*>::s_hash = &g_hash_ptr;
-*/
+// ATTRIBUTE TYPE MAPPINGS =====================================================
template <class T>
struct KindValueToTableValueMapping {
typedef typename AttrKind::value_type table_identifier;
};
+// ATTRIBUTE HASH TABLES =======================================================
+
// use a TAG to indicate which table it should be in
template <class value_type>
struct AttrHash : public __gnu_cxx::hash_map<std::pair<unsigned, SoftNode>, value_type, AttrHashFcn> {};
-/*
template <>
class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHashBoolFcn> {
return *this;
}
+
+ operator bool() const {
+ return (d_word & (1 << d_bit)) ? true : false;
+ }
};
class BitIterator {
- std::pair<SoftNode, uint64_t>& d_word;
+ std::pair<const SoftNode, uint64_t>* d_entry;
- int d_bit;
+ unsigned d_bit;
public:
BitIterator() :
- d_word((uint64_t&) d_bit),
- d_bit(-1) {
+ d_entry(NULL),
+ d_bit(0) {
}
- BitIterator(std::pair<SoftNode, uint64_t>& entry, unsigned bit) :
- d_entry(entry),
+ BitIterator(std::pair<const SoftNode, uint64_t>& entry, unsigned bit) :
+ d_entry(&entry),
d_bit(bit) {
}
- BitAccessor operator*() {
- return BitAccessor(d_word, d_bit);
+ std::pair<const SoftNode, BitAccessor> operator*() {
+ return std::make_pair(d_entry->first, BitAccessor(d_entry->second, d_bit));
+ }
+
+ bool operator==(const BitIterator& b) {
+ return d_entry == b.d_entry && d_bit == b.d_bit;
}
};
class ConstBitIterator {
- uint64_t& d_word;
+ const std::pair<const SoftNode, uint64_t>* d_entry;
unsigned d_bit;
public:
- ConstBitIterator(uint64_t& word, unsigned bit) :
- d_word(word),
+ ConstBitIterator() :
+ d_entry(NULL),
+ d_bit(0) {
+ }
+
+ ConstBitIterator(const std::pair<const SoftNode, uint64_t>& entry, unsigned bit) :
+ d_entry(&entry),
d_bit(bit) {
}
- bool operator*() {
- return (d_word & (1 << d_bit)) ? true : false;
+ std::pair<const SoftNode, bool> operator*() {
+ return std::make_pair(d_entry->first, (d_entry->second & (1 << d_bit)) ? true : false);
+ }
+
+ bool operator==(const ConstBitIterator& b) {
+ return d_entry == b.d_entry && d_bit == b.d_bit;
}
};
if(i == super::end()) {
return BitIterator();
}
+ Debug.printf("boolattr", "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", &(*i).second, (*i).second, k.first);
return BitIterator(*i, k.first);
}
+ BitIterator end() {
+ return BitIterator();
+ }
+
ConstBitIterator find(const std::pair<unsigned, SoftNode>& k) const {
super::const_iterator i = super::find(k.second);
+ if(i == super::end()) {
+ return ConstBitIterator();
+ }
+ Debug.printf("boolattr", "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", &(*i).second, (*i).second, k.first);
return ConstBitIterator(*i, k.first);
}
+ ConstBitIterator end() const {
+ return ConstBitIterator();
+ }
+
BitAccessor operator[](const std::pair<unsigned, SoftNode>& k) {
uint64_t& word = super::operator[](k.second);
return BitAccessor(word, k.first);
}
-};
-*/
+};/* class AttrHash<bool> */
+
+// ATTRIBUTE PATTERN ===========================================================
/**
* An "attribute type" structure.
static inline unsigned getId() { return s_id; }
static inline unsigned getHashValue() { return s_hashValue; }
+ static const bool has_default_value = false;
+
private:
/** an id */
- static unsigned s_id;
+ static const unsigned s_id;
/** an extra hash value (to avoid same-value-type collisions) */
- static unsigned s_hashValue;
+ static const unsigned s_hashValue;
};
/**
static inline void cleanup(const bool&) {}
static inline unsigned getId() { return s_id; }
- static inline unsigned getBit() { return s_bit; }
static inline unsigned getHashValue() { return s_hashValue; }
-private:
+ static const bool has_default_value = true;
+ static const bool default_value = false;
- /** an id */
- static unsigned s_id;
+ static inline unsigned checkID(unsigned id) {
+ AlwaysAssert(id <= 63,
+ "Too many boolean node attributes registered during initialization !");
+ return id;
+ }
+
+private:
/** a bit assignment */
- static unsigned s_bit;
+ static const unsigned s_id;
/** an extra hash value (to avoid same-value-type collisions) */
- static unsigned s_hashValue;
+ static const unsigned s_hashValue;
};
+// SPECIFIC, GLOBAL ATTRIBUTE DEFINITIONS ======================================
+
namespace attr {
struct VarName {};
struct Type {};
template <class T>
unsigned LastAttributeId<T>::s_id = 0;
-
- struct BitAssignment {
- static unsigned s_bit;
- };
}/* CVC4::expr::attr namespace */
typedef Attribute<attr::VarName, std::string> VarNameAttr;
typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr;
-/*
-template <class Attr>
-class AttributeTable {
- typedef typename Attr::value_type value_type;
-
- AttrTable<value_type>& d_table;
-
-};
-*/
-
-/*
-template <class T>
-struct AttrTables {
-
-};
-*/
+// ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
template <class T, class value_t>
-unsigned Attribute<T, value_t>::s_id =
+const unsigned Attribute<T, value_t>::s_id =
attr::LastAttributeId<typename KindValueToTableValueMapping<value_t>::table_value_type>::s_id++;
template <class T, class value_t>
-unsigned Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id;
+const unsigned Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id;
template <class T>
-unsigned Attribute<T, bool>::s_id =
- attr::LastAttributeId<bool>::s_id++;
-template <class T>
-unsigned Attribute<T, bool>::s_bit =
- attr::BitAssignment::s_bit++;
+const unsigned Attribute<T, bool>::s_id =
+ Attribute<T, bool>::checkID(attr::LastAttributeId<bool>::s_id++);
template <class T>
-unsigned Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id;
+const unsigned Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id;
class AttributeManager;
//inline AttrHash<KindTableValueMapping<T> >& get(AttributeManager& am);
};
+// ATTRIBUTE MANAGER ===========================================================
+
class AttributeManager {
NodeManager* d_nm;
- AttrHash<uint64_t> d_bools;
+ AttrHash<bool> d_bools;
AttrHash<uint64_t> d_ints;
AttrHash<SoftNode> d_exprs;
AttrHash<std::string> d_strings;
typename AttrKind::value_type getAttribute(const Node& n,
const AttrKind&);
+ template <class AttrKind>
+ bool hasAttribute(const Node& n,
+ const AttrKind&);
+
template <class AttrKind>
bool hasAttribute(const Node& n,
const AttrKind&,
- typename AttrKind::value_type* = NULL);
+ typename AttrKind::value_type*);
template <class AttrKind>
void setAttribute(const Node& n,
const typename AttrKind::value_type& value);
};
+// MAPPING OF ATTRIBUTE KINDS TO TABLES IN THE ATTRIBUTE MANAGER ===============
+
template <>
struct getTable<bool> {
- typedef AttrHash<uint64_t> table_type;
+ typedef AttrHash<bool> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_bools;
}
}
};
+// ATTRIBUTE MANAGER IMPLEMENTATIONS ===========================================
+
template <class AttrKind>
typename AttrKind::value_type AttributeManager::getAttribute(const Node& n,
- const AttrKind& marker) {
+ const AttrKind&) {
typedef typename AttrKind::value_type value_type;
typedef KindValueToTableValueMapping<value_type> mapping;
return typename AttrKind::value_type();
}
- return mapping::convertBack(i->second);
+ return mapping::convertBack((*i).second);
}
+/* helper template class for hasAttribute(), specialized based on
+ * whether AttrKind has a "default value" that all Nodes implicitly
+ * have or not. */
+template <bool has_default, class AttrKind>
+struct HasAttribute;
+
template <class AttrKind>
-bool AttributeManager::hasAttribute(const Node& n,
- const AttrKind&,
- typename AttrKind::value_type* ret) {
+struct HasAttribute<true, AttrKind> {
+ static inline bool hasAttribute(AttributeManager* am,
+ const Node& n) {
+ return true;
+ }
- typedef typename AttrKind::value_type value_type;
- typedef KindValueToTableValueMapping<value_type> mapping;
- typedef typename getTable<value_type>::table_type table_type;
+ static inline bool hasAttribute(AttributeManager* am,
+ const Node& n,
+ typename AttrKind::value_type* ret) {
+ if(ret != NULL) {
+ typedef typename AttrKind::value_type value_type;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ typedef typename getTable<value_type>::table_type table_type;
- table_type& ah = getTable<value_type>::get(*this);
- typename table_type::iterator i = ah.find(std::make_pair(AttrKind::getId(), n));
+ table_type& ah = getTable<value_type>::get(*am);
+ typename table_type::iterator i = ah.find(std::make_pair(AttrKind::getId(), n));
- if(i == ah.end()) {
- return false;
+ if(i == ah.end()) {
+ *ret = AttrKind::default_value;
+ } else {
+ *ret = mapping::convertBack((*i).second);
+ }
+ }
+
+ return true;
}
+};
+
+template <class AttrKind>
+struct HasAttribute<false, AttrKind> {
+ static inline bool hasAttribute(AttributeManager* am,
+ const Node& n) {
+ typedef typename AttrKind::value_type value_type;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ typedef typename getTable<value_type>::table_type table_type;
+
+ table_type& ah = getTable<value_type>::get(*am);
+ typename table_type::iterator i = ah.find(std::make_pair(AttrKind::getId(), n));
+
+ if(i == ah.end()) {
+ return false;
+ }
- if(ret != NULL) {
- *ret = mapping::convertBack(i->second);
+ return true;
}
- return true;
+ static inline bool hasAttribute(AttributeManager* am,
+ const Node& n,
+ typename AttrKind::value_type* ret) {
+ typedef typename AttrKind::value_type value_type;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ typedef typename getTable<value_type>::table_type table_type;
+
+ table_type& ah = getTable<value_type>::get(*am);
+ typename table_type::iterator i = ah.find(std::make_pair(AttrKind::getId(), n));
+
+ if(i == ah.end()) {
+ return false;
+ }
+
+ if(ret != NULL) {
+ *ret = mapping::convertBack((*i).second);
+ }
+
+ return true;
+ }
+};
+
+template <class AttrKind>
+bool AttributeManager::hasAttribute(const Node& n,
+ const AttrKind&) {
+ return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, n);
+}
+
+template <class AttrKind>
+bool AttributeManager::hasAttribute(const Node& n,
+ const AttrKind&,
+ typename AttrKind::value_type* ret) {
+ return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, n, ret);
}
template <class AttrKind>
ah[std::make_pair(AttrKind::getId(), n)] = mapping::convert(value);
}
-/*
-
-template <class attr>
-struct last_attribute_id {
- static unsigned value;
-};
-
-template <class attr>
-unsigned last_attribute_id<attr>::value = 0;
-
-template <class attr>
-unsigned register_attribute_kind() {
- return last_attribute_id<attr>::value++;
-}
-
-*/
-
}/* CVC4::expr namespace */
}/* CVC4 namespace */
#include <iostream>
#include "util/output.h"
+using namespace std;
+
namespace CVC4 {
/* Definitions of the declared globals from output.h... */
null_streambuf null_sb;
-std::ostream null_os(&null_sb);
-
-DebugC DebugOut (&std::cout);
-WarningC Warning(&std::cerr);
-MessageC Message(&std::cout);
-NoticeC Notice (&std::cout);
-ChatC Chat (&std::cout);
-TraceC Trace (&std::cout);
+ostream null_os(&null_sb);
+
+DebugC DebugOut(&cout);
+WarningC Warning (&cerr);
+MessageC Message (&cout);
+NoticeC Notice (&cout);
+ChatC Chat (&cout);
+TraceC Trace (&cout);
+
+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;
+ }
+}
+
+void DebugC::printf(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;
+ }
+}
+
+void 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);
+ va_end(vl);
+ *d_os << buf;
+}
+
+void 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);
+ va_end(vl);
+ *d_os << buf;
+}
+
+void 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);
+ va_end(vl);
+ *d_os << buf;
+}
+
+void 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);
+ va_end(vl);
+ *d_os << buf;
+}
+
+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;
+ }
+}
+
+void TraceC::printf(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;
+ }
+}
}/* CVC4 namespace */
public:
DebugC(std::ostream* os) : d_os(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 operator()(const char* tag, const char* s) {
+ if(d_tags.find(std::string(tag)) != d_tags.end()) {
+ *d_os << s;
+ }
+ }
- static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
- static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+ void operator()(const char* tag, const std::string& s) {
+ if(d_tags.find(std::string(tag)) != d_tags.end()) {
+ *d_os << s;
+ }
+ }
+
+ void operator()(const std::string& tag, const char* s) {
+ if(d_tags.find(tag) != d_tags.end()) {
+ *d_os << s;
+ }
+ }
+
+ void operator()(const std::string& tag, const std::string& s) {
+ if(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)));
std::ostream& operator()(const char* tag) {
- if(d_tags.find(std::string(tag)) != d_tags.end())
+ if(d_tags.find(std::string(tag)) != d_tags.end()) {
return *d_os;
- else return null_os;
+ } else {
+ return null_os;
+ }
}
std::ostream& operator()(std::string tag) {
- if(d_tags.find(tag) != d_tags.end())
+ if(d_tags.find(tag) != d_tags.end()) {
return *d_os;
- else return null_os;
+ } else {
+ return null_os;
+ }
}
/**
* The "Yeting option" - this allows use of Debug() without a tag
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))) {
- // 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;
- }
- void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) {
- }
+ void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
+ void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
std::ostream& operator()(const char* tag) {
- if(d_tags.find(tag) != d_tags.end())
+ if(d_tags.find(tag) != d_tags.end()) {
return *d_os;
- else return null_os;
+ } else {
+ return null_os;
+ }
}
std::ostream& operator()(std::string tag) {
- if(d_tags.find(tag) != d_tags.end())
+ if(d_tags.find(tag) != d_tags.end()) {
return *d_os;
- else return null_os;
+ } else {
+ return null_os;
+ }
}
void on (const char* tag) { d_tags.insert(std::string(tag)); };
struct Test2;
struct Test3;
struct Test4;
+struct Test5;
typedef Attribute<Test1, std::string> TestStringAttr1;
typedef Attribute<Test2, std::string> TestStringAttr2;
-typedef Attribute<Test3, bool> TestFlag1;
-typedef Attribute<Test4, bool> TestFlag2;
+typedef Attribute<Test1, bool> TestFlag1;
+typedef Attribute<Test2, bool> TestFlag2;
+typedef Attribute<Test3, bool> TestFlag3;
+typedef Attribute<Test4, bool> TestFlag4;
+typedef Attribute<Test5, bool> TestFlag5;
class NodeWhite : public CxxTest::TestSuite {
TS_ASSERT(TestFlag1::s_id == 0);
TS_ASSERT(TestFlag2::s_id == 1);
- TS_ASSERT(attr::LastAttributeId<bool>::s_id == 2);
- TS_ASSERT(TestFlag1::s_bit == 0);
- TS_ASSERT(TestFlag2::s_bit == 1);
- TS_ASSERT(attr::BitAssignment::s_bit == 2);
+ TS_ASSERT(TestFlag3::s_id == 2);
+ TS_ASSERT(TestFlag4::s_id == 3);
+ TS_ASSERT(TestFlag5::s_id == 4);
+ TS_ASSERT(attr::LastAttributeId<bool>::s_id == 5);
}
void testAttributes() {
AttributeManager& am = d_nm->d_am;
+ //Debug.on("boolattr");
+
Node a = d_nm->mkVar();
Node b = d_nm->mkVar();
Node c = d_nm->mkVar();
b.setAttribute(VarNameAttr(), "b");
c.setAttribute(VarNameAttr(), "c");
+ // test that all boolean flags are FALSE to start
+ 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");
+ TS_ASSERT(! b.getAttribute(TestFlag1()));
+ 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");
+ TS_ASSERT(! unnamed.getAttribute(TestFlag1()));
+
+ 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");
+ TS_ASSERT(! b.getAttribute(TestFlag2()));
+ 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");
+ TS_ASSERT(! unnamed.getAttribute(TestFlag2()));
+
+ 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");
+ TS_ASSERT(! b.getAttribute(TestFlag3()));
+ 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");
+ TS_ASSERT(! unnamed.getAttribute(TestFlag3()));
+
+ 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");
+ TS_ASSERT(! b.getAttribute(TestFlag4()));
+ 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");
+ TS_ASSERT(! unnamed.getAttribute(TestFlag4()));
+
+ 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");
+ TS_ASSERT(! b.getAttribute(TestFlag5()));
+ 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");
+ TS_ASSERT(! unnamed.getAttribute(TestFlag5()));
+
+ // test that they all HAVE the boolean attributes
+ Debug("boolattr", "get flag 1 on a (should be F)\n");
+ TS_ASSERT(a.hasAttribute(TestFlag1()));
+ Debug("boolattr", "get flag 1 on b (should be F)\n");
+ TS_ASSERT(b.hasAttribute(TestFlag1()));
+ Debug("boolattr", "get flag 1 on c (should be F)\n");
+ TS_ASSERT(c.hasAttribute(TestFlag1()));
+ Debug("boolattr", "get flag 1 on unnamed (should be F)\n");
+ TS_ASSERT(unnamed.hasAttribute(TestFlag1()));
+
+ Debug("boolattr", "get flag 2 on a (should be F)\n");
+ TS_ASSERT(a.hasAttribute(TestFlag2()));
+ Debug("boolattr", "get flag 2 on b (should be F)\n");
+ TS_ASSERT(b.hasAttribute(TestFlag2()));
+ Debug("boolattr", "get flag 2 on c (should be F)\n");
+ TS_ASSERT(c.hasAttribute(TestFlag2()));
+ Debug("boolattr", "get flag 2 on unnamed (should be F)\n");
+ TS_ASSERT(unnamed.hasAttribute(TestFlag2()));
+
+ Debug("boolattr", "get flag 3 on a (should be F)\n");
+ TS_ASSERT(a.hasAttribute(TestFlag3()));
+ Debug("boolattr", "get flag 3 on b (should be F)\n");
+ TS_ASSERT(b.hasAttribute(TestFlag3()));
+ Debug("boolattr", "get flag 3 on c (should be F)\n");
+ TS_ASSERT(c.hasAttribute(TestFlag3()));
+ Debug("boolattr", "get flag 3 on unnamed (should be F)\n");
+ TS_ASSERT(unnamed.hasAttribute(TestFlag3()));
+
+ Debug("boolattr", "get flag 4 on a (should be F)\n");
+ TS_ASSERT(a.hasAttribute(TestFlag4()));
+ Debug("boolattr", "get flag 4 on b (should be F)\n");
+ TS_ASSERT(b.hasAttribute(TestFlag4()));
+ Debug("boolattr", "get flag 4 on c (should be F)\n");
+ TS_ASSERT(c.hasAttribute(TestFlag4()));
+ Debug("boolattr", "get flag 4 on unnamed (should be F)\n");
+ TS_ASSERT(unnamed.hasAttribute(TestFlag4()));
+
+ Debug("boolattr", "get flag 5 on a (should be F)\n");
+ TS_ASSERT(a.hasAttribute(TestFlag5()));
+ Debug("boolattr", "get flag 5 on b (should be F)\n");
+ TS_ASSERT(b.hasAttribute(TestFlag5()));
+ Debug("boolattr", "get flag 5 on c (should be F)\n");
+ TS_ASSERT(c.hasAttribute(TestFlag5()));
+ Debug("boolattr", "get flag 5 on unnamed (should be F)\n");
+ TS_ASSERT(unnamed.hasAttribute(TestFlag5()));
+
+ // test two-arg version of hasAttribute()
+ bool bb;
+ Debug("boolattr", "get flag 1 on a (should be F)\n");
+ TS_ASSERT(a.hasAttribute(TestFlag1(), &bb));
+ TS_ASSERT(! bb);
+ Debug("boolattr", "get flag 1 on b (should be F)\n");
+ TS_ASSERT(b.hasAttribute(TestFlag1(), &bb));
+ TS_ASSERT(! bb);
+ Debug("boolattr", "get flag 1 on c (should be F)\n");
+ TS_ASSERT(c.hasAttribute(TestFlag1(), &bb));
+ TS_ASSERT(! bb);
+ Debug("boolattr", "get flag 1 on unnamed (should be F)\n");
+ TS_ASSERT(unnamed.hasAttribute(TestFlag1(), &bb));
+ TS_ASSERT(! bb);
+
+ Debug("boolattr", "get flag 2 on a (should be F)\n");
+ TS_ASSERT(a.hasAttribute(TestFlag2(), &bb));
+ TS_ASSERT(! bb);
+ Debug("boolattr", "get flag 2 on b (should be F)\n");
+ TS_ASSERT(b.hasAttribute(TestFlag2(), &bb));
+ TS_ASSERT(! bb);
+ Debug("boolattr", "get flag 2 on c (should be F)\n");
+ TS_ASSERT(c.hasAttribute(TestFlag2(), &bb));
+ TS_ASSERT(! bb);
+ Debug("boolattr", "get flag 2 on unnamed (should be F)\n");
+ TS_ASSERT(unnamed.hasAttribute(TestFlag2(), &bb));
+ TS_ASSERT(! bb);
+
+ Debug("boolattr", "get flag 3 on a (should be F)\n");
+ TS_ASSERT(a.hasAttribute(TestFlag3(), &bb));
+ TS_ASSERT(! bb);
+ Debug("boolattr", "get flag 3 on b (should be F)\n");
+ TS_ASSERT(b.hasAttribute(TestFlag3(), &bb));
+ TS_ASSERT(! bb);
+ Debug("boolattr", "get flag 3 on c (should be F)\n");
+ TS_ASSERT(c.hasAttribute(TestFlag3(), &bb));
+ TS_ASSERT(! bb);
+ Debug("boolattr", "get flag 3 on unnamed (should be F)\n");
+ TS_ASSERT(unnamed.hasAttribute(TestFlag3(), &bb));
+ TS_ASSERT(! bb);
+
+ Debug("boolattr", "get flag 4 on a (should be F)\n");
+ TS_ASSERT(a.hasAttribute(TestFlag4(), &bb));
+ TS_ASSERT(! bb);
+ Debug("boolattr", "get flag 4 on b (should be F)\n");
+ TS_ASSERT(b.hasAttribute(TestFlag4(), &bb));
+ TS_ASSERT(! bb);
+ Debug("boolattr", "get flag 4 on c (should be F)\n");
+ TS_ASSERT(c.hasAttribute(TestFlag4(), &bb));
+ TS_ASSERT(! bb);
+ Debug("boolattr", "get flag 4 on unnamed (should be F)\n");
+ TS_ASSERT(unnamed.hasAttribute(TestFlag4(), &bb));
+ TS_ASSERT(! bb);
+
+ Debug("boolattr", "get flag 5 on a (should be F)\n");
+ TS_ASSERT(a.hasAttribute(TestFlag5(), &bb));
+ TS_ASSERT(! bb);
+ Debug("boolattr", "get flag 5 on b (should be F)\n");
+ TS_ASSERT(b.hasAttribute(TestFlag5(), &bb));
+ TS_ASSERT(! bb);
+ Debug("boolattr", "get flag 5 on c (should be F)\n");
+ TS_ASSERT(c.hasAttribute(TestFlag5(), &bb));
+ TS_ASSERT(! bb);
+ Debug("boolattr", "get flag 5 on unnamed (should be F)\n");
+ TS_ASSERT(unnamed.hasAttribute(TestFlag5(), &bb));
+ TS_ASSERT(! bb);
+
+ // setting boolean flags
+ Debug("boolattr", "set flag 1 on a to T\n");
a.setAttribute(TestFlag1(), true);
+ Debug("boolattr", "set flag 1 on b to F\n");
b.setAttribute(TestFlag1(), false);
+ Debug("boolattr", "set flag 1 on c to F\n");
c.setAttribute(TestFlag1(), false);
+ Debug("boolattr", "set flag 1 on unnamed to T\n");
unnamed.setAttribute(TestFlag1(), true);
+ Debug("boolattr", "set flag 2 on a to F\n");
a.setAttribute(TestFlag2(), false);
+ Debug("boolattr", "set flag 2 on b to T\n");
b.setAttribute(TestFlag2(), true);
+ Debug("boolattr", "set flag 2 on c to T\n");
c.setAttribute(TestFlag2(), true);
+ Debug("boolattr", "set flag 2 on unnamed to F\n");
unnamed.setAttribute(TestFlag2(), false);
+ Debug("boolattr", "set flag 3 on a to T\n");
+ a.setAttribute(TestFlag3(), true);
+ Debug("boolattr", "set flag 3 on b to T\n");
+ b.setAttribute(TestFlag3(), true);
+ Debug("boolattr", "set flag 3 on c to T\n");
+ c.setAttribute(TestFlag3(), true);
+ Debug("boolattr", "set flag 3 on unnamed to T\n");
+ unnamed.setAttribute(TestFlag3(), true);
+
+ Debug("boolattr", "set flag 4 on a to T\n");
+ a.setAttribute(TestFlag4(), true);
+ Debug("boolattr", "set flag 4 on b to T\n");
+ b.setAttribute(TestFlag4(), true);
+ Debug("boolattr", "set flag 4 on c to T\n");
+ c.setAttribute(TestFlag4(), true);
+ Debug("boolattr", "set flag 4 on unnamed to T\n");
+ unnamed.setAttribute(TestFlag4(), true);
+
+ Debug("boolattr", "set flag 5 on a to T\n");
+ a.setAttribute(TestFlag5(), true);
+ Debug("boolattr", "set flag 5 on b to T\n");
+ b.setAttribute(TestFlag5(), true);
+ Debug("boolattr", "set flag 5 on c to F\n");
+ c.setAttribute(TestFlag5(), false);
+ Debug("boolattr", "set flag 5 on unnamed to T\n");
+ unnamed.setAttribute(TestFlag5(), true);
+
TS_ASSERT(a.getAttribute(VarNameAttr()) == "a");
TS_ASSERT(a.getAttribute(VarNameAttr()) != "b");
TS_ASSERT(a.getAttribute(VarNameAttr()) != "c");
TS_ASSERT(! c.hasAttribute(TestStringAttr2()));
TS_ASSERT(! unnamed.hasAttribute(TestStringAttr2()));
+ 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");
TS_ASSERT(! b.getAttribute(TestFlag1()));
+ 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");
TS_ASSERT(unnamed.getAttribute(TestFlag1()));
+ 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");
TS_ASSERT(b.getAttribute(TestFlag2()));
+ 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");
TS_ASSERT(! unnamed.getAttribute(TestFlag2()));
+ 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");
+ TS_ASSERT(b.getAttribute(TestFlag3()));
+ 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");
+ TS_ASSERT(unnamed.getAttribute(TestFlag3()));
+
+ 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");
+ TS_ASSERT(b.getAttribute(TestFlag4()));
+ 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");
+ TS_ASSERT(unnamed.getAttribute(TestFlag4()));
+
+ 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");
+ TS_ASSERT(b.getAttribute(TestFlag5()));
+ 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");
+ TS_ASSERT(unnamed.getAttribute(TestFlag5()));
+
a.setAttribute(TestStringAttr1(), "foo");
b.setAttribute(TestStringAttr1(), "bar");
c.setAttribute(TestStringAttr1(), "baz");
projects / cvc5.git / commitdiff