From 48b47300e36d3b14ac1abe070cc0ba9784dbbd25 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sat, 7 Apr 2012 12:43:17 -0700
Subject: Added dumping abstracted model in &vta.

---
 src/aig/gia/gia.h       |  1 +
 src/aig/gia/giaAbsVta.c | 36 ++++++++++++++++++++++++++++++++++++
 src/base/abci/abc.c     |  8 ++++++--
 3 files changed, 43 insertions(+), 2 deletions(-)

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index caafc1e4..1d7bf625 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -210,6 +210,7 @@ struct Gia_ParVta_t_
     int            nRatioMin;     // stop when less than this % of object is abstracted
     int            fUseTermVars;  // use terminal variables
     int            fUseRollback;  // use rollback to the starting number of frames
+    int            fDumpVabs;     // dumps the abstracted model
     int            fVerbose;      // verbose flag
     int            iFrame;        // the number of frames covered 
 };
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index a697ee16..5ee030ec 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -1428,6 +1428,39 @@ void Gia_VtaSendCancel( Vta_Man_t * p, int fVerbose )
     Gia_ManToBridgeBadAbs( stdout );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Send abstracted model or send cancel.]
+
+  Description [Counter-example will be sent automatically when &vta terminates.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_VtaDumpAbsracted( Vta_Man_t * p, int fVerbose )
+{
+    Gia_Man_t * pAbs;
+    if ( fVerbose )
+        Abc_Print( 1, "Dumping abstracted model into file \"vabs.aig\"...\n" );
+    if ( !Abc_FrameIsBridgeMode() )
+        return;
+    // create obj classes
+    Vec_IntFreeP( &p->pGia->vObjClasses );
+    p->pGia->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
+    // create gate classes
+    Vec_IntFreeP( &p->pGia->vGateClasses );
+    p->pGia->vGateClasses = Gia_VtaConvertToGla( p->pGia, p->pGia->vObjClasses );
+    Vec_IntFreeP( &p->pGia->vObjClasses );
+    // create abstrated model
+    pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses );
+    Vec_IntFreeP( &p->pGia->vGateClasses );
+    // send it out
+    Gia_WriteAiger( pAbs, "vabs.aig", 0, 0 );
+    Gia_ManStop( pAbs );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Collect nodes/flops involved in different timeframes.]
@@ -1568,6 +1601,9 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
             // send new one 
             Gia_VtaSendAbsracted( p, pPars->fVerbose );
             fOneIsSent = 1;
+            // dump the model
+            if ( p->pPars->fDumpVabs )
+                Gia_VtaDumpAbsracted( p, pPars->fVerbose );
         }
         // check if the number of objects is below limit
         if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 31256e87..8798763e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27222,7 +27222,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Gia_VtaSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRtrvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRtrdvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -27309,6 +27309,9 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'r':
             pPars->fUseRollback ^= 1;
             break;
+        case 'd':
+            pPars->fDumpVabs ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -27354,7 +27357,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &vta [-FSPCLTR num] [-trvh]\n" );
+    Abc_Print( -2, "usage: &vta [-FSPCLTR num] [-trdvh]\n" );
     Abc_Print( -2, "\t         refines abstracted object map with proof-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 );
@@ -27365,6 +27368,7 @@ usage:
     Abc_Print( -2, "\t-R num : minimum percentage of abstracted objects (0<=num<=100) [default = %d]\n", pPars->nRatioMin );
     Abc_Print( -2, "\t-t     : toggle using terminal variables [default = %s]\n", pPars->fUseTermVars? "yes": "no" );
     Abc_Print( -2, "\t-r     : toggle using rollback after the starting frames [default = %s]\n", pPars->fUseRollback? "yes": "no" );
+    Abc_Print( -2, "\t-d     : toggle dumping abstracted model into file \"vabs.aig\" [default = %s]\n", pPars->fDumpVabs? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
-- 
cgit v1.2.3