adds new feature: re.loop

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index f987de2f12a13de3b7c3ddb5f649e71d50fc2973..518c30e81e403ff3fb34e708def2b81cdc777776 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1346,6 +1346,7 @@ builtinOp[CVC4::Kind& kind]
   | REPLUS_TOK     { $kind = CVC4::kind::REGEXP_PLUS; }
   | REOPT_TOK      { $kind = CVC4::kind::REGEXP_OPT; }
   | RERANGE_TOK    { $kind = CVC4::kind::REGEXP_RANGE; }
+  | RELOOP_TOK    { $kind = CVC4::kind::REGEXP_LOOP; }
 
   // NOTE: Theory operators go here
   ;
@@ -1721,6 +1722,7 @@ RESTAR_TOK : 're.*';
 REPLUS_TOK : 're.+';
 REOPT_TOK : 're.opt';
 RERANGE_TOK : 're.range';
+RELOOP_TOK : 're.loop';
 RENOSTR_TOK : 're.nostr';
 REALLCHAR_TOK : 're.allchar';
 

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 6485670b5e614a40bb92914182be2006a9230f0f..4063193399f57c3c8e69c348451b60cfe19e3032 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -347,6 +347,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::REGEXP_PLUS: out << "re.+ "; break;
   case kind::REGEXP_OPT: out << "re.opt "; break;
   case kind::REGEXP_RANGE: out << "re.range "; break;
+  case kind::REGEXP_LOOP: out << "re.loop "; break;
   case kind::REGEXP_EMPTY: out << "re.nostr "; break;
   case kind::REGEXP_SIGMA: out << "re.allchar "; break;
 

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index b28c2fd9d717ccb1ed7b2b57467e5ba450f4993f..67b60fdfea64c83f1034e6c8097ba345d1da7ede 100644 (file)
--- 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 52c76880bd2848f85cb56794625b81866accdcd8..033c860fd53c0e7a66f7abf52866bfff29ae7ba8 100644 (file)
--- 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;\r
        return intersectInternal(r1, r2, cache, spflag);\r
 }\r
+\r
+Node RegExpOpr::complement(Node r, int &ret) {\r
+       Node rNode;\r
+       ret = 1;\r
+       if(d_compl_cache.find(r) != d_compl_cache.end()) {\r
+               rNode = d_compl_cache[r].first;\r
+               ret = d_compl_cache[r].second;\r
+       } else {\r
+               if(r == d_emptyRegexp) {\r
+                       rNode = d_sigma_star;\r
+               } else if(r == d_emptySingleton) {\r
+                       rNode = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, d_sigma, d_sigma_star);\r
+               } else if(!checkConstRegExp(r)) {\r
+                       //TODO: var to be extended\r
+                       ret = 0;\r
+               } else {\r
+                       std::set<unsigned> cset;\r
+                       SetNodes vset;\r
+                       firstChars(r, cset, vset);\r
+                       Assert(!vset.empty(), "Regexp 1298 Error");\r
+                       std::vector< Node > vec_nodes;\r
+                       for(unsigned i=0; i<d_card; i++) {\r
+                               CVC4::String c = CVC4::String::convertUnsignedIntToChar(i);\r
+                               Node n = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c));\r
+                               Node r2;\r
+                               if(cset.find(i) == cset.end()) {\r
+                                       r2 = d_sigma_star;\r
+                               } else {\r
+                                       int rt;\r
+                                       derivativeS(r, c, r2);\r
+                                       if(r2 == r) {\r
+                                               r2 = d_emptyRegexp;\r
+                                       } else {\r
+                                               r2 = complement(r2, rt);\r
+                                       }\r
+                               }\r
+                               n = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, n, r2));\r
+                               vec_nodes.push_back(n);\r
+                       }\r
+                       rNode = vec_nodes.size()==0? d_emptyRegexp : vec_nodes.size()==1? vec_nodes[0] :\r
+                                               NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes);\r
+               }\r
+               std::pair< Node, int > p(rNode, ret);\r
+               d_compl_cache[r] = p;\r
+       }\r
+       Trace("regexp-compl") << "COMPL( " << mkString(r) << " ) = " << mkString(rNode) << ", ret=" << ret << std::endl;\r
+       return rNode;\r
+}\r
 //printing\r
 std::string RegExpOpr::niceChar( Node r ) {\r
        if(r.isConst()) {\r

diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index fcac28890e1778e53ee31d197e36d479f8a16ecd..11686882048f0f25a2f0fb7bf76b220c6f6174c1 100644 (file)
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -54,10 +54,10 @@ private:
        \r
        std::map< PairNodes, Node > d_simpl_cache;\r
        std::map< PairNodes, Node > d_simpl_neg_cache;\r
-       std::map< Node, Node > d_compl_cache;\r
        std::map< Node, std::pair< int, Node > > d_delta_cache;\r
        std::map< PairNodeStr, Node > d_dv_cache;\r
        std::map< PairNodeStr, std::pair< Node, int > > d_deriv_cache;\r
+       std::map< Node, std::pair< Node, int > > d_compl_cache;\r
        std::map< Node, bool > d_cstre_cache;\r
        std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_cset_cache;\r
        std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_fset_cache;\r
@@ -86,6 +86,7 @@ public:
        Node derivativeSingle( Node r, CVC4::String c );\r
        bool guessLength( Node r, int &co );\r
        Node intersect(Node r1, Node r2, bool &spflag);\r
+       Node complement(Node r, int &ret);\r
 \r
        std::string mkString( Node r );\r
 };\r

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 3f576d4f582af7530f3a95a522dc76bd97004dc4..a19d35d4b8f0bc647961c234aeb6e11456fd5173 100644 (file)
--- 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 7196dc8f23047da8d832a0f0e71af589dc90831f..42962308d925b2d3eca80fd380ddb604ad87b3e4 100644 (file)
--- 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 7eb4ac3d01a07951dfec7159acd6d65cdccf986d..eef8f980571bfd3357e709057fd23bee5d932bcb 100644 (file)
--- 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();
   }
 };

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index e820765201ed3a8668782c200917a16b1fd2c86e..9977da6a5ef6d062a61b517fba6241d0cd149a6e 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -44,13 +44,13 @@ TESTS =     \
   loop006.smt2 \
   loop007.smt2 \
   loop008.smt2 \
-  loop009.smt2
-
-#regexp002.smt2
+  loop009.smt2 \
+  reloop.smt2
 
 FAILING_TESTS =
 
 EXTRA_DIST = $(TESTS) \
+  regexp002.smt2 \
   type002.smt2
 
 # and make sure to distribute it

diff --git a/test/regress/regress0/strings/reloop.smt2 b/test/regress/regress0/strings/reloop.smt2
new file mode 100644 (file)
index 0000000..f546071
--- /dev/null
+++ b/test/regress/regress0/strings/reloop.smt2
@@ -0,0 +1,17 @@
+(set-logic QF_S)\r
+(set-info :status sat)\r
+\r
+(declare-fun x () String)\r
+(declare-fun y () String)\r
+(declare-fun z () String)\r
+(declare-fun w () String)\r
+\r
+(assert (str.in.re x (re.loop (str.to.re "a") 5)))\r
+(assert (str.in.re y (re.loop (str.to.re "b") 2 5)))\r
+(assert (str.in.re z (re.loop (str.to.re "c") 5)))\r
+(assert (> (str.len z) 7))\r
+(assert (str.in.re w (re.loop (str.to.re "b") 2 7)))\r
+(assert (> (str.len w) 2))\r
+(assert (< (str.len w) 5))\r
+\r
+(check-sat)\r