diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-28 11:05:09 -0600 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-28 22:59:00 -0600 |
commit | acb79cbe43ddcd855db042b7c937fc2eacaa0ac3 (patch) | |
tree | e8af21bba458cbc2a00d3512519cea3e07af3b65 /src/theory/strings/regexp_operation.h | |
parent | 76f497ef9444a81143ad35b2eda899e119b8e662 (diff) |
a new regular expression engine for solving both positive and negative membership constraints
Diffstat (limited to 'src/theory/strings/regexp_operation.h')
-rw-r--r-- | src/theory/strings/regexp_operation.h | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index d7dde018a..32bfb2b3d 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -32,25 +32,33 @@ class RegExpOpr { typedef std::pair< Node, CVC4::String > PairDvStr;
private:
Node d_emptyString;
+ Node d_true;
+ Node d_false;
+ Node d_emptyRegexp;
+ Node d_zero;
+ Node d_one;
+
char d_char_start;
char d_char_end;
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< 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;
//bool checkStarPlus( Node t );
- void simplifyRegExp( Node s, Node r, std::vector< Node > &new_nodes );
+ void simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes );
+ void simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes );
std::string niceChar( Node r );
int gcd ( int a, int b );
public:
RegExpOpr();
bool checkConstRegExp( Node r );
- void simplify(Node t, std::vector< Node > &new_nodes);
+ void simplify(Node t, std::vector< Node > &new_nodes, bool polarity);
Node mkAllExceptOne( char c );
Node complement( Node r );
int delta( Node r );
|