From 7fe11c51cfb050dafef1cf875dc4eb4e65352465 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 16 Mar 2015 19:38:43 +0700 Subject: Several bug fixes and silencing requests. --- src/aig/gia/giaFx.c | 4 +++- src/base/abci/abc.c | 2 +- src/base/wlc/wlcReadSmt.c | 6 +++--- src/proof/cec/cec.h | 2 +- src/proof/cec/cecCec.c | 7 +++++-- src/proof/cec/cecCore.c | 7 ++++--- 6 files changed, 17 insertions(+), 11 deletions(-) diff --git a/src/aig/gia/giaFx.c b/src/aig/gia/giaFx.c index 73a8cf5c..4fff177c 100644 --- a/src/aig/gia/giaFx.c +++ b/src/aig/gia/giaFx.c @@ -282,7 +282,7 @@ Vec_Int_t * Gia_ManFxTopoOrder( Vec_Wec_t * vCubes, int nInputs, int nStart, Vec // quit if there is no new nodes if ( nNodeMax == nStart ) { - printf( "The network is unchanged by fast extract.\n" ); + //printf( "The network is unchanged by fast extract.\n" ); return NULL; } // find first cube and how many cubes @@ -459,6 +459,8 @@ Gia_Man_t * Gia_ManPerformFx( Gia_Man_t * p, int nNewNodesMax, int LitCountMax, Gia_Man_t * pNew = NULL; Vec_Wec_t * vCubes; Vec_Str_t * vCompl; + if ( Gia_ManAndNum(p) == 0 ) + return Gia_ManDup(p); // abctime clk; assert( Gia_ManHasMapping(p) ); // collect information diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index de96b546..10a6f191 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -30301,7 +30301,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Fraig(): There is no AIG.\n" ); return 1; } - pTemp = Cec_ManSatSweeping( pAbc->pGia, pPars ); + pTemp = Cec_ManSatSweeping( pAbc->pGia, pPars, 0 ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c index 8143be6c..dcf018b7 100644 --- a/src/base/wlc/wlcReadSmt.c +++ b/src/base/wlc/wlcReadSmt.c @@ -706,12 +706,12 @@ static inline char * Smt_PrsLoadFile( char * pFileName, char ** ppLimit ) // move the file current reading position to the beginning rewind( pFile ); // load the contents of the file into memory - pBuffer = ABC_ALLOC( char, nFileSize + 3 ); + pBuffer = ABC_ALLOC( char, nFileSize + 16 ); pBuffer[0] = '\n'; RetValue = fread( pBuffer+1, nFileSize, 1, pFile ); // terminate the string with '\0' - pBuffer[nFileSize + 0] = '\n'; - pBuffer[nFileSize + 1] = '\0'; + pBuffer[nFileSize + 1] = '\n'; + pBuffer[nFileSize + 2] = '\0'; *ppLimit = pBuffer + nFileSize + 2; return pBuffer; } diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index 3fb5d0b0..805a5d73 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -210,7 +210,7 @@ extern void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p ); extern void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p ); extern void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p ); extern void Cec_ManChcSetDefaultParams( Cec_ParChc_t * p ); -extern Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars ); +extern Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSilent ); extern Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars ); extern void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars ); /*=== cecSeq.c ==========================================================*/ diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c index d6e8456d..1465a721 100644 --- a/src/proof/cec/cecCec.c +++ b/src/proof/cec/cecCec.c @@ -358,7 +358,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) pParsFra->fVerbose = pPars->fVerbose; pParsFra->fCheckMiter = 1; pParsFra->fDualOut = 1; - pNew = Cec_ManSatSweeping( p, pParsFra ); + pNew = Cec_ManSatSweeping( p, pParsFra, pPars->fSilent ); pPars->iOutFail = pParsFra->iOutFail; // update pInit->pCexComb = p->pCexComb; p->pCexComb = NULL; @@ -371,8 +371,11 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) { if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) ) Abc_Print( 1, "Counter-example simulation has failed.\n" ); + if ( !pPars->fSilent ) + { Abc_Print( 1, "Networks are NOT EQUIVALENT. " ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + } return 0; } p = Gia_ManDup( pInit ); @@ -542,7 +545,7 @@ Aig_Man_t * Cec_FraigCombinational( Aig_Man_t * pAig, int nConfs, int fVerbose ) pFraPars->nItersMax = 20; pFraPars->fVerbose = fVerbose; pGia = Gia_ManFromAigSimple( pAig ); - Cec_ManSatSweeping( pGia, pFraPars ); + Cec_ManSatSweeping( pGia, pFraPars, 0 ); Gia_ManReprToAigRepr( pAig, pGia ); Gia_ManStop( pGia ); return Aig_ManDupSimple( pAig ); diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c index 71335e85..c9e9f67a 100644 --- a/src/proof/cec/cecCore.c +++ b/src/proof/cec/cecCore.c @@ -334,7 +334,7 @@ void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars ) +Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSilent ) { int fOutputResult = 0; Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; @@ -521,12 +521,13 @@ finalize: pTemp = p->pAig; p->pAig = NULL; if ( pTemp == NULL && pSim->iOut >= 0 ) { + if ( !fSilent ) Abc_Print( 1, "Disproved at least one output of the miter (zero-based number %d).\n", pSim->iOut ); pPars->iOutFail = pSim->iOut; } - else if ( pSim->pCexes ) + else if ( pSim->pCexes && !fSilent ) Abc_Print( 1, "Disproved %d outputs of the miter.\n", pSim->nOuts ); - if ( fTimeOut ) + if ( fTimeOut && !fSilent ) Abc_Print( 1, "Timed out after %d seconds.\n", (int)((double)Abc_Clock() - clkTotal)/CLOCKS_PER_SEC ); pAig->pCexComb = pSim->pCexComb; pSim->pCexComb = NULL; -- cgit v1.2.3