Enabling AIGs without structural hashing.

5 files changed, 25 insertions, 19 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 );