Improvements to BDD reachability.

src/aig/llb/llb4Image.c

@@ -847,7 +847,7 @@ Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vV
 //Extra_bddPrintSupport( p->dd, pPart->bFunc ); printf( "\n" );
     }
     Llb_Nonlin4Free( p );
-Abc_PrintTime( 1, "Reparametrization time", clock() - clk );
+//Abc_PrintTime( 1, "Reparametrization time", clock() - clk );
     return vGroups;
 }
 

src/aig/llb/llb4Nonlin.c

@@ -675,6 +675,10 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
             p->bBad = Llb_Nonlin4ComputeInitState( p->dd, p->pAig, p->vOrder, p->pPars->fBackward );  Cudd_Ref( p->bBad );
         }
         // create init state
+        if ( p->pPars->fCluster )
+            p->bCurrent = p->dd->bFunc, p->dd->bFunc = NULL; 
+        else
+        {
             p->bCurrent = Llb_Nonlin4ComputeBad( p->dd, p->pAig, p->vOrder );          
             if ( p->bCurrent == NULL )
             {
@@ -684,6 +688,7 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
                 return -1;
             }
             Cudd_Ref( p->bCurrent );
+        }
         // remap into the next states
         p->bCurrent = Cudd_bddVarMap( p->dd, bAux = p->bCurrent );
         if ( p->bCurrent == NULL )
@@ -702,6 +707,10 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
         // create bad state in the ring manager
         if ( !p->pPars->fSkipOutCheck )
         {
+            if ( p->pPars->fCluster )
+                p->bBad = p->dd->bFunc, p->dd->bFunc = NULL; 
+            else
+            {
                 p->bBad = Llb_Nonlin4ComputeBad( p->dd, p->pAig, p->vOrder );          
                 if ( p->bBad == NULL )
                 {
@@ -712,6 +721,9 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
                 }
                 Cudd_Ref( p->bBad );
             }
+        }
+        else if ( p->dd->bFunc )
+            Cudd_RecursiveDeref( p->dd, p->dd->bFunc ), p->dd->bFunc = NULL;
         // compute the starting set of states
         p->bCurrent = Llb_Nonlin4ComputeInitState( p->dd, p->pAig, p->vOrder, p->pPars->fBackward );  Cudd_Ref( p->bCurrent );
     }
@@ -925,8 +937,9 @@ Llb_Mnx_t * Llb_MnxStart( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
 
     if ( pPars->fCluster )
     {
-        Llb_Nonlin4Cluster( p->pAig, &p->dd, &p->vOrder, &p->vRoots, pPars->nBddMax, pPars->fVerbose );
-        Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
+//        Llb_Nonlin4Cluster( p->pAig, &p->dd, &p->vOrder, &p->vRoots, pPars->nBddMax, pPars->fVerbose );
+//        Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
+        Llb4_Nonlin4Sweep( p->pAig, pPars->nBddMax, pPars->nClusterMax, &p->dd, &p->vOrder, &p->vRoots, pPars->fVerbose );
     }
     else
     {

src/aig/llb/llbInt.h

@@ -188,7 +188,7 @@ extern DdNode *        Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager *
 /*=== llb4Cex.c =======================================================*/
 extern Abc_Cex_t *     Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int fVerbose );
 /*=== llb4Cluster.c =======================================================*/
-extern void            Llb_Nonlin4Cluster( Aig_Man_t * pAig, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int nBddMax, int fVerbose );
+//extern void            Llb_Nonlin4Cluster( Aig_Man_t * pAig, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int nBddMax, int fVerbose );
 /*=== llb4Image.c =======================================================*/
 extern DdNode *        Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q );
 extern Vec_Ptr_t *     Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vVars2Q, int nSizeMax );
@@ -196,6 +196,8 @@ extern Vec_Ptr_t *     Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec
 //extern Vec_Int_t *     Llb_AigMap( Aig_Man_t * pAig, int nLutSize, int nLutMin );
 /*=== llb4Nonlin.c ======================================================*/
 extern int             Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars );
+/*=== llb4Sweep.c ======================================================*/
+extern void            Llb4_Nonlin4Sweep( Aig_Man_t * pAig, int nSweepMax, int nClusterMax, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int fVerbose );
  
 
 ABC_NAMESPACE_HEADER_END

src/aig/llb/module.make

@@ -18,6 +18,6 @@ SRC +=    src/aig/llb/llb.c \
     src/aig/llb/llb3Image.c \
     src/aig/llb/llb3Nonlin.c \
     src/aig/llb/llb4Cex.c \
-    src/aig/llb/llb4Cluster.c \
     src/aig/llb/llb4Image.c \
-    src/aig/llb/llb4Nonlin.c
+    src/aig/llb/llb4Nonlin.c \
+    src/aig/llb/llb4Sweep.c