Version abc71001

1 files changed, 726 insertions, 0 deletions

diff --git a/src/base/abci/abcHaig.c b/src/base/abci/abcHaig.c
new file mode 100644
index 00000000..d3513bbe
--- /dev/null
+++ b/src/base/abci/abcHaig.c
@@ -0,0 +1,726 @@
+/**CFile****************************************************************
+
+  FileName    [abcHaig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Implements history AIG for combinational rewriting.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcHaig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Start history AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkHaigStart( Abc_Ntk_t * pNtk )
+{
+    Hop_Man_t * p;
+    Abc_Obj_t * pObj, * pTemp;
+    int i;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // check if the package is already started
+    if ( pNtk->pHaig )
+    {
+        Abc_NtkHaigStop( pNtk );
+        assert( pNtk->pHaig == NULL );
+        printf( "Warning: Previous history AIG was removed.\n" );
+    }
+    // make sure the data is clean
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        assert( pObj->pEquiv == NULL );
+    // start the HOP package
+    p = Hop_ManStart();
+    p->vObjs = Vec_PtrAlloc( 4096 );
+    Vec_PtrPush( p->vObjs, Hop_ManConst1(p) );
+    // map the constant node
+    Abc_AigConst1(pNtk)->pEquiv = Hop_ManConst1(p);
+    // map the CIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->pEquiv = Hop_ObjCreatePi(p);
+    // map the internal nodes
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        pObj->pEquiv = Hop_And( p, Abc_ObjChild0Equiv(pObj), Abc_ObjChild1Equiv(pObj) );
+    // map the choice nodes
+    if ( Abc_NtkGetChoiceNum( pNtk ) )
+    {
+        // print warning about choice nodes
+        printf( "Warning: The choice nodes in the original AIG are converted into HAIG.\n" );
+        Abc_NtkForEachNode( pNtk, pObj, i )
+        {
+            if ( !Abc_AigNodeIsChoice( pObj ) )
+                continue;
+            for ( pTemp = pObj->pData; pTemp; pTemp = pTemp->pData )
+                Hop_ObjCreateChoice( pObj->pEquiv, pTemp->pEquiv );
+        }
+    }
+    // make sure everything is okay
+    if ( !Hop_ManCheck(p) )
+    {
+        printf( "Abc_NtkHaigStart: Check for History AIG has failed.\n" );
+        Hop_ManStop(p);
+        return 0;
+    }
+    pNtk->pHaig = p;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops history AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkHaigStop( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    assert( Abc_NtkIsStrash(pNtk) );
+    if ( pNtk->pHaig == NULL )
+    {
+        printf( "Warning: History AIG is not allocated.\n" );
+        return 1;
+    }
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->pEquiv = NULL;
+    Hop_ManStop( pNtk->pHaig );
+    pNtk->pHaig = NULL;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers the HAIG to the new network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkHaigTranfer( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    if ( pNtkOld->pHaig == NULL )
+        return;
+    // transfer the package
+    assert( pNtkNew->pHaig == NULL );
+    pNtkNew->pHaig = pNtkOld->pHaig;
+    pNtkOld->pHaig = NULL;
+    // transfer constant pointer
+    Abc_AigConst1(pNtkOld)->pCopy->pEquiv = Abc_AigConst1(pNtkOld)->pEquiv;
+    // transfer the CI pointers
+    Abc_NtkForEachCi( pNtkOld, pObj, i )
+        pObj->pCopy->pEquiv = pObj->pEquiv;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the nodes in the classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkHaigCollectMembers( Hop_Man_t * p )
+{
+    Vec_Ptr_t * vObjs;
+    Hop_Obj_t * pObj;
+    int i;
+    vObjs = Vec_PtrAlloc( 4098 );
+    Vec_PtrForEachEntry( p->vObjs, pObj, i )
+    {
+        if ( pObj->pData == NULL )
+            continue;
+        pObj->pData = Hop_ObjRepr( pObj );
+        Vec_PtrPush( vObjs, pObj );
+    }
+    return vObjs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkHaigCreateClasses( Vec_Ptr_t * vMembers )
+{
+    Vec_Ptr_t * vClasses;
+    Hop_Obj_t * pObj, * pRepr;
+    int i;
+
+    // count classes
+    vClasses = Vec_PtrAlloc( 4098 );
+    Vec_PtrForEachEntry( vMembers, pObj, i )
+    {
+        pRepr = pObj->pData;
+        assert( pRepr->pData == NULL );
+        if ( pRepr->fMarkA == 0 ) // new
+        {
+            pRepr->fMarkA = 1;
+            Vec_PtrPush( vClasses, pRepr );
+        }
+    }
+
+    // set representatives as representatives
+    Vec_PtrForEachEntry( vClasses, pObj, i )
+    {
+        pObj->fMarkA = 0;
+        pObj->pData = pObj;
+    }
+
+    // go through the members and update
+    Vec_PtrForEachEntry( vMembers, pObj, i )
+    {
+        pRepr = pObj->pData;
+        if ( ((Hop_Obj_t *)pRepr->pData)->Id > pObj->Id )
+            pRepr->pData = pObj;
+    }
+
+    // change representatives of the class
+    Vec_PtrForEachEntry( vMembers, pObj, i )
+    {
+        pRepr = pObj->pData;
+        pObj->pData = pRepr->pData;
+        assert( ((Hop_Obj_t *)pObj->pData)->Id <= pObj->Id );
+    }
+
+    // update classes
+    Vec_PtrForEachEntry( vClasses, pObj, i )
+    {
+        pRepr = pObj->pData;
+        assert( pRepr->pData == pRepr );
+//        pRepr->pData = NULL;
+        Vec_PtrWriteEntry( vClasses, i, pRepr );
+        Vec_PtrPush( vMembers, pObj );
+    }
+
+    Vec_PtrForEachEntry( vMembers, pObj, i )
+        if ( pObj->pData == pObj )
+            pObj->pData = NULL;
+
+/*
+    Vec_PtrForEachEntry( vMembers, pObj, i )
+    {
+        printf( "ObjId = %4d : ", pObj->Id );
+        if ( pObj->pData == NULL )
+        {
+            printf( "NULL" );
+        }
+        else
+        {
+            printf( "%4d", ((Hop_Obj_t *)pObj->pData)->Id );
+            assert( ((Hop_Obj_t *)pObj->pData)->Id <= pObj->Id );
+        }
+        printf( "\n" );
+    }
+*/
+    return vClasses;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts how many data members have non-trivial fanout.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkHaigCountFans( Hop_Man_t * p )
+{
+    Hop_Obj_t * pObj;
+    int i, Counter = 0;
+    Vec_PtrForEachEntry( p->vObjs, pObj, i )
+    {
+        if ( pObj->pData == NULL )
+            continue;
+        if ( Hop_ObjRefs(pObj) > 0 )
+            Counter++;
+    }
+    printf( "The number of class members with fanouts = %5d.\n", Counter );
+    return Counter;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Hop_Obj_t * Hop_ObjReprHop( Hop_Obj_t * pObj )
+{
+    Hop_Obj_t * pRepr;
+    assert( pObj->pNext != NULL );
+    if ( pObj->pData == NULL )
+        return pObj->pNext;
+    pRepr = pObj->pData;
+    assert( pRepr->pData == pRepr );
+    return Hop_NotCond( pRepr->pNext, pObj->fPhase ^ pRepr->fPhase );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Hop_Obj_t * Hop_ObjChild0Hop( Hop_Obj_t * pObj ) { return Hop_NotCond( Hop_ObjReprHop(Hop_ObjFanin0(pObj)), Hop_ObjFaninC0(pObj) ); }
+static inline Hop_Obj_t * Hop_ObjChild1Hop( Hop_Obj_t * pObj ) { return Hop_NotCond( Hop_ObjReprHop(Hop_ObjFanin1(pObj)), Hop_ObjFaninC1(pObj) ); }
+
+/**Function*************************************************************
+
+  Synopsis    [Stops history AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Man_t * Abc_NtkHaigReconstruct( Hop_Man_t * p )
+{ 
+    Hop_Man_t * pNew;
+    Hop_Obj_t * pObj;
+    int i, Counter = 0;
+    Vec_PtrForEachEntry( p->vObjs, pObj, i )
+        pObj->pNext = NULL;
+    // start the HOP package
+    pNew = Hop_ManStart();
+    pNew->vObjs = Vec_PtrAlloc( p->nCreated );
+    Vec_PtrPush( pNew->vObjs, Hop_ManConst1(pNew) );
+    // map the constant node
+    Hop_ManConst1(p)->pNext = Hop_ManConst1(pNew);
+    // map the CIs
+    Hop_ManForEachPi( p, pObj, i )
+        pObj->pNext = Hop_ObjCreatePi(pNew);
+    // map the internal nodes
+    Vec_PtrForEachEntry( p->vObjs, pObj, i )
+    {
+        if ( !Hop_ObjIsNode(pObj) )
+            continue;
+        pObj->pNext = Hop_And( pNew, Hop_ObjChild0Hop(pObj), Hop_ObjChild1Hop(pObj) );
+//        assert( !Hop_IsComplement(pObj->pNext) );
+        if ( Hop_ManConst1(pNew) == Hop_Regular(pObj->pNext) )
+            Counter++;
+        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 );
+    // transfer the POs
+    Hop_ManForEachPo( p, pObj, i )
+        Hop_ObjCreatePo( pNew, Hop_ObjChild0Hop(pObj) );
+    // check the new manager
+    if ( !Hop_ManCheck(pNew) )
+    {
+        printf( "Abc_NtkHaigReconstruct: Check for History AIG has failed.\n" );
+        Hop_ManStop(pNew);
+        return NULL;
+    }
+    return pNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pOld is in the TFI of pNew.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkHaigCheckTfi_rec( Abc_Obj_t * pNode, Abc_Obj_t * pOld )
+{
+    if ( pNode == NULL )
+        return 0;
+    if ( pNode == pOld )
+        return 1;
+    // check the trivial cases
+    if ( Abc_ObjIsCi(pNode) )
+        return 0;
+    assert( Abc_ObjIsNode(pNode) );
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return 0;
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pNode );
+    // check the children
+    if ( Abc_NtkHaigCheckTfi_rec( Abc_ObjFanin0(pNode), pOld ) )
+        return 1;
+    if ( Abc_NtkHaigCheckTfi_rec( Abc_ObjFanin1(pNode), pOld ) )
+        return 1;
+    // check equivalent nodes
+    return Abc_NtkHaigCheckTfi_rec( pNode->pData, pOld );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pOld is in the TFI of pNew.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkHaigCheckTfi( Abc_Ntk_t * pNtk, Abc_Obj_t * pOld, Abc_Obj_t * pNew )
+{
+    assert( !Abc_ObjIsComplement(pOld) );
+    assert( !Abc_ObjIsComplement(pNew) );
+    Abc_NtkIncrementTravId(pNtk);
+    return Abc_NtkHaigCheckTfi_rec( pNew, pOld );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Abc_Obj_t * Hop_ObjChild0Next( Hop_Obj_t * pObj ) { return Abc_ObjNotCond( (Abc_Obj_t *)Hop_ObjFanin0(pObj)->pNext, Hop_ObjFaninC0(pObj) );  }
+static inline Abc_Obj_t * Hop_ObjChild1Next( Hop_Obj_t * pObj ) { return Abc_ObjNotCond( (Abc_Obj_t *)Hop_ObjFanin1(pObj)->pNext, Hop_ObjFaninC1(pObj) );  }
+
+/**Function*************************************************************
+
+  Synopsis    [Stops history AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkHaigRecreateAig( Abc_Ntk_t * pNtk, Hop_Man_t * p )
+{
+    Abc_Ntk_t * pNtkAig;
+    Abc_Obj_t * pObjOld, * pObjAbcThis, * pObjAbcRepr;
+    Hop_Obj_t * pObj;
+    int i;
+    assert( p->nCreated == Vec_PtrSize(p->vObjs) );
+
+    // start the new network
+    pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+
+    // transfer new nodes to the PIs of HOP
+    Hop_ManConst1(p)->pNext = (Hop_Obj_t *)Abc_AigConst1( pNtkAig );
+    Hop_ManForEachPi( p, pObj, i )
+        pObj->pNext = (Hop_Obj_t *)Abc_NtkCi( pNtkAig, i );
+
+    // construct new nodes
+    Vec_PtrForEachEntry( p->vObjs, pObj, i )
+    {
+        if ( !Hop_ObjIsNode(pObj) )
+            continue;
+        pObj->pNext = (Hop_Obj_t *)Abc_AigAnd( pNtkAig->pManFunc, Hop_ObjChild0Next(pObj), Hop_ObjChild1Next(pObj) );
+        assert( !Hop_IsComplement(pObj->pNext) );
+    }
+
+    // set the COs
+    Abc_NtkForEachCo( pNtk, pObjOld, i )
+        Abc_ObjAddFanin( pObjOld->pCopy, Hop_ObjChild0Next(Hop_ManPo(p,i)) );
+
+    // construct choice nodes
+    Vec_PtrForEachEntry( p->vObjs, pObj, i )
+    {
+        // skip the node without choices
+        if ( pObj->pData == NULL )
+            continue;
+        // skip the representative of the class
+        if ( pObj->pData == pObj )
+            continue;
+        // do not create choices for constant 1 and PIs
+        if ( !Hop_ObjIsNode(pObj->pData) )
+            continue;
+        // get the corresponding new nodes
+        pObjAbcThis = (Abc_Obj_t *)pObj->pNext;
+        pObjAbcRepr = (Abc_Obj_t *)((Hop_Obj_t *)pObj->pData)->pNext;
+        // the new node cannot be already in the class
+        assert( pObjAbcThis->pData == NULL );
+        // the new node cannot have fanouts
+        assert( Abc_ObjFanoutNum(pObjAbcThis) == 0 );
+        // these should be different nodes
+        assert( pObjAbcRepr != pObjAbcThis );
+        // do not create choices if there is a path from pObjAbcThis to pObjAbcRepr
+        if ( !Abc_NtkHaigCheckTfi( pNtkAig, pObjAbcRepr, pObjAbcThis ) )
+        {
+            // find the last node in the class
+            while ( pObjAbcRepr->pData )
+                pObjAbcRepr = pObjAbcRepr->pData;
+            // add the new node at the end of the list
+            pObjAbcRepr->pData = pObjAbcThis;
+        }
+    }
+
+    // finish the new network
+//    Abc_NtkFinalize( pNtk, pNtkAig );
+//    Abc_AigCleanup( pNtkAig->pManFunc );
+    // check correctness of the network
+    if ( !Abc_NtkCheck( pNtkAig ) )
+    {
+        printf( "Abc_NtkHaigUse: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkAig );
+        return NULL;
+    }
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resets representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkHaigResetReprsOld( Hop_Man_t * pMan )
+{
+    Vec_Ptr_t * vMembers, * vClasses;
+
+    // collect members of the classes and make them point to reprs
+    vMembers = Abc_NtkHaigCollectMembers( pMan );
+    printf( "Collected %6d class members.\n", Vec_PtrSize(vMembers) );
+
+    // create classes
+    vClasses = Abc_NtkHaigCreateClasses( vMembers );
+    printf( "Collected %6d classes. (Ave = %5.2f)\n", Vec_PtrSize(vClasses), 
+        (float)(Vec_PtrSize(vMembers))/Vec_PtrSize(vClasses) );
+
+    Vec_PtrFree( vMembers );
+    Vec_PtrFree( vClasses );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resets representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkHaigResetReprs( Hop_Man_t * p )
+{
+    Hop_Obj_t * pObj, * pRepr;
+    int i, nClasses, nMembers, nFanouts, nNormals;
+    // clear self-classes
+    Vec_PtrForEachEntry( p->vObjs, pObj, i )
+    {
+        // fix the strange situation of double-loop
+        pRepr = pObj->pData;
+        if ( pRepr && pRepr->pData == pObj )
+            pRepr->pData = pRepr;
+        // remove self-loops
+        if ( pObj->pData == pObj )
+            pObj->pData = NULL;
+    }
+    // set representatives
+    Vec_PtrForEachEntry( p->vObjs, pObj, i )
+    {
+        if ( pObj->pData == NULL )
+            continue;
+        // get representative of the node
+        pRepr = Hop_ObjRepr( pObj );
+        pRepr->pData = pRepr;
+        // set the representative
+        pObj->pData = pRepr;
+    }
+    // make each class point to the smallest topological order
+    Vec_PtrForEachEntry( p->vObjs, pObj, i )
+    {
+        if ( pObj->pData == NULL )
+            continue;
+        pRepr = Hop_ObjRepr( pObj );
+        if ( pRepr->Id > pObj->Id )
+        {
+            pRepr->pData = pObj;
+            pObj->pData = pObj;
+        }
+        else
+            pObj->pData = pRepr;
+    }
+    // count classes, members, and fanouts - and verify
+    nMembers = nClasses = nFanouts = nNormals = 0;
+    Vec_PtrForEachEntry( p->vObjs, pObj, i )
+    {
+        if ( pObj->pData == NULL )
+            continue;
+        // count members
+        nMembers++;
+        // count the classes and fanouts
+        if ( pObj->pData == pObj )
+            nClasses++;
+        else if ( Hop_ObjRefs(pObj) > 0 )
+            nFanouts++;
+        else
+            nNormals++;
+        // compare representatives
+        pRepr = Hop_ObjRepr( pObj );
+        assert( pObj->pData == pRepr );
+        assert( pRepr->Id <= pObj->Id );
+    }
+//    printf( "Nodes = %7d.  Member = %7d.  Classes = %6d.  Fanouts = %6d.  Normals = %6d.\n", 
+//        Hop_ManNodeNum(p), nMembers, nClasses, nFanouts, nNormals );
+    return nFanouts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops history AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk )
+{
+    Hop_Man_t * pMan, * pManTemp;
+    Abc_Ntk_t * pNtkAig;
+    Abc_Obj_t * pObj;
+    int i;
+
+    // check if HAIG is available
+    assert( Abc_NtkIsStrash(pNtk) );
+    if ( pNtk->pHaig == NULL )
+    {
+        printf( "Warning: History AIG is not available.\n" );
+        return NULL;
+    }
+    // convert HOP package into AIG with choices
+    // print HAIG stats
+//    Hop_ManPrintStats( pMan ); // USES DATA!!!
+
+    // add the POs
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Hop_ObjCreatePo( pNtk->pHaig, Abc_ObjChild0Equiv(pObj) );
+
+    // clean the old network
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->pEquiv = NULL;
+    pMan = pNtk->pHaig; 
+    pNtk->pHaig = 0;
+
+    // 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 );
+
+    // free HAIG
+    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                                ///
+////////////////////////////////////////////////////////////////////////
+
+