summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/strings/theory_strings.cpp138
-rw-r--r--src/theory/strings/theory_strings.h1
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp58
-rw-r--r--src/theory/strings/theory_strings_preprocess.h4
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp79
-rw-r--r--src/theory/strings/theory_strings_rewriter.h5
-rw-r--r--src/theory/strings/theory_strings_type_rules.h12
-rw-r--r--test/regress/regress0/strings/regexp002.smt219
8 files changed, 227 insertions, 89 deletions
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; i<urc.size(); i++ ){
+ //add the others as lemmas
+ sendLemma( d_true, urc[i], "RegExp Definition");
+ }
+
Node unr2 = x.eqNode( mkConcat( sk_s, sk_xp ) );
Node unr3 = NodeManager::currentNM()->mkNode( 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; i<r.getNumChildren(); ++i) {
Node sk = NodeManager::currentNM()->mkSkolem( "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; i<r.getNumChildren(); ++i) {
- simplifyRegExp( s, r[i], c_or );
+ simplifyRegExp( s, r[i], c_or, nn );
}
Node eq = NodeManager::currentNM()->mkNode( 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; i<r.getNumChildren(); ++i) {
- simplifyRegExp( s, r[i], ret );
+ simplifyRegExp( s, r[i], ret, nn );
}
break;
- /*
- case kind::REGEXP_OPT:
- {
- Node eq_empty = NodeManager::currentNM()->mkNode( 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<new_nodes.size(); ++i) {
+ Trace("strings-preprocess") << " " << new_nodes[i];
+ }
+ Trace("strings-preprocess") << std::endl;
+ }
+
+ return retNode;
}
void StringsPreprocess::simplify(std::vector< Node > &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<TNode, Node, TNodeHashFunction> 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> 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> node_vec;
+ Node preNode = Node::null();
+ for(unsigned int i=0; i<node.getNumChildren(); ++i) {
+ Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp preNode: " << preNode << std::endl;
+ Node tmpNode = node[i];
+ if(node[i].getKind() == kind::REGEXP_CONCAT) {
+ tmpNode = prerewriteConcatRegExp(node[i]);
+ if(tmpNode.getKind() == kind::REGEXP_CONCAT) {
+ unsigned int j=0;
+ if(!preNode.isNull()) {
+ if(tmpNode[0].getKind() == kind::STRING_TO_REGEXP) {
+ preNode = rewriteConcatString(
+ NodeManager::currentNM()->mkNode( 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(; j<tmpNode.getNumChildren() - 1; ++j) {
+ node_vec.push_back( tmpNode[j] );
+ }
+ tmpNode = tmpNode[j];
+ }
+ }
+ if( tmpNode.getKind() == kind::STRING_TO_REGEXP ) {
+ if(preNode.isNull()) {
+ preNode = tmpNode[0];
+ } else {
+ preNode = rewriteConcatString(
+ NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0] ) );
+ }
+ } else {
+ if(!preNode.isNull()) {
+ if(preNode.getKind() == kind::CONST_STRING && preNode.getConst<String>().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<t.getNumChildren(); ++i ) {
if( !checkConstRegExp(t[i]) ) return false;
@@ -146,7 +210,7 @@ bool TheoryStringsRewriter::checkConstRegExp( Node t ) {
}
}
-bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned int index_start, Node r ) {
+bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned int index_start, TNode r ) {
Assert( index_start <= s.size() );
int k = r.getKind();
switch( k ) {
@@ -247,17 +311,17 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
}
if( x.getKind() == kind::CONST_STRING && checkConstRegExp(node[1]) ) {
- //TODO x \in R[y]
//test whether x in node[1]
CVC4::String s = x.getConst<String>();
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> 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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback