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.h | |
| 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.h')
| -rw-r--r-- | src/expr/node_manager.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index f47795c15..61ef1d39d 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -43,6 +43,8 @@ namespace CVC4 { class StatisticsRegistry; class ResourceManager; +class DType; + namespace expr { namespace attr { class AttributeUniqueId; @@ -429,6 +431,7 @@ public: unsigned registerDatatype(Datatype* dt); /** get datatype for index */ const Datatype & getDatatypeForIndex( unsigned index ) const; + const DType& getDTypeForIndex(unsigned index) const; /** Get a Kind from an operator expression */ static inline Kind operatorToKind(TNode n); |