From 4f0f2e09f84b66c1ed9a842a71a09f2f1ec65588 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 28 Sep 2016 16:27:39 -0700
Subject: Adding flag 'pdr -e' to output only support variables in the
 invariant.

---
 src/proof/pdr/pdr.h     |  1 +
 src/proof/pdr/pdrCore.c |  1 +
 src/proof/pdr/pdrInv.c  | 10 ++++------
 3 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'src/proof')

diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index 3dffac17..529a161f 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -52,6 +52,7 @@ struct Pdr_Par_t_
     int fTwoRounds;       // use two rounds for generalization
     int fMonoCnf;         // monolythic CNF
     int fDumpInv;         // dump inductive invariant
+    int fUseSupp;         // use support in the invariant
     int fShortest;        // forces bug traces to be shortest
     int fShiftStart;      // allows clause pushing to start from an intermediate frame
     int fReuseProofOblig; // reuses proof-obligationgs in the last timeframe
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 5b619f4b..c020c56a 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -60,6 +60,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
     pPars->fTwoRounds     =       0;  // use two rounds for generalization
     pPars->fMonoCnf       =       0;  // monolythic CNF
     pPars->fDumpInv       =       0;  // dump inductive invariant
+    pPars->fUseSupp       =       1;  // using support variables in the invariant
     pPars->fShortest      =       0;  // forces bug traces to be shortest
     pPars->fUsePropOut    =       1;  // use property output
     pPars->fVerbose       =       0;  // verbose output
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index e5093359..02b90a36 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -339,7 +339,6 @@ void Pdr_ManDumpAig( Aig_Man_t * p, Vec_Ptr_t * vCubes )
 ***********************************************************************/
 void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
 {
-    int fUseSupp = 1;
     FILE * pFile;
     Vec_Int_t * vFlopCounts;
     Vec_Ptr_t * vCubes;
@@ -370,14 +369,14 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
         Count++;
     }
     // collect variable appearances
-    vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; 
+    vFlopCounts = p->pPars->fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; 
     // output the header
     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, ".i %d\n", p->pPars->fUseSupp ? Pdr_ManCountVariables(p, kStart) : Aig_ManRegNum(p->pAig) );
     fprintf( pFile, ".o 1\n" );
     fprintf( pFile, ".p %d\n", Count );
     // output flop names
@@ -386,7 +385,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
     {
         fprintf( pFile, ".ilb" );
         for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
-            if ( !fUseSupp || Vec_IntEntry( vFlopCounts, i ) )
+            if ( !p->pPars->fUseSupp || Vec_IntEntry( vFlopCounts, i ) )
                 fprintf( pFile, " %s", pNamesCi[Saig_ManPiNum(p->pAig) + i] );
         fprintf( pFile, "\n" );
         ABC_FREE( pNamesCi );
@@ -423,7 +422,6 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
 ***********************************************************************/
 Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p )
 {
-    int fUseSupp = 1;
     Vec_Str_t * vStr;
     Vec_Int_t * vFlopCounts;
     Vec_Ptr_t * vCubes;
@@ -438,7 +436,7 @@ Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p )
         vCubes = Vec_PtrDup( p->vInfCubes );
     Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
     // collect variable appearances
-    vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; 
+    vFlopCounts = p->pPars->fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; 
     // output cubes
     Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
     {
-- 
cgit v1.2.3