diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-10-20 21:25:57 -0500 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-10-20 21:28:48 -0500 |
commit | 60aab6e5b7dde21603eb039f37921614d4424d59 (patch) | |
tree | 82636da4881edfbe2a059984557e193de0e1f7da /src/theory/strings | |
parent | 2f4925e3d366bf58437025e0a5b238468e6514f8 (diff) |
adds regular expression range
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/kinds | 2 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 13 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_type_rules.h | 34 |
3 files changed, 49 insertions, 0 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index f4fbd7194..e325708c2 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -70,6 +70,7 @@ operator REGEXP_INTER 2: "regexp intersection" operator REGEXP_STAR 1 "regexp *" operator REGEXP_PLUS 1 "regexp +" operator REGEXP_OPT 1 "regexp ?" +operator REGEXP_RANGE 2 "regexp range" #constant REGEXP_EMPTY \ # ::CVC4::RegExp \ @@ -95,6 +96,7 @@ typerule REGEXP_INTER ::CVC4::theory::strings::RegExpInterTypeRule typerule REGEXP_STAR ::CVC4::theory::strings::RegExpStarTypeRule typerule REGEXP_PLUS ::CVC4::theory::strings::RegExpPlusTypeRule typerule REGEXP_OPT ::CVC4::theory::strings::RegExpOptTypeRule +typerule REGEXP_RANGE ::CVC4::theory::strings::RegExpRangeTypeRule typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 5ba67c25f..95e19c5aa 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -351,6 +351,19 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_OR, NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ), node[0]); + } else if(node.getKind() == kind::REGEXP_RANGE) { + std::vector< Node > vec_nodes; + char c = node[0].getConst<String>().getFirstChar(); + char end = node[1].getConst<String>().getFirstChar(); + for(; c<=end; ++c) { + Node n = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( ::CVC4::String( c ) ) ); + vec_nodes.push_back( n ); + } + if(vec_nodes.size() == 1) { + retNode = vec_nodes[0]; + } else { + retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes ); + } } Trace("strings-prerewrite") << "Strings::preRewrite returning " << retNode << std::endl; diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 8af063284..080d6abf5 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -203,6 +203,40 @@ public: } }; +class RegExpRangeTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + char ch[2]; + + for(int i=0; i<2; ++i) { + TypeNode t = (*it).getType(check); + if (!t.isString()) { + throw TypeCheckingExceptionPrivate(n, "expecting a string term in regexp range"); + } + if( (*it).getKind() != kind::CONST_STRING ) { + throw TypeCheckingExceptionPrivate(n, "expecting a constant string term in regexp range"); + } + if( (*it).getConst<String>().size() != 1 ) { + throw TypeCheckingExceptionPrivate(n, "expecting a single constant string term in regexp range"); + } + ch[i] = (*it).getConst<String>().getFirstChar(); + ++it; + } + if(ch[0] > ch[1]) { + throw TypeCheckingExceptionPrivate(n, "expecting the first constant is less or equal to the second one in regexp range"); + } + + if( it != it_end ) { + throw TypeCheckingExceptionPrivate(n, "too many terms in regexp range"); + } + + return nodeManager->regexpType(); + } +}; + class StringToRegExpTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) |