Added timeout to &reachn.

6 files changed, 114 insertions, 1505 deletions

diff --git a/src/aig/llb/llb2Bad.c b/src/aig/llb/llb2Bad.c
index 8322698b..4099805b 100644
--- a/src/aig/llb/llb2Bad.c
+++ b/src/aig/llb/llb2Bad.c
@@ -42,12 +42,12 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd )
+DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut )
 {
     Vec_Ptr_t * vNodes;
     DdNode * bBdd0, * bBdd1, * bTemp, * bResult;
     Aig_Obj_t * pObj;
-    int i;
+    int i, k;
     assert( Cudd_ReadSize(dd) == Aig_ManPiNum(pInit) );
     // initialize elementary variables
     Aig_ManConst1(pInit)->pData = Cudd_ReadOne( dd );
@@ -64,6 +64,14 @@ DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd )
         bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
         bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
         pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );          Cudd_Ref( (DdNode *)pObj->pData );
+
+        if ( i % 10 == 0 && TimeOut && clock() >= TimeOut )
+        {
+            Vec_PtrForEachEntryStop( Aig_Obj_t *, vNodes, pObj, k, i+1 )
+                Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
+            Vec_PtrFree( vNodes );
+            return NULL;
+        }
     }
     // quantify PIs of each PO
     bResult = Cudd_ReadLogicZero( dd );  Cudd_Ref( bResult );
diff --git a/src/aig/llb/llb2Core.c b/src/aig/llb/llb2Core.c
index e440438f..45add7e9 100644
--- a/src/aig/llb/llb2Core.c
+++ b/src/aig/llb/llb2Core.c
@@ -217,10 +217,17 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
     // compute initial states
     if ( p->pPars->fBackward )
     {
+        // create init state in the global manager
+        bTemp = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeLimit );   
+        if ( bTemp == NULL )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
+            return -1;
+        }
+        Cudd_Ref( bTemp );
         // create bad state in the ring manager
         p->ddR->bFunc = Llb_CoreComputeCube( p->ddR, p->vVarsCs, 0, NULL );      Cudd_Ref( p->ddR->bFunc );
-        // create init state in the global manager
-        bTemp    = Llb_BddComputeBad( p->pInit, p->ddR );                        Cudd_Ref( bTemp );
         bCurrent = Llb_BddQuantifyPis( p->pInit, p->ddR, bTemp );                Cudd_Ref( bCurrent );
         Cudd_RecursiveDeref( p->ddR, bTemp );
         bReached = Cudd_bddTransfer( p->ddR, p->ddG, bCurrent );                 Cudd_Ref( bReached );
@@ -231,7 +238,16 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
     else
     {
         // create bad state in the ring manager
-        p->ddR->bFunc = Llb_BddComputeBad( p->pInit, p->ddR );                   Cudd_Ref( p->ddR->bFunc );
+        p->ddR->bFunc = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeLimit );  
+        if ( p->ddR->bFunc == NULL )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
+            return -1;
+        }
+        if ( p->ddR->bFunc == NULL )
+            return -1;
+        Cudd_Ref( p->ddR->bFunc );
         // create init state in the working and global manager
         bCurrent = Llb_CoreComputeCube( p->dd,  p->vVarsCs, 1, NULL );           Cudd_Ref( bCurrent );
         bReached = Llb_CoreComputeCube( p->ddG, p->vVarsCs, 0, NULL );           Cudd_Ref( bReached );
diff --git a/src/aig/llb/llb3Image.c b/src/aig/llb/llb3Image.c
index 1866a87c..87e09c46 100644
--- a/src/aig/llb/llb3Image.c
+++ b/src/aig/llb/llb3Image.c
@@ -524,7 +524,7 @@ Vec_Ptr_t * Llb_NonlinCutNodes( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * v
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Llb_NonlinBuildBdds( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, DdManager * dd )
+Vec_Ptr_t * Llb_NonlinBuildBdds( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, DdManager * dd, int TimeOut )
 {
     Vec_Ptr_t * vNodes, * vResult;
     Aig_Obj_t * pObj;
@@ -541,6 +541,15 @@ Vec_Ptr_t * Llb_NonlinBuildBdds( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t *
         bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
         bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
         pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );   Cudd_Ref( (DdNode *)pObj->pData );
+
+        if ( i % 10 == 0 && TimeOut && clock() >= TimeOut )
+        {
+            Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+                if ( pObj->pData )
+                    Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
+            Vec_PtrFree( vNodes );
+            return NULL;
+        }
     }
 
     vResult = Vec_PtrAlloc( 100 );
@@ -600,14 +609,16 @@ void Llb_NonlinAddPair( Llb_Mgr_t * p, DdNode * bFunc, int iPart, int iVar )
   SeeAlso     []
 
 ***********************************************************************/
-void Llb_NonlinStart( Llb_Mgr_t * p )
+int Llb_NonlinStart( Llb_Mgr_t * p, int TimeOut )
 {
     Vec_Ptr_t * vRootBdds;
     Llb_Prt_t * pPart;
     DdNode * bFunc;
     int i, k, nSuppSize;
     // create and collect BDDs
-    vRootBdds = Llb_NonlinBuildBdds( p->pAig, p->vLeaves, p->vRoots, p->dd ); // come referenced
+    vRootBdds = Llb_NonlinBuildBdds( p->pAig, p->vLeaves, p->vRoots, p->dd, TimeOut ); // come referenced
+    if ( vRootBdds == NULL )
+        return 0;
     Vec_PtrPush( vRootBdds, p->bCurrent );
     // add pairs (refs are consumed inside)
     Vec_PtrForEachEntry( DdNode *, vRootBdds, bFunc, i )
@@ -634,6 +645,7 @@ void Llb_NonlinStart( Llb_Mgr_t * p )
     Llb_MgrForEachPart( p, pPart, i )
         if ( Llb_NonlinHasSingletonVars(p, pPart) )
             Llb_NonlinQuantify1( p, pPart, 0 );
+    return 1;
 }
 
 /**Function*************************************************************
@@ -844,7 +856,7 @@ void Llb_NonlinFree( Llb_Mgr_t * p )
 
 ***********************************************************************/
 DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, 
-    DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder, int Limit )
+    DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder, int Limit, int TimeOut )
 {
     Llb_Prt_t * pPart, * pPart1, * pPart2;
     Llb_Mgr_t * p;
@@ -854,7 +866,11 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo
     // start the manager
     clk2 = clock();
     p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd, bCurrent );
-    Llb_NonlinStart( p );
+    if ( !Llb_NonlinStart( p, TimeOut ) )
+    {
+        Llb_NonlinFree( p );
+        return NULL;
+    }
     timeBuild += clock() - clk2;
     timeInside = clock() - clk2;
     // compute scores
diff --git a/src/aig/llb/llb3Nonlin.c b/src/aig/llb/llb3Nonlin.c
index c22f5a0c..59304768 100644
--- a/src/aig/llb/llb3Nonlin.c
+++ b/src/aig/llb/llb3Nonlin.c
@@ -294,7 +294,7 @@ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p )
 //Extra_bddPrintSupport( p->dd, bRing );   printf( "\n" );
         // compute the next states
         bImage = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bState, 
-            p->pPars->fReorder, p->pPars->fVeryVerbose, p->pOrder, ABC_INFINITY ); // consumed reference
+            p->pPars->fReorder, p->pPars->fVeryVerbose, p->pOrder, ABC_INFINITY, ABC_INFINITY ); // consumed reference
         assert( bImage != NULL );
         Cudd_Ref( bImage );
 //Extra_bddPrintSupport( p->dd, bImage );  printf( "\n" );
@@ -340,6 +340,44 @@ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p )
     return pCex;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Perform reachability with hints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_NonlinReoHook( DdManager * dd, char * Type, void * Method )
+{
+    Aig_Man_t * pAig = (Aig_Man_t *)dd->bFunc;
+    Aig_Obj_t * pObj;
+    int i;
+    printf( "Order: " );
+    for ( i = 0; i < Cudd_ReadSize(dd); i++ )
+    {
+        pObj = Aig_ManObj( pAig, i );
+        if ( pObj == NULL )
+            continue;
+        if ( Saig_ObjIsPi(pAig, pObj) )
+            printf( "pi" );
+        else if ( Saig_ObjIsLo(pAig, pObj) )
+            printf( "lo" );
+        else if ( Saig_ObjIsPo(pAig, pObj) )
+            printf( "po" );
+        else if ( Saig_ObjIsLi(pAig, pObj) )
+            printf( "li" );
+        else continue;
+        printf( "%d=%d ", i, dd->perm[i] );
+    }
+    printf( "\n" );
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Perform reachability with hints.]
@@ -364,8 +402,20 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
     else
         p->pPars->TimeTarget = 0;
 
+    // set reordering hooks
+    assert( p->dd->bFunc == NULL );
+//    p->dd->bFunc = (DdNode *)p->pAig;
+//    Cudd_AddHook( p->dd, Llb_NonlinReoHook, CUDD_POST_REORDERING_HOOK );
+
     // create bad state in the ring manager
-    p->ddR->bFunc  = Llb_BddComputeBad( p->pInit, p->ddR );          Cudd_Ref( p->ddR->bFunc );
+    p->ddR->bFunc  = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeTarget );          
+    if ( p->ddR->bFunc == NULL )
+    {
+        if ( !p->pPars->fSilent )
+            printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
+        return -1;
+    }
+    Cudd_Ref( p->ddR->bFunc );
     // compute the starting set of states
     bCurrent       = Llb_NonlinComputeInitState( p->pAig, p->dd );   Cudd_Ref( bCurrent );
     p->ddG->bFunc  = Llb_NonlinComputeInitState( p->pAig, p->ddG );  Cudd_Ref( p->ddG->bFunc );  // reached
@@ -429,8 +479,16 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
         nBddSize0 = Cudd_DagSize( bCurrent );
         bNext = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bCurrent, 
 //            p->pPars->fReorder, p->pPars->fVeryVerbose, p->pOrder, nIters ? p->pPars->nBddMax : ABC_INFINITY );
-            p->pPars->fReorder, p->pPars->fVeryVerbose, p->pOrder, ABC_INFINITY );
+            p->pPars->fReorder, p->pPars->fVeryVerbose, p->pOrder, ABC_INFINITY, p->pPars->TimeTarget );
 //        Abc_PrintTime( 1, "Image time", clock() - clk3 );
+        if ( bNext == NULL )
+        {
+            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;
+            return -1;
+        }
         if ( bNext == NULL )  // Llb_NonlimImage() consumes reference of bCurrent!!!
         {
             DdNode * bVar, * bVarG;
@@ -632,6 +690,7 @@ void Llb_MnnStop( Llb_Mnn_t * p )
         ABC_PRTP( "  reo    ", p->timeReo,   p->timeTotal );
         ABC_PRTP( "  reoG   ", p->timeReoG,  p->timeTotal );
     }
+    p->dd->bFunc = NULL;
     if ( p->ddR->bFunc )
         Cudd_RecursiveDeref( p->ddR, p->ddR->bFunc );
     Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
diff --git a/src/aig/llb/llb3Nonlin_multi.c b/src/aig/llb/llb3Nonlin_multi.c
deleted file mode 100644
index 22ff2491..00000000
--- a/src/aig/llb/llb3Nonlin_multi.c
+++ /dev/null
@@ -1,1490 +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"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Llb_Var_t_ Llb_Var_t;
-struct Llb_Var_t_ 
-{
-    int           iVar;      // variable number
-    int           nScore;    // variable score
-    Vec_Int_t *   vParts;    // partitions
-};
-
-typedef struct Llb_Prt_t_ Llb_Prt_t;
-struct Llb_Prt_t_ 
-{
-    int           iPart;     // partition number
-    int           nSize;     // the number of BDD nodes
-    DdNode *      bFunc;     // the partition
-    Vec_Int_t *   vVars;     // support
-};
-
-typedef struct Llb_Mgr_t_ Llb_Mgr_t;
-struct Llb_Mgr_t_
-{
-    Aig_Man_t *   pAig;      // AIG manager
-    Vec_Ptr_t *   vLeaves;   // leaves in the AIG manager
-    Vec_Ptr_t *   vRoots;    // roots in the AIG manager
-    DdManager *   dd;        // working BDD manager
-    Vec_Ptr_t *   vFuncs;    // current state functions in terms of vLeaves
-    int *         pVars2Q;   // variables to quantify
-    // internal
-    Llb_Prt_t **  pParts;    // partitions
-    Llb_Var_t **  pVars;     // variables
-    int           iPartFree; // next free partition
-    int           nVars;     // the number of BDD variables
-    int           nSuppMax;  // maximum support size
-    // temporary
-    int *         pSupp;     // temporary support storage
-};
-
-static inline Llb_Var_t * Llb_MgrVar( Llb_Mgr_t * p, int i )   { return p->pVars[i];  }
-static inline Llb_Prt_t * Llb_MgrPart( Llb_Mgr_t * p, int i )  { return p->pParts[i]; }
-
-// iterator over vars
-#define Llb_MgrForEachVar( p, pVar, i )     \
-    for ( i = 0; (i < p->nVars) && (((pVar) = Llb_MgrVar(p, i)), 1); i++ ) if ( pVar == NULL ) {} else
-// iterator over parts
-#define Llb_MgrForEachPart( p, pPart, i )   \
-    for ( i = 0; (i < p->iPartFree) && (((pPart) = Llb_MgrPart(p, i)), 1); i++ ) if ( pPart == NULL ) {} else
-
-// iterator over vars of one partition
-#define Llb_PartForEachVar( p, pPart, pVar, i )   \
-    for ( i = 0; (i < Vec_IntSize(pPart->vVars)) && (((pVar) = Llb_MgrVar(p, Vec_IntEntry(pPart->vVars,i))), 1); i++ )
-// iterator over parts of one variable
-#define Llb_VarForEachPart( p, pVar, pPart, i )   \
-    for ( i = 0; (i < Vec_IntSize(pVar->vParts)) && (((pPart) = Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,i))), 1); i++ )
-
-static int timeBuild, timeAndEx, timeOther;
-static int nSuppMax;
-
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Finds variable whose 0-cofactor is the smallest.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Llb_NonlinFindBestVar( DdManager * dd, DdNode * bFunc, Vec_Int_t * vVars )
-{
-    DdNode * bCof, * bVar;
-    int i, iVar, iVarBest = -1;
-    int Size, Size0, Size1;
-    if ( vVars == NULL )
-        vVars = Vec_IntStartNatural( Cudd_ReadSize(dd) );
-    printf( "\nOriginal = %6d.  SuppSize = %3d. Vars = %3d.\n", 
-        Size = Cudd_DagSize(bFunc), Cudd_SupportSize(dd, bFunc), Vec_IntSize(vVars) );
-    Vec_IntForEachEntry( vVars, iVar, i )
-    {
-        printf( "Var =%3d : ", iVar );
-        bVar = Cudd_bddIthVar(dd, iVar);
-
-        bCof = Cudd_Cofactor( dd, bFunc, Cudd_Not(bVar) );      Cudd_Ref( bCof );
-        printf( "Supp0 =%3d  ",    Cudd_SupportSize(dd, bCof) );
-        printf( "Size0 =%6d   ", Size0 = Cudd_DagSize(bCof) );
-        Cudd_RecursiveDeref( dd, bCof );
-
-        bCof = Cudd_Cofactor( dd, bFunc, bVar );                Cudd_Ref( bCof );
-        printf( "Supp1 =%3d  ",    Cudd_SupportSize(dd, bCof) );
-        printf( "Size1 =%6d   ", Size1 = Cudd_DagSize(bCof) );
-        Cudd_RecursiveDeref( dd, bCof );
-
-        printf( "D =%6d  ", Size0 + Size1 - Size );
-        printf( "B =%6d\n", ABC_MAX(Size0, Size1) - ABC_MIN(Size0, Size1) );
-    }
-    return iVarBest;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Finds variable whose 0-cofactor is the smallest.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Llb_NonlinTrySubsetting( DdManager * dd, DdNode * bFunc )
-{
-    DdNode * bNew;
-    printf( "Original = %6d.  SuppSize = %3d.    ", 
-        Cudd_DagSize(bFunc), Cudd_SupportSize(dd, bFunc) );
-    bNew = Cudd_SubsetHeavyBranch( dd, bFunc, Cudd_SupportSize(dd, bFunc), 1000 );  Cudd_Ref( bNew );
-    printf( "Result   = %6d.  SuppSize = %3d.\n", 
-        Cudd_DagSize(bNew), Cudd_SupportSize(dd, bNew) );
-    Cudd_RecursiveDeref( dd, bNew );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Removes one variable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Llb_NonlinRemoveVar( Llb_Mgr_t * p, Llb_Var_t * pVar )
-{
-    assert( p->pVars[pVar->iVar] == pVar );
-    p->pVars[pVar->iVar] = NULL;
-    Vec_IntFree( pVar->vParts );
-    ABC_FREE( pVar );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Removes one partition.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Llb_NonlinRemovePart( Llb_Mgr_t * p, Llb_Prt_t * pPart )
-{
-    assert( p->pParts[pPart->iPart] == pPart );
-    p->pParts[pPart->iPart] = NULL;
-    Vec_IntFree( pPart->vVars );
-    Cudd_RecursiveDeref( p->dd, pPart->bFunc );
-    ABC_FREE( pPart );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Create cube with singleton variables.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Llb_NonlinCreateCube1( Llb_Mgr_t * p, Llb_Prt_t * pPart )
-{
-    DdNode * bCube, * bTemp;
-    Llb_Var_t * pVar;
-    int i;
-    bCube = Cudd_ReadOne(p->dd);   Cudd_Ref( bCube );
-    Llb_PartForEachVar( p, pPart, pVar, i )
-    {
-        assert( Vec_IntSize(pVar->vParts) > 0 );
-        if ( Vec_IntSize(pVar->vParts) != 1 )
-            continue;
-        assert( Vec_IntEntry(pVar->vParts, 0) == pPart->iPart );
-        bCube = Cudd_bddAnd( p->dd, bTemp = bCube, Cudd_bddIthVar(p->dd, pVar->iVar) ); Cudd_Ref( bCube );
-        Cudd_RecursiveDeref( p->dd, bTemp );
-    }
-    Cudd_Deref( bCube );
-    return bCube;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Create cube of variables appearing only in two partitions.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Llb_NonlinCreateCube2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2 )
-{
-    DdNode * bCube, * bTemp;
-    Llb_Var_t * pVar;
-    int i;
-    bCube = Cudd_ReadOne(p->dd);   Cudd_Ref( bCube );
-    Llb_PartForEachVar( p, pPart1, pVar, i )
-    {
-        assert( Vec_IntSize(pVar->vParts) > 0 );
-        if ( Vec_IntSize(pVar->vParts) != 2 )
-            continue;
-        if ( (Vec_IntEntry(pVar->vParts, 0) == pPart1->iPart && Vec_IntEntry(pVar->vParts, 1) == pPart2->iPart) ||
-             (Vec_IntEntry(pVar->vParts, 0) == pPart2->iPart && Vec_IntEntry(pVar->vParts, 1) == pPart1->iPart) )
-        {
-            bCube = Cudd_bddAnd( p->dd, bTemp = bCube, Cudd_bddIthVar(p->dd, pVar->iVar) );   Cudd_Ref( bCube );
-            Cudd_RecursiveDeref( p->dd, bTemp );
-        }
-    }
-    Cudd_Deref( bCube );
-    return bCube;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if partition has singleton variables.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Llb_NonlinHasSingletonVars( Llb_Mgr_t * p, Llb_Prt_t * pPart )
-{
-    Llb_Var_t * pVar;
-    int i;
-    Llb_PartForEachVar( p, pPart, pVar, i )
-        if ( Vec_IntSize(pVar->vParts) == 1 )
-            return 1;
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if partition has singleton variables.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Llb_NonlinPrint( Llb_Mgr_t * p )
-{
-    Llb_Prt_t * pPart;
-    Llb_Var_t * pVar;
-    int i, k;
-    printf( "\n" );
-    Llb_MgrForEachVar( p, pVar, i )
-    {
-        printf( "Var %3d : ", i );
-        Llb_VarForEachPart( p, pVar, pPart, k )
-            printf( "%d ", pPart->iPart );
-        printf( "\n" );
-    }
-    Llb_MgrForEachPart( p, pPart, i )
-    {
-        printf( "Part %3d : ", i );
-        Llb_PartForEachVar( p, pPart, pVar, k )
-            printf( "%d ", pVar->iVar );
-        printf( "\n" );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Quantifies singles belonging to one partition.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Llb_NonlinQuantify1( Llb_Mgr_t * p, Llb_Prt_t * pPart, int fSubset )
-{
-    Llb_Var_t * pVar;
-    Llb_Prt_t * pTemp;
-    Vec_Ptr_t * vSingles;
-    DdNode * bCube, * bTemp;
-    int i, RetValue, nSizeNew;
-    if ( fSubset )
-    {        
-        int Length;
-//        int nSuppSize = Cudd_SupportSize( p->dd, pPart->bFunc );
-//        pPart->bFunc = Cudd_SubsetHeavyBranch( p->dd, bTemp = pPart->bFunc, nSuppSize, 3*pPart->nSize/4 );  Cudd_Ref( pPart->bFunc );
-        pPart->bFunc = Cudd_LargestCube( p->dd, bTemp = pPart->bFunc, &Length );  Cudd_Ref( pPart->bFunc );
-
-        printf( "Subsetting %3d : ", pPart->iPart );
-        printf( "(Supp =%3d  Node =%5d) -> ", Cudd_SupportSize(p->dd, bTemp),        Cudd_DagSize(bTemp) );
-        printf( "(Supp =%3d  Node =%5d)\n",   Cudd_SupportSize(p->dd, pPart->bFunc), Cudd_DagSize(pPart->bFunc) );
-
-        RetValue = (Cudd_DagSize(bTemp) == Cudd_DagSize(pPart->bFunc));
-
-        Cudd_RecursiveDeref( p->dd, bTemp );
-
-        if ( RetValue )
-            return 1;
-    }
-    else
-    {
-        // create cube to be quantified
-        bCube = Llb_NonlinCreateCube1( p, pPart );   Cudd_Ref( bCube );
-//        assert( !Cudd_IsConstant(bCube) );
-        // derive new function
-        pPart->bFunc = Cudd_bddExistAbstract( p->dd, bTemp = pPart->bFunc, bCube );  Cudd_Ref( pPart->bFunc );
-        Cudd_RecursiveDeref( p->dd, bTemp );
-        Cudd_RecursiveDeref( p->dd, bCube );
-    }
-    // get support
-    vSingles = Vec_PtrAlloc( 0 );
-    nSizeNew = Cudd_DagSize(pPart->bFunc);
-    Extra_SupportArray( p->dd, pPart->bFunc, p->pSupp );
-    Llb_PartForEachVar( p, pPart, pVar, i )
-        if ( p->pSupp[pVar->iVar] )
-        {
-            assert( Vec_IntSize(pVar->vParts) > 1 );
-            pVar->nScore -= pPart->nSize - nSizeNew;
-        }
-        else
-        {
-            RetValue = Vec_IntRemove( pVar->vParts, pPart->iPart );
-            assert( RetValue );
-            pVar->nScore -= pPart->nSize;
-            if ( Vec_IntSize(pVar->vParts) == 0 )
-                Llb_NonlinRemoveVar( p, pVar );
-            else if ( Vec_IntSize(pVar->vParts) == 1 )
-                Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) );
-        }
-
-    // update partition
-    pPart->nSize = nSizeNew;
-    Vec_IntClear( pPart->vVars );
-    for ( i = 0; i < p->nVars; i++ )
-        if ( p->pSupp[i] && p->pVars2Q[i] )
-            Vec_IntPush( pPart->vVars, i );
-    // remove other variables
-    Vec_PtrForEachEntry( Llb_Prt_t *, vSingles, pTemp, i )
-        Llb_NonlinQuantify1( p, pTemp, 0 );
-    Vec_PtrFree( vSingles );
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Quantifies singles belonging to one partition.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Llb_NonlinQuantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2, int Limit )
-{
-    int fVerbose = 0;
-    Llb_Var_t * pVar;
-    Llb_Prt_t * pTemp;
-    Vec_Ptr_t * vSingles;
-    DdNode * bCube, * bFunc;
-    int i, RetValue, nSuppSize;
-    int iPart1 = pPart1->iPart;
-    int iPart2 = pPart2->iPart;
-/*
-    if ( iPart1 == 91 && iPart2 == 134 )
-    {
-        fVerbose = 1;
-    }
-*/
-    // create cube to be quantified
-    bCube = Llb_NonlinCreateCube2( p, pPart1, pPart2 );   Cudd_Ref( bCube );
-if ( fVerbose )
-{
-printf( "\n" );
-printf( "\n" );
-Llb_NonlinPrint( p );
-printf( "Conjoining partitions %d and %d.\n", pPart1->iPart, pPart2->iPart );
-Extra_bddPrintSupport( p->dd, bCube );  printf( "\n" );
-}
-
-    // derive new function
-//    bFunc = Cudd_bddAndAbstract( p->dd, pPart1->bFunc, pPart2->bFunc, bCube );  Cudd_Ref( bFunc );
-    bFunc = Cudd_bddAndAbstractLimit( p->dd, pPart1->bFunc, pPart2->bFunc, bCube, Limit );  
-    if ( bFunc == NULL )
-    {
-        int RetValue;
-        Cudd_RecursiveDeref( p->dd, bCube );
-        if ( pPart1->nSize < pPart2->nSize )
-            RetValue = Llb_NonlinQuantify1( p, pPart1, 1 );
-        else
-            RetValue = Llb_NonlinQuantify1( p, pPart2, 1 );
-        if ( RetValue )
-            Limit = Limit + 1000;
-
-        Llb_NonlinQuantify2( p, pPart1, pPart2, Limit );
-        return 1;
-    }
-    Cudd_Ref( bFunc );
-    Cudd_RecursiveDeref( p->dd, bCube );
-    // create new partition
-    pTemp = p->pParts[p->iPartFree] = ABC_CALLOC( Llb_Prt_t, 1 );
-    pTemp->iPart = p->iPartFree++;
-    pTemp->nSize = Cudd_DagSize(bFunc);
-    pTemp->bFunc = bFunc;
-    pTemp->vVars = Vec_IntAlloc( 8 );
-    // update variables
-    Llb_PartForEachVar( p, pPart1, pVar, i )
-    {
-        RetValue = Vec_IntRemove( pVar->vParts, pPart1->iPart );
-        assert( RetValue );
-        pVar->nScore -= pPart1->nSize;
-    }
-    // update variables
-    Llb_PartForEachVar( p, pPart2, pVar, i )
-    {
-        RetValue = Vec_IntRemove( pVar->vParts, pPart2->iPart );
-        assert( RetValue );
-        pVar->nScore -= pPart2->nSize;
-    }
-    // add variables to the new partition
-    nSuppSize = 0;
-    Extra_SupportArray( p->dd, bFunc, p->pSupp );
-    for ( i = 0; i < p->nVars; i++ )
-    {
-        nSuppSize += p->pSupp[i];
-        if ( p->pSupp[i] && p->pVars2Q[i] )
-        {
-            pVar = Llb_MgrVar( p, i );
-            pVar->nScore += pTemp->nSize;
-            Vec_IntPush( pVar->vParts, pTemp->iPart );
-            Vec_IntPush( pTemp->vVars, i );
-        }
-    }
-    p->nSuppMax = ABC_MAX( p->nSuppMax, nSuppSize ); 
-    // remove variables and collect partitions with singleton variables
-    vSingles = Vec_PtrAlloc( 0 );
-    Llb_PartForEachVar( p, pPart1, pVar, i )
-    {
-        if ( Vec_IntSize(pVar->vParts) == 0 )
-            Llb_NonlinRemoveVar( p, pVar );
-        else if ( Vec_IntSize(pVar->vParts) == 1 )
-        {
-            if ( fVerbose )
-                printf( "Adding partition %d because of var %d.\n", 
-                    Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0))->iPart, pVar->iVar );
-            Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) );
-        }
-    }
-    Llb_PartForEachVar( p, pPart2, pVar, i )
-    {
-        if ( pVar == NULL )
-            continue;
-        if ( Vec_IntSize(pVar->vParts) == 0 )
-            Llb_NonlinRemoveVar( p, pVar );
-        else if ( Vec_IntSize(pVar->vParts) == 1 )
-        {
-            if ( fVerbose )
-                printf( "Adding partition %d because of var %d.\n", 
-                    Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0))->iPart, pVar->iVar );
-            Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) );
-        }
-    }
-    // remove partitions
-    Llb_NonlinRemovePart( p, pPart1 );
-    Llb_NonlinRemovePart( p, pPart2 );
-    // remove other variables
-if ( fVerbose )
-Llb_NonlinPrint( p );
-    Vec_PtrForEachEntry( Llb_Prt_t *, vSingles, pTemp, i )
-    {
-if ( fVerbose )
-printf( "Updating partitiong %d with singlton vars.\n", pTemp->iPart );
-        Llb_NonlinQuantify1( p, pTemp, 0 );
-    }
-if ( fVerbose )
-Llb_NonlinPrint( p );
-    Vec_PtrFree( vSingles );
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes volume of the cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Llb_NonlinCutNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
-{
-    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
-        return;
-    Aig_ObjSetTravIdCurrent(p, pObj);
-    if ( Saig_ObjIsLi(p, pObj) )
-    {
-        Llb_NonlinCutNodes_rec(p, Aig_ObjFanin0(pObj), vNodes);
-        return;
-    }
-    if ( Aig_ObjIsConst1(pObj) )
-        return;
-    assert( Aig_ObjIsNode(pObj) );
-    Llb_NonlinCutNodes_rec(p, Aig_ObjFanin0(pObj), vNodes);
-    Llb_NonlinCutNodes_rec(p, Aig_ObjFanin1(pObj), vNodes);
-    Vec_PtrPush( vNodes, pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes volume of the cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Llb_NonlinCutNodes( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper )
-{
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj;
-    int i;
-    // mark the lower cut with the traversal ID
-    Aig_ManIncrementTravId(p);
-    Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i )
-        Aig_ObjSetTravIdCurrent( p, pObj );
-    // count the upper cut
-    vNodes = Vec_PtrAlloc( 100 );
-    Vec_PtrForEachEntry( Aig_Obj_t *, vUpper, pObj, i )
-        Llb_NonlinCutNodes_rec( p, pObj, vNodes );
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns array of BDDs for the roots in terms of the leaves.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Llb_NonlinBuildBdds( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, DdManager * dd )
-{
-    Vec_Ptr_t * vNodes, * vResult;
-    Aig_Obj_t * pObj;
-    DdNode * bBdd0, * bBdd1, * bProd;
-    int i;
-
-    Aig_ManConst1(p)->pData = Cudd_ReadOne( dd );
-    Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i )
-        pObj->pData = Cudd_bddIthVar( dd, Aig_ObjId(pObj) );
-
-    vNodes = Llb_NonlinCutNodes( p, vLower, vUpper );
-    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
-    {
-        bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
-        bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
-        pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );   Cudd_Ref( (DdNode *)pObj->pData );
-    }
-
-    vResult = Vec_PtrAlloc( 100 );
-    Vec_PtrForEachEntry( Aig_Obj_t *, vUpper, pObj, i )
-    {
-        if ( Aig_ObjIsNode(pObj) )
-        {
-            bProd = Cudd_bddXnor( dd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)), (DdNode *)pObj->pData );  Cudd_Ref( bProd );
-        }
-        else
-        {
-            assert( Saig_ObjIsLi(p, pObj) );
-            bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
-            bProd = Cudd_bddXnor( dd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)), bBdd0 );                  Cudd_Ref( bProd );
-        }
-        Vec_PtrPush( vResult, bProd );
-    }
-    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
-        Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
-
-    Vec_PtrFree( vNodes );
-    return vResult;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Starts non-linear quantification scheduling.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Llb_NonlinAddPair( Llb_Mgr_t * p, DdNode * bFunc, int iPart, int iVar )
-{
-    if ( p->pVars[iVar] == NULL )
-    {
-        p->pVars[iVar] = ABC_CALLOC( Llb_Var_t, 1 );
-        p->pVars[iVar]->iVar   = iVar;
-        p->pVars[iVar]->nScore = 0;
-        p->pVars[iVar]->vParts = Vec_IntAlloc( 8 );
-    }
-    Vec_IntPush( p->pVars[iVar]->vParts, iPart );
-    Vec_IntPush( p->pParts[iPart]->vVars, iVar );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Starts non-linear quantification scheduling.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Llb_NonlinStart( Llb_Mgr_t * p )
-{
-    Vec_Ptr_t * vRootBdds;
-    Llb_Prt_t * pPart;
-    DdNode * bFunc;
-    int i, k, nSuppSize;
-    // create and collect BDDs
-    vRootBdds = Llb_NonlinBuildBdds( p->pAig, p->vLeaves, p->vRoots, p->dd ); // come referenced
-    Vec_PtrForEachEntry( DdNode *, p->vFuncs, bFunc, i )
-        Vec_PtrPush( vRootBdds, bFunc );
-    // add pairs (refs are consumed inside)
-    Vec_PtrForEachEntry( DdNode *, vRootBdds, bFunc, i )
-    {
-        assert( !Cudd_IsConstant(bFunc) );
-        // create partition
-        p->pParts[i] = ABC_CALLOC( Llb_Prt_t, 1 );
-        p->pParts[i]->iPart = i;
-        p->pParts[i]->bFunc = bFunc;
-        p->pParts[i]->vVars = Vec_IntAlloc( 8 );
-        // add support dependencies
-        nSuppSize = 0;
-        Extra_SupportArray( p->dd, bFunc, p->pSupp );
-        for ( k = 0; k < p->nVars; k++ )
-        {
-            nSuppSize += p->pSupp[k];
-            if ( p->pSupp[k] && p->pVars2Q[k] )
-                Llb_NonlinAddPair( p, bFunc, i, k );
-        }
-        p->nSuppMax = ABC_MAX( p->nSuppMax, nSuppSize ); 
-    }
-    Vec_PtrFree( vRootBdds );
-    // remove singles
-    Llb_MgrForEachPart( p, pPart, i )
-        if ( Llb_NonlinHasSingletonVars(p, pPart) )
-            Llb_NonlinQuantify1( p, pPart, 0 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Starts non-linear quantification scheduling.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Llb_Mgr_t * Llb_NonlinAlloc( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, DdManager * dd, Vec_Ptr_t * vFuncs )
-{
-    Llb_Mgr_t * p;
-    p = ABC_CALLOC( Llb_Mgr_t, 1 );
-    p->pAig      = pAig;
-    p->vLeaves   = vLeaves;
-    p->vRoots    = vRoots;
-    p->dd        = dd;
-    p->vFuncs    = vFuncs;
-    p->pVars2Q   = pVars2Q;
-    p->nVars     = Cudd_ReadSize(dd);
-    p->iPartFree = Vec_PtrSize(vRoots) + Vec_PtrSize(vFuncs);
-    p->pVars     = ABC_CALLOC( Llb_Var_t *, p->nVars );
-    p->pParts    = ABC_CALLOC( Llb_Prt_t *, 2 * p->iPartFree );
-    p->pSupp     = ABC_ALLOC( int, Cudd_ReadSize(dd) );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops non-linear quantification scheduling.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Llb_NonlinFree( Llb_Mgr_t * p )
-{
-    Llb_Prt_t * pPart;
-    Llb_Var_t * pVar;
-    int i;
-    Llb_MgrForEachVar( p, pVar, i )
-        Llb_NonlinRemoveVar( p, pVar );
-    Llb_MgrForEachPart( p, pPart, i )
-        Llb_NonlinRemovePart( p, pPart );
-    ABC_FREE( p->pVars );
-    ABC_FREE( p->pParts );
-    ABC_FREE( p->pSupp );
-    ABC_FREE( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks that each var appears in at least one partition.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Llb_NonlinCheckVars( Llb_Mgr_t * p )
-{
-    Llb_Var_t * pVar;
-    int i;
-    Llb_MgrForEachVar( p, pVar, i )
-        assert( Vec_IntSize(pVar->vParts) > 1 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Find next partition to quantify]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Llb_NonlinNextPartitions( Llb_Mgr_t * p, Llb_Prt_t ** ppPart1, Llb_Prt_t ** ppPart2 )
-{
-    Llb_Var_t * pVar, * pVarBest = NULL;
-    Llb_Prt_t * pPart, * pPart1Best = NULL, * pPart2Best = NULL;
-    int i;
-    Llb_NonlinCheckVars( p );
-    // find variable with minimum score
-    Llb_MgrForEachVar( p, pVar, i )
-        if ( pVarBest == NULL || pVarBest->nScore > pVar->nScore )
-            pVarBest = pVar;
-    if ( pVarBest == NULL )
-        return 0;
-    // find two partitions with minimum size
-    Llb_VarForEachPart( p, pVarBest, pPart, i )
-    {
-        if ( pPart1Best == NULL )
-            pPart1Best = pPart;
-        else if ( pPart2Best == NULL )
-            pPart2Best = pPart;
-        else if ( pPart1Best->nSize > pPart->nSize || pPart2Best->nSize > pPart->nSize )
-        {
-            if ( pPart1Best->nSize > pPart2Best->nSize )
-                pPart1Best = pPart;
-            else
-                pPart2Best = pPart;
-        }
-    }
-    *ppPart1 = pPart1Best;
-    *ppPart2 = pPart2Best;
-    return 1; 
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reorders BDDs in the working manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Llb_NonlinReorder( DdManager * dd, int fVerbose )
-{
-    int clk = clock();
-    if ( fVerbose )
-        Abc_Print( 1, "Reordering... Before =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
-    Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
-    if ( fVerbose )
-        Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
-    Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
-    if ( fVerbose )
-        Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
-    if ( fVerbose )
-        Abc_PrintTime( 1, "Time", clock() - clk );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recomputes scores after variable reordering.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Llb_NonlinRecomputeScores( Llb_Mgr_t * p )
-{
-    Llb_Prt_t * pPart;
-    Llb_Var_t * pVar;
-    int i, k;
-    Llb_MgrForEachPart( p, pPart, i )
-        pPart->nSize = Cudd_DagSize(pPart->bFunc);
-    Llb_MgrForEachVar( p, pVar, i )
-    {
-        pVar->nScore = 0;
-        Llb_VarForEachPart( p, pVar, pPart, k )
-            pVar->nScore += pPart->nSize;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recomputes scores after variable reordering.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Llb_NonlinVerifyScores( Llb_Mgr_t * p )
-{
-    Llb_Prt_t * pPart;
-    Llb_Var_t * pVar;
-    int i, k, nScore;
-    Llb_MgrForEachPart( p, pPart, i )
-        assert( pPart->nSize == Cudd_DagSize(pPart->bFunc) );
-    Llb_MgrForEachVar( p, pVar, i )
-    {
-        nScore = 0;
-        Llb_VarForEachPart( p, pVar, pPart, k )
-            nScore += pPart->nSize;
-        assert( nScore == pVar->nScore );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs image computation.]
-
-  Description [Computes image of BDDs (vFuncs).]
-               
-  SideEffects [BDDs in vFuncs are derefed inside. The result is refed.]
-
-  SeeAlso     []
-
-***********************************************************************/
-int Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, 
-    DdManager * dd, Vec_Ptr_t * vFuncs, int fReorder, int fVerbose, int * pOrder, int * pfSubset, int Limit )
-{
-    Llb_Prt_t * pPart, * pPart1, * pPart2;
-    Llb_Mgr_t * p;
-    int i, nReorders, timeInside, fSubset = 0;
-    int clk = clock(), clk2;
-    // start the manager
-    clk2 = clock();
-    p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd, vFuncs );
-    Llb_NonlinStart( p );
-    timeBuild += clock() - clk2;
-    timeInside = clock() - clk2;
-    // reorder variables
-//    if ( fReorder )
-//        Llb_NonlinReorder( dd, fVerbose );
-    // compute scores
-    Llb_NonlinRecomputeScores( p );
-    // save permutation
-    memcpy( pOrder, dd->invperm, sizeof(int) * dd->size );
-    // iteratively quantify variables
-    while ( Llb_NonlinNextPartitions(p, &pPart1, &pPart2) )
-    {
-        nReorders = Cudd_ReadReorderings(dd);
-        clk2 = clock();
-        fSubset |= Llb_NonlinQuantify2( p, pPart1, pPart2, Limit );
-        timeAndEx += clock() - clk2;
-        timeInside += clock() - clk2;
-        if ( nReorders < Cudd_ReadReorderings(dd) )
-            Llb_NonlinRecomputeScores( p );
-//        else
-//            Llb_NonlinVerifyScores( p );
-    }
-    // load partitions
-    Vec_PtrClear( vFuncs );
-    Llb_MgrForEachPart( p, pPart, i )
-    {
-        Vec_PtrPush( vFuncs, pPart->bFunc );
-        Cudd_Ref( pPart->bFunc );
-    }
-    nSuppMax = p->nSuppMax;
-    Llb_NonlinFree( p );
-    // reorder variables
-    if ( fReorder )
-        Llb_NonlinReorder( dd, fVerbose );
-    timeOther += clock() - clk - timeInside;
-    if ( pfSubset )
-        *pfSubset |= fSubset;
-    return 1;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Llb_NonlinPrepareVarMap( Aig_Man_t * pAig, Vec_Int_t ** pvNs2Glo, Vec_Int_t ** pvGlo2Cs )
-{
-    Aig_Obj_t * pObjLi, * pObjLo;
-    int i, iVarLi, iVarLo;
-    *pvNs2Glo = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
-    *pvGlo2Cs = Vec_IntStartFull( Aig_ManRegNum(pAig) );
-    Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
-    {
-        iVarLi = Aig_ObjId(pObjLi);
-        iVarLo = Aig_ObjId(pObjLo);
-        assert( iVarLi >= 0 && iVarLi < Aig_ManObjNumMax(pAig) );
-        assert( iVarLo >= 0 && iVarLo < Aig_ManObjNumMax(pAig) );
-        Vec_IntWriteEntry( *pvNs2Glo, iVarLi, i );
-        Vec_IntWriteEntry( *pvGlo2Cs, i, iVarLo );
-    }
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd )
-{
-    Aig_Obj_t * pObj;
-    DdNode * bRes, * bVar, * bTemp;
-    int i, iVar;
-    bRes = Cudd_ReadOne( dd );   Cudd_Ref( bRes );
-    Saig_ManForEachLo( pAig, pObj, i )
-    {
-        iVar = (Cudd_ReadSize(dd) == Aig_ManRegNum(pAig)) ? i : Aig_ObjId(pObj);
-        bVar = Cudd_bddIthVar( dd, iVar );
-        bRes = Cudd_bddAnd( dd, bTemp = bRes, Cudd_Not(bVar) );  Cudd_Ref( bRes );
-        Cudd_RecursiveDeref( dd, bTemp );
-    }
-    Cudd_Deref( bRes );
-    return bRes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Llb_NonlinComputeInitStateVec( Aig_Man_t * pAig, DdManager * dd )
-{
-    Vec_Ptr_t * vFuncs;
-    Aig_Obj_t * pObj;
-    DdNode * bVar;
-    int i;
-    vFuncs = Vec_PtrAlloc( Aig_ManRegNum(pAig) );
-    Saig_ManForEachLo( pAig, pObj, i )
-    {
-        bVar = Cudd_bddIthVar( dd, Aig_ObjId(pObj) );  Cudd_Ref( bVar );
-        Vec_PtrPush( vFuncs, Cudd_Not(bVar) );
-    }
-    return vFuncs;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Llb_NonlinDerefVec( DdManager * dd, Vec_Ptr_t * vFuncs )
-{
-    DdNode * bFunc;
-    int i;
-    Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i )
-        Cudd_RecursiveDeref( dd, bFunc );
-    Vec_PtrFree( vFuncs );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Llb_NonlinTransferVec( DdManager * dd, DdManager * ddG, Vec_Ptr_t * vFuncs, Vec_Int_t * vNs2Glo )
-{
-    DdNode * bFunc, * bTemp;
-    int i;
-    Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i )
-    {
-        bFunc = Extra_TransferPermute( dd, ddG, bTemp = bFunc, Vec_IntArray(vNs2Glo) );    Cudd_Ref( bFunc );
-        Cudd_RecursiveDeref( dd, bTemp );
-        Vec_PtrWriteEntry( vFuncs, i, bFunc );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Llb_NonlinSharpVec( DdManager * ddG, DdNode * bReached, Vec_Ptr_t * vFuncs )
-{
-    DdNode * bFunc, * bTemp;
-    int i;
-    Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i )
-    {
-        bFunc = Cudd_bddAnd( ddG, bTemp = bFunc, Cudd_Not(bReached) );   Cudd_Ref( bFunc );
-        Cudd_RecursiveDeref( ddG, bTemp );
-        Vec_PtrWriteEntry( vFuncs, i, bFunc );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Llb_NonlinAddToReachVec( DdManager * ddG, DdNode * bReached, Vec_Ptr_t * vFuncs )
-{
-    DdNode * bFunc, * bProd, * bTemp;
-    int i;
-    bProd = Cudd_ReadOne( ddG );  Cudd_Ref( bProd );
-    Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i )
-    {
-        bProd = Cudd_bddAnd( ddG, bTemp = bProd, bFunc );     Cudd_Ref( bProd );
-        Cudd_RecursiveDeref( ddG, bTemp );
-    }
-    if ( Cudd_IsConstant(bProd) )
-    {
-        Cudd_RecursiveDeref( ddG, bProd );
-        return NULL;
-    }
-    bTemp = Cudd_bddOr( ddG, bReached, bProd );   Cudd_Ref( bTemp );
-    Cudd_RecursiveDeref( ddG, bProd );
-    Cudd_Deref( bTemp );
-    return bTemp;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Llb_NonlinCreateReachVec( DdManager * dd, DdManager * ddG, DdNode * bReachG, Vec_Int_t * vGlo2Cs )
-{
-    Vec_Ptr_t * vFuncs;
-    DdNode * bFunc;
-    vFuncs = Vec_PtrAlloc( 1 );
-    bFunc = Extra_TransferPermute( ddG, dd, bReachG, Vec_IntArray(vGlo2Cs) );    Cudd_Ref( bFunc );
-    Vec_PtrPush( vFuncs, bFunc );
-//    Llb_NonlinReorder( dd, 1 );
-    return vFuncs;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Llb_NonlinPrintVec( DdManager * dd, Vec_Ptr_t * vFuncs )
-{
-    DdNode * bFunc;
-    int i;
-    Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i )
-    {
-        printf( "%2d :  ", i );
-        printf( "Support =%5d  ", Cudd_SupportSize(dd, bFunc) );
-        printf( "DagSize =%7d\n", Cudd_DagSize(bFunc) );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Perform reachability with hints.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Llb_NonlinReachability( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
-{ 
-    Aig_Obj_t * pObj;
-    Vec_Ptr_t * vLeaves, * vRoots, * vParts;
-    Vec_Int_t * vNs2Glo, * vGlo2Cs;
-    DdManager * dd, * ddG;
-    DdNode * bReached, * bTemp;
-    int i, nIters, nBddSize0, nBddSize, Limit, fSubset, * pVars2Q, * pOrder;
-    int clk2, clk3, clk = clock();
-//    int RetValue;
-    int timeImage = 0;
-    int timeTran1 = 0;
-    int timeTran2 = 0;
-    int timeGloba = 0;
-    int timeOther = 0;
-    int timeTotal = 0;
-    int timeReo   = 0;
-    int timeReoG  = 0;
-    assert( Aig_ManRegNum(pAig) > 0 );
-    timeBuild = timeAndEx = timeOther = 0;
-
-    // compute time to stop
-    if ( pPars->TimeLimit )
-        pPars->TimeTarget = clock() + pPars->TimeLimit * CLOCKS_PER_SEC;
-    else
-        pPars->TimeTarget = 0;
-
-    // create leaves
-    vLeaves = Vec_PtrAlloc( Aig_ManPiNum(pAig) );
-    Aig_ManForEachPi( pAig, pObj, i )
-        Vec_PtrPush( vLeaves, pObj );
-
-    // create roots
-    vRoots = Vec_PtrAlloc( Aig_ManPoNum(pAig) );
-    Saig_ManForEachLi( pAig, pObj, i )
-        Vec_PtrPush( vRoots, pObj );
-
-    // variables to quantify
-    pOrder  = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
-    pVars2Q = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
-    Aig_ManForEachPi( pAig, pObj, i )
-        pVars2Q[Aig_ObjId(pObj)] = 1;
-
-    // start the managers
-    Llb_NonlinPrepareVarMap( pAig, &vNs2Glo, &vGlo2Cs ); 
-    dd  = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    ddG = Cudd_Init( Aig_ManRegNum(pAig),    0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
-    Cudd_AutodynEnable( ddG, CUDD_REORDER_SYMM_SIFT );
-
-    // compute the starting set of states
-    vParts   = Llb_NonlinComputeInitStateVec( pAig, dd );
-    bReached = Llb_NonlinComputeInitState( pAig, ddG );          Cudd_Ref( bReached );
-    fSubset  = 1;
-    for ( Limit = pPars->nBddMax; fSubset; Limit *= 2 )
-    {
-        if ( pPars->fVerbose )
-        printf( "*********** LIMIT %d ************\n", Limit );
-        fSubset = 0;
-        for ( nIters = 0; nIters < pPars->nIterMax; nIters++ )
-        { 
-            clk2 = clock();
-            // check the runtime limit
-            if ( pPars->TimeLimit && clock() >= pPars->TimeTarget )
-            {
-                if ( !pPars->fSilent )
-                    printf( "Reached timeout during image computation (%d seconds).\n",  pPars->TimeLimit );
-                pPars->iFrame = nIters - 1;
-                Llb_NonlinDerefVec( dd, vParts );      vParts = NULL;
-                Cudd_RecursiveDeref( ddG, bReached );  bReached = NULL;
-                return -1;
-            }
-
-//            Llb_NonlinReorder( dd, 1 );
-
-            // compute the next states
-            clk3 = clock();
-            nBddSize0 = Cudd_SharingSize( (DdNode **)Vec_PtrArray(vParts), Vec_PtrSize(vParts) );
-            if ( !Llb_NonlinImage( pAig, vLeaves, vRoots, pVars2Q, dd, vParts, pPars->fReorder, pPars->fVeryVerbose, pOrder, &fSubset, Limit ) )
-            {
-                if ( !pPars->fSilent )
-                    printf( "Reached timeout during image computation (%d seconds).\n",  pPars->TimeLimit );
-                pPars->iFrame = nIters - 1;
-                Llb_NonlinDerefVec( dd, vParts );      vParts = NULL;
-                Cudd_RecursiveDeref( ddG, bReached );  bReached = NULL;
-                return -1;
-            }
-            timeImage += clock() - clk3;
-            nBddSize = Cudd_SharingSize( (DdNode **)Vec_PtrArray(vParts), Vec_PtrSize(vParts) );
-//            Llb_NonlinPrintVec( dd, vParts );
-
-            // check containment in reached and derive new frontier
-            clk3 = clock();
-            Llb_NonlinTransferVec( dd, ddG, vParts, vNs2Glo );
-            timeTran1 += clock() - clk3;
-
-            clk3 = clock();
-            Llb_NonlinSharpVec( ddG, bReached, vParts );
-            bReached = Llb_NonlinAddToReachVec( ddG, bTemp = bReached, vParts );
-            if ( bReached == NULL )
-            {
-                bReached = bTemp;
-                Llb_NonlinDerefVec( ddG, vParts );      vParts = NULL;
-                if ( fSubset )
-                    vParts = Llb_NonlinCreateReachVec( dd, ddG, bReached, vGlo2Cs );
-                break;
-            }
-            Cudd_Ref( bReached );
-            Cudd_RecursiveDeref( ddG, bTemp );
-            timeGloba += clock() - clk3;
-
-            // reset permutation
-    //        RetValue = Cudd_CheckZeroRef( dd );
-    //        assert( RetValue == 0 );
-    //        Cudd_ShuffleHeap( dd, pOrder );
-
-            clk3 = clock();
-            Llb_NonlinTransferVec( ddG, dd, vParts, vGlo2Cs );
-//            Llb_NonlinDerefVec( ddG, vParts );      vParts = NULL;
-//            vParts = Llb_NonlinCreateReachVec( dd, ddG, bReached, vGlo2Cs );
-            timeTran2 += clock() - clk3;
-
-            // report the results
-            if ( pPars->fVerbose )
-            {
-                printf( "I =%3d : ",   nIters );
-                printf( "Fr =%6d ",    nBddSize0 );
-                printf( "Im =%6d  ",   nBddSize );
-                printf( "(%4d %3d)  ", Cudd_ReadReorderings(dd),  Cudd_ReadGarbageCollections(dd) );
-                printf( "Rea =%6d  ",  Cudd_DagSize(bReached) );
-                printf( "(%4d %3d)  ", Cudd_ReadReorderings(ddG), Cudd_ReadGarbageCollections(ddG) );
-                printf( "S =%4d ",     nSuppMax );
-                printf( "P =%2d  ",    Vec_PtrSize(vParts) );
-                Abc_PrintTime( 1, "T", clock() - clk2 );
-            }
-    /*
-            if ( pPars->fVerbose )
-            {
-                double nMints = Cudd_CountMinterm(ddG, bReached, Saig_ManRegNum(pAig) );
-    //            Extra_bddPrint( ddG, bReached );printf( "\n" );
-                printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(pAig)) );
-                fflush( stdout ); 
-            }
-    */
-
-            if ( nIters == pPars->nIterMax - 1 )
-            {
-                if ( !pPars->fSilent )
-                    printf( "Reached limit on the number of timeframes (%d).\n",  pPars->nIterMax );
-                pPars->iFrame = nIters;
-                Llb_NonlinDerefVec( dd, vParts );      vParts = NULL;
-                Cudd_RecursiveDeref( ddG, bReached );  bReached = NULL;
-                return -1;
-            }
-
-//            Llb_NonlinReorder( ddG, 1 );
-//            Llb_NonlinFindBestVar( ddG, bReached, NULL );
-        }
-    } 
-    
-    if ( bReached == NULL )
-        return 0; // reachable
-    // report the stats
-    if ( pPars->fVerbose )
-    {
-        double nMints = Cudd_CountMinterm(ddG, bReached, Saig_ManRegNum(pAig) );
-        if ( nIters >= pPars->nIterMax || nBddSize > pPars->nBddMax )
-            printf( "Reachability analysis is stopped after %d frames.\n", nIters );
-        else
-            printf( "Reachability analysis completed after %d frames.\n", nIters );
-        printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(pAig)) );
-        fflush( stdout ); 
-    }
-    if ( nIters >= pPars->nIterMax || nBddSize > pPars->nBddMax )
-    {
-        if ( !pPars->fSilent )
-            printf( "Verified only for states reachable in %d frames.  ", nIters );
-        Cudd_RecursiveDeref( ddG, bReached );
-        return -1; // undecided
-    }
-    // cleanup
-    Cudd_RecursiveDeref( ddG, bReached );
-    timeReo  = Cudd_ReadReorderingTime(dd);
-    timeReoG = Cudd_ReadReorderingTime(ddG);
-    Extra_StopManager( dd );
-    Extra_StopManager( ddG );
-    // cleanup
-    Vec_IntFree( vNs2Glo );
-    Vec_IntFree( vGlo2Cs );
-    Vec_PtrFree( vLeaves );
-    Vec_PtrFree( vRoots );
-    ABC_FREE( pVars2Q );
-    ABC_FREE( pOrder );
-    // report
-    if ( !pPars->fSilent )
-        printf( "The miter is proved unreachable after %d iterations.  ", nIters );
-    pPars->iFrame = nIters - 1;
-    Abc_PrintTime( 1, "Time", clock() - clk );
-
-    if ( pPars->fVerbose ) 
-    {
-        timeTotal = clock() - clk;
-        timeOther = timeTotal - timeImage - timeTran1 - timeTran2 - timeGloba;
-        ABC_PRTP( "Image    ", timeImage, timeTotal );
-        ABC_PRTP( "  build  ", timeBuild, timeTotal );
-        ABC_PRTP( "  and-ex ", timeAndEx, timeTotal );
-        ABC_PRTP( "  other  ", timeOther, timeTotal );
-        ABC_PRTP( "Transfer1", timeTran1, timeTotal );
-        ABC_PRTP( "Transfer2", timeTran2, timeTotal );
-        ABC_PRTP( "Global   ", timeGloba, timeTotal );
-        ABC_PRTP( "Other    ", timeOther, timeTotal );
-        ABC_PRTP( "TOTAL    ", timeTotal, timeTotal );
-        ABC_PRTP( "  reo    ", timeReo,   timeTotal );
-        ABC_PRTP( "  reoG   ", timeReoG,  timeTotal );
-    }
-    return 1; // unreachable
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Finds balanced cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Llb_NonlinExperiment( Aig_Man_t * pAig, int Num )
-{
-    Gia_ParLlb_t Pars, * pPars = &Pars;
-    Aig_Man_t * p;
-
-    Llb_ManSetDefaultParams( pPars );
-    pPars->fVerbose = 1;
-
-    p = Aig_ManDupFlopsOnly( pAig );
-//Aig_ManShow( p, 0, NULL );
-    Aig_ManPrintStats( pAig );
-    Aig_ManPrintStats( p );
-
-    Llb_NonlinReachability( p, pPars );
-
-    Aig_ManStop( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Finds balanced cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Llb_NonlinCoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
-{
-    Aig_Man_t * p;
-    int RetValue = -1;
-
-    p = Aig_ManDupFlopsOnly( pAig );
-//Aig_ManShow( p, 0, NULL );
-    if ( pPars->fVerbose )
-    Aig_ManPrintStats( pAig );
-    if ( pPars->fVerbose )
-    Aig_ManPrintStats( p );
-
-    if ( !pPars->fSkipReach )
-        RetValue = Llb_NonlinReachability( p, pPars );
-
-    Aig_ManStop( p );
-    return RetValue;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/llb/llbInt.h b/src/aig/llb/llbInt.h
index 80f391fe..36d3796c 100644
--- a/src/aig/llb/llbInt.h
+++ b/src/aig/llb/llbInt.h
@@ -146,7 +146,7 @@ extern int             Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, D
 extern void            Llb_MtrSchedule( Llb_Mtr_t * p );
 
 /*=== llb2Bad.c ======================================================*/
-extern DdNode *        Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd );
+extern DdNode *        Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut );
 extern DdNode *        Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc );
 /*=== llb2Core.c ======================================================*/
 extern DdNode *        Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarIndex, char * pValues );
@@ -168,7 +168,7 @@ extern DdNode *        Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMan
 
 /*=== llb3Image.c ======================================================*/
 extern DdNode *        Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, 
-                           DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder, int Limit );
+                           DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder, int Limit, int TimeLimit );
 
 ABC_NAMESPACE_HEADER_END