diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-07-28 10:44:55 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-28 12:44:55 -0500 |
| commit | 7ad41fe71b9f7d206ee6d1c642bb7926bffea6c7 (patch) | |
| tree | fc5d9cb07fbce3a28395eb30aabb6d6633724e02 /src/api/cvc4cpp.cpp | |
| parent | e63544462eb850a27f7b416f2f0613efb96eef1d (diff) | |
Supporting seq.nth (#4723)
This PR adds support for seq.nth operator by eliminating it during expandDefinitions, based on sub-sequences.
Tests that use this operator are also included.
Diffstat (limited to 'src/api/cvc4cpp.cpp')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index fa995a00a..c009f69e5 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -305,6 +305,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {SEQ_SUFFIX, CVC4::Kind::STRING_SUFFIX}, {CONST_SEQUENCE, CVC4::Kind::CONST_SEQUENCE}, {SEQ_UNIT, CVC4::Kind::SEQ_UNIT}, + {SEQ_NTH, CVC4::Kind::SEQ_NTH}, /* Quantifiers --------------------------------------------------------- */ {FORALL, CVC4::Kind::FORALL}, {EXISTS, CVC4::Kind::EXISTS}, @@ -580,6 +581,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::REGEXP_COMPLEMENT, REGEXP_COMPLEMENT}, {CVC4::Kind::CONST_SEQUENCE, CONST_SEQUENCE}, {CVC4::Kind::SEQ_UNIT, SEQ_UNIT}, + {CVC4::Kind::SEQ_NTH, SEQ_NTH}, /* Quantifiers ----------------------------------------------------- */ {CVC4::Kind::FORALL, FORALL}, {CVC4::Kind::EXISTS, EXISTS}, |