Important bug fix in XOR balancing (balance -x).

1 files changed, 91 insertions, 185 deletions

diff --git a/src/opt/dar/darBalance.c b/src/opt/dar/darBalance.c
index 484b86e7..34559bec 100644
--- a/src/opt/dar/darBalance.c
+++ b/src/opt/dar/darBalance.c
@@ -34,15 +34,9 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-
-
-static inline word  Dar_BalPack( int Lev, int Id )  { return (((word)Lev) << 32) | Id; }
-static inline int   Dar_BalUnpackLev( word Num )    { return (Num >> 32);              }
-static inline int   Dar_BalUnpackId( word Num )     { return Num & 0xFFFF;             }
-
 /**Function*************************************************************
 
-  Synopsis    [Collects one multi-input gate.]
+  Synopsis    [Uniqifies the node.]
 
   Description []
                
@@ -51,131 +45,92 @@ static inline int   Dar_BalUnpackId( word Num )     { return Num & 0xFFFF;
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Wrd_t * Dar_BalSuperXor( Aig_Man_t * p, Aig_Obj_t * pObj, int * pfCompl )
+int Dar_ObjCompareLits( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
 {
-    Aig_Obj_t * pObj0, * pObj1, * pRoot = NULL;
-    Vec_Wrd_t * vSuper;
-    word Num, NumNext;
-    int i, k, fCompl = 0;
-    assert( !Aig_IsComplement(pObj) );
-    assert( Aig_ObjIsExor(pObj) );
-    // start iteration
-    vSuper = Vec_WrdAlloc( 10 );
-    Vec_WrdPush( vSuper, Dar_BalPack(Aig_ObjLevel(pObj), Aig_ObjId(pObj)) );
-    while ( Vec_WrdSize(vSuper) > 0 && Vec_WrdSize(vSuper) < 10000 )
-    {
-        // make sure there are no duplicates
-        Num = Vec_WrdEntry( vSuper, 0 );
-        Vec_WrdForEachEntryStart( vSuper, NumNext, i, 1 )
-        {
-            assert( Num < NumNext );
-            Num = NumNext;
-        }
-        // extract XOR gate decomposable on the topmost level
-        Vec_WrdForEachEntryReverse( vSuper, Num, i )
-        {
-            pRoot = Aig_ManObj( p, Dar_BalUnpackId(Num) );
-            if ( Aig_ObjIsExor(pRoot) && Aig_ObjRefs(pRoot) == 1 )
-            {
-                Vec_WrdRemove( vSuper, Num );
-                break;
-            }
-        }
-        if ( i == -1 )
-            break;
-        // extract
-        assert( !Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) );
-        pObj0 = Aig_ObjChild0(pObj);
-        pObj1 = Aig_ObjChild1(pObj);
-        fCompl ^= Aig_IsComplement(pObj0);  pObj0 = Aig_Regular(pObj0);
-        fCompl ^= Aig_IsComplement(pObj1);  pObj1 = Aig_Regular(pObj1);
-        Vec_WrdPushOrder( vSuper, Dar_BalPack(Aig_ObjLevel(pObj0), Aig_ObjId(pObj0)) );
-        Vec_WrdPushOrder( vSuper, Dar_BalPack(Aig_ObjLevel(pObj1), Aig_ObjId(pObj1)) );
-        // remove duplicates
-        k = 0;
-        Vec_WrdForEachEntry( vSuper, Num, i )
-        {
-            if ( i + 1 == Vec_WrdSize(vSuper) )
-            {
-                Vec_WrdWriteEntry( vSuper, k++, Num );
-                break;
-            }
-            NumNext = Vec_WrdEntry( vSuper, i+1 );
-            assert( Num <= NumNext );
-            if ( Num == NumNext )
-                i++;
-            else
-                Vec_WrdWriteEntry( vSuper, k++, Num );
-        }
-        Vec_WrdShrink( vSuper, k );
-    }
-    *pfCompl = fCompl;
-    Vec_WrdForEachEntry( vSuper, Num, i )
-        Vec_WrdWriteEntry( vSuper, i, Dar_BalUnpackId(Num) );
-    return vSuper;
+    int Diff = Aig_ObjToLit(*pp1) - Aig_ObjToLit(*pp2);
+    if ( Diff < 0 )
+        return -1;
+    if ( Diff > 0 ) 
+        return 1;
+    return 0; 
 }
-Vec_Wrd_t * Dar_BalSuperAnd( Aig_Man_t * p, Aig_Obj_t * pObj )
+void Dar_BalanceUniqify( Aig_Obj_t * pObj, Vec_Ptr_t * vNodes, int fExor )
 {
-    Aig_Obj_t * pObj0, * pObj1, * pRoot = NULL;
-    Vec_Wrd_t * vSuper;
-    word Num, NumNext;
+    Aig_Obj_t * pTemp, * pTempNext;
     int i, k;
-    assert( !Aig_IsComplement(pObj) );
-    // start iteration
-    vSuper = Vec_WrdAlloc( 10 );
-    Vec_WrdPush( vSuper, Dar_BalPack(Aig_ObjLevel(pObj), Aig_ObjToLit(pObj)) );
-    while ( Vec_WrdSize(vSuper) > 0 && Vec_WrdSize(vSuper) < 10000 )
+    // sort the nodes by their literal
+    Vec_PtrSort( vNodes, (int (*)())Dar_ObjCompareLits );
+    // remove duplicates
+    k = 0;
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pTemp, i )
     {
-        // make sure there are no duplicates
-        Num = Vec_WrdEntry( vSuper, 0 );
-        Vec_WrdForEachEntryStart( vSuper, NumNext, i, 1 )
-        {
-            assert( Num < NumNext );
-            Num = NumNext;
-        }
-        // extract AND gate decomposable on the topmost level
-        Vec_WrdForEachEntryReverse( vSuper, Num, i )
+        if ( i + 1 == Vec_PtrSize(vNodes) )
         {
-            pRoot = Aig_ObjFromLit( p, Dar_BalUnpackId(Num) );
-            if ( !Aig_IsComplement(pRoot) && Aig_ObjIsNode(pRoot) && Aig_ObjRefs(pRoot) == 1 )
-            {
-                Vec_WrdRemove( vSuper, Num );
-                break;
-            }
-        }
-        if ( i == -1 )
+            Vec_PtrWriteEntry( vNodes, k++, pTemp );
             break;
-        // extract
-        pObj0 = Aig_ObjChild0(pRoot);
-        pObj1 = Aig_ObjChild1(pRoot);
-        Vec_WrdPushOrder( vSuper, Dar_BalPack(Aig_ObjLevel(Aig_Regular(pObj0)), Aig_ObjToLit(pObj0)) );
-        Vec_WrdPushOrder( vSuper, Dar_BalPack(Aig_ObjLevel(Aig_Regular(pObj1)), Aig_ObjToLit(pObj1)) );
-        // remove duplicates
-        k = 0;
-        Vec_WrdForEachEntry( vSuper, Num, i )
+        }
+        pTempNext = (Aig_Obj_t *)Vec_PtrEntry( vNodes, i+1 );
+        if ( !fExor && pTemp == Aig_Not(pTempNext) ) // pos_lit & neg_lit = 0
         {
-            if ( i + 1 == Vec_WrdSize(vSuper) )
-            {
-                Vec_WrdWriteEntry( vSuper, k++, Num );
-                break;
-            }
-            NumNext = Vec_WrdEntry( vSuper, i+1 );
-            assert( Num <= NumNext );
-            if ( Num + 1 == NumNext && (NumNext & 1) ) // pos_lit & neg_lit = 0
-            {
-                Vec_WrdClear( vSuper );
-                return vSuper;
-            }
-            if ( Num < NumNext )
-                Vec_WrdWriteEntry( vSuper, k++, Num );
+            Vec_PtrClear( vNodes );
+            return;
         }
-        Vec_WrdShrink( vSuper, k );
+        if ( pTemp != pTempNext )  // save if different
+            Vec_PtrWriteEntry( vNodes, k++, pTemp );
+        else if ( fExor ) // in case of XOR, remove identical
+            i++;
+    }
+    Vec_PtrShrink( vNodes, k );
+    // check that there is no duplicates
+    pTemp = (Aig_Obj_t *)Vec_PtrEntry( vNodes, 0 );
+    Vec_PtrForEachEntryStart( Aig_Obj_t *, vNodes, pTempNext, i, 1 )
+    {
+        assert( pTemp != pTempNext );
+        pTemp = pTempNext;
     }
-    Vec_WrdForEachEntry( vSuper, Num, i )
-        Vec_WrdWriteEntry( vSuper, i, Dar_BalUnpackId(Num) );
-    return vSuper;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Collects the nodes of the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
+{
+    if ( pObj != pRoot && (Aig_IsComplement(pObj) || Aig_ObjType(pObj) != Aig_ObjType(pRoot) || Aig_ObjRefs(pObj) > 1 || Vec_PtrSize(vSuper) > 10000) )
+        Vec_PtrPush( vSuper, pObj );
+    else
+    {
+        assert( !Aig_IsComplement(pObj) );
+        assert( Aig_ObjIsNode(pObj) );
+        // go through the branches
+        Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper );
+        Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper );
+    }
+}
+Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
+{
+    Vec_Ptr_t * vNodes;
+    assert( !Aig_IsComplement(pObj) );
+    assert( Aig_ObjIsNode(pObj) );
+    // extend the storage
+    if ( Vec_VecSize( vStore ) <= Level )
+        Vec_VecPush( vStore, Level, 0 );
+    // get the temporary array of nodes
+    vNodes = Vec_VecEntry( vStore, Level );
+    Vec_PtrClear( vNodes );
+    // collect the nodes in the implication supergate
+    Dar_BalanceCone_rec( pObj, pObj, vNodes );
+    // remove duplicates
+    Dar_BalanceUniqify( pObj, vNodes, Aig_ObjIsExor(pObj) );
+    return vNodes;
+}
 
 
 /**Function*************************************************************
@@ -189,6 +144,7 @@ Vec_Wrd_t * Dar_BalSuperAnd( Aig_Man_t * p, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
+/*
 int Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
 {
     int RetValue1, RetValue2, i;
@@ -235,19 +191,7 @@ int Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper
     // return 1 if at least one branch has a duplicate
     return RetValue1 || RetValue2;
 }
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the nodes of the supergate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Dar_BalanceCone( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
+Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
 {
     Vec_Ptr_t * vNodes;
     int RetValue, i;
@@ -270,50 +214,7 @@ Vec_Ptr_t * Dar_BalanceCone( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Vec_t * vStore
         vNodes->nSize = 0;
     return vNodes;
 }
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the nodes of the supergate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Dar_BalanceCone_( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
-{
-    Vec_Wrd_t * vSuper;
-    Vec_Ptr_t * vNodes;
-    word Num;
-    int i;
-    assert( !Aig_IsComplement(pObj) );
-    // extend the storage
-    if ( Vec_VecSize( vStore ) <= Level )
-        Vec_VecPush( vStore, Level, 0 );
-    // get the temporary array of nodes
-    vNodes = Vec_VecEntry( vStore, Level );
-    Vec_PtrClear( vNodes );
-    // collect the nodes in the implication supergate
-    // load the result into the output array
-    if ( Aig_ObjIsExor(pObj) )
-    {
-        int fCompl = 0;
-        vSuper = Dar_BalSuperXor( p, pObj, &fCompl ); 
-        Vec_WrdForEachEntry( vSuper, Num, i )
-            Vec_PtrPush( vNodes, Aig_ManObj(p, Dar_BalUnpackId(Num)) );
-        assert( fCompl == 0 );
-    }
-    else
-    {
-        vSuper = Dar_BalSuperAnd( p, pObj );
-        Vec_WrdForEachEntry( vSuper, Num, i )
-            Vec_PtrPush( vNodes, Aig_ObjFromLit(p, Dar_BalUnpackId(Num)) );
-    }
-    Vec_WrdFree( vSuper );
-    return vNodes;
-}
+*/
 
 /**Function*************************************************************
 
@@ -460,12 +361,16 @@ int Aig_NodeCompareLevelsDecrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
   SeeAlso     []
 
 ***********************************************************************/
-void Dar_BalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj )
+void Dar_BalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj, int fExor )
 {
     Aig_Obj_t * pObj1, * pObj2;
     int i;
     if ( Vec_PtrPushUnique(vStore, pObj) )
+    {
+        if ( fExor )
+            Vec_PtrRemove(vStore, pObj);
         return;
+    }
     // find the p of the node
     for ( i = vStore->nSize-1; i > 0; i-- )
     {
@@ -506,7 +411,7 @@ Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t
         // pull out the last two nodes
         pObj1 = (Aig_Obj_t *)Vec_PtrPop(vSuper);
         pObj2 = (Aig_Obj_t *)Vec_PtrPop(vSuper);
-        Dar_BalancePushUniqueOrderByLevel( vSuper, Aig_Oper(p, pObj1, pObj2, Type) );
+        Dar_BalancePushUniqueOrderByLevel( vSuper, Aig_Oper(p, pObj1, pObj2, Type), Type == AIG_OBJ_EXOR );
     }
     return (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0);
 }
@@ -576,7 +481,7 @@ Aig_Obj_t * Dar_BalanceBuildSuperTop( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Typ
         pObj = Dar_BalanceBuildSuper( p, vSubset, Type, fUpdateLevel );
         Vec_PtrFree( vSubset );
         // add the new output
-        Dar_BalancePushUniqueOrderByLevel( vSuper, pObj );
+        Dar_BalancePushUniqueOrderByLevel( vSuper, pObj, Type == AIG_OBJ_EXOR );
     }
     return (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0);
 }
@@ -592,7 +497,7 @@ Aig_Obj_t * Dar_BalanceBuildSuperTop( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Typ
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel )
+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;
@@ -604,7 +509,7 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObjOl
         return (Aig_Obj_t *)pObjOld->pData;
     assert( Aig_ObjIsNode(pObjOld) );
     // get the implication supergate
-    vSuper = Dar_BalanceCone( p, pObjOld, vStore, Level );
+    vSuper = Dar_BalanceCone( pObjOld, vStore, Level );
     // check if supergate contains two nodes in the opposite polarity
     if ( vSuper->nSize == 0 )
         return (Aig_Obj_t *)(pObjOld->pData = Aig_ManConst0(pNew));
@@ -615,7 +520,7 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObjOl
     // for each old node, derive the new well-balanced node
     for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
     {
-        pObjNew = Dar_Balance_rec( pNew, p, Aig_Regular((Aig_Obj_t *)vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
+        pObjNew = Dar_Balance_rec( pNew, Aig_Regular((Aig_Obj_t *)vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
         vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement((Aig_Obj_t *)vSuper->pArray[i]) );
     }
     // build the supergate
@@ -702,7 +607,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
             {
                 // perform balancing
                 pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
-                pObjNew = Dar_Balance_rec( pNew, p, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
+                pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
                 pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
                 // save arrival time of the output
                 arrTime = (float)Aig_Regular(pObjNew)->Level;
@@ -729,7 +634,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
         Aig_ManForEachCo( p, pObj, i )
         {
             pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
-            pObjNew = Dar_Balance_rec( pNew, p, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
+            pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
             pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
             pObjNew = Aig_ObjCreateCo( pNew, pObjNew );
             pObjNew->pHaig = pObj->pHaig;
@@ -828,5 +733,6 @@ void Dar_BalancePrintStats( Aig_Man_t * p )
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
+
 ABC_NAMESPACE_IMPL_END