Avoid ambiguous overloads in BitVector (#2169)

`long` is a 32-bit integer on Windows. CVC4's BitVector class had a
constructor for `unsigned int` and `unsigned long`, which lead to issues
with the new CVC4 C++ API because the two constructors were ambiguous
overloads. This commit changes the constructors to use `uint32_t` and
`uint64_t`, which are plattform independent and more explicit (mirroring

diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index a82e74a0d795df8991699e2e447efc97a220f20c..afee609cf64b82e8c4f755a4d3ebfeeeff4cac04 100644 (file)
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -274,21 +274,20 @@ symbolicRoundingMode::symbolicRoundingMode(const symbolicRoundingMode &old)
 symbolicProposition symbolicRoundingMode::valid(void) const
 {
   NodeManager *nm = NodeManager::currentNM();
-  Node zero(nm->mkConst(
-      BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, (long unsigned int)0)));
+  Node zero(nm->mkConst(BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, 0u)));
 
   // Is there a better encoding of this?
   return symbolicProposition(nm->mkNode(
       kind::BITVECTOR_AND,
-      nm->mkNode(kind::BITVECTOR_COMP,
-                 nm->mkNode(kind::BITVECTOR_AND,
-                            *this,
-                            nm->mkNode(kind::BITVECTOR_SUB,
-                                       *this,
-                                       nm->mkConst(BitVector(
-                                           SYMFPU_NUMBER_OF_ROUNDING_MODES,
-                                           (long unsigned int)1)))),
-                 zero),
+      nm->mkNode(
+          kind::BITVECTOR_COMP,
+          nm->mkNode(kind::BITVECTOR_AND,
+                     *this,
+                     nm->mkNode(kind::BITVECTOR_SUB,
+                                *this,
+                                nm->mkConst(BitVector(
+                                    SYMFPU_NUMBER_OF_ROUNDING_MODES, 1u)))),
+          zero),
       nm->mkNode(kind::BITVECTOR_NOT,
                  nm->mkNode(kind::BITVECTOR_COMP, *this, zero))));
 }

diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index fbd1c60b73c3b8daafa14b11eb5c7894cd828263..13c1f14dd901e8ac7bf612f8b7216fc5f2d01720 100644 (file)
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -19,6 +19,7 @@
 #ifndef __CVC4__BITVECTOR_H
 #define __CVC4__BITVECTOR_H
 
+#include <cstdint>
 #include <iosfwd>
 
 #include "base/exception.h"
@@ -36,12 +37,26 @@ class CVC4_PUBLIC BitVector
 
   BitVector(unsigned size = 0) : d_size(size), d_value(0) {}
 
-  BitVector(unsigned size, unsigned int z) : d_size(size), d_value(z)
+  /**
+   * BitVector constructor using a 32-bit unsigned integer for the value.
+   *
+   * Note: we use an explicit bit-width here to be consistent across
+   * platforms (long is 32-bit when compiling 64-bit binaries on
+   * Windows but 64-bit on Linux) and to prevent ambiguous overloads.
+   */
+  BitVector(unsigned size, uint32_t z) : d_size(size), d_value(z)
   {
     d_value = d_value.modByPow2(size);
   }
 
-  BitVector(unsigned size, unsigned long int z) : d_size(size), d_value(z)
+  /**
+   * BitVector constructor using a 64-bit unsigned integer for the value.
+   *
+   * Note: we use an explicit bit-width here to be consistent across
+   * platforms (long is 32-bit when compiling 64-bit binaries on
+   * Windows but 64-bit on Linux) and to prevent ambiguous overloads.
+   */
+  BitVector(unsigned size, uint64_t z) : d_size(size), d_value(z)
   {
     d_value = d_value.modByPow2(size);
   }