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/api/cvc4cppkind.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/api/cvc4cppkind.h')
| -rw-r--r-- | src/api/cvc4cppkind.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 591ff9b1e..ca5696537 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -2172,6 +2172,14 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind) */ REGEXP_SIGMA, + /** + * Regexp complement. + * Parameters: 1 + * -[1]: Term of sort RegExp + * Create with: + * mkTerm(Kind kind, Term child1) + */ + REGEXP_COMPLEMENT, #if 0 /* regexp rv (internal use only) */ REGEXP_RV, |