diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-25 09:49:31 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-25 09:49:31 -0800 |
| commit | 80773b95221237134719e08948ed1b74ac049536 (patch) | |
| tree | 6dc27a68593dcd77656f4eceead3e7f6744f530c /src/proof/abs | |
| parent | 06797fb6119a4710d4d06a3c565d0bac682499e0 (diff) | |
| download | abc-80773b95221237134719e08948ed1b74ac049536.tar.gz abc-80773b95221237134719e08948ed1b74ac049536.tar.bz2 abc-80773b95221237134719e08948ed1b74ac049536.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 | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c index 97a8b644..420adfc3 100644 --- a/src/proof/abs/absGla.c +++ b/src/proof/abs/absGla.c @@ -1539,9 +1539,27 @@ 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 ) + { + // 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 |