Version abc70901

5 files changed, 584 insertions, 278 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f740ee18..571aa02c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2977,6 +2977,9 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
+    printf("This command will be available soon\n");
+    return 0;
+
     // set defaults
     memset( pPars, 0, sizeof(Lpk_Par_t) );
     pPars->nLutsMax     =  4; // (N) the maximum number of LUTs in the structure
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index fa6771b3..64cb2b38 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -648,46 +648,32 @@ Abc_Obj_t * Abc_NodeFraigTrust( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
+int Abc_NtkFraigStore( Abc_Ntk_t * pNtkAdd )
 {
-    Abc_Ntk_t * pStore;
-    int nAndsOld;
-
-    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
+    Vec_Ptr_t * vStore;
+    Abc_Ntk_t * pNtk;
+    // create the network to be stored
+    pNtk = Abc_NtkStrash( pNtkAdd, 0, 0, 0 );
+    if ( pNtk == NULL )
     {
-        printf( "The netlist need to be converted into a logic network before adding it to storage.\n" );
+        printf( "Abc_NtkFraigStore: Initial strashing has failed.\n" );
         return 0;
     }
-
     // get the network currently stored
-    pStore = Abc_FrameReadNtkStore();
-    if ( pStore == NULL )
+    vStore = Abc_FrameReadStore();
+    if ( Vec_PtrSize(vStore) > 0 )
     {
-        // start the stored network
-        pStore = Abc_NtkStrash( pNtk, 0, 0, 0 );
-        if ( pStore == NULL )
+        // check that the networks have the same PIs
+        // reorder PIs of pNtk2 according to pNtk1
+        if ( !Abc_NtkCompareSignals( pNtk, Vec_PtrEntry(vStore, 0), 1, 1 ) )
         {
-            printf( "Abc_NtkFraigStore: Initial strashing has failed.\n" );
-            return 0;
+            printf( "Trying to store the network with different primary inputs.\n" );
+            printf( "The previously stored networks are deleted and this one is added.\n" );
+            Abc_NtkFraigStoreClean();
         }
-        // save the parameters
-        Abc_FrameSetNtkStore( pStore );
-        Abc_FrameSetNtkStoreSize( 1 );
-        nAndsOld = 0;
     }
-    else
-    {
-        // add the new network to storage
-        nAndsOld = Abc_NtkNodeNum( pStore );
-        if ( !Abc_NtkAppend( pStore, pNtk, 0 ) )
-        {
-            printf( "The current network cannot be appended to the stored network.\n" );
-            return 0;
-        }
-        // set the number of networks stored
-        Abc_FrameSetNtkStoreSize( Abc_FrameReadNtkStoreSize() + 1 );
-    }
-    printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld );
+    Vec_PtrPush( vStore, pNtk );
+    printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pNtk) );
     return 1;
 }
 
@@ -704,54 +690,48 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFraigRestore()
 {
-    extern Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams );
-
+    extern Abc_Ntk_t * Abc_NtkFraigPartitioned( Vec_Ptr_t * vStore, void * pParams );
     Fraig_Params_t Params;
-    Abc_Ntk_t * pStore, * pFraig;
+    Vec_Ptr_t * vStore;
+    Abc_Ntk_t * pNtk, * pFraig;
     int nWords1, nWords2, nWordsMin;
     int clk = clock();
 
     // get the stored network
-    pStore = Abc_FrameReadNtkStore();
-    Abc_FrameSetNtkStore( NULL );
-    if ( pStore == NULL )
+    vStore = Abc_FrameReadStore();
+    if ( Vec_PtrSize(vStore) == 0 )
     {
         printf( "There are no network currently in storage.\n" );
         return NULL;
     }
-    printf( "Currently stored %d networks with %d nodes will be fraiged.\n", 
-        Abc_FrameReadNtkStoreSize(), Abc_NtkNodeNum(pStore) );
+    printf( "Currently stored %d networks will be fraiged.\n", Vec_PtrSize(vStore) );
+    pNtk = Vec_PtrEntry( vStore, 0 );
 
     // to determine the number of simulation patterns
     // use the following strategy
     // at least 64 words (32 words random and 32 words dynamic)
     // no more than 256M for one circuit (128M + 128M)
     nWords1 = 32;
-    nWords2 = (1<<27) / (Abc_NtkNodeNum(pStore) + Abc_NtkCiNum(pStore));
+    nWords2 = (1<<27) / (Abc_NtkNodeNum(pNtk) + Abc_NtkCiNum(pNtk));
     nWordsMin = ABC_MIN( nWords1, nWords2 );
 
     // set parameters for fraiging
     Fraig_ParamsSetDefault( &Params );
-    Params.nPatsRand  = nWordsMin * 32; // the number of words of random simulation info
-    Params.nPatsDyna  = nWordsMin * 32; // the number of words of dynamic simulation info
-    Params.nBTLimit   = 999999;             // the max number of backtracks to perform
-    Params.fFuncRed   =  1;             // performs only one level hashing
-    Params.fFeedBack  =  1;             // enables solver feedback
-    Params.fDist1Pats =  1;             // enables distance-1 patterns
-    Params.fDoSparse  =  1;             // performs equiv tests for sparse functions 
-    Params.fChoicing  =  1;             // enables recording structural choices
-    Params.fTryProve  =  0;             // tries to solve the final miter
-    Params.fVerbose   =  0;             // the verbosiness flag
-
-//    Fraig_ManReportChoices( p );
-    // transform it into FRAIG
-//    pFraig = Abc_NtkFraig( pStore, &Params, 1, 0 );
-    pFraig = Abc_NtkFraigPartitioned( pStore, &Params );
-
-PRT( "Total fraiging time", clock() - clk );
-    if ( pFraig == NULL )
-        return NULL;
-    Abc_NtkDelete( pStore );
+    Params.nPatsRand  = nWordsMin * 32;    // the number of words of random simulation info
+    Params.nPatsDyna  = nWordsMin * 32;    // the number of words of dynamic simulation info
+    Params.nBTLimit   = 1000;              // the max number of backtracks to perform
+    Params.fFuncRed   =    1;              // performs only one level hashing
+    Params.fFeedBack  =    1;              // enables solver feedback
+    Params.fDist1Pats =    1;              // enables distance-1 patterns
+    Params.fDoSparse  =    1;              // performs equiv tests for sparse functions 
+    Params.fChoicing  =    1;              // enables recording structural choices
+    Params.fTryProve  =    0;              // tries to solve the final miter
+    Params.fVerbose   =    0;              // the verbosiness flag
+
+    // perform partitioned computation of structural choices
+    pFraig = Abc_NtkFraigPartitioned( vStore, &Params );
+    Abc_NtkFraigStoreClean();
+PRT( "Total choicing time", clock() - clk );
     return pFraig;
 }
 
@@ -768,12 +748,13 @@ PRT( "Total fraiging time", clock() - clk );
 ***********************************************************************/
 void Abc_NtkFraigStoreClean()
 {
-    Abc_Ntk_t * pStore;
-    // get the stored network
-    pStore = Abc_FrameReadNtkStore();
-    if ( pStore )
-        Abc_NtkDelete( pStore );
-    Abc_FrameSetNtkStore( NULL );
+    Vec_Ptr_t * vStore;
+    Abc_Ntk_t * pNtk;
+    int i;
+    vStore = Abc_FrameReadStore();
+    Vec_PtrForEachEntry( vStore, pNtk, i )
+        Abc_NtkDelete( pNtk );
+    Vec_PtrClear( vStore );
 }
 
 /**Function*************************************************************
@@ -794,7 +775,7 @@ void Abc_NtkFraigStoreCheck( Abc_Ntk_t * pFraig )
     int i, k;
     // check that the PO functions are correct
     nPoFinal = Abc_NtkPoNum(pFraig);
-    nStored  = Abc_FrameReadNtkStoreSize();
+    nStored  = Abc_FrameReadStoreSize();
     assert( nPoFinal % nStored == 0 );
     nPoOrig  = nPoFinal / nStored;
     for ( i = 0; i < nPoOrig; i++ )
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 5dc63750..adda6653 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -314,7 +314,7 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
             Abc_ObjAddFanin( pNode, pMiter );
             // assign the name to the node
             if ( nPartSize == 1 )
-                sprintf( Buffer, "%s", Abc_ObjName(Abc_NtkPo(pNtk1,i)) );
+                sprintf( Buffer, "%s", Abc_ObjName(Abc_NtkCo(pNtk1,i)) );
             else
                 sprintf( Buffer, "%d", i );
             Abc_ObjAssignName( pNode, "miter_", Buffer );
diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c
index 23e9d28d..85c4e918 100644
--- a/src/base/abci/abcPart.c
+++ b/src/base/abci/abcPart.c
@@ -24,13 +24,238 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+typedef struct Supp_Man_t_     Supp_Man_t;
+struct Supp_Man_t_
+{
+    int              nChunkSize;    // the size of one chunk of memory (~1 Mb)
+    int              nStepSize;     // the step size in saving memory (~64 bytes)
+    char *           pFreeBuf;      // the pointer to free memory
+    int              nFreeSize;     // the size of remaining free memory
+    Vec_Ptr_t *      vMemory;       // the memory allocated
+    Vec_Ptr_t *      vFree;         // the vector of free pieces of memory
+};
+
+typedef struct Supp_One_t_     Supp_One_t;
+struct Supp_One_t_
+{
+    int              nRefs;         // the number of references
+    int              nOuts;         // the number of outputs
+    int              nOutsAlloc;    // the array size
+    int              pOuts[0];      // the array of outputs
+};
+
+static inline int    Supp_SizeType( int nSize, int nStepSize )     { return nSize / nStepSize + ((nSize % nStepSize) > 0); }
+static inline char * Supp_OneNext( char * pPart )                  { return *((char **)pPart);                             }
+static inline void   Supp_OneSetNext( char * pPart, char * pNext ) { *((char **)pPart) = pNext;                            }
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Prepare supports.]
+  Synopsis    [Start the memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Supp_Man_t * Supp_ManStart( int nChunkSize, int nStepSize )
+{
+    Supp_Man_t * p;
+    p = ALLOC( Supp_Man_t, 1 );
+    memset( p, 0, sizeof(Supp_Man_t) );
+    p->nChunkSize = nChunkSize;
+    p->nStepSize  = nStepSize;
+    p->vMemory    = Vec_PtrAlloc( 1000 );
+    p->vFree      = Vec_PtrAlloc( 1000 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Supp_ManStop( Supp_Man_t * p )
+{
+    void * pMemory;
+    int i;
+    Vec_PtrForEachEntry( p->vMemory, pMemory, i )
+        free( pMemory );
+    Vec_PtrFree( p->vMemory );
+    Vec_PtrFree( p->vFree );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fetches the memory entry of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Supp_ManFetch( Supp_Man_t * p, int nSize )
+{
+    int Type, nSizeReal;
+    char * pMemory;
+    assert( nSize > 0 );
+    Type = Supp_SizeType( nSize, p->nStepSize );
+    Vec_PtrFillExtra( p->vFree, Type + 1, NULL );
+    if ( pMemory = Vec_PtrEntry( p->vFree, Type ) )
+    {
+        Vec_PtrWriteEntry( p->vFree, Type, Supp_OneNext(pMemory) );
+        return pMemory;
+    }
+    nSizeReal = p->nStepSize * Type;
+    if ( p->nFreeSize < nSizeReal )
+    {
+        p->pFreeBuf = ALLOC( char, p->nChunkSize );
+        p->nFreeSize = p->nChunkSize;
+        Vec_PtrPush( p->vMemory, p->pFreeBuf );
+    }
+    assert( p->nFreeSize >= nSizeReal );
+    pMemory = p->pFreeBuf;
+    p->pFreeBuf  += nSizeReal;
+    p->nFreeSize -= nSizeReal;
+    return pMemory;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the memory entry of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Supp_ManRecycle( Supp_Man_t * p, char * pMemory, int nSize )
+{
+    int Type;
+    Type = Supp_SizeType( nSize, p->nStepSize );
+    Vec_PtrFillExtra( p->vFree, Type + 1, NULL );
+    Supp_OneSetNext( pMemory, Vec_PtrEntry(p->vFree, Type) );
+    Vec_PtrWriteEntry( p->vFree, Type, pMemory );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fetches the memory entry of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Supp_One_t * Supp_ManFetchEntry( Supp_Man_t * p, int nWords, int nRefs )
+{
+    Supp_One_t * pPart;
+    pPart = (Supp_One_t *)Supp_ManFetch( p, sizeof(Supp_One_t) + sizeof(int) * nWords );
+    pPart->nRefs = nRefs;
+    pPart->nOuts = 0;
+    pPart->nOutsAlloc = nWords;
+    return pPart;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the memory entry of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Supp_ManRecycleEntry( Supp_Man_t * p, Supp_One_t * pEntry )
+{
+    assert( pEntry->nOuts <= pEntry->nOutsAlloc );
+    assert( pEntry->nOuts >= pEntry->nOutsAlloc/2 );
+    Supp_ManRecycle( p, (char *)pEntry, sizeof(Supp_One_t) + sizeof(int) * pEntry->nOutsAlloc );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two entries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Supp_One_t * Supp_ManMergeEntry( Supp_Man_t * pMan, Supp_One_t * p1, Supp_One_t * p2, int nRefs )
+{
+    Supp_One_t * p = Supp_ManFetchEntry( pMan, p1->nOuts + p2->nOuts, nRefs );
+    int * pBeg1 = p1->pOuts;
+    int * pBeg2 = p2->pOuts;
+    int * pBeg  = p->pOuts;
+    int * pEnd1 = p1->pOuts + p1->nOuts;
+    int * pEnd2 = p2->pOuts + p2->nOuts;
+    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+    {
+        if ( *pBeg1 == *pBeg2 )
+            *pBeg++ = *pBeg1++, pBeg2++;
+        else if ( *pBeg1 < *pBeg2 )
+            *pBeg++ = *pBeg1++;
+        else 
+            *pBeg++ = *pBeg2++;
+    }
+    while ( pBeg1 < pEnd1 )
+        *pBeg++ = *pBeg1++;
+    while ( pBeg2 < pEnd2 )
+        *pBeg++ = *pBeg2++;
+    p->nOuts = pBeg - p->pOuts;
+    assert( p->nOuts <= p->nOutsAlloc );
+    assert( p->nOuts >= p1->nOuts );
+    assert( p->nOuts >= p2->nOuts );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Tranfers the entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Supp_ManTransferEntry( Supp_One_t * p )
+{
+    Vec_Int_t * vSupp;
+    int i;
+    vSupp = Vec_IntAlloc( p->nOuts );
+    for ( i = 0; i < p->nOuts; i++ )
+        Vec_IntPush( vSupp, p->pOuts[i] );
+    return vSupp;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes supports of the POs in the multi-output AIG.]
 
   Description []
                
@@ -39,7 +264,152 @@
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Abc_NtkPartitionCollectSupps( Abc_Ntk_t * pNtk )
+Vec_Ptr_t * Abc_NtkDfsNatural( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj, * pNext;
+    int i, k;
+    assert( Abc_NtkIsStrash(pNtk) );
+    vNodes = Vec_PtrAlloc( Abc_NtkObjNum(pNtk) );
+    Abc_NtkIncrementTravId( pNtk );
+    // add the constant-1 nodes
+    pObj = Abc_AigConst1(pNtk);
+    Abc_NodeSetTravIdCurrent( pObj );
+    Vec_PtrPush( vNodes, pObj );
+    // add the CIs/nodes/COs in the topological order
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        // check the fanins and add CIs
+        Abc_ObjForEachFanin( pObj, pNext, k )
+            if ( Abc_ObjIsCi(pNext) && !Abc_NodeIsTravIdCurrent(pNext) )
+            {
+                Abc_NodeSetTravIdCurrent( pNext );
+                Vec_PtrPush( vNodes, pNext );
+            }
+        // add the node
+        Vec_PtrPush( vNodes, pObj );
+        // check the fanouts and add COs
+        Abc_ObjForEachFanout( pObj, pNext, k )
+            if ( Abc_ObjIsCo(pNext) && !Abc_NodeIsTravIdCurrent(pNext) )
+            {
+                Abc_NodeSetTravIdCurrent( pNext );
+                Vec_PtrPush( vNodes, pNext );
+            }
+    }
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes supports of the POs.]
+
+  Description [Returns the ptr-vector of int-vectors.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkComputeSupportsSmart( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vSupports;
+    Vec_Ptr_t * vNodes;
+    Vec_Int_t * vSupp;
+    Supp_Man_t * p;
+    Supp_One_t * pPart0, * pPart1;
+    Abc_Obj_t * pObj;
+    int i;
+    // set the number of PIs/POs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->pNext = (Abc_Obj_t *)i;
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        pObj->pNext = (Abc_Obj_t *)i;
+    // start the support computation manager
+    p = Supp_ManStart( 1 << 20, 1 << 6 );
+    // consider objects in the topological order
+    vSupports = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
+    Abc_NtkCleanCopy(pNtk);
+    // order the nodes so that the PIs and POs follow naturally
+    vNodes = Abc_NtkDfsNatural( pNtk );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        if ( Abc_ObjIsNode(pObj) )
+        {
+            pPart0 = (Supp_One_t *)Abc_ObjFanin0(pObj)->pCopy;
+            pPart1 = (Supp_One_t *)Abc_ObjFanin1(pObj)->pCopy;
+            pObj->pCopy = (Abc_Obj_t *)Supp_ManMergeEntry( p, pPart0, pPart1, Abc_ObjFanoutNum(pObj) );
+            assert( pPart0->nRefs > 0 );
+            if ( --pPart0->nRefs == 0 )
+                Supp_ManRecycleEntry( p, pPart0 );
+            assert( pPart1->nRefs > 0 );
+            if ( --pPart1->nRefs == 0 )
+                Supp_ManRecycleEntry( p, pPart1 );
+            continue;
+        }
+        if ( Abc_ObjIsCo(pObj) )
+        {
+            pPart0 = (Supp_One_t *)Abc_ObjFanin0(pObj)->pCopy;
+            // only save the CO if it is non-trivial
+            if ( Abc_ObjIsNode(Abc_ObjFanin0(pObj)) )
+            {
+                vSupp = Supp_ManTransferEntry(pPart0);
+                Vec_IntPush( vSupp, (int)pObj->pNext );
+                Vec_PtrPush( vSupports, vSupp );
+            }
+            assert( pPart0->nRefs > 0 );
+            if ( --pPart0->nRefs == 0 )
+                Supp_ManRecycleEntry( p, pPart0 );
+            continue;
+        }
+        if ( Abc_ObjIsCi(pObj) )
+        {
+            if ( Abc_ObjFanoutNum(pObj) )
+            {
+                pPart0 = (Supp_One_t *)Supp_ManFetchEntry( p, 1, Abc_ObjFanoutNum(pObj) );
+                pPart0->pOuts[ pPart0->nOuts++ ] = (int)pObj->pNext;
+                pObj->pCopy = (Abc_Obj_t *)pPart0;
+            }
+            continue;
+        }
+        if ( pObj == Abc_AigConst1(pNtk) )
+        {
+            if ( Abc_ObjFanoutNum(pObj) )
+                pObj->pCopy = (Abc_Obj_t *)Supp_ManFetchEntry( p, 0, Abc_ObjFanoutNum(pObj) );
+            continue;
+        }
+        assert( 0 );
+    }
+    Vec_PtrFree( vNodes );
+//printf( "Memory usage = %d Mb.\n", Vec_PtrSize(p->vMemory) * p->nChunkSize / (1<<20) );
+    Supp_ManStop( p );
+    // sort supports by size
+    Vec_VecSort( (Vec_Vec_t *)vSupports, 1 );
+    // clear the number of PIs/POs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->pNext = NULL;
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        pObj->pNext = NULL;
+/*
+    Vec_PtrForEachEntry( vSupports, vSupp, i )
+        printf( "%d ", Vec_IntSize(vSupp) );
+    printf( "\n" );
+*/
+    return vSupports;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes supports of the POs using naive method.]
+
+  Description [Returns the ptr-vector of int-vectors.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkComputeSupportsNaive( Abc_Ntk_t * pNtk )
 {
     Vec_Ptr_t * vSupp, * vSupports;
     Vec_Int_t * vSuppI;
@@ -47,29 +417,39 @@ Vec_Ptr_t * Abc_NtkPartitionCollectSupps( Abc_Ntk_t * pNtk )
     int i, k;
     // set the PI numbers
     Abc_NtkForEachCi( pNtk, pObj, i )
-        pObj->pCopy = (void *)i;
-    // save hte CI numbers
+        pObj->pNext = (void *)i;
+    // save the CI numbers
     vSupports = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
     Abc_NtkForEachCo( pNtk, pObj, i )
     {
+        if ( !Abc_ObjIsNode(Abc_ObjFanin0(pObj)) )
+            continue;
         vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
         vSuppI = (Vec_Int_t *)vSupp;
         Vec_PtrForEachEntry( vSupp, pTemp, k )
-            Vec_IntWriteEntry( vSuppI, k, (int)pTemp->pCopy );
+            Vec_IntWriteEntry( vSuppI, k, (int)pTemp->pNext );
         Vec_IntSort( vSuppI, 0 );
         // append the number of this output
         Vec_IntPush( vSuppI, i );
         // save the support in the vector
         Vec_PtrPush( vSupports, vSuppI );
     }
+    // clean the CI numbers
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->pNext = NULL;
     // sort supports by size
     Vec_VecSort( (Vec_Vec_t *)vSupports, 1 );
+/*
+    Vec_PtrForEachEntry( vSupports, vSuppI, i )
+        printf( "%d ", Vec_IntSize(vSuppI) );
+    printf( "\n" );
+*/
     return vSupports;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Start char-bases support representation.]
+  Synopsis    [Start bitwise support representation.]
 
   Description []
                
@@ -78,23 +458,24 @@ Vec_Ptr_t * Abc_NtkPartitionCollectSupps( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_NtkSuppCharStart( Vec_Int_t * vOne, int nPis )
+unsigned * Abc_NtkSuppCharStart( Vec_Int_t * vOne, int nPis )
 {
-    char * pBuffer;
+    unsigned * pBuffer;
     int i, Entry;
-    pBuffer = ALLOC( char, nPis );
-    memset( pBuffer, 0, sizeof(char) * nPis );
+    int nWords = Abc_BitWordNum(nPis);
+    pBuffer = ALLOC( unsigned, nWords );
+    memset( pBuffer, 0, sizeof(unsigned) * nWords );
     Vec_IntForEachEntry( vOne, Entry, i )
     {
         assert( Entry < nPis );
-        pBuffer[Entry] = 1;
+        Abc_InfoSetBit( pBuffer, Entry );
     }
     return pBuffer;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Add to char-bases support representation.]
+  Synopsis    [Add to bitwise support representation.]
 
   Description []
                
@@ -103,19 +484,19 @@ char * Abc_NtkSuppCharStart( Vec_Int_t * vOne, int nPis )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkSuppCharAdd( char * pBuffer, Vec_Int_t * vOne, int nPis )
+void Abc_NtkSuppCharAdd( unsigned * pBuffer, Vec_Int_t * vOne, int nPis )
 {
     int i, Entry;
     Vec_IntForEachEntry( vOne, Entry, i )
     {
         assert( Entry < nPis );
-        pBuffer[Entry] = 1;
+        Abc_InfoSetBit( pBuffer, Entry );
     }
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Find the common variables using char-bases support representation.]
+  Synopsis    [Find the common variables using bitwise support representation.]
 
   Description []
                
@@ -124,11 +505,11 @@ void Abc_NtkSuppCharAdd( char * pBuffer, Vec_Int_t * vOne, int nPis )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkSuppCharCommon( char * pBuffer, Vec_Int_t * vOne )
+int Abc_NtkSuppCharCommon( unsigned * pBuffer, Vec_Int_t * vOne )
 {
     int i, Entry, nCommon = 0;
     Vec_IntForEachEntry( vOne, Entry, i )
-        nCommon += pBuffer[Entry];
+        nCommon += Abc_InfoHasBit(pBuffer, Entry);
     return nCommon;
 }
 
@@ -143,7 +524,7 @@ int Abc_NtkSuppCharCommon( char * pBuffer, Vec_Int_t * vOne )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsChar, int nPartSizeLimit, Vec_Int_t * vOne )
+int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsChar, int nSuppSizeLimit, Vec_Int_t * vOne )
 {
 /*
     Vec_Int_t * vPartSupp, * vPart;
@@ -178,7 +559,7 @@ int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vParts
     return iBest;
 */
 
-    Vec_Int_t * vPartSupp, * vPart;
+    Vec_Int_t * vPartSupp;//, * vPart;
     int Attract, Repulse, Value, ValueBest;
     int i, nCommon, iBest;
 //    int nCommon2;
@@ -186,16 +567,24 @@ int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vParts
     ValueBest = 0;
     Vec_PtrForEachEntry( vPartSuppsAll, vPartSupp, i )
     {
-        vPart = Vec_PtrEntry( vPartsAll, i );
-        if ( nPartSizeLimit > 0 && Vec_IntSize(vPart) >= nPartSizeLimit )
-            continue;
+        // skip partitions with too many outputs
+//        vPart = Vec_PtrEntry( vPartsAll, i );
+//        if ( nSuppSizeLimit > 0 && Vec_IntSize(vPart) >= nSuppSizeLimit )
+//            continue;
+        // find the number of common variables between this output and the partitions
 //        nCommon2 = Vec_IntTwoCountCommon( vPartSupp, vOne );
         nCommon = Abc_NtkSuppCharCommon( Vec_PtrEntry(vPartSuppsChar, i), vOne );
 //        assert( nCommon2 == nCommon );
+        // if no common variables, continue searching
         if ( nCommon == 0 )
             continue;
+        // if all variables are common, the best partition if found
         if ( nCommon == Vec_IntSize(vOne) )
             return i;
+        // skip partitions whose size exceeds the limit
+        if ( nSuppSizeLimit > 0 && Vec_IntSize(vPartSupp) >= 2 * nSuppSizeLimit )
+            continue;
+        // figure out might be the good partition for this one
         Attract = 1000 * nCommon / Vec_IntSize(vOne);
         if ( Vec_IntSize(vPartSupp) < 100 )
             Repulse = 1;
@@ -238,7 +627,7 @@ void Abc_NtkPartitionPrint( Abc_Ntk_t * pNtk, Vec_Ptr_t * vPartsAll, Vec_Ptr_t *
         if ( i == Vec_PtrSize(vPartsAll) - 1 )
             break;
     }
-    assert( Counter == Abc_NtkCoNum(pNtk) );
+//    assert( Counter == Abc_NtkCoNum(pNtk) );
     printf( "\nTotal = %d. Outputs = %d.\n", Counter, Abc_NtkCoNum(pNtk) );
 }
 
@@ -253,20 +642,20 @@ void Abc_NtkPartitionPrint( Abc_Ntk_t * pNtk, Vec_Ptr_t * vPartsAll, Vec_Ptr_t *
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll, int nPartSizeLimit )
+void Abc_NtkPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll, int nSuppSizeLimit )
 {
     Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
     int i, iPart;
 
-    if ( nPartSizeLimit == 0 )
-        nPartSizeLimit = 200;
+    if ( nSuppSizeLimit == 0 )
+        nSuppSizeLimit = 200;
 
     // pack smaller partitions into larger blocks
     iPart = 0;
     vPart = vPartSupp = NULL;
     Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
     {
-        if ( Vec_IntSize(vOne) < nPartSizeLimit )
+        if ( Vec_IntSize(vOne) < nSuppSizeLimit )
         {
             if ( vPartSupp == NULL )
             {
@@ -282,7 +671,7 @@ void Abc_NtkPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll,
                 Vec_IntFree( vTemp );
                 Vec_IntFree( Vec_PtrEntry(vPartsAll, i) );
             }
-            if ( Vec_IntSize(vPartSupp) < nPartSizeLimit )
+            if ( Vec_IntSize(vPartSupp) < nSuppSizeLimit )
                 continue;
         }
         else
@@ -318,23 +707,25 @@ void Abc_NtkPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll,
 
   Synopsis    [Perform the smart partitioning.]
 
-  Description []
+  Description [Returns the ptr-vector of int-vectors.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int nPartSizeLimit, int fVerbose )
+Vec_Ptr_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int nSuppSizeLimit, int fVerbose )
 {
+    ProgressBar * pProgress;
     Vec_Ptr_t * vPartSuppsChar;
-    Vec_Ptr_t * vSupps, * vPartsAll, * vPartsAll2, * vPartSuppsAll, * vPartPtr;
+    Vec_Ptr_t * vSupps, * vPartsAll, * vPartsAll2, * vPartSuppsAll;
     Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
     int i, iPart, iOut, clk, clk2, timeFind = 0;
 
     // compute the supports for all outputs
 clk = clock();
-    vSupps = Abc_NtkPartitionCollectSupps( pNtk );
+//    vSupps = Abc_NtkComputeSupportsNaive( pNtk );
+    vSupps = Abc_NtkComputeSupportsSmart( pNtk );
 if ( fVerbose )
 {
 PRT( "Supps", clock() - clk );
@@ -346,15 +737,19 @@ PRT( "Supps", clock() - clk );
 clk = clock();
     vPartsAll = Vec_PtrAlloc( 256 );
     vPartSuppsAll = Vec_PtrAlloc( 256 );
+    pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(vSupps) );
     Vec_PtrForEachEntry( vSupps, vOne, i )
     {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+//        if ( i % 1000 == 0 )
+//            printf( "CIs = %6d. COs = %6d. Processed = %6d (out of %6d). Parts = %6d.\r", 
+//                Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), i, Vec_PtrSize(vSupps), Vec_PtrSize(vPartsAll) ); 
         // get the output number
         iOut = Vec_IntPop(vOne);
         // find closely matching part
 clk2 = clock();
-        iPart = Abc_NtkPartitionSmartFindPart( vPartSuppsAll, vPartsAll, vPartSuppsChar, nPartSizeLimit, vOne );
+        iPart = Abc_NtkPartitionSmartFindPart( vPartSuppsAll, vPartsAll, vPartSuppsChar, nSuppSizeLimit, vOne );
 timeFind += clock() - clk2;
-//printf( "%4d->%4d  ", i, iPart );
         if ( iPart == -1 )
         {
             // create new partition
@@ -383,6 +778,7 @@ timeFind += clock() - clk2;
             Abc_NtkSuppCharAdd( Vec_PtrEntry(vPartSuppsChar, iPart), vOne, Abc_NtkCiNum(pNtk) );
         }
     }
+    Extra_ProgressBarStop( pProgress );
 
     // stop char-based support representation
     Vec_PtrForEachEntry( vPartSuppsChar, vTemp, i )
@@ -411,20 +807,20 @@ clk = clock();
 
     // compact small partitions
 //    Abc_NtkPartitionPrint( pNtk, vPartsAll, vPartSuppsAll );
-    Abc_NtkPartitionCompact( vPartsAll, vPartSuppsAll, nPartSizeLimit );
-    if ( fVerbose )
-//    Abc_NtkPartitionPrint( pNtk, vPartsAll, vPartSuppsAll );
-    printf( "Created %d partitions.\n", Vec_PtrSize(vPartsAll) );
+    Abc_NtkPartitionCompact( vPartsAll, vPartSuppsAll, nSuppSizeLimit );
 
 if ( fVerbose )
 {
 PRT( "Comps", clock() - clk );
 }
+    if ( fVerbose )
+    printf( "Created %d partitions.\n", Vec_PtrSize(vPartsAll) );
+//    Abc_NtkPartitionPrint( pNtk, vPartsAll, vPartSuppsAll );
 
     // cleanup
     Vec_VecFree( (Vec_Vec_t *)vSupps );
     Vec_VecFree( (Vec_Vec_t *)vPartSuppsAll );
-
+/*
     // converts from intergers to nodes
     Vec_PtrForEachEntry( vPartsAll, vPart, iPart )
     {
@@ -434,34 +830,54 @@ PRT( "Comps", clock() - clk );
         Vec_IntFree( vPart );
         Vec_PtrWriteEntry( vPartsAll, iPart, vPartPtr );
     }
-    return (Vec_Vec_t *)vPartsAll;
+*/
+    return vPartsAll;
 }
 
 /**Function*************************************************************
 
   Synopsis    [Perform the naive partitioning.]
 
-  Description []
+  Description [Returns the ptr-vector of int-vectors.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Vec_t * Abc_NtkPartitionNaive( Abc_Ntk_t * pNtk, int nPartSize )
+Vec_Ptr_t * Abc_NtkPartitionNaive( Abc_Ntk_t * pNtk, int nPartSize )
 {
-    Vec_Vec_t * vParts;
+    Vec_Ptr_t * vParts;
     Abc_Obj_t * pObj;
     int nParts, i;
     nParts = (Abc_NtkCoNum(pNtk) / nPartSize) + ((Abc_NtkCoNum(pNtk) % nPartSize) > 0);
-    vParts = Vec_VecStart( nParts );
+    vParts = (Vec_Ptr_t *)Vec_VecStart( nParts );
     Abc_NtkForEachCo( pNtk, pObj, i )
-        Vec_VecPush( vParts, i / nPartSize, pObj );
+        Vec_IntPush( Vec_PtrEntry(vParts, i / nPartSize), i );
     return vParts;
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Converts from intergers to pointers for the given network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkConvertCos( Abc_Ntk_t * pNtk, Vec_Int_t * vOuts, Vec_Ptr_t * vOutsPtr )
+{
+    int Out, i;
+    Vec_PtrClear( vOutsPtr );
+    Vec_IntForEachEntry( vOuts, Out, i )
+        Vec_PtrPush( vOutsPtr, Abc_NtkCo(pNtk, Out) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns representative of the given node.]
 
   Description []
@@ -506,134 +922,6 @@ static inline Abc_Obj_t * Abc_NtkPartStitchCopy1( Vec_Ptr_t * vEquiv, Abc_Obj_t
 
 /**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 []
@@ -762,6 +1050,20 @@ Abc_Ntk_t * Abc_NtkPartStitchChoices( Abc_Ntk_t * pNtk, Vec_Ptr_t * vParts )
         }
     }
 
+    // connect the remaining POs
+/*
+    Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew);
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->pCopy = Abc_NtkCi( pNtkNew, i );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        pObj->pCopy = Abc_NtkCo( pNtkNew, i );
+*/
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        if ( Abc_ObjFaninNum(pObj->pCopy) == 0 )
+            Abc_ObjAddFanin( pObj->pCopy, Abc_ObjChild0Copy(pObj) );
+    }
+
     // transform into the HOP manager
     pMan = Abc_NtkPartStartHop( pNtkNew );
     pNtkNew = Abc_NtkHopRemoveLoops( pNtkTemp = pNtkNew, pMan );
@@ -788,47 +1090,57 @@ Abc_Ntk_t * Abc_NtkPartStitchChoices( Abc_Ntk_t * pNtk, Vec_Ptr_t * vParts )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams )
+Abc_Ntk_t * Abc_NtkFraigPartitioned( Vec_Ptr_t * vStore, 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;
+    Vec_Ptr_t * vParts, * vFraigs, * vOnePtr;
+    Vec_Int_t * vOne;
+    Abc_Ntk_t * pNtk, * pNtk2, * pNtkAig, * pNtkFraig;
+    int i, k;
 
     // perform partitioning
+    pNtk = Vec_PtrEntry( vStore, 0 );
     assert( Abc_NtkIsStrash(pNtk) );
 //    vParts = Abc_NtkPartitionNaive( pNtk, 20 );
-    vParts = Abc_NtkPartitionSmart( pNtk, 0, 0 );
+    vParts = Abc_NtkPartitionSmart( pNtk, 300, 0 );
 
     Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
 
     // fraig each partition
-    vFraigs = Vec_PtrAlloc( Vec_VecSize(vParts) );
-    Vec_VecForEachLevel( vParts, vOne, i )
+    vOnePtr = Vec_PtrAlloc( 1000 );
+    vFraigs = Vec_PtrAlloc( Vec_PtrSize(vParts) );
+    Vec_PtrForEachEntry( vParts, vOne, i )
     {
-        pNtkAig = Abc_NtkCreateConeArray( pNtk, vOne, 0 );
-        pNtkFraig = Abc_NtkFraig( pNtkAig, pParams, 0, 0 );
+        // start the partition 
+        Abc_NtkConvertCos( pNtk, vOne, vOnePtr );
+        pNtkAig = Abc_NtkCreateConeArray( pNtk, vOnePtr, 0 );
+        // add nodes to the partition
+        Vec_PtrForEachEntryStart( vStore, pNtk2, k, 1 )
+        {
+            Abc_NtkConvertCos( pNtk2, vOne, vOnePtr );
+            Abc_NtkAppendToCone( pNtkAig, pNtk2, vOnePtr );
+        }
+        printf( "Fraiging part %4d  (out of %4d)  PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r", 
+            i+1, Vec_PtrSize(vParts), Abc_NtkPiNum(pNtkAig), Abc_NtkPoNum(pNtkAig), 
+            Abc_NtkNodeNum(pNtkAig), Abc_AigLevel(pNtkAig) );
+        // fraig the partition
+        pNtkFraig = Abc_NtkFraig( pNtkAig, pParams, 1, 0 );
         Vec_PtrPush( vFraigs, pNtkFraig );
         Abc_NtkDelete( pNtkAig );
-
-        printf( "Finished part %d (out of %d)\r", i+1, Vec_VecSize(vParts) );
     }
-    Vec_VecFree( vParts );
+    printf( "                                                                                          \r" );
+    Vec_VecFree( (Vec_Vec_t *)vParts );
 
     Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
 
     // derive the final network
     pNtkFraig = Abc_NtkPartStitchChoices( pNtk, vFraigs );
     Vec_PtrForEachEntry( vFraigs, pNtkAig, i )
-    {
-//        Abc_NtkPrintStats( stdout, pNtkAig, 0 );
         Abc_NtkDelete( pNtkAig );
-    }
     Vec_PtrFree( vFraigs );
-
+    Vec_PtrFree( vOnePtr );
     return pNtkFraig;
 }
 
@@ -848,8 +1160,8 @@ void Abc_NtkFraigPartitionedTime( 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;
+    Vec_Ptr_t * vParts, * vFraigs, * vOnePtr;
+    Vec_Int_t * vOne;
     Abc_Ntk_t * pNtkAig, * pNtkFraig;
     int i;
     int clk = clock();
@@ -857,22 +1169,24 @@ void Abc_NtkFraigPartitionedTime( Abc_Ntk_t * pNtk, void * pParams )
     // perform partitioning
     assert( Abc_NtkIsStrash(pNtk) );
 //    vParts = Abc_NtkPartitionNaive( pNtk, 20 );
-    vParts = Abc_NtkPartitionSmart( pNtk, 0, 0 );
+    vParts = Abc_NtkPartitionSmart( pNtk, 300, 0 );
 
     Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
 
     // fraig each partition
-    vFraigs = Vec_PtrAlloc( Vec_VecSize(vParts) );
-    Vec_VecForEachLevel( vParts, vOne, i )
+    vOnePtr = Vec_PtrAlloc( 1000 );
+    vFraigs = Vec_PtrAlloc( Vec_PtrSize(vParts) );
+    Vec_PtrForEachEntry( vParts, vOne, i )
     {
-        pNtkAig = Abc_NtkCreateConeArray( pNtk, vOne, 0 );
+        Abc_NtkConvertCos( pNtk, vOne, vOnePtr );
+        pNtkAig = Abc_NtkCreateConeArray( pNtk, vOnePtr, 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) );
+        printf( "Finished part %5d (out of %5d)\r", i+1, Vec_PtrSize(vParts) );
     }
-    Vec_VecFree( vParts );
+    Vec_VecFree( (Vec_Vec_t *)vParts );
 
     Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
 
@@ -880,7 +1194,7 @@ void Abc_NtkFraigPartitionedTime( Abc_Ntk_t * pNtk, void * pParams )
     Vec_PtrForEachEntry( vFraigs, pNtkAig, i )
         Abc_NtkDelete( pNtkAig );
     Vec_PtrFree( vFraigs );
-
+    Vec_PtrFree( vOnePtr );
     PRT( "Partitioned fraiging time", clock() - clk );
 }
 
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 67ecaae0..9c9bbcfd 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -293,7 +293,7 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in
         }
         else
         {
-            printf( "Finished part %d (out of %d)\r", i+1, Abc_NtkPoNum(pMiter) );
+            printf( "Finished part %5d (out of %5d)\r", i+1, Abc_NtkPoNum(pMiter) );
             nOutputs += nPartSize;
         }
 //        if ( pMiter->pModel )
@@ -301,7 +301,7 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in
         if ( pMiterPart )
             Abc_NtkDelete( pMiterPart );
     }
-
+  
     Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
 
     if ( Status == 1 )
@@ -325,12 +325,13 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in
 void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose )
 {
     extern int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd );
-    extern Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int nPartSizeLimit, int fVerbose );
+    extern Vec_Ptr_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int nPartSizeLimit, int fVerbose );
+    extern void Abc_NtkConvertCos( Abc_Ntk_t * pNtk, Vec_Int_t * vOuts, Vec_Ptr_t * vOnePtr );
     extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
     extern void * Abc_FrameGetGlobalFrame();
 
-    Vec_Vec_t * vParts;
-    Vec_Ptr_t * vOne;
+    Vec_Ptr_t * vParts, * vOnePtr;
+    Vec_Int_t * vOne;
     Prove_Params_t Params, * pParams = &Params;
     Abc_Ntk_t * pMiter, * pMiterPart;
     int i, RetValue, Status, nOutputs;
@@ -368,15 +369,17 @@ void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds
     Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
 
     // partition the outputs
-    vParts = Abc_NtkPartitionSmart( pMiter, 50, 1 );
+    vParts = Abc_NtkPartitionSmart( pMiter, 300, 0 );
 
     // fraig each partition
     Status = 1;
     nOutputs = 0;
-    Vec_VecForEachLevel( vParts, vOne, i )
+    vOnePtr = Vec_PtrAlloc( 1000 );
+    Vec_PtrForEachEntry( vParts, vOne, i )
     {
         // get this part of the miter
-        pMiterPart = Abc_NtkCreateConeArray( pMiter, vOne, 0 );
+        Abc_NtkConvertCos( pMiter, vOne, vOnePtr );
+        pMiterPart = Abc_NtkCreateConeArray( pMiter, vOnePtr, 0 );
         Abc_NtkCombinePos( pMiterPart, 0 );
         // check the miter for being constant
         RetValue = Abc_NtkMiterIsConstant( pMiterPart );
@@ -391,6 +394,9 @@ void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds
             Abc_NtkDelete( pMiterPart );
             continue;
         }
+        printf( "Verifying part %4d  (out of %4d)  PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r", 
+            i+1, Vec_PtrSize(vParts), Abc_NtkPiNum(pMiterPart), Abc_NtkPoNum(pMiterPart), 
+            Abc_NtkNodeNum(pMiterPart), Abc_AigLevel(pMiterPart) );
         // solve the problem
         RetValue = Abc_NtkIvyProve( &pMiterPart, pParams );
         if ( RetValue == -1 )
@@ -412,12 +418,14 @@ void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds
         }
         else
         {
-            printf( "Finished part %d (out of %d)\r", i+1, Vec_VecSize(vParts) );
-            nOutputs += Vec_PtrSize(vOne);
+//            printf( "Finished part %5d (out of %5d)\r", i+1, Vec_PtrSize(vParts) );
+            nOutputs += Vec_IntSize(vOne);
         }
         Abc_NtkDelete( pMiterPart );
     }
-    Vec_VecFree( vParts );
+    printf( "                                                                                          \r" );
+    Vec_VecFree( (Vec_Vec_t *)vParts );
+    Vec_PtrFree( vOnePtr );
 
     Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );