Logic sharing for multi-input gates.

6 files changed, 606 insertions, 462 deletions

diff --git a/abclib.dsp b/abclib.dsp
index b6fd2713..59a73aff 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -423,10 +423,6 @@ SOURCE=.\src\base\abci\abcSense.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\base\abci\abcShare.c
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\base\abci\abcSpeedup.c
 # End Source File
 # Begin Source File
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 46974edb..bc6f1bc3 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -572,6 +572,7 @@ extern ABC_DLL void               Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj )
 /*=== abcDar.c ============================================================*/
 extern ABC_DLL int                Abc_NtkPhaseFrameNum( Abc_Ntk_t * pNtk );
 extern ABC_DLL int                Abc_NtkDarPrintCone( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkBalanceExor( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose );
 /*=== abcDelay.c ==========================================================*/
 extern ABC_DLL float              Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib );
 /*=== abcDfs.c ==========================================================*/
@@ -852,6 +853,7 @@ extern ABC_DLL word               Abc_SopToTruth( char * pSop, int nInputs );
 extern ABC_DLL void               Abc_SopToTruth7( char * pSop, int nInputs, word r[2] );
 extern ABC_DLL void               Abc_SopToTruthBig( char * pSop, int nInputs, word ** pVars, word * pCube, word * pRes );
 /*=== abcStrash.c ==========================================================*/
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkRestrash( Abc_Ntk_t * pNtk, int fCleanup );
 extern ABC_DLL Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk, int fAllNodes, int fCleanup, int fRecord );
 extern ABC_DLL Abc_Obj_t *        Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int fRecord );
 extern ABC_DLL int                Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 55208cad..f8fe22a4 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -115,6 +115,7 @@ static int Abc_CommandRestructure            ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandResubstitute           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRr                     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCascade                ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExtract                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandLogic                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandComb                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -560,6 +561,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "resub",         Abc_CommandResubstitute,     1 );
 //    Cmd_CommandAdd( pAbc, "Synthesis",    "rr",            Abc_CommandRr,               1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "cascade",       Abc_CommandCascade,          1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "extract",       Abc_CommandExtract,          1 );
 
     Cmd_CommandAdd( pAbc, "Various",      "logic",         Abc_CommandLogic,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "comb",          Abc_CommandComb,             1 );
@@ -2805,7 +2807,6 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fUpdateLevel;
     int fExor;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkBalanceExor( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose );
     pNtk = Abc_FrameReadNtk(pAbc);
 
     // set defaults
@@ -5381,6 +5382,88 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Abc_Ntk_t * Abc_NtkShareXor( Abc_Ntk_t * pNtk, int nMultiSize, int fAnd, int fVerbose );
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c, nMultiSize, fAnd, fVerbose;
+    pNtk = Abc_FrameReadNtk(pAbc);
+
+    // set defaults
+    nMultiSize = 3;
+    fAnd       = 0;
+    fVerbose   = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Kavh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nMultiSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nMultiSize < 0 ) 
+                goto usage;
+            break;
+        case 'a':
+            fAnd ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( -1, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        Abc_Print( -1, "Can only collapse a logic network or an AIG.\n" );
+        return 1;
+    }
+    // get the new network
+    pNtkRes = Abc_NtkShareXor( pNtk, nMultiSize, fAnd, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        Abc_Print( -1, "Cascade synthesis has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: extract [-K <num>] [-vh]\n" );
+    Abc_Print( -2, "\t           extracts logic sharing from multi-input XOR gates\n" );
+    Abc_Print( -2, "\t-K <num> : the min gate size to consider for extraction [default = %d]\n", nMultiSize );
+//    Abc_Print( -2, "\t-a       : toggle multi-input XOR vs multi-input AND [default = %s]\n", fAnd? "AND": "XOR" );
+    Abc_Print( -2, "\t-v       : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : print the command usage\n");
+    Abc_Print( -2, "\t         \n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
@@ -9020,8 +9103,14 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
         Aig_ManStop( pAig );
 */
-        extern void Abc_NtkShareXor( Abc_Ntk_t * pNtk );
-        Abc_NtkShareXor( pNtk );
+/*
+        extern Abc_Ntk_t * Abc_NtkShareXor( Abc_Ntk_t * pNtk );
+        Abc_Ntk_t * pNtkRes = Abc_NtkShareXor( pNtk );
+        if ( pNtkRes == NULL )
+            printf( "Transformation has failed.\n" );
+        else
+            Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+*/
     }
 
 //    Abc2_NtkTestGia( "", 1 );
diff --git a/src/base/abci/abcExtract.c b/src/base/abci/abcExtract.c
index e6b4193b..cc2532de 100644
--- a/src/base/abci/abcExtract.c
+++ b/src/base/abci/abcExtract.c
@@ -1,12 +1,12 @@
 /**CFile****************************************************************
 
-  FileName    [abcMvCost.c]
+  FileName    [abcShare.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
   PackageName [Network and node package.]
 
-  Synopsis    [Calculating the cost of one MV block.]
+  Synopsis    [Shared logic extraction.]
 
   Author      [Alan Mishchenko]
   
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: abcMvCost.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: abcShare.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -22,17 +22,143 @@
 
 ABC_NAMESPACE_IMPL_START
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define SHARE_NUM 2
+
+typedef struct Abc_ShaMan_t_ Abc_ShaMan_t;
+struct Abc_ShaMan_t_ 
+{
+    int             nMultiSize;
+    int             fVerbose;
+    Abc_Ntk_t *     pNtk;
+    Vec_Ptr_t *     vBuckets;
+    Vec_Int_t *     vObj2Lit;
+    int             nStartCols;
+    int             nCountXors;
+    int             nFoundXors;
+};
+
+static inline word  Abc_NtkSharePack( int Lev, int Id )  { return (((word)Lev) << 32) | Id; }
+static inline int   Abc_NtkShareUnpackLev( word Num )    { return (Num >> 32);              }
+static inline int   Abc_NtkShareUnpackId( word Num )     { return Num & 0xFFFF;             }
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    [Working with the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_ShaMan_t * Abc_ShaManStart( Abc_Ntk_t * pNtk )
+{
+    Abc_ShaMan_t * p;
+    p = ABC_CALLOC( Abc_ShaMan_t, 1 );
+    p->pNtk      = pNtk;
+    p->vObj2Lit  = Vec_IntAlloc( 1000 );
+    return p;
+}
+void Abc_ShaManStop( Abc_ShaMan_t * p )
+{
+    Vec_Ptr_t * vBucket;
+    int i;
+    Vec_PtrForEachEntry( Vec_Ptr_t *, p->vBuckets, vBucket, i )
+        Vec_VecFree( (Vec_Vec_t *)vBucket );
+    Vec_PtrFreeP( &p->vBuckets );
+    Vec_IntFreeP( &p->vObj2Lit );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects one multi-input XOR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wrd_t * Abc_NtkShareSuperXor( Abc_Obj_t * pObjInit, int * pfCompl, int * pCounter )
+{
+    int fCompl = Abc_ObjIsComplement(pObjInit);
+    Abc_Obj_t * pObj = Abc_ObjRegular(pObjInit);
+    Abc_Ntk_t * pNtk = Abc_ObjNtk(pObj);
+    Abc_Obj_t * pObjC, * pObj0, * pObj1, * pRoot;
+    Vec_Wrd_t * vSuper;
+    word Num, NumNext;
+    int i, k;
+    assert( Abc_NodeIsExorType(pObj) );
+    // start iteration
+    vSuper = Vec_WrdAlloc( 10 );
+    Vec_WrdPush( vSuper, Abc_NtkSharePack(Abc_ObjLevel(pObj), Abc_ObjId(pObj)) );
+    while ( Vec_WrdSize(vSuper) > 0 )
+    {
+        // 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 = Abc_NtkObj( pNtk, Abc_NtkShareUnpackId(Num) );
+            if ( Abc_NodeIsExorType(pRoot) )
+            {
+                Vec_WrdRemove( vSuper, Num );
+                break;
+            }
+        }
+        if ( i == -1 )
+            break;
+        // extract
+        pObjC = Abc_NodeRecognizeMux( pRoot, &pObj1, &pObj0 );
+        assert( pObj1 == Abc_ObjNot(pObj0) );
+        fCompl ^= Abc_ObjIsComplement(pObjC);  pObjC = Abc_ObjRegular(pObjC);
+        fCompl ^= Abc_ObjIsComplement(pObj0);  pObj0 = Abc_ObjRegular(pObj0);
+        Vec_WrdPushOrder( vSuper, Abc_NtkSharePack(Abc_ObjLevel(pObjC), Abc_ObjId(pObjC)) );
+        Vec_WrdPushOrder( vSuper, Abc_NtkSharePack(Abc_ObjLevel(pObj0), Abc_ObjId(pObj0)) );
+        (*pCounter)++;
+        // 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, Abc_NtkShareUnpackId(Num) );
+    return vSuper;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -42,11 +168,385 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_MvCostTest( Abc_Ntk_t * pNtk )
+void Abc_NtkSharePrint( Abc_ShaMan_t * p )
 {
+    Vec_Ptr_t * vBucket;
+    Vec_Int_t * vInput;
+    int i, k, j, ObjId;
+    char * pBuffer = ABC_ALLOC( char, Vec_IntSize(p->vObj2Lit) + 1 );
+    int * pCounters = ABC_CALLOC( int, Vec_IntSize(p->vObj2Lit) + 1 );
+    int nTotal = 0;
+    Vec_PtrForEachEntry( Vec_Ptr_t *, p->vBuckets, vBucket, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vBucket, vInput, j )
+    {
+        for ( k = 0; k < Vec_IntSize(p->vObj2Lit); k++ )
+            pBuffer[k] = '0';
+        pBuffer[k] = 0;
+
+        Vec_IntForEachEntryStart( vInput, ObjId, k, SHARE_NUM )
+        {
+            assert( ObjId < Vec_IntSize(p->vObj2Lit) );
+            pBuffer[ObjId] = '1';
+            pCounters[ObjId]++;
+        }
+        printf( "%4d%3d: %s\n", Vec_IntEntry(vInput, 0), Vec_IntEntry(vInput, 1), pBuffer );
+    }
+
+    for ( i = 0; i < Vec_IntSize(p->vObj2Lit); i++ )
+        if ( pCounters[i] > 0 )
+            printf( "%d=%d ", i, pCounters[i] ); 
+    printf( "\n" );
+
+    nTotal = 0;
+    for ( i = 0; i < p->nStartCols; i++ )
+        nTotal += pCounters[i] - 1;
+    printf( "Total = %d.  ", nTotal );
+    printf( "Xors = %d.\n", Vec_IntSize(p->vObj2Lit) - p->nStartCols + nTotal );
+
+    ABC_FREE( pCounters );
+    ABC_FREE( pBuffer );
 
+    printf( "Bucket contents: " );
+    Vec_PtrForEachEntry( Vec_Ptr_t *, p->vBuckets, vBucket, i )
+        printf( "%d ", Vec_PtrSize(vBucket) );
+    printf( "\n" );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkShareFindBestMatch( Vec_Ptr_t * vBuckets, Vec_Int_t ** pvInput, Vec_Int_t ** pvInput2 )
+{
+    int nPoolSize = 40;
+    Vec_Ptr_t * vPool = Vec_PtrAlloc( nPoolSize );
+    Vec_Ptr_t * vBucket;
+    Vec_Int_t * vInput, * vInput2, * vInputBest = NULL, * vInputBest2 = NULL;
+    int i, k, Cost, CostBest = 0, Delay, DelayBest = 0;
+
+    Vec_PtrForEachEntryReverse( Vec_Ptr_t *, vBuckets, vBucket, i )
+        Vec_PtrForEachEntry( Vec_Int_t *, vBucket, vInput, k )
+        {
+            Vec_PtrPush( vPool, vInput );
+            if ( Vec_PtrSize(vPool) == nPoolSize )
+                goto outside;
+        }
+outside:
+
+    Vec_PtrForEachEntryReverse( Vec_Int_t *, vPool, vInput, i )
+    Vec_PtrForEachEntryReverse( Vec_Int_t *, vPool, vInput2, k )
+    {
+        if ( i == k )
+            continue;
+
+        vInput->pArray += SHARE_NUM;
+        vInput2->pArray += SHARE_NUM;
+        vInput->nSize -= SHARE_NUM;
+        vInput2->nSize -= SHARE_NUM;
+
+        Cost = Vec_IntTwoCountCommon(vInput, vInput2);
+
+        vInput->pArray -= SHARE_NUM;
+        vInput2->pArray -= SHARE_NUM;
+        vInput->nSize += SHARE_NUM;
+        vInput2->nSize += SHARE_NUM;
+
+        if ( Cost < 2 )
+            continue;
+
+        Delay = Abc_MaxInt( Vec_IntEntry(vInput, 1), Vec_IntEntry(vInput2, 1) );
+
+        if ( CostBest < Cost || (CostBest == Cost && (DelayBest > Delay)) )
+        {
+            CostBest = Cost;
+            DelayBest = Delay;
+            vInputBest = vInput;
+            vInputBest2 = vInput2;
+        }
+    }
+    Vec_PtrFree( vPool );
+
+    *pvInput  = vInputBest;
+    *pvInput2 = vInputBest2;
+
+    if ( vInputBest == NULL )
+        return;
+
+    Vec_PtrRemove( (Vec_Ptr_t *)Vec_PtrEntry(vBuckets, Vec_IntSize(vInputBest)-SHARE_NUM),  (Vec_Int_t *)vInputBest ); 
+    Vec_PtrRemove( (Vec_Ptr_t *)Vec_PtrEntry(vBuckets, Vec_IntSize(vInputBest2)-SHARE_NUM), (Vec_Int_t *)vInputBest2 ); 
+}
+void Abc_NtkShareOptimize( Abc_ShaMan_t * p )
+{
+    Abc_Obj_t * pObj, * pObj0, * pObj1;
+    Vec_Int_t * vInput, * vInput2;
+    Vec_Int_t * vNew, * vOld1, * vOld2;
+    int i;
+    for ( i = 0; ; i++ )
+    {
+        Abc_NtkShareFindBestMatch( p->vBuckets, &vInput, &vInput2 );
+        if ( vInput == NULL )
+            break;
+
+        // create new node
+        pObj0 = Abc_ObjFromLit( p->pNtk, Vec_IntEntry(vInput,  0) );
+        pObj1 = Abc_ObjFromLit( p->pNtk, Vec_IntEntry(vInput2, 0) );
+        pObj  = Abc_AigXor( (Abc_Aig_t *)p->pNtk->pManFunc, pObj0, pObj1 );
+        p->nCountXors++;
+
+        // save new node
+        vOld1 = Vec_IntAlloc( 16 );  Vec_IntPush( vOld1, Vec_IntEntry(vInput,  0) );  Vec_IntPush( vOld1, Vec_IntEntry(vInput,  1) );
+        vOld2 = Vec_IntAlloc( 16 );  Vec_IntPush( vOld2, Vec_IntEntry(vInput2, 0) );  Vec_IntPush( vOld2, Vec_IntEntry(vInput2, 1) );
+        vNew  = Vec_IntAlloc( 16 );  Vec_IntPush( vNew,  Abc_ObjToLit(pObj) );        Vec_IntPush( vNew, Abc_ObjLevel(Abc_ObjRegular(pObj)) );
+
+        // compute new arrays
+        vInput->pArray += SHARE_NUM;
+        vInput2->pArray += SHARE_NUM;
+        vInput->nSize -= SHARE_NUM;
+        vInput2->nSize -= SHARE_NUM;
+
+        Vec_IntTwoSplit( vInput, vInput2, vNew, vOld1, vOld2 );
+
+        vInput->pArray -= SHARE_NUM;
+        vInput2->pArray -= SHARE_NUM;
+        vInput->nSize += SHARE_NUM;
+        vInput2->nSize += SHARE_NUM;
+
+        // add to the old ones
+        Vec_IntPush( vOld1, Vec_IntSize(p->vObj2Lit) );
+        Vec_IntPush( vOld2, Vec_IntSize(p->vObj2Lit) );
+        Vec_IntPush( p->vObj2Lit, Abc_ObjToLit(pObj) );
+
+        Vec_PtrPush( (Vec_Ptr_t *)Vec_PtrEntry(p->vBuckets, Vec_IntSize(vOld1)-SHARE_NUM), vOld1 );
+        Vec_PtrPush( (Vec_Ptr_t *)Vec_PtrEntry(p->vBuckets, Vec_IntSize(vOld2)-SHARE_NUM), vOld2 );
+        Vec_PtrPush( (Vec_Ptr_t *)Vec_PtrEntry(p->vBuckets, Vec_IntSize(vNew)-SHARE_NUM), vNew );
+
+        Vec_IntFree( vInput );
+        Vec_IntFree( vInput2 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkUpdateNetwork( Abc_ShaMan_t * p )
+{
+    Abc_Ntk_t * pNtk;
+    Vec_Int_t * vInput, * vMap2Repl;
+    Vec_Ptr_t * vOrig, * vRepl, * vBucket;
+    Abc_Obj_t * pObj, * pNew;
+    int i, j, k, ObjId, iLit;
+
+    vOrig = Vec_PtrAlloc( p->nStartCols );
+    vRepl = Vec_PtrAlloc( p->nStartCols );
+    for ( i = 0; i < p->nStartCols; i++ )
+    {
+        iLit = Vec_IntEntry( p->vObj2Lit, i );
+
+        pObj = Abc_NtkObj( p->pNtk, Abc_Lit2Var(iLit) );
+        pNew = Abc_ObjNotCond( Abc_AigConst1(p->pNtk), !Abc_LitIsCompl(iLit) );
+
+        Vec_PtrPush( vOrig, pObj );
+        Vec_PtrPush( vRepl, pNew );
+
+        p->nCountXors--;
+    }
+
+    // go through the columns
+    Vec_PtrForEachEntry( Vec_Ptr_t *, p->vBuckets, vBucket, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vBucket, vInput, j )
+    {
+        Vec_IntForEachEntryStart( vInput, ObjId, k, SHARE_NUM )
+        {
+            assert( ObjId < Vec_IntSize(p->vObj2Lit) );
+            if ( ObjId >= p->nStartCols )
+                break;
+            assert( ObjId < p->nStartCols );
+            iLit = Vec_IntEntry( vInput, 0 );
+
+            pNew = (Abc_Obj_t *)Vec_PtrEntry( vRepl, ObjId );
+            pNew = Abc_AigXor( (Abc_Aig_t *)p->pNtk->pManFunc, pNew, Abc_ObjFromLit(p->pNtk, iLit) );
+            Vec_PtrWriteEntry( vRepl, ObjId, pNew );
+            p->nCountXors++;
+        }
+    }
+
+    if ( p->fVerbose )
+        printf( "Total XORs collected = %d.  Total XORs constructed = %d.\n", p->nFoundXors, p->nCountXors );
+
+    // create map of originals
+    vMap2Repl = Vec_IntStartFull( Abc_NtkObjNumMax(p->pNtk) );
+    Vec_PtrForEachEntry( Abc_Obj_t *, vOrig, pObj, i )
+        Vec_IntWriteEntry( vMap2Repl, Abc_ObjId(pObj), Abc_ObjToLit((Abc_Obj_t *)Vec_PtrEntry(vRepl, i)) );
+    Vec_PtrFree( vOrig );
+    Vec_PtrFree( vRepl );
+
+    // update fanin pointers
+    Abc_NtkForEachObj( p->pNtk, pObj, i )
+    {
+        if ( Abc_ObjIsCo(pObj) || Abc_ObjIsNode(pObj) )
+        {
+            iLit = Vec_IntEntry( vMap2Repl, Abc_ObjFaninId0(pObj) );
+            if ( iLit >= 0 )
+            {
+                pObj->fCompl0 ^= Abc_LitIsCompl(iLit);
+                Vec_IntWriteEntry( &pObj->vFanins, 0, Abc_Lit2Var(iLit) );
+            }
+        }
+        if ( Abc_ObjIsNode(pObj) )
+        {
+            iLit = Vec_IntEntry( vMap2Repl, Abc_ObjFaninId1(pObj) );
+            if ( iLit >= 0 )
+            {
+                pObj->fCompl1 ^= Abc_LitIsCompl(iLit);
+                Vec_IntWriteEntry( &pObj->vFanins, 1, Abc_Lit2Var(iLit) );
+            }
+        }
+    }
+    Vec_IntFree( vMap2Repl );
+
+//    pNtk = Abc_NtkRestrash( p->pNtk, 1 );
+    pNtk = Abc_NtkBalanceExor( p->pNtk, 1, 0 );
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates multi-input XOR representation for the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkTraverseSupers_rec( Abc_ShaMan_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vInputs )
+{
+    if ( Abc_NodeIsTravIdCurrent( pObj ) )
+        return;
+    Abc_NodeSetTravIdCurrent( pObj );
+    if ( Abc_ObjIsCi(pObj) )
+        return;
+    assert( Abc_ObjIsNode(pObj) );
+    if ( Abc_NodeIsExorType(pObj) )
+    {
+        Vec_Wrd_t * vSuper;
+        int k, fCompl;
+        word Num;
+        vSuper = Abc_NtkShareSuperXor( pObj, &fCompl, &p->nFoundXors );
+        if ( Vec_WrdSize(vSuper) >= p->nMultiSize )
+        {
+            Vec_WrdForEachEntry( vSuper, Num, k )
+            {
+                Vec_Int_t * vInput = (Vec_Int_t *)Vec_PtrEntry( vInputs, (int)Num );
+                if ( vInput == NULL )
+                {
+                    vInput = Vec_IntAlloc( 10 );
+                    Vec_IntPush( vInput, Abc_Var2Lit((int)Num, 0) );
+                    Vec_IntPush( vInput, Abc_ObjLevel(Abc_NtkObj(p->pNtk, (int)Num)) );
+                    assert( SHARE_NUM == Vec_IntSize(vInput) );
+                    Vec_PtrWriteEntry( vInputs, (int)Num, vInput );
+                }
+                Vec_IntPush( vInput, Vec_IntSize(p->vObj2Lit) );
+            }
+            Vec_IntPush( p->vObj2Lit, Abc_Var2Lit(Abc_ObjId(pObj), fCompl) );
+        }
+        // call recursively
+        Vec_WrdForEachEntry( vSuper, Num, k )
+            Abc_NtkTraverseSupers_rec( p, Abc_NtkObj(p->pNtk, (int)Num), vInputs );
+        Vec_WrdFree( vSuper );
+    }
+    else
+    {
+        Abc_NtkTraverseSupers_rec( p, Abc_ObjFanin0(pObj), vInputs );
+        Abc_NtkTraverseSupers_rec( p, Abc_ObjFanin1(pObj), vInputs );
+    }
+}
+void Abc_NtkTraverseSupers( Abc_ShaMan_t * p )
+{
+    Vec_Ptr_t * vInputs;
+    Vec_Int_t * vInput;
+    Abc_Obj_t * pObj;
+    int i, nOnesMax;
+
+    // create mapping of nodes into their column vectors
+    vInputs = Vec_PtrStart( Abc_NtkObjNumMax(p->pNtk) );
+    Abc_NtkIncrementTravId( p->pNtk );
+    Abc_NtkForEachCo( p->pNtk, pObj, i )
+        Abc_NtkTraverseSupers_rec( p, Abc_ObjFanin0(pObj), vInputs );
+    p->nStartCols = Vec_IntSize(p->vObj2Lit);
+
+    // find the largest number of 1s
+    nOnesMax = 0;
+    Vec_PtrForEachEntry( Vec_Int_t *, vInputs, vInput, i )
+        if ( vInput )
+            nOnesMax = Abc_MaxInt( nOnesMax, Vec_IntSize(vInput)-SHARE_NUM );
+
+    // create buckets
+    assert( p->vBuckets == NULL );
+    p->vBuckets = Vec_PtrAlloc( nOnesMax + 1 );
+    for ( i = 0; i <= nOnesMax; i++ )
+        Vec_PtrPush( p->vBuckets, Vec_PtrAlloc(10) );
+
+    // load vectors into buckets
+    Vec_PtrForEachEntry( Vec_Int_t *, vInputs, vInput, i )
+        if ( vInput )
+            Vec_PtrPush( (Vec_Ptr_t *)Vec_PtrEntry(p->vBuckets, Vec_IntSize(vInput)-SHARE_NUM), vInput );
+    Vec_PtrFree( vInputs );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Extracts one multi-output XOR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkShareXor( Abc_Ntk_t * pNtk, int nMultiSize, int fAnd, int fVerbose )
+{
+    Abc_Ntk_t * pNtkNew;
+    Abc_ShaMan_t * p;
+    assert( Abc_NtkIsStrash(pNtk) );
+    p = Abc_ShaManStart( pNtk );
+    p->nMultiSize = nMultiSize;
+    p->fVerbose   = fVerbose;
+    Abc_NtkTraverseSupers( p );
+    if ( p->nStartCols < 2 )
+    {
+        Abc_ShaManStop( p );
+        return Abc_NtkDup( pNtk );
+    }
+    if ( fVerbose )
+        Abc_NtkSharePrint( p );
+    Abc_NtkShareOptimize( p );
+    if ( fVerbose )
+        Abc_NtkSharePrint( p );
+    pNtkNew = Abc_NtkUpdateNetwork( p );
+    Abc_ShaManStop( p );
+    return pNtkNew;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcShare.c b/src/base/abci/abcShare.c
deleted file mode 100644
index 0dee4214..00000000
--- a/src/base/abci/abcShare.c
+++ /dev/null
@@ -1,448 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [abcShare.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Shared logic extraction.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: abcShare.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "src/base/abc/abc.h"
-
-ABC_NAMESPACE_IMPL_START
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-#define SHARE_NUM 2
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-static inline word  Abc_NtkSharePack( int Lev, int Id )   { return (((word)Lev) << 32) | Id;    }
-static inline int   Abc_NtkShareUnpackLev( word Num )     { return (Num >> 32);                 }
-static inline int   Abc_NtkShareUnpackId( word Num )      { return Num & 0xFFFF;                }
-
-/**Function*************************************************************
-
-  Synopsis    [Collects one multi-input XOR.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Wrd_t * Abc_NtkShareSuperXor( Abc_Obj_t * pObjInit, int * pfCompl )
-{
-    int fCompl = Abc_ObjIsComplement(pObjInit);
-    Abc_Obj_t * pObj = Abc_ObjRegular(pObjInit);
-    Abc_Ntk_t * pNtk = Abc_ObjNtk(pObj);
-    Abc_Obj_t * pObjC, * pObj0, * pObj1, * pRoot;
-    Vec_Wrd_t * vSuper;
-    word Num, NumNext;
-    int i, k;
-    assert( Abc_NodeIsExorType(pObj) );
-    // start iteration
-    vSuper = Vec_WrdAlloc( 10 );
-    Vec_WrdPush( vSuper, Abc_NtkSharePack(Abc_ObjLevel(pObj), Abc_ObjId(pObj)) );
-    while ( Vec_WrdSize(vSuper) > 0 )
-    {
-        // 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 = Abc_NtkObj( pNtk, Abc_NtkShareUnpackId(Num) );
-            if ( Abc_NodeIsExorType(pRoot) )
-            {
-                Vec_WrdRemove( vSuper, Num );
-                break;
-            }
-        }
-        if ( i == -1 )
-            break;
-        // extract
-        pObjC = Abc_NodeRecognizeMux( pRoot, &pObj1, &pObj0 );
-        assert( pObj1 == Abc_ObjNot(pObj0) );
-        fCompl ^= Abc_ObjIsComplement(pObjC);  pObjC = Abc_ObjRegular(pObjC);
-        fCompl ^= Abc_ObjIsComplement(pObj0);  pObj0 = Abc_ObjRegular(pObj0);
-        Vec_WrdPushOrder( vSuper, Abc_NtkSharePack(Abc_ObjLevel(pObjC), Abc_ObjId(pObjC)) );
-        Vec_WrdPushOrder( vSuper, Abc_NtkSharePack(Abc_ObjLevel(pObj0), Abc_ObjId(pObj0)) );
-        // 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, Abc_NtkShareUnpackId(Num) );
-    return vSuper;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Abc_NtkShareFindBest_( Vec_Ptr_t * vBuckets )
-{
-    Vec_Ptr_t * vBucket;
-    int i;
-    Vec_PtrForEachEntryReverse( Vec_Ptr_t *, vBuckets, vBucket, i )
-    {
-        if ( Vec_PtrSize(vBucket) == 0 )
-            continue;
-        return (Vec_Int_t *)Vec_PtrPop( vBucket );
-    }
-    return NULL;
-}
-Vec_Int_t * Abc_NtkShareFindBestMatch_( Vec_Ptr_t * vBuckets, Vec_Int_t * vInput2 )
-{
-    Vec_Ptr_t * vBucket, * vBucketBest = NULL;
-    Vec_Int_t * vInput, * vInputBest = NULL;
-    int i, k, Cost, CostBest = 0;
-    Vec_PtrForEachEntry( Vec_Ptr_t *, vBuckets, vBucket, i )
-        Vec_PtrForEachEntry( Vec_Int_t *, vBucket, vInput, k )
-        {
-            vInput->pArray += SHARE_NUM;
-            vInput2->pArray += SHARE_NUM;
-            vInput->nSize -= SHARE_NUM;
-            vInput2->nSize -= SHARE_NUM;
-
-            Cost = Vec_IntTwoCountCommon(vInput, vInput2);
-
-            vInput->pArray -= SHARE_NUM;
-            vInput2->pArray -= SHARE_NUM;
-            vInput->nSize += SHARE_NUM;
-            vInput2->nSize += SHARE_NUM;
-
-            if ( Cost < 2 )
-                continue;
-
-            if ( CostBest < Cost )
-            {
-                CostBest = Cost;
-                vInputBest = vInput;
-                vBucketBest = vBucket;
-            }
-        }
-    if ( vInputBest )
-        Vec_PtrRemove( vBucketBest, (Vec_Int_t *)vInputBest ); 
-    printf( "%d ", CostBest );
-    return vInputBest;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkShareFindBestMatch( Vec_Ptr_t * vBuckets, Vec_Int_t ** pvInput, Vec_Int_t ** pvInput2 )
-{
-    int nPoolSize = 40;
-    Vec_Ptr_t * vPool = Vec_PtrAlloc( nPoolSize );
-    Vec_Ptr_t * vBucket;
-    Vec_Int_t * vInput, * vInput2, * vInputBest = NULL, * vInputBest2 = NULL;
-    int i, k, Cost, CostBest = 0, Delay, DelayBest = 0;
-
-    Vec_PtrForEachEntryReverse( Vec_Ptr_t *, vBuckets, vBucket, i )
-        Vec_PtrForEachEntry( Vec_Int_t *, vBucket, vInput, k )
-        {
-            Vec_PtrPush( vPool, vInput );
-            if ( Vec_PtrSize(vPool) == nPoolSize )
-                goto outside;
-        }
-outside:
-
-    Vec_PtrForEachEntryReverse( Vec_Int_t *, vPool, vInput, i )
-    Vec_PtrForEachEntryReverse( Vec_Int_t *, vPool, vInput2, k )
-    {
-        if ( i == k )
-            continue;
-
-        vInput->pArray += SHARE_NUM;
-        vInput2->pArray += SHARE_NUM;
-        vInput->nSize -= SHARE_NUM;
-        vInput2->nSize -= SHARE_NUM;
-
-        Cost = Vec_IntTwoCountCommon(vInput, vInput2);
-
-        vInput->pArray -= SHARE_NUM;
-        vInput2->pArray -= SHARE_NUM;
-        vInput->nSize += SHARE_NUM;
-        vInput2->nSize += SHARE_NUM;
-
-        if ( Cost < 2 )
-            continue;
-
-        Delay = Abc_MaxInt( Vec_IntEntry(vInput, 1), Vec_IntEntry(vInput2, 1) );
-
-        if ( CostBest < Cost || (CostBest == Cost && (DelayBest > Delay)) )
-        {
-            CostBest = Cost;
-            DelayBest = Delay;
-            vInputBest = vInput;
-            vInputBest2 = vInput2;
-        }
-    }
-    Vec_PtrFree( vPool );
-
-    *pvInput  = vInputBest;
-    *pvInput2 = vInputBest2;
-
-    if ( vInputBest == NULL )
-        return;
-
-    Vec_PtrRemove( (Vec_Ptr_t *)Vec_PtrEntry(vBuckets, Vec_IntSize(vInputBest)-SHARE_NUM),  (Vec_Int_t *)vInputBest ); 
-    Vec_PtrRemove( (Vec_Ptr_t *)Vec_PtrEntry(vBuckets, Vec_IntSize(vInputBest2)-SHARE_NUM), (Vec_Int_t *)vInputBest2 ); 
-}
-
-void Abc_NtkSharePrint( Abc_Ntk_t * pNtk, Vec_Ptr_t * vBuckets, int Counter )
-{
-    Vec_Ptr_t * vBucket;
-    Vec_Int_t * vInput;
-    int i, k, j, ObjId;
-    char * pBuffer = ABC_ALLOC( char, Counter + 1 );
-    int * pCounters = ABC_CALLOC( int, Counter + 1 );
-    int nTotal = 0;
-    Vec_PtrForEachEntry( Vec_Ptr_t *, vBuckets, vBucket, i )
-    Vec_PtrForEachEntry( Vec_Int_t *, vBucket, vInput, j )
-    {
-        for ( k = 0; k < Counter; k++ )
-            pBuffer[k] = '0';
-        pBuffer[k] = 0;
-
-        Vec_IntForEachEntryStart( vInput, ObjId, k, SHARE_NUM )
-        {
-            assert( ObjId < Counter );
-            pBuffer[ObjId] = '1';
-            pCounters[ObjId]++;
-        }
-
-        printf( "%4d%3d: %s\n", Vec_IntEntry(vInput, 0), Vec_IntEntry(vInput, 1), pBuffer );
-    }
-    ABC_FREE( pBuffer );
-
-    for ( i = 0; i < Counter; i++ )
-        if ( pCounters[i] > 0 )
-            printf( "%d=%d ", i, pCounters[i] ); 
-
-    nTotal = 0;
-    for ( i = 0; i < Abc_NtkCoNum(pNtk); i++ )
-        nTotal += pCounters[i] - 1;
-    printf( "Total = %d.\n", nTotal );
-    printf( "Xors = %d.\n", Counter - Abc_NtkCoNum(pNtk) + nTotal );
-
-    ABC_FREE( pCounters );
-}
-
-void Abc_NtkShareOptimize( Abc_Ntk_t * pNtk, Vec_Ptr_t * vBuckets, int * pCounter )
-{
-    Abc_Obj_t * pObj, * pObj0, * pObj1;
-    Vec_Int_t * vInput, * vInput2;
-    Vec_Int_t * vNew, * vOld1, * vOld2;
-    int i, iLit;
-    for ( i = 0; ; i++ )
-    {
-        Abc_NtkShareFindBestMatch( vBuckets, &vInput, &vInput2 );
-        if ( vInput == NULL )
-            break;
-
-        // create new node
-        pObj0 = Abc_ObjFromLit( pNtk, Vec_IntEntry(vInput,  0) );
-        pObj1 = Abc_ObjFromLit( pNtk, Vec_IntEntry(vInput2, 0) );
-        pObj  = Abc_AigXor( (Abc_Aig_t *)pNtk->pManFunc, pObj0, pObj1 );
-        iLit  = Abc_ObjToLit( pObj );
-
-        // save new node
-        vOld1 = Vec_IntAlloc( 16 );  Vec_IntPush( vOld1, Vec_IntEntry(vInput,  0) );  Vec_IntPush( vOld1, Vec_IntEntry(vInput,  1) );
-        vOld2 = Vec_IntAlloc( 16 );  Vec_IntPush( vOld2, Vec_IntEntry(vInput2, 0) );  Vec_IntPush( vOld2, Vec_IntEntry(vInput2, 1) );
-        vNew  = Vec_IntAlloc( 16 );  Vec_IntPush( vNew,  iLit );                      Vec_IntPush( vNew, Abc_ObjLevel(Abc_ObjRegular(pObj)) );
-
-        // compute new arrays
-        vInput->pArray += SHARE_NUM;
-        vInput2->pArray += SHARE_NUM;
-        vInput->nSize -= SHARE_NUM;
-        vInput2->nSize -= SHARE_NUM;
-
-        Vec_IntTwoSplit( vInput, vInput2, vNew, vOld1, vOld2 );
-
-        vInput->pArray -= SHARE_NUM;
-        vInput2->pArray -= SHARE_NUM;
-        vInput->nSize += SHARE_NUM;
-        vInput2->nSize += SHARE_NUM;
-
-        // add to the old ones
-        Vec_IntPush( vOld1, *pCounter );
-        Vec_IntPush( vOld2, *pCounter );
-        (*pCounter)++;
-
-        Vec_PtrPush( (Vec_Ptr_t *)Vec_PtrEntry(vBuckets, Vec_IntSize(vOld1)-SHARE_NUM), vOld1 );
-        Vec_PtrPush( (Vec_Ptr_t *)Vec_PtrEntry(vBuckets, Vec_IntSize(vOld2)-SHARE_NUM), vOld2 );
-        Vec_PtrPush( (Vec_Ptr_t *)Vec_PtrEntry(vBuckets, Vec_IntSize(vNew)-SHARE_NUM), vNew );
-
-        Vec_IntFree( vInput );
-        Vec_IntFree( vInput2 );
-    }
-    printf( "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Extracts one multi-output XOR.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkShareXor( Abc_Ntk_t * pNtk )
-{
-    Vec_Ptr_t * vBuckets, * vBucket;
-    Vec_Ptr_t * vInputs;
-    Vec_Int_t * vInput;
-    Vec_Wrd_t * vSuper;
-    Abc_Obj_t * pObj;
-    word Num;
-    int i, k, ObjId, fCompl, nOnesMax, Counter;
-    assert( Abc_NtkIsStrash(pNtk) );
-
-    vInputs = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
-    Abc_NtkForEachCo( pNtk, pObj, i )
-    {
-        if ( !Abc_NodeIsExorType(Abc_ObjFanin0(pObj)) )
-            continue;
-        vSuper = Abc_NtkShareSuperXor( Abc_ObjChild0(pObj), &fCompl );
-//printf( "%d ", Vec_WrdSize(vSuper) );
-
-        pObj->fMarkA = fCompl;
-        Vec_WrdForEachEntry( vSuper, Num, k )
-        {
-            ObjId = Abc_NtkShareUnpackId(Num);
-            vInput = (Vec_Int_t *)Vec_PtrEntry( vInputs, ObjId );
-            if ( vInput == NULL )
-            {
-                vInput = Vec_IntAlloc( 10 );
-                Vec_IntPush( vInput, Abc_Var2Lit(ObjId, 0) );
-                Vec_IntPush( vInput, Abc_ObjLevel(Abc_NtkObj(pNtk, ObjId)) );
-                assert( SHARE_NUM == Vec_IntSize(vInput) );
-                Vec_PtrWriteEntry( vInputs, ObjId, vInput );
-            }
-//            Vec_IntPush( vInput, Abc_ObjFaninId0(pObj) );
-//            Vec_IntPush( vInput, Abc_ObjId(pObj) );
-            Vec_IntPush( vInput, i );
-        }
-        Vec_WrdFree( vSuper );
-    }
-//printf( "\n" );
-
-    // find the largest number of 1s
-    nOnesMax = 0;
-    Vec_PtrForEachEntry( Vec_Int_t *, vInputs, vInput, i )
-        if ( vInput )
-            nOnesMax = Abc_MaxInt( nOnesMax, Vec_IntSize(vInput)-SHARE_NUM );
-
-    vBuckets = Vec_PtrAlloc( nOnesMax + 1 );
-    for ( i = 0; i <= nOnesMax; i++ )
-        Vec_PtrPush( vBuckets, Vec_PtrAlloc(10) );
-
-    Vec_PtrForEachEntry( Vec_Int_t *, vInputs, vInput, i )
-        if ( vInput )
-            Vec_PtrPush( (Vec_Ptr_t *)Vec_PtrEntry(vBuckets, Vec_IntSize(vInput)-SHARE_NUM), vInput );
-
-    // find the best match
-    Counter = Abc_NtkCoNum(pNtk);
-    Abc_NtkShareOptimize( pNtk, vBuckets, &Counter );
-
-    Abc_NtkSharePrint( pNtk, vBuckets, Counter );
-
-    // clean up
-    Vec_PtrForEachEntry( Vec_Ptr_t *, vBuckets, vBucket, i )
-        printf( "%d ", Vec_PtrSize(vBucket) );
-    printf( "\n" );
-
-    Vec_PtrForEachEntry( Vec_Ptr_t *, vBuckets, vBucket, i )
-        Vec_VecFree( (Vec_Vec_t *)vBucket );
-    Vec_PtrFree( vBuckets );
-
-/*
-    // print
-    Vec_PtrForEachEntry( Vec_Int_t *, vInputs, vInput, i )
-    {
-        if ( vInput == NULL )
-            continue;
-        pObj = Abc_NtkObj(pNtk, i);
-        assert( Abc_ObjIsCi(pObj) );
-
-        Vec_IntForEachEntryStart( vInput, ObjId, k, SHARE_NUM )
-            Abc_NtkObj( pNtk, ObjId )->fMarkA = 1;
-
-        Abc_NtkForEachCo( pNtk, pObj, k )
-            printf( "%d", pObj->fMarkA );
-        printf( "\n" );
-
-        Vec_IntForEachEntryStart( vInput, ObjId, k, SHARE_NUM )
-            Abc_NtkObj( pNtk, ObjId )->fMarkA = 0;
-    }
-
-    Vec_PtrForEachEntry( Vec_Int_t *, vInputs, vInput, i )
-        Vec_IntFreeP( &vInput );
-*/
-    Vec_PtrFree( vInputs );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 835cf925..5bb93ada 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -49,6 +49,7 @@ static void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, int fAl
 Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, int fCleanup )
 {
 //    extern int timeRetime;
+    Vec_Ptr_t * vNodes;
     Abc_Ntk_t * pNtkAig;
     Abc_Obj_t * pObj;
     int i, nNodes;//, RetValue;
@@ -60,8 +61,10 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, int fCleanup )
     // start the new network (constants and CIs of the old network will point to the their counterparts in the new network)
     pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
     // restrash the nodes (assuming a topological order of the old network)
-    Abc_NtkForEachNode( pNtk, pObj, i )
+    vNodes = Abc_NtkDfs( pNtk, 0 );
+    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
         pObj->pCopy = Abc_AigAnd( (Abc_Aig_t *)pNtkAig->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+    Vec_PtrFree( vNodes );
     // finalize the network
     Abc_NtkFinalize( pNtk, pNtkAig );
     // print warning about self-feed latches
@@ -69,7 +72,9 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, int fCleanup )
 //        printf( "Warning: The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtkAig) );
     // perform cleanup if requested
     if ( fCleanup && (nNodes = Abc_AigCleanup((Abc_Aig_t *)pNtkAig->pManFunc)) ) 
-        printf( "Abc_NtkRestrash(): AIG cleanup removed %d nodes (this is a bug).\n", nNodes );
+    {
+//        printf( "Abc_NtkRestrash(): AIG cleanup removed %d nodes (this is a bug).\n", nNodes );
+    }
     // duplicate EXDC 
     if ( pNtk->pExdc )
         pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );