diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-08-02 12:58:37 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-08-02 12:58:37 +0700 |
| commit | 49df91f071d6828113ded55f371e15d192304222 (patch) | |
| tree | 6d089abb35681ede68d8691adc6b39cd4092de05 /src/base/abci | |
| parent | 64f31f98bf5b317dc08f0e96bf1aa617053c918d (diff) | |
| download | abc-49df91f071d6828113ded55f371e15d192304222.tar.gz abc-49df91f071d6828113ded55f371e15d192304222.tar.bz2 abc-49df91f071d6828113ded55f371e15d192304222.zip | |
Several bug fixes.
Diffstat (limited to 'src/base/abci')
| -rw-r--r-- | src/base/abci/abcDar.c | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index ebeafa86..3b0cbb06 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1824,9 +1824,9 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars ) printf( "(timeout %d sec). ", pPars->nTimeOut ); else printf( "(conf limit %d). ", pPars->nConfLimit ); - if ( pNtk->vSeqModelVec ) - Vec_PtrFreeFree( pNtk->vSeqModelVec ); - pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL; +// if ( pNtk->vSeqModelVec ) +// Vec_PtrFreeFree( pNtk->vSeqModelVec ); +// pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL; } } else // if ( RetValue == 0 ) @@ -1838,7 +1838,17 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars ) } else { - printf( "All %d outputs are proved SAT. ", Saig_ManPoNum(pMan) - pMan->nConstrs ); + int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan); + if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 ) + printf( "All %d outputs are found to be SAT. ", nOutputs ); + else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs ) + printf( "None of the %d outputs is found to be SAT. ", nOutputs ); + else + printf( "Some outputs (%d out of %d) are proved SAT. ", + nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs ); + if ( pNtk->vSeqModelVec ) + Vec_PtrFreeFree( pNtk->vSeqModelVec ); + pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL; } } ABC_PRT( "Time", clock() - clk ); |