diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-16 20:24:37 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-16 20:24:37 +0000 |
commit | 9576517676138a8ca2887a967f1b056662ef6754 (patch) | |
tree | f0040a8189d20496dcaa760055b2b818f8a57525 /src/expr/attribute.cpp | |
parent | 12ad4cf2de936acbf8c21117804c69b2deaa7272 (diff) |
* test/unit/Makefile.am, test/unit/expr/attribute_white.h,
test/unit/expr/node_white.h: add whitebox attribute test (pulled out
attribute stuff from node_white)
* test/unit/parser/parser_black.h: fix memory leaks uncovered by
valgrind
* src/theory/interrupted.h: actually make this "lightweight" (not
derived from CVC4::Exception), as promised in my last commit
* src/theory/uf/theory_uf.h, test/unit/expr/attribute_black.h: match
the new-style cleanup function definition
* src/expr/attribute.cpp, src/expr/attribute.h: support for attribute
deletion, custom cleanup functions, clearer cleanup function
definition.
* src/expr/node_manager.h, src/expr/node_manager.cpp: reclaim
remaining zombies in dtor, rename NodeValueSet ==> "NodeValuePool",
and enable freeing of NodeValues
* src/expr/type.h, src/expr/type.cpp: reference-counting for types,
customized cleanup function for types, also code cleanup
* (various): changed "const Type*" to "Type*" (to enable
reference-counting etc. Types are still immutable.)
* src/util/output.h: add ::isOn()-- which queries whether a
Debug/Trace flag is currently on or not.
* src/smt/smt_engine.cpp, src/parser/antlr_parser.cpp,
src/expr/type.cpp, src/expr/expr_manager.cpp, various others:
minor code cleanup
Diffstat (limited to 'src/expr/attribute.cpp')
-rw-r--r-- | src/expr/attribute.cpp | 43 |
1 files changed, 31 insertions, 12 deletions
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index e8e93f6ff..be54a973e 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -17,24 +17,43 @@ #include "expr/node_value.h" #include "util/output.h" +#include <utility> + +using namespace std; + namespace CVC4 { namespace expr { namespace attr { +/** + * Search for the NodeValue in all attribute tables and remove it, + * calling the cleanup function if one is defined. + */ +template <class T> +inline void AttributeManager::deleteFromTable(AttrHash<T>& table, + NodeValue* nv) { + for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::s_id; ++id) { + typedef AttributeTraits<T, false> traits_t; + typedef AttrHash<T> hash_t; + pair<uint64_t, NodeValue*> pr = std::make_pair(id, nv); + if(traits_t::cleanup[id] != NULL) { + typename hash_t::iterator i = table.find(pr); + if(i != table.end()) { + traits_t::cleanup[id]((*i).second); + table.erase(pr); + } + } else { + table.erase(pr); + } + } +} + void AttributeManager::deleteAllAttributes(NodeValue* nv) { d_bools.erase(nv); - for(unsigned id = 0; id < attr::LastAttributeId<uint64_t, false>::s_id; ++id) { - d_ints.erase(std::make_pair(id, nv)); - } - for(unsigned id = 0; id < attr::LastAttributeId<TNode, false>::s_id; ++id) { - d_exprs.erase(std::make_pair(id, nv)); - } - for(unsigned id = 0; id < attr::LastAttributeId<std::string, false>::s_id; ++id) { - d_strings.erase(std::make_pair(id, nv)); - } - for(unsigned id = 0; id < attr::LastAttributeId<void*, false>::s_id; ++id) { - d_ptrs.erase(std::make_pair(id, nv)); - } + deleteFromTable(d_ints, nv); + deleteFromTable(d_exprs, nv); + deleteFromTable(d_strings, nv); + deleteFromTable(d_ptrs, nv); // FIXME CD-bools in optimized table /* |