summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/attribute.h54
-rw-r--r--src/expr/node.cpp44
-rw-r--r--src/expr/node.h21
3 files changed, 33 insertions, 86 deletions
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 1d2705240..12de9eb5f 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -56,7 +56,7 @@ namespace expr {
struct AttrHashFcn {
enum { LARGE_PRIME = 1 };
- std::size_t operator()(const std::pair<uint64_t, SoftNode>& p) const {
+ std::size_t operator()(const std::pair<unsigned, SoftNode>& p) const {
return p.first * LARGE_PRIME + p.second.hash();
}
};
@@ -122,7 +122,7 @@ struct KindTableMapping {
// use a TAG to indicate which table it should be in
template <class value_type>
-struct AttrHash : public __gnu_cxx::hash_map<std::pair<uint64_t, SoftNode>, value_type, AttrHashFcn> {};
+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> {
@@ -215,23 +215,19 @@ class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHas
public:
- typedef std::pair<uint64_t, SoftNode> key_type;
+ typedef std::pair<unsigned, SoftNode> key_type;
typedef bool data_type;
typedef std::pair<const key_type, data_type> value_type;
typedef BitIterator iterator;
typedef ConstBitIterator const_iterator;
- BitIterator find(const std::pair<uint64_t, SoftNode>& k) {
+ BitIterator find(const std::pair<unsigned, SoftNode>& k) {
super::iterator i = super::find(k.second);
if(i == super::end()) {
return BitIterator();
}
- Debug.printf("boolattr",
- "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
- &(*i).second,
- (unsigned long long)((*i).second),
- unsigned(k.first));
+ 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);
}
@@ -239,16 +235,12 @@ public:
return BitIterator();
}
- ConstBitIterator find(const std::pair<uint64_t, SoftNode>& k) const {
+ 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,
- (unsigned long long)((*i).second),
- unsigned(k.first));
+ 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);
}
@@ -256,7 +248,7 @@ public:
return ConstBitIterator();
}
- BitAccessor operator[](const std::pair<uint64_t, SoftNode>& k) {
+ BitAccessor operator[](const std::pair<unsigned, SoftNode>& k) {
uint64_t& word = super::operator[](k.second);
return BitAccessor(word, k.first);
}
@@ -276,18 +268,18 @@ struct Attribute {
/** cleanup routine when the Node goes away */
static inline void cleanup(const value_t&) {}
- static inline uint64_t getId() { return s_id; }
- static inline uint64_t getHashValue() { return s_hashValue; }
+ 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 const uint64_t s_id;
+ static const unsigned s_id;
/** an extra hash value (to avoid same-value-type collisions) */
- static const uint64_t s_hashValue;
+ static const unsigned s_hashValue;
};
/**
@@ -302,13 +294,13 @@ struct Attribute<T, bool> {
/** cleanup routine when the Node goes away */
static inline void cleanup(const bool&) {}
- static inline uint64_t getId() { return s_id; }
- static inline uint64_t getHashValue() { return s_hashValue; }
+ static inline unsigned getId() { return s_id; }
+ static inline unsigned getHashValue() { return s_hashValue; }
static const bool has_default_value = true;
static const bool default_value = false;
- static inline uint64_t checkID(uint64_t id) {
+ static inline unsigned checkID(unsigned id) {
AlwaysAssert(id <= 63,
"Too many boolean node attributes registered during initialization !");
return id;
@@ -317,10 +309,10 @@ struct Attribute<T, bool> {
private:
/** a bit assignment */
- static const uint64_t s_id;
+ static const unsigned s_id;
/** an extra hash value (to avoid same-value-type collisions) */
- static const uint64_t s_hashValue;
+ static const unsigned s_hashValue;
};
// SPECIFIC, GLOBAL ATTRIBUTE DEFINITIONS ======================================
@@ -331,11 +323,11 @@ namespace attr {
template <class T>
struct LastAttributeId {
- static uint64_t s_id;
+ static unsigned s_id;
};
template <class T>
- uint64_t LastAttributeId<T>::s_id = 0;
+ unsigned LastAttributeId<T>::s_id = 0;
}/* CVC4::expr::attr namespace */
typedef Attribute<attr::VarName, std::string> VarNameAttr;
@@ -344,16 +336,16 @@ typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr;
// ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
template <class T, class value_t>
-const uint64_t 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>
-const uint64_t 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>
-const uint64_t Attribute<T, bool>::s_id =
+const unsigned Attribute<T, bool>::s_id =
Attribute<T, bool>::checkID(attr::LastAttributeId<bool>::s_id++);
template <class T>
-const uint64_t Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id;
+const unsigned Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id;
class AttributeManager;
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 79490d58e..644570b24 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -97,83 +97,51 @@ Node& Node::operator=(const Node& e) {
}
Node Node::eqExpr(const Node& right) const {
- Assert( NodeManager::currentNM() != NULL,
- "There is no current CVC4::NodeManager associated to this thread.\n"
- "Perhaps a public-facing function is missing a NodeManagerScope ?" );
-
return NodeManager::currentNM()->mkNode(EQUAL, *this, right);
}
Node Node::notExpr() const {
- Assert( NodeManager::currentNM() != NULL,
- "There is no current CVC4::NodeManager associated to this thread.\n"
- "Perhaps a public-facing function is missing a NodeManagerScope ?" );
-
return NodeManager::currentNM()->mkNode(NOT, *this);
}
Node Node::andExpr(const Node& right) const {
- Assert( NodeManager::currentNM() != NULL,
- "There is no current CVC4::NodeManager associated to this thread.\n"
- "Perhaps a public-facing function is missing a NodeManagerScope ?" );
-
return NodeManager::currentNM()->mkNode(AND, *this, right);
}
Node Node::orExpr(const Node& right) const {
- Assert( NodeManager::currentNM() != NULL,
- "There is no current CVC4::NodeManager associated to this thread.\n"
- "Perhaps a public-facing function is missing a NodeManagerScope ?" );
-
return NodeManager::currentNM()->mkNode(OR, *this, right);
}
Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const {
- Assert( NodeManager::currentNM() != NULL,
- "There is no current CVC4::NodeManager associated to this thread.\n"
- "Perhaps a public-facing function is missing a NodeManagerScope ?" );
-
return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart);
}
Node Node::iffExpr(const Node& right) const {
- Assert( NodeManager::currentNM() != NULL,
- "There is no current CVC4::NodeManager associated to this thread.\n"
- "Perhaps a public-facing function is missing a NodeManagerScope ?" );
-
return NodeManager::currentNM()->mkNode(IFF, *this, right);
}
Node Node::impExpr(const Node& right) const {
- Assert( NodeManager::currentNM() != NULL,
- "There is no current CVC4::NodeManager associated to this thread.\n"
- "Perhaps a public-facing function is missing a NodeManagerScope ?" );
-
return NodeManager::currentNM()->mkNode(IMPLIES, *this, right);
}
Node Node::xorExpr(const Node& right) const {
- Assert( NodeManager::currentNM() != NULL,
- "There is no current CVC4::NodeManager associated to this thread.\n"
- "Perhaps a public-facing function is missing a NodeManagerScope ?" );
-
return NodeManager::currentNM()->mkNode(XOR, *this, right);
}
-static void indent(ostream & o, int indent) {
- for(int i=0; i < indent; i++) {
+static void indent(ostream & o, int indent){
+ for(int i=0; i < indent; i++)
o << ' ';
- }
}
void Node::printAst(ostream & o, int ind) const {
indent(o, ind);
o << '(';
o << getKind();
- if(getKind() == VARIABLE) {
+ if(getKind() == VARIABLE){
o << ' ' << getId();
- } else if(getNumChildren() >= 1) {
- for(Node::iterator child = begin(); child != end(); ++child) {
+
+ }else if(getNumChildren() >= 1){
+ for(Node::iterator child = begin(); child != end(); ++child){
o << endl;
(*child).printAst(o, ind + 1);
}
diff --git a/src/expr/node.h b/src/expr/node.h
index a39dc5b7e..463ff8144 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -48,6 +48,7 @@ using CVC4::expr::NodeValue;
class Node {
friend class NodeValue;
+ friend class SoftNode;
/** A convenient null-valued encapsulated pointer */
static Node s_null;
@@ -105,7 +106,7 @@ public:
bool operator!=(const Node& e) const { return d_ev != e.d_ev; }
Node operator[](int i) const {
- Assert(i >= 0 && unsigned(i) < d_ev->d_nchildren);
+ Assert(i >= 0 && i < d_ev->d_nchildren);
return Node(d_ev->d_children[i]);
}
@@ -129,11 +130,9 @@ public:
Node impExpr(const Node& right) const;
Node xorExpr(const Node& right) const;
- /*
Node plusExpr(const Node& right) const;
Node uMinusExpr() const;
Node multExpr(const Node& right) const;
- */
inline Kind getKind() const;
@@ -172,9 +171,9 @@ public:
* @param indent number of spaces to indent the formula by.
*/
void printAst(std::ostream & o, int indent = 0) const;
-
+
private:
-
+
/**
* Pretty printer for use within gdb
* This is not intended to be used outside of gdb.
@@ -263,30 +262,18 @@ inline size_t Node::getNumChildren() const {
template <class AttrKind>
inline typename AttrKind::value_type Node::getAttribute(const AttrKind&) {
- Assert( NodeManager::currentNM() != NULL,
- "There is no current CVC4::NodeManager associated to this thread.\n"
- "Perhaps a public-facing function is missing a NodeManagerScope ?" );
-
return NodeManager::currentNM()->getAttribute(*this, AttrKind());
}
template <class AttrKind>
inline bool Node::hasAttribute(const AttrKind&,
typename AttrKind::value_type* ret) {
- Assert( NodeManager::currentNM() != NULL,
- "There is no current CVC4::NodeManager associated to this thread.\n"
- "Perhaps a public-facing function is missing a NodeManagerScope ?" );
-
return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret);
}
template <class AttrKind>
inline void Node::setAttribute(const AttrKind&,
const typename AttrKind::value_type& value) {
- Assert( NodeManager::currentNM() != NULL,
- "There is no current CVC4::NodeManager associated to this thread.\n"
- "Perhaps a public-facing function is missing a NodeManagerScope ?" );
-
NodeManager::currentNM()->setAttribute(*this, AttrKind(), value);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback