From 70a7ae4dc962e43c38cec19a5549673a46045d71 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Thu, 27 Mar 2014 16:54:46 -0500 Subject: [PATCH] adds new feature: re.loop --- src/parser/smt2/Smt2.g | 2 + src/printer/smt2/smt2_printer.cpp | 1 + src/theory/strings/kinds | 2 + src/theory/strings/regexp_operation.cpp | 48 +++ src/theory/strings/theory_strings.cpp | 52 +-- .../strings/theory_strings_rewriter.cpp | 39 +++ .../strings/theory_strings_type_rules.h | 296 ++++++++++-------- test/regress/regress0/strings/Makefile.am | 6 +- test/regress/regress0/strings/reloop.smt2 | 17 + 9 files changed, 314 insertions(+), 149 deletions(-) create mode 100644 test/regress/regress0/strings/reloop.smt2 diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index f987de2f1..518c30e81 100644 --- 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 6485670b5..406319339 100644 --- 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 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 d02baf3a7..8cb8c124a 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -1293,6 +1293,54 @@ Node RegExpOpr::intersect(Node r1, Node r2, bool &spflag) { 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 cset; + SetNodes vset; + firstChars(r, cset, vset); + Assert(!vset.empty(), "Regexp 1298 Error"); + std::vector< Node > vec_nodes; + for(unsigned i=0; imkNode(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/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(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(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().getNumerator().toUnsignedInt(); + std::vector< Node > vec_nodes; + for(unsigned i=0; imkNode(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().getNumerator().toUnsignedInt(); + if(u <= l) { + retNode = n; + } else { + std::vector< Node > vec2; + vec2.push_back(n); + for(unsigned j=l; jmkNode(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().size() != 1 ) { + throw TypeCheckingExceptionPrivate(n, "expecting a single constant string term in regexp range"); + } + ch[i] = (*it).getConst().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().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().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 e82076520..9977da6a5 100644 --- 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 index 000000000..f54607121 --- /dev/null +++ b/test/regress/regress0/strings/reloop.smt2 @@ -0,0 +1,17 @@ +(set-logic QF_S) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) +(declare-fun w () String) + +(assert (str.in.re x (re.loop (str.to.re "a") 5))) +(assert (str.in.re y (re.loop (str.to.re "b") 2 5))) +(assert (str.in.re z (re.loop (str.to.re "c") 5))) +(assert (> (str.len z) 7)) +(assert (str.in.re w (re.loop (str.to.re "b") 2 7))) +(assert (> (str.len w) 2)) +(assert (< (str.len w) 5)) + +(check-sat) -- 2.30.2