diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-08-27 17:28:08 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-27 17:28:08 -0700 |
commit | fa55d0680afab5d319f393bafd3f7ecdf8870b1f (patch) | |
tree | 80e7be0751c8675ff18620cea2697b647b411b12 /src/api | |
parent | a442b02d9a695a04f12d58fee71f7e1afbfa1473 (diff) |
New C++ API: Fix isDefinedKind() to not be ambigious with respect to … (#2384)
…underlying type.
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cvc4cppkind.h | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 65affcad4..f91f934f9 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -30,8 +30,13 @@ namespace api { /** * The kind of a CVC4 term. + * + * Note that the underlying type of Kind must be signed (to enable range + * checks for validity). The size of this type depends on the size of + * CVC4::Kind (__CVC4__EXPR__NODE_VALUE__NBITS__KIND, currently 10 bits, + * see expr/metakind_template.h). */ -enum CVC4_PUBLIC Kind +enum CVC4_PUBLIC Kind : int32_t { /** * Internal kind. |