Improved abstraction refinement.

src/aig/gia/giaAbsGla.c

@@ -1303,7 +1303,7 @@ void Gla_ManStop( Gla_Man_t * p )
     Gla_Obj_t * pGla;
     int i;
 
-//    if ( p->pPars->fVerbose )
+    if ( p->pPars->fVerbose )
         Abc_Print( 1, "SAT solver:  Var = %d  Cla = %d  Conf = %d  Lrn = %d  Reduce = %d  Cex = %d  Objs+ = %d\n", 
             sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), 
             sat_solver2_nlearnts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
@@ -2102,8 +2102,8 @@ finish:
     {
         if ( p->pPars->fVerbose && Status == -1 )
             printf( "\n" );
-        if ( pAig->vGateClasses != NULL )
-            Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
+//        if ( pAig->vGateClasses != NULL )
+//            Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
         Vec_IntFreeP( &pAig->vGateClasses );
         pAig->vGateClasses = Gla_ManTranslate( p );
         if ( Status == -1 )

src/aig/gia/giaAbsGla2.c

@@ -440,7 +440,7 @@ void Ga2_ManStop( Ga2_Man_t * p )
 {
     Vec_IntFreeP( &p->pGia->vMapping );
     Gia_ManSetPhase( p->pGia );
-//    if ( p->pPars->fVerbose )
+    if ( p->pPars->fVerbose )
         Abc_Print( 1, "SAT solver:  Var = %d  Cla = %d  Conf = %d  Lrn = %d  Reduce = %d  Cex = %d  ObjsAdded = %d\n", 
             sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), 
             sat_solver2_nconflicts(p->pSat), sat_solver2_nlearnts(p->pSat), 
@@ -1527,7 +1527,11 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                     goto finish;
                 assert( RetValue == l_False );
                 if ( c == 0 )
+                {
+                    p->pPars->nFramesNoChange++;
                     break;
+                }
+                p->pPars->nFramesNoChange = 0;
 
                 // derive the core
                 assert( p->pSat->pPrf2 != NULL );
@@ -1601,16 +1605,16 @@ finish:
     // analize the results
     if ( pAig->pCexSeq == NULL )
     {
-        if ( pAig->vGateClasses != NULL )
-            Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
+//        if ( pAig->vGateClasses != NULL )
+//            Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
         Vec_IntFreeP( &pAig->vGateClasses );
         pAig->vGateClasses = Ga2_ManAbsTranslate( p );
         if ( Status == l_Undef )
         {
             if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit ) 
-                Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d.  ", p->pPars->nTimeOut, f );
+                Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction.    ", p->pPars->nTimeOut, f, p->pPars->nFramesNoChange );
             else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
-                Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d.  ", pPars->nConfLimit, f );
+                Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction.  ", pPars->nConfLimit, f, p->pPars->nFramesNoChange );
             else if ( Vec_IntSize(p->vAbs) >= p->nMarked * (100 - pPars->nRatioMin) / 100 )
                 Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d.  ", pPars->nRatioMin, f );
             else
@@ -1619,7 +1623,7 @@ finish:
         else
         {
             p->pPars->iFrame++;
-            Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction.  ", f );
+            Abc_Print( 1, "SAT solver completed %d frames and produced a %d-stable abstraction.  ", f, p->pPars->nFramesNoChange );
         }
     }
     else

src/aig/gia/giaAbsRef.c

@@ -721,6 +721,7 @@ Vec_Int_t * Ga2_FilterSelected( Rnm_Man_t * p, Vec_Int_t * vSelect )
 Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fVerbose )
 {
     int fVerify = 0;
+    int fPostProcess = 1;
     Vec_Int_t * vSelected = Vec_IntAlloc( 100 );
     Vec_Int_t * vNew;
     clock_t clk, clk2 = clock();
@@ -754,16 +755,19 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in
         p->timeBwd += clock() - clk;
     }
 
-    vNew = Ga2_FilterSelected( p, vSelected );
-    if ( Vec_IntSize(vNew) > 0 )
+    if ( fPostProcess )
     {
-        Vec_IntFree( vSelected );
-        vSelected = vNew;
-    }
-    else
-    {
-        Vec_IntFree( vNew );
-//        printf( "\nBig refinement.\n" );
+        vNew = Ga2_FilterSelected( p, vSelected );
+        if ( Vec_IntSize(vNew) > 0 )
+        {
+            Vec_IntFree( vSelected );
+            vSelected = vNew;
+        }
+        else
+        {
+            Vec_IntFree( vNew );
+    //        printf( "\nBig refinement.\n" );
+        }
     }
 
     // clean values

src/aig/gia/giaAbsVta.c

@@ -1064,7 +1064,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
 ***********************************************************************/
 void Vga_ManStop( Vta_Man_t * p )
 {
-//    if ( p->pPars->fVerbose )
+    if ( p->pPars->fVerbose )
         Abc_Print( 1, "SAT solver:  Var = %d  Cla = %d  Conf = %d  Lrn = %d  Reduce = %d  Cex = %d  Objs+ = %d\n", 
             sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), 
             sat_solver2_nlearnts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
@@ -1706,8 +1706,8 @@ finish:
         else
         {
             assert( Vec_PtrSize(p->vCores) > 0 );
-            if ( pAig->vObjClasses != NULL )
-                Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
+//            if ( pAig->vObjClasses != NULL )
+//                Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
             Vec_IntFreeP( &pAig->vObjClasses );
             pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
             if ( Status == -1 )