From 4ec5ee410d4523ca1396ff4c7247e3a7ceaf027a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 25 Feb 2017 16:22:31 -0800 Subject: Adding dump of trivial abstraction map at the beginning in &gla -m. --- src/proof/abs/absGla.c | 40 +++++++++++++++++++++++++--------------- 1 file changed, 25 insertions(+), 15 deletions(-) (limited to 'src/proof') diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c index 420adfc3..5f8503a5 100644 --- a/src/proof/abs/absGla.c +++ b/src/proof/abs/absGla.c @@ -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" ); } -- cgit v1.2.3