adding fixed size bit-vectors

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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<cstdlib>
+#include<iostream>
+#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);
+}

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);

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<limits.h>
+#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<fixed_bit_vector*>(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<char const* const>(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;
+}
+
+
+

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<string.h>
+#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<int>(val);
+        get_bit_word(bit_idx) ^= (-_val ^ get_bit_word(bit_idx)) & get_pos_mask(bit_idx);
+    }
+
+};
+
+
+
+#endif /* _FIXED_BIT_VECTOR_H_ */
+