adds intersection

1 files changed, 34 insertions, 17 deletions

diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index 7b41c1764..9bd694f5c 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -1,17 +1,17 @@
-/*********************                                                        */
-/*! \file regexp_operation.h
- ** \verbatim
- ** Original author: Tianyi Liang
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Regular Expression Operations

+/*********************                                                        */

+/*! \file regexp_operation.h

+ ** \verbatim

+ ** Original author: Tianyi Liang

+ ** Major contributors: none

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 project.

+ ** Copyright (c) 2009-2013  New York University and The University of Iowa

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

  **

- ** Regular Expression Operations

+ ** \brief Symbolic Regular Expresion Operations

+ **

+ ** Symbolic Regular Expression Operations

  **/

 

 #include "cvc4_private.h"

@@ -20,7 +20,10 @@
 #define __CVC4__THEORY__STRINGS__REGEXP__OPERATION_H

 

 #include <vector>

+#include <set>

+#include <algorithm>

 #include "util/hash.h"

+#include "util/regexp.h"

 #include "theory/theory.h"

 #include "theory/rewriter.h"

 //#include "context/cdhashmap.h"

@@ -31,11 +34,15 @@ namespace strings {
 

 class RegExpOpr {

 	typedef std::pair< Node, CVC4::String > PairDvStr;

+	typedef std::set< Node > SetNodes;

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

 

 private:

+	unsigned d_card;

     Node d_emptyString;

     Node d_true;

     Node d_false;

+	Node d_emptySingleton;

 	Node d_emptyRegexp;

 	Node d_zero;

 	Node d_one;

@@ -45,12 +52,15 @@ private:
 	Node d_sigma;

 	Node d_sigma_star;

 	

-	std::map< std::pair< Node, Node >, Node > d_simpl_cache;

-	std::map< std::pair< Node, Node >, Node > d_simpl_neg_cache;

+	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, int > d_delta_cache;

 	std::map< PairDvStr, Node > d_dv_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;

+	std::map< PairNodes, Node > d_inter_cache;

 	//bool checkStarPlus( Node t );

 	void simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes );

 	void simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes );

@@ -58,6 +68,13 @@ private:
 	int gcd ( int a, int b );

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

+	void firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset );

+

+	//TODO: for intersection

+	bool follow( Node r, CVC4::String c, std::vector< char > &vec_chars );

+

 public:

 	RegExpOpr();

 

@@ -66,8 +83,8 @@ public:
 	int delta( Node r );

 	Node derivativeSingle( Node r, CVC4::String c );

 	bool guessLength( Node r, int &co );

-	void firstChar( Node r );

-	bool follow( Node r, CVC4::String c, std::vector< char > &vec_chars );

+	Node intersect(Node r1, Node r2);

+

 	std::string mkString( Node r );

 };