Enabling AIGs without structural hashing.

9 files changed, 41 insertions, 27 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 );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 551961c9..e1d69bf1 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26761,7 +26761,7 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
             Aig_ManStop( pAig );
             // perform undc/zero
             pInits = Abc_NtkCollectLatchValuesStr( pAbc->pNtkCur );
-            pGia = Gia_ManDupZeroUndc( pTemp = pGia, pInits, fVerbose );
+            pGia = Gia_ManDupZeroUndc( pTemp = pGia, pInits, 0, fVerbose );
             Gia_ManStop( pTemp );
             ABC_FREE( pInits );
         }
@@ -32141,7 +32141,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
             Gia_Man_t * pTemp;
             if ( !pPars->fSilent )
             Abc_Print( 1, "Assuming the current network is a single-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit );
-            pTemp = Gia_ManTransformToDual( pAbc->pGia );
+            pTemp = Gia_ManDemiterToDual( pAbc->pGia );
             pAbc->Status = Cec_ManVerify( pTemp, pPars );
             ABC_SWAP( Abc_Cex_t *, pAbc->pGia->pCexComb, pTemp->pCexComb );
             Gia_ManStop( pTemp );
diff --git a/src/base/cba/cbaBlast.c b/src/base/cba/cbaBlast.c
index 322d4372..490a36eb 100644
--- a/src/base/cba/cbaBlast.c
+++ b/src/base/cba/cbaBlast.c
@@ -1013,7 +1013,7 @@ Gia_Man_t * Cba_NtkBlast( Cba_Ntk_t * p, int fSeq )
     {
         Gia_ManSetRegNum( pNew, Vec_StrSize(vInit) );
         Vec_StrPush( vInit, '\0' );
-        pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 1 );
+        pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 0, 1 );
         Gia_ManDupRemapLiterals( vBits, pTemp );
         Gia_ManStop( pTemp );
         Vec_StrFreeP( &vInit );
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index adce0d57..65940176 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -274,10 +274,10 @@ void Wlc_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int *
     {
         int And1 = Gia_ManHashAnd(pNew, a, b);
         int And1_= Gia_ManHashAnd(pNew, Abc_LitNot(a), Abc_LitNot(b));
-        int Xor  = Abc_LitNot(Gia_ManHashOr(pNew, And1, And1_));
+        int Xor  = Gia_ManHashAnd(pNew, Abc_LitNot(And1), Abc_LitNot(And1_));
         int And2 = Gia_ManHashAnd(pNew, c, Xor);
         int And2_= Gia_ManHashAnd(pNew, Abc_LitNot(c), Abc_LitNot(Xor));
-        *ps      = Abc_LitNot(Gia_ManHashOr(pNew, And2, And2_));
+        *ps      = Gia_ManHashAnd(pNew, Abc_LitNot(And2), Abc_LitNot(And2_));
         *pc      = Gia_ManHashOr (pNew, And1, And2);
     }
 }
@@ -1209,9 +1209,12 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple
     assert( nFFins == nFFouts );
     Gia_ManSetRegNum( pNew, nFFins );
     // finalize AIG
-    pNew = Gia_ManCleanup( pTemp = pNew );
-    Gia_ManDupRemapLiterals( vBits, pTemp );
-    Gia_ManStop( pTemp );
+    if ( !fGiaSimple )
+    {
+        pNew = Gia_ManCleanup( pTemp = pNew );
+        Gia_ManDupRemapLiterals( vBits, pTemp );
+        Gia_ManStop( pTemp );
+    }
     // transform AIG with init state
     if ( p->pInits )
     {
@@ -1222,7 +1225,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple
         }
         else
         {
-            pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, 1 );
+            pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, fGiaSimple, 1 );
             Gia_ManDupRemapLiterals( vBits, pTemp );
             Gia_ManStop( pTemp );
         }