darBalance.c

Go to the documentation of this file.

 
#include "darInt.h"
#include "misc/tim/tim.h"
 
ABC_NAMESPACE_IMPL_START
 

 
//#define USE_LUTSIZE_BALANCE


int Dar_ObjCompareLits( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
{
    int Diff = Aig_ObjToLit(*pp1) - Aig_ObjToLit(*pp2);
    if ( Diff < 0 )
        return -1;
    if ( Diff > 0 ) 
        return 1;
    return 0; 
}
void Dar_BalanceUniqify( Aig_Obj_t * pObj, Vec_Ptr_t * vNodes, int fExor )
{
    Aig_Obj_t * pTemp, * pTempNext;
    int i, k;
    // sort the nodes by their literal
    Vec_PtrSort( vNodes, (int (*)(const void *, const void *))Dar_ObjCompareLits );
    // remove duplicates
    k = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pTemp, i )
    {
        if ( i + 1 == Vec_PtrSize(vNodes) )
        {
            Vec_PtrWriteEntry( vNodes, k++, pTemp );
            break;
        }
        pTempNext = (Aig_Obj_t *)Vec_PtrEntry( vNodes, i+1 );
        if ( !fExor && pTemp == Aig_Not(pTempNext) ) // pos_lit & neg_lit = 0
        {
            Vec_PtrClear( vNodes );
            return;
        }
        if ( pTemp != pTempNext )  // save if different
            Vec_PtrWriteEntry( vNodes, k++, pTemp );
        else if ( fExor ) // in case of XOR, remove identical
            i++;
    }
    Vec_PtrShrink( vNodes, k );
    if ( Vec_PtrSize(vNodes) < 2 )
        return;
    // check that there is no duplicates
    pTemp = (Aig_Obj_t *)Vec_PtrEntry( vNodes, 0 );
    Vec_PtrForEachEntryStart( Aig_Obj_t *, vNodes, pTempNext, i, 1 )
    {
        assert( pTemp != pTempNext );
        pTemp = pTempNext;
    }
}

void Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
{
    if ( pObj != pRoot && (Aig_IsComplement(pObj) || Aig_ObjType(pObj) != Aig_ObjType(pRoot) || Aig_ObjRefs(pObj) > 1 || Vec_PtrSize(vSuper) > 10000) )
        Vec_PtrPush( vSuper, pObj );
    else
    {
        assert( !Aig_IsComplement(pObj) );
        assert( Aig_ObjIsNode(pObj) );
        // go through the branches
        Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper );
        Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper );
    }
}
Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
{
    Vec_Ptr_t * vNodes;
    assert( !Aig_IsComplement(pObj) );
    assert( Aig_ObjIsNode(pObj) );
    // extend the storage
    if ( Vec_VecSize( vStore ) <= Level )
        Vec_VecPush( vStore, Level, 0 );
    // get the temporary array of nodes
    vNodes = Vec_VecEntry( vStore, Level );
    Vec_PtrClear( vNodes );
    // collect the nodes in the implication supergate
    Dar_BalanceCone_rec( pObj, pObj, vNodes );
    // remove duplicates
    Dar_BalanceUniqify( pObj, vNodes, Aig_ObjIsExor(pObj) );
    return vNodes;
}
 

/*
int Dar_BalanceCone_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)->fMarkB )
    {
        if ( Aig_ObjIsExor(pRoot) )
        {
            assert( !Aig_IsComplement(pObj) );
            // check if the node occurs in the same polarity
            Vec_PtrRemove( vSuper, pObj );
            Aig_Regular(pObj)->fMarkB = 0;
//printf( " Duplicated EXOR input!!! " );
            return 1;
        }
        else
        {
            // 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_PtrSize(vSuper) > 10000) )
    {
        Vec_PtrPush( vSuper, pObj );
        Aig_Regular(pObj)->fMarkB = 1;
        return 0;
    }
    assert( !Aig_IsComplement(pObj) );
    assert( Aig_ObjIsNode(pObj) );
    // go through the branches
    RetValue1 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper );
    RetValue2 = Dar_BalanceCone_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;
}
Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
{
    Vec_Ptr_t * vNodes;
    int RetValue, i;
    assert( !Aig_IsComplement(pObj) );
    // extend the storage
    if ( Vec_VecSize( vStore ) <= Level )
        Vec_VecPush( vStore, Level, 0 );
    // get the temporary array of nodes
    vNodes = Vec_VecEntry( vStore, Level );
    Vec_PtrClear( vNodes );
    // collect the nodes in the implication supergate
    RetValue = Dar_BalanceCone_rec( pObj, pObj, vNodes );
    assert( RetValue != 0 || vNodes->nSize > 1 );
    // unmark the visited nodes
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
        Aig_Regular(pObj)->fMarkB = 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 )
        vNodes->nSize = 0;
    return vNodes;
}
*/

int Dar_BalanceFindLeft( Vec_Ptr_t * vSuper )
{
    Aig_Obj_t * pObjRight, * pObjLeft;
    int Current;
    // if two or less nodes, pair with the first
    if ( Vec_PtrSize(vSuper) < 3 )
        return 0;
    // set the pointer to the one before the last
    Current = Vec_PtrSize(vSuper) - 2;
    pObjRight = (Aig_Obj_t *)Vec_PtrEntry( vSuper, Current );
    // go through the nodes to the left of this one
    for ( Current--; Current >= 0; Current-- )
    {
        // get the next node on the left
        pObjLeft = (Aig_Obj_t *)Vec_PtrEntry( vSuper, Current );
        // if the level of this node is different, quit the loop
        if ( Aig_ObjLevel(Aig_Regular(pObjLeft)) != Aig_ObjLevel(Aig_Regular(pObjRight)) )
            break;
    }
    Current++;    
    // get the node, for which the equality holds
    pObjLeft = (Aig_Obj_t *)Vec_PtrEntry( vSuper, Current );
    assert( Aig_ObjLevel(Aig_Regular(pObjLeft)) == Aig_ObjLevel(Aig_Regular(pObjRight)) );
    return Current;
}

void Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor )
{
    Aig_Obj_t * pObj1, * pObj2, * pObj3, * pGhost;
    int RightBound, i;
    // get the right bound
    RightBound = Vec_PtrSize(vSuper) - 2;
    assert( LeftBound <= RightBound );
    if ( LeftBound == RightBound )
        return;
    // get the two last nodes
    pObj1 = (Aig_Obj_t *)Vec_PtrEntry( vSuper, RightBound + 1 );
    pObj2 = (Aig_Obj_t *)Vec_PtrEntry( vSuper, RightBound     );
    if ( Aig_Regular(pObj1) == p->pConst1 || Aig_Regular(pObj2) == p->pConst1 || Aig_Regular(pObj1) == Aig_Regular(pObj2) )
        return;
    // find the first node that can be shared
    for ( i = RightBound; i >= LeftBound; i-- )
    {
        pObj3 = (Aig_Obj_t *)Vec_PtrEntry( vSuper, i );
        if ( Aig_Regular(pObj3) == p->pConst1 )
        {
            Vec_PtrWriteEntry( vSuper, i,          pObj2 );
            Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
            return;
        }
        if ( Aig_Regular(pObj1) == Aig_Regular(pObj3) )
        {
            if ( pObj3 == pObj2 )
                return;
            Vec_PtrWriteEntry( vSuper, i,          pObj2 );
            Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
            return;
        }
        pGhost = Aig_ObjCreateGhost( p, pObj1, pObj3, fExor? AIG_OBJ_EXOR : AIG_OBJ_AND );
        if ( Aig_TableLookup( p, pGhost ) )
        {
            if ( pObj3 == pObj2 )
                return;
            Vec_PtrWriteEntry( vSuper, i,          pObj2 );
            Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
            return;
        }
    }
/*
    // we did not find the node to share, randomize choice
    {
        int Choice = Aig_ManRandom(0) % (RightBound - LeftBound + 1);
        pObj3 = Vec_PtrEntry( vSuper, LeftBound + Choice );
        if ( pObj3 == pObj2 )
            return;
        Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pObj2 );
        Vec_PtrWriteEntry( vSuper, RightBound,         pObj3 );
    }
*/
}

int Aig_NodeCompareLevelsDecrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
{
    int Diff = Aig_ObjLevel(Aig_Regular(*pp1)) - Aig_ObjLevel(Aig_Regular(*pp2));
    if ( Diff > 0 )
        return -1;
    if ( Diff < 0 ) 
        return 1;
    Diff = Aig_ObjId(Aig_Regular(*pp1)) - Aig_ObjId(Aig_Regular(*pp2));
    if ( Diff > 0 )
        return -1;
    if ( Diff < 0 ) 
        return 1;
    return 0; 
}

void Dar_BalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj, int fExor )
{
    Aig_Obj_t * pObj1, * pObj2;
    int i;
    if ( Vec_PtrPushUnique(vStore, pObj) )
    {
        if ( fExor )
            Vec_PtrRemove(vStore, pObj);
        return;
    }
    // find the p of the node
    for ( i = vStore->nSize-1; i > 0; i-- )
    {
        pObj1 = (Aig_Obj_t *)vStore->pArray[i  ];
        pObj2 = (Aig_Obj_t *)vStore->pArray[i-1];
        if ( Aig_ObjLevel(Aig_Regular(pObj1)) <= Aig_ObjLevel(Aig_Regular(pObj2)) )
            break;
        vStore->pArray[i  ] = pObj2;
        vStore->pArray[i-1] = pObj1;
    }
}

Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel )
{
    Aig_Obj_t * pObj1, * pObj2;
    int LeftBound;
    assert( vSuper->nSize > 1 );
    // sort the new nodes by level in the decreasing order
    Vec_PtrSort( vSuper, (int (*)(const void *, const void *))Aig_NodeCompareLevelsDecrease );
    // balance the nodes
    while ( vSuper->nSize > 1 )
    {
        // find the left bound on the node to be paired
        LeftBound = (!fUpdateLevel)? 0 : Dar_BalanceFindLeft( vSuper );
        // find the node that can be shared (if no such node, randomize choice)
        Dar_BalancePermute( p, vSuper, LeftBound, Type == AIG_OBJ_EXOR );
        // pull out the last two nodes
        pObj1 = (Aig_Obj_t *)Vec_PtrPop(vSuper);
        pObj2 = (Aig_Obj_t *)Vec_PtrPop(vSuper);
        Dar_BalancePushUniqueOrderByLevel( vSuper, Aig_Oper(p, pObj1, pObj2, Type), Type == AIG_OBJ_EXOR );
    }
    return vSuper->nSize ? (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0) : Aig_ManConst0(p);
}
 

int Aig_BaseSize( Aig_Man_t * p, Aig_Obj_t * pObj, int nLutSize )
{
    int nBaseSize;
    pObj = Aig_Regular(pObj);
    if ( Aig_ObjIsConst1(pObj) )
        return 0;
    if ( Aig_ObjLevel(pObj) >= nLutSize )
        return 1;
    nBaseSize = Aig_SupportSize( p, pObj );
    if ( nBaseSize >= nLutSize )
        return 1;
    return nBaseSize;
}

Aig_Obj_t * Dar_BalanceBuildSuperTop( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel, int nLutSize )
{
    Vec_Ptr_t * vSubset;
    Aig_Obj_t * pObj;
    int i, nBaseSizeAll, nBaseSize;
    assert( vSuper->nSize > 1 );
    // sort the new nodes by level in the decreasing order
    Vec_PtrSort( vSuper, (int (*)(const void *, const void *))Aig_NodeCompareLevelsDecrease );
    // add one LUT at a time
    while ( Vec_PtrSize(vSuper) > 1 )
    {
        // isolate the group of nodes with nLutSize inputs
        nBaseSizeAll = 0;
        vSubset = Vec_PtrAlloc( nLutSize );
        Vec_PtrForEachEntryReverse( Aig_Obj_t *, vSuper, pObj, i )
        {
            nBaseSize = Aig_BaseSize( p, pObj, nLutSize );
            if ( nBaseSizeAll + nBaseSize > nLutSize && Vec_PtrSize(vSubset) > 1 )
                break;
            nBaseSizeAll += nBaseSize;
            Vec_PtrPush( vSubset, pObj );
        }
        // remove them from vSuper
        Vec_PtrShrink( vSuper, Vec_PtrSize(vSuper) - Vec_PtrSize(vSubset) );
        // create the new supergate
        pObj = Dar_BalanceBuildSuper( p, vSubset, Type, fUpdateLevel );
        Vec_PtrFree( vSubset );
        // add the new output
        Dar_BalancePushUniqueOrderByLevel( vSuper, pObj, Type == AIG_OBJ_EXOR );
    }
    return (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0);
}

Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel )
{
    Aig_Obj_t * pObjNew;
    Vec_Ptr_t * vSuper;
    int i;
    assert( !Aig_IsComplement(pObjOld) );
    assert( !Aig_ObjIsBuf(pObjOld) );
    // return if the result is known
    if ( pObjOld->pData )
        return (Aig_Obj_t *)pObjOld->pData;
    assert( Aig_ObjIsNode(pObjOld) );
    // get the implication supergate
    vSuper = Dar_BalanceCone( pObjOld, vStore, Level );
    // check if supergate contains two nodes in the opposite polarity
    if ( vSuper->nSize == 0 )
        return (Aig_Obj_t *)(pObjOld->pData = Aig_ManConst0(pNew));
    // for each old node, derive the new well-balanced node
    for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
    {
        pObjNew = Dar_Balance_rec( pNew, Aig_Regular((Aig_Obj_t *)vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
        if ( pObjNew == NULL )
            return NULL;
        vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement((Aig_Obj_t *)vSuper->pArray[i]) );
    }
    // check for exactly one node
    if ( vSuper->nSize == 1 )
        return (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0);
    // build the supergate
#ifdef USE_LUTSIZE_BALANCE
    pObjNew = Dar_BalanceBuildSuperTop( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel, 6 );
#else
    pObjNew = Dar_BalanceBuildSuper( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel );
#endif
    if ( pNew->Time2Quit && !(Aig_Regular(pObjNew)->Id & 255) && Abc_Clock() > pNew->Time2Quit )
        return NULL;
    // make sure the balanced node is not assigned
//    assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level );
    assert( pObjOld->pData == NULL );
    return (Aig_Obj_t *)(pObjOld->pData = pObjNew);
}

Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj, * pDriver, * pObjNew;
    Vec_Vec_t * vStore;
    int i;
    assert( Aig_ManVerifyTopoOrder(p) );
    // create the new manager 
    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    pNew->nAsserts = p->nAsserts;
    pNew->nConstrs = p->nConstrs;
    pNew->nBarBufs = p->nBarBufs;
    pNew->Time2Quit = p->Time2Quit;
    if ( p->vFlopNums )
        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
    // map the PI nodes
    Aig_ManCleanData( p );
    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
    vStore = Vec_VecAlloc( 50 );
    if ( p->pManTime != NULL )
    {
        float arrTime;
        Tim_ManIncrementTravId( (Tim_Man_t *)p->pManTime );
        Aig_ManSetCioIds( p );
        Aig_ManForEachObj( p, pObj, i )
        {
            if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) )
                continue;
            if ( Aig_ObjIsCi(pObj) )
            {
                // copy the PI
                pObjNew = Aig_ObjCreateCi(pNew); 
                pObj->pData = pObjNew;
                // set the arrival time of the new PI
                arrTime = Tim_ManGetCiArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj) );
                pObjNew->Level = (int)arrTime;
            }
            else if ( Aig_ObjIsCo(pObj) )
            {
                // perform balancing
                pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
                pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
                if ( pObjNew == NULL )
                {
                    Vec_VecFree( vStore );
                    Aig_ManStop( pNew );
                    return NULL;
                }
                pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
                // save arrival time of the output
                arrTime = (float)Aig_Regular(pObjNew)->Level;
                Tim_ManSetCoArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj), arrTime );
                // create PO
                pObjNew = Aig_ObjCreateCo( pNew, pObjNew );
            }
            else
                assert( 0 );
        }
        Aig_ManCleanCioIds( p );
        pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 );
    }
    else
    {
        Aig_ManForEachCi( p, pObj, i )
        {
            pObjNew = Aig_ObjCreateCi(pNew); 
            pObjNew->Level = pObj->Level;
            pObj->pData = pObjNew;
        }
        if ( p->nBarBufs == 0 )
        {
            Aig_ManForEachCo( p, pObj, i )
            {
                pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
                pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
                if ( pObjNew == NULL )
                {
                    Vec_VecFree( vStore );
                    Aig_ManStop( pNew );
                    return NULL;
                }
                pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
                pObjNew = Aig_ObjCreateCo( pNew, pObjNew );
            }
        }
        else
        {
            Vec_Ptr_t * vLits = Vec_PtrStart( Aig_ManCoNum(p) );
            Aig_ManForEachCo( p, pObj, i )
            {
                int k = i < p->nBarBufs ? Aig_ManCoNum(p) - p->nBarBufs + i : i - p->nBarBufs;
                pObj = Aig_ManCo( p, k );
                pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
                pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
                if ( pObjNew == NULL )
                {
                    Vec_VecFree( vStore );
                    Aig_ManStop( pNew );
                    return NULL;
                }
                pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
                Vec_PtrWriteEntry( vLits, k, pObjNew );
                if ( i < p->nBarBufs )
                    Aig_ManCi(pNew, Aig_ManCiNum(p) - p->nBarBufs + i)->Level = Aig_Regular(pObjNew)->Level;
            }
            Aig_ManForEachCo( p, pObj, i )
                Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrEntry(vLits, i) );
            Vec_PtrFree(vLits);
        }
    }
    Vec_VecFree( vStore );
    // remove dangling nodes
    Aig_ManCleanup( pNew );
    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
    // check the resulting AIG
    if ( !Aig_ManCheck(pNew) )
        printf( "Dar_ManBalance(): The check has failed.\n" );
    return pNew;
}

Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose )
{
    Aig_Man_t * pAigXor, * pRes;
    if ( fExor )
    {
        pAigXor = Aig_ManDupExor( pAig );
        if ( fVerbose )
            Dar_BalancePrintStats( pAigXor );
        pRes = Dar_ManBalance( pAigXor, fUpdateLevel );
        Aig_ManStop( pAigXor );
    }
    else
    {
        pRes = Dar_ManBalance( pAig, fUpdateLevel );
    }
    return pRes;
}

void Dar_BalancePrintStats( Aig_Man_t * p )
{
    Vec_Ptr_t * vSuper;
    Aig_Obj_t * pObj, * pTemp;
    int i, k;
    if ( Aig_ManExorNum(p) == 0 )
    {
        printf( "There is no EXOR gates.\n" );
        return;
    }
    Aig_ManForEachExor( p, pObj, i )
    {
        Aig_ObjFanin0(pObj)->fMarkA = 1;
        Aig_ObjFanin1(pObj)->fMarkA = 1;
        assert( !Aig_ObjFaninC0(pObj) );
        assert( !Aig_ObjFaninC1(pObj) );
    }
    vSuper = Vec_PtrAlloc( 1000 );
    Aig_ManForEachExor( p, pObj, i )
    {
        if ( pObj->fMarkA && pObj->nRefs == 1 )
            continue;
        Vec_PtrClear( vSuper );
        Dar_BalanceCone_rec( pObj, pObj, vSuper );
        Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pTemp, k )
            pTemp->fMarkB = 0;
        if ( Vec_PtrSize(vSuper) < 3 )
            continue;
        printf( "  %d(", Vec_PtrSize(vSuper) );
        Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pTemp, k )
            printf( " %d", pTemp->Level );
        printf( " )" );
    }
    Vec_PtrFree( vSuper );
    Aig_ManForEachObj( p, pObj, i )
        pObj->fMarkA = 0;
    printf( "\n" );
}

 
 
ABC_NAMESPACE_IMPL_END