}
std::vector<internal::TypeNode> 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]);
// 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"))
}
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,
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();
: 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)
{
}
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<DType> datatypes;
datatypes.push_back(datatype);
- std::vector<TypeNode> result = mkMutualDatatypeTypes(datatypes, flags);
+ std::vector<TypeNode> result = mkMutualDatatypeTypes(datatypes);
Assert(result.size() == 1);
return result.front();
}
std::vector<TypeNode> NodeManager::mkMutualDatatypeTypes(
- const std::vector<DType>& datatypes, uint32_t flags)
+ const std::vector<DType>& datatypes)
{
std::set<TypeNode> unresolvedTypes;
// scan the list of datatypes to find unresolved datatypes
{
dt.collectUnresolvedDatatypeTypes(unresolvedTypes);
}
- return mkMutualDatatypeTypesInternal(datatypes, unresolvedTypes, flags);
+ return mkMutualDatatypeTypesInternal(datatypes, unresolvedTypes);
}
std::vector<TypeNode> NodeManager::mkMutualDatatypeTypesInternal(
const std::vector<DType>& datatypes,
- const std::set<TypeNode>& unresolvedTypes,
- uint32_t flags)
+ const std::set<TypeNode>& unresolvedTypes)
{
std::map<std::string, TypeNode> nameResolutions;
std::vector<TypeNode> dtts;
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);
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))
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);
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();
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;
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
/** 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
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<TypeNode> mkMutualDatatypeTypes(
- const std::vector<DType>& datatypes, uint32_t flags = DATATYPE_FLAG_NONE);
+ const std::vector<DType>& datatypes);
/**
* Make a type representing a constructor with the given argument (subfield)
/** 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);
*/
std::vector<TypeNode> mkMutualDatatypeTypesInternal(
const std::vector<DType>& datatypes,
- const std::set<TypeNode>& unresolvedTypes,
- uint32_t flags = DATATYPE_FLAG_NONE);
+ const std::set<TypeNode>& unresolvedTypes);
typedef std::unordered_set<expr::NodeValue*,
expr::NodeValuePoolHashFunction,
{
expr::NodeValue nv;
expr::NodeValue* child[N];
- }; /* struct NodeManager::NVStorage<N> */
+ };
/**
* A map of tuple and record types to their corresponding datatype.
bool d_initialized;
- size_t next_id;
+ /** The next node identifier */
+ size_t d_nextId;
expr::attr::AttributeManager* d_attrManager;
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,
{
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
util::ITEUtilities d_iteUtilities;
Statistics d_statistics;
-
- static const uint32_t zombieHuntThreshold = 524288;
};
} // namespace passes
{
datatypes.push_back(sdts[i].getDatatype());
}
- std::vector<TypeNode> types = nm->mkMutualDatatypeTypes(
- datatypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
+ std::vector<TypeNode> types = nm->mkMutualDatatypeTypes(datatypes);
Trace("srs-input") << "...finished." << std::endl;
Assert(types.size() == datatypes.size());
std::map<Node, TypeNode> subtermTypes;
// 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)
datatypes.push_back(sdts[i].getDatatype());
}
// make the datatype types
- std::vector<TypeNode> datatypeTypes = nm->mkMutualDatatypeTypes(
- datatypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
+ std::vector<TypeNode> datatypeTypes = nm->mkMutualDatatypeTypes(datatypes);
TypeNode sdtS = datatypeTypes[0];
if (TraceIsOn("dtsygus-gen-debug"))
{
sdt.initializeDatatype(nm->integerType(), bvl, false, false);
std::vector<DType> datatypes;
datatypes.push_back(sdt.getDatatype());
- std::vector<TypeNode> dtypes = nm->mkMutualDatatypeTypes(
- datatypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
+ std::vector<TypeNode> 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);
}
Trace("sygus-grammar-def") << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl;
Assert(!datatypes.empty());
- std::vector<TypeNode> types = NodeManager::currentNM()->mkMutualDatatypeTypes(
- datatypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
+ std::vector<TypeNode> types =
+ NodeManager::currentNM()->mkMutualDatatypeTypes(datatypes);
Trace("sygus-grammar-def") << "...finished" << std::endl;
Assert(types.size() == datatypes.size());
return types[0];
datatypes.push_back(sdts[i].getDatatype());
}
std::vector<TypeNode> types =
- NodeManager::currentNM()->mkMutualDatatypeTypes(
- datatypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
+ NodeManager::currentNM()->mkMutualDatatypeTypes(datatypes);
Assert(types.size() == 1);
return types[0];
}
Trace("sygus-grammar-normalize-build") << "\n";
}
Assert(d_dt_all.size() == d_unres_t_all.size());
- std::vector<TypeNode> types = NodeManager::currentNM()->mkMutualDatatypeTypes(
- d_dt_all, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
+ std::vector<TypeNode> types =
+ NodeManager::currentNM()->mkMutualDatatypeTypes(d_dt_all);
Assert(types.size() == d_dt_all.size());
/* Clear accumulators */
d_dt_all.clear();
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();
/** 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.
*/
Node callRewriteEquality(theory::TheoryId theoryId, TNode equality);
- void clearCachesInternal();
-
/**
* Has n been rewritten with proofs? This checks if n is in d_tpgNodes.
*/
Rewriter::Rewriter() : d_resourceManager(nullptr), d_tpg(nullptr) {}
-void Rewriter::clearCachesInternal()
-{
- typedef cvc5::internal::expr::attr::AttributeUniqueId AttributeUniqueId;
- std::vector<AttributeUniqueId> preids;
- // clang-format off
- ${pre_rewrite_attribute_ids} // clang-format on
-
- std::vector<AttributeUniqueId>
- postids;
- // clang-format off
- ${post_rewrite_attribute_ids} // clang-format on
-
- std::vector<const AttributeUniqueId*>
- 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
projects / cvc5.git / commitdiff