Mffc-based structural decomposition of the network and bug fixes in reordering package.

abclib.dsp

@@ -307,6 +307,10 @@ SOURCE=.\src\base\abci\abcMerge.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abci\abcMffc.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abci\abcMini.c
 # End Source File
 # Begin Source File
@@ -3563,6 +3567,10 @@ SOURCE=.\src\aig\int\int.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\int\intCheck.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\int\intContain.c
 # End Source File
 # Begin Source File

src/base/abci/abcCascade.c

@@ -126,9 +126,9 @@ DdNode * Abc_NtkBddToAdd( DdManager * dd, DdNode * bFunc, int nOuts )
     stmm_table * tTable;
     stmm_generator * gen;
     tTable = stmm_init_table( st_ptrcmp, st_ptrhash );
-    aFunc = Abc_NtkBddToAdd_rec( dd, Cudd_Regular(bFunc), nOuts, tTable, Cudd_IsComplement(bFunc) );  Cudd_Ref(aFunc);
+    aFunc = Abc_NtkBddToAdd_rec( dd, Cudd_Regular(bFunc), nOuts, tTable, Cudd_IsComplement(bFunc) );  
     stmm_foreach_item( tTable, gen, (char **)&bTemp, (char **)&aTemp )
-        Cudd_RecursiveDeref( dd, aFunc );
+        Cudd_RecursiveDeref( dd, aTemp );
     stmm_free_table( tTable );
     Cudd_Deref( aFunc );
     return aFunc;
@@ -189,10 +189,12 @@ void Abc_NtkBddDecTry( reo_man * pReo, DdManager * dd, DdNode ** pFuncs, int nOu
 //Abc_NodeShowBddOne( dd, aFunc );
     // perform reordering for BDD width
     aFuncNew = Extra_Reorder( pReo, dd, aFunc, NULL );                  Cudd_Ref( aFuncNew );
+printf( "Before = %d.  After = %d.\n", Cudd_DagSize(aFunc), Cudd_DagSize(aFuncNew) );
+//Abc_NodeShowBddOne( dd, aFuncNew );
     Cudd_RecursiveDeref( dd, aFuncNew );
     Cudd_RecursiveDeref( dd, aFunc );
     // print the result
-    reoProfileWidthPrint( pReo );
+//    reoProfileWidthPrint( pReo );
 }
 
 /**Function*************************************************************
@@ -268,6 +270,8 @@ void Abc_NtkBddDec( Abc_Ntk_t * pNtk, int fVerbose )
 
     pReo = Extra_ReorderInit( Abc_NtkCiNum(pNtk), 1000 );
     Extra_ReorderSetMinimizationType( pReo, REO_MINIMIZE_WIDTH );
+//    Extra_ReorderSetVerification( pReo, 1 );
+    Extra_ReorderSetVerbosity( pReo, 1 );
 
     Abc_NtkBddDecInt( pReo, dd, pFuncs, Abc_NtkCoNum(pNtk) );
     Extra_ReorderQuit( pReo );

src/bdd/reo/reoCore.c

@@ -122,7 +122,7 @@ void reoReorderArray( reo_man * p, DdManager * dd, DdNode * Funcs[], DdNode * Fu
 
     if ( p->fVerbose )
     {
-        printf( "INITIAL: " );
+        printf( "INITIAL:\n" );
         if ( p->fMinWidth )
             reoProfileWidthPrint(p);
         else if ( p->fMinApl )
@@ -141,7 +141,7 @@ void reoReorderArray( reo_man * p, DdManager * dd, DdNode * Funcs[], DdNode * Fu
         // print statistics after each iteration
         if ( p->fVerbose )
         {
-            printf( "ITER #%d: ", i+1 );
+            printf( "ITER #%d:\n", i+1 );
             if ( p->fMinWidth )
                 reoProfileWidthPrint(p);
             else if ( p->fMinApl )

src/bdd/reo/reoProfile.c

@@ -200,7 +200,7 @@ void reoProfileWidthStart( reo_man * p )
             p->pPlanes[v].statsWidth = p->pPlanes[v-1].statsWidth + pWidthStart[v] - pWidthStop[v];
         p->pPlanes[v].statsCost = p->pPlanes[v].statsWidth;
         p->nWidthCur += p->pPlanes[v].statsWidth;
-//        printf( "Level %2d: Width = %5d. Correct = %d.\n", v, Temp, p->pPlanes[v].statsWidth );
+        printf( "Level %2d: Width = %5d.\n", v, p->pPlanes[v].statsWidth );
     }
     p->nWidthBeg = p->nWidthCur;
     ABC_FREE( pWidthStart );
@@ -328,7 +328,7 @@ void reoProfileWidthPrint( reo_man * p )
     TotalWidth = 0;
     for ( i = 0; i <= p->nSupp; i++ )
     {
-//        printf( "Level = %2d. Width = %3d.\n", i, p->pProfile[i] );
+        printf( "Level = %2d. Width = %3d.\n", i, p->pPlanes[i].statsWidth );
         if ( WidthMax < p->pPlanes[i].statsWidth )
              WidthMax = p->pPlanes[i].statsWidth;
         TotalWidth += p->pPlanes[i].statsWidth;

src/bdd/reo/reoUnits.c

@@ -97,7 +97,8 @@ void reoUnitsRecycleUnitList( reo_man * p, reo_plane * pPlane )
         pTail = pUnit;
     pTail->Next = p->pUnitFreeList;
     p->pUnitFreeList    = pPlane->pHead;
-    memset( pPlane, 0, sizeof(reo_plane) );
+//    memset( pPlane, 0, sizeof(reo_plane) );
+    pPlane->pHead = NULL;
 }
 
 /**Function*************************************************************