%pdra: added an option -i for weaker proof-based refinement

src/base/wlc/wlc.h

@@ -179,6 +179,7 @@ struct Wlc_Par_t_
     int                    fHybrid;            // Use a hybrid of CBR and PBR
     int                    fCheckCombUnsat;    // Check if ABS becomes comb. unsat
     int                    fAbs2;              // Use UFAR style createAbs
+    int                    fProofUsePPI;       // Use PPI values in PBR
     int                    fVerbose;           // verbose output
     int                    fPdrVerbose;        // verbose output
 };

src/base/wlc/wlcAbs.c

@@ -148,7 +148,7 @@ static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num
     return vCores;
 }
 
-static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, int nbits_old_pis, int num_sel_pis, int * p_num_ppis, int sel_pi_first) 
+static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, int nbits_old_pis, int num_sel_pis, int * p_num_ppis, int sel_pi_first, int fUsePPI) 
 {
     Gia_Man_t * pGiaChoice = Wlc_NtkBitBlast( pChoice, NULL, -1, 0, 0, 0, 0 );
     int nbits_new_pis = Wlc_NtkNumPiBits( pChoice );
@@ -179,8 +179,15 @@ static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, i
             if ( i >= nbits_old_pis && i < nbits_old_pis + num_ppis + num_sel_pis ) 
             {
                 is_sel_pi = sel_pi_first ? (i < nbits_old_pis + num_sel_pis) : (i >= nbits_old_pis + num_ppis);
-                if(f == 0 || !is_sel_pi)
+                if( f == 0 && is_sel_pi )
                     Gia_ManPi(pGiaChoice, i)->Value = Gia_ManAppendCi(pFrames);
+                if( !is_sel_pi )
+                {
+                    if ( !fUsePPI )
+                        Gia_ManPi(pGiaChoice, i)->Value = Gia_ManAppendCi(pFrames);
+                    else
+                        Gia_ManPi(pGiaChoice, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i + num_undc_pis);
+                }
             } 
             else if (i < nbits_old_pis) 
             {
@@ -446,8 +453,13 @@ static int Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Abc_Cex_t * pCe
     }
 
     pNtkWithChoices = vBlacks ? Wlc_NtkIntroduceChoices( p, vBlacks ) : NULL;
-    pGiaFrames = Wlc_NtkUnrollWithCex( pNtkWithChoices, pCex, Wlc_NtkNumPiBits( p ), Vec_IntSize( vBlacks ), &num_ppis, 0 );
+    pGiaFrames = Wlc_NtkUnrollWithCex( pNtkWithChoices, pCex, Wlc_NtkNumPiBits( p ), Vec_IntSize( vBlacks ), &num_ppis, 0, pPars->fProofUsePPI );
+
+    if ( !pPars->fProofUsePPI )
         vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, pCex->iFrame+1, Vec_IntSize( vBlacks ), num_ppis, vChoiceMark, 0, 0, pPars );
+    else
+        vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, pCex->iFrame+1, Vec_IntSize( vBlacks ), 0, vChoiceMark, 0, 0, pPars );
+
     Wlc_NtkFree( pNtkWithChoices );
     Gia_ManStop( pGiaFrames );
     Vec_BitFree( vUnmark );

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, "AMXFILabrcdpmuxvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcdipmuxvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -550,6 +550,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             pPars->fAbs2 ^= 1;
             break;
+        case 'i':
+            pPars->fProofUsePPI ^= 1;
+            break;
         case 'p':
             pPars->fPushClauses ^= 1;
             break;
@@ -579,7 +582,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] [-abrcdpmxuvwh]\n" );
+    Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcdipmxuvwh]\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 );
@@ -593,6 +596,7 @@ usage:
     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-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-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-m     : toggle refining the whole MFFC of a PPI [default = %s]\n",              pPars->fMFFC? "yes": "no" );

src/base/wlc/wlcNtk.c

@@ -123,6 +123,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
     pPars->fHybrid       =            1;   // Use a hybrid of CBR and PBR
     pPars->fCheckCombUnsat =          0;   // Check if ABS becomes comb. unsat
     pPars->fAbs2         =            0;   // Use UFAR style createAbs
+    pPars->fProofUsePPI  =            0;   // Use PPI values in PBR
     pPars->fVerbose      =            0;   // verbose output`
     pPars->fPdrVerbose   =            0;   // show verbose PDR output
 }