Theory of strings.

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

2 files changed, 17 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));
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 061e73fc9..322f7ad92 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -554,6 +554,9 @@ public:
   /** Get the constituent types of a symbolic expression type */
   std::vector<TypeNode> getSExprTypes() const;
 
+  /** Is this a regexp type */
+  bool isRegExp() const;
+
   /** Is this a bit-vector type */
   bool isBitVector() const;
 
@@ -842,6 +845,12 @@ inline bool TypeNode::isString() const {
     getConst<TypeConstant>() == STRING_TYPE;
 }
 
+/** Is this a regexp type */
+inline bool TypeNode::isRegExp() const {
+  return getKind() == kind::TYPE_CONSTANT &&
+    getConst<TypeConstant>() == REGEXP_TYPE;
+}
+
 inline bool TypeNode::isArray() const {
   return getKind() == kind::ARRAY_TYPE;
 }