diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-05-05 18:01:14 -0500 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-05-05 18:01:14 -0500 |
| commit | 22acfb03456d5816c550d822ef7e27d147475eee (patch) | |
| tree | 213305b8e490f168a5216afe20bfa066d2acac57 /src/theory/strings/regexp_operation.cpp | |
| parent | 632ed29e9d82ddef49d0c3382dce1439aa67698a (diff) | |
add constant regular expression check for intersection.
Diffstat (limited to 'src/theory/strings/regexp_operation.cpp')
| -rw-r--r-- | src/theory/strings/regexp_operation.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index fef6cec96..954f8603a 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -1255,7 +1255,12 @@ 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);
+ if(checkConstRegExp(r1) && checkConstRegExp(r2)) {
+ return intersectInternal(r1, r2, cache, spflag);
+ } else {
+ spflag = true;
+ return Node::null();
+ }
}
Node RegExpOpr::complement(Node r, int &ret) {
|