Adding PDR with abstraction.

3 files changed, 11 insertions, 41 deletions

diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 5aa689f5..f77bc05f 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -706,7 +706,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
     {
         Counter++;
         pThis = Pdr_QueueHead( p );
-        if ( pThis->iFrame == 0 )
+        if ( pThis->iFrame == 0 || (p->pPars->fUseAbs && Pdr_SetIsInit(pThis->pState, -1)) )
             return 0; // SAT
         if ( pThis->iFrame > kMax ) // finished this level
             return 1;
@@ -862,7 +862,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
     while ( 1 )
     {
         int fRefined = 0;
-        if ( p->pPars->fUseAbs && iFrame == 3 )
+        if ( p->pPars->fUseAbs && p->vAbsFlops == NULL && iFrame == 2 )
         {
             int i, Prio;
             assert( p->vAbsFlops == NULL );
@@ -995,7 +995,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                             Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
                             Pdr_ManPrintClauses( p, 0 );
                         }
-                        if ( p->pPars->fVerbose )
+                        if ( p->pPars->fVerbose && !p->pPars->fUseAbs )
                             Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart );
                         p->pPars->iFrame = iFrame;
                         if ( !p->pPars->fSolveAll )
@@ -1043,6 +1043,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                         Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
                 }
             }
+            if ( fRefined )
+                break;
             if ( p->pTime4Outs )
             {
                 abctime timeSince = Abc_Clock() - clkOne;
@@ -1059,9 +1061,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                 p->timeToStopOne = 0;
             }
         }
-
         if ( p->pPars->fVerbose )
             Pdr_ManPrintProgress( p, !fRefined, Abc_Clock() - clkStart );
+        if ( fRefined )
+            continue;
         // open a new timeframe
         p->nQueLim = p->pPars->nRestLimit;
         assert( pCube == NULL );
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index e3233a3a..554add9b 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -470,8 +470,8 @@ void Pdr_ManReportInvariant( Pdr_Man_t * p )
     Vec_Ptr_t * vCubes;
     int kStart = Pdr_ManFindInvariantStart( p );
     vCubes = Pdr_ManCollectCubes( p, kStart );
-    Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d) (%.2f)\n", 
-        kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig), 1.0*p->nXsimLits/p->nXsimRuns );
+    Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d) (cex = %d, ave = %.2f)\n", 
+        kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig), p->nCexesTotal, 1.0*p->nXsimLits/p->nXsimRuns );
 //    Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d)\n", 
 //        kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig) );
     Vec_PtrFree( vCubes );
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c
index 283a0e1d..acbf70f5 100644
--- a/src/proof/pdr/pdrTsim.c
+++ b/src/proof/pdr/pdrTsim.c
@@ -473,54 +473,21 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
     Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits );
     assert( Vec_IntSize(vRes) > 0 );
     //p->tTsim += Abc_Clock() - clk;
+
     // move abstracted literals from flops to inputs
     if ( p->pPars->fUseAbs && p->vAbsFlops )
     {
-        int i, iLit, Used, k = 0, fAllNegs = 1;
+        int i, iLit, k = 0;
         Vec_IntForEachEntry( vRes, iLit, i )
         {
             if ( Vec_IntEntry(p->vAbsFlops, Abc_Lit2Var(iLit)) ) // used flop
-            {
                 Vec_IntWriteEntry( vRes, k++, iLit );
-                fAllNegs &= Abc_LitIsCompl(iLit);
-            }
             else
                 Vec_IntPush( vPiLits, 2*Saig_ManPiNum(p->pAig) + iLit );
         }
         Vec_IntShrink( vRes, k );
-        if ( fAllNegs ) // insert any positive literal
-        {
-            Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
-            {
-                if ( !Saig_ObjIsLo( p->pAig, pObj ) )
-                    continue;
-                if ( Vec_IntEntry(vCiVals, i) )
-                {
-                    Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
-                    Vec_IntPush( vRes, Abc_Var2Lit(Entry, 0) );
-                    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 );
-    assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
-
     //ZH: Disabled assertion because this invariant doesn't hold with down
     //because of the join operation which can bring in initial states
     //assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );