}\r
\r
// 0-unknown, 1-yes, 2-no\r
-int RegExpOpr::delta( Node r ) {\r
- Trace("strings-regexp-delta") << "RegExp-Delta starts with " << mkString( r ) << std::endl;\r
+int RegExpOpr::delta( Node r, Node &exp ) {\r
+ Trace("regexp-delta") << "RegExp-Delta starts with " << mkString( r ) << std::endl;\r
int ret = 0;\r
if( d_delta_cache.find( r ) != d_delta_cache.end() ) {\r
- ret = d_delta_cache[r];\r
+ ret = d_delta_cache[r].first;\r
+ exp = d_delta_cache[r].second;\r
} else {\r
int k = r.getKind();\r
switch( k ) {\r
break;\r
}\r
case kind::STRING_TO_REGEXP: {\r
- if(r[0].isConst()) {\r
- if(r[0] == d_emptyString) {\r
+ Node tmp = Rewriter::rewrite(r[0]);\r
+ if(tmp.isConst()) {\r
+ if(tmp == d_emptyString) {\r
ret = 1;\r
} else {\r
ret = 2;\r
}\r
} else {\r
ret = 0;\r
+ if(tmp.getKind() == kind::STRING_CONCAT) {\r
+ for(unsigned i=0; i<tmp.getNumChildren(); i++) {\r
+ if(tmp[i].isConst()) {\r
+ ret = 2; break;\r
+ }\r
+ }\r
+\r
+ }\r
+ if(ret == 0) {\r
+ exp = r[0].eqNode(d_emptyString);\r
+ }\r
}\r
break;\r
}\r
case kind::REGEXP_CONCAT: {\r
bool flag = false;\r
+ std::vector< Node > vec_nodes;\r
for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
- int tmp = delta( r[i] );\r
+ Node exp2;\r
+ int tmp = delta( r[i], exp2 );\r
if(tmp == 2) {\r
ret = 2;\r
break;\r
} else if(tmp == 0) {\r
+ vec_nodes.push_back( exp2 );\r
flag = true;\r
}\r
}\r
- if(!flag && ret != 2) {\r
- ret = 1;\r
+ if(ret != 2) {\r
+ if(!flag) {\r
+ ret = 1;\r
+ } else {\r
+ exp = vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode(kind::AND, vec_nodes);\r
+ }\r
}\r
break;\r
}\r
case kind::REGEXP_UNION: {\r
bool flag = false;\r
+ std::vector< Node > vec_nodes;\r
for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
- int tmp = delta( r[i] );\r
+ Node exp2;\r
+ int tmp = delta( r[i], exp2 );\r
if(tmp == 1) {\r
ret = 1;\r
break;\r
} else if(tmp == 0) {\r
+ vec_nodes.push_back( exp2 );\r
flag = true;\r
}\r
}\r
- if(!flag && ret != 1) {\r
- ret = 2;\r
+ if(ret != 1) {\r
+ if(!flag) {\r
+ ret = 2;\r
+ } else {\r
+ exp = vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode(kind::OR, vec_nodes);\r
+ }\r
}\r
break;\r
}\r
case kind::REGEXP_INTER: {\r
- bool flag = true;\r
+ bool flag = false;\r
+ std::vector< Node > vec_nodes;\r
for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
- int tmp = delta( r[i] );\r
+ Node exp2;\r
+ int tmp = delta( r[i], exp2 );\r
if(tmp == 2) {\r
- ret = 2; flag=false;\r
+ ret = 2;\r
break;\r
} else if(tmp == 0) {\r
- flag=false;\r
- break;\r
+ vec_nodes.push_back( exp2 );\r
+ flag = true;\r
}\r
}\r
- if(flag) {\r
- ret = 1;\r
+ if(ret != 2) {\r
+ if(!flag) {\r
+ ret = 1;\r
+ } else {\r
+ exp = vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode(kind::AND, vec_nodes);\r
+ }\r
}\r
break;\r
}\r
break;\r
}\r
case kind::REGEXP_PLUS: {\r
- ret = delta( r[0] );\r
+ ret = delta( r[0], exp );\r
break;\r
}\r
case kind::REGEXP_OPT: {\r
//return Node::null();\r
}\r
}\r
- d_delta_cache[r] = ret;\r
+ if(!exp.isNull()) {\r
+ exp = Rewriter::rewrite(exp);\r
+ }\r
+ std::pair< int, Node > p(ret, exp);\r
+ d_delta_cache[r] = p;\r
+ }\r
+ Trace("regexp-delta") << "RegExp-Delta returns : " << ret << std::endl;\r
+ return ret;\r
+}\r
+\r
+// 0-unknown, 1-yes, 2-no\r
+int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) {\r
+ Assert( c.size() < 2 );\r
+ Trace("regexp-deriv") << "RegExp-deriv starts with R{ " << mkString( r ) << " }, c=" << c << std::endl;\r
+ \r
+ int ret = 1;\r
+ retNode = d_emptyRegexp;\r
+ \r
+ PairNodeStr dv = std::make_pair( r, c );\r
+ if( d_deriv_cache.find( dv ) != d_deriv_cache.end() ) {\r
+ retNode = d_deriv_cache[dv].first;\r
+ ret = d_deriv_cache[dv].second;\r
+ } else if( c.isEmptyString() ) {\r
+ Node expNode;\r
+ ret = delta( r, expNode );\r
+ if(ret == 0) {\r
+ retNode = NodeManager::currentNM()->mkNode(kind::ITE, expNode, r, d_emptyRegexp);\r
+ } else if(ret == 1) {\r
+ retNode = r;\r
+ }\r
+ std::pair< Node, int > p(retNode, ret);\r
+ d_deriv_cache[dv] = p;\r
+ } else {\r
+ switch( r.getKind() ) {\r
+ case kind::REGEXP_EMPTY: {\r
+ ret = 2;\r
+ break;\r
+ }\r
+ case kind::REGEXP_SIGMA: {\r
+ retNode = d_emptySingleton;\r
+ break;\r
+ }\r
+ case kind::STRING_TO_REGEXP: {\r
+ Node tmp = Rewriter::rewrite(r[0]);\r
+ if(tmp.isConst()) {\r
+ if(tmp == d_emptyString) {\r
+ ret = 2;\r
+ } else {\r
+ if(tmp.getConst< CVC4::String >().getFirstChar() == c.getFirstChar()) {\r
+ retNode = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, \r
+ tmp.getConst< CVC4::String >().size() == 1 ? d_emptyString : NodeManager::currentNM()->mkConst( tmp.getConst< CVC4::String >().substr(1) ) );\r
+ } else {\r
+ ret = 2;\r
+ }\r
+ }\r
+ } else {\r
+ ret = 0;\r
+ Node rest;\r
+ if(tmp.getKind() == kind::STRING_CONCAT) {\r
+ Node t2 = tmp[0];\r
+ if(t2.isConst()) {\r
+ if(t2.getConst< CVC4::String >().getFirstChar() == c.getFirstChar()) {\r
+ Node n = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, \r
+ tmp.getConst< CVC4::String >().size() == 1 ? d_emptyString : NodeManager::currentNM()->mkConst( tmp.getConst< CVC4::String >().substr(1) ) );\r
+ std::vector< Node > vec_nodes;\r
+ vec_nodes.push_back(n);\r
+ for(unsigned i=1; i<tmp.getNumChildren(); i++) {\r
+ vec_nodes.push_back(tmp[i]);\r
+ }\r
+ retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_nodes);\r
+ ret = 1;\r
+ } else {\r
+ ret = 2;\r
+ }\r
+ } else {\r
+ tmp = tmp[0];\r
+ std::vector< Node > vec_nodes;\r
+ for(unsigned i=1; i<tmp.getNumChildren(); i++) {\r
+ vec_nodes.push_back(tmp[i]);\r
+ }\r
+ rest = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_nodes);\r
+ }\r
+ }\r
+ if(ret == 0) {\r
+ Node sk = NodeManager::currentNM()->mkSkolem( "rsp_$$", NodeManager::currentNM()->stringType(), "Split RegExp" );\r
+ retNode = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, sk);\r
+ if(!rest.isNull()) {\r
+ retNode = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, retNode, rest));\r
+ }\r
+ Node exp = tmp.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT,\r
+ NodeManager::currentNM()->mkConst(c), sk));\r
+ retNode = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE, exp, retNode, d_emptyRegexp));\r
+ }\r
+ }\r
+ break;\r
+ }\r
+ case kind::REGEXP_CONCAT: {\r
+ std::vector< Node > vec_nodes;\r
+ std::vector< Node > delta_nodes;\r
+ Node dnode = d_true;\r
+ for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
+ Node dc;\r
+ Node exp2;\r
+ int rt = derivativeS(r[i], c, dc);\r
+ if(rt != 2) {\r
+ if(rt == 0) {\r
+ ret = 0;\r
+ }\r
+ std::vector< Node > vec_nodes2;\r
+ if(dc != d_emptySingleton) {\r
+ vec_nodes2.push_back( dc );\r
+ }\r
+ for(unsigned j=i+1; j<r.getNumChildren(); ++j) {\r
+ if(r[j] != d_emptySingleton) {\r
+ vec_nodes2.push_back( r[j] );\r
+ }\r
+ }\r
+ Node tmp = vec_nodes2.size()==0 ? d_emptySingleton : \r
+ vec_nodes2.size()==1 ? vec_nodes2[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, vec_nodes2 );\r
+ if(dnode != d_true) {\r
+ tmp = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE, dnode, tmp, d_emptyRegexp));\r
+ ret = 0;\r
+ }\r
+ if(std::find(vec_nodes.begin(), vec_nodes.end(), tmp) == vec_nodes.end()) {\r
+ vec_nodes.push_back( tmp );\r
+ }\r
+ }\r
+ Node exp3;\r
+ int rt2 = delta( r[i], exp3 );\r
+ if( rt2 == 0 ) {\r
+ dnode = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, dnode, exp3));\r
+ } else if( rt2 == 2 ) {\r
+ break;\r
+ }\r
+ }\r
+ retNode = vec_nodes.size() == 0 ? d_emptyRegexp :\r
+ ( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes ) );\r
+ if(retNode == d_emptyRegexp) {\r
+ ret = 2;\r
+ }\r
+ break;\r
+ }\r
+ case kind::REGEXP_UNION: {\r
+ std::vector< Node > vec_nodes;\r
+ for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
+ Node dc;\r
+ int rt = derivativeS(r[i], c, dc);\r
+ if(rt == 0) {\r
+ ret = 0;\r
+ }\r
+ if(rt != 2) {\r
+ if(std::find(vec_nodes.begin(), vec_nodes.end(), dc) == vec_nodes.end()) {\r
+ vec_nodes.push_back( dc );\r
+ }\r
+ }\r
+ Trace("regexp-deriv") << "RegExp-deriv OR R[" << i << "]{ " << mkString(r[i]) << " returns " << mkString(dc) << std::endl;\r
+ }\r
+ retNode = vec_nodes.size() == 0 ? d_emptyRegexp :\r
+ ( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes ) );\r
+ if(retNode == d_emptyRegexp) {\r
+ ret = 2;\r
+ }\r
+ break;\r
+ }\r
+ case kind::REGEXP_INTER: {\r
+ bool flag = true;\r
+ bool flag_sg = false;\r
+ std::vector< Node > vec_nodes;\r
+ for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
+ Node dc;\r
+ int rt = derivativeS(r[i], c, dc);\r
+ if(rt == 0) {\r
+ ret = 0;\r
+ } else if(rt == 2) {\r
+ flag = false;\r
+ break;\r
+ }\r
+ if(dc == d_sigma_star) {\r
+ flag_sg = true;\r
+ } else {\r
+ if(std::find(vec_nodes.begin(), vec_nodes.end(), dc) == vec_nodes.end()) {\r
+ vec_nodes.push_back( dc );\r
+ }\r
+ }\r
+ }\r
+ if(flag) {\r
+ if(vec_nodes.size() == 0 && flag_sg) {\r
+ retNode = d_sigma_star;\r
+ } else {\r
+ retNode = vec_nodes.size() == 0 ? d_emptyRegexp :\r
+ ( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_INTER, vec_nodes ) );\r
+ if(retNode == d_emptyRegexp) {\r
+ ret = 2;\r
+ }\r
+ }\r
+ } else {\r
+ retNode = d_emptyRegexp;\r
+ ret = 2;\r
+ }\r
+ break;\r
+ }\r
+ case kind::REGEXP_STAR: {\r
+ Node dc;\r
+ ret = derivativeS(r[0], c, dc);\r
+ retNode = dc==d_emptyRegexp ? dc : (dc==d_emptySingleton ? r : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, dc, r ));\r
+ break;\r
+ }\r
+ default: {\r
+ Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in derivative of RegExp." << std::endl;\r
+ Assert( false, "Unsupported Term" );\r
+ }\r
+ }\r
+ if(retNode != d_emptyRegexp) {\r
+ retNode = Rewriter::rewrite( retNode );\r
+ }\r
+ std::pair< Node, int > p(retNode, ret);\r
+ d_deriv_cache[dv] = p;\r
}\r
- Trace("strings-regexp-delta") << "RegExp-Delta returns : " << ret << std::endl;\r
+\r
+ Trace("regexp-deriv") << "RegExp-deriv returns : " << mkString( retNode ) << std::endl;\r
return ret;\r
}\r
\r
Assert( c.size() < 2 );\r
Trace("regexp-deriv") << "RegExp-deriv starts with R{ " << mkString( r ) << " }, c=" << c << std::endl;\r
Node retNode = d_emptyRegexp;\r
- PairDvStr dv = std::make_pair( r, c );\r
+ PairNodeStr dv = std::make_pair( r, c );\r
if( d_dv_cache.find( dv ) != d_dv_cache.end() ) {\r
retNode = d_dv_cache[dv];\r
} else if( c.isEmptyString() ){\r
- int tmp = delta( r );\r
+ Node exp;\r
+ int tmp = delta( r, exp );\r
if(tmp == 0) {\r
// TODO variable\r
retNode = d_emptyRegexp;\r
vec_nodes.push_back( tmp );\r
}\r
}\r
-\r
- if( delta( r[i] ) != 1 ) {\r
+ Node exp;\r
+ if( delta( r[i], exp ) != 1 ) {\r
break;\r
}\r
}\r
for(unsigned i=0; i<r.getNumChildren(); i++) {\r
firstChars(r[i], cset, vset);\r
Node n = r[i];\r
- int r = delta( n );\r
+ Node exp;\r
+ int r = delta( n, exp );\r
if(r != 1) {\r
break;\r
}\r
}\r
}\r
break;\r
- /*\r
- case kind::REGEXP_PLUS:\r
- {\r
- ret = delta( r[0] );\r
- }\r
- break;\r
- case kind::REGEXP_OPT:\r
- {\r
- ret = 1;\r
- }\r
- break;\r
- case kind::REGEXP_RANGE:\r
- {\r
- ret = 2;\r
- }\r
- break;*/\r
default: {\r
Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in delta of RegExp." << std::endl;\r
//AlwaysAssert( false );\r
}\r
}\r
\r
-Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< unsigned, std::set< PairNodes > > cache ) {\r
+Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< unsigned, std::set< PairNodes > > cache, bool &spflag ) {\r
+ if(spflag) {\r
+ //TODO: var\r
+ return Node::null();\r
+ }\r
std::pair < Node, Node > p(r1, r2);\r
std::map < std::pair< Node, Node >, Node >::const_iterator itr = d_inter_cache.find(p);\r
Node rNode;\r
if(itr != d_inter_cache.end()) {\r
- //Trace("regexp-intersect") << "INTERSECT Case 0: Cached " << std::endl;\r
rNode = itr->second;\r
} else {\r
- if(r1 == d_emptyRegexp || r2 == d_emptyRegexp) {\r
- Trace("regexp-intersect") << "INTERSECT Case 1: one empty RE" << std::endl;\r
+ if(r1 == r2) {\r
+ rNode = r1;\r
+ } else if(r1 == d_emptyRegexp || r2 == d_emptyRegexp) {\r
+ Trace("regexp-intersect") << "INTERSECT Case 1: one empty RE" << std::endl;\r
rNode = d_emptyRegexp;\r
} else if(r1 == d_emptySingleton || r2 == d_emptySingleton) {\r
Trace("regexp-intersect") << "INTERSECT Case 2: one empty Singleton" << std::endl;\r
- int r = delta(r1 == d_emptySingleton ? r2 : r1);\r
+ Node exp;\r
+ int r = delta((r1 == d_emptySingleton ? r2 : r1), exp);\r
if(r == 0) {\r
//TODO: variable\r
- AlwaysAssert( false, "Unsupported Yet, 892 REO" );\r
+ spflag = true;\r
+ //Assert( false, "Unsupported Yet, 892 REO" );\r
} else if(r == 1) {\r
rNode = d_emptySingleton;\r
} else {\r
std::map< unsigned, std::set< PairNodes > > cache2(cache);\r
PairNodes p(r1l, r2l);\r
cache2[ *itr ].insert( p );\r
- Node rt = intersectInternal(r1l, r2l, cache2);\r
+ Node rt = intersectInternal(r1l, r2l, cache2, spflag);\r
+ if(spflag) {\r
+ //TODO:\r
+ return Node::null();\r
+ }\r
rt = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, \r
NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c)), rt) );\r
vec_nodes.push_back(rt);\r
}\r
}\r
rNode = vec_nodes.size()==0 ? d_emptyRegexp : vec_nodes.size()==1 ? vec_nodes[0] :\r
- NodeManager::currentNM()->mkNode(kind::OR, vec_nodes);\r
+ NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes);\r
rNode = Rewriter::rewrite( rNode );\r
} else {\r
Trace("regexp-intersect") << "INTERSECT Case 3.2: diff cset" << std::endl;\r
}\r
} else {\r
//TODO: non-empty var set\r
- AlwaysAssert( false, "Unsupported Yet, 927 REO" );\r
+ spflag = true;\r
+ //Assert( false, "Unsupported Yet, 927 REO" );\r
}\r
}\r
d_inter_cache[p] = rNode;\r
Trace("regexp-intersect") << "INTERSECT( " << mkString(r1) << ", " << mkString(r2) << " ) = " << mkString(rNode) << std::endl;\r
return rNode;\r
}\r
-Node RegExpOpr::intersect(Node r1, Node r2) {\r
+Node RegExpOpr::intersect(Node r1, Node r2, bool &spflag) {\r
std::map< unsigned, std::set< PairNodes > > cache;\r
- return intersectInternal(r1, r2, cache);\r
+ return intersectInternal(r1, r2, cache, spflag);\r
}\r
//printing\r
std::string RegExpOpr::niceChar( Node r ) {\r
d_regexp_ccached(c),
d_str_re_map(c),
d_inter_cache(c),
+ d_inter_index(c),
d_regexp_ant(c),
d_input_vars(u),
d_input_var_lsum(u),
NodeManager::currentNM()->mkNode( kind::REGEXP_STAR,
NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, rep_c ) ) );
conc = str_in_re;
+ } else if(t_yz.isConst()) {
+ CVC4::String s = t_yz.getConst< CVC4::String >();
+ unsigned size = s.size();
+ std::vector< Node > vconc;
+ for(unsigned len=1; len<=size; len++) {
+ Node y = NodeManager::currentNM()->mkConst(s.substr(0, len));
+ Node z = NodeManager::currentNM()->mkConst(s.substr(len, size - len));
+ Node restr = s_zy;
+ Node cc;
+ if(r != d_emptyString) {
+ std::vector< Node > v2(vec_r);
+ v2.insert(v2.begin(), y);
+ v2.insert(v2.begin(), z);
+ restr = mkConcat( z, y );
+ cc = Rewriter::rewrite(s_zy.eqNode( mkConcat( v2 ) ));
+ } else {
+ cc = Rewriter::rewrite(s_zy.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, z, y) ));
+ }
+ if(cc == d_false) {
+ continue;
+ }
+ Node conc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index],
+ NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT,
+ NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, y),
+ NodeManager::currentNM()->mkNode(kind::REGEXP_STAR,
+ NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, restr))));
+ cc = cc==d_true ? conc2 : NodeManager::currentNM()->mkNode( kind::AND, cc, conc2 );
+ d_regexp_ant[conc2] = ant;
+ vconc.push_back(cc);
+ }
+ conc = vconc.size()==0 ? Node::null() : vconc.size()==1 ? vconc[0] : NodeManager::currentNM()->mkNode(kind::OR, vconc);
} else {
Trace("strings-loop") << "Strings::Loop: Normal Breaking." << std::endl;
//right
} // normal case
//set its antecedant to ant, to say when it is relevant
- d_regexp_ant[str_in_re] = ant;
- //unroll the str in re constraint once
- // unrollStar( str_in_re );
+ if(!str_in_re.isNull()) {
+ d_regexp_ant[str_in_re] = ant;
+ }
sendLemma( ant, conc, "LOOP-BREAK" );
++(d_statistics.d_loop_lemmas);
if(options::stringEIT()) {
for(NodeListMap::const_iterator itr_xr = d_str_re_map.begin();
itr_xr != d_str_re_map.end(); ++itr_xr ) {
+ bool spflag = false;
+ Node x = (*itr_xr).first;
NodeList* lst = (*itr_xr).second;
- if(lst->size() > 1) {
- Node r = (*lst)[0];
- NodeList::const_iterator itr_lst = lst->begin();
- ++itr_lst;
- for(;itr_lst != lst->end(); ++itr_lst) {
- Node r2 = *itr_lst;
- r = d_regexp_opr.intersect(r, r2);
- if(r == d_emptyRegexp) {
- std::vector< Node > vec_nodes;
- Node x = (*itr_xr).first;
+ if(d_inter_index.find(x) == d_inter_index.end()) {
+ d_inter_index[x] = 0;
+ }
+ int cur_inter_idx = d_inter_index[x];
+ if(cur_inter_idx != (int)lst->size()) {
+ if(lst->size() == 1) {
+ d_inter_cache[x] = (*lst)[0];
+ d_inter_index[x] = 1;
+ } else if(lst->size() > 1) {
+ Node r;
+ if(d_inter_cache.find(x) != d_inter_cache.end()) {
+ r = d_inter_cache[x];
+ }
+ if(r.isNull()) {
+ r = (*lst)[0];
+ cur_inter_idx = 1;
+ }
+ NodeList::const_iterator itr_lst = lst->begin();
+ for(int i=0; i<cur_inter_idx; i++) {
++itr_lst;
- for(NodeList::const_iterator itr2 = lst->begin();
- itr2 != itr_lst; ++itr2) {
- Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, *itr2);
- vec_nodes.push_back( n );
+ }
+ for(;itr_lst != lst->end(); ++itr_lst) {
+ Node r2 = *itr_lst;
+ r = d_regexp_opr.intersect(r, r2, spflag);
+ if(spflag) {
+ break;
+ } else if(r == d_emptyRegexp) {
+ std::vector< Node > vec_nodes;
+ ++itr_lst;
+ for(NodeList::const_iterator itr2 = lst->begin();
+ itr2 != itr_lst; ++itr2) {
+ Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, *itr2);
+ vec_nodes.push_back( n );
+ }
+ Node antec = vec_nodes.size() == 1? vec_nodes[0] : NodeManager::currentNM()->mkNode(kind::AND, vec_nodes);
+ Node conc;
+ sendLemma(antec, conc, "INTERSEC CONFLICT");
+ addedLemma = true;
+ break;
+ }
+ if(d_conflict) {
+ break;
}
- Node antec = vec_nodes.size() == 1? vec_nodes[0] : NodeManager::currentNM()->mkNode(kind::AND, vec_nodes);
- Node conc;
- sendLemma(antec, conc, "INTERSEC CONFLICT");
- addedLemma = true;
- break;
}
- if(d_conflict) {
- break;
+ //updates
+ if(!d_conflict && !spflag) {
+ d_inter_cache[x] = r;
+ d_inter_index[x] = (int)lst->size();
}
}
}
}
}*/
if(areEqual(x, d_emptyString)) {
- int rdel = d_regexp_opr.delta(r);
- if(rdel == 1) {
- d_regexp_ccached.insert(atom);
- } else if(rdel == 2) {
- Node antec = mkRegExpAntec(atom, x.eqNode(d_emptyString));
- Node conc = Node::null();
- sendLemma(antec, conc, "RegExp Delta CONFLICT");
- addedLemma = true;
- d_regexp_ccached.insert(atom);
- return false;
+ Node exp;
+ switch(d_regexp_opr.delta(r, exp)) {
+ case 0: {
+ Node antec = mkRegExpAntec(atom, x.eqNode(d_emptyString));
+ sendLemma(antec, exp, "RegExp Delta");
+ addedLemma = true;
+ d_regexp_ccached.insert(atom);
+ return false;
+ }
+ case 1: {
+ d_regexp_ccached.insert(atom);
+ break;
+ }
+ case 2: {
+ Node antec = mkRegExpAntec(atom, x.eqNode(d_emptyString));
+ Node conc = Node::null();
+ sendLemma(antec, conc, "RegExp Delta CONFLICT");
+ addedLemma = true;
+ d_regexp_ccached.insert(atom);
+ return false;
+ }
+ default:
+ //Impossible
+ break;
}
} else {
Node xr = getRepresentative( x );
bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
// TODO cstr in vre
Assert(x != d_emptyString);
- Trace("strings-regexp-split") << "TheoryStrings::splitRegExp: x=" << x << ", r= " << r << std::endl;
+ Trace("regexp-split") << "TheoryStrings::splitRegExp: x=" << x << ", r= " << r << std::endl;
//if(x.isConst()) {
// Node n = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, r );
// Node r = Rewriter::rewrite( n );
bool flag = true;
for(unsigned i=0; i<s.size(); ++i) {
CVC4::String c = s.substr(i, 1);
- dc = d_regexp_opr.derivativeSingle(dc, c);
- if(dc == d_emptyRegexp) {
+ Node dc2;
+ int rt = d_regexp_opr.derivativeS(dc, c, dc2);
+ if(rt == 0) {
+ //TODO
+ } else if(rt == 2) {
// CONFLICT
flag = false;
break;
}
}
lst->push_back( r );
- //TODO: make it smarter
- /*
- unsigned size = lst->size();
- if(size == 1) {
- d_inter_cache[x] = r;
- } else {
- Node r1 = (*lst)[size - 2];
- Node rr = d_regexp_opr.intersect(r1, r);
- d_inter_cache[x] = rr;
- }*/
}
}
}
projects / cvc5.git / commitdiff