adds new feature: re.loop

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();
   }
 };