From: Tianyi Liang Date: Mon, 14 Oct 2013 21:27:33 +0000 (-0500) Subject: Adds Regular Expression support. X-Git-Tag: cvc5-1.0.0~7275^2~21 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=177f347c7db9ef276dbaebe166080abc78a2bf73;p=cvc5.git Adds Regular Expression support. --- diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 9f33e9191..cfc9fa77e 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -903,10 +903,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v // for some y,z,k Trace("strings-loop") << "Must add lemma." << std::endl; - //need to break - Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); - Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); - Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + Trace("strings-loop") << "Cache: " << normal_form_src[i] << " vs " << normal_form_src[j] << std::endl; antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); //require that x is non-empty @@ -920,55 +917,77 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v d_pending_req_phase[ x_empty ] = true; - //t1 * ... * tn = y * z - std::vector< Node > c1c; - //n[loop_n_index][index]....n[loop_n_index][loop_lindex-1] - for( int r=index; r<=loop_index-1; r++ ) { - c1c.push_back( normal_forms[loop_n_index][r] ); - } - Node conc1 = mkConcat( c1c ); - conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, conc1, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) ); - std::vector< Node > c2c; - //s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] - for( int r=other_index+1; r < (int)normal_forms[other_n_index].size(); r++ ) { - c2c.push_back( normal_forms[other_n_index][r] ); - } - Node left2 = mkConcat( c2c ); - std::vector< Node > c3c; - c3c.push_back( sk_z ); - c3c.push_back( sk_y ); - //r1 * ... * rk = n[loop_n_index][loop_index+1]....n[loop_n_index][loop_index-1] - for( int r=loop_index+1; r < (int)normal_forms[loop_n_index].size(); r++ ) { - c3c.push_back( normal_forms[loop_n_index][r] ); - } - Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, left2, - mkConcat( c3c ) ); - Node conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( sk_y, sk_w ) ); - Node conc4 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, - NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, - NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, mkConcat( sk_z, sk_y ) ) ) ); - unrollStar( conc4 ); - - Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y ); - //Node sk_z_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_z ); - //Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y_len, d_zero); - //Node len_z_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z_len, d_zero); - //Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y, d_emptyString); - //Node zz_imp_yz = NodeManager::currentNM()->mkNode( kind::IMPLIES, len_z_eq_zero, len_y_eq_zero); - - //Node z_neq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z, d_emptyString).negate(); - //Node len_x_gt_len_y = NodeManager::currentNM()->mkNode( kind::GT, - // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, normal_forms[other_n_index][other_index]), - // sk_y_len ); + //need to break + Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); Node ant = mkExplain( antec, antec_new_lits ); - conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2, conc3, conc4 );//, x_eq_y_rest );// , z_neq_empty //, len_x_gt_len_y - - //Node x_eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], d_emptyString); - //conc = NodeManager::currentNM()->mkNode( kind::OR, x_eq_empty, conc ); + if(index == loop_index - 1 && + other_index + 2 == (int) normal_forms[other_n_index].size() && + loop_index + 1 == (int) normal_forms[loop_n_index].size() && + normal_forms[loop_n_index][index] == normal_forms[other_n_index][other_index + 1] && + normal_forms[loop_n_index][index].isConst() ) { + Trace("strings-loop") << "Special case (X)=" << normal_forms[other_n_index][other_index] << " " << std::endl; + Trace("strings-loop") << "... (C)=" << normal_forms[loop_n_index][index] << " " << std::endl; + //special case + Node conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( normal_forms[loop_n_index][index], sk_w ) ); + Node conc4 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, + NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, + NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, normal_forms[loop_n_index][index] ) ) ); + unrollStar( conc4 ); + conc = conc4; + } else { + Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + //t1 * ... * tn = y * z + std::vector< Node > c1c; + //n[loop_n_index][index]....n[loop_n_index][loop_lindex-1] + for( int r=index; r<=loop_index-1; r++ ) { + c1c.push_back( normal_forms[loop_n_index][r] ); + } + Node conc1 = mkConcat( c1c ); + conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, conc1, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) ); + std::vector< Node > c2c; + //s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] + for( int r=other_index+1; r < (int)normal_forms[other_n_index].size(); r++ ) { + c2c.push_back( normal_forms[other_n_index][r] ); + } + Node left2 = mkConcat( c2c ); + std::vector< Node > c3c; + c3c.push_back( sk_z ); + c3c.push_back( sk_y ); + //r1 * ... * rk = n[loop_n_index][loop_index+1]....n[loop_n_index][loop_index-1] + for( int r=loop_index+1; r < (int)normal_forms[loop_n_index].size(); r++ ) { + c3c.push_back( normal_forms[loop_n_index][r] ); + } + Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, left2, + mkConcat( c3c ) ); + Node conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( sk_y, sk_w ) ); + Node conc4 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, + NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, + NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, mkConcat( sk_z, sk_y ) ) ) ); + unrollStar( conc4 ); + + //Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y ); + //Node sk_z_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_z ); + //Node len_z_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_z_len, d_zero ); + //Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y_len, d_zero); + //Node len_z_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z_len, d_zero); + //Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y, d_emptyString); + //Node zz_imp_yz = NodeManager::currentNM()->mkNode( kind::IMPLIES, sk_z.eqNode(d_emptyString), sk_y.eqNode(d_emptyString)); + + //Node z_neq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z, d_emptyString).negate(); + //Node len_x_gt_len_y = NodeManager::currentNM()->mkNode( kind::GT, + // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, normal_forms[other_n_index][other_index]), + // sk_y_len ); + conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2, conc3, conc4 );//, x_eq_y_rest );// , z_neq_empty //, len_x_gt_len_y + + //Node x_eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], d_emptyString); + //conc = NodeManager::currentNM()->mkNode( kind::OR, x_eq_empty, conc ); + } // normal case //we will be done addNormalFormPair( normal_form_src[i], normal_form_src[j] ); + //Assert( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ); sendLemma( ant, conc, "Loop" ); return true; }else{ @@ -1198,6 +1217,7 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) { void TheoryStrings::addNormalFormPair( Node n1, Node n2 ) { if( !isNormalFormPair( n1, n2 ) ){ + //Assert( !isNormalFormPair( n1, n2 ) ); NodeList* lst; NodeListMap::iterator nf_i = d_nf_pairs.find( n1 ); if( nf_i == d_nf_pairs.end() ){ @@ -1759,12 +1779,30 @@ bool TheoryStrings::unrollStar( Node atom ) { Node sk_s= NodeManager::currentNM()->mkSkolem( "s_unroll_$$", x.getType(), "created for unrolling" ); Node sk_xp= NodeManager::currentNM()->mkSkolem( "x_unroll_$$", x.getType(), "created for unrolling" ); Node unr0 = sk_s.eqNode( d_emptyString ).negate(); + // must also call preprocessing on unr1 Node unr1 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_s, r[0] ); + + std::vector< Node > urc; + urc.push_back( unr1 ); + + StringsPreprocess spp; + spp.simplify( urc ); + for( unsigned i=1; imkNode( kind::STRING_IN_REGEXP, sk_xp, r ); unr3 = Rewriter::rewrite( unr3 ); d_reg_exp_unroll_depth[unr3] = depth + 1; - Node unr = NodeManager::currentNM()->mkNode( kind::AND, unr0, unr1, unr2, unr3 ); + + //|x|>|xp| + Node len_x_gt_len_xp = NodeManager::currentNM()->mkNode( kind::GT, + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ), + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_xp ) ); + + Node unr = NodeManager::currentNM()->mkNode( kind::AND, unr0, urc[0], unr2, unr3, len_x_gt_len_xp ); Node lem = NodeManager::currentNM()->mkNode( kind::OR, xeqe, unr ); sendLemma( atom, lem, "Unroll" ); return true; diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 48bc28b05..d059d8bba 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -21,6 +21,7 @@ #include "theory/theory.h" #include "theory/uf/equality_engine.h" +#include "theory/strings/theory_strings_preprocess.h" #include "context/cdchunk_list.h" diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 472a6d89c..378fa3428 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -21,7 +21,7 @@ namespace CVC4 { namespace theory { namespace strings { -void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret ) { +void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn ) { int k = r.getKind(); switch( k ) { case kind::STRING_TO_REGEXP: @@ -35,19 +35,19 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret std::vector< Node > cc; for(unsigned i=0; imkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" ); - simplifyRegExp( sk, r[i], ret ); + simplifyRegExp( sk, r[i], ret, nn ); cc.push_back( sk ); } Node cc_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, cc ) ); - ret.push_back( cc_eq ); + nn.push_back( cc_eq ); } break; case kind::REGEXP_OR: { std::vector< Node > c_or; for(unsigned i=0; imkNode( kind::OR, c_or ); ret.push_back( eq ); @@ -55,21 +55,9 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret break; case kind::REGEXP_INTER: for(unsigned i=0; imkNode( kind::EQUAL, s, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ); - std::vector< Node > rr; - simplifyRegExp( s, r[0], rr ); - Node nrr = rr.size()==1 ? rr[0] : NodeManager::currentNM()->mkNode( kind::AND, rr ); - ret.push_back( NodeManager::currentNM()->mkNode( kind::OR, eq_empty, nrr) ); - } - break; - //case kind::REGEXP_PLUS: - */ case kind::REGEXP_STAR: { Node eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r ); @@ -78,6 +66,8 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret break; default: //TODO: special sym: sigma, none, all + Trace("strings-preprocess") << "Unsupported term: " << r << " in simplifyRegExp." << std::endl; + Assert( false ); break; } } @@ -99,26 +89,27 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { return (*i).second.isNull() ? t : (*i).second; } - /* - if( t.getKind() == kind::STRING_IN_REGEXP ){ + Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << std::endl; + Node retNode = t; + if( t.getKind() == kind::STRING_IN_REGEXP ) { // t0 in t1 Node t0 = simplify( t[0], new_nodes ); //if(!checkStarPlus( t[1] )) { //rewrite it std::vector< Node > ret; - simplifyRegExp( t0, t[1], ret ); + std::vector< Node > nn; + simplifyRegExp( t0, t[1], ret, nn ); + new_nodes.insert( new_nodes.end(), nn.begin(), nn.end() ); Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret ); d_cache[t] = (t == n) ? Node::null() : n; - return n; + retNode = n; //} else { // TODO // return (t0 == t[0]) ? t : NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, t0, t[1] ); //} - }else - */ - if( t.getKind() == kind::STRING_SUBSTR ){ + } else if( t.getKind() == kind::STRING_SUBSTR ){ Node sk1 = NodeManager::currentNM()->mkSkolem( "st1sym_$$", t.getType(), "created for substr" ); Node sk2 = NodeManager::currentNM()->mkSkolem( "st2sym_$$", t.getType(), "created for substr" ); Node sk3 = NodeManager::currentNM()->mkSkolem( "st3sym_$$", t.getType(), "created for substr" ); @@ -134,7 +125,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { new_nodes.push_back( len_sk2_eq_j ); d_cache[t] = sk2; - return sk2; + retNode = sk2; } else if( t.getNumChildren()>0 ){ std::vector< Node > cc; if (t.getMetaKind() == kind::metakind::PARAMETERIZED) { @@ -149,15 +140,26 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { if(changed) { Node n = NodeManager::currentNM()->mkNode( t.getKind(), cc ); d_cache[t] = n; - return n; + retNode = n; } else { d_cache[t] = Node::null(); - return t; + retNode = t; } }else{ d_cache[t] = Node::null(); - return t; + retNode = t; } + + Trace("strings-preprocess") << "StringsPreprocess::simplify returns: " << retNode << std::endl; + if(!new_nodes.empty()) { + Trace("strings-preprocess") << " ... new nodes:"; + for(unsigned int i=0; i &vec_node) { diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index ce00a75ce..7bc60c1a1 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -32,10 +32,10 @@ class StringsPreprocess { std::hash_map d_cache; private: bool checkStarPlus( Node t ); - void simplifyRegExp( Node s, Node r, std::vector< Node > &ret ); + void simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn ); Node simplify( Node t, std::vector< Node > &new_nodes ); public: -void simplify(std::vector< Node > &vec_node); + void simplify(std::vector< Node > &vec_node); }; }/* CVC4::theory::strings namespace */ diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 31203b767..7b74a95ac 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -21,7 +21,7 @@ using namespace CVC4::kind; using namespace CVC4::theory; using namespace CVC4::theory::strings; -Node TheoryStringsRewriter::rewriteConcatString(TNode node) { +Node TheoryStringsRewriter::rewriteConcatString( TNode node ) { Trace("strings-prerewrite") << "Strings::rewriteConcatString start " << node << std::endl; Node retNode = node; std::vector node_vec; @@ -81,6 +81,70 @@ Node TheoryStringsRewriter::rewriteConcatString(TNode node) { return retNode; } +Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) { + Assert( node.getKind() == kind::REGEXP_CONCAT ); + Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp start " << node << std::endl; + Node retNode = node; + std::vector node_vec; + Node preNode = Node::null(); + for(unsigned int i=0; imkNode( kind::STRING_CONCAT, preNode, tmpNode[0][0] ) ); + node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) ); + preNode = Node::null(); + ++j; + } else { + node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) ); + preNode = Node::null(); + node_vec.push_back( tmpNode[0] ); + ++j; + } + } + for(; jmkNode( kind::STRING_CONCAT, preNode, tmpNode[0] ) ); + } + } else { + if(!preNode.isNull()) { + if(preNode.getKind() == kind::CONST_STRING && preNode.getConst().isEmptyString() ) { + preNode = Node::null(); + } else { + node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) ); + preNode = Node::null(); + } + } + node_vec.push_back( tmpNode ); + } + } + if(!preNode.isNull()) { + node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) ); + } + if(node_vec.size() > 1) { + retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, node_vec); + } else { + retNode = node_vec[0]; + } + Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp end " << retNode << std::endl; + return retNode; +} + void TheoryStringsRewriter::simplifyRegExp( Node s, Node r, std::vector< Node > &ret ) { int k = r.getKind(); switch( k ) { @@ -131,7 +195,7 @@ void TheoryStringsRewriter::simplifyRegExp( Node s, Node r, std::vector< Node > break; } } -bool TheoryStringsRewriter::checkConstRegExp( Node t ) { +bool TheoryStringsRewriter::checkConstRegExp( TNode t ) { if( t.getKind() != kind::STRING_TO_REGEXP ) { for( unsigned i = 0; i(); retNode = NodeManager::currentNM()->mkConst( testConstStringInRegExp( s, 0, node[1] ) ); } else { - if( node[1].getKind() == kind::REGEXP_STAR ) { + //if( node[1].getKind() == kind::REGEXP_STAR ) { if( x == node[0] ) { retNode = node; } else { retNode = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, node[1] ); } + /* } else { std::vector node_vec; simplifyRegExp( x, node[1], node_vec ); @@ -268,6 +332,7 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { retNode = node_vec[0]; } } + */ } //Trace("strings-prerewrite") << "Strings::rewriteMembership end " << retNode << std::endl; return retNode; @@ -347,7 +412,9 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { if(node.getKind() == kind::STRING_CONCAT) { retNode = rewriteConcatString(node); - } else if(node.getKind() == kind::REGEXP_PLUS) { + } else if(node.getKind() == kind::REGEXP_CONCAT) { + retNode = prerewriteConcatRegExp(node); + } else if(node.getKind() == kind::REGEXP_PLUS) { retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, node[0], NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, node[0])); } else if(node.getKind() == kind::REGEXP_OPT) { diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index 9dcfb4ce5..c416abd69 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -30,11 +30,12 @@ namespace strings { class TheoryStringsRewriter { public: - static bool checkConstRegExp( Node t ); - static bool testConstStringInRegExp( CVC4::String &s, unsigned int index_start, Node r ); + static bool checkConstRegExp( TNode t ); + static bool testConstStringInRegExp( CVC4::String &s, unsigned int index_start, TNode r ); static void simplifyRegExp( Node s, Node r, std::vector< Node > &ret ); static Node rewriteConcatString(TNode node); + static Node prerewriteConcatRegExp(TNode node); static Node rewriteMembership(TNode node); static RewriteResponse postRewrite(TNode node); diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index f63cd32fc..8af063284 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -37,12 +37,17 @@ public: 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"); + } return nodeManager->stringType(); } }; @@ -97,12 +102,17 @@ public: 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"); + 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(); } }; diff --git a/test/regress/regress0/strings/regexp002.smt2 b/test/regress/regress0/strings/regexp002.smt2 new file mode 100644 index 000000000..e2a44a9ab --- /dev/null +++ b/test/regress/regress0/strings/regexp002.smt2 @@ -0,0 +1,19 @@ +(set-logic QF_S) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) + +(assert (str.in.re x + (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") )) + )) + +(assert (str.in.re y + (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") )) + )) + +(assert (not (= x y))) +(assert (= (str.len x) (str.len y))) +(assert (= (str.len y) 3)) + +(check-sat)