From f5f9665a43576ff9524687b13f6099fd90e86c98 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 23 Apr 2022 10:48:28 -0500 Subject: [PATCH] Minor cleanup of NodeManager (#8650) --- src/api/cpp/cvc5.cpp | 4 +- src/expr/node_builder.cpp | 6 +- src/expr/node_manager_template.cpp | 46 ++--------- src/expr/node_manager_template.h | 79 +++++-------------- src/preprocessing/passes/ite_simp.cpp | 18 ----- src/preprocessing/passes/ite_simp.h | 2 - src/preprocessing/passes/synth_rew_rules.cpp | 6 +- src/theory/datatypes/sygus_datatype_utils.cpp | 3 +- src/theory/quantifiers/sygus/cegis_unif.cpp | 3 +- .../quantifiers/sygus/sygus_grammar_cons.cpp | 7 +- .../quantifiers/sygus/sygus_grammar_norm.cpp | 4 +- src/theory/rewriter.cpp | 9 --- src/theory/rewriter.h | 5 -- src/theory/rewriter_tables_template.h | 25 ------ 14 files changed, 40 insertions(+), 177 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 84967b5c9..e0983f3af 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -4458,9 +4458,7 @@ Sort Grammar::resolve() } std::vector datatypeTypes = - d_solver->getNodeManager()->mkMutualDatatypeTypes( - datatypes, - internal::NodeManager::DATATYPE_FLAG_PLACEHOLDER); + d_solver->getNodeManager()->mkMutualDatatypeTypes(datatypes); // return is the first datatype return Sort(d_solver, datatypeTypes[0]); diff --git a/src/expr/node_builder.cpp b/src/expr/node_builder.cpp index 276dab5e4..693eadd39 100644 --- a/src/expr/node_builder.cpp +++ b/src/expr/node_builder.cpp @@ -415,7 +415,7 @@ expr::NodeValue* NodeBuilder::constructNV() // reference counts in this case. nv->d_nchildren = 0; nv->d_kind = d_nv->d_kind; - nv->d_id = d_nm->next_id++; // FIXME multithreading + nv->d_id = d_nm->d_nextId++; nv->d_rc = 0; setUsed(); if (TraceIsOn("gc")) @@ -497,7 +497,7 @@ expr::NodeValue* NodeBuilder::constructNV() } nv->d_nchildren = d_inlineNv.d_nchildren; nv->d_kind = d_inlineNv.d_kind; - nv->d_id = d_nm->next_id++; // FIXME multithreading + nv->d_id = d_nm->d_nextId++; nv->d_rc = 0; std::copy(d_inlineNv.d_children, @@ -557,7 +557,7 @@ expr::NodeValue* NodeBuilder::constructNV() crop(); expr::NodeValue* nv = d_nv; - nv->d_id = d_nm->next_id++; // FIXME multithreading + nv->d_id = d_nm->d_nextId++; d_nv = &d_inlineNv; d_nvMaxChildren = default_nchild_thresh; setUsed(); diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp index 779687eed..57b59dce9 100644 --- a/src/expr/node_manager_template.cpp +++ b/src/expr/node_manager_template.cpp @@ -110,11 +110,10 @@ NodeManager::NodeManager() : d_skManager(new SkolemManager), d_bvManager(new BoundVarManager), d_initialized(false), - next_id(0), + d_nextId(0), d_attrManager(new expr::attr::AttributeManager()), d_nodeUnderDeletion(nullptr), - d_inReclaimZombies(false), - d_abstractValueCount(0) + d_inReclaimZombies(false) { } @@ -556,19 +555,19 @@ TypeNode NodeManager::mkSequenceType(TypeNode elementType) return mkTypeNode(kind::SEQUENCE_TYPE, elementType); } -TypeNode NodeManager::mkDatatypeType(DType& datatype, uint32_t flags) +TypeNode NodeManager::mkDatatypeType(DType& datatype) { // 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); + std::vector result = mkMutualDatatypeTypes(datatypes); Assert(result.size() == 1); return result.front(); } std::vector NodeManager::mkMutualDatatypeTypes( - const std::vector& datatypes, uint32_t flags) + const std::vector& datatypes) { std::set unresolvedTypes; // scan the list of datatypes to find unresolved datatypes @@ -576,13 +575,12 @@ std::vector NodeManager::mkMutualDatatypeTypes( { dt.collectUnresolvedDatatypeTypes(unresolvedTypes); } - return mkMutualDatatypeTypesInternal(datatypes, unresolvedTypes, flags); + return mkMutualDatatypeTypesInternal(datatypes, unresolvedTypes); } std::vector NodeManager::mkMutualDatatypeTypesInternal( const std::vector& datatypes, - const std::set& unresolvedTypes, - uint32_t flags) + const std::set& unresolvedTypes) { std::map nameResolutions; std::vector dtts; @@ -868,23 +866,6 @@ 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() { NodeBuilder nb(this, kind::SORT_TYPE); @@ -1157,12 +1138,6 @@ Node NodeManager::mkBag(const TypeNode& t, const TNode n, const TNode m) return bag; } -Node NodeManager::mkUninterpretedSortValue(const TypeNode& type) -{ - Node n = mkConst(UninterpretedSortValue(type, ++d_abstractValueCount)); - return n; -} - bool NodeManager::hasOperator(Kind k) { switch (kind::MetaKind mk = kind::metaKindOf(k)) @@ -1228,7 +1203,7 @@ NodeClass NodeManager::mkConstInternal(Kind k, const T& val) nv->d_nchildren = 0; nv->d_kind = k; - nv->d_id = next_id++; // FIXME multithreading + nv->d_id = d_nextId++; nv->d_rc = 0; new (&nv->d_children) T(val); @@ -1267,11 +1242,6 @@ void NodeManager::deleteAttributes( 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(); diff --git a/src/expr/node_manager_template.h b/src/expr/node_manager_template.h index d8927f43a..4e84b16fc 100644 --- a/src/expr/node_manager_template.h +++ b/src/expr/node_manager_template.h @@ -48,14 +48,21 @@ class DType; class Rational; namespace expr { - namespace attr { - class AttributeUniqueId; - class AttributeManager; - } // namespace attr - class TypeChecker; - } // namespace expr +namespace attr { +class AttributeUniqueId; +class AttributeManager; +} // namespace attr +class TypeChecker; +} // namespace expr + +/** + * The node manager. + * + * This class should not be used simulatenously in multiple threads. It is a + * singleton that is accessible via NodeManager::currentNM(). + */ class NodeManager { friend class cvc5::Solver; @@ -66,24 +73,6 @@ class NodeManager friend class NodeBuilder; public: - /** - * Bits for use in mkDatatypeType() flags. - * - * DATATYPE_FLAG_PLACEHOLDER indicates that the type should not be printed - * out as a definition, for example, in models or during dumping. - */ - enum - { - DATATYPE_FLAG_NONE = 0, - DATATYPE_FLAG_PLACEHOLDER = 1 - }; /* enum */ - - /** Bits for use in mkSort() flags. */ - enum - { - SORT_FLAG_NONE = 0, - SORT_FLAG_PLACEHOLDER = 1 - }; /* enum */ /** * Return true if given kind is n-ary. The test is based on n-ary kinds @@ -143,25 +132,6 @@ class NodeManager /** Get this node manager's bound variable manager */ BoundVarManager* getBoundVarManager() { return d_bvManager.get(); } - /** 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; - - /** - * 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); - /** * Return the datatype at the given index owned by this class. Type nodes are * associated with datatypes through the DatatypeIndexConstant class. The @@ -493,14 +463,14 @@ class NodeManager TypeNode mkSequenceType(TypeNode elementType); /** Make a type representing the given datatype. */ - TypeNode mkDatatypeType(DType& datatype, uint32_t flags = DATATYPE_FLAG_NONE); + TypeNode mkDatatypeType(DType& datatype); /** * 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); + const std::vector& datatypes); /** * Make a type representing a constructor with the given argument (subfield) @@ -655,9 +625,6 @@ class NodeManager /** Create a raw symbol with the given type. */ Node mkRawSymbol(const std::string& name, const TypeNode& type); - /** Make a new uninterpreted sort value with the given type. */ - Node mkUninterpretedSortValue(const TypeNode& type); - /** make unique (per Type,Kind) variable. */ Node mkNullaryOperator(const TypeNode& type, Kind k); @@ -802,8 +769,7 @@ class NodeManager */ std::vector mkMutualDatatypeTypesInternal( const std::vector& datatypes, - const std::set& unresolvedTypes, - uint32_t flags = DATATYPE_FLAG_NONE); + const std::set& unresolvedTypes); typedef std::unordered_set */ + }; /** * A map of tuple and record types to their corresponding datatype. @@ -1010,7 +976,8 @@ class NodeManager bool d_initialized; - size_t next_id; + /** The next node identifier */ + size_t d_nextId; expr::attr::AttributeManager* d_attrManager; @@ -1063,14 +1030,6 @@ class NodeManager 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. - */ - uint32_t d_abstractValueCount; }; /* class NodeManager */ inline TypeNode NodeManager::mkArrayType(TypeNode indexType, diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index 48c045582..e8f5e8998 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -203,24 +203,6 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess) { result = d_iteUtilities.compress(assertionsToPreprocess); } - - if (result) - { - // if false, don't bother to reclaim memory here. - NodeManager* nm = NodeManager::currentNM(); - if (nm->poolSize() >= zombieHuntThreshold) - { - verbose(2) << "..ite simplifier did quite a bit of work.. " - << nm->poolSize() << endl; - verbose(2) << "....node manager contains " << nm->poolSize() - << " nodes before cleanup" << endl; - d_iteUtilities.clear(); - d_env.getRewriter()->clearCaches(); - nm->reclaimZombiesUntil(zombieHuntThreshold); - verbose(2) << "....node manager contains " << nm->poolSize() - << " nodes after cleanup" << endl; - } - } } // Do theory specific preprocessing passes diff --git a/src/preprocessing/passes/ite_simp.h b/src/preprocessing/passes/ite_simp.h index 53812f93f..7b8e19f50 100644 --- a/src/preprocessing/passes/ite_simp.h +++ b/src/preprocessing/passes/ite_simp.h @@ -49,8 +49,6 @@ class ITESimp : public PreprocessingPass util::ITEUtilities d_iteUtilities; Statistics d_statistics; - - static const uint32_t zombieHuntThreshold = 524288; }; } // namespace passes diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index 3569d1250..8308ca11c 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -395,8 +395,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( { datatypes.push_back(sdts[i].getDatatype()); } - std::vector types = nm->mkMutualDatatypeTypes( - datatypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER); + std::vector types = nm->mkMutualDatatypeTypes(datatypes); Trace("srs-input") << "...finished." << std::endl; Assert(types.size() == datatypes.size()); std::map subtermTypes; @@ -440,8 +439,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( // set that this is a sygus datatype sdttl.initializeDatatype(t, sygusVarList, false, false); DType dttl = sdttl.getDatatype(); - TypeNode tlt = - nm->mkDatatypeType(dttl, NodeManager::DATATYPE_FLAG_PLACEHOLDER); + TypeNode tlt = nm->mkDatatypeType(dttl); tlGrammarTypes[t] = tlt; Trace("srs-input") << "Grammar is: " << std::endl; Trace("srs-input") << printer::smt2::Smt2Printer::sygusGrammarString(tlt) diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp index 935d912b7..6b833cb81 100644 --- a/src/theory/datatypes/sygus_datatype_utils.cpp +++ b/src/theory/datatypes/sygus_datatype_utils.cpp @@ -546,8 +546,7 @@ TypeNode substituteAndGeneralizeSygusType(TypeNode sdt, datatypes.push_back(sdts[i].getDatatype()); } // make the datatype types - std::vector datatypeTypes = nm->mkMutualDatatypeTypes( - datatypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER); + std::vector datatypeTypes = nm->mkMutualDatatypeTypes(datatypes); TypeNode sdtS = datatypeTypes[0]; if (TraceIsOn("dtsygus-gen-debug")) { diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index e70d48032..9686b081d 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -487,8 +487,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) sdt.initializeDatatype(nm->integerType(), bvl, false, false); std::vector datatypes; datatypes.push_back(sdt.getDatatype()); - std::vector dtypes = nm->mkMutualDatatypeTypes( - datatypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER); + std::vector dtypes = nm->mkMutualDatatypeTypes(datatypes); d_virtual_enum = sm->mkDummySkolem("_ve", dtypes[0]); d_tds->registerEnumerator( d_virtual_enum, Node::null(), d_parent, ROLE_ENUM_CONSTRAINED); diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 81c75a176..f6cdc2411 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -1544,8 +1544,8 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType( } Trace("sygus-grammar-def") << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl; Assert(!datatypes.empty()); - std::vector types = NodeManager::currentNM()->mkMutualDatatypeTypes( - datatypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER); + std::vector types = + NodeManager::currentNM()->mkMutualDatatypeTypes(datatypes); Trace("sygus-grammar-def") << "...finished" << std::endl; Assert(types.size() == datatypes.size()); return types[0]; @@ -1591,8 +1591,7 @@ TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_a datatypes.push_back(sdts[i].getDatatype()); } std::vector types = - NodeManager::currentNM()->mkMutualDatatypeTypes( - datatypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER); + NodeManager::currentNM()->mkMutualDatatypeTypes(datatypes); Assert(types.size() == 1); return types[0]; } diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index 58090c98a..85ddc9f5f 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -526,8 +526,8 @@ TypeNode SygusGrammarNorm::normalizeSygusType(TypeNode tn, Node sygus_vars) Trace("sygus-grammar-normalize-build") << "\n"; } Assert(d_dt_all.size() == d_unres_t_all.size()); - std::vector types = NodeManager::currentNM()->mkMutualDatatypeTypes( - d_dt_all, NodeManager::DATATYPE_FLAG_PLACEHOLDER); + std::vector types = + NodeManager::currentNM()->mkMutualDatatypeTypes(d_dt_all); Assert(types.size() == d_dt_all.size()); /* Clear accumulators */ d_dt_all.clear(); diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 22b852b92..bf74c0281 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -481,15 +481,6 @@ RewriteResponse Rewriter::processTrustRewriteResponse( return RewriteResponse(tresponse.d_status, trn.getNode()); } -void Rewriter::clearCaches() -{ -#ifdef CVC5_ASSERTIONS - d_rewriteStack.reset(nullptr); -#endif - - clearCachesInternal(); -} - bool Rewriter::hasRewrittenWithProofs(TNode n) const { return d_tpgNodes.find(n) != d_tpgNodes.end(); diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 95defbe63..273ef036e 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -89,9 +89,6 @@ class Rewriter { /** Set proof node manager */ void setProofNodeManager(ProofNodeManager* pnm); - /** Garbage collects the rewrite caches. */ - void clearCaches(); - /** * Registers a theory rewriter with this rewriter. The rewriter does not own * the theory rewriters. @@ -153,8 +150,6 @@ class Rewriter { */ Node callRewriteEquality(theory::TheoryId theoryId, TNode equality); - void clearCachesInternal(); - /** * Has n been rewritten with proofs? This checks if n is in d_tpgNodes. */ diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h index 9fb824812..4159cefaf 100644 --- a/src/theory/rewriter_tables_template.h +++ b/src/theory/rewriter_tables_template.h @@ -82,30 +82,5 @@ ${post_rewrite_set_cache} Rewriter::Rewriter() : d_resourceManager(nullptr), d_tpg(nullptr) {} -void Rewriter::clearCachesInternal() -{ - typedef cvc5::internal::expr::attr::AttributeUniqueId AttributeUniqueId; - std::vector preids; - // clang-format off - ${pre_rewrite_attribute_ids} // clang-format on - - std::vector - postids; - // clang-format off - ${post_rewrite_attribute_ids} // clang-format on - - std::vector - allids; - for (size_t i = 0, size = preids.size(); i < size; ++i) - { - allids.push_back(&preids[i]); - } - for (size_t i = 0, size = postids.size(); i < size; ++i) - { - allids.push_back(&postids[i]); - } - NodeManager::currentNM()->deleteAttributes(allids); -} - } // namespace theory } // namespace cvc5::internal -- 2.30.2