projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
a442b02
)
New C++ API: Fix isDefinedKind() to not be ambigious with respect to … (#2384)
author
Aina Niemetz
<aina.niemetz@gmail.com>
Tue, 28 Aug 2018 00:28:08 +0000
(17:28 -0700)
committer
Andres Noetzli
<andres.noetzli@gmail.com>
Tue, 28 Aug 2018 00:28:08 +0000
(17:28 -0700)
…underlying type.
src/api/cvc4cppkind.h
patch
|
blob
|
history
diff --git
a/src/api/cvc4cppkind.h
b/src/api/cvc4cppkind.h
index 65affcad4e4b245af3b1e49eae4257f133c27246..f91f934f9369774390c04a0d6cc2d935d66c1cbb 100644
(file)
--- 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.