New proof-based abstraction code.

7 files changed, 747 insertions, 64 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 64867307..2471e71c 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -3503,10 +3503,6 @@ SOURCE=.\src\aig\saig\saigAbsCba.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\saig\saigAbsGla.c
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\aig\saig\saigAbsPba.c
 # End Source File
 # Begin Source File
@@ -3551,6 +3547,14 @@ SOURCE=.\src\aig\saig\saigDup.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\saig\saigGlaCba.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\saig\saigGlaPba.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\saig\saigHaig.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 5f2b94a4..d3165526 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -603,7 +603,8 @@ Gia_Man_t *                Gia_ManCexAbstractionDerive( Gia_Man_t * pGia );
 int                        Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose );
 extern int                 Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame );
 extern int                 Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars );
-extern int                 Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fUseCnf );
+extern int                 Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf );
+extern int                 Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars );
 /*=== giaAiger.c ===========================================================*/
 extern int                 Gia_FileSize( char * pFileName );
 extern Gia_Man_t *         Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck );
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index ba50b238..54b65484 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -379,7 +379,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit
 ***********************************************************************/
 int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf )
 {
-    extern Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose );
+    extern Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose );
     Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
     Vec_Int_t * vGateClasses;
     Aig_Man_t * pAig;
@@ -393,7 +393,43 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf )
 */
     // perform abstraction
     pAig = Gia_ManToAigSimple( pGia );
-    vGateClasses = Aig_GlaManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose );
+    vGateClasses = Aig_Gla1ManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose );
+    Aig_ManStop( pAig );
+
+    // update the map
+    Vec_IntFreeP( &pGia->vGateClasses );
+    pGia->vGateClasses = vGateClasses;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive unrolled timeframes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars )
+{
+    extern Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose );
+    Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
+    Vec_Int_t * vGateClasses;
+    Aig_Man_t * pAig;
+/*
+    // check if flop classes are given
+    if ( pGia->vGateClasses == NULL )
+    {
+        Abc_Print( 0, "Initial gate map is not given. Trivial abstraction is assumed.\n" );
+        pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(pGia) );
+    }
+*/
+    // perform abstraction
+    pAig = Gia_ManToAigSimple( pGia );
+    vGateClasses = Aig_Gla2ManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fVerbose );
     Aig_ManStop( pAig );
 
     // update the map
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index 4efc1d80..df6fd7cb 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -1,6 +1,5 @@
 SRC +=    src/aig/saig/saigAbs.c \
     src/aig/saig/saigAbsCba.c \
-    src/aig/saig/saigAbsGla.c \
     src/aig/saig/saigAbsPba.c \
     src/aig/saig/saigAbsStart.c \
     src/aig/saig/saigAbsVfa.c \
@@ -12,6 +11,8 @@ SRC +=    src/aig/saig/saigAbs.c \
     src/aig/saig/saigConstr.c \
     src/aig/saig/saigConstr2.c \
     src/aig/saig/saigDup.c \
+    src/aig/saig/saigGlaCba.c \
+    src/aig/saig/saigGlaPba.c \
     src/aig/saig/saigHaig.c \
     src/aig/saig/saigInd.c \
     src/aig/saig/saigIoa.c \
diff --git a/src/aig/saig/saigAbsGla.c b/src/aig/saig/saigGlaCba.c
index 69b4cb66..8fca4796 100644
--- a/src/aig/saig/saigAbsGla.c
+++ b/src/aig/saig/saigGlaCba.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [saigAbsGla.c]
+  FileName    [saigGlaCba.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: saigAbsGla.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: saigGlaCba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -29,8 +29,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Aig_GlaMan_t_ Aig_GlaMan_t;
-struct Aig_GlaMan_t_
+typedef struct Aig_Gla1Man_t_ Aig_Gla1Man_t;
+struct Aig_Gla1Man_t_
 {
     // user data
     Aig_Man_t *    pAig;
@@ -79,7 +79,7 @@ struct Aig_GlaMan_t_
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Aig_GlaAddConst( sat_solver * pSat, int iVar, int fCompl )
+static inline int Aig_Gla1AddConst( sat_solver * pSat, int iVar, int fCompl )
 {
     lit Lit = toLitCond( iVar, fCompl );
     if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) )
@@ -98,7 +98,7 @@ static inline int Aig_GlaAddConst( sat_solver * pSat, int iVar, int fCompl )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Aig_GlaAddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl )
+static inline int Aig_Gla1AddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl )
 {
     lit Lits[2];
 
@@ -126,7 +126,7 @@ static inline int Aig_GlaAddBuffer( sat_solver * pSat, int iVar0, int iVar1, int
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 )
+static inline int Aig_Gla1AddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 )
 {
     lit Lits[3];
 
@@ -160,7 +160,7 @@ static inline int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iV
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Aig_GlaCollectAssigned_( Aig_Man_t * p, Vec_Int_t * vGateClasses )
+Vec_Int_t * Aig_Gla1CollectAssigned_( Aig_Man_t * p, Vec_Int_t * vGateClasses )
 {
     Vec_Int_t * vAssigned;
     Aig_Obj_t * pObj;
@@ -197,7 +197,7 @@ Vec_Int_t * Aig_GlaCollectAssigned_( Aig_Man_t * p, Vec_Int_t * vGateClasses )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_GlaCollectAbstr( Aig_GlaMan_t * p )
+void Aig_Gla1CollectAbstr( Aig_Gla1Man_t * p )
 {
     Aig_Obj_t * pObj;
     int i, Entry;
@@ -210,20 +210,20 @@ void Aig_GlaCollectAbstr( Aig_GlaMan_t * p )
         assert( Entry == 1 );
         pObj = Aig_ManObj( p->pAig, i );
         if ( Vec_IntFind( p->vAssigned, Aig_ObjId(pObj) ) == -1 )
-            printf( "Aig_GlaCollectAbstr(): Object not found\n" );
+            printf( "Aig_Gla1CollectAbstr(): Object not found\n" );
         if ( Aig_ObjIsNode(pObj) )
         {
             if ( Vec_IntFind( p->vAssigned, Aig_ObjFaninId0(pObj) ) == -1 )
-                printf( "Aig_GlaCollectAbstr(): Node's fanin is not found\n" );
+                printf( "Aig_Gla1CollectAbstr(): Node's fanin is not found\n" );
             if ( Vec_IntFind( p->vAssigned, Aig_ObjFaninId1(pObj) ) == -1 )
-                printf( "Aig_GlaCollectAbstr(): Node's fanin is not found\n" );
+                printf( "Aig_Gla1CollectAbstr(): Node's fanin is not found\n" );
         }
         else if ( Saig_ObjIsLo(p->pAig, pObj) ) 
         {
             Aig_Obj_t * pObjLi;
             pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
             if ( Vec_IntFind( p->vAssigned, Aig_ObjFaninId0(pObjLi) ) == -1 )
-                printf( "Aig_GlaCollectAbstr(): Flop's fanin is not found\n" );
+                printf( "Aig_Gla1CollectAbstr(): Flop's fanin is not found\n" );
         }
         else assert( Aig_ObjIsConst1(pObj) );
     }
@@ -258,13 +258,13 @@ void Aig_GlaCollectAbstr( Aig_GlaMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_GlaDeriveAbs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
+void Aig_Gla1DeriveAbs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
 {
     if ( pObj->pData )
         return;
     assert( Aig_ObjIsNode(pObj) );
-    Aig_GlaDeriveAbs_rec( pNew, Aig_ObjFanin0(pObj) );
-    Aig_GlaDeriveAbs_rec( pNew, Aig_ObjFanin1(pObj) );
+    Aig_Gla1DeriveAbs_rec( pNew, Aig_ObjFanin0(pObj) );
+    Aig_Gla1DeriveAbs_rec( pNew, Aig_ObjFanin1(pObj) );
     pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
 }
 
@@ -279,7 +279,7 @@ void Aig_GlaDeriveAbs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p )
+Aig_Man_t * Aig_Gla1DeriveAbs( Aig_Gla1Man_t * p )
 { 
     Aig_Man_t * pNew;
     Aig_Obj_t * pObj;
@@ -303,7 +303,7 @@ Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p )
     // create internal nodes
     Aig_ManForEachObjVec( p->vNodes, p->pAig, pObj, i )
 //        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-        Aig_GlaDeriveAbs_rec( pNew, pObj );
+        Aig_Gla1DeriveAbs_rec( pNew, pObj );
     // create PO
     Saig_ManForEachPo( p->pAig, pObj, i )
         pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
@@ -332,7 +332,7 @@ Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_GlaFetchVar( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
+int Aig_Gla1FetchVar( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k )
 {
     int i, iVecId, iSatVar;
     assert( k < p->nFrames );
@@ -368,7 +368,7 @@ int Aig_GlaFetchVar( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
+int Aig_Gla1ObjAddToSolver( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k )
 {
     if ( k == p->nFrames )
     {
@@ -388,17 +388,17 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
     assert( k < p->nFrames );
     assert( Vec_IntEntry(p->vIncluded, Aig_ObjId(pObj)) );
     if ( Aig_ObjIsConst1(pObj) )
-        return Aig_GlaAddConst( p->pSat, Aig_GlaFetchVar(p, pObj, k), 0 );
+        return Aig_Gla1AddConst( p->pSat, Aig_Gla1FetchVar(p, pObj, k), 0 );
     if ( Saig_ObjIsLo(p->pAig, pObj) )
     {
         Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
         if ( k == 0 )
         {
-            Aig_GlaFetchVar( p, Aig_ObjFanin0(pObjLi), 0 );
-            return Aig_GlaAddConst( p->pSat, Aig_GlaFetchVar(p, pObj, k), 1 );
+            Aig_Gla1FetchVar( p, Aig_ObjFanin0(pObjLi), 0 );
+            return Aig_Gla1AddConst( p->pSat, Aig_Gla1FetchVar(p, pObj, k), 1 );
         }
-        return Aig_GlaAddBuffer( p->pSat, Aig_GlaFetchVar(p, pObj, k), 
-                Aig_GlaFetchVar(p, Aig_ObjFanin0(pObjLi), k-1), 
+        return Aig_Gla1AddBuffer( p->pSat, Aig_Gla1FetchVar(p, pObj, k), 
+                Aig_Gla1FetchVar(p, Aig_ObjFanin0(pObjLi), k-1), 
                 Aig_ObjFaninC0(pObjLi) );
     }
     else
@@ -407,9 +407,9 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
         int i, Entry;
         assert( Aig_ObjIsNode(pObj) );
         if ( p->vObj2Cnf == NULL )
-            return Aig_GlaAddNode( p->pSat, Aig_GlaFetchVar(p, pObj, k), 
-                        Aig_GlaFetchVar(p, Aig_ObjFanin0(pObj), k), 
-                        Aig_GlaFetchVar(p, Aig_ObjFanin1(pObj), k), 
+            return Aig_Gla1AddNode( p->pSat, Aig_Gla1FetchVar(p, pObj, k), 
+                        Aig_Gla1FetchVar(p, Aig_ObjFanin0(pObj), k), 
+                        Aig_Gla1FetchVar(p, Aig_ObjFanin1(pObj), k), 
                         Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
         // derive clauses
         assert( pObj->fMarkA );
@@ -422,7 +422,7 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
         // derive variables
         Cnf_CollectLeaves( pObj, p->vLeaves, 0 );
         Vec_PtrForEachEntry( Aig_Obj_t *, p->vLeaves, pObj, i )
-            Aig_GlaFetchVar( p, pObj, k );
+            Aig_Gla1FetchVar( p, pObj, k );
         // translate clauses
         assert( Vec_IntSize(vClauses) >= 2 );
         assert( Vec_IntEntry(vClauses, 0) == 0 );
@@ -433,7 +433,7 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
                 Vec_IntClear( p->vLits );
                 continue;
             }
-            Vec_IntPush( p->vLits, (Entry & 1) ^ (2 * Aig_GlaFetchVar(p, Aig_ManObj(p->pAig, Entry >> 1), k)) );
+            Vec_IntPush( p->vLits, (Entry & 1) ^ (2 * Aig_Gla1FetchVar(p, Aig_ManObj(p->pAig, Entry >> 1), k)) );
             if ( i == Vec_IntSize(vClauses) - 1 || Vec_IntEntry(vClauses, i+1) == 0 )
             {
                 if ( !sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits)+Vec_IntSize(p->vLits) ) )
@@ -455,12 +455,12 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig, int fNaiveCnf )
+Aig_Gla1Man_t * Aig_Gla1ManStart( Aig_Man_t * pAig, int fNaiveCnf )
 {
-    Aig_GlaMan_t * p;
+    Aig_Gla1Man_t * p;
     int i;
 
-    p = ABC_CALLOC( Aig_GlaMan_t, 1 );
+    p = ABC_CALLOC( Aig_Gla1Man_t, 1 );
     p->pAig      = pAig;
     p->vAssigned = Vec_IntAlloc( 1000 );
     p->vIncluded = Vec_IntStart( Aig_ManObjNumMax(pAig) );
@@ -511,7 +511,7 @@ Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig, int fNaiveCnf )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_GlaManStop( Aig_GlaMan_t * p )
+void Aig_Gla1ManStop( Aig_Gla1Man_t * p )
 {
     Vec_IntFreeP( &p->vAssigned );
     Vec_IntFreeP( &p->vIncluded );
@@ -551,7 +551,7 @@ void Aig_GlaManStop( Aig_GlaMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Cex_t * Aig_GlaDeriveCex( Aig_GlaMan_t * p, int iFrame )
+Abc_Cex_t * Aig_Gla1DeriveCex( Aig_Gla1Man_t * p, int iFrame )
 {
     Abc_Cex_t * pCex;
     Aig_Obj_t * pObj;
@@ -600,7 +600,7 @@ Abc_Cex_t * Aig_GlaDeriveCex( Aig_GlaMan_t * p, int iFrame )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_GlaPrintAbstr( Aig_GlaMan_t * p, int f, int r, int v, int c )
+void Aig_Gla1PrintAbstr( Aig_Gla1Man_t * p, int f, int r, int v, int c )
 {
     if ( r == 0 )
         printf( "== %3d ==", f );
@@ -621,7 +621,7 @@ void Aig_GlaPrintAbstr( Aig_GlaMan_t * p, int f, int r, int v, int c )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_GlaExtendIncluded( Aig_GlaMan_t * p )
+void Aig_Gla1ExtendIncluded( Aig_Gla1Man_t * p )
 {
     Aig_Obj_t * pObj;
     int i, k;
@@ -651,11 +651,11 @@ void Aig_GlaExtendIncluded( Aig_GlaMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose )
+Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose )
 {
     int nStart = 0;
     Vec_Int_t * vResult = NULL;
-    Aig_GlaMan_t * p;
+    Aig_Gla1Man_t * p;
     Aig_Man_t * pAbs;
     Aig_Obj_t * pObj;
     Abc_Cex_t * pCex;
@@ -673,14 +673,14 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in
     }
 
     // start the solver
-    p = Aig_GlaManStart( pAig, fNaiveCnf );
+    p = Aig_Gla1ManStart( pAig, fNaiveCnf );
     p->nFramesMax = nFramesMax;
     p->nConfLimit = nConfLimit;
     p->fVerbose   = fVerbose;
 
     // include constant node
     Vec_IntWriteEntry( p->vIncluded, 0, 1 );
-    Aig_GlaFetchVar( p, Aig_ManConst1(pAig), 0 );
+    Aig_Gla1FetchVar( p, Aig_ManConst1(pAig), 0 );
 
     // set runtime limit
     if ( TimeLimit )
@@ -692,16 +692,16 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in
         // initialize abstraction in this timeframe
         Aig_ManForEachObjVec( p->vAssigned, pAig, pObj, i )
             if ( Vec_IntEntry(p->vIncluded, Aig_ObjId(pObj)) )
-                if ( !Aig_GlaObjAddToSolver( p, pObj, f ) )
+                if ( !Aig_Gla1ObjAddToSolver( p, pObj, f ) )
                     printf( "Error!  SAT solver became UNSAT.\n" );
 
         // create output literal to represent property failure
         pObj    = Aig_ManPo( pAig, 0 );
-        iSatVar = Aig_GlaFetchVar( p, Aig_ObjFanin0(pObj), f );
+        iSatVar = Aig_Gla1FetchVar( p, Aig_ObjFanin0(pObj), f );
         Lit     = toLitCond( iSatVar, Aig_ObjFaninC0(pObj) );
 
         // try solving the abstraction
-        Aig_GlaCollectAbstr( p );
+        Aig_Gla1CollectAbstr( p );
         for ( r = 0; r < 1000000; r++ )
         {
             // try to find a counter-example
@@ -730,9 +730,9 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in
             }
             clk = clock();
             // derive abstraction
-            pAbs = Aig_GlaDeriveAbs( p );
+            pAbs = Aig_Gla1DeriveAbs( p );
             // derive counter-example
-            pCex = Aig_GlaDeriveCex( p, f );
+            pCex = Aig_Gla1DeriveCex( p, f );
             // verify the counter-example
             RetValue = Saig_ManVerifyCex( pAbs, pCex );
             if ( RetValue == 0 )
@@ -746,7 +746,7 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in
                 assert( Vec_IntEntry( p->vIncluded, Aig_ObjId(pObj) ) == 0 );
                 Vec_IntWriteEntry( p->vIncluded, Aig_ObjId(pObj), 1 );
                 for ( g = 0; g <= f; g++ )
-                    if ( !Aig_GlaObjAddToSolver( p, pObj, g ) )
+                    if ( !Aig_Gla1ObjAddToSolver( p, pObj, g ) )
                         printf( "Error!  SAT solver became UNSAT.\n" );
             }
             if ( Vec_IntSize(vPPiRefine) == 0 )
@@ -763,9 +763,9 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in
             p->timeRef += clock() - clk;
 
             // prepare abstraction
-            Aig_GlaCollectAbstr( p );
+            Aig_Gla1CollectAbstr( p );
             if ( fVerbose )
-                Aig_GlaPrintAbstr( p, f, r, p->pSat->size, nConfAft - nConfBef );
+                Aig_Gla1PrintAbstr( p, f, r, p->pSat->size, nConfAft - nConfBef );
         }
         if ( RetValue != l_False )
             break;
@@ -786,9 +786,9 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in
     }
     // prepare return value
     if ( !fNaiveCnf && p->vIncluded )
-        Aig_GlaExtendIncluded( p );
+        Aig_Gla1ExtendIncluded( p );
     vResult = p->vIncluded;  p->vIncluded = NULL;
-    Aig_GlaManStop( p );
+    Aig_Gla1ManStop( p );
     return vResult;
 }
 
diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c
new file mode 100644
index 00000000..e18b6830
--- /dev/null
+++ b/src/aig/saig/saigGlaPba.c
@@ -0,0 +1,518 @@
+/**CFile****************************************************************
+
+  FileName    [saigGlaPba.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Gate level abstraction.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigGlaPba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+#include "satSolver.h"
+#include "satStore.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Aig_Gla2Man_t_ Aig_Gla2Man_t;
+struct Aig_Gla2Man_t_
+{
+    // user data
+    Aig_Man_t *    pAig;
+    int            nConfMax;
+    int            nFramesMax;
+    int            fVerbose;
+    // unrolling
+    Vec_Int_t *    vObj2Vec;   // maps obj ID into its vec ID
+    Vec_Int_t *    vVec2Var;   // maps vec ID into its sat Var (nFrames per vec ID)
+    Vec_Int_t *    vVar2Inf;   // maps sat Var into its frame and obj ID
+    Vec_Int_t *    vCla2Obj;   // maps sat Var into its first clause
+    // SAT solver
+    sat_solver *   pSat;
+    // statistics
+    int            timePre;
+    int            timeSat;
+    int            timeTotal;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Adds constant to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Aig_Gla2AddConst( sat_solver * pSat, int iVar, int fCompl )
+{
+    lit Lit = toLitCond( iVar, fCompl );
+    if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) )
+        return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds buffer to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Aig_Gla2AddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl )
+{
+    lit Lits[2];
+
+    Lits[0] = toLitCond( iVar0, 0 );
+    Lits[1] = toLitCond( iVar1, !fCompl );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+        return 0;
+
+    Lits[0] = toLitCond( iVar0, 1 );
+    Lits[1] = toLitCond( iVar1, fCompl );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+        return 0;
+
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds buffer to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Aig_Gla2AddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 )
+{
+    lit Lits[3];
+
+    Lits[0] = toLitCond( iVar, 1 );
+    Lits[1] = toLitCond( iVar0, fCompl0 );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+        return 0;
+
+    Lits[0] = toLitCond( iVar, 1 );
+    Lits[1] = toLitCond( iVar1, fCompl1 );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+        return 0;
+
+    Lits[0] = toLitCond( iVar, 0 );
+    Lits[1] = toLitCond( iVar0, !fCompl0 );
+    Lits[2] = toLitCond( iVar1, !fCompl1 );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
+        return 0;
+
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Finds existing SAT variable or creates a new one.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_Gla2FetchVar( Aig_Gla2Man_t * p, Aig_Obj_t * pObj, int k )
+{
+    int i, iVecId, iSatVar;
+    assert( k < p->nFramesMax );
+    iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
+    if ( iVecId == 0 )
+    {
+        iVecId = Vec_IntSize( p->vVec2Var ) / p->nFramesMax;
+        for ( i = 0; i < p->nFramesMax; i++ )
+            Vec_IntPush( p->vVec2Var, 0 );
+        Vec_IntWriteEntry( p->vObj2Vec, Aig_ObjId(pObj), iVecId );
+    }
+    iSatVar = Vec_IntEntry( p->vVec2Var, iVecId * p->nFramesMax + k );
+    if ( iSatVar == 0 )
+    {
+        iSatVar = Vec_IntSize( p->vVar2Inf ) / 2;
+        Vec_IntPush( p->vVar2Inf, Aig_ObjId(pObj) );
+        Vec_IntPush( p->vVar2Inf, k );
+        Vec_IntWriteEntry( p->vVec2Var, iVecId * p->nFramesMax + k, iSatVar );
+    }
+    return iSatVar;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Assigns variables to the AIG nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_Gla2AssignVars_rec( Aig_Gla2Man_t * p, Aig_Obj_t * pObj, int f )
+{
+    int nVars = Vec_IntSize(p->vVar2Inf);
+    Aig_Gla2FetchVar( p, pObj, f );
+    if ( nVars == Vec_IntSize(p->vVar2Inf) )
+        return;
+    if ( Aig_ObjIsConst1(pObj) )
+        return;
+    if ( Saig_ObjIsPo( p->pAig, pObj ) )
+    {
+        Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0(pObj), f );
+        return;
+    }
+    if ( Aig_ObjIsPi( pObj ) )
+    {
+        if ( Saig_ObjIsLo(p->pAig, pObj) && f > 0 )
+            Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0( Saig_ObjLoToLi(p->pAig, pObj) ), f-1 );
+        return;
+    }
+    assert( Aig_ObjIsNode(pObj) );
+    Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0(pObj), f );
+    Aig_Gla2AssignVars_rec( p, Aig_ObjFanin1(pObj), f );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_Gla2CreateSatSolver( Aig_Gla2Man_t * p )
+{
+    Vec_Int_t * vPoLits;
+    Aig_Obj_t * pObj;
+    int i, f, ObjId, nVars, RetValue = 1;
+
+    // assign variables
+//    for ( f = p->nFramesMax - 1; f >= 0; f-- )
+    for ( f = 0; f < p->nFramesMax; f++ )
+        Aig_Gla2AssignVars_rec( p, Aig_ManPo(p->pAig, 0), f );
+
+    // create SAT solver
+    p->pSat = sat_solver_new();
+    sat_solver_store_alloc( p->pSat ); 
+    sat_solver_setnvars( p->pSat, Vec_IntSize(p->vVar2Inf)/2 );
+
+    // add clauses
+    nVars = Vec_IntSize( p->vVar2Inf );
+    Vec_IntForEachEntryDouble( p->vVar2Inf, ObjId, f, i )
+    {
+        if ( ObjId == -1 )
+            continue;
+        pObj = Aig_ManObj( p->pAig, ObjId );
+        if ( Aig_ObjIsNode(pObj) )
+        {
+            RetValue &= Aig_Gla2AddNode( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 
+                                                  Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObj), f), 
+                                                  Aig_Gla2FetchVar(p, Aig_ObjFanin1(pObj), f), 
+                                                  Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
+            Vec_IntPush( p->vCla2Obj, ObjId );
+            Vec_IntPush( p->vCla2Obj, ObjId );
+            Vec_IntPush( p->vCla2Obj, ObjId );
+        }
+        else if ( Saig_ObjIsLo(p->pAig, pObj) )
+        {
+            if ( f == 0 )
+            {
+                RetValue &= Aig_Gla2AddConst( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 1 );
+                Vec_IntPush( p->vCla2Obj, ObjId );
+            }
+            else
+            {
+                Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
+                RetValue &= Aig_Gla2AddBuffer( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 
+                                                        Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObjLi), f-1), 
+                                                        Aig_ObjFaninC0(pObjLi) );
+                Vec_IntPush( p->vCla2Obj, ObjId );
+                Vec_IntPush( p->vCla2Obj, ObjId );
+            }
+        }
+        else if ( Saig_ObjIsPo(p->pAig, pObj) )
+        {
+            RetValue &= Aig_Gla2AddBuffer( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 
+                                                    Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObj), f), 
+                                                    Aig_ObjFaninC0(pObj) );
+            Vec_IntPush( p->vCla2Obj, ObjId );
+            Vec_IntPush( p->vCla2Obj, ObjId );
+        }
+        else if ( Aig_ObjIsConst1(pObj) )
+        {
+            RetValue &= Aig_Gla2AddConst( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 0 );
+            Vec_IntPush( p->vCla2Obj, ObjId );
+        }
+        else assert( Saig_ObjIsPi(p->pAig, pObj) );
+    }
+
+    // add output clause
+    vPoLits = Vec_IntAlloc( p->nFramesMax );
+    for ( f = 0; f < p->nFramesMax; f++ )
+        Vec_IntPush( vPoLits, 2 * Aig_Gla2FetchVar(p, Aig_ManPo(p->pAig, 0), f) );
+    RetValue &= sat_solver_addclause( p->pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) );
+    Vec_IntFree( vPoLits );
+    Vec_IntPush( p->vCla2Obj, 0 );
+
+    assert( nVars == Vec_IntSize(p->vVar2Inf) );
+    assert( ((Sto_Man_t *)p->pSat->pStore)->nClauses == Vec_IntSize(p->vCla2Obj) );
+
+    sat_solver_store_mark_roots( p->pSat ); 
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Gla2Man_t * Aig_Gla2ManStart( Aig_Man_t * pAig, int nFramesMax )
+{
+    Aig_Gla2Man_t * p;
+    int i;
+
+    p = ABC_CALLOC( Aig_Gla2Man_t, 1 );
+    p->pAig       = pAig;
+
+    p->vObj2Vec   = Vec_IntStart( Aig_ManObjNumMax(pAig) );
+    p->vVec2Var   = Vec_IntAlloc( 1 << 20 );
+    p->vVar2Inf   = Vec_IntAlloc( 1 << 20 );
+    p->vCla2Obj   = Vec_IntAlloc( 1 << 20 );
+
+    // skip first vector ID
+    p->nFramesMax = nFramesMax;
+    for ( i = 0; i < p->nFramesMax; i++ )
+        Vec_IntPush( p->vVec2Var, -1 );
+
+    // skip  first SAT variable
+    Vec_IntPush( p->vVar2Inf, -1 );
+    Vec_IntPush( p->vVar2Inf, -1 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_Gla2ManStop( Aig_Gla2Man_t * p )
+{
+    Vec_IntFreeP( &p->vObj2Vec );
+    Vec_IntFreeP( &p->vVec2Var );
+    Vec_IntFreeP( &p->vVar2Inf );
+    Vec_IntFreeP( &p->vCla2Obj );
+
+    if ( p->pSat )
+        sat_solver_delete( p->pSat );
+    ABC_FREE( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Finds the set of clauses involved in the UNSAT core.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbose, int * piRetValue )
+{
+    Vec_Int_t * vCore;
+    void * pSatCnf; 
+    Intp_Man_t * pManProof;
+    int RetValue, clk = clock();
+    if ( piRetValue )
+        *piRetValue = -1;
+    // solve the problem
+    RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+    if ( RetValue == l_Undef )
+    {
+        printf( "Conflict limit is reached.\n" );
+        return NULL;
+    }
+    if ( RetValue == l_True )
+    {
+        printf( "The BMC problem is SAT.\n" );
+        if ( piRetValue )
+            *piRetValue = 0;
+        return NULL;
+    }
+    if ( fVerbose )
+    {
+        printf( "SAT solver returned UNSAT after %d conflicts.  ", pSat->stats.conflicts );
+        ABC_PRT( "Time", clock() - clk );
+    }
+    assert( RetValue == l_False );
+    pSatCnf = sat_solver_store_release( pSat ); 
+    // derive the UNSAT core
+    clk = clock();
+    pManProof = Intp_ManAlloc();
+    vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0 );
+    Intp_ManFree( pManProof );
+    Sto_ManFree( (Sto_Man_t *)pSatCnf );
+    if ( fVerbose )
+    {
+        printf( "SAT core contains %d clauses (out of %d).  ", Vec_IntSize(vCore), pSat->stats.clauses );
+        ABC_PRT( "Time", clock() - clk );
+    }
+    return vCore;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects abstracted objects.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Aig_Gla2ManCollect( Aig_Gla2Man_t * p, Vec_Int_t * vCore )
+{
+    Vec_Int_t * vResult;
+    Aig_Obj_t * pObj;
+    int i, ClaId;
+    vResult = Vec_IntStart( Aig_ManObjNumMax(p->pAig) );
+    Vec_IntWriteEntry( vResult, 0, 1 ); // add const1
+    Vec_IntForEachEntry( vCore, ClaId, i )
+    {
+        pObj = Aig_ManObj( p->pAig, Vec_IntEntry(p->vCla2Obj, ClaId) );
+        if ( Saig_ObjIsPi(p->pAig, pObj) || Saig_ObjIsPo(p->pAig, pObj) )
+            continue;
+        assert( Saig_ObjIsLo(p->pAig, pObj) || Aig_ObjIsNode(pObj) );
+        Vec_IntWriteEntry( vResult, Aig_ObjId(pObj), 1 );
+    }
+    return vResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs gate-level localization abstraction.]
+
+  Description [Returns array of objects included in the abstraction. This array
+  may contain only const1, flop outputs, and internal nodes, that is, objects
+  that should have clauses added to the SAT solver.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose )
+{
+    int nStart = 0;
+    Aig_Gla2Man_t * p;
+    Vec_Int_t * vCore, * vResult;
+    int clk, clkTotal = clock();
+    assert( Saig_ManPoNum(pAig) == 1 );
+
+    if ( fVerbose )
+    {
+        if ( TimeLimit )
+            printf( "Abstracting from frame %d to frame %d with timeout %d sec.\n", nStart, nFramesMax, TimeLimit );
+        else
+            printf( "Abstracting from frame %d to frame %d with no timeout.\n", nStart, nFramesMax );
+    }
+
+    // start the solver
+    clk = clock();
+    p = Aig_Gla2ManStart( pAig, nFramesMax );
+    if ( !Aig_Gla2CreateSatSolver( p ) )
+    {
+        printf( "Error!  SAT solver became UNSAT.\n" );
+        Aig_Gla2ManStop( p );
+        return NULL;
+    }
+    p->timePre += clock() - clk;
+
+    // set runtime limit
+    if ( TimeLimit )
+        sat_solver_set_runtime_limit( p->pSat, clock() + TimeLimit * CLOCKS_PER_SEC );
+
+    // compute UNSAT core
+    clk = clock();
+    vCore = Saig_AbsSolverUnsatCore( p->pSat, nConfLimit, fVerbose, NULL );
+    if ( vCore == NULL )
+    {
+        Aig_Gla2ManStop( p );
+        return NULL;
+    }
+    p->timeSat += clock() - clk;
+    p->timeTotal = clock() - clkTotal;
+
+    // print stats
+    if ( fVerbose )
+    {
+        ABC_PRTP( "Pre   ", p->timePre,   p->timeTotal );
+        ABC_PRTP( "Sat   ", p->timeSat,   p->timeTotal );
+        ABC_PRTP( "Total ", p->timeTotal, p->timeTotal );
+    }
+
+    // prepare return value
+    vResult = Aig_Gla2ManCollect( p, vCore );
+    Vec_IntFree( vCore );
+    Aig_Gla2ManStop( p );
+    return vResult;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index fec9d78b..06da9698 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -379,6 +379,7 @@ static int Abc_CommandAbc9AbsCba             ( 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_CommandAbc9GlaCba             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9GlaPba             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Reparam            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Posplit            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9ReachM             ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -832,6 +833,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_cba",      Abc_CommandAbc9GlaCba,       0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&gla_pba",      Abc_CommandAbc9GlaPba,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&reparam",      Abc_CommandAbc9Reparam,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&posplit",      Abc_CommandAbc9Posplit,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&reachm",       Abc_CommandAbc9ReachM,       0 );
@@ -28714,12 +28716,12 @@ int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &abs_cba [-SFCMT num] [-vh]\n" );
+    Abc_Print( -2, "usage: &abs_cba [-SFCT num] [-vh]\n" );
     Abc_Print( -2, "\t         refines abstracted flop map with CEX-based abstraction\n" );
     Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
     Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
     Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", pPars->nConfLimit );
-    Abc_Print( -2, "\t-M num : the max number of flops to add (0 = not used) [default = %d]\n", pPars->nFfToAddMax );
+//    Abc_Print( -2, "\t-M num : the max number of flops to add (0 = not used) [default = %d]\n", pPars->nFfToAddMax );
     Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
     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");
@@ -29020,6 +29022,11 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" );
         return 0;
     }
+    if ( pPars->nFramesMax < 1 )
+    {
+        Abc_Print( 1, "The number of frames should be a positive integer.\n" );
+        return 0;
+    }
     pAbc->Status = Gia_ManGlaCbaPerform( pAbc->pGia, pPars, fNaiveCnf );
     if ( pPars->nStart == 0 )
        pAbc->nFrames = pPars->iFrame;
@@ -29028,12 +29035,12 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &gla_cba [-SFCMT num] [-cvh]\n" );
+    Abc_Print( -2, "usage: &gla_cba [-FCT num] [-cvh]\n" );
     Abc_Print( -2, "\t         refines abstracted object map with CEX-based abstraction\n" );
-    Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
+//    Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
     Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
     Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", pPars->nConfLimit );
-    Abc_Print( -2, "\t-M num : the max number of flops to add (0 = not used) [default = %d]\n", pPars->nFfToAddMax );
+//    Abc_Print( -2, "\t-M num : the max number of flops to add (0 = not used) [default = %d]\n", pPars->nFfToAddMax );
     Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
     Abc_Print( -2, "\t-c     : toggle using naive CNF computation [default = %s]\n", fNaiveCnf? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
@@ -29052,6 +29059,122 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Saig_ParBmc_t Pars, * pPars = &Pars;
+    int c;
+    Saig_ParBmcSetDefaultParams( pPars );
+    pPars->nStart     = 0;  //(pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
+    pPars->nFramesMax = 10; //pPars->nStart + 10;
+    pPars->nConfLimit = 1000000;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTcvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nStart = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nStart < 0 ) 
+                goto usage;
+            break;
+        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 '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 '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 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9AbsCba(): There is no AIG.\n" );
+        return 1;
+    } 
+    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 < 1 )
+    {
+        Abc_Print( 1, "The number of frames should be a positive integer.\n" );
+        return 0;
+    }
+    pAbc->Status = Gia_ManGlaPbaPerform( pAbc->pGia, pPars );
+    if ( pPars->nStart == 0 )
+       pAbc->nFrames = pPars->iFrame;
+    Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
+//    printf( "This command is currently not enabled.\n" );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &gla_pba [-FCT num] [-vh]\n" );
+    Abc_Print( -2, "\t         refines abstracted object map with proof-based abstraction\n" );
+//    Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
+    Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
+    Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", pPars->nConfLimit );
+    Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
+    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_CommandAbc9Reparam( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp = NULL;