Added deriving abstraction in GIA from the precomputed flop map.

1 files changed, 6 insertions, 34 deletions

diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index 7a4e51f4..2f7959a8 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -120,12 +120,12 @@ Vec_Int_t * Gia_ManClasses2Flops( Vec_Int_t * vFlopClasses )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManCexAbstraction( Gia_Man_t * p, Vec_Int_t * vFlops )
+Gia_Man_t * Gia_ManDupAbstractionAig( Gia_Man_t * p, Vec_Int_t * vFlops )
 {
     Gia_Man_t * pGia;
     Aig_Man_t * pNew, * pTemp;
     pNew = Gia_ManToAig( p, 0 );
-    pNew = Saig_ManDeriveAbstraction( pTemp = pNew, vFlops );
+    pNew = Saig_ManDupAbstraction( pTemp = pNew, vFlops );
     Aig_ManStop( pTemp );
     pGia = Gia_ManFromAig( pNew );
 //    pGia->vCiNumsOrig = pNew->vCiNumsOrig; 
@@ -168,32 +168,6 @@ void Gia_ManCexAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars )
 
 /**Function*************************************************************
 
-  Synopsis    [Derives abstraction using the latch map.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia )
-{
-    Vec_Int_t * vFlops;
-    Gia_Man_t * pAbs = NULL;
-    if ( pGia->vFlopClasses == NULL )
-    {
-        printf( "Gia_ManCexAbstractionDerive(): Abstraction latch map is missing.\n" );
-        return NULL;
-    }
-    vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
-    pAbs = Gia_ManCexAbstraction( pGia, vFlops );
-    Vec_IntFree( vFlops );
-    return pAbs;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Refines abstraction using the latch map.]
 
   Description []
@@ -273,8 +247,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo
         return 0;
     }
     // derive abstraction
-    vFlops = Saig_ManClasses2Flops( pGia->vFlopClasses );
-    pAbs = Gia_ManCexAbstraction( pGia, vFlops );
+    pAbs = Gia_ManDupAbstraction( pGia, pGia->vFlopClasses );
     // refine abstraction using PBA
     pAig = Gia_ManToAigSimple( pAbs );
     Gia_ManStop( pAbs );
@@ -283,6 +256,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo
     // derive new classes
     if ( vFlopsNew != NULL )
     {
+        vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
         vSelected = Gia_ManFlopsSelect( vFlops, vFlopsNew );
         Vec_IntFree( pGia->vFlopClasses );
         pGia->vFlopClasses = Saig_ManFlops2Classes( Gia_ManRegNum(pGia), vSelected );
@@ -292,7 +266,6 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo
         Vec_IntFree( vFlops );
         return 1;
     }
-    Vec_IntFree( vFlops );
     // found counter-eample for the abstracted model
     // or exceeded conflict limit
     return 0;
@@ -321,8 +294,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
         pGia->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) );
     }
     // derive abstraction
-    vFlops = Saig_ManClasses2Flops( pGia->vFlopClasses );
-    pAbs = Gia_ManCexAbstraction( pGia, vFlops );
+    pAbs = Gia_ManDupAbstraction( pGia, pGia->vFlopClasses );
     // refine abstraction using PBA
     pAig = Gia_ManToAigSimple( pAbs );
     Gia_ManStop( pAbs );
@@ -331,6 +303,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
     // derive new classes
     if ( vFlopsNew != NULL )
     {
+        vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
 //        vSelected = Saig_ManFlopsSelect( vFlops, vFlopsNew );
         vSelected = NULL;
         Vec_IntFree( pGia->vFlopClasses );
@@ -341,7 +314,6 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
         Vec_IntFree( vFlops );
         return 1;
     }
-    Vec_IntFree( vFlops );
     // found counter-eample for the abstracted model
     // or exceeded conflict limit
     return 0;