1 /* Boolector: Satisfiability Modulo Theories (SMT) solver.
2 *
3 * Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
4 *
5 * This file is part of Boolector.
6 * See COPYING for more information on using this software.
7 */
8
9 #include "btoraigvec.h"
10 #include "btorcore.h"
11 #include "btoropt.h"
12 #include "utils/btoraigmap.h"
13 #include "utils/btorutil.h"
14
15 #include <assert.h>
16 #include <limits.h>
17 #include <stdlib.h>
18 #include <string.h>
19
20 /*------------------------------------------------------------------------*/
21
22 static BtorAIGVec *
new_aigvec(BtorAIGVecMgr * avmgr,uint32_t width)23 new_aigvec (BtorAIGVecMgr *avmgr, uint32_t width)
24 {
25 assert (avmgr);
26 assert (width > 0);
27
28 BtorAIGVec *result;
29
30 result = btor_mem_malloc (avmgr->btor->mm,
31 sizeof (BtorAIGVec) + sizeof (BtorAIG *) * width);
32 result->width = width;
33 avmgr->cur_num_aigvecs++;
34 if (avmgr->max_num_aigvecs < avmgr->cur_num_aigvecs)
35 avmgr->max_num_aigvecs = avmgr->cur_num_aigvecs;
36 return result;
37 }
38
39 BtorAIGVec *
btor_aigvec_const(BtorAIGVecMgr * avmgr,const BtorBitVector * bits)40 btor_aigvec_const (BtorAIGVecMgr *avmgr, const BtorBitVector *bits)
41 {
42 assert (avmgr);
43 assert (bits);
44
45 BtorAIGVec *result;
46 uint32_t i, width;
47 width = btor_bv_get_width (bits);
48 assert (width > 0);
49 result = new_aigvec (avmgr, width);
50 for (i = 0; i < width; i++)
51 result->aigs[i] =
52 !btor_bv_get_bit (bits, width - 1 - i) ? BTOR_AIG_FALSE : BTOR_AIG_TRUE;
53 return result;
54 }
55
56 BtorAIGVec *
btor_aigvec_zero(BtorAIGVecMgr * avmgr,uint32_t width)57 btor_aigvec_zero (BtorAIGVecMgr *avmgr, uint32_t width)
58 {
59 assert (avmgr);
60 assert (width);
61
62 BtorAIGVec *result;
63 uint32_t i;
64 result = new_aigvec (avmgr, width);
65 for (i = 0; i < width; i++) result->aigs[i] = BTOR_AIG_FALSE;
66 return result;
67 }
68
69 BtorAIGVec *
btor_aigvec_var(BtorAIGVecMgr * avmgr,uint32_t width)70 btor_aigvec_var (BtorAIGVecMgr *avmgr, uint32_t width)
71 {
72 assert (avmgr);
73 assert (width > 0);
74
75 BtorAIGVec *result;
76 uint32_t i;
77
78 result = new_aigvec (avmgr, width);
79 for (i = 1; i <= width; i++)
80 result->aigs[width - i] = btor_aig_var (avmgr->amgr);
81 return result;
82 }
83
84 void
btor_aigvec_invert(BtorAIGVecMgr * avmgr,BtorAIGVec * av)85 btor_aigvec_invert (BtorAIGVecMgr *avmgr, BtorAIGVec *av)
86 {
87 uint32_t i, width;
88 (void) avmgr;
89 assert (avmgr);
90 assert (av);
91 assert (av->width > 0);
92 width = av->width;
93 for (i = 0; i < width; i++) av->aigs[i] = BTOR_INVERT_AIG (av->aigs[i]);
94 }
95
96 BtorAIGVec *
btor_aigvec_not(BtorAIGVecMgr * avmgr,BtorAIGVec * av)97 btor_aigvec_not (BtorAIGVecMgr *avmgr, BtorAIGVec *av)
98 {
99 BtorAIGVec *result;
100 uint32_t i, width;
101 assert (avmgr);
102 assert (av);
103 assert (av->width > 0);
104 width = av->width;
105 result = new_aigvec (avmgr, width);
106 for (i = 0; i < width; i++)
107 result->aigs[i] = btor_aig_not (avmgr->amgr, av->aigs[i]);
108 return result;
109 }
110
111 BtorAIGVec *
btor_aigvec_slice(BtorAIGVecMgr * avmgr,BtorAIGVec * av,uint32_t upper,uint32_t lower)112 btor_aigvec_slice (BtorAIGVecMgr *avmgr,
113 BtorAIGVec *av,
114 uint32_t upper,
115 uint32_t lower)
116 {
117 BtorAIGVec *result;
118 uint32_t i, width, diff, counter;
119 assert (avmgr);
120 assert (av);
121 assert (av->width > 0);
122 assert (upper < av->width);
123 assert (lower <= upper);
124 counter = 0;
125 width = av->width;
126 diff = upper - lower;
127 result = new_aigvec (avmgr, diff + 1);
128 for (i = width - upper - 1; i <= width - upper - 1 + diff; i++)
129 result->aigs[counter++] = btor_aig_copy (avmgr->amgr, av->aigs[i]);
130 return result;
131 }
132
133 BtorAIGVec *
btor_aigvec_and(BtorAIGVecMgr * avmgr,BtorAIGVec * av1,BtorAIGVec * av2)134 btor_aigvec_and (BtorAIGVecMgr *avmgr, BtorAIGVec *av1, BtorAIGVec *av2)
135 {
136 BtorAIGVec *result;
137 uint32_t i, width;
138 assert (avmgr);
139 assert (av1);
140 assert (av2);
141 assert (av1->width == av2->width);
142 assert (av1->width > 0);
143 width = av1->width;
144 result = new_aigvec (avmgr, width);
145 for (i = 0; i < width; i++)
146 result->aigs[i] = btor_aig_and (avmgr->amgr, av1->aigs[i], av2->aigs[i]);
147 return result;
148 }
149
150 static BtorAIG *
lt_aigvec(BtorAIGVecMgr * avmgr,BtorAIGVec * av1,BtorAIGVec * av2)151 lt_aigvec (BtorAIGVecMgr *avmgr, BtorAIGVec *av1, BtorAIGVec *av2)
152 {
153 BtorAIGMgr *amgr;
154 BtorAIG *res, *tmp, *term0, *term1;
155 uint32_t i, j;
156
157 amgr = avmgr->amgr;
158 res = BTOR_AIG_FALSE;
159 for (j = 1, i = av1->width - 1; j <= av1->width; j++, i--)
160 {
161 term0 = btor_aig_and (amgr, av1->aigs[i], BTOR_INVERT_AIG (av2->aigs[i]));
162
163 tmp = btor_aig_and (amgr, BTOR_INVERT_AIG (term0), res);
164 btor_aig_release (amgr, term0);
165 btor_aig_release (amgr, res);
166 res = tmp;
167
168 term1 = btor_aig_and (amgr, BTOR_INVERT_AIG (av1->aigs[i]), av2->aigs[i]);
169
170 tmp = btor_aig_or (amgr, term1, res);
171 btor_aig_release (amgr, term1);
172 btor_aig_release (amgr, res);
173 res = tmp;
174 }
175
176 return res;
177 }
178
179 BtorAIGVec *
btor_aigvec_ult(BtorAIGVecMgr * avmgr,BtorAIGVec * av1,BtorAIGVec * av2)180 btor_aigvec_ult (BtorAIGVecMgr *avmgr, BtorAIGVec *av1, BtorAIGVec *av2)
181 {
182 BtorAIGVec *result;
183 assert (avmgr);
184 assert (av1);
185 assert (av2);
186 assert (av1->width == av2->width);
187 assert (av1->width > 0);
188 result = new_aigvec (avmgr, 1);
189 result->aigs[0] = lt_aigvec (avmgr, av1, av2);
190 return result;
191 }
192
193 BtorAIGVec *
btor_aigvec_eq(BtorAIGVecMgr * avmgr,BtorAIGVec * av1,BtorAIGVec * av2)194 btor_aigvec_eq (BtorAIGVecMgr *avmgr, BtorAIGVec *av1, BtorAIGVec *av2)
195 {
196 BtorAIGMgr *amgr;
197 BtorAIGVec *result;
198 BtorAIG *result_aig, *temp1, *temp2;
199 uint32_t i, width;
200 assert (avmgr);
201 assert (av1);
202 assert (av2);
203 assert (av1->width == av2->width);
204 assert (av1->width > 0);
205 amgr = avmgr->amgr;
206 width = av1->width;
207 result = new_aigvec (avmgr, 1);
208 result_aig = btor_aig_eq (amgr, av1->aigs[0], av2->aigs[0]);
209 for (i = 1; i < width; i++)
210 {
211 temp1 = btor_aig_eq (amgr, av1->aigs[i], av2->aigs[i]);
212 temp2 = btor_aig_and (amgr, result_aig, temp1);
213 btor_aig_release (amgr, temp1);
214 btor_aig_release (amgr, result_aig);
215 result_aig = temp2;
216 }
217 result->aigs[0] = result_aig;
218 return result;
219 }
220
221 static BtorAIG *
half_adder(BtorAIGMgr * amgr,BtorAIG * x,BtorAIG * y,BtorAIG ** cout)222 half_adder (BtorAIGMgr *amgr, BtorAIG *x, BtorAIG *y, BtorAIG **cout)
223 {
224 BtorAIG *res, *x_and_y, *not_x, *not_y, *not_x_and_not_y, *x_xnor_y;
225 x_and_y = btor_aig_and (amgr, x, y);
226 not_x = BTOR_INVERT_AIG (x);
227 not_y = BTOR_INVERT_AIG (y);
228 not_x_and_not_y = btor_aig_and (amgr, not_x, not_y);
229 x_xnor_y = btor_aig_or (amgr, x_and_y, not_x_and_not_y);
230 res = BTOR_INVERT_AIG (x_xnor_y);
231 *cout = x_and_y;
232 btor_aig_release (amgr, not_x_and_not_y);
233 return res;
234 }
235
236 static BtorAIG *
full_adder(BtorAIGMgr * amgr,BtorAIG * x,BtorAIG * y,BtorAIG * cin,BtorAIG ** cout)237 full_adder (
238 BtorAIGMgr *amgr, BtorAIG *x, BtorAIG *y, BtorAIG *cin, BtorAIG **cout)
239 {
240 BtorAIG *sum, *c1, *c2, *res;
241 sum = half_adder (amgr, x, y, &c1);
242 res = half_adder (amgr, sum, cin, &c2);
243 *cout = btor_aig_or (amgr, c1, c2);
244 btor_aig_release (amgr, sum);
245 btor_aig_release (amgr, c1);
246 btor_aig_release (amgr, c2);
247 return res;
248 }
249
250 static int32_t
compare_aigvec_lsb_first(BtorAIGVec * a,BtorAIGVec * b)251 compare_aigvec_lsb_first (BtorAIGVec *a, BtorAIGVec *b)
252 {
253 uint32_t width, i;
254 int32_t res;
255 assert (a);
256 assert (b);
257 width = a->width;
258 assert (width == b->width);
259 res = 0;
260 for (i = 0; !res && i < width; i++)
261 res = btor_aig_compare (a->aigs[i], b->aigs[i]);
262 return res;
263 }
264
265 BtorAIGVec *
btor_aigvec_add(BtorAIGVecMgr * avmgr,BtorAIGVec * av1,BtorAIGVec * av2)266 btor_aigvec_add (BtorAIGVecMgr *avmgr, BtorAIGVec *av1, BtorAIGVec *av2)
267 {
268 assert (avmgr);
269 assert (av1);
270 assert (av2);
271 assert (av1->width == av2->width);
272 assert (av1->width > 0);
273
274 BtorAIGMgr *amgr;
275 BtorAIGVec *result;
276 BtorAIG *cout, *cin;
277 uint32_t i, j;
278
279 if (btor_opt_get (avmgr->btor, BTOR_OPT_SORT_AIGVEC) > 0
280 && compare_aigvec_lsb_first (av1, av2) > 0)
281 {
282 BTOR_SWAP (BtorAIGVec *, av1, av2);
283 }
284
285 amgr = avmgr->amgr;
286 result = new_aigvec (avmgr, av1->width);
287 cout = cin = BTOR_AIG_FALSE; /* for 'cout' to avoid warning */
288 for (j = 1, i = av1->width - 1; j <= av1->width; j++, i--)
289 {
290 result->aigs[i] = full_adder (amgr, av1->aigs[i], av2->aigs[i], cin, &cout);
291 btor_aig_release (amgr, cin);
292 cin = cout;
293 }
294 btor_aig_release (amgr, cout);
295 return result;
296 }
297
298 static BtorAIGVec *
sll_n_bits_aigvec(BtorAIGVecMgr * avmgr,BtorAIGVec * av,uint32_t n,BtorAIG * shift)299 sll_n_bits_aigvec (BtorAIGVecMgr *avmgr,
300 BtorAIGVec *av,
301 uint32_t n,
302 BtorAIG *shift)
303 {
304 BtorAIGMgr *amgr;
305 BtorAIGVec *result;
306 BtorAIG *and1, *and2, *not_shift;
307 uint32_t i, j, width;
308 assert (avmgr);
309 assert (av);
310 assert (av->width > 0);
311 assert (n < av->width);
312 if (n == 0) return btor_aigvec_copy (avmgr, av);
313 amgr = avmgr->amgr;
314 width = av->width;
315 not_shift = btor_aig_not (amgr, shift);
316 result = new_aigvec (avmgr, width);
317 for (i = 0; i < width - n; i++)
318 {
319 and1 = btor_aig_and (amgr, av->aigs[i], not_shift);
320 and2 = btor_aig_and (amgr, av->aigs[i + n], shift);
321 result->aigs[i] = btor_aig_or (amgr, and1, and2);
322 btor_aig_release (amgr, and1);
323 btor_aig_release (amgr, and2);
324 }
325 for (j = width - n; j < width; j++)
326 result->aigs[j] = btor_aig_and (amgr, av->aigs[j], not_shift);
327 btor_aig_release (amgr, not_shift);
328 return result;
329 }
330
331 static BtorAIGVec *
translate_shift(BtorAIGVecMgr * avmgr,BtorAIGVec * av1,BtorAIGVec * av2,BtorAIGVec * (* fun)(BtorAIGVecMgr *,BtorAIGVec *,BtorAIGVec *))332 translate_shift (BtorAIGVecMgr *avmgr,
333 BtorAIGVec *av1,
334 BtorAIGVec *av2,
335 BtorAIGVec *(*fun) (BtorAIGVecMgr *,
336 BtorAIGVec *,
337 BtorAIGVec *) )
338 {
339 assert (avmgr);
340 assert (av1);
341 assert (av2);
342 assert (av1->width);
343 assert (av2->width);
344
345 BtorAIGVec *res, *av_cond, *av_then, *av_else;
346 BtorAIGVec *tmp, *zero, *upper2, *lower2, *av1_new, *av2_new;
347 uint32_t width, pow2, width_shift, delta1, delta2;
348
349 width = av1->width;
350
351 /* When represented as AIG vectors, we require that the vector to be shifted
352 * has a power of 2 width, and the shift width is log2 of this width. The
353 * given vectors av1 and av2 have the same bit-width, which is not necessarily
354 * a power of 2. Hence the requirement for translation.
355 *
356 * First, we determine the smallest power of 2 that is greater/equal than
357 * the bit-width of the given AIG vectors such that width_shift = log2 (pow2).
358 */
359 for (pow2 = 1, width_shift = 0; pow2 < width; pow2 *= 2) width_shift++;
360 assert (pow2 == (1u << width_shift));
361
362 if (width == 1)
363 {
364 assert (pow2 == 1);
365 assert (width_shift == 0);
366
367 tmp = btor_aigvec_not (avmgr, av2);
368 res = btor_aigvec_and (avmgr, av1, tmp);
369 btor_aigvec_release_delete (avmgr, tmp);
370 }
371 else
372 {
373 assert (width > 1);
374 assert (width <= pow2);
375
376 /* the delta (in # bits) for 'pow2' and 'width' */
377 delta1 = pow2 - width;
378 /* the delta (in # bits) for 'width' and 'width_shift' (= log2(pow2)) */
379 delta2 = width - width_shift;
380
381 assert (width_shift > 0);
382
383 upper2 = btor_aigvec_slice (avmgr, av2, width - 1, width - delta2);
384 lower2 = btor_aigvec_slice (avmgr, av2, width_shift - 1, 0);
385
386 assert (upper2->width == delta2);
387 assert (lower2->width == width_shift);
388
389 /**
390 * if shift width is >= bit-width, result is 0
391 * -> we translate given shift to
392 * ite (shift width >= bit-width, 0, shift (av1_new, av2_new))
393 * where
394 * - 'shift' is the given shift function (sll, srl) and
395 * - 'av1_new' and 'av2_new' are the given vectors converted to the
396 * required widths 'pow2' and 'width_shift'.
397 */
398
399 /* condition for ite */
400 if (delta2 > 1)
401 {
402 /* 0_[upper2->width] */
403 zero = btor_aigvec_zero (avmgr, delta2);
404 /* redor: ~(0_[upper2->width] = upper2) */
405 tmp = btor_aigvec_eq (avmgr, zero, upper2);
406 av_cond = btor_aigvec_not (avmgr, tmp);
407 btor_aigvec_release_delete (avmgr, tmp);
408 btor_aigvec_release_delete (avmgr, zero);
409 }
410 else
411 {
412 av_cond = btor_aigvec_copy (avmgr, upper2);
413 }
414 btor_aigvec_release_delete (avmgr, upper2);
415
416 /* then branch for ite */
417 av_then = btor_aigvec_zero (avmgr, width);
418
419 /* else branch for ite */
420 if (!delta1)
421 {
422 av1_new = btor_aigvec_copy (avmgr, av1);
423 }
424 else
425 {
426 tmp = btor_aigvec_zero (avmgr, delta1);
427 av1_new = btor_aigvec_concat (avmgr, tmp, av1);
428 btor_aigvec_release_delete (avmgr, tmp);
429 }
430 assert (av1_new->width == pow2);
431 av2_new = lower2;
432 av_else = fun (avmgr, av1_new, av2_new);
433 btor_aigvec_release_delete (avmgr, av1_new);
434 btor_aigvec_release_delete (avmgr, av2_new);
435 if (delta1 > 0)
436 {
437 tmp = btor_aigvec_slice (avmgr, av_else, width - 1, 0);
438 btor_aigvec_release_delete (avmgr, av_else);
439 av_else = tmp;
440 }
441
442 res = btor_aigvec_cond (avmgr, av_cond, av_then, av_else);
443
444 btor_aigvec_release_delete (avmgr, av_cond);
445 btor_aigvec_release_delete (avmgr, av_then);
446 btor_aigvec_release_delete (avmgr, av_else);
447 }
448 return res;
449 }
450
451 static BtorAIGVec *
aigvec_sll(BtorAIGVecMgr * avmgr,BtorAIGVec * av1,BtorAIGVec * av2)452 aigvec_sll (BtorAIGVecMgr *avmgr, BtorAIGVec *av1, BtorAIGVec *av2)
453 {
454 assert (avmgr);
455 assert (av1);
456 assert (av2);
457 assert (av1->width);
458 assert (btor_util_is_power_of_2 (av1->width));
459 assert (btor_util_log_2 (av1->width) == av2->width);
460
461 BtorAIGVec *result, *temp;
462 uint32_t i, j, width;
463
464 width = av2->width;
465 result = sll_n_bits_aigvec (avmgr, av1, 1, av2->aigs[av2->width - 1]);
466 for (j = 2, i = width - 2; j <= width; j++, i--)
467 {
468 temp = result;
469 result = sll_n_bits_aigvec (
470 avmgr, temp, btor_util_pow_2 (width - i - 1), av2->aigs[i]);
471 btor_aigvec_release_delete (avmgr, temp);
472 }
473 return result;
474 }
475
476 BtorAIGVec *
btor_aigvec_sll(BtorAIGVecMgr * avmgr,BtorAIGVec * av1,BtorAIGVec * av2)477 btor_aigvec_sll (BtorAIGVecMgr *avmgr, BtorAIGVec *av1, BtorAIGVec *av2)
478 {
479 assert (avmgr);
480 assert (av1);
481 assert (av2);
482 assert (av1->width);
483 assert (av1->width == av2->width);
484 return translate_shift (avmgr, av1, av2, aigvec_sll);
485 }
486
487 static BtorAIGVec *
srl_n_bits_aigvec(BtorAIGVecMgr * avmgr,BtorAIGVec * av,uint32_t n,BtorAIG * shift)488 srl_n_bits_aigvec (BtorAIGVecMgr *avmgr,
489 BtorAIGVec *av,
490 uint32_t n,
491 BtorAIG *shift)
492 {
493 BtorAIGMgr *amgr;
494 BtorAIGVec *result;
495 BtorAIG *and1, *and2, *not_shift;
496 uint32_t i, width;
497 assert (avmgr);
498 assert (av);
499 assert (av->width > 0);
500 assert (n < av->width);
501 if (n == 0) return btor_aigvec_copy (avmgr, av);
502 amgr = avmgr->amgr;
503 width = av->width;
504 not_shift = btor_aig_not (amgr, shift);
505 result = new_aigvec (avmgr, width);
506 for (i = 0; i < n; i++)
507 result->aigs[i] = btor_aig_and (amgr, av->aigs[i], not_shift);
508 for (i = n; i < width; i++)
509 {
510 and1 = btor_aig_and (amgr, av->aigs[i], not_shift);
511 and2 = btor_aig_and (amgr, av->aigs[i - n], shift);
512 result->aigs[i] = btor_aig_or (amgr, and1, and2);
513 btor_aig_release (amgr, and1);
514 btor_aig_release (amgr, and2);
515 }
516 btor_aig_release (amgr, not_shift);
517 return result;
518 }
519
520 static BtorAIGVec *
aigvec_srl(BtorAIGVecMgr * avmgr,BtorAIGVec * av1,BtorAIGVec * av2)521 aigvec_srl (BtorAIGVecMgr *avmgr, BtorAIGVec *av1, BtorAIGVec *av2)
522 {
523 BtorAIGVec *result, *temp;
524 uint32_t i, j, width;
525 assert (avmgr);
526 assert (av1);
527 assert (av2);
528 assert (av1->width);
529 assert (btor_util_is_power_of_2 (av1->width));
530 assert (btor_util_log_2 (av1->width) == av2->width);
531 width = av2->width;
532 result = srl_n_bits_aigvec (avmgr, av1, 1, av2->aigs[av2->width - 1]);
533 for (j = 2, i = width - 2; j <= width; j++, i--)
534 {
535 temp = result;
536 result = srl_n_bits_aigvec (
537 avmgr, temp, btor_util_pow_2 (width - i - 1), av2->aigs[i]);
538 btor_aigvec_release_delete (avmgr, temp);
539 }
540 return result;
541 }
542
543 BtorAIGVec *
btor_aigvec_srl(BtorAIGVecMgr * avmgr,BtorAIGVec * av1,BtorAIGVec * av2)544 btor_aigvec_srl (BtorAIGVecMgr *avmgr, BtorAIGVec *av1, BtorAIGVec *av2)
545 {
546 assert (avmgr);
547 assert (av1);
548 assert (av2);
549 assert (av1->width);
550 assert (av1->width == av2->width);
551 return translate_shift (avmgr, av1, av2, aigvec_srl);
552 }
553
554 static BtorAIGVec *
mul_aigvec(BtorAIGVecMgr * avmgr,BtorAIGVec * a,BtorAIGVec * b)555 mul_aigvec (BtorAIGVecMgr *avmgr, BtorAIGVec *a, BtorAIGVec *b)
556 {
557 BtorAIG *cin, *cout, *and, *tmp;
558 BtorAIGMgr *amgr;
559 BtorAIGVec *res;
560 uint32_t i, j, k, ik, jk, width;
561
562 width = a->width;
563 amgr = btor_aigvec_get_aig_mgr (avmgr);
564
565 assert (width > 0);
566 assert (width == b->width);
567
568 if (btor_opt_get (avmgr->btor, BTOR_OPT_SORT_AIGVEC) > 0
569 && compare_aigvec_lsb_first (a, b) > 0)
570 {
571 BTOR_SWAP (BtorAIGVec *, a, b);
572 }
573
574 res = new_aigvec (avmgr, width);
575
576 for (k = 0; k < width; k++)
577 res->aigs[k] = btor_aig_and (amgr, a->aigs[k], b->aigs[width - 1]);
578
579 for (ik = 2, i = width - 2; ik <= width; ik++, i--)
580 {
581 cout = BTOR_AIG_FALSE;
582 for (jk = 0, j = i; jk <= i; jk++, j--)
583 {
584 and = btor_aig_and (amgr, a->aigs[width - 1 - i + j], b->aigs[i]);
585 tmp = res->aigs[j];
586 cin = cout;
587 res->aigs[j] = full_adder (amgr, tmp, and, cin, &cout);
588 btor_aig_release (amgr, and);
589 btor_aig_release (amgr, tmp);
590 btor_aig_release (amgr, cin);
591 }
592 btor_aig_release (amgr, cout);
593 }
594
595 return res;
596 }
597
598 BtorAIGVec *
btor_aigvec_mul(BtorAIGVecMgr * avmgr,BtorAIGVec * a,BtorAIGVec * b)599 btor_aigvec_mul (BtorAIGVecMgr *avmgr, BtorAIGVec *a, BtorAIGVec *b)
600 {
601 return mul_aigvec (avmgr, a, b);
602 }
603
604 static void
SC_GATE_CO_aigvec(BtorAIGMgr * amgr,BtorAIG ** CO,BtorAIG * R,BtorAIG * D,BtorAIG * CI)605 SC_GATE_CO_aigvec (
606 BtorAIGMgr *amgr, BtorAIG **CO, BtorAIG *R, BtorAIG *D, BtorAIG *CI)
607 {
608 BtorAIG *D_or_CI, *D_and_CI, *M;
609 D_or_CI = btor_aig_or (amgr, D, CI);
610 D_and_CI = btor_aig_and (amgr, D, CI);
611 M = btor_aig_and (amgr, D_or_CI, R);
612 *CO = btor_aig_or (amgr, M, D_and_CI);
613 btor_aig_release (amgr, D_or_CI);
614 btor_aig_release (amgr, D_and_CI);
615 btor_aig_release (amgr, M);
616 }
617
618 static void
SC_GATE_S_aigvec(BtorAIGMgr * amgr,BtorAIG ** S,BtorAIG * R,BtorAIG * D,BtorAIG * CI,BtorAIG * Q)619 SC_GATE_S_aigvec (BtorAIGMgr *amgr,
620 BtorAIG **S,
621 BtorAIG *R,
622 BtorAIG *D,
623 BtorAIG *CI,
624 BtorAIG *Q)
625 {
626 BtorAIG *D_and_CI, *D_or_CI;
627 BtorAIG *T2_or_R, *T2_and_R;
628 BtorAIG *T1, *T2;
629 D_or_CI = btor_aig_or (amgr, D, CI);
630 D_and_CI = btor_aig_and (amgr, D, CI);
631 T1 = btor_aig_and (amgr, D_or_CI, BTOR_INVERT_AIG (D_and_CI));
632 T2 = btor_aig_and (amgr, T1, Q);
633 T2_or_R = btor_aig_or (amgr, T2, R);
634 T2_and_R = btor_aig_and (amgr, T2, R);
635 *S = btor_aig_and (amgr, T2_or_R, BTOR_INVERT_AIG (T2_and_R));
636 btor_aig_release (amgr, T1);
637 btor_aig_release (amgr, T2);
638 btor_aig_release (amgr, D_and_CI);
639 btor_aig_release (amgr, D_or_CI);
640 btor_aig_release (amgr, T2_and_R);
641 btor_aig_release (amgr, T2_or_R);
642 }
643
644 static void
udiv_urem_aigvec(BtorAIGVecMgr * avmgr,BtorAIGVec * Ain,BtorAIGVec * Din,BtorAIGVec ** Qptr,BtorAIGVec ** Rptr)645 udiv_urem_aigvec (BtorAIGVecMgr *avmgr,
646 BtorAIGVec *Ain,
647 BtorAIGVec *Din,
648 BtorAIGVec **Qptr,
649 BtorAIGVec **Rptr)
650 {
651 BtorAIG **A, **nD, ***S, ***C;
652 BtorAIGVec *Q, *R;
653 BtorAIGMgr *amgr;
654 BtorMemMgr *mem;
655 uint32_t size, i, j;
656
657 size = Ain->width;
658 assert (size > 0);
659
660 amgr = btor_aigvec_get_aig_mgr (avmgr);
661 mem = avmgr->btor->mm;
662
663 BTOR_NEWN (mem, A, size);
664 for (i = 0; i < size; i++) A[i] = Ain->aigs[size - 1 - i];
665
666 BTOR_NEWN (mem, nD, size);
667 for (i = 0; i < size; i++) nD[i] = BTOR_INVERT_AIG (Din->aigs[size - 1 - i]);
668
669 BTOR_NEWN (mem, S, size + 1);
670 for (j = 0; j <= size; j++)
671 {
672 BTOR_NEWN (mem, S[j], size + 1);
673 for (i = 0; i <= size; i++) S[j][i] = BTOR_AIG_FALSE;
674 }
675
676 BTOR_NEWN (mem, C, size + 1);
677 for (j = 0; j <= size; j++)
678 {
679 BTOR_NEWN (mem, C[j], size + 1);
680 for (i = 0; i <= size; i++) C[j][i] = BTOR_AIG_FALSE;
681 }
682
683 R = new_aigvec (avmgr, size);
684 Q = new_aigvec (avmgr, size);
685
686 for (j = 0; j <= size - 1; j++)
687 {
688 S[j][0] = btor_aig_copy (amgr, A[size - j - 1]);
689 C[j][0] = BTOR_AIG_TRUE;
690
691 for (i = 0; i <= size - 1; i++)
692 SC_GATE_CO_aigvec (amgr, &C[j][i + 1], S[j][i], nD[i], C[j][i]);
693
694 Q->aigs[j] = btor_aig_or (amgr, C[j][size], S[j][size]);
695
696 for (i = 0; i <= size - 1; i++)
697 SC_GATE_S_aigvec (
698 amgr, &S[j + 1][i + 1], S[j][i], nD[i], C[j][i], Q->aigs[j]);
699 }
700
701 for (i = size; i >= 1; i--)
702 R->aigs[size - i] = btor_aig_copy (amgr, S[size][i]);
703
704 for (j = 0; j <= size; j++)
705 {
706 for (i = 0; i <= size; i++) btor_aig_release (amgr, C[j][i]);
707 BTOR_DELETEN (mem, C[j], size + 1);
708 }
709 BTOR_DELETEN (mem, C, size + 1);
710
711 for (j = 0; j <= size; j++)
712 {
713 for (i = 0; i <= size; i++) btor_aig_release (amgr, S[j][i]);
714 BTOR_DELETEN (mem, S[j], size + 1);
715 }
716 BTOR_DELETEN (mem, S, size + 1);
717
718 BTOR_DELETEN (mem, nD, size);
719 BTOR_DELETEN (mem, A, size);
720
721 *Qptr = Q;
722 *Rptr = R;
723 }
724
725 BtorAIGVec *
btor_aigvec_udiv(BtorAIGVecMgr * avmgr,BtorAIGVec * av1,BtorAIGVec * av2)726 btor_aigvec_udiv (BtorAIGVecMgr *avmgr, BtorAIGVec *av1, BtorAIGVec *av2)
727 {
728 BtorAIGVec *quotient = 0;
729 BtorAIGVec *remainder = 0;
730 assert (avmgr);
731 assert (av1);
732 assert (av2);
733 assert (av1->width == av2->width);
734 assert (av1->width > 0);
735 udiv_urem_aigvec (avmgr, av1, av2, "ient, &remainder);
736 btor_aigvec_release_delete (avmgr, remainder);
737 return quotient;
738 }
739
740 BtorAIGVec *
btor_aigvec_urem(BtorAIGVecMgr * avmgr,BtorAIGVec * av1,BtorAIGVec * av2)741 btor_aigvec_urem (BtorAIGVecMgr *avmgr, BtorAIGVec *av1, BtorAIGVec *av2)
742 {
743 BtorAIGVec *quotient, *remainder;
744 assert (avmgr);
745 assert (av1);
746 assert (av2);
747 assert (av1->width == av2->width);
748 assert (av1->width > 0);
749 udiv_urem_aigvec (avmgr, av1, av2, "ient, &remainder);
750 btor_aigvec_release_delete (avmgr, quotient);
751 return remainder;
752 }
753
754 BtorAIGVec *
btor_aigvec_concat(BtorAIGVecMgr * avmgr,BtorAIGVec * av1,BtorAIGVec * av2)755 btor_aigvec_concat (BtorAIGVecMgr *avmgr, BtorAIGVec *av1, BtorAIGVec *av2)
756 {
757 BtorAIGMgr *amgr;
758 BtorAIGVec *result;
759 uint32_t i, pos, len_av1, len_av2;
760 assert (avmgr);
761 assert (av1);
762 assert (av2);
763 assert (av1->width > 0);
764 assert (av2->width > 0);
765 assert (INT32_MAX - av1->width >= av2->width);
766 pos = 0;
767 amgr = avmgr->amgr;
768 len_av1 = av1->width;
769 len_av2 = av2->width;
770 result = new_aigvec (avmgr, len_av1 + len_av2);
771 for (i = 0; i < len_av1; i++)
772 result->aigs[pos++] = btor_aig_copy (amgr, av1->aigs[i]);
773 for (i = 0; i < len_av2; i++)
774 result->aigs[pos++] = btor_aig_copy (amgr, av2->aigs[i]);
775 return result;
776 }
777
778 BtorAIGVec *
btor_aigvec_cond(BtorAIGVecMgr * avmgr,BtorAIGVec * av_cond,BtorAIGVec * av_if,BtorAIGVec * av_else)779 btor_aigvec_cond (BtorAIGVecMgr *avmgr,
780 BtorAIGVec *av_cond,
781 BtorAIGVec *av_if,
782 BtorAIGVec *av_else)
783 {
784 BtorAIGMgr *amgr;
785 BtorAIGVec *result;
786 uint32_t i, width;
787 assert (avmgr);
788 assert (av_cond);
789 assert (av_if);
790 assert (av_else);
791 assert (av_cond->width == 1);
792 assert (av_if->width == av_else->width);
793 assert (av_if->width > 0);
794 amgr = avmgr->amgr;
795 width = av_if->width;
796 result = new_aigvec (avmgr, width);
797 for (i = 0; i < width; i++)
798 result->aigs[i] = btor_aig_cond (
799 amgr, av_cond->aigs[0], av_if->aigs[i], av_else->aigs[i]);
800 return result;
801 }
802
803 BtorAIGVec *
btor_aigvec_copy(BtorAIGVecMgr * avmgr,BtorAIGVec * av)804 btor_aigvec_copy (BtorAIGVecMgr *avmgr, BtorAIGVec *av)
805 {
806 BtorAIGMgr *amgr;
807 BtorAIGVec *result;
808 uint32_t i, width;
809 assert (avmgr);
810 assert (av);
811 amgr = avmgr->amgr;
812 width = av->width;
813 result = new_aigvec (avmgr, width);
814 for (i = 0; i < width; i++)
815 result->aigs[i] = btor_aig_copy (amgr, av->aigs[i]);
816 return result;
817 }
818
819 BtorAIGVec *
btor_aigvec_clone(BtorAIGVec * av,BtorAIGVecMgr * avmgr)820 btor_aigvec_clone (BtorAIGVec *av, BtorAIGVecMgr *avmgr)
821 {
822 assert (av);
823 assert (avmgr);
824
825 uint32_t i;
826 BtorAIGVec *res;
827 BtorAIGMgr *amgr;
828 BtorAIG *aig, *caig;
829
830 amgr = avmgr->amgr;
831 res = new_aigvec (avmgr, av->width);
832 for (i = 0; i < av->width; i++)
833 {
834 if (btor_aig_is_const (av->aigs[i]))
835 res->aigs[i] = av->aigs[i];
836 else
837 {
838 aig = av->aigs[i];
839 assert (BTOR_REAL_ADDR_AIG (aig)->id >= 0);
840 assert ((size_t) BTOR_REAL_ADDR_AIG (aig)->id
841 < BTOR_COUNT_STACK (amgr->id2aig));
842 caig = BTOR_PEEK_STACK (amgr->id2aig, BTOR_REAL_ADDR_AIG (aig)->id);
843 assert (caig);
844 assert (!btor_aig_is_const (caig));
845 if (BTOR_IS_INVERTED_AIG (aig))
846 res->aigs[i] = BTOR_INVERT_AIG (caig);
847 else
848 res->aigs[i] = caig;
849 assert (res->aigs[i]);
850 }
851 }
852 return res;
853 }
854
855 void
btor_aigvec_to_sat_tseitin(BtorAIGVecMgr * avmgr,BtorAIGVec * av)856 btor_aigvec_to_sat_tseitin (BtorAIGVecMgr *avmgr, BtorAIGVec *av)
857 {
858 BtorAIGMgr *amgr;
859 uint32_t i, width;
860 assert (avmgr);
861 assert (av);
862 amgr = btor_aigvec_get_aig_mgr (avmgr);
863 if (!btor_sat_is_initialized (amgr->smgr)) return;
864 width = av->width;
865 for (i = 0; i < width; i++) btor_aig_to_sat_tseitin (amgr, av->aigs[i]);
866 }
867
868 void
btor_aigvec_release_delete(BtorAIGVecMgr * avmgr,BtorAIGVec * av)869 btor_aigvec_release_delete (BtorAIGVecMgr *avmgr, BtorAIGVec *av)
870 {
871 BtorMemMgr *mm;
872 BtorAIGMgr *amgr;
873 uint32_t i, width;
874 assert (avmgr);
875 assert (av);
876 assert (av->width > 0);
877 mm = avmgr->btor->mm;
878 amgr = avmgr->amgr;
879 width = av->width;
880 for (i = 0; i < width; i++) btor_aig_release (amgr, av->aigs[i]);
881 btor_mem_free (mm, av, sizeof (BtorAIGVec) + sizeof (BtorAIG *) * av->width);
882 avmgr->cur_num_aigvecs--;
883 }
884
885 BtorAIGVecMgr *
btor_aigvec_mgr_new(Btor * btor)886 btor_aigvec_mgr_new (Btor *btor)
887 {
888 assert (btor);
889
890 BtorAIGVecMgr *avmgr;
891 BTOR_CNEW (btor->mm, avmgr);
892 avmgr->btor = btor;
893 avmgr->amgr = btor_aig_mgr_new (btor);
894 return avmgr;
895 }
896
897 BtorAIGVecMgr *
btor_aigvec_mgr_clone(Btor * btor,BtorAIGVecMgr * avmgr)898 btor_aigvec_mgr_clone (Btor *btor, BtorAIGVecMgr *avmgr)
899 {
900 assert (btor);
901 assert (avmgr);
902
903 BtorAIGVecMgr *res;
904 BTOR_NEW (btor->mm, res);
905
906 res->btor = btor;
907 res->amgr = btor_aig_mgr_clone (btor, avmgr->amgr);
908 res->max_num_aigvecs = avmgr->max_num_aigvecs;
909 res->cur_num_aigvecs = avmgr->cur_num_aigvecs;
910 return res;
911 }
912
913 void
btor_aigvec_mgr_delete(BtorAIGVecMgr * avmgr)914 btor_aigvec_mgr_delete (BtorAIGVecMgr *avmgr)
915 {
916 assert (avmgr);
917 btor_aig_mgr_delete (avmgr->amgr);
918 BTOR_DELETE (avmgr->btor->mm, avmgr);
919 }
920
921 BtorAIGMgr *
btor_aigvec_get_aig_mgr(const BtorAIGVecMgr * avmgr)922 btor_aigvec_get_aig_mgr (const BtorAIGVecMgr *avmgr)
923 {
924 return avmgr ? avmgr->amgr : 0;
925 }
926