From 16dc02e7f6b9c22ecea2c878c9bb63d34264d378 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 16 Feb 2012 20:54:41 -0800 Subject: Improved memory management of proof-logging and propagated changes. --- abclib.dsp | 4 -- src/sat/bsat/satProof.c | 136 ++++++++++++++++++++++++++++++++++++++-------- src/sat/bsat/satSolver2.c | 13 +++-- src/sat/bsat/vecSet.h | 14 ++++- 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 -- cgit v1.2.3