From a08f9d1f33c110ded40ee395d328de1fac087463 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 14 Apr 2016 10:28:34 -0500 Subject: [PATCH] Add missing function for regexp to expr manager. --- src/expr/expr_manager_template.cpp | 5 ++++ src/expr/expr_manager_template.h | 3 +++ src/expr/node_manager.h | 4 +-- src/expr/type.cpp | 11 ++++++++ src/expr/type.h | 19 ++++++++++++++ .../strings/theory_strings_type_rules.h | 26 +++++++++---------- 6 files changed, 53 insertions(+), 15 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(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; @@ -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 e304fb794..eae993545 100644 --- 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(); } }; -- 2.30.2