From 71cbf17e7f0352556af12ccccf9051e02c773e58 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 13 Feb 2011 17:46:48 -0800 Subject: Unified the use of counter-examples in three packages. --- src/base/abc/abc.h | 1 + src/base/abc/abcNtk.c | 4 +--- src/base/abci/abc.c | 7 +++---- src/base/abci/abcDar.c | 25 ++++++++++++------------- src/base/abci/abcDprove2.c | 2 +- src/base/abci/abcLog.c | 2 +- src/base/abci/abcVerify.c | 4 ++-- src/base/cmd/cmdPlugin.c | 10 ++++------ 8 files changed, 25 insertions(+), 30 deletions(-) (limited to 'src/base') diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 3357ff46..c1c6a91c 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -38,6 +38,7 @@ #include "extra.h" #include "stmm.h" #include "nm.h" +#include "utilCex.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index 821cca4c..d58e9c72 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -131,9 +131,7 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_ if ( pNtk->vOnehots ) pNtkNew->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots ); if ( pNtk->pSeqModel ) - { - pNtkNew->pSeqModel = Gia_ManDupCounterExample( pNtk->pSeqModel, Abc_NtkLatchNum(pNtk) ); - } + pNtkNew->pSeqModel = Abc_CexDup( pNtk->pSeqModel, Abc_NtkLatchNum(pNtk) ); // check that the CI/CO/latches are copied correctly assert( Abc_NtkCiNum(pNtk) == Abc_NtkCiNum(pNtkNew) ); assert( Abc_NtkCoNum(pNtk) == Abc_NtkCoNum(pNtkNew) ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 7ee6769e..4b95b900 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -17580,7 +17580,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pSimInfo[0] != 1 ) Abc_Print( 1, "ERROR in Abc_NtkMiterSat(): Generated counter example is invalid.\n" ); ABC_FREE( pSimInfo ); - pAbc->pCex = Gia_ManCreateFromComb( 0, Abc_NtkPiNum(pNtk), 0, pNtk->pModel ); + pAbc->pCex = Abc_CexCreate( 0, Abc_NtkPiNum(pNtk), pNtk->pModel, 0, 0, 0 ); } pAbc->Status = RetValue; if ( RetValue == -1 ) @@ -19840,8 +19840,7 @@ 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_ManVerifyCounterExample( pGia, pAbc->pCex, 0 ) ) -// if ( !Ssw_SmlRunCounterExample( pAig, pAbc->pCex ) ) + if ( !Gia_ManVerifyCex( pGia, pAbc->pCex, 0 ) ) Abc_Print( 1, "Main AIG: The cex does not fail any outputs.\n" ); else Abc_Print( 1, "Main AIG: The cex is correct.\n" ); @@ -19860,7 +19859,7 @@ 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_ManVerifyCounterExample( pAbc->pGia, pAbc->pCex, 0 ) ) + if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) ) Abc_Print( 1, "And AIG: The cex does not fail any outputs.\n" ); else Abc_Print( 1, "And AIG: The cex is correct.\n" ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index a6fa9ce6..225bf1be 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -21,7 +21,6 @@ #include "abc.h" #include "main.h" #include "giaAig.h" -#include "saig.h" #include "dar.h" #include "cnf.h" #include "fra.h" @@ -1790,7 +1789,7 @@ ABC_PRT( "Time", clock() - clk ); // verify counter-example if ( pNtk->pSeqModel ) { - status = Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel ); + status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel ); if ( status == 0 ) printf( "Abc_NtkDarBmc(): Counter-example verification has FAILED.\n" ); } @@ -1857,7 +1856,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars ) ABC_PRT( "Time", clock() - clk ); if ( pNtk->pSeqModel ) { - status = Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel ); + status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel ); if ( status == 0 ) printf( "Abc_NtkDarBmc3(): Counter-example verification has FAILED.\n" ); } @@ -1902,7 +1901,7 @@ int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars, Aig_Man pTemp->pSeqModel = NULL; RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0 ); if ( pTemp->pData ) - pTemp->pSeqModel = Gia_ManCreateFromComb( Aig_ManRegNum(pMan), Saig_ManPiNum(pMan), i, (int *)pTemp->pData ); + pTemp->pSeqModel = Abc_CexCreate( Aig_ManRegNum(pMan), Saig_ManPiNum(pMan), (int *)pTemp->pData, 0, i, 1 ); // pNtk->pModel = pTemp->pData, pTemp->pData = NULL; } else @@ -2150,7 +2149,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar ) { Abc_Cex_t * pCex = pNtk->pSeqModel; printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).\n", pCex->iPo, pCex->iFrame ); - if ( !Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel ) ) + if ( !Saig_ManVerifyCex( pMan, pNtk->pSeqModel ) ) printf( "Abc_NtkDarProve(): Counter-example verification has FAILED.\n" ); } } @@ -2274,7 +2273,7 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) Aig_Man_t * pTemp = Saig_ManDupOrpos( pMan ); RetValue = Pdr_ManSolve( pTemp, pPars, ppCex ); if ( RetValue == 0 ) - (*ppCex)->iPo = Ssw_SmlFindOutputCounterExample( pMan, *ppCex ); + (*ppCex)->iPo = Saig_ManFindFailedPoCex( pMan, *ppCex ); Aig_ManStop( pTemp ); } else @@ -2290,7 +2289,7 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) assert( 0 ); ABC_PRT( "Time", clock() - clk ); - if ( *ppCex && !Ssw_SmlRunCounterExample( pMan, *ppCex ) ) + if ( *ppCex && !Saig_ManVerifyCex( pMan, *ppCex ) ) printf( "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" ); Aig_ManStop( pMan ); return RetValue; @@ -2710,7 +2709,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in { printf( "Simulation iterated %d times with %d words asserted output %d in frame %d. ", nFrames, nWords, pCex->iPo, pCex->iFrame ); - status = Ssw_SmlRunCounterExample( pMan, pCex ); + status = Saig_ManVerifyCex( pMan, pCex ); if ( status == 0 ) printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" ); } @@ -2737,7 +2736,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in { printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", nFrames, nWords, pCex->iPo, pCex->iFrame ); - status = Ssw_SmlRunCounterExample( pMan, pCex ); + status = Saig_ManVerifyCex( pMan, pCex ); if ( status == 0 ) printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" ); } @@ -2767,7 +2766,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in { printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", nFrames, nWords, pCex->iPo, pCex->iFrame ); - status = Ssw_SmlRunCounterExample( pMan, pCex ); + status = Saig_ManVerifyCex( pMan, pCex ); if ( status == 0 ) printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" ); } @@ -2798,7 +2797,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in { printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", nFrames, nWords, pGia->pCexSeq->iPo, pGia->pCexSeq->iFrame ); - status = Ssw_SmlRunCounterExample( pMan, pGia->pCexSeq ); + status = Saig_ManVerifyCex( pMan, pGia->pCexSeq ); if ( status == 0 ) printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" ); } @@ -2825,7 +2824,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in { printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", nFrames, nWords, pCex->iPo, pCex->iFrame ); - status = Ssw_SmlRunCounterExample( pMan, pCex ); + status = Saig_ManVerifyCex( pMan, pCex ); if ( status == 0 ) printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" ); } @@ -2847,7 +2846,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in { printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", nFrames, nWords, pCex->iPo, pCex->iFrame ); - status = Ssw_SmlRunCounterExample( pMan, pCex ); + status = Saig_ManVerifyCex( pMan, pCex ); if ( status == 0 ) printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" ); } diff --git a/src/base/abci/abcDprove2.c b/src/base/abci/abcDprove2.c index 7d432612..b9b2c10a 100644 --- a/src/base/abci/abcDprove2.c +++ b/src/base/abci/abcDprove2.c @@ -384,7 +384,7 @@ finish: // verify counter-example if ( pNtk->pSeqModel ) { - int status = Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel ); + int status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel ); if ( status == 0 ) printf( "Abc_NtkDarBmc(): Counter-example verification has FAILED.\n" ); } diff --git a/src/base/abci/abcLog.c b/src/base/abci/abcLog.c index 071d7943..7eece0e3 100644 --- a/src/base/abci/abcLog.c +++ b/src/base/abci/abcLog.c @@ -197,7 +197,7 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames ) printf( "Incorrect number of bits.\n" ); return -1; } - pCex = Gia_ManAllocCounterExample( nRegs, (Vec_IntSize(vNums)-nRegs)/nFrames, nFrames ); + pCex = Abc_CexAlloc( nRegs, (Vec_IntSize(vNums)-nRegs)/nFrames, nFrames ); pCex->iPo = iPo; pCex->iFrame = nFrames - 1; assert( Vec_IntSize(vNums) == pCex->nBits ); diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 58b8fbb8..acdfcd93 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -24,6 +24,7 @@ #include "fraig.h" #include "sim.h" #include "aig.h" +#include "saig.h" #include "gia.h" #include "ssw.h" @@ -1029,7 +1030,6 @@ void Abc_NtkSimulteBuggyMiter( Abc_Ntk_t * pNtk ) int Abc_NtkIsTrueCex( Abc_Ntk_t * pNtk, Abc_Cex_t * pCex ) { extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); -// extern int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ); Aig_Man_t * pMan; int status, fStrashed = 0; if ( !Abc_NtkIsStrash(pNtk) ) @@ -1040,7 +1040,7 @@ int Abc_NtkIsTrueCex( Abc_Ntk_t * pNtk, Abc_Cex_t * pCex ) pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan ) { - status = Ssw_SmlRunCounterExample( pMan, pCex ); + status = Saig_ManVerifyCex( pMan, pCex ); Aig_ManStop( pMan ); } if ( fStrashed ) diff --git a/src/base/cmd/cmdPlugin.c b/src/base/cmd/cmdPlugin.c index 116687c7..1e2b7712 100644 --- a/src/base/cmd/cmdPlugin.c +++ b/src/base/cmd/cmdPlugin.c @@ -484,20 +484,18 @@ int Cmd_CommandAbcPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "Counter example has a wrong length.\n" ); else { - extern int Gia_ManVerifyCounterExampleAllOuts( Gia_Man_t * pAig, Abc_Cex_t * p ); - Abc_Print( 1, "Problem is satisfiable. Found counter-example in frame %d. ", nFrames-1 ); Abc_PrintTime( 1, "Time", clk ); ABC_FREE( pAbc->pCex ); - pAbc->pCex = Gia_ManDeriveCexFromArray( pAbc->pGia, vCex, 0, nFrames-1 ); + pAbc->pCex = Abc_CexCreate( Gia_ManRegNum(pAbc->pGia), Gia_ManPiNum(pAbc->pGia), Vec_IntArray(vCex), nFrames-1, 0, 0 ); -// Gia_ManPrintCex( pAbc->pCex ); +// Abc_CexPrint( pAbc->pCex ); -// if ( !Gia_ManVerifyCounterExample( pAbc->pGia, pAbc->pCex, 0 ) ) +// if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) ) // Abc_Print( 1, "Generated counter-example is INVALID.\n" ); // remporary work-around to detect the output number - October 18, 2010 - pAbc->pCex->iPo = Gia_ManVerifyCounterExampleAllOuts( pAbc->pGia, pAbc->pCex ); + pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pAbc->pGia, pAbc->pCex ); if ( pAbc->pCex->iPo == -1 ) { Abc_Print( 1, "Generated counter-example is INVALID.\n" ); -- cgit v1.2.3