diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-12-04 16:13:41 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-12-04 16:13:41 -0600 |
| commit | 31175341b81e26f7373d75f65cddc69386f0ac86 (patch) | |
| tree | 12892f55e82fc22224b32310bbab5e1db76a4585 /src/theory/strings/regexp_operation.h | |
| parent | c2d84b857aabfaf949f80726a8660ee72ce14ad9 (diff) | |
clean up and improve intersection
Diffstat (limited to 'src/theory/strings/regexp_operation.h')
| -rw-r--r-- | src/theory/strings/regexp_operation.h | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index 3b898e5f5..a522161fb 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -65,6 +65,7 @@ private: 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, bool > d_norv_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 ); @@ -75,11 +76,11 @@ private: bool isPairNodesInSet(std::set< PairNodes > &s, Node n1, Node n2); 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 ); bool containC2(unsigned cnt, Node n); 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 ); + bool testNoRV(Node r); + Node intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > cache, unsigned cnt ); Node removeIntersection(Node r); void firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset ); |