diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-13 19:06:32 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-13 19:06:32 -0700 |
| commit | 3c4351aee49eebb4055a3922d11f2d4b0f772728 (patch) | |
| tree | 7a585bf659fdce86740a726c734170fc0f38fa0f /src | |
| parent | 8c162f0577bd825f3d1f81a1723fbd23f4c8d3a9 (diff) | |
| download | abc-3c4351aee49eebb4055a3922d11f2d4b0f772728.tar.gz abc-3c4351aee49eebb4055a3922d11f2d4b0f772728.tar.bz2 abc-3c4351aee49eebb4055a3922d11f2d4b0f772728.zip | |
Debugging a proof error.
Diffstat (limited to 'src')
| -rw-r--r-- | src/sat/bsat/satProof.c | 13 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.c | 6 |
2 files changed, 7 insertions, 12 deletions
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index 7613e022..5e2ce067 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -338,7 +338,6 @@ void Sat_ProofReduce2( sat_solver2 * s ) 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 ) { @@ -347,7 +346,6 @@ void Sat_ProofReduce2( sat_solver2 * s ) if ( pPivot && pPivot <= pNode ) { s->hProofPivot = hTemp; - s->iProofPivot = i; pPivot = NULL; } } @@ -382,7 +380,6 @@ 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; @@ -396,14 +393,12 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ) clock_t clk = clock(); static clock_t TimeTotal = 0; int RetValue; - -Sat_ProofCheck0( vProof ); +//Sat_ProofCheck0( vProof ); // collect visited nodes nSize = Proof_MarkUsedRec( vProof, vRoots ); vUsed = Vec_PtrAlloc( nSize ); - -Sat_ProofCheck0( vProof ); +//Sat_ProofCheck0( vProof ); // relabel nodes to use smaller space Vec_SetShrinkS( vProof, 2 ); @@ -432,7 +427,6 @@ Sat_ProofCheck0( vProof ); assert( hProofPivot >= 1 && hProofPivot <= Vec_SetHandCurrent(vProof) ); pPivot = Proof_NodeRead( vProof, hProofPivot ); RetValue = Vec_SetHandCurrentS(vProof); -// s->iProofPivot = Vec_PtrSize(vUsed); // compact the nodes Vec_PtrForEachEntry( satset *, vUsed, pNode, i ) { @@ -460,8 +454,7 @@ Sat_ProofCheck0( vProof ); Vec_SetShrink( vProof, Vec_SetHandCurrentS(vProof) ); Vec_SetShrinkLimits( vProof ); // Sat_ProofReduceCheck( s ); - -Sat_ProofCheck0( vProof ); +//Sat_ProofCheck0( vProof ); return RetValue; } diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index bb81ccdd..b84f5a5f 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1571,8 +1571,10 @@ void sat_solver2_rollback( sat_solver2* s ) if ( s->fProofLogging ) { veci_resize(&s->claProofs, s->stats.learnts); -// Vec_SetShrink(&s->Proofs, s->hProofPivot); // past bug here - Sat_ProofReduce( &s->Proofs, &s->claProofs, s->hProofPivot ); +// Vec_SetShrink(&s->Proofs, s->hProofPivot); + // some weird bug here, which shows only on 64-bits! + // temporarily, perform more general proof reduction + Sat_ProofReduce( &s->Proofs, &s->claProofs, s->hProofPivot ); } // initialize other vars |