diff options
author | Mathias Soeken <mathias.soeken@gmail.com> | 2016-09-29 22:10:16 -0700 |
---|---|---|
committer | Mathias Soeken <mathias.soeken@gmail.com> | 2016-09-29 22:10:16 -0700 |
commit | f5be1575832e2028eed0942aa69315870532669e (patch) | |
tree | 8888abf063a2bf70829dcc840c9add39a1d7d9b0 /src/proof/pdr | |
parent | e601df9deac339b7404ef366bf10dc0acad8ad3a (diff) | |
parent | 9a35f82d5fd396f04a0baaa50b390281c4673172 (diff) | |
download | abc-f5be1575832e2028eed0942aa69315870532669e.tar.gz abc-f5be1575832e2028eed0942aa69315870532669e.tar.bz2 abc-f5be1575832e2028eed0942aa69315870532669e.zip |
Merged alanmi/abc into default
Diffstat (limited to 'src/proof/pdr')
-rw-r--r-- | src/proof/pdr/pdr.h | 1 | ||||
-rw-r--r-- | src/proof/pdr/pdrCore.c | 1 | ||||
-rw-r--r-- | src/proof/pdr/pdrInv.c | 10 |
3 files changed, 6 insertions, 6 deletions
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 ) { |