diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-26 13:54:41 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-26 13:54:41 -0600 |
commit | b320aa323923822a7702997bbca05e8512da55a4 (patch) | |
tree | 62ed510b54bbfef908296a264002052efc4fff98 /src/theory/strings/regexp_operation.h | |
parent | f26ea8026e94252e4f1418be473d10a5f957b988 (diff) |
Basic support for regular expression complement (#3437)
Fixes #3408 .
Adds basic rewriter, parsing, type checking and implements the required cases in regexp_operation.cpp. It also adds some missing documentation in regexp_operation.h
Diffstat (limited to 'src/theory/strings/regexp_operation.h')
-rw-r--r-- | src/theory/strings/regexp_operation.h | 21 |
1 files changed, 19 insertions, 2 deletions
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index 91d5df744..b9dbedba5 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -41,10 +41,13 @@ namespace strings { */ enum RegExpConstType { - // the regular expression doesn't contain variables or re.allchar or re.range + // the regular expression doesn't contain variables or re.comp, + // re.allchar or re.range (call these three operators "non-concrete + // operators"). Notice that re.comp is a non-concrete operator + // since it can be seen as indirectly defined in terms of re.allchar. RE_C_CONRETE_CONSTANT, // the regular expression doesn't contain variables, but may contain - // re.allchar or re.range + // re.comp, re.allchar or re.range RE_C_CONSTANT, // the regular expression may contain variables RE_C_VARIABLE, @@ -122,6 +125,20 @@ class RegExpOpr { /** is k a native operator whose return type is a regular expression? */ static bool isRegExpKind(Kind k); void simplify(Node t, std::vector< Node > &new_nodes, bool polarity); + /** + * This method returns 1 if the empty string is in r, 2 if the empty string + * is not in r, or 0 if it is unknown whether the empty string is in r. + * TODO (project #2): refactor the return value of this function. + * + * If this method returns 0, then exp is updated to an explanation that + * would imply that the empty string is in r. + * + * For example, + * - delta( (re.inter (str.to.re x) (re.* "A")) ) returns 0 and sets exp to + * x = "", + * - delta( (re.++ (str.to.re "A") R) ) returns 2, + * - delta( (re.union (re.* "A") R) ) returns 1. + */ int delta( Node r, Node &exp ); int derivativeS( Node r, CVC4::String c, Node &retNode ); Node derivativeSingle( Node r, CVC4::String c ); |