diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-03-27 17:21:01 -0500 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-03-27 17:21:01 -0500 |
| commit | 005f46c18a40dd83dc8e042bfe2725c4b0a566d3 (patch) | |
| tree | 2887c446241258700681dd7280b31c6a53e18834 /src/theory/strings/regexp_operation.cpp | |
| parent | 70a7ae4dc962e43c38cec19a5549673a46045d71 (diff) | |
| parent | f814750622a50835d4be99b1ced54af5e25d8ed4 (diff) | |
Merge branch 'master' of github.com:tiliang/CVC4
Conflicts:
src/theory/strings/regexp_operation.cpp
src/theory/strings/regexp_operation.h
Diffstat (limited to 'src/theory/strings/regexp_operation.cpp')
| -rw-r--r-- | src/theory/strings/regexp_operation.cpp | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 8cb8c124a..528436033 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -695,10 +695,8 @@ void RegExpOpr::firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset ) for(unsigned i=0; i<r.getNumChildren(); i++) {
firstChars(r[i], cset, vset);
Node n = r[i];
- Node exp;
int r = delta( n, exp );
- if(r != 1) {
break;
}
@@ -1210,7 +1208,6 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< unsigned, std::se //TODO: var
return Node::null();
}
- std::pair < Node, Node > p(r1, r2);
std::map < std::pair< Node, Node >, Node >::const_iterator itr = d_inter_cache.find(p);
Node rNode;
@@ -1280,7 +1277,6 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< unsigned, std::se //TODO: non-empty var set
spflag = true;
//Assert( false, "Unsupported Yet, 927 REO" );
- }
}
d_inter_cache[p] = rNode;
@@ -1291,7 +1287,6 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< unsigned, std::se Node RegExpOpr::intersect(Node r1, Node r2, bool &spflag) {
std::map< unsigned, std::set< PairNodes > > cache;
return intersectInternal(r1, r2, cache, spflag);
- }
Node RegExpOpr::complement(Node r, int &ret) {
|