summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat/satProof.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-07-13 19:06:32 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2012-07-13 19:06:32 -0700
commit3c4351aee49eebb4055a3922d11f2d4b0f772728 (patch)
tree7a585bf659fdce86740a726c734170fc0f38fa0f /src/sat/bsat/satProof.c
parent8c162f0577bd825f3d1f81a1723fbd23f4c8d3a9 (diff)
downloadabc-3c4351aee49eebb4055a3922d11f2d4b0f772728.tar.gz
abc-3c4351aee49eebb4055a3922d11f2d4b0f772728.tar.bz2
abc-3c4351aee49eebb4055a3922d11f2d4b0f772728.zip
Debugging a proof error.
Diffstat (limited to 'src/sat/bsat/satProof.c')
-rw-r--r--src/sat/bsat/satProof.c13
1 files changed, 3 insertions, 10 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;
}