summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2021-03-09 12:11:35 -0800
committerGitHub <noreply@github.com>2021-03-09 20:11:35 +0000
commitba06bb6c4cd2b16437fcfe5fe29acb6c8c890649 (patch)
treee6e7cf2634bd44a892ae93aa9c2605193efd26e0
parentb384526f32eab67bce49c26e38d9bd7d8b1baca0 (diff)
New C++ Api: Clean up usage of internal kind. (#6087)
-rw-r--r--src/api/cvc4cpp.cpp61
-rw-r--r--src/api/cvc4cpp.h10
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback