From: Andres Noetzli Date: Fri, 19 Nov 2021 22:23:39 +0000 (-0800) Subject: Clean up relationship of metakind and node_manager (#7649) X-Git-Tag: cvc5-1.0.0~794 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f324550c46da99333a43aacdd7b9651eb23fa6ca;p=cvc5.git Clean up relationship of metakind and node_manager (#7649) Before this commit, we were including `metakind.h` twice in `node_manager.h`, once without and once with defining `CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP`. Additionally, `mkmetakind` generated structs that mapped types to kinds. This commit makes all of this obsolete by directly generating instantiations of `mkConst`, which allows us to get rid of the double include and the `ConstantMap`. --- diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 45ce01edb..dcbc4aa97 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -49,7 +49,6 @@ libcvc5_add_sources( node_builder.h node_converter.cpp node_converter.h - node_manager.cpp node_manager.h node_manager_attributes.h node_self_iterator.h @@ -106,6 +105,7 @@ libcvc5_add_sources(GENERATED kind.h metakind.cpp metakind.h + node_manager.cpp type_checker.cpp type_properties.h ) @@ -168,6 +168,16 @@ add_custom_command( DEPENDS mkmetakind metakind_template.cpp metakind.h ${KINDS_FILES} ) +add_custom_command( + OUTPUT node_manager.cpp + COMMAND + ${mkmetakind_script} + ${CMAKE_CURRENT_LIST_DIR}/node_manager_template.cpp + ${KINDS_FILES} + > ${CMAKE_CURRENT_BINARY_DIR}/node_manager.cpp + DEPENDS mkmetakind node_manager_template.cpp node_manager.h ${KINDS_FILES} +) + add_custom_command( OUTPUT type_checker.cpp COMMAND @@ -184,6 +194,7 @@ add_custom_target(gen-expr kind.h metakind.cpp metakind.h + node_manager.cpp type_checker.cpp type_properties.h ) diff --git a/src/expr/metakind_template.cpp b/src/expr/metakind_template.cpp index 857a76889..d43c055d4 100644 --- a/src/expr/metakind_template.cpp +++ b/src/expr/metakind_template.cpp @@ -19,6 +19,7 @@ #include #include "expr/metakind.h" +#include "expr/node_manager.h" #include "expr/node_value.h" // clang-format off @@ -231,6 +232,7 @@ ${metakind_ubchildren} return ubs[k]; } + } // namespace metakind /** diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 935b65ab6..d049de4a5 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -25,6 +25,10 @@ namespace cvc5 { +// clang-format off +${metakind_fwd_decls} +// clang-format on + namespace expr { class NodeValue; } // namespace expr @@ -32,23 +36,6 @@ namespace expr { namespace kind { namespace metakind { -/** - * Static, compile-time information about types T representing cvc5 - * constants: - * - * typename ConstantMap::OwningTheory - * - * The theory in charge of constructing T when constructing Nodes - * with NodeManager::mkConst(T). - * - * typename ConstantMap::kind - * - * The kind to use when constructing Nodes with - * NodeManager::mkConst(T). - */ -template -struct ConstantMap; - struct NodeValueCompare { template static bool compare(const ::cvc5::expr::NodeValue* nv1, @@ -132,24 +119,3 @@ struct NodeValuePoolEq { } // namespace cvc5 #endif /* CVC5__KIND__METAKIND_H */ - -#ifdef CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP - -namespace cvc5 { - -// clang-format off -${metakind_fwd_decls} -// clang-format on - -namespace kind { -namespace metakind { - -// clang-format off -${metakind_constantMaps_decls} -// clang-format on - -} // namespace metakind -} // namespace kind -} // namespace cvc5 - -#endif /* CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP */ diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 9b3d5a776..d5f6d9b1a 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -53,6 +53,7 @@ metakind_constDeleters= metakind_ubchildren= metakind_lbchildren= metakind_operatorKinds= +metakind_mkConst= seen_theory=false seen_theory_builtin=false @@ -280,11 +281,22 @@ ${class} const& NodeValue::getConst< ${class} >() const { fi if [ "${skip_const_map}" != true ]; then - metakind_constantMaps_decls="${metakind_constantMaps_decls} -template <> -struct ConstantMap< ${class} > { - static constexpr Kind kind = ::cvc5::kind::$1; -};/* ConstantMap< ${class} > */ + metakind_mkConst="${metakind_mkConst} +template<> +Node NodeManager::mkConst<${class}>(const ${class}& val) +{ + return mkConstInternal(::cvc5::kind::$1, val); +} + +template<> +TypeNode NodeManager::mkTypeConst<${class}>(const ${class}& val) +{ + return mkConstInternal(::cvc5::kind::$1, val); +} +" + metakind_mkConst="${metakind_mkConst} +template +Node NodeManager::mkConst(Kind k, const ${class}& val); " fi @@ -422,7 +434,6 @@ for var in \ metakind_includes \ metakind_kinds \ metakind_constantMaps \ - metakind_constantMaps_decls \ metakind_compares \ metakind_constHashes \ metakind_constPrinters \ @@ -430,6 +441,7 @@ for var in \ metakind_ubchildren \ metakind_lbchildren \ metakind_operatorKinds \ + metakind_mkConst \ template \ ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp deleted file mode 100644 index 7b1c2de13..000000000 --- a/src/expr/node_manager.cpp +++ /dev/null @@ -1,1124 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Morgan Deters, Tim King - * - * 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 "expr/node_manager.h" - -#include -#include -#include -#include - -#include "base/check.h" -#include "base/listener.h" -#include "expr/attribute.h" -#include "expr/bound_var_manager.h" -#include "expr/datatype_index.h" -#include "expr/dtype.h" -#include "expr/dtype_cons.h" -#include "expr/metakind.h" -#include "expr/node_manager_attributes.h" -#include "expr/skolem_manager.h" -#include "expr/type_checker.h" -#include "theory/bags/bag_make_op.h" -#include "theory/sets/singleton_op.h" -#include "util/abstract_value.h" -#include "util/bitvector.h" -#include "util/rational.h" -#include "util/resource_manager.h" - -using namespace std; -using namespace cvc5::expr; - -namespace cvc5 { - -namespace { - -/** - * This class sets it reference argument to true and ensures that it gets set - * to false on destruction. This can be used to make sure a flag gets toggled - * in a function even on exceptional exit (e.g., see reclaimZombies()). - */ -struct ScopedBool { - bool& d_value; - - ScopedBool(bool& value) : - d_value(value) { - - Debug("gc") << ">> setting ScopedBool\n"; - d_value = true; - } - - ~ScopedBool() { - Debug("gc") << "<< clearing ScopedBool\n"; - d_value = false; - } -}; - -/** - * Similarly, ensure d_nodeUnderDeletion gets set to NULL even on - * exceptional exit from NodeManager::reclaimZombies(). - */ -struct NVReclaim { - NodeValue*& d_deletionField; - - NVReclaim(NodeValue*& deletionField) : - d_deletionField(deletionField) { - - Debug("gc") << ">> setting NVRECLAIM field\n"; - } - - ~NVReclaim() { - Debug("gc") << "<< clearing NVRECLAIM field\n"; - d_deletionField = NULL; - } -}; - -} // namespace - -namespace attr { - struct LambdaBoundVarListTag { }; - } // namespace attr - -// attribute that stores the canonical bound variable list for function types -typedef expr::Attribute LambdaBoundVarListAttr; - -NodeManager::NodeManager() - : d_skManager(new SkolemManager), - d_bvManager(new BoundVarManager), - d_initialized(false), - next_id(0), - d_attrManager(new expr::attr::AttributeManager()), - d_nodeUnderDeletion(nullptr), - d_inReclaimZombies(false), - d_abstractValueCount(0) -{ -} - -NodeManager* NodeManager::currentNM() -{ - thread_local static NodeManager nm; - return &nm; -} - -bool NodeManager::isNAryKind(Kind k) -{ - return kind::metakind::getMaxArityForKind(k) == expr::NodeValue::MAX_CHILDREN; -} - -TypeNode NodeManager::booleanType() -{ - return mkTypeConst(BOOLEAN_TYPE); -} - -TypeNode NodeManager::integerType() -{ - return mkTypeConst(INTEGER_TYPE); -} - -TypeNode NodeManager::realType() -{ - return mkTypeConst(REAL_TYPE); -} - -TypeNode NodeManager::stringType() -{ - return mkTypeConst(STRING_TYPE); -} - -TypeNode NodeManager::regExpType() -{ - return mkTypeConst(REGEXP_TYPE); -} - -TypeNode NodeManager::roundingModeType() -{ - return mkTypeConst(ROUNDINGMODE_TYPE); -} - -TypeNode NodeManager::boundVarListType() -{ - return mkTypeConst(BOUND_VAR_LIST_TYPE); -} - -TypeNode NodeManager::instPatternType() -{ - return mkTypeConst(INST_PATTERN_TYPE); -} - -TypeNode NodeManager::instPatternListType() -{ - return mkTypeConst(INST_PATTERN_LIST_TYPE); -} - -TypeNode NodeManager::builtinOperatorType() -{ - return mkTypeConst(BUILTIN_OPERATOR_TYPE); -} - -TypeNode NodeManager::mkBitVectorType(unsigned size) -{ - return mkTypeConst(BitVectorSize(size)); -} - -TypeNode NodeManager::sExprType() -{ - return mkTypeConst(SEXPR_TYPE); -} - -TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig) -{ - return mkTypeConst(FloatingPointSize(exp, sig)); -} - -TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs) -{ - return mkTypeConst(fs); -} - -void NodeManager::init() { - if (d_initialized) - { - return; - } - d_initialized = true; - - // Note: This code cannot be part of the constructor because it indirectly - // calls `NodeManager::currentNM()`, which is where the `NodeManager` is - // being constructed. - poolInsert( &expr::NodeValue::null() ); - - for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) { - Kind k = Kind(i); - - if(hasOperator(k)) { - d_operators[i] = mkConst(Kind(k)); - } - } -} - -NodeManager::~NodeManager() { - // Destroy skolem and bound var manager before cleaning up attributes and - // zombies - d_skManager = nullptr; - d_bvManager = nullptr; - - { - ScopedBool dontGC(d_inReclaimZombies); - // By this point, all SolverEngines should have been deleted, along with - // all their attributes - d_attrManager->deleteAllAttributes(); - } - - for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) { - d_operators[i] = Node::null(); - } - - d_unique_vars.clear(); - - TypeNode dummy; - d_tt_cache.d_children.clear(); - d_tt_cache.d_data = dummy; - d_rt_cache.d_children.clear(); - d_rt_cache.d_data = dummy; - - // clear the datatypes - d_dtypes.clear(); - - Assert(!d_attrManager->inGarbageCollection()); - - std::vector order = TopologicalSort(d_maxedOut); - d_maxedOut.clear(); - - while (!d_zombies.empty() || !order.empty()) { - if (d_zombies.empty()) { - // Delete the maxed out nodes in toplogical order once we know - // there are no additional zombies, or other nodes to worry about. - Assert(!order.empty()); - // We process these in reverse to reverse the topological order. - NodeValue* greatest_maxed_out = order.back(); - order.pop_back(); - Assert(greatest_maxed_out->HasMaximizedReferenceCount()); - Debug("gc") << "Force zombify " << greatest_maxed_out << std::endl; - greatest_maxed_out->d_rc = 0; - markForDeletion(greatest_maxed_out); - } else { - reclaimZombies(); - } - } - - if (d_initialized) - { - poolRemove(&expr::NodeValue::null()); - } - - if(Debug.isOn("gc:leaks")) { - Debug("gc:leaks") << "still in pool:" << endl; - for(NodeValuePool::const_iterator i = d_nodeValuePool.begin(), - iend = d_nodeValuePool.end(); - i != iend; - ++i) { - Debug("gc:leaks") << " " << *i - << " id=" << (*i)->d_id - << " rc=" << (*i)->d_rc - << " " << **i << endl; - } - Debug("gc:leaks") << ":end:" << endl; - } - - // defensive coding, in case destruction-order issues pop up (they often do) - delete d_attrManager; - d_attrManager = NULL; -} - -const DType& NodeManager::getDTypeForIndex(size_t index) const -{ - // if this assertion fails, it is likely due to not managing datatypes - // properly w.r.t. multiple NodeManagers. - Assert(index < d_dtypes.size()); - return *d_dtypes[index]; -} - -void NodeManager::reclaimZombies() { - // FIXME multithreading - Assert(!d_attrManager->inGarbageCollection()); - - Debug("gc") << "reclaiming " << d_zombies.size() << " zombie(s)!\n"; - - // during reclamation, reclaimZombies() is never supposed to be called - Assert(!d_inReclaimZombies) - << "NodeManager::reclaimZombies() not re-entrant!"; - - // whether exit is normal or exceptional, the Reclaim dtor is called - // and ensures that d_inReclaimZombies is set back to false. - ScopedBool r(d_inReclaimZombies); - - // We copy the set away and clear the NodeManager's set of zombies. - // This is because reclaimZombie() decrements the RC of the - // NodeValue's children, which may (recursively) reclaim them. - // - // Let's say we're reclaiming zombie NodeValue "A" and its child "B" - // then becomes a zombie (NodeManager::markForDeletion(B) is called). - // - // One way to handle B's zombification would be simply to put it - // into d_zombies. This is what we do. However, if we were to - // concurrently process d_zombies in the loop below, such addition - // may be invisible to us (B is leaked) or even invalidate our - // iterator, causing a crash. So we need to copy the set away. - - vector zombies; - zombies.reserve(d_zombies.size()); - remove_copy_if(d_zombies.begin(), - d_zombies.end(), - back_inserter(zombies), - NodeValueReferenceCountNonZero()); - d_zombies.clear(); - -#ifdef _LIBCPP_VERSION - NodeValue* last = NULL; -#endif - for(vector::iterator i = zombies.begin(); - i != zombies.end(); - ++i) { - NodeValue* nv = *i; -#ifdef _LIBCPP_VERSION - // Work around an apparent bug in libc++'s hash_set<> which can - // (very occasionally) have an element repeated. - if(nv == last) { - continue; - } - last = nv; -#endif - - // collect ONLY IF still zero - if(nv->d_rc == 0) { - if(Debug.isOn("gc")) { - Debug("gc") << "deleting node value " << nv - << " [" << nv->d_id << "]: "; - nv->printAst(Debug("gc")); - Debug("gc") << endl; - } - - // remove from the pool - kind::MetaKind mk = nv->getMetaKind(); - if(mk != kind::metakind::VARIABLE && mk != kind::metakind::NULLARY_OPERATOR) { - poolRemove(nv); - } - - // whether exit is normal or exceptional, the NVReclaim dtor is - // called and ensures that d_nodeUnderDeletion is set back to - // NULL. - NVReclaim rc(d_nodeUnderDeletion); - d_nodeUnderDeletion = nv; - - // remove attributes - { // notify listeners of deleted node - TNode n; - n.d_nv = nv; - nv->d_rc = 1; // so that TNode doesn't assert-fail - // this would mean that one of the listeners stowed away - // a reference to this node! - Assert(nv->d_rc == 1); - } - nv->d_rc = 0; - d_attrManager->deleteAllAttributes(nv); - - // decr ref counts of children - nv->decrRefCounts(); - if(mk == kind::metakind::CONSTANT) { - // Destroy (call the destructor for) the C++ type representing - // the constant in this NodeValue. This is needed for - // e.g. cvc5::Rational, since it has a gmp internal - // representation that mallocs memory and should be cleaned - // up. (This won't delete a pointer value if used as a - // constant, but then, you should probably use a smart-pointer - // type for a constant payload.) - kind::metakind::deleteNodeValueConstant(nv); - } - free(nv); - } - } -}/* NodeManager::reclaimZombies() */ - -std::vector NodeManager::TopologicalSort( - const std::vector& roots) { - std::vector order; - // The stack of nodes to visit. The Boolean value is false when visiting the - // node in preorder and true when visiting it in postorder. - std::vector > stack; - // Nodes that have been visited in both pre- and postorder - NodeValueIDSet visited; - const NodeValueIDSet root_set(roots.begin(), roots.end()); - - for (size_t index = 0; index < roots.size(); index++) { - NodeValue* root = roots[index]; - if (visited.find(root) == visited.end()) { - stack.push_back(std::make_pair(false, root)); - } - while (!stack.empty()) { - NodeValue* current = stack.back().second; - const bool visited_children = stack.back().first; - Debug("gc") << "Topological sort " << current << " " << visited_children - << std::endl; - if (visited_children) { - if (root_set.find(current) != root_set.end()) { - order.push_back(current); - } - stack.pop_back(); - } - else if (visited.find(current) == visited.end()) - { - stack.back().first = true; - visited.insert(current); - for (unsigned i = 0; i < current->getNumChildren(); ++i) { - expr::NodeValue* child = current->getChild(i); - stack.push_back(std::make_pair(false, child)); - } - } - else - { - stack.pop_back(); - } - } - } - Assert(order.size() == roots.size()); - return order; -} /* NodeManager::TopologicalSort() */ - -TypeNode NodeManager::getType(TNode n, bool check) -{ - TypeNode typeNode; - bool hasType = getAttribute(n, TypeAttr(), typeNode); - bool needsCheck = check && !getAttribute(n, TypeCheckedAttr()); - - - Debug("getType") << this << " getting type for " << &n << " " << n << ", check=" << check << ", needsCheck = " << needsCheck << ", hasType = " << hasType << endl; - -#ifdef CVC5_DEBUG - // already did type check eagerly upon creation in node builder - bool doTypeCheck = false; -#else - bool doTypeCheck = true; -#endif - if (needsCheck && doTypeCheck) - { - /* Iterate and compute the children bottom up. This avoids stack - overflows in computeType() when the Node graph is really deep, - which should only affect us when we're type checking lazily. */ - stack worklist; - worklist.push(n); - - while( !worklist.empty() ) { - TNode m = worklist.top(); - - bool readyToCompute = true; - - for( TNode::iterator it = m.begin(), end = m.end(); - it != end; - ++it ) { - if( !hasAttribute(*it, TypeAttr()) - || (check && !getAttribute(*it, TypeCheckedAttr())) ) { - readyToCompute = false; - worklist.push(*it); - } - } - - if( readyToCompute ) { - Assert(check || m.getMetaKind() != kind::metakind::NULLARY_OPERATOR); - /* All the children have types, time to compute */ - typeNode = TypeChecker::computeType(this, m, check); - worklist.pop(); - } - } // end while - - /* Last type computed in loop should be the type of n */ - Assert(typeNode == getAttribute(n, TypeAttr())); - } else if( !hasType || needsCheck ) { - /* We can compute the type top-down, without worrying about - deep recursion. */ - Assert(check || n.getMetaKind() != kind::metakind::NULLARY_OPERATOR); - typeNode = TypeChecker::computeType(this, n, check); - } - - /* The type should be have been computed and stored. */ - Assert(hasAttribute(n, TypeAttr())); - /* The check should have happened, if we asked for it. */ - Assert(!check || getAttribute(n, TypeCheckedAttr())); - - Debug("getType") << "type of " << &n << " " << n << " is " << typeNode << endl; - return typeNode; -} - -TypeNode NodeManager::mkBagType(TypeNode elementType) -{ - CheckArgument( - !elementType.isNull(), elementType, "unexpected NULL element type"); - Debug("bags") << "making bags type " << elementType << std::endl; - return mkTypeNode(kind::BAG_TYPE, elementType); -} - -TypeNode NodeManager::mkSequenceType(TypeNode elementType) -{ - CheckArgument( - !elementType.isNull(), elementType, "unexpected NULL element type"); - return mkTypeNode(kind::SEQUENCE_TYPE, elementType); -} - -TypeNode NodeManager::mkDatatypeType(DType& datatype, uint32_t flags) -{ - // Not worth a special implementation; this doesn't need to be fast - // code anyway. - std::vector datatypes; - datatypes.push_back(datatype); - std::vector result = mkMutualDatatypeTypes(datatypes, flags); - Assert(result.size() == 1); - return result.front(); -} - -std::vector NodeManager::mkMutualDatatypeTypes( - const std::vector& datatypes, uint32_t flags) -{ - std::set unresolvedTypes; - return mkMutualDatatypeTypes(datatypes, unresolvedTypes, flags); -} - -std::vector NodeManager::mkMutualDatatypeTypes( - const std::vector& datatypes, - const std::set& unresolvedTypes, - uint32_t flags) -{ - std::map nameResolutions; - std::vector dtts; - - // First do some sanity checks, set up the final Type to be used for - // each datatype, and set up the "named resolutions" used to handle - // simple self- and mutual-recursion, for example in the definition - // "nat = succ(pred:nat) | zero", a named resolution can handle the - // pred selector. - for (const DType& dt : datatypes) - { - uint32_t index = d_dtypes.size(); - d_dtypes.push_back(std::unique_ptr(new DType(dt))); - DType* dtp = d_dtypes.back().get(); - TypeNode typeNode; - if (dtp->getNumParameters() == 0) - { - typeNode = mkTypeConst(DatatypeIndexConstant(index)); - } - else - { - TypeNode cons = mkTypeConst(DatatypeIndexConstant(index)); - std::vector params; - params.push_back(cons); - for (uint32_t ip = 0; ip < dtp->getNumParameters(); ++ip) - { - params.push_back(dtp->getParameter(ip)); - } - - typeNode = mkTypeNode(kind::PARAMETRIC_DATATYPE, params); - } - if (nameResolutions.find(dtp->getName()) != nameResolutions.end()) - { - throw Exception( - "cannot construct two datatypes at the same time with the same name"); - } - nameResolutions.insert(std::make_pair(dtp->getName(), typeNode)); - dtts.push_back(typeNode); - } - - // Second, set up the type substitution map for complex type - // resolution (e.g. if "list" is the type we're defining, and it has - // a selector of type "ARRAY INT OF list", this can't be taken care - // of using the named resolutions that we set up above. A - // preliminary array type was set up, and now needs to have "list" - // substituted in it for the correct type. - // - // @TODO get rid of named resolutions altogether and handle - // everything with these resolutions? - std::vector paramTypes; - std::vector paramReplacements; - std::vector placeholders; // to hold the "unresolved placeholders" - std::vector replacements; // to hold our final, resolved types - for (const TypeNode& ut : unresolvedTypes) - { - std::string name = ut.getAttribute(expr::VarNameAttr()); - std::map::const_iterator resolver = - nameResolutions.find(name); - if (resolver == nameResolutions.end()) - { - throw Exception("cannot resolve type " + name - + "; it's not among the datatypes being defined"); - } - // We will instruct the Datatype to substitute "ut" (the - // unresolved SortType used as a placeholder in complex types) - // with "(*resolver).second" (the TypeNode we created in the - // first step, above). - if (ut.isSort()) - { - placeholders.push_back(ut); - replacements.push_back((*resolver).second); - } - else - { - Assert(ut.isSortConstructor()); - paramTypes.push_back(ut); - paramReplacements.push_back((*resolver).second); - } - } - - // Lastly, perform the final resolutions and checks. - for (const TypeNode& ut : dtts) - { - const DType& dt = ut.getDType(); - if (!dt.isResolved()) - { - const_cast(dt).resolve(nameResolutions, - placeholders, - replacements, - paramTypes, - paramReplacements); - } - // Check the datatype has been resolved properly. - for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) - { - const DTypeConstructor& c = dt[i]; - TypeNode testerType CVC5_UNUSED = c.getTester().getType(); - Assert(c.isResolved() && testerType.isTester() && testerType[0] == ut) - << "malformed tester in datatype post-resolution"; - TypeNode ctorType CVC5_UNUSED = c.getConstructor().getType(); - Assert(ctorType.isConstructor() - && ctorType.getNumChildren() == c.getNumArgs() + 1 - && ctorType.getRangeType() == ut) - << "malformed constructor in datatype post-resolution"; - // for all selectors... - for (size_t j = 0, nargs = c.getNumArgs(); j < nargs; j++) - { - const DTypeSelector& a = c[j]; - TypeNode selectorType = a.getType(); - Assert(a.isResolved() && selectorType.isSelector() - && selectorType[0] == ut) - << "malformed selector in datatype post-resolution"; - // This next one's a "hard" check, performed in non-debug builds - // as well; the other ones should all be guaranteed by the - // cvc5::DType class, but this actually needs to be checked. - if (selectorType.getRangeType().isFunctionLike()) - { - throw Exception("cannot put function-like things in datatypes"); - } - } - } - } - - return dtts; -} - -TypeNode NodeManager::mkConstructorType(const std::vector& args, - TypeNode range) -{ - std::vector sorts = args; - sorts.push_back(range); - return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts); -} - -TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) -{ - CheckArgument( - domain.isDatatype(), domain, "cannot create non-datatype selector type"); - return mkTypeNode(kind::SELECTOR_TYPE, domain, range); -} - -TypeNode NodeManager::mkTesterType(TypeNode domain) -{ - CheckArgument( - domain.isDatatype(), domain, "cannot create non-datatype tester"); - return mkTypeNode(kind::TESTER_TYPE, domain); -} - -TypeNode NodeManager::mkDatatypeUpdateType(TypeNode domain, TypeNode range) -{ - CheckArgument( - domain.isDatatype(), domain, "cannot create non-datatype upater type"); - // It is a function type domain x range -> domain, we store only the - // arguments - return mkTypeNode(kind::UPDATER_TYPE, domain, range); -} - -TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) { - if( index==types.size() ){ - if( d_data.isNull() ){ - std::stringstream sst; - sst << "__cvc5_tuple"; - for (unsigned i = 0; i < types.size(); ++ i) { - sst << "_" << types[i]; - } - DType dt(sst.str()); - dt.setTuple(); - std::stringstream ssc; - ssc << sst.str() << "_ctor"; - std::shared_ptr c = - std::make_shared(ssc.str()); - for (unsigned i = 0; i < types.size(); ++ i) { - std::stringstream ss; - ss << sst.str() << "_stor_" << i; - c->addArg(ss.str().c_str(), types[i]); - } - dt.addConstructor(c); - d_data = nm->mkDatatypeType(dt); - Debug("tuprec-debug") << "Return type : " << d_data << std::endl; - } - return d_data; - }else{ - return d_children[types[index]].getTupleType( nm, types, index+1 ); - } -} - -TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Record& rec, unsigned index ) { - if (index == rec.size()) - { - if( d_data.isNull() ){ - std::stringstream sst; - sst << "__cvc5_record"; - for (const std::pair& i : rec) - { - sst << "_" << i.first << "_" << i.second; - } - DType dt(sst.str()); - dt.setRecord(); - std::stringstream ssc; - ssc << sst.str() << "_ctor"; - std::shared_ptr c = - std::make_shared(ssc.str()); - for (const std::pair& i : rec) - { - c->addArg(i.first, i.second); - } - dt.addConstructor(c); - d_data = nm->mkDatatypeType(dt); - Debug("tuprec-debug") << "Return type : " << d_data << std::endl; - } - return d_data; - } - return d_children[rec[index].second][rec[index].first].getRecordType( - nm, rec, index + 1); -} - -TypeNode NodeManager::mkFunctionType(const std::vector& sorts) -{ - Assert(sorts.size() >= 2); - return mkTypeNode(kind::FUNCTION_TYPE, sorts); -} - -TypeNode NodeManager::mkPredicateType(const std::vector& sorts) -{ - Assert(sorts.size() >= 1); - std::vector sortNodes; - sortNodes.insert(sortNodes.end(), sorts.begin(), sorts.end()); - sortNodes.push_back(booleanType()); - return mkFunctionType(sortNodes); -} - -TypeNode NodeManager::mkFunctionType(const TypeNode& domain, - const TypeNode& range) -{ - std::vector sorts; - sorts.push_back(domain); - sorts.push_back(range); - return mkFunctionType(sorts); -} - -TypeNode NodeManager::mkFunctionType(const std::vector& argTypes, - const TypeNode& range) -{ - Assert(argTypes.size() >= 1); - std::vector sorts(argTypes); - sorts.push_back(range); - return mkFunctionType(sorts); -} - -TypeNode NodeManager::mkTupleType(const std::vector& types) { - std::vector< TypeNode > ts; - Debug("tuprec-debug") << "Make tuple type : "; - for (unsigned i = 0; i < types.size(); ++ i) { - CheckArgument(!types[i].isFunctionLike(), types, "cannot put function-like types in tuples"); - ts.push_back( types[i] ); - Debug("tuprec-debug") << types[i] << " "; - } - Debug("tuprec-debug") << std::endl; - return d_tt_cache.getTupleType( this, ts ); -} - -TypeNode NodeManager::mkRecordType(const Record& rec) { - return d_rt_cache.getRecordType( this, rec ); -} - -void NodeManager::reclaimAllZombies(){ - reclaimZombiesUntil(0u); -} - -/** Reclaim zombies while there are more than k nodes in the pool (if possible).*/ -void NodeManager::reclaimZombiesUntil(uint32_t k){ - if(safeToReclaimZombies()){ - while(poolSize() >= k && !d_zombies.empty()){ - reclaimZombies(); - } - } -} - -size_t NodeManager::poolSize() const{ - return d_nodeValuePool.size(); -} - -TypeNode NodeManager::mkSort(uint32_t flags) { - NodeBuilder nb(this, kind::SORT_TYPE); - Node sortTag = NodeBuilder(this, kind::SORT_TAG); - nb << sortTag; - return nb.constructTypeNode(); -} - -TypeNode NodeManager::mkSort(const std::string& name, uint32_t flags) { - NodeBuilder nb(this, kind::SORT_TYPE); - Node sortTag = NodeBuilder(this, kind::SORT_TAG); - nb << sortTag; - TypeNode tn = nb.constructTypeNode(); - setAttribute(tn, expr::VarNameAttr(), name); - return tn; -} - -TypeNode NodeManager::mkSort(TypeNode constructor, - const std::vector& children, - uint32_t flags) { - Assert(constructor.getKind() == kind::SORT_TYPE - && constructor.getNumChildren() == 0) - << "expected a sort constructor"; - Assert(children.size() > 0) << "expected non-zero # of children"; - Assert(hasAttribute(constructor.d_nv, expr::SortArityAttr()) - && hasAttribute(constructor.d_nv, expr::VarNameAttr())) - << "expected a sort constructor"; - std::string name = getAttribute(constructor.d_nv, expr::VarNameAttr()); - Assert(getAttribute(constructor.d_nv, expr::SortArityAttr()) - == children.size()) - << "arity mismatch in application of sort constructor"; - NodeBuilder nb(this, kind::SORT_TYPE); - Node sortTag = Node(constructor.d_nv->d_children[0]); - nb << sortTag; - nb.append(children); - TypeNode type = nb.constructTypeNode(); - setAttribute(type, expr::VarNameAttr(), name); - return type; -} - -TypeNode NodeManager::mkSortConstructor(const std::string& name, - size_t arity, - uint32_t flags) -{ - Assert(arity > 0); - NodeBuilder nb(this, kind::SORT_TYPE); - Node sortTag = NodeBuilder(this, kind::SORT_TAG); - nb << sortTag; - TypeNode type = nb.constructTypeNode(); - setAttribute(type, expr::VarNameAttr(), name); - setAttribute(type, expr::SortArityAttr(), arity); - return type; -} - -Node NodeManager::mkVar(const std::string& name, const TypeNode& type) -{ - Node n = NodeBuilder(this, kind::VARIABLE); - setAttribute(n, TypeAttr(), type); - setAttribute(n, TypeCheckedAttr(), true); - setAttribute(n, expr::VarNameAttr(), name); - return n; -} - -Node NodeManager::mkBoundVar(const std::string& name, const TypeNode& type) { - Node n = mkBoundVar(type); - setAttribute(n, expr::VarNameAttr(), name); - return n; -} - -Node NodeManager::getBoundVarListForFunctionType( TypeNode tn ) { - Assert(tn.isFunction()); - Node bvl = tn.getAttribute(LambdaBoundVarListAttr()); - if( bvl.isNull() ){ - std::vector< Node > vars; - for( unsigned i=0; i& children) -{ - AlwaysAssert(kind::isAssociative(kind)) << "Illegal kind in mkAssociative"; - - const unsigned int max = kind::metakind::getMaxArityForKind(kind); - size_t numChildren = children.size(); - - /* If the number of children is within bounds, then there's nothing to do. */ - if (numChildren <= max) - { - return mkNode(kind, children); - } - const unsigned int min = kind::metakind::getMinArityForKind(kind); - - std::vector::const_iterator it = children.begin(); - std::vector::const_iterator end = children.end(); - - /* The new top-level children and the children of each sub node */ - std::vector newChildren; - std::vector subChildren; - - while (it != end && numChildren > max) - { - /* Grab the next max children and make a node for them. */ - for (std::vector::const_iterator next = it + max; it != next; - ++it, --numChildren) - { - subChildren.push_back(*it); - } - Node subNode = mkNode(kind, subChildren); - newChildren.push_back(subNode); - - subChildren.clear(); - } - - // add the leftover children - if (numChildren > 0) - { - for (; it != end; ++it) - { - newChildren.push_back(*it); - } - } - - /* It would be really weird if this happened (it would require - * min > 2, for one thing), but let's make sure. */ - AlwaysAssert(newChildren.size() >= min) - << "Too few new children in mkAssociative"; - - // recurse - return mkAssociative(kind, newChildren); -} - -Node NodeManager::mkLeftAssociative(Kind kind, - const std::vector& children) -{ - Node n = children[0]; - for (size_t i = 1, size = children.size(); i < size; i++) - { - n = mkNode(kind, n, children[i]); - } - return n; -} - -Node NodeManager::mkRightAssociative(Kind kind, - const std::vector& children) -{ - Node n = children[children.size() - 1]; - for (size_t i = children.size() - 1; i > 0;) - { - n = mkNode(kind, children[--i], n); - } - return n; -} - -Node NodeManager::mkChain(Kind kind, const std::vector& children) -{ - if (children.size() == 2) - { - // if this is the case exactly 1 pair will be generated so the - // AND is not required - return mkNode(kind, children[0], children[1]); - } - std::vector cchildren; - for (size_t i = 0, nargsmo = children.size() - 1; i < nargsmo; i++) - { - cchildren.push_back(mkNode(kind, children[i], children[i + 1])); - } - return mkNode(kind::AND, cchildren); -} - -Node NodeManager::mkVar(const TypeNode& type) -{ - Node n = NodeBuilder(this, kind::VARIABLE); - setAttribute(n, TypeAttr(), type); - setAttribute(n, TypeCheckedAttr(), true); - return n; -} - -Node NodeManager::mkBoundVar(const TypeNode& type) { - Node n = NodeBuilder(this, kind::BOUND_VARIABLE); - setAttribute(n, TypeAttr(), type); - setAttribute(n, TypeCheckedAttr(), true); - return n; -} - -Node NodeManager::mkInstConstant(const TypeNode& type) { - Node n = NodeBuilder(this, kind::INST_CONSTANT); - n.setAttribute(TypeAttr(), type); - n.setAttribute(TypeCheckedAttr(), true); - return n; -} - -Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) { - std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type ); - if( it==d_unique_vars[k].end() ){ - Node n = NodeBuilder(this, k).constructNode(); - setAttribute(n, TypeAttr(), type); - //setAttribute(n, TypeCheckedAttr(), true); - d_unique_vars[k][type] = n; - Assert(n.getMetaKind() == kind::metakind::NULLARY_OPERATOR); - return n; - }else{ - return it->second; - } -} - -Node NodeManager::mkSingleton(const TypeNode& t, const TNode n) -{ - Assert(n.getType().isSubtypeOf(t)) - << "Invalid operands for mkSingleton. The type '" << n.getType() - << "' of node '" << n << "' is not a subtype of '" << t << "'." - << std::endl; - Node op = mkConst(SetSingletonOp(t)); - Node singleton = mkNode(kind::SET_SINGLETON, op, n); - return singleton; -} - -Node NodeManager::mkBag(const TypeNode& t, const TNode n, const TNode m) -{ - Assert(n.getType().isSubtypeOf(t)) - << "Invalid operands for mkBag. The type '" << n.getType() - << "' of node '" << n << "' is not a subtype of '" << t << "'." - << std::endl; - Node op = mkConst(BagMakeOp(t)); - Node bag = mkNode(kind::BAG_MAKE, op, n, m); - return bag; -} - -Node NodeManager::mkAbstractValue(const TypeNode& type) { - Node n = mkConst(AbstractValue(++d_abstractValueCount)); - n.setAttribute(TypeAttr(), type); - n.setAttribute(TypeCheckedAttr(), true); - return n; -} - -bool NodeManager::safeToReclaimZombies() const{ - // FIXME multithreading - return !d_inReclaimZombies && !d_attrManager->inGarbageCollection(); -} - -void NodeManager::deleteAttributes(const std::vector& ids){ - d_attrManager->deleteAttributes(ids); -} - -void NodeManager::debugHook(int debugFlag){ - // For debugging purposes only, DO NOT CHECK IN ANY CODE! -} - -Kind NodeManager::getKindForFunction(TNode fun) -{ - TypeNode tn = fun.getType(); - if (tn.isFunction()) - { - return kind::APPLY_UF; - } - else if (tn.isConstructor()) - { - return kind::APPLY_CONSTRUCTOR; - } - else if (tn.isSelector()) - { - return kind::APPLY_SELECTOR; - } - else if (tn.isTester()) - { - return kind::APPLY_TESTER; - } - return kind::UNDEFINED_KIND; -} - -Node NodeManager::mkNode(Kind kind, std::initializer_list children) -{ - NodeBuilder nb(this, kind); - nb.append(children.begin(), children.end()); - return nb.constructNode(); -} - -Node NodeManager::mkNode(TNode opNode, std::initializer_list children) -{ - NodeBuilder nb(this, operatorToKind(opNode)); - if (opNode.getKind() != kind::BUILTIN) - { - nb << opNode; - } - nb.append(children.begin(), children.end()); - return nb.constructNode(); -} - -Node NodeManager::mkConstReal(const Rational& r) -{ - return mkConst(kind::CONST_RATIONAL, r); -} - -Node NodeManager::mkConstInt(const Rational& r) -{ - // !!!! Note will update to CONST_INTEGER. - return mkConst(kind::CONST_RATIONAL, r); -} - -} // namespace cvc5 diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index f3dc1c1df..5b74b04e1 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -16,7 +16,6 @@ #include "cvc5_private.h" /* circular dependency; force node.h first */ -//#include "expr/attribute.h" #include "expr/node.h" #include "expr/type_node.h" @@ -29,7 +28,7 @@ #include "base/check.h" #include "expr/kind.h" -#include "expr/metakind.h" +#include "expr/node_builder.h" #include "expr/node_value.h" #include "util/floatingpoint_size.h" @@ -561,19 +560,14 @@ class NodeManager * Determine whether Nodes of a particular Kind have operators. * @returns true if Nodes of Kind k have operators. */ - static inline bool hasOperator(Kind k); + 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. */ - inline TNode operatorOf(Kind k) { - AssertArgument( kind::metaKindOf(k) == kind::metakind::OPERATOR, k, - "Kind is not an OPERATOR-kinded kind " - "in NodeManager::operatorOf()" ); - return d_operators[k]; - } + TNode operatorOf(Kind k); /** * Retrieve an attribute for a node. @@ -1038,37 +1032,6 @@ inline void NodeManager::poolRemove(expr::NodeValue* nv) { d_nodeValuePool.erase(nv);// FIXME multithreading } -} // namespace cvc5 - -#define CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP -#include "expr/metakind.h" -#undef CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP - -#include "expr/node_builder.h" - -namespace cvc5 { - -// general expression-builders - -inline bool NodeManager::hasOperator(Kind k) { - switch(kind::MetaKind mk = kind::metaKindOf(k)) { - - case kind::metakind::INVALID: - case kind::metakind::VARIABLE: - case kind::metakind::NULLARY_OPERATOR: - return false; - - case kind::metakind::OPERATOR: - case kind::metakind::PARAMETERIZED: - return true; - - case kind::metakind::CONSTANT: - return false; - - default: Unhandled() << mk; - } -} - inline Kind NodeManager::operatorToKind(TNode n) { return kind::operatorToKind(n.d_nv); } @@ -1207,75 +1170,6 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind, return NodeBuilder(this, kind).append(children).constructTypeNode(); } -template -Node NodeManager::mkConst(const T& val) { - return mkConstInternal(kind::metakind::ConstantMap::kind, val); -} - -template -Node NodeManager::mkConst(Kind k, const T& val) -{ - return mkConstInternal(k, val); -} - -template -TypeNode NodeManager::mkTypeConst(const T& val) { - return mkConstInternal(kind::metakind::ConstantMap::kind, - val); -} - -template -NodeClass NodeManager::mkConstInternal(Kind k, const T& val) -{ - NVStorage<1> nvStorage; - expr::NodeValue& nvStack = reinterpret_cast(nvStorage); - - nvStack.d_id = 0; - nvStack.d_kind = k; - nvStack.d_rc = 0; - nvStack.d_nchildren = 1; - -#if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6)) -#pragma GCC diagnostic push -#pragma GCC diagnostic ignored "-Warray-bounds" -#endif - - nvStack.d_children[0] = - const_cast(reinterpret_cast(&val)); - expr::NodeValue* nv = poolLookup(&nvStack); - -#if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6)) -#pragma GCC diagnostic pop -#endif - - if(nv != NULL) { - return NodeClass(nv); - } - - nv = (expr::NodeValue*) - std::malloc(sizeof(expr::NodeValue) + sizeof(T)); - if(nv == NULL) { - throw std::bad_alloc(); - } - - nv->d_nchildren = 0; - nv->d_kind = k; - nv->d_id = next_id++;// FIXME multithreading - nv->d_rc = 0; - - new (&nv->d_children) T(val); - - poolInsert(nv); - if(Debug.isOn("gc")) { - Debug("gc") << "creating node value " << nv - << " [" << nv->d_id << "]: "; - nv->printAst(Debug("gc")); - Debug("gc") << std::endl; - } - - return NodeClass(nv); -} - } // namespace cvc5 #endif /* CVC5__NODE_MANAGER_H */ diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp new file mode 100644 index 000000000..06f5bcfb6 --- /dev/null +++ b/src/expr/node_manager_template.cpp @@ -0,0 +1,1287 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, Tim King + * + * 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 +#include +#include +#include + +#include "base/check.h" +#include "base/listener.h" +#include "expr/attribute.h" +#include "expr/bound_var_manager.h" +#include "expr/datatype_index.h" +#include "expr/dtype.h" +#include "expr/dtype_cons.h" +#include "expr/metakind.h" +#include "expr/node_manager.h" +#include "expr/node_manager_attributes.h" +#include "expr/skolem_manager.h" +#include "expr/type_checker.h" +#include "theory/bags/bag_make_op.h" +#include "theory/sets/singleton_op.h" +#include "util/abstract_value.h" +#include "util/bitvector.h" +#include "util/rational.h" +#include "util/resource_manager.h" + +// clang-format off +${metakind_includes} +// clang-format off + +using namespace std; +using namespace cvc5::expr; + +namespace cvc5 { + +namespace { + +/** + * This class sets it reference argument to true and ensures that it gets set + * to false on destruction. This can be used to make sure a flag gets toggled + * in a function even on exceptional exit (e.g., see reclaimZombies()). + */ +struct ScopedBool { + bool& d_value; + + ScopedBool(bool& value) : + d_value(value) { + + Debug("gc") << ">> setting ScopedBool\n"; + d_value = true; + } + + ~ScopedBool() { + Debug("gc") << "<< clearing ScopedBool\n"; + d_value = false; + } +}; + +/** + * Similarly, ensure d_nodeUnderDeletion gets set to NULL even on + * exceptional exit from NodeManager::reclaimZombies(). + */ +struct NVReclaim { + NodeValue*& d_deletionField; + + NVReclaim(NodeValue*& deletionField) : + d_deletionField(deletionField) { + + Debug("gc") << ">> setting NVRECLAIM field\n"; + } + + ~NVReclaim() { + Debug("gc") << "<< clearing NVRECLAIM field\n"; + d_deletionField = NULL; + } +}; + +} // namespace + +// clang-format off +${metakind_mkConst} +// clang-format on + +namespace attr { +struct LambdaBoundVarListTag +{ +}; +} // namespace attr + +// attribute that stores the canonical bound variable list for function types +typedef expr::Attribute + LambdaBoundVarListAttr; + +NodeManager::NodeManager() + : d_skManager(new SkolemManager), + d_bvManager(new BoundVarManager), + d_initialized(false), + next_id(0), + d_attrManager(new expr::attr::AttributeManager()), + d_nodeUnderDeletion(nullptr), + d_inReclaimZombies(false), + d_abstractValueCount(0) +{ +} + +NodeManager* NodeManager::currentNM() +{ + thread_local static NodeManager nm; + return &nm; +} + +bool NodeManager::isNAryKind(Kind k) +{ + return kind::metakind::getMaxArityForKind(k) == expr::NodeValue::MAX_CHILDREN; +} + +TypeNode NodeManager::booleanType() +{ + return mkTypeConst(BOOLEAN_TYPE); +} + +TypeNode NodeManager::integerType() +{ + return mkTypeConst(INTEGER_TYPE); +} + +TypeNode NodeManager::realType() +{ + return mkTypeConst(REAL_TYPE); +} + +TypeNode NodeManager::stringType() +{ + return mkTypeConst(STRING_TYPE); +} + +TypeNode NodeManager::regExpType() +{ + return mkTypeConst(REGEXP_TYPE); +} + +TypeNode NodeManager::roundingModeType() +{ + return mkTypeConst(ROUNDINGMODE_TYPE); +} + +TypeNode NodeManager::boundVarListType() +{ + return mkTypeConst(BOUND_VAR_LIST_TYPE); +} + +TypeNode NodeManager::instPatternType() +{ + return mkTypeConst(INST_PATTERN_TYPE); +} + +TypeNode NodeManager::instPatternListType() +{ + return mkTypeConst(INST_PATTERN_LIST_TYPE); +} + +TypeNode NodeManager::builtinOperatorType() +{ + return mkTypeConst(BUILTIN_OPERATOR_TYPE); +} + +TypeNode NodeManager::mkBitVectorType(unsigned size) +{ + return mkTypeConst(BitVectorSize(size)); +} + +TypeNode NodeManager::sExprType() +{ + return mkTypeConst(SEXPR_TYPE); +} + +TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig) +{ + return mkTypeConst(FloatingPointSize(exp, sig)); +} + +TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs) +{ + return mkTypeConst(fs); +} + +void NodeManager::init() +{ + if (d_initialized) + { + return; + } + d_initialized = true; + + // Note: This code cannot be part of the constructor because it indirectly + // calls `NodeManager::currentNM()`, which is where the `NodeManager` is + // being constructed. + poolInsert(&expr::NodeValue::null()); + + for (unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) + { + Kind k = Kind(i); + + if (hasOperator(k)) + { + d_operators[i] = mkConst(Kind(k)); + } + } +} + +NodeManager::~NodeManager() +{ + // Destroy skolem and bound var manager before cleaning up attributes and + // zombies + d_skManager = nullptr; + d_bvManager = nullptr; + + { + ScopedBool dontGC(d_inReclaimZombies); + // By this point, all SolverEngines should have been deleted, along with + // all their attributes + d_attrManager->deleteAllAttributes(); + } + + for (unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) + { + d_operators[i] = Node::null(); + } + + d_unique_vars.clear(); + + TypeNode dummy; + d_tt_cache.d_children.clear(); + d_tt_cache.d_data = dummy; + d_rt_cache.d_children.clear(); + d_rt_cache.d_data = dummy; + + // clear the datatypes + d_dtypes.clear(); + + Assert(!d_attrManager->inGarbageCollection()); + + std::vector order = TopologicalSort(d_maxedOut); + d_maxedOut.clear(); + + while (!d_zombies.empty() || !order.empty()) + { + if (d_zombies.empty()) + { + // Delete the maxed out nodes in toplogical order once we know + // there are no additional zombies, or other nodes to worry about. + Assert(!order.empty()); + // We process these in reverse to reverse the topological order. + NodeValue* greatest_maxed_out = order.back(); + order.pop_back(); + Assert(greatest_maxed_out->HasMaximizedReferenceCount()); + Debug("gc") << "Force zombify " << greatest_maxed_out << std::endl; + greatest_maxed_out->d_rc = 0; + markForDeletion(greatest_maxed_out); + } + else + { + reclaimZombies(); + } + } + + if (d_initialized) + { + poolRemove(&expr::NodeValue::null()); + } + + if (Debug.isOn("gc:leaks")) + { + Debug("gc:leaks") << "still in pool:" << endl; + for (NodeValuePool::const_iterator i = d_nodeValuePool.begin(), + iend = d_nodeValuePool.end(); + i != iend; + ++i) + { + Debug("gc:leaks") << " " << *i << " id=" << (*i)->d_id + << " rc=" << (*i)->d_rc << " " << **i << endl; + } + Debug("gc:leaks") << ":end:" << endl; + } + + // defensive coding, in case destruction-order issues pop up (they often do) + delete d_attrManager; + d_attrManager = NULL; +} + +const DType& NodeManager::getDTypeForIndex(size_t index) const +{ + // if this assertion fails, it is likely due to not managing datatypes + // properly w.r.t. multiple NodeManagers. + Assert(index < d_dtypes.size()); + return *d_dtypes[index]; +} + +void NodeManager::reclaimZombies() +{ + // FIXME multithreading + Assert(!d_attrManager->inGarbageCollection()); + + Debug("gc") << "reclaiming " << d_zombies.size() << " zombie(s)!\n"; + + // during reclamation, reclaimZombies() is never supposed to be called + Assert(!d_inReclaimZombies) + << "NodeManager::reclaimZombies() not re-entrant!"; + + // whether exit is normal or exceptional, the Reclaim dtor is called + // and ensures that d_inReclaimZombies is set back to false. + ScopedBool r(d_inReclaimZombies); + + // We copy the set away and clear the NodeManager's set of zombies. + // This is because reclaimZombie() decrements the RC of the + // NodeValue's children, which may (recursively) reclaim them. + // + // Let's say we're reclaiming zombie NodeValue "A" and its child "B" + // then becomes a zombie (NodeManager::markForDeletion(B) is called). + // + // One way to handle B's zombification would be simply to put it + // into d_zombies. This is what we do. However, if we were to + // concurrently process d_zombies in the loop below, such addition + // may be invisible to us (B is leaked) or even invalidate our + // iterator, causing a crash. So we need to copy the set away. + + vector zombies; + zombies.reserve(d_zombies.size()); + remove_copy_if(d_zombies.begin(), + d_zombies.end(), + back_inserter(zombies), + NodeValueReferenceCountNonZero()); + d_zombies.clear(); + +#ifdef _LIBCPP_VERSION + NodeValue* last = NULL; +#endif + for (vector::iterator i = zombies.begin(); i != zombies.end(); + ++i) + { + NodeValue* nv = *i; +#ifdef _LIBCPP_VERSION + // Work around an apparent bug in libc++'s hash_set<> which can + // (very occasionally) have an element repeated. + if (nv == last) + { + continue; + } + last = nv; +#endif + + // collect ONLY IF still zero + if (nv->d_rc == 0) + { + if (Debug.isOn("gc")) + { + Debug("gc") << "deleting node value " << nv << " [" << nv->d_id + << "]: "; + nv->printAst(Debug("gc")); + Debug("gc") << endl; + } + + // remove from the pool + kind::MetaKind mk = nv->getMetaKind(); + if (mk != kind::metakind::VARIABLE + && mk != kind::metakind::NULLARY_OPERATOR) + { + poolRemove(nv); + } + + // whether exit is normal or exceptional, the NVReclaim dtor is + // called and ensures that d_nodeUnderDeletion is set back to + // NULL. + NVReclaim rc(d_nodeUnderDeletion); + d_nodeUnderDeletion = nv; + + // remove attributes + { // notify listeners of deleted node + TNode n; + n.d_nv = nv; + nv->d_rc = 1; // so that TNode doesn't assert-fail + // this would mean that one of the listeners stowed away + // a reference to this node! + Assert(nv->d_rc == 1); + } + nv->d_rc = 0; + d_attrManager->deleteAllAttributes(nv); + + // decr ref counts of children + nv->decrRefCounts(); + if (mk == kind::metakind::CONSTANT) + { + // Destroy (call the destructor for) the C++ type representing + // the constant in this NodeValue. This is needed for + // e.g. cvc5::Rational, since it has a gmp internal + // representation that mallocs memory and should be cleaned + // up. (This won't delete a pointer value if used as a + // constant, but then, you should probably use a smart-pointer + // type for a constant payload.) + kind::metakind::deleteNodeValueConstant(nv); + } + free(nv); + } + } +} /* NodeManager::reclaimZombies() */ + +std::vector NodeManager::TopologicalSort( + const std::vector& roots) +{ + std::vector order; + // The stack of nodes to visit. The Boolean value is false when visiting the + // node in preorder and true when visiting it in postorder. + std::vector > stack; + // Nodes that have been visited in both pre- and postorder + NodeValueIDSet visited; + const NodeValueIDSet root_set(roots.begin(), roots.end()); + + for (size_t index = 0; index < roots.size(); index++) + { + NodeValue* root = roots[index]; + if (visited.find(root) == visited.end()) + { + stack.push_back(std::make_pair(false, root)); + } + while (!stack.empty()) + { + NodeValue* current = stack.back().second; + const bool visited_children = stack.back().first; + Debug("gc") << "Topological sort " << current << " " << visited_children + << std::endl; + if (visited_children) + { + if (root_set.find(current) != root_set.end()) + { + order.push_back(current); + } + stack.pop_back(); + } + else if (visited.find(current) == visited.end()) + { + stack.back().first = true; + visited.insert(current); + for (unsigned i = 0; i < current->getNumChildren(); ++i) + { + expr::NodeValue* child = current->getChild(i); + stack.push_back(std::make_pair(false, child)); + } + } + else + { + stack.pop_back(); + } + } + } + Assert(order.size() == roots.size()); + return order; +} /* NodeManager::TopologicalSort() */ + +TypeNode NodeManager::getType(TNode n, bool check) +{ + TypeNode typeNode; + bool hasType = getAttribute(n, TypeAttr(), typeNode); + bool needsCheck = check && !getAttribute(n, TypeCheckedAttr()); + + Debug("getType") << this << " getting type for " << &n << " " << n + << ", check=" << check << ", needsCheck = " << needsCheck + << ", hasType = " << hasType << endl; + +#ifdef CVC5_DEBUG + // already did type check eagerly upon creation in node builder + bool doTypeCheck = false; +#else + bool doTypeCheck = true; +#endif + if (needsCheck && doTypeCheck) + { + /* Iterate and compute the children bottom up. This avoids stack + overflows in computeType() when the Node graph is really deep, + which should only affect us when we're type checking lazily. */ + stack worklist; + worklist.push(n); + + while (!worklist.empty()) + { + TNode m = worklist.top(); + + bool readyToCompute = true; + + for (TNode::iterator it = m.begin(), end = m.end(); it != end; ++it) + { + if (!hasAttribute(*it, TypeAttr()) + || (check && !getAttribute(*it, TypeCheckedAttr()))) + { + readyToCompute = false; + worklist.push(*it); + } + } + + if (readyToCompute) + { + Assert(check || m.getMetaKind() != kind::metakind::NULLARY_OPERATOR); + /* All the children have types, time to compute */ + typeNode = TypeChecker::computeType(this, m, check); + worklist.pop(); + } + } // end while + + /* Last type computed in loop should be the type of n */ + Assert(typeNode == getAttribute(n, TypeAttr())); + } + else if (!hasType || needsCheck) + { + /* We can compute the type top-down, without worrying about + deep recursion. */ + Assert(check || n.getMetaKind() != kind::metakind::NULLARY_OPERATOR); + typeNode = TypeChecker::computeType(this, n, check); + } + + /* The type should be have been computed and stored. */ + Assert(hasAttribute(n, TypeAttr())); + /* The check should have happened, if we asked for it. */ + Assert(!check || getAttribute(n, TypeCheckedAttr())); + + Debug("getType") << "type of " << &n << " " << n << " is " << typeNode + << endl; + return typeNode; +} + +TypeNode NodeManager::mkBagType(TypeNode elementType) +{ + CheckArgument( + !elementType.isNull(), elementType, "unexpected NULL element type"); + Debug("bags") << "making bags type " << elementType << std::endl; + return mkTypeNode(kind::BAG_TYPE, elementType); +} + +TypeNode NodeManager::mkSequenceType(TypeNode elementType) +{ + CheckArgument( + !elementType.isNull(), elementType, "unexpected NULL element type"); + return mkTypeNode(kind::SEQUENCE_TYPE, elementType); +} + +TypeNode NodeManager::mkDatatypeType(DType& datatype, uint32_t flags) +{ + // Not worth a special implementation; this doesn't need to be fast + // code anyway. + std::vector datatypes; + datatypes.push_back(datatype); + std::vector result = mkMutualDatatypeTypes(datatypes, flags); + Assert(result.size() == 1); + return result.front(); +} + +std::vector NodeManager::mkMutualDatatypeTypes( + const std::vector& datatypes, uint32_t flags) +{ + std::set unresolvedTypes; + return mkMutualDatatypeTypes(datatypes, unresolvedTypes, flags); +} + +std::vector NodeManager::mkMutualDatatypeTypes( + const std::vector& datatypes, + const std::set& unresolvedTypes, + uint32_t flags) +{ + std::map nameResolutions; + std::vector dtts; + + // First do some sanity checks, set up the final Type to be used for + // each datatype, and set up the "named resolutions" used to handle + // simple self- and mutual-recursion, for example in the definition + // "nat = succ(pred:nat) | zero", a named resolution can handle the + // pred selector. + for (const DType& dt : datatypes) + { + uint32_t index = d_dtypes.size(); + d_dtypes.push_back(std::unique_ptr(new DType(dt))); + DType* dtp = d_dtypes.back().get(); + TypeNode typeNode; + if (dtp->getNumParameters() == 0) + { + typeNode = mkTypeConst(DatatypeIndexConstant(index)); + } + else + { + TypeNode cons = mkTypeConst(DatatypeIndexConstant(index)); + std::vector params; + params.push_back(cons); + for (uint32_t ip = 0; ip < dtp->getNumParameters(); ++ip) + { + params.push_back(dtp->getParameter(ip)); + } + + typeNode = mkTypeNode(kind::PARAMETRIC_DATATYPE, params); + } + if (nameResolutions.find(dtp->getName()) != nameResolutions.end()) + { + throw Exception( + "cannot construct two datatypes at the same time with the same name"); + } + nameResolutions.insert(std::make_pair(dtp->getName(), typeNode)); + dtts.push_back(typeNode); + } + + // Second, set up the type substitution map for complex type + // resolution (e.g. if "list" is the type we're defining, and it has + // a selector of type "ARRAY INT OF list", this can't be taken care + // of using the named resolutions that we set up above. A + // preliminary array type was set up, and now needs to have "list" + // substituted in it for the correct type. + // + // @TODO get rid of named resolutions altogether and handle + // everything with these resolutions? + std::vector paramTypes; + std::vector paramReplacements; + std::vector placeholders; // to hold the "unresolved placeholders" + std::vector replacements; // to hold our final, resolved types + for (const TypeNode& ut : unresolvedTypes) + { + std::string name = ut.getAttribute(expr::VarNameAttr()); + std::map::const_iterator resolver = + nameResolutions.find(name); + if (resolver == nameResolutions.end()) + { + throw Exception("cannot resolve type " + name + + "; it's not among the datatypes being defined"); + } + // We will instruct the Datatype to substitute "ut" (the + // unresolved SortType used as a placeholder in complex types) + // with "(*resolver).second" (the TypeNode we created in the + // first step, above). + if (ut.isSort()) + { + placeholders.push_back(ut); + replacements.push_back((*resolver).second); + } + else + { + Assert(ut.isSortConstructor()); + paramTypes.push_back(ut); + paramReplacements.push_back((*resolver).second); + } + } + + // Lastly, perform the final resolutions and checks. + for (const TypeNode& ut : dtts) + { + const DType& dt = ut.getDType(); + if (!dt.isResolved()) + { + const_cast(dt).resolve(nameResolutions, + placeholders, + replacements, + paramTypes, + paramReplacements); + } + // Check the datatype has been resolved properly. + for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) + { + const DTypeConstructor& c = dt[i]; + TypeNode testerType CVC5_UNUSED = c.getTester().getType(); + Assert(c.isResolved() && testerType.isTester() && testerType[0] == ut) + << "malformed tester in datatype post-resolution"; + TypeNode ctorType CVC5_UNUSED = c.getConstructor().getType(); + Assert(ctorType.isConstructor() + && ctorType.getNumChildren() == c.getNumArgs() + 1 + && ctorType.getRangeType() == ut) + << "malformed constructor in datatype post-resolution"; + // for all selectors... + for (size_t j = 0, nargs = c.getNumArgs(); j < nargs; j++) + { + const DTypeSelector& a = c[j]; + TypeNode selectorType = a.getType(); + Assert(a.isResolved() && selectorType.isSelector() + && selectorType[0] == ut) + << "malformed selector in datatype post-resolution"; + // This next one's a "hard" check, performed in non-debug builds + // as well; the other ones should all be guaranteed by the + // cvc5::DType class, but this actually needs to be checked. + if (selectorType.getRangeType().isFunctionLike()) + { + throw Exception("cannot put function-like things in datatypes"); + } + } + } + } + + return dtts; +} + +TypeNode NodeManager::mkConstructorType(const std::vector& args, + TypeNode range) +{ + std::vector sorts = args; + sorts.push_back(range); + return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts); +} + +TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) +{ + CheckArgument( + domain.isDatatype(), domain, "cannot create non-datatype selector type"); + return mkTypeNode(kind::SELECTOR_TYPE, domain, range); +} + +TypeNode NodeManager::mkTesterType(TypeNode domain) +{ + CheckArgument( + domain.isDatatype(), domain, "cannot create non-datatype tester"); + return mkTypeNode(kind::TESTER_TYPE, domain); +} + +TypeNode NodeManager::mkDatatypeUpdateType(TypeNode domain, TypeNode range) +{ + CheckArgument( + domain.isDatatype(), domain, "cannot create non-datatype upater type"); + // It is a function type domain x range -> domain, we store only the + // arguments + return mkTypeNode(kind::UPDATER_TYPE, domain, range); +} + +TypeNode NodeManager::TupleTypeCache::getTupleType(NodeManager* nm, + std::vector& types, + unsigned index) +{ + if (index == types.size()) + { + if (d_data.isNull()) + { + std::stringstream sst; + sst << "__cvc5_tuple"; + for (unsigned i = 0; i < types.size(); ++i) + { + sst << "_" << types[i]; + } + DType dt(sst.str()); + dt.setTuple(); + std::stringstream ssc; + ssc << sst.str() << "_ctor"; + std::shared_ptr c = + std::make_shared(ssc.str()); + for (unsigned i = 0; i < types.size(); ++i) + { + std::stringstream ss; + ss << sst.str() << "_stor_" << i; + c->addArg(ss.str().c_str(), types[i]); + } + dt.addConstructor(c); + d_data = nm->mkDatatypeType(dt); + Debug("tuprec-debug") << "Return type : " << d_data << std::endl; + } + return d_data; + } + else + { + return d_children[types[index]].getTupleType(nm, types, index + 1); + } +} + +TypeNode NodeManager::RecTypeCache::getRecordType(NodeManager* nm, + const Record& rec, + unsigned index) +{ + if (index == rec.size()) + { + if (d_data.isNull()) + { + std::stringstream sst; + sst << "__cvc5_record"; + for (const std::pair& i : rec) + { + sst << "_" << i.first << "_" << i.second; + } + DType dt(sst.str()); + dt.setRecord(); + std::stringstream ssc; + ssc << sst.str() << "_ctor"; + std::shared_ptr c = + std::make_shared(ssc.str()); + for (const std::pair& i : rec) + { + c->addArg(i.first, i.second); + } + dt.addConstructor(c); + d_data = nm->mkDatatypeType(dt); + Debug("tuprec-debug") << "Return type : " << d_data << std::endl; + } + return d_data; + } + return d_children[rec[index].second][rec[index].first].getRecordType( + nm, rec, index + 1); +} + +TypeNode NodeManager::mkFunctionType(const std::vector& sorts) +{ + Assert(sorts.size() >= 2); + return mkTypeNode(kind::FUNCTION_TYPE, sorts); +} + +TypeNode NodeManager::mkPredicateType(const std::vector& sorts) +{ + Assert(sorts.size() >= 1); + std::vector sortNodes; + sortNodes.insert(sortNodes.end(), sorts.begin(), sorts.end()); + sortNodes.push_back(booleanType()); + return mkFunctionType(sortNodes); +} + +TypeNode NodeManager::mkFunctionType(const TypeNode& domain, + const TypeNode& range) +{ + std::vector sorts; + sorts.push_back(domain); + sorts.push_back(range); + return mkFunctionType(sorts); +} + +TypeNode NodeManager::mkFunctionType(const std::vector& argTypes, + const TypeNode& range) +{ + Assert(argTypes.size() >= 1); + std::vector sorts(argTypes); + sorts.push_back(range); + return mkFunctionType(sorts); +} + +TypeNode NodeManager::mkTupleType(const std::vector& types) +{ + std::vector ts; + Debug("tuprec-debug") << "Make tuple type : "; + for (unsigned i = 0; i < types.size(); ++i) + { + CheckArgument(!types[i].isFunctionLike(), + types, + "cannot put function-like types in tuples"); + ts.push_back(types[i]); + Debug("tuprec-debug") << types[i] << " "; + } + Debug("tuprec-debug") << std::endl; + return d_tt_cache.getTupleType(this, ts); +} + +TypeNode NodeManager::mkRecordType(const Record& rec) +{ + return d_rt_cache.getRecordType(this, rec); +} + +void NodeManager::reclaimAllZombies() { reclaimZombiesUntil(0u); } + +/** Reclaim zombies while there are more than k nodes in the pool (if + * possible).*/ +void NodeManager::reclaimZombiesUntil(uint32_t k) +{ + if (safeToReclaimZombies()) + { + while (poolSize() >= k && !d_zombies.empty()) + { + reclaimZombies(); + } + } +} + +size_t NodeManager::poolSize() const { return d_nodeValuePool.size(); } + +TypeNode NodeManager::mkSort(uint32_t flags) +{ + NodeBuilder nb(this, kind::SORT_TYPE); + Node sortTag = NodeBuilder(this, kind::SORT_TAG); + nb << sortTag; + return nb.constructTypeNode(); +} + +TypeNode NodeManager::mkSort(const std::string& name, uint32_t flags) +{ + NodeBuilder nb(this, kind::SORT_TYPE); + Node sortTag = NodeBuilder(this, kind::SORT_TAG); + nb << sortTag; + TypeNode tn = nb.constructTypeNode(); + setAttribute(tn, expr::VarNameAttr(), name); + return tn; +} + +TypeNode NodeManager::mkSort(TypeNode constructor, + const std::vector& children, + uint32_t flags) +{ + Assert(constructor.getKind() == kind::SORT_TYPE + && constructor.getNumChildren() == 0) + << "expected a sort constructor"; + Assert(children.size() > 0) << "expected non-zero # of children"; + Assert(hasAttribute(constructor.d_nv, expr::SortArityAttr()) + && hasAttribute(constructor.d_nv, expr::VarNameAttr())) + << "expected a sort constructor"; + std::string name = getAttribute(constructor.d_nv, expr::VarNameAttr()); + Assert(getAttribute(constructor.d_nv, expr::SortArityAttr()) + == children.size()) + << "arity mismatch in application of sort constructor"; + NodeBuilder nb(this, kind::SORT_TYPE); + Node sortTag = Node(constructor.d_nv->d_children[0]); + nb << sortTag; + nb.append(children); + TypeNode type = nb.constructTypeNode(); + setAttribute(type, expr::VarNameAttr(), name); + return type; +} + +TypeNode NodeManager::mkSortConstructor(const std::string& name, + size_t arity, + uint32_t flags) +{ + Assert(arity > 0); + NodeBuilder nb(this, kind::SORT_TYPE); + Node sortTag = NodeBuilder(this, kind::SORT_TAG); + nb << sortTag; + TypeNode type = nb.constructTypeNode(); + setAttribute(type, expr::VarNameAttr(), name); + setAttribute(type, expr::SortArityAttr(), arity); + return type; +} + +Node NodeManager::mkVar(const std::string& name, const TypeNode& type) +{ + Node n = NodeBuilder(this, kind::VARIABLE); + setAttribute(n, TypeAttr(), type); + setAttribute(n, TypeCheckedAttr(), true); + setAttribute(n, expr::VarNameAttr(), name); + return n; +} + +Node NodeManager::mkBoundVar(const std::string& name, const TypeNode& type) +{ + Node n = mkBoundVar(type); + setAttribute(n, expr::VarNameAttr(), name); + return n; +} + +Node NodeManager::getBoundVarListForFunctionType(TypeNode tn) +{ + Assert(tn.isFunction()); + Node bvl = tn.getAttribute(LambdaBoundVarListAttr()); + if (bvl.isNull()) + { + std::vector vars; + for (unsigned i = 0; i < tn.getNumChildren() - 1; i++) + { + vars.push_back(mkBoundVar(tn[i])); + } + bvl = mkNode(kind::BOUND_VAR_LIST, vars); + Trace("functions") << "Make standard bound var list " << bvl << " for " + << tn << std::endl; + tn.setAttribute(LambdaBoundVarListAttr(), bvl); + } + return bvl; +} + +Node NodeManager::mkAssociative(Kind kind, const std::vector& children) +{ + AlwaysAssert(kind::isAssociative(kind)) << "Illegal kind in mkAssociative"; + + const unsigned int max = kind::metakind::getMaxArityForKind(kind); + size_t numChildren = children.size(); + + /* If the number of children is within bounds, then there's nothing to do. */ + if (numChildren <= max) + { + return mkNode(kind, children); + } + const unsigned int min = kind::metakind::getMinArityForKind(kind); + + std::vector::const_iterator it = children.begin(); + std::vector::const_iterator end = children.end(); + + /* The new top-level children and the children of each sub node */ + std::vector newChildren; + std::vector subChildren; + + while (it != end && numChildren > max) + { + /* Grab the next max children and make a node for them. */ + for (std::vector::const_iterator next = it + max; it != next; + ++it, --numChildren) + { + subChildren.push_back(*it); + } + Node subNode = mkNode(kind, subChildren); + newChildren.push_back(subNode); + + subChildren.clear(); + } + + // add the leftover children + if (numChildren > 0) + { + for (; it != end; ++it) + { + newChildren.push_back(*it); + } + } + + /* It would be really weird if this happened (it would require + * min > 2, for one thing), but let's make sure. */ + AlwaysAssert(newChildren.size() >= min) + << "Too few new children in mkAssociative"; + + // recurse + return mkAssociative(kind, newChildren); +} + +Node NodeManager::mkLeftAssociative(Kind kind, + const std::vector& children) +{ + Node n = children[0]; + for (size_t i = 1, size = children.size(); i < size; i++) + { + n = mkNode(kind, n, children[i]); + } + return n; +} + +Node NodeManager::mkRightAssociative(Kind kind, + const std::vector& children) +{ + Node n = children[children.size() - 1]; + for (size_t i = children.size() - 1; i > 0;) + { + n = mkNode(kind, children[--i], n); + } + return n; +} + +Node NodeManager::mkChain(Kind kind, const std::vector& children) +{ + if (children.size() == 2) + { + // if this is the case exactly 1 pair will be generated so the + // AND is not required + return mkNode(kind, children[0], children[1]); + } + std::vector cchildren; + for (size_t i = 0, nargsmo = children.size() - 1; i < nargsmo; i++) + { + cchildren.push_back(mkNode(kind, children[i], children[i + 1])); + } + return mkNode(kind::AND, cchildren); +} + +Node NodeManager::mkVar(const TypeNode& type) +{ + Node n = NodeBuilder(this, kind::VARIABLE); + setAttribute(n, TypeAttr(), type); + setAttribute(n, TypeCheckedAttr(), true); + return n; +} + +Node NodeManager::mkBoundVar(const TypeNode& type) +{ + Node n = NodeBuilder(this, kind::BOUND_VARIABLE); + setAttribute(n, TypeAttr(), type); + setAttribute(n, TypeCheckedAttr(), true); + return n; +} + +Node NodeManager::mkInstConstant(const TypeNode& type) +{ + Node n = NodeBuilder(this, kind::INST_CONSTANT); + n.setAttribute(TypeAttr(), type); + n.setAttribute(TypeCheckedAttr(), true); + return n; +} + +Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) +{ + std::map::iterator it = d_unique_vars[k].find(type); + if (it == d_unique_vars[k].end()) + { + Node n = NodeBuilder(this, k).constructNode(); + setAttribute(n, TypeAttr(), type); + // setAttribute(n, TypeCheckedAttr(), true); + d_unique_vars[k][type] = n; + Assert(n.getMetaKind() == kind::metakind::NULLARY_OPERATOR); + return n; + } + else + { + return it->second; + } +} + +Node NodeManager::mkSingleton(const TypeNode& t, const TNode n) +{ + Assert(n.getType().isSubtypeOf(t)) + << "Invalid operands for mkSingleton. The type '" << n.getType() + << "' of node '" << n << "' is not a subtype of '" << t << "'." + << std::endl; + Node op = mkConst(SetSingletonOp(t)); + Node singleton = mkNode(kind::SET_SINGLETON, op, n); + return singleton; +} + +Node NodeManager::mkBag(const TypeNode& t, const TNode n, const TNode m) +{ + Assert(n.getType().isSubtypeOf(t)) + << "Invalid operands for mkBag. The type '" << n.getType() + << "' of node '" << n << "' is not a subtype of '" << t << "'." + << std::endl; + Node op = mkConst(BagMakeOp(t)); + Node bag = mkNode(kind::BAG_MAKE, op, n, m); + return bag; +} + +Node NodeManager::mkAbstractValue(const TypeNode& type) +{ + Node n = mkConst(AbstractValue(++d_abstractValueCount)); + n.setAttribute(TypeAttr(), type); + n.setAttribute(TypeCheckedAttr(), true); + return n; +} + +bool NodeManager::hasOperator(Kind k) +{ + switch (kind::MetaKind mk = kind::metaKindOf(k)) + { + case kind::metakind::INVALID: + case kind::metakind::VARIABLE: + case kind::metakind::NULLARY_OPERATOR: return false; + + case kind::metakind::OPERATOR: + case kind::metakind::PARAMETERIZED: return true; + + case kind::metakind::CONSTANT: return false; + + default: Unhandled() << mk; + } +} + +TNode NodeManager::operatorOf(Kind k) +{ + AssertArgument(kind::metaKindOf(k) == kind::metakind::OPERATOR, + k, + "Kind is not an OPERATOR-kinded kind " + "in NodeManager::operatorOf()"); + 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) +{ + NVStorage<1> nvStorage; + expr::NodeValue& nvStack = reinterpret_cast(nvStorage); + + nvStack.d_id = 0; + nvStack.d_kind = k; + nvStack.d_rc = 0; + nvStack.d_nchildren = 1; + +#if defined(__GNUC__) \ + && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6)) +#pragma GCC diagnostic push +#pragma GCC diagnostic ignored "-Warray-bounds" +#endif + + nvStack.d_children[0] = const_cast( + reinterpret_cast(&val)); + expr::NodeValue* nv = poolLookup(&nvStack); + +#if defined(__GNUC__) \ + && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6)) +#pragma GCC diagnostic pop +#endif + + if (nv != NULL) + { + return NodeClass(nv); + } + + nv = (expr::NodeValue*)std::malloc(sizeof(expr::NodeValue) + sizeof(T)); + if (nv == NULL) + { + throw std::bad_alloc(); + } + + nv->d_nchildren = 0; + nv->d_kind = k; + nv->d_id = next_id++; // FIXME multithreading + nv->d_rc = 0; + + new (&nv->d_children) T(val); + + poolInsert(nv); + if (Debug.isOn("gc")) + { + Debug("gc") << "creating node value " << nv << " [" << nv->d_id << "]: "; + nv->printAst(Debug("gc")); + Debug("gc") << std::endl; + } + + return NodeClass(nv); +} + +bool NodeManager::safeToReclaimZombies() const +{ + // FIXME multithreading + return !d_inReclaimZombies && !d_attrManager->inGarbageCollection(); +} + +void NodeManager::deleteAttributes( + const std::vector& ids) +{ + d_attrManager->deleteAttributes(ids); +} + +void NodeManager::debugHook(int debugFlag) +{ + // For debugging purposes only, DO NOT CHECK IN ANY CODE! +} + +Kind NodeManager::getKindForFunction(TNode fun) +{ + TypeNode tn = fun.getType(); + if (tn.isFunction()) + { + return kind::APPLY_UF; + } + else if (tn.isConstructor()) + { + return kind::APPLY_CONSTRUCTOR; + } + else if (tn.isSelector()) + { + return kind::APPLY_SELECTOR; + } + else if (tn.isTester()) + { + return kind::APPLY_TESTER; + } + return kind::UNDEFINED_KIND; +} + +Node NodeManager::mkNode(Kind kind, std::initializer_list children) +{ + NodeBuilder nb(this, kind); + nb.append(children.begin(), children.end()); + return nb.constructNode(); +} + +Node NodeManager::mkNode(TNode opNode, std::initializer_list children) +{ + NodeBuilder nb(this, operatorToKind(opNode)); + if (opNode.getKind() != kind::BUILTIN) + { + nb << opNode; + } + nb.append(children.begin(), children.end()); + return nb.constructNode(); +} + +Node NodeManager::mkConstReal(const Rational& r) +{ + return mkConst(kind::CONST_RATIONAL, r); +} + +Node NodeManager::mkConstInt(const Rational& r) +{ + // !!!! Note will update to CONST_INTEGER. + return mkConst(kind::CONST_RATIONAL, r); +} + +} // namespace cvc5