Changes to be able to compile ABC without CUDD.

1 files changed, 0 insertions, 904 deletions

diff --git a/src/proof/llb/llb1Reach.c b/src/proof/llb/llb1Reach.c
deleted file mode 100644
index fae7bee2..00000000
--- a/src/proof/llb/llb1Reach.c
+++ /dev/null
@@ -1,904 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [llb1Reach.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [BDD based reachability.]
-
-  Synopsis    [Reachability analysis.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: llb1Reach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "llbInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
- 
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Derives global BDD for the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Llb_ManConstructOutBdd( Aig_Man_t * pAig, Aig_Obj_t * pNode, DdManager * dd )
-{
-    DdNode * bBdd0, * bBdd1, * bFunc;
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj = NULL;
-    int i;
-    abctime TimeStop;
-    if ( Aig_ObjFanin0(pNode) == Aig_ManConst1(pAig) )
-        return Cudd_NotCond( Cudd_ReadOne(dd), Aig_ObjFaninC0(pNode) );
-    TimeStop = dd->TimeStop;  dd->TimeStop = 0;
-    vNodes = Aig_ManDfsNodes( pAig, &pNode, 1 );
-    assert( Vec_PtrSize(vNodes) > 0 );
-    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
-    {
-        if ( !Aig_ObjIsNode(pObj) )
-            continue;
-        bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
-        bBdd1 = Cudd_NotCond( Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
-        pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );  Cudd_Ref( (DdNode *)pObj->pData );
-    }
-    bFunc = (DdNode *)pObj->pData; Cudd_Ref( bFunc );
-    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
-    {
-        if ( !Aig_ObjIsNode(pObj) )
-            continue;
-        Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
-    }
-    Vec_PtrFree( vNodes );
-    if ( Aig_ObjIsCo(pNode) )
-        bFunc = Cudd_NotCond( bFunc, Aig_ObjFaninC0(pNode) );
-    Cudd_Deref( bFunc );
-    dd->TimeStop = TimeStop;
-    return bFunc;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives BDD for the group.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Llb_ManConstructGroupBdd( Llb_Man_t * p, Llb_Grp_t * pGroup )
-{
-    Aig_Obj_t * pObj;
-    DdNode * bBdd0, * bBdd1, * bRes, * bXor, * bTemp;
-    int i, k;
-    Aig_ManConst1(p->pAig)->pData = Cudd_ReadOne( p->dd );
-    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
-        pObj->pData = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
-    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vNodes, pObj, i )
-    {
-        bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
-        bBdd1 = Cudd_NotCond( Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
-//        pObj->pData = Extra_bddAndTime( p->dd, bBdd0, bBdd1, p->pPars->TimeTarget );  
-        pObj->pData = Cudd_bddAnd( p->dd, bBdd0, bBdd1 );  
-        if ( pObj->pData == NULL )
-        {
-            Vec_PtrForEachEntryStop( Aig_Obj_t *, pGroup->vNodes, pObj, k, i )
-                if ( pObj->pData )
-                    Cudd_RecursiveDeref( p->dd, (DdNode *)pObj->pData );
-            return NULL;
-        }
-        Cudd_Ref( (DdNode *)pObj->pData );
-    }
-    bRes = Cudd_ReadOne( p->dd );   Cudd_Ref( bRes );
-    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
-    {
-        if ( Aig_ObjIsCo(pObj) )
-            bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
-        else
-            bBdd0 = (DdNode *)pObj->pData;
-        bBdd1 = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
-        bXor  = Cudd_bddXor( p->dd, bBdd0, bBdd1 );                  Cudd_Ref( bXor );
-//        bRes  = Extra_bddAndTime( p->dd, bTemp = bRes, Cudd_Not(bXor), p->pPars->TimeTarget );  
-        bRes  = Cudd_bddAnd( p->dd, bTemp = bRes, Cudd_Not(bXor) );  
-        if ( bRes == NULL )
-        {
-            Cudd_RecursiveDeref( p->dd, bTemp );
-            Cudd_RecursiveDeref( p->dd, bXor );
-            Vec_PtrForEachEntryStop( Aig_Obj_t *, pGroup->vNodes, pObj, k, i )
-                if ( pObj->pData )
-                    Cudd_RecursiveDeref( p->dd, (DdNode *)pObj->pData );
-            return NULL;
-        }        
-        Cudd_Ref( bRes );
-        Cudd_RecursiveDeref( p->dd, bTemp );
-        Cudd_RecursiveDeref( p->dd, bXor );
-    }
-    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vNodes, pObj, i )
-        Cudd_RecursiveDeref( p->dd, (DdNode *)pObj->pData );
-    Cudd_Deref( bRes );
-    return bRes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives quantification cube.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Llb_ManConstructQuantCubeIntern( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace, int fBackward )
-{
-    Aig_Obj_t * pObj;
-    DdNode * bRes, * bTemp, * bVar;
-    int i, iGroupFirst, iGroupLast;
-    abctime TimeStop;
-    TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
-    bRes = Cudd_ReadOne( p->dd );   Cudd_Ref( bRes );
-    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
-    {
-        if ( fBackward && Saig_ObjIsPi(p->pAig, pObj) )
-            continue;
-        iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj));
-        iGroupLast  = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj));
-        assert( iGroupFirst <= iGroupLast );
-        if ( iGroupFirst < iGroupLast )
-            continue;
-        bVar  = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
-        bRes  = Cudd_bddAnd( p->dd, bTemp = bRes, bVar );  Cudd_Ref( bRes );
-        Cudd_RecursiveDeref( p->dd, bTemp );
-    }
-    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
-    {
-        if ( fBackward && Saig_ObjIsPi(p->pAig, pObj) )
-            continue;
-        iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj));
-        iGroupLast  = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj));
-        assert( iGroupFirst <= iGroupLast );
-        if ( iGroupFirst < iGroupLast )
-            continue;
-        bVar  = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
-        bRes  = Cudd_bddAnd( p->dd, bTemp = bRes, bVar );  Cudd_Ref( bRes );
-        Cudd_RecursiveDeref( p->dd, bTemp );
-    }
-    Cudd_Deref( bRes );
-    p->dd->TimeStop = TimeStop;
-    return bRes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives quantification cube.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Llb_ManConstructQuantCubeFwd( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace )
-{
-    Aig_Obj_t * pObj;
-    DdNode * bRes, * bTemp, * bVar;
-    int i, iGroupLast;
-    abctime TimeStop;
-    TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
-    bRes = Cudd_ReadOne( p->dd );   Cudd_Ref( bRes );
-    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
-    {
-        iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj));
-        assert( iGroupLast >= iGrpPlace );
-        if ( iGroupLast > iGrpPlace )
-            continue;
-        bVar  = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
-        bRes  = Cudd_bddAnd( p->dd, bTemp = bRes, bVar );  Cudd_Ref( bRes );
-        Cudd_RecursiveDeref( p->dd, bTemp );
-    }
-    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
-    {
-        iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj));
-        assert( iGroupLast >= iGrpPlace );
-        if ( iGroupLast > iGrpPlace )
-            continue;
-        bVar  = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
-        bRes  = Cudd_bddAnd( p->dd, bTemp = bRes, bVar );  Cudd_Ref( bRes );
-        Cudd_RecursiveDeref( p->dd, bTemp );
-    }
-    Cudd_Deref( bRes );
-    p->dd->TimeStop = TimeStop;
-    return bRes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives quantification cube.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Llb_ManConstructQuantCubeBwd( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace )
-{
-    Aig_Obj_t * pObj;
-    DdNode * bRes, * bTemp, * bVar;
-    int i, iGroupFirst;
-    abctime TimeStop;
-    TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
-    bRes = Cudd_ReadOne( p->dd );   Cudd_Ref( bRes );
-    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
-    {
-        if ( Saig_ObjIsPi(p->pAig, pObj) )
-            continue;
-        iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj));
-        assert( iGroupFirst <= iGrpPlace );
-        if ( iGroupFirst < iGrpPlace )
-            continue;
-        bVar  = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
-        bRes  = Cudd_bddAnd( p->dd, bTemp = bRes, bVar );  Cudd_Ref( bRes );
-        Cudd_RecursiveDeref( p->dd, bTemp );
-    }
-    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
-    {
-        if ( Saig_ObjIsPi(p->pAig, pObj) )
-            continue;
-        iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj));
-        assert( iGroupFirst <= iGrpPlace );
-        if ( iGroupFirst < iGrpPlace )
-            continue;
-        bVar  = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
-        bRes  = Cudd_bddAnd( p->dd, bTemp = bRes, bVar );  Cudd_Ref( bRes );
-        Cudd_RecursiveDeref( p->dd, bTemp );
-    }
-    Cudd_Deref( bRes );
-    p->dd->TimeStop = TimeStop;
-    return bRes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Llb_ManComputeInitState( Llb_Man_t * p, 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( p->pAig, pObj, i )
-    {
-        iVar  = (dd == p->ddG) ? i : Vec_IntEntry(p->vObj2Var, 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    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Llb_ManComputeImage( Llb_Man_t * p, DdNode * bInit, int fBackward )
-{
-    int fCheckSupport = 0;
-    Llb_Grp_t * pGroup;
-    DdNode * bImage, * bGroup, * bCube, * bTemp;
-    int k, Index;
-    bImage = bInit;  Cudd_Ref( bImage );
-    for ( k = 1; k < p->pMatrix->nCols-1; k++ )
-    {
-        if ( fBackward )
-            Index = p->pMatrix->nCols - 1 - k;
-        else
-            Index = k;
-
-        // compute group BDD
-        pGroup = p->pMatrix->pColGrps[Index];
-        bGroup = Llb_ManConstructGroupBdd( p, pGroup );
-        if ( bGroup == NULL )
-        {
-            Cudd_RecursiveDeref( p->dd, bImage );
-            return NULL;
-        }
-        Cudd_Ref( bGroup );
-        // quantify variables appearing only in this group
-        bCube  = Llb_ManConstructQuantCubeIntern( p, pGroup, Index, fBackward );       Cudd_Ref( bCube );
-        bGroup = Cudd_bddExistAbstract( p->dd, bTemp = bGroup, bCube );         
-        if ( bGroup == NULL )
-        {
-            Cudd_RecursiveDeref( p->dd, bTemp );
-            Cudd_RecursiveDeref( p->dd, bCube );
-            return NULL;
-        }
-        Cudd_Ref( bGroup );
-        Cudd_RecursiveDeref( p->dd, bTemp );
-        Cudd_RecursiveDeref( p->dd, bCube );
-        // perform partial product
-        if ( fBackward )
-            bCube  = Llb_ManConstructQuantCubeBwd( p, pGroup, Index );
-        else
-            bCube  = Llb_ManConstructQuantCubeFwd( p, pGroup, Index );
-        Cudd_Ref( bCube );
-//        bImage = Extra_bddAndAbstractTime( p->dd, bTemp = bImage, bGroup, bCube, p->pPars->TimeTarget );   
-        bImage = Cudd_bddAndAbstract( p->dd, bTemp = bImage, bGroup, bCube );   
-        if ( bImage == NULL )
-        {
-            Cudd_RecursiveDeref( p->dd, bTemp );
-            Cudd_RecursiveDeref( p->dd, bGroup );
-            Cudd_RecursiveDeref( p->dd, bCube );
-            return NULL;
-        }
-        Cudd_Ref( bImage );
-        Cudd_RecursiveDeref( p->dd, bTemp );
-        Cudd_RecursiveDeref( p->dd, bGroup );
-        Cudd_RecursiveDeref( p->dd, bCube );
-    }
-
-    // make sure image depends on next state vars
-    if ( fCheckSupport )
-    {
-        bCube = Cudd_Support( p->dd, bImage );    Cudd_Ref( bCube );
-        for ( bTemp = bCube; bTemp != p->dd->one; bTemp = cuddT(bTemp) )
-        {
-            int ObjId = Vec_IntEntry( p->vVar2Obj, bTemp->index );
-            Aig_Obj_t * pObj = Aig_ManObj( p->pAig, ObjId );
-            if ( !Saig_ObjIsLi(p->pAig, pObj) )
-                printf( "Var %d assigned to obj %d that is not LI\n", bTemp->index, ObjId );
-        }
-        Cudd_RecursiveDeref( p->dd, bCube );
-    }
-    Cudd_Deref( bImage );
-    return bImage;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNsVars )
-{
-    DdNode * bConstr, * bFunc, * bTemp;
-    Aig_Obj_t * pObj;
-    int i, Entry;
-    abctime TimeStop;
-    if ( vHints == NULL )
-        return Cudd_ReadOne( p->dd );
-    TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
-    assert( Aig_ManCiNum(p->pAig) == Aig_ManCiNum(p->pAigGlo) );
-    // assign const and PI nodes to the original AIG
-    Aig_ManCleanData( p->pAig );
-    Aig_ManConst1( p->pAig )->pData = Cudd_ReadOne( p->dd );
-    Saig_ManForEachPi( p->pAig, pObj, i )
-        pObj->pData = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var,Aig_ObjId(pObj)) );
-    Saig_ManForEachLo( p->pAig, pObj, i )
-    {
-        if ( fUseNsVars )
-            Entry = Vec_IntEntry( p->vObj2Var, Aig_ObjId(Saig_ObjLoToLi(p->pAig, pObj)) );
-        else
-            Entry = Vec_IntEntry( p->vObj2Var, Aig_ObjId(pObj) );
-        pObj->pData = Cudd_bddIthVar( p->dd, Entry );
-    }
-    // transfer them to the global AIG
-    Aig_ManCleanData( p->pAigGlo );
-    Aig_ManConst1( p->pAigGlo )->pData = Cudd_ReadOne( p->dd );
-    Aig_ManForEachCi( p->pAigGlo, pObj, i )
-        pObj->pData = Aig_ManCi(p->pAig, i)->pData;
-    // derive consraints
-    bConstr = Cudd_ReadOne( p->dd );   Cudd_Ref( bConstr );
-    Vec_IntForEachEntry( vHints, Entry, i )
-    {
-        if ( Entry != 0 && Entry != 1 )
-            continue;
-        bFunc = Llb_ManConstructOutBdd( p->pAigGlo, Aig_ManObj(p->pAigGlo, i), p->dd );  Cudd_Ref( bFunc );
-        bFunc = Cudd_NotCond( bFunc, Entry ); // restrict to not constraint
-        // make the product
-        bConstr = Cudd_bddAnd( p->dd, bTemp = bConstr, bFunc );                          Cudd_Ref( bConstr );
-        Cudd_RecursiveDeref( p->dd, bTemp );
-        Cudd_RecursiveDeref( p->dd, bFunc );
-    }
-    Cudd_Deref( bConstr );
-    p->dd->TimeStop = TimeStop;
-    return bConstr;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Perform reachability with hints and returns reached states in ppGlo.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Llb_ManReachDeriveCex( Llb_Man_t * p )
-{
-    Abc_Cex_t * pCex;
-    Aig_Obj_t * pObj;
-    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;
-
-/*
-    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, p->vGlo2Ns, 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_ManComputeImage( p, bState, 1 ); 
-        assert( bImage != NULL );
-        Cudd_Ref( bImage );
-        Cudd_RecursiveDeref( p->dd, bState );
-//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 );
-//Extra_bddPrintSupport( p->ddR, bImage );  printf( "\n" );
-
-        // 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 );
-/*
-        for ( i = 0; i < p->ddR->size; i++ )
-            printf( "%d ", pValues[i] );
-        printf( "\n" );
-*/
-        // 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, p->vGlo2Ns, 1, pValues );   Cudd_Ref( bState );
-    }
-    assert( nPiOffset == Saig_ManRegNum(p->pAig) );
-    // update the output number
-//Abc_CexPrint( pCex );
-    RetValue = Saig_ManFindFailedPoCex( p->pAigGlo, pCex );
-    assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pAigGlo) ); // invalid CEX!!!
-    pCex->iPo = RetValue;
-    // cleanup
-    ABC_FREE( pValues );
-    return pCex;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Perform reachability with hints and returns reached states in ppGlo.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo )
-{
-    int * pNs2Glo = Vec_IntArray( p->vNs2Glo );
-    int * pCs2Glo = Vec_IntArray( p->vCs2Glo );
-    int * pGlo2Cs = Vec_IntArray( p->vGlo2Cs );
-    DdNode * bCurrent, * bReached, * bNext, * bTemp, * bCube;
-    DdNode * bConstrCs, * bConstrNs;
-    abctime clk2, clk = Abc_Clock();
-    int nIters, nBddSize = 0;
-//    int nThreshold = 10000;
-
-    // compute time to stop
-    p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
-
-    // define variable limits
-    Llb_ManPrepareVarLimits( p );
-
-    // start the managers
-    assert( p->dd == NULL );
-    assert( p->ddG == NULL );
-    assert( p->ddR == NULL );
-    p->dd  = Cudd_Init( Vec_IntSize(p->vVar2Obj), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    p->ddR = Cudd_Init( Aig_ManCiNum(p->pAig),    0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    if ( pddGlo && *pddGlo )
-        p->ddG = *pddGlo, *pddGlo = NULL; 
-    else
-        p->ddG = Cudd_Init( Aig_ManRegNum(p->pAig),   0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-
-    if ( p->pPars->fReorder )
-    {
-        Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
-        Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT );
-        Cudd_AutodynEnable( p->ddR, CUDD_REORDER_SYMM_SIFT );
-    }
-    else
-    {
-        Cudd_AutodynDisable( p->dd );
-        Cudd_AutodynDisable( p->ddG );
-        Cudd_AutodynDisable( p->ddR );
-    }
-
-    // set the stop time parameter
-    p->dd->TimeStop  = p->pPars->TimeTarget;
-    p->ddG->TimeStop = p->pPars->TimeTarget;
-    p->ddR->TimeStop = p->pPars->TimeTarget;
-
-    // create bad state in the ring manager
-    p->ddR->bFunc  = Llb_BddComputeBad( p->pAigGlo, 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 );
-
-    // derive constraints
-    bConstrCs = Llb_ManCreateConstraints( p, vHints, 0 );   Cudd_Ref( bConstrCs );
-    bConstrNs = Llb_ManCreateConstraints( p, vHints, 1 );   Cudd_Ref( bConstrNs );
-//Extra_bddPrint( p->dd, bConstrCs ); printf( "\n" );
-//Extra_bddPrint( p->dd, bConstrNs ); printf( "\n" );
-
-    // perform reachability analysis
-    // compute the starting set of states
-    if ( p->ddG->bFunc )
-    {
-        bReached = p->ddG->bFunc; p->ddG->bFunc = NULL;
-        bCurrent = Extra_TransferPermute( p->ddG, p->dd, bReached, pGlo2Cs );    Cudd_Ref( bCurrent );
-    }
-    else
-    {
-        bReached = Llb_ManComputeInitState( p, p->ddG );                         Cudd_Ref( bReached );
-        bCurrent = Llb_ManComputeInitState( p, p->dd  );                         Cudd_Ref( bCurrent );
-    }
-//Extra_bddPrintSupport( p->ddG, bReached ); printf( "\n" );
-//Extra_bddPrintSupport( p->dd,  bCurrent ); printf( "\n" );
-
-//Extra_bddPrintSupport( p->dd, bCurrent ); printf( "\n" );
-    for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ )
-    { 
-        clk2 = Abc_Clock();
-        // check the runtime limit
-        if ( p->pPars->TimeLimit && Abc_Clock() > p->pPars->TimeTarget )
-        {
-            if ( !p->pPars->fSilent )
-                printf( "Reached timeout during image computation (%d seconds).\n",  p->pPars->TimeLimit );
-            p->pPars->iFrame = nIters - 1;
-            Cudd_RecursiveDeref( p->dd,  bCurrent );  bCurrent = NULL;
-            Cudd_RecursiveDeref( p->dd,  bConstrCs ); bConstrCs = NULL;
-            Cudd_RecursiveDeref( p->dd,  bConstrNs ); bConstrNs = NULL;
-            Cudd_RecursiveDeref( p->ddG, bReached );  bReached = NULL;
-            return -1;
-        }
-
-        // save the onion ring
-        bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, pCs2Glo );
-        if ( bTemp == NULL )
-        {
-            if ( !p->pPars->fSilent )
-                printf( "Reached timeout (%d seconds) during ring transfer.\n",  p->pPars->TimeLimit );
-            p->pPars->iFrame = nIters - 1;
-            Cudd_RecursiveDeref( p->dd,  bCurrent );  bCurrent = NULL;
-            Cudd_RecursiveDeref( p->dd,  bConstrCs ); bConstrCs = NULL;
-            Cudd_RecursiveDeref( p->dd,  bConstrNs ); bConstrNs = NULL;
-            Cudd_RecursiveDeref( p->ddG, bReached );  bReached = NULL;
-            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->pAigGlo->pSeqModel == NULL );
-            if ( !p->pPars->fBackward )
-                p->pAigGlo->pSeqModel = Llb_ManReachDeriveCex( p ); 
-            if ( !p->pPars->fSilent )
-            {
-                if ( !p->pPars->fBackward )
-                    Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", p->pAigGlo->pSeqModel->iPo, p->pAigGlo->pName, p->pAigGlo->pName, nIters );
-                else
-                    Abc_Print( 1, "Output ??? of miter \"%s\" was asserted in frame %d (counter-example is not produced).  ", p->pAigGlo->pName, nIters );
-                Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
-            }
-            p->pPars->iFrame = nIters - 1;
-            Cudd_RecursiveDeref( p->dd,  bCurrent );  bCurrent = NULL;
-            Cudd_RecursiveDeref( p->dd,  bConstrCs ); bConstrCs = NULL;
-            Cudd_RecursiveDeref( p->dd,  bConstrNs ); bConstrNs = NULL;
-            Cudd_RecursiveDeref( p->ddG, bReached );  bReached = NULL;
-            return 0; 
-        }
-
-        // restrict reachable states using constraints
-        if ( vHints )
-        {
-            bCurrent = Cudd_bddAnd( p->dd, bTemp = bCurrent, bConstrCs );                                Cudd_Ref( bCurrent );
-            Cudd_RecursiveDeref( p->dd, bTemp );
-        }
-
-        // quantify variables appearing only in the init state
-        bCube    = Llb_ManConstructQuantCubeIntern( p, (Llb_Grp_t *)Vec_PtrEntry(p->vGroups,0), 0, 0 );  Cudd_Ref( bCube );
-        bCurrent = Cudd_bddExistAbstract( p->dd, bTemp = bCurrent, bCube );                              Cudd_Ref( bCurrent );
-        Cudd_RecursiveDeref( p->dd, bTemp );
-        Cudd_RecursiveDeref( p->dd, bCube );
-
-        // compute the next states
-        bNext = Llb_ManComputeImage( p, bCurrent, 0 );
-        if ( bNext == NULL )
-        {
-            if ( !p->pPars->fSilent )
-                printf( "Reached timeout (%d seconds) during image computation.\n",  p->pPars->TimeLimit );
-            p->pPars->iFrame = nIters - 1;
-            Cudd_RecursiveDeref( p->dd,  bCurrent );   bCurrent = NULL;
-            Cudd_RecursiveDeref( p->dd,  bConstrCs );  bConstrCs = NULL;
-            Cudd_RecursiveDeref( p->dd,  bConstrNs );  bConstrNs = NULL;
-            Cudd_RecursiveDeref( p->ddG, bReached );   bReached = NULL;
-            return -1;
-        }
-        Cudd_Ref( bNext );
-        Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
-
-        // restrict reachable states using constraints
-        if ( vHints )
-        {
-            bNext = Cudd_bddAnd( p->dd, bTemp = bNext, bConstrNs );                Cudd_Ref( bNext );
-            Cudd_RecursiveDeref( p->dd, bTemp );
-        }
-//Extra_bddPrintSupport( p->dd, bNext ); printf( "\n" );
-
-        // remap these states into the current state vars
-//        bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pNs2Glo );    Cudd_Ref( bNext );
-//        Cudd_RecursiveDeref( p->dd, bTemp );
-//        bNext = Extra_TransferPermuteTime( p->dd, p->ddG, bTemp = bNext, pNs2Glo, p->pPars->TimeTarget );    
-        bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pNs2Glo );    
-        if ( bNext == 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,  bTemp );  
-            Cudd_RecursiveDeref( p->dd,  bConstrCs );  bConstrCs = NULL;
-            Cudd_RecursiveDeref( p->dd,  bConstrNs );  bConstrNs = NULL;
-            Cudd_RecursiveDeref( p->ddG, bReached );   bReached = NULL;
-            return -1;
-        }
-        Cudd_Ref( bNext );
-        Cudd_RecursiveDeref( p->dd, bTemp );  
-
-
-        // check if there are any new states
-        if ( Cudd_bddLeq( p->ddG, bNext, bReached ) ) // implication = no new states
-        {
-            Cudd_RecursiveDeref( p->ddG,  bNext );     bNext = NULL;
-            break;
-        }
-
-        // check the BDD size
-        nBddSize = Cudd_DagSize(bNext);
-        if ( nBddSize > p->pPars->nBddMax )
-        {
-            Cudd_RecursiveDeref( p->ddG,  bNext );     bNext = NULL;
-            break;
-        }
-
-        // get the new states
-        bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) );
-        if ( bCurrent == NULL )
-        {
-            Cudd_RecursiveDeref( p->ddG,  bNext );        bNext = NULL;
-            Cudd_RecursiveDeref( p->ddG,  bReached );     bReached = NULL;
-            break;
-        }
-        Cudd_Ref( bCurrent );
-        // minimize the new states with the reached states
-//        bCurrent = Cudd_bddConstrain( p->ddG, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
-//        bCurrent = Cudd_bddRestrict( p->ddG, bTemp = bCurrent, Cudd_Not(bReached) );  Cudd_Ref( bCurrent );
-//        Cudd_RecursiveDeref( p->ddG, bTemp );
-//printf( "Initial BDD =%7d. Constrained BDD =%7d.\n", Cudd_DagSize(bTemp), Cudd_DagSize(bCurrent) );
-
-        // remap these states into the current state vars
-//        bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs );   Cudd_Ref( bCurrent );
-//        Cudd_RecursiveDeref( p->ddG, bTemp );
-//        bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs, p->pPars->TimeTarget );    
-        bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs );    
-        if ( bCurrent == 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;
-            Cudd_RecursiveDeref( p->ddG, bTemp );  
-            Cudd_RecursiveDeref( p->dd,  bConstrCs );  bConstrCs = NULL;
-            Cudd_RecursiveDeref( p->dd,  bConstrNs );  bConstrNs = NULL;
-            Cudd_RecursiveDeref( p->ddG, bReached );   bReached = NULL;
-            return -1;
-        }
-        Cudd_Ref( bCurrent );
-        Cudd_RecursiveDeref( p->ddG, bTemp ); 
-        
-
-        // add to the reached states
-        bReached = Cudd_bddOr( p->ddG, bTemp = bReached, bNext );                       
-        if ( bReached == NULL )
-        {
-            Cudd_RecursiveDeref( p->ddG,  bTemp );     bTemp = NULL;
-            Cudd_RecursiveDeref( p->ddG,  bNext );     bNext = NULL;
-            break;
-        }
-        Cudd_Ref( bReached );
-        Cudd_RecursiveDeref( p->ddG, bTemp );
-        Cudd_RecursiveDeref( p->ddG, bNext );
-        bNext = NULL;
-
-        if ( p->pPars->fVerbose )
-        {
-            fprintf( stdout, "F =%5d : ",    nIters );
-            fprintf( stdout, "Im =%6d  ",    nBddSize );
-            fprintf( stdout, "(%4d %3d)   ", Cudd_ReadReorderings(p->dd),  Cudd_ReadGarbageCollections(p->dd) );
-            fprintf( stdout, "Rea =%6d  ",   Cudd_DagSize(bReached) );
-            fprintf( stdout, "(%4d%4d)   ",  Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) );
-            Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
-        }
-/*
-        if ( p->pPars->fVerbose )
-        {
-            double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) );
-//            Extra_bddPrint( p->ddG, bReached );printf( "\n" );
-            fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
-            fflush( stdout ); 
-        }
-*/
-    }
-    Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
-    Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
-    if ( bReached == NULL )
-    {
-        p->pPars->iFrame = nIters - 1;
-        return 0; // reachable
-    }
-//    assert( bCurrent == NULL );
-    if ( bCurrent )
-        Cudd_RecursiveDeref( p->dd, bCurrent );
-    // report the stats
-    if ( p->pPars->fVerbose )
-    {
-        double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) );
-        if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax )
-            fprintf( stdout, "Reachability analysis is stopped after %d frames.\n", nIters );
-        else
-            fprintf( stdout, "Reachability analysis completed after %d frames.\n", nIters );
-        fprintf( stdout, "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;
-        Cudd_RecursiveDeref( p->ddG, bReached );
-        return -1; // undecided
-    }
-    if ( pddGlo ) 
-    {
-        assert( p->ddG->bFunc == NULL );
-        p->ddG->bFunc = bReached; bReached = NULL;
-        assert( *pddGlo == NULL );
-        *pddGlo = p->ddG;  p->ddG = NULL;
-    }
-    else
-        Cudd_RecursiveDeref( p->ddG, bReached );
-    if ( !p->pPars->fSilent )
-        printf( "The miter is proved unreachable after %d iterations.  ", nIters );
-    p->pPars->iFrame = nIters - 1;
-    return 1; // unreachable
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-