diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-03-25 01:08:29 -0500 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-03-27 16:56:14 -0500 |
| commit | 03034910cedc64a1a3a5d83715c79294cb35bee8 (patch) | |
| tree | a5fcdf31fb0b21bc62b47ec001c4d59f0ab9bede /src/theory/strings/theory_strings.h | |
| parent | c4f976a5c8338042f92da98bc54266ff55652833 (diff) | |
adds intersection
Diffstat (limited to 'src/theory/strings/theory_strings.h')
| -rw-r--r-- | src/theory/strings/theory_strings.h | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index e07c61a19..355c536dd 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -118,12 +118,6 @@ private: */ Node d_ufSubstr; - /** - * Function symbol used to implement uninterpreted undefined string - * semantics. Needed to deal with partial str2int function. - */ - Node d_ufS2I; - // Constants Node d_emptyString; Node d_emptyRegexp; @@ -308,12 +302,15 @@ private: NodeSet d_pos_ctn_cached; NodeSet d_neg_ctn_cached; - // Regular Expression + // Symbolic Regular Expression private: // regular expression memberships NodeList d_regexp_memberships; NodeSet d_regexp_ucached; NodeSet d_regexp_ccached; + // intersection + NodeListMap d_str_re_map; + NodeNodeMap d_inter_cache; // antecedant for why regexp membership must be true NodeNodeMap d_regexp_ant; // membership length @@ -324,6 +321,7 @@ private: CVC4::String getHeadConst( Node x ); bool splitRegExp( Node x, Node r, Node ant ); bool addMembershipLength(Node atom); + void addMembership(Node assertion); // Finite Model Finding |