diff options
42 files changed, 270 insertions, 818 deletions
@@ -2359,6 +2359,14 @@ SOURCE=.\src\misc\util\util_hack.h # End Source File # Begin Source File +SOURCE=.\src\misc\util\utilCex.c +# End Source File +# Begin Source File + +SOURCE=.\src\misc\util\utilCex.h +# End Source File +# Begin Source File + SOURCE=.\src\misc\util\utilFile.c # End Source File # Begin Source File @@ -4118,10 +4126,6 @@ SOURCE=.\src\aig\llb\llb3Nonlin.c SOURCE=.\src\aig\llb\llbInt.h # End Source File # End Group -# Begin Group "bll" - -# PROP Default_Filter "" -# End Group # End Group # End Group # Begin Group "Header Files" diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index ddedb4e2..f667d4e3 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -33,6 +33,7 @@ #include <time.h> #include "vec.h" +#include "utilCex.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// diff --git a/src/aig/bbr/bbrCex.c b/src/aig/bbr/bbrCex.c index 8f99ea3c..4a1a1d67 100644 --- a/src/aig/bbr/bbrCex.c +++ b/src/aig/bbr/bbrCex.c @@ -19,7 +19,6 @@ ***********************************************************************/ #include "bbr.h" -#include "ssw.h" ABC_NAMESPACE_IMPL_START @@ -60,7 +59,7 @@ Abc_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, //printf( "\nDeriving counter-example.\n" ); // allocate room for the counter-example - pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(p), Saig_ManPiNum(p), Vec_PtrSize(vOnionRings)+1 ); + pCex = Abc_CexAlloc( Saig_ManRegNum(p), Saig_ManPiNum(p), Vec_PtrSize(vOnionRings)+1 ); pCex->iFrame = Vec_PtrSize(vOnionRings); pCex->iPo = iOutput; nPiOffset = Saig_ManRegNum(p) + Saig_ManPiNum(p) * Vec_PtrSize(vOnionRings); @@ -153,7 +152,7 @@ Abc_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, // verify the counter example if ( Vec_PtrSize(vOnionRings) < 1000 ) { - RetValue = Ssw_SmlRunCounterExample( p, pCex ); + RetValue = Saig_ManVerifyCex( p, pCex ); if ( RetValue == 0 && !fSilent ) printf( "Aig_ManVerifyUsingBdds(): Counter-example verification has FAILED.\n" ); } diff --git a/src/aig/bbr/bbrReach.c b/src/aig/bbr/bbrReach.c index c2433d45..ef355992 100644 --- a/src/aig/bbr/bbrReach.c +++ b/src/aig/bbr/bbrReach.c @@ -19,7 +19,6 @@ ***********************************************************************/ #include "bbr.h" -#include "ssw.h" ABC_NAMESPACE_IMPL_START @@ -568,7 +567,7 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, Saig_ParBbr_t * pPars ) else Vec_IntPush( vInputMap, -1 ); // create new pattern - pCexNew = Ssw_SmlAllocCounterExample( Saig_ManRegNum(pInit), Saig_ManPiNum(pInit), pCexOld->iFrame+1 ); + pCexNew = Abc_CexAlloc( Saig_ManRegNum(pInit), Saig_ManPiNum(pInit), pCexOld->iFrame+1 ); pCexNew->iFrame = pCexOld->iFrame; pCexNew->iPo = pCexOld->iPo; // copy the bit-data diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c index 0859a9ad..9fd8a03f 100644 --- a/src/aig/cec/cecCec.c +++ b/src/aig/cec/cecCec.c @@ -164,7 +164,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) { if ( p->pCexComb != NULL ) { - if ( p->pCexComb && !Gia_ManVerifyCounterExample( p, p->pCexComb, 1 ) ) + if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) ) Abc_Print( 1, "Counter-example simulation has failed.\n" ); Abc_Print( 1, "Networks are NOT EQUIVALENT. " ); Abc_PrintTime( 1, "Time", clock() - clk ); @@ -220,7 +220,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) fflush( stdout ); RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose, &pPars->iOutFail ); p->pCexComb = pNew->pCexComb; pNew->pCexComb = NULL; - if ( p->pCexComb && !Gia_ManVerifyCounterExample( p, p->pCexComb, 1 ) ) + if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) ) Abc_Print( 1, "Counter-example simulation has failed.\n" ); Gia_ManStop( pNew ); return RetValue; diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c index b91e8523..c255d50e 100644 --- a/src/aig/cec/cecSeq.c +++ b/src/aig/cec/cecSeq.c @@ -338,7 +338,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) } Gia_ManRandom( 1 ); // prepare starting pattern - pState = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), 0, 0 ); + pState = Abc_CexAlloc( Gia_ManRegNum(pAig), 0, 0 ); pState->iFrame = -1; pState->iPo = -1; // prepare SAT solving @@ -359,7 +359,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) Abc_Print( 1, "Cec_ManSeqSemiformal: There are only trivial equiv candidates left (PO drivers). Quitting.\n" ); break; } -// Gia_ManPrintCounterExample( pState ); +// Abc_CexPrint( pState ); // derive speculatively reduced model // pSrm = Gia_ManSpecReduceInit( pAig, pState, pPars->nFrames, pPars->fDualOut ); pSrm = Gia_ManSpecReduceInitFrames( pAig, pState, pPars->nFrames, &nFramesReal, pPars->fDualOut, pPars->nMinOutputs ); diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index aee38d08..a0073ca1 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -376,12 +376,6 @@ extern Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int extern Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords ); extern Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p ); extern Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ); -extern void Fra_SmlFreeCounterExample( Abc_Cex_t * p ); -extern Abc_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ); -extern int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ); -extern int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Abc_Cex_t * p ); -extern Abc_Cex_t * Fra_SmlSimpleCounterExample( Aig_Man_t * pAig, int * pModel, int iFrame, int iPo ); - ABC_NAMESPACE_HEADER_END diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c index ae9e4bc5..3907fcdd 100644 --- a/src/aig/fra/fraBmc.c +++ b/src/aig/fra/fraBmc.c @@ -417,7 +417,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew clk = clock(); iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFrames ); if ( iOutput >= 0 ) - pAig->pSeqModel = Fra_SmlTrivCounterExample( pAig, iOutput ); + pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig), iOutput ); else { pBmc->pAigFraig = Fra_FraigEquivence( pBmc->pAigFrames, nBTLimit, 1 ); @@ -428,7 +428,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew ABC_FREE( pBmc->pAigFraig->pData ); } else if ( iOutput >= 0 ) - pAig->pSeqModel = Fra_SmlTrivCounterExample( pAig, iOutput ); + pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig), iOutput ); } if ( fVerbose ) { diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 7608791f..4b893cb2 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -203,14 +203,14 @@ clk = clock(); if ( pTemp->pSeqModel ) { - if ( !Ssw_SmlRunCounterExample( pTemp, pTemp->pSeqModel ) ) + if ( !Saig_ManVerifyCex( pTemp, pTemp->pSeqModel ) ) printf( "Fra_FraigSec(): Counter-example verification has FAILED.\n" ); if ( Saig_ManPiNum(p) != Saig_ManPiNum(pTemp) ) printf( "The counter-example is invalid because of phase abstraction.\n" ); else { ABC_FREE( p->pSeqModel ); - p->pSeqModel = Ssw_SmlDupCounterExample( pTemp->pSeqModel, Aig_ManRegNum(p) ); + p->pSeqModel = Abc_CexDup( pTemp->pSeqModel, Aig_ManRegNum(p) ); ABC_FREE( pTemp->pSeqModel ); } } @@ -443,7 +443,7 @@ ABC_PRT( "Time", clock() - clk ); else { ABC_FREE( p->pSeqModel ); - p->pSeqModel = Ssw_SmlDupCounterExample( pNew->pSeqModel, Aig_ManRegNum(p) ); + p->pSeqModel = Abc_CexDup( pNew->pSeqModel, Aig_ManRegNum(p) ); ABC_FREE( pNew->pSeqModel ); } @@ -505,7 +505,7 @@ clk = clock(); RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &Depth ); if ( pTemp->pSeqModel ) { - pCex = p->pSeqModel = Ssw_SmlDupCounterExample( pTemp->pSeqModel, Aig_ManRegNum(p) ); + pCex = p->pSeqModel = Abc_CexDup( pTemp->pSeqModel, Aig_ManRegNum(p) ); pCex->iPo = i; Aig_ManStop( pTemp ); break; @@ -548,7 +548,7 @@ clk = clock(); { Abc_Cex_t * pCex; pCex = pNew->pSeqModel = pNewOrpos->pSeqModel; pNewOrpos->pSeqModel = NULL; - pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pNew->pSeqModel ); + pCex->iPo = Saig_ManFindFailedPoCex( pNew, pNew->pSeqModel ); } Aig_ManStop( pNewOrpos ); } @@ -598,7 +598,7 @@ ABC_PRT( "Time", clock() - clk ); printf( "Running property directed reachability...\n" ); RetValue = Pdr_ManSolve( pNewOrpos, pPars, &pCex ); if ( pCex ) - pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pCex ); + pCex->iPo = Saig_ManFindFailedPoCex( pNew, pCex ); Aig_ManStop( pNewOrpos ); pNew->pSeqModel = pCex; } @@ -665,7 +665,7 @@ ABC_PRT( "Time", clock() - clkTotal ); else { ABC_FREE( p->pSeqModel ); - p->pSeqModel = Ssw_SmlDupCounterExample( pNew->pSeqModel, Aig_ManRegNum(p) ); + p->pSeqModel = Abc_CexDup( pNew->pSeqModel, Aig_ManRegNum(p) ); ABC_FREE( pNew->pSeqModel ); } } diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index 25c30989..37620a16 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "fra.h" +#include "saig.h" ABC_NAMESPACE_IMPL_START @@ -879,45 +880,6 @@ Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW /**Function************************************************************* - Synopsis [Allocates a counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Fra_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames ) -{ - Abc_Cex_t * pCex; - int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames ); - pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); - memset( pCex, 0, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); - pCex->nRegs = nRegs; - pCex->nPis = nRealPis; - pCex->nBits = nRegs + nRealPis * nFrames; - return pCex; -} - -/**Function************************************************************* - - Synopsis [Frees the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fra_SmlFreeCounterExample( Abc_Cex_t * pCex ) -{ - ABC_FREE( pCex ); -} - -/**Function************************************************************* - Synopsis [Creates sequential counter-example from the simulation info.] Description [] @@ -960,7 +922,7 @@ Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p ) assert( iBit < 32 * p->nWordsFrame ); // allocate the counter example - pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 ); + pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 ); pCex->iPo = iPo; pCex->iFrame = iFrame; @@ -981,10 +943,10 @@ Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p ) } } // verify the counter example - if ( !Fra_SmlRunCounterExample( p->pAig, pCex ) ) + if ( !Saig_ManVerifyCex( p->pAig, pCex ) ) { printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" ); - Fra_SmlFreeCounterExample( pCex ); + Abc_CexFree( pCex ); pCex = NULL; } return pCex; @@ -1026,7 +988,7 @@ Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, in } assert( iPo >= 0 ); // allocate the counter example - pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 ); + pCex = Abc_CexAlloc( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 ); pCex->iPo = iPo; pCex->iFrame = iFrame; @@ -1040,186 +1002,16 @@ Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, in } // verify the counter example - if ( !Fra_SmlRunCounterExample( pAig, pCex ) ) + if ( !Saig_ManVerifyCex( pAig, pCex ) ) { printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" ); - Fra_SmlFreeCounterExample( pCex ); + Abc_CexFree( pCex ); pCex = NULL; } return pCex; } -/**Function************************************************************* - - Synopsis [Make the trivial counter-example for the trivially asserted output.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ) -{ - Abc_Cex_t * pCex; - int nTruePis, nTruePos, iPo, iFrame; - assert( Aig_ManRegNum(pAig) > 0 ); - nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig); - nTruePos = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig); - iPo = iFrameOut % nTruePos; - iFrame = iFrameOut / nTruePos; - // allocate the counter example - pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 ); - pCex->iPo = iPo; - pCex->iFrame = iFrame; - return pCex; -} - -/**Function************************************************************* - - Synopsis [Resimulates the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ) -{ - Fra_Sml_t * pSml; - Aig_Obj_t * pObj; - int RetValue, i, k, iBit; - assert( Aig_ManRegNum(pAig) > 0 ); - assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) ); - // start a new sequential simulator - pSml = Fra_SmlStart( pAig, 0, p->iFrame+1, 1 ); - // assign simulation info for the registers - iBit = 0; - Aig_ManForEachLoSeq( pAig, pObj, i ) - Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 ); - // assign simulation info for the primary inputs - for ( i = 0; i <= p->iFrame; i++ ) - Aig_ManForEachPiSeq( pAig, pObj, k ) - Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i ); - assert( iBit == p->nBits ); - // run random simulation - Fra_SmlSimulateOne( pSml ); - // check if the given output has failed - RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) ); - Fra_SmlStop( pSml ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Make the trivial counter-example for the trivially asserted output.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Fra_SmlSimpleCounterExample( Aig_Man_t * pAig, int * pModel, int iFrame, int iPo ) -{ - Abc_Cex_t * pCex; - int iBit; - pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(pAig), Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), iFrame + 1 ); - pCex->iPo = iPo; - pCex->iFrame = iFrame; - for ( iBit = Aig_ManRegNum(pAig); iBit < pCex->nBits; iBit++ ) - if ( pModel[iBit-Aig_ManRegNum(pAig)] ) - Aig_InfoSetBit( pCex->pData, iBit ); -/* - if ( !Fra_SmlRunCounterExample( pAig, pCex ) ) - { - printf( "Fra_SmlSimpleCounterExample(): Counter-example is invalid.\n" ); -// Fra_SmlFreeCounterExample( pCex ); -// pCex = NULL; - } -*/ - return pCex; -} - -/**Function************************************************************* - - Synopsis [Resimulates the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Abc_Cex_t * p ) -{ - Fra_Sml_t * pSml; - Aig_Obj_t * pObj; - int RetValue, i, k, iBit; - unsigned * pSims; - assert( Aig_ManRegNum(pAig) > 0 ); - assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) ); - // start a new sequential simulator - pSml = Fra_SmlStart( pAig, 0, p->iFrame+1, 1 ); - // assign simulation info for the registers - iBit = 0; - Aig_ManForEachLoSeq( pAig, pObj, i ) -// Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 ); - Fra_SmlAssignConst( pSml, pObj, 0, 0 ); - // assign simulation info for the primary inputs - iBit = p->nRegs; - for ( i = 0; i <= p->iFrame; i++ ) - Aig_ManForEachPiSeq( pAig, pObj, k ) - Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i ); - assert( iBit == p->nBits ); - // run random simulation - Fra_SmlSimulateOne( pSml ); - // check if the given output has failed - RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) ); - - // write the output file - for ( i = 0; i <= p->iFrame; i++ ) - { -/* - Aig_ManForEachLoSeq( pAig, pObj, k ) - { - pSims = Fra_ObjSim(pSml, pObj->Id); - fprintf( pFile, "%d", (int)(pSims[i] != 0) ); - } - fprintf( pFile, " " ); -*/ - Aig_ManForEachPiSeq( pAig, pObj, k ) - { - pSims = Fra_ObjSim(pSml, pObj->Id); - fprintf( pFile, "%d", (int)(pSims[i] != 0) ); - } -/* - fprintf( pFile, " " ); - Aig_ManForEachPoSeq( pAig, pObj, k ) - { - pSims = Fra_ObjSim(pSml, pObj->Id); - fprintf( pFile, "%d", (int)(pSims[i] != 0) ); - } - fprintf( pFile, " " ); - Aig_ManForEachLiSeq( pAig, pObj, k ) - { - pSims = Fra_ObjSim(pSml, pObj->Id); - fprintf( pFile, "%d", (int)(pSims[i] != 0) ); - } -*/ - fprintf( pFile, "\n" ); - } - - Fra_SmlStop( pSml ); - return RetValue; -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/fsim/fsimSim.c b/src/aig/fsim/fsimSim.c index 2da7db15..56aeab2f 100644 --- a/src/aig/fsim/fsimSim.c +++ b/src/aig/fsim/fsimSim.c @@ -434,7 +434,7 @@ Abc_Cex_t * Fsim_ManGenerateCounter( Aig_Man_t * pAig, int iFrame, int iOut, int Abc_Cex_t * p; unsigned * pData; int f, i, w, iPioId, Counter; - p = Ssw_SmlAllocCounterExample( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 ); + p = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 ); p->iFrame = iFrame; p->iPo = iOut; // fill in the binary data diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index e3546686..b2f039a7 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -33,6 +33,7 @@ #include <time.h> #include "vec.h" +#include "utilCex.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -788,17 +789,13 @@ extern Vec_Int_t * Gia_ManCollectPoIds( Gia_Man_t * p ); extern int Gia_ObjIsMuxType( Gia_Obj_t * pNode ); extern int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ppFan0, Gia_Obj_t ** ppFan1 ); extern Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE ); -extern Abc_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames ); -extern Abc_Cex_t * Gia_ManDeriveCexFromArray( Gia_Man_t * pAig, Vec_Int_t * vValues, int nSkip, int iFrame ); -extern Abc_Cex_t * Gia_ManCreateFromComb( int nRegs, int nRealPis, int iPo, int * pModel ); -extern Abc_Cex_t * Gia_ManDupCounterExample( Abc_Cex_t * p, int nRegsNew ); -extern int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ); -extern void Gia_ManPrintCounterExample( Abc_Cex_t * p ); extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode ); extern int Gia_ManHasChoices( Gia_Man_t * p ); extern int Gia_ManHasDangling( Gia_Man_t * p ); extern Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p ); extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj ); +extern int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ); +extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p ); /*=== giaCTas.c ===========================================================*/ typedef struct Tas_Man_t_ Tas_Man_t; extern Tas_Man_t * Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit ); @@ -808,8 +805,6 @@ extern void Tas_ManSatPrintStats( Tas_Man_t * p ); extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ); extern int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs ); - - ABC_NAMESPACE_HEADER_END diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c index 38e010f1..607e5ac6 100644 --- a/src/aig/gia/giaAbs.c +++ b/src/aig/gia/giaAbs.c @@ -530,8 +530,8 @@ void Gia_ManCexAbstractionStartNew( Gia_Man_t * pGia, Gia_ParAbs_t * pPars ) { printf( "Problem is satisfiable. Found counter-example in frame %d. ", nFrames-1 ); Abc_PrintTime( 1, "Time", clk ); - pGia->pCexSeq = Gia_ManDeriveCexFromArray( pGia, vCex, 0, nFrames-1 ); - if ( !Gia_ManVerifyCounterExample( pGia, pGia->pCexSeq, 0 ) ) + pGia->pCexSeq = Abc_CexCreate( Gia_ManRegNum(pGia), Gia_ManPiNum(pGia), Vec_IntArray(vCex), nFrames-1, 0, 0 ); + if ( !Gia_ManVerifyCex( pGia, pGia->pCexSeq, 0 ) ) Abc_Print( 1, "Generated counter-example is INVALID.\n" ); pPars->Status = 0; } diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 4ded9a78..71204548 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -416,7 +416,7 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p ) } Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); if ( p->pCexSeq ) - pNew->pCexSeq = Gia_ManDupCounterExample( p->pCexSeq, Gia_ManRegNum(p) ); + pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) ); return pNew; } @@ -764,7 +764,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); if ( p->pCexSeq ) - pNew->pCexSeq = Gia_ManDupCounterExample( p->pCexSeq, Gia_ManRegNum(p) ); + pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) ); return pNew; } diff --git a/src/aig/gia/giaEra2.c b/src/aig/gia/giaEra2.c index 64464832..dedbc032 100644 --- a/src/aig/gia/giaEra2.c +++ b/src/aig/gia/giaEra2.c @@ -1758,7 +1758,7 @@ int Gia_ManArePerform( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbos // verify if ( pAig->pCexSeq ) { - if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) ) + if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) ) printf( "Generated counter-example is INVALID. \n" ); else printf( "Generated counter-example verified correctly. \n" ); @@ -1922,7 +1922,7 @@ Abc_Cex_t * Gia_ManAreDeriveCex( Gia_ManAre_t * p, Gia_StaAre_t * pLast ) Vec_PtrPush( vStates, pSta ); assert( Vec_PtrSize(vStates) >= 1 ); // start the counter-example - pCex = Gia_ManAllocCounterExample( Gia_ManRegNum(p->pAig), Gia_ManPiNum(p->pAig), Vec_PtrSize(vStates) ); + pCex = Abc_CexAlloc( Gia_ManRegNum(p->pAig), Gia_ManPiNum(p->pAig), Vec_PtrSize(vStates) ); pCex->iFrame = Vec_PtrSize(vStates)-1; pCex->iPo = p->iOutFail; // compute states diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c index 1de1a2d4..18e02d81 100644 --- a/src/aig/gia/giaSim.c +++ b/src/aig/gia/giaSim.c @@ -436,7 +436,7 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int Abc_Cex_t * p; unsigned * pData; int f, i, w, iPioId, Counter; - p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 ); + p = Abc_CexAlloc( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 ); p->iFrame = iFrame; p->iPo = iOut; // fill in the binary data @@ -513,7 +513,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars ) pPars->iOutFail = iOut; pAig->pCexSeq = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids ); Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d was asserted in frame %d. ", iOut, i ); - if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) ) + if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) ) { // Abc_Print( 1, "\n" ); Abc_Print( 1, "\nGenerated counter-example is INVALID. " ); diff --git a/src/aig/gia/giaSim2.c b/src/aig/gia/giaSim2.c index 4131f942..e1a5aa07 100644 --- a/src/aig/gia/giaSim2.c +++ b/src/aig/gia/giaSim2.c @@ -606,7 +606,7 @@ Abc_Cex_t * Gia_Sim2GenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int Abc_Cex_t * p; unsigned * pData; int f, i, w, Counter; - p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 ); + p = Abc_CexAlloc( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 ); p->iFrame = iFrame; p->iPo = iOut; // fill in the binary data @@ -663,7 +663,7 @@ int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars ) pPars->iOutFail = iOut; pAig->pCexSeq = Gia_Sim2GenerateCounter( pAig, i, iOut, p->nWords, iPat ); Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d was asserted in frame %d. ", iOut, i ); - if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) ) + if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) ) { // Abc_Print( 1, "\n" ); Abc_Print( 1, "\nGenerated counter-example is INVALID. " ); diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 82bdb367..2794956a 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -829,244 +829,6 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob /**Function************************************************************* - Synopsis [Allocates a counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames ) -{ - Abc_Cex_t * pCex; - int nWords = Gia_BitWordNum( nRegs + nRealPis * nFrames ); - pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); - memset( pCex, 0, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); - pCex->nRegs = nRegs; - pCex->nPis = nRealPis; - pCex->nBits = nRegs + nRealPis * nFrames; - return pCex; -} - - -/**Function************************************************************* - - Synopsis [Prints the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManPrintCex( Abc_Cex_t * p ) -{ - int i, f, k; - for ( k = 0; k < p->nRegs; k++ ) - printf( "%d", Gia_InfoHasBit(p->pData, k) ); - printf( "\n" ); - for ( f = 0; f <= p->iFrame; f++ ) - { - for ( i = 0; i < p->nPis; i++ ) - printf( "%d", Gia_InfoHasBit(p->pData, k++) ); - printf( "\n" ); - } -} - -/**Function************************************************************* - - Synopsis [Derives the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Gia_ManDeriveCexFromArray( Gia_Man_t * pAig, Vec_Int_t * vValues, int nSkip, int iFrame ) -{ - Abc_Cex_t * pCex; - int i; - pCex = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 ); - assert( Vec_IntSize(vValues) == nSkip + pCex->nBits ); - pCex->iPo = 0; - pCex->iFrame = iFrame; - for ( i = 0; i < pCex->nBits; i++ ) - if ( Vec_IntEntry(vValues, nSkip + i) ) - Gia_InfoSetBit( pCex->pData, i ); - return pCex; -} - -/**Function************************************************************* - - Synopsis [Allocates a counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Gia_ManCreateFromComb( int nRegs, int nRealPis, int iPo, int * pModel ) -{ - Abc_Cex_t * pCex; - int i; - pCex = Gia_ManAllocCounterExample( nRegs, nRealPis, 1 ); - pCex->iPo = iPo; - pCex->iFrame = 0; - for ( i = pCex->nRegs; i < pCex->nBits; i++ ) - if ( pModel[i-pCex->nRegs] ) - Gia_InfoSetBit( pCex->pData, i ); - return pCex; -} - -/**Function************************************************************* - - Synopsis [Resimulates the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ) -{ - Gia_Obj_t * pObj, * pObjRi, * pObjRo; - int RetValue, i, k, iBit = 0; - Gia_ManCleanMark0(pAig); - Gia_ManForEachRo( pAig, pObj, i ) - pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); - for ( i = 0; i <= p->iFrame; i++ ) - { - Gia_ManForEachPi( pAig, pObj, k ) - pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); - Gia_ManForEachAnd( pAig, pObj, k ) - pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & - (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); - Gia_ManForEachCo( pAig, pObj, k ) - pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); - if ( i == p->iFrame ) - break; - Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k ) - { - pObjRo->fMark0 = pObjRi->fMark0; - } - } - assert( iBit == p->nBits ); - if ( fDualOut ) - RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0; - else - RetValue = Gia_ManPo(pAig, p->iPo)->fMark0; - Gia_ManCleanMark0(pAig); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Resimulates the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManVerifyCounterExampleAllOuts( Gia_Man_t * pAig, Abc_Cex_t * p ) -{ - Gia_Obj_t * pObj, * pObjRi, * pObjRo; - int RetValue, i, k, iBit = 0; - Gia_ManCleanMark0(pAig); - Gia_ManForEachRo( pAig, pObj, i ) - pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); - for ( i = 0; i <= p->iFrame; i++ ) - { - Gia_ManForEachPi( pAig, pObj, k ) - pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); - Gia_ManForEachAnd( pAig, pObj, k ) - pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & - (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); - Gia_ManForEachCo( pAig, pObj, k ) - pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); - Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k ) - pObjRo->fMark0 = pObjRi->fMark0; - } - assert( iBit == p->nBits ); - // remember the number of failed output - RetValue = -1; - Gia_ManForEachPo( pAig, pObj, i ) - if ( Gia_ManPo(pAig, i)->fMark0 ) - { - RetValue = i; - break; - } - Gia_ManCleanMark0(pAig); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Make the trivial counter-example for the trivially asserted output.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Gia_ManDupCounterExample( Abc_Cex_t * p, int nRegsNew ) -{ - Abc_Cex_t * pCex; - int i; - pCex = Gia_ManAllocCounterExample( nRegsNew, p->nPis, p->iFrame+1 ); - pCex->iPo = p->iPo; - pCex->iFrame = p->iFrame; - for ( i = p->nRegs; i < p->nBits; i++ ) - if ( Gia_InfoHasBit(p->pData, i) ) - Gia_InfoSetBit( pCex->pData, pCex->nRegs + i - p->nRegs ); - return pCex; -} - -/**Function************************************************************* - - Synopsis [Prints out the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManPrintCounterExample( Abc_Cex_t * p ) -{ - int i, f, k; - printf( "Counter-example: iPo = %d iFrame = %d nRegs = %d nPis = %d nBits = %d\n", - p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits ); - printf( "State : " ); - for ( k = 0; k < p->nRegs; k++ ) - printf( "%d", Gia_InfoHasBit(p->pData, k) ); - printf( "\n" ); - for ( f = 0; f <= p->iFrame; f++ ) - { - printf( "Frame %2d : ", f ); - for ( i = 0; i < p->nPis; i++ ) - printf( "%d", Gia_InfoHasBit(p->pData, k++) ); - printf( "\n" ); - } - assert( k == p->nBits ); -} - -/**Function************************************************************* - Synopsis [Dereferences the node's MFFC.] Description [] @@ -1371,6 +1133,91 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj ) */ } +/**Function************************************************************* + + Synopsis [Resimulates the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ) +{ + Gia_Obj_t * pObj, * pObjRi, * pObjRo; + int RetValue, i, k, iBit = 0; + Gia_ManCleanMark0(pAig); + Gia_ManForEachRo( pAig, pObj, i ) + pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); + for ( i = 0; i <= p->iFrame; i++ ) + { + Gia_ManForEachPi( pAig, pObj, k ) + pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); + Gia_ManForEachAnd( pAig, pObj, k ) + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & + (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + Gia_ManForEachCo( pAig, pObj, k ) + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + if ( i == p->iFrame ) + break; + Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k ) + { + pObjRo->fMark0 = pObjRi->fMark0; + } + } + assert( iBit == p->nBits ); + if ( fDualOut ) + RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0; + else + RetValue = Gia_ManPo(pAig, p->iPo)->fMark0; + Gia_ManCleanMark0(pAig); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Resimulates the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p ) +{ + Gia_Obj_t * pObj, * pObjRi, * pObjRo; + int RetValue, i, k, iBit = 0; + Gia_ManCleanMark0(pAig); + Gia_ManForEachRo( pAig, pObj, i ) + pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); + for ( i = 0; i <= p->iFrame; i++ ) + { + Gia_ManForEachPi( pAig, pObj, k ) + pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); + Gia_ManForEachAnd( pAig, pObj, k ) + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & + (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + Gia_ManForEachCo( pAig, pObj, k ) + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k ) + pObjRo->fMark0 = pObjRi->fMark0; + } + assert( iBit == p->nBits ); + // remember the number of failed output + RetValue = -1; + Gia_ManForEachPo( pAig, pObj, i ) + if ( Gia_ManPo(pAig, i)->fMark0 ) + { + RetValue = i; + break; + } + Gia_ManCleanMark0(pAig); + return RetValue; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/int/intCtrex.c b/src/aig/int/intCtrex.c index 28b1e293..0aa60040 100644 --- a/src/aig/int/intCtrex.c +++ b/src/aig/int/intCtrex.c @@ -133,7 +133,7 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose ) if ( status == l_True ) { int i, * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); - pCtrex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames ); + pCtrex = Abc_CexAlloc( Saig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames ); pCtrex->iFrame = nFrames - 1; pCtrex->iPo = 0; for ( i = 0; i < Vec_IntSize(vCiIds); i++ ) @@ -145,7 +145,7 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose ) sat_solver_delete( pSat ); Vec_IntFree( vCiIds ); // verify counter-example - status = Ssw_SmlRunCounterExample( pAig, pCtrex ); + status = Saig_ManVerifyCex( pAig, pCtrex ); if ( status == 0 ) printf( "Inter_ManGetCounterExample(): Counter-example verification has FAILED.\n" ); // report the results diff --git a/src/aig/llb/llb2Core.c b/src/aig/llb/llb2Core.c index 596a34af..4685db0e 100644 --- a/src/aig/llb/llb2Core.c +++ b/src/aig/llb/llb2Core.c @@ -94,7 +94,6 @@ DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarInde ***********************************************************************/ Abc_Cex_t * Llb_CoreDeriveCex( Llb_Img_t * p ) { - extern Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames ); Abc_Cex_t * pCex; Aig_Obj_t * pObj; Vec_Ptr_t * vSupps, * vQuant0, * vQuant1; @@ -112,7 +111,7 @@ Abc_Cex_t * Llb_CoreDeriveCex( Llb_Img_t * p ) // Llb_ImgQuantifyFirst( p->pAig, p->vDdMans, vQuant0 ); // allocate room for the counter-example - pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) ); + pCex = Abc_CexAlloc( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) ); pCex->iFrame = Vec_PtrSize(p->vRings) - 1; pCex->iPo = -1; @@ -178,7 +177,7 @@ Abc_Cex_t * Llb_CoreDeriveCex( Llb_Img_t * p ) } assert( nPiOffset == Saig_ManRegNum(p->pAig) ); // update the output number - RetValue = Ssw_SmlFindOutputCounterExample( p->pInit, pCex ); + RetValue = Saig_ManFindFailedPoCex( p->pInit, pCex ); assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pInit) ); // invalid CEX!!! pCex->iPo = RetValue; // cleanup diff --git a/src/aig/llb/llb3Nonlin.c b/src/aig/llb/llb3Nonlin.c index e52e28ca..62ce441c 100644 --- a/src/aig/llb/llb3Nonlin.c +++ b/src/aig/llb/llb3Nonlin.c @@ -237,7 +237,6 @@ DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd ) ***********************************************************************/ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p ) { - extern Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames ); Abc_Cex_t * pCex; Aig_Obj_t * pObj; Vec_Int_t * vVarsNs; @@ -263,7 +262,7 @@ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p ) printf( "\n" ); */ // allocate room for the counter-example - pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) ); + pCex = Abc_CexAlloc( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) ); pCex->iFrame = Vec_PtrSize(p->vRings) - 1; pCex->iPo = -1; @@ -330,7 +329,8 @@ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p ) } assert( nPiOffset == Saig_ManRegNum(p->pAig) ); // update the output number - RetValue = Ssw_SmlFindOutputCounterExample( p->pInit, pCex ); +//Abc_CexPrint( pCex ); + RetValue = Saig_ManFindFailedPoCex( p->pInit, pCex ); assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pInit) ); // invalid CEX!!! pCex->iPo = RetValue; // cleanup diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index b1017bdb..bf5681b9 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -149,6 +149,8 @@ extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFr extern Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * p ); extern Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs ); extern Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops ); +extern int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p ); +extern int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p ); /*=== saigHaig.c ==========================================================*/ extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose ); /*=== saigInd.c ==========================================================*/ diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c index 938a66e2..471d5d2d 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -101,12 +101,12 @@ Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexA Abc_Cex_t * pCex; Aig_Obj_t * pObj; int i, f; - if ( !Ssw_SmlRunCounterExample( pAbs, pCexAbs ) ) + if ( !Saig_ManVerifyCex( pAbs, pCexAbs ) ) printf( "Saig_ManCexRemap(): The intial counter-example is invalid.\n" ); else printf( "Saig_ManCexRemap(): The intial counter-example is correct.\n" ); // start the counter-example - pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 ); + pCex = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 ); pCex->iFrame = pCexAbs->iFrame; pCex->iPo = pCexAbs->iPo; // copy the bit data @@ -121,10 +121,10 @@ Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexA } } // verify the counter example - if ( !Ssw_SmlRunCounterExample( p, pCex ) ) + if ( !Saig_ManVerifyCex( p, pCex ) ) { printf( "Saig_ManCexRemap(): Counter-example is invalid.\n" ); - Ssw_SmlFreeCounterExample( pCex ); + Abc_CexFree( pCex ); pCex = NULL; } else @@ -194,7 +194,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo printf( "Running property directed reachability...\n" ); RetValue = Pdr_ManSolve( pAbsOrpos, pPars, &pCex ); if ( pCex ) - pCex->iPo = Ssw_SmlFindOutputCounterExample( pAbs, pCex ); + pCex->iPo = Saig_ManFindFailedPoCex( pAbs, pCex ); Aig_ManStop( pAbsOrpos ); pAbs->pSeqModel = pCex; if ( RetValue ) diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index 8aa3af80..cb506054 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -301,11 +301,10 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim } else if ( status == l_True ) { -// extern void * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ); Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames ); int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); pModel[Aig_ManPiNum(pFrames)] = pObj->Id; - pAig->pSeqModel = (Abc_Cex_t *)Fra_SmlCopyCounterExample( pAig, pFrames, pModel ); + pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel ); ABC_FREE( pModel ); Vec_IntFree( vCiIds ); diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index 3d57ae6e..9c36deb3 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -637,7 +637,7 @@ Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p ) Aig_Obj_t * pObj, * pObjFrm; int i, f, iVarNum; // start the counter-example - pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), p->iFrameFail+1 ); + pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), p->iFrameFail+1 ); pCex->iFrame = p->iFrameFail; pCex->iPo = p->iOutputFail; // copy the bit data @@ -656,10 +656,10 @@ Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p ) } } // verify the counter example - if ( !Ssw_SmlRunCounterExample( p->pAig, pCex ) ) + if ( !Saig_ManVerifyCex( p->pAig, pCex ) ) { printf( "Saig_BmcGenerateCounterExample(): Counter-example is invalid.\n" ); - Ssw_SmlFreeCounterExample( pCex ); + Abc_CexFree( pCex ); pCex = NULL; } return pCex; diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index a75297f7..570e8a26 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -1108,8 +1108,7 @@ clkOther += clock() - clk2; continue; if ( Lit == 1 ) { - extern Abc_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ); - Abc_Cex_t * pCex = Fra_SmlTrivCounterExample( pAig, f*Saig_ManPoNum(pAig)+i ); + Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ); printf( "Output %d is trivially SAT in frame %d.\n", i, f ); if ( !pPars->fSolveAll ) { @@ -1137,9 +1136,8 @@ clkOther += clock() - clk2; } else if ( status == l_True ) { -// extern void * Fra_SmlSimpleCounterExample( Aig_Man_t * p, int * pModel, int iFrame, int iPo ); int * pModel = Sat_SolverGetModel( p->pSat, Vec_IntArray(p->vPiVars), Vec_IntSize(p->vPiVars) ); - Abc_Cex_t * pCex = Fra_SmlSimpleCounterExample( pAig, pModel, f, i ); + Abc_Cex_t * pCex = Abc_CexCreate( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), pModel, f, i, 1 ); ABC_FREE( pModel ); fFirst = 0; if ( !pPars->fSolveAll ) diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c index f4e557f8..b2b33bdb 100644 --- a/src/aig/saig/saigDup.c +++ b/src/aig/saig/saigDup.c @@ -265,6 +265,91 @@ Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops ) return pNew; } +/**Function************************************************************* + + Synopsis [Resimulates the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p ) +{ + Aig_Obj_t * pObj, * pObjRi, * pObjRo; + int RetValue, i, k, iBit = 0; + Aig_ManCleanMarkB(pAig); + Aig_ManConst1(pAig)->fMarkB = 1; + Saig_ManForEachLo( pAig, pObj, i ) + pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++); + for ( i = 0; i <= p->iFrame; i++ ) + { + Saig_ManForEachPi( pAig, pObj, k ) + pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++); + Aig_ManForEachNode( pAig, pObj, k ) + pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & + (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj)); + Aig_ManForEachPo( pAig, pObj, k ) + pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj); + if ( i == p->iFrame ) + break; + Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k ) + pObjRo->fMarkB = pObjRi->fMarkB; + } + assert( iBit == p->nBits ); + RetValue = Aig_ManPo(pAig, p->iPo)->fMarkB; + Aig_ManCleanMarkB(pAig); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Resimulates the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p ) +{ + Aig_Obj_t * pObj, * pObjRi, * pObjRo; + int RetValue, i, k, iBit = 0; + Aig_ManCleanMarkB(pAig); + Aig_ManConst1(pAig)->fMarkB = 1; + Saig_ManForEachLo( pAig, pObj, i ) + pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++); + for ( i = 0; i <= p->iFrame; i++ ) + { + Saig_ManForEachPi( pAig, pObj, k ) + pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++); + Aig_ManForEachNode( pAig, pObj, k ) + pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & + (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj)); + Aig_ManForEachPo( pAig, pObj, k ) + pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj); + if ( i == p->iFrame ) + break; + Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k ) + pObjRo->fMarkB = pObjRi->fMarkB; + } + assert( iBit == p->nBits ); + // remember the number of failed output + RetValue = -1; + Saig_ManForEachPo( pAig, pObj, i ) + if ( pObj->fMarkB ) + { + RetValue = i; + break; + } + Aig_ManCleanMarkB(pAig); + return RetValue; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saigSimSeq.c b/src/aig/saig/saigSimSeq.c index 37bb12b5..cc5a9e05 100644 --- a/src/aig/saig/saigSimSeq.c +++ b/src/aig/saig/saigSimSeq.c @@ -418,7 +418,7 @@ Abc_Cex_t * Raig_ManGenerateCounter( Aig_Man_t * pAig, int iFrame, int iOut, int Abc_Cex_t * p; unsigned * pData; int f, i, w, iPioId, Counter; - p = Ssw_SmlAllocCounterExample( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 ); + p = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 ); p->iFrame = iFrame; p->iPo = iOut; // fill in the binary data diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index bf8c918e..437e6ec8 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -123,18 +123,9 @@ extern int Ssw_SmlNumFrames( Ssw_Sml_t * p ); extern int Ssw_SmlNumWordsTotal( Ssw_Sml_t * p ); extern unsigned * Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj ); extern int Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); -extern Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames ); -extern void Ssw_SmlFreeCounterExample( Abc_Cex_t * pCex ); -extern int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ); -extern int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ); -extern Abc_Cex_t * Ssw_SmlDupCounterExample( Abc_Cex_t * p, int nRegsNew ); - - ABC_NAMESPACE_HEADER_END - - #endif //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ssw/sswBmc.c b/src/aig/ssw/sswBmc.c index aba32304..d565d5d3 100644 --- a/src/aig/ssw/sswBmc.c +++ b/src/aig/ssw/sswBmc.c @@ -94,7 +94,7 @@ Abc_Cex_t * Ssw_BmcGetCounterExample( Ssw_Frm_t * pFrm, Ssw_Sat_t * pSat, int iP int f, i, nShift; assert( Saig_ManRegNum(pFrm->pAig) > 0 ); // allocate the counter example - pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(pFrm->pAig), Saig_ManPiNum(pFrm->pAig), iFrame + 1 ); + pCex = Abc_CexAlloc( Saig_ManRegNum(pFrm->pAig), Saig_ManPiNum(pFrm->pAig), iFrame + 1 ); pCex->iPo = iPo; pCex->iFrame = iFrame; // create data-bits diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c index 404302f2..e68f08cd 100644 --- a/src/aig/ssw/sswSim.c +++ b/src/aig/ssw/sswSim.c @@ -1248,131 +1248,6 @@ unsigned * Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj ) return Ssw_ObjSim( p, pObj->Id ); } - -/**Function************************************************************* - - Synopsis [Allocates a counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames ) -{ - Abc_Cex_t * pCex; - int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames ); - pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); - memset( pCex, 0, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); - pCex->nRegs = nRegs; - pCex->nPis = nRealPis; - pCex->nBits = nRegs + nRealPis * nFrames; - return pCex; -} - -/**Function************************************************************* - - Synopsis [Frees the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ssw_SmlFreeCounterExample( Abc_Cex_t * pCex ) -{ - ABC_FREE( pCex ); -} - -/**Function************************************************************* - - Synopsis [Resimulates the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ) -{ - Ssw_Sml_t * pSml; - Aig_Obj_t * pObj; - int RetValue, i, k, iBit; - if ( Saig_ManPiNum(pAig) != p->nPis ) - return 0; -// if ( Saig_ManRegNum(pAig) != p->nRegs ) -// return 0; -// assert( Aig_ManRegNum(pAig) > 0 ); -// assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) ); - // start a new sequential simulator - pSml = Ssw_SmlStart( pAig, 0, p->iFrame+1, 1 ); - // assign simulation info for the registers - iBit = 0; - Saig_ManForEachLo( pAig, pObj, i ) - Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 ); - // assign simulation info for the primary inputs - iBit = Saig_ManRegNum(pAig); - for ( i = 0; i <= p->iFrame; i++ ) - Saig_ManForEachPi( pAig, pObj, k ) - Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i ); -// assert( iBit == p->nBits ); - // run random simulation - Ssw_SmlSimulateOne( pSml ); - // check if the given output has failed - RetValue = !Ssw_SmlNodeIsZeroFrame( pSml, Aig_ManPo(pAig, p->iPo), p->iFrame ); - Ssw_SmlStop( pSml ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Resimulates the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ) -{ - Ssw_Sml_t * pSml; - Aig_Obj_t * pObj; - int i, k, iBit, iOut; - assert( Aig_ManRegNum(pAig) > 0 ); - assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) ); - // start a new sequential simulator - pSml = Ssw_SmlStart( pAig, 0, p->iFrame+1, 1 ); - // assign simulation info for the registers - iBit = 0; - Saig_ManForEachLo( pAig, pObj, i ) - Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 ); - // assign simulation info for the primary inputs - for ( i = 0; i <= p->iFrame; i++ ) - Saig_ManForEachPi( pAig, pObj, k ) - Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i ); - assert( iBit == p->nBits ); - // run random simulation - Ssw_SmlSimulateOne( pSml ); - // check if the given output has failed - iOut = -1; - Saig_ManForEachPo( pAig, pObj, k ) - if ( !Ssw_SmlNodeIsZeroFrame( pSml, Aig_ManPo(pAig, k), p->iFrame ) ) - { - iOut = k; - break; - } - Ssw_SmlStop( pSml ); - return iOut; -} - /**Function************************************************************* Synopsis [Creates sequential counter-example from the simulation info.] @@ -1417,7 +1292,7 @@ Abc_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p ) assert( iBit < 32 * p->nWordsFrame ); // allocate the counter example - pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 ); + pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 ); pCex->iPo = iPo; pCex->iFrame = iFrame; @@ -1438,126 +1313,14 @@ Abc_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p ) } } // verify the counter example - if ( !Ssw_SmlRunCounterExample( p->pAig, pCex ) ) + if ( !Saig_ManVerifyCex( p->pAig, pCex ) ) { printf( "Ssw_SmlGetCounterExample(): Counter-example is invalid.\n" ); - Ssw_SmlFreeCounterExample( pCex ); + Abc_CexFree( pCex ); pCex = NULL; } return pCex; } - -/**Function************************************************************* - - Synopsis [Generates seq counter-example from the combinational one.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Ssw_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ) -{ - Abc_Cex_t * pCex; - Aig_Obj_t * pObj; - int i, nFrames, nTruePis, nTruePos, iPo, iFrame; - // get the number of frames - assert( Aig_ManRegNum(pAig) > 0 ); - assert( Aig_ManRegNum(pFrames) == 0 ); - nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig); - nTruePos = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig); - nFrames = Aig_ManPiNum(pFrames) / nTruePis; - assert( nTruePis * nFrames == Aig_ManPiNum(pFrames) ); - assert( nTruePos * nFrames == Aig_ManPoNum(pFrames) ); - // find the PO that failed - iPo = -1; - iFrame = -1; - Aig_ManForEachPo( pFrames, pObj, i ) - if ( pObj->Id == pModel[Aig_ManPiNum(pFrames)] ) - { - iPo = i % nTruePos; - iFrame = i / nTruePos; - break; - } - assert( iPo >= 0 ); - // allocate the counter example - pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 ); - pCex->iPo = iPo; - pCex->iFrame = iFrame; - - // copy the bit data - for ( i = 0; i < Aig_ManPiNum(pFrames); i++ ) - { - if ( pModel[i] ) - Aig_InfoSetBit( pCex->pData, pCex->nRegs + i ); - if ( pCex->nRegs + i == pCex->nBits - 1 ) - break; - } - - // verify the counter example - if ( !Ssw_SmlRunCounterExample( pAig, pCex ) ) - { - printf( "Ssw_SmlGetCounterExample(): Counter-example is invalid.\n" ); - Ssw_SmlFreeCounterExample( pCex ); - pCex = NULL; - } - return pCex; - -} - -/**Function************************************************************* - - Synopsis [Make the trivial counter-example for the trivially asserted output.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Ssw_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ) -{ - Abc_Cex_t * pCex; - int nTruePis, nTruePos, iPo, iFrame; - assert( Aig_ManRegNum(pAig) > 0 ); - nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig); - nTruePos = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig); - iPo = iFrameOut % nTruePos; - iFrame = iFrameOut / nTruePos; - // allocate the counter example - pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 ); - pCex->iPo = iPo; - pCex->iFrame = iFrame; - return pCex; -} - -/**Function************************************************************* - - Synopsis [Make the trivial counter-example for the trivially asserted output.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Ssw_SmlDupCounterExample( Abc_Cex_t * p, int nRegsNew ) -{ - Abc_Cex_t * pCex; - int i; - pCex = Ssw_SmlAllocCounterExample( nRegsNew, p->nPis, p->iFrame+1 ); - pCex->iPo = p->iPo; - pCex->iFrame = p->iFrame; - for ( i = p->nRegs; i < p->nBits; i++ ) - if ( Aig_InfoHasBit(p->pData, i) ) - Aig_InfoSetBit( pCex->pData, pCex->nRegs + i - p->nRegs ); - return pCex; -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// 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" ); diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h index aca9a509..1321f028 100644 --- a/src/misc/util/abc_global.h +++ b/src/misc/util/abc_global.h @@ -288,18 +288,6 @@ static inline void Abc_PrintMemoryP( int level, const char * pStr, int time, int } -// sequential counter-example -typedef struct Abc_Cex_t_ Abc_Cex_t; -struct Abc_Cex_t_ -{ - int iPo; // the zero-based number of PO, for which verification failed - int iFrame; // the zero-based number of the time-frame, for which verificaiton failed - int nRegs; // the number of registers in the miter - int nPis; // the number of primary inputs in the miter - int nBits; // the number of words of bit data used - unsigned pData[0]; // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis) -}; - ABC_NAMESPACE_HEADER_END #endif diff --git a/src/misc/util/module.make b/src/misc/util/module.make index c70d582a..776a1705 100644 --- a/src/misc/util/module.make +++ b/src/misc/util/module.make @@ -1 +1,3 @@ -SRC += src/misc/util/utilFile.c src/misc/util/utilSignal.c +SRC += src/misc/util/utilCex.c \ + src/misc/util/utilFile.c \ + src/misc/util/utilSignal.c diff --git a/src/sat/pdr/pdrMan.c b/src/sat/pdr/pdrMan.c index 789f4ce8..97f0992b 100644 --- a/src/sat/pdr/pdrMan.c +++ b/src/sat/pdr/pdrMan.c @@ -19,7 +19,6 @@ ***********************************************************************/ #include "pdrInt.h" -#include "ssw.h" ABC_NAMESPACE_IMPL_START @@ -165,7 +164,7 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p ) for ( pObl = p->pQueue; pObl; pObl = pObl->pNext ) nFrames++; // create the counter-example - pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames ); + pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames ); pCex->iPo = (p->pPars->iOutput==-1)? 0 : p->pPars->iOutput; pCex->iFrame = nFrames-1; for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ ) |