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 | |
parent | 2f4925e3d366bf58437025e0a5b238468e6514f8 (diff) |
adds regular expression range
Diffstat (limited to 'src')
-rw-r--r-- | src/parser/smt2/Smt2.g | 2 | ||||
-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 | ||||
-rw-r--r-- | src/util/regexp.h | 8 |
5 files changed, 59 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 885a7c487..c7e088124 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1255,6 +1255,7 @@ builtinOp[CVC4::Kind& kind] | RESTAR_TOK { $kind = CVC4::kind::REGEXP_STAR; } | REPLUS_TOK { $kind = CVC4::kind::REGEXP_PLUS; } | REOPT_TOK { $kind = CVC4::kind::REGEXP_OPT; } + | RERANGE_TOK { $kind = CVC4::kind::REGEXP_RANGE; } // NOTE: Theory operators go here ; @@ -1628,6 +1629,7 @@ REINTER_TOK : 're.itr'; RESTAR_TOK : 're.*'; REPLUS_TOK : 're.+'; REOPT_TOK : 're.opt'; +RERANGE_TOK : 're.range'; /** * A sequence of printable ASCII characters (except backslash) that starts 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) diff --git a/src/util/regexp.h b/src/util/regexp.h index 31a39e6f9..024bfd32e 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -57,6 +57,10 @@ public: } } + String(const char c) { + d_str.push_back( convertCharToUnsignedInt(c) ); + } + String(const std::vector<unsigned int> &s) : d_str(s) { } ~String() {} @@ -151,6 +155,10 @@ public: return d_str.size(); } + char getFirstChar() const { + return convertUnsignedIntToChar( d_str[0] ); + } + String substr(unsigned i) const { std::vector<unsigned int> ret_vec; std::vector<unsigned int>::const_iterator itr = d_str.begin() + i; |