Dump last frame clauses with 'pdr -d' even if the problem is SAT or undecided.

3 files changed, 17 insertions, 7 deletions

diff --git a/src/sat/pdr/pdrCore.c b/src/sat/pdr/pdrCore.c
index 6b1e4850..025ada06 100644
--- a/src/sat/pdr/pdrCore.c
+++ b/src/sat/pdr/pdrCore.c
@@ -614,8 +614,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                     Pdr_ManPrintProgress( p, 1, clock() - clkStart );
                 Pdr_ManReportInvariant( p );
                 Pdr_ManVerifyInvariant( p );
-                if ( p->pPars->fDumpInv )
-                    Pdr_ManDumpClauses( p, (char *)"inv.pla" );
                 p->pPars->iFrame = k;
                 return 1; // UNSAT
             }
@@ -669,6 +667,9 @@ int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit,
     p = Pdr_ManStart( pAig, pPars, pvPrioInit? *pvPrioInit : NULL );
     RetValue = Pdr_ManSolveInt( p );
     *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p );
+    if ( p->pPars->fDumpInv )
+        Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 );
+
 //    if ( *ppCex && pPars->fVerbose )
 //        printf( "Found counter-example in frame %d after exploring %d frames.\n", 
 //            (*ppCex)->iFrame, p->nFrames );
diff --git a/src/sat/pdr/pdrInt.h b/src/sat/pdr/pdrInt.h
index b51731bf..39fffc48 100644
--- a/src/sat/pdr/pdrInt.h
+++ b/src/sat/pdr/pdrInt.h
@@ -144,7 +144,7 @@ extern int             Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t
 /*=== pdrInv.c ==========================================================*/
 extern void            Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time );
 extern void            Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart );
-extern void            Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName );
+extern void            Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved );
 extern void            Pdr_ManReportInvariant( Pdr_Man_t * p );
 extern void            Pdr_ManVerifyInvariant( Pdr_Man_t * p );
 /*=== pdrMan.c ==========================================================*/
diff --git a/src/sat/pdr/pdrInv.c b/src/sat/pdr/pdrInv.c
index e2e3cdb7..2f630e28 100644
--- a/src/sat/pdr/pdrInv.c
+++ b/src/sat/pdr/pdrInv.c
@@ -136,7 +136,10 @@ int Pdr_ManFindInvariantStart( Pdr_Man_t * p )
     Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax+1 )
         if ( Vec_PtrSize(vArrayK) == 0 )
             return k;
-    return -1;
+//    return -1;
+    // if there is no starting point (as in case of SAT or undecided), return the last frame
+//    printf( "The last timeframe contains %d clauses.\n", Vec_PtrSize(Vec_VecEntry(p->vClauses, kMax)) );
+    return kMax;
 }
 
 /**Function*************************************************************
@@ -227,7 +230,7 @@ void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart )
   SeeAlso     [] 
 
 ***********************************************************************/
-void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName )
+void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
 {
     int fUseSupp = 1;
     FILE * pFile;
@@ -250,7 +253,10 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName )
     // collect variable appearances
     vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; 
     // output the header
-    fprintf( pFile, "# Inductive invariant for \"%s\"\n", p->pAig->pName );
+    if ( fProved )
+        fprintf( pFile, "# Inductive invariant for \"%s\"\n", p->pAig->pName );
+    else
+        fprintf( pFile, "# Clauses of the last timeframe for \"%s\"\n", p->pAig->pName );
     fprintf( pFile, "# generated by PDR in ABC on %s\n", Aig_TimeStamp() );
     fprintf( pFile, ".i %d\n", fUseSupp ? Pdr_ManCountVariables(p, kStart) : Aig_ManRegNum(p->pAig) );
     fprintf( pFile, ".o 1\n" );
@@ -277,7 +283,10 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName )
     fclose( pFile );
     Vec_IntFreeP( &vFlopCounts );
     Vec_PtrFree( vCubes );
-    printf( "Inductive invariant was written into file \"%s\".\n", pFileName );
+    if ( fProved )
+        printf( "Inductive invariant was written into file \"%s\".\n", pFileName );
+    else
+        printf( "Clauses of the last timeframe were written into file \"%s\".\n", pFileName );
 }