Enabling AIGs without structural hashing.

6 files changed, 29 insertions, 18 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 81a6d11a..58b00db2 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1204,7 +1204,7 @@ extern Gia_Man_t *         Gia_ManDupDfsClasses( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
 extern Gia_Man_t *         Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose );
 extern Gia_Man_t *         Gia_ManDupAndOr( Gia_Man_t * p, int nOuts, int fUseOr, int fCompl );
-extern Gia_Man_t *         Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fVerbose );
+extern Gia_Man_t *         Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fGiaSimple, int fVerbose );
 extern Gia_Man_t *         Gia_ManMiter2( Gia_Man_t * p, char * pInit, int fVerbose );
 extern Gia_Man_t *         Gia_ManTransformMiter( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManTransformMiter2( Gia_Man_t * p );
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 2aadf07f..8e7423aa 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -848,7 +848,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi
             }
         }
         pInit[i] = 0;
-        pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 1 );
+        pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, fGiaSimple, 1 );
         pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0;
         Gia_ManStop( pTemp );
         ABC_FREE( pInit );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 66b80ace..3ffb948e 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -2618,7 +2618,7 @@ Gia_Man_t * Gia_ManTransformTwoWord2DualOutput( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fVerbose )
+Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fGiaSimple, int fVerbose )
 {
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj;
@@ -2635,6 +2635,7 @@ Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fVerbose )
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    pNew->fGiaSimple = fGiaSimple;
     Gia_ManConst0(p)->Value = 0;
     // create primary inputs
     Gia_ManForEachPi( p, pObj, i )
@@ -2707,7 +2708,7 @@ Gia_Man_t * Gia_ManMiter2( Gia_Man_t * pStart, char * pInit, int fVerbose )
     for ( i = 0; i < Gia_ManPiNum(pStart); i++ )
         assert( pInit[i] == 'x' || pInit[i] == 'X' );
     // normalize the manager
-    pUndc = Gia_ManDupZeroUndc( pStart, pInit + Gia_ManPiNum(pStart), fVerbose );
+    pUndc = Gia_ManDupZeroUndc( pStart, pInit + Gia_ManPiNum(pStart), 0, fVerbose );
     // create new init string
     pInitNew = ABC_ALLOC( char, Gia_ManPiNum(pUndc)+1 );
     for ( i = 0; i < Gia_ManPiNum(pStart); i++ )
diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c
index 5bfdbae2..d4a47ac5 100644
--- a/src/aig/gia/giaHash.c
+++ b/src/aig/gia/giaHash.c
@@ -666,10 +666,15 @@ int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 )
 ***********************************************************************/
 int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 )  
 { 
-    int fCompl = Abc_LitIsCompl(iLit0) ^ Abc_LitIsCompl(iLit1);
-    int iTemp0 = Gia_ManHashAnd( p, Abc_LitRegular(iLit0), Abc_LitNot(Abc_LitRegular(iLit1)) );
-    int iTemp1 = Gia_ManHashAnd( p, Abc_LitRegular(iLit1), Abc_LitNot(Abc_LitRegular(iLit0)) );
-    return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl );
+    if ( p->fGiaSimple )
+        return Gia_ManHashOr(p, Gia_ManHashAnd(p, iLit0, Abc_LitNot(iLit1)), Gia_ManHashAnd(p, Abc_LitNot(iLit0), iLit1) );
+    else
+    {
+        int fCompl = Abc_LitIsCompl(iLit0) ^ Abc_LitIsCompl(iLit1);
+        int iTemp0 = Gia_ManHashAnd( p, Abc_LitRegular(iLit0), Abc_LitNot(Abc_LitRegular(iLit1)) );
+        int iTemp1 = Gia_ManHashAnd( p, Abc_LitRegular(iLit1), Abc_LitNot(Abc_LitRegular(iLit0)) );
+        return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl );
+    }
 }
 
 /**Function*************************************************************
@@ -685,14 +690,19 @@ int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 )
 ***********************************************************************/
 int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 )  
 { 
-    int iTemp0, iTemp1, fCompl = 0;
-    if ( iData0 > iData1 )
-        iData0 ^= iData1, iData1 ^= iData0, iData0 ^= iData1, iCtrl = Abc_LitNot(iCtrl);
-    if ( Abc_LitIsCompl(iData1) )
-        iData0 = Abc_LitNot(iData0), iData1 = Abc_LitNot(iData1), fCompl = 1;
-    iTemp0 = Gia_ManHashAnd( p, Abc_LitNot(iCtrl), iData0 );
-    iTemp1 = Gia_ManHashAnd( p, iCtrl, iData1 );
-    return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl );
+    if ( p->fGiaSimple )
+        return Gia_ManHashOr(p, Gia_ManHashAnd(p, iCtrl, iData1), Gia_ManHashAnd(p, Abc_LitNot(iCtrl), iData0) );
+    else
+    {
+        int iTemp0, iTemp1, fCompl = 0;
+        if ( iData0 > iData1 )
+            iData0 ^= iData1, iData1 ^= iData0, iData0 ^= iData1, iCtrl = Abc_LitNot(iCtrl);
+        if ( Abc_LitIsCompl(iData1) )
+            iData0 = Abc_LitNot(iData0), iData1 = Abc_LitNot(iData1), fCompl = 1;
+        iTemp0 = Gia_ManHashAnd( p, Abc_LitNot(iCtrl), iData0 );
+        iTemp1 = Gia_ManHashAnd( p, iCtrl, iData1 );
+        return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl );
+    }
 }
 
 /**Function*************************************************************
diff --git a/src/aig/gia/giaRex.c b/src/aig/gia/giaRex.c
index 2eacc8d7..ebfc9401 100644
--- a/src/aig/gia/giaRex.c
+++ b/src/aig/gia/giaRex.c
@@ -309,7 +309,7 @@ Gia_Man_t * Gia_ManRex2Gia( char * pStrInit, int fOrder, int fVerbose )
     Gia_ManStop( pTemp );
 
     // add initial state
-    pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 0 );
+    pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 0, 0 );
     Gia_ManStop( pTemp );
     Vec_StrFree( vInit );
 /*
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index 40573025..71b9a475 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -871,7 +871,7 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v
                 pInit[i] = 'X';
         }
         pInit[i] = 0;
-        pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 1 );
+        pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 0, 1 );
         pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0;
         Gia_ManStop( pTemp );
         ABC_FREE( pInit );