Scalable gate-level abstraction.

src/aig/gia/giaAbsGla2.c

@@ -1549,8 +1549,8 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                 continue;
             assert( Lit > 1 );
             // check for counter-examples
-//            if ( p->nSatVars > sat_solver2_nvars(p->pSat) )
-//                sat_solver2_setnvars( p->pSat, p->nSatVars );
+            if ( p->nSatVars > sat_solver2_nvars(p->pSat) )
+                sat_solver2_setnvars( p->pSat, p->nSatVars );
             nVarsOld = p->nSatVars;
             for ( c = 0; ; c++ )
             {
@@ -1666,9 +1666,9 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                 // if abstraction grew more than a certain percentage, force a restart
                 if ( pPars->nRatioMax == 0 )
                     break;
-                if ( Vec_IntSize(p->vAbs) - nAbsOld >= nAbsOld * pPars->nRatioMax / 100 )
+                if ( (f > 20 || Vec_IntSize(p->vAbs) > 100) && Vec_IntSize(p->vAbs) - nAbsOld >= nAbsOld * pPars->nRatioMax / 100 )
                 {
-                    if ( p->pPars->fVeryVerbose )
+                    if ( p->pPars->fVerbose )
                     Abc_Print( 1, "Forcing restart because abstraction grew from %d to %d (more than %d %%).\n", 
                         nAbsOld, Vec_IntSize(p->vAbs), pPars->nRatioMax );
                     break;
@@ -1685,7 +1685,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
     }
 finish:
     Prf_ManStopP( &p->pSat->pPrf2 );
-    if ( p->pPars->fVeryVerbose )
+    if ( p->pPars->fVerbose )
     Abc_Print( 1, "\n" );
     // analize the results
     if ( pAig->pCexSeq == NULL )

src/aig/gia/giaAbsVta.c

@@ -158,7 +158,7 @@ void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
     p->nLearnedPerce =     40;   // max number of learned clauses
     p->nTimeOut      =      0;   // timeout in seconds
     p->nRatioMin     =     10;   // stop when less than this % of object is abstracted
-    p->nRatioMax     =      0;   // restart when more than this % of object is abstracted
+    p->nRatioMax     =     30;   // restart when more than this % of object is abstracted
     p->fUseTermVars  =      0;   // use terminal variables
     p->fUseRollback  =      0;   // use rollback to the starting number of frames
     p->fVerbose      =      0;   // verbose flag

src/aig/gia/giaUtil.c

@@ -847,6 +847,24 @@ int Gia_NodeRef_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
     return Counter + 1;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [References the node's MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManPoMffcSize( Gia_Man_t * p )
+{
+    Gia_ManCreateRefs( p );
+    return Gia_NodeDeref_rec( p, Gia_ObjFanin0(Gia_ManPo(p, 0)) );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Returns the number of internal nodes in the MFFC.]