1 /**CFile****************************************************************
2
3 FileName [giaUtil.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Scalable AIG package.]
8
9 Synopsis [Various utilities.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: giaUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "gia.h"
22 #include "base/main/mainInt.h"
23
24 ABC_NAMESPACE_IMPL_START
25
26
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30
31 #define NUMBER1 3716960521u
32 #define NUMBER2 2174103536u
33
34 ////////////////////////////////////////////////////////////////////////
35 /// FUNCTION DEFINITIONS ///
36 ////////////////////////////////////////////////////////////////////////
37
38 /**Function*************************************************************
39
40 Synopsis [Creates a sequence or random numbers.]
41
42 Description []
43
44 SideEffects []
45
46 SeeAlso [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx]
47
48 ***********************************************************************/
Gia_ManRandom(int fReset)49 unsigned Gia_ManRandom( int fReset )
50 {
51 static unsigned int m_z = NUMBER1;
52 static unsigned int m_w = NUMBER2;
53 if ( fReset )
54 {
55 m_z = NUMBER1;
56 m_w = NUMBER2;
57 }
58 m_z = 36969 * (m_z & 65535) + (m_z >> 16);
59 m_w = 18000 * (m_w & 65535) + (m_w >> 16);
60 return (m_z << 16) + m_w;
61 }
Gia_ManRandomW(int fReset)62 word Gia_ManRandomW( int fReset )
63 {
64 return ((word)Gia_ManRandom(fReset) << 32) | ((word)Gia_ManRandom(fReset) << 0);
65 }
66
67
68
69 /**Function*************************************************************
70
71 Synopsis [Creates random info for the primary inputs.]
72
73 Description []
74
75 SideEffects []
76
77 SeeAlso []
78
79 ***********************************************************************/
Gia_ManRandomInfo(Vec_Ptr_t * vInfo,int iInputStart,int iWordStart,int iWordStop)80 void Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop )
81 {
82 unsigned * pInfo;
83 int i, w;
84 Vec_PtrForEachEntryStart( unsigned *, vInfo, pInfo, i, iInputStart )
85 for ( w = iWordStart; w < iWordStop; w++ )
86 pInfo[w] = Gia_ManRandom(0);
87 }
88
89
90 /**Function*************************************************************
91
92 Synopsis [Returns the time stamp.]
93
94 Description [The file should be closed.]
95
96 SideEffects []
97
98 SeeAlso []
99
100 ***********************************************************************/
Gia_TimeStamp()101 char * Gia_TimeStamp()
102 {
103 static char Buffer[100];
104 char * TimeStamp;
105 time_t ltime;
106 // get the current time
107 time( <ime );
108 TimeStamp = asctime( localtime( <ime ) );
109 TimeStamp[ strlen(TimeStamp) - 1 ] = 0;
110 strcpy( Buffer, TimeStamp );
111 return Buffer;
112 }
113
114 /**Function*************************************************************
115
116 Synopsis [Returns the composite name of the file.]
117
118 Description []
119
120 SideEffects []
121
122 SeeAlso []
123
124 ***********************************************************************/
Gia_FileNameGenericAppend(char * pBase,char * pSuffix)125 char * Gia_FileNameGenericAppend( char * pBase, char * pSuffix )
126 {
127 static char Buffer[1000];
128 char * pDot;
129 strcpy( Buffer, pBase );
130 if ( (pDot = strrchr( Buffer, '.' )) )
131 *pDot = 0;
132 strcat( Buffer, pSuffix );
133 if ( (pDot = strrchr( Buffer, '\\' )) || (pDot = strrchr( Buffer, '/' )) )
134 return pDot+1;
135 return Buffer;
136 }
137
138 /**Function*************************************************************
139
140 Synopsis []
141
142 Description []
143
144 SideEffects []
145
146 SeeAlso []
147
148 ***********************************************************************/
Gia_ManIncrementTravId(Gia_Man_t * p)149 void Gia_ManIncrementTravId( Gia_Man_t * p )
150 {
151 if ( p->pTravIds == NULL )
152 {
153 p->nTravIdsAlloc = Gia_ManObjNum(p) + 100;
154 p->pTravIds = ABC_CALLOC( int, p->nTravIdsAlloc );
155 p->nTravIds = 0;
156 }
157 while ( p->nTravIdsAlloc < Gia_ManObjNum(p) )
158 {
159 p->nTravIdsAlloc *= 2;
160 p->pTravIds = ABC_REALLOC( int, p->pTravIds, p->nTravIdsAlloc );
161 memset( p->pTravIds + p->nTravIdsAlloc/2, 0, sizeof(int) * p->nTravIdsAlloc/2 );
162 }
163 p->nTravIds++;
164 }
165
166 /**Function*************************************************************
167
168 Synopsis [Sets phases of the internal nodes.]
169
170 Description []
171
172 SideEffects []
173
174 SeeAlso []
175
176 ***********************************************************************/
Gia_ManCleanMark01(Gia_Man_t * p)177 void Gia_ManCleanMark01( Gia_Man_t * p )
178 {
179 Gia_Obj_t * pObj;
180 int i;
181 Gia_ManForEachObj( p, pObj, i )
182 pObj->fMark0 = pObj->fMark1 = 0;
183 }
184
185 /**Function*************************************************************
186
187 Synopsis [Sets phases of the internal nodes.]
188
189 Description []
190
191 SideEffects []
192
193 SeeAlso []
194
195 ***********************************************************************/
Gia_ManSetMark0(Gia_Man_t * p)196 void Gia_ManSetMark0( Gia_Man_t * p )
197 {
198 Gia_Obj_t * pObj;
199 int i;
200 Gia_ManForEachObj( p, pObj, i )
201 pObj->fMark0 = 1;
202 }
203
204 /**Function*************************************************************
205
206 Synopsis [Sets phases of the internal nodes.]
207
208 Description []
209
210 SideEffects []
211
212 SeeAlso []
213
214 ***********************************************************************/
Gia_ManCleanMark0(Gia_Man_t * p)215 void Gia_ManCleanMark0( Gia_Man_t * p )
216 {
217 Gia_Obj_t * pObj;
218 int i;
219 Gia_ManForEachObj( p, pObj, i )
220 pObj->fMark0 = 0;
221 }
222
223 /**Function*************************************************************
224
225 Synopsis [Sets phases of the internal nodes.]
226
227 Description []
228
229 SideEffects []
230
231 SeeAlso []
232
233 ***********************************************************************/
Gia_ManCheckMark0(Gia_Man_t * p)234 void Gia_ManCheckMark0( Gia_Man_t * p )
235 {
236 Gia_Obj_t * pObj;
237 int i;
238 Gia_ManForEachObj( p, pObj, i )
239 assert( pObj->fMark0 == 0 );
240 }
241
242 /**Function*************************************************************
243
244 Synopsis [Sets phases of the internal nodes.]
245
246 Description []
247
248 SideEffects []
249
250 SeeAlso []
251
252 ***********************************************************************/
Gia_ManSetMark1(Gia_Man_t * p)253 void Gia_ManSetMark1( Gia_Man_t * p )
254 {
255 Gia_Obj_t * pObj;
256 int i;
257 Gia_ManForEachObj( p, pObj, i )
258 pObj->fMark1 = 1;
259 }
260
261 /**Function*************************************************************
262
263 Synopsis [Sets phases of the internal nodes.]
264
265 Description []
266
267 SideEffects []
268
269 SeeAlso []
270
271 ***********************************************************************/
Gia_ManCleanMark1(Gia_Man_t * p)272 void Gia_ManCleanMark1( Gia_Man_t * p )
273 {
274 Gia_Obj_t * pObj;
275 int i;
276 Gia_ManForEachObj( p, pObj, i )
277 pObj->fMark1 = 0;
278 }
279
280 /**Function*************************************************************
281
282 Synopsis [Sets phases of the internal nodes.]
283
284 Description []
285
286 SideEffects []
287
288 SeeAlso []
289
290 ***********************************************************************/
Gia_ManCheckMark1(Gia_Man_t * p)291 void Gia_ManCheckMark1( Gia_Man_t * p )
292 {
293 Gia_Obj_t * pObj;
294 int i;
295 Gia_ManForEachObj( p, pObj, i )
296 assert( pObj->fMark1 == 0 );
297 }
298
299 /**Function*************************************************************
300
301 Synopsis [Cleans the value.]
302
303 Description []
304
305 SideEffects []
306
307 SeeAlso []
308
309 ***********************************************************************/
Gia_ManCleanValue(Gia_Man_t * p)310 void Gia_ManCleanValue( Gia_Man_t * p )
311 {
312 int i;
313 for ( i = 0; i < p->nObjs; i++ )
314 p->pObjs[i].Value = 0;
315 }
316
317 /**Function*************************************************************
318
319 Synopsis [Cleans the value.]
320
321 Description []
322
323 SideEffects []
324
325 SeeAlso []
326
327 ***********************************************************************/
Gia_ManFillValue(Gia_Man_t * p)328 void Gia_ManFillValue( Gia_Man_t * p )
329 {
330 int i;
331 for ( i = 0; i < p->nObjs; i++ )
332 p->pObjs[i].Value = ~0;
333 }
334
335 /**Function*************************************************************
336
337 Synopsis [Sets the phase of one object.]
338
339 Description []
340
341 SideEffects []
342
343 SeeAlso []
344
345 ***********************************************************************/
Gia_ObjSetPhase(Gia_Man_t * p,Gia_Obj_t * pObj)346 void Gia_ObjSetPhase( Gia_Man_t * p, Gia_Obj_t * pObj )
347 {
348 if ( Gia_ObjIsAnd(pObj) )
349 {
350 int fPhase0 = Gia_ObjPhase(Gia_ObjFanin0(pObj)) ^ Gia_ObjFaninC0(pObj);
351 int fPhase1 = Gia_ObjPhase(Gia_ObjFanin1(pObj)) ^ Gia_ObjFaninC1(pObj);
352 if ( Gia_ObjIsMux(p, pObj) )
353 {
354 int fPhase2 = Gia_ObjPhase(Gia_ObjFanin2(p, pObj)) ^ Gia_ObjFaninC2(p, pObj);
355 pObj->fPhase = (fPhase2 && fPhase1) || (!fPhase2 && fPhase0);
356 }
357 else if ( Gia_ObjIsXor(pObj) )
358 pObj->fPhase = fPhase0 ^ fPhase1;
359 else
360 pObj->fPhase = fPhase0 & fPhase1;
361 }
362 else if ( Gia_ObjIsCo(pObj) )
363 pObj->fPhase = (Gia_ObjPhase(Gia_ObjFanin0(pObj)) ^ Gia_ObjFaninC0(pObj));
364 else
365 pObj->fPhase = 0;
366 }
367
368 /**Function*************************************************************
369
370 Synopsis [Sets phases of the internal nodes.]
371
372 Description []
373
374 SideEffects []
375
376 SeeAlso []
377
378 ***********************************************************************/
Gia_ManSetPhase(Gia_Man_t * p)379 void Gia_ManSetPhase( Gia_Man_t * p )
380 {
381 Gia_Obj_t * pObj;
382 int i;
383 Gia_ManForEachObj( p, pObj, i )
384 Gia_ObjSetPhase( p, pObj );
385 }
Gia_ManSetPhasePattern(Gia_Man_t * p,Vec_Int_t * vCiValues)386 void Gia_ManSetPhasePattern( Gia_Man_t * p, Vec_Int_t * vCiValues )
387 {
388 Gia_Obj_t * pObj;
389 int i;
390 assert( Gia_ManCiNum(p) == Vec_IntSize(vCiValues) );
391 Gia_ManForEachObj( p, pObj, i )
392 if ( Gia_ObjIsCi(pObj) )
393 pObj->fPhase = Vec_IntEntry( vCiValues, Gia_ObjCioId(pObj) );
394 else
395 Gia_ObjSetPhase( p, pObj );
396 }
397
398 /**Function*************************************************************
399
400 Synopsis [Sets phases of the internal nodes.]
401
402 Description []
403
404 SideEffects []
405
406 SeeAlso []
407
408 ***********************************************************************/
Gia_ManSetPhase1(Gia_Man_t * p)409 void Gia_ManSetPhase1( Gia_Man_t * p )
410 {
411 Gia_Obj_t * pObj;
412 int i;
413 Gia_ManForEachCi( p, pObj, i )
414 pObj->fPhase = 1;
415 Gia_ManForEachObj( p, pObj, i )
416 if ( !Gia_ObjIsCi(pObj) )
417 Gia_ObjSetPhase( p, pObj );
418 }
419
420 /**Function*************************************************************
421
422 Synopsis [Sets phases of the internal nodes.]
423
424 Description []
425
426 SideEffects []
427
428 SeeAlso []
429
430 ***********************************************************************/
Gia_ManCleanPhase(Gia_Man_t * p)431 void Gia_ManCleanPhase( Gia_Man_t * p )
432 {
433 Gia_Obj_t * pObj;
434 int i;
435 Gia_ManForEachObj( p, pObj, i )
436 pObj->fPhase = 0;
437 }
438
439 /**Function*************************************************************
440
441 Synopsis [Returns the number of COs whose value is 1.]
442
443 Description []
444
445 SideEffects []
446
447 SeeAlso []
448
449 ***********************************************************************/
Gia_ManCheckCoPhase(Gia_Man_t * p)450 int Gia_ManCheckCoPhase( Gia_Man_t * p )
451 {
452 Gia_Obj_t * pObj;
453 int i, Counter = 0;
454 Gia_ManForEachCo( p, pObj, i )
455 Counter += pObj->fPhase;
456 return Counter;
457 }
458
459 /**Function*************************************************************
460
461 Synopsis [Prepares copies for the model.]
462
463 Description []
464
465 SideEffects []
466
467 SeeAlso []
468
469 ***********************************************************************/
Gia_ManCleanLevels(Gia_Man_t * p,int Size)470 void Gia_ManCleanLevels( Gia_Man_t * p, int Size )
471 {
472 if ( p->vLevels == NULL )
473 p->vLevels = Vec_IntAlloc( Size );
474 Vec_IntFill( p->vLevels, Size, 0 );
475 }
476 /**Function*************************************************************
477
478 Synopsis [Prepares copies for the model.]
479
480 Description []
481
482 SideEffects []
483
484 SeeAlso []
485
486 ***********************************************************************/
Gia_ManCleanTruth(Gia_Man_t * p)487 void Gia_ManCleanTruth( Gia_Man_t * p )
488 {
489 if ( p->vTruths == NULL )
490 p->vTruths = Vec_IntAlloc( Gia_ManObjNum(p) );
491 Vec_IntFill( p->vTruths, Gia_ManObjNum(p), -1 );
492 }
493
494 /**Function*************************************************************
495
496 Synopsis [Assigns levels.]
497
498 Description []
499
500 SideEffects []
501
502 SeeAlso []
503
504 ***********************************************************************/
Gia_ManLevelNum(Gia_Man_t * p)505 int Gia_ManLevelNum( Gia_Man_t * p )
506 {
507 Gia_Obj_t * pObj;
508 int i;
509 Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
510 p->nLevels = 0;
511 Gia_ManForEachObj( p, pObj, i )
512 {
513 if ( !p->fGiaSimple && Gia_ObjIsBuf(pObj) )
514 Gia_ObjSetBufLevel( p, pObj );
515 else if ( Gia_ObjIsAnd(pObj) )
516 Gia_ObjSetGateLevel( p, pObj );
517 else if ( Gia_ObjIsCo(pObj) )
518 Gia_ObjSetCoLevel( p, pObj );
519 else
520 Gia_ObjSetLevel( p, pObj, 0 );
521 p->nLevels = Abc_MaxInt( p->nLevels, Gia_ObjLevel(p, pObj) );
522 }
523 return p->nLevels;
524 }
Gia_ManLevelAve(Gia_Man_t * p)525 float Gia_ManLevelAve( Gia_Man_t * p )
526 {
527 Gia_Obj_t * pObj;
528 int i, Ave = 0;
529 assert( p->vLevels );
530 Gia_ManForEachCo( p, pObj, i )
531 Ave += Gia_ObjLevel(p, pObj);
532 return (float)Ave / Gia_ManCoNum(p);
533 }
534
535 /**Function*************************************************************
536
537 Synopsis [Assigns levels using CI level information.]
538
539 Description []
540
541 SideEffects []
542
543 SeeAlso []
544
545 ***********************************************************************/
Gia_ManGetCiLevels(Gia_Man_t * p)546 Vec_Int_t * Gia_ManGetCiLevels( Gia_Man_t * p )
547 {
548 Vec_Int_t * vCiLevels;
549 Gia_Obj_t * pObj;
550 int i;
551 if ( p->vLevels == NULL )
552 return NULL;
553 vCiLevels = Vec_IntAlloc( Gia_ManCiNum(p) );
554 Gia_ManForEachCi( p, pObj, i )
555 Vec_IntPush( vCiLevels, Gia_ObjLevel(p, pObj) );
556 return vCiLevels;
557 }
Gia_ManSetLevels(Gia_Man_t * p,Vec_Int_t * vCiLevels)558 int Gia_ManSetLevels( Gia_Man_t * p, Vec_Int_t * vCiLevels )
559 {
560 Gia_Obj_t * pObj;
561 int i;
562 if ( vCiLevels == NULL )
563 return Gia_ManLevelNum( p );
564 assert( Vec_IntSize(vCiLevels) == Gia_ManCiNum(p) );
565 Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
566 p->nLevels = 0;
567 Gia_ManForEachCi( p, pObj, i )
568 {
569 Gia_ObjSetLevel( p, pObj, Vec_IntEntry(vCiLevels, i) );
570 p->nLevels = Abc_MaxInt( p->nLevels, Gia_ObjLevel(p, pObj) );
571 }
572 Gia_ManForEachObj( p, pObj, i )
573 {
574 if ( Gia_ObjIsAnd(pObj) )
575 Gia_ObjSetGateLevel( p, pObj );
576 else if ( Gia_ObjIsCo(pObj) )
577 Gia_ObjSetCoLevel( p, pObj );
578 else continue;
579 p->nLevels = Abc_MaxInt( p->nLevels, Gia_ObjLevel(p, pObj) );
580 }
581 return p->nLevels;
582 }
583
584 /**Function*************************************************************
585
586 Synopsis [Compute reverse levels.]
587
588 Description []
589
590 SideEffects []
591
592 SeeAlso []
593
594 ***********************************************************************/
Gia_ManReverseLevel(Gia_Man_t * p)595 Vec_Int_t * Gia_ManReverseLevel( Gia_Man_t * p )
596 {
597 Vec_Int_t * vLevelRev;
598 Gia_Obj_t * pObj;
599 int i;
600 vLevelRev = Vec_IntStart( Gia_ManObjNum(p) );
601 Gia_ManForEachAndReverse( p, pObj, i )
602 {
603 int LevelR = Vec_IntEntry( vLevelRev, i );
604 if ( Gia_ObjIsMux(p, pObj) )
605 {
606 Vec_IntUpdateEntry( vLevelRev, Gia_ObjFaninId0(pObj, i), LevelR + 2 );
607 Vec_IntUpdateEntry( vLevelRev, Gia_ObjFaninId1(pObj, i), LevelR + 2 );
608 Vec_IntUpdateEntry( vLevelRev, Gia_ObjFaninId2(p, i), LevelR + 2 );
609 }
610 else if ( Gia_ObjIsXor(pObj) )
611 {
612 Vec_IntUpdateEntry( vLevelRev, Gia_ObjFaninId0(pObj, i), LevelR + 2 );
613 Vec_IntUpdateEntry( vLevelRev, Gia_ObjFaninId1(pObj, i), LevelR + 2 );
614 }
615 else if ( Gia_ObjIsBuf(pObj) )
616 {
617 Vec_IntUpdateEntry( vLevelRev, Gia_ObjFaninId0(pObj, i), LevelR );
618 }
619 else
620 {
621 Vec_IntUpdateEntry( vLevelRev, Gia_ObjFaninId0(pObj, i), LevelR + 1 );
622 Vec_IntUpdateEntry( vLevelRev, Gia_ObjFaninId1(pObj, i), LevelR + 1 );
623 }
624 }
625 return vLevelRev;
626 }
627
628 /**Function*************************************************************
629
630 Synopsis [Compute required levels.]
631
632 Description []
633
634 SideEffects []
635
636 SeeAlso []
637
638 ***********************************************************************/
Gia_ManRequiredLevel(Gia_Man_t * p)639 Vec_Int_t * Gia_ManRequiredLevel( Gia_Man_t * p )
640 {
641 Vec_Int_t * vRequired;
642 Gia_Obj_t * pObj;
643 int i, LevelMax = 0;
644 vRequired = Gia_ManReverseLevel( p );
645 Gia_ManForEachCi( p, pObj, i )
646 LevelMax = Abc_MaxInt( LevelMax, Vec_IntEntry(vRequired, Gia_ObjId(p, pObj)) );
647 Gia_ManForEachObj( p, pObj, i )
648 Vec_IntWriteEntry( vRequired, i, LevelMax - Vec_IntEntry(vRequired, i) );
649 return vRequired;
650 }
651
652 /**Function*************************************************************
653
654 Synopsis [Compute slacks measured using the number of AIG levels.]
655
656 Description []
657
658 SideEffects []
659
660 SeeAlso []
661
662 ***********************************************************************/
Gia_ManComputeSlacks(Gia_Man_t * p)663 Vec_Int_t * Gia_ManComputeSlacks( Gia_Man_t * p )
664 {
665 Gia_Obj_t * pObj;
666 int i, nLevels = Gia_ManLevelNum( p );
667 Vec_Int_t * vLevelR = Gia_ManReverseLevel( p );
668 Vec_Int_t * vSlacks = Vec_IntAlloc( Gia_ManObjNum(p) );
669 Gia_ManForEachObj( p, pObj, i )
670 Vec_IntPush( vSlacks, nLevels - Gia_ObjLevelId(p, i) - Vec_IntEntry(vLevelR, i) );
671 assert( Vec_IntSize(vSlacks) == Gia_ManObjNum(p) );
672 Vec_IntFree( vLevelR );
673 return vSlacks;
674 }
675
676 /**Function*************************************************************
677
678 Synopsis [Assigns levels.]
679
680 Description []
681
682 SideEffects []
683
684 SeeAlso []
685
686 ***********************************************************************/
Gia_ManCreateValueRefs(Gia_Man_t * p)687 void Gia_ManCreateValueRefs( Gia_Man_t * p )
688 {
689 Gia_Obj_t * pObj;
690 int i;
691 Gia_ManForEachObj( p, pObj, i )
692 {
693 pObj->Value = 0;
694 if ( Gia_ObjIsAnd(pObj) )
695 {
696 Gia_ObjFanin0(pObj)->Value++;
697 if ( !Gia_ObjIsBuf(pObj) )
698 Gia_ObjFanin1(pObj)->Value++;
699 }
700 else if ( Gia_ObjIsCo(pObj) )
701 Gia_ObjFanin0(pObj)->Value++;
702 }
703 }
704
705 /**Function*************************************************************
706
707 Synopsis [Assigns references.]
708
709 Description []
710
711 SideEffects []
712
713 SeeAlso []
714
715 ***********************************************************************/
Gia_ManCreateRefs(Gia_Man_t * p)716 void Gia_ManCreateRefs( Gia_Man_t * p )
717 {
718 Gia_Obj_t * pObj;
719 int i;
720 assert( p->pRefs == NULL );
721 p->pRefs = ABC_CALLOC( int, Gia_ManObjNum(p) );
722 Gia_ManForEachObj( p, pObj, i )
723 {
724 if ( Gia_ObjIsAnd(pObj) )
725 {
726 Gia_ObjRefFanin0Inc( p, pObj );
727 if ( !Gia_ObjIsBuf(pObj) )
728 Gia_ObjRefFanin1Inc( p, pObj );
729 if ( Gia_ObjIsMuxId(p, i) )
730 Gia_ObjRefFanin2Inc( p, pObj );
731 }
732 else if ( Gia_ObjIsCo(pObj) )
733 Gia_ObjRefFanin0Inc( p, pObj );
734 }
735 }
736
737 /**Function*************************************************************
738
739 Synopsis [Assigns references.]
740
741 Description []
742
743 SideEffects []
744
745 SeeAlso []
746
747 ***********************************************************************/
Gia_ManCreateMuxRefs(Gia_Man_t * p)748 int * Gia_ManCreateMuxRefs( Gia_Man_t * p )
749 {
750 Gia_Obj_t * pObj, * pCtrl, * pFan0, * pFan1;
751 int i, * pMuxRefs;
752 pMuxRefs = ABC_CALLOC( int, Gia_ManObjNum(p) );
753 Gia_ManForEachObj( p, pObj, i )
754 {
755 if ( Gia_ObjRecognizeExor( pObj, &pFan0, &pFan1 ) )
756 continue;
757 if ( !Gia_ObjIsMuxType(pObj) )
758 continue;
759 pCtrl = Gia_ObjRecognizeMux( pObj, &pFan0, &pFan1 );
760 pMuxRefs[ Gia_ObjId(p, Gia_Regular(pCtrl)) ]++;
761 }
762 return pMuxRefs;
763 }
764
765 /**Function*************************************************************
766
767 Synopsis [Computes the maximum frontier size.]
768
769 Description []
770
771 SideEffects []
772
773 SeeAlso []
774
775 ***********************************************************************/
Gia_ManBfsForCrossCut(Gia_Man_t * p)776 Vec_Int_t * Gia_ManBfsForCrossCut( Gia_Man_t * p )
777 {
778 Vec_Int_t * vNodes = Vec_IntAlloc( Gia_ManObjNum(p) );
779 Vec_Vec_t * vLevels = Gia_ManLevelize( p );
780 Vec_Ptr_t * vObjs;
781 Gia_Obj_t * pObj;
782 int i, k;
783 Vec_VecForEachLevel( vLevels, vObjs, i )
784 Vec_PtrForEachEntry( Gia_Obj_t *, vObjs, pObj, k )
785 Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
786 Vec_VecFree( vLevels );
787 return vNodes;
788 }
789
Gia_ManDfsForCrossCut_rec(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vNodes)790 void Gia_ManDfsForCrossCut_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
791 {
792 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
793 return;
794 Gia_ObjSetTravIdCurrent(p, pObj);
795 if ( Gia_ObjIsCi(pObj) )
796 {
797 Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
798 return;
799 }
800 if ( Gia_ObjIsCo(pObj) )
801 {
802 Gia_ObjFanin0(pObj)->Value++;
803 Gia_ManDfsForCrossCut_rec( p, Gia_ObjFanin0(pObj), vNodes );
804 Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
805 return;
806 }
807 assert( Gia_ObjIsAnd(pObj) );
808 Gia_ObjFanin0(pObj)->Value++;
809 Gia_ObjFanin1(pObj)->Value++;
810 Gia_ManDfsForCrossCut_rec( p, Gia_ObjFanin0(pObj), vNodes );
811 Gia_ManDfsForCrossCut_rec( p, Gia_ObjFanin1(pObj), vNodes );
812 Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
813 }
Gia_ManDfsForCrossCut(Gia_Man_t * p,int fReverse)814 Vec_Int_t * Gia_ManDfsForCrossCut( Gia_Man_t * p, int fReverse )
815 {
816 Vec_Int_t * vNodes;
817 Gia_Obj_t * pObj;
818 int i;
819 Gia_ManCleanValue( p );
820 vNodes = Vec_IntAlloc( Gia_ManObjNum(p) );
821 Gia_ManIncrementTravId( p );
822 if ( fReverse )
823 {
824 Gia_ManForEachCoReverse( p, pObj, i )
825 if ( !Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
826 Gia_ManDfsForCrossCut_rec( p, pObj, vNodes );
827 }
828 else
829 {
830 Gia_ManForEachCo( p, pObj, i )
831 if ( !Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
832 Gia_ManDfsForCrossCut_rec( p, pObj, vNodes );
833 }
834 return vNodes;
835 }
Gia_ManCrossCut(Gia_Man_t * p,int fReverse)836 int Gia_ManCrossCut( Gia_Man_t * p, int fReverse )
837 {
838 Vec_Int_t * vNodes;
839 Gia_Obj_t * pObj;
840 int i, nCutCur = 0, nCutMax = 0;
841 vNodes = Gia_ManDfsForCrossCut( p, fReverse );
842 //vNodes = Gia_ManBfsForCrossCut( p );
843 Gia_ManForEachObjVec( vNodes, p, pObj, i )
844 {
845 if ( pObj->Value )
846 nCutCur++;
847 if ( nCutMax < nCutCur )
848 nCutMax = nCutCur;
849 if ( Gia_ObjIsAnd(pObj) )
850 {
851 if ( --Gia_ObjFanin0(pObj)->Value == 0 )
852 nCutCur--;
853 if ( --Gia_ObjFanin1(pObj)->Value == 0 )
854 nCutCur--;
855 }
856 else if ( Gia_ObjIsCo(pObj) )
857 {
858 if ( --Gia_ObjFanin0(pObj)->Value == 0 )
859 nCutCur--;
860 }
861 }
862 Vec_IntFree( vNodes );
863 Gia_ManForEachObj( p, pObj, i )
864 assert( pObj->Value == 0 );
865 return nCutMax;
866 }
867
868
869 /**Function*************************************************************
870
871 Synopsis [Collects PO Ids into one array.]
872
873 Description []
874
875 SideEffects []
876
877 SeeAlso []
878
879 ***********************************************************************/
Gia_ManCollectPoIds(Gia_Man_t * p)880 Vec_Int_t * Gia_ManCollectPoIds( Gia_Man_t * p )
881 {
882 Vec_Int_t * vStart;
883 int Entry, i;
884 vStart = Vec_IntAlloc( Gia_ManPoNum(p) );
885 Vec_IntForEachEntryStop( p->vCos, Entry, i, Gia_ManPoNum(p) )
886 Vec_IntPush( vStart, Entry );
887 return vStart;
888 }
889
890
891 /**Function*************************************************************
892
893 Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
894
895 Description []
896
897 SideEffects []
898
899 SeeAlso []
900
901 ***********************************************************************/
Gia_ObjIsMuxType(Gia_Obj_t * pNode)902 int Gia_ObjIsMuxType( Gia_Obj_t * pNode )
903 {
904 Gia_Obj_t * pNode0, * pNode1;
905 // check that the node is regular
906 assert( !Gia_IsComplement(pNode) );
907 // if the node is not AND, this is not MUX
908 if ( !Gia_ObjIsAnd(pNode) || Gia_ObjIsBuf(pNode) )
909 return 0;
910 // if the children are not complemented, this is not MUX
911 if ( !Gia_ObjFaninC0(pNode) || !Gia_ObjFaninC1(pNode) )
912 return 0;
913 // get children
914 pNode0 = Gia_ObjFanin0(pNode);
915 pNode1 = Gia_ObjFanin1(pNode);
916 // if the children are not ANDs, this is not MUX
917 if ( !Gia_ObjIsAnd(pNode0) || !Gia_ObjIsAnd(pNode1) )
918 return 0;
919 // otherwise the node is MUX iff it has a pair of equal grandchildren
920 return (Gia_ObjFanin0(pNode0) == Gia_ObjFanin0(pNode1) && (Gia_ObjFaninC0(pNode0) ^ Gia_ObjFaninC0(pNode1))) ||
921 (Gia_ObjFanin0(pNode0) == Gia_ObjFanin1(pNode1) && (Gia_ObjFaninC0(pNode0) ^ Gia_ObjFaninC1(pNode1))) ||
922 (Gia_ObjFanin1(pNode0) == Gia_ObjFanin0(pNode1) && (Gia_ObjFaninC1(pNode0) ^ Gia_ObjFaninC0(pNode1))) ||
923 (Gia_ObjFanin1(pNode0) == Gia_ObjFanin1(pNode1) && (Gia_ObjFaninC1(pNode0) ^ Gia_ObjFaninC1(pNode1)));
924 }
925
926
927 /**Function*************************************************************
928
929 Synopsis [Recognizes what nodes are inputs of the EXOR.]
930
931 Description []
932
933 SideEffects []
934
935 SeeAlso []
936
937 ***********************************************************************/
Gia_ObjRecognizeExor(Gia_Obj_t * pObj,Gia_Obj_t ** ppFan0,Gia_Obj_t ** ppFan1)938 int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ppFan0, Gia_Obj_t ** ppFan1 )
939 {
940 Gia_Obj_t * p0, * p1;
941 assert( !Gia_IsComplement(pObj) );
942 if ( !Gia_ObjIsAnd(pObj) || Gia_ObjIsBuf(pObj) )
943 return 0;
944 assert( Gia_ObjIsAnd(pObj) );
945 p0 = Gia_ObjChild0(pObj);
946 p1 = Gia_ObjChild1(pObj);
947 if ( !Gia_IsComplement(p0) || !Gia_IsComplement(p1) )
948 return 0;
949 p0 = Gia_Regular(p0);
950 p1 = Gia_Regular(p1);
951 if ( !Gia_ObjIsAnd(p0) || !Gia_ObjIsAnd(p1) )
952 return 0;
953 if ( Gia_ObjFanin0(p0) != Gia_ObjFanin0(p1) || Gia_ObjFanin1(p0) != Gia_ObjFanin1(p1) )
954 return 0;
955 if ( Gia_ObjFaninC0(p0) == Gia_ObjFaninC0(p1) || Gia_ObjFaninC1(p0) == Gia_ObjFaninC1(p1) )
956 return 0;
957 if ( ppFan0 ) *ppFan0 = Gia_ObjChild0(p0);
958 if ( ppFan1 ) *ppFan1 = Gia_ObjChild1(p0);
959 return 1;
960 }
961
962 /**Function*************************************************************
963
964 Synopsis [Recognizes what nodes are control and data inputs of a MUX.]
965
966 Description [If the node is a MUX, returns the control variable C.
967 Assigns nodes T and E to be the then and else variables of the MUX.
968 Node C is never complemented. Nodes T and E can be complemented.
969 This function also recognizes EXOR/NEXOR gates as MUXes.]
970
971 SideEffects []
972
973 SeeAlso []
974
975 ***********************************************************************/
Gia_ObjRecognizeMux(Gia_Obj_t * pNode,Gia_Obj_t ** ppNodeT,Gia_Obj_t ** ppNodeE)976 Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE )
977 {
978 Gia_Obj_t * pNode0, * pNode1;
979 assert( !Gia_IsComplement(pNode) );
980 assert( Gia_ObjIsMuxType(pNode) );
981 // get children
982 pNode0 = Gia_ObjFanin0(pNode);
983 pNode1 = Gia_ObjFanin1(pNode);
984
985 // find the control variable
986 if ( Gia_ObjFanin1(pNode0) == Gia_ObjFanin1(pNode1) && (Gia_ObjFaninC1(pNode0) ^ Gia_ObjFaninC1(pNode1)) )
987 {
988 // if ( FrGia_IsComplement(pNode1->p2) )
989 if ( Gia_ObjFaninC1(pNode0) )
990 { // pNode2->p2 is positive phase of C
991 *ppNodeT = Gia_Not(Gia_ObjChild0(pNode1));//pNode2->p1);
992 *ppNodeE = Gia_Not(Gia_ObjChild0(pNode0));//pNode1->p1);
993 return Gia_ObjChild1(pNode1);//pNode2->p2;
994 }
995 else
996 { // pNode1->p2 is positive phase of C
997 *ppNodeT = Gia_Not(Gia_ObjChild0(pNode0));//pNode1->p1);
998 *ppNodeE = Gia_Not(Gia_ObjChild0(pNode1));//pNode2->p1);
999 return Gia_ObjChild1(pNode0);//pNode1->p2;
1000 }
1001 }
1002 else if ( Gia_ObjFanin0(pNode0) == Gia_ObjFanin0(pNode1) && (Gia_ObjFaninC0(pNode0) ^ Gia_ObjFaninC0(pNode1)) )
1003 {
1004 // if ( FrGia_IsComplement(pNode1->p1) )
1005 if ( Gia_ObjFaninC0(pNode0) )
1006 { // pNode2->p1 is positive phase of C
1007 *ppNodeT = Gia_Not(Gia_ObjChild1(pNode1));//pNode2->p2);
1008 *ppNodeE = Gia_Not(Gia_ObjChild1(pNode0));//pNode1->p2);
1009 return Gia_ObjChild0(pNode1);//pNode2->p1;
1010 }
1011 else
1012 { // pNode1->p1 is positive phase of C
1013 *ppNodeT = Gia_Not(Gia_ObjChild1(pNode0));//pNode1->p2);
1014 *ppNodeE = Gia_Not(Gia_ObjChild1(pNode1));//pNode2->p2);
1015 return Gia_ObjChild0(pNode0);//pNode1->p1;
1016 }
1017 }
1018 else if ( Gia_ObjFanin0(pNode0) == Gia_ObjFanin1(pNode1) && (Gia_ObjFaninC0(pNode0) ^ Gia_ObjFaninC1(pNode1)) )
1019 {
1020 // if ( FrGia_IsComplement(pNode1->p1) )
1021 if ( Gia_ObjFaninC0(pNode0) )
1022 { // pNode2->p2 is positive phase of C
1023 *ppNodeT = Gia_Not(Gia_ObjChild0(pNode1));//pNode2->p1);
1024 *ppNodeE = Gia_Not(Gia_ObjChild1(pNode0));//pNode1->p2);
1025 return Gia_ObjChild1(pNode1);//pNode2->p2;
1026 }
1027 else
1028 { // pNode1->p1 is positive phase of C
1029 *ppNodeT = Gia_Not(Gia_ObjChild1(pNode0));//pNode1->p2);
1030 *ppNodeE = Gia_Not(Gia_ObjChild0(pNode1));//pNode2->p1);
1031 return Gia_ObjChild0(pNode0);//pNode1->p1;
1032 }
1033 }
1034 else if ( Gia_ObjFanin1(pNode0) == Gia_ObjFanin0(pNode1) && (Gia_ObjFaninC1(pNode0) ^ Gia_ObjFaninC0(pNode1)) )
1035 {
1036 // if ( FrGia_IsComplement(pNode1->p2) )
1037 if ( Gia_ObjFaninC1(pNode0) )
1038 { // pNode2->p1 is positive phase of C
1039 *ppNodeT = Gia_Not(Gia_ObjChild1(pNode1));//pNode2->p2);
1040 *ppNodeE = Gia_Not(Gia_ObjChild0(pNode0));//pNode1->p1);
1041 return Gia_ObjChild0(pNode1);//pNode2->p1;
1042 }
1043 else
1044 { // pNode1->p2 is positive phase of C
1045 *ppNodeT = Gia_Not(Gia_ObjChild0(pNode0));//pNode1->p1);
1046 *ppNodeE = Gia_Not(Gia_ObjChild1(pNode1));//pNode2->p2);
1047 return Gia_ObjChild1(pNode0);//pNode1->p2;
1048 }
1049 }
1050 assert( 0 ); // this is not MUX
1051 return NULL;
1052 }
Gia_ObjRecognizeMuxLits(Gia_Man_t * p,Gia_Obj_t * pNode,int * iLitT,int * iLitE)1053 int Gia_ObjRecognizeMuxLits( Gia_Man_t * p, Gia_Obj_t * pNode, int * iLitT, int * iLitE )
1054 {
1055 Gia_Obj_t * pNodeT, * pNodeE;
1056 Gia_Obj_t * pCtrl = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
1057 assert( pCtrl != NULL );
1058 *iLitT = Gia_Obj2Lit( p, pNodeT );
1059 *iLitE = Gia_Obj2Lit( p, pNodeE );
1060 return Gia_Obj2Lit( p, pCtrl );
1061 }
1062
1063
1064 /**Function*************************************************************
1065
1066 Synopsis [Dereferences the node's MFFC.]
1067
1068 Description []
1069
1070 SideEffects []
1071
1072 SeeAlso []
1073
1074 ***********************************************************************/
Gia_NodeDeref_rec(Gia_Man_t * p,Gia_Obj_t * pNode)1075 int Gia_NodeDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
1076 {
1077 Gia_Obj_t * pFanin;
1078 int Counter = 0;
1079 if ( Gia_ObjIsCi(pNode) )
1080 return 0;
1081 assert( Gia_ObjIsAnd(pNode) );
1082 pFanin = Gia_ObjFanin0(pNode);
1083 assert( Gia_ObjRefNum(p, pFanin) > 0 );
1084 if ( Gia_ObjRefDec(p, pFanin) == 0 )
1085 Counter += Gia_NodeDeref_rec( p, pFanin );
1086 pFanin = Gia_ObjFanin1(pNode);
1087 assert( Gia_ObjRefNum(p, pFanin) > 0 );
1088 if ( Gia_ObjRefDec(p, pFanin) == 0 )
1089 Counter += Gia_NodeDeref_rec( p, pFanin );
1090 return Counter + 1;
1091 }
1092
1093 /**Function*************************************************************
1094
1095 Synopsis [References the node's MFFC.]
1096
1097 Description []
1098
1099 SideEffects []
1100
1101 SeeAlso []
1102
1103 ***********************************************************************/
Gia_NodeRef_rec(Gia_Man_t * p,Gia_Obj_t * pNode)1104 int Gia_NodeRef_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
1105 {
1106 Gia_Obj_t * pFanin;
1107 int Counter = 0;
1108 if ( Gia_ObjIsCi(pNode) )
1109 return 0;
1110 assert( Gia_ObjIsAnd(pNode) );
1111 pFanin = Gia_ObjFanin0(pNode);
1112 if ( Gia_ObjRefInc(p, pFanin) == 0 )
1113 Counter += Gia_NodeRef_rec( p, pFanin );
1114 pFanin = Gia_ObjFanin1(pNode);
1115 if ( Gia_ObjRefInc(p, pFanin) == 0 )
1116 Counter += Gia_NodeRef_rec( p, pFanin );
1117 return Counter + 1;
1118 }
1119
1120
1121 /**Function*************************************************************
1122
1123 Synopsis [References the node's MFFC.]
1124
1125 Description []
1126
1127 SideEffects []
1128
1129 SeeAlso []
1130
1131 ***********************************************************************/
Gia_ManPoMffcSize(Gia_Man_t * p)1132 int Gia_ManPoMffcSize( Gia_Man_t * p )
1133 {
1134 Gia_ManCreateRefs( p );
1135 return Gia_NodeDeref_rec( p, Gia_ObjFanin0(Gia_ManPo(p, 0)) );
1136 }
1137
1138 /**Function*************************************************************
1139
1140 Synopsis [Returns the number of internal nodes in the MFFC.]
1141
1142 Description []
1143
1144 SideEffects []
1145
1146 SeeAlso []
1147
1148 ***********************************************************************/
Gia_NodeMffcSize(Gia_Man_t * p,Gia_Obj_t * pNode)1149 int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode )
1150 {
1151 int ConeSize1, ConeSize2;
1152 assert( !Gia_IsComplement(pNode) );
1153 assert( Gia_ObjIsCand(pNode) );
1154 ConeSize1 = Gia_NodeDeref_rec( p, pNode );
1155 ConeSize2 = Gia_NodeRef_rec( p, pNode );
1156 assert( ConeSize1 == ConeSize2 );
1157 assert( ConeSize1 >= 0 );
1158 return ConeSize1;
1159 }
1160
1161 /**Function*************************************************************
1162
1163 Synopsis [Returns the number of internal nodes in the MFFC.]
1164
1165 Description []
1166
1167 SideEffects []
1168
1169 SeeAlso []
1170
1171 ***********************************************************************/
Gia_NodeCollect_rec(Gia_Man_t * p,Gia_Obj_t * pNode,Vec_Int_t * vSupp)1172 void Gia_NodeCollect_rec( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSupp )
1173 {
1174 if ( Gia_ObjIsTravIdCurrent(p, pNode) )
1175 return;
1176 Gia_ObjSetTravIdCurrent(p, pNode);
1177 if ( Gia_ObjRefNum(p, pNode) || Gia_ObjIsCi(pNode) )
1178 {
1179 Vec_IntPush( vSupp, Gia_ObjId(p, pNode) );
1180 return;
1181 }
1182 assert( Gia_ObjIsAnd(pNode) );
1183 Gia_NodeCollect_rec( p, Gia_ObjFanin0(pNode), vSupp );
1184 Gia_NodeCollect_rec( p, Gia_ObjFanin1(pNode), vSupp );
1185 }
Gia_NodeMffcSizeSupp(Gia_Man_t * p,Gia_Obj_t * pNode,Vec_Int_t * vSupp)1186 int Gia_NodeMffcSizeSupp( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSupp )
1187 {
1188 int ConeSize1, ConeSize2;
1189 assert( !Gia_IsComplement(pNode) );
1190 assert( Gia_ObjIsAnd(pNode) );
1191 Vec_IntClear( vSupp );
1192 Gia_ManIncrementTravId( p );
1193 ConeSize1 = Gia_NodeDeref_rec( p, pNode );
1194 Gia_NodeCollect_rec( p, Gia_ObjFanin0(pNode), vSupp );
1195 Gia_NodeCollect_rec( p, Gia_ObjFanin1(pNode), vSupp );
1196 ConeSize2 = Gia_NodeRef_rec( p, pNode );
1197 assert( ConeSize1 == ConeSize2 );
1198 assert( ConeSize1 >= 0 );
1199 return ConeSize1;
1200 }
1201
1202 /**Function*************************************************************
1203
1204 Synopsis [Returns 1 if AIG has dangling nodes.]
1205
1206 Description []
1207
1208 SideEffects []
1209
1210 SeeAlso []
1211
1212 ***********************************************************************/
Gia_ManHasDangling(Gia_Man_t * p)1213 int Gia_ManHasDangling( Gia_Man_t * p )
1214 {
1215 Gia_Obj_t * pObj;
1216 int i, Counter = 0;
1217 Gia_ManForEachObj( p, pObj, i )
1218 {
1219 pObj->fMark0 = 0;
1220 if ( Gia_ObjIsCo(pObj) )
1221 Gia_ObjFanin0(pObj)->fMark0 = 1;
1222 else if ( Gia_ObjIsMux(p, pObj) )
1223 {
1224 Gia_ObjFanin0(pObj)->fMark0 = 1;
1225 Gia_ObjFanin1(pObj)->fMark0 = 1;
1226 Gia_ObjFanin2(p, pObj)->fMark0 = 1;
1227 }
1228 else if ( Gia_ObjIsAnd(pObj) )
1229 {
1230 Gia_ObjFanin0(pObj)->fMark0 = 1;
1231 Gia_ObjFanin1(pObj)->fMark0 = 1;
1232 }
1233 }
1234 Gia_ManForEachAnd( p, pObj, i )
1235 Counter += !pObj->fMark0;
1236 Gia_ManCleanMark0( p );
1237 return Counter;
1238 }
1239
1240 /**Function*************************************************************
1241
1242 Synopsis [Returns 1 if AIG has dangling nodes.]
1243
1244 Description []
1245
1246 SideEffects []
1247
1248 SeeAlso []
1249
1250 ***********************************************************************/
Gia_ManMarkDangling(Gia_Man_t * p)1251 int Gia_ManMarkDangling( Gia_Man_t * p )
1252 {
1253 Gia_Obj_t * pObj;
1254 int i, Counter = 0;
1255 Gia_ManForEachObj( p, pObj, i )
1256 {
1257 pObj->fMark0 = 0;
1258 if ( Gia_ObjIsAnd(pObj) )
1259 {
1260 Gia_ObjFanin0(pObj)->fMark0 = 1;
1261 Gia_ObjFanin1(pObj)->fMark0 = 1;
1262 }
1263 else if ( Gia_ObjIsCo(pObj) )
1264 Gia_ObjFanin0(pObj)->fMark0 = 1;
1265 }
1266 Gia_ManForEachAnd( p, pObj, i )
1267 Counter += !pObj->fMark0;
1268 return Counter;
1269 }
1270
1271 /**Function*************************************************************
1272
1273 Synopsis [Returns 1 if AIG has dangling nodes.]
1274
1275 Description []
1276
1277 SideEffects []
1278
1279 SeeAlso []
1280
1281 ***********************************************************************/
Gia_ManGetDangling(Gia_Man_t * p)1282 Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p )
1283 {
1284 Vec_Int_t * vDangles;
1285 Gia_Obj_t * pObj;
1286 int i;
1287 Gia_ManForEachObj( p, pObj, i )
1288 {
1289 pObj->fMark0 = 0;
1290 if ( Gia_ObjIsAnd(pObj) )
1291 {
1292 Gia_ObjFanin0(pObj)->fMark0 = 1;
1293 Gia_ObjFanin1(pObj)->fMark0 = 1;
1294 }
1295 else if ( Gia_ObjIsCo(pObj) )
1296 Gia_ObjFanin0(pObj)->fMark0 = 1;
1297 }
1298 vDangles = Vec_IntAlloc( 100 );
1299 Gia_ManForEachAnd( p, pObj, i )
1300 if ( !pObj->fMark0 )
1301 Vec_IntPush( vDangles, i );
1302 Gia_ManCleanMark0( p );
1303 return vDangles;
1304 }
1305 /**Function*************************************************************
1306
1307 Synopsis [Verbose printing of the AIG node.]
1308
1309 Description []
1310
1311 SideEffects []
1312
1313 SeeAlso []
1314
1315 ***********************************************************************/
Gia_ObjPrint(Gia_Man_t * p,Gia_Obj_t * pObj)1316 void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj )
1317 {
1318 if ( pObj == NULL )
1319 {
1320 printf( "Object is NULL." );
1321 return;
1322 }
1323 if ( Gia_IsComplement(pObj) )
1324 {
1325 printf( "Compl " );
1326 pObj = Gia_Not(pObj);
1327 }
1328 assert( !Gia_IsComplement(pObj) );
1329 printf( "Obj %4d : ", Gia_ObjId(p, pObj) );
1330 if ( Gia_ObjIsConst0(pObj) )
1331 printf( "constant 0" );
1332 else if ( Gia_ObjIsPi(p, pObj) )
1333 printf( "PI" );
1334 else if ( Gia_ObjIsPo(p, pObj) )
1335 printf( "PO( %4d%s )", Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " ") );
1336 else if ( Gia_ObjIsCi(pObj) )
1337 printf( "RO( %4d%s )", Gia_ObjFaninId0p(p, Gia_ObjRoToRi(p, pObj)), (Gia_ObjFaninC0(Gia_ObjRoToRi(p, pObj))? "\'" : " ") );
1338 else if ( Gia_ObjIsCo(pObj) )
1339 printf( "RI( %4d%s )", Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " ") );
1340 // else if ( Gia_ObjIsBuf(pObj) )
1341 // printf( "BUF( %d%s )", Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " ") );
1342 else if ( Gia_ObjIsXor(pObj) )
1343 printf( "XOR( %4d%s, %4d%s )",
1344 Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " "),
1345 Gia_ObjFaninId1p(p, pObj), (Gia_ObjFaninC1(pObj)? "\'" : " ") );
1346 else if ( Gia_ObjIsMuxId(p, Gia_ObjId(p, pObj)) )
1347 printf( "MUX( %4d%s, %4d%s, %4d%s )",
1348 Gia_ObjFaninId2p(p, pObj), (Gia_ObjFaninC2(p, pObj)? "\'" : " "),
1349 Gia_ObjFaninId1p(p, pObj), (Gia_ObjFaninC1(pObj)? "\'" : " "),
1350 Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " ") );
1351 else
1352 printf( "AND( %4d%s, %4d%s )",
1353 Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " "),
1354 Gia_ObjFaninId1p(p, pObj), (Gia_ObjFaninC1(pObj)? "\'" : " ") );
1355 if ( p->pRefs )
1356 printf( " (refs = %3d)", Gia_ObjRefNum(p, pObj) );
1357 if ( pObj->fMark0 )
1358 printf( " mark0" );
1359 if ( pObj->fMark1 )
1360 printf( " mark1" );
1361 if ( Gia_ManHasMapping(p) && Gia_ObjIsLut(p, Gia_ObjId(p, pObj)) )
1362 {
1363 int i, iFan;
1364 printf( " Cut = { " );
1365 Gia_LutForEachFanin( p, Gia_ObjId(p, pObj), iFan, i )
1366 printf( "%d ", iFan );
1367 printf( "}" );
1368 }
1369 if ( Gia_ManHasMapping2(p) && Gia_ObjIsLut2(p, Gia_ObjId(p, pObj)) )
1370 {
1371 int i, iFan;
1372 printf( " Cut = { " );
1373 Gia_LutForEachFanin2( p, Gia_ObjId(p, pObj), iFan, i )
1374 printf( "%d ", iFan );
1375 printf( "}" );
1376 }
1377 printf( "\n" );
1378 /*
1379 if ( p->pRefs )
1380 {
1381 Gia_Obj_t * pFanout;
1382 int i;
1383 int iFan = -1; // Suppress "might be used uninitialized"
1384 printf( "\nFanouts:\n" );
1385 Gia_ObjForEachFanout( p, pObj, pFanout, iFan, i )
1386 {
1387 printf( " " );
1388 printf( "Node %4d : ", Gia_ObjId(pFanout) );
1389 if ( Gia_ObjIsPo(pFanout) )
1390 printf( "PO( %4d%s )", Gia_ObjFanin0(pFanout)->Id, (Gia_ObjFaninC0(pFanout)? "\'" : " ") );
1391 else if ( Gia_ObjIsBuf(pFanout) )
1392 printf( "BUF( %d%s )", Gia_ObjFanin0(pFanout)->Id, (Gia_ObjFaninC0(pFanout)? "\'" : " ") );
1393 else
1394 printf( "AND( %4d%s, %4d%s )",
1395 Gia_ObjFanin0(pFanout)->Id, (Gia_ObjFaninC0(pFanout)? "\'" : " "),
1396 Gia_ObjFanin1(pFanout)->Id, (Gia_ObjFaninC1(pFanout)? "\'" : " ") );
1397 printf( "\n" );
1398 }
1399 return;
1400 }
1401 */
1402 }
Gia_ManPrint(Gia_Man_t * p)1403 void Gia_ManPrint( Gia_Man_t * p )
1404 {
1405 Gia_Obj_t * pObj;
1406 int i;
1407 printf( "GIA manager has %d ANDs, %d XORs, %d MUXes.\n",
1408 Gia_ManAndNum(p) - Gia_ManXorNum(p) - Gia_ManMuxNum(p), Gia_ManXorNum(p), Gia_ManMuxNum(p) );
1409 Gia_ManForEachObj( p, pObj, i )
1410 Gia_ObjPrint( p, pObj );
1411 }
Gia_ManPrintCo_rec(Gia_Man_t * p,Gia_Obj_t * pObj)1412 void Gia_ManPrintCo_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
1413 {
1414 if ( Gia_ObjIsAnd(pObj) )
1415 {
1416 Gia_ManPrintCo_rec( p, Gia_ObjFanin0(pObj) );
1417 Gia_ManPrintCo_rec( p, Gia_ObjFanin1(pObj) );
1418 if ( Gia_ObjIsMux(p, pObj) )
1419 Gia_ManPrintCo_rec( p, Gia_ObjFanin2(p, pObj) );
1420 }
1421 Gia_ObjPrint( p, pObj );
1422 }
Gia_ManPrintCo(Gia_Man_t * p,Gia_Obj_t * pObj)1423 void Gia_ManPrintCo( Gia_Man_t * p, Gia_Obj_t * pObj )
1424 {
1425 assert( Gia_ObjIsCo(pObj) );
1426 printf( "TFI cone of CO number %d:\n", Gia_ObjCioId(pObj) );
1427 Gia_ManPrintCo_rec( p, Gia_ObjFanin0(pObj) );
1428 Gia_ObjPrint( p, pObj );
1429 }
1430
Gia_ManPrintCollect_rec(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vNodes)1431 void Gia_ManPrintCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
1432 {
1433 if ( Vec_IntFind(vNodes, Gia_ObjId(p, pObj)) >= 0 )
1434 return;
1435 assert( Gia_ObjIsAnd(pObj) );
1436 Gia_ManPrintCollect_rec( p, Gia_ObjFanin0(pObj), vNodes );
1437 Gia_ManPrintCollect_rec( p, Gia_ObjFanin1(pObj), vNodes );
1438 if ( Gia_ObjIsMux(p, pObj) )
1439 Gia_ManPrintCollect_rec( p, Gia_ObjFanin2(p, pObj), vNodes );
1440 Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
1441 }
Gia_ManPrintCone(Gia_Man_t * p,Gia_Obj_t * pObj,int * pLeaves,int nLeaves,Vec_Int_t * vNodes)1442 void Gia_ManPrintCone( Gia_Man_t * p, Gia_Obj_t * pObj, int * pLeaves, int nLeaves, Vec_Int_t * vNodes )
1443 {
1444 int i;
1445 Vec_IntClear( vNodes );
1446 for ( i = 0; i < nLeaves; i++ )
1447 Vec_IntPush( vNodes, pLeaves[i] );
1448 Gia_ManPrintCollect_rec( p, pObj, vNodes );
1449 printf( "GIA logic cone for node %d:\n", Gia_ObjId(p, pObj) );
1450 Gia_ManForEachObjVec( vNodes, p, pObj, i )
1451 Gia_ObjPrint( p, pObj );
1452 }
Gia_ManPrintConeMulti(Gia_Man_t * p,Vec_Int_t * vObjs,Vec_Int_t * vLeaves,Vec_Int_t * vNodes)1453 void Gia_ManPrintConeMulti( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
1454 {
1455 Gia_Obj_t * pObj;
1456 int i;
1457 Vec_IntClear( vNodes );
1458 Vec_IntAppend( vNodes, vLeaves );
1459 Gia_ManForEachObjVec( vObjs, p, pObj, i )
1460 Gia_ManPrintCollect_rec( p, pObj, vNodes );
1461 printf( "GIA logic cone for %d nodes:\n", Vec_IntSize(vObjs) );
1462 Gia_ManForEachObjVec( vNodes, p, pObj, i )
1463 Gia_ObjPrint( p, pObj );
1464 }
1465
Gia_ManPrintCollect2_rec(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vNodes)1466 void Gia_ManPrintCollect2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
1467 {
1468 if ( Vec_IntFind(vNodes, Gia_ObjId(p, pObj)) >= 0 )
1469 return;
1470 if ( Gia_ObjIsCo(pObj) || Gia_ObjIsAnd(pObj) )
1471 Gia_ManPrintCollect2_rec( p, Gia_ObjFanin0(pObj), vNodes );
1472 if ( Gia_ObjIsAnd(pObj) )
1473 Gia_ManPrintCollect2_rec( p, Gia_ObjFanin1(pObj), vNodes );
1474 if ( Gia_ObjIsMux(p, pObj) )
1475 Gia_ManPrintCollect2_rec( p, Gia_ObjFanin2(p, pObj), vNodes );
1476 Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
1477 }
Gia_ManPrintCone2(Gia_Man_t * p,Gia_Obj_t * pObj)1478 void Gia_ManPrintCone2( Gia_Man_t * p, Gia_Obj_t * pObj )
1479 {
1480 Vec_Int_t * vNodes;
1481 int i;
1482 vNodes = Vec_IntAlloc( 100 );
1483 Gia_ManPrintCollect2_rec( p, pObj, vNodes );
1484 printf( "GIA logic cone for node %d:\n", Gia_ObjId(p, pObj) );
1485 Gia_ManForEachObjVec( vNodes, p, pObj, i )
1486 Gia_ObjPrint( p, pObj );
1487 Vec_IntFree( vNodes );
1488 }
1489
1490 /**Function*************************************************************
1491
1492 Synopsis [Complements the constraint outputs.]
1493
1494 Description []
1495
1496 SideEffects []
1497
1498 SeeAlso []
1499
1500 ***********************************************************************/
Gia_ManInvertConstraints(Gia_Man_t * pAig)1501 void Gia_ManInvertConstraints( Gia_Man_t * pAig )
1502 {
1503 Gia_Obj_t * pObj;
1504 int i;
1505 if ( Gia_ManConstrNum(pAig) == 0 )
1506 return;
1507 Gia_ManForEachPo( pAig, pObj, i )
1508 if ( i >= Gia_ManPoNum(pAig) - Gia_ManConstrNum(pAig) )
1509 Gia_ObjFlipFaninC0( pObj );
1510 }
Gia_ManInvertPos(Gia_Man_t * pAig)1511 void Gia_ManInvertPos( Gia_Man_t * pAig )
1512 {
1513 Gia_Obj_t * pObj;
1514 int i;
1515 Gia_ManForEachPo( pAig, pObj, i )
1516 Gia_ObjFlipFaninC0( pObj );
1517 }
1518
1519 /**Function*************************************************************
1520
1521 Synopsis [Testing the speedup due to grouping POs into batches.]
1522
1523 Description []
1524
1525 SideEffects []
1526
1527 SeeAlso []
1528
1529 ***********************************************************************/
Gia_ManCollectObjs_rec(Gia_Man_t * p,int iObjId,Vec_Int_t * vObjs,int Limit)1530 void Gia_ManCollectObjs_rec( Gia_Man_t * p, int iObjId, Vec_Int_t * vObjs, int Limit )
1531 {
1532 Gia_Obj_t * pObj;
1533 if ( Vec_IntSize(vObjs) == Limit )
1534 return;
1535 if ( Gia_ObjIsTravIdCurrentId(p, iObjId) )
1536 return;
1537 Gia_ObjSetTravIdCurrentId(p, iObjId);
1538 pObj = Gia_ManObj( p, iObjId );
1539 if ( Gia_ObjIsAnd(pObj) )
1540 {
1541 Gia_ManCollectObjs_rec( p, Gia_ObjFaninId0p(p, pObj), vObjs, Limit );
1542 if ( Vec_IntSize(vObjs) == Limit )
1543 return;
1544 Gia_ManCollectObjs_rec( p, Gia_ObjFaninId1p(p, pObj), vObjs, Limit );
1545 if ( Vec_IntSize(vObjs) == Limit )
1546 return;
1547 }
1548 Vec_IntPush( vObjs, iObjId );
1549 }
Gia_ManComputePoTruthTables(Gia_Man_t * p,int nBytesMax)1550 unsigned * Gia_ManComputePoTruthTables( Gia_Man_t * p, int nBytesMax )
1551 {
1552 int nVars = Gia_ManPiNum(p);
1553 int nTruthWords = Abc_TruthWordNum( nVars );
1554 int nTruths = nBytesMax / (sizeof(unsigned) * nTruthWords);
1555 int nTotalNodes = 0, nRounds = 0;
1556 Vec_Int_t * vObjs;
1557 Gia_Obj_t * pObj;
1558 abctime clk = Abc_Clock();
1559 int i;
1560 printf( "Var = %d. Words = %d. Truths = %d.\n", nVars, nTruthWords, nTruths );
1561 vObjs = Vec_IntAlloc( nTruths );
1562 Gia_ManIncrementTravId( p );
1563 Gia_ManForEachPo( p, pObj, i )
1564 {
1565 Gia_ManCollectObjs_rec( p, Gia_ObjFaninId0p(p, pObj), vObjs, nTruths );
1566 if ( Vec_IntSize(vObjs) == nTruths )
1567 {
1568 nRounds++;
1569 // printf( "%d ", i );
1570 nTotalNodes += Vec_IntSize( vObjs );
1571 Vec_IntClear( vObjs );
1572 Gia_ManIncrementTravId( p );
1573 }
1574 }
1575 // printf( "\n" );
1576 nTotalNodes += Vec_IntSize( vObjs );
1577 Vec_IntFree( vObjs );
1578
1579 printf( "Rounds = %d. Objects = %d. Total = %d. ", nRounds, Gia_ManObjNum(p), nTotalNodes );
1580 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1581
1582 return NULL;
1583 }
1584
1585
1586 /**Function*************************************************************
1587
1588 Synopsis [Returns 1 if the manager are structural identical.]
1589
1590 Description []
1591
1592 SideEffects []
1593
1594 SeeAlso []
1595
1596 ***********************************************************************/
Gia_ManCompare(Gia_Man_t * p1,Gia_Man_t * p2)1597 int Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 )
1598 {
1599 Gia_Obj_t * pObj1, * pObj2;
1600 int i;
1601 if ( Gia_ManObjNum(p1) != Gia_ManObjNum(p2) )
1602 {
1603 printf( "AIGs have different number of objects.\n" );
1604 return 0;
1605 }
1606 Gia_ManCleanValue( p1 );
1607 Gia_ManCleanValue( p2 );
1608 Gia_ManForEachObj( p1, pObj1, i )
1609 {
1610 pObj2 = Gia_ManObj( p2, i );
1611 if ( memcmp( pObj1, pObj2, sizeof(Gia_Obj_t) ) )
1612 {
1613 printf( "Objects %d are different.\n", i );
1614 return 0;
1615 }
1616 if ( p1->pReprs && p2->pReprs )
1617 {
1618 if ( memcmp( &p1->pReprs[i], &p2->pReprs[i], sizeof(Gia_Rpr_t) ) )
1619 {
1620 printf( "Representatives of objects %d are different.\n", i );
1621 return 0;
1622 }
1623 }
1624 }
1625 return 1;
1626 }
1627
1628 /**Function*************************************************************
1629
1630 Synopsis [Marks nodes that appear as faninis of other nodes.]
1631
1632 Description []
1633
1634 SideEffects []
1635
1636 SeeAlso []
1637
1638 ***********************************************************************/
Gia_ManMarkFanoutDrivers(Gia_Man_t * p)1639 void Gia_ManMarkFanoutDrivers( Gia_Man_t * p )
1640 {
1641 Gia_Obj_t * pObj;
1642 int i;
1643 Gia_ManForEachObj( p, pObj, i )
1644 {
1645 pObj->fMark0 = 0;
1646 if ( Gia_ObjIsAnd(pObj) )
1647 {
1648 Gia_ObjFanin0(pObj)->fMark0 = 1;
1649 Gia_ObjFanin1(pObj)->fMark0 = 1;
1650 }
1651 else if ( Gia_ObjIsCo(pObj) )
1652 Gia_ObjFanin0(pObj)->fMark0 = 1;
1653 }
1654 }
1655
1656
1657 /**Function*************************************************************
1658
1659 Synopsis [Swaps PO number 0 with PO number i.]
1660
1661 Description []
1662
1663 SideEffects []
1664
1665 SeeAlso []
1666
1667 ***********************************************************************/
Gia_ManSwapPos(Gia_Man_t * p,int i)1668 void Gia_ManSwapPos( Gia_Man_t * p, int i )
1669 {
1670 int Lit0, LitI;
1671 assert( i >= 0 && i < Gia_ManPoNum(p) );
1672 if ( i == 0 )
1673 return;
1674 Lit0 = Gia_ObjFaninLit0p( p, Gia_ManPo(p, 0) );
1675 LitI = Gia_ObjFaninLit0p( p, Gia_ManPo(p, i) );
1676 Gia_ManPatchCoDriver( p, 0, LitI );
1677 Gia_ManPatchCoDriver( p, i, Lit0 );
1678 }
1679
1680 /**Function*************************************************************
1681
1682 Synopsis [Save/load value from file.]
1683
1684 Description []
1685
1686 SideEffects []
1687
1688 SeeAlso []
1689
1690 ***********************************************************************/
Gia_ManSaveValue(Gia_Man_t * p)1691 Vec_Int_t * Gia_ManSaveValue( Gia_Man_t * p )
1692 {
1693 Vec_Int_t * vValues;
1694 Gia_Obj_t * pObj;
1695 int i;
1696 vValues = Vec_IntAlloc( Gia_ManObjNum(p) );
1697 Gia_ManForEachObj( p, pObj, i )
1698 Vec_IntPush( vValues, pObj->Value );
1699 return vValues;
1700 }
Gia_ManLoadValue(Gia_Man_t * p,Vec_Int_t * vValues)1701 void Gia_ManLoadValue( Gia_Man_t * p, Vec_Int_t * vValues )
1702 {
1703 Gia_Obj_t * pObj;
1704 int i;
1705 Gia_ManForEachObj( p, pObj, i )
1706 pObj->Value = Vec_IntEntry(vValues, i);
1707 }
1708
1709
1710 /**Function*************************************************************
1711
1712 Synopsis [Returns the array containing the first fanout of each object.]
1713
1714 Description []
1715
1716 SideEffects []
1717
1718 SeeAlso []
1719
1720 ***********************************************************************/
Gia_ManFirstFanouts(Gia_Man_t * p)1721 Vec_Int_t * Gia_ManFirstFanouts( Gia_Man_t * p )
1722 {
1723 Vec_Int_t * vFans = Vec_IntStart( Gia_ManObjNum(p) );
1724 Gia_Obj_t * pObj;
1725 int i;
1726 Gia_ManForEachObj( p, pObj, i )
1727 {
1728 if ( Gia_ObjIsAnd(pObj) )
1729 {
1730 if ( Vec_IntEntry(vFans, Gia_ObjFaninId0p(p, pObj)) == 0 )
1731 Vec_IntWriteEntry(vFans, Gia_ObjFaninId0p(p, pObj), i);
1732 if ( Vec_IntEntry(vFans, Gia_ObjFaninId1p(p, pObj)) == 0 )
1733 Vec_IntWriteEntry(vFans, Gia_ObjFaninId1p(p, pObj), i);
1734 if ( Gia_ObjIsMuxId(p, i) && Vec_IntEntry(vFans, Gia_ObjFaninId2p(p, pObj)) == 0 )
1735 Vec_IntWriteEntry(vFans, Gia_ObjFaninId2p(p, pObj), i);
1736 }
1737 else if ( Gia_ObjIsCo(pObj) )
1738 {
1739 if ( Vec_IntEntry(vFans, Gia_ObjFaninId0p(p, pObj)) == 0 )
1740 Vec_IntWriteEntry(vFans, Gia_ObjFaninId0p(p, pObj), i);
1741 }
1742 }
1743 return vFans;
1744 }
1745
1746 /**Function*************************************************************
1747
1748 Synopsis [Returns 1 if AIG has choices.]
1749
1750 Description []
1751
1752 SideEffects []
1753
1754 SeeAlso []
1755
1756 ***********************************************************************/
Gia_ManHasChoices_very_old(Gia_Man_t * p)1757 int Gia_ManHasChoices_very_old( Gia_Man_t * p )
1758 {
1759 Gia_Obj_t * pObj;
1760 int i, Counter1 = 0, Counter2 = 0;
1761 int nFailNoRepr = 0;
1762 int nFailHaveRepr = 0;
1763 int nChoiceNodes = 0;
1764 int nChoices = 0;
1765 if ( p->pReprs == NULL || p->pNexts == NULL )
1766 return 0;
1767 // check if there are any representatives
1768 Gia_ManForEachObj( p, pObj, i )
1769 {
1770 if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
1771 {
1772 // printf( "%d ", i );
1773 Counter1++;
1774 }
1775 // if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
1776 // Counter2++;
1777 }
1778 // printf( "\n" );
1779 Gia_ManForEachObj( p, pObj, i )
1780 {
1781 // if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
1782 // Counter1++;
1783 if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
1784 {
1785 // printf( "%d ", i );
1786 Counter2++;
1787 }
1788 }
1789 // printf( "\n" );
1790 if ( Counter1 == 0 )
1791 {
1792 printf( "Warning: AIG has repr data-strucure but not reprs.\n" );
1793 return 0;
1794 }
1795 printf( "%d nodes have reprs.\n", Counter1 );
1796 printf( "%d nodes have nexts.\n", Counter2 );
1797 // check if there are any internal nodes without fanout
1798 // make sure all nodes without fanout have representatives
1799 // make sure all nodes with fanout have no representatives
1800 ABC_FREE( p->pRefs );
1801 Gia_ManCreateRefs( p );
1802 Gia_ManForEachAnd( p, pObj, i )
1803 {
1804 if ( Gia_ObjRefNum(p, pObj) == 0 )
1805 {
1806 if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) == NULL )
1807 nFailNoRepr++;
1808 else
1809 nChoices++;
1810 }
1811 else
1812 {
1813 if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) != NULL )
1814 nFailHaveRepr++;
1815 if ( Gia_ObjNextObj( p, Gia_ObjId(p, pObj) ) != NULL )
1816 nChoiceNodes++;
1817 }
1818 if ( Gia_ObjReprObj( p, i ) )
1819 assert( Gia_ObjRepr(p, i) < i );
1820 }
1821 if ( nChoices == 0 )
1822 return 0;
1823 if ( nFailNoRepr )
1824 {
1825 printf( "Gia_ManHasChoices_very_old(): Error: %d internal nodes have no fanout and no repr.\n", nFailNoRepr );
1826 // return 0;
1827 }
1828 if ( nFailHaveRepr )
1829 {
1830 printf( "Gia_ManHasChoices_very_old(): Error: %d internal nodes have both fanout and repr.\n", nFailHaveRepr );
1831 // return 0;
1832 }
1833 // printf( "Gia_ManHasChoices_very_old(): AIG has %d choice nodes with %d choices.\n", nChoiceNodes, nChoices );
1834 return 1;
1835 }
1836
1837
1838 /**Function*************************************************************
1839
1840 Synopsis [Proving multi-output properties.]
1841
1842 Description []
1843
1844 SideEffects []
1845
1846 SeeAlso []
1847
1848 ***********************************************************************/
Gia_ManGroupProve(Gia_Man_t * pInit,char * pCommLine,int nGroupSize,int fVerbose)1849 Vec_Int_t * Gia_ManGroupProve( Gia_Man_t * pInit, char * pCommLine, int nGroupSize, int fVerbose )
1850 {
1851 Abc_Frame_t * pAbc = Abc_FrameReadGlobalFrame();
1852 Gia_Man_t * p = Gia_ManDup( pInit );
1853 Gia_Man_t * pGroup;
1854 Vec_Int_t * vOuts;
1855 Vec_Int_t * vOutMap;
1856 Vec_Ptr_t * vCexes;
1857 int i, k, nGroupCur, nGroups;
1858 abctime clk, timeComm = 0;
1859 abctime timeStart = Abc_Clock();
1860 // pre-conditions
1861 assert( nGroupSize > 0 );
1862 assert( pCommLine != NULL );
1863 assert( p->nConstrs == 0 );
1864 Abc_Print( 1, "RUNNING MultiProve: Group size = %d. Command line = \"%s\".\n", nGroupSize, pCommLine );
1865 // create output map
1866 vOuts = Vec_IntStartNatural( Gia_ManPoNum(p) );
1867 vOutMap = Vec_IntAlloc( Gia_ManPoNum(p) );
1868 vCexes = Vec_PtrAlloc( Gia_ManPoNum(p) );
1869 nGroups = Gia_ManPoNum(p) / nGroupSize + (int)((Gia_ManPoNum(p) % nGroupSize) > 0);
1870 for ( i = 0; i < nGroups; i++ )
1871 {
1872 // derive the group
1873 nGroupCur = ((i + 1) * nGroupSize < Gia_ManPoNum(p)) ? nGroupSize : Gia_ManPoNum(p) - i * nGroupSize;
1874 pGroup = Gia_ManDupCones( p, Vec_IntArray(vOuts) + i * nGroupSize, nGroupCur, 0 );
1875 Abc_Print( 1, "GROUP %4d : %4d <= PoId < %4d : ", i, i * nGroupSize, i * nGroupSize + nGroupCur );
1876 // set the current GIA
1877 Abc_FrameUpdateGia( pAbc, pGroup );
1878 // solve the group
1879 clk = Abc_Clock();
1880 Cmd_CommandExecute( pAbc, pCommLine );
1881 timeComm += Abc_Clock() - clk;
1882 // get the solution status
1883 if ( nGroupSize == 1 )
1884 {
1885 Vec_IntPush( vOutMap, Abc_FrameReadProbStatus(pAbc) );
1886 Vec_PtrPush( vCexes, Abc_FrameReadCex(pAbc) );
1887 }
1888 else // if ( nGroupSize > 1 )
1889 {
1890 Vec_Int_t * vStatusCur = Abc_FrameReadPoStatuses( pAbc );
1891 Vec_Ptr_t * vCexesCur = Abc_FrameReadCexVec( pAbc );
1892 assert( vStatusCur != NULL ); // only works for "bmc3" and "pdr"
1893 // assert( vCexesCur != NULL );
1894 for ( k = 0; k < nGroupCur; k++ )
1895 {
1896 Vec_IntPush( vOutMap, Vec_IntEntry(vStatusCur, k) );
1897 Vec_PtrPush( vCexes, vCexesCur ? Vec_PtrEntry(vCexesCur, k) : NULL );
1898 }
1899 }
1900 }
1901 assert( Vec_PtrSize(vCexes) == Gia_ManPoNum(p) );
1902 assert( Vec_IntSize(vOutMap) == Gia_ManPoNum(p) );
1903 // set CEXes
1904 if ( Vec_PtrCountZero(vCexes) < Vec_PtrSize(vCexes) )
1905 Abc_FrameReplaceCexVec( pAbc, &vCexes );
1906 else // there is no CEXes
1907 Vec_PtrFree( vCexes );
1908 // report the result
1909 Abc_Print( 1, "SUMMARY: " );
1910 Abc_Print( 1, "Properties = %6d. ", Gia_ManPoNum(p) );
1911 Abc_Print( 1, "UNSAT = %6d. ", Vec_IntCountEntry(vOutMap, 1) );
1912 Abc_Print( 1, "SAT = %6d. ", Vec_IntCountEntry(vOutMap, 0) );
1913 Abc_Print( 1, "UNDEC = %6d. ", Vec_IntCountEntry(vOutMap, -1) );
1914 Abc_Print( 1, "\n" );
1915 Abc_PrintTime( 1, "Command time", timeComm );
1916 Abc_PrintTime( 1, "Total time ", Abc_Clock() - timeStart );
1917 // cleanup
1918 Vec_IntFree( vOuts );
1919 Gia_ManStop( p );
1920 return vOutMap;
1921 }
1922
1923
1924 /**Function*************************************************************
1925
1926 Synopsis []
1927
1928 Description []
1929
1930 SideEffects []
1931
1932 SeeAlso []
1933
1934 ***********************************************************************/
Gia_ManPoXSim(Gia_Man_t * p,int nFrames,int fVerbose)1935 Vec_Int_t * Gia_ManPoXSim( Gia_Man_t * p, int nFrames, int fVerbose )
1936 {
1937 Vec_Int_t * vRes;
1938 Gia_Obj_t * pObj;
1939 int f, k, nLeft = Gia_ManPoNum(p);
1940 vRes = Vec_IntAlloc( Gia_ManPoNum(p) );
1941 Vec_IntFill( vRes, Gia_ManPoNum(p), nFrames );
1942 Gia_ObjTerSimSet0( Gia_ManConst0(p) );
1943 Gia_ManForEachRi( p, pObj, k )
1944 Gia_ObjTerSimSet0( pObj );
1945 for ( f = 0; f < nFrames; f++ )
1946 {
1947 Gia_ManForEachPi( p, pObj, k )
1948 Gia_ObjTerSimSetX( pObj );
1949 Gia_ManForEachRo( p, pObj, k )
1950 Gia_ObjTerSimRo( p, pObj );
1951 Gia_ManForEachAnd( p, pObj, k )
1952 Gia_ObjTerSimAnd( pObj );
1953 Gia_ManForEachCo( p, pObj, k )
1954 Gia_ObjTerSimCo( pObj );
1955 if ( fVerbose )
1956 {
1957 Gia_ManForEachPo( p, pObj, k )
1958 Gia_ObjTerSimPrint( pObj );
1959 printf( "\n" );
1960 }
1961 Gia_ManForEachPo( p, pObj, k )
1962 if ( Vec_IntEntry(vRes, k) == nFrames && Gia_ObjTerSimGetX(pObj) )
1963 Vec_IntWriteEntry(vRes, k, f), nLeft--;
1964 if ( nLeft == 0 )
1965 break;
1966 }
1967 if ( fVerbose )
1968 {
1969 if ( nLeft == 0 )
1970 printf( "Simulation converged after %d frames.\n", f+1 );
1971 else
1972 printf( "Simulation terminated after %d frames.\n", nFrames );
1973 }
1974 // Vec_IntPrint( vRes );
1975 return vRes;
1976 }
1977
1978 #define MAX_LUT_SIZE 8
1979 typedef struct Gia_MapLut_t_
1980 {
1981 int Type; // node type: PI=1, PO=2, LUT=3
1982 int Out; // ID
1983 int StartId; // -1
1984 int nFans; // fanin count
1985 float Delay; // 0.0
1986 int pFans[MAX_LUT_SIZE]; // fanin IDs
1987 unsigned pTruth[MAX_LUT_SIZE<6?1:(1<<(MAX_LUT_SIZE-5))]; // the truth table
1988 } Gia_MapLut_t;
1989
1990 /**Function*************************************************************
1991
1992 Synopsis []
1993
1994 Description []
1995
1996 SideEffects []
1997
1998 SeeAlso []
1999
2000 ***********************************************************************/
Gia_AigerWriteLut(Gia_Man_t * p,char * pFileName)2001 void Gia_AigerWriteLut( Gia_Man_t * p, char * pFileName )
2002 {
2003 Gia_Obj_t * pObj;
2004 int i, k, iFan, iLut = 0;
2005 int LutSizeMax = Gia_ManLutSizeMax( p );
2006 int nUints = Abc_TruthWordNum(LutSizeMax);
2007 int nLuts = 1 + Gia_ManCiNum(p) + Gia_ManCoNum(p) + Gia_ManLutNum(p);
2008 Gia_MapLut_t * pLuts = ABC_CALLOC( Gia_MapLut_t, nLuts );
2009 Vec_Wrd_t * vTruths = Vec_WrdStart( Gia_ManObjNum(p) );
2010 assert( LutSizeMax <= 6 );
2011 // set obj numbers
2012 // constant
2013 pLuts->Type = 3;
2014 memset( pLuts->pTruth, 0xFF, sizeof(unsigned) * nUints );
2015 Gia_ManFillValue(p);
2016 Gia_ManConst0(p)->Value = pLuts[iLut].Out = Abc_Var2Lit( iLut, 0 );
2017 iLut++;
2018 // inputs
2019 Gia_ManForEachCi( p, pObj, i )
2020 {
2021 pLuts[iLut].Type = 1;
2022 memset( pLuts[iLut].pTruth, 0xAA, sizeof(unsigned) * nUints );
2023 pObj->Value = pLuts[iLut].Out = Abc_Var2Lit( iLut, 0 );
2024 iLut++;
2025 }
2026 // nodes
2027 Gia_ManForEachObj( p, pObj, i )
2028 if ( i && Gia_ObjIsLut(p, i) )
2029 {
2030 pLuts[iLut].Type = 3;
2031 Gia_LutForEachFanin( p, i, iFan, k )
2032 pLuts[iLut].pFans[k] = Gia_ManObj(p, iFan)->Value;
2033 pLuts[iLut].nFans = k;
2034 *(word *)pLuts[iLut].pTruth = Gia_LutComputeTruth6(p, i, vTruths);
2035 pObj->Value = pLuts[iLut].Out = Abc_Var2Lit( iLut, 0 );
2036 iLut++;
2037 }
2038 // outputs
2039 Gia_ManForEachCo( p, pObj, i )
2040 {
2041 pLuts[iLut].Type = 2;
2042 pLuts[iLut].pFans[0] = Gia_ObjFanin0(pObj)->Value;
2043 if ( Gia_ObjFaninC0(pObj) ^ Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
2044 memset( pLuts[iLut].pTruth, 0x55, sizeof(unsigned) * nUints );
2045 else
2046 memset( pLuts[iLut].pTruth, 0xAA, sizeof(unsigned) * nUints );
2047 pLuts[iLut].nFans = 1;
2048 pObj->Value = pLuts[iLut].Out = Abc_Var2Lit( iLut, 0 );
2049 iLut++;
2050 }
2051 assert( iLut == nLuts );
2052 // dump into a file
2053 {
2054 FILE * pFile = fopen( pFileName, "wb" );
2055 if ( pFile == NULL )
2056 printf( "Cannot open file \"%s\" for writing.\n", pFileName );
2057 else
2058 {
2059 int nSize1 = nLuts * sizeof(Gia_MapLut_t);
2060 int nSize2 = fwrite( pLuts, 1, nSize1, pFile );
2061 assert( nSize1 == nSize2 );
2062 printf( "Successfully dumped %d bytes of binary data.\n", nSize1 );
2063 }
2064 fclose( pFile );
2065 }
2066 ABC_FREE( pLuts );
2067 Vec_WrdFree( vTruths );
2068 }
2069
2070 /**Function*************************************************************
2071
2072 Synopsis []
2073
2074 Description []
2075
2076 SideEffects []
2077
2078 SeeAlso []
2079
2080 ***********************************************************************/
Gia_DumpLutSizeDistrib(Gia_Man_t * p,char * pFileName)2081 void Gia_DumpLutSizeDistrib( Gia_Man_t * p, char * pFileName )
2082 {
2083 FILE * pTable = fopen( pFileName, "a+" );
2084 int i, Counts[10] = {0};
2085 Gia_ManForEachLut( p, i )
2086 if ( Gia_ObjLutSize(p, i) > 0 && Gia_ObjLutSize(p, i) < 10 )
2087 Counts[ Gia_ObjLutSize(p, i) ]++;
2088 fprintf( pTable, "%s", p->pName );
2089 for ( i = 1; i < 10; i++ )
2090 fprintf( pTable, " %d", Counts[i] );
2091 fprintf( pTable, "\n" );
2092 fclose( pTable );
2093 }
2094
2095 /**Function*************************************************************
2096
2097 Synopsis [Check if two logic cones have overlap.]
2098
2099 Description []
2100
2101 SideEffects []
2102
2103 SeeAlso []
2104
2105 ***********************************************************************/
Gia_ManCheckSuppMark_rec(Gia_Man_t * p,Gia_Obj_t * pObj)2106 void Gia_ManCheckSuppMark_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
2107 {
2108 if ( pObj->fMark0 )
2109 return;
2110 pObj->fMark0 = 1;
2111 if ( Gia_ObjIsCi(pObj) )
2112 return;
2113 Gia_ManCheckSuppMark_rec( p, Gia_ObjFanin0(pObj) );
2114 Gia_ManCheckSuppMark_rec( p, Gia_ObjFanin1(pObj) );
2115 }
Gia_ManCheckSuppUnmark_rec(Gia_Man_t * p,Gia_Obj_t * pObj)2116 void Gia_ManCheckSuppUnmark_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
2117 {
2118 if ( !pObj->fMark0 )
2119 return;
2120 pObj->fMark0 = 0;
2121 if ( Gia_ObjIsCi(pObj) )
2122 return;
2123 Gia_ManCheckSuppUnmark_rec( p, Gia_ObjFanin0(pObj) );
2124 Gia_ManCheckSuppUnmark_rec( p, Gia_ObjFanin1(pObj) );
2125 }
Gia_ManCheckSupp_rec(Gia_Man_t * p,Gia_Obj_t * pObj)2126 int Gia_ManCheckSupp_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
2127 {
2128 if ( pObj->fMark0 )
2129 return 1;
2130 if ( Gia_ObjIsCi(pObj) )
2131 return 0;
2132 if ( Gia_ManCheckSupp_rec( p, Gia_ObjFanin0(pObj) ) )
2133 return 1;
2134 return Gia_ManCheckSupp_rec( p, Gia_ObjFanin1(pObj) );
2135 }
Gia_ManCheckSuppOverlap(Gia_Man_t * p,int iNode1,int iNode2)2136 int Gia_ManCheckSuppOverlap( Gia_Man_t * p, int iNode1, int iNode2 )
2137 {
2138 int Result;
2139 if ( iNode1 == 0 || iNode2 == 0 )
2140 return 0;
2141 Gia_ManCheckSuppMark_rec( p, Gia_ManObj(p, iNode1) );
2142 Result = Gia_ManCheckSupp_rec( p, Gia_ManObj(p, iNode2) );
2143 Gia_ManCheckSuppUnmark_rec( p, Gia_ManObj(p, iNode1) );
2144 return Result;
2145 }
2146
2147
2148 /**Function*************************************************************
2149
2150 Synopsis [Count PIs with fanout.]
2151
2152 Description []
2153
2154 SideEffects []
2155
2156 SeeAlso []
2157
2158 ***********************************************************************/
Gia_ManCountPisWithFanout(Gia_Man_t * p)2159 int Gia_ManCountPisWithFanout( Gia_Man_t * p )
2160 {
2161 Gia_Obj_t * pObj;
2162 int i, Count = 0;
2163 Gia_ManForEachCi( p, pObj, i )
2164 pObj->fMark0 = 0;
2165 Gia_ManForEachAnd( p, pObj, i )
2166 {
2167 Gia_ObjFanin0(pObj)->fMark0 = 1;
2168 Gia_ObjFanin1(pObj)->fMark0 = 1;
2169 }
2170 Gia_ManForEachCo( p, pObj, i )
2171 Gia_ObjFanin0(pObj)->fMark0 = 1;
2172 Gia_ManForEachCi( p, pObj, i )
2173 Count += pObj->fMark0;
2174 Gia_ManForEachObj( p, pObj, i )
2175 pObj->fMark0 = 0;
2176 return Count;
2177 }
2178
2179 /**Function*************************************************************
2180
2181 Synopsis [Count POs driven by non-zero driver.]
2182
2183 Description []
2184
2185 SideEffects []
2186
2187 SeeAlso []
2188
2189 ***********************************************************************/
Gia_ManCountPosWithNonZeroDrivers(Gia_Man_t * p)2190 int Gia_ManCountPosWithNonZeroDrivers( Gia_Man_t * p )
2191 {
2192 Gia_Obj_t * pObj;
2193 int i, Count = 0;
2194 Gia_ManForEachCo( p, pObj, i )
2195 Count += Gia_ObjFaninLit0(pObj, Gia_ObjId(p, pObj)) != 0;
2196 return Count;
2197 }
2198
2199 /**Function*************************************************************
2200
2201 Synopsis []
2202
2203 Description []
2204
2205 SideEffects []
2206
2207 SeeAlso []
2208
2209 ***********************************************************************/
Gia_ManUpdateCopy(Vec_Int_t * vCopy,Gia_Man_t * p)2210 void Gia_ManUpdateCopy( Vec_Int_t * vCopy, Gia_Man_t * p )
2211 {
2212 Gia_Obj_t * pObj;
2213 int i, iLit;
2214 Vec_IntForEachEntry( vCopy, iLit, i )
2215 {
2216 if ( iLit == -1 )
2217 continue;
2218 pObj = Gia_ManObj( p, Abc_Lit2Var(iLit) );
2219 if ( !~pObj->Value )
2220 Vec_IntWriteEntry( vCopy, i, -1 );
2221 else
2222 Vec_IntWriteEntry( vCopy, i, Abc_LitNotCond(pObj->Value, Abc_LitIsCompl(iLit)) );
2223 }
2224 }
2225
2226 /**Function*************************************************************
2227
2228 Synopsis []
2229
2230 Description []
2231
2232 SideEffects []
2233
2234 SeeAlso []
2235
2236 ***********************************************************************/
Gia_ManDupWithMuxPos(Gia_Man_t * p)2237 Gia_Man_t * Gia_ManDupWithMuxPos( Gia_Man_t * p )
2238 {
2239 Vec_Int_t * vPoints = Vec_IntAlloc( 1000 );
2240 Vec_Int_t * vQuads = Vec_IntAlloc( 1000 );
2241 Vec_Bit_t * vHeads = Vec_BitStart( Gia_ManObjNum(p) );
2242 Vec_Bit_t * vDatas = Vec_BitStart( Gia_ManObjNum(p) );
2243 Gia_Obj_t * pObj, * pCtrl, * pData0, * pData1;
2244 Gia_Man_t * pNew = Gia_ManDup( p ); int i, iObj;
2245 assert( Gia_ManRegNum(pNew) == 0 );
2246 Gia_ManForEachAnd( pNew, pObj, i )
2247 {
2248 if ( !Gia_ObjIsMuxType(pObj) )
2249 continue;
2250 pCtrl = Gia_ObjRecognizeMux( pObj, &pData1, &pData0 );
2251 pCtrl = Gia_Regular(pCtrl);
2252 pData0 = Gia_Regular(pData0);
2253 pData1 = Gia_Regular(pData1);
2254 Vec_IntPushTwo( vQuads, Gia_ObjId(pNew, pObj), Gia_ObjId(pNew, pCtrl) );
2255 Vec_IntPushTwo( vQuads, Gia_ObjId(pNew, pData0), Gia_ObjId(pNew, pData1) );
2256 Vec_BitWriteEntry( vHeads, Gia_ObjId(pNew, pObj), 1 );
2257 Vec_BitWriteEntry( vDatas, Gia_ObjId(pNew, pData0), 1 );
2258 Vec_BitWriteEntry( vDatas, Gia_ObjId(pNew, pData1), 1 );
2259 }
2260 Gia_ManForEachCo( pNew, pObj, i )
2261 Gia_ObjFanin0(pObj)->fMark0 = 1;
2262 for ( i = 0; i < Vec_IntSize(vQuads)/4; i++ )
2263 {
2264 int iObj = Vec_IntEntry( vQuads, 4*i+0 );
2265 int iCtrl = Vec_IntEntry( vQuads, 4*i+1 );
2266 int iData0 = Vec_IntEntry( vQuads, 4*i+2 );
2267 int iData1 = Vec_IntEntry( vQuads, 4*i+3 );
2268 if ( (Vec_BitEntry(vHeads, iObj) && Vec_BitEntry(vDatas, iObj)) ||
2269 (Vec_BitEntry(vHeads, iData0) && Vec_BitEntry(vDatas, iData0)) ||
2270 (Vec_BitEntry(vHeads, iData1) && Vec_BitEntry(vDatas, iData1)) )
2271 {
2272 Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
2273 Gia_Obj_t * pCtrl = Gia_ManObj( p, iCtrl );
2274 Gia_Obj_t * pData0 = Gia_ManObj( p, iData0 );
2275 Gia_Obj_t * pData1 = Gia_ManObj( p, iData1 );
2276 if ( Gia_ObjIsAnd(pObj) && !pObj->fMark0 ) Vec_IntPush( vPoints, iObj );
2277 if ( Gia_ObjIsAnd(pCtrl) && !pCtrl->fMark0 ) Vec_IntPush( vPoints, iCtrl );
2278 if ( Gia_ObjIsAnd(pData0) && !pData0->fMark0 ) Vec_IntPush( vPoints, iData0 );
2279 if ( Gia_ObjIsAnd(pData1) && !pData1->fMark0 ) Vec_IntPush( vPoints, iData1 );
2280 }
2281 }
2282 Gia_ManCleanMark0( pNew );
2283 Vec_IntUniqify( vPoints );
2284 Vec_IntForEachEntry( vPoints, iObj, i )
2285 Gia_ManAppendCo( pNew, Abc_Var2Lit(iObj, 0) );
2286 Vec_IntFree( vPoints );
2287 Vec_IntFree( vQuads );
2288 Vec_BitFree( vHeads );
2289 Vec_BitFree( vDatas );
2290 return pNew;
2291 }
2292
2293
2294 ////////////////////////////////////////////////////////////////////////
2295 /// END OF FILE ///
2296 ////////////////////////////////////////////////////////////////////////
2297
2298
2299 ABC_NAMESPACE_IMPL_END
2300
2301