Added switch '&gla -m' to dump original miter with the abstraction map.

src/aig/gia/gia.h

@@ -226,13 +226,14 @@ struct Gia_ParVta_t_
     int            fUseRollback;  // use rollback to the starting number of frames
     int            fPropFanout;   // propagate fanout implications
     int            fAddLayer;     // refinement strategy by adding layers
-    int            fUseSkip;
-    int            fUseSimple;
-    int            fSkipHash;
+    int            fUseSkip;      // skip proving intermediate timeframes
+    int            fUseSimple;    // use simple CNF construction
+    int            fSkipHash;     // skip hashing CNF while unrolling
     int            fDumpVabs;     // dumps the abstracted model
+    int            fDumpMabs;     // dumps the original AIG with abstraction map
     char *         pFileVabs;     // dumps the abstracted model into this file
     int            fVerbose;      // verbose flag
-    int            fVeryVerbose;
+    int            fVeryVerbose;  // print additional information
     int            iFrame;        // the number of frames covered
     int            nFramesNoChange; // the number of last frames without changes
 };

src/aig/gia/giaAbsGla2.c

@@ -1325,18 +1325,26 @@ void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose )
 {
     char * pFileNameDef = "glabs.aig";
     char * pFileName = p->pPars->pFileVabs ? p->pPars->pFileVabs : pFileNameDef;
-    Gia_Man_t * pAbs;
-    Vec_Int_t * vGateClasses;
     if ( fVerbose )
         Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
-    // create abstraction
-    vGateClasses = Ga2_ManAbsTranslate( p );
-    pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
-    Vec_IntFreeP( &vGateClasses );
+    if ( p->pPars->fDumpVabs )
+    {
+        // dump absracted model
+        Vec_Int_t * vGateClasses = Ga2_ManAbsTranslate( p );
+        Gia_Man_t * pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
         Gia_ManCleanValue( p->pGia );
-    // write into file
         Gia_WriteAiger( pAbs, pFileName, 0, 0 );
         Gia_ManStop( pAbs );
+        Vec_IntFreeP( &vGateClasses );
+    }
+    else if ( p->pPars->fDumpMabs )
+    {
+        // dump abstraction map
+        Vec_IntFreeP( &p->pGia->vGateClasses );
+        p->pGia->vGateClasses = Ga2_ManAbsTranslate( p );
+        Gia_WriteAiger( p->pGia, pFileName, 0, 0 );
+    }
+    else assert( 0 );
 }
 
 /**Function*************************************************************
@@ -1426,7 +1434,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         Abc_Print( 1, "FrameMax = %d  ConfMax = %d  Timeout = %d  RatioMin = %d %%  RatioMax = %d %%\n", 
             pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin, pPars->nRatioMax );
         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->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs );
         Abc_Print( 1, " Frame   %%   Abs  PPI   FF   LUT   Confl  Cex   Vars   Clas   Lrns     Time      Mem\n" );
     }
     // iterate unrolling
@@ -1620,7 +1628,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                 }
 
                 // dump the model into file
-                if ( p->pPars->fDumpVabs )
+                if ( p->pPars->fDumpVabs || p->pPars->fDumpMabs )
                 {
                     Abc_FrameSetCex( NULL );
                     Abc_FrameSetNFrames( f+1 );

src/base/abci/abc.c

@@ -28196,7 +28196,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c, fStartVta = 0, fNewAlgo = 1;
     Gia_VtaSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FSCLDETRPAtrfkadnscbwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FSCLDETRPAtrfkadmnscbwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -28326,6 +28326,9 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             pPars->fDumpVabs ^= 1;
             break;
+        case 'm':
+            pPars->fDumpMabs ^= 1;
+            break;
         case 'n':
             fNewAlgo ^= 1;
             break;
@@ -28386,7 +28389,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &gla [-FSCLDETRP num] [-A file] [-fkadnscbwvh]\n" );
+    Abc_Print( -2, "usage: &gla [-FSCLDETRP num] [-A file] [-fkadmnscbwvh]\n" );
     Abc_Print( -2, "\t          fixed-time-frame gate-level proof- and cex-based abstraction\n" );
     Abc_Print( -2, "\t-F num  : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
     Abc_Print( -2, "\t-S num  : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
@@ -28402,6 +28405,7 @@ usage:
     Abc_Print( -2, "\t-k      : toggle using VTA to kick start GLA for starting frames [default = %s]\n", fStartVta? "yes": "no" );
     Abc_Print( -2, "\t-a      : toggle refinement by adding one layers of gates [default = %s]\n", pPars->fAddLayer? "yes": "no" );
     Abc_Print( -2, "\t-d      : toggle dumping abstracted model into a file [default = %s]\n", pPars->fDumpVabs? "yes": "no" );
+    Abc_Print( -2, "\t-m      : toggle dumping abstraction map into a file [default = %s]\n", pPars->fDumpMabs? "yes": "no" );
     Abc_Print( -2, "\t-n      : toggle using new algorithms [default = %s]\n", fNewAlgo? "yes": "no" );
     Abc_Print( -2, "\t-s      : toggle skipping previously proved timeframes [default = %s]\n", pPars->fUseSkip? "yes": "no" );
     Abc_Print( -2, "\t-c      : toggle using naive (2-input AND node) CNF encoding [default = %s]\n", pPars->fUseSimple? "yes": "no" );