Changes to be able to compile ABC without CUDD.

1 files changed, 0 insertions, 1185 deletions

diff --git a/src/proof/llb/llb4Nonlin.c b/src/proof/llb/llb4Nonlin.c
deleted file mode 100644
index a9421358..00000000
--- a/src/proof/llb/llb4Nonlin.c
+++ /dev/null
@@ -1,1185 +0,0 @@
-/**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
-