Variable timeframe abstraction.

3 files changed, 85 insertions, 27 deletions

diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index b8420014..1eaf4407 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -295,7 +295,55 @@ Vec_Int_t * Proof_CollectUsedRec( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hR
 
 
 
- 
+  
+/**Function*************************************************************
+
+  Synopsis    [Checks the validity of the check point.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_ProofReduceCheck_rec( Vec_Int_t * vProof, Vec_Int_t * vClauses, satset * pNode, int hClausePivot, Vec_Ptr_t * vVisited )
+{
+    satset * pFanin;
+    int k;
+    if ( pNode->Id )
+        return;
+    pNode->Id = -1;
+    Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k )
+        if ( (pNode->pEnts[k] & 1) == 0 ) // proof node
+            Sat_ProofReduceCheck_rec( vProof, vClauses, pFanin, hClausePivot, vVisited );
+        else // problem clause
+            assert( (pNode->pEnts[k] >> 2) < hClausePivot );
+    Vec_PtrPush( vVisited, pNode );
+}
+void Sat_ProofReduceCheckOne( sat_solver2 * s, int iLearnt, Vec_Ptr_t * vVisited )
+{
+    Vec_Int_t * vProof   = (Vec_Int_t *)&s->proofs;
+    Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
+    Vec_Int_t * vRoots   = (Vec_Int_t *)&s->claProofs;
+    int hProofNode = Vec_IntEntry( vRoots, iLearnt );
+    satset * pNode = Proof_NodeRead( vProof, hProofNode );
+    Sat_ProofReduceCheck_rec( vProof, vClauses, pNode, s->hClausePivot, vVisited );
+}
+void Sat_ProofReduceCheck( sat_solver2 * s )
+{
+    Vec_Ptr_t * vVisited;
+    satset * c;
+    int h, i = 1;
+    vVisited = Vec_PtrAlloc( 1000 );
+    sat_solver_foreach_learnt( s, c, h )
+        if ( h < s->hLearntPivot )
+            Sat_ProofReduceCheckOne( s, i++, vVisited );
+    Vec_PtrForEachEntry( satset *, vVisited, c, i )
+        c->Id = 0;
+    Vec_PtrFree( vVisited );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Reduces the proof to contain only roots and their children.]
@@ -311,6 +359,7 @@ void Sat_ProofReduce( sat_solver2 * s )
 {
     Vec_Int_t * vProof   = (Vec_Int_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_Int_t * vUsed;
@@ -328,9 +377,11 @@ void Sat_ProofReduce( sat_solver2 * s )
     Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
     {
         pNode->Id = hNewHandle; hNewHandle += Proof_NodeSize(pNode->nEnts);
-        Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
-            if ( pFanin )
+        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_ForeachNodeVec( vRoots, vProof, pNode, i )
@@ -352,6 +403,8 @@ void Sat_ProofReduce( sat_solver2 * s )
         Abc_PrintTime( 1, "Time", TimeTotal );
     }
     Vec_IntShrink( vProof, hNewHandle );
+
+    Sat_ProofReduceCheck( s );
 }
 
 
@@ -520,6 +573,7 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_
     // clean core clauses and reexpress core in terms of clause IDs
     Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
     {
+        assert( (int*)pNode < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) );
         pNode->mark = 0;
         if ( fUseIds )
 //            Vec_IntWriteEntry( vCore, i, pNode->Id - 1 );
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index e4d713d1..5a54a64e 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -1399,23 +1399,35 @@ void luby2_test()
 void sat_solver2_reducedb(sat_solver2* s)
 {
     static int TimeTotal = 0;
-    cla h,* pArray,* pArray2;
     satset * c, * pivot;
-    int Counter, CounterStart;
+    cla h,* pArray,* pArray2;
+    int * pPerm, * pClaAct, nClaAct, ActCutOff;
     int i, j, k, hTemp, hHandle, clk = clock();
+    int Counter, CounterStart;
 
+    // check if it is time to reduce
     if ( s->nLearntMax == 0 || s->stats.learnts < (unsigned)s->nLearntMax )
         return;
-
-    CounterStart   = s->stats.learnts - (s->nLearntMax / 3);
     s->nLearntMax = s->nLearntMax * 11 / 10;
 
-    // remove 2/3 of learned clauses while skipping small clauses
+    // preserve 1/10 of last clauses
+    CounterStart  = s->stats.learnts - (s->nLearntMax / 10);
+
+    // preserve 1/10 of most active clauses
+    pClaAct = veci_begin(&s->claActs) + 1;
+    nClaAct = veci_size(&s->claActs) - 1;
+    pPerm = Abc_SortCost( pClaAct, nClaAct );
+    assert( pClaAct[pPerm[0]] <= pClaAct[pPerm[nClaAct-1]] );
+    ActCutOff = pClaAct[pPerm[nClaAct*9/10]];
+    ABC_FREE( pPerm );
+//    ActCutOff = ABC_INFINITY;
+
+    // mark learned clauses to remove
     Counter = 0;
     veci_resize( &s->learnt_live, 0 );
     sat_solver_foreach_learnt( s, c, h )
     {
-        if ( Counter++ > CounterStart || c->nEnts < 3 || s->reasons[lit_var(c->pEnts[0])] == (h<<1)+1 )
+        if ( Counter++ > CounterStart || c->nEnts < 3 || pClaAct[c->Id-1] >= ActCutOff || s->reasons[lit_var(c->pEnts[0])] == (h<<1)+1 )
             veci_push( &s->learnt_live, h );
         else
             c->mark = 1;
@@ -1471,6 +1483,7 @@ void sat_solver2_reducedb(sat_solver2* s)
         }
     // compact clauses
     pivot = satset_read( &s->learnts, s->hLearntPivot );
+    s->hLearntPivot = hHandle;
     satset_foreach_entry_vec( &s->learnt_live, &s->learnts, c, i )
     {
         hTemp = c->Id; c->Id = i + 1;
@@ -1484,6 +1497,8 @@ void sat_solver2_reducedb(sat_solver2* s)
     assert( hHandle == hTemp + satset_size(c->nEnts) );
     veci_resize(&s->learnts,hHandle);
     s->stats.learnts = veci_size(&s->learnt_live);
+    assert( s->hLearntPivot <= veci_size(&s->learnts) );
+    assert( s->hClausePivot <= veci_size(&s->clauses) );
 
     // compact proof (compacts 'proofs' and update 'claProofs')
     if ( s->fProofLogging )
@@ -1551,24 +1566,9 @@ void sat_solver2_rollback( sat_solver2* s )
     // reset watcher lists
     for ( i = 2*s->iVarPivot; i < 2*s->size; i++ )
         s->wlists[i].size = 0;
-    // clean the room
-    for ( i = s->iVarPivot; i < s->size; i++ )
-    {
-        *((int*)s->vi + i) = 0;
-        s->levels  [i] = 0;
-        s->assigns [i] = varX;
-        s->reasons [i] = 0;        
-        s->units   [i] = 0;        
-#ifdef USE_FLOAT_ACTIVITY2
-        s->activity[i] = 0;
-#else
-        s->activity[i] = (1<<10);
-#endif
-        s->model   [i] = 0; 
-        s->orderpos[i] = -1;
-    }
-    s->size = s->iVarPivot;
+
     // initialize other vars
+    s->size = s->iVarPivot;
     if ( s->size == 0 )
     {
     //    s->size                   = 0;
diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h
index 01740580..8f7a5fab 100644
--- a/src/sat/bsat/satVec.h
+++ b/src/sat/bsat/satVec.h
@@ -44,7 +44,11 @@ static inline void veci_new (veci* v) {
 static inline void   veci_delete (veci* v)          { ABC_FREE(v->ptr);   }
 static inline int*   veci_begin  (veci* v)          { return v->ptr;  }
 static inline int    veci_size   (veci* v)          { return v->size; }
-static inline void   veci_resize (veci* v, int k)   { assert(k <= v->size); v->size = k;         } // only safe to shrink !!
+static inline void   veci_resize (veci* v, int k)   { 
+    assert(k <= v->size); 
+//    memset( veci_begin(v) + k, -1, sizeof(int) * (veci_size(v) - k) );
+    v->size = k;         
+} // only safe to shrink !!
 static inline int    veci_pop    (veci* v)          { assert(v->size); return v->ptr[--v->size]; }
 static inline void   veci_push   (veci* v, int e)
 {