From cd12fa8461a9c2e973e95168abeb69c8c94fb10b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 15 Sep 2014 20:00:45 -0700 Subject: [PATCH] adding fixed size bit-vectors Signed-off-by: Nikolaj Bjorner --- src/test/fixed_bit_vector.cpp | 118 ++++++++++++++++++++++++++ src/test/main.cpp | 1 + src/util/fixed_bit_vector.cpp | 151 ++++++++++++++++++++++++++++++++++ src/util/fixed_bit_vector.h | 118 ++++++++++++++++++++++++++ 4 files changed, 388 insertions(+) create mode 100644 src/test/fixed_bit_vector.cpp create mode 100644 src/util/fixed_bit_vector.cpp create mode 100644 src/util/fixed_bit_vector.h diff --git a/src/test/fixed_bit_vector.cpp b/src/test/fixed_bit_vector.cpp new file mode 100644 index 000000000..01d60c347 --- /dev/null +++ b/src/test/fixed_bit_vector.cpp @@ -0,0 +1,118 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + fixed_bit_vector.cpp + +Abstract: + + Test fixed-size bit vector module + +Author: + + Nikolaj Bjorner (nbjorner) 2014-9-15. + +Revision History: + + based on bit_vector.cpp + +--*/ +#include +#include +#include"fixed_bit_vector.h" +#include"vector.h" + + +static void tst1() { + fixed_bit_vector_manager m(30); + fixed_bit_vector *b; + b = m.allocate0(); + b->set(0, true); + b->set(1, false); + b->set(2, true); + SASSERT(b->get(0) == true); + SASSERT(b->get(1) == false); + SASSERT(b->get(2) == true); + SASSERT(b->get(3) == false); + SASSERT(b->get(29) == false); + m.deallocate(b); +} + +static void tst_or() { + { + fixed_bit_vector_manager m(10); + fixed_bit_vector *b1, *b2; + b1 = m.allocate0(); + b2 = m.allocate0(); + + b1->set(4); + b2->set(8); + b2->set(3); + b2->set(2); + b2->set(1); + m.display(std::cout, *b1) << "\n"; + m.display(std::cout, *b2) << "\n"; + m.set_or(*b1, *b2); + m.display(std::cout, *b1) << "\n"; + SASSERT(!m.equals(*b1, *b2)); + b1->unset(4); + SASSERT(m.equals(*b1, *b2)); + b1->unset(3); + SASSERT(!m.equals(*b1, *b2)); + m.deallocate(b1); + m.deallocate(b2); + } +} + +static void tst_and() { + +} + + + +static void tst_eq(unsigned num_bits) { + fixed_bit_vector_manager m(num_bits); + fixed_bit_vector* b1 = m.allocate0(); + fixed_bit_vector* b2 = m.allocate0(); + fixed_bit_vector* b3 = m.allocate0(); + + b1->set(3, true); + SASSERT(!m.equals(*b1, *b2)); + SASSERT(m.equals(*b2, *b3)); + + b3->set(3, true); + SASSERT(m.equals(*b1, *b3)); + + b2->set(num_bits-1, true); + b3->set(num_bits-1); + b3->unset(3); + SASSERT(m.equals(*b2, *b3)); + m.fill0(*b1); + m.set_neg(*b1); + m.fill1(*b2); + SASSERT(m.equals(*b1, *b2)); + m.fill0(*b1); + for (unsigned i = 0; i < num_bits; ++i) { + b1->set(i, true); + } + SASSERT(m.equals(*b1, *b2)); + m.deallocate(b1); + m.deallocate(b2); + m.deallocate(b3); +} + +void tst_fixed_bit_vector() { + tst1(); + tst_or(); + tst_and(); + tst_eq(15); + tst_eq(16); + tst_eq(17); + tst_eq(31); + tst_eq(32); + tst_eq(33); + tst_eq(63); + tst_eq(64); + tst_eq(65); +} diff --git a/src/test/main.cpp b/src/test/main.cpp index d97a94a16..e58845bcf 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -140,6 +140,7 @@ int main(int argc, char ** argv) { TST(ast); TST(optional); TST(bit_vector); + TST(fixed_bit_vector); TST(string_buffer); TST(map); TST(diff_logic); diff --git a/src/util/fixed_bit_vector.cpp b/src/util/fixed_bit_vector.cpp new file mode 100644 index 000000000..c674bafda --- /dev/null +++ b/src/util/fixed_bit_vector.cpp @@ -0,0 +1,151 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + fixed_bit_vector.cpp + +Abstract: + + Simple bitvector implementation for fixed size bit-vectors. + +Author: + + Nikolaj Bjorner (nbjorner) 2014-9-15. + Leonardo de Moura (leonardo) 2006-10-03. + +Revision History: + Based on bit_vector.cpp + +--*/ + +#include +#include"fixed_bit_vector.h" +#include"trace.h" +#include"hash.h" + + +fixed_bit_vector_manager::fixed_bit_vector_manager(unsigned num_bits): + m_alloc("fixed_bit_vector") { + m_num_bits = num_bits; + m_num_words = num_words(num_bits); + m_num_bytes = m_num_words * sizeof(unsigned); + unsigned bit_rest = m_num_bits % 32; + m_mask = (1U << bit_rest) - 1; + if (m_mask == 0) m_mask = UINT_MAX; +} + + +fixed_bit_vector* fixed_bit_vector_manager::allocate() { + return static_cast(m_alloc.allocate(m_num_bytes)); +} + +fixed_bit_vector* fixed_bit_vector_manager::allocate0() { + fixed_bit_vector* result = allocate(); + fill0(*result); + return result; +} + +fixed_bit_vector* fixed_bit_vector_manager::allocate1() { + fixed_bit_vector* result = allocate(); + fill1(*result); + return result; +} + +fixed_bit_vector* fixed_bit_vector_manager::allocate(fixed_bit_vector& bv) { + fixed_bit_vector* result = allocate(); + copy(*result, bv); + return result; +} + +void fixed_bit_vector_manager::deallocate(fixed_bit_vector* bv) { + m_alloc.deallocate(m_num_bytes, bv); +} + + +void fixed_bit_vector_manager::copy(fixed_bit_vector& dst, fixed_bit_vector const& src) const { + memcpy(dst.m_data, src.m_data, num_bytes()); +} + + +fixed_bit_vector& +fixed_bit_vector_manager::fill0(fixed_bit_vector& bv) const { + memset(bv.m_data, 0, num_bytes()); + return bv; +} + +fixed_bit_vector& +fixed_bit_vector_manager::fill1(fixed_bit_vector& bv) const { + memset(bv.m_data, 0xFF, num_bytes()); + return bv; +} + +fixed_bit_vector& +fixed_bit_vector_manager::set_and(fixed_bit_vector& dst, fixed_bit_vector const& src) const { + for (unsigned i = 0; i < m_num_words; i++) + dst.m_data[i] &= src.m_data[i]; + return dst; +} + +fixed_bit_vector& +fixed_bit_vector_manager::set_or(fixed_bit_vector& dst, fixed_bit_vector const& src) const { + for (unsigned i = 0; i < m_num_words; i++) + dst.m_data[i] |= src.m_data[i]; + return dst; +} + +fixed_bit_vector& +fixed_bit_vector_manager::set_neg(fixed_bit_vector& dst) const { + for (unsigned i = 0; i < m_num_words; i++) + dst.m_data[i] = ~dst.m_data[i]; + return dst; +} + +unsigned fixed_bit_vector_manager::last_word(fixed_bit_vector const& bv) const { + unsigned n = num_words(); + if (n == 0) return 0; + return bv.m_data[n-1] & m_mask; +} + +bool fixed_bit_vector_manager::equals(fixed_bit_vector const& a, fixed_bit_vector const& b) const { + if (&a == &b) return true; + unsigned n = num_words(); + if (n == 0) + return true; + for (unsigned i = 0; i < n - 1; i++) { + if (a.m_data[i] != b.m_data[i]) + return false; + } + return last_word(a) == last_word(b); +} +unsigned fixed_bit_vector_manager::hash(fixed_bit_vector const& src) const { + return string_hash(reinterpret_cast(src.m_data), num_bits()/8, num_bits()); +} + +bool fixed_bit_vector_manager::contains(fixed_bit_vector const& a, fixed_bit_vector const& b) const { + unsigned n = num_words(); + if (n == 0) + return true; + + for (unsigned i = 0; i < n - 1; ++i) { + if ((a.m_data[i] & b.m_data[i]) != b.m_data[i]) + return false; + } + unsigned b_data = last_word(b); + return (last_word(a) & b_data) == b_data; +} + +std::ostream& fixed_bit_vector_manager::display(std::ostream& out, fixed_bit_vector const& b) const { + unsigned i = num_bits(); + while (i > 0) { + --i; + if (b.get(i)) + out << "1"; + else + out << "0"; + } + return out; +} + + + diff --git a/src/util/fixed_bit_vector.h b/src/util/fixed_bit_vector.h new file mode 100644 index 000000000..636c03e1b --- /dev/null +++ b/src/util/fixed_bit_vector.h @@ -0,0 +1,118 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + fixed_bit_vector.h + +Abstract: + + Simple bitvector implementation for fixed size bit-vectors. + +Author: + + Nikolaj Bjorner (nbjorner) 2014-9-15. + +Revision History: + + Related to bit_vector, but is based on a manager. + +--*/ +#ifndef _FIXED_BIT_VECTOR_H_ +#define _FIXED_BIT_VECTOR_H_ + +#include +#include"debug.h" +#include"small_object_allocator.h" + +class fixed_bit_vector; +class fixed_bit_vector_manager { + friend class fixed_bit_vector; + small_object_allocator m_alloc; + unsigned m_num_bits; + unsigned m_num_bytes; + unsigned m_num_words; + unsigned m_mask; + unsigned num_bytes() const { return m_num_bytes; } + + static unsigned num_words(unsigned num_bits) { + return (num_bits + 31) / 32; + } + +public: + fixed_bit_vector_manager(unsigned num_bits); + + fixed_bit_vector* allocate(); + fixed_bit_vector* allocate1(); + fixed_bit_vector* allocate0(); + fixed_bit_vector* allocate(fixed_bit_vector& bv); + void deallocate(fixed_bit_vector* bv); + + void copy(fixed_bit_vector& dst, fixed_bit_vector const& src) const; + unsigned num_words() const { return m_num_words; } + unsigned num_bits() const { return m_num_bits; } + fixed_bit_vector& reset(fixed_bit_vector& bv) const { return fill0(bv); } + fixed_bit_vector& fill0(fixed_bit_vector& bv) const; + fixed_bit_vector& fill1(fixed_bit_vector& bv) const; + fixed_bit_vector& set_and(fixed_bit_vector& dst, fixed_bit_vector const& src) const; + fixed_bit_vector& set_or(fixed_bit_vector& dst, fixed_bit_vector const& src) const; + fixed_bit_vector& set_neg(fixed_bit_vector& dst) const; + unsigned last_word(fixed_bit_vector const& bv) const; + bool equals(fixed_bit_vector const& a, fixed_bit_vector const& b) const; + unsigned hash(fixed_bit_vector const& src) const; + bool contains(fixed_bit_vector const& a, fixed_bit_vector const& b) const; + std::ostream& display(std::ostream& out, fixed_bit_vector const& b) const; +}; + +class fixed_bit_vector { + friend class fixed_bit_vector_manager; + unsigned m_data[1]; + + static unsigned get_pos_mask(unsigned bit_idx) { + return 1 << (bit_idx % 32); + } + + + unsigned get_bit_word(unsigned bit_idx) const { + return m_data[bit_idx / 32]; + } + + unsigned & get_bit_word(unsigned bit_idx) { + return m_data[bit_idx / 32]; + } + +public: + + fixed_bit_vector() {} + + ~fixed_bit_vector() {} + + unsigned get_word(unsigned word_idx) const { return m_data[word_idx]; } + + bool operator[](unsigned bit_idx) const { + return get(bit_idx); + } + + bool get(unsigned bit_idx) const { + return (get_bit_word(bit_idx) & get_pos_mask(bit_idx)) != 0; + } + + void set(unsigned bit_idx) { + get_bit_word(bit_idx) |= get_pos_mask(bit_idx); + } + + void unset(unsigned bit_idx) { + get_bit_word(bit_idx) &= ~get_pos_mask(bit_idx); + } + + void set(unsigned bit_idx, bool val) { + int _val = static_cast(val); + get_bit_word(bit_idx) ^= (-_val ^ get_bit_word(bit_idx)) & get_pos_mask(bit_idx); + } + +}; + + + +#endif /* _FIXED_BIT_VECTOR_H_ */ +