Enabling AIGs without structural hashing.

14 files changed, 60 insertions, 42 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 1877821a..65f6a76d 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -112,6 +112,7 @@ struct Gia_Man_t_
     int            nHTable;       // hash table size 
     int            fAddStrash;    // performs additional structural hashing
     int            fSweeper;      // sweeper is running
+    int            fGiaSimple;    // simple mode (no const-propagation and strashing)
     int *          pRefs;         // the reference count
     int *          pLutRefs;      // the reference count
     Vec_Int_t *    vLevels;       // levels of the nodes
@@ -632,7 +633,7 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 )
     Gia_Obj_t * pObj = Gia_ManAppendObj( p );
     assert( iLit0 >= 0 && Abc_Lit2Var(iLit0) < Gia_ManObjNum(p) );
     assert( iLit1 >= 0 && Abc_Lit2Var(iLit1) < Gia_ManObjNum(p) );
-    assert( Abc_Lit2Var(iLit0) != Abc_Lit2Var(iLit1) );
+    assert( p->fGiaSimple || Abc_Lit2Var(iLit0) != Abc_Lit2Var(iLit1) );
     if ( iLit0 < iLit1 )
     {
         pObj->iDiff0  = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0);
@@ -1112,8 +1113,8 @@ static inline int         Gia_ObjCellId( Gia_Man_t * p, int iLit )          { re
 
 /*=== giaAiger.c ===========================================================*/
 extern int                 Gia_FileSize( char * pFileName );
-extern Gia_Man_t *         Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipStrash, int fCheck );
-extern Gia_Man_t *         Gia_AigerRead( char * pFileName, int fSkipStrash, int fCheck );
+extern Gia_Man_t *         Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSimple, int fSkipStrash, int fCheck );
+extern Gia_Man_t *         Gia_AigerRead( char * pFileName, int fGiaSimple, int fSkipStrash, int fCheck );
 extern void                Gia_AigerWrite( 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_AigerWriteIntoMemoryStr( Gia_Man_t * p );
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 940d75ac..2aadf07f 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -173,7 +173,7 @@ Vec_Str_t * Gia_AigerWriteLiterals( Vec_Int_t * vLits )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipStrash, int fCheck )
+Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSimple, int fSkipStrash, int fCheck )
 {
     Gia_Man_t * pNew, * pTemp;
     Vec_Int_t * vLits = NULL, * vPoTypes = NULL;
@@ -255,6 +255,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
     // allocate the empty AIG
     pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
     pNew->nConstrs = nConstr;
+    pNew->fGiaSimple = fGiaSimple;
 
     // prepare the array of nodes
     vNodes = Vec_IntAlloc( 1 + nTotal );
@@ -282,7 +283,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
     }
 
     // create the AND gates
-    if ( !fSkipStrash )
+    if ( !fGiaSimple && !fSkipStrash )
         Gia_ManHashAlloc( pNew );
     for ( i = 0; i < nAnds; i++ )
     {
@@ -293,7 +294,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
         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 );
-        if ( fSkipStrash )
+        if ( !fGiaSimple && fSkipStrash )
         {
             if ( iNode0 == iNode1 )
                 Vec_IntPush( vNodes, Gia_ManAppendBuf(pNew, iNode0) );
@@ -303,7 +304,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
         else
             Vec_IntPush( vNodes, Gia_ManHashAnd(pNew, iNode0, iNode1) );
     }
-    if ( !fSkipStrash )
+    if ( !fGiaSimple && !fSkipStrash )
         Gia_ManHashStop( pNew );
 
     // remember the place where symbols begin
@@ -526,7 +527,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
                 vStr = Vec_StrStart( Gia_AigerReadInt(pCur) );             pCur += 4;
                 memcpy( Vec_StrArray(vStr), pCur, Vec_StrSize(vStr) );
                 pCur += Vec_StrSize(vStr);
-                pNew->pAigExtra = Gia_AigerReadFromMemory( Vec_StrArray(vStr), Vec_StrSize(vStr), 0, 0 );
+                pNew->pAigExtra = Gia_AigerReadFromMemory( Vec_StrArray(vStr), Vec_StrSize(vStr), 0, 0, 0 );
                 Vec_StrFree( vStr );
                 if ( fVerbose ) printf( "Finished reading extension \"a\".\n" );
             }
@@ -790,7 +791,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
         Vec_IntFreeP( &vPoTypes );
     }
 
-    if ( !fSkipStrash && Gia_ManHasDangling(pNew) )
+    if ( !fGiaSimple && !fSkipStrash && Gia_ManHasDangling(pNew) )
     {
         Tim_Man_t * pManTime;
         Vec_Int_t * vFlopMap, * vGateMap, * vObjMap;
@@ -853,7 +854,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
         ABC_FREE( pInit );
     }
     Vec_IntFreeP( &vInits );
-    if ( !fSkipStrash && pNew->vMapping )
+    if ( !fGiaSimple && !fSkipStrash && pNew->vMapping )
     {
         Abc_Print( 0, "Structural hashing enabled while reading AIGER invalidated the mapping.  Consider using \"&r -s\".\n" );
         Vec_IntFreeP( &pNew->vMapping );
@@ -872,7 +873,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_AigerRead( char * pFileName, int fSkipStrash, int fCheck )
+Gia_Man_t * Gia_AigerRead( char * pFileName, int fGiaSimple, int fSkipStrash, int fCheck )
 {
     FILE * pFile;
     Gia_Man_t * pNew;
@@ -888,7 +889,7 @@ Gia_Man_t * Gia_AigerRead( char * pFileName, int fSkipStrash, int fCheck )
     RetValue = fread( pContents, nFileSize, 1, pFile );
     fclose( pFile );
 
-    pNew = Gia_AigerReadFromMemory( pContents, nFileSize, fSkipStrash, fCheck );
+    pNew = Gia_AigerReadFromMemory( pContents, nFileSize, fGiaSimple, fSkipStrash, fCheck );
     ABC_FREE( pContents );
     if ( pNew )
     {
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 71b32d7d..d383ce41 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -1185,7 +1185,7 @@ void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerb
         return;
     }
     // read AIGER file
-    pMiter = Gia_AigerRead( pFileName, 0, 0 );
+    pMiter = Gia_AigerRead( pFileName, 0, 0, 0 );
     if ( pMiter == NULL )
     {
         Abc_Print( 1, "Gia_ManEquivMark(): Input file %s could not be read.\n", pFileName );
@@ -1869,13 +1869,13 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p
         Abc_Print( 1, "Equivalences are not defined.\n" );
         return 0;
     }
-    pGia1 = Gia_AigerRead( pName1, 0, 0 );
+    pGia1 = Gia_AigerRead( pName1, 0, 0, 0 );
     if ( pGia1 == NULL )
     {
         Abc_Print( 1, "Cannot read first file %s.\n", pName1 );
         return 0;
     }
-    pGia2 = Gia_AigerRead( pName2, 0, 0 );
+    pGia2 = Gia_AigerRead( pName2, 0, 0, 0 );
     if ( pGia2 == NULL )
     {
         Gia_ManStop( pGia2 );
@@ -2008,13 +2008,13 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName
         Abc_Print( 1, "Equivalences are not defined.\n" );
         return 0;
     }
-    pGia1 = Gia_AigerRead( pName1, 0, 0 );
+    pGia1 = Gia_AigerRead( pName1, 0, 0, 0 );
     if ( pGia1 == NULL )
     {
         Abc_Print( 1, "Cannot read first file %s.\n", pName1 );
         return 0;
     }
-    pGia2 = Gia_AigerRead( pName2, 0, 0 );
+    pGia2 = Gia_AigerRead( pName2, 0, 0, 0 );
     if ( pGia2 == NULL )
     {
         Gia_ManStop( pGia2 );
diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c
index 725f03af..5bfdbae2 100644
--- a/src/aig/gia/giaHash.c
+++ b/src/aig/gia/giaHash.c
@@ -575,7 +575,11 @@ int Gia_ManHashMuxReal( Gia_Man_t * p, int iLitC, int iLit1, int iLit0 )
 ***********************************************************************/
 int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 )  
 { 
-//    return Gia_ManAppendAnd2( p, iLit0, iLit1 );
+    if ( p->fGiaSimple )
+    {
+        assert( p->nHTable == 0 );
+        return Gia_ManAppendAnd( p, iLit0, iLit1 );
+    }
     if ( iLit0 < 2 )
         return iLit0 ? iLit1 : 0;
     if ( iLit1 < 2 )
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index feab0db1..40573025 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -906,7 +906,7 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fS
         return Status;
     }
     // read original AIG
-    pSpec = Gia_AigerRead( pFileSpec ? pFileSpec : pGia->pSpec, 0, 0 );
+    pSpec = Gia_AigerRead( pFileSpec ? pFileSpec : pGia->pSpec, 0, 0, 0 );
     if ( Gia_ManBoxNum(pSpec) && pSpec->pAigExtra == NULL )
     {
         Gia_ManStop( pSpec );
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
diff --git a/src/sat/bmc/bmcEco.c b/src/sat/bmc/bmcEco.c
index 07fdd704..9d30fc09 100644
--- a/src/sat/bmc/bmcEco.c
+++ b/src/sat/bmc/bmcEco.c
@@ -283,8 +283,8 @@ void Bmc_EcoMiterTest()
     }
     fclose( pFile );
     // read files
-    pGold = Gia_AigerRead( pFileGold, 0, 0 );
-    pOld  = Gia_AigerRead( pFileOld, 0, 0 );
+    pGold = Gia_AigerRead( pFileGold, 0, 0, 0 );
+    pOld  = Gia_AigerRead( pFileOld, 0, 0, 0 );
     // create ECO miter
     vFans = Vec_IntAlloc( Gia_ManCiNum(pOld) );
     Gia_ManForEachCi( pOld, pObj, i )