diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-03-27 16:54:46 -0500 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-03-27 16:54:46 -0500 |
commit | f814750622a50835d4be99b1ced54af5e25d8ed4 (patch) | |
tree | a88850d7f84c9ace1558bd2bbf529a76960fa7c3 /src/theory/strings | |
parent | 2631074ec6d430893c926b294df292893bab68b4 (diff) |
adds new feature: re.loop
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/kinds | 2 | ||||
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 48 | ||||
-rw-r--r-- | src/theory/strings/regexp_operation.h | 3 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 52 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 39 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_type_rules.h | 296 |
6 files changed, 293 insertions, 147 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index b28c2fd9d..67b60fdfe 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -77,6 +77,7 @@ operator REGEXP_STAR 1 "regexp *" operator REGEXP_PLUS 1 "regexp +" operator REGEXP_OPT 1 "regexp ?" operator REGEXP_RANGE 2 "regexp range" +operator REGEXP_LOOP 2:3 "regexp loop" operator REGEXP_EMPTY 0 "regexp empty" operator REGEXP_SIGMA 0 "regexp all charactors" @@ -88,6 +89,7 @@ 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 REGEXP_LOOP ::CVC4::theory::strings::RegExpLoopTypeRule typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 52c76880b..033c860fd 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -1287,6 +1287,54 @@ Node RegExpOpr::intersect(Node r1, Node r2, bool &spflag) { std::map< unsigned, std::set< PairNodes > > cache;
return intersectInternal(r1, r2, cache, spflag);
}
+
+Node RegExpOpr::complement(Node r, int &ret) {
+ Node rNode;
+ ret = 1;
+ if(d_compl_cache.find(r) != d_compl_cache.end()) {
+ rNode = d_compl_cache[r].first;
+ ret = d_compl_cache[r].second;
+ } else {
+ if(r == d_emptyRegexp) {
+ rNode = d_sigma_star;
+ } else if(r == d_emptySingleton) {
+ rNode = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, d_sigma, d_sigma_star);
+ } else if(!checkConstRegExp(r)) {
+ //TODO: var to be extended
+ ret = 0;
+ } else {
+ std::set<unsigned> cset;
+ SetNodes vset;
+ firstChars(r, cset, vset);
+ Assert(!vset.empty(), "Regexp 1298 Error");
+ std::vector< Node > vec_nodes;
+ for(unsigned i=0; i<d_card; i++) {
+ CVC4::String c = CVC4::String::convertUnsignedIntToChar(i);
+ Node n = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c));
+ Node r2;
+ if(cset.find(i) == cset.end()) {
+ r2 = d_sigma_star;
+ } else {
+ int rt;
+ derivativeS(r, c, r2);
+ if(r2 == r) {
+ r2 = d_emptyRegexp;
+ } else {
+ r2 = complement(r2, rt);
+ }
+ }
+ n = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, n, r2));
+ vec_nodes.push_back(n);
+ }
+ rNode = vec_nodes.size()==0? d_emptyRegexp : vec_nodes.size()==1? vec_nodes[0] :
+ NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes);
+ }
+ std::pair< Node, int > p(rNode, ret);
+ d_compl_cache[r] = p;
+ }
+ Trace("regexp-compl") << "COMPL( " << mkString(r) << " ) = " << mkString(rNode) << ", ret=" << ret << std::endl;
+ return rNode;
+}
//printing
std::string RegExpOpr::niceChar( Node r ) {
if(r.isConst()) {
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index fcac28890..116868820 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -54,10 +54,10 @@ private: std::map< PairNodes, Node > d_simpl_cache;
std::map< PairNodes, Node > d_simpl_neg_cache;
- std::map< Node, Node > d_compl_cache;
std::map< Node, std::pair< int, Node > > d_delta_cache;
std::map< PairNodeStr, Node > d_dv_cache;
std::map< PairNodeStr, std::pair< Node, int > > d_deriv_cache;
+ std::map< Node, std::pair< Node, int > > d_compl_cache;
std::map< Node, bool > d_cstre_cache;
std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_cset_cache;
std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_fset_cache;
@@ -86,6 +86,7 @@ public: Node derivativeSingle( Node r, CVC4::String c );
bool guessLength( Node r, int &co );
Node intersect(Node r1, Node r2, bool &spflag);
+ Node complement(Node r, int &ret);
std::string mkString( Node r );
};
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 3f576d4f5..a19d35d4b 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2850,30 +2850,36 @@ bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) { } void TheoryStrings::addMembership(Node assertion) { - d_regexp_memberships.push_back( assertion ); - - if(options::stringEIT()) { - bool polarity = assertion.getKind() != kind::NOT; - if(polarity) { - TNode atom = polarity ? assertion : assertion[0]; - Node x = atom[0]; - Node r = atom[1]; - NodeList* lst; - NodeListMap::iterator itr_xr = d_str_re_map.find( x ); - if( itr_xr == d_str_re_map.end() ){ - lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, - ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); - d_str_re_map.insertDataFromContextMemory( x, lst ); - } else { - lst = (*itr_xr).second; - } - //check - for( NodeList::const_iterator itr = lst->begin(); itr != lst->end(); ++itr ) { - if( r == *itr ) { - return; - } + bool polarity = assertion.getKind() != kind::NOT; + TNode atom = polarity ? assertion : assertion[0]; + Node x = atom[0]; + Node r = atom[1]; + if(polarity) { + NodeList* lst; + NodeListMap::iterator itr_xr = d_str_re_map.find( x ); + if( itr_xr == d_str_re_map.end() ){ + lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, + ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); + d_str_re_map.insertDataFromContextMemory( x, lst ); + } else { + lst = (*itr_xr).second; + } + //check + for( NodeList::const_iterator itr = lst->begin(); itr != lst->end(); ++itr ) { + if( r == *itr ) { + return; } - lst->push_back( r ); + } + lst->push_back( r ); + d_regexp_memberships.push_back( assertion ); + } else { + if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) { + int rt; + Node r2 = d_regexp_opr.complement(r, rt); + Node a = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r2); + d_regexp_memberships.push_back( a ); + } else { + d_regexp_memberships.push_back( assertion ); } } } diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 7196dc8f2..42962308d 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -530,6 +530,10 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { retNode = prerewriteConcatRegExp(node); } else if(node.getKind() == kind::REGEXP_UNION) { retNode = prerewriteOrRegExp(node); + } else if(node.getKind() == kind::REGEXP_STAR) { + if(node[0].getKind() == kind::REGEXP_STAR) { + retNode = node[0]; + } } else if(node.getKind() == kind::REGEXP_PLUS) { retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, node[0], NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, node[0])); @@ -550,6 +554,41 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { } else { retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes ); } + } else if(node.getKind() == kind::REGEXP_LOOP) { + Node r = node[0]; + if(r.getKind() == kind::REGEXP_STAR) { + retNode = r; + } else { + unsigned l = node[1].getConst<Rational>().getNumerator().toUnsignedInt(); + std::vector< Node > vec_nodes; + for(unsigned i=0; i<l; i++) { + vec_nodes.push_back(r); + } + if(node.getNumChildren() == 3) { + Node n = vec_nodes.size()==0 ? NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(CVC4::String(""))) + : vec_nodes.size()==1 ? r : prerewriteConcatRegExp(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_nodes)); + unsigned u = node[2].getConst<Rational>().getNumerator().toUnsignedInt(); + if(u <= l) { + retNode = n; + } else { + std::vector< Node > vec2; + vec2.push_back(n); + for(unsigned j=l; j<u; j++) { + vec_nodes.push_back(r); + n = vec_nodes.size()==1? r : prerewriteConcatRegExp(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_nodes)); + vec2.push_back(n); + } + retNode = prerewriteOrRegExp(NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec2)); + } + } else { + Node rest = NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, r); + retNode = vec_nodes.size()==0? rest : prerewriteConcatRegExp( vec_nodes.size()==1? + NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, r, rest) + :NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, + NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_nodes), rest) ); + } + } + Trace("strings-lp") << "Strings::lp " << node << " => " << retNode << std::endl; } 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 7eb4ac3d0..eef8f9805 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -35,18 +35,20 @@ class StringConcatTypeRule { 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(); - int size = 0; - for (; it != it_end; ++ it) { - TypeNode t = (*it).getType(check); - if (!t.isString()) { - throw TypeCheckingExceptionPrivate(n, "expecting string terms in string concat"); - } - ++size; - } - if(size < 2) { - throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in string concat"); + if( check ){ + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + int size = 0; + for (; it != it_end; ++ it) { + TypeNode t = (*it).getType(check); + if (!t.isString()) { + throw TypeCheckingExceptionPrivate(n, "expecting string terms in string concat"); + } + ++size; + } + if(size < 2) { + throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in string concat"); + } } return nodeManager->stringType(); } @@ -56,7 +58,7 @@ class StringLengthTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { - if( check ){ + if( check ) { TypeNode t = n[0].getType(check); if (!t.isString()) { throw TypeCheckingExceptionPrivate(n, "expecting string terms in string length"); @@ -70,7 +72,7 @@ class StringSubstrTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { - if( check ){ + if( check ) { TypeNode t = n[0].getType(check); if (!t.isString()) { throw TypeCheckingExceptionPrivate(n, "expecting a string term in substr"); @@ -92,7 +94,7 @@ class StringContainTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { - if( check ){ + if( check ) { TypeNode t = n[0].getType(check); if (!t.isString()) { throw TypeCheckingExceptionPrivate(n, "expecting an orginal string term in string contain"); @@ -110,7 +112,7 @@ class StringCharAtTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { - if( check ){ + if( check ) { TypeNode t = n[0].getType(check); if (!t.isString()) { throw TypeCheckingExceptionPrivate(n, "expecting a string term in string char at 0"); @@ -128,7 +130,7 @@ class StringIndexOfTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { - if( check ){ + if( check ) { TypeNode t = n[0].getType(check); if (!t.isString()) { throw TypeCheckingExceptionPrivate(n, "expecting a string term in string indexof 0"); @@ -150,7 +152,7 @@ class StringReplaceTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { - if( check ){ + if( check ) { TypeNode t = n[0].getType(check); if (!t.isString()) { throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 0"); @@ -244,18 +246,20 @@ class RegExpConcatTypeRule { 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(); - int size = 0; - for (; it != it_end; ++ it) { - TypeNode t = (*it).getType(check); - if (!t.isRegExp()) { - throw TypeCheckingExceptionPrivate(n, "expecting regexp terms in regexp concat"); - } - ++size; - } - if(size < 2) { - throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in regexp concat"); + if( check ) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + int size = 0; + for (; it != it_end; ++ it) { + TypeNode t = (*it).getType(check); + if (!t.isRegExp()) { + throw TypeCheckingExceptionPrivate(n, "expecting regexp terms in regexp concat"); + } + ++size; + } + if(size < 2) { + throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in regexp concat"); + } } return nodeManager->regexpType(); } @@ -265,14 +269,16 @@ class RegExpUnionTypeRule { 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(); - for (; it != it_end; ++ it) { - TypeNode t = (*it).getType(check); - if (!t.isRegExp()) { - throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); - } - } + if( check ) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + for (; it != it_end; ++ it) { + TypeNode t = (*it).getType(check); + if (!t.isRegExp()) { + throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); + } + } + } return nodeManager->regexpType(); } }; @@ -281,14 +287,16 @@ class RegExpInterTypeRule { 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(); - for (; it != it_end; ++ it) { - TypeNode t = (*it).getType(check); - if (!t.isRegExp()) { - throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); - } - } + if( check ) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + for (; it != it_end; ++ it) { + TypeNode t = (*it).getType(check); + if (!t.isRegExp()) { + throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); + } + } + } return nodeManager->regexpType(); } }; @@ -297,16 +305,17 @@ class RegExpStarTypeRule { 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(); - TypeNode t = (*it).getType(check); - if (!t.isRegExp()) { - throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); - } - if(++it != it_end) { - throw TypeCheckingExceptionPrivate(n, "too many regexp"); - } - + if( check ) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + TypeNode t = (*it).getType(check); + if (!t.isRegExp()) { + throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); + } + if(++it != it_end) { + throw TypeCheckingExceptionPrivate(n, "too many regexp"); + } + } return nodeManager->regexpType(); } }; @@ -315,16 +324,17 @@ class RegExpPlusTypeRule { 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(); - TypeNode t = (*it).getType(check); - if (!t.isRegExp()) { - throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); - } - if(++it != it_end) { - throw TypeCheckingExceptionPrivate(n, "too many regexp"); - } - + if( check ) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + TypeNode t = (*it).getType(check); + if (!t.isRegExp()) { + throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); + } + if(++it != it_end) { + throw TypeCheckingExceptionPrivate(n, "too many regexp"); + } + } return nodeManager->regexpType(); } }; @@ -333,16 +343,17 @@ class RegExpOptTypeRule { 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(); - TypeNode t = (*it).getType(check); - if (!t.isRegExp()) { - throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); - } - if(++it != it_end) { - throw TypeCheckingExceptionPrivate(n, "too many regexp"); - } - + if( check ) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + TypeNode t = (*it).getType(check); + if (!t.isRegExp()) { + throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); + } + if(++it != it_end) { + throw TypeCheckingExceptionPrivate(n, "too many regexp"); + } + } return nodeManager->regexpType(); } }; @@ -351,32 +362,69 @@ 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]; + if( check ) { + 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"); + } - for(int i=0; i<2; ++i) { + if( it != it_end ) { + throw TypeCheckingExceptionPrivate(n, "too many terms in regexp range"); + } + } + return nodeManager->regexpType(); + } +}; + +class RegExpLoopTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + if( check ) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); TypeNode t = (*it).getType(check); - if (!t.isString()) { - throw TypeCheckingExceptionPrivate(n, "expecting a string term in regexp range"); + if (!t.isRegExp()) { + throw TypeCheckingExceptionPrivate(n, "expecting a regexp term in regexp loop 1"); } - if( (*it).getKind() != kind::CONST_STRING ) { - throw TypeCheckingExceptionPrivate(n, "expecting a constant string term in regexp range"); + ++it; t = (*it).getType(check); + if (!t.isInteger()) { + throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 2"); } - if( (*it).getConst<String>().size() != 1 ) { - throw TypeCheckingExceptionPrivate(n, "expecting a single constant string term in regexp range"); + if(!(*it).isConst()) { + throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 2"); } - ch[i] = (*it).getConst<String>().getFirstChar(); ++it; + if(it != it_end) { + t = (*it).getType(check); + if (!t.isInteger()) { + throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 3"); + } + if(!(*it).isConst()) { + throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 3"); + } + //if(++it != it_end) { + // throw TypeCheckingExceptionPrivate(n, "too many regexp"); + //} + } } - 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(); } }; @@ -385,19 +433,20 @@ class StringToRegExpTypeRule { 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(); - TypeNode t = (*it).getType(check); - if (!t.isString()) { - throw TypeCheckingExceptionPrivate(n, "expecting string terms"); - } - //if( (*it).getKind() != kind::CONST_STRING ) { - // throw TypeCheckingExceptionPrivate(n, "expecting constant string terms"); - //} - if(++it != it_end) { - throw TypeCheckingExceptionPrivate(n, "too many terms"); - } - + if( check ) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + TypeNode t = (*it).getType(check); + if (!t.isString()) { + throw TypeCheckingExceptionPrivate(n, "expecting string terms"); + } + //if( (*it).getKind() != kind::CONST_STRING ) { + // throw TypeCheckingExceptionPrivate(n, "expecting constant string terms"); + //} + if(++it != it_end) { + throw TypeCheckingExceptionPrivate(n, "too many terms"); + } + } return nodeManager->regexpType(); } }; @@ -406,21 +455,22 @@ class StringInRegExpTypeRule { 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(); - TypeNode t = (*it).getType(check); - if (!t.isString()) { - throw TypeCheckingExceptionPrivate(n, "expecting string terms"); - } - ++it; - t = (*it).getType(check); - if (!t.isRegExp()) { - throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); - } - if(++it != it_end) { - throw TypeCheckingExceptionPrivate(n, "too many terms"); - } - + if( check ) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + TypeNode t = (*it).getType(check); + if (!t.isString()) { + throw TypeCheckingExceptionPrivate(n, "expecting string terms"); + } + ++it; + t = (*it).getType(check); + if (!t.isRegExp()) { + throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); + } + if(++it != it_end) { + throw TypeCheckingExceptionPrivate(n, "too many terms"); + } + } return nodeManager->booleanType(); } }; |