diff options
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); |