Scalable gate-level abstraction.

src/aig/gia/gia.h

@@ -224,6 +224,9 @@ struct Gia_ParVta_t_
     int            fUseRollback;  // use rollback to the starting number of frames
     int            fPropFanout;   // propagate fanout implications
     int            fAddLayer;     // refinement strategy by adding layers
+    int            fUseSkip;
+    int            fUseSimple;
+    int            fUseHash;
     int            fDumpVabs;     // dumps the abstracted model
     char *         pFileVabs;     // dumps the abstracted model into this file
     int            fVerbose;      // verbose flag

src/aig/gia/giaAbsGla2.c

@@ -237,9 +237,8 @@ void Ga2_ManCollectLeaves_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLea
     Ga2_ManCollectLeaves_rec( p, Gia_ObjFanin0(pObj), vLeaves, 0 );
     Ga2_ManCollectLeaves_rec( p, Gia_ObjFanin1(pObj), vLeaves, 0 );
 }
-int Ga2_ManMarkup( Gia_Man_t * p, int N )
+int Ga2_ManMarkup( Gia_Man_t * p, int N, int fSimple )
 {
-    int fSimple = 0;
     static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
     clock_t clk = clock();
     Vec_Int_t * vLeaves;
@@ -339,7 +338,7 @@ void Ga2_ManComputeTest( Gia_Man_t * p )
     Gia_Obj_t * pObj;
     int i, Counter = 0;
     clk = clock();
-    Ga2_ManMarkup( p, 5 );
+    Ga2_ManMarkup( p, 5, 0 );
     Abc_PrintTime( 1, "Time", clock() - clk );
     Gia_ManForEachAnd( p, pObj, i )
     {
@@ -375,7 +374,7 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
     p->pGia      = pGia;
     p->pPars     = pPars;
     // markings 
-    p->nMarked   = Ga2_ManMarkup( pGia, 5 );
+    p->nMarked   = Ga2_ManMarkup( pGia, 5, pPars->fUseSimple );
     p->vCnfs     = Vec_PtrAlloc( 1000 );
     Vec_PtrPush( p->vCnfs, Vec_IntAlloc(0) );
     Vec_PtrPush( p->vCnfs, Vec_IntAlloc(0) );
@@ -885,8 +884,8 @@ static inline void Ga2_ManAddToAbsOneDynamic( Ga2_Man_t * p, Gia_Obj_t * pObj, i
             }
             else
             {
-                int fUseHash = 0;
-                if ( fUseHash )
+//                int fUseHash = 1;
+                if ( p->pPars->fUseHash )
                 {
                     int * pLookup, nSize = Vec_IntSize(p->vLits);
                     assert( Vec_IntSize(p->vLits) < 5 );
@@ -1087,6 +1086,8 @@ void Ga2_ManRestart( Ga2_Man_t * p )
     // set runtime limit
     if ( p->pPars->nTimeOut )
         sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + p->timeStart );
+    // clean the hash table
+    memset( p->pTable, 0, 6 * sizeof(int) * p->nTable );
 }
 
 /**Function*************************************************************
@@ -1374,7 +1375,7 @@ void Ga2_ManAbsPrintFrame( Ga2_Man_t * p, int nFrames, int nConfls, int nCexes,
     Abc_PrintInt( sat_solver2_nlearnts(p->pSat) );
     Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
     Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
-    Abc_Print( 1, "%s", (fFinal && nCexes) ? "\n" : "\r" );
+    Abc_Print( 1, "%s", (fFinal && nCexes) ? "\n" : "\n" );
     fflush( stdout );
 }
 
@@ -1459,7 +1460,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
     Vec_Int_t * vCore, * vPPis;
     clock_t clk2, clk = clock();
     int Status, RetValue = -1, fOneIsSent = 0;
-    int i, c, f, Lit;
+    int i, c, f, Lit, iFrameProved = -1;
     // check trivial case 
     assert( Gia_ManPoNum(pAig) == 1 ); 
     ABC_FREE( pAig->pCexSeq );
@@ -1524,6 +1525,8 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
             Lit = Abc_LitNotCond( Lit, Gia_ObjFaninC0(Gia_ManPo(pAig,0)) );
             if ( Lit == 0 )
                 continue;
+            if ( p->pPars->fUseSkip && f <= iFrameProved )
+                continue;
             assert( Lit > 1 );
             // check for counter-examples
             sat_solver2_setnvars( p->pSat, p->nSatVars );
@@ -1635,6 +1638,8 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                     Ga2_GlaDumpAbsracted( p, pPars->fVerbose );
                 }
 
+                iFrameProved = f;
+                printf( "\n" );
                 break;  // temporary
             }
         }

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, "FSPCLDETRAtrfkadnvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLDETRAtrfkadnscbvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -28245,6 +28245,15 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'n':
             fNewAlgo ^= 1;
             break;
+        case 's':
+            pPars->fUseSkip ^= 1;
+            break;
+        case 'c':
+            pPars->fUseSimple ^= 1;
+            break;
+        case 'b':
+            pPars->fUseHash ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -28290,7 +28299,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &gla [-FSCLDETR num] [-A file] [-fkadnvh]\n" );
+    Abc_Print( -2, "usage: &gla [-FSCLDETR num] [-A file] [-fkadnscbvh]\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 );
@@ -28306,11 +28315,15 @@ usage:
     Abc_Print( -2, "\t-a      : toggle refinement by adding one layers of gates [default = %s]\n", pPars->fAddLayer? "yes": "no" );
     Abc_Print( -2, "\t-d      : toggle dumping abstracted model into a file [default = %s]\n", pPars->fDumpVabs? "yes": "no" );
     Abc_Print( -2, "\t-n      : toggle using new algorithms [default = %s]\n", fNewAlgo? "yes": "no" );
+    Abc_Print( -2, "\t-s      : toggle skipping previously proved timeframes [default = %s]\n", pPars->fUseSkip? "yes": "no" );
+    Abc_Print( -2, "\t-c      : toggle using naive (2-input AND node) CNF encoding [default = %s]\n", pPars->fUseSimple? "yes": "no" );
+    Abc_Print( -2, "\t-b      : toggle using hashing during CNF construction [default = %s]\n", pPars->fUseHash? "yes": "no" );
     Abc_Print( -2, "\t-v      : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h      : print the command usage\n");
     return 1;
 } 
 
+
 /**Function*************************************************************
 
   Synopsis    []