%pdra: added an option -t for disabling trace reuse

5 files changed, 12 insertions, 3 deletions

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 028a4f1d..eb8f4aa4 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -182,6 +182,7 @@ struct Wlc_Par_t_
     int                    fProofUsePPI;       // Use PPI values in PBR
     int                    fUseBmc3;           // Run BMC3 in parallel 
     int                    fShrinkAbs;         // Shrink Abs with BMC
+    int                    fShrinkScratch;     // Restart pdr from scratch after shrinking
     int                    fVerbose;           // verbose output
     int                    fPdrVerbose;        // verbose output
 };
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index b3ac623e..390770ea 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -1511,7 +1511,7 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig )
         assert( Vec_VecSize( pWla->vClauses) >= 2 ); 
         
         if ( pWla->fNewAbs )
-            IPdr_ManRebuildClauses( pPdr, pWla->vClauses );
+            IPdr_ManRebuildClauses( pPdr, pWla->pPars->fShrinkScratch ? NULL : pWla->vClauses );
         else
             IPdr_ManRestoreClauses( pPdr, pWla->vClauses, NULL );
 
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index dbbf060e..4e6fbd18 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -464,7 +464,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, "AMXFILabrcdipqmsuxvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcdipqmstuxvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -567,6 +567,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 's':
             pPars->fShrinkAbs ^= 1;
             break;
+        case 't':
+            pPars->fShrinkScratch ^= 1;
+            break;
         case 'u':
             pPars->fCheckCombUnsat ^= 1;
             break;
@@ -590,7 +593,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
     Wlc_NtkPdrAbs( pNtk, pPars );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcdipqmxsuvwh]\n" );
+    Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcdipqmxstuvwh]\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 );
@@ -606,6 +609,7 @@ usage:
     Abc_Print( -2, "\t-d     : toggle using another way of creating abstractions [default = %s]\n",    pPars->fAbs2? "yes": "no" );
     Abc_Print( -2, "\t-i     : toggle using PPI values in proof-based refinement [default = %s]\n",    pPars->fProofUsePPI? "yes": "no" );
     Abc_Print( -2, "\t-s     : toggle shrinking abstractions with BMC [default = %s]\n",               pPars->fShrinkAbs? "yes": "no" );
+    Abc_Print( -2, "\t-t     : toggle restarting pdr from scratch after shrinking abstractions with BMC [default = %s]\n",               pPars->fShrinkScratch? "yes": "no" );
     Abc_Print( -2, "\t-u     : toggle checking combinationally unsat [default = %s]\n",                pPars->fCheckCombUnsat? "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-q     : toggle running bmc3 in parallel for CEX [default = %s]\n",              pPars->fUseBmc3? "yes": "no" );
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index 43b98d9a..6efa0f6b 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -126,6 +126,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
     pPars->fProofUsePPI  =            0;   // Use PPI values in PBR
     pPars->fUseBmc3      =            0;   // Run BMC3 in parallel
     pPars->fShrinkAbs    =            0;   // Shrink Abs with BMC
+    pPars->fShrinkScratch=            0;   // Restart pdr from scratch after shrinking
     pPars->fVerbose      =            0;   // verbose output`
     pPars->fPdrVerbose   =            0;   // show verbose PDR output
 }
diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c
index c59bfe1c..7bb3319d 100644
--- a/src/proof/pdr/pdrIncr.c
+++ b/src/proof/pdr/pdrIncr.c
@@ -261,6 +261,9 @@ int IPdr_ManRebuildClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses )
     int RetValue = -1;
     int nCubes = 0;
 
+    if ( vClauses == NULL )
+        return RetValue;
+
     assert( Vec_VecSize(vClauses) >= 2 );
     assert( Vec_VecSize(p->vClauses) == 0 ); 
     Vec_VecExpand( p->vClauses, 1 );