← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriEngine/Structures/BitField.h

  • Committer: srba.jiri at gmail
  • Date: 2020-09-11 14:23:39 UTC
  • mfrom: (213.1.151 interval_tar)
  • Revision ID: srba.jiri@gmail.com-20200911142339-bq9328s1gppw24uj
merged in lp:~verifypn-maintainers/verifypn/interval_tar doing 
- Implements TAR w/o z3, but using a simple integer inference engine for Hoare logic.
 - Replaces LP-Solve with GLPK, reduces computation-time and memory overhead
 - Implements new global properties, translated into CTL formulae.

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/Structures/BitField.h
1
 
/* PeTe - Petri Engine exTremE
2
 
 * Copyright (C) 2011  Jonas Finnemann Jensen <jopsen@gmail.com>,
3
 
 *                     Thomas Søndersø Nielsen <primogens@gmail.com>,
4
 
 *                     Lars Kærlund Østergaard <larsko@gmail.com>
5
 
 * 
6
 
 * This program is free software: you can redistribute it and/or modify
7
 
 * it under the terms of the GNU General Public License as published by
8
 
 * the Free Software Foundation, either version 3 of the License, or
9
 
 * (at your option) any later version.
10
 
 * 
11
 
 * This program is distributed in the hope that it will be useful,
12
 
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
13
 
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
14
 
 * GNU General Public License for more details.
15
 
 * 
16
 
 * You should have received a copy of the GNU General Public License
17
 
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
18
 
 */
19
 
#ifndef BITFIELD_H
20
 
#define BITFIELD_H
21
 
 
22
 
#include <stdint.h>
23
 
#include <string.h>
24
 
#include <assert.h>
25
 
#include <limits.h>
26
 
 
27
 
namespace PetriEngine {
28
 
    namespace Structures {
29
 
 
30
 
        /** Representation of a BitField */
31
 
        class BitField {
32
 
        private:
33
 
            /** Definition of underlying type for the bitfield*/
34
 
            typedef unsigned int _word;
35
 
 
36
 
            /** Number of bits per word */
37
 
            static const size_t _bitsPerWord = CHAR_BIT * sizeof (_word);
38
 
 
39
 
            /** Number of words for size */
40
 
            size_t _words() const {
41
 
                return (_size + _bitsPerWord - 1) / _bitsPerWord;
42
 
            }
43
 
 
44
 
            /** Word offset for a given position */
45
 
            static size_t _wordOffset(size_t pos) {
46
 
                return pos / _bitsPerWord;
47
 
            }
48
 
 
49
 
            /** Bit offset offset for a given position */
50
 
            static size_t _bitOffset(size_t pos) {
51
 
                return pos % _bitsPerWord;
52
 
            }
53
 
 
54
 
            /** Bitmask for pos in a word */
55
 
            static _word _bitmask(size_t pos) {
56
 
                return ((_word) 1) << _bitOffset(pos);
57
 
            }
58
 
 
59
 
            /** Underlying word array */
60
 
            _word* _bits;
61
 
            size_t _size;
62
 
        public:
63
 
 
64
 
            /** Create a new empty bitfield */
65
 
            BitField(size_t size) {
66
 
                _size = size;
67
 
                _bits = new _word[_words()];
68
 
                clear();
69
 
            }
70
 
 
71
 
            /** Copy create a bitfield from another */
72
 
            BitField(const BitField& bf) {
73
 
                _size = bf._size;
74
 
                _bits = new _word[_words()];
75
 
                for (size_t i = 0; i < _words(); i++)
76
 
                    _bits[i] = bf._bits[i];
77
 
            }
78
 
 
79
 
            /** Destructor */
80
 
            ~BitField() {
81
 
                if (_bits) {
82
 
                    delete[] _bits;
83
 
                    _bits = NULL;
84
 
                }
85
 
            }
86
 
 
87
 
            /** Get the size of the bitfield*/
88
 
            size_t size() const {
89
 
                return _size;
90
 
            }
91
 
 
92
 
            /** Clear all bits */
93
 
            BitField& clear() {
94
 
                for (size_t i = 0; i < _words(); i++)
95
 
                    _bits[i] = 0;
96
 
                return *this;
97
 
            }
98
 
 
99
 
            /** Clear bit at position pos */
100
 
            BitField& clear(size_t pos) {
101
 
                _bits[_wordOffset(pos)] &= ~_bitmask(pos);
102
 
                return *this;
103
 
            }
104
 
 
105
 
            /** Test bit at position pos */
106
 
            bool test(size_t pos) const {
107
 
                return (_bits[_wordOffset(pos)] & _bitmask(pos)) != (_word) 0;
108
 
            }
109
 
 
110
 
            /** Set all bits */
111
 
            BitField& set() {
112
 
                memset(_bits, 0xff, sizeof (_word) * _words());
113
 
                //Sanitize
114
 
                _bits[_words() - 1] = _bits[_words() - 1] & ~((~(_word) 0) << _bitOffset(_size));
115
 
                return *this;
116
 
            }
117
 
 
118
 
            /** Set bit a position pos */
119
 
            BitField& set(size_t pos) {
120
 
                _bits[_wordOffset(pos)] |= _bitmask(pos);
121
 
                return *this;
122
 
            }
123
 
 
124
 
            /** Set bit a position pos to value */
125
 
            BitField& set(size_t pos, bool value) {
126
 
                if (value)
127
 
                    set(pos);
128
 
                else
129
 
                    clear(pos);
130
 
                return *this;
131
 
            }
132
 
 
133
 
            /** Flip all bits */
134
 
            BitField& flip() {
135
 
                for (size_t i = 0; i < _words() - 1; i++)
136
 
                    _bits[i] = ~_bits[i];
137
 
                //Sanitize
138
 
                _bits[_words() - 1] = ~_bits[_words() - 1] & ~((~(_word) 0) << _bitOffset(_size));
139
 
                return *this;
140
 
            }
141
 
 
142
 
            /** Flip bit at position pos */
143
 
            BitField& flip(size_t pos) {
144
 
                _bits[_wordOffset(pos)] ^= _bitmask(pos);
145
 
                return *this;
146
 
            }
147
 
 
148
 
            /** Test if any bit is set */
149
 
            bool any() const {
150
 
                for (size_t i = 0; i < _words(); i++)
151
 
                    if (_bits[i] != (_word) 0)
152
 
                        return true;
153
 
                return false;
154
 
            }
155
 
 
156
 
            /** Test if no bits are set */
157
 
            bool none() const {
158
 
                return !any();
159
 
            }
160
 
 
161
 
            /** Get the first set element, -1 if none */
162
 
            int first() const {
163
 
                for (size_t i = 0; i < _size; i++)
164
 
                    if (test(i))
165
 
                        return i;
166
 
                return -1;
167
 
            }
168
 
 
169
 
            BitField& operator=(const BitField& rhs) {
170
 
                for (size_t i = 0; i < _words(); i++)
171
 
                    _bits[i] = rhs._bits[i];
172
 
                return *this;
173
 
            }
174
 
 
175
 
            BitField& operator&=(const BitField& rhs) {
176
 
                for (size_t i = 0; i < _words(); i++)
177
 
                    _bits[i] &= rhs._bits[i];
178
 
                return *this;
179
 
            }
180
 
 
181
 
            BitField& operator|=(const BitField& rhs) {
182
 
                for (size_t i = 0; i < _words(); i++)
183
 
                    _bits[i] |= rhs._bits[i];
184
 
                return *this;
185
 
            }
186
 
 
187
 
            BitField& operator^=(const BitField& rhs) {
188
 
                for (size_t i = 0; i < _words(); i++)
189
 
                    _bits[i] ^= rhs._bits[i];
190
 
                return *this;
191
 
            }
192
 
 
193
 
            BitField operator~() const {
194
 
                return BitField(*this).flip();
195
 
            }
196
 
 
197
 
            bool operator==(const BitField& rhs) const {
198
 
                for (size_t i = 0; i < _words(); i++)
199
 
                    if (_bits[i] != rhs._bits[i])
200
 
                        return false;
201
 
                return true;
202
 
            }
203
 
 
204
 
            bool operator!=(const BitField& rhs) const {
205
 
                for (size_t i = 0; i < _words(); i++)
206
 
                    if (_bits[i] != rhs._bits[i])
207
 
                        return true;
208
 
                return false;
209
 
            }
210
 
        };
211
 
 
212
 
        inline BitField operator&(const BitField& lhs, const BitField& rhs) {
213
 
            BitField retval(lhs);
214
 
            retval &= rhs;
215
 
            return retval;
216
 
        }
217
 
 
218
 
        inline BitField operator|(const BitField& lhs, const BitField& rhs) {
219
 
            BitField retval(lhs);
220
 
            retval |= rhs;
221
 
            return retval;
222
 
        }
223
 
 
224
 
        inline BitField operator^(const BitField& lhs, const BitField& rhs) {
225
 
            BitField retval(lhs);
226
 
            retval ^= rhs;
227
 
            return retval;
228
 
        }
229
 
 
230
 
    } // Structures
231
 
} // PetriEngine
232
 
 
233
 
#endif // BITFIELD_H