mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

fixes for #1296, removing COMPILE_TIME_ASSERT

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-09 13:59:44 -07:00
parent f359f23885
commit cae414e575
13 changed files with 27 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/rewriter/maximize_ac_sharing.cpp
View file

@ -54,13 +54,13 @@ br_status maximize_ac_sharing::reduce_app(func_decl * f, unsigned num_args, expr
TRACE("ac_sharing_detail", tout << "args: "; for (unsigned i = 0; i < num_args; i++) tout << mk_pp(_args[i], m) << "\n";);
try_to_reuse:
if (num_args > 1 && num_args < MAX_NUM_ARGS_FOR_OPT) {
for (unsigned i = 0; i < num_args - 1; i++) {
for (unsigned i = 0; i + 1 < num_args; i++) {
for (unsigned j = i + 1; j < num_args; j++) {
if (contains(f, _args[i], _args[j])) {
TRACE("ac_sharing_detail", tout << "reusing args: " << i << " " << j << "\n";);
_args[i] = m.mk_app(f, _args[i], _args[j]);
SASSERT(num_args > 1);
for (unsigned w = j; w < num_args - 1; w++) {
for (unsigned w = j; w + 1 < num_args; w++) {
_args[w] = _args[w+1];
}
num_args--;
@ -144,6 +144,7 @@ void maximize_ac_sharing::restore_entries(unsigned old_lim) {
while (i != old_lim) {
--i;
entry * e = m_entries[i];
m_cache.remove(e);
m.dec_ref(e->m_arg1);
m.dec_ref(e->m_arg2);
}

8
src/sat/sat_watched.h
View file

@ -109,10 +109,10 @@ namespace sat {
bool operator!=(watched const & w) const { return !operator==(w); }
};
COMPILE_TIME_ASSERT(0 <= watched::BINARY && watched::BINARY <= 3);
COMPILE_TIME_ASSERT(0 <= watched::TERNARY && watched::TERNARY <= 3);
COMPILE_TIME_ASSERT(0 <= watched::CLAUSE && watched::CLAUSE <= 3);
COMPILE_TIME_ASSERT(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3);
static_assert(0 <= watched::BINARY && watched::BINARY <= 3, "");
static_assert(0 <= watched::TERNARY && watched::TERNARY <= 3, "");
static_assert(0 <= watched::CLAUSE && watched::CLAUSE <= 3, "");
static_assert(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3, "");
struct watched_lt {
bool operator()(watched const & w1, watched const & w2) const {

4
src/smt/smt_theory_var_list.h
View file

@ -67,9 +67,9 @@ namespace smt {
};
// 32 bit machine
COMPILE_TIME_ASSERT(sizeof(expr*) != 4 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int));
static_assert(sizeof(expr*) != 4 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int), "32 bit");
// 64 bit machine
COMPILE_TIME_ASSERT(sizeof(expr*) != 8 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int) + /* a structure must be aligned */ sizeof(int));
static_assert(sizeof(expr*) != 8 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int) + /* a structure must be aligned */ sizeof(int), "64 bit");
};
#endif /* SMT_THEORY_VAR_LIST_H_ */

4
src/util/approx_set.h
View file

@ -29,7 +29,7 @@ public:
static const unsigned long long zero = 0ull;
static const unsigned long long one = 1ull;
};
COMPILE_TIME_ASSERT(sizeof(unsigned long long) == 8);
static_assert(sizeof(unsigned long long) == 8, "");
template <> class approx_set_traits<unsigned> {
public:
@ -37,7 +37,7 @@ public:
static const unsigned zero = 0;
static const unsigned one = 1;
};
COMPILE_TIME_ASSERT(sizeof(unsigned) == 4);
static_assert(sizeof(unsigned) == 4, "unsigned are 4 bytes");
template<typename T, typename T2U_Proc, typename R=unsigned long long>
class approx_set_tpl : private T2U_Proc {

2
src/util/bit_vector.h
View file

@ -24,7 +24,7 @@ Revision History:
#include "util/vector.h"
#include "util/memory_manager.h"
COMPILE_TIME_ASSERT(sizeof(unsigned) == 4);
static_assert(sizeof(unsigned) == 4, "unsigned are 4 bytes");
#define BV_DEFAULT_CAPACITY 2
class bit_vector {

1
src/util/debug.h
View file

@ -90,7 +90,6 @@ bool is_debug_enabled(const char * tag);
exit(-1); \
}
#define COMPILE_TIME_ASSERT(expr) static_assert(expr, "")
void finalize_debug();
/*

2
src/util/double_manager.h
View file

@ -97,7 +97,7 @@ public:
}
};
COMPILE_TIME_ASSERT(sizeof(uint64) == sizeof(double));
static_assert(sizeof(uint64) == sizeof(double), "");
#endif /* DOUBLE_MANAGER_H_ */

6
src/util/mpf.cpp
View file

@ -73,7 +73,7 @@ mpf_manager::~mpf_manager() {
}
void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, int value) {
COMPILE_TIME_ASSERT(sizeof(int) == 4);
static_assert(sizeof(int) == 4, "assume integers are 4 bytes");
o.sign = false;
o.ebits = ebits;
@ -119,7 +119,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, double value) {
// double === mpf(11, 53)
COMPILE_TIME_ASSERT(sizeof(double) == 8);
static_assert(sizeof(double) == 8, "doubles are 8 bytes");
uint64 raw;
memcpy(&raw, &value, sizeof(double));
@ -155,7 +155,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, double value) {
void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, float value) {
// single === mpf(8, 24)
COMPILE_TIME_ASSERT(sizeof(float) == 4);
static_assert(sizeof(float) == 4, "floats are 4 bytes");
unsigned int raw;
memcpy(&raw, &value, sizeof(float));

4
src/util/mpff.cpp
View file

@ -27,8 +27,8 @@ Revision History:
#include "util/bit_util.h"
#include "util/trace.h"
COMPILE_TIME_ASSERT(sizeof(mpn_digit) == sizeof(unsigned));
COMPILE_TIME_ASSERT(sizeof(unsigned) == 4);
static_assert(sizeof(mpn_digit) == sizeof(unsigned), "");
static_assert(sizeof(unsigned) == 4, "unsigned haven't changed size for a while");
// MIN_MSW is an shorthand for 0x8000..00, i.e., the minimal most significand word.
#define MIN_MSW (1u << (sizeof(unsigned) * 8 - 1))

2
src/util/mpn.cpp
View file

@ -24,7 +24,7 @@ Revision History:
#define max(a,b) (((a) > (b)) ? (a) : (b))
typedef uint64 mpn_double_digit;
COMPILE_TIME_ASSERT(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit));
static_assert(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit), "size alignment");
const mpn_digit mpn_manager::zero = 0;

10
src/util/mpz.cpp
View file

@ -558,7 +558,7 @@ void mpz_manager<SYNCH>::big_rem(mpz const & a, mpz const & b, mpz & c) {
template<bool SYNCH>
void mpz_manager<SYNCH>::gcd(mpz const & a, mpz const & b, mpz & c) {
COMPILE_TIME_ASSERT(sizeof(a.m_val) == sizeof(int));
static_assert(sizeof(a.m_val) == sizeof(int), "size mismatch");
if (is_small(a) && is_small(b) && a.m_val != INT_MIN && b.m_val != INT_MIN) {
int _a = a.m_val;
int _b = b.m_val;
@ -724,7 +724,7 @@ void mpz_manager<SYNCH>::gcd(mpz const & a, mpz const & b, mpz & c) {
#ifdef LEHMER_GCD
// For now, it only works if sizeof(digit_t) == sizeof(unsigned)
COMPILE_TIME_ASSERT(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;
mpz a1, b1, t, r, tmp;
@ -1754,7 +1754,7 @@ void mpz_manager<SYNCH>::mul2k(mpz & a, unsigned k) {
}
#ifndef _MP_GMP
COMPILE_TIME_ASSERT(sizeof(digit_t) == 4 || sizeof(digit_t) == 8);
static_assert(sizeof(digit_t) == 4 || sizeof(digit_t) == 8, "");
#endif
template<bool SYNCH>
@ -1821,7 +1821,7 @@ unsigned mpz_manager<SYNCH>::log2(mpz const & a) {
if (is_small(a))
return ::log2((unsigned)a.m_val);
#ifndef _MP_GMP
COMPILE_TIME_ASSERT(sizeof(digit_t) == 8 || sizeof(digit_t) == 4);
static_assert(sizeof(digit_t) == 8 || sizeof(digit_t) == 4, "");
mpz_cell * c = a.m_ptr;
unsigned sz = c->m_size;
digit_t * ds = c->m_digits;
@ -1843,7 +1843,7 @@ unsigned mpz_manager<SYNCH>::mlog2(mpz const & a) {
if (is_small(a))
return ::log2((unsigned)-a.m_val);
#ifndef _MP_GMP
COMPILE_TIME_ASSERT(sizeof(digit_t) == 8 || sizeof(digit_t) == 4);
static_assert(sizeof(digit_t) == 8 || sizeof(digit_t) == 4, "");
mpz_cell * c = a.m_ptr;
unsigned sz = c->m_size;
digit_t * ds = c->m_digits;

1
src/util/uint_set.h
View file

@ -22,7 +22,6 @@ Revision History:
#include "util/util.h"
#include "util/vector.h"
COMPILE_TIME_ASSERT(sizeof(unsigned) == 4);
class uint_set : unsigned_vector {

6
src/util/util.h
View file

@ -33,13 +33,13 @@ Revision History:
typedef unsigned long long uint64;
#endif
COMPILE_TIME_ASSERT(sizeof(uint64) == 8);
static_assert(sizeof(uint64) == 8, "64 bits please");
#ifndef int64
typedef long long int64;
#endif
COMPILE_TIME_ASSERT(sizeof(int64) == 8);
static_assert(sizeof(int64) == 8, "64 bits");
#ifndef INT64_MIN
#define INT64_MIN static_cast<int64>(0x8000000000000000ull)
@ -111,7 +111,7 @@ inline unsigned next_power_of_two(unsigned v) {
unsigned log2(unsigned v);
unsigned uint64_log2(uint64 v);
COMPILE_TIME_ASSERT(sizeof(unsigned) == 4);
static_assert(sizeof(unsigned) == 4, "unsigned are 32 bits");
// Return the number of 1 bits in v.
static inline unsigned get_num_1bits(unsigned v) {