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

Making GLA PBA and GLA CBA communicate information.

This commit is contained in:
Alan Mishchenko 2011-11-22 19:07:00 -08:00
parent ff938c7141
commit 0a5d856cec
3 changed files with 14 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/aig/gia/giaAbs.c
View File

@ -484,8 +484,11 @@ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars )
pGia->vGateClasses = vGateClasses;
}
// clean up the abstraction map
pGiaAbs = Gia_ManDupAbsGates( pGia, pGia->vGateClasses );
Gia_ManStop( pGiaAbs );
if ( pGia->vGateClasses )
{
pGiaAbs = Gia_ManDupAbsGates( pGia, pGia->vGateClasses );
Gia_ManStop( pGiaAbs );
}
if ( p->fVerbose )
Gia_ManPrintStats( pGia, 0 );
return 1;

6
src/aig/saig/saigGlaPba.c
View File

@ -579,7 +579,7 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
return NULL;
}
sat_solver_set_random( p->pSat, fSkipRand );
p->timePre += Abc_Clock(1,0);
p->timePre += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC;
// set runtime limit
if ( TimeLimit )
@ -593,8 +593,8 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
Aig_Gla2ManStop( p );
return NULL;
}
p->timeSat += Abc_Clock(1,0);
p->timeTotal = Abc_Clock(0,0);
p->timeSat += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC;
p->timeTotal = (Abc_Clock(0,0)/ABC_CPS)*CLOCKS_PER_SEC;
// print stats
if ( fVerbose )

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

@ -28952,8 +28952,8 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
Saig_ParBmc_t Pars, * pPars = &Pars;
int c, fNaiveCnf = 0;
Saig_ParBmcSetDefaultParams( pPars );
pPars->nStart = 0; // (pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
pPars->nFramesMax = 0; // pPars->nStart + 10;
pPars->nStart = (pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
pPars->nFramesMax = 0;
pPars->nConfLimit = 0;
pPars->nTimeOut = 60;
Extra_UtilGetoptReset();
@ -29054,10 +29054,9 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
pAbc->Status = Gia_ManGlaCbaPerform( pAbc->pGia, pPars, fNaiveCnf );
if ( pPars->nStart == 0 )
// if ( pPars->nStart == 0 )
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
// printf( "This command is currently not enabled.\n" );
return 0;
usage:
@ -29090,8 +29089,8 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv )
Saig_ParBmc_t Pars, * pPars = &Pars;
int c;
Saig_ParBmcSetDefaultParams( pPars );
pPars->nStart = 0; //(pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
pPars->nFramesMax = 10; //pPars->nStart + 10;
pPars->nStart = 0;
pPars->nFramesMax = (pAbc->nFrames >= 0) ? pAbc->nFrames : 10;
pPars->nConfLimit = 0;
pPars->fSkipRand = 0;
Extra_UtilGetoptReset();
@ -29183,7 +29182,7 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nStart )
Abc_Print( 0, "The starting frame is specified. The resulting abstraction may be unsound.\n" );
pAbc->Status = Gia_ManGlaPbaPerform( pAbc->pGia, pPars );
if ( pPars->nStart == 0 )
// if ( pPars->nStart == 0 )
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;