Version abc80130

1 files changed, 0 insertions, 723 deletions

diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
deleted file mode 100644
index c7488487..00000000
--- a/src/aig/aig/aigDfs.c
+++ /dev/null
@@ -1,723 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [aigDfs.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [AIG package.]
-
-  Synopsis    [DFS traversal procedures.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - April 28, 2007.]
-
-  Revision    [$Id: aigDfs.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManDfs_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
-{
-    if ( pObj == NULL )
-        return;
-    assert( !Aig_IsComplement(pObj) );
-    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
-        return;
-//    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
-    Aig_ManDfs_rec( p, Aig_ObjFanin0(pObj), vNodes );
-    Aig_ManDfs_rec( p, Aig_ObjFanin1(pObj), vNodes );
-    assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
-    Aig_ObjSetTravIdCurrent(p, pObj);
-    Vec_PtrPush( vNodes, pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj;
-    int i;
-    Aig_ManIncrementTravId( p );
-    // mark constant and PIs
-    Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
-    Aig_ManForEachPi( p, pObj, i )
-        Aig_ObjSetTravIdCurrent( p, pObj );
-    // if there are latches, mark them
-    if ( Aig_ManLatchNum(p) > 0 )
-        Aig_ManForEachObj( p, pObj, i )
-            if ( Aig_ObjIsLatch(pObj) )
-                Aig_ObjSetTravIdCurrent( p, pObj );
-    // go through the nodes
-    vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
-    Aig_ManForEachObj( p, pObj, i )
-        if ( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) )
-            Aig_ManDfs_rec( p, pObj, vNodes );
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Aig_ManDfsPio( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj;
-    int i;
-    Aig_ManIncrementTravId( p );
-    vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) );
-    Aig_ManForEachPo( p, pObj, i )
-        Aig_ManDfs_rec( p, pObj, vNodes );
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes )
-{
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj;
-    int i;
-    assert( Aig_ManLatchNum(p) == 0 );
-    Aig_ManIncrementTravId( p );
-    // mark constant and PIs
-    Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
-    Aig_ManForEachPi( p, pObj, i )
-        Aig_ObjSetTravIdCurrent( p, pObj );
-    // go through the nodes
-    vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
-    for ( i = 0; i < nNodes; i++ )
-        Aig_ManDfs_rec( p, ppNodes[i], vNodes );
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManDfsChoices_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
-{
-    if ( pObj == NULL )
-        return;
-    assert( !Aig_IsComplement(pObj) );
-    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
-        return;
-    assert( Aig_ObjIsNode(pObj) );
-    Aig_ManDfsChoices_rec( p, Aig_ObjFanin0(pObj), vNodes );
-    Aig_ManDfsChoices_rec( p, Aig_ObjFanin1(pObj), vNodes );
-    Aig_ManDfsChoices_rec( p, p->pEquivs[pObj->Id], vNodes );
-    assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
-    Aig_ObjSetTravIdCurrent(p, pObj);
-    Vec_PtrPush( vNodes, pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Aig_ManDfsChoices( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj;
-    int i;
-    assert( p->pEquivs != NULL );
-    Aig_ManIncrementTravId( p );
-    // mark constant and PIs
-    Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
-    Aig_ManForEachPi( p, pObj, i )
-        Aig_ObjSetTravIdCurrent( p, pObj );
-    // go through the nodes
-    vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
-    Aig_ManForEachPo( p, pObj, i )
-        Aig_ManDfsChoices_rec( p, Aig_ObjFanin0(pObj), vNodes );
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes in the reverse DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManDfsReverse_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
-{
-    Aig_Obj_t * pFanout;
-    int iFanout = -1, i;
-    assert( !Aig_IsComplement(pObj) );
-    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
-        return;
-    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
-    Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
-        Aig_ManDfsReverse_rec( p, pFanout, vNodes );
-    assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
-    Aig_ObjSetTravIdCurrent(p, pObj);
-    Vec_PtrPush( vNodes, pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes in the reverse DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj;
-    int i;
-    Aig_ManIncrementTravId( p );
-    // mark POs
-    Aig_ManForEachPo( p, pObj, i )
-        Aig_ObjSetTravIdCurrent( p, pObj );
-    // if there are latches, mark them
-    if ( Aig_ManLatchNum(p) > 0 )
-        Aig_ManForEachObj( p, pObj, i )
-            if ( Aig_ObjIsLatch(pObj) )
-                Aig_ObjSetTravIdCurrent( p, pObj );
-    // go through the nodes
-    vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
-    Aig_ManForEachObj( p, pObj, i )
-        if ( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) )
-            Aig_ManDfsReverse_rec( p, pObj, vNodes );
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the max number of levels in the manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManLevelNum( Aig_Man_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i, LevelsMax;
-    LevelsMax = 0;
-    Aig_ManForEachPo( p, pObj, i )
-        LevelsMax = AIG_MAX( LevelsMax, (int)Aig_ObjFanin0(pObj)->Level );
-    return LevelsMax;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the max number of levels in the manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManCountLevels( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj;
-    int i, LevelsMax, Level0, Level1;
-    // initialize the levels
-    Aig_ManConst1(p)->iData = 0;
-    Aig_ManForEachPi( p, pObj, i )
-        pObj->iData = 0;
-    // compute levels in a DFS order
-    vNodes = Aig_ManDfs( p );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-    {
-        Level0 = Aig_ObjFanin0(pObj)->iData;
-        Level1 = Aig_ObjFanin1(pObj)->iData;
-        pObj->iData = 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Level0, Level1);
-    }
-    Vec_PtrFree( vNodes );
-    // get levels of the POs
-    LevelsMax = 0;
-    Aig_ManForEachPo( p, pObj, i )
-        LevelsMax = AIG_MAX( LevelsMax, Aig_ObjFanin0(pObj)->iData );
-    return LevelsMax;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of AIG nodes rooted at this cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ConeMark_rec( Aig_Obj_t * pObj )
-{
-    assert( !Aig_IsComplement(pObj) );
-    if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
-        return;
-    Aig_ConeMark_rec( Aig_ObjFanin0(pObj) );
-    Aig_ConeMark_rec( Aig_ObjFanin1(pObj) );
-    assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
-    Aig_ObjSetMarkA( pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of AIG nodes rooted at this cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ConeCleanAndMark_rec( Aig_Obj_t * pObj )
-{
-    assert( !Aig_IsComplement(pObj) );
-    if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
-        return;
-    Aig_ConeCleanAndMark_rec( Aig_ObjFanin0(pObj) );
-    Aig_ConeCleanAndMark_rec( Aig_ObjFanin1(pObj) );
-    assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
-    Aig_ObjSetMarkA( pObj );
-    pObj->pData = NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of AIG nodes rooted at this cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ConeCountAndMark_rec( Aig_Obj_t * pObj )
-{
-    int Counter;
-    assert( !Aig_IsComplement(pObj) );
-    if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
-        return 0;
-    Counter = 1 + Aig_ConeCountAndMark_rec( Aig_ObjFanin0(pObj) ) + 
-        Aig_ConeCountAndMark_rec( Aig_ObjFanin1(pObj) );
-    assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
-    Aig_ObjSetMarkA( pObj );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of AIG nodes rooted at this cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ConeUnmark_rec( Aig_Obj_t * pObj )
-{
-    assert( !Aig_IsComplement(pObj) );
-    if ( !Aig_ObjIsNode(pObj) || !Aig_ObjIsMarkA(pObj) )
-        return;
-    Aig_ConeUnmark_rec( Aig_ObjFanin0(pObj) ); 
-    Aig_ConeUnmark_rec( Aig_ObjFanin1(pObj) );
-    assert( Aig_ObjIsMarkA(pObj) ); // loop detection
-    Aig_ObjClearMarkA( pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of AIG nodes rooted at this cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_DagSize( Aig_Obj_t * pObj )
-{
-    int Counter;
-    Counter = Aig_ConeCountAndMark_rec( Aig_Regular(pObj) );
-    Aig_ConeUnmark_rec( Aig_Regular(pObj) );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the support size of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_SupportSize_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int * pCounter )
-{
-    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
-        return;
-    Aig_ObjSetTravIdCurrent(p, pObj);
-    if ( Aig_ObjIsPi(pObj) )
-    {
-        (*pCounter)++;
-        return;
-    }
-    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
-    Aig_SupportSize_rec( p, Aig_ObjFanin0(pObj), pCounter );
-    if ( Aig_ObjFanin1(pObj) )
-        Aig_SupportSize_rec( p, Aig_ObjFanin1(pObj), pCounter );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the support size of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
-    int Counter = 0;
-    assert( !Aig_IsComplement(pObj) );
-    assert( !Aig_ObjIsPo(pObj) );
-    Aig_ManIncrementTravId( p );
-    Aig_SupportSize_rec( p, pObj, &Counter );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Transfers the AIG from one manager into another.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_Transfer_rec( Aig_Man_t * pDest, Aig_Obj_t * pObj )
-{
-    assert( !Aig_IsComplement(pObj) );
-    if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
-        return;
-    Aig_Transfer_rec( pDest, Aig_ObjFanin0(pObj) ); 
-    Aig_Transfer_rec( pDest, Aig_ObjFanin1(pObj) );
-    pObj->pData = Aig_And( pDest, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
-    Aig_ObjSetMarkA( pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Transfers the AIG from one manager into another.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pRoot, int nVars )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    // solve simple cases
-    if ( pSour == pDest )
-        return pRoot;
-    if ( Aig_ObjIsConst1( Aig_Regular(pRoot) ) )
-        return Aig_NotCond( Aig_ManConst1(pDest), Aig_IsComplement(pRoot) );
-    // set the PI mapping
-    Aig_ManForEachPi( pSour, pObj, i )
-    {
-        if ( i == nVars )
-           break;
-        pObj->pData = Aig_IthVar(pDest, i);
-    }
-    // transfer and set markings
-    Aig_Transfer_rec( pDest, Aig_Regular(pRoot) );
-    // clear the markings
-    Aig_ConeUnmark_rec( Aig_Regular(pRoot) );
-    return Aig_NotCond( Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_Compose_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFunc, Aig_Obj_t * pVar )
-{
-    assert( !Aig_IsComplement(pObj) );
-    if ( Aig_ObjIsMarkA(pObj) )
-        return;
-    if ( Aig_ObjIsConst1(pObj) || Aig_ObjIsPi(pObj) )
-    {
-        pObj->pData = pObj == pVar ? pFunc : pObj;
-        return;
-    }
-    Aig_Compose_rec( p, Aig_ObjFanin0(pObj), pFunc, pVar ); 
-    Aig_Compose_rec( p, Aig_ObjFanin1(pObj), pFunc, pVar );
-    pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
-    Aig_ObjSetMarkA( pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar )
-{
-    // quit if the PI variable is not defined
-    if ( iVar >= Aig_ManPiNum(p) )
-    {
-        printf( "Aig_Compose(): The PI variable %d is not defined.\n", iVar );
-        return NULL;
-    }
-    // recursively perform composition
-    Aig_Compose_rec( p, Aig_Regular(pRoot), pFunc, Aig_ManPi(p, iVar) );
-    // clear the markings
-    Aig_ConeUnmark_rec( Aig_Regular(pRoot) );
-    return Aig_NotCond( Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the internal nodes of the cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ObjCollectCut_rec( Aig_Obj_t * pNode, Vec_Ptr_t * vNodes )
-{
-//    Aig_Obj_t * pFan0 = Aig_ObjFanin0(pNode);
-//    Aig_Obj_t * pFan1 = Aig_ObjFanin1(pNode);
-    if ( pNode->fMarkA )
-        return;
-    pNode->fMarkA = 1;
-    assert( Aig_ObjIsNode(pNode) );
-    Aig_ObjCollectCut_rec( Aig_ObjFanin0(pNode), vNodes );
-    Aig_ObjCollectCut_rec( Aig_ObjFanin1(pNode), vNodes );
-    Vec_PtrPush( vNodes, pNode );
-//printf( "added %d  ", pNode->Id );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the internal nodes of the cut.]
-
-  Description [Does not include the leaves of the cut.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ObjCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    // collect and mark the leaves
-    Vec_PtrClear( vNodes );
-    Vec_PtrForEachEntry( vLeaves, pObj, i )
-    {
-        assert( pObj->fMarkA == 0 );
-        pObj->fMarkA = 1;
-//        printf( "%d " , pObj->Id );
-    }
-//printf( "\n" );
-    // collect and mark the nodes
-    Aig_ObjCollectCut_rec( pRoot, vNodes );
-    // clean the nodes
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-        pObj->fMarkA = 0;
-    Vec_PtrForEachEntry( vLeaves, pObj, i )
-        pObj->fMarkA = 0;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the nodes of the supergate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ObjCollectSuper_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
-{
-    int RetValue1, RetValue2, i;
-    // check if the node is visited
-    if ( Aig_Regular(pObj)->fMarkA )
-    {
-        // check if the node occurs in the same polarity
-        for ( i = 0; i < vSuper->nSize; i++ )
-            if ( vSuper->pArray[i] == pObj )
-                return 1;
-        // check if the node is present in the opposite polarity
-        for ( i = 0; i < vSuper->nSize; i++ )
-            if ( vSuper->pArray[i] == Aig_Not(pObj) )
-                return -1;
-        assert( 0 );
-        return 0;
-    }
-    // if the new node is complemented or a PI, another gate begins
-    if ( pObj != pRoot && (Aig_IsComplement(pObj) || Aig_ObjType(pObj) != Aig_ObjType(pRoot) || Aig_ObjRefs(pObj) > 1) )
-    {
-        Vec_PtrPush( vSuper, pObj );
-        Aig_Regular(pObj)->fMarkA = 1;
-        return 0;
-    }
-    assert( !Aig_IsComplement(pObj) );
-    assert( Aig_ObjIsNode(pObj) );
-    // go through the branches
-    RetValue1 = Aig_ObjCollectSuper_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper );
-    RetValue2 = Aig_ObjCollectSuper_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper );
-    if ( RetValue1 == -1 || RetValue2 == -1 )
-        return -1;
-    // return 1 if at least one branch has a duplicate
-    return RetValue1 || RetValue2;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the nodes of the supergate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
-{
-    int RetValue, i;
-    assert( !Aig_IsComplement(pObj) );
-    assert( Aig_ObjIsNode(pObj) );
-    // collect the nodes in the implication supergate
-    Vec_PtrClear( vSuper );
-    RetValue = Aig_ObjCollectSuper_rec( pObj, pObj, vSuper );
-    assert( Vec_PtrSize(vSuper) > 1 );
-    // unmark the visited nodes
-    Vec_PtrForEachEntry( vSuper, pObj, i )
-        Aig_Regular(pObj)->fMarkA = 0;
-    // if we found the node and its complement in the same implication supergate, 
-    // return empty set of nodes (meaning that we should use constant-0 node)
-    if ( RetValue == -1 )
-        vSuper->nSize = 0;
-    return RetValue;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-