Add missing function for regexp to expr manager.

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 4475554b1387ea7855cfcfe7aafb1523cbe3d36e..84f674d2bb944efcd5327dad40c25adc49fb177f 100644 (file)
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -142,6 +142,11 @@ StringType ExprManager::stringType() const {
   return StringType(Type(d_nodeManager, new TypeNode(d_nodeManager->stringType())));
 }
 
+RegExpType ExprManager::regExpType() const {
+  NodeManagerScope nms(d_nodeManager);
+  return StringType(Type(d_nodeManager, new TypeNode(d_nodeManager->regExpType())));
+}
+
 RealType ExprManager::realType() const {
   NodeManagerScope nms(d_nodeManager);
   return RealType(Type(d_nodeManager, new TypeNode(d_nodeManager->realType())));

diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 72fa5d1b6c857167a83b928c656ffe8e477c96d9..04f2f4289d0137cd29279e893e0e0f730847a985 100644 (file)
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -121,6 +121,9 @@ public:
   /** Get the type for strings. */
   StringType stringType() const;
 
+  /** Get the type for regular expressions. */
+  RegExpType regExpType() const;
+
   /** Get the type for reals. */
   RealType realType() const;
 

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 7fa93d38dedcb4c1ce90ef378aea60115220079a..7d2b13e4c4998da7c7dfe17d3ffb669dea7b6c99 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -705,7 +705,7 @@ public:
   inline TypeNode stringType();
 
   /** Get the (singleton) type for RegExp. */
-  inline TypeNode regexpType();
+  inline TypeNode regExpType();
 
   /** Get the (singleton) type for rounding modes. */
   inline TypeNode roundingModeType();
@@ -1001,7 +1001,7 @@ inline TypeNode NodeManager::stringType() {
 }
 
 /** Get the (singleton) type for regexps. */
-inline TypeNode NodeManager::regexpType() {
+inline TypeNode NodeManager::regExpType() {
   return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE));
 }
 

diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 5b4fef39563a56503200f85aa3998f96443ca86c..0c4d554ef9fb358ce5549098bda0539a356b74c7 100644 (file)
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -223,6 +223,12 @@ bool Type::isString() const {
   return d_typeNode->isString();
 }
 
+/** Is this the regexp type? */
+bool Type::isRegExp() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isRegExp();
+}
+
 /** Is this the rounding mode type? */
 bool Type::isRoundingMode() const {
   NodeManagerScope nms(d_nodeManager);
@@ -427,6 +433,11 @@ StringType::StringType(const Type& t) throw(IllegalArgumentException) :
   PrettyCheckArgument(isNull() || isString(), this);
 }
 
+RegExpType::RegExpType(const Type& t) throw(IllegalArgumentException) :
+  Type(t) {
+  PrettyCheckArgument(isNull() || isRegExp(), this);
+}
+
 RoundingModeType::RoundingModeType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
   PrettyCheckArgument(isNull() || isRoundingMode(), this);

diff --git a/src/expr/type.h b/src/expr/type.h
index a2d6207fb30990790a5c06687ff8c53d04ba32b0..43cb3ffbf699403b9f56c250fa6677a8b5acb09d 100644 (file)
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -47,6 +47,7 @@ class BooleanType;
 class IntegerType;
 class RealType;
 class StringType;
+class RegExpType;
 class RoundingModeType;
 class BitVectorType;
 class ArrayType;
@@ -257,6 +258,12 @@ public:
    */
   bool isString() const;
 
+  /**
+   * Is this the regexp type?
+   * @return true if the type is the regexp type
+   */
+  bool isRegExp() const;
+
   /**
    * Is this the rounding mode type?
    * @return true if the type is the rounding mode type
@@ -423,6 +430,18 @@ public:
   StringType(const Type& type) throw(IllegalArgumentException);
 };/* class StringType */
 
+/**
+ * Singleton class encapsulating the string type.
+ */
+class CVC4_PUBLIC RegExpType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  RegExpType(const Type& type) throw(IllegalArgumentException);
+};/* class RegExpType */
+
+
 /**
  * Singleton class encapsulating the rounding mode type.
  */

diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index e304fb794700cb928bc2ca5c6abee32f3b57c24e..eae993545db0e573e106cac759dcf87e00a44e92 100644 (file)
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -239,7 +239,7 @@ class RegExpConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -262,7 +262,7 @@ public:
          throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in regexp concat");
       }
     }
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -280,7 +280,7 @@ public:
          }
       }
     }
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -298,7 +298,7 @@ public:
        }
       }
     }
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -312,7 +312,7 @@ public:
         throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
       }
     }
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -326,7 +326,7 @@ public:
         throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
       }
     }
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -340,7 +340,7 @@ public:
         throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
       }
     }
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -373,7 +373,7 @@ public:
         throw TypeCheckingExceptionPrivate(n, "expecting standard ASCII characters in regexp range, or please set the option strings-std-ascii to be false");
       }
     }
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -409,7 +409,7 @@ public:
         //}
       }
     }
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -426,7 +426,7 @@ public:
       //  throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
       //}
     }
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -456,7 +456,7 @@ public:
     throw (TypeCheckingExceptionPrivate, AssertionException) {
 
     Assert(n.getKind() == kind::REGEXP_EMPTY);
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -466,7 +466,7 @@ public:
     throw (TypeCheckingExceptionPrivate, AssertionException) {
 
     Assert(n.getKind() == kind::REGEXP_SIGMA);
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -480,7 +480,7 @@ public:
         throw TypeCheckingExceptionPrivate(n, "expecting an integer term in RV");
       }
     }
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };