Version abc80207

17 files changed, 672 insertions, 98 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 339fd810..64268358 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -39,7 +39,7 @@ extern "C" {
 #include "aig.h"
 #include "dar.h"
 #include "satSolver.h"
-//#include "bar.h"
+#include "ioa.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c
index a35e1169..8e3a03e1 100644
--- a/src/aig/fra/fraClaus.c
+++ b/src/aig/fra/fraClaus.c
@@ -1530,7 +1530,7 @@ void Fra_ClausWriteIndClauses( Clu_Man_t * p )
     extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
     Aig_Man_t * pNew;
     Aig_Obj_t * pClause, * pLiteral;
-    char Buffer[500];
+    char Buffer[500], * pName;
     int * pStart, * pVar2Id; 
     int Beg, End, i, k;
     // create mapping from SAT vars to node IDs
@@ -1561,7 +1561,9 @@ void Fra_ClausWriteIndClauses( Clu_Man_t * p )
     free( pVar2Id );
     Aig_ManCleanup( pNew );
     // write the manager into a file
-    sprintf( Buffer, "%s_care.aig", p->pAig->pName );
+    pName = Ioa_FileNameGeneric(p->pAig->pName);
+    sprintf( Buffer, "%s_care.aig", pName );
+    free( pName );
     printf( "Care clauses are written into file \"%s\".\n", Buffer );
     Ioa_WriteAiger( pNew, Buffer, 0, 1 );
     Aig_ManStop( pNew );
diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c
index 4a3f9b03..8796f827 100644
--- a/src/aig/fra/fraHot.c
+++ b/src/aig/fra/fraHot.c
@@ -130,7 +130,7 @@ int Fra_OneHotNodesAreClause( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * p
 ***********************************************************************/
 Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim )
 {
-    int fSkipConstEqu = 1;
+    int fSkipConstEqu = 0;
     Vec_Int_t * vOneHots;
     Aig_Obj_t * pObj1, * pObj2;
     int i, k;
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 07044b52..ea17706c 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -471,12 +471,14 @@ clk2 = clock();
     if ( p->pPars->fWriteImps && p->vOneHots && Fra_OneHotCount(p, p->vOneHots) )
     {
         extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
-        char Buffer[500];
+        char Buffer[500], * pStart;
         Aig_Man_t * pNew;
         pManAigNew = Aig_ManDup( pManAig, 1 );
 //        pManAigNew->pManExdc = Fra_OneHotCreateExdc( p, p->vOneHots );
         pNew = Fra_OneHotCreateExdc( p, p->vOneHots );
-        sprintf( Buffer, "%s_care.aig", p->pManAig->pName );
+        pStart = Ioa_FileNameGeneric(p->pManAig->pName);
+        sprintf( Buffer, "%s_care.aig", pStart );
+        free( pStart );
         printf( "Care one-hotness clauses are written into file \"%s\".\n", Buffer );
         Ioa_WriteAiger( pNew, Buffer, 0, 1 );
         Aig_ManStop( pNew );
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index de517705..c882672b 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -1025,7 +1025,7 @@ int Abc_NtkLevelReverse( Abc_Ntk_t * pNtk )
     return LevelsMax;
 }
 
-
+ 
 /**Function*************************************************************
 
   Synopsis    [Recursively detects combinational loops.]
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 266f8075..4b872aa3 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3130,7 +3130,7 @@ int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nWindow      = 62;
     pPars->nCands       =  5;
     pPars->nSimWords    =  4;
-    pPars->nGrowthLevel =  0;
+    pPars->nGrowthLevel =  1;
     pPars->fArea        =  0;
     pPars->fVerbose     =  0;
     pPars->fVeryVerbose =  0;
@@ -3225,7 +3225,7 @@ usage:
     fprintf( pErr, "\t-W <NM>  : fanin/fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
     fprintf( pErr, "\t-C <num> : the max number of resub candidates (1 <= n) [default = %d]\n", pPars->nCands );
     fprintf( pErr, "\t-S <num> : the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords );
-    fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
+    fprintf( pErr, "\t-L <num> : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
     fprintf( pErr, "\t-a       : toggle optimization for area only [default = %s]\n", pPars->fArea? "yes": "no" );
     fprintf( pErr, "\t-v       : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w       : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
@@ -3264,13 +3264,15 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nDepthMax    =  20;
     pPars->nDivMax      = 200;
     pPars->nWinSizeMax  = 300;
-    pPars->nGrowthLevel =   0;
+    pPars->nGrowthLevel =   1;
     pPars->fResub       =   1;
     pPars->fArea        =   0;
+    pPars->fMoreEffort  =   0;
+    pPars->fSwapEdge    =   0;
     pPars->fVerbose     =   0;
     pPars->fVeryVerbose =   0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLravwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLraesvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -3335,6 +3337,12 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'a':
             pPars->fArea ^= 1;
             break;
+        case 'e':
+            pPars->fMoreEffort ^= 1;
+            break;
+        case 's':
+            pPars->fSwapEdge ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -3368,15 +3376,17 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: mfs [-WFDML <num>] [-arvh]\n" );
+    fprintf( pErr, "usage: mfs [-WFDML <num>] [-raesvh]\n" );
     fprintf( pErr, "\t           performs don't-care-based optimization of logic networks\n" );
     fprintf( pErr, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs );
     fprintf( pErr, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax );
     fprintf( pErr, "\t-D <num> : the max depth nodes to try (0 = no limit) [default = %d]\n", pPars->nDepthMax );
     fprintf( pErr, "\t-M <num> : the max size of  window to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );
-    fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
-    fprintf( pErr, "\t-a       : toggle minimizing area or edges [default = %s]\n", pPars->fArea? "area": "edges" );
+    fprintf( pErr, "\t-L <num> : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
     fprintf( pErr, "\t-r       : toggle resubstitution and dc-minimization [default = %s]\n", pPars->fResub? "resub": "dc-min" );
+    fprintf( pErr, "\t-a       : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
+    fprintf( pErr, "\t-e       : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" );
+    fprintf( pErr, "\t-s       : toggle evaluation of edge swapping [default = %s]\n", pPars->fSwapEdge? "yes": "no" );
     fprintf( pErr, "\t-v       : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w       : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     fprintf( pErr, "\t-h       : print the command usage\n");
@@ -6208,12 +6218,14 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fSorter;
     int fMesh;
     int fFpga;
+    int fOneHot;
     int fVerbose;
     char * FileName;
     extern void Abc_GenAdder( char * pFileName, int nVars );
     extern void Abc_GenSorter( char * pFileName, int nVars );
     extern void Abc_GenMesh( char * pFileName, int nVars );
     extern void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars );
+    extern void Abc_GenOneHot( char * pFileName, int nVars );
 
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -6226,9 +6238,10 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
     fSorter = 0;
     fMesh = 0;
     fFpga = 0;
+    fOneHot = 0;
     fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Nasmfvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Nasmftvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -6255,6 +6268,9 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'f':
             fFpga ^= 1;
             break;
+        case 't':
+            fOneHot ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -6282,18 +6298,21 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_GenFpga( FileName, 4, 3, 10 );
 //        Abc_GenFpga( FileName, 2, 2, 3 );
 //        Abc_GenFpga( FileName, 3, 2, 5 );
+    else if ( fOneHot )
+        Abc_GenOneHot( FileName, nVars );
     else
         printf( "Type of circuit is not specified.\n" );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: gen [-N] [-asmfvh] <file>\n" );
+    fprintf( pErr, "usage: gen [-N num] [-asmftvh] <file>\n" );
     fprintf( pErr, "\t         generates simple circuits\n" );
     fprintf( pErr, "\t-N num : the number of variables [default = %d]\n", nVars );  
     fprintf( pErr, "\t-a     : generate ripple-carry adder [default = %s]\n", fAdder? "yes": "no" );  
     fprintf( pErr, "\t-s     : generate a sorter [default = %s]\n", fSorter? "yes": "no" );  
     fprintf( pErr, "\t-m     : generate a mesh [default = %s]\n", fMesh? "yes": "no" );  
     fprintf( pErr, "\t-f     : generate a LUT FPGA structure [default = %s]\n", fFpga? "yes": "no" );  
+    fprintf( pErr, "\t-t     : generate one-hotness conditions [default = %s]\n", fOneHot? "yes": "no" );  
     fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
     fprintf( pErr, "\t<file> : output file name\n");
@@ -6634,7 +6653,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
     extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
 //    extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
-    extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
+//    extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
     extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
 //    extern void Abc_NtkDarTestBlif( char * pFileName );
 
diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c
index bfb41374..0b66c476 100644
--- a/src/base/abci/abcGen.c
+++ b/src/base/abci/abcGen.c
@@ -504,6 +504,48 @@ void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars )
     fclose( pFile );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Generates structure of L K-LUTs implementing an N-var function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_GenOneHot( char * pFileName, int nVars )
+{
+    FILE * pFile;
+    int i, k, Counter, nDigitsIn, nDigitsOut;
+    pFile = fopen( pFileName, "w" );
+    fprintf( pFile, "# One-hotness condition for %d vars generated by ABC on %s\n", nVars, Extra_TimeStamp() );
+    fprintf( pFile, ".model 1hot_%dvars\n", nVars );
+    fprintf( pFile, ".inputs" );
+    nDigitsIn = Extra_Base10Log( nVars );
+    for ( i = 0; i < nVars; i++ )
+        fprintf( pFile, " i%0*d", nDigitsIn, i );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, ".outputs" );
+    nDigitsOut = Extra_Base10Log( nVars * (nVars - 1) / 2 );
+    for ( i = 0; i < nVars * (nVars - 1) / 2; i++ )
+        fprintf( pFile, " o%0*d", nDigitsOut, i );
+    fprintf( pFile, "\n" );
+    Counter = 0;
+    for ( i = 0; i < nVars; i++ )
+        for ( k = i+1; k < nVars; k++ )
+        {
+            fprintf( pFile, ".names i%0*d i%0*d o%0*d\n", nDigitsIn, i, nDigitsIn, k, nDigitsOut, Counter ); 
+            fprintf( pFile, "11 0\n" ); 
+            Counter++;
+        }
+    fprintf( pFile, ".end\n" ); 
+    fprintf( pFile, "\n" ); 
+    fclose( pFile );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 257d930f..a054a474 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -1130,6 +1130,7 @@ int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd )
     pNode = Abc_NtkCreatePo( pNtk );
     Abc_ObjAddFanin( pNode, pMiter );
     Abc_ObjAssignName( pNode, "miter", NULL );
+    Abc_NtkOrderCisCos( pNtk );
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtk ) )
     {
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 2dc03d5c..8640b7a8 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -46,6 +46,7 @@ static int CmdCommandRecall        ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int CmdCommandEmpty         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 #ifdef WIN32
 static int CmdCommandLs            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int CmdCommandScrGen        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 #endif
 static int CmdCommandSis           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandMvsis         ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -86,6 +87,7 @@ void Cmd_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Basic", "empty",     CmdCommandEmpty,          0); 
 #ifdef WIN32
     Cmd_CommandAdd( pAbc, "Basic", "ls",        CmdCommandLs,             0 );
+    Cmd_CommandAdd( pAbc, "Basic", "scrgen",    CmdCommandScrGen,         0 );
 #endif
 
     Cmd_CommandAdd( pAbc, "Various", "sis",     CmdCommandSis,            1); 
@@ -1068,17 +1070,6 @@ usage:
 
 
 #ifdef WIN32
-/**Function*************************************************************
-
-  Synopsis    [Command to print the contents of the current directory (Windows).]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 #include <io.h>
 
 // these structures are defined in <io.h> but are for some reason invisible
@@ -1097,6 +1088,20 @@ extern long _findfirst( char *filespec, struct _finddata_t *fileinfo );
 extern int  _findnext( long handle, struct _finddata_t *fileinfo );
 extern int  _findclose( long handle );
 
+extern char * _getcwd( char * buffer, int maxlen );
+extern int    _chdir( const char *dirname );
+
+/**Function*************************************************************
+
+  Synopsis    [Command to print the contents of the current directory (Windows).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int CmdCommandLs( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     struct _finddata_t c_file;
@@ -1181,15 +1186,238 @@ int CmdCommandLs( Abc_Frame_t * pAbc, int argc, char **argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "Usage: ls [-l] [-b]\n" );
+    fprintf( pAbc->Err, "usage: ls [-l] [-b]\n" );
     fprintf( pAbc->Err, "       print the file names in the current directory\n" );
     fprintf( pAbc->Err, "        -l : print in the long format [default = short]\n" );
     fprintf( pAbc->Err, "        -b : print only .mv files [default = all]\n" );
     return 1; 
 }
-#endif
 
 
+/**Function*************************************************************
+
+  Synopsis    [Generates the script for running ABC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int CmdCommandScrGen( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    struct _finddata_t c_file;
+    long   hFile;
+    FILE * pFile = NULL;
+    char * pFileStr = "test.s";
+    char * pDirStr = NULL;
+    char * pComStr = "ps";
+    char * pWriteStr = NULL;
+    char   Buffer[1000], Line[2000];
+    int    nFileNameMax, nFileNameCur;
+    int    Counter = 0;
+    int    fUseCurrent;
+    char   c;
+
+    fUseCurrent = 0;
+    Extra_UtilGetoptReset();
+    while ( (c = Extra_UtilGetopt(argc, argv, "FDCWch") ) != EOF )
+    {
+        switch (c)
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pAbc->Err, "Command line switch \"-F\" should be followed by a string.\n" );
+                goto usage;
+            }
+            pFileStr = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pAbc->Err, "Command line switch \"-D\" should be followed by a string.\n" );
+                goto usage;
+            }
+            pDirStr = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pAbc->Err, "Command line switch \"-C\" should be followed by a string.\n" );
+                goto usage;
+            }
+            pComStr = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pAbc->Err, "Command line switch \"-W\" should be followed by a string.\n" );
+                goto usage;
+            }
+            pWriteStr = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
+        case 'c':
+            fUseCurrent ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+
+//    printf( "File = %s.\n", pFileStr );
+//    printf( "Dir = %s.\n", pDirStr );
+//    printf( "Com = %s.\n", pComStr );
+    if ( pDirStr == NULL )
+        fUseCurrent = 1;
+
+    if ( _getcwd( Buffer, 1000 ) == NULL )
+    {
+        printf( "Cannot get the current directory.\n" );
+        return 0;
+    }
+    if ( fUseCurrent )
+        pFile = fopen( pFileStr, "w" );
+    if ( pDirStr )
+    {
+        if ( _chdir(pDirStr) )
+        {
+            printf( "Cannot change to directory: %s\n", pDirStr );
+            return 0;
+        }
+    }
+    if ( !fUseCurrent )
+        pFile = fopen( pFileStr, "w" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file %s.\n", pFileStr );
+        if ( pDirStr && _chdir(Buffer) )
+        {
+            printf( "Cannot change to the current directory: %s\n", Buffer );
+            return 0;
+        }
+        return 0;
+    }
+
+    // find the first file in the directory
+    if( (hFile = _findfirst( "*.*", &c_file )) == -1L )
+    {
+        if ( pDirStr )
+            printf( "No files in the current directory.\n" );
+        else
+            printf( "No files in directory: %s\n", pDirStr );
+        if ( pDirStr && _chdir(Buffer) )
+        {
+            printf( "Cannot change to the current directory: %s\n", Buffer );
+            return 0;
+        }
+    }
+
+    // get the longest file name
+    {
+        nFileNameMax = 0;
+        do
+        {
+            // skip script and txt files
+            nFileNameCur = strlen(c_file.name);
+            if ( c_file.name[nFileNameCur-1] == '.' )
+                continue;
+            if ( nFileNameCur > 2 &&
+                 c_file.name[nFileNameCur-1] == 's' && 
+                 c_file.name[nFileNameCur-2] == '.' ) 
+                 continue;
+            if ( nFileNameCur > 4 &&
+                 c_file.name[nFileNameCur-1] == 't' && 
+                 c_file.name[nFileNameCur-2] == 'x' && 
+                 c_file.name[nFileNameCur-3] == 't' && 
+                 c_file.name[nFileNameCur-4] == '.' ) 
+                 continue;
+            if ( nFileNameMax < nFileNameCur )
+                nFileNameMax = nFileNameCur;
+        }
+        while( _findnext( hFile, &c_file ) == 0 );
+        _findclose( hFile );
+    }
+
+    // print the script file
+    {
+        if( (hFile = _findfirst( "*.*", &c_file )) == -1L )
+        {
+            if ( pDirStr )
+                printf( "No files in the current directory.\n" );
+            else
+                printf( "No files in directory: %s\n", pDirStr );
+        }
+        fprintf( pFile, "# Script file produced by ABC on %s\n", Extra_TimeStamp() );
+        fprintf( pFile, "# Command line was: scrgen -F %s -D %s -C \"%s\"%s%s\n", 
+            pFileStr, pDirStr, pComStr, pWriteStr?" -W ":"", pWriteStr?pWriteStr:"" );
+        do
+        {
+            // skip script and txt files
+            nFileNameCur = strlen(c_file.name);
+            if ( c_file.name[nFileNameCur-1] == '.' )
+                continue;
+            if ( nFileNameCur > 2 &&
+                 c_file.name[nFileNameCur-1] == 's' && 
+                 c_file.name[nFileNameCur-2] == '.' ) 
+                 continue;
+            if ( nFileNameCur > 4 &&
+                 c_file.name[nFileNameCur-1] == 't' && 
+                 c_file.name[nFileNameCur-2] == 'x' && 
+                 c_file.name[nFileNameCur-3] == 't' && 
+                 c_file.name[nFileNameCur-4] == '.' ) 
+                 continue;
+            sprintf( Line, "r %s%s%-*s ; %s", pDirStr?pDirStr:"", pDirStr?"/":"", nFileNameMax, c_file.name, pComStr );
+            for ( c = (int)strlen(Line)-1; c >= 0; c-- )
+                if ( Line[c] == '\\' )
+                    Line[c] = '/';
+            fprintf( pFile, "%s", Line );
+            if ( pWriteStr )
+            {
+                sprintf( Line, " ; w %s/%-*s", pWriteStr, nFileNameMax, c_file.name );
+                for ( c = (int)strlen(Line)-1; c >= 0; c-- )
+                    if ( Line[c] == '\\' )
+                        Line[c] = '/';
+                fprintf( pFile, "%s", Line );
+            }
+            fprintf( pFile, "\n", Line );
+        }
+        while( _findnext( hFile, &c_file ) == 0 );
+        _findclose( hFile );
+    }
+    fclose( pFile );
+    if ( pDirStr && _chdir(Buffer) )
+    {
+        printf( "Cannot change to the current directory: %s\n", Buffer );
+        return 0;
+    }
+
+    // report
+    if ( fUseCurrent )
+        printf( "Script file \"%s\" was saved in the current directory.\n", pFileStr );
+    else
+        printf( "Script file \"%s\" was saved in directory: %s\n", pFileStr, pDirStr );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: scrgen -F <str> -D <str> -C <str> -W <str> -ch\n" );
+    fprintf( pAbc->Err, "\t          generates script for running ABC\n" );
+    fprintf( pAbc->Err, "\t-F str  : the name of the script file [default = \"test.s\"]\n" );
+    fprintf( pAbc->Err, "\t-D str  : the directory to read files from [default = current]\n" );
+    fprintf( pAbc->Err, "\t-C str  : the sequence of commands to run [default = \"ps\"]\n" );
+    fprintf( pAbc->Err, "\t-W str  : the directory to write the resulting files [default = no writing]\n" );
+    fprintf( pAbc->Err, "\t-c      : toggle placing file in current/target dir [default = %s]\n", fUseCurrent? "current": "target" );
+    fprintf( pAbc->Err, "\t-h      : print the command usage\n\n");
+    fprintf( pAbc->Err, "\tExample : scrgen -F test1.s -D a/in -C \"ps; st; ps\" -W a/out\n" );
+    return 1; 
+}
+#endif
+
 
 #ifdef WIN32
 #define unlink _unlink
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index d0750178..ffa25c7f 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -218,7 +218,20 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
     p->pNtkCur = pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 );
     // read the model name
     if ( strcmp( p->vTokens->pArray[0], ".model" ) == 0 )
-        pNtk->pName = Extra_UtilStrsav( p->vTokens->pArray[1] );
+    {
+        char * pToken, * pPivot;
+        if ( Vec_PtrSize(p->vTokens) != 2 )
+        {
+            p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
+            sprintf( p->sError, "The .model line does not have exactly two entries." );
+            Io_ReadBlifPrintErrorMessage( p );
+            return NULL;
+        }
+        for ( pPivot = pToken = Vec_PtrEntry(p->vTokens, 1); *pToken; pToken++ )
+            if ( *pToken == '/' || *pToken == '\\' )
+                pPivot = pToken+1;
+        pNtk->pName = Extra_UtilStrsav( pPivot );
+    }
     else if ( strcmp( p->vTokens->pArray[0], ".exdc" ) != 0 ) 
     {
         printf( "%s: File parsing skipped after line %d (\"%s\").\n", p->pFileName, 
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index 97f2fbf3..8a1fe309 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -90,7 +90,7 @@ static Io_MvMod_t *      Io_MvModAlloc();
 static void              Io_MvModFree( Io_MvMod_t * p );
 static char *            Io_MvLoadFile( char * pFileName );
 static void              Io_MvReadPreparse( Io_MvMan_t * p );
-static void              Io_MvReadInterfaces( Io_MvMan_t * p );
+static int               Io_MvReadInterfaces( Io_MvMan_t * p );
 static Abc_Lib_t *       Io_MvParse( Io_MvMan_t * p );
 static int               Io_MvParseLineModel( Io_MvMod_t * p, char * pLine );
 static int               Io_MvParseLineInputs( Io_MvMod_t * p, char * pLine );
@@ -128,7 +128,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
     FILE * pFile;
     Io_MvMan_t * p;
     Abc_Ntk_t * pNtk;
-    Abc_Lib_t * pDesign;
+    Abc_Lib_t * pDesign = NULL;
     char * pDesignName;
     int RetValue, i;
 
@@ -161,10 +161,9 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
     p->pDesign->pManFunc = NULL;
     // prepare the file for parsing
     Io_MvReadPreparse( p );
-    // parse interfaces of each network
-    Io_MvReadInterfaces( p );
-    // construct the network
-    pDesign = Io_MvParse( p );
+    // parse interfaces of each network and construct the network
+    if ( Io_MvReadInterfaces( p ) )
+        pDesign = Io_MvParse( p );
     if ( p->sError[0] )
         fprintf( stdout, "%s\n", p->sError );
     Io_MvFree( p );
@@ -646,7 +645,7 @@ static void Io_MvReadPreparse( Io_MvMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static void Io_MvReadInterfaces( Io_MvMan_t * p )
+static int Io_MvReadInterfaces( Io_MvMan_t * p )
 {
     Io_MvMod_t * pMod;
     char * pLine;
@@ -656,22 +655,23 @@ static void Io_MvReadInterfaces( Io_MvMan_t * p )
     {
         // parse the model
         if ( !Io_MvParseLineModel( pMod, pMod->pName ) )
-            return;
+            return 0;
         // add model to the design
         if ( !Abc_LibAddModel( p->pDesign, pMod->pNtk ) )
         {
             sprintf( p->sError, "Line %d: Model %s is defined twice.", Io_MvGetLine(p, pMod->pName), pMod->pName );
-            return;
+            return 0;
         }
         // parse the inputs
         Vec_PtrForEachEntry( pMod->vInputs, pLine, k )
             if ( !Io_MvParseLineInputs( pMod, pLine ) )
-                return;
+                return 0;
         // parse the outputs
         Vec_PtrForEachEntry( pMod->vOutputs, pLine, k )
             if ( !Io_MvParseLineOutputs( pMod, pLine ) )
-                return;
+                return 0;
     }
+    return 1;
 }
 
 
@@ -767,7 +767,7 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p )
 static int Io_MvParseLineModel( Io_MvMod_t * p, char * pLine )
 {
     Vec_Ptr_t * vTokens = p->pMan->vTokens;
-    char * pToken;
+    char * pToken, * pPivot;
     Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
     pToken = Vec_PtrEntry( vTokens, 0 );
     assert( !strcmp(pToken, "model") );
@@ -782,7 +782,10 @@ static int Io_MvParseLineModel( Io_MvMod_t * p, char * pLine )
         p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLIFMV, 1 );
     else 
         p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 );
-    p->pNtk->pName = Extra_UtilStrsav( Vec_PtrEntry(vTokens, 1) );
+    for ( pPivot = pToken = Vec_PtrEntry(vTokens, 1); *pToken; pToken++ )
+        if ( *pToken == '/' || *pToken == '\\' )
+            pPivot = pToken+1;
+    p->pNtk->pName = Extra_UtilStrsav( pPivot );
     return 1;
 }
 
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index 9595bc72..df06168c 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -705,6 +705,24 @@ static inline void Vec_PtrCleanSimInfo( Vec_Ptr_t * vInfo, int iWord, int nWords
 
 /**Function*************************************************************
 
+  Synopsis    [Cleans simulation info of each entry beginning with iWord.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrFillSimInfo( Vec_Ptr_t * vInfo, int iWord, int nWords )
+{
+    int i;
+    for ( i = 0; i < vInfo->nSize; i++ )
+        memset( (char*)Vec_PtrEntry(vInfo,i) + 4*iWord, 0xFF, 4*(nWords-iWord) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Resizes the array of simulation info.]
 
   Description [Doubles the number of objects for which siminfo is allocated.]
diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h
index 9fc6a253..cb2da431 100644
--- a/src/opt/mfs/mfs.h
+++ b/src/opt/mfs/mfs.h
@@ -49,6 +49,8 @@ struct Mfs_Par_t_
     int           nGrowthLevel;  // the maximum allowed growth in level
     int           fResub;        // performs resubstitution
     int           fArea;         // performs optimization for area
+    int           fMoreEffort;   // performs high-affort minimization
+    int           fSwapEdge;     // performs edge swapping
     int           fDelay;        // performs optimization for delay
     int           fVerbose;      // enable basic stats
     int           fVeryVerbose;  // enable detailed stats
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 332a6ad9..aed0abe5 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -74,10 +74,14 @@ clk = clock();
         return 1;
     }
     // solve the SAT problem
-    if ( p->pPars->fArea )
-        Abc_NtkMfsResubArea( p, pNode );
+    if ( p->pPars->fSwapEdge )
+        Abc_NtkMfsEdgeSwapEval( p, pNode );
     else
-        Abc_NtkMfsResubEdge( p, pNode );
+    {
+        Abc_NtkMfsResubNode( p, pNode );
+        if ( p->pPars->fMoreEffort )
+            Abc_NtkMfsResubNode2( p, pNode );
+    }
 p->timeSat += clock() - clk;
     return 1;
 }
@@ -140,12 +144,13 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
     ProgressBar * pProgress;
     Mfs_Man_t * p;
     Abc_Obj_t * pObj;
-    int i, clk = clock();
+    int i, nFaninMax, clk = clock();
     int nTotalNodesBeg = Abc_NtkNodeNum(pNtk);
     int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk);
 
     assert( Abc_NtkIsLogic(pNtk) );
-    if ( Abc_NtkGetFaninMax(pNtk) > MFS_FANIN_MAX )
+    nFaninMax = Abc_NtkGetFaninMax(pNtk);
+    if ( nFaninMax > MFS_FANIN_MAX )
     {
         printf( "Some nodes have more than %d fanins. Quitting.\n", MFS_FANIN_MAX );
         return 1;
@@ -162,7 +167,8 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
 
     // start the manager
     p = Mfs_ManAlloc( pPars );
-    p->pNtk  = pNtk;
+    p->pNtk = pNtk;
+    p->nFaninMax = nFaninMax;
     if ( pNtk->pExcare )
     {
         Abc_Ntk_t * pTemp;
@@ -170,7 +176,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
         p->pCare = Abc_NtkToDar( pTemp, 0 );
         Abc_NtkDelete( pTemp );
     }
-    if ( pPars->fVerbose )
+//    if ( pPars->fVerbose )
     {
         if ( p->pCare != NULL )
             printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) );
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index 54826bc1..ddd16407 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -49,6 +49,7 @@ struct Mfs_Man_t_
     Mfs_Par_t *         pPars;
     Abc_Ntk_t *         pNtk;
     Aig_Man_t *         pCare;
+    int                 nFaninMax;
     // intermeditate data for the node
     Vec_Ptr_t *         vRoots;    // the roots of the window
     Vec_Ptr_t *         vSupp;     // the support of the window
@@ -78,7 +79,6 @@ struct Mfs_Man_t_
     // performance statistics
     int                 nNodesTried;
     int                 nNodesResub;
-    int                 nNodesGained;
     int                 nMintsCare;
     int                 nMintsTotal;
     int                 nNodesBad;
@@ -119,8 +119,10 @@ extern Mfs_Man_t *      Mfs_ManAlloc( Mfs_Par_t * pPars );
 extern void             Mfs_ManStop( Mfs_Man_t * p );
 extern void             Mfs_ManClean( Mfs_Man_t * p );
 /*=== mfsResub.c ==========================================================*/
-extern int              Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode );
-extern int              Abc_NtkMfsResubEdge( Mfs_Man_t * p, Abc_Obj_t * pNode );
+extern void             Abc_NtkMfsPrintResubStats( Mfs_Man_t * p );
+extern int              Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode );
+extern int              Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode );
+extern int              Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode );
 /*=== mfsSat.c ==========================================================*/
 extern void             Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode );
 /*=== mfsStrash.c ==========================================================*/
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index 67981d5a..519b855d 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -85,12 +85,12 @@ void Mfs_ManClean( Mfs_Man_t * p )
     if ( p->vDivs )
         Vec_PtrFree( p->vDivs );
     p->pAigWin = NULL;
-    p->pCnf   = NULL;
-    p->pSat   = NULL;
-    p->vRoots = NULL;
-    p->vSupp  = NULL;
-    p->vNodes = NULL;
-    p->vDivs  = NULL;
+    p->pCnf    = NULL;
+    p->pSat    = NULL;
+    p->vRoots  = NULL;
+    p->vSupp   = NULL;
+    p->vNodes  = NULL;
+    p->vDivs   = NULL;
 }
 
 /**Function*************************************************************
@@ -117,6 +117,11 @@ void Mfs_ManPrint( Mfs_Man_t * p )
         printf( "\n" );
         printf( "Nodes = %d. Tried = %d. Resub = %d. Skipped = %d. SAT calls = %d.\n", 
             Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nNodesBad, p->nSatCalls );
+        if ( p->pPars->fSwapEdge )
+            printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n", 
+                p->nNodesResub, Abc_NtkGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Abc_NtkGetTotalFanins(p->pNtk) );
+        else
+            Abc_NtkMfsPrintResubStats( p );
     }
     else
     {
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index ae1132f2..1e9da4d2 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -57,6 +57,35 @@ void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFani
 
 /**Function*************************************************************
 
+  Synopsis    [Prints resub candidate stats.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMfsPrintResubStats( Mfs_Man_t * p )
+{
+    Abc_Obj_t * pFanin, * pNode;
+    int i, k, nAreaCrits = 0, nAreaExpanse = 0;
+    int nFaninMax = Abc_NtkGetFaninMax(p->pNtk);
+    Abc_NtkForEachNode( p->pNtk, pNode, i )
+        Abc_ObjForEachFanin( pNode, pFanin, k )
+        {
+            if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
+            {
+                nAreaCrits++;
+                nAreaExpanse += (int)(Abc_ObjFaninNum(pNode) < nFaninMax);
+            }
+        }
+    printf( "Total area-critical fanins = %d. Belonging to expandable nodes = %d.\n", 
+        nAreaCrits, nAreaExpanse );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Tries resubstitution.]
 
   Description [Returns 1 if it is feasible, or 0 if c-ex is found.]
@@ -68,7 +97,7 @@ void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFani
 ***********************************************************************/
 int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
 {
-    unsigned * pData, * pDataTot;
+    unsigned * pData;
     int RetValue, iVar, i;
     p->nSatCalls++;
     RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
@@ -77,17 +106,16 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
         return 1;
     p->nSatCexes++;
     // store the counter-example
-    pData = Vec_PtrEntry( p->vDivCexes, p->nCexes++ );
-    assert( pData[0] == 0 );
     Vec_IntForEachEntry( p->vProjVars, iVar, i )
     {
-        if ( sat_solver_var_value( p->pSat, iVar ) )
-            Aig_InfoSetBit( pData, i );
+        pData = Vec_PtrEntry( p->vDivCexes, i );
+        if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!!
+        {
+            assert( Aig_InfoHasBit(pData, p->nCexes) );
+            Aig_InfoXorBit( pData, p->nCexes );
+        }
     }
-    // AND the result with the previous ones
-    pDataTot = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
-    for ( i = 0; i < p->nDivWords; i++ )
-        pDataTot[i] &= pData[i];
+    p->nCexes++;
     return 0;
 }
 
@@ -102,22 +130,19 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove )
+int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove, int fSkipUpdate )
 {
     int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
     unsigned * pData;
     int pCands[MFS_FANIN_MAX];
-    int iVar, i, nCands, clk;
+    int iVar, i, nCands, nWords, w, clk;
     Abc_Obj_t * pFanin;
     Hop_Obj_t * pFunc;
     assert( iFanin >= 0 );
 
     // clean simulation info
-    Vec_PtrCleanSimInfo( p->vDivCexes, 0, p->nDivWords ); 
-    pData = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
-    memset( pData, 0xFF, sizeof(unsigned) * p->nDivWords );
+    Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords ); 
     p->nCexes = 0;
-
     if ( fVeryVerbose )
     {
         printf( "\n" );
@@ -143,7 +168,8 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
         if ( fVeryVerbose )
         printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin );
         p->nNodesResub++;
-//        p->nNodesGained += Abc_NodeMffcLabel(pNode);
+        if ( fSkipUpdate )
+            return 1;
 clk = clock();
         // derive the function
         pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
@@ -156,11 +182,6 @@ p->timeInt += clock() - clk;
     if ( fOnlyRemove )
         return 0;
 
-    // shift variables by 1
-    for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- )
-        p->vFanins->pArray[i] = p->vFanins->pArray[i-1];
-    p->vFanins->nSize++;
-
     if ( fVeryVerbose )
     {
         for ( i = 0; i < 8; i++ )
@@ -180,37 +201,52 @@ p->timeInt += clock() - clk;
         if ( fVeryVerbose )
         {
             printf( "%3d: %2d ", p->nCexes, iVar );
-            pData = Vec_PtrEntry( p->vDivCexes, p->nCexes-1 );
-//            Extra_PrintBinary( stdout, pData, Vec_PtrSize(p->vDivs) );
             for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
-                printf( "%d", Aig_InfoHasBit(pData, i) );
+            {
+                pData = Vec_PtrEntry( p->vDivCexes, i );
+                printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) );
+            }
             printf( "\n" );
         }
 
         // find the next divisor to try
-        pData = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
+        nWords = Aig_BitWordNum(p->nCexes);
+        assert( nWords <= p->nDivWords );
         for ( iVar = 0; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
-            if ( Aig_InfoHasBit( pData, iVar ) )
+        {
+            pData  = Vec_PtrEntry( p->vDivCexes, iVar );
+            for ( w = 0; w < nWords; w++ )
+                if ( pData[w] != ~0 )
+                    break;
+            if ( w == nWords )
                 break;
+        }
         if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
             return 0;
+
         pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
         if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 ) )
         {
             if ( fVeryVerbose )
             printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar );
             p->nNodesResub++;
-//            p->nNodesGained += Abc_NodeMffcLabel(pNode);
+            if ( fSkipUpdate )
+                return 1;
 clk = clock();
             // derive the function
             pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 );
-            // update the network
-//            Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) );
+            // shift fanins by 1
+            for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- )
+                p->vFanins->pArray[i] = p->vFanins->pArray[i-1];
+            p->vFanins->nSize++;
             Vec_PtrWriteEntry( p->vFanins, 0, Vec_PtrEntry(p->vDivs, iVar) );
+            // update the network
             Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
 p->timeInt += clock() - clk;
             return 1;
         }
+        if ( p->nCexes >= p->pPars->nDivMax )
+            break;
     }
     return 0;
 }
@@ -226,16 +262,155 @@ p->timeInt += clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode )
+int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int iFanin2 )
 {
+    int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
+    unsigned * pData, * pData2;
+    int pCands[MFS_FANIN_MAX];
+    int iVar, iVar2, i, w, nCands, clk, nWords, fBreak;
     Abc_Obj_t * pFanin;
-    int i;
+    Hop_Obj_t * pFunc;
+    assert( iFanin >= 0 );
+    assert( iFanin2 >= 0 || iFanin2 == -1 );
+
+    // clean simulation info
+    Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords ); 
+    p->nCexes = 0;
+    if ( fVeryVerbose )
+    {
+        printf( "\n" );
+        printf( "Node %5d : Level = %2d. Divs = %3d.  Fanins = %d/%d (out of %d). MFFC = %d\n", 
+            pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode), 
+            iFanin, iFanin2, Abc_ObjFaninNum(pNode), 
+            Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 );
+    }
+
+    // try fanins without the critical fanin
+    nCands = 0;
+    Vec_PtrClear( p->vFanins );
     Abc_ObjForEachFanin( pNode, pFanin, i )
-        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
+    {
+        if ( i == iFanin || i == iFanin2 )
+            continue;
+        Vec_PtrPush( p->vFanins, pFanin );
+        iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
+        pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
+    }
+    if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands ) )
+    {
+        if ( fVeryVerbose )
+        printf( "Node %d: Fanins %d/%d can be removed.\n", pNode->Id, iFanin, iFanin2 );
+        p->nNodesResub++;
+clk = clock();
+        // derive the function
+        pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
+        // update the network
+        Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
+p->timeInt += clock() - clk;
+        return 1;
+    }
+
+    if ( fVeryVerbose )
+    {
+        for ( i = 0; i < 11; i++ )
+            printf( " " );
+        for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ )
+            printf( "%d", i % 10 );
+        for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
+            if ( i == iFanin || i == iFanin2 )
+                printf( "*" );
+            else
+                printf( "%c", 'a' + i );
+        printf( "\n" );
+    }
+    iVar = iVar2 = -1;
+    while ( 1 )
+    {
+        if ( fVeryVerbose )
         {
-            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0 ) )
-                return 1;
+            printf( "%3d: %2d %2d ", p->nCexes, iVar, iVar2 );
+            for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
+            {
+                pData = Vec_PtrEntry( p->vDivCexes, i );
+                printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) );
+            }
+            printf( "\n" );
+        }
+
+        // find the next divisor to try
+        nWords = Aig_BitWordNum(p->nCexes);
+        assert( nWords <= p->nDivWords );
+        fBreak = 0;
+        for ( iVar = 1; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
+        {
+            pData  = Vec_PtrEntry( p->vDivCexes, iVar );
+            for ( iVar2 = 0; iVar2 < iVar; iVar2++ )
+            {
+                pData2 = Vec_PtrEntry( p->vDivCexes, iVar2 );
+                for ( w = 0; w < nWords; w++ )
+                    if ( (pData[w] | pData2[w]) != ~0 )
+                        break;
+                if ( w == nWords )
+                {
+                    fBreak = 1;
+                    break;
+                }
+            }
+            if ( fBreak )
+                break;
+        }
+        if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
+            return 0;
+
+        pCands[nCands]   = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 );
+        pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
+        if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 ) )
+        {
+            if ( fVeryVerbose )
+            printf( "Node %d: Fanins %d/%d can be replaced by divisors %d/%d.\n", pNode->Id, iFanin, iFanin2, iVar, iVar2 );
+            p->nNodesResub++;
+clk = clock();
+            // derive the function
+            pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+2 );
+            // shift fanins by 1
+            for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- )
+                p->vFanins->pArray[i] = p->vFanins->pArray[i-1];
+            p->vFanins->nSize++;
+            // shift fanins by 1
+            for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- )
+                p->vFanins->pArray[i] = p->vFanins->pArray[i-1];
+            p->vFanins->nSize++;
+            Vec_PtrWriteEntry( p->vFanins, 0, Vec_PtrEntry(p->vDivs, iVar2) );
+            Vec_PtrWriteEntry( p->vFanins, 1, Vec_PtrEntry(p->vDivs, iVar) );
+            // update the network
+            Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
+p->timeInt += clock() - clk;
+            return 1;
         }
+        if ( p->nCexes >= p->pPars->nDivMax )
+            break;
+    }
+    return 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluates the possibility of replacing given edge by another edge.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 1 );
     return 0;
 }
 
@@ -250,25 +425,81 @@ int Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMfsResubEdge( Mfs_Man_t * p, Abc_Obj_t * pNode )
+int Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
 {
     Abc_Obj_t * pFanin;
     int i;
+    // try replacing area critical fanins
     Abc_ObjForEachFanin( pNode, pFanin, i )
         if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
         {
-            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0 ) )
+            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
                 return 1;
         }
+    // try removing redundant edges
+    if ( !p->pPars->fArea )
+    {
+        Abc_ObjForEachFanin( pNode, pFanin, i )
+            if ( Abc_ObjIsCi(pFanin) || Abc_ObjFanoutNum(pFanin) != 1 )
+            {
+                if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
+                    return 1;
+            }
+    }
+    if ( Abc_ObjFaninNum(pNode) == p->nFaninMax )
+        return 0;
+    // try replacing area critical fanins while adding two new fanins
     Abc_ObjForEachFanin( pNode, pFanin, i )
-        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) != 1 )
+        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
         {
-            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1 ) )
+            if ( Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
                 return 1;
         }
     return 0;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs resubstitution for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin, * pFanin2;
+    int i, k;
+/*
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
+        {
+            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
+                return 1;
+        }
+*/
+    if ( Abc_ObjFaninNum(pNode) < 2 )
+        return 0;
+    // try replacing one area critical fanin and one other fanin while adding two new fanins
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+    {
+        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
+        {
+            // consider second fanin to remove at the same time
+            Abc_ObjForEachFanin( pNode, pFanin2, k )
+            {
+                if ( i != k && Abc_NtkMfsSolveSatResub2( p, pNode, i, k ) )
+                    return 1;
+            }
+        }
+    }
+    return 0;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////