Scalable gate-level abstraction.

src/aig/gia/gia.h

@@ -226,7 +226,7 @@ struct Gia_ParVta_t_
     int            fAddLayer;     // refinement strategy by adding layers
     int            fUseSkip;
     int            fUseSimple;
-    int            fUseHash;
+    int            fSkipHash;
     int            fDumpVabs;     // dumps the abstracted model
     char *         pFileVabs;     // dumps the abstracted model into this file
     int            fVerbose;      // verbose flag

src/aig/gia/giaAbsGla.c

@@ -1734,11 +1734,11 @@ void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfl
     Abc_PrintInt( sat_solver2_nlearnts(p->pSat) );
 //    Abc_Print( 1, " %6d", nCoreSize > 0 ? nCoreSize : 0 ); 
     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, "%5.0f MB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<20) );
 //    Abc_PrintInt( p->nAbsNew );
 //    Abc_PrintInt( p->nLrnNew );
 //    Abc_Print( 1, "%4.1f MB", 4.0 * p->nLrnNew * Abc_BitWordNum(p->nAbsNew) / (1<<20) );
-    Abc_Print( 1, "%s", nCoreSize > 0 ? "\n" : "\r" );
+    Abc_Print( 1, "%s", (nCoreSize > 0 && nCexes > 0) ? "\n" : "\r" );
     fflush( stdout );
 }
 void Gla_ManReportMemory( Gla_Man_t * p )

src/aig/gia/giaAbsGla2.c

@@ -30,7 +30,7 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-#define GA2_BIG_NUM 0x3FFFFFFF
+#define GA2_BIG_NUM 0x3FFFFFF0
 
 typedef struct Ga2_Man_t_ Ga2_Man_t; // manager
 struct Ga2_Man_t_
@@ -796,6 +796,7 @@ static inline void Ga2_ManAddToAbsOneDynamic( Ga2_Man_t * p, Gia_Obj_t * pObj, i
     Gia_Obj_t * pLeaf;
     unsigned uTruth;
     int i, Lit;
+
     assert( Ga2_ObjIsAbs0(p, pObj) );
     assert( Gia_ObjIsConst0(pObj) || Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) );
     if ( Gia_ObjIsConst0(pObj) || (f == 0 && Gia_ObjIsRo(p->pGia, pObj)) )
@@ -814,7 +815,6 @@ static inline void Ga2_ManAddToAbsOneDynamic( Ga2_Man_t * p, Gia_Obj_t * pObj, i
     }
     else
     {
-        int pLits[5];
         assert( Gia_ObjIsAnd(pObj) );
         Vec_IntClear( p->vLits );
         vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
@@ -827,16 +827,16 @@ static inline void Ga2_ManAddToAbsOneDynamic( Ga2_Man_t * p, Gia_Obj_t * pObj, i
             }
             else if ( Ga2_ObjIsLeaf0(p, pLeaf) ) // belongs to original PPIs
             {
-//                Lit = Ga2_ObjFindLit( p, pLeaf, f );
-                Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f );
+                Lit = Ga2_ObjFindLit( p, pLeaf, f );
+//                Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f );
                 if ( Lit == -1 )
                 {
-                    Lit = GA2_BIG_NUM + i;
-                    assert( 0 );
+                    Lit = GA2_BIG_NUM + 2*i;
+//                    assert( 0 );
                 }
             }
             else assert( 0 );
-            Vec_IntPush( p->vLits, (pLits[i] = Lit) );
+            Vec_IntPush( p->vLits, Lit );
         }
 
         // minimize truth table
@@ -851,7 +851,7 @@ static inline void Ga2_ManAddToAbsOneDynamic( Ga2_Man_t * p, Gia_Obj_t * pObj, i
             Lit = Vec_IntEntry( p->vLits, 0 );
             if ( Lit >= GA2_BIG_NUM )
             {
-                pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, Lit-GA2_BIG_NUM) );
+                pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, (Lit-GA2_BIG_NUM)/2) );
                 Lit = Ga2_ObjFindLit( p, pLeaf, f );
                 assert( Lit == -1 );
                 Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f );
@@ -859,6 +859,7 @@ static inline void Ga2_ManAddToAbsOneDynamic( Ga2_Man_t * p, Gia_Obj_t * pObj, i
             assert( Lit >= 0 );
             Lit = Abc_LitNotCond( Lit, uTruth == 0x55555555 );
             Ga2_ObjAddLit( p, pObj, f, Lit );
+            assert( Lit < 10000000 );
         }
         else
         {
@@ -868,24 +869,28 @@ static inline void Ga2_ManAddToAbsOneDynamic( Ga2_Man_t * p, Gia_Obj_t * pObj, i
             {
                 if ( Lit >= GA2_BIG_NUM )
                 {
-                    pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, Lit-GA2_BIG_NUM) );
+                    pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, (Lit-GA2_BIG_NUM)/2) );
                     Lit = Ga2_ObjFindLit( p, pLeaf, f );
                     assert( Lit == -1 );
                     Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f );
                     Vec_IntWriteEntry( p->vLits, i, Lit );
                 }
+                assert( Lit < 10000000 );
             }
 
             // add new nodes
             if ( Vec_IntSize(p->vLits) == 5 )
             {
+                Vec_IntClear( p->vLits );
+                Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, i )
+                    Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pLeaf, f ) );
                 Lit = Ga2_ObjFindOrAddLit(p, pObj, f);
-                Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), pLits, Lit, -1 );
+                Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), Lit, -1 );
             }
             else
             {
 //                int fUseHash = 1;
-                if ( p->pPars->fUseHash )
+                if ( !p->pPars->fSkipHash )
                 {
                     int * pLookup, nSize = Vec_IntSize(p->vLits);
                     assert( Vec_IntSize(p->vLits) < 5 );
@@ -1374,7 +1379,7 @@ void Ga2_ManAbsPrintFrame( Ga2_Man_t * p, int nFrames, int nConfls, int nCexes,
     Abc_PrintInt( sat_solver2_nclauses(p->pSat) );
     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, "%5.0f MB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<20) );
     Abc_Print( 1, "%s", ((fFinal && nCexes) || p->pPars->fVeryVerbose) ? "\n" : "\r" );
     fflush( stdout );
 }
@@ -1654,6 +1659,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
     }
 finish:
     Prf_ManStopP( &p->pSat->pPrf2 );
+    Abc_Print( 1, "\n" );
     // analize the results
     if ( pAig->pCexSeq == NULL )
     {

src/base/abci/abc.c

@@ -28252,7 +28252,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
             pPars->fUseSimple ^= 1;
             break;
         case 'b':
-            pPars->fUseHash ^= 1;
+            pPars->fSkipHash ^= 1;
             break;
         case 'v':
             pPars->fVerbose ^= 1;
@@ -28320,7 +28320,7 @@ usage:
     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-b      : toggle CNF construction without hashing [default = %s]\n", pPars->fSkipHash? "yes": "no" );
     Abc_Print( -2, "\t-v      : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w      : toggle printing more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h      : print the command usage\n");