Theory of strings.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

1 files changed, 8 insertions, 0 deletions

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index a65655501..31f6d75d9 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -683,6 +683,9 @@ public:
   /** Get the (singleton) type for strings. */
   inline TypeNode stringType();
 
+  /** Get the (singleton) type for RegExp. */
+  inline TypeNode regexpType();
+
   /** Get the bound var list type. */
   inline TypeNode boundVarListType();
 
@@ -1030,6 +1033,11 @@ inline TypeNode NodeManager::stringType() {
   return TypeNode(mkTypeConst<TypeConstant>(STRING_TYPE));
 }
 
+/** Get the (singleton) type for regexps. */
+inline TypeNode NodeManager::regexpType() {
+  return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE));
+}
+
 /** Get the bound var list type. */
 inline TypeNode NodeManager::boundVarListType() {
   return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE));