diff options
Diffstat (limited to 'src/proof/abs/absGla.c')
| -rw-r--r-- | src/proof/abs/absGla.c | 30 |
1 files changed, 29 insertions, 1 deletions
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c index 97a8b644..5f8503a5 100644 --- a/src/proof/abs/absGla.c +++ b/src/proof/abs/absGla.c @@ -1539,9 +1539,37 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) Abc_Print( 1, "LrnStart = %d LrnDelta = %d LrnRatio = %d %% Skip = %d SimpleCNF = %d Dump = %d\n", pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs ); if ( pPars->fDumpVabs || pPars->fDumpMabs ) - Abc_Print( 1, "%s will be dumped into file \"%s\".\n", + Abc_Print( 1, "%s will be continously dumped into file \"%s\".\n", pPars->fDumpVabs ? "Abstracted model" : "Miter with abstraction map", Ga2_GlaGetFileName(p, pPars->fDumpVabs) ); + if ( pPars->fDumpMabs ) + { + { + 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" ); } // iterate unrolling |