From 3b62ee457544bcc8f6191746bff895f2f98cddf9 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 20 May 2016 16:23:48 -0700
Subject: Enabling AIGs without structural hashing.

---
 src/base/abci/abc.c     |  4 ++--
 src/base/cba/cbaBlast.c |  2 +-
 src/base/wlc/wlcBlast.c | 15 +++++++++------
 3 files changed, 12 insertions(+), 9 deletions(-)

(limited to 'src/base')

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 );
         }
-- 
cgit v1.2.3