diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-11-14 20:50:18 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-11-14 20:50:18 -0800 |
| commit | 2eb2402b01541ed672ac2b7e742f1e1aa38542e8 (patch) | |
| tree | dc989cb3689988c4ab5f6128d4aff5f626f95735 /src/sat/bmc | |
| parent | 9173799c9672fd8f56d55c05a989c573e5629996 (diff) | |
| download | abc-2eb2402b01541ed672ac2b7e742f1e1aa38542e8.tar.gz abc-2eb2402b01541ed672ac2b7e742f1e1aa38542e8.tar.bz2 abc-2eb2402b01541ed672ac2b7e742f1e1aa38542e8.zip | |
Added command 'cexcut' and 'cexmerge'.
Diffstat (limited to 'src/sat/bmc')
| -rw-r--r-- | src/sat/bmc/bmc.h | 4 | ||||
| -rw-r--r-- | src/sat/bmc/bmcCexCut.c | 23 |
2 files changed, 15 insertions, 12 deletions
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 5d789dcb..45caa3c5 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -75,8 +75,8 @@ extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFra extern void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ); extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ); /*=== bmcCexCut.c ==========================================================*/ -extern Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose ); -extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose ); +extern Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fVerbose ); +extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fVerbose ); /*=== bmcCexMin.c ==========================================================*/ extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex ); diff --git a/src/sat/bmc/bmcCexCut.c b/src/sat/bmc/bmcCexCut.c index bbb1bc73..98786620 100644 --- a/src/sat/bmc/bmcCexCut.c +++ b/src/sat/bmc/bmcCexCut.c @@ -43,7 +43,7 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose ) +Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fVerbose ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj, * pObjRo, * pObjRi; @@ -141,13 +141,16 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); - // create new GIA - pNew = Gia_ManDupWithNewPo( p, pTemp = pNew ); - Gia_ManStop( pTemp ); + if ( !fCombOnly ) + { + // create new GIA + pNew = Gia_ManDupWithNewPo( p, pTemp = pNew ); + Gia_ManStop( pTemp ); - // create new initial state - pNew = Gia_ManDupFlip( pTemp = pNew, Vec_BitArray(vInitNew) ); - Gia_ManStop( pTemp ); + // create new initial state + pNew = Gia_ManDupFlip( pTemp = pNew, Vec_BitArray(vInitNew) ); + Gia_ManStop( pTemp ); + } Vec_BitFree( vInitNew ); return pNew; @@ -164,18 +167,18 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in SeeAlso [] ***********************************************************************/ -Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose ) +Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fVerbose ) { Aig_Man_t * pAig; Gia_Man_t * pGia, * pRes; pGia = Gia_ManFromAigSimple( p ); if ( !Gia_ManVerifyCex( pGia, pCex, 0 ) ) { - Abc_Print( 1, "Current CEX does not fail AIG \"%s\".\n", p->pName ); + Abc_Print( 1, "Current CEX does not fail AIG \"%s\".\n", p->pName ); Gia_ManStop( pGia ); return NULL; } - pRes = Bmc_GiaTargetStates( pGia, pCex, iFrBeg, iFrEnd, fVerbose ); + pRes = Bmc_GiaTargetStates( pGia, pCex, iFrBeg, iFrEnd, fCombOnly, fVerbose ); pAig = Gia_ManToAigSimple( pRes ); Gia_ManStop( pGia ); Gia_ManStop( pRes ); |