From bbf4b9a58ddb8cada254e0a54ae96564e4e8c06c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 13 Jul 2012 18:47:04 -0700 Subject: Debugging a proof error. --- src/misc/vec/vecSet.h | 42 +++++++++++++++++------------------------- src/sat/bsat/satProof.c | 34 +++++++++------------------------- 2 files changed, 26 insertions(+), 50 deletions(-) diff --git a/src/misc/vec/vecSet.h b/src/misc/vec/vecSet.h index 0045e3df..c96636f8 100644 --- a/src/misc/vec/vecSet.h +++ b/src/misc/vec/vecSet.h @@ -156,7 +156,7 @@ static inline void Vec_SetRestart( Vec_Set_t * p ) /**Function************************************************************* - Synopsis [Returns memory in bytes occupied by the vector.] + Synopsis [Freeing vector.] Description [] @@ -165,17 +165,22 @@ static inline void Vec_SetRestart( Vec_Set_t * p ) SeeAlso [] ***********************************************************************/ -static inline double Vec_ReportMemory( Vec_Set_t * p ) +static inline void Vec_SetFree_( Vec_Set_t * p ) { - double Mem = sizeof(Vec_Set_t); - Mem += p->nPagesAlloc * sizeof(void *); - Mem += sizeof(word) * (1 << p->nPageSize) * (1 + p->iPage); - return Mem; + 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 [Freeing vector.] + Synopsis [Returns memory in bytes occupied by the vector.] Description [] @@ -184,17 +189,12 @@ static inline double Vec_ReportMemory( Vec_Set_t * p ) 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 ) +static inline double Vec_ReportMemory( Vec_Set_t * p ) { - Vec_SetFree_( p ); - ABC_FREE( p ); + double Mem = sizeof(Vec_Set_t); + Mem += p->nPagesAlloc * sizeof(void *); + Mem += sizeof(word) * (1 << p->nPageSize) * (1 + p->iPage); + return Mem; } /**Function************************************************************* @@ -233,19 +233,11 @@ static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize ) } static inline int Vec_SetAppendS( Vec_Set_t * p, int nSize ) { - int Before1, Before2, After; int nWords = Vec_SetWordNum( nSize ); assert( nWords < (1 << p->nPageSize) ); - Before1 = Vec_SetLimitS( p->pPages[p->iPageS] ); - if ( Vec_SetLimitS( p->pPages[p->iPageS] ) + nWords >= (1 << p->nPageSize) ) Vec_SetWriteLimitS( p->pPages[++p->iPageS], 2 ); - Before2 = Vec_SetLimitS( p->pPages[p->iPageS] ); - Vec_SetIncLimitS( p->pPages[p->iPageS], nWords ); - After = Vec_SetLimitS( p->pPages[p->iPageS] ); - - assert( Vec_SetHandCurrentS(p) - nWords < (1 << p->nPageSize) ); return Vec_SetHandCurrentS(p) - nWords; } diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index 56de299e..d54f94b4 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -369,6 +369,7 @@ void Sat_ProofReduce2( sat_solver2 * s ) } */ + void Sat_ProofCheck0( Vec_Set_t * vProof ) { satset * pNode, * pFanin; @@ -381,6 +382,7 @@ void Sat_ProofCheck0( Vec_Set_t * vProof ) } } + int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ) { // Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs; @@ -394,15 +396,13 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ) clock_t clk = clock(); static clock_t TimeTotal = 0; int RetValue; - static int Count = 0; - Count++; - - Sat_ProofCheck0( vProof ); // collect visited nodes nSize = Proof_MarkUsedRec( vProof, vRoots ); vUsed = Vec_PtrAlloc( nSize ); +Sat_ProofCheck0( vProof ); + // relabel nodes to use smaller space Vec_SetShrinkS( vProof, 2 ); Vec_SetForEachEntry( satset *, vProof, nSize, pNode, i, j ) @@ -411,15 +411,13 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ) if ( pNode->Id == 0 ) continue; pNode->Id = Vec_SetAppendS( vProof, 2 + pNode->nEnts ); - assert( pNode->Id > 1 ); - assert( pNode->Id < (1<nPageSize) ); - assert( pNode->Id + nSize < (1<nPageSize) ); + assert( pNode->Id > 0 ); Vec_PtrPush( vUsed, pNode ); // update fanins Proof_NodeForeachFanin( vProof, pNode, pFanin, k ) if ( (pNode->pEnts[k] & 1) == 0 ) // proof node { - assert( pFanin->Id > 1 ); + assert( pFanin->Id > 0 ); pNode->pEnts[k] = (pFanin->Id << 2) | (pNode->pEnts[k] & 2); } // else // problem clause @@ -427,40 +425,26 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ) } // update roots Proof_ForeachNodeVec1( vRoots, vProof, pNode, i ) - { - assert( pNode->Id > 1 ); Vec_IntWriteEntry( vRoots, i, pNode->Id ); - } // determine new pivot assert( hProofPivot >= 1 && hProofPivot <= Vec_SetHandCurrent(vProof) ); pPivot = Proof_NodeRead( vProof, hProofPivot ); RetValue = Vec_SetHandCurrentS(vProof); // s->iProofPivot = Vec_PtrSize(vUsed); - - Sat_ProofCheck0( vProof ); - // compact the nodes Vec_PtrForEachEntry( satset *, vUsed, pNode, i ) { - int X = Proof_NodeWordNum(pNode->nEnts); hTemp = pNode->Id; pNode->Id = 0; - assert( hTemp > 1 ); - assert( hTemp + Proof_NodeWordNum(pNode->nEnts) < (1<nPageSize) ); memmove( Vec_SetEntry(vProof, hTemp), pNode, sizeof(word)*Proof_NodeWordNum(pNode->nEnts) ); if ( pPivot && pPivot <= pNode ) { RetValue = hTemp; pPivot = NULL; } - { - satset * pTemp = (satset *)Vec_SetEntry(vProof, hTemp); - assert( pTemp->partA == 0 ); - assert( X == Vec_SetWordNum( 2 + pTemp->nEnts ) ); - } } Vec_SetWriteEntryNum( vProof, Vec_PtrSize(vUsed) ); Vec_PtrFree( vUsed ); - + // report the result if ( fVerbose ) { @@ -475,7 +459,8 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ) Vec_SetShrinkLimits( vProof ); // Sat_ProofReduceCheck( s ); - Sat_ProofCheck0( vProof ); +Sat_ProofCheck0( vProof ); + return RetValue; } @@ -644,7 +629,6 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Set_t * vProof, Vec_Int_t * vUsed ) if ( pFanin == NULL ) { int Entry = (pNode->pEnts[k] >> 2); - assert( Entry <= MaxCla ); if ( Abc_InfoHasBit(pBitMap, Entry) ) continue; Abc_InfoSetBit(pBitMap, Entry); -- cgit v1.2.3