Improved memory management of proof-logging and propagated changes.

12 files changed, 450 insertions, 2666 deletions

diff --git a/src/proof/fra/fraCec.c b/src/proof/fra/fraCec.c
index ac11b0bb..1ef9091a 100644
--- a/src/proof/fra/fraCec.c
+++ b/src/proof/fra/fraCec.c
@@ -147,7 +147,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
             pMan->pData = Sat_Solver2GetModel( pSat, vCiIds->pArray, vCiIds->nSize );
         }
         // free the sat_solver2
-        if ( fVerbose )
+//        if ( fVerbose )
             Sat_Solver2PrintStats( stdout, pSat );
     //sat_solver2_store_write( pSat, "trace.cnf" );
     //sat_solver2_store_free( pSat );
@@ -253,7 +253,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
             pMan->pData = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
         }
         // free the sat_solver
-        if ( fVerbose )
+//        if ( fVerbose )
             Sat_SolverPrintStats( stdout, pSat );
     //sat_solver_store_write( pSat, "trace.cnf" );
     //sat_solver_store_free( pSat );
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index 1eaf4407..dcb02bcd 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -22,18 +22,16 @@
 #include "src/misc/vec/vec.h"
 #include "src/aig/aig/aig.h"
 #include "satTruth.h"
-#include "vecRec.h"
+#include "vecSet.h"
 
 ABC_NAMESPACE_IMPL_START
 
 
 /*
-    Proof is represented as a vector of integers.
-    The first entry is -1.
-    A resolution record is represented by a handle (an offset in this array).
+    Proof is represented as a vector of records.
+    A resolution record is represented by a handle (an offset in this vector).
     A resolution record entry is <size><label><ant1><ant2>...<antN>
-    Label is initialized to 0.
-    Root clauses are given by their handles.
+    Label is initialized to 0. Root clauses are given by their handles.
     They are marked by bitshifting by 2 bits up and setting the LSB to 1
 */
 
@@ -58,26 +56,25 @@ struct satset_t
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline satset* Proof_NodeRead    (Vec_Int_t* p, cla h)     { return satset_read( (veci*)p, h );   }
-//static inline cla     Proof_NodeHandle  (Vec_Int_t* p, satset* c) { return satset_handle( (veci*)p, c ); }
-//static inline int     Proof_NodeCheck   (Vec_Int_t* p, satset* c) { return satset_check( (veci*)p, c );  }
-static inline int     Proof_NodeSize    (int nEnts)               { return sizeof(satset)/4 + nEnts;     }
-
-static inline satset* Proof_ResolveRead (Vec_Rec_t* p, cla h)     { return (satset*)Vec_RecEntryP(p, h); }
+static inline satset* Proof_ClauseRead  ( Vec_Int_t* p, cla h )     { assert( h > 0 );     return satset_read( (veci *)p, h );    }
+static inline satset* Proof_NodeRead    ( Vec_Set_t* p, cla h )     { assert( h > 0 );     return (satset*)Vec_SetEntry( p, h );  }
+static inline int     Proof_NodeWordNum ( int nEnts )               { assert( nEnts > 0 ); return 1 + ((nEnts + 1) >> 1);         }
 
 // iterating through nodes in the proof
-#define Proof_ForeachNode( p, pNode, h )                         \
-    for ( h = 1; (h < Vec_IntSize(p)) && ((pNode) = Proof_NodeRead(p, h)); h += Proof_NodeSize(pNode->nEnts) )
+#define Proof_ForeachClauseVec( pVec, p, pNode, i )          \
+    for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_ClauseRead(p, Vec_IntEntry(pVec,i))); i++ )
 #define Proof_ForeachNodeVec( pVec, p, pNode, i )            \
     for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_NodeRead(p, Vec_IntEntry(pVec,i))); i++ )
+#define Proof_ForeachNodeVec1( pVec, p, pNode, i )            \
+    for ( i = 1; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_NodeRead(p, Vec_IntEntry(pVec,i))); i++ )
 
 // iterating through fanins of a proof node
-#define Proof_NodeForeachFanin( p, pNode, pFanin, i )        \
-    for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = (pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(p, pNode->pEnts[i] >> 2)), 1); i++ )
+#define Proof_NodeForeachFanin( pProof, pNode, pFanin, i )        \
+    for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = (pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(pProof, pNode->pEnts[i] >> 2)), 1); i++ )
 #define Proof_NodeForeachLeaf( pClauses, pNode, pLeaf, i )   \
-    for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pClauses, pNode->pEnts[i] >> 2) : NULL), 1); i++ )
-#define Proof_NodeForeachFaninLeaf( p, pClauses, pNode, pFanin, i )    \
-    for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pClauses, pNode->pEnts[i] >> 2) : Proof_NodeRead(p, pNode->pEnts[i] >> 2)); i++ )
+    for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_ClauseRead(pClauses, pNode->pEnts[i] >> 2) : NULL), 1); i++ )
+#define Proof_NodeForeachFaninLeaf( pProof, pClauses, pNode, pFanin, i )    \
+    for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_ClauseRead(pClauses, pNode->pEnts[i] >> 2) : Proof_NodeRead(pProof, pNode->pEnts[i] >> 2)); i++ )
 
 
 ////////////////////////////////////////////////////////////////////////
@@ -86,48 +83,6 @@ static inline satset* Proof_ResolveRead (Vec_Rec_t* p, cla h)     { return (sats
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the number of proof nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Proof_CountAll( Vec_Int_t * p )
-{
-    satset * pNode;
-    int hNode, Counter = 0;
-    Proof_ForeachNode( p, pNode, hNode )
-        Counter++;
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects all resolution nodes belonging to the proof.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Proof_CollectAll( Vec_Int_t * p )
-{
-    Vec_Int_t * vUsed;
-    satset * pNode;
-    int hNode;
-    vUsed = Vec_IntAlloc( 1000 );
-    Proof_ForeachNode( p, pNode, hNode )
-        Vec_IntPush( vUsed, hNode );
-    return vUsed;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Cleans collected resultion nodes belonging to the proof.]
 
   Description []
@@ -137,7 +92,7 @@ Vec_Int_t * Proof_CollectAll( Vec_Int_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Proof_CleanCollected( Vec_Int_t * vProof, Vec_Int_t * vUsed )
+void Proof_CleanCollected( Vec_Set_t * vProof, Vec_Int_t * vUsed )
 {
     satset * pNode;
     int hNode;
@@ -147,7 +102,7 @@ void Proof_CleanCollected( Vec_Int_t * vProof, Vec_Int_t * vUsed )
 
 /**Function*************************************************************
 
-  Synopsis    [Recursively visits useful proof nodes.]
+  Synopsis    [Marks useful nodes of the proof.]
 
   Description []
                
@@ -156,7 +111,7 @@ void Proof_CleanCollected( Vec_Int_t * vProof, Vec_Int_t * vUsed )
   SeeAlso     []
 
 ***********************************************************************/
-void Proof_CollectUsed_iter( Vec_Int_t * vProof, int hNode, Vec_Int_t * vUsed, Vec_Int_t * vStack )
+void Proof_CollectUsed_iter( Vec_Set_t * vProof, int hNode, Vec_Int_t * vUsed, Vec_Int_t * vStack )
 {
     satset * pNext, * pNode = Proof_NodeRead( vProof, hNode );
     int i;
@@ -198,46 +153,33 @@ void Proof_CollectUsed_iter( Vec_Int_t * vProof, int hNode, Vec_Int_t * vUsed, V
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Proof_CollectUsedIter( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hRoot )
+Vec_Int_t * Proof_CollectUsedIter( Vec_Set_t * vProof, Vec_Int_t * vRoots, int fSort )
 {
+    int fVerify = 0;
     Vec_Int_t * vUsed, * vStack;
     int clk = clock();
     int i, Entry, iPrev = 0;
-    assert( (hRoot > 0) ^ (vRoots != NULL) );
     vUsed = Vec_IntAlloc( 1000 );
     vStack = Vec_IntAlloc( 1000 );
-    if ( hRoot )
-        Proof_CollectUsed_iter( vProof, hRoot, vUsed, vStack );
-    else
-    {
-        Vec_IntForEachEntry( vRoots, Entry, i )
+    Vec_IntForEachEntry( vRoots, Entry, i )
+        if ( Entry >= 0 )
             Proof_CollectUsed_iter( vProof, Entry, vUsed, vStack );
-    }
     Vec_IntFree( vStack );
 //    Abc_PrintTime( 1, "Iterative clause collection time", clock() - clk );
-
-/*
-    // verify topological order
-    iPrev = 0;
-    Vec_IntForEachEntry( vUsed, Entry, i )
-    {
-        printf( "%d ", Entry - iPrev );
-        iPrev = Entry;
-    }
-*/
     clk = clock();
-//    Vec_IntSort( vUsed, 0 );
     Abc_Sort( Vec_IntArray(vUsed), Vec_IntSize(vUsed) );
 //    Abc_PrintTime( 1, "Postprocessing with sorting time", clock() - clk );
-
     // verify topological order
-    iPrev = 0;
-    Vec_IntForEachEntry( vUsed, Entry, i )
+    if ( fVerify )
     {
-        if ( iPrev >= Entry )
-            printf( "Out of topological order!!!\n" );
-        assert( iPrev < Entry );
-        iPrev = Entry;
+        iPrev = 0;
+        Vec_IntForEachEntry( vUsed, Entry, i )
+        {
+            if ( iPrev >= Entry )
+                printf( "Out of topological order!!!\n" );
+            assert( iPrev < Entry );
+            iPrev = Entry;
+        }
     }
     return vUsed;
 }
@@ -253,7 +195,7 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Int_t * vProof, Vec_Int_t * vRoots, int h
   SeeAlso     []
 
 ***********************************************************************/
-void Proof_CollectUsed_rec( Vec_Int_t * vProof, int hNode, Vec_Int_t * vUsed )
+void Proof_CollectUsed_rec( Vec_Set_t * vProof, int hNode, Vec_Int_t * vUsed )
 {
     satset * pNext, * pNode = Proof_NodeRead( vProof, hNode );
     int i;
@@ -277,19 +219,14 @@ void Proof_CollectUsed_rec( Vec_Int_t * vProof, int hNode, Vec_Int_t * vUsed )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Proof_CollectUsedRec( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hRoot )
+Vec_Int_t * Proof_CollectUsedRec( Vec_Set_t * vProof, Vec_Int_t * vRoots )
 {
     Vec_Int_t * vUsed;
-    assert( (hRoot > 0) ^ (vRoots != NULL) );
+    int i, Entry;
     vUsed = Vec_IntAlloc( 1000 );
-    if ( hRoot )
-        Proof_CollectUsed_rec( vProof, hRoot, vUsed );
-    else
-    {
-        int i, Entry;
-        Vec_IntForEachEntry( vRoots, Entry, i )
+    Vec_IntForEachEntry( vRoots, Entry, i )
+        if ( Entry >= 0 )
             Proof_CollectUsed_rec( vProof, Entry, vUsed );
-    }
     return vUsed;
 }
 
@@ -307,7 +244,7 @@ Vec_Int_t * Proof_CollectUsedRec( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hR
   SeeAlso     []
 
 ***********************************************************************/
-void Sat_ProofReduceCheck_rec( Vec_Int_t * vProof, Vec_Int_t * vClauses, satset * pNode, int hClausePivot, Vec_Ptr_t * vVisited )
+void Sat_ProofReduceCheck_rec( Vec_Set_t * vProof, Vec_Int_t * vClauses, satset * pNode, int hClausePivot, Vec_Ptr_t * vVisited )
 {
     satset * pFanin;
     int k;
@@ -323,7 +260,7 @@ void Sat_ProofReduceCheck_rec( Vec_Int_t * vProof, Vec_Int_t * vClauses, satset
 }
 void Sat_ProofReduceCheckOne( sat_solver2 * s, int iLearnt, Vec_Ptr_t * vVisited )
 {
-    Vec_Int_t * vProof   = (Vec_Int_t *)&s->proofs;
+    Vec_Set_t * vProof   = (Vec_Set_t *)&s->Proofs;
     Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
     Vec_Int_t * vRoots   = (Vec_Int_t *)&s->claProofs;
     int hProofNode = Vec_IntEntry( vRoots, iLearnt );
@@ -357,26 +294,24 @@ void Sat_ProofReduceCheck( sat_solver2 * s )
 ***********************************************************************/
 void Sat_ProofReduce( sat_solver2 * s )
 {
-    Vec_Int_t * vProof   = (Vec_Int_t *)&s->proofs;
+    Vec_Set_t * vProof   = (Vec_Set_t *)&s->Proofs;
     Vec_Int_t * vRoots   = (Vec_Int_t *)&s->claProofs;
     Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
 
     int fVerbose = 0;
     Vec_Int_t * vUsed;
     satset * pNode, * pFanin;
-    int i, k, hTemp, hNewHandle = 1, clk = clock();
+    int i, k, hTemp, clk = clock();
     static int TimeTotal = 0;
 
     // collect visited nodes
-    vUsed = Proof_CollectUsedIter( vProof, vRoots, 0 );
-//    printf( "The proof uses %d out of %d proof nodes (%.2f %%)\n", 
-//        Vec_IntSize(vUsed), Proof_CountAll(vProof), 
-//        100.0 * Vec_IntSize(vUsed) / Proof_CountAll(vProof) );
+    vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 );
 
     // relabel nodes to use smaller space
+    Vec_SetShrinkS( vProof, 1 );
     Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
     {
-        pNode->Id = hNewHandle; hNewHandle += Proof_NodeSize(pNode->nEnts);
+        pNode->Id = Vec_SetAppendS( vProof, 2+pNode->nEnts );
         Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k )
             if ( (pNode->pEnts[k] & 1) == 0 ) // proof node
                 pNode->pEnts[k] = (pFanin->Id << 2) | (pNode->pEnts[k] & 2);
@@ -384,26 +319,27 @@ void Sat_ProofReduce( sat_solver2 * s )
                 assert( (int*)pFanin >= Vec_IntArray(vClauses) && (int*)pFanin < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) );
     }
     // update roots
-    Proof_ForeachNodeVec( vRoots, vProof, pNode, i )
+    Proof_ForeachNodeVec1( vRoots, vProof, pNode, i )
         Vec_IntWriteEntry( vRoots, i, pNode->Id );
     // compact the nodes
     Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
     {
         hTemp = pNode->Id; pNode->Id = 0;
-        memmove( Vec_IntArray(vProof) + hTemp, pNode, sizeof(int)*Proof_NodeSize(pNode->nEnts) );
+        memmove( Vec_SetEntry(vProof, hTemp), pNode, sizeof(word)*Proof_NodeWordNum(pNode->nEnts) );
     }
+    Vec_SetWriteEntryNum( vProof, Vec_IntSize(vUsed) );
     Vec_IntFree( vUsed );
 
     // report the result
     if ( fVerbose )
     {
-        printf( "The proof was reduced from %10d to %10d integers (by %6.2f %%)  ", 
-            Vec_IntSize(vProof), hNewHandle, 100.0 * (Vec_IntSize(vProof) - hNewHandle) / Vec_IntSize(vProof) );
+        printf( "The proof was reduced from %6.2f Mb to %6.2f Mb (by %6.2f %%)  ", 
+            1.0 * Vec_SetMemory(vProof) / (1<<20), 1.0 * Vec_SetMemoryS(vProof) / (1<<20), 
+            100.0 * (Vec_SetMemory(vProof) - Vec_SetMemoryS(vProof)) / Vec_SetMemory(vProof) );
         TimeTotal += clock() - clk;
         Abc_PrintTime( 1, "Time", TimeTotal );
     }
-    Vec_IntShrink( vProof, hNewHandle );
-
+    Vec_SetShrink( vProof, Vec_SetHandCurrentS(vProof) );
     Sat_ProofReduceCheck( s );
 }
 
@@ -419,7 +355,7 @@ void Sat_ProofReduce( sat_solver2 * s )
   SeeAlso     []
 
 ***********************************************************************/
-int Sat_ProofCheckResolveOne( Vec_Rec_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp )
+int Sat_ProofCheckResolveOne( Vec_Set_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp )
 {
     satset * c;
     int h, i, k, Var = -1, Count = 0;
@@ -452,9 +388,9 @@ int Sat_ProofCheckResolveOne( Vec_Rec_t * p, satset * c1, satset * c2, Vec_Int_t
         if ( (c2->pEnts[i] >> 1) != Var )
             Vec_IntPushUnique( vTemp, c2->pEnts[i] );
     // create new resolution entry
-    h = Vec_RecPush( p, Vec_IntArray(vTemp), Vec_IntSize(vTemp) );
+    h = Vec_SetAppend( p, Vec_IntArray(vTemp), Vec_IntSize(vTemp) );
     // return the new entry
-    c = Proof_ResolveRead( p, h );
+    c = Proof_NodeRead( p, h );
     c->nEnts = Vec_IntSize(vTemp)-2;
     return h;
 }
@@ -470,15 +406,15 @@ int Sat_ProofCheckResolveOne( Vec_Rec_t * p, satset * c1, satset * c2, Vec_Int_t
   SeeAlso     []
 
 ***********************************************************************/
-satset * Sat_ProofCheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Rec_t * vResolves, int iAnt )
+satset * Sat_ProofCheckReadOne( Vec_Int_t * vClauses, Vec_Set_t * vProof, Vec_Set_t * vResolves, int iAnt )
 {
     satset * pAnt;
     if ( iAnt & 1 )
-        return Proof_NodeRead( vClauses, iAnt >> 2 );
+        return Proof_ClauseRead( vClauses, iAnt >> 2 );
     assert( iAnt > 0 );
     pAnt = Proof_NodeRead( vProof, iAnt >> 2 );
     assert( pAnt->Id > 0 );
-    return Proof_ResolveRead( vResolves, pAnt->Id );
+    return Proof_NodeRead( vResolves, pAnt->Id );
 }
 
 /**Function*************************************************************
@@ -495,24 +431,21 @@ satset * Sat_ProofCheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Re
 void Sat_ProofCheck( sat_solver2 * s )
 {
     Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
-    Vec_Int_t * vProof   = (Vec_Int_t *)&s->proofs;
-    Vec_Rec_t * vResolves;
+    Vec_Set_t * vProof   = (Vec_Set_t *)&s->Proofs;
+    Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots;
+    Vec_Set_t * vResolves;
     Vec_Int_t * vUsed, * vTemp;
     satset * pSet, * pSet0, * pSet1;
     int i, k, hRoot, Handle, Counter = 0, clk = clock(); 
-//    if ( s->hLearntLast < 0 )
-//        return;
-//    hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
     hRoot = s->hProofLast;
     if ( hRoot == -1 )
         return;
-
     // collect visited clauses
-    vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
+    vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 );
     Proof_CleanCollected( vProof, vUsed );
     // perform resolution steps
     vTemp = Vec_IntAlloc( 1000 );
-    vResolves = Vec_RecAlloc();
+    vResolves = Vec_SetAlloc();
     Proof_ForeachNodeVec( vUsed, vProof, pSet, i )
     {
         pSet0 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] );
@@ -520,25 +453,23 @@ void Sat_ProofCheck( sat_solver2 * s )
         {
             pSet1  = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] );
             Handle = Sat_ProofCheckResolveOne( vResolves, pSet0, pSet1, vTemp );
-            pSet0  = Proof_ResolveRead( vResolves, Handle );
+            pSet0  = Proof_NodeRead( vResolves, Handle );
         }
         pSet->Id = Handle;
-//printf( "Clause for proof %d: ", Vec_IntEntry(vUsed, i) );
-//satset_print( pSet0 );
         Counter++;
     }
     Vec_IntFree( vTemp );
     // clean the proof
     Proof_CleanCollected( vProof, vUsed );
     // compare the final clause
-    printf( "Used %6.2f Mb for resolvents.\n", 4.0 * Vec_RecSize(vResolves) / (1<<20) );
+    printf( "Used %6.2f Mb for resolvents.\n", 1.0 * Vec_SetMemory(vResolves) / (1<<20) );
     if ( pSet0->nEnts > 0 )
         printf( "Derived clause with %d lits instead of the empty clause.  ", pSet0->nEnts );
     else
         printf( "Proof verification successful.  " );
     Abc_PrintTime( 1, "Time", clock() - clk );
     // cleanup
-    Vec_RecFree( vResolves );
+    Vec_SetFree( vResolves );
     Vec_IntFree( vUsed );
 }
 
@@ -554,7 +485,7 @@ void Sat_ProofCheck( sat_solver2 * s )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vUsed, int fUseIds )
+Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Set_t * vProof, Vec_Int_t * vUsed, int fUseIds )
 {
     Vec_Int_t * vCore;
     satset * pNode, * pFanin;
@@ -571,12 +502,11 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_
             }
     }
     // clean core clauses and reexpress core in terms of clause IDs
-    Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
+    Proof_ForeachClauseVec( vCore, vClauses, pNode, i )
     {
         assert( (int*)pNode < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) );
         pNode->mark = 0;
         if ( fUseIds )
-//            Vec_IntWriteEntry( vCore, i, pNode->Id - 1 );
             Vec_IntWriteEntry( vCore, i, pNode->Id );
     }
     return vCore;
@@ -644,8 +574,9 @@ void Sat_ProofInterpolantCheckVars( sat_solver2 * s, Vec_Int_t * vGloVars )
 void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
 {
     Vec_Int_t * vClauses  = (Vec_Int_t *)&s->clauses;
-    Vec_Int_t * vProof    = (Vec_Int_t *)&s->proofs;
+    Vec_Set_t * vProof    = (Vec_Set_t *)&s->Proofs;
     Vec_Int_t * vGlobVars = (Vec_Int_t *)pGloVars;
+    Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots;
     Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap;
     satset * pNode, * pFanin;
     Aig_Man_t * pAig;
@@ -661,7 +592,7 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
     Sat_ProofInterpolantCheckVars( s, vGlobVars );
 
     // collect visited nodes
-    vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
+    vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 );
     // collect core clauses (cleans vUsed and vCore)
     vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 0 );
 
@@ -678,7 +609,7 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
 
     // copy the numbers out and derive interpol for clause
     vCoreNums = Vec_IntAlloc( Vec_IntSize(vCore) );
-    Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
+    Proof_ForeachClauseVec( vCore, vClauses, pNode, i )
     {
         if ( pNode->partA )
         {
@@ -719,7 +650,7 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
     Aig_ManCleanup( pAig );
 
     // move the results back
-    Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
+    Proof_ForeachClauseVec( vCore, vClauses, pNode, i )
         pNode->Id = Vec_IntEntry( vCoreNums, i );
     Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
         pNode->Id = 0;
@@ -745,8 +676,9 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
 word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
 {
     Vec_Int_t * vClauses  = (Vec_Int_t *)&s->clauses;
-    Vec_Int_t * vProof    = (Vec_Int_t *)&s->proofs;
+    Vec_Set_t * vProof    = (Vec_Set_t *)&s->Proofs;
     Vec_Int_t * vGlobVars = (Vec_Int_t *)pGloVars;
+    Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots;
     Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap;
     satset * pNode, * pFanin;
     Tru_Man_t * pTru;
@@ -755,9 +687,6 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
     word * pRes = ABC_ALLOC( word, nWords );
     int i, k, iVar, Lit, Entry, hRoot;
     assert( nVars > 0 && nVars <= 16 );
-//    if ( s->hLearntLast < 0 )
-//        return NULL;
-//    hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
     hRoot = s->hProofLast;
     if ( hRoot == -1 )
         return NULL;
@@ -765,7 +694,7 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
     Sat_ProofInterpolantCheckVars( s, vGlobVars );
 
     // collect visited nodes
-    vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
+    vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 );
     // collect core clauses (cleans vUsed and vCore)
     vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 0 );
 
@@ -779,7 +708,7 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
 
     // copy the numbers out and derive interpol for clause
     vCoreNums = Vec_IntAlloc( Vec_IntSize(vCore) );
-    Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
+    Proof_ForeachClauseVec( vCore, vClauses, pNode, i )
     {
         if ( pNode->partA )
         {
@@ -808,7 +737,7 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
         Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k )
         {
 //            assert( pFanin->Id < 2*Aig_ManObjNumMax(pAig) );
-            assert( pFanin->Id <= Tru_ManHandleMax(pTru) );
+//            assert( pFanin->Id <= Tru_ManHandleMax(pTru) );
             if ( k == 0 )
 //                pObj = Aig_ObjFromLit( pAig, pFanin->Id );
                 pRes = Tru_ManCopyNotCond( pRes, Tru_ManFunc(pTru, pFanin->Id & ~1), nWords, pFanin->Id & 1 );
@@ -829,7 +758,7 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
 //    Aig_ManCleanup( pAig );
 
     // move the results back
-    Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
+    Proof_ForeachClauseVec( vCore, vClauses, pNode, i )
         pNode->Id = Vec_IntEntry( vCoreNums, i );
     Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
         pNode->Id = 0;
@@ -856,18 +785,15 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
 void * Sat_ProofCore( sat_solver2 * s )
 {
     Vec_Int_t * vClauses  = (Vec_Int_t *)&s->clauses;
-    Vec_Int_t * vProof    = (Vec_Int_t *)&s->proofs;
+    Vec_Set_t * vProof    = (Vec_Set_t *)&s->Proofs;
+    Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots;
     Vec_Int_t * vCore, * vUsed;
     int hRoot;
-//    if ( s->hLearntLast < 0 )
-//        return NULL;
-//    hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
     hRoot = s->hProofLast;
     if ( hRoot == -1 )
         return NULL;
-
     // collect visited clauses
-    vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
+    vUsed = Proof_CollectUsedIter( vProof, vRoots, 0 );
     // collect core clauses 
     vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 1 );
     Vec_IntFree( vUsed );
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 8a3cbc33..181d152a 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -71,11 +71,6 @@ static inline int irand(double* seed, int size) {
 
 
 //=================================================================================================
-// Predeclarations:
-
-static void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *));
-
-//=================================================================================================
 // Variable datatype + minor functions:
 
 static const int var0  = 1;
@@ -90,12 +85,12 @@ struct varinfo_t
     unsigned lev    : 28;  // variable level
 };
 
-static inline int     var_level     (sat_solver* s, int v)            { return s->levels[v]; }
-static inline int     var_value     (sat_solver* s, int v)            { return s->assigns[v]; }
+static inline int     var_level     (sat_solver* s, int v)            { return s->levels[v];   }
+static inline int     var_value     (sat_solver* s, int v)            { return s->assigns[v];  }
 static inline int     var_polar     (sat_solver* s, int v)            { return s->polarity[v]; }
 
-static inline void    var_set_level (sat_solver* s, int v, int lev)   { s->levels[v] = lev;  }
-static inline void    var_set_value (sat_solver* s, int v, int val)   { s->assigns[v] = val;  }
+static inline void    var_set_level (sat_solver* s, int v, int lev)   { s->levels[v] = lev;    }
+static inline void    var_set_value (sat_solver* s, int v, int val)   { s->assigns[v] = val;   }
 static inline void    var_set_polar (sat_solver* s, int v, int pol)   { s->polarity[v] = pol;  }
 
 // variable tags
@@ -130,7 +125,7 @@ int sat_solver_get_var_value(sat_solver* s, int v)
     assert( 0 );
     return 0;
 }
-
+ 
 //=================================================================================================
 // Clause datatype + minor functions:
 
@@ -140,6 +135,8 @@ struct clause_t
     lit lits[0];
 };
 
+static inline clause*  clause_read         (sat_solver* s, int h)  { return (clause *)Vec_SetEntry(&s->Mem, h>>1);     }
+
 static inline int      clause_nlits        (clause* c)             { return c->size_learnt >> 1;                       }
 static inline lit*     clause_begin        (clause* c)             { return c->lits;                                   }
 static inline int      clause_learnt       (clause* c)             { return c->size_learnt & 1;                        }
@@ -155,21 +152,18 @@ static inline void     clause_print        (clause* c)             {
     printf( "}\n" );
 }
 
-static inline clause* clause_read( sat_solver* s, int h )          { return (clause *)Vec_RecEntryP(&s->Mem, h);       }
-static inline int     clause_size( int nLits, int fLearnt )        { int a = nLits + fLearnt + 1; return a + (a & 1);  }
-
 //=================================================================================================
 // Encode literals in clause pointers:
 
-static inline int     clause_from_lit (lit l)       { return l + l + 1;                            }
-static inline int     clause_is_lit   (int h)       { return (h & 1);                              }
-static inline lit     clause_read_lit (int h)       { return (lit)(h >> 1);                        }
+static inline int      clause_from_lit (lit l)       { return l + l + 1;                            }
+static inline int      clause_is_lit   (int h)       { return (h & 1);                              }
+static inline lit      clause_read_lit (int h)       { return (lit)(h >> 1);                        }
 
 //=================================================================================================
 // Simple helpers:
 
-static inline int     sat_solver_dl(sat_solver* s)                { return veci_size(&s->trail_lim); }
-static inline veci*   sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l];            }
+static inline int      sat_solver_dl(sat_solver* s)                { return veci_size(&s->trail_lim); }
+static inline veci*    sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l];            }
 
 //=================================================================================================
 // Variable order functions:
@@ -418,15 +412,6 @@ static void sortrnd(void** array, int size, int(*comp)(const void *, const void
     }
 }
 
-void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *))
-{
-//    int i;
-    double seed = 91648253;
-    sortrnd(array,size,comp,&seed);
-//    for ( i = 1; i < size; i++ )
-//        assert(comp(array[i-1], array[i])<0);
-}
-
 //=================================================================================================
 // Clause functions:
 
@@ -451,9 +436,9 @@ static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
     }
 
     // create new clause
-    h = Vec_RecAppend( &s->Mem, clause_size(size, learnt) );
-    c = clause_read( s, h );
+    h = Vec_SetAppend( &s->Mem, NULL, size + learnt + 1 ) << 1;
     assert( !(h & 1) );
+    c = clause_read( s, h );
     if ( s->hLearnts == -1 && learnt )
         s->hLearnts = h;
     c->size_learnt = (size << 1) | learnt;
@@ -927,9 +912,9 @@ sat_solver* sat_solver_new(void)
 {
     sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver));
 
-    Vec_RecAlloc_(&s->Mem);
+    Vec_SetAlloc_(&s->Mem);
     s->hLearnts = -1;
-    s->hBinary = Vec_RecAppend( &s->Mem, clause_size(2, 0) );
+    s->hBinary = Vec_SetAppend( &s->Mem, NULL, 3 ) << 1;
     s->binary = clause_read( s, s->hBinary );
     s->binary->size_learnt = (2 << 1);
 
@@ -1049,7 +1034,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
 
 void sat_solver_delete(sat_solver* s)
 {
-    Vec_RecFree_( &s->Mem );
+    Vec_SetFree_( &s->Mem );
 
     // delete vectors
     veci_delete(&s->order);
@@ -1087,10 +1072,10 @@ void sat_solver_delete(sat_solver* s)
 void sat_solver_rollback( sat_solver* s )
 {
     int i;
-    Vec_RecRestart( &s->Mem );
+    Vec_SetRestart( &s->Mem );
 
     s->hLearnts = -1;
-    s->hBinary = Vec_RecAppend( &s->Mem, clause_size(2, 0) );
+    s->hBinary = Vec_SetAppend( &s->Mem, NULL, 3 ) << 1;
     s->binary = clause_read( s, s->hBinary );
     s->binary->size_learnt = (2 << 1);
 
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 30b3742b..de102227 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -29,7 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <assert.h>
 
 #include "satVec.h"
-#include "vecRec.h"
+#include "vecSet.h"
 
 ABC_NAMESPACE_HEADER_START
 
@@ -92,7 +92,7 @@ struct sat_solver_t
     int         qtail;         // Tail index of queue.
 
     // clauses
-    Vec_Rec_t   Mem;
+    Vec_Set_t   Mem;
     int         hLearnts;      // the first learnt clause
     int         hBinary;       // the special binary clause
     clause *    binary;
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 5a54a64e..34908f13 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -172,10 +172,12 @@ static inline void proof_chain_start( sat_solver2* s, satset* c )
 {
     if ( s->fProofLogging )
     {
-        s->iStartChain = veci_size(&s->proofs);
-        veci_push(&s->proofs, 0);
-        veci_push(&s->proofs, 0);
-        veci_push(&s->proofs, clause_proofid(s, c, 0) );
+        int ProofId = clause_proofid(s, c, 0);
+        assert( ProofId > 0 );
+        veci_resize( &s->temp_proof, 0 );
+        veci_push( &s->temp_proof, 0 );
+        veci_push( &s->temp_proof, 0 );
+        veci_push( &s->temp_proof, ProofId );
     }
 }
 
@@ -183,12 +185,10 @@ static inline void proof_chain_resolve( sat_solver2* s, satset* cls, int Var )
 {
     if ( s->fProofLogging )
     {
-//        int CapOld = (&s->proofs)->cap;
         satset* c = cls ? cls : var_unit_clause( s, Var );
-        veci_push(&s->proofs, clause_proofid(s, c, var_is_partA(s,Var)) );
-//        printf( "%d %d  ", clause_proofid(s, c), Var );
-//        if ( (&s->proofs)->cap > CapOld )
-//            printf( "Resized proof from %d to %d.\n", CapOld, (&s->proofs)->cap );
+        int ProofId = clause_proofid(s, c, var_is_partA(s,Var));
+        assert( ProofId > 0 );
+        veci_push( &s->temp_proof, ProofId );
     }
 }
 
@@ -196,12 +196,10 @@ static inline int proof_chain_stop( sat_solver2* s )
 {
     if ( s->fProofLogging )
     {
-        int RetValue = s->iStartChain;
-        satset* c = (satset*)(veci_begin(&s->proofs) + s->iStartChain);
-        assert( s->iStartChain > 0 && s->iStartChain < veci_size(&s->proofs) );
-        c->nEnts = veci_size(&s->proofs) - s->iStartChain - 2;
-        s->iStartChain = 0;
-        return RetValue;
+        int h = Vec_SetAppend( &s->Proofs, veci_begin(&s->temp_proof), veci_size(&s->temp_proof) );
+        satset * c = (satset *)Vec_SetEntry( &s->Proofs, h );
+        c->nEnts = veci_size(&s->temp_proof) - 2;
+        return h;
     }
     return 0;
 }
@@ -1119,20 +1117,6 @@ sat_solver2* sat_solver2_new(void)
 {
     sat_solver2* s = (sat_solver2 *)ABC_CALLOC( char, sizeof(sat_solver2) );
 
-    // initialize vectors
-    veci_new(&s->order);
-    veci_new(&s->trail_lim);
-    veci_new(&s->tagged);
-    veci_new(&s->stack);
-    veci_new(&s->temp_clause);
-    veci_new(&s->conf_final);
-    veci_new(&s->mark_levels);
-    veci_new(&s->min_lit_order); 
-    veci_new(&s->min_step_order);
-    veci_new(&s->learnt_live);
-    veci_new(&s->claActs);    veci_push(&s->claActs,   -1);
-    veci_new(&s->claProofs);  veci_push(&s->claProofs, -1);
-
 #ifdef USE_FLOAT_ACTIVITY2
     s->var_inc        = 1;
     s->cla_inc        = 1;
@@ -1156,6 +1140,23 @@ sat_solver2* sat_solver2_new(void)
     s->nLearntMax     =  0;
     s->fVerbose       =  0;
 
+    // initialize vectors
+    veci_new(&s->order);
+    veci_new(&s->trail_lim);
+    veci_new(&s->tagged);
+    veci_new(&s->stack);
+    veci_new(&s->temp_clause);
+    veci_new(&s->temp_proof);
+    veci_new(&s->conf_final);
+    veci_new(&s->mark_levels);
+    veci_new(&s->min_lit_order); 
+    veci_new(&s->min_step_order);
+    veci_new(&s->learnt_live);
+    veci_new(&s->claActs);    veci_push(&s->claActs,   -1);
+    veci_new(&s->claProofs);  veci_push(&s->claProofs, -1);
+    if ( s->fProofLogging )
+        Vec_SetAlloc_( &s->Proofs );
+
     // prealloc clause
     assert( !s->clauses.ptr );
     s->clauses.cap = (1 << 20);
@@ -1166,21 +1167,17 @@ sat_solver2* sat_solver2_new(void)
     s->learnts.cap = (1 << 20);
     s->learnts.ptr = ABC_ALLOC( int, s->learnts.cap );
     veci_push(&s->learnts, -1);
-    // prealloc proofs
-    if ( s->fProofLogging )
-    {
-        assert( !s->proofs.ptr );
-        s->proofs.cap = (1 << 20);
-        s->proofs.ptr = ABC_ALLOC( int, s->proofs.cap );
-        veci_push(&s->proofs, -1);
-    }
+
     // initialize clause pointers
-    s->hLearntLast    = -1; // the last learnt clause 
-    s->hProofLast     = -1; // the last proof ID
-    s->hClausePivot   =  1; // the pivot among clauses
-    s->hLearntPivot   =  1; // the pivot moang learned clauses
-    s->iVarPivot      =  0; // the pivot among the variables
-    s->iSimpPivot     =  0; // marker of unit-clauses
+    s->hLearntLast            = -1; // the last learnt clause 
+    s->hProofLast             = -1; // the last proof ID
+    // initialize rollback
+    s->iVarPivot              =  0; // the pivot for variables
+    s->iTrailPivot            =  0; // the pivot for trail
+    s->iProofPivot            =  0; // the pivot for proof records
+    s->hClausePivot           =  1; // the pivot for problem clause
+    s->hLearntPivot           =  1; // the pivot for learned clause
+    s->hProofPivot            =  1; // the pivot for proof records
     return s;
 }
 
@@ -1241,35 +1238,38 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
 
 void sat_solver2_delete(sat_solver2* s)
 {
-//    veci * pCore;
+    int fVerify = 0;
+    if ( fVerify )
+    {
+        veci * 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 ); 
+        if ( s->fProofLogging )
+            Sat_ProofCheck( s );
+    }
 
     // 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 ); 
+    printf( "Used %6.2f Mb for proof-logging.   Unit clauses = %d.\n", 1.0 * Vec_SetMemory(&s->Proofs) / (1<<20), s->nUnits );
 
-    if ( s->fProofLogging )
-        Sat_ProofCheck( s );
-*/
     // delete vectors
     veci_delete(&s->order);
     veci_delete(&s->trail_lim);
     veci_delete(&s->tagged);
     veci_delete(&s->stack);
     veci_delete(&s->temp_clause);
+    veci_delete(&s->temp_proof);
     veci_delete(&s->conf_final);
     veci_delete(&s->mark_levels);
     veci_delete(&s->min_lit_order);
     veci_delete(&s->min_step_order);
     veci_delete(&s->learnt_live);
-    veci_delete(&s->proofs);
     veci_delete(&s->claActs);
     veci_delete(&s->claProofs);
     veci_delete(&s->clauses);
     veci_delete(&s->learnts);
+//    veci_delete(&s->proofs);
+    Vec_SetFree_( &s->Proofs );
 
     // delete arrays
     if (s->vi != 0){
@@ -1514,11 +1514,13 @@ void sat_solver2_rollback( sat_solver2* s )
 {
     int i, k, j;
     assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size );
-    assert( s->iSimpPivot >= 0 && s->iSimpPivot <= s->qtail );
+    assert( s->iTrailPivot >= 0 && s->iTrailPivot <= s->qtail );
+    assert( s->iProofPivot >= 0 && s->iProofPivot <= Vec_SetEntryNum(&s->Proofs) );
     assert( s->hClausePivot >= 1 && s->hClausePivot <= veci_size(&s->clauses) );
     assert( s->hLearntPivot >= 1 && s->hLearntPivot <= veci_size(&s->learnts) );
+    assert( s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(&s->Proofs) );
     // reset implication queue
-    solver2_canceluntil_rollback( s, s->iSimpPivot );
+    solver2_canceluntil_rollback( s, s->iTrailPivot );
     // update order 
     if ( s->iVarPivot < s->size )
     { 
@@ -1558,7 +1560,9 @@ void sat_solver2_rollback( sat_solver2* s )
         veci_resize(&s->claActs,   first->Id);
         if ( s->fProofLogging ) {
             veci_resize(&s->claProofs, first->Id);
-            Sat_ProofReduce( s );
+            Vec_SetWriteEntryNum(&s->Proofs, s->iProofPivot);
+            Vec_SetShrink(&s->Proofs, s->hProofPivot);
+//            Sat_ProofReduce( s );
         }
         s->stats.learnts = first->Id-1;
         veci_resize(&s->learnts, s->hLearntPivot);
@@ -1600,12 +1604,16 @@ void sat_solver2_rollback( sat_solver2* s )
         s->stats.learnts_literals = 0;
         s->stats.tot_literals     = 0;
         // initialize clause pointers
-        s->hLearntLast    = -1; // the last learnt clause 
-        s->hProofLast     = -1; // the last proof ID
-        s->hClausePivot   =  1; // the pivot among clauses
-        s->hLearntPivot   =  1; // the pivot among learned clauses
-        s->iVarPivot      =  0; // the pivot among the variables
-        s->iSimpPivot     =  0; // marker of unit-clauses
+        s->hLearntLast            = -1; // the last learnt clause 
+        s->hProofLast             = -1; // the last proof ID
+
+        // initialize rollback
+        s->iVarPivot              =  0; // the pivot for variables
+        s->iTrailPivot            =  0; // the pivot for trail
+        s->iProofPivot            =  0; // the pivot for proof records
+        s->hClausePivot           =  1; // the pivot for problem clause
+        s->hLearntPivot           =  1; // the pivot for learned clause
+        s->hProofPivot            =  1; // the pivot for proof records
     }
 }
 
@@ -1803,7 +1811,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
         printf("==============================================================================\n");
 
     solver2_canceluntil(s,0);
-    assert( s->qhead == s->qtail );
+//    assert( s->qhead == s->qtail );
 //    if ( status == l_True )
 //        sat_solver2_verify( s );
     return status;
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index 4b1eec61..ffbae964 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -29,6 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <assert.h>
 
 #include "satVec.h"
+#include "vecSet.h"
 
 ABC_NAMESPACE_HEADER_START
 
@@ -112,16 +113,19 @@ struct sat_solver2_t
     veci            clauses;        // clause memory
     veci            learnts;        // learnt memory
     veci*           wlists;         // watcher lists (for each literal)
+    veci            claActs;        // clause activities
+    veci            claProofs;      // clause proofs
     int             hLearntLast;    // in proof-logging mode, the ID of the final conflict clause (conf_final)
     int             hProofLast;     // in proof-logging mode, the ID of the final conflict clause (conf_final)
-    int             hClausePivot;   // the pivot among problem clause
-    int             hLearntPivot;   // the pivot among learned clause
-    int             iVarPivot;      // the pivot among the variables
-    int             iSimpPivot;     // marker of unit-clauses
     int             nof_learnts;    // the number of clauses to trigger reduceDB
 
-    veci            claActs;        // clause activities
-    veci            claProofs;      // clause proofs
+    // rollback
+    int             iVarPivot;      // the pivot for variables
+    int             iTrailPivot;    // the pivot for trail
+    int             iProofPivot;    // the pivot for proof records
+    int             hClausePivot;   // the pivot for problem clause
+    int             hLearntPivot;   // the pivot for learned clause
+    int             hProofPivot;    // the pivot for proof records
 
     // internal state
     varinfo2 *      vi;             // variable information
@@ -146,8 +150,8 @@ struct sat_solver2_t
     veci            learnt_live;    // remaining clauses after reduce DB
 
     // proof logging
-    veci            proofs;         // sequence of proof records
-    int             iStartChain;    // temporary variable to remember beginning of the current chain in proof logging
+    Vec_Set_t       Proofs;         // sequence of proof records
+    veci            temp_proof;     // temporary place to store proofs
     int             nUnits;         // the total number of unit clauses
 
     // statistics
@@ -251,10 +255,12 @@ static inline int sat_solver2_set_learntmax(sat_solver2* s, int nLearntMax)
 static inline void sat_solver2_bookmark(sat_solver2* s)
 {
     assert( s->qhead == s->qtail );
-    s->hLearntPivot = veci_size(&s->learnts);
-    s->hClausePivot = veci_size(&s->clauses);
     s->iVarPivot    = s->size;
-    s->iSimpPivot   = s->qhead;
+    s->iTrailPivot  = s->qhead;
+    s->iProofPivot  = Vec_SetEntryNum(&s->Proofs);
+    s->hClausePivot = veci_size(&s->clauses);
+    s->hLearntPivot = veci_size(&s->learnts);
+    s->hProofPivot  = Vec_SetHandCurrent(&s->Proofs);
 }
 
 static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark )
diff --git a/src/sat/bsat/satSolver_old.c b/src/sat/bsat/satSolver_old.c
deleted file mode 100644
index 4d851d0f..00000000
--- a/src/sat/bsat/satSolver_old.c
+++ /dev/null
@@ -1,1766 +0,0 @@
-/**************************************************************************************************
-MiniSat -- Copyright (c) 2005, Niklas Sorensson
-http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
-
-Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
-associated documentation files (the "Software"), to deal in the Software without restriction,
-including without limitation the rights to use, copy, modify, merge, publish, distribute,
-sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in all copies or
-substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
-NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
-DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
-OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
-**************************************************************************************************/
-// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
-
-#include <stdio.h>
-#include <assert.h>
-#include <string.h>
-#include <math.h>
-
-#include "satSolver.h"
-#include "satStore.h"
-
-ABC_NAMESPACE_IMPL_START
-
-//#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-#define SAT_USE_ANALYZE_FINAL
-
-//=================================================================================================
-// Debug:
-
-//#define VERBOSEDEBUG
-
-// For derivation output (verbosity level 2)
-#define L_IND    "%-*d"
-#define L_ind    sat_solver_dl(s)*2+2,sat_solver_dl(s)
-#define L_LIT    "%sx%d"
-#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
-
-// Just like 'assert()' but expression will be evaluated in the release version as well.
-static inline void check(int expr) { assert(expr); }
-
-static void printlits(lit* begin, lit* end)
-{
-    int i;
-    for (i = 0; i < end - begin; i++)
-        printf(L_LIT" ",L_lit(begin[i]));
-}
-
-//=================================================================================================
-// Random numbers:
-
-
-// Returns a random float 0 <= x < 1. Seed must never be 0.
-static inline double drand(double* seed) {
-    int q;
-    *seed *= 1389796;
-    q = (int)(*seed / 2147483647);
-    *seed -= (double)q * 2147483647;
-    return *seed / 2147483647; }
-
-
-// Returns a random integer 0 <= x < size. Seed must never be 0.
-static inline int irand(double* seed, int size) {
-    return (int)(drand(seed) * size); }
-
-
-//=================================================================================================
-// Predeclarations:
-
-static void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *));
-
-//=================================================================================================
-// Clause datatype + minor functions:
-
-struct clause_t
-{
-    int size_learnt;
-    lit lits[0];
-};
-
-static inline int      clause_size         (clause* c)             { return c->size_learnt >> 1;                       }
-static inline lit*     clause_begin        (clause* c)             { return c->lits;                                   }
-static inline int      clause_learnt       (clause* c)             { return c->size_learnt & 1;                        }
-static inline float    clause_activity     (clause* c)             { return *((float*)&c->lits[c->size_learnt>>1]);    }
-static inline unsigned clause_activity2    (clause* c)             { return *((unsigned*)&c->lits[c->size_learnt>>1]); }
-static inline void     clause_setactivity  (clause* c, float a)    { *((float*)&c->lits[c->size_learnt>>1]) = a;       }
-static inline void     clause_setactivity2 (clause* c, unsigned a) { *((unsigned*)&c->lits[c->size_learnt>>1]) = a;    }
-static inline void     clause_print        (clause* c)             { 
-    int i;
-    printf( "{ " );
-    for ( i = 0; i < clause_size(c); i++ )
-        printf( "%d ", (clause_begin(c)[i] & 1)? -(clause_begin(c)[i] >> 1) : clause_begin(c)[i] >> 1 );
-    printf( "}\n" );
-}
-
-//=================================================================================================
-// Encode literals in clause pointers:
-
-static inline clause* clause_from_lit (lit l)     { return (clause*)((ABC_PTRUINT_T)l + (ABC_PTRUINT_T)l + 1);  }
-static inline int     clause_is_lit   (clause* c) { return ((ABC_PTRUINT_T)c & 1);                              }
-static inline lit     clause_read_lit (clause* c) { return (lit)((ABC_PTRUINT_T)c >> 1);                        }
-
-//=================================================================================================
-// Simple helpers:
-
-static inline int     sat_solver_dl(sat_solver* s)                { return veci_size(&s->trail_lim); }
-static inline vecp*   sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l];            }
-
-//=================================================================================================
-// Variable order functions:
-
-static inline void order_update(sat_solver* s, int v) // updateorder
-{
-    int*    orderpos = s->orderpos;
-    int*    heap     = veci_begin(&s->order);
-    int     i        = orderpos[v];
-    int     x        = heap[i];
-    int     parent   = (i - 1) / 2;
-
-    assert(s->orderpos[v] != -1);
-
-    while (i != 0 && s->activity[x] > s->activity[heap[parent]]){
-        heap[i]           = heap[parent];
-        orderpos[heap[i]] = i;
-        i                 = parent;
-        parent            = (i - 1) / 2;
-    }
-    heap[i]     = x;
-    orderpos[x] = i;
-}
-
-static inline void order_assigned(sat_solver* s, int v) 
-{
-}
-
-static inline void order_unassigned(sat_solver* s, int v) // undoorder
-{
-    int* orderpos = s->orderpos;
-    if (orderpos[v] == -1){
-        orderpos[v] = veci_size(&s->order);
-        veci_push(&s->order,v);
-        order_update(s,v);
-//printf( "+%d ", v );
-    }
-}
-
-static inline int  order_select(sat_solver* s, float random_var_freq) // selectvar
-{
-    int*    heap;
-    int*    orderpos;
-
-    lbool* values = s->assigns;
-
-    // Random decision:
-    if (drand(&s->random_seed) < random_var_freq){
-        int next = irand(&s->random_seed,s->size);
-        assert(next >= 0 && next < s->size);
-        if (values[next] == l_Undef)
-            return next;
-    }
-
-    // Activity based decision:
-
-    heap     = veci_begin(&s->order);
-    orderpos = s->orderpos;
-
-
-    while (veci_size(&s->order) > 0){
-        int    next  = heap[0];
-        int    size  = veci_size(&s->order)-1;
-        int    x     = heap[size];
-
-        veci_resize(&s->order,size);
-
-        orderpos[next] = -1;
-
-        if (size > 0){
-
-            int    i     = 0;
-            int    child = 1;
-
-
-            while (child < size){
-                if (child+1 < size && s->activity[heap[child]] < s->activity[heap[child+1]])
-                    child++;
-
-                assert(child < size);
-
-                if (s->activity[x] >= s->activity[heap[child]])
-                    break;
-
-                heap[i]           = heap[child];
-                orderpos[heap[i]] = i;
-                i                 = child;
-                child             = 2 * child + 1;
-            }
-            heap[i]           = x;
-            orderpos[heap[i]] = i;
-        }
-
-//printf( "-%d ", next );
-        if (values[next] == l_Undef)
-            return next;
-    }
-
-    return var_Undef;
-}
-
-//=================================================================================================
-// Activity functions:
-
-#ifdef USE_FLOAT_ACTIVITY
-
-static inline void act_var_rescale(sat_solver* s)  {
-    double* activity = s->activity;
-    int i;
-    for (i = 0; i < s->size; i++)
-        activity[i] *= 1e-100;
-    s->var_inc *= 1e-100;
-}
-static inline void act_clause_rescale(sat_solver* s) {
-    static int Total = 0;
-    clause** cs = (clause**)vecp_begin(&s->learnts);
-    int i, clk = clock();
-    for (i = 0; i < vecp_size(&s->learnts); i++){
-        float a = clause_activity(cs[i]);
-        clause_setactivity(cs[i], a * (float)1e-20);
-    }
-    s->cla_inc *= (float)1e-20;
-
-    Total += clock() - clk;
-    printf( "Rescaling...   Cla inc = %10.3f  Conf = %10d   ", s->cla_inc,  s->stats.conflicts );
-    Abc_PrintTime( 1, "Time", Total );
-}
-static inline void act_var_bump(sat_solver* s, int v) {
-    s->activity[v] += s->var_inc;
-    if (s->activity[v] > 1e100)
-        act_var_rescale(s);
-    if (s->orderpos[v] != -1)
-        order_update(s,v);
-}
-static inline void act_var_bump_global(sat_solver* s, int v) {
-    s->activity[v] += (s->var_inc * 3.0 * s->pGlobalVars[v]);
-    if (s->activity[v] > 1e100)
-        act_var_rescale(s);
-    if (s->orderpos[v] != -1)
-        order_update(s,v);
-}
-static inline void act_var_bump_factor(sat_solver* s, int v) {
-    s->activity[v] += (s->var_inc * s->factors[v]);
-    if (s->activity[v] > 1e100)
-        act_var_rescale(s);
-    if (s->orderpos[v] != -1)
-        order_update(s,v);
-}
-static inline void act_clause_bump(sat_solver* s, clause *c) {
-    float a = clause_activity(c) + s->cla_inc;
-    clause_setactivity(c,a);
-    if (a > 1e20) act_clause_rescale(s);
-}
-static inline void act_var_decay(sat_solver* s)    { s->var_inc *= s->var_decay; }
-static inline void act_clause_decay(sat_solver* s) { s->cla_inc *= s->cla_decay; }
-
-#else
-
-static inline void act_var_rescale(sat_solver* s) {
-    unsigned* activity = s->activity;
-    int i;
-    for (i = 0; i < s->size; i++)
-        activity[i] >>= 19;
-    s->var_inc >>= 19;
-    s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) );
-}
-static inline void act_clause_rescale(sat_solver* s) {
-    static int Total = 0;
-    clause** cs = (clause**)vecp_begin(&s->learnts);
-    int i, clk = clock();
-    for (i = 0; i < vecp_size(&s->learnts); i++){
-        unsigned a = clause_activity2(cs[i]);
-        clause_setactivity2(cs[i], a >> 14);
-    }
-    s->cla_inc >>= 14;
-    s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
-
-//    Total += clock() - clk;
-//    printf( "Rescaling...   Cla inc = %5d  Conf = %10d   ", s->cla_inc,  s->stats.conflicts );
-//    Abc_PrintTime( 1, "Time", Total );
-}
-static inline void act_var_bump(sat_solver* s, int v) {
-    s->activity[v] += s->var_inc;
-    if (s->activity[v] & 0x80000000)
-        act_var_rescale(s);
-    if (s->orderpos[v] != -1)
-        order_update(s,v);
-}
-static inline void act_var_bump_global(sat_solver* s, int v) {}
-static inline void act_var_bump_factor(sat_solver* s, int v) {}
-static inline void act_clause_bump(sat_solver* s, clause*c) {
-    unsigned a = clause_activity2(c) + s->cla_inc;
-    clause_setactivity2(c,a);
-    if (a & 0x80000000) 
-        act_clause_rescale(s);
-}
-static inline void act_var_decay(sat_solver* s)    { s->var_inc += (s->var_inc >>  4); }
-static inline void act_clause_decay(sat_solver* s) { s->cla_inc += (s->cla_inc >> 10); }
-
-#endif
-
-
-//=================================================================================================
-// Clause functions:
-
-/* pre: size > 1 && no variable occurs twice
- */
-static clause* clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
-{
-    int size;
-    clause* c;
-    int i;
-
-    assert(end - begin > 1);
-    assert(learnt >= 0 && learnt < 2);
-    size           = end - begin;
-
-    // do not allocate memory for the two-literal problem clause
-    if ( size == 2 && !learnt )
-    {
-        vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(clause_from_lit(begin[1])));
-        vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(clause_from_lit(begin[0])));
-        return NULL;
-    }
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-    c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
-#else
-    c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) );
-#endif
-
-    c->size_learnt = (size << 1) | learnt;
-    assert(((ABC_PTRUINT_T)c & 1) == 0);
-
-    for (i = 0; i < size; i++)
-        c->lits[i] = begin[i];
-
-    if (learnt)
-        *((float*)&c->lits[size]) = 0.0;
-
-    assert(begin[0] >= 0);
-    assert(begin[0] < s->size*2);
-    assert(begin[1] >= 0);
-    assert(begin[1] < s->size*2);
-
-    assert(lit_neg(begin[0]) < s->size*2);
-    assert(lit_neg(begin[1]) < s->size*2);
-
-    //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
-    //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
-
-    vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
-    vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
-
-    return c;
-}
-
-
-//=================================================================================================
-// Minor (solver) functions:
-
-static inline int sat_solver_enqueue(sat_solver* s, lit l, clause* from)
-{
-    lbool* values = s->assigns;
-    int    v      = lit_var(l);
-    lbool  val    = values[v];
-    lbool  sig;
-#ifdef VERBOSEDEBUG
-    printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
-#endif
-
-    sig = !lit_sign(l); sig += sig - 1;
-    if (val != l_Undef){
-        return val == sig;
-    }else{
-        int*     levels  = s->levels;
-        clause** reasons = s->reasons;
-        // New fact -- store it.
-#ifdef VERBOSEDEBUG
-        printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
-#endif
-        values [v] = sig;
-        levels [v] = sat_solver_dl(s);
-        reasons[v] = from;
-        s->trail[s->qtail++] = l;
-
-        order_assigned(s, v);
-        return true;
-    }
-}
-
-
-static inline int sat_solver_assume(sat_solver* s, lit l){
-    assert(s->qtail == s->qhead);
-    assert(s->assigns[lit_var(l)] == l_Undef);
-#ifdef VERBOSEDEBUG
-    printf(L_IND"assume("L_LIT")  ", L_ind, L_lit(l));
-    printf( "act = %.20f\n", s->activity[lit_var(l)] );
-#endif
-    veci_push(&s->trail_lim,s->qtail);
-    return sat_solver_enqueue(s,l,(clause*)0);
-}
-
-
-static void sat_solver_canceluntil(sat_solver* s, int level) {
-    lit*     trail;   
-    lbool*   values;  
-    clause** reasons; 
-    int      bound;
-    int      lastLev;
-    int      c;
-    
-    if (sat_solver_dl(s) <= level)
-        return;
-
-    trail   = s->trail;
-    values  = s->assigns;
-    reasons = s->reasons;
-    bound   = (veci_begin(&s->trail_lim))[level];
-    lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1];
-
-    ////////////////////////////////////////
-    // added to cancel all assignments
-//    if ( level == -1 )
-//        bound = 0;
-    ////////////////////////////////////////
-
-    for (c = s->qtail-1; c >= bound; c--) {
-        int     x  = lit_var(trail[c]);
-        values [x] = l_Undef;
-        reasons[x] = (clause*)0;
-        if ( c < lastLev )
-            s->polarity[x] = !lit_sign(trail[c]);
-    }
-
-    for (c = s->qhead-1; c >= bound; c--)
-        order_unassigned(s,lit_var(trail[c]));
-
-    s->qhead = s->qtail = bound;
-    veci_resize(&s->trail_lim,level);
-}
-
-static void sat_solver_record(sat_solver* s, veci* cls)
-{
-    lit*    begin = veci_begin(cls);
-    lit*    end   = begin + veci_size(cls);
-    clause* c     = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : (clause*)0;
-    sat_solver_enqueue(s,*begin,c);
-
-    ///////////////////////////////////
-    // add clause to internal storage
-    if ( s->pStore )
-    {
-        int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end );
-        assert( RetValue );
-    }
-    ///////////////////////////////////
-
-    assert(veci_size(cls) > 0);
-
-    if (c != 0) {
-        vecp_push(&s->learnts,c);
-        act_clause_bump(s,c);
-        s->stats.learnts++;
-        s->stats.learnts_literals += veci_size(cls);
-    }
-}
-
-
-static double sat_solver_progress(sat_solver* s)
-{
-    lbool*  values = s->assigns;
-    int*    levels = s->levels;
-    int     i;
-
-    double  progress = 0;
-    double  F        = 1.0 / s->size;
-    for (i = 0; i < s->size; i++)
-        if (values[i] != l_Undef)
-            progress += pow(F, levels[i]);
-    return progress / s->size;
-}
-
-//=================================================================================================
-// Major methods:
-
-static int sat_solver_lit_removable(sat_solver* s, lit l, int minl)
-{
-    lbool*   tags    = s->tags;
-    clause** reasons = s->reasons;
-    int*     levels  = s->levels;
-    int      top     = veci_size(&s->tagged);
-
-    assert(lit_var(l) >= 0 && lit_var(l) < s->size);
-    assert(reasons[lit_var(l)] != 0);
-    veci_resize(&s->stack,0);
-    veci_push(&s->stack,lit_var(l));
-
-    while (veci_size(&s->stack) > 0){
-        clause* c;
-        int v = veci_begin(&s->stack)[veci_size(&s->stack)-1];
-        assert(v >= 0 && v < s->size);
-        veci_resize(&s->stack,veci_size(&s->stack)-1);
-        assert(reasons[v] != 0);
-        c    = reasons[v];
-
-        if (clause_is_lit(c)){
-            int v = lit_var(clause_read_lit(c));
-            if (tags[v] == l_Undef && levels[v] != 0){
-                if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
-                    veci_push(&s->stack,v);
-                    tags[v] = l_True;
-                    veci_push(&s->tagged,v);
-                }else{
-                    int* tagged = veci_begin(&s->tagged);
-                    int j;
-                    for (j = top; j < veci_size(&s->tagged); j++)
-                        tags[tagged[j]] = l_Undef;
-                    veci_resize(&s->tagged,top);
-                    return false;
-                }
-            }
-        }else{
-            lit*    lits = clause_begin(c);
-            int     i, j;
-
-            for (i = 1; i < clause_size(c); i++){
-                int v = lit_var(lits[i]);
-                if (tags[v] == l_Undef && levels[v] != 0){
-                    if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
-
-                        veci_push(&s->stack,lit_var(lits[i]));
-                        tags[v] = l_True;
-                        veci_push(&s->tagged,v);
-                    }else{
-                        int* tagged = veci_begin(&s->tagged);
-                        for (j = top; j < veci_size(&s->tagged); j++)
-                            tags[tagged[j]] = l_Undef;
-                        veci_resize(&s->tagged,top);
-                        return false;
-                    }
-                }
-            }
-        }
-    }
-
-    return true;
-}
-
-
-/*_________________________________________________________________________________________________
-|
-|  analyzeFinal : (p : Lit)  ->  [void]
-|  
-|  Description:
-|    Specialized analysis procedure to express the final conflict in terms of assumptions.
-|    Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
-|    stores the result in 'out_conflict'.
-|________________________________________________________________________________________________@*/
-/*
-void Solver::analyzeFinal(Clause* confl, bool skip_first)
-{
-    // -- NOTE! This code is relatively untested. Please report bugs!
-    conflict.clear();
-    if (root_level == 0) return;
-
-    vec<char>& seen  = analyze_seen;
-    for (int i = skip_first ? 1 : 0; i < confl->size(); i++){
-        Var x = var((*confl)[i]);
-        if (level[x] > 0)
-            seen[x] = 1;
-    }
-
-    int start = (root_level >= trail_lim.size()) ? trail.size()-1 : trail_lim[root_level];
-    for (int i = start; i >= trail_lim[0]; i--){
-        Var     x = var(trail[i]);
-        if (seen[x]){
-            GClause r = reason[x];
-            if (r == GClause_NULL){
-                assert(level[x] > 0);
-                conflict.push(~trail[i]);
-            }else{
-                if (r.isLit()){
-                    Lit p = r.lit();
-                    if (level[var(p)] > 0)
-                        seen[var(p)] = 1;
-                }else{
-                    Clause& c = *r.clause();
-                    for (int j = 1; j < c.size(); j++)
-                        if (level[var(c[j])] > 0)
-                            seen[var(c[j])] = 1;
-                }
-            }
-            seen[x] = 0;
-        }
-    }
-}
-*/
-
-#ifdef SAT_USE_ANALYZE_FINAL
-
-static void sat_solver_analyze_final(sat_solver* s, clause* conf, int skip_first)
-{
-    int i, j, start;
-    veci_resize(&s->conf_final,0);
-    if ( s->root_level == 0 )
-        return;
-    assert( veci_size(&s->tagged) == 0 );
-//    assert( s->tags[lit_var(p)] == l_Undef );
-//    s->tags[lit_var(p)] = l_True;
-    for (i = skip_first ? 1 : 0; i < clause_size(conf); i++)
-    {
-        int x = lit_var(clause_begin(conf)[i]);
-        if (s->levels[x] > 0)
-        {
-            s->tags[x] = l_True;
-            veci_push(&s->tagged,x);
-        }
-    }
-
-    start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->root_level];
-    for (i = start; i >= (veci_begin(&s->trail_lim))[0]; i--){
-        int x = lit_var(s->trail[i]);
-        if (s->tags[x] == l_True){
-            if (s->reasons[x] == NULL){
-                assert(s->levels[x] > 0);
-                veci_push(&s->conf_final,lit_neg(s->trail[i]));
-            }else{
-                clause* c = s->reasons[x];
-                if (clause_is_lit(c)){
-                    lit q = clause_read_lit(c);
-                    assert(lit_var(q) >= 0 && lit_var(q) < s->size);
-                    if (s->levels[lit_var(q)] > 0)
-                    {
-                        s->tags[lit_var(q)] = l_True;
-                        veci_push(&s->tagged,lit_var(q));
-                    }
-                }
-                else{
-                    int* lits = clause_begin(c);
-                    for (j = 1; j < clause_size(c); j++)
-                        if (s->levels[lit_var(lits[j])] > 0)
-                        {
-                            s->tags[lit_var(lits[j])] = l_True;
-                            veci_push(&s->tagged,lit_var(lits[j]));
-                        }
-                }
-            }
-        }
-    }
-    for (i = 0; i < veci_size(&s->tagged); i++)
-        s->tags[veci_begin(&s->tagged)[i]] = l_Undef;
-    veci_resize(&s->tagged,0);
-}
-
-#endif
-
-
-static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
-{
-    lit*     trail   = s->trail;
-    lbool*   tags    = s->tags;
-    clause** reasons = s->reasons;
-    int*     levels  = s->levels;
-    int      cnt     = 0;
-    lit      p       = lit_Undef;
-    int      ind     = s->qtail-1;
-    lit*     lits;
-    int      i, j, minl;
-    int*     tagged;
-
-    veci_push(learnt,lit_Undef);
-
-    do{
-        assert(c != 0);
-
-        if (clause_is_lit(c)){
-            lit q = clause_read_lit(c);
-            assert(lit_var(q) >= 0 && lit_var(q) < s->size);
-            if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
-                tags[lit_var(q)] = l_True;
-                veci_push(&s->tagged,lit_var(q));
-                act_var_bump(s,lit_var(q));
-                if (levels[lit_var(q)] == sat_solver_dl(s))
-                    cnt++;
-                else
-                    veci_push(learnt,q);
-            }
-        }else{
-
-            if (clause_learnt(c))
-                act_clause_bump(s,c);
-
-            lits = clause_begin(c);
-            //printlits(lits,lits+clause_size(c)); printf("\n");
-            for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){
-                lit q = lits[j];
-                assert(lit_var(q) >= 0 && lit_var(q) < s->size);
-                if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
-                    tags[lit_var(q)] = l_True;
-                    veci_push(&s->tagged,lit_var(q));
-                    act_var_bump(s,lit_var(q));
-                    if (levels[lit_var(q)] == sat_solver_dl(s))
-                        cnt++;
-                    else
-                        veci_push(learnt,q);
-                }
-            }
-        }
-
-        while (tags[lit_var(trail[ind--])] == l_Undef);
-
-        p = trail[ind+1];
-        c = reasons[lit_var(p)];
-        cnt--;
-
-    }while (cnt > 0);
-
-    *veci_begin(learnt) = lit_neg(p);
-
-    lits = veci_begin(learnt);
-    minl = 0;
-    for (i = 1; i < veci_size(learnt); i++){
-        int lev = levels[lit_var(lits[i])];
-        minl    |= 1 << (lev & 31);
-    }
-
-    // simplify (full)
-    for (i = j = 1; i < veci_size(learnt); i++){
-        if (reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lits[i],minl))
-            lits[j++] = lits[i];
-    }
-
-    // update size of learnt + statistics
-    veci_resize(learnt,j);
-    s->stats.tot_literals += j;
-
-    // clear tags
-    tagged = veci_begin(&s->tagged);
-    for (i = 0; i < veci_size(&s->tagged); i++)
-        tags[tagged[i]] = l_Undef;
-    veci_resize(&s->tagged,0);
-
-#ifdef DEBUG
-    for (i = 0; i < s->size; i++)
-        assert(tags[i] == l_Undef);
-#endif
-
-#ifdef VERBOSEDEBUG
-    printf(L_IND"Learnt {", L_ind);
-    for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i]));
-#endif
-    if (veci_size(learnt) > 1){
-        int max_i = 1;
-        int max   = levels[lit_var(lits[1])];
-        lit tmp;
-
-        for (i = 2; i < veci_size(learnt); i++)
-            if (levels[lit_var(lits[i])] > max){
-                max   = levels[lit_var(lits[i])];
-                max_i = i;
-            }
-
-        tmp         = lits[1];
-        lits[1]     = lits[max_i];
-        lits[max_i] = tmp;
-    }
-#ifdef VERBOSEDEBUG
-    {
-        int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0;
-        printf(" } at level %d\n", lev);
-    }
-#endif
-}
-
-
-clause* sat_solver_propagate(sat_solver* s)
-{
-    lbool*  values = s->assigns;
-    clause* confl  = (clause*)0;
-    lit*    lits;
-    lit false_lit;
-    lbool sig;
-
-    //printf("sat_solver_propagate\n");
-    while (confl == 0 && s->qtail - s->qhead > 0){
-        lit  p  = s->trail[s->qhead++];
-        vecp* ws = sat_solver_read_wlist(s,p);
-        clause **begin = (clause**)vecp_begin(ws);
-        clause **end   = begin + vecp_size(ws);
-        clause **i, **j;
-
-        s->stats.propagations++;
-        s->simpdb_props--;
-
-        //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
-        for (i = j = begin; i < end; ){
-            if (clause_is_lit(*i)){
-
-                int Lit = clause_read_lit(*i);
-                sig = !lit_sign(Lit); sig += sig - 1;
-                if (values[lit_var(Lit)] == sig){
-                    *j++ = *i++;
-                    continue;
-                }
-
-                *j++ = *i;
-                if (!sat_solver_enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
-                    confl = s->binary;
-                    (clause_begin(confl))[1] = lit_neg(p);
-                    (clause_begin(confl))[0] = clause_read_lit(*i++);
-                    // Copy the remaining watches:
-                    while (i < end)
-                        *j++ = *i++;
-                }
-            }else{
-
-                lits = clause_begin(*i);
-
-                // Make sure the false literal is data[1]:
-                false_lit = lit_neg(p);
-                if (lits[0] == false_lit){
-                    lits[0] = lits[1];
-                    lits[1] = false_lit;
-                }
-                assert(lits[1] == false_lit);
-                //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n");
-
-                // If 0th watch is true, then clause is already satisfied.
-                sig = !lit_sign(lits[0]); sig += sig - 1;
-                if (values[lit_var(lits[0])] == sig){
-                    *j++ = *i;
-                }else{
-                    // Look for new watch:
-                    lit* stop = lits + clause_size(*i);
-                    lit* k;
-                    for (k = lits + 2; k < stop; k++){
-                        lbool sig = lit_sign(*k); sig += sig - 1;
-                        if (values[lit_var(*k)] != sig){
-                            lits[1] = *k;
-                            *k = false_lit;
-                            vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
-                            goto next; }
-                    }
-
-                    *j++ = *i;
-                    // Clause is unit under assignment:
-                    if (!sat_solver_enqueue(s,lits[0], *i)){
-                        confl = *i++;
-                        // Copy the remaining watches:
-                        while (i < end)
-                            *j++ = *i++;
-                    }
-                }
-            }
-        next:
-            i++;
-        }
-
-        s->stats.inspects += j - (clause**)vecp_begin(ws);
-        vecp_resize(ws,j - (clause**)vecp_begin(ws));
-    }
-
-    return confl;
-}
-
-//=================================================================================================
-// External solver functions:
-
-sat_solver* sat_solver_new(void)
-{
-    sat_solver* s = (sat_solver*)ABC_ALLOC( char, sizeof(sat_solver));
-    memset( s, 0, sizeof(sat_solver) );
-
-    // initialize vectors
-    vecp_new(&s->clauses);
-    vecp_new(&s->learnts);
-    veci_new(&s->order);
-    veci_new(&s->trail_lim);
-    veci_new(&s->tagged);
-    veci_new(&s->stack);
-    veci_new(&s->model);
-    veci_new(&s->act_vars);
-    veci_new(&s->temp_clause);
-    veci_new(&s->conf_final);
-
-    // initialize arrays
-    s->wlists    = 0;
-    s->activity  = 0;
-    s->factors   = 0;
-    s->assigns   = 0;
-    s->orderpos  = 0;
-    s->reasons   = 0;
-    s->levels    = 0;
-    s->tags      = 0;
-    s->trail     = 0;
-
-
-    // initialize other vars
-    s->size                   = 0;
-    s->cap                    = 0;
-    s->qhead                  = 0;
-    s->qtail                  = 0;
-#ifdef USE_FLOAT_ACTIVITY
-    s->var_inc                = 1;
-    s->cla_inc                = 1;
-    s->var_decay              = (float)(1 / 0.95  );
-    s->cla_decay              = (float)(1 / 0.999 );
-#else
-    s->var_inc                = (1 <<  5);
-    s->cla_inc                = (1 << 11);
-#endif
-    s->root_level             = 0;
-    s->simpdb_assigns         = 0;
-    s->simpdb_props           = 0;
-    s->random_seed            = 91648253;
-    s->progress_estimate      = 0;
-    s->binary                 = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2);
-    s->binary->size_learnt    = (2 << 1);
-    s->verbosity              = 0;
-
-    s->stats.starts           = 0;
-    s->stats.decisions        = 0;
-    s->stats.propagations     = 0;
-    s->stats.inspects         = 0;
-    s->stats.conflicts        = 0;
-    s->stats.clauses          = 0;
-    s->stats.clauses_literals = 0;
-    s->stats.learnts          = 0;
-    s->stats.learnts_literals = 0;
-    s->stats.tot_literals     = 0;
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-    s->pMem = NULL;
-#else
-    s->pMem = Sat_MmStepStart( 10 );
-#endif
-    return s;
-}
-
-void sat_solver_setnvars(sat_solver* s,int n)
-{
-    int var;
-
-    if (s->cap < n){
-        int old_cap = s->cap;
-        while (s->cap < n) s->cap = s->cap*2+1;
-
-        s->wlists    = ABC_REALLOC(vecp,   s->wlists,   s->cap*2);
-#ifdef USE_FLOAT_ACTIVITY
-        s->activity  = ABC_REALLOC(double,   s->activity, s->cap);
-#else
-        s->activity  = ABC_REALLOC(unsigned, s->activity, s->cap);
-#endif
-        s->factors   = ABC_REALLOC(double, s->factors,  s->cap);
-        s->assigns   = ABC_REALLOC(lbool,  s->assigns,  s->cap);
-        s->orderpos  = ABC_REALLOC(int,    s->orderpos, s->cap);
-        s->reasons   = ABC_REALLOC(clause*,s->reasons,  s->cap);
-        s->levels    = ABC_REALLOC(int,    s->levels,   s->cap);
-        s->tags      = ABC_REALLOC(lbool,  s->tags,     s->cap);
-        s->trail     = ABC_REALLOC(lit,    s->trail,    s->cap);
-        s->polarity  = ABC_REALLOC(char,   s->polarity, s->cap);
-        memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(vecp) );
-    }
-
-    for (var = s->size; var < n; var++){
-        assert(!s->wlists[2*var].size);
-        assert(!s->wlists[2*var+1].size);
-        if ( s->wlists[2*var].ptr == NULL )
-            vecp_new(&s->wlists[2*var]);
-        if ( s->wlists[2*var+1].ptr == NULL )
-            vecp_new(&s->wlists[2*var+1]);
-#ifdef USE_FLOAT_ACTIVITY
-        s->activity[var] = 0;
-#else
-        s->activity[var] = (1<<10);
-#endif
-        s->factors  [var] = 0;
-        s->assigns  [var] = l_Undef;
-        s->orderpos [var] = veci_size(&s->order);
-        s->reasons  [var] = (clause*)0;
-        s->levels   [var] = 0;
-        s->tags     [var] = l_Undef;
-        s->polarity [var] = 0;
-        
-        /* does not hold because variables enqueued at top level will not be reinserted in the heap
-           assert(veci_size(&s->order) == var); 
-         */
-        veci_push(&s->order,var);
-        order_update(s, var);
-    }
-
-    s->size = n > s->size ? n : s->size;
-}
-
-void sat_solver_delete(sat_solver* s)
-{
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-    int i;
-    for (i = 0; i < vecp_size(&s->clauses); i++)
-        ABC_FREE(vecp_begin(&s->clauses)[i]);
-    for (i = 0; i < vecp_size(&s->learnts); i++)
-        ABC_FREE(vecp_begin(&s->learnts)[i]);
-#else
-    Sat_MmStepStop( s->pMem, 0 );
-#endif
-
-    // delete vectors
-    vecp_delete(&s->clauses);
-    vecp_delete(&s->learnts);
-    veci_delete(&s->order);
-    veci_delete(&s->trail_lim);
-    veci_delete(&s->tagged);
-    veci_delete(&s->stack);
-    veci_delete(&s->model);
-    veci_delete(&s->act_vars);
-    veci_delete(&s->temp_clause);
-    veci_delete(&s->conf_final);
-    ABC_FREE(s->binary);
-
-    // delete arrays
-    if (s->wlists != 0){
-        int i;
-        for (i = 0; i < s->cap*2; i++)
-            vecp_delete(&s->wlists[i]);
-        ABC_FREE(s->wlists   );
-        ABC_FREE(s->activity );
-        ABC_FREE(s->factors  );
-        ABC_FREE(s->assigns  );
-        ABC_FREE(s->orderpos );
-        ABC_FREE(s->reasons  );
-        ABC_FREE(s->levels   );
-        ABC_FREE(s->trail    );
-        ABC_FREE(s->tags     );
-        ABC_FREE(s->polarity );
-    }
-
-    sat_solver_store_free(s);
-    ABC_FREE(s);
-}
-
-void sat_solver_rollback( sat_solver* s )
-{
-    int i;
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-    for (i = 0; i < vecp_size(&s->clauses); i++)
-        ABC_FREE(vecp_begin(&s->clauses)[i]);
-    for (i = 0; i < vecp_size(&s->learnts); i++)
-        ABC_FREE(vecp_begin(&s->learnts)[i]);
-#else
-    Sat_MmStepRestart( s->pMem );
-#endif
-    vecp_resize(&s->clauses, 0);
-    vecp_resize(&s->learnts, 0);
-    veci_resize(&s->trail_lim, 0);
-    veci_resize(&s->order, 0);
-    for ( i = 0; i < s->size*2; i++ )
-        s->wlists[i].size = 0;
-
-    // initialize other vars
-    s->size                   = 0;
-//    s->cap                    = 0;
-    s->qhead                  = 0;
-    s->qtail                  = 0;
-#ifdef USE_FLOAT_ACTIVITY
-    s->var_inc                = 1;
-    s->cla_inc                = 1;
-    s->var_decay              = (float)(1 / 0.95  );
-    s->cla_decay              = (float)(1 / 0.999 );
-#else
-    s->var_inc                = (1 <<  5);
-    s->cla_inc                = (1 << 11);
-#endif
-    s->root_level             = 0;
-    s->simpdb_assigns         = 0;
-    s->simpdb_props           = 0;
-    s->random_seed            = 91648253;
-    s->progress_estimate      = 0;
-    s->verbosity              = 0;
-
-    s->stats.starts           = 0;
-    s->stats.decisions        = 0;
-    s->stats.propagations     = 0;
-    s->stats.inspects         = 0;
-    s->stats.conflicts        = 0;
-    s->stats.clauses          = 0;
-    s->stats.clauses_literals = 0;
-    s->stats.learnts          = 0;
-    s->stats.learnts_literals = 0;
-    s->stats.tot_literals     = 0;
-}
-
-
-static void clause_remove(sat_solver* s, clause* c)
-{
-    lit* lits = clause_begin(c);
-    assert(lit_neg(lits[0]) < s->size*2);
-    assert(lit_neg(lits[1]) < s->size*2);
-
-    //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
-    //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
-
-    assert(lits[0] < s->size*2);
-    vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
-    vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
-
-    if (clause_learnt(c)){
-        s->stats.learnts--;
-        s->stats.learnts_literals -= clause_size(c);
-    }else{
-        s->stats.clauses--;
-        s->stats.clauses_literals -= clause_size(c);
-    }
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-    ABC_FREE(c);
-#else
-    Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
-#endif
-}
-
-static lbool clause_simplify(sat_solver* s, clause* c)
-{
-    lit*   lits   = clause_begin(c);
-    lbool* values = s->assigns;
-    int i;
-
-    assert(sat_solver_dl(s) == 0);
-
-    for (i = 0; i < clause_size(c); i++){
-        lbool sig = !lit_sign(lits[i]); sig += sig - 1;
-        if (values[lit_var(lits[i])] == sig)
-            return l_True;
-    }
-    return l_False;
-}
-
-int sat_solver_simplify(sat_solver* s)
-{
-    clause** reasons;
-    int type;
-
-    assert(sat_solver_dl(s) == 0);
-
-    if (sat_solver_propagate(s) != 0)
-        return false;
-
-    if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
-        return true;
-
-    reasons = s->reasons;
-    for (type = 0; type < 2; type++){
-        vecp*    cs  = type ? &s->learnts : &s->clauses;
-        clause** cls = (clause**)vecp_begin(cs);
-
-        int i, j;
-        for (j = i = 0; i < vecp_size(cs); i++){
-            if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] &&
-                clause_simplify(s,cls[i]) == l_True)
-                clause_remove(s,cls[i]);
-            else
-                cls[j++] = cls[i];
-        }
-        vecp_resize(cs,j);
-    }
-
-    s->simpdb_assigns = s->qhead;
-    // (shouldn't depend on 'stats' really, but it will do for now)
-    s->simpdb_props   = (int)(s->stats.clauses_literals + s->stats.learnts_literals);
-
-    return true;
-}
-
-
-static int clause_cmp (const void* x, const void* y) {
-    return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }
-
-void sat_solver_reducedb(sat_solver* s)
-{
-    int      i, j;
-    double   extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity
-    clause** learnts = (clause**)vecp_begin(&s->learnts);
-    clause** reasons = s->reasons;
-
-    sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
-
-    for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
-        if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
-            clause_remove(s,learnts[i]);
-        else
-            learnts[j++] = learnts[i];
-    }
-    for (; i < vecp_size(&s->learnts); i++){
-        if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim)
-            clause_remove(s,learnts[i]);
-        else
-            learnts[j++] = learnts[i];
-    }
-
-    //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j);
-
-
-    vecp_resize(&s->learnts,j);
-}
-
-int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
-{
-    clause * c;
-    lit *i,*j;
-    int maxvar;
-    lbool* values;
-    lit last;
-
-    veci_resize( &s->temp_clause, 0 );
-    for ( i = begin; i < end; i++ )
-        veci_push( &s->temp_clause, *i );
-    begin = veci_begin( &s->temp_clause );
-    end = begin + veci_size( &s->temp_clause );
-
-    if (begin == end) 
-        return false;
-
-    //printlits(begin,end); printf("\n");
-    // insertion sort
-    maxvar = lit_var(*begin);
-    for (i = begin + 1; i < end; i++){
-        lit l = *i;
-        maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
-        for (j = i; j > begin && *(j-1) > l; j--)
-            *j = *(j-1);
-        *j = l;
-    }
-    sat_solver_setnvars(s,maxvar+1);
-//    sat_solver_setnvars(s, lit_var(*(end-1))+1 );
-
-    ///////////////////////////////////
-    // add clause to internal storage
-    if ( s->pStore )
-    {
-        int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end );
-        assert( RetValue );
-    }
-    ///////////////////////////////////
-
-    //printlits(begin,end); printf("\n");
-    values = s->assigns;
-
-    // delete duplicates
-    last = lit_Undef;
-    for (i = j = begin; i < end; i++){
-        //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]));
-        lbool sig = !lit_sign(*i); sig += sig - 1;
-        if (*i == lit_neg(last) || sig == values[lit_var(*i)])
-            return true;   // tautology
-        else if (*i != last && values[lit_var(*i)] == l_Undef)
-            last = *j++ = *i;
-    }
-//    j = i;
-
-    if (j == begin)          // empty clause
-        return false;
-
-    if (j - begin == 1) // unit clause
-        return sat_solver_enqueue(s,*begin,(clause*)0);
-
-    // create new clause
-    c = clause_create_new(s,begin,j,0);
-    if ( c )
-        vecp_push(&s->clauses,c);
-
-
-    s->stats.clauses++;
-    s->stats.clauses_literals += j - begin;
-
-    return true;
-}
-
-
-double luby(double y, int x)
-{
-    int size, seq;
-    for (size = 1, seq = 0; size < x+1; seq++, size = 2*size + 1);
-    while (size-1 != x){
-        size = (size-1) >> 1;
-        seq--;
-        x = x % size;
-    }
-    return pow(y, (double)seq);
-} 
-
-void luby_test()
-{
-    int i;
-    for ( i = 0; i < 20; i++ )
-        printf( "%d ", (int)luby(2,i) );
-    printf( "\n" );
-}
-
-static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT64_T nof_learnts)
-{
-    int*    levels          = s->levels;
-    double  var_decay       = 0.95;
-    double  clause_decay    = 0.999;
-    double  random_var_freq = s->fNotUseRandom ? 0.0 : 0.02;
-
-    ABC_INT64_T  conflictC       = 0;
-    veci    learnt_clause;
-    int     i;
-
-    assert(s->root_level == sat_solver_dl(s));
-
-    s->nRestarts++;
-    s->stats.starts++;
-//    s->var_decay = (float)(1 / var_decay   );  // move this to sat_solver_new()
-//    s->cla_decay = (float)(1 / clause_decay);  // move this to sat_solver_new()
-    veci_resize(&s->model,0);
-    veci_new(&learnt_clause);
-
-    // use activity factors in every even restart
-    if ( (s->nRestarts & 1) && veci_size(&s->act_vars) > 0 )
-//    if ( veci_size(&s->act_vars) > 0 )
-        for ( i = 0; i < s->act_vars.size; i++ )
-            act_var_bump_factor(s, s->act_vars.ptr[i]);
-
-    // use activity factors in every restart
-    if ( s->pGlobalVars && veci_size(&s->act_vars) > 0 )
-        for ( i = 0; i < s->act_vars.size; i++ )
-            act_var_bump_global(s, s->act_vars.ptr[i]);
-
-    for (;;){
-        clause* confl = sat_solver_propagate(s);
-        if (confl != 0){
-            // CONFLICT
-            int blevel;
-
-#ifdef VERBOSEDEBUG
-            printf(L_IND"**CONFLICT**\n", L_ind);
-#endif
-            s->stats.conflicts++; conflictC++;
-            if (sat_solver_dl(s) == s->root_level){
-#ifdef SAT_USE_ANALYZE_FINAL
-                sat_solver_analyze_final(s, confl, 0);
-#endif
-                veci_delete(&learnt_clause);
-                return l_False;
-            }
-
-            veci_resize(&learnt_clause,0);
-            sat_solver_analyze(s, confl, &learnt_clause);
-            blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level;
-            blevel = s->root_level > blevel ? s->root_level : blevel;
-            sat_solver_canceluntil(s,blevel);
-            sat_solver_record(s,&learnt_clause);
-#ifdef SAT_USE_ANALYZE_FINAL
-//            if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0;    // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions)
-            if ( learnt_clause.size == 1 ) s->levels[lit_var(learnt_clause.ptr[0])] = 0;
-#endif
-            act_var_decay(s);
-            act_clause_decay(s);
-
-        }else{
-            // NO CONFLICT
-            int next;
- 
-            if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
-                // Reached bound on number of conflicts:
-                s->progress_estimate = sat_solver_progress(s);
-                sat_solver_canceluntil(s,s->root_level);
-                veci_delete(&learnt_clause);
-                return l_Undef; }
-
-            if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) ||
-//                 (s->nInsLimit  && s->stats.inspects  > s->nInsLimit) )
-                 (s->nInsLimit  && s->stats.propagations > s->nInsLimit) )
-            {
-                // Reached bound on number of conflicts:
-                s->progress_estimate = sat_solver_progress(s);
-                sat_solver_canceluntil(s,s->root_level);
-                veci_delete(&learnt_clause);
-                return l_Undef; 
-            }
-
-            if (sat_solver_dl(s) == 0 && !s->fSkipSimplify)
-                // Simplify the set of problem clauses:
-                sat_solver_simplify(s);
-
-//            if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
-                // Reduce the set of learnt clauses:
-//                sat_solver_reducedb(s);
-
-            // New variable decision:
-            s->stats.decisions++;
-            next = order_select(s,(float)random_var_freq);
-
-            if (next == var_Undef){
-                // Model found:
-                lbool* values = s->assigns;
-                int i;
-                veci_resize(&s->model, 0);
-                for (i = 0; i < s->size; i++) 
-                    veci_push(&s->model,(int)values[i]);
-                sat_solver_canceluntil(s,s->root_level);
-                veci_delete(&learnt_clause);
-
-                /*
-                veci apa; veci_new(&apa);
-                for (i = 0; i < s->size; i++) 
-                    veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i))));
-                printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n");
-                veci_delete(&apa);
-                */
-
-                return l_True;
-            }
-
-            if ( s->polarity[next] ) // positive polarity
-                sat_solver_assume(s,toLit(next));
-            else
-                sat_solver_assume(s,lit_neg(toLit(next)));
-        }
-    }
-
-    return l_Undef; // cannot happen
-}
-
-int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
-{
-    int restart_iter = 0;
-    ABC_INT64_T  nof_conflicts;
-    ABC_INT64_T  nof_learnts   = sat_solver_nclauses(s) / 3;
-    lbool   status        = l_Undef;
-    lbool*  values        = s->assigns;
-    lit*    i;
-
-    ////////////////////////////////////////////////
-    if ( s->fSolved )
-    {
-        if ( s->pStore )
-        {
-            int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
-            assert( RetValue );
-        }
-        return l_False;
-    }
-    ////////////////////////////////////////////////
-
-    // set the external limits
-    s->nCalls++;
-    s->nRestarts  = 0;
-    s->nConfLimit = 0;
-    s->nInsLimit  = 0;
-    if ( nConfLimit )
-        s->nConfLimit = s->stats.conflicts + nConfLimit;
-    if ( nInsLimit )
-//        s->nInsLimit = s->stats.inspects + nInsLimit;
-        s->nInsLimit = s->stats.propagations + nInsLimit;
-    if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) )
-        s->nConfLimit = nConfLimitGlobal;
-    if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) )
-        s->nInsLimit = nInsLimitGlobal;
-
-#ifndef SAT_USE_ANALYZE_FINAL
-
-    //printf("solve: "); printlits(begin, end); printf("\n");
-    for (i = begin; i < end; i++){
-        switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){
-        case 1: // l_True: 
-            break;
-        case 0: // l_Undef
-            sat_solver_assume(s, *i);
-            if (sat_solver_propagate(s) == NULL)
-                break;
-            // fallthrough
-        case -1: // l_False 
-            sat_solver_canceluntil(s, 0);
-            return l_False;
-        }
-    }
-    s->root_level = sat_solver_dl(s);
-
-#endif
-
-/*
-    // Perform assumptions:
-    root_level = assumps.size();
-    for (int i = 0; i < assumps.size(); i++){
-        Lit p = assumps[i];
-        assert(var(p) < nVars());
-        if (!sat_solver_assume(p)){
-            GClause r = reason[var(p)];
-            if (r != GClause_NULL){
-                Clause* confl;
-                if (r.isLit()){
-                    confl = propagate_tmpbin;
-                    (*confl)[1] = ~p;
-                    (*confl)[0] = r.lit();
-                }else
-                    confl = r.clause();
-                analyzeFinal(confl, true);
-                conflict.push(~p);
-            }else
-                conflict.clear(),
-                conflict.push(~p);
-            cancelUntil(0);
-            return false; }
-        Clause* confl = propagate();
-        if (confl != NULL){
-            analyzeFinal(confl), assert(conflict.size() > 0);
-            cancelUntil(0);
-            return false; }
-    }
-    assert(root_level == decisionLevel());
-*/
-
-#ifdef SAT_USE_ANALYZE_FINAL
-    // Perform assumptions:
-    s->root_level = end - begin;
-    for ( i = begin; i < end; i++ )
-    {
-        lit p = *i;
-        assert(lit_var(p) < s->size);
-        veci_push(&s->trail_lim,s->qtail);
-        if (!sat_solver_enqueue(s,p,(clause*)0))
-        {
-            clause * r = s->reasons[lit_var(p)];
-            if (r != NULL)
-            {
-                clause* confl;
-                if (clause_is_lit(r))
-                {
-                    confl = s->binary;
-                    (clause_begin(confl))[1] = lit_neg(p);
-                    (clause_begin(confl))[0] = clause_read_lit(r);
-                }
-                else
-                    confl = r;
-                sat_solver_analyze_final(s, confl, 1);
-                veci_push(&s->conf_final, lit_neg(p));
-            }
-            else
-            {
-                veci_resize(&s->conf_final,0);
-                veci_push(&s->conf_final, lit_neg(p));
-                // the two lines below are a bug fix by Siert Wieringa 
-                if (s->levels[lit_var(p)] > 0)
-                    veci_push(&s->conf_final, p);
-            }
-            sat_solver_canceluntil(s, 0);
-            return l_False; 
-        }
-        else
-        {
-            clause* confl = sat_solver_propagate(s);
-            if (confl != NULL){
-                sat_solver_analyze_final(s, confl, 0);
-                assert(s->conf_final.size > 0);
-                sat_solver_canceluntil(s, 0);
-                return l_False; }
-        }
-    }
-    assert(s->root_level == sat_solver_dl(s));
-#endif
-
-    s->nCalls2++;
-
-    if (s->verbosity >= 1){
-        printf("==================================[MINISAT]===================================\n");
-        printf("| Conflicts |     ORIGINAL     |              LEARNT              | Progress |\n");
-        printf("|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |\n");
-        printf("==============================================================================\n");
-    }
-
-    while (status == l_Undef){
-//        int nConfs = 0;
-        double Ratio = (s->stats.learnts == 0)? 0.0 :
-            s->stats.learnts_literals / (double)s->stats.learnts;
-        if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
-            break;
-
-        if (s->verbosity >= 1)
-        {
-            printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", 
-                (double)s->stats.conflicts,
-                (double)s->stats.clauses, 
-                (double)s->stats.clauses_literals,
-                (double)nof_learnts, 
-                (double)s->stats.learnts, 
-                (double)s->stats.learnts_literals,
-                Ratio,
-                s->progress_estimate*100);
-            fflush(stdout);
-        }
-        nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) );
-//printf( "%d ", (int)nof_conflicts );
-//        nConfs = s->stats.conflicts;
-        status = sat_solver_search(s, nof_conflicts, nof_learnts);
-//        if ( status == l_True )
-//            printf( "%d ", s->stats.conflicts - nConfs );
-
-//        nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5;
-        nof_learnts    = nof_learnts * 11 / 10; //*= 1.1;
-//printf( "%d ", s->stats.conflicts  );
-        // quit the loop if reached an external limit
-        if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
-        {
-//            printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
-            break;
-        }
-//        if ( s->nInsLimit  && s->stats.inspects > s->nInsLimit )
-        if ( s->nInsLimit  && s->stats.propagations > s->nInsLimit )
-        {
-//            printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
-            break;
-        }
-        if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
-            break;
-    }
-//printf( "\n" );
-    if (s->verbosity >= 1)
-        printf("==============================================================================\n");
-
-    sat_solver_canceluntil(s,0);
-
-    ////////////////////////////////////////////////
-    if ( status == l_False && s->pStore )
-    {
-        int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
-        assert( RetValue );
-    }
-    ////////////////////////////////////////////////
-    return status;
-}
-
-
-int sat_solver_nvars(sat_solver* s)
-{
-    return s->size;
-}
-
-
-int sat_solver_nclauses(sat_solver* s)
-{
-    return vecp_size(&s->clauses);
-}
-
-
-int sat_solver_nconflicts(sat_solver* s)
-{
-    return (int)s->stats.conflicts;
-}
-
-//=================================================================================================
-// Clause storage functions:
-
-void sat_solver_store_alloc( sat_solver * s )
-{
-    assert( s->pStore == NULL );
-    s->pStore = Sto_ManAlloc();
-}
-
-void sat_solver_store_write( sat_solver * s, char * pFileName )
-{
-    if ( s->pStore ) Sto_ManDumpClauses( (Sto_Man_t *)s->pStore, pFileName );
-}
-
-void sat_solver_store_free( sat_solver * s )
-{
-    if ( s->pStore ) Sto_ManFree( (Sto_Man_t *)s->pStore );
-    s->pStore = NULL;
-}
-
-int sat_solver_store_change_last( sat_solver * s )
-{
-    if ( s->pStore ) return Sto_ManChangeLastClause( (Sto_Man_t *)s->pStore );
-    return -1;
-}
- 
-void sat_solver_store_mark_roots( sat_solver * s )
-{
-    if ( s->pStore ) Sto_ManMarkRoots( (Sto_Man_t *)s->pStore );
-}
-
-void sat_solver_store_mark_clauses_a( sat_solver * s )
-{
-    if ( s->pStore ) Sto_ManMarkClausesA( (Sto_Man_t *)s->pStore );
-}
-
-void * sat_solver_store_release( sat_solver * s )
-{
-    void * pTemp;
-    if ( s->pStore == NULL )
-        return NULL;
-    pTemp = s->pStore;
-    s->pStore = NULL;
-    return pTemp;
-}
-
-//=================================================================================================
-// Sorting functions (sigh):
-
-static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *))
-{
-    int     i, j, best_i;
-    void*   tmp;
-
-    for (i = 0; i < size-1; i++){
-        best_i = i;
-        for (j = i+1; j < size; j++){
-            if (comp(array[j], array[best_i]) < 0)
-                best_i = j;
-        }
-        tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
-    }
-}
-
-
-static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed)
-{
-    if (size <= 15)
-        selectionsort(array, size, comp);
-
-    else{
-        void*       pivot = array[irand(seed, size)];
-        void*       tmp;
-        int         i = -1;
-        int         j = size;
-
-        for(;;){
-            do i++; while(comp(array[i], pivot)<0);
-            do j--; while(comp(pivot, array[j])<0);
-
-            if (i >= j) break;
-
-            tmp = array[i]; array[i] = array[j]; array[j] = tmp;
-        }
-
-        sortrnd(array    , i     , comp, seed);
-        sortrnd(&array[i], size-i, comp, seed);
-    }
-}
-
-void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *))
-{
-//    int i;
-    double seed = 91648253;
-    sortrnd(array,size,comp,&seed);
-//    for ( i = 1; i < size; i++ )
-//        assert(comp(array[i-1], array[i])<0);
-}
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/sat/bsat/satSolver_old.h b/src/sat/bsat/satSolver_old.h
deleted file mode 100644
index d2228f79..00000000
--- a/src/sat/bsat/satSolver_old.h
+++ /dev/null
@@ -1,210 +0,0 @@
-/**************************************************************************************************
-MiniSat -- Copyright (c) 2005, Niklas Sorensson
-http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
-
-Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
-associated documentation files (the "Software"), to deal in the Software without restriction,
-including without limitation the rights to use, copy, modify, merge, publish, distribute,
-sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in all copies or
-substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
-NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
-DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
-OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
-**************************************************************************************************/
-// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
-
-#ifndef ABC__sat__bsat__satSolver_old_h
-#define ABC__sat__bsat__satSolver_old_h
-
-
-#include <stdio.h>
-#include <stdlib.h>
-#include <string.h>
-#include <assert.h>
-
-#include "satVec.h"
-#include "satMem.h"
-
-ABC_NAMESPACE_HEADER_START
-
-//#define USE_FLOAT_ACTIVITY
-
-//=================================================================================================
-// Public interface:
-
-struct sat_solver_t;
-typedef struct sat_solver_t sat_solver;
-
-extern sat_solver* sat_solver_new(void);
-extern void        sat_solver_delete(sat_solver* s);
-
-extern int         sat_solver_addclause(sat_solver* s, lit* begin, lit* end);
-extern int         sat_solver_simplify(sat_solver* s);
-extern int         sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
-extern void        sat_solver_rollback( sat_solver* s );
-
-extern int         sat_solver_nvars(sat_solver* s);
-extern int         sat_solver_nclauses(sat_solver* s);
-extern int         sat_solver_nconflicts(sat_solver* s);
-
-extern void        sat_solver_setnvars(sat_solver* s,int n);
-
-extern void        Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
-extern void        Sat_SolverPrintStats( FILE * pFile, sat_solver * p );
-extern int *       Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars );
-extern void        Sat_SolverDoubleClauses( sat_solver * p, int iVar );
-
-// trace recording
-extern void        Sat_SolverTraceStart( sat_solver * pSat, char * pName );
-extern void        Sat_SolverTraceStop( sat_solver * pSat );
-extern void        Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot );
-
-// clause storage
-extern void        sat_solver_store_alloc( sat_solver * s );
-extern void        sat_solver_store_write( sat_solver * s, char * pFileName );
-extern void        sat_solver_store_free( sat_solver * s );
-extern void        sat_solver_store_mark_roots( sat_solver * s );
-extern void        sat_solver_store_mark_clauses_a( sat_solver * s );
-extern void *      sat_solver_store_release( sat_solver * s ); 
-
-//=================================================================================================
-// Solver representation:
-
-struct clause_t;
-typedef struct clause_t clause;
-
-struct sat_solver_t
-{
-    int      size;          // nof variables
-    int      cap;           // size of varmaps
-    int      qhead;         // Head index of queue.
-    int      qtail;         // Tail index of queue.
-
-    // clauses
-    vecp     clauses;       // List of problem constraints. (contains: clause*)
-    vecp     learnts;       // List of learnt clauses. (contains: clause*)
-
-    // activities
-#ifdef USE_FLOAT_ACTIVITY
-    double   var_inc;       // Amount to bump next variable with.
-    double   var_decay;     // INVERSE decay factor for variable activity: stores 1/decay. 
-    float    cla_inc;       // Amount to bump next clause with.
-    float    cla_decay;     // INVERSE decay factor for clause activity: stores 1/decay.
-    double*  activity;      // A heuristic measurement of the activity of a variable.
-#else
-    int      var_inc;       // Amount to bump next variable with.
-    int      cla_inc;       // Amount to bump next clause with.
-    unsigned*activity;      // A heuristic measurement of the activity of a variable.
-#endif
-
-    vecp*    wlists;        // 
-    lbool*   assigns;       // Current values of variables.
-    int*     orderpos;      // Index in variable order.
-    clause** reasons;       //
-    int*     levels;        //
-    lit*     trail;
-    char*    polarity;
-
-    clause*  binary;        // A temporary binary clause
-    lbool*   tags;          //
-    veci     tagged;        // (contains: var)
-    veci     stack;         // (contains: var)
-
-    veci     order;         // Variable order. (heap) (contains: var)
-    veci     trail_lim;     // Separator indices for different decision levels in 'trail'. (contains: int)
-    veci     model;         // If problem is solved, this vector contains the model (contains: lbool).
-    veci     conf_final;    // If problem is unsatisfiable (possibly under assumptions),
-                            // this vector represent the final conflict clause expressed in the assumptions.
-
-    int      root_level;    // Level of first proper decision.
-    int      simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
-    int      simpdb_props;  // Number of propagations before next 'simplifyDB()'.
-    double   random_seed;
-    double   progress_estimate;
-    int      verbosity;     // Verbosity level. 0=silent, 1=some progress report, 2=everything
-
-    stats_t    stats;
-
-    ABC_INT64_T   nConfLimit;    // external limit on the number of conflicts
-    ABC_INT64_T   nInsLimit;     // external limit on the number of implications
-    int           nRuntimeLimit; // external limit on runtime
-
-    veci     act_vars;      // variables whose activity has changed
-    double*  factors;       // the activity factors
-    int      nRestarts;     // the number of local restarts
-    int      nCalls;        // the number of local restarts
-    int      nCalls2;        // the number of local restarts
- 
-    Sat_MmStep_t * pMem;
-
-    int      fSkipSimplify; // set to one to skip simplification of the clause database
-    int      fNotUseRandom; // do not allow random decisions with a fixed probability
-
-    int *    pGlobalVars;   // for experiments with global vars during interpolation
-    // clause store
-    void *   pStore;
-    int      fSolved;
-
-    // trace recording
-    FILE *   pFile;
-    int      nClauses;
-    int      nRoots;
-
-    veci     temp_clause;    // temporary storage for a CNF clause
-};
-
-static int sat_solver_var_value( sat_solver* s, int v ) 
-{
-    assert( s->model.ptr != NULL && v < s->size );
-    return (int)(s->model.ptr[v] == l_True);
-}
-static int sat_solver_var_literal( sat_solver* s, int v ) 
-{
-    assert( s->model.ptr != NULL && v < s->size );
-    return toLitCond( v, s->model.ptr[v] != l_True );
-}
-static void sat_solver_act_var_clear(sat_solver* s) 
-{
-    int i;
-    for (i = 0; i < s->size; i++)
-        s->activity[i] = 0.0;
-    s->var_inc = 1.0;
-}
-static void sat_solver_compress(sat_solver* s) 
-{
-    if ( s->qtail != s->qhead )
-    {
-        int RetValue = sat_solver_simplify(s);
-        assert( RetValue != 0 );
-    }
-}
-
-static int sat_solver_final(sat_solver* s, int ** ppArray)
-{
-    *ppArray = s->conf_final.ptr;
-    return s->conf_final.size;
-}
-
-static int sat_solver_set_runtime_limit(sat_solver* s, int Limit)
-{
-    int nRuntimeLimit = s->nRuntimeLimit;
-    s->nRuntimeLimit = Limit;
-    return nRuntimeLimit;
-}
-
-static int sat_solver_set_random(sat_solver* s, int fNotUseRandom)
-{
-    int fNotUseRandomOld = s->fNotUseRandom;
-    s->fNotUseRandom = fNotUseRandom;
-    return fNotUseRandomOld;
-}
-
-ABC_NAMESPACE_HEADER_END
-
-#endif
diff --git a/src/sat/bsat/satTruth.c b/src/sat/bsat/satTruth.c
index 7d69f558..dc5644b3 100644
--- a/src/sat/bsat/satTruth.c
+++ b/src/sat/bsat/satTruth.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "satTruth.h"
-#include "vecRec.h"
+#include "vecSet.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -39,7 +39,7 @@ struct Tru_Man_t_
     int              nEntrySize;   // the size of one entry in 'int'
     int              nTableSize;   // hash table size
     int *            pTable;       // hash table
-    Vec_Rec_t *      pMem;         // memory for truth tables
+    Vec_Set_t *      pMem;         // memory for truth tables
     word *           pZero;        // temporary truth table 
     int              hIthVars[16]; // variable handles
     int              nTableLookups;
@@ -53,7 +53,7 @@ struct Tru_One_t_
     word             pTruth[0];    // truth table
 };
 
-static inline Tru_One_t * Tru_ManReadOne( Tru_Man_t * p, int h ) { return h ? (Tru_One_t *)Vec_RecEntryP(p->pMem, h) : NULL; }
+static inline Tru_One_t * Tru_ManReadOne( Tru_Man_t * p, int h ) { return h ? (Tru_One_t *)Vec_SetEntry(p->pMem, h) : NULL; }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -140,7 +140,7 @@ void Tru_ManResize( Tru_Man_t * p )
         *pSpot = pThis->Handle;
         Counter++;
     }
-    assert( Counter == Vec_RecEntryNum(p->pMem) );
+    assert( Counter == Vec_SetEntryNum(p->pMem) );
     ABC_FREE( pTableOld );
 }
 
@@ -163,7 +163,7 @@ int Tru_ManInsert( Tru_Man_t * p, word * pTruth )
     if ( Tru_ManEqual1(pTruth, p->nWords) )
         return 1;
     p->nTableLookups++;
-    if ( Vec_RecEntryNum(p->pMem) > 2 * p->nTableSize )
+    if ( Vec_SetEntryNum(p->pMem) > 2 * p->nTableSize )
         Tru_ManResize( p );
     fCompl = pTruth[0] & 1;
     if ( fCompl )  
@@ -172,7 +172,7 @@ int Tru_ManInsert( Tru_Man_t * p, word * pTruth )
     if ( *pSpot == 0 )
     {
         Tru_One_t * pEntry;
-        *pSpot = Vec_RecAppend( p->pMem, p->nEntrySize );
+        *pSpot = Vec_SetAppend( p->pMem, NULL, p->nEntrySize );
         assert( (*pSpot & 1) == 0 );
         pEntry = Tru_ManReadOne( p, *pSpot );
         Tru_ManCopy( pEntry->pTruth, pTruth, p->nWords );
@@ -215,7 +215,7 @@ Tru_Man_t * Tru_ManAlloc( int nVars )
     p->nEntrySize = (sizeof(Tru_One_t) + p->nWords * sizeof(word))/sizeof(int);
     p->nTableSize = 8147;
     p->pTable     = ABC_CALLOC( int, p->nTableSize );
-    p->pMem       = Vec_RecAlloc();
+    p->pMem       = Vec_SetAlloc();
     // initialize truth tables
     p->pZero = ABC_ALLOC( word, p->nWords );
     for ( i = 0; i < nVars; i++ )
@@ -247,8 +247,8 @@ Tru_Man_t * Tru_ManAlloc( int nVars )
 ***********************************************************************/
 void Tru_ManFree( Tru_Man_t * p )
 {
-    printf( "Lookups = %d. Entries = %d.\n", p->nTableLookups, Vec_RecEntryNum(p->pMem) );
-    Vec_RecFree( p->pMem );
+    printf( "Lookups = %d. Entries = %d.\n", p->nTableLookups, Vec_SetEntryNum(p->pMem) );
+    Vec_SetFree( p->pMem );
     ABC_FREE( p->pZero );
     ABC_FREE( p->pTable );
     ABC_FREE( p );
@@ -287,25 +287,9 @@ word * Tru_ManFunc( Tru_Man_t * p, int h )
     assert( (h & 1) == 0 );
     if ( h == 0 )
         return p->pZero;
-    assert( Vec_RecChunk(h) );
     return Tru_ManReadOne( p, h )->pTruth;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Returns stored truth table]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Tru_ManHandleMax( Tru_Man_t * p )
-{
-    return p->pMem->hCurrent;
-}
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/bsat/satTruth.h b/src/sat/bsat/satTruth.h
index 2f17b6f0..dcbf6526 100644
--- a/src/sat/bsat/satTruth.h
+++ b/src/sat/bsat/satTruth.h
@@ -77,7 +77,7 @@ extern void          Tru_ManFree( Tru_Man_t * p );
 extern word *        Tru_ManVar( Tru_Man_t * p, int v );
 extern word *        Tru_ManFunc( Tru_Man_t * p, int h );
 extern int           Tru_ManInsert( Tru_Man_t * p, word * pTruth );
-extern int           Tru_ManHandleMax( Tru_Man_t * p );
+//extern int           Tru_ManHandleMax( Tru_Man_t * p );
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/sat/bsat/vecRec.h b/src/sat/bsat/vecRec.h
deleted file mode 100644
index 82d7183d..00000000
--- a/src/sat/bsat/vecRec.h
+++ /dev/null
@@ -1,396 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [vecRec.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Resizable arrays.]
-
-  Synopsis    [Array of records.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: vecRec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
- 
-#ifndef ABC__sat__bsat__vecRec_h
-#define ABC__sat__bsat__vecRec_h
-
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-#include <stdio.h>
-
-ABC_NAMESPACE_HEADER_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-// data-structure for logging entries
-// memory is allocated in 'p->Mask+1' int chunks
-// the first 'int' of each entry cannot be 0
-typedef struct Vec_Rec_t_ Vec_Rec_t;
-struct Vec_Rec_t_ 
-{
-    int                Mask;         // mask for the log size
-    int                hCurrent;     // current position
-    int                hShadow;      // current position
-    int                nEntries;     // total number of entries
-    int                nChunks;      // total number of chunks
-    int                nChunksAlloc; // the number of allocated chunks
-    int **             pChunks;      // the chunks
-};
-
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-// p is vector of records
-// Size is given by the user
-// Handle is returned to the user
-// c (chunk) and s (shift) are variables used here
-#define Vec_RecForEachEntry( p, Size, Handle, c, s )   \
-    for ( c = 1; c <= p->nChunks; c++ )                \
-        for ( s = 0; p->pChunks[c][s] && ((Handle) = (((c)<<16)|(s))); s += Size, assert(s < p->Mask) )
-
-#define Vec_RecForEachEntryStart( p, Size, Handle, c, s, hStart )   \
-    for ( c = Vec_RecChunk(hStart), s = Vec_RecShift(hStart); c <= p->nChunks; c++, s = 0 )                \
-        for ( ; p->pChunks[c][s] && ((Handle) = (((c)<<16)|(s))); s += Size, assert(s < p->Mask) )
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Rec_t * Vec_RecAlloc()
-{
-    Vec_Rec_t * p;
-    p = ABC_CALLOC( Vec_Rec_t, 1 );
-    p->Mask          = (1 << 15) - 1; // chunk size = 2^15 ints = 128 Kb
-    p->hCurrent      = (1 << 16);
-    p->nChunks       = 1;
-    p->nChunksAlloc  = 16;
-    p->pChunks       = ABC_CALLOC( int *, p->nChunksAlloc );
-    p->pChunks[0]    = NULL;
-    p->pChunks[1]    = ABC_ALLOC( int, (1 << 16) );
-    p->pChunks[1][0] = 0;
-    return p;
-}
-static inline void Vec_RecAlloc_( Vec_Rec_t * p )
-{
-//    Vec_Rec_t * p;
-//    p = ABC_CALLOC( Vec_Rec_t, 1 );
-    memset( p, 0, sizeof(Vec_Rec_t) );
-    p->Mask          = (1 << 15) - 1; // chunk size = 2^15 ints = 128 Kb
-    p->hCurrent      = (1 << 16);
-    p->nChunks       = 1;
-    p->nChunksAlloc  = 16;
-    p->pChunks       = ABC_CALLOC( int *, p->nChunksAlloc );
-    p->pChunks[0]    = NULL;
-    p->pChunks[1]    = ABC_ALLOC( int, (1 << 16) );
-    p->pChunks[1][0] = 0;
-//    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_RecChunk( int i )
-{
-    return i>>16;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_RecShift( int i )
-{
-    return i&0xFFFF;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_RecSize( Vec_Rec_t * p )
-{
-    return Vec_RecChunk(p->hCurrent) * (p->Mask + 1); 
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_RecEntryNum( Vec_Rec_t * p )
-{
-    return p->nEntries;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_RecEntry( Vec_Rec_t * p, int i )
-{
-    assert( i <= p->hCurrent );
-    return p->pChunks[Vec_RecChunk(i)][Vec_RecShift(i)];
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int * Vec_RecEntryP( Vec_Rec_t * p, int i )
-{
-    assert( i <= p->hCurrent );
-    return p->pChunks[Vec_RecChunk(i)] + Vec_RecShift(i);
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_RecRestart( Vec_Rec_t * p )
-{
-    p->hCurrent = (1 << 16);
-    p->nChunks  = 1;
-    p->nEntries = 0;
-    p->pChunks[1][0] = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_RecShrink( Vec_Rec_t * p, int h )
-{
-    int i;
-    assert( Vec_RecEntry(p, h) == 0 );
-    for ( i = Vec_RecChunk(h)+1; i < p->nChunksAlloc; i++ )
-        ABC_FREE( p->pChunks[i] );
-    p->nChunks = Vec_RecChunk(h);
-    p->hCurrent = h;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_RecFree( Vec_Rec_t * p )
-{
-    int i;
-    for ( i = 0; i < p->nChunksAlloc; i++ )
-        ABC_FREE( p->pChunks[i] );
-    ABC_FREE( p->pChunks );
-    ABC_FREE( p );
-}
-static inline void Vec_RecFree_( Vec_Rec_t * p )
-{
-    int i;
-    for ( i = 0; i < p->nChunksAlloc; i++ )
-        ABC_FREE( p->pChunks[i] );
-    ABC_FREE( p->pChunks );
-//    ABC_FREE( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_RecAppend( Vec_Rec_t * p, int nSize )
-{
-    assert( nSize <= p->Mask );
-    assert( Vec_RecEntry(p, p->hCurrent) == 0 );
-    assert( Vec_RecChunk(p->hCurrent) == p->nChunks );
-    if ( Vec_RecShift(p->hCurrent) + nSize >= p->Mask )
-    {
-        if ( ++p->nChunks == p->nChunksAlloc )
-        {
-            p->pChunks = ABC_REALLOC( int *, p->pChunks, p->nChunksAlloc * 2 );
-            memset( p->pChunks + p->nChunksAlloc, 0, sizeof(int *) * p->nChunksAlloc );
-            p->nChunksAlloc *= 2;
-        }
-        if ( p->pChunks[p->nChunks] == NULL )
-            p->pChunks[p->nChunks] = ABC_ALLOC( int, (p->Mask + 1) );
-        p->pChunks[p->nChunks][0] = 0;
-        p->hCurrent = p->nChunks << 16;
-    }
-    p->hCurrent += nSize;
-    *Vec_RecEntryP(p, p->hCurrent) = 0;
-    p->nEntries++;
-    return p->hCurrent - nSize;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_RecPush( Vec_Rec_t * p, int * pArray, int nSize )
-{
-    int Handle = Vec_RecAppend( p, nSize );
-    memmove( Vec_RecEntryP(p, Handle), pArray, sizeof(int) * nSize );
-    return Handle;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_RecSetShadow( Vec_Rec_t * p, int hShadow )
-{
-    p->hShadow = hShadow;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_RecReadShadow( Vec_Rec_t * p )
-{
-    return p->hShadow;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_RecAppendShadow( Vec_Rec_t * p, int nSize )
-{
-    if ( Vec_RecShift(p->hShadow) + nSize >= p->Mask )
-        p->hShadow = ((Vec_RecChunk(p->hShadow) + 1) << 16);
-    p->hShadow += nSize;
-    return p->hShadow - nSize;
-}
-
-
-ABC_NAMESPACE_HEADER_END
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/sat/bsat/vecSet.h b/src/sat/bsat/vecSet.h
new file mode 100644
index 00000000..e95c3332
--- /dev/null
+++ b/src/sat/bsat/vecSet.h
@@ -0,0 +1,247 @@
+/**CFile****************************************************************
+
+  FileName    [vecSet.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT solvers.]
+
+  Synopsis    [Multi-page dynamic array.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: vecSet.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__sat__bsat__vecSet_h
+#define ABC__sat__bsat__vecSet_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// data-structure for logging entries
+// memory is allocated in 2^16 word-sized pages
+// the first 'word' of each page is used storing additional data
+// the first 'int' of additional data stores the word limit
+// the second 'int' of the additional data stores the shadow word limit
+
+typedef struct Vec_Set_t_ Vec_Set_t;
+struct Vec_Set_t_ 
+{
+    int                nEntries;     // entry count
+    int                iPage;        // current page
+    int                iPageS;       // shadow page
+    int                nPagesAlloc;  // page count allocated
+    word **            pPages;       // page pointers
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int     Vec_SetHandPage( int h )                   { return h >> 16;                }
+static inline int     Vec_SetHandShift( int h )                  { return h & 0xFFFF;             }
+
+static inline word *  Vec_SetEntry( Vec_Set_t * p, int h )       { return p->pPages[Vec_SetHandPage(h)] + Vec_SetHandShift(h);     }
+static inline int     Vec_SetEntryNum( Vec_Set_t * p )           { return p->nEntries;            }
+static inline void    Vec_SetWriteEntryNum( Vec_Set_t * p, int i){ p->nEntries = i;               }
+
+static inline int     Vec_SetLimit( word * p )                   { return ((int*)p)[0];           }
+static inline int     Vec_SetLimitS( word * p )                  { return ((int*)p)[1];           }
+
+static inline int     Vec_SetIncLimit( word * p, int nWords )    { return ((int*)p)[0] += nWords; }
+static inline int     Vec_SetIncLimitS( word * p, int nWords )   { return ((int*)p)[1] += nWords; }
+
+static inline void    Vec_SetWriteLimit( word * p, int nWords )  { ((int*)p)[0] = nWords;         }
+static inline void    Vec_SetWriteLimitS( word * p, int nWords ) { ((int*)p)[1] = nWords;         }
+
+static inline int     Vec_SetHandCurrent( Vec_Set_t * p )        { return (p->iPage << 16)  + Vec_SetLimit(p->pPages[p->iPage]);   }
+static inline int     Vec_SetHandCurrentS( Vec_Set_t * p )       { return (p->iPageS << 16) + Vec_SetLimitS(p->pPages[p->iPageS]); }
+
+static inline int     Vec_SetHandMemory( Vec_Set_t * p, int h )  { return Vec_SetHandPage(h) * 0x8FFFF + Vec_SetHandShift(h) * 8;  }
+static inline int     Vec_SetMemory( Vec_Set_t * p )             { return Vec_SetHandMemory(p, Vec_SetHandCurrent(p));             }
+static inline int     Vec_SetMemoryS( Vec_Set_t * p )            { return Vec_SetHandMemory(p, Vec_SetHandCurrentS(p));            }
+static inline int     Vec_SetMemoryAll( Vec_Set_t * p )          { return (p->iPage+1) * 0x8FFFF;                                  }
+
+// Type is the Set type
+// pVec is vector of set
+// nSize should be given by the user
+// pSet is the pointer to the set
+// p (page) and s (shift) are variables used here
+#define Vec_SetForEachEntry( Type, pVec, nSize, pSet, p, s )   \
+    for ( p = 0; p <= pVec->iPage; p++ )                       \
+        for ( s = 1; s < Vec_SetLimit(pVec->pPages[p]) && ((pSet) = (Type)(pVec->pPages[p] + (s))); s += nSize )
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocating vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_SetAlloc_( Vec_Set_t * p )
+{
+    memset( p, 0, sizeof(Vec_Set_t) );
+    p->nPagesAlloc  = 256;
+    p->pPages       = ABC_CALLOC( word *, p->nPagesAlloc );
+    p->pPages[0]    = ABC_ALLOC( word, 0x10000 );
+    p->pPages[0][0] = ~0;
+    Vec_SetWriteLimit( p->pPages[0], 1 );
+}
+static inline Vec_Set_t * Vec_SetAlloc()
+{
+    Vec_Set_t * p;
+    p = ABC_CALLOC( Vec_Set_t, 1 );
+    Vec_SetAlloc_( p );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resetting vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_SetRestart( Vec_Set_t * p )
+{
+    p->nEntries     = 0;
+    p->iPage        = 0;
+    p->iPageS       = 0;
+    p->pPages[0][0] = ~0;
+    Vec_SetWriteLimit( p->pPages[0], 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Freeing vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_SetFree_( Vec_Set_t * p )
+{
+    int i;
+    for ( i = 0; i < p->nPagesAlloc; i++ )
+        ABC_FREE( p->pPages[i] );
+    ABC_FREE( p->pPages );
+}
+static inline void Vec_SetFree( Vec_Set_t * p )
+{
+    Vec_SetFree_( p );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Appending entries to vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize )
+{
+    int nWords = (nSize + 1) >> 1;
+    assert( nWords < 0x10000 );
+    p->nEntries++;
+    if ( Vec_SetLimit( p->pPages[p->iPage] ) + nWords > 0x10000 )
+    {
+        if ( ++p->iPage == p->nPagesAlloc )
+        {
+            p->pPages = ABC_REALLOC( word *, p->pPages, p->nPagesAlloc * 2 );
+            memset( p->pPages + p->nPagesAlloc, 0, sizeof(word *) * p->nPagesAlloc );
+            p->nPagesAlloc *= 2;
+        }
+        if ( p->pPages[p->iPage] == NULL )
+            p->pPages[p->iPage] = ABC_ALLOC( word, 0x10000 );
+        p->pPages[p->iPage][0] = ~0;
+        Vec_SetWriteLimit( p->pPages[p->iPage], 1 );
+    }
+    if ( pArray )
+    memmove( p->pPages[p->iPage] + Vec_SetLimit(p->pPages[p->iPage]), pArray, sizeof(int) * nSize );
+    Vec_SetIncLimit( p->pPages[p->iPage], nWords );
+    return Vec_SetHandCurrent(p) - nWords;
+}
+static inline int Vec_SetAppendS( Vec_Set_t * p, int nSize )
+{
+    int nWords = (nSize + 1) >> 1;
+    assert( nWords < 0x10000 );
+    if ( Vec_SetLimitS( p->pPages[p->iPageS] ) + nWords > 0x10000 )
+        Vec_SetWriteLimitS( p->pPages[++p->iPageS], 1 );
+    Vec_SetIncLimitS( p->pPages[p->iPageS], nWords );
+    return Vec_SetHandCurrentS(p) - nWords;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Shrinking vector size.]
+
+  Description []
+               
+  SideEffects [This procedure does not update the number of entries.]
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_SetShrink( Vec_Set_t * p, int h )
+{
+    assert( h <= Vec_SetHandCurrent(p) );
+    p->iPage = Vec_SetHandPage(h);
+    Vec_SetWriteLimit( p->pPages[p->iPage], Vec_SetHandShift(h) );
+}
+static inline void Vec_SetShrinkS( Vec_Set_t * p, int h ) 
+{ 
+    assert( h <= Vec_SetHandCurrent(p) );
+    p->iPageS = Vec_SetHandPage(h); 
+    Vec_SetWriteLimitS( p->pPages[p->iPageS], Vec_SetHandShift(h) );  
+}
+
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+