Logic restructuring after mapping.

4 files changed, 334 insertions, 50 deletions

diff --git a/src/base/acb/acb.h b/src/base/acb/acb.h
index 7c228acb..baecd161 100644
--- a/src/base/acb/acb.h
+++ b/src/base/acb/acb.h
@@ -256,7 +256,8 @@ static inline int *          Acb_ObjFanins( Acb_Ntk_t * p, int i )
 static inline int            Acb_ObjFanin( Acb_Ntk_t * p, int i, int k )             { return Acb_ObjFanins(p, i)[k+1];                                                                     }
 static inline int            Acb_ObjFaninNum( Acb_Ntk_t * p, int i )                 { return Acb_ObjFanins(p, i)[0];                                                                       }
 static inline int            Acb_ObjFanoutNum( Acb_Ntk_t * p, int i )                { return Vec_IntSize( Vec_WecEntry(&p->vFanouts, i) );                                                 }
-static inline Vec_Int_t *    Acb_ObjFanoutVec( Acb_Ntk_t * p, int i )                { return Vec_WecEntry( &p->vFanouts, i );                                                              }
+static inline Vec_Int_t *    Acb_ObjFanoutVec( Acb_Ntk_t * p, int i )                { assert(i>0); return Vec_WecEntry( &p->vFanouts, i );                                                 }
+static inline int            Acb_ObjFanout( Acb_Ntk_t * p, int i, int k )            { return Vec_IntEntry( Acb_ObjFanoutVec(p, i), k );                                                    }
 static inline int            Acb_ObjFanin0( Acb_Ntk_t * p, int i )                   { return Acb_ObjFanins(p, i)[1];                                                                       }
 static inline int            Acb_ObjCioId( Acb_Ntk_t * p, int i )                    { return Acb_ObjFanins(p, i)[2];                                                                       }
  
@@ -276,7 +277,6 @@ static inline int            Acb_ObjLevelR( Acb_Ntk_t * p, int i )
 static inline int            Acb_ObjPathD( Acb_Ntk_t * p, int i )                    { assert(i>0); return Vec_IntEntry(&p->vPathD, i);                                                     }
 static inline int            Acb_ObjPathR( Acb_Ntk_t * p, int i )                    { assert(i>0); return Vec_IntEntry(&p->vPathR, i);                                                     }
 static inline float          Acb_ObjCounts( Acb_Ntk_t * p, int i )                   { assert(i>0); return Vec_FltEntry(&p->vCounts, i);                                                    }
-static inline Vec_Int_t *    Acb_ObjFanout( Acb_Ntk_t * p, int i )                   { assert(i>0); return Vec_WecEntry(&p->vFanouts, i);                                                   }
 static inline Vec_Str_t *    Acb_ObjCnfs( Acb_Ntk_t * p, int i )                     { assert(i>0); return (Vec_Str_t *)Vec_WecEntry(&p->vCnfs, i);                                         }
 
 static inline void           Acb_ObjSetCopy( Acb_Ntk_t * p, int i, int x )           { assert(Acb_ObjCopy(p, i) == -1); Vec_IntWriteEntry( &p->vObjCopy, i, x );                            }
@@ -361,6 +361,8 @@ static inline void           Acb_NtkIncTravId( Acb_Ntk_t * p )
     for ( i = Vec_StrSize(&p->vObjType)-1; i > 0; i-- ) if ( !Acb_ObjType(p, i) ) {} else   
 #define Acb_NtkForEachNode( p, i )                                        \
     for ( i = 1; i < Vec_StrSize(&p->vObjType); i++ ) if ( !Acb_ObjType(p, i) || Acb_ObjIsCio(p, i) ) {} else   
+#define Acb_NtkForEachNodeSupp( p, i, nSuppSize )                         \
+    for ( i = 1; i < Vec_StrSize(&p->vObjType); i++ ) if ( !Acb_ObjType(p, i) || Acb_ObjIsCio(p, i) || Acb_ObjFaninNum(p, i) != nSuppSize ) {} else   
 #define Acb_NtkForEachNodeReverse( p, i )                                 \
     for ( i = Vec_StrSize(&p->vObjType)-1; i > 0; i-- ) if ( !Acb_ObjType(p, i) || Acb_ObjIsCio(p, i) ) {} else   
 #define Acb_NtkForEachObjType( p, Type, i )                               \
@@ -403,12 +405,35 @@ static inline int Acb_ObjFonNum( Acb_Ntk_t * p, int iObj )
         Count++;
     return Count;
 }
+static inline int Acb_ObjWhatFanin( Acb_Ntk_t * p, int iObj, int iFaninGiven )
+{
+    int k, iFanin, * pFanins;
+    Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
+        if ( iFanin == iFaninGiven )
+            return k;
+    return -1;
+}
 static inline void Acb_ObjAddFanin( Acb_Ntk_t * p, int iObj, int iFanin )
 {
     int * pFanins = Acb_ObjFanins( p, iObj );
     assert( pFanins[ 1 + pFanins[0] ] == -1 );
     pFanins[ 1 + pFanins[0]++ ] = iFanin;
 }
+static inline void Acb_ObjDeleteFaninIndex( Acb_Ntk_t * p, int iObj, int iFaninIndex )
+{
+    int i, * pFanins = Acb_ObjFanins( p, iObj );
+    pFanins[0]--;
+    for ( i = iFaninIndex; i < pFanins[0]; i++ )
+        pFanins[ 1 + i ] = pFanins[ 2 + i ];
+    pFanins[ 1 + pFanins[0] ] = -1;
+}
+static inline void Acb_ObjDeleteFanin( Acb_Ntk_t * p, int iObj, int iFanin )
+{
+    int * pFanins = Acb_ObjFanins( p, iObj );
+    int iFaninIndex = Acb_ObjWhatFanin( p, iObj, iFanin );
+    assert( pFanins[ 1 + iFaninIndex ] == iFanin );
+    Acb_ObjDeleteFaninIndex( p, iObj, iFaninIndex );
+}
 static inline void Acb_ObjAddFanins( Acb_Ntk_t * p, int iObj, Vec_Int_t * vFanins )
 {
     int i, iFanin;
@@ -495,12 +520,23 @@ static inline void Acb_ObjDelete( Acb_Ntk_t * p, int iObj )
     Acb_ObjForEachFon( p, iObj, i )
         Acb_ObjCleanType( p, i );
 }
+static inline void Acb_ObjAddFaninFanoutOne( Acb_Ntk_t * p, int iObj, int iFanin )
+{
+    Vec_IntPush( Vec_WecEntry(&p->vFanouts, iFanin), iObj );
+    Acb_ObjAddFanin( p, iObj, iFanin );
+}
 static inline void Acb_ObjAddFaninFanout( Acb_Ntk_t * p, int iObj )
 {
     int k, iFanin, * pFanins; 
     Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
         Vec_IntPush( Vec_WecEntry(&p->vFanouts, iFanin), iObj );
 }
+static inline void Acb_ObjRemoveFaninFanoutOne( Acb_Ntk_t * p, int iObj, int iFanin )
+{
+    int RetValue = Vec_IntRemove( Vec_WecEntry(&p->vFanouts, iFanin), iObj );
+    assert( RetValue );
+    Acb_ObjDeleteFanin( p, iObj, iFanin );
+}
 static inline void Acb_ObjRemoveFaninFanout( Acb_Ntk_t * p, int iObj )
 {
     int k, iFanin, * pFanins; 
@@ -510,6 +546,19 @@ static inline void Acb_ObjRemoveFaninFanout( Acb_Ntk_t * p, int iObj )
         assert( RetValue );
     }
 }
+static inline void Acb_ObjPatchFanin( Acb_Ntk_t * p, int iObj, int iFanin, int iFaninNew )
+{
+    int i, RetValue, * pFanins = Acb_ObjFanins( p, iObj );
+    assert( iFanin != iFaninNew );
+    for ( i = 0; i < pFanins[0]; i++ )
+        if ( pFanins[ 1 + i ] == iFanin )
+            pFanins[ 1 + i ] = iFaninNew;
+    if ( !Acb_NtkHasObjFanout(p) )
+        return;
+    RetValue = Vec_IntRemove( Vec_WecEntry(&p->vFanouts, iFanin), iObj );
+    assert( RetValue );
+    Vec_IntPush( Vec_WecEntry(&p->vFanouts, iFaninNew), iObj );
+}
 static inline void Acb_NtkCreateFanout( Acb_Ntk_t * p )
 {
     int iObj; 
diff --git a/src/base/acb/acbMfs.c b/src/base/acb/acbMfs.c
index d8c6fb16..9fce00f8 100644
--- a/src/base/acb/acbMfs.c
+++ b/src/base/acb/acbMfs.c
@@ -1576,7 +1576,7 @@ cleanup:
 void Acb_NtkOpt( Acb_Ntk_t * pNtk, Acb_Par_t * pPars )
 {
     Acb_Mfs_t * pMan = Acb_MfsStart( pNtk, pPars );
-    //if ( pPars->fVerbose )
+    if ( pPars->fVerbose )
         printf( "%s-optimization parameters: TfiLev(I) = %d  TfoLev(O) = %d  WinMax(W) = %d  LutSize = %d\n", 
             pMan->pPars->fArea ? "Area" : "Delay", pMan->pPars->nTfiLevMax, pMan->pPars->nTfoLevMax, pMan->pPars->nWinNodeMax, pMan->pPars->nLutSize );
     Acb_NtkCreateFanout( pNtk );  // fanout data structure
@@ -1592,8 +1592,8 @@ void Acb_NtkOpt( Acb_Ntk_t * pNtk, Acb_Par_t * pPars )
                 if ( iObj < nNodes && !Vec_BitEntry(vVisited, iObj) && Acb_NtkObjMffcEstimate(pNtk, iObj) >= n )
                 {
                     pMan->nNodes++;
-                    if ( iObj != 103 )
-                        continue;
+                    //if ( iObj != 103 )
+                    //    continue;
                     //Acb_NtkOptNode( pMan, iObj );
                     while ( (RetValue = Acb_NtkOptNode(pMan, iObj)) && Acb_ObjFaninNum(pNtk, iObj) );                    
                     Vec_BitWriteEntry( vVisited, iObj, 1 );
@@ -1609,13 +1609,13 @@ void Acb_NtkOpt( Acb_Ntk_t * pNtk, Acb_Par_t * pPars )
             int iObj = Vec_QuePop(pNtk->vQue);
             if ( !Acb_ObjType(pNtk, iObj) )
                 continue;
-            if ( iObj != 103 )
-                continue;
+            //if ( iObj != 103 )
+            //    continue;
             //printf( "Trying node %4d (%4d) ", iObj, Value );
             Acb_NtkOptNode( pMan, iObj ); 
         }
     }
-    //if ( pPars->fVerbose )
+    if ( pPars->fVerbose )
     {
         pMan->timeTotal = Abc_Clock() - pMan->timeTotal;
         printf( "Node = %d  Win = %d (Ave = %d)  DivAve = %d   Change = %d  C = %d  N1 = %d  N2 = %d  N3 = %d   Over = %d  Str = %d  2Node = %d.\n", 
diff --git a/src/base/acb/acbPush.c b/src/base/acb/acbPush.c
index 08edc4d1..7ede912f 100644
--- a/src/base/acb/acbPush.c
+++ b/src/base/acb/acbPush.c
@@ -33,7 +33,105 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
-  Synopsis    [Check if the node can have its logic pushed.]
+  Synopsis    [Pushing logic to the fanout.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acb_ObjPushToFanout( Acb_Ntk_t * p, int iObj, int iFaninIndex, int iFanout )
+{
+    word c0, uTruthObjNew, uTruthObj = Acb_ObjTruth( p, iObj ), Gate;
+    word c1, uTruthFanNew, uTruthFan = Acb_ObjTruth( p, iFanout );
+    int DecType = Abc_TtCheckOutAnd( uTruthObj, iFaninIndex, &uTruthObjNew );
+    int iFanin = Acb_ObjFanin( p, iObj, iFaninIndex );
+    int iFanoutObjIndex = Acb_ObjWhatFanin( p, iFanout, iObj );
+    int iFanoutFaninIndex = Acb_ObjWhatFanin( p, iFanout, iFanin );
+    if ( iFanoutFaninIndex == -1 )
+        iFanoutFaninIndex = Acb_ObjFaninNum(p, iFanout); 
+    assert( !Acb_ObjIsCio(p, iObj) );
+    assert( !Acb_ObjIsCio(p, iFanout) );
+    assert( iFanoutFaninIndex >= 0 );
+    assert( iFaninIndex < Acb_ObjFaninNum(p, iObj) );
+    assert( Acb_ObjFanoutNum(p, iObj) == 1 );
+    // compute new function of the fanout
+    c0 = Abc_Tt6Cofactor0( uTruthFan, iFanoutObjIndex );
+    c1 = Abc_Tt6Cofactor1( uTruthFan, iFanoutObjIndex );
+    if ( DecType == 0 ) //  F = i * G
+        Gate =  s_Truths6[iFanoutFaninIndex] & s_Truths6[iFanoutObjIndex];
+    else if ( DecType == 1 ) //  F = ~i * G
+        Gate = ~s_Truths6[iFanoutFaninIndex] & s_Truths6[iFanoutObjIndex];
+    else if ( DecType == 2 ) //  F = ~i + G
+        Gate = ~s_Truths6[iFanoutFaninIndex] | s_Truths6[iFanoutObjIndex];
+    else if ( DecType == 3 ) //  F = i + G
+        Gate =  s_Truths6[iFanoutFaninIndex] | s_Truths6[iFanoutObjIndex];
+    else if ( DecType == 4 ) //  F = i # G
+        Gate =  s_Truths6[iFanoutFaninIndex] ^ s_Truths6[iFanoutObjIndex];
+    else assert( 0 );
+    uTruthFanNew = (~Gate & c0) | (Gate & c1);
+    // update functions
+    Vec_WrdWriteEntry( &p->vObjTruth, iObj, Abc_Tt6RemoveVar(uTruthObjNew, iFaninIndex) );
+    Vec_WrdWriteEntry( &p->vObjTruth, iFanout, uTruthFanNew );
+    // update fanins
+    Acb_ObjRemoveFaninFanoutOne( p, iObj, iFanin );
+    if ( iFanoutFaninIndex == Acb_ObjFaninNum(p, iFanout) ) // adding new
+        Acb_ObjAddFaninFanoutOne( p, iFanout, iFanin );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Pushing logic to the fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acb_ObjPushToFanin( Acb_Ntk_t * p, int iObj, int iFaninIndex2, int iFanin )
+{
+    word uTruthObjNew, uTruthObj = Acb_ObjTruth( p, iObj );
+    word uTruthFanNew, uTruthFan = Acb_ObjTruth( p, iFanin );
+    int iFaninIndex = Acb_ObjWhatFanin( p, iObj, iFanin );
+    int DecType = Abc_TtCheckDsdAnd( uTruthObj, iFaninIndex, iFaninIndex2, &uTruthObjNew );
+    int iFanin2 = Acb_ObjFanin( p, iObj, iFaninIndex2 );
+    int iFaninFaninIndex = Acb_ObjWhatFanin( p, iFanin, iFanin2 );
+    if ( iFaninFaninIndex == -1 )
+        iFaninFaninIndex = Acb_ObjFaninNum(p, iFanin); 
+    assert( !Acb_ObjIsCio(p, iObj) );
+    assert( !Acb_ObjIsCio(p, iFanin) );
+    assert( iFaninIndex  < Acb_ObjFaninNum(p, iObj) );
+    assert( iFaninIndex2 < Acb_ObjFaninNum(p, iObj) );
+    assert( iFaninIndex != iFaninIndex2 );
+    assert( Acb_ObjFanoutNum(p, iFanin) == 1 );
+    // compute new function of the fanout
+    if ( DecType == 0 )      //  i *  j
+        uTruthFanNew =  uTruthFan &  s_Truths6[iFaninFaninIndex];
+    else if ( DecType == 1 ) //  i * !j
+        uTruthFanNew = ~uTruthFan &  s_Truths6[iFaninFaninIndex];
+    else if ( DecType == 2 ) // !i *  j
+        uTruthFanNew =  uTruthFan & ~s_Truths6[iFaninFaninIndex];
+    else if ( DecType == 3 ) // !i * !j
+        uTruthFanNew = ~uTruthFan & ~s_Truths6[iFaninFaninIndex];
+    else if ( DecType == 4 ) //  i #  j
+        uTruthFanNew =  uTruthFan ^  s_Truths6[iFaninFaninIndex];
+    else assert( 0 );
+    // update functions
+    Vec_WrdWriteEntry( &p->vObjTruth, iObj, Abc_Tt6RemoveVar(uTruthObjNew, iFaninIndex2) );
+    Vec_WrdWriteEntry( &p->vObjTruth, iFanin, uTruthFanNew );
+    // update fanins
+    Acb_ObjRemoveFaninFanoutOne( p, iObj, iFanin2 );
+    if ( iFaninFaninIndex == Acb_ObjFaninNum(p, iFanin) ) // adding new
+        Acb_ObjAddFaninFanoutOne( p, iFanin, iFanin2 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removing constants, buffers, duplicated fanins.]
 
   Description []
                
@@ -42,50 +140,155 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-int Acb_ObjCheckFaninDsd( Acb_Ntk_t * p, int iObj, int iFanIndex )
+static inline int Acb_ObjFindNodeFanout( Acb_Ntk_t * p, int iObj )
+{
+    int i, iFanout;
+    Acb_ObjForEachFanout( p, iObj, iFanout, i )
+        if ( !Acb_ObjIsCio(p, iFanout) )
+            return iFanout;
+    return -1;
+}
+int Acb_ObjSuppMin_int( Acb_Ntk_t * p, int iObj )
 {
     int k, iFanin, * pFanins;
+    word uTruth = Acb_ObjTruth( p, iObj );
     Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
-        if ( Abc_TtCheckDsdAnd(Acb_ObjTruth(p, iObj), iFanIndex, k, NULL) >= 0 )
-            return 1;
+    {
+        if ( Abc_Tt6HasVar(uTruth, k) )
+            continue;
+        Acb_ObjDeleteFaninIndex( p, iObj, k );
+        Vec_IntRemove( Vec_WecEntry(&p->vFanouts, iFanin), iObj );
+        Vec_WrdWriteEntry( &p->vObjTruth, iObj, Abc_Tt6RemoveVar(uTruth, k) );
+        return 1;
+    }
     return 0;
 }
-int Acb_ObjCountFaninAbsorb( Acb_Ntk_t * p, int iObj, int iFanin, int iFanIndex, int nLutSize )
+void Acb_ObjSuppMin( Acb_Ntk_t * p, int iObj )
 {
-    if ( Acb_ObjSetTravIdCur(p, iFanin) )
-        return 0;
-    if ( Acb_ObjIsCi(p, iFanin) )
-        return 0;
-    if ( Acb_ObjFanoutNum(p, iFanin) > 1 )
-        return 0;
-    if ( !Acb_ObjCheckFaninDsd(p, iObj, iFanIndex) ) 
-        return 0;
-    if ( Acb_ObjFaninNum(p, iFanin) == nLutSize )
-        return 0;
-    return 1;
+    while ( Acb_ObjSuppMin_int(p, iObj) );
 }
-int Acb_NtkObjPushEstimate( Acb_Ntk_t * p, int iObj, int nLutSize )
+void Acb_ObjRemoveDup( Acb_Ntk_t * p, int iObj, int i, int j )
 {
-    int k, iFanin, * pFanins;
-    int Count = Acb_ObjFaninNum(p, iObj);
-    Acb_NtkIncTravId( p );
-    Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
+    word c00, c11, uTruthNew, uTruth = Acb_ObjTruth( p, iObj );
+    assert( !Acb_ObjIsCio(p, iObj) );
+    assert( Acb_ObjFanin(p, iObj, i) == Acb_ObjFanin(p, iObj, j) );
+    c00 = Abc_Tt6Cofactor0( Abc_Tt6Cofactor0(uTruth, i), j );
+    c11 = Abc_Tt6Cofactor1( Abc_Tt6Cofactor1(uTruth, i), j );
+    uTruthNew = (~s_Truths6[i] & c00) | (s_Truths6[i] & c11);
+    Vec_WrdWriteEntry( &p->vObjTruth, iObj, Abc_Tt6RemoveVar(uTruthNew, j) );
+    Acb_ObjDeleteFaninIndex( p, iObj, j );
+    Vec_IntRemove( Vec_WecEntry(&p->vFanouts, iObj), Acb_ObjFanin(p, iObj, j) );
+    Acb_ObjSuppMin( p, iObj );
+}
+int Acb_ObjRemoveDupFanins_int( Acb_Ntk_t * p, int iObj )
+{
+    int i, k, * pFanins = Acb_ObjFanins( p, iObj );
+    for ( i = 0; i < pFanins[0]; i++ )
+    for ( k = i+1; k < pFanins[0]; k++ )
     {
-        Count -= Acb_ObjCountFaninAbsorb( p, iObj, iFanin, k, nLutSize );
-        if ( Count <= 0 )
-            return 1;
+        if ( pFanins[1+i] != pFanins[1+k] )
+            continue;
+        Acb_ObjRemoveDup( p, iObj, i, k );
+        return 1;
     }
-    if ( Acb_ObjFanoutNum(p, iObj) > 1 )
-        return 0;
+    return 0;
+}
+void Acb_ObjRemoveDupFanins( Acb_Ntk_t * p, int iObj )
+{
+    assert( !Acb_ObjIsCio(p, iObj) );
+    while ( Acb_ObjRemoveDupFanins_int(p, iObj) );
+}
+void Acb_ObjRemoveConst( Acb_Ntk_t * p, int iObj )
+{
+    int iFanout;
+    word uTruth = Acb_ObjTruth( p, iObj );
+    assert( !Acb_ObjIsCio(p, iObj) );
+    assert( Acb_ObjFaninNum(p, iObj) == 0 );
+    assert( uTruth == 0 || ~uTruth == 0 );
+    while ( (iFanout = Acb_ObjFindNodeFanout(p, iObj)) >= 0 )
+    {
+        int iObjIndex = Acb_ObjWhatFanin( p, iFanout, iObj );
+        word uTruthF = Acb_ObjTruth( p, iFanout );
+        Acb_ObjRemoveFaninFanoutOne( p, iFanout, iObj );
+        uTruthF = (uTruth & 1) ? Abc_Tt6Cofactor1(uTruthF, iObjIndex) : Abc_Tt6Cofactor0(uTruthF, iObjIndex);
+        Vec_WrdWriteEntry( &p->vObjTruth, iFanout, Abc_Tt6RemoveVar(uTruthF, iObjIndex) );
+        Acb_ObjSuppMin( p, iFanout );
+    }
+    if ( Acb_ObjFanoutNum(p, iObj) == 0 )
+        Acb_ObjCleanType( p, iObj );
+}
+void Acb_ObjRemoveBufInv( Acb_Ntk_t * p, int iObj )
+{
+    int iFanout;
+    word uTruth = Acb_ObjTruth( p, iObj );
+    assert( !Acb_ObjIsCio(p, iObj) );
+    assert( Acb_ObjFaninNum(p, iObj) == 1 );
+    assert( uTruth == s_Truths6[0] || ~uTruth == s_Truths6[0] );
+    while ( (iFanout = Acb_ObjFindNodeFanout(p, iObj)) >= 0 )
+    {
+        int iFanin = Acb_ObjFanin( p, iObj, 0 );
+        int iObjIndex = Acb_ObjWhatFanin( p, iFanout, iObj );
+        Acb_ObjPatchFanin( p, iFanout, iObj, iFanin );
+        if ( uTruth & 1 ) // inv
+        {
+            word uTruthF = Acb_ObjTruth( p, iFanout );
+            Vec_WrdWriteEntry( &p->vObjTruth, iFanout, Abc_Tt6Flip(uTruthF, iObjIndex) );
+        }
+        Acb_ObjRemoveDupFanins( p, iFanout );
+    }
+    while ( (uTruth & 1) == 0 && Acb_ObjFanoutNum(p, iObj) > 0 )
+    {
+        int iFanin = Acb_ObjFanin( p, iObj, 0 );
+        int iFanout = Acb_ObjFanout( p, iObj, 0 );
+        assert( Acb_ObjIsCo(p, iFanout) );
+        Acb_ObjPatchFanin( p, iFanout, iObj, iFanin );
+    }
+    if ( Acb_ObjFanoutNum(p, iObj) == 0 )
+    {
+        Acb_ObjRemoveFaninFanout( p, iObj );
+        Acb_ObjRemoveFanins( p, iObj );
+        Acb_ObjCleanType( p, iObj );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Check if the node can have its logic pushed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Acb_ObjFindPushableIndex( Acb_Ntk_t * p, int iObj, int iFanIndex )
+{
+    int k, iFanin, * pFanins;
     Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
-        if ( Abc_TtCheckOutAnd(Acb_ObjTruth(p, iObj), k, NULL) )
-            break;
-    if ( k == Acb_ObjFaninNum(p, iFanin) )
-        return 0;
-    iFanin = Vec_IntEntry( Acb_ObjFanout(p, iObj), 0 );
-    if ( Acb_ObjFaninNum(p, iFanin) == nLutSize )
+        if ( k != iFanIndex && Abc_TtCheckDsdAnd(Acb_ObjTruth(p, iObj), k, iFanIndex, NULL) >= 0 )
+            return k;
+    return -1;
+}
+int Acb_ObjPushToFanins( Acb_Ntk_t * p, int iObj, int nLutSize )
+{
+    int k, k2, iFanin, * pFanins;
+    if ( Acb_ObjFaninNum(p, iObj) < 2 )
         return 0;
-    return 1;
+    Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
+    {
+        if ( Acb_ObjIsCi(p, iFanin) )
+            continue;
+        if ( Acb_ObjFanoutNum(p, iFanin) > 1 )
+            continue;
+        if ( Acb_ObjFaninNum(p, iFanin) == nLutSize )
+            continue;
+        if ( (k2 = Acb_ObjFindPushableIndex(p, iObj, k)) == -1 )
+            continue;
+        Acb_ObjPushToFanin( p, iObj, k2, iFanin );
+        return 1;
+    }
+    return 0;
 }
 
 /**Function*************************************************************
@@ -101,18 +304,43 @@ int Acb_NtkObjPushEstimate( Acb_Ntk_t * p, int iObj, int nLutSize )
 ***********************************************************************/
 void Acb_NtkPushLogic( Acb_Ntk_t * p, int nLutSize, int fVerbose )
 {
-    //Vec_Bit_t * vVisited = Vec_BitStart( Acb_NtkObjNumMax(p) );
-    int n = 0, iObj, nNodes = 0;
+    int n = 0, iObj, nNodes = Acb_NtkNodeNum(p), nPushes = 0;
     Acb_NtkCreateFanout( p );  // fanout data structure
+    Acb_NtkForEachNodeSupp( p, iObj, 0 )
+        Acb_ObjRemoveConst( p, iObj );
+    Acb_NtkForEachNodeSupp( p, iObj, 1 )
+        Acb_ObjRemoveBufInv( p, iObj );
     for ( n = 2; n <= nLutSize; n++ )
-        Acb_NtkForEachNode( p, iObj )
+        Acb_NtkForEachNodeSupp( p, iObj, n )
         {
-            if ( !Acb_NtkObjPushEstimate(p, iObj, nLutSize) )
-                continue;
-            nNodes++;
+            while ( Acb_ObjPushToFanins(p, iObj, nLutSize) )
+                nPushes++;
+            if ( Acb_ObjFaninNum(p, iObj) == 1 )
+                Acb_ObjRemoveBufInv( p, iObj );
         }
-    printf( "Performed optimization at %d nodes.\n", nNodes );
-    //Vec_BitFree( vVisited );
+    printf( "Saved %d nodes after %d pushes.\n", nNodes - Acb_NtkNodeNum(p), nPushes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Pushing logic to the fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acb_NtkPushLogic2( Acb_Ntk_t * p, int nLutSize, int fVerbose )
+{
+    int iObj;
+    Acb_NtkCreateFanout( p );  // fanout data structure
+    Acb_NtkForEachObj( p, iObj )
+        if ( !Acb_ObjIsCio(p, iObj) )
+            break;
+    Acb_ObjPushToFanout( p, iObj, Acb_ObjFaninNum(p, iObj)-1, Acb_ObjFanout(p, iObj, 0) );
+//    Acb_ObjPushToFanin( p, Acb_ObjFanout(p, iObj, 0), Acb_ObjFaninNum(p, iObj)-1, iObj );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index f02a9835..4736a291 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -1378,6 +1378,13 @@ static inline void Abc_TtMoveVar( word * pF, int nVars, int * V2P, int * P2V, in
     P2V[jVar] ^= P2V[iVar];
     P2V[iVar] ^= P2V[jVar];
 }
+static inline word Abc_Tt6RemoveVar( word t, int iVar )
+{
+    assert( !Abc_Tt6HasVar(t, iVar) );
+    while ( iVar < 5 )
+        t = Abc_Tt6SwapAdjacent( t, iVar++ );
+    return t;
+}
 
 /**Function*************************************************************
 
@@ -2222,7 +2229,7 @@ static inline int Abc_TtCheckOutAnd( word t, int i, word * pOut )
 {
     word c0 = Abc_Tt6Cofactor0( t, i );
     word c1 = Abc_Tt6Cofactor1( t, i );
-    assert( c0 == c1 );
+    assert( c0 != c1 );
     if ( c0 == 0 ) //  F = i * G
     {
         if ( pOut ) *pOut = c1;