From: Aina Niemetz Date: Tue, 4 Jan 2022 20:15:53 +0000 (-0800) Subject: Reorder NodeManager class according to code guidelines. (#7873) X-Git-Tag: cvc5-1.0.0~603 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2b78fb1eab7aac831980b9396f924579b65b03b6;p=cvc5.git Reorder NodeManager class according to code guidelines. (#7873) This only moves code, and removes some redundant inline keywords. --- diff --git a/src/expr/node_manager_template.h b/src/expr/node_manager_template.h index 073077344..5e562c18e 100644 --- a/src/expr/node_manager_template.h +++ b/src/expr/node_manager_template.h @@ -66,6 +66,25 @@ class NodeManager friend class NodeBuilder; public: + /** + * Bits for use in mkDatatypeType() flags. + * + * DATATYPE_FLAG_PLACEHOLDER indicates that the type should not be printed + * out as a definition, for example, in models or during dumping. + */ + enum + { + DATATYPE_FLAG_NONE = 0, + DATATYPE_FLAG_PLACEHOLDER = 1 + }; /* enum */ + + /** Bits for use in mkSort() flags. */ + enum + { + SORT_FLAG_NONE = 0, + SORT_FLAG_PLACEHOLDER = 1 + }; /* enum */ + /** * Return true if given kind is n-ary. The test is based on n-ary kinds * having their maximal arity as the maximal possible number of children @@ -85,305 +104,455 @@ class NodeManager return Node(tn.d_nv->getOperator()); } - private: - /** - * Instead of creating an instance using the constructor, - * `NodeManager::currentNM()` should be used to retrieve an instance of - * `NodeManager`. - */ - explicit NodeManager(); - ~NodeManager(); + /** The node manager in the current public-facing cvc5 library context */ + static NodeManager* currentNM(); - /** Predicate for use with STL algorithms */ - struct NodeValueReferenceCountNonZero { - bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; } - }; + /** Get a Kind from an operator expression */ + static Kind operatorToKind(TNode n); - typedef std::unordered_set NodeValuePool; - typedef std::unordered_set NodeValueIDSet; + /** Get corresponding application kind for function + * + * Different functional nodes are applied differently, according to their + * type. For example, uninterpreted functions (of FUNCTION_TYPE) are applied + * via APPLY_UF, while constructors (of CONSTRUCTOR_TYPE) via + * APPLY_CONSTRUCTOR. This method provides the correct application according + * to which functional type fun has. + * + * @param fun The functional node + * @return the correct application kind for fun. If fun's type is not function + * like (see TypeNode::isFunctionLike), then UNDEFINED_KIND is returned. + */ + static Kind getKindForFunction(TNode fun); - /** The skolem manager */ - std::unique_ptr d_skManager; - /** The bound variable manager */ - std::unique_ptr d_bvManager; + /** + * Determine whether Nodes of a particular Kind have operators. + * @returns true if Nodes of Kind k have operators. + */ + static bool hasOperator(Kind k); - NodeValuePool d_nodeValuePool; + /** + * Initialize the node manager by adding a null node to the pool and filling + * the caches for `operatorOf()`. This method must be called before using the + * NodeManager. This method may be called multiple times. Subsequent calls to + * this method have no effect. + */ + void init(); - bool d_initialized; + /** Get this node manager's skolem manager */ + SkolemManager* getSkolemManager() { return d_skManager.get(); } + /** Get this node manager's bound variable manager */ + BoundVarManager* getBoundVarManager() { return d_bvManager.get(); } - size_t next_id; + /** Reclaim zombies while there are more than k nodes in the pool (if + * possible).*/ + void reclaimZombiesUntil(uint32_t k); - expr::attr::AttributeManager* d_attrManager; + /** Reclaims all zombies (if possible).*/ + void reclaimAllZombies(); + + /** Size of the node pool. */ + size_t poolSize() const; /** - * The node value we're currently freeing. This unique node value - * is permitted to have outstanding TNodes to it (in "soft" - * contexts, like as a key in attribute tables), even though - * normally it's an error to have a TNode to a node value with a - * reference count of 0. Being "under deletion" also enables - * assertions that inc() is not called on it. + * This function gives developers a hook into the NodeManager. + * This can be changed in node_manager.cpp without recompiling most of cvc5. + * + * debugHook is a debugging only function, and should not be present in + * any published code! */ - expr::NodeValue* d_nodeUnderDeletion; + void debugHook(int debugFlag); /** - * True iff we are in reclaimZombies(). This avoids unnecessary - * recursion; a NodeValue being deleted might zombify other - * NodeValues, but these shouldn't trigger a (recursive) call to - * reclaimZombies(). + * Return the datatype at the given index owned by this class. Type nodes are + * associated with datatypes through the DatatypeIndexConstant class. The + * argument index is intended to be a value taken from that class. + * + * Type nodes must access their DTypes through a level of indirection to + * prevent cycles in the Node AST (as DTypes themselves contain Nodes), which + * would lead to memory leaks. Thus TypeNode are given a DatatypeIndexConstant + * which is used as an index to retrieve the DType via this call. */ - bool d_inReclaimZombies; + const DType& getDTypeForIndex(size_t index) const; + + /** get the canonical bound variable list for function type tn */ + Node getBoundVarListForFunctionType(TypeNode tn); /** - * The set of zombie nodes. We may want to revisit this design, as - * we might like to delete nodes in least-recently-used order. But - * we also need to avoid processing a zombie twice. + * Get the (singleton) operator of an OPERATOR-kinded kind. The + * returned node n will have kind BUILTIN, and calling + * n.getConst() will yield k. */ - NodeValueIDSet d_zombies; + TNode operatorOf(Kind k); /** - * NodeValues with maxed out reference counts. These live as long as the - * NodeManager. They have a custom deallocation procedure at the very end. + * 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 + * AttrKind::value_type if not. */ - std::vector d_maxedOut; + template + inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv, + const AttrKind& attr) const; /** - * A set of operator singletons (w.r.t. to this NodeManager - * instance) for operators. Conceptually, Nodes with kind, say, - * PLUS, are APPLYs of a PLUS operator to arguments. This array - * holds the set of operators for these things. A PLUS operator is - * a Node with kind "BUILTIN", and if you call - * plusOperator->getConst(), you get kind::PLUS back. + * 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 true iff attr is set for + * nv. */ - Node d_operators[kind::LAST_KIND]; - - /** unique vars per (Kind,Type) */ - std::map< Kind, std::map< TypeNode, Node > > d_unique_vars; - - /** A list of datatypes owned by this node manager */ - std::vector > d_dtypes; + template + inline bool hasAttribute(expr::NodeValue* nv, const AttrKind& attr) const; /** - * A map of tuple and record types to their corresponding datatype. + * Check whether an attribute is set for a node, and, if so, + * retrieve it. + * + * @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. + * value will be set to the value of the attribute, if it is + * set for nv; otherwise, it will be set to the default + * value of the attribute. + * @returns true iff attr is set for + * nv. */ - class TupleTypeCache { - public: - std::map< TypeNode, TupleTypeCache > d_children; - TypeNode d_data; - TypeNode getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index = 0 ); - }; - class RecTypeCache { - public: - std::map< TypeNode, std::map< std::string, RecTypeCache > > d_children; - TypeNode d_data; - TypeNode getRecordType( NodeManager * nm, const Record& rec, unsigned index = 0 ); - }; - TupleTypeCache d_tt_cache; - RecTypeCache d_rt_cache; + template + inline bool getAttribute(expr::NodeValue* nv, + const AttrKind& attr, + typename AttrKind::value_type& value) const; /** - * Keep a count of all abstract values produced by this NodeManager. - * Abstract values have a type attribute, so if multiple SolverEngines - * are attached to this NodeManager, we don't want their abstract - * values to overlap. + * Set an attribute for a node. If the node doesn't have the + * attribute, this function assigns one. If the node has one, this + * overwrites it. + * + * @param nv the node value + * @param attr an instance of the attribute kind to set + * @param value the value of attr for nv */ - unsigned d_abstractValueCount; + template + inline void setAttribute(expr::NodeValue* nv, + const AttrKind& attr, + const typename AttrKind::value_type& value); /** - * Look up a NodeValue in the pool associated to this NodeManager. - * The NodeValue argument need not be a "completely-constructed" - * NodeValue. In particular, "non-inlined" constants are permitted - * (see below). - * - * For non-CONSTANT metakinds, nv's d_kind and d_nchildren should be - * correctly set, and d_children[0..n-1] should be valid (extant) - * NodeValues for lookup. - * - * For CONSTANT metakinds, nv's d_kind should be set correctly. - * Normally a CONSTANT would have d_nchildren == 0 and the constant - * value inlined in the d_children space. However, here we permit - * "non-inlined" NodeValues to avoid unnecessary copying. For - * these, d_nchildren == 1, and d_nchildren is a pointer to the - * constant value. + * Retrieve an attribute for a TNode. * - * The point of this complex design is to permit efficient lookups - * (without fully constructing a NodeValue). In the case that the - * argument is not fully constructed, and this function returns - * NULL, the caller should fully construct an equivalent one before - * calling poolInsert(). NON-FULLY-CONSTRUCTED NODEVALUES are not - * permitted in the pool! + * @param n the node + * @param attr an instance of the attribute kind to retrieve. + * @returns the attribute, if set, or a default-constructed + * AttrKind::value_type if not. */ - inline expr::NodeValue* poolLookup(expr::NodeValue* nv) const; + template + inline typename AttrKind::value_type getAttribute(TNode n, + const AttrKind& attr) const; /** - * Insert a NodeValue into the NodeManager's pool. + * Check whether an attribute is set for a TNode. * - * It is an error to insert a NodeValue already in the pool. - * Enquire first with poolLookup(). + * @param n the node + * @param attr an instance of the attribute kind to check + * @returns true iff attr is set for n. */ - inline void poolInsert(expr::NodeValue* nv); + template + inline bool hasAttribute(TNode n, const AttrKind& attr) const; /** - * Remove a NodeValue from the NodeManager's pool. + * Check whether an attribute is set for a TNode and, if so, retieve + * it. * - * It is an error to request the removal of a NodeValue from the - * pool that is not in the pool. + * @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. + * value will be set to the value of the attribute, if it is + * set for nv; otherwise, it will be set to the default value of + * the attribute. + * @returns true iff attr is set for n. */ - inline void poolRemove(expr::NodeValue* nv); + template + inline bool getAttribute(TNode n, + const AttrKind& attr, + typename AttrKind::value_type& value) const; /** - * Determine if nv is currently being deleted by the NodeManager. + * Set an attribute for a node. If the node doesn't have the + * attribute, this function assigns one. If the node has one, this + * overwrites it. + * + * @param n the node + * @param attr an instance of the attribute kind to set + * @param value the value of attr for n */ - inline bool isCurrentlyDeleting(const expr::NodeValue* nv) const { - return d_nodeUnderDeletion == nv; - } + template + inline void setAttribute(TNode n, + const AttrKind& attr, + const typename AttrKind::value_type& value); /** - * Register a NodeValue as a zombie. + * Retrieve an attribute for a TypeNode. + * + * @param n the type node + * @param attr an instance of the attribute kind to retrieve. + * @returns the attribute, if set, or a default-constructed + * AttrKind::value_type if not. */ - inline void markForDeletion(expr::NodeValue* nv) { - Assert(nv->d_rc == 0); + template + inline typename AttrKind::value_type getAttribute(TypeNode n, + const AttrKind& attr) const; - // if d_reclaiming is set, make sure we don't call - // reclaimZombies(), because it's already running. - if(Debug.isOn("gc")) { - Debug("gc") << "zombifying node value " << nv - << " [" << nv->d_id << "]: "; - nv->printAst(Debug("gc")); - Debug("gc") << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "") - << std::endl; - } + /** + * Check whether an attribute is set for a TypeNode. + * + * @param n the type node + * @param attr an instance of the attribute kind to check + * @returns true iff attr is set for n. + */ + template + inline bool hasAttribute(TypeNode n, const AttrKind& attr) const; - // `d_zombies` uses the node id to hash and compare nodes. If `d_zombies` - // already contains a node value with the same id as `nv`, but the pointers - // are different, then the wrong `NodeManager` was in scope for one of the - // two nodes when it reached refcount zero. - Assert(d_zombies.find(nv) == d_zombies.end() || *d_zombies.find(nv) == nv); + /** + * Check whether an attribute is set for a TypeNode and, if so, retieve + * it. + * + * @param n the type node + * @param attr an instance of the attribute kind to check + * @param value a reference to an object of the attribute's value type. + * value will be set to the value of the attribute, if it is + * set for nv; otherwise, it will be set to the default value of + * the attribute. + * @returns true iff attr is set for n. + */ + template + inline bool getAttribute(TypeNode n, + const AttrKind& attr, + typename AttrKind::value_type& value) const; - d_zombies.insert(nv); + /** + * Set an attribute for a type node. If the node doesn't have the + * attribute, this function assigns one. If the type node has one, + * this overwrites it. + * + * @param n the type node + * @param attr an instance of the attribute kind to set + * @param value the value of attr for n + */ + template + inline void setAttribute(TypeNode n, + const AttrKind& attr, + const typename AttrKind::value_type& value); - if(safeToReclaimZombies()) { - if(d_zombies.size() > 5000) { - reclaimZombies(); - } - } - } + /** Deletes a list of attributes from the NM's AttributeManager.*/ + void deleteAttributes( + const std::vector& ids); /** - * Register a NodeValue as having a maxed out reference count. This NodeValue - * will live as long as its containing NodeManager. + * Get the type for the given node and optionally do type checking. + * + * Initial type computation will be near-constant time if + * type checking is not requested. Results are memoized, so that + * subsequent calls to getType() without type checking will be + * constant time. + * + * Initial type checking is linear in the size of the expression. + * Again, the results are memoized, so that subsequent calls to + * getType(), with or without type checking, will be constant + * time. + * + * NOTE: A TypeCheckingException can be thrown even when type + * checking is not requested. getType() will always return a + * valid and correct type and, thus, an exception will be thrown + * when no valid or correct type can be computed (e.g., if the + * arguments to a bit-vector operation aren't bit-vectors). When + * type checking is not requested, getType() will do the minimum + * amount of checking required to return a valid result. + * + * @param n the Node for which we want a type + * @param check whether we should check the type as we compute it + * (default: false) */ - inline void markRefCountMaxedOut(expr::NodeValue* nv) { - Assert(nv->HasMaximizedReferenceCount()); - if(Debug.isOn("gc")) { - Debug("gc") << "marking node value " << nv - << " [" << nv->d_id << "]: as maxed out" << std::endl; - } - d_maxedOut.push_back(nv); - } + TypeNode getType(TNode n, bool check = false); + + /** Get the (singleton) type for Booleans. */ + TypeNode booleanType(); + + /** Get the (singleton) type for integers. */ + TypeNode integerType(); + + /** Get the (singleton) type for reals. */ + TypeNode realType(); + + /** Get the (singleton) type for strings. */ + TypeNode stringType(); + + /** Get the (singleton) type for RegExp. */ + TypeNode regExpType(); + + /** Get the (singleton) type for rounding modes. */ + TypeNode roundingModeType(); + + /** Get the bound var list type. */ + TypeNode boundVarListType(); + + /** Get the instantiation pattern type. */ + TypeNode instPatternType(); + + /** Get the instantiation pattern type. */ + TypeNode instPatternListType(); /** - * Reclaim all zombies. - */ - void reclaimZombies(); + * Get the (singleton) type for builtin operators (that is, the type + * of the Node returned from Node::getOperator() when the operator + * is built-in, like EQUAL). */ + TypeNode builtinOperatorType(); /** - * It is safe to collect zombies. + * Make a function type from domain to range. + * + * @param domain the domain type + * @param range the range type + * @returns the functional type domain -> range */ - bool safeToReclaimZombies() const; + TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range); /** - * Returns a reverse topological sort of a list of NodeValues. The NodeValues - * must be valid and have ids. The NodeValues are not modified (including ref - * counts). + * Make a function type with input types from + * argTypes. argTypes must have at least one element. + * + * @param argTypes the domain is a tuple (argTypes[0], ..., argTypes[n]) + * @param range the range type + * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range */ - static std::vector TopologicalSort( - const std::vector& roots); + TypeNode mkFunctionType(const std::vector& argTypes, + const TypeNode& range); /** - * This template gives a mechanism to stack-allocate a NodeValue - * with enough space for N children (where N is a compile-time - * constant). You use it like this: - * - * NVStorage<4> nvStorage; - * NodeValue& nvStack = reinterpret_cast(nvStorage); + * Make a function type with input types from + * sorts[0..sorts.size()-2] and result type + * sorts[sorts.size()-1]. sorts must have + * at least 2 elements. * - * ...and then you can use nvStack as a NodeValue that you know has - * room for 4 children. + * @param sorts The argument and range sort of the function type, where the + * range type is the last in this vector. + * @return the function type */ - template - struct NVStorage { - expr::NodeValue nv; - expr::NodeValue* child[N]; - };/* struct NodeManager::NVStorage */ - - // undefined private copy constructor (disallow copy) - NodeManager(const NodeManager&) = delete; + TypeNode mkFunctionType(const std::vector& sorts); - NodeManager& operator=(const NodeManager&) = delete; + /** + * Make a predicate type with input types from + * sorts. The result with be a function type with range + * BOOLEAN. sorts must have at least one + * element. + */ + TypeNode mkPredicateType(const std::vector& sorts); /** - * Create a variable with the given name and type. NOTE that no - * lookup is done on the name. If you mkVar("a", type) and then - * mkVar("a", type) again, you have two variables. The NodeManager - * version of this is private to avoid internal uses of mkVar() from - * within cvc5. Such uses should employ SkolemManager::mkSkolem() instead. + * Make a tuple type with types from + * types. types must have at least one + * element. + * + * @param types a vector of types + * @returns the tuple type (types[0], ..., types[n]) */ - Node mkVar(const std::string& name, const TypeNode& type); + TypeNode mkTupleType(const std::vector& types); - /** Create a variable with the given type. */ - Node mkVar(const TypeNode& type); + /** + * Make a record type with the description from rec. + * + * @param rec a description of the record + * @returns the record type + */ + TypeNode mkRecordType(const Record& rec); - public: /** - * Initialize the node manager by adding a null node to the pool and filling - * the caches for `operatorOf()`. This method must be called before using the - * NodeManager. This method may be called multiple times. Subsequent calls to - * this method have no effect. + * @returns the symbolic expression type */ - void init(); + TypeNode sExprType(); - /** The node manager in the current public-facing cvc5 library context */ - static NodeManager* currentNM(); - /** Get this node manager's skolem manager */ - SkolemManager* getSkolemManager() { return d_skManager.get(); } - /** Get this node manager's bound variable manager */ - BoundVarManager* getBoundVarManager() { return d_bvManager.get(); } + /** Make the type of floating-point with exp bit exponent and + sig bit significand */ + TypeNode mkFloatingPointType(unsigned exp, unsigned sig); + TypeNode mkFloatingPointType(FloatingPointSize fs); + + /** Make the type of bitvectors of size size */ + TypeNode mkBitVectorType(unsigned size); + + /** Make the type of arrays with the given parameterization */ + TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType); + + /** Make the type of set with the given parameterization */ + TypeNode mkSetType(TypeNode elementType); + + /** Make the type of bags with the given parameterization */ + TypeNode mkBagType(TypeNode elementType); + + /** Make the type of sequences with the given parameterization */ + TypeNode mkSequenceType(TypeNode elementType); + + /** Make a type representing the given datatype. */ + TypeNode mkDatatypeType(DType& datatype, uint32_t flags = DATATYPE_FLAG_NONE); /** - * Return the datatype at the given index owned by this class. Type nodes are - * associated with datatypes through the DatatypeIndexConstant class. The - * argument index is intended to be a value taken from that class. - * - * Type nodes must access their DTypes through a level of indirection to - * prevent cycles in the Node AST (as DTypes themselves contain Nodes), which - * would lead to memory leaks. Thus TypeNode are given a DatatypeIndexConstant - * which is used as an index to retrieve the DType via this call. + * Make a set of types representing the given datatypes, which may be + * mutually recursive. */ - const DType& getDTypeForIndex(size_t index) const; - - /** Get a Kind from an operator expression */ - static inline Kind operatorToKind(TNode n); + std::vector mkMutualDatatypeTypes( + const std::vector& datatypes, uint32_t flags = DATATYPE_FLAG_NONE); - /** Get corresponding application kind for function + /** + * Make a set of types representing the given datatypes, which may + * be mutually recursive. unresolvedTypes is a set of SortTypes + * that were used as placeholders in the Datatypes for the Datatypes + * of the same name. This is just a more complicated version of the + * above mkMutualDatatypeTypes() function, but is required to handle + * complex types. * - * Different functional nodes are applied differently, according to their - * type. For example, uninterpreted functions (of FUNCTION_TYPE) are applied - * via APPLY_UF, while constructors (of CONSTRUCTOR_TYPE) via - * APPLY_CONSTRUCTOR. This method provides the correct application according - * to which functional type fun has. + * For example, unresolvedTypes might contain the single sort "list" + * (with that name reported from SortType::getName()). The + * datatypes list might have the single datatype * - * @param fun The functional node - * @return the correct application kind for fun. If fun's type is not function - * like (see TypeNode::isFunctionLike), then UNDEFINED_KIND is returned. + * DATATYPE + * list = cons(car:ARRAY INT OF list, cdr:list) | nil; + * END; + * + * To represent the Type of the array, the user had to create a + * placeholder type (an uninterpreted sort) to stand for "list" in + * the type of "car". It is this placeholder sort that should be + * passed in unresolvedTypes. If the datatype was of the simpler + * form: + * + * DATATYPE + * list = cons(car:list, cdr:list) | nil; + * END; + * + * then no complicated Type needs to be created, and the above, + * simpler form of mkMutualDatatypeTypes() is enough. */ - static Kind getKindForFunction(TNode fun); + std::vector mkMutualDatatypeTypes( + const std::vector& datatypes, + const std::set& unresolvedTypes, + uint32_t flags = DATATYPE_FLAG_NONE); + + /** + * Make a type representing a constructor with the given argument (subfield) + * types and return type range. + */ + TypeNode mkConstructorType(const std::vector& args, TypeNode range); + + /** Make a type representing a selector with the given parameterization */ + TypeNode mkSelectorType(TypeNode domain, TypeNode range); + + /** Make a type representing a tester with given parameterization */ + TypeNode mkTesterType(TypeNode domain); + + /** Make a type representing an updater with the given parameterization */ + TypeNode mkDatatypeUpdateType(TypeNode domain, TypeNode range); + + /* General expression-builders ------------------------------------------ */ - // general expression-builders - // /** Create a node with no child. */ Node mkNode(Kind kind); @@ -478,9 +647,6 @@ class NodeManager */ Node mkGroundValue(const TypeNode& tn); - /** get the canonical bound variable list for function type tn */ - Node getBoundVarListForFunctionType( TypeNode tn ); - /** * Create an Node by applying an associative operator to the children. * If children.size() is greater than the max arity for @@ -490,542 +656,393 @@ class NodeManager * 2, then calling mkAssociative(FOO,a,b,c) will return * (FOO (FOO a b) c) or (FOO a (FOO b c)). * The order of the arguments will be preserved in a left-to-right - * traversal of the resulting tree. - */ - Node mkAssociative(Kind kind, const std::vector& children); - - /** - * Create an Node by applying an binary left-associative operator to the - * children. For example, mkLeftAssociative( f, { a, b, c } ) returns - * f( f( a, b ), c ). - */ - Node mkLeftAssociative(Kind kind, const std::vector& children); - /** - * Create an Node by applying an binary right-associative operator to the - * children. For example, mkRightAssociative( f, { a, b, c } ) returns - * f( a, f( b, c ) ). - */ - Node mkRightAssociative(Kind kind, const std::vector& children); - - /** make chain - * - * Given a kind k and arguments t_1, ..., t_n, this returns the - * conjunction of: - * (k t_1 t_2) .... (k t_{n-1} t_n) - * It is expected that k is a kind denoting a predicate, and args is a list - * of terms of size >= 2 such that the terms above are well-typed. - */ - Node mkChain(Kind kind, const std::vector& children); - - /** Create a instantiation constant with the given type. */ - Node mkInstConstant(const TypeNode& type); - - /** Make a new abstract value with the given type. */ - Node mkAbstractValue(const TypeNode& type); - - /** make unique (per Type,Kind) variable. */ - Node mkNullaryOperator(const TypeNode& type, Kind k); - - /** - * Create a singleton set from the given element n. - * @param t the element type of the returned set. - * Note that the type of n needs to be a subtype of t. - * @param n the single element in the singleton. - * @return a singleton set constructed from the element n. - */ - Node mkSingleton(const TypeNode& t, const TNode n); - - /** - * Create a bag from the given element n along with its multiplicity m. - * @param t the element type of the returned bag. - * Note that the type of n needs to be a subtype of t. - * @param n the element that is used to to construct the bag - * @param m the multiplicity of the element n - * @return a bag that contains m occurrences of n. - */ - Node mkBag(const TypeNode& t, const TNode n, const TNode m); - - /** - * Create a constant of type T. It will have the appropriate - * CONST_* kind defined for T. - */ - template - Node mkConst(const T&); - - /** - * Create a constant of type `T` with an explicit kind `k`. - */ - template - Node mkConst(Kind k, const T&); - - template - TypeNode mkTypeConst(const T&); - - template - NodeClass mkConstInternal(Kind k, const T&); - - /** - * Make constant real. Returns constant of kind CONST_RATIONAL with Rational - * payload. - */ - Node mkConstReal(const Rational& r); - - /** - * Make constant real. Returns constant of kind CONST_INTEGER with Rational - * payload. - * - * !!! Note until subtypes are eliminated, this returns a constant of kind - * CONST_RATIONAL. - */ - Node mkConstInt(const Rational& r); - - /** - * Make constant real or int, which calls one of the above methods based - * on the type tn. - */ - Node mkConstRealOrInt(const TypeNode& tn, const Rational& r); - - /** Create a node with children. */ - TypeNode mkTypeNode(Kind kind, TypeNode child1); - TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2); - TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2, - TypeNode child3); - TypeNode mkTypeNode(Kind kind, const std::vector& children); - - /** - * Determine whether Nodes of a particular Kind have operators. - * @returns true if Nodes of Kind k have operators. - */ - static bool hasOperator(Kind k); - - /** - * Get the (singleton) operator of an OPERATOR-kinded kind. The - * returned node n will have kind BUILTIN, and calling - * n.getConst() will yield k. - */ - TNode operatorOf(Kind k); - - /** - * 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 - * AttrKind::value_type if not. - */ - template - inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv, - 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 - * @returns true iff attr is set for - * nv. - */ - template - inline bool hasAttribute(expr::NodeValue* nv, - const AttrKind& attr) const; - - /** - * Check whether an attribute is set for a node, and, if so, - * retrieve it. - * - * @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. - * value will be set to the value of the attribute, if it is - * set for nv; otherwise, it will be set to the default - * value of the attribute. - * @returns true iff attr is set for - * nv. + * traversal of the resulting tree. */ - template - inline bool getAttribute(expr::NodeValue* nv, - const AttrKind& attr, - typename AttrKind::value_type& value) const; + Node mkAssociative(Kind kind, const std::vector& children); /** - * Set an attribute for a node. If the node doesn't have the - * attribute, this function assigns one. If the node has one, this - * overwrites it. - * - * @param nv the node value - * @param attr an instance of the attribute kind to set - * @param value the value of attr for nv + * Create an Node by applying an binary left-associative operator to the + * children. For example, mkLeftAssociative( f, { a, b, c } ) returns + * f( f( a, b ), c ). */ - template - inline void setAttribute(expr::NodeValue* nv, - const AttrKind& attr, - const typename AttrKind::value_type& value); - + Node mkLeftAssociative(Kind kind, const std::vector& children); /** - * 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 - * AttrKind::value_type if not. + * Create an Node by applying an binary right-associative operator to the + * children. For example, mkRightAssociative( f, { a, b, c } ) returns + * f( a, f( b, c ) ). */ - template - inline typename AttrKind::value_type - getAttribute(TNode n, const AttrKind& attr) const; + Node mkRightAssociative(Kind kind, const std::vector& children); - /** - * Check whether an attribute is set for a TNode. + /** make chain * - * @param n the node - * @param attr an instance of the attribute kind to check - * @returns true iff attr is set for n. + * Given a kind k and arguments t_1, ..., t_n, this returns the + * conjunction of: + * (k t_1 t_2) .... (k t_{n-1} t_n) + * It is expected that k is a kind denoting a predicate, and args is a list + * of terms of size >= 2 such that the terms above are well-typed. */ - template - inline bool hasAttribute(TNode n, - const AttrKind& attr) const; + Node mkChain(Kind kind, const std::vector& children); + + /** Create a instantiation constant with the given type. */ + Node mkInstConstant(const TypeNode& type); + + /** Make a new abstract value with the given type. */ + Node mkAbstractValue(const TypeNode& type); + + /** make unique (per Type,Kind) variable. */ + Node mkNullaryOperator(const TypeNode& type, Kind k); /** - * Check whether an attribute is set for a TNode and, if so, retieve - * it. - * - * @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. - * value will be set to the value of the attribute, if it is - * set for nv; otherwise, it will be set to the default value of - * the attribute. - * @returns true iff attr is set for n. + * Create a singleton set from the given element n. + * @param t the element type of the returned set. + * Note that the type of n needs to be a subtype of t. + * @param n the single element in the singleton. + * @return a singleton set constructed from the element n. */ - template - inline bool getAttribute(TNode n, - const AttrKind& attr, - typename AttrKind::value_type& value) const; + Node mkSingleton(const TypeNode& t, const TNode n); /** - * Set an attribute for a node. If the node doesn't have the - * attribute, this function assigns one. If the node has one, this - * overwrites it. - * - * @param n the node - * @param attr an instance of the attribute kind to set - * @param value the value of attr for n + * Create a bag from the given element n along with its multiplicity m. + * @param t the element type of the returned bag. + * Note that the type of n needs to be a subtype of t. + * @param n the element that is used to to construct the bag + * @param m the multiplicity of the element n + * @return a bag that contains m occurrences of n. */ - template - inline void setAttribute(TNode n, - const AttrKind& attr, - const typename AttrKind::value_type& value); + Node mkBag(const TypeNode& t, const TNode n, const TNode m); /** - * Retrieve an attribute for a TypeNode. - * - * @param n the type node - * @param attr an instance of the attribute kind to retrieve. - * @returns the attribute, if set, or a default-constructed - * AttrKind::value_type if not. + * Create a constant of type T. It will have the appropriate + * CONST_* kind defined for T. */ - template - inline typename AttrKind::value_type - getAttribute(TypeNode n, const AttrKind& attr) const; + template + Node mkConst(const T&); /** - * Check whether an attribute is set for a TypeNode. - * - * @param n the type node - * @param attr an instance of the attribute kind to check - * @returns true iff attr is set for n. + * Create a constant of type `T` with an explicit kind `k`. */ - template - inline bool hasAttribute(TypeNode n, - const AttrKind& attr) const; + template + Node mkConst(Kind k, const T&); + + template + TypeNode mkTypeConst(const T&); + + template + NodeClass mkConstInternal(Kind k, const T&); /** - * Check whether an attribute is set for a TypeNode and, if so, retieve - * it. - * - * @param n the type node - * @param attr an instance of the attribute kind to check - * @param value a reference to an object of the attribute's value type. - * value will be set to the value of the attribute, if it is - * set for nv; otherwise, it will be set to the default value of - * the attribute. - * @returns true iff attr is set for n. + * Make constant real. Returns constant of kind CONST_RATIONAL with Rational + * payload. */ - template - inline bool getAttribute(TypeNode n, - const AttrKind& attr, - typename AttrKind::value_type& value) const; + Node mkConstReal(const Rational& r); /** - * Set an attribute for a type node. If the node doesn't have the - * attribute, this function assigns one. If the type node has one, - * this overwrites it. + * Make constant real. Returns constant of kind CONST_INTEGER with Rational + * payload. * - * @param n the type node - * @param attr an instance of the attribute kind to set - * @param value the value of attr for n + * !!! Note until subtypes are eliminated, this returns a constant of kind + * CONST_RATIONAL. */ - template - inline void setAttribute(TypeNode n, - const AttrKind& attr, - const typename AttrKind::value_type& value); + Node mkConstInt(const Rational& r); - /** Get the (singleton) type for Booleans. */ - TypeNode booleanType(); + /** + * Make constant real or int, which calls one of the above methods based + * on the type tn. + */ + Node mkConstRealOrInt(const TypeNode& tn, const Rational& r); - /** Get the (singleton) type for integers. */ - TypeNode integerType(); + /** Create a node with children. */ + TypeNode mkTypeNode(Kind kind, TypeNode child1); + TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2); + TypeNode mkTypeNode(Kind kind, + TypeNode child1, + TypeNode child2, + TypeNode child3); + TypeNode mkTypeNode(Kind kind, const std::vector& children); - /** Get the (singleton) type for reals. */ - TypeNode realType(); + /** Make a new (anonymous) sort of arity 0. */ + TypeNode mkSort(uint32_t flags = SORT_FLAG_NONE); - /** Get the (singleton) type for strings. */ - TypeNode stringType(); + /** Make a new sort with the given name of arity 0. */ + TypeNode mkSort(const std::string& name, uint32_t flags = SORT_FLAG_NONE); - /** Get the (singleton) type for RegExp. */ - TypeNode regExpType(); + /** Make a new sort by parameterizing the given sort constructor. */ + TypeNode mkSort(TypeNode constructor, + const std::vector& children, + uint32_t flags = SORT_FLAG_NONE); - /** Get the (singleton) type for rounding modes. */ - TypeNode roundingModeType(); + /** Make a new sort with the given name and arity. */ + TypeNode mkSortConstructor(const std::string& name, + size_t arity, + uint32_t flags = SORT_FLAG_NONE); - /** Get the bound var list type. */ - TypeNode boundVarListType(); + private: + typedef std::unordered_set + NodeValuePool; + typedef std::unordered_set + NodeValueIDSet; - /** Get the instantiation pattern type. */ - TypeNode instPatternType(); + /** Predicate for use with STL algorithms */ + struct NodeValueReferenceCountNonZero + { + bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; } + }; - /** Get the instantiation pattern type. */ - TypeNode instPatternListType(); + /** + * This template gives a mechanism to stack-allocate a NodeValue + * with enough space for N children (where N is a compile-time + * constant). You use it like this: + * + * NVStorage<4> nvStorage; + * NodeValue& nvStack = reinterpret_cast(nvStorage); + * + * ...and then you can use nvStack as a NodeValue that you know has + * room for 4 children. + */ + template + struct NVStorage + { + expr::NodeValue nv; + expr::NodeValue* child[N]; + }; /* struct NodeManager::NVStorage */ /** - * Get the (singleton) type for builtin operators (that is, the type - * of the Node returned from Node::getOperator() when the operator - * is built-in, like EQUAL). */ - TypeNode builtinOperatorType(); + * A map of tuple and record types to their corresponding datatype. + */ + class TupleTypeCache + { + public: + std::map d_children; + TypeNode d_data; + TypeNode getTupleType(NodeManager* nm, + std::vector& types, + unsigned index = 0); + }; + class RecTypeCache + { + public: + std::map> d_children; + TypeNode d_data; + TypeNode getRecordType(NodeManager* nm, + const Record& rec, + unsigned index = 0); + }; /** - * Make a function type from domain to range. - * - * @param domain the domain type - * @param range the range type - * @returns the functional type domain -> range + * Returns a reverse topological sort of a list of NodeValues. The NodeValues + * must be valid and have ids. The NodeValues are not modified (including ref + * counts). */ - TypeNode mkFunctionType(const TypeNode& domain, - const TypeNode& range); + static std::vector TopologicalSort( + const std::vector& roots); /** - * Make a function type with input types from - * argTypes. argTypes must have at least one element. - * - * @param argTypes the domain is a tuple (argTypes[0], ..., argTypes[n]) - * @param range the range type - * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range + * Instead of creating an instance using the constructor, + * `NodeManager::currentNM()` should be used to retrieve an instance of + * `NodeManager`. */ - TypeNode mkFunctionType(const std::vector& argTypes, - const TypeNode& range); + explicit NodeManager(); + ~NodeManager(); + // undefined private copy constructor (disallow copy) + NodeManager(const NodeManager&) = delete; + NodeManager& operator=(const NodeManager&) = delete; /** - * Make a function type with input types from - * sorts[0..sorts.size()-2] and result type - * sorts[sorts.size()-1]. sorts must have - * at least 2 elements. + * Look up a NodeValue in the pool associated to this NodeManager. + * The NodeValue argument need not be a "completely-constructed" + * NodeValue. In particular, "non-inlined" constants are permitted + * (see below). + * + * For non-CONSTANT metakinds, nv's d_kind and d_nchildren should be + * correctly set, and d_children[0..n-1] should be valid (extant) + * NodeValues for lookup. + * + * For CONSTANT metakinds, nv's d_kind should be set correctly. + * Normally a CONSTANT would have d_nchildren == 0 and the constant + * value inlined in the d_children space. However, here we permit + * "non-inlined" NodeValues to avoid unnecessary copying. For + * these, d_nchildren == 1, and d_nchildren is a pointer to the + * constant value. * - * @param sorts The argument and range sort of the function type, where the - * range type is the last in this vector. - * @return the function type + * The point of this complex design is to permit efficient lookups + * (without fully constructing a NodeValue). In the case that the + * argument is not fully constructed, and this function returns + * NULL, the caller should fully construct an equivalent one before + * calling poolInsert(). NON-FULLY-CONSTRUCTED NODEVALUES are not + * permitted in the pool! */ - TypeNode mkFunctionType(const std::vector& sorts); + expr::NodeValue* poolLookup(expr::NodeValue* nv) const; /** - * Make a predicate type with input types from - * sorts. The result with be a function type with range - * BOOLEAN. sorts must have at least one - * element. + * Insert a NodeValue into the NodeManager's pool. + * + * It is an error to insert a NodeValue already in the pool. + * Enquire first with poolLookup(). */ - TypeNode mkPredicateType(const std::vector& sorts); + void poolInsert(expr::NodeValue* nv); /** - * Make a tuple type with types from - * types. types must have at least one - * element. + * Remove a NodeValue from the NodeManager's pool. * - * @param types a vector of types - * @returns the tuple type (types[0], ..., types[n]) + * It is an error to request the removal of a NodeValue from the + * pool that is not in the pool. */ - TypeNode mkTupleType(const std::vector& types); + void poolRemove(expr::NodeValue* nv); /** - * Make a record type with the description from rec. - * - * @param rec a description of the record - * @returns the record type + * Determine if nv is currently being deleted by the NodeManager. */ - TypeNode mkRecordType(const Record& rec); + inline bool isCurrentlyDeleting(const expr::NodeValue* nv) const + { + return d_nodeUnderDeletion == nv; + } /** - * @returns the symbolic expression type + * Register a NodeValue as a zombie. */ - TypeNode sExprType(); - - /** Make the type of floating-point with exp bit exponent and - sig bit significand */ - TypeNode mkFloatingPointType(unsigned exp, unsigned sig); - TypeNode mkFloatingPointType(FloatingPointSize fs); - - /** Make the type of bitvectors of size size */ - TypeNode mkBitVectorType(unsigned size); + inline void markForDeletion(expr::NodeValue* nv) + { + Assert(nv->d_rc == 0); - /** Make the type of arrays with the given parameterization */ - inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType); + // if d_reclaiming is set, make sure we don't call + // reclaimZombies(), because it's already running. + if (Debug.isOn("gc")) + { + Debug("gc") << "zombifying node value " << nv << " [" << nv->d_id + << "]: "; + nv->printAst(Debug("gc")); + Debug("gc") << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "") + << std::endl; + } - /** Make the type of set with the given parameterization */ - inline TypeNode mkSetType(TypeNode elementType); + // `d_zombies` uses the node id to hash and compare nodes. If `d_zombies` + // already contains a node value with the same id as `nv`, but the pointers + // are different, then the wrong `NodeManager` was in scope for one of the + // two nodes when it reached refcount zero. + Assert(d_zombies.find(nv) == d_zombies.end() || *d_zombies.find(nv) == nv); - /** Make the type of bags with the given parameterization */ - TypeNode mkBagType(TypeNode elementType); + d_zombies.insert(nv); - /** Make the type of sequences with the given parameterization */ - TypeNode mkSequenceType(TypeNode elementType); + if (safeToReclaimZombies()) + { + if (d_zombies.size() > 5000) + { + reclaimZombies(); + } + } + } - /** Bits for use in mkDatatypeType() flags. - * - * DATATYPE_FLAG_PLACEHOLDER indicates that the type should not be printed - * out as a definition, for example, in models or during dumping. + /** + * Register a NodeValue as having a maxed out reference count. This NodeValue + * will live as long as its containing NodeManager. */ - enum + inline void markRefCountMaxedOut(expr::NodeValue* nv) { - DATATYPE_FLAG_NONE = 0, - DATATYPE_FLAG_PLACEHOLDER = 1 - }; /* enum */ - - /** Make a type representing the given datatype. */ - TypeNode mkDatatypeType(DType& datatype, uint32_t flags = DATATYPE_FLAG_NONE); + Assert(nv->HasMaximizedReferenceCount()); + if (Debug.isOn("gc")) + { + Debug("gc") << "marking node value " << nv << " [" << nv->d_id + << "]: as maxed out" << std::endl; + } + d_maxedOut.push_back(nv); + } /** - * Make a set of types representing the given datatypes, which may be - * mutually recursive. + * Reclaim all zombies. */ - std::vector mkMutualDatatypeTypes( - const std::vector& datatypes, uint32_t flags = DATATYPE_FLAG_NONE); + void reclaimZombies(); /** - * Make a set of types representing the given datatypes, which may - * be mutually recursive. unresolvedTypes is a set of SortTypes - * that were used as placeholders in the Datatypes for the Datatypes - * of the same name. This is just a more complicated version of the - * above mkMutualDatatypeTypes() function, but is required to handle - * complex types. - * - * For example, unresolvedTypes might contain the single sort "list" - * (with that name reported from SortType::getName()). The - * datatypes list might have the single datatype - * - * DATATYPE - * list = cons(car:ARRAY INT OF list, cdr:list) | nil; - * END; - * - * To represent the Type of the array, the user had to create a - * placeholder type (an uninterpreted sort) to stand for "list" in - * the type of "car". It is this placeholder sort that should be - * passed in unresolvedTypes. If the datatype was of the simpler - * form: - * - * DATATYPE - * list = cons(car:list, cdr:list) | nil; - * END; - * - * then no complicated Type needs to be created, and the above, - * simpler form of mkMutualDatatypeTypes() is enough. + * It is safe to collect zombies. */ - std::vector mkMutualDatatypeTypes( - const std::vector& datatypes, - const std::set& unresolvedTypes, - uint32_t flags = DATATYPE_FLAG_NONE); + bool safeToReclaimZombies() const; /** - * Make a type representing a constructor with the given argument (subfield) - * types and return type range. + * Create a variable with the given name and type. NOTE that no + * lookup is done on the name. If you mkVar("a", type) and then + * mkVar("a", type) again, you have two variables. The NodeManager + * version of this is private to avoid internal uses of mkVar() from + * within cvc5. Such uses should employ SkolemManager::mkSkolem() instead. */ - TypeNode mkConstructorType(const std::vector& args, TypeNode range); + Node mkVar(const std::string& name, const TypeNode& type); - /** Make a type representing a selector with the given parameterization */ - TypeNode mkSelectorType(TypeNode domain, TypeNode range); + /** Create a variable with the given type. */ + Node mkVar(const TypeNode& type); - /** Make a type representing a tester with given parameterization */ - TypeNode mkTesterType(TypeNode domain); + /** The skolem manager */ + std::unique_ptr d_skManager; + /** The bound variable manager */ + std::unique_ptr d_bvManager; - /** Make a type representing an updater with the given parameterization */ - TypeNode mkDatatypeUpdateType(TypeNode domain, TypeNode range); + NodeValuePool d_nodeValuePool; - /** Bits for use in mkSort() flags. */ - enum - { - SORT_FLAG_NONE = 0, - SORT_FLAG_PLACEHOLDER = 1 - }; /* enum */ + bool d_initialized; - /** Make a new (anonymous) sort of arity 0. */ - TypeNode mkSort(uint32_t flags = SORT_FLAG_NONE); + size_t next_id; - /** Make a new sort with the given name of arity 0. */ - TypeNode mkSort(const std::string& name, uint32_t flags = SORT_FLAG_NONE); + expr::attr::AttributeManager* d_attrManager; - /** Make a new sort by parameterizing the given sort constructor. */ - TypeNode mkSort(TypeNode constructor, - const std::vector& children, - uint32_t flags = SORT_FLAG_NONE); + /** + * The node value we're currently freeing. This unique node value + * is permitted to have outstanding TNodes to it (in "soft" + * contexts, like as a key in attribute tables), even though + * normally it's an error to have a TNode to a node value with a + * reference count of 0. Being "under deletion" also enables + * assertions that inc() is not called on it. + */ + expr::NodeValue* d_nodeUnderDeletion; - /** Make a new sort with the given name and arity. */ - TypeNode mkSortConstructor(const std::string& name, - size_t arity, - uint32_t flags = SORT_FLAG_NONE); + /** + * True iff we are in reclaimZombies(). This avoids unnecessary + * recursion; a NodeValue being deleted might zombify other + * NodeValues, but these shouldn't trigger a (recursive) call to + * reclaimZombies(). + */ + bool d_inReclaimZombies; /** - * Get the type for the given node and optionally do type checking. - * - * Initial type computation will be near-constant time if - * type checking is not requested. Results are memoized, so that - * subsequent calls to getType() without type checking will be - * constant time. - * - * Initial type checking is linear in the size of the expression. - * Again, the results are memoized, so that subsequent calls to - * getType(), with or without type checking, will be constant - * time. - * - * NOTE: A TypeCheckingException can be thrown even when type - * checking is not requested. getType() will always return a - * valid and correct type and, thus, an exception will be thrown - * when no valid or correct type can be computed (e.g., if the - * arguments to a bit-vector operation aren't bit-vectors). When - * type checking is not requested, getType() will do the minimum - * amount of checking required to return a valid result. - * - * @param n the Node for which we want a type - * @param check whether we should check the type as we compute it - * (default: false) + * The set of zombie nodes. We may want to revisit this design, as + * we might like to delete nodes in least-recently-used order. But + * we also need to avoid processing a zombie twice. */ - TypeNode getType(TNode n, bool check = false); + NodeValueIDSet d_zombies; - /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/ - void reclaimZombiesUntil(uint32_t k); + /** + * NodeValues with maxed out reference counts. These live as long as the + * NodeManager. They have a custom deallocation procedure at the very end. + */ + std::vector d_maxedOut; - /** Reclaims all zombies (if possible).*/ - void reclaimAllZombies(); + /** + * A set of operator singletons (w.r.t. to this NodeManager + * instance) for operators. Conceptually, Nodes with kind, say, + * PLUS, are APPLYs of a PLUS operator to arguments. This array + * holds the set of operators for these things. A PLUS operator is + * a Node with kind "BUILTIN", and if you call + * plusOperator->getConst(), you get kind::PLUS back. + */ + Node d_operators[kind::LAST_KIND]; - /** Size of the node pool. */ - size_t poolSize() const; + /** unique vars per (Kind,Type) */ + std::map> d_unique_vars; - /** Deletes a list of attributes from the NM's AttributeManager.*/ - void deleteAttributes(const std::vector< const expr::attr::AttributeUniqueId* >& ids); + /** A list of datatypes owned by this node manager */ + std::vector> d_dtypes; + + TupleTypeCache d_tt_cache; + RecTypeCache d_rt_cache; /** - * This function gives developers a hook into the NodeManager. - * This can be changed in node_manager.cpp without recompiling most of cvc5. - * - * debugHook is a debugging only function, and should not be present in - * any published code! + * Keep a count of all abstract values produced by this NodeManager. + * Abstract values have a type attribute, so if multiple SolverEngines + * are attached to this NodeManager, we don't want their abstract + * values to overlap. */ - void debugHook(int debugFlag); + uint32_t d_abstractValueCount; }; /* class NodeManager */ inline TypeNode NodeManager::mkArrayType(TypeNode indexType,