diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-08-04 11:31:31 +0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-08-04 11:31:31 +0800 |
| commit | fbb12a06f20e40eea8d8aa45982d1f9f1cdb9809 (patch) | |
| tree | 849fe7a8e8d4a066f6aae1972e872002f663b302 /src/aig/saig | |
| parent | 825b0b5ee3b51f09526c641ac9b030226ec09ca8 (diff) | |
| download | abc-fbb12a06f20e40eea8d8aa45982d1f9f1cdb9809.tar.gz abc-fbb12a06f20e40eea8d8aa45982d1f9f1cdb9809.tar.bz2 abc-fbb12a06f20e40eea8d8aa45982d1f9f1cdb9809.zip | |
Bug fix in PBA.
Diffstat (limited to 'src/aig/saig')
| -rw-r--r-- | src/aig/saig/saigAbsPba.c | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c index 3f8fb222..21d92f57 100644 --- a/src/aig/saig/saigAbsPba.c +++ b/src/aig/saig/saigAbsPba.c @@ -201,7 +201,7 @@ Abc_Cex_t * Saig_ManPbaDeriveCex( Aig_Man_t * pAig, sat_solver * pSat, Cnf_Dat_t ***********************************************************************/ Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int nConfLimit, int fVerbose ) { - Vec_Int_t * vFlops, * vMapVar2FF, * vAssumps, * vPiVarMap; + Vec_Int_t * vFlops = NULL, * vMapVar2FF, * vAssumps, * vPiVarMap; Aig_Man_t * pFrames; sat_solver * pSat; Cnf_Dat_t * pCnf; @@ -248,6 +248,8 @@ Abc_PrintTime( 1, "Solving", clock() - clk ); { if ( RetValue == l_True ) { + printf( "Saig_ManPerformPba(): The eproblem is SAT. Abstraction refinement is still not enabled.\n" ); +/* Vec_Int_t * vAbsFfsToAdd; ABC_FREE( pAig->pSeqModel ); pAig->pSeqModel = Saig_ManPbaDeriveCex( pAig, pSat, pCnf, nFrames, vPiVarMap ); @@ -263,7 +265,8 @@ Abc_PrintTime( 1, "Solving", clock() - clk ); printf( "Adding %d registers to the abstraction. ", Vec_IntSize(vAbsFfsToAdd) ); Abc_PrintTime( 0, "Time", clock() - clk ); } - return vAbsFfsToAdd; + vFlops = vAbsFfsToAdd; +*/ } else { |