diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-04-06 06:39:01 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-04-06 06:39:01 +0000 |
commit | 4143f662e0c5ef311e98dbd554500b98cd02ecdb (patch) | |
tree | 79abe3f9393d41450ada658dbd3f0914680048c9 /src/expr | |
parent | 6ad21b68e654b940d97caea6d34404d0a6b6e628 (diff) |
* Add some protected ContextObj accessors for ContextObj-derived classes:
+ Context* getContext() -- gets the context
+ ContextMemoryManager* getCMM() -- gets the CMM
+ int getLevel() -- the scope level of the ContextObj's most recent update
+ bool isCurrent() -- true iff the most recent update is the current top level
In particular, the ContextObj::getCMM() call cleans up by TheoryUF's
ECData::addPredecessor() function substantially (re: code review bug #64).
* Fix serious bugs in context operations that corrupted the ContextObj
linked lists. Closes bug #85.
* Identified a bug in the way objects of the "Link" class are
allocated; see bug #96.
* Re-enable context white-box tests that ensure proper links in linked
lists. Closes bug #86.
* Re-enable CDMap<>::emptyTrash(). Closes bug #87.
* Add a tracing option (-t foo or --trace foo) to the driver to enable
Trace("foo") output stream. -d foo implies -t foo.
* Minor clean-up of some TheoryUF code; addition of some documentation
(re: code review bug #64).
* Address some things that caused Doxygen discomfort.
* Address an issue raised in NodeManager's code review (bug #65).
* Remove an inaccurate comment in Attribute code (re: code review bug #61).
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/attribute.cpp | 1 | ||||
-rw-r--r-- | src/expr/attribute.h | 5 | ||||
-rw-r--r-- | src/expr/command.cpp | 8 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 2 | ||||
-rw-r--r-- | src/expr/node_manager.h | 17 |
5 files changed, 12 insertions, 21 deletions
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index 5e8918133..1eeec68af 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -34,7 +34,6 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) { // FIXME CD-bools in optimized table for(unsigned id = 0; id < attr::LastAttributeId<bool, true>::s_id; ++id) { - Debug("gc") << "looking for " << id << " x " << nv << ":" << *nv << std::endl; d_cdbools.obliterate(std::make_pair(id, nv)); } for(unsigned id = 0; id < attr::LastAttributeId<uint64_t, true>::s_id; ++id) { diff --git a/src/expr/attribute.h b/src/expr/attribute.h index c79f4da80..27cddf299 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -112,11 +112,6 @@ public: typename AttrKind::value_type getAttribute(NodeValue* nv, const AttrKind&) const; - // Note that there are two, distinct hasAttribute() declarations for - // a reason (rather than using a default argument): they permit more - // optimized code. The first (without parameter "ret") need never - // check whether its parameter is NULL. - /** * Determine if a particular attribute exists for a particular node. * diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 934c405ad..5fc9dee20 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -42,7 +42,7 @@ void CommandSequence::invoke(SmtEngine* smtEngine) { } } -void CheckSatCommand::toStream(ostream& out) const { +void CheckSatCommand::toStream(std::ostream& out) const { if(d_expr.isNull()) { out << "CheckSat()"; } else { @@ -50,7 +50,7 @@ void CheckSatCommand::toStream(ostream& out) const { } } -void CommandSequence::toStream(ostream& out) const { +void CommandSequence::toStream(std::ostream& out) const { out << "CommandSequence[" << endl; for(unsigned i = d_index; i < d_commandSequence.size(); ++i) { out << *d_commandSequence[i] << endl; @@ -75,7 +75,7 @@ void PushCommand::invoke(SmtEngine* smtEngine) { smtEngine->push(); } -void PushCommand::toStream(ostream& out) const { +void PushCommand::toStream(std::ostream& out) const { out << "Push()"; } @@ -83,7 +83,7 @@ void PopCommand::invoke(SmtEngine* smtEngine) { smtEngine->pop(); } -void PopCommand::toStream(ostream& out) const { +void PopCommand::toStream(std::ostream& out) const { out << "Pop()"; } diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index bb665ef81..a8d957c91 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -132,7 +132,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, child5.getNode()))); } -Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& children) { +Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) { const unsigned n = children.size(); CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, "Exprs with kind %s must have at least %u children and " diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 3f7196178..0f8938397 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -159,19 +159,16 @@ class NodeManager { */ inline void markForDeletion(expr::NodeValue* nv) { Assert(nv->d_rc == 0); + // if d_reclaiming is set, make sure we don't call // reclaimZombies(), because it's already running. - if(d_reclaiming) {// FIXME multithreading - // currently reclaiming zombies; just push onto the list - Debug("gc") << "zombifying node value " << nv - << " [" << nv->d_id << "]: " << *nv - << " [CURRENTLY-RECLAIMING]\n"; - d_zombies.insert(nv);// FIXME multithreading - } else { - Debug("gc") << "zombifying node value " << nv - << " [" << nv->d_id << "]: " << *nv << "\n"; - d_zombies.insert(nv);// FIXME multithreading + Debug("gc") << "zombifying node value " << nv + << " [" << nv->d_id << "]: " << *nv + << (d_reclaiming ? " [CURRENTLY-RECLAIMING]" : "") + << std::endl; + d_zombies.insert(nv);// FIXME multithreading + if(!d_reclaiming) {// FIXME multithreading // for now, collect eagerly. can add heuristic here later.. reclaimZombies(); } |