spot  2.1.2
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
bitvect.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
3 // Développement de l'Epita (LRDE).
4 //
5 // This file is part of Spot, a model checking library.
6 //
7 // Spot is free software; you can redistribute it and/or modify it
8 // under the terms of the GNU General Public License as published by
9 // the Free Software Foundation; either version 3 of the License, or
10 // (at your option) any later version.
11 //
12 // Spot is distributed in the hope that it will be useful, but WITHOUT
13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15 // License for more details.
16 //
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <http://www.gnu.org/licenses/>.
19 
20 #pragma once
21 
22 #include <spot/misc/common.hh>
23 #include <cstddef>
24 #include <cstdlib>
25 #include <cassert>
26 #include <iosfwd>
27 #include <iostream>
28 #include <algorithm>
29 
30 namespace spot
31 {
34 
35  class bitvect;
36  class bitvect_array;
37 
41  SPOT_API bitvect* make_bitvect(size_t bitcount);
42 
46  SPOT_API bitvect_array* make_bitvect_array(size_t bitcount,
47  size_t vectcount);
48 
50  class SPOT_API bitvect
51  {
52  private:
53  // Used by make_bitvect to construct a large bitvect in place.
54  bitvect(size_t size, size_t block_count);
55  bitvect(size_t size, size_t block_count, bool);
56 
57  public:
58  typedef unsigned long block_t;
59 
60  bitvect():
61  size_(0),
62  block_count_(1),
63  storage_(&local_storage_),
64  local_storage_(0)
65  {
66  }
67 
68  bitvect(const bitvect& other):
69  size_(other.size_),
70  block_count_(1),
71  storage_(&local_storage_)
72  {
73  *this = other;
74  }
75 
76  bitvect* clone() const;
77 
78  void make_empty()
79  {
80  size_ = 0;
81  }
82 
83  bitvect& operator=(const bitvect& other)
84  {
85  reserve_blocks(other.block_count_);
86  size_ = other.size();
87  for (size_t i = 0; i < block_count_; ++i)
88  storage_[i] = other.storage_[i];
89  return *this;
90  }
91 
92  ~bitvect()
93  {
94  if (storage_ != &local_storage_)
95  free(storage_);
96  }
97 
101  void reserve_blocks(size_t new_block_count)
102  {
103  if (new_block_count < block_count_)
104  return;
105  if (storage_ == &local_storage_)
106  {
107  block_t* new_storage_ = static_cast<block_t*>
108  (malloc(new_block_count * sizeof(block_t)));
109  for (size_t i = 0; i < block_count_; ++i)
110  new_storage_[i] = storage_[i];
111  storage_ = new_storage_;
112  }
113  else
114  {
115  storage_ = static_cast<block_t*>
116  (realloc(storage_, new_block_count * sizeof(block_t)));
117  }
118  block_count_ = new_block_count;
119  }
120 
121  private:
122  void grow()
123  {
124  size_t new_block_count_ = (block_count_ + 1) * 7 / 5;
125  reserve_blocks(new_block_count_);
126  }
127 
128  public:
129 
130  size_t used_blocks() const
131  {
132  const size_t bpb = 8 * sizeof(block_t);
133  return (size_ + bpb - 1) / bpb;
134  }
135 
137  void push_back(bool val)
138  {
139  if (size() == capacity())
140  grow();
141  size_t pos = size_++;
142  if (val)
143  set(pos);
144  else
145  clear(pos);
146  }
147 
149  void push_back(block_t data, unsigned count)
150  {
151  if (size() + count > capacity())
152  grow();
153  const size_t bpb = 8 * sizeof(block_t);
154 
155  // Clear the higher bits.
156  if (count != bpb)
157  data &= (1UL << count) - 1;
158 
159  size_t n = size() % bpb;
160  size_t i = size_ / bpb;
161  size_ += count;
162  if (n == 0) // Aligned on block_t boundary
163  {
164  storage_[i] = data;
165  }
166  else // Only (bpb-n) bits free in this block.
167  {
168  // Take the lower bpb-n bits of data...
169  block_t mask = (1UL << (bpb - n)) - 1;
170  block_t data1 = (data & mask) << n;
171  mask <<= n;
172  // ... write them on the higher bpb-n bits of last block.
173  storage_[i] = (storage_[i] & ~mask) | data1;
174  // Write the remaining bits in the next block.
175  if (bpb - n < count)
176  storage_[i + 1] = data >> (bpb - n);
177  }
178  }
179 
180  size_t size() const
181  {
182  return size_;
183  }
184 
185  size_t capacity() const
186  {
187  return 8 * block_count_ * sizeof(block_t);
188  }
189 
190  size_t hash() const;
191 
192  bool get(size_t pos) const
193  {
194  SPOT_ASSERT(pos < size_);
195  const size_t bpb = 8 * sizeof(block_t);
196  return storage_[pos / bpb] & (1UL << (pos % bpb));
197  }
198 
199  void clear_all()
200  {
201  for (size_t i = 0; i < block_count_; ++i)
202  storage_[i] = 0;
203  }
204 
205  bool is_fully_clear() const
206  {
207  size_t i;
208  const size_t bpb = 8 * sizeof(bitvect::block_t);
209  size_t rest = size() % bpb;
210  for (i = 0; i < block_count_ - !!rest; ++i)
211  if (storage_[i] != 0)
212  return false;
213  // The last block might not be fully used, compare only the
214  // relevant portion.
215  if (!rest)
216  return true;
217  block_t mask = (1UL << rest) - 1;
218  return (storage_[i] & mask) == 0;
219  }
220 
221  bool is_fully_set() const
222  {
223  size_t i;
224  const size_t bpb = 8 * sizeof(bitvect::block_t);
225  size_t rest = size() % bpb;
226  for (i = 0; i < block_count_ - !!rest; ++i)
227  if (storage_[i] != -1UL)
228  return false;
229  if (!rest)
230  return true;
231  // The last block might not be fully used, compare only the
232  // relevant portion.
233  block_t mask = (1UL << rest) - 1;
234  return ((~storage_[i]) & mask) == 0;
235  }
236 
237  void set_all()
238  {
239  for (size_t i = 0; i < block_count_; ++i)
240  storage_[i] = -1UL;
241  }
242 
243  void flip_all()
244  {
245  for (size_t i = 0; i < block_count_; ++i)
246  storage_[i] = ~storage_[i];
247  }
248 
249  void set(size_t pos)
250  {
251  SPOT_ASSERT(pos < size_);
252  const size_t bpb = 8 * sizeof(block_t);
253  storage_[pos / bpb] |= 1UL << (pos % bpb);
254  }
255 
256  void clear(size_t pos)
257  {
258  SPOT_ASSERT(pos < size_);
259  const size_t bpb = 8 * sizeof(block_t);
260  storage_[pos / bpb] &= ~(1UL << (pos % bpb));
261  }
262 
263  void flip(size_t pos)
264  {
265  SPOT_ASSERT(pos < size_);
266  const size_t bpb = 8 * sizeof(block_t);
267  storage_[pos / bpb] ^= (1UL << (pos % bpb));
268  }
269 
270 
271  bitvect& operator|=(const bitvect& other)
272  {
273  SPOT_ASSERT(other.size_ <= size_);
274  unsigned m = std::min(other.block_count_, block_count_);
275  for (size_t i = 0; i < m; ++i)
276  storage_[i] |= other.storage_[i];
277  return *this;
278  }
279 
280  bitvect& operator&=(const bitvect& other)
281  {
282  SPOT_ASSERT(other.size_ <= size_);
283  unsigned m = std::min(other.block_count_, block_count_);
284  for (size_t i = 0; i < m; ++i)
285  storage_[i] &= other.storage_[i];
286  return *this;
287  }
288 
289  bitvect& operator^=(const bitvect& other)
290  {
291  SPOT_ASSERT(other.size_ <= size_);
292  unsigned m = std::min(other.block_count_, block_count_);
293  for (size_t i = 0; i < m; ++i)
294  storage_[i] ^= other.storage_[i];
295  return *this;
296  }
297 
298  bitvect& operator-=(const bitvect& other)
299  {
300  SPOT_ASSERT(other.block_count_ <= block_count_);
301  for (size_t i = 0; i < other.block_count_; ++i)
302  storage_[i] &= ~other.storage_[i];
303  return *this;
304  }
305 
306  bool is_subset_of(const bitvect& other) const
307  {
308  SPOT_ASSERT(other.block_count_ >= block_count_);
309 
310  size_t i;
311  const size_t bpb = 8 * sizeof(bitvect::block_t);
312  size_t rest = size() % bpb;
313  for (i = 0; i < block_count_ - !!rest; ++i)
314  if ((storage_[i] & other.storage_[i]) != other.storage_[i])
315  return false;
316  if (!rest)
317  return true;
318 
319  // The last block might not be fully used, compare only the
320  // relevant portion.
321  block_t mask = (1UL << rest) - 1;
322  return ((storage_[i] & mask & other.storage_[i])
323  == (other.storage_[i] & mask));
324  }
325 
326  bool operator==(const bitvect& other) const
327  {
328  if (other.size_ != size_)
329  return false;
330  if (size_ == 0)
331  return true;
332  size_t i;
333  size_t m = other.used_blocks();
334  const size_t bpb = 8 * sizeof(bitvect::block_t);
335  size_t rest = size() % bpb;
336  for (i = 0; i < m - !!rest; ++i)
337  if (storage_[i] != other.storage_[i])
338  return false;
339  if (!rest)
340  return true;
341  // The last block might not be fully used, compare only the
342  // relevant portion.
343  block_t mask = (1UL << rest) - 1;
344  return (storage_[i] & mask) == (other.storage_[i] & mask);
345  }
346 
347  bool operator!=(const bitvect& other) const
348  {
349  return !(*this == other);
350  }
351 
352  bool operator<(const bitvect& other) const
353  {
354  if (size_ != other.size_)
355  return size_ < other.size_;
356  if (size_ == 0)
357  return false;
358  size_t i;
359  size_t m = other.used_blocks();
360  const size_t bpb = 8 * sizeof(bitvect::block_t);
361  size_t rest = size() % bpb;
362  for (i = 0; i < m - !!rest; ++i)
363  if (storage_[i] > other.storage_[i])
364  return false;
365  if (!rest)
366  return true;
367  // The last block might not be fully used, compare only the
368  // relevant portion.
369  block_t mask = (1UL << rest) - 1;
370  return (storage_[i] & mask) < (other.storage_[i] & mask);
371  }
372 
373  bool operator>=(const bitvect& other) const
374  {
375  return !(*this < other);
376  }
377 
378  bool operator>(const bitvect& other) const
379  {
380  return other < *this;
381  }
382 
383  bool operator<=(const bitvect& other) const
384  {
385  return !(other < *this);
386  }
387 
388  // \brief Extract a range of bits.
389  //
390  // Build a new bit-vector using the bits from \a begin (included)
391  // to \a end (excluded).
392  bitvect* extract_range(size_t begin, size_t end)
393  {
394  SPOT_ASSERT(begin <= end);
395  SPOT_ASSERT(end <= size());
396  size_t count = end - begin;
397  bitvect* res = make_bitvect(count);
398  res->make_empty();
399 
400  if (end == begin)
401  return res;
402 
403  const size_t bpb = 8 * sizeof(bitvect::block_t);
404 
405  size_t indexb = begin / bpb;
406  unsigned bitb = begin % bpb;
407  size_t indexe = (end - 1) / bpb;
408 
409  if (indexb == indexe)
410  {
411  block_t data = storage_[indexb];
412  data >>= bitb;
413  res->push_back(data, count);
414  }
415  else
416  {
417  block_t data = storage_[indexb];
418  data >>= bitb;
419  res->push_back(data, bpb - bitb);
420  count -= bpb - bitb;
421  while (count >= bpb)
422  {
423  ++indexb;
424  res->push_back(storage_[indexb], bpb);
425  count -= bpb;
426  SPOT_ASSERT(indexb != indexe || count == 0);
427  }
428  if (count > 0)
429  {
430  ++indexb;
431  SPOT_ASSERT(indexb == indexe);
432  SPOT_ASSERT(count == end % bpb);
433  res->push_back(storage_[indexb], count);
434  }
435  }
436  return res;
437  }
438 
439  friend SPOT_API bitvect* make_bitvect(size_t bitcount);
440 
442  friend SPOT_API std::ostream& operator<<(std::ostream&,
443  const bitvect&);
444 
445  private:
446  friend SPOT_API bitvect_array* make_bitvect_array(size_t bitcount,
447  size_t vectcount);
448 
449  size_t size_;
450  size_t block_count_;
451  // storage_ points to local_storage_ as long as size_ <= block_count_ * 8.
452  block_t* storage_;
453  // Keep this at the end of the structure: when make_bitvect is used,
454  // it may allocate more block_t at the end of this structure.
455  block_t local_storage_;
456  };
457 
458  class SPOT_API bitvect_array
459  {
460  private:
462  bitvect_array(size_t size, size_t bvsize):
463  size_(size),
464  bvsize_(bvsize)
465  {
466  }
467 
468  SPOT_LOCAL bitvect_array(const bitvect_array&) = delete;
469  SPOT_LOCAL void operator=(const bitvect_array&) = delete;
470 
471  // Extra storage has been allocated at the end of the struct.
472  char* storage()
473  {
474  return reinterpret_cast<char*>(this) + sizeof(*this);
475  }
476 
477  const char* storage() const
478  {
479  return reinterpret_cast<const char*>(this) + sizeof(*this);
480  }
481 
482  public:
483  ~bitvect_array()
484  {
485  for (size_t i = 0; i < size_; ++i)
486  at(i).~bitvect();
487  }
488 
490  size_t size() const
491  {
492  return size_;
493  }
494 
496  bitvect& at(const size_t index)
497  {
498  SPOT_ASSERT(index < size_);
499  return *reinterpret_cast<bitvect*>(storage() + index * bvsize_);
500  }
501 
502  void clear_all()
503  {
504  // FIXME: This could be changed into a large memset if the
505  // individual vectors where not allowed to be reallocated.
506  for (unsigned s = 0; s < size_; s++)
507  at(s).clear_all();
508  }
509 
511  const bitvect& at(const size_t index) const
512  {
513  SPOT_ASSERT(index < size_);
514  return *reinterpret_cast<const bitvect*>(storage() + index * bvsize_);
515  }
516 
517  friend SPOT_API bitvect_array* make_bitvect_array(size_t bitcount,
518  size_t vectcount);
519 
520 
522  friend SPOT_API std::ostream& operator<<(std::ostream&,
523  const bitvect_array&);
524 
525  private:
526  size_t size_;
527  size_t bvsize_;
528  };
529 
531 }
Definition: graph.hh:32
size_t size() const
The number of bitvect in the array.
Definition: bitvect.hh:490
const bitvect & at(const size_t index) const
Return the bit-vector at index.
Definition: bitvect.hh:511
void push_back(bool val)
Append one bit.
Definition: bitvect.hh:137
Definition: bitvect.hh:458
void push_back(block_t data, unsigned count)
Append the lowest count bits of data.
Definition: bitvect.hh:149
bitvect & at(const size_t index)
Return the bit-vector at index.
Definition: bitvect.hh:496
void reserve_blocks(size_t new_block_count)
Definition: bitvect.hh:101
A bit vector.
Definition: bitvect.hh:50

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Oct 14 2016 15:38:12 for spot by doxygen 1.8.8