From 22acfb03456d5816c550d822ef7e27d147475eee Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Mon, 5 May 2014 18:01:14 -0500 Subject: add constant regular expression check for intersection. --- src/theory/strings/regexp_operation.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'src/theory') 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) { -- cgit v1.2.3