summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/Makefile.am1
-rw-r--r--src/expr/attribute.cpp63
-rw-r--r--src/expr/attribute.h94
-rw-r--r--src/expr/attribute_internals.h19
-rw-r--r--src/expr/attribute_unique_id.h52
-rw-r--r--src/expr/node.h8
-rw-r--r--src/expr/node_manager.cpp8
-rw-r--r--src/expr/node_manager.h13
-rw-r--r--src/expr/node_value.h2
9 files changed, 260 insertions, 0 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 16ee454c8..13358d294 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -20,6 +20,7 @@ libexpr_la_SOURCES = \
node_manager.cpp \
node_manager_attributes.h \
type_checker.h \
+ attribute_unique_id.h \
attribute.h \
attribute_internals.h \
attribute.cpp \
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 20d52e3cc..92a21546c 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -26,6 +26,15 @@ namespace CVC4 {
namespace expr {
namespace attr {
+
+void AttributeManager::debugHook(int debugFlag) {
+ /* DO NOT CHECK IN ANY CODE INTO THE DEBUG HOOKS!
+ * debugHook() is an empty function for the purpose of debugging
+ * the AttributeManager without recompiling all of CVC4.
+ * Formally this is a nop.
+ */
+}
+
void AttributeManager::deleteAllAttributes(NodeValue* nv) {
d_bools.erase(nv);
deleteFromTable(d_ints, nv);
@@ -60,6 +69,60 @@ void AttributeManager::deleteAllAttributes() {
d_cdptrs.clear();
}
+void AttributeManager::deleteAttributes(const AttrIdVec& atids){
+ typedef std::map<uint64_t, std::vector< uint64_t> > AttrToVecMap;
+ AttrToVecMap perTableIds;
+
+ for(AttrIdVec::const_iterator it = atids.begin(), it_end = atids.end(); it != it_end; ++it){
+ const AttributeUniqueId& pair = *(*it);
+ std::vector< uint64_t>& inTable = perTableIds[pair.getTableId()];
+ inTable.push_back(pair.getWithinTypeId());
+ }
+ AttrToVecMap::iterator it = perTableIds.begin(), it_end = perTableIds.end();
+ for(; it != it_end; ++it){
+ Assert(((*it).first) <= LastAttrTable);
+ AttrTableId tableId = (AttrTableId) ((*it).first);
+ std::vector< uint64_t>& ids = (*it).second;
+ std::sort(ids.begin(), ids.end());
+
+ switch(tableId){
+ case AttrTableBool:
+ Unimplemented("delete attributes is unimplemented for bools");
+ break;
+ case AttrTableUInt64:
+ deleteAttributesFromTable(d_ints, ids);
+ break;
+ case AttrTableTNode:
+ deleteAttributesFromTable(d_tnodes, ids);
+ break;
+ case AttrTableNode:
+ deleteAttributesFromTable(d_nodes, ids);
+ break;
+ case AttrTableTypeNode:
+ deleteAttributesFromTable(d_types, ids);
+ break;
+ case AttrTableString:
+ deleteAttributesFromTable(d_strings, ids);
+ break;
+ case AttrTablePointer:
+ deleteAttributesFromTable(d_ptrs, ids);
+ break;
+
+ case AttrTableCDBool:
+ case AttrTableCDUInt64:
+ case AttrTableCDTNode:
+ case AttrTableCDNode:
+ case AttrTableCDString:
+ case AttrTableCDPointer:
+ Unimplemented("CDAttributes cannot be deleted. Contact Tim/Morgan if this behaviour is desired.");
+ break;
+ case LastAttrTable:
+ default:
+ Unreachable();
+ }
+ }
+}
+
}/* CVC4::expr::attr namespace */
}/* CVC4::expr namespace */
}/* CVC4 namespace */
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index f9939fa90..605427190 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -26,6 +26,7 @@
#include <string>
#include <stdint.h>
+#include "expr/attribute_unique_id.h"
// include supporting templates
#define CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
@@ -87,6 +88,12 @@ class AttributeManager {
template <class T>
void deleteAllFromTable(AttrHash<T>& table);
+ template <class T>
+ void deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids);
+
+ template <class T>
+ void reconstructTable(AttrHash<T>& table);
+
/**
* getTable<> is a helper template that gets the right table from an
* AttributeManager given its type.
@@ -169,6 +176,29 @@ public:
* Remove all attributes from the tables.
*/
void deleteAllAttributes();
+
+
+ /**
+ * Determines the AttrTableId of an attribute.
+ *
+ * @param attr the attribute
+ * @return the id of the attribute table.
+ */
+ template <class AttrKind>
+ static AttributeUniqueId getAttributeId(const AttrKind& attr);
+
+ /** A list of attributes. */
+ typedef std::vector< const AttributeUniqueId* > AttrIdVec;
+
+ /** Deletes a list of attributes. */
+ void deleteAttributes(const AttrIdVec& attributeIds);
+
+ /**
+ * debugHook() is an empty function for the purpose of debugging
+ * the AttributeManager without recompiling all of CVC4.
+ * Formally this is a nop.
+ */
+ void debugHook(int debugFlag);
};
}/* CVC4::expr::attr namespace */
@@ -187,6 +217,7 @@ struct getTable;
/** Access the "d_bools" member of AttributeManager. */
template <>
struct getTable<bool, false> {
+ static const AttrTableId id = AttrTableBool;
typedef AttrHash<bool> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_bools;
@@ -199,6 +230,7 @@ struct getTable<bool, false> {
/** Access the "d_ints" member of AttributeManager. */
template <>
struct getTable<uint64_t, false> {
+ static const AttrTableId id = AttrTableUInt64;
typedef AttrHash<uint64_t> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_ints;
@@ -211,6 +243,7 @@ struct getTable<uint64_t, false> {
/** Access the "d_tnodes" member of AttributeManager. */
template <>
struct getTable<TNode, false> {
+ static const AttrTableId id = AttrTableTNode;
typedef AttrHash<TNode> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_tnodes;
@@ -223,6 +256,7 @@ struct getTable<TNode, false> {
/** Access the "d_nodes" member of AttributeManager. */
template <>
struct getTable<Node, false> {
+ static const AttrTableId id = AttrTableNode;
typedef AttrHash<Node> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_nodes;
@@ -235,6 +269,7 @@ struct getTable<Node, false> {
/** Access the "d_types" member of AttributeManager. */
template <>
struct getTable<TypeNode, false> {
+ static const AttrTableId id = AttrTableTypeNode;
typedef AttrHash<TypeNode> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_types;
@@ -247,6 +282,7 @@ struct getTable<TypeNode, false> {
/** Access the "d_strings" member of AttributeManager. */
template <>
struct getTable<std::string, false> {
+ static const AttrTableId id = AttrTableString;
typedef AttrHash<std::string> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_strings;
@@ -259,6 +295,7 @@ struct getTable<std::string, false> {
/** Access the "d_ptrs" member of AttributeManager. */
template <class T>
struct getTable<T*, false> {
+ static const AttrTableId id = AttrTablePointer;
typedef AttrHash<void*> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_ptrs;
@@ -271,6 +308,7 @@ struct getTable<T*, false> {
/** Access the "d_ptrs" member of AttributeManager. */
template <class T>
struct getTable<const T*, false> {
+ static const AttrTableId id = AttrTablePointer;
typedef AttrHash<void*> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_ptrs;
@@ -283,6 +321,7 @@ struct getTable<const T*, false> {
/** Access the "d_cdbools" member of AttributeManager. */
template <>
struct getTable<bool, true> {
+ static const AttrTableId id = AttrTableCDBool;
typedef CDAttrHash<bool> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_cdbools;
@@ -295,6 +334,7 @@ struct getTable<bool, true> {
/** Access the "d_cdints" member of AttributeManager. */
template <>
struct getTable<uint64_t, true> {
+ static const AttrTableId id = AttrTableCDUInt64;
typedef CDAttrHash<uint64_t> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_cdints;
@@ -307,6 +347,7 @@ struct getTable<uint64_t, true> {
/** Access the "d_tnodes" member of AttributeManager. */
template <>
struct getTable<TNode, true> {
+ static const AttrTableId id = AttrTableCDTNode;
typedef CDAttrHash<TNode> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_cdtnodes;
@@ -319,6 +360,7 @@ struct getTable<TNode, true> {
/** Access the "d_cdnodes" member of AttributeManager. */
template <>
struct getTable<Node, true> {
+ static const AttrTableId id = AttrTableCDNode;
typedef CDAttrHash<Node> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_cdnodes;
@@ -331,6 +373,7 @@ struct getTable<Node, true> {
/** Access the "d_cdstrings" member of AttributeManager. */
template <>
struct getTable<std::string, true> {
+ static const AttrTableId id = AttrTableCDString;
typedef CDAttrHash<std::string> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_cdstrings;
@@ -343,6 +386,7 @@ struct getTable<std::string, true> {
/** Access the "d_cdptrs" member of AttributeManager. */
template <class T>
struct getTable<T*, true> {
+ static const AttrTableId id = AttrTableCDPointer;
typedef CDAttrHash<void*> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_cdptrs;
@@ -355,6 +399,7 @@ struct getTable<T*, true> {
/** Access the "d_cdptrs" member of AttributeManager. */
template <class T>
struct getTable<const T*, true> {
+ static const AttrTableId id = AttrTableCDPointer;
typedef CDAttrHash<void*> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_cdptrs;
@@ -584,6 +629,55 @@ inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
table.clear();
}
+template <class AttrKind>
+AttributeUniqueId AttributeManager::getAttributeId(const AttrKind& attr){
+ typedef typename AttrKind::value_type value_type;
+ AttrTableId tableId = getTable<value_type,
+ AttrKind::context_dependent>::id;
+ return AttributeUniqueId(tableId, attr.getId());
+}
+
+template <class T>
+void AttributeManager::deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids){
+ typedef AttributeTraits<T, false> traits_t;
+ typedef AttrHash<T> hash_t;
+
+ typename hash_t::iterator it = table.begin();
+ typename hash_t::iterator tmp;
+ typename hash_t::iterator it_end = table.end();
+
+ std::vector<uint64_t>::const_iterator begin_ids = ids.begin();
+ std::vector<uint64_t>::const_iterator end_ids = ids.end();
+
+ size_t initialSize = table.size();
+ while (it != it_end){
+ uint64_t id = (*it).first.first;
+
+ if(std::binary_search(begin_ids, end_ids, id)){
+ tmp = it;
+ ++it;
+ if(traits_t::getCleanup()[id] != NULL) {
+ traits_t::getCleanup()[id]((*tmp).second);
+ }
+ table.erase(tmp);
+ }else{
+ ++it;
+ }
+ }
+ static const size_t ReconstructShrinkRatio = 8;
+ if(initialSize/ReconstructShrinkRatio > table.size()){
+ reconstructTable(table);
+ }
+}
+
+template <class T>
+void AttributeManager::reconstructTable(AttrHash<T>& table){
+ typedef AttrHash<T> hash_t;
+ hash_t cpy;
+ cpy.insert(table.begin(), table.end());
+ cpy.swap(table);
+}
+
}/* CVC4::expr::attr namespace */
}/* CVC4::expr namespace */
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index a0086440b..fa6459481 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -357,6 +357,15 @@ public:
super::clear();
}
+ /** Is the hash table empty? */
+ bool empty() const {
+ return super::empty();
+ }
+
+ /** This is currently very misleading! */
+ size_t size() const {
+ return super::size();
+ }
};/* class AttrHash<bool> */
/**
@@ -558,6 +567,16 @@ public:
super::clear();
}
+ /** Is the hash table empty? */
+ bool empty() const {
+ return super::empty();
+ }
+
+ /** This is currently very misleading! */
+ size_t size() const {
+ return super::size();
+ }
+
};/* class CDAttrHash<bool> */
}/* CVC4::expr::attr namespace */
diff --git a/src/expr/attribute_unique_id.h b/src/expr/attribute_unique_id.h
new file mode 100644
index 000000000..79c6bfd8f
--- /dev/null
+++ b/src/expr/attribute_unique_id.h
@@ -0,0 +1,52 @@
+
+#pragma once
+
+#include "cvc4_private.h"
+#include <stdint.h>
+
+// ATTRIBUTE IDs ============================================================
+
+namespace CVC4 {
+namespace expr {
+namespace attr {
+
+/** A unique id for each attribute table. */
+enum AttrTableId {
+ AttrTableBool,
+ AttrTableUInt64,
+ AttrTableTNode,
+ AttrTableNode,
+ AttrTableTypeNode,
+ AttrTableString,
+ AttrTablePointer,
+ AttrTableCDBool,
+ AttrTableCDUInt64,
+ AttrTableCDTNode,
+ AttrTableCDNode,
+ AttrTableCDString,
+ AttrTableCDPointer,
+ LastAttrTable
+};
+
+/**
+ * This uniquely indentifies attributes across tables.
+ */
+class AttributeUniqueId {
+ AttrTableId d_tableId;
+ uint64_t d_withinTypeId;
+
+public:
+ AttributeUniqueId() : d_tableId(LastAttrTable), d_withinTypeId(0){}
+
+ AttributeUniqueId(AttrTableId tableId, uint64_t within)
+ : d_tableId(tableId), d_withinTypeId(within)
+ {}
+
+ AttrTableId getTableId() const{ return d_tableId; }
+ uint64_t getWithinTypeId() const{ return d_withinTypeId; }
+
+};/* CVC4::expr::attr::AttributeUniqueId */
+
+}/* CVC4::expr::attr namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
diff --git a/src/expr/node.h b/src/expr/node.h
index 3a5b6f135..0a4b853aa 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -566,6 +566,14 @@ public:
inline const T& getConst() const;
/**
+ * Returns the reference count of this node.
+ * @return the refcount
+ */
+ unsigned getRefCount() const {
+ return d_nv->getRefCount();
+ }
+
+ /**
* Returns the value of the given attribute that this has been attached.
* @param attKind the kind of the attribute
* @return the value of the attribute
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index f6424cfe0..cede6ff1f 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -586,4 +586,12 @@ Node NodeManager::mkAbstractValue(const TypeNode& type) {
return n;
}
+void NodeManager::deleteAttributes(const std::vector<const expr::attr::AttributeUniqueId*>& ids){
+ d_attrManager->deleteAttributes(ids);
+}
+
+void NodeManager::debugHook(int debugFlag){
+ // For debugging purposes only, DO NOT CHECK IN ANY CODE!
+}
+
}/* CVC4 namespace */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 51ed1f94d..32c492003 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -46,6 +46,7 @@ class StatisticsRegistry;
namespace expr {
namespace attr {
+ class AttributeUniqueId;
class AttributeManager;
}/* CVC4::expr::attr namespace */
@@ -859,6 +860,18 @@ public:
*/
static inline TypeNode fromType(Type t);
+ /** Deletes a list of attributes from the NM's AttributeManager.*/
+ void deleteAttributes(const std::vector< const expr::attr::AttributeUniqueId* >& ids);
+
+ /**
+ * This function gives developers a hook into the NodeManager.
+ * This can be changed in node_manager.cpp without recompiling most of cvc4.
+ *
+ * debugHook is a debugging only function, and should not be present in
+ * any published code!
+ */
+ void debugHook(int debugFlag);
+
};/* class NodeManager */
/**
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index e9d14c38e..24132491a 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -264,6 +264,8 @@ public:
: d_nchildren;
}
+ unsigned getRefCount() const { return d_rc; }
+
std::string toString() const;
void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
OutputLanguage = language::output::LANG_AST) const;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback