Dumping BDD variable order after 'clp'.

6 files changed, 27 insertions, 10 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 312354da..c36bde70 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -600,7 +600,7 @@ extern ABC_DLL int                Abc_NtkCheckUniqueCiNames( Abc_Ntk_t * pNtk );
 extern ABC_DLL int                Abc_NtkCheckUniqueCoNames( Abc_Ntk_t * pNtk );
 extern ABC_DLL int                Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk );
 /*=== abcCollapse.c ==========================================================*/
-extern ABC_DLL Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fVerbose );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fDumpOrder, int fVerbose );
 extern ABC_DLL Abc_Ntk_t *        Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fCnfShared, int fVerbose );
 extern ABC_DLL Gia_Man_t *        Abc_NtkClpGia( Abc_Ntk_t * pNtk );
 /*=== abcCut.c ==========================================================*/
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b7f0517e..411f66ed 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3355,6 +3355,7 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fDualRail;
     int fReorder;
     int fReverse;
+    int fDumpOrder;
     int c;
     char * pLogFileName = NULL;
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -3364,9 +3365,10 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
     fReorder = 1;
     fReverse = 0;
     fDualRail = 0;
+    fDumpOrder = 0;
     fBddSizeMax = ABC_INFINITY;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "BLrodvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "BLrodxvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -3399,6 +3401,9 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             fDualRail ^= 1;
             break;
+        case 'x':
+            fDumpOrder ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -3423,11 +3428,11 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // get the new network
     if ( Abc_NtkIsStrash(pNtk) )
-        pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fReverse, fVerbose );
+        pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fReverse, fDumpOrder, fVerbose );
     else
     {
         pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 );
-        pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fReverse, fVerbose );
+        pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fReverse, fDumpOrder, fVerbose );
         Abc_NtkDelete( pNtk );
     }
     if ( pNtkRes == NULL )
@@ -3450,13 +3455,14 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: collapse [-B <num>] [-L file] [-rodvh]\n" );
+    Abc_Print( -2, "usage: collapse [-B <num>] [-L file] [-rodxvh]\n" );
     Abc_Print( -2, "\t          collapses the network by constructing global BDDs\n" );
     Abc_Print( -2, "\t-B <num>: limit on live BDD nodes during collapsing [default = %d]\n", fBddSizeMax );
     Abc_Print( -2, "\t-L file : the log file name [default = %s]\n",  pLogFileName ? pLogFileName : "no logging" );
     Abc_Print( -2, "\t-r      : toggles dynamic variable reordering [default = %s]\n", fReorder? "yes": "no" );
     Abc_Print( -2, "\t-o      : toggles reverse variable ordering [default = %s]\n", fReverse? "yes": "no" );
     Abc_Print( -2, "\t-d      : toggles dual-rail collapsing mode [default = %s]\n", fDualRail? "yes": "no" );
+    Abc_Print( -2, "\t-x      : toggles dumping file \"order.txt\" with variable order [default = %s]\n", fDumpOrder? "yes": "no" );
     Abc_Print( -2, "\t-v      : print verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h      : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index ca54d542..136712cb 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -195,7 +195,16 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk, int fReverse )
     Extra_ProgressBarStop( pProgress );
     return pNtkNew;
 }
-Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fVerbose )
+void Abc_NtkDumpVariableOrder( Abc_Ntk_t * pNtk )
+{
+    DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk );
+    FILE * pFile = fopen( "order.txt", "wb" ); int i;
+    for ( i = 0; i < dd->size; i++ )
+        fprintf( pFile, "%d ", dd->invperm[i] );
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+}
+Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fDumpOrder, int fVerbose )
 {
     Abc_Ntk_t * pNtkNew;
     abctime clk = Abc_Clock();
@@ -210,6 +219,8 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
         printf( "Shared BDD size = %6d nodes.  ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
         ABC_PRT( "BDD construction time", Abc_Clock() - clk );
     }
+    if ( fDumpOrder ) 
+        Abc_NtkDumpVariableOrder( pNtk );
 
     // create the new network
     pNtkNew = Abc_NtkFromGlobalBdds( pNtk, fReverse );
@@ -236,7 +247,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
 
 #else
 
-Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fVerbose )
+Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fDumpOrder, int fVerbose )
 {
     return NULL;
 }
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 5dc125d0..3f268ea2 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -601,7 +601,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
             printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit );
             fflush( stdout );
         }
-        pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0, 0 );
+        pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0, 0, 0 );
         if ( pNtk )   
         {
             Abc_NtkDelete( pNtkTemp );
diff --git a/src/base/abci/abcLutmin.c b/src/base/abci/abcLutmin.c
index 2ac44060..be01beb6 100644
--- a/src/base/abci/abcLutmin.c
+++ b/src/base/abci/abcLutmin.c
@@ -739,7 +739,7 @@ Abc_Ntk_t * Abc_NtkLutmin( Abc_Ntk_t * pNtkInit, int nLutSize, int fVerbose )
     else
         pNtkNew = Abc_NtkStrash( pNtkInit, 0, 1, 0 );
     // collapse the network 
-    pNtkNew = Abc_NtkCollapse( pTemp = pNtkNew, 10000, 0, 1, 0, 0 );
+    pNtkNew = Abc_NtkCollapse( pTemp = pNtkNew, 10000, 0, 1, 0, 0, 0 );
     Abc_NtkDelete( pTemp );
     if ( pNtkNew == NULL )
         return NULL;
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index 03722926..b14c0827 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -201,7 +201,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
             fflush( stdout );
         }
         clk = Abc_Clock();
-        pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0, 0 );
+        pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0, 0, 0 );
         if ( pNtk )   
         {
             Abc_NtkDelete( pNtkTemp );