Integrated new proof-logging into proof-based gate-level abstraction.

9 files changed, 766 insertions, 246 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index a79e12dd..c652f1a0 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -606,7 +606,7 @@ int                        Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Ce
 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 fNaiveCnf );
-extern int                 Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars );
+extern int                 Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver );
 /*=== 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 165bc996..e9861977 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -424,9 +424,10 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars )
+int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver )
 {
     extern Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose );
+    extern Vec_Int_t * Aig_Gla3ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose );
     Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
     Vec_Int_t * vGateClasses;
     Gia_Man_t * pGiaAbs;
@@ -447,7 +448,10 @@ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars )
     }
 
     // perform abstraction
-    vGateClasses = Aig_Gla2ManPerform( pAig, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fSkipRand, p->fVerbose );
+    if ( fNewSolver )
+        vGateClasses = Aig_Gla3ManPerform( pAig, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fSkipRand, p->fVerbose );
+    else
+        vGateClasses = Aig_Gla2ManPerform( pAig, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fSkipRand, p->fVerbose );
     Aig_ManStop( pAig );
 
     // update the BMC depth
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index df6fd7cb..cbd25a18 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -13,6 +13,7 @@ SRC +=    src/aig/saig/saigAbs.c \
     src/aig/saig/saigDup.c \
     src/aig/saig/saigGlaCba.c \
     src/aig/saig/saigGlaPba.c \
+    src/aig/saig/saigGlaPba2.c \
     src/aig/saig/saigHaig.c \
     src/aig/saig/saigInd.c \
     src/aig/saig/saigIoa.c \
diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c
index 5834db76..cdbc05c7 100644
--- a/src/aig/saig/saigGlaPba.c
+++ b/src/aig/saig/saigGlaPba.c
@@ -432,11 +432,10 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo
     Vec_Int_t * vCore;
     void * pSatCnf; 
     Intp_Man_t * pManProof;
-    int RetValue;
+    int RetValue, clk = clock();
     if ( piRetValue )
         *piRetValue = -1;
     // solve the problem
-    Abc_Clock(2,1);
     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 )
     {
@@ -453,19 +452,19 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo
     if ( fVerbose )
     {
         printf( "SAT solver returned UNSAT after %7d conflicts.      ", pSat->stats.conflicts );
-        ABC_PRT( "Time", (Abc_Clock(2,0)/ABC_CPS)*CLOCKS_PER_SEC );
+        Abc_PrintTime( 1, "Time", clock() - clk );
     }
     assert( RetValue == l_False );
     pSatCnf = sat_solver_store_release( pSat ); 
     // derive the UNSAT core
-    Abc_Clock(2,1);
+    clk = clock();
     pManProof = Intp_ManAlloc();
     vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0 );
     Intp_ManFree( pManProof );
     if ( fVerbose )
     {
-        printf( "SAT core contains %8d clauses (out of %8d).   ", Vec_IntSize(vCore), ((Sto_Man_t *)pSatCnf)->nRoots );
-        ABC_PRT( "Time", (Abc_Clock(2,0)/ABC_CPS)*CLOCKS_PER_SEC );
+        printf( "SAT core contains %8d clauses (out of %8d).   ", Vec_IntSize(vCore), sat_solver_nclauses(pSat) );
+        Abc_PrintTime( 1, "Time", clock() - clk );
     }
     Sto_ManFree( (Sto_Man_t *)pSatCnf );
     return vCore;
@@ -561,7 +560,6 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
     int clk, clk2 = clock();
     assert( Saig_ManPoNum(pAig) == 1 );
 
-    Abc_Clock(0,1); 
     if ( fVerbose )
     {
         if ( TimeLimit )
@@ -572,7 +570,6 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
 
     // start the solver
     clk = clock();
-    Abc_Clock(1,1); 
     p = Aig_Gla2ManStart( pAig, nStart, nFramesMax, fVerbose );
     if ( !Aig_Gla2CreateSatSolver( p ) )
     {
@@ -581,7 +578,6 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
         return NULL;
     }
     sat_solver_set_random( p->pSat, fSkipRand );
-//    p->timePre += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC;
     p->timePre += clock() - clk;
 
     // set runtime limit
@@ -590,15 +586,12 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
 
     // compute UNSAT core
     clk = clock();
-    Abc_Clock(1,1); 
     vCore = Saig_AbsSolverUnsatCore( p->pSat, nConfLimit, fVerbose, NULL );
     if ( vCore == NULL )
     {
         Aig_Gla2ManStop( p );
         return NULL;
     }
-//    p->timeSat += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC;
-//    p->timeTotal = (Abc_Clock(0,0)/ABC_CPS)*CLOCKS_PER_SEC;
     p->timeSat += clock() - clk;
     p->timeTotal += clock() - clk2;
 
diff --git a/src/aig/saig/saigGlaPba2.c b/src/aig/saig/saigGlaPba2.c
new file mode 100644
index 00000000..8de5fb32
--- /dev/null
+++ b/src/aig/saig/saigGlaPba2.c
@@ -0,0 +1,558 @@
+/**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 "satSolver2.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Aig_Gla3Man_t_ Aig_Gla3Man_t;
+struct Aig_Gla3Man_t_
+{
+    // user data
+    Aig_Man_t *    pAig;
+    int            nStart;
+    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
+    // clause mapping
+    Vec_Int_t *    vCla2Obj;   // maps clause into its root object
+    Vec_Int_t *    vCla2Fra;   // maps clause into its frame
+    Vec_Int_t *    vVec2Use;   // maps vec ID into its used frames (nFrames per vec ID)
+    // SAT solver
+    sat_solver2 *  pSat;
+    // statistics
+    int            timePre;
+    int            timeSat;
+    int            timeTotal;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+#define ABC_CPS 1000
+
+/**Function*************************************************************
+
+  Synopsis    [Adds constant to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Aig_Gla3AddConst( sat_solver2 * pSat, int iVar, int fCompl )
+{
+    lit Lit = toLitCond( iVar, fCompl );
+    if ( !sat_solver2_addclause( pSat, &Lit, &Lit + 1 ) )
+        return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds buffer to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Aig_Gla3AddBuffer( sat_solver2 * pSat, int iVar0, int iVar1, int fCompl )
+{
+    lit Lits[2];
+
+    Lits[0] = toLitCond( iVar0, 0 );
+    Lits[1] = toLitCond( iVar1, !fCompl );
+    if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) )
+        return 0;
+
+    Lits[0] = toLitCond( iVar0, 1 );
+    Lits[1] = toLitCond( iVar1, fCompl );
+    if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) )
+        return 0;
+
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds buffer to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Aig_Gla3AddNode( sat_solver2 * 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_solver2_addclause( pSat, Lits, Lits + 2 ) )
+        return 0;
+
+    Lits[0] = toLitCond( iVar, 1 );
+    Lits[1] = toLitCond( iVar1, fCompl1 );
+    if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) )
+        return 0;
+
+    Lits[0] = toLitCond( iVar, 0 );
+    Lits[1] = toLitCond( iVar0, !fCompl0 );
+    Lits[2] = toLitCond( iVar1, !fCompl1 );
+    if ( !sat_solver2_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_Gla3FetchVar( Aig_Gla3Man_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_Gla3AssignVars_rec( Aig_Gla3Man_t * p, Aig_Obj_t * pObj, int f )
+{
+    int nVars = Vec_IntSize(p->vVar2Inf);
+    Aig_Gla3FetchVar( p, pObj, f );
+    if ( nVars == Vec_IntSize(p->vVar2Inf) )
+        return;
+    if ( Aig_ObjIsConst1(pObj) )
+        return;
+    if ( Saig_ObjIsPo( p->pAig, pObj ) )
+    {
+        Aig_Gla3AssignVars_rec( p, Aig_ObjFanin0(pObj), f );
+        return;
+    }
+    if ( Aig_ObjIsPi( pObj ) )
+    {
+        if ( Saig_ObjIsLo(p->pAig, pObj) && f > 0 )
+            Aig_Gla3AssignVars_rec( p, Aig_ObjFanin0( Saig_ObjLoToLi(p->pAig, pObj) ), f-1 );
+        return;
+    }
+    assert( Aig_ObjIsNode(pObj) );
+    Aig_Gla3AssignVars_rec( p, Aig_ObjFanin0(pObj), f );
+    Aig_Gla3AssignVars_rec( p, Aig_ObjFanin1(pObj), f );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_Gla3CreateSatSolver( Aig_Gla3Man_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-- )
+        Aig_Gla3AssignVars_rec( p, Aig_ManPo(p->pAig, 0), f );
+
+    // create SAT solver
+    p->pSat = sat_solver2_new();
+    sat_solver2_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) )
+        {
+            Aig_Gla3AddNode( p->pSat, Aig_Gla3FetchVar(p, pObj, f), 
+                                      Aig_Gla3FetchVar(p, Aig_ObjFanin0(pObj), f), 
+                                      Aig_Gla3FetchVar(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 );
+
+            Vec_IntPush( p->vCla2Fra, f );
+            Vec_IntPush( p->vCla2Fra, f );
+            Vec_IntPush( p->vCla2Fra, f );
+        }
+        else if ( Saig_ObjIsLo(p->pAig, pObj) )
+        {
+            if ( f == 0 )
+            {
+                Aig_Gla3AddConst( p->pSat, Aig_Gla3FetchVar(p, pObj, f), 1 );
+                Vec_IntPush( p->vCla2Obj, ObjId );
+
+                Vec_IntPush( p->vCla2Fra, f );
+            }
+            else
+            {
+                Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
+                Aig_Gla3AddBuffer( p->pSat, Aig_Gla3FetchVar(p, pObj, f), 
+                                            Aig_Gla3FetchVar(p, Aig_ObjFanin0(pObjLi), f-1), 
+                                            Aig_ObjFaninC0(pObjLi) );
+                Vec_IntPush( p->vCla2Obj, ObjId );
+                Vec_IntPush( p->vCla2Obj, ObjId );
+
+                Vec_IntPush( p->vCla2Fra, f );
+                Vec_IntPush( p->vCla2Fra, f );
+            }
+        }
+        else if ( Saig_ObjIsPo(p->pAig, pObj) )
+        {
+            Aig_Gla3AddBuffer( p->pSat, Aig_Gla3FetchVar(p, pObj, f), 
+                                        Aig_Gla3FetchVar(p, Aig_ObjFanin0(pObj), f), 
+                                        Aig_ObjFaninC0(pObj) );
+            Vec_IntPush( p->vCla2Obj, ObjId );
+            Vec_IntPush( p->vCla2Obj, ObjId );
+
+            Vec_IntPush( p->vCla2Fra, f );
+            Vec_IntPush( p->vCla2Fra, f );
+        }
+        else if ( Aig_ObjIsConst1(pObj) )
+        {
+            Aig_Gla3AddConst( p->pSat, Aig_Gla3FetchVar(p, pObj, f), 0 );
+            Vec_IntPush( p->vCla2Obj, ObjId );
+
+            Vec_IntPush( p->vCla2Fra, f );
+        }
+        else assert( Saig_ObjIsPi(p->pAig, pObj) );
+    }
+
+    // add output clause
+    vPoLits = Vec_IntAlloc( p->nFramesMax );
+    for ( f = p->nStart; f < p->nFramesMax; f++ )
+        Vec_IntPush( vPoLits, 2 * Aig_Gla3FetchVar(p, Aig_ManPo(p->pAig, 0), f) );
+    sat_solver2_addclause( p->pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) );
+    Vec_IntFree( vPoLits );
+    Vec_IntPush( p->vCla2Obj, 0 );
+    Vec_IntPush( p->vCla2Fra, 0 );
+    assert( Vec_IntSize(p->vCla2Fra) == Vec_IntSize(p->vCla2Obj) );
+    assert( nVars == Vec_IntSize(p->vVar2Inf) );
+    assert( Vec_IntSize(p->vCla2Obj) == (int)p->pSat->stats.clauses );
+    if ( p->fVerbose )
+        printf( "The resulting SAT problem contains %d variables and %d clauses.\n", 
+            p->pSat->size, p->pSat->stats.clauses );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Gla3Man_t * Aig_Gla3ManStart( Aig_Man_t * pAig, int nStart, int nFramesMax, int fVerbose )
+{
+    Aig_Gla3Man_t * p;
+    int i;
+
+    p = ABC_CALLOC( Aig_Gla3Man_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 );
+    p->vCla2Fra   = Vec_IntAlloc( 1 << 20 );
+
+    // skip first vector ID
+    p->nStart     = nStart;
+    p->nFramesMax = nFramesMax;
+    p->fVerbose   = fVerbose;
+    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_Gla3ManStop( Aig_Gla3Man_t * p )
+{
+    Vec_IntFreeP( &p->vObj2Vec );
+    Vec_IntFreeP( &p->vVec2Var );
+    Vec_IntFreeP( &p->vVar2Inf );
+    Vec_IntFreeP( &p->vCla2Obj );
+    Vec_IntFreeP( &p->vCla2Fra );
+    Vec_IntFreeP( &p->vVec2Use );
+
+    if ( p->pSat )
+        sat_solver2_delete( p->pSat );
+    ABC_FREE( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Finds the set of clauses involved in the UNSAT core.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Aig_Gla3ManUnsatCore( sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue )
+{
+    Vec_Int_t * vCore;
+    int RetValue, clk = clock();
+    if ( piRetValue )
+        *piRetValue = -1;
+    // solve the problem
+    RetValue = sat_solver2_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 %7d conflicts.      ", pSat->stats.conflicts );
+        Abc_PrintTime( 1, "Time", clock() - clk );
+    }
+    assert( RetValue == l_False );
+
+    // derive the UNSAT core
+    clk = clock();
+    vCore = Sat_ProofCore( pSat );
+    if ( fVerbose )
+    {
+        printf( "SAT core contains %8d clauses (out of %8d).   ", Vec_IntSize(vCore), sat_solver2_nclauses(pSat) );
+        Abc_PrintTime( 1, "Time", clock() - clk );
+    }
+    return vCore;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects abstracted objects.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Aig_Gla3ManCollect( Aig_Gla3Man_t * p, Vec_Int_t * vCore )
+{
+    Vec_Int_t * vResult;
+    Aig_Obj_t * pObj;
+    int i, ClaId, iVecId;
+//    p->vVec2Use = Vec_IntStart( Vec_IntSize(p->vVec2Var) );
+
+    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) || Aig_ObjIsConst1(pObj) )
+            continue;
+        assert( Saig_ObjIsLo(p->pAig, pObj) || Aig_ObjIsNode(pObj) );
+        Vec_IntWriteEntry( vResult, Aig_ObjId(pObj), 1 );
+        if ( p->vVec2Use )
+        {
+            iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
+            Vec_IntWriteEntry( p->vVec2Use, iVecId * p->nFramesMax + Vec_IntEntry(p->vCla2Fra, ClaId), 1 );
+        }
+    }
+    // count the number of objects in each frame
+    if ( p->vVec2Use )
+    {
+        Vec_Int_t * vCounts = Vec_IntStart( p->nFramesMax );
+        int v, f, Entry, nVecIds = Vec_IntSize(p->vVec2Use) / p->nFramesMax;
+        for ( f = 0; f < p->nFramesMax; f++ )
+        for ( v = 0; v < nVecIds; v++ )
+            if ( Vec_IntEntry( p->vVec2Use, v * p->nFramesMax + f ) )
+                Vec_IntAddToEntry( vCounts, f, 1 );
+        Vec_IntForEachEntry( vCounts, Entry, f )
+            printf( "%d ", Entry );
+        printf( "\n" );
+        Vec_IntFree( vCounts );
+    }
+    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_Gla3ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose )
+{
+    Aig_Gla3Man_t * p;
+    Vec_Int_t * vCore, * vResult;
+    int nTimeToStop = time(NULL) + TimeLimit;
+    int clk, clk2 = 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_Gla3ManStart( pAig, nStart, nFramesMax, fVerbose );
+    if ( !Aig_Gla3CreateSatSolver( p ) )
+    {
+        printf( "Error!  SAT solver became UNSAT.\n" );
+        Aig_Gla3ManStop( p );
+        return NULL;
+    }
+    sat_solver2_set_random( p->pSat, fSkipRand );
+    p->timePre += clock() - clk;
+
+    // set runtime limit
+    if ( TimeLimit )
+        sat_solver2_set_runtime_limit( p->pSat, nTimeToStop );
+
+    // compute UNSAT core
+    clk = clock();
+    vCore = Aig_Gla3ManUnsatCore( p->pSat, nConfLimit, fVerbose, NULL );
+    if ( vCore == NULL )
+    {
+        Aig_Gla3ManStop( p );
+        return NULL;
+    }
+    p->timeSat += clock() - clk;
+    p->timeTotal += clock() - clk2;
+
+    // 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_Gla3ManCollect( p, vCore );
+    Vec_IntFree( vCore );
+    Aig_Gla3ManStop( 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 daf92b1b..2050d985 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -29093,13 +29093,14 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Saig_ParBmc_t Pars, * pPars = &Pars;
     int c;
+    int fNewSolver = 0;
     Saig_ParBmcSetDefaultParams( pPars );
     pPars->nStart     =  0;  
     pPars->nFramesMax = (pAbc->nFrames >= 0) ? pAbc->nFrames : 10;
     pPars->nConfLimit =  0;
     pPars->fSkipRand  =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTrvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTrnvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -29150,6 +29151,9 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'r':
             pPars->fSkipRand ^= 1;
             break;
+        case 'n':
+            fNewSolver ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -29186,20 +29190,21 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pPars->nStart )
         Abc_Print( 0, "The starting frame is specified. The resulting abstraction may be unsound.\n" );
-    pAbc->Status = Gia_ManGlaPbaPerform( pAbc->pGia, pPars );
+    pAbc->Status = Gia_ManGlaPbaPerform( pAbc->pGia, pPars, fNewSolver );
 //    if ( pPars->nStart == 0 )
        pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &gla_pba [-SFCT num] [-rvh]\n" );
+    Abc_Print( -2, "usage: &gla_pba [-SFCT num] [-rnvh]\n" );
     Abc_Print( -2, "\t         refines abstracted object map with proof-based abstraction\n" );
     Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [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 (0=unused) [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-r     : toggle using random decisiont during SAT solving [default = %s]\n", !pPars->fSkipRand? "yes": "no" );
+    Abc_Print( -2, "\t-n     : toggle using on-the-fly proof-logging [default = %s]\n", fNewSolver? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index f817ab3d..d51df229 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -66,7 +66,7 @@ static inline void Rec_IntPush( Rec_Int_t * p, int Entry )
 {
     if ( (p->nSize >> p->nShift) == Vec_PtrSize(p->vPages) )
         Vec_PtrPush( p->vPages, ABC_ALLOC(int, p->Mask+1) );
-    ((int*)p->vPages->pArray[p->nSize >> p->nShift])[p->nSize++ & p->Mask] = Entry;
+    ((int*)Vec_PtrEntry(p->vPages, p->nSize >> p->nShift))[p->nSize++ & p->Mask] = Entry;
 }
 static inline void Rec_IntAppend( Rec_Int_t * p, int * pArray, int nSize )
 {
@@ -79,7 +79,7 @@ static inline void Rec_IntAppend( Rec_Int_t * p, int * pArray, int nSize )
     if ( (p->nSize >> p->nShift) == Vec_PtrSize(p->vPages) )
         Vec_PtrPush( p->vPages, ABC_ALLOC(int, p->Mask+1) );
 //    assert( (p->nSize >> p->nShift) + 1 == Vec_PtrSize(p->vPages) );
-    memmove( (int*)p->vPages->pArray[p->nSize >> p->nShift] + (p->nSize & p->Mask), pArray, sizeof(int) * nSize );
+    memmove( (int*)Vec_PtrEntry(p->vPages, p->nSize >> p->nShift) + (p->nSize & p->Mask), pArray, sizeof(int) * nSize );
     p->nLast = p->nSize;
     p->nSize += nSize;
 }
@@ -357,149 +357,6 @@ Vec_Int_t * Proof_CollectUsedRec( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hR
 
 
 
-
-/**Function*************************************************************
-
-  Synopsis    [Collects nodes belonging to the UNSAT core.]
-
-  Description [The result is the array of root clause indexes.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vUsed )
-{
-    Vec_Int_t * vCore;
-    satset * pNode, * pFanin;
-    int i, k, clk = clock();
-    vCore = Vec_IntAlloc( 1000 );
-    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
-    {
-        pNode->Id = 0;
-        Proof_NodeForeachLeaf( vClauses, pNode, pFanin, k )
-            if ( pFanin && !pFanin->mark )
-            {
-                pFanin->mark = 1;
-                Vec_IntPush( vCore, Proof_NodeHandle(vClauses, pFanin) );
-            }
-    }
-    // clean core clauses
-    Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
-        pNode->mark = 0;
-    return vCore;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Computes UNSAT core.]
-
-  Description [The result is the array of root clause indexes.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Sat_ProofCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hNode )
-{
-    Vec_Int_t * vCore, * vUsed;
-    // collect visited clauses
-    vUsed = Proof_CollectUsedIter( vProof, NULL, hNode );
-    // collect core clauses 
-    vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed );
-    Vec_IntFree( vUsed );
-    return vCore;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes interpolant of the proof.]
-
-  Description [Aassuming that vars/clause of partA are marked.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hNode, Vec_Int_t * vGlobVars )
-{
-    Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap;
-    satset * pNode, * pFanin;
-    Aig_Man_t * pAig;
-    Aig_Obj_t * pObj;
-    int i, k, iVar, Entry;
-
-    // collect visited nodes
-    vUsed = Proof_CollectUsedIter( vProof, NULL, hNode );
-    // collect core clauses (cleans vUsed and vCore)
-    vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed );
-
-    // map variables into their global numbers
-    vVarMap = Vec_IntStartFull( Vec_IntFindMax(vGlobVars) + 1 );
-    Vec_IntForEachEntry( vGlobVars, Entry, i )
-        Vec_IntWriteEntry( vVarMap, Entry, i );
-
-    // start the AIG
-    pAig = Aig_ManStart( 10000 );
-    pAig->pName = Aig_UtilStrsav( "interpol" );
-    for ( i = 0; i < Vec_IntSize(vGlobVars); i++ )
-        Aig_ObjCreatePi( pAig );
-
-    // copy the numbers out and derive interpol for clause
-    vCoreNums = Vec_IntAlloc( Vec_IntSize(vCore) );
-    Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
-    {
-        if ( pNode->partA )
-        {
-            pObj = Aig_ManConst0( pAig );
-            satset_foreach_var( pNode, iVar, k, 0 )
-                if ( iVar < Vec_IntSize(vVarMap) && Vec_IntEntry(vVarMap, iVar) >= 0 )
-                    pObj = Aig_Or( pAig, pObj, Aig_IthVar(pAig, iVar) );
-        }
-        else
-            pObj = Aig_ManConst1( pAig );
-        // remember the interpolant
-        Vec_IntPush( vCoreNums, pNode->Id );
-        pNode->Id = Aig_ObjToLit(pObj);
-    }
-    Vec_IntFree( vVarMap );
-
-    // copy the numbers out and derive interpol for resolvents
-    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
-    {
-        assert( pNode->nEnts > 1 );
-        Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k )
-        {
-            if ( k == 0 )
-                pObj = Aig_ObjFromLit( pAig, pFanin->Id );
-            else if ( pNode->pEnts[k] & 2 ) // variable of A
-                pObj = Aig_Or( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) );
-            else
-                pObj = Aig_And( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) );
-        }
-        // remember the interpolant
-        pNode->Id = Aig_ObjToLit(pObj);
-    }
-    // save the result
-    assert( Proof_NodeHandle(vProof, pNode) == hNode );
-    Aig_ObjCreatePo( pAig, pObj );
-    Aig_ManCleanup( pAig );
-
-    // move the results back
-    Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
-        pNode->Id = Vec_IntEntry( vCoreNums, i );
-    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
-        pNode->Id = 0;
-    // cleanup
-    Vec_IntFree( vCore );
-    Vec_IntFree( vUsed );
-    Vec_IntFree( vCoreNums );
-    return pAig;
-}
  
 /**Function*************************************************************
 
@@ -512,11 +369,12 @@ Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int
   SeeAlso     []
 
 ***********************************************************************/
-void Sat_ProofReduce( veci * pProof, veci * pRoots )
+void Sat_ProofReduce( sat_solver2 * s )
 {
+    Vec_Int_t * vProof   = (Vec_Int_t *)&s->proofs;
+    Vec_Int_t * vRoots   = (Vec_Int_t *)&s->claProofs;
+
     int fVerbose = 0;
-    Vec_Int_t * vProof = (Vec_Int_t *)pProof;
-    Vec_Int_t * vRoots = (Vec_Int_t *)pRoots;
     Vec_Int_t * vUsed;
     satset * pNode, * pFanin;
     int i, k, hTemp, hNewHandle = 1, clk = clock();
@@ -575,7 +433,7 @@ void Sat_ProofReduce( veci * pProof, veci * pRoots )
   SeeAlso     []
 
 ***********************************************************************/
-satset * Proof_ResolveOne( Vec_Int_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp )
+satset * Sat_ProofCheckResolveOne( Vec_Int_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp )
 {
     satset * c;
     int i, k, hNode, Var = -1, Count = 0;
@@ -627,7 +485,7 @@ satset * Proof_ResolveOne( Vec_Int_t * p, satset * c1, satset * c2, Vec_Int_t *
   SeeAlso     []
 
 ***********************************************************************/
-satset * Proof_CheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vResolves, int iAnt )
+satset * Sat_ProofCheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vResolves, int iAnt )
 {
     satset * pAnt;
     if ( iAnt & 1 )
@@ -649,14 +507,13 @@ satset * Proof_CheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t
   SeeAlso     []
 
 ***********************************************************************/
-void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot )
+void Sat_ProofCheck( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot )
 {
     Vec_Int_t * vUsed, * vResolves, * vTemp;
     satset * pSet, * pSet0, * pSet1;
     int i, k, Counter = 0, clk = clock(); 
     // collect visited clauses
-    vUsed = Proof_CollectUsedRec( vProof, NULL, hRoot );
-//    vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
+    vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
     Proof_CleanCollected( vProof, vUsed );
     // perform resolution steps
     vTemp = Vec_IntAlloc( 1000 );
@@ -664,11 +521,11 @@ void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot )
     Vec_IntPush( vResolves, -1 );
     Proof_ForeachNodeVec( vUsed, vProof, pSet, i )
     {
-        pSet0 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] );
+        pSet0 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] );
         for ( k = 1; k < (int)pSet->nEnts; k++ )
         {
-            pSet1 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] );
-            pSet0 = Proof_ResolveOne( vResolves, pSet0, pSet1, vTemp );
+            pSet1 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] );
+            pSet0 = Sat_ProofCheckResolveOne( vResolves, pSet0, pSet1, vTemp );
         }
         pSet->Id = Proof_NodeHandle( vResolves, pSet0 );
 //printf( "Clause for proof %d: ", Vec_IntEntry(vUsed, i) );
@@ -703,7 +560,7 @@ void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot )
   SeeAlso     []
 
 ***********************************************************************/
-satset * Proof_ResolveOne( Rec_Int_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp )
+satset * Sat_ProofCheckResolveOne( Rec_Int_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp )
 {
     satset * c;
     int i, k, Var = -1, Count = 0;
@@ -754,7 +611,7 @@ satset * Proof_ResolveOne( Rec_Int_t * p, satset * c1, satset * c2, Vec_Int_t *
   SeeAlso     []
 
 ***********************************************************************/
-satset * Proof_CheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Rec_Int_t * vResolves, int iAnt )
+satset * Sat_ProofCheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Rec_Int_t * vResolves, int iAnt )
 {
     satset * pAnt;
     if ( iAnt & 1 )
@@ -776,14 +633,17 @@ satset * Proof_CheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Rec_Int_t
   SeeAlso     []
 
 ***********************************************************************/
-void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot )
+void Sat_ProofCheck( sat_solver2 * s )
 {
+    Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
+    Vec_Int_t * vProof   = (Vec_Int_t *)&s->proofs;
+    int hRoot = veci_begin(&s->claProofs)[satset_read(&s->clauses, s->hLearntLast)->Id];
+
     Rec_Int_t * vResolves;
     Vec_Int_t * vUsed, * vTemp;
     satset * pSet, * pSet0, * pSet1;
     int i, k, Counter = 0, clk = clock(); 
     // collect visited clauses
-//    vUsed = Proof_CollectUsedRec( vProof, NULL, hRoot );
     vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
     Proof_CleanCollected( vProof, vUsed );
     // perform resolution steps
@@ -792,11 +652,11 @@ void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot )
     Rec_IntPush( vResolves, -1 );
     Proof_ForeachNodeVec( vUsed, vProof, pSet, i )
     {
-        pSet0 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] );
+        pSet0 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] );
         for ( k = 1; k < (int)pSet->nEnts; k++ )
         {
-            pSet1 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] );
-            pSet0 = Proof_ResolveOne( vResolves, pSet0, pSet1, vTemp );
+            pSet1 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] );
+            pSet0 = Sat_ProofCheckResolveOne( vResolves, pSet0, pSet1, vTemp );
         }
         pSet->Id = Rec_IntSizeLast( vResolves );
 //printf( "Clause for proof %d: ", Vec_IntEntry(vUsed, i) );
@@ -818,52 +678,162 @@ void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot )
     Vec_IntFree( vUsed );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Collects nodes belonging to the UNSAT core.]
+
+  Description [The resulting array contains 0-based IDs of root clauses.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vUsed )
+{
+    Vec_Int_t * vCore;
+    satset * pNode, * pFanin;
+    int i, k, clk = clock();
+    vCore = Vec_IntAlloc( 1000 );
+    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
+    {
+        pNode->Id = 0;
+        Proof_NodeForeachLeaf( vClauses, pNode, pFanin, k )
+            if ( pFanin && !pFanin->mark )
+            {
+                pFanin->mark = 1;
+                Vec_IntPush( vCore, Proof_NodeHandle(vClauses, pFanin) );
+            }
+    }
+    // clean core clauses and reexpress core in terms of clause IDs
+    Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
+    {
+        pNode->mark = 0;
+        Vec_IntWriteEntry( vCore, i, pNode->Id - 1 );
+    }
+    return vCore;
+}
+
 
 /**Function*************************************************************
 
   Synopsis    [Computes interpolant of the proof.]
 
-  Description [Aassuming that global vars and A-clauses are marked.]
+  Description [Aassuming that vars/clause of partA are marked.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pRoots, int hRoot )
+void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
 {
-    Vec_Int_t * vClauses  = (Vec_Int_t *)pClauses;
-    Vec_Int_t * vProof    = (Vec_Int_t *)pProof;
-    Vec_Int_t * vRoots    = (Vec_Int_t *)pRoots;
-//    Vec_Int_t * vUsed, * vCore;
-//    int i, Entry;
-/*
-    // collect visited clauses
-    vUsed = Proof_CollectUsedRec( vProof, NULL, hRoot );
-    Proof_CleanCollected( vProof, vUsed );
-    printf( "Found %d useful resolution nodes.\n", Vec_IntSize(vUsed) );
-    Vec_IntFree( vUsed );
-*/
-/*
-    // collect visited clauses
+    Vec_Int_t * vClauses  = (Vec_Int_t *)&s->clauses;
+    Vec_Int_t * vProof    = (Vec_Int_t *)&s->proofs;
+    Vec_Int_t * vGlobVars = (Vec_Int_t *)pGloVars;
+    int hRoot = veci_begin(&s->claProofs)[satset_read(&s->clauses, s->hLearntLast)->Id];
+
+    Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap;
+    satset * pNode, * pFanin;
+    Aig_Man_t * pAig;
+    Aig_Obj_t * pObj;
+    int i, k, iVar, Entry;
+
+    // collect visited nodes
     vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
-    Proof_CleanCollected( vProof, vUsed );
-    printf( "Found %d useful resolution nodes.\n", Vec_IntSize(vUsed) );
-    Vec_IntFree( vUsed );
+    // collect core clauses (cleans vUsed and vCore)
+    vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed );
+
+    // map variables into their global numbers
+    vVarMap = Vec_IntStartFull( Vec_IntFindMax(vGlobVars) + 1 );
+    Vec_IntForEachEntry( vGlobVars, Entry, i )
+        Vec_IntWriteEntry( vVarMap, Entry, i );
+
+    // start the AIG
+    pAig = Aig_ManStart( 10000 );
+    pAig->pName = Aig_UtilStrsav( "interpol" );
+    for ( i = 0; i < Vec_IntSize(vGlobVars); i++ )
+        Aig_ObjCreatePi( pAig );
+
+    // copy the numbers out and derive interpol for clause
+    vCoreNums = Vec_IntAlloc( Vec_IntSize(vCore) );
+    Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
+    {
+        if ( pNode->partA )
+        {
+            pObj = Aig_ManConst0( pAig );
+            satset_foreach_var( pNode, iVar, k, 0 )
+                if ( iVar < Vec_IntSize(vVarMap) && Vec_IntEntry(vVarMap, iVar) >= 0 )
+                    pObj = Aig_Or( pAig, pObj, Aig_IthVar(pAig, iVar) );
+        }
+        else
+            pObj = Aig_ManConst1( pAig );
+        // remember the interpolant
+        Vec_IntPush( vCoreNums, pNode->Id );
+        pNode->Id = Aig_ObjToLit(pObj);
+    }
+    Vec_IntFree( vVarMap );
 
-    vCore = Sat_ProofCore( vClauses, vProof, hRoot );
+    // copy the numbers out and derive interpol for resolvents
+    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
+    {
+        assert( pNode->nEnts > 1 );
+        Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k )
+        {
+            if ( k == 0 )
+                pObj = Aig_ObjFromLit( pAig, pFanin->Id );
+            else if ( pNode->pEnts[k] & 2 ) // variable of A
+                pObj = Aig_Or( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) );
+            else
+                pObj = Aig_And( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) );
+        }
+        // remember the interpolant
+        pNode->Id = Aig_ObjToLit(pObj);
+    }
+    // save the result
+    assert( Proof_NodeHandle(vProof, pNode) == hRoot );
+    Aig_ObjCreatePo( pAig, pObj );
+    Aig_ManCleanup( pAig );
+
+    // move the results back
+    Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
+        pNode->Id = Vec_IntEntry( vCoreNums, i );
+    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
+        pNode->Id = 0;
+    // cleanup
     Vec_IntFree( vCore );
-*/
-/*
-    printf( "Found %d useful resolution nodes.\n", Vec_IntSize(vUsed) );
     Vec_IntFree( vUsed );
-    vUsed = Proof_CollectAll( vProof );
-    printf( "Found %d total  resolution nodes.\n", Vec_IntSize(vUsed) );
+    Vec_IntFree( vCoreNums );
+    return pAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes UNSAT core.]
+
+  Description [The result is the array of root clause indexes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Sat_ProofCore( sat_solver2 * s )
+{
+    Vec_Int_t * vClauses  = (Vec_Int_t *)&s->clauses;
+    Vec_Int_t * vProof    = (Vec_Int_t *)&s->proofs;
+    int hRoot = veci_begin(&s->claProofs)[satset_read(&s->clauses, s->hLearntLast)->Id];
+
+    Vec_Int_t * vCore, * vUsed;
+    // collect visited clauses
+    vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
+    // collect core clauses 
+    vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed );
     Vec_IntFree( vUsed );
-*/
-    Proof_Check( vClauses, vProof, hRoot );
+    return vCore;
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 8fdc2ecb..fab5e7da 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -28,7 +28,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 ABC_NAMESPACE_IMPL_START
 
-
 #define SAT_USE_ANALYZE_FINAL
 #define SAT_USE_PROOF_LOGGING
 
@@ -369,7 +368,7 @@ static inline void act_clause_decay(sat_solver2* s) { s->cla_inc += (s->cla_inc
 //=================================================================================================
 // Clause functions:
 
-static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id)
+static int clause_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id)
 {
     satset* c;
     int i, Cid, nLits = end - begin;
@@ -516,7 +515,7 @@ static void solver2_record(sat_solver2* s, veci* cls, int proof_id)
 {
     lit* begin = veci_begin(cls);
     lit* end   = begin + veci_size(cls);
-    int  Cid   = clause_new(s,begin,end,1, proof_id);
+    int  Cid   = clause_create_new(s,begin,end,1, proof_id);
     assert(veci_size(cls) > 0);
     if ( veci_size(cls) == 1 )
     {
@@ -888,6 +887,7 @@ satset* solver2_propagate(sat_solver2* s)
     veci* ws;
     lit* lits, false_lit, p, * stop, * k;
     cla* begin,* end, *i, *j;
+    int Lit;
 
     while (confl == 0 && s->qtail - s->qhead > 0){
 
@@ -926,9 +926,10 @@ satset* solver2_propagate(sat_solver2* s)
                 }
 
                 // Did not find watch -- clause is unit under assignment:
+                Lit = lits[0];
                 if (s->fProofLogging && solver2_dlevel(s) == 0){
-                    int k, x, proof_id, Cid, Var = lit_var(lits[0]);
-                    int fLitIsFalse = (var_value(s, Var) == !lit_sign(lits[0])); 
+                    int k, x, proof_id, Cid, Var = lit_var(Lit);
+                    int fLitIsFalse = (var_value(s, Var) == !lit_sign(Lit)); 
                     // Log production of top-level unit clause:
                     proof_chain_start( s, c );
                     satset_foreach_var( c, x, k, 1 ){
@@ -937,7 +938,7 @@ satset* solver2_propagate(sat_solver2* s)
                     }
                     proof_id = proof_chain_stop( s );
                     // get a new clause
-                    Cid = clause_new( s, lits, lits + 1, 1, proof_id );
+                    Cid = clause_create_new( s, &Lit, &Lit + 1, 1, proof_id );
                     assert( (var_unit_clause(s, Var) == NULL) != fLitIsFalse ); 
                     // if variable already has unit clause, it must be with the other polarity 
                     // in this case, we should derive the empty clause here
@@ -948,13 +949,13 @@ satset* solver2_propagate(sat_solver2* s)
                         proof_chain_start( s, clause_read(s,Cid) );
                         proof_chain_resolve( s, NULL, Var );
                         proof_id = proof_chain_stop( s );
-                        clause_new( s, lits, lits, 1, proof_id );
+                        clause_create_new( s, &Lit, &Lit, 1, proof_id );
                     }
                 }
 
                 *j++ = *i;
                 // Clause is unit under assignment:
-                if (!solver2_enqueue(s,lits[0], *i)){
+                if (!solver2_enqueue(s,Lit, *i)){
                     confl = clause_read(s,*i++);
                     // Copy the remaining watches:
                     while (i < end)
@@ -1275,16 +1276,17 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
 
 void sat_solver2_delete(sat_solver2* s)
 {
-    satset * c = clause_read(s, s->hLearntLast);
+//    veci * pCore;
     // report statistics
     printf( "Used %6.2f Mb for proof-logging.   Unit clauses = %d.\n", 2.0 * veci_size(&s->proofs) / (1<<20), s->nUnits );
+/*
+    pCore = Sat_ProofCore( s );
+    printf( "UNSAT core contains %d clauses (%6.2f %%).\n", veci_size(pCore), 100.0*veci_size(pCore)/veci_size(&s->clauses) );
+    veci_delete( pCore );
+    ABC_FREE( pCore );
 
-    Sat_ProofTest( 
-        &s->clauses,      // clauses
-        &s->proofs,   // proof clauses
-        NULL,             // proof roots
-        veci_begin(&s->claProofs)[c->Id]  // one root
-         );  
+*/
+//    Sat_ProofCheck( s );
 
     // delete vectors
     veci_delete(&s->order);
@@ -1308,10 +1310,7 @@ void sat_solver2_delete(sat_solver2* s)
         int i;
         if ( s->wlists )
             for (i = 0; i < s->size*2; i++)
-            {
-//                printf( "%d ", s->wlists[i].size );
                 veci_delete(&s->wlists[i]);
-            }
         ABC_FREE(s->wlists   );
         ABC_FREE(s->vi       );
         ABC_FREE(s->trail    );
@@ -1375,7 +1374,7 @@ int sat_solver2_addclause__(sat_solver2* s, lit* begin, lit* end)
         return solver2_enqueue(s,*begin,0);
 
     // create new clause
-    return clause_new(s,begin,j,0,0);
+    return clause_create_new(s,begin,j,0,0);
 }
 
 int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end)
@@ -1404,21 +1403,17 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end)
     sat_solver2_setnvars(s,maxvar+1);
 
     // create a new clause
-    Cid = clause_new( s, begin, end, 0, 0 );
+    Cid = clause_create_new( s, begin, end, 0, 0 );
     // handle unit clause
     if ( begin + 1 == end )
     {
-        printf( "Adding unit clause %d\n", begin[0] );
+//        printf( "Adding unit clause %d\n", begin[0] );
 //        solver2_canceluntil(s, 0);
         if ( s->fProofLogging )
             var_set_unit_clause( s, lit_var(begin[0]), Cid );
         if ( !solver2_enqueue(s,begin[0],0) )
             assert( 0 );
     }
-
-    // count literals
-    s->stats.clauses++;
-    s->stats.clauses_literals += end - begin;
     return Cid;
 }
 
@@ -1447,7 +1442,6 @@ void luby2_test()
 // updates clauses, watches, units, and proof
 void solver2_reducedb(sat_solver2* s)
 {
-    extern void Sat_ProofReduce( veci * pProof, veci * pRoots );
     satset * c;
     cla h,* pArray,* pArray2;
     int Counter = 0, CounterStart = s->stats.learnts * 3 / 4; // 2/3;
@@ -1504,7 +1498,7 @@ void solver2_reducedb(sat_solver2* s)
     s->stats.learnts = veci_size(&s->learnt_live);
 
     // compact proof (compacts 'proofs' and update 'claProofs')
-    Sat_ProofReduce( &s->proofs, &s->claProofs );
+    Sat_ProofReduce( s );
 
     TimeTotal += clock() - clk;
     Abc_PrintTime( 1, "Time", TimeTotal );
@@ -1658,7 +1652,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
          // reduce the set of learnt clauses:
         if (nof_learnts > 0 && s->stats.learnts > nof_learnts)
         {
-            solver2_reducedb(s);
+//            solver2_reducedb(s);
             nof_learnts = nof_learnts * 11 / 10;
         }
         // perform next run
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index 2e745bc2..137f1968 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -59,14 +59,6 @@ extern void         sat_solver2TraceStart( sat_solver2 * pSat, char * pName );
 extern void         sat_solver2TraceStop( sat_solver2 * pSat );
 extern void         sat_solver2TraceWrite( sat_solver2 * pSat, int * pBeg, int * pEnd, int fRoot );
 
-// clause storage
-extern void         sat_solver2_store_alloc( sat_solver2 * s );
-extern void         sat_solver2_store_write( sat_solver2 * s, char * pFileName );
-extern void         sat_solver2_store_free( sat_solver2 * s );
-extern void         sat_solver2_store_mark_roots( sat_solver2 * s );
-extern void         sat_solver2_store_mark_clauses_a( sat_solver2 * s );
-extern void *       sat_solver2_store_release( sat_solver2 * s ); 
-
 // global variables
 extern int          var_is_partA (sat_solver2* s, int v);
 extern void         var_set_partA(sat_solver2* s, int v, int partA);
@@ -76,6 +68,11 @@ extern void         clause_set_partA(sat_solver2* s, int handle, int partA);
 // other clause functions
 extern int          clause_id(sat_solver2* s, int h);
  
+// proof-based APIs
+extern void *       Sat_ProofCore( sat_solver2 * s );
+extern void *       Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars );
+extern void         Sat_ProofReduce( sat_solver2 * s );
+extern void         Sat_ProofCheck( sat_solver2 * s );
 
 //=================================================================================================
 // Solver representation:
@@ -247,8 +244,6 @@ static inline int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom)
     return fNotUseRandomOld;
 }
 
-extern void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pRoots, int hRoot );
-
 ABC_NAMESPACE_HEADER_END
 
 #endif