From 2fa304d8dea48687cdc6dec79b81323a7ea85825 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Sat, 31 Mar 2018 14:45:04 +0700 Subject: [PATCH] Remove int64, uint64 typedefs in favor of int64_t / uint64_t. --- src/api/api_context.cpp | 2 +- src/api/api_numeral.cpp | 2 +- src/ast/ast.h | 12 +-- src/ast/ast_smt2_pp.cpp | 2 +- src/ast/bv_decl_plugin.h | 2 +- src/ast/dl_decl_plugin.cpp | 12 +-- src/ast/dl_decl_plugin.h | 12 +-- src/ast/fpa/fpa2bv_converter.cpp | 2 +- src/ast/rewriter/bv_rewriter.cpp | 26 +++--- src/ast/rewriter/dl_rewriter.cpp | 2 +- src/math/hilbert/hilbert_basis.h | 2 +- src/math/polynomial/polynomial.cpp | 4 +- src/math/polynomial/polynomial.h | 4 +- src/math/polynomial/upolynomial.h | 4 +- .../polynomial/upolynomial_factorization.cpp | 6 +- src/math/subpaving/subpaving.cpp | 4 +- src/math/subpaving/subpaving_t.h | 16 ++-- src/muz/base/dl_context.cpp | 20 ++--- src/muz/base/dl_context.h | 10 +-- src/muz/base/dl_costs.cpp | 2 +- src/muz/base/dl_costs.h | 2 +- src/muz/base/dl_util.cpp | 12 +-- src/muz/base/dl_util.h | 6 +- src/muz/ddnf/ddnf.cpp | 4 +- src/muz/fp/datalog_parser.cpp | 32 +++---- src/muz/rel/dl_base.cpp | 2 +- src/muz/rel/dl_base.h | 2 +- src/muz/rel/dl_relation_manager.cpp | 10 +-- src/muz/rel/dl_sparse_table.cpp | 4 +- src/muz/rel/dl_sparse_table.h | 18 ++-- src/muz/rel/doc.cpp | 4 +- src/muz/rel/doc.h | 4 +- src/muz/rel/rel_context.cpp | 2 +- src/muz/rel/tbv.cpp | 6 +- src/muz/rel/tbv.h | 6 +- src/muz/rel/udoc_relation.cpp | 4 +- src/qe/qe_dl_plugin.cpp | 8 +- src/shell/datalog_frontend.cpp | 2 +- src/smt/smt_context.cpp | 2 +- src/smt/theory_dl.cpp | 6 +- src/tactic/bv/bv_bounds_tactic.cpp | 14 +-- src/test/algebraic.cpp | 2 +- src/test/dl_query.cpp | 6 +- src/test/mpff.cpp | 30 +++---- src/test/mpfx.cpp | 2 +- src/test/mpq.cpp | 2 +- src/test/mpz.cpp | 6 +- src/test/prime_generator.cpp | 6 +- src/test/rational.cpp | 4 +- src/util/checked_int64.h | 22 ++--- src/util/double_manager.h | 8 +- src/util/hash.h | 4 +- src/util/hwf.cpp | 36 ++++---- src/util/hwf.h | 8 +- src/util/inf_eps_rational.h | 4 +- src/util/inf_int_rational.h | 4 +- src/util/inf_rational.h | 4 +- src/util/inf_s_integer.h | 4 +- src/util/mpbq.cpp | 2 +- src/util/mpbq.h | 2 +- src/util/mpf.cpp | 16 ++-- src/util/mpf.h | 4 +- src/util/mpff.cpp | 76 ++++++++-------- src/util/mpff.h | 22 ++--- src/util/mpfx.cpp | 32 +++---- src/util/mpfx.h | 14 +-- src/util/mpn.cpp | 2 +- src/util/mpq.h | 18 ++-- src/util/mpz.cpp | 90 +++++++++---------- src/util/mpz.h | 32 +++---- src/util/mpzzp.h | 16 ++-- src/util/prime_generator.cpp | 20 ++--- src/util/prime_generator.h | 8 +- src/util/rational.h | 10 +-- src/util/rlimit.cpp | 4 +- src/util/rlimit.h | 8 +- src/util/s_integer.h | 8 +- src/util/total_order.h | 30 +++---- src/util/util.cpp | 2 +- src/util/util.h | 22 ++--- 80 files changed, 437 insertions(+), 449 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 12a4642c1..c8b365f22 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -184,7 +184,7 @@ namespace api { e = m_bv_util.mk_numeral(n, s); } else if (fid == get_datalog_fid() && n.is_uint64()) { - uint64 sz; + uint64_t sz; if (m_datalog_util.try_get_size(s, sz) && sz <= n.get_uint64()) { invoke_error_handler(Z3_INVALID_ARG); diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index ab379c3de..de9886571 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -172,7 +172,7 @@ extern "C" { if (mk_c(c)->bvutil().is_numeral(e, r, bv_size)) { return Z3_TRUE; } - uint64 v; + uint64_t v; if (mk_c(c)->datalog_util().is_numeral(e, v)) { r = rational(v, rational::ui64()); return Z3_TRUE; diff --git a/src/ast/ast.h b/src/ast/ast.h index 68e02d791..35e9a1cbb 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -298,11 +298,11 @@ class sort_size { SS_FINITE_VERY_BIG, SS_INFINITE } m_kind; - uint64 m_size; // It is only meaningful if m_kind == SS_FINITE - sort_size(kind_t k, uint64 r):m_kind(k), m_size(r) {} + uint64_t m_size; // It is only meaningful if m_kind == SS_FINITE + sort_size(kind_t k, uint64_t r):m_kind(k), m_size(r) {} public: sort_size():m_kind(SS_INFINITE) {} - sort_size(uint64 const & sz):m_kind(SS_FINITE), m_size(sz) {} + sort_size(uint64_t const & sz):m_kind(SS_FINITE), m_size(sz) {} sort_size(sort_size const& other): m_kind(other.m_kind), m_size(other.m_size) {} explicit sort_size(rational const& r) { if (r.is_uint64()) { @@ -316,7 +316,7 @@ public: } static sort_size mk_infinite() { return sort_size(SS_INFINITE, 0); } static sort_size mk_very_big() { return sort_size(SS_FINITE_VERY_BIG, 0); } - static sort_size mk_finite(uint64 r) { return sort_size(SS_FINITE, r); } + static sort_size mk_finite(uint64_t r) { return sort_size(SS_FINITE, r); } bool is_infinite() const { return m_kind == SS_INFINITE; } bool is_very_big() const { return m_kind == SS_FINITE_VERY_BIG; } @@ -324,7 +324,7 @@ public: static bool is_very_big_base2(unsigned power) { return power >= 64; } - uint64 size() const { SASSERT(is_finite()); return m_size; } + uint64_t size() const { SASSERT(is_finite()); return m_size; } }; std::ostream& operator<<(std::ostream& out, sort_size const & ss); @@ -346,7 +346,7 @@ public: decl_info(family_id, k, num_parameters, parameters, private_parameters) { } - sort_info(family_id family_id, decl_kind k, uint64 num_elements, + sort_info(family_id family_id, decl_kind k, uint64_t num_elements, unsigned num_parameters = 0, parameter const * parameters = nullptr, bool private_parameters = false): decl_info(family_id, k, num_parameters, parameters, private_parameters), m_num_elements(num_elements) { } diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 8ad7c27f1..aeaebc6bf 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -387,7 +387,7 @@ format * smt2_pp_environment::pp_string_literal(app * t) { } format * smt2_pp_environment::pp_datalog_literal(app * t) { - uint64 v; + uint64_t v; VERIFY (get_dlutil().is_numeral(t, v)); std::ostringstream buffer; buffer << v; diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 4aff8cd06..e128f2c03 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -384,7 +384,7 @@ public: app * mk_numeral(rational const & val, sort* s) const; app * mk_numeral(rational const & val, unsigned bv_size) const; - app * mk_numeral(uint64 u, unsigned bv_size) const { return mk_numeral(rational(u, rational::ui64()), bv_size); } + app * mk_numeral(uint64_t u, unsigned bv_size) const { return mk_numeral(rational(u, rational::ui64()), bv_size); } sort * mk_sort(unsigned bv_size); unsigned get_bv_size(sort const * s) const { diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp index e5b9ed930..f4a538abd 100644 --- a/src/ast/dl_decl_plugin.cpp +++ b/src/ast/dl_decl_plugin.cpp @@ -652,9 +652,9 @@ namespace datalog { // create a constant belonging to a given finite domain. - app* dl_decl_util::mk_numeral(uint64 value, sort* s) { + app* dl_decl_util::mk_numeral(uint64_t value, sort* s) { if (is_finite_sort(s)) { - uint64 sz = 0; + uint64_t sz = 0; if (try_get_size(s, sz) && sz <= value) { m.raise_exception("value is out of bounds"); } @@ -680,7 +680,7 @@ namespace datalog { return nullptr; } - bool dl_decl_util::is_numeral(const expr* e, uint64& v) const { + bool dl_decl_util::is_numeral(const expr* e, uint64_t& v) const { if (is_numeral(e)) { const app* c = to_app(e); SASSERT(c->get_decl()->get_num_parameters() == 2); @@ -693,7 +693,7 @@ namespace datalog { return false; } - bool dl_decl_util::is_numeral_ext(expr* e, uint64& v) const { + bool dl_decl_util::is_numeral_ext(expr* e, uint64_t& v) const { if (is_numeral(e, v)) { return true; } @@ -724,7 +724,7 @@ namespace datalog { return m.is_true(c) || m.is_false(c); } - sort* dl_decl_util::mk_sort(const symbol& name, uint64 domain_size) { + sort* dl_decl_util::mk_sort(const symbol& name, uint64_t domain_size) { if (domain_size == 0) { std::stringstream sstm; sstm << "Domain size of sort '" << name << "' may not be 0"; @@ -734,7 +734,7 @@ namespace datalog { return m.mk_sort(m_fid, DL_FINITE_SORT, 2, params); } - bool dl_decl_util::try_get_size(const sort * s, uint64& size) const { + bool dl_decl_util::try_get_size(const sort * s, uint64_t& size) const { sort_size sz = s->get_info()->get_num_elements(); if (sz.is_finite()) { size = sz.size(); diff --git a/src/ast/dl_decl_plugin.h b/src/ast/dl_decl_plugin.h index 03b9d1fd8..257404f70 100644 --- a/src/ast/dl_decl_plugin.h +++ b/src/ast/dl_decl_plugin.h @@ -122,7 +122,7 @@ namespace datalog { // Contract for func_decl: // parameters[0] - array sort // Contract for OP_DL_CONSTANT: - // parameters[0] - rational containing uint64 with constant value + // parameters[0] - rational containing uint64_t with constant value // parameters[1] - a DL_FINITE_SORT sort of the constant // Contract for others: // no parameters @@ -166,7 +166,7 @@ namespace datalog { dl_decl_util(ast_manager& m); // create a constant belonging to a given finite domain. // the options include the DL_FINITE_SORT, BV_SORT, and BOOL_SORT - app* mk_numeral(uint64 value, sort* s); + app* mk_numeral(uint64_t value, sort* s); app* mk_lt(expr* a, expr* b); @@ -176,19 +176,19 @@ namespace datalog { bool is_numeral(const expr* c) const { return is_app_of(c, m_fid, OP_DL_CONSTANT); } - bool is_numeral(const expr* e, uint64& v) const; + bool is_numeral(const expr* e, uint64_t& v) const; // // Utilities for extracting constants // from bit-vectors and finite domains. // - bool is_numeral_ext(expr* c, uint64& v) const; + bool is_numeral_ext(expr* c, uint64_t& v) const; bool is_numeral_ext(expr* c) const; - sort* mk_sort(const symbol& name, uint64 domain_size); + sort* mk_sort(const symbol& name, uint64_t domain_size); - bool try_get_size(const sort *, uint64& size) const; + bool try_get_size(const sort *, uint64_t& size) const; bool is_finite_sort(sort* s) const { return is_sort_of(s, m_fid, DL_FINITE_SORT); diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index c84af84d6..b7b0b6f08 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1071,7 +1071,7 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r SASSERT(m_mpz_manager.is_int64(max_exp_diff)); SASSERT(m_mpz_manager.get_uint64(max_exp_diff) <= UINT_MAX); - uint64 max_exp_diff_ui64 = m_mpz_manager.get_uint64(max_exp_diff); + uint64_t max_exp_diff_ui64 = m_mpz_manager.get_uint64(max_exp_diff); SASSERT(max_exp_diff_ui64 <= UINT_MAX); unsigned max_exp_diff_ui = (unsigned)max_exp_diff_ui64; m_mpz_manager.del(max_exp_diff); diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index e327df452..a0adb6398 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -680,8 +680,8 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_ if (v.is_neg()) mod(v, rational::power_of_two(sz), v); if (v.is_uint64()) { - uint64 u = v.get_uint64(); - uint64 e = shift_right(u, low) & (shift_left(1ull, sz) - 1ull); + uint64_t u = v.get_uint64(); + uint64_t e = shift_right(u, low) & (shift_left(1ull, sz) - 1ull); result = mk_numeral(numeral(e, numeral::ui64()), sz); return BR_DONE; } @@ -811,7 +811,7 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) { SASSERT(r1.is_uint64() && r2.is_uint64()); SASSERT(r2.get_uint64() < bv_size); - uint64 r = shift_left(r1.get_uint64(), r2.get_uint64()); + uint64_t r = shift_left(r1.get_uint64(), r2.get_uint64()); numeral rn(r, numeral::ui64()); rn = m_util.norm(rn, bv_size); result = mk_numeral(rn, bv_size); @@ -860,7 +860,7 @@ br_status bv_rewriter::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) { if (bv_size <= 64) { SASSERT(r1.is_uint64()); SASSERT(r2.is_uint64()); - uint64 r = shift_right(r1.get_uint64(), r2.get_uint64()); + uint64_t r = shift_right(r1.get_uint64(), r2.get_uint64()); numeral rn(r, numeral::ui64()); rn = m_util.norm(rn, bv_size); result = mk_numeral(rn, bv_size); @@ -902,11 +902,11 @@ br_status bv_rewriter::mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result) { bool is_num1 = is_numeral(arg1, r1, bv_size); if (bv_size <= 64 && is_num1 && is_num2) { - uint64 n1 = r1.get_uint64(); - uint64 n2_orig = r2.get_uint64(); - uint64 n2 = n2_orig % bv_size; + uint64_t n1 = r1.get_uint64(); + uint64_t n2_orig = r2.get_uint64(); + uint64_t n2 = n2_orig % bv_size; SASSERT(n2 < bv_size); - uint64 r = shift_right(n1, n2); + uint64_t r = shift_right(n1, n2); bool sign = (n1 & shift_left(1ull, bv_size - 1ull)) != 0; if (n2_orig > n2) { if (sign) { @@ -917,9 +917,9 @@ br_status bv_rewriter::mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result) { } } else if (sign) { - uint64 allone = shift_left(1ull, bv_size) - 1ull; - uint64 mask = ~(shift_left(1ull, bv_size - n2) - 1ull); - mask &= allone; + uint64_t allone = shift_left(1ull, bv_size) - 1ull; + uint64_t mask = ~(shift_left(1ull, bv_size - n2) - 1ull); + mask &= allone; r |= mask; } result = mk_numeral(numeral(r, numeral::ui64()), bv_size); @@ -2021,7 +2021,7 @@ br_status bv_rewriter::mk_bv_ext_rotate_left(expr * arg1, expr * arg2, expr_ref numeral r2; unsigned bv_size; if (is_numeral(arg2, r2, bv_size)) { - unsigned shift = static_cast((r2 % numeral(bv_size)).get_uint64() % static_cast(bv_size)); + unsigned shift = static_cast((r2 % numeral(bv_size)).get_uint64() % static_cast(bv_size)); return mk_bv_rotate_left(shift, arg1, result); } return BR_FAILED; @@ -2031,7 +2031,7 @@ br_status bv_rewriter::mk_bv_ext_rotate_right(expr * arg1, expr * arg2, expr_ref numeral r2; unsigned bv_size; if (is_numeral(arg2, r2, bv_size)) { - unsigned shift = static_cast((r2 % numeral(bv_size)).get_uint64() % static_cast(bv_size)); + unsigned shift = static_cast((r2 % numeral(bv_size)).get_uint64() % static_cast(bv_size)); return mk_bv_rotate_right(shift, arg1, result); } return BR_FAILED; diff --git a/src/ast/rewriter/dl_rewriter.cpp b/src/ast/rewriter/dl_rewriter.cpp index 74ea7814e..73944085b 100644 --- a/src/ast/rewriter/dl_rewriter.cpp +++ b/src/ast/rewriter/dl_rewriter.cpp @@ -22,7 +22,7 @@ Revision History: br_status dl_rewriter::mk_app_core( func_decl * f, unsigned num_args, expr* const* args, expr_ref& result) { ast_manager& m = result.get_manager(); - uint64 v1, v2; + uint64_t v1, v2; switch(f->get_decl_kind()) { case datalog::OP_DL_LT: if (m_util.is_numeral_ext(args[0], v1) && diff --git a/src/math/hilbert/hilbert_basis.h b/src/math/hilbert/hilbert_basis.h index a0350492a..54208d268 100644 --- a/src/math/hilbert/hilbert_basis.h +++ b/src/math/hilbert/hilbert_basis.h @@ -20,7 +20,7 @@ Revision History: Hilbert basis can be templatized based on traits that define numeral: - as rational, mpz, checked_int64 + as rational, mpz, checked_int64 (checked or unchecked). --*/ diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index a58f26597..35a95ce82 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -5479,7 +5479,7 @@ namespace polynomial { } p_prime = derivative(p, x); resultant(p, p_prime, x, r); - bool sign = (static_cast(m) * static_cast(m-1))%4 != 0; + bool sign = (static_cast(m) * static_cast(m-1))%4 != 0; TRACE("resultant", tout << "discriminant sign: " << sign << "\n";); scoped_numeral lc(m_manager); if (const_coeff(p, x, m, lc)) { @@ -6963,7 +6963,7 @@ namespace polynomial { return m_imp->m().set_zp(p); } - void manager::set_zp(uint64 p) { + void manager::set_zp(uint64_t p) { return m_imp->m().set_zp(p); } diff --git a/src/math/polynomial/polynomial.h b/src/math/polynomial/polynomial.h index 43774f0ac..374a51084 100644 --- a/src/math/polynomial/polynomial.h +++ b/src/math/polynomial/polynomial.h @@ -218,7 +218,7 @@ namespace polynomial { \brief Set manager as Z_p[X1, ..., Xn] */ void set_zp(numeral const & p); - void set_zp(uint64 p); + void set_zp(uint64_t p); /** \brief Abstract event handler. @@ -1043,7 +1043,7 @@ namespace polynomial { scoped_numeral m_p; public: scoped_set_zp(manager & _m, numeral const & p):m(_m), m_modular(m.modular()), m_p(m.m()) { m_p = m.p(); m.set_zp(p); } - scoped_set_zp(manager & _m, uint64 p):m(_m), m_modular(m.modular()), m_p(m.m()) { m_p = m.p(); m.set_zp(p); } + scoped_set_zp(manager & _m, uint64_t p):m(_m), m_modular(m.modular()), m_p(m.m()) { m_p = m.p(); m.set_zp(p); } ~scoped_set_zp() { if (m_modular) m.set_zp(m_p); else m.set_z(); } }; }; diff --git a/src/math/polynomial/upolynomial.h b/src/math/polynomial/upolynomial.h index 6bd3e4a27..439b4be9f 100644 --- a/src/math/polynomial/upolynomial.h +++ b/src/math/polynomial/upolynomial.h @@ -153,7 +153,7 @@ namespace upolynomial { \brief Set manager as Z_p[X] */ void set_zp(numeral const & p) { m().set_zp(p); } - void set_zp(uint64 p) { m().set_zp(p); } + void set_zp(uint64_t p) { m().set_zp(p); } void checkpoint(); @@ -486,7 +486,7 @@ namespace upolynomial { core_manager::scoped_numeral m_p; public: scoped_set_zp(core_manager & _m, numeral const & p):m(_m), m_modular(m.modular()), m_p(m.m()) { m_p = m.p(); m.set_zp(p); } - scoped_set_zp(core_manager & _m, uint64 p):m(_m), m_modular(m.modular()), m_p(m.m()) { m_p = m.p(); m.set_zp(p); } + scoped_set_zp(core_manager & _m, uint64_t p):m(_m), m_modular(m.modular()), m_p(m.m()) { m_p = m.p(); m.set_zp(p); } ~scoped_set_zp() { if (m_modular) m.set_zp(m_p); else m.set_z(); } }; diff --git a/src/math/polynomial/upolynomial_factorization.cpp b/src/math/polynomial/upolynomial_factorization.cpp index a1f6e6ec1..5d9d3f1f1 100644 --- a/src/math/polynomial/upolynomial_factorization.cpp +++ b/src/math/polynomial/upolynomial_factorization.cpp @@ -38,9 +38,9 @@ unsigned get_p_from_manager(zp_numeral_manager const & zp_nm) { if (!nm.is_uint64(p)) { throw upolynomial_exception("The prime number attempted in factorization is too big!"); } - uint64 p_uint64 = nm.get_uint64(p); + uint64_t p_uint64 = nm.get_uint64(p); unsigned p_uint = static_cast(p_uint64); - if (((uint64)p_uint) != p_uint64) { + if (((uint64_t)p_uint) != p_uint64) { throw upolynomial_exception("The prime number attempted in factorization is too big!"); } return p_uint; @@ -1075,7 +1075,7 @@ bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs, while (trials < params.m_p_trials) { upm.checkpoint(); // construct prime to check - uint64 next_prime = prime_it.next(); + uint64_t next_prime = prime_it.next(); if (next_prime > params.m_max_p) { fs.push_back(f_pp, k); return false; diff --git a/src/math/subpaving/subpaving.cpp b/src/math/subpaving/subpaving.cpp index 1f32a6189..16a9a9a9e 100644 --- a/src/math/subpaving/subpaving.cpp +++ b/src/math/subpaving/subpaving.cpp @@ -150,12 +150,12 @@ namespace subpaving { void int2hwf(mpz const & a, hwf & o) { if (!m_qm.is_int64(a)) throw subpaving::exception(); - int64 val = m_qm.get_int64(a); + int64_t val = m_qm.get_int64(a); double dval = static_cast(val); m_ctx.nm().set(o, dval); double _dval = m_ctx.nm().m().to_double(o); // TODO check the following test - if (static_cast(_dval) != val) + if (static_cast(_dval) != val) throw subpaving::exception(); } diff --git a/src/math/subpaving/subpaving_t.h b/src/math/subpaving/subpaving_t.h index 360b2a32f..02c538828 100644 --- a/src/math/subpaving/subpaving_t.h +++ b/src/math/subpaving/subpaving_t.h @@ -73,17 +73,17 @@ public: // TODO: add SIN, COS, TAN, ... }; protected: - kind m_kind; - uint64 m_timestamp; + kind m_kind; + uint64_t m_timestamp; public: constraint(kind k):m_kind(k), m_timestamp(0) {} kind get_kind() const { return m_kind; } // Return the timestamp of the last propagation visit - uint64 timestamp() const { return m_timestamp; } + uint64_t timestamp() const { return m_timestamp; } // Reset propagation visit time - void set_visited(uint64 ts) { m_timestamp = ts; } + void set_visited(uint64_t ts) { m_timestamp = ts; } }; /** @@ -149,17 +149,17 @@ public: unsigned m_lower:1; unsigned m_open:1; unsigned m_mark:1; - uint64 m_timestamp; + uint64_t m_timestamp; bound * m_prev; justification m_jst; - void set_timestamp(uint64 ts) { m_timestamp = ts; } + void set_timestamp(uint64_t ts) { m_timestamp = ts; } public: var x() const { return static_cast(m_x); } numeral const & value() const { return m_val; } numeral & value() { return m_val; } bool is_lower() const { return m_lower; } bool is_open() const { return m_open; } - uint64 timestamp() const { return m_timestamp; } + uint64_t timestamp() const { return m_timestamp; } bound * prev() const { return m_prev; } justification jst() const { return m_jst; } void display(std::ostream & out, numeral_manager & nm, display_var_proc const & proc = display_var_proc()); @@ -486,7 +486,7 @@ private: id_gen m_node_id_gen; - uint64 m_timestamp; + uint64_t m_timestamp; node * m_root; // m_leaf_head is the head of a doubly linked list of leaf nodes to be processed. node * m_leaf_head; diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 521cf0dc9..54c07da28 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -45,7 +45,7 @@ namespace datalog { protected: sort_ref m_sort; bool m_limited_size; - uint64 m_size; + uint64_t m_size; sort_domain(sort_kind k, context & ctx, sort * s) : m_kind(k), m_sort(s, ctx.get_manager()) { @@ -103,15 +103,15 @@ namespace datalog { }; class context::uint64_sort_domain : public sort_domain { - typedef map > el2num; - typedef svector num2el; + typedef map > el2num; + typedef svector num2el; el2num m_el_numbers; num2el m_el_names; public: uint64_sort_domain(context & ctx, sort * s) : sort_domain(SK_UINT64, ctx, s) {} - finite_element get_number(uint64 el) { + finite_element get_number(uint64_t el) { //we number symbols starting from zero, so table->size() is equal to the //index of the symbol to be added next @@ -368,14 +368,14 @@ namespace datalog { return dom.get_number(sym); } - context::finite_element context::get_constant_number(relation_sort srt, uint64 el) { + context::finite_element context::get_constant_number(relation_sort srt, uint64_t el) { sort_domain & dom0 = get_sort_domain(srt); SASSERT(dom0.get_kind()==SK_UINT64); uint64_sort_domain & dom = static_cast(dom0); return dom.get_number(el); } - void context::print_constant_name(relation_sort srt, uint64 num, std::ostream & out) + void context::print_constant_name(relation_sort srt, uint64_t num, std::ostream & out) { if (has_sort_domain(srt)) { SASSERT(num<=UINT_MAX); @@ -386,7 +386,7 @@ namespace datalog { } } - bool context::try_get_sort_constant_count(relation_sort srt, uint64 & constant_count) { + bool context::try_get_sort_constant_count(relation_sort srt, uint64_t & constant_count) { if (!has_sort_domain(srt)) { return false; } @@ -394,18 +394,18 @@ namespace datalog { return true; } - uint64 context::get_sort_size_estimate(relation_sort srt) { + uint64_t context::get_sort_size_estimate(relation_sort srt) { if (get_decl_util().is_rule_sort(srt)) { return 1; } - uint64 res; + uint64_t res; if (!try_get_sort_constant_count(srt, res)) { const sort_size & sz = srt->get_num_elements(); if (sz.is_finite()) { res = sz.size(); } else { - res = std::numeric_limits::max(); + res = std::numeric_limits::max(); } } return res; diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index f37826feb..865c746db 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -61,7 +61,7 @@ namespace datalog { class relation_manager; typedef sort * relation_sort; - typedef uint64 table_element; + typedef uint64_t table_element; typedef svector table_fact; typedef app * relation_element; @@ -351,16 +351,16 @@ namespace datalog { /** \brief Return number of a symbol in a DK_UINT64 kind sort (\see register_sort() ) */ - finite_element get_constant_number(relation_sort srt, uint64 el); + finite_element get_constant_number(relation_sort srt, uint64_t el); /** \brief Output name of constant with number \c num in sort \c sort. */ - void print_constant_name(relation_sort sort, uint64 num, std::ostream & out); + void print_constant_name(relation_sort sort, uint64_t num, std::ostream & out); - bool try_get_sort_constant_count(relation_sort srt, uint64 & constant_count); + bool try_get_sort_constant_count(relation_sort srt, uint64_t & constant_count); - uint64 get_sort_size_estimate(relation_sort srt); + uint64_t get_sort_size_estimate(relation_sort srt); /** \brief Assign names of variables used in the declaration of a predicate. diff --git a/src/muz/base/dl_costs.cpp b/src/muz/base/dl_costs.cpp index d429af803..70688cd59 100644 --- a/src/muz/base/dl_costs.cpp +++ b/src/muz/base/dl_costs.cpp @@ -141,7 +141,7 @@ namespace datalog { } void cost_recorder::start(accounted_object * obj) { - uint64 curr_time = static_cast(m_stopwatch->get_current_seconds()*1000); + uint64_t curr_time = static_cast(m_stopwatch->get_current_seconds()*1000); if(m_obj) { costs::time_type time_delta = static_cast(curr_time-m_last_time); costs & c = m_obj->get_current_costs(); diff --git a/src/muz/base/dl_costs.h b/src/muz/base/dl_costs.h index 59d4fd8c1..6a5b5e5d6 100644 --- a/src/muz/base/dl_costs.h +++ b/src/muz/base/dl_costs.h @@ -95,7 +95,7 @@ namespace datalog { stopwatch * m_stopwatch; bool m_running; - uint64 m_last_time; + uint64_t m_last_time; public: cost_recorder(); ~cost_recorder(); diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp index c2622cec4..7cc9d4b03 100644 --- a/src/muz/base/dl_util.cpp +++ b/src/muz/base/dl_util.cpp @@ -165,7 +165,7 @@ namespace datalog { } expr * arg = f->get_arg(i); - uint64 sym_num; + uint64_t sym_num; SASSERT(is_app(arg)); VERIFY( ctx.get_decl_util().is_numeral_ext(to_app(arg), sym_num) ); relation_sort sort = pred_decl->get_domain(i); @@ -621,7 +621,7 @@ namespace datalog { return name.substr(ofs, count); } - bool string_to_uint64(const char * s, uint64 & res) { + bool string_to_uint64(const char * s, uint64_t & res) { #if _WINDOWS int converted = sscanf_s(s, "%I64u", &res); #else @@ -634,9 +634,9 @@ namespace datalog { return true; } - bool read_uint64(const char * & s, uint64 & res) { - static const uint64 max_but_one_digit = ULLONG_MAX/10; - static const uint64 max_but_one_digit_safe = (ULLONG_MAX-9)/10; + bool read_uint64(const char * & s, uint64_t & res) { + static const uint64_t max_but_one_digit = ULLONG_MAX/10; + static const uint64_t max_but_one_digit_safe = (ULLONG_MAX-9)/10; if(*s<'0' || *s>'9') { return false; @@ -664,7 +664,7 @@ namespace datalog { return true; } - std::string to_string(uint64 num) { + std::string to_string(uint64_t num) { std::stringstream stm; stm< uint64_vector; - typedef hashtable > uint64_set; - typedef map > num2sym; + typedef svector uint64_vector; + typedef hashtable > uint64_set; + typedef map > num2sym; typedef map sym2nums; num2sym m_number_names; @@ -1261,7 +1261,7 @@ private: return true; } - bool inp_num_to_element(sort * s, uint64 num, table_element & res) { + bool inp_num_to_element(sort * s, uint64_t num, table_element & res) { if(s==m_bool_sort.get() || s==m_short_sort.get()) { res = mk_table_const(num, s); return true; @@ -1332,7 +1332,7 @@ private: if(*ptr==0) { break; } - uint64 num; + uint64_t num; if(!read_uint64(ptr, num)) { throw default_exception(default_exception::fmt(), "number expected on line %d in file %s", m_current_line, m_current_file.c_str()); @@ -1389,7 +1389,7 @@ private: bool fact_fail = false; fact.reset(); for(unsigned i=0;im_key; uint64_set & sort_content = *sit->m_value; //the +1 is for a zero element which happens to appear in the problem files - uint64 domain_size = sort_content.size()+1; + uint64_t domain_size = sort_content.size()+1; // sort * s; if(!m_use_map_names) { /* s = */ register_finite_sort(sort_name, domain_size, context::SK_UINT64); @@ -1428,7 +1428,7 @@ private: uint64_set::iterator cit = sort_content.begin(); uint64_set::iterator cend = sort_content.end(); for(; cit!=cend; ++cit) { - uint64 const_num = *cit; + uint64_t const_num = *cit; inp_num_to_element(s, const_num); } */ @@ -1443,7 +1443,7 @@ private: *ptr=0; } - bool parse_map_line(char * full_line, uint64 & num, symbol & name) { + bool parse_map_line(char * full_line, uint64_t & num, symbol & name) { cut_off_comment(full_line); if(full_line[0]==0) { return false; @@ -1515,7 +1515,7 @@ private: m_current_line++; char * full_line = rdr.get_line(); - uint64 num; + uint64_t num; symbol el_name; if(!parse_map_line(full_line, num, el_name)) { diff --git a/src/muz/rel/dl_base.cpp b/src/muz/rel/dl_base.cpp index 20418e3bb..5dd21a9f0 100644 --- a/src/muz/rel/dl_base.cpp +++ b/src/muz/rel/dl_base.cpp @@ -384,7 +384,7 @@ namespace datalog { VERIFY(sig.first_functional() == 1); - uint64 upper_bound = get_signature()[0]; + uint64_t upper_bound = get_signature()[0]; bool empty_table = empty(); if (upper_bound > (1 << 18)) { diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index dfdcb304d..4d202f2a2 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -832,7 +832,7 @@ namespace datalog { class table_plugin; class table_base; - typedef uint64 table_sort; + typedef uint64_t table_sort; typedef svector table_signature_base0; typedef uint64_hash table_sort_hash; diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp index deb289277..c9fc4f173 100644 --- a/src/muz/rel/dl_relation_manager.cpp +++ b/src/muz/rel/dl_relation_manager.cpp @@ -448,7 +448,7 @@ namespace datalog { } std::string relation_manager::to_nice_string(const relation_element & el) const { - uint64 val; + uint64_t val; std::stringstream stm; if(get_context().get_decl_util().is_numeral_ext(el, val)) { stm << val; @@ -461,7 +461,7 @@ namespace datalog { std::string relation_manager::to_nice_string(const relation_sort & s, const relation_element & el) const { std::stringstream stm; - uint64 val; + uint64_t val; if(get_context().get_decl_util().is_numeral_ext(el, val)) { get_context().print_constant_name(s, val, stm); } @@ -1339,9 +1339,9 @@ namespace datalog { class relation_manager::default_table_filter_not_equal_fn : public table_mutator_fn, auxiliary_table_filter_fn { unsigned m_column; - uint64 m_value; + uint64_t m_value; public: - default_table_filter_not_equal_fn(context & ctx, unsigned column, uint64 value) + default_table_filter_not_equal_fn(context & ctx, unsigned column, uint64_t value) : m_column(column), m_value(value) { } @@ -1372,7 +1372,7 @@ namespace datalog { return nullptr; } dl_decl_util decl_util(m); - uint64 value = 0; + uint64_t value = 0; if (!decl_util.is_numeral_ext(y, value)) { return nullptr; } diff --git a/src/muz/rel/dl_sparse_table.cpp b/src/muz/rel/dl_sparse_table.cpp index 779172b0d..bb48211c7 100644 --- a/src/muz/rel/dl_sparse_table.cpp +++ b/src/muz/rel/dl_sparse_table.cpp @@ -93,7 +93,7 @@ namespace datalog { // // ----------------------------------- - unsigned get_domain_length(uint64 dom_size) { + unsigned get_domain_length(uint64_t dom_size) { SASSERT(dom_size>0); unsigned length = 0; @@ -128,7 +128,7 @@ namespace datalog { unsigned sig_sz = sig.size(); unsigned first_functional = sig_sz-m_functional_col_cnt; for (unsigned i=0; i0); SASSERT(length<=64); diff --git a/src/muz/rel/dl_sparse_table.h b/src/muz/rel/dl_sparse_table.h index a9f3b31a4..fbbbd12f8 100644 --- a/src/muz/rel/dl_sparse_table.h +++ b/src/muz/rel/dl_sparse_table.h @@ -153,7 +153,7 @@ namespace datalog { variable. Otherwise \c m_reserve==NO_RESERVE. The size of m_data is actually 8 bytes larger than stated in m_data_size, so that we may - deref an uint64 pointer at the end of the array. + deref an uint64_t pointer at the end of the array. */ storage m_data; storage_indexer m_data_indexer; @@ -290,10 +290,10 @@ namespace datalog { //the following two operations allow breaking of the object invariant! void resize_data(size_t sz) { m_data_size = sz; - if (sz + sizeof(uint64) < sz) { + if (sz + sizeof(uint64_t) < sz) { throw default_exception("overflow resizing data section for sparse table"); } - m_data.resize(sz + sizeof(uint64)); + m_data.resize(sz + sizeof(uint64_t)); } bool insert_offset(store_offset ofs) { @@ -321,8 +321,8 @@ namespace datalog { class column_info { unsigned m_big_offset; unsigned m_small_offset; - uint64 m_mask; - uint64 m_write_mask; + uint64_t m_mask; + uint64_t m_write_mask; public: unsigned m_offset; //!< in bits unsigned m_length; //!< in bits @@ -330,7 +330,7 @@ namespace datalog { column_info(unsigned offset, unsigned length) \ : m_big_offset(offset/8), m_small_offset(offset%8), - m_mask( length==64 ? ULLONG_MAX : (static_cast(1)<(1)<(rec+m_big_offset); - uint64 res = *ptr; + const uint64_t * ptr = reinterpret_cast(rec+m_big_offset); + uint64_t res = *ptr; res>>=m_small_offset; res&=m_mask; return res; } void set(char * rec, table_element val) const { SASSERT( (val&~m_mask)==0 ); //the value fits into the column - uint64 * ptr = reinterpret_cast(rec+m_big_offset); + uint64_t * ptr = reinterpret_cast(rec+m_big_offset); *ptr&=m_write_mask; *ptr|=val<restart_time); remaining_time_limit -= restart_time; } - uint64 new_restart_time = static_cast(restart_time)*m_context.initial_restart_timeout(); + uint64_t new_restart_time = static_cast(restart_time)*m_context.initial_restart_timeout(); if (new_restart_time > UINT_MAX) { restart_time = UINT_MAX; } diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp index 69cc4819a..b96f32114 100644 --- a/src/muz/rel/tbv.cpp +++ b/src/muz/rel/tbv.cpp @@ -72,7 +72,7 @@ tbv* tbv_manager::allocate(tbv const& bv) { copy(*r, bv); return r; } -tbv* tbv_manager::allocate(uint64 val) { +tbv* tbv_manager::allocate(uint64_t val) { tbv* v = allocate0(); for (unsigned bit = std::min(64u, num_tbits()); bit-- > 0;) { if (val & (1ULL << bit)) { @@ -84,7 +84,7 @@ tbv* tbv_manager::allocate(uint64 val) { return v; } -tbv* tbv_manager::allocate(uint64 val, unsigned hi, unsigned lo) { +tbv* tbv_manager::allocate(uint64_t val, unsigned hi, unsigned lo) { tbv* v = allocateX(); SASSERT(64 >= num_tbits() && num_tbits() > hi && hi >= lo); set(*v, val, hi, lo); @@ -134,7 +134,7 @@ void tbv_manager::set(tbv& dst, unsigned index, tbit value) { } -void tbv_manager::set(tbv& dst, uint64 val, unsigned hi, unsigned lo) { +void tbv_manager::set(tbv& dst, uint64_t val, unsigned hi, unsigned lo) { SASSERT(lo <= hi && hi < num_tbits()); for (unsigned i = 0; i < hi - lo + 1; ++i) { set(dst, lo + i, (val & (1ULL << i))?BIT_1:BIT_0); diff --git a/src/muz/rel/tbv.h b/src/muz/rel/tbv.h index 22c25a5e9..346208a3f 100644 --- a/src/muz/rel/tbv.h +++ b/src/muz/rel/tbv.h @@ -51,9 +51,9 @@ public: tbv* allocate0(); tbv* allocateX(); tbv* allocate(tbv const& bv); - tbv* allocate(uint64 n); + tbv* allocate(uint64_t n); tbv* allocate(rational const& r); - tbv* allocate(uint64 n, unsigned hi, unsigned lo); + tbv* allocate(uint64_t n, unsigned hi, unsigned lo); tbv* allocate(tbv const& bv, unsigned const* permutation); tbv* allocate(char const* bv); @@ -80,7 +80,7 @@ public: std::ostream& display(std::ostream& out, tbv const& b, unsigned hi, unsigned lo) const; tbv* project(bit_vector const& to_delete, tbv const& src); bool is_well_formed(tbv const& b) const; // - does not contain BIT_z; - void set(tbv& dst, uint64 n, unsigned hi, unsigned lo); + void set(tbv& dst, uint64_t n, unsigned hi, unsigned lo); void set(tbv& dst, rational const& r, unsigned hi, unsigned lo); void set(tbv& dst, tbv const& other, unsigned hi, unsigned lo); void set(tbv& dst, unsigned index, tbit value); diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index ff23a5e53..2e9ab693c 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -261,7 +261,7 @@ namespace datalog { num_bits = 1; return true; } - uint64 n, sz; + uint64_t n, sz; ast_manager& m = get_ast_manager(); if (dl.is_numeral(e, n) && dl.try_get_size(m.get_sort(e), sz)) { num_bits = 0; @@ -277,7 +277,7 @@ namespace datalog { return bv.get_bv_size(s); if (m.is_bool(s)) return 1; - uint64 sz; + uint64_t sz; if (dl.try_get_size(s, sz)) { while (sz > 0) ++num_bits, sz /= 2; return num_bits; diff --git a/src/qe/qe_dl_plugin.cpp b/src/qe/qe_dl_plugin.cpp index 8d688d80c..6e411511d 100644 --- a/src/qe/qe_dl_plugin.cpp +++ b/src/qe/qe_dl_plugin.cpp @@ -70,7 +70,7 @@ namespace qe { return false; } eq_atoms& eqs = get_eqs(x.x(), fml); - uint64 domain_size; + uint64_t domain_size; if (is_small_domain(x, eqs, domain_size)) { num_branches = rational(domain_size, rational::ui64()); } @@ -84,7 +84,7 @@ namespace qe { SASSERT(v.is_unsigned()); eq_atoms& eqs = get_eqs(x.x(), fml); unsigned uv = v.get_unsigned(); - uint64 domain_size; + uint64_t domain_size; if (is_small_domain(x, eqs, domain_size)) { SASSERT(v < rational(domain_size, rational::ui64())); assign_small_domain(x, eqs, uv); @@ -98,7 +98,7 @@ namespace qe { SASSERT(v.is_unsigned()); eq_atoms& eqs = get_eqs(x.x(), fml); unsigned uv = v.get_unsigned(); - uint64 domain_size; + uint64_t domain_size; if (is_small_domain(x, eqs, domain_size)) { SASSERT(uv < domain_size); subst_small_domain(x, eqs, uv, fml); @@ -115,7 +115,7 @@ namespace qe { private: - bool is_small_domain(contains_app& x, eq_atoms& eqs, uint64& domain_size) { + bool is_small_domain(contains_app& x, eq_atoms& eqs, uint64_t& domain_size) { VERIFY(m_util.try_get_size(m.get_sort(x.x()), domain_size)); return domain_size < eqs.num_eqs() + eqs.num_neqs(); } diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp index 427c1015f..9cc13b897 100644 --- a/src/shell/datalog_frontend.cpp +++ b/src/shell/datalog_frontend.cpp @@ -212,7 +212,7 @@ unsigned read_datalog(char const * file) { if (early_termination) { IF_VERBOSE(1, verbose_stream() << "restarting saturation\n";); - uint64 new_timeout = static_cast(timeout)*ctx.initial_restart_timeout(); + uint64_t new_timeout = static_cast(timeout)*ctx.initial_restart_timeout(); if(new_timeout>UINT_MAX) { timeout=UINT_MAX; } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index e20eae0bd..608b7c63e 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3951,7 +3951,7 @@ namespace smt { #if 0 { static unsigned counter = 0; - static uint64 total = 0; + static uint64_t total = 0; static unsigned max = 0; counter++; total += num_lits; diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp index 285c03946..824bd1d9e 100644 --- a/src/smt/theory_dl.cpp +++ b/src/smt/theory_dl.cpp @@ -182,7 +182,7 @@ namespace smt { if (n->get_decl() != v) { expr* rep = m().mk_app(r, n); - uint64 vl; + uint64_t vl; if (u().is_numeral_ext(n, vl)) { assert_cnstr(m().mk_eq(rep, mk_bv_constant(vl, s))); } @@ -237,12 +237,12 @@ namespace smt { return true; } - app* mk_bv_constant(uint64 val, sort* s) { + app* mk_bv_constant(uint64_t val, sort* s) { return b().mk_numeral(rational(val, rational::ui64()), 64); } app* max_value(sort* s) { - uint64 sz; + uint64_t sz; VERIFY(u().try_get_size(s, sz)); SASSERT(sz > 0); return mk_bv_constant(sz-1, s); diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index 2cd6a5a1b..2704d92ff 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -25,7 +25,7 @@ Author: #include "ast/ast_pp.h" #include -static uint64 uMaxInt(unsigned sz) { +static uint64_t uMaxInt(unsigned sz) { SASSERT(sz <= 64); return ULLONG_MAX >> (64u - sz); } @@ -35,12 +35,12 @@ namespace { struct interval { // l < h: [l, h] // l > h: [0, h] U [l, UMAX_INT] - uint64 l, h; + uint64_t l, h; unsigned sz; bool tight; interval() {} - interval(uint64 l, uint64 h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) { + interval(uint64_t l, uint64_t h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) { // canonicalize full set if (is_wrapped() && l == h + 1) { this->l = 0; @@ -183,7 +183,7 @@ namespace { svector m_expr_vars; svector m_bound_exprs; - bool is_number(expr *e, uint64& n, unsigned& sz) const { + bool is_number(expr *e, uint64_t& n, unsigned& sz) const { rational r; if (m_bv.is_numeral(e, r, sz) && sz <= 64) { n = r.get_uint64(); @@ -193,7 +193,7 @@ namespace { } bool is_bound(expr *e, expr*& v, interval& b) const { - uint64 n; + uint64_t n; expr *lhs = nullptr, *rhs = nullptr; unsigned sz; @@ -550,7 +550,7 @@ namespace { svector m_expr_vars; svector m_bound_exprs; - bool is_number(expr *e, uint64& n, unsigned& sz) const { + bool is_number(expr *e, uint64_t& n, unsigned& sz) const { rational r; if (m_bv.is_numeral(e, r, sz) && sz <= 64) { n = r.get_uint64(); @@ -560,7 +560,7 @@ namespace { } bool is_bound(expr *e, expr*& v, interval& b) const { - uint64 n; + uint64_t n; expr *lhs = nullptr, *rhs = nullptr; unsigned sz = 0; diff --git a/src/test/algebraic.cpp b/src/test/algebraic.cpp index b893b5ee2..38948c0d7 100644 --- a/src/test/algebraic.cpp +++ b/src/test/algebraic.cpp @@ -278,7 +278,7 @@ static void tst_select_small(mpbq_manager & m, scoped_mpbq const & l, scoped_mpb std::cout << "choice: " << r << " as decimal: "; m.display_decimal(std::cout, r); std::cout << std::endl; } -static void tst_select_small(mpbq_manager & m, int64 n1, unsigned k1, int64 n2, unsigned k2, bool expected) { +static void tst_select_small(mpbq_manager & m, int64_t n1, unsigned k1, int64_t n2, unsigned k2, bool expected) { scoped_mpbq l(m); scoped_mpbq u(m); m.set(l, n1, k1); diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp index c5765bd6b..3dc99e33c 100644 --- a/src/test/dl_query.cpp +++ b/src/test/dl_query.cpp @@ -95,12 +95,12 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params, f_b.reset(); f_q.reset(); for(unsigned col=0; colget_domain(0); - uint64 var_sz; + uint64_t var_sz; TRUSTME( ctx.try_get_sort_constant_count(var_sort, var_sz) ); for(unsigned attempt=0; attempt(100)); - m.set(b, static_cast(-100)); + m.set(a, static_cast(100)); + m.set(b, static_cast(-100)); std::cout << "[test2], a: " << a << ", b: " << b << "\n"; } @@ -75,7 +75,7 @@ static void tst4() { static void tst5() { mpff_manager m; scoped_mpff a(m), b(m); - m.set(a, static_cast(1) << 63); + m.set(a, static_cast(1) << 63); m.display_raw(std::cout, a); std::cout << "\n"; ENSURE(m.is_zero(b)); ENSURE(m.lt(b, a)); @@ -117,7 +117,7 @@ static void tst7() { #define MK_BIN_OP(OP) \ -static void tst_ ## OP ## _core(int64 n1, uint64 d1, int64 n2, uint64 d2, unsigned precision = 2, unsigned exp = 0) { \ +static void tst_ ## OP ## _core(int64_t n1, uint64_t d1, int64_t n2, uint64_t d2, unsigned precision = 2, unsigned exp = 0) { \ TRACE("mpff_bug", tout << n1 << "/" << d1 << ", " << n2 << "/" << d2 << "\n";); \ unsynch_mpq_manager qm; \ scoped_mpq qa(qm), qb(qm), qc(qm), qt(qm); \ @@ -207,7 +207,7 @@ static void tst_set64(unsigned N, unsigned prec) { mpff_manager fm(prec); scoped_mpff a(fm); - fm.set(a, static_cast(INT64_MAX)); + fm.set(a, static_cast(INT64_MAX)); ENSURE(fm.is_int64(a)); ENSURE(fm.is_uint64(a)); fm.inc(a); @@ -221,7 +221,7 @@ static void tst_set64(unsigned N, unsigned prec) { ENSURE(fm.is_int64(a)); ENSURE(fm.is_uint64(a)); - fm.set(a, static_cast(INT64_MIN)); + fm.set(a, static_cast(INT64_MIN)); ENSURE(fm.is_int64(a)); ENSURE(!fm.is_uint64(a)); fm.dec(a); @@ -235,7 +235,7 @@ static void tst_set64(unsigned N, unsigned prec) { ENSURE(fm.is_int64(a)); ENSURE(!fm.is_uint64(a)); - fm.set(a, static_cast(UINT64_MAX)); + fm.set(a, static_cast(UINT64_MAX)); ENSURE(fm.is_uint64(a)); ENSURE(!fm.is_int64(a)); fm.inc(a); @@ -250,23 +250,23 @@ static void tst_set64(unsigned N, unsigned prec) { for (unsigned i = 0; i < N; i++) { { - uint64 v = (static_cast(rand()) << 32) + static_cast(rand()); + uint64_t v = (static_cast(rand()) << 32) + static_cast(rand()); fm.set(a, v); ENSURE(fm.is_uint64(a)); - v = (static_cast(rand() % 3) << 32) + static_cast(rand()); + v = (static_cast(rand() % 3) << 32) + static_cast(rand()); fm.set(a, v); ENSURE(fm.is_uint64(a)); } { - int64 v = (static_cast(rand() % INT_MAX) << 32) + static_cast(rand()); + int64_t v = (static_cast(rand() % INT_MAX) << 32) + static_cast(rand()); if (rand()%2 == 0) v = -v; fm.set(a, v); ENSURE(fm.is_int64(a)); - v = (static_cast(rand() % 3) << 32) + static_cast(rand()); + v = (static_cast(rand() % 3) << 32) + static_cast(rand()); if (rand()%2 == 0) v = -v; fm.set(a, v); @@ -336,7 +336,7 @@ static void tst_power(unsigned prec = 2) { m.set(a, UINT_MAX); m.inc(a); ENSURE(m.is_power_of_two(a, k) && k == 32); - ENSURE(m.get_uint64(a) == static_cast(UINT_MAX) + 1); + ENSURE(m.get_uint64(a) == static_cast(UINT_MAX) + 1); m.power(a, 2, a); ENSURE(m.is_power_of_two(a, k) && k == 64); m.power(a, 4, a); @@ -538,7 +538,7 @@ static void tst_add_corner(unsigned prec) { } #endif -static void tst_decimal(int64 n, uint64 d, bool to_plus_inf, unsigned prec, char const * expected, unsigned decimal_places = UINT_MAX) { +static void tst_decimal(int64_t n, uint64_t d, bool to_plus_inf, unsigned prec, char const * expected, unsigned decimal_places = UINT_MAX) { mpff_manager m(prec); scoped_mpff a(m); m.set_rounding(to_plus_inf); @@ -567,7 +567,7 @@ static void tst_decimal() { tst_decimal(-32, 5, true, 2, "-6.39999999999999999965305530480463858111761510372161865234375"); } -static void tst_prev_power_2(int64 n, uint64 d, unsigned expected) { +static void tst_prev_power_2(int64_t n, uint64_t d, unsigned expected) { mpff_manager m; scoped_mpff a(m); m.set(a, n, d); @@ -598,7 +598,7 @@ static void tst_div(unsigned prec) { scoped_mpff a(m), b(m), c(m); m.round_to_plus_inf(); m.set(a, 1); - m.set(b, static_cast(UINT64_MAX)); + m.set(b, static_cast(UINT64_MAX)); m.div(a, b, c); m.display_raw(std::cout, a); std::cout << "\n"; m.display_raw(std::cout, b); std::cout << "\n"; diff --git a/src/test/mpfx.cpp b/src/test/mpfx.cpp index f9dc123f5..f5cf7e2fb 100644 --- a/src/test/mpfx.cpp +++ b/src/test/mpfx.cpp @@ -35,7 +35,7 @@ static void tst1() { m.display_decimal(std::cout, a); std::cout << "\n"; } -static void tst_prev_power_2(int64 n, uint64 d, unsigned expected) { +static void tst_prev_power_2(int64_t n, uint64_t d, unsigned expected) { mpfx_manager m; scoped_mpfx a(m); m.set(a, n, d); diff --git a/src/test/mpq.cpp b/src/test/mpq.cpp index 7b60d9dcb..6294a97f7 100644 --- a/src/test/mpq.cpp +++ b/src/test/mpq.cpp @@ -133,7 +133,7 @@ static void set_str_bug() { ENSURE(a == b); } -static void tst_prev_power_2(int64 n, uint64 d, unsigned expected) { +static void tst_prev_power_2(int64_t n, uint64_t d, unsigned expected) { unsynch_mpq_manager m; scoped_mpq a(m); m.set(a, n, d); diff --git a/src/test/mpz.cpp b/src/test/mpz.cpp index 7926388df..cf7f3d8e6 100644 --- a/src/test/mpz.cpp +++ b/src/test/mpz.cpp @@ -50,7 +50,7 @@ static void tst1() { static void tst2() { synch_mpz_manager m; mpz v1, v2, v3; - m.set(v1, static_cast(UINT_MAX)); + m.set(v1, static_cast(UINT_MAX)); m.add(v1, m.mk_z(1), v2); m.mul(v2, v2, v3); std::cout << "v2:\n" << m.to_string(v2) << "\n"; @@ -63,7 +63,7 @@ static void tst2() { static void tst2b() { synch_mpz_manager m; mpz v1, v2, v3; - m.set(v1, static_cast(UINT_MAX)); + m.set(v1, static_cast(UINT_MAX)); m.add(v1, m.mk_z(1), v2); m.mul(v2, v2, v3); std::cout << "v2:\n" << m.to_string(v2) << "\n"; @@ -282,7 +282,7 @@ void tst_int_min_bug() { mpz big; mpz expected; mpz r; - m.set(big, static_cast(UINT64_MAX)); + m.set(big, static_cast(UINT64_MAX)); m.set(expected, "18446744075857035263"); m.sub(big, intmin, r); std::cout << "r: " << m.to_string(r) << "\nexpected: " << m.to_string(expected) << "\n"; diff --git a/src/test/prime_generator.cpp b/src/test/prime_generator.cpp index 12c38ef78..3820959d9 100644 --- a/src/test/prime_generator.cpp +++ b/src/test/prime_generator.cpp @@ -25,7 +25,7 @@ void tst_prime_generator() { prime_generator gen; for (unsigned i = 0; i < 10000; i++) { - uint64 p = gen(i); + uint64_t p = gen(i); std::cout << p << ", "; if (i % 11 == 0) std::cout << "\n"; std::cout.flush(); @@ -33,8 +33,8 @@ void tst_prime_generator() { continue; m.set(sqrt_p, p); m.root(sqrt_p, 2); - uint64 k = m.get_uint64(sqrt_p); - for (uint64 i = 2; i <= k; i++) { + uint64_t k = m.get_uint64(sqrt_p); + for (uint64_t i = 2; i <= k; i++) { ENSURE(p % i != 0); } } diff --git a/src/test/rational.cpp b/src/test/rational.cpp index 0618a01fb..ac477a02f 100644 --- a/src/test/rational.cpp +++ b/src/test/rational.cpp @@ -194,8 +194,8 @@ static void tst2() { ENSURE(uint64_max.is_uint64()); // get_int64, get_uint64 - uint64 u1 = uint64_max.get_uint64(); - uint64 u2 = UINT64_MAX; + uint64_t u1 = uint64_max.get_uint64(); + uint64_t u2 = UINT64_MAX; VERIFY(u1 == u2); std::cout << "int64_max: " << int64_max << ", INT64_MAX: " << INT64_MAX << ", int64_max.get_int64(): " << int64_max.get_int64() << ", int64_max.get_uint64(): " << int64_max.get_uint64() << "\n"; ENSURE(int64_max.get_int64() == INT64_MAX); diff --git a/src/util/checked_int64.h b/src/util/checked_int64.h index e5a88fb31..507564a2e 100644 --- a/src/util/checked_int64.h +++ b/src/util/checked_int64.h @@ -7,7 +7,7 @@ Module Name: Abstract: - A class for wrapping checked (and unchecked) int64 operations. + A class for wrapping checked (and unchecked) int64_t operations. Note: the mpfx class defines a more general class of fixed-point operations. A tradeoff is that it relies on a manager. This class several of the most common operations from rational, so @@ -29,15 +29,15 @@ Revision History: template class checked_int64 { - int64 m_value; + int64_t m_value; typedef checked_int64 ci; - rational r64(int64 i) { return rational(i, rational::i64()); } + rational r64(int64_t i) { return rational(i, rational::i64()); } public: checked_int64(): m_value(0) {} - checked_int64(int64 v): m_value(v) {} + checked_int64(int64_t v): m_value(v) {} checked_int64(checked_int64 const& other) { m_value = other.m_value; } class overflow_exception : public z3_exception { @@ -57,7 +57,7 @@ public: static checked_int64 one() { return ci(1); } static checked_int64 minus_one() { return ci(-1);} - int64 get_int64() const { return m_value; } + int64_t get_int64() const { return m_value; } checked_int64 abs() const { if (m_value >= 0) { @@ -117,9 +117,9 @@ public: checked_int64& operator+=(checked_int64 const& other) { if (CHECK) { - uint64 x = static_cast(m_value); - uint64 y = static_cast(other.m_value); - int64 r = static_cast(x + y); + uint64_t x = static_cast(m_value); + uint64_t y = static_cast(other.m_value); + int64_t r = static_cast(x + y); if (m_value > 0 && other.m_value > 0 && r <= 0) throw overflow_exception(); if (m_value < 0 && other.m_value < 0 && r >= 0) throw overflow_exception(); m_value = r; @@ -132,9 +132,9 @@ public: checked_int64& operator-=(checked_int64 const& other) { if (CHECK) { - uint64 x = static_cast(m_value); - uint64 y = static_cast(other.m_value); - int64 r = static_cast(x - y); + uint64_t x = static_cast(m_value); + uint64_t y = static_cast(other.m_value); + int64_t r = static_cast(x - y); if (m_value > 0 && other.m_value < 0 && r <= 0) throw overflow_exception(); if (m_value < 0 && other.m_value > 0 && r >= 0) throw overflow_exception(); m_value = r; diff --git a/src/util/double_manager.h b/src/util/double_manager.h index 7532a3b8b..481701f42 100644 --- a/src/util/double_manager.h +++ b/src/util/double_manager.h @@ -75,8 +75,8 @@ public: static void set(double & a, char const * val) { a = atof(val); } static void set(double & a, int val) { a = static_cast(val); } static void set(double & a, unsigned val) { a = static_cast(val); } - static void set(double & a, int64 val) { a = static_cast(val); } - static void set(double & a, uint64 val) { a = static_cast(val); } + static void set(double & a, int64_t val) { a = static_cast(val); } + static void set(double & a, uint64_t val) { a = static_cast(val); } static void swap(double & a, double & b) { std::swap(a, b); } bool is_pos(double a) const { return a > m_zero_tolerance; } bool is_neg(double a) const { return a < m_zero_tolerance; } @@ -93,11 +93,11 @@ public: } static unsigned hash(double a) { - return hash_ull(static_cast(a)); + return hash_ull(static_cast(a)); } }; -static_assert(sizeof(uint64) == sizeof(double), ""); +static_assert(sizeof(uint64_t) == sizeof(double), ""); #endif /* DOUBLE_MANAGER_H_ */ diff --git a/src/util/hash.h b/src/util/hash.h index bc6117cac..a2af8253f 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -140,8 +140,8 @@ struct size_t_hash { }; struct uint64_hash { - typedef uint64 data; - unsigned operator()(uint64 x) const { return static_cast(x); } + typedef uint64_t data; + unsigned operator()(uint64_t x) const { return static_cast(x); } }; struct bool_hash { diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index 014e62625..c59621b6b 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -91,8 +91,8 @@ hwf_manager::~hwf_manager() { } -uint64 RAW(double X) { uint64 tmp; memcpy(&tmp, &(X), sizeof(uint64)); return tmp; } -double DBL(uint64 X) { double tmp; memcpy(&tmp, &(X), sizeof(double)); return tmp; } +uint64_t RAW(double X) { uint64_t tmp; memcpy(&tmp, &(X), sizeof(uint64_t)); return tmp; } +double DBL(uint64_t X) { double tmp; memcpy(&tmp, &(X), sizeof(double)); return tmp; } void hwf_manager::set(hwf & o, int value) { o.value = (double) value; @@ -147,7 +147,7 @@ void hwf_manager::set(hwf & o, mpf_rounding_mode rm, mpq const & significand, mp mpq sig; m_mpq_manager.set(sig, significand); - int64 exp = m_mpz_manager.get_int64(exponent); + int64_t exp = m_mpz_manager.get_int64(exponent); if (m_mpq_manager.is_zero(significand)) o.value = 0.0; @@ -160,17 +160,17 @@ void hwf_manager::set(hwf & o, mpf_rounding_mode rm, mpq const & significand, mp } hwf s; s.value = m_mpq_manager.get_double(sig); - uint64 r = (RAW(s.value) & 0x800FFFFFFFFFFFFFull) | ((exp + 1023) << 52); + uint64_t r = (RAW(s.value) & 0x800FFFFFFFFFFFFFull) | ((exp + 1023) << 52); o.value = DBL(r); } } -void hwf_manager::set(hwf & o, bool sign, uint64 significand, int exponent) { +void hwf_manager::set(hwf & o, bool sign, uint64_t significand, int exponent) { // Assumption: this represents (sign * -1) * (significand/2^sbits) * 2^exponent. SASSERT(significand <= 0x000FFFFFFFFFFFFFull); SASSERT(-1022 <= exponent && exponent <= 1023); - uint64 raw = (sign?0x8000000000000000ull:0); - raw |= (((uint64)exponent) + 1023) << 52; + uint64_t raw = (sign?0x8000000000000000ull:0); + raw |= (((uint64_t)exponent) + 1023) << 52; raw |= significand; memcpy(&o.value, &raw, sizeof(double)); } @@ -428,7 +428,7 @@ void hwf_manager::to_rational(hwf const & x, unsynch_mpq_manager & qm, mpq & o) } bool hwf_manager::is_zero(hwf const & x) { - uint64 t = RAW(x.value) & 0x7FFFFFFFFFFFFFFFull; + uint64_t t = RAW(x.value) & 0x7FFFFFFFFFFFFFFFull; return (t == 0x0ull); // CMW: I tried, and these are slower: // return (t != 0x0ull) ? false : true; @@ -483,12 +483,12 @@ bool hwf_manager::is_ninf(hwf const & x) { } bool hwf_manager::is_normal(hwf const & x) { - uint64 t = RAW(x.value) & 0x7FF0000000000000ull; + uint64_t t = RAW(x.value) & 0x7FF0000000000000ull; return (t != 0x0ull && t != 0x7FF0000000000000ull); } bool hwf_manager::is_denormal(hwf const & x) { - uint64 t = RAW(x.value); + uint64_t t = RAW(x.value); return ((t & 0x7FF0000000000000ull) == 0x0 && (t & 0x000FFFFFFFFFFFFFull) != 0x0); } @@ -498,7 +498,7 @@ bool hwf_manager::is_regular(hwf const & x) { // Note that +-0.0 and denormal numbers have exponent==0; these are regular. // All normal numbers are also regular. What remains is +-Inf and NaN, they are // not regular and they are the only numbers that have exponent 7FF. - uint64 e = RAW(x.value) & 0x7FF0000000000000ull; // the exponent + uint64_t e = RAW(x.value) & 0x7FF0000000000000ull; // the exponent return (e != 0x7FF0000000000000ull); } @@ -513,15 +513,15 @@ bool hwf_manager::is_int(hwf const & x) { return false; else { - uint64 t = sig(x); + uint64_t t = sig(x); unsigned shift = 52 - ((unsigned)e); - uint64 mask = (0x1ull << shift) - 1; + uint64_t mask = (0x1ull << shift) - 1; return (t & mask) == 0; } } void hwf_manager::mk_nzero(hwf & o) { - uint64 raw = 0x8000000000000000ull; + uint64_t raw = 0x8000000000000000ull; o.value = DBL(raw); } @@ -537,22 +537,22 @@ void hwf_manager::mk_zero(bool sign, hwf & o) { } void hwf_manager::mk_nan(hwf & o) { - uint64 raw = 0x7FF0000000000001ull; + uint64_t raw = 0x7FF0000000000001ull; o.value = DBL(raw); } void hwf_manager::mk_inf(bool sign, hwf & o) { - uint64 raw = (sign) ? 0xFFF0000000000000ull : 0x7FF0000000000000ull; + uint64_t raw = (sign) ? 0xFFF0000000000000ull : 0x7FF0000000000000ull; o.value = DBL(raw); } void hwf_manager::mk_pinf(hwf & o) { - uint64 raw = 0x7FF0000000000000ull; + uint64_t raw = 0x7FF0000000000000ull; o.value = DBL(raw); } void hwf_manager::mk_ninf(hwf & o) { - uint64 raw = 0xFFF0000000000000ull; + uint64_t raw = 0xFFF0000000000000ull; o.value = DBL(raw); } diff --git a/src/util/hwf.h b/src/util/hwf.h index 5f7692204..21e7655ea 100644 --- a/src/util/hwf.h +++ b/src/util/hwf.h @@ -28,8 +28,8 @@ class hwf { friend class hwf_manager; double value; hwf & operator=(hwf const & other) { UNREACHABLE(); return *this; } - uint64 get_raw() const { - uint64 n; + uint64_t get_raw() const { + uint64_t n; SASSERT(sizeof(n) == sizeof(value)); memcpy(&n, &value, sizeof(value)); return n; @@ -60,7 +60,7 @@ public: void set(hwf & o, mpf_rounding_mode rm, mpq const & value); void set(hwf & o, mpf_rounding_mode rm, char const * value); void set(hwf & o, mpf_rounding_mode rm, mpq const & significand, mpz const & exponent); - void set(hwf & o, bool sign, uint64 significand, int exponent); + void set(hwf & o, bool sign, uint64_t significand, int exponent); void set(hwf & o, hwf const & x); // auxiliary methods to make the interface compatible with mpf @@ -128,7 +128,7 @@ public: return (x.get_raw() & 0x8000000000000000ull) != 0; } - uint64 sig(hwf const & x) const { + uint64_t sig(hwf const & x) const { return x.get_raw() & 0x000FFFFFFFFFFFFFull; } diff --git a/src/util/inf_eps_rational.h b/src/util/inf_eps_rational.h index c184623ca..d0b6f2d99 100644 --- a/src/util/inf_eps_rational.h +++ b/src/util/inf_eps_rational.h @@ -118,12 +118,12 @@ class inf_eps_rational { bool is_rational() const { return m_infty.is_zero() && m_r.is_rational(); } - int64 get_int64() const { + int64_t get_int64() const { SASSERT(is_int64()); return m_r.get_int64(); } - uint64 get_uint64() const { + uint64_t get_uint64() const { SASSERT(is_uint64()); return m_r.get_uint64(); } diff --git a/src/util/inf_int_rational.h b/src/util/inf_int_rational.h index c9c82052e..44ed76ebd 100644 --- a/src/util/inf_int_rational.h +++ b/src/util/inf_int_rational.h @@ -109,12 +109,12 @@ class inf_int_rational { bool is_rational() const { return m_second == 0; } - int64 get_int64() const { + int64_t get_int64() const { SASSERT(is_int64()); return m_first.get_int64(); } - uint64 get_uint64() const { + uint64_t get_uint64() const { SASSERT(is_uint64()); return m_first.get_uint64(); } diff --git a/src/util/inf_rational.h b/src/util/inf_rational.h index d49e45f50..c3f4160ba 100644 --- a/src/util/inf_rational.h +++ b/src/util/inf_rational.h @@ -122,12 +122,12 @@ class inf_rational { bool is_rational() const { return m_second.is_zero(); } - int64 get_int64() const { + int64_t get_int64() const { SASSERT(is_int64()); return m_first.get_int64(); } - uint64 get_uint64() const { + uint64_t get_uint64() const { SASSERT(is_uint64()); return m_first.get_uint64(); } diff --git a/src/util/inf_s_integer.h b/src/util/inf_s_integer.h index 067000202..dd136d1b9 100644 --- a/src/util/inf_s_integer.h +++ b/src/util/inf_s_integer.h @@ -60,8 +60,8 @@ class inf_s_integer { bool is_int64() const { return m_second == 0; } bool is_uint64() const { return m_second == 0; } bool is_rational() const { return m_second == 0; } - int64 get_int64() const { return m_first; } - uint64 get_uint64() const { return m_first; } + int64_t get_int64() const { return m_first; } + uint64_t get_uint64() const { return m_first; } s_integer get_rational() const { return s_integer(m_first); } s_integer get_infinitesimal() const { return s_integer(m_second); } inf_s_integer & operator=(const inf_s_integer & r) { diff --git a/src/util/mpbq.cpp b/src/util/mpbq.cpp index 9fcd1b58f..3edbdab67 100644 --- a/src/util/mpbq.cpp +++ b/src/util/mpbq.cpp @@ -250,7 +250,7 @@ void mpbq_manager::mul(mpbq const & a, mpz const & b, mpbq & r) { } void mpbq_manager::power(mpbq & a, unsigned k) { - SASSERT(static_cast(k) * static_cast(a.k()) <= static_cast(UINT_MAX)); + SASSERT(static_cast(k) * static_cast(a.k()) <= static_cast(UINT_MAX)); // We don't need to normalize because: // If a.m_k == 0, then a is an integer, and the result be an integer // If a.m_k > 0, then a.m_num must be odd, and the (a.m_num)^k will also be odd diff --git a/src/util/mpbq.h b/src/util/mpbq.h index 61ef2b0e2..ed8a8c523 100644 --- a/src/util/mpbq.h +++ b/src/util/mpbq.h @@ -84,7 +84,7 @@ public: void set(mpbq & a, mpz const & n, unsigned k) { m_manager.set(a.m_num, n); a.m_k = k; normalize(a); } void set(mpbq & a, mpz const & n) { m_manager.set(a.m_num, n); a.m_k = 0; } void set(mpbq & a, mpbq const & b) { m_manager.set(a.m_num, b.m_num); a.m_k = b.m_k; } - void set(mpbq & a, int64 n, unsigned k) { m_manager.set(a.m_num, n); a.m_k = k; normalize(a); } + void set(mpbq & a, int64_t n, unsigned k) { m_manager.set(a.m_num, n); a.m_k = k; normalize(a); } bool is_int(mpbq const & a) const { return a.m_k == 0; } void get_numerator(mpbq const & a, mpz & n) { m_manager.set(n, a.m_num); } diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index b9829f02d..17705cc34 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -115,11 +115,11 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, double value) { // double === mpf(11, 53) static_assert(sizeof(double) == 8, "doubles are 8 bytes"); - uint64 raw; + uint64_t raw; memcpy(&raw, &value, sizeof(double)); bool sign = (raw >> 63) != 0; - int64 e = ((raw & 0x7FF0000000000000ull) >> 52) - 1023; - uint64 s = raw & 0x000FFFFFFFFFFFFFull; + int64_t e = ((raw & 0x7FF0000000000000ull) >> 52) - 1023; + uint64_t s = raw & 0x000FFFFFFFFFFFFFull; TRACE("mpf_dbg", tout << "set: " << value << " is: raw=" << raw << " (double)" << " sign=" << sign << " s=" << s << " e=" << e << std::endl;); @@ -300,7 +300,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode TRACE("mpf_dbg", tout << "set: res = " << to_string(o) << std::endl;); } -void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, bool sign, mpf_exp_t exponent, uint64 significand) { +void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, bool sign, mpf_exp_t exponent, uint64_t significand) { // Assumption: this represents (sign * -1) * (significand/2^sbits) * 2^exponent. o.ebits = ebits; o.sbits = sbits; @@ -1711,8 +1711,8 @@ void mpf_manager::to_rational(mpf const & x, unsynch_mpq_manager & qm, mpq & o) double mpf_manager::to_double(mpf const & x) { SASSERT(x.ebits <= 11 && x.sbits <= 53); - uint64 raw = 0; - int64 sig = 0, exp = 0; + uint64_t raw = 0; + int64_t sig = 0, exp = 0; sig = m_mpz_manager.get_uint64(x.significand); sig <<= 53 - x.sbits; @@ -1741,7 +1741,7 @@ float mpf_manager::to_float(mpf const & x) { unsigned int raw = 0; unsigned int sig = 0, exp = 0; - uint64 q = m_mpz_manager.get_uint64(x.significand); + uint64_t q = m_mpz_manager.get_uint64(x.significand); SASSERT(q < 4294967296ull); sig = q & 0x00000000FFFFFFFF; sig <<= 24 - x.sbits; @@ -1751,7 +1751,7 @@ float mpf_manager::to_float(mpf const & x) { else if (has_bot_exp(x)) exp = -127; else { - int64 q = x.exponent; + int64_t q = x.exponent; SASSERT(q < 4294967296ll); exp = q & 0x00000000FFFFFFFF; } diff --git a/src/util/mpf.h b/src/util/mpf.h index 27116e2de..107ada0bd 100644 --- a/src/util/mpf.h +++ b/src/util/mpf.h @@ -35,7 +35,7 @@ typedef enum { MPF_ROUND_TOWARD_ZERO } mpf_rounding_mode; -typedef int64 mpf_exp_t; +typedef int64_t mpf_exp_t; class mpf { friend class mpf_manager; @@ -80,7 +80,7 @@ public: void set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode rm, mpq const & value); void set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode rm, char const * value); void set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode rm, mpz const & exponent, mpq const & significand); - void set(mpf & o, unsigned ebits, unsigned sbits, bool sign, mpf_exp_t exponent, uint64 significand); + void set(mpf & o, unsigned ebits, unsigned sbits, bool sign, mpf_exp_t exponent, uint64_t significand); void set(mpf & o, unsigned ebits, unsigned sbits, bool sign, mpf_exp_t exponent, mpz const & significand); void set(mpf & o, mpf const & x); void set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode rm, mpf const & x); diff --git a/src/util/mpff.cpp b/src/util/mpff.cpp index eac9cc80c..64e07f9f0 100644 --- a/src/util/mpff.cpp +++ b/src/util/mpff.cpp @@ -155,27 +155,27 @@ bool mpff_manager::is_uint64(mpff const & n) const { !has_one_at_first_k_bits(m_precision, sig(n), -n.m_exponent); } -uint64 mpff_manager::get_uint64(mpff const & a) const { +uint64_t mpff_manager::get_uint64(mpff const & a) const { SASSERT(is_uint64(a)); if (is_zero(a)) return 0; int exp = -a.m_exponent - sizeof(unsigned) * 8 * (m_precision - 2); SASSERT(exp >= 0); - uint64 * s = reinterpret_cast(sig(a) + (m_precision - 2)); + uint64_t * s = reinterpret_cast(sig(a) + (m_precision - 2)); return *s >> exp; } -int64 mpff_manager::get_int64(mpff const & a) const { +int64_t mpff_manager::get_int64(mpff const & a) const { SASSERT(is_int64(a)); if (is_zero(a)) return 0; int exp = -a.m_exponent - sizeof(unsigned) * 8 * (m_precision - 2); SASSERT(exp >= 0); - uint64 * s = reinterpret_cast(sig(a) + (m_precision - 2)); + uint64_t * s = reinterpret_cast(sig(a) + (m_precision - 2)); // INT64_MIN case if (exp == 0 && *s == 0x8000000000000000ull && is_neg(a)) { return INT64_MIN; } else { - int64 r = *s >> exp; + int64_t r = *s >> exp; if (is_neg(a)) r = -r; return r; @@ -249,26 +249,26 @@ void mpff_manager::set(mpff & n, unsigned v) { SASSERT(check(n)); } -void mpff_manager::set(mpff & n, int64 v) { +void mpff_manager::set(mpff & n, int64_t v) { if (v == 0) { reset(n); } else { if (v < 0) { - set(n, 1 + static_cast(-(1+v))); + set(n, 1 + static_cast(-(1+v))); n.m_sign = 1; } else { - set(n, static_cast(v)); + set(n, static_cast(v)); } } SASSERT(check(n)); SASSERT(get_int64(n) == v); } -void mpff_manager::set(mpff & n, uint64 v) { +void mpff_manager::set(mpff & n, uint64_t v) { #ifdef Z3DEBUG - uint64 old_v = v; + uint64_t old_v = v; #endif if (v == 0) { reset(n); @@ -278,7 +278,7 @@ void mpff_manager::set(mpff & n, uint64 v) { n.m_sign = 0; unsigned * _v = reinterpret_cast(&v); int num_leading_zeros = nlz(2, _v); - n.m_exponent = static_cast(8 * sizeof(uint64)) - num_leading_zeros - static_cast(m_precision_bits); + n.m_exponent = static_cast(8 * sizeof(uint64_t)) - num_leading_zeros - static_cast(m_precision_bits); v <<= num_leading_zeros; SASSERT(m_precision >= 2); unsigned * s = sig(n); @@ -299,7 +299,7 @@ void mpff_manager::set(mpff & n, int num, unsigned den) { SASSERT(check(n)); } -void mpff_manager::set(mpff & n, int64 num, uint64 den) { +void mpff_manager::set(mpff & n, int64_t num, uint64_t den) { scoped_mpff a(*this), b(*this); set(a, num); set(b, den); @@ -470,7 +470,7 @@ bool mpff_manager::lt(mpff const & a, mpff const & b) const { } } -void mpff_manager::inc_significand(unsigned * s, int64 & exp) { +void mpff_manager::inc_significand(unsigned * s, int64_t & exp) { if (!::inc(m_precision, s)) { SASSERT(::is_zero(m_precision, s)); s[m_precision - 1] = MIN_MSW; @@ -597,7 +597,7 @@ void mpff_manager::prev(mpff & a) { SASSERT(check(a)); } -void mpff_manager::set_big_exponent(mpff & a, int64 e) { +void mpff_manager::set_big_exponent(mpff & a, int64_t e) { SASSERT(e > INT_MAX || e < INT_MIN); if (e > INT_MAX) { if (a.m_sign == 1) { @@ -715,7 +715,7 @@ void mpff_manager::add_sub(bool is_sub, mpff const & a, mpff const & b, mpff & c else if (num_leading_zeros == sizeof(unsigned) * 8 - 1) { // shift 1 right bool _inc_significand = ((c.m_sign == 1) != m_to_plus_inf) && has_one_at_first_k_bits(m_precision*2, sig_r, 1); - int64 exp_c = exp_a; + int64_t exp_c = exp_a; exp_c++; shr(m_precision + 1, sig_r, 1, m_precision, sig_c); if (_inc_significand) @@ -728,7 +728,7 @@ void mpff_manager::add_sub(bool is_sub, mpff const & a, mpff const & b, mpff & c // Now, we can assume sig_r has size m_precision SASSERT(num_leading_zeros > 0); // shift left num_leading_zeros - int64 exp_c = exp_a; + int64_t exp_c = exp_a; exp_c -= num_leading_zeros; shl(m_precision, sig_r, num_leading_zeros, m_precision, sig_c); set_exponent(c, exp_c); @@ -752,7 +752,7 @@ void mpff_manager::add_sub(bool is_sub, mpff const & a, mpff const & b, mpff & c reset(c); } else if (num_leading_zeros > 0) { - int64 exp_c = exp_a; + int64_t exp_c = exp_a; exp_c -= num_leading_zeros; shl(m_precision, sig_c, num_leading_zeros, m_precision, sig_c); set_exponent(c, exp_c); @@ -787,10 +787,10 @@ void mpff_manager::mul(mpff const & a, mpff const & b, mpff & c) { allocate_if_needed(c); TRACE("mpff", tout << "mul("; display(tout, a); tout << ", "; display(tout, b); tout << ")\n";); c.m_sign = a.m_sign ^ b.m_sign; - // use int64 to make sure we do not have overflows - int64 exp_a = a.m_exponent; - int64 exp_b = b.m_exponent; - int64 exp_c = exp_a + exp_b; + // use int64_t to make sure we do not have overflows + int64_t exp_a = a.m_exponent; + int64_t exp_b = b.m_exponent; + int64_t exp_c = exp_a + exp_b; // store result in m_buffers[0] unsigned * r = m_buffers[0].c_ptr(); m_mpn_manager.mul(sig(a), m_precision, sig(b), m_precision, r); @@ -834,7 +834,7 @@ void mpff_manager::div(mpff const & a, mpff const & b, mpff & c) { #if 1 else if (is_two(b)) { set(c, a); - int64 exp_c = a.m_exponent; + int64_t exp_c = a.m_exponent; exp_c--; set_exponent(c, exp_c); } @@ -842,10 +842,10 @@ void mpff_manager::div(mpff const & a, mpff const & b, mpff & c) { else { allocate_if_needed(c); c.m_sign = a.m_sign ^ b.m_sign; - // use int64 to make sure we do not have overflows - int64 exp_a = a.m_exponent; - int64 exp_b = b.m_exponent; - int64 exp_c = exp_a - exp_b; + // use int64_t to make sure we do not have overflows + int64_t exp_a = a.m_exponent; + int64_t exp_b = b.m_exponent; + int64_t exp_c = exp_a - exp_b; exp_c -= m_precision_bits; // we will multiplying (shifting) a by 2^m_precision_bits. // copy a to buffer 0, and shift by m_precision_bits @@ -1023,7 +1023,7 @@ void mpff_manager::power(mpff const & a, unsigned p, mpff & b) { b.m_sign = 0; else b.m_sign = a.m_sign; - int64 exp = a.m_exponent; + int64_t exp = a.m_exponent; exp *= p; if (exp > INT_MAX || exp < INT_MIN) throw overflow_exception(); @@ -1057,7 +1057,7 @@ void mpff_manager::power(mpff const & a, unsigned p, mpff & b) { bool mpff_manager::is_power_of_two(mpff const & a, unsigned & k) const { if (!is_power_of_two(a)) return false; - int64 exp = a.m_exponent + m_precision_bits - 1; + int64_t exp = a.m_exponent + m_precision_bits - 1; SASSERT(exp >= 0); k = static_cast(exp); return true; @@ -1132,7 +1132,7 @@ void mpff_manager::to_mpq_core(mpff const & n, mpq_manager & m, mpq & t) if (exp < 0) { // Avoid -INT_MIN == INT_MIN issue. It is not really useful, since we will run out of memory anyway. if (exp == INT_MIN) - abs_exp = static_cast(-static_cast(INT_MIN)); + abs_exp = static_cast(-static_cast(INT_MIN)); else abs_exp = -exp; } @@ -1177,7 +1177,7 @@ void mpff_manager::display(std::ostream & out, mpff const & n) const { svector & u_buffer = const_cast(this)->m_buffers[0]; int num_trailing_zeros = ntz(m_precision, u_buffer.c_ptr()); int shift = 0; - int64 exp = n.m_exponent; // use int64 to avoid -INT_MIN == INT_MIN issue + int64_t exp = n.m_exponent; // use int64_t to avoid -INT_MIN == INT_MIN issue if (exp < 0) { if (num_trailing_zeros >= -exp) { shift = static_cast(-exp); @@ -1194,7 +1194,7 @@ void mpff_manager::display(std::ostream & out, mpff const & n) const { out << m_mpn_manager.to_string(u_buffer.c_ptr(), m_precision, str_buffer.begin(), str_buffer.size()); if (exp > 0) { if (exp <= 63) { - uint64 _exp = 1; + uint64_t _exp = 1; _exp <<= exp; out << "*" << _exp; } @@ -1209,7 +1209,7 @@ void mpff_manager::display(std::ostream & out, mpff const & n) const { else if (exp < 0) { exp = -exp; if (exp <= 63) { - uint64 _exp = 1; + uint64_t _exp = 1; _exp <<= exp; out << "/" << _exp; } @@ -1225,8 +1225,8 @@ void mpff_manager::display(std::ostream & out, mpff const & n) const { void mpff_manager::display_decimal(std::ostream & out, mpff const & n, unsigned prec, unsigned min_exponent) { // The result in scientific notation when n.m_exponent >= min_exponent or n.m_exponent <= - min_exponent - m_precision_bits - int64 exp = n.m_exponent; - if (exp >= min_exponent || exp <= -static_cast(min_exponent) - m_precision_bits || is_int(n)) { + int64_t exp = n.m_exponent; + if (exp >= min_exponent || exp <= -static_cast(min_exponent) - m_precision_bits || is_int(n)) { display(out, n); return; } @@ -1327,7 +1327,7 @@ void mpff_manager::display_smt2(std::ostream & out, mpff const & n, bool decimal svector & u_buffer = const_cast(this)->m_buffers[0]; int num_trailing_zeros = ntz(m_precision, u_buffer.c_ptr()); int shift = 0; - int64 exp = n.m_exponent; + int64_t exp = n.m_exponent; if (exp < 0) { if (num_trailing_zeros >= -exp) { shift = static_cast(-exp); @@ -1353,7 +1353,7 @@ void mpff_manager::display_smt2(std::ostream & out, mpff const & n, bool decimal if (exp != 0) { if (exp < 0) exp = -exp; if (exp <= 63) { - uint64 _exp = 1; + uint64_t _exp = 1; _exp <<= exp; out << _exp; if (decimal) out << ".0"; @@ -1387,8 +1387,8 @@ unsigned mpff_manager::prev_power_of_two(mpff const & a) { return 0; if (a.m_exponent <= -static_cast(m_precision_bits)) return 0; // Number is smaller than 1 - SASSERT(static_cast(a.m_exponent) + static_cast(m_precision_bits) - 1 >= 0); - SASSERT(static_cast(a.m_exponent) + static_cast(m_precision_bits) - 1 <= static_cast(static_cast(UINT_MAX))); + SASSERT(static_cast(a.m_exponent) + static_cast(m_precision_bits) - 1 >= 0); + SASSERT(static_cast(a.m_exponent) + static_cast(m_precision_bits) - 1 <= static_cast(static_cast(UINT_MAX))); return m_precision_bits + a.m_exponent - 1; } diff --git a/src/util/mpff.h b/src/util/mpff.h index e34f2cb41..8023053d2 100644 --- a/src/util/mpff.h +++ b/src/util/mpff.h @@ -92,7 +92,7 @@ class mpff_manager { // // Remarks: // - // - All values of type int, unsigned, int64 and uint64 can be precisely represented as mpff numerals. + // - All values of type int, unsigned, int64_t and uint64_t can be precisely represented as mpff numerals. // // - Hardware float and double values (corresponding to rationals) can also be precisely represented as mpff numerals. // That is, NaN, +oo and -oo are not supported by this module. @@ -141,14 +141,14 @@ class mpff_manager { // copy (and shift by m_precision_bits) n to buffer idx void to_buffer_shifting(unsigned idx, mpff const & n) const; - void inc_significand(unsigned * s, int64 & exp); + void inc_significand(unsigned * s, int64_t & exp); void inc_significand(mpff & a); void dec_significand(mpff & a); bool min_significand(mpff const & a) const; void set_min_significand(mpff & a); void set_max_significand(mpff & a); - void set_big_exponent(mpff & a, int64 e); - void set_exponent(mpff & a, int64 e) { + void set_big_exponent(mpff & a, int64_t e); + void set_exponent(mpff & a, int64_t e) { if (e > INT_MAX || e < INT_MIN) set_big_exponent(a, e); else @@ -286,12 +286,12 @@ public: bool is_plus_epsilon(mpff const & a) const; /** - \brief Return true if \c a is an integer and fits in an int64 machine integer. + \brief Return true if \c a is an integer and fits in an int64_t machine integer. */ bool is_int64(mpff const & a) const; /** - \brief Return true if \c a is a non-negative integer and fits in an int64 machine integer. + \brief Return true if \c a is a non-negative integer and fits in an int64_t machine integer. */ bool is_uint64(mpff const & a) const; @@ -372,10 +372,10 @@ public: void set(mpff & n, int v); void set(mpff & n, unsigned v); - void set(mpff & n, int64 v); - void set(mpff & n, uint64 v); + void set(mpff & n, int64_t v); + void set(mpff & n, uint64_t v); void set(mpff & n, int num, unsigned den); - void set(mpff & n, int64 num, uint64 den); + void set(mpff & n, int64_t num, uint64_t den); void set(mpff & n, mpff const & v); void set(mpff & n, unsynch_mpz_manager & m, mpz const & v); void set(mpff & n, synch_mpz_manager & m, mpz const & v); @@ -448,14 +448,14 @@ public: \pre is_int64(n) */ - int64 get_int64(mpff const & n) const; + int64_t get_int64(mpff const & n) const; /** \brief Return n as an uint64. \pre is_uint64(n) */ - uint64 get_uint64(mpff const & n) const; + uint64_t get_uint64(mpff const & n) const; /** \brief Return the biggest k s.t. 2^k <= a. diff --git a/src/util/mpfx.cpp b/src/util/mpfx.cpp index e46708341..e17a5e766 100644 --- a/src/util/mpfx.cpp +++ b/src/util/mpfx.cpp @@ -164,10 +164,10 @@ void mpfx_manager::set(mpfx & n, unsigned v) { SASSERT(check(n)); } -void mpfx_manager::set(mpfx & n, int64 v) { +void mpfx_manager::set(mpfx & n, int64_t v) { if (m_int_part_sz == 1) { - if (v < -static_cast(static_cast(UINT_MAX)) || - v > static_cast(static_cast(UINT_MAX))) + if (v < -static_cast(static_cast(UINT_MAX)) || + v > static_cast(static_cast(UINT_MAX))) throw overflow_exception(); } if (v == 0) { @@ -175,11 +175,11 @@ void mpfx_manager::set(mpfx & n, int64 v) { } else { if (v < 0) { - set(n, static_cast(-v)); + set(n, static_cast(-v)); n.m_sign = 1; } else { - set(n, static_cast(v)); + set(n, static_cast(v)); } } SASSERT(is_int(n)); @@ -187,9 +187,9 @@ void mpfx_manager::set(mpfx & n, int64 v) { SASSERT(check(n)); } -void mpfx_manager::set(mpfx & n, uint64 v) { +void mpfx_manager::set(mpfx & n, uint64_t v) { if (m_int_part_sz == 1) { - if (v > static_cast(UINT_MAX)) + if (v > static_cast(UINT_MAX)) throw overflow_exception(); } @@ -200,7 +200,7 @@ void mpfx_manager::set(mpfx & n, uint64 v) { allocate_if_needed(n); n.m_sign = 0; unsigned * w = words(n); - uint64 * _vp = &v; + uint64_t * _vp = &v; unsigned * _v = nullptr; memcpy(&_v, &_vp, sizeof(unsigned*)); for (unsigned i = 0; i < m_total_sz; i++) @@ -226,7 +226,7 @@ void mpfx_manager::set(mpfx & n, int num, unsigned den) { SASSERT(check(n)); } -void mpfx_manager::set(mpfx & n, int64 num, uint64 den) { +void mpfx_manager::set(mpfx & n, int64_t num, uint64_t den) { scoped_mpfx a(*this), b(*this); set(a, num); set(b, den); @@ -677,27 +677,27 @@ bool mpfx_manager::is_power_of_two(mpfx const & a) const { return is_power_of_two(a, k); } -int64 mpfx_manager::get_int64(mpfx const & n) const { +int64_t mpfx_manager::get_int64(mpfx const & n) const { SASSERT(is_int64(n)); unsigned * w = words(n); w += m_frac_part_sz; - uint64 r = 0; - memcpy(&r, w, sizeof(uint64)); + uint64_t r = 0; + memcpy(&r, w, sizeof(uint64_t)); if (r == 0x8000000000000000ull) { SASSERT(is_neg(n)); return INT64_MIN; } else { - return is_neg(n) ? -static_cast(r) : r; + return is_neg(n) ? -static_cast(r) : r; } } -uint64 mpfx_manager::get_uint64(mpfx const & n) const { +uint64_t mpfx_manager::get_uint64(mpfx const & n) const { SASSERT(is_uint64(n)); unsigned * w = words(n); w += m_frac_part_sz; - uint64 r = 0; - memcpy(&r, w, sizeof(uint64)); + uint64_t r = 0; + memcpy(&r, w, sizeof(uint64_t)); return r; } diff --git a/src/util/mpfx.h b/src/util/mpfx.h index 03a805f69..a8e93f0b0 100644 --- a/src/util/mpfx.h +++ b/src/util/mpfx.h @@ -200,12 +200,12 @@ public: bool is_minus_one(mpfx const & n) const { return is_neg(n) && is_abs_one(n); } /** - \brief Return true if \c a is an integer and fits in an int64 machine integer. + \brief Return true if \c a is an integer and fits in an \c int64_t machine integer. */ bool is_int64(mpfx const & a) const; /** - \brief Return true if \c a is a non-negative integer and fits in an int64 machine integer. + \brief Return true if \c a is a non-negative integer and fits in an \c int64_t machine integer. */ bool is_uint64(mpfx const & a) const; @@ -306,10 +306,10 @@ public: void set(mpfx & n, int v); void set(mpfx & n, unsigned v); - void set(mpfx & n, int64 v); - void set(mpfx & n, uint64 v); + void set(mpfx & n, int64_t v); + void set(mpfx & n, uint64_t v); void set(mpfx & n, int num, unsigned den); - void set(mpfx & n, int64 num, uint64 den); + void set(mpfx & n, int64_t num, uint64_t den); void set(mpfx & n, mpfx const & v); void set(mpfx & n, unsynch_mpz_manager & m, mpz const & v); void set(mpfx & n, synch_mpz_manager & m, mpz const & v); @@ -343,14 +343,14 @@ public: \pre is_int64(n) */ - int64 get_int64(mpfx const & n) const; + int64_t get_int64(mpfx const & n) const; /** \brief Return n as an uint64. \pre is_uint64(n) */ - uint64 get_uint64(mpfx const & n) const; + uint64_t get_uint64(mpfx const & n) const; /** \brief Convert n into a mpz numeral. diff --git a/src/util/mpn.cpp b/src/util/mpn.cpp index 2059ea6fd..b8cab4a9f 100644 --- a/src/util/mpn.cpp +++ b/src/util/mpn.cpp @@ -23,7 +23,7 @@ Revision History: #define max(a,b) (((a) > (b)) ? (a) : (b)) -typedef uint64 mpn_double_digit; +typedef uint64_t mpn_double_digit; static_assert(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit), "size alignment"); const mpn_digit mpn_manager::zero = 0; diff --git a/src/util/mpq.h b/src/util/mpq.h index fd0ae13d4..f1b261278 100644 --- a/src/util/mpq.h +++ b/src/util/mpq.h @@ -686,7 +686,7 @@ public: normalize(a); } - void set(mpq & a, int64 n, uint64 d) { + void set(mpq & a, int64_t n, uint64_t d) { SASSERT(d != 0); set(a.m_num, n); set(a.m_den, d); @@ -718,16 +718,16 @@ public: void set(mpq & a, char const * val); - void set(mpz & a, int64 val) { mpz_manager::set(a, val); } + void set(mpz & a, int64_t val) { mpz_manager::set(a, val); } - void set(mpq & a, int64 val) { + void set(mpq & a, int64_t val) { set(a.m_num, val); reset_denominator(a); } - void set(mpz & a, uint64 val) { mpz_manager::set(a, val); } + void set(mpz & a, uint64_t val) { mpz_manager::set(a, val); } - void set(mpq & a, uint64 val) { + void set(mpq & a, uint64_t val) { set(a.m_num, val); reset_denominator(a); } @@ -765,17 +765,17 @@ public: bool is_int64(mpz const & a) const { return mpz_manager::is_int64(a); } - uint64 get_uint64(mpz const & a) const { return mpz_manager::get_uint64(a); } + uint64_t get_uint64(mpz const & a) const { return mpz_manager::get_uint64(a); } - int64 get_int64(mpz const & a) const { return mpz_manager::get_int64(a); } + int64_t get_int64(mpz const & a) const { return mpz_manager::get_int64(a); } bool is_uint64(mpq const & a) const { return is_int(a) && is_uint64(a.m_num); } bool is_int64(mpq const & a) const { return is_int(a) && is_int64(a.m_num); } - uint64 get_uint64(mpq const & a) const { SASSERT(is_uint64(a)); return get_uint64(a.m_num); } + uint64_t get_uint64(mpq const & a) const { SASSERT(is_uint64(a)); return get_uint64(a.m_num); } - int64 get_int64(mpq const & a) const { SASSERT(is_int64(a)); return get_int64(a.m_num); } + int64_t get_int64(mpq const & a) const { SASSERT(is_int64(a)); return get_int64(a.m_num); } double get_double(mpz const & a) const { return mpz_manager::get_double(a); } diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 7ad472ef1..39ea428a7 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -81,7 +81,7 @@ static T gcd_core(T u, T v) { } unsigned u_gcd(unsigned u, unsigned v) { return gcd_core(u, v); } -uint64 u64_gcd(uint64 u, uint64 v) { return gcd_core(u, v); } +uint64_t u64_gcd(uint64_t u, uint64_t v) { return gcd_core(u, v); } template mpz_manager::mpz_manager(): @@ -89,7 +89,7 @@ mpz_manager::mpz_manager(): if (SYNCH) omp_init_nest_lock(&m_lock); #ifndef _MP_GMP - if (sizeof(digit_t) == sizeof(uint64)) { + if (sizeof(digit_t) == sizeof(uint64_t)) { // 64-bit machine m_init_cell_capacity = 4; } @@ -101,7 +101,7 @@ mpz_manager::mpz_manager(): m_arg[i] = allocate(m_init_cell_capacity); m_arg[i]->m_size = 1; } - set(m_int_min, -static_cast(INT_MIN)); + set(m_int_min, -static_cast(INT_MIN)); #else // GMP mpz_init(m_tmp); @@ -122,8 +122,8 @@ mpz_manager::mpz_manager(): mpz_init(m_int64_max); mpz_init(m_int64_min); - max_l = static_cast(INT64_MAX % static_cast(UINT_MAX)); - max_h = static_cast(INT64_MAX / static_cast(UINT_MAX)); + max_l = static_cast(INT64_MAX % static_cast(UINT_MAX)); + max_h = static_cast(INT64_MAX / static_cast(UINT_MAX)); mpz_set_ui(m_int64_max, max_h); mpz_set_ui(m_tmp, UINT_MAX); mpz_mul(m_int64_max, m_tmp, m_int64_max); @@ -134,7 +134,7 @@ mpz_manager::mpz_manager(): #endif mpz one(1); - set(m_two64, (uint64)UINT64_MAX); + set(m_two64, (uint64_t)UINT64_MAX); add(m_two64, one, m_two64); } @@ -162,13 +162,13 @@ mpz_manager::~mpz_manager() { } template -void mpz_manager::set_big_i64(mpz & c, int64 v) { +void mpz_manager::set_big_i64(mpz & c, int64_t v) { #ifndef _MP_GMP if (is_small(c)) { c.m_ptr = allocate(m_init_cell_capacity); } SASSERT(capacity(c) >= m_init_cell_capacity); - uint64 _v; + uint64_t _v; if (v < 0) { _v = -v; c.m_val = -1; @@ -177,7 +177,7 @@ void mpz_manager::set_big_i64(mpz & c, int64 v) { _v = v; c.m_val = 1; } - if (sizeof(digit_t) == sizeof(uint64)) { + if (sizeof(digit_t) == sizeof(uint64_t)) { // 64-bit machine digits(c)[0] = static_cast(_v); c.m_ptr->m_size = 1; @@ -192,7 +192,7 @@ void mpz_manager::set_big_i64(mpz & c, int64 v) { if (is_small(c)) { c.m_ptr = allocate(); } - uint64 _v; + uint64_t _v; bool sign; if (v < 0) { _v = -v; @@ -212,14 +212,14 @@ void mpz_manager::set_big_i64(mpz & c, int64 v) { } template -void mpz_manager::set_big_ui64(mpz & c, uint64 v) { +void mpz_manager::set_big_ui64(mpz & c, uint64_t v) { #ifndef _MP_GMP if (is_small(c)) { c.m_ptr = allocate(m_init_cell_capacity); } SASSERT(capacity(c) >= m_init_cell_capacity); c.m_val = 1; - if (sizeof(digit_t) == sizeof(uint64)) { + if (sizeof(digit_t) == sizeof(uint64_t)) { // 64-bit machine digits(c)[0] = static_cast(v); c.m_ptr->m_size = 1; @@ -726,7 +726,7 @@ void mpz_manager::gcd(mpz const & a, mpz const & b, mpz & c) { // For now, it only works if sizeof(digit_t) == sizeof(unsigned) static_assert(sizeof(digit_t) == sizeof(unsigned), ""); - int64 a_hat, b_hat, A, B, C, D, T, q, a_sz, b_sz; + int64_t a_hat, b_hat, A, B, C, D, T, q, a_sz, b_sz; mpz a1, b1, t, r, tmp; set(a1, a); set(b1, b); @@ -766,10 +766,10 @@ void mpz_manager::gcd(mpz const & a, mpz const & b, mpz & c) { D = 1; while (true) { // Loop invariants - SASSERT(a_hat + A <= static_cast(UINT_MAX) + 1); - SASSERT(a_hat + B < static_cast(UINT_MAX) + 1); - SASSERT(b_hat + C < static_cast(UINT_MAX) + 1); - SASSERT(b_hat + D <= static_cast(UINT_MAX) + 1); + SASSERT(a_hat + A <= static_cast(UINT_MAX) + 1); + SASSERT(a_hat + B < static_cast(UINT_MAX) + 1); + SASSERT(b_hat + C < static_cast(UINT_MAX) + 1); + SASSERT(b_hat + D <= static_cast(UINT_MAX) + 1); // overflows can't happen since I'm using int64 if (b_hat + C == 0 || b_hat + D == 0) break; @@ -1035,7 +1035,7 @@ void mpz_manager::bitwise_or(mpz const & a, mpz const & b, mpz & c) { mod(a1, m_two64, a2); mod(b1, m_two64, b2); TRACE("mpz", tout << "a2: " << to_string(a2) << ", b2: " << to_string(b2) << "\n";); - uint64 v = get_uint64(a2) | get_uint64(b2); + uint64_t v = get_uint64(a2) | get_uint64(b2); TRACE("mpz", tout << "uint(a2): " << get_uint64(a2) << ", uint(b2): " << get_uint64(b2) << "\n";); set(tmp, v); mul(tmp, m, tmp); @@ -1082,7 +1082,7 @@ void mpz_manager::bitwise_and(mpz const & a, mpz const & b, mpz & c) { while (!is_zero(a1) && !is_zero(b1)) { mod(a1, m_two64, a2); mod(b1, m_two64, b2); - uint64 v = get_uint64(a2) & get_uint64(b2); + uint64_t v = get_uint64(a2) & get_uint64(b2); set(tmp, v); mul(tmp, m, tmp); add(c, tmp, c); // c += m * v @@ -1119,7 +1119,7 @@ void mpz_manager::bitwise_xor(mpz const & a, mpz const & b, mpz & c) { while (!is_zero(a1) && !is_zero(b1)) { mod(a1, m_two64, a2); mod(b1, m_two64, b2); - uint64 v = get_uint64(a2) ^ get_uint64(b2); + uint64_t v = get_uint64(a2) ^ get_uint64(b2); set(tmp, v); mul(tmp, m, tmp); add(c, tmp, c); // c += m * v @@ -1151,7 +1151,7 @@ template void mpz_manager::bitwise_not(unsigned sz, mpz const & a, mpz & c) { SASSERT(is_nonneg(a)); if (is_small(a) && sz <= 63) { - int64 mask = (static_cast(1) << sz) - static_cast(1); + int64_t mask = (static_cast(1) << sz) - static_cast(1); set_i64(c, (~ i64(a)) & mask); } else { @@ -1161,11 +1161,11 @@ void mpz_manager::bitwise_not(unsigned sz, mpz const & a, mpz & c) { set(c, 0); while (sz > 0) { mod(a1, m_two64, a2); - uint64 n = get_uint64(a2); - uint64 v = ~n; + uint64_t n = get_uint64(a2); + uint64_t v = ~n; SASSERT(~v == n); if (sz < 64) { - uint64 mask = (1ull << static_cast(sz)) - 1ull; + uint64_t mask = (1ull << static_cast(sz)) - 1ull; v = mask & v; } TRACE("bitwise_not", tout << "sz: " << sz << ", v: " << v << ", n: " << n << "\n";); @@ -1265,7 +1265,7 @@ bool mpz_manager::is_uint64(mpz const & a) const { return false; if (is_small(a)) return true; - if (sizeof(digit_t) == sizeof(uint64)) { + if (sizeof(digit_t) == sizeof(uint64_t)) { return size(a) <= 1; } else { @@ -1286,9 +1286,9 @@ bool mpz_manager::is_int64(mpz const & a) const { #ifndef _MP_GMP if (!is_abs_uint64(a)) return false; - uint64 num = big_abs_to_uint64(a); - uint64 msb = static_cast(1) << 63; - uint64 msb_val = msb & num; + uint64_t num = big_abs_to_uint64(a); + uint64_t msb = static_cast(1) << 63; + uint64_t msb_val = msb & num; if (a.m_val >= 0) { // non-negative number. return (0 == msb_val); @@ -1307,54 +1307,54 @@ bool mpz_manager::is_int64(mpz const & a) const { } template -uint64 mpz_manager::get_uint64(mpz const & a) const { +uint64_t mpz_manager::get_uint64(mpz const & a) const { if (is_small(a)) - return static_cast(a.m_val); + return static_cast(a.m_val); #ifndef _MP_GMP SASSERT(a.m_ptr->m_size > 0); return big_abs_to_uint64(a); #else // GMP version - if (sizeof(uint64) == sizeof(unsigned long)) { + if (sizeof(uint64_t) == sizeof(unsigned long)) { return mpz_get_ui(*a.m_ptr); } else { mpz_manager * _this = const_cast(this); mpz_set(_this->m_tmp, *a.m_ptr); mpz_mod(_this->m_tmp, m_tmp, m_two32); - uint64 r = static_cast(mpz_get_ui(m_tmp)); + uint64_t r = static_cast(mpz_get_ui(m_tmp)); mpz_set(_this->m_tmp, *a.m_ptr); mpz_div(_this->m_tmp, m_tmp, m_two32); - r += static_cast(mpz_get_ui(m_tmp)) << static_cast(32); + r += static_cast(mpz_get_ui(m_tmp)) << static_cast(32); return r; } #endif } template -int64 mpz_manager::get_int64(mpz const & a) const { +int64_t mpz_manager::get_int64(mpz const & a) const { if (is_small(a)) - return static_cast(a.m_val); + return static_cast(a.m_val); #ifndef _MP_GMP SASSERT(is_int64(a)); - uint64 num = big_abs_to_uint64(a); + uint64_t num = big_abs_to_uint64(a); if (a.m_val < 0) { if (num != 0 && (num << 1) == 0) return INT64_MIN; - return -static_cast(num); + return -static_cast(num); } - return static_cast(num); + return static_cast(num); #else // GMP - if (sizeof(int64) == sizeof(long) || mpz_fits_slong_p(*a.m_ptr)) { + if (sizeof(int64_t) == sizeof(long) || mpz_fits_slong_p(*a.m_ptr)) { return mpz_get_si(*a.m_ptr); } else { mpz_manager * _this = const_cast(this); mpz_mod(_this->m_tmp, *a.m_ptr, m_two32); - int64 r = static_cast(mpz_get_ui(m_tmp)); + int64_t r = static_cast(mpz_get_ui(m_tmp)); mpz_div(_this->m_tmp, *a.m_ptr, m_two32); - r += static_cast(mpz_get_si(m_tmp)) << static_cast(32); + r += static_cast(mpz_get_si(m_tmp)) << static_cast(32); return r; } #endif @@ -1370,7 +1370,7 @@ double mpz_manager::get_double(mpz const & a) const { unsigned sz = size(a); for (unsigned i = 0; i < sz; i++) { r += d * static_cast(digits(a)[i]); - if (sizeof(digit_t) == sizeof(uint64)) + if (sizeof(digit_t) == sizeof(uint64_t)) d *= static_cast(UINT64_MAX); // 64-bit version else d *= static_cast(UINT_MAX); // 32-bit version @@ -1696,7 +1696,7 @@ void mpz_manager::mul2k(mpz & a, unsigned k) { if (k == 0 || is_zero(a)) return; if (is_small(a) && k < 32) { - set_i64(a, i64(a) * (static_cast(1) << k)); + set_i64(a, i64(a) * (static_cast(1) << k)); return; } #ifndef _MP_GMP @@ -1798,9 +1798,9 @@ unsigned mpz_manager::power_of_two_multiple(mpz const & a) { if (sizeof(digit_t) == 8) { // TODO: we can remove this if after we move to MPN // In MPN the digit_t is always an unsigned integer - if (static_cast(v) % (static_cast(1) << 32) == 0) { + if (static_cast(v) % (static_cast(1) << 32) == 0) { r += 32; - v = static_cast(static_cast(v) / (static_cast(1) << 32)); + v = static_cast(static_cast(v) / (static_cast(1) << 32)); } } COUNT_DIGIT_RIGHT_ZEROS(); diff --git a/src/util/mpz.h b/src/util/mpz.h index f4c3f6f0d..92c6d0d10 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -30,7 +30,7 @@ Revision History: #include "util/mpn.h" unsigned u_gcd(unsigned u, unsigned v); -uint64 u64_gcd(uint64 u, uint64 v); +uint64_t u64_gcd(uint64_t u, uint64_t v); #ifdef _MP_GMP typedef unsigned digit_t; @@ -192,11 +192,11 @@ class mpz_manager { template void set(mpz & a, int sign, unsigned sz); - static int64 i64(mpz const & a) { return static_cast(a.m_val); } + static int64_t i64(mpz const & a) { return static_cast(a.m_val); } - void set_big_i64(mpz & c, int64 v); + void set_big_i64(mpz & c, int64_t v); - void set_i64(mpz & c, int64 v) { + void set_i64(mpz & c, int64_t v) { if (v >= INT_MIN && v <= INT_MAX) { del(c); c.m_val = static_cast(v); @@ -208,7 +208,7 @@ class mpz_manager { } } - void set_big_ui64(mpz & c, uint64 v); + void set_big_ui64(mpz & c, uint64_t v); #ifndef _MP_GMP static unsigned capacity(mpz const & c) { return c.m_ptr->m_capacity; } @@ -221,24 +221,24 @@ class mpz_manager { static bool is_abs_uint64(mpz const & a) { if (is_small(a)) return true; - if (sizeof(digit_t) == sizeof(uint64)) + if (sizeof(digit_t) == sizeof(uint64_t)) return size(a) <= 1; else return size(a) <= 2; } // CAST the absolute value into a UINT64 - static uint64 big_abs_to_uint64(mpz const & a) { + static uint64_t big_abs_to_uint64(mpz const & a) { SASSERT(is_abs_uint64(a)); SASSERT(!is_small(a)); if (a.m_ptr->m_size == 1) return digits(a)[0]; - if (sizeof(digit_t) == sizeof(uint64)) + if (sizeof(digit_t) == sizeof(uint64_t)) // 64-bit machine return digits(a)[0]; else // 32-bit machine - return ((static_cast(digits(a)[1]) << 32) | (static_cast(digits(a)[0]))); + return ((static_cast(digits(a)[1]) << 32) | (static_cast(digits(a)[0]))); } template @@ -426,8 +426,8 @@ public: void machine_div_rem(mpz const & a, mpz const & b, mpz & q, mpz & r) { STRACE("mpz", tout << "[mpz-ext] divrem(" << to_string(a) << ", " << to_string(b) << ") == ";); if (is_small(a) && is_small(b)) { - int64 _a = i64(a); - int64 _b = i64(b); + int64_t _a = i64(a); + int64_t _b = i64(b); set_i64(q, _a / _b); set_i64(r, _a % _b); } @@ -686,16 +686,16 @@ public: if (val <= INT_MAX) set(a, static_cast(val)); else - set(a, static_cast(static_cast(val))); + set(a, static_cast(static_cast(val))); } void set(mpz & a, char const * val); - void set(mpz & a, int64 val) { + void set(mpz & a, int64_t val) { set_i64(a, val); } - void set(mpz & a, uint64 val) { + void set(mpz & a, uint64_t val) { if (val < INT_MAX) { del(a); a.m_val = static_cast(val); @@ -729,9 +729,9 @@ public: bool is_int64(mpz const & a) const; - uint64 get_uint64(mpz const & a) const; + uint64_t get_uint64(mpz const & a) const; - int64 get_int64(mpz const & a) const; + int64_t get_int64(mpz const & a) const; bool is_uint(mpz const & a) const { return is_uint64(a) && get_uint64(a) < UINT_MAX; } diff --git a/src/util/mpzzp.h b/src/util/mpzzp.h index a30eff7b6..82ed55bbc 100644 --- a/src/util/mpzzp.h +++ b/src/util/mpzzp.h @@ -87,7 +87,7 @@ public: setup_p(); } - mpzzp_manager(numeral_manager & _m, uint64 p, bool prime = true): + mpzzp_manager(numeral_manager & _m, uint64_t p, bool prime = true): m_manager(_m), m_z(false) { m().set(m_p, p); @@ -120,7 +120,7 @@ public: void set_z() { m_z = true; } void set_zp(mpz const & new_p) { m_z = false; m_p_prime = true; m().set(m_p, new_p); setup_p(); } - void set_zp(uint64 new_p) { m_z = false; m_p_prime = true; m().set(m_p, new_p); setup_p(); } + void set_zp(uint64_t new_p) { m_z = false; m_p_prime = true; m().set(m_p, new_p); setup_p(); } // p = p^2 void set_p_sq() { SASSERT(!m_z); m_p_prime = false; m().mul(m_p, m_p, m_p); setup_p(); } void set_zp_swap(mpz & new_p) { SASSERT(!m_z); m().swap(m_p, new_p); setup_p(); } @@ -230,14 +230,14 @@ public: void set(mpz & a, int val) { m().set(a, val); p_normalize(a); } void set(mpz & a, unsigned val) { m().set(a, val); p_normalize(a); } void set(mpz & a, char const * val) { m().set(a, val); p_normalize(a); } - void set(mpz & a, int64 val) { m().set(a, val); p_normalize(a); } - void set(mpz & a, uint64 val) { m().set(a, val); p_normalize(a); } + void set(mpz & a, int64_t val) { m().set(a, val); p_normalize(a); } + void set(mpz & a, uint64_t val) { m().set(a, val); p_normalize(a); } void set(mpz & a, mpz const & val) { m().set(a, val); p_normalize(a); } bool is_uint64(mpz & a) const { const_cast(this)->p_normalize(a); return m().is_uint64(a); } bool is_int64(mpz & a) const { const_cast(this)->p_normalize(a); return m().is_int64(a); } - uint64 get_uint64(mpz & a) const { const_cast(this)->p_normalize(a); return m().get_uint64(a); } - int64 get_int64(mpz & a) const { const_cast(this)->p_normalize(a); return m().get_int64(a); } + uint64_t get_uint64(mpz & a) const { const_cast(this)->p_normalize(a); return m().get_uint64(a); } + int64_t get_int64(mpz & a) const { const_cast(this)->p_normalize(a); return m().get_int64(a); } double get_double(mpz & a) const { const_cast(this)->p_normalize(a); return m().get_double(a); } void power(mpz const & a, unsigned k, mpz & b) { SASSERT(is_p_normalized(a)); @@ -265,8 +265,8 @@ public: bool is_uint64(mpz const & a) const { return m().is_uint64(a); } bool is_int64(mpz const & a) const { return m().is_int64(a); } - uint64 get_uint64(mpz const & a) const { return m().get_uint64(a); } - int64 get_int64(mpz const & a) const { return m().get_int64(a); } + uint64_t get_uint64(mpz const & a) const { return m().get_uint64(a); } + int64_t get_int64(mpz const & a) const { return m().get_int64(a); } void mul2k(mpz & a, unsigned k) { m().mul2k(a, k); p_normalize(a); } void mul2k(mpz const & a, unsigned k, mpz & r) { m().mul2k(a, k, r); p_normalize(r); } diff --git a/src/util/prime_generator.cpp b/src/util/prime_generator.cpp index dbcccaaf7..6c0376e52 100644 --- a/src/util/prime_generator.cpp +++ b/src/util/prime_generator.cpp @@ -26,11 +26,11 @@ prime_generator::prime_generator() { process_next_k_numbers(128); } -void prime_generator::process_next_k_numbers(uint64 k) { - svector todo; - uint64 begin = m_primes.back() + 2; - uint64 end = begin + k; - for (uint64 i = begin; i < end; i+=2) { +void prime_generator::process_next_k_numbers(uint64_t k) { + svector todo; + uint64_t begin = m_primes.back() + 2; + uint64_t end = begin + k; + for (uint64_t i = begin; i < end; i+=2) { todo.push_back(i); } unsigned j = 1; @@ -38,7 +38,7 @@ void prime_generator::process_next_k_numbers(uint64 k) { while (!todo.empty()) { unsigned sz = m_primes.size(); for (; j < sz; j++) { - uint64 p = m_primes[j]; + uint64_t p = m_primes[j]; unsigned todo_sz = todo.size(); unsigned k1 = 0; unsigned k2 = 0; @@ -59,7 +59,7 @@ void prime_generator::process_next_k_numbers(uint64 k) { return; } } - uint64 p = m_primes.back(); + uint64_t p = m_primes.back(); p = p*p; unsigned todo_sz = todo.size(); unsigned k1 = 0; @@ -83,7 +83,7 @@ void prime_generator::finalize() { m_primes.finalize(); } -uint64 prime_generator::operator()(unsigned idx) { +uint64_t prime_generator::operator()(unsigned idx) { if (idx < m_primes.size()) return m_primes[idx]; if (idx > PRIME_LIST_MAX_SIZE) @@ -109,14 +109,14 @@ prime_iterator::prime_iterator(prime_generator * g):m_idx(0) { } } -uint64 prime_iterator::next() { +uint64_t prime_iterator::next() { unsigned idx = m_idx; m_idx++; if (!m_global) { return (*m_generator)(idx); } else { - uint64 r; + uint64_t r; #pragma omp critical (prime_iterator) { r = (*m_generator)(idx); diff --git a/src/util/prime_generator.h b/src/util/prime_generator.h index 2e16ebfbe..bd388954c 100644 --- a/src/util/prime_generator.h +++ b/src/util/prime_generator.h @@ -32,11 +32,11 @@ public: \brief Prime generator */ class prime_generator { - svector m_primes; - void process_next_k_numbers(uint64 k); + svector m_primes; + void process_next_k_numbers(uint64_t k); public: prime_generator(); - uint64 operator()(unsigned idx); + uint64_t operator()(unsigned idx); void finalize(); }; @@ -46,7 +46,7 @@ class prime_iterator { bool m_global; public: prime_iterator(prime_generator * g = nullptr); - uint64 next(); + uint64_t next(); static void finalize(); /* ADD_FINALIZER('prime_iterator::finalize();') diff --git a/src/util/rational.h b/src/util/rational.h index 392a1982b..dc7b79419 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -59,10 +59,10 @@ public: explicit rational(char const * v) { m().set(m_val, v); } struct i64 {}; - rational(int64 i, i64) { m().set(m_val, i); } + rational(int64_t i, i64) { m().set(m_val, i); } struct ui64 {}; - rational(uint64 i, ui64) { m().set(m_val, i); } + rational(uint64_t i, ui64) { m().set(m_val, i); } ~rational() { m().del(m_val); } @@ -98,9 +98,9 @@ public: bool is_int64() const { return m().is_int64(m_val); } - uint64 get_uint64() const { return m().get_uint64(m_val); } + uint64_t get_uint64() const { return m().get_uint64(m_val); } - int64 get_int64() const { return m().get_int64(m_val); } + int64_t get_int64() const { return m().get_int64(m_val); } bool is_unsigned() const { return is_uint64() && (get_uint64() < (1ull << 32)); } @@ -113,7 +113,7 @@ public: if (is_small() && is_int()) return true; // we don't assume that if it is small, then it is int32. if (!is_int64()) return false; - int64 v = get_int64(); + int64_t v = get_int64(); return INT_MIN <= v && v <= INT_MAX; } diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index e625cab95..e3afd0d92 100644 --- a/src/util/rlimit.cpp +++ b/src/util/rlimit.cpp @@ -26,7 +26,7 @@ reslimit::reslimit(): m_limit(0) { } -uint64 reslimit::count() const { +uint64_t reslimit::count() const { return m_count; } @@ -41,7 +41,7 @@ bool reslimit::inc(unsigned offset) { } void reslimit::push(unsigned delta_limit) { - uint64 new_limit = delta_limit + m_count; + uint64_t new_limit = delta_limit + m_count; if (new_limit <= m_count) { new_limit = 0; } diff --git a/src/util/rlimit.h b/src/util/rlimit.h index 0c81f9449..60d26be7f 100644 --- a/src/util/rlimit.h +++ b/src/util/rlimit.h @@ -24,9 +24,9 @@ Revision History: class reslimit { volatile unsigned m_cancel; bool m_suspend; - uint64 m_count; - uint64 m_limit; - svector m_limits; + uint64_t m_count; + uint64_t m_limit; + svector m_limits; ptr_vector m_children; void set_cancel(unsigned f); @@ -41,7 +41,7 @@ public: bool inc(); bool inc(unsigned offset); - uint64 count() const; + uint64_t count() const; bool get_cancel_flag() const { return m_cancel > 0 && !m_suspend; } diff --git a/src/util/s_integer.h b/src/util/s_integer.h index 658ae8eea..80310368d 100644 --- a/src/util/s_integer.h +++ b/src/util/s_integer.h @@ -46,9 +46,9 @@ public: s_integer(const s_integer & r):m_val(r.m_val) {} explicit s_integer(int n):m_val(n) {} struct i64 {}; - explicit s_integer(int64 i, i64):m_val(static_cast(i)) {} + explicit s_integer(int64_t i, i64):m_val(static_cast(i)) {} struct ui64 {}; - explicit s_integer(uint64 i, ui64):m_val(static_cast(i)) {} + explicit s_integer(uint64_t i, ui64):m_val(static_cast(i)) {} explicit s_integer(const char * str); explicit s_integer(const rational & r):m_val(static_cast(r.get_int64())) {} @@ -60,8 +60,8 @@ public: static bool is_int64() { return true; } static bool is_uint64() { return true; } int get_int() const { return m_val; } - int64 get_int64() const { return m_val; } - uint64 get_uint64() const { return m_val; } + int64_t get_int64() const { return m_val; } + uint64_t get_uint64() const { return m_val; } static bool is_unsigned() { return true; } unsigned get_unsigned() const { return static_cast(m_val); } s_integer const& get_s_integer() const { return *this; } diff --git a/src/util/total_order.h b/src/util/total_order.h index a309b63a1..44ab6f749 100644 --- a/src/util/total_order.h +++ b/src/util/total_order.h @@ -35,7 +35,7 @@ class total_order { struct cell { cell * m_next; cell * m_prev; - uint64 m_val; + uint64_t m_val; T m_data; }; @@ -53,11 +53,11 @@ class total_order { m_base.m_val = 0; } - uint64 v(cell * a) const { return a->m_val; } + uint64_t v(cell * a) const { return a->m_val; } - uint64 vb(cell * a) const { return v(a) - v(base()); } + uint64_t vb(cell * a) const { return v(a) - v(base()); } - uint64 vbn(cell * a) const { return a->m_next == base() ? UINT64_MAX : vb(a->m_next); } + uint64_t vbn(cell * a) const { return a->m_next == base() ? UINT64_MAX : vb(a->m_next); } cell * mk_cell(T const & a) { SASSERT(!m_map.contains(a)); @@ -84,18 +84,18 @@ class total_order { } void _insert_after(cell * a, cell * b) { - uint64 vb_a = vb(a); - uint64 vbn_a = vbn(a); + uint64_t vb_a = vb(a); + uint64_t vbn_a = vbn(a); SASSERT(vb_a < vbn_a); if (vbn_a < 2 || (vb_a > vbn_a - 2)) { TRACE("total_order", tout << "relabeling...\n"; tout << "\n";); - uint64 v0 = v(a); - unsigned sz = size(); - uint64 ideal_gap = UINT64_MAX / sz; - uint64 goal_gap = ideal_gap / 32; - cell * c = a->m_next->m_next; - unsigned j = 2; - uint64 curr_gap = (v(c) - v0) / j; + uint64_t v0 = v(a); + unsigned sz = size(); + uint64_t ideal_gap = UINT64_MAX / sz; + uint64_t goal_gap = ideal_gap / 32; + cell * c = a->m_next->m_next; + unsigned j = 2; + uint64_t curr_gap = (v(c) - v0) / j; while (j < sz && curr_gap < goal_gap) { j++; c = c->m_next; @@ -105,7 +105,7 @@ class total_order { if (j == sz) curr_gap = ideal_gap; c = a->m_next; - uint64 inc = curr_gap; + uint64_t inc = curr_gap; for (unsigned i = 0; i < j; i++) { c->m_val = v0 + inc; c = c->m_next; @@ -116,7 +116,7 @@ class total_order { vbn_a = vbn(a); } SASSERT(vb_a <= vbn_a - 2); - uint64 vb_b = vb_a + ((vbn_a - vb_a)/2); + uint64_t vb_b = vb_a + ((vbn_a - vb_a)/2); SASSERT(vb_b > vb_a); SASSERT(vb_b < vbn_a); b->m_val = vb_b + v(base()); diff --git a/src/util/util.cpp b/src/util/util.cpp index 0b58419f8..8ffa89877 100644 --- a/src/util/util.cpp +++ b/src/util/util.cpp @@ -80,7 +80,7 @@ unsigned log2(unsigned v) { return r; } -unsigned uint64_log2(uint64 v) { +unsigned uint64_log2(uint64_t v) { unsigned r = 0; if (v & 0xFFFFFFFF00000000ull) { v >>= 32; diff --git a/src/util/util.h b/src/util/util.h index ad427dfaf..3fc6f6510 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -29,23 +29,11 @@ Revision History: #define SIZE_MAX std::numeric_limits::max() #endif -#ifndef uint64 -typedef unsigned long long uint64; -#endif - -static_assert(sizeof(uint64) == 8, "64 bits please"); - -#ifndef int64 -typedef long long int64; -#endif - -static_assert(sizeof(int64) == 8, "64 bits"); - #ifndef INT64_MIN -#define INT64_MIN static_cast(0x8000000000000000ull) +#define INT64_MIN static_cast(0x8000000000000000ull) #endif #ifndef INT64_MAX -#define INT64_MAX static_cast(0x7fffffffffffffffull) +#define INT64_MAX static_cast(0x7fffffffffffffffull) #endif #ifndef UINT64_MAX #define UINT64_MAX 0xffffffffffffffffull @@ -110,7 +98,7 @@ inline unsigned next_power_of_two(unsigned v) { \brief Return the position of the most significant bit. */ unsigned log2(unsigned v); -unsigned uint64_log2(uint64 v); +unsigned uint64_log2(uint64_t v); static_assert(sizeof(unsigned) == 4, "unsigned are 32 bits"); @@ -136,11 +124,11 @@ static inline unsigned get_num_1bits(unsigned v) { // Remark: on gcc, the operators << and >> do not produce zero when the second argument >= 64. // So, I'm using the following two definitions to fix the problem -static inline uint64 shift_right(uint64 x, uint64 y) { +static inline uint64_t shift_right(uint64_t x, uint64_t y) { return y < 64ull ? (x >> y) : 0ull; } -static inline uint64 shift_left(uint64 x, uint64 y) { +static inline uint64_t shift_left(uint64_t x, uint64_t y) { return y < 64ull ? (x << y) : 0ull; }