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