diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-25 16:22:31 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-25 16:22:31 -0800 |
| commit | 4ec5ee410d4523ca1396ff4c7247e3a7ceaf027a (patch) | |
| tree | 80d83b3b7d90ddd6cc699fe590e4fc3a35ef4e88 /src/proof/abs | |
| parent | 7d5b1c572bfb5385dc79f795d4c9d3294adbdae6 (diff) | |
| download | abc-4ec5ee410d4523ca1396ff4c7247e3a7ceaf027a.tar.gz abc-4ec5ee410d4523ca1396ff4c7247e3a7ceaf027a.tar.bz2 abc-4ec5ee410d4523ca1396ff4c7247e3a7ceaf027a.zip | |
Adding dump of trivial abstraction map at the beginning in &gla -m.
Diffstat (limited to 'src/proof/abs')
| -rw-r--r-- | src/proof/abs/absGla.c | 40 |
1 files changed, 25 insertions, 15 deletions
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" ); } |