/**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_Mnx_t_ Llb_Mnx_t;
struct Llb_Mnx_t_
{
    // user info
    Aig_Man_t *     pAig;           // AIG manager
    Gia_ParLlb_t *  pPars;          // parameters

    // intermediate BDDs
    DdManager *     dd;             // BDD manager
    DdNode *        bBad;           // bad states in terms of CIs
    DdNode *        bReached;       // reached states 
    DdNode *        bCurrent;       // from states
    DdNode *        bNext;          // to states
    Vec_Ptr_t *     vRings;         // onion rings in ddR
    Vec_Ptr_t *     vRoots;         // BDDs for partitions

    // structural info
    Vec_Int_t *     vOrder;         // for each object ID, its BDD variable number or -1
    Vec_Int_t *     vVars2Q;        // 1 if variable is quantifiable; 0 othervise

    int             timeImage;
    int             timeRemap;
    int             timeReo;
    int             timeOther;
    int             timeTotal;
};

static inline int Llb_MnxBddVar( Vec_Int_t * vOrder, Aig_Obj_t * pObj ) { return Vec_IntEntry(vOrder, Aig_ObjId(pObj)); }

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

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////
 
/**Function*************************************************************

  Synopsis    [Computes bad in working manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * Llb_Nonlin4ComputeBad( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
{
    Vec_Ptr_t * vNodes;
    DdNode * bBdd, * bBdd0, * bBdd1, * bTemp, * bResult;
    Aig_Obj_t * pObj;
    int i;
    Aig_ManCleanData( pAig );
    // assign elementary variables
    Aig_ManConst1(pAig)->pData = Cudd_ReadOne(dd); 
    Aig_ManForEachPi( pAig, pObj, i )
        pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) );
    // compute internal nodes
    vNodes = Aig_ManDfsNodes( pAig, (Aig_Obj_t **)Vec_PtrArray(pAig->vPos), Saig_ManPoNum(pAig) );
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
    {
        if ( !Aig_ObjIsNode(pObj) )
            continue;
        bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
        bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
        bBdd  = Cudd_bddAnd( dd, bBdd0, bBdd1 );
        if ( bBdd == NULL )
        {
            Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
                if ( Aig_ObjIsNode(pObj) && pObj->pData != NULL )
                    Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
            Vec_PtrFree( vNodes );
            return NULL;
        }
        Cudd_Ref( bBdd );
        pObj->pData = bBdd;
    }
    // quantify PIs of each PO
    bResult = Cudd_ReadLogicZero( dd );  Cudd_Ref( bResult );
    Saig_ManForEachPo( pAig, pObj, i )
    {
        bBdd0   = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
        bResult = Cudd_bddOr( dd, bTemp = bResult, bBdd0 );     
        if ( bResult == NULL )
        {
            Cudd_RecursiveDeref( dd, bTemp );
            break;
        }
        Cudd_Ref( bResult );
        Cudd_RecursiveDeref( dd, bTemp );
    }
    // deref
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
        if ( Aig_ObjIsNode(pObj) && pObj->pData != NULL )
            Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
    Vec_PtrFree( vNodes );
    if ( bResult )
        Cudd_Deref( bResult );
//if ( bResult )
//printf( "Bad state = %d.\n", Cudd_DagSize(bResult) );
    return bResult;
}

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

  Synopsis    [Derives BDDs for the partitions.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Ptr_t * Llb_Nonlin4DerivePartitions( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
{
    Vec_Ptr_t * vRoots;
    Aig_Obj_t * pObj;
    DdNode * bBdd, * bBdd0, * bBdd1, * bPart;
    int i;
    Aig_ManCleanData( pAig );
    // assign elementary variables
    Aig_ManConst1(pAig)->pData = Cudd_ReadOne(dd); 
    Aig_ManForEachPi( pAig, pObj, i )
        pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) );
    Aig_ManForEachNode( pAig, pObj, i )
        if ( Llb_MnxBddVar(vOrder, pObj) >= 0 )
        {
            pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) );
            Cudd_Ref( (DdNode *)pObj->pData );
        }
    Saig_ManForEachLi( pAig, pObj, i )
        pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) );
    // compute intermediate BDDs
    vRoots = Vec_PtrAlloc( 100 );
    Aig_ManForEachNode( pAig, pObj, i )
    {
        bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
        bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
        bBdd  = Cudd_bddAnd( dd, bBdd0, bBdd1 );
        if ( bBdd == NULL )
            goto finish;
        Cudd_Ref( bBdd );
        if ( pObj->pData == NULL )
        {
            pObj->pData = bBdd;
            continue;
        }
        // create new partition
        bPart = Cudd_bddXnor( dd, (DdNode *)pObj->pData, bBdd );  
        if ( bPart == NULL )
            goto finish;
        Cudd_Ref( bPart );
        Cudd_RecursiveDeref( dd, bBdd );
        Vec_PtrPush( vRoots, bPart );
//printf( "%d ", Cudd_DagSize(bPart) );
    }
    // compute register output BDDs
    Saig_ManForEachLi( pAig, pObj, i )
    {
        bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
        bPart = Cudd_bddXnor( dd, (DdNode *)pObj->pData, bBdd0 );  
        if ( bPart == NULL )
            goto finish;
        Cudd_Ref( bPart );
        Vec_PtrPush( vRoots, bPart );
//printf( "%d ", Cudd_DagSize(bPart) );
    }
//printf( "\n" );
    Aig_ManForEachNode( pAig, pObj, i )
        Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
    return vRoots;
    // early termination
finish:
    Aig_ManForEachNode( pAig, pObj, i )
        if ( pObj->pData )
            Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
    Vec_PtrForEachEntry( DdNode *, vRoots, bPart, i )
        Cudd_RecursiveDeref( dd, bPart );
    Vec_PtrFree( vRoots );
    return NULL;
}

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

  Synopsis    [Find simple variable ordering.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Llb_Nonlin4CreateOrderSimple( Aig_Man_t * pAig )
{
    Vec_Int_t * vOrder;
    Aig_Obj_t * pObj;
    int i, Counter = 0;
    vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
    Aig_ManForEachPi( pAig, pObj, i )
        Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
    Saig_ManForEachLi( pAig, pObj, i )
        Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
    return vOrder;
}

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

  Synopsis    [Find good static variable ordering.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_Nonlin4CreateOrderSmart_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vOrder, int * pCounter )
{
    Aig_Obj_t * pFanin0, * pFanin1;
    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
        return;
    Aig_ObjSetTravIdCurrent( pAig, pObj );
    assert( Llb_MnxBddVar(vOrder, pObj) < 0 );
    if ( Aig_ObjIsPi(pObj) )
    {
        Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
        return;
    }
    // try fanins with higher level first
    pFanin0 = Aig_ObjFanin0(pObj);
    pFanin1 = Aig_ObjFanin1(pObj);
//    if ( pFanin0->Level > pFanin1->Level || (pFanin0->Level == pFanin1->Level && pFanin0->Id < pFanin1->Id) )
    if ( pFanin0->Level > pFanin1->Level )
    {
        Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin0, vOrder, pCounter );
        Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin1, vOrder, pCounter );
    }
    else
    {
        Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin1, vOrder, pCounter );
        Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin0, vOrder, pCounter );
    }
    if ( pObj->fMarkA )
        Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
}

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

  Synopsis    [Collect nodes with the given fanout count.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Llb_Nonlin4CollectHighRefNodes( Aig_Man_t * pAig, int nFans )
{
    Vec_Int_t * vNodes;
    Aig_Obj_t * pObj;
    int i;
    Aig_ManCleanMarkA( pAig );
    Aig_ManForEachNode( pAig, pObj, i )
        if ( Aig_ObjRefs(pObj) >= nFans )
            pObj->fMarkA = 1;
    // unmark flop drivers
    Saig_ManForEachLi( pAig, pObj, i )
        Aig_ObjFanin0(pObj)->fMarkA = 0;
    // collect mapping
    vNodes = Vec_IntAlloc( 100 );
    Aig_ManForEachNode( pAig, pObj, i )
        if ( pObj->fMarkA )
            Vec_IntPush( vNodes, Aig_ObjId(pObj) );
    Aig_ManCleanMarkA( pAig );
    return vNodes;
}

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

  Synopsis    [Find good static variable ordering.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Llb_Nonlin4CreateOrderSmart( Aig_Man_t * pAig )
{
    Vec_Int_t * vNodes = NULL;
    Vec_Int_t * vOrder;
    Aig_Obj_t * pObj;
    int i, Counter = 0;
/*
    // mark internal nodes to be used
    Aig_ManCleanMarkA( pAig );
    vNodes = Llb_Nonlin4CollectHighRefNodes( pAig, 4 );
    Aig_ManForEachNodeVec( pAig, vNodes, pObj, i )
        pObj->fMarkA = 1;
printf( "Techmapping added %d pivots.\n", Vec_IntSize(vNodes) );
*/

    // collect nodes in the order
    vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
    Aig_ManIncrementTravId( pAig );
    Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
    Saig_ManForEachLi( pAig, pObj, i )
    {
        Llb_Nonlin4CreateOrderSmart_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter );
        Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
    }
    Aig_ManForEachPi( pAig, pObj, i )
        if ( Llb_MnxBddVar(vOrder, pObj) < 0 )
            Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
    assert( Counter <= Aig_ManPiNum(pAig) + Aig_ManRegNum(pAig) + (vNodes?Vec_IntSize(vNodes):0) );
    Aig_ManCleanMarkA( pAig );
    Vec_IntFreeP( &vNodes );
    return vOrder;
}


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

  Synopsis    [Creates quantifiable varaibles for both types of traversal.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Llb_Nonlin4CreateVars2Q( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, int fForward )
{
    Vec_Int_t * vVars2Q;
    Aig_Obj_t * pObj;
    int i;
    vVars2Q = Vec_IntAlloc( 0 );
    Vec_IntFill( vVars2Q, Cudd_ReadSize(dd), 1 );
    if ( fForward )
    {
        Saig_ManForEachLi( pAig, pObj, i )
            Vec_IntWriteEntry( vVars2Q, Llb_MnxBddVar(vOrder, pObj), 0 );
    }
    else
    {
        Aig_ManForEachPi( pAig, pObj, i )
            Vec_IntWriteEntry( vVars2Q, Llb_MnxBddVar(vOrder, pObj), 0 );
    }
    return vVars2Q;
}

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

  Synopsis    [Compute initial state in terms of current state variables.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_Nonlin4SetupVarMap( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
{
    DdNode ** pVarsX, ** pVarsY;
    Aig_Obj_t * pObjLo, * pObjLi;
    int i;
    pVarsX = ABC_ALLOC( DdNode *, Cudd_ReadSize(dd) );
    pVarsY = ABC_ALLOC( DdNode *, Cudd_ReadSize(dd) );
    Saig_ManForEachLiLo( pAig, pObjLo, pObjLi, i )
    {
        pVarsX[i] = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObjLo) );
        pVarsY[i] = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObjLi) );
    }
    Cudd_SetVarMap( dd, pVarsX, pVarsY, Aig_ManRegNum(pAig) );
    ABC_FREE( pVarsX );
    ABC_FREE( pVarsY );
}

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

  Synopsis    [Compute initial state in terms of current state variables.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * Llb_Nonlin4ComputeInitState( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
{
    Aig_Obj_t * pObj;
    DdNode * bRes, * bVar, * bTemp;
    int i, TimeStop;
    TimeStop = dd->TimeStop;  dd->TimeStop = 0;
    bRes = Cudd_ReadOne( dd );   Cudd_Ref( bRes );
    Saig_ManForEachLo( pAig, pObj, i )
    {
        bVar = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) );
        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    [Compute initial state in terms of current state variables.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * Llb_Nonlin4ComputeCube( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, char * pValues )
{
    Aig_Obj_t * pObj, * pObjLi;
    DdNode * bRes, * bVar, * bTemp;
    int i, TimeStop;
    TimeStop = dd->TimeStop;  dd->TimeStop = 0;
    bRes = Cudd_ReadOne( dd );   Cudd_Ref( bRes );
    Saig_ManForEachLo( pAig, pObj, i )
    {
        if ( pValues[Llb_MnxBddVar(vOrder, pObj)] == 2 )
            continue;
        // get the correspoding flop input variable
        pObjLi = Saig_ObjLoToLi(pAig, pObj);
        bVar = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObjLi) );
        if ( pValues[Llb_MnxBddVar(vOrder, pObj)] == 0 )
            bVar = Cudd_Not(bVar);
        // create cube
        bRes = Cudd_bddAnd( dd, bTemp = bRes, 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_Nonlin4DeriveCex( Llb_Mnx_t * p )
{
    Abc_Cex_t * pCex;
    Aig_Obj_t * pObj;
    DdNode * bState, * bImage, * bOneCube, * bRing;
    int i, v, RetValue, nPiOffset;
    char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->dd) );
    assert( Vec_PtrSize(p->vRings) > 0 );
    // disable the timeout
    p->dd->TimeStop  = 0;

    // update quantifiable vars
    Vec_IntFreeP( &p->vVars2Q );
    p->vVars2Q = Llb_Nonlin4CreateVars2Q( p->dd, p->pAig, p->vOrder, 0 );

    // 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->dd, (DdNode *)Vec_PtrEntryLast(p->vRings), p->bBad );  Cudd_Ref( bOneCube );
    RetValue = Cudd_bddPickOneCube( p->dd, bOneCube, pValues );
    Cudd_RecursiveDeref( p->dd, 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[Llb_MnxBddVar(p->vOrder, pObj)] == 1 )
            Aig_InfoSetBit( pCex->pData, nPiOffset + i );

    // write state in terms of NS variables
    if ( Vec_PtrSize(p->vRings) > 1 )
    {
        bState = Llb_Nonlin4ComputeCube( p->dd, p->pAig, p->vOrder, pValues );   Cudd_Ref( bState );
    }
    // perform backward analysis
    Vec_PtrForEachEntryReverse( DdNode *, p->vRings, bRing, v )
    { 
        if ( v == Vec_PtrSize(p->vRings) - 1 )
            continue;
        // compute the next states
        bImage = Llb_Nonlin4Image( p->dd, p->vRoots, bState, p->vVars2Q );
        assert( bImage != NULL );
        Cudd_Ref( bImage );
        Cudd_RecursiveDeref( p->dd, bState );

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

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

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

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

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


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

  Synopsis    [Perform reachability with hints.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
{ 
    DdNode * bAux;
    int nIters, nBddSizeFr, nBddSizeTo, nBddSizeTo2;
    int clkTemp, clkIter, clk = clock();
    assert( Aig_ManRegNum(p->pAig) > 0 );

    // compute time to stop
    if ( p->pPars->TimeLimit )
        p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC;
    else
        p->pPars->TimeTarget = 0;
    // set the stop time parameter
    p->dd->TimeStop  = p->pPars->TimeTarget;

    // create bad state in the ring manager
    if ( !p->pPars->fSkipOutCheck )
    {
        p->bBad = Llb_Nonlin4ComputeBad( p->dd, p->pAig, p->vOrder );          
        if ( p->bBad == 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->bBad );
    }

    // compute the starting set of states
    p->bCurrent = Llb_Nonlin4ComputeInitState( p->dd, p->pAig, p->vOrder );  Cudd_Ref( p->bCurrent );
    p->bReached = p->bCurrent;                                               Cudd_Ref( p->bCurrent );
    for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ )
    { 
        clkIter = clock();
        // check the runtime limit
        if ( p->pPars->TimeLimit && 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;
            return -1;
        }

        // save the onion ring
        Vec_PtrPush( p->vRings, p->bCurrent );   Cudd_Ref( p->bCurrent );

        // check it for bad states
        if ( !p->pPars->fSkipOutCheck && !Cudd_bddLeq( p->dd, p->bCurrent, Cudd_Not(p->bBad) ) ) 
        {
            assert( p->pAig->pSeqModel == NULL );
            if ( !p->pPars->fBackward )
                p->pAig->pSeqModel = Llb_Nonlin4DeriveCex( p ); 
            if ( !p->pPars->fSilent )
            {
                if ( !p->pPars->fBackward )
                    printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).  ", p->pAig->pSeqModel->iPo, nIters );
                else
                    printf( "Output ??? was asserted in frame %d (counter-example is not produced).  ", nIters );
                Abc_PrintTime( 1, "Time", clock() - clk );
            }
            p->pPars->iFrame = nIters - 1;
            return 0;
        }

        // compute the next states
        clkTemp = clock();
        p->bNext = Llb_Nonlin4Image( p->dd, p->vRoots, p->bCurrent, p->vVars2Q );
        if ( p->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;
            return -1;
        }
        Cudd_Ref( p->bNext );
        p->timeImage += clock() - clkTemp;

        // remap into current states
        clkTemp = clock();
        p->bNext = Cudd_bddVarMap( p->dd, bAux = p->bNext );
        if ( p->bNext == NULL )
        {
            if ( !p->pPars->fSilent )
                printf( "Reached timeout (%d seconds) during remapping next states.\n",  p->pPars->TimeLimit );
            Cudd_RecursiveDeref( p->dd, bAux );
            p->pPars->iFrame = nIters - 1;
            return -1;
        }
        Cudd_Ref( p->bNext );
        Cudd_RecursiveDeref( p->dd, bAux );
        p->timeRemap += clock() - clkTemp;

        // collect statistics
        if ( p->pPars->fVerbose )
        {
            nBddSizeFr  = Cudd_DagSize( p->bCurrent );
            nBddSizeTo  = Cudd_DagSize( bAux );
            nBddSizeTo2 = Cudd_DagSize( p->bNext );
        }
        Cudd_RecursiveDeref( p->dd, p->bCurrent ); p->bCurrent = NULL;

        // derive new states
        p->bCurrent = Cudd_bddAnd( p->dd, p->bNext, Cudd_Not(p->bReached) );     
        if ( p->bCurrent == 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;
            return -1;
        }
        Cudd_Ref( p->bCurrent );
        Cudd_RecursiveDeref( p->dd, p->bNext ); p->bNext = NULL;
        if ( Cudd_IsConstant(p->bCurrent) )
            break;

        // add to the reached set
        p->bReached = Cudd_bddOr( p->dd, bAux = p->bReached, p->bCurrent );                 
        if ( p->bReached == 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, bAux );  
            return -1;
        }
        Cudd_Ref( p->bReached );
        Cudd_RecursiveDeref( p->dd, bAux );  

        // report the results
        if ( p->pPars->fVerbose )
        {
            printf( "I =%5d : ",   nIters );
            printf( "Fr =%7d  ",    nBddSizeFr );
            printf( "ImNs =%7d  ",  nBddSizeTo );
            printf( "ImCs =%7d  ",  nBddSizeTo2 );
            printf( "Rea =%7d   ",  Cudd_DagSize(p->bReached) );
            printf( "(%4d %4d)  ", Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) );
            Abc_PrintTime( 1, "T", clock() - clkIter );
        }
/*
        if ( pPars->fVerbose )
        {
            double nMints = Cudd_CountMinterm(p->dd, bReached, Saig_ManRegNum(p->pAig) );
//            Extra_bddPrint( p->dd, bReached );printf( "\n" );
            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 - 1 )
        {
            if ( !p->pPars->fSilent )
                printf( "Reached limit on the number of timeframes (%d).\n",  p->pPars->nIterMax );
            p->pPars->iFrame = nIters;
            return -1;
        }
    }
    
    // report the stats
    if ( p->pPars->fVerbose )
    {
        double nMints = Cudd_CountMinterm(p->dd, p->bReached, Saig_ManRegNum(p->pAig) );
        if ( p->bCurrent && Cudd_IsConstant(p->bCurrent) )
            printf( "Reachability analysis completed after %d frames.\n", nIters );
        else
            printf( "Reachability analysis is stopped 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 ( p->bCurrent == NULL || !Cudd_IsConstant(p->bCurrent) )
    {
        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", clock() - clk );
    return 1; // unreachable
}

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

  Synopsis    [Reorders BDDs in the working manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_Nonlin4Reorder( DdManager * dd, int fTwice, int fVerbose )
{
    int clk = clock();
    if ( fVerbose )
        Abc_Print( 1, "Reordering... Before =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
    Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
    if ( fVerbose )
        Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
    if ( fTwice )
    {
        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
        if ( fVerbose )
            Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
    }
    if ( fVerbose )
        Abc_PrintTime( 1, "Time", clock() - clk );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Llb_Mnx_t * Llb_MnxStart( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
{
    Llb_Mnx_t * p;
    p = ABC_CALLOC( Llb_Mnx_t, 1 );
    p->pAig    = pAig;
    p->pPars   = pPars;
//    p->vOrder  = Llb_Nonlin4CreateOrderSimple( pAig );
    p->vOrder  = Llb_Nonlin4CreateOrderSmart( pAig );
    p->dd      = Cudd_Init( Vec_IntSize(p->vOrder), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
    Llb_Nonlin4SetupVarMap( p->dd, pAig, p->vOrder );
    Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
    p->vVars2Q = Llb_Nonlin4CreateVars2Q( p->dd, pAig, p->vOrder, 1 );
    p->vRoots  = Llb_Nonlin4DerivePartitions( p->dd, pAig, p->vOrder );
    p->vRings  = Vec_PtrAlloc( 100 );
    if ( pPars->fReorder )
        Llb_Nonlin4Reorder( p->dd, 0, 1 );
    return p;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_MnxStop( Llb_Mnx_t * p )
{
    DdNode * bTemp;
    int i;
    if ( p->pPars->fVerbose ) 
    {
        p->timeReo = Cudd_ReadReorderingTime(p->dd);
        p->timeOther = p->timeTotal - p->timeImage - p->timeRemap;
        ABC_PRTP( "Image    ", p->timeImage, p->timeTotal );
        ABC_PRTP( "Remap    ", p->timeRemap, p->timeTotal );
        ABC_PRTP( "Other    ", p->timeOther, p->timeTotal );
        ABC_PRTP( "TOTAL    ", p->timeTotal, p->timeTotal );
        ABC_PRTP( "  reo    ", p->timeReo,   p->timeTotal );
    }
    // remove BDDs
    if ( p->bBad )
        Cudd_RecursiveDeref( p->dd, p->bBad );
    if ( p->bReached )
        Cudd_RecursiveDeref( p->dd, p->bReached );
    if ( p->bCurrent )
        Cudd_RecursiveDeref( p->dd, p->bCurrent );
    if ( p->bNext )
        Cudd_RecursiveDeref( p->dd, p->bNext );
    Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
        Cudd_RecursiveDeref( p->dd, bTemp );
    Vec_PtrForEachEntry( DdNode *, p->vRoots, bTemp, i )
        Cudd_RecursiveDeref( p->dd, bTemp );
    // remove arrays
    Vec_PtrFree( p->vRings );
    Vec_PtrFree( p->vRoots );
    Extra_StopManager( p->dd );
    Vec_IntFreeP( &p->vOrder );
    Vec_IntFreeP( &p->vVars2Q );
    ABC_FREE( p );
}


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

  Synopsis    [Finds balanced cut.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
{
    Llb_Mnx_t * pMnn;
    int RetValue = -1;
    if ( pPars->fVerbose )
    Aig_ManPrintStats( pAig );
    if ( !pPars->fSkipReach )
    {
        int clk = clock();
        pMnn = Llb_MnxStart( pAig, pPars );
        RetValue = Llb_Nonlin4Reachability( pMnn );
        pMnn->timeTotal = clock() - clk;
        Llb_MnxStop( pMnn );
    }
    return RetValue;
}

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


ABC_NAMESPACE_IMPL_END