Performance bug in k-resub and faster windowing.

2 files changed, 236 insertions, 26 deletions

diff --git a/src/aig/gia/giaResub.c b/src/aig/gia/giaResub.c
index b0b67c46..a1343290 100644
--- a/src/aig/gia/giaResub.c
+++ b/src/aig/gia/giaResub.c
@@ -1248,34 +1248,37 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit )
         Vec_IntPushTwo( p->vGates, iDiv0, Abc_Var2Lit(iNode, fComp1) );
         return Abc_Var2Lit( iNode+1, fComp );
     }
-    if ( nLimit == 2 )
-        return -1;
-    iResLit = Gia_ManFindGateGate( p->pSets, p->vDivs, p->nWords, p->vUnatePairs, p->vUnatePairsW, p->pDivA, p->pDivB );
-    if ( iResLit >= 0 ) // and(pair,pair)
+//    if ( nLimit == 2 )
+//        return -1;
+    if ( nLimit >= 3 )
     {
-        int iNode  = nVars + Vec_IntSize(p->vGates)/2;
+        iResLit = Gia_ManFindGateGate( p->pSets, p->vDivs, p->nWords, p->vUnatePairs, p->vUnatePairsW, p->pDivA, p->pDivB );
+        if ( iResLit >= 0 ) // and(pair,pair)
+        {
+            int iNode  = nVars + Vec_IntSize(p->vGates)/2;
 
-        int fComp  = Abc_LitIsCompl(iResLit);
-        int iDiv0  = Abc_Lit2Var(iResLit) & 0x7FFF; // pair
-        int iDiv1  = Abc_Lit2Var(iResLit) >> 15;    // pair
+            int fComp  = Abc_LitIsCompl(iResLit);
+            int iDiv0  = Abc_Lit2Var(iResLit) & 0x7FFF; // pair
+            int iDiv1  = Abc_Lit2Var(iResLit) >> 15;    // pair
 
-        int Div0   = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv0) );
-        int fComp0 = Abc_LitIsCompl(Div0) ^ Abc_LitIsCompl(iDiv0);
-        int iDiv00 = Abc_Lit2Var(Div0) & 0x7FFF;
-        int iDiv01 = Abc_Lit2Var(Div0) >> 15;   
+            int Div0   = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv0) );
+            int fComp0 = Abc_LitIsCompl(Div0) ^ Abc_LitIsCompl(iDiv0);
+            int iDiv00 = Abc_Lit2Var(Div0) & 0x7FFF;
+            int iDiv01 = Abc_Lit2Var(Div0) >> 15;   
         
-        int Div1   = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv1) );
-        int fComp1 = Abc_LitIsCompl(Div1) ^ Abc_LitIsCompl(iDiv1);
-        int iDiv10 = Abc_Lit2Var(Div1) & 0x7FFF;
-        int iDiv11 = Abc_Lit2Var(Div1) >> 15;   
+            int Div1   = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv1) );
+            int fComp1 = Abc_LitIsCompl(Div1) ^ Abc_LitIsCompl(iDiv1);
+            int iDiv10 = Abc_Lit2Var(Div1) & 0x7FFF;
+            int iDiv11 = Abc_Lit2Var(Div1) >> 15;   
         
-        Vec_IntPushTwo( p->vGates, iDiv00, iDiv01 );
-        Vec_IntPushTwo( p->vGates, iDiv10, iDiv11 );
-        Vec_IntPushTwo( p->vGates, Abc_Var2Lit(iNode, fComp0), Abc_Var2Lit(iNode+1, fComp1) );
-        return Abc_Var2Lit( iNode+2, fComp );
+            Vec_IntPushTwo( p->vGates, iDiv00, iDiv01 );
+            Vec_IntPushTwo( p->vGates, iDiv10, iDiv11 );
+            Vec_IntPushTwo( p->vGates, Abc_Var2Lit(iNode, fComp0), Abc_Var2Lit(iNode+1, fComp1) );
+            return Abc_Var2Lit( iNode+2, fComp );
+        }
     }
-    if ( nLimit == 3 )
-        return -1;
+//    if ( nLimit == 3 )
+//        return -1;
     if ( Vec_IntSize(p->vUnateLits[0]) + Vec_IntSize(p->vUnateLits[1]) + Vec_IntSize(p->vUnatePairs[0]) + Vec_IntSize(p->vUnatePairs[1]) == 0 )
         return -1;
 
@@ -1289,9 +1292,10 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit )
     Max2 = Abc_MaxInt(TopTwoW[0], TopTwoW[1]);
     if ( Abc_MaxInt(Max1, Max2) == 0 )
         return -1;
+
     if ( Max1 > Max2/2 )
     {
-        if ( Max1 == TopOneW[0] || Max1 == TopOneW[1] )
+        if ( nLimit >= 2 && (Max1 == TopOneW[0] || Max1 == TopOneW[1]) )
         {
             int fUseOr  = Max1 == TopOneW[0];
             int iDiv    = Vec_IntEntry( p->vUnateLits[!fUseOr], 0 );
@@ -1335,7 +1339,7 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit )
     }
     else
     {
-        if ( Max2 == TopTwoW[0] || Max2 == TopTwoW[1] )
+        if ( nLimit >= 3 && (Max2 == TopTwoW[0] || Max2 == TopTwoW[1]) )
         {
             int fUseOr  = Max2 == TopTwoW[0];
             int iDiv    = Vec_IntEntry( p->vUnatePairs[!fUseOr], 0 );
diff --git a/src/aig/gia/giaResub2.c b/src/aig/gia/giaResub2.c
index 23d73dd8..468730fe 100644
--- a/src/aig/gia/giaResub2.c
+++ b/src/aig/gia/giaResub2.c
@@ -540,7 +540,10 @@ Gia_Man_t * Gia_ManResub2Test( Gia_Man_t * p )
     //printf( "Performed resub %d times.  Reduced %d nodes.\n", nResubs, nObjsNew ? Gia_ManObjNum(p) - nObjsNew : 0 );
     Abc_ResubPrepareManager( 0 );
     if ( nObjsNew )
+    {
         pNew = Gia_ManFromResub( pObjsNew, nObjsNew, Gia_ManCiNum(p) );
+        pNew->pName = Abc_UtilStrsav( p->pName );
+    }
     else 
         pNew = Gia_ManDup( p );
     ABC_FREE( pObjs );
@@ -967,6 +970,193 @@ void Gia_RsbWindowGrow( Gia_Man_t * p, Vec_Wec_t * vLevels, Vec_Int_t * vWin, Ve
 
 /**Function*************************************************************
 
+  Synopsis    [Grow window for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+// uses levelized structure (vLevels) to collect in array vWin divisors supported by the cut (vIn)
+void Gia_WinCreateFromCut( Gia_Man_t * p, Vec_Int_t * vIn, Vec_Wec_t * vLevels, Vec_Int_t * vWin )
+{
+    Vec_Int_t * vLevel; 
+    Gia_Obj_t * pObj, * pFanout;
+    int k, i, f, iObj, Level;
+    Vec_Int_t * vUsed = Vec_IntAlloc( 100 );
+    // precondition:  the levelized structure is empty
+    assert( Vec_WecSizeSize(vLevels) == 0 );
+    // clean the resulting array
+    Vec_IntClear( vWin );
+    // start a new trav ID and add nodes to the levelized structure
+    Gia_ManIncrementTravId( p );
+    Vec_IntForEachEntry( vIn, iObj, i )
+    {
+        Gia_ObjSetTravIdCurrentId( p, iObj );
+        Vec_WecPush( vLevels, Gia_ObjLevelId(p, iObj), iObj );
+        Vec_IntPush( vWin, iObj );
+        Vec_IntPushUniqueOrder( vUsed, Gia_ObjLevelId(p, iObj) );
+    }
+    // iterate through all objects and explore their fanouts
+    //Vec_WecForEachLevel( vLevels, vLevel, k )
+    Vec_IntForEachEntry( vUsed, Level, k )
+    {
+        vLevel = Vec_WecEntry( vLevels, Level );
+        Gia_ManForEachObjVec( vLevel, p, pObj, i )
+            Gia_ObjForEachFanoutStatic( p, pObj, pFanout, f )
+            {
+                if ( f == 5 ) // explore first 5 fanouts of the node
+                    break;
+                if ( Gia_ObjIsAnd(pFanout) && // internal node
+                    !Gia_ObjIsTravIdCurrent(p, pFanout) && // not in the window
+                     Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin0(pFanout)) && // but fanins are
+                     Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin1(pFanout)) )  // in the window
+                {
+                    // add fanout to the window and to the levelized structure
+                    Gia_ObjSetTravIdCurrent( p, pFanout );
+                    Vec_WecPush( vLevels, Gia_ObjLevel(p, pFanout), Gia_ObjId(p, pFanout) );
+                    Vec_IntPush( vWin, Gia_ObjId(p, pFanout) );
+                    Vec_IntPushUniqueOrder( vUsed, Gia_ObjLevel(p, pFanout) );
+                }
+            }
+        Vec_IntClear( vLevel );
+    }
+    Vec_IntSort( vWin, 0 );
+    Vec_IntFree( vUsed );
+}
+// update the cut until both fanins of AND nodes are not in the cut
+int Gia_RsbExpandCut( Gia_Man_t * p, Vec_Int_t * vIns )
+{
+    int fOnlyPis = 0, fChange = 1, nSize = Vec_IntSize(vIns);
+    while ( fChange )
+    {
+        Gia_Obj_t * pObj;
+        int i, iFan0, iFan1, fHave0, fHave1;
+        fOnlyPis = 1;
+        fChange = 0;
+        // check if some nodes can be expanded without increasing cut size
+        Gia_ManForEachObjVec( vIns, p, pObj, i )
+        {
+            assert( Gia_ObjIsTravIdCurrent(p, pObj) );
+            if ( !Gia_ObjIsAnd(pObj) )
+                continue;
+            fOnlyPis = 0;
+            iFan0 = Gia_ObjFaninId0p(p, pObj);
+            iFan1 = Gia_ObjFaninId1p(p, pObj);
+            fHave0 = Gia_ObjIsTravIdCurrentId(p, iFan0);
+            fHave1 = Gia_ObjIsTravIdCurrentId(p, iFan1);
+            if ( !fHave0 && !fHave1 )
+                continue;
+            // can expand because one of the fanins is already in the cut
+            // remove current cut node
+            Vec_IntDrop( vIns, i );
+            // add missing fanin
+            if ( !fHave0 )  
+            {
+                Vec_IntPush( vIns, iFan0 );
+                Gia_ObjSetTravIdCurrentId( p, iFan0 );
+            }
+            if ( !fHave1 )  
+            {
+                Vec_IntPush( vIns, iFan1 );
+                Gia_ObjSetTravIdCurrentId( p, iFan1 );
+            }
+            fChange = 1;
+            break;
+        }
+    }
+    assert( Vec_IntSize(vIns) <= nSize );
+    return fOnlyPis;
+}
+int Gia_RsbFindFaninAdd( int iFan, int pFanins[32], int pFaninCounts[32], int nFanins )
+{
+    int i;
+    for ( i = 0; i < nFanins; i++ )
+        if ( pFanins[i] == iFan )
+            break;
+    pFanins[i] = iFan;
+    pFaninCounts[i]++;
+    return nFanins + (i == nFanins);
+}                        
+int Gia_RsbFindFaninToAddToCut( Gia_Man_t * p, Vec_Int_t * vIns )
+{
+    Gia_Obj_t * pObj;
+    int nFanins = 0, pFanins[64] = {0}, pFaninCounts[64] = {0};
+    int i, iFan0, iFan1, iFanMax = -1, CountMax = 0;
+    Gia_ManForEachObjVec( vIns, p, pObj, i )
+    {
+        if ( !Gia_ObjIsAnd(pObj) )
+            continue;
+        iFan0 = Gia_ObjFaninId0p(p, pObj);
+        iFan1 = Gia_ObjFaninId1p(p, pObj);
+        assert( !Gia_ObjIsTravIdCurrentId(p, iFan0) );
+        assert( !Gia_ObjIsTravIdCurrentId(p, iFan1) );
+        nFanins = Gia_RsbFindFaninAdd( iFan0, pFanins, pFaninCounts, nFanins );
+        nFanins = Gia_RsbFindFaninAdd( iFan1, pFanins, pFaninCounts, nFanins );
+        assert( nFanins < 64 );
+    }
+    // find fanin with the highest count
+    for ( i = 0; i < nFanins; i++ )
+        if ( CountMax < pFaninCounts[i] )
+        {
+            CountMax = pFaninCounts[i];
+            iFanMax  = pFanins[i];
+        }
+    return iFanMax;
+}
+// precondition: nodes in vWin and in vIns are marked with the current ID
+void Gia_RsbWindowGrow2( Gia_Man_t * p, Vec_Wec_t * vLevels, Vec_Int_t * vWin, Vec_Int_t * vIns, int nInputsMax )
+{
+    // window will be recomputed later
+    Vec_IntClear( vWin );
+    // expand the cut without increasing its cost
+    if ( !Gia_RsbExpandCut( p, vIns ) )
+    {
+        // save it as the best cut
+        Vec_Int_t * vBest = Vec_IntSize(vIns) <= nInputsMax ? Vec_IntDup(vIns) : NULL;
+        int fOnlyPis = 0, Iter = 0;
+        // iterate expansion until  
+        // (1) the cut cannot be expanded because all leaves are PIs
+        // (2) the cut size exceeded the limit for 5 consecutive iterations
+        while ( !fOnlyPis && (Vec_IntSize(vIns) <= nInputsMax || Iter < 5) )
+        {
+            int iFanBest = Gia_RsbFindFaninToAddToCut( p, vIns );
+            Vec_IntPush( vIns, iFanBest );
+            Gia_ObjSetTravIdCurrentId( p, iFanBest );
+            fOnlyPis = Gia_RsbExpandCut( p, vIns );
+            if ( Vec_IntSize(vIns) > nInputsMax )
+                Iter++;
+            else
+                Iter = 0;                
+            if ( Vec_IntSize(vIns) <= nInputsMax && (!vBest || Vec_IntSize(vBest) <= Vec_IntSize(vIns)) )
+            {
+                if ( vBest )
+                    Vec_IntClear(vBest);
+                else
+                    vBest = Vec_IntAlloc( 10 );
+                Vec_IntAppend( vBest, vIns );
+            }
+        }
+        if ( vBest )
+        {
+            Vec_IntClear( vIns );
+            Vec_IntAppend( vIns, vBest );
+            Vec_IntFree( vBest );
+        }
+        else
+            assert( Vec_IntSize(vIns) > nInputsMax );
+    }
+    if ( Vec_IntSize(vIns) <= nInputsMax )
+    {
+        Vec_IntSort( vIns, 0 );
+        Gia_WinCreateFromCut( p, vIns, vLevels, vWin );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Create window for the node.]
 
   Description []
@@ -987,8 +1177,8 @@ int Gia_RsbWindowCompute( Gia_Man_t * p, int iObj, int nInputsMax, int nLevelsMa
     // vWin and vIns are labeled with the current trav ID
     //Vec_IntPrint( vWin );    
     //Vec_IntPrint( vIns );    
-    if ( Vec_IntSize(vIns) <= nInputsMax + 2 ) // consider windows, which initially has a larger input space
-        Gia_RsbWindowGrow( p, vLevels, vWin, vIns, nInputsMax );
+    if ( Vec_IntSize(vIns) <= nInputsMax + 3 ) // consider windows, which initially has a larger input space
+        Gia_RsbWindowGrow2( p, vLevels, vWin, vIns, nInputsMax );
     if ( Vec_IntSize(vIns) <= nInputsMax )
     {
         Vec_IntSort( vWin, 0 );
@@ -1208,6 +1398,22 @@ void Gia_RsbEnumerateWindows( Gia_Man_t * p, int nInputsMax, int nLevelsMax )
     Hsh_VecManStop( pHash );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Apply k-resub to one AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_RsbTryOneWindow( Gia_Man_t * p )
+{
+    return Gia_ManResub2Test( p );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////