Enabling AIGs without structural hashing.

8 files changed, 33 insertions, 21 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 259c1b14..fad93838 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -14737,7 +14737,7 @@ int Abc_CommandRecStart3( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
         }
         fclose( pFile );
-        pGia = Gia_AigerRead( FileName, 1, 0 );
+        pGia = Gia_AigerRead( FileName, 0, 1, 0 );
         if ( pGia == NULL )
         {
             Abc_Print( -1, "Reading AIGER has failed.\n" );
@@ -15043,7 +15043,7 @@ int Abc_CommandRecMerge3( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
         }
         fclose( pFile );
-        pGia = Gia_AigerRead( FileName, 1, 0 );
+        pGia = Gia_AigerRead( FileName, 0, 1, 0 );
         if ( pGia == NULL )
         {
             Abc_Print( -1, "Reading AIGER has failed.\n" );
@@ -26331,12 +26331,16 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c, nArgcNew;
     int fUseMini = 0;
     int fVerbose = 0;
+    int fGiaSimple = 0;
     int fSkipStrash = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "smvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "csmvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'c':
+            fGiaSimple ^= 1;
+            break;
         case 's':
             fSkipStrash ^= 1;
             break;
@@ -26379,14 +26383,15 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    else if ( Extra_FileIsType( FileName, ".v", NULL, NULL ) )
 //        Abc3_ReadShowHie( FileName, fSkipStrash );
     else 
-        pAig = Gia_AigerRead( FileName, fSkipStrash, 0 );
+        pAig = Gia_AigerRead( FileName, fGiaSimple, fSkipStrash, 0 );
     if ( pAig )
         Abc_FrameUpdateGia( pAbc, pAig );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &r [-smvh] <file>\n" );
+    Abc_Print( -2, "usage: &r [-csmvh] <file>\n" );
     Abc_Print( -2, "\t         reads the current AIG from the AIGER file\n" );
+    Abc_Print( -2, "\t-c     : toggles reading simple AIG [default = %s]\n", fGiaSimple? "yes": "no" );
     Abc_Print( -2, "\t-s     : toggles structural hashing while reading [default = %s]\n", !fSkipStrash? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggles reading MiniAIG rather than AIGER file [default = %s]\n", fUseMini? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" );
@@ -30628,7 +30633,7 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     fclose( pFile );
-    pSecond = Gia_AigerRead( FileName, 0, 0 );
+    pSecond = Gia_AigerRead( FileName, 0, 0, 0 );
     if ( pSecond == NULL )
     {
         Abc_Print( -1, "Reading AIGER has failed.\n" );
@@ -30791,7 +30796,7 @@ int Abc_CommandAbc9Append( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     fclose( pFile );
-    pSecond = Gia_AigerRead( FileName, 0, 0 );
+    pSecond = Gia_AigerRead( FileName, 0, 0, 0 );
     if ( pSecond == NULL )
     {
         Abc_Print( -1, "Reading AIGER has failed.\n" );
@@ -32171,7 +32176,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     fclose( pFile );
-    pSecond = Gia_AigerRead( FileName, 0, 0 );
+    pSecond = Gia_AigerRead( FileName, 0, 0, 0 );
     if ( pSecond == NULL )
     {
         Abc_Print( -1, "Reading AIGER has failed.\n" );
@@ -38359,7 +38364,7 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 0;
         }
         fclose( pFile );
-        pGold = Gia_AigerRead( pFileName, 0, 0 );
+        pGold = Gia_AigerRead( pFileName, 0, 0, 0 );
         if ( pGold == NULL )
         {
             Abc_Print( -1, "Abc_CommandAbc9FFTest(): Cannot read file \"%s\" with golden model.\n", pFileName );
@@ -39689,7 +39694,7 @@ int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     fclose( pFile );
-    pSecond = Gia_AigerRead( FileName, 0, 0 );
+    pSecond = Gia_AigerRead( FileName, 0, 0, 0 );
     if ( pSecond == NULL )
     {
         Abc_Print( -1, "Reading AIGER has failed.\n" );
diff --git a/src/base/abci/abcTim.c b/src/base/abci/abcTim.c
index ba183402..3f68b815 100644
--- a/src/base/abci/abcTim.c
+++ b/src/base/abci/abcTim.c
@@ -566,7 +566,7 @@ void Abc_NtkTestTimByWritingFile( Gia_Man_t * pGia, char * pFileName )
         Gia_ManReverseClasses( pGia, 1 );
 
     // read file
-    pGia2 = Gia_AigerRead( pFileName, 1, 1 );
+    pGia2 = Gia_AigerRead( pFileName, 0, 1, 1 );
 
     // normalize choices
     if ( Gia_ManHasChoices(pGia2) )
diff --git a/src/base/cmd/cmdPlugin.c b/src/base/cmd/cmdPlugin.c
index 64837c80..ab517ed8 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_AigerReadFromMemory( pStr, nBinaryPart, 0, 0 ); 
+        pGia = Gia_AigerReadFromMemory( pStr, nBinaryPart, 0, 0, 0 ); 
     }
     Vec_StrFree( vStr );
     return pGia;
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 453cb157..b023e17d 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -252,7 +252,7 @@ extern Vec_Int_t *    Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p );
 extern Wlc_Ntk_t *    Wlc_NtkAbstractNodes( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes );
 extern Wlc_Ntk_t *    Wlc_NtkUifNodePairs( Wlc_Ntk_t * pNtk, Vec_Int_t * vPairs );
 /*=== wlcBlast.c ========================================================*/
-extern Gia_Man_t *    Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds );
+extern Gia_Man_t *    Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple );
 /*=== wlcCom.c ========================================================*/
 extern void           Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk );
 /*=== wlcNtk.c ========================================================*/
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 6ddd7a60..adce0d57 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -716,7 +716,7 @@ void Wlc_BlastSquare( Gia_Man_t * pNew, int * pNum, int nNum, Vec_Int_t * vTmp,
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
+Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple )
 {
     int fVerbose = 0;
     int fUseOldMultiplierBlasting = 0;
@@ -740,7 +740,9 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
     // create AIG manager
     pNew = Gia_ManStart( 5 * Wlc_NtkObjNum(p) + 1000 );
     pNew->pName = Abc_UtilStrsav( p->pName );
-    Gia_ManHashAlloc( pNew );
+    pNew->fGiaSimple = fGiaSimple;
+    if ( !fGiaSimple )
+        Gia_ManHashAlloc( pNew );
     // prepare for AIG with boxes
     if ( vBoxIds )
     {
@@ -770,6 +772,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
         // create AIG manager for logic of the boxes
         pExtra = Gia_ManStart( Wlc_NtkObjNum(p) );
         Gia_ManHashAlloc( pExtra );
+        assert( !fGiaSimple );
     }
     // blast in the topological order
     Wlc_NtkForEachObj( p, pObj, i )
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 1584e346..bbb897ea 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -328,12 +328,15 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
     Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
     Vec_Int_t * vBoxIds = NULL;
     Gia_Man_t * pNew = NULL;
-    int c, fMulti = 0, fVerbose  = 0;
+    int c, fGiaSimple = 0, fMulti = 0, fVerbose  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cmvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'c':
+            fGiaSimple ^= 1;
+            break;
         case 'm':
             fMulti ^= 1;
             break;
@@ -358,7 +361,7 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_Print( 1, "Warning:  There is no multipliers in the design.\n" );
     }
     // transform
-    pNew = Wlc_NtkBitBlast( pNtk, vBoxIds );
+    pNew = Wlc_NtkBitBlast( pNtk, vBoxIds, fGiaSimple );
     Vec_IntFreeP( &vBoxIds );
     if ( pNew == NULL )
     {
@@ -368,8 +371,9 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_FrameUpdateGia( pAbc, pNew );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%blast [-mvh]\n" );
+    Abc_Print( -2, "usage: %%blast [-cmvh]\n" );
     Abc_Print( -2, "\t         performs bit-blasting of the word-level design\n" );
+    Abc_Print( -2, "\t-c     : toggle using AIG w/o const propagation and strashing [default = %s]\n", fGiaSimple? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggle creating boxes for all multipliers in the design [default = %s]\n", fMulti? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index 0aedef30..eaecf449 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -1287,7 +1287,7 @@ void Io_ReadWordTest( char * pFileName )
         return;
     Wlc_WriteVer( pNtk, "test.v", 0, 0 );
 
-    pNew = Wlc_NtkBitBlast( pNtk, NULL );
+    pNew = Wlc_NtkBitBlast( pNtk, NULL, 0 );
     Gia_AigerWrite( pNew, "test.aig", 0, 0 );
     Gia_ManStop( pNew );
 
diff --git a/src/base/wlc/wlcSim.c b/src/base/wlc/wlcSim.c
index b0cea038..6cd081a5 100644
--- a/src/base/wlc/wlcSim.c
+++ b/src/base/wlc/wlcSim.c
@@ -129,7 +129,7 @@ Vec_Ptr_t * Wlc_NtkSimulate( Wlc_Ntk_t * p, Vec_Int_t * vNodes, int nWords, int
 {
     Gia_Obj_t * pObj; 
     Vec_Ptr_t * vOne, * vRes;
-    Gia_Man_t * pGia = Wlc_NtkBitBlast( p, NULL );
+    Gia_Man_t * pGia = Wlc_NtkBitBlast( p, NULL, 0 );
     Wlc_Obj_t * pWlcObj;
     int f, i, k, w, nBits, Counter = 0;
     // allocate simulation info for one timeframe