diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-09 12:11:35 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-09 20:11:35 +0000 |
commit | ba06bb6c4cd2b16437fcfe5fe29acb6c8c890649 (patch) | |
tree | e6e7cf2634bd44a892ae93aa9c2605193efd26e0 | |
parent | b384526f32eab67bce49c26e38d9bd7d8b1baca0 (diff) |
New C++ Api: Clean up usage of internal kind. (#6087)
-rw-r--r-- | src/api/cvc4cpp.cpp | 61 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 10 |
2 files changed, 32 insertions, 39 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index fbbaeee24..0ce3ee058 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -659,13 +659,37 @@ const static std::unordered_set<Kind, KindHashFunction> s_indexed_kinds( namespace { +/** Convert a CVC4::Kind (internal) to a CVC4::api::Kind (external). */ +CVC4::api::Kind intToExtKind(CVC4::Kind k) +{ + auto it = api::s_kinds_internal.find(k); + if (it == api::s_kinds_internal.end()) + { + return api::INTERNAL_KIND; + } + return it->second; +} + +/** Convert a CVC4::api::Kind (external) to a CVC4::Kind (internal). */ +CVC4::Kind extToIntKind(CVC4::api::Kind k) +{ + auto it = api::s_kinds.find(k); + if (it == api::s_kinds.end()) + { + return CVC4::Kind::UNDEFINED_KIND; + } + return it->second; +} + +/** Return true if given kind is a defined external kind. */ bool isDefinedKind(Kind k) { return k > UNDEFINED_KIND && k < LAST_KIND; } -/** Returns true if the internal kind is one where the API term structure - * differs from internal structure. This happens for APPLY_* kinds. - * The API takes a "higher-order" perspective and treats functions as well - * as datatype constructors/selectors/testers as terms - * but interally they are not +/** + * Return true if the internal kind is one where the API term structure + * differs from internal structure. This happens for APPLY_* kinds. + * The API takes a "higher-order" perspective and treats functions as well + * as datatype constructors/selectors/testers as terms + * but interally they are not */ bool isApplyKind(CVC4::Kind k) { @@ -674,12 +698,14 @@ bool isApplyKind(CVC4::Kind k) } #ifdef CVC4_ASSERTIONS +/** Return true if given kind is a defined internal kind. */ bool isDefinedIntKind(CVC4::Kind k) { return k != CVC4::Kind::UNDEFINED_KIND && k != CVC4::Kind::LAST_KIND; } #endif +/** Return the minimum arity of given kind. */ uint32_t minArity(Kind k) { Assert(isDefinedKind(k)); @@ -695,6 +721,7 @@ uint32_t minArity(Kind k) return min; } +/** Return the maximum arity of given kind. */ uint32_t maxArity(Kind k) { Assert(isDefinedKind(k)); @@ -5969,28 +5996,4 @@ Options& Solver::getOptions(void) { return d_smtEngine->getOptions(); } } // namespace api -/* -------------------------------------------------------------------------- */ -/* Kind Conversions */ -/* -------------------------------------------------------------------------- */ - -CVC4::api::Kind intToExtKind(CVC4::Kind k) -{ - auto it = api::s_kinds_internal.find(k); - if (it == api::s_kinds_internal.end()) - { - return api::INTERNAL_KIND; - } - return it->second; -} - -CVC4::Kind extToIntKind(CVC4::api::Kind k) -{ - auto it = api::s_kinds.find(k); - if (it == api::s_kinds.end()) - { - return CVC4::Kind::UNDEFINED_KIND; - } - return it->second; -} - } // namespace CVC4 diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 1d6367b31..3d26f5c7b 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -20,10 +20,6 @@ #define CVC4__API__CVC4CPP_H #include "api/cvc4cppkind.h" -// !!! Only temporarily public until the parser is fully migrated to the new -// API. !!! -#include "expr/kind.h" -// !!! #include <map> #include <memory> @@ -3639,11 +3635,5 @@ class CVC4_PUBLIC Solver }; } // namespace api - -// !!! Only temporarily public until the parser is fully migrated to the -// new API. !!! -CVC4::api::Kind intToExtKind(CVC4::Kind k); -CVC4::Kind extToIntKind(CVC4::api::Kind k); - } // namespace CVC4 #endif |