1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2017 SRI International.
4 *
5 * Yices is free software: you can redistribute it and/or modify
6 * it under the terms of the GNU General Public License as published by
7 * the Free Software Foundation, either version 3 of the License, or
8 * (at your option) any later version.
9 *
10 * Yices is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 *
15 * You should have received a copy of the GNU General Public License
16 * along with Yices. If not, see <http://www.gnu.org/licenses/>.
17 */
18
19 /*
20 * BIT VECTORS
21 */
22
23 #ifndef __BIT_VECTORS_H
24 #define __BIT_VECTORS_H 1
25
26 #include <stdint.h>
27 #include <string.h>
28 #include <stdbool.h>
29 #include <assert.h>
30
31 #include "utils/memalloc.h"
32
33
34 typedef unsigned char byte_t;
35
36
37 /*
38 * Allocation of a bit vector of n bits (indexed from 0 to n-1)
39 * - not initialized
40 */
allocate_bitvector(uint32_t n)41 static inline byte_t *allocate_bitvector(uint32_t n) {
42 n = (n + 7) >> 3;
43 return safe_malloc(n);
44 }
45
46 /*
47 * Extend to n bits. New bits are uninitialized
48 */
extend_bitvector(byte_t * bv,uint32_t n)49 static inline byte_t *extend_bitvector(byte_t *bv, uint32_t n) {
50 n = (n + 7) >> 3;
51 return safe_realloc(bv, n);
52 }
53
54
55
56 /*
57 * Allocate a bitvector of n bits and initialize all to 0
58 */
allocate_bitvector0(uint32_t n)59 static inline byte_t *allocate_bitvector0(uint32_t n) {
60 byte_t *tmp;
61
62 n = (n + 7) >> 3;
63 tmp = (byte_t *) safe_malloc(n);
64 memset(tmp, 0, n);
65 return tmp;
66 }
67
68
69 /*
70 * Extend to n bits. Initialize all new bits to 0
71 * - n = new size
72 * - m = current size
73 * (for this to work, bv must be allocated via allocate_bitvector0)
74 */
extend_bitvector0(byte_t * bv,uint32_t n,uint32_t m)75 static inline byte_t *extend_bitvector0(byte_t *bv, uint32_t n, uint32_t m) {
76 byte_t *tmp;
77
78 n = (n + 7) >> 3;
79 m = (m + 7) >> 3;
80 assert(m <= n);
81 tmp = (byte_t *) safe_realloc(bv, n);
82 memset(tmp + m, 0, n - m);
83 return tmp;
84 }
85
86
87
88 /*
89 * Delete
90 */
delete_bitvector(byte_t * bv)91 static inline void delete_bitvector(byte_t *bv) {
92 safe_free(bv);
93 }
94
95
96 /*
97 * Clear all the bits:
98 * - n must be the full size of bv (as used when bv was allocated)
99 */
clear_bitvector(byte_t * bv,uint32_t n)100 static inline void clear_bitvector(byte_t *bv, uint32_t n) {
101 n = (n + 7) >> 3;
102 memset(bv, 0, n);
103 }
104
105
106 /*
107 * Set all the bits
108 * - n must be the full size of bv (as used when bv was allocated)
109 */
set_bitvector(byte_t * bv,uint32_t n)110 static inline void set_bitvector(byte_t *bv, uint32_t n) {
111 n = (n + 7) >> 3;
112 memset(bv, 0xff, n);
113 }
114
115
116 /*
117 * Set bit i
118 */
set_bit(byte_t * bv,uint32_t i)119 static inline void set_bit(byte_t *bv, uint32_t i) {
120 uint32_t j;
121 byte_t mask;
122
123 j = i >> 3;
124 mask = 1 << (i & 0x7);
125 bv[j] |= mask;
126 }
127
128 /*
129 * Clear bit i
130 */
clr_bit(byte_t * bv,uint32_t i)131 static inline void clr_bit(byte_t *bv, uint32_t i) {
132 uint32_t j;
133 byte_t mask;
134
135 j = i >> 3;
136 mask = 1 << (i & 0x7);
137 bv[j] &= ~mask;
138 }
139
140
141 /*
142 * Assign bit i: to 1 if bit is true, to 0 otherwise
143 */
assign_bit_old(byte_t * bv,uint32_t i,bool bit)144 static inline void assign_bit_old(byte_t *bv, uint32_t i, bool bit) {
145 uint32_t j;
146 byte_t mask;
147
148 j = i >> 3;
149 mask = 1 << (i & 0x7);
150 if (bit) {
151 bv[j] |= mask;
152 } else {
153 bv[j] &= ~mask;
154 }
155 }
156
157 // variant: without if-then-else
assign_bit(byte_t * bv,uint32_t i,bool bit)158 static inline void assign_bit(byte_t *bv, uint32_t i, bool bit) {
159 uint32_t j;
160 byte_t x, mask;
161
162 j = (i >> 3);
163 mask = 1 << (i & 0x7);
164 x = ((byte_t) bit) << (i & 0x7);
165 bv[j] ^= (bv[j] ^ x) & mask;
166 }
167
168
169 /*
170 * Flip bit i
171 */
flip_bit(byte_t * bv,uint32_t i)172 static inline void flip_bit(byte_t *bv, uint32_t i) {
173 uint32_t j;
174 byte_t mask;
175
176 j = i >> 3;
177 mask = 1 << (i & 0x7);
178 bv[j] ^= mask;
179 }
180
181 /*
182 * Test bit i: return 0 if bit i is 0, 1 otherwise
183 */
tst_bit(byte_t * bv,uint32_t i)184 static inline bool tst_bit(byte_t *bv, uint32_t i) {
185 uint32_t j;
186 byte_t mask;
187
188 j = i >> 3;
189 mask = 1 << (i & 0x7);
190 return bv[j] & mask; // converted to bool
191 }
192
193
194 #endif /* __BIT_VECTORS_H */
195