%pdra: added an option -s

5 files changed, 86 insertions, 20 deletions

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index f0ea18d3..028a4f1d 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -181,6 +181,7 @@ struct Wlc_Par_t_
     int                    fAbs2;              // Use UFAR style createAbs
     int                    fProofUsePPI;       // Use PPI values in PBR
     int                    fUseBmc3;           // Run BMC3 in parallel 
+    int                    fShrinkAbs;         // Shrink Abs with BMC
     int                    fVerbose;           // verbose output
     int                    fPdrVerbose;        // verbose output
 };
@@ -199,6 +200,9 @@ struct Wla_Man_t_
     void      * pPdrPars;
     void      * pThread;
 
+    int iCexFrame;
+    int fNewAbs;
+
     int nIters;
     int nTotalCla;
     int nDisj;
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index 8a63fc36..ce9e5da8 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -619,12 +619,11 @@ static Wlc_Ntk_t * Wlc_NtkAbs2( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks, Vec_Int_t
     return pNew;
 }
 
-static Vec_Int_t * Wlc_NtkProofReduce( Wlc_Ntk_t * p, Wlc_Par_t * pPars, int nFrames, Vec_Int_t * vWhites )
+static Vec_Bit_t * Wlc_NtkProofReduce( Wlc_Ntk_t * p, Wlc_Par_t * pPars, int nFrames, Vec_Int_t * vWhites )
 {
     Gia_Man_t * pGiaFrames;
     Wlc_Ntk_t * pNtkWithChoices = NULL; 
     Vec_Int_t * vCoreSels;
-    Vec_Int_t * vCoreWhites = NULL;
     Vec_Bit_t * vChoiceMark; 
     int first_sel_pi;
     int i, Entry;
@@ -642,16 +641,15 @@ static Vec_Int_t * Wlc_NtkProofReduce( Wlc_Ntk_t * p, Wlc_Par_t * pPars, int nFr
 
     Wlc_NtkFree( pNtkWithChoices );
     Gia_ManStop( pGiaFrames );
-    Vec_BitFree( vChoiceMark );
  
-    vCoreWhites = Vec_IntAlloc( Vec_IntSize(vWhites) );
+    Vec_BitReset( vChoiceMark );
     Vec_IntForEachEntry( vCoreSels, Entry, i )
-        Vec_IntPush( vCoreWhites, Vec_IntEntry( vWhites, Entry ) );
+        Vec_BitWriteEntry( vChoiceMark, Entry, 1 );
 
-    Abc_Print( 1, "ProofReduce: remove %d out of %d white boxes.\n", Vec_IntSize(vWhites) - Vec_IntSize(vCoreWhites), Vec_IntSize(vWhites) );
+    Abc_Print( 1, "ProofReduce: remove %d out of %d white boxes.\n", Vec_IntSize(vWhites) - Vec_BitCount(vChoiceMark), Vec_IntSize(vWhites) );
 
     Vec_IntFree( vCoreSels );
-    return vCoreWhites;
+    return vChoiceMark;
 }
 
 static int Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Abc_Cex_t * pCex, Vec_Int_t * vBlacks, Vec_Int_t ** pvRefine )
@@ -1280,6 +1278,26 @@ Vec_Int_t * Wla_ManCollectWhites( Wla_Man_t * pWla )
     return vWhites;
 }
 
+int Wla_ManShrinkAbs( Wla_Man_t * pWla, int nFrames )
+{
+    int i, Entry;
+    int RetValue = 0;
+
+    Vec_Int_t * vWhites = Wla_ManCollectWhites( pWla );
+    Vec_Bit_t * vCoreMarks = Wlc_NtkProofReduce( pWla->p, pWla->pPars, nFrames, vWhites );
+
+    RetValue = Vec_IntSize( vWhites ) != Vec_BitCount( vCoreMarks );
+
+    Vec_IntForEachEntry( vWhites, Entry, i )
+        if ( !Vec_BitEntry( vCoreMarks, i ) )
+            Vec_BitWriteEntry( pWla->vUnmark, Entry, 0 );
+
+    Vec_IntFree( vWhites );
+    Vec_BitFree( vCoreMarks );
+
+    return RetValue;
+}
+
 Wlc_Ntk_t * Wla_ManCreateAbs( Wla_Man_t * pWla )
 {
     Wlc_Ntk_t * pAbs;
@@ -1287,8 +1305,8 @@ Wlc_Ntk_t * Wla_ManCreateAbs( Wla_Man_t * pWla )
     // get abstracted GIA and the set of pseudo-PIs (vBlacks)
     if ( pWla->vBlacks == NULL )
     {
-       pWla->vBlacks = Wlc_NtkGetBlacks( pWla->p, pWla->pPars );
-       pWla->vSignals = Vec_IntDup( pWla->vBlacks );
+        pWla->vBlacks = Wlc_NtkGetBlacks( pWla->p, pWla->pPars );
+        pWla->vSignals = Vec_IntDup( pWla->vBlacks );
     }
     else
     {
@@ -1421,8 +1439,13 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig )
     pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
     if ( pWla->vClauses ) {
         assert( Vec_VecSize( pWla->vClauses) >= 2 ); 
-        IPdr_ManRestoreClauses( pPdr, pWla->vClauses, NULL );
-        //IPdr_ManRebuildClauses( pPdr, pWla->vClauses );
+        
+        if ( pWla->fNewAbs )
+            IPdr_ManRebuildClauses( pPdr, pWla->vClauses );
+        else
+            IPdr_ManRestoreClauses( pPdr, pWla->vClauses, NULL );
+
+        pWla->fNewAbs = 0;
     }
 
     RetValue = IPdr_ManSolveInt( pPdr, pWla->pPars->fCheckClauses, pWla->pPars->fPushClauses );
@@ -1464,6 +1487,14 @@ void Wla_ManRefine( Wla_Man_t * pWla )
     abctime clk;
     int nNodes;
     Vec_Int_t * vRefine = NULL;
+
+    if ( pWla->fNewAbs )
+    {
+        assert( pWla->pCex == NULL );
+        Gia_ManStop( pWla->pGia ); pWla->pGia = NULL;
+        return;
+    }
+
     // perform refinement
     if ( pWla->pPars->fHybrid || !pWla->pPars->fProofRefine )
     {
@@ -1519,12 +1550,14 @@ void Wla_ManRefine( Wla_Man_t * pWla )
     if ( pWla->pCex->iFrame > 0 )
     {
         Vec_Int_t * vWhites = Wla_ManCollectWhites( pWla );
-        Vec_Int_t * vCore = Wlc_NtkProofReduce( pWla->p, pWla->pPars, pWla->pCex->iFrame, vWhites );
+        Vec_Bit_t * vCore = Wlc_NtkProofReduce( pWla->p, pWla->pPars, pWla->pCex->iFrame, vWhites );
         Vec_IntFree( vWhites );
-        Vec_IntFree( vCore );
+        Vec_BitFree( vCore );
     }
     */
 
+    pWla->iCexFrame = pWla->pCex->iFrame;
+
     Vec_IntFree( vRefine );
     Gia_ManStop( pWla->pGia ); pWla->pGia = NULL;
     Abc_CexFree( pWla->pCex ); pWla->pCex = NULL;
@@ -1551,10 +1584,13 @@ Wla_Man_t * Wla_ManStart( Wlc_Ntk_t * pNtk, Wlc_Par_t * pPars )
     } 
     p->pPdrPars = (void *)pPdrPars;
 
-    p->nIters = 1;
+    p->iCexFrame = 0;
+    p->fNewAbs   = 0;
+
+    p->nIters    = 1;
     p->nTotalCla = 0;
-    p->nDisj = 0;
-    p->nNDisj = 0;
+    p->nDisj     = 0;
+    p->nNDisj    = 0;
 
     return p;
 }
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 871b3e5d..dbbf060e 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, "AMXFILabrcdipqmuxvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcdipqmsuxvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -564,6 +564,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'm':
             pPars->fMFFC ^= 1;
             break;
+        case 's':
+            pPars->fShrinkAbs ^= 1;
+            break;
         case 'u':
             pPars->fCheckCombUnsat ^= 1;
             break;
@@ -587,7 +590,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] [-abrcdipqmxuvwh]\n" );
+    Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcdipqmxsuvwh]\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 );
@@ -602,6 +605,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-s     : toggle shrinking abstractions with BMC [default = %s]\n",               pPars->fShrinkAbs? "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 d1eaf7c5..43b98d9a 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -125,6 +125,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
     pPars->fAbs2         =            0;   // Use UFAR style createAbs
     pPars->fProofUsePPI  =            0;   // Use PPI values in PBR
     pPars->fUseBmc3      =            0;   // Run BMC3 in parallel
+    pPars->fShrinkAbs    =            0;   // Shrink Abs with BMC
     pPars->fVerbose      =            0;   // verbose output`
     pPars->fPdrVerbose   =            0;   // show verbose PDR output
 }
diff --git a/src/base/wlc/wlcPth.c b/src/base/wlc/wlcPth.c
index 783dbe6f..8cdc682e 100644
--- a/src/base/wlc/wlcPth.c
+++ b/src/base/wlc/wlcPth.c
@@ -40,6 +40,7 @@ ABC_NAMESPACE_IMPL_START
 
 extern Abc_Ntk_t *   Abc_NtkFromAigPhase( Aig_Man_t * pAig );
 extern int           Abc_NtkDarBmc3( Abc_Ntk_t * pAbcNtk, Saig_ParBmc_t * pBmcPars, int fOrDecomp );
+extern int           Wla_ManShrinkAbs( Wla_Man_t * pWla, int nFrames );
 
 static volatile int  g_nRunIds = 0;             // the number of the last prover instance
 int Wla_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; }
@@ -55,6 +56,7 @@ void Wla_ManConcurrentBmc3( Wla_Man_t * pWla, Aig_Man_t * pAig, Abc_Cex_t ** ppC
 // information given to the thread
 typedef struct Bmc3_ThData_t_
 {
+    Wla_Man_t *  pWla;
     Aig_Man_t *  pAig;
     Abc_Cex_t ** ppCex;
     int          RunId;
@@ -84,6 +86,7 @@ void * Wla_Bmc3Thread ( void * pArg )
 {
     int status;
     int RetValue = -1;
+    int nFramesNoChangeLim = 10;
     Bmc3_ThData_t * pData = (Bmc3_ThData_t *)pArg;
     Abc_Ntk_t * pAbcNtk = Abc_NtkFromAigPhase( pData->pAig );
     Saig_ParBmc_t BmcPars, *pBmcPars = &BmcPars;
@@ -91,6 +94,9 @@ void * Wla_Bmc3Thread ( void * pArg )
     pBmcPars->pFuncStop = Wla_CallBackToStop;
     pBmcPars->RunId = pData->RunId;
 
+    if ( pData->pWla->nIters > 1 && pData->pWla->pPars->fShrinkAbs )
+        pBmcPars->nFramesMax = pData->pWla->iCexFrame + nFramesNoChangeLim;
+
     RetValue = Abc_NtkDarBmc3( pAbcNtk, pBmcPars, 0 );
 
     if ( RetValue == 0 )
@@ -106,10 +112,24 @@ void * Wla_Bmc3Thread ( void * pArg )
         ++g_nRunIds;
         status = pthread_mutex_unlock(&g_mutex);  assert( status == 0 );
     }
-    else
+    else if ( RetValue == -1 )
     {
-        if ( pData->fVerbose )
+        if ( pData->RunId < g_nRunIds && pData->fVerbose )
             Abc_Print( 1, "Bmc3 was cancelled. RunId=%d.\n", pData->RunId );
+
+        if ( pData->RunId == g_nRunIds )
+        {
+            RetValue = Wla_ManShrinkAbs( pData->pWla, pData->pWla->iCexFrame + nFramesNoChangeLim );
+            pData->pWla->iCexFrame += nFramesNoChangeLim; 
+            
+            if ( RetValue )
+            {
+                pData->pWla->fNewAbs = 1;
+                status = pthread_mutex_lock(&g_mutex);  assert( status == 0 );
+                ++g_nRunIds;
+                status = pthread_mutex_unlock(&g_mutex);  assert( status == 0 );
+            }
+        }
     }
 
     // free memory
@@ -132,6 +152,7 @@ void Wla_ManConcurrentBmc3( Wla_Man_t * pWla, Aig_Man_t * pAig, Abc_Cex_t ** ppC
     pWla->pThread = (void *)ABC_CALLOC( pthread_t, 1 );
 
     pData = ABC_CALLOC( Bmc3_ThData_t, 1 );
+    pData->pWla = pWla;
     pData->pAig = pAig;
     pData->ppCex = ppCex;
     pData->RunId = g_nRunIds;