Commit 5a3b1a99 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

bitvect: implement a dynamic bit-vector class.

* src/misc/bitvect.cc, src/misc/bitvect.hh: New files.
* src/misc/Makefile.am: Add them.
* src/tgbatest/bitvect.cc, src/tgbatest/bitvect.test: New files.
* src/tgbatest/Makefile.am: Add them.
parent dfc5ff95
......@@ -33,6 +33,7 @@ misc_HEADERS = \
bareword.hh \
bddlt.hh \
bddop.hh \
bitvect.hh \
casts.hh \
common.hh \
escape.hh \
......@@ -59,6 +60,7 @@ noinst_LTLIBRARIES = libmisc.la
libmisc_la_SOURCES = \
bareword.cc \
bddop.cc \
bitvect.cc \
escape.cc \
formater.cc \
intvcomp.cc \
......
// -*- coding: utf-8 -*-
// Copyright (C) 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#ifdef HAVE_CONFIG_H
# include "config.h"
#endif
#include "bitvect.hh"
#include <new>
#include <iostream>
#include <cmath>
#include <hashfunc.hh>
#include <cstring>
namespace spot
{
namespace
{
// How many block_t do we need to store BITCOUNT bits?
size_t block_needed(size_t bitcount)
{
const size_t bpb = 8 * sizeof(bitvect::block_t);
size_t n = (bitcount + bpb - 1) / bpb;
if (n < 1)
return 1;
return n;
}
// Fowler–Noll–Vo hash parameters for 64bits
template<int numbytes>
struct fnv
{
static unsigned long init()
{
return 14695981039346656037UL;
}
static unsigned long prime()
{
return 1099511628211UL;
}
};
// Fowler–Noll–Vo hash parameters for 32bits
template<>
struct fnv<4>
{
static unsigned int init()
{
return 2166136261U;
}
static unsigned int prime()
{
return 16777619U;
}
};
}
bitvect::bitvect(size_t size, size_t block_count):
size_(size),
block_count_(block_count),
storage_(&local_storage_)
{
clear_all();
}
bitvect::bitvect(size_t size, size_t block_count, bool):
size_(size),
block_count_(block_count),
storage_(&local_storage_)
{
}
bitvect* bitvect::clone() const
{
size_t n = block_needed(size_);
// Allocate some memory for the bitvect. The instance
// already contains one int of local_storage_, but
// we allocate n-1 more so that we store the table.
void* mem = operator new(sizeof(bitvect)
+ (n - 1) * sizeof(bitvect::block_t));
bitvect* res = new(mem) bitvect(size_, n, true);
memcpy(res->storage_, storage_, res->block_count_ * sizeof(block_t));
return res;
}
size_t bitvect::hash() const
{
block_t res = fnv<sizeof(block_t)>::init();
size_t i;
for (i = 0; i < block_count_ - 1; ++i)
{
res ^= storage_[i];
res *= fnv<sizeof(block_t)>::prime();
}
// Deal with the last block, that might not be fully used.
// Compute the number n of bits used in the last block.
const size_t bpb = 8 * sizeof(bitvect::block_t);
size_t n = size() % bpb;
// Use only the least n bits from storage_[i].
res ^= storage_[i] & ((1UL << n) - 1);
return res;
}
bitvect* make_bitvect(size_t bitcount)
{
size_t n = block_needed(bitcount);
// Allocate some memory for the bitvect. The instance
// already contains one int of local_storage_, but
// we allocate n-1 more so that we store the table.
void* mem = operator new(sizeof(bitvect)
+ (n - 1) * sizeof(bitvect::block_t));
return new(mem) bitvect(bitcount, n);
}
bitvect_array* make_bitvect_array(size_t bitcount, size_t vectcount)
{
size_t n = block_needed(bitcount);
// Size of one bitvect.
size_t bvsize = sizeof(bitvect) + (n - 1) * sizeof(bitvect::block_t);
// Allocate the bitvect_array with enough space at the end
// to store all bitvect instances.
void* mem = operator new(sizeof(bitvect_array) + bvsize * vectcount);
bitvect_array* bva = new(mem) bitvect_array(vectcount, bvsize);
// Initialize all the bitvect instances.
for (size_t i = 0; i < vectcount; ++i)
new(bva->storage_ + i * bvsize) bitvect(bitcount, n);
return bva;
}
std::ostream& operator<<(std::ostream& os , const bitvect& v)
{
for (size_t i = 0, end = v.size(); i != end; ++i)
os << (v.get(i) ? '1' : '0');
return os;
}
std::ostream& operator<<(std::ostream& os , const bitvect_array& a)
{
size_t end = a.size();
if (end == 0)
{
os << "empty\n";
return os;
}
int w = floor(log10(end - 1)) + 1;
for (size_t i = 0; i != end; ++i)
{
os.width(w);
os << i;
os.width(1);
os << ": " << a.at(i) << "\n";
}
return os;
}
}
This diff is collapsed.
......@@ -31,6 +31,7 @@ check_SCRIPTS = defs
# Keep this sorted alphabetically.
check_PROGRAMS = \
bddprod \
bitvect \
complement \
explicit \
explicit2 \
......@@ -48,6 +49,7 @@ check_PROGRAMS = \
# Keep this sorted alphabetically.
bddprod_SOURCES = ltlprod.cc
bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT
bitvect_SOURCES = bitvect.cc
complement_SOURCES = complementation.cc
explicit_SOURCES = explicit.cc
explicit2_SOURCES = explicit2.cc
......@@ -69,6 +71,7 @@ tripprod_SOURCES = tripprod.cc
# because such failures will be easier to diagnose and fix.
TESTS = \
intvcomp.test \
bitvect.test \
eltl2tgba.test \
explicit.test \
explicit2.test \
......
// -*- coding: utf-8 -*-
// Copyright (C) 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include <iostream>
#include "misc/bitvect.hh"
void ruler()
{
std::cout << "\n ";
for (size_t x = 0; x < 76; ++x)
if (x % 10 == 0)
std::cout << x / 10;
else
std::cout << "_";
std::cout << "\n ";
for (size_t x = 0; x < 76; ++x)
std::cout << x % 10;
std::cout << "\n\n";
}
#define ECHO(name) std::cout << #name": " << *name << "\n"
int main()
{
ruler();
spot::bitvect* v = spot::make_bitvect(15);
ECHO(v);
v->set(10);
v->set(7);
v->set(12);
ECHO(v);
ruler();
spot::bitvect* w = spot::make_bitvect(42);
w->set(30);
w->set(41);
w->set(13);
w->set(7);
ECHO(w);
*w ^= *v;
ECHO(w);
ruler();
spot::bitvect* x = spot::make_bitvect(75);
x->set(70);
x->set(60);
ECHO(x);
*x |= *w;
ECHO(x);
for (size_t i = 0; i < 30; ++i)
w->push_back((i & 3) == 0);
ECHO(w);
*x &= *w;
ECHO(x);
x->set_all();
ECHO(x);
ruler();
w->push_back(0x09, 4);
ECHO(w);
spot::bitvect* y = w->extract_range(0, 71);
ECHO(y);
delete y;
y = w->extract_range(0, 64);
ECHO(y);
delete y;
y = w->extract_range(64, 75);
ECHO(y);
delete y;
y = w->extract_range(0, 75);
ECHO(y);
delete y;
y = w->extract_range(7, 64);
ECHO(y);
delete y;
y = w->extract_range(7, 72);
ECHO(y);
delete y;
delete v;
delete w;
delete x;
ruler();
spot::bitvect_array* a = spot::make_bitvect_array(60, 10);
for (size_t y = 0; y < a->size(); ++y)
for (size_t x = 0; x < 60; ++x)
{
if (((x ^ y) & 3) < 2)
a->at(y).set(x);
}
std::cout << *a;
ruler();
for (size_t i = 0; i < 12; ++i)
a->at(4).push_back((i & 2) == 0);
a->at(6) = a->at(4);
a->at(8) = a->at(7);
a->at(6) ^= a->at(8);
std::cout << *a;
std::cout << "Comp: "
<< (a->at(0) == a->at(1))
<< (a->at(0) == a->at(2))
<< (a->at(1) != a->at(2))
<< (a->at(0) < a->at(2))
<< (a->at(0) > a->at(2))
<< (a->at(3) < a->at(4))
<< (a->at(5) > a->at(6)) << std::endl;
delete a;
}
#!/bin/sh
# Copyright (C) 2013 Laboratoire de Recherche et Dveloppement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 3 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
. ./defs
set -e
run 0 ../bitvect | tee stderr
cat >expected <<EOF
0_________1_________2_________3_________4_________5_________6_________7_____
0123456789012345678901234567890123456789012345678901234567890123456789012345
v: 000000000000000
v: 000000010010100
0_________1_________2_________3_________4_________5_________6_________7_____
0123456789012345678901234567890123456789012345678901234567890123456789012345
w: 000000010000010000000000000000100000000001
w: 000000000010110000000000000000100000000001
0_________1_________2_________3_________4_________5_________6_________7_____
0123456789012345678901234567890123456789012345678901234567890123456789012345
x: 000000000000000000000000000000000000000000000000000000000000100000000010000
x: 000000000010110000000000000000100000000001000000000000000000100000000010000
w: 000000000010110000000000000000100000000001100010001000100010001000100010
x: 000000000010110000000000000000100000000001000000000000000000000000000010000
x: 111111111111111111111111111111111111111111111111111111111111111111111111111
0_________1_________2_________3_________4_________5_________6_________7_____
0123456789012345678901234567890123456789012345678901234567890123456789012345
w: 0000000000101100000000000000001000000000011000100010001000100010001000101001
y: 00000000001011000000000000000010000000000110001000100010001000100010001
y: 0000000000101100000000000000001000000000011000100010001000100010
y: 00100010100
y: 000000000010110000000000000000100000000001100010001000100010001000100010100
y: 000101100000000000000001000000000011000100010001000100010
y: 00010110000000000000000100000000001100010001000100010001000100010
0_________1_________2_________3_________4_________5_________6_________7_____
0123456789012345678901234567890123456789012345678901234567890123456789012345
0: 110011001100110011001100110011001100110011001100110011001100
1: 110011001100110011001100110011001100110011001100110011001100
2: 001100110011001100110011001100110011001100110011001100110011
3: 001100110011001100110011001100110011001100110011001100110011
4: 110011001100110011001100110011001100110011001100110011001100
5: 110011001100110011001100110011001100110011001100110011001100
6: 001100110011001100110011001100110011001100110011001100110011
7: 001100110011001100110011001100110011001100110011001100110011
8: 110011001100110011001100110011001100110011001100110011001100
9: 110011001100110011001100110011001100110011001100110011001100
0_________1_________2_________3_________4_________5_________6_________7_____
0123456789012345678901234567890123456789012345678901234567890123456789012345
0: 110011001100110011001100110011001100110011001100110011001100
1: 110011001100110011001100110011001100110011001100110011001100
2: 001100110011001100110011001100110011001100110011001100110011
3: 001100110011001100110011001100110011001100110011001100110011
4: 110011001100110011001100110011001100110011001100110011001100110011001100
5: 110011001100110011001100110011001100110011001100110011001100
6: 111111111111111111111111111111111111111111111111111111111111110011001100
7: 001100110011001100110011001100110011001100110011001100110011
8: 001100110011001100110011001100110011001100110011001100110011
9: 110011001100110011001100110011001100110011001100110011001100
Comp: 1011010
EOF
diff expected stderr
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment