diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-04-25 12:35:05 -0500 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-04-25 12:35:05 -0500 |
| commit | 970200b932eb2999b57c8ab8348c4695c08eff6d (patch) | |
| tree | d94f67a12dd406232cbb539880a9f967b52cd34d /src/base | |
| parent | 3eae30a3c3f8799471821ec28f6bd993770f72d8 (diff) | |
| download | abc-970200b932eb2999b57c8ab8348c4695c08eff6d.tar.gz abc-970200b932eb2999b57c8ab8348c4695c08eff6d.tar.bz2 abc-970200b932eb2999b57c8ab8348c4695c08eff6d.zip | |
Made testcex reset the number of the PO that failed.
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/abci/abc.c | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 0e1d7b21..0988549a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -19822,9 +19822,14 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 ); Gia_Man_t * pGia = Gia_ManFromAigSimple( pAig ); - if ( !Gia_ManVerifyCex( pGia, pAbc->pCex, 0 ) ) +// if ( !Gia_ManVerifyCex( pGia, pAbc->pCex, 0 ) ) + int iPoOld = pAbc->pCex->iPo; + pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pGia, pAbc->pCex ); + if ( pAbc->pCex->iPo == -1 ) Abc_Print( 1, "Main AIG: The cex does not fail any outputs.\n" ); - else + else if ( iPoOld != pAbc->pCex->iPo ) + Abc_Print( 1, "Main AIG: The cex refined PO %d instead of PO %d.\n", pAbc->pCex->iPo, iPoOld ); + else Abc_Print( 1, "Main AIG: The cex is correct.\n" ); Gia_ManStop( pGia ); Aig_ManStop( pAig ); @@ -19841,9 +19846,14 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "And AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Gia_ManPoNum(pAbc->pGia), pAbc->pCex->iPo ); else { - if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) ) +// if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) ) + int iPoOld = pAbc->pCex->iPo; + pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pAbc->pGia, pAbc->pCex ); + if ( pAbc->pCex->iPo == -1 ) Abc_Print( 1, "And AIG: The cex does not fail any outputs.\n" ); - else + else if ( iPoOld != pAbc->pCex->iPo ) + Abc_Print( 1, "And AIG: The cex refined PO %d instead of PO %d.\n", pAbc->pCex->iPo, iPoOld ); + else Abc_Print( 1, "And AIG: The cex is correct.\n" ); } return 0; |