mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

fix multiplier base for #5022

Browse source 
add also some C++ API shorthands for retrieving numerals
This commit is contained in:
Nikolaj Bjorner 2021-02-12 11:53:40 -08:00
parent d0c96abe30
commit c808f74591
2 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/api/c++/z3++.h
View file

@ -825,6 +825,11 @@ namespace z3 {
bool is_numeral(double& d) const { if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; } bool is_numeral(double& d) const { if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; }
bool as_binary(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_binary_string(ctx(), m_ast); check_error(); return true; } bool as_binary(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_binary_string(ctx(), m_ast); check_error(); return true; }
double as_double() const { double d = 0; is_numeral(d); return d; }
uint64_t as_uint64() const { uint64_t r = 0; is_numeral_u64(r); return r; }
uint64_t as_int64() const { int64_t r = 0; is_numeral_i64(r); return r; }
/** /**
\brief Return true if this expression is an application. \brief Return true if this expression is an application.
*/ */

4
src/util/mpz.cpp
View file

@ -1682,9 +1682,9 @@ double mpz_manager<SYNCH>::get_double(mpz const & a) const {
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
r += d * static_cast<double>(digits(a)[i]); r += d * static_cast<double>(digits(a)[i]);
if (sizeof(digit_t) == sizeof(uint64_t)) if (sizeof(digit_t) == sizeof(uint64_t))
d *= static_cast<double>(UINT64_MAX); // 64-bit version d *= (1.0 + static_cast<double>(UINT64_MAX)); // 64-bit version, multiply by 2^64
else else
d *= static_cast<double>(UINT_MAX); // 32-bit version d *= (1.0 + static_cast<double>(UINT_MAX)); // 32-bit version, multiply by 2^32
} }
if (!(r >= 0.0)) { if (!(r >= 0.0)) {
r = static_cast<double>(UINT64_MAX); // some large number r = static_cast<double>(UINT64_MAX); // some large number