From a01b479013e702050c2be0ccce1435fac8ed0e99 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 3 Aug 2012 21:44:00 -0700
Subject: Scalable gate-level abstraction.

---
 src/aig/gia/giaAbsGla2.c | 10 +++++-----
 src/aig/gia/giaAbsVta.c  |  2 +-
 src/aig/gia/giaUtil.c    | 18 ++++++++++++++++++
 3 files changed, 24 insertions(+), 6 deletions(-)

(limited to 'src')

diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c
index 1476e704..85f0c00d 100644
--- a/src/aig/gia/giaAbsGla2.c
+++ b/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 )
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 68310510..5d070e78 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/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
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 72fdf307..6f01e5cd 100644
--- a/src/aig/gia/giaUtil.c
+++ b/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.]
-- 
cgit v1.2.3