STRING_TYPE and CONST_STRING and associate type infrastructure implemented.

1 files changed, 8 insertions, 0 deletions

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 84ed78662..adba8087c 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -515,6 +515,9 @@ public:
   /** Get the (singleton) type for pseudobooleans. */
   inline TypeNode pseudobooleanType();
 
+  /** Get the (singleton) type for strings. */
+  inline TypeNode stringType();
+
   /** Get the (singleton) type for sorts. */
   inline TypeNode kindType();
 
@@ -780,6 +783,11 @@ inline TypeNode NodeManager::pseudobooleanType() {
   return TypeNode(mkTypeConst<TypeConstant>(PSEUDOBOOLEAN_TYPE));
 }
 
+/** Get the (singleton) type for strings. */
+inline TypeNode NodeManager::stringType() {
+  return TypeNode(mkTypeConst<TypeConstant>(STRING_TYPE));
+}
+
 /** Get the (singleton) type for sorts. */
 inline TypeNode NodeManager::kindType() {
   return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE));