From 42c58baf0a2a96c1f3bd797d64834d02adfb9a59 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sun, 4 Apr 2010 19:55:47 +0000 Subject: * Node::isAtomic() now looks at an "atomic" attribute of arguments instead of assuming it's atomic based on kind. Atomicity is determined at node building time. Fixes bug #81. If this is determined to make node building too slow, we can allocate another attribute "AtomicHasBeenComputed" to lazily compute atomicity. * TheoryImpl<> has gone away. Theory implementations now derive from Theory directly and share a single RegisteredAttr attribute for term registration (which shouldn't overlap: every term is "owned" by exactly one Theory). Fixes bug #79. * Additional atomicity tests in ExprBlack unit test. * More appropriate whitebox testing for attribute ID assignment (AttributeWhite unit test). * Better (and more correct) assertion checking in NodeBuilderBlack. * run-regression script now checks exit status against what's provided in "% EXIT: " gesture in .cvc input files, and stderr against "% EXPECT-ERROR: ". These can be used to support intended failures. Fixes bug #84. Also add "% EXIT: " gestures to all .cvc regressions in repository. * Solved some "control reaches end of non-void function" warnings in src/parser/bounded_token_buffer.cpp by replacing "AlwaysAssert(false)" with "Unreachable()" (which is known statically to never return normally). * Regression tests now use the cvc4 binary under builds/$(CURRENT_BUILD)/src/main instead of the one in bin/ which may not be properly installed yet at that point of the build. (Partially fixes bug #46.) * -fvisibility=hidden is now included by configure.ac instead of each Makefile.am, which will make it easier to support platforms (e.g. cygwin) that do things a different way. * TheoryUF code formatting. (re: my code review bug #64) * CDMap<> is leaking memory again, pending a fix for bug #85 in the context subsystem. (To avoid serious errors, can't free context objects.) * add ContextWhite unit test for bug #85 (though it's currently "defanged," awaiting the bugfix) * Minor documentation, other cleanup. --- src/expr/node_manager.h | 97 ++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 87 insertions(+), 10 deletions(-) (limited to 'src/expr/node_manager.h') diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 99b1471f9..71242f2e1 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -35,18 +35,15 @@ namespace CVC4 { -class Type; - namespace expr { -namespace attr { - -struct VarName {}; -struct Type {}; +// Definition of an attribute for the variable name. +// TODO: hide this attribute behind a NodeManager interface. +namespace attr { + struct VarNameTag {}; }/* CVC4::expr::attr namespace */ -typedef Attribute VarNameAttr; -typedef ManagedAttribute TypeAttr; +typedef expr::Attribute VarNameAttr; }/* CVC4::expr namespace */ @@ -125,6 +122,44 @@ class NodeManager { expr::NodeValue* child[N]; };/* struct NodeManager::NVStorage */ + // attribute tags + struct TypeTag {}; + struct AtomicTag {}; + + // NodeManager's attributes. These aren't exposed outside of this + // class; use the getters. + typedef expr::ManagedAttribute TypeAttr; + typedef expr::Attribute AtomicAttr; + + /** + * Returns true if this node is atomic (has no more Boolean + * structure). This is the NodeValue version for NodeManager's + * internal use. There's a public version of this function below + * that takes a TNode. + * @param nv the node to check for atomicity + * @return true if atomic + */ + inline bool isAtomic(expr::NodeValue* nv) const { + // The kindCanBeAtomic() and metakind checking are just optimizations + // (to avoid the hashtable lookup). We assume that all nodes have + // the atomic attribute pre-computed and set at their time of + // creation. This is because: + // (1) it's super cheap to do it bottom-up. + // (2) if we computed it lazily, we'd need a second attribute to + // tell us whether we had computed it yet or not. + // The pre-computation and registration occurs in poolInsert(). + AssertArgument(nv->getMetaKind() != kind::metakind::INVALID, *nv, + "NodeManager::isAtomic() called on INVALID node (%s)", + kind::kindToString(nv->getKind()).c_str()); + return + nv->getMetaKind() == kind::metakind::VARIABLE || + nv->getMetaKind() == kind::metakind::CONSTANT || + ( kind::kindCanBeAtomic(nv->getKind()) && + getAttribute(nv, AtomicAttr()) ); + } + public: NodeManager(context::Context* ctxt); @@ -324,6 +359,15 @@ public: * TODO: Does this call compute the type if it's not already available? */ inline Type* getType(TNode n) const; + + /** + * Returns true if this node is atomic (has no more Boolean structure) + * @param n the node to check for atomicity + * @return true if atomic + */ + inline bool isAtomic(TNode n) const { + return isAtomic(n.d_nv); + } }; /** @@ -476,7 +520,7 @@ inline Type* NodeManager::mkSort(const std::string& name) const { } inline Type* NodeManager::getType(TNode n) const { - return getAttribute(n, CVC4::expr::TypeAttr()); + return getAttribute(n, TypeAttr()); } inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const { @@ -492,6 +536,39 @@ inline void NodeManager::poolInsert(expr::NodeValue* nv) { Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(), "NodeValue already in the pool!"); d_nodeValuePool.insert(nv);// FIXME multithreading + + switch(nv->getMetaKind()) { + case kind::metakind::INVALID: + case kind::metakind::VARIABLE: + case kind::metakind::CONSTANT: + // nothing to do (don't bother setting the attribute, isAtomic() + // on VARIABLEs and CONSTANTs is always true) + break; + + case kind::metakind::OPERATOR: + case kind::metakind::PARAMETERIZED: + { + // register this NodeValue as atomic or not; use nv_begin/end + // because we need to consider the operator too in the case of + // PARAMETERIZED-metakinded nodes (i.e. APPLYs); they could have a + // buried ITE. + + // assume it's atomic if its kind can be atomic, check children + // to see if that is actually true + bool atomic = kind::kindCanBeAtomic(nv->getKind()); + if(atomic) { + for(expr::NodeValue::nv_iterator i = nv->nv_begin(); + i != nv->nv_end(); + ++i) { + if(!(atomic = isAtomic(*i))) { + break; + } + } + } + + setAttribute(nv, AtomicAttr(), atomic); + } + } } inline void NodeManager::poolRemove(expr::NodeValue* nv) { @@ -569,7 +646,7 @@ inline Node NodeManager::mkVar(Type* type, const std::string& name) { inline Node NodeManager::mkVar(Type* type) { Node n = mkVar(); type->inc();// reference-count the type - n.setAttribute(expr::TypeAttr(), type); + n.setAttribute(TypeAttr(), type); return n; } -- cgit v1.2.3