added an option -r to %pdra: proof-based refinement only

4 files changed, 21 insertions, 8 deletions

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 1a2bc505..f5dbba42 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -171,11 +171,12 @@ struct Wlc_Par_t_
     int                    nIterMax;           // the max number of iterations
     int                    nLimit;             // the max number of signals
     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                    fPdra;              // Use pdr -nct                     
+    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                    fPdra;              // Use pdr -nct
     int                    fProofRefine;       // Use proof-based refinement
+    int                    fHybrid;            // Use a hybrid of CBR and PBR
     int                    fVerbose;           // verbose output
     int                    fPdrVerbose;        // verbose output
 };
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index 69d1df77..1eb5a964 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -1107,9 +1107,16 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
         }
 
         // perform refinement
-        clk2 = Abc_Clock();
-        vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
-        tCbr += Abc_Clock() - clk2;
+        if ( pPars->fHybrid || !pPars->fProofRefine )
+        {
+            clk2 = Abc_Clock();
+            vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
+            tCbr += Abc_Clock() - clk2;
+        }
+        else // proof-based only
+        {
+            vRefine = Vec_IntDup( vPisNew );
+        }
         if ( pPars->fProofRefine ) 
         {
             clk2 = Abc_Clock();
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 781f4a9a..0c9cdabb 100644
--- a/src/base/wlc/wlcCom.c
+++ b/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, "AMXFILabcpmxvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcpmxvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -538,6 +538,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'b':
             pPars->fProofRefine ^= 1;
             break;
+        case 'r':
+            pPars->fHybrid ^= 1;
+            break;
         case 'x':
             pPars->fXorOutput ^= 1;
             break;
@@ -581,6 +584,7 @@ usage:
     Abc_Print( -2, "\t-x     : toggle XORing outputs of word-level miter [default = %s]\n",            pPars->fXorOutput? "yes": "no" );
     Abc_Print( -2, "\t-a     : toggle running pdr with -nct [default = %s]\n",                         pPars->fPdra? "yes": "no" );
     Abc_Print( -2, "\t-b     : toggle using proof-based refinement [default = %s]\n",                  pPars->fProofRefine? "yes": "no" );
+    Abc_Print( -2, "\t-r     : toggle using both cex-based and proof-based refinement [default = %s]\n",                  pPars->fHybrid? "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-m     : toggle refining the whole MFFC of a PPI [default = %s]\n",              pPars->fMFFC? "yes": "no" );
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index 02af1a16..89699949 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -120,6 +120,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
     pPars->fMFFC         =            1;   // Refine the entire MFFC of a PPI 
     pPars->fPdra         =            0;   // Use pdr -nct 
     pPars->fProofRefine  =            0;   // Use proof-based refinement
+    pPars->fHybrid       =            1;   // Use a hybrid of CBR and PBR
     pPars->fVerbose      =            0;   // verbose output`
     pPars->fPdrVerbose   =            0;   // show verbose PDR output
 }