Merged alanmi/abc into default

15 files changed, 817 insertions, 294 deletions

diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index f01ef07a..dd3a75b7 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -1077,6 +1077,7 @@ void Abc_NtkLogicMakeSimpleCosTest( Abc_Ntk_t * pNtk, int fDuplicate )
 ***********************************************************************/
 int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, int fDuplicate )
 {
+    int fAddBuffers = 1;
     Vec_Ptr_t * vDrivers, * vCoTerms;
     Abc_Obj_t * pNode, * pDriver, * pDriverNew, * pFanin;
     int i, k, LevelMax, nTotal = 0;
@@ -1191,6 +1192,12 @@ int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, int fDuplicate )
     // collect COs that needs fixing by adding buffers or duplicating
     vCoTerms = Vec_PtrAlloc( 100 );
     Abc_NtkIncrementTravId( pNtk );
+    
+    // The following cases should be addressed only if the network is written 
+    // into a BLIF file. Otherwise, it is possible to skip them:
+    // (1) if a CO points to a CI with a different name
+    // (2) if an internal node drives more than one CO
+    if ( fAddBuffers )
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
         // if the driver is a CI and has different name, this is an error
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index dabeb982..806a5de7 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -481,6 +481,8 @@ static int Abc_CommandAbc9Fadds              ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9ATree              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Polyn              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Acec               ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Anorm              ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Decla              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Esop               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Exorcism           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Mfs                ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1124,6 +1126,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&atree",        Abc_CommandAbc9ATree,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&polyn",        Abc_CommandAbc9Polyn,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&acec",         Abc_CommandAbc9Acec,         0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&anorm",        Abc_CommandAbc9Anorm,        0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&decla",        Abc_CommandAbc9Decla,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&esop",         Abc_CommandAbc9Esop,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&exorcism",     Abc_CommandAbc9Exorcism,     0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&mfs",          Abc_CommandAbc9Mfs,          0 );
@@ -19532,7 +19536,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( Abc_NtkIsComb(pNtk) )
     {
-        Abc_Print( -1, "The network is combinational (run \"fraig\" or \"fraig_sweep\").\n" );
+        Abc_Print( 0, "The network is combinational (run \"fraig\" or \"fraig_sweep\").\n" );
         return 0;
     }
 
@@ -28592,15 +28596,21 @@ usage:
 int Abc_CommandAbc9Show( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Vec_Int_t * vBold = NULL;
-    int c, fAdders = 0;
+    int c, fAdders = 0, fFadds = 0, fPath = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "afph" ) ) != EOF )
     {
         switch ( c )
         {
         case 'a':
             fAdders ^= 1;
             break;
+        case 'f':
+            fFadds ^= 1;
+            break;
+        case 'p':
+            fPath ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -28623,14 +28633,16 @@ int Abc_CommandAbc9Show( Abc_Frame_t * pAbc, int argc, char ** argv )
         Gia_ManForEachLut( pAbc->pGia, c )
             Vec_IntPush( vBold, c );
     }
-    Gia_ManShow( pAbc->pGia, vBold, fAdders );
+    Gia_ManShow( pAbc->pGia, vBold, fAdders, fFadds, fPath );
     Vec_IntFreeP( &vBold );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &show [-ah]\n" );
+    Abc_Print( -2, "usage: &show [-afph]\n" );
     Abc_Print( -2, "\t        shows the current GIA using GSView\n" );
     Abc_Print( -2, "\t-a    : toggle visualazing adders [default = %s]\n", fAdders? "yes": "no" );
+    Abc_Print( -2, "\t-f    : toggle showing only full-adders with \"-a\" [default = %s]\n", fFadds? "yes": "no" );
+    Abc_Print( -2, "\t-p    : toggle showing the critical path of a LUT mapping [default = %s]\n", fPath? "yes": "no" );
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -31954,7 +31966,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( Gia_ManRegNum(pAbc->pGia) == 0 )
     {
-        Abc_Print( -1, "The network is combinational.\n" );
+        Abc_Print( 0, "The network is combinational.\n" );
         return 0;
     }
     pTemp = Cec_ManLSCorrespondence( pAbc->pGia, pPars );
@@ -32915,8 +32927,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Cec_ParCec_t ParsCec, * pPars = &ParsCec;
     FILE * pFile;
-    Gia_Man_t * pSecond, * pMiter;
-    char * FileName, * pTemp;
+    Gia_Man_t * pGias[2] = {NULL, NULL}, * pMiter;
     char ** pArgvNew;
     int c, nArgcNew, fMiter = 0, fDualOutput = 0, fDumpMiter = 0;
     Cec_ManCecSetDefaultParams( pPars );
@@ -32971,13 +32982,15 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
-    if ( pAbc->pGia == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9Cec(): There is no AIG.\n" );
-        return 1;
-    }
+    pArgvNew = argv + globalUtilOptind;
+    nArgcNew = argc - globalUtilOptind;
     if ( fMiter )
     {
+        if ( pAbc->pGia == NULL || nArgcNew != 0 )
+        {
+            Abc_Print( -1, "Abc_CommandAbc9Cec(): A miter cannot be given as an argument of command &cec and should be entered using &r.\n" );
+            return 1;
+        }
         if ( fDualOutput )
         {
             if ( Gia_ManPoNum(pAbc->pGia) & 1 )
@@ -32986,14 +32999,14 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
                 return 1;
             }
             if ( !pPars->fSilent )
-            Abc_Print( 1, "Assuming the current network is a double-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit );
+            Abc_Print( 1, "Assuming the current network is a double-output miter.\n" );
             pAbc->Status = Cec_ManVerify( pAbc->pGia, pPars );
         }
         else
         {
             Gia_Man_t * pTemp;
             if ( !pPars->fSilent )
-            Abc_Print( 1, "Assuming the current network is a single-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit );
+            Abc_Print( 1, "Assuming the current network is a single-output miter.\n" );
             pTemp = Gia_ManDemiterToDual( pAbc->pGia );
             pAbc->Status = Cec_ManVerify( pTemp, pPars );
             ABC_SWAP( Abc_Cex_t *, pAbc->pGia->pCexComb, pTemp->pCexComb );
@@ -33002,41 +33015,81 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
         return 0;
     }
-
-    pArgvNew = argv + globalUtilOptind;
-    nArgcNew = argc - globalUtilOptind;
-    if ( nArgcNew != 1 )
+    if ( nArgcNew > 2 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Cec(): Wrong number of command-line arguments.\n" );
+        return 1;
+    }
+    if ( nArgcNew == 2 )
     {
-        if ( pAbc->pGia->pSpec == NULL )
+        char * pFileNames[2] = { pArgvNew[0], pArgvNew[1] }, * pTemp;
+        int n;
+        for ( n = 0; n < 2; n++ )
         {
-            Abc_Print( -1, "File name is not given on the command line.\n" );
-            return 1;
+            // fix the wrong symbol
+            for ( pTemp = pFileNames[n]; *pTemp; pTemp++ )
+                if ( *pTemp == '>' )
+                    *pTemp = '\\';
+            if ( (pFile = fopen( pFileNames[n], "r" )) == NULL )
+            {
+                Abc_Print( -1, "Cannot open input file \"%s\". ", pFileNames[n] );
+                if ( (pFileNames[n] = Extra_FileGetSimilarName( pFileNames[n], ".aig", NULL, NULL, NULL, NULL )) )
+                    Abc_Print( 1, "Did you mean \"%s\"?", pFileNames[n] );
+                Abc_Print( 1, "\n" );
+                return 1;
+            }
+            fclose( pFile );
+            pGias[n] = Gia_AigerRead( pFileNames[n], 0, 0, 0 );
+            if ( pGias[n] == NULL )
+            {
+                Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", pFileNames[n] );
+                return 0;
+            }
         }
-        FileName = pAbc->pGia->pSpec;
     }
     else
-        FileName = pArgvNew[0];
-    // fix the wrong symbol
-    for ( pTemp = FileName; *pTemp; pTemp++ )
-        if ( *pTemp == '>' )
-            *pTemp = '\\';
-    if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
-        Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
-        if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", NULL, NULL, NULL, NULL )) )
-            Abc_Print( 1, "Did you mean \"%s\"?", FileName );
-        Abc_Print( 1, "\n" );
-        return 1;
-    }
-    fclose( pFile );
-    pSecond = Gia_AigerRead( FileName, 0, 0, 0 );
-    if ( pSecond == NULL )
-    {
-        Abc_Print( -1, "Reading AIGER has failed.\n" );
-        return 0;
+        char * FileName, * pTemp;
+        if ( pAbc->pGia == NULL )
+        {
+            Abc_Print( -1, "Abc_CommandAbc9Cec(): There is no current AIG.\n" );
+            return 1;
+        }
+        pGias[0] = pAbc->pGia;
+        if ( nArgcNew == 1 )
+            FileName = pArgvNew[0];
+        else
+        {
+            assert( nArgcNew == 0 );
+            if ( pAbc->pGia->pSpec == NULL )
+            {
+                Abc_Print( -1, "File name is not given on the command line.\n" );
+                return 1;
+            }
+            FileName = pAbc->pGia->pSpec;
+        }
+        // fix the wrong symbol
+        for ( pTemp = FileName; *pTemp; pTemp++ )
+            if ( *pTemp == '>' )
+                *pTemp = '\\';
+        if ( (pFile = fopen( FileName, "r" )) == NULL )
+        {
+            Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
+            if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", NULL, NULL, NULL, NULL )) )
+                Abc_Print( 1, "Did you mean \"%s\"?", FileName );
+            Abc_Print( 1, "\n" );
+            return 1;
+        }
+        fclose( pFile );
+        pGias[1] = Gia_AigerRead( FileName, 0, 0, 0 );
+        if ( pGias[1] == NULL )
+        {
+            Abc_Print( -1, "Reading AIGER has failed.\n" );
+            return 0;
+        }
     }
     // compute the miter
-    pMiter = Gia_ManMiter( pAbc->pGia, pSecond, 0, 1, 0, 0, pPars->fVerbose );
+    pMiter = Gia_ManMiter( pGias[0], pGias[1], 0, 1, 0, 0, pPars->fVerbose );
     if ( pMiter )
     {
         if ( fDumpMiter )
@@ -33045,10 +33098,12 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
             Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0 );
         }
         pAbc->Status = Cec_ManVerify( pMiter, pPars );
-        Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
+        Abc_FrameReplaceCex( pAbc, &pGias[0]->pCexComb );
         Gia_ManStop( pMiter );
     }
-    Gia_ManStop( pSecond );
+    if ( pGias[0] != pAbc->pGia )
+        Gia_ManStop( pGias[0] );
+    Gia_ManStop( pGias[1] );
     return 0;
 
 usage:
@@ -36166,7 +36221,7 @@ int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     Abc_Print( -2, "usage: &satlut [-NICDQ num] [-drwvh]\n" );
-    Abc_Print( -2, "\t           performs SAT-based remapping of the 4-LUT network\n" );
+    Abc_Print( -2, "\t           performs SAT-based remapping of the LUT-mapped network\n" );
     Abc_Print( -2, "\t-N num   : the limit on AIG nodes in the window (num <= 128) [default = %d]\n", nNumber );
     Abc_Print( -2, "\t-I num   : the limit on the number of improved windows [default = %d]\n", nImproves );
     Abc_Print( -2, "\t-C num   : the limit on the number of conflicts [default = %d]\n", nBTLimit );
@@ -40528,14 +40583,12 @@ usage:
 int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pFile;
-    Cec_ParCec_t ParsCec, * pPars = &ParsCec;
-    Gia_Man_t * pSecond;
-    char * FileName, * pTemp;
+    Acec_ParCec_t ParsCec, * pPars = &ParsCec;
     char ** pArgvNew;
-    int c, nArgcNew, fMiter = 0, fDualOutput = 0, fTwoOutput = 0;
-    Cec_ManCecSetDefaultParams( pPars );
+    int c, nArgcNew;
+    Acec_ManCecSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdtvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CTmdtbvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -40561,17 +40614,17 @@ int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->TimeLimit < 0 )
                 goto usage;
             break;
-        case 'n':
-            pPars->fNaive ^= 1;
-            break;
         case 'm':
-            fMiter ^= 1;
+            pPars->fMiter ^= 1;
             break;
         case 'd':
-            fDualOutput ^= 1;
+            pPars->fDualOutput ^= 1;
             break;
         case 't':
-            fTwoOutput ^= 1;
+            pPars->fTwoOutput ^= 1;
+            break;
+        case 'b':
+            pPars->fBooth ^= 1;
             break;
         case 'v':
             pPars->fVerbose ^= 1;
@@ -40582,15 +40635,20 @@ int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
-    if ( fMiter )
+    if ( pPars->fMiter )
     {
         Gia_Man_t * pGia0, * pGia1, * pDual;
+        if ( argc != globalUtilOptind )
+        {
+            Abc_Print( -1, "Abc_CommandAbc9Acec(): If the input is a miter, it cannot be given on the command line.\n" );
+            return 1;
+        }
         if ( pAbc->pGia == NULL )
         {
             Abc_Print( -1, "Abc_CommandAbc9Acec(): There is no AIG.\n" );
             return 1;
         }
-        if ( fDualOutput )
+        if ( pPars->fDualOutput )
         {
             if ( Gia_ManPoNum(pAbc->pGia) & 1 )
             {
@@ -40600,28 +40658,28 @@ int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( !pPars->fSilent )
             Abc_Print( 1, "Assuming the current network is a double-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit );
             Gia_ManDemiterDual( pAbc->pGia, &pGia0, &pGia1 );
-            pAbc->Status = Gia_PolynCec( pGia0, pGia1, pPars );
+            pAbc->Status = Acec_Solve( pGia0, pGia1, pPars );
         }
-        else if ( fTwoOutput )
+        else if ( pPars->fTwoOutput )
         {
             if ( Gia_ManPoNum(pAbc->pGia) & 1 )
             {
-                Abc_Print( -1, "The dual-output miter should have an even number of outputs.\n" );
+                Abc_Print( -1, "The two-output miter should have an even number of outputs.\n" );
                 return 1;
             }
             if ( !pPars->fSilent )
             Abc_Print( 1, "Assuming the current network is a two-word miter. (Conflict limit = %d.)\n", pPars->nBTLimit );
             Gia_ManDemiterTwoWords( pAbc->pGia, &pGia0, &pGia1 );
-            pAbc->Status = Gia_PolynCec( pGia0, pGia1, pPars );
+            pAbc->Status = Acec_Solve( pGia0, pGia1, pPars );
         }
-        else
+        else // regular single- or multi-output miter
         {
             if ( !pPars->fSilent )
-            Abc_Print( 1, "Assuming the current network is a single-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit );
+            Abc_Print( 1, "Assuming the current network is a regular single- or multi-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit );
             pDual = Gia_ManDemiterToDual( pAbc->pGia );
             Gia_ManDemiterDual( pDual, &pGia0, &pGia1 );
             Gia_ManStop( pDual );
-            pAbc->Status = Gia_PolynCec( pGia0, pGia1, pPars );
+            pAbc->Status = Acec_Solve( pGia0, pGia1, pPars );
         }
         Abc_FrameReplaceCex( pAbc, &pGia0->pCexComb );
         Gia_ManStop( pGia0 );
@@ -40631,52 +40689,97 @@ int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     pArgvNew = argv + globalUtilOptind;
     nArgcNew = argc - globalUtilOptind;
-    if ( nArgcNew != 1 )
+    if ( nArgcNew == 0 || nArgcNew == 1 )
     {
-        if ( pAbc->pGia->pSpec == NULL )
+        Gia_Man_t * pSecond;
+        char * pTemp, * FileName = NULL;
+        if ( nArgcNew == 0 )
         {
-            Abc_Print( -1, "File name is not given on the command line.\n" );
-            return 1;
+            FileName = pAbc->pGia->pSpec;
+            if ( FileName == NULL )
+            {
+                Abc_Print( -1, "File name is not given on the command line.\n" );
+                return 1;
+            }
         }
-        FileName = pAbc->pGia->pSpec;
+        else // if ( nArgcNew == 1 )
+        {
+            FileName = pArgvNew[0];
+            // fix the wrong symbol
+            for ( pTemp = FileName; *pTemp; pTemp++ )
+                if ( *pTemp == '>' )
+                    *pTemp = '\\';
+            if ( (pFile = fopen( FileName, "r" )) == NULL )
+            {
+                Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
+                if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", NULL, NULL, NULL, NULL )) )
+                    Abc_Print( 1, "Did you mean \"%s\"?", FileName );
+                Abc_Print( 1, "\n" );
+                return 1;
+            }
+            fclose( pFile );
+        }
+        pSecond = Gia_AigerRead( FileName, 0, 0, 0 );
+        if ( pSecond == NULL )
+        {
+            Abc_Print( -1, "Reading AIGER has failed.\n" );
+            return 0;
+        }
+        pAbc->Status = Acec_Solve( pAbc->pGia, pSecond, pPars );
+        Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
+        Gia_ManStop( pSecond );
     }
-    else
-        FileName = pArgvNew[0];
-    // fix the wrong symbol
-    for ( pTemp = FileName; *pTemp; pTemp++ )
-        if ( *pTemp == '>' )
-            *pTemp = '\\';
-    if ( (pFile = fopen( FileName, "r" )) == NULL )
+    else if ( nArgcNew == 2 )
     {
-        Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
-        if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", NULL, NULL, NULL, NULL )) )
-            Abc_Print( 1, "Did you mean \"%s\"?", FileName );
-        Abc_Print( 1, "\n" );
-        return 1;
+        Gia_Man_t * pGias[2] = {NULL};  int i;
+        char * pTemp, * FileName[2] = { pArgvNew[0], pArgvNew[1] };
+        for ( i = 0; i < 2; i++ )
+        {
+            // fix the wrong symbol
+            for ( pTemp = FileName[i]; *pTemp; pTemp++ )
+                if ( *pTemp == '>' )
+                    *pTemp = '\\';
+            if ( (pFile = fopen( FileName[i], "r" )) == NULL )
+            {
+                Abc_Print( -1, "Cannot open input file \"%s\". ", FileName[i] );
+                if ( (FileName[i] = Extra_FileGetSimilarName( FileName[i], ".aig", NULL, NULL, NULL, NULL )) )
+                    Abc_Print( 1, "Did you mean \"%s\"?", FileName[i] );
+                Abc_Print( 1, "\n" );
+                return 1;
+            }
+            fclose( pFile );
+            pGias[i] = Gia_AigerRead( FileName[i], 0, 0, 0 );
+            if ( pGias[i] == NULL )
+            {
+                Abc_Print( -1, "Reading AIGER has failed.\n" );
+                return 0;
+            }
+        }
+        pAbc->Status = Acec_Solve( pGias[0], pGias[1], pPars );
+        Abc_FrameReplaceCex( pAbc, &pGias[0]->pCexComb );
+        Gia_ManStop( pGias[0] );
+        Gia_ManStop( pGias[1] );
     }
-    fclose( pFile );
-    pSecond = Gia_AigerRead( FileName, 0, 0, 0 );
-    if ( pSecond == NULL )
+    else
     {
-        Abc_Print( -1, "Reading AIGER has failed.\n" );
-        return 0;
+        Abc_Print( -1, "Too many command-line arguments.\n" );
+        return 1;
     }
-    pAbc->Status = Gia_PolynCec( pAbc->pGia, pSecond, pPars );
-    Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
-    Gia_ManStop( pSecond );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &acec [-CT num] [-nmdtvh]\n" );
+    Abc_Print( -2, "usage: &acec [-CT num] [-mdtbvh] <file1> <file2>\n" );
     Abc_Print( -2, "\t         combinational equivalence checking for arithmetic circuits\n" );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
-    Abc_Print( -2, "\t-n     : toggle using naive SAT-based checking [default = %s]\n", pPars->fNaive? "yes":"no");
-    Abc_Print( -2, "\t-m     : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits");
-    Abc_Print( -2, "\t-d     : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no");
-    Abc_Print( -2, "\t-t     : toggle using two-word miter [default = %s]\n", fTwoOutput? "yes":"no");
+    Abc_Print( -2, "\t-m     : toggle miter vs. two circuits [default = %s]\n", pPars->fMiter? "miter":"two circuits");
+    Abc_Print( -2, "\t-d     : toggle using dual output miter [default = %s]\n", pPars->fDualOutput? "yes":"no");
+    Abc_Print( -2, "\t-t     : toggle using two-word miter [default = %s]\n", pPars->fTwoOutput? "yes":"no");
+    Abc_Print( -2, "\t-b     : toggle working with Booth multipliers [default = %s]\n", pPars->fBooth? "yes":"no");
     Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no");
     Abc_Print( -2, "\t-h     : print the command usage\n");
+    Abc_Print( -2, "\tfile1  : (optional) the file with the first network\n");
+    Abc_Print( -2, "\tfile2  : (optional) the file with the second network\n");
     return 1;
 }
 
@@ -40691,6 +40794,107 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Anorm( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pTemp;
+    int c, fBooth = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "bvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'b':
+            fBooth ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Anorm(): There is no AIG.\n" );
+        return 0;
+    }
+    pTemp = Acec_Normalize( pAbc->pGia, fBooth, fVerbose );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &anorm [-bvh]\n" );
+    Abc_Print( -2, "\t         normalize adder trees in the current AIG\n" );
+    Abc_Print( -2, "\t-b     : toggles working with Booth multipliers [default = %s]\n",  fBooth? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n",  fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Decla( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pTemp;
+    int c, fBooth = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "bvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'b':
+            fBooth ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Decla(): There is no AIG.\n" );
+        return 0;
+    }
+    pTemp = Acec_ManDecla( pAbc->pGia, fBooth, fVerbose );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &decla [-bvh]\n" );
+    Abc_Print( -2, "\t         removes carry look ahead adders\n" );
+    Abc_Print( -2, "\t-b     : toggles working with Booth multipliers [default = %s]\n",  fBooth? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n",  fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Esop( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose, Vec_Wec_t ** pvRes );
@@ -41006,7 +41210,7 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
     Sbd_Par_t Pars, * pPars = &Pars;
     Sbd_ParSetDefault( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KWFMCacvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KSNPWFMCmcdpvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -41021,6 +41225,39 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nLutSize < 0 )
                 goto usage;
             break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nLutNum = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nLutNum < 0 )
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nCutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nCutSize < 0 )
+                goto usage;
+            break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nCutNum = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nCutNum < 0 )
+                goto usage;
+            break;
         case 'W':
             if ( globalUtilOptind >= argc )
             {
@@ -41065,11 +41302,17 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nBTLimit < 0 )
                 goto usage;
             break;
-        case 'a':
-            pPars->fArea ^= 1;
+        case 'm':
+            pPars->fMapping ^= 1;
             break;
         case 'c':
-            pPars->fCover ^= 1;
+            pPars->fMoreCuts ^= 1;
+            break;
+        case 'd':
+            pPars->fFindDivs ^= 1;
+            break;
+        case 'p':
+            pPars->fUsePath ^= 1;
             break;
         case 'v':
             pPars->fVerbose ^= 1;
@@ -41085,33 +41328,35 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pGia == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9Mfs(): There is no AIG.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9Mfsd(): There is no AIG.\n" );
         return 0;
     }
     if ( Gia_ManBufNum(pAbc->pGia) )
     {
-        Abc_Print( -1, "Abc_CommandAbc9Mfs(): This command does not work with barrier buffers.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9Mfsd(): This command does not work with barrier buffers.\n" );
         return 1;
     }
     if ( Gia_ManHasMapping(pAbc->pGia) )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9Mfs(): The current AIG has mapping (run &st to unmap).\n" );
-        return 0;
-    }
+        Abc_Print( 1, "The current AIG has mapping, which can be used to determine critical path if \"-p\" is selected.\n" );
     pTemp = Sbd_NtkPerform( pAbc->pGia, pPars );
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &mfsd [-KWFMC <num>] [-acvwh]\n" );
+    Abc_Print( -2, "usage: &mfsd [-KSNPWFMC <num>] [-mcdpvwh]\n" );
     Abc_Print( -2, "\t           performs SAT-based delay-oriented AIG optimization\n" );
     Abc_Print( -2, "\t-K <num> : the LUT size for delay minimization (2 <= num <= 6) [default = %d]\n",         pPars->nLutSize );
+    Abc_Print( -2, "\t-S <num> : the LUT structure size (1 <= num <= 2) [default = %d]\n",                      pPars->nLutNum );
+    Abc_Print( -2, "\t-N <num> : the cut size considered for optimization (2 <= num <= 10) [default = %d]\n",   pPars->nCutSize );
+    Abc_Print( -2, "\t-P <num> : the number of cuts computed at a node (1 <= num <= 500) [default = %d]\n",     pPars->nCutNum );
     Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n",             pPars->nTfoLevels );
     Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n",                pPars->nTfoFanMax );
     Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n",    pPars->nWinSizeMax );
     Abc_Print( -2, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n",   pPars->nBTLimit );
-    Abc_Print( -2, "\t-a       : toggle minimizing area or area+edges [default = %s]\n",                        pPars->fArea? "area": "area+edges" );
-    Abc_Print( -2, "\t-c       : toggle using complete slow covering procedure [default = %s]\n",               pPars->fCover? "yes": "no" );
+    Abc_Print( -2, "\t-m       : toggle generating delay-oriented mapping [default = %s]\n",                    pPars->fMapping? "yes": "no" );
+    Abc_Print( -2, "\t-c       : toggle using several cuts at each node [default = %s]\n",                      pPars->fMoreCuts? "yes": "no" );
+    Abc_Print( -2, "\t-d       : toggle additional search for good divisors [default = %s]\n",                  pPars->fFindDivs? "yes": "no" );
+    Abc_Print( -2, "\t-p       : toggle optimizing critical path only [default = %s]\n",                        pPars->fUsePath? "yes": "no" );
     Abc_Print( -2, "\t-v       : toggle printing optimization summary [default = %s]\n",                        pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w       : toggle printing detailed stats for each node [default = %s]\n",                pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n");
@@ -42541,8 +42786,6 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Jf_ManTestCnf( pAbc->pGia );
 //    Gia_ManCheckFalseTest( pAbc->pGia, nFrames );
 //    Gia_ParTest( pAbc->pGia, nWords, nProcs );
-//    Gia_PolynExplore( pAbc->pGia );
-//    Gia_ManTestSatEnum( pAbc->pGia );
 
 //    printf( "\nThis command is currently disabled.\n\n" );
     return 0;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 9f672485..147f7c2f 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1946,17 +1946,17 @@ finish:
     // report the miter
     if ( RetValue == 1 )
     {
-        Abc_Print( 1, "Networks are equivalent.   " );
+        Abc_Print( 1, "Networks are equivalent.  " );
 ABC_PRT( "Time", Abc_Clock() - clkTotal );
     }
     else if ( RetValue == 0 )
     {
-        Abc_Print( 1, "Networks are NOT EQUIVALENT.   " );
+        Abc_Print( 1, "Networks are NOT EQUIVALENT.  " );
 ABC_PRT( "Time", Abc_Clock() - clkTotal );
     }
     else
     {
-        Abc_Print( 1, "Networks are UNDECIDED.   " );
+        Abc_Print( 1, "Networks are UNDECIDED.  " );
 ABC_PRT( "Time", Abc_Clock() - clkTotal );
     }
     fflush( stdout );
@@ -3695,17 +3695,17 @@ int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nTimeOut, int nFramesMax, int nCo
     RetValue = Saig_ManInduction( pMan, nTimeOut, nFramesMax, nConfMax, fUnique, fUniqueAll, fGetCex, fVerbose, fVeryVerbose );
     if ( RetValue == 1 )
     {
-        Abc_Print( 1, "Networks are equivalent.   " );
+        Abc_Print( 1, "Networks are equivalent.  " );
 ABC_PRT( "Time", Abc_Clock() - clkTotal );
     }
     else if ( RetValue == 0 )
     {
-        Abc_Print( 1, "Networks are NOT EQUIVALENT.   " );
+        Abc_Print( 1, "Networks are NOT EQUIVALENT.  " );
 ABC_PRT( "Time", Abc_Clock() - clkTotal );
     }
     else
     {
-        Abc_Print( 1, "Networks are UNDECIDED.   " );
+        Abc_Print( 1, "Networks are UNDECIDED.  " );
 ABC_PRT( "Time", Abc_Clock() - clkTotal );
     }
     if ( fGetCex )
diff --git a/src/base/abci/abcDress3.c b/src/base/abci/abcDress3.c
index 33545f0a..ce0cb7f5 100644
--- a/src/base/abci/abcDress3.c
+++ b/src/base/abci/abcDress3.c
@@ -35,32 +35,6 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
-  Synopsis    [Compute equivalence classes of nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkComputeGiaEquivs( Gia_Man_t * pGia, int nConfs, int fVerbose )
-{
-    Gia_Man_t * pTemp;
-    Cec_ParFra_t ParsFra, * pPars = &ParsFra;
-    Cec_ManFraSetDefaultParams( pPars );
-    pPars->fUseOrigIds = 1;
-    pPars->fSatSweeping = 1;
-    pPars->nBTLimit = nConfs;
-    pPars->fVerbose = fVerbose;
-    pTemp = Cec_ManSatSweeping( pGia, pPars, 0 );
-    Gia_ManStop( pTemp );
-    pTemp = Gia_ManOrigIdsReduce( pGia, pGia->vIdsEquiv );
-    Gia_ManStop( pTemp );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Converts AIG from HOP to GIA.]
 
   Description []
@@ -315,13 +289,15 @@ void Abc_NtkDumpEquivFile( char * pFileName, Vec_Int_t * vClasses, Abc_Ntk_t * p
 void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, int fByName, int fVerbose )
 {
     //abctime clk = Abc_Clock();
+    Gia_Man_t * pTemp;
     Vec_Int_t * vClasses;
     // derive shared AIG for the two networks
     Gia_Man_t * pGia = Abc_NtkAigToGiaTwo( pNtks[0], pNtks[1], fByName );
     if ( fVerbose )
         printf( "Computing equivalences for networks \"%s\" and \"%s\" with conflict limit %d.\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]), nConfs );
     // compute equivalences in this AIG
-    Abc_NtkComputeGiaEquivs( pGia, nConfs, fVerbose );
+    pTemp = Gia_ManComputeGiaEquivs( pGia, nConfs, fVerbose );
+    Gia_ManStop( pTemp );
     //if ( fVerbose )
     //    Abc_PrintTime( 1, "Equivalence computation time", Abc_Clock() - clk );
     if ( fVerbose )
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c
index 757034cd..adb64d79 100644
--- a/src/base/abci/abcExact.c
+++ b/src/base/abci/abcExact.c
@@ -873,7 +873,7 @@ static void Ses_StoreRead( Ses_Store_t * pStore, const char * pFilename, int fSy
 
     fclose( pFile );
 
-    printf( "read %lu entries from file\n", nEntries );
+    printf( "read %lu entries from file\n", (long)nEntries );
 }
 
 // computes top decomposition of variables wrt. to AND and OR
diff --git a/src/base/abci/abcMfs.c b/src/base/abci/abcMfs.c
index e33d6c73..d44ca1a0 100644
--- a/src/base/abci/abcMfs.c
+++ b/src/base/abci/abcMfs.c
@@ -259,7 +259,7 @@ int Abc_NtkPerformMfs( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
     if ( nFaninMax > 6 )
     {
         Abc_Print( 1, "Currently \"mfs\" cannot process the network containing nodes with more than 6 fanins.\n" );
-        return 0;
+        return 1;
     }
     if ( !Abc_NtkHasSop(pNtk) )
         if ( !Abc_NtkToSop( pNtk, -1, ABC_INFINITY ) )
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 25d1d113..7199c529 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -122,6 +122,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
 ***********************************************************************/
 void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose )
 {
+    abctime clk = Abc_Clock();
     Prove_Params_t Params, * pParams = &Params;
 //    Fraig_Params_t Params;
 //    Fraig_Man_t * pMan;
@@ -170,18 +171,20 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
     RetValue = Abc_NtkMiterIsConstant( pMiter );
     if ( RetValue == 0 )
     {
-        printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
+        printf( "Networks are NOT EQUIVALENT after structural hashing.  " );
         // report the error
         pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
         Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
         ABC_FREE( pMiter->pModel );
         Abc_NtkDelete( pMiter );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
         return;
     }
     if ( RetValue == 1 )
     {
-        printf( "Networks are equivalent after structural hashing.\n" );
+        printf( "Networks are equivalent after structural hashing.  " );
         Abc_NtkDelete( pMiter );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
         return;
     }
 /*
@@ -220,18 +223,19 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
 //    pParams->fVerbose = 1;
     RetValue = Abc_NtkIvyProve( &pMiter, pParams );
     if ( RetValue == -1 )
-        printf( "Networks are undecided (resource limits is reached).\n" );
+        printf( "Networks are undecided (resource limits is reached).  " );
     else if ( RetValue == 0 )
     {
         int * pSimInfo = Abc_NtkVerifySimulatePattern( pMiter, pMiter->pModel );
         if ( pSimInfo[0] != 1 )
             printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
         else
-            printf( "Networks are NOT EQUIVALENT.\n" );
+            printf( "Networks are NOT EQUIVALENT.  " );
         ABC_FREE( pSimInfo );
     }
     else
-        printf( "Networks are equivalent.\n" );
+        printf( "Networks are equivalent.  " );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     if ( pMiter->pModel )
         Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
     Abc_NtkDelete( pMiter );
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 0b7c1788..ab037139 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -1147,26 +1147,7 @@ usage:
 
 #if defined(WIN32) && !defined(__cplusplus)
 #include <direct.h>
-
-// these structures are defined in <io.h> but are for some reason invisible
-typedef unsigned long _fsize_t; // Could be 64 bits for Win32
-
-struct _finddata_t {
-    unsigned    attrib;
-    time_t      time_create;    // -1 for FAT file systems
-    time_t      time_access;    // -1 for FAT file systems
-    time_t      time_write;
-    _fsize_t    size;
-    char        name[260];
-};
-
-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 );
-
+#include <io.h>
 
 /**Function*************************************************************
 
diff --git a/src/base/cmd/cmdLoad.c b/src/base/cmd/cmdLoad.c
index 7f7c1b60..accd9440 100644
--- a/src/base/cmd/cmdLoad.c
+++ b/src/base/cmd/cmdLoad.c
@@ -97,26 +97,7 @@ int CmdCommandLoad( Abc_Frame_t * pAbc, int argc, char ** argv )
 #if defined(WIN32) && !defined(__cplusplus)
 
 #include <direct.h>
-
-
-// these structures are defined in <io.h> but are for some reason invisible
-typedef unsigned long _fsize_t; // Could be 64 bits for Win32
-
-struct _finddata_t {
-    unsigned    attrib;
-    time_t      time_create;    // -1 for FAT file systems 
-    time_t      time_access;    // -1 for FAT file systems 
-    time_t      time_write;
-    _fsize_t    size;
-    char        name[260];
-};
-
-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 );
+#include <io.h>
 
 /**Function*************************************************************
 
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 05cb09c1..9647d020 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -95,8 +95,6 @@ void        Abc_FrameSetStatus( int Status )                 { ABC_FREE( s_Globa
 void        Abc_FrameSetManDsd( void * pMan )                { if (s_GlobalFrame->pManDsd  && s_GlobalFrame->pManDsd  != pMan) If_DsdManFree((If_DsdMan_t *)s_GlobalFrame->pManDsd,  0); s_GlobalFrame->pManDsd = pMan;  }
 void        Abc_FrameSetManDsd2( void * pMan )               { if (s_GlobalFrame->pManDsd2 && s_GlobalFrame->pManDsd2 != pMan) If_DsdManFree((If_DsdMan_t *)s_GlobalFrame->pManDsd2, 0); s_GlobalFrame->pManDsd2 = pMan; }
 void        Abc_FrameSetInv( Vec_Int_t * vInv )              { Vec_IntFreeP(&s_GlobalFrame->pAbcWlcInv); s_GlobalFrame->pAbcWlcInv = vInv; }
-void        Abc_FrameSetCnf( Vec_Int_t * vCnf )              { Vec_IntFreeP(&s_GlobalFrame->pAbcWlcCnf); s_GlobalFrame->pAbcWlcCnf = vCnf; }
-void        Abc_FrameSetStr( Vec_Str_t * vStr )              { Vec_StrFreeP(&s_GlobalFrame->pAbcWlcStr); s_GlobalFrame->pAbcWlcStr = vStr; }
 void        Abc_FrameSetJsonStrs( Abc_Nam_t * pStrs )        { Abc_NamDeref( s_GlobalFrame->pJsonStrs ); s_GlobalFrame->pJsonStrs = pStrs; }
 void        Abc_FrameSetJsonObjs( Vec_Wec_t * vObjs )        { Vec_WecFreeP(&s_GlobalFrame->vJsonObjs ); s_GlobalFrame->vJsonObjs = vObjs; }
 
@@ -227,8 +225,6 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
     ABC_FREE( p->pCex2 );
     ABC_FREE( p->pCex );
     Vec_IntFreeP( &p->pAbcWlcInv );
-    Vec_IntFreeP( &p->pAbcWlcCnf );
-    Vec_StrFreeP( &p->pAbcWlcStr );
     Abc_NamDeref( s_GlobalFrame->pJsonStrs );
     Vec_WecFreeP(&s_GlobalFrame->vJsonObjs );    
     ABC_FREE( p );
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index ff59b81a..278a9191 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -129,8 +129,6 @@ struct Abc_Frame_t_
     void *          pAbc85Delay;
     void *          pAbcWlc;
     Vec_Int_t *     pAbcWlcInv;
-    Vec_Int_t *     pAbcWlcCnf;
-    Vec_Str_t *     pAbcWlcStr;
     void *          pAbcBac;
     void *          pAbcCba;
     void *          pAbcPla;
diff --git a/src/base/main/mainReal.c b/src/base/main/mainReal.c
index ee43d38d..31bfef75 100644
--- a/src/base/main/mainReal.c
+++ b/src/base/main/mainReal.c
@@ -196,7 +196,7 @@ int Abc_RealMain( int argc, char * argv[] )
             case 't':
                 if ( TypeCheck( pAbc, globalUtilOptarg ) )
                 {
-                    if ( !strcmp(globalUtilOptarg, "none") == 0 )
+                    if ( (!strcmp(globalUtilOptarg, "none")) == 0 )
                     {
                         fInitRead = 1;
                         sprintf( sReadCmd, "read_%s", globalUtilOptarg );
@@ -211,7 +211,7 @@ int Abc_RealMain( int argc, char * argv[] )
             case 'T':
                 if ( TypeCheck( pAbc, globalUtilOptarg ) )
                 {
-                    if (!strcmp(globalUtilOptarg, "none") == 0)
+                    if ( (!strcmp(globalUtilOptarg, "none")) == 0)
                     {
                         fFinalWrite = 1;
                         sprintf( sWriteCmd, "write_%s", globalUtilOptarg);
diff --git a/src/base/wlc/wlcAbc.c b/src/base/wlc/wlcAbc.c
index 0bf27f7b..1a98fb71 100644
--- a/src/base/wlc/wlcAbc.c
+++ b/src/base/wlc/wlcAbc.c
@@ -42,7 +42,7 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
+void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vCounts, int fVerbose )
 {
     Wlc_Obj_t * pObj;
     int i, k, nNum, nRange, nBits = 0;
@@ -53,7 +53,7 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
         nRange = Wlc_ObjRange(pObj);
         for ( k = 0; k < nRange; k++ )
         {
-            nNum = Vec_IntEntry(vInv, nBits + k);
+            nNum = Vec_IntEntry(vCounts, nBits + k);
             if ( nNum )
                 break;
         }
@@ -65,7 +65,7 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
         printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
         for ( k = 0; k < nRange; k++ )
         {
-            nNum = Vec_IntEntry( vInv, nBits + k );
+            nNum = Vec_IntEntry( vCounts, nBits + k );
             if ( nNum == 0 )
                 continue;
             printf( "  [%d] -> %d", k, nNum );
@@ -73,8 +73,8 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
         printf( "\n");
         nBits += nRange;
     }
-    //printf( "%d %d\n", Vec_IntSize(vInv), nBits );
-    assert( Vec_IntSize(vInv) == nBits );
+    //printf( "%d %d\n", Vec_IntSize(vCounts), nBits );
+    assert( Vec_IntSize(vCounts) == nBits );
 }
 
 /**Function*************************************************************
@@ -88,8 +88,14 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose )
+Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv )
 {
+    extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv );
+    extern Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts );
+
+    Vec_Int_t * vCounts = Pdr_InvCounts( vInv );
+    Vec_Str_t * vSop = Pdr_InvPrintStr( vInv, vCounts );
+
     Wlc_Obj_t * pObj;
     int i, k, nNum, nRange, nBits = 0;
     Abc_Ntk_t * pMainNtk = NULL;
@@ -98,46 +104,69 @@ Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop,
     // start the network
     pMainNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
     // duplicate the name and the spec
-    pMainNtk->pName = Extra_UtilStrsav(pNtk->pName);
+    pMainNtk->pName = Extra_UtilStrsav(pNtk ? pNtk->pName : "inv");
     // create primary inputs
-    Wlc_NtkForEachCi( pNtk, pObj, i )
+    if ( pNtk == NULL )
     {
-        if ( pObj->Type != WLC_OBJ_FO )
-            continue;
-        nRange = Wlc_ObjRange(pObj);
-        for ( k = 0; k < nRange; k++ )
+        int Entry, nInputs = Abc_SopGetVarNum( Vec_StrArray(vSop) );
+        Vec_IntForEachEntry( vCounts, Entry, i )
         {
-            nNum = Vec_IntEntry(vInv, nBits + k);
-            if ( nNum )
-                break;
+            if ( Entry == 0 )
+                continue;
+            pMainObj = Abc_NtkCreatePi( pMainNtk );
+            sprintf( Buffer, "pi%d", i );
+            Abc_ObjAssignName( pMainObj, Buffer, NULL );
         }
-        if ( k == nRange )
+        if ( Abc_NtkPiNum(pMainNtk) != nInputs )
         {
-            nBits += nRange;
-            continue;
+            printf( "Mismatch between number of inputs and the number of literals in the invariant.\n" );
+            Abc_NtkDelete( pMainNtk );
+            return NULL;
         }
-        //printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
-        for ( k = 0; k < nRange; k++ )
+    }
+    else
+    {
+        Wlc_NtkForEachCi( pNtk, pObj, i )
         {
-            nNum = Vec_IntEntry( vInv, nBits + k );
-            if ( nNum == 0 )
+            if ( pObj->Type != WLC_OBJ_FO )
                 continue;
-            //printf( "  [%d] -> %d", k, nNum );
-            pMainObj = Abc_NtkCreatePi( pMainNtk );
-            sprintf( Buffer, "%s[%d]", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k );
-            Abc_ObjAssignName( pMainObj, Buffer, NULL );
-
+            nRange = Wlc_ObjRange(pObj);
+            for ( k = 0; k < nRange; k++ )
+            {
+                nNum = Vec_IntEntry(vCounts, nBits + k);
+                if ( nNum )
+                    break;
+            }
+            if ( k == nRange )
+            {
+                nBits += nRange;
+                continue;
+            }
+            //printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
+            for ( k = 0; k < nRange; k++ )
+            {
+                nNum = Vec_IntEntry( vCounts, nBits + k );
+                if ( nNum == 0 )
+                    continue;
+                //printf( "  [%d] -> %d", k, nNum );
+                pMainObj = Abc_NtkCreatePi( pMainNtk );
+                sprintf( Buffer, "%s[%d]", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k );
+                Abc_ObjAssignName( pMainObj, Buffer, NULL );
+
+            }
+            //printf( "\n");
+            nBits += nRange;
         }
-        //printf( "\n");
-        nBits += nRange;
     }
-    //printf( "%d %d\n", Vec_IntSize(vInv), nBits );
-    assert( Vec_IntSize(vInv) == nBits );
+    //printf( "%d %d\n", Vec_IntSize(vCounts), nBits );
+    assert( pNtk == NULL || Vec_IntSize(vCounts) == nBits );
     // create node
     pMainObj = Abc_NtkCreateNode( pMainNtk );
     Abc_NtkForEachPi( pMainNtk, pMainTemp, i )
         Abc_ObjAddFanin( pMainObj, pMainTemp );
     pMainObj->pData = Abc_SopRegister( (Mem_Flex_t *)pMainNtk->pManFunc, Vec_StrArray(vSop) );
+    Vec_IntFree( vCounts );
+    Vec_StrFree( vSop );
     // create PO
     pMainTemp = Abc_NtkCreatePo( pMainNtk );
     Abc_ObjAddFanin( pMainTemp, pMainObj );
@@ -145,6 +174,66 @@ Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop,
     return pMainNtk;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Translate current network into an interpolant.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, int nRegs )
+{
+    Vec_Int_t * vRes = NULL;
+    if ( Abc_NtkPoNum(pNtk) != 1 )
+        printf( "The number of outputs is other than 1.\n" );
+    else if ( Abc_NtkNodeNum(pNtk) != 1 )
+        printf( "The number of internal nodes is other than 1.\n" );
+    else
+    {
+        Abc_Obj_t * pNode = Abc_ObjFanin0( Abc_NtkCo(pNtk, 0) );
+        char * pName, * pCube, * pSop = (char *)pNode->pData;
+        Vec_Int_t * vFanins = Vec_IntAlloc( Abc_ObjFaninNum(pNode) );
+        Abc_Obj_t * pFanin; int i, k, Value, nLits;
+        Abc_ObjForEachFanin( pNode, pFanin, i )
+        {
+            assert( Abc_ObjIsCi(pFanin) );
+            pName = Abc_ObjName(pFanin);
+            for ( k = (int)strlen(pName)-1; k >= 0; k-- )
+                if ( pName[k] < '0' || pName[k] > '9' )
+                    break;
+            if ( k == (int)strlen(pName)-1 )
+            {
+                printf( "Cannot read input name of fanin %d.\n", i );
+                Value = i;
+            }
+            else 
+                Value = atoi(pName + k + 1);
+            Vec_IntPush( vFanins, Value );
+        }
+        assert( Vec_IntSize(vFanins) == Abc_ObjFaninNum(pNode) );
+        vRes = Vec_IntAlloc( 1000 );
+        Vec_IntPush( vRes, Abc_SopGetCubeNum(pSop) );
+        Abc_SopForEachCube( pSop, Abc_ObjFaninNum(pNode), pCube )
+        {
+            nLits = 0;
+            Abc_CubeForEachVar( pCube, Value, k )
+                if ( Value != '-' )
+                    nLits++;
+            Vec_IntPush( vRes, nLits );
+            Abc_CubeForEachVar( pCube, Value, k )
+                if ( Value != '-' )
+                    Vec_IntPush( vRes, Abc_Var2Lit(Vec_IntEntry(vFanins, k), (int)Value == '0') );
+        }
+        Vec_IntPush( vRes, nRegs );
+        Vec_IntFree( vFanins );
+    }
+    return vRes;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index ec3b040d..b49c2dd7 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -643,6 +643,41 @@ void Wlc_IntInsert( Vec_Int_t * vProd, Vec_Int_t * vLevel, int Node, int Level )
     Vec_IntInsert( vProd,  i + 1, Node  );
     Vec_IntInsert( vLevel, i + 1, Level );
 }
+void Wlc_BlastPrintMatrix( Gia_Man_t * p, Vec_Wec_t * vProds )
+{
+    int fVerbose = 0;
+    Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
+    Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vLevel;  word Truth;
+    int i, k, iLit; 
+    Vec_WecForEachLevel( vProds, vLevel, i )
+        Vec_IntForEachEntry( vLevel, iLit, k )
+            if ( Gia_ObjIsAnd(Gia_ManObj(p, Abc_Lit2Var(iLit))) )
+                Vec_IntPushUnique( vSupp, Abc_Lit2Var(iLit) );
+    printf( "Booth partial products: %d pps, %d unique, %d nodes.\n", 
+        Vec_WecSizeSize(vProds), Vec_IntSize(vSupp), Gia_ManAndNum(p) );
+    Vec_IntPrint( vSupp );
+
+    if ( fVerbose )
+    Vec_WecForEachLevel( vProds, vLevel, i )
+        Vec_IntForEachEntry( vLevel, iLit, k )
+        {
+            printf( "Obj = %4d : ", Abc_Lit2Var(iLit) );
+            printf( "Compl = %d  ", Abc_LitIsCompl(iLit) );
+            printf( "Rank = %2d  ", i );
+            Truth = Gia_ObjComputeTruth6Cis( p, iLit, vSupp, vTemp );
+            Extra_PrintHex( stdout, (unsigned*)&Truth, Vec_IntSize(vSupp) );
+            if ( Vec_IntSize(vSupp) == 4 ) printf( "    " );
+            if ( Vec_IntSize(vSupp) == 3 ) printf( "      " );
+            if ( Vec_IntSize(vSupp) <= 2 ) printf( "       " );
+            printf( "  " );
+            Vec_IntPrint( vSupp );
+            if ( k == Vec_IntSize(vLevel)-1 )
+                printf( "\n" );
+        }
+    Vec_IntFree( vSupp );
+    Vec_WrdFree( vTemp );
+}
 void Wlc_BlastReduceMatrix( Gia_Man_t * pNew, Vec_Wec_t * vProds, Vec_Wec_t * vLevels, Vec_Int_t * vRes )
 {
     Vec_Int_t * vLevel, * vProd;
@@ -812,6 +847,7 @@ void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int
         Vec_WecPush( vLevels, k, 0 );
     }
     //Vec_WecPrint( vProds, 0 );
+    //Wlc_BlastPrintMatrix( pNew, vProds );
     //printf( "Cutoff ID for partial products = %d.\n", Gia_ManObjNum(pNew) );
     Wlc_BlastReduceMatrix( pNew, vProds, vLevels, vRes );
 
@@ -1509,7 +1545,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
         assert( Vec_PtrSize(pNew->vNamesOut) == Gia_ManCoNum(pNew) );
     }
 
-    pNew->pSpec = Abc_UtilStrsav( p->pSpec ? p->pSpec : p->pName );
+    //pNew->pSpec = Abc_UtilStrsav( p->pSpec ? p->pSpec : p->pName );
     // dump the miter parts
     if ( 0 )
     {
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index f3eb6dd7..93614938 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -32,18 +32,21 @@ static int  Abc_CommandReadWlc  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandWriteWlc ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandPs       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandBlast    ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int  Abc_CommandPsInv    ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int  Abc_CommandGetInv   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandProfile  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandTest     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
+static int  Abc_CommandInvPs    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandInvPrint ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandInvCheck ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandInvGet   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandInvPut   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandInvMin   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
 static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc )                       { return (Wlc_Ntk_t *)pAbc->pAbcWlc;                      }
 static inline void        Wlc_AbcFreeNtk( Abc_Frame_t * pAbc )                      { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(pAbc));  }
 static inline void        Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk )  { Wlc_AbcFreeNtk(pAbc); pAbc->pAbcWlc = pNtk;             }
 
 static inline Vec_Int_t * Wlc_AbcGetInv( Abc_Frame_t * pAbc )                       { return pAbc->pAbcWlcInv;                                }
-static inline Vec_Int_t * Wlc_AbcGetCnf( Abc_Frame_t * pAbc )                       { return pAbc->pAbcWlcCnf;                                }
-static inline Vec_Str_t * Wlc_AbcGetStr( Abc_Frame_t * pAbc )                       { return pAbc->pAbcWlcStr;                                }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -66,10 +69,15 @@ void Wlc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Word level", "%write",      Abc_CommandWriteWlc,  0 );
     Cmd_CommandAdd( pAbc, "Word level", "%ps",         Abc_CommandPs,        0 );
     Cmd_CommandAdd( pAbc, "Word level", "%blast",      Abc_CommandBlast,     0 );
-    Cmd_CommandAdd( pAbc, "Word level", "%psinv",      Abc_CommandPsInv,     0 );
-    Cmd_CommandAdd( pAbc, "Word level", "%getinv",     Abc_CommandGetInv,    0 );
     Cmd_CommandAdd( pAbc, "Word level", "%profile",    Abc_CommandProfile,   0 );
     Cmd_CommandAdd( pAbc, "Word level", "%test",       Abc_CommandTest,      0 );
+
+    Cmd_CommandAdd( pAbc, "Word level", "inv_ps",      Abc_CommandInvPs,     0 );
+    Cmd_CommandAdd( pAbc, "Word level", "inv_print",   Abc_CommandInvPrint,  0 );
+    Cmd_CommandAdd( pAbc, "Word level", "inv_check",   Abc_CommandInvCheck,  0 );
+    Cmd_CommandAdd( pAbc, "Word level", "inv_get",     Abc_CommandInvGet,    0 );
+    Cmd_CommandAdd( pAbc, "Word level", "inv_put",     Abc_CommandInvPut,    0 );
+    Cmd_CommandAdd( pAbc, "Word level", "inv_min",     Abc_CommandInvMin,    0 );
 }
 
 /**Function********************************************************************
@@ -440,10 +448,108 @@ usage:
   SeeAlso     []
 
 ******************************************************************************/
-int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    int c, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandProfile(): There is no current design.\n" );
+        return 0;
+    }
+    Wlc_WinProfileArith( pNtk );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: %%profile [-vh]\n" );
+    Abc_Print( -2, "\t         profiles arithmetic components in the word-level networks\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Wlc_NtkSimulateTest( Wlc_Ntk_t * p );
+    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    int c, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" );
+        return 0;
+    }
+    // transform
+    //pNtk = Wlc_NtkUifNodePairs( pNtk, NULL );
+    //pNtk = Wlc_NtkAbstractNodes( pNtk, NULL );
+    //Wlc_AbcUpdateNtk( pAbc, pNtk );
+    //Wlc_GenerateSmtStdout( pAbc );
+    //Wlc_NtkSimulateTest( (Wlc_Ntk_t *)pAbc->pAbcWlc );
+    pNtk = Wlc_NtkDupSingleNodes( pNtk );
+    Wlc_AbcUpdateNtk( pAbc, pNtk );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: %%test [-vh]\n" );
+    Abc_Print( -2, "\t         experiments with word-level networks\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Abc_CommandInvPs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv );
     extern void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose );
     Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    Vec_Int_t * vCounts;
     int c, fVerbose  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
@@ -461,24 +567,66 @@ int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pNtk == NULL )
     {
-        Abc_Print( 1, "Abc_CommandPsInv(): There is no current design.\n" );
+        Abc_Print( 1, "Abc_CommandInvPs(): There is no current design.\n" );
         return 0;
     }
-    if ( Wlc_AbcGetNtk(pAbc) == NULL )
+    if ( Wlc_AbcGetInv(pAbc) == NULL )
     {
-        Abc_Print( 1, "Abc_CommandPsInv(): There is no saved invariant.\n" );
+        Abc_Print( 1, "Abc_CommandInvPs(): Invariant is not available.\n" );
         return 0;
     }
+    vCounts = Pdr_InvCounts( Wlc_AbcGetInv(pAbc) );
+    Wlc_NtkPrintInvStats( pNtk, vCounts, fVerbose );
+    Vec_IntFree( vCounts );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: inv_ps [-vh]\n" );
+    Abc_Print( -2, "\t         prints statistics for inductive invariant\n" );
+    Abc_Print( -2, "\t         (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Abc_CommandInvPrint( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Pdr_InvPrint( Vec_Int_t * vInv );
+    int c, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'v':
+                fVerbose ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
     if ( Wlc_AbcGetInv(pAbc) == NULL )
     {
-        Abc_Print( 1, "Abc_CommandPsInv(): Invariant is not available.\n" );
+        Abc_Print( 1, "Abc_CommandInvPs(): Invariant is not available.\n" );
         return 0;
     }
-    Wlc_NtkPrintInvStats( pNtk, Wlc_AbcGetInv(pAbc), fVerbose );
+    Pdr_InvPrint( Wlc_AbcGetInv(pAbc) );
     return 0;
-    usage:
-    Abc_Print( -2, "usage: %%psinv [-vh]\n" );
-    Abc_Print( -2, "\t         prints statistics for inductive invariant\n" );
+usage:
+    Abc_Print( -2, "usage: inv_print [-vh]\n" );
+    Abc_Print( -2, "\t         prints the current inductive invariant\n" );
     Abc_Print( -2, "\t         (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
@@ -496,11 +644,9 @@ int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv )
   SeeAlso     []
 
 ******************************************************************************/
-int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose );
-    Abc_Ntk_t * pMainNtk;
-    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    extern Vec_Int_t * Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv );
     int c, fVerbose  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
@@ -516,28 +662,76 @@ int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv )
                 goto usage;
         }
     }
-    if ( pNtk == NULL )
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandInvMin(): There is no current design.\n" );
+        return 0;
+    }
+    if ( Wlc_AbcGetInv(pAbc) == NULL )
     {
-        Abc_Print( 1, "Abc_CommandGetInv(): There is no current design.\n" );
+        Abc_Print( 1, "Abc_CommandInvMin(): There is no saved invariant.\n" );
         return 0;
     }
-    if ( Wlc_AbcGetNtk(pAbc) == NULL )
+    if ( Gia_ManRegNum(pAbc->pGia) != Vec_IntEntryLast(Wlc_AbcGetInv(pAbc)) )
     {
-        Abc_Print( 1, "Abc_CommandGetInv(): There is no saved invariant.\n" );
+        Abc_Print( 1, "Abc_CommandInvMin(): The number of flops in the invariant and in GIA should be the same.\n" );
         return 0;
     }
+    Pdr_InvCheck( pAbc->pGia, Wlc_AbcGetInv(pAbc)  );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: inv_check [-vh]\n" );
+    Abc_Print( -2, "\t         checks that the invariant is indeed an inductive invariant\n" );
+    Abc_Print( -2, "\t         (AIG representing the design should be in the &-space)\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Abc_CommandInvGet( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv );
+    Abc_Ntk_t * pMainNtk;
+    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    int c, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'v':
+                fVerbose ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
     if ( Wlc_AbcGetInv(pAbc) == NULL )
     {
-        Abc_Print( 1, "Abc_CommandGetInv(): Invariant is not available.\n" );
+        Abc_Print( 1, "Abc_CommandInvGet(): Invariant is not available.\n" );
         return 0;
     }
     // derive the network
-    pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc), Wlc_AbcGetStr(pAbc), fVerbose );
+    pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc) );
     // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk );
+    if ( pMainNtk )
+        Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk );
     return 0;
-    usage:
-    Abc_Print( -2, "usage: %%getinv [-vh]\n" );
+usage:
+    Abc_Print( -2, "usage: inv_get [-vh]\n" );
     Abc_Print( -2, "\t         places invariant found by PDR as the current network in the main-space\n" );
     Abc_Print( -2, "\t         (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
@@ -556,34 +750,45 @@ int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv )
   SeeAlso     []
 
 ******************************************************************************/
-int Abc_CommandProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandInvPut( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    extern Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, int nRegs );
+    Vec_Int_t * vInv = NULL;
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     int c, fVerbose  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
+            case 'v':
+                fVerbose ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
         }
     }
     if ( pNtk == NULL )
     {
-        Abc_Print( 1, "Abc_CommandProfile(): There is no current design.\n" );
+        Abc_Print( 1, "Abc_CommandInvPut(): There is no current design.\n" );
         return 0;
     }
-    Wlc_WinProfileArith( pNtk );
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandInvPut(): There is no current AIG.\n" );
+        return 0;
+    }
+    // derive the network
+    vInv = Wlc_NtkGetPut( pNtk, Gia_ManRegNum(pAbc->pGia) );
+    if ( vInv )
+        Abc_FrameSetInv( vInv );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%profile [-vh]\n" );
-    Abc_Print( -2, "\t         profiles arithmetic components in the word-level networks\n" );
+    Abc_Print( -2, "usage: inv_put [-vh]\n" );
+    Abc_Print( -2, "\t         inputs the current network in the main-space as an invariant\n" );
+    Abc_Print( -2, "\t         (AIG representing the design should be in the &-space)\n" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
@@ -600,42 +805,49 @@ usage:
   SeeAlso     []
 
 ******************************************************************************/
-int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandInvMin( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Wlc_NtkSimulateTest( Wlc_Ntk_t * p );
-    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    extern Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv );
+    Vec_Int_t * vInv, * vInv2;
     int c, fVerbose  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
+            case 'v':
+                fVerbose ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
         }
     }
-    if ( pNtk == NULL )
+    if ( pAbc->pGia == NULL )
     {
-        Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" );
+        Abc_Print( 1, "Abc_CommandInvMin(): There is no current design.\n" );
         return 0;
     }
-    // transform
-    //pNtk = Wlc_NtkUifNodePairs( pNtk, NULL );
-    //pNtk = Wlc_NtkAbstractNodes( pNtk, NULL );
-    //Wlc_AbcUpdateNtk( pAbc, pNtk );
-    //Wlc_GenerateSmtStdout( pAbc );
-    //Wlc_NtkSimulateTest( (Wlc_Ntk_t *)pAbc->pAbcWlc );
-    pNtk = Wlc_NtkDupSingleNodes( pNtk );
-    Wlc_AbcUpdateNtk( pAbc, pNtk );
+    if ( Wlc_AbcGetInv(pAbc) == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandInvMin(): Invariant is not available.\n" );
+        return 0;
+    }
+    vInv = Wlc_AbcGetInv(pAbc);
+    if ( Gia_ManRegNum(pAbc->pGia) != Vec_IntEntryLast(vInv) )
+    {
+        Abc_Print( 1, "Abc_CommandInvMin(): The number of flops in the invariant and in GIA should be the same.\n" );
+        return 0;
+    }
+    vInv2 = Pdr_InvMinimize( pAbc->pGia, vInv );
+    if ( vInv2 )
+        Abc_FrameSetInv( vInv2 );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%test [-vh]\n" );
-    Abc_Print( -2, "\t         experiments with word-level networks\n" );
+    Abc_Print( -2, "usage: inv_min [-vh]\n" );
+    Abc_Print( -2, "\t         minimizes the number of clauses in the current invariant\n" );
+    Abc_Print( -2, "\t         (AIG representing the design should be in the &-space)\n" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;