diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-14 10:28:34 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-14 11:01:35 -0500 |
commit | a08f9d1f33c110ded40ee395d328de1fac087463 (patch) | |
tree | d999c0482bcd3dd1104d03d03859765545a7a6c8 /src/expr | |
parent | d87431b64a27c073e31652166a24f0c87b22c041 (diff) |
Add missing function for regexp to expr manager.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 5 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 3 | ||||
-rw-r--r-- | src/expr/node_manager.h | 4 | ||||
-rw-r--r-- | src/expr/type.cpp | 11 | ||||
-rw-r--r-- | src/expr/type.h | 19 |
5 files changed, 40 insertions, 2 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 4475554b1..84f674d2b 100644 --- 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 72fa5d1b6..04f2f4289 100644 --- 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 7fa93d38d..7d2b13e4c 100644 --- 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 5b4fef395..0c4d554ef 100644 --- 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 a2d6207fb..43cb3ffbf 100644 --- 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; @@ -258,6 +259,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 */ @@ -424,6 +431,18 @@ public: };/* 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. */ class CVC4_PUBLIC RoundingModeType : public Type { |