New C++ API: Fix isDefinedKind() to not be ambigious with respect to … (#2384)
authorAina Niemetz <aina.niemetz@gmail.com>
Tue, 28 Aug 2018 00:28:08 +0000 (17:28 -0700)
committerAndres Noetzli <andres.noetzli@gmail.com>
Tue, 28 Aug 2018 00:28:08 +0000 (17:28 -0700)
…underlying type.

src/api/cvc4cppkind.h

index 65affcad4e4b245af3b1e49eae4257f133c27246..f91f934f9369774390c04a0d6cc2d935d66c1cbb 100644 (file)
@@ -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.