diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-12-08 12:44:08 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-12-08 12:44:08 -0800 |
| commit | a68593c4f2b79b4adaf76dfe6b5dfc3bc63bb323 (patch) | |
| tree | 55f7c003ef35e737dfaba191e4c7814be91563bf | |
| parent | 8e5d771feb5e0914e4acecfaa942a60766882f4d (diff) | |
| download | abc-a68593c4f2b79b4adaf76dfe6b5dfc3bc63bb323.tar.gz abc-a68593c4f2b79b4adaf76dfe6b5dfc3bc63bb323.tar.bz2 abc-a68593c4f2b79b4adaf76dfe6b5dfc3bc63bb323.zip | |
Deriving CEX after phase/tempor/reparam.
| -rw-r--r-- | src/base/abci/abc.c | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 5d9dd107..e0bcb523 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -17972,8 +17972,7 @@ int Abc_CommandDarPhase( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } pCexNew = Abc_CexTransformPhase( pAbc->pCex, Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk), Abc_NtkLatchNum(pNtk) ); - Abc_CexFree( pAbc->pCex ); - pAbc->pCex = pCexNew; + Abc_FrameReplaceCex( pAbc, &pCexNew ); return 0; } if ( !Abc_NtkLatchNum(pNtk) ) @@ -21546,8 +21545,7 @@ int Abc_CommandTempor( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } pCexNew = Abc_CexTransformTempor( pAbc->pCex, Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk), Abc_NtkLatchNum(pNtk) ); - Abc_CexFree( pAbc->pCex ); - pAbc->pCex = pCexNew; + Abc_FrameReplaceCex( pAbc, &pCexNew ); return 0; } // modify the current network @@ -22492,8 +22490,8 @@ int Abc_CommandReconcile( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); extern Abc_Cex_t * Llb4_Nonlin4NormalizeCex( Aig_Man_t * pAigOrg, Aig_Man_t * pAigRpm, Abc_Cex_t * pCexRpm ); Abc_Cex_t * pCex; - Abc_Ntk_t * pNtk1, * pNtk2; - Aig_Man_t * pAig1, * pAig2; + Abc_Ntk_t * pNtk1 = NULL, * pNtk2 = NULL; + Aig_Man_t * pAig1 = NULL, * pAig2 = NULL; int c; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) @@ -22555,16 +22553,17 @@ int Abc_CommandReconcile( Abc_Frame_t * pAbc, int argc, char ** argv ) pCex = Llb4_Nonlin4NormalizeCex( pAig1, pAig2, pAbc->pCex ); Aig_ManStop( pAig1 ); Aig_ManStop( pAig2 ); - Abc_NtkDelete( pNtk2 ); + if ( pNtk2 ) Abc_NtkDelete( pNtk2 ); if ( pCex == NULL ) { Abc_Print( 1,"Counter-example computation has failed.\n" ); - Abc_NtkDelete( pNtk1 ); + if ( pNtk1 ) Abc_NtkDelete( pNtk1 ); return 1; } // replace the current network - Abc_FrameReplaceCurrentNetwork( pAbc, pNtk1 ); + if ( pNtk1 ) + Abc_FrameReplaceCurrentNetwork( pAbc, pNtk1 ); // update the counter-example pAbc->nFrames = pCex->iFrame; Abc_FrameReplaceCex( pAbc, &pCex ); |