diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-30 09:17:00 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-07-30 09:17:00 -0500 |
| commit | c9fa0516fd28b48940edf2a714e33bee6eacc396 (patch) | |
| tree | c5c2f6a3689b3984fe19ab2610fe53d98f1fc36a /src/theory/strings/regexp_operation.cpp | |
| parent | 943a4781526e5d5e9ca943a0955f30fbb9f7ba61 (diff) | |
Handle RE intersections modulo equality (#3120)
Diffstat (limited to 'src/theory/strings/regexp_operation.cpp')
| -rw-r--r-- | src/theory/strings/regexp_operation.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index bd693c6c3..f11254794 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -1493,9 +1493,12 @@ Node RegExpOpr::intersect(Node r1, Node r2, bool &spflag) { Node rr1 = removeIntersection(r1); Node rr2 = removeIntersection(r2); std::map< PairNodes, Node > cache; + Trace("regexp-intersect-node") << "Intersect (1): " << rr1 << std::endl; + Trace("regexp-intersect-node") << "Intersect (2): " << rr2 << std::endl; Trace("regexp-intersect") << "Start INTERSECTION(\n\t" << mkString(r1) << ",\n\t"<< mkString(r2) << ")" << std::endl; Node retNode = intersectInternal(rr1, rr2, cache, 1); Trace("regexp-intersect") << "End INTERSECTION(\n\t" << mkString(r1) << ",\n\t"<< mkString(r2) << ") =\n\t" << mkString(retNode) << std::endl; + Trace("regexp-intersect-node") << "Intersect finished." << std::endl; return retNode; } else { spflag = true; |