1 /**CFile****************************************************************
2 
3   FileName    [darBalance.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [DAG-aware AIG rewriting.]
8 
9   Synopsis    [Algebraic AIG balancing.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - April 28, 2007.]
16 
17   Revision    [$Id: darBalance.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "darInt.h"
22 #include "misc/tim/tim.h"
23 
24 ABC_NAMESPACE_IMPL_START
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 ///                        DECLARATIONS                              ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 //#define USE_LUTSIZE_BALANCE
32 
33 ////////////////////////////////////////////////////////////////////////
34 ///                     FUNCTION DEFINITIONS                         ///
35 ////////////////////////////////////////////////////////////////////////
36 
37 /**Function*************************************************************
38 
39   Synopsis    [Uniqifies the node.]
40 
41   Description []
42 
43   SideEffects []
44 
45   SeeAlso     []
46 
47 ***********************************************************************/
Dar_ObjCompareLits(Aig_Obj_t ** pp1,Aig_Obj_t ** pp2)48 int Dar_ObjCompareLits( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
49 {
50     int Diff = Aig_ObjToLit(*pp1) - Aig_ObjToLit(*pp2);
51     if ( Diff < 0 )
52         return -1;
53     if ( Diff > 0 )
54         return 1;
55     return 0;
56 }
Dar_BalanceUniqify(Aig_Obj_t * pObj,Vec_Ptr_t * vNodes,int fExor)57 void Dar_BalanceUniqify( Aig_Obj_t * pObj, Vec_Ptr_t * vNodes, int fExor )
58 {
59     Aig_Obj_t * pTemp, * pTempNext;
60     int i, k;
61     // sort the nodes by their literal
62     Vec_PtrSort( vNodes, (int (*)())Dar_ObjCompareLits );
63     // remove duplicates
64     k = 0;
65     Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pTemp, i )
66     {
67         if ( i + 1 == Vec_PtrSize(vNodes) )
68         {
69             Vec_PtrWriteEntry( vNodes, k++, pTemp );
70             break;
71         }
72         pTempNext = (Aig_Obj_t *)Vec_PtrEntry( vNodes, i+1 );
73         if ( !fExor && pTemp == Aig_Not(pTempNext) ) // pos_lit & neg_lit = 0
74         {
75             Vec_PtrClear( vNodes );
76             return;
77         }
78         if ( pTemp != pTempNext )  // save if different
79             Vec_PtrWriteEntry( vNodes, k++, pTemp );
80         else if ( fExor ) // in case of XOR, remove identical
81             i++;
82     }
83     Vec_PtrShrink( vNodes, k );
84     if ( Vec_PtrSize(vNodes) < 2 )
85         return;
86     // check that there is no duplicates
87     pTemp = (Aig_Obj_t *)Vec_PtrEntry( vNodes, 0 );
88     Vec_PtrForEachEntryStart( Aig_Obj_t *, vNodes, pTempNext, i, 1 )
89     {
90         assert( pTemp != pTempNext );
91         pTemp = pTempNext;
92     }
93 }
94 
95 /**Function*************************************************************
96 
97   Synopsis    [Collects the nodes of the supergate.]
98 
99   Description []
100 
101   SideEffects []
102 
103   SeeAlso     []
104 
105 ***********************************************************************/
Dar_BalanceCone_rec(Aig_Obj_t * pRoot,Aig_Obj_t * pObj,Vec_Ptr_t * vSuper)106 void Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
107 {
108     if ( pObj != pRoot && (Aig_IsComplement(pObj) || Aig_ObjType(pObj) != Aig_ObjType(pRoot) || Aig_ObjRefs(pObj) > 1 || Vec_PtrSize(vSuper) > 10000) )
109         Vec_PtrPush( vSuper, pObj );
110     else
111     {
112         assert( !Aig_IsComplement(pObj) );
113         assert( Aig_ObjIsNode(pObj) );
114         // go through the branches
115         Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper );
116         Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper );
117     }
118 }
Dar_BalanceCone(Aig_Obj_t * pObj,Vec_Vec_t * vStore,int Level)119 Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
120 {
121     Vec_Ptr_t * vNodes;
122     assert( !Aig_IsComplement(pObj) );
123     assert( Aig_ObjIsNode(pObj) );
124     // extend the storage
125     if ( Vec_VecSize( vStore ) <= Level )
126         Vec_VecPush( vStore, Level, 0 );
127     // get the temporary array of nodes
128     vNodes = Vec_VecEntry( vStore, Level );
129     Vec_PtrClear( vNodes );
130     // collect the nodes in the implication supergate
131     Dar_BalanceCone_rec( pObj, pObj, vNodes );
132     // remove duplicates
133     Dar_BalanceUniqify( pObj, vNodes, Aig_ObjIsExor(pObj) );
134     return vNodes;
135 }
136 
137 
138 /**Function*************************************************************
139 
140   Synopsis    [Collects the nodes of the supergate.]
141 
142   Description []
143 
144   SideEffects []
145 
146   SeeAlso     []
147 
148 ***********************************************************************/
149 /*
150 int Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
151 {
152     int RetValue1, RetValue2, i;
153     // check if the node is visited
154     if ( Aig_Regular(pObj)->fMarkB )
155     {
156         if ( Aig_ObjIsExor(pRoot) )
157         {
158             assert( !Aig_IsComplement(pObj) );
159             // check if the node occurs in the same polarity
160             Vec_PtrRemove( vSuper, pObj );
161             Aig_Regular(pObj)->fMarkB = 0;
162 //printf( " Duplicated EXOR input!!! " );
163             return 1;
164         }
165         else
166         {
167             // check if the node occurs in the same polarity
168             for ( i = 0; i < vSuper->nSize; i++ )
169                 if ( vSuper->pArray[i] == pObj )
170                     return 1;
171             // check if the node is present in the opposite polarity
172             for ( i = 0; i < vSuper->nSize; i++ )
173                 if ( vSuper->pArray[i] == Aig_Not(pObj) )
174                     return -1;
175         }
176         assert( 0 );
177         return 0;
178     }
179     // if the new node is complemented or a PI, another gate begins
180     if ( pObj != pRoot && (Aig_IsComplement(pObj) || Aig_ObjType(pObj) != Aig_ObjType(pRoot) || Aig_ObjRefs(pObj) > 1 || Vec_PtrSize(vSuper) > 10000) )
181     {
182         Vec_PtrPush( vSuper, pObj );
183         Aig_Regular(pObj)->fMarkB = 1;
184         return 0;
185     }
186     assert( !Aig_IsComplement(pObj) );
187     assert( Aig_ObjIsNode(pObj) );
188     // go through the branches
189     RetValue1 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper );
190     RetValue2 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper );
191     if ( RetValue1 == -1 || RetValue2 == -1 )
192         return -1;
193     // return 1 if at least one branch has a duplicate
194     return RetValue1 || RetValue2;
195 }
196 Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
197 {
198     Vec_Ptr_t * vNodes;
199     int RetValue, i;
200     assert( !Aig_IsComplement(pObj) );
201     // extend the storage
202     if ( Vec_VecSize( vStore ) <= Level )
203         Vec_VecPush( vStore, Level, 0 );
204     // get the temporary array of nodes
205     vNodes = Vec_VecEntry( vStore, Level );
206     Vec_PtrClear( vNodes );
207     // collect the nodes in the implication supergate
208     RetValue = Dar_BalanceCone_rec( pObj, pObj, vNodes );
209     assert( RetValue != 0 || vNodes->nSize > 1 );
210     // unmark the visited nodes
211     Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
212         Aig_Regular(pObj)->fMarkB = 0;
213     // if we found the node and its complement in the same implication supergate,
214     // return empty set of nodes (meaning that we should use constant-0 node)
215     if ( RetValue == -1 )
216         vNodes->nSize = 0;
217     return vNodes;
218 }
219 */
220 
221 /**Function*************************************************************
222 
223   Synopsis    [Finds the left bound on the next candidate to be paired.]
224 
225   Description [The nodes in the array are in the decreasing order of levels.
226   The last node in the array has the smallest level. By default it would be paired
227   with the next node on the left. However, it may be possible to pair it with some
228   other node on the left, in such a way that the new node is shared. This procedure
229   finds the index of the left-most node, which can be paired with the last node.]
230 
231   SideEffects []
232 
233   SeeAlso     []
234 
235 ***********************************************************************/
Dar_BalanceFindLeft(Vec_Ptr_t * vSuper)236 int Dar_BalanceFindLeft( Vec_Ptr_t * vSuper )
237 {
238     Aig_Obj_t * pObjRight, * pObjLeft;
239     int Current;
240     // if two or less nodes, pair with the first
241     if ( Vec_PtrSize(vSuper) < 3 )
242         return 0;
243     // set the pointer to the one before the last
244     Current = Vec_PtrSize(vSuper) - 2;
245     pObjRight = (Aig_Obj_t *)Vec_PtrEntry( vSuper, Current );
246     // go through the nodes to the left of this one
247     for ( Current--; Current >= 0; Current-- )
248     {
249         // get the next node on the left
250         pObjLeft = (Aig_Obj_t *)Vec_PtrEntry( vSuper, Current );
251         // if the level of this node is different, quit the loop
252         if ( Aig_ObjLevel(Aig_Regular(pObjLeft)) != Aig_ObjLevel(Aig_Regular(pObjRight)) )
253             break;
254     }
255     Current++;
256     // get the node, for which the equality holds
257     pObjLeft = (Aig_Obj_t *)Vec_PtrEntry( vSuper, Current );
258     assert( Aig_ObjLevel(Aig_Regular(pObjLeft)) == Aig_ObjLevel(Aig_Regular(pObjRight)) );
259     return Current;
260 }
261 
262 /**Function*************************************************************
263 
264   Synopsis    [Moves closer to the end the node that is best for sharing.]
265 
266   Description [If there is no node with sharing, randomly chooses one of
267   the legal nodes.]
268 
269   SideEffects []
270 
271   SeeAlso     []
272 
273 ***********************************************************************/
Dar_BalancePermute(Aig_Man_t * p,Vec_Ptr_t * vSuper,int LeftBound,int fExor)274 void Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor )
275 {
276     Aig_Obj_t * pObj1, * pObj2, * pObj3, * pGhost;
277     int RightBound, i;
278     // get the right bound
279     RightBound = Vec_PtrSize(vSuper) - 2;
280     assert( LeftBound <= RightBound );
281     if ( LeftBound == RightBound )
282         return;
283     // get the two last nodes
284     pObj1 = (Aig_Obj_t *)Vec_PtrEntry( vSuper, RightBound + 1 );
285     pObj2 = (Aig_Obj_t *)Vec_PtrEntry( vSuper, RightBound     );
286     if ( Aig_Regular(pObj1) == p->pConst1 || Aig_Regular(pObj2) == p->pConst1 || Aig_Regular(pObj1) == Aig_Regular(pObj2) )
287         return;
288     // find the first node that can be shared
289     for ( i = RightBound; i >= LeftBound; i-- )
290     {
291         pObj3 = (Aig_Obj_t *)Vec_PtrEntry( vSuper, i );
292         if ( Aig_Regular(pObj3) == p->pConst1 )
293         {
294             Vec_PtrWriteEntry( vSuper, i,          pObj2 );
295             Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
296             return;
297         }
298         if ( Aig_Regular(pObj1) == Aig_Regular(pObj3) )
299         {
300             if ( pObj3 == pObj2 )
301                 return;
302             Vec_PtrWriteEntry( vSuper, i,          pObj2 );
303             Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
304             return;
305         }
306         pGhost = Aig_ObjCreateGhost( p, pObj1, pObj3, fExor? AIG_OBJ_EXOR : AIG_OBJ_AND );
307         if ( Aig_TableLookup( p, pGhost ) )
308         {
309             if ( pObj3 == pObj2 )
310                 return;
311             Vec_PtrWriteEntry( vSuper, i,          pObj2 );
312             Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
313             return;
314         }
315     }
316 /*
317     // we did not find the node to share, randomize choice
318     {
319         int Choice = Aig_ManRandom(0) % (RightBound - LeftBound + 1);
320         pObj3 = Vec_PtrEntry( vSuper, LeftBound + Choice );
321         if ( pObj3 == pObj2 )
322             return;
323         Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pObj2 );
324         Vec_PtrWriteEntry( vSuper, RightBound,         pObj3 );
325     }
326 */
327 }
328 
329 /**Function*************************************************************
330 
331   Synopsis    [Procedure used for sorting the nodes in decreasing order of levels.]
332 
333   Description []
334 
335   SideEffects []
336 
337   SeeAlso     []
338 
339 ***********************************************************************/
Aig_NodeCompareLevelsDecrease(Aig_Obj_t ** pp1,Aig_Obj_t ** pp2)340 int Aig_NodeCompareLevelsDecrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
341 {
342     int Diff = Aig_ObjLevel(Aig_Regular(*pp1)) - Aig_ObjLevel(Aig_Regular(*pp2));
343     if ( Diff > 0 )
344         return -1;
345     if ( Diff < 0 )
346         return 1;
347     Diff = Aig_ObjId(Aig_Regular(*pp1)) - Aig_ObjId(Aig_Regular(*pp2));
348     if ( Diff > 0 )
349         return -1;
350     if ( Diff < 0 )
351         return 1;
352     return 0;
353 }
354 
355 /**Function*************************************************************
356 
357   Synopsis    [Inserts a new node in the order by levels.]
358 
359   Description []
360 
361   SideEffects []
362 
363   SeeAlso     []
364 
365 ***********************************************************************/
Dar_BalancePushUniqueOrderByLevel(Vec_Ptr_t * vStore,Aig_Obj_t * pObj,int fExor)366 void Dar_BalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj, int fExor )
367 {
368     Aig_Obj_t * pObj1, * pObj2;
369     int i;
370     if ( Vec_PtrPushUnique(vStore, pObj) )
371     {
372         if ( fExor )
373             Vec_PtrRemove(vStore, pObj);
374         return;
375     }
376     // find the p of the node
377     for ( i = vStore->nSize-1; i > 0; i-- )
378     {
379         pObj1 = (Aig_Obj_t *)vStore->pArray[i  ];
380         pObj2 = (Aig_Obj_t *)vStore->pArray[i-1];
381         if ( Aig_ObjLevel(Aig_Regular(pObj1)) <= Aig_ObjLevel(Aig_Regular(pObj2)) )
382             break;
383         vStore->pArray[i  ] = pObj2;
384         vStore->pArray[i-1] = pObj1;
385     }
386 }
387 
388 /**Function*************************************************************
389 
390   Synopsis    [Builds implication supergate.]
391 
392   Description []
393 
394   SideEffects []
395 
396   SeeAlso     []
397 
398 ***********************************************************************/
Dar_BalanceBuildSuper(Aig_Man_t * p,Vec_Ptr_t * vSuper,Aig_Type_t Type,int fUpdateLevel)399 Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel )
400 {
401     Aig_Obj_t * pObj1, * pObj2;
402     int LeftBound;
403     assert( vSuper->nSize > 1 );
404     // sort the new nodes by level in the decreasing order
405     Vec_PtrSort( vSuper, (int (*)(void))Aig_NodeCompareLevelsDecrease );
406     // balance the nodes
407     while ( vSuper->nSize > 1 )
408     {
409         // find the left bound on the node to be paired
410         LeftBound = (!fUpdateLevel)? 0 : Dar_BalanceFindLeft( vSuper );
411         // find the node that can be shared (if no such node, randomize choice)
412         Dar_BalancePermute( p, vSuper, LeftBound, Type == AIG_OBJ_EXOR );
413         // pull out the last two nodes
414         pObj1 = (Aig_Obj_t *)Vec_PtrPop(vSuper);
415         pObj2 = (Aig_Obj_t *)Vec_PtrPop(vSuper);
416         Dar_BalancePushUniqueOrderByLevel( vSuper, Aig_Oper(p, pObj1, pObj2, Type), Type == AIG_OBJ_EXOR );
417     }
418     return (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0);
419 }
420 
421 
422 /**Function*************************************************************
423 
424   Synopsis    [Returns affective support size.]
425 
426   Description []
427 
428   SideEffects []
429 
430   SeeAlso     []
431 
432 ***********************************************************************/
Aig_BaseSize(Aig_Man_t * p,Aig_Obj_t * pObj,int nLutSize)433 int Aig_BaseSize( Aig_Man_t * p, Aig_Obj_t * pObj, int nLutSize )
434 {
435     int nBaseSize;
436     pObj = Aig_Regular(pObj);
437     if ( Aig_ObjIsConst1(pObj) )
438         return 0;
439     if ( Aig_ObjLevel(pObj) >= nLutSize )
440         return 1;
441     nBaseSize = Aig_SupportSize( p, pObj );
442     if ( nBaseSize >= nLutSize )
443         return 1;
444     return nBaseSize;
445 }
446 
447 /**Function*************************************************************
448 
449   Synopsis    [Builds implication supergate.]
450 
451   Description []
452 
453   SideEffects []
454 
455   SeeAlso     []
456 
457 ***********************************************************************/
Dar_BalanceBuildSuperTop(Aig_Man_t * p,Vec_Ptr_t * vSuper,Aig_Type_t Type,int fUpdateLevel,int nLutSize)458 Aig_Obj_t * Dar_BalanceBuildSuperTop( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel, int nLutSize )
459 {
460     Vec_Ptr_t * vSubset;
461     Aig_Obj_t * pObj;
462     int i, nBaseSizeAll, nBaseSize;
463     assert( vSuper->nSize > 1 );
464     // sort the new nodes by level in the decreasing order
465     Vec_PtrSort( vSuper, (int (*)(void))Aig_NodeCompareLevelsDecrease );
466     // add one LUT at a time
467     while ( Vec_PtrSize(vSuper) > 1 )
468     {
469         // isolate the group of nodes with nLutSize inputs
470         nBaseSizeAll = 0;
471         vSubset = Vec_PtrAlloc( nLutSize );
472         Vec_PtrForEachEntryReverse( Aig_Obj_t *, vSuper, pObj, i )
473         {
474             nBaseSize = Aig_BaseSize( p, pObj, nLutSize );
475             if ( nBaseSizeAll + nBaseSize > nLutSize && Vec_PtrSize(vSubset) > 1 )
476                 break;
477             nBaseSizeAll += nBaseSize;
478             Vec_PtrPush( vSubset, pObj );
479         }
480         // remove them from vSuper
481         Vec_PtrShrink( vSuper, Vec_PtrSize(vSuper) - Vec_PtrSize(vSubset) );
482         // create the new supergate
483         pObj = Dar_BalanceBuildSuper( p, vSubset, Type, fUpdateLevel );
484         Vec_PtrFree( vSubset );
485         // add the new output
486         Dar_BalancePushUniqueOrderByLevel( vSuper, pObj, Type == AIG_OBJ_EXOR );
487     }
488     return (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0);
489 }
490 
491 /**Function*************************************************************
492 
493   Synopsis    [Returns the new node constructed.]
494 
495   Description []
496 
497   SideEffects []
498 
499   SeeAlso     []
500 
501 ***********************************************************************/
Dar_Balance_rec(Aig_Man_t * pNew,Aig_Obj_t * pObjOld,Vec_Vec_t * vStore,int Level,int fUpdateLevel)502 Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel )
503 {
504     Aig_Obj_t * pObjNew;
505     Vec_Ptr_t * vSuper;
506     int i;
507     assert( !Aig_IsComplement(pObjOld) );
508     assert( !Aig_ObjIsBuf(pObjOld) );
509     // return if the result is known
510     if ( pObjOld->pData )
511         return (Aig_Obj_t *)pObjOld->pData;
512     assert( Aig_ObjIsNode(pObjOld) );
513     // get the implication supergate
514     vSuper = Dar_BalanceCone( pObjOld, vStore, Level );
515     // check if supergate contains two nodes in the opposite polarity
516     if ( vSuper->nSize == 0 )
517         return (Aig_Obj_t *)(pObjOld->pData = Aig_ManConst0(pNew));
518     // for each old node, derive the new well-balanced node
519     for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
520     {
521         pObjNew = Dar_Balance_rec( pNew, Aig_Regular((Aig_Obj_t *)vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
522         if ( pObjNew == NULL )
523             return NULL;
524         vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement((Aig_Obj_t *)vSuper->pArray[i]) );
525     }
526     // check for exactly one node
527     if ( vSuper->nSize == 1 )
528         return (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0);
529     // build the supergate
530 #ifdef USE_LUTSIZE_BALANCE
531     pObjNew = Dar_BalanceBuildSuperTop( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel, 6 );
532 #else
533     pObjNew = Dar_BalanceBuildSuper( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel );
534 #endif
535     if ( pNew->Time2Quit && !(Aig_Regular(pObjNew)->Id & 255) && Abc_Clock() > pNew->Time2Quit )
536         return NULL;
537     // make sure the balanced node is not assigned
538 //    assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level );
539     assert( pObjOld->pData == NULL );
540     return (Aig_Obj_t *)(pObjOld->pData = pObjNew);
541 }
542 
543 /**Function*************************************************************
544 
545   Synopsis    [Performs algebraic balancing of the AIG.]
546 
547   Description []
548 
549   SideEffects []
550 
551   SeeAlso     []
552 
553 ***********************************************************************/
Dar_ManBalance(Aig_Man_t * p,int fUpdateLevel)554 Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
555 {
556     Aig_Man_t * pNew;
557     Aig_Obj_t * pObj, * pDriver, * pObjNew;
558     Vec_Vec_t * vStore;
559     int i;
560     assert( Aig_ManVerifyTopoOrder(p) );
561     // create the new manager
562     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
563     pNew->pName = Abc_UtilStrsav( p->pName );
564     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
565     pNew->nAsserts = p->nAsserts;
566     pNew->nConstrs = p->nConstrs;
567     pNew->nBarBufs = p->nBarBufs;
568     pNew->Time2Quit = p->Time2Quit;
569     if ( p->vFlopNums )
570         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
571     // map the PI nodes
572     Aig_ManCleanData( p );
573     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
574     vStore = Vec_VecAlloc( 50 );
575     if ( p->pManTime != NULL )
576     {
577         float arrTime;
578         Tim_ManIncrementTravId( (Tim_Man_t *)p->pManTime );
579         Aig_ManSetCioIds( p );
580         Aig_ManForEachObj( p, pObj, i )
581         {
582             if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) )
583                 continue;
584             if ( Aig_ObjIsCi(pObj) )
585             {
586                 // copy the PI
587                 pObjNew = Aig_ObjCreateCi(pNew);
588                 pObj->pData = pObjNew;
589                 // set the arrival time of the new PI
590                 arrTime = Tim_ManGetCiArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj) );
591                 pObjNew->Level = (int)arrTime;
592             }
593             else if ( Aig_ObjIsCo(pObj) )
594             {
595                 // perform balancing
596                 pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
597                 pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
598                 if ( pObjNew == NULL )
599                 {
600                     Vec_VecFree( vStore );
601                     Aig_ManStop( pNew );
602                     return NULL;
603                 }
604                 pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
605                 // save arrival time of the output
606                 arrTime = (float)Aig_Regular(pObjNew)->Level;
607                 Tim_ManSetCoArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj), arrTime );
608                 // create PO
609                 pObjNew = Aig_ObjCreateCo( pNew, pObjNew );
610             }
611             else
612                 assert( 0 );
613         }
614         Aig_ManCleanCioIds( p );
615         pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 );
616     }
617     else
618     {
619         Aig_ManForEachCi( p, pObj, i )
620         {
621             pObjNew = Aig_ObjCreateCi(pNew);
622             pObjNew->Level = pObj->Level;
623             pObj->pData = pObjNew;
624         }
625         if ( p->nBarBufs == 0 )
626         {
627             Aig_ManForEachCo( p, pObj, i )
628             {
629                 pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
630                 pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
631                 if ( pObjNew == NULL )
632                 {
633                     Vec_VecFree( vStore );
634                     Aig_ManStop( pNew );
635                     return NULL;
636                 }
637                 pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
638                 pObjNew = Aig_ObjCreateCo( pNew, pObjNew );
639             }
640         }
641         else
642         {
643             Vec_Ptr_t * vLits = Vec_PtrStart( Aig_ManCoNum(p) );
644             Aig_ManForEachCo( p, pObj, i )
645             {
646                 int k = i < p->nBarBufs ? Aig_ManCoNum(p) - p->nBarBufs + i : i - p->nBarBufs;
647                 pObj = Aig_ManCo( p, k );
648                 pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
649                 pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
650                 if ( pObjNew == NULL )
651                 {
652                     Vec_VecFree( vStore );
653                     Aig_ManStop( pNew );
654                     return NULL;
655                 }
656                 pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
657                 Vec_PtrWriteEntry( vLits, k, pObjNew );
658                 if ( i < p->nBarBufs )
659                     Aig_ManCi(pNew, Aig_ManCiNum(p) - p->nBarBufs + i)->Level = Aig_Regular(pObjNew)->Level;
660             }
661             Aig_ManForEachCo( p, pObj, i )
662                 Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrEntry(vLits, i) );
663             Vec_PtrFree(vLits);
664         }
665     }
666     Vec_VecFree( vStore );
667     // remove dangling nodes
668     Aig_ManCleanup( pNew );
669     Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
670     // check the resulting AIG
671     if ( !Aig_ManCheck(pNew) )
672         printf( "Dar_ManBalance(): The check has failed.\n" );
673     return pNew;
674 }
675 
676 /**Function*************************************************************
677 
678   Synopsis    [Reproduces script "compress2".]
679 
680   Description []
681 
682   SideEffects []
683 
684   SeeAlso     []
685 
686 ***********************************************************************/
Dar_ManBalanceXor(Aig_Man_t * pAig,int fExor,int fUpdateLevel,int fVerbose)687 Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose )
688 {
689     Aig_Man_t * pAigXor, * pRes;
690     if ( fExor )
691     {
692         pAigXor = Aig_ManDupExor( pAig );
693         if ( fVerbose )
694             Dar_BalancePrintStats( pAigXor );
695         pRes = Dar_ManBalance( pAigXor, fUpdateLevel );
696         Aig_ManStop( pAigXor );
697     }
698     else
699     {
700         pRes = Dar_ManBalance( pAig, fUpdateLevel );
701     }
702     return pRes;
703 }
704 
705 /**Function*************************************************************
706 
707   Synopsis    [Inserts a new node in the order by levels.]
708 
709   Description []
710 
711   SideEffects []
712 
713   SeeAlso     []
714 
715 ***********************************************************************/
Dar_BalancePrintStats(Aig_Man_t * p)716 void Dar_BalancePrintStats( Aig_Man_t * p )
717 {
718     Vec_Ptr_t * vSuper;
719     Aig_Obj_t * pObj, * pTemp;
720     int i, k;
721     if ( Aig_ManExorNum(p) == 0 )
722     {
723         printf( "There is no EXOR gates.\n" );
724         return;
725     }
726     Aig_ManForEachExor( p, pObj, i )
727     {
728         Aig_ObjFanin0(pObj)->fMarkA = 1;
729         Aig_ObjFanin1(pObj)->fMarkA = 1;
730         assert( !Aig_ObjFaninC0(pObj) );
731         assert( !Aig_ObjFaninC1(pObj) );
732     }
733     vSuper = Vec_PtrAlloc( 1000 );
734     Aig_ManForEachExor( p, pObj, i )
735     {
736         if ( pObj->fMarkA && pObj->nRefs == 1 )
737             continue;
738         Vec_PtrClear( vSuper );
739         Dar_BalanceCone_rec( pObj, pObj, vSuper );
740         Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pTemp, k )
741             pTemp->fMarkB = 0;
742         if ( Vec_PtrSize(vSuper) < 3 )
743             continue;
744         printf( "  %d(", Vec_PtrSize(vSuper) );
745         Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pTemp, k )
746             printf( " %d", pTemp->Level );
747         printf( " )" );
748     }
749     Vec_PtrFree( vSuper );
750     Aig_ManForEachObj( p, pObj, i )
751         pObj->fMarkA = 0;
752     printf( "\n" );
753 }
754 
755 ////////////////////////////////////////////////////////////////////////
756 ///                       END OF FILE                                ///
757 ////////////////////////////////////////////////////////////////////////
758 
759 
760 ABC_NAMESPACE_IMPL_END
761 
762