diff options
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/Makefile.am | 2 | ||||
| -rw-r--r-- | src/expr/metakind_template.h | 20 | ||||
| -rwxr-xr-x | src/expr/mkexpr | 17 | ||||
| -rwxr-xr-x | src/expr/mkmetakind | 8 | ||||
| -rw-r--r-- | src/expr/node.h | 4 | ||||
| -rw-r--r-- | src/expr/node_manager.h | 97 |
6 files changed, 125 insertions, 23 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 76f6ef1a4..1f5e403cc 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -1,7 +1,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libexpr.la diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 052458cbe..96152d075 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -113,6 +113,9 @@ enum MetaKind_t { // individual MetaKind constants under kind::metakind:: typedef ::CVC4::kind::metakind::MetaKind_t MetaKind; +/** + * Get the metakind for a particular kind. + */ static inline MetaKind metaKindOf(Kind k) { static const MetaKind metaKinds[] = { metakind::INVALID, /* NULL_EXPR */ @@ -123,15 +126,20 @@ ${metakind_kinds} return metaKinds[k]; }/* metaKindOf(k) */ -static inline bool kindIsAtomic(Kind k) { - static const bool isAtomic[] = { +/** + * Determine if a particular kind can be atomic or not. Some kinds + * are never atomic (OR, NOT, ITE...), some can be atomic depending on + * their children (PLUS might have an ITE under it, for instance). + */ +static inline bool kindCanBeAtomic(Kind k) { + static const bool canBeAtomic[] = { false, /* NULL_EXPR */ -${metakind_isatomic} +${metakind_canbeatomic} false /* LAST_KIND */ - };/* isAtomic[] */ + };/* canBeAtomic[] */ - return isAtomic[k]; -}/* kindIsAtomic(k) */ + return canBeAtomic[k]; +}/* kindCanBeAtomic(k) */ }/* CVC4::kind namespace */ diff --git a/src/expr/mkexpr b/src/expr/mkexpr index 6508f8121..f59388def 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -32,6 +32,23 @@ cat <<EOF ** for the CVC4 project. **/ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ + +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ + +/* Edit the template file instead: */ +/* $1 */ + EOF me=$(basename "$0") diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 3884f636a..b8dbc2dd6 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -200,11 +200,11 @@ function register_metakind { nc=$3 if [ $mk = NONATOMIC_OPERATOR ]; then - metakind_isatomic="${metakind_isatomic} false, /* $k */ + metakind_canbeatomic="${metakind_canbeatomic} false, /* $k */ "; mk=OPERATOR else - metakind_isatomic="${metakind_isatomic} true, /* $k */ + metakind_canbeatomic="${metakind_canbeatomic} true, /* $k */ "; fi @@ -278,7 +278,7 @@ while [ $# -gt 0 ]; do metakind_kinds="${metakind_kinds} /* from $b */ " - metakind_isatomic="${metakind_isatomic} + metakind_canbeatomic="${metakind_canbeatomic} /* from $b */ " source "$kf" @@ -293,7 +293,7 @@ text=$(cat "$template") for var in \ metakind_includes \ metakind_kinds \ - metakind_isatomic \ + metakind_canbeatomic \ metakind_constantMaps \ metakind_compares \ metakind_constHashes \ diff --git a/src/expr/node.h b/src/expr/node.h index 6f6fdfb4d..3a2aca571 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -587,8 +587,8 @@ template <bool ref_count> NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::s_null); template <bool ref_count> -bool NodeTemplate<ref_count>::isAtomic() const { - return kind::kindIsAtomic(getKind()); +inline bool NodeTemplate<ref_count>::isAtomic() const { + return NodeManager::currentNM()->isAtomic(*this); } // FIXME: escape from type system convenient but is there a better 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<attr::VarName, std::string> VarNameAttr; -typedef ManagedAttribute<attr::Type, CVC4::Type*, attr::TypeCleanupStrategy> TypeAttr; +typedef expr::Attribute<attr::VarNameTag, std::string> VarNameAttr; }/* CVC4::expr namespace */ @@ -125,6 +122,44 @@ class NodeManager { expr::NodeValue* child[N]; };/* struct NodeManager::NVStorage<N> */ + // attribute tags + struct TypeTag {}; + struct AtomicTag {}; + + // NodeManager's attributes. These aren't exposed outside of this + // class; use the getters. + typedef expr::ManagedAttribute<TypeTag, + CVC4::Type*, + expr::attr::TypeCleanupStrategy> TypeAttr; + typedef expr::Attribute<AtomicTag, bool> 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; } |