path: root/src/proof/acec/acecTree.c

/**CFile****************************************************************

  FileName    [acecTree.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [CEC for arithmetic circuits.]

  Synopsis    [Adder tree construction.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: acecTree.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#include "acecInt.h"

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Acec_BoxFree( Acec_Box_t * pBox )
{
    Vec_WecFreeP( &pBox->vAdds );
    Vec_WecFreeP( &pBox->vLeafs );
    Vec_WecFreeP( &pBox->vRoots );
    Vec_WecFreeP( &pBox->vLeafLits );
    Vec_WecFreeP( &pBox->vRootLits );
    Vec_WecFreeP( &pBox->vUnique );
    Vec_WecFreeP( &pBox->vShared );
    Vec_BitFreeP( &pBox->vInvHadds );
    ABC_FREE( pBox );
}
void Acec_BoxFreeP( Acec_Box_t ** ppBox )
{
    if ( *ppBox )
        Acec_BoxFree( *ppBox );
    *ppBox = NULL;
}

/**Function*************************************************************

  Synopsis    [Find internal cut points with exactly one adder fanin/fanout.]

  Description [Returns a map of point into its input/output adder.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Acec_TreeAddInOutPoint( Vec_Int_t * vMap, int iObj, int iAdd, int fOut )
{
    int * pPlace = Vec_IntEntryP( vMap, Abc_Var2Lit(iObj, fOut) );
    if ( *pPlace == -1 )
        *pPlace = iAdd;
    else if ( *pPlace >= 0 )
        *pPlace = -2;
}
Vec_Int_t * Acec_TreeFindPoints( Gia_Man_t * p, Vec_Int_t * vAdds )
{
    Vec_Int_t * vMap = Vec_IntStartFull( 2*Gia_ManObjNum(p) );
    int i;
    for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
    {
        Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+0), i, 0 );
        Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+1), i, 0 );
        Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+2), i, 0 );
        Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+3), i, 1 );
        Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+4), i, 1 );
    }
    return vMap;
}

/**Function*************************************************************

  Synopsis    [Find adder trees as groups of adders connected vis cut-points.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Acec_TreeWhichPoint( Vec_Int_t * vAdds, int iAdd, int iObj )
{
    int k;
    for ( k = 0; k < 5; k++ )
        if ( Vec_IntEntry(vAdds, 6*iAdd+k) == iObj )
            return k;
    assert( 0 );
    return -1;
}
void Acec_TreeFindTrees2_rec( Vec_Int_t * vAdds, Vec_Int_t * vMap, int iAdd, int Rank, Vec_Int_t * vTree, Vec_Bit_t * vFound )
{
    extern void Acec_TreeFindTrees_rec( Vec_Int_t * vAdds, Vec_Int_t * vMap, int iObj, int Rank, Vec_Int_t * vTree, Vec_Bit_t * vFound );
    int k;
    if ( Vec_BitEntry(vFound, iAdd) )
        return;
    Vec_BitWriteEntry( vFound, iAdd, 1 );
    Vec_IntPush( vTree, iAdd );
    Vec_IntPush( vTree, Rank );
    //printf( "Assigning rank %d to (%d:%d).\n", Rank, Vec_IntEntry(vAdds, 6*iAdd+3), Vec_IntEntry(vAdds, 6*iAdd+4) );
    for ( k = 0; k < 5; k++ )
        Acec_TreeFindTrees_rec( vAdds, vMap, Vec_IntEntry(vAdds, 6*iAdd+k), k == 4 ? Rank + 1 : Rank, vTree, vFound );
}
void Acec_TreeFindTrees_rec( Vec_Int_t * vAdds, Vec_Int_t * vMap, int iObj, int Rank, Vec_Int_t * vTree, Vec_Bit_t * vFound )
{
    int In  = Vec_IntEntry( vMap, Abc_Var2Lit(iObj, 1) );
    int Out = Vec_IntEntry( vMap, Abc_Var2Lit(iObj, 0) );
    if ( In < 0 || Out < 0 )
        return;
    Acec_TreeFindTrees2_rec( vAdds, vMap, In,  Acec_TreeWhichPoint(vAdds, In, iObj) == 4 ? Rank-1 : Rank, vTree, vFound );
    Acec_TreeFindTrees2_rec( vAdds, vMap, Out, Rank, vTree, vFound );
}
Vec_Wec_t * Acec_TreeFindTrees( Gia_Man_t * p, Vec_Int_t * vAdds )
{
    Vec_Wec_t * vTrees = Vec_WecAlloc( 10 );
    Vec_Int_t * vMap   = Acec_TreeFindPoints( p, vAdds );
    Vec_Bit_t * vFound = Vec_BitStart( Vec_IntSize(vAdds)/6 );
    Vec_Int_t * vTree;
    int i, k, In, Out, Box, Rank, MinRank;
    // go through the cut-points
    Vec_IntForEachEntryDouble( vMap, In, Out, i )
    {
        if ( In < 0 || Out < 0 )
            continue;
        assert( Vec_BitEntry(vFound, In) == Vec_BitEntry(vFound, Out) );
        if ( Vec_BitEntry(vFound, In) )
            continue;
        vTree = Vec_WecPushLevel( vTrees );
        Acec_TreeFindTrees_rec( vAdds, vMap, i/2, 0, vTree, vFound );
        // normalize rank
        MinRank = ABC_INFINITY;
        Vec_IntForEachEntryDouble( vTree, Box, Rank, k )
            MinRank = Abc_MinInt( MinRank, Rank );
        Vec_IntForEachEntryDouble( vTree, Box, Rank, k )
            Vec_IntWriteEntry( vTree, k+1, Rank - MinRank );
    }
    Vec_BitFree( vFound );
    Vec_IntFree( vMap );
    // sort by size
    Vec_WecSort( vTrees, 1 );
    return vTrees;
}
void Acec_TreeFindTreesTest( Gia_Man_t * p )
{
    Vec_Wec_t * vTrees;

    abctime clk = Abc_Clock();
    Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, 1 );
    int nFadds = Ree_ManCountFadds( vAdds );
    printf( "Detected %d adders (%d FAs and %d HAs).  ", Vec_IntSize(vAdds)/6, nFadds, Vec_IntSize(vAdds)/6-nFadds );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );

    clk = Abc_Clock();
    vTrees = Acec_TreeFindTrees( p, vAdds );
    printf( "Collected %d trees with %d adders in them.  ", Vec_WecSize(vTrees), Vec_WecSizeSize(vTrees)/2 );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    Vec_WecPrint( vTrees, 0 );

    Vec_WecFree( vTrees );
    Vec_IntFree( vAdds );
}


/**Function*************************************************************

  Synopsis    [Creates leaves and roots.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Acec_CreateBoxMaxRank( Vec_Int_t * vTree )
{
    int k, Box, Rank, MaxRank = 0;
    Vec_IntForEachEntryDouble( vTree, Box, Rank, k )
        MaxRank = Abc_MaxInt( MaxRank, Rank );
    return MaxRank;
}
void Acec_TreeInsOuts( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree, Vec_Wec_t * vBoxes, Vec_Wec_t * vLeaves, Vec_Wec_t * vRoots )
{
    Vec_Bit_t * vIsLeaf = Vec_BitStart( Gia_ManObjNum(p) );
    Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(p) );
    Vec_Int_t * vLevel;
    int i, k, Box, Rank;
    Vec_BitWriteEntry( vIsLeaf, 0, 1 );
    Vec_BitWriteEntry( vIsRoot, 0, 1 );
    Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
    {
        Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+0), 1 );
        Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+1), 1 );
        Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+2), 1 );
        Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+3), 1 );
        Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+4), 1 );
    }
    Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
    {
        Vec_WecPush( vBoxes, Rank, Box );
        for ( k = 0; k < 3; k++ )
        {
            if ( Vec_BitEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+k) ) )
                continue;
            Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+k), 1 );
            Vec_WecPush( vLeaves, Rank, Vec_IntEntry(vAdds, 6*Box+k) );
        }
        for ( k = 3; k < 5; k++ )
        {
            if ( Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+k) ) )
                continue;
            Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+k), 1 );
            Vec_WecPush( vRoots, k == 4 ? Rank + 1 : Rank, Abc_Var2Lit(Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), k==4), Vec_IntEntry(vAdds, 6*Box+2)!=0)  );
        }
    }
    Vec_BitFree( vIsLeaf );
    Vec_BitFree( vIsRoot );
    // sort each level
    Vec_WecForEachLevel( vBoxes, vLevel, i )
        Vec_IntSort( vLevel, 0 );
    Vec_WecForEachLevel( vLeaves, vLevel, i )
        Vec_IntSort( vLevel, 0 );
    Vec_WecForEachLevel( vRoots, vLevel, i )
        Vec_IntSort( vLevel, 0 );
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Acec_TreeVerifyPhaseOne_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
{
    int Truth0, Truth1;
    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
        return pObj->Value;
    Gia_ObjSetTravIdCurrent(p, pObj);
    assert( Gia_ObjIsAnd(pObj) );
    assert( !Gia_ObjIsXor(pObj) );
    Truth0 = Acec_TreeVerifyPhaseOne_rec( p, Gia_ObjFanin0(pObj) );
    Truth1 = Acec_TreeVerifyPhaseOne_rec( p, Gia_ObjFanin1(pObj) );
    Truth0 = Gia_ObjFaninC0(pObj) ? 0xFF & ~Truth0 : Truth0;
    Truth1 = Gia_ObjFaninC1(pObj) ? 0xFF & ~Truth1 : Truth1;
    return (pObj->Value = Truth0 & Truth1);
}
void Acec_TreeVerifyPhaseOne( Gia_Man_t * p, Vec_Int_t * vAdds, int iBox, Vec_Bit_t * vPhase )
{
    Gia_Obj_t * pObj;
    unsigned TruthXor, TruthMaj, Truths[3] = { 0xAA, 0xCC, 0xF0 };
    int k, iObj, fFadd = Vec_IntEntry(vAdds, 6*iBox+2) > 0;

    //if ( !fFadd )
    //    return;

    Gia_ManIncrementTravId( p );
    for ( k = 0; k < 3; k++ )
    {
        iObj = Vec_IntEntry( vAdds, 6*iBox+k );
        if ( iObj == 0 )
            continue;
        pObj = Gia_ManObj( p, iObj );
        pObj->Value = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~Truths[k] : Truths[k];
        Gia_ObjSetTravIdCurrent( p, pObj );
    }

    iObj = Vec_IntEntry( vAdds, 6*iBox+3 );
    TruthXor = Acec_TreeVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
    TruthXor = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~TruthXor : TruthXor;

    iObj = Vec_IntEntry( vAdds, 6*iBox+4 );
    TruthMaj = Acec_TreeVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
    TruthMaj = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~TruthMaj : TruthMaj;

    if ( fFadd ) // FADD
    {
        if ( TruthXor != 0x96 )
            printf( "Fadd %d sum is wrong.\n", iBox );
        if ( TruthMaj != 0xE8 )
            printf( "Fadd %d carry is wrong.\n", iBox );
    }
    else
    {
        if ( TruthXor != 0x66 )
            printf( "Hadd %d sum is wrong.\n", iBox );
        if ( TruthMaj != 0x88 )
            printf( "Hadd %d carry is wrong.\n", iBox );
    }
}
void Acec_TreeVerifyPhases( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes, Vec_Bit_t * vPhase )
{
    Vec_Int_t * vLevel;
    int i, k, Box;
    Vec_WecForEachLevel( vBoxes, vLevel, i )
        Vec_IntForEachEntry( vLevel, Box, k )
            Acec_TreeVerifyPhaseOne( p, vAdds, Box, vPhase );
}

/**Function*************************************************************

  Synopsis    [Creates polarity.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Acec_TreeCarryMap( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes )
{
    Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
    Vec_Int_t * vLevel;
    int i, k, Box;
    Vec_WecForEachLevel( vBoxes, vLevel, i )
        Vec_IntForEachEntry( vLevel, Box, k )
            Vec_IntWriteEntry( vMap, Vec_IntEntry(vAdds, 6*Box+4), Box );
    return vMap;
}
void Acec_TreePhases_rec( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, int Node, int fPhase,
                         Vec_Bit_t * vPhase, Vec_Bit_t * vInvHadds, Vec_Bit_t * vVisit )
{
    int k, iBox, iXor, Sign, fXorPhase, fPhaseThis;
    assert( Node != 0 );
    if ( Vec_BitEntry(vVisit, Node) )
    {
        assert( Vec_BitEntry(vPhase, Node) == fPhase );
        return;
    }
    Vec_BitWriteEntry( vVisit, Node, 1 );
    if ( fPhase )
        Vec_BitWriteEntry( vPhase, Node, fPhase );
    iBox = Vec_IntEntry( vMap, Node );
    if ( iBox == -1 )
        return;
    assert( Node == Vec_IntEntry( vAdds, 6*iBox+4 ) );
    iXor = Vec_IntEntry( vAdds, 6*iBox+3 );
    Sign = Vec_IntEntry( vAdds, 6*iBox+5 );
    fXorPhase = ((Sign >> 3) & 1);
    if ( Vec_IntEntry(vAdds, 6*iBox+2) == 0 )
    {
        fPhase ^= ((Sign >> 2) & 1);
        // remember complemented HADD
        if ( fPhase )
            Vec_BitWriteEntry( vInvHadds, iBox, 1 );
    }
    for ( k = 0; k < 3; k++ )
    {
        int iObj = Vec_IntEntry( vAdds, 6*iBox+k );
        if ( iObj == 0 )
            continue;
        fPhaseThis = ((Sign >> k) & 1) ^ fPhase;
        fXorPhase ^= fPhaseThis;
        Acec_TreePhases_rec( p, vAdds, vMap, iObj, fPhaseThis, vPhase, vInvHadds, vVisit );
    }
    if ( Vec_BitEntry(vVisit, iXor) )
        assert( Vec_BitEntry(vPhase, iXor) == fXorPhase );
    if ( fXorPhase )
        Vec_BitWriteEntry( vPhase, iXor, fXorPhase );
}
void Acec_TreePhases( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes, 
                     Vec_Wec_t * vLeaves, Vec_Wec_t * vRoots, 
                     Vec_Wec_t * vLeafLits, Vec_Wec_t * vRootLits, Vec_Bit_t * vInvHadds )
{
    Vec_Int_t * vMap = Acec_TreeCarryMap( p, vAdds, vBoxes );
    Vec_Bit_t * vPhase = Vec_BitStart( Gia_ManObjNum(p) );
    Vec_Bit_t * vVisit = Vec_BitStart( Gia_ManObjNum(p) );
    Vec_Int_t * vLevel;
    int i, k, iObj;
    Vec_WecForEachLevelReverse( vRoots, vLevel, i )
    {
        Vec_IntForEachEntry( vLevel, iObj, k )
        {
            int fFadd = Abc_LitIsCompl(iObj);
            int fCout = Abc_LitIsCompl(Abc_Lit2Var(iObj));
            int Node  = Abc_Lit2Var(Abc_Lit2Var(iObj));
            if ( !fCout )
                continue;
            Acec_TreePhases_rec( p, vAdds, vMap, Node, fFadd, vPhase, vInvHadds, vVisit );
        }
    }
    Vec_IntFree( vMap );
    Vec_BitFree( vVisit );
    Acec_TreeVerifyPhases( p, vAdds, vBoxes, vPhase );
    // create leaves
    Vec_WecForEachLevel( vLeaves, vLevel, i )
        Vec_IntForEachEntry( vLevel, iObj, k )
            Vec_WecPush( vLeafLits, i, Abc_Var2Lit(iObj, Vec_BitEntry(vPhase, iObj)) );
    // add constants
    Vec_WecForEachLevel( vBoxes, vLevel, i )
        Vec_IntForEachEntry( vLevel, iObj, k )
            if ( Vec_BitEntry(vInvHadds, iObj) )
                Vec_WecPush( vLeafLits, i, 1 );
    // create roots
    Vec_WecForEachLevel( vRoots, vLevel, i )
        Vec_IntForEachEntry( vLevel, iObj, k )
            iObj >>= 2, Vec_WecPush( vRootLits, i, Abc_Var2Lit(iObj, Vec_BitEntry(vPhase, iObj)) );
    // cleanup
    Vec_BitFree( vPhase );
}

/**Function*************************************************************

  Synopsis    [Derives one adder tree.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Acec_PrintAdders( Vec_Wec_t * vBoxes, Vec_Int_t * vAdds )
{
    Vec_Int_t * vLevel;
    int i, k, iBox;
    Vec_WecForEachLevel( vBoxes, vLevel, i )
    {
        printf( " %4d : {", i );
        Vec_IntForEachEntry( vLevel, iBox, k )
            printf( " %s%d=(%d,%d)", Vec_IntEntry(vAdds, 6*iBox+2) == 0 ? "*":"", iBox, 
                                     Vec_IntEntry(vAdds, 6*iBox+3), Vec_IntEntry(vAdds, 6*iBox+4) );
        printf( " }\n" );
    }
}
void Vec_WecPrintLits( Vec_Wec_t * p )
{
    Vec_Int_t * vVec;
    int i, k, Entry;
    Vec_WecForEachLevel( p, vVec, i )
    {
        printf( " %4d : {", i );
        Vec_IntForEachEntry( vVec, Entry, k )
            printf( " %c%d", Abc_LitIsCompl(Entry) ? '-' : '+', Abc_Lit2Var(Entry) );
        printf( " }\n" );
    }
}
void Acec_PrintRootLits( Vec_Wec_t * vRoots )
{
    Vec_Int_t * vLevel;
    int i, k, iObj;
    Vec_WecForEachLevel( vRoots, vLevel, i )
    {
        printf( "Rank %d : ", i );
        Vec_IntForEachEntry( vLevel, iObj, k )
        {
            int fFadd = Abc_LitIsCompl(iObj);
            int fCout = Abc_LitIsCompl(Abc_Lit2Var(iObj));
            int Node  = Abc_Lit2Var(Abc_Lit2Var(iObj));
            printf( "%d%s%s ", Node, fCout ? "*" : "", (fCout && fFadd) ? "*" : "" );
        }
        printf( "\n" );
    }
}
void Acec_PrintBox( Acec_Box_t * pBox, Vec_Int_t * vAdds )
{
    printf( "Adders:\n" );
    Acec_PrintAdders( pBox->vAdds, vAdds );
    printf( "Inputs:\n" );
    Vec_WecPrintLits( pBox->vLeafLits );
    printf( "Outputs:\n" );
    Vec_WecPrintLits( pBox->vRootLits );
    //printf( "Raw outputs:\n" );
    //Acec_PrintRootLits( pBox->vRoots );
}

Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree )
{
    int MaxRank = Acec_CreateBoxMaxRank(vTree);

    Acec_Box_t * pBox = ABC_CALLOC( Acec_Box_t, 1 );
    pBox->pGia      = p;

    pBox->vAdds     = Vec_WecStart( MaxRank + 1 );
    pBox->vLeafs    = Vec_WecStart( MaxRank + 1 );
    pBox->vRoots    = Vec_WecStart( MaxRank + 2 );

    Acec_TreeInsOuts( p, vAdds, vTree, pBox->vAdds, pBox->vLeafs, pBox->vRoots );

    pBox->vLeafLits = Vec_WecStart( Vec_WecSize(pBox->vLeafs) );
    pBox->vRootLits = Vec_WecStart( Vec_WecSize(pBox->vRoots) );
    pBox->vInvHadds = Vec_BitStart( Vec_IntSize(vAdds)/6 );

    Acec_TreePhases( p, vAdds, pBox->vAdds, pBox->vLeafs, pBox->vRoots, pBox->vLeafLits, pBox->vRootLits, pBox->vInvHadds );

    return pBox;
}
void Acec_CreateBoxTest( Gia_Man_t * p )
{
    Acec_Box_t * pBox;
    Vec_Wec_t * vTrees;
    Vec_Int_t * vTree;

    abctime clk = Abc_Clock();
    Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, 1 );
    int i, nFadds = Ree_ManCountFadds( vAdds );
    printf( "Detected %d adders (%d FAs and %d HAs).  ", Vec_IntSize(vAdds)/6, nFadds, Vec_IntSize(vAdds)/6-nFadds );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );

    clk = Abc_Clock();
    vTrees = Acec_TreeFindTrees( p, vAdds );
    printf( "Collected %d trees with %d adders in them.  ", Vec_WecSize(vTrees), Vec_WecSizeSize(vTrees)/2 );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    //Vec_WecPrint( vTrees, 0 );

    Vec_WecForEachLevel( vTrees, vTree, i )
    {
        pBox = Acec_CreateBox( p, vAdds, Vec_WecEntry(vTrees, i) );
        printf( "Processing tree %d:  Ranks = %d.  Adders = %d.  Leaves = %d.  Roots = %d.\n", 
            i, Vec_WecSize(pBox->vAdds), Vec_WecSizeSize(pBox->vAdds), 
            Vec_WecSizeSize(pBox->vLeafLits), Vec_WecSizeSize(pBox->vRootLits)  );
        Acec_PrintBox( pBox, vAdds );
        Acec_BoxFreeP( &pBox );
    }

    Vec_WecFree( vTrees );
    Vec_IntFree( vAdds );
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, int fVerbose )
{
    Acec_Box_t * pBox = NULL;
    Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, fVerbose );
    Vec_Wec_t * vTrees = Acec_TreeFindTrees( p, vAdds );
    if ( vTrees && Vec_WecSize(vTrees) > 0 )
        pBox = Acec_CreateBox( p, vAdds, Vec_WecEntry(vTrees, 0) );
    if ( pBox )//&& fVerbose )
        printf( "Processing tree %d:  Ranks = %d.  Adders = %d.  Leaves = %d.  Roots = %d.\n", 
            0, Vec_WecSize(pBox->vAdds), Vec_WecSizeSize(pBox->vAdds), 
            Vec_WecSizeSize(pBox->vLeafLits), Vec_WecSizeSize(pBox->vRootLits)  );
    if ( pBox && fVerbose )
        Acec_PrintBox( pBox, vAdds );
    Vec_WecFreeP( &vTrees );
    Vec_IntFree( vAdds );
    return pBox;
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END