diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-06 01:22:01 -0600 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-05 23:22:01 -0800 |
commit | 46bae5d2a8b22867f917c6f644e46e29884049f9 (patch) | |
tree | a915862a8b8fda9d50b2fbed950640f8da280f7d /src/expr/node_manager.cpp | |
parent | 643e4d5369734923267694c55363ec0456f18263 (diff) |
Introduce the Node-level Datatypes API (#3462)
This adds classes corresponding to the Node-level Datatype API "DType", which is a specification for a datatype type. It does not enable the use of this layer yet. A followup PR will update the Expr-level Datatype to use the Node-level code, which is currently verified to be functional on this branch: https://github.com/ajreynol/CVC4/tree/dtype-integrate. Futher PRs will make the internal (Node-level) code forgo the use of the Expr-layer datatype, which will then enable the Expr-layer to be replaced by the Term-layer datatype.
Most of the documentation for the methods in DType/DTypeConstructor/DTypeSelector was copied from Datatype/DatatypeConstructor/DatatypeConstructorArg.
Diffstat (limited to 'src/expr/node_manager.cpp')
-rw-r--r-- | src/expr/node_manager.cpp | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 5223fd02c..201e428de 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -24,6 +24,7 @@ #include "base/check.h" #include "base/listener.h" #include "expr/attribute.h" +#include "expr/dtype.h" #include "expr/node_manager_attributes.h" #include "expr/node_manager_listeners.h" #include "expr/type_checker.h" @@ -186,6 +187,7 @@ NodeManager::~NodeManager() { d_rt_cache.d_children.clear(); d_rt_cache.d_data = dummy; + // TODO: switch to DType for (std::vector<Datatype*>::iterator datatype_iter = d_ownedDatatypes.begin(), datatype_end = d_ownedDatatypes.end(); @@ -253,10 +255,22 @@ unsigned NodeManager::registerDatatype(Datatype* dt) { } const Datatype & NodeManager::getDatatypeForIndex( unsigned index ) const{ + // when the Node-level API is in place, this function will be deleted. Assert(index < d_ownedDatatypes.size()); return *d_ownedDatatypes[index]; } +const DType& NodeManager::getDTypeForIndex(unsigned index) const +{ + // when the Node-level API is in place, this function will be replaced by a + // direct lookup into a d_ownedDTypes vector, similar to d_ownedDatatypes + // above. + Unreachable() << "NodeManager::getDTypeForIndex: DType is not available in " + "the current implementation."; + const Datatype& d = getDatatypeForIndex(index); + return *d.d_internal; +} + void NodeManager::reclaimZombies() { // FIXME multithreading Assert(!d_attrManager->inGarbageCollection()); |