diff options
| author | Baruch Sterin <baruchs@gmail.com> | 2011-02-01 16:19:38 -0800 |
|---|---|---|
| committer | Baruch Sterin <baruchs@gmail.com> | 2011-02-01 16:19:38 -0800 |
| commit | 35e05b7e5a422c3c075711eba3b4329c35ac426f (patch) | |
| tree | 0594feba48403b8291f25d6bbf0df6610981fc62 /src/aig/saig/saigAbs.c | |
| parent | 3a41da37a28535aed93abc3b91130539624fb3ca (diff) | |
| parent | d4291dab37a647ac3d8d0f4e91e571bbb4e3553b (diff) | |
| download | abc-35e05b7e5a422c3c075711eba3b4329c35ac426f.tar.gz abc-35e05b7e5a422c3c075711eba3b4329c35ac426f.tar.bz2 abc-35e05b7e5a422c3c075711eba3b4329c35ac426f.zip | |
merge pyabc changes into mainline
Diffstat (limited to 'src/aig/saig/saigAbs.c')
| -rw-r--r-- | src/aig/saig/saigAbs.c | 26 |
1 files changed, 23 insertions, 3 deletions
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c index 194add25..938a66e2 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -22,6 +22,7 @@ #include "ssw.h" #include "fra.h" #include "bbr.h" +#include "pdr.h" ABC_NAMESPACE_IMPL_START @@ -173,15 +174,32 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo { extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames ); Vec_Int_t * vFlopsNew; - int i, Entry; + int i, Entry, RetValue; *piRetValue = -1; if ( fUseDprove && Aig_ManRegNum(pAbs) > 0 ) { +/* Fra_Sec_t SecPar, * pSecPar = &SecPar; - int RetValue; Fra_SecSetDefaultParams( pSecPar ); pSecPar->fVerbose = fVerbose; RetValue = Fra_FraigSec( pAbs, pSecPar, NULL ); +*/ + Abc_Cex_t * pCex = NULL; + Aig_Man_t * pAbsOrpos = Saig_ManDupOrpos( pAbs ); + Pdr_Par_t Pars, * pPars = &Pars; + Pdr_ManSetDefaultParams( pPars ); + pPars->nTimeOut = 10; + pPars->fVerbose = fVerbose; + if ( pPars->fVerbose ) + printf( "Running property directed reachability...\n" ); + RetValue = Pdr_ManSolve( pAbsOrpos, pPars, &pCex ); + if ( pCex ) + pCex->iPo = Ssw_SmlFindOutputCounterExample( pAbs, pCex ); + Aig_ManStop( pAbsOrpos ); + pAbs->pSeqModel = pCex; + if ( RetValue ) + *piRetValue = 1; + } else if ( fUseBdds && (Aig_ManRegNum(pAbs) > 0 && Aig_ManRegNum(pAbs) <= 80) ) { @@ -195,7 +213,9 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo pPars->fReorderImage = 1; pPars->fVerbose = fVerbose; pPars->fSilent = 0; - Aig_ManVerifyUsingBdds( pAbs, pPars ); + RetValue = Aig_ManVerifyUsingBdds( pAbs, pPars ); + if ( RetValue ) + *piRetValue = 1; } else { |