diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-11-06 17:18:31 -0600 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-11-06 17:20:04 -0600 |
commit | 78f1deb6dcb2492275642ff3a52b5611b95fecbb (patch) | |
tree | 1020f03dfbef0e9e5c8759b888dd75885aa2ac37 | |
parent | 657a5e91cb0310f5791c9e9e887da71f395e1f07 (diff) |
bug fix
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 14 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 105 |
2 files changed, 71 insertions, 48 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 0a7701862..fa686dd9f 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -31,6 +31,7 @@ RegExpOpr::RegExpOpr() { }
bool RegExpOpr::checkConstRegExp( Node r ) {
+ Trace("strings-regexp-cstre") << "RegExp-CheckConstRegExp starts with " << mkString( r ) << std::endl;
bool ret = true;
if( d_cstre_cache.find( r ) != d_cstre_cache.end() ) {
ret = d_cstre_cache[r];
@@ -159,7 +160,7 @@ int RegExpOpr::delta( Node r ) { //null - no solution
Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {
Assert( c.size() < 2 );
- Trace("strings-regexp-derivative") << "RegExp-derivative starts with " << mkString( r ) << ", c=" << c << std::endl;
+ Trace("strings-regexp-derivative") << "RegExp-derivative starts with R{ " << mkString( r ) << " }, c=" << c << std::endl;
Node retNode = Node::null();
PairDvStr dv = std::make_pair( r, c );
if( d_dv_cache.find( dv ) != d_dv_cache.end() ) {
@@ -236,7 +237,7 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { vec_nodes.push_back( dc );
}
}
-
+ Trace("strings-regexp-derivative") << "RegExp-derivative OR R[" << i << "]{ " << mkString(r[i]) << " returns " << (dc.isNull() ? "NULL" : mkString(dc) ) << std::endl;
}
retNode = vec_nodes.size() == 0 ? Node::null() :
( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes ) );
@@ -296,16 +297,16 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { break;
case kind::REGEXP_OPT:
{
- return derivativeSingle(r[0], c);
+ retNode = derivativeSingle(r[0], c);
}
break;
case kind::REGEXP_RANGE:
{
char ch = c.getFirstChar();
if (ch >= r[0].getConst< CVC4::String >().getFirstChar() && ch <= r[1].getConst< CVC4::String >().getFirstChar() ) {
- return d_emptyString;
+ retNode = d_emptyString;
} else {
- return Node::null();
+ retNode = Node::null();
}
}
break;
@@ -315,6 +316,9 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { //AlwaysAssert( false );
//return Node::null();
}
+ if(!retNode.isNull()) {
+ retNode = Rewriter::rewrite( retNode );
+ }
d_dv_cache[dv] = retNode;
}
Trace("strings-regexp-derivative") << "RegExp-derivative returns : " << ( retNode.isNull() ? "NULL" : mkString( retNode ) ) << std::endl;
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index e5ce2d6d3..fc4b3ba9c 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1017,17 +1017,19 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //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 && @@ -1977,7 +1979,6 @@ bool TheoryStrings::checkMemberships() { 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 )) { @@ -2039,11 +2040,11 @@ bool TheoryStrings::checkMemberships() { } 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 >(); } @@ -2053,47 +2054,65 @@ CVC4::String TheoryStrings::getHeadConst( Node x ) { } 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() { |