diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-07-25 13:43:44 -0500 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-07-25 13:43:44 -0500 |
| commit | c143281522a76a0fae3bb4167feca75e5aef326a (patch) | |
| tree | 59fd6126a3d5f4ba9aff6f14b16b8417bdc0fb70 /src/theory/strings/regexp_operation.h | |
| parent | 4e1e7cae681ac746a79505420dc0cc1febee226c (diff) | |
patch for regular expression intersection caching
Diffstat (limited to 'src/theory/strings/regexp_operation.h')
| -rw-r--r-- | src/theory/strings/regexp_operation.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index e4ae1208d..2ae578cd6 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -69,9 +69,14 @@ private: std::string niceChar( Node r ); int gcd ( int a, int b ); Node mkAllExceptOne( char c ); + 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 ); void firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset ); //TODO: for intersection |