1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 aig.cpp
7
8 Abstract:
9
10 And-inverted graphs
11
12 Author:
13
14 Leonardo (leonardo) 2011-05-13
15
16 Notes:
17
18 --*/
19 #include "tactic/aig/aig.h"
20 #include "tactic/goal.h"
21 #include "ast/ast_smt2_pp.h"
22
23 #define USE_TWO_LEVEL_RULES
24 #define FIRST_NODE_ID (UINT_MAX/2)
25
26 struct aig;
27
28 class aig_lit {
29 friend class aig_ref;
30 aig * m_ref;
31 public:
aig_lit(aig * n=nullptr)32 aig_lit(aig * n = nullptr):m_ref(n) {}
aig_lit(aig_ref const & r)33 aig_lit(aig_ref const & r):m_ref(static_cast<aig*>(r.m_ref)) {}
is_inverted() const34 bool is_inverted() const { return (reinterpret_cast<size_t>(m_ref) & static_cast<size_t>(1)) == static_cast<size_t>(1); }
invert()35 void invert() { m_ref = reinterpret_cast<aig*>(reinterpret_cast<size_t>(m_ref) ^ static_cast<size_t>(1)); }
ptr() const36 aig * ptr() const { return reinterpret_cast<aig*>(reinterpret_cast<size_t>(m_ref) & ~static_cast<size_t>(1)); }
ptr_non_inverted() const37 aig * ptr_non_inverted() const { SASSERT(!is_inverted()); return m_ref; }
is_null() const38 bool is_null() const { return m_ref == nullptr; }
operator ==(aig_lit const & r1,aig_lit const & r2)39 friend bool operator==(aig_lit const & r1, aig_lit const & r2) { return r1.m_ref == r2.m_ref; }
operator !=(aig_lit const & r1,aig_lit const & r2)40 friend bool operator!=(aig_lit const & r1, aig_lit const & r2) { return r1.m_ref != r2.m_ref; }
operator =(aig_lit const & r)41 aig_lit & operator=(aig_lit const & r) { m_ref = r.m_ref; return *this; }
42 static aig_lit null;
43 };
44
45 aig_lit aig_lit::null;
46
47 struct aig {
48 unsigned m_id;
49 unsigned m_ref_count;
50 aig_lit m_children[2];
51 unsigned m_mark:1;
aigaig52 aig() {}
53 };
54
55 #if Z3DEBUG
is_true(aig_lit const & r)56 inline bool is_true(aig_lit const & r) { return !r.is_inverted() && r.ptr_non_inverted()->m_id == 0; }
57 #endif
58 // inline bool is_false(aig_lit const & r) { return r.is_inverted() && r.ptr()->m_id == 0; }
is_var(aig * n)59 inline bool is_var(aig * n) { return n->m_children[0].is_null(); }
is_var(aig_lit const & n)60 inline bool is_var(aig_lit const & n) { return is_var(n.ptr()); }
id(aig_lit const & n)61 inline unsigned id(aig_lit const & n) { return n.ptr()->m_id; }
ref_count(aig_lit const & n)62 inline unsigned ref_count(aig_lit const & n) { return n.ptr()->m_ref_count; }
left(aig * n)63 inline aig_lit left(aig * n) { return n->m_children[0]; }
right(aig * n)64 inline aig_lit right(aig * n) { return n->m_children[1]; }
left(aig_lit const & n)65 inline aig_lit left(aig_lit const & n) { return left(n.ptr()); }
right(aig_lit const & n)66 inline aig_lit right(aig_lit const & n) { return right(n.ptr()); }
67
to_idx(aig * p)68 inline unsigned to_idx(aig * p) { SASSERT(!is_var(p)); return p->m_id - FIRST_NODE_ID; }
69
70
unmark(unsigned sz,aig * const * ns)71 static void unmark(unsigned sz, aig * const * ns) {
72 for (unsigned i = 0; i < sz; i++) {
73 ns[i]->m_mark = false;
74 }
75 }
76
77 struct aig_hash {
operator ()aig_hash78 unsigned operator()(aig * n) const {
79 SASSERT(!is_var(n));
80 return hash_u_u(id(n->m_children[0]), id(n->m_children[1]));
81 }
82 };
83
84 struct aig_eq {
operator ()aig_eq85 bool operator()(aig * n1, aig * n2) const {
86 SASSERT(!is_var(n1));
87 SASSERT(!is_var(n2));
88 return
89 n1->m_children[0] == n2->m_children[0] &&
90 n1->m_children[1] == n2->m_children[1];
91 }
92 };
93
94 class aig_table : public chashtable<aig*, aig_hash, aig_eq> {
95 public:
96 };
97
98 struct aig_lit_lt {
operator ()aig_lit_lt99 bool operator()(aig_lit const & l1, aig_lit const & l2) const {
100 if (id(l1) < id(l2)) return true;
101 if (id(l1) == id(l2)) return l1.is_inverted() && !l2.is_inverted();
102 return false;
103 }
104 };
105
106 struct aig_manager::imp {
107 id_gen m_var_id_gen;
108 id_gen m_node_id_gen;
109 aig_table m_table;
110 unsigned m_num_aigs;
111 expr_ref_vector m_var2exprs;
112 small_object_allocator m_allocator;
113 ptr_vector<aig> m_to_delete;
114 aig_lit m_true;
115 aig_lit m_false;
116 bool m_default_gate_encoding;
117 unsigned long long m_max_memory;
118
dec_ref_coreaig_manager::imp119 void dec_ref_core(aig * n) {
120 SASSERT(n->m_ref_count > 0);
121 n->m_ref_count--;
122 if (n->m_ref_count == 0)
123 m_to_delete.push_back(n);
124 }
125
checkpointaig_manager::imp126 void checkpoint() {
127 if (memory::get_allocation_size() > m_max_memory)
128 throw aig_exception(TACTIC_MAX_MEMORY_MSG);
129 if (!m().inc())
130 throw aig_exception(m().limit().get_cancel_msg());
131 }
132
dec_ref_coreaig_manager::imp133 void dec_ref_core(aig_lit const & r) { dec_ref_core(r.ptr()); }
134
dec_ref_resultaig_manager::imp135 void dec_ref_result(aig * n) { SASSERT(n->m_ref_count > 0); n->m_ref_count--; }
dec_ref_resultaig_manager::imp136 void dec_ref_result(aig_lit const & r) { dec_ref_result(r.ptr()); }
137
process_to_deleteaig_manager::imp138 void process_to_delete() {
139 while (!m_to_delete.empty()) {
140 aig * n = m_to_delete.back();
141 m_to_delete.pop_back();
142 delete_node(n);
143 }
144 }
145
delete_nodeaig_manager::imp146 void delete_node(aig * n) {
147 TRACE("aig_lit_count", tout << "deleting: "; display_ref(tout, n); tout << "\n";);
148 SASSERT(m_num_aigs > 0);
149 m_num_aigs--;
150 if (is_var(n)) {
151 m_var_id_gen.recycle(n->m_id);
152 m_var2exprs.set(n->m_id, nullptr);
153 }
154 else {
155 m_table.erase(n);
156 m_node_id_gen.recycle(n->m_id);
157 dec_ref_core(n->m_children[0]);
158 dec_ref_core(n->m_children[1]);
159 }
160 m_allocator.deallocate(sizeof(aig), n);
161 }
162
allocate_nodeaig_manager::imp163 aig * allocate_node() {
164 return static_cast<aig*>(m_allocator.allocate(sizeof(aig)));
165 }
166
mk_varaig_manager::imp167 aig * mk_var(expr * t) {
168 m_num_aigs++;
169 aig * r = allocate_node();
170 r->m_id = m_var_id_gen.mk();
171 r->m_ref_count = 0;
172 r->m_mark = false;
173 r->m_children[0] = aig_lit();
174 SASSERT(r->m_id <= m_var2exprs.size());
175 if (r->m_id == m_var2exprs.size())
176 m_var2exprs.push_back(t);
177 else
178 m_var2exprs.set(r->m_id, t);
179 return r;
180 }
181
mk_node_coreaig_manager::imp182 aig_lit mk_node_core(aig_lit const & l, aig_lit const & r) {
183 aig * new_node = allocate_node();
184 new_node->m_children[0] = l;
185 new_node->m_children[1] = r;
186 aig * old_node = m_table.insert_if_not_there(new_node);
187 if (old_node != new_node) {
188 m_allocator.deallocate(sizeof(aig), new_node);
189 return aig_lit(old_node);
190 }
191 m_num_aigs++;
192 new_node->m_id = m_node_id_gen.mk();
193 new_node->m_ref_count = 0;
194 new_node->m_mark = false;
195 SASSERT(new_node->m_ref_count == 0);
196 inc_ref(l);
197 inc_ref(r);
198 return aig_lit(new_node);
199 }
200
is_not_eqaig_manager::imp201 bool is_not_eq(aig_lit const & l, aig_lit const & r) const {
202 return l.ptr() == r.ptr() && l.is_inverted() != r.is_inverted();
203 }
204
205 /**
206 \brief Create an AIG representing (l and r)
207 Apply two-level minimization rules that guarantee that
208 locally the size is decreasing, and globally is not increasing.
209 */
mk_nodeaig_manager::imp210 aig_lit mk_node(aig_lit l, aig_lit r) {
211 start:
212 bool sign1 = l.is_inverted();
213 aig * n1 = l.ptr();
214 bool sign2 = r.is_inverted();
215 aig * n2 = r.ptr();
216
217 if (n1->m_id == 0) {
218 if (sign1)
219 return m_false; // false and r
220 else
221 return r; // true and r
222 }
223
224 if (n2->m_id == 0) {
225 if (sign2)
226 return m_false; // l and false;
227 else
228 return l; // l and true;
229 }
230
231 if (n1 == n2) {
232 if (sign1 == sign2)
233 return l; // l and l;
234 else
235 return m_false; // l and not l
236 }
237
238 #ifdef USE_TWO_LEVEL_RULES
239 if (!is_var(n1)) {
240 aig_lit a = n1->m_children[0];
241 aig_lit b = n1->m_children[1];
242
243 if (is_not_eq(a, r) || is_not_eq(b, r)) {
244 if (sign1) {
245 // substitution
246 return r; // (not (a and b)) and r --> r IF a = (not r) or b = (not r)
247 }
248 else {
249 // contradiction
250 return m_false; // (a and b) and r --> false IF a = (not r) or b = (not r)
251 }
252 }
253 if (a == r) {
254 if (sign1) {
255 // substitution
256 // not (a and b) and r --> (not b) and r IF a == r
257 l = b;
258 l.invert();
259 goto start;
260 }
261 else {
262 // substitution
263 return l; // (a and b) and r --> (a and b) IF a = r
264 }
265 }
266 if (b == r) {
267 if (sign1) {
268 // substitution
269 // not (a and b) and r --> (not a) and r IF b == r
270 l = a;
271 l.invert();
272 goto start;
273 }
274 else {
275 // substitution
276 return l; // (a and b) and r --> (a and b) IF b = r;
277 }
278 }
279
280 if (!is_var(n2)) {
281 aig_lit c = n2->m_children[0];
282 aig_lit d = n2->m_children[1];
283
284 if (!sign1 && !sign2) {
285 // contradiction
286 if (is_not_eq(a, c) || is_not_eq(a, d) || is_not_eq(b, c) || is_not_eq(b, d))
287 return m_false; // (a and b) and (c and d) --> false IF a = not(c) OR a = not(d) or b = not(c) or b = not(d)
288 // idempotence
289 if (a == c || b == c) {
290 r = d; // (a and b) and (c and d) --> (a and b) and d IF a == c or b == c
291 goto start;
292 }
293 // idempotence
294 if (b == c || b == d) {
295 l = a; // (a and b) and (c and d) --> a and (c and d) IF b == c or b == d
296 goto start;
297 }
298 // idempotence
299 if (a == d || b == d) {
300 r = c;
301 goto start; // (a and b) and (c and d) --> (a and b) and c IF a == d or b == d
302 }
303 // idempotence
304 if (a == c || a == d) {
305 l = b; // (a and b) and (c and d) --> b and (c and d) IF a == c or a == d
306 goto start;
307 }
308 }
309
310 if (sign1 && !sign2) {
311 // subsumption
312 if (is_not_eq(a, c) || is_not_eq(a, d) || is_not_eq(b, c) || is_not_eq(b, d))
313 return r; // not (a and b) and (c and d) --> (c and d)
314
315 // substitution
316 if (b == c || b == d) {
317 // not (a and b) and (c and d) --> (not a) and (c and d)
318 a.invert();
319 l = a;
320 goto start;
321 }
322
323 // substitution
324 if (a == c || a == d) {
325 // not (a and b) and (c and d) --> (not b) and (c and d)
326 b.invert();
327 l = b;
328 goto start;
329 }
330 }
331
332 if (!sign1 && sign2) {
333 // subsumption
334 if (is_not_eq(a, c) || is_not_eq(a, d) || is_not_eq(b, c) || is_not_eq(b, d))
335 return l; // (a and b) and not (c and d) --> (a and b)
336
337 // substitution
338 if (c == a || c == b) {
339 // (a and b) and not (c and d) --> (a and b) and (not d);
340 d.invert();
341 r = d;
342 goto start;
343 }
344
345 // substitution
346 if (d == a || d == b) {
347 // (a and b) and not (c and d) --> (a and b) and (not c);
348 c.invert();
349 r = c;
350 goto start;
351 }
352 }
353
354 if (sign1 && sign2) {
355 // resolution
356 if (a == c && is_not_eq(b, d)) {
357 a.invert(); // (not (a and b)) and (not (a and (not b))) --> not a
358 return a;
359 }
360 SASSERT(!(a == d && is_not_eq(b, c))); // cannot happen because we sort args
361 // resolution
362 if (is_not_eq(a, c) && b == d) {
363 b.invert(); // (not (a and b)) and (not (a and (not b))) --> not b
364 return b;
365 }
366 SASSERT(!(is_not_eq(a, d) && b == c)); // cannot happen because we sort args
367 }
368 }
369 }
370
371 if (!is_var(n2)) {
372 aig_lit a = n2->m_children[0];
373 aig_lit b = n2->m_children[1];
374 if (is_not_eq(l, a) || is_not_eq(l, b)) {
375 if (sign2) {
376 // substitution
377 return l; // l and (not (a and b)) --> l IF a = (not l) or b = (not l)
378 }
379 else {
380 // contradiction
381 return m_false; // l and (a and b) --> false IF a = (not l) or b = (not l)
382 }
383 }
384 if (a == l) {
385 if (sign2) {
386 // substitution
387 // l and not (a and b) and r --> l and (not b) IF a == l
388 r = b;
389 r.invert();
390 goto start;
391 }
392 else {
393 // substitution
394 return r; // l and (a and b) --> (a and b) IF a = l;
395 }
396 }
397 if (b == l) {
398 if (sign2) {
399 // substitution
400 // l and not (a and b) --> l and (not a) IF b == l
401 r = a;
402 r.invert();
403 goto start;
404 }
405 else {
406 // substitution
407 return r; // l and (a and b) --> (a and b) IF b = l;
408 }
409 }
410 }
411 #endif
412
413 if (n1->m_id > n2->m_id)
414 return mk_node_core(r, l);
415 else
416 return mk_node_core(l, r);
417 }
418
419 struct expr2aig {
420 struct frame {
421 app * m_t;
422 unsigned m_idx;
423 unsigned m_spos;
frameaig_manager::imp::expr2aig::frame424 frame(app * t, unsigned spos):m_t(t), m_idx(0), m_spos(spos) {}
425 };
426 imp & m;
427 svector<frame> m_frame_stack;
428 svector<aig_lit> m_result_stack;
429 obj_map<expr, aig_lit> m_cache;
430
expr2aigaig_manager::imp::expr2aig431 expr2aig(imp & _m):m(_m) {}
432
~expr2aigaig_manager::imp::expr2aig433 ~expr2aig() {
434 obj_map<expr, aig_lit>::iterator it = m_cache.begin();
435 obj_map<expr, aig_lit>::iterator end = m_cache.end();
436 for (; it != end; ++it) {
437 TRACE("expr2aig", tout << "dec-ref: "; m.display_ref(tout, it->m_value);
438 tout << " ref-count: " << ref_count(it->m_value) << "\n";);
439 m.dec_ref(it->m_value);
440 }
441 restore_result_stack(0);
442 }
443
save_resultaig_manager::imp::expr2aig444 void save_result(aig_lit & r) {
445 m.inc_ref(r);
446 m_result_stack.push_back(r);
447 }
448
cache_resultaig_manager::imp::expr2aig449 void cache_result(expr * t, aig_lit const & r) {
450 TRACE("expr2aig", tout << "caching:\n" << mk_ismt2_pp(t, m.m()) << "\n---> "; m.display_ref(tout, r); tout << "\n";);
451 SASSERT(!m_cache.contains(t));
452 m.inc_ref(r);
453 m_cache.insert(t, r);
454 }
455
is_cachedaig_manager::imp::expr2aig456 bool is_cached(expr * t) {
457 aig_lit r;
458 if (m_cache.find(t, r)) {
459 save_result(r);
460 return true;
461 }
462 return false;
463 }
464
process_varaig_manager::imp::expr2aig465 void process_var(expr * t) {
466 if (is_cached(t))
467 return;
468 aig_lit r(m.mk_var(t));
469 SASSERT(ref_count(r) == 0);
470 cache_result(t, r);
471 save_result(r);
472 }
473
mk_frameaig_manager::imp::expr2aig474 void mk_frame(app * t) {
475 m_frame_stack.push_back(frame(t, m_result_stack.size()));
476 }
477
visitaig_manager::imp::expr2aig478 bool visit(expr * t) {
479 if (is_app(t)) {
480 app * tapp = to_app(t);
481 if (tapp->get_family_id() == m.m().get_basic_family_id()) {
482 switch (tapp->get_decl_kind()) {
483 case OP_TRUE: save_result(m.m_true); return true;
484 case OP_FALSE: save_result(m.m_false); return true;
485 case OP_EQ:
486 if (!m.m().is_bool(tapp->get_arg(0)))
487 break;
488 case OP_NOT:
489 case OP_OR:
490 case OP_AND:
491 case OP_XOR:
492 case OP_IMPLIES:
493 case OP_ITE:
494 if (tapp->get_ref_count() > 1 && is_cached(tapp))
495 return true;
496 mk_frame(tapp);
497 return false;
498 default:
499 break;
500 }
501 }
502 process_var(t);
503 return true;
504 }
505 else {
506 // quantifiers and free variables are handled as aig variables
507 process_var(t);
508 return true;
509 }
510 }
511
restore_result_stackaig_manager::imp::expr2aig512 void restore_result_stack(unsigned old_sz) {
513 unsigned sz = m_result_stack.size();
514 SASSERT(old_sz <= sz);
515 for (unsigned i = old_sz; i < sz; i++)
516 m.dec_ref(m_result_stack[i]);
517 m_result_stack.shrink(old_sz);
518 }
519
save_node_resultaig_manager::imp::expr2aig520 void save_node_result(unsigned spos, aig_lit r) {
521 m.inc_ref(r);
522 restore_result_stack(spos);
523 save_result(r);
524 SASSERT(ref_count(r) >= 2);
525 m.dec_ref(r);
526 }
527
mk_oraig_manager::imp::expr2aig528 void mk_or(unsigned spos) {
529 SASSERT(spos <= m_result_stack.size());
530 unsigned num = m_result_stack.size() - spos;
531 aig_lit r = m.mk_or(num, m_result_stack.begin() + spos);
532 save_node_result(spos, r);
533 }
534
mk_andaig_manager::imp::expr2aig535 void mk_and(unsigned spos) {
536 SASSERT(spos <= m_result_stack.size());
537 unsigned num = m_result_stack.size() - spos;
538 aig_lit r = m.mk_and(num, m_result_stack.begin() + spos);
539 save_node_result(spos, r);
540 }
541
mk_iteaig_manager::imp::expr2aig542 void mk_ite(unsigned spos) {
543 SASSERT(spos + 3 == m_result_stack.size());
544 aig_lit r = m.mk_ite(m_result_stack[spos], m_result_stack[spos+1], m_result_stack[spos+2]);
545 save_node_result(spos, r);
546 }
547
mk_iffaig_manager::imp::expr2aig548 void mk_iff(unsigned spos) {
549 if (spos + 2 != m_result_stack.size())
550 throw default_exception("aig conversion assumes expressions have been simplified");
551 SASSERT(spos + 2 == m_result_stack.size());
552 aig_lit r = m.mk_iff(m_result_stack[spos], m_result_stack[spos+1]);
553 save_node_result(spos, r);
554 }
555
mk_xoraig_manager::imp::expr2aig556 void mk_xor(unsigned spos) {
557 SASSERT(spos <= m_result_stack.size());
558 unsigned num = m_result_stack.size() - spos;
559 aig_lit r;
560 switch (num) {
561 case 0:
562 r = m.m_true;
563 break;
564 case 1:
565 r = m_result_stack[spos];
566 break;
567 case 2:
568 r = m.mk_xor(m_result_stack[spos], m_result_stack[spos+1]);
569 break;
570 default:
571 r = m.mk_xor(m_result_stack[spos], m_result_stack[spos+1]);
572 for (unsigned i = 2; i < num; ++i) {
573 r = m.mk_xor(r, m_result_stack[spos + i]);
574 }
575 break;
576 }
577 save_node_result(spos, r);
578 }
579
mk_impliesaig_manager::imp::expr2aig580 void mk_implies(unsigned spos) {
581 SASSERT(spos + 2 == m_result_stack.size());
582 aig_lit r = m.mk_implies(m_result_stack[spos], m_result_stack[spos+1]);
583 save_node_result(spos, r);
584 }
585
mk_aigaig_manager::imp::expr2aig586 void mk_aig(frame & fr) {
587 SASSERT(fr.m_t->get_family_id() == m.m().get_basic_family_id());
588 switch (fr.m_t->get_decl_kind()) {
589 case OP_NOT:
590 m_result_stack[fr.m_spos].invert();
591 break;
592 case OP_OR:
593 mk_or(fr.m_spos);
594 break;
595 case OP_AND:
596 mk_and(fr.m_spos);
597 break;
598 case OP_EQ:
599 SASSERT(m.m().is_bool(fr.m_t->get_arg(0)));
600 mk_iff(fr.m_spos);
601 break;
602 case OP_XOR:
603 mk_xor(fr.m_spos);
604 break;
605 case OP_IMPLIES:
606 mk_implies(fr.m_spos);
607 break;
608 case OP_ITE:
609 mk_ite(fr.m_spos);
610 break;
611 default:
612 UNREACHABLE();
613 }
614 if (fr.m_t->get_ref_count() > 1) {
615 cache_result(fr.m_t, m_result_stack.back());
616 }
617 }
618
operator ()aig_manager::imp::expr2aig619 aig_lit operator()(expr * n) {
620 SASSERT(check_cache());
621 if (!visit(n)) {
622 while (!m_frame_stack.empty()) {
623 loop:
624 m.checkpoint();
625 frame & fr = m_frame_stack.back();
626 if (fr.m_idx == 0 && fr.m_t->get_ref_count() > 1) {
627 if (is_cached(fr.m_t)) {
628 m_frame_stack.pop_back();
629 continue;
630 }
631 }
632 unsigned num_args = fr.m_t->get_num_args();
633 while (fr.m_idx < num_args) {
634 expr * arg = fr.m_t->get_arg(fr.m_idx);
635 fr.m_idx++;
636 if (!visit(arg))
637 goto loop;
638 }
639 mk_aig(fr);
640 m_frame_stack.pop_back();
641 }
642 }
643 SASSERT(m_result_stack.size() == 1);
644 aig_lit r = m_result_stack.back();
645 m_result_stack.pop_back();
646 m.dec_ref_result(r);
647 SASSERT(check_cache());
648 return r;
649 }
650
check_cacheaig_manager::imp::expr2aig651 bool check_cache() const {
652 for (auto const& kv : m_cache) {
653 VERIFY(ref_count(kv.m_value) > 0);
654 }
655 return true;
656 }
657 };
658
659 /**
660 \brief Return true if the AIG represents an if-then-else
661 */
662 template<bool Collect>
is_ite_coreaig_manager::imp663 bool is_ite_core(aig * n, aig_lit & c, aig_lit & t, aig_lit & e) const {
664 if (is_var(n))
665 return false;
666 aig_lit l = left(n);
667 aig_lit r = right(n);
668 if (l.is_inverted() && r.is_inverted()) {
669 aig * l_ptr = l.ptr();
670 aig * r_ptr = r.ptr();
671 if (is_var(l_ptr) || is_var(r_ptr))
672 return false;
673 aig_lit l1 = left(l_ptr);
674 aig_lit l2 = right(l_ptr);
675 aig_lit r1 = left(r_ptr);
676 aig_lit r2 = right(r_ptr);
677 if (is_not_eq(l1, r1)) {
678 if (Collect) {
679 l1.invert(); l2.invert(); r1.invert(); r2.invert();
680 if (l1.is_inverted()) {
681 c = r1; t = l2; e = r2;
682 }
683 else {
684 c = l1; t = r2; e = l2;
685 }
686 }
687 return true;
688 }
689 else if (is_not_eq(l1, r2)) {
690 if (Collect) {
691 l1.invert(); l2.invert(); r1.invert(); r2.invert();
692 if (l1.is_inverted()) {
693 c = r2; t = l2; e = r1;
694 }
695 else {
696 c = l1; t = r1; e = l2;
697 }
698 }
699 return true;
700 }
701 else if (is_not_eq(l2, r1)) {
702 if (Collect) {
703 l1.invert(); l2.invert(); r1.invert(); r2.invert();
704 if (l2.is_inverted()) {
705 c = r1; t = l1; e = r2;
706 }
707 else {
708 c = l2; t = r2; e = l1;
709 }
710 }
711 return true;
712 }
713 else if (is_not_eq(l2, r2)) {
714 if (Collect) {
715 l1.invert(); l2.invert(); r1.invert(); r2.invert();
716 if (l2.is_inverted()) {
717 c = r2; t = l1; e = r1;
718 }
719 else {
720 c = l2; t = r1; e = l1;
721 }
722 }
723 return true;
724 }
725 }
726 return false;
727 }
728
is_iteaig_manager::imp729 bool is_ite(aig * n, aig_lit & c, aig_lit & t, aig_lit & e) const {
730 return is_ite_core<true>(n, c, t, e);
731 }
732
is_iteaig_manager::imp733 bool is_ite(aig * n) const {
734 static aig_lit c, t, e;
735 return is_ite_core<false>(n, c, t, e);
736 }
737
738 /**
739 \brief Return true if the AIG represents an iff
740 */
is_iffaig_manager::imp741 bool is_iff(aig * n) const {
742 if (is_var(n))
743 return false;
744 aig_lit l = left(n);
745 aig_lit r = right(n);
746 if (l.is_inverted() && r.is_inverted()) {
747 if (is_var(l) || is_var(r))
748 return false;
749 return is_not_eq(left(l), left(r)) && is_not_eq(right(l), right(r));
750 }
751 return false;
752 }
753
var2expraig_manager::imp754 expr * var2expr(aig * n) const {
755 SASSERT(is_var(n));
756 return m_var2exprs[n->m_id];
757 }
758
759 struct aig2expr {
760 imp & m;
761 ast_manager & ast_mng;
762 enum kind { AIG_AND,
763 AIG_AUX_AND, // does not have an associated expr
764 AIG_ITE
765 };
766 struct frame {
767 aig * m_node;
768 unsigned m_kind:2;
769 unsigned m_first:1;
frameaig_manager::imp::aig2expr::frame770 frame(aig * n, kind k):m_node(n), m_kind(k), m_first(true) {}
771 };
772 expr_ref_vector m_cache;
773 svector<frame> m_frame_stack;
774
aig2expraig_manager::imp::aig2expr775 aig2expr(imp & _m):m(_m), ast_mng(m.m()), m_cache(ast_mng) {}
776
get_cachedaig_manager::imp::aig2expr777 expr * get_cached(aig * n) {
778 if (is_var(n)) {
779 return n->m_id == 0 ? ast_mng.mk_true() : m.var2expr(n);
780 }
781 else {
782 CTRACE("aig2expr", !is_cached(n), tout << "invalid get_cached for "; m.display_ref(tout, n); tout << "\n";);
783 SASSERT(is_cached(n));
784 return m_cache.get(to_idx(n));
785 }
786 }
787
invertaig_manager::imp::aig2expr788 expr * invert(expr * n) {
789 if (ast_mng.is_not(n))
790 return to_app(n)->get_arg(0);
791 if (ast_mng.is_true(n))
792 return ast_mng.mk_false();
793 SASSERT(!ast_mng.is_false(n));
794 return ast_mng.mk_not(n);
795 }
796
get_cachedaig_manager::imp::aig2expr797 expr * get_cached(aig_lit const & n) {
798 if (n.is_inverted())
799 return invert(get_cached(n.ptr()));
800 else
801 return get_cached(n.ptr());
802 }
803
is_cachedaig_manager::imp::aig2expr804 bool is_cached(aig * n) {
805 if (is_var(n))
806 return true;
807 unsigned idx = to_idx(n);
808 if (idx >= m_cache.size()) {
809 m_cache.resize(idx+1);
810 return false;
811 }
812 return m_cache.get(idx) != nullptr;
813 }
814
cache_resultaig_manager::imp::aig2expr815 void cache_result(aig * n, expr * t) {
816 unsigned idx = to_idx(n);
817 SASSERT(idx < m_cache.size());
818 SASSERT(m_cache.get(idx) == 0);
819 m_cache.set(idx, t);
820 }
821
visit_and_childaig_manager::imp::aig2expr822 void visit_and_child(aig_lit c, bool & visited) {
823 aig * n = c.ptr();
824 if (is_cached(n))
825 return;
826 if (m.is_ite(n))
827 m_frame_stack.push_back(frame(n, AIG_ITE));
828 else if (!c.is_inverted() && n->m_ref_count == 1)
829 m_frame_stack.push_back(frame(n, AIG_AUX_AND));
830 else
831 m_frame_stack.push_back(frame(n, AIG_AND));
832 visited = false;
833 }
834
visit_ite_childaig_manager::imp::aig2expr835 void visit_ite_child(aig_lit c, bool & visited) {
836 aig * n = c.ptr();
837 if (is_cached(n))
838 return;
839 m_frame_stack.push_back(frame(n, m.is_ite(n) ? AIG_ITE : AIG_AND));
840 visited = false;
841 }
842
843 ptr_vector<expr> m_and_children;
844 ptr_vector<aig> m_and_todo;
845
add_childaig_manager::imp::aig2expr846 void add_child(aig_lit c) {
847 aig * n = c.ptr();
848 if (c.is_inverted()) {
849 // adding (not c) since I build an OR node
850 m_and_children.push_back(get_cached(n));
851 return;
852 }
853 if (is_cached(n)) {
854 m_and_children.push_back(invert(get_cached(n)));
855 return;
856 }
857 SASSERT(n->m_ref_count == 1);
858 m_and_todo.push_back(n);
859 }
860
mk_andaig_manager::imp::aig2expr861 void mk_and(aig * n) {
862 m_and_children.reset();
863 m_and_todo.reset();
864 add_child(left(n));
865 add_child(right(n));
866 while (!m_and_todo.empty()) {
867 aig * t = m_and_todo.back();
868 SASSERT(!is_var(t));
869 m_and_todo.pop_back();
870 add_child(left(t));
871 add_child(right(t));
872 }
873 expr * r = ast_mng.mk_not(ast_mng.mk_or(m_and_children.size(), m_and_children.data()));
874 cache_result(n, r);
875 TRACE("aig2expr", tout << "caching AND "; m.display_ref(tout, n); tout << "\n";);
876 }
877
mk_iteaig_manager::imp::aig2expr878 void mk_ite(aig * n) {
879 aig_lit c, t, e;
880 VERIFY(m.is_ite(n, c, t, e));
881 if (c.is_inverted()) {
882 c.invert();
883 std::swap(t, e);
884 }
885 expr * r;
886 if (m.is_not_eq(t, e)) {
887 r = ast_mng.mk_iff(get_cached(c), get_cached(t));
888 }
889 else {
890 r = ast_mng.mk_ite(get_cached(c), get_cached(t), get_cached(e));
891 }
892 cache_result(n, r);
893 TRACE("aig2expr", tout << "caching ITE/IFF "; m.display_ref(tout, n); tout << "\n";);
894 }
895
896 /**
897 \brief Return an expression representing the negation of p.
898 */
process_rootaig_manager::imp::aig2expr899 expr * process_root(aig * r) {
900 if (is_cached(r))
901 return get_cached(r);
902 m_frame_stack.push_back(frame(r, m.is_ite(r) ? AIG_ITE : AIG_AND));
903 while (!m_frame_stack.empty()) {
904 m.checkpoint();
905 frame & fr = m_frame_stack.back();
906 aig * n = fr.m_node;
907 if (is_cached(n)) {
908 m_frame_stack.pop_back();
909 continue;
910 }
911 if (fr.m_first) {
912 fr.m_first = false;
913 bool visited = true;
914 switch (fr.m_kind) {
915 case AIG_AND:
916 case AIG_AUX_AND:
917 visit_and_child(left(n), visited);
918 visit_and_child(right(n), visited);
919 break;
920 case AIG_ITE: {
921 aig_lit a = left(left(n));
922 aig_lit b = right(left(n));
923 aig_lit c = left(right(n));
924 aig_lit d = right(right(n));
925 visit_ite_child(a, visited);
926 visit_ite_child(b, visited);
927 if (c.ptr() != a.ptr() && c.ptr() != b.ptr())
928 visit_ite_child(c, visited);
929 if (d.ptr() != a.ptr() && d.ptr() != b.ptr())
930 visit_ite_child(d, visited);
931 break;
932 }
933 default:
934 UNREACHABLE();
935 break;
936 }
937 if (!visited)
938 continue;
939 }
940 switch (fr.m_kind){
941 case AIG_AUX_AND:
942 // do nothing
943 TRACE("aig2expr", tout << "skipping aux AND "; m.display_ref(tout, n); tout << "\n";);
944 break;
945 case AIG_AND:
946 mk_and(n);
947 break;
948 case AIG_ITE:
949 mk_ite(n);
950 break;
951 default:
952 UNREACHABLE();
953 break;
954 }
955 m_frame_stack.pop_back();
956 }
957 return get_cached(r);
958 }
959
960 /**
961 \brief (Debugging) Naive AIG -> EXPR
962 */
naiveaig_manager::imp::aig2expr963 void naive(aig_lit const & l, expr_ref & r) {
964 expr_ref_vector cache(ast_mng);
965 ptr_vector<aig> todo;
966 todo.push_back(l.ptr());
967 while (!todo.empty()) {
968 aig * t = todo.back();
969 if (is_var(t)) {
970 todo.pop_back();
971 continue;
972 }
973 unsigned idx = to_idx(t);
974 cache.reserve(idx+1);
975 if (cache.get(idx) != nullptr) {
976 todo.pop_back();
977 continue;
978 }
979 bool ok = true;
980 for (unsigned i = 0; i < 2; i++) {
981 aig * c = t->m_children[i].ptr();
982 if (!is_var(c) && cache.get(to_idx(c), nullptr) == nullptr) {
983 todo.push_back(c);
984 ok = false;
985 }
986 }
987 if (!ok)
988 continue;
989 expr * args[2];
990 for (unsigned i = 0; i < 2; i++) {
991 aig_lit l = t->m_children[i];
992 aig * c = l.ptr();
993 if (is_var(c))
994 args[i] = m.m_var2exprs.get(c->m_id);
995 else
996 args[i] = cache.get(to_idx(c), nullptr);
997 if (!l.is_inverted())
998 args[i] = invert(args[i]);
999 }
1000 cache.set(idx, ast_mng.mk_not(ast_mng.mk_or(args[0], args[1])));
1001 todo.pop_back();
1002 }
1003 aig * c = l.ptr();
1004 if (is_var(c))
1005 r = m.m_var2exprs.get(c->m_id);
1006 else
1007 r = cache.get(to_idx(c));
1008 if (l.is_inverted())
1009 r = invert(r);
1010 }
1011
operator ()aig_manager::imp::aig2expr1012 void operator()(aig_lit const & l, expr_ref & r) {
1013 naive(l, r);
1014 }
1015
operator ()aig_manager::imp::aig2expr1016 void operator()(aig_lit const & l, goal & g) {
1017 g.reset();
1018 sbuffer<aig_lit> roots;
1019 roots.push_back(l);
1020 while (!roots.empty()) {
1021 aig_lit n = roots.back();
1022 roots.pop_back();
1023 if (n.is_inverted()) {
1024 g.assert_expr(invert(process_root(n.ptr())), nullptr, nullptr);
1025 continue;
1026 }
1027 aig * p = n.ptr();
1028 if (m.is_ite(p)) {
1029 g.assert_expr(process_root(p), nullptr, nullptr);
1030 continue;
1031 }
1032 if (is_var(p)) {
1033 g.assert_expr(m.var2expr(p), nullptr, nullptr);
1034 continue;
1035 }
1036 roots.push_back(left(p));
1037 roots.push_back(right(p));
1038 }
1039 }
1040
1041 };
1042
1043 struct max_sharing_proc {
1044 struct frame {
1045 aig * m_node;
1046 unsigned short m_idx;
frameaig_manager::imp::max_sharing_proc::frame1047 frame(aig * n):m_node(n), m_idx(0) {}
1048 };
1049 imp & m;
1050 svector<frame> m_frame_stack;
1051 svector<aig_lit> m_result_stack;
1052 svector<aig_lit> m_cache;
1053 ptr_vector<aig> m_saved;
1054
max_sharing_procaig_manager::imp::max_sharing_proc1055 max_sharing_proc(imp & _m):m(_m) {}
1056
~max_sharing_procaig_manager::imp::max_sharing_proc1057 ~max_sharing_proc() {
1058 reset_saved();
1059 }
1060
reset_savedaig_manager::imp::max_sharing_proc1061 void reset_saved() {
1062 m.dec_array_ref(m_saved.size(), m_saved.data());
1063 m_saved.finalize();
1064 }
1065
reset_cacheaig_manager::imp::max_sharing_proc1066 void reset_cache() {
1067 m_cache.finalize();
1068 reset_saved();
1069 }
1070
push_resultaig_manager::imp::max_sharing_proc1071 void push_result(aig_lit n) {
1072 m_result_stack.push_back(n);
1073 if (!n.is_null())
1074 m.inc_ref(n);
1075 }
1076
is_cachedaig_manager::imp::max_sharing_proc1077 bool is_cached(aig * p) {
1078 SASSERT(!is_var(p));
1079 if (p->m_ref_count <= 1)
1080 return false;
1081 unsigned idx = to_idx(p);
1082 if (idx >= m_cache.size()) {
1083 m_cache.resize(idx+1, aig_lit::null);
1084 return false;
1085 }
1086 aig_lit c = m_cache[idx];
1087 if (!c.is_null()) {
1088 push_result(c);
1089 return true;
1090 }
1091 return false;
1092 }
1093
visitaig_manager::imp::max_sharing_proc1094 bool visit(aig * p) {
1095 if (is_var(p)) {
1096 push_result(nullptr);
1097 return true;
1098 }
1099 if (is_cached(p))
1100 return true;
1101 m_frame_stack.push_back(frame(p));
1102 return false;
1103 }
1104
visitaig_manager::imp::max_sharing_proc1105 bool visit(aig_lit l) { return visit(l.ptr()); }
1106
save_resultaig_manager::imp::max_sharing_proc1107 void save_result(aig * o, aig_lit n) {
1108 SASSERT(!is_var(o));
1109 if (o->m_ref_count > 1) {
1110 unsigned idx = to_idx(o);
1111 if (idx >= m_cache.size())
1112 m_cache.resize(idx+1, aig_lit::null);
1113 m_cache[idx] = n;
1114 m_saved.push_back(o);
1115 m_saved.push_back(n.ptr());
1116 m.inc_ref(o);
1117 m.inc_ref(n);
1118 }
1119 if (o != n.ptr()) {
1120 push_result(n);
1121 }
1122 else {
1123 SASSERT(!n.is_inverted());
1124 push_result(aig_lit::null);
1125 }
1126 }
1127
pop2_resultaig_manager::imp::max_sharing_proc1128 void pop2_result() {
1129 aig_lit r1 = m_result_stack.back();
1130 m_result_stack.pop_back();
1131 aig_lit r2 = m_result_stack.back();
1132 m_result_stack.pop_back();
1133 if (!r1.is_null()) m.dec_ref(r1);
1134 if (!r2.is_null()) m.dec_ref(r2);
1135 }
1136
improve_sharing_leftaig_manager::imp::max_sharing_proc1137 bool improve_sharing_left(aig * o, aig_lit n) {
1138 SASSERT(!left(n).is_inverted());
1139 SASSERT(!is_var(left(n)));
1140 aig_lit a = left(left(n));
1141 aig_lit b = right(left(n));
1142 aig_lit c = right(n);
1143 TRACE("max_sharing",
1144 tout << "trying (and "; m.display_ref(tout, a);
1145 tout << " (and "; m.display_ref(tout, b);
1146 tout << " "; m.display_ref(tout, c);
1147 tout << "))\n";);
1148 aig_lit bc = m.mk_and(b, c);
1149 m.inc_ref(bc);
1150 if (ref_count(bc) > 1) {
1151 aig_lit r = m.mk_and(a, bc);
1152 if (n.is_inverted())
1153 r.invert();
1154 save_result(o, r);
1155 m.dec_ref(bc);
1156 TRACE("max_sharing", tout << "improved:\n"; m.display(tout, o); tout << "---->\n"; m.display(tout, r););
1157 return true;
1158 }
1159 m.dec_ref(bc);
1160
1161 TRACE("max_sharing",
1162 tout << "trying (and "; m.display_ref(tout, a);
1163 tout << " (and "; m.display_ref(tout, c);
1164 tout << " "; m.display_ref(tout, b);
1165 tout << "))\n";);
1166 aig_lit ac = m.mk_and(a, c);
1167 m.inc_ref(ac);
1168 if (ref_count(ac) > 1) {
1169 aig_lit r = m.mk_and(b, ac);
1170 if (n.is_inverted())
1171 r.invert();
1172 save_result(o, r);
1173 m.dec_ref(ac);
1174 TRACE("max_sharing", tout << "improved:\n"; m.display(tout, o); tout << "---->\n"; m.display(tout, r););
1175 return true;
1176 }
1177 m.dec_ref(ac);
1178
1179 return false;
1180 }
1181
improve_sharing_rightaig_manager::imp::max_sharing_proc1182 bool improve_sharing_right(aig * o, aig_lit n) {
1183 SASSERT(!right(n).is_inverted());
1184 SASSERT(!is_var(right(n)));
1185 aig_lit a = left(n);
1186 aig_lit b = left(right(n));
1187 aig_lit c = right(right(n));
1188 TRACE("max_sharing",
1189 tout << "trying (and (and "; m.display_ref(tout, a);
1190 tout << " "; m.display_ref(tout, b);
1191 tout << ") "; m.display_ref(tout, c);
1192 tout << ")\n";);
1193 aig_lit ab = m.mk_and(a, b);
1194 m.inc_ref(ab);
1195 if (ref_count(ab) > 1) {
1196 aig_lit r = m.mk_and(ab, c);
1197 if (n.is_inverted())
1198 r.invert();
1199 save_result(o, r);
1200 m.dec_ref(ab);
1201 TRACE("max_sharing", tout << "improved:\n"; m.display(tout, o); tout << "---->\n"; m.display(tout, r););
1202 return true;
1203 }
1204 m.dec_ref(ab);
1205
1206 aig_lit ac = m.mk_and(a, c);
1207 TRACE("max_sharing",
1208 tout << "trying (and (and "; m.display_ref(tout, a);
1209 tout << " "; m.display_ref(tout, c);
1210 tout << ") "; m.display_ref(tout, b);
1211 tout << ")\n";);
1212 m.inc_ref(ac);
1213 if (ref_count(ac) > 1) {
1214 aig_lit r = m.mk_and(ac, b);
1215 if (n.is_inverted())
1216 r.invert();
1217 save_result(o, r);
1218 m.dec_ref(ac);
1219 TRACE("max_sharing", tout << "improved:\n"; m.display(tout, o); tout << "---->\n"; m.display(tout, r););
1220 return true;
1221 }
1222 m.dec_ref(ac);
1223 return false;
1224 }
1225
improve_sharing_coreaig_manager::imp::max_sharing_proc1226 void improve_sharing_core(aig * o, aig_lit n) {
1227 if (!is_var(n)) {
1228 aig_lit l = left(n);
1229 if (!l.is_inverted() && ref_count(l) == 1 && !is_var(l) && improve_sharing_left(o, n))
1230 return;
1231 aig_lit r = right(n);
1232 if (!r.is_inverted() && ref_count(r) == 1 && !is_var(r) && improve_sharing_right(o, n))
1233 return;
1234 }
1235 save_result(o, n);
1236 }
1237
improve_sharingaig_manager::imp::max_sharing_proc1238 void improve_sharing(aig * p) {
1239 unsigned sz = m_result_stack.size();
1240 aig_lit new_l = m_result_stack[sz-2];
1241 aig_lit new_r = m_result_stack[sz-1];
1242 if (new_l.is_null() && new_r.is_null()) {
1243 pop2_result();
1244 improve_sharing_core(p, aig_lit(p));
1245 return;
1246 }
1247 aig_lit l = left(p);
1248 aig_lit r = right(p);
1249 if (!new_l.is_null()) {
1250 if (l.is_inverted())
1251 new_l.invert();
1252 l = new_l;
1253 }
1254 if (!new_r.is_null()) {
1255 if (r.is_inverted())
1256 new_r.invert();
1257 r = new_r;
1258 }
1259 aig_lit n = m.mk_and(l, r);
1260 m.inc_ref(n);
1261 pop2_result();
1262 improve_sharing_core(p, n);
1263 m.dec_ref(n);
1264 }
1265
processaig_manager::imp::max_sharing_proc1266 void process(aig * p) {
1267 if (visit(p))
1268 return;
1269 while (!m_frame_stack.empty()) {
1270 start:
1271 frame & fr = m_frame_stack.back();
1272 aig * n = fr.m_node;
1273 TRACE("max_sharing", tout << "processing "; m.display_ref(tout, n); tout << " idx: " << fr.m_idx << "\n";);
1274 switch (fr.m_idx) {
1275 case 0:
1276 fr.m_idx++;
1277 if (!visit(left(n)))
1278 goto start;
1279 case 1:
1280 fr.m_idx++;
1281 if (!visit(right(n)))
1282 goto start;
1283 default:
1284 if (!is_cached(n))
1285 improve_sharing(n);
1286 m_frame_stack.pop_back();
1287 break;
1288 }
1289 }
1290 }
1291
operator ()aig_manager::imp::max_sharing_proc1292 aig_lit operator()(aig_lit p) {
1293 process(p.ptr());
1294 SASSERT(m_result_stack.size() == 1);
1295 aig_lit r = m_result_stack.back();
1296 TRACE("max_sharing", tout << "r.is_null(): " << r.is_null() << "\n";);
1297 SASSERT(r.is_null() || ref_count(r) >= 1);
1298 reset_cache();
1299 if (r.is_null()) {
1300 r = p;
1301 m.inc_ref(r);
1302 }
1303 else if (p.is_inverted()) {
1304 r.invert();
1305 }
1306 m_result_stack.pop_back();
1307 TRACE("max_sharing", tout << "result:\n"; m.display(tout, r););
1308 m.dec_ref_result(r);
1309 return r;
1310 }
1311 };
1312
1313 public:
impaig_manager::imp1314 imp(ast_manager & m, unsigned long long max_memory, bool default_gate_encoding):
1315 m_var_id_gen(0),
1316 m_node_id_gen(FIRST_NODE_ID),
1317 m_num_aigs(0),
1318 m_var2exprs(m),
1319 m_allocator("aig"),
1320 m_true(mk_var(m.mk_true())) {
1321 SASSERT(is_true(m_true));
1322 m_false = m_true;
1323 m_false.invert();
1324 inc_ref(m_true);
1325 inc_ref(m_false);
1326 m_max_memory = max_memory;
1327 m_default_gate_encoding = default_gate_encoding;
1328 }
1329
~impaig_manager::imp1330 ~imp() {
1331 dec_ref(m_true);
1332 dec_ref(m_false);
1333 SASSERT(m_num_aigs == 0);
1334 }
1335
maig_manager::imp1336 ast_manager & m() const { return m_var2exprs.get_manager(); }
1337
1338
inc_refaig_manager::imp1339 void inc_ref(aig * n) { n->m_ref_count++; }
inc_refaig_manager::imp1340 void inc_ref(aig_lit const & r) { inc_ref(r.ptr()); }
dec_refaig_manager::imp1341 void dec_ref(aig * n) {
1342 dec_ref_core(n);
1343 process_to_delete();
1344 }
dec_refaig_manager::imp1345 void dec_ref(aig_lit const & r) { dec_ref(r.ptr()); }
1346
dec_array_refaig_manager::imp1347 void dec_array_ref(unsigned sz, aig * const * ns) {
1348 for (unsigned i = 0; i < sz; i++)
1349 if (ns[i])
1350 dec_ref(ns[i]);
1351 }
1352
mk_andaig_manager::imp1353 aig_lit mk_and(aig_lit r1, aig_lit r2) {
1354 aig_lit r = mk_node(r1, r2);
1355 TRACE("mk_and_bug",
1356 display(tout, r1);
1357 tout << "AND\n";
1358 display(tout, r2);
1359 tout << "-->\n";
1360 display(tout, r);
1361 tout << "\n";);
1362 return r;
1363 }
1364
mk_andaig_manager::imp1365 aig_lit mk_and(unsigned num, aig_lit * args) {
1366 switch (num) {
1367 case 0:
1368 return m_true;
1369 case 1:
1370 return args[0];
1371 case 2:
1372 return mk_and(args[0], args[1]);
1373 default:
1374 // No need to use stable_sort, aig_lit_lt is a total order on AIG nodes
1375 std::sort(args, args+num, aig_lit_lt());
1376 aig_lit r = mk_and(args[0], args[1]);
1377 inc_ref(r);
1378 for (unsigned i = 2; i < num; i++) {
1379 aig_lit new_r = mk_and(r, args[i]);
1380 inc_ref(new_r);
1381 dec_ref(r);
1382 r = new_r;
1383 }
1384 dec_ref_result(r);
1385 return r;
1386 }
1387 }
1388
mk_oraig_manager::imp1389 aig_lit mk_or(aig_lit r1, aig_lit r2) {
1390 r1.invert();
1391 r2.invert();
1392 aig_lit r = mk_and(r1, r2);
1393 r.invert();
1394 return r;
1395 }
1396
mk_oraig_manager::imp1397 aig_lit mk_or(unsigned num, aig_lit * args) {
1398 switch (num) {
1399 case 0:
1400 return m_false;
1401 case 1:
1402 return args[0];
1403 case 2:
1404 return mk_or(args[0], args[1]);
1405 default:
1406 std::sort(args, args+num, aig_lit_lt());
1407 aig_lit r = mk_or(args[0], args[1]);
1408 inc_ref(r);
1409 for (unsigned i = 2; i < num; i++) {
1410 aig_lit new_r = mk_or(r, args[i]);
1411 inc_ref(new_r);
1412 dec_ref(r);
1413 r = new_r;
1414 }
1415 dec_ref_result(r);
1416 return r;
1417 }
1418 }
1419
mk_iteaig_manager::imp1420 aig_lit mk_ite(aig_lit c, aig_lit t, aig_lit e) {
1421 if (m_default_gate_encoding) {
1422 t.invert();
1423 aig_lit n1 = mk_and(c, t); // c and (not t)
1424 c.invert();
1425 e.invert();
1426 aig_lit n2 = mk_and(c, e); // (not c) and (not e)
1427 inc_ref(n1);
1428 inc_ref(n2);
1429 n1.invert();
1430 n2.invert();
1431 aig_lit r = mk_and(n1, n2);
1432 inc_ref(r);
1433 dec_ref(n1);
1434 dec_ref(n2);
1435 dec_ref_result(r);
1436 return r;
1437 }
1438 else {
1439 aig_lit n1 = mk_and(c, t);
1440 inc_ref(n1);
1441 c.invert();
1442 aig_lit n2 = mk_and(c, e);
1443 inc_ref(n2);
1444 n1.invert();
1445 n2.invert();
1446 aig_lit r = mk_and(n1, n2);
1447 r.invert();
1448 inc_ref(r);
1449 dec_ref(n1);
1450 dec_ref(n2);
1451 dec_ref_result(r);
1452 return r;
1453 }
1454 }
1455
mk_iffaig_manager::imp1456 aig_lit mk_iff(aig_lit lhs, aig_lit rhs) {
1457 if (m_default_gate_encoding) {
1458 rhs.invert();
1459 aig_lit n1 = mk_and(lhs, rhs); // lhs and (not rhs)
1460 lhs.invert();
1461 rhs.invert();
1462 aig_lit n2 = mk_and(lhs, rhs); // (not lhs) and rhs
1463 inc_ref(n1);
1464 inc_ref(n2);
1465 n1.invert();
1466 n2.invert();
1467 aig_lit r = mk_and(n1, n2);
1468 inc_ref(r);
1469 dec_ref(n1);
1470 dec_ref(n2);
1471 dec_ref_result(r);
1472 return r;
1473 }
1474 else {
1475 aig_lit n1 = mk_and(lhs, rhs); // lhs and rhs
1476 inc_ref(n1);
1477 lhs.invert();
1478 rhs.invert();
1479 aig_lit n2 = mk_and(lhs, rhs); // not lhs and not rhs
1480 inc_ref(n2);
1481 n1.invert();
1482 n2.invert();
1483 aig_lit r = mk_and(n1, n2);
1484 r.invert();
1485 inc_ref(r);
1486 dec_ref(n1);
1487 dec_ref(n2);
1488 dec_ref_result(r);
1489 return r;
1490 }
1491 }
1492
mk_xoraig_manager::imp1493 aig_lit mk_xor(aig_lit lhs, aig_lit rhs) {
1494 lhs.invert();
1495 return mk_iff(lhs, rhs);
1496 }
1497
mk_impliesaig_manager::imp1498 aig_lit mk_implies(aig_lit lhs, aig_lit rhs) {
1499 lhs.invert();
1500 return mk_or(lhs, rhs);
1501 }
1502
mk_aigaig_manager::imp1503 aig_lit mk_aig(expr * t) {
1504 aig_lit r;
1505 {
1506 expr2aig proc(*this);
1507 r = proc(t);
1508 inc_ref(r);
1509 }
1510 dec_ref_result(r);
1511 return r;
1512 }
1513
1514 template<typename S>
mk_aigaig_manager::imp1515 aig_lit mk_aig(S const & s) {
1516 aig_lit r;
1517 r = m_true;
1518 inc_ref(r);
1519 try {
1520 expr2aig proc(*this);
1521 unsigned sz = s.size();
1522 for (unsigned i = 0; i < sz; i++) {
1523 SASSERT(ref_count(r) >= 1);
1524 expr * t = s.form(i);
1525 aig_lit n = proc(t);
1526 inc_ref(n);
1527 aig_lit new_r = mk_and(r, n);
1528 SASSERT(proc.check_cache());
1529 inc_ref(new_r);
1530 dec_ref(r);
1531 dec_ref(n);
1532 SASSERT(proc.check_cache());
1533 r = new_r;
1534 }
1535 SASSERT(ref_count(r) >= 1);
1536 }
1537 catch (const aig_exception & ex) {
1538 dec_ref(r);
1539 throw ex;
1540 }
1541 dec_ref_result(r);
1542 return r;
1543 }
1544
to_formulaaig_manager::imp1545 void to_formula(aig_lit const & r, goal & g) {
1546 aig2expr proc(*this);
1547 proc(r, g);
1548 }
1549
to_formulaaig_manager::imp1550 void to_formula(aig_lit const & r, expr_ref & result) {
1551 aig2expr proc(*this);
1552 proc(r, result);
1553 }
1554
max_sharingaig_manager::imp1555 aig_lit max_sharing(aig_lit l) {
1556 max_sharing_proc p(*this);
1557 return p(l);
1558 }
1559
display_refaig_manager::imp1560 void display_ref(std::ostream & out, aig * r) const {
1561 if (is_var(r))
1562 out << "#" << r->m_id;
1563 else
1564 out << "@" << (r->m_id - FIRST_NODE_ID);
1565 }
1566
display_refaig_manager::imp1567 void display_ref(std::ostream & out, aig_lit const & r) const {
1568 if (r.is_inverted())
1569 out << "-";
1570 display_ref(out, r.ptr());
1571 }
1572
displayaig_manager::imp1573 void display(std::ostream & out, aig_lit const & r) const {
1574 display_ref(out, r);
1575 out << "\n";
1576 ptr_vector<aig> queue;
1577 unsigned qhead = 0;
1578 queue.push_back(r.ptr());
1579 while (qhead < queue.size()) {
1580 aig * n = queue[qhead];
1581 qhead++;
1582 display_ref(out, n); out << ": ";
1583 if (is_var(n)) {
1584 out << mk_ismt2_pp(m_var2exprs[n->m_id], m()) << "\n";
1585 }
1586 else {
1587 display_ref(out, n->m_children[0]);
1588 out << " ";
1589 display_ref(out, n->m_children[1]);
1590 out << "\n";
1591 aig * c1 = n->m_children[0].ptr();
1592 aig * c2 = n->m_children[1].ptr();
1593 if (!c1->m_mark) {
1594 c1->m_mark = true;
1595 queue.push_back(c1);
1596 }
1597 if (!c2->m_mark) {
1598 c2->m_mark = true;
1599 queue.push_back(c2);
1600 }
1601 }
1602 }
1603 unmark(queue.size(), queue.data());
1604 }
1605
display_smt2_refaig_manager::imp1606 void display_smt2_ref(std::ostream & out, aig_lit const & r) const {
1607 if (r.is_inverted())
1608 out << "(not ";
1609 if (is_var(r)) {
1610 out << mk_ismt2_pp(var2expr(r.ptr()), m());
1611 }
1612 else {
1613 out << "aig" << to_idx(r.ptr());
1614 }
1615 if (r.is_inverted())
1616 out << ")";
1617 }
1618
display_smt2aig_manager::imp1619 void display_smt2(std::ostream & out, aig_lit const & r) const {
1620 ptr_vector<aig> to_unmark;
1621 ptr_vector<aig> todo;
1622 todo.push_back(r.ptr());
1623 while (!todo.empty()) {
1624 aig * t = todo.back();
1625 if (t->m_mark) {
1626 todo.pop_back();
1627 continue;
1628 }
1629 if (is_var(t)) {
1630 to_unmark.push_back(t);
1631 t->m_mark = true;
1632 todo.pop_back();
1633 continue;
1634 }
1635 bool visited = true;
1636 for (unsigned i = 0; i < 2; i++) {
1637 aig_lit c = t->m_children[i];
1638 aig * data = c.ptr();
1639 if (!data->m_mark) {
1640 todo.push_back(data);
1641 visited = false;
1642 }
1643 }
1644 if (!visited)
1645 continue;
1646 to_unmark.push_back(t);
1647 t->m_mark = true;
1648 out << "(define-fun aig" << to_idx(t) << " () Bool (and";
1649 for (unsigned i = 0; i < 2; i++) {
1650 out << " ";
1651 display_smt2_ref(out, t->m_children[i]);
1652 }
1653 out << "))\n";
1654 todo.pop_back();
1655 }
1656 out << "(assert ";
1657 display_smt2_ref(out, r);
1658 out << ")\n";
1659 unmark(to_unmark.size(), to_unmark.data());
1660 }
1661
get_num_aigsaig_manager::imp1662 unsigned get_num_aigs() const {
1663 return m_num_aigs;
1664 }
1665 };
1666
1667
aig_ref()1668 aig_ref::aig_ref():
1669 m_manager(nullptr),
1670 m_ref(nullptr) {
1671 }
1672
aig_ref(aig_manager & m,aig_lit const & l)1673 aig_ref::aig_ref(aig_manager & m, aig_lit const & l):
1674 m_manager(&m),
1675 m_ref(l.m_ref) {
1676 m.m_imp->inc_ref(l);
1677 }
1678
~aig_ref()1679 aig_ref::~aig_ref() {
1680 if (m_ref != nullptr) {
1681 m_manager->m_imp->dec_ref(aig_lit(*this));
1682 }
1683 }
1684
operator =(aig_ref const & r)1685 aig_ref & aig_ref::operator=(aig_ref const & r) {
1686 if (r.m_ref != nullptr)
1687 r.m_manager->m_imp->inc_ref(aig_lit(r));
1688 if (m_ref != nullptr)
1689 m_manager->m_imp->dec_ref(aig_lit(*this));
1690 m_ref = r.m_ref;
1691 m_manager = r.m_manager;
1692 return *this;
1693 }
1694
aig_manager(ast_manager & m,unsigned long long max,bool default_gate_encoding)1695 aig_manager::aig_manager(ast_manager & m, unsigned long long max, bool default_gate_encoding) {
1696 m_imp = alloc(imp, m, max, default_gate_encoding);
1697 }
1698
~aig_manager()1699 aig_manager::~aig_manager() {
1700 dealloc(m_imp);
1701 }
1702
set_max_memory(unsigned long long max)1703 void aig_manager::set_max_memory(unsigned long long max) {
1704 m_imp->m_max_memory = max;
1705 }
1706
mk_aig(expr * n)1707 aig_ref aig_manager::mk_aig(expr * n) {
1708 return aig_ref(*this, m_imp->mk_aig(n));
1709 }
1710
mk_aig(goal const & s)1711 aig_ref aig_manager::mk_aig(goal const & s) {
1712 return aig_ref(*this, m_imp->mk_aig(s));
1713 }
1714
mk_not(aig_ref const & r)1715 aig_ref aig_manager::mk_not(aig_ref const & r) {
1716 aig_lit l(r);
1717 l.invert();
1718 return aig_ref(*this, l);
1719 }
1720
mk_and(aig_ref const & r1,aig_ref const & r2)1721 aig_ref aig_manager::mk_and(aig_ref const & r1, aig_ref const & r2) {
1722 return aig_ref(*this, m_imp->mk_and(aig_lit(r1), aig_lit(r2)));
1723 }
1724
mk_or(aig_ref const & r1,aig_ref const & r2)1725 aig_ref aig_manager::mk_or(aig_ref const & r1, aig_ref const & r2) {
1726 return aig_ref(*this, m_imp->mk_or(aig_lit(r1), aig_lit(r2)));
1727 }
1728
mk_iff(aig_ref const & r1,aig_ref const & r2)1729 aig_ref aig_manager::mk_iff(aig_ref const & r1, aig_ref const & r2) {
1730 return aig_ref(*this, m_imp->mk_iff(aig_lit(r1), aig_lit(r2)));
1731 }
1732
mk_ite(aig_ref const & r1,aig_ref const & r2,aig_ref const & r3)1733 aig_ref aig_manager::mk_ite(aig_ref const & r1, aig_ref const & r2, aig_ref const & r3) {
1734 return aig_ref(*this, m_imp->mk_ite(aig_lit(r1), aig_lit(r2), aig_lit(r3)));
1735 }
1736
max_sharing(aig_ref & r)1737 void aig_manager::max_sharing(aig_ref & r) {
1738 r = aig_ref(*this, m_imp->max_sharing(aig_lit(r)));
1739 }
1740
to_formula(aig_ref const & r,goal & g)1741 void aig_manager::to_formula(aig_ref const & r, goal & g) {
1742 SASSERT(!g.proofs_enabled());
1743 SASSERT(!g.unsat_core_enabled());
1744 return m_imp->to_formula(aig_lit(r), g);
1745 }
1746
to_formula(aig_ref const & r,expr_ref & res)1747 void aig_manager::to_formula(aig_ref const & r, expr_ref & res) {
1748 return m_imp->to_formula(aig_lit(r), res);
1749 }
1750
display(std::ostream & out,aig_ref const & r) const1751 void aig_manager::display(std::ostream & out, aig_ref const & r) const {
1752 m_imp->display(out, aig_lit(r));
1753 }
1754
display_smt2(std::ostream & out,aig_ref const & r) const1755 void aig_manager::display_smt2(std::ostream & out, aig_ref const & r) const {
1756 m_imp->display_smt2(out, aig_lit(r));
1757 }
1758
get_num_aigs() const1759 unsigned aig_manager::get_num_aigs() const {
1760 return m_imp->get_num_aigs();
1761 }
1762
1763
1764
1765