4 files changed, 43 insertions, 10 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index eef8675f..d312f437 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -496,19 +496,20 @@ static inline Gia_Obj_t * Gia_ManAppendObj( Gia_Man_t * p )
 { 
     if ( p->nObjs == p->nObjsAlloc )
     {
-        if ( 2 * p->nObjsAlloc > (1 << 29) )
+        int nObjNew = Abc_MinInt( 2 * p->nObjsAlloc, (1 << 29) );
+        if ( p->nObjs == (1 << 29) )
             printf( "Hard limit on the number of nodes (2^29) is reached. Quitting...\n" ), exit(1);
         if ( p->fVerbose )
-            printf("Extending GIA object storage: %d -> %d.\n", p->nObjsAlloc, 2 * p->nObjsAlloc );
+            printf("Extending GIA object storage: %d -> %d.\n", p->nObjsAlloc, nObjNew );
         assert( p->nObjsAlloc > 0 );
-        p->pObjs = ABC_REALLOC( Gia_Obj_t, p->pObjs, 2 * p->nObjsAlloc );
-        memset( p->pObjs + p->nObjsAlloc, 0, sizeof(Gia_Obj_t) * p->nObjsAlloc );
+        p->pObjs = ABC_REALLOC( Gia_Obj_t, p->pObjs, nObjNew );
+        memset( p->pObjs + p->nObjsAlloc, 0, sizeof(Gia_Obj_t) * (nObjNew - p->nObjsAlloc) );
         if ( p->pMuxes )
         {
-            p->pMuxes = ABC_REALLOC( unsigned, p->pMuxes, 2 * p->nObjsAlloc );
-            memset( p->pMuxes + p->nObjsAlloc, 0, sizeof(unsigned) * p->nObjsAlloc );
+            p->pMuxes = ABC_REALLOC( unsigned, p->pMuxes, nObjNew );
+            memset( p->pMuxes + p->nObjsAlloc, 0, sizeof(unsigned) * (nObjNew - p->nObjsAlloc) );
         }
-        p->nObjsAlloc *= 2;
+        p->nObjsAlloc = nObjNew;
     }
     return Gia_ManObj( p, p->nObjs++ );
 }
diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c
index b256b165..ae17c176 100644
--- a/src/aig/gia/giaHash.c
+++ b/src/aig/gia/giaHash.c
@@ -666,9 +666,14 @@ 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 = Gia_ManHashAnd( p, Abc_LitNot(iCtrl), iData0 );
-    int iTemp1 = Gia_ManHashAnd( p, iCtrl, iData1 );
-    return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), 1 );
+    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/giaJf.c b/src/aig/gia/giaJf.c
index 8ca16f29..f243dd8f 100644
--- a/src/aig/gia/giaJf.c
+++ b/src/aig/gia/giaJf.c
@@ -1500,6 +1500,7 @@ Gia_Man_t * Jf_ManDeriveGia( Jf_Man_t * p )
     Vec_IntFree( vCover );
     Gia_ManHashStop( pNew );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p->pGia) );
+//    Dsm_ManReportStats();
     return pNew;
 }
 
diff --git a/src/opt/dau/dauGia.c b/src/opt/dau/dauGia.c
index 4ced55e6..7fc7c92e 100644
--- a/src/opt/dau/dauGia.c
+++ b/src/opt/dau/dauGia.c
@@ -30,6 +30,11 @@ ABC_NAMESPACE_IMPL_START
 
 extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
 
+
+static int m_Calls = 0;
+static int m_NonDsd = 0;
+static int m_Non1Step = 0;
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -175,6 +180,7 @@ int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches,
         vLeaves.nSize = nVars;
         vLeaves.pArray = Fanins;        
         Res = Kit_TruthToGia( pGia, (unsigned *)&Func, nVars, vCover, &vLeaves, 1 );
+        m_Non1Step++;
         return Abc_LitNotCond( Res, fCompl );
     }
     assert( 0 );
@@ -209,12 +215,32 @@ int Dsm_ManDeriveGia( void * p, word uTruth, Vec_Int_t * vLeaves, Vec_Int_t * vC
     Gia_Man_t * pGia = (Gia_Man_t *)p;
     char pDsd[1000];
     int nSizeNonDec;
+    m_Calls++;
 //    static int Counter = 0; Counter++;
     nSizeNonDec = Dau_DsdDecompose( &uTruth, Vec_IntSize(vLeaves), 1, 1, pDsd );
+    if ( nSizeNonDec )
+        m_NonDsd++;
 //    printf( "%s\n", pDsd );
     return Dau_DsdToGia( pGia, pDsd, Vec_IntArray(vLeaves), vCover );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Convert TT to GIA via DSD.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dsm_ManReportStats()
+{
+    printf( "Calls = %d. NonDSD = %d. Non1Step = %d.\n", m_Calls, m_NonDsd, m_Non1Step );
+    m_Calls = m_NonDsd = m_Non1Step = 0;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///