added options of checking and pushing to %pdra

src/base/wlc/wlc.h

@@ -184,6 +184,8 @@ struct WlcPdr_Par_t_
     int                    nBitsFlop;          // flop bit-width
     int                    nIterMax;           // the max number of iterations
     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                    fVerbose;           // verbose output
     int                    fPdrVerbose;        // verbose output
 };

src/base/wlc/wlcAbs.c

@@ -32,7 +32,7 @@ ABC_NAMESPACE_IMPL_START
 
 extern Vec_Vec_t *   IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast );
 extern int           IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses );
-extern int           IPdr_ManSolveInt( Pdr_Man_t * p );
+extern int           IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -59,6 +59,8 @@ void WlcPdr_ManSetDefaultParams( WlcPdr_Par_t * pPars )
     pPars->nBitsFlop   = ABC_INFINITY;   // flop bit-width
     pPars->nIterMax    =         1000;   // the max number of iterations
     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->fVerbose    =            0;   // verbose output
     pPars->fPdrVerbose =            0;   // show verbose PDR output
 }
@@ -76,7 +78,7 @@ void WlcPdr_ManSetDefaultParams( WlcPdr_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose )
+static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose )
 {
     Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) );
     Wlc_Obj_t * pObj; int i, Count[4] = {0};
@@ -197,7 +199,7 @@ static void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t *
   SeeAlso     []
 
 ***********************************************************************/
-static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, int fVerbose )
+static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, int fVerbose )
 {
     Wlc_Ntk_t * pNtkNew = NULL;
     Vec_Int_t * vPisOld = Vec_IntAlloc( 100 );
@@ -401,7 +403,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars )
             IPdr_ManRestore( pPdr, vClauses );
         }
 
-        RetValue = IPdr_ManSolveInt( pPdr );
+        RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses );
         pPdr->tTotal += Abc_Clock() - pdrClk;
 
         pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;

src/base/wlc/wlcCom.c

@@ -462,7 +462,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     WlcPdr_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpxvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -524,6 +524,12 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'x':
             pPars->fXorOutput ^= 1;
             break;
+        case 'c':
+            pPars->fCheckClauses ^= 1;
+            break;
+        case 'p':
+            pPars->fPushClauses ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -544,7 +550,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] [-xvwh]\n" );
+    Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-cpxvwh]\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 );
@@ -552,6 +558,8 @@ usage:
     Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n",         pPars->nBitsFlop );
     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-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/proof/pdr/pdrIncr.c

@@ -68,7 +68,9 @@ void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [ Check if each cube c_k in frame k satisfies the query
+                R_{k-1} && T && !c_k && c_k' (must be UNSAT).
+                Return True if all cubes pass the check. ]
 
   Description []
                
@@ -214,7 +216,7 @@ int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses )
   SeeAlso     []
 
 ***********************************************************************/
-int IPdr_ManSolveInt( Pdr_Man_t * p )
+int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
 {
     int fPrintClauses = 0;
     Pdr_Set_t * pCube = NULL;
@@ -242,7 +244,34 @@ int IPdr_ManSolveInt( Pdr_Man_t * p )
         Pdr_ManCreateSolver( p, (iFrame = 0) );
     else {
         iFrame = Vec_VecSize(p->vClauses) - 1;
+
+        if ( fCheckClauses )
+        {
+            if ( p->pPars->fVerbose )
+               Abc_Print( 1, "IPDR: Checking the reloaded length-%d trace...", iFrame + 1 ) ;
             IPdr_ManCheckClauses( p );
+            if ( p->pPars->fVerbose )
+               Abc_Print( 1, " Passed!\n" ) ;
+        }
+
+        if ( fPushClauses )
+        {
+            p->iUseFrame = Abc_MaxInt(iFrame, 1);
+
+            if ( p->pPars->fVerbose ) 
+            {
+                Abc_Print( 1, "IPDR: Pushing the reloaded clauses. Before:\n" );
+                Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
+            }
+
+            RetValue = Pdr_ManPushClauses( p );
+
+            if ( p->pPars->fVerbose ) 
+            {
+                Abc_Print( 1, "IPDR: Finished pushing. After:\n" );
+                Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
+            }
+        }
     }
     while ( 1 )
     {
@@ -602,7 +631,7 @@ int IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
 
     p = Pdr_ManStart( pAig, pPars, NULL );
     while ( 1 ) {
-        RetValue = IPdr_ManSolveInt( p );
+        RetValue = IPdr_ManSolveInt( p, 1, 0 );
 
         if ( RetValue == -1 && pPars->iFrame == pPars->nFrameMax) {
             vClausesSaved = IPdr_ManSaveClauses( p, 1 );