bitvect.cc 5.07 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
// 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
23
#include <spot/misc/bitvect.hh>
24
25
26
27
28
#include <new>
#include <iostream>
#include <cmath>
#include <hashfunc.hh>
#include <cstring>
29
#include <climits>
30
31
32
33
34
35
36
37
38
39
40
41

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)
42
        return 1;
43
44
45
      return n;
    }

46
47
    // Fowler-Noll-Vo hash parameters.
    // Add specializations as needed.
48
49
    template<int numbytes>
    struct fnv
50
51
52
53
54
55
56
57
58
59
    {
    };

    // Do not define the following if ULONG_MAX cannot
    // hold a 64-bit value, otherwise the parser will
    // choke when parsing the constants.
#if ULONG_MAX >> 31 >> 31 >> 1 > 0
    // Fowler-Noll-Vo hash parameters for 64bits
    template<>
    struct fnv<8>
60
61
62
    {
      static unsigned long init()
      {
63
        return 14695981039346656037UL;
64
65
66
67
      }

      static unsigned long prime()
      {
68
        return 1099511628211UL;
69
70
      }
    };
71
#endif
72

73
    // Fowler-Noll-Vo hash parameters for 32bits
74
75
76
    template<>
    struct fnv<4>
    {
77
      static unsigned long init()
78
      {
79
        return 2166136261UL;
80
81
      }

82
      static unsigned long prime()
83
      {
84
        return 16777619UL;
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
      }
    };

  }

  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)
112
                             + (n - 1) * sizeof(bitvect::block_t));
113
114
115
116
117
118
119
120
121
122
    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;
123
124
125
126
    size_t m = used_blocks();
    if (m == 0)
      return res;
    for (i = 0; i < m - 1; ++i)
127
      {
128
129
        res ^= storage_[i];
        res *= fnv<sizeof(block_t)>::prime();
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
      }
    // 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)
147
                             + (n - 1) * sizeof(bitvect::block_t));
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
    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)
163
       new(bva->storage() + i * bvsize) bitvect(bitcount, n);
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
     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)
      {
179
180
        os << "empty\n";
        return os;
181
182
183
184
      }
    int w = floor(log10(end - 1)) + 1;
    for (size_t i = 0; i != end; ++i)
      {
185
186
187
188
        os.width(w);
        os << i;
        os.width(1);
        os << ": " << a.at(i) << '\n';
189
190
191
192
      }
    return os;
  }
}