From abdb1691f287587f18801733e4ab7248167db1ca Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Tue, 25 Mar 2014 01:08:29 -0500
Subject: [PATCH] adds intersection

---
 src/theory/strings/regexp_operation.cpp | 6 ++++++
 src/theory/strings/regexp_operation.h   | 4 +++-
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 52c76880b..d02baf3a7 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -695,8 +695,10 @@ 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;
 					}
@@ -1202,11 +1204,13 @@ void RegExpOpr::getCharSet( Node r, std::set<unsigned> &pcset, SetNodes &pvset )
 	}
 }
 
+
 Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< unsigned, std::set< PairNodes > > cache, bool &spflag ) {
 	if(spflag) {
 		//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;
@@ -1276,6 +1280,7 @@ 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;
@@ -1286,6 +1291,7 @@ 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);
+
 }
 //printing
 std::string RegExpOpr::niceChar( Node r ) {
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index fcac28890..5ff054033 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -33,7 +33,9 @@ namespace theory {
 namespace strings {
 
 class RegExpOpr {
+
 	typedef std::pair< Node, CVC4::String > PairNodeStr;
+
 	typedef std::set< Node > SetNodes;
 	typedef std::pair< Node, Node > PairNodes;
 
@@ -70,6 +72,7 @@ private:
 	Node mkAllExceptOne( char c );
 
 	void getCharSet( Node r, std::set<unsigned> &pcset, SetNodes &pvset );
+
 	Node intersectInternal( Node r1, Node r2, std::map< unsigned, std::set< PairNodes > > cache, bool &spflag );
 	void firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset );
 
@@ -86,7 +89,6 @@ public:
 	Node derivativeSingle( Node r, CVC4::String c );
 	bool guessLength( Node r, int &co );
 	Node intersect(Node r1, Node r2, bool &spflag);
-
 	std::string mkString( Node r );
 };
 
-- 
2.30.2