mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source 
73aee81bfa8e0edccd25066d755ce2.
This commit is contained in:
Nikolaj Bjorner 2013-03-23 13:57:12 -07:00
commit e73c06a8b0
3 changed files with 27 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/test/bit_vector.cpp
View file

@ -276,12 +276,35 @@ static void tst_bv_reset() {
}
}
static void tst_eq() {
bit_vector b1, b2, b3;
b1.resize(32);
b2.resize(32);
b3.resize(32);
b1.set(3, true);
SASSERT(b1 != b2);
SASSERT(!(b1 == b2));
SASSERT(b2 == b3);
b3.set(3, true);
SASSERT(b1 == b3);
SASSERT(!(b1 != b3));
b2.set(31, true);
b3.set(31);
b3.unset(3);
SASSERT(b2 == b3);
SASSERT(!(b2 != b3));
}
void tst_bit_vector() {
tst_crash();
tst_shift();
tst_or();
tst_and();
tst_bv_reset();
tst_eq();
return;
tst2();
for (unsigned i = 0; i < 20; i++) {

3
src/util/bit_vector.cpp
View file

@ -116,7 +116,7 @@ void bit_vector::shift_right(unsigned k) {
}
}
bool bit_vector::operator==(bit_vector const & source) {
bool bit_vector::operator==(bit_vector const & source) const {
if (m_num_bits != source.m_num_bits)
return false;
unsigned n = num_words();
@ -129,6 +129,7 @@ bool bit_vector::operator==(bit_vector const & source) {
}
unsigned bit_rest = source.m_num_bits % 32;
unsigned mask = (1 << bit_rest) - 1;
if (mask == 0) mask = UINT_MAX;
return (m_data[i] & mask) == (source.m_data[i] & mask);
}

4
src/util/bit_vector.h
View file

@ -171,9 +171,9 @@ public:
resize(sz, val);
}
bool operator==(bit_vector const & other);
bool operator==(bit_vector const & other) const;
bool operator!=(bit_vector const & other) { return !operator==(other); }
bool operator!=(bit_vector const & other) const { return !operator==(other); }
bit_vector & operator=(bit_vector const & source) {
m_num_bits = source.m_num_bits;