Adding command to dump UNSAT core of BMC instance.

11 files changed, 497 insertions, 20 deletions

diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c
index 14f47c5c..d26bbe89 100644
--- a/src/aig/saig/saigGlaPba.c
+++ b/src/aig/saig/saigGlaPba.c
@@ -429,7 +429,7 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo
     // derive the UNSAT core
     clk = clock();
     pManProof = Intp_ManAlloc();
-    vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0 );
+    vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0, 0 );
     Intp_ManFree( pManProof );
     if ( fVerbose )
     {
diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c
index ff3e45df..a1bebd64 100644
--- a/src/aig/saig/saigRetMin.c
+++ b/src/aig/saig/saigRetMin.c
@@ -128,7 +128,7 @@ int Saig_ManRetimeUnsatCore( Aig_Man_t * p, int fVerbose )
     sat_solver_delete( pSat );
     // derive the UNSAT core
     pManProof = Intp_ManAlloc();
-    vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, fVeryVerbose );
+    vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0, fVeryVerbose );
     Intp_ManFree( pManProof );
     Sto_ManFree( (Sto_Man_t *)pSatCnf );
     // derive the set of variables on which the core depends
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 397cee76..3810fdaf 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -397,6 +397,7 @@ static int Abc_CommandAbc9PoPart             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9GroupProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9MultiProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Bmc                ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9BCore              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9ICheck             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SatTest            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9FFTest             ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -965,6 +966,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&gprove",       Abc_CommandAbc9GroupProve,   0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&mprove",       Abc_CommandAbc9MultiProve,   0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&bmc",          Abc_CommandAbc9Bmc,          0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&bcore",        Abc_CommandAbc9BCore,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&icheck",       Abc_CommandAbc9ICheck,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&sattest",      Abc_CommandAbc9SatTest,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&fftest",       Abc_CommandAbc9FFTest,       0 );
@@ -32745,6 +32747,135 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9BCore( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c;
+    Bmc_BCorePar_t Pars, * pPars = &Pars;
+    memset( pPars, 0, sizeof(Bmc_BCorePar_t) );
+    pPars->iFrame        =   10;  // timeframe
+    pPars->iOutput       =    0;  // property output
+    pPars->nTimeOut      =    0;  // timeout in seconds
+    pPars->pFilePivots   = NULL;  // file name with AIG IDs of pivot objects
+    pPars->pFileProof    = NULL;  // file name to write the resulting proof
+    pPars->fVerbose      =    0;  // verbose output
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FOTVvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->iFrame = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->iFrame < 0 )
+                goto usage;
+            break;
+        case 'O':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->iOutput = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->iOutput < 0 )
+                goto usage;
+            break;
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nTimeOut = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nTimeOut < 0 )
+                goto usage;
+            break;
+        case 'V':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-V\" should be followed by a file name.\n" );
+                goto usage;
+            }
+            pPars->pFilePivots = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9BCore(): There is no AIG.\n" );
+        return 0;
+    }
+    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9BCore(): AIG has no registers.\n" );
+        return 0;
+    }
+    // get the file name
+    if ( pPars->pFilePivots != NULL )
+    {
+        FILE * pFile;
+        pFile = fopen( pPars->pFilePivots, "r" );
+        if ( pFile == NULL )
+        {
+            Abc_Print( -1, "Abc_CommandAbc9BCore(): Cannot open file \"%s\" with pivot node IDs.\n", pPars->pFilePivots );
+            return 0;
+        }
+        fclose( pFile );
+    }
+    // get the file name
+    if ( argc == globalUtilOptind + 1 )
+    {
+        FILE * pFile;
+        pPars->pFileProof = argv[globalUtilOptind];
+        pFile = fopen( pPars->pFileProof, "wb" );
+        if ( pFile == NULL )
+        {
+            Abc_Print( -1, "Abc_CommandAbc9BCore(): Cannot open file \"%s\" for writing the proof.\n", pPars->pFileProof );
+            return 0;
+        }
+        fclose( pFile );
+    }
+    Bmc_ManBCorePerform( pAbc->pGia, pPars );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &bcore [-FOTV num] [-vh] <file>\n" );
+    Abc_Print( -2, "\t         records UNSAT core of the BMC instance\n" );
+    Abc_Print( -2, "\t-F num : the zero-based index of a timeframe [default = %d]\n",         pPars->iFrame );
+    Abc_Print( -2, "\t-O num : the zero-based index of a primary output [default = %d]\n",    pPars->iOutput );
+    Abc_Print( -2, "\t-T num : approximate timeout in seconds [default = %d]\n",              pPars->nTimeOut );
+    Abc_Print( -2, "\t-V file: file name with AIG IDs of pivot variables [default = no pivots]\n" );
+    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");
+    Abc_Print( -2, "\t<file> : file name to write the resulting proof [default = stdout]\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     int c, nFramesMax = 1, nTimeOut = 0, fEmpty = 0, fSearch = 1, fReverse = 0, fDump = 0, fVerbose = 0;
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 3eeeb7b5..558b2d62 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -94,7 +94,18 @@ struct Bmc_AndPar_t_
     int         nFailOuts;      // the number of failed outputs
     int         nDropOuts;      // the number of dropped outputs
 };
- 
+  
+typedef struct Bmc_BCorePar_t_ Bmc_BCorePar_t;
+struct Bmc_BCorePar_t_
+{
+    int         iFrame;         // timeframe
+    int         iOutput;        // property output
+    int         nTimeOut;       // timeout in seconds
+    char *      pFilePivots;    // file name with AIG IDs of pivot objects
+    char *      pFileProof;     // file name to write the resulting proof
+    int         fVerbose;       // verbose output
+};
+
 typedef struct Bmc_MulPar_t_ Bmc_MulPar_t;
 struct Bmc_MulPar_t_
 {
@@ -117,6 +128,8 @@ struct Bmc_MulPar_t_
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== bmcBCore.c ==========================================================*/
+extern void              Bmc_ManBCorePerform( Gia_Man_t * pGia, Bmc_BCorePar_t * pPars );
 /*=== bmcBmc.c ==========================================================*/
 extern int               Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit );
 /*=== bmcBmc2.c ==========================================================*/
diff --git a/src/sat/bmc/bmcBCore.c b/src/sat/bmc/bmcBCore.c
new file mode 100644
index 00000000..cde49f52
--- /dev/null
+++ b/src/sat/bmc/bmcBCore.c
@@ -0,0 +1,272 @@
+/**CFile****************************************************************
+
+  FileName    [bmcBCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based bounded model checking.]
+
+  Synopsis    [Performs recording of BMC core.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bmcBCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bmc.h"
+#include "sat/bsat/satSolver.h"
+#include "sat/bsat/satStore.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Collect pivot variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Bmc_ManBCoreReadPivots( char * pName )
+{
+    int Num;
+    Vec_Int_t * vPivots = Vec_IntAlloc( 100 );
+    FILE * pFile = fopen( pName, "r" );
+    while ( fscanf( pFile, "%d", &Num ) == 1 )
+        Vec_IntPush( vPivots, Num );
+    fclose( pFile );
+    return vPivots;
+}
+Vec_Int_t * Bmc_ManBCoreCollectPivots( Gia_Man_t * p, char * pName, Vec_Int_t * vVarMap )
+{
+    Gia_Obj_t * pObj;
+    int i, iVar, iFrame;
+    Vec_Int_t * vPivots = Vec_IntAlloc( 100 );
+    Vec_Int_t * vVars = Bmc_ManBCoreReadPivots( pName );
+    Gia_ManForEachObj( p, pObj, i )
+        pObj->fMark0 = 0;
+    Vec_IntForEachEntry( vVars, iVar, i )
+        if ( iVar > 0 && iVar < Gia_ManObjNum(p) )
+            Gia_ManObj( p, iVar )->fMark0 = 1;
+        else
+            printf( "Cannot find object with Id %d in the given AIG.\n", iVar );
+    Vec_IntForEachEntryDouble( vVarMap, iVar, iFrame, i )
+        if ( Gia_ManObj( p, iVar )->fMark0 )
+            Vec_IntPush( vPivots, Abc_Lit2Var(i) );
+    Gia_ManForEachObj( p, pObj, i )
+        pObj->fMark0 = 0;
+    Vec_IntFree( vVars );
+    return vPivots;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect (Id; Frame) pairs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Bmc_ManBCoreAssignVar( Gia_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vNodes )
+{
+    pObj->Value = Abc_Lit2Var(Vec_IntSize(vNodes));
+    Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
+    Vec_IntPush( vNodes, f );
+//    printf( "Obj %3d  Frame %3d  --->  Var %3d    ", Gia_ObjId(p, pObj), f, pObj->Value );
+//    Gia_ObjPrint( p, pObj );
+}
+void Bmc_ManBCoreCollect_rec( Gia_Man_t * p, int Id, int f, Vec_Int_t * vNodes, Vec_Int_t * vRootsNew )
+{
+    Gia_Obj_t * pObj;
+    if ( Gia_ObjIsTravIdCurrentId(p, Id) )
+        return;
+    Gia_ObjSetTravIdCurrentId(p, Id);
+    pObj = Gia_ManObj( p, Id );
+    Bmc_ManBCoreAssignVar( p, pObj, f, vNodes );
+    if ( Gia_ObjIsPi(p, pObj) )
+        return;
+    if ( Gia_ObjIsRo(p, pObj) )
+    {
+        Vec_IntPush( vRootsNew, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Bmc_ManBCoreCollect_rec( p, Gia_ObjFaninId0p(p, pObj), f, vNodes, vRootsNew );
+    Bmc_ManBCoreCollect_rec( p, Gia_ObjFaninId1p(p, pObj), f, vNodes, vRootsNew );
+}
+Vec_Int_t * Bmc_ManBCoreCollect( Gia_Man_t * p, int iFrame, int iOut, sat_solver * pSat )
+{
+    Gia_Obj_t * pObj; 
+    int f, i, iObj, nNodesOld;
+    Vec_Int_t * vNodes  = Vec_IntAlloc( 100 );
+    Vec_Int_t * vRoots  = Vec_IntAlloc( 100 );
+    Vec_Int_t * vRoots2 = Vec_IntAlloc( 100 );
+    assert( iFrame >= 0 && iOut >= 0 );
+    // add first variables
+    Vec_IntPush( vNodes, -1 );
+    Vec_IntPush( vNodes, -1 );
+    Bmc_ManBCoreAssignVar( p, Gia_ManPo(p, iOut), iFrame, vNodes );
+    // start with root node
+    Vec_IntPush( vRoots, Gia_ObjId(p, Gia_ManPo(p, iOut)) );
+    // iterate through time frames
+    for ( f = iFrame; f >= 0; f-- )
+    {
+        Gia_ManIncrementTravId( p );
+        // add constant node
+        Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
+        Bmc_ManBCoreAssignVar( p, Gia_ManConst0(p), f, vNodes );
+        sat_solver_add_const( pSat, Gia_ManConst0(p)->Value, 1 );
+        // collect nodes in this timeframe
+        Vec_IntClear( vRoots2 );
+        nNodesOld = Vec_IntSize(vNodes);
+        Gia_ManForEachObjVec( vRoots, p, pObj, i )
+            Bmc_ManBCoreCollect_rec( p, Gia_ObjFaninId0p(p, pObj), f, vNodes, vRoots2 );
+        if ( f == iFrame )
+        {
+            // add the final clause
+            pObj = Gia_ManPo(p, iOut);
+            assert( pObj->Value == 1 );
+            assert( Gia_ObjFanin0(pObj)->Value == 3 );
+//            sat_solver_add_const( pSat, Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );
+            sat_solver_add_constraint( pSat, Gia_ObjFanin0(pObj)->Value, pObj->Value, Gia_ObjFaninC0(pObj) );
+        }
+        else
+        {
+            // connect current RIs to previous ROs
+            Gia_ManForEachObjVec( vRoots, p, pObj, i )
+                sat_solver_add_buffer( pSat, pObj->Value, Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );
+        }
+        Gia_ManForEachObjVec( vRoots2, p, pObj, i )
+            pObj->Value = Gia_ObjRiToRo(p, pObj)->Value;
+        // add nodes of this timeframe
+        Vec_IntForEachEntryStart( vNodes, iObj, i, nNodesOld )
+        {
+            pObj = Gia_ManObj(p, iObj); i++;
+            if ( Gia_ObjIsCi(pObj) )
+                continue;
+            assert( Gia_ObjIsAnd(pObj) );
+            sat_solver_add_and( pSat, pObj->Value, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
+        }
+        // collect constant node
+        ABC_SWAP( Vec_Int_t *, vRoots, vRoots2 );
+    }
+    // add constraint variables for the init state
+    Gia_ManForEachObjVec( vRoots, p, pObj, i )
+    {
+        sat_solver_add_constraint( pSat, pObj->Value, Abc_Lit2Var(Vec_IntSize(vNodes)), 1 );
+        pObj = Gia_ObjRiToRo(p, pObj);
+        Bmc_ManBCoreAssignVar( p, pObj, -1, vNodes );
+    }
+    Vec_IntFree( vRoots );
+    Vec_IntFree( vRoots2 );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bmc_ManBCorePerform( Gia_Man_t * p, Bmc_BCorePar_t * pPars )
+{
+    clock_t clk = clock();
+    Intp_Man_t * pManProof;
+    Vec_Int_t * vVarMap, * vCore;
+    sat_solver * pSat;
+    FILE * pFile;
+    void * pSatCnf; 
+    int RetValue;
+    // create SAT solver
+    pSat = sat_solver_new();
+    sat_solver_store_alloc( pSat ); 
+    sat_solver_setnvars( pSat, 1000 );
+    sat_solver_set_runtime_limit( pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
+    vVarMap = Bmc_ManBCoreCollect( p, pPars->iFrame, pPars->iOutput, pSat );
+    sat_solver_store_mark_roots( pSat ); 
+    // create pivot variables
+    if ( pPars->pFilePivots )
+    {
+        Vec_Int_t * vPivots = Bmc_ManBCoreCollectPivots(p, pPars->pFilePivots, vVarMap);
+        sat_solver_set_pivot_variables( pSat, Vec_IntArray(vPivots), Vec_IntSize(vPivots) );
+        Vec_IntReleaseArray( vPivots );
+        Vec_IntFree( vPivots );
+    }
+    // solve the problem
+    RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+    if ( RetValue == l_Undef )
+    {
+        Vec_IntFree( vVarMap );
+        sat_solver_delete( pSat );
+        printf( "Timeout of conflict limit is reached.\n" );
+        return;
+    }
+    if ( RetValue == l_True )
+    {
+        Vec_IntFree( vVarMap );
+        sat_solver_delete( pSat );
+        printf( "The BMC problem is SAT.\n" );
+        return;
+    }
+    if ( pPars->fVerbose )
+    {
+        printf( "SAT solver returned UNSAT after %7d conflicts.      ", (int)pSat->stats.conflicts );
+        Abc_PrintTime( 1, "Time", clock() - clk );
+    }
+    assert( RetValue == l_False );
+    pSatCnf = sat_solver_store_release( pSat ); 
+    Sto_ManDumpClauses( (Sto_Man_t *)pSatCnf, "cnf_store.txt" );
+    // derive the UNSAT core
+    clk = clock();
+    pManProof = Intp_ManAlloc();
+    vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 1, pPars->fVerbose );
+    Intp_ManFree( pManProof );
+    if ( pPars->fVerbose )
+    {
+        printf( "UNSAT core contains %8d (out of %8d) learned clauses.   ", Vec_IntSize(vCore), sat_solver_nconflicts(pSat) );
+        Abc_PrintTime( 1, "Time", clock() - clk );
+    }
+    // write the problem
+    pFile = pPars->pFileProof ? fopen( pPars->pFileProof, "wb" ) : stdout;
+    Intp_ManUnsatCorePrintForBmc( pFile, (Sto_Man_t *)pSatCnf, vCore, vVarMap );
+    if ( pFile != stdout )
+        fclose( pFile );
+    // cleanup
+    Sto_ManFree( (Sto_Man_t *)pSatCnf );
+    Vec_IntFree( vVarMap );
+    Vec_IntFree( vCore );
+    sat_solver_delete( pSat );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
index 6deb9eb1..2ce321c6 100644
--- a/src/sat/bmc/module.make
+++ b/src/sat/bmc/module.make
@@ -1,4 +1,5 @@
-SRC +=    src/sat/bmc/bmcBmc.c \
+SRC +=    src/sat/bmc/bmcBCore.c \
+    src/sat/bmc/bmcBmc.c \
     src/sat/bmc/bmcBmc2.c \
     src/sat/bmc/bmcBmc3.c \
     src/sat/bmc/bmcBmcAnd.c \
diff --git a/src/sat/bsat/satInterP.c b/src/sat/bsat/satInterP.c
index 414879b6..efd03dd3 100644
--- a/src/sat/bsat/satInterP.c
+++ b/src/sat/bsat/satInterP.c
@@ -916,19 +916,20 @@ void Intp_ManUnsatCoreVerify( Sto_Man_t * pCnf, Vec_Int_t * vCore )
   SeeAlso     []
 
 ***********************************************************************/
-void Intp_ManUnsatCore_rec( Vec_Ptr_t * vAntClas, int iThis, Vec_Int_t * vCore, int nRoots, Vec_Int_t * vVisited )
+void Intp_ManUnsatCore_rec( Vec_Ptr_t * vAntClas, int iThis, Vec_Int_t * vCore, int nRoots, Vec_Str_t * vVisited, int fLearned )
 {
 //    int i, iStop, iStart;
     Vec_Int_t * vAnt;
     int i, Entry;
     // skip visited clauses
-    if ( Vec_IntEntry( vVisited, iThis ) )
+    if ( Vec_StrEntry( vVisited, iThis ) )
         return;
-    Vec_IntWriteEntry( vVisited, iThis, 1 );
+    Vec_StrWriteEntry( vVisited, iThis, 1 );
     // add a root clause to the core
     if ( iThis < nRoots )
     {
-        Vec_IntPush( vCore, iThis );
+        if ( !fLearned )
+            Vec_IntPush( vCore, iThis );
         return; 
     }
     // iterate through the clauses
@@ -939,7 +940,10 @@ void Intp_ManUnsatCore_rec( Vec_Ptr_t * vAntClas, int iThis, Vec_Int_t * vCore,
     vAnt = (Vec_Int_t *)Vec_PtrEntry( vAntClas, iThis - nRoots );
     Vec_IntForEachEntry( vAnt, Entry, i )
 //        Intp_ManUnsatCore_rec( vAntClas, Vec_IntEntry(vAnties, i), vCore, nRoots, vVisited );
-        Intp_ManUnsatCore_rec( vAntClas, Entry, vCore, nRoots, vVisited );
+        Intp_ManUnsatCore_rec( vAntClas, Entry, vCore, nRoots, vVisited, fLearned );
+    // collect learned clause
+    if ( fLearned )
+        Vec_IntPush( vCore, iThis );
 }
 
 /**Function*************************************************************
@@ -956,10 +960,10 @@ void Intp_ManUnsatCore_rec( Vec_Ptr_t * vAntClas, int iThis, Vec_Int_t * vCore,
   SeeAlso     []
 
 ***********************************************************************/
-void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose )
+void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fLearned, int fVerbose )
 {
     Vec_Int_t * vCore;
-    Vec_Int_t * vVisited;
+    Vec_Str_t * vVisited;
     Sto_Cls_t * pClause;
     int RetValue = 1;
     abctime clkTotal = Abc_Clock();
@@ -1021,7 +1025,7 @@ void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose )
 
     if ( fVerbose )
     {
-        ABC_PRT( "Core", Abc_Clock() - clkTotal );
+//        ABC_PRT( "Core", Abc_Clock() - clkTotal );
     printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d.  Ave = %.2f.  Mem = %.2f MB\n", 
         p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,  
         1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 
@@ -1031,9 +1035,9 @@ p->timeTotal += Abc_Clock() - clkTotal;
 
     // derive the UNSAT core
     vCore = Vec_IntAlloc( 1000 );
-    vVisited = Vec_IntStart( p->pCnf->pEmpty->Id+1 );
-    Intp_ManUnsatCore_rec( p->vAntClas, p->pCnf->pEmpty->Id, vCore, p->pCnf->nRoots, vVisited );
-    Vec_IntFree( vVisited );
+    vVisited = Vec_StrStart( p->pCnf->pEmpty->Id+1 );
+    Intp_ManUnsatCore_rec( p->vAntClas, p->pCnf->pEmpty->Id, vCore, p->pCnf->nRoots, vVisited, fLearned );
+    Vec_StrFree( vVisited );
     if ( fVerbose )
         printf( "Root clauses = %d. Learned clauses = %d. UNSAT core size = %d.\n", 
             p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, Vec_IntSize(vCore) );
@@ -1041,6 +1045,48 @@ p->timeTotal += Abc_Clock() - clkTotal;
     return vCore;   
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prints learned clauses in terms of original problem varibles.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Intp_ManUnsatCorePrintForBmc( FILE * pFile, Sto_Man_t * pCnf, void * vCore0, void * vVarMap0 )
+{
+    Vec_Int_t * vCore   = (Vec_Int_t *)vCore0;
+    Vec_Int_t * vVarMap = (Vec_Int_t *)vVarMap0;
+    Vec_Ptr_t * vClaMap;
+    Sto_Cls_t * pClause;
+    int v, i, iClause, fCompl, iObj, iFrame;
+    // create map of clause
+    vClaMap = Vec_PtrAlloc( pCnf->nClauses );
+    Sto_ManForEachClause( pCnf, pClause )
+        Vec_PtrPush( vClaMap, pClause );
+    // print clauses
+    fprintf( pFile, "UNSAT contains %d learned clauses:\n", Vec_IntSize(vCore) );
+    Vec_IntForEachEntry( vCore, iClause, i )
+    {
+        pClause = (Sto_Cls_t *)Vec_PtrEntry(vClaMap, iClause);
+        fprintf( pFile, "%6d : %6d : ", i, iClause - pCnf->nRoots );
+        for ( v = 0; v < (int)pClause->nLits; v++ )
+        {
+            fCompl = Abc_LitIsCompl(pClause->pLits[v]);
+            iObj   = Vec_IntEntry(vVarMap, 2*Abc_Lit2Var(pClause->pLits[v]));
+            iFrame = Vec_IntEntry(vVarMap, 2*Abc_Lit2Var(pClause->pLits[v])+1);
+            fprintf( pFile, "%s%d(%d) ", fCompl ? "!":"", iObj, iFrame );
+        }
+        if ( pClause->nLits == 0 )
+            fprintf( pFile, "Empty" );
+        fprintf( pFile, "\n" );
+    }
+    Vec_PtrFree( vClaMap );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 922f1eb7..5ea0b348 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1153,6 +1153,7 @@ void sat_solver_delete(sat_solver* s)
 //    veci_delete(&s->model);
     veci_delete(&s->act_vars);
     veci_delete(&s->unit_lits);
+    veci_delete(&s->pivot_vars);
     veci_delete(&s->temp_clause);
     veci_delete(&s->conf_final);
 
@@ -1490,10 +1491,17 @@ void sat_solver_rollback( sat_solver* s )
 
 int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
 {
+    int fVerbose = 0;
     lit *i,*j;
     int maxvar;
     lit last;
     assert( begin < end );
+    if ( fVerbose )
+    {
+        for ( i = begin; i < end; i++ )
+            printf( "%s%d ", (*i)&1 ? "!":"", (*i)>>1 );
+        printf( "\n" );
+    }
 
     veci_resize( &s->temp_clause, 0 );
     for ( i = begin; i < end; i++ )
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index fb19490c..ccb7d6c4 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -170,6 +170,7 @@ struct sat_solver_t
     int         nCalls;        // the number of local restarts
     int         nCalls2;       // the number of local restarts
     veci        unit_lits;     // variables whose activity has changed
+    veci        pivot_vars;    // pivot variables
 
     int         fSkipSimplify; // set to one to skip simplification of the clause database
     int         fNotUseRandom; // do not allow random decisions with a fixed probability
@@ -255,7 +256,12 @@ static inline void sat_solver_bookmark(sat_solver* s)
         memcpy( s->activity2, s->activity, sizeof(unsigned) * s->iVarPivot );
     }
 }
-
+static inline void sat_solver_set_pivot_variables( sat_solver* s, int * pPivots, int nPivots )
+{
+    s->pivot_vars.cap = nPivots;
+    s->pivot_vars.size = nPivots;
+    s->pivot_vars.ptr = pPivots;
+}
 static inline int sat_solver_count_usedvars(sat_solver* s)
 {
     int i, nVars = 0;
diff --git a/src/sat/bsat/satStore.c b/src/sat/bsat/satStore.c
index fab13666..ad055efe 100644
--- a/src/sat/bsat/satStore.c
+++ b/src/sat/bsat/satStore.c
@@ -320,9 +320,9 @@ void Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName )
     {
         for ( i = 0; i < (int)pClause->nLits; i++ )
             fprintf( pFile, " %d", lit_print(pClause->pLits[i]) );
-        fprintf( pFile, "\n" );
+        fprintf( pFile, " 0\n" );
     }
-    fprintf( pFile, " 0\n" );
+//    fprintf( pFile, " 0\n" );
     fclose( pFile );
 }
 
diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h
index 960f391a..f2480a7d 100644
--- a/src/sat/bsat/satStore.h
+++ b/src/sat/bsat/satStore.h
@@ -142,8 +142,8 @@ extern void *       Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void
 typedef struct Intp_Man_t_ Intp_Man_t;
 extern Intp_Man_t * Intp_ManAlloc();
 extern void         Intp_ManFree( Intp_Man_t * p );
-extern void *       Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose );
-
+extern void *       Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fLearned, int fVerbose );
+extern void         Intp_ManUnsatCorePrintForBmc( FILE * pFile, Sto_Man_t * pCnf, void * vCore, void * vVarMap );
 
 
 ABC_NAMESPACE_HEADER_END