Allow for skipping structural hashing when reading GIA from file.

5 files changed, 25 insertions, 20 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index a74da4cb..b3a8fdc1 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -723,8 +723,8 @@ extern void                Gia_VtaSetDefaultParams( Gia_ParVta_t * p );
 extern int                 Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars );
 /*=== giaAiger.c ===========================================================*/
 extern int                 Gia_FileSize( char * pFileName );
-extern Gia_Man_t *         Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck );
-extern Gia_Man_t *         Gia_ReadAiger( char * pFileName, int fCheck );
+extern Gia_Man_t *         Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fSkipStrash, int fCheck );
+extern Gia_Man_t *         Gia_ReadAiger( char * pFileName, int fSkipStrash, int fCheck );
 extern void                Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
 extern void                Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits );
 extern Vec_Str_t *         Gia_WriteAigerIntoMemoryStr( Gia_Man_t * p );
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 1f36cfdc..14cbf913 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -638,7 +638,7 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck )
+Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fSkipStrash, int fCheck )
 {
     Gia_Man_t * pNew, * pTemp;
     Vec_Int_t * vLits = NULL, * vPoTypes = NULL;
@@ -747,7 +747,8 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
     }
 
     // create the AND gates
-    Gia_ManHashAlloc( pNew );
+    if ( fSkipStrash )
+        Gia_ManHashAlloc( pNew );
     for ( i = 0; i < nAnds; i++ )
     {
         uLit = ((i + 1 + nInputs + nLatches) << 1);
@@ -757,10 +758,13 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
         iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
         iNode1 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
         assert( Vec_IntSize(vNodes) == i + 1 + nInputs + nLatches );
-//        Vec_IntPush( vNodes, Gia_And(pNew, iNode0, iNode1) );
-        Vec_IntPush( vNodes, Gia_ManHashAnd(pNew, iNode0, iNode1) );
+        if ( fSkipStrash )
+            Vec_IntPush( vNodes, Gia_ManAppendAnd(pNew, iNode0, iNode1) );
+        else
+            Vec_IntPush( vNodes, Gia_ManHashAnd(pNew, iNode0, iNode1) );
     }
-    Gia_ManHashStop( pNew );
+    if ( fSkipStrash )
+        Gia_ManHashStop( pNew );
 
     // remember the place where symbols begin
     pSymbols = pCur;
@@ -1067,7 +1071,7 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
+Gia_Man_t * Gia_ReadAiger( char * pFileName, int fSkipStrash, int fCheck )
 {
     FILE * pFile;
     Gia_Man_t * pNew;
@@ -1083,7 +1087,7 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
     RetValue = fread( pContents, nFileSize, 1, pFile );
     fclose( pFile );
 
-    pNew = Gia_ReadAigerFromMemory( pContents, nFileSize, fCheck );
+    pNew = Gia_ReadAigerFromMemory( pContents, nFileSize, fSkipStrash, fCheck );
     ABC_FREE( pContents );
     if ( pNew )
     {
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 62ef03a4..03570cd4 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -1224,7 +1224,7 @@ void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerb
         return;
     }
     // read AIGER file
-    pMiter = Gia_ReadAiger( pFileName, 0 );
+    pMiter = Gia_ReadAiger( pFileName, 0, 0 );
     if ( pMiter == NULL )
     {
         printf( "Gia_ManEquivMark(): Input file %s could not be read.\n", pFileName );
@@ -1782,13 +1782,13 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p
         printf( "Equivalences are not defined.\n" );
         return 0;
     }
-    pGia1 = Gia_ReadAiger( pName1, 0 );
+    pGia1 = Gia_ReadAiger( pName1, 0, 0 );
     if ( pGia1 == NULL )
     {
         printf( "Cannot read first file %s.\n", pName1 );
         return 0;
     }
-    pGia2 = Gia_ReadAiger( pName2, 0 );
+    pGia2 = Gia_ReadAiger( pName2, 0, 0 );
     if ( pGia2 == NULL )
     {
         Gia_ManStop( pGia2 );
@@ -1921,13 +1921,13 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName
         printf( "Equivalences are not defined.\n" );
         return 0;
     }
-    pGia1 = Gia_ReadAiger( pName1, 0 );
+    pGia1 = Gia_ReadAiger( pName1, 0, 0 );
     if ( pGia1 == NULL )
     {
         printf( "Cannot read first file %s.\n", pName1 );
         return 0;
     }
-    pGia2 = Gia_ReadAiger( pName2, 0 );
+    pGia2 = Gia_ReadAiger( pName2, 0, 0 );
     if ( pGia2 == NULL )
     {
         Gia_ManStop( pGia2 );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e218ad82..da66df65 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -840,6 +840,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 
     {
         extern void Dar_LibStart();
+ //       char * pMem = malloc( (1<<30) * 3 / 2 );
         Dar_LibStart();
     }
     {
@@ -12731,7 +12732,7 @@ int Abc_CommandRecStart2( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
         }
         fclose( pFile );
-        pGia = Gia_ReadAiger( FileName, 0 );
+        pGia = Gia_ReadAiger( FileName, 1, 0 );
         if ( pGia == NULL )
         {
             Abc_Print( -1, "Reading AIGER has failed.\n" );
@@ -13079,7 +13080,7 @@ int Abc_CommandRecMerge2( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
         }
         fclose( pFile );
-        pGia = Gia_ReadAiger( FileName, 0 );
+        pGia = Gia_ReadAiger( FileName, 0, 0 );
         if ( pGia == NULL )
         {
             Abc_Print( -1, "Reading AIGER has failed.\n" );
@@ -22725,7 +22726,7 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     fclose( pFile );
 
-    pAig = Gia_ReadAiger( FileName, 0 );
+    pAig = Gia_ReadAiger( FileName, 0, 0 );
     Abc_CommandUpdate9( pAbc, pAig );
     return 0;
 
@@ -25212,7 +25213,7 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     fclose( pFile );
-    pSecond = Gia_ReadAiger( FileName, 0 );
+    pSecond = Gia_ReadAiger( FileName, 0, 0 );
     if ( pSecond == NULL )
     {
         Abc_Print( -1, "Reading AIGER has failed.\n" );
@@ -26299,7 +26300,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     fclose( pFile );
-    pSecond = Gia_ReadAiger( FileName, 0 );
+    pSecond = Gia_ReadAiger( FileName, 0, 0 );
     if ( pSecond == NULL )
     {
         Abc_Print( -1, "Reading AIGER has failed.\n" );
diff --git a/src/base/cmd/cmdPlugin.c b/src/base/cmd/cmdPlugin.c
index 429c2f72..118fc95a 100644
--- a/src/base/cmd/cmdPlugin.c
+++ b/src/base/cmd/cmdPlugin.c
@@ -391,7 +391,7 @@ Gia_Man_t * Abc_ManReadAig( char * pFileName, char * pToken )
             fclose( pFile );
         }
         // derive AIG
-        pGia = Gia_ReadAigerFromMemory( pStr, nBinaryPart, 0 ); 
+        pGia = Gia_ReadAigerFromMemory( pStr, nBinaryPart, 0, 0 ); 
     }
     Vec_StrFree( vStr );
     return pGia;