Added command &gla_purify.

6 files changed, 322 insertions, 181 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index aebcc7eb..3eda381d 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -702,6 +702,11 @@ extern int                 Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int
 extern int                 Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars );
 extern int                 Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf );
 extern int                 Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver );
+extern Vec_Int_t *         Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta );
+extern Vec_Int_t *         Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames );
+extern Vec_Int_t *         Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla );
+extern Vec_Int_t *         Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla );
+extern unsigned *          Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj );
 /*=== giaAbsGla.c ===========================================================*/
 extern int                 Gia_GlaPerform( Gia_Man_t * p, Gia_ParVta_t * pPars, int fStartVta );
 /*=== giaAbsVta.c ===========================================================*/
@@ -941,11 +946,6 @@ extern void                Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern int                 Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
 extern int                 Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs );
 extern void                Gia_ManInvertConstraints( Gia_Man_t * pAig );
-extern Vec_Int_t *         Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta );
-extern Vec_Int_t *         Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames );
-extern Vec_Int_t *         Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla );
-extern Vec_Int_t *         Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla );
-extern unsigned *          Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj );
 
 /*=== giaCTas.c ===========================================================*/
 typedef struct Tas_Man_t_  Tas_Man_t;
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index 9e37c5ed..59b5ddfe 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -498,6 +498,216 @@ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver )
     return 1;
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Converting VTA vector to GLA vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta )
+{
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vGla;
+    int nObjMask, nObjs = Gia_ManObjNum(p);
+    int i, Entry, nFrames = Vec_IntEntry( vVta, 0 );
+    assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
+    // get the bitmask
+    nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
+    assert( nObjs <= nObjMask );
+    // go through objects
+    vGla = Vec_IntStart( nObjs );
+    Vec_IntForEachEntryStart( vVta, Entry, i, nFrames+2 )
+    {
+        pObj = Gia_ManObj( p, (Entry &  nObjMask) );
+        assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsConst0(pObj) );
+        Vec_IntAddToEntry( vGla, (Entry &  nObjMask), 1 );
+    }
+    Vec_IntWriteEntry( vGla, 0, nFrames );
+    return vGla;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converting GLA vector to VTA vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames )
+{
+    Vec_Int_t * vVta;
+    int nObjBits, nObjMask, nObjs = Gia_ManObjNum(p);
+    int i, k, j, Entry, Counter, nGlaSize;
+    //. get the GLA size
+    nGlaSize = Vec_IntSum(vGla);
+    // get the bitmask
+    nObjBits = Abc_Base2Log(nObjs);
+    nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
+    assert( nObjs <= nObjMask );
+    // go through objects
+    vVta = Vec_IntAlloc( 1000 );
+    Vec_IntPush( vVta, nFrames );
+    Counter = nFrames + 2;
+    for ( i = 0; i <= nFrames; i++, Counter += i * nGlaSize )
+        Vec_IntPush( vVta, Counter );
+    for ( i = 0; i < nFrames; i++ )
+        for ( k = 0; k <= i; k++ )
+            Vec_IntForEachEntry( vGla, Entry, j )
+                if ( Entry ) 
+                    Vec_IntPush( vVta, (k << nObjBits) | j );
+    Counter = Vec_IntEntry(vVta, nFrames+1);
+    assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
+    return vVta;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converting GLA vector to FLA vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_FlaConvertToGla_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vGla )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    Vec_IntWriteEntry( vGla, Gia_ObjId(p, pObj), 1 );
+    if ( Gia_ObjIsRo(p, pObj) )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
+    Gia_FlaConvertToGla_rec( p, Gia_ObjFanin1(pObj), vGla );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converting FLA vector to GLA vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla )
+{
+    Vec_Int_t * vGla;
+    Gia_Obj_t * pObj;
+    int i;
+    // mark const0 and relevant CI objects
+    Gia_ManIncrementTravId( p );
+    Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p));
+    Gia_ManForEachPi( p, pObj, i )
+        Gia_ObjSetTravIdCurrent(p, pObj);
+    Gia_ManForEachRo( p, pObj, i )
+        if ( !Vec_IntEntry(vFla, i) )
+            Gia_ObjSetTravIdCurrent(p, pObj);
+    // label all objects reachable from the PO and selected flops
+    vGla = Vec_IntStart( Gia_ManObjNum(p) );
+    Vec_IntWriteEntry( vGla, 0, 1 );
+    Gia_ManForEachPo( p, pObj, i )
+        Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
+    Gia_ManForEachRi( p, pObj, i )
+        if ( Vec_IntEntry(vFla, i) )
+            Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
+    return vGla;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converting GLA vector to FLA vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla )
+{
+    Vec_Int_t * vFla;
+    Gia_Obj_t * pObj;
+    int i;
+    vFla = Vec_IntStart( Gia_ManRegNum(p) );
+    Gia_ManForEachRo( p, pObj, i )
+        if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
+            Vec_IntWriteEntry( vFla, i, 1 );
+    return vFla;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManGlaPurify( Gia_Man_t * p, int nPurifyRatio, int fVerbose )
+{
+    int i, Entry, CountUpTo, CountAll, CountRem, * pCounts;
+    int nFrames = Vec_IntEntry( p->vGateClasses, 0 );
+    if ( nFrames < 2 )
+    {
+        printf( "Gate-level abstraction is missing object count information.\n" );
+        return;
+    }
+    // collect info
+    CountAll = 0;
+    pCounts = ABC_CALLOC( int, nFrames + 1 );
+    assert( Vec_IntSize(p->vGateClasses) == Gia_ManObjNum(p) );
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+    {
+        Entry = Vec_IntEntry( p->vGateClasses, i );
+        assert( Entry >= 0 && Entry <= nFrames );
+        if ( Entry == 0 )
+            continue;
+        CountAll++;
+        pCounts[Entry]++;
+    }
+    // print entries
+    CountUpTo = 0;
+    for ( i = 0; i <= nFrames; i++ )
+        printf( "%d=%d(%d) ", i, pCounts[i], CountUpTo += pCounts[i] );
+    printf( "\n" );
+    // removing entries appearing only ones
+    CountRem = 0;
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+    {
+        if ( Vec_IntEntry( p->vGateClasses, i ) == 0 )
+            continue;
+        if ( Vec_IntEntry( p->vGateClasses, i ) <= nPurifyRatio )
+        {
+            CountRem++;
+            Vec_IntWriteEntry( p->vGateClasses, i, 0 );
+        }
+    }
+    printf( "Removed %d entries appearing less or equal than %d times (out of %d).\n", CountRem, nPurifyRatio, CountAll ); 
+    ABC_FREE( pCounts );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 7a509f7f..64ea44b0 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -83,9 +83,9 @@ struct Gla_Man_t_
     Vec_Int_t *    vTemp;           // temporary array
     Vec_Int_t *    vAddedNew;       // temporary array
     Vec_Int_t *    vObjCounts;      // object counters
+    Vec_Int_t *    vCoreCounts;     // counts how many times each object appears in the core
     // refinement
     Vec_Int_t *    pvRefis;         // vectors of each object
-//    Vec_Int_t *    vPrioSels;       // selected priorities
     // statistics  
     clock_t        timeInit;
     clock_t        timeSat;
@@ -296,7 +296,7 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
                     assert( i >= Vec_IntSize(vPis) );
                     iObjId = Vec_IntEntry( vPPis, i - Vec_IntSize(vPis) );
                     assert( iObjId > 0 && iObjId < Gia_ManObjNum(p) );
-                    if ( Vec_IntEntry( p->vGateClasses, iObjId ) == 1 )
+                    if ( Vec_IntEntry( p->vGateClasses, iObjId ) > 0 )
                         continue;
                     assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
                     Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
@@ -963,7 +963,6 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
     p->vAbs  = Vec_IntAlloc( 100 );
     p->vTemp = Vec_IntAlloc( 100 );
     p->vAddedNew = Vec_IntAlloc( 100 );
-//    p->vPrioSels = Vec_IntAlloc( 100 );
     p->vObjCounts = Vec_IntAlloc( 100 );
 
     // internal data
@@ -978,6 +977,7 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
     // derive new gate map
     assert( pGia0->vGateClasses != 0 );
     p->pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) );
+    p->vCoreCounts = Vec_IntStart( Gia_ManObjNum(p->pGia) );
     // update p->pCnf->vMapping, p->pCnf->pObj2Count, p->pCnf->pObj2Clause 
     // (here are not updating p->pCnf->pVarNums because it is not needed)
     vMappingNew = Vec_IntStart( Gia_ManObjNum(p->pGia) );
@@ -1129,7 +1129,6 @@ Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
     p->vAbs = Vec_IntAlloc( 100 );
     p->vTemp = Vec_IntAlloc( 100 );
     p->vAddedNew = Vec_IntAlloc( 100 );
-//    p->vPrioSels = Vec_IntAlloc( 100 );
     // internal data
     pAig = Gia_ManToAigSimple( p->pGia );
     p->pCnf  = Cnf_DeriveOther( pAig, 1 );
@@ -1228,7 +1227,7 @@ void Gla_ManStop( Gla_Man_t * p )
     Vec_IntFreeP( &p->vObjCounts );
     Vec_IntFreeP( &p->vCla2Obj );
     Vec_IntFreeP( &p->vAddedNew );
-//    Vec_IntFreeP( &p->vPrioSels );
+    Vec_IntFreeP( &p->vCoreCounts );
     Vec_IntFreeP( &p->vTemp );
     Vec_IntFreeP( &p->vAbs );
     ABC_FREE( p->pvRefis );
@@ -1276,7 +1275,7 @@ int Gia_GlaAbsCount( Gla_Man_t * p, int fRo, int fAnd )
   SeeAlso     []
 
 ***********************************************************************/
-int Gla_ManTranslate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vMap )
+int Gla_ManTranslate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vGla, int nUsageCount )
 {
     int Value0, Value1;
     if ( Gia_ObjIsTravIdCurrent(p, pObj) )
@@ -1285,41 +1284,46 @@ int Gla_ManTranslate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vMap )
     if ( Gia_ObjIsCi(pObj) )
         return 0;
     assert( Gia_ObjIsAnd(pObj) );
-    Value0 = Gla_ManTranslate_rec( p, Gia_ObjFanin0(pObj), vMap );
-    Value1 = Gla_ManTranslate_rec( p, Gia_ObjFanin1(pObj), vMap );
+    Value0 = Gla_ManTranslate_rec( p, Gia_ObjFanin0(pObj), vGla, nUsageCount );
+    Value1 = Gla_ManTranslate_rec( p, Gia_ObjFanin1(pObj), vGla, nUsageCount );
     if ( Value0 || Value1 )
-        Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), 1 );
+        Vec_IntAddToEntry( vGla, Gia_ObjId(p, pObj), nUsageCount );
     return Value0 || Value1;
 }
 Vec_Int_t * Gla_ManTranslate( Gla_Man_t * p )
 {
-    Vec_Int_t * vRes, * vRes2;
+    Vec_Int_t * vGla, * vGla2;
     Gla_Obj_t * pObj, * pFanin;
     Gia_Obj_t * pGiaObj;
-    int i, k;
-    vRes = Vec_IntStart( Gia_ManObjNum(p->pGia) );
+    int i, k, nUsageCount;
+    vGla = Vec_IntStart( Gia_ManObjNum(p->pGia) );
     Gla_ManForEachObjAbs( p, pObj, i )
     {
-        Vec_IntWriteEntry( vRes, pObj->iGiaObj, 1 );
+        nUsageCount = Vec_IntEntry(p->vCoreCounts, pObj->iGiaObj);
+        assert( nUsageCount >= 0 );
         pGiaObj = Gla_ManGiaObj( p, pObj );
         if ( Gia_ObjIsConst0(pGiaObj) || Gia_ObjIsRo(p->pGia, pGiaObj) )
+        {
+            Vec_IntWriteEntry( vGla, pObj->iGiaObj, nUsageCount );
             continue;
+        }
         assert( Gia_ObjIsAnd(pGiaObj) );
         Gia_ManIncrementTravId( p->pGia );
         Gla_ObjForEachFanin( p, pObj, pFanin, k )
             Gia_ObjSetTravIdCurrent( p->pGia, Gla_ManGiaObj(p, pFanin) );
-        Gla_ManTranslate_rec( p->pGia, pGiaObj, vRes );
+        Gla_ManTranslate_rec( p->pGia, pGiaObj, vGla, nUsageCount );
     }
-    if ( p->pGia->vLutConfigs )
+    Vec_IntWriteEntry( vGla, 0, p->pPars->iFrame+1 );
+    if ( p->pGia->vLutConfigs ) // use mapping from new to old
     {
-        vRes2 = Vec_IntStart( Gia_ManObjNum(p->pGia0) );
+        vGla2 = Vec_IntStart( Gia_ManObjNum(p->pGia0) );
         for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
-            if ( Vec_IntEntry(vRes, i) )
-                Vec_IntWriteEntry( vRes2, Vec_IntEntry(p->pGia->vLutConfigs, i), 1 );
-        Vec_IntFree( vRes );
-        return vRes2;
+            if ( Vec_IntEntry(vGla, i) )
+                Vec_IntWriteEntry( vGla2, Vec_IntEntry(p->pGia->vLutConfigs, i), Vec_IntEntry(vGla, i) );
+        Vec_IntFree( vGla );
+        return vGla2;
     }
-    return vRes;
+    return vGla;
 }
 
 
@@ -1471,6 +1475,13 @@ void Gla_ManAddClauses( Gla_Man_t * p, int iObj, int iFrame, Vec_Int_t * vLits )
     }
     else assert( 0 );
 }
+void Gia_GlaAddToCounters( Gla_Man_t * p, Vec_Int_t * vCore )
+{
+    Gla_Obj_t * pGla;
+    int i;
+    Gla_ManForEachObjAbsVec( vCore, p, pGla, i )
+        Vec_IntAddToEntry( p->vCoreCounts, pGla->iGiaObj, 1 );
+}
 void Gia_GlaAddToAbs( Gla_Man_t * p, Vec_Int_t * vAbsAdd, int fCheck )
 {
     Gla_Obj_t * pGla;
@@ -1882,7 +1893,8 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
         }
         assert( Status == 1 );
         // valid core is obtained
-        nCoreSize = Vec_IntSize(vCore);
+        nCoreSize = Vec_IntSize( vCore );
+        Gia_GlaAddToCounters( p, vCore );
         if ( i == 0 )
             Vec_IntFree( vCore );
         else
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index cba90721..520385b8 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1683,7 +1683,7 @@ Vec_Int_t * Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses )
     {
         if ( Entry == 0 )
             continue;
-        assert( Entry == 1 );
+        assert( Entry > 0 );
         pObj = Gia_ManObj( p, i );
         Vec_IntPush( vAssigned, Gia_ObjId(p, pObj) );
         if ( Gia_ObjIsAnd(pObj) )
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 6e2c49ff..3acd3213 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1280,159 +1280,6 @@ void Gia_ManInvertConstraints( Gia_Man_t * pAig )
 
 /**Function*************************************************************
 
-  Synopsis    [Converting VTA vector to GLA vector.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta )
-{
-    Gia_Obj_t * pObj;
-    Vec_Int_t * vGla;
-    int nObjMask, nObjs = Gia_ManObjNum(p);
-    int i, Entry, nFrames = Vec_IntEntry( vVta, 0 );
-    assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
-    // get the bitmask
-    nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
-    assert( nObjs <= nObjMask );
-    // go through objects
-    vGla = Vec_IntStart( nObjs );
-    Vec_IntWriteEntry( vGla, 0, 1 );
-    Vec_IntForEachEntryStart( vVta, Entry, i, nFrames+2 )
-    {
-        pObj = Gia_ManObj( p, (Entry &  nObjMask) );
-        assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsConst0(pObj) );
-        Vec_IntWriteEntry( vGla, (Entry &  nObjMask), 1 );
-    }
-    return vGla;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Converting GLA vector to VTA vector.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames )
-{
-    Vec_Int_t * vVta;
-    int nObjBits, nObjMask, nObjs = Gia_ManObjNum(p);
-    int i, k, j, Entry, Counter, nGlaSize;
-    //. get the GLA size
-    nGlaSize = Vec_IntSum(vGla);
-    // get the bitmask
-    nObjBits = Abc_Base2Log(nObjs);
-    nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
-    assert( nObjs <= nObjMask );
-    // go through objects
-    vVta = Vec_IntAlloc( 1000 );
-    Vec_IntPush( vVta, nFrames );
-    Counter = nFrames + 2;
-    for ( i = 0; i <= nFrames; i++, Counter += i * nGlaSize )
-        Vec_IntPush( vVta, Counter );
-    for ( i = 0; i < nFrames; i++ )
-        for ( k = 0; k <= i; k++ )
-            Vec_IntForEachEntry( vGla, Entry, j )
-                if ( Entry ) 
-                    Vec_IntPush( vVta, (k << nObjBits) | j );
-    Counter = Vec_IntEntry(vVta, nFrames+1);
-    assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
-    return vVta;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Converting GLA vector to FLA vector.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_FlaConvertToGla_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vGla )
-{
-    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
-        return;
-    Gia_ObjSetTravIdCurrent(p, pObj);
-    Vec_IntWriteEntry( vGla, Gia_ObjId(p, pObj), 1 );
-    if ( Gia_ObjIsRo(p, pObj) )
-        return;
-    assert( Gia_ObjIsAnd(pObj) );
-    Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
-    Gia_FlaConvertToGla_rec( p, Gia_ObjFanin1(pObj), vGla );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Converting FLA vector to GLA vector.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla )
-{
-    Vec_Int_t * vGla;
-    Gia_Obj_t * pObj;
-    int i;
-    // mark const0 and relevant CI objects
-    Gia_ManIncrementTravId( p );
-    Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p));
-    Gia_ManForEachPi( p, pObj, i )
-        Gia_ObjSetTravIdCurrent(p, pObj);
-    Gia_ManForEachRo( p, pObj, i )
-        if ( !Vec_IntEntry(vFla, i) )
-            Gia_ObjSetTravIdCurrent(p, pObj);
-    // label all objects reachable from the PO and selected flops
-    vGla = Vec_IntStart( Gia_ManObjNum(p) );
-    Vec_IntWriteEntry( vGla, 0, 1 );
-    Gia_ManForEachPo( p, pObj, i )
-        Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
-    Gia_ManForEachRi( p, pObj, i )
-        if ( Vec_IntEntry(vFla, i) )
-            Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
-    return vGla;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Converting GLA vector to FLA vector.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla )
-{
-    Vec_Int_t * vFla;
-    Gia_Obj_t * pObj;
-    int i;
-    vFla = Vec_IntStart( Gia_ManRegNum(p) );
-    Gia_ManForEachRo( p, pObj, i )
-        if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
-            Vec_IntWriteEntry( vFla, i, 1 );
-    return vFla;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Testing the speedup due to grouping POs into batches.]
 
   Description []
@@ -1627,6 +1474,7 @@ void Gia_ObjComputeTruthTableTest( Gia_Man_t * p )
 }
 
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 5f93db11..9d06104d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -347,6 +347,7 @@ static int Abc_CommandAbc9AbsRefine          ( Abc_Frame_t * pAbc, int argc, cha
 //static int Abc_CommandAbc9AbsPba             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9GlaDerive          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9GlaRefine          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9GlaPurify          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9GlaCba             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9GlaPba             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Gla                ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -795,6 +796,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&abs_pba",      Abc_CommandAbc9AbsPba,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&gla_derive",   Abc_CommandAbc9GlaDerive,    0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&gla_refine",   Abc_CommandAbc9GlaRefine,    0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&gla_purify",   Abc_CommandAbc9GlaPurify,    0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&gla_cba",      Abc_CommandAbc9GlaCba,       0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&gla_pba",      Abc_CommandAbc9GlaPba,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&gla",          Abc_CommandAbc9Gla,          0 );
@@ -27160,6 +27162,75 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9GlaPurify( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Gia_ManGlaPurify( Gia_Man_t * p, int nPurifyRatio, int fVerbose );
+    int fMinCut = 0;
+    int nPurifyRatio = 0;
+    int c, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Rmvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'R':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nPurifyRatio = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nPurifyRatio < 0 ) 
+                goto usage;
+            break;
+        case 'm':
+            fMinCut ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9GlaPurify(): There is no AIG.\n" );
+        return 1;
+    } 
+    if ( pAbc->pGia->vGateClasses == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9GlaPurify(): There is no gate-level abstraction.\n" );
+        return 0;
+    }
+    Gia_ManGlaPurify( pAbc->pGia, nPurifyRatio, fVerbose );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &gla_purify [-R num] [-vh]\n" );
+    Abc_Print( -2, "\t         purifies gate-level abstraction by removing less frequent objects\n" );
+//    Abc_Print( -2, "\t-R num : the percetage of rare objects to remove [default = %d]\n", nPurifyRatio );
+    Abc_Print( -2, "\t-R num : remove objects with usage count less or equal than this [default = %d]\n", nPurifyRatio );
+//    Abc_Print( -2, "\t-m     : toggle using min-cut to derive the refinements [default = %s]\n", fMinCut? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+} 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Saig_ParBmc_t Pars, * pPars = &Pars;