Proof-logging in the updated solver.

3 files changed, 124 insertions, 176 deletions

diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index a06dd412..0a5920c7 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -28,10 +28,11 @@ ABC_NAMESPACE_IMPL_START
 /*
     Proof is represented as a vector of integers.
     The first entry is -1.
-    The clause is represented as an offset in this array.
-    One clause's entry is <size><label><ant1><ant2>...<antN>
+    A resolution record is represented by a handle (an offset in this array).
+    A resolution record entry is <size><label><ant1><ant2>...<antN>
     Label is initialized to 0.
-    Root clauses are 1-based. They are marked by prepending bit 1;
+    Root clauses are given by their handles.
+    They are marked by bitshifting by 2 bits up and setting the LSB to 1
 */
 /*
 
@@ -59,11 +60,11 @@ static inline cla     Proof_NodeHandle (Vec_Int_t* p, satset* c)  { return satse
 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;     }
 
-#define Proof_ForeachNode( p, pNode, hNode )             \
-    satset_foreach_entry( ((veci*)p), pNode, hNode, 1 )
-#define Proof_ForeachNodeVec( pVec, p, pNode, i )        \
+#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_ForeachNodeVec( pVec, p, pNode, i )            \
     for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_NodeRead(p, Vec_IntEntry(pVec,i))); i++ )
-#define Proof_NodeForeachFanin( p, pNode, pFanin, i )    \
+#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_NodeForeachLeaf( pLeaves, pNode, pLeaf, i )    \
     for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pLeaves, pNode->pEnts[i] >> 2) : NULL), 1); i++ )
@@ -139,7 +140,7 @@ void Proof_CollectUsed_iter( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed, V
     while ( Vec_IntSize(vStack) )
     {
         hNode = Vec_IntPop( vStack );
-        if ( hNode & 1 ) // extrated second time
+        if ( hNode & 1 ) // extracted second time
         {
             Vec_IntPush( vUsed, hNode >> 1 );
             continue;
@@ -171,6 +172,8 @@ void Proof_CollectUsed_iter( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed, V
 Vec_Int_t * Proof_CollectUsedIter( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hRoot )
 {
     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 );
@@ -184,6 +187,30 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Int_t * vProof, Vec_Int_t * vRoots, int h
             Proof_CollectUsed_iter( vProof, pNode, 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 ( iPrev >= Entry )
+            printf( "Out of topological order!!!\n" );
+        assert( iPrev < Entry );
+        iPrev = Entry;
+    }
     return vUsed;
 }
 
@@ -224,10 +251,9 @@ void Proof_CollectUsed_rec( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed )
 ***********************************************************************/
 Vec_Int_t * Proof_CollectUsedRec( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hRoot )
 {
-    Vec_Int_t * vUsed, * vStack;
+    Vec_Int_t * vUsed;
     assert( (hRoot > 0) ^ (vRoots != NULL) );
     vUsed = Vec_IntAlloc( 1000 );
-    vStack = Vec_IntAlloc( 1000 );
     if ( hRoot )
         Proof_CollectUsed_rec( vProof, Proof_NodeRead(vProof, hRoot), vUsed );
     else
@@ -237,7 +263,6 @@ Vec_Int_t * Proof_CollectUsedRec( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hR
         Proof_ForeachNodeVec( vRoots, vProof, pNode, i )
             Proof_CollectUsed_rec( vProof, pNode, vUsed );
     }
-    Vec_IntFree( vStack );
     return vUsed;
 }
  
@@ -333,6 +358,7 @@ void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot )
     int i, k, Counter = 0, clk = clock(); 
     // collect visited clauses
     vUsed = Proof_CollectUsedRec( vProof, NULL, hRoot );
+//    vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
     Proof_CleanCollected( vProof, vUsed );
     // perform resolution steps
     vTemp = Vec_IntAlloc( 1000 );
@@ -366,104 +392,79 @@ void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot )
     Vec_IntFree( vUsed );
 }
 
-
-
-
-
 /**Function*************************************************************
 
-  Synopsis    [Recursively visits useful proof nodes.]
+  Synopsis    [Reduces the proof to contain only roots and their children.]
 
-  Description []
+  Description [The result is updated proof and updated roots.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Sat_ProofReduceOne( Vec_Int_t * p, satset * pNode, int * pnSize, Vec_Int_t * vStack )
+void Sat_ProofReduce( Vec_Int_t * vProof, Vec_Int_t * vRoots )
 {
-    satset * pNext;
-    int i, NodeId;
-    if ( pNode->Id )
-        return pNode->Id;
-    // start with node
-    pNode->Id = 1;
-    Vec_IntPush( vStack, Proof_NodeHandle(p, pNode) );
-    // perform DFS search
-    while ( Vec_IntSize(vStack) )
+    Vec_Int_t * vUsed;
+    satset * pNode, * pFanin;
+    int i, k, nSize = 1;
+    // collect visited nodes
+    vUsed = Proof_CollectUsedIter( vProof, vRoots, 0 );
+    // relabel nodes to use smaller space
+    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
     {
-        NodeId = Vec_IntPop( vStack );
-        if ( NodeId & 1 ) // extrated second time
-        {
-            pNode = Proof_NodeRead( p, NodeId ^ 1 );
-            pNode->Id = *pnSize;
-            *pnSize += Proof_NodeSize(pNode->nEnts);
-            // update fanins
-            Proof_NodeForeachFanin( p, pNode, pNext, i )
-                if ( pNext )
-                    pNode->pEnts[i] = pNext->Id;
-            continue;
-        }
-        // extracted first time
-        // add second time
-        Vec_IntPush( vStack, NodeId ^ 1 );
-        // add its anticedents
-        pNode = Proof_NodeRead( p, NodeId );
-        Proof_NodeForeachFanin( p, pNode, pNext, i )
-            if ( pNext && !pNext->Id )
-            {
-                pNext->Id = 1;
-                Vec_IntPush( vStack, Proof_NodeHandle(p, pNode) ); // add first time
-            }
+        pNode->Id = nSize;
+        nSize += Proof_NodeSize(pNode->nEnts);
+        Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
+            if ( pFanin )
+                pNode->pEnts[i] = (pFanin->Id << 2) | (pNode->pEnts[i] & 2);
+    }
+    // compact the nodes
+    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
+    {
+        memmove( Vec_IntArray(vProof) + pNode->Id, pNode, Proof_NodeSize(pNode->nEnts) );
+        pNode->Id = 0;
     }
-    return pNode->Id;
+    // report the result
+    printf( "The proof was reduced from %d to %d (by %6.2f %%)\n", 
+        Vec_IntSize(vProof), nSize, 100.0 * (Vec_IntSize(vProof) - nSize) / Vec_IntSize(vProof) );
+    Vec_IntShrink( vProof, nSize );
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Reduces the proof to contain only roots and their children.]
+  Synopsis    [Collects nodes belonging to the UNSAT core.]
 
-  Description [The result is updated proof and updated roots.]
+  Description [The result is the array of root clause indexes.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Sat_ProofReduce( Vec_Int_t * p, Vec_Int_t * vRoots )
+Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vUsed )
 {
-    int i, nSize = 1;
-    int * pBeg, * pEnd, * pNew;
-    Vec_Int_t * vStack;
-    satset * pNode;
-    // mark used nodes
-    vStack = Vec_IntAlloc( 1000 );
-    Proof_ForeachNodeVec( vRoots, p, pNode, i )
-        vRoots->pArray[i] = Sat_ProofReduceOne( p, pNode, &nSize, vStack );
-    Vec_IntFree( vStack );
-    // compact proof
-    pNew = Vec_IntArray(p) + 1;
-    Proof_ForeachNode( p, pNode, i )
+    Vec_Int_t * vCore;
+    satset * pNode, * pFanin;
+    int i, k, clk = clock();
+    vCore = Vec_IntAlloc( 1000 );
+    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
     {
-        if ( !pNode->Id )
-            continue;
-        assert( pNew - Vec_IntArray(p) == pNode->Id );
         pNode->Id = 0;
-        pBeg = (int *)pNode;
-        pEnd = pBeg + Proof_NodeSize(pNode->nEnts);
-        while ( pBeg < pEnd )
-            *pNew++ = *pBeg++;
+        Proof_NodeForeachLeaf( vClauses, pNode, pFanin, k )
+            if ( pFanin && !pFanin->mark )
+            {
+                pFanin->mark = 1;
+                Vec_IntPush( vCore, Proof_NodeHandle(vClauses, pFanin) );
+            }
     }
-    // report the result
-    printf( "The proof was reduced from %d to %d (by %6.2f %%)\n", 
-        Vec_IntSize(p), nSize, 100.0 * (Vec_IntSize(p) - nSize) / Vec_IntSize(p) );
-    assert( pNew - Vec_IntArray(p) == nSize );
-    Vec_IntShrink( p, nSize );
+    // clean core clauses
+    Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
+        pNode->mark = 0;
+    return vCore;
 }
 
-
-
 /**Function*************************************************************
 
   Synopsis    [Computes UNSAT core.]
@@ -475,31 +476,14 @@ void Sat_ProofReduce( Vec_Int_t * p, Vec_Int_t * vRoots )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Sat_ProofCore( Vec_Int_t * vProof, Vec_Int_t * vRoots )
+Vec_Int_t * Sat_ProofCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hNode )
 {
     Vec_Int_t * vCore, * vUsed;
-    satset * pNode, * pFanin;
-    int i, k, clk = clock();;
     // collect visited clauses
-    vUsed = Proof_CollectUsedIter( vProof, vRoots, 0 );
+    vUsed = Proof_CollectUsedIter( vProof, NULL, hNode );
     // collect core clauses 
-    vCore = Vec_IntAlloc( 1000 );
-    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
-    {
-        pNode->Id = 0;
-        Proof_NodeForeachLeaf( vRoots, pNode, pFanin, k )
-            if ( pFanin && !pFanin->mark )
-            {
-                pFanin->mark = 1;
-                Vec_IntPush( vCore, Proof_NodeHandle(vRoots, pFanin) );
-            }
-    }
-    // clean core clauses
-    Proof_ForeachNodeVec( vCore, vRoots, pNode, i )
-        pNode->mark = 0;
+    vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed );
     Vec_IntFree( vUsed );
-    printf( "Collected %d core clauses.  ", Vec_IntSize(vCore) );
-    Abc_PrintTime( 1, "Time", clock() - clk );
     return vCore;
 }
 
@@ -514,20 +498,23 @@ Vec_Int_t * Sat_ProofCore( Vec_Int_t * vProof, Vec_Int_t * vRoots )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot, Vec_Int_t * vGlobVars )
+Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hNode, Vec_Int_t * vGlobVars )
 {
-    Vec_Int_t * vUsed, * vCore, * vVarMap;
-    Vec_Int_t * vUsedNums, * vCoreNums;
+    Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap;
     satset * pNode, * pFanin;
     Aig_Man_t * pAig;
     Aig_Obj_t * pObj;
     int i, k, iVar, Entry;
 
-    // collect core clauses
-    vCore = Sat_ProofCore( vProof, vClauses );
-    // collect visited clauses
-    vUsed = Proof_CollectUsedRec( vProof, NULL, hRoot );
-    Proof_CleanCollected( vProof, vUsed );
+    // collect visited nodes
+    vUsed = Proof_CollectUsedIter( vProof, NULL, hNode );
+    // collect core clauses (cleans vUsed and vCore)
+    vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed );
+
+    // map variables into their global numbers
+    vVarMap = Vec_IntStartFull( Vec_IntFindMax(vGlobVars) + 1 );
+    Vec_IntForEachEntry( vGlobVars, Entry, i )
+        Vec_IntWriteEntry( vVarMap, Entry, i );
 
     // start the AIG
     pAig = Aig_ManStart( 10000 );
@@ -535,11 +522,6 @@ Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int
     for ( i = 0; i < Vec_IntSize(vGlobVars); i++ )
         Aig_ObjCreatePi( pAig );
 
-    // map variables into their global numbers
-    vVarMap = Vec_IntStartFull( Vec_IntFindMax(vGlobVars) + 1 );
-    Vec_IntForEachEntry( vGlobVars, Entry, i )
-        Vec_IntWriteEntry( vVarMap, Entry, i );
-
     // copy the numbers out and derive interpol for clause
     vCoreNums = Vec_IntAlloc( Vec_IntSize(vCore) );
     Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
@@ -547,7 +529,7 @@ Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int
         if ( pNode->partA )
         {
             pObj = Aig_ManConst0( pAig );
-            satset_foreach_var( pNode, iVar, k )
+            satset_foreach_var( pNode, iVar, k, 0 )
                 if ( iVar < Vec_IntSize(vVarMap) && Vec_IntEntry(vVarMap, iVar) >= 0 )
                     pObj = Aig_Or( pAig, pObj, Aig_IthVar(pAig, iVar) );
         }
@@ -560,24 +542,23 @@ Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int
     Vec_IntFree( vVarMap );
 
     // copy the numbers out and derive interpol for resolvents
-    vUsedNums = Vec_IntAlloc( Vec_IntSize(vUsed) );
     Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
     {
         assert( pNode->nEnts > 1 );
         Proof_NodeForeachFaninRoot( vProof, vClauses, pNode, pFanin, k )
         {
             if ( k == 0 )
-                pObj = Aig_ObjFromLit(pAig, pFanin->Id);
+                pObj = Aig_ObjFromLit( pAig, pFanin->Id );
             else if ( pNode->pEnts[k] & 2 ) // variable of A
                 pObj = Aig_Or( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) );
             else
                 pObj = Aig_And( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) );
         }
         // remember the interpolant
-        Vec_IntPush( vUsedNums, pNode->Id );
         pNode->Id = Aig_ObjToLit(pObj);
     }
     // save the result
+    assert( Proof_NodeHandle(vProof, pNode) == hNode );
     Aig_ObjCreatePo( pAig, pObj );
     Aig_ManCleanup( pAig );
 
@@ -585,23 +566,14 @@ Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int
     Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
         pNode->Id = Vec_IntEntry( vCoreNums, i );
     Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
-        pNode->Id = Vec_IntEntry( vUsedNums, i );
+        pNode->Id = 0;
     // cleanup
     Vec_IntFree( vCore );
     Vec_IntFree( vUsed );
     Vec_IntFree( vCoreNums );
-    Vec_IntFree( vUsedNums );
     return pAig;
 }
 
-/*
-    Sat_ProofTest( 
-        &s->clauses,      // clauses
-        &s->proof_clas,   // proof clauses
-        NULL,             // proof roots
-        veci_begin(&s->claProofs)[clause_read(s, s->iLearntLast)->Id)],  // one root
-        &s->glob_vars );  // global variables (for interpolation)
-*/
 
 /**Function*************************************************************
 
@@ -621,36 +593,30 @@ void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pRoots, int hRoot )
     Vec_Int_t * vRoots    = (Vec_Int_t *)pRoots;
     Vec_Int_t * vUsed, * vCore;
 //    int i, Entry;
-
+/*
     // collect visited clauses
     vUsed = Proof_CollectUsedRec( vProof, NULL, hRoot );
     Proof_CleanCollected( vProof, vUsed );
     printf( "Found %d useful resolution nodes.\n", Vec_IntSize(vUsed) );
     Vec_IntFree( vUsed );
-
+*/
     // collect visited clauses
     vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
     Proof_CleanCollected( vProof, vUsed );
     printf( "Found %d useful resolution nodes.\n", Vec_IntSize(vUsed) );
     Vec_IntFree( vUsed );
 
-    vCore = Sat_ProofCore( vProof, vClauses );
+    vCore = Sat_ProofCore( vClauses, vProof, hRoot );
     Vec_IntFree( vCore );
 
-
-
-//    Vec_IntForEachEntry( vUsed, Entry, i )
-//        printf( "%d ", Entry );
-//    printf( "\n" );
 /*
     printf( "Found %d useful resolution nodes.\n", Vec_IntSize(vUsed) );
     Vec_IntFree( vUsed );
     vUsed = Proof_CollectAll( vProof );
     printf( "Found %d total  resolution nodes.\n", Vec_IntSize(vUsed) );
     Vec_IntFree( vUsed );
-
-    Proof_Check( vClauses, vProof, hRoot );
 */
+    Proof_Check( vClauses, vProof, hRoot );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index cde37116..325f69cc 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -600,9 +600,7 @@ static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first)
         return -1;
     proof_chain_start( s, conf );
     assert( veci_size(&s->tagged) == 0 );
-    for ( i = skip_first; i < (int)conf->nEnts; i++ )
-    {
-        x = lit_var(conf->pEnts[i]);
+    satset_foreach_var( conf, x, i, skip_first ){
         if ( var_level(s,x) )
             var_set_tag(s, x, 1);
         else
@@ -616,13 +614,12 @@ static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first)
             satset* c = clause_read(s, var_reason(s,x));
             if (c){
                 proof_chain_resolve( s, c, x );
-                for (j = 1; j < (int)c->nEnts; j++) {
-                    x = lit_var(c->pEnts[j]);
+                satset_foreach_var( c, x, j, 1 ){
                     if ( var_level(s,x) )
                         var_set_tag(s, x, 1);
                     else
                         proof_chain_resolve( s, NULL, x );
-                }
+                } 
             }else {
                 assert( var_level(s,x) );
                 veci_push(&s->conf_final,lit_neg(s->trail[i]));
@@ -656,8 +653,7 @@ static int solver2_lit_removable_rec(sat_solver2* s, int v)
         return 0;
     }
 
-    for ( i = 1; i < (int)c->nEnts; i++ ){
-        x = lit_var(c->pEnts[i]);
+    satset_foreach_var( c, x, i, 1 ){
         if (var_tag(s,x) & 1)
             solver2_lit_removable_rec(s, x);
         else{
@@ -704,8 +700,7 @@ static int solver2_lit_removable(sat_solver2* s, int x)
         }
         x >>= 1;
         c = clause_read(s, var_reason(s,x));
-        for (i = 1; i < (int)c->nEnts; i++){
-            x = lit_var(c->pEnts[i]);
+        satset_foreach_var( c, x, i, 1 ){
             if (var_tag(s,x) || !var_level(s,x))
                 continue;
             if (!var_reason(s,x) || !var_lev_mark(s,x)){
@@ -740,8 +735,7 @@ static void solver2_logging_order(sat_solver2* s, int x)
         c = clause_read(s, var_reason(s,x));
 //        if ( !c )
 //            printf( "solver2_logging_order(): Error in conflict analysis!!!\n" );
-        for (i = 1; i < (int)c->nEnts; i++){
-            x = lit_var(c->pEnts[i]);
+        satset_foreach_var( c, x, i, 1 ){
             if ( !var_level(s,x) || (var_tag(s,x) & 1) )
                 continue;
             veci_push(&s->stack, x << 1);
@@ -757,11 +751,9 @@ static void solver2_logging_order_rec(sat_solver2* s, int x)
     if ( (var_tag(s,x) & 8) )
         return;
     c = clause_read(s, var_reason(s,x));
-    for (i = 1; i < (int)c->nEnts; i++){
-        y = lit_var(c->pEnts[i]);
+    satset_foreach_var( c, y, i, 1 )
         if ( var_level(s,y) && (var_tag(s,y) & 1) == 0 )
             solver2_logging_order_rec(s, y);
-    }
     var_add_tag(s, x, 8);
     veci_push(&s->min_step_order, x);
 }
@@ -769,7 +761,7 @@ static void solver2_logging_order_rec(sat_solver2* s, int x)
 static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
 {
     int cnt      = 0;
-    lit p        = lit_Undef;
+    lit p        = 0;
     int x, ind   = s->qtail-1;
     int proof_id = 0;
     lit* lits,* vars, i, j, k;
@@ -784,8 +776,7 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
         assert(c != 0);
         if (c->learnt)
             act_clause_bump(s,c);
-        for ( j = (int)(p != lit_Undef); j < (int)c->nEnts; j++){
-            x = lit_var(c->pEnts[j]);
+        satset_foreach_var( c, x, j, (int)(p > 0) ){
             assert(x >= 0 && x < s->size);
             if ( var_tag(s, x) )
                 continue;
@@ -822,7 +813,7 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
     // simplify (full)
     veci_resize(&s->min_lit_order, 0);
     for (i = j = 1; i < veci_size(learnt); i++){
-//        if (!solver2_lit_removable( s,lit_var(lits[i])) )
+//        if (!solver2_lit_removable( s,lit_var(lits[i])))
         if (!solver2_lit_removable_rec(s,lit_var(lits[i]))) // changed to vars!!!
             lits[j++] = lits[i];
     } 
@@ -834,20 +825,17 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
         veci_resize(&s->min_step_order, 0);
         vars = veci_begin(&s->min_lit_order);
         for (i = 0; i < veci_size(&s->min_lit_order); i++)
-//            solver2_logging_order( s, vars[i] );
-            solver2_logging_order_rec( s, vars[i] );
+//            solver2_logging_order(s, vars[i]);
+            solver2_logging_order_rec(s, vars[i]);
 
         // add them in the reverse order
         vars = veci_begin(&s->min_step_order);
         for (i = veci_size(&s->min_step_order); i > 0; ) { i--;
             c = clause_read(s, var_reason(s,vars[i]));
             proof_chain_resolve( s, c, vars[i] );
-            for ( k = 1; k < (int)c->nEnts; k++ )
-            {
-                x = lit_var(c->pEnts[k]);
+            satset_foreach_var(c, x, k, 1)
                 if ( var_level(s,x) == 0 )
                     proof_chain_resolve( s, NULL, x );
-            }
         }
         proof_id = proof_chain_stop( s );
     }
@@ -940,13 +928,11 @@ satset* solver2_propagate(sat_solver2* s)
 
                 // Did not find watch -- clause is unit under assignment:
                 if (s->fProofLogging && solver2_dlevel(s) == 0){
-                    int k, proof_id, Cid, Var = lit_var(lits[0]);
+                    int k, x, proof_id, Cid, Var = lit_var(lits[0]);
                     int fLitIsFalse = (var_value(s, Var) == !lit_sign(lits[0])); 
                     // Log production of top-level unit clause:
                     proof_chain_start( s, c );
-                    for ( k = 1; k < (int)c->nEnts; k++ )
-                    {
-                        int x = lit_var(c->pEnts[k]);
+                    satset_foreach_var( c, x, k, 1 ){
                         assert( var_level(s, x) == 0 );
                         proof_chain_resolve( s, NULL, x );
                     }
@@ -1007,12 +993,11 @@ static void clause_remove(sat_solver2* s, satset* c)
 
 static lbool clause_simplify(sat_solver2* s, satset* c)
 {
-    int i;
+    int i, x;
     assert(solver2_dlevel(s) == 0);
-    for (i = 0; i < (int)c->nEnts; i++){
-        if (var_value(s, lit_var(c->pEnts[i])) == lit_sign(c->pEnts[i]))
+    satset_foreach_var( c, x, i, 0 )
+        if (var_value(s, x) == lit_sign(c->pEnts[i]))
             return l_True;
-    }
     return l_False;
 }
 
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index e091d488..d77c0141 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -176,13 +176,10 @@ static inline void    satset_print  (satset * c)          {
     printf( "}\n" );
 }
 
-#define satset_foreach_entry( p, c, h, s )  \
+#define satset_foreach_entry( p, c, h, s )            \
     for ( h = s; (h < veci_size(p)) && (((c) = satset_read(p, h)), 1); h += satset_size(c->nEnts) )
-#define satset_foreach_var( p, var, i )        \
-    for ( i = 0; (i < (int)(p)->nEnts) && ((var) = lit_var((p)->pEnts[i])); i++ )
-#define satset_foreach_lit( p, lit, i )        \
-    for ( i = 0; (i < (int)(p)->nEnts) && ((lit) = (p)->pEnts[i]); i++ )
-
+#define satset_foreach_var( p, var, i, start )        \
+    for ( i = start; (i < (int)(p)->nEnts) && ((var) = lit_var((p)->pEnts[i])); i++ )
 
 //=================================================================================================
 // Public APIs: