Cumulative update to BDD-based reachability, speeding up &reachm and other changes.

4 files changed, 279 insertions, 126 deletions

diff --git a/src/aig/llb/llb3Image.c b/src/aig/llb/llb3Image.c
index 2c16c550..098f9f45 100644
--- a/src/aig/llb/llb3Image.c
+++ b/src/aig/llb/llb3Image.c
@@ -50,7 +50,6 @@ struct Llb_Mgr_t_
     Vec_Ptr_t *   vLeaves;   // leaves in the AIG manager
     Vec_Ptr_t *   vRoots;    // roots in the AIG manager
     DdManager *   dd;        // working BDD manager
-    DdNode *      bCurrent;  // current state functions in terms of vLeaves
     int *         pVars2Q;   // variables to quantify
     // internal
     Llb_Prt_t **  pParts;    // partitions
@@ -624,42 +623,51 @@ void Llb_NonlinAddPair( Llb_Mgr_t * p, DdNode * bFunc, int iPart, int iVar )
   SeeAlso     []
 
 ***********************************************************************/
+void Llb_NonlinAddPartition( Llb_Mgr_t * p, int i, DdNode * bFunc )
+{
+    int k, nSuppSize;
+    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 ); 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts non-linear quantification scheduling.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Llb_NonlinStart( Llb_Mgr_t * p, int TimeOut )
 {
     Vec_Ptr_t * vRootBdds;
-    Llb_Prt_t * pPart;
     DdNode * bFunc;
-    int i, k, nSuppSize;
+    int i;
     // create and collect BDDs
     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 )
-    {
-        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 ); 
-    }
+        Llb_NonlinAddPartition( p, i, bFunc );
     Vec_PtrFree( vRootBdds );
-    // remove singles
-    Llb_MgrForEachPart( p, pPart, i )
-        if ( Llb_NonlinHasSingletonVars(p, pPart) )
-            Llb_NonlinQuantify1( p, pPart, 0 );
     return 1;
 }
 
@@ -672,8 +680,7 @@ int Llb_NonlinStart( Llb_Mgr_t * p, int TimeOut )
   SideEffects []
 
   SeeAlso     []
-
-***********************************************************************/
+**********************************************************************/
 void Llb_NonlinCheckVars( Llb_Mgr_t * p )
 {
     Llb_Var_t * pVar;
@@ -736,7 +743,7 @@ int Llb_NonlinNextPartitions( Llb_Mgr_t * p, Llb_Prt_t ** ppPart1, Llb_Prt_t **
   SeeAlso     []
 
 ***********************************************************************/
-void Llb_NonlinReorder( DdManager * dd, int fVerbose )
+void Llb_NonlinReorder( DdManager * dd, int fTwice, int fVerbose )
 {
     int clk = clock();
     if ( fVerbose )
@@ -744,9 +751,12 @@ void Llb_NonlinReorder( DdManager * dd, int fVerbose )
     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 ( fTwice )
+    {
+        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
+        if ( fVerbose )
+            Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+    }
     if ( fVerbose )
         Abc_PrintTime( 1, "Time", clock() - clk );
 }
@@ -815,7 +825,7 @@ void Llb_NonlinVerifyScores( Llb_Mgr_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Llb_Mgr_t * Llb_NonlinAlloc( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, DdManager * dd, DdNode * bCurrent )
+Llb_Mgr_t * Llb_NonlinAlloc( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, DdManager * dd )
 {
     Llb_Mgr_t * p;
     p = ABC_CALLOC( Llb_Mgr_t, 1 );
@@ -823,12 +833,11 @@ Llb_Mgr_t * Llb_NonlinAlloc( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t *
     p->vLeaves   = vLeaves;
     p->vRoots    = vRoots;
     p->dd        = dd;
-    p->bCurrent  = bCurrent;
     p->pVars2Q   = pVars2Q;
     p->nVars     = Cudd_ReadSize(dd);
-    p->iPartFree = Vec_PtrSize(vRoots) + 1;
+    p->iPartFree = Vec_PtrSize(vRoots);
     p->pVars     = ABC_CALLOC( Llb_Var_t *, p->nVars );
-    p->pParts    = ABC_CALLOC( Llb_Prt_t *, 2 * p->iPartFree );
+    p->pParts    = ABC_CALLOC( Llb_Prt_t *, 2 * p->iPartFree + 2 );
     p->pSupp     = ABC_ALLOC( int, Cudd_ReadSize(dd) );
     return p;
 }
@@ -880,17 +889,24 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo
     int clk = clock(), clk2;
     // start the manager
     clk2 = clock();
-    p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd, bCurrent );
+    p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd );
     if ( !Llb_NonlinStart( p, TimeOut ) )
     {
         Llb_NonlinFree( p );
         return NULL;
     }
+    // add partition
+    Llb_NonlinAddPartition( p, p->iPartFree++, bCurrent );
+    // remove singles
+    Llb_MgrForEachPart( p, pPart, i )
+        if ( Llb_NonlinHasSingletonVars(p, pPart) )
+            Llb_NonlinQuantify1( p, pPart, 0 );
     timeBuild += clock() - clk2;
     timeInside = clock() - clk2;
     // compute scores
     Llb_NonlinRecomputeScores( p );
     // save permutation
+    if ( pOrder )
     memcpy( pOrder, dd->invperm, sizeof(int) * dd->size );
     // iteratively quantify variables
     while ( Llb_NonlinNextPartitions(p, &pPart1, &pPart2) )
@@ -913,6 +929,111 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo
     bFunc = Cudd_ReadOne(p->dd);   Cudd_Ref( bFunc );
     Llb_MgrForEachPart( p, pPart, i )
     {
+        bFunc = Cudd_bddAnd( p->dd, bTemp = bFunc, pPart->bFunc );   Cudd_Ref( bFunc );
+        Cudd_RecursiveDeref( p->dd, bTemp );
+    }
+    nSuppMax = p->nSuppMax;
+    Llb_NonlinFree( p );
+    // reorder variables
+    if ( fReorder )
+        Llb_NonlinReorder( dd, 0, fVerbose );
+    timeOther += clock() - clk - timeInside;
+    // return
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+
+
+
+static Llb_Mgr_t * p = NULL;
+
+/**Function*************************************************************
+
+  Synopsis    [Starts image computation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst )
+{
+    DdManager * dd;
+    int clk = clock();
+    assert( p == NULL );
+    // start a new manager (disable reordering)
+    dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    Cudd_ShuffleHeap( dd, pOrder );
+//    if ( fFirst )
+        Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
+    // start the manager
+    p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd );
+    if ( !Llb_NonlinStart( p, 0 ) )
+    {
+        Llb_NonlinFree( p );
+        return NULL;
+    }
+    timeBuild += clock() - clk;
+//    if ( !fFirst )
+//        Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
+    return dd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs image computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int fVerbose, int * pOrder )
+{
+    Llb_Prt_t * pPart, * pPart1, * pPart2;
+    DdNode * bFunc, * bTemp;
+    int i, nReorders, timeInside = 0;
+    int clk = clock(), clk2;
+
+    // add partition
+    Llb_NonlinAddPartition( p, p->iPartFree++, bCurrent );
+    // remove singles
+    Llb_MgrForEachPart( p, pPart, i )
+        if ( Llb_NonlinHasSingletonVars(p, pPart) )
+            Llb_NonlinQuantify1( p, pPart, 0 );
+    // reorder
+    if ( fReorder )
+        Llb_NonlinReorder( p->dd, 0, 0 );
+    // save permutation
+    memcpy( pOrder, p->dd->invperm, sizeof(int) * p->dd->size );
+
+    // compute scores
+    Llb_NonlinRecomputeScores( p );
+    // iteratively quantify variables
+    while ( Llb_NonlinNextPartitions(p, &pPart1, &pPart2) )
+    {
+        clk2 = clock();
+        nReorders = Cudd_ReadReorderings(p->dd);
+        if ( !Llb_NonlinQuantify2( p, pPart1, pPart2, 0, 0 ) )
+        {
+            Llb_NonlinFree( p );
+            return NULL;
+        }
+        timeAndEx  += clock() - clk2;
+        timeInside += clock() - clk2;
+        if ( nReorders < Cudd_ReadReorderings(p->dd) )
+            Llb_NonlinRecomputeScores( p );
+//        else
+//            Llb_NonlinVerifyScores( p );
+    }
+    // load partitions
+    bFunc = Cudd_ReadOne(p->dd);   Cudd_Ref( bFunc );
+    Llb_MgrForEachPart( p, pPart, i )
+    {
         bFunc = Cudd_bddAnd( p->dd, bTemp = bFunc, pPart->bFunc );
         if ( bFunc == NULL )
         {
@@ -924,16 +1045,43 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo
         Cudd_RecursiveDeref( p->dd, bTemp );
     }
     nSuppMax = p->nSuppMax;
-    Llb_NonlinFree( p );
     // reorder variables
-    if ( fReorder )
-        Llb_NonlinReorder( dd, fVerbose );
+//    if ( fReorder )
+//        Llb_NonlinReorder( p->dd, 0, fVerbose );
+    // save permutation
+//    memcpy( pOrder, p->dd->invperm, sizeof(int) * Cudd_ReadSize(p->dd) );
+
     timeOther += clock() - clk - timeInside;
     // return
     Cudd_Deref( bFunc );
     return bFunc;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Quits image computation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_NonlinImageQuit()
+{
+    DdManager * dd;
+    if ( p == NULL )
+        return;
+    dd = p->dd;
+    Llb_NonlinFree( p );
+    if ( dd->bFunc )
+        Cudd_RecursiveDeref( dd, dd->bFunc );
+    Extra_StopManager( dd );
+//    Cudd_Quit ( dd );
+    p = NULL;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/llb/llb3Nonlin.c b/src/aig/llb/llb3Nonlin.c
index c10db9e3..1cdd2c96 100644
--- a/src/aig/llb/llb3Nonlin.c
+++ b/src/aig/llb/llb3Nonlin.c
@@ -42,13 +42,18 @@ struct Llb_Mnn_t_
     Vec_Ptr_t *     vLeaves;        
     Vec_Ptr_t *     vRoots;
     int *           pVars2Q;
-    int *           pOrder;
+    int *           pOrderL;
+    int *           pOrderL2;
+    int *           pOrderG;
 
     Vec_Int_t *     vCs2Glo;        // cur state variables into global variables
     Vec_Int_t *     vNs2Glo;        // next state variables into global variables
     Vec_Int_t *     vGlo2Cs;        // global variables into cur state variables
     Vec_Int_t *     vGlo2Ns;        // global variables into next state variables
 
+    int             ddLocReos;
+    int             ddLocGrbs;
+
     int             timeImage;
     int             timeTran1;
     int             timeTran2;
@@ -297,7 +302,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, ABC_INFINITY ); // consumed reference
+            p->pPars->fReorder, p->pPars->fVeryVerbose, NULL, ABC_INFINITY, ABC_INFINITY ); // consumed reference
         assert( bImage != NULL );
         Cudd_Ref( bImage );
 //Extra_bddPrintSupport( p->dd, bImage );  printf( "\n" );
@@ -393,10 +398,37 @@ int Llb_NonlinReoHook( DdManager * dd, char * Type, void * Method )
   SeeAlso     []
 
 ***********************************************************************/
+int Llb_NonlinCompPerms( DdManager * dd, int * pVar2Lev )
+{
+    DdSubtable * pSubt;
+    int i, Sum = 0, Entry;
+    for ( i = 0; i < dd->size; i++ )
+    {
+        pSubt = &(dd->subtables[dd->perm[i]]);
+        if ( pSubt->keys == pSubt->dead + 1 )
+            continue;
+        Entry = ABC_MAX(dd->perm[i], pVar2Lev[i]) - ABC_MIN(dd->perm[i], pVar2Lev[i]);
+        Sum += Entry;
+//printf( "%d-%d(%d) ", dd->perm[i], pV2L[i], Entry );
+    }
+    return Sum;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Perform reachability with hints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Llb_NonlinReachability( Llb_Mnn_t * p )
 { 
-    DdNode * bCurrent, * bNext, * bTemp;
-    int iVar, nIters, nBddSize0, nBddSize, Limit = p->pPars->nBddMax;
+    DdNode * bTemp, * bNext;
+    int nIters, nBddSize0, nBddSize, NumCmp, Limit = p->pPars->nBddMax;
     int clk2, clk3, clk = clock();
     assert( Aig_ManRegNum(p->pAig) > 0 );
 
@@ -425,7 +457,9 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
     }
     Cudd_Ref( p->ddR->bFunc );
     // compute the starting set of states
-    bCurrent       = Llb_NonlinComputeInitState( p->pAig, p->dd );   Cudd_Ref( bCurrent );
+    Cudd_Quit( p->dd );
+    p->dd = Llb_NonlinImageStart( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->pOrderL, 1 );
+    p->dd->bFunc   = Llb_NonlinComputeInitState( p->pAig, p->dd );   Cudd_Ref( p->dd->bFunc );   // current
     p->ddG->bFunc  = Llb_NonlinComputeInitState( p->pAig, p->ddG );  Cudd_Ref( p->ddG->bFunc );  // reached
     p->ddG->bFunc2 = Llb_NonlinComputeInitState( p->pAig, p->ddG );  Cudd_Ref( p->ddG->bFunc2 ); // frontier 
     for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ )
@@ -437,18 +471,18 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
             if ( !p->pPars->fSilent )
                 printf( "Reached timeout (%d seconds) during image computation.\n",  p->pPars->TimeLimit );
             p->pPars->iFrame = nIters - 1;
-            Cudd_RecursiveDeref( p->dd,  bCurrent );  bCurrent = NULL;
+            Llb_NonlinImageQuit();
             return -1;
         }
 
         // save the onion ring
-        bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, Vec_IntArray(p->vCs2Glo) );
+        bTemp = Extra_TransferPermute( p->dd, p->ddR, p->dd->bFunc, Vec_IntArray(p->vCs2Glo) );
         if ( bTemp == NULL )
         {
             if ( !p->pPars->fSilent )
                 printf( "Reached timeout (%d seconds) during ring transfer.\n",  p->pPars->TimeLimit );
             p->pPars->iFrame = nIters - 1;
-            Cudd_RecursiveDeref( p->dd,  bCurrent );  bCurrent = NULL;
+            Llb_NonlinImageQuit();
             return -1;
         }
         Cudd_Ref( bTemp );
@@ -460,7 +494,6 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
             assert( p->pInit->pSeqModel == NULL );
             if ( !p->pPars->fBackward )
                 p->pInit->pSeqModel = Llb_NonlinDeriveCex( p ); 
-            Cudd_RecursiveDeref( p->dd,  bCurrent );  bCurrent = NULL;
             if ( !p->pPars->fSilent )
             {
                 if ( !p->pPars->fBackward )
@@ -469,85 +502,32 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
                     printf( "Output ??? was asserted in frame %d (counter-example is not produced).  ", nIters );
                 Abc_PrintTime( 1, "Time", clock() - clk );
             }
+            Llb_NonlinImageQuit();
             return 0;
         }
 
-        // check the size
-        if ( Cudd_DagSize(bCurrent) > p->pPars->nBddMax )
-        {
-            DdNode * bVar, * bVarG;
-
-            // find the best variable
-            iVar     = Llb_NonlinFindBestVar( p->dd, bCurrent, p->pAig );
-
-            // get cofactor in the working manager
-            bVar     = Cudd_bddIthVar( p->dd, Aig_ObjId(Saig_ManLo(p->pAig,iVar)) );
-            bCurrent = Cudd_bddAnd( p->dd, bTemp = bCurrent, Cudd_Not(bVar) );                  Cudd_Ref( bCurrent );
-            Cudd_RecursiveDeref( p->dd, bTemp );            
- 
-            // get cofactor in the global manager
-            bVarG    = Cudd_bddIthVar(p->ddG, iVar);
-            p->ddG->bFunc2 = Cudd_bddAnd( p->ddG, bTemp = p->ddG->bFunc2, Cudd_Not(bVarG) );    Cudd_Ref( p->ddG->bFunc2 );
-            Cudd_RecursiveDeref( p->ddG, bTemp );            
-        }
-
         // compute the next states
         clk3 = clock();
-        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->TimeTarget );
-//        Abc_PrintTime( 1, "Image time", clock() - clk3 );
+        nBddSize0 = Cudd_DagSize( p->dd->bFunc );
+        bNext = Llb_NonlinImageCompute( p->dd->bFunc, p->pPars->fReorder, 0, 1, p->pOrderL ); // consumes ref   
+//        bNext = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bCurrent, 
+//            p->pPars->fReorder, p->pPars->fVeryVerbose, NULL, ABC_INFINITY, p->pPars->TimeTarget );
         if ( 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;
-            Cudd_RecursiveDeref( p->dd,  bCurrent );  bCurrent = NULL;
+            Llb_NonlinImageQuit();
             return -1;
         }
-        if ( bNext == NULL )  // Llb_NonlimImage() consumes reference of bCurrent!!!
-        {
-            DdNode * bVar, * bVarG;
-//          if ( !p->pPars->fSilent )
-//              printf( "Reached timeout during image computation (%d seconds).\n",  p->pPars->TimeLimit );
-//          p->pPars->iFrame = nIters - 1;
-//          return -1;
-
-            printf( "Should never happen!\n" );
- 
-            // get the frontier in the working manager
-            bCurrent = Extra_TransferPermute( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs) );   Cudd_Ref( bCurrent );
-
-            // find the best variable
-            iVar     = Llb_NonlinFindBestVar( p->dd, bCurrent, p->pAig );
-
-            // get cofactor in the working manager
-            bVar     = Cudd_bddIthVar( p->dd, Aig_ObjId(Saig_ManLo(p->pAig,iVar)) );
-            bCurrent = Cudd_bddAnd( p->dd, bTemp = bCurrent, Cudd_Not(bVar) );                  Cudd_Ref( bCurrent );
-            Cudd_RecursiveDeref( p->dd, bTemp );            
-
-            // get cofactor in the global manager
-            bVarG    = Cudd_bddIthVar(p->dd, iVar);
-            p->ddG->bFunc2 = Cudd_bddAnd( p->ddG, bTemp = p->ddG->bFunc2, Cudd_Not(bVarG) );    Cudd_Ref( p->ddG->bFunc2 );
-            Cudd_RecursiveDeref( p->ddG, bTemp );            
-
-//            Cudd_ReduceHeap( p->dd, CUDD_REORDER_SIFT, 1 );
-            p->pPars->nBddMax = ABC_INFINITY;
-            nIters--;
-            continue;
-        }
-        else
-            p->pPars->nBddMax = Limit;
-
         Cudd_Ref( bNext );
         nBddSize = Cudd_DagSize( bNext );
         p->timeImage += clock() - clk3;
 
+
         // transfer to the state manager
         clk3 = clock();
         Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 );
-//        p->ddG->bFunc2 = Extra_TransferPermuteTime( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo), p->pPars->TimeTarget );    
         p->ddG->bFunc2 = Extra_TransferPermute( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo) );    
         if ( p->ddG->bFunc2 == NULL )
         {
@@ -555,12 +535,24 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
                 printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n",  p->pPars->TimeLimit );
             p->pPars->iFrame = nIters - 1;
             Cudd_RecursiveDeref( p->dd,  bNext );  
+            Llb_NonlinImageQuit();
             return -1;
         }
         Cudd_Ref( p->ddG->bFunc2 );
         Cudd_RecursiveDeref( p->dd, bNext );
         p->timeTran1 += clock() - clk3;
 
+        // save permutation
+        NumCmp = Llb_NonlinCompPerms( p->dd, p->pOrderL2 );
+        // save order before image computation
+        memcpy( p->pOrderL2, p->dd->perm, sizeof(int) * p->dd->size );
+        // update the image computation manager
+        p->timeReo   += Cudd_ReadReorderingTime(p->dd);
+        p->ddLocReos += Cudd_ReadReorderings(p->dd);
+        p->ddLocGrbs += Cudd_ReadGarbageCollections(p->dd);
+        Llb_NonlinImageQuit();
+        p->dd = Llb_NonlinImageStart( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->pOrderL, 0 );
+
         // derive new states
         clk3 = clock();
         p->ddG->bFunc2 = Cudd_bddAnd( p->ddG, bTemp = p->ddG->bFunc2, Cudd_Not(p->ddG->bFunc) );     
@@ -570,6 +562,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
                 printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n",  p->pPars->TimeLimit );
             p->pPars->iFrame = nIters - 1;
             Cudd_RecursiveDeref( p->ddG, bTemp );  
+            Llb_NonlinImageQuit();
             return -1;
         }
         Cudd_Ref( p->ddG->bFunc2 );
@@ -584,6 +577,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
                 printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n",  p->pPars->TimeLimit );
             p->pPars->iFrame = nIters - 1;
             Cudd_RecursiveDeref( p->ddG, bTemp );  
+            Llb_NonlinImageQuit();
             return -1;
         }
         Cudd_Ref( p->ddG->bFunc );
@@ -593,20 +587,20 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
         // reset permutation
 //        RetValue = Cudd_CheckZeroRef( dd );
 //        assert( RetValue == 0 );
-//        Cudd_ShuffleHeap( dd, pOrder );
+//        Cudd_ShuffleHeap( dd, pOrderG );
 
         // move new states to the working manager
         clk3 = clock();
-//        bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs), p->pPars->TimeTarget ); 
-        bCurrent = Extra_TransferPermute( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs) ); 
-        if ( bCurrent == NULL )
+        p->dd->bFunc = Extra_TransferPermute( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs) ); 
+        if ( p->dd->bFunc == NULL )
         {
             if ( !p->pPars->fSilent )
                 printf( "Reached timeout (%d seconds) during image computation in transfer 2.\n",  p->pPars->TimeLimit );
             p->pPars->iFrame = nIters - 1;
+            Llb_NonlinImageQuit();
             return -1;
         }
-        Cudd_Ref( bCurrent );
+        Cudd_Ref( p->dd->bFunc );
         p->timeTran2 += clock() - clk3;
 
         // report the results
@@ -615,11 +609,14 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
             printf( "I =%3d : ",   nIters );
             printf( "Fr =%7d ",    nBddSize0 );
             printf( "Im =%7d  ",   nBddSize );
-            printf( "(%4d %4d)  ", Cudd_ReadReorderings(p->dd),  Cudd_ReadGarbageCollections(p->dd) );
+            printf( "(%4d %4d)  ", p->ddLocReos, p->ddLocGrbs );
             printf( "Rea =%6d  ",  Cudd_DagSize(p->ddG->bFunc) );
             printf( "(%4d %4d)  ", Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) );
             printf( "S =%4d ",     nSuppMax );
+            printf( "cL =%5d ",    NumCmp );
+            printf( "cG =%5d ",    Llb_NonlinCompPerms( p->ddG, p->pOrderG ) );
             Abc_PrintTime( 1, "T", clock() - clk2 );
+            memcpy( p->pOrderG, p->ddG->perm, sizeof(int) * p->ddG->size );
         }
 /*
         if ( pPars->fVerbose )
@@ -630,18 +627,16 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
             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;
-            Cudd_RecursiveDeref( p->dd,  bCurrent );       bCurrent = NULL;
+            Llb_NonlinImageQuit();
             return -1;
         }
-//        Llb_NonlinReorder( p->ddG, 1 );
-//        Llb_NonlinFindBestVar( p->ddG, bReached, NULL );
     }
+    Llb_NonlinImageQuit();
     
     // report the stats
     if ( p->pPars->fVerbose )
@@ -704,10 +699,14 @@ Llb_Mnn_t * Llb_MnnStart( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t *  p
     Saig_ManForEachLi( pAig, pObj, i )
         Vec_PtrPush( p->vRoots, pObj );
     // variables to quantify
-    p->pOrder  = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
+    p->pOrderL = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
+    p->pOrderL2= ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
+    p->pOrderG = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
     p->pVars2Q = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
     Aig_ManForEachPi( pAig, pObj, i )
         p->pVars2Q[Aig_ObjId(pObj)] = 1;
+    for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
+        p->pOrderL[i] = p->pOrderL2[i] = p->pOrderG[i] = i;
     Llb_NonlinPrepareVarMap( p ); 
     return p;
 }
@@ -730,7 +729,6 @@ void Llb_MnnStop( Llb_Mnn_t * p )
     if ( p->pPars->fVerbose ) 
     {
         p->timeOther = p->timeTotal - p->timeImage - p->timeTran1 - p->timeTran2 - p->timeGloba;
-        p->timeReo   = Cudd_ReadReorderingTime(p->dd);
         p->timeReoG  = Cudd_ReadReorderingTime(p->ddG);
         ABC_PRTP( "Image    ", p->timeImage, p->timeTotal );
         ABC_PRTP( "  build  ",    timeBuild, p->timeTotal );
@@ -744,7 +742,6 @@ 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 )
@@ -755,7 +752,7 @@ void Llb_MnnStop( Llb_Mnn_t * p )
     if ( p->ddG->bFunc2 )
         Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 );
 //    printf( "manager1\n" );
-    Extra_StopManager( p->dd );
+//    Extra_StopManager( p->dd );
 //    printf( "manager2\n" );
     Extra_StopManager( p->ddG );
 //    printf( "manager3\n" );
@@ -767,7 +764,9 @@ void Llb_MnnStop( Llb_Mnn_t * p )
     Vec_PtrFree( p->vLeaves );
     Vec_PtrFree( p->vRoots );
     ABC_FREE( p->pVars2Q );
-    ABC_FREE( p->pOrder );
+    ABC_FREE( p->pOrderL );
+    ABC_FREE( p->pOrderL2 );
+    ABC_FREE( p->pOrderG );
     ABC_FREE( p );
 }
 
diff --git a/src/aig/llb/llbInt.h b/src/aig/llb/llbInt.h
index 6bca2adb..dd938436 100644
--- a/src/aig/llb/llbInt.h
+++ b/src/aig/llb/llbInt.h
@@ -172,9 +172,15 @@ extern DdNode *        Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMan
                            Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQuant1, Vec_Int_t * vDriRefs, 
                            int TimeTarget, int fBackward, int fReorder, int fVerbose );
 
+extern DdManager *     Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst );
+extern DdNode *        Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int fVerbose, int * pOrder );
+extern void            Llb_NonlinImageQuit();
+
 /*=== 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, int TimeTarget );
+/*=== llb3Nonlin.c ======================================================*/
+extern DdNode *        Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd );
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 9890dbcf..c055c3ad 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27937,7 +27937,7 @@ usage:
     Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax );
     Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit );
     Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
-    Abc_Print( -2, "\t-r     : enable dynamic BDD variable reordering [default = %s]\n", pPars->fReorder? "yes": "no" );  
+    Abc_Print( -2, "\t-r     : enable additional BDD var reordering before image [default = %s]\n", pPars->fReorder? "yes": "no" );  
     Abc_Print( -2, "\t-b     : perform backward reachability analysis [default = %s]\n", pPars->fBackward? "yes": "no" );  
     Abc_Print( -2, "\t-y     : skip checking property outputs [default = %s]\n", pPars->fSkipOutCheck? "yes": "no" );  
     Abc_Print( -2, "\t-z     : skip reachability (run preparation phase only) [default = %s]\n", pPars->fSkipReach? "yes": "no" );  
@@ -28069,7 +28069,7 @@ usage:
     Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax );
     Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit );
     Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
-    Abc_Print( -2, "\t-r     : enable dynamic BDD variable reordering [default = %s]\n", pPars->fReorder? "yes": "no" );  
+    Abc_Print( -2, "\t-r     : enable additional BDD var reordering before image [default = %s]\n", pPars->fReorder? "yes": "no" );  
     Abc_Print( -2, "\t-y     : skip checking property outputs [default = %s]\n", pPars->fSkipOutCheck? "yes": "no" );  
     Abc_Print( -2, "\t-z     : skip reachability (run preparation phase only) [default = %s]\n", pPars->fSkipReach? "yes": "no" );  
     Abc_Print( -2, "\t-v     : prints verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );