Debugging a proof error.

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<<vProof->nPageSize) );
-        assert( pNode->Id + nSize < (1<<vProof->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<<vProof->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);