From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Mon, 5 May 2014 23:01:14 +0000 (-0500)
Subject: add constant regular expression check for intersection.
X-Git-Tag: cvc5-1.0.0~6930
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=22acfb03456d5816c550d822ef7e27d147475eee;p=cvc5.git

add constant regular expression check for intersection.
---

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) {