Version abc70408

14 files changed, 1127 insertions, 50 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 0c7c03f8..98942ca3 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -594,6 +594,7 @@ extern Vec_Ptr_t *        Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll );
 extern Vec_Ptr_t *        Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
 extern Vec_Ptr_t *        Abc_NtkDfsReverse( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkDfsReverseNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
+extern Vec_Ptr_t *        Abc_NtkDfsReverseNodesContained( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
 extern Vec_Ptr_t *        Abc_NtkDfsSeq( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkDfsSeqReverse( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkDfsIter( Abc_Ntk_t * pNtk, int fCollectAll );
@@ -742,6 +743,7 @@ extern Abc_Ntk_t *        Abc_NtkStartRead( char * pName );
 extern void               Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkDup( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNodeName, int fUseAllCis );
+extern Abc_Ntk_t *        Abc_NtkCreateConeArray( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, int fUseAllCis );
 extern Abc_Ntk_t *        Abc_NtkCreateMffc( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNodeName );
 extern Abc_Ntk_t *        Abc_NtkCreateTarget( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues );
 extern Abc_Ntk_t *        Abc_NtkCreateFromNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 4c2bb218..f34a3e85 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -405,6 +405,8 @@ Abc_Obj_t * Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
 {
     Abc_Obj_t * pAnd, * pConst1;
     unsigned Key;
+    assert( Abc_ObjRegular(p0)->pNtk->pManFunc == pMan );
+    assert( Abc_ObjRegular(p1)->pNtk->pManFunc == pMan );
     // check for trivial cases
     pConst1 = Abc_AigConst1(pMan->pNtkAig);
     if ( p0 == p1 )
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index e1728296..3072e40f 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -918,9 +918,7 @@ int Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk )
     assert( !Abc_NtkIsNetlist(pNtk) );
     Abc_NtkForEachCo( pNtk, pObj, i )
     {
-        nCiId = Nm_ManFindIdByName( pNtk->pManName, Abc_ObjName(pObj), ABC_OBJ_PI );
-        if ( nCiId == -1 )
-            nCiId = Nm_ManFindIdByName( pNtk->pManName, Abc_ObjName(pObj), ABC_OBJ_BO );
+        nCiId = Nm_ManFindIdByNameTwoTypes( pNtk->pManName, Abc_ObjName(pObj), ABC_OBJ_PI, ABC_OBJ_BO );
         if ( nCiId == -1 )
             continue;
         pObjCi = Abc_NtkObj( pNtk, nCiId );
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index 4fabd1ff..b682f8ae 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -269,6 +269,79 @@ Vec_Ptr_t * Abc_NtkDfsReverseNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int
     return vNodes;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns the levelized array of TFO nodes.]
+
+  Description [Collects the levelized array of internal nodes, leaving out CIs/COs.
+  However it marks both CIs and COs with the current TravId.
+  Collects only the nodes whose support does not exceed the set of given CI nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkDfsReverseNodesContained( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj, * pFanout, * pFanin;
+    int i, k, m, nLevels;
+    // set the levels
+    nLevels = Abc_NtkLevel( pNtk );
+    // set the traversal ID
+    Abc_NtkIncrementTravId( pNtk );
+    // start the array of nodes
+    vNodes = Vec_PtrStart( nLevels + 2 );
+    for ( i = 0; i < nNodes; i++ )
+    {
+        pObj = ppNodes[i];
+        assert( Abc_ObjIsCi(pObj) );
+        Abc_NodeSetTravIdCurrent( pObj );
+        // add to the array
+        assert( pObj->Level == 0 );
+        pObj->pCopy = Vec_PtrEntry( vNodes, pObj->Level );
+        Vec_PtrWriteEntry( vNodes, pObj->Level, pObj );
+    }
+    // iterate through the levels
+    for ( i = 0; i <= nLevels; i++ )
+    {
+        // iterate through the nodes on each level
+        for ( pObj = Vec_PtrEntry(vNodes, i); pObj; pObj = pObj->pCopy )
+        {
+            // iterate through the fanouts of each node
+            Abc_ObjForEachFanout( pObj, pFanout, k )
+            {
+                // skip visited nodes
+                if ( Abc_NodeIsTravIdCurrent(pFanout) )
+                    continue;
+                // visit the fanins of this fanout
+                Abc_ObjForEachFanin( pFanout, pFanin, m )
+                {
+                    if ( !Abc_NodeIsTravIdCurrent(pFanin) )
+                        break;
+                }
+                if ( m < Abc_ObjFaninNum(pFanout) )
+                    continue;
+                // all fanins are already collected
+
+                // mark the node as visited
+                Abc_NodeSetTravIdCurrent( pFanout );
+                // handle the COs
+                if ( Abc_ObjIsCo(pFanout) )
+                    pFanout->Level = nLevels + 1;
+                // add to the array
+                pFanout->pCopy = Vec_PtrEntry( vNodes, pFanout->Level );
+                Vec_PtrWriteEntry( vNodes, pFanout->Level, pFanout );
+                // handle the COs
+                if ( Abc_ObjIsCo(pFanout) )
+                    pFanout->Level = 0;
+            }
+        }
+    }
+    return vNodes;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index df193212..ce187f60 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -564,6 +564,86 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNode
 
 /**Function*************************************************************
 
+  Synopsis    [Creates the network composed of several logic cones.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkCreateConeArray( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, int fUseAllCis )
+{
+    Abc_Ntk_t * pNtkNew; 
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj, * pFanin, * pNodeCoNew;
+    char Buffer[1000];
+    int i, k;
+
+    assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) );
+    
+    // start the network
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
+    // set the name
+    sprintf( Buffer, "%s_part", pNtk->pName );
+    pNtkNew->pName = Extra_UtilStrsav(Buffer);
+
+    // establish connection between the constant nodes
+    if ( Abc_NtkIsStrash(pNtk) )
+        Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew);
+
+    // collect the nodes in the TFI of the output (mark the TFI)
+    vNodes = Abc_NtkDfsNodes( pNtk, (Abc_Obj_t **)Vec_PtrArray(vRoots), Vec_PtrSize(vRoots) );
+
+    // create the PIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+    {
+        if ( fUseAllCis || Abc_NodeIsTravIdCurrent(pObj) ) // TravId is set by DFS
+        {
+            pObj->pCopy = Abc_NtkCreatePi(pNtkNew);
+            Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL );
+        }
+    }
+
+    // copy the nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        // if it is an AIG, add to the hash table
+        if ( Abc_NtkIsStrash(pNtk) )
+        {
+            pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+        }
+        else
+        {
+            Abc_NtkDupObj( pNtkNew, pObj, 0 );
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+                Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+        }
+    }
+    Vec_PtrFree( vNodes );
+
+    // add the PO corresponding to the nodes
+    Vec_PtrForEachEntry( vRoots, pObj, i )
+    {
+        // create the PO node
+        pNodeCoNew = Abc_NtkCreatePo( pNtkNew );
+        // connect the internal nodes to the new CO
+        if ( Abc_ObjIsCo(pObj) )
+            Abc_ObjAddFanin( pNodeCoNew, Abc_ObjChild0Copy(pObj) );
+        else
+            Abc_ObjAddFanin( pNodeCoNew, pObj->pCopy );
+        // assign the name
+        Abc_ObjAssignName( pNodeCoNew, Abc_ObjName(pObj), NULL );
+    }
+
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkCreateConeArray(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates the network composed of MFFC of one node.]
 
   Description []
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 23b89a5b..3de48f00 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -1595,6 +1595,140 @@ void Abc_NtkPrint256()
     fclose( pFile );
 }
 
+
+static     int * pSupps;
+
+/**Function*************************************************************
+
+  Synopsis    [Compares the supergates by their level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkCompareConesCompare( int * pNum1, int * pNum2 )
+{
+    if ( pSupps[*pNum1] > pSupps[*pNum2] )
+        return -1;
+    if ( pSupps[*pNum1] < pSupps[*pNum2] )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Analyze choice node support.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCompareCones( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vSupp, * vNodes, * vReverse;
+    Abc_Obj_t * pObj, * pTemp;
+    int Iter, i, k, Counter, CounterCos, CounterCosNew;
+    int * pPerms;
+
+    // sort COs by support size
+    pPerms = ALLOC( int, Abc_NtkCoNum(pNtk) );
+    pSupps = ALLOC( int, Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        pPerms[i] = i;
+        vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
+        pSupps[i] = Vec_PtrSize(vSupp);
+        Vec_PtrFree( vSupp );
+    }
+    qsort( (void *)pPerms, Abc_NtkCoNum(pNtk), sizeof(int), (int (*)(const void *, const void *)) Abc_NtkCompareConesCompare );
+
+    // consider COs in this order
+    Iter = 0;
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        pObj = Abc_NtkCo( pNtk, pPerms[i] );
+        if ( pObj->fMarkA )
+            continue;
+        Iter++;
+
+        vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
+        vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 );
+        vReverse = Abc_NtkDfsReverseNodesContained( pNtk, (Abc_Obj_t **)Vec_PtrArray(vSupp), Vec_PtrSize(vSupp) );
+        // count the number of nodes in the reverse cone
+        Counter = 0;
+        for ( k = 1; k < Vec_PtrSize(vReverse) - 1; k++ )
+            for ( pTemp = Vec_PtrEntry(vReverse, k); pTemp; pTemp = pTemp->pCopy )
+                Counter++;
+        CounterCos = CounterCosNew = 0;
+        for ( pTemp = Vec_PtrEntryLast(vReverse); pTemp; pTemp = pTemp->pCopy )
+        {
+            assert( Abc_ObjIsCo(pTemp) );
+            CounterCos++;
+            if ( pTemp->fMarkA == 0 )
+                CounterCosNew++;
+            pTemp->fMarkA = 1;
+        }
+        // print statistics
+        printf( "%4d CO %5d :  Supp = %5d.  Lev = %3d.  Cone = %5d.  Rev = %5d.  COs = %3d (%3d).\n",
+            Iter, pPerms[i], Vec_PtrSize(vSupp), Abc_ObjLevel(Abc_ObjFanin0(pObj)), Vec_PtrSize(vNodes), Counter, CounterCos, CounterCosNew );
+
+        // free arrays
+        Vec_PtrFree( vSupp );
+        Vec_PtrFree( vNodes );
+        Vec_PtrFree( vReverse );
+
+        if ( Vec_PtrSize(vSupp) < 10 )
+            break;
+    }
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        pObj->fMarkA = 0;
+
+    free( pPerms );
+    free( pSupps );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Analyze choice node support.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCompareSupports( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vSupp;
+    Abc_Obj_t * pObj, * pTemp;
+    int i, nNodesOld;
+    assert( Abc_NtkIsStrash(pNtk) );
+    Abc_AigForEachAnd( pNtk, pObj, i )
+    {
+        if ( !Abc_AigNodeIsChoice(pObj) )
+            continue;
+
+        vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
+        nNodesOld = Vec_PtrSize(vSupp);
+        Vec_PtrFree( vSupp );
+
+        for ( pTemp = pObj->pData; pTemp; pTemp = pTemp->pData )
+        {
+            vSupp = Abc_NtkNodeSupport( pNtk, &pTemp, 1 );
+            if ( nNodesOld != Vec_PtrSize(vSupp) )
+                printf( "Choice orig = %3d  Choice new = %3d\n", nNodesOld, Vec_PtrSize(vSupp) );
+            Vec_PtrFree( vSupp );
+        }
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index a91d6325..39d7cb2b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2914,7 +2914,7 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nGrowthLevel =  1;
     pPars->fSatur       =  1;
     pPars->fZeroCost    =  0; 
-    pPars->fVerbose     =  1;
+    pPars->fVerbose     =  0;
     pPars->fVeryVerbose =  0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszvwh" ) ) != EOF )
@@ -3834,6 +3834,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    char Buffer[32];
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtk1, * pNtk2, * pNtkRes;
     int fDelete1, fDelete2;
@@ -3842,6 +3843,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int fCheck;
     int fComb;
+    int nPartSize;
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -3850,11 +3852,23 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     fComb  = 1;
     fCheck = 1;
+    nPartSize = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Pch" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nPartSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nPartSize < 0 ) 
+                goto usage;
+            break;
         case 'c':
             fComb ^= 1;
             break;
@@ -3869,7 +3883,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
 
     // compute the miter
-    pNtkRes = Abc_NtkMiter( pNtk1, pNtk2, fComb, 0 );
+    pNtkRes = Abc_NtkMiter( pNtk1, pNtk2, fComb, nPartSize );
     if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
     if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
 
@@ -3884,14 +3898,19 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: miter [-ch] <file1> <file2>\n" );
-    fprintf( pErr, "\t        computes the miter of the two circuits\n" );
-    fprintf( pErr, "\t-c    : computes combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" );
-    fprintf( pErr, "\t-h    : print the command usage\n");
-    fprintf( pErr, "\tfile1 : (optional) the file with the first network\n");
-    fprintf( pErr, "\tfile2 : (optional) the file with the second network\n");
-    fprintf( pErr, "\t        if no files are given, uses the current network and its spec\n");
-    fprintf( pErr, "\t        if one file is given, uses the current network and the file\n");
+    if ( nPartSize == 0 )
+        strcpy( Buffer, "unused" );
+    else
+        sprintf( Buffer, "%d", nPartSize );
+    fprintf( pErr, "usage: miter [-P num] [-ch] <file1> <file2>\n" );
+    fprintf( pErr, "\t         computes the miter of the two circuits\n" );
+    fprintf( pErr, "\t-P num : output partition size [default = %s]\n", Buffer );
+    fprintf( pErr, "\t-c     : computes combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    fprintf( pErr, "\tfile1  : (optional) the file with the first network\n");
+    fprintf( pErr, "\tfile2  : (optional) the file with the second network\n");
+    fprintf( pErr, "\t         if no files are given, uses the current network and its spec\n");
+    fprintf( pErr, "\t         if one file is given, uses the current network and the file\n");
     return 1;
 }
 
@@ -5915,6 +5934,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk );
 //    extern void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk );
 //    extern int Pr_ManProofTest( char * pFileName );
+    extern void Abc_NtkCompareSupports( Abc_Ntk_t * pNtk );
+    extern void Abc_NtkCompareCones( Abc_Ntk_t * pNtk );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -6010,6 +6031,17 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 */
 //    Abc_NtkMaxFlowTest( pNtk );
 //    Pr_ManProofTest( "trace.cnf" );
+
+//    Abc_NtkCompareSupports( pNtk );
+//    Abc_NtkCompareCones( pNtk );
+
+    {
+        extern Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int fVerbose );
+        Vec_Vec_t * vParts;
+        vParts = Abc_NtkPartitionSmart( pNtk, 1 );
+        Vec_VecFree( vParts );
+    }
+
     return 0;
 
 usage:
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index 96c468fe..30e49af2 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -704,6 +704,8 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFraigRestore()
 {
+    extern Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams );
+
     Fraig_Params_t Params;
     Abc_Ntk_t * pStore, * pFraig;
     int nWords1, nWords2, nWordsMin;
@@ -743,7 +745,9 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
 
 //    Fraig_ManReportChoices( p );
     // transform it into FRAIG
-    pFraig = Abc_NtkFraig( pStore, &Params, 1, 0 );
+//    pFraig = Abc_NtkFraig( pStore, &Params, 1, 0 );
+    pFraig = Abc_NtkFraigPartitioned( pStore, &Params );
+
 PRT( "Total fraiging time", clock() - clk );
     if ( pFraig == NULL )
         return NULL;
diff --git a/src/base/abci/abcHaig.c b/src/base/abci/abcHaig.c
index a0ed5906..d3513bbe 100644
--- a/src/base/abci/abcHaig.c
+++ b/src/base/abci/abcHaig.c
@@ -364,7 +364,7 @@ Hop_Man_t * Abc_NtkHaigReconstruct( Hop_Man_t * p )
         if ( pObj->pData ) // member of the class
             Hop_Regular(pObj->pNext)->pData = Hop_Regular(((Hop_Obj_t *)pObj->pData)->pNext);
     }
-    printf( " Counter = %d.\n", Counter );
+//    printf( " Counter = %d.\n", Counter );
     // transfer the POs
     Hop_ManForEachPo( p, pObj, i )
         Hop_ObjCreatePo( pNew, Hop_ObjChild0Hop(pObj) );
@@ -681,15 +681,7 @@ Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk )
         pMan = Abc_NtkHaigReconstruct( pManTemp = pMan );
         Hop_ManStop( pManTemp );
     }
-/*
-    pMan = Abc_NtkHaigReconstruct( pManTemp = pMan );
-    Hop_ManStop( pManTemp );
-    Abc_NtkHaigResetReprs( pMan );
 
-    pMan = Abc_NtkHaigReconstruct( pManTemp = pMan );
-    Hop_ManStop( pManTemp );
-    Abc_NtkHaigResetReprs( pMan );
-*/
     // traverse in the topological order and create new AIG
     pNtkAig = Abc_NtkHaigRecreateAig( pNtk, pMan );
     Hop_ManStop( pMan );
@@ -698,6 +690,35 @@ Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk )
     return pNtkAig;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Transform HOP manager into the one without loops.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkHopRemoveLoops( Abc_Ntk_t * pNtk, Hop_Man_t * pMan )
+{
+    Abc_Ntk_t * pNtkAig;
+    Hop_Man_t * pManTemp;
+
+    // iteratively reconstruct the HOP manager to create choice nodes
+    while ( Abc_NtkHaigResetReprs( pMan ) )
+    {
+        pMan = Abc_NtkHaigReconstruct( pManTemp = pMan );
+        Hop_ManStop( pManTemp );
+    }
+
+    // traverse in the topological order and create new AIG
+    pNtkAig = Abc_NtkHaigRecreateAig( pNtk, pMan );
+    Hop_ManStop( pMan );
+    return pNtkAig;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 823d81cc..445c73c1 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -25,7 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize );
-static void        Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb );
+static void        Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize );
 static void        Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter );
 static void        Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize );
 static void        Abc_NtkAddFrame( Abc_Ntk_t * pNetNew, Abc_Ntk_t * pNet, int iFrame );
@@ -94,7 +94,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, in
     pNtkMiter->pName = Extra_UtilStrsav(Buffer);
 
     // perform strashing
-    Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, fComb );
+    Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize );
     Abc_NtkMiterAddOne( pNtk1, pNtkMiter );
     Abc_NtkMiterAddOne( pNtk2, pNtkMiter );
     Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize );
@@ -120,7 +120,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, in
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb )
+void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize )
 {
     Abc_Obj_t * pObj, * pObjNew;
     int i;
@@ -143,10 +143,13 @@ void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtk
             // add name
             Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), NULL );
         }
-        // create the only PO
-        pObjNew = Abc_NtkCreatePo( pNtkMiter );
-        // add the PO name
-        Abc_ObjAssignName( pObjNew, "miter", NULL );
+        if ( nPartSize <= 0 )
+        {
+            // create the only PO
+            pObjNew = Abc_NtkCreatePo( pNtkMiter );
+            // add the PO name
+            Abc_ObjAssignName( pObjNew, "miter", NULL );
+        }
     }
     else
     {
@@ -161,10 +164,13 @@ void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtk
             // add name
             Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), NULL );
         }
-        // create the only PO
-        pObjNew = Abc_NtkCreatePo( pNtkMiter );
-        // add the PO name
-        Abc_ObjAssignName( pObjNew, "miter", NULL );
+        if ( nPartSize <= 0 )
+        {
+            // create the only PO
+            pObjNew = Abc_NtkCreatePo( pNtkMiter );
+            // add the PO name
+            Abc_ObjAssignName( pObjNew, "miter", NULL );
+        }
         // create the latches
         Abc_NtkForEachLatch( pNtk1, pObj, i )
         {
@@ -276,7 +282,7 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
             Abc_ObjAddFanin( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjChild0Copy(Abc_ObjFanin0(pNode)) );
     }
     // add the miter
-    if ( nPartSize == 0 )
+    if ( nPartSize <= 0 )
     {
         pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairs );
         Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
@@ -284,7 +290,7 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
     }
     else
     {
-        char Buffer[10];
+        char Buffer[1024];
         Vec_Ptr_t * vPairsPart;
         int nParts, i, k, iCur;
         assert( Vec_PtrSize(vPairs) == 2 * Abc_NtkCoNum(pNtk1) );
@@ -303,15 +309,14 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
                 Vec_PtrPush( vPairsPart, Vec_PtrEntry(vPairs, 2*iCur+1) );
             }
             pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairsPart );
-            if ( i == 0 )
-                Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
+            pNode = Abc_NtkCreatePo( pNtkMiter );
+            Abc_ObjAddFanin( pNode, pMiter );
+            // assign the name to the node
+            if ( nPartSize == 1 )
+                sprintf( Buffer, "%s", Abc_ObjName(Abc_NtkPo(pNtk1,i)) );
             else
-            {
                 sprintf( Buffer, "%d", i );
-                pNode = Abc_NtkCreatePo( pNtkMiter );
-                Abc_ObjAssignName( pNode, "miter", Buffer );
-                Abc_ObjAddFanin( pNode, pMiter );
-            }
+            Abc_ObjAssignName( pNode, "miter_", Buffer );
         }
         Vec_PtrFree( vPairsPart );
         Vec_PtrFree( vPairs );
@@ -355,7 +360,7 @@ Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOr, int
     pNtkMiter->pName = Extra_UtilStrsav(Buffer);
 
     // perform strashing
-    Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, 1 );
+    Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, 1, -1 );
     Abc_NtkMiterAddOne( pNtk1, pNtkMiter );
     Abc_NtkMiterAddOne( pNtk2, pNtkMiter );
 //    Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, 1 );
@@ -414,7 +419,7 @@ Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues )
     pRoot = Abc_NtkCo( pNtk, 0 );
 
     // perform strashing
-    Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1 );
+    Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1, -1 );
     // set the first cofactor
     Vec_IntForEachEntry( vPiValues, Value, i )
     {
@@ -482,7 +487,7 @@ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In
     pRoot = Abc_NtkCo( pNtk, Out );
 
     // perform strashing
-    Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1 );
+    Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1, -1 );
     // set the first cofactor
     Abc_NtkCi(pNtk, In1)->pCopy = Abc_ObjNot( Abc_AigConst1(pNtkMiter) );
     if ( In2 >= 0 )
@@ -547,7 +552,7 @@ Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist )
     pRoot = Abc_NtkCo( pNtk, 0 );
 
     // perform strashing
-    Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1 );
+    Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1, -1 );
     // set the first cofactor
     Abc_NtkCi(pNtk, In)->pCopy = Abc_ObjNot( Abc_AigConst1(pNtkMiter) );
     // add the first cofactor
diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c
new file mode 100644
index 00000000..14e33c36
--- /dev/null
+++ b/src/base/abci/abcPart.c
@@ -0,0 +1,703 @@
+/**CFile****************************************************************
+
+  FileName    [abcPart.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Output partitioning package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcPart.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Prepare supports.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkPartitionCollectSupps( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vSupp, * vSupports;
+    Vec_Int_t * vSuppI;
+    Abc_Obj_t * pObj, * pTemp;
+    int i, k;
+    vSupports = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
+        vSuppI = (Vec_Int_t *)vSupp;
+        Vec_PtrForEachEntry( vSupp, pTemp, k )
+            Vec_IntWriteEntry( vSuppI, k, pTemp->Id );
+        Vec_IntSort( vSuppI, 0 );
+        // append the number of this output
+        Vec_IntPush( vSuppI, i );
+        // save the support in the vector
+        Vec_PtrPush( vSupports, vSuppI );
+    }
+    // sort supports by size
+    Vec_VecSort( (Vec_Vec_t *)vSupports, 1 );
+    return vSupports;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find the best partition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Int_t * vOne )
+{
+    Vec_Int_t * vPartSupp;
+    double Attract, Repulse, Cost, CostBest;
+    int i, nCommon, iBest;
+    iBest = -1;
+    CostBest = 0.0;
+    Vec_PtrForEachEntry( vPartSuppsAll, vPartSupp, i )
+    {
+        nCommon = Vec_IntTwoCountCommon( vPartSupp, vOne );
+        if ( nCommon == Vec_IntSize(vOne) )
+            return i;
+        Attract = 1.0 * nCommon / Vec_IntSize(vOne);
+        if ( Vec_IntSize(vPartSupp) < 100 )
+            Repulse = 1.0;
+        else
+            Repulse = log10( Vec_IntSize(vPartSupp) / 10.0 );
+        Cost = pow( Attract, pow(Repulse, 5.0) );
+        if ( CostBest < Cost )
+        {
+            CostBest = Cost;
+            iBest = i;
+        }
+    }
+    if ( CostBest < 0.6 )
+        return -1;
+    return iBest;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Perform the smart partitioning.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPartitionPrint( Abc_Ntk_t * pNtk, Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll )
+{
+    Vec_Int_t * vOne;
+    int i, nOutputs, Counter;
+
+    Counter = 0;
+    Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
+    {
+        nOutputs = Vec_IntSize(Vec_PtrEntry(vPartsAll, i));
+        printf( "%d=(%d,%d) ", i, Vec_IntSize(vOne), nOutputs );
+        Counter += nOutputs;
+        if ( i == Vec_PtrSize(vPartsAll) - 1 )
+            break;
+    }
+    assert( Counter == Abc_NtkCoNum(pNtk) );
+    printf( "\nTotal = %d. Outputs = %d.\n", Counter, Abc_NtkCoNum(pNtk) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Perform the smart partitioning.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll )
+{
+    Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
+    int i, iPart;
+
+    // pack smaller partitions into larger blocks
+    iPart = 0;
+    vPart = vPartSupp = NULL;
+    Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
+    {
+        if ( Vec_IntSize(vOne) < 200 )
+        {
+            if ( vPartSupp == NULL )
+            {
+                assert( vPart == NULL );
+                vPartSupp = Vec_IntDup(vOne);
+                vPart = Vec_PtrEntry(vPartsAll, i);
+            }
+            else
+            {
+                vPartSupp = Vec_IntTwoMerge( vTemp = vPartSupp, vOne );
+                Vec_IntFree( vTemp );
+                vPart = Vec_IntTwoMerge( vTemp = vPart, Vec_PtrEntry(vPartsAll, i) );
+                Vec_IntFree( vTemp );
+                Vec_IntFree( Vec_PtrEntry(vPartsAll, i) );
+            }
+            if ( Vec_IntSize(vPartSupp) < 200 )
+                continue;
+        }
+        else
+            vPart = Vec_PtrEntry(vPartsAll, i);
+        // add the partition 
+        Vec_PtrWriteEntry( vPartsAll, iPart, vPart );  
+        vPart = NULL;
+        if ( vPartSupp ) 
+        {
+            Vec_IntFree( Vec_PtrEntry(vPartSuppsAll, iPart) );
+            Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp );  
+            vPartSupp = NULL;
+        }
+        iPart++;
+    }
+    // add the last one
+    if ( vPart )
+    {
+        Vec_PtrWriteEntry( vPartsAll, iPart, vPart );  
+        vPart = NULL;
+
+        assert( vPartSupp != NULL );
+        Vec_IntFree( Vec_PtrEntry(vPartSuppsAll, iPart) );
+        Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp );  
+        vPartSupp = NULL;
+        iPart++;
+    }
+    Vec_PtrShrink( vPartsAll, iPart );
+    Vec_PtrShrink( vPartsAll, iPart );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Perform the smart partitioning.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Vec_Ptr_t * vSupps, * vPartsAll, * vPartsAll2, * vPartSuppsAll, * vPartPtr;
+    Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
+    int i, iPart, iOut, clk;
+
+    // compute the supports for all outputs
+clk = clock();
+    vSupps = Abc_NtkPartitionCollectSupps( pNtk );
+if ( fVerbose )
+{
+PRT( "Supps", clock() - clk );
+}
+
+    // create partitions
+clk = clock();
+    vPartsAll = Vec_PtrAlloc( 256 );
+    vPartSuppsAll = Vec_PtrAlloc( 256 );
+    Vec_PtrForEachEntry( vSupps, vOne, i )
+    {
+        // get the output number
+        iOut = Vec_IntPop(vOne);
+        // find closely matching part
+        iPart = Abc_NtkPartitionSmartFindPart( vPartSuppsAll, vOne );
+        if ( iPart == -1 )
+        {
+            // create new partition
+            vPart = Vec_IntAlloc( 32 );
+            Vec_IntPush( vPart, iOut );
+            // create new partition support
+            vPartSupp = Vec_IntDup( vOne );
+            // add this partition and its support
+            Vec_PtrPush( vPartsAll, vPart );
+            Vec_PtrPush( vPartSuppsAll, vPartSupp );
+        }
+        else
+        {
+            // add output to this partition
+            vPart = Vec_PtrEntry( vPartsAll, iPart );
+            Vec_IntPush( vPart, iOut );
+            // merge supports
+            vPartSupp = Vec_PtrEntry( vPartSuppsAll, iPart );
+            vPartSupp = Vec_IntTwoMerge( vTemp = vPartSupp, vOne );
+            Vec_IntFree( vTemp );
+            // reinsert new support
+            Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp );
+        }
+    }
+if ( fVerbose )
+{
+PRT( "Parts", clock() - clk );
+}
+
+clk = clock();
+    // remember number of supports
+    Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
+        Vec_IntPush( vOne, i );
+    // sort the supports in the decreasing order
+    Vec_VecSort( (Vec_Vec_t *)vPartSuppsAll, 1 );
+    // reproduce partitions
+    vPartsAll2 = Vec_PtrAlloc( 256 );
+    Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
+        Vec_PtrPush( vPartsAll2, Vec_PtrEntry(vPartsAll, Vec_IntPop(vOne)) );
+    Vec_PtrFree( vPartsAll );
+    vPartsAll = vPartsAll2;
+
+    // compact small partitions
+//    Abc_NtkPartitionPrint( pNtk, vPartsAll, vPartSuppsAll );
+    Abc_NtkPartitionCompact( vPartsAll, vPartSuppsAll );
+    if ( fVerbose )
+    Abc_NtkPartitionPrint( pNtk, vPartsAll, vPartSuppsAll );
+if ( fVerbose )
+{
+PRT( "Comps", clock() - clk );
+}
+
+    // cleanup
+    Vec_VecFree( (Vec_Vec_t *)vSupps );
+    Vec_VecFree( (Vec_Vec_t *)vPartSuppsAll );
+
+    // converts from intergers to nodes
+    Vec_PtrForEachEntry( vPartsAll, vPart, iPart )
+    {
+        vPartPtr = Vec_PtrAlloc( Vec_IntSize(vPart) );
+        Vec_IntForEachEntry( vPart, iOut, i )
+            Vec_PtrPush( vPartPtr, Abc_NtkCo(pNtk, iOut) );
+        Vec_IntFree( vPart );
+        Vec_PtrWriteEntry( vPartsAll, iPart, vPartPtr );
+    }
+    return (Vec_Vec_t *)vPartsAll;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Perform the naive partitioning.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Abc_NtkPartitionNaive( Abc_Ntk_t * pNtk, int nPartSize )
+{
+    Vec_Vec_t * vParts;
+    Abc_Obj_t * pObj;
+    int nParts, i;
+    nParts = (Abc_NtkCoNum(pNtk) / nPartSize) + ((Abc_NtkCoNum(pNtk) % nPartSize) > 0);
+    vParts = Vec_VecStart( nParts );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Vec_VecPush( vParts, i / nPartSize, pObj );
+    return vParts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns representative of the given node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkPartStitchFindRepr_rec( Vec_Ptr_t * vEquiv, Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pRepr;
+    pRepr = Vec_PtrEntry( vEquiv, pObj->Id );
+    if ( pRepr == NULL || pRepr == pObj )
+        return pObj;
+    return Abc_NtkPartStitchFindRepr_rec( vEquiv, pRepr );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the representative of the fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Abc_Obj_t * Abc_NtkPartStitchCopy0( Vec_Ptr_t * vEquiv, Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFan = Abc_ObjFanin0( pObj );
+    Abc_Obj_t * pRepr = Abc_NtkPartStitchFindRepr_rec( vEquiv, pFan );
+    return Abc_ObjNotCond( pRepr->pCopy, pRepr->fPhase ^ pFan->fPhase ^ Abc_ObjFaninC1(pObj) );
+}
+static inline Abc_Obj_t * Abc_NtkPartStitchCopy1( Vec_Ptr_t * vEquiv, Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFan = Abc_ObjFanin1( pObj );
+    Abc_Obj_t * pRepr = Abc_NtkPartStitchFindRepr_rec( vEquiv, pFan );
+    return Abc_ObjNotCond( pRepr->pCopy, pRepr->fPhase ^ pFan->fPhase ^ Abc_ObjFaninC1(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stitches together several networks with choice nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkPartStitchChoices_old( Abc_Ntk_t * pNtk, Vec_Ptr_t * vParts )
+{
+    Vec_Ptr_t * vNodes, * vEquiv;
+    Abc_Ntk_t * pNtkNew, * pNtkNew2, * pNtkTemp;
+    Abc_Obj_t * pObj, * pFanin, * pRepr0, * pRepr1, * pRepr;
+    int i, k, iNodeId;
+
+    // start a new network similar to the original one
+    assert( Abc_NtkIsStrash(pNtk) );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // duplicate the name and the spec
+    pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
+    pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+
+    // annotate parts to point to the new network
+    vEquiv = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) + 1 );
+    Vec_PtrForEachEntry( vParts, pNtkTemp, i )
+    {
+        assert( Abc_NtkIsStrash(pNtkTemp) );
+        Abc_NtkCleanCopy( pNtkTemp );
+
+        // map the CI nodes
+        Abc_AigConst1(pNtkTemp)->pCopy = Abc_AigConst1(pNtkNew);
+        Abc_NtkForEachCi( pNtkTemp, pObj, k )
+        {
+            iNodeId = Nm_ManFindIdByNameTwoTypes( pNtkNew->pManName, Abc_ObjName(pObj), ABC_OBJ_PI, ABC_OBJ_BO );
+            if ( iNodeId == -1 )
+            {
+                printf( "Cannot find CI node %s in the original network.\n", Abc_ObjName(pObj) );
+                return NULL;
+            }
+            pObj->pCopy = Abc_NtkObj( pNtkNew, iNodeId );
+        }
+
+        // add the internal nodes while saving representatives
+        vNodes = Abc_AigDfs( pNtkTemp, 1, 0 );
+        Vec_PtrForEachEntry( vNodes, pObj, k )
+        {
+            pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+            assert( !Abc_ObjIsComplement(pObj->pCopy) );
+            if ( !Abc_AigNodeIsChoice(pObj) )
+                continue;
+            // find the earliest representative of the choice node
+            pRepr0 = NULL;
+            for ( pFanin = pObj; pFanin; pFanin = pFanin->pData )
+            {
+                pRepr1 = Abc_NtkPartStitchFindRepr_rec( vEquiv, pFanin->pCopy );
+                if ( pRepr0 == NULL || pRepr0->Id > pRepr1->Id )
+                    pRepr0 = pRepr1;
+            }
+            // set this representative for the representives of all choices
+            for ( pFanin = pObj; pFanin; pFanin = pFanin->pData )
+            {
+                pRepr1 = Abc_NtkPartStitchFindRepr_rec( vEquiv, pFanin->pCopy );
+                Vec_PtrWriteEntry( vEquiv, pRepr1->Id, pRepr0 );
+            }
+        }
+        Vec_PtrFree( vNodes );
+
+        // map the CO nodes
+        Abc_NtkForEachCo( pNtkTemp, pObj, k )
+        {
+            iNodeId = Nm_ManFindIdByNameTwoTypes( pNtkNew->pManName, Abc_ObjName(pObj), ABC_OBJ_PO, ABC_OBJ_BI );
+            if ( iNodeId == -1 )
+            {
+                printf( "Cannot find CO node %s in the original network.\n", Abc_ObjName(pObj) );
+                return NULL;
+            }
+            pObj->pCopy = Abc_NtkObj( pNtkNew, iNodeId );
+            Abc_ObjAddFanin( pObj->pCopy, Abc_ObjChild0Copy(pObj) );
+        }
+    }
+
+    // reconstruct the AIG
+    pNtkNew2 = Abc_NtkStartFrom( pNtkNew, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // duplicate the name and the spec
+    pNtkNew2->pName = Extra_UtilStrsav(pNtkNew->pName);
+    pNtkNew2->pSpec = Extra_UtilStrsav(pNtkNew->pSpec);
+    // duplicate internal nodes
+    Abc_AigForEachAnd( pNtkNew, pObj, i )
+    {
+        pRepr0 = Abc_NtkPartStitchCopy0( vEquiv, pObj );
+        pRepr1 = Abc_NtkPartStitchCopy1( vEquiv, pObj );
+        pObj->pCopy = Abc_AigAnd( pNtkNew2->pManFunc, pRepr0, pRepr1 );
+        assert( !Abc_ObjIsComplement(pObj->pCopy) );
+        // add the choice if applicable
+        pRepr = Abc_NtkPartStitchFindRepr_rec( vEquiv, pObj );
+        if ( pObj != pRepr )
+        {
+            assert( pObj->Id > pRepr->Id );
+            if ( pObj->pCopy != pRepr->pCopy )
+            {
+                assert( pObj->pCopy->Id > pRepr->pCopy->Id );
+                pObj->pCopy->pData = pRepr->pCopy->pData;
+                pRepr->pCopy->pData = pObj->pCopy;
+            }
+        }
+    }
+    // connect the COs
+    Abc_NtkForEachCo( pNtkNew, pObj, k )
+        Abc_ObjAddFanin( pObj->pCopy, Abc_NtkPartStitchCopy0(vEquiv,pObj) );
+
+    // replace the network
+    Abc_NtkDelete( pNtkNew );
+    pNtkNew = pNtkNew2;
+
+    // check correctness of the new network
+    Vec_PtrFree( vEquiv );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkPartStitchChoices: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Hop_Obj_t * Hop_ObjChild0Next( Abc_Obj_t * pObj ) { return Hop_NotCond( (Hop_Obj_t *)Abc_ObjFanin0(pObj)->pNext, Abc_ObjFaninC0(pObj) ); }
+static inline Hop_Obj_t * Hop_ObjChild1Next( Abc_Obj_t * pObj ) { return Hop_NotCond( (Hop_Obj_t *)Abc_ObjFanin1(pObj)->pNext, Abc_ObjFaninC1(pObj) ); }
+
+
+/**Function*************************************************************
+
+  Synopsis    [Stitches together several networks with choice nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Man_t * Abc_NtkPartStartHop( Abc_Ntk_t * pNtk )
+{
+    Hop_Man_t * pMan;
+    Abc_Obj_t * pObj;
+    int i;
+    // start the HOP package
+    pMan = Hop_ManStart();
+    pMan->vObjs = Vec_PtrAlloc( Abc_NtkObjNumMax(pNtk) + 1  );
+    Vec_PtrPush( pMan->vObjs, Hop_ManConst1(pMan) );
+    // map constant node and PIs
+    Abc_AigConst1(pNtk)->pNext = (Abc_Obj_t *)Hop_ManConst1(pMan);
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->pNext = (Abc_Obj_t *)Hop_ObjCreatePi(pMan);
+    // map the internal nodes
+    Abc_AigForEachAnd( pNtk, pObj, i )
+    {
+        pObj->pNext = (Abc_Obj_t *)Hop_And( pMan, Hop_ObjChild0Next(pObj), Hop_ObjChild1Next(pObj) );
+        assert( !Abc_ObjIsComplement(pObj->pNext) );
+    }
+    // set the choice nodes
+    Abc_AigForEachAnd( pNtk, pObj, i )
+    {
+        if ( pObj->pCopy )
+            ((Hop_Obj_t *)pObj->pNext)->pData = pObj->pCopy->pNext;
+    }
+    // transfer the POs
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Hop_ObjCreatePo( pMan, Hop_ObjChild0Next(pObj) );
+    // check the new manager
+    if ( !Hop_ManCheck(pMan) )
+        printf( "Abc_NtkPartStartHop: HOP manager check has failed.\n" );
+    return pMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stitches together several networks with choice nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkPartStitchChoices( Abc_Ntk_t * pNtk, Vec_Ptr_t * vParts )
+{
+    extern Abc_Ntk_t * Abc_NtkHopRemoveLoops( Abc_Ntk_t * pNtk, Hop_Man_t * pMan );
+
+    Hop_Man_t * pMan;
+    Vec_Ptr_t * vNodes;
+    Abc_Ntk_t * pNtkNew, * pNtkTemp;
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k, iNodeId;
+
+    // start a new network similar to the original one
+    assert( Abc_NtkIsStrash(pNtk) );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+
+    // annotate parts to point to the new network
+    Vec_PtrForEachEntry( vParts, pNtkTemp, i )
+    {
+        assert( Abc_NtkIsStrash(pNtkTemp) );
+        Abc_NtkCleanCopy( pNtkTemp );
+
+        // map the CI nodes
+        Abc_AigConst1(pNtkTemp)->pCopy = Abc_AigConst1(pNtkNew);
+        Abc_NtkForEachCi( pNtkTemp, pObj, k )
+        {
+            iNodeId = Nm_ManFindIdByNameTwoTypes( pNtkNew->pManName, Abc_ObjName(pObj), ABC_OBJ_PI, ABC_OBJ_BO );
+            if ( iNodeId == -1 )
+            {
+                printf( "Cannot find CI node %s in the original network.\n", Abc_ObjName(pObj) );
+                return NULL;
+            }
+            pObj->pCopy = Abc_NtkObj( pNtkNew, iNodeId );
+        }
+
+        // add the internal nodes while saving representatives
+        vNodes = Abc_AigDfs( pNtkTemp, 1, 0 );
+        Vec_PtrForEachEntry( vNodes, pObj, k )
+        {
+            pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+            assert( !Abc_ObjIsComplement(pObj->pCopy) );
+            if ( Abc_AigNodeIsChoice(pObj) )
+                for ( pFanin = pObj->pData; pFanin; pFanin = pFanin->pData )
+                    pFanin->pCopy->pCopy = pObj->pCopy;
+        }
+        Vec_PtrFree( vNodes );
+
+        // map the CO nodes
+        Abc_NtkForEachCo( pNtkTemp, pObj, k )
+        {
+            iNodeId = Nm_ManFindIdByNameTwoTypes( pNtkNew->pManName, Abc_ObjName(pObj), ABC_OBJ_PO, ABC_OBJ_BI );
+            if ( iNodeId == -1 )
+            {
+                printf( "Cannot find CO node %s in the original network.\n", Abc_ObjName(pObj) );
+                return NULL;
+            }
+            pObj->pCopy = Abc_NtkObj( pNtkNew, iNodeId );
+            Abc_ObjAddFanin( pObj->pCopy, Abc_ObjChild0Copy(pObj) );
+        }
+    }
+
+    // transform into the HOP manager
+    pMan = Abc_NtkPartStartHop( pNtkNew );
+    pNtkNew = Abc_NtkHopRemoveLoops( pNtkTemp = pNtkNew, pMan );
+    Abc_NtkDelete( pNtkTemp );
+
+    // check correctness of the new network
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkPartStitchChoices: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stitches together several networks with choice nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams )
+{
+    extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
+    extern void * Abc_FrameGetGlobalFrame();
+
+    Vec_Vec_t * vParts;
+    Vec_Ptr_t * vFraigs, * vOne;
+    Abc_Ntk_t * pNtkAig, * pNtkFraig;
+    int i;
+
+    // perform partitioning
+    assert( Abc_NtkIsStrash(pNtk) );
+//    vParts = Abc_NtkPartitionNaive( pNtk, 20 );
+    vParts = Abc_NtkPartitionSmart( pNtk, 0 );
+
+    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
+
+    // fraig each partition
+    vFraigs = Vec_PtrAlloc( Vec_VecSize(vParts) );
+    Vec_VecForEachLevel( vParts, vOne, i )
+    {
+        pNtkAig = Abc_NtkCreateConeArray( pNtk, vOne, 0 );
+        pNtkFraig = Abc_NtkFraig( pNtkAig, pParams, 0, 0 );
+        Vec_PtrPush( vFraigs, pNtkFraig );
+        Abc_NtkDelete( pNtkAig );
+
+        printf( "Finished part %d (out of %d)\r", i+1, Vec_VecSize(vParts) );
+    }
+    Vec_VecFree( vParts );
+
+    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
+
+    // derive the final network
+    pNtkFraig = Abc_NtkPartStitchChoices( pNtk, vFraigs );
+    Vec_PtrForEachEntry( vFraigs, pNtkAig, i )
+        Abc_NtkDelete( pNtkAig );
+    Vec_PtrFree( vFraigs );
+
+    return pNtkFraig;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 4f48f3bf..b1a0dc5b 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -168,6 +168,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos )
     // perform strashing
     nNewCis = 0;
     Abc_NtkCleanCopy( pNtk2 );
+    Abc_AigConst1(pNtk2)->pCopy = Abc_AigConst1(pNtk1);
     Abc_NtkForEachCi( pNtk2, pObj, i )
     {
         pName = Abc_ObjName(pObj);
@@ -196,6 +197,27 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos )
             Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj->pCopy), NULL );
         }
     }
+    else
+    {
+        Abc_Obj_t * pObjOld, * pDriverOld, * pDriverNew;
+        int fCompl, iNodeId;
+        // OR the choices
+        Abc_NtkForEachCo( pNtk2, pObj, i )
+        {
+            iNodeId = Nm_ManFindIdByNameTwoTypes( pNtk1->pManName, Abc_ObjName(pObj), ABC_OBJ_PO, ABC_OBJ_BI );
+            assert( iNodeId >= 0 );
+            pObjOld = Abc_NtkObj( pNtk1, iNodeId );
+            // derive the new driver
+            pDriverOld = Abc_ObjChild0( pObjOld );
+            pDriverNew = Abc_ObjChild0Copy( pObj );
+            pDriverNew = Abc_AigOr( pNtk1->pManFunc, pDriverOld, pDriverNew );
+            if ( Abc_ObjRegular(pDriverOld) == Abc_ObjRegular(pDriverNew) )
+                continue;
+            // replace the old driver by the new driver
+            fCompl = Abc_ObjRegular(pDriverOld)->fPhase ^ Abc_ObjRegular(pDriverNew)->fPhase;
+            Abc_ObjPatchFanin( pObjOld, Abc_ObjRegular(pDriverOld), Abc_ObjNotCond(Abc_ObjRegular(pDriverNew), fCompl) );
+        }
+    }
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtk1 ) )
     {
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index e8eb6c7f..5d5bccb8 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -29,6 +29,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcNtbdd.c \
     src/base/abci/abcOdc.c \
     src/base/abci/abcOrder.c \
+    src/base/abci/abcPart.c \
     src/base/abci/abcPlace.c \
     src/base/abci/abcPrint.c \
     src/base/abci/abcProve.c \
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 166925e4..1a9a4617 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -53,8 +53,8 @@ void *      Abc_FrameReadManDd()                     { if ( s_GlobalFrame->dd ==
 void *      Abc_FrameReadManDec()                    { if ( s_GlobalFrame->pManDec == NULL ) s_GlobalFrame->pManDec = Dec_ManStart();                                        return s_GlobalFrame->pManDec; } 
 char *      Abc_FrameReadFlag( char * pFlag )        { return Cmd_FlagReadByName( s_GlobalFrame, pFlag );  } 
 
-void        Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk ) { s_GlobalFrame->pStored  = pNtk;     } 
-void        Abc_FrameSetNtkStoreSize( int nStored )  { s_GlobalFrame->nStored  = nStored;  }
+void        Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk ) { s_GlobalFrame->pStored   = pNtk;    } 
+void        Abc_FrameSetNtkStoreSize( int nStored )  { s_GlobalFrame->nStored   = nStored; }
 void        Abc_FrameSetLibLut( void * pLib )        { s_GlobalFrame->pLibLut   = pLib;    } 
 void        Abc_FrameSetLibGen( void * pLib )        { s_GlobalFrame->pLibGen   = pLib;    } 
 void        Abc_FrameSetLibSuper( void * pLib )      { s_GlobalFrame->pLibSuper = pLib;    }