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 "btoraig.h"
10
11 #include "btorabort.h"
12 #include "btorcore.h"
13 #include "btorsat.h"
14 #include "utils/btoraigmap.h"
15 #include "utils/btorhashptr.h"
16 #include "utils/btorutil.h"
17
18 #include <assert.h>
19 #include <limits.h>
20 #include <stdarg.h>
21 #include <stdio.h>
22 #include <stdlib.h>
23
24 /*------------------------------------------------------------------------*/
25
26 #define BTOR_INIT_AIG_UNIQUE_TABLE(mm, table) \
27 do \
28 { \
29 assert (mm); \
30 (table).size = 1; \
31 (table).num_elements = 0; \
32 BTOR_CNEW (mm, (table).chains); \
33 } while (0)
34
35 #define BTOR_RELEASE_AIG_UNIQUE_TABLE(mm, table) \
36 do \
37 { \
38 assert (mm); \
39 BTOR_DELETEN (mm, (table).chains, (table).size); \
40 } while (0)
41
42 #define BTOR_AIG_UNIQUE_TABLE_LIMIT 30
43
44 #define BTOR_AIG_UNIQUE_TABLE_PRIME 2000000137u
45
46 #define BTOR_FIND_AND_AIG_CONTRADICTION_LIMIT 8
47
48 /*------------------------------------------------------------------------*/
49
50 //#define BTOR_EXTRACT_TOP_LEVEL_MULTI_OR
51
52 //#define BTOR_AIG_TO_CNF_TOP_ELIM
53
54 #define BTOR_AIG_TO_CNF_EXTRACT_ONLY_NON_SHARED
55
56 #define BTOR_AIG_TO_CNF_EXTRACT_ITE
57
58 #define BTOR_AIG_TO_CNF_EXTRACT_XOR
59
60 // #define BTOR_AIG_TO_CNF_NARY_AND
61
62 /*------------------------------------------------------------------------*/
63
64 static void
setup_aig_and_add_to_id_table(BtorAIGMgr * amgr,BtorAIG * aig)65 setup_aig_and_add_to_id_table (BtorAIGMgr *amgr, BtorAIG *aig)
66 {
67 int32_t id;
68
69 id = BTOR_COUNT_STACK (amgr->id2aig);
70 BTOR_ABORT (id == INT32_MAX, "AIG id overflow");
71 aig->refs = 1;
72 aig->id = id;
73 BTOR_PUSH_STACK (amgr->id2aig, aig);
74 assert (aig->id >= 0);
75 assert (BTOR_COUNT_STACK (amgr->id2aig) == (size_t) aig->id + 1);
76 assert (BTOR_PEEK_STACK (amgr->id2aig, aig->id) == aig);
77 }
78
79 static BtorAIG *
new_and_aig(BtorAIGMgr * amgr,BtorAIG * left,BtorAIG * right)80 new_and_aig (BtorAIGMgr *amgr, BtorAIG *left, BtorAIG *right)
81 {
82 assert (amgr);
83 assert (!btor_aig_is_const (left));
84 assert (!btor_aig_is_const (right));
85
86 BtorAIG *aig;
87 size_t size;
88
89 size = sizeof (BtorAIG) + 2 * sizeof (int32_t);
90 aig = btor_mem_malloc (amgr->btor->mm, size);
91 memset (aig, 0, size);
92 setup_aig_and_add_to_id_table (amgr, aig);
93 aig->children[0] = btor_aig_get_id (left);
94 aig->children[1] = btor_aig_get_id (right);
95 amgr->cur_num_aigs++;
96 if (amgr->max_num_aigs < amgr->cur_num_aigs)
97 amgr->max_num_aigs = amgr->cur_num_aigs;
98 return aig;
99 }
100
101 static void
release_cnf_id_aig_mgr(BtorAIGMgr * amgr,BtorAIG * aig)102 release_cnf_id_aig_mgr (BtorAIGMgr *amgr, BtorAIG *aig)
103 {
104 assert (!BTOR_IS_INVERTED_AIG (aig));
105 assert (aig->cnf_id > 0);
106 assert ((size_t) aig->cnf_id < BTOR_SIZE_STACK (amgr->cnfid2aig));
107 assert (amgr->cnfid2aig.start[aig->cnf_id] == aig->id);
108 if (amgr->smgr->have_restore) return;
109 amgr->cnfid2aig.start[aig->cnf_id] = 0;
110 btor_sat_mgr_release_cnf_id (amgr->smgr, aig->cnf_id);
111 aig->cnf_id = 0;
112 }
113
114 static void
delete_aig_node(BtorAIGMgr * amgr,BtorAIG * aig)115 delete_aig_node (BtorAIGMgr *amgr, BtorAIG *aig)
116 {
117 assert (!BTOR_IS_INVERTED_AIG (aig));
118 assert (amgr);
119 if (btor_aig_is_const (aig)) return;
120 if (aig->cnf_id) release_cnf_id_aig_mgr (amgr, aig);
121 amgr->id2aig.start[aig->id] = 0;
122 if (aig->is_var)
123 {
124 amgr->cur_num_aig_vars--;
125 BTOR_DELETE (amgr->btor->mm, aig);
126 }
127 else
128 {
129 amgr->cur_num_aigs--;
130 btor_mem_free (
131 amgr->btor->mm, aig, sizeof (BtorAIG) + 2 * sizeof (int32_t));
132 }
133 }
134
135 static uint32_t
hash_aig(int32_t id0,int32_t id1,uint32_t table_size)136 hash_aig (int32_t id0, int32_t id1, uint32_t table_size)
137 {
138 uint32_t hash;
139 assert (table_size > 0);
140 assert (btor_util_is_power_of_2 (table_size));
141 hash = 547789289u * (uint32_t) abs (id0);
142 hash += 786695309u * (uint32_t) abs (id1);
143 hash *= BTOR_AIG_UNIQUE_TABLE_PRIME;
144 hash &= table_size - 1;
145 return hash;
146 }
147
148 static uint32_t
compute_aig_hash(BtorAIG * aig,uint32_t table_size)149 compute_aig_hash (BtorAIG *aig, uint32_t table_size)
150 {
151 uint32_t hash;
152 assert (!BTOR_IS_INVERTED_AIG (aig));
153 assert (btor_aig_is_and (aig));
154 hash = hash_aig (aig->children[0], aig->children[1], table_size);
155 return hash;
156 }
157
158 static void
delete_aig_nodes_unique_table_entry(BtorAIGMgr * amgr,BtorAIG * aig)159 delete_aig_nodes_unique_table_entry (BtorAIGMgr *amgr, BtorAIG *aig)
160 {
161 uint32_t hash;
162 BtorAIG *cur, *prev;
163 assert (amgr);
164 assert (!BTOR_IS_INVERTED_AIG (aig));
165 assert (btor_aig_is_and (aig));
166 prev = 0;
167 hash = compute_aig_hash (aig, amgr->table.size);
168 cur = btor_aig_get_by_id (amgr, amgr->table.chains[hash]);
169 while (cur != aig)
170 {
171 assert (!BTOR_IS_INVERTED_AIG (cur));
172 prev = cur;
173 cur = btor_aig_get_by_id (amgr, cur->next);
174 }
175 assert (cur);
176 if (!prev)
177 amgr->table.chains[hash] = cur->next;
178 else
179 prev->next = cur->next;
180 amgr->table.num_elements--;
181 }
182
183 static void
inc_aig_ref_counter(BtorAIG * aig)184 inc_aig_ref_counter (BtorAIG *aig)
185 {
186 if (!btor_aig_is_const (aig))
187 {
188 BTOR_ABORT (BTOR_REAL_ADDR_AIG (aig)->refs == UINT32_MAX,
189 "reference counter overflow");
190 BTOR_REAL_ADDR_AIG (aig)->refs++;
191 }
192 }
193
194 static BtorAIG *
inc_aig_ref_counter_and_return(BtorAIG * aig)195 inc_aig_ref_counter_and_return (BtorAIG *aig)
196 {
197 inc_aig_ref_counter (aig);
198 return aig;
199 }
200
201 static int32_t *
find_and_aig(BtorAIGMgr * amgr,BtorAIG * left,BtorAIG * right)202 find_and_aig (BtorAIGMgr *amgr, BtorAIG *left, BtorAIG *right)
203 {
204 assert (amgr);
205 assert (!btor_aig_is_const (left));
206 assert (!btor_aig_is_const (right));
207
208 BtorAIG *cur;
209 uint32_t hash;
210 int32_t *result;
211
212 if (btor_opt_get (amgr->btor, BTOR_OPT_SORT_AIG) > 0
213 && BTOR_REAL_ADDR_AIG (right)->id < BTOR_REAL_ADDR_AIG (left)->id)
214 {
215 BTOR_SWAP (BtorAIG *, left, right);
216 }
217
218 hash = hash_aig (BTOR_REAL_ADDR_AIG (left)->id,
219 BTOR_REAL_ADDR_AIG (right)->id,
220 amgr->table.size);
221 result = amgr->table.chains + hash;
222 cur = btor_aig_get_by_id (amgr, *result);
223 while (cur)
224 {
225 assert (!BTOR_IS_INVERTED_AIG (cur));
226 assert (btor_aig_is_and (cur));
227 if (btor_aig_get_left_child (amgr, cur) == left
228 && btor_aig_get_right_child (amgr, cur) == right)
229 break;
230 #ifndef NDEBUG
231 if (btor_opt_get (amgr->btor, BTOR_OPT_SORT_AIG) > 0)
232 assert (btor_aig_get_left_child (amgr, cur) != right
233 || btor_aig_get_right_child (amgr, cur) != left);
234 #endif
235 result = &cur->next;
236 cur = cur->next == 0 ? 0 : btor_aig_get_by_id (amgr, cur->next);
237 }
238 return result;
239 }
240
241 static BtorAIG *
find_and_aig_node(BtorAIGMgr * amgr,BtorAIG * left,BtorAIG * right)242 find_and_aig_node (BtorAIGMgr *amgr, BtorAIG *left, BtorAIG *right)
243 {
244 int32_t *lookup;
245 BtorAIG *res;
246 lookup = find_and_aig (amgr, left, right);
247 assert (lookup);
248 res = *lookup ? btor_aig_get_by_id (amgr, *lookup) : 0;
249 return res;
250 }
251
252 static void
enlarge_aig_nodes_unique_table(BtorAIGMgr * amgr)253 enlarge_aig_nodes_unique_table (BtorAIGMgr *amgr)
254 {
255 BtorMemMgr *mm;
256 int32_t *new_chains;
257 uint32_t i, size, new_size;
258 uint32_t hash;
259 BtorAIG *temp = 0;
260 BtorAIG *cur = 0;
261 assert (amgr);
262 size = amgr->table.size;
263 new_size = size << 1;
264 assert (new_size / size == 2);
265 mm = amgr->btor->mm;
266 BTOR_CNEWN (mm, new_chains, new_size);
267 for (i = 0; i < size; i++)
268 {
269 cur = btor_aig_get_by_id (amgr, amgr->table.chains[i]);
270 while (cur)
271 {
272 assert (!BTOR_IS_INVERTED_AIG (cur));
273 assert (btor_aig_is_and (cur));
274 temp = btor_aig_get_by_id (amgr, cur->next);
275 hash = compute_aig_hash (cur, new_size);
276 cur->next = new_chains[hash];
277 new_chains[hash] = cur->id;
278 cur = temp;
279 }
280 }
281 BTOR_RELEASE_AIG_UNIQUE_TABLE (mm, amgr->table);
282 amgr->table.size = new_size;
283 amgr->table.chains = new_chains;
284 }
285
286 BtorAIG *
btor_aig_copy(BtorAIGMgr * amgr,BtorAIG * aig)287 btor_aig_copy (BtorAIGMgr *amgr, BtorAIG *aig)
288 {
289 assert (amgr);
290 (void) amgr;
291 if (btor_aig_is_const (aig)) return aig;
292 return inc_aig_ref_counter_and_return (aig);
293 }
294
295 void
btor_aig_release(BtorAIGMgr * amgr,BtorAIG * aig)296 btor_aig_release (BtorAIGMgr *amgr, BtorAIG *aig)
297 {
298 BtorAIG *cur, *l, *r;
299 BtorAIGPtrStack stack;
300 BtorMemMgr *mm;
301
302 assert (amgr);
303 mm = amgr->btor->mm;
304
305 if (!btor_aig_is_const (aig))
306 {
307 cur = BTOR_REAL_ADDR_AIG (aig);
308 assert (cur->refs > 0u);
309 if (cur->refs > 1u)
310 {
311 cur->refs--;
312 }
313 else
314 {
315 assert (cur->refs == 1u);
316 BTOR_INIT_STACK (mm, stack);
317 goto BTOR_RELEASE_AIG_WITHOUT_POP;
318
319 while (!BTOR_EMPTY_STACK (stack))
320 {
321 cur = BTOR_POP_STACK (stack);
322 cur = BTOR_REAL_ADDR_AIG (cur);
323
324 if (cur->refs > 1u)
325 {
326 cur->refs--;
327 }
328 else
329 {
330 BTOR_RELEASE_AIG_WITHOUT_POP:
331 assert (cur->refs == 1u);
332 if (!btor_aig_is_var (cur))
333 {
334 assert (btor_aig_is_and (cur));
335 l = btor_aig_get_left_child (amgr, cur);
336 r = btor_aig_get_right_child (amgr, cur);
337 BTOR_PUSH_STACK (stack, r);
338 BTOR_PUSH_STACK (stack, l);
339 delete_aig_nodes_unique_table_entry (amgr, cur);
340 }
341
342 delete_aig_node (amgr, cur);
343 }
344 }
345 BTOR_RELEASE_STACK (stack);
346 }
347 }
348 }
349
350 BtorAIG *
btor_aig_var(BtorAIGMgr * amgr)351 btor_aig_var (BtorAIGMgr *amgr)
352 {
353 BtorAIG *aig;
354 assert (amgr);
355 BTOR_CNEW (amgr->btor->mm, aig);
356 setup_aig_and_add_to_id_table (amgr, aig);
357 aig->is_var = 1;
358 amgr->cur_num_aig_vars++;
359 if (amgr->max_num_aig_vars < amgr->cur_num_aig_vars)
360 amgr->max_num_aig_vars = amgr->cur_num_aig_vars;
361 return aig;
362 }
363
364 BtorAIG *
btor_aig_not(BtorAIGMgr * amgr,BtorAIG * aig)365 btor_aig_not (BtorAIGMgr *amgr, BtorAIG *aig)
366 {
367 assert (amgr);
368 (void) amgr;
369 inc_aig_ref_counter (aig);
370 return BTOR_INVERT_AIG (aig);
371 }
372
373 static bool
find_and_contradiction_aig(BtorAIGMgr * amgr,BtorAIG * aig,BtorAIG * a0,BtorAIG * a1,uint32_t * calls)374 find_and_contradiction_aig (
375 BtorAIGMgr *amgr, BtorAIG *aig, BtorAIG *a0, BtorAIG *a1, uint32_t *calls)
376 {
377 assert (amgr);
378 assert (aig);
379 assert (a0);
380 assert (a1);
381 assert (calls);
382 (void) amgr;
383
384 if (*calls >= BTOR_FIND_AND_AIG_CONTRADICTION_LIMIT) return false;
385
386 if (!BTOR_IS_INVERTED_AIG (aig) && btor_aig_is_and (aig))
387 {
388 if (btor_aig_get_left_child (amgr, aig) == BTOR_INVERT_AIG (a0)
389 || btor_aig_get_left_child (amgr, aig) == BTOR_INVERT_AIG (a1)
390 || btor_aig_get_right_child (amgr, aig) == BTOR_INVERT_AIG (a0)
391 || btor_aig_get_right_child (amgr, aig) == BTOR_INVERT_AIG (a1))
392 return true;
393 *calls += 1;
394 return find_and_contradiction_aig (
395 amgr, btor_aig_get_left_child (amgr, aig), a0, a1, calls)
396 || find_and_contradiction_aig (
397 amgr, btor_aig_get_right_child (amgr, aig), a0, a1, calls);
398 }
399 return false;
400 }
401
402 static BtorAIG *
simp_aig_by_sat(BtorAIGMgr * amgr,BtorAIG * aig)403 simp_aig_by_sat (BtorAIGMgr *amgr, BtorAIG *aig)
404 {
405 int32_t lit, val, repr, sign;
406 BtorAIG *res;
407
408 /* fixed handling for const aigs not supported by minisat
409 * (returns 0) FIXME why? */
410 if (btor_aig_is_const (aig)) return aig;
411
412 lit = btor_aig_get_cnf_id (aig);
413 if (!lit) return aig;
414 val = btor_sat_fixed (amgr->smgr, lit);
415 if (val) return (val < 0) ? BTOR_AIG_FALSE : BTOR_AIG_TRUE;
416 repr = btor_sat_repr (amgr->smgr, lit);
417 if ((sign = (repr < 0))) repr = -repr;
418 assert (repr >= 0);
419 assert ((size_t) repr < BTOR_SIZE_STACK (amgr->cnfid2aig));
420 res = btor_aig_get_by_id (amgr, amgr->cnfid2aig.start[repr]);
421 if (!res) return aig;
422 if (sign) res = BTOR_INVERT_AIG (res);
423 return res;
424 }
425
426 BtorAIG *
btor_aig_and(BtorAIGMgr * amgr,BtorAIG * left,BtorAIG * right)427 btor_aig_and (BtorAIGMgr *amgr, BtorAIG *left, BtorAIG *right)
428 {
429 BtorAIG *res, *real_left, *real_right;
430 int32_t *lookup;
431 uint32_t calls;
432
433 assert (amgr);
434
435 if (amgr->smgr->initialized)
436 {
437 left = simp_aig_by_sat (amgr, left);
438 right = simp_aig_by_sat (amgr, right);
439 }
440
441 calls = 0;
442
443 BTOR_AIG_TWO_LEVEL_OPT_TRY_AGAIN:
444 if (left == BTOR_AIG_FALSE || right == BTOR_AIG_FALSE) return BTOR_AIG_FALSE;
445
446 if (left == BTOR_AIG_TRUE) return inc_aig_ref_counter_and_return (right);
447
448 if (right == BTOR_AIG_TRUE || (left == right))
449 return inc_aig_ref_counter_and_return (left);
450 if (left == BTOR_INVERT_AIG (right)) return BTOR_AIG_FALSE;
451
452 real_left = BTOR_REAL_ADDR_AIG (left);
453 real_right = BTOR_REAL_ADDR_AIG (right);
454
455 /* 2 level minimization rules for AIGs */
456 /* first rule of contradiction */
457 if (btor_aig_is_and (real_left) && !BTOR_IS_INVERTED_AIG (left))
458 {
459 if (btor_aig_get_left_child (amgr, real_left) == BTOR_INVERT_AIG (right)
460 || btor_aig_get_right_child (amgr, real_left)
461 == BTOR_INVERT_AIG (right))
462 return BTOR_AIG_FALSE;
463 }
464 /* use commutativity */
465 if (btor_aig_is_and (real_right) && !BTOR_IS_INVERTED_AIG (right))
466 {
467 if (btor_aig_get_left_child (amgr, real_right) == BTOR_INVERT_AIG (left)
468 || btor_aig_get_right_child (amgr, real_right)
469 == BTOR_INVERT_AIG (left))
470 return BTOR_AIG_FALSE;
471 }
472 /* second rule of contradiction */
473 if (btor_aig_is_and (real_right) && btor_aig_is_and (real_left)
474 && !BTOR_IS_INVERTED_AIG (left) && !BTOR_IS_INVERTED_AIG (right))
475 {
476 if (btor_aig_get_left_child (amgr, real_left)
477 == BTOR_INVERT_AIG (btor_aig_get_left_child (amgr, real_right))
478 || btor_aig_get_left_child (amgr, real_left)
479 == BTOR_INVERT_AIG (btor_aig_get_right_child (amgr, real_right))
480 || btor_aig_get_right_child (amgr, real_left)
481 == BTOR_INVERT_AIG (btor_aig_get_left_child (amgr, real_right))
482 || btor_aig_get_right_child (amgr, real_left)
483 == BTOR_INVERT_AIG (btor_aig_get_right_child (amgr, real_right)))
484 return BTOR_AIG_FALSE;
485 }
486 /* first rule of subsumption */
487 if (btor_aig_is_and (real_left) && BTOR_IS_INVERTED_AIG (left))
488 {
489 if (btor_aig_get_left_child (amgr, real_left) == BTOR_INVERT_AIG (right)
490 || btor_aig_get_right_child (amgr, real_left)
491 == BTOR_INVERT_AIG (right))
492 return inc_aig_ref_counter_and_return (right);
493 }
494 /* use commutativity */
495 if (btor_aig_is_and (real_right) && BTOR_IS_INVERTED_AIG (right))
496 {
497 if (btor_aig_get_left_child (amgr, real_right) == BTOR_INVERT_AIG (left)
498 || btor_aig_get_right_child (amgr, real_right)
499 == BTOR_INVERT_AIG (left))
500 return inc_aig_ref_counter_and_return (left);
501 }
502 /* second rule of subsumption */
503 if (btor_aig_is_and (real_right) && btor_aig_is_and (real_left)
504 && BTOR_IS_INVERTED_AIG (left) && !BTOR_IS_INVERTED_AIG (right))
505 {
506 if (btor_aig_get_left_child (amgr, real_left)
507 == BTOR_INVERT_AIG (btor_aig_get_left_child (amgr, real_right))
508 || btor_aig_get_left_child (amgr, real_left)
509 == BTOR_INVERT_AIG (btor_aig_get_right_child (amgr, real_right))
510 || btor_aig_get_right_child (amgr, real_left)
511 == BTOR_INVERT_AIG (btor_aig_get_left_child (amgr, real_right))
512 || btor_aig_get_right_child (amgr, real_left)
513 == BTOR_INVERT_AIG (btor_aig_get_right_child (amgr, real_right)))
514 return inc_aig_ref_counter_and_return (right);
515 }
516 /* use commutativity */
517 if (btor_aig_is_and (real_right) && btor_aig_is_and (real_left)
518 && !BTOR_IS_INVERTED_AIG (left) && BTOR_IS_INVERTED_AIG (right))
519 {
520 if (btor_aig_get_left_child (amgr, real_left)
521 == BTOR_INVERT_AIG (btor_aig_get_left_child (amgr, real_right))
522 || btor_aig_get_left_child (amgr, real_left)
523 == BTOR_INVERT_AIG (btor_aig_get_right_child (amgr, real_right))
524 || btor_aig_get_right_child (amgr, real_left)
525 == BTOR_INVERT_AIG (btor_aig_get_left_child (amgr, real_right))
526 || btor_aig_get_right_child (amgr, real_left)
527 == BTOR_INVERT_AIG (btor_aig_get_right_child (amgr, real_right)))
528 return inc_aig_ref_counter_and_return (left);
529 }
530 /* rule of resolution */
531 if (btor_aig_is_and (real_right) && btor_aig_is_and (real_left)
532 && BTOR_IS_INVERTED_AIG (left) && BTOR_IS_INVERTED_AIG (right))
533 {
534 if ((btor_aig_get_left_child (amgr, real_left)
535 == btor_aig_get_left_child (amgr, real_right)
536 && btor_aig_get_right_child (amgr, real_left)
537 == BTOR_INVERT_AIG (
538 btor_aig_get_right_child (amgr, real_right)))
539 || (btor_aig_get_left_child (amgr, real_left)
540 == btor_aig_get_right_child (amgr, real_right)
541 && btor_aig_get_right_child (amgr, real_left)
542 == BTOR_INVERT_AIG (
543 btor_aig_get_left_child (amgr, real_right))))
544 return inc_aig_ref_counter_and_return (
545 BTOR_INVERT_AIG (btor_aig_get_left_child (amgr, real_left)));
546 }
547 /* use commutativity */
548 if (btor_aig_is_and (real_right) && btor_aig_is_and (real_left)
549 && BTOR_IS_INVERTED_AIG (left) && BTOR_IS_INVERTED_AIG (right))
550 {
551 if ((btor_aig_get_right_child (amgr, real_right)
552 == btor_aig_get_right_child (amgr, real_left)
553 && btor_aig_get_left_child (amgr, real_right)
554 == BTOR_INVERT_AIG (btor_aig_get_left_child (amgr, real_left)))
555 || (btor_aig_get_right_child (amgr, real_right)
556 == btor_aig_get_left_child (amgr, real_left)
557 && btor_aig_get_left_child (amgr, real_right)
558 == BTOR_INVERT_AIG (
559 btor_aig_get_right_child (amgr, real_left))))
560 return inc_aig_ref_counter_and_return (
561 BTOR_INVERT_AIG (btor_aig_get_right_child (amgr, real_right)));
562 }
563 /* asymmetric rule of idempotency */
564 if (btor_aig_is_and (real_left) && !BTOR_IS_INVERTED_AIG (left))
565 {
566 if (btor_aig_get_left_child (amgr, real_left) == right
567 || btor_aig_get_right_child (amgr, real_left) == right)
568 return inc_aig_ref_counter_and_return (left);
569 }
570 /* use commutativity */
571 if (btor_aig_is_and (real_right) && !BTOR_IS_INVERTED_AIG (right))
572 {
573 if (btor_aig_get_left_child (amgr, real_right) == left
574 || btor_aig_get_right_child (amgr, real_right) == left)
575 return inc_aig_ref_counter_and_return (right);
576 }
577 /* symmetric rule of idempotency */
578 if (btor_aig_is_and (real_right) && btor_aig_is_and (real_left)
579 && !BTOR_IS_INVERTED_AIG (left) && !BTOR_IS_INVERTED_AIG (right))
580 {
581 if (btor_aig_get_left_child (amgr, real_left)
582 == btor_aig_get_left_child (amgr, real_right)
583 || btor_aig_get_right_child (amgr, real_left)
584 == btor_aig_get_left_child (amgr, real_right))
585 {
586 right = btor_aig_get_right_child (amgr, real_right);
587 goto BTOR_AIG_TWO_LEVEL_OPT_TRY_AGAIN;
588 }
589 }
590 /* use commutativity */
591 if (btor_aig_is_and (real_right) && btor_aig_is_and (real_left)
592 && !BTOR_IS_INVERTED_AIG (left) && !BTOR_IS_INVERTED_AIG (right))
593 {
594 if (btor_aig_get_left_child (amgr, real_left)
595 == btor_aig_get_right_child (amgr, real_right)
596 || btor_aig_get_right_child (amgr, real_left)
597 == btor_aig_get_right_child (amgr, real_right))
598 {
599 right = btor_aig_get_left_child (amgr, real_right);
600 goto BTOR_AIG_TWO_LEVEL_OPT_TRY_AGAIN;
601 }
602 }
603 /* asymmetric rule of substitution */
604 if (btor_aig_is_and (real_left) && BTOR_IS_INVERTED_AIG (left))
605 {
606 if (btor_aig_get_right_child (amgr, real_left) == right)
607 {
608 left = BTOR_INVERT_AIG (btor_aig_get_left_child (amgr, real_left));
609 goto BTOR_AIG_TWO_LEVEL_OPT_TRY_AGAIN;
610 }
611 if (btor_aig_get_left_child (amgr, real_left) == right)
612 {
613 left = BTOR_INVERT_AIG (btor_aig_get_right_child (amgr, real_left));
614 goto BTOR_AIG_TWO_LEVEL_OPT_TRY_AGAIN;
615 }
616 }
617 /* use commutativity */
618 if (btor_aig_is_and (real_right) && BTOR_IS_INVERTED_AIG (right))
619 {
620 if (btor_aig_get_left_child (amgr, real_right) == left)
621 {
622 right = BTOR_INVERT_AIG (btor_aig_get_right_child (amgr, real_right));
623 goto BTOR_AIG_TWO_LEVEL_OPT_TRY_AGAIN;
624 }
625 if (btor_aig_get_right_child (amgr, real_right) == left)
626 {
627 right = BTOR_INVERT_AIG (btor_aig_get_left_child (amgr, real_right));
628 goto BTOR_AIG_TWO_LEVEL_OPT_TRY_AGAIN;
629 }
630 }
631 /* symmetric rule of substitution */
632 if (btor_aig_is_and (real_left) && BTOR_IS_INVERTED_AIG (left)
633 && btor_aig_is_and (real_right) && !BTOR_IS_INVERTED_AIG (right))
634 {
635 if ((btor_aig_get_right_child (amgr, real_left)
636 == btor_aig_get_left_child (amgr, real_right))
637 || (btor_aig_get_right_child (amgr, real_left)
638 == btor_aig_get_right_child (amgr, real_right)))
639 {
640 left = BTOR_INVERT_AIG (btor_aig_get_left_child (amgr, real_left));
641 goto BTOR_AIG_TWO_LEVEL_OPT_TRY_AGAIN;
642 }
643 if ((btor_aig_get_left_child (amgr, real_left)
644 == btor_aig_get_left_child (amgr, real_right))
645 || (btor_aig_get_left_child (amgr, real_left)
646 == btor_aig_get_right_child (amgr, real_right)))
647 {
648 left = BTOR_INVERT_AIG (btor_aig_get_right_child (amgr, real_left));
649 goto BTOR_AIG_TWO_LEVEL_OPT_TRY_AGAIN;
650 }
651 }
652 /* use commutativity */
653 if (btor_aig_is_and (real_right) && BTOR_IS_INVERTED_AIG (right)
654 && btor_aig_is_and (real_left) && !BTOR_IS_INVERTED_AIG (left))
655 {
656 if ((btor_aig_get_left_child (amgr, real_right)
657 == btor_aig_get_right_child (amgr, real_left))
658 || (btor_aig_get_left_child (amgr, real_right)
659 == btor_aig_get_left_child (amgr, real_left)))
660 {
661 right = BTOR_INVERT_AIG (btor_aig_get_right_child (amgr, real_right));
662 goto BTOR_AIG_TWO_LEVEL_OPT_TRY_AGAIN;
663 }
664 if ((btor_aig_get_right_child (amgr, real_right)
665 == btor_aig_get_right_child (amgr, real_left))
666 || (btor_aig_get_right_child (amgr, real_right)
667 == btor_aig_get_left_child (amgr, real_left)))
668 {
669 right = BTOR_INVERT_AIG (btor_aig_get_left_child (amgr, real_right));
670 goto BTOR_AIG_TWO_LEVEL_OPT_TRY_AGAIN;
671 }
672 }
673
674 if (find_and_contradiction_aig (amgr, left, left, right, &calls)
675 || find_and_contradiction_aig (amgr, right, left, right, &calls))
676 return BTOR_AIG_FALSE;
677
678 // Implicit XOR normalization .... (TODO keep it?)
679
680 if (BTOR_IS_INVERTED_AIG (left) && btor_aig_is_and (real_left)
681 && BTOR_IS_INVERTED_AIG (right) && btor_aig_is_and (real_right)
682 && btor_aig_get_left_child (amgr, real_left)
683 == BTOR_INVERT_AIG (btor_aig_get_left_child (amgr, real_right))
684 && btor_aig_get_right_child (amgr, real_left)
685 == BTOR_INVERT_AIG (btor_aig_get_right_child (amgr, real_right)))
686 {
687 BtorAIG *l = find_and_aig_node (
688 amgr,
689 btor_aig_get_left_child (amgr, real_left),
690 BTOR_INVERT_AIG (btor_aig_get_right_child (amgr, real_left)));
691 if (l)
692 {
693 BtorAIG *r = find_and_aig_node (
694 amgr,
695 BTOR_INVERT_AIG (btor_aig_get_left_child (amgr, real_left)),
696 btor_aig_get_right_child (amgr, real_left));
697 if (r)
698 {
699 res =
700 find_and_aig_node (amgr, BTOR_INVERT_AIG (l), BTOR_INVERT_AIG (r));
701 if (res)
702 {
703 inc_aig_ref_counter (res);
704 return BTOR_INVERT_AIG (res);
705 }
706 }
707 }
708 }
709
710 // TODO Implicit ITE normalization ....
711
712 lookup = find_and_aig (amgr, left, right);
713 assert (lookup);
714 res = *lookup ? btor_aig_get_by_id (amgr, *lookup) : 0;
715 if (!res)
716 {
717 if (amgr->table.num_elements == amgr->table.size
718 && btor_util_log_2 (amgr->table.size) < BTOR_AIG_UNIQUE_TABLE_LIMIT)
719 {
720 enlarge_aig_nodes_unique_table (amgr);
721 lookup = find_and_aig (amgr, left, right);
722 }
723 if (btor_opt_get (amgr->btor, BTOR_OPT_SORT_AIG) > 0
724 && real_right->id < real_left->id)
725 {
726 BTOR_SWAP (BtorAIG *, left, right);
727 }
728 res = new_and_aig (amgr, left, right);
729 *lookup = res->id;
730 inc_aig_ref_counter (left);
731 inc_aig_ref_counter (right);
732 assert (amgr->table.num_elements < INT32_MAX);
733 amgr->table.num_elements++;
734 }
735 else
736 {
737 inc_aig_ref_counter (res);
738 }
739 return res;
740 }
741
742 BtorAIG *
btor_aig_or(BtorAIGMgr * amgr,BtorAIG * left,BtorAIG * right)743 btor_aig_or (BtorAIGMgr *amgr, BtorAIG *left, BtorAIG *right)
744 {
745 assert (amgr);
746 return BTOR_INVERT_AIG (
747 btor_aig_and (amgr, BTOR_INVERT_AIG (left), BTOR_INVERT_AIG (right)));
748 }
749
750 BtorAIG *
btor_aig_eq(BtorAIGMgr * amgr,BtorAIG * left,BtorAIG * right)751 btor_aig_eq (BtorAIGMgr *amgr, BtorAIG *left, BtorAIG *right)
752 {
753 BtorAIG *eq, *eq_left, *eq_right;
754 assert (amgr);
755
756 eq_left =
757 BTOR_INVERT_AIG (btor_aig_and (amgr, left, BTOR_INVERT_AIG (right)));
758 eq_right =
759 BTOR_INVERT_AIG (btor_aig_and (amgr, BTOR_INVERT_AIG (left), right));
760 eq = btor_aig_and (amgr, eq_left, eq_right);
761 btor_aig_release (amgr, eq_left);
762 btor_aig_release (amgr, eq_right);
763 return eq;
764 }
765
766 BtorAIG *
btor_aig_cond(BtorAIGMgr * amgr,BtorAIG * a_cond,BtorAIG * a_if,BtorAIG * a_else)767 btor_aig_cond (BtorAIGMgr *amgr,
768 BtorAIG *a_cond,
769 BtorAIG *a_if,
770 BtorAIG *a_else)
771 {
772 BtorAIG *cond, *and1, *and2;
773 assert (amgr);
774 and1 = btor_aig_and (amgr, a_if, a_cond);
775 and2 = btor_aig_and (amgr, a_else, BTOR_INVERT_AIG (a_cond));
776 cond = btor_aig_or (amgr, and1, and2);
777 btor_aig_release (amgr, and1);
778 btor_aig_release (amgr, and2);
779 return cond;
780 }
781
782 BtorAIGMgr *
btor_aig_mgr_new(Btor * btor)783 btor_aig_mgr_new (Btor *btor)
784 {
785 assert (btor);
786
787 BtorAIGMgr *amgr;
788
789 BTOR_CNEW (btor->mm, amgr);
790 amgr->btor = btor;
791 BTOR_INIT_AIG_UNIQUE_TABLE (btor->mm, amgr->table);
792 amgr->smgr = btor_sat_mgr_new (btor);
793 BTOR_INIT_STACK (btor->mm, amgr->id2aig);
794 BTOR_PUSH_STACK (amgr->id2aig, BTOR_AIG_FALSE);
795 BTOR_PUSH_STACK (amgr->id2aig, BTOR_AIG_TRUE);
796 assert ((size_t) BTOR_AIG_FALSE == 0);
797 assert ((size_t) BTOR_AIG_TRUE == 1);
798 BTOR_INIT_STACK (btor->mm, amgr->cnfid2aig);
799 return amgr;
800 }
801
802 static BtorAIG *
clone_aig(BtorMemMgr * mm,BtorAIG * aig)803 clone_aig (BtorMemMgr *mm, BtorAIG *aig)
804 {
805 assert (mm);
806
807 size_t size;
808 BtorAIG *res, *real_aig;
809
810 if (btor_aig_is_const (aig)) return aig;
811
812 real_aig = BTOR_REAL_ADDR_AIG (aig);
813 size = sizeof (BtorAIG);
814 if (!real_aig->is_var) size += 2 * sizeof (int32_t);
815 res = btor_mem_malloc (mm, size);
816 memcpy (res, real_aig, size);
817
818 res = BTOR_IS_INVERTED_AIG (aig) ? BTOR_INVERT_AIG (res) : res;
819 return res;
820 }
821
822 static void
clone_aigs(BtorAIGMgr * amgr,BtorAIGMgr * clone)823 clone_aigs (BtorAIGMgr *amgr, BtorAIGMgr *clone)
824 {
825 assert (amgr);
826 assert (clone);
827
828 uint32_t i;
829 size_t size;
830 BtorMemMgr *mm;
831 BtorAIG *aig;
832
833 mm = clone->btor->mm;
834
835 /* clone id2aig table */
836 BTOR_INIT_STACK (mm, clone->id2aig);
837 size = BTOR_SIZE_STACK (amgr->id2aig);
838 if (size)
839 {
840 BTOR_CNEWN (mm, clone->id2aig.start, size);
841 clone->id2aig.end = clone->id2aig.start + size;
842 clone->id2aig.top = clone->id2aig.start + BTOR_COUNT_STACK (amgr->id2aig);
843 }
844 for (i = 0; i < BTOR_COUNT_STACK (amgr->id2aig); i++)
845 {
846 aig = clone_aig (mm, BTOR_PEEK_STACK (amgr->id2aig, i));
847 BTOR_POKE_STACK (clone->id2aig, i, aig);
848 }
849
850 /* clone unique table */
851 BTOR_CNEWN (mm, clone->table.chains, amgr->table.size);
852 clone->table.size = amgr->table.size;
853 clone->table.num_elements = amgr->table.num_elements;
854 memcpy (clone->table.chains,
855 amgr->table.chains,
856 amgr->table.size * sizeof (int32_t));
857
858 /* clone cnfid2aig table */
859 BTOR_INIT_STACK (mm, clone->cnfid2aig);
860 size = BTOR_SIZE_STACK (amgr->cnfid2aig);
861 if (size)
862 {
863 BTOR_CNEWN (mm, clone->cnfid2aig.start, size);
864 clone->cnfid2aig.end = clone->cnfid2aig.start + size;
865 clone->cnfid2aig.top = clone->cnfid2aig.start;
866 memcpy (
867 clone->cnfid2aig.start, amgr->cnfid2aig.start, size * sizeof (int32_t));
868 }
869 assert (BTOR_SIZE_STACK (clone->cnfid2aig)
870 == BTOR_SIZE_STACK (amgr->cnfid2aig));
871 assert (BTOR_COUNT_STACK (clone->cnfid2aig)
872 == BTOR_COUNT_STACK (amgr->cnfid2aig));
873 }
874
875 BtorAIGMgr *
btor_aig_mgr_clone(Btor * btor,BtorAIGMgr * amgr)876 btor_aig_mgr_clone (Btor *btor, BtorAIGMgr *amgr)
877 {
878 assert (btor);
879 assert (amgr);
880
881 BtorAIGMgr *res;
882
883 BTOR_CNEW (btor->mm, res);
884 res->btor = btor;
885
886 res->smgr = btor_sat_mgr_clone (btor, amgr->smgr);
887 /* Note: we do not yet clone aigs here (we need the clone of the aig
888 * manager for that). */
889 res->max_num_aigs = amgr->max_num_aigs;
890 res->max_num_aig_vars = amgr->max_num_aig_vars;
891 res->cur_num_aigs = amgr->cur_num_aigs;
892 res->cur_num_aig_vars = amgr->cur_num_aig_vars;
893 res->num_cnf_vars = amgr->num_cnf_vars;
894 res->num_cnf_clauses = amgr->num_cnf_clauses;
895 res->num_cnf_literals = amgr->num_cnf_literals;
896 clone_aigs (amgr, res);
897 return res;
898 }
899
900 void
btor_aig_mgr_delete(BtorAIGMgr * amgr)901 btor_aig_mgr_delete (BtorAIGMgr *amgr)
902 {
903 BtorMemMgr *mm;
904 assert (amgr);
905 assert (getenv ("BTORLEAK") || getenv ("BTORLEAKAIG")
906 || amgr->table.num_elements == 0);
907 mm = amgr->btor->mm;
908 BTOR_RELEASE_AIG_UNIQUE_TABLE (mm, amgr->table);
909 btor_sat_mgr_delete (amgr->smgr);
910 BTOR_RELEASE_STACK (amgr->id2aig);
911 BTOR_RELEASE_STACK (amgr->cnfid2aig);
912 BTOR_DELETE (mm, amgr);
913 }
914
915 static bool
is_xor_aig(BtorAIGMgr * amgr,BtorAIG * aig,BtorAIGPtrStack * leafs)916 is_xor_aig (BtorAIGMgr *amgr, BtorAIG *aig, BtorAIGPtrStack *leafs)
917 {
918 #ifdef BTOR_AIG_TO_CNF_EXTRACT_XOR
919 BtorAIG *l, *r, *ll, *lr, *rl, *rr;
920
921 assert (btor_aig_is_and (aig));
922 assert (!BTOR_IS_INVERTED_AIG (aig));
923
924 l = btor_aig_get_left_child (amgr, aig);
925 if (!BTOR_IS_INVERTED_AIG (l)) return false;
926 l = BTOR_REAL_ADDR_AIG (l);
927 #ifdef BTOR_AIG_TO_CNF_EXTRACT_ONLY_NON_SHARED
928 if (l->refs > 1) return false;
929 #endif
930
931 r = btor_aig_get_right_child (amgr, aig);
932 if (!BTOR_IS_INVERTED_AIG (r)) return false;
933 r = BTOR_REAL_ADDR_AIG (r);
934 #ifdef BTOR_AIG_TO_CNF_EXTRACT_ONLY_NON_SHARED
935 if (r->refs > 1) return false;
936 #endif
937
938 ll = btor_aig_get_left_child (amgr, l);
939 lr = btor_aig_get_right_child (amgr, l);
940
941 rl = btor_aig_get_left_child (amgr, r);
942 rr = btor_aig_get_right_child (amgr, r);
943
944 if (ll == BTOR_INVERT_AIG (rl) && lr == BTOR_INVERT_AIG (rr))
945 {
946 BTOR_PUSH_STACK (*leafs, rr);
947 BTOR_PUSH_STACK (*leafs, ll);
948 return true;
949 }
950
951 assert (!btor_opt_get (amgr->btor, BTOR_OPT_SORT_AIG)
952 || ll != BTOR_INVERT_AIG (rr) || lr != BTOR_INVERT_AIG (rl));
953
954 return false;
955 #else
956 (void) amgr;
957 (void) aig;
958 (void) leafs;
959 return false;
960 #endif
961 }
962
963 static bool
is_ite_aig(BtorAIGMgr * amgr,BtorAIG * aig,BtorAIGPtrStack * leafs)964 is_ite_aig (BtorAIGMgr *amgr, BtorAIG *aig, BtorAIGPtrStack *leafs)
965 {
966 #ifdef BTOR_AIG_TO_CNF_EXTRACT_ITE
967 BtorAIG *l, *r, *ll, *lr, *rl, *rr;
968
969 assert (btor_aig_is_and (aig));
970 assert (!BTOR_IS_INVERTED_AIG (aig));
971
972 l = btor_aig_get_left_child (amgr, aig);
973 if (!BTOR_IS_INVERTED_AIG (l)) return false;
974 l = BTOR_REAL_ADDR_AIG (l);
975 #ifdef BTOR_AIG_TO_CNF_EXTRACT_ONLY_NON_SHARED
976 if (l->refs > 1) return false;
977 #endif
978
979 r = btor_aig_get_right_child (amgr, aig);
980 if (!BTOR_IS_INVERTED_AIG (r)) return false;
981 r = BTOR_REAL_ADDR_AIG (r);
982 #ifdef BTOR_AIG_TO_CNF_EXTRACT_ONLY_NON_SHARED
983 if (r->refs > 1) return false;
984 #endif
985
986 ll = btor_aig_get_left_child (amgr, l);
987 lr = btor_aig_get_right_child (amgr, l);
988
989 rl = btor_aig_get_left_child (amgr, r);
990 rr = btor_aig_get_right_child (amgr, r);
991
992 // aig == (!ll | !lr)(!rl | !rr)
993
994 if (BTOR_INVERT_AIG (lr) == rl)
995 {
996 // aig == (!rl -> !ll)(rl -> !rr) = rl ? !rr : !ll
997 BTOR_PUSH_STACK (*leafs, BTOR_INVERT_AIG (ll)); // else
998 BTOR_PUSH_STACK (*leafs, BTOR_INVERT_AIG (rr)); // then
999 BTOR_PUSH_STACK (*leafs, rl); // cond
1000 return true;
1001 }
1002 if (BTOR_INVERT_AIG (ll) == rl)
1003 {
1004 // aig == (!rl -> !lr)(rl -> !rr)
1005 BTOR_PUSH_STACK (*leafs, BTOR_INVERT_AIG (lr)); // else
1006 BTOR_PUSH_STACK (*leafs, BTOR_INVERT_AIG (rr)); // then
1007 BTOR_PUSH_STACK (*leafs, rl); // cond
1008 return true;
1009 }
1010 if (BTOR_INVERT_AIG (lr) == rr)
1011 {
1012 // aig == (!rr -> !ll)(rr -> !rl)
1013 BTOR_PUSH_STACK (*leafs, BTOR_INVERT_AIG (ll)); // else
1014 BTOR_PUSH_STACK (*leafs, BTOR_INVERT_AIG (rl)); // then
1015 BTOR_PUSH_STACK (*leafs, rr); // cond
1016 return true;
1017 }
1018 if (BTOR_INVERT_AIG (ll) == rr)
1019 {
1020 // aig == (!rr -> !lr)(rr -> !rl)
1021 BTOR_PUSH_STACK (*leafs, BTOR_INVERT_AIG (lr)); // else
1022 BTOR_PUSH_STACK (*leafs, BTOR_INVERT_AIG (rl)); // then
1023 BTOR_PUSH_STACK (*leafs, rr); // cond
1024 return true;
1025 }
1026
1027 return false;
1028 #else
1029 (void) amgr;
1030 (void) aig;
1031 (void) leafs;
1032 return false;
1033 #endif
1034 }
1035
1036 static void
set_next_id_aig_mgr(BtorAIGMgr * amgr,BtorAIG * root)1037 set_next_id_aig_mgr (BtorAIGMgr *amgr, BtorAIG *root)
1038 {
1039 assert (!BTOR_IS_INVERTED_AIG (root));
1040 assert (!root->cnf_id);
1041 root->cnf_id = btor_sat_mgr_next_cnf_id (amgr->smgr);
1042 assert (root->cnf_id > 0);
1043 BTOR_FIT_STACK (amgr->cnfid2aig, (size_t) root->cnf_id);
1044 amgr->cnfid2aig.start[root->cnf_id] = root->id;
1045 assert (amgr->cnfid2aig.start[root->cnf_id] == root->id);
1046 amgr->num_cnf_vars++;
1047 }
1048
1049 #ifdef BTOR_EXTRACT_TOP_LEVEL_MULTI_OR
1050 static bool
is_or_aig(BtorAIGMgr * amgr,BtorAIG * root,BtorAIGPtrStack * leafs)1051 is_or_aig (BtorAIGMgr *amgr, BtorAIG *root, BtorAIGPtrStack *leafs)
1052 {
1053 assert (amgr);
1054 assert (root);
1055 assert (leafs);
1056 assert (BTOR_EMPTY_STACK (*leafs));
1057
1058 BtorAIG *real_cur, *cur, **p;
1059 BtorAIGPtrStack tree;
1060 BtorMemMgr *mm;
1061
1062 if (!BTOR_IS_INVERTED_AIG (root)
1063 || !btor_aig_is_and (BTOR_REAL_ADDR_AIG (root)))
1064 return false;
1065
1066 mm = amgr->btor->mm;
1067 root = BTOR_REAL_ADDR_AIG (root);
1068
1069 BTOR_INIT_STACK (mm, tree);
1070 BTOR_PUSH_STACK (tree, btor_aig_get_right_child (amgr, root));
1071 BTOR_PUSH_STACK (tree, btor_aig_get_left_child (amgr, root));
1072
1073 while (!BTOR_EMPTY_STACK (tree))
1074 {
1075 cur = BTOR_POP_STACK (tree);
1076 real_cur = BTOR_REAL_ADDR_AIG (cur);
1077
1078 if (btor_aig_is_const (real_cur))
1079 {
1080 assert (cur == BTOR_AIG_FALSE);
1081 continue;
1082 }
1083
1084 if (real_cur->mark) continue;
1085
1086 if (!BTOR_IS_INVERTED_AIG (cur) && btor_aig_is_and (real_cur))
1087 {
1088 BTOR_PUSH_STACK (tree, btor_aig_get_right_child (amgr, real_cur));
1089 BTOR_PUSH_STACK (tree, btor_aig_get_left_child (amgr, real_cur));
1090 }
1091 else
1092 {
1093 BTOR_PUSH_STACK (*leafs, cur);
1094 real_cur->mark = 1;
1095 }
1096 }
1097
1098 for (p = (*leafs).start; p < (*leafs).top; p++)
1099 {
1100 cur = *p;
1101 assert (BTOR_REAL_ADDR_AIG (cur)->mark);
1102 BTOR_REAL_ADDR_AIG (cur)->mark = 0;
1103 }
1104
1105 BTOR_RELEASE_STACK (tree);
1106 return true;
1107 }
1108 #endif
1109
1110 void
btor_aig_to_sat_tseitin(BtorAIGMgr * amgr,BtorAIG * start)1111 btor_aig_to_sat_tseitin (BtorAIGMgr *amgr, BtorAIG *start)
1112 {
1113 BtorAIGPtrStack stack, tree, leafs, marked;
1114 int32_t x, y, a, b, c;
1115 bool isxor, isite;
1116 BtorAIG *root, *cur;
1117 BtorSATMgr *smgr;
1118 BtorMemMgr *mm;
1119 uint32_t local;
1120 BtorAIG **p;
1121
1122 if (btor_aig_is_const (start)) return;
1123
1124 assert (amgr);
1125
1126 smgr = amgr->smgr;
1127 mm = amgr->btor->mm;
1128
1129 BTOR_INIT_STACK (mm, stack);
1130 BTOR_INIT_STACK (mm, tree);
1131 BTOR_INIT_STACK (mm, leafs);
1132 BTOR_INIT_STACK (mm, marked);
1133
1134 start = BTOR_REAL_ADDR_AIG (start);
1135 BTOR_PUSH_STACK (stack, start);
1136
1137 while (!BTOR_EMPTY_STACK (stack))
1138 {
1139 root = BTOR_REAL_ADDR_AIG (BTOR_POP_STACK (stack));
1140
1141 if (root->mark == 2)
1142 {
1143 assert (root->cnf_id);
1144 assert (root->local < root->refs);
1145 root->local++;
1146 continue;
1147 }
1148
1149 if (root->cnf_id) continue;
1150
1151 if (btor_aig_is_var (root))
1152 {
1153 set_next_id_aig_mgr (amgr, root);
1154 continue;
1155 }
1156
1157 assert (root->mark < 2);
1158 assert (btor_aig_is_and (root));
1159 assert (BTOR_EMPTY_STACK (tree));
1160 assert (BTOR_EMPTY_STACK (leafs));
1161
1162 if ((isxor = is_xor_aig (amgr, root, &leafs)))
1163 isite = 0;
1164 else
1165 isite = is_ite_aig (amgr, root, &leafs);
1166
1167 if (!isxor && !isite)
1168 {
1169 #ifdef BTOR_AIG_TO_CNF_NARY_AND
1170 BTOR_PUSH_STACK (tree, btor_aig_get_right_child (amgr, root));
1171 BTOR_PUSH_STACK (tree, btor_aig_get_left_child (amgr, root));
1172
1173 while (!BTOR_EMPTY_STACK (tree))
1174 {
1175 cur = BTOR_POP_STACK (tree);
1176
1177 if (BTOR_IS_INVERTED_AIG (cur) || btor_aig_is_var (cur)
1178 || cur->refs > 1u || cur->cnf_id)
1179 {
1180 BTOR_PUSH_STACK (leafs, cur);
1181 }
1182 else
1183 {
1184 BTOR_PUSH_STACK (tree, btor_aig_get_right_child (amgr, cur));
1185 BTOR_PUSH_STACK (tree, btor_aig_get_left_child (amgr, cur));
1186 }
1187 }
1188 #else
1189 BTOR_PUSH_STACK (leafs, btor_aig_get_left_child (amgr, root));
1190 BTOR_PUSH_STACK (leafs, btor_aig_get_right_child (amgr, root));
1191 #endif
1192 }
1193
1194 if (root->mark == 0)
1195 {
1196 root->mark = 1;
1197 assert (root->refs >= 1);
1198 assert (!root->local);
1199 root->local = 1;
1200 BTOR_PUSH_STACK (marked, root);
1201 BTOR_PUSH_STACK (stack, root);
1202 for (p = leafs.start; p < leafs.top; p++) BTOR_PUSH_STACK (stack, *p);
1203 }
1204 else
1205 {
1206 assert (root->mark == 1);
1207 root->mark = 2;
1208
1209 set_next_id_aig_mgr (amgr, root);
1210 x = root->cnf_id;
1211 assert (x);
1212
1213 if (isxor)
1214 {
1215 assert (BTOR_COUNT_STACK (leafs) == 2);
1216 a = btor_aig_get_cnf_id (leafs.start[0]);
1217 b = btor_aig_get_cnf_id (leafs.start[1]);
1218
1219 btor_sat_add (smgr, -x);
1220 btor_sat_add (smgr, a);
1221 btor_sat_add (smgr, -b);
1222 btor_sat_add (smgr, 0);
1223
1224 btor_sat_add (smgr, -x);
1225 btor_sat_add (smgr, -a);
1226 btor_sat_add (smgr, b);
1227 btor_sat_add (smgr, 0);
1228
1229 btor_sat_add (smgr, x);
1230 btor_sat_add (smgr, -a);
1231 btor_sat_add (smgr, -b);
1232 btor_sat_add (smgr, 0);
1233
1234 btor_sat_add (smgr, x);
1235 btor_sat_add (smgr, a);
1236 btor_sat_add (smgr, b);
1237 btor_sat_add (smgr, 0);
1238 amgr->num_cnf_clauses += 4;
1239 amgr->num_cnf_literals += 12;
1240 }
1241 else if (isite)
1242 {
1243 assert (BTOR_COUNT_STACK (leafs) == 3);
1244 a = btor_aig_get_cnf_id (leafs.start[0]); // else
1245 b = btor_aig_get_cnf_id (leafs.start[1]); // then
1246 c = btor_aig_get_cnf_id (leafs.start[2]); // cond
1247
1248 btor_sat_add (smgr, -x);
1249 btor_sat_add (smgr, -c);
1250 btor_sat_add (smgr, b);
1251 btor_sat_add (smgr, 0);
1252
1253 btor_sat_add (smgr, -x);
1254 btor_sat_add (smgr, c);
1255 btor_sat_add (smgr, a);
1256 btor_sat_add (smgr, 0);
1257
1258 btor_sat_add (smgr, x);
1259 btor_sat_add (smgr, -c);
1260 btor_sat_add (smgr, -b);
1261 btor_sat_add (smgr, 0);
1262
1263 btor_sat_add (smgr, x);
1264 btor_sat_add (smgr, c);
1265 btor_sat_add (smgr, -a);
1266 btor_sat_add (smgr, 0);
1267 amgr->num_cnf_clauses += 4;
1268 amgr->num_cnf_literals += 12;
1269 }
1270 else
1271 {
1272 for (p = leafs.start; p < leafs.top; p++)
1273 {
1274 cur = *p;
1275 y = btor_aig_get_cnf_id (cur);
1276 assert (y);
1277 btor_sat_add (smgr, -y);
1278 amgr->num_cnf_literals++;
1279 }
1280 btor_sat_add (smgr, x);
1281 btor_sat_add (smgr, 0);
1282 amgr->num_cnf_clauses++;
1283 amgr->num_cnf_literals++;
1284
1285 for (p = leafs.start; p < leafs.top; p++)
1286 {
1287 cur = *p;
1288 y = btor_aig_get_cnf_id (cur);
1289 btor_sat_add (smgr, -x);
1290 btor_sat_add (smgr, y);
1291 btor_sat_add (smgr, 0);
1292 amgr->num_cnf_clauses++;
1293 amgr->num_cnf_literals += 2;
1294 }
1295 }
1296 }
1297 BTOR_RESET_STACK (leafs);
1298 }
1299 BTOR_RELEASE_STACK (stack);
1300 BTOR_RELEASE_STACK (leafs);
1301 BTOR_RELEASE_STACK (tree);
1302
1303 while (!BTOR_EMPTY_STACK (marked))
1304 {
1305 cur = BTOR_POP_STACK (marked);
1306 assert (!BTOR_IS_INVERTED_AIG (cur));
1307 assert (cur->mark > 0);
1308 cur->mark = 0;
1309 assert (cur->cnf_id);
1310 assert (btor_aig_is_and (cur));
1311 local = cur->local;
1312 assert (local > 0);
1313 cur->local = 0;
1314 if (cur == start) continue;
1315 assert (cur->refs >= local);
1316 if (cur->refs > local) continue;
1317 release_cnf_id_aig_mgr (amgr, cur);
1318 }
1319 BTOR_RELEASE_STACK (marked);
1320 }
1321
1322 static void
aig_to_sat_tseitin(BtorAIGMgr * amgr,BtorAIG * aig)1323 aig_to_sat_tseitin (BtorAIGMgr *amgr, BtorAIG *aig)
1324 {
1325 assert (amgr);
1326 assert (!btor_aig_is_const (aig));
1327 BTOR_MSG (amgr->btor->msg,
1328 3,
1329 "transforming AIG into CNF using Tseitin transformation");
1330 btor_aig_to_sat_tseitin (amgr, aig);
1331 }
1332
1333 void
btor_aig_to_sat(BtorAIGMgr * amgr,BtorAIG * aig)1334 btor_aig_to_sat (BtorAIGMgr *amgr, BtorAIG *aig)
1335 {
1336 assert (amgr);
1337 if (!btor_sat_is_initialized (amgr->smgr)) return;
1338 if (!btor_aig_is_const (aig)) aig_to_sat_tseitin (amgr, aig);
1339 }
1340
1341 void
btor_aig_add_toplevel_to_sat(BtorAIGMgr * amgr,BtorAIG * root)1342 btor_aig_add_toplevel_to_sat (BtorAIGMgr *amgr, BtorAIG *root)
1343 {
1344 assert (amgr);
1345 assert (root);
1346
1347 if (!btor_sat_is_initialized (amgr->smgr)) return;
1348
1349 #ifdef BTOR_AIG_TO_CNF_TOP_ELIM
1350 BtorMemMgr *mm;
1351 BtorSATMgr *smgr;
1352 BtorAIG *aig, *left;
1353 BtorAIGPtrStack stack;
1354 #ifdef BTOR_EXTRACT_TOP_LEVEL_MULTI_OR
1355 BtorAIGPtrStack leafs;
1356 BtorAIG **p;
1357 #else
1358 BtorAIG *real_aig, *right;
1359 #endif
1360
1361 mm = amgr->btor->mm;
1362 smgr = amgr->smgr;
1363
1364 if (!btor_sat_is_initialized (smgr)) return;
1365
1366 if (root == BTOR_AIG_TRUE) return;
1367
1368 if (root == BTOR_AIG_FALSE)
1369 {
1370 btor_sat_add (smgr, 0); /* add empty clause */
1371 amgr->num_cnf_clauses++;
1372 return;
1373 }
1374
1375 BTOR_INIT_STACK (mm, stack);
1376 aig = root;
1377 goto BTOR_ADD_TOPLEVEL_AIG_TO_SAT_WITHOUT_POP;
1378
1379 while (!BTOR_EMPTY_STACK (stack))
1380 {
1381 aig = BTOR_POP_STACK (stack);
1382 BTOR_ADD_TOPLEVEL_AIG_TO_SAT_WITHOUT_POP:
1383 if (!BTOR_IS_INVERTED_AIG (aig) && btor_aig_is_and (aig))
1384 {
1385 BTOR_PUSH_STACK (stack, btor_aig_get_right_child (amgr, aig));
1386 BTOR_PUSH_STACK (stack, btor_aig_get_left_child (amgr, aig));
1387 }
1388 else
1389 {
1390 #ifdef BTOR_EXTRACT_TOP_LEVEL_MULTI_OR
1391 BTOR_INIT_STACK (mm, leafs);
1392 if (is_or_aig (amgr, aig, &leafs))
1393 {
1394 assert (BTOR_COUNT_STACK (leafs) > 1);
1395 for (p = leafs.start; p < leafs.top; p++)
1396 {
1397 left = *p;
1398 if (btor_aig_is_const (left)) // TODO reachable?
1399 continue;
1400 btor_aig_to_sat (amgr, left);
1401 }
1402 for (p = leafs.start; p < leafs.top; p++)
1403 {
1404 left = *p;
1405 assert (btor_aig_get_cnf_id (left));
1406 btor_sat_add (smgr, btor_aig_get_cnf_id (BTOR_INVERT_AIG (left)));
1407 amgr->num_cnf_literals++;
1408 }
1409 btor_sat_add (smgr, 0);
1410 amgr->num_cnf_clauses++;
1411 }
1412 else
1413 {
1414 btor_aig_to_sat (amgr, aig);
1415 btor_sat_add (smgr, btor_aig_get_cnf_id (aig));
1416 btor_sat_add (smgr, 0);
1417 amgr->num_cnf_literals++;
1418 amgr->num_cnf_clauses++;
1419 }
1420 BTOR_RELEASE_STACK (leafs);
1421 #else
1422 real_aig = BTOR_REAL_ADDR_AIG (aig);
1423 if (BTOR_IS_INVERTED_AIG (aig) && btor_aig_is_and (real_aig))
1424 {
1425 left = BTOR_INVERT_AIG (btor_aig_get_left_child (amgr, real_aig));
1426 right = BTOR_INVERT_AIG (btor_aig_get_right_child (amgr, real_aig));
1427 btor_aig_to_sat (amgr, left);
1428 btor_aig_to_sat (amgr, right);
1429 btor_sat_add (smgr, btor_aig_get_cnf_id (left));
1430 btor_sat_add (smgr, btor_aig_get_cnf_id (right));
1431 btor_sat_add (smgr, 0);
1432 amgr->num_cnf_clauses++;
1433 amgr->num_cnf_literals += 2;
1434 }
1435 else
1436 {
1437 btor_aig_to_sat (amgr, aig);
1438 btor_sat_add (smgr, btor_aig_get_cnf_id (aig));
1439 btor_sat_add (smgr, 0);
1440 amgr->num_cnf_clauses++;
1441 amgr->num_cnf_literals++;
1442 }
1443 #endif
1444 }
1445 }
1446 BTOR_RELEASE_STACK (stack);
1447 #else
1448 if (root == BTOR_AIG_TRUE) return;
1449
1450 if (root == BTOR_AIG_FALSE)
1451 {
1452 btor_sat_add (amgr->smgr, 0);
1453 return;
1454 }
1455 btor_aig_to_sat (amgr, root);
1456 btor_sat_add (amgr->smgr, btor_aig_get_cnf_id (root));
1457 btor_sat_add (amgr->smgr, 0);
1458 #endif
1459 }
1460
1461 BtorSATMgr *
btor_aig_get_sat_mgr(const BtorAIGMgr * amgr)1462 btor_aig_get_sat_mgr (const BtorAIGMgr *amgr)
1463 {
1464 return amgr ? amgr->smgr : 0;
1465 }
1466
1467 int32_t
btor_aig_get_assignment(BtorAIGMgr * amgr,BtorAIG * aig)1468 btor_aig_get_assignment (BtorAIGMgr *amgr, BtorAIG *aig)
1469 {
1470 assert (amgr);
1471 if (aig == BTOR_AIG_TRUE) return 1;
1472 if (aig == BTOR_AIG_FALSE) return -1;
1473
1474 /* Note: If an AIG is not yet encoded to SAT or if the SAT solver returns
1475 * undefined for a variable, we implicitly initialize it with false (-1). */
1476 int32_t val = -1;
1477 if (BTOR_REAL_ADDR_AIG (aig)->cnf_id > 0)
1478 {
1479 val = btor_sat_deref (amgr->smgr, BTOR_REAL_ADDR_AIG (aig)->cnf_id);
1480 if (val == 0)
1481 {
1482 val = -1;
1483 }
1484 }
1485 return BTOR_IS_INVERTED_AIG (aig) ? -val : val;
1486 }
1487
1488 int32_t
btor_aig_compare(const BtorAIG * aig0,const BtorAIG * aig1)1489 btor_aig_compare (const BtorAIG *aig0, const BtorAIG *aig1)
1490 {
1491 if (aig0 == aig1) return 0;
1492 if (BTOR_INVERT_AIG (aig0) == aig1)
1493 return BTOR_IS_INVERTED_AIG (aig0) ? -1 : 1;
1494 if (BTOR_IS_INVERTED_AIG (aig0)) aig0 = BTOR_INVERT_AIG (aig0);
1495 if (aig0 == BTOR_AIG_FALSE) return -1;
1496 assert (aig0 != BTOR_AIG_TRUE);
1497 if (BTOR_IS_INVERTED_AIG (aig1)) aig1 = BTOR_INVERT_AIG (aig1);
1498 if (aig1 == BTOR_AIG_FALSE) return 1;
1499 assert (aig1 != BTOR_AIG_TRUE);
1500 return aig0->id - aig1->id;
1501 }
1502
1503 /* hash AIG by id */
1504 uint32_t
btor_aig_hash_by_id(const BtorAIG * aig)1505 btor_aig_hash_by_id (const BtorAIG *aig)
1506 {
1507 assert (aig);
1508 return (uint32_t) btor_aig_get_id (aig) * 7334147u;
1509 }
1510
1511 /* compare AIG by id */
1512 int32_t
btor_aig_compare_by_id(const BtorAIG * aig0,const BtorAIG * aig1)1513 btor_aig_compare_by_id (const BtorAIG *aig0, const BtorAIG *aig1)
1514 {
1515 assert (aig0);
1516 assert (aig1);
1517
1518 int32_t id0, id1;
1519
1520 id0 = btor_aig_get_id (aig0);
1521 id1 = btor_aig_get_id (aig1);
1522 if (id0 < id1) return -1;
1523 if (id0 > id1) return 1;
1524 return 0;
1525 }
1526
1527 int32_t
btor_compare_aig_by_id_qsort_asc(const void * aig0,const void * aig1)1528 btor_compare_aig_by_id_qsort_asc (const void *aig0, const void *aig1)
1529 {
1530 assert (aig0);
1531 assert (!btor_aig_is_const (aig0));
1532 assert (aig1);
1533 assert (!btor_aig_is_const (aig1));
1534
1535 int32_t id0, id1;
1536
1537 id0 = BTOR_REAL_ADDR_AIG (*(BtorAIG **) aig0)->id;
1538 id1 = BTOR_REAL_ADDR_AIG (*(BtorAIG **) aig1)->id;
1539 return id0 - id1;
1540 }
1541