diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-09-28 16:27:39 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-09-28 16:27:39 -0700 |
| commit | 4f0f2e09f84b66c1ed9a842a71a09f2f1ec65588 (patch) | |
| tree | ecd646bd842662c7c4d165b3f2e7358c0d752c2b /src/proof/pdr/pdrInv.c | |
| parent | ca93730781ac2a6559e16a6203786073b1cbd514 (diff) | |
| download | abc-4f0f2e09f84b66c1ed9a842a71a09f2f1ec65588.tar.gz abc-4f0f2e09f84b66c1ed9a842a71a09f2f1ec65588.tar.bz2 abc-4f0f2e09f84b66c1ed9a842a71a09f2f1ec65588.zip | |
Adding flag 'pdr -e' to output only support variables in the invariant.
Diffstat (limited to 'src/proof/pdr/pdrInv.c')
| -rw-r--r-- | src/proof/pdr/pdrInv.c | 10 |
1 files changed, 4 insertions, 6 deletions
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 ) { |