From 577d4b6bde6c31bd77254de9355666f6b698cc45 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 15 Dec 2021 11:03:26 -0800 Subject: Explicitly disallow `mkConst(Rational)` The `Rational` payload can be associated with two kinds (`CONST_INTEGER` and `CONST_RATIONAL`), so we should never call `NodeManager::mkConst(Rational)`, but instead use `NodeManager::mkConstInt()` and `NodeManager::mkConstReal()`. Currently, calling `NodeManager::mkConst(Rational)` silently creates an integer constant, which is dangerous. This commit makes it a compile-time error instead. --- src/expr/CMakeLists.txt | 13 +- src/expr/mkmetakind | 21 +- src/expr/node_manager.h | 1211 ---------------------------- src/expr/node_manager_template.cpp | 6 - src/expr/node_manager_template.h | 1215 +++++++++++++++++++++++++++++ src/theory/arith/kinds | 6 +- src/theory/strings/sequences_rewriter.cpp | 2 +- 7 files changed, 1250 insertions(+), 1224 deletions(-) delete mode 100644 src/expr/node_manager.h create mode 100644 src/expr/node_manager_template.h diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 9a89dfbe6..e00e938e0 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -47,7 +47,6 @@ libcvc5_add_sources( node_builder.h node_converter.cpp node_converter.h - node_manager.h node_manager_attributes.h node_self_iterator.h node_trie.cpp @@ -104,6 +103,7 @@ libcvc5_add_sources(GENERATED metakind.cpp metakind.h node_manager.cpp + node_manager.h type_checker.cpp type_properties.cpp type_properties.h @@ -177,6 +177,16 @@ add_custom_command( DEPENDS mkmetakind metakind_template.cpp metakind.h ${KINDS_FILES} ) +add_custom_command( + OUTPUT node_manager.h + COMMAND + ${mkmetakind_script} + ${CMAKE_CURRENT_LIST_DIR}/node_manager_template.h + ${KINDS_FILES} + > ${CMAKE_CURRENT_BINARY_DIR}/node_manager.h + DEPENDS mkmetakind node_manager_template.h ${KINDS_FILES} +) + add_custom_command( OUTPUT node_manager.cpp COMMAND @@ -204,6 +214,7 @@ add_custom_target(gen-expr metakind.cpp metakind.h node_manager.cpp + node_manager.h type_checker.cpp type_properties.cpp type_properties.h diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index d5f6d9b1a..3ee7dc59b 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -54,6 +54,7 @@ metakind_ubchildren= metakind_lbchildren= metakind_operatorKinds= metakind_mkConst= +metakind_mkConstDelete= seen_theory=false seen_theory_builtin=false @@ -295,8 +296,23 @@ TypeNode NodeManager::mkTypeConst<${class}>(const ${class}& val) } " metakind_mkConst="${metakind_mkConst} -template -Node NodeManager::mkConst(Kind k, const ${class}& val); +template<> +Node NodeManager::mkConst(Kind k, const ${class}& val) +{ + return mkConstInternal(k, val); +} +" + elif [[ "${payload_seen}" != true ]]; then + metakind_mkConstDelete="${metakind_mkConstDelete} +template<> +Node NodeManager::mkConst<${class}>(const ${class}& val) = delete; +" + metakind_mkConst="${metakind_mkConst} +template<> +Node NodeManager::mkConst(Kind k, const ${class}& val) +{ + return mkConstInternal(k, val); +} " fi @@ -442,6 +458,7 @@ for var in \ metakind_lbchildren \ metakind_operatorKinds \ metakind_mkConst \ + metakind_mkConstDelete \ template \ ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h deleted file mode 100644 index b2682661e..000000000 --- a/src/expr/node_manager.h +++ /dev/null @@ -1,1211 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Andrew Reynolds, Christopher L. Conway - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * A manager for Nodes. - */ - -#include "cvc5_private.h" - -/* circular dependency; force node.h first */ -#include "expr/node.h" -#include "expr/type_node.h" - -#ifndef CVC5__NODE_MANAGER_H -#define CVC5__NODE_MANAGER_H - -#include -#include -#include - -#include "base/check.h" -#include "expr/kind.h" -#include "expr/node_builder.h" -#include "expr/node_value.h" -#include "util/floatingpoint_size.h" - -namespace cvc5 { - -using Record = std::vector>; - -namespace api { -class Solver; -} - -class ResourceManager; -class SkolemManager; -class BoundVarManager; - -class DType; -class Rational; - -namespace expr { - namespace attr { - class AttributeUniqueId; - class AttributeManager; - } // namespace attr - - class TypeChecker; - } // namespace expr - -class NodeManager -{ - friend class api::Solver; - friend class expr::NodeValue; - friend class expr::TypeChecker; - friend class SkolemManager; - - friend class NodeBuilder; - - public: - /** - * 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 - * of a node. - */ - static bool isNAryKind(Kind k); - - /** - * Returns a node representing the operator of this `TypeNode`. - * PARAMETERIZED-metakinded types (the SORT_TYPE is one of these) have an - * operator. "Little-p parameterized" types (like Array), are OPERATORs, not - * PARAMETERIZEDs. - */ - static Node operatorFromType(const TypeNode& tn) - { - Assert(tn.getMetaKind() == kind::metakind::PARAMETERIZED); - 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(); - - /** Predicate for use with STL algorithms */ - struct NodeValueReferenceCountNonZero { - bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; } - }; - - typedef std::unordered_set NodeValuePool; - typedef std::unordered_set NodeValueIDSet; - - /** The skolem manager */ - std::unique_ptr d_skManager; - /** The bound variable manager */ - std::unique_ptr d_bvManager; - - NodeValuePool d_nodeValuePool; - - bool d_initialized; - - size_t next_id; - - expr::attr::AttributeManager* d_attrManager; - - /** - * 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; - - /** - * 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; - - /** - * 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. - */ - NodeValueIDSet d_zombies; - - /** - * 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; - - /** - * 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]; - - /** 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; - - /** - * 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 ); - }; - TupleTypeCache d_tt_cache; - RecTypeCache d_rt_cache; - - /** - * 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. - */ - unsigned d_abstractValueCount; - - /** - * 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. - * - * 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! - */ - inline expr::NodeValue* poolLookup(expr::NodeValue* nv) const; - - /** - * Insert a NodeValue into the NodeManager's pool. - * - * It is an error to insert a NodeValue already in the pool. - * Enquire first with poolLookup(). - */ - inline void poolInsert(expr::NodeValue* nv); - - /** - * Remove a NodeValue from the NodeManager's pool. - * - * It is an error to request the removal of a NodeValue from the - * pool that is not in the pool. - */ - inline void poolRemove(expr::NodeValue* nv); - - /** - * Determine if nv is currently being deleted by the NodeManager. - */ - inline bool isCurrentlyDeleting(const expr::NodeValue* nv) const { - return d_nodeUnderDeletion == nv; - } - - /** - * Register a NodeValue as a zombie. - */ - inline void markForDeletion(expr::NodeValue* nv) { - Assert(nv->d_rc == 0); - - // 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; - } - - // `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); - - d_zombies.insert(nv); - - if(safeToReclaimZombies()) { - if(d_zombies.size() > 5000) { - reclaimZombies(); - } - } - } - - /** - * Register a NodeValue as having a maxed out reference count. This NodeValue - * will live as long as its containing NodeManager. - */ - 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); - } - - /** - * Reclaim all zombies. - */ - void reclaimZombies(); - - /** - * It is safe to collect zombies. - */ - bool safeToReclaimZombies() const; - - /** - * 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). - */ - static std::vector TopologicalSort( - const std::vector& roots); - - /** - * 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 */ - - // undefined private copy constructor (disallow copy) - NodeManager(const NodeManager&) = delete; - - NodeManager& operator=(const NodeManager&) = delete; - - /** - * 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. - */ - Node mkVar(const std::string& name, const TypeNode& type); - - /** Create a variable with the given type. */ - Node mkVar(const TypeNode& type); - - 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. - */ - void init(); - - /** 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(); } - - /** - * 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. - */ - const DType& getDTypeForIndex(size_t index) const; - - /** Get a Kind from an operator expression */ - static inline Kind operatorToKind(TNode n); - - /** 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); - - // general expression-builders - // - /** Create a node with no child. */ - Node mkNode(Kind kind); - - /** Create a node with one child. */ - Node mkNode(Kind kind, TNode child1); - - /** Create a node with two children. */ - Node mkNode(Kind kind, TNode child1, TNode child2); - - /** Create a node with three children. */ - Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3); - - /** Create a node with an arbitrary number of children. */ - template - Node mkNode(Kind kind, const std::vector >& children); - - /** Create a node using an initializer list. - * - * This function serves two purposes: - * - We can avoid creating a temporary vector in some cases, e.g., when we - * want to create a node with a fixed, large number of children - * - It makes sure that calls to `mkNode` that braced-init-lists work as - * expected, e.g., mkNode(REGEXP_NONE, {}) will call this overload instead - * of creating a node with a null node as a child. - */ - Node mkNode(Kind kind, std::initializer_list children); - - /** - * Create an AND node with arbitrary number of children. This returns the - * true node if children is empty, or the single node in children if - * it contains only one node. - * - * We define construction of AND as a special case here since it is widely - * used for e.g. constructing explanations. - */ - template - Node mkAnd(const std::vector >& children); - - /** - * Create an OR node with arbitrary number of children. This returns the - * false node if children is empty, or the single node in children if - * it contains only one node. - * - * We define construction of OR as a special case here since it is widely - * used for e.g. constructing explanations or lemmas. - */ - template - Node mkOr(const std::vector >& children); - - /** Create a node (with no children) by operator. */ - Node mkNode(TNode opNode); - - /** Create a node with one child by operator. */ - Node mkNode(TNode opNode, TNode child1); - - /** Create a node with two children by operator. */ - Node mkNode(TNode opNode, TNode child1, TNode child2); - - /** Create a node with three children by operator. */ - Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3); - - /** Create a node by applying an operator to the children. */ - template - Node mkNode(TNode opNode, const std::vector >& children); - - /** - * Create a node by applying an operator to an arbitrary number of children. - * - * Analoguous to `mkNode(Kind, std::initializer_list)`. - */ - Node mkNode(TNode opNode, std::initializer_list children); - - Node mkBoundVar(const std::string& name, const TypeNode& type); - - Node mkBoundVar(const TypeNode& type); - - /** - * Construct and return a ground term of a given type. If the type is not - * well founded, this function throws an exception. - * - * @param tn The type - * @return a ground term of the type - */ - Node mkGroundTerm(const TypeNode& tn); - - /** - * Construct and return a ground value of a given type. If the type is not - * well founded, this function throws an exception. - * - * @param tn The type - * @return a ground value of the type - */ - 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 - * kind, then the expression will be broken up into - * suitably-sized chunks, taking advantage of the associativity of - * kind. For example, if kind FOO has max arity - * 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. - */ - template - inline bool getAttribute(expr::NodeValue* nv, - const AttrKind& attr, - typename AttrKind::value_type& value) const; - - /** - * 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 - */ - template - inline void setAttribute(expr::NodeValue* nv, - const AttrKind& attr, - const typename AttrKind::value_type& value); - - /** - * Retrieve an attribute for a TNode. - * - * @param n the node - * @param attr an instance of the attribute kind to retrieve. - * @returns the attribute, if set, or a default-constructed - * AttrKind::value_type if not. - */ - template - inline typename AttrKind::value_type - getAttribute(TNode n, const AttrKind& attr) const; - - /** - * Check whether an attribute is set for a TNode. - * - * @param n the node - * @param attr an instance of the attribute kind to check - * @returns true iff attr is set for n. - */ - template - inline bool hasAttribute(TNode n, - const AttrKind& attr) const; - - /** - * 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. - */ - template - inline bool getAttribute(TNode n, - const AttrKind& attr, - typename AttrKind::value_type& value) const; - - /** - * 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 - */ - template - inline void setAttribute(TNode n, - const AttrKind& attr, - const typename AttrKind::value_type& value); - - /** - * 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. - */ - template - inline typename AttrKind::value_type - getAttribute(TypeNode n, const AttrKind& attr) const; - - /** - * 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; - - /** - * 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; - - /** - * 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); - - /** 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(); - - /** - * 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(); - - /** - * Make a function type from domain to range. - * - * @param domain the domain type - * @param range the range type - * @returns the functional type domain -> range - */ - TypeNode mkFunctionType(const TypeNode& domain, - const TypeNode& range); - - /** - * 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 - */ - TypeNode mkFunctionType(const std::vector& argTypes, - const TypeNode& range); - - /** - * 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. - * - * @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 - */ - TypeNode mkFunctionType(const std::vector& sorts); - - /** - * 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); - - /** - * 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]) - */ - TypeNode mkTupleType(const std::vector& types); - - /** - * 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); - - /** - * @returns the symbolic expression type - */ - 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); - - /** Make the type of arrays with the given parameterization */ - inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType); - - /** Make the type of set with the given parameterization */ - inline 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); - - /** 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 */ - - /** Make a type representing the given datatype. */ - TypeNode mkDatatypeType(DType& datatype, uint32_t flags = DATATYPE_FLAG_NONE); - - /** - * Make a set of types representing the given datatypes, which may be - * mutually recursive. - */ - std::vector mkMutualDatatypeTypes( - const std::vector& datatypes, uint32_t flags = DATATYPE_FLAG_NONE); - - /** - * 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. - */ - 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); - - /** Bits for use in mkSort() flags. */ - enum - { - SORT_FLAG_NONE = 0, - SORT_FLAG_PLACEHOLDER = 1 - }; /* enum */ - - /** Make a new (anonymous) sort of arity 0. */ - TypeNode mkSort(uint32_t flags = SORT_FLAG_NONE); - - /** Make a new sort with the given name of arity 0. */ - TypeNode mkSort(const std::string& name, uint32_t flags = SORT_FLAG_NONE); - - /** Make a new sort by parameterizing the given sort constructor. */ - TypeNode mkSort(TypeNode constructor, - const std::vector& children, - uint32_t flags = SORT_FLAG_NONE); - - /** 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 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) - */ - TypeNode getType(TNode n, bool check = false); - - /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/ - void reclaimZombiesUntil(uint32_t k); - - /** Reclaims all zombies (if possible).*/ - void reclaimAllZombies(); - - /** Size of the node pool. */ - size_t poolSize() const; - - /** Deletes a list of attributes from the NM's AttributeManager.*/ - void deleteAttributes(const std::vector< const expr::attr::AttributeUniqueId* >& ids); - - /** - * 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! - */ - void debugHook(int debugFlag); -}; /* class NodeManager */ - -inline TypeNode NodeManager::mkArrayType(TypeNode indexType, - TypeNode constituentType) { - CheckArgument(!indexType.isNull(), indexType, - "unexpected NULL index type"); - CheckArgument(!constituentType.isNull(), constituentType, - "unexpected NULL constituent type"); - Debug("arrays") << "making array type " << indexType << " " - << constituentType << std::endl; - return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType); -} - -inline TypeNode NodeManager::mkSetType(TypeNode elementType) { - CheckArgument(!elementType.isNull(), elementType, - "unexpected NULL element type"); - Debug("sets") << "making sets type " << elementType << std::endl; - return mkTypeNode(kind::SET_TYPE, elementType); -} - -inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const { - NodeValuePool::const_iterator find = d_nodeValuePool.find(nv); - if(find == d_nodeValuePool.end()) { - return NULL; - } else { - return *find; - } -} - -inline void NodeManager::poolInsert(expr::NodeValue* nv) { - Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end()) - << "NodeValue already in the pool!"; - d_nodeValuePool.insert(nv);// FIXME multithreading -} - -inline void NodeManager::poolRemove(expr::NodeValue* nv) { - Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end()) - << "NodeValue is not in the pool!"; - - d_nodeValuePool.erase(nv);// FIXME multithreading -} - -inline Kind NodeManager::operatorToKind(TNode n) { - return kind::operatorToKind(n.d_nv); -} - -inline Node NodeManager::mkNode(Kind kind) -{ - NodeBuilder nb(this, kind); - return nb.constructNode(); -} - -inline Node NodeManager::mkNode(Kind kind, TNode child1) { - NodeBuilder nb(this, kind); - nb << child1; - return nb.constructNode(); -} - -inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) { - NodeBuilder nb(this, kind); - nb << child1 << child2; - return nb.constructNode(); -} - -inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, - TNode child3) { - NodeBuilder nb(this, kind); - nb << child1 << child2 << child3; - return nb.constructNode(); -} - -// N-ary version -template -inline Node NodeManager::mkNode(Kind kind, - const std::vector >& - children) { - NodeBuilder nb(this, kind); - nb.append(children); - return nb.constructNode(); -} - -template -Node NodeManager::mkAnd(const std::vector >& children) -{ - if (children.empty()) - { - return mkConst(true); - } - else if (children.size() == 1) - { - return children[0]; - } - return mkNode(kind::AND, children); -} - -template -Node NodeManager::mkOr(const std::vector >& children) -{ - if (children.empty()) - { - return mkConst(false); - } - else if (children.size() == 1) - { - return children[0]; - } - return mkNode(kind::OR, children); -} - -// for operators -inline Node NodeManager::mkNode(TNode opNode) { - NodeBuilder nb(this, operatorToKind(opNode)); - if(opNode.getKind() != kind::BUILTIN) { - nb << opNode; - } - return nb.constructNode(); -} - -inline Node NodeManager::mkNode(TNode opNode, TNode child1) { - NodeBuilder nb(this, operatorToKind(opNode)); - if(opNode.getKind() != kind::BUILTIN) { - nb << opNode; - } - nb << child1; - return nb.constructNode(); -} - -inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) { - NodeBuilder nb(this, operatorToKind(opNode)); - if(opNode.getKind() != kind::BUILTIN) { - nb << opNode; - } - nb << child1 << child2; - return nb.constructNode(); -} - -inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2, - TNode child3) { - NodeBuilder nb(this, operatorToKind(opNode)); - if(opNode.getKind() != kind::BUILTIN) { - nb << opNode; - } - nb << child1 << child2 << child3; - return nb.constructNode(); -} - -// N-ary version for operators -template -inline Node NodeManager::mkNode(TNode opNode, - const std::vector >& - children) { - NodeBuilder nb(this, operatorToKind(opNode)); - if(opNode.getKind() != kind::BUILTIN) { - nb << opNode; - } - nb.append(children); - return nb.constructNode(); -} - -inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1) { - return (NodeBuilder(this, kind) << child1).constructTypeNode(); -} - -inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1, - TypeNode child2) { - return (NodeBuilder(this, kind) << child1 << child2).constructTypeNode(); -} - -inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1, - TypeNode child2, TypeNode child3) { - return (NodeBuilder(this, kind) << child1 << child2 << child3) - .constructTypeNode(); -} - -// N-ary version for types -inline TypeNode NodeManager::mkTypeNode(Kind kind, - const std::vector& children) { - return NodeBuilder(this, kind).append(children).constructTypeNode(); -} - -} // namespace cvc5 - -#endif /* CVC5__NODE_MANAGER_H */ diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp index 4f235a53a..944d7fe66 100644 --- a/src/expr/node_manager_template.cpp +++ b/src/expr/node_manager_template.cpp @@ -1158,12 +1158,6 @@ TNode NodeManager::operatorOf(Kind k) return d_operators[k]; } -template -Node NodeManager::mkConst(Kind k, const T& val) -{ - return mkConstInternal(k, val); -} - template NodeClass NodeManager::mkConstInternal(Kind k, const T& val) { diff --git a/src/expr/node_manager_template.h b/src/expr/node_manager_template.h new file mode 100644 index 000000000..073077344 --- /dev/null +++ b/src/expr/node_manager_template.h @@ -0,0 +1,1215 @@ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Andrew Reynolds, Christopher L. Conway + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A manager for Nodes. + */ + +#include "cvc5_private.h" + +/* circular dependency; force node.h first */ +#include "expr/node.h" +#include "expr/type_node.h" + +#ifndef CVC5__NODE_MANAGER_H +#define CVC5__NODE_MANAGER_H + +#include +#include +#include + +#include "base/check.h" +#include "expr/kind.h" +#include "expr/node_builder.h" +#include "expr/node_value.h" +#include "util/floatingpoint_size.h" + +namespace cvc5 { + +using Record = std::vector>; + +namespace api { +class Solver; +} + +class ResourceManager; +class SkolemManager; +class BoundVarManager; + +class DType; +class Rational; + +namespace expr { + namespace attr { + class AttributeUniqueId; + class AttributeManager; + } // namespace attr + + class TypeChecker; + } // namespace expr + +class NodeManager +{ + friend class api::Solver; + friend class expr::NodeValue; + friend class expr::TypeChecker; + friend class SkolemManager; + + friend class NodeBuilder; + + public: + /** + * 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 + * of a node. + */ + static bool isNAryKind(Kind k); + + /** + * Returns a node representing the operator of this `TypeNode`. + * PARAMETERIZED-metakinded types (the SORT_TYPE is one of these) have an + * operator. "Little-p parameterized" types (like Array), are OPERATORs, not + * PARAMETERIZEDs. + */ + static Node operatorFromType(const TypeNode& tn) + { + Assert(tn.getMetaKind() == kind::metakind::PARAMETERIZED); + 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(); + + /** Predicate for use with STL algorithms */ + struct NodeValueReferenceCountNonZero { + bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; } + }; + + typedef std::unordered_set NodeValuePool; + typedef std::unordered_set NodeValueIDSet; + + /** The skolem manager */ + std::unique_ptr d_skManager; + /** The bound variable manager */ + std::unique_ptr d_bvManager; + + NodeValuePool d_nodeValuePool; + + bool d_initialized; + + size_t next_id; + + expr::attr::AttributeManager* d_attrManager; + + /** + * 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; + + /** + * 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; + + /** + * 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. + */ + NodeValueIDSet d_zombies; + + /** + * 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; + + /** + * 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]; + + /** 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; + + /** + * 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 ); + }; + TupleTypeCache d_tt_cache; + RecTypeCache d_rt_cache; + + /** + * 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. + */ + unsigned d_abstractValueCount; + + /** + * 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. + * + * 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! + */ + inline expr::NodeValue* poolLookup(expr::NodeValue* nv) const; + + /** + * Insert a NodeValue into the NodeManager's pool. + * + * It is an error to insert a NodeValue already in the pool. + * Enquire first with poolLookup(). + */ + inline void poolInsert(expr::NodeValue* nv); + + /** + * Remove a NodeValue from the NodeManager's pool. + * + * It is an error to request the removal of a NodeValue from the + * pool that is not in the pool. + */ + inline void poolRemove(expr::NodeValue* nv); + + /** + * Determine if nv is currently being deleted by the NodeManager. + */ + inline bool isCurrentlyDeleting(const expr::NodeValue* nv) const { + return d_nodeUnderDeletion == nv; + } + + /** + * Register a NodeValue as a zombie. + */ + inline void markForDeletion(expr::NodeValue* nv) { + Assert(nv->d_rc == 0); + + // 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; + } + + // `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); + + d_zombies.insert(nv); + + if(safeToReclaimZombies()) { + if(d_zombies.size() > 5000) { + reclaimZombies(); + } + } + } + + /** + * Register a NodeValue as having a maxed out reference count. This NodeValue + * will live as long as its containing NodeManager. + */ + 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); + } + + /** + * Reclaim all zombies. + */ + void reclaimZombies(); + + /** + * It is safe to collect zombies. + */ + bool safeToReclaimZombies() const; + + /** + * 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). + */ + static std::vector TopologicalSort( + const std::vector& roots); + + /** + * 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 */ + + // undefined private copy constructor (disallow copy) + NodeManager(const NodeManager&) = delete; + + NodeManager& operator=(const NodeManager&) = delete; + + /** + * 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. + */ + Node mkVar(const std::string& name, const TypeNode& type); + + /** Create a variable with the given type. */ + Node mkVar(const TypeNode& type); + + 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. + */ + void init(); + + /** 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(); } + + /** + * 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. + */ + const DType& getDTypeForIndex(size_t index) const; + + /** Get a Kind from an operator expression */ + static inline Kind operatorToKind(TNode n); + + /** 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); + + // general expression-builders + // + /** Create a node with no child. */ + Node mkNode(Kind kind); + + /** Create a node with one child. */ + Node mkNode(Kind kind, TNode child1); + + /** Create a node with two children. */ + Node mkNode(Kind kind, TNode child1, TNode child2); + + /** Create a node with three children. */ + Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3); + + /** Create a node with an arbitrary number of children. */ + template + Node mkNode(Kind kind, const std::vector >& children); + + /** Create a node using an initializer list. + * + * This function serves two purposes: + * - We can avoid creating a temporary vector in some cases, e.g., when we + * want to create a node with a fixed, large number of children + * - It makes sure that calls to `mkNode` that braced-init-lists work as + * expected, e.g., mkNode(REGEXP_NONE, {}) will call this overload instead + * of creating a node with a null node as a child. + */ + Node mkNode(Kind kind, std::initializer_list children); + + /** + * Create an AND node with arbitrary number of children. This returns the + * true node if children is empty, or the single node in children if + * it contains only one node. + * + * We define construction of AND as a special case here since it is widely + * used for e.g. constructing explanations. + */ + template + Node mkAnd(const std::vector >& children); + + /** + * Create an OR node with arbitrary number of children. This returns the + * false node if children is empty, or the single node in children if + * it contains only one node. + * + * We define construction of OR as a special case here since it is widely + * used for e.g. constructing explanations or lemmas. + */ + template + Node mkOr(const std::vector >& children); + + /** Create a node (with no children) by operator. */ + Node mkNode(TNode opNode); + + /** Create a node with one child by operator. */ + Node mkNode(TNode opNode, TNode child1); + + /** Create a node with two children by operator. */ + Node mkNode(TNode opNode, TNode child1, TNode child2); + + /** Create a node with three children by operator. */ + Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3); + + /** Create a node by applying an operator to the children. */ + template + Node mkNode(TNode opNode, const std::vector >& children); + + /** + * Create a node by applying an operator to an arbitrary number of children. + * + * Analoguous to `mkNode(Kind, std::initializer_list)`. + */ + Node mkNode(TNode opNode, std::initializer_list children); + + Node mkBoundVar(const std::string& name, const TypeNode& type); + + Node mkBoundVar(const TypeNode& type); + + /** + * Construct and return a ground term of a given type. If the type is not + * well founded, this function throws an exception. + * + * @param tn The type + * @return a ground term of the type + */ + Node mkGroundTerm(const TypeNode& tn); + + /** + * Construct and return a ground value of a given type. If the type is not + * well founded, this function throws an exception. + * + * @param tn The type + * @return a ground value of the type + */ + 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 + * kind, then the expression will be broken up into + * suitably-sized chunks, taking advantage of the associativity of + * kind. For example, if kind FOO has max arity + * 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. + */ + template + inline bool getAttribute(expr::NodeValue* nv, + const AttrKind& attr, + typename AttrKind::value_type& value) const; + + /** + * 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 + */ + template + inline void setAttribute(expr::NodeValue* nv, + const AttrKind& attr, + const typename AttrKind::value_type& value); + + /** + * Retrieve an attribute for a TNode. + * + * @param n the node + * @param attr an instance of the attribute kind to retrieve. + * @returns the attribute, if set, or a default-constructed + * AttrKind::value_type if not. + */ + template + inline typename AttrKind::value_type + getAttribute(TNode n, const AttrKind& attr) const; + + /** + * Check whether an attribute is set for a TNode. + * + * @param n the node + * @param attr an instance of the attribute kind to check + * @returns true iff attr is set for n. + */ + template + inline bool hasAttribute(TNode n, + const AttrKind& attr) const; + + /** + * 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. + */ + template + inline bool getAttribute(TNode n, + const AttrKind& attr, + typename AttrKind::value_type& value) const; + + /** + * 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 + */ + template + inline void setAttribute(TNode n, + const AttrKind& attr, + const typename AttrKind::value_type& value); + + /** + * 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. + */ + template + inline typename AttrKind::value_type + getAttribute(TypeNode n, const AttrKind& attr) const; + + /** + * 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; + + /** + * 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; + + /** + * 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); + + /** 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(); + + /** + * 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(); + + /** + * Make a function type from domain to range. + * + * @param domain the domain type + * @param range the range type + * @returns the functional type domain -> range + */ + TypeNode mkFunctionType(const TypeNode& domain, + const TypeNode& range); + + /** + * 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 + */ + TypeNode mkFunctionType(const std::vector& argTypes, + const TypeNode& range); + + /** + * 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. + * + * @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 + */ + TypeNode mkFunctionType(const std::vector& sorts); + + /** + * 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); + + /** + * 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]) + */ + TypeNode mkTupleType(const std::vector& types); + + /** + * 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); + + /** + * @returns the symbolic expression type + */ + 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); + + /** Make the type of arrays with the given parameterization */ + inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType); + + /** Make the type of set with the given parameterization */ + inline 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); + + /** 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 */ + + /** Make a type representing the given datatype. */ + TypeNode mkDatatypeType(DType& datatype, uint32_t flags = DATATYPE_FLAG_NONE); + + /** + * Make a set of types representing the given datatypes, which may be + * mutually recursive. + */ + std::vector mkMutualDatatypeTypes( + const std::vector& datatypes, uint32_t flags = DATATYPE_FLAG_NONE); + + /** + * 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. + */ + 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); + + /** Bits for use in mkSort() flags. */ + enum + { + SORT_FLAG_NONE = 0, + SORT_FLAG_PLACEHOLDER = 1 + }; /* enum */ + + /** Make a new (anonymous) sort of arity 0. */ + TypeNode mkSort(uint32_t flags = SORT_FLAG_NONE); + + /** Make a new sort with the given name of arity 0. */ + TypeNode mkSort(const std::string& name, uint32_t flags = SORT_FLAG_NONE); + + /** Make a new sort by parameterizing the given sort constructor. */ + TypeNode mkSort(TypeNode constructor, + const std::vector& children, + uint32_t flags = SORT_FLAG_NONE); + + /** 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 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) + */ + TypeNode getType(TNode n, bool check = false); + + /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/ + void reclaimZombiesUntil(uint32_t k); + + /** Reclaims all zombies (if possible).*/ + void reclaimAllZombies(); + + /** Size of the node pool. */ + size_t poolSize() const; + + /** Deletes a list of attributes from the NM's AttributeManager.*/ + void deleteAttributes(const std::vector< const expr::attr::AttributeUniqueId* >& ids); + + /** + * 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! + */ + void debugHook(int debugFlag); +}; /* class NodeManager */ + +inline TypeNode NodeManager::mkArrayType(TypeNode indexType, + TypeNode constituentType) { + CheckArgument(!indexType.isNull(), indexType, + "unexpected NULL index type"); + CheckArgument(!constituentType.isNull(), constituentType, + "unexpected NULL constituent type"); + Debug("arrays") << "making array type " << indexType << " " + << constituentType << std::endl; + return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType); +} + +inline TypeNode NodeManager::mkSetType(TypeNode elementType) { + CheckArgument(!elementType.isNull(), elementType, + "unexpected NULL element type"); + Debug("sets") << "making sets type " << elementType << std::endl; + return mkTypeNode(kind::SET_TYPE, elementType); +} + +inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const { + NodeValuePool::const_iterator find = d_nodeValuePool.find(nv); + if(find == d_nodeValuePool.end()) { + return NULL; + } else { + return *find; + } +} + +inline void NodeManager::poolInsert(expr::NodeValue* nv) { + Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end()) + << "NodeValue already in the pool!"; + d_nodeValuePool.insert(nv);// FIXME multithreading +} + +inline void NodeManager::poolRemove(expr::NodeValue* nv) { + Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end()) + << "NodeValue is not in the pool!"; + + d_nodeValuePool.erase(nv);// FIXME multithreading +} + +inline Kind NodeManager::operatorToKind(TNode n) { + return kind::operatorToKind(n.d_nv); +} + +inline Node NodeManager::mkNode(Kind kind) +{ + NodeBuilder nb(this, kind); + return nb.constructNode(); +} + +inline Node NodeManager::mkNode(Kind kind, TNode child1) { + NodeBuilder nb(this, kind); + nb << child1; + return nb.constructNode(); +} + +inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) { + NodeBuilder nb(this, kind); + nb << child1 << child2; + return nb.constructNode(); +} + +inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, + TNode child3) { + NodeBuilder nb(this, kind); + nb << child1 << child2 << child3; + return nb.constructNode(); +} + +// N-ary version +template +inline Node NodeManager::mkNode(Kind kind, + const std::vector >& + children) { + NodeBuilder nb(this, kind); + nb.append(children); + return nb.constructNode(); +} + +template +Node NodeManager::mkAnd(const std::vector >& children) +{ + if (children.empty()) + { + return mkConst(true); + } + else if (children.size() == 1) + { + return children[0]; + } + return mkNode(kind::AND, children); +} + +template +Node NodeManager::mkOr(const std::vector >& children) +{ + if (children.empty()) + { + return mkConst(false); + } + else if (children.size() == 1) + { + return children[0]; + } + return mkNode(kind::OR, children); +} + +// for operators +inline Node NodeManager::mkNode(TNode opNode) { + NodeBuilder nb(this, operatorToKind(opNode)); + if(opNode.getKind() != kind::BUILTIN) { + nb << opNode; + } + return nb.constructNode(); +} + +inline Node NodeManager::mkNode(TNode opNode, TNode child1) { + NodeBuilder nb(this, operatorToKind(opNode)); + if(opNode.getKind() != kind::BUILTIN) { + nb << opNode; + } + nb << child1; + return nb.constructNode(); +} + +inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) { + NodeBuilder nb(this, operatorToKind(opNode)); + if(opNode.getKind() != kind::BUILTIN) { + nb << opNode; + } + nb << child1 << child2; + return nb.constructNode(); +} + +inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2, + TNode child3) { + NodeBuilder nb(this, operatorToKind(opNode)); + if(opNode.getKind() != kind::BUILTIN) { + nb << opNode; + } + nb << child1 << child2 << child3; + return nb.constructNode(); +} + +// N-ary version for operators +template +inline Node NodeManager::mkNode(TNode opNode, + const std::vector >& + children) { + NodeBuilder nb(this, operatorToKind(opNode)); + if(opNode.getKind() != kind::BUILTIN) { + nb << opNode; + } + nb.append(children); + return nb.constructNode(); +} + +inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1) { + return (NodeBuilder(this, kind) << child1).constructTypeNode(); +} + +inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1, + TypeNode child2) { + return (NodeBuilder(this, kind) << child1 << child2).constructTypeNode(); +} + +inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1, + TypeNode child2, TypeNode child3) { + return (NodeBuilder(this, kind) << child1 << child2 << child3) + .constructTypeNode(); +} + +// N-ary version for types +inline TypeNode NodeManager::mkTypeNode(Kind kind, + const std::vector& children) { + return NodeBuilder(this, kind).append(children).constructTypeNode(); +} + +// clang-format off +${metakind_mkConstDelete} +// clang-format off + +} // namespace cvc5 + +#endif /* CVC5__NODE_MANAGER_H */ diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index f577b4109..e496cf335 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -54,13 +54,13 @@ constant DIVISIBLE_OP \ sort REAL_TYPE \ Cardinality::REALS \ well-founded \ - "NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0))" \ + "NodeManager::currentNM()->mkConstReal(Rational(0))" \ "expr/node_manager.h" \ "real type" sort INTEGER_TYPE \ Cardinality::INTEGERS \ well-founded \ - "NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0))" \ + "NodeManager::currentNM()->mkConstInt(Rational(0))" \ "expr/node_manager.h" \ "integer type" @@ -73,7 +73,7 @@ constant CONST_RATIONAL \ constant CONST_INTEGER \ class \ - Rational \ + Rational+ \ ::cvc5::RationalHashFunction \ "util/rational.h" \ "a multiple-precision integer constant; payload is an instance of the cvc5::Rational class" diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 1ccb67490..634f27294 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -2089,7 +2089,7 @@ Node SequencesRewriter::rewriteUpdate(Node node) NodeManager* nm = NodeManager::currentNM(); Node idx = nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, s), - nm->mkNode(PLUS, i, nm->mkConst(Rational(1)))); + nm->mkNode(PLUS, i, nm->mkConstInt(Rational(1)))); Node ret = nm->mkNode(STRING_REV, nm->mkNode(STRING_UPDATE, s, idx, x)); return returnRewrite(node, ret, Rewrite::UPD_REV); } -- cgit v1.2.3