source: vis_dev/vis-2.3/src/puresat/puresatAig.c

Last change on this file was 14, checked in by cecile, 15 years ago

vis2.3
File size: 24.4 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3 FileName [puresatAig.c]
4
5 PackageName [puresat]
6
7 Synopsis [Abstraction refinement for large scale invariant checking.]
8
9 Description [This file contains the functions to check invariant properties
10 by the PureSAT abstraction refinement algorithm, which is entirely based on
11 SAT solver, the input of which could be either CNF or AIG. It has several
12 parts:
13
14 * Localization-reduction base Abstraction
15 * K-induction or interpolation to prove the truth of a property
16 * Bounded Model Checking to find bugs
17 * Incremental concretization based methods to verify abstract bugs
18 * Incremental SAT solver to improve efficiency
19 * UNSAT proof based method to obtain refinement
20 * AROSAT to bring in only necessary latches into unsat proofs
21 * Bridge abstraction to get compact coarse refinement
22 * Refinement minization to guarrantee minimal refinements
23 * Unsat proof-based refinement minimization to eliminate multiple candidate
24 by on SAT test
25 * Refinement prediction to decrease the number of refinement iterations
26 * Dynamic switching to redistribute computional resources to improve
27 efficiency
28
29 For more information, please check the BMC'03, ICCAD'04, STTT'05 and TACAS'05
30 paper of Li et al., "A satisfiability-based appraoch to abstraction
31 refinement in model checking", " Abstraction in symbolic model checking
32 using satisfiability as the only decision procedure", "Efficient computation
33 of small abstraction refinements", and "Efficient abstraction refinement in
34 interpolation-based unbounded model checking"]
35
36 Author [Bing Li]
37
38 Copyright [Copyright (c) 2004 The Regents of the Univ. of Colorado.
39 All rights reserved.
40
41 Permission is hereby granted, without written agreement and without
42 license or royalty fees, to use, copy, modify, and distribute this
43 software and its documentation for any purpose, provided that the
44 above copyright notice and the following two paragraphs appear in
45 all copies of this software.]
46
47******************************************************************************/
48#include "maigInt.h"
49#include "baig.h"
50#include "ntk.h"
51#include "puresatInt.h"
52/*---------------------------------------------------------------------------*/
53/* Constant declarations */
54/*---------------------------------------------------------------------------*/
55
56/*---------------------------------------------------------------------------*/
57/* Type declarations */
58/*---------------------------------------------------------------------------*/
59
60
61/*---------------------------------------------------------------------------*/
62/* Structure declarations */
63/*---------------------------------------------------------------------------*/
64
65
66/*---------------------------------------------------------------------------*/
67/* Variable declarations */
68/*---------------------------------------------------------------------------*/
69
70/*---------------------------------------------------------------------------*/
71/* Macro declarations */
72/*---------------------------------------------------------------------------*/
73
74/**AutomaticStart*************************************************************/
75
76/*---------------------------------------------------------------------------*/
77/* Static function prototypes */
78/*---------------------------------------------------------------------------*/
79
80
81/**AutomaticEnd***************************************************************/
82
83/*---------------------------------------------------------------------------*/
84/* Definition of exported functions */
85/*---------------------------------------------------------------------------*/
86
87
88/*---------------------------------------------------------------------------*/
89/* Definition of internal functions */
90/*---------------------------------------------------------------------------*/
91
92/**Function********************************************************************
93
94 Synopsis [For AIG recovery--unconnect output for nodes eliminated]
95
96 Description [For AIG recovery--unconnect output for nodes eliminated]
97
98 SideEffects []
99
100 SeeAlso []
101
102******************************************************************************/
103
104void
105PureSat_unconnectOutput(
106 bAig_Manager_t *manager,
107 bAigEdge_t from,
108 bAigEdge_t to)
109{
110 bAigEdge_t cur, *pfan, *newfan;
111 int i, nfan,find=0;
112
113 from = bAig_NonInvertedEdge(from);
114 to = bAig_NonInvertedEdge(to);
115
116 pfan = (bAigEdge_t *)fanout(from);
117 nfan = nFanout(from);
118 newfan = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*(nfan));
119 for(i=0; i<nfan; i++) {
120 cur = pfan[i];
121 cur = cur >> 1;
122 cur = bAig_NonInvertedEdge(cur);
123 if(cur == to) {
124 find = 1;
125 memcpy(newfan, pfan, sizeof(bAigEdge_t)*i);
126 memcpy(&(newfan[i]), &(pfan[i+1]), sizeof(bAigEdge_t)*(nfan-i-1));
127 newfan[nfan-1] = 0;
128
129 fanout(from) = (bAigEdge_t)newfan;
130
131
132 free(pfan);
133 nFanout(from) = nfan-1;
134 break;
135 }
136 }
137 assert(find);
138}
139
140
141/**Function********************************************************************
142
143 Synopsis [for AIG generation---create connection between new and
144 old aig nodes]
145
146 Description []
147
148 SideEffects []
149
150 SeeAlso []
151
152******************************************************************************/
153
154void
155PureSat_connectOutput(
156 bAig_Manager_t *manager,
157 bAigEdge_t from,
158 bAigEdge_t to,
159 int inputIndex)
160{
161 bAigEdge_t *pfan;
162 bAigEdge_t nfan;
163
164 to = bAig_NonInvertedEdge(to);
165 pfan = (bAigEdge_t *)fanout(from);
166 nfan = nFanout(from);
167 if(nfan == 0) pfan = malloc((sizeof(bAigEdge_t)*2));
168 else pfan = realloc(pfan, sizeof(bAigEdge_t)*(nfan+2));
169 to += bAig_IsInverted(from);
170 to = to << 1;
171 to += inputIndex;
172 pfan[nfan++] = to;
173 pfan[nfan] = 0;
174 fanout(from) = (bAigEdge_t)pfan;
175 nFanout(from) = nfan;
176}
177
178
179/**Function********************************************************************
180
181 Synopsis [Check whether a node has been created or not]
182
183 Description []
184
185 SideEffects []
186
187 SeeAlso []
188
189******************************************************************************/
190
191bAigEdge_t
192PureSat_HashTableLookup(
193 bAig_Manager_t *manager,
194 bAigEdge_t node1,
195 bAigEdge_t node2)
196{
197 bAigEdge_t key = HashTableFunction(node1, node2);
198 bAigEdge_t node;
199
200 node = manager->HashTableArray[manager->class_][key];
201 if (node == bAig_NULL) {
202 return bAig_NULL;
203 }
204 else{
205 while ( (rightChild(bAig_NonInvertedEdge(node)) != node2) ||
206 (leftChild(bAig_NonInvertedEdge(node)) != node1)) {
207
208 if (next(bAig_NonInvertedEdge(node)) == bAig_NULL){
209 return(bAig_NULL);
210 }
211 node = next(bAig_NonInvertedEdge(node)); /* Get the next Node */
212 } /* While loop */
213 return(node);
214
215 } /* If Then Else */
216
217} /* End of HashTableLookup() */
218
219
220/**Function********************************************************************
221
222 Synopsis [Add one new node to hash table]
223
224 Description []
225
226 SideEffects []
227
228 SeeAlso []
229
230******************************************************************************/
231
232int
233PureSat_HashTableAdd(
234 bAig_Manager_t *manager,
235 bAigEdge_t nodeIndexParent,
236 bAigEdge_t nodeIndex1,
237 bAigEdge_t nodeIndex2)
238{
239 bAigEdge_t key = HashTableFunction(nodeIndex1, nodeIndex2);
240 bAigEdge_t nodeIndex;
241 bAigEdge_t node;
242
243 nodeIndex = manager->HashTableArray[manager->class_][key];
244 if (nodeIndex == bAig_NULL) {
245 manager->HashTableArray[manager->class_][key] = nodeIndexParent;
246 return TRUE;
247 }
248 else{
249 node = nodeIndex;
250 nodeIndex = next(bAig_NonInvertedEdge(nodeIndex)); /* Get the Node */
251 while (nodeIndex != bAig_NULL) {
252 node = nodeIndex;
253 nodeIndex = next(bAig_NonInvertedEdge(nodeIndex));
254 }
255 next(bAig_NonInvertedEdge(node)) = nodeIndexParent;
256 return TRUE;
257 }
258
259}
260
261
262
263/**Function********************************************************************
264
265 Synopsis [Create a node for AND operation]
266
267 Description []
268
269 SideEffects []
270
271 SeeAlso []
272
273******************************************************************************/
274
275bAigEdge_t
276PureSat_CreateAndNode(
277 bAig_Manager_t *manager,
278 bAigEdge_t node1,
279 bAigEdge_t node2)
280{
281
282 bAigEdge_t varIndex;
283 char *name = NIL(char);
284 char *node1Str = util_inttostr(node1);
285 char *node2Str = util_inttostr(node2);
286 long class_ = manager->class_;
287
288 name = util_strcat4("Nd", node1Str,"_", node2Str);
289 while (st_lookup(manager->SymbolTableArray[class_], name, &varIndex)){
290 fprintf(vis_stdout, "Find redundant node at %ld %ld\n", node1, node2);
291 name = util_strcat3(name, node1Str, node2Str);
292 }
293 FREE(node1Str);
294 FREE(node2Str);
295 varIndex = bAig_CreateNode(manager, node1, node2);
296 if (varIndex == bAig_NULL){
297 FREE(name);
298 return (varIndex);
299 }
300 /* Insert the varaible in the Symbol Table */
301 st_insert(manager->SymbolTableArray[class_], name, (char*) (long) varIndex);
302 manager->nameList[bAigNodeID(varIndex)] = name;
303
304 return(varIndex);
305
306}
307
308
309/**Function********************************************************************
310
311 Synopsis [And function for 2 aig nodes]
312
313 Description []
314
315 SideEffects []
316
317 SeeAlso []
318
319******************************************************************************/
320
321bAigEdge_t
322PureSat_And2(
323 bAig_Manager_t *manager,
324 bAigEdge_t nodeIndex1,
325 bAigEdge_t nodeIndex2)
326{
327 bAigEdge_t newNodeIndex;
328
329 newNodeIndex = PureSat_CreateAndNode(manager, nodeIndex1, nodeIndex2) ;
330
331 PureSat_HashTableAdd(manager, newNodeIndex, nodeIndex1, nodeIndex2);
332 PureSat_connectOutput(manager, nodeIndex1, newNodeIndex, 0);
333 PureSat_connectOutput(manager, nodeIndex2, newNodeIndex, 1);
334
335 return newNodeIndex;
336
337}
338
339
340/**Function********************************************************************
341
342 Synopsis [And function for 3 aig nodes]
343
344 Description []
345
346 SideEffects []
347
348 SeeAlso []
349
350******************************************************************************/
351
352bAigEdge_t
353PureSat_And3(
354 bAig_Manager_t *manager,
355 bAigEdge_t l,
356 bAigEdge_t r)
357{
358 int caseIndex, caseSig;
359 bAigEdge_t rl, rr;
360
361 rl = leftChild(r);
362 rr = rightChild(r);
363
364 caseIndex = 0; /* (a)(b c) */
365 if(bAigCompareNode(l, rl)) {
366 caseIndex = 1; /* (a)(a b) */
367 }
368 else if(bAigCompareNode(l, rr)) {
369 caseIndex = 2; /* (a)(b a) */
370 }
371
372 caseSig = 0;
373 if(bAig_IsInverted(l)) caseSig += 8;
374 if(bAig_IsInverted(rl)) caseSig += 4;
375 if(bAig_IsInverted(rr)) caseSig += 2;
376 if(bAig_IsInverted(r)) caseSig += 1;
377 if(caseIndex == 0) {
378 return(PureSat_And2(manager, l, r));
379 }
380 else if(caseIndex == 1) {
381 switch(caseSig) {
382 case 2 :
383 case 0 :
384 case 14 :
385 case 12 :
386 return(r);
387 case 10 :
388 case 8 :
389 case 6 :
390 case 4 :
391 return(bAig_Zero);
392 case 3 :
393 case 1 :
394 case 15 :
395 case 13 :
396 return(PureSat_And(manager, rl, bAig_Not(rr)));
397 case 11 :
398 case 9 :
399 case 7 :
400 case 5 :
401 return(l);
402 }
403 }
404 else if(caseIndex == 2) {
405 switch(caseSig) {
406 case 4 :
407 case 0 :
408 case 14 :
409 case 10 :
410 return(r);
411 case 12 :
412 case 8 :
413 case 6 :
414 case 2 :
415 return(bAig_Zero);
416 case 5 :
417 case 1 :
418 case 15 :
419 case 11 :
420 return(PureSat_And(manager, bAig_Not(rl), rr));
421 case 13 :
422 case 9 :
423 case 7 :
424 case 3 :
425 return(l);
426 }
427 }
428 return(0);
429}
430
431
432/**Function********************************************************************
433
434 Synopsis [And function for 4 aig nodes]
435
436 Description []
437
438 SideEffects []
439
440 SeeAlso []
441
442******************************************************************************/
443
444bAigEdge_t
445PureSat_And4(
446 bAig_Manager_t *manager,
447 bAigEdge_t l,
448 bAigEdge_t r)
449{
450 int caseIndex, caseSig;
451 bAigEdge_t ll, lr, rl, rr;
452 bAigEdge_t t1, t2;
453
454 ll = leftChild(l);
455 lr = rightChild(l);
456 rl = leftChild(r);
457 rr = rightChild(r);
458
459 if(bAigCompareNode(l, rl) ||
460 bAigCompareNode(l, rr)) {
461 return(PureSat_And3(manager, l, r));
462 }
463 else if(bAigCompareNode(r, ll) ||
464 bAigCompareNode(r, lr)) {
465 return(PureSat_And3(manager, r, l));
466 }
467
468 if(ll > lr+1) bAigSwap(ll, lr);
469 if(rl > rr+1) bAigSwap(rl, rr);
470
471 caseIndex = 0; /* (a b)(c d) */
472 if(bAigCompareNode(ll, rl)) {
473 if(bAigCompareNode(lr, rr)) {
474 caseIndex = 4; /* (a b) (a b) */
475 }
476 else {
477 caseIndex = 1; /* (a b) (a c) */
478 if(lr > rr+1) {
479 bAigSwap(ll, rl);
480 bAigSwap(lr, rr);
481 bAigSwap(l, r);
482 }
483 }
484 }
485 else if(bAigCompareNode(lr, rl)) {
486 caseIndex = 2; /* (b a)(a c) */
487 }
488 else if(bAigCompareNode(lr, rr)) {
489 caseIndex = 3; /* (b a)(c a) */
490 if(ll > rl+1) {
491 bAigSwap(ll, rl);
492 bAigSwap(lr, rr);
493 bAigSwap(l, r);
494 }
495 }
496 else if(bAigCompareNode(ll, rr)) {
497 /* (a b)(c a) */
498 bAigSwap(ll, rl);
499 bAigSwap(lr, rr);
500 bAigSwap(l, r);
501 caseIndex = 2; /* (c a )(a b) because of c < b */
502 }
503
504 caseSig = 0;
505 if(bAig_IsInverted(ll)) caseSig += 32;
506 if(bAig_IsInverted(lr)) caseSig += 16;
507 if(bAig_IsInverted(l)) caseSig += 8;
508 if(bAig_IsInverted(rl)) caseSig += 4;
509 if(bAig_IsInverted(rr)) caseSig += 2;
510 if(bAig_IsInverted(r)) caseSig += 1;
511
512 if(caseIndex == 0) {
513 return(PureSat_And2(manager, l, r));
514 }
515 else if(caseIndex == 1) {
516 switch(caseSig) {
517 case 19 :
518 case 17 :
519 case 3 :
520 case 1 :
521 case 55 :
522 case 53 :
523 case 39 :
524 case 37 :
525 t1 = PureSat_And(manager, lr, bAig_Not(rr));
526 t2 = PureSat_And(manager, ll, t1);
527 return(t2);
528 case 18 :
529 case 16 :
530 case 2 :
531 case 0 :
532 case 54 :
533 case 52 :
534 case 38 :
535 case 36 :
536 t1 = PureSat_And(manager, lr, rr);
537 t2 = PureSat_And(manager, ll, t1);
538 return(t2);
539 case 26 :
540 case 24 :
541 case 10 :
542 case 8 :
543 case 62 :
544 case 60 :
545 case 46 :
546 case 44 :
547 t1 = PureSat_And(manager, bAig_Not(lr), rr);
548 t2 = PureSat_And(manager, ll, t1);
549 return(t2);
550 case 61 :
551 case 27 :
552 case 25 :
553 case 11 :
554 case 63 :
555 case 47 :
556 case 9 :
557 case 45 :
558 t1 = PureSat_And(manager, bAig_Not(lr), bAig_Not(rr));
559 t2 = PureSat_Or(manager, bAig_Not(ll), t1);
560 return(t2);
561 case 23 :
562 case 21 :
563 case 7 :
564 case 5 :
565 case 51 :
566 case 49 :
567 case 35 :
568 case 33 :
569 return(l);
570 case 30 :
571 case 28 :
572 case 14 :
573 case 12 :
574 case 58 :
575 case 56 :
576 case 42 :
577 case 40 :
578 return(r);
579 case 22 :
580 case 20 :
581 case 6 :
582 case 4 :
583 case 50 :
584 case 48 :
585 case 34 :
586 case 32 :
587 return(bAig_Zero);
588 case 31 :
589 case 29 :
590 case 15 :
591 case 13 :
592 case 59 :
593 case 57 :
594 case 43 :
595 case 41 :
596 t1 = PureSat_And2(manager, l, r);
597 return(t1);
598 }
599 }
600 else if(caseIndex == 2) {
601 switch(caseSig) {
602 case 35 :
603 case 33 :
604 case 3 :
605 case 1 :
606 case 55 :
607 case 53 :
608 case 23 :
609 case 21 :
610 t1 = PureSat_And(manager, lr, bAig_Not(rr));
611 t2 = PureSat_And(manager, ll, t1);
612 return(t2);
613 case 34 :
614 case 32 :
615 case 2 :
616 case 0 :
617 case 54 :
618 case 52 :
619 case 22 :
620 case 20 :
621 t1 = PureSat_And(manager, lr, rr);
622 t2 = PureSat_And(manager, ll, t1);
623 return(t2);
624 case 42 :
625 case 40 :
626 case 10 :
627 case 8 :
628 case 62 :
629 case 60 :
630 case 30 :
631 case 28 :
632 t1 = PureSat_And(manager, lr, rr);
633 t2 = PureSat_And(manager, bAig_Not(ll), t1);
634 return(t2);
635 case 43 :
636 case 41 :
637 case 11 :
638 case 9 :
639 case 63 :
640 case 61 :
641 case 31 :
642 case 29 :
643 t1 = PureSat_And(manager, bAig_Not(ll), bAig_Not(rr));
644 t2 = PureSat_Or(manager, bAig_Not(lr), t1);
645 return(t2);
646 case 39 :
647 case 37 :
648 case 7 :
649 case 5 :
650 case 51 :
651 case 49 :
652 case 19 :
653 case 17 :
654 return(l);
655 case 46 :
656 case 44 :
657 case 14 :
658 case 12 :
659 case 58 :
660 case 56 :
661 case 26 :
662 case 24 :
663 return(r);
664 case 38 :
665 case 36 :
666 case 6 :
667 case 4 :
668 case 50 :
669 case 48 :
670 case 18 :
671 case 16 :
672 return(bAig_Zero);
673 case 45 :
674 case 15 :
675 case 13 :
676 case 59 :
677 case 57 :
678 case 47 :
679 case 27 :
680 case 25 :
681 t1 = PureSat_And2(manager, l, r);
682 return(t1);
683 }
684 }
685 else if(caseIndex == 3) {
686 switch(caseSig) {
687 case 37 :
688 case 33 :
689 case 5 :
690 case 1 :
691 case 55 :
692 case 51 :
693 case 23 :
694 case 19 :
695 t1 = PureSat_And(manager, bAig_Not(rl), lr);
696 t2 = PureSat_And(manager, ll, t1);
697 return(t2);
698 case 36 :
699 case 32 :
700 case 4 :
701 case 0 :
702 case 54 :
703 case 50 :
704 case 22 :
705 case 18 :
706 t1 = PureSat_And(manager, rl, lr);
707 t2 = PureSat_And(manager, ll, t1);
708 return(t2);
709 case 44 :
710 case 40 :
711 case 12 :
712 case 8 :
713 case 62 :
714 case 58 :
715 case 30 :
716 case 26 :
717 t1 = PureSat_And(manager, rl, lr);
718 t2 = PureSat_And(manager, bAig_Not(ll), t1);
719 return(t2);
720 case 45 :
721 case 41 :
722 case 13 :
723 case 9 :
724 case 63 :
725 case 59 :
726 case 31 :
727 case 27 :
728 t1 = PureSat_And(manager, bAig_Not(ll), bAig_Not(rl));
729 t2 = PureSat_Or(manager, bAig_Not(lr), t1);
730 return(t2);
731 case 39 :
732 case 35 :
733 case 7 :
734 case 3 :
735 case 53 :
736 case 49 :
737 case 21 :
738 case 17 :
739 return(l);
740 case 46 :
741 case 42 :
742 case 14 :
743 case 10 :
744 case 60 :
745 case 56 :
746 case 28 :
747 case 24 :
748 return(r);
749 case 38 :
750 case 34 :
751 case 6 :
752 case 2 :
753 case 52 :
754 case 48 :
755 case 20 :
756 case 16 :
757 return(bAig_Zero);
758 case 47 :
759 case 43 :
760 case 15 :
761 case 11 :
762 case 61 :
763 case 57 :
764 case 29 :
765 case 25 :
766 t1 = PureSat_And2(manager, l, r);
767 return(t1);
768 }
769 }
770 else if(caseIndex == 4) {
771 switch(caseSig) {
772 case 22 :
773 case 20 :
774 case 6 :
775 case 4 :
776 case 50 :
777 case 48 :
778 case 34 :
779 case 32 :
780 case 2 :
781 case 16 :
782 case 52 :
783 case 1 :
784 case 8 :
785 case 19 :
786 case 26 :
787 case 37 :
788 case 44 :
789 case 38 :
790 case 55 :
791 case 62 :
792 return(bAig_Zero);
793 case 0 :
794 case 18 :
795 case 36 :
796 case 54 :
797 case 9 :
798 case 27 :
799 case 45 :
800 case 63 :
801 case 5 :
802 case 23 :
803 case 33 :
804 case 51 :
805 case 3 :
806 case 17 :
807 case 49 :
808 case 7 :
809 case 35 :
810 case 21 :
811 case 39 :
812 case 53 :
813 return(l);
814 case 40 :
815 case 58 :
816 case 12 :
817 case 30 :
818 case 24 :
819 case 10 :
820 case 14 :
821 case 56 :
822 case 28 :
823 case 42 :
824 case 60 :
825 case 46 :
826 return(r);
827 case 11 :
828 case 47 :
829 case 25 :
830 case 61 :
831 return(bAig_Not(ll));
832 case 41 :
833 case 59 :
834 case 13 :
835 case 31 :
836 return(bAig_Not(lr));
837 case 15 :
838 t1 = PureSat_And(manager, ll, bAig_Not(lr));
839 t2 = PureSat_And(manager, bAig_Not(ll), lr);
840 return(bAig_Not(PureSat_And2(manager, bAig_Not(t1), bAig_Not(t2))));
841 case 57 :
842 t1 = PureSat_And(manager, rl, bAig_Not(rr));
843 t2 = PureSat_And(manager, bAig_Not(rl), rr);
844 return(bAig_Not(PureSat_And2(manager, bAig_Not(t1), bAig_Not(t2))));
845 case 29 :
846 t1 = PureSat_And(manager, ll, lr);
847 t2 = PureSat_And(manager, bAig_Not(ll), bAig_Not(lr));
848 return((PureSat_And2(manager, bAig_Not(t1), bAig_Not(t2))));
849 case 43 :
850 t1 = PureSat_And(manager, rl, rr);
851 t2 = PureSat_And(manager, bAig_Not(rl), bAig_Not(rr));
852 return((PureSat_And2(manager, bAig_Not(t1), bAig_Not(t2))));
853 }
854 }
855 return(0);
856}
857
858
859
860/**Function********************************************************************
861
862 Synopsis [test whether two level minimization can be enabled--iff the two
863 nodes are in the same timeframe]
864
865 Description [output, l,r,ll,lr,rl,rr must be in the same class to pass the test]
866
867 SideEffects []
868
869 SeeAlso []
870
871******************************************************************************/
872
873
874int PureSat_Test2LevelMini(bAig_Manager_t *manager,
875 bAigEdge_t l,
876 bAigEdge_t r)
877{
878 int class_ = bAig_Class(l);
879 bAigEdge_t ll,lr,rl,rr;
880
881 if(!manager->test2LevelMini)
882 return 0;
883
884 if(class_!= bAig_Class(r) || class_ != manager->class_)
885 return 0;
886
887 ll = leftChild(l);
888 if(ll!=bAig_NULL && class_!=bAig_Class(ll))
889 return 0;
890 lr = rightChild(l);
891 if(lr!=bAig_NULL && class_!=bAig_Class(lr))
892 return 0;
893 rl = leftChild(r);
894 if(rl!=bAig_NULL && class_!=bAig_Class(rl))
895 return 0;
896 rr = rightChild(r);
897 if(rr!=bAig_NULL && class_!=bAig_Class(rr))
898 return 0;
899
900 return 1;
901}
902
903/**Function********************************************************************
904
905 Synopsis [And function for two AIG nodes. The difference with
906 bAigCreateAndNode is that here two level minimization
907 is only allowed with the same timeframe, otherwise the
908 global variable for interpolation generation may not be
909 latch variables]
910
911 Description []
912
913 SideEffects []
914
915 SeeAlso []
916
917******************************************************************************/
918
919bAigEdge_t
920PureSat_And(
921 bAig_Manager_t *manager,
922 bAigEdge_t nodeIndex1,
923 bAigEdge_t nodeIndex2)
924{
925
926 bAigEdge_t newNodeIndex;
927
928 nodeIndex1 = bAig_GetCanonical(manager, nodeIndex1);
929 nodeIndex2 = bAig_GetCanonical(manager, nodeIndex2);
930
931 newNodeIndex = nodeIndex1; /* The left node has the smallest index */
932 if (bAig_NonInvertedEdge(nodeIndex1) > bAig_NonInvertedEdge(nodeIndex2)){
933 nodeIndex1 = nodeIndex2;
934 nodeIndex2 = newNodeIndex;
935 }
936
937 if ( nodeIndex2 == bAig_Zero ) {
938 return bAig_Zero;
939 }
940 if ( nodeIndex1 == bAig_Zero ) {
941 return bAig_Zero;
942 }
943 if ( nodeIndex2 == bAig_One ) {
944 return nodeIndex1;
945 }
946 if ( nodeIndex1 == bAig_One ) {
947 return nodeIndex2;
948 }
949 if ( nodeIndex1 == nodeIndex2 ) {
950 return nodeIndex1;
951 }
952 if ( nodeIndex1 == bAig_Not(nodeIndex2) ) {
953 return bAig_Zero;
954 }
955
956 /* Look for the new node in the Hash table */
957 newNodeIndex = PureSat_HashTableLookup(manager, nodeIndex1, nodeIndex2);
958
959
960 if (newNodeIndex == bAig_NULL){
961 if(!PureSat_Test2LevelMini(manager,nodeIndex1,nodeIndex2)){
962 newNodeIndex = PureSat_And2(manager, nodeIndex1, nodeIndex2);
963 return newNodeIndex;
964 }
965
966 if(bAigIsVar(manager, nodeIndex1) && bAigIsVar(manager, nodeIndex2))
967 newNodeIndex = PureSat_And2(manager, nodeIndex1, nodeIndex2);
968 else if(bAigIsVar(manager, nodeIndex1))
969 newNodeIndex = PureSat_And3(manager, nodeIndex1, nodeIndex2);
970 else if(bAigIsVar(manager, nodeIndex2))
971 newNodeIndex = PureSat_And3(manager, nodeIndex2, nodeIndex1);
972 else {
973 newNodeIndex = PureSat_And4(manager, nodeIndex1, nodeIndex2);
974 }
975 }
976
977 return newNodeIndex;
978
979}
980
981
982/**Function********************************************************************
983
984 Synopsis [OR operation for two aig nodes]
985
986 Description []
987
988 SideEffects []
989
990 SeeAlso []
991
992******************************************************************************/
993
994bAigEdge_t
995PureSat_Or(
996 bAig_Manager_t *manager,
997 bAigEdge_t nodeIndex1,
998 bAigEdge_t nodeIndex2)
999{
1000 return ( bAig_Not(PureSat_And(manager, bAig_Not(nodeIndex1), bAig_Not(nodeIndex2))));
1001}
1002
1003
1004/**Function********************************************************************
1005
1006 Synopsis [XOR operation for two aig nodes]
1007
1008 Description []
1009
1010 SideEffects []
1011
1012 SeeAlso []
1013
1014******************************************************************************/
1015
1016bAigEdge_t
1017PureSat_Xor(
1018 bAig_Manager_t *manager,
1019 bAigEdge_t nodeIndex1,
1020 bAigEdge_t nodeIndex2)
1021{
1022 return PureSat_Or(manager,
1023 PureSat_And(manager, nodeIndex1, bAig_Not(nodeIndex2)),
1024 PureSat_And(manager, bAig_Not(nodeIndex1),nodeIndex2)
1025 );
1026}
1027
1028
1029/**Function********************************************************************
1030
1031 Synopsis [EQ operation for two aig nodes]
1032
1033 Description []
1034
1035 SideEffects []
1036
1037 SeeAlso []
1038
1039******************************************************************************/
1040
1041bAigEdge_t
1042PureSat_Eq(
1043 bAig_Manager_t *manager,
1044 bAigEdge_t nodeIndex1,
1045 bAigEdge_t nodeIndex2)
1046{
1047 return bAig_Not(
1048 PureSat_Xor(manager, nodeIndex1, nodeIndex2)
1049 );
1050}
1051
1052
1053/**Function********************************************************************
1054
1055 Synopsis [THEN operation for two aig nodes]
1056
1057 Description []
1058
1059 SideEffects []
1060
1061 SeeAlso []
1062
1063******************************************************************************/
1064
1065bAigEdge_t
1066PureSat_Then(
1067 bAig_Manager_t *manager,
1068 bAigEdge_t nodeIndex1,
1069 bAigEdge_t nodeIndex2)
1070{
1071 return PureSat_Or(manager,
1072 bAig_Not(nodeIndex1),
1073 nodeIndex2);
1074}
1075
1076
1077
1078/**Function********************************************************************
1079
1080 Synopsis [Create variable AIG nodes]
1081
1082 Description []
1083
1084 SideEffects []
1085
1086 SeeAlso []
1087
1088******************************************************************************/
1089
1090
1091bAigEdge_t
1092PureSat_CreateVarNode(
1093 bAig_Manager_t *manager,
1094 nameType_t *name)
1095{
1096
1097 bAigEdge_t varIndex;
1098 int class_ = manager->class_;
1099
1100
1101 if (!st_lookup(manager->SymbolTableArray[class_], name, &varIndex)){
1102 varIndex = bAig_CreateNode(manager, bAig_NULL, bAig_NULL);
1103 if (varIndex == bAig_NULL){
1104 return (varIndex);
1105 }
1106 /* Insert the varaible in the Symbol Table */
1107 st_insert(manager->SymbolTableArray[class_],
1108 name, (char*) (long) varIndex);
1109 manager->nameList[bAigNodeID(varIndex)] = name;
1110 return(varIndex);
1111 }
1112 else {
1113 return (varIndex);
1114 }
1115}
Note: See TracBrowser for help on using the repository browser.