diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-08 23:49:47 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-08 23:49:47 +0000 |
commit | cf4d347cbbbb4c1a1e1db99337cfd2b22b84b756 (patch) | |
tree | ceea43e3d37525038bed10b115c73a8aa08ce68d /src/expr/attribute.cpp | |
parent | de0160112edbed8ce9b62bf87172ae2f0e99a013 (diff) |
This fixes regressions at levels >= 1 which were failing
* implement zombification and garbage collection of NodeValues
(but GC not turned on yet)
* implement removal of key nodes from all attribute tables
* audit NodeBuilder and fix memory leaks and improper reference-count
management. This is in many places a re-write. Clearly documented
invariants on NodeBuilder state. (Closes Bug 38)
* created a "BackedNodeBuilder" that can be used to construct
NodeBuilders with a stack-based backing store for a size that's not
a compile-time constant.
* NodeValues no longer depend on Node for toStream()'ing
* make unit test-building "silent" with --enable-silent-rules
* (Makefile.am, Makefile.builds.in) fix top-level build system so that
"make regressN" works with unbuilt/out-of-date source trees in the
expected way.
* (various) code cleanup, documentation, formatting
Diffstat (limited to 'src/expr/attribute.cpp')
-rw-r--r-- | src/expr/attribute.cpp | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp new file mode 100644 index 000000000..e8e93f6ff --- /dev/null +++ b/src/expr/attribute.cpp @@ -0,0 +1,61 @@ +/********************* */ +/** 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. + ** + ** AttributeManager implementation. + **/ + +#include "expr/attribute.h" +#include "expr/node_value.h" +#include "util/output.h" + +namespace CVC4 { +namespace expr { +namespace attr { + +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)); + } + + // FIXME CD-bools in optimized table + /* + for(unsigned id = 0; id < attr::LastAttributeId<bool, true>::s_id; ++id) { + d_cdbools.erase(std::make_pair(id, nv)); + } + for(unsigned id = 0; id < attr::LastAttributeId<uint64_t, true>::s_id; ++id) { + d_cdints.erase(std::make_pair(id, nv)); + } + for(unsigned id = 0; id < attr::LastAttributeId<TNode, true>::s_id; ++id) { + d_cdexprs.erase(std::make_pair(id, nv)); + } + for(unsigned id = 0; id < attr::LastAttributeId<std::string, true>::s_id; ++id) { + d_cdstrings.erase(std::make_pair(id, nv)); + } + for(unsigned id = 0; id < attr::LastAttributeId<void*, true>::s_id; ++id) { + d_cdptrs.erase(std::make_pair(id, nv)); + } + */ +} + +}/* CVC4::expr::attr namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ |