Created new abstraction package from the code that was all over the place.

1 files changed, 1899 insertions, 0 deletions

diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c
new file mode 100644
index 00000000..b026c6e3
--- /dev/null
+++ b/src/proof/abs/absGla.c
@@ -0,0 +1,1899 @@
+/**CFile****************************************************************
+
+  FileName    [absGla2.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Abstraction package.]
+
+  Synopsis    [Scalable gate-level abstraction.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: absGla2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sat/cnf/cnf.h"
+#include "sat/bsat/satSolver2.h"
+#include "base/main/main.h"
+#include "abs.h"
+#include "absRef.h"
+//#include "absRef2.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define GA2_BIG_NUM 0x3FFFFFF0
+
+typedef struct Ga2_Man_t_ Ga2_Man_t; // manager
+struct Ga2_Man_t_
+{
+    // user data
+    Gia_Man_t *    pGia;         // working AIG manager
+    Abs_Par_t *    pPars;        // parameters
+    // markings 
+    Vec_Ptr_t *    vCnfs;        // for each object: CNF0, CNF1
+    // abstraction
+    Vec_Int_t *    vIds;         // abstraction ID for each GIA object
+    Vec_Int_t *    vProofIds;    // mapping of GIA objects into their proof IDs
+    Vec_Int_t *    vAbs;         // array of abstracted objects
+    Vec_Int_t *    vValues;      // array of objects with abstraction ID assigned
+    int            nProofIds;    // the counter of proof IDs
+    int            LimAbs;       // limit value for starting abstraction objects
+    int            LimPpi;       // limit value for starting PPI objects
+    int            nMarked;      // total number of marked nodes and flops
+    // refinement
+    Rnm_Man_t *    pRnm;         // refinement manager
+//    Rf2_Man_t *    pRf2;         // refinement manager
+    // SAT solver and variables
+    Vec_Ptr_t *    vId2Lit;      // mapping, for each timeframe, of object ID into SAT literal
+    sat_solver2 *  pSat;         // incremental SAT solver
+    int            nSatVars;     // the number of SAT variables
+    int            nCexes;       // the number of counter-examples
+    int            nObjAdded;    // objs added during refinement
+    // hash table
+    int *          pTable;
+    int            nTable;
+    int            nHashHit;
+    int            nHashMiss;
+    int            nHashOver;
+    // temporaries
+    Vec_Int_t *    vLits;
+    Vec_Int_t *    vIsopMem;
+    char * pSopSizes, ** pSops;  // CNF representation
+    // statistics  
+    clock_t        timeStart;
+    clock_t        timeInit;
+    clock_t        timeSat;
+    clock_t        timeUnsat;
+    clock_t        timeCex;
+    clock_t        timeOther;
+};
+
+static inline int         Ga2_ObjOffset( Gia_Man_t * p, Gia_Obj_t * pObj )       { return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj));                                                    }
+static inline int         Ga2_ObjLeaveNum( Gia_Man_t * p, Gia_Obj_t * pObj )     { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj));                                                }
+static inline int *       Ga2_ObjLeavePtr( Gia_Man_t * p, Gia_Obj_t * pObj )     { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1);                                           }
+static inline unsigned    Ga2_ObjTruth( Gia_Man_t * p, Gia_Obj_t * pObj )        { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1);       }
+static inline int         Ga2_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj )       { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2);       }
+static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj )       { static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v;  }
+
+static inline int         Ga2_ObjId( Ga2_Man_t * p, Gia_Obj_t * pObj )           { return Vec_IntEntry(p->vIds, Gia_ObjId(p->pGia, pObj));                                                  }
+static inline void        Ga2_ObjSetId( Ga2_Man_t * p, Gia_Obj_t * pObj, int i ) { Vec_IntWriteEntry(p->vIds, Gia_ObjId(p->pGia, pObj), i);                                                 }
+
+static inline Vec_Int_t * Ga2_ObjCnf0( Ga2_Man_t * p, Gia_Obj_t * pObj )         { assert(Ga2_ObjId(p,pObj) >= 0); return Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj)   );                  }
+static inline Vec_Int_t * Ga2_ObjCnf1( Ga2_Man_t * p, Gia_Obj_t * pObj )         { assert(Ga2_ObjId(p,pObj) >= 0); return Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj)+1 );                  }
+
+static inline int         Ga2_ObjIsAbs0( Ga2_Man_t * p, Gia_Obj_t * pObj )       { assert(Ga2_ObjId(p,pObj) >= 0); return Ga2_ObjId(p,pObj) >= 0         && Ga2_ObjId(p,pObj) < p->LimAbs;  }
+static inline int         Ga2_ObjIsLeaf0( Ga2_Man_t * p, Gia_Obj_t * pObj )      { assert(Ga2_ObjId(p,pObj) >= 0); return Ga2_ObjId(p,pObj) >= p->LimAbs && Ga2_ObjId(p,pObj) < p->LimPpi;  }
+static inline int         Ga2_ObjIsAbs( Ga2_Man_t * p, Gia_Obj_t * pObj )        { return Ga2_ObjId(p,pObj) >= 0 &&  Ga2_ObjCnf0(p,pObj);                                                   }
+static inline int         Ga2_ObjIsLeaf( Ga2_Man_t * p, Gia_Obj_t * pObj )       { return Ga2_ObjId(p,pObj) >= 0 && !Ga2_ObjCnf0(p,pObj);                                                   }
+
+static inline Vec_Int_t * Ga2_MapFrameMap( Ga2_Man_t * p, int f )                { return (Vec_Int_t *)Vec_PtrEntry( p->vId2Lit, f );                                                       }
+
+// returns literal of this object, or -1 if SAT variable of the object is not assigned
+static inline int Ga2_ObjFindLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )  
+{ 
+//    int Id = Ga2_ObjId(p,pObj);
+    assert( Ga2_ObjId(p,pObj) >= 0 && Ga2_ObjId(p,pObj) < Vec_IntSize(p->vValues) );
+    return Vec_IntEntry( Ga2_MapFrameMap(p, f), Ga2_ObjId(p,pObj) );
+}
+// inserts literal of this object
+static inline void Ga2_ObjAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f, int Lit )  
+{ 
+//    assert( Lit > 1 );
+    assert( Ga2_ObjFindLit(p, pObj, f) == -1 );
+    Vec_IntSetEntry( Ga2_MapFrameMap(p, f), Ga2_ObjId(p,pObj), Lit );
+}
+// returns or inserts-and-returns literal of this object
+static inline int Ga2_ObjFindOrAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )  
+{ 
+    int Lit = Ga2_ObjFindLit( p, pObj, f );
+    if ( Lit == -1 )
+    {
+        Lit = toLitCond( p->nSatVars++, 0 );
+        Ga2_ObjAddLit( p, pObj, f, Lit );
+    }
+//    assert( Lit > 1 );
+    return Lit;
+}
+
+
+// calling pthreads
+extern void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose );
+extern void Gia_Ga2ProveCancel( int fVerbose );
+extern int  Gia_Ga2ProveCheck( int fVerbose );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes truth table for the marked node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Ga2_ObjComputeTruth_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fFirst )
+{
+    unsigned Val0, Val1;
+    if ( pObj->fPhase && !fFirst )
+        return pObj->Value;
+    assert( Gia_ObjIsAnd(pObj) );
+    Val0 = Ga2_ObjComputeTruth_rec( p, Gia_ObjFanin0(pObj), 0 );
+    Val1 = Ga2_ObjComputeTruth_rec( p, Gia_ObjFanin1(pObj), 0 );
+    return (Gia_ObjFaninC0(pObj) ? ~Val0 : Val0) & (Gia_ObjFaninC1(pObj) ? ~Val1 : Val1);
+}
+unsigned Ga2_ManComputeTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves )
+{
+    static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+    Gia_Obj_t * pObj;
+    unsigned Res;
+    int i;
+    Gia_ManForEachObjVec( vLeaves, p, pObj, i )
+        pObj->Value = uTruth5[i];
+    Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 );
+    Gia_ManForEachObjVec( vLeaves, p, pObj, i )
+        pObj->Value = 0;
+    return Res;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns AIG marked for CNF generation.]
+
+  Description [The marking satisfies the following requirements:
+  Each marked node has the number of marked fanins no more than N.]
+               
+  SideEffects [Uses pObj->fPhase to store the markings.]
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ga2_ManBreakTree_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fFirst, int N )
+{   // breaks a tree rooted at the node into N-feasible subtrees
+    int Val0, Val1;
+    if ( pObj->fPhase && !fFirst )
+        return 1;
+    Val0 = Ga2_ManBreakTree_rec( p, Gia_ObjFanin0(pObj), 0, N );
+    Val1 = Ga2_ManBreakTree_rec( p, Gia_ObjFanin1(pObj), 0, N );
+    if ( Val0 + Val1 < N )
+        return Val0 + Val1;
+    if ( Val0 + Val1 == N )
+    {
+        pObj->fPhase = 1;
+        return 1;
+    }
+    assert( Val0 + Val1 > N );
+    assert( Val0 < N && Val1 < N );
+    if ( Val0 >= Val1 )
+    {
+        Gia_ObjFanin0(pObj)->fPhase = 1;
+        Val0 = 1;
+    }
+    else 
+    {
+        Gia_ObjFanin1(pObj)->fPhase = 1;
+        Val1 = 1;
+    }
+    if ( Val0 + Val1 < N )
+        return Val0 + Val1;
+    if ( Val0 + Val1 == N )
+    {
+        pObj->fPhase = 1;
+        return 1;
+    }
+    assert( 0 );
+    return -1;
+}
+int Ga2_ManCheckNodesAnd( Gia_Man_t * p, Vec_Int_t * vNodes )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManForEachObjVec( vNodes, p, pObj, i )
+        if ( (!Gia_ObjFanin0(pObj)->fPhase && Gia_ObjFaninC0(pObj)) || 
+             (!Gia_ObjFanin1(pObj)->fPhase && Gia_ObjFaninC1(pObj)) )
+            return 0;
+    return 1;
+}
+void Ga2_ManCollectNodes_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes, int fFirst )
+{
+    if ( pObj->fPhase && !fFirst )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Ga2_ManCollectNodes_rec( p, Gia_ObjFanin0(pObj), vNodes, 0 );
+    Ga2_ManCollectNodes_rec( p, Gia_ObjFanin1(pObj), vNodes, 0 );
+    Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
+
+}
+void Ga2_ManCollectLeaves_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLeaves, int fFirst )
+{
+    if ( pObj->fPhase && !fFirst )
+    {
+        Vec_IntPushUnique( vLeaves, Gia_ObjId(p, pObj) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Ga2_ManCollectLeaves_rec( p, Gia_ObjFanin0(pObj), vLeaves, 0 );
+    Ga2_ManCollectLeaves_rec( p, Gia_ObjFanin1(pObj), vLeaves, 0 );
+}
+int Ga2_ManMarkup( Gia_Man_t * p, int N, int fSimple )
+{
+    static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+//    clock_t clk = clock();
+    Vec_Int_t * vLeaves;
+    Gia_Obj_t * pObj;
+    int i, k, Leaf, CountMarks;
+
+    vLeaves = Vec_IntAlloc( 100 );
+
+    if ( fSimple )
+    {
+        Gia_ManForEachObj( p, pObj, i )
+            pObj->fPhase = !Gia_ObjIsCo(pObj);
+    }
+    else
+    {
+        // label nodes with multiple fanouts and inputs MUXes
+        Gia_ManForEachObj( p, pObj, i )
+        {
+            pObj->Value = 0;
+            if ( !Gia_ObjIsAnd(pObj) )
+                continue;
+            Gia_ObjFanin0(pObj)->Value++;
+            Gia_ObjFanin1(pObj)->Value++;
+            if ( !Gia_ObjIsMuxType(pObj) )
+                continue;
+            Gia_ObjFanin0(Gia_ObjFanin0(pObj))->Value++;
+            Gia_ObjFanin1(Gia_ObjFanin0(pObj))->Value++;
+            Gia_ObjFanin0(Gia_ObjFanin1(pObj))->Value++;
+            Gia_ObjFanin1(Gia_ObjFanin1(pObj))->Value++;
+        }
+        Gia_ManForEachObj( p, pObj, i )
+        {
+            pObj->fPhase = 0;
+            if ( Gia_ObjIsAnd(pObj) )
+                pObj->fPhase = (pObj->Value > 1);
+            else if ( Gia_ObjIsCo(pObj) )
+                Gia_ObjFanin0(pObj)->fPhase = 1;
+            else 
+                pObj->fPhase = 1;
+        } 
+        // add marks when needed
+        Gia_ManForEachAnd( p, pObj, i )
+        {
+            if ( !pObj->fPhase )
+                continue;
+            Vec_IntClear( vLeaves );
+            Ga2_ManCollectLeaves_rec( p, pObj, vLeaves, 1 );
+            if ( Vec_IntSize(vLeaves) > N )
+                Ga2_ManBreakTree_rec( p, pObj, 1, N );
+        }
+    }
+
+    // verify that the tree is split correctly
+    Vec_IntFreeP( &p->vMapping );
+    p->vMapping = Vec_IntStart( Gia_ManObjNum(p) );
+    Gia_ManForEachRo( p, pObj, i )
+    {
+        Gia_Obj_t * pObjRi = Gia_ObjRoToRi(p, pObj);
+        assert( pObj->fPhase );
+        assert( Gia_ObjFanin0(pObjRi)->fPhase );
+        // create map
+        Vec_IntWriteEntry( p->vMapping, Gia_ObjId(p, pObj), Vec_IntSize(p->vMapping) );
+        Vec_IntPush( p->vMapping, 1 );
+        Vec_IntPush( p->vMapping, Gia_ObjFaninId0p(p, pObjRi) );
+        Vec_IntPush( p->vMapping, Gia_ObjFaninC0(pObjRi) ? 0x55555555 : 0xAAAAAAAA );
+        Vec_IntPush( p->vMapping, -1 );  // placeholder for ref counter
+    }
+    CountMarks = Gia_ManRegNum(p);
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( !pObj->fPhase )
+            continue;
+        Vec_IntClear( vLeaves );
+        Ga2_ManCollectLeaves_rec( p, pObj, vLeaves, 1 );
+        assert( Vec_IntSize(vLeaves) <= N );
+        // create map
+        Vec_IntWriteEntry( p->vMapping, i, Vec_IntSize(p->vMapping) );
+        Vec_IntPush( p->vMapping, Vec_IntSize(vLeaves) );
+        Vec_IntForEachEntry( vLeaves, Leaf, k )
+        {            
+            Vec_IntPush( p->vMapping, Leaf );
+            Gia_ManObj(p, Leaf)->Value = uTruth5[k];
+            assert( Gia_ManObj(p, Leaf)->fPhase );
+        }
+        Vec_IntPush( p->vMapping,  (int)Ga2_ObjComputeTruth_rec( p, pObj, 1 ) );
+        Vec_IntPush( p->vMapping, -1 );  // placeholder for ref counter
+        CountMarks++;
+    }
+//    Abc_PrintTime( 1, "Time", clock() - clk );
+    Vec_IntFree( vLeaves );
+    Gia_ManCleanValue( p );
+    return CountMarks;
+}
+void Ga2_ManComputeTest( Gia_Man_t * p )
+{
+    clock_t clk;
+//    unsigned uTruth;
+    Gia_Obj_t * pObj;
+    int i, Counter = 0;
+    clk = clock();
+    Ga2_ManMarkup( p, 5, 0 );
+    Abc_PrintTime( 1, "Time", clock() - clk );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( !pObj->fPhase )
+            continue;
+//        uTruth = Ga2_ObjTruth( p, pObj );
+//        printf( "%6d : ", Counter );
+//        Kit_DsdPrintFromTruth( &uTruth, Ga2_ObjLeaveNum(p, pObj) ); 
+//        printf( "\n" );
+        Counter++;
+    }
+    Abc_Print( 1, "Marked AND nodes = %6d.  ", Counter );
+    Abc_PrintTime( 1, "Time", clock() - clk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Abs_Par_t * pPars )
+{
+    Ga2_Man_t * p;
+    p = ABC_CALLOC( Ga2_Man_t, 1 );
+    p->timeStart = clock();
+    // user data
+    p->pGia      = pGia;
+    p->pPars     = pPars;
+    // markings 
+    p->nMarked   = Ga2_ManMarkup( pGia, 5, pPars->fUseSimple );
+    p->vCnfs     = Vec_PtrAlloc( 1000 );
+    Vec_PtrPush( p->vCnfs, Vec_IntAlloc(0) );
+    Vec_PtrPush( p->vCnfs, Vec_IntAlloc(0) );
+    // abstraction
+    p->vIds      = Vec_IntStartFull( Gia_ManObjNum(pGia) );
+    p->vProofIds = Vec_IntAlloc( 0 );
+    p->vAbs      = Vec_IntAlloc( 1000 );
+    p->vValues   = Vec_IntAlloc( 1000 );
+    // add constant node to abstraction
+    Ga2_ObjSetId( p, Gia_ManConst0(pGia), 0 );
+    Vec_IntPush( p->vValues, 0 );
+    Vec_IntPush( p->vAbs, 0 );
+    // refinement
+    p->pRnm      = Rnm_ManStart( pGia );
+//    p->pRf2      = Rf2_ManStart( pGia );
+    // SAT solver and variables
+    p->vId2Lit   = Vec_PtrAlloc( 1000 );
+    // temporaries
+    p->vLits     = Vec_IntAlloc( 100 );
+    p->vIsopMem  = Vec_IntAlloc( 100 );
+    Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
+    // hash table
+    p->nTable = Abc_PrimeCudd(1<<18);
+    p->pTable = ABC_CALLOC( int, 6 * p->nTable ); 
+    return p;
+}
+
+void Ga2_ManDumpStats( Gia_Man_t * pGia, Abs_Par_t * pPars, sat_solver2 * pSat, int iFrame, int fUseN )
+{
+    FILE * pFile;
+    char pFileName[32];
+    sprintf( pFileName, "stats_gla%s%s.txt", fUseN ? "n":"", pPars->fUseFullProof ? "p":"" ); 
+
+    pFile = fopen( pFileName, "a+" );
+
+    fprintf( pFile, "%s pi=%d ff=%d and=%d mem=%d bmc=%d", 
+        pGia->pName, 
+        Gia_ManPiNum(pGia), Gia_ManRegNum(pGia), Gia_ManAndNum(pGia), 
+        (int)(1 + sat_solver2_memory_proof(pSat)/(1<<20)),
+        iFrame );
+
+    if ( pGia->vGateClasses )
+    fprintf( pFile, " ff=%d and=%d",                 
+        Gia_GlaCountFlops( pGia, pGia->vGateClasses ),
+        Gia_GlaCountNodes( pGia, pGia->vGateClasses )  );
+
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+}
+void Ga2_ManReportMemory( Ga2_Man_t * p )
+{
+    double memTot = 0;
+    double memAig = 1.0 * p->pGia->nObjsAlloc * sizeof(Gia_Obj_t) + Vec_IntMemory(p->pGia->vMapping);
+    double memSat = sat_solver2_memory( p->pSat, 1 );
+    double memPro = sat_solver2_memory_proof( p->pSat );
+    double memMap = Vec_VecMemoryInt( (Vec_Vec_t *)p->vId2Lit );
+    double memRef = Rnm_ManMemoryUsage( p->pRnm );
+    double memHash= sizeof(int) * 6 * p->nTable;
+    double memOth = sizeof(Ga2_Man_t);
+    memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCnfs );
+    memOth += Vec_IntMemory( p->vIds );
+    memOth += Vec_IntMemory( p->vProofIds );
+    memOth += Vec_IntMemory( p->vAbs );
+    memOth += Vec_IntMemory( p->vValues );
+    memOth += Vec_IntMemory( p->vLits );
+    memOth += Vec_IntMemory( p->vIsopMem );
+    memOth += 336450 + (sizeof(char) + sizeof(char*)) * 65536;
+    memTot = memAig + memSat + memPro + memMap + memRef + memHash + 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: Refine   ", memRef, memTot );
+    ABC_PRMP( "Memory: Hash     ", memHash,memTot );
+    ABC_PRMP( "Memory: Other    ", memOth, memTot );
+    ABC_PRMP( "Memory: TOTAL    ", memTot, memTot );
+}
+void Ga2_ManStop( Ga2_Man_t * p )
+{
+    Vec_IntFreeP( &p->pGia->vMapping );
+    Gia_ManSetPhase( p->pGia );
+    if ( p->pPars->fVerbose )
+        Abc_Print( 1, "SAT solver:  Var = %d  Cla = %d  Conf = %d  Lrn = %d  Reduce = %d  Cex = %d  ObjsAdded = %d\n", 
+            sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), 
+            sat_solver2_nconflicts(p->pSat), sat_solver2_nlearnts(p->pSat), 
+            p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
+    if ( p->pPars->fVerbose )
+    Abc_Print( 1, "Hash hits = %d.  Hash misses = %d.  Hash overs = %d.\n", 
+        p->nHashHit, p->nHashMiss, p->nHashOver );
+
+    if( p->pSat ) sat_solver2_delete( p->pSat );
+    Vec_VecFree( (Vec_Vec_t *)p->vCnfs );
+    Vec_VecFree( (Vec_Vec_t *)p->vId2Lit );
+    Vec_IntFree( p->vIds );
+    Vec_IntFree( p->vProofIds );
+    Vec_IntFree( p->vAbs );
+    Vec_IntFree( p->vValues );
+    Vec_IntFree( p->vLits );
+    Vec_IntFree( p->vIsopMem );
+    Rnm_ManStop( p->pRnm, 0 );
+//    Rf2_ManStop( p->pRf2, p->pPars->fVerbose );
+    ABC_FREE( p->pTable );
+    ABC_FREE( p->pSopSizes );
+    ABC_FREE( p->pSops[1] );
+    ABC_FREE( p->pSops );
+    ABC_FREE( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes a minimized truth table.]
+
+  Description [Input literals can be 0/1 (const 0/1), non-trivial literals 
+  (integers that are more than 1) and unassigned literals (large integers).
+  This procedure computes the truth table that essentially depends on input
+  variables ordered in the increasing order of their positive literals.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Ga2_ObjTruthDepends( unsigned t, int v )
+{
+    static unsigned uInvTruth5[5] = { 0x55555555, 0x33333333, 0x0F0F0F0F, 0x00FF00FF, 0x0000FFFF };
+    assert( v >= 0 && v <= 4 );
+    return ((t ^ (t >> (1 << v))) & uInvTruth5[v]);
+}
+unsigned Ga2_ObjComputeTruthSpecial( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vLits )
+{
+    int fVerbose = 0;
+    static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+    unsigned Res;
+    Gia_Obj_t * pObj;
+    int i, Entry;
+//    int Id = Gia_ObjId(p, pRoot);
+    assert( Gia_ObjIsAnd(pRoot) );
+
+    if ( fVerbose )
+    printf( "Object %d.\n", Gia_ObjId(p, pRoot) );
+
+    // assign elementary truth tables
+    Gia_ManForEachObjVec( vLeaves, p, pObj, i )
+    {
+        Entry = Vec_IntEntry( vLits, i );
+        assert( Entry >= 0 );
+        if ( Entry == 0 )
+            pObj->Value = 0;
+        else if ( Entry == 1 )
+            pObj->Value = ~0;
+        else // non-trivial literal
+            pObj->Value = uTruth5[i];
+        if ( fVerbose )
+        printf( "%d ", Entry );
+    }
+
+    if ( fVerbose )
+    {
+    Res = Ga2_ObjTruth( p, pRoot );
+//    Kit_DsdPrintFromTruth( &Res, Vec_IntSize(vLeaves) );
+    printf( "\n" );
+    }
+
+    // compute truth table
+    Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 );
+    if ( Res != 0 && Res != ~0 )
+    {
+        // find essential variables
+        int nUsed = 0, pUsed[5];
+        for ( i = 0; i < Vec_IntSize(vLeaves); i++ )
+            if ( Ga2_ObjTruthDepends( Res, i ) )
+                pUsed[nUsed++] = i;
+        assert( nUsed > 0 );
+        // order positions by literal value
+        Vec_IntSelectSortCost( pUsed, nUsed, vLits );
+        assert( Vec_IntEntry(vLits, pUsed[0]) <= Vec_IntEntry(vLits, pUsed[nUsed-1]) );
+        // assign elementary truth tables to the leaves
+        Gia_ManForEachObjVec( vLeaves, p, pObj, i )
+        {
+            Entry = Vec_IntEntry( vLits, i );
+            assert( Entry >= 0 );
+            if ( Entry == 0 )
+                pObj->Value = 0;
+            else if ( Entry == 1 )
+                pObj->Value = ~0;
+            else // non-trivial literal
+                pObj->Value = 0xDEADCAFE; // not important
+        }
+        for ( i = 0; i < nUsed; i++ )
+        {
+            Entry = Vec_IntEntry( vLits, pUsed[i] );
+            assert( Entry > 1 );
+            pObj = Gia_ManObj( p, Vec_IntEntry(vLeaves, pUsed[i]) );
+            pObj->Value = Abc_LitIsCompl(Entry) ? ~uTruth5[i] : uTruth5[i];
+//            pObj->Value = uTruth5[i];
+            // remember this literal
+            pUsed[i] = Abc_LitRegular(Entry);
+//            pUsed[i] = Entry;
+        }
+        // compute truth table
+        Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 );
+        // reload the literals
+        Vec_IntClear( vLits );
+        for ( i = 0; i < nUsed; i++ )
+        {
+            Vec_IntPush( vLits, pUsed[i] );
+            assert( Ga2_ObjTruthDepends(Res, i) );
+            if ( fVerbose )
+            printf( "%d ", pUsed[i] );
+        }
+        for ( ; i < 5; i++ )
+            assert( !Ga2_ObjTruthDepends(Res, i) );
+
+if ( fVerbose )
+{
+//    Kit_DsdPrintFromTruth( &Res, nUsed );
+    printf( "\n" );
+}
+
+    }
+    else
+    {
+
+if ( fVerbose )
+{
+    Vec_IntClear( vLits );
+    printf( "Const %d\n", Res > 0 );
+}
+
+    }
+    Gia_ManForEachObjVec( vLeaves, p, pObj, i )
+        pObj->Value = 0;
+    return Res;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns CNF of the function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Ga2_ManCnfCompute( unsigned uTruth, int nVars, Vec_Int_t * vCover )
+{
+    extern int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth );
+    int RetValue;
+    assert( nVars <= 5 );
+    // transform truth table into the SOP
+    RetValue = Kit_TruthIsop( &uTruth, nVars, vCover, 0 );
+    assert( RetValue == 0 );
+    // check the case of constant cover
+    return Vec_IntDup( vCover );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives CNF for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Ga2_ManCnfAddDynamic( Ga2_Man_t * p, int uTruth, int Lits[], int iLitOut, int ProofId )
+{
+    int i, k, b, Cube, nClaLits, ClaLits[6];
+//    assert( uTruth > 0 && uTruth < 0xffff );
+    for ( i = 0; i < 2; i++ )
+    {
+        if ( i )
+            uTruth = 0xffff & ~uTruth;
+//        Extra_PrintBinary( stdout, &uTruth, 16 ); printf( "\n" );
+        for ( k = 0; k < p->pSopSizes[uTruth]; k++ )
+        {
+            nClaLits = 0;
+            ClaLits[nClaLits++] = i ? lit_neg(iLitOut) : iLitOut;
+            Cube = p->pSops[uTruth][k];
+            for ( b = 3; b >= 0; b-- )
+            {
+                if ( Cube % 3 == 0 ) // value 0 --> add positive literal
+                {
+                    assert( Lits[b] > 1 );
+                    ClaLits[nClaLits++] = Lits[b];
+                }
+                else if ( Cube % 3 == 1 ) // value 1 --> add negative literal
+                {
+                    assert( Lits[b] > 1 );
+                    ClaLits[nClaLits++] = lit_neg(Lits[b]);
+                }
+                Cube = Cube / 3;
+            }
+            sat_solver2_addclause( p->pSat, ClaLits, ClaLits+nClaLits, ProofId );
+        }
+    }
+}
+void Ga2_ManCnfAddStatic( sat_solver2 * pSat, Vec_Int_t * vCnf0, Vec_Int_t * vCnf1, int Lits[], int iLitOut, int ProofId )
+{
+    Vec_Int_t * vCnf;
+    int i, k, b, Cube, Literal, nClaLits, ClaLits[6];
+    for ( i = 0; i < 2; i++ )
+    {
+        vCnf = i ? vCnf1 : vCnf0;
+        Vec_IntForEachEntry( vCnf, Cube, k )
+        {
+            nClaLits = 0;
+            ClaLits[nClaLits++] = i ? lit_neg(iLitOut) : iLitOut;
+            for ( b = 0; b < 5; b++ )
+            {
+                Literal = 3 & (Cube >> (b << 1));
+                if ( Literal == 1 ) // value 0 --> add positive literal
+                {
+//                    assert( Lits[b] > 1 );
+                    ClaLits[nClaLits++] = Lits[b];
+                }
+                else if ( Literal == 2 ) // value 1 --> add negative literal
+                {
+//                    assert( Lits[b] > 1 );
+                    ClaLits[nClaLits++] = lit_neg(Lits[b]);
+                }
+                else if ( Literal != 0 )
+                    assert( 0 );
+            }
+            sat_solver2_addclause( pSat, ClaLits, ClaLits+nClaLits, ProofId );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Saig_ManBmcHashKey( int * pArray )
+{
+    static int s_Primes[5] = { 12582917, 25165843, 50331653, 100663319, 201326611 };
+    unsigned i, Key = 0;
+    for ( i = 0; i < 5; i++ )
+        Key += pArray[i] * s_Primes[i];
+    return Key;
+}
+static inline int * Saig_ManBmcLookup( Ga2_Man_t * p, int * pArray )
+{
+    int * pTable = p->pTable + 6 * (Saig_ManBmcHashKey(pArray) % p->nTable);
+    if ( memcmp( pTable, pArray, 20 ) )
+    {
+        if ( pTable[0] == 0 )
+            p->nHashMiss++;
+        else
+            p->nHashOver++;
+        memcpy( pTable, pArray, 20 );
+        pTable[5] = 0;
+    }
+    else
+        p->nHashHit++;
+    assert( pTable + 5 < pTable + 6 * p->nTable );
+    return pTable + 5;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs )
+{
+    unsigned uTruth;
+    int nLeaves;
+//    int Id = Gia_ObjId(p->pGia, pObj);
+    assert( pObj->fPhase );
+    assert( Vec_PtrSize(p->vCnfs) == 2 * Vec_IntSize(p->vValues) );
+    // assign abstraction ID to the node
+    if ( Ga2_ObjId(p,pObj) == -1 )
+    {
+        Ga2_ObjSetId( p, pObj, Vec_IntSize(p->vValues) );
+        Vec_IntPush( p->vValues, Gia_ObjId(p->pGia, pObj) );
+        Vec_PtrPush( p->vCnfs, NULL );
+        Vec_PtrPush( p->vCnfs, NULL );
+    }
+    assert( Ga2_ObjCnf0(p, pObj) == NULL );
+    if ( !fAbs )
+        return;
+    Vec_IntPush( p->vAbs, Gia_ObjId(p->pGia, pObj) );
+    assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
+    // compute parameters
+    nLeaves = Ga2_ObjLeaveNum(p->pGia, pObj);
+    uTruth = Ga2_ObjTruth( p->pGia, pObj );
+    // create CNF for pos/neg phases
+    Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj),     Ga2_ManCnfCompute( uTruth, nLeaves, p->vIsopMem) );    
+    Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj) + 1, Ga2_ManCnfCompute(~uTruth, nLeaves, p->vIsopMem) );
+}
+
+static inline void Ga2_ManAddToAbsOneStatic( Ga2_Man_t * p, Gia_Obj_t * pObj, int f, int fUseId )
+{
+    Vec_Int_t * vLeaves;
+    Gia_Obj_t * pLeaf;
+    int k, Lit, iLitOut = Ga2_ObjFindOrAddLit( p, pObj, f );
+    assert( iLitOut > 1 );
+    assert( Gia_ObjIsConst0(pObj) || Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) );
+    if ( Gia_ObjIsConst0(pObj) || (f == 0 && Gia_ObjIsRo(p->pGia, pObj)) )
+    {
+        iLitOut = Abc_LitNot( iLitOut );
+        sat_solver2_addclause( p->pSat, &iLitOut, &iLitOut + 1, fUseId ? Gia_ObjId(p->pGia, pObj) : -1 );
+    }
+    else
+    {
+        int fUseStatic = 1;
+        Vec_IntClear( p->vLits );
+        vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
+        Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, k )
+        {
+            Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f - Gia_ObjIsRo(p->pGia, pObj) );
+            Vec_IntPush( p->vLits, Lit );
+            if ( Lit < 2 )
+                fUseStatic = 0;
+        }
+        if ( fUseStatic || Gia_ObjIsRo(p->pGia, pObj) )
+            Ga2_ManCnfAddStatic( p->pSat, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, fUseId ? Gia_ObjId(p->pGia, pObj) : -1 );
+        else
+        {
+            unsigned uTruth = Ga2_ObjComputeTruthSpecial( p->pGia, pObj, vLeaves, p->vLits );
+            Ga2_ManCnfAddDynamic( p, uTruth & 0xFFFF, Vec_IntArray(p->vLits), iLitOut, Gia_ObjId(p->pGia, pObj) );
+        }
+    }
+}
+static inline void Ga2_ManAddToAbsOneDynamic( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
+{
+//    int Id = Gia_ObjId(p->pGia, pObj);
+    Vec_Int_t * vLeaves;
+    Gia_Obj_t * pLeaf;
+    unsigned uTruth;
+    int i, Lit;
+
+    assert( Ga2_ObjIsAbs0(p, pObj) );
+    assert( Gia_ObjIsConst0(pObj) || Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) );
+    if ( Gia_ObjIsConst0(pObj) || (f == 0 && Gia_ObjIsRo(p->pGia, pObj)) )
+    {
+        Ga2_ObjAddLit( p, pObj, f, 0 );
+    }
+    else if ( Gia_ObjIsRo(p->pGia, pObj) )
+    {
+        // if flop is included in the abstraction, but its driver is not
+        // flop input driver has no variable assigned -- we assign it here
+        pLeaf = Gia_ObjRoToRi( p->pGia, pObj );
+        Lit = Ga2_ObjFindOrAddLit( p, Gia_ObjFanin0(pLeaf), f-1 );
+        assert( Lit >= 0 );
+        Lit = Abc_LitNotCond( Lit, Gia_ObjFaninC0(pLeaf) );
+        Ga2_ObjAddLit( p, pObj, f, Lit );
+    }
+    else
+    {
+        assert( Gia_ObjIsAnd(pObj) );
+        Vec_IntClear( p->vLits );
+        vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
+        Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, i )
+        {
+            if ( Ga2_ObjIsAbs0(p, pLeaf) )      // belongs to original abstraction
+            {
+                Lit = Ga2_ObjFindLit( p, pLeaf, f );
+                assert( Lit >= 0 );
+            }
+            else if ( Ga2_ObjIsLeaf0(p, pLeaf) ) // belongs to original PPIs
+            {
+                Lit = Ga2_ObjFindLit( p, pLeaf, f );
+//                Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f );
+                if ( Lit == -1 )
+                {
+                    Lit = GA2_BIG_NUM + 2*i;
+//                    assert( 0 );
+                }
+            }
+            else assert( 0 );
+            Vec_IntPush( p->vLits, Lit );
+        }
+
+        // minimize truth table
+        uTruth = Ga2_ObjComputeTruthSpecial( p->pGia, pObj, vLeaves, p->vLits );
+        if ( uTruth == 0 || uTruth == ~0 ) // const 0 / 1
+        {
+            Lit = (uTruth > 0);
+            Ga2_ObjAddLit( p, pObj, f, Lit );
+        }
+        else if ( uTruth == 0xAAAAAAAA || uTruth == 0x55555555 )  // buffer / inverter
+        {
+            Lit = Vec_IntEntry( p->vLits, 0 );
+            if ( Lit >= GA2_BIG_NUM )
+            {
+                pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, (Lit-GA2_BIG_NUM)/2) );
+                Lit = Ga2_ObjFindLit( p, pLeaf, f );
+                assert( Lit == -1 );
+                Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f );
+            }
+            assert( Lit >= 0 );
+            Lit = Abc_LitNotCond( Lit, uTruth == 0x55555555 );
+            Ga2_ObjAddLit( p, pObj, f, Lit );
+            assert( Lit < 10000000 );
+        }
+        else
+        {
+            assert( Vec_IntSize(p->vLits) > 1 && Vec_IntSize(p->vLits) < 6 );
+            // replace literals
+            Vec_IntForEachEntry( p->vLits, Lit, i )
+            {
+                if ( Lit >= GA2_BIG_NUM )
+                {
+                    pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, (Lit-GA2_BIG_NUM)/2) );
+                    Lit = Ga2_ObjFindLit( p, pLeaf, f );
+                    assert( Lit == -1 );
+                    Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f );
+                    Vec_IntWriteEntry( p->vLits, i, Lit );
+                }
+                assert( Lit < 10000000 );
+            }
+
+            // add new nodes
+            if ( Vec_IntSize(p->vLits) == 5 )
+            {
+                Vec_IntClear( p->vLits );
+                Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, i )
+                    Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pLeaf, f ) );
+                Lit = Ga2_ObjFindOrAddLit(p, pObj, f);
+                Ga2_ManCnfAddStatic( p->pSat, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), Lit, -1 );
+            }
+            else
+            {
+//                int fUseHash = 1;
+                if ( !p->pPars->fSkipHash )
+                {
+                    int * pLookup, nSize = Vec_IntSize(p->vLits);
+                    assert( Vec_IntSize(p->vLits) < 5 );
+                    assert( Vec_IntEntry(p->vLits, 0) <= Vec_IntEntryLast(p->vLits) );
+                    assert( Ga2_ObjFindLit(p, pObj, f) == -1 );
+                    for ( i = Vec_IntSize(p->vLits); i < 4; i++ )
+                        Vec_IntPush( p->vLits, GA2_BIG_NUM );
+                    Vec_IntPush( p->vLits, (int)uTruth );
+                    assert( Vec_IntSize(p->vLits) == 5 );
+
+                    // perform structural hashing here!!!
+                    pLookup = Saig_ManBmcLookup( p, Vec_IntArray(p->vLits) );
+                    if ( *pLookup == 0 )
+                    {
+                        *pLookup = Ga2_ObjFindOrAddLit(p, pObj, f);
+                        Vec_IntShrink( p->vLits, nSize );
+                        Ga2_ManCnfAddDynamic( p, uTruth & 0xFFFF, Vec_IntArray(p->vLits), *pLookup, -1 );
+                    }
+                    else
+                        Ga2_ObjAddLit( p, pObj, f, *pLookup );
+
+                }
+                else
+                {
+                    Lit = Ga2_ObjFindOrAddLit(p, pObj, f);
+                    Ga2_ManCnfAddDynamic( p, uTruth & 0xFFFF, Vec_IntArray(p->vLits), Lit, -1 );
+                }
+            }
+        }
+    }
+}
+
+void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f )
+{
+    int fSimple = 0;
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
+    {
+        if ( i == p->LimAbs )
+            break;
+        if ( fSimple )
+            Ga2_ManAddToAbsOneStatic( p, pObj, f, 0 );
+        else
+            Ga2_ManAddToAbsOneDynamic( p, pObj, f );
+    }
+    Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
+        if ( i >= p->LimAbs )
+            Ga2_ManAddToAbsOneStatic( p, pObj, f, 1 );
+//    sat_solver2_simplify( p->pSat );
+}
+
+void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
+{
+    Vec_Int_t * vLeaves;
+    Gia_Obj_t * pObj, * pFanin;
+    int f, i, k;
+    // add abstraction objects
+    Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
+    {
+        Ga2_ManSetupNode( p, pObj, 1 );
+        if ( p->pSat->pPrf2 )
+            Vec_IntWriteEntry( p->vProofIds, Gia_ObjId(p->pGia, pObj), p->nProofIds++ );
+    }
+    // add PPI objects
+    Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
+    {
+        vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
+        Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
+            if ( Ga2_ObjId( p, pFanin ) == -1 )
+                Ga2_ManSetupNode( p, pFanin, 0 );
+    }
+    // add new clauses to the timeframes
+    for ( f = 0; f <= p->pPars->iFrame; f++ )
+    {
+        Vec_IntFillExtra( Ga2_MapFrameMap(p, f), Vec_IntSize(p->vValues), -1 );
+        Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
+            Ga2_ManAddToAbsOneStatic( p, pObj, f, 1 );
+    }
+//    sat_solver2_simplify( p->pSat );
+}
+
+void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues, int nSatVars )
+{
+    Vec_Int_t * vMap;
+    Gia_Obj_t * pObj;
+    int i, k, Entry;
+    assert( nAbs > 0 );
+    assert( nValues > 0 );
+    assert( nSatVars > 0 );
+    // shrink abstraction
+    Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
+    {
+        if ( !i ) continue;
+        assert( Ga2_ObjCnf0(p, pObj) != NULL );
+        assert( Ga2_ObjCnf1(p, pObj) != NULL );
+        if ( i < nAbs )
+            continue;
+        Vec_IntFree( Ga2_ObjCnf0(p, pObj) );
+        Vec_IntFree( Ga2_ObjCnf1(p, pObj) );
+        Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj),     NULL );    
+        Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj) + 1, NULL );
+    }
+    Vec_IntShrink( p->vAbs, nAbs );
+    // shrink values
+    Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
+    {
+        assert( Ga2_ObjId(p,pObj) >= 0 );
+        if ( i < nValues )
+            continue;
+        Ga2_ObjSetId( p, pObj, -1 );
+    }
+    Vec_IntShrink( p->vValues, nValues );
+    Vec_PtrShrink( p->vCnfs, 2 * nValues );
+    // hack to clear constant
+    if ( nValues == 1 )
+        nValues = 0;
+    // clean mapping for each timeframe
+    Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i )
+    {
+        Vec_IntShrink( vMap, nValues );
+        Vec_IntForEachEntryStart( vMap, Entry, k, p->LimAbs )
+            if ( Entry >= 2*nSatVars )
+                Vec_IntWriteEntry( vMap, k, -1 );
+    }
+    // shrink SAT variables
+    p->nSatVars = nSatVars;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ga2_ManAbsTranslate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vClasses, int fFirst )
+{
+    if ( pObj->fPhase && !fFirst )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Ga2_ManAbsTranslate_rec( p, Gia_ObjFanin0(pObj), vClasses, 0 );
+    Ga2_ManAbsTranslate_rec( p, Gia_ObjFanin1(pObj), vClasses, 0 );
+    Vec_IntWriteEntry( vClasses, Gia_ObjId(p, pObj), 1 );
+}
+
+Vec_Int_t * Ga2_ManAbsTranslate( Ga2_Man_t * p )
+{
+    Vec_Int_t * vGateClasses;
+    Gia_Obj_t * pObj;
+    int i;
+    vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) );
+    Vec_IntWriteEntry( vGateClasses, 0, 1 );
+    Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+            Ga2_ManAbsTranslate_rec( p->pGia, pObj, vGateClasses, 1 );
+        else if ( Gia_ObjIsRo(p->pGia, pObj) )
+            Vec_IntWriteEntry( vGateClasses, Gia_ObjId(p->pGia, pObj), 1 );
+        else if ( !Gia_ObjIsConst0(pObj) )
+            assert( 0 );
+//        Gia_ObjPrint( p->pGia, pObj );
+    }
+    return vGateClasses;
+}
+
+Vec_Int_t * Ga2_ManAbsDerive( Gia_Man_t * p )
+{
+    Vec_Int_t * vToAdd;
+    Gia_Obj_t * pObj;
+    int i;
+    vToAdd = Vec_IntAlloc( 1000 );
+    Gia_ManForEachRo( p, pObj, i )
+        if ( pObj->fPhase && Vec_IntEntry(p->vGateClasses, Gia_ObjId(p, pObj)) )
+            Vec_IntPush( vToAdd, Gia_ObjId(p, pObj) );
+    Gia_ManForEachAnd( p, pObj, i )
+        if ( pObj->fPhase && Vec_IntEntry(p->vGateClasses, i) )
+            Vec_IntPush( vToAdd, i );
+    return vToAdd;
+}
+
+void Ga2_ManRestart( Ga2_Man_t * p )
+{
+    Vec_Int_t * vToAdd;
+    int Lit = 1;
+    assert( p->pGia != NULL && p->pGia->vGateClasses != NULL );
+    assert( Gia_ManPi(p->pGia, 0)->fPhase ); // marks are set
+    // clear SAT variable numbers (begin with 1)
+    if ( p->pSat ) sat_solver2_delete( p->pSat );
+    p->pSat      = sat_solver2_new();
+    p->pSat->nLearntStart = p->pPars->nLearnedStart;
+    p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
+    p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
+    p->pSat->nLearntMax   = p->pSat->nLearntStart;
+    // add clause x0 = 0  (lit0 = 1; lit1 = 0)
+    sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, -1 );
+    // remove previous abstraction
+    Ga2_ManShrinkAbs( p, 1, 1, 1 );
+    // start new abstraction
+    vToAdd = Ga2_ManAbsDerive( p->pGia );
+    assert( p->pSat->pPrf2 == NULL );
+    assert( p->pPars->iFrame < 0 );
+    Ga2_ManAddToAbs( p, vToAdd );
+    Vec_IntFree( vToAdd );
+    p->LimAbs = Vec_IntSize(p->vAbs);
+    p->LimPpi = Vec_IntSize(p->vValues);
+    // set runtime limit
+    if ( p->pPars->nTimeOut )
+        sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + p->timeStart );
+    // clean the hash table
+    memset( p->pTable, 0, 6 * sizeof(int) * p->nTable );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Vec_IntCheckUnique( Vec_Int_t * p )
+{
+    int RetValue;
+    Vec_Int_t * pDup = Vec_IntDup( p );
+    Vec_IntUniqify( pDup );
+    RetValue = Vec_IntSize(p) - Vec_IntSize(pDup);
+    Vec_IntFree( pDup );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Ga2_ObjSatValue( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
+{
+    int Lit = Ga2_ObjFindLit( p, pObj, f );
+    assert( !Gia_ObjIsConst0(pObj) );
+    if ( Lit == -1 )
+        return 0;
+    if ( Abc_Lit2Var(Lit) >= p->pSat->size )
+        return 0;
+    return Abc_LitIsCompl(Lit) ^ sat_solver2_var_value( p->pSat, Abc_Lit2Var(Lit) );
+}
+Abc_Cex_t * Ga2_ManDeriveCex( Ga2_Man_t * p, Vec_Int_t * vPis )
+{
+    Abc_Cex_t * pCex;
+    Gia_Obj_t * pObj;
+    int i, f;
+    pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 );
+    pCex->iPo = 0;
+    pCex->iFrame = p->pPars->iFrame;
+    Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
+    {
+        if ( !Gia_ObjIsPi(p->pGia, pObj) )
+            continue;
+        assert( Gia_ObjIsPi(p->pGia, pObj) );
+        for ( f = 0; f <= pCex->iFrame; f++ )
+            if ( Ga2_ObjSatValue( p, pObj, f ) )
+                Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Gia_ObjCioId(pObj) );
+    }
+    return pCex;
+} 
+void Ga2_ManRefinePrint( Ga2_Man_t * p, Vec_Int_t * vVec )
+{
+    Gia_Obj_t * pObj, * pFanin;
+    int i, k;
+    printf( "\n         Unsat core: \n" );
+    Gia_ManForEachObjVec( vVec, p->pGia, pObj, i )
+    {
+        Vec_Int_t * vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
+        printf( "%12d : ", i );
+        printf( "Obj =%6d ", Gia_ObjId(p->pGia, pObj) );
+        if ( Gia_ObjIsRo(p->pGia, pObj) )
+            printf( "ff " );
+        else
+            printf( "   " );
+        if ( Ga2_ObjIsAbs0(p, pObj) )
+            printf( "a " );
+        else if ( Ga2_ObjIsLeaf0(p, pObj) )
+            printf( "l " );
+        else 
+            printf( "  " );
+        printf( "Fanins: " );
+        Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
+        {
+            printf( "%6d ", Gia_ObjId(p->pGia, pFanin) );
+            if ( Gia_ObjIsRo(p->pGia, pFanin) )
+                printf( "ff " );
+            else
+                printf( "   " );
+            if ( Ga2_ObjIsAbs0(p, pFanin) )
+                printf( "a " );
+            else if ( Ga2_ObjIsLeaf0(p, pFanin) )
+                printf( "l " );
+            else
+                printf( "  " );
+        }
+        printf( "\n" );
+    }
+}
+void Ga2_ManRefinePrintPPis( Ga2_Man_t * p )
+{
+    Vec_Int_t * vVec = Vec_IntAlloc( 100 );
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
+    {
+        if ( !i ) continue;
+        if ( Ga2_ObjIsAbs(p, pObj) )
+            continue;
+        assert( pObj->fPhase );
+        assert( Ga2_ObjIsLeaf(p, pObj) );
+        assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj) );
+        Vec_IntPush( vVec, Gia_ObjId(p->pGia, pObj) );
+    }
+    printf( "        Current PPIs (%d): ", Vec_IntSize(vVec) );
+    Vec_IntSort( vVec, 1 );
+    Gia_ManForEachObjVec( vVec, p->pGia, pObj, i )
+        printf( "%d ", Gia_ObjId(p->pGia, pObj) );
+    printf( "\n" );
+    Vec_IntFree( vVec );
+}
+
+
+void Ga2_GlaPrepareCexAndMap( Ga2_Man_t * p, Abc_Cex_t ** ppCex, Vec_Int_t ** pvMaps )
+{
+    Abc_Cex_t * pCex;
+    Vec_Int_t * vMap;
+    Gia_Obj_t * pObj;
+    int f, i, k;
+/*
+    Gia_ManForEachObj( p->pGia, pObj, i )
+        if ( Ga2_ObjId(p, pObj) >= 0 )
+            assert( Vec_IntEntry(p->vValues, Ga2_ObjId(p, pObj)) == i );
+*/
+    // find PIs and PPIs
+    vMap = Vec_IntAlloc( 1000 );
+    Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
+    {
+        if ( !i ) continue;
+        if ( Ga2_ObjIsAbs(p, pObj) )
+            continue;
+        assert( pObj->fPhase );
+        assert( Ga2_ObjIsLeaf(p, pObj) );
+        assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj) );
+        Vec_IntPush( vMap, Gia_ObjId(p->pGia, pObj) );
+    }
+    // derive counter-example
+    pCex = Abc_CexAlloc( 0, Vec_IntSize(vMap), p->pPars->iFrame+1 );
+    pCex->iFrame = p->pPars->iFrame;
+    for ( f = 0; f <= p->pPars->iFrame; f++ )
+        Gia_ManForEachObjVec( vMap, p->pGia, pObj, k )
+            if ( Ga2_ObjSatValue( p, pObj, f ) )
+                Abc_InfoSetBit( pCex->pData, f * Vec_IntSize(vMap) + k );
+    *pvMaps = vMap;
+    *ppCex = pCex;
+}
+Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p )
+{
+    Abc_Cex_t * pCex;
+    Vec_Int_t * vMap, * vVec;
+    Gia_Obj_t * pObj;
+    int i, k;
+    if ( p->pPars->fAddLayer )
+    {
+        // use simplified refinement strategy, which adds logic near at PPI without finding important ones
+        vVec = Vec_IntAlloc( 100 );
+        Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
+        {
+            if ( !i ) continue;
+            if ( Ga2_ObjIsAbs(p, pObj) )
+                continue;
+            assert( pObj->fPhase );
+            assert( Ga2_ObjIsLeaf(p, pObj) );
+            assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj) );
+            if ( Gia_ObjIsPi(p->pGia, pObj) )
+                continue;
+            Vec_IntPush( vVec, Gia_ObjId(p->pGia, pObj) );
+        }
+        p->nObjAdded += Vec_IntSize(vVec);
+        return vVec;
+    }
+    Ga2_GlaPrepareCexAndMap( p, &pCex, &vMap );
+ //    Rf2_ManRefine( p->pRf2, pCex, vMap, p->pPars->fPropFanout, 1 );
+    vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 1, 1 );
+//    printf( "Refinement %d\n", Vec_IntSize(vVec) );
+    Abc_CexFree( pCex );
+    if ( Vec_IntSize(vVec) == 0 )
+    {
+        Vec_IntFree( vVec );
+        Abc_CexFreeP( &p->pGia->pCexSeq );
+        p->pGia->pCexSeq = Ga2_ManDeriveCex( p, vMap );
+        Vec_IntFree( vMap );
+        return NULL;
+    }
+    Vec_IntFree( vMap );
+    // remove those already added
+    k = 0;
+    Gia_ManForEachObjVec( vVec, p->pGia, pObj, i )
+        if ( !Ga2_ObjIsAbs(p, pObj) )
+            Vec_IntWriteEntry( vVec, k++, Gia_ObjId(p->pGia, pObj) );
+    Vec_IntShrink( vVec, k );
+
+    // these objects should be PPIs that are not abstracted yet
+    Gia_ManForEachObjVec( vVec, p->pGia, pObj, i )
+        assert( pObj->fPhase );//&& Ga2_ObjIsLeaf(p, pObj) );
+    p->nObjAdded += Vec_IntSize(vVec);
+    return vVec;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a new manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ga2_GlaAbsCount( Ga2_Man_t * p, int fRo, int fAnd )
+{
+    Gia_Obj_t * pObj;
+    int i, Counter = 0;
+    if ( fRo )
+        Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
+            Counter += Gia_ObjIsRo(p->pGia, pObj);
+    else if ( fAnd )
+        Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
+            Counter += Gia_ObjIsAnd(pObj);
+    else assert( 0 );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ga2_ManAbsPrintFrame( Ga2_Man_t * p, int nFrames, int nConfls, int nCexes, clock_t Time, int fFinal )
+{
+    if ( Abc_FrameIsBatchMode() && !(((fFinal && nCexes) || p->pPars->fVeryVerbose)) )
+        return;
+    Abc_Print( 1, "%4d :", nFrames );
+    Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * Vec_IntSize(p->vAbs) / p->nMarked) ); 
+    Abc_Print( 1, "%6d", Vec_IntSize(p->vAbs) );
+    Abc_Print( 1, "%5d", Vec_IntSize(p->vValues)-Vec_IntSize(p->vAbs)-1 );
+    Abc_Print( 1, "%5d", Ga2_GlaAbsCount(p, 1, 0) );
+    Abc_Print( 1, "%6d", Ga2_GlaAbsCount(p, 0, 1) );
+    Abc_Print( 1, "%8d", nConfls );
+    if ( nCexes == 0 )
+        Abc_Print( 1, "%5c", '-' ); 
+    else
+        Abc_Print( 1, "%5d", nCexes ); 
+    Abc_PrintInt( sat_solver2_nvars(p->pSat) );
+    Abc_PrintInt( sat_solver2_nclauses(p->pSat) );
+    Abc_PrintInt( sat_solver2_nlearnts(p->pSat) );
+    Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
+    Abc_Print( 1, "%5.0f MB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<20) );
+    Abc_Print( 1, "%s", ((fFinal && nCexes) || p->pPars->fVeryVerbose) ? "\n" : "\r" );
+    fflush( stdout );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Send abstracted model or send cancel.]
+
+  Description [Counter-example will be sent automatically when &vta terminates.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Ga2_GlaGetFileName( Ga2_Man_t * p, int fAbs )
+{
+    static char * pFileNameDef = "glabs.aig";
+    if ( p->pPars->pFileVabs )
+        return p->pPars->pFileVabs;
+    if ( p->pGia->pSpec )
+    {
+        if ( fAbs )
+            return Extra_FileNameGenericAppend( p->pGia->pSpec, "_abs.aig");
+        else
+            return Extra_FileNameGenericAppend( p->pGia->pSpec, "_gla.aig");
+    }
+    return pFileNameDef;
+}
+
+void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose )
+{
+    char * pFileName;
+    assert( p->pPars->fDumpMabs || p->pPars->fDumpVabs || p->pPars->fCallProver );
+    if ( p->pPars->fDumpMabs )
+    {
+        pFileName = Ga2_GlaGetFileName(p, 0);
+//        if ( fVerbose )
+//            Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName );
+        // dump abstraction map
+        Vec_IntFreeP( &p->pGia->vGateClasses );
+        p->pGia->vGateClasses = Ga2_ManAbsTranslate( p );
+        Gia_WriteAiger( p->pGia, pFileName, 0, 0 );
+    }
+    if ( p->pPars->fDumpVabs || p->pPars->fCallProver )
+    {
+        Vec_Int_t * vGateClasses;
+        Gia_Man_t * pAbs;
+        pFileName = Ga2_GlaGetFileName(p, 1);
+//        if ( fVerbose )
+//            Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
+        // dump absracted model
+        vGateClasses = Ga2_ManAbsTranslate( p );
+        pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
+        Gia_ManCleanValue( p->pGia );
+        Gia_WriteAiger( pAbs, pFileName, 0, 0 );
+        Gia_ManStop( pAbs );
+        Vec_IntFreeP( &vGateClasses );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Send abstracted model or send cancel.]
+
+  Description [Counter-example will be sent automatically when &vta terminates.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_Ga2SendAbsracted( Ga2_Man_t * p, int fVerbose )
+{
+    extern int Gia_ManToBridgeAbsNetlist( FILE * pFile, Gia_Man_t * p );
+    Gia_Man_t * pAbs;
+    Vec_Int_t * vGateClasses;
+    assert( Abc_FrameIsBridgeMode() );
+//    if ( fVerbose )
+//        Abc_Print( 1, "Sending abstracted model...\n" );
+    // create abstraction (value of p->pGia is not used here)
+    vGateClasses = Ga2_ManAbsTranslate( p );
+    pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
+    Vec_IntFreeP( &vGateClasses );
+    Gia_ManCleanValue( p->pGia );
+    // send it out
+    Gia_ManToBridgeAbsNetlist( stdout, pAbs );
+    Gia_ManStop( pAbs );
+}
+void Gia_Ga2SendCancel( Ga2_Man_t * p, int fVerbose )
+{
+    extern int Gia_ManToBridgeBadAbs( FILE * pFile );
+    assert( Abc_FrameIsBridgeMode() );
+//    if ( fVerbose )
+//        Abc_Print( 1, "Cancelling previously sent model...\n" );
+    Gia_ManToBridgeBadAbs( stdout );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs gate-level abstraction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
+{
+    int fUseSecondCore = 1;
+    Ga2_Man_t * p;
+    Vec_Int_t * vCore, * vPPis;
+    clock_t clk2, clk = clock();
+    int Status = l_Undef, RetValue = -1, iFrameTryToProve = -1, fOneIsSent = 0;
+    int i, c, f, Lit;
+    // check trivial case 
+    assert( Gia_ManPoNum(pAig) == 1 ); 
+    ABC_FREE( pAig->pCexSeq );
+    if ( Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManPo(pAig,0))) )
+    {
+        if ( !Gia_ObjFaninC0(Gia_ManPo(pAig,0)) )
+        {
+            Abc_Print( 1, "Sequential miter is trivially UNSAT.\n" );
+            return 1;
+        }
+        pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 );
+        Abc_Print( 1, "Sequential miter is trivially SAT.\n" );
+        return 0;
+    }
+    // create gate classes if not given
+    if ( pAig->vGateClasses == NULL )
+    {
+        pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
+        Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
+        Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)), 1 );
+    }
+    // start the manager
+    p = Ga2_ManStart( pAig, pPars );
+    p->timeInit = clock() - clk;
+    // perform initial abstraction
+    if ( p->pPars->fVerbose )
+    {
+        Abc_Print( 1, "Running gate-level abstraction (GLA) with the following parameters:\n" );
+        Abc_Print( 1, "FrameMax = %d  ConfMax = %d  Timeout = %d  RatioMin = %d %%  RatioMax = %d %%\n", 
+            pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin, pPars->nRatioMax );
+        Abc_Print( 1, "LrnStart = %d  LrnDelta = %d  LrnRatio = %d %%  Skip = %d  SimpleCNF = %d  Dump = %d\n", 
+            pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs|pPars->fCallProver );
+        if ( pPars->fDumpVabs || pPars->fDumpMabs )
+            Abc_Print( 1, "%s will be dumped into file \"%s\".\n", 
+                pPars->fDumpVabs ? "Abstracted model" : "Miter with abstraction map",
+                Ga2_GlaGetFileName(p, pPars->fDumpVabs) );
+        Abc_Print( 1, " Frame   %%   Abs  PPI   FF   LUT   Confl  Cex   Vars   Clas   Lrns     Time        Mem\n" );
+    }
+    // iterate unrolling
+    for ( i = f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; i++ )
+    {
+        int nAbsOld;
+        // remember the timeframe
+        p->pPars->iFrame = -1;
+        // create new SAT solver
+        Ga2_ManRestart( p );
+        // remember abstraction size after the last restart
+        nAbsOld = Vec_IntSize(p->vAbs);
+        // unroll the circuit
+        for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ )
+        {
+            // remember current limits
+            int nConflsBeg = sat_solver2_nconflicts(p->pSat);
+            int nAbs       = Vec_IntSize(p->vAbs);
+            int nValues    = Vec_IntSize(p->vValues);
+            int nVarsOld;
+            // remember the timeframe
+            p->pPars->iFrame = f;
+            // extend and clear storage
+            if ( f == Vec_PtrSize(p->vId2Lit) )
+                Vec_PtrPush( p->vId2Lit, Vec_IntAlloc(0) );
+            Vec_IntFillExtra( Ga2_MapFrameMap(p, f), Vec_IntSize(p->vValues), -1 );
+            // add static clauses to this timeframe
+            Ga2_ManAddAbsClauses( p, f );
+            // skip checking if skipcheck is enabled (&gla -s)
+            if ( p->pPars->fUseSkip && f <= p->pPars->iFrameProved )
+                continue;
+            // skip checking if we need to skip several starting frames (&gla -S <num>)
+            if ( p->pPars->nFramesStart && f <= p->pPars->nFramesStart )
+                continue;
+            // get the output literal
+//            Lit = Ga2_ManUnroll_rec( p, Gia_ManPo(pAig,0), f );
+            Lit = Ga2_ObjFindLit( p, Gia_ObjFanin0(Gia_ManPo(pAig,0)), f );
+            assert( Lit >= 0 );
+            Lit = Abc_LitNotCond( Lit, Gia_ObjFaninC0(Gia_ManPo(pAig,0)) );
+            if ( Lit == 0 )
+                continue;
+            assert( Lit > 1 );
+            // check for counter-examples
+            if ( p->nSatVars > sat_solver2_nvars(p->pSat) )
+                sat_solver2_setnvars( p->pSat, p->nSatVars );
+            nVarsOld = p->nSatVars;
+            for ( c = 0; ; c++ )
+            {
+                // consider the special case when the target literal is implied false
+                // by implications which happened as a result of previous refinements
+                // note that incremental UNSAT core cannot be computed because there is no learned clauses
+                // in this case, we will assume that UNSAT core cannot reduce the problem
+                if ( var_is_assigned(p->pSat, Abc_Lit2Var(Lit)) )
+                {
+                    Prf_ManStopP( &p->pSat->pPrf2 );
+                    break;
+                }
+                // perform SAT solving
+                clk2 = clock();
+                Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+                if ( Status == l_True ) // perform refinement
+                {
+                    p->nCexes++;
+                    p->timeSat += clock() - clk2;
+
+                    // cancel old one if it was sent
+                    if ( Abc_FrameIsBridgeMode() && fOneIsSent )
+                    {
+                        Gia_Ga2SendCancel( p, pPars->fVerbose );
+                        fOneIsSent = 0;
+                    }
+                    if ( iFrameTryToProve >= 0 )
+                    {
+                        Gia_Ga2ProveCancel( pPars->fVerbose );
+                        iFrameTryToProve = -1;
+                    }
+
+                    // perform refinement
+                    clk2 = clock();
+                    vPPis = Ga2_ManRefine( p );
+                    p->timeCex += clock() - clk2;
+                    if ( vPPis == NULL )
+                    {
+                        if ( pPars->fVerbose )
+                            Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 );
+                        goto finish;
+                    }
+
+                    if ( c == 0 )
+                    {
+//                        Ga2_ManRefinePrintPPis( p );
+                        // create bookmark to be used for rollback
+                        assert( nVarsOld == p->pSat->size );
+                        sat_solver2_bookmark( p->pSat );
+                        // start incremental proof manager
+                        assert( p->pSat->pPrf2 == NULL );
+                        p->pSat->pPrf2 = Prf_ManAlloc();
+                        if ( p->pSat->pPrf2 )
+                        {
+                            p->nProofIds = 0;
+                            Vec_IntFill( p->vProofIds, Gia_ManObjNum(p->pGia), -1 );
+                            Prf_ManRestart( p->pSat->pPrf2, p->vProofIds, sat_solver2_nlearnts(p->pSat), Vec_IntSize(vPPis) );
+                        }
+                    }
+                    else
+                    {
+                        // resize the proof logger
+                        if ( p->pSat->pPrf2 )
+                            Prf_ManGrow( p->pSat->pPrf2, p->nProofIds + Vec_IntSize(vPPis) );
+                    }
+
+                    Ga2_ManAddToAbs( p, vPPis );
+                    Vec_IntFree( vPPis );
+                    if ( pPars->fVerbose )
+                        Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c+1, clock() - clk, 0 );
+                    continue;
+                }
+                p->timeUnsat += clock() - clk2;
+                if ( Status == l_Undef ) // ran out of resources
+                    goto finish;
+                if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit ) // timeout
+                    goto finish;
+                if ( c == 0 )
+                {
+                    if ( f > p->pPars->iFrameProved )
+                        p->pPars->nFramesNoChange++;
+                    break;
+                }
+                if ( f > p->pPars->iFrameProved )
+                    p->pPars->nFramesNoChange = 0;
+
+                // derive the core
+                assert( p->pSat->pPrf2 != NULL );
+                vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat );
+                Prf_ManStopP( &p->pSat->pPrf2 );
+                // update the SAT solver
+                sat_solver2_rollback( p->pSat );
+                // reduce abstraction
+                Ga2_ManShrinkAbs( p, nAbs, nValues, nVarsOld );
+
+                // purify UNSAT core
+                if ( fUseSecondCore )
+                {
+//                    int nOldCore = Vec_IntSize(vCore);
+                    // reverse the order of objects in the core
+//                    Vec_IntSort( vCore, 0 );
+//                    Vec_IntPrint( vCore );
+                    // create bookmark to be used for rollback
+                    assert( nVarsOld == p->pSat->size );
+                    sat_solver2_bookmark( p->pSat );
+                    // start incremental proof manager
+                    assert( p->pSat->pPrf2 == NULL );
+                    p->pSat->pPrf2 = Prf_ManAlloc();
+                    if ( p->pSat->pPrf2 )
+                    {
+                        p->nProofIds = 0;
+                        Vec_IntFill( p->vProofIds, Gia_ManObjNum(p->pGia), -1 );
+                        Prf_ManRestart( p->pSat->pPrf2, p->vProofIds, sat_solver2_nlearnts(p->pSat), Vec_IntSize(vCore) );
+
+                        Ga2_ManAddToAbs( p, vCore );
+                        Vec_IntFree( vCore );
+                    }
+                    // run SAT solver
+                    clk2 = clock();
+                    Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+                    if ( Status == l_Undef )
+                        goto finish;
+                    assert( Status == l_False );
+                    p->timeUnsat += clock() - clk2;
+
+                    // derive the core
+                    assert( p->pSat->pPrf2 != NULL );
+                    vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat );
+                    Prf_ManStopP( &p->pSat->pPrf2 );
+                    // update the SAT solver
+                    sat_solver2_rollback( p->pSat );
+                    // reduce abstraction
+                    Ga2_ManShrinkAbs( p, nAbs, nValues, nVarsOld );
+//                    printf( "\n%4d -> %4d\n", nOldCore, Vec_IntSize(vCore) );
+                }
+
+                Ga2_ManAddToAbs( p, vCore );
+//                Ga2_ManRefinePrint( p, vCore );
+                Vec_IntFree( vCore );
+                break;
+            }
+            // remember the last proved frame
+            if ( p->pPars->iFrameProved < f )
+                p->pPars->iFrameProved = f;
+            // print statistics
+            if ( pPars->fVerbose )
+                Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 );
+            // check if abstraction was proved
+            if ( Gia_Ga2ProveCheck( pPars->fVerbose ) )
+            {
+                RetValue = 1;
+                goto finish;
+            }
+            if ( c > 0 ) 
+            {
+                if ( p->pPars->fVeryVerbose )
+                    Abc_Print( 1, "\n" );
+                // recompute the abstraction
+                Vec_IntFreeP( &pAig->vGateClasses );
+                pAig->vGateClasses = Ga2_ManAbsTranslate( p );
+                // check if the number of objects is below limit
+                if ( Vec_IntSize(p->vAbs) >= p->nMarked * (100 - pPars->nRatioMin) / 100 )
+                {
+                    Status = l_Undef;
+                    goto finish;
+                }
+            }
+            // check the number of stable frames
+            if ( p->pPars->nFramesNoChange == p->pPars->nFramesNoChangeLim )
+            {
+                // dump the model into file
+                if ( p->pPars->fDumpVabs || p->pPars->fDumpMabs || p->pPars->fCallProver )
+                {
+                    char Command[1000];
+                    Abc_FrameSetStatus( -1 );
+                    Abc_FrameSetCex( NULL );
+                    Abc_FrameSetNFrames( f+1 );
+                    sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig"), ".status") );
+                    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
+                    Ga2_GlaDumpAbsracted( p, pPars->fVerbose );
+                }
+                // call the prover
+                if ( p->pPars->fCallProver )
+                {
+                    // cancel old one if it is proving
+                    if ( iFrameTryToProve >= 0 )
+                        Gia_Ga2ProveCancel( pPars->fVerbose );
+                    // prove new one
+                    Gia_Ga2ProveAbsracted( Ga2_GlaGetFileName(p, 1), pPars->fVerbose );
+                    iFrameTryToProve = f;
+                }
+                // speak to the bridge
+                if ( Abc_FrameIsBridgeMode() )
+                {
+                    // cancel old one if it was sent
+                    if ( fOneIsSent )
+                        Gia_Ga2SendCancel( p, pPars->fVerbose );
+                    // send new one 
+                    Gia_Ga2SendAbsracted( p, pPars->fVerbose );
+                    fOneIsSent = 1;
+                }
+            }
+            // if abstraction grew more than a certain percentage, force a restart
+            if ( pPars->nRatioMax == 0 )
+                continue;
+            if ( c > 0 && (f > 20 || Vec_IntSize(p->vAbs) > 100) && Vec_IntSize(p->vAbs) - nAbsOld >= nAbsOld * pPars->nRatioMax / 100 )
+            {
+                if ( p->pPars->fVerbose )
+                Abc_Print( 1, "Forcing restart because abstraction grew from %d to %d (more than %d %%).\n", 
+                    nAbsOld, Vec_IntSize(p->vAbs), pPars->nRatioMax );
+                break;
+            }
+        }
+    }
+finish:
+    Prf_ManStopP( &p->pSat->pPrf2 );
+    // cancel old one if it is proving
+    if ( iFrameTryToProve >= 0 )
+        Gia_Ga2ProveCancel( pPars->fVerbose );
+    // analize the results
+    if ( RetValue == 1 )
+        Abc_Print( 1, "GLA completed %d frames and proved abstraction derived in frame %d.  ", p->pPars->iFrameProved+1, iFrameTryToProve );
+    else if ( pAig->pCexSeq == NULL )
+    {
+//        if ( pAig->vGateClasses != NULL )
+//            Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
+        Vec_IntFreeP( &pAig->vGateClasses );
+        pAig->vGateClasses = Ga2_ManAbsTranslate( p );
+        if ( Status == l_Undef )
+        {
+            if ( p->pPars->fVerbose )
+                Abc_Print( 1, "\n" );
+            if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit ) 
+                Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction.    ", p->pPars->nTimeOut, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
+            else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
+                Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction.  ", pPars->nConfLimit, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
+            else if ( Vec_IntSize(p->vAbs) >= p->nMarked * (100 - pPars->nRatioMin) / 100 )
+                Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d.  ", pPars->nRatioMin, p->pPars->iFrameProved+1 );
+            else
+                Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d.  ", p->pPars->iFrameProved+1 );
+        }
+        else
+        {
+            p->pPars->iFrame = p->pPars->iFrameProved;
+            Abc_Print( 1, "GLA completed %d frames and produced a %d-stable abstraction.  ", p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
+        }
+    }
+    else
+    {
+        if ( p->pPars->fVerbose )
+            Abc_Print( 1, "\n" );
+        if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
+            Abc_Print( 1, "    Gia_ManPerformGlaOld(): CEX verification has failed!\n" );
+        Abc_Print( 1, "True counter-example detected in frame %d.  ", f );
+        p->pPars->iFrame = f - 1;
+        Vec_IntFreeP( &pAig->vGateClasses );
+        RetValue = 0;
+    }
+    Abc_PrintTime( 1, "Time", clock() - clk );
+    if ( p->pPars->fVerbose )
+    {
+        p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit;
+        ABC_PRTP( "Runtime: Initializing", p->timeInit,   clock() - clk );
+        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 );
+        Ga2_ManReportMemory( p );
+    }
+//    Ga2_ManDumpStats( p->pGia, p->pPars, p->pSat, p->pPars->iFrameProved, 0 );
+    Ga2_ManStop( p );
+    fflush( stdout );
+    return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+