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

Adding dump of trivial abstraction map at the beginning in &gla -m.

This commit is contained in:
Alan Mishchenko 2017-02-25 16:22:31 -08:00
parent 7d5b1c572b
commit 4ec5ee410d
1 changed files with 25 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
src/proof/abs/absGla.c
View File

@ -1544,21 +1544,31 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
Ga2_GlaGetFileName(p, pPars->fDumpVabs) );
if ( pPars->fDumpMabs )
{
// create trivial abstraction map
Gia_Obj_t * pObj;
char * pFileName = Ga2_GlaGetFileName(p, 0);
Vec_Int_t * vMap = pAig->vGateClasses; pAig->vGateClasses = NULL;
pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
Gia_ManForEachAnd( pAig, pObj, i )
Vec_IntWriteEntry( pAig->vGateClasses, i, 1 );
Gia_ManForEachRo( pAig, pObj, i )
Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjId(pAig, pObj), 1 );
Gia_AigerWrite( pAig, pFileName, 0, 0 );
Vec_IntFree( pAig->vGateClasses );
pAig->vGateClasses = vMap;
if ( p->pPars->fVerbose )
Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName );
{
char Command[1000];
Abc_FrameSetStatus( -1 );
Abc_FrameSetCex( NULL );
Abc_FrameSetNFrames( -1 );
sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((char *)(p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig"), ".status"));
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
}
{
// create trivial abstraction map
Gia_Obj_t * pObj;
char * pFileName = Ga2_GlaGetFileName(p, 0);
Vec_Int_t * vMap = pAig->vGateClasses; pAig->vGateClasses = NULL;
pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
Gia_ManForEachAnd( pAig, pObj, i )
Vec_IntWriteEntry( pAig->vGateClasses, i, 1 );
Gia_ManForEachRo( pAig, pObj, i )
Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjId(pAig, pObj), 1 );
Gia_AigerWrite( pAig, pFileName, 0, 0 );
Vec_IntFree( pAig->vGateClasses );
pAig->vGateClasses = vMap;
if ( p->pPars->fVerbose )
Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName );
}
}
Abc_Print( 1, " Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" );
}