Gate level abstraction (command &gla).

4 files changed, 1074 insertions, 10 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index b4ce11e6..dc3a3b01 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -625,6 +625,8 @@ 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 );
+/*=== giaAbsGla.c ===========================================================*/
+extern int                 Gia_GlaPerform( Gia_Man_t * p, Gia_ParVta_t * pPars );
 /*=== giaAbsVta.c ===========================================================*/
 extern void                Gia_VtaSetDefaultParams( Gia_ParVta_t * p );
 extern Vec_Ptr_t *         Gia_VtaAbsToFrames( Vec_Int_t * vAbs );
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 5dac89a6..368505e9 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -20,6 +20,9 @@
 
 #include "gia.h"
 #include "giaAig.h"
+#include "src/sat/cnf/cnf.h"
+#include "src/sat/bsat/satSolver2.h"
+#include "src/base/main/main.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -28,6 +31,63 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+typedef struct Gla_Obj_t_ Gla_Obj_t; // object
+struct Gla_Obj_t_
+{
+    int           iGiaObj;         // corresponding GIA obj
+    unsigned      fAbs      :  1;  // belongs to abstraction
+    unsigned      fCompl0   :  1;  // compl bit of the first fanin
+//    unsigned      fCompl1   :  1;  // compl bit of the second fanin
+    unsigned      fConst    :  1;  // object attribute
+    unsigned      fPi       :  1;  // object attribute
+    unsigned      fPo       :  1;  // object attribute
+    unsigned      fRo       :  1;  // object attribute
+    unsigned      fRi       :  1;  // object attribute
+    unsigned      fAnd      :  1;  // object attribute
+    unsigned      nFanins   : 24;  // fanin count
+    int           Fanins[4];       // fanins
+    Vec_Int_t     vFrames;         // variables in each timeframe
+};
+
+typedef struct Gla_Man_t_ Gla_Man_t; // manager
+struct Gla_Man_t_
+{
+    // user data
+    Gia_Man_t *   pGia;            // AIG manager
+    Gia_ParVta_t* pPars;           // parameters
+    // internal data
+    Gla_Obj_t *   pObjs;           // objects
+    int           nObjs;           // the number of objects
+    // other data
+    int           nCexes;          // the number of counter-examples
+    int           nSatVars;        // the number of SAT variables
+    Cnf_Dat_t *   pCnf;            // CNF derived for the nodes
+    sat_solver2 * pSat;            // incremental SAT solver
+    Vec_Int_t *   vCla2Obj;        // mapping of clauses into GLA objs
+    Vec_Int_t *   vTemp;           // temporary array
+    Vec_Int_t *   vAddedNew;       // temporary array
+    // statistics 
+    int           timeSat;
+    int           timeUnsat;
+    int           timeCex;
+    int           timeOther;
+};
+
+// object procedures
+static inline int         Gla_ObjId( Gla_Man_t * p, Gla_Obj_t * pObj )     { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs;  }
+static inline Gla_Obj_t * Gla_ManObj( Gla_Man_t * p, int i )               { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL;                 }
+static inline Gia_Obj_t * Gla_ManGiaObj( Gla_Man_t * p, Gla_Obj_t * pObj ) { return Gia_ManObj( p->pGia, pObj->iGiaObj );                                      }
+
+// iterator through abstracted objects
+#define Gla_ManForEachObjAbs( p, pObj )              \
+    for ( pObj = p->pObjs + 1; pObj < p->pObjs + p->nObjs; pObj++ ) if ( !pObj->fAbs ) {} else
+#define Gla_ManForEachObjAbsVec( vVec, p, pObj, i )  \
+    for ( i = 0; i < Vec_IntSize(vVec) && ((pObj = Gla_ManObj(p, Vec_IntEntry(vVec, i))),1); i++) 
+
+// iterator through fanins of an abstracted object
+#define Gla_ObjForEachFanin( p, pObj, pFanin, i )    \
+    for ( i = 0; (i < (int)pObj->nFanins) && ((pFanin = Gla_ManObj(p, pObj->Fanins[i])),1); i++ )
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -170,6 +230,732 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
     return -1;
 }
 
+
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Adds clauses for the given obj in the given frame.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gla_ManCollectFanins( Gla_Man_t * p, Gla_Obj_t * pGla, int iObj, Vec_Int_t * vFanins )
+{
+    int i, nClauses, iFirstClause, * pLit;
+    nClauses = p->pCnf->pObj2Count[pGla->iGiaObj];
+    iFirstClause = p->pCnf->pObj2Clause[pGla->iGiaObj];
+    Vec_IntClear( vFanins );
+    for ( i = iFirstClause; i < iFirstClause + nClauses; i++ )
+        for ( pLit = p->pCnf->pClauses[i]; pLit < p->pCnf->pClauses[i+1]; pLit++ )
+            if ( lit_var(*pLit) != iObj )
+                Vec_IntPushUnique( vFanins, lit_var(*pLit) );
+    assert( Vec_IntSize( vFanins ) <= 4 );
+    Vec_IntSort( vFanins, 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a new manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
+{
+    Gla_Man_t * p;
+    Aig_Man_t * pAig;
+    Gia_Obj_t * pObj;
+    Gla_Obj_t * pGla;
+    int i, * pLits;
+    // start
+    p = ABC_CALLOC( Gla_Man_t, 1 );
+    p->pGia  = pGia;
+    p->pPars = pPars;
+    p->vTemp = Vec_IntAlloc( 100 );
+    p->vAddedNew = Vec_IntAlloc( 100 );
+    // internal data
+    pAig = Gia_ManToAigSimple( p->pGia );
+    p->pCnf  = Cnf_DeriveOther( pAig );
+    Aig_ManStop( pAig );
+    // count the number of variables
+    p->nObjs = 1;
+    Gia_ManForEachObj( p->pGia, pObj, i )
+        if ( p->pCnf->pObj2Count[i] >= 0 )
+            pObj->Value = p->nObjs++;
+        else
+            pObj->Value = ~0;
+    // re-express CNF using new variable IDs
+    pLits = p->pCnf->pClauses[0];
+    for ( i = 0; i < p->pCnf->nLiterals; i++ )
+    {
+        pObj = Gia_ManObj( p->pGia, lit_var(pLits[i]) );
+        assert( ~pObj->Value );
+        pLits[i] = toLitCond( pObj->Value, lit_sign(pLits[i]) );
+    }
+    // create objects
+    p->pObjs = ABC_CALLOC( Gla_Obj_t, p->nObjs );
+    Gia_ManForEachObj( p->pGia, pObj, i )
+    {
+        if ( !~pObj->Value )
+            continue;
+        pGla = Gla_ManObj( p, pObj->Value );
+        pGla->iGiaObj = i;
+        pGla->fCompl0 = Gia_ObjFaninC0(pObj);
+//        pGla->fCompl1 = Gia_ObjFaninC1(pObj);
+        pGla->fConst  = Gia_ObjIsConst0(pObj);
+        pGla->fPi     = Gia_ObjIsPi(p->pGia, pObj);
+        pGla->fPo     = Gia_ObjIsPo(p->pGia, pObj);
+        pGla->fRi     = Gia_ObjIsRi(p->pGia, pObj);
+        pGla->fRo     = Gia_ObjIsRo(p->pGia, pObj);
+        pGla->fAnd    = Gia_ObjIsAnd(pObj);
+        if ( Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) )
+            continue;
+        if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) )
+        {
+            Gla_ManCollectFanins( p, pGla, pObj->Value, p->vTemp );
+            pGla->fConst  = Gia_ObjIsConst0(pObj);
+            pGla->nFanins = Vec_IntSize( p->vTemp );
+            memcpy( pGla->Fanins, Vec_IntArray(p->vTemp), sizeof(int) * Vec_IntSize(p->vTemp) );
+            continue;
+        }
+        assert( Gia_ObjIsRo(p->pGia, pObj) );
+        pGla->nFanins = 1;
+        pGla->Fanins[0] = Gia_ObjFanin0( Gia_ObjRoToRi(p->pGia, pObj) )->Value;
+        pGla->fCompl0  = Gia_ObjFaninC0( Gia_ObjRoToRi(p->pGia, pObj) );
+    }
+    // abstraction 
+    assert( pGia->vGateClasses != NULL );
+    for ( pGla = p->pObjs + 1; pGla < p->pObjs + p->nObjs; pGla++ )
+        pGla->fAbs = (Vec_IntEntry( pGia->vGateClasses, pGla->iGiaObj ) == 1);
+    // other 
+    p->vCla2Obj  = Vec_IntAlloc( 1000 );  Vec_IntPush( p->vCla2Obj, -1 );
+    p->pSat      = sat_solver2_new();
+    p->nSatVars  = 1;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a new manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gla_ManStop( Gla_Man_t * p )
+{
+    Gla_Obj_t * pGla;
+    for ( pGla = p->pObjs + 1; pGla < p->pObjs + p->nObjs; pGla++ )
+        ABC_FREE( pGla->vFrames.pArray );
+    Cnf_DataFree( p->pCnf );
+    sat_solver2_delete( p->pSat );
+    Vec_IntFree( p->vCla2Obj );
+    Vec_IntFree( p->vAddedNew );
+    Vec_IntFree( p->vTemp );
+    ABC_FREE( p->pObjs );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a new manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_GlaAbsCount( Gla_Man_t * p, int fRo, int fAnd )
+{
+    Gla_Obj_t * pObj;
+    int Counter = 0;
+    if ( fRo )
+        Gla_ManForEachObjAbs( p, pObj )
+            Counter += (pObj->fRo && pObj->fAbs);
+    else if ( fAnd )
+        Gla_ManForEachObjAbs( p, pObj )
+            Counter += (pObj->fAnd && pObj->fAbs);
+    else
+        Gla_ManForEachObjAbs( p, pObj )
+            Counter += (pObj->fAbs);
+    return Counter;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives new abstraction map.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gla_ManTranslate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vMap )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    assert( Gia_ObjIsAnd(pObj) );
+    Gla_ManTranslate_rec( p, Gia_ObjFanin0(pObj), vMap );
+    Gla_ManTranslate_rec( p, Gia_ObjFanin1(pObj), vMap );
+    Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), 1 );
+}
+Vec_Int_t * Gla_ManTranslate( Gla_Man_t * p )
+{
+    Vec_Int_t * vRes;
+    Gla_Obj_t * pObj, * pFanin;
+    Gia_Obj_t * pGiaObj;
+    int k;
+    vRes = Vec_IntStart( Gia_ManObjNum(p->pGia) );
+    Gla_ManForEachObjAbs( p, pObj )
+    {
+        pGiaObj = Gla_ManGiaObj( p, pObj );
+        Vec_IntWriteEntry( vRes, pObj->iGiaObj, 1 );
+        if ( Gia_ObjIsConst0(pGiaObj) || Gia_ObjIsRo(p->pGia, pGiaObj) )
+            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, Gla_ManGiaObj(p, pObj), vRes );
+    }
+    return vRes;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collect pseudo-PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gla_ManCollectPPis( Gla_Man_t * p )
+{
+    Vec_Int_t * vPPis;
+    Gla_Obj_t * pObj, * pFanin;
+    int k;
+    vPPis = Vec_IntAlloc( 1000 );
+    Gla_ManForEachObjAbs( p, pObj )
+    {
+        assert( pObj->fConst || pObj->fRo || pObj->fAnd );
+        Gla_ObjForEachFanin( p, pObj, pFanin, k )
+            if ( !pFanin->fPi && !pFanin->fAbs )
+                Vec_IntPush( vPPis, pObj->Fanins[k] );
+    }
+    Vec_IntUniqify( vPPis );
+    Vec_IntReverseOrder( vPPis );
+    return vPPis;
+}
+int Gla_ManCountPPis( Gla_Man_t * p )
+{
+    Vec_Int_t * vPPis = Gla_ManCollectPPis( p );
+    int RetValue = Vec_IntSize( vPPis );
+    Vec_IntFree( vPPis );
+    return RetValue;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Adds CNF for the given timeframe.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gla_ManGetVar( Gla_Man_t * p, int iObj, int iFrame )
+{
+    Gla_Obj_t * pGla = Gla_ManObj( p, iObj );
+    int iVar = Vec_IntGetEntry( &pGla->vFrames, iFrame );
+    assert( !pGla->fPo && !pGla->fRi );
+    if ( iVar == 0 )
+    {
+        Vec_IntSetEntry( &pGla->vFrames, iFrame, (iVar = p->nSatVars++) );
+        // remember the change
+        Vec_IntPush( p->vAddedNew, iObj );
+        Vec_IntPush( p->vAddedNew, iFrame );
+    }
+    return iVar;
+}
+void Gla_ManAddClauses( Gla_Man_t * p, int iObj, int iFrame, Vec_Int_t * vLits )
+{
+    Gla_Obj_t * pGlaObj = Gla_ManObj( p, iObj );
+    int iVar, iVar1, iVar2;
+    if ( iObj == 4753 )
+    {
+        int s = 0;
+    }
+    if ( pGlaObj->fConst )
+    {
+        iVar = Gla_ManGetVar( p, iObj, iFrame );
+        sat_solver2_add_const( p->pSat, iVar, 1, 0 );
+        // remember the clause
+        Vec_IntPush( p->vCla2Obj, iObj );
+    }
+    else if ( pGlaObj->fRo )
+    {
+        assert( pGlaObj->nFanins == 1 );
+        if ( iFrame == 0 )
+        {
+            iVar = Gla_ManGetVar( p, iObj, iFrame );
+            sat_solver2_add_const( p->pSat, iVar, 1, 0 );
+            // remember the clause
+            Vec_IntPush( p->vCla2Obj, iObj );
+        }
+        else
+        {
+            iVar1 = Gla_ManGetVar( p, iObj, iFrame );
+//            pGlaObj = Gla_ManObj( p, pGlaObj->Fanins[0] );
+//            assert( pGlaObj->fRo && pGlaObj->nFanins == 1 );
+//            assert( Vec_IntSize(&pGlaObj->vFrames) == 0 );
+            iVar2 = Gla_ManGetVar( p, pGlaObj->Fanins[0], iFrame-1 );
+            sat_solver2_add_buffer( p->pSat, iVar1, iVar2, pGlaObj->fCompl0, 0 );
+            // remember the clause
+            Vec_IntPush( p->vCla2Obj, iObj );
+            Vec_IntPush( p->vCla2Obj, iObj );
+        }
+    }
+    else if ( pGlaObj->fAnd )
+    {
+        int i, RetValue, nClauses, iFirstClause, * pLit;
+        nClauses = p->pCnf->pObj2Count[pGlaObj->iGiaObj];
+        iFirstClause = p->pCnf->pObj2Clause[pGlaObj->iGiaObj];
+        for ( i = iFirstClause; i < iFirstClause + nClauses; i++ )
+        {
+            Vec_IntClear( vLits );
+            for ( pLit = p->pCnf->pClauses[i]; pLit < p->pCnf->pClauses[i+1]; pLit++ )
+            {
+                iVar = Gla_ManGetVar( p, lit_var(*pLit), iFrame );
+                Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
+            }
+            RetValue = sat_solver2_addclause( p->pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
+            assert( RetValue );
+            // remember the clause
+            Vec_IntPush( p->vCla2Obj, iObj );
+        }
+    }
+    else assert( 0 );
+}
+void Gia_GlaAddToAbs( Gla_Man_t * p, Vec_Int_t * vAbsAdd, int fCheck )
+{
+    Gla_Obj_t * pGla;
+    int i;
+    Gla_ManForEachObjAbsVec( vAbsAdd, p, pGla, i )
+    {
+        assert( !fCheck || pGla->fAbs == 0 );
+        pGla->fAbs = 1;
+        // remember the change
+        Vec_IntPush( p->vAddedNew, Gla_ObjId(p, pGla) );
+        Vec_IntPush( p->vAddedNew, -1 );
+    }
+}
+void Gia_GlaAddTimeFrame( Gla_Man_t * p, int f )
+{
+    Gla_Obj_t * pObj;
+    Gla_ManForEachObjAbs( p, pObj )
+        Gla_ManAddClauses( p, Gla_ObjId(p, pObj), f, p->vTemp );
+    sat_solver2_simplify( p->pSat );
+}
+void Gia_GlaAddOneSlice( Gla_Man_t * p, int fCur, Vec_Int_t * vCore )
+{
+    int f, i, iGlaObj;
+    for ( f = fCur; f >= 0; f-- )
+        Vec_IntForEachEntry( vCore, iGlaObj, i )
+            Gla_ManAddClauses( p, iGlaObj, f, p->vTemp );
+    sat_solver2_simplify( p->pSat );
+}
+void Gla_ManRollBack( Gla_Man_t * p )
+{
+    int i, iObj, iFrame;
+    Vec_IntForEachEntryDouble( p->vAddedNew, iObj, iFrame, i )
+    {
+        if ( iFrame == -1 )
+        {
+            assert( Gla_ManObj(p, iObj)->fAbs == 1 );
+            Gla_ManObj(p, iObj)->fAbs = 0;
+        }
+        else
+        {
+            assert( Vec_IntEntry( &Gla_ManObj(p, iObj)->vFrames, iFrame ) > 0 );
+            Vec_IntWriteEntry( &Gla_ManObj(p, iObj)->vFrames, iFrame, 0 );
+        }
+    }
+}
+
+
+            
+
+
+/**Function*************************************************************
+
+  Synopsis    [Finds the set of clauses involved in the UNSAT core.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gla_ManGetOutLit( Gla_Man_t * p, int f )
+{
+    Gia_Obj_t * pObj   = Gia_ManPo(p->pGia, 0);
+    Gia_Obj_t * pFanin = Gia_ObjFanin0(pObj);
+    Gla_Obj_t * pGla   = Gla_ManObj(p, pFanin->Value);
+    int iSat = Vec_IntEntry( &pGla->vFrames, f );
+    assert( iSat > 0 );
+    return Abc_Var2Lit( iSat, Gia_ObjFaninC0(pObj) );
+}
+Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, Vec_Int_t * vCla2Obj, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls )
+{
+    Vec_Int_t * vCore;
+    int iLit = Gla_ManGetOutLit( p, f );
+    int nConfPrev = pSat->stats.conflicts;
+    int i, Entry, RetValue, clk = clock();
+    if ( piRetValue )
+        *piRetValue = 1;
+    // solve the problem
+    RetValue = sat_solver2_solve( pSat, &iLit, &iLit+1, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+    if ( pnConfls )
+        *pnConfls = (int)pSat->stats.conflicts - nConfPrev;
+    if ( RetValue == l_Undef )
+    {
+        if ( piRetValue )
+            *piRetValue = -1;
+        return NULL;
+    }
+    if ( RetValue == l_True )
+    {
+        if ( piRetValue )
+            *piRetValue = 0;
+        return NULL;
+    }
+    if ( fVerbose )
+    {
+//        Abc_Print( 1, "%6d", (int)pSat->stats.conflicts - nConfPrev );
+//        Abc_Print( 1, "UNSAT after %7d conflicts.      ", pSat->stats.conflicts );
+//        Abc_PrintTime( 1, "Time", clock() - clk );
+    }
+    assert( RetValue == l_False );
+
+    // derive the UNSAT core
+    clk = clock();
+    vCore = (Vec_Int_t *)Sat_ProofCore( pSat );
+    if ( fVerbose )
+    {
+//        Abc_Print( 1, "Core is %8d clauses (out of %8d).   ", Vec_IntSize(vCore), sat_solver2_nclauses(pSat) );
+//        Abc_PrintTime( 1, "Time", clock() - clk );
+    }
+
+    // remap core into original objects 
+    Vec_IntForEachEntry( vCore, Entry, i )
+        Vec_IntWriteEntry( vCore, i, Vec_IntEntry(p->vCla2Obj, Entry) );
+    Vec_IntUniqify( vCore );
+    Vec_IntReverseOrder( vCore );
+    if ( fVerbose )
+    {
+//        Abc_Print( 1, "Core is %8d vars    (out of %8d).   ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) );
+//        Abc_PrintTime( 1, "Time", clock() - clk );
+    }
+    return vCore;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfls, int nCexes, int Time )
+{
+    Abc_Print( 1, "%3d :", nFrames-1 );
+    Abc_Print( 1, "%6d", Gia_GlaAbsCount(p, 0, 0) );
+    Abc_Print( 1, "%5d", Gla_ManCountPPis(p) );
+    Abc_Print( 1, "%5d", Gia_GlaAbsCount(p, 1, 0) );
+    Abc_Print( 1, "%6d", Gia_GlaAbsCount(p, 0, 1) );
+    Abc_Print( 1, "%8d", nConfls );
+    if ( nCexes == 0 )
+        Abc_Print( 1, "%5c", '-' ); 
+    else
+        Abc_Print( 1, "%5d", nCexes ); 
+    Abc_Print( 1, " %6d", nCoreSize > 0 ? nCoreSize : 0 ); 
+    Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) ); 
+    Abc_Print( 1, "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) );
+    Abc_Print( 1, "%s", nCoreSize > 0 ? "\n" : "\r" );
+    fflush( stdout );
+}
+void Gla_ManReportMemory( Gla_Man_t * p )
+{
+    Gla_Obj_t * pGla;
+    double memTot = 0;
+    double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t);
+    double memSat = sat_solver2_memory( p->pSat );
+    double memPro = sat_solver2_memory_proof( p->pSat );
+    double memMap = p->nObjs * sizeof(Gla_Obj_t);
+    double memOth = sizeof(Gla_Man_t);
+    for ( pGla = p->pObjs; pGla < p->pObjs + p->nObjs; pGla++ )
+        memMap += Vec_IntCap(&pGla->vFrames) * sizeof(int);
+    memOth += Vec_IntCap(p->vCla2Obj) * sizeof(int);
+    memOth += Vec_IntCap(p->vAddedNew) * sizeof(int);
+    memOth += Vec_IntCap(p->vTemp) * sizeof(int);
+    memTot = memAig + memSat + memPro + memMap + memOth;
+    ABC_PRMP( "Memory: AIG  ", memAig, memTot );
+    ABC_PRMP( "Memory: SAT  ", memSat, memTot );
+    ABC_PRMP( "Memory: Proof", memPro, memTot );
+    ABC_PRMP( "Memory: Map  ", memMap, memTot );
+    ABC_PRMP( "Memory: Other", memOth, memTot );
+    ABC_PRMP( "Memory: TOTAL", memTot, memTot );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Send abstracted model or send cancel.]
+
+  Description [Counter-example will be sent automatically when &vta terminates.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose )
+{
+    char * pFileName = p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig";
+    Gia_Man_t * pAbs;
+    if ( fVerbose )
+        Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
+//    if ( !Abc_FrameIsBridgeMode() )
+//        return;
+    // create gate classes
+    Vec_IntFreeP( &p->pGia->vGateClasses );
+    p->pGia->vGateClasses = Gla_ManTranslate( p );
+    // create abstrated model
+    pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses );
+    Vec_IntFreeP( &p->pGia->vGateClasses );
+    // send it out
+    Gia_WriteAiger( pAbs, pFileName, 0, 0 );
+    Gia_ManStop( pAbs );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs gate-level abstraction]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
+{
+    Gla_Man_t * p;
+    Vec_Int_t * vCore, * vPPis;
+    Abc_Cex_t * pCex = NULL;
+    int i, f, nConfls, Status, nCoreSize, RetValue = -1;
+    int clk = clock(), clk2;
+    // preconditions
+    assert( Gia_ManPoNum(pAig) == 1 );
+    assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
+    // start the manager
+    p = Gla_ManStart( pAig, pPars );
+    p->pSat->fVerbose = p->pPars->fVerbose;
+    sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax );
+    // set runtime limit
+    if ( p->pPars->nTimeOut )
+        sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 );
+    // perform initial abstraction
+    if ( p->pPars->fVerbose )
+    {
+        Abc_Print( 1, "Running variable-timeframe abstraction (VTA) with the following parameters:\n" );
+        Abc_Print( 1, "FrameStart = %d  FrameMax = %d  Conf = %d  Timeout = %d. RatioMin = %d %%.\n", 
+            p->pPars->nFramesStart, p->pPars->nFramesMax, p->pPars->nConfLimit, p->pPars->nTimeOut, pPars->nRatioMin );
+        Abc_Print( 1, "Frame   Abs  PPI   FF   AND   Confl  Cex   Core    SatVar      Time\n" );
+    }
+    for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
+    {
+        int nConflsBeg = sat_solver2_nconflicts(p->pSat);
+        p->pPars->iFrame = f;
+        // load timeframe
+        Gia_GlaAddTimeFrame( p, f );
+        // create bookmark to be used for rollback
+//            sat_solver2_reducedb( p->pSat );
+        sat_solver2_bookmark( p->pSat );
+        Vec_IntClear( p->vAddedNew );
+//        nClaOld = Vec_IntSize( p->vCla2Obj );
+        // iterate as long as there are counter-examples
+        for ( i = 0; ; i++ )
+        { 
+            clk2 = clock();
+            vCore = Gla_ManUnsatCore( p, f, p->vCla2Obj, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
+            assert( (vCore != NULL) == (Status == 1) );
+            if ( Status == -1 ) // resource limit is reached
+                goto finish;
+            if ( vCore != NULL )
+            {
+                p->timeUnsat += clock() - clk2;
+                break;
+            }
+            p->timeSat += clock() - clk2;
+            assert( Status == 0 );
+            p->nCexes++;
+            // perform the refinement
+            clk2 = clock();
+//            pCex = Vta_ManRefineAbstraction( p, f );
+            pCex = NULL;
+
+            vPPis = Gla_ManCollectPPis( p );
+            Gia_GlaAddToAbs( p, vPPis, 1 );
+            Gia_GlaAddOneSlice( p, f, vPPis );
+            Vec_IntFree( vPPis );
+
+            p->timeCex += clock() - clk2;
+            if ( pCex != NULL )
+            {
+                RetValue = 0;
+                goto finish;
+            }
+            // print the result (do not count it towards change)
+            if ( p->pPars->fVerbose )
+            Gla_ManAbsPrintFrame( p, -1, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk );
+        }
+        assert( Status == 1 );
+        // valid core is obtained
+        nCoreSize = Vec_IntSize(vCore);
+        if ( i == 0 )
+            Vec_IntFree( vCore );
+        else
+        {
+            // update the SAT solver
+            sat_solver2_rollback( p->pSat );
+            // update storage
+            Gla_ManRollBack( p );
+            Vec_IntShrink( p->vCla2Obj, (int)p->pSat->stats.clauses+1 );
+            // load this timeframe
+            Gia_GlaAddToAbs( p, vCore, 0 );
+            Gia_GlaAddOneSlice( p, f, vCore );
+            Vec_IntFree( vCore );
+            // run SAT solver
+            clk2 = clock();
+            vCore = Gla_ManUnsatCore( p, f, p->vCla2Obj, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
+            p->timeUnsat += clock() - clk2;
+            assert( (vCore != NULL) == (Status == 1) );
+            Vec_IntFree( vCore );
+            if ( Status == -1 ) // resource limit is reached
+                break;
+            if ( Status == 0 )
+            {
+    //            Vta_ManSatVerify( p );
+                // make sure, there was no initial abstraction (otherwise, it was invalid)
+                assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart );
+    //            pCex = Vga_ManDeriveCex( p );
+                RetValue = 0;
+                break;
+            }
+        }
+        // print the result
+        if ( p->pPars->fVerbose )
+        Gla_ManAbsPrintFrame( p, nCoreSize, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk );
+
+        // dump the model
+        if ( p->pPars->fDumpVabs && (f & 1) )
+        {
+            Abc_FrameSetCex( NULL );
+            Abc_FrameSetNFrames( f+1 );
+            Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "write_status gla.status" );
+            Gia_GlaDumpAbsracted( p, pPars->fVerbose );
+        }
+
+        // check if the number of objects is below limit
+        if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 )
+        {
+            Status = -1;
+            break;
+        }
+    }
+finish:
+    // analize the results
+    if ( pCex == NULL )
+    {
+        if ( pAig->vGateClasses != NULL )
+            Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
+        Vec_IntFreeP( &pAig->vGateClasses );
+        pAig->vGateClasses = Gla_ManTranslate( p );
+        if ( Status == -1 )
+        {
+            if ( p->pPars->nTimeOut && time(NULL) >= p->pSat->nRuntimeLimit ) 
+                Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d.  ", p->pPars->nTimeOut, f );
+            else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
+                Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d.  ", pPars->nConfLimit, f );
+            else if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 )
+                Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d.  ", pPars->nRatioMin, f );
+            else
+                Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d.  ", f );
+        }
+        else
+            Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction.  ", f );
+    }
+    else
+    {
+        ABC_FREE( p->pGia->pCexSeq );
+        p->pGia->pCexSeq = pCex;
+        if ( !Gia_ManVerifyCex( p->pGia, pCex, 0 ) )
+            Abc_Print( 1, "    Gia_GlaPerform(): CEX verification has failed!\n" );
+        Abc_Print( 1, "Counter-example detected in frame %d.  ", f );
+        p->pPars->iFrame = pCex->iFrame - 1;
+    }
+    Abc_PrintTime( 1, "Time", clock() - clk );
+
+    p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex;
+    ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat,  clock() - clk );
+    ABC_PRTP( "Runtime: Solver SAT  ", p->timeSat,    clock() - clk );
+    ABC_PRTP( "Runtime: Refinement  ", p->timeCex,    clock() - clk );
+    ABC_PRTP( "Runtime: Other       ", p->timeOther,  clock() - clk );
+    ABC_PRTP( "Runtime: TOTAL       ", clock() - clk, clock() - clk );
+    Gla_ManReportMemory( p );
+
+    Gla_ManStop( p );
+    fflush( stdout );
+    return RetValue;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index cf19947a..17a85bad 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -57,6 +57,7 @@ struct Gia_ManBmc_t_
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#define SAIG_TER_NON 0
 #define SAIG_TER_ZER 1
 #define SAIG_TER_ONE 2
 #define SAIG_TER_UND 3
@@ -91,6 +92,13 @@ static inline void Saig_ManBmcSimInfoSet( unsigned * pInfo, Aig_Obj_t * pObj, in
     pInfo[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
 }
 
+static inline int Saig_ManBmcSimInfoClear( unsigned * pInfo, Aig_Obj_t * pObj )
+{
+    int Value = Saig_ManBmcSimInfoGet( pInfo, pObj );
+    pInfo[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
+    return Value;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Returns the number of LIs with binary ternary info.]
@@ -220,6 +228,97 @@ void Saig_ManBmcTerSimTest( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Count the number of non-ternary per frame.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManBmcCountNonternary_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vInfos, unsigned * pInfo, int f, int * pCounter )
+{ 
+    int Value = Saig_ManBmcSimInfoClear( pInfo, pObj );
+    if ( Value == SAIG_TER_NON )
+        return 0;
+    assert( f >= 0 );
+    pCounter[f] += (Value == SAIG_TER_UND);
+    if ( Saig_ObjIsPi(p, pObj) || (f == 0 && Saig_ObjIsLo(p, pObj)) || Aig_ObjIsConst1(pObj) )
+        return 0;
+    if ( Saig_ObjIsLi(p, pObj) )
+        return Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(pObj), vInfos, pInfo, f, pCounter );
+    if ( Saig_ObjIsLo(p, pObj) )
+        return Saig_ManBmcCountNonternary_rec( p, Saig_ObjLoToLi(p, pObj), vInfos, (unsigned *)Vec_PtrEntry(vInfos, f-1), f-1, pCounter );
+    assert( Aig_ObjIsNode(pObj) );
+    Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(pObj), vInfos, pInfo, f, pCounter );
+    Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin1(pObj), vInfos, pInfo, f, pCounter );
+    return 0;
+}
+void Saig_ManBmcCountNonternary( Aig_Man_t * p, Vec_Ptr_t * vInfos, int iFrame )
+{
+    int i, * pCounters = ABC_CALLOC( int, iFrame + 1 );
+    unsigned * pInfo = (unsigned *)Vec_PtrEntry(vInfos, iFrame);
+    assert( Saig_ManBmcSimInfoGet( pInfo, Aig_ManCo(p, 0) ) == SAIG_TER_UND );
+    Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(Aig_ManCo(p, 0)), vInfos, pInfo, iFrame, pCounters );
+    for ( i = 0; i <= iFrame; i++ )
+        printf( "%d=%d ", i, pCounters[i] );
+    printf( "\n" );
+    ABC_FREE( pCounters );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of POs with binary ternary info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManBmcTerSimCount01Po( Aig_Man_t * p, unsigned * pInfo )
+{
+    Aig_Obj_t * pObj;
+    int i, Counter = 0;
+    Saig_ManForEachPo( p, pObj, i )
+        Counter += (Saig_ManBmcSimInfoGet(pInfo, pObj) != SAIG_TER_UND);
+    return Counter;
+}
+Vec_Ptr_t * Saig_ManBmcTerSimPo( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vInfos;
+    unsigned * pInfo = NULL;
+    int i, nPoBin;
+    vInfos = Vec_PtrAlloc( 100 );
+    for ( i = 0; ; i++ )
+    {
+        if ( i % 100 == 0 )
+            printf( "Frame %5d\n", i );
+        pInfo = Saig_ManBmcTerSimOne( p, pInfo );
+        Vec_PtrPush( vInfos, pInfo );
+        nPoBin = Saig_ManBmcTerSimCount01Po( p, pInfo );
+        if ( nPoBin < Saig_ManPoNum(p) )
+            break;
+    }
+    printf( "Detected terminary PO in frame %d.\n", i );
+    Saig_ManBmcCountNonternary( p, vInfos, i );
+    return vInfos;
+}
+void Saig_ManBmcTerSimTestPo( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vInfos;
+    vInfos = Saig_ManBmcTerSimPo( p );
+    Vec_PtrFreeFree( vInfos );
+}
+
+
+
+
+/**Function*************************************************************
+
   Synopsis    [Collects internal nodes in the DFS order.]
 
   Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c7c811f0..2b0bd0af 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -349,6 +349,7 @@ static int Abc_CommandAbc9GlaDerive          ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9GlaRefine          ( 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 );
 static int Abc_CommandAbc9Vta                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Vta2Gla            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Reparam            ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -793,6 +794,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&gla_refine",   Abc_CommandAbc9GlaRefine,    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 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&vta",          Abc_CommandAbc9Vta,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&vta_gla",      Abc_CommandAbc9Vta2Gla,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&reparam",      Abc_CommandAbc9Reparam,      0 );
@@ -9211,20 +9213,15 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig );
     extern Aig_Man_t * Abc_NtkToDarBmc( Abc_Ntk_t * pNtk, Vec_Int_t ** pvMap );
     extern void Abc2_NtkTestGia( char * pFileName, int fVerbose );
+    extern void Saig_ManBmcTerSimTestPo( Aig_Man_t * p );
 
     if ( pNtk )
     {
-/*
+
         Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
-        if ( fNewAlgo )
-            Saig_IsoDetectFast( pAig );
-        else
-        {
-            Aig_Man_t * pRes = Iso_ManTest( pAig, fVerbose );
-            Aig_ManStopP( &pRes );
-        }
+        Saig_ManBmcTerSimTestPo( pAig );
         Aig_ManStop( pAig );
-*/
+
 /*
         extern Abc_Ntk_t * Abc_NtkShareXor( Abc_Ntk_t * pNtk );
         Abc_Ntk_t * pNtkRes = Abc_NtkShareXor( pNtk );
@@ -27370,6 +27367,186 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_ParVta_t Pars, * pPars = &Pars;
+    int c;
+    Gia_VtaSetDefaultParams( pPars );
+    pPars->nLearntMax = 100000;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrdvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFramesMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFramesMax < 0 ) 
+                goto usage;
+            break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFramesStart = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFramesStart < 0 ) 
+                goto usage;
+            break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFramesPast = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFramesPast < 0 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nConfLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nConfLimit < 0 ) 
+                goto usage;
+            break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nLearntMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nLearntMax < 0 ) 
+                goto usage;
+            break;
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nTimeOut = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nTimeOut < 0 ) 
+                goto usage;
+            break;
+        case 'R':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nRatioMin = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nRatioMin < 0 ) 
+                goto usage;
+            break;
+        case 'A':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-A\" should be followed by a file name.\n" );
+                goto usage;
+            }
+            pPars->pFileVabs = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
+        case 't':
+            pPars->fUseTermVars ^= 1;
+            break;
+        case 'r':
+            pPars->fUseRollback ^= 1;
+            break;
+        case 'd':
+            pPars->fDumpVabs ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "There is no AIG.\n" );
+        return 0;
+    } 
+    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
+    {
+        Abc_Print( -1, "The network is combinational.\n" );
+        return 0;
+    }
+    if ( Gia_ManPoNum(pAbc->pGia) > 1 )
+    {
+        Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" );
+        return 0;
+    }
+    if ( pPars->nFramesMax < 0 )
+    {
+        Abc_Print( 1, "The number of starting frames should be a positive integer.\n" );
+        return 0;
+    }
+    if ( pPars->nFramesMax && pPars->nFramesStart > pPars->nFramesMax )
+    {
+        Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" );
+        return 0;
+    }
+    if ( pPars->nFramesStart < 1 )
+    {
+        Abc_Print( 1, "The starting frame should be 1 or larger.\n" );
+        return 0;
+    }
+    pAbc->Status  = Gia_GlaPerform( pAbc->pGia, pPars );
+    pAbc->nFrames = pPars->iFrame;
+    Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &gla [-FSCLTR num] [-A file] [-dvh]\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 );
+//    Abc_Print( -2, "\t-P num  : the number of previous frames for UNSAT core [default = %d]\n", pPars->nFramesPast );
+    Abc_Print( -2, "\t-C num  : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit );
+    Abc_Print( -2, "\t-L num  : the max number of learned clauses to keep (0=unused) [default = %d]\n", pPars->nLearntMax );
+    Abc_Print( -2, "\t-T num  : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
+    Abc_Print( -2, "\t-R num  : minimum percentage of abstracted objects (0<=num<=100) [default = %d]\n", pPars->nRatioMin );
+    Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"glabs.aig\"]\n" );
+//    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 a file [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;
+} 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_ParVta_t Pars, * pPars = &Pars;
@@ -27486,7 +27663,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pGia == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9AbsCba(): There is no AIG.\n" );
+        Abc_Print( -1, "There is no AIG.\n" );
         return 1;
     } 
     if ( Gia_ManRegNum(pAbc->pGia) == 0 )