/**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"
#include "base/abc/abc.h"
#include "aig/gia/giaAig.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

    abctime         timeImage;
    abctime         timeRemap;
    abctime         timeReo;
    abctime         timeOther;
    abctime         timeTotal;
};

//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, * bCube;
    Aig_Obj_t * pObj;
    int i;
    Aig_ManCleanData( pAig );
    // assign elementary variables
    Aig_ManConst1(pAig)->pData = Cudd_ReadOne(dd); 
    Aig_ManForEachCi( pAig, pObj, i )
        pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
    // compute internal nodes
    vNodes = Aig_ManDfsNodes( pAig, (Aig_Obj_t **)Vec_PtrArray(pAig->vCos), 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 )
    {
        bCube = Cudd_ReadOne(dd);  Cudd_Ref( bCube );
        Saig_ManForEachPi( pAig, pObj, i )
        {
            bCube = Cudd_bddAnd( dd, bTemp = bCube, (DdNode *)pObj->pData );  
            if ( bCube == NULL )
            {
                Cudd_RecursiveDeref( dd, bTemp );
                Cudd_RecursiveDeref( dd, bResult );
                bResult = NULL;
                break;
            }
            Cudd_Ref( bCube );
            Cudd_RecursiveDeref( dd, bTemp );
        }
        if ( bResult != NULL )
        {
            bResult = Cudd_bddExistAbstract( dd, bTemp = bResult, bCube );  Cudd_Ref( bResult );
            Cudd_RecursiveDeref( dd, bTemp );
            Cudd_RecursiveDeref( dd, bCube );
            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_ManForEachCi( pAig, pObj, i )
        pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
    Aig_ManForEachNode( pAig, pObj, i )
        if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
        {
            pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
            Cudd_Ref( (DdNode *)pObj->pData );
        }
    Saig_ManForEachLi( pAig, pObj, i )
        pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(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_ManForEachCi( 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_Nonlin4CreateOrder_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_ObjBddVar(vOrder, pObj) < 0 );
    if ( Aig_ObjIsCi(pObj) )
    {
//        if ( Saig_ObjIsLo(pAig, pObj) )
//            Vec_IntWriteEntry( vOrder, Aig_ObjId(Saig_ObjLoToLi(pAig, pObj)), (*pCounter)++ );
        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_Nonlin4CreateOrder_rec( pAig, pFanin0, vOrder, pCounter );
        Llb_Nonlin4CreateOrder_rec( pAig, pFanin1, vOrder, pCounter );
    }
    else
    {
        Llb_Nonlin4CreateOrder_rec( pAig, pFanin1, vOrder, pCounter );
        Llb_Nonlin4CreateOrder_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_Nonlin4CreateOrder( 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_ManForEachObjVec( vNodes, pAig, 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 )
    {
        Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
        Llb_Nonlin4CreateOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter );
    }
    Aig_ManForEachCi( pAig, pObj, i )
        if ( Llb_ObjBddVar(vOrder, pObj) < 0 )
        {
//            if ( Saig_ObjIsLo(pAig, pObj) )
//                Vec_IntWriteEntry( vOrder, Aig_ObjId(Saig_ObjLoToLi(pAig, pObj)), Counter++ );
            Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
        }
    assert( Counter <= Aig_ManCiNum(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 fBackward )
{
    Vec_Int_t * vVars2Q;
    Aig_Obj_t * pObjLi, * pObjLo;
    int i;
    vVars2Q = Vec_IntAlloc( 0 );
    Vec_IntFill( vVars2Q, Cudd_ReadSize(dd), 1 );
    Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
        Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, fBackward ? pObjLo : pObjLi), 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 )
    {
        assert( Llb_ObjBddVar(vOrder, pObjLo) >= 0 );
        assert( Llb_ObjBddVar(vOrder, pObjLi) >= 0 );
        pVarsX[i] = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObjLo) );
        pVarsY[i] = Cudd_bddIthVar( dd, Llb_ObjBddVar(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, int fBackward )
{
    Aig_Obj_t * pObjLi, * pObjLo;
    DdNode * bRes, * bVar, * bTemp;
    int i;
    abctime TimeStop;
    TimeStop = dd->TimeStop;  dd->TimeStop = 0;
    bRes = Cudd_ReadOne( dd );   Cudd_Ref( bRes );
    Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
    {
        bVar = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, fBackward? pObjLi : pObjLo) );
        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, int Flag )
{
    Aig_Obj_t * pObjLo, * pObjLi, * pObjTemp;
    DdNode * bRes, * bVar, * bTemp;
    int i;
    abctime TimeStop;
    TimeStop = dd->TimeStop;  dd->TimeStop = 0;
    bRes = Cudd_ReadOne( dd );   Cudd_Ref( bRes );
    Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
    {
        if ( Flag )
            pObjTemp = pObjLo, pObjLo = pObjLi, pObjLi = pObjTemp;
        // get the correspoding flop input variable
        bVar = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObjLi) );
        if ( pValues[Llb_ObjBddVar(vOrder, pObjLo)] != 1 )
            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    [Compute initial state in terms of current state variables.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_Nonlin4RecordState( Aig_Man_t * pAig, Vec_Int_t * vOrder, unsigned * pState, char * pValues, int fBackward )
{
    Aig_Obj_t * pObjLo, * pObjLi;
    int i;
    Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
        if ( pValues[Llb_ObjBddVar(vOrder, fBackward? pObjLi : pObjLo)] == 1 )
            Abc_InfoSetBit( pState, i );
}

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

  Synopsis    [Multiply every partition by the cube.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Ptr_t * Llb_Nonlin4Multiply( DdManager * dd, DdNode * bCube, Vec_Ptr_t * vParts )
{
    Vec_Ptr_t * vNew;
    DdNode * bTemp, * bFunc;
    int i;
    vNew = Vec_PtrAlloc( Vec_PtrSize(vParts) );
    Vec_PtrForEachEntry( DdNode *, vParts, bFunc, i )
    {
        bTemp = Cudd_bddAnd( dd, bFunc, bCube );  Cudd_Ref( bTemp );
        Vec_PtrPush( vNew, bTemp );
    }
    return vNew;
}

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

  Synopsis    [Multiply every partition by the cube.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_Nonlin4Deref( DdManager * dd, Vec_Ptr_t * vParts )
{
    DdNode * bFunc;
    int i;
    Vec_PtrForEachEntry( DdNode *, vParts, bFunc, i )
        Cudd_RecursiveDeref( dd, bFunc );
    Vec_PtrFree( vParts );
}

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

  Synopsis    [Derives counter-example by backward reachability.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Ptr_t * Llb_Nonlin4DeriveCex( Llb_Mnx_t * p, int fBackward, int fVerbose )
{
    Vec_Int_t * vVars2Q;
    Vec_Ptr_t * vStates, * vRootsNew;
    Aig_Obj_t * pObj;
    DdNode * bState = NULL, * bImage, * bOneCube, * bRing;
    int i, v, RetValue;//, clk = Abc_Clock();
    char * pValues;
    assert( Vec_PtrSize(p->vRings) > 0 );
    // disable the timeout
    p->dd->TimeStop  = 0;

    // start the state set
    vStates = Vec_PtrAllocSimInfo( Vec_PtrSize(p->vRings), Abc_BitWordNum(Aig_ManRegNum(p->pAig)) );
    Vec_PtrCleanSimInfo( vStates, 0, Abc_BitWordNum(Aig_ManRegNum(p->pAig)) );
    if ( fBackward )
        Vec_PtrReverseOrder( vStates );

    // get the last cube
    pValues = ABC_ALLOC( char, Cudd_ReadSize(p->dd) );
    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 );

    // record the cube
    Llb_Nonlin4RecordState( p->pAig, p->vOrder, (unsigned *)Vec_PtrEntryLast(vStates), pValues, fBackward );

    // write state in terms of NS variables
    if ( Vec_PtrSize(p->vRings) > 1 )
    {
        bState = Llb_Nonlin4ComputeCube( p->dd, p->pAig, p->vOrder, pValues, fBackward );   Cudd_Ref( bState );
    }
    // perform backward analysis
    vVars2Q = Llb_Nonlin4CreateVars2Q( p->dd, p->pAig, p->vOrder, !fBackward );
    Vec_PtrForEachEntryReverse( DdNode *, p->vRings, bRing, v )
    { 
        if ( v == Vec_PtrSize(p->vRings) - 1 )
            continue;

        // preprocess partitions
        vRootsNew = Llb_Nonlin4Multiply( p->dd, bState, p->vRoots );
        Cudd_RecursiveDeref( p->dd, bState );

        // compute the next states
        bImage = Llb_Nonlin4Image( p->dd, vRootsNew, NULL, vVars2Q ); Cudd_Ref( bImage );
        Llb_Nonlin4Deref( p->dd, vRootsNew );

        // 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 );

        // record the cube
        Llb_Nonlin4RecordState( p->pAig, p->vOrder, (unsigned *)Vec_PtrEntry(vStates, v), pValues, fBackward );

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

        // write state in terms of NS variables
        bState = Llb_Nonlin4ComputeCube( p->dd, p->pAig, p->vOrder, pValues, fBackward );   Cudd_Ref( bState );
    }
    Vec_IntFree( vVars2Q );
    ABC_FREE( pValues );
    if ( fBackward )
        Vec_PtrReverseOrder( vStates );
//    if ( fVerbose )
//        Abc_PrintTime( 1, "BDD-based cex generation time", Abc_Clock() - clk );
    return vStates;
}


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

  Synopsis    [Perform reachability with hints.]

  Description []
               
  SideEffects []

  SeeAlso     []

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

    if ( p->pPars->fBackward )
    {
        // create bad state in the ring manager
        if ( !p->pPars->fSkipOutCheck )
        {
            p->bBad = Llb_Nonlin4ComputeInitState( p->dd, p->pAig, p->vOrder, p->pPars->fBackward );  Cudd_Ref( p->bBad );
        }
        // create init state
        if ( p->pPars->fCluster )
            p->bCurrent = p->dd->bFunc, p->dd->bFunc = NULL; 
        else
        {
            p->bCurrent = Llb_Nonlin4ComputeBad( p->dd, p->pAig, p->vOrder );          
            if ( p->bCurrent == 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->bCurrent );
        }
        // remap into the next states
        p->bCurrent = Cudd_bddVarMap( p->dd, bAux = p->bCurrent );
        if ( p->bCurrent == NULL )
        {
            if ( !p->pPars->fSilent )
                printf( "Reached timeout (%d seconds) during remapping bad states.\n",  p->pPars->TimeLimit );
            Cudd_RecursiveDeref( p->dd, bAux );
            p->pPars->iFrame = -1;
            return -1;
        }
        Cudd_Ref( p->bCurrent );
        Cudd_RecursiveDeref( p->dd, bAux );
    }
    else
    {
        // create bad state in the ring manager
        if ( !p->pPars->fSkipOutCheck )
        {
            if ( p->pPars->fCluster )
                p->bBad = p->dd->bFunc, p->dd->bFunc = NULL; 
            else
            {
                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 );
            }
        }
        else if ( p->dd->bFunc )
            Cudd_RecursiveDeref( p->dd, p->dd->bFunc ), p->dd->bFunc = NULL;
        // compute the starting set of states
        p->bCurrent = Llb_Nonlin4ComputeInitState( p->dd, p->pAig, p->vOrder, p->pPars->fBackward );  Cudd_Ref( p->bCurrent );
    }
    // perform iterations
    p->bReached = p->bCurrent; Cudd_Ref( p->bReached );
    for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ )
    { 
        clkIter = Abc_Clock();
        // check the runtime limit
        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;
            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) ) ) 
        {
            Vec_Ptr_t * vStates;
            assert( p->pAig->pSeqModel == NULL );
            vStates = Llb_Nonlin4DeriveCex( p, p->pPars->fBackward, p->pPars->fVerbose ); 
            p->pAig->pSeqModel = Llb4_Nonlin4TransformCex( p->pAig, vStates, -1, p->pPars->fVerbose );
            Vec_PtrFreeP( &vStates );
            if ( !p->pPars->fSilent )
            {
                Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", p->pAig->pSeqModel->iPo, p->pAig->pName, nIters );
                Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
            }
            p->pPars->iFrame = nIters - 1;
            return 0;
        }

        // compute the next states
        clkTemp = Abc_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 += Abc_Clock() - clkTemp;

        // remap into current states
        clkTemp = Abc_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 += Abc_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;
/*
        // reduce BDD size using constrain // Cudd_bddRestrict
        p->bCurrent = Cudd_bddRestrict( p->dd, bAux = p->bCurrent, Cudd_Not(p->bReached) );   
        Cudd_Ref( p->bCurrent );
printf( "Before = %d.  After = %d.\n", Cudd_DagSize(bAux), Cudd_DagSize(p->bCurrent) );
        Cudd_RecursiveDeref( p->dd, bAux );
*/

        // 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", Abc_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 );
    if ( !p->pPars->fSilent )
        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    p->pPars->iFrame = nIters - 1;
    return 1; // unreachable
}

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

  Synopsis    [Reorders BDDs in the working manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_Nonlin4Reorder( DdManager * dd, int fTwice, int fVerbose )
{
    abctime clk = Abc_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", Abc_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;

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

    if ( pPars->fCluster )
    {
//        Llb_Nonlin4Cluster( p->pAig, &p->dd, &p->vOrder, &p->vRoots, pPars->nBddMax, pPars->fVerbose );
//        Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
        Llb4_Nonlin4Sweep( p->pAig, pPars->nBddMax, pPars->nClusterMax, &p->dd, &p->vOrder, &p->vRoots, pPars->fVerbose );
		// set the stop time parameter
		p->dd->TimeStop  = p->pPars->TimeTarget;
    }
    else
    {
//    p->vOrder  = Llb_Nonlin4CreateOrderSimple( pAig );
        p->vOrder  = Llb_Nonlin4CreateOrder( pAig );
        p->dd      = Cudd_Init( Vec_IntCountPositive(p->vOrder) + 1, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
        Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
        Cudd_SetMaxGrowth( p->dd, 1.05 );
		// set the stop time parameter
		p->dd->TimeStop  = p->pPars->TimeTarget;
        p->vRoots  = Llb_Nonlin4DerivePartitions( p->dd, pAig, p->vOrder );
    }

    Llb_Nonlin4SetupVarMap( p->dd, pAig, p->vOrder );
    p->vVars2Q = Llb_Nonlin4CreateVars2Q( p->dd, pAig, p->vOrder, p->pPars->fBackward );
    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 );
	if ( p->vRings )
    Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
        Cudd_RecursiveDeref( p->dd, bTemp );
	if ( p->vRoots )
    Vec_PtrForEachEntry( DdNode *, p->vRoots, bTemp, i )
        Cudd_RecursiveDeref( p->dd, bTemp );
    // remove arrays
    Vec_PtrFreeP( &p->vRings );
    Vec_PtrFreeP( &p->vRoots );
//Cudd_PrintInfo( p->dd, stdout );
    Extra_StopManager( p->dd );
    Vec_IntFreeP( &p->vOrder );
    Vec_IntFreeP( &p->vVars2Q );
    ABC_FREE( p );
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_MnxCheckNextStateVars( Llb_Mnx_t * p )
{
    Aig_Obj_t * pObj;
    int i, Counter0 = 0, Counter1 = 0;
    Saig_ManForEachLi( p->pAig, pObj, i )
        if ( Saig_ObjIsLo(p->pAig, Aig_ObjFanin0(pObj)) )
        {
            if ( Aig_ObjFaninC0(pObj) )
                Counter0++;
            else
                Counter1++;
        }
    printf( "Total = %d.  Direct LO = %d. Compl LO = %d.\n", Aig_ManRegNum(p->pAig), Counter1, Counter0 );
}

/**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->fCluster && Aig_ManObjNum(pAig) >= (1 << 15) )
    {
        printf( "The number of objects is more than 2^15.  Clustering cannot be used.\n" );
        return RetValue;
    }
    {
        abctime clk = Abc_Clock();
        pMnn = Llb_MnxStart( pAig, pPars );
//Llb_MnxCheckNextStateVars( pMnn );
        if ( !pPars->fSkipReach )
            RetValue = Llb_Nonlin4Reachability( pMnn );
        pMnn->timeTotal = Abc_Clock() - clk;
        Llb_MnxStop( pMnn );
    }
    return RetValue;
}


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

  Synopsis    [Takes an AIG and returns an AIG representing reachable states.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Llb_ReachableStates( Aig_Man_t * pAig )
{
    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
    Vec_Int_t * vPermute;
    Vec_Ptr_t * vNames;
    Gia_ParLlb_t Pars, * pPars = &Pars;
    DdManager * dd;
    DdNode * bReached;
    Llb_Mnx_t * pMnn;
    Abc_Ntk_t * pNtk, * pNtkMuxes;
    Aig_Obj_t * pObj;
    int i, RetValue;
    abctime clk = Abc_Clock();

    // create parameters
    Llb_ManSetDefaultParams( pPars );
    pPars->fSkipOutCheck = 1;
    pPars->fCluster      = 0;
    pPars->fReorder      = 0;
    pPars->fSilent       = 1;
    pPars->nBddMax       = 100;
    pPars->nClusterMax   = 500;

    // run reachability
    pMnn = Llb_MnxStart( pAig, pPars );
    RetValue = Llb_Nonlin4Reachability( pMnn );
    assert( RetValue == 1 );

    // print BDD
//    Extra_bddPrint( pMnn->dd, pMnn->bReached ); 
//    Extra_bddPrintSupport( pMnn->dd, pMnn->bReached ); 
//    printf( "\n" );

    // collect flop output variables
    vPermute = Vec_IntStartFull( Cudd_ReadSize(pMnn->dd) );
    Saig_ManForEachLo( pAig, pObj, i )
        Vec_IntWriteEntry( vPermute, Llb_ObjBddVar(pMnn->vOrder, pObj), i );

    // transfer the reached state BDD into the new manager
    dd = Cudd_Init( Saig_ManRegNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
    Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
    bReached = Extra_TransferPermute( pMnn->dd, dd, pMnn->bReached, Vec_IntArray(vPermute) );  Cudd_Ref( bReached );
    Vec_IntFree( vPermute );
    assert( Cudd_ReadSize(dd) == Saig_ManRegNum(pAig) );

    // quit reachability engine
    pMnn->timeTotal = Abc_Clock() - clk;
    Llb_MnxStop( pMnn );

    // derive the network
    vNames = Abc_NodeGetFakeNames( Saig_ManRegNum(pAig) );
    pNtk = Abc_NtkDeriveFromBdd( dd, bReached, "reached", vNames );
    Abc_NodeFreeNames( vNames );
    Cudd_RecursiveDeref( dd, bReached );
    Cudd_Quit( dd );

    // convert
    pNtkMuxes = Abc_NtkBddToMuxes( pNtk );
    Abc_NtkDelete( pNtk );
    pNtk = Abc_NtkStrash( pNtkMuxes, 0, 1, 0 );
    Abc_NtkDelete( pNtkMuxes );
    pAig = Abc_NtkToDar( pNtk, 0, 0 );
    Abc_NtkDelete( pNtk );
    return pAig;
}
Gia_Man_t * Llb_ReachableStatesGia( Gia_Man_t * p )
{
    Gia_Man_t * pNew;
    Aig_Man_t * pAig, * pReached;
    pAig = Gia_ManToAigSimple( p );
    pReached = Llb_ReachableStates( pAig );
    Aig_ManStop( pAig );
    pNew = Gia_ManFromAigSimple( pReached );
    Aig_ManStop( pReached );
    return pNew;
}

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


ABC_NAMESPACE_IMPL_END