diff options
Diffstat (limited to 'src/expr/attribute.cpp')
-rw-r--r-- | src/expr/attribute.cpp | 37 |
1 files changed, 24 insertions, 13 deletions
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index 2cd884bba..63ea770ca 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -17,6 +17,7 @@ #include "expr/attribute.h" #include "expr/node_value.h" #include "util/output.h" +#include "smt/smt_engine.h" #include <utility> @@ -26,13 +27,16 @@ namespace CVC4 { namespace expr { namespace attr { -AttributeManager::AttributeManager(context::Context* ctxt) : +SmtAttributes::SmtAttributes(context::Context* ctxt) : d_cdbools(ctxt), d_cdints(ctxt), d_cdtnodes(ctxt), d_cdnodes(ctxt), d_cdstrings(ctxt), - d_cdptrs(ctxt), + d_cdptrs(ctxt) { +} + +AttributeManager::AttributeManager() : d_inGarbageCollection(false) {} @@ -40,6 +44,15 @@ bool AttributeManager::inGarbageCollection() const { return d_inGarbageCollection; } +SmtAttributes& AttributeManager::getSmtAttributes(SmtEngine* smt) { + Assert(smt != NULL); + return *smt->d_smtAttributes; +} + +const SmtAttributes& AttributeManager::getSmtAttributes(SmtEngine* smt) const { + return *smt->d_smtAttributes; +} + 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 @@ -57,6 +70,10 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) { deleteFromTable(d_types, nv); deleteFromTable(d_strings, nv); deleteFromTable(d_ptrs, nv); +} + +void SmtAttributes::deleteAllAttributes(TNode n) { + NodeValue* nv = n.d_nv; d_cdbools.erase(nv); deleteFromTable(d_cdints, nv); @@ -74,32 +91,25 @@ void AttributeManager::deleteAllAttributes() { deleteAllFromTable(d_types); deleteAllFromTable(d_strings); deleteAllFromTable(d_ptrs); - - d_cdbools.clear(); - d_cdints.clear(); - d_cdtnodes.clear(); - d_cdnodes.clear(); - d_cdstrings.clear(); - d_cdptrs.clear(); } -void AttributeManager::deleteAttributes(const AttrIdVec& atids){ +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){ + 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){ + 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){ + switch(tableId) { case AttrTableBool: Unimplemented("delete attributes is unimplemented for bools"); break; @@ -130,6 +140,7 @@ void AttributeManager::deleteAttributes(const AttrIdVec& atids){ case AttrTableCDPointer: Unimplemented("CDAttributes cannot be deleted. Contact Tim/Morgan if this behavior is desired."); break; + case LastAttrTable: default: Unreachable(); |