Version abc90528

committer: Baruch Sterin <baruchs@gmail.com>

7 files changed, 334 insertions, 21 deletions

diff --git a/src/base/abc/abcLib.c b/src/base/abc/abcLib.c
index 138dc9a1..4540462d 100644
--- a/src/base/abc/abcLib.c
+++ b/src/base/abc/abcLib.c
@@ -82,7 +82,7 @@ void Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave )
                 continue;
 //            pNtk->pManFunc = NULL;
             pNtk->pDesign = NULL;
-            if ( pNtk->pManFunc == pNtkSave->pManFunc )
+            if ( pNtkSave && pNtk->pManFunc == pNtkSave->pManFunc )
                 pNtk->pManFunc = NULL;
             Abc_NtkDelete( pNtk );
         }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 946b7210..660bf3e1 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -310,6 +310,7 @@ static int Abc_CommandAbc9Cec        ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandAbc9Force      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Embed      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9If         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Era        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Test       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandAbcTestNew     ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -629,6 +630,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "AIG",          "&force",        Abc_CommandAbc9Force,        0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&embed",        Abc_CommandAbc9Embed,        0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&if",           Abc_CommandAbc9If,           0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&era",          Abc_CommandAbc9Era,          0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&test",         Abc_CommandAbc9Test,         0 );
 
     Cmd_CommandAdd( pAbc, "Various",      "testnew",         Abc_CommandAbcTestNew,     0 );
@@ -18973,8 +18975,8 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else
     {
-//        extern void * Nal_ManRead( char * pFileName );
         pAbc->pAbc8Ntl = NULL;
+//        extern void * Nal_ManRead( char * pFileName );
 //        pAbc->pAbc8Ntl = Nal_ManRead( pFileName );
 //        Ioa_WriteBlif( pAbc->pAbc8Ntl, "test_boxes.blif" );
         if ( pAbc->pAbc8Ntl == NULL )
@@ -19104,7 +19106,7 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void * Ntl_ManInsertAig( void * p, Aig_Man_t * pAig );
     extern void * Ntl_ManDup( void * pOld );
     extern void Ntl_ManFree( void * p );
-    extern Aig_Man_t * Ntl_ManCollapseSeq( void * p, int nMinDomSize );
+    extern Aig_Man_t * Ntl_ManCollapseSeq( void * p, int nMinDomSize, int fVerbose );
 
     // set defaults
     fAig = 0;
@@ -19142,7 +19144,7 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
         if ( fCollapsed )
         {
             extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
-            pTemp = Ntl_ManCollapseSeq( pAbc->pAbc8Ntl, 0 );
+            pTemp = Ntl_ManCollapseSeq( pAbc->pAbc8Ntl, 0, 0 );
             if ( fBlif )
                 Saig_ManDumpBlif( pTemp, pFileName );
             else
@@ -19632,7 +19634,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( pAbc->pAbc8Lib == NULL )
     {
-        printf( "LUT library is not given. Using default LUT library.\n" );
+//        printf( "LUT library is not given. Using default LUT library.\n" );
         pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 );
     }
 
@@ -19774,7 +19776,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
     // enable truth table computation if choices are selected
     if ( (c = Aig_ManChoiceNum( pAbc->pAbc8Aig )) )
     {
-        printf( "Performing LUT mapping with %d choices.\n", c );
+//        printf( "Performing LUT mapping with %d choices.\n", c );
         pPars->fExpRed = 0;
     }
     // enable truth table computation if cut minimization is selected
@@ -20813,17 +20815,19 @@ int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nPartSize;
     int nConfLimit;
     int nLevelMax;
+    int fUseCSat;
     extern Aig_Man_t * Ntl_ManExtract( void * p );
-    extern void * Ntl_ManFraig( void * p, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose );
+    extern void * Ntl_ManFraig( void * p, int nPartSize, int nConfLimit, int nLevelMax, int fUseCSat, int fVerbose );
     extern void Ntl_ManFree( void * p );
 
     // set defaults
     nPartSize    = 0;
     nConfLimit   = 100;   
     nLevelMax    = 0;
+    fUseCSat     = 0;
     fVerbose     = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PCLvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PCLcvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -20860,6 +20864,9 @@ int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nLevelMax < 0 ) 
                 goto usage;
             break;
+        case 'c':
+            fUseCSat ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -20877,7 +20884,7 @@ int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the input file name
-    pNtlNew = Ntl_ManFraig( pAbc->pAbc8Ntl, nPartSize, nConfLimit, nLevelMax, fVerbose );
+    pNtlNew = Ntl_ManFraig( pAbc->pAbc8Ntl, nPartSize, nConfLimit, nLevelMax, fUseCSat, fVerbose );
     if ( pNtlNew == NULL )
     {
         printf( "Abc_CommandAbc8Fraig(): Tranformation of the AIG has failed.\n" );
@@ -20905,6 +20912,7 @@ usage:
     fprintf( stdout, "\t-P num : partition size (0 = partitioning is not used) [default = %d]\n", nPartSize );
     fprintf( stdout, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
     fprintf( stdout, "\t-L num : limit on node level to fraig (0 = fraig all nodes) [default = %d]\n", nLevelMax );
+//    fprintf( stdout, "\t-c     : toggle using new AIG package and SAT solver [default = %s]\n", fUseCSat? "yes": "no" );
     fprintf( stdout, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
     return 1;
@@ -21018,19 +21026,23 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     void * pNtlNew;
     int c;
+    int fScorrGia;
+    int fUseCSat;
     int nFramesP;
     int nConfMax;
     int fVerbose;
     extern Aig_Man_t * Ntl_ManExtract( void * p );
-    extern void * Ntl_ManLcorr( void * p, int nConfMax, int fVerbose );
+    extern void * Ntl_ManLcorr( void * p, int nConfMax, int fScorrGia, int fUseCSat, int fVerbose );
     extern int Ntl_ManIsComb( void * p );
 
     // set defaults
+    fScorrGia  = 0;
+    fUseCSat   = 0;
     nFramesP   = 0;
     nConfMax   = 10000;
     fVerbose   = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PCvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PCncvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -21056,6 +21068,12 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nConfMax < 0 ) 
                 goto usage;
             break;
+        case 'n':
+            fScorrGia ^= 1;
+            break;
+        case 'c':
+            fUseCSat ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -21079,7 +21097,7 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the input file name
-    pNtlNew = Ntl_ManLcorr( pAbc->pAbc8Ntl, nConfMax, fVerbose );
+    pNtlNew = Ntl_ManLcorr( pAbc->pAbc8Ntl, nConfMax, fScorrGia, fUseCSat, fVerbose );
     if ( pNtlNew == NULL )
     {
         printf( "Abc_CommandAbc8Lcorr(): Tranformation of the AIG has failed.\n" );
@@ -21102,10 +21120,12 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( stdout, "usage: *lcorr [-C num] [-vh]\n" );
+    fprintf( stdout, "usage: *lcorr [-C num] [-ncvh]\n" );
     fprintf( stdout, "\t         computes latch correspondence for the netlist\n" );
 //    fprintf( stdout, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
     fprintf( stdout, "\t-C num : max conflict number when proving latch equivalence [default = %d]\n", nConfMax );
+    fprintf( stdout, "\t-n     : toggle using new AIG package [default = %s]\n", fScorrGia? "yes": "no" );
+    fprintf( stdout, "\t-c     : toggle using new AIG package and SAT solver [default = %s]\n", fUseCSat? "yes": "no" );
     fprintf( stdout, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
     return 1;
@@ -21625,7 +21645,7 @@ int Abc_CommandAbc8Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
  
     // sweep the current design
     Counter = Ntl_ManSweep( pAbc->pAbc8Ntl, fVerbose );
-    if ( Counter == 0 )
+    if ( Counter == 0 && fVerbose )
         printf( "The netlist is unchanged by sweep.\n" );
 
     // if mapped, create new AIG and new mapped network
@@ -24508,6 +24528,7 @@ usage:
     fprintf( stdout, "\t-h     : print the command usage\n");
     return 1;
 }
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -24739,6 +24760,80 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Era( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pTemp = NULL;
+    int c, fVerbose = 0;
+    int fMiter = 0;
+    int nStatesMax = 1000000;
+    extern void Gia_ManCollectReachable( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbose );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Smvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-S\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nStatesMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nStatesMax < 0 ) 
+                goto usage;
+            break;
+        case 'm':
+            fMiter ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Era(): There is no AIG.\n" );
+        return 1;
+    } 
+    if ( Gia_ManPiNum(pAbc->pAig) > 12 )
+    {
+        printf( "Abc_CommandAbc9Era(): The number of PIs (%d) should be no more than 12.\n", Gia_ManPiNum(pAbc->pAig) );
+        return 1;
+    }
+    if ( Gia_ManRegNum(pAbc->pAig) == 0 )
+    {
+        printf( "Abc_CommandAbc9Era(): The network is combinational.\n" );
+        return 1;
+    }
+    Gia_ManCollectReachable( pAbc->pAig, nStatesMax, fMiter, fVerbose );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &era [-S num] [-mvh]\n" );
+    fprintf( stdout, "\t          explicit reachability analysis for small sequential AIGs\n" );
+    fprintf( stdout, "\t-S num  : the max number of states to traverse (num > 0) [default = %d]\n", nStatesMax );
+    fprintf( stdout, "\t-m      : stop when the miter output is 1 [default = %s]\n", fMiter? "yes": "no" );
+    fprintf( stdout, "\t-v      : print verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h      : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp = NULL;
diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c
index 5e9093e7..b77f9d77 100644
--- a/src/base/abci/abcXsim.c
+++ b/src/base/abci/abcXsim.c
@@ -20,6 +20,8 @@
 
 #include "abc.h"
 
+extern unsigned            Gia_ManRandom( int fReset );
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -50,13 +52,15 @@ static inline int  Abc_XsimAnd( int Value0, int Value1 )
 }
 static inline int  Abc_XsimRand2()   
 {
-    return (rand() & 1) ? XVS1 : XVS0;
+//    return (rand() & 1) ? XVS1 : XVS0;
+    return (Gia_ManRandom(0) & 1) ? XVS1 : XVS0;
 }
 static inline int  Abc_XsimRand3()   
 {
     int RetValue;
     do { 
-        RetValue = rand() & 3; 
+//        RetValue = rand() & 3; 
+        RetValue = Gia_ManRandom(0) & 3; 
     } while ( RetValue == 0 );
     return RetValue;
 }
@@ -108,7 +112,8 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fXInputs, int fXS
     Abc_Obj_t * pObj;
     int i, f;
     assert( Abc_NtkIsStrash(pNtk) );
-    srand( 0x12341234 );
+//    srand( 0x12341234 );
+    Gia_ManRandom( 1 );
     // start simulation
     Abc_ObjSetXsim( Abc_AigConst1(pNtk), XVS1 );
     if ( fXInputs )
@@ -194,7 +199,8 @@ void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fUseXval, int fVe
     Abc_Obj_t * pObj;
     int i, f;
     assert( Abc_NtkIsStrash(pNtk) );
-    srand( 0x12341234 );
+//    srand( 0x12341234 );
+    Gia_ManRandom( 1 );
     // initialize the values
     Abc_ObjSetXsim( Abc_AigConst1(pNtk), XVS1 );
     Abc_NtkForEachLatch( pNtk, pObj, i )
diff --git a/src/base/io/io.c b/src/base/io/io.c
index e29a3009..ecc6302f 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -2343,13 +2343,17 @@ int IoCommandWriteTruth( Abc_Frame_t * pAbc, int argc, char **argv )
     char * pFileName;
     FILE * pFile;
     unsigned * pTruth;
+    int fReverse = 0;
     int c;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "rh" ) ) != EOF )
     {
         switch ( c )
         {
+            case 'r':
+                fReverse ^= 1;
+                break;
             case 'h':
                 goto usage;
             default:
@@ -2394,7 +2398,7 @@ int IoCommandWriteTruth( Abc_Frame_t * pAbc, int argc, char **argv )
     // convert to logic
     Abc_NtkToAig( pNtk );
     vTruth = Vec_IntAlloc( 0 );
-    pTruth = Hop_ManConvertAigToTruth( pNtk->pManFunc, pNode->pData, Abc_ObjFaninNum(pNode), vTruth, 0 );
+    pTruth = Hop_ManConvertAigToTruth( pNtk->pManFunc, pNode->pData, Abc_ObjFaninNum(pNode), vTruth, fReverse );
     pFile = fopen( pFileName, "w" );
     if ( pFile == NULL )
     {
@@ -2408,8 +2412,9 @@ int IoCommandWriteTruth( Abc_Frame_t * pAbc, int argc, char **argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_truth [-h] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_truth [-rh] <file>\n" );
     fprintf( pAbc->Err, "\t         writes truth table into a file\n" );
+    fprintf( pAbc->Err, "\t-r     : toggle reversing bits in the truth table [default = %s]\n", fReverse? "yes":"no" );
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
     fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
     return 1;
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index b6eb29e3..f2c3e8c2 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -535,6 +535,71 @@ int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens )
   SeeAlso     []
 
 ***********************************************************************/
+int Io_ReadBlifReorderFormalNames( Vec_Ptr_t * vTokens, Mio_Gate_t * pGate )
+{
+    Mio_Pin_t * pGatePin;
+    char * pName, * pNamePin;
+    int i, k, nSize, Length;
+    nSize = Vec_PtrSize(vTokens);
+    if ( nSize - 3 != Mio_GateReadInputs(pGate) )
+        return 0;
+    // check if the names are in order
+    for ( pGatePin = Mio_GateReadPins(pGate), i = 0; pGatePin; pGatePin = Mio_PinReadNext(pGatePin), i++ )
+    {
+        pNamePin = Mio_PinReadName(pGatePin);
+        Length = strlen(pNamePin);
+        pName = Vec_PtrEntry(vTokens, i+2);
+        if ( !strncmp( pNamePin, pName, Length ) && pName[Length] == '=' )
+            continue;
+        break;
+    }
+    if ( i == nSize - 3 )
+        return 1;
+    // reorder the pins
+    for ( pGatePin = Mio_GateReadPins(pGate), i = 0; pGatePin; pGatePin = Mio_PinReadNext(pGatePin), i++ )
+    {
+        pNamePin = Mio_PinReadName(pGatePin);
+        Length = strlen(pNamePin);
+        for ( k = 2; k < nSize; k++ )
+        {
+            pName = Vec_PtrEntry(vTokens, k);
+            if ( !strncmp( pNamePin, pName, Length ) && pName[Length] == '=' )
+            {
+                Vec_PtrPush( vTokens, pName );
+                break;
+            }
+        }
+    }
+    pNamePin = Mio_GateReadOutName(pGate);
+    Length = strlen(pNamePin);
+    for ( k = 2; k < nSize; k++ )
+    {
+        pName = Vec_PtrEntry(vTokens, k);
+        if ( !strncmp( pNamePin, pName, Length ) && pName[Length] == '=' )
+        {
+            Vec_PtrPush( vTokens, pName );
+            break;
+        }
+    }
+    if ( Vec_PtrSize(vTokens) - nSize != nSize - 2 )
+        return 0;
+    Vec_PtrForEachEntryStart( vTokens, pName, k, nSize )
+        Vec_PtrWriteEntry( vTokens, k - nSize + 2, pName );
+    Vec_PtrShrink( vTokens, nSize );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Io_ReadBlifNetworkGate( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
 {
     Mio_Library_t * pGenlib; 
@@ -581,6 +646,16 @@ int Io_ReadBlifNetworkGate( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
         p->pNtkCur->pManFunc = pGenlib;
     }
 
+    // reorder the formal inputs to be in the same order as in the gate
+    if ( !Io_ReadBlifReorderFormalNames( vTokens, pGate ) )
+    {
+        p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
+        sprintf( p->sError, "Mismatch in the fanins of gate \"%s\".", (char*)vTokens->pArray[1] );
+        Io_ReadBlifPrintErrorMessage( p );
+        return 1;
+    }
+
+
     // remove the formal parameter names
     for ( i = 2; i < vTokens->nSize; i++ )
     {
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index 95e7cd1d..2e2388d3 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -1828,6 +1828,7 @@ static char * Io_ReadBlifCleanName( char * pName )
 ***********************************************************************/
 static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens )
 {
+    extern int Io_ReadBlifReorderFormalNames( Vec_Ptr_t * vTokens, Mio_Gate_t * pGate );
     Mio_Library_t * pGenlib; 
     Mio_Gate_t * pGate;
     Abc_Obj_t * pNode;
@@ -1868,6 +1869,13 @@ static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens )
         p->pNtk->pManFunc = pGenlib;
     }
 
+    // reorder the formal inputs to be in the same order as in the gate
+    if ( !Io_ReadBlifReorderFormalNames( vTokens, pGate ) )
+    {
+        sprintf( p->pMan->sError, "Line %d: Mismatch in the fanins of gate \"%s\".", Io_MvGetLine(p->pMan, pName), (char*)vTokens->pArray[1] );
+        return 0;
+    }
+
     // remove the formal parameter names
     for ( i = 2; i < vTokens->nSize; i++ )
     {
diff --git a/src/base/main/main.c b/src/base/main/main.c
index 3aee2e44..738f217c 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -310,6 +310,130 @@ static int TypeCheck( Abc_Frame_t * pAbc, char * s )
     }
 }
 
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Find the file name.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_MainFileName( char * pFileName )
+{
+    static char Buffer[200];
+    char * pExtension;
+    assert( strlen(pFileName) < 190 );
+    pExtension = Extra_FileNameExtension( pFileName );
+    if ( pExtension == NULL )
+        sprintf( Buffer, "%s.opt", pFileName );
+    else
+    {
+        strncpy( Buffer, pFileName, pExtension-pFileName-1 );
+        sprintf( Buffer+(pExtension-pFileName-1), ".opt.%s", pExtension );
+    }
+    return Buffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [The main() procedure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int main_( int argc, char * argv[] )
+{
+    extern void Nwk_ManPrintStatsUpdate( void * p, void * pAig, void * pNtk,
+         int nRegInit, int nLutInit, int nLevInit, int Time );
+    char * pComs[20] = 
+    {
+/*00*/  "*r -am ",
+/*01*/  "*w -abc 1.aig",
+/*02*/  "*lcorr -nc",//; *ps",
+/*03*/  "*scorr -nc",//; *ps",
+/*04*/  "*dch; *if -K 4 -C 16 -F 3 -A 2; *sw -m",//; *ps",
+/*05*/  "*dch; *if -K 4 -C 16 -F 3 -A 2; *sw -m",//; *ps", 
+/*06*/  "*w ",
+/*07*/  "*w -abc 2.aig",
+/*08*/  "miter -mc 1.aig 2.aig; sim -F 4 -W 4 -mv"
+    };
+    char Command[1000];
+    int i, nComs;
+    Abc_Frame_t * pAbc;
+    FILE * pFile;
+    int nRegInit, nLutInit, nLevInit;
+    int clkStart = clock();
+
+    // added to detect memory leaks:
+#if defined(_DEBUG) && defined(_MSC_VER) 
+    _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
+#endif
+
+    // check that the file is present
+    if ( argc != 2 )
+    {
+        printf( "Expecting one command argument (file name).\n" );
+        return 0;
+    }
+    pFile = fopen( argv[1], "r" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\".\n", argv[1] );
+        return 0;
+    }
+    fclose( pFile );
+
+    // count the number of commands
+    for ( nComs = 0; nComs < 20; nComs++ )
+        if ( pComs[nComs] == NULL )
+            break;
+    // perform the commands
+    printf( "Reading design \"%s\"...\n", argv[1] );
+    pAbc = Abc_FrameGetGlobalFrame();
+    for ( i = 0; i < nComs; i++ )
+    {
+
+        if ( i == 0 )
+            sprintf( Command, "%s%s", pComs[i], argv[1] );
+        else if ( i == 6 )
+            sprintf( Command, "%s%s", pComs[i], Abc_MainFileName(argv[1]) );
+        else 
+            sprintf( Command, "%s", pComs[i] );
+        if ( Cmd_CommandExecute( pAbc, Command ) )
+        {
+            printf( "Internal command %d failed.\n", i );
+            return 0;
+        }
+        if ( i == 0 )
+        {
+            extern int Nwk_ManStatsRegs( void * p );
+            extern int Nwk_ManStatsLuts( void * pNtk );
+            extern int Nwk_ManStatsLevs( void * pNtk );
+            nRegInit = Nwk_ManStatsRegs( pAbc->pAbc8Ntl );
+            nLutInit = Nwk_ManStatsLuts( pAbc->pAbc8Nwk );
+            nLevInit = Nwk_ManStatsLevs( pAbc->pAbc8Nwk );
+        }
+        if ( i >= 1 && i <= 5 )
+        Nwk_ManPrintStatsUpdate( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, pAbc->pAbc8Nwk, 
+            nRegInit, nLutInit, nLevInit, clkStart );
+    }
+    Abc_Stop(); 
+    printf( "Writing optimized design \"%s\"...\n", Abc_MainFileName(argv[1]) );
+    ABC_PRT( "Total time", clock() - clkStart );
+    printf( "\n" );
+    return 0;  
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////