}\r
\r
bool RegExpOpr::checkConstRegExp( Node r ) {\r
+ Trace("strings-regexp-cstre") << "RegExp-CheckConstRegExp starts with " << mkString( r ) << std::endl;\r
bool ret = true;\r
if( d_cstre_cache.find( r ) != d_cstre_cache.end() ) {\r
ret = d_cstre_cache[r];\r
//null - no solution\r
Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {\r
Assert( c.size() < 2 );\r
- Trace("strings-regexp-derivative") << "RegExp-derivative starts with " << mkString( r ) << ", c=" << c << std::endl;\r
+ Trace("strings-regexp-derivative") << "RegExp-derivative starts with R{ " << mkString( r ) << " }, c=" << c << std::endl;\r
Node retNode = Node::null();\r
PairDvStr dv = std::make_pair( r, c );\r
if( d_dv_cache.find( dv ) != d_dv_cache.end() ) {\r
vec_nodes.push_back( dc );\r
}\r
}\r
-\r
+ Trace("strings-regexp-derivative") << "RegExp-derivative OR R[" << i << "]{ " << mkString(r[i]) << " returns " << (dc.isNull() ? "NULL" : mkString(dc) ) << std::endl;\r
}\r
retNode = vec_nodes.size() == 0 ? Node::null() :\r
( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes ) );\r
break;\r
case kind::REGEXP_OPT:\r
{\r
- return derivativeSingle(r[0], c);\r
+ retNode = derivativeSingle(r[0], c);\r
}\r
break;\r
case kind::REGEXP_RANGE:\r
{\r
char ch = c.getFirstChar();\r
if (ch >= r[0].getConst< CVC4::String >().getFirstChar() && ch <= r[1].getConst< CVC4::String >().getFirstChar() ) {\r
- return d_emptyString;\r
+ retNode = d_emptyString;\r
} else {\r
- return Node::null();\r
+ retNode = Node::null();\r
}\r
}\r
break;\r
//AlwaysAssert( false );\r
//return Node::null();\r
}\r
+ if(!retNode.isNull()) {\r
+ retNode = Rewriter::rewrite( retNode );\r
+ }\r
d_dv_cache[dv] = retNode;\r
}\r
Trace("strings-regexp-derivative") << "RegExp-derivative returns : " << ( retNode.isNull() ? "NULL" : mkString( retNode ) ) << std::endl;\r
//d_pending_req_phase[ x_empty ] = true;
if( !areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString ) ){
//try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
- sendSplit( normal_forms[loop_n_index][loop_index], d_emptyString, "Loop Empty" );
+ sendSplit( normal_forms[loop_n_index][loop_index], d_emptyString, "Loop Empty x" );
return true;
- } else if( !areDisequal( t_yz, d_emptyString ) ) {
+ } else if( !areDisequal( t_yz, d_emptyString ) && t_yz.getKind()!=kind::CONST_STRING ) {
//TODO...........
//try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
- sendSplit( t_yz, d_emptyString, "Loop Empty" );
+ sendSplit( t_yz, d_emptyString, "Loop Empty yz" );
return true;
} else {
//need to break
antec.push_back( normal_forms[loop_n_index][loop_index].eqNode( d_emptyString ).negate() );
- antec.push_back( t_yz.eqNode( d_emptyString ).negate() );
+ if( t_yz.getKind()!=kind::CONST_STRING ){
+ antec.push_back( t_yz.eqNode( d_emptyString ).negate() );
+ }
Node ant = mkExplain( antec, antec_new_lits );
Node str_in_re;
if( s_zy == t_yz &&
Assert( atom.getKind()==kind::STRING_IN_REGEXP );
Node x = atom[0];
Node r = atom[1];
- //TODO
Assert( r.getKind()==kind::REGEXP_STAR );
if( !areEqual( x, d_emptyString ) ){
//if(splitRegExp( x, r, atom )) {
}
CVC4::String TheoryStrings::getHeadConst( Node x ) {
- if( x.isConst() && x != d_emptyString ) {
+ if( x.isConst() ) {
return x.getConst< String >();
} else if( x.getKind() == kind::STRING_CONCAT ) {
- if( x[0].isConst() && x[0] != d_emptyString ) {
- return x.getConst< String >();
+ if( x[0].isConst() ) {
+ return x[0].getConst< String >();
} else {
return d_emptyString.getConst< String >();
}
}
bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
- x = Rewriter::rewrite( x );
- if(x == d_emptyString) {
- if(d_regexp_opr.delta( r ) == 1) {
- }
- return false;
- } else {
- CVC4::String s = getHeadConst( x );
- if( !s.isEmptyString() && d_regexp_opr.checkConstRegExp( r ) ) {
- Node conc = Node::null();
- Node dc = r;
- 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.isNull()) {
- // CONFLICT
- flag = false;
- break;
- }
+ // TODO cstr in vre
+ Assert(x != d_emptyString);
+ Trace("strings-regexp-split") << "TheoryStrings::splitRegExp: x=" << x << ", r= " << r << std::endl;
+ CVC4::String s = getHeadConst( x );
+ if( !s.isEmptyString() && d_regexp_opr.checkConstRegExp( r ) ) {
+ Node conc = Node::null();
+ Node dc = r;
+ 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.isNull()) {
+ // CONFLICT
+ flag = false;
+ break;
}
- // send lemma
- if(flag) {
- Node left = Node::null();
- if(x.isConst()) {
- left = d_emptyString;
- if(d_regexp_opr.delta(dc)) {
- //TODO yes
- } else {
- // TODO conflict
- }
+ }
+ // send lemma
+ if(flag) {
+ if(x.isConst()) {
+ /*
+ left = d_emptyString;
+ if(d_regexp_opr.delta(dc) == 1) {
+ //TODO yes possible?
+ } else if(d_regexp_opr.delta(dc) == 0) {
+ //TODO possible?
} else {
- //TODO find x rest
- conc = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, dc );
+ // TODO conflict possible?
+ }*/
+ Assert(false, "Impossible: TheoryStrings::splitRegExp: const string in const regular expression.");
+ return false;
+ } else {
+ Assert( x.getKind() == kind::STRING_CONCAT );
+ std::vector< Node > vec_nodes;
+ for(unsigned int i=1; i<x.getNumChildren(); ++i ) {
+ vec_nodes.push_back( x[i] );
}
+ Node left = vec_nodes.size() == 1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, vec_nodes );
+ left = Rewriter::rewrite( left );
+ conc = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, left, dc );
+
+ std::vector< Node > sdc;
+ sdc.push_back( conc );
+
+ StringsPreprocess spp;
+ spp.simplify( sdc );
+ for( unsigned i=1; i<sdc.size(); i++ ){
+ //add the others as lemmas
+ sendLemma( d_true, sdc[i], "RegExp Definition");
+ }
+
+ conc = sdc[0];
}
- sendLemma(ant, conc, "RegExp Const Split");
- } else {
- return false;
}
+ sendLemma(ant, conc, "RegExp Const Split");
+ return true;
+ } else {
+ return false;
}
- return false;
}
Node TheoryStrings::getNextDecisionRequest() {
projects / cvc5.git / commitdiff