diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-07-15 04:25:57 -0700 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-07-15 04:25:57 -0700 |
| commit | d4c49e755a53e7333c7638a5aeafe8baa2ea56d3 (patch) | |
| tree | d5e31f1b318cf85ed511c37f9afc5ab836700386 /src/theory/fp | |
| parent | 292b2c5712ce31282ac3ec564f268ee7f0aa3506 (diff) | |
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
Diffstat (limited to 'src/theory/fp')
| -rw-r--r-- | src/theory/fp/fp_converter.cpp | 21 |
1 files changed, 10 insertions, 11 deletions
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index a82e74a0d..afee609cf 100644 --- 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)))); } |