Scalable gate-level abstraction.

4 files changed, 51 insertions, 22 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 91adcd5f..2d7a0695 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -220,6 +220,7 @@ struct Gia_ParVta_t_
     int            nLearnedPerce; // percentage of clauses to leave
     int            nTimeOut;      // timeout in seconds
     int            nRatioMin;     // stop when less than this % of object is abstracted
+    int            nRatioMax;     // restart when the number of abstracted object is more than this
     int            fUseTermVars;  // use terminal variables
     int            fUseRollback;  // use rollback to the starting number of frames
     int            fPropFanout;   // propagate fanout implications
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c
index 3bca462a..7e5056c7 100644
--- a/src/aig/gia/giaAbsGla2.c
+++ b/src/aig/gia/giaAbsGla2.c
@@ -396,8 +396,8 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
     p->vIsopMem  = Vec_IntAlloc( 100 );
     Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
     // hash table
-    p->nTable = 1000003;
-    p->pTable = ABC_CALLOC( int, 6 * p->nTable ); // 2.4 MB
+    p->nTable = Abc_PrimeCudd(1<<18);
+    p->pTable = ABC_CALLOC( int, 6 * p->nTable ); 
     return p;
 }
 void Ga2_ManReportMemory( Ga2_Man_t * p )
@@ -408,6 +408,7 @@ void Ga2_ManReportMemory( Ga2_Man_t * p )
     double memPro = sat_solver2_memory_proof( p->pSat );
     double memMap = Vec_VecMemoryInt( (Vec_Vec_t *)p->vId2Lit );
     double memRef = Rnm_ManMemoryUsage( p->pRnm );
+    double memHash= sizeof(int) * 6 * p->nTable;
     double memOth = sizeof(Ga2_Man_t);
     memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCnfs );
     memOth += Vec_IntMemory( p->vIds );
@@ -417,12 +418,13 @@ void Ga2_ManReportMemory( Ga2_Man_t * p )
     memOth += Vec_IntMemory( p->vLits );
     memOth += Vec_IntMemory( p->vIsopMem );
     memOth += 336450 + (sizeof(char) + sizeof(char*)) * 65536;
-    memTot = memAig + memSat + memPro + memMap + memRef + memOth;
+    memTot = memAig + memSat + memPro + memMap + memRef + memHash + memOth;
     ABC_PRMP( "Memory: AIG      ", memAig, memTot );
     ABC_PRMP( "Memory: SAT      ", memSat, memTot );
     ABC_PRMP( "Memory: Proof    ", memPro, memTot );
     ABC_PRMP( "Memory: Map      ", memMap, memTot );
     ABC_PRMP( "Memory: Refine   ", memRef, memTot );
+    ABC_PRMP( "Memory: Hash     ", memHash,memTot );
     ABC_PRMP( "Memory: Other    ", memOth, memTot );
     ABC_PRMP( "Memory: TOTAL    ", memTot, memTot );
 }
@@ -435,6 +437,7 @@ void Ga2_ManStop( Ga2_Man_t * p )
             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 );
+    if ( p->pPars->fVerbose )
     Abc_Print( 1, "Hash hits = %d.  Hash misses = %d.  Hash overs = %d.\n", 
         p->nHashHit, p->nHashMiss, p->nHashOver );
 
@@ -894,7 +897,7 @@ static inline void Ga2_ManAddToAbsOneDynamic( Ga2_Man_t * p, Gia_Obj_t * pObj, i
                 {
                     int * pLookup, nSize = Vec_IntSize(p->vLits);
                     assert( Vec_IntSize(p->vLits) < 5 );
-                    assert( Vec_IntEntry(p->vLits, 0) < Vec_IntEntryLast(p->vLits) );
+                    assert( Vec_IntEntry(p->vLits, 0) <= Vec_IntEntryLast(p->vLits) );
                     assert( Ga2_ObjFindLit(p, pObj, f) == -1 );
                     for ( i = Vec_IntSize(p->vLits); i < 4; i++ )
                         Vec_IntPush( p->vLits, GA2_BIG_NUM );
@@ -928,7 +931,6 @@ void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f )
     int fSimple = 0;
     Gia_Obj_t * pObj;
     int i;
-    // add variables for the leaves
     Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
     {
         if ( i == p->LimAbs )
@@ -941,6 +943,7 @@ void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f )
     Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
         if ( i >= p->LimAbs )
             Ga2_ManAddToAbsOneStatic( p, pObj, f );
+//    sat_solver2_simplify( p->pSat );
 }
 
 void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
@@ -970,13 +973,14 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
         Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
             Ga2_ManAddToAbsOneStatic( p, pObj, f );
     }
+//    sat_solver2_simplify( p->pSat );
 }
 
 void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues, int nSatVars )
 {
     Vec_Int_t * vMap;
     Gia_Obj_t * pObj;
-    int i;
+    int i, k, Entry;
     assert( nAbs > 0 );
     assert( nValues > 0 );
     assert( nSatVars > 0 );
@@ -1004,9 +1008,17 @@ void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues, int nSatVars )
     }
     Vec_IntShrink( p->vValues, nValues );
     Vec_PtrShrink( p->vCnfs, 2 * nValues );
+    // hack to clear constant
+    if ( nValues == 1 )
+        nValues = 0;
     // clean mapping for each timeframe
     Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i )
-        Vec_IntClear( vMap );
+    {
+        Vec_IntShrink( vMap, nValues );
+        Vec_IntForEachEntry( vMap, Entry, k )
+            if ( Entry >= 2*nSatVars )
+                Vec_IntWriteEntry( vMap, k, -1 );
+    }
     // shrink SAT variables
     p->nSatVars = nSatVars;
 }
@@ -1503,10 +1515,13 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
     // iterate unrolling
     for ( i = f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; i++ )
     {
+        int nAbsOld;
         // remember the timeframe
         p->pPars->iFrame = -1;
         // create new SAT solver
         Ga2_ManRestart( p );
+        // remember abstraction size after the last restart
+        nAbsOld = Vec_IntSize(p->vAbs);
         // unroll the circuit
         for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ )
         {
@@ -1534,7 +1549,8 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                 continue;
             assert( Lit > 1 );
             // check for counter-examples
-            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++ )
             {
@@ -1646,7 +1662,17 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                 iFrameProved = f;
                 if ( p->pPars->fVeryVerbose )
                     Abc_Print( 1, "\n" );
-                break;  // temporary
+
+                // 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 ( p->pPars->fVeryVerbose )
+                    Abc_Print( 1, "Forcing restart because abstraction grew from %d to %d (more than %d %%).\n", 
+                        nAbsOld, Vec_IntSize(p->vAbs), pPars->nRatioMax );
+                    break;
+                }
             }
         }
 
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 59e3eb40..68310510 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -158,6 +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->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/base/abci/abc.c b/src/base/abci/abc.c
index 794de44a..44617786 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -28112,7 +28112,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c, fStartVta = 0, fNewAlgo = 0;
     Gia_VtaSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLDETRAtrfkadnscbwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FSCLDETRPAtrfkadnscbwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -28138,17 +28138,6 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nFramesStart < 0 ) 
                 goto usage;
             break;
-        case 'P':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nFramesPast = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nFramesPast < 0 ) 
-                goto usage;
-            break;
         case 'C':
             if ( globalUtilOptind >= argc )
             {
@@ -28215,6 +28204,17 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nRatioMin < 0 ) 
                 goto usage;
             break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nRatioMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nRatioMax < 0 ) 
+                goto usage;
+            break;
         case 'A':
             if ( globalUtilOptind >= argc )
             {
@@ -28302,7 +28302,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &gla [-FSCLDETR num] [-A file] [-fkadnscbwvh]\n" );
+    Abc_Print( -2, "usage: &gla [-FSCLDETRP num] [-A file] [-fkadnscbwvh]\n" );
     Abc_Print( -2, "\t          fixed-time-frame gate-level proof- and cex-based abstraction\n" );
     Abc_Print( -2, "\t-F num  : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
     Abc_Print( -2, "\t-S num  : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
@@ -28312,6 +28312,7 @@ usage:
     Abc_Print( -2, "\t-E num  : ratio percentage for learned clause removal [default = %d]\n", pPars->nLearnedPerce );
     Abc_Print( -2, "\t-T num  : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
     Abc_Print( -2, "\t-R num  : minimum percentage of abstracted objects (0<=num<=100) [default = %d]\n", pPars->nRatioMin );
+    Abc_Print( -2, "\t-P num  : maximum percentage of added objects before a restart (0<=num<=100) [default = %d]\n", pPars->nRatioMax );
     Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"glabs.aig\"]\n" );
     Abc_Print( -2, "\t-f      : toggle propagating fanout implications [default = %s]\n", pPars->fPropFanout? "yes": "no" );
     Abc_Print( -2, "\t-k      : toggle using VTA to kick start GLA for starting frames [default = %s]\n", fStartVta? "yes": "no" );