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

  FileName    [llb2Nonlin.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [BDD based reachability.]

  Synopsis    [Non-linear quantification scheduling.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "llbInt.h"

ABC_NAMESPACE_IMPL_START
 

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

typedef struct Llb_Mnn_t_ Llb_Mnn_t;
struct Llb_Mnn_t_
{
    Aig_Man_t *     pInit;          // AIG manager
    Aig_Man_t *     pAig;           // AIG manager
    Gia_ParLlb_t *  pPars;          // parameters

    DdManager *     dd;             // BDD manager
    DdManager *     ddG;            // BDD manager
    DdManager *     ddR;            // BDD manager
    Vec_Ptr_t *     vRings;         // onion rings in ddR

    Vec_Ptr_t *     vLeaves;        
    Vec_Ptr_t *     vRoots;
    int *           pVars2Q;
    int *           pOrderL;
    int *           pOrderL2;
    int *           pOrderG;

    Vec_Int_t *     vCs2Glo;        // cur state variables into global variables
    Vec_Int_t *     vNs2Glo;        // next state variables into global variables
    Vec_Int_t *     vGlo2Cs;        // global variables into cur state variables
    Vec_Int_t *     vGlo2Ns;        // global variables into next state variables

    int             ddLocReos;
    int             ddLocGrbs;

    abctime         timeImage;
    abctime         timeTran1;
    abctime         timeTran2;
    abctime         timeGloba;
    abctime         timeOther;
    abctime         timeTotal;
    abctime         timeReo;
    abctime         timeReoG;

};

extern abctime timeBuild, timeAndEx, timeOther;
extern int nSuppMax;

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

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

  Synopsis    [Finds variable whose 0-cofactor is the smallest.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Llb_NonlinFindBestVar( DdManager * dd, DdNode * bFunc, Aig_Man_t * pAig )
{
    int fVerbose = 0;
    Aig_Obj_t * pObj;
    DdNode * bCof, * bVar;
    int i, iVar, iVarBest = -1, iValue, iValueBest = ABC_INFINITY, Size0Best = -1;
    int Size, Size0, Size1;
    abctime clk = Abc_Clock();
    Size = Cudd_DagSize(bFunc);
//    printf( "Original = %6d.  SuppSize = %3d. Vars = %3d.\n", 
//        Size = Cudd_DagSize(bFunc), Cudd_SupportSize(dd, bFunc), Aig_ManRegNum(pAig) );
    Saig_ManForEachLo( pAig, pObj, i )
    {
        iVar = Aig_ObjId(pObj);

if ( fVerbose )
printf( "Var =%3d : ", iVar );
        bVar = Cudd_bddIthVar(dd, iVar);

        bCof = Cudd_bddAnd( dd, bFunc, Cudd_Not(bVar) );          Cudd_Ref( bCof );
        Size0 = Cudd_DagSize(bCof);
if ( fVerbose )
printf( "Supp0 =%3d  ",  Cudd_SupportSize(dd, bCof) );
if ( fVerbose )
printf( "Size0 =%6d   ", Size0 );
        Cudd_RecursiveDeref( dd, bCof );

        bCof = Cudd_bddAnd( dd, bFunc, bVar );                    Cudd_Ref( bCof );
        Size1 = Cudd_DagSize(bCof);
if ( fVerbose )
printf( "Supp1 =%3d  ",  Cudd_SupportSize(dd, bCof) );
if ( fVerbose )
printf( "Size1 =%6d   ", Size1 );
        Cudd_RecursiveDeref( dd, bCof );

        iValue = Abc_MaxInt(Size0, Size1) - Abc_MinInt(Size0, Size1) + Size0 + Size1 - Size;
if ( fVerbose )
printf( "D =%6d  ", Size0 + Size1 - Size );
if ( fVerbose )
printf( "B =%6d  ", Abc_MaxInt(Size0, Size1) - Abc_MinInt(Size0, Size1) );
if ( fVerbose )
printf( "S =%6d\n", iValue );
        if ( Size0 > 1 && Size1 > 1 && iValueBest > iValue )
        {
            iValueBest = iValue;
            iVarBest   = i;
            Size0Best  = Size0;
        }
    }
    printf( "BestVar = %4d/%4d.  Value =%6d.  Orig =%6d. Size0 =%6d. ", 
        iVarBest, Aig_ObjId(Saig_ManLo(pAig,iVarBest)), iValueBest, Size, Size0Best );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    return iVarBest;
}


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

  Synopsis    [Finds variable whose 0-cofactor is the smallest.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_NonlinTrySubsetting( DdManager * dd, DdNode * bFunc )
{
    DdNode * bNew;
    printf( "Original = %6d.  SuppSize = %3d.    ", 
        Cudd_DagSize(bFunc), Cudd_SupportSize(dd, bFunc) );
    bNew = Cudd_SubsetHeavyBranch( dd, bFunc, Cudd_SupportSize(dd, bFunc), 1000 );  Cudd_Ref( bNew );
    printf( "Result   = %6d.  SuppSize = %3d.\n", 
        Cudd_DagSize(bNew), Cudd_SupportSize(dd, bNew) );
    Cudd_RecursiveDeref( dd, bNew );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_NonlinPrepareVarMap( Llb_Mnn_t * p )
{
    Aig_Obj_t * pObjLi, * pObjLo, * pObj;
    int i, iVarLi, iVarLo;
    p->vCs2Glo = Vec_IntStartFull( Aig_ManObjNumMax(p->pAig) );
    p->vNs2Glo = Vec_IntStartFull( Aig_ManObjNumMax(p->pAig) );
    p->vGlo2Cs = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
    p->vGlo2Ns = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
    Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
    {
        iVarLi = Aig_ObjId(pObjLi);
        iVarLo = Aig_ObjId(pObjLo);
        assert( iVarLi >= 0 && iVarLi < Aig_ManObjNumMax(p->pAig) );
        assert( iVarLo >= 0 && iVarLo < Aig_ManObjNumMax(p->pAig) );
        Vec_IntWriteEntry( p->vCs2Glo, iVarLo, i );
        Vec_IntWriteEntry( p->vNs2Glo, iVarLi, i );
        Vec_IntWriteEntry( p->vGlo2Cs, i, iVarLo );
        Vec_IntWriteEntry( p->vGlo2Ns, i, iVarLi );
    }
    // add mapping of the PIs
    Saig_ManForEachPi( p->pAig, pObj, i )
    {
        Vec_IntWriteEntry( p->vCs2Glo, Aig_ObjId(pObj), Aig_ManRegNum(p->pAig)+i );
        Vec_IntWriteEntry( p->vNs2Glo, Aig_ObjId(pObj), Aig_ManRegNum(p->pAig)+i );
    }
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd )
{
    Aig_Obj_t * pObj;
    DdNode * bRes, * bVar, * bTemp;
    int i, iVar;
    abctime TimeStop;
    TimeStop = dd->TimeStop;  dd->TimeStop = 0;
    bRes = Cudd_ReadOne( dd );   Cudd_Ref( bRes );
    Saig_ManForEachLo( pAig, pObj, i )
    {
        iVar = (Cudd_ReadSize(dd) == Aig_ManRegNum(pAig)) ? i : Aig_ObjId(pObj);
        bVar = Cudd_bddIthVar( dd, iVar );
        bRes = Cudd_bddAnd( dd, bTemp = bRes, Cudd_Not(bVar) );  Cudd_Ref( bRes );
        Cudd_RecursiveDeref( dd, bTemp );
    }
    Cudd_Deref( bRes );
    dd->TimeStop = TimeStop;
    return bRes;
}


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

  Synopsis    [Derives counter-example by backward reachability.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p )
{
    Abc_Cex_t * pCex;
    Aig_Obj_t * pObj;
    Vec_Int_t * vVarsNs;
    DdNode * bState = NULL, * bImage, * bOneCube, * bTemp, * bRing;
    int i, v, RetValue, nPiOffset;
    char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) );
    assert( Vec_PtrSize(p->vRings) > 0 );

    p->dd->TimeStop  = 0;
    p->ddR->TimeStop = 0;

    // update quantifiable vars
    memset( p->pVars2Q, 0, sizeof(int) * Cudd_ReadSize(p->dd) );
    vVarsNs = Vec_IntAlloc( Aig_ManRegNum(p->pAig) );
    Saig_ManForEachLi( p->pAig, pObj, i )
    {
        p->pVars2Q[Aig_ObjId(pObj)] = 1;
        Vec_IntPush( vVarsNs, Aig_ObjId(pObj) );
    }
/*
    Saig_ManForEachLo( p->pAig, pObj, i )
        printf( "%d ", pObj->Id );
    printf( "\n" );
    Saig_ManForEachLi( p->pAig, pObj, i )
        printf( "%d(%d) ", pObj->Id, Aig_ObjFaninId0(pObj) );
    printf( "\n" );
*/
    // allocate room for the counter-example
    pCex = Abc_CexAlloc( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
    pCex->iFrame = Vec_PtrSize(p->vRings) - 1;
    pCex->iPo = -1;

    // get the last cube
    bOneCube = Cudd_bddIntersect( p->ddR, (DdNode *)Vec_PtrEntryLast(p->vRings), p->ddR->bFunc );  Cudd_Ref( bOneCube );
    RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
    Cudd_RecursiveDeref( p->ddR, bOneCube );
    assert( RetValue );

    // write PIs of counter-example
    nPiOffset = Saig_ManRegNum(p->pAig) + Saig_ManPiNum(p->pAig) * (Vec_PtrSize(p->vRings) - 1);
    Saig_ManForEachPi( p->pAig, pObj, i )
        if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
            Abc_InfoSetBit( pCex->pData, nPiOffset + i );

    // write state in terms of NS variables
    if ( Vec_PtrSize(p->vRings) > 1 )
    {
        bState = Llb_CoreComputeCube( p->dd, vVarsNs, 1, pValues );   Cudd_Ref( bState );
    }
    // perform backward analysis
    Vec_PtrForEachEntryReverse( DdNode *, p->vRings, bRing, v )
    { 
        if ( v == Vec_PtrSize(p->vRings) - 1 )
            continue;
//Extra_bddPrintSupport( p->dd, bState );  printf( "\n" );
//Extra_bddPrintSupport( p->dd, bRing );   printf( "\n" );
        // compute the next states
        bImage = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bState, 
            p->pPars->fReorder, p->pPars->fVeryVerbose, NULL ); // consumed reference
        assert( bImage != NULL );
        Cudd_Ref( bImage );
//Extra_bddPrintSupport( p->dd, bImage );  printf( "\n" );

        // move reached states into ring manager
        bImage = Extra_TransferPermute( p->dd, p->ddR, bTemp = bImage, Vec_IntArray(p->vCs2Glo) );    Cudd_Ref( bImage );
        Cudd_RecursiveDeref( p->dd, bTemp );

        // intersect with the previous set
        bOneCube = Cudd_bddIntersect( p->ddR, bImage, bRing );                Cudd_Ref( bOneCube );
        Cudd_RecursiveDeref( p->ddR, bImage );

        // find any assignment of the BDD
        RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
        Cudd_RecursiveDeref( p->ddR, bOneCube );
        assert( RetValue );

        // write PIs of counter-example
        nPiOffset -= Saig_ManPiNum(p->pAig);
        Saig_ManForEachPi( p->pAig, pObj, i )
            if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
                Abc_InfoSetBit( pCex->pData, nPiOffset + i );

        // check that we get the init state
        if ( v == 0 )
        {
            Saig_ManForEachLo( p->pAig, pObj, i )
                assert( pValues[i] == 0 );
            break;
        }

        // write state in terms of NS variables
        bState = Llb_CoreComputeCube( p->dd, vVarsNs, 1, pValues );   Cudd_Ref( bState );
    }
    assert( nPiOffset == Saig_ManRegNum(p->pAig) );
    // update the output number
//Abc_CexPrint( pCex );
    RetValue = Saig_ManFindFailedPoCex( p->pInit, pCex );
    assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pInit) ); // invalid CEX!!!
    pCex->iPo = RetValue;
    // cleanup
    ABC_FREE( pValues );
    Vec_IntFree( vVarsNs );
    return pCex;
}


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

  Synopsis    [Perform reachability with hints.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Llb_NonlinReoHook( DdManager * dd, char * Type, void * Method )
{
    Aig_Man_t * pAig = (Aig_Man_t *)dd->bFunc;
    Aig_Obj_t * pObj;
    int i;
    printf( "Order: " );
    for ( i = 0; i < Cudd_ReadSize(dd); i++ )
    {
        pObj = Aig_ManObj( pAig, i );
        if ( pObj == NULL )
            continue;
        if ( Saig_ObjIsPi(pAig, pObj) )
            printf( "pi" );
        else if ( Saig_ObjIsLo(pAig, pObj) )
            printf( "lo" );
        else if ( Saig_ObjIsPo(pAig, pObj) )
            printf( "po" );
        else if ( Saig_ObjIsLi(pAig, pObj) )
            printf( "li" );
        else continue;
        printf( "%d=%d ", i, dd->perm[i] );
    }
    printf( "\n" );
    return 1;
}

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

  Synopsis    [Perform reachability with hints.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Llb_NonlinCompPerms( DdManager * dd, int * pVar2Lev )
{
    DdSubtable * pSubt;
    int i, Sum = 0, Entry;
    for ( i = 0; i < dd->size; i++ )
    {
        pSubt = &(dd->subtables[dd->perm[i]]);
        if ( pSubt->keys == pSubt->dead + 1 )
            continue;
        Entry = Abc_MaxInt(dd->perm[i], pVar2Lev[i]) - Abc_MinInt(dd->perm[i], pVar2Lev[i]);
        Sum += Entry;
//printf( "%d-%d(%d) ", dd->perm[i], pV2L[i], Entry );
    }
    return Sum;
}

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

  Synopsis    [Perform reachability with hints.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Llb_NonlinReachability( Llb_Mnn_t * p )
{ 
    DdNode * bTemp, * bNext;
    int nIters, nBddSize0, nBddSize = -1, NumCmp;//, Limit = p->pPars->nBddMax;
    abctime clk2, clk3, clk = Abc_Clock();
    assert( Aig_ManRegNum(p->pAig) > 0 );

    // compute time to stop
    p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;

    // set the stop time parameter
    p->dd->TimeStop  = p->pPars->TimeTarget;
    p->ddG->TimeStop = p->pPars->TimeTarget;
    p->ddR->TimeStop = p->pPars->TimeTarget;

    // set reordering hooks
    assert( p->dd->bFunc == NULL );
//    p->dd->bFunc = (DdNode *)p->pAig;
//    Cudd_AddHook( p->dd, Llb_NonlinReoHook, CUDD_POST_REORDERING_HOOK );

    // create bad state in the ring manager
    p->ddR->bFunc  = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeTarget );          
    if ( p->ddR->bFunc == NULL )
    {
        if ( !p->pPars->fSilent )
            printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
        p->pPars->iFrame = -1;
        return -1;
    }
    Cudd_Ref( p->ddR->bFunc );
    // compute the starting set of states
    Cudd_Quit( p->dd );
    p->dd = Llb_NonlinImageStart( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->pOrderL, 1, p->pPars->TimeTarget );
    if ( p->dd == NULL )
    {
        if ( !p->pPars->fSilent )
            printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
        p->pPars->iFrame = -1;
        return -1;
    }
    p->dd->bFunc   = Llb_NonlinComputeInitState( p->pAig, p->dd );   Cudd_Ref( p->dd->bFunc );   // current
    p->ddG->bFunc  = Llb_NonlinComputeInitState( p->pAig, p->ddG );  Cudd_Ref( p->ddG->bFunc );  // reached
    p->ddG->bFunc2 = Llb_NonlinComputeInitState( p->pAig, p->ddG );  Cudd_Ref( p->ddG->bFunc2 ); // frontier 
    for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ )
    { 
        // check the runtime limit
        clk2 = Abc_Clock();
        if ( p->pPars->TimeLimit && Abc_Clock() > p->pPars->TimeTarget )
        {
            if ( !p->pPars->fSilent )
                printf( "Reached timeout (%d seconds) during image computation.\n",  p->pPars->TimeLimit );
            p->pPars->iFrame = nIters - 1;
            Llb_NonlinImageQuit();
            return -1;
        }

        // save the onion ring
        bTemp = Extra_TransferPermute( p->dd, p->ddR, p->dd->bFunc, Vec_IntArray(p->vCs2Glo) );
        if ( bTemp == NULL )
        {
            if ( !p->pPars->fSilent )
                printf( "Reached timeout (%d seconds) during ring transfer.\n",  p->pPars->TimeLimit );
            p->pPars->iFrame = nIters - 1;
            Llb_NonlinImageQuit();
            return -1;
        }
        Cudd_Ref( bTemp );
        Vec_PtrPush( p->vRings, bTemp );

        // check it for bad states
        if ( !p->pPars->fSkipOutCheck && !Cudd_bddLeq( p->ddR, bTemp, Cudd_Not(p->ddR->bFunc) ) ) 
        {
            assert( p->pInit->pSeqModel == NULL );
            if ( !p->pPars->fBackward )
                p->pInit->pSeqModel = Llb_NonlinDeriveCex( p ); 
            if ( !p->pPars->fSilent )
            {
                if ( !p->pPars->fBackward )
                    Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", p->pInit->pSeqModel->iPo, nIters );
                else
                    Abc_Print( 1, "Output ??? was asserted in frame %d (counter-example is not produced).  ", nIters );
                Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
            }
            p->pPars->iFrame = nIters - 1;
            Llb_NonlinImageQuit();
            return 0;
        }

        // compute the next states
        clk3 = Abc_Clock();
        nBddSize0 = Cudd_DagSize( p->dd->bFunc );
        bNext = Llb_NonlinImageCompute( p->dd->bFunc, p->pPars->fReorder, 0, 1, p->pOrderL ); // consumes ref   
//        bNext = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bCurrent, 
//            p->pPars->fReorder, p->pPars->fVeryVerbose, NULL, ABC_INFINITY, p->pPars->TimeTarget );
        if ( bNext == NULL )
        {
            if ( !p->pPars->fSilent )
                printf( "Reached timeout (%d seconds) during image computation in quantification.\n",  p->pPars->TimeLimit );
            p->pPars->iFrame = nIters - 1;
            Llb_NonlinImageQuit();
            return -1;
        }
        Cudd_Ref( bNext );
        nBddSize = Cudd_DagSize( bNext );
        p->timeImage += Abc_Clock() - clk3;


        // transfer to the state manager
        clk3 = Abc_Clock();
        Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 );
        p->ddG->bFunc2 = Extra_TransferPermute( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo) );    
//        p->ddG->bFunc2 = Extra_bddAndPermute( p->ddG, Cudd_Not(p->ddG->bFunc), p->dd, bNext, Vec_IntArray(p->vNs2Glo) );    
        if ( p->ddG->bFunc2 == NULL )
        {
            if ( !p->pPars->fSilent )
                printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n",  p->pPars->TimeLimit );
            p->pPars->iFrame = nIters - 1;
            Cudd_RecursiveDeref( p->dd,  bNext );  
            Llb_NonlinImageQuit();
            return -1;
        }
        Cudd_Ref( p->ddG->bFunc2 );
        Cudd_RecursiveDeref( p->dd, bNext );
        p->timeTran1 += Abc_Clock() - clk3;

        // save permutation
        NumCmp = Llb_NonlinCompPerms( p->dd, p->pOrderL2 );
        // save order before image computation
        memcpy( p->pOrderL2, p->dd->perm, sizeof(int) * p->dd->size );
        // update the image computation manager
        p->timeReo   += Cudd_ReadReorderingTime(p->dd);
        p->ddLocReos += Cudd_ReadReorderings(p->dd);
        p->ddLocGrbs += Cudd_ReadGarbageCollections(p->dd);
        Llb_NonlinImageQuit();
        p->dd = Llb_NonlinImageStart( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->pOrderL, 0, p->pPars->TimeTarget );
        if ( p->dd == NULL )
        {
            if ( !p->pPars->fSilent )
                printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
            p->pPars->iFrame = nIters - 1;
            return -1;
        }
        //Extra_TestAndPerm( p->ddG, Cudd_Not(p->ddG->bFunc), p->ddG->bFunc2 );    

        // derive new states
        clk3 = Abc_Clock();
        p->ddG->bFunc2 = Cudd_bddAnd( p->ddG, bTemp = p->ddG->bFunc2, Cudd_Not(p->ddG->bFunc) );     
        if ( p->ddG->bFunc2 == NULL )
        {
            if ( !p->pPars->fSilent )
                printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n",  p->pPars->TimeLimit );
            p->pPars->iFrame = nIters - 1;
            Cudd_RecursiveDeref( p->ddG, bTemp );  
            Llb_NonlinImageQuit();
            return -1;
        }
        Cudd_Ref( p->ddG->bFunc2 );
        Cudd_RecursiveDeref( p->ddG, bTemp );
        p->timeGloba += Abc_Clock() - clk3;

        if ( Cudd_IsConstant(p->ddG->bFunc2) )
            break;
        // add to the reached set
        clk3 = Abc_Clock();
        p->ddG->bFunc = Cudd_bddOr( p->ddG, bTemp = p->ddG->bFunc, p->ddG->bFunc2 );                 
        if ( p->ddG->bFunc == NULL )
        {
            if ( !p->pPars->fSilent )
                printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n",  p->pPars->TimeLimit );
            p->pPars->iFrame = nIters - 1;
            Cudd_RecursiveDeref( p->ddG, bTemp );  
            Llb_NonlinImageQuit();
            return -1;
        }
        Cudd_Ref( p->ddG->bFunc );
        Cudd_RecursiveDeref( p->ddG, bTemp );
        p->timeGloba += Abc_Clock() - clk3;

        // reset permutation
//        RetValue = Cudd_CheckZeroRef( dd );
//        assert( RetValue == 0 );
//        Cudd_ShuffleHeap( dd, pOrderG );

        // move new states to the working manager
        clk3 = Abc_Clock();
        p->dd->bFunc = Extra_TransferPermute( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs) ); 
        if ( p->dd->bFunc == NULL )
        {
            if ( !p->pPars->fSilent )
                printf( "Reached timeout (%d seconds) during image computation in transfer 2.\n",  p->pPars->TimeLimit );
            p->pPars->iFrame = nIters - 1;
            Llb_NonlinImageQuit();
            return -1;
        }
        Cudd_Ref( p->dd->bFunc );
        p->timeTran2 += Abc_Clock() - clk3;

        // report the results
        if ( p->pPars->fVerbose )
        {
            printf( "I =%3d : ",   nIters );
            printf( "Fr =%7d ",    nBddSize0 );
            printf( "Im =%7d  ",   nBddSize );
            printf( "(%4d %4d)  ", p->ddLocReos, p->ddLocGrbs );
            printf( "Rea =%6d  ",  Cudd_DagSize(p->ddG->bFunc) );
            printf( "(%4d %4d)  ", Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) );
            printf( "S =%4d ",     nSuppMax );
            printf( "cL =%5d ",    NumCmp );
            printf( "cG =%5d ",    Llb_NonlinCompPerms( p->ddG, p->pOrderG ) );
            Abc_PrintTime( 1, "T", Abc_Clock() - clk2 );
            memcpy( p->pOrderG, p->ddG->perm, sizeof(int) * p->ddG->size );
        }
/*
        if ( pPars->fVerbose )
        {
            double nMints = Cudd_CountMinterm(ddG, bReached, Saig_ManRegNum(pAig) );
//            Extra_bddPrint( ddG, bReached );printf( "\n" );
            printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(pAig)) );
            fflush( stdout ); 
        }
*/
        if ( nIters == p->pPars->nIterMax - 1 )
        {
            if ( !p->pPars->fSilent )
                printf( "Reached limit on the number of timeframes (%d).\n",  p->pPars->nIterMax );
            p->pPars->iFrame = nIters;
            Llb_NonlinImageQuit();
            return -1;
        }
    }
    Llb_NonlinImageQuit();
    
    // report the stats
    if ( p->pPars->fVerbose )
    {
        double nMints = Cudd_CountMinterm(p->ddG, p->ddG->bFunc, Saig_ManRegNum(p->pAig) );
        if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax )
            printf( "Reachability analysis is stopped after %d frames.\n", nIters );
        else
            printf( "Reachability analysis completed after %d frames.\n", nIters );
        printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
        fflush( stdout ); 
    }
    if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax )
    {
        if ( !p->pPars->fSilent )
            printf( "Verified only for states reachable in %d frames.  ", nIters );
        p->pPars->iFrame = p->pPars->nIterMax;
        return -1; // undecided
    }
    // report
    if ( !p->pPars->fSilent )
        printf( "The miter is proved unreachable after %d iterations.  ", nIters );
    p->pPars->iFrame = nIters - 1;
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    return 1; // unreachable
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Llb_Mnn_t * Llb_MnnStart( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t *  pPars )
{
    Llb_Mnn_t * p;
    Aig_Obj_t * pObj;
    int i;
    p = ABC_CALLOC( Llb_Mnn_t, 1 );
    p->pInit = pInit;
    p->pAig  = pAig;
    p->pPars = pPars;
    p->dd    = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
    p->ddG   = Cudd_Init( Aig_ManRegNum(pAig),    0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
    p->ddR   = Cudd_Init( Aig_ManCiNum(pAig),     0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
    Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
    Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT );
    Cudd_AutodynEnable( p->ddR, CUDD_REORDER_SYMM_SIFT );
    p->vRings = Vec_PtrAlloc( 100 );
    // create leaves
    p->vLeaves = Vec_PtrAlloc( Aig_ManCiNum(pAig) );
    Aig_ManForEachCi( pAig, pObj, i )
        Vec_PtrPush( p->vLeaves, pObj );
    // create roots
    p->vRoots = Vec_PtrAlloc( Aig_ManCoNum(pAig) );
    Saig_ManForEachLi( pAig, pObj, i )
        Vec_PtrPush( p->vRoots, pObj );
    // variables to quantify
    p->pOrderL = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
    p->pOrderL2= ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
    p->pOrderG = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
    p->pVars2Q = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
    Aig_ManForEachCi( pAig, pObj, i )
        p->pVars2Q[Aig_ObjId(pObj)] = 1;
    for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
        p->pOrderL[i] = p->pOrderL2[i] = p->pOrderG[i] = i;
    Llb_NonlinPrepareVarMap( p ); 
    return p;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_MnnStop( Llb_Mnn_t * p )
{
    DdNode * bTemp;
    int i;
    if ( p->pPars->fVerbose ) 
    {
        p->timeOther = p->timeTotal - p->timeImage - p->timeTran1 - p->timeTran2 - p->timeGloba;
        p->timeReoG  = Cudd_ReadReorderingTime(p->ddG);
        ABC_PRTP( "Image    ", p->timeImage, p->timeTotal );
        ABC_PRTP( "  build  ",    timeBuild, p->timeTotal );
        ABC_PRTP( "  and-ex ",    timeAndEx, p->timeTotal );
        ABC_PRTP( "  other  ",    timeOther, p->timeTotal );
        ABC_PRTP( "Transfer1", p->timeTran1, p->timeTotal );
        ABC_PRTP( "Transfer2", p->timeTran2, p->timeTotal );
        ABC_PRTP( "Global   ", p->timeGloba, p->timeTotal );
        ABC_PRTP( "Other    ", p->timeOther, p->timeTotal );
        ABC_PRTP( "TOTAL    ", p->timeTotal, p->timeTotal );
        ABC_PRTP( "  reo    ", p->timeReo,   p->timeTotal );
        ABC_PRTP( "  reoG   ", p->timeReoG,  p->timeTotal );
    }
    if ( p->ddR->bFunc )
        Cudd_RecursiveDeref( p->ddR, p->ddR->bFunc );
    Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
        Cudd_RecursiveDeref( p->ddR, bTemp );
    Vec_PtrFree( p->vRings );
    if ( p->ddG->bFunc )
        Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc );
    if ( p->ddG->bFunc2 )
        Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 );
//    printf( "manager1\n" );
//    Extra_StopManager( p->dd );
//    printf( "manager2\n" );
    Extra_StopManager( p->ddG );
//    printf( "manager3\n" );
    Extra_StopManager( p->ddR );
    Vec_IntFreeP( &p->vCs2Glo );
    Vec_IntFreeP( &p->vNs2Glo );
    Vec_IntFreeP( &p->vGlo2Cs );
    Vec_IntFreeP( &p->vGlo2Ns );
    Vec_PtrFree( p->vLeaves );
    Vec_PtrFree( p->vRoots );
    ABC_FREE( p->pVars2Q );
    ABC_FREE( p->pOrderL );
    ABC_FREE( p->pOrderL2 );
    ABC_FREE( p->pOrderG );
    ABC_FREE( p );
}


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

  Synopsis    [Finds balanced cut.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_NonlinExperiment( Aig_Man_t * pAig, int Num )
{
    Llb_Mnn_t * pMnn;
    Gia_ParLlb_t Pars, * pPars = &Pars;
    Aig_Man_t * p;
    abctime clk = Abc_Clock();

    Llb_ManSetDefaultParams( pPars );
    pPars->fVerbose = 1;

    p = Aig_ManDupFlopsOnly( pAig );
//Aig_ManShow( p, 0, NULL );
    Aig_ManPrintStats( pAig );
    Aig_ManPrintStats( p );

    pMnn = Llb_MnnStart( pAig, p, pPars );
    Llb_NonlinReachability( pMnn );
    pMnn->timeTotal = Abc_Clock() - clk;
    Llb_MnnStop( pMnn );

    Aig_ManStop( p );
}

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

  Synopsis    [Finds balanced cut.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Llb_NonlinCoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
{
    Llb_Mnn_t * pMnn;
    Aig_Man_t * p;
    int RetValue = -1;

    p = Aig_ManDupFlopsOnly( pAig );
//Aig_ManShow( p, 0, NULL );
    if ( pPars->fVerbose )
    Aig_ManPrintStats( pAig );
    if ( pPars->fVerbose )
    Aig_ManPrintStats( p );

    if ( !pPars->fSkipReach )
    {
        abctime clk = Abc_Clock();
        pMnn = Llb_MnnStart( pAig, p, pPars );
        RetValue = Llb_NonlinReachability( pMnn );
        pMnn->timeTotal = Abc_Clock() - clk;
        Llb_MnnStop( pMnn );
    }

    Aig_ManStop( p );
    return RetValue;
}

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


ABC_NAMESPACE_IMPL_END