Various modifications.

13 files changed, 141 insertions, 104 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 011f4f91..38f70c9c 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -927,10 +927,14 @@ static inline int         Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i )   { re
     for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ )      if ( !Gia_ObjIsMuxId(p, i) ) {} else
 #define Gia_ManForEachCi( p, pObj, i )                                  \
     for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((pObj) = Gia_ManCi(p, i)); i++ )
+#define Gia_ManForEachCiId( p, Id, i )                                  \
+    for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((Id) = Gia_ObjId(p, Gia_ManCi(p, i))); i++ )
 #define Gia_ManForEachCiReverse( p, pObj, i )                           \
     for ( i = Vec_IntSize(p->vCis) - 1; (i >= 0) && ((pObj) = Gia_ManCi(p, i)); i-- )
 #define Gia_ManForEachCo( p, pObj, i )                                  \
     for ( i = 0; (i < Vec_IntSize(p->vCos)) && ((pObj) = Gia_ManCo(p, i)); i++ )
+#define Gia_ManForEachCoId( p, Id, i )                                  \
+    for ( i = 0; (i < Vec_IntSize(p->vCos)) && ((Id) = Gia_ObjId(p, Gia_ManCo(p, i))); i++ )
 #define Gia_ManForEachCoReverse( p, pObj, i )                           \
     for ( i = Vec_IntSize(p->vCos) - 1; (i >= 0) && ((pObj) = Gia_ManCo(p, i)); i-- )
 #define Gia_ManForEachCoDriver( p, pObj, i )                            \
@@ -1172,7 +1176,9 @@ extern int                 Gia_MmStepReadMemUsage( Gia_MmStep_t * p );
 extern Gia_Man_t *         Gia_ManReadMiniAig( char * pFileName );
 extern void                Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName );
 /*=== giaMuxes.c ===========================================================*/
-extern Gia_Man_t *         Gia_ManDupMuxes( Gia_Man_t * p );
+extern void                Gia_ManCountMuxXor( Gia_Man_t * p, int * pnMuxes, int * pnXors );
+extern void                Gia_ManPrintMuxStats( Gia_Man_t * p );
+extern Gia_Man_t *         Gia_ManDupMuxes( Gia_Man_t * p, int Limit );
 extern Gia_Man_t *         Gia_ManDupNoMuxes( Gia_Man_t * p );
 /*=== giaPat.c ===========================================================*/
 extern void                Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit );
@@ -1282,7 +1288,6 @@ extern Vec_Int_t *         Gia_ManRequiredLevel( Gia_Man_t * p );
 extern void                Gia_ManCreateValueRefs( Gia_Man_t * p );
 extern void                Gia_ManCreateRefs( Gia_Man_t * p );
 extern int *               Gia_ManCreateMuxRefs( Gia_Man_t * p );
-extern void                Gia_ManCountMuxXor( Gia_Man_t * p, int * pnMuxes, int * pnXors );
 extern int                 Gia_ManCrossCut( Gia_Man_t * p, int fReverse );
 extern int                 Gia_ManIsNormalized( Gia_Man_t * p );
 extern Vec_Int_t *         Gia_ManCollectPoIds( Gia_Man_t * p );
diff --git a/src/aig/gia/giaBalance.c b/src/aig/gia/giaBalance.c
index 77b85b48..9760cf39 100644
--- a/src/aig/gia/giaBalance.c
+++ b/src/aig/gia/giaBalance.c
@@ -358,7 +358,7 @@ Gia_Man_t * Gia_ManBalance( Gia_Man_t * p, int fSimpleAnd, int fVerbose )
 {
     Gia_Man_t * pNew, * pNew1, * pNew2;
     if ( fVerbose )      Gia_ManPrintStats( p, NULL );
-    pNew = fSimpleAnd ? Gia_ManDup( p ) : Gia_ManDupMuxes( p );
+    pNew = fSimpleAnd ? Gia_ManDup( p ) : Gia_ManDupMuxes( p, 2 );
     if ( fVerbose )      Gia_ManPrintStats( pNew, NULL );
     pNew1 = Gia_ManBalanceInt( pNew );
     if ( fVerbose )      Gia_ManPrintStats( pNew1, NULL );
@@ -958,7 +958,7 @@ Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax,
     pNew0 = Gia_ManHasMapping(p) ? (Gia_Man_t *)Dsm_ManDeriveGia(p, 0) : p;
     if ( fVerbose )     Gia_ManPrintStats( pNew0, NULL );
     // derive internal manager
-    pNew = fSimpleAnd ? Gia_ManDup( pNew0 ) : Gia_ManDupMuxes( pNew0 );
+    pNew = fSimpleAnd ? Gia_ManDup( pNew0 ) : Gia_ManDupMuxes( pNew0, 2 );
     if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
     if ( pNew0 != p ) Gia_ManStop( pNew0 );
     // perform the operation
@@ -1046,7 +1046,7 @@ Gia_Man_t * Gia_ManAigSyn3( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
 {
     Gia_Man_t * pNew, * pTemp;
     Jf_Par_t Pars, * pPars = &Pars;
-    Lf_ManSetDefaultPars( pPars );
+    Jf_ManSetDefaultPars( pPars );
     pPars->nRelaxRatio = 40;
     if ( fVerbose )     Gia_ManPrintStats( p, NULL );
     if ( Gia_ManAndNum(p) == 0 )
@@ -1057,7 +1057,7 @@ Gia_Man_t * Gia_ManAigSyn3( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
     Gia_ManAigTransferPiLevels( pNew, p );
     // perform mapping
     pPars->nLutSize = 6;
-    pNew = Lf_ManPerformMapping( pTemp = pNew, pPars );
+    pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
     if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
 //    Gia_ManStop( pTemp );
     // perform balancing
@@ -1067,7 +1067,7 @@ Gia_Man_t * Gia_ManAigSyn3( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
     Gia_ManStop( pTemp );
     // perform mapping
     pPars->nLutSize = 4;
-    pNew = Lf_ManPerformMapping( pTemp = pNew, pPars );
+    pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
     if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
 //    Gia_ManStop( pTemp );
     // perform balancing
@@ -1081,7 +1081,7 @@ Gia_Man_t * Gia_ManAigSyn4( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
 {
     Gia_Man_t * pNew, * pTemp;
     Jf_Par_t Pars, * pPars = &Pars;
-    Lf_ManSetDefaultPars( pPars );
+    Jf_ManSetDefaultPars( pPars );
     pPars->nRelaxRatio = 40;
     if ( fVerbose )     Gia_ManPrintStats( p, NULL );
     if ( Gia_ManAndNum(p) == 0 )
@@ -1093,7 +1093,7 @@ Gia_Man_t * Gia_ManAigSyn4( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
     Gia_ManAigTransferPiLevels( pNew, p );
     // perform mapping
     pPars->nLutSize = 7;
-    pNew = Lf_ManPerformMapping( pTemp = pNew, pPars );
+    pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
     if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
 //    Gia_ManStop( pTemp );
     // perform extraction
@@ -1108,7 +1108,7 @@ Gia_Man_t * Gia_ManAigSyn4( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
     Gia_ManStop( pTemp );
     // perform mapping
     pPars->nLutSize = 5;
-    pNew = Lf_ManPerformMapping( pTemp = pNew, pPars );
+    pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
     if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
 //    Gia_ManStop( pTemp );
     // perform extraction
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 3b9e6d3b..f1470287 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -421,32 +421,13 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars )
     Abc_Print( 1, "  mem =%5.2f MB", Gia_ManMemory(p)/(1<<20) );
     if ( Gia_ManHasDangling(p) )
         Abc_Print( 1, "  ch =%5d", Gia_ManEquivCountClasses(p) );
-    if ( p->pMuxes )
-    {
-        int nAnds = Gia_ManAndNum(p)-Gia_ManXorNum(p)-Gia_ManMuxNum(p);
-        int nXors = Gia_ManXorNum(p);
-        int nMuxes = Gia_ManMuxNum(p);
-        int nTotal = nAnds + 3*nXors + 3*nMuxes;
-        Abc_Print( 1, "\nXOR/MUX stats:" );
-        Abc_Print( 1, "  xor =%8d (%6.2f %%)  ", nXors,  300.0*nXors/nTotal );
-        Abc_Print( 1, "  mux =%8d (%6.2f %%)  ", nMuxes, 300.0*nMuxes/nTotal );
-        Abc_Print( 1, "  and =%8d (%6.2f %%)  ", nAnds,  100.0*nAnds/nTotal );
-    }
-    else if ( pPars->fMuxXor )
-    {
-        int nAnds, nMuxes, nXors, nTotal = Gia_ManAndNum(p);
-        Gia_ManCountMuxXor( p, &nMuxes, &nXors );
-        nAnds = Gia_ManAndNum(p)-3*nMuxes-3*nXors;
-        Abc_Print( 1, "\nXOR/MUX stats:" );
-        Abc_Print( 1, "  xor =%8d (%6.2f %%)  ", nXors,  300.0*nXors/nTotal );
-        Abc_Print( 1, "  mux =%8d (%6.2f %%)  ", nMuxes, 300.0*nMuxes/nTotal );
-        Abc_Print( 1, "  and =%8d (%6.2f %%)  ", nAnds,  100.0*nAnds/nTotal );
-    }
+    if ( pPars && pPars->fMuxXor )
+        printf( "\nXOR/MUX " ), Gia_ManPrintMuxStats( p );
     if ( pPars && pPars->fSwitch )
     {
-        if ( p->pSwitching )
-            Abc_Print( 1, "  power =%7.2f", Gia_ManEvaluateSwitching(p) );
-        else
+//        if ( p->pSwitching )
+//            Abc_Print( 1, "  power =%7.2f", Gia_ManEvaluateSwitching(p) );
+//        else
             Abc_Print( 1, "  power =%7.2f", Gia_ManComputeSwitching(p, 48, 16, 0) );
     }
 //    Abc_Print( 1, "obj =%5d  ", Gia_ManObjNum(p) );
diff --git a/src/aig/gia/giaMuxes.c b/src/aig/gia/giaMuxes.c
index b4afe214..db44e219 100644
--- a/src/aig/gia/giaMuxes.c
+++ b/src/aig/gia/giaMuxes.c
@@ -33,7 +33,7 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
-  Synopsis    [Derives GIA with MUXes.]
+  Synopsis    [Counts XORs and MUXes.]
 
   Description []
                
@@ -42,7 +42,56 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManDupMuxes( Gia_Man_t * p )
+void Gia_ManCountMuxXor( Gia_Man_t * p, int * pnMuxes, int * pnXors )
+{
+    Gia_Obj_t * pObj, * pFan0, * pFan1; int i;
+    *pnMuxes = *pnXors = 0;
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( !Gia_ObjIsMuxType(pObj) )
+            continue;
+        if ( Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
+            (*pnXors)++;
+        else
+            (*pnMuxes)++;
+    }
+}
+void Gia_ManPrintMuxStats( Gia_Man_t * p )
+{
+    int nAnds, nMuxes, nXors, nTotal;
+    if ( p->pMuxes )
+    {
+        nAnds  = Gia_ManAndNum(p)-Gia_ManXorNum(p)-Gia_ManMuxNum(p);
+        nXors  = Gia_ManXorNum(p);
+        nMuxes = Gia_ManMuxNum(p);
+        nTotal = nAnds + 3*nXors + 3*nMuxes;
+    }
+    else 
+    {
+        Gia_ManCountMuxXor( p, &nMuxes, &nXors );
+        nAnds  = Gia_ManAndNum(p) - 3*nMuxes - 3*nXors;
+        nTotal = Gia_ManAndNum(p);
+    }
+    Abc_Print( 1, "stats:  " );
+    Abc_Print( 1, "xor =%8d %6.2f %%   ", nXors,  300.0*nXors/nTotal );
+    Abc_Print( 1, "mux =%8d %6.2f %%   ", nMuxes, 300.0*nMuxes/nTotal );
+    Abc_Print( 1, "and =%8d %6.2f %%   ", nAnds,  100.0*nAnds/nTotal );
+    Abc_Print( 1, "obj =%8d  ", Gia_ManAndNum(p) );
+    fflush( stdout );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives GIA with MUXes.]
+
+  Description [Create MUX if the sum of fanin references does not exceed limit.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupMuxes( Gia_Man_t * p, int Limit )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj, * pFan0, * pFan1, * pFanC;
@@ -51,7 +100,7 @@ Gia_Man_t * Gia_ManDupMuxes( Gia_Man_t * p )
     ABC_FREE( p->pRefs );
     Gia_ManCreateRefs( p ); 
     // start the new manager
-    pNew = Gia_ManStart( 5000 );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->pMuxes = ABC_CALLOC( unsigned, pNew->nObjsAlloc );
@@ -64,7 +113,7 @@ Gia_Man_t * Gia_ManDupMuxes( Gia_Man_t * p )
     Gia_ManHashStart( pNew );
     Gia_ManForEachAnd( p, pObj, i )
     {
-        if ( !Gia_ObjIsMuxType(pObj) || (Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)) > 1 || Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) > 1) )
+        if ( !Gia_ObjIsMuxType(pObj) || Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)) + Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) > Limit )
             pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
         else if ( Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
             pObj->Value = Gia_ManHashXorReal( pNew, Gia_ObjLitCopy(p, Gia_ObjToLit(p, pFan0)), Gia_ObjLitCopy(p, Gia_ObjToLit(p, pFan1)) );
@@ -147,7 +196,7 @@ Gia_Man_t * Gia_ManDupNoMuxes( Gia_Man_t * p )
 Gia_Man_t * Gia_ManDupMuxesTest( Gia_Man_t * p )
 {
     Gia_Man_t * pNew, * pNew2;
-    pNew = Gia_ManDupMuxes( p );
+    pNew = Gia_ManDupMuxes( p, 2 );
     pNew2 = Gia_ManDupNoMuxes( pNew );
     Gia_ManPrintStats( p, NULL );
     Gia_ManPrintStats( pNew, NULL );
@@ -277,7 +326,7 @@ void Gia_ManMuxProfiling( Gia_Man_t * p )
     Vec_Int_t * vCounts;
     int i, nRefs, Size, Count, Total = 0, Roots = 0;
 
-    pNew = Gia_ManDupMuxes( p );
+    pNew = Gia_ManDupMuxes( p, 2 );
     Gia_ManCreateRefs( pNew );
     Gia_ManForEachCo( pNew, pObj, i )
         Gia_ObjRefFanin0Inc( pNew, pObj );
diff --git a/src/aig/gia/giaResub.c b/src/aig/gia/giaResub.c
index 4b196fa4..b8c0e294 100644
--- a/src/aig/gia/giaResub.c
+++ b/src/aig/gia/giaResub.c
@@ -261,7 +261,7 @@ void Gia_ManAddDivisors( Gia_Man_t * p, Vec_Wec_t * vMffcs )
 void Gia_ManResubTest( Gia_Man_t * p )
 {
     Vec_Wec_t * vMffcs;
-    Gia_Man_t * pNew = Gia_ManDupMuxes( p );
+    Gia_Man_t * pNew = Gia_ManDupMuxes( p, 2 );
 abctime clkStart = Abc_Clock();
     vMffcs = Gia_ManComputeMffcs( pNew, 4, 100, 8, 100 );
     Gia_ManAddDivisors( pNew, vMffcs );
diff --git a/src/aig/gia/giaSwitch.c b/src/aig/gia/giaSwitch.c
index 5e97910b..a7b63864 100644
--- a/src/aig/gia/giaSwitch.c
+++ b/src/aig/gia/giaSwitch.c
@@ -758,6 +758,7 @@ float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbO
     // perform the computation of switching activity
     vSwitching = Gia_ManComputeSwitchProbs( pDfs, nFrames, nPref, fProbOne );
     // transfer the computed result to the original AIG
+    ABC_FREE( p->pSwitching );
     p->pSwitching = ABC_CALLOC( unsigned char, Gia_ManObjNum(p) );
     pSwitching = (float *)vSwitching->pArray;
     Gia_ManForEachObj( p, pObj, i )
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 365a8539..e16ee44f 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -746,34 +746,6 @@ int * Gia_ManCreateMuxRefs( Gia_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Assigns references.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_ManCountMuxXor( Gia_Man_t * p, int * pnMuxes, int * pnXors )
-{
-    Gia_Obj_t * pObj, * pFan0, * pFan1; 
-    int i;
-    *pnMuxes = 0;
-    *pnXors = 0;
-    Gia_ManForEachAnd( p, pObj, i )
-    {
-        if ( !Gia_ObjIsMuxType(pObj) )
-            continue;
-        if ( Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
-            (*pnXors)++;
-        else
-            (*pnMuxes)++;
-    }
-}
-
-/**Function*************************************************************
-
   Synopsis    [Computes the maximum frontier size.]
 
   Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 23873106..ee5a2b93 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -295,8 +295,8 @@ static int Abc_CommandInduction              ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandConstr                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandUnfold                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFold                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandUnfold2                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFold2                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandUnfold2                ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFold2                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBm                     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBm2                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSaucy                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -327,7 +327,7 @@ static int Abc_CommandAbc9PFan               ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9PSig               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Status             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Show               ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9Hash               ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Strash             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Topand             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Add1Hot            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Cof                ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -874,8 +874,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "constr",        Abc_CommandConstr,           0 );
     Cmd_CommandAdd( pAbc, "Verification", "unfold",        Abc_CommandUnfold,           1 );
     Cmd_CommandAdd( pAbc, "Verification", "fold",          Abc_CommandFold,             1 );
-    Cmd_CommandAdd( pAbc, "Verification", "unfold2",        Abc_CommandUnfold2,           1 );    // jlong 
-    Cmd_CommandAdd( pAbc, "Verification", "fold2",        Abc_CommandFold2,           1 );    // jlong 
+    Cmd_CommandAdd( pAbc, "Verification", "unfold2",       Abc_CommandUnfold2,          1 );    // jlong 
+    Cmd_CommandAdd( pAbc, "Verification", "fold2",         Abc_CommandFold2,            1 );    // jlong 
     Cmd_CommandAdd( pAbc, "Verification", "bm",            Abc_CommandBm,               1 );
     Cmd_CommandAdd( pAbc, "Verification", "bm2",           Abc_CommandBm2,              1 );
     Cmd_CommandAdd( pAbc, "Verification", "saucy3",        Abc_CommandSaucy,            1 );
@@ -903,7 +903,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&psig",         Abc_CommandAbc9PSig,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&status",       Abc_CommandAbc9Status,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&show",         Abc_CommandAbc9Show,         0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&st",           Abc_CommandAbc9Hash,         0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&st",           Abc_CommandAbc9Strash,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&topand",       Abc_CommandAbc9Topand,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&add1hot",      Abc_CommandAbc9Add1Hot,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&cof",          Abc_CommandAbc9Cof,          0 );
@@ -25622,17 +25622,29 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandAbc9Hash( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp;
-    int c, fAddStrash = 0;
+    int c, Limit = 2;
+    int fAddStrash = 0;
     int fCollapse = 0;
     int fAddMuxes = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "acmh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Lacmh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            Limit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( Limit < 0 )
+                goto usage;
+            break;
         case 'a':
             fAddStrash ^= 1;
             break;
@@ -25650,11 +25662,18 @@ int Abc_CommandAbc9Hash( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pGia == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9Hash(): There is no AIG.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9Strash(): There is no AIG.\n" );
         return 1;
     }
     if ( fAddMuxes )
-        pTemp = Gia_ManDupMuxes( pAbc->pGia );
+    {
+        if ( pAbc->pGia->pMuxes )
+        {
+            Abc_Print( -1, "Abc_CommandAbc9Strash(): The AIG already has MUXes.\n" );
+            return 1;
+        }
+        pTemp = Gia_ManDupMuxes( pAbc->pGia, Limit );
+    }
     else if ( fCollapse && pAbc->pGia->pAigExtra )
     {
         Gia_Man_t * pNew = Gia_ManDupUnnormalize( pAbc->pGia );
@@ -25663,18 +25682,21 @@ int Abc_CommandAbc9Hash( Abc_Frame_t * pAbc, int argc, char ** argv )
         pNew->pManTime = NULL;
         Gia_ManStop( pNew );
     }
+    else if ( pAbc->pGia->pMuxes )
+        pTemp = Gia_ManDupNoMuxes( pAbc->pGia );
     else
         pTemp = Gia_ManRehash( pAbc->pGia, fAddStrash );
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &st [-acmh]\n" );
-    Abc_Print( -2, "\t        performs structural hashing\n" );
-    Abc_Print( -2, "\t-a    : toggle additional hashing [default = %s]\n", fAddStrash? "yes": "no" );
-    Abc_Print( -2, "\t-c    : toggle collapsing hierarchical AIG [default = %s]\n", fCollapse? "yes": "no" );
-    Abc_Print( -2, "\t-m    : toggle converting to larger gates [default = %s]\n", fAddMuxes? "yes": "no" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
+    Abc_Print( -2, "usage: &st [-L num] [-acmh]\n" );
+    Abc_Print( -2, "\t         performs structural hashing\n" );
+    Abc_Print( -2, "\t-a     : toggle additional hashing [default = %s]\n", fAddStrash? "yes": "no" );
+    Abc_Print( -2, "\t-c     : toggle collapsing hierarchical AIG [default = %s]\n", fCollapse? "yes": "no" );
+    Abc_Print( -2, "\t-m     : toggle converting to larger gates [default = %s]\n", fAddMuxes? "yes": "no" );
+    Abc_Print( -2, "\t-L num : create MUX when sum of refs does not exceed this limit [default = %d]\n", Limit );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
 
@@ -29372,12 +29394,15 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
     nArgcNew = argc - globalUtilOptind;
     if ( nArgcNew != 1 )
     {
-        Abc_Print( -1, "File name is not given on the command line.\n" );
-        return 1;
+        if ( pAbc->pGia->pSpec == NULL )
+        {
+            Abc_Print( -1, "File name is not given on the command line.\n" );
+            return 1;
+        }
+        FileName = pAbc->pGia->pSpec;
     }
-
-    // get the input file name
-    FileName = pArgvNew[0];
+    else
+        FileName = pArgvNew[0];
     // fix the wrong symbol
     for ( pTemp = FileName; *pTemp; pTemp++ )
         if ( *pTemp == '>' )
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index c368cbf9..9f709411 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -500,9 +500,11 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPrepr
     if ( p->pPars->fVerbose )
     {
         char Symb = fPreprocess? 'P' : ((Mode == 0)? 'D' : ((Mode == 1)? 'F' : 'A'));
-        Abc_Print( 1, "%c: Del = %7.2f. Ar = %9.1f. Edge = %8d. Switch = %7.2f. Cut = %8d. ", 
-            Symb, p->RequiredGlo, p->AreaGlo, p->nNets, p->dPower, p->nCutsMerged );
-//        printf( "Cut0 =%4d. Cut1 =%4d. ", p->nBestCutSmall[0], p->nBestCutSmall[1] );
+        Abc_Print( 1, "%c:  Del = %7.2f.  Ar = %9.1f.  Edge = %8d.  ", 
+            Symb, p->RequiredGlo, p->AreaGlo, p->nNets );
+        if ( p->dPower )
+        Abc_Print( 1, "Switch = %7.2f.  ", p->dPower );
+        Abc_Print( 1, "Cut = %8d.  ", p->nCutsMerged );
         Abc_PrintTime( 1, "T", Abc_Clock() - clk );
 //    Abc_Print( 1, "Max number of cuts = %d. Average number of cuts = %5.2f.\n", 
 //        p->nCutsMax, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
diff --git a/src/map/if/ifReduce.c b/src/map/if/ifReduce.c
index fec999cb..d50bc40c 100644
--- a/src/map/if/ifReduce.c
+++ b/src/map/if/ifReduce.c
@@ -57,8 +57,11 @@ void If_ManImproveMapping( If_Man_t * p )
     If_ManComputeRequired( p );
     if ( p->pPars->fVerbose )
     {
-        Abc_Print( 1, "E: Del = %7.2f. Ar = %9.1f. Edge = %8d. Switch = %7.2f. Cut = %8d. ", 
-            p->RequiredGlo, p->AreaGlo, p->nNets, p->dPower, p->nCutsMerged );
+        Abc_Print( 1, "E:  Del = %7.2f.  Ar = %9.1f.  Edge = %8d.  ", 
+            p->RequiredGlo, p->AreaGlo, p->nNets );
+        if ( p->dPower )
+        Abc_Print( 1, "Switch = %7.2f.  ", p->dPower );
+        Abc_Print( 1, "Cut = %8d.  ", p->nCutsMerged );
         Abc_PrintTime( 1, "T", Abc_Clock() - clk );
     }
 }
diff --git a/src/map/mpm/mpmCore.c b/src/map/mpm/mpmCore.c
index de2d7bc7..1395d1d0 100644
--- a/src/map/mpm/mpmCore.c
+++ b/src/map/mpm/mpmCore.c
@@ -95,7 +95,7 @@ Gia_Man_t * Mpm_ManLutMapping( Gia_Man_t * pGia, Mpm_Par_t * pPars )
     assert( pPars->nNumCuts <= MPM_CUT_MAX );
     if ( pPars->fUseGates )
     {
-        pGia = Gia_ManDupMuxes( pGia );
+        pGia = Gia_ManDupMuxes( pGia, 2 );
         p = Mig_ManCreate( pGia );
         Gia_ManStop( pGia );
     }
diff --git a/src/map/mpm/mpmGates.c b/src/map/mpm/mpmGates.c
index aa70e143..d2af268d 100644
--- a/src/map/mpm/mpmGates.c
+++ b/src/map/mpm/mpmGates.c
@@ -287,7 +287,7 @@ Abc_Ntk_t * Mpm_ManCellMapping( Gia_Man_t * pGia, Mpm_Par_t * pPars, void * pMio
     assert( pPars->nNumCuts <= MPM_CUT_MAX );
     if ( pPars->fUseGates )
     {
-        pGia = Gia_ManDupMuxes( pGia );
+        pGia = Gia_ManDupMuxes( pGia, 2 );
         p = Mig_ManCreate( pGia );
         Gia_ManStop( pGia );
     }
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index f3b1a3b0..b43700ae 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -66,14 +66,13 @@ void Cec_ManTransformPattern( Gia_Man_t * p, int iOut, int * pValues )
   SeeAlso     []
 
 ***********************************************************************/
-int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail )
+int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail, abctime clkTotal )
 {
 //    extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
     extern int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs );
     Gia_Man_t * pTemp = Gia_ManTransformMiter( pMiter );
     Aig_Man_t * pMiterCec = Gia_ManToAig( pTemp, 0 );
     int RetValue, iOut, nOuts;
-    abctime clkTotal = Abc_Clock();
     if ( piOutFail )
         *piOutFail = -1;
     Gia_ManStop( pTemp );
@@ -83,12 +82,12 @@ int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail )
     if ( RetValue == 1 )
     {
         Abc_Print( 1, "Networks are equivalent.   " );
-Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
     }
     else if ( RetValue == 0 )
     {
         Abc_Print( 1, "Networks are NOT EQUIVALENT.   " );
-Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
         if ( pMiterCec->pData == NULL )
             Abc_Print( 1, "Counter-example is not available.\n" );
         else
@@ -113,7 +112,7 @@ Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
     else
     {
         Abc_Print( 1, "Networks are UNDECIDED.   " );
-Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
     }
     fflush( stdout );
     Aig_ManStop( pMiterCec );
@@ -275,7 +274,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
     if ( pPars->fVerbose )
         Abc_Print( 1, "Calling the old CEC engine.\n" );
     fflush( stdout );
-    RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose, &pPars->iOutFail );
+    RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose, &pPars->iOutFail, clkTotal );
     p->pCexComb = pNew->pCexComb; pNew->pCexComb = NULL;
     if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) )
         Abc_Print( 1, "Counter-example simulation has failed.\n" );