diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-11-06 10:43:06 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-11-06 10:59:42 -0600 |
| commit | e79fe51d91c329a92b9141a65305ebce5c108c21 (patch) | |
| tree | eebd164e2177adaeeafc75d81de6139a3ff27d44 /src/theory/strings/theory_strings.h | |
| parent | ad0f78965f23b0994cac6a210650697b9a20cceb (diff) | |
add seperate regular expression files
Diffstat (limited to 'src/theory/strings/theory_strings.h')
| -rw-r--r-- | src/theory/strings/theory_strings.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 8f21888a2..1291fc94e 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -22,6 +22,7 @@ #include "theory/theory.h" #include "theory/uf/equality_engine.h" #include "theory/strings/theory_strings_preprocess.h" +#include "theory/strings/regexp_operation.h" #include "context/cdchunk_list.h" @@ -252,6 +253,12 @@ protected: void seperateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts ); void printConcat( std::vector< Node >& n, const char * c ); + // Regular Expression +private: + RegExpOpr d_regexp_opr; + CVC4::String getHeadConst( Node x ); + bool splitRegExp( Node x, Node r, Node ant ); + private: // Finite Model Finding //bool d_fmf; |