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 * OPERATIONS ON SMALL BITVECTOR CONSTANTS
21 */
22
23 /*
24 * A bitvector of size <= 64 can be stored compactly in a 64bit
25 * unsigned integer. The following operations normalize and
26 * manipulate bit vector constants in this representation.
27 *
28 * The data structures defined in bv_constants.h can be used
29 * for bitvector constants of larger sizes.
30 */
31
32 #ifndef __BV64_CONSTANTS_H
33 #define __BV64_CONSTANTS_H
34
35 #include <stdint.h>
36 #include <stdbool.h>
37 #include <stdio.h>
38 #include <assert.h>
39
40 #include "terms/rationals.h"
41
42
43 /*
44 * Mask for normalizing an n-bit constant where 0 < n <= 64
45 * - x & mask64(n) is the normalization of x
46 * (i.e., high-order bits are 0)
47 * - warning: shift by 64 is undefined in C
48 */
mask64(uint32_t n)49 static inline uint64_t mask64(uint32_t n) {
50 assert(0 < n && n <= 64);
51 return (~((uint64_t) 0)) >> (64 - n);
52 }
53
54
55 /*
56 * Normalize c modulo 2^n (set high-order bits to 0)
57 */
norm64(uint64_t c,uint32_t n)58 static inline uint64_t norm64(uint64_t c, uint32_t n) {
59 assert(0 < n && n <= 64);
60 return c & mask64(n);
61 }
62
63
64 /*
65 * Check whether c is equal to -1 modulo 2^n
66 */
bvconst64_is_minus_one(uint64_t c,uint32_t n)67 static inline bool bvconst64_is_minus_one(uint64_t c, uint32_t n) {
68 assert(0 < n && n <= 64);
69 return (c & mask64(n)) == mask64(n);
70 }
71
72
73 /*
74 * Mask to select the sign bit in an n-bit number
75 */
sgn_bit_mask64(uint32_t n)76 static inline uint64_t sgn_bit_mask64(uint32_t n) {
77 assert(0 < n && n <= 64);
78 return ((uint64_t) 1) << (n - 1);
79 }
80
81
82 /*
83 * Test whether bit k of c is 1 or 0
84 * - true means 1, false means 0
85 */
tst_bit64(uint64_t c,uint32_t k)86 static inline bool tst_bit64(uint64_t c, uint32_t k) {
87 assert(0 <= k && k < 64);
88 return c & (((uint64_t) 1) << k);
89 }
90
91
92 /*
93 * Clear or set bit k of c
94 */
clr_bit64(uint64_t c,uint32_t k)95 static inline uint64_t clr_bit64(uint64_t c, uint32_t k) {
96 assert(0 <= k && k < 64);
97 return c & ~(((uint64_t) 1) << k);
98 }
99
set_bit64(uint64_t c,uint32_t k)100 static inline uint64_t set_bit64(uint64_t c, uint32_t k) {
101 assert(0 <= k && k < 64);
102 return c | (((uint64_t) 1) << k);
103 }
104
105
106 /*
107 * Get the sign bit of c, interpreted as an n-bit 2s-complement
108 * number.
109 */
tst_sign_bit64(uint64_t c,uint32_t n)110 static inline bool tst_sign_bit64(uint64_t c, uint32_t n) {
111 assert(0 < n && n <= 64);
112 return tst_bit64(c, n-1);
113 }
114
is_neg64(uint64_t c,uint32_t n)115 static inline bool is_neg64(uint64_t c, uint32_t n) {
116 return tst_sign_bit64(c, n);
117 }
118
is_pos64(uint64_t c,uint32_t n)119 static inline bool is_pos64(uint64_t c, uint32_t n) {
120 return ! tst_sign_bit64(c, n);
121 }
122
123
124 /*
125 * Maximal and minimal n-bit signed number
126 */
max_signed64(uint32_t n)127 static inline uint64_t max_signed64(uint32_t n) {
128 assert(0 < n && n <= 64);
129 return (n == 1) ? 0 : mask64(n-1); // all bits 1, except the sign bit
130 }
131
min_signed64(uint32_t n)132 static inline uint64_t min_signed64(uint32_t n) {
133 return sgn_bit_mask64(n); // all bits 0, except the sign bit
134 }
135
136
137
138 /*
139 * Arithmetic and logical shift
140 */
141
142 /*
143 * Shift left: (a << b), padding with 0.
144 * - n = number of bits in a and b
145 * - if b is more than n, this returns 0b00000
146 * - the result is normalized
147 */
148 extern uint64_t bvconst64_lshl(uint64_t a, uint64_t b, uint32_t n);
149
150
151 /*
152 * Logical shift right: (a >> b), padding with 0
153 * - n = number of bits in a and b
154 * - if b is more than n, return 0b00000
155 * - the result is normalized.
156 */
157 extern uint64_t bvconst64_lshr(uint64_t a, uint64_t b, uint32_t n);
158
159
160 /*
161 * Arithmetic shift right: (a >> b), padding with a's sign bit
162 * - n = number of bits in a and b
163 * - if b is more than n, return 0b00000 or 0b11111 depending on a's sign bit
164 * - the result is normalized.
165 */
166 extern uint64_t bvconst64_ashr(uint64_t a, uint64_t b, uint32_t n);
167
168
169
170 /*
171 * Operations on constants interpreted as n-bit 2's complement numbers.
172 */
173
174 /*
175 * Convert c into a signed 64 bit number
176 */
177 extern int64_t signed_int64(uint64_t c, uint32_t n);
178
179
180 /*
181 * Check whether a >= b: both are interpreted as n-bit signed numbers
182 */
183 extern bool signed64_ge(uint64_t a, uint64_t b, uint32_t n);
184
185
186 /*
187 * Check whether a>b: both are interpreted as n-bit signed numbers
188 */
189 extern bool signed64_gt(uint64_t a, uint64_t b, uint32_t n);
190
191
192 /*
193 * Variants: a <= b and a < b
194 */
signed64_le(uint64_t a,uint64_t b,uint32_t n)195 static inline bool signed64_le(uint64_t a, uint64_t b, uint32_t n) {
196 return signed64_ge(b, a, n);
197 }
198
signed64_lt(uint64_t a,uint64_t b,uint32_t n)199 static inline bool signed64_lt(uint64_t a, uint64_t b, uint32_t n) {
200 return signed64_gt(b, a, n);
201 }
202
203
204
205 /*
206 * DIVISIONS
207 *
208 * These are the quotient and remainder operations defined in the SMT-LIB notation.
209 * They are identical to the usual division and remainder operation, except that a
210 * zero divider is allowed.
211 *
212 * All operations compute the quotient or remainder in the division of x by y.
213 * Both x and y must be normalized modulo 2^n, and the result is also normalized
214 * modulo 2^n,
215 *
216 * Unsigned division: x and y are interpreted as unsigned n-bit numbers
217 * bvconst64_udiv2z(x, y, n): quotient
218 * bvconst64_urem2z(x, y, n): remainder
219 *
220 * Signed division: x and y are interpreted as 2's complement n-bit numbers
221 * (This is 'truncated division' with rounding toward 0)
222 * bvconst64_sdiv2z(x, y, n): quotient in signed division
223 * bvconst64_srem2z(x, y, n): remainder in signed division
224 *
225 * Floor division: x and y are interpreted as 2's complement n-bit number.
226 * Rounding is toward minus infinity.
227 * bcconst64_smod2z(x, y, n): remainder
228 *
229 * Properties:
230 * a1 = a2 * (udiv a1 a2) + (urem a1 a2)
231 * a1 = a2 * (sdiv a1 a2) + (srem a1 a2)
232 * a1 = a2 * (floor a1/a2) + (smod a1 a2)
233 * (sdiv a1 a2) has the same sign as a1/a2
234 * (srem a1 a2) has the same sign as a1
235 * (smod a1 a2) has the same sign as a2
236 *
237 * For division by 0, we use the following rules:
238 * (udiv a 0) = 0b11...1
239 * (urem a 0) = a
240 * (sdiv a 0) = 0b111..1 if a >= 0
241 * (sdiv a 0) = 0b00..01 if a < 0
242 * (srem a 0) = a
243 * (smod a 0) = a
244 */
245 extern uint64_t bvconst64_udiv2z(uint64_t x, uint64_t y, uint32_t n);
246 extern uint64_t bvconst64_urem2z(uint64_t x, uint64_t y, uint32_t n);
247 extern uint64_t bvconst64_sdiv2z(uint64_t x, uint64_t y, uint32_t n);
248 extern uint64_t bvconst64_srem2z(uint64_t x, uint64_t y, uint32_t n);
249 extern uint64_t bvconst64_smod2z(uint64_t x, uint64_t y, uint32_t n);
250
251
252
253 /*
254 * Convert a string of '0's and '1's to a constant
255 * - n = number of bits (n must be between 1 and 64)
256 * - s must be at least n character long.
257 *
258 * Read the first n characters of s. All must be '0' and '1'
259 * - the string is interpreted as a big-endian format: the
260 * first character is the high order bit.
261 *
262 * If the string format is wrong, return -1 and leave *a unchanged.
263 * Otherwise, return 0 and store the result in *a (normalized modulo 2^n).
264 */
265 extern int32_t bvconst64_set_from_string(uint64_t *a, uint32_t n, char *s);
266
267
268 /*
269 * Convert a string interpreted as an hexadecimal number to a constant.
270 * - n = number of characters to read (n must be between 1 and 16)
271 * - s must be at least n character long.
272 *
273 * Read the first n characters of s.
274 * All must be in the ranges '0' to '9' or 'a' to 'f' or 'A' to 'F'.
275 * The string is read in big-endian format: first character defines
276 * the four high-order bits.
277 *
278 * Return -1 if the format is wrong (and leave *a unchanged).
279 * Return 0 otherwise and store the result in a, normalized modulo 2^4n.
280 */
281 extern int32_t bvconst64_set_from_hexa_string(uint64_t *a, uint32_t n, char *s);
282
283
284 /*
285 * Convert the n low-order bits of a rational q to a bitvector
286 * constant of n-bits
287 * - q must be an integer
288 */
289 extern uint64_t bvconst64_from_q(uint32_t n, rational_t *q);
290
291
292 /*
293 * Display a in binary format. n = number of bits
294 */
295 extern void bvconst64_print(FILE *f, uint64_t a, uint32_t n);
296
297
298 /*
299 * Store the n lowest order bits of bv into a
300 * - as an integer array: a[i] = bit i of bv (either 0 or 1)
301 * - n must be positive and no more than 64
302 */
303 extern void bvconst64_get_array(uint64_t bv, int32_t *a, uint32_t n);
304
305
306
307 #endif /* __BV64_CONSTANTS_H */
308