spot  2.2.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 #include <new>
30 
31 namespace spot
32 {
35 
36  class bitvect;
37  class bitvect_array;
38 
42  SPOT_API bitvect* make_bitvect(size_t bitcount);
43 
47  SPOT_API bitvect_array* make_bitvect_array(size_t bitcount,
48  size_t vectcount);
49 
51  class SPOT_API bitvect
52  {
53  private:
54  // Used by make_bitvect to construct a large bitvect in place.
55  bitvect(size_t size, size_t block_count);
56  bitvect(size_t size, size_t block_count, bool);
57 
58  public:
59  typedef unsigned long block_t;
60 
61  bitvect():
62  size_(0),
63  block_count_(1),
64  storage_(&local_storage_),
65  local_storage_(0)
66  {
67  }
68 
69  bitvect(const bitvect& other):
70  size_(other.size_),
71  block_count_(1),
72  storage_(&local_storage_)
73  {
74  *this = other;
75  }
76 
77  bitvect* clone() const;
78 
79  void make_empty()
80  {
81  size_ = 0;
82  }
83 
84  bitvect& operator=(const bitvect& other)
85  {
86  reserve_blocks(other.block_count_);
87  size_ = other.size();
88  for (size_t i = 0; i < block_count_; ++i)
89  storage_[i] = other.storage_[i];
90  return *this;
91  }
92 
93  ~bitvect()
94  {
95  if (storage_ != &local_storage_)
96  free(storage_);
97  }
98 
102  void reserve_blocks(size_t new_block_count)
103  {
104  if (new_block_count < block_count_)
105  return;
106  if (storage_ == &local_storage_)
107  {
108  block_t* new_storage_ = static_cast<block_t*>
109  (malloc(new_block_count * sizeof(block_t)));
110  for (size_t i = 0; i < block_count_; ++i)
111  new_storage_[i] = storage_[i];
112  storage_ = new_storage_;
113  }
114  else
115  {
116  auto old = storage_;
117  storage_ = static_cast<block_t*>
118  (realloc(old, new_block_count * sizeof(block_t)));
119  if (!storage_)
120  {
121  free(old);
122  throw std::bad_alloc();
123  }
124  }
125  block_count_ = new_block_count;
126  }
127 
128  private:
129  void grow()
130  {
131  size_t new_block_count_ = (block_count_ + 1) * 7 / 5;
132  reserve_blocks(new_block_count_);
133  }
134 
135  public:
136 
137  size_t used_blocks() const
138  {
139  const size_t bpb = 8 * sizeof(block_t);
140  return (size_ + bpb - 1) / bpb;
141  }
142 
144  void push_back(bool val)
145  {
146  if (size() == capacity())
147  grow();
148  size_t pos = size_++;
149  if (val)
150  set(pos);
151  else
152  clear(pos);
153  }
154 
156  void push_back(block_t data, unsigned count)
157  {
158  if (size() + count > capacity())
159  grow();
160  const size_t bpb = 8 * sizeof(block_t);
161 
162  // Clear the higher bits.
163  if (count != bpb)
164  data &= (1UL << count) - 1;
165 
166  size_t n = size() % bpb;
167  size_t i = size_ / bpb;
168  size_ += count;
169  if (n == 0) // Aligned on block_t boundary
170  {
171  storage_[i] = data;
172  }
173  else // Only (bpb-n) bits free in this block.
174  {
175  // Take the lower bpb-n bits of data...
176  block_t mask = (1UL << (bpb - n)) - 1;
177  block_t data1 = (data & mask) << n;
178  mask <<= n;
179  // ... write them on the higher bpb-n bits of last block.
180  storage_[i] = (storage_[i] & ~mask) | data1;
181  // Write the remaining bits in the next block.
182  if (bpb - n < count)
183  storage_[i + 1] = data >> (bpb - n);
184  }
185  }
186 
187  size_t size() const
188  {
189  return size_;
190  }
191 
192  size_t capacity() const
193  {
194  return 8 * block_count_ * sizeof(block_t);
195  }
196 
197  size_t hash() const;
198 
199  bool get(size_t pos) const
200  {
201  SPOT_ASSERT(pos < size_);
202  const size_t bpb = 8 * sizeof(block_t);
203  return storage_[pos / bpb] & (1UL << (pos % bpb));
204  }
205 
206  void clear_all()
207  {
208  for (size_t i = 0; i < block_count_; ++i)
209  storage_[i] = 0;
210  }
211 
212  bool is_fully_clear() const
213  {
214  size_t i;
215  const size_t bpb = 8 * sizeof(bitvect::block_t);
216  size_t rest = size() % bpb;
217  for (i = 0; i < block_count_ - !!rest; ++i)
218  if (storage_[i] != 0)
219  return false;
220  // The last block might not be fully used, compare only the
221  // relevant portion.
222  if (!rest)
223  return true;
224  block_t mask = (1UL << rest) - 1;
225  return (storage_[i] & mask) == 0;
226  }
227 
228  bool is_fully_set() const
229  {
230  size_t i;
231  const size_t bpb = 8 * sizeof(bitvect::block_t);
232  size_t rest = size() % bpb;
233  for (i = 0; i < block_count_ - !!rest; ++i)
234  if (storage_[i] != -1UL)
235  return false;
236  if (!rest)
237  return true;
238  // The last block might not be fully used, compare only the
239  // relevant portion.
240  block_t mask = (1UL << rest) - 1;
241  return ((~storage_[i]) & mask) == 0;
242  }
243 
244  void set_all()
245  {
246  for (size_t i = 0; i < block_count_; ++i)
247  storage_[i] = -1UL;
248  }
249 
250  void flip_all()
251  {
252  for (size_t i = 0; i < block_count_; ++i)
253  storage_[i] = ~storage_[i];
254  }
255 
256  void set(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 clear(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  void flip(size_t pos)
271  {
272  SPOT_ASSERT(pos < size_);
273  const size_t bpb = 8 * sizeof(block_t);
274  storage_[pos / bpb] ^= (1UL << (pos % bpb));
275  }
276 
277 
278  bitvect& operator|=(const bitvect& other)
279  {
280  SPOT_ASSERT(other.size_ <= size_);
281  unsigned m = std::min(other.block_count_, block_count_);
282  for (size_t i = 0; i < m; ++i)
283  storage_[i] |= other.storage_[i];
284  return *this;
285  }
286 
287  bitvect& operator&=(const bitvect& other)
288  {
289  SPOT_ASSERT(other.size_ <= size_);
290  unsigned m = std::min(other.block_count_, block_count_);
291  for (size_t i = 0; i < m; ++i)
292  storage_[i] &= other.storage_[i];
293  return *this;
294  }
295 
296  bitvect& operator^=(const bitvect& other)
297  {
298  SPOT_ASSERT(other.size_ <= size_);
299  unsigned m = std::min(other.block_count_, block_count_);
300  for (size_t i = 0; i < m; ++i)
301  storage_[i] ^= other.storage_[i];
302  return *this;
303  }
304 
305  bitvect& operator-=(const bitvect& other)
306  {
307  SPOT_ASSERT(other.block_count_ <= block_count_);
308  for (size_t i = 0; i < other.block_count_; ++i)
309  storage_[i] &= ~other.storage_[i];
310  return *this;
311  }
312 
313  bool is_subset_of(const bitvect& other) const
314  {
315  SPOT_ASSERT(other.block_count_ >= block_count_);
316 
317  size_t i;
318  const size_t bpb = 8 * sizeof(bitvect::block_t);
319  size_t rest = size() % bpb;
320  for (i = 0; i < block_count_ - !!rest; ++i)
321  if ((storage_[i] & other.storage_[i]) != storage_[i])
322  return false;
323  if (!rest)
324  return true;
325 
326  // The last block might not be fully used, compare only the
327  // relevant portion.
328  block_t mask = (1UL << rest) - 1;
329  return ((storage_[i] & mask & other.storage_[i])
330  == (storage_[i] & mask));
331  }
332 
333  bool operator==(const bitvect& other) const
334  {
335  if (other.size_ != size_)
336  return false;
337  if (size_ == 0)
338  return true;
339  size_t i;
340  size_t m = other.used_blocks();
341  const size_t bpb = 8 * sizeof(bitvect::block_t);
342  size_t rest = size() % bpb;
343  for (i = 0; i < m - !!rest; ++i)
344  if (storage_[i] != other.storage_[i])
345  return false;
346  if (!rest)
347  return true;
348  // The last block might not be fully used, compare only the
349  // relevant portion.
350  block_t mask = (1UL << rest) - 1;
351  return (storage_[i] & mask) == (other.storage_[i] & mask);
352  }
353 
354  bool operator!=(const bitvect& other) const
355  {
356  return !(*this == other);
357  }
358 
359  bool operator<(const bitvect& other) const
360  {
361  if (size_ != other.size_)
362  return size_ < other.size_;
363  if (size_ == 0)
364  return false;
365  size_t i;
366  size_t m = other.used_blocks();
367  const size_t bpb = 8 * sizeof(bitvect::block_t);
368  size_t rest = size() % bpb;
369  for (i = 0; i < m - !!rest; ++i)
370  if (storage_[i] > other.storage_[i])
371  return false;
372  if (!rest)
373  return true;
374  // The last block might not be fully used, compare only the
375  // relevant portion.
376  block_t mask = (1UL << rest) - 1;
377  return (storage_[i] & mask) < (other.storage_[i] & mask);
378  }
379 
380  bool operator>=(const bitvect& other) const
381  {
382  return !(*this < other);
383  }
384 
385  bool operator>(const bitvect& other) const
386  {
387  return other < *this;
388  }
389 
390  bool operator<=(const bitvect& other) const
391  {
392  return !(other < *this);
393  }
394 
395  // \brief Extract a range of bits.
396  //
397  // Build a new bit-vector using the bits from \a begin (included)
398  // to \a end (excluded).
399  bitvect* extract_range(size_t begin, size_t end)
400  {
401  SPOT_ASSERT(begin <= end);
402  SPOT_ASSERT(end <= size());
403  size_t count = end - begin;
404  bitvect* res = make_bitvect(count);
405  res->make_empty();
406 
407  if (end == begin)
408  return res;
409 
410  const size_t bpb = 8 * sizeof(bitvect::block_t);
411 
412  size_t indexb = begin / bpb;
413  unsigned bitb = begin % bpb;
414  size_t indexe = (end - 1) / bpb;
415 
416  if (indexb == indexe)
417  {
418  block_t data = storage_[indexb];
419  data >>= bitb;
420  res->push_back(data, count);
421  }
422  else
423  {
424  block_t data = storage_[indexb];
425  data >>= bitb;
426  res->push_back(data, bpb - bitb);
427  count -= bpb - bitb;
428  while (count >= bpb)
429  {
430  ++indexb;
431  res->push_back(storage_[indexb], bpb);
432  count -= bpb;
433  SPOT_ASSERT(indexb != indexe || count == 0);
434  }
435  if (count > 0)
436  {
437  ++indexb;
438  SPOT_ASSERT(indexb == indexe);
439  SPOT_ASSERT(count == end % bpb);
440  res->push_back(storage_[indexb], count);
441  }
442  }
443  return res;
444  }
445 
446  friend SPOT_API bitvect* make_bitvect(size_t bitcount);
447 
449  friend SPOT_API std::ostream& operator<<(std::ostream&,
450  const bitvect&);
451 
452  private:
453  friend SPOT_API bitvect_array* make_bitvect_array(size_t bitcount,
454  size_t vectcount);
455 
456  size_t size_;
457  size_t block_count_;
458  // storage_ points to local_storage_ as long as size_ <= block_count_ * 8.
459  block_t* storage_;
460  // Keep this at the end of the structure: when make_bitvect is used,
461  // it may allocate more block_t at the end of this structure.
462  block_t local_storage_;
463  };
464 
465  class SPOT_API bitvect_array
466  {
467  private:
469  bitvect_array(size_t size, size_t bvsize):
470  size_(size),
471  bvsize_(bvsize)
472  {
473  }
474 
475  SPOT_LOCAL bitvect_array(const bitvect_array&) = delete;
476  SPOT_LOCAL void operator=(const bitvect_array&) = delete;
477 
478  // Extra storage has been allocated at the end of the struct.
479  char* storage()
480  {
481  return reinterpret_cast<char*>(this) + sizeof(*this);
482  }
483 
484  const char* storage() const
485  {
486  return reinterpret_cast<const char*>(this) + sizeof(*this);
487  }
488 
489  public:
490  ~bitvect_array()
491  {
492  for (size_t i = 0; i < size_; ++i)
493  at(i).~bitvect();
494  }
495 
497  size_t size() const
498  {
499  return size_;
500  }
501 
503  bitvect& at(const size_t index)
504  {
505  SPOT_ASSERT(index < size_);
506  return *reinterpret_cast<bitvect*>(storage() + index * bvsize_);
507  }
508 
509  void clear_all()
510  {
511  // FIXME: This could be changed into a large memset if the
512  // individual vectors where not allowed to be reallocated.
513  for (unsigned s = 0; s < size_; s++)
514  at(s).clear_all();
515  }
516 
518  const bitvect& at(const size_t index) const
519  {
520  SPOT_ASSERT(index < size_);
521  return *reinterpret_cast<const bitvect*>(storage() + index * bvsize_);
522  }
523 
524  friend SPOT_API bitvect_array* make_bitvect_array(size_t bitcount,
525  size_t vectcount);
526 
527 
529  friend SPOT_API std::ostream& operator<<(std::ostream&,
530  const bitvect_array&);
531 
532  private:
533  size_t size_;
534  size_t bvsize_;
535  };
536 
538 }
Definition: graph.hh:32
size_t size() const
The number of bitvect in the array.
Definition: bitvect.hh:497
const bitvect & at(const size_t index) const
Return the bit-vector at index.
Definition: bitvect.hh:518
void push_back(bool val)
Append one bit.
Definition: bitvect.hh:144
Definition: bitvect.hh:465
void push_back(block_t data, unsigned count)
Append the lowest count bits of data.
Definition: bitvect.hh:156
bitvect & at(const size_t index)
Return the bit-vector at index.
Definition: bitvect.hh:503
void reserve_blocks(size_t new_block_count)
Definition: bitvect.hh:102
A bit vector.
Definition: bitvect.hh:51

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Dec 16 2016 06:04:07 for spot by doxygen 1.8.8