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