added an option -m for %pdra

src/base/wlc/wlc.h

@@ -172,6 +172,7 @@ struct Wlc_Par_t_
     int                    fXorOutput;         // XOR outputs of word-level miter
     int                    fCheckClauses;      // Check clauses in the reloaded trace                    
     int                    fPushClauses;       // Push clauses in the reloaded trace                    
+    int                    fMFFC;              // Refine the entire MFFC of a PPI                     
     int                    fVerbose;           // verbose output
     int                    fPdrVerbose;        // verbose output
 };

src/base/wlc/wlcCom.c

@@ -462,7 +462,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Wlc_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpxvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpmxvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -530,6 +530,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'p':
             pPars->fPushClauses ^= 1;
             break;
+        case 'm':
+            pPars->fMFFC ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -550,7 +553,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
     Wlc_NtkPdrAbs( pNtk, pPars );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-cpxvwh]\n" );
+    Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-cpmxvwh]\n" );
     Abc_Print( -2, "\t         abstraction for word-level networks\n" );
     Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
     Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n",        pPars->nBitsMul );
@@ -559,7 +562,8 @@ usage:
     Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n",                   pPars->nIterMax );
     Abc_Print( -2, "\t-x     : toggle XORing outputs of word-level miter [default = %s]\n",            pPars->fXorOutput? "yes": "no" );
     Abc_Print( -2, "\t-c     : toggle checking clauses in the reloaded trace [default = %s]\n",        pPars->fCheckClauses? "yes": "no" );
-    Abc_Print( -2, "\t-p     : toggle pushing clauses in the reloaded trace [default = %s]\n",        pPars->fPushClauses? "yes": "no" );
+    Abc_Print( -2, "\t-p     : toggle pushing clauses in the reloaded trace [default = %s]\n",         pPars->fPushClauses? "yes": "no" );
+    Abc_Print( -2, "\t-m     : toggle refining the whole MFFC of a PPI [default = %s]\n",              pPars->fMFFC? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",                  pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing verbose PDR output [default = %s]\n",                   pPars->fPdrVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");

src/base/wlc/wlcNtk.c

@@ -116,6 +116,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
     pPars->fXorOutput  =            1;   // XOR outputs of word-level miter
     pPars->fCheckClauses =          1;   // Check clauses in the reloaded trace                    
     pPars->fPushClauses =           0;   // Push clauses in the reloaded trace                    
+    pPars->fMFFC       =            1;   // Refine the entire MFFC of a PPI 
     pPars->fVerbose    =            0;   // verbose output`
     pPars->fPdrVerbose =            0;   // show verbose PDR output
 }