Proof-logging in the updated solver.

3 files changed, 163 insertions, 65 deletions

diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index 8fa17e94..a06dd412 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -64,10 +64,11 @@ static inline int     Proof_NodeSize   (int nEnts)                { return sizeo
 #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 )    \
-    for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = ((pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(p, pNode->pEnts[i] >> 1))), 1); i++ )
-#define Proof_NodeForeachFanin2( p, pNode, pFanin, iFanin, i )    \
-    for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = ((pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(p, pNode->pEnts[i] >> 1))), ((iFanin) = ((pNode->pEnts[i] & 1) ? pNode->pEnts[i] >> 1 : 0)), 1); 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++ )
+#define Proof_NodeForeachFaninRoot( p, pLeaves, pNode, pFanin, i )    \
+    for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pLeaves, pNode->pEnts[i] >> 2) : Proof_NodeRead(p, pNode->pEnts[i] >> 2)); i++ )
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -125,7 +126,7 @@ void Proof_CleanCollected( Vec_Int_t * vProof, Vec_Int_t * vUsed )
   SeeAlso     []
 
 ***********************************************************************/
-void Proof_CollectUsedInt( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed, Vec_Int_t * vStack )
+void Proof_CollectUsed_iter( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed, Vec_Int_t * vStack )
 {
     satset * pNext;
     int i, hNode;
@@ -167,7 +168,37 @@ void Proof_CollectUsedInt( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed, Vec
   SeeAlso     []
 
 ***********************************************************************/
-void Proof_CollectUsedRec( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed )
+Vec_Int_t * Proof_CollectUsedIter( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hRoot )
+{
+    Vec_Int_t * vUsed, * vStack;
+    assert( (hRoot > 0) ^ (vRoots != NULL) );
+    vUsed = Vec_IntAlloc( 1000 );
+    vStack = Vec_IntAlloc( 1000 );
+    if ( hRoot )
+        Proof_CollectUsed_iter( vProof, Proof_NodeRead(vProof, hRoot), vUsed, vStack );
+    else
+    {
+        satset * pNode;
+        int i;
+        Proof_ForeachNodeVec( vRoots, vProof, pNode, i )
+            Proof_CollectUsed_iter( vProof, pNode, vUsed, vStack );
+    }
+    Vec_IntFree( vStack );
+    return vUsed;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively visits useful proof nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Proof_CollectUsed_rec( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed )
 {
     satset * pNext;
     int i;
@@ -176,7 +207,7 @@ void Proof_CollectUsedRec( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed )
     pNode->Id = 1;
     Proof_NodeForeachFanin( p, pNode, pNext, i )
         if ( pNext && !pNext->Id )
-            Proof_CollectUsedRec( p, pNext, vUsed );
+            Proof_CollectUsed_rec( p, pNext, vUsed );
     Vec_IntPush( vUsed, Proof_NodeHandle(p, pNode) );
 }
 
@@ -191,22 +222,20 @@ void Proof_CollectUsedRec( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Proof_CollectUsed( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hRoot )
+Vec_Int_t * Proof_CollectUsedRec( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hRoot )
 {
     Vec_Int_t * vUsed, * vStack;
     assert( (hRoot > 0) ^ (vRoots != NULL) );
     vUsed = Vec_IntAlloc( 1000 );
     vStack = Vec_IntAlloc( 1000 );
     if ( hRoot )
-//        Proof_CollectUsedInt( vProof, Proof_NodeRead(vProof, hRoot), vUsed, vStack );
-        Proof_CollectUsedRec( vProof, Proof_NodeRead(vProof, hRoot), vUsed );
+        Proof_CollectUsed_rec( vProof, Proof_NodeRead(vProof, hRoot), vUsed );
     else
     {
         satset * pNode;
         int i;
         Proof_ForeachNodeVec( vRoots, vProof, pNode, i )
-//            Proof_CollectUsedInt( vProof, pNode, vUsed, vStack );
-            Proof_CollectUsedRec( vProof, pNode, vUsed );
+            Proof_CollectUsed_rec( vProof, pNode, vUsed );
     }
     Vec_IntFree( vStack );
     return vUsed;
@@ -279,9 +308,9 @@ satset * Proof_CheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t
 {
     satset * pAnt;
     if ( iAnt & 1 )
-        return Proof_NodeRead( vClauses, iAnt >> 1 );
+        return Proof_NodeRead( vClauses, iAnt >> 2 );
     assert( iAnt > 0 );
-    pAnt = Proof_NodeRead( vProof, iAnt >> 1 );
+    pAnt = Proof_NodeRead( vProof, iAnt >> 2 );
     assert( pAnt->Id > 0 );
     return Proof_NodeRead( vResolves, pAnt->Id );
 }
@@ -303,7 +332,7 @@ void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot )
     satset * pSet, * pSet0, * pSet1;
     int i, k, Counter = 0, clk = clock(); 
     // collect visited clauses
-    vUsed = Proof_CollectUsed( vProof, NULL, hRoot );
+    vUsed = Proof_CollectUsedRec( vProof, NULL, hRoot );
     Proof_CleanCollected( vProof, vUsed );
     // perform resolution steps
     vTemp = Vec_IntAlloc( 1000 );
@@ -433,6 +462,8 @@ void Sat_ProofReduce( Vec_Int_t * p, Vec_Int_t * vRoots )
     Vec_IntShrink( p, nSize );
 }
 
+
+
 /**Function*************************************************************
 
   Synopsis    [Computes UNSAT core.]
@@ -444,29 +475,31 @@ void Sat_ProofReduce( Vec_Int_t * p, Vec_Int_t * vRoots )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Sat_ProofCore( Vec_Int_t * vProof, int nRoots, Vec_Int_t * vRoots )
+Vec_Int_t * Sat_ProofCore( Vec_Int_t * vProof, Vec_Int_t * vRoots )
 {
-    unsigned * pSeen;
     Vec_Int_t * vCore, * vUsed;
-    satset * pNode;
-    int i, * pBeg;
+    satset * pNode, * pFanin;
+    int i, k, clk = clock();;
     // collect visited clauses
-    vUsed = Proof_CollectUsed( vProof, vRoots, 0 );
-    // find the core
+    vUsed = Proof_CollectUsedIter( vProof, vRoots, 0 );
+    // collect core clauses 
     vCore = Vec_IntAlloc( 1000 );
-    pSeen = ABC_CALLOC( unsigned, Aig_BitWordNum(nRoots) );
     Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
     {
         pNode->Id = 0;
-        for ( pBeg = pNode->pEnts; pBeg < pNode->pEnts + pNode->nEnts; pBeg++ )
-            if ( (*pBeg & 1) && !Aig_InfoHasBit((unsigned *)pBeg, *pBeg>>1) )
+        Proof_NodeForeachLeaf( vRoots, pNode, pFanin, k )
+            if ( pFanin && !pFanin->mark )
             {
-                Aig_InfoSetBit( (unsigned *)pBeg, *pBeg>>1 );
-                Vec_IntPush( vCore, (*pBeg>>1)-1 );
+                pFanin->mark = 1;
+                Vec_IntPush( vCore, Proof_NodeHandle(vRoots, pFanin) );
             }
     }
+    // clean core clauses
+    Proof_ForeachNodeVec( vCore, vRoots, pNode, i )
+        pNode->mark = 0;
     Vec_IntFree( vUsed );
-    ABC_FREE( pSeen );
+    printf( "Collected %d core clauses.  ", Vec_IntSize(vCore) );
+    Abc_PrintTime( 1, "Time", clock() - clk );
     return vCore;
 }
 
@@ -474,7 +507,7 @@ Vec_Int_t * Sat_ProofCore( Vec_Int_t * vProof, int nRoots, Vec_Int_t * vRoots )
 
   Synopsis    [Computes interpolant of the proof.]
 
-  Description [Aassuming that global vars and A-clauses are marked.]
+  Description [Aassuming that vars/clause of partA are marked.]
                
   SideEffects []
 
@@ -483,19 +516,81 @@ Vec_Int_t * Sat_ProofCore( Vec_Int_t * vProof, int nRoots, Vec_Int_t * vRoots )
 ***********************************************************************/
 Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot, Vec_Int_t * vGlobVars )
 {
-    Vec_Int_t * vUsed;
+    Vec_Int_t * vUsed, * vCore, * vVarMap;
+    Vec_Int_t * vUsedNums, * vCoreNums;
+    satset * pNode, * pFanin;
     Aig_Man_t * pAig;
-    int i;
+    Aig_Obj_t * pObj;
+    int i, k, iVar, Entry;
 
+    // collect core clauses
+    vCore = Sat_ProofCore( vProof, vClauses );
     // collect visited clauses
-    vUsed = Proof_CollectUsed( vProof, NULL, hRoot );
+    vUsed = Proof_CollectUsedRec( vProof, NULL, hRoot );
+    Proof_CleanCollected( vProof, vUsed );
 
     // start the AIG
     pAig = Aig_ManStart( 10000 );
     pAig->pName = Aig_UtilStrsav( "interpol" );
     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 )
+    {
+        if ( pNode->partA )
+        {
+            pObj = Aig_ManConst0( pAig );
+            satset_foreach_var( pNode, iVar, k )
+                if ( iVar < Vec_IntSize(vVarMap) && Vec_IntEntry(vVarMap, iVar) >= 0 )
+                    pObj = Aig_Or( pAig, pObj, Aig_IthVar(pAig, iVar) );
+        }
+        else
+            pObj = Aig_ManConst1( pAig );
+        // remember the interpolant
+        Vec_IntPush( vCoreNums, pNode->Id );
+        pNode->Id = Aig_ObjToLit(pObj);
+    }
+    Vec_IntFree( vVarMap );
+
+    // copy the numbers out and derive interpol for resolvents
+    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);
+            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
+    Aig_ObjCreatePo( pAig, pObj );
+    Aig_ManCleanup( pAig );
+
+    // move the results back
+    Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
+        pNode->Id = Vec_IntEntry( vCoreNums, i );
+    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
+        pNode->Id = Vec_IntEntry( vUsedNums, i );
+    // cleanup
+    Vec_IntFree( vCore );
+    Vec_IntFree( vUsed );
+    Vec_IntFree( vCoreNums );
+    Vec_IntFree( vUsedNums );
     return pAig;
 }
 
@@ -503,7 +598,6 @@ Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int
     Sat_ProofTest( 
         &s->clauses,      // clauses
         &s->proof_clas,   // proof clauses
-        &s->proof_vars,   // proof variables
         NULL,             // proof roots
         veci_begin(&s->claProofs)[clause_read(s, s->iLearntLast)->Id)],  // one root
         &s->glob_vars );  // global variables (for interpolation)
@@ -520,23 +614,35 @@ Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int
   SeeAlso     []
 
 ***********************************************************************/
-void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pVars, veci * pRoots, int hRoot, veci * pGlobVars )
+void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pRoots, int hRoot )
 {
     Vec_Int_t * vClauses  = (Vec_Int_t *)pClauses;
     Vec_Int_t * vProof    = (Vec_Int_t *)pProof;
-    Vec_Int_t * vVars     = (Vec_Int_t *)pVars;
     Vec_Int_t * vRoots    = (Vec_Int_t *)pRoots;
-    Vec_Int_t * vGlobVars = (Vec_Int_t *)pGlobVars;
-    Vec_Int_t * vUsed;
+    Vec_Int_t * vUsed, * vCore;
 //    int i, Entry;
 
     // collect visited clauses
-    vUsed = Proof_CollectUsed( vProof, NULL, hRoot );
+    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 );
+    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 );
@@ -544,6 +650,7 @@ void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pVars, veci * pRoots,
     Vec_IntFree( vUsed );
 
     Proof_Check( vClauses, vProof, hRoot );
+*/
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 1c9e9dbb..cde37116 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -85,13 +85,13 @@ struct varinfo_t
 {
     unsigned val    :  2;  // variable value 
     unsigned pol    :  1;  // last polarity
-    unsigned glo    :  1;  // global variable
+    unsigned partA  :  1;  // partA variable
     unsigned tag    :  4;  // conflict analysis tags
     unsigned lev    : 24;  // variable level
 };
 
-int    var_is_global (sat_solver2* s, int v)            { return s->vi[v].glo; }
-void   var_set_global(sat_solver2* s, int v, int glo)   { s->vi[v].glo = glo; if (glo) veci_push(&s->glob_vars, v); }
+int    var_is_partA (sat_solver2* s, int v)              { return s->vi[v].partA;  }
+void   var_set_partA(sat_solver2* s, int v, int partA)   { s->vi[v].partA = partA; }
 
 static inline int     var_value     (sat_solver2* s, int v)            { return s->vi[v].val; }
 static inline int     var_polar     (sat_solver2* s, int v)            { return s->vi[v].pol; }
@@ -145,7 +145,7 @@ static inline void    solver2_clear_marks(sat_solver2* s)              {
 static inline satset* clause_read   (sat_solver2* s, cla h)      { return satset_read( &s->clauses, h );    }
 static inline cla     clause_handle (sat_solver2* s, satset* c)  { return satset_handle( &s->clauses, c );  }
 static inline int     clause_check  (sat_solver2* s, satset* c)  { return satset_check( &s->clauses, c );   }
-static inline int     clause_proofid(sat_solver2* s, satset* c)  { return c->learnt ? veci_begin(&s->claProofs)[c->Id]<<1 : (clause_handle(s,c)<<1) | 1;                   }
+static inline int     clause_proofid(sat_solver2* s, satset* c, int partA)  { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (clause_handle(s,c)<<2) | 1; }
 
 //static inline int     var_reason    (sat_solver2* s, int v)      { return (s->reasons[v]&1) ? 0 : s->reasons[v] >> 1;                   } 
 //static inline int     lit_reason    (sat_solver2* s, int l)      { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)] >> 1; } 
@@ -180,10 +180,7 @@ static inline void proof_chain_start( sat_solver2* s, satset* c )
         s->iStartChain = veci_size(&s->proof_clas);
         veci_push(&s->proof_clas, 0);
         veci_push(&s->proof_clas, 0);
-        veci_push(&s->proof_clas, clause_proofid(s, c) );
-        veci_push(&s->proof_vars, 0);
-        veci_push(&s->proof_vars, 0);
-        veci_push(&s->proof_vars, 0);
+        veci_push(&s->proof_clas, clause_proofid(s, c, 0) );
     }
 }
 
@@ -192,8 +189,7 @@ static inline void proof_chain_resolve( sat_solver2* s, satset* cls, int Var )
     if ( s->fProofLogging )
     {
         satset* c = cls ? cls : var_unit_clause( s, Var );
-        veci_push(&s->proof_clas, clause_proofid(s, c) );
-        veci_push(&s->proof_vars, Var);
+        veci_push(&s->proof_clas, clause_proofid(s, c, var_is_partA(s,Var)) );
 //        printf( "%d %d  ", clause_proofid(s, c), Var );
     }
 }
@@ -1225,9 +1221,7 @@ sat_solver2* sat_solver2_new(void)
     veci_new(&s->mark_levels);
     veci_new(&s->min_lit_order); 
     veci_new(&s->min_step_order);
-    veci_new(&s->glob_vars);
     veci_new(&s->proof_clas); veci_push(&s->proof_clas, -1);
-    veci_new(&s->proof_vars); veci_push(&s->proof_vars, -1);
     veci_new(&s->claActs);    veci_push(&s->claActs,    -1);
     veci_new(&s->claProofs);  veci_push(&s->claProofs,  -1);
 
@@ -1256,8 +1250,6 @@ sat_solver2* sat_solver2_new(void)
     {
         s->proof_clas.cap = (1 << 20);
         s->proof_clas.ptr = ABC_REALLOC( int, s->proof_clas.ptr, s->proof_clas.cap );
-        s->proof_vars.cap = (1 << 20);
-        s->proof_vars.ptr = ABC_REALLOC( int, s->proof_vars.ptr, s->proof_clas.cap );
     }
     return s;
 }
@@ -1306,16 +1298,14 @@ void sat_solver2_delete(sat_solver2* s)
 {
     satset * c = clause_read(s, s->iLearntLast);
     // report statistics
-    assert( veci_size(&s->proof_clas) == veci_size(&s->proof_vars) );
-    printf( "Used %6.2f Mb for proof-logging.   Unit clauses = %d.\n", 8.0 * veci_size(&s->proof_clas) / (1<<20), s->nUnits );
+    printf( "Used %6.2f Mb for proof-logging.   Unit clauses = %d.\n", 2.0 * veci_size(&s->proof_clas) / (1<<20), s->nUnits );
 
     Sat_ProofTest( 
         &s->clauses,      // clauses
         &s->proof_clas,   // proof clauses
-        &s->proof_vars,   // proof variables
         NULL,             // proof roots
-        veci_begin(&s->claProofs)[c->Id],  // one root
-        &s->glob_vars );  // global variables (for interpolation)
+        veci_begin(&s->claProofs)[c->Id]  // one root
+         );  
 
     // delete vectors
     veci_delete(&s->order);
@@ -1328,9 +1318,7 @@ void sat_solver2_delete(sat_solver2* s)
     veci_delete(&s->mark_levels);
     veci_delete(&s->min_lit_order);
     veci_delete(&s->min_step_order);
-    veci_delete(&s->glob_vars);
     veci_delete(&s->proof_clas);
-    veci_delete(&s->proof_vars);
     veci_delete(&s->claActs);
     veci_delete(&s->claProofs);
     veci_delete(&s->clauses);
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index 1cdc8bd9..e091d488 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -68,8 +68,8 @@ extern void         sat_solver2_store_mark_clauses_a( sat_solver2 * s );
 extern void *       sat_solver2_store_release( sat_solver2 * s ); 
 
 // global variables
-extern int          var_is_global (sat_solver2* s, int v);
-extern void         var_set_global(sat_solver2* s, int v, int glo);
+extern int          var_is_partA (sat_solver2* s, int v);
+extern void         var_set_partA(sat_solver2* s, int v, int partA);
 // clause grouping (these two only work after creating a clause before the solver is called)
 extern int          clause_is_partA (sat_solver2* s, int handle);
 extern void         clause_set_partA(sat_solver2* s, int handle, int partA);
@@ -143,7 +143,6 @@ struct sat_solver2_t
 
     // proof logging
     veci            proof_clas;     // sequence of proof clauses
-    veci            proof_vars;     // sequence of proof variables 
     int             iStartChain;    // temporary variable to remember beginning of the current chain in proof logging
     int             nUnits;         // the total number of unit clauses
 
@@ -177,9 +176,13 @@ static inline void    satset_print  (satset * c)          {
     printf( "}\n" );
 }
 
-
 #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++ )
+
 
 //=================================================================================================
 // Public APIs:
@@ -245,7 +248,7 @@ static inline int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom)
     return fNotUseRandomOld;
 }
 
-extern void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pVars, veci * pRoots, int hRoot, veci * pGlobVars );
+extern void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pRoots, int hRoot );
 
 ABC_NAMESPACE_HEADER_END