Improvements to BDD reachability.

5 files changed, 38 insertions, 23 deletions

diff --git a/src/aig/llb/llb1Cluster.c b/src/aig/llb/llb1Cluster.c
index 8a41fe58..758994b5 100644
--- a/src/aig/llb/llb1Cluster.c
+++ b/src/aig/llb/llb1Cluster.c
@@ -11,7 +11,7 @@
   Author      [Alan Mishchenko]
   
   Affiliation [UC Berkeley]
-
+ 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
   Revision    [$Id: llb1Cluster.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
diff --git a/src/aig/llb/llb4Image.c b/src/aig/llb/llb4Image.c
index acc34b22..031c8830 100644
--- a/src/aig/llb/llb4Image.c
+++ b/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;
 }
 
diff --git a/src/aig/llb/llb4Nonlin.c b/src/aig/llb/llb4Nonlin.c
index 5659f25a..b153c8af 100644
--- a/src/aig/llb/llb4Nonlin.c
+++ b/src/aig/llb/llb4Nonlin.c
@@ -675,15 +675,20 @@ 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
-        p->bCurrent = Llb_Nonlin4ComputeBad( p->dd, p->pAig, p->vOrder );          
-        if ( p->bCurrent == NULL )
+        if ( p->pPars->fCluster )
+            p->bCurrent = p->dd->bFunc, p->dd->bFunc = NULL; 
+        else
         {
-            if ( !p->pPars->fSilent )
-                printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
-            p->pPars->iFrame = -1;
-            return -1;
+            p->bCurrent = Llb_Nonlin4ComputeBad( p->dd, p->pAig, p->vOrder );          
+            if ( p->bCurrent == NULL )
+            {
+                if ( !p->pPars->fSilent )
+                    printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
+                p->pPars->iFrame = -1;
+                return -1;
+            }
+            Cudd_Ref( p->bCurrent );
         }
-        Cudd_Ref( p->bCurrent );
         // remap into the next states
         p->bCurrent = Cudd_bddVarMap( p->dd, bAux = p->bCurrent );
         if ( p->bCurrent == NULL )
@@ -702,16 +707,23 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
         // create bad state in the ring manager
         if ( !p->pPars->fSkipOutCheck )
         {
-            p->bBad = Llb_Nonlin4ComputeBad( p->dd, p->pAig, p->vOrder );          
-            if ( p->bBad == NULL )
+            if ( p->pPars->fCluster )
+                p->bBad = p->dd->bFunc, p->dd->bFunc = NULL; 
+            else
             {
-                if ( !p->pPars->fSilent )
-                    printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
-                p->pPars->iFrame = -1;
-                return -1;
+                p->bBad = Llb_Nonlin4ComputeBad( p->dd, p->pAig, p->vOrder );          
+                if ( p->bBad == NULL )
+                {
+                    if ( !p->pPars->fSilent )
+                        printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
+                    p->pPars->iFrame = -1;
+                    return -1;
+                }
+                Cudd_Ref( p->bBad );
             }
-            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
     {
diff --git a/src/aig/llb/llbInt.h b/src/aig/llb/llbInt.h
index 23eb455e..ce62f79b 100644
--- a/src/aig/llb/llbInt.h
+++ b/src/aig/llb/llbInt.h
@@ -136,7 +136,7 @@ extern void            Llb_MtrVerifyMatrix( Llb_Mtr_t * p );
 extern Llb_Mtr_t *     Llb_MtrCreate( Llb_Man_t * p );
 extern void            Llb_MtrFree( Llb_Mtr_t * p );
 extern void            Llb_MtrPrint( Llb_Mtr_t * p, int fOrder );
-extern void            Llb_MtrPrintMatrixStats( Llb_Mtr_t * p );
+extern void            Llb_MtrPrintMatrixStats( Llb_Mtr_t * p ); 
 /*=== llbPart.c ======================================================*/
 extern Llb_Grp_t *     Llb_ManGroupAlloc( Llb_Man_t * pMan );
 extern void            Llb_ManGroupStop( Llb_Grp_t * p );
@@ -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,7 +196,9 @@ 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
 
diff --git a/src/aig/llb/module.make b/src/aig/llb/module.make
index 29b07700..1e8ea974 100644
--- a/src/aig/llb/module.make
+++ b/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