Changes to clause mapping.

8 files changed, 75 insertions, 134 deletions

diff --git a/src/aig/aig/aigRepar.c b/src/aig/aig/aigRepar.c
index f730a545..9232dc0f 100644
--- a/src/aig/aig/aigRepar.c
+++ b/src/aig/aig/aigRepar.c
@@ -52,13 +52,13 @@ static inline void Aig_ManInterAddBuffer( sat_solver2 * pSat, int iVarA, int iVa
 
     Lits[0] = toLitCond( iVarA, 0 );
     Lits[1] = toLitCond( iVarB, !fCompl );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, 0 );
     if ( fMark )
         clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVarA, 1 );
     Lits[1] = toLitCond( iVarB, fCompl );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, 0 );
     if ( fMark )
         clause2_set_partA( pSat, Cid, 1 );
 }
@@ -83,28 +83,28 @@ static inline void Aig_ManInterAddXor( sat_solver2 * pSat, int iVarA, int iVarB,
     Lits[0] = toLitCond( iVarA, !fCompl );
     Lits[1] = toLitCond( iVarB, 1 );
     Lits[2] = toLitCond( iVarC, 1 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, 0 );
     if ( fMark )
         clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVarA, !fCompl );
     Lits[1] = toLitCond( iVarB, 0 );
     Lits[2] = toLitCond( iVarC, 0 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, 0 );
     if ( fMark )
         clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVarA, fCompl );
     Lits[1] = toLitCond( iVarB, 1 );
     Lits[2] = toLitCond( iVarC, 0 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, 0 );
     if ( fMark )
         clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVarA, fCompl );
     Lits[1] = toLitCond( iVarB, 0 );
     Lits[2] = toLitCond( iVarC, 1 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, 0 );
     if ( fMark )
         clause2_set_partA( pSat, Cid, 1 );
 }
@@ -151,14 +151,14 @@ void Aig_ManInterTest( Aig_Man_t * pMan, int fVerbose )
     // add clauses of A
     for ( i = 0; i < pCnf->nClauses; i++ )
     {
-        Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] );
+        Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1], 0 );
         clause2_set_partA( pSat, Cid, 1 );
     }
 
     // add clauses of B
     Cnf_DataLift( pCnf, pCnf->nVars );
     for ( i = 0; i < pCnf->nClauses; i++ )
-        sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] );
+        sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1], 0 );
     Cnf_DataLift( pCnf, -pCnf->nVars );
 
     // add PI equality clauses
@@ -282,7 +282,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose )
         Cnf_DataLift( pCnf, ShiftCnf[k] );
         for ( i = 0; i < pCnf->nClauses; i++ )
         {
-            Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] );
+            Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1], 0 );
             clause2_set_partA( pSat, Cid, k==0 );
         }
         // add equality p[k] == A1/B1
@@ -292,7 +292,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose )
         Cnf_DataLift( pCnf, pCnf->nVars );
         for ( i = 0; i < pCnf->nClauses; i++ )
         {
-            Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] );
+            Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1], 0 );
             clause2_set_partA( pSat, Cid, k==0 );
         }
         // add comparator (!p[k] ^ A2/B2) == or[k]
@@ -302,7 +302,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose )
             Aig_ManInterAddXor( pSat, ShiftP[k] + i, pCnf->pVarNums[pObj->Id], ShiftOr[k] + i, k==1, k==0 );
             Vec_IntPush( vVars, toLitCond(ShiftOr[k] + i, 1) );
         }
-        Cid = sat_solver2_addclause( pSat, Vec_IntArray(vVars), Vec_IntArray(vVars) + Vec_IntSize(vVars) );
+        Cid = sat_solver2_addclause( pSat, Vec_IntArray(vVars), Vec_IntArray(vVars) + Vec_IntSize(vVars), 0 );
         clause2_set_partA( pSat, Cid, k==0 );
         // return to normal
         Cnf_DataLift( pCnf, -ShiftCnf[k]-pCnf->nVars );
@@ -361,7 +361,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose )
             // add to A
             for ( i = 0; i < pCnfInter->nClauses; i++ )
             {
-                Cid = sat_solver2_addclause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] );
+                Cid = sat_solver2_addclause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1], 0 );
                 clause2_set_partA( pSat, Cid, c==0 );
             }
             // connect to the inputs
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 001cd6ee..a19d4d75 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -79,7 +79,6 @@ struct Gla_Man_t_
     int            nSatVars;        // the number of SAT variables
     Cnf_Dat_t *    pCnf;            // CNF derived for the nodes
     sat_solver2 *  pSat;            // incremental SAT solver
-    Vec_Int_t *    vCla2Obj;        // mapping of clauses into GLA objs
     Vec_Int_t *    vTemp;           // temporary array
     Vec_Int_t *    vAddedNew;       // temporary array
     Vec_Int_t *    vObjCounts;      // object counters
@@ -1096,7 +1095,6 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
         Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) );
     }
     // other 
-    p->vCla2Obj  = Vec_IntAlloc( 1000 ); // Vec_IntPush( p->vCla2Obj, -1 );
     p->pSat      = sat_solver2_new();
 //    p->pSat->fVerbose = p->pPars->fVerbose;
 //    sat_solver2_set_learntmax( p->pSat, pPars->nLearnedMax );
@@ -1195,7 +1193,6 @@ Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
         Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) );
     }
     // other 
-    p->vCla2Obj  = Vec_IntAlloc( 1000 ); // Vec_IntPush( p->vCla2Obj, -1 );
     p->pSat      = sat_solver2_new();
     p->nSatVars  = 1;
     return p;
@@ -1229,7 +1226,6 @@ void Gla_ManStop( Gla_Man_t * p )
 //    Gia_ManStaticFanoutStart( p->pGia0 );
     sat_solver2_delete( p->pSat );
     Vec_IntFreeP( &p->vObjCounts );
-    Vec_IntFreeP( &p->vCla2Obj );
     Vec_IntFreeP( &p->vAddedNew );
     Vec_IntFreeP( &p->vCoreCounts );
     Vec_IntFreeP( &p->vTemp );
@@ -1434,9 +1430,7 @@ void Gla_ManAddClauses( Gla_Man_t * p, int iObj, int iFrame, Vec_Int_t * vLits )
     if ( pGlaObj->fConst )
     {
         iVar = Gla_ManGetVar( p, iObj, iFrame );
-        sat_solver2_add_const( p->pSat, iVar, 1, 0 );
-        // remember the clause
-        Vec_IntPush( p->vCla2Obj, iObj );
+        sat_solver2_add_const( p->pSat, iVar, 1, 0, iObj );
     }
     else if ( pGlaObj->fRo )
     {
@@ -1444,18 +1438,13 @@ void Gla_ManAddClauses( Gla_Man_t * p, int iObj, int iFrame, Vec_Int_t * vLits )
         if ( iFrame == 0 )
         {
             iVar = Gla_ManGetVar( p, iObj, iFrame );
-            sat_solver2_add_const( p->pSat, iVar, 1, 0 );
-            // remember the clause
-            Vec_IntPush( p->vCla2Obj, iObj );
+            sat_solver2_add_const( p->pSat, iVar, 1, 0, iObj );
         }
         else
         {
             iVar1 = Gla_ManGetVar( p, iObj, iFrame );
             iVar2 = Gla_ManGetVar( p, pGlaObj->Fanins[0], iFrame-1 );
-            sat_solver2_add_buffer( p->pSat, iVar1, iVar2, pGlaObj->fCompl0, 0 );
-            // remember the clause
-            Vec_IntPush( p->vCla2Obj, iObj );
-            Vec_IntPush( p->vCla2Obj, iObj );
+            sat_solver2_add_buffer( p->pSat, iVar1, iVar2, pGlaObj->fCompl0, 0, iObj );
         }
     }
     else if ( pGlaObj->fAnd )
@@ -1471,10 +1460,7 @@ void Gla_ManAddClauses( Gla_Man_t * p, int iObj, int iFrame, Vec_Int_t * vLits )
                 iVar = Gla_ManGetVar( p, lit_var(*pLit), iFrame );
                 Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
             }
-            RetValue = sat_solver2_addclause( p->pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
-            assert( RetValue );
-            // remember the clause
-            Vec_IntPush( p->vCla2Obj, iObj );
+            RetValue = sat_solver2_addclause( p->pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits), iObj );
         }
     }
     else assert( 0 );
@@ -1555,12 +1541,11 @@ int Gla_ManGetOutLit( Gla_Man_t * p, int f )
         return -1;
     return Abc_Var2Lit( iSat, p->pObjRoot->fCompl0 );
 }
-Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, Vec_Int_t * vCla2Obj, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls )
+Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls )
 {
     Vec_Int_t * vCore;
-    int iLit = Gla_ManGetOutLit( p, f );
     int nConfPrev = pSat->stats.conflicts;
-    int i, Entry, RetValue;
+    int RetValue, iLit = Gla_ManGetOutLit( p, f );
     clock_t clk = clock();
     if ( piRetValue )
         *piRetValue = 1;
@@ -1595,23 +1580,11 @@ Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, Vec_Int_t * vCla2Obj, sat_so
 //        Abc_PrintTime( 1, "Time", clock() - clk );
     }
     assert( RetValue == l_False );
-
     // derive the UNSAT core
     clk = clock();
     vCore = (Vec_Int_t *)Sat_ProofCore( pSat );
     if ( fVerbose )
     {
-//        Abc_Print( 1, "Core is %8d clauses (out of %8d).   ", Vec_IntSize(vCore), sat_solver2_nclauses(pSat) );
-//        Abc_PrintTime( 1, "Time", clock() - clk );
-    }
-
-    // remap core into original objects 
-    Vec_IntForEachEntry( vCore, Entry, i )
-        Vec_IntWriteEntry( vCore, i, Vec_IntEntry(p->vCla2Obj, Entry) );
-    Vec_IntUniqify( vCore );
-    Vec_IntReverseOrder( vCore );
-    if ( fVerbose )
-    {
 //        Abc_Print( 1, "Core is %8d vars    (out of %8d).   ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) );
 //        Abc_PrintTime( 1, "Time", clock() - clk );
     }
@@ -1670,7 +1643,6 @@ void Gla_ManReportMemory( Gla_Man_t * p )
         memMap += Vec_IntCap(&pGla->vFrames) * sizeof(int);
     for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
         memRef += Vec_IntCap(&p->pvRefis[i]) * sizeof(int);
-    memOth += Vec_IntCap(p->vCla2Obj) * sizeof(int);
     memOth += Vec_IntCap(p->vAddedNew) * sizeof(int);
     memOth += Vec_IntCap(p->vTemp) * sizeof(int);
     memOth += Vec_IntCap(p->vAbs) * sizeof(int);
@@ -1841,7 +1813,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
         for ( i = 0; ; i++ )
         { 
             clk2 = clock();
-            vCore = Gla_ManUnsatCore( p, f, p->vCla2Obj, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
+            vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
             assert( (vCore != NULL) == (Status == 1) );
             if ( Status == -1 ) // resource limit is reached
             {
@@ -1914,15 +1886,15 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
             sat_solver2_rollback( p->pSat );
             // update storage
             Gla_ManRollBack( p );
-            Vec_IntShrink( p->vCla2Obj, (int)p->pSat->stats.clauses );
             p->nSatVars = nVarsOld;
             // load this timeframe
+            Vec_IntSort( vCore, 1 );
             Gia_GlaAddToAbs( p, vCore, 0 );
             Gia_GlaAddOneSlice( p, f, vCore );
             Vec_IntFree( vCore );
             // run SAT solver
             clk2 = clock();
-            vCore = Gla_ManUnsatCore( p, f, p->vCla2Obj, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
+            vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
             p->timeUnsat += clock() - clk2;
             assert( (vCore != NULL) == (Status == 1) );
             Vec_IntFreeP( &vCore );
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index ee89d03f..735bb823 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -67,7 +67,6 @@ struct Vta_Man_t_
     int           nSeenGla;     // seen objects in all frames
     int           nSeenAll;     // seen objects in all frames
     // other data
-    Vec_Int_t *   vCla2Var;     // map clauses into variables
     Vec_Ptr_t *   vCores;       // unsat core for each frame
     sat_solver2 * pSat;         // incremental SAT solver
     Vec_Int_t *   vAddedNew;    // the IDs of variables added to the solver
@@ -1034,7 +1033,6 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
     p->nSeenGla    = 1;
     p->nSeenAll    = 1;
     // other data
-    p->vCla2Var    = Vec_IntAlloc( 1000 ); // Vec_IntPush( p->vCla2Var, -1 );
     p->vCores      = Vec_PtrAlloc( 100 );
     p->pSat        = sat_solver2_new();
 //    p->pSat->fVerbose = p->pPars->fVerbose;
@@ -1071,7 +1069,6 @@ void Vga_ManStop( Vta_Man_t * p )
     Vec_BitFreeP( &p->vSeenGla );
     Vec_IntFreeP( &p->vSeens );
     Vec_IntFreeP( &p->vOrder );
-    Vec_IntFreeP( &p->vCla2Var );
     Vec_IntFreeP( &p->vAddedNew );
     sat_solver2_delete( p->pSat );
     ABC_FREE( p->pBins );
@@ -1098,7 +1095,7 @@ static inline int Vga_ManGetOutLit( Vta_Man_t * p, int f )
     if ( f == 0 && Gia_ObjIsRo(p->pGia, Gia_ObjFanin0(pObj)) && !Gia_ObjFaninC0(pObj) )
         return -Vta_ObjId(p, pThis);
     return Abc_Var2Lit( Vta_ObjId(p, pThis), Gia_ObjFaninC0(pObj) );
-}
+} 
 
 /**Function*************************************************************
 
@@ -1111,13 +1108,11 @@ static inline int Vga_ManGetOutLit( Vta_Man_t * p, int f )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls )
+Vec_Int_t * Vta_ManUnsatCore( int iLit, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls )
 {
-    Vec_Int_t * vPres;
-    Vec_Int_t * vCore;
-    int k, i, Entry, RetValue;
     clock_t clk = clock();
-    int nConfPrev = pSat->stats.conflicts;
+    Vec_Int_t * vCore;
+    int RetValue, nConfPrev = pSat->stats.conflicts;
     if ( piRetValue )
         *piRetValue = 1;
     // consider special case when PO points to the flop
@@ -1151,32 +1146,11 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat
 //        Abc_PrintTime( 1, "Time", clock() - clk );
     }
     assert( RetValue == l_False );
-
     // derive the UNSAT core
     clk = clock();
     vCore = (Vec_Int_t *)Sat_ProofCore( pSat );
     if ( fVerbose )
     {
-//        Abc_Print( 1, "Core is %8d clauses (out of %8d).   ", Vec_IntSize(vCore), sat_solver2_nclauses(pSat) );
-//        Abc_PrintTime( 1, "Time", clock() - clk );
-    }
-
-    // remap core into variables
-    clk = clock();
-    vPres = Vec_IntStart( sat_solver2_nvars(pSat) );
-    k = 0; 
-    Vec_IntForEachEntry( vCore, Entry, i )
-    {
-        Entry = Vec_IntEntry(vCla2Var, Entry);
-        if ( Vec_IntEntry(vPres, Entry) )
-            continue;
-        Vec_IntWriteEntry( vPres, Entry, 1 );
-        Vec_IntWriteEntry( vCore, k++, Entry );
-    }
-    Vec_IntShrink( vCore, k );
-    Vec_IntFree( vPres );
-    if ( fVerbose )
-    {
 //        Abc_Print( 1, "Core is %8d vars    (out of %8d).   ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) );
 //        Abc_PrintTime( 1, "Time", clock() - clk );
     }
@@ -1322,10 +1296,7 @@ void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame )
         iThis0 = Vta_ObjId(p, pThis0);
         pThis1 = Vga_ManFindOrAdd( p, Gia_ObjFaninId1p(p->pGia, pObj), iFrame );
         sat_solver2_add_and( p->pSat, iMainVar, iThis0, Vta_ObjId(p, pThis1), 
-            Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
-        Vec_IntPush( p->vCla2Var, iMainVar );
-        Vec_IntPush( p->vCla2Var, iMainVar );
-        Vec_IntPush( p->vCla2Var, iMainVar );
+            Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0, iMainVar );
     }
     else if ( Gia_ObjIsRo(p->pGia, pObj) )
     {
@@ -1334,29 +1305,23 @@ void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame )
             if ( p->pPars->fUseTermVars )
             {
                 pThis0 = Vga_ManFindOrAdd( p, iObj, -1 );
-                sat_solver2_add_constraint( p->pSat, iMainVar, Vta_ObjId(p, pThis0), 1, 0 );
-                Vec_IntPush( p->vCla2Var, iMainVar );
-                Vec_IntPush( p->vCla2Var, iMainVar );
+                sat_solver2_add_constraint( p->pSat, iMainVar, Vta_ObjId(p, pThis0), 1, 0, iMainVar );
             }
             else
             {
-                sat_solver2_add_const( p->pSat, iMainVar, 1, 0 );
-                Vec_IntPush( p->vCla2Var, iMainVar );
+                sat_solver2_add_const( p->pSat, iMainVar, 1, 0, iMainVar );
             }
         }
         else
         {
             pObj = Gia_ObjRoToRi( p->pGia, pObj );
             pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame-1 );
-            sat_solver2_add_buffer( p->pSat, iMainVar, Vta_ObjId(p, pThis0), Gia_ObjFaninC0(pObj), 0 );  
-            Vec_IntPush( p->vCla2Var, iMainVar );
-            Vec_IntPush( p->vCla2Var, iMainVar );
+            sat_solver2_add_buffer( p->pSat, iMainVar, Vta_ObjId(p, pThis0), Gia_ObjFaninC0(pObj), 0, iMainVar );  
         }
     }
     else if ( Gia_ObjIsConst0(pObj) )
     {
-        sat_solver2_add_const( p->pSat, iMainVar, 1, 0 );
-        Vec_IntPush( p->vCla2Var, iMainVar );
+        sat_solver2_add_const( p->pSat, iMainVar, 1, 0, iMainVar );
     }
     else //if ( !Gia_ObjIsPi(p->pGia, pObj) )
         assert( 0 );
@@ -1530,7 +1495,6 @@ void Gia_VtaPrintMemory( Vta_Man_t * p )
     memOth += Vec_IntCap(p->vOrder) * sizeof(int);
     memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vFrames );
     memOth += Vec_BitCap(p->vSeenGla) * sizeof(int);
-    memOth += Vec_IntCap(p->vCla2Var) * sizeof(int);
     memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCores );
     memOth += Vec_IntCap(p->vAddedNew) * sizeof(int);
     memTot = memAig + memSat + memPro + memMap + memOth;
@@ -1617,7 +1581,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         for ( i = 0; ; i++ )
         { 
             clk2 = clock();
-            vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
+            vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
             assert( (vCore != NULL) == (Status == 1) );
             if ( Status == -1 ) // resource limit is reached
             {
@@ -1658,14 +1622,13 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         sat_solver2_rollback( p->pSat );
         // update storage
         Vga_ManRollBack( p, nObjOld );
-        Vec_IntShrink( p->vCla2Var, (int)p->pSat->stats.clauses );
         // load this timeframe
         Vga_ManLoadSlice( p, vCore, 0 );
         Vec_IntFree( vCore );
 
         // run SAT solver
         clk2 = clock();
-        vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
+        vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
         p->timeUnsat += clock() - clk2;
         assert( (vCore != NULL) == (Status == 1) );
         if ( Status == -1 ) // resource limit is reached
diff --git a/src/aig/saig/saigGlaPba2.c b/src/aig/saig/saigGlaPba2.c
index 5e745f4c..cff7b7fc 100644
--- a/src/aig/saig/saigGlaPba2.c
+++ b/src/aig/saig/saigGlaPba2.c
@@ -72,7 +72,7 @@ struct Aig_Gla3Man_t_
 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 ) )
+    if ( !sat_solver2_addclause( pSat, &Lit, &Lit + 1, 0 ) )
         return 0;
     return 1;
 }
@@ -94,12 +94,12 @@ static inline int Aig_Gla3AddBuffer( sat_solver2 * pSat, int iVar0, int iVar1, i
 
     Lits[0] = toLitCond( iVar0, 0 );
     Lits[1] = toLitCond( iVar1, !fCompl );
-    if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) )
+    if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) )
         return 0;
 
     Lits[0] = toLitCond( iVar0, 1 );
     Lits[1] = toLitCond( iVar1, fCompl );
-    if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) )
+    if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) )
         return 0;
 
     return 1;
@@ -122,18 +122,18 @@ static inline int Aig_Gla3AddNode( sat_solver2 * pSat, int iVar, int iVar0, int
 
     Lits[0] = toLitCond( iVar, 1 );
     Lits[1] = toLitCond( iVar0, fCompl0 );
-    if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) )
+    if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) )
         return 0;
 
     Lits[0] = toLitCond( iVar, 1 );
     Lits[1] = toLitCond( iVar1, fCompl1 );
-    if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) )
+    if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) )
         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 ) )
+    if ( !sat_solver2_addclause( pSat, Lits, Lits + 3, 0 ) )
         return 0;
 
     return 1;
@@ -302,7 +302,7 @@ int Aig_Gla3CreateSatSolver( Aig_Gla3Man_t * p )
     vPoLits = Vec_IntAlloc( p->nFramesMax );
     for ( f = p->nStart; f < p->nFramesMax; f++ )
         Vec_IntPush( vPoLits, 2 * Aig_Gla3FetchVar(p, Aig_ManCo(p->pAig, 0), f) );
-    sat_solver2_addclause( p->pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) );
+    sat_solver2_addclause( p->pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits), 0 );
     Vec_IntFree( vPoLits );
     Vec_IntPush( p->vCla2Obj, 0 );
     Vec_IntPush( p->vCla2Fra, 0 );
diff --git a/src/sat/bsat/satClause.h b/src/sat/bsat/satClause.h
index 7769dc36..d5df71ad 100644
--- a/src/sat/bsat/satClause.h
+++ b/src/sat/bsat/satClause.h
@@ -136,7 +136,7 @@ static inline lit      clause_read_lit( cla h )                     { return (li
 static inline int      clause_learnt_h( Sat_Mem_t * p, cla h )      { return (h & p->uLearnedMask) > 0;            }
 static inline int      clause_learnt( clause * c )                  { return c->lrn;                               }
 static inline int      clause_id( clause * c )                      { return c->lits[c->size];                     }
-static inline int      clause_set_id( clause * c, int id )          { c->lits[c->size] = id;                       }
+static inline void     clause_set_id( clause * c, int id )          { c->lits[c->size] = id;                       }
 static inline int      clause_size( clause * c )                    { return c->size;                              }
 static inline lit *    clause_begin( clause * c )                   { return c->lits;                              }
 static inline lit *    clause_end( clause * c )                     { return c->lits + c->size;                    }
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 0bca05ed..7597207b 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -1245,7 +1245,7 @@ void sat_solver2_delete(sat_solver2* s)
 }
 
 
-int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end)
+int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end, int Id)
 {
     cla Cid;
     lit *i,*j,*iFree = NULL;
@@ -1294,6 +1294,8 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end)
 
     // create a new clause
     Cid = clause2_create_new( s, begin, end, 0, 0 );
+    if ( Id )
+        clause2_set_id( s, Cid, Id );
 
     // handle unit clause
     if ( count+1 == end-begin )
@@ -1461,6 +1463,7 @@ void sat_solver2_reducedb(sat_solver2* s)
             continue;
         if ( !clause_learnt_h(pMem, s->reasons[i]) ) // problem clause
             continue;
+        assert( c->lrn );
         c = clause2_read( s, s->reasons[i] );
         assert( c->mark == 0 );
         s->reasons[i] = clause_id(c); // updating handle here!!!
@@ -1478,6 +1481,7 @@ void sat_solver2_reducedb(sat_solver2* s)
                 pArray[j++] = pArray[k];
             else 
             {
+                assert( c->lrn );
                 c = clause2_read(s, pArray[k]);
                 if ( !c->mark ) // useful learned clause
                    pArray[j++] = clause_id(c); // updating handle here!!!
@@ -1491,6 +1495,7 @@ void sat_solver2_reducedb(sat_solver2* s)
         for ( i = 0; i < s->size; i++ )
             if ( s->units[i] && clause_learnt_h(pMem, s->units[i]) )
             {
+                assert( c->lrn );
                 c = clause2_read( s, s->units[i] );
                 assert( c->mark == 0 );
                 s->units[i] = clause_id(c);
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index f5fe3000..81ecea76 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -45,7 +45,7 @@ typedef struct sat_solver2_t sat_solver2;
 extern sat_solver2* sat_solver2_new(void);
 extern void         sat_solver2_delete(sat_solver2* s);
 
-extern int          sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end);
+extern int          sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end, int Id);
 extern int          sat_solver2_simplify(sat_solver2* s);
 extern int          sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
 extern void         sat_solver2_rollback(sat_solver2* s);
@@ -159,13 +159,14 @@ struct sat_solver2_t
     clock_t         nRuntimeLimit;  // external limit on runtime
 };
 
-static inline clause * clause2_read( sat_solver2 * s, cla h )                  { return Sat_MemClauseHand( &s->Mem, h );   }
+static inline clause * clause2_read( sat_solver2 * s, cla h )                  { return Sat_MemClauseHand( &s->Mem, h ); }
 static inline int      clause2_proofid(sat_solver2* s, clause* c, int partA)   { return c->lrn ? (veci_begin(&s->claProofs)[clause_id(c)]<<2) | (partA<<1) : (clause_id(c)<<2) | (partA<<1) | 1; }
 
 // these two only work after creating a clause before the solver is called
-static inline int   clause2_is_partA (sat_solver2* s, int h)                   { return clause2_read(s, h)->partA;         }
-static inline void  clause2_set_partA(sat_solver2* s, int h, int partA)        { clause2_read(s, h)->partA = partA;        }
-static inline int   clause2_id(sat_solver2* s, int h)                          { return clause_id(clause2_read(s, h));     }
+static inline int   clause2_is_partA (sat_solver2* s, int h)                   { return clause2_read(s, h)->partA;       }
+static inline void  clause2_set_partA(sat_solver2* s, int h, int partA)        { clause2_read(s, h)->partA = partA;      }
+static inline int   clause2_id(sat_solver2* s, int h)                          { return clause_id(clause2_read(s, h));   }
+static inline void  clause2_set_id(sat_solver2* s, int h, int id)              { clause_set_id(clause2_read(s, h), id);  }
 
 //=================================================================================================
 // Public APIs:
@@ -237,19 +238,19 @@ static inline void sat_solver2_bookmark(sat_solver2* s)
     Sat_MemBookMark( &s->Mem );
 }
 
-static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark )
+static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark, int Id )
 {
     lit Lits[1];
     int Cid;
     assert( iVar >= 0 );
 
     Lits[0] = toLitCond( iVar, fCompl );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 1 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 1, Id );
     if ( fMark )
         clause2_set_partA( pSat, Cid, 1 );
     return 1;
 }
-static inline int sat_solver2_add_buffer( sat_solver2 * pSat, int iVarA, int iVarB, int fCompl, int fMark )
+static inline int sat_solver2_add_buffer( sat_solver2 * pSat, int iVarA, int iVarB, int fCompl, int fMark, int Id )
 {
     lit Lits[2];
     int Cid;
@@ -257,43 +258,43 @@ static inline int sat_solver2_add_buffer( sat_solver2 * pSat, int iVarA, int iVa
 
     Lits[0] = toLitCond( iVarA, 0 );
     Lits[1] = toLitCond( iVarB, !fCompl );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, Id );
     if ( fMark )
         clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVarA, 1 );
     Lits[1] = toLitCond( iVarB, fCompl );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, Id );
     if ( fMark )
         clause2_set_partA( pSat, Cid, 1 );
     return 2;
 }
-static inline int sat_solver2_add_and( sat_solver2 * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fMark )
+static inline int sat_solver2_add_and( sat_solver2 * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fMark, int Id )
 {
     lit Lits[3];
     int Cid;
 
     Lits[0] = toLitCond( iVar, 1 );
     Lits[1] = toLitCond( iVar0, fCompl0 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, Id );
     if ( fMark )
         clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVar, 1 );
     Lits[1] = toLitCond( iVar1, fCompl1 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, Id );
     if ( fMark )
         clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVar, 0 );
     Lits[1] = toLitCond( iVar0, !fCompl0 );
     Lits[2] = toLitCond( iVar1, !fCompl1 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, Id );
     if ( fMark )
         clause2_set_partA( pSat, Cid, 1 );
     return 3;
 }
-static inline int sat_solver2_add_xor( sat_solver2 * pSat, int iVarA, int iVarB, int iVarC, int fCompl, int fMark )
+static inline int sat_solver2_add_xor( sat_solver2 * pSat, int iVarA, int iVarB, int iVarC, int fCompl, int fMark, int Id )
 {
     lit Lits[3];
     int Cid;
@@ -302,33 +303,33 @@ static inline int sat_solver2_add_xor( sat_solver2 * pSat, int iVarA, int iVarB,
     Lits[0] = toLitCond( iVarA, !fCompl );
     Lits[1] = toLitCond( iVarB, 1 );
     Lits[2] = toLitCond( iVarC, 1 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, Id );
     if ( fMark )
         clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVarA, !fCompl );
     Lits[1] = toLitCond( iVarB, 0 );
     Lits[2] = toLitCond( iVarC, 0 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, Id );
     if ( fMark )
         clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVarA, fCompl );
     Lits[1] = toLitCond( iVarB, 1 );
     Lits[2] = toLitCond( iVarC, 0 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, Id );
     if ( fMark )
         clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVarA, fCompl );
     Lits[1] = toLitCond( iVarB, 0 );
     Lits[2] = toLitCond( iVarC, 1 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, Id );
     if ( fMark )
         clause2_set_partA( pSat, Cid, 1 );
     return 4;
 }
-static inline int sat_solver2_add_constraint( sat_solver2 * pSat, int iVar, int iVar2, int fCompl, int fMark )
+static inline int sat_solver2_add_constraint( sat_solver2 * pSat, int iVar, int iVar2, int fCompl, int fMark, int Id )
 {
     lit Lits[2];
     int Cid;
@@ -336,13 +337,13 @@ static inline int sat_solver2_add_constraint( sat_solver2 * pSat, int iVar, int
 
     Lits[0] = toLitCond( iVar, fCompl );
     Lits[1] = toLitCond( iVar2, 0 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, Id );
     if ( fMark )
         clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVar, fCompl );
     Lits[1] = toLitCond( iVar2, 1 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, Id );
     if ( fMark )
         clause2_set_partA( pSat, Cid, 1 );
     return 2;
diff --git a/src/sat/cnf/cnfMan.c b/src/sat/cnf/cnfMan.c
index 10043882..a8c63bf5 100644
--- a/src/sat/cnf/cnfMan.c
+++ b/src/sat/cnf/cnfMan.c
@@ -453,7 +453,7 @@ void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit )
     sat_solver2_setnvars( pSat, p->nVars * nFrames );
     for ( i = 0; i < p->nClauses; i++ )
     {
-        if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) )
+        if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1], 0 ) )
         {
             sat_solver2_delete( pSat );
             return NULL;
@@ -472,14 +472,14 @@ void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit )
             {
                 Lits[0] = (f-1)*nLitsAll + toLitCond( p->pVarNums[pObjLi->Id], 0 );
                 Lits[1] =  f   *nLitsAll + toLitCond( p->pVarNums[pObjLo->Id], 1 );
-                if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) )
+                if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) )
                 {
                     sat_solver2_delete( pSat );
                     return NULL;
                 }
                 Lits[0]++;
                 Lits[1]--;
-                if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) )
+                if ( !sat_solver2_addclause( pSat, Lits, Lits + 2, 0 ) )
                 {
                     sat_solver2_delete( pSat );
                     return NULL;
@@ -490,7 +490,7 @@ void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit )
                 pLits[i] += nLitsAll;
             for ( i = 0; i < p->nClauses; i++ )
             {
-                if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) )
+                if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1], 0 ) )
                 {
                     sat_solver2_delete( pSat );
                     return NULL;
@@ -509,7 +509,7 @@ void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit )
         Aig_ManForEachLoSeq( p->pMan, pObjLo, i )
         {
             Lits[0] = toLitCond( p->pVarNums[pObjLo->Id], 1 );
-            if ( !sat_solver2_addclause( pSat, Lits, Lits + 1 ) )
+            if ( !sat_solver2_addclause( pSat, Lits, Lits + 1, 0 ) )
             {
                 sat_solver2_delete( pSat );
                 return NULL;
@@ -572,7 +572,7 @@ int Cnf_DataWriteOrClause2( void * p, Cnf_Dat_t * pCnf )
     pLits = ABC_ALLOC( int, Aig_ManCoNum(pCnf->pMan) );
     Aig_ManForEachCo( pCnf->pMan, pObj, i )
         pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
-    if ( !sat_solver2_addclause( pSat, pLits, pLits + Aig_ManCoNum(pCnf->pMan) ) )
+    if ( !sat_solver2_addclause( pSat, pLits, pLits + Aig_ManCoNum(pCnf->pMan), 0 ) )
     {
         ABC_FREE( pLits );
         return 0;