spot  2.7
bitvect.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2013-2018 Laboratoire de Recherche et Développement
3 // 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 operator delete(void *ptr)
80  {
81  // This object was allocated using a placement new.
82  ::operator delete(ptr);
83  }
84 
85  void make_empty()
86  {
87  size_ = 0;
88  }
89 
90  bitvect& operator=(const bitvect& other)
91  {
92  reserve_blocks(other.block_count_);
93  size_ = other.size();
94  for (size_t i = 0; i < block_count_; ++i)
95  storage_[i] = other.storage_[i];
96  return *this;
97  }
98 
99  ~bitvect()
100  {
101  if (storage_ != &local_storage_)
102  free(storage_);
103  }
104 
108  void reserve_blocks(size_t new_block_count)
109  {
110  if (new_block_count < block_count_)
111  return;
112  if (storage_ == &local_storage_)
113  {
114  block_t* new_storage_ = static_cast<block_t*>
115  (malloc(new_block_count * sizeof(block_t)));
116  for (size_t i = 0; i < block_count_; ++i)
117  new_storage_[i] = storage_[i];
118  storage_ = new_storage_;
119  }
120  else
121  {
122  auto old = storage_;
123  storage_ = static_cast<block_t*>
124  (realloc(old, new_block_count * sizeof(block_t)));
125  if (!storage_)
126  {
127  free(old);
128  throw std::bad_alloc();
129  }
130  }
131  block_count_ = new_block_count;
132  }
133 
134  private:
135  void grow()
136  {
137  size_t new_block_count_ = (block_count_ + 1) * 7 / 5;
138  reserve_blocks(new_block_count_);
139  }
140 
141  public:
142 
143  size_t used_blocks() const
144  {
145  const size_t bpb = 8 * sizeof(block_t);
146  return (size_ + bpb - 1) / bpb;
147  }
148 
149  size_t size() const
150  {
151  return size_;
152  }
153 
154  size_t capacity() const
155  {
156  return 8 * block_count_ * sizeof(block_t);
157  }
158 
159  size_t hash() const noexcept;
160 
161  bool get(size_t pos) const
162  {
163  SPOT_ASSERT(pos < size_);
164  const size_t bpb = 8 * sizeof(block_t);
165  return storage_[pos / bpb] & (1UL << (pos % bpb));
166  }
167 
168  void clear_all()
169  {
170  for (size_t i = 0; i < block_count_; ++i)
171  storage_[i] = 0;
172  }
173 
174  bool is_fully_clear() const
175  {
176  size_t i;
177  const size_t bpb = 8 * sizeof(bitvect::block_t);
178  size_t rest = size() % bpb;
179  for (i = 0; i < block_count_ - !!rest; ++i)
180  if (storage_[i] != 0)
181  return false;
182  // The last block might not be fully used, compare only the
183  // relevant portion.
184  if (!rest)
185  return true;
186  block_t mask = (1UL << rest) - 1;
187  return (storage_[i] & mask) == 0;
188  }
189 
190  bool is_fully_set() const
191  {
192  size_t i;
193  const size_t bpb = 8 * sizeof(bitvect::block_t);
194  size_t rest = size() % bpb;
195  for (i = 0; i < block_count_ - !!rest; ++i)
196  if (storage_[i] != -1UL)
197  return false;
198  if (!rest)
199  return true;
200  // The last block might not be fully used, compare only the
201  // relevant portion.
202  block_t mask = (1UL << rest) - 1;
203  return ((~storage_[i]) & mask) == 0;
204  }
205 
206  void set_all()
207  {
208  for (size_t i = 0; i < block_count_; ++i)
209  storage_[i] = -1UL;
210  }
211 
212  void flip_all()
213  {
214  for (size_t i = 0; i < block_count_; ++i)
215  storage_[i] = ~storage_[i];
216  }
217 
218  void set(size_t pos)
219  {
220  SPOT_ASSERT(pos < size_);
221  const size_t bpb = 8 * sizeof(block_t);
222  storage_[pos / bpb] |= 1UL << (pos % bpb);
223  }
224 
225  void clear(size_t pos)
226  {
227  SPOT_ASSERT(pos < size_);
228  const size_t bpb = 8 * sizeof(block_t);
229  storage_[pos / bpb] &= ~(1UL << (pos % bpb));
230  }
231 
232  void flip(size_t pos)
233  {
234  SPOT_ASSERT(pos < size_);
235  const size_t bpb = 8 * sizeof(block_t);
236  storage_[pos / bpb] ^= (1UL << (pos % bpb));
237  }
238 
239 
240  bitvect& operator|=(const bitvect& other)
241  {
242  SPOT_ASSERT(other.size_ <= size_);
243  unsigned m = std::min(other.block_count_, block_count_);
244  for (size_t i = 0; i < m; ++i)
245  storage_[i] |= other.storage_[i];
246  return *this;
247  }
248 
249  bitvect& operator&=(const bitvect& other)
250  {
251  SPOT_ASSERT(other.size_ <= size_);
252  unsigned m = std::min(other.block_count_, block_count_);
253  for (size_t i = 0; i < m; ++i)
254  storage_[i] &= other.storage_[i];
255  return *this;
256  }
257 
258  bitvect& operator^=(const bitvect& other)
259  {
260  SPOT_ASSERT(other.size_ <= size_);
261  unsigned m = std::min(other.block_count_, block_count_);
262  for (size_t i = 0; i < m; ++i)
263  storage_[i] ^= other.storage_[i];
264  return *this;
265  }
266 
267  bitvect& operator-=(const bitvect& other)
268  {
269  SPOT_ASSERT(other.block_count_ <= block_count_);
270  for (size_t i = 0; i < other.block_count_; ++i)
271  storage_[i] &= ~other.storage_[i];
272  return *this;
273  }
274 
275  bool is_subset_of(const bitvect& other) const
276  {
277  SPOT_ASSERT(other.block_count_ >= block_count_);
278 
279  size_t i;
280  const size_t bpb = 8 * sizeof(bitvect::block_t);
281  size_t rest = size() % bpb;
282  for (i = 0; i < block_count_ - !!rest; ++i)
283  if ((storage_[i] & other.storage_[i]) != storage_[i])
284  return false;
285  if (!rest)
286  return true;
287 
288  // The last block might not be fully used, compare only the
289  // relevant portion.
290  block_t mask = (1UL << rest) - 1;
291  return ((storage_[i] & mask & other.storage_[i])
292  == (storage_[i] & mask));
293  }
294 
295  bool operator==(const bitvect& other) const
296  {
297  if (other.size_ != size_)
298  return false;
299  if (size_ == 0)
300  return true;
301  size_t i;
302  size_t m = other.used_blocks();
303  const size_t bpb = 8 * sizeof(bitvect::block_t);
304  size_t rest = size() % bpb;
305  for (i = 0; i < m - !!rest; ++i)
306  if (storage_[i] != other.storage_[i])
307  return false;
308  if (!rest)
309  return true;
310  // The last block might not be fully used, compare only the
311  // relevant portion.
312  block_t mask = (1UL << rest) - 1;
313  return (storage_[i] & mask) == (other.storage_[i] & mask);
314  }
315 
316  bool operator!=(const bitvect& other) const
317  {
318  return !(*this == other);
319  }
320 
321  bool operator<(const bitvect& other) const
322  {
323  if (size_ != other.size_)
324  return size_ < other.size_;
325  if (size_ == 0)
326  return false;
327  size_t i;
328  size_t m = other.used_blocks();
329  const size_t bpb = 8 * sizeof(bitvect::block_t);
330  size_t rest = size() % bpb;
331  for (i = 0; i < m - !!rest; ++i)
332  if (storage_[i] > other.storage_[i])
333  return false;
334  if (!rest)
335  return true;
336  // The last block might not be fully used, compare only the
337  // relevant portion.
338  block_t mask = (1UL << rest) - 1;
339  return (storage_[i] & mask) < (other.storage_[i] & mask);
340  }
341 
342  bool operator>=(const bitvect& other) const
343  {
344  return !(*this < other);
345  }
346 
347  bool operator>(const bitvect& other) const
348  {
349  return other < *this;
350  }
351 
352  bool operator<=(const bitvect& other) const
353  {
354  return !(other < *this);
355  }
356 
357  friend SPOT_API bitvect* make_bitvect(size_t bitcount);
358 
360  friend SPOT_API std::ostream& operator<<(std::ostream&,
361  const bitvect&);
362 
363  private:
364  friend SPOT_API bitvect_array* make_bitvect_array(size_t bitcount,
365  size_t vectcount);
366 
367  size_t size_;
368  size_t block_count_;
369  // storage_ points to local_storage_ as long as size_ <= block_count_ * 8.
370  block_t* storage_;
371  // Keep this at the end of the structure: when make_bitvect is used,
372  // it may allocate more block_t at the end of this structure.
373  block_t local_storage_;
374  };
375 
376  class SPOT_API bitvect_array
377  {
378  private:
380  bitvect_array(size_t size, size_t bvsize):
381  size_(size),
382  bvsize_(bvsize)
383  {
384  }
385 
386  SPOT_LOCAL bitvect_array(const bitvect_array&) = delete;
387  SPOT_LOCAL void operator=(const bitvect_array&) = delete;
388 
389  // Extra storage has been allocated at the end of the struct.
390  char* storage()
391  {
392  return reinterpret_cast<char*>(this) + sizeof(*this);
393  }
394 
395  const char* storage() const
396  {
397  return reinterpret_cast<const char*>(this) + sizeof(*this);
398  }
399 
400  public:
401  ~bitvect_array()
402  {
403  for (size_t i = 0; i < size_; ++i)
404  at(i).~bitvect();
405  }
406 
407  void operator delete(void *ptr)
408  {
409  // This object was allocated using a placement new.
410  ::operator delete(ptr);
411  }
412 
414  size_t size() const
415  {
416  return size_;
417  }
418 
420  bitvect& at(const size_t index)
421  {
422  SPOT_ASSERT(index < size_);
423  return *reinterpret_cast<bitvect*>(storage() + index * bvsize_);
424  }
425 
426  void clear_all()
427  {
428  // FIXME: This could be changed into a large memset if the
429  // individual vectors where not allowed to be reallocated.
430  for (unsigned s = 0; s < size_; s++)
431  at(s).clear_all();
432  }
433 
435  const bitvect& at(const size_t index) const
436  {
437  SPOT_ASSERT(index < size_);
438  return *reinterpret_cast<const bitvect*>(storage() + index * bvsize_);
439  }
440 
441  friend SPOT_API bitvect_array* make_bitvect_array(size_t bitcount,
442  size_t vectcount);
443 
444 
446  friend SPOT_API std::ostream& operator<<(std::ostream&,
447  const bitvect_array&);
448 
449  private:
450  size_t size_;
451  size_t bvsize_;
452  };
453 
455 }
Definition: automata.hh:26
Definition: bitvect.hh:376
const bitvect & at(const size_t index) const
Return the bit-vector at index.
Definition: bitvect.hh:435
bitvect & at(const size_t index)
Return the bit-vector at index.
Definition: bitvect.hh:420
size_t size() const
The number of bitvect in the array.
Definition: bitvect.hh:414
void reserve_blocks(size_t new_block_count)
Definition: bitvect.hh:108
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 Feb 27 2015 10:00:07 for spot by doxygen 1.8.13