adds intersection

2 files changed, 9 insertions, 1 deletions

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

 };