1 /**CFile****************************************************************
2 
3   FileName    [aigDfs.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [AIG package.]
8 
9   Synopsis    [DFS traversal procedures.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - April 28, 2007.]
16 
17   Revision    [$Id: aigDfs.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "aig.h"
22 #include "misc/tim/tim.h"
23 
24 ABC_NAMESPACE_IMPL_START
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 ///                        DECLARATIONS                              ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 ////////////////////////////////////////////////////////////////////////
32 ///                     FUNCTION DEFINITIONS                         ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 /**Function*************************************************************
36 
37   Synopsis    [Verifies that the objects are in a topo order.]
38 
39   Description []
40 
41   SideEffects []
42 
43   SeeAlso     []
44 
45 ***********************************************************************/
Aig_ManVerifyTopoOrder(Aig_Man_t * p)46 int Aig_ManVerifyTopoOrder( Aig_Man_t * p )
47 {
48     Aig_Obj_t * pObj, * pNext;
49     int i, k, iBox, iTerm1, nTerms;
50     Aig_ManSetCioIds( p );
51     Aig_ManIncrementTravId( p );
52     Aig_ManForEachObj( p, pObj, i )
53     {
54         if ( Aig_ObjIsNode(pObj) )
55         {
56             pNext = Aig_ObjFanin0(pObj);
57             if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
58             {
59                 printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id );
60                 return 0;
61             }
62             pNext = Aig_ObjFanin1(pObj);
63             if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
64             {
65                 printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id );
66                 return 0;
67             }
68         }
69         else if ( Aig_ObjIsCo(pObj) || Aig_ObjIsBuf(pObj) )
70         {
71             pNext = Aig_ObjFanin0(pObj);
72             if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
73             {
74                 printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id );
75                 return 0;
76             }
77         }
78         else if ( Aig_ObjIsCi(pObj) )
79         {
80             if ( p->pManTime )
81             {
82                 iBox = Tim_ManBoxForCi( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj) );
83                 if ( iBox >= 0 ) // this is not a true PI
84                 {
85                     iTerm1 = Tim_ManBoxInputFirst( (Tim_Man_t *)p->pManTime, iBox );
86                     nTerms = Tim_ManBoxInputNum( (Tim_Man_t *)p->pManTime, iBox );
87                     for ( k = 0; k < nTerms; k++ )
88                     {
89                         pNext = Aig_ManCo( p, iTerm1 + k );
90                         assert( Tim_ManBoxForCo( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pNext) ) == iBox );
91                         if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
92                         {
93                             printf( "Box %d has input %d that is not in a topological order.\n", iBox, pNext->Id );
94                             return 0;
95                         }
96                     }
97                 }
98             }
99         }
100         else if ( !Aig_ObjIsConst1(pObj) )
101             assert( 0 );
102         Aig_ObjSetTravIdCurrent( p, pObj );
103     }
104     Aig_ManCleanCioIds( p );
105     return 1;
106 }
107 
108 /**Function*************************************************************
109 
110   Synopsis    [Collects internal nodes in the DFS order.]
111 
112   Description []
113 
114   SideEffects []
115 
116   SeeAlso     []
117 
118 ***********************************************************************/
Aig_ManDfs_rec(Aig_Man_t * p,Aig_Obj_t * pObj,Vec_Ptr_t * vNodes)119 void Aig_ManDfs_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
120 {
121     if ( pObj == NULL )
122         return;
123     assert( !Aig_IsComplement(pObj) );
124     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
125         return;
126     Aig_ObjSetTravIdCurrent(p, pObj);
127     if ( p->pEquivs && Aig_ObjEquiv(p, pObj) )
128         Aig_ManDfs_rec( p, Aig_ObjEquiv(p, pObj), vNodes );
129     Aig_ManDfs_rec( p, Aig_ObjFanin0(pObj), vNodes );
130     Aig_ManDfs_rec( p, Aig_ObjFanin1(pObj), vNodes );
131     Vec_PtrPush( vNodes, pObj );
132 }
133 
134 /**Function*************************************************************
135 
136   Synopsis    [Collects objects of the AIG in the DFS order.]
137 
138   Description [Works with choice nodes.]
139 
140   SideEffects []
141 
142   SeeAlso     []
143 
144 ***********************************************************************/
Aig_ManDfs(Aig_Man_t * p,int fNodesOnly)145 Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p, int fNodesOnly )
146 {
147     Vec_Ptr_t * vNodes;
148     Aig_Obj_t * pObj;
149     int i;
150     Aig_ManIncrementTravId( p );
151     Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
152     // start the array of nodes
153     vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) );
154     // mark PIs if they should not be collected
155     if ( fNodesOnly )
156         Aig_ManForEachCi( p, pObj, i )
157             Aig_ObjSetTravIdCurrent( p, pObj );
158     else
159         Vec_PtrPush( vNodes, Aig_ManConst1(p) );
160     // collect nodes reachable in the DFS order
161     Aig_ManForEachCo( p, pObj, i )
162         Aig_ManDfs_rec( p, fNodesOnly? Aig_ObjFanin0(pObj): pObj, vNodes );
163     if ( fNodesOnly )
164         assert( Vec_PtrSize(vNodes) == Aig_ManNodeNum(p) );
165     else
166         assert( Vec_PtrSize(vNodes) == Aig_ManObjNum(p) );
167     return vNodes;
168 }
169 
170 /**Function*************************************************************
171 
172   Synopsis    [Collects internal nodes in the DFS order.]
173 
174   Description []
175 
176   SideEffects []
177 
178   SeeAlso     []
179 
180 ***********************************************************************/
Aig_ManDfsAll_rec(Aig_Man_t * p,Aig_Obj_t * pObj,Vec_Ptr_t * vNodes)181 void Aig_ManDfsAll_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
182 {
183     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
184         return;
185     Aig_ObjSetTravIdCurrent(p, pObj);
186     if ( Aig_ObjIsCi(pObj) )
187     {
188         Vec_PtrPush( vNodes, pObj );
189         return;
190     }
191     if ( Aig_ObjIsCo(pObj) )
192     {
193         Aig_ManDfsAll_rec( p, Aig_ObjFanin0(pObj), vNodes );
194         Vec_PtrPush( vNodes, pObj );
195         return;
196     }
197     assert( Aig_ObjIsNode(pObj) );
198     Aig_ManDfsAll_rec( p, Aig_ObjFanin0(pObj), vNodes );
199     Aig_ManDfsAll_rec( p, Aig_ObjFanin1(pObj), vNodes );
200     Vec_PtrPush( vNodes, pObj );
201 }
Aig_ManDfsArray(Aig_Man_t * p,Aig_Obj_t ** pNodes,int nNodes)202 Vec_Ptr_t * Aig_ManDfsArray( Aig_Man_t * p, Aig_Obj_t ** pNodes, int nNodes )
203 {
204     Vec_Ptr_t * vNodes;
205     int i;
206     Aig_ManIncrementTravId( p );
207     vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) );
208     // add constant
209     Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
210     Vec_PtrPush( vNodes, Aig_ManConst1(p) );
211     // collect nodes reachable in the DFS order
212     for ( i = 0; i < nNodes; i++ )
213         Aig_ManDfsAll_rec( p, pNodes[i], vNodes );
214     return vNodes;
215 }
216 
217 /**Function*************************************************************
218 
219   Synopsis    [Collects objects of the AIG in the DFS order.]
220 
221   Description []
222 
223   SideEffects []
224 
225   SeeAlso     []
226 
227 ***********************************************************************/
Aig_ManDfsAll(Aig_Man_t * p)228 Vec_Ptr_t * Aig_ManDfsAll( Aig_Man_t * p )
229 {
230     Vec_Ptr_t * vNodes;
231     Aig_Obj_t * pObj;
232     int i;
233     Aig_ManIncrementTravId( p );
234     vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) );
235     // add constant
236     Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
237     Vec_PtrPush( vNodes, Aig_ManConst1(p) );
238     // collect nodes reachable in the DFS order
239     Aig_ManForEachCo( p, pObj, i )
240         Aig_ManDfsAll_rec( p, pObj, vNodes );
241     Aig_ManForEachCi( p, pObj, i )
242         if ( !Aig_ObjIsTravIdCurrent(p, pObj) )
243             Vec_PtrPush( vNodes, pObj );
244     assert( Vec_PtrSize(vNodes) == Aig_ManObjNum(p) );
245     return vNodes;
246 }
247 
248 /**Function*************************************************************
249 
250   Synopsis    [Collects internal nodes in the DFS order.]
251 
252   Description []
253 
254   SideEffects []
255 
256   SeeAlso     []
257 
258 ***********************************************************************/
Aig_ManDfsPreorder_rec(Aig_Man_t * p,Aig_Obj_t * pObj,Vec_Ptr_t * vNodes)259 void Aig_ManDfsPreorder_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
260 {
261     if ( pObj == NULL )
262         return;
263     assert( !Aig_IsComplement(pObj) );
264     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
265         return;
266     Aig_ObjSetTravIdCurrent(p, pObj);
267     Vec_PtrPush( vNodes, pObj );
268     if ( p->pEquivs && Aig_ObjEquiv(p, pObj) )
269         Aig_ManDfs_rec( p, Aig_ObjEquiv(p, pObj), vNodes );
270     Aig_ManDfsPreorder_rec( p, Aig_ObjFanin0(pObj), vNodes );
271     Aig_ManDfsPreorder_rec( p, Aig_ObjFanin1(pObj), vNodes );
272 }
273 
274 /**Function*************************************************************
275 
276   Synopsis    [Collects objects of the AIG in the DFS order.]
277 
278   Description [Works with choice nodes.]
279 
280   SideEffects []
281 
282   SeeAlso     []
283 
284 ***********************************************************************/
Aig_ManDfsPreorder(Aig_Man_t * p,int fNodesOnly)285 Vec_Ptr_t * Aig_ManDfsPreorder( Aig_Man_t * p, int fNodesOnly )
286 {
287     Vec_Ptr_t * vNodes;
288     Aig_Obj_t * pObj;
289     int i;
290     Aig_ManIncrementTravId( p );
291     Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
292     // start the array of nodes
293     vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) );
294     // mark PIs if they should not be collected
295     if ( fNodesOnly )
296         Aig_ManForEachCi( p, pObj, i )
297             Aig_ObjSetTravIdCurrent( p, pObj );
298     else
299         Vec_PtrPush( vNodes, Aig_ManConst1(p) );
300     // collect nodes reachable in the DFS order
301     Aig_ManForEachCo( p, pObj, i )
302         Aig_ManDfsPreorder_rec( p, fNodesOnly? Aig_ObjFanin0(pObj): pObj, vNodes );
303     if ( fNodesOnly )
304         assert( Vec_PtrSize(vNodes) == Aig_ManNodeNum(p) );
305     else
306         assert( Vec_PtrSize(vNodes) == Aig_ManObjNum(p) );
307     return vNodes;
308 }
309 
310 /**Function*************************************************************
311 
312   Synopsis    [Levelizes the nodes.]
313 
314   Description []
315 
316   SideEffects []
317 
318   SeeAlso     []
319 
320 ***********************************************************************/
Aig_ManLevelize(Aig_Man_t * p)321 Vec_Vec_t * Aig_ManLevelize( Aig_Man_t * p )
322 {
323     Aig_Obj_t * pObj;
324     Vec_Vec_t * vLevels;
325     int nLevels, i;
326     nLevels = Aig_ManLevelNum( p );
327     vLevels = Vec_VecStart( nLevels + 1 );
328     Aig_ManForEachObj( p, pObj, i )
329     {
330         assert( (int)pObj->Level <= nLevels );
331         Vec_VecPush( vLevels, pObj->Level, pObj );
332     }
333     return vLevels;
334 }
335 
336 /**Function*************************************************************
337 
338   Synopsis    [Collects internal nodes and PIs in the DFS order.]
339 
340   Description []
341 
342   SideEffects []
343 
344   SeeAlso     []
345 
346 ***********************************************************************/
Aig_ManDfsNodes(Aig_Man_t * p,Aig_Obj_t ** ppNodes,int nNodes)347 Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes )
348 {
349     Vec_Ptr_t * vNodes;
350 //    Aig_Obj_t * pObj;
351     int i;
352     Aig_ManIncrementTravId( p );
353     // mark constant and PIs
354     Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
355 //    Aig_ManForEachCi( p, pObj, i )
356 //        Aig_ObjSetTravIdCurrent( p, pObj );
357     // go through the nodes
358     vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
359     for ( i = 0; i < nNodes; i++ )
360         if ( Aig_ObjIsCo(ppNodes[i]) )
361             Aig_ManDfs_rec( p, Aig_ObjFanin0(ppNodes[i]), vNodes );
362         else
363             Aig_ManDfs_rec( p, ppNodes[i], vNodes );
364     return vNodes;
365 }
366 
367 /**Function*************************************************************
368 
369   Synopsis    [Collects internal nodes in the DFS order.]
370 
371   Description []
372 
373   SideEffects []
374 
375   SeeAlso     []
376 
377 ***********************************************************************/
Aig_ManDfsChoices_rec(Aig_Man_t * p,Aig_Obj_t * pObj,Vec_Ptr_t * vNodes)378 void Aig_ManDfsChoices_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
379 {
380     if ( pObj == NULL )
381         return;
382     assert( !Aig_IsComplement(pObj) );
383     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
384         return;
385     assert( Aig_ObjIsNode(pObj) );
386     Aig_ManDfsChoices_rec( p, Aig_ObjFanin0(pObj), vNodes );
387     Aig_ManDfsChoices_rec( p, Aig_ObjFanin1(pObj), vNodes );
388     Aig_ManDfsChoices_rec( p, Aig_ObjEquiv(p, pObj), vNodes );
389     assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
390     Aig_ObjSetTravIdCurrent(p, pObj);
391     Vec_PtrPush( vNodes, pObj );
392 }
393 
394 /**Function*************************************************************
395 
396   Synopsis    [Collects internal nodes in the DFS order.]
397 
398   Description []
399 
400   SideEffects []
401 
402   SeeAlso     []
403 
404 ***********************************************************************/
Aig_ManDfsChoices(Aig_Man_t * p)405 Vec_Ptr_t * Aig_ManDfsChoices( Aig_Man_t * p )
406 {
407     Vec_Ptr_t * vNodes;
408     Aig_Obj_t * pObj;
409     int i, Counter = 0;
410 
411     Aig_ManForEachNode( p, pObj, i )
412     {
413         if ( Aig_ObjEquiv(p, pObj) == NULL )
414             continue;
415         Counter = 0;
416         for ( pObj = Aig_ObjEquiv(p, pObj) ; pObj; pObj = Aig_ObjEquiv(p, pObj) )
417             Counter++;
418 //        printf( "%d ", Counter );
419     }
420 //    printf( "\n" );
421 
422     assert( p->pEquivs != NULL );
423     Aig_ManIncrementTravId( p );
424     // mark constant and PIs
425     Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
426     Aig_ManForEachCi( p, pObj, i )
427         Aig_ObjSetTravIdCurrent( p, pObj );
428     // go through the nodes
429     vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
430     Aig_ManForEachCo( p, pObj, i )
431         Aig_ManDfsChoices_rec( p, Aig_ObjFanin0(pObj), vNodes );
432     return vNodes;
433 }
434 
435 /**Function*************************************************************
436 
437   Synopsis    [Collects internal nodes in the reverse DFS order.]
438 
439   Description []
440 
441   SideEffects []
442 
443   SeeAlso     []
444 
445 ***********************************************************************/
Aig_ManDfsReverse_rec(Aig_Man_t * p,Aig_Obj_t * pObj,Vec_Ptr_t * vNodes)446 void Aig_ManDfsReverse_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
447 {
448     Aig_Obj_t * pFanout;
449     int iFanout = -1, i;
450     assert( !Aig_IsComplement(pObj) );
451     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
452         return;
453     assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
454     Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
455         Aig_ManDfsReverse_rec( p, pFanout, vNodes );
456     assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
457     Aig_ObjSetTravIdCurrent(p, pObj);
458     Vec_PtrPush( vNodes, pObj );
459 }
460 
461 /**Function*************************************************************
462 
463   Synopsis    [Collects internal nodes in the reverse DFS order.]
464 
465   Description []
466 
467   SideEffects []
468 
469   SeeAlso     []
470 
471 ***********************************************************************/
Aig_ManDfsReverse(Aig_Man_t * p)472 Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p )
473 {
474     Vec_Ptr_t * vNodes;
475     Aig_Obj_t * pObj;
476     int i;
477     Aig_ManIncrementTravId( p );
478     // mark POs
479     Aig_ManForEachCo( p, pObj, i )
480         Aig_ObjSetTravIdCurrent( p, pObj );
481     // go through the nodes
482     vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
483     Aig_ManForEachObj( p, pObj, i )
484         if ( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) )
485             Aig_ManDfsReverse_rec( p, pObj, vNodes );
486     return vNodes;
487 }
488 
489 /**Function*************************************************************
490 
491   Synopsis    [Computes the max number of levels in the manager.]
492 
493   Description []
494 
495   SideEffects []
496 
497   SeeAlso     []
498 
499 ***********************************************************************/
Aig_ManLevelNum(Aig_Man_t * p)500 int Aig_ManLevelNum( Aig_Man_t * p )
501 {
502     Aig_Obj_t * pObj;
503     int i, LevelsMax;
504     LevelsMax = 0;
505     Aig_ManForEachCo( p, pObj, i )
506         LevelsMax = Abc_MaxInt( LevelsMax, (int)Aig_ObjFanin0(pObj)->Level );
507     return LevelsMax;
508 }
509 
510 //#if 0
511 
512 /**Function*************************************************************
513 
514   Synopsis    [Computes levels for AIG with choices and white boxes.]
515 
516   Description []
517 
518   SideEffects []
519 
520   SeeAlso     []
521 
522 ***********************************************************************/
Aig_ManChoiceLevel_rec(Aig_Man_t * p,Aig_Obj_t * pObj)523 void Aig_ManChoiceLevel_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
524 {
525     Aig_Obj_t * pNext;
526     int i, iBox, iTerm1, nTerms, LevelMax = 0;
527     if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
528         return;
529     Aig_ObjSetTravIdCurrent( p, pObj );
530     if ( Aig_ObjIsCi(pObj) )
531     {
532         if ( p->pManTime )
533         {
534             iBox = Tim_ManBoxForCi( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj) );
535             if ( iBox >= 0 ) // this is not a true PI
536             {
537                 iTerm1 = Tim_ManBoxInputFirst( (Tim_Man_t *)p->pManTime, iBox );
538                 nTerms = Tim_ManBoxInputNum( (Tim_Man_t *)p->pManTime, iBox );
539                 for ( i = 0; i < nTerms; i++ )
540                 {
541                     pNext = Aig_ManCo(p, iTerm1 + i);
542                     Aig_ManChoiceLevel_rec( p, pNext );
543                     if ( LevelMax < Aig_ObjLevel(pNext) )
544                         LevelMax = Aig_ObjLevel(pNext);
545                 }
546                 LevelMax++;
547             }
548         }
549 //        printf( "%d ", pObj->Level );
550     }
551     else if ( Aig_ObjIsCo(pObj) )
552     {
553         pNext = Aig_ObjFanin0(pObj);
554         Aig_ManChoiceLevel_rec( p, pNext );
555         if ( LevelMax < Aig_ObjLevel(pNext) )
556             LevelMax = Aig_ObjLevel(pNext);
557     }
558     else if ( Aig_ObjIsNode(pObj) )
559     {
560         // get the maximum level of the two fanins
561         pNext = Aig_ObjFanin0(pObj);
562         Aig_ManChoiceLevel_rec( p, pNext );
563         if ( LevelMax < Aig_ObjLevel(pNext) )
564             LevelMax = Aig_ObjLevel(pNext);
565         pNext = Aig_ObjFanin1(pObj);
566         Aig_ManChoiceLevel_rec( p, pNext );
567         if ( LevelMax < Aig_ObjLevel(pNext) )
568             LevelMax = Aig_ObjLevel(pNext);
569         LevelMax++;
570 
571         // get the level of the nodes in the choice node
572         if ( p->pEquivs && (pNext = Aig_ObjEquiv(p, pObj)) )
573         {
574             Aig_ManChoiceLevel_rec( p, pNext );
575             if ( LevelMax < Aig_ObjLevel(pNext) )
576                 LevelMax = Aig_ObjLevel(pNext);
577         }
578     }
579     else if ( !Aig_ObjIsConst1(pObj) )
580         assert( 0 );
581     Aig_ObjSetLevel( pObj, LevelMax );
582 }
583 
584 /**Function*************************************************************
585 
586   Synopsis    [Computes levels for AIG with choices and white boxes.]
587 
588   Description []
589 
590   SideEffects []
591 
592   SeeAlso     []
593 
594 ***********************************************************************/
Aig_ManChoiceLevel(Aig_Man_t * p)595 int Aig_ManChoiceLevel( Aig_Man_t * p )
596 {
597     Aig_Obj_t * pObj;
598     int i, LevelMax = 0;
599     Aig_ManForEachObj( p, pObj, i )
600         Aig_ObjSetLevel( pObj, 0 );
601     Aig_ManSetCioIds( p );
602     Aig_ManIncrementTravId( p );
603     Aig_ManForEachCo( p, pObj, i )
604     {
605         Aig_ManChoiceLevel_rec( p, pObj );
606         if ( LevelMax < Aig_ObjLevel(pObj) )
607             LevelMax = Aig_ObjLevel(pObj);
608     }
609     // account for dangling boxes
610     Aig_ManForEachCi( p, pObj, i )
611     {
612         Aig_ManChoiceLevel_rec( p, pObj );
613         if ( LevelMax < Aig_ObjLevel(pObj) )
614             LevelMax = Aig_ObjLevel(pObj);
615     }
616     Aig_ManCleanCioIds( p );
617 //    Aig_ManForEachNode( p, pObj, i )
618 //        assert( Aig_ObjLevel(pObj) > 0 );
619     return LevelMax;
620 }
621 
622 //#endif
623 
624 /**Function*************************************************************
625 
626   Synopsis    [Counts the number of AIG nodes rooted at this cone.]
627 
628   Description []
629 
630   SideEffects []
631 
632   SeeAlso     []
633 
634 ***********************************************************************/
Aig_ConeMark_rec(Aig_Obj_t * pObj)635 void Aig_ConeMark_rec( Aig_Obj_t * pObj )
636 {
637     assert( !Aig_IsComplement(pObj) );
638     if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
639         return;
640     Aig_ConeMark_rec( Aig_ObjFanin0(pObj) );
641     Aig_ConeMark_rec( Aig_ObjFanin1(pObj) );
642     assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
643     Aig_ObjSetMarkA( pObj );
644 }
645 
646 /**Function*************************************************************
647 
648   Synopsis    [Counts the number of AIG nodes rooted at this cone.]
649 
650   Description []
651 
652   SideEffects []
653 
654   SeeAlso     []
655 
656 ***********************************************************************/
Aig_ConeCleanAndMark_rec(Aig_Obj_t * pObj)657 void Aig_ConeCleanAndMark_rec( Aig_Obj_t * pObj )
658 {
659     assert( !Aig_IsComplement(pObj) );
660     if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
661         return;
662     Aig_ConeCleanAndMark_rec( Aig_ObjFanin0(pObj) );
663     Aig_ConeCleanAndMark_rec( Aig_ObjFanin1(pObj) );
664     assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
665     Aig_ObjSetMarkA( pObj );
666     pObj->pData = NULL;
667 }
668 
669 /**Function*************************************************************
670 
671   Synopsis    [Counts the number of AIG nodes rooted at this cone.]
672 
673   Description []
674 
675   SideEffects []
676 
677   SeeAlso     []
678 
679 ***********************************************************************/
Aig_ConeCountAndMark_rec(Aig_Obj_t * pObj)680 int Aig_ConeCountAndMark_rec( Aig_Obj_t * pObj )
681 {
682     int Counter;
683     assert( !Aig_IsComplement(pObj) );
684     if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
685         return 0;
686     Counter = 1 + Aig_ConeCountAndMark_rec( Aig_ObjFanin0(pObj) ) +
687         Aig_ConeCountAndMark_rec( Aig_ObjFanin1(pObj) );
688     assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
689     Aig_ObjSetMarkA( pObj );
690     return Counter;
691 }
692 
693 /**Function*************************************************************
694 
695   Synopsis    [Counts the number of AIG nodes rooted at this cone.]
696 
697   Description []
698 
699   SideEffects []
700 
701   SeeAlso     []
702 
703 ***********************************************************************/
Aig_ConeUnmark_rec(Aig_Obj_t * pObj)704 void Aig_ConeUnmark_rec( Aig_Obj_t * pObj )
705 {
706     assert( !Aig_IsComplement(pObj) );
707     if ( !Aig_ObjIsNode(pObj) || !Aig_ObjIsMarkA(pObj) )
708         return;
709     Aig_ConeUnmark_rec( Aig_ObjFanin0(pObj) );
710     Aig_ConeUnmark_rec( Aig_ObjFanin1(pObj) );
711     assert( Aig_ObjIsMarkA(pObj) ); // loop detection
712     Aig_ObjClearMarkA( pObj );
713 }
714 
715 /**Function*************************************************************
716 
717   Synopsis    [Counts the number of AIG nodes rooted at this cone.]
718 
719   Description []
720 
721   SideEffects []
722 
723   SeeAlso     []
724 
725 ***********************************************************************/
Aig_DagSize(Aig_Obj_t * pObj)726 int Aig_DagSize( Aig_Obj_t * pObj )
727 {
728     int Counter;
729     Counter = Aig_ConeCountAndMark_rec( Aig_Regular(pObj) );
730     Aig_ConeUnmark_rec( Aig_Regular(pObj) );
731     return Counter;
732 }
733 
734 /**Function*************************************************************
735 
736   Synopsis    [Counts the support size of the node.]
737 
738   Description []
739 
740   SideEffects []
741 
742   SeeAlso     []
743 
744 ***********************************************************************/
Aig_SupportSize_rec(Aig_Man_t * p,Aig_Obj_t * pObj,int * pCounter)745 void Aig_SupportSize_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int * pCounter )
746 {
747     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
748         return;
749     Aig_ObjSetTravIdCurrent(p, pObj);
750     if ( Aig_ObjIsCi(pObj) )
751     {
752         (*pCounter)++;
753         return;
754     }
755     assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
756     Aig_SupportSize_rec( p, Aig_ObjFanin0(pObj), pCounter );
757     if ( Aig_ObjFanin1(pObj) )
758         Aig_SupportSize_rec( p, Aig_ObjFanin1(pObj), pCounter );
759 }
760 
761 /**Function*************************************************************
762 
763   Synopsis    [Counts the support size of the node.]
764 
765   Description []
766 
767   SideEffects []
768 
769   SeeAlso     []
770 
771 ***********************************************************************/
Aig_SupportSize(Aig_Man_t * p,Aig_Obj_t * pObj)772 int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj )
773 {
774     int Counter = 0;
775     assert( !Aig_IsComplement(pObj) );
776     assert( !Aig_ObjIsCo(pObj) );
777     Aig_ManIncrementTravId( p );
778     Aig_SupportSize_rec( p, pObj, &Counter );
779     return Counter;
780 }
781 
782 /**Function*************************************************************
783 
784   Synopsis    [Counts the support size of the node.]
785 
786   Description []
787 
788   SideEffects []
789 
790   SeeAlso     []
791 
792 ***********************************************************************/
Aig_SupportSizeTest(Aig_Man_t * p)793 int Aig_SupportSizeTest( Aig_Man_t * p )
794 {
795     Aig_Obj_t * pObj;
796     int i, Counter = 0;
797     abctime clk = Abc_Clock();
798     Aig_ManForEachObj( p, pObj, i )
799         if ( Aig_ObjIsNode(pObj) )
800             Counter += (Aig_SupportSize(p, pObj) <= 16);
801     printf( "Nodes with small support %d (out of %d)\n", Counter, Aig_ManNodeNum(p) );
802     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
803     return Counter;
804 }
805 
806 /**Function*************************************************************
807 
808   Synopsis    [Counts the support size of the node.]
809 
810   Description []
811 
812   SideEffects []
813 
814   SeeAlso     []
815 
816 ***********************************************************************/
Aig_Support_rec(Aig_Man_t * p,Aig_Obj_t * pObj,Vec_Ptr_t * vSupp)817 void Aig_Support_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vSupp )
818 {
819     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
820         return;
821     Aig_ObjSetTravIdCurrent(p, pObj);
822     if ( Aig_ObjIsConst1(pObj) )
823         return;
824     if ( Aig_ObjIsCi(pObj) )
825     {
826         Vec_PtrPush( vSupp, pObj );
827         return;
828     }
829     assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
830     Aig_Support_rec( p, Aig_ObjFanin0(pObj), vSupp );
831     if ( Aig_ObjFanin1(pObj) )
832         Aig_Support_rec( p, Aig_ObjFanin1(pObj), vSupp );
833 }
834 
835 /**Function*************************************************************
836 
837   Synopsis    [Counts the support size of the node.]
838 
839   Description []
840 
841   SideEffects []
842 
843   SeeAlso     []
844 
845 ***********************************************************************/
Aig_Support(Aig_Man_t * p,Aig_Obj_t * pObj)846 Vec_Ptr_t * Aig_Support( Aig_Man_t * p, Aig_Obj_t * pObj )
847 {
848     Vec_Ptr_t * vSupp;
849     assert( !Aig_IsComplement(pObj) );
850     assert( !Aig_ObjIsCo(pObj) );
851     Aig_ManIncrementTravId( p );
852     vSupp = Vec_PtrAlloc( 100 );
853     Aig_Support_rec( p, pObj, vSupp );
854     return vSupp;
855 }
856 
857 /**Function*************************************************************
858 
859   Synopsis    [Counts the support size of the node.]
860 
861   Description []
862 
863   SideEffects []
864 
865   SeeAlso     []
866 
867 ***********************************************************************/
Aig_SupportNodes(Aig_Man_t * p,Aig_Obj_t ** ppObjs,int nObjs,Vec_Ptr_t * vSupp)868 void Aig_SupportNodes( Aig_Man_t * p, Aig_Obj_t ** ppObjs, int nObjs, Vec_Ptr_t * vSupp )
869 {
870     int i;
871     Vec_PtrClear( vSupp );
872     Aig_ManIncrementTravId( p );
873     Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
874     for ( i = 0; i < nObjs; i++ )
875     {
876         assert( !Aig_IsComplement(ppObjs[i]) );
877         if ( Aig_ObjIsCo(ppObjs[i]) )
878             Aig_Support_rec( p, Aig_ObjFanin0(ppObjs[i]), vSupp );
879         else
880             Aig_Support_rec( p, ppObjs[i], vSupp );
881     }
882 }
883 
884 /**Function*************************************************************
885 
886   Synopsis    [Transfers the AIG from one manager into another.]
887 
888   Description []
889 
890   SideEffects []
891 
892   SeeAlso     []
893 
894 ***********************************************************************/
Aig_Transfer_rec(Aig_Man_t * pDest,Aig_Obj_t * pObj)895 void Aig_Transfer_rec( Aig_Man_t * pDest, Aig_Obj_t * pObj )
896 {
897     assert( !Aig_IsComplement(pObj) );
898     if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
899         return;
900     Aig_Transfer_rec( pDest, Aig_ObjFanin0(pObj) );
901     Aig_Transfer_rec( pDest, Aig_ObjFanin1(pObj) );
902     pObj->pData = Aig_And( pDest, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
903     assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
904     Aig_ObjSetMarkA( pObj );
905 }
906 
907 /**Function*************************************************************
908 
909   Synopsis    [Transfers the AIG from one manager into another.]
910 
911   Description []
912 
913   SideEffects []
914 
915   SeeAlso     []
916 
917 ***********************************************************************/
Aig_Transfer(Aig_Man_t * pSour,Aig_Man_t * pDest,Aig_Obj_t * pRoot,int nVars)918 Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pRoot, int nVars )
919 {
920     Aig_Obj_t * pObj;
921     int i;
922     // solve simple cases
923     if ( pSour == pDest )
924         return pRoot;
925     if ( Aig_ObjIsConst1( Aig_Regular(pRoot) ) )
926         return Aig_NotCond( Aig_ManConst1(pDest), Aig_IsComplement(pRoot) );
927     // set the PI mapping
928     Aig_ManForEachCi( pSour, pObj, i )
929     {
930         if ( i == nVars )
931            break;
932         pObj->pData = Aig_IthVar(pDest, i);
933     }
934     // transfer and set markings
935     Aig_Transfer_rec( pDest, Aig_Regular(pRoot) );
936     // clear the markings
937     Aig_ConeUnmark_rec( Aig_Regular(pRoot) );
938     return Aig_NotCond( (Aig_Obj_t *)Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) );
939 }
940 
941 /**Function*************************************************************
942 
943   Synopsis    [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
944 
945   Description []
946 
947   SideEffects []
948 
949   SeeAlso     []
950 
951 ***********************************************************************/
Aig_Compose_rec(Aig_Man_t * p,Aig_Obj_t * pObj,Aig_Obj_t * pFunc,Aig_Obj_t * pVar)952 void Aig_Compose_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFunc, Aig_Obj_t * pVar )
953 {
954     assert( !Aig_IsComplement(pObj) );
955     if ( Aig_ObjIsMarkA(pObj) )
956         return;
957     if ( Aig_ObjIsConst1(pObj) || Aig_ObjIsCi(pObj) )
958     {
959         pObj->pData = pObj == pVar ? pFunc : pObj;
960         return;
961     }
962     Aig_Compose_rec( p, Aig_ObjFanin0(pObj), pFunc, pVar );
963     Aig_Compose_rec( p, Aig_ObjFanin1(pObj), pFunc, pVar );
964     pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
965     assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
966     Aig_ObjSetMarkA( pObj );
967 }
968 
969 /**Function*************************************************************
970 
971   Synopsis    [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
972 
973   Description []
974 
975   SideEffects []
976 
977   SeeAlso     []
978 
979 ***********************************************************************/
Aig_Compose(Aig_Man_t * p,Aig_Obj_t * pRoot,Aig_Obj_t * pFunc,int iVar)980 Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar )
981 {
982     // quit if the PI variable is not defined
983     if ( iVar >= Aig_ManCiNum(p) )
984     {
985         printf( "Aig_Compose(): The PI variable %d is not defined.\n", iVar );
986         return NULL;
987     }
988     // recursively perform composition
989     Aig_Compose_rec( p, Aig_Regular(pRoot), pFunc, Aig_ManCi(p, iVar) );
990     // clear the markings
991     Aig_ConeUnmark_rec( Aig_Regular(pRoot) );
992     return Aig_NotCond( (Aig_Obj_t *)Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) );
993 }
994 
995 /**Function*************************************************************
996 
997   Synopsis    [Computes the internal nodes of the cut.]
998 
999   Description []
1000 
1001   SideEffects []
1002 
1003   SeeAlso     []
1004 
1005 ***********************************************************************/
Aig_ObjCollectCut_rec(Aig_Obj_t * pNode,Vec_Ptr_t * vNodes)1006 void Aig_ObjCollectCut_rec( Aig_Obj_t * pNode, Vec_Ptr_t * vNodes )
1007 {
1008 //    Aig_Obj_t * pFan0 = Aig_ObjFanin0(pNode);
1009 //    Aig_Obj_t * pFan1 = Aig_ObjFanin1(pNode);
1010     if ( pNode->fMarkA )
1011         return;
1012     pNode->fMarkA = 1;
1013     assert( Aig_ObjIsNode(pNode) );
1014     Aig_ObjCollectCut_rec( Aig_ObjFanin0(pNode), vNodes );
1015     Aig_ObjCollectCut_rec( Aig_ObjFanin1(pNode), vNodes );
1016     Vec_PtrPush( vNodes, pNode );
1017 //printf( "added %d  ", pNode->Id );
1018 }
1019 
1020 /**Function*************************************************************
1021 
1022   Synopsis    [Computes the internal nodes of the cut.]
1023 
1024   Description [Does not include the leaves of the cut.]
1025 
1026   SideEffects []
1027 
1028   SeeAlso     []
1029 
1030 ***********************************************************************/
Aig_ObjCollectCut(Aig_Obj_t * pRoot,Vec_Ptr_t * vLeaves,Vec_Ptr_t * vNodes)1031 void Aig_ObjCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes )
1032 {
1033     Aig_Obj_t * pObj;
1034     int i;
1035     // collect and mark the leaves
1036     Vec_PtrClear( vNodes );
1037     Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
1038     {
1039         assert( pObj->fMarkA == 0 );
1040         pObj->fMarkA = 1;
1041 //        printf( "%d " , pObj->Id );
1042     }
1043 //printf( "\n" );
1044     // collect and mark the nodes
1045     Aig_ObjCollectCut_rec( pRoot, vNodes );
1046     // clean the nodes
1047     Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
1048         pObj->fMarkA = 0;
1049     Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
1050         pObj->fMarkA = 0;
1051 }
1052 
1053 
1054 /**Function*************************************************************
1055 
1056   Synopsis    [Collects the nodes of the supergate.]
1057 
1058   Description []
1059 
1060   SideEffects []
1061 
1062   SeeAlso     []
1063 
1064 ***********************************************************************/
Aig_ObjCollectSuper_rec(Aig_Obj_t * pRoot,Aig_Obj_t * pObj,Vec_Ptr_t * vSuper)1065 int Aig_ObjCollectSuper_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
1066 {
1067     int RetValue1, RetValue2, i;
1068     // check if the node is visited
1069     if ( Aig_Regular(pObj)->fMarkA )
1070     {
1071         // check if the node occurs in the same polarity
1072         for ( i = 0; i < vSuper->nSize; i++ )
1073             if ( vSuper->pArray[i] == pObj )
1074                 return 1;
1075         // check if the node is present in the opposite polarity
1076         for ( i = 0; i < vSuper->nSize; i++ )
1077             if ( vSuper->pArray[i] == Aig_Not(pObj) )
1078                 return -1;
1079         assert( 0 );
1080         return 0;
1081     }
1082     // if the new node is complemented or a PI, another gate begins
1083     if ( pObj != pRoot && (Aig_IsComplement(pObj) || Aig_ObjType(pObj) != Aig_ObjType(pRoot) || Aig_ObjRefs(pObj) > 1) )
1084     {
1085         Vec_PtrPush( vSuper, pObj );
1086         Aig_Regular(pObj)->fMarkA = 1;
1087         return 0;
1088     }
1089     assert( !Aig_IsComplement(pObj) );
1090     assert( Aig_ObjIsNode(pObj) );
1091     // go through the branches
1092     RetValue1 = Aig_ObjCollectSuper_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper );
1093     RetValue2 = Aig_ObjCollectSuper_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper );
1094     if ( RetValue1 == -1 || RetValue2 == -1 )
1095         return -1;
1096     // return 1 if at least one branch has a duplicate
1097     return RetValue1 || RetValue2;
1098 }
1099 
1100 /**Function*************************************************************
1101 
1102   Synopsis    [Collects the nodes of the supergate.]
1103 
1104   Description []
1105 
1106   SideEffects []
1107 
1108   SeeAlso     []
1109 
1110 ***********************************************************************/
Aig_ObjCollectSuper(Aig_Obj_t * pObj,Vec_Ptr_t * vSuper)1111 int Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
1112 {
1113     int RetValue, i;
1114     assert( !Aig_IsComplement(pObj) );
1115     assert( Aig_ObjIsNode(pObj) );
1116     // collect the nodes in the implication supergate
1117     Vec_PtrClear( vSuper );
1118     RetValue = Aig_ObjCollectSuper_rec( pObj, pObj, vSuper );
1119     assert( Vec_PtrSize(vSuper) > 1 );
1120     // unmark the visited nodes
1121     Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pObj, i )
1122         Aig_Regular(pObj)->fMarkA = 0;
1123     // if we found the node and its complement in the same implication supergate,
1124     // return empty set of nodes (meaning that we should use constant-0 node)
1125     if ( RetValue == -1 )
1126         vSuper->nSize = 0;
1127     return RetValue;
1128 }
1129 
1130 ////////////////////////////////////////////////////////////////////////
1131 ///                       END OF FILE                                ///
1132 ////////////////////////////////////////////////////////////////////////
1133 
1134 
1135 ABC_NAMESPACE_IMPL_END
1136 
1137