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 | |
| 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')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 2 | ||||
| -rw-r--r-- | src/api/cvc4cppkind.h | 8 |
2 files changed, 10 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 622d48ac9..4e5f4604e 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -277,6 +277,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {REGEXP_LOOP, CVC4::Kind::REGEXP_LOOP}, {REGEXP_EMPTY, CVC4::Kind::REGEXP_EMPTY}, {REGEXP_SIGMA, CVC4::Kind::REGEXP_SIGMA}, + {REGEXP_COMPLEMENT, CVC4::Kind::REGEXP_COMPLEMENT}, /* Quantifiers --------------------------------------------------------- */ {FORALL, CVC4::Kind::FORALL}, {EXISTS, CVC4::Kind::EXISTS}, @@ -540,6 +541,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::REGEXP_LOOP, REGEXP_LOOP}, {CVC4::Kind::REGEXP_EMPTY, REGEXP_EMPTY}, {CVC4::Kind::REGEXP_SIGMA, REGEXP_SIGMA}, + {CVC4::Kind::REGEXP_COMPLEMENT, REGEXP_COMPLEMENT}, /* Quantifiers ----------------------------------------------------- */ {CVC4::Kind::FORALL, FORALL}, {CVC4::Kind::EXISTS, EXISTS}, 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, |