Adding PDR with abstraction.

5 files changed, 39 insertions, 13 deletions

diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index fb35269d..5aa689f5 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -861,7 +861,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
     Pdr_ManCreateSolver( p, (iFrame = 0) );
     while ( 1 )
     {
-        if ( p->pPars->fUseAbs && iFrame == 2 )
+        int fRefined = 0;
+        if ( p->pPars->fUseAbs && iFrame == 3 )
         {
             int i, Prio;
             assert( p->vAbsFlops == NULL );
@@ -872,9 +873,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                 if ( Prio >> p->nPrioShift  )
                     Vec_IntWriteEntry( p->vAbsFlops, i, 1 );
         }
-        if ( p->pPars->fUseAbs && p->vAbsFlops )
-            printf( "Starting frame %d with %d flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops) );
-
+        //if ( p->pPars->fUseAbs && p->vAbsFlops )
+        //    printf( "Starting frame %d with %d flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops) );
         p->nFrames = iFrame;
         assert( iFrame == Vec_PtrSize(p->vSolvers)-1 );
         p->iUseFrame = Abc_MaxInt(iFrame, 1);
@@ -1000,12 +1000,15 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                         p->pPars->iFrame = iFrame;
                         if ( !p->pPars->fSolveAll )
                         {
+                            abctime clk = Abc_Clock();
                             Abc_Cex_t * pCex = Pdr_ManDeriveCexAbs(p);
+                            p->tAbs += Abc_Clock() - clk;
                             if ( pCex == NULL )
                             {
                                 assert( p->pPars->fUseAbs );
                                 Pdr_QueueClean( p );
                                 pCube = NULL;
+                                fRefined = 1;
                                 break; // keep solving
                             }
                             p->pAig->pSeqModel = pCex;
@@ -1058,7 +1061,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
         }
 
         if ( p->pPars->fVerbose )
-            Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
+            Pdr_ManPrintProgress( p, !fRefined, Abc_Clock() - clkStart );
         // open a new timeframe
         p->nQueLim = p->pPars->nRestLimit;
         assert( pCube == NULL );
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index 2ee4ae09..a6d249e8 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -96,6 +96,8 @@ struct Pdr_Man_t_
     Vec_Int_t * vAbsFlops; // flops currently used
     Vec_Int_t * vMapFf2Ppi;
     Vec_Int_t * vMapPpi2Ff;
+    int         nCexes;
+    int         nCexesTotal;
     // terminary simulation
     Txs_Man_t * pTxs;      
     // internal use
@@ -142,6 +144,7 @@ struct Pdr_Man_t_
     abctime     tTsim;
     abctime     tContain;
     abctime     tCnf;
+    abctime     tAbs;
     abctime     tTotal;
 };
 
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index 7a8a66d6..e3233a3a 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -80,8 +80,10 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time )
     }
     for ( i = ThisSize; i < 70; i++ )
         Abc_Print( 1, " " );
-    Abc_Print( 1, "%6d", p->nQueMax );
-    Abc_Print( 1, "%6d", p->nAbsFlops );
+    Abc_Print( 1, "%5d", p->nQueMax );
+    Abc_Print( 1, "%5d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops );
+    if ( p->pPars->fUseAbs )
+    Abc_Print( 1, "%5d", p->nCexes );
     Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC );
     if ( p->pPars->fSolveAll )
         Abc_Print( 1, "  CEX =%4d", p->pPars->nFailOuts );
@@ -89,7 +91,7 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time )
         Abc_Print( 1, "  T/O =%3d", p->pPars->nDropOuts );
     Abc_Print( 1, "%s", fClose ? "\n":"\r" );
     if ( fClose )
-        p->nQueMax = 0;
+        p->nQueMax = 0, p->nCexes = 0;
     fflush( stdout );
 }
 
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index e2807c92..c19041ee 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -324,8 +324,8 @@ void Pdr_ManStop( Pdr_Man_t * p )
     Aig_ManCleanMarkAB( p->pAig );
     if ( p->pPars->fVerbose ) 
     {
-        Abc_Print( 1, "Block =%5d  Oblig =%6d  Clause =%6d  Call =%6d (sat=%.1f%%)  Start =%4d\n", 
-            p->nBlocks, p->nObligs, p->nCubes, p->nCalls, 100.0 * p->nCallsS / p->nCalls, p->nStarts );
+        Abc_Print( 1, "Block =%5d  Oblig =%6d  Clause =%6d  Call =%6d (sat=%.1f%%)  Cex =%4d  Start =%4d\n", 
+            p->nBlocks, p->nObligs, p->nCubes, p->nCalls, 100.0 * p->nCallsS / p->nCalls, p->nCexesTotal, p->nStarts );
         ABC_PRTP( "SAT solving", p->tSat,       p->tTotal );
         ABC_PRTP( "  unsat    ", p->tSatUnsat,  p->tTotal );
         ABC_PRTP( "  sat      ", p->tSatSat,    p->tTotal );
@@ -334,6 +334,7 @@ void Pdr_ManStop( Pdr_Man_t * p )
         ABC_PRTP( "Ternary sim", p->tTsim,      p->tTotal );
         ABC_PRTP( "Containment", p->tContain,   p->tTotal );
         ABC_PRTP( "CNF compute", p->tCnf,       p->tTotal );
+        ABC_PRTP( "Refinement ", p->tAbs,       p->tTotal );
         ABC_PRTP( "TOTAL      ", p->tTotal,     p->tTotal );
         fflush( stdout );
     }
@@ -503,7 +504,7 @@ Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p )
     assert( f == nFrames );
     // perform CEX minimization
     pAbs = Gia_ManDupAbs( p->pGia, p->vMapPpi2Ff, p->vMapFf2Ppi );
-    pCexCare = Bmc_CexCareMinimizeAig( pAbs, nPis, pCex, 1, 1, 1 );
+    pCexCare = Bmc_CexCareMinimizeAig( pAbs, nPis, pCex, 1, 0, 0 );
     Gia_ManStop( pAbs );
     assert( pCexCare->nPis == pCex->nPis );
     Abc_CexFree( pCex );
@@ -520,7 +521,9 @@ Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p )
     Abc_CexFree( pCexCare );
     if ( nFfRefined == 0 ) // no refinement -- this is a real CEX
         return Pdr_ManDeriveCex(p);
-    printf( "CEX-based refinement refined %d flops.\n", nFfRefined );
+    //printf( "CEX-based refinement refined %d flops.\n", nFfRefined );
+    p->nCexesTotal++;
+    p->nCexes++;
     return NULL;
 }
 
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c
index 1cff03c7..283a0e1d 100644
--- a/src/proof/pdr/pdrTsim.c
+++ b/src/proof/pdr/pdrTsim.c
@@ -476,7 +476,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
     // move abstracted literals from flops to inputs
     if ( p->pPars->fUseAbs && p->vAbsFlops )
     {
-        int i, iLit, k = 0, fAllNegs = 1;
+        int i, iLit, Used, k = 0, fAllNegs = 1;
         Vec_IntForEachEntry( vRes, iLit, i )
         {
             if ( Vec_IntEntry(p->vAbsFlops, Abc_Lit2Var(iLit)) ) // used flop
@@ -501,6 +501,21 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
                     break;
                 }
             }
+            // add any flop that is not in the cone
+            if ( i == Vec_IntSize(vCiObjs) )
+            {
+                Vec_IntForEachEntry( p->vAbsFlops, Used, i )
+                {
+                    if ( !Used )
+                        continue;
+                    if ( Vec_IntFind( vRes, Abc_Var2Lit(i, 1) ) >= 0 )
+                        continue;
+                    Vec_IntPush( vRes, Abc_Var2Lit(i, 0) );
+                    //Vec_IntPrint( vRes );
+                    break;
+                }
+                assert( i < Vec_IntSize(p->vAbsFlops) );
+            }
         }
     }
     pRes = Pdr_SetCreate( vRes, vPiLits );