* A hash function for attribute table keys. Attribute table keys are
* pairs, (unique-attribute-id, Node).
*/
-struct AttrHashFcn {
+struct AttrHashStrategy {
enum { LARGE_PRIME = 32452843ul };
std::size_t operator()(const std::pair<uint64_t, NodeValue*>& p) const {
return p.first * LARGE_PRIME + p.second->getId();
* don't have to store a pair as the key, because we use a known bit
* in [0..63] for each attribute
*/
-struct AttrHashBoolFcn {
+struct AttrHashBoolStrategy {
std::size_t operator()(NodeValue* nv) const {
return (size_t)nv->getId();
}
struct AttrHash :
public __gnu_cxx::hash_map<std::pair<uint64_t, NodeValue*>,
value_type,
- AttrHashFcn> {
+ AttrHashStrategy> {
};
/**
class AttrHash<bool> :
protected __gnu_cxx::hash_map<NodeValue*,
uint64_t,
- AttrHashBoolFcn> {
+ AttrHashBoolStrategy> {
/** A "super" type, like in Java, for easy reference below. */
- typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrHashBoolFcn> super;
+ typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrHashBoolStrategy> super;
/**
* BitAccessor allows us to return a bit "by reference." Of course,
class CDAttrHash :
public CVC4::context::CDMap<std::pair<uint64_t, NodeValue*>,
value_type,
- AttrHashFcn> {
+ AttrHashStrategy> {
public:
CDAttrHash(context::Context* ctxt) :
context::CDMap<std::pair<uint64_t, NodeValue*>,
value_type,
- AttrHashFcn>(ctxt) {
+ AttrHashStrategy>(ctxt) {
}
};
namespace attr {
/** Default cleanup for unmanaged Attribute<> */
-struct NullCleanupFcn {
-};/* struct NullCleanupFcn */
+struct NullCleanupStrategy {
+};/* struct NullCleanupStrategy */
/** Default cleanup for ManagedAttribute<> */
template <class T>
-struct ManagedAttributeCleanupFcn {
-};/* struct ManagedAttributeCleanupFcn<> */
+struct ManagedAttributeCleanupStrategy {
+};/* struct ManagedAttributeCleanupStrategy<> */
/** Specialization for T* */
template <class T>
-struct ManagedAttributeCleanupFcn<T*> {
+struct ManagedAttributeCleanupStrategy<T*> {
static inline void cleanup(T* p) { delete p; }
-};/* struct ManagedAttributeCleanupFcn<T*> */
+};/* struct ManagedAttributeCleanupStrategy<T*> */
/** Specialization for const T* */
template <class T>
-struct ManagedAttributeCleanupFcn<const T*> {
+struct ManagedAttributeCleanupStrategy<const T*> {
static inline void cleanup(const T* p) { delete p; }
-};/* struct ManagedAttributeCleanupFcn<const T*> */
+};/* struct ManagedAttributeCleanupStrategy<const T*> */
/**
* Helper for Attribute<> class below to determine whether a cleanup
* is defined or not.
*/
template <class T, class C>
-struct getCleanupFcn {
+struct getCleanupStrategy {
typedef T value_type;
typedef KindValueToTableValueMapping<value_type> mapping;
static void fn(typename mapping::table_value_type t) {
C::cleanup(mapping::convertBack(t));
}
-};/* struct getCleanupFcn<> */
+};/* struct getCleanupStrategy<> */
/**
- * Specialization for NullCleanupFcn.
+ * Specialization for NullCleanupStrategy.
*/
template <class T>
-struct getCleanupFcn<T, NullCleanupFcn> {
+struct getCleanupStrategy<T, NullCleanupStrategy> {
typedef T value_type;
typedef KindValueToTableValueMapping<value_type> mapping;
static void (*const fn)(typename mapping::table_value_type);
-};/* struct getCleanupFcn<T, NullCleanupFcn> */
+};/* struct getCleanupStrategy<T, NullCleanupStrategy> */
// out-of-class initialization required (because it's a non-integral type)
template <class T>
-void (*const getCleanupFcn<T, NullCleanupFcn>::fn)(typename getCleanupFcn<T, NullCleanupFcn>::mapping::table_value_type) = NULL;
+void (*const getCleanupStrategy<T, NullCleanupStrategy>::fn)(typename getCleanupStrategy<T, NullCleanupStrategy>::mapping::table_value_type) = NULL;
/**
- * Specialization for ManagedAttributeCleanupFcn<T>.
+ * Specialization for ManagedAttributeCleanupStrategy<T>.
*/
template <class T>
-struct getCleanupFcn<T, ManagedAttributeCleanupFcn<T> > {
+struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> > {
typedef T value_type;
typedef KindValueToTableValueMapping<value_type> mapping;
static void (*const fn)(typename mapping::table_value_type);
-};/* struct getCleanupFcn<T, ManagedAttributeCleanupFcn<T> > */
+};/* struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> > */
// out-of-class initialization required (because it's a non-integral type)
template <class T>
-void (*const getCleanupFcn<T, ManagedAttributeCleanupFcn<T> >::fn)(typename getCleanupFcn<T, ManagedAttributeCleanupFcn<T> >::mapping::table_value_type) = NULL;
+void (*const getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> >::fn)(typename getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> >::mapping::table_value_type) = NULL;
/**
- * Specialization for ManagedAttributeCleanupFcn<T*>.
+ * Specialization for ManagedAttributeCleanupStrategy<T*>.
*/
template <class T>
-struct getCleanupFcn<T*, ManagedAttributeCleanupFcn<T*> > {
+struct getCleanupStrategy<T*, ManagedAttributeCleanupStrategy<T*> > {
typedef T* value_type;
- typedef ManagedAttributeCleanupFcn<value_type> C;
+ typedef ManagedAttributeCleanupStrategy<value_type> C;
typedef KindValueToTableValueMapping<value_type> mapping;
static void fn(typename mapping::table_value_type t) {
C::cleanup(mapping::convertBack(t));
}
-};/* struct getCleanupFcn<T*, ManagedAttributeCleanupFcn<T*> > */
+};/* struct getCleanupStrategy<T*, ManagedAttributeCleanupStrategy<T*> > */
/**
- * Specialization for ManagedAttributeCleanupFcn<const T*>.
+ * Specialization for ManagedAttributeCleanupStrategy<const T*>.
*/
template <class T>
-struct getCleanupFcn<const T*, ManagedAttributeCleanupFcn<const T*> > {
+struct getCleanupStrategy<const T*, ManagedAttributeCleanupStrategy<const T*> > {
typedef const T* value_type;
- typedef ManagedAttributeCleanupFcn<value_type> C;
+ typedef ManagedAttributeCleanupStrategy<value_type> C;
typedef KindValueToTableValueMapping<value_type> mapping;
static void fn(typename mapping::table_value_type t) {
C::cleanup(mapping::convertBack(t));
}
-};/* struct getCleanupFcn<const T*, ManagedAttributeCleanupFcn<const T*> > */
+};/* struct getCleanupStrategy<const T*, ManagedAttributeCleanupStrategy<const T*> > */
/**
* Cause compile-time error for improperly-instantiated
- * getCleanupFcn<>.
+ * getCleanupStrategy<>.
*/
template <class T, class U>
-struct getCleanupFcn<T, ManagedAttributeCleanupFcn<U> >;
+struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<U> >;
}/* CVC4::expr::attr namespace */
*
* @param value_t the underlying value_type for the attribute kind
*
- * @param CleanupFcn Clean-up routine for associated values when the
+ * @param CleanupStrategy Clean-up routine for associated values when the
* Node goes away. Useful, e.g., for pointer-valued attributes when
* the values are "owned" by the table.
*
*/
template <class T,
class value_t,
- class CleanupFcn = attr::NullCleanupFcn,
+ class CleanupStrategy = attr::NullCleanupStrategy,
bool context_dep = false>
class Attribute {
/**
typedef attr::AttributeTraits<table_value_type, context_dep> traits;
uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::s_id++;
Assert(traits::cleanup.size() == id);// sanity check
- traits::cleanup.push_back(attr::getCleanupFcn<value_t, CleanupFcn>::fn);
+ traits::cleanup.push_back(attr::getCleanupStrategy<value_t, CleanupStrategy>::fn);
return id;
}
};/* class Attribute<> */
* flag attributes with a specialized cleanup function.
*/
/* -- doesn't work; other specialization is "more specific" ??
-template <class T, class CleanupFcn, bool context_dep>
-class Attribute<T, bool, CleanupFcn, context_dep> {
+template <class T, class CleanupStrategy, bool context_dep>
+class Attribute<T, bool, CleanupStrategy, context_dep> {
template <bool> struct ERROR_bool_attributes_cannot_have_cleanup_functions;
ERROR_bool_attributes_cannot_have_cleanup_functions<true> blah;
};
* An "attribute type" structure for boolean flags (special).
*/
template <class T, bool context_dep>
-class Attribute<T, bool, attr::NullCleanupFcn, context_dep> {
+class Attribute<T, bool, attr::NullCleanupStrategy, context_dep> {
/** IDs for bool-valued attributes are actually bit assignments. */
static const uint64_t s_id;
template <class T,
class value_type>
struct CDAttribute :
- public Attribute<T, value_type, attr::NullCleanupFcn, true> {};
+ public Attribute<T, value_type, attr::NullCleanupStrategy, true> {};
/**
* This is a managed attribute kind (the only difference between
*/
template <class T,
class value_type,
- class CleanupFcn = attr::ManagedAttributeCleanupFcn<value_type> >
+ class CleanupStrategy = attr::ManagedAttributeCleanupStrategy<value_type> >
struct ManagedAttribute :
- public Attribute<T, value_type, CleanupFcn, false> {};
+ public Attribute<T, value_type, CleanupStrategy, false> {};
// ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
// "cleanup" vector before registerAttribute() is called. This is
// important because otherwise the vector is initialized later,
// clearing the first-pushed cleanup function.
-template <class T, class value_t, class CleanupFcn, bool context_dep>
-const uint64_t Attribute<T, value_t, CleanupFcn, context_dep>::s_id =
+template <class T, class value_t, class CleanupStrategy, bool context_dep>
+const uint64_t Attribute<T, value_t, CleanupStrategy, context_dep>::s_id =
( attr::AttributeTraits<typename attr::KindValueToTableValueMapping<value_t>::table_value_type, context_dep>::cleanup.size(),
- Attribute<T, value_t, CleanupFcn, context_dep>::registerAttribute() );
+ Attribute<T, value_t, CleanupStrategy, context_dep>::registerAttribute() );
/** Assign unique IDs to attributes at load time. */
template <class T, bool context_dep>
-const uint64_t Attribute<T, bool, attr::NullCleanupFcn, context_dep>::s_id =
- Attribute<T, bool, attr::NullCleanupFcn, context_dep>::registerAttribute();
+const uint64_t Attribute<T, bool, attr::NullCleanupStrategy, context_dep>::s_id =
+ Attribute<T, bool, attr::NullCleanupStrategy, context_dep>::registerAttribute();
// ATTRIBUTE MANAGER ===========================================================
* @return true if the given node has the given attribute
*/
template <class AttrKind>
- bool hasAttribute(NodeValue* nv,
+ bool getAttribute(NodeValue* nv,
const AttrKind&,
typename AttrKind::value_type& ret) const;
* This implementation returns the AttrKind's default value if the
* Node doesn't have the given attribute.
*/
- static inline bool hasAttribute(const AttributeManager* am,
+ static inline bool getAttribute(const AttributeManager* am,
NodeValue* nv,
typename AttrKind::value_type& ret) {
typedef typename AttrKind::value_type value_type;
return true;
}
- static inline bool hasAttribute(const AttributeManager* am,
+ static inline bool getAttribute(const AttributeManager* am,
NodeValue* nv,
typename AttrKind::value_type& ret) {
typedef typename AttrKind::value_type value_type;
}
template <class AttrKind>
-bool AttributeManager::hasAttribute(NodeValue* nv,
+bool AttributeManager::getAttribute(NodeValue* nv,
const AttrKind&,
typename AttrKind::value_type& ret) const {
- return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, nv, ret);
+ return HasAttribute<AttrKind::has_default_value, AttrKind>::getAttribute(this, nv, ret);
}
template <class AttrKind>
* @return true if this node has the requested attribute
*/
template <class AttrKind>
- inline bool hasAttribute(const AttrKind& attKind,
+ inline bool getAttribute(const AttrKind& attKind,
typename AttrKind::value_type& value) const;
/**
namespace CVC4 {
// for hash_maps, hash_sets..
-struct NodeHashFcn {
+struct NodeHashFunction {
size_t operator()(const CVC4::Node& node) const {
return (size_t) node.getId();
}
template <bool ref_count>
template <class AttrKind>
-inline bool NodeTemplate<ref_count>::hasAttribute(const AttrKind&,
+inline bool NodeTemplate<ref_count>::getAttribute(const AttrKind&,
typename AttrKind::value_type& ret) const {
Assert( NodeManager::currentNM() != NULL,
"There is no current CVC4::NodeManager associated to this thread.\n"
"Perhaps a public-facing function is missing a NodeManagerScope ?" );
- return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret);
+ return NodeManager::currentNM()->getAttribute(*this, AttrKind(), ret);
}
template <bool ref_count>
}/* CVC4::expr::attr namespace */
typedef Attribute<attr::VarName, std::string> VarNameAttr;
-typedef ManagedAttribute<attr::Type, CVC4::Type*, attr::TypeCleanupFcn> TypeAttr;
+typedef ManagedAttribute<attr::Type, CVC4::Type*, attr::TypeCleanupStrategy> TypeAttr;
}/* CVC4::expr namespace */
class NodeManager {
- static __thread NodeManager* s_current;
-
template <class Builder> friend class CVC4::NodeBuilderBase;
+ friend class NodeManagerScope;
+ friend class expr::NodeValue;
typedef __gnu_cxx::hash_set<expr::NodeValue*,
- expr::NodeValueInternalHashFcn,
+ expr::NodeValueInternalHashFunction,
expr::NodeValue::NodeValueEq> NodeValuePool;
typedef __gnu_cxx::hash_set<expr::NodeValue*,
- expr::NodeValueIDHashFcn,
+ expr::NodeValueIDHashFunction,
expr::NodeValue::NodeValueEq> ZombieSet;
+ static __thread NodeManager* s_current;
+
NodeValuePool d_nodeValuePool;
expr::attr::AttributeManager d_attrManager;
+ expr::NodeValue* d_underTheShotgun;
+
+ bool d_reclaiming;
+ ZombieSet d_zombies;
expr::NodeValue* poolLookup(expr::NodeValue* nv) const;
void poolInsert(expr::NodeValue* nv);
void poolRemove(expr::NodeValue* nv);
- friend class NodeManagerScope;
- friend class expr::NodeValue;
-
bool isCurrentlyDeleting(const expr::NodeValue *nv) const{
return d_underTheShotgun == nv;
}
- expr::NodeValue* d_underTheShotgun;
-
- bool d_reclaiming;
- ZombieSet d_zombies;
-
/**
* Register a NodeValue as a zombie.
*/
d_underTheShotgun(NULL),
d_reclaiming(false)
- {
+ { // static initialization
poolInsert( &expr::NodeValue::s_null );
}
~NodeManager();
+ /** The node manager in the current context. */
static NodeManager* currentNM() { return s_current; }
// general expression-builders
+ /** Create a node with no children. */
Node mkNode(Kind kind);
+
+ /** Create a node with one child. */
Node mkNode(Kind kind, TNode child1);
+
+ /** Create a node with two children. */
Node mkNode(Kind kind, TNode child1, TNode child2);
+
+ /** Create a node with three children. */
Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3);
+
+ /** Create a node with four children. */
Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4);
+
+ /** Create a node with five children. */
Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5);
- // N-ary version
+
+ /** Create a node with an arbitrary number of children. */
Node mkNode(Kind kind, const std::vector<Node>& children);
- // variables are special, because duplicates are permitted
+ // NOTE: variables are special, because duplicates are permitted
+
+ /** Create a variable with the given type and name. */
Node mkVar(Type* type, const std::string& name);
+
+ /** Create a variable with the given type. */
Node mkVar(Type* type);
+
+ /** Create a variable of unknown type (?). */
Node mkVar();
+ /** Retrieve an attribute for a node.
+ *
+ * @param nv the node value
+ * @param attr an instance of the attribute kind to retrieve.
+ * @returns the attribute, if set, or a default-constructed
+ * <code>AttrKind::value_type</code> if not.
+ */
template <class AttrKind>
inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv,
- const AttrKind&) const;
-
- // Note that there are two, distinct hasAttribute() declarations for
- // a reason (rather than using a pointer-valued argument with a
- // default value): they permit more optimized code in the underlying
- // hasAttribute() implementations.
-
+ const AttrKind& attr) const;
+
+ /* NOTE: there are two, distinct hasAttribute() declarations for
+ a reason (rather than using a pointer-valued argument with a
+ default value): they permit more optimized code in the underlying
+ hasAttribute() implementations. */
+
+ /** Check whether an attribute is set for a node.
+ *
+ * @param nv the node value
+ * @param attr an instance of the attribute kind to check
+ * @returns <code>true</code> iff <code>attr</code> is set for <code>nv</code>.
+ */
template <class AttrKind>
inline bool hasAttribute(expr::NodeValue* nv,
- const AttrKind&) const;
-
+ const AttrKind& attr) const;
+
+ /** Check whether an attribute is set for a node.
+ *
+ * @param nv the node value
+ * @param attr an instance of the attribute kind to check
+ * @param value a reference to an object of the attribute's value type.
+ * <code>value</code> will be set to the value of the attribute, if it is
+ * set for <code>nv</code>; otherwise, it will be set to the default value of
+ * the attribute.
+ * @returns <code>true</code> iff <code>attr</code> is set for <code>nv</code>.
+ */
template <class AttrKind>
- inline bool hasAttribute(expr::NodeValue* nv,
- const AttrKind&,
- typename AttrKind::value_type&) const;
-
+ inline bool getAttribute(expr::NodeValue* nv,
+ const AttrKind& attr,
+ typename AttrKind::value_type& value) const;
+
+ /** Set an attribute for a node.
+ *
+ * @param nv the node value
+ * @param attr an instance of the attribute kind to set
+ * @param value the value of <code>attr</code> for <code>nv</code>
+ */
template <class AttrKind>
inline void setAttribute(expr::NodeValue* nv,
const AttrKind&,
const typename AttrKind::value_type& value);
+ /** Retrieve an attribute for a TNode.
+ *
+ * @param n the node
+ * @param attr an instance of the attribute kind to retrieve.
+ * @returns the attribute, if set, or a default-constructed
+ * <code>AttrKind::value_type</code> if not.
+ */
template <class AttrKind>
inline typename AttrKind::value_type getAttribute(TNode n,
const AttrKind&) const;
- // Note that there are two, distinct hasAttribute() declarations for
- // a reason (rather than using a pointer-valued argument with a
- // default value): they permit more optimized code in the underlying
- // hasAttribute() implementations.
+ /* NOTE: there are two, distinct hasAttribute() declarations for
+ a reason (rather than using a pointer-valued argument with a
+ default value): they permit more optimized code in the underlying
+ hasAttribute() implementations. */
+ /** Check whether an attribute is set for a TNode.
+ *
+ * @param n the node
+ * @param attr an instance of the attribute kind to check
+ * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
+ */
template <class AttrKind>
inline bool hasAttribute(TNode n,
- const AttrKind&) const;
-
+ const AttrKind& attr) const;
+
+ /** Check whether an attribute is set for a TNode.
+ *
+ * @param n the node
+ * @param attr an instance of the attribute kind to check
+ * @param value a reference to an object of the attribute's value type.
+ * <code>value</code> will be set to the value of the attribute, if it is
+ * set for <code>nv</code>; otherwise, it will be set to the default value of
+ * the attribute.
+ * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
+ */
template <class AttrKind>
- inline bool hasAttribute(TNode n,
- const AttrKind&,
- typename AttrKind::value_type&) const;
-
+ inline bool getAttribute(TNode n,
+ const AttrKind& attr,
+ typename AttrKind::value_type& value) const;
+
+ /** Set an attribute for a TNode.
+ *
+ * @param n the node
+ * @param attr an instance of the attribute kind to set
+ * @param value the value of <code>attr</code> for <code>n</code>
+ */
template <class AttrKind>
inline void setAttribute(TNode n,
const AttrKind&,
/** Make a new sort with the given name. */
inline Type* mkSort(const std::string& name) const;
+ /** Get the type for the given node.
+ *
+ * TODO: Does this call compute the type if it's not already available?
+ */
inline Type* getType(TNode n) const;
};
/**
- * Resource-acquisition-is-instantiation C++ idiom: create one of
- * these "scope" objects to temporarily change the thread-specific
- * notion of the "current" NodeManager for Node creation/deletion,
- * etc. On destruction, the previous NodeManager pointer is restored.
- * Therefore such objects should only be created and destroyed in a
- * well-scoped manner (such as on the stack).
+ * This class changes the "current" thread-global
+ * <code>NodeManager</code> when it is created and reinstates the
+ * previous thread-global <code>NodeManager</code> when it is
+ * destroyed, effectively maintaining a set of nested
+ * <code>NodeManager</code> scopes. This is especially useful on
+ * public-interface calls into the CVC4 library, where CVC4's notion
+ * of the "current" <code>NodeManager</code> should be set to match
+ * the calling context. See, for example, the implementations of
+ * public calls in the <code>ExprManager</code> and
+ * <code>SmtEngine</code> classes.
*
- * This is especially useful on public-interface calls into the CVC4
- * library, where CVC4's notion of the "current" NodeManager should be
- * set to match the calling context. See, for example, the
- * implementations of public calls in the ExprManager and SmtEngine
- * classes.
- *
- * You may create a NodeManagerScope with "new" and destroy it with
- * "delete", or place it as a data member of an object that is, but if
- * the scope of these new/delete pairs isn't properly maintained, the
- * incorrect "current" NodeManager pointer may be restored after a
- * delete.
+ * The client must be careful to create and destroy
+ * <code>NodeManagerScope</code> objects in a well-nested manner (such
+ * as on the stack). You may create a <code>NodeManagerScope</code>
+ * with <code>new</code> and destroy it with <code>delete</code>, or
+ * place it as a data member of an object that is, but if the scope of
+ * these <code>new</code>/<code>delete</code> pairs isn't properly
+ * maintained, the incorrect "current" <code>NodeManager</code>
+ * pointer may be restored after a delete.
*/
class NodeManagerScope {
+ /** The old NodeManager, to be restored on destruction. */
NodeManager *d_oldNodeManager;
public:
};
/**
- * A wrapper (essentially) for NodeManagerScope. The current
- * "NodeManager" pointer is set to this Expr's underlying
- * ExpressionManager's NodeManager. When the ExprManagerScope is
- * destroyed, the previous NodeManager is restored.
- *
- * This is especially useful on public-interface calls into the CVC4
- * library, where CVC4's notion of the "current" NodeManager should be
- * set to match the calling context. See, for example, the
- * implementations of public calls in the Expr class.
- *
- * Without this, we'd need Expr to be a friend of ExprManager.
+ * Creates
+ * a <code>NodeManagerScope</code> with the underlying <code>NodeManager</code>
+ * of a given <code>Expr</code> or <code>ExprManager</code>.
+ * The <code>NodeManagerScope</code> is destroyed when the <code>ExprManagerScope</code>
+ * is destroyed. See <code>NodeManagerScope</code> for more information.
*/
+// NOTE: Without this, we'd need Expr to be a friend of ExprManager.
+// [chris 3/25/2010] Why?
class ExprManagerScope {
NodeManagerScope d_nms;
public:
? NodeManager::currentNM()
: e.getExprManager()->getNodeManager()) {
}
+ inline ExprManagerScope(const ExprManager& exprManager) :
+ d_nms(exprManager.getNodeManager()) {
+ }
};
template <class AttrKind>
}
template <class AttrKind>
-inline bool NodeManager::hasAttribute(expr::NodeValue* nv,
+inline bool NodeManager::getAttribute(expr::NodeValue* nv,
const AttrKind&,
typename AttrKind::value_type& ret) const {
- return d_attrManager.hasAttribute(nv, AttrKind(), ret);
+ return d_attrManager.getAttribute(nv, AttrKind(), ret);
}
template <class AttrKind>
}
template <class AttrKind>
-inline bool NodeManager::hasAttribute(TNode n,
+inline bool NodeManager::getAttribute(TNode n,
const AttrKind&,
typename AttrKind::value_type& ret) const {
- return d_attrManager.hasAttribute(n.d_nv, AttrKind(), ret);
+ return d_attrManager.getAttribute(n.d_nv, AttrKind(), ret);
}
template <class AttrKind>
string s;
// conceptually "this" is const, and hasAttribute() doesn't change
// its argument, but it requires a non-const key arg (for now)
- if(NodeManager::currentNM()->hasAttribute(const_cast<NodeValue*>(this),
+ if(NodeManager::currentNM()->getAttribute(const_cast<NodeValue*>(this),
VarNameAttr(), s)) {
out << s;
} else {
* PERFORMING for other uses! NodeValue::internalHash() will lead to
* collisions for all VARIABLEs.
*/
-struct NodeValueInternalHashFcn {
+struct NodeValueInternalHashFunction {
inline size_t operator()(const NodeValue* nv) const {
return (size_t) nv->internalHash();
}
-};/* struct NodeValueHashFcn */
+};/* struct NodeValueInternalHashFunction */
/**
* For hash_maps, hash_sets, etc.
*/
-struct NodeValueIDHashFcn {
+struct NodeValueIDHashFunction {
inline size_t operator()(const NodeValue* nv) const {
return (size_t) nv->getId();
}
namespace expr {
namespace attr {
- struct TypeCleanupFcn;
+ struct TypeCleanupStrategy;
}/* CVC4::expr::attr namespace */
}/* CVC4::expr namespace */
}
friend class ::CVC4::NodeManager;
- friend struct ::CVC4::expr::attr::TypeCleanupFcn;
+ friend struct ::CVC4::expr::attr::TypeCleanupStrategy;
};
/**
namespace expr {
namespace attr {
-struct TypeCleanupFcn {
+struct TypeCleanupStrategy {
static void cleanup(Type* t) {
// reference-count the Type
t->dec();
namespace CVC4 {
namespace parser {
-struct StringHashFcn {
+struct StringHashFunction {
size_t operator()(const std::string& str) const {
return __gnu_cxx::hash<const char*>()(str.c_str());
}
private:
/** The name to expression bindings */
- typedef __gnu_cxx::hash_map<std::string, ObjectType, StringHashFcn>
+ typedef __gnu_cxx::hash_map<std::string, ObjectType, StringHashFunction>
LookupTable;
/** The table iterator */
SatSolver *d_satSolver;
/** Cache of what literal have been registered to a node. */
- typedef __gnu_cxx::hash_map<Node, SatLiteral, NodeHashFcn> TranslationCache;
+ typedef __gnu_cxx::hash_map<Node, SatLiteral, NodeHashFunction> TranslationCache;
TranslationCache d_translationCache;
/** Cache of what nodes have been registered to a literal. */
- typedef __gnu_cxx::hash_map<SatLiteral, Node, SatSolver::SatLiteralHashFcn> NodeCache;
+ typedef __gnu_cxx::hash_map<SatLiteral, Node, SatSolver::SatLiteralHashFunction> NodeCache;
NodeCache d_nodeCache;
protected:
public:
/** Hash function for literals */
- struct SatLiteralHashFcn {
+ struct SatLiteralHashFunction {
inline size_t operator()(const SatLiteral& literal) const;
};
}
inline size_t
-SatSolver::SatLiteralHashFcn::operator()(const SatLiteral& literal) const {
+SatSolver::SatLiteralHashFunction::operator()(const SatLiteral& literal) const {
return (size_t) minisat::toInt(literal);
}
ECData* ecN;
- if(n.hasAttribute(ECAttr(), ecN)){
+ if(n.getAttribute(ECAttr(), ecN)){
/* registerTerm(n) is only called when a node has not been seen in the
* current context. ECAttr() is not a context-dependent attribute.
* When n.hasAttribute(ECAttr(),...) is true on a registerTerm(n) call,
* Cleanup function for ECData. This will be used for called whenever
* a ECAttr is being destructed.
*/
-struct ECCleanupFcn{
+struct ECCleanupStrategy{
static void cleanup(ECData* ec){
Debug("ufgc") << "cleaning up ECData " << ec << "\n";
ec->deleteSelf();
/**
* ECAttr is the attribute that maps a node to an equivalence class.
*/
-typedef expr::Attribute<EquivClass, ECData*, ECCleanupFcn > ECAttr;
+typedef expr::Attribute<EquivClass, ECData*, ECCleanupStrategy > ECAttr;
} /* CVC4::theory::uf namespace */
} /* CVC4::theory namespace */
MyData* data;
MyData* data1;
MyDataAttribute attr;
- TS_ASSERT(!node->hasAttribute(attr, data));
+ TS_ASSERT(!node->getAttribute(attr, data));
node->setAttribute(attr, new MyData());
- TS_ASSERT(node->hasAttribute(attr, data1));
+ TS_ASSERT(node->getAttribute(attr, data1));
TS_ASSERT(MyData::count == 1);
delete node;
}
// test two-arg version of hasAttribute()
bool bb;
Debug("boolattr", "get flag 1 on a (should be F)\n");
- TS_ASSERT(a.hasAttribute(TestFlag1cd(), bb));
+ TS_ASSERT(a.getAttribute(TestFlag1cd(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 1 on b (should be F)\n");
- TS_ASSERT(b.hasAttribute(TestFlag1cd(), bb));
+ TS_ASSERT(b.getAttribute(TestFlag1cd(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 1 on c (should be F)\n");
- TS_ASSERT(c.hasAttribute(TestFlag1cd(), bb));
+ TS_ASSERT(c.getAttribute(TestFlag1cd(), bb));
TS_ASSERT(! bb);
// setting boolean flags
// test two-arg version of hasAttribute()
bool bb;
Debug("boolattr", "get flag 1 on a (should be F)\n");
- TS_ASSERT(a.hasAttribute(TestFlag1(), bb));
+ TS_ASSERT(a.getAttribute(TestFlag1(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 1 on b (should be F)\n");
- TS_ASSERT(b.hasAttribute(TestFlag1(), bb));
+ TS_ASSERT(b.getAttribute(TestFlag1(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 1 on c (should be F)\n");
- TS_ASSERT(c.hasAttribute(TestFlag1(), bb));
+ TS_ASSERT(c.getAttribute(TestFlag1(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 1 on unnamed (should be F)\n");
- TS_ASSERT(unnamed.hasAttribute(TestFlag1(), bb));
+ TS_ASSERT(unnamed.getAttribute(TestFlag1(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 2 on a (should be F)\n");
- TS_ASSERT(a.hasAttribute(TestFlag2(), bb));
+ TS_ASSERT(a.getAttribute(TestFlag2(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 2 on b (should be F)\n");
- TS_ASSERT(b.hasAttribute(TestFlag2(), bb));
+ TS_ASSERT(b.getAttribute(TestFlag2(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 2 on c (should be F)\n");
- TS_ASSERT(c.hasAttribute(TestFlag2(), bb));
+ TS_ASSERT(c.getAttribute(TestFlag2(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 2 on unnamed (should be F)\n");
- TS_ASSERT(unnamed.hasAttribute(TestFlag2(), bb));
+ TS_ASSERT(unnamed.getAttribute(TestFlag2(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 3 on a (should be F)\n");
- TS_ASSERT(a.hasAttribute(TestFlag3(), bb));
+ TS_ASSERT(a.getAttribute(TestFlag3(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 3 on b (should be F)\n");
- TS_ASSERT(b.hasAttribute(TestFlag3(), bb));
+ TS_ASSERT(b.getAttribute(TestFlag3(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 3 on c (should be F)\n");
- TS_ASSERT(c.hasAttribute(TestFlag3(), bb));
+ TS_ASSERT(c.getAttribute(TestFlag3(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 3 on unnamed (should be F)\n");
- TS_ASSERT(unnamed.hasAttribute(TestFlag3(), bb));
+ TS_ASSERT(unnamed.getAttribute(TestFlag3(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 4 on a (should be F)\n");
- TS_ASSERT(a.hasAttribute(TestFlag4(), bb));
+ TS_ASSERT(a.getAttribute(TestFlag4(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 4 on b (should be F)\n");
- TS_ASSERT(b.hasAttribute(TestFlag4(), bb));
+ TS_ASSERT(b.getAttribute(TestFlag4(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 4 on c (should be F)\n");
- TS_ASSERT(c.hasAttribute(TestFlag4(), bb));
+ TS_ASSERT(c.getAttribute(TestFlag4(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 4 on unnamed (should be F)\n");
- TS_ASSERT(unnamed.hasAttribute(TestFlag4(), bb));
+ TS_ASSERT(unnamed.getAttribute(TestFlag4(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 5 on a (should be F)\n");
- TS_ASSERT(a.hasAttribute(TestFlag5(), bb));
+ TS_ASSERT(a.getAttribute(TestFlag5(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 5 on b (should be F)\n");
- TS_ASSERT(b.hasAttribute(TestFlag5(), bb));
+ TS_ASSERT(b.getAttribute(TestFlag5(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 5 on c (should be F)\n");
- TS_ASSERT(c.hasAttribute(TestFlag5(), bb));
+ TS_ASSERT(c.getAttribute(TestFlag5(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 5 on unnamed (should be F)\n");
- TS_ASSERT(unnamed.hasAttribute(TestFlag5(), bb));
+ TS_ASSERT(unnamed.getAttribute(TestFlag5(), bb));
TS_ASSERT(! bb);
// setting boolean flags
projects / cvc5.git / commitdiff