Variable timeframe abstraction.

4 files changed, 100 insertions, 31 deletions

diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 9c50ae52..45e36243 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -62,6 +62,7 @@ struct Vta_Man_t_
     Vec_Int_t *   vSeens;       // seen objects
     Vec_Bit_t *   vSeenGla;     // seen objects in all frames
     int           nSeenGla;     // seen objects in all frames
+    int           nSeenAll;     // seen objects in all frames
     // other data
     Vec_Int_t *   vCla2Var;     // map clauses into variables
     Vec_Ptr_t *   vCores;       // unsat core for each frame
@@ -149,7 +150,7 @@ void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
     p->nFramesStart  =      5;   // starting frame 
     p->nFramesPast   =      4;   // overlap frames
     p->nConfLimit    =      0;   // conflict limit
-    p->nLearntMax    =      0;   // max number of learned clauses
+    p->nLearntMax    =  15000;   // max number of learned clauses
     p->nTimeOut      =      0;   // timeout in seconds
     p->nRatioMin     =     10;   // stop when less than this % of object is abstracted
     p->fUseTermVars  =      1;   // use terminal variables
@@ -968,6 +969,8 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
             if ( !Gia_ObjIsPi(p->pGia, pObj) )
                 Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
         sat_solver2_simplify( p->pSat );
+
+//        printf( "VecCla grew to %d.       \n\n", Vec_IntSize(p->vCla2Var) );
     }
     Vec_IntFree( vTermsToAdd );
     return pCex;
@@ -1005,6 +1008,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
     p->vSeens      = Vec_IntStart( Gia_ManObjNum(pGia) * p->nWords );
     p->vSeenGla    = Vec_BitStart( Gia_ManObjNum(pGia) );
     p->nSeenGla    = 1;
+    p->nSeenAll    = 1;
     // start the abstraction
     if ( pGia->vObjClasses == NULL )
         p->vFrames = Gia_ManUnrollAbs( pGia, pPars->nFramesStart );
@@ -1167,6 +1171,7 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nC
                 Abc_InfoSetBit( pInfo, iFrame );
                 pCountUni[iFrame+1]++;
                 pCountUni[0]++;
+                p->nSeenAll++;
             }
             pCountAll[iFrame+1]++;
             pCountAll[0]++;
@@ -1180,8 +1185,12 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nC
 //    printf( "%5d%5d", pCountAll[0], pCountUni[0] ); 
     printf( "%3d :", nFrames-1 );
     printf( "%6d", p->nSeenGla ); 
-    printf( "%8d", nConfls ); 
-    printf( "%5d", nCexes ); 
+    printf( "%4d", Abc_MinInt(100, 100 * p->nSeenAll / (p->nSeenGla * nFrames)) ); 
+    printf( "%8d", nConfls );
+    if ( nCexes == 0 )
+        printf( "%5c", '-' ); 
+    else
+        printf( "%5d", nCexes ); 
     if ( vCore == NULL )
     {
         printf( "    ..." ); 
@@ -1414,7 +1423,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         printf( "FrameStart = %d  FramePast = %d  FrameMax = %d  Conf = %d  Timeout = %d. RatioMin = %d %%.\n", 
             p->pPars->nFramesStart, p->pPars->nFramesPast, p->pPars->nFramesMax, 
             p->pPars->nConfLimit, p->pPars->nTimeOut, pPars->nRatioMin );
-        printf( "Frame   Abs   Confl  Cex   Core   F0   F1   F2   F3  ...\n" );
+        printf( "Frame   Abs   %%   Confl  Cex   Core   F0   F1   F2   F3  ...\n" );
     }
     for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
     {
@@ -1428,6 +1437,8 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         {
             Vga_ManAddClausesOne( p, 0, f );
             Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
+
+//            printf( "VecCla grew ttto %d.        \n\n", Vec_IntSize(p->vCla2Var) );
         }
         else
         {
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)
 {