abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaUtil.c
Go to the documentation of this file.
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 ***********************************************************************/
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 }
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 ***********************************************************************/
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 ***********************************************************************/
101 char * Gia_TimeStamp()
102 {
103  static char Buffer[100];
104  char * TimeStamp;
105  time_t ltime;
106  // get the current time
107  time( &ltime );
108  TimeStamp = asctime( localtime( &ltime ) );
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 }
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ( 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 }
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 ***********************************************************************/
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 }
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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  Gia_ObjFanin1(pObj)->Value++;
698  }
699  else if ( Gia_ObjIsCo(pObj) )
700  Gia_ObjFanin0(pObj)->Value++;
701  }
702 }
703 
704 /**Function*************************************************************
705 
706  Synopsis [Assigns references.]
707 
708  Description []
709 
710  SideEffects []
711 
712  SeeAlso []
713 
714 ***********************************************************************/
715 void Gia_ManCreateRefs( Gia_Man_t * p )
716 {
717  Gia_Obj_t * pObj;
718  int i;
719  assert( p->pRefs == NULL );
720  p->pRefs = ABC_CALLOC( int, Gia_ManObjNum(p) );
721  Gia_ManForEachObj( p, pObj, i )
722  {
723  if ( Gia_ObjIsAnd(pObj) )
724  {
725  Gia_ObjRefFanin0Inc( p, pObj );
726  Gia_ObjRefFanin1Inc( p, pObj );
727  if ( Gia_ObjIsMuxId(p, i) )
728  Gia_ObjRefFanin2Inc( p, pObj );
729  }
730  else if ( Gia_ObjIsCo(pObj) )
731  Gia_ObjRefFanin0Inc( p, pObj );
732  }
733 }
734 
735 /**Function*************************************************************
736 
737  Synopsis [Assigns references.]
738 
739  Description []
740 
741  SideEffects []
742 
743  SeeAlso []
744 
745 ***********************************************************************/
746 int * Gia_ManCreateMuxRefs( Gia_Man_t * p )
747 {
748  Gia_Obj_t * pObj, * pCtrl, * pFan0, * pFan1;
749  int i, * pMuxRefs;
750  pMuxRefs = ABC_CALLOC( int, Gia_ManObjNum(p) );
751  Gia_ManForEachObj( p, pObj, i )
752  {
753  if ( Gia_ObjRecognizeExor( pObj, &pFan0, &pFan1 ) )
754  continue;
755  if ( !Gia_ObjIsMuxType(pObj) )
756  continue;
757  pCtrl = Gia_ObjRecognizeMux( pObj, &pFan0, &pFan1 );
758  pMuxRefs[ Gia_ObjId(p, Gia_Regular(pCtrl)) ]++;
759  }
760  return pMuxRefs;
761 }
762 
763 /**Function*************************************************************
764 
765  Synopsis [Computes the maximum frontier size.]
766 
767  Description []
768 
769  SideEffects []
770 
771  SeeAlso []
772 
773 ***********************************************************************/
774 void Gia_ManDfsForCrossCut_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
775 {
776  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
777  return;
778  Gia_ObjSetTravIdCurrent(p, pObj);
779  if ( Gia_ObjIsCi(pObj) )
780  {
781  Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
782  return;
783  }
784  if ( Gia_ObjIsCo(pObj) )
785  {
786  Gia_ObjFanin0(pObj)->Value++;
787  Gia_ManDfsForCrossCut_rec( p, Gia_ObjFanin0(pObj), vNodes );
788  Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
789  return;
790  }
791  assert( Gia_ObjIsAnd(pObj) );
792  Gia_ObjFanin0(pObj)->Value++;
793  Gia_ObjFanin1(pObj)->Value++;
794  Gia_ManDfsForCrossCut_rec( p, Gia_ObjFanin0(pObj), vNodes );
795  Gia_ManDfsForCrossCut_rec( p, Gia_ObjFanin1(pObj), vNodes );
796  Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
797 }
798 Vec_Int_t * Gia_ManDfsForCrossCut( Gia_Man_t * p, int fReverse )
799 {
800  Vec_Int_t * vNodes;
801  Gia_Obj_t * pObj;
802  int i;
803  Gia_ManCleanValue( p );
804  vNodes = Vec_IntAlloc( Gia_ManObjNum(p) );
805  Gia_ManIncrementTravId( p );
806  if ( fReverse )
807  {
808  Gia_ManForEachCoReverse( p, pObj, i )
809  if ( !Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
810  Gia_ManDfsForCrossCut_rec( p, pObj, vNodes );
811  }
812  else
813  {
814  Gia_ManForEachCo( p, pObj, i )
815  if ( !Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
816  Gia_ManDfsForCrossCut_rec( p, pObj, vNodes );
817  }
818  return vNodes;
819 }
820 int Gia_ManCrossCut( Gia_Man_t * p, int fReverse )
821 {
822  Vec_Int_t * vNodes;
823  Gia_Obj_t * pObj;
824  int i, nCutCur = 0, nCutMax = 0;
825  vNodes = Gia_ManDfsForCrossCut( p, fReverse );
826  Gia_ManForEachObjVec( vNodes, p, pObj, i )
827  {
828  if ( pObj->Value )
829  nCutCur++;
830  if ( nCutMax < nCutCur )
831  nCutMax = nCutCur;
832  if ( Gia_ObjIsAnd(pObj) )
833  {
834  if ( --Gia_ObjFanin0(pObj)->Value == 0 )
835  nCutCur--;
836  if ( --Gia_ObjFanin1(pObj)->Value == 0 )
837  nCutCur--;
838  }
839  else if ( Gia_ObjIsCo(pObj) )
840  {
841  if ( --Gia_ObjFanin0(pObj)->Value == 0 )
842  nCutCur--;
843  }
844  }
845  Vec_IntFree( vNodes );
846  Gia_ManForEachObj( p, pObj, i )
847  assert( pObj->Value == 0 );
848  return nCutMax;
849 }
850 
851 
852 /**Function*************************************************************
853 
854  Synopsis [Collects PO Ids into one array.]
855 
856  Description []
857 
858  SideEffects []
859 
860  SeeAlso []
861 
862 ***********************************************************************/
863 Vec_Int_t * Gia_ManCollectPoIds( Gia_Man_t * p )
864 {
865  Vec_Int_t * vStart;
866  int Entry, i;
867  vStart = Vec_IntAlloc( Gia_ManPoNum(p) );
868  Vec_IntForEachEntryStop( p->vCos, Entry, i, Gia_ManPoNum(p) )
869  Vec_IntPush( vStart, Entry );
870  return vStart;
871 }
872 
873 
874 /**Function*************************************************************
875 
876  Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
877 
878  Description []
879 
880  SideEffects []
881 
882  SeeAlso []
883 
884 ***********************************************************************/
885 int Gia_ObjIsMuxType( Gia_Obj_t * pNode )
886 {
887  Gia_Obj_t * pNode0, * pNode1;
888  // check that the node is regular
889  assert( !Gia_IsComplement(pNode) );
890  // if the node is not AND, this is not MUX
891  if ( !Gia_ObjIsAnd(pNode) || Gia_ObjIsBuf(pNode) )
892  return 0;
893  // if the children are not complemented, this is not MUX
894  if ( !Gia_ObjFaninC0(pNode) || !Gia_ObjFaninC1(pNode) )
895  return 0;
896  // get children
897  pNode0 = Gia_ObjFanin0(pNode);
898  pNode1 = Gia_ObjFanin1(pNode);
899  // if the children are not ANDs, this is not MUX
900  if ( !Gia_ObjIsAnd(pNode0) || !Gia_ObjIsAnd(pNode1) )
901  return 0;
902  // otherwise the node is MUX iff it has a pair of equal grandchildren
903  return (Gia_ObjFanin0(pNode0) == Gia_ObjFanin0(pNode1) && (Gia_ObjFaninC0(pNode0) ^ Gia_ObjFaninC0(pNode1))) ||
904  (Gia_ObjFanin0(pNode0) == Gia_ObjFanin1(pNode1) && (Gia_ObjFaninC0(pNode0) ^ Gia_ObjFaninC1(pNode1))) ||
905  (Gia_ObjFanin1(pNode0) == Gia_ObjFanin0(pNode1) && (Gia_ObjFaninC1(pNode0) ^ Gia_ObjFaninC0(pNode1))) ||
906  (Gia_ObjFanin1(pNode0) == Gia_ObjFanin1(pNode1) && (Gia_ObjFaninC1(pNode0) ^ Gia_ObjFaninC1(pNode1)));
907 }
908 
909 
910 /**Function*************************************************************
911 
912  Synopsis [Recognizes what nodes are inputs of the EXOR.]
913 
914  Description []
915 
916  SideEffects []
917 
918  SeeAlso []
919 
920 ***********************************************************************/
921 int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ppFan0, Gia_Obj_t ** ppFan1 )
922 {
923  Gia_Obj_t * p0, * p1;
924  assert( !Gia_IsComplement(pObj) );
925  if ( !Gia_ObjIsAnd(pObj) || Gia_ObjIsBuf(pObj) )
926  return 0;
927  assert( Gia_ObjIsAnd(pObj) );
928  p0 = Gia_ObjChild0(pObj);
929  p1 = Gia_ObjChild1(pObj);
930  if ( !Gia_IsComplement(p0) || !Gia_IsComplement(p1) )
931  return 0;
932  p0 = Gia_Regular(p0);
933  p1 = Gia_Regular(p1);
934  if ( !Gia_ObjIsAnd(p0) || !Gia_ObjIsAnd(p1) )
935  return 0;
936  if ( Gia_ObjFanin0(p0) != Gia_ObjFanin0(p1) || Gia_ObjFanin1(p0) != Gia_ObjFanin1(p1) )
937  return 0;
938  if ( Gia_ObjFaninC0(p0) == Gia_ObjFaninC0(p1) || Gia_ObjFaninC1(p0) == Gia_ObjFaninC1(p1) )
939  return 0;
940  *ppFan0 = Gia_ObjChild0(p0);
941  *ppFan1 = Gia_ObjChild1(p0);
942  return 1;
943 }
944 
945 /**Function*************************************************************
946 
947  Synopsis [Recognizes what nodes are control and data inputs of a MUX.]
948 
949  Description [If the node is a MUX, returns the control variable C.
950  Assigns nodes T and E to be the then and else variables of the MUX.
951  Node C is never complemented. Nodes T and E can be complemented.
952  This function also recognizes EXOR/NEXOR gates as MUXes.]
953 
954  SideEffects []
955 
956  SeeAlso []
957 
958 ***********************************************************************/
959 Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE )
960 {
961  Gia_Obj_t * pNode0, * pNode1;
962  assert( !Gia_IsComplement(pNode) );
963  assert( Gia_ObjIsMuxType(pNode) );
964  // get children
965  pNode0 = Gia_ObjFanin0(pNode);
966  pNode1 = Gia_ObjFanin1(pNode);
967 
968  // find the control variable
969  if ( Gia_ObjFanin1(pNode0) == Gia_ObjFanin1(pNode1) && (Gia_ObjFaninC1(pNode0) ^ Gia_ObjFaninC1(pNode1)) )
970  {
971 // if ( FrGia_IsComplement(pNode1->p2) )
972  if ( Gia_ObjFaninC1(pNode0) )
973  { // pNode2->p2 is positive phase of C
974  *ppNodeT = Gia_Not(Gia_ObjChild0(pNode1));//pNode2->p1);
975  *ppNodeE = Gia_Not(Gia_ObjChild0(pNode0));//pNode1->p1);
976  return Gia_ObjChild1(pNode1);//pNode2->p2;
977  }
978  else
979  { // pNode1->p2 is positive phase of C
980  *ppNodeT = Gia_Not(Gia_ObjChild0(pNode0));//pNode1->p1);
981  *ppNodeE = Gia_Not(Gia_ObjChild0(pNode1));//pNode2->p1);
982  return Gia_ObjChild1(pNode0);//pNode1->p2;
983  }
984  }
985  else if ( Gia_ObjFanin0(pNode0) == Gia_ObjFanin0(pNode1) && (Gia_ObjFaninC0(pNode0) ^ Gia_ObjFaninC0(pNode1)) )
986  {
987 // if ( FrGia_IsComplement(pNode1->p1) )
988  if ( Gia_ObjFaninC0(pNode0) )
989  { // pNode2->p1 is positive phase of C
990  *ppNodeT = Gia_Not(Gia_ObjChild1(pNode1));//pNode2->p2);
991  *ppNodeE = Gia_Not(Gia_ObjChild1(pNode0));//pNode1->p2);
992  return Gia_ObjChild0(pNode1);//pNode2->p1;
993  }
994  else
995  { // pNode1->p1 is positive phase of C
996  *ppNodeT = Gia_Not(Gia_ObjChild1(pNode0));//pNode1->p2);
997  *ppNodeE = Gia_Not(Gia_ObjChild1(pNode1));//pNode2->p2);
998  return Gia_ObjChild0(pNode0);//pNode1->p1;
999  }
1000  }
1001  else if ( Gia_ObjFanin0(pNode0) == Gia_ObjFanin1(pNode1) && (Gia_ObjFaninC0(pNode0) ^ Gia_ObjFaninC1(pNode1)) )
1002  {
1003 // if ( FrGia_IsComplement(pNode1->p1) )
1004  if ( Gia_ObjFaninC0(pNode0) )
1005  { // pNode2->p2 is positive phase of C
1006  *ppNodeT = Gia_Not(Gia_ObjChild0(pNode1));//pNode2->p1);
1007  *ppNodeE = Gia_Not(Gia_ObjChild1(pNode0));//pNode1->p2);
1008  return Gia_ObjChild1(pNode1);//pNode2->p2;
1009  }
1010  else
1011  { // pNode1->p1 is positive phase of C
1012  *ppNodeT = Gia_Not(Gia_ObjChild1(pNode0));//pNode1->p2);
1013  *ppNodeE = Gia_Not(Gia_ObjChild0(pNode1));//pNode2->p1);
1014  return Gia_ObjChild0(pNode0);//pNode1->p1;
1015  }
1016  }
1017  else if ( Gia_ObjFanin1(pNode0) == Gia_ObjFanin0(pNode1) && (Gia_ObjFaninC1(pNode0) ^ Gia_ObjFaninC0(pNode1)) )
1018  {
1019 // if ( FrGia_IsComplement(pNode1->p2) )
1020  if ( Gia_ObjFaninC1(pNode0) )
1021  { // pNode2->p1 is positive phase of C
1022  *ppNodeT = Gia_Not(Gia_ObjChild1(pNode1));//pNode2->p2);
1023  *ppNodeE = Gia_Not(Gia_ObjChild0(pNode0));//pNode1->p1);
1024  return Gia_ObjChild0(pNode1);//pNode2->p1;
1025  }
1026  else
1027  { // pNode1->p2 is positive phase of C
1028  *ppNodeT = Gia_Not(Gia_ObjChild0(pNode0));//pNode1->p1);
1029  *ppNodeE = Gia_Not(Gia_ObjChild1(pNode1));//pNode2->p2);
1030  return Gia_ObjChild1(pNode0);//pNode1->p2;
1031  }
1032  }
1033  assert( 0 ); // this is not MUX
1034  return NULL;
1035 }
1036 int Gia_ObjRecognizeMuxLits( Gia_Man_t * p, Gia_Obj_t * pNode, int * iLitT, int * iLitE )
1037 {
1038  Gia_Obj_t * pNodeT, * pNodeE;
1039  Gia_Obj_t * pCtrl = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
1040  assert( pCtrl != NULL );
1041  *iLitT = Gia_Obj2Lit( p, pNodeT );
1042  *iLitE = Gia_Obj2Lit( p, pNodeE );
1043  return Gia_Obj2Lit( p, pCtrl );
1044 }
1045 
1046 
1047 /**Function*************************************************************
1048 
1049  Synopsis [Dereferences the node's MFFC.]
1050 
1051  Description []
1052 
1053  SideEffects []
1054 
1055  SeeAlso []
1056 
1057 ***********************************************************************/
1058 int Gia_NodeDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
1059 {
1060  Gia_Obj_t * pFanin;
1061  int Counter = 0;
1062  if ( Gia_ObjIsCi(pNode) )
1063  return 0;
1064  assert( Gia_ObjIsAnd(pNode) );
1065  pFanin = Gia_ObjFanin0(pNode);
1066  assert( Gia_ObjRefNum(p, pFanin) > 0 );
1067  if ( Gia_ObjRefDec(p, pFanin) == 0 )
1068  Counter += Gia_NodeDeref_rec( p, pFanin );
1069  pFanin = Gia_ObjFanin1(pNode);
1070  assert( Gia_ObjRefNum(p, pFanin) > 0 );
1071  if ( Gia_ObjRefDec(p, pFanin) == 0 )
1072  Counter += Gia_NodeDeref_rec( p, pFanin );
1073  return Counter + 1;
1074 }
1075 
1076 /**Function*************************************************************
1077 
1078  Synopsis [References the node's MFFC.]
1079 
1080  Description []
1081 
1082  SideEffects []
1083 
1084  SeeAlso []
1085 
1086 ***********************************************************************/
1087 int Gia_NodeRef_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
1088 {
1089  Gia_Obj_t * pFanin;
1090  int Counter = 0;
1091  if ( Gia_ObjIsCi(pNode) )
1092  return 0;
1093  assert( Gia_ObjIsAnd(pNode) );
1094  pFanin = Gia_ObjFanin0(pNode);
1095  if ( Gia_ObjRefInc(p, pFanin) == 0 )
1096  Counter += Gia_NodeRef_rec( p, pFanin );
1097  pFanin = Gia_ObjFanin1(pNode);
1098  if ( Gia_ObjRefInc(p, pFanin) == 0 )
1099  Counter += Gia_NodeRef_rec( p, pFanin );
1100  return Counter + 1;
1101 }
1102 
1103 
1104 /**Function*************************************************************
1105 
1106  Synopsis [References the node's MFFC.]
1107 
1108  Description []
1109 
1110  SideEffects []
1111 
1112  SeeAlso []
1113 
1114 ***********************************************************************/
1115 int Gia_ManPoMffcSize( Gia_Man_t * p )
1116 {
1117  Gia_ManCreateRefs( p );
1118  return Gia_NodeDeref_rec( p, Gia_ObjFanin0(Gia_ManPo(p, 0)) );
1119 }
1120 
1121 /**Function*************************************************************
1122 
1123  Synopsis [Returns the number of internal nodes in the MFFC.]
1124 
1125  Description []
1126 
1127  SideEffects []
1128 
1129  SeeAlso []
1130 
1131 ***********************************************************************/
1132 int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode )
1133 {
1134  int ConeSize1, ConeSize2;
1135  assert( !Gia_IsComplement(pNode) );
1136  assert( Gia_ObjIsCand(pNode) );
1137  ConeSize1 = Gia_NodeDeref_rec( p, pNode );
1138  ConeSize2 = Gia_NodeRef_rec( p, pNode );
1139  assert( ConeSize1 == ConeSize2 );
1140  assert( ConeSize1 >= 0 );
1141  return ConeSize1;
1142 }
1143 
1144 /**Function*************************************************************
1145 
1146  Synopsis [Returns 1 if AIG has dangling nodes.]
1147 
1148  Description []
1149 
1150  SideEffects []
1151 
1152  SeeAlso []
1153 
1154 ***********************************************************************/
1155 int Gia_ManHasDangling( Gia_Man_t * p )
1156 {
1157  Gia_Obj_t * pObj;
1158  int i, Counter = 0;
1159  Gia_ManForEachObj( p, pObj, i )
1160  {
1161  pObj->fMark0 = 0;
1162  if ( Gia_ObjIsCo(pObj) )
1163  Gia_ObjFanin0(pObj)->fMark0 = 1;
1164  else if ( Gia_ObjIsMux(p, pObj) )
1165  {
1166  Gia_ObjFanin0(pObj)->fMark0 = 1;
1167  Gia_ObjFanin1(pObj)->fMark0 = 1;
1168  Gia_ObjFanin2(p, pObj)->fMark0 = 1;
1169  }
1170  else if ( Gia_ObjIsAnd(pObj) )
1171  {
1172  Gia_ObjFanin0(pObj)->fMark0 = 1;
1173  Gia_ObjFanin1(pObj)->fMark0 = 1;
1174  }
1175  }
1176  Gia_ManForEachAnd( p, pObj, i )
1177  Counter += !pObj->fMark0;
1178  Gia_ManCleanMark0( p );
1179  return Counter;
1180 }
1181 
1182 /**Function*************************************************************
1183 
1184  Synopsis [Returns 1 if AIG has dangling nodes.]
1185 
1186  Description []
1187 
1188  SideEffects []
1189 
1190  SeeAlso []
1191 
1192 ***********************************************************************/
1193 int Gia_ManMarkDangling( Gia_Man_t * p )
1194 {
1195  Gia_Obj_t * pObj;
1196  int i, Counter = 0;
1197  Gia_ManForEachObj( p, pObj, i )
1198  {
1199  pObj->fMark0 = 0;
1200  if ( Gia_ObjIsAnd(pObj) )
1201  {
1202  Gia_ObjFanin0(pObj)->fMark0 = 1;
1203  Gia_ObjFanin1(pObj)->fMark0 = 1;
1204  }
1205  else if ( Gia_ObjIsCo(pObj) )
1206  Gia_ObjFanin0(pObj)->fMark0 = 1;
1207  }
1208  Gia_ManForEachAnd( p, pObj, i )
1209  Counter += !pObj->fMark0;
1210  return Counter;
1211 }
1212 
1213 /**Function*************************************************************
1214 
1215  Synopsis [Returns 1 if AIG has dangling nodes.]
1216 
1217  Description []
1218 
1219  SideEffects []
1220 
1221  SeeAlso []
1222 
1223 ***********************************************************************/
1224 Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p )
1225 {
1226  Vec_Int_t * vDangles;
1227  Gia_Obj_t * pObj;
1228  int i;
1229  Gia_ManForEachObj( p, pObj, i )
1230  {
1231  pObj->fMark0 = 0;
1232  if ( Gia_ObjIsAnd(pObj) )
1233  {
1234  Gia_ObjFanin0(pObj)->fMark0 = 1;
1235  Gia_ObjFanin1(pObj)->fMark0 = 1;
1236  }
1237  else if ( Gia_ObjIsCo(pObj) )
1238  Gia_ObjFanin0(pObj)->fMark0 = 1;
1239  }
1240  vDangles = Vec_IntAlloc( 100 );
1241  Gia_ManForEachAnd( p, pObj, i )
1242  if ( !pObj->fMark0 )
1243  Vec_IntPush( vDangles, i );
1244  Gia_ManCleanMark0( p );
1245  return vDangles;
1246 }
1247 /**Function*************************************************************
1248 
1249  Synopsis [Verbose printing of the AIG node.]
1250 
1251  Description []
1252 
1253  SideEffects []
1254 
1255  SeeAlso []
1256 
1257 ***********************************************************************/
1258 void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj )
1259 {
1260  if ( pObj == NULL )
1261  {
1262  printf( "Object is NULL." );
1263  return;
1264  }
1265  if ( Gia_IsComplement(pObj) )
1266  {
1267  printf( "Compl " );
1268  pObj = Gia_Not(pObj);
1269  }
1270  assert( !Gia_IsComplement(pObj) );
1271  printf( "Obj %4d : ", Gia_ObjId(p, pObj) );
1272  if ( Gia_ObjIsConst0(pObj) )
1273  printf( "constant 0" );
1274  else if ( Gia_ObjIsPi(p, pObj) )
1275  printf( "PI" );
1276  else if ( Gia_ObjIsPo(p, pObj) )
1277  printf( "PO( %4d%s )", Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " ") );
1278  else if ( Gia_ObjIsCi(pObj) )
1279  printf( "RO( %4d%s )", Gia_ObjFaninId0p(p, Gia_ObjRoToRi(p, pObj)), (Gia_ObjFaninC0(Gia_ObjRoToRi(p, pObj))? "\'" : " ") );
1280  else if ( Gia_ObjIsCo(pObj) )
1281  printf( "RI( %4d%s )", Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " ") );
1282 // else if ( Gia_ObjIsBuf(pObj) )
1283 // printf( "BUF( %d%s )", Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " ") );
1284  else if ( Gia_ObjIsXor(pObj) )
1285  printf( "XOR( %4d%s, %4d%s )",
1286  Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " "),
1287  Gia_ObjFaninId1p(p, pObj), (Gia_ObjFaninC1(pObj)? "\'" : " ") );
1288  else if ( Gia_ObjIsMuxId(p, Gia_ObjId(p, pObj)) )
1289  printf( "MUX( %4d%s, %4d%s, %4d%s )",
1290  Gia_ObjFaninId2p(p, pObj), (Gia_ObjFaninC2(p, pObj)? "\'" : " "),
1291  Gia_ObjFaninId1p(p, pObj), (Gia_ObjFaninC1(pObj)? "\'" : " "),
1292  Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " ") );
1293  else
1294  printf( "AND( %4d%s, %4d%s )",
1295  Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " "),
1296  Gia_ObjFaninId1p(p, pObj), (Gia_ObjFaninC1(pObj)? "\'" : " ") );
1297  if ( p->pRefs )
1298  printf( " (refs = %3d)", Gia_ObjRefNum(p, pObj) );
1299  if ( pObj->fMark0 )
1300  printf( " mark0" );
1301  if ( pObj->fMark1 )
1302  printf( " mark1" );
1303  printf( "\n" );
1304 /*
1305  if ( p->pRefs )
1306  {
1307  Gia_Obj_t * pFanout;
1308  int i;
1309  int iFan = -1; // Suppress "might be used uninitialized"
1310  printf( "\nFanouts:\n" );
1311  Gia_ObjForEachFanout( p, pObj, pFanout, iFan, i )
1312  {
1313  printf( " " );
1314  printf( "Node %4d : ", Gia_ObjId(pFanout) );
1315  if ( Gia_ObjIsPo(pFanout) )
1316  printf( "PO( %4d%s )", Gia_ObjFanin0(pFanout)->Id, (Gia_ObjFaninC0(pFanout)? "\'" : " ") );
1317  else if ( Gia_ObjIsBuf(pFanout) )
1318  printf( "BUF( %d%s )", Gia_ObjFanin0(pFanout)->Id, (Gia_ObjFaninC0(pFanout)? "\'" : " ") );
1319  else
1320  printf( "AND( %4d%s, %4d%s )",
1321  Gia_ObjFanin0(pFanout)->Id, (Gia_ObjFaninC0(pFanout)? "\'" : " "),
1322  Gia_ObjFanin1(pFanout)->Id, (Gia_ObjFaninC1(pFanout)? "\'" : " ") );
1323  printf( "\n" );
1324  }
1325  return;
1326  }
1327 */
1328 }
1329 void Gia_ManPrint( Gia_Man_t * p )
1330 {
1331  Gia_Obj_t * pObj;
1332  int i;
1333  printf( "GIA manager has %d ANDs, %d XORs, %d MUXes.\n",
1334  Gia_ManAndNum(p) - Gia_ManXorNum(p) - Gia_ManMuxNum(p), Gia_ManXorNum(p), Gia_ManMuxNum(p) );
1335  Gia_ManForEachObj( p, pObj, i )
1336  Gia_ObjPrint( p, pObj );
1337 }
1338 void Gia_ManPrintCo_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
1339 {
1340  if ( Gia_ObjIsAnd(pObj) )
1341  {
1342  Gia_ManPrintCo_rec( p, Gia_ObjFanin0(pObj) );
1343  Gia_ManPrintCo_rec( p, Gia_ObjFanin1(pObj) );
1344  if ( Gia_ObjIsMux(p, pObj) )
1345  Gia_ManPrintCo_rec( p, Gia_ObjFanin2(p, pObj) );
1346  }
1347  Gia_ObjPrint( p, pObj );
1348 }
1349 void Gia_ManPrintCo( Gia_Man_t * p, Gia_Obj_t * pObj )
1350 {
1351  assert( Gia_ObjIsCo(pObj) );
1352  printf( "TFI cone of CO number %d:\n", Gia_ObjCioId(pObj) );
1353  Gia_ManPrintCo_rec( p, Gia_ObjFanin0(pObj) );
1354  Gia_ObjPrint( p, pObj );
1355 }
1356 
1357 void Gia_ManPrintCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
1358 {
1359  if ( Vec_IntFind(vNodes, Gia_ObjId(p, pObj)) >= 0 )
1360  return;
1361  assert( Gia_ObjIsAnd(pObj) );
1362  Gia_ManPrintCollect_rec( p, Gia_ObjFanin0(pObj), vNodes );
1363  Gia_ManPrintCollect_rec( p, Gia_ObjFanin1(pObj), vNodes );
1364  if ( Gia_ObjIsMux(p, pObj) )
1365  Gia_ManPrintCollect_rec( p, Gia_ObjFanin2(p, pObj), vNodes );
1366  Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
1367 }
1368 void Gia_ManPrintCone( Gia_Man_t * p, Gia_Obj_t * pObj, int * pLeaves, int nLeaves, Vec_Int_t * vNodes )
1369 {
1370  int i;
1371  Vec_IntClear( vNodes );
1372  for ( i = 0; i < nLeaves; i++ )
1373  Vec_IntPush( vNodes, pLeaves[i] );
1374  Gia_ManPrintCollect_rec( p, pObj, vNodes );
1375  printf( "GIA logic cone for node %d:\n", Gia_ObjId(p, pObj) );
1376  Gia_ManForEachObjVec( vNodes, p, pObj, i )
1377  Gia_ObjPrint( p, pObj );
1378 }
1379 
1380 void Gia_ManPrintCollect2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
1381 {
1382  if ( Vec_IntFind(vNodes, Gia_ObjId(p, pObj)) >= 0 )
1383  return;
1384  if ( Gia_ObjIsCo(pObj) || Gia_ObjIsAnd(pObj) )
1385  Gia_ManPrintCollect2_rec( p, Gia_ObjFanin0(pObj), vNodes );
1386  if ( Gia_ObjIsAnd(pObj) )
1387  Gia_ManPrintCollect2_rec( p, Gia_ObjFanin1(pObj), vNodes );
1388  if ( Gia_ObjIsMux(p, pObj) )
1389  Gia_ManPrintCollect2_rec( p, Gia_ObjFanin2(p, pObj), vNodes );
1390  Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
1391 }
1392 void Gia_ManPrintCone2( Gia_Man_t * p, Gia_Obj_t * pObj )
1393 {
1394  Vec_Int_t * vNodes;
1395  int i;
1396  vNodes = Vec_IntAlloc( 100 );
1397  Gia_ManPrintCollect2_rec( p, pObj, vNodes );
1398  printf( "GIA logic cone for node %d:\n", Gia_ObjId(p, pObj) );
1399  Gia_ManForEachObjVec( vNodes, p, pObj, i )
1400  Gia_ObjPrint( p, pObj );
1401  Vec_IntFree( vNodes );
1402 }
1403 
1404 /**Function*************************************************************
1405 
1406  Synopsis [Complements the constraint outputs.]
1407 
1408  Description []
1409 
1410  SideEffects []
1411 
1412  SeeAlso []
1413 
1414 ***********************************************************************/
1415 void Gia_ManInvertConstraints( Gia_Man_t * pAig )
1416 {
1417  Gia_Obj_t * pObj;
1418  int i;
1419  if ( Gia_ManConstrNum(pAig) == 0 )
1420  return;
1421  Gia_ManForEachPo( pAig, pObj, i )
1422  if ( i >= Gia_ManPoNum(pAig) - Gia_ManConstrNum(pAig) )
1423  Gia_ObjFlipFaninC0( pObj );
1424 }
1425 void Gia_ManInvertPos( Gia_Man_t * pAig )
1426 {
1427  Gia_Obj_t * pObj;
1428  int i;
1429  Gia_ManForEachPo( pAig, pObj, i )
1430  Gia_ObjFlipFaninC0( pObj );
1431 }
1432 
1433 /**Function*************************************************************
1434 
1435  Synopsis [Testing the speedup due to grouping POs into batches.]
1436 
1437  Description []
1438 
1439  SideEffects []
1440 
1441  SeeAlso []
1442 
1443 ***********************************************************************/
1444 void Gia_ManCollectObjs_rec( Gia_Man_t * p, int iObjId, Vec_Int_t * vObjs, int Limit )
1445 {
1446  Gia_Obj_t * pObj;
1447  if ( Vec_IntSize(vObjs) == Limit )
1448  return;
1449  if ( Gia_ObjIsTravIdCurrentId(p, iObjId) )
1450  return;
1451  Gia_ObjSetTravIdCurrentId(p, iObjId);
1452  pObj = Gia_ManObj( p, iObjId );
1453  if ( Gia_ObjIsAnd(pObj) )
1454  {
1455  Gia_ManCollectObjs_rec( p, Gia_ObjFaninId0p(p, pObj), vObjs, Limit );
1456  if ( Vec_IntSize(vObjs) == Limit )
1457  return;
1458  Gia_ManCollectObjs_rec( p, Gia_ObjFaninId1p(p, pObj), vObjs, Limit );
1459  if ( Vec_IntSize(vObjs) == Limit )
1460  return;
1461  }
1462  Vec_IntPush( vObjs, iObjId );
1463 }
1464 unsigned * Gia_ManComputePoTruthTables( Gia_Man_t * p, int nBytesMax )
1465 {
1466  int nVars = Gia_ManPiNum(p);
1467  int nTruthWords = Abc_TruthWordNum( nVars );
1468  int nTruths = nBytesMax / (sizeof(unsigned) * nTruthWords);
1469  int nTotalNodes = 0, nRounds = 0;
1470  Vec_Int_t * vObjs;
1471  Gia_Obj_t * pObj;
1472  abctime clk = Abc_Clock();
1473  int i;
1474  printf( "Var = %d. Words = %d. Truths = %d.\n", nVars, nTruthWords, nTruths );
1475  vObjs = Vec_IntAlloc( nTruths );
1476  Gia_ManIncrementTravId( p );
1477  Gia_ManForEachPo( p, pObj, i )
1478  {
1479  Gia_ManCollectObjs_rec( p, Gia_ObjFaninId0p(p, pObj), vObjs, nTruths );
1480  if ( Vec_IntSize(vObjs) == nTruths )
1481  {
1482  nRounds++;
1483 // printf( "%d ", i );
1484  nTotalNodes += Vec_IntSize( vObjs );
1485  Vec_IntClear( vObjs );
1486  Gia_ManIncrementTravId( p );
1487  }
1488  }
1489 // printf( "\n" );
1490  nTotalNodes += Vec_IntSize( vObjs );
1491  Vec_IntFree( vObjs );
1492 
1493  printf( "Rounds = %d. Objects = %d. Total = %d. ", nRounds, Gia_ManObjNum(p), nTotalNodes );
1494  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1495 
1496  return NULL;
1497 }
1498 
1499 
1500 /**Function*************************************************************
1501 
1502  Synopsis [Returns 1 if the manager are structural identical.]
1503 
1504  Description []
1505 
1506  SideEffects []
1507 
1508  SeeAlso []
1509 
1510 ***********************************************************************/
1511 int Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 )
1512 {
1513  Gia_Obj_t * pObj1, * pObj2;
1514  int i;
1515  if ( Gia_ManObjNum(p1) != Gia_ManObjNum(p2) )
1516  {
1517  printf( "AIGs have different number of objects.\n" );
1518  return 0;
1519  }
1520  Gia_ManCleanValue( p1 );
1521  Gia_ManCleanValue( p2 );
1522  Gia_ManForEachObj( p1, pObj1, i )
1523  {
1524  pObj2 = Gia_ManObj( p2, i );
1525  if ( memcmp( pObj1, pObj2, sizeof(Gia_Obj_t) ) )
1526  {
1527  printf( "Objects %d are different.\n", i );
1528  return 0;
1529  }
1530  if ( p1->pReprs && p2->pReprs )
1531  {
1532  if ( memcmp( &p1->pReprs[i], &p2->pReprs[i], sizeof(Gia_Rpr_t) ) )
1533  {
1534  printf( "Representatives of objects %d are different.\n", i );
1535  return 0;
1536  }
1537  }
1538  }
1539  return 1;
1540 }
1541 
1542 /**Function*************************************************************
1543 
1544  Synopsis [Marks nodes that appear as faninis of other nodes.]
1545 
1546  Description []
1547 
1548  SideEffects []
1549 
1550  SeeAlso []
1551 
1552 ***********************************************************************/
1553 void Gia_ManMarkFanoutDrivers( Gia_Man_t * p )
1554 {
1555  Gia_Obj_t * pObj;
1556  int i;
1557  Gia_ManForEachObj( p, pObj, i )
1558  {
1559  pObj->fMark0 = 0;
1560  if ( Gia_ObjIsAnd(pObj) )
1561  {
1562  Gia_ObjFanin0(pObj)->fMark0 = 1;
1563  Gia_ObjFanin1(pObj)->fMark0 = 1;
1564  }
1565  else if ( Gia_ObjIsCo(pObj) )
1566  Gia_ObjFanin0(pObj)->fMark0 = 1;
1567  }
1568 }
1569 
1570 
1571 /**Function*************************************************************
1572 
1573  Synopsis [Swaps PO number 0 with PO number i.]
1574 
1575  Description []
1576 
1577  SideEffects []
1578 
1579  SeeAlso []
1580 
1581 ***********************************************************************/
1582 void Gia_ManSwapPos( Gia_Man_t * p, int i )
1583 {
1584  int Lit0, LitI;
1585  assert( i >= 0 && i < Gia_ManPoNum(p) );
1586  if ( i == 0 )
1587  return;
1588  Lit0 = Gia_ObjFaninLit0p( p, Gia_ManPo(p, 0) );
1589  LitI = Gia_ObjFaninLit0p( p, Gia_ManPo(p, i) );
1590  Gia_ManPatchCoDriver( p, 0, LitI );
1591  Gia_ManPatchCoDriver( p, i, Lit0 );
1592 }
1593 
1594 /**Function*************************************************************
1595 
1596  Synopsis [Save/load value from file.]
1597 
1598  Description []
1599 
1600  SideEffects []
1601 
1602  SeeAlso []
1603 
1604 ***********************************************************************/
1605 Vec_Int_t * Gia_ManSaveValue( Gia_Man_t * p )
1606 {
1607  Vec_Int_t * vValues;
1608  Gia_Obj_t * pObj;
1609  int i;
1610  vValues = Vec_IntAlloc( Gia_ManObjNum(p) );
1611  Gia_ManForEachObj( p, pObj, i )
1612  Vec_IntPush( vValues, pObj->Value );
1613  return vValues;
1614 }
1615 void Gia_ManLoadValue( Gia_Man_t * p, Vec_Int_t * vValues )
1616 {
1617  Gia_Obj_t * pObj;
1618  int i;
1619  Gia_ManForEachObj( p, pObj, i )
1620  pObj->Value = Vec_IntEntry(vValues, i);
1621 }
1622 
1623 
1624 /**Function*************************************************************
1625 
1626  Synopsis [Returns the array containing the first fanout of each object.]
1627 
1628  Description []
1629 
1630  SideEffects []
1631 
1632  SeeAlso []
1633 
1634 ***********************************************************************/
1635 Vec_Int_t * Gia_ManFirstFanouts( Gia_Man_t * p )
1636 {
1637  Vec_Int_t * vFans = Vec_IntStart( Gia_ManObjNum(p) );
1638  Gia_Obj_t * pObj;
1639  int i;
1640  Gia_ManForEachObj( p, pObj, i )
1641  {
1642  if ( Gia_ObjIsAnd(pObj) )
1643  {
1644  if ( Vec_IntEntry(vFans, Gia_ObjFaninId0p(p, pObj)) == 0 )
1645  Vec_IntWriteEntry(vFans, Gia_ObjFaninId0p(p, pObj), i);
1646  if ( Vec_IntEntry(vFans, Gia_ObjFaninId1p(p, pObj)) == 0 )
1647  Vec_IntWriteEntry(vFans, Gia_ObjFaninId1p(p, pObj), i);
1648  if ( Gia_ObjIsMuxId(p, i) && Vec_IntEntry(vFans, Gia_ObjFaninId2p(p, pObj)) == 0 )
1649  Vec_IntWriteEntry(vFans, Gia_ObjFaninId2p(p, pObj), i);
1650  }
1651  else if ( Gia_ObjIsCo(pObj) )
1652  {
1653  if ( Vec_IntEntry(vFans, Gia_ObjFaninId0p(p, pObj)) == 0 )
1654  Vec_IntWriteEntry(vFans, Gia_ObjFaninId0p(p, pObj), i);
1655  }
1656  }
1657  return vFans;
1658 }
1659 
1660 /**Function*************************************************************
1661 
1662  Synopsis [Returns 1 if AIG has choices.]
1663 
1664  Description []
1665 
1666  SideEffects []
1667 
1668  SeeAlso []
1669 
1670 ***********************************************************************/
1671 int Gia_ManHasChoices_very_old( Gia_Man_t * p )
1672 {
1673  Gia_Obj_t * pObj;
1674  int i, Counter1 = 0, Counter2 = 0;
1675  int nFailNoRepr = 0;
1676  int nFailHaveRepr = 0;
1677  int nChoiceNodes = 0;
1678  int nChoices = 0;
1679  if ( p->pReprs == NULL || p->pNexts == NULL )
1680  return 0;
1681  // check if there are any representatives
1682  Gia_ManForEachObj( p, pObj, i )
1683  {
1684  if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
1685  {
1686 // printf( "%d ", i );
1687  Counter1++;
1688  }
1689 // if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
1690 // Counter2++;
1691  }
1692 // printf( "\n" );
1693  Gia_ManForEachObj( p, pObj, i )
1694  {
1695 // if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
1696 // Counter1++;
1697  if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
1698  {
1699 // printf( "%d ", i );
1700  Counter2++;
1701  }
1702  }
1703 // printf( "\n" );
1704  if ( Counter1 == 0 )
1705  {
1706  printf( "Warning: AIG has repr data-strucure but not reprs.\n" );
1707  return 0;
1708  }
1709  printf( "%d nodes have reprs.\n", Counter1 );
1710  printf( "%d nodes have nexts.\n", Counter2 );
1711  // check if there are any internal nodes without fanout
1712  // make sure all nodes without fanout have representatives
1713  // make sure all nodes with fanout have no representatives
1714  ABC_FREE( p->pRefs );
1715  Gia_ManCreateRefs( p );
1716  Gia_ManForEachAnd( p, pObj, i )
1717  {
1718  if ( Gia_ObjRefNum(p, pObj) == 0 )
1719  {
1720  if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) == NULL )
1721  nFailNoRepr++;
1722  else
1723  nChoices++;
1724  }
1725  else
1726  {
1727  if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) != NULL )
1728  nFailHaveRepr++;
1729  if ( Gia_ObjNextObj( p, Gia_ObjId(p, pObj) ) != NULL )
1730  nChoiceNodes++;
1731  }
1732  if ( Gia_ObjReprObj( p, i ) )
1733  assert( Gia_ObjRepr(p, i) < i );
1734  }
1735  if ( nChoices == 0 )
1736  return 0;
1737  if ( nFailNoRepr )
1738  {
1739  printf( "Gia_ManHasChoices_very_old(): Error: %d internal nodes have no fanout and no repr.\n", nFailNoRepr );
1740 // return 0;
1741  }
1742  if ( nFailHaveRepr )
1743  {
1744  printf( "Gia_ManHasChoices_very_old(): Error: %d internal nodes have both fanout and repr.\n", nFailHaveRepr );
1745 // return 0;
1746  }
1747 // printf( "Gia_ManHasChoices_very_old(): AIG has %d choice nodes with %d choices.\n", nChoiceNodes, nChoices );
1748  return 1;
1749 }
1750 
1751 
1752 /**Function*************************************************************
1753 
1754  Synopsis [Proving multi-output properties.]
1755 
1756  Description []
1757 
1758  SideEffects []
1759 
1760  SeeAlso []
1761 
1762 ***********************************************************************/
1763 Vec_Int_t * Gia_ManGroupProve( Gia_Man_t * pInit, char * pCommLine, int nGroupSize, int fVerbose )
1764 {
1765  Abc_Frame_t * pAbc = Abc_FrameReadGlobalFrame();
1766  Gia_Man_t * p = Gia_ManDup( pInit );
1767  Gia_Man_t * pGroup;
1768  Vec_Int_t * vOuts;
1769  Vec_Int_t * vOutMap;
1770  Vec_Ptr_t * vCexes;
1771  int i, k, nGroupCur, nGroups;
1772  abctime clk, timeComm = 0;
1773  abctime timeStart = Abc_Clock();
1774  // pre-conditions
1775  assert( nGroupSize > 0 );
1776  assert( pCommLine != NULL );
1777  assert( p->nConstrs == 0 );
1778  Abc_Print( 1, "RUNNING MultiProve: Group size = %d. Command line = \"%s\".\n", nGroupSize, pCommLine );
1779  // create output map
1780  vOuts = Vec_IntStartNatural( Gia_ManPoNum(p) );
1781  vOutMap = Vec_IntAlloc( Gia_ManPoNum(p) );
1782  vCexes = Vec_PtrAlloc( Gia_ManPoNum(p) );
1783  nGroups = Gia_ManPoNum(p) / nGroupSize + (int)((Gia_ManPoNum(p) % nGroupSize) > 0);
1784  for ( i = 0; i < nGroups; i++ )
1785  {
1786  // derive the group
1787  nGroupCur = ((i + 1) * nGroupSize < Gia_ManPoNum(p)) ? nGroupSize : Gia_ManPoNum(p) - i * nGroupSize;
1788  pGroup = Gia_ManDupCones( p, Vec_IntArray(vOuts) + i * nGroupSize, nGroupCur, 0 );
1789  Abc_Print( 1, "GROUP %4d : %4d <= PoId < %4d : ", i, i * nGroupSize, i * nGroupSize + nGroupCur );
1790  // set the current GIA
1791  Abc_FrameUpdateGia( pAbc, pGroup );
1792  // solve the group
1793  clk = Abc_Clock();
1794  Cmd_CommandExecute( pAbc, pCommLine );
1795  timeComm += Abc_Clock() - clk;
1796  // get the solution status
1797  if ( nGroupSize == 1 )
1798  {
1799  Vec_IntPush( vOutMap, Abc_FrameReadProbStatus(pAbc) );
1800  Vec_PtrPush( vCexes, Abc_FrameReadCex(pAbc) );
1801  }
1802  else // if ( nGroupSize > 1 )
1803  {
1804  Vec_Int_t * vStatusCur = Abc_FrameReadPoStatuses( pAbc );
1805  Vec_Ptr_t * vCexesCur = Abc_FrameReadCexVec( pAbc );
1806  assert( vStatusCur != NULL ); // only works for "bmc3" and "pdr"
1807 // assert( vCexesCur != NULL );
1808  for ( k = 0; k < nGroupCur; k++ )
1809  {
1810  Vec_IntPush( vOutMap, Vec_IntEntry(vStatusCur, k) );
1811  Vec_PtrPush( vCexes, vCexesCur ? Vec_PtrEntry(vCexesCur, k) : NULL );
1812  }
1813  }
1814  }
1815  assert( Vec_PtrSize(vCexes) == Gia_ManPoNum(p) );
1816  assert( Vec_IntSize(vOutMap) == Gia_ManPoNum(p) );
1817  // set CEXes
1818  if ( Vec_PtrCountZero(vCexes) < Vec_PtrSize(vCexes) )
1819  Abc_FrameReplaceCexVec( pAbc, &vCexes );
1820  else // there is no CEXes
1821  Vec_PtrFree( vCexes );
1822  // report the result
1823  Abc_Print( 1, "SUMMARY: " );
1824  Abc_Print( 1, "Properties = %6d. ", Gia_ManPoNum(p) );
1825  Abc_Print( 1, "UNSAT = %6d. ", Vec_IntCountEntry(vOutMap, 1) );
1826  Abc_Print( 1, "SAT = %6d. ", Vec_IntCountEntry(vOutMap, 0) );
1827  Abc_Print( 1, "UNDEC = %6d. ", Vec_IntCountEntry(vOutMap, -1) );
1828  Abc_Print( 1, "\n" );
1829  Abc_PrintTime( 1, "Command time", timeComm );
1830  Abc_PrintTime( 1, "Total time ", Abc_Clock() - timeStart );
1831  // cleanup
1832  Vec_IntFree( vOuts );
1833  Gia_ManStop( p );
1834  return vOutMap;
1835 }
1836 
1837 
1838 /**Function*************************************************************
1839 
1840  Synopsis []
1841 
1842  Description []
1843 
1844  SideEffects []
1845 
1846  SeeAlso []
1847 
1848 ***********************************************************************/
1849 Vec_Int_t * Gia_ManPoXSim( Gia_Man_t * p, int nFrames, int fVerbose )
1850 {
1851  Vec_Int_t * vRes;
1852  Gia_Obj_t * pObj;
1853  int f, k, nLeft = Gia_ManPoNum(p);
1854  vRes = Vec_IntAlloc( Gia_ManPoNum(p) );
1855  Vec_IntFill( vRes, Gia_ManPoNum(p), nFrames );
1856  Gia_ObjTerSimSet0( Gia_ManConst0(p) );
1857  Gia_ManForEachRi( p, pObj, k )
1858  Gia_ObjTerSimSet0( pObj );
1859  for ( f = 0; f < nFrames; f++ )
1860  {
1861  Gia_ManForEachPi( p, pObj, k )
1862  Gia_ObjTerSimSetX( pObj );
1863  Gia_ManForEachRo( p, pObj, k )
1864  Gia_ObjTerSimRo( p, pObj );
1865  Gia_ManForEachAnd( p, pObj, k )
1866  Gia_ObjTerSimAnd( pObj );
1867  Gia_ManForEachCo( p, pObj, k )
1868  Gia_ObjTerSimCo( pObj );
1869  if ( fVerbose )
1870  {
1871  Gia_ManForEachPo( p, pObj, k )
1872  Gia_ObjTerSimPrint( pObj );
1873  printf( "\n" );
1874  }
1875  Gia_ManForEachPo( p, pObj, k )
1876  if ( Vec_IntEntry(vRes, k) == nFrames && Gia_ObjTerSimGetX(pObj) )
1877  Vec_IntWriteEntry(vRes, k, f), nLeft--;
1878  if ( nLeft == 0 )
1879  break;
1880  }
1881  if ( fVerbose )
1882  {
1883  if ( nLeft == 0 )
1884  printf( "Simulation converged after %d frames.\n", f+1 );
1885  else
1886  printf( "Simulation terminated after %d frames.\n", nFrames );
1887  }
1888 // Vec_IntPrint( vRes );
1889  return vRes;
1890 }
1891 
1892 ////////////////////////////////////////////////////////////////////////
1893 /// END OF FILE ///
1894 ////////////////////////////////////////////////////////////////////////
1895 
1896 
1897 ABC_NAMESPACE_IMPL_END
1898 
memset
char * memset()
Gia_ManPatchCoDriver
static void Gia_ManPatchCoDriver(Gia_Man_t *p, int iCoIndex, int iLit0)
Definition: gia.h:739
Gia_ObjRefFanin2Inc
static void Gia_ObjRefFanin2Inc(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:526
Gia_ObjLevelId
static int Gia_ObjLevelId(Gia_Man_t *p, int Id)
Definition: gia.h:500
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Gia_ObjTerSimCo
static void Gia_ObjTerSimCo(Gia_Obj_t *pObj)
Definition: gia.h:797
Gia_ObjRefFanin0Inc
static void Gia_ObjRefFanin0Inc(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:524
Abc_FrameReplaceCexVec
void Abc_FrameReplaceCexVec(Abc_Frame_t *pAbc, Vec_Ptr_t **pvCexVec)
Definition: abc.c:515
Gia_ObjChild0
static Gia_Obj_t * Gia_ObjChild0(Gia_Obj_t *pObj)
Definition: gia.h:457
Gia_ManMuxNum
static int Gia_ManMuxNum(Gia_Man_t *p)
Definition: gia.h:391
Gia_ObjFaninC2
static int Gia_ObjFaninC2(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:453
Gia_ManMarkDangling
int Gia_ManMarkDangling(Gia_Man_t *p)
Definition: giaUtil.c:1193
Gia_ManDupCones
Gia_Man_t * Gia_ManDupCones(Gia_Man_t *p, int *pPos, int nPos, int fTrimPis)
Definition: giaDup.c:2691
Gia_ManCleanLevels
void Gia_ManCleanLevels(Gia_Man_t *p, int Size)
Definition: giaUtil.c:470
Gia_ObjTerSimRo
static void Gia_ObjTerSimRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:808
Gia_ManCollectPoIds
Vec_Int_t * Gia_ManCollectPoIds(Gia_Man_t *p)
Definition: giaUtil.c:863
Gia_ManCreateRefs
void Gia_ManCreateRefs(Gia_Man_t *p)
Definition: giaUtil.c:715
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Gia_ObjPhase
static int Gia_ObjPhase(Gia_Obj_t *pObj)
Definition: gia.h:415
Gia_ObjTerSimSet0
static void Gia_ObjTerSimSet0(Gia_Obj_t *pObj)
Definition: gia.h:770
Vec_IntForEachEntryStop
#define Vec_IntForEachEntryStop(vVec, Entry, i, Stop)
Definition: vecInt.h:58
Gia_ManSetPhasePattern
void Gia_ManSetPhasePattern(Gia_Man_t *p, Vec_Int_t *vCiValues)
Definition: giaUtil.c:386
Abc_FrameReadPoStatuses
ABC_DLL Vec_Int_t * Abc_FrameReadPoStatuses(Abc_Frame_t *p)
Definition: mainFrame.c:72
Gia_ManDup
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition: giaDup.c:552
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_ManInvertPos
void Gia_ManInvertPos(Gia_Man_t *pAig)
Definition: giaUtil.c:1425
Vec_PtrForEachEntryStart
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition: vecPtr.h:57
Gia_Man_t_::pTravIds
int * pTravIds
Definition: gia.h:153
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Gia_Man_t_::pNexts
int * pNexts
Definition: gia.h:122
Gia_ManPoNum
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
Abc_FrameReadCex
void * Abc_FrameReadCex(void *pAbc)
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Gia_ManRandomW
word Gia_ManRandomW(int fReset)
Definition: giaUtil.c:62
Gia_TimeStamp
char * Gia_TimeStamp()
Definition: giaUtil.c:101
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_IntCountEntry
static int Vec_IntCountEntry(Vec_Int_t *p, int Entry)
Definition: vecInt.h:1156
Gia_ObjRefFanin1Inc
static void Gia_ObjRefFanin1Inc(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:525
Cmd_CommandExecute
int Cmd_CommandExecute(void *pAbc, char *pCommandLine)
Gia_Regular
static Gia_Obj_t * Gia_Regular(Gia_Obj_t *p)
Definition: gia.h:377
Gia_ObjIsTravIdCurrent
static int Gia_ObjIsTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:533
Gia_ObjIsMuxType
int Gia_ObjIsMuxType(Gia_Obj_t *pNode)
Definition: giaUtil.c:885
NUMBER2
#define NUMBER2
Definition: giaUtil.c:32
Gia_ManPo
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
ABC_REALLOC
#define ABC_REALLOC(type, obj, num)
Definition: abc_global.h:233
Gia_ObjFaninLit0p
static int Gia_ObjFaninLit0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:469
Gia_ObjIsCand
static int Gia_ObjIsCand(Gia_Obj_t *pObj)
Definition: gia.h:429
Gia_ManGetCiLevels
Vec_Int_t * Gia_ManGetCiLevels(Gia_Man_t *p)
Definition: giaUtil.c:546
Gia_ManConstrNum
static int Gia_ManConstrNum(Gia_Man_t *p)
Definition: gia.h:395
Gia_ObjSetGateLevel
static void Gia_ObjSetGateLevel(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:509
Gia_ObjRecognizeExor
int Gia_ObjRecognizeExor(Gia_Obj_t *pObj, Gia_Obj_t **ppFan0, Gia_Obj_t **ppFan1)
Definition: giaUtil.c:921
Gia_ManPoMffcSize
int Gia_ManPoMffcSize(Gia_Man_t *p)
Definition: giaUtil.c:1115
Gia_ObjIsConst0
static int Gia_ObjIsConst0(Gia_Obj_t *pObj)
Definition: gia.h:430
Abc_FrameReadCexVec
ABC_DLL Vec_Ptr_t * Abc_FrameReadCexVec(Abc_Frame_t *p)
Definition: mainFrame.c:69
Gia_Man_t_::pObjs
Gia_Obj_t * pObjs
Definition: gia.h:103
Gia_ManSetPhase
void Gia_ManSetPhase(Gia_Man_t *p)
Definition: giaUtil.c:379
Gia_Man_t_::vCos
Vec_Int_t * vCos
Definition: gia.h:109
Gia_ObjFaninId1p
static int Gia_ObjFaninId1p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:464
Gia_ManLoadValue
void Gia_ManLoadValue(Gia_Man_t *p, Vec_Int_t *vValues)
Definition: giaUtil.c:1615
Vec_IntFind
static int Vec_IntFind(Vec_Int_t *p, int Entry)
Definition: vecInt.h:895
Gia_ManPrintCo
void Gia_ManPrintCo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaUtil.c:1349
Gia_ObjRefNum
static int Gia_ObjRefNum(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:521
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Gia_ManReverseLevel
Vec_Int_t * Gia_ManReverseLevel(Gia_Man_t *p)
Definition: giaUtil.c:595
Gia_ObjTerSimPrint
static void Gia_ObjTerSimPrint(Gia_Obj_t *pObj)
Definition: gia.h:817
Gia_ObjIsBuf
static int Gia_ObjIsBuf(Gia_Obj_t *pObj)
Definition: gia.h:427
Gia_ManCompare
int Gia_ManCompare(Gia_Man_t *p1, Gia_Man_t *p2)
Definition: giaUtil.c:1511
Gia_ManLevelNum
int Gia_ManLevelNum(Gia_Man_t *p)
Definition: giaUtil.c:505
Gia_ManCleanPhase
void Gia_ManCleanPhase(Gia_Man_t *p)
Definition: giaUtil.c:431
Gia_ManPrintCo_rec
void Gia_ManPrintCo_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaUtil.c:1338
Abc_TruthWordNum
static int Abc_TruthWordNum(int nVars)
Definition: abc_global.h:256
Gia_Obj_t_::fMark1
unsigned fMark1
Definition: gia.h:84
Gia_Man_t_::nLevels
int nLevels
Definition: gia.h:116
Gia_ManCheckCoPhase
int Gia_ManCheckCoPhase(Gia_Man_t *p)
Definition: giaUtil.c:450
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Gia_ManSetPhase1
void Gia_ManSetPhase1(Gia_Man_t *p)
Definition: giaUtil.c:409
Gia_Man_t_::nObjs
int nObjs
Definition: gia.h:101
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Vec_IntStartNatural
static Vec_Int_t * Vec_IntStartNatural(int nSize)
Definition: bblif.c:192
Gia_NodeMffcSize
int Gia_NodeMffcSize(Gia_Man_t *p, Gia_Obj_t *pNode)
Definition: giaUtil.c:1132
Gia_ObjTerSimGetX
static int Gia_ObjTerSimGetX(Gia_Obj_t *pObj)
Definition: gia.h:777
Gia_NodeRef_rec
int Gia_NodeRef_rec(Gia_Man_t *p, Gia_Obj_t *pNode)
Definition: giaUtil.c:1087
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Gia_Man_t_::pRefs
int * pRefs
Definition: gia.h:114
Gia_Obj_t_
Definition: gia.h:75
Abc_FrameReadProbStatus
int Abc_FrameReadProbStatus(void *pAbc)
Gia_ObjSetBufLevel
static void Gia_ObjSetBufLevel(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:505
Gia_ManSetLevels
int Gia_ManSetLevels(Gia_Man_t *p, Vec_Int_t *vCiLevels)
Definition: giaUtil.c:558
Gia_ManHasChoices_very_old
int Gia_ManHasChoices_very_old(Gia_Man_t *p)
Definition: giaUtil.c:1671
Gia_ObjChild1
static Gia_Obj_t * Gia_ObjChild1(Gia_Obj_t *pObj)
Definition: gia.h:458
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Gia_Not
static Gia_Obj_t * Gia_Not(Gia_Obj_t *p)
Definition: gia.h:378
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Gia_ManAndNum
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
Gia_ObjLevel
static int Gia_ObjLevel(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:501
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Gia_ManCreateValueRefs
void Gia_ManCreateValueRefs(Gia_Man_t *p)
Definition: giaUtil.c:687
Abc_Frame_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Frame_t_ Abc_Frame_t
INCLUDES ///.
Definition: base/main/main.h:39
Gia_ManCleanTruth
void Gia_ManCleanTruth(Gia_Man_t *p)
Definition: giaUtil.c:487
Gia_ManLevelAve
float Gia_ManLevelAve(Gia_Man_t *p)
Definition: giaUtil.c:525
Gia_ObjIsMuxId
static int Gia_ObjIsMuxId(Gia_Man_t *p, int iObj)
Definition: gia.h:424
Gia_ManRandomInfo
void Gia_ManRandomInfo(Vec_Ptr_t *vInfo, int iInputStart, int iWordStart, int iWordStop)
Definition: giaUtil.c:80
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Gia_Man_t_::nConstrs
int nConstrs
Definition: gia.h:117
Gia_Man_t_::vTruths
Vec_Int_t * vTruths
Definition: gia.h:139
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Gia_Man_t_::nTravIds
int nTravIds
Definition: gia.h:118
Gia_ManCleanValue
void Gia_ManCleanValue(Gia_Man_t *p)
Definition: giaUtil.c:310
Gia_ManRandom
unsigned Gia_ManRandom(int fReset)
FUNCTION DEFINITIONS ///.
Definition: giaUtil.c:49
Gia_ManPrintCollect2_rec
void Gia_ManPrintCollect2_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vNodes)
Definition: giaUtil.c:1380
Gia_ManCheckMark1
void Gia_ManCheckMark1(Gia_Man_t *p)
Definition: giaUtil.c:291
Gia_ObjFlipFaninC0
static void Gia_ObjFlipFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:472
Gia_ManSetMark1
void Gia_ManSetMark1(Gia_Man_t *p)
Definition: giaUtil.c:253
Gia_ManForEachAndReverse
#define Gia_ManForEachAndReverse(p, pObj, i)
Definition: gia.h:1010
Gia_ObjRoToRi
static Gia_Obj_t * Gia_ObjRoToRi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:446
Gia_ObjPrint
void Gia_ObjPrint(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaUtil.c:1258
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Gia_ObjSetTravIdCurrent
static void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
Gia_ObjRefInc
static int Gia_ObjRefInc(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:522
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Vec_IntFill
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
memcmp
int memcmp()
Vec_IntUpdateEntry
static void Vec_IntUpdateEntry(Vec_Int_t *p, int i, int Value)
Definition: vecInt.h:468
Gia_ObjIsXor
static int Gia_ObjIsXor(Gia_Obj_t *pObj)
Definition: gia.h:423
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Gia_ManRequiredLevel
Vec_Int_t * Gia_ManRequiredLevel(Gia_Man_t *p)
Definition: giaUtil.c:639
Gia_ManGroupProve
Vec_Int_t * Gia_ManGroupProve(Gia_Man_t *pInit, char *pCommLine, int nGroupSize, int fVerbose)
Definition: giaUtil.c:1763
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Counter
static int Counter
Definition: extraBddMisc.c:1877
Gia_ManCleanMark1
void Gia_ManCleanMark1(Gia_Man_t *p)
Definition: giaUtil.c:272
Gia_ManXorNum
static int Gia_ManXorNum(Gia_Man_t *p)
Definition: gia.h:390
Gia_ManSetMark0
void Gia_ManSetMark0(Gia_Man_t *p)
Definition: giaUtil.c:196
Gia_ManCreateMuxRefs
int * Gia_ManCreateMuxRefs(Gia_Man_t *p)
Definition: giaUtil.c:746
Gia_ManFirstFanouts
Vec_Int_t * Gia_ManFirstFanouts(Gia_Man_t *p)
Definition: giaUtil.c:1635
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
Gia_ObjNextObj
static Gia_Obj_t * Gia_ObjNextObj(Gia_Man_t *p, int Id)
Definition: gia.h:911
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Vec_PtrCountZero
static int Vec_PtrCountZero(Vec_Ptr_t *p)
Definition: vecPtr.h:343
Gia_ManDfsForCrossCut
Vec_Int_t * Gia_ManDfsForCrossCut(Gia_Man_t *p, int fReverse)
Definition: giaUtil.c:798
strcpy
char * strcpy()
Gia_ObjFanin2
static Gia_Obj_t * Gia_ObjFanin2(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:456
Gia_ObjIsTravIdCurrentId
static int Gia_ObjIsTravIdCurrentId(Gia_Man_t *p, int Id)
Definition: gia.h:536
NUMBER1
#define NUMBER1
DECLARATIONS ///.
Definition: giaUtil.c:31
Gia_NodeDeref_rec
int Gia_NodeDeref_rec(Gia_Man_t *p, Gia_Obj_t *pNode)
Definition: giaUtil.c:1058
Gia_ManPrint
void Gia_ManPrint(Gia_Man_t *p)
Definition: giaUtil.c:1329
Gia_ObjIsCo
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
Gia_ObjNext
static int Gia_ObjNext(Gia_Man_t *p, int Id)
Definition: gia.h:912
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Gia_ManSaveValue
Vec_Int_t * Gia_ManSaveValue(Gia_Man_t *p)
Definition: giaUtil.c:1605
Gia_ObjRefDec
static int Gia_ObjRefDec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:523
Gia_ManInvertConstraints
void Gia_ManInvertConstraints(Gia_Man_t *pAig)
Definition: giaUtil.c:1415
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Gia_ObjReprObj
static Gia_Obj_t * Gia_ObjReprObj(Gia_Man_t *p, int Id)
Definition: gia.h:886
Gia_ManCiNum
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
Gia_ManPoXSim
Vec_Int_t * Gia_ManPoXSim(Gia_Man_t *p, int nFrames, int fVerbose)
Definition: giaUtil.c:1849
Gia_ObjSetPhase
void Gia_ObjSetPhase(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaUtil.c:346
Gia_Obj_t_::fPhase
unsigned fPhase
Definition: gia.h:85
Gia_ManCleanMark01
void Gia_ManCleanMark01(Gia_Man_t *p)
Definition: giaUtil.c:177
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Gia_IsComplement
static int Gia_IsComplement(Gia_Obj_t *p)
Definition: gia.h:380
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Gia_ManComputeSlacks
Vec_Int_t * Gia_ManComputeSlacks(Gia_Man_t *p)
Definition: giaUtil.c:663
Gia_ObjSetCoLevel
static void Gia_ObjSetCoLevel(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:504
Gia_Obj_t_::fMark0
unsigned fMark0
Definition: gia.h:79
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_Man_t_
Definition: gia.h:95
Gia_ManCleanMark0
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition: giaUtil.c:215
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Gia_ManPrintCone2
void Gia_ManPrintCone2(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaUtil.c:1392
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
Gia_ManCheckMark0
void Gia_ManCheckMark0(Gia_Man_t *p)
Definition: giaUtil.c:234
Gia_ObjRecognizeMuxLits
int Gia_ObjRecognizeMuxLits(Gia_Man_t *p, Gia_Obj_t *pNode, int *iLitT, int *iLitE)
Definition: giaUtil.c:1036
Gia_ManMarkFanoutDrivers
void Gia_ManMarkFanoutDrivers(Gia_Man_t *p)
Definition: giaUtil.c:1553
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition: giaUtil.c:328
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Gia_ManPrintCone
void Gia_ManPrintCone(Gia_Man_t *p, Gia_Obj_t *pObj, int *pLeaves, int nLeaves, Vec_Int_t *vNodes)
Definition: giaUtil.c:1368
Gia_ObjFaninId0p
static int Gia_ObjFaninId0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:463
Gia_Man_t_::nTravIdsAlloc
int nTravIdsAlloc
Definition: gia.h:154
strcat
char * strcat()
Abc_FrameReadGlobalFrame
ABC_DLL Abc_Frame_t * Abc_FrameReadGlobalFrame()
Definition: mainFrame.c:616
Gia_ObjIsPo
static int Gia_ObjIsPo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:442
Gia_ManComputePoTruthTables
unsigned * Gia_ManComputePoTruthTables(Gia_Man_t *p, int nBytesMax)
Definition: giaUtil.c:1464
Gia_ObjRecognizeMux
Gia_Obj_t * Gia_ObjRecognizeMux(Gia_Obj_t *pNode, Gia_Obj_t **ppNodeT, Gia_Obj_t **ppNodeE)
Definition: giaUtil.c:959
Gia_ManCollectObjs_rec
void Gia_ManCollectObjs_rec(Gia_Man_t *p, int iObjId, Vec_Int_t *vObjs, int Limit)
Definition: giaUtil.c:1444
Gia_ObjFaninId2p
static int Gia_ObjFaninId2p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:465
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Abc_FrameUpdateGia
void Abc_FrameUpdateGia(Abc_Frame_t *pAbc, Gia_Man_t *pNew)
Definition: abc.c:616
Gia_ManCrossCut
int Gia_ManCrossCut(Gia_Man_t *p, int fReverse)
Definition: giaUtil.c:820
Gia_ManPrintCollect_rec
void Gia_ManPrintCollect_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vNodes)
Definition: giaUtil.c:1357
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition: giaUtil.c:149
Gia_Man_t_::pReprs
Gia_Rpr_t * pReprs
Definition: gia.h:121
assert
#define assert(ex)
Definition: util_old.h:213
strlen
int strlen()
Gia_ObjFaninId2
static int Gia_ObjFaninId2(Gia_Man_t *p, int ObjId)
Definition: gia.h:462
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Gia_Man_t_::vLevels
Vec_Int_t * vLevels
Definition: gia.h:115
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
Gia_ManSwapPos
void Gia_ManSwapPos(Gia_Man_t *p, int i)
Definition: giaUtil.c:1582
Gia_Rpr_t_
Definition: gia.h:56
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
strrchr
char * strrchr()
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_ObjIsCi
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Gia_ObjSetTravIdCurrentId
static void Gia_ObjSetTravIdCurrentId(Gia_Man_t *p, int Id)
Definition: gia.h:535
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
Gia_ObjFaninId1
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:461
Gia_ObjIsMux
static int Gia_ObjIsMux(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:425
Gia_ObjTerSimSetX
static void Gia_ObjTerSimSetX(Gia_Obj_t *pObj)
Definition: gia.h:772
Gia_ManForEachCoReverse
#define Gia_ManForEachCoReverse(p, pObj, i)
Definition: gia.h:1028
Gia_ManDfsForCrossCut_rec
void Gia_ManDfsForCrossCut_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vNodes)
Definition: giaUtil.c:774
Gia_ObjCioId
static int Gia_ObjCioId(Gia_Obj_t *pObj)
Definition: gia.h:411
Gia_Obj2Lit
static int Gia_Obj2Lit(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:433
Gia_ManGetDangling
Vec_Int_t * Gia_ManGetDangling(Gia_Man_t *p)
Definition: giaUtil.c:1224
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Gia_ObjRepr
static int Gia_ObjRepr(Gia_Man_t *p, int Id)
Definition: gia.h:887
Gia_ObjTerSimAnd
static void Gia_ObjTerSimAnd(Gia_Obj_t *pObj)
Definition: gia.h:785
Gia_FileNameGenericAppend
char * Gia_FileNameGenericAppend(char *pBase, char *pSuffix)
Definition: giaUtil.c:125
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Gia_ObjFaninId0
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
Gia_ObjIsPi
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441
Gia_ManCoNum
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
Gia_ObjSetLevel
static void Gia_ObjSetLevel(Gia_Man_t *p, Gia_Obj_t *pObj, int l)
Definition: gia.h:503
Gia_ManHasDangling
int Gia_ManHasDangling(Gia_Man_t *p)
Definition: giaUtil.c:1155