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 ++++++++++++++++++++++++++++++++++++
 2 files changed, 37 insertions(+)

(limited to 'src/aig')

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 )
-- 
cgit v1.2.3