%pdra: added an option for disabling incremental solving

src/base/wlc/wlc.h

@@ -175,6 +175,7 @@ struct Wlc_Par_t_
     int                    fPushClauses;       // Push clauses in the reloaded trace
     int                    fMFFC;              // Refine the entire MFFC of a PPI
     int                    fPdra;              // Use pdr -nct
+    int                    fLoadTrace;         // Load previous traces if any
     int                    fProofRefine;       // Use proof-based refinement
     int                    fHybrid;            // Use a hybrid of CBR and PBR
     int                    fCheckCombUnsat;    // Check if ABS becomes comb. unsat

src/base/wlc/wlcAbs.c

@@ -1530,7 +1530,8 @@ int Wla_ManSolveInt( Wla_Man_t * pWla, Aig_Man_t * pAig )
     RetValue = IPdr_ManSolveInt( pPdr, pWla->pPars->fCheckClauses, pWla->pPars->fPushClauses );
     pPdr->tTotal += Abc_Clock() - clk;
     pWla->tPdr += pPdr->tTotal;
-    pWla->vClauses = IPdr_ManSaveClauses( pPdr, 0 );
+    if ( pWla->pPars->fLoadTrace)
+        pWla->vClauses = IPdr_ManSaveClauses( pPdr, 0 );
     Pdr_ManStop( pPdr );
 
 

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, "AMXFILabrcdipqmstuxvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcdilpqmstuxvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -555,6 +555,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'i':
             pPars->fProofUsePPI ^= 1;
             break;
+        case 'l':
+            pPars->fLoadTrace ^= 1;
+            break;
         case 'p':
             pPars->fPushClauses ^= 1;
             break;
@@ -593,7 +596,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] [-abrcdipqmxstuvwh]\n" );
+    Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcdilpqmxstuvwh]\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 );
@@ -608,6 +611,7 @@ usage:
     Abc_Print( -2, "\t-c     : toggle checking clauses in the reloaded trace [default = %s]\n",        pPars->fCheckClauses? "yes": "no" );
     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-l     : toggle loading previous PDR traces [default = %s]\n",                   pPars->fLoadTrace? "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" );

src/base/wlc/wlcNtk.c

@@ -119,6 +119,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
     pPars->fPushClauses  =            0;   // Push clauses in the reloaded trace                    
     pPars->fMFFC         =            1;   // Refine the entire MFFC of a PPI 
     pPars->fPdra         =            0;   // Use pdr -nct 
+    pPars->fLoadTrace    =            1;   // Load previous PDR traces 
     pPars->fProofRefine  =            0;   // Use proof-based refinement
     pPars->fHybrid       =            1;   // Use a hybrid of CBR and PBR
     pPars->fCheckCombUnsat =          0;   // Check if ABS becomes comb. unsat