Improved memory management of proof-logging and propagated changes.

4 files changed, 130 insertions, 37 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 2de1a0b2..d10fd390 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1259,10 +1259,6 @@ SOURCE=.\src\sat\bsat\satVec.h
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\sat\bsat\vecRec.h
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\sat\bsat\vecSet.h
 # End Source File
 # End Group
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index dcb02bcd..81adb18b 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -102,7 +102,7 @@ void Proof_CleanCollected( Vec_Set_t * vProof, Vec_Int_t * vUsed )
 
 /**Function*************************************************************
 
-  Synopsis    [Marks useful nodes of the proof.]
+  Synopsis    []
 
   Description []
                
@@ -141,18 +141,6 @@ void Proof_CollectUsed_iter( Vec_Set_t * vProof, int hNode, Vec_Int_t * vUsed, V
             }
     }
 }
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively visits useful proof nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 Vec_Int_t * Proof_CollectUsedIter( Vec_Set_t * vProof, Vec_Int_t * vRoots, int fSort )
 {
     int fVerify = 0;
@@ -186,7 +174,7 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Set_t * vProof, Vec_Int_t * vRoots, int f
 
 /**Function*************************************************************
 
-  Synopsis    [Recursively visits useful proof nodes.]
+  Synopsis    [Recursively collects useful proof nodes.]
 
   Description []
                
@@ -207,6 +195,16 @@ void Proof_CollectUsed_rec( Vec_Set_t * vProof, int hNode, Vec_Int_t * vUsed )
             Proof_CollectUsed_rec( vProof, pNode->pEnts[i] >> 2, vUsed );
     Vec_IntPush( vUsed, hNode );
 }
+Vec_Int_t * Proof_CollectUsedRec( Vec_Set_t * vProof, Vec_Int_t * vRoots )
+{
+    Vec_Int_t * vUsed;
+    int i, Entry;
+    vUsed = Vec_IntAlloc( 1000 );
+    Vec_IntForEachEntry( vRoots, Entry, i )
+        if ( Entry >= 0 )
+            Proof_CollectUsed_rec( vProof, Entry, vUsed );
+    return vUsed;
+}
 
 /**Function*************************************************************
 
@@ -219,15 +217,25 @@ void Proof_CollectUsed_rec( Vec_Set_t * vProof, int hNode, Vec_Int_t * vUsed )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Proof_CollectUsedRec( Vec_Set_t * vProof, Vec_Int_t * vRoots )
+int Proof_MarkUsed_rec( Vec_Set_t * vProof, int hNode )
 {
-    Vec_Int_t * vUsed;
-    int i, Entry;
-    vUsed = Vec_IntAlloc( 1000 );
+    satset * pNext, * pNode = Proof_NodeRead( vProof, hNode );
+    int i, Counter = 1;
+    if ( pNode->Id )
+        return 0;
+    pNode->Id = 1;
+    Proof_NodeForeachFanin( vProof, pNode, pNext, i )
+        if ( pNext && !pNext->Id )
+            Counter += Proof_MarkUsed_rec( vProof, pNode->pEnts[i] >> 2 );
+    return Counter;
+}
+int Proof_MarkUsedRec( Vec_Set_t * vProof, Vec_Int_t * vRoots )
+{
+    int i, Entry, Counter = 0;
     Vec_IntForEachEntry( vRoots, Entry, i )
         if ( Entry >= 0 )
-            Proof_CollectUsed_rec( vProof, Entry, vUsed );
-    return vUsed;
+            Counter += Proof_MarkUsed_rec( vProof, Entry );
+    return Counter;
 }
 
 
@@ -292,7 +300,7 @@ void Sat_ProofReduceCheck( sat_solver2 * s )
   SeeAlso     []
 
 ***********************************************************************/
-void Sat_ProofReduce( sat_solver2 * s )
+void Sat_ProofReduce2( sat_solver2 * s )
 {
     Vec_Set_t * vProof   = (Vec_Set_t *)&s->Proofs;
     Vec_Int_t * vRoots   = (Vec_Int_t *)&s->claProofs;
@@ -300,7 +308,7 @@ void Sat_ProofReduce( sat_solver2 * s )
 
     int fVerbose = 0;
     Vec_Int_t * vUsed;
-    satset * pNode, * pFanin;
+    satset * pNode, * pFanin, * pPivot;
     int i, k, hTemp, clk = clock();
     static int TimeTotal = 0;
 
@@ -321,11 +329,22 @@ void Sat_ProofReduce( sat_solver2 * s )
     // update roots
     Proof_ForeachNodeVec1( vRoots, vProof, pNode, i )
         Vec_IntWriteEntry( vRoots, i, pNode->Id );
+    // determine new pivot
+    assert( s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(vProof) );
+    pPivot = Proof_NodeRead( vProof, s->hProofPivot );
+    s->hProofPivot = Vec_SetHandCurrentS(vProof);
+    s->iProofPivot = Vec_IntSize(vUsed);
     // compact the nodes
     Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
     {
         hTemp = pNode->Id; pNode->Id = 0;
         memmove( Vec_SetEntry(vProof, hTemp), pNode, sizeof(word)*Proof_NodeWordNum(pNode->nEnts) );
+        if ( pPivot && pPivot <= pNode )
+        { 
+            s->hProofPivot = hTemp;
+            s->iProofPivot = i;
+            pPivot = NULL;
+        }
     }
     Vec_SetWriteEntryNum( vProof, Vec_IntSize(vUsed) );
     Vec_IntFree( vUsed );
@@ -333,6 +352,7 @@ void Sat_ProofReduce( sat_solver2 * s )
     // report the result
     if ( fVerbose )
     {
+        printf( "\n" );
         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) );
@@ -341,6 +361,75 @@ void Sat_ProofReduce( sat_solver2 * s )
     }
     Vec_SetShrink( vProof, Vec_SetHandCurrentS(vProof) );
     Sat_ProofReduceCheck( s );
+} 
+
+void Sat_ProofReduce( sat_solver2 * s )
+{
+    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_Ptr_t * vUsed;
+    satset * pNode, * pFanin, * pPivot;
+    int i, j, k, hTemp, nSize, clk = clock();
+    static int TimeTotal = 0;
+
+    // collect visited nodes
+    nSize = Proof_MarkUsedRec( vProof, vRoots );
+    vUsed = Vec_PtrAlloc( nSize );
+
+    // relabel nodes to use smaller space
+    Vec_SetShrinkS( vProof, 1 );
+    Vec_SetForEachEntry( satset *, vProof, nSize, pNode, i, j )
+    {
+        nSize = Vec_SetWordNum( 2 + pNode->nEnts );
+        if ( pNode->Id == 0 ) 
+            continue;
+        pNode->Id = Vec_SetAppendS( vProof, 2 + pNode->nEnts );
+        Vec_PtrPush( vUsed, pNode );
+        // update fanins
+        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);
+            else // problem clause
+                assert( (int*)pFanin >= Vec_IntArray(vClauses) && (int*)pFanin < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) );
+    }
+    // update roots
+    Proof_ForeachNodeVec1( vRoots, vProof, pNode, i )
+        Vec_IntWriteEntry( vRoots, i, pNode->Id );
+    // determine new pivot
+    assert( s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(vProof) );
+    pPivot = Proof_NodeRead( vProof, s->hProofPivot );
+    s->hProofPivot = Vec_SetHandCurrentS(vProof);
+    s->iProofPivot = Vec_PtrSize(vUsed);
+    // compact the nodes
+    Vec_PtrForEachEntry( satset *, vUsed, pNode, i )
+    {
+        hTemp = pNode->Id; pNode->Id = 0;
+        memmove( Vec_SetEntry(vProof, hTemp), pNode, sizeof(word)*Proof_NodeWordNum(pNode->nEnts) );
+        if ( pPivot && pPivot <= pNode )
+        {
+            s->hProofPivot = hTemp;
+            s->iProofPivot = i;
+            pPivot = NULL;
+        }
+    }
+    Vec_SetWriteEntryNum( vProof, Vec_PtrSize(vUsed) );
+    Vec_PtrFree( vUsed );
+
+    // report the result
+    if ( fVerbose )
+    {
+        printf( "\n" );
+        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_SetShrink( vProof, Vec_SetHandCurrentS(vProof) );
+    Vec_SetShrinkLimits( vProof );
+//    Sat_ProofReduceCheck( s );
 }
 
 
@@ -788,8 +877,7 @@ void * Sat_ProofCore( sat_solver2 * s )
     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;
-    hRoot = s->hProofLast;
+    int hRoot = s->hProofLast;
     if ( hRoot == -1 )
         return NULL;
     // collect visited clauses
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 34908f13..a58cf22b 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -1403,7 +1403,7 @@ void sat_solver2_reducedb(sat_solver2* s)
     cla h,* pArray,* pArray2;
     int * pPerm, * pClaAct, nClaAct, ActCutOff;
     int i, j, k, hTemp, hHandle, clk = clock();
-    int Counter, CounterStart;
+    int Counter, CounterStart, LastSize;
 
     // check if it is time to reduce
     if ( s->nLearntMax == 0 || s->stats.learnts < (unsigned)s->nLearntMax )
@@ -1487,14 +1487,15 @@ void sat_solver2_reducedb(sat_solver2* s)
     satset_foreach_entry_vec( &s->learnt_live, &s->learnts, c, i )
     {
         hTemp = c->Id; c->Id = i + 1;
-        memmove( veci_begin(&s->learnts) + hTemp, c, sizeof(int)*satset_size(c->nEnts) );
+        LastSize = satset_size(c->nEnts);
+        memmove( veci_begin(&s->learnts) + hTemp, c, sizeof(int)*LastSize );
         if ( pivot && pivot <= c )
         {
             s->hLearntPivot = hTemp;
             pivot = NULL;
         }
     }
-    assert( hHandle == hTemp + satset_size(c->nEnts) );
+    assert( hHandle == hTemp + LastSize );
     veci_resize(&s->learnts,hHandle);
     s->stats.learnts = veci_size(&s->learnt_live);
     assert( s->hLearntPivot <= veci_size(&s->learnts) );
@@ -1560,9 +1561,9 @@ void sat_solver2_rollback( sat_solver2* s )
         veci_resize(&s->claActs,   first->Id);
         if ( s->fProofLogging ) {
             veci_resize(&s->claProofs, first->Id);
-            Vec_SetWriteEntryNum(&s->Proofs, s->iProofPivot);
-            Vec_SetShrink(&s->Proofs, s->hProofPivot);
-//            Sat_ProofReduce( s );
+//            Vec_SetWriteEntryNum(&s->Proofs, s->iProofPivot); // <- some bug here
+//            Vec_SetShrink(&s->Proofs, s->hProofPivot);
+            Sat_ProofReduce( s );
         }
         s->stats.learnts = first->Id-1;
         veci_resize(&s->learnts, s->hLearntPivot);
diff --git a/src/sat/bsat/vecSet.h b/src/sat/bsat/vecSet.h
index e95c3332..b1c4de63 100644
--- a/src/sat/bsat/vecSet.h
+++ b/src/sat/bsat/vecSet.h
@@ -61,6 +61,7 @@ struct Vec_Set_t_
 
 static inline int     Vec_SetHandPage( int h )                   { return h >> 16;                }
 static inline int     Vec_SetHandShift( int h )                  { return h & 0xFFFF;             }
+static inline int     Vec_SetWordNum( int nSize )                { return (nSize + 1) >> 1;       }
 
 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;            }
@@ -181,7 +182,7 @@ static inline void Vec_SetFree( Vec_Set_t * p )
 ***********************************************************************/
 static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize )
 {
-    int nWords = (nSize + 1) >> 1;
+    int nWords = Vec_SetWordNum( nSize );
     assert( nWords < 0x10000 );
     p->nEntries++;
     if ( Vec_SetLimit( p->pPages[p->iPage] ) + nWords > 0x10000 )
@@ -198,13 +199,13 @@ static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize )
         Vec_SetWriteLimit( p->pPages[p->iPage], 1 );
     }
     if ( pArray )
-    memmove( p->pPages[p->iPage] + Vec_SetLimit(p->pPages[p->iPage]), pArray, sizeof(int) * nSize );
+        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;
+    int nWords = Vec_SetWordNum( nSize );
     assert( nWords < 0x10000 );
     if ( Vec_SetLimitS( p->pPages[p->iPageS] ) + nWords > 0x10000 )
         Vec_SetWriteLimitS( p->pPages[++p->iPageS], 1 );
@@ -236,6 +237,13 @@ static inline void Vec_SetShrinkS( Vec_Set_t * p, int h )
     Vec_SetWriteLimitS( p->pPages[p->iPageS], Vec_SetHandShift(h) );  
 }
 
+static inline void Vec_SetShrinkLimits( Vec_Set_t * p )
+{
+    int i;
+    for ( i = 0; i <= p->iPage; i++ )
+        Vec_SetWriteLimit( p->pPages[i], Vec_SetLimitS(p->pPages[i]) );
+}
+
 
 ABC_NAMESPACE_HEADER_END