Merge branch 'master' of github.com:tiliang/CVC4

Conflicts:
	src/theory/strings/regexp_operation.cpp
	src/theory/strings/regexp_operation.h

2 files changed, 3 insertions, 9 deletions

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 8cb8c124a..528436033 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -695,10 +695,8 @@ 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;

 					}

@@ -1210,7 +1208,6 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< unsigned, std::se
 		//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;

@@ -1280,7 +1277,6 @@ 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;

@@ -1291,7 +1287,6 @@ 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);

-
 }

 

 Node RegExpOpr::complement(Node r, int &ret) {

diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index 5ff054033..116868820 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -33,9 +33,7 @@ namespace theory {
 namespace strings {

 

 class RegExpOpr {

-
 	typedef std::pair< Node, CVC4::String > PairNodeStr;

-
 	typedef std::set< Node > SetNodes;

 	typedef std::pair< Node, Node > PairNodes;

 

@@ -56,10 +54,10 @@ private:
 	

 	std::map< PairNodes, Node > d_simpl_cache;

 	std::map< PairNodes, Node > d_simpl_neg_cache;

-	std::map< Node, Node > d_compl_cache;

 	std::map< Node, std::pair< int, Node > > d_delta_cache;

 	std::map< PairNodeStr, Node > d_dv_cache;

 	std::map< PairNodeStr, std::pair< Node, int > > d_deriv_cache;

+	std::map< Node, std::pair< Node, int > > d_compl_cache;

 	std::map< Node, bool > d_cstre_cache;

 	std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_cset_cache;

 	std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_fset_cache;

@@ -72,7 +70,6 @@ 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 );

 

@@ -89,6 +86,8 @@ public:
 	Node derivativeSingle( Node r, CVC4::String c );

 	bool guessLength( Node r, int &co );

 	Node intersect(Node r1, Node r2, bool &spflag);

+	Node complement(Node r, int &ret);

+

 	std::string mkString( Node r );

 };