diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-11-26 22:09:38 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-11-26 22:09:38 -0600 |
| commit | 388a6acf4acd50a7611faae91b3489ac2209e584 (patch) | |
| tree | 481b5e06632ead33c41d683357e6f0767d7a8479 /src/theory/strings/regexp_operation.h | |
| parent | 02dd486ff30041764da04a016b0abdc75a6a3d93 (diff) | |
add intersection rewriting
Diffstat (limited to 'src/theory/strings/regexp_operation.h')
| -rw-r--r-- | src/theory/strings/regexp_operation.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index 6a31a23fb..3b898e5f5 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -64,6 +64,7 @@ private: 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; + std::map< Node, Node > d_rm_inter_cache; std::map< Node, std::vector< PairNodes > > d_split_cache; //bool checkStarPlus( Node t ); void simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes ); @@ -79,6 +80,7 @@ private: Node convert1(unsigned cnt, Node n); void convert2(unsigned cnt, Node n, Node &r1, Node &r2); Node intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node > cache, bool &spflag, unsigned cnt ); + Node removeIntersection(Node r); void firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset ); //TODO: for intersection |