Version abc80329

1 files changed, 255 insertions, 201 deletions

diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index 03707481..63f6f232 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -25,151 +25,12 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level, int fUpdateLevel );
-static Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level );
-static int         Dar_BalanceFindLeft( Vec_Ptr_t * vSuper );
-static void        Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor );
-static void        Dar_BalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj );
-static Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Performs algebraic balancing of the AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
-{
-    Aig_Man_t * pNew;
-    Aig_Obj_t * pObj, * pDriver, * pObjNew;
-    Vec_Vec_t * vStore;
-    int i;
-    // create the new manager 
-    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->nRegs = p->nRegs;
-    pNew->nAsserts = p->nAsserts;
-    if ( p->vFlopNums )
-        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
-    // map the PI nodes
-    Aig_ManCleanData( p );
-    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    vStore = Vec_VecAlloc( 50 );
-    if ( p->pManTime != NULL )
-    {
-        float arrTime;
-        Tim_ManIncrementTravId( p->pManTime );
-        Aig_ManSetPioNumbers( p );
-        Aig_ManForEachObj( p, pObj, i )
-        {
-            if ( Aig_ObjIsAnd(pObj) || Aig_ObjIsConst1(pObj) )
-                continue;
-            if ( Aig_ObjIsPi(pObj) )
-            {
-                // copy the PI
-                pObjNew = Aig_ObjCreatePi(pNew); 
-                pObj->pData = pObjNew;
-                // set the arrival time of the new PI
-                arrTime = Tim_ManGetPiArrival( p->pManTime, Aig_ObjPioNum(pObj) );
-                pObjNew->Level = (int)arrTime;
-            }
-            else if ( Aig_ObjIsPo(pObj) )
-            {
-                // perform balancing
-                pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
-                pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
-                pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
-                Aig_ObjCreatePo( pNew, pObjNew );
-                // save arrival time of the output
-                arrTime = (float)Aig_Regular(pObjNew)->Level;
-                Tim_ManSetPoArrival( p->pManTime, Aig_ObjPioNum(pObj), arrTime );
-            }
-            else
-                assert( 0 );
-        }
-        Aig_ManCleanPioNumbers( p );
-        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
-    }
-    else
-    {
-        Aig_ManForEachPi( p, pObj, i )
-        {
-            pObjNew = Aig_ObjCreatePi(pNew); 
-            pObjNew->Level = pObj->Level;
-            pObj->pData = pObjNew;
-        }
-        Aig_ManForEachPo( p, pObj, i )
-        {
-            pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
-            pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
-            pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
-            Aig_ObjCreatePo( pNew, pObjNew );
-        }
-    }
-    Vec_VecFree( vStore );
-    // remove dangling nodes
-    Aig_ManCleanup( pNew );
-    // check the resulting AIG
-    if ( !Aig_ManCheck(pNew) )
-        printf( "Dar_ManBalance(): The check has failed.\n" );
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the new node constructed.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel )
-{
-    Aig_Obj_t * pObjNew;
-    Vec_Ptr_t * vSuper;
-    int i;
-    assert( !Aig_IsComplement(pObjOld) );
-    assert( !Aig_ObjIsBuf(pObjOld) );
-    // return if the result is known
-    if ( pObjOld->pData )
-        return pObjOld->pData;
-    assert( Aig_ObjIsNode(pObjOld) );
-    // get the implication supergate
-    vSuper = Dar_BalanceCone( pObjOld, vStore, Level );
-    // check if supergate contains two nodes in the opposite polarity
-    if ( vSuper->nSize == 0 )
-        return pObjOld->pData = Aig_ManConst0(pNew);
-    if ( Vec_PtrSize(vSuper) < 2 )
-        printf( "BUG!\n" );
-    // for each old node, derive the new well-balanced node
-    for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
-    {
-        pObjNew = Dar_Balance_rec( pNew, Aig_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
-        vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement(vSuper->pArray[i]) );
-    }
-    // build the supergate
-    pObjNew = Dar_BalanceBuildSuper( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel );
-    // make sure the balanced node is not assigned
-//    assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level );
-    assert( pObjOld->pData == NULL );
-    Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig;
-    return pObjOld->pData = pObjNew;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Collects the nodes of the supergate.]
 
   Description []
@@ -185,14 +46,26 @@ int Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper
     // check if the node is visited
     if ( Aig_Regular(pObj)->fMarkB )
     {
-        // check if the node occurs in the same polarity
-        for ( i = 0; i < vSuper->nSize; i++ )
-            if ( vSuper->pArray[i] == pObj )
-                return 1;
-        // check if the node is present in the opposite polarity
-        for ( i = 0; i < vSuper->nSize; i++ )
-            if ( vSuper->pArray[i] == Aig_Not(pObj) )
-                return -1;
+        if ( Aig_ObjIsExor(pRoot) )
+        {
+            assert( !Aig_IsComplement(pObj) );
+            // check if the node occurs in the same polarity
+            Vec_PtrRemove( vSuper, pObj );
+            Aig_Regular(pObj)->fMarkB = 0;
+//printf( " Duplicated EXOR input!!! " );
+            return 1;
+        }
+        else
+        {
+            // check if the node occurs in the same polarity
+            for ( i = 0; i < vSuper->nSize; i++ )
+                if ( vSuper->pArray[i] == pObj )
+                    return 1;
+            // check if the node is present in the opposite polarity
+            for ( i = 0; i < vSuper->nSize; i++ )
+                if ( vSuper->pArray[i] == Aig_Not(pObj) )
+                    return -1;
+        }
         assert( 0 );
         return 0;
     }
@@ -251,60 +124,6 @@ Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
 
 /**Function*************************************************************
 
-  Synopsis    [Procedure used for sorting the nodes in decreasing order of levels.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_NodeCompareLevelsDecrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
-{
-    int Diff = Aig_ObjLevel(Aig_Regular(*pp1)) - Aig_ObjLevel(Aig_Regular(*pp2));
-    if ( Diff > 0 )
-        return -1;
-    if ( Diff < 0 ) 
-        return 1;
-    return 0; 
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Builds implication supergate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel )
-{
-    Aig_Obj_t * pObj1, * pObj2;
-    int LeftBound;
-    assert( vSuper->nSize > 1 );
-    // sort the new nodes by level in the decreasing order
-    Vec_PtrSort( vSuper, Aig_NodeCompareLevelsDecrease );
-    // balance the nodes
-    while ( vSuper->nSize > 1 )
-    {
-        // find the left bound on the node to be paired
-        LeftBound = (!fUpdateLevel)? 0 : Dar_BalanceFindLeft( vSuper );
-        // find the node that can be shared (if no such node, randomize choice)
-        Dar_BalancePermute( p, vSuper, LeftBound, Type == AIG_OBJ_EXOR );
-        // pull out the last two nodes
-        pObj1 = Vec_PtrPop(vSuper);
-        pObj2 = Vec_PtrPop(vSuper);
-        Dar_BalancePushUniqueOrderByLevel( vSuper, Aig_Oper(p, pObj1, pObj2, Type) );
-    }
-    return Vec_PtrEntry(vSuper, 0);
-}
-
-/**Function*************************************************************
-
   Synopsis    [Finds the left bound on the next candidate to be paired.]
 
   Description [The nodes in the array are in the decreasing order of levels. 
@@ -405,6 +224,27 @@ void Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int f
 
 /**Function*************************************************************
 
+  Synopsis    [Procedure used for sorting the nodes in decreasing order of levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NodeCompareLevelsDecrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
+{
+    int Diff = Aig_ObjLevel(Aig_Regular(*pp1)) - Aig_ObjLevel(Aig_Regular(*pp2));
+    if ( Diff > 0 )
+        return -1;
+    if ( Diff < 0 ) 
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
   Synopsis    [Inserts a new node in the order by levels.]
 
   Description []
@@ -432,6 +272,220 @@ void Dar_BalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Builds implication supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel )
+{
+    Aig_Obj_t * pObj1, * pObj2;
+    int LeftBound;
+    assert( vSuper->nSize > 1 );
+    // sort the new nodes by level in the decreasing order
+    Vec_PtrSort( vSuper, Aig_NodeCompareLevelsDecrease );
+    // balance the nodes
+    while ( vSuper->nSize > 1 )
+    {
+        // find the left bound on the node to be paired
+        LeftBound = (!fUpdateLevel)? 0 : Dar_BalanceFindLeft( vSuper );
+        // find the node that can be shared (if no such node, randomize choice)
+        Dar_BalancePermute( p, vSuper, LeftBound, Type == AIG_OBJ_EXOR );
+        // pull out the last two nodes
+        pObj1 = Vec_PtrPop(vSuper);
+        pObj2 = Vec_PtrPop(vSuper);
+        Dar_BalancePushUniqueOrderByLevel( vSuper, Aig_Oper(p, pObj1, pObj2, Type) );
+    }
+    return Vec_PtrEntry(vSuper, 0);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the new node constructed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel )
+{
+    Aig_Obj_t * pObjNew;
+    Vec_Ptr_t * vSuper;
+    int i;
+    assert( !Aig_IsComplement(pObjOld) );
+    assert( !Aig_ObjIsBuf(pObjOld) );
+    // return if the result is known
+    if ( pObjOld->pData )
+        return pObjOld->pData;
+    assert( Aig_ObjIsNode(pObjOld) );
+    // get the implication supergate
+    vSuper = Dar_BalanceCone( pObjOld, vStore, Level );
+    // check if supergate contains two nodes in the opposite polarity
+    if ( vSuper->nSize == 0 )
+        return pObjOld->pData = Aig_ManConst0(pNew);
+    if ( Vec_PtrSize(vSuper) < 2 )
+        printf( "BUG!\n" );
+    // for each old node, derive the new well-balanced node
+    for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
+    {
+        pObjNew = Dar_Balance_rec( pNew, Aig_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
+        vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement(vSuper->pArray[i]) );
+    }
+    // build the supergate
+    pObjNew = Dar_BalanceBuildSuper( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel );
+    // make sure the balanced node is not assigned
+//    assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level );
+    assert( pObjOld->pData == NULL );
+    Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig;
+    return pObjOld->pData = pObjNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs algebraic balancing of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pDriver, * pObjNew;
+    Vec_Vec_t * vStore;
+    int i;
+    // create the new manager 
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->nRegs = p->nRegs;
+    pNew->nAsserts = p->nAsserts;
+    if ( p->vFlopNums )
+        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+    // map the PI nodes
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    vStore = Vec_VecAlloc( 50 );
+    if ( p->pManTime != NULL )
+    {
+        float arrTime;
+        Tim_ManIncrementTravId( p->pManTime );
+        Aig_ManSetPioNumbers( p );
+        Aig_ManForEachObj( p, pObj, i )
+        {
+            if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) )
+                continue;
+            if ( Aig_ObjIsPi(pObj) )
+            {
+                // copy the PI
+                pObjNew = Aig_ObjCreatePi(pNew); 
+                pObj->pData = pObjNew;
+                // set the arrival time of the new PI
+                arrTime = Tim_ManGetPiArrival( p->pManTime, Aig_ObjPioNum(pObj) );
+                pObjNew->Level = (int)arrTime;
+            }
+            else if ( Aig_ObjIsPo(pObj) )
+            {
+                // perform balancing
+                pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
+                pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
+                pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
+                Aig_ObjCreatePo( pNew, pObjNew );
+                // save arrival time of the output
+                arrTime = (float)Aig_Regular(pObjNew)->Level;
+                Tim_ManSetPoArrival( p->pManTime, Aig_ObjPioNum(pObj), arrTime );
+            }
+            else
+                assert( 0 );
+        }
+        Aig_ManCleanPioNumbers( p );
+        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+    }
+    else
+    {
+        Aig_ManForEachPi( p, pObj, i )
+        {
+            pObjNew = Aig_ObjCreatePi(pNew); 
+            pObjNew->Level = pObj->Level;
+            pObj->pData = pObjNew;
+        }
+        Aig_ManForEachPo( p, pObj, i )
+        {
+            pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
+            pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
+            pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
+            Aig_ObjCreatePo( pNew, pObjNew );
+        }
+    }
+    Vec_VecFree( vStore );
+    // remove dangling nodes
+    Aig_ManCleanup( pNew );
+    // check the resulting AIG
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Dar_ManBalance(): The check has failed.\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts a new node in the order by levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_BalancePrintStats( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vSuper;
+    Aig_Obj_t * pObj, * pTemp;
+    int i, k;
+    if ( Aig_ManExorNum(p) == 0 )
+    {
+        printf( "There is no EXOR gates.\n" );
+        return;
+    }
+    Aig_ManForEachExor( p, pObj, i )
+    {
+        Aig_ObjFanin0(pObj)->fMarkA = 1;
+        Aig_ObjFanin1(pObj)->fMarkA = 1;
+        assert( !Aig_ObjFaninC0(pObj) );
+        assert( !Aig_ObjFaninC1(pObj) );
+    }
+    vSuper = Vec_PtrAlloc( 1000 );
+    Aig_ManForEachExor( p, pObj, i )
+    {
+        if ( pObj->fMarkA && pObj->nRefs == 1 )
+            continue;
+        Vec_PtrClear( vSuper );
+        Dar_BalanceCone_rec( pObj, pObj, vSuper );
+        Vec_PtrForEachEntry( vSuper, pTemp, k )
+            pTemp->fMarkB = 0;
+        if ( Vec_PtrSize(vSuper) < 3 )
+            continue;
+        printf( "  %d(", Vec_PtrSize(vSuper) );
+        Vec_PtrForEachEntry( vSuper, pTemp, k )
+            printf( " %d", pTemp->Level );
+        printf( " )" );
+    }
+    Vec_PtrFree( vSuper );
+    Aig_ManForEachObj( p, pObj, i )
+        pObj->fMarkA = 0;
+    printf( "\n" );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///