luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Several bug fixes and silencing requests.

This commit is contained in:
Alan Mishchenko 2015-03-16 19:38:43 +07:00
parent 1e757a8567
commit 7fe11c51cf
6 changed files with 17 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/aig/gia/giaFx.c
View File

@ -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

2
src/base/abci/abc.c
View File

@ -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;

6
src/base/wlc/wlcReadSmt.c
View File

@ -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;
}

2
src/proof/cec/cec.h
View File

@ -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 ==========================================================*/

7
src/proof/cec/cecCec.c
View File

@ -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 );

7
src/proof/cec/cecCore.c
View File

@ -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;