bitvect.cc 4.19 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2013, 2014, 2017, 2018 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
//
// 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
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
      return n;
    }

  }

  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.
69
70
    void* mem = ::operator new(sizeof(bitvect)
                               + (n - 1) * sizeof(bitvect::block_t));
71
72
73
74
75
    bitvect* res = new(mem) bitvect(size_, n, true);
    memcpy(res->storage_, storage_, res->block_count_ * sizeof(block_t));
    return res;
  }

76
  size_t bitvect::hash() const noexcept
77
  {
78
    const size_t m = used_blocks();
79
    if (m == 0)
80
81
82
      return fnv_hash(storage_, storage_ + m);

    size_t res = fnv_hash(storage_, storage_ + m - 1);
83
84
85
86
87
    // 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].
88
    res ^= storage_[m-1] & ((1UL << n) - 1);
89
90
91
92
93
94
95
96
97
    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.
98
99
    void* mem = ::operator new(sizeof(bitvect)
                               + (n - 1) * sizeof(bitvect::block_t));
100
101
102
103
104
105
106
107
108
109
110
    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.
111
     void* mem = ::operator new(sizeof(bitvect_array) + bvsize * vectcount);
112
113
114
     bitvect_array* bva = new(mem) bitvect_array(vectcount, bvsize);
     // Initialize all the bitvect instances.
     for (size_t i = 0; i < vectcount; ++i)
115
       new(bva->storage() + i * bvsize) bitvect(bitcount, n);
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
     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)
      {
131
132
        os << "empty\n";
        return os;
133
134
135
136
      }
    int w = floor(log10(end - 1)) + 1;
    for (size_t i = 0; i != end; ++i)
      {
137
138
139
140
        os.width(w);
        os << i;
        os.width(1);
        os << ": " << a.at(i) << '\n';
141
142
143
144
      }
    return os;
  }
}