abc/src/opt/sbd/sbdCut2.c - third_party/vtr-verilog-to-routing - Git at Google


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


              FileName    [sbdCut2.c]


              SystemName  [ABC: Logic synthesis and verification system.]


              PackageName [SAT-based optimization using internal don't-cares.]


              Synopsis    [Cut computation.]


              Author      [Alan Mishchenko]


              Affiliation [UC Berkeley]


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


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


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


            #include "sbdInt.h"


            ABC_NAMESPACE_IMPL_START


            ////////////////////////////////////////////////////////////////////////

            
            ///                        DECLARATIONS                              ///

            
            ////////////////////////////////////////////////////////////////////////


            #define SBD_MAX_CUTSIZE   10

            
            #define SBD_MAX_CUTNUM    501


            #define SBD_CUT_NO_LEAF   0xF


            typedef struct Sbd_Cut_t_ Sbd_Cut_t;

            
            struct Sbd_Cut_t_

            
            {

            
                word            Sign;                      // signature

            
                int             iFunc;                     // functionality

            
                int             Cost;                      // cut cost

            
                int             CostLev;                   // cut cost

            
                unsigned        nTreeLeaves  :  9;         // tree leaves

            
                unsigned        nSlowLeaves  :  9;         // slow leaves

            
                unsigned        nTopLeaves   : 10;         // top leaves

            
                unsigned        nLeaves      :  4;         // leaf count

            
                int             pLeaves[SBD_MAX_CUTSIZE];  // leaves

            
            };


            struct Sbd_Srv_t_

            
            {

            
                int             nLutSize;

            
                int             nCutSize;

            
                int             nCutNum;

            
                int             fVerbose;

            
                Gia_Man_t *     pGia;                      // user's AIG manager (will be modified by adding nodes)

            
                Vec_Int_t *     vMirrors;                  // mirrors for each node

            
                Vec_Int_t *     vLutLevs;                  // delays for each node

            
                Vec_Int_t *     vLevs;                     // levels for each node

            
                Vec_Int_t *     vRefs;                     // refs for each node

            
                Sbd_Cut_t       pCuts[SBD_MAX_CUTNUM];     // temporary cuts

            
                Sbd_Cut_t *     ppCuts[SBD_MAX_CUTNUM];    // temporary cut pointers

            
                abctime         clkStart;                  // starting time

            
                Vec_Int_t *     vCut0;                     // current cut

            
                Vec_Int_t *     vCut;                      // current cut

            
                Vec_Int_t *     vCutTop;                   // current cut

            
                Vec_Int_t *     vCutBot;                   // current cut

            
            };


            ////////////////////////////////////////////////////////////////////////

            
            ///                     FUNCTION DEFINITIONS                         ///

            
            ////////////////////////////////////////////////////////////////////////


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


              Synopsis    []


              Description []


              SideEffects []


              SeeAlso     []


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

            
            Sbd_Srv_t * Sbd_ManCutServerStart( Gia_Man_t * pGia, Vec_Int_t * vMirrors,

            
                                               Vec_Int_t * vLutLevs, Vec_Int_t * vLevs, Vec_Int_t * vRefs,

            
                                               int nLutSize, int nCutSize, int nCutNum, int fVerbose )

            
            {

            
                Sbd_Srv_t * p;

            
                assert( nLutSize <= nCutSize );

            
                assert( nCutSize < SBD_CUT_NO_LEAF );

            
                assert( nCutSize > 1 && nCutSize <= SBD_MAX_CUTSIZE );

            
                assert( nCutNum > 1 && nCutNum < SBD_MAX_CUTNUM );

            
                p = ABC_CALLOC( Sbd_Srv_t, 1 );

            
                p->clkStart = Abc_Clock();

            
                p->nLutSize = nLutSize;

            
                p->nCutSize = nCutSize;

            
                p->nCutNum  = nCutNum;

            
                p->fVerbose = fVerbose;

            
                p->pGia     = pGia;

            
                p->vMirrors = vMirrors;

            
                p->vLutLevs = vLutLevs;

            
                p->vLevs    = vLevs;

            
                p->vRefs    = vRefs;

            
                p->vCut0    = Vec_IntAlloc( 100 );

            
                p->vCut     = Vec_IntAlloc( 100 );

            
                p->vCutTop  = Vec_IntAlloc( 100 );

            
                p->vCutBot  = Vec_IntAlloc( 100 );

            
                return p;

            
            }

            
            void Sbd_ManCutServerStop( Sbd_Srv_t * p )

            
            {

            
                Vec_IntFree( p->vCut0 );

            
                Vec_IntFree( p->vCut );

            
                Vec_IntFree( p->vCutTop );

            
                Vec_IntFree( p->vCutBot );

            
                ABC_FREE( p );

            
            }


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


              Synopsis    []


              Description []


              SideEffects []


              SeeAlso     []


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

            
            int Sbd_ManCutIsTopo_rec( Gia_Man_t * p, Vec_Int_t * vMirrors, int iObj )

            
            {

            
                Gia_Obj_t * pObj;

            
                int Ret0, Ret1;

            
                if ( Vec_IntEntry(vMirrors, iObj) >= 0 )

            
                    iObj = Abc_Lit2Var(Vec_IntEntry(vMirrors, iObj));

            
                if ( !iObj || Gia_ObjIsTravIdCurrentId(p, iObj) )

            
                    return 1;

            
                Gia_ObjSetTravIdCurrentId(p, iObj);

            
                pObj = Gia_ManObj( p, iObj );

            
                if ( Gia_ObjIsCi(pObj) )

            
                    return 0;

            
                assert( Gia_ObjIsAnd(pObj) );

            
                Ret0 = Sbd_ManCutIsTopo_rec( p, vMirrors, Gia_ObjFaninId0(pObj, iObj) );

            
                Ret1 = Sbd_ManCutIsTopo_rec( p, vMirrors, Gia_ObjFaninId1(pObj, iObj) );

            
                return Ret0 && Ret1;

            
            }

            
            int Sbd_ManCutIsTopo( Gia_Man_t * p, Vec_Int_t * vMirrors, Vec_Int_t * vCut, int iObj )

            
            {

            
                int i, Entry, RetValue;

            
                Gia_ManIncrementTravId( p );

            
                Vec_IntForEachEntry( vCut, Entry, i )

            
                    Gia_ObjSetTravIdCurrentId( p, Entry );

            
                RetValue = Sbd_ManCutIsTopo_rec( p, vMirrors, iObj );

            
                if ( RetValue == 0 )

            
                    printf( "Cut of node %d is not tological\n", iObj );

            
                assert( RetValue );

            
                return RetValue;

            
            }


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


              Synopsis    []


              Description []


              SideEffects []


              SeeAlso     []


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

            
            static inline int Sbd_ManCutExpandOne( Gia_Man_t * p, Vec_Int_t * vMirrors, Vec_Int_t * vLutLevs, Vec_Int_t * vCut, int iThis, int iObj )

            
            {

            
                int Lit0m, Lit1m, Fan0, Fan1, iPlace0, iPlace1;

            
                int LutLev = Vec_IntEntry( vLutLevs, iObj );

            
                Gia_Obj_t * pObj = Gia_ManObj(p, iObj);

            
                if ( Gia_ObjIsCi(pObj) )

            
                    return 0;

            
                assert( Gia_ObjIsAnd(pObj) );

            
                Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) );

            
                Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, iObj) );

            
                Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);

            
                Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);

            
                iPlace0 = Vec_IntFind( vCut, Fan0 );

            
                iPlace1 = Vec_IntFind( vCut, Fan1 );

            
                if ( iPlace0 == -1 && iPlace1 == -1 )

            
                    return 0;

            
                if ( Vec_IntEntry(vLutLevs, Fan0) > LutLev || Vec_IntEntry(vLutLevs, Fan1) > LutLev )

            
                    return 0;

            
                Vec_IntDrop( vCut, iThis );

            
                if ( iPlace0 == -1 && Fan0 )

            
                    Vec_IntPushOrder( vCut, Fan0 );

            
                if ( iPlace1 == -1 && Fan1 )

            
                    Vec_IntPushOrder( vCut, Fan1 );

            
                return 1;

            
            }

            
            void Vec_IntIsOrdered( Vec_Int_t * vCut )

            
            {

            
                int i, Prev, Entry;

            
                Prev = Vec_IntEntry( vCut, 0 );

            
                Vec_IntForEachEntryStart( vCut, Entry, i, 1 )

            
                {

            
                    assert( Prev < Entry );

            
                    Prev = Entry;

            
                }

            
            }

            
            void Sbd_ManCutExpand( Gia_Man_t * p, Vec_Int_t * vMirrors, Vec_Int_t * vLutLevs, Vec_Int_t * vCut )

            
            {

            
                int i, Entry;

            
                do

            
                {

            
                    Vec_IntForEachEntry( vCut, Entry, i )

            
                        if ( Sbd_ManCutExpandOne( p, vMirrors, vLutLevs, vCut, i, Entry ) )

            
                            break;

            
                }

            
                while ( i < Vec_IntSize(vCut) );

            
            }

            
            void Sbd_ManCutReload( Vec_Int_t * vMirrors, Vec_Int_t * vLutLevs, int LevStop, Vec_Int_t * vCut, Vec_Int_t * vCutTop, Vec_Int_t * vCutBot )

            
            {

            
                int i, Entry;

            
                Vec_IntClear( vCutTop );

            
                Vec_IntClear( vCutBot );

            
                Vec_IntForEachEntry( vCut, Entry, i )

            
                {

            
                    assert( Entry );

            
                    assert( Vec_IntEntry(vMirrors, Entry) == -1 );

            
                    assert( Vec_IntEntry(vLutLevs, Entry) <= LevStop );

            
                    if ( Vec_IntEntry(vLutLevs, Entry) == LevStop )

            
                        Vec_IntPush( vCutTop, Entry );

            
                    else

            
                        Vec_IntPush( vCutBot, Entry );

            
                }

            
                Vec_IntIsOrdered( vCut );

            
            }

            
            int Sbd_ManCutCollect_rec( Gia_Man_t * p, Vec_Int_t * vMirrors, int iObj, int LevStop, Vec_Int_t * vLutLevs, Vec_Int_t * vCut )

            
            {

            
                Gia_Obj_t * pObj;

            
                int Ret0, Ret1;

            
                if ( Vec_IntEntry(vMirrors, iObj) >= 0 )

            
                    iObj = Abc_Lit2Var(Vec_IntEntry(vMirrors, iObj));

            
                if ( !iObj || Gia_ObjIsTravIdCurrentId(p, iObj) )

            
                    return 1;

            
                Gia_ObjSetTravIdCurrentId(p, iObj);

            
                pObj = Gia_ManObj( p, iObj );

            
                if ( Gia_ObjIsCi(pObj) || Vec_IntEntry(vLutLevs, iObj) <= LevStop )

            
                {

            
                    Vec_IntPush( vCut, iObj );

            
                    return Vec_IntEntry(vLutLevs, iObj) <= LevStop;

            
                }

            
                assert( Gia_ObjIsAnd(pObj) );

            
                Ret0 = Sbd_ManCutCollect_rec( p, vMirrors, Gia_ObjFaninId0(pObj, iObj), LevStop, vLutLevs, vCut );

            
                Ret1 = Sbd_ManCutCollect_rec( p, vMirrors, Gia_ObjFaninId1(pObj, iObj), LevStop, vLutLevs, vCut );

            
                return Ret0 && Ret1;

            
            }


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


              Synopsis    []


              Description []


              SideEffects []


              SeeAlso     []


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

            
            int Sbd_ManCutReduceTop( Gia_Man_t * p, Vec_Int_t * vMirrors, int iObj, Vec_Int_t * vLutLevs, Vec_Int_t * vCut, Vec_Int_t * vCutTop, int nCutSize )

            
            {

            
                int i, Entry, Lit0m, Lit1m, Fan0, Fan1;

            
                int LevStop = Vec_IntEntry(vLutLevs, iObj) - 2;

            
                Vec_IntIsOrdered( vCut );

            
                Vec_IntForEachEntryReverse( vCutTop, Entry, i )

            
                {

            
                    Gia_Obj_t * pObj = Gia_ManObj( p, Entry );

            
                    if ( Gia_ObjIsCi(pObj) )

            
                        continue;

            
                    assert( Gia_ObjIsAnd(pObj) );

            
                    assert( Vec_IntEntry(vLutLevs, Entry) == LevStop );

            
                    Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, Entry) );

            
                    Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, Entry) );

            
                    Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, Entry);

            
                    Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, Entry);

            
                    if ( Vec_IntEntry(vLutLevs, Fan0) > LevStop || Vec_IntEntry(vLutLevs, Fan1) > LevStop )

            
                        continue;

            
                    assert( Vec_IntEntry(vLutLevs, Fan0) <= LevStop );

            
                    assert( Vec_IntEntry(vLutLevs, Fan1) <= LevStop );

            
                    if ( Vec_IntEntry(vLutLevs, Fan0) == LevStop && Vec_IntEntry(vLutLevs, Fan1) == LevStop )

            
                        continue;

            
                    Vec_IntRemove( vCut, Entry );

            
                    if ( Fan0 ) Vec_IntPushUniqueOrder( vCut, Fan0 );

            
                    if ( Fan1 ) Vec_IntPushUniqueOrder( vCut, Fan1 );

            
                    //Sbd_ManCutIsTopo( p, vMirrors, vCut, iObj );

            
                    return 1;

            
                }

            
                return 0;

            
            }


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


              Synopsis    []


              Description []


              SideEffects []


              SeeAlso     []


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

            
            int Sbd_ManCutServerFirst( Sbd_Srv_t * p, int iObj, int * pLeaves )

            
            {

            
                int RetValue, LevStop = Vec_IntEntry(p->vLutLevs, iObj) - 2;


                Vec_IntClear( p->vCut );

            
                Gia_ManIncrementTravId( p->pGia );

            
                RetValue = Sbd_ManCutCollect_rec( p->pGia, p->vMirrors, iObj, LevStop, p->vLutLevs, p->vCut );

            
                if ( RetValue == 0 ) // cannot build delay-improving cut

            
                    return -1;

            
                // check if the current cut is good

            
                Vec_IntSort( p->vCut, 0 );

            
            /*

            
                Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );

            
                if ( Vec_IntSize(p->vCut) <= p->nCutSize && Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )

            
                {

            
                    //printf( "%d ", Vec_IntSize(p->vCut) );

            
                    memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );

            
                    return Vec_IntSize(p->vCut);

            
                }

            
            */

            
                // try to expand the cut

            
                Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );

            
                Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );

            
                if ( Vec_IntSize(p->vCut) <= p->nCutSize && Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )

            
                {

            
                    //printf( "1=(%d,%d) ", Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );

            
                    //printf( "%d ", Vec_IntSize(p->vCut) );

            
                    memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );

            
                    return Vec_IntSize(p->vCut);

            
                }


                // try to reduce the topmost

            
                Vec_IntClear( p->vCut0 );

            
                Vec_IntAppend( p->vCut0, p->vCut );

            
                if ( Vec_IntSize(p->vCut) < p->nCutSize && Sbd_ManCutReduceTop( p->pGia, p->vMirrors, iObj, p->vLutLevs, p->vCut, p->vCutTop, p->nCutSize ) )

            
                {

            
                    Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );

            
                    Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );

            
                    assert( Vec_IntSize(p->vCut) <= p->nCutSize );

            
                    if ( Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )

            
                    {

            
                        //printf( "%d -> %d (%d + %d)\n", Vec_IntSize(p->vCut0), Vec_IntSize(p->vCut), Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );

            
                        memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );

            
                        return Vec_IntSize(p->vCut);

            
                    }

            
                    // try again

            
                    if ( Vec_IntSize(p->vCut) < p->nCutSize && Sbd_ManCutReduceTop( p->pGia, p->vMirrors, iObj, p->vLutLevs, p->vCut, p->vCutTop, p->nCutSize ) )

            
                    {

            
                        Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );

            
                        Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );

            
                        assert( Vec_IntSize(p->vCut) <= p->nCutSize );

            
                        if ( Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )

            
                        {

            
                            //printf( "* %d -> %d (%d + %d)\n", Vec_IntSize(p->vCut0), Vec_IntSize(p->vCut), Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );

            
                            memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );

            
                            return Vec_IntSize(p->vCut);

            
                        }

            
                        // try again

            
                        if ( Vec_IntSize(p->vCut) < p->nCutSize && Sbd_ManCutReduceTop( p->pGia, p->vMirrors, iObj, p->vLutLevs, p->vCut, p->vCutTop, p->nCutSize ) )

            
                        {

            
                            Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );

            
                            Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );

            
                            assert( Vec_IntSize(p->vCut) <= p->nCutSize );

            
                            if ( Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )

            
                            {

            
                                //printf( "** %d -> %d (%d + %d)\n", Vec_IntSize(p->vCut0), Vec_IntSize(p->vCut), Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );

            
                                memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );

            
                                return Vec_IntSize(p->vCut);

            
                            }

            
                            // try again

            
                            if ( Vec_IntSize(p->vCut) < p->nCutSize && Sbd_ManCutReduceTop( p->pGia, p->vMirrors, iObj, p->vLutLevs, p->vCut, p->vCutTop, p->nCutSize ) )

            
                            {

            
                                Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );

            
                                Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );

            
                                assert( Vec_IntSize(p->vCut) <= p->nCutSize );

            
                                if ( Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )

            
                                {

            
                                    //printf( "*** %d -> %d (%d + %d)\n", Vec_IntSize(p->vCut0), Vec_IntSize(p->vCut), Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );

            
                                    memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );

            
                                    return Vec_IntSize(p->vCut);

            
                                }

            
                            }

            
                        }

            
                    }

            
                }


                // recompute the cut

            
                Vec_IntClear( p->vCut );

            
                Gia_ManIncrementTravId( p->pGia );

            
                RetValue = Sbd_ManCutCollect_rec( p->pGia, p->vMirrors, iObj, LevStop-1, p->vLutLevs, p->vCut );

            
                if ( RetValue == 0 ) // cannot build delay-improving cut

            
                    return -1;

            
                // check if the current cut is good

            
                Vec_IntSort( p->vCut, 0 );

            
            /*

            
                Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );

            
                if ( Vec_IntSize(p->vCut) <= p->nCutSize && Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )

            
                {

            
                    //printf( "%d ", Vec_IntSize(p->vCut) );

            
                    memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );

            
                    return Vec_IntSize(p->vCut);

            
                }

            
            */

            
                // try to expand the cut

            
                Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );

            
                Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );

            
                if ( Vec_IntSize(p->vCut) <= p->nCutSize && Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )

            
                {

            
                    //printf( "2=(%d,%d) ", Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );

            
                    //printf( "%d ", Vec_IntSize(p->vCut) );

            
                    memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );

            
                    return Vec_IntSize(p->vCut);

            
                }


                return -1;

            
            }


            ////////////////////////////////////////////////////////////////////////

            
            ///                       END OF FILE                                ///

            
            ////////////////////////////////////////////////////////////////////////


            ABC_NAMESPACE_IMPL_END
	/CFile**************************************************************

	FileName [sbdCut2.c]

	SystemName [ABC: Logic synthesis and verification system.]

	PackageName [SAT-based optimization using internal don't-cares.]

	Synopsis [Cut computation.]

	Author [Alan Mishchenko]

	Affiliation [UC Berkeley]

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

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

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

	#include "sbdInt.h"

	ABC_NAMESPACE_IMPL_START


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

	#define SBD_MAX_CUTSIZE 10
	#define SBD_MAX_CUTNUM 501

	#define SBD_CUT_NO_LEAF 0xF

	typedef struct Sbd_Cut_t_ Sbd_Cut_t;
	struct Sbd_Cut_t_
	{
	word Sign; // signature
	int iFunc; // functionality
	int Cost; // cut cost
	int CostLev; // cut cost
	unsigned nTreeLeaves : 9; // tree leaves
	unsigned nSlowLeaves : 9; // slow leaves
	unsigned nTopLeaves : 10; // top leaves
	unsigned nLeaves : 4; // leaf count
	int pLeaves[SBD_MAX_CUTSIZE]; // leaves
	};

	struct Sbd_Srv_t_
	{
	int nLutSize;
	int nCutSize;
	int nCutNum;
	int fVerbose;
	Gia_Man_t * pGia; // user's AIG manager (will be modified by adding nodes)
	Vec_Int_t * vMirrors; // mirrors for each node
	Vec_Int_t * vLutLevs; // delays for each node
	Vec_Int_t * vLevs; // levels for each node
	Vec_Int_t * vRefs; // refs for each node
	Sbd_Cut_t pCuts[SBD_MAX_CUTNUM]; // temporary cuts
	Sbd_Cut_t * ppCuts[SBD_MAX_CUTNUM]; // temporary cut pointers
	abctime clkStart; // starting time
	Vec_Int_t * vCut0; // current cut
	Vec_Int_t * vCut; // current cut
	Vec_Int_t * vCutTop; // current cut
	Vec_Int_t * vCutBot; // current cut
	};

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

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

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	Sbd_Srv_t * Sbd_ManCutServerStart( Gia_Man_t * pGia, Vec_Int_t * vMirrors,
	Vec_Int_t * vLutLevs, Vec_Int_t * vLevs, Vec_Int_t * vRefs,
	int nLutSize, int nCutSize, int nCutNum, int fVerbose )
	{
	Sbd_Srv_t * p;
	assert( nLutSize <= nCutSize );
	assert( nCutSize < SBD_CUT_NO_LEAF );
	assert( nCutSize > 1 && nCutSize <= SBD_MAX_CUTSIZE );
	assert( nCutNum > 1 && nCutNum < SBD_MAX_CUTNUM );
	p = ABC_CALLOC( Sbd_Srv_t, 1 );
	p->clkStart = Abc_Clock();
	p->nLutSize = nLutSize;
	p->nCutSize = nCutSize;
	p->nCutNum = nCutNum;
	p->fVerbose = fVerbose;
	p->pGia = pGia;
	p->vMirrors = vMirrors;
	p->vLutLevs = vLutLevs;
	p->vLevs = vLevs;
	p->vRefs = vRefs;
	p->vCut0 = Vec_IntAlloc( 100 );
	p->vCut = Vec_IntAlloc( 100 );
	p->vCutTop = Vec_IntAlloc( 100 );
	p->vCutBot = Vec_IntAlloc( 100 );
	return p;
	}
	void Sbd_ManCutServerStop( Sbd_Srv_t * p )
	{
	Vec_IntFree( p->vCut0 );
	Vec_IntFree( p->vCut );
	Vec_IntFree( p->vCutTop );
	Vec_IntFree( p->vCutBot );
	ABC_FREE( p );
	}

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

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	int Sbd_ManCutIsTopo_rec( Gia_Man_t * p, Vec_Int_t * vMirrors, int iObj )
	{
	Gia_Obj_t * pObj;
	int Ret0, Ret1;
	if ( Vec_IntEntry(vMirrors, iObj) >= 0 )
	iObj = Abc_Lit2Var(Vec_IntEntry(vMirrors, iObj));
	if ( !iObj \|\| Gia_ObjIsTravIdCurrentId(p, iObj) )
	return 1;
	Gia_ObjSetTravIdCurrentId(p, iObj);
	pObj = Gia_ManObj( p, iObj );
	if ( Gia_ObjIsCi(pObj) )
	return 0;
	assert( Gia_ObjIsAnd(pObj) );
	Ret0 = Sbd_ManCutIsTopo_rec( p, vMirrors, Gia_ObjFaninId0(pObj, iObj) );
	Ret1 = Sbd_ManCutIsTopo_rec( p, vMirrors, Gia_ObjFaninId1(pObj, iObj) );
	return Ret0 && Ret1;
	}
	int Sbd_ManCutIsTopo( Gia_Man_t * p, Vec_Int_t * vMirrors, Vec_Int_t * vCut, int iObj )
	{
	int i, Entry, RetValue;
	Gia_ManIncrementTravId( p );
	Vec_IntForEachEntry( vCut, Entry, i )
	Gia_ObjSetTravIdCurrentId( p, Entry );
	RetValue = Sbd_ManCutIsTopo_rec( p, vMirrors, iObj );
	if ( RetValue == 0 )
	printf( "Cut of node %d is not tological\n", iObj );
	assert( RetValue );
	return RetValue;
	}

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

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	static inline int Sbd_ManCutExpandOne( Gia_Man_t * p, Vec_Int_t * vMirrors, Vec_Int_t * vLutLevs, Vec_Int_t * vCut, int iThis, int iObj )
	{
	int Lit0m, Lit1m, Fan0, Fan1, iPlace0, iPlace1;
	int LutLev = Vec_IntEntry( vLutLevs, iObj );
	Gia_Obj_t * pObj = Gia_ManObj(p, iObj);
	if ( Gia_ObjIsCi(pObj) )
	return 0;
	assert( Gia_ObjIsAnd(pObj) );
	Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) );
	Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, iObj) );
	Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
	Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
	iPlace0 = Vec_IntFind( vCut, Fan0 );
	iPlace1 = Vec_IntFind( vCut, Fan1 );
	if ( iPlace0 == -1 && iPlace1 == -1 )
	return 0;
	if ( Vec_IntEntry(vLutLevs, Fan0) > LutLev \|\| Vec_IntEntry(vLutLevs, Fan1) > LutLev )
	return 0;
	Vec_IntDrop( vCut, iThis );
	if ( iPlace0 == -1 && Fan0 )
	Vec_IntPushOrder( vCut, Fan0 );
	if ( iPlace1 == -1 && Fan1 )
	Vec_IntPushOrder( vCut, Fan1 );
	return 1;
	}
	void Vec_IntIsOrdered( Vec_Int_t * vCut )
	{
	int i, Prev, Entry;
	Prev = Vec_IntEntry( vCut, 0 );
	Vec_IntForEachEntryStart( vCut, Entry, i, 1 )
	{
	assert( Prev < Entry );
	Prev = Entry;
	}
	}
	void Sbd_ManCutExpand( Gia_Man_t * p, Vec_Int_t * vMirrors, Vec_Int_t * vLutLevs, Vec_Int_t * vCut )
	{
	int i, Entry;
	do
	{
	Vec_IntForEachEntry( vCut, Entry, i )
	if ( Sbd_ManCutExpandOne( p, vMirrors, vLutLevs, vCut, i, Entry ) )
	break;
	}
	while ( i < Vec_IntSize(vCut) );
	}
	void Sbd_ManCutReload( Vec_Int_t * vMirrors, Vec_Int_t * vLutLevs, int LevStop, Vec_Int_t * vCut, Vec_Int_t * vCutTop, Vec_Int_t * vCutBot )
	{
	int i, Entry;
	Vec_IntClear( vCutTop );
	Vec_IntClear( vCutBot );
	Vec_IntForEachEntry( vCut, Entry, i )
	{
	assert( Entry );
	assert( Vec_IntEntry(vMirrors, Entry) == -1 );
	assert( Vec_IntEntry(vLutLevs, Entry) <= LevStop );
	if ( Vec_IntEntry(vLutLevs, Entry) == LevStop )
	Vec_IntPush( vCutTop, Entry );
	else
	Vec_IntPush( vCutBot, Entry );
	}
	Vec_IntIsOrdered( vCut );
	}
	int Sbd_ManCutCollect_rec( Gia_Man_t * p, Vec_Int_t * vMirrors, int iObj, int LevStop, Vec_Int_t * vLutLevs, Vec_Int_t * vCut )
	{
	Gia_Obj_t * pObj;
	int Ret0, Ret1;
	if ( Vec_IntEntry(vMirrors, iObj) >= 0 )
	iObj = Abc_Lit2Var(Vec_IntEntry(vMirrors, iObj));
	if ( !iObj \|\| Gia_ObjIsTravIdCurrentId(p, iObj) )
	return 1;
	Gia_ObjSetTravIdCurrentId(p, iObj);
	pObj = Gia_ManObj( p, iObj );
	if ( Gia_ObjIsCi(pObj) \|\| Vec_IntEntry(vLutLevs, iObj) <= LevStop )
	{
	Vec_IntPush( vCut, iObj );
	return Vec_IntEntry(vLutLevs, iObj) <= LevStop;
	}
	assert( Gia_ObjIsAnd(pObj) );
	Ret0 = Sbd_ManCutCollect_rec( p, vMirrors, Gia_ObjFaninId0(pObj, iObj), LevStop, vLutLevs, vCut );
	Ret1 = Sbd_ManCutCollect_rec( p, vMirrors, Gia_ObjFaninId1(pObj, iObj), LevStop, vLutLevs, vCut );
	return Ret0 && Ret1;
	}

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

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	int Sbd_ManCutReduceTop( Gia_Man_t * p, Vec_Int_t * vMirrors, int iObj, Vec_Int_t * vLutLevs, Vec_Int_t * vCut, Vec_Int_t * vCutTop, int nCutSize )
	{
	int i, Entry, Lit0m, Lit1m, Fan0, Fan1;
	int LevStop = Vec_IntEntry(vLutLevs, iObj) - 2;
	Vec_IntIsOrdered( vCut );
	Vec_IntForEachEntryReverse( vCutTop, Entry, i )
	{
	Gia_Obj_t * pObj = Gia_ManObj( p, Entry );
	if ( Gia_ObjIsCi(pObj) )
	continue;
	assert( Gia_ObjIsAnd(pObj) );
	assert( Vec_IntEntry(vLutLevs, Entry) == LevStop );
	Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, Entry) );
	Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, Entry) );
	Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, Entry);
	Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, Entry);
	if ( Vec_IntEntry(vLutLevs, Fan0) > LevStop \|\| Vec_IntEntry(vLutLevs, Fan1) > LevStop )
	continue;
	assert( Vec_IntEntry(vLutLevs, Fan0) <= LevStop );
	assert( Vec_IntEntry(vLutLevs, Fan1) <= LevStop );
	if ( Vec_IntEntry(vLutLevs, Fan0) == LevStop && Vec_IntEntry(vLutLevs, Fan1) == LevStop )
	continue;
	Vec_IntRemove( vCut, Entry );
	if ( Fan0 ) Vec_IntPushUniqueOrder( vCut, Fan0 );
	if ( Fan1 ) Vec_IntPushUniqueOrder( vCut, Fan1 );
	//Sbd_ManCutIsTopo( p, vMirrors, vCut, iObj );
	return 1;
	}
	return 0;
	}

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

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	int Sbd_ManCutServerFirst( Sbd_Srv_t * p, int iObj, int * pLeaves )
	{
	int RetValue, LevStop = Vec_IntEntry(p->vLutLevs, iObj) - 2;

	Vec_IntClear( p->vCut );
	Gia_ManIncrementTravId( p->pGia );
	RetValue = Sbd_ManCutCollect_rec( p->pGia, p->vMirrors, iObj, LevStop, p->vLutLevs, p->vCut );
	if ( RetValue == 0 ) // cannot build delay-improving cut
	return -1;
	// check if the current cut is good
	Vec_IntSort( p->vCut, 0 );
	/*
	Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
	if ( Vec_IntSize(p->vCut) <= p->nCutSize && Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
	{
	//printf( "%d ", Vec_IntSize(p->vCut) );
	memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
	return Vec_IntSize(p->vCut);
	}
	*/
	// try to expand the cut
	Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );
	Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
	if ( Vec_IntSize(p->vCut) <= p->nCutSize && Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
	{
	//printf( "1=(%d,%d) ", Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );
	//printf( "%d ", Vec_IntSize(p->vCut) );
	memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
	return Vec_IntSize(p->vCut);
	}

	// try to reduce the topmost
	Vec_IntClear( p->vCut0 );
	Vec_IntAppend( p->vCut0, p->vCut );
	if ( Vec_IntSize(p->vCut) < p->nCutSize && Sbd_ManCutReduceTop( p->pGia, p->vMirrors, iObj, p->vLutLevs, p->vCut, p->vCutTop, p->nCutSize ) )
	{
	Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );
	Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
	assert( Vec_IntSize(p->vCut) <= p->nCutSize );
	if ( Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
	{
	//printf( "%d -> %d (%d + %d)\n", Vec_IntSize(p->vCut0), Vec_IntSize(p->vCut), Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );
	memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
	return Vec_IntSize(p->vCut);
	}
	// try again
	if ( Vec_IntSize(p->vCut) < p->nCutSize && Sbd_ManCutReduceTop( p->pGia, p->vMirrors, iObj, p->vLutLevs, p->vCut, p->vCutTop, p->nCutSize ) )
	{
	Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );
	Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
	assert( Vec_IntSize(p->vCut) <= p->nCutSize );
	if ( Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
	{
	//printf( "* %d -> %d (%d + %d)\n", Vec_IntSize(p->vCut0), Vec_IntSize(p->vCut), Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );
	memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
	return Vec_IntSize(p->vCut);
	}
	// try again
	if ( Vec_IntSize(p->vCut) < p->nCutSize && Sbd_ManCutReduceTop( p->pGia, p->vMirrors, iObj, p->vLutLevs, p->vCut, p->vCutTop, p->nCutSize ) )
	{
	Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );
	Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
	assert( Vec_IntSize(p->vCut) <= p->nCutSize );
	if ( Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
	{
	//printf( "** %d -> %d (%d + %d)\n", Vec_IntSize(p->vCut0), Vec_IntSize(p->vCut), Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );
	memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
	return Vec_IntSize(p->vCut);
	}
	// try again
	if ( Vec_IntSize(p->vCut) < p->nCutSize && Sbd_ManCutReduceTop( p->pGia, p->vMirrors, iObj, p->vLutLevs, p->vCut, p->vCutTop, p->nCutSize ) )
	{
	Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );
	Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
	assert( Vec_IntSize(p->vCut) <= p->nCutSize );
	if ( Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
	{
	//printf( "*** %d -> %d (%d + %d)\n", Vec_IntSize(p->vCut0), Vec_IntSize(p->vCut), Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );
	memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
	return Vec_IntSize(p->vCut);
	}
	}
	}
	}
	}

	// recompute the cut
	Vec_IntClear( p->vCut );
	Gia_ManIncrementTravId( p->pGia );
	RetValue = Sbd_ManCutCollect_rec( p->pGia, p->vMirrors, iObj, LevStop-1, p->vLutLevs, p->vCut );
	if ( RetValue == 0 ) // cannot build delay-improving cut
	return -1;
	// check if the current cut is good
	Vec_IntSort( p->vCut, 0 );
	/*
	Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
	if ( Vec_IntSize(p->vCut) <= p->nCutSize && Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
	{
	//printf( "%d ", Vec_IntSize(p->vCut) );
	memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
	return Vec_IntSize(p->vCut);
	}
	*/
	// try to expand the cut
	Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );
	Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
	if ( Vec_IntSize(p->vCut) <= p->nCutSize && Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
	{
	//printf( "2=(%d,%d) ", Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );
	//printf( "%d ", Vec_IntSize(p->vCut) );
	memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
	return Vec_IntSize(p->vCut);
	}

	return -1;
	}

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


	ABC_NAMESPACE_IMPL_END