Version abc71001

1 files changed, 762 insertions, 0 deletions

diff --git a/src/base/abci/abcReconv.c b/src/base/abci/abcReconv.c
new file mode 100644
index 00000000..e77f055a
--- /dev/null
+++ b/src/base/abci/abcReconv.c
@@ -0,0 +1,762 @@
+/**CFile****************************************************************
+
+  FileName    [abcReconv.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Computation of reconvergence-driven cuts.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcReconv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct Abc_ManCut_t_
+{
+    // user specified parameters
+    int              nNodeSizeMax;  // the limit on the size of the supernode
+    int              nConeSizeMax;  // the limit on the size of the containing cone
+    int              nNodeFanStop;  // the limit on the size of the supernode
+    int              nConeFanStop;  // the limit on the size of the containing cone
+    // internal parameters
+    Vec_Ptr_t *      vNodeLeaves;   // fanins of the collapsed node (the cut)
+    Vec_Ptr_t *      vConeLeaves;   // fanins of the containing cone
+    Vec_Ptr_t *      vVisited;      // the visited nodes
+    Vec_Vec_t *      vLevels;       // the data structure to compute TFO nodes
+    Vec_Ptr_t *      vNodesTfo;     // the nodes in the TFO of the cut
+};
+
+static int   Abc_NodeBuildCutLevelOne_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nSizeLimit, int nFaninLimit );
+static int   Abc_NodeBuildCutLevelTwo_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nFaninLimit );
+static void  Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Unmarks the TFI cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Abc_NodesMark( Vec_Ptr_t * vVisited )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    Vec_PtrForEachEntry( vVisited, pNode, i )
+        pNode->fMarkA = 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Unmarks the TFI cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Abc_NodesUnmark( Vec_Ptr_t * vVisited )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    Vec_PtrForEachEntry( vVisited, pNode, i )
+        pNode->fMarkA = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Unmarks the TFI cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Abc_NodesUnmarkB( Vec_Ptr_t * vVisited )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    Vec_PtrForEachEntry( vVisited, pNode, i )
+        pNode->fMarkB = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluate the cost of removing the node from the set of leaves.]
+
+  Description [Returns the number of new leaves that will be brought in.
+  Returns large number if the node cannot be removed from the set of leaves.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_NodeGetLeafCostOne( Abc_Obj_t * pNode, int nFaninLimit )
+{
+    int Cost;
+    // make sure the node is in the construction zone
+    assert( pNode->fMarkB == 1 );  
+    // cannot expand over the PI node
+    if ( Abc_ObjIsCi(pNode) )
+        return 999;
+    // get the cost of the cone
+    Cost = (!Abc_ObjFanin0(pNode)->fMarkB) + (!Abc_ObjFanin1(pNode)->fMarkB);
+    // always accept if the number of leaves does not increase
+    if ( Cost < 2 )
+        return Cost;
+    // skip nodes with many fanouts
+    if ( Abc_ObjFanoutNum(pNode) > nFaninLimit )
+        return 999;
+    // return the number of nodes that will be on the leaves if this node is removed
+    return Cost;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluate the cost of removing the node from the set of leaves.]
+
+  Description [Returns the number of new leaves that will be brought in.
+  Returns large number if the node cannot be removed from the set of leaves.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_NodeGetLeafCostTwo( Abc_Obj_t * pNode, int nFaninLimit, 
+    Abc_Obj_t ** ppLeafToAdd, Abc_Obj_t ** pNodeToMark1, Abc_Obj_t ** pNodeToMark2 )
+{
+    Abc_Obj_t * pFanin0, * pFanin1, * pTemp;
+    Abc_Obj_t * pGrand, * pGrandToAdd;
+    // make sure the node is in the construction zone
+    assert( pNode->fMarkB == 1 );  
+    // cannot expand over the PI node
+    if ( Abc_ObjIsCi(pNode) )
+        return 999;
+    // skip nodes with many fanouts
+//    if ( Abc_ObjFanoutNum(pNode) > nFaninLimit )
+//        return 999;
+    // get the children
+    pFanin0 = Abc_ObjFanin0(pNode);
+    pFanin1 = Abc_ObjFanin1(pNode);
+    assert( !pFanin0->fMarkB && !pFanin1->fMarkB );
+    // count the number of unique grandchildren that will be included
+    // return infinite cost if this number if more than 1
+    if ( Abc_ObjIsCi(pFanin0) && Abc_ObjIsCi(pFanin1) )
+        return 999;
+    // consider the special case when a non-CI fanin can be dropped
+    if ( !Abc_ObjIsCi(pFanin0) && Abc_ObjFanin0(pFanin0)->fMarkB && Abc_ObjFanin1(pFanin0)->fMarkB )
+    {
+        *ppLeafToAdd  = pFanin1;
+        *pNodeToMark1 = pFanin0;
+        *pNodeToMark2 = NULL;
+        return 1;
+    }
+    if ( !Abc_ObjIsCi(pFanin1) && Abc_ObjFanin0(pFanin1)->fMarkB && Abc_ObjFanin1(pFanin1)->fMarkB )
+    {
+        *ppLeafToAdd  = pFanin0;
+        *pNodeToMark1 = pFanin1;
+        *pNodeToMark2 = NULL;
+        return 1;
+    }
+
+    // make the first node CI if any
+    if ( Abc_ObjIsCi(pFanin1) )
+        pTemp = pFanin0, pFanin0 = pFanin1, pFanin1 = pTemp;
+    // consider the first node
+    pGrandToAdd = NULL;
+    if ( Abc_ObjIsCi(pFanin0) )
+    {
+        *pNodeToMark1 = NULL;
+        pGrandToAdd = pFanin0;
+    }
+    else
+    {
+        *pNodeToMark1 = pFanin0;
+        pGrand = Abc_ObjFanin0(pFanin0);
+        if ( !pGrand->fMarkB )
+        {
+            if ( pGrandToAdd && pGrandToAdd != pGrand )
+                return 999;
+            pGrandToAdd = pGrand;
+        }
+        pGrand = Abc_ObjFanin1(pFanin0);
+        if ( !pGrand->fMarkB )
+        {
+            if ( pGrandToAdd && pGrandToAdd != pGrand )
+                return 999;
+            pGrandToAdd = pGrand;
+        }
+    }
+    // consider the second node
+    *pNodeToMark2 = pFanin1;
+    pGrand = Abc_ObjFanin0(pFanin1);
+    if ( !pGrand->fMarkB )
+    {
+        if ( pGrandToAdd && pGrandToAdd != pGrand )
+            return 999;
+        pGrandToAdd = pGrand;
+    }
+    pGrand = Abc_ObjFanin1(pFanin1);
+    if ( !pGrand->fMarkB )
+    {
+        if ( pGrandToAdd && pGrandToAdd != pGrand )
+            return 999;
+        pGrandToAdd = pGrand;
+    }
+    assert( pGrandToAdd != NULL );
+    *ppLeafToAdd = pGrandToAdd;
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Finds a fanin-limited, reconvergence-driven cut for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot, bool fContain )
+{
+    Abc_Obj_t * pNode;
+    int i;
+
+    assert( !Abc_ObjIsComplement(pRoot) );
+    assert( Abc_ObjIsNode(pRoot) );
+
+    // start the visited nodes and mark them
+    Vec_PtrClear( p->vVisited );
+    Vec_PtrPush( p->vVisited, pRoot );
+    Vec_PtrPush( p->vVisited, Abc_ObjFanin0(pRoot) );
+    Vec_PtrPush( p->vVisited, Abc_ObjFanin1(pRoot) );
+    pRoot->fMarkB = 1;
+    Abc_ObjFanin0(pRoot)->fMarkB = 1;
+    Abc_ObjFanin1(pRoot)->fMarkB = 1;
+
+    // start the cut 
+    Vec_PtrClear( p->vNodeLeaves );
+    Vec_PtrPush( p->vNodeLeaves, Abc_ObjFanin0(pRoot) );
+    Vec_PtrPush( p->vNodeLeaves, Abc_ObjFanin1(pRoot) );
+
+    // compute the cut
+    while ( Abc_NodeBuildCutLevelOne_int( p->vVisited, p->vNodeLeaves, p->nNodeSizeMax, p->nNodeFanStop ) );
+    assert( Vec_PtrSize(p->vNodeLeaves) <= p->nNodeSizeMax );
+
+    // return if containing cut is not requested
+    if ( !fContain )
+    {
+        // unmark both fMarkA and fMarkB in tbe TFI
+        Abc_NodesUnmarkB( p->vVisited );
+        return p->vNodeLeaves;
+    }
+
+//printf( "\n\n\n" );
+    // compute the containing cut
+    assert( p->nNodeSizeMax < p->nConeSizeMax );
+    // copy the current boundary
+    Vec_PtrClear( p->vConeLeaves );
+    Vec_PtrForEachEntry( p->vNodeLeaves, pNode, i )
+        Vec_PtrPush( p->vConeLeaves, pNode );
+    // compute the containing cut
+    while ( Abc_NodeBuildCutLevelOne_int( p->vVisited, p->vConeLeaves, p->nConeSizeMax, p->nConeFanStop ) );
+    assert( Vec_PtrSize(p->vConeLeaves) <= p->nConeSizeMax );
+    // unmark TFI using fMarkA and fMarkB
+    Abc_NodesUnmarkB( p->vVisited );
+    return p->vNodeLeaves;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Builds reconvergence-driven cut by changing one leaf at a time.]
+
+  Description [This procedure looks at the current leaves and tries to change 
+  one leaf at a time in such a way that the cut grows as little as possible.
+  In evaluating the fanins, this procedure looks only at their immediate 
+  predecessors (this is why it is called a one-level construction procedure).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeBuildCutLevelOne_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nSizeLimit, int nFaninLimit )
+{
+    Abc_Obj_t * pNode, * pFaninBest, * pNext;
+    int CostBest, CostCur, i;
+    // find the best fanin
+    CostBest   = 100;
+    pFaninBest = NULL;
+//printf( "Evaluating fanins of the cut:\n" );
+    Vec_PtrForEachEntry( vLeaves, pNode, i )
+    {
+        CostCur = Abc_NodeGetLeafCostOne( pNode, nFaninLimit );
+//printf( "    Fanin %s has cost %d.\n", Abc_ObjName(pNode), CostCur );
+//        if ( CostBest > CostCur ) // performance improvement: expand the variable with the smallest level
+        if ( CostBest > CostCur ||
+             (CostBest == CostCur && pNode->Level > pFaninBest->Level) )
+        {
+            CostBest   = CostCur;
+            pFaninBest = pNode;
+        }
+        if ( CostBest == 0 )
+            break;
+    }
+    if ( pFaninBest == NULL )
+        return 0;
+//        return Abc_NodeBuildCutLevelTwo_int( vVisited, vLeaves, nFaninLimit );
+
+    assert( CostBest < 3 );
+    if ( vLeaves->nSize - 1 + CostBest > nSizeLimit )
+        return 0;
+//        return Abc_NodeBuildCutLevelTwo_int( vVisited, vLeaves, nFaninLimit );
+
+    assert( Abc_ObjIsNode(pFaninBest) );
+    // remove the node from the array
+    Vec_PtrRemove( vLeaves, pFaninBest );
+//printf( "Removing fanin %s.\n", Abc_ObjName(pFaninBest) );
+
+    // add the left child to the fanins
+    pNext = Abc_ObjFanin0(pFaninBest);
+    if ( !pNext->fMarkB )
+    {
+//printf( "Adding fanin %s.\n", Abc_ObjName(pNext) );
+        pNext->fMarkB = 1;
+        Vec_PtrPush( vLeaves, pNext );
+        Vec_PtrPush( vVisited, pNext );
+    }
+    // add the right child to the fanins
+    pNext = Abc_ObjFanin1(pFaninBest);
+    if ( !pNext->fMarkB )
+    {
+//printf( "Adding fanin %s.\n", Abc_ObjName(pNext) );
+        pNext->fMarkB = 1;
+        Vec_PtrPush( vLeaves, pNext );
+        Vec_PtrPush( vVisited, pNext );
+    }
+    assert( vLeaves->nSize <= nSizeLimit );
+    // keep doing this
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Builds reconvergence-driven cut by changing one leaf at a time.]
+
+  Description [This procedure looks at the current leaves and tries to change 
+  one leaf at a time in such a way that the cut grows as little as possible.
+  In evaluating the fanins, this procedure looks across two levels of fanins
+  (this is why it is called a two-level construction procedure).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeBuildCutLevelTwo_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nFaninLimit )
+{
+    Abc_Obj_t * pNode, * pLeafToAdd, * pNodeToMark1, * pNodeToMark2;
+    int CostCur, i;
+    // find the best fanin
+    Vec_PtrForEachEntry( vLeaves, pNode, i )
+    {
+        CostCur = Abc_NodeGetLeafCostTwo( pNode, nFaninLimit, &pLeafToAdd, &pNodeToMark1, &pNodeToMark2 );
+        if ( CostCur < 2 )
+            break;
+    }
+    if ( CostCur > 2 )
+        return 0;
+    // remove the node from the array
+    Vec_PtrRemove( vLeaves, pNode );
+    // add the node to the leaves
+    if ( pLeafToAdd )
+    {
+        assert( !pLeafToAdd->fMarkB );
+        pLeafToAdd->fMarkB = 1;
+        Vec_PtrPush( vLeaves, pLeafToAdd );
+        Vec_PtrPush( vVisited, pLeafToAdd );
+    }
+    // mark the other nodes
+    if ( pNodeToMark1 )
+    {
+        assert( !pNodeToMark1->fMarkB );
+        pNodeToMark1->fMarkB = 1;
+        Vec_PtrPush( vVisited, pNodeToMark1 );
+    }
+    if ( pNodeToMark2 )
+    {
+        assert( !pNodeToMark2->fMarkB );
+        pNodeToMark2->fMarkB = 1;
+        Vec_PtrPush( vVisited, pNodeToMark2 );
+    }
+    // keep doing this
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Get the nodes contained in the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeConeCollect( Abc_Obj_t ** ppRoots, int nRoots, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited, int fIncludeFanins )
+{
+    Abc_Obj_t * pTemp;
+    int i;
+    // mark the fanins of the cone
+    Abc_NodesMark( vLeaves );
+    // collect the nodes in the DFS order
+    Vec_PtrClear( vVisited );
+    // add the fanins
+    if ( fIncludeFanins )
+        Vec_PtrForEachEntry( vLeaves, pTemp, i )
+            Vec_PtrPush( vVisited, pTemp );
+    // add other nodes
+    for ( i = 0; i < nRoots; i++ )
+        Abc_NodeConeMarkCollect_rec( ppRoots[i], vVisited );
+    // unmark both sets
+    Abc_NodesUnmark( vLeaves );
+    Abc_NodesUnmark( vVisited );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFI cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited )
+{
+    if ( pNode->fMarkA == 1 )
+        return;
+    // visit transitive fanin 
+    if ( Abc_ObjIsNode(pNode) )
+    {
+        Abc_NodeConeMarkCollect_rec( Abc_ObjFanin0(pNode), vVisited );
+        Abc_NodeConeMarkCollect_rec( Abc_ObjFanin1(pNode), vVisited );
+    }
+    assert( pNode->fMarkA == 0 );
+    pNode->fMarkA = 1;
+    Vec_PtrPush( vVisited, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns BDD representing the logic function of the cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited )
+{
+    Abc_Obj_t * pNode;
+    DdNode * bFunc0, * bFunc1, * bFunc;
+    int i;
+    // get the nodes in the cut without fanins in the DFS order
+    Abc_NodeConeCollect( &pRoot, 1, vLeaves, vVisited, 0 );
+    // set the elementary BDDs
+    Vec_PtrForEachEntry( vLeaves, pNode, i )
+        pNode->pCopy = (Abc_Obj_t *)pbVars[i];
+    // compute the BDDs for the collected nodes
+    Vec_PtrForEachEntry( vVisited, pNode, i )
+    {
+        assert( !Abc_ObjIsPi(pNode) );
+        bFunc0 = Cudd_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
+        bFunc1 = Cudd_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) );
+        bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );    Cudd_Ref( bFunc );
+        pNode->pCopy = (Abc_Obj_t *)bFunc;
+    }
+    Cudd_Ref( bFunc );
+    // dereference the intermediate ones
+    Vec_PtrForEachEntry( vVisited, pNode, i )
+        Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy );
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns BDD representing the transition relation of the cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, Vec_Ptr_t * vVisited )
+{
+    DdNode * bFunc0, * bFunc1, * bFunc, * bTrans, * bTemp, * bCube, * bResult;
+    Abc_Obj_t * pNode;
+    int i;
+    // get the nodes in the cut without fanins in the DFS order
+    Abc_NodeConeCollect( (Abc_Obj_t **)vRoots->pArray, vRoots->nSize, vLeaves, vVisited, 0 );
+    // set the elementary BDDs
+    Vec_PtrForEachEntry( vLeaves, pNode, i )
+        pNode->pCopy = (Abc_Obj_t *)pbVarsX[i];
+    // compute the BDDs for the collected nodes
+    Vec_PtrForEachEntry( vVisited, pNode, i )
+    {
+        bFunc0 = Cudd_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
+        bFunc1 = Cudd_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) );
+        bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );    Cudd_Ref( bFunc );
+        pNode->pCopy = (Abc_Obj_t *)bFunc;
+    }
+    // compute the transition relation of the cone
+    bTrans = b1;    Cudd_Ref( bTrans );
+    Vec_PtrForEachEntry( vRoots, pNode, i )
+    {
+        bFunc = Cudd_bddXnor( dd, (DdNode *)pNode->pCopy, pbVarsY[i] );  Cudd_Ref( bFunc );
+        bTrans = Cudd_bddAnd( dd, bTemp = bTrans, bFunc );               Cudd_Ref( bTrans );
+        Cudd_RecursiveDeref( dd, bTemp );
+        Cudd_RecursiveDeref( dd, bFunc );
+    }
+    // dereference the intermediate ones
+    Vec_PtrForEachEntry( vVisited, pNode, i )
+        Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy );
+    // compute don't-cares
+    bCube = Extra_bddComputeRangeCube( dd, vRoots->nSize, vRoots->nSize + vLeaves->nSize );  Cudd_Ref( bCube );
+    bResult = Cudd_bddExistAbstract( dd, bTrans, bCube );                Cudd_Ref( bResult );
+    bResult = Cudd_Not( bResult );
+    Cudd_RecursiveDeref( dd, bCube );
+    Cudd_RecursiveDeref( dd, bTrans );
+    Cudd_Deref( bResult );
+    return bResult;
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Starts the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop )
+{
+    Abc_ManCut_t * p;
+    p = ALLOC( Abc_ManCut_t, 1 );
+    memset( p, 0, sizeof(Abc_ManCut_t) );
+    p->vNodeLeaves  = Vec_PtrAlloc( 100 );
+    p->vConeLeaves  = Vec_PtrAlloc( 100 );
+    p->vVisited     = Vec_PtrAlloc( 100 );
+    p->vLevels      = Vec_VecAlloc( 100 );
+    p->vNodesTfo    = Vec_PtrAlloc( 100 );
+    p->nNodeSizeMax = nNodeSizeMax;
+    p->nConeSizeMax = nConeSizeMax;
+    p->nNodeFanStop = nNodeFanStop;
+    p->nConeFanStop = nConeFanStop;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkManCutStop( Abc_ManCut_t * p )
+{
+    Vec_PtrFree( p->vNodeLeaves );
+    Vec_PtrFree( p->vConeLeaves );
+    Vec_PtrFree( p->vVisited    );
+    Vec_VecFree( p->vLevels );
+    Vec_PtrFree( p->vNodesTfo );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the leaves of the cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p )
+{
+    return p->vConeLeaves;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the leaves of the cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkManCutReadCutSmall( Abc_ManCut_t * p )
+{
+    return p->vNodeLeaves;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the leaves of the cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkManCutReadVisited( Abc_ManCut_t * p )
+{
+    return p->vVisited;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the TFO of the cut in the topological order.]
+
+  Description [TFO of the cut is defined as a set of nodes, for which the cut
+  is a cut, that is, every path from the collected nodes to the CIs goes through 
+  a node in the cut. The nodes are collected if their level does not exceed
+  the given number (LevelMax). The nodes are returned in the topological order.
+  If the root node is given, its MFFC is marked, so that the collected nodes
+  do not contain any nodes in the MFFC.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int LevelMax )
+{
+    Abc_Ntk_t * pNtk = pRoot->pNtk;
+    Vec_Ptr_t * vVec;
+    Abc_Obj_t * pNode, * pFanout;
+    int i, k, v, LevelMin;
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    // assuming that the structure is clean
+    Vec_VecForEachLevel( p->vLevels, vVec, i )
+        assert( vVec->nSize == 0 );
+
+    // put fanins into the structure while labeling them
+    Abc_NtkIncrementTravId( pNtk );
+    LevelMin = -1;
+    Vec_PtrForEachEntry( vLeaves, pNode, i )
+    {
+        if ( pNode->Level > (unsigned)LevelMax )
+            continue;
+        Abc_NodeSetTravIdCurrent( pNode );
+        Vec_VecPush( p->vLevels, pNode->Level, pNode );
+        if ( LevelMin < (int)pNode->Level )
+            LevelMin = pNode->Level;
+    }
+    assert( LevelMin >= 0 );
+
+    // mark MFFC 
+    if ( pRoot )
+        Abc_NodeMffcLabelAig( pRoot );
+
+    // go through the levels up
+    Vec_PtrClear( p->vNodesTfo );
+    Vec_VecForEachEntryStart( p->vLevels, pNode, i, k, LevelMin )
+    {
+        if ( i > LevelMax )
+            break;
+        // if the node is not marked, it is not a fanin
+        if ( !Abc_NodeIsTravIdCurrent(pNode) )
+        {
+            // check if it belongs to the TFO
+            if ( !Abc_NodeIsTravIdCurrent(Abc_ObjFanin0(pNode)) || 
+                 !Abc_NodeIsTravIdCurrent(Abc_ObjFanin1(pNode)) )
+                 continue;
+            // save the node in the TFO and label it
+            Vec_PtrPush( p->vNodesTfo, pNode );
+            Abc_NodeSetTravIdCurrent( pNode );
+        }
+        // go through the fanouts and add them to the structure if they meet the conditions
+        Abc_ObjForEachFanout( pNode, pFanout, v )
+        {
+            // skip if fanout is a CO or its level exceeds
+            if ( Abc_ObjIsCo(pFanout) || pFanout->Level > (unsigned)LevelMax )
+                continue;
+            // skip if it is already added or if it is in MFFC
+            if ( Abc_NodeIsTravIdCurrent(pFanout) )
+                continue;
+            // add it to the structure but do not mark it (until tested later)
+            Vec_VecPushUnique( p->vLevels, pFanout->Level, pFanout );
+        }
+    }
+
+    // clear the levelized structure
+    Vec_VecForEachLevelStart( p->vLevels, vVec, i, LevelMin )
+    {
+        if ( i > LevelMax )
+            break;
+        Vec_PtrClear( vVec );
+    }
+    return p->vNodesTfo;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+