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
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<expr::NodeValue*,
- expr::NodeValuePoolHashFunction,
- expr::NodeValuePoolEq> NodeValuePool;
- typedef std::unordered_set<expr::NodeValue*,
- expr::NodeValueIDHashFunction,
- expr::NodeValueIDEquality> 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<SkolemManager> d_skManager;
- /** The bound variable manager */
- std::unique_ptr<BoundVarManager> 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<cvc5::Kind>() 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
+ * <code>AttrKind::value_type</code> if not.
*/
- std::vector<expr::NodeValue*> d_maxedOut;
+ template <class AttrKind>
+ 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<cvc5::Kind>(), 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 <code>true</code> iff <code>attr</code> is set for
+ * <code>nv</code>.
*/
- 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<std::unique_ptr<DType> > d_dtypes;
+ template <class AttrKind>
+ 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.
+ * <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>.
*/
- 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 <class AttrKind>
+ 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 <code>attr</code> for <code>nv</code>
*/
- unsigned d_abstractValueCount;
+ template <class AttrKind>
+ 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
+ * <code>AttrKind::value_type</code> if not.
*/
- inline expr::NodeValue* poolLookup(expr::NodeValue* nv) const;
+ template <class AttrKind>
+ 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 <code>true</code> iff <code>attr</code> is set for <code>n</code>.
*/
- inline void poolInsert(expr::NodeValue* nv);
+ template <class AttrKind>
+ 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.
+ * <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>.
*/
- inline void poolRemove(expr::NodeValue* nv);
+ template <class AttrKind>
+ 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 <code>attr</code> for <code>n</code>
*/
- inline bool isCurrentlyDeleting(const expr::NodeValue* nv) const {
- return d_nodeUnderDeletion == nv;
- }
+ template <class AttrKind>
+ 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
+ * <code>AttrKind::value_type</code> if not.
*/
- inline void markForDeletion(expr::NodeValue* nv) {
- Assert(nv->d_rc == 0);
+ template <class AttrKind>
+ 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 <code>true</code> iff <code>attr</code> is set for <code>n</code>.
+ */
+ template <class AttrKind>
+ 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.
+ * <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 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 <code>attr</code> for <code>n</code>
+ */
+ template <class AttrKind>
+ 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<const expr::attr::AttributeUniqueId*>& 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. <code>argTypes</code> 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<expr::NodeValue*> TopologicalSort(
- const std::vector<expr::NodeValue*>& roots);
+ TypeNode mkFunctionType(const std::vector<TypeNode>& 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<NodeValue&>(nvStorage);
+ * Make a function type with input types from
+ * <code>sorts[0..sorts.size()-2]</code> and result type
+ * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> 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 <size_t N>
- struct NVStorage {
- expr::NodeValue nv;
- expr::NodeValue* child[N];
- };/* struct NodeManager::NVStorage<N> */
-
- // undefined private copy constructor (disallow copy)
- NodeManager(const NodeManager&) = delete;
+ TypeNode mkFunctionType(const std::vector<TypeNode>& sorts);
- NodeManager& operator=(const NodeManager&) = delete;
+ /**
+ * Make a predicate type with input types from
+ * <code>sorts</code>. The result with be a function type with range
+ * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
+ * element.
+ */
+ TypeNode mkPredicateType(const std::vector<TypeNode>& 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
+ * <code>types</code>. <code>types</code> 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<TypeNode>& 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 <code>exp</code> bit exponent and
+ <code>sig</code> bit significand */
+ TypeNode mkFloatingPointType(unsigned exp, unsigned sig);
+ TypeNode mkFloatingPointType(FloatingPointSize fs);
+
+ /** Make the type of bitvectors of size <code>size</code> */
+ 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<TypeNode> mkMutualDatatypeTypes(
+ const std::vector<DType>& 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<TypeNode> mkMutualDatatypeTypes(
+ const std::vector<DType>& datatypes,
+ const std::set<TypeNode>& 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<TypeNode>& 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);
*/
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 <code>children.size()</code> is greater than the max arity for
* 2, then calling <code>mkAssociative(FOO,a,b,c)</code> will return
* <code>(FOO (FOO a b) c)</code> or <code>(FOO a (FOO b c))</code>.
* 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<Node>& 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<Node>& 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<Node>& 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<Node>& 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 <class T>
- Node mkConst(const T&);
-
- /**
- * Create a constant of type `T` with an explicit kind `k`.
- */
- template <class T>
- Node mkConst(Kind k, const T&);
-
- template <class T>
- TypeNode mkTypeConst(const T&);
-
- template <class NodeClass, class T>
- 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<TypeNode>& 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<cvc5::Kind>() 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
- * <code>AttrKind::value_type</code> if not.
- */
- template <class AttrKind>
- 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 <code>true</code> iff <code>attr</code> is set for
- * <code>nv</code>.
- */
- template <class AttrKind>
- 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.
- * <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>.
+ * traversal of the resulting tree.
*/
- template <class AttrKind>
- inline bool getAttribute(expr::NodeValue* nv,
- const AttrKind& attr,
- typename AttrKind::value_type& value) const;
+ Node mkAssociative(Kind kind, const std::vector<Node>& 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 <code>attr</code> for <code>nv</code>
+ * 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 <class AttrKind>
- inline void setAttribute(expr::NodeValue* nv,
- const AttrKind& attr,
- const typename AttrKind::value_type& value);
-
+ Node mkLeftAssociative(Kind kind, const std::vector<Node>& 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
- * <code>AttrKind::value_type</code> 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 <class AttrKind>
- inline typename AttrKind::value_type
- getAttribute(TNode n, const AttrKind& attr) const;
+ Node mkRightAssociative(Kind kind, const std::vector<Node>& 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 <code>true</code> iff <code>attr</code> is set for <code>n</code>.
+ * 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 <class AttrKind>
- inline bool hasAttribute(TNode n,
- const AttrKind& attr) const;
+ Node mkChain(Kind kind, const std::vector<Node>& 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.
- * <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>.
+ * 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 <class AttrKind>
- 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 <code>attr</code> for <code>n</code>
+ * 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 <class AttrKind>
- 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
- * <code>AttrKind::value_type</code> if not.
+ * Create a constant of type T. It will have the appropriate
+ * CONST_* kind defined for T.
*/
- template <class AttrKind>
- inline typename AttrKind::value_type
- getAttribute(TypeNode n, const AttrKind& attr) const;
+ template <class T>
+ 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 <code>true</code> iff <code>attr</code> is set for <code>n</code>.
+ * Create a constant of type `T` with an explicit kind `k`.
*/
- template <class AttrKind>
- inline bool hasAttribute(TypeNode n,
- const AttrKind& attr) const;
+ template <class T>
+ Node mkConst(Kind k, const T&);
+
+ template <class T>
+ TypeNode mkTypeConst(const T&);
+
+ template <class NodeClass, class T>
+ 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.
- * <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>.
+ * Make constant real. Returns constant of kind CONST_RATIONAL with Rational
+ * payload.
*/
- template <class AttrKind>
- 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 <code>attr</code> for <code>n</code>
+ * !!! Note until subtypes are eliminated, this returns a constant of kind
+ * CONST_RATIONAL.
*/
- template <class AttrKind>
- 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<TypeNode>& 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<TypeNode>& 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<expr::NodeValue*,
+ expr::NodeValuePoolHashFunction,
+ expr::NodeValuePoolEq>
+ NodeValuePool;
+ typedef std::unordered_set<expr::NodeValue*,
+ expr::NodeValueIDHashFunction,
+ expr::NodeValueIDEquality>
+ 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<NodeValue&>(nvStorage);
+ *
+ * ...and then you can use nvStack as a NodeValue that you know has
+ * room for 4 children.
+ */
+ template <size_t N>
+ struct NVStorage
+ {
+ expr::NodeValue nv;
+ expr::NodeValue* child[N];
+ }; /* struct NodeManager::NVStorage<N> */
/**
- * 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<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);
+ };
/**
- * 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<expr::NodeValue*> TopologicalSort(
+ const std::vector<expr::NodeValue*>& roots);
/**
- * Make a function type with input types from
- * argTypes. <code>argTypes</code> 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<TypeNode>& 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
- * <code>sorts[0..sorts.size()-2]</code> and result type
- * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> 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<TypeNode>& sorts);
+ expr::NodeValue* poolLookup(expr::NodeValue* nv) const;
/**
- * Make a predicate type with input types from
- * <code>sorts</code>. The result with be a function type with range
- * <code>BOOLEAN</code>. <code>sorts</code> 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<TypeNode>& sorts);
+ void poolInsert(expr::NodeValue* nv);
/**
- * Make a tuple type with types from
- * <code>types</code>. <code>types</code> 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<TypeNode>& 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 <code>exp</code> bit exponent and
- <code>sig</code> bit significand */
- TypeNode mkFloatingPointType(unsigned exp, unsigned sig);
- TypeNode mkFloatingPointType(FloatingPointSize fs);
-
- /** Make the type of bitvectors of size <code>size</code> */
- 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<TypeNode> mkMutualDatatypeTypes(
- const std::vector<DType>& 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<TypeNode> mkMutualDatatypeTypes(
- const std::vector<DType>& datatypes,
- const std::set<TypeNode>& 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<TypeNode>& 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<SkolemManager> d_skManager;
+ /** The bound variable manager */
+ std::unique_ptr<BoundVarManager> 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<TypeNode>& 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<expr::NodeValue*> 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<cvc5::Kind>(), 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<Kind, std::map<TypeNode, Node>> 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<std::unique_ptr<DType>> 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,
projects / cvc5.git / commitdiff