diff options
| author | makaimann <makaim@stanford.edu> | 2020-06-04 18:21:37 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-04 18:21:37 -0700 |
| commit | a2fc412f22552ae0e8f9c36650d1de2d362638dd (patch) | |
| tree | 5f66f0f8128a826e6099845191ccbe5efdd0f3c3 /src/api/cvc4cpp.cpp | |
| parent | 67678d6c8a28e71483d8171311725e9e1a86775c (diff) | |
Add a method for retrieving base of a constant array through API (#4494)
Diffstat (limited to 'src/api/cvc4cpp.cpp')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 734fcddae..164df0631 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -213,7 +213,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ /* Arrays -------------------------------------------------------------- */ {SELECT, CVC4::Kind::SELECT}, {STORE, CVC4::Kind::STORE}, - {STORE_ALL, CVC4::Kind::STORE_ALL}, + {CONST_ARRAY, CVC4::Kind::STORE_ALL}, /* Datatypes ----------------------------------------------------------- */ {APPLY_SELECTOR, CVC4::Kind::APPLY_SELECTOR}, {APPLY_CONSTRUCTOR, CVC4::Kind::APPLY_CONSTRUCTOR}, @@ -479,7 +479,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> /* Arrays ---------------------------------------------------------- */ {CVC4::Kind::SELECT, SELECT}, {CVC4::Kind::STORE, STORE}, - {CVC4::Kind::STORE_ALL, STORE_ALL}, + {CVC4::Kind::STORE_ALL, CONST_ARRAY}, /* Datatypes ------------------------------------------------------- */ {CVC4::Kind::APPLY_SELECTOR, APPLY_SELECTOR}, {CVC4::Kind::APPLY_CONSTRUCTOR, APPLY_CONSTRUCTOR}, @@ -1492,6 +1492,15 @@ bool Term::isConst() const return d_expr->isConst(); } +Term Term::getConstArrayBase() const +{ + CVC4_API_CHECK_NOT_NULL; + // CONST_ARRAY kind maps to STORE_ALL internal kind + CVC4_API_CHECK(d_expr->getKind() == CVC4::Kind::STORE_ALL) + << "Expecting a CONST_ARRAY Term when calling getConstArrayBase()"; + return Term(d_solver, d_expr->getConst<ArrayStoreAll>().getExpr()); +} + Term Term::notTerm() const { CVC4_API_CHECK_NOT_NULL; |