Updates and changes to several packages.

12 files changed, 162 insertions, 40 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index f3a40ca1..6fc30367 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -255,6 +255,7 @@ struct Jf_Par_t_
     int            nRoundsEla;
     int            nRelaxRatio;
     int            nCoarseLimit;
+    int            nAreaTuner;
     int            nVerbLimit;
     int            DelayTarget;
     int            fAreaOnly;
@@ -911,11 +912,12 @@ static inline void        Gia_ObjSetFanout( Gia_Man_t * p, Gia_Obj_t * pObj, int
 #define Gia_ObjForEachFanoutStaticId( p, Id, FanId, i )      \
     for ( i = 0; (i < Gia_ObjFanoutNumId(p, Id))   && (((FanId) = Gia_ObjFanoutId(p, Id, i)), 1); i++ )
 
-static inline int         Gia_ManHasMapping( Gia_Man_t * p )                { return p->vMapping != NULL;                }
-static inline int         Gia_ObjIsLut( Gia_Man_t * p, int Id )             { return Vec_IntEntry(p->vMapping, Id) != 0; }
+static inline int         Gia_ManHasMapping( Gia_Man_t * p )                { return p->vMapping != NULL;                                            }
+static inline int         Gia_ObjIsLut( Gia_Man_t * p, int Id )             { return Vec_IntEntry(p->vMapping, Id) != 0;                             }
 static inline int         Gia_ObjLutSize( Gia_Man_t * p, int Id )           { return Vec_IntEntry(p->vMapping, Vec_IntEntry(p->vMapping, Id));       }
 static inline int *       Gia_ObjLutFanins( Gia_Man_t * p, int Id )         { return Vec_IntEntryP(p->vMapping, Vec_IntEntry(p->vMapping, Id)) + 1;  }
-static inline int         Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i )   { return Gia_ObjLutFanins(p, Id)[i];         }
+static inline int         Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i )   { return Gia_ObjLutFanins(p, Id)[i];                                     }
+static inline int         Gia_ObjLutIsMux( Gia_Man_t * p, int Id )          { return (int)(Gia_ObjLutFanins(p, Id)[Gia_ObjLutSize(p, Id)] == -Id);   }
 
 #define Gia_ManForEachLut( p, i )                              \
     for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsLut(p, i) ) {} else
@@ -1334,6 +1336,7 @@ extern Vec_Int_t *         Gia_ManCollectPoIds( Gia_Man_t * p );
 extern int                 Gia_ObjIsMuxType( Gia_Obj_t * pNode );
 extern int                 Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ppFan0, Gia_Obj_t ** ppFan1 );
 extern Gia_Obj_t *         Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE );
+extern int                 Gia_ObjRecognizeMuxLits( Gia_Man_t * p, Gia_Obj_t * pNode, int * iLitT, int * iLitE );
 extern int                 Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode );
 extern int                 Gia_ManHasDangling( Gia_Man_t * p );
 extern int                 Gia_ManMarkDangling( Gia_Man_t * p );
diff --git a/src/aig/gia/giaBalance.c b/src/aig/gia/giaBalance.c
index abb6dd19..611bbf87 100644
--- a/src/aig/gia/giaBalance.c
+++ b/src/aig/gia/giaBalance.c
@@ -1032,6 +1032,7 @@ Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fOldAlgo, int fCoarsen, int fCutM
         pPars->fCoarsen    = fCoarsen;
         pPars->fCutMin     = fCutMin;
         pPars->nRelaxRatio = nRelaxRatio;
+        pPars->nAreaTuner  = 1;
     }
     if ( fVerbose )     Gia_ManPrintStats( p, NULL );
     if ( Gia_ManAndNum(p) == 0 )
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 537ffd0a..20204798 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -318,29 +318,32 @@ void Gia_ManPrintGetMuxFanins( Gia_Man_t * p, Gia_Obj_t * pObj, int * pFanins )
 }
 int Gia_ManCountDupLut6( Gia_Man_t * p )
 {
-    int i, nCountDup = 0, nCountPis = 0;
-    Gia_ManCleanMark0( p );
+    int i, nCountDup = 0, nCountPis = 0, nCountMux = 0;
+    Gia_ManCleanMark01( p );
     Gia_ManForEachLut( p, i )
-        if ( Gia_ObjLutSize(p, i) == 3 && Gia_ObjLutFanins(p, i)[3] == -i )
+        if ( Gia_ObjLutSize(p, i) == 3 && Gia_ObjLutIsMux(p, i) )
         {
             Gia_Obj_t * pFanin;
             int pFanins[3];
             Gia_ManPrintGetMuxFanins( p, Gia_ManObj(p, i), pFanins );
+            Gia_ManObj(p, i)->fMark1 = 1;
 
             pFanin = Gia_ManObj(p, pFanins[1]);
             nCountPis += Gia_ObjIsCi(pFanin);
             nCountDup += pFanin->fMark0;
+            nCountMux += pFanin->fMark1;
             pFanin->fMark0 = 1;
 
             pFanin = Gia_ManObj(p, pFanins[2]);
             nCountPis += Gia_ObjIsCi(pFanin);
             nCountDup += pFanin->fMark0;
+            nCountMux += pFanin->fMark1;
             pFanin->fMark0 = 1;
         }
-    Gia_ManCleanMark0( p );
-    if ( nCountDup + nCountPis )
-        printf( "Dup fanins = %d.  CI fanins = %d.  Total = %d.  (%.2f %%)\n", 
-            nCountDup, nCountPis, nCountDup + nCountPis, 100.0 * (nCountDup + nCountPis) / Gia_ManLutNum(p) );
+    Gia_ManCleanMark01( p );
+    if ( nCountDup + nCountPis + nCountMux )
+        printf( "Dup fanins = %d.  CI fanins = %d.  MUX fanins = %d.  Total = %d.  (%.2f %%)\n", 
+            nCountDup, nCountPis, nCountMux, nCountDup + nCountPis, 100.0 * (nCountDup + nCountPis + nCountMux) / Gia_ManLutNum(p) );
     return nCountDup + nCountPis;
 }
 
@@ -354,7 +357,7 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p, char * pDumpFile )
     pLevels = ABC_CALLOC( int, Gia_ManObjNum(p) );
     Gia_ManForEachLut( p, i )
     {
-        if ( Gia_ObjLutSize(p, i) == 3 && Gia_ObjLutFanins(p, i)[3] == -i )
+        if ( Gia_ObjLutSize(p, i) == 3 && Gia_ObjLutIsMux(p, i) )
         {
             int pFanins[3];
             Gia_ManPrintGetMuxFanins( p, Gia_ManObj(p, i), pFanins );
@@ -1576,7 +1579,7 @@ void Gia_ManTransferMapping( Gia_Man_t * pGia, Gia_Man_t * p )
         Vec_IntPush( p->vMapping, Gia_ObjLutSize(pGia, i) );
         Gia_LutForEachFanin( pGia, i, iFan, k )
             Vec_IntPush( p->vMapping, Abc_Lit2Var(Gia_ObjValue(Gia_ManObj(pGia, iFan))) );
-        Vec_IntPush( p->vMapping, Gia_ObjId(p, pObj) );
+        Vec_IntPush( p->vMapping, Gia_ObjLutIsMux(pGia, i) ? -Gia_ObjId(p, pObj) : Gia_ObjId(p, pObj) );
     }
     Gia_ManMappingVerify( p );
 }
diff --git a/src/aig/gia/giaLf.c b/src/aig/gia/giaLf.c
index ebd0dc18..96a633f4 100644
--- a/src/aig/gia/giaLf.c
+++ b/src/aig/gia/giaLf.c
@@ -52,10 +52,6 @@ Gia_Man_t * Lf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
 {
     return Jf_ManPerformMapping( pGia, pPars );
 }
-Gia_Man_t * Gia_ManPerformLfMapping( Gia_Man_t * p, Jf_Par_t * pPars, int fNormalized )
-{
-    return Jf_ManPerformMapping( p, pPars );
-}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/gia/giaMf.c b/src/aig/gia/giaMf.c
index 0ff54c8d..da571904 100644
--- a/src/aig/gia/giaMf.c
+++ b/src/aig/gia/giaMf.c
@@ -943,7 +943,7 @@ static inline int Mf_CutArea( Mf_Man_t * p, int nLeaves, int iFunc )
     if ( p->pPars->fGenCnf )
         return Vec_IntEntry(&p->vCnfSizes, Abc_Lit2Var(iFunc));
     if ( p->pPars->fOptEdge )
-        return nLeaves + 1;
+        return nLeaves + p->pPars->nAreaTuner;
     return 1;
 }
 static inline void Mf_CutParams( Mf_Man_t * p, Mf_Cut_t * pCut, float FlowRefs )
@@ -1386,6 +1386,7 @@ void Mf_ManSetDefaultPars( Jf_Par_t * pPars )
     pPars->nRoundsEla   =  1;
     pPars->nRelaxRatio  =  0;
     pPars->nCoarseLimit =  3;
+    pPars->nAreaTuner   =  1;
     pPars->nVerbLimit   =  5;
     pPars->DelayTarget  = -1;
     pPars->fAreaOnly    =  0;
diff --git a/src/aig/gia/giaStr.c b/src/aig/gia/giaStr.c
index 823d7f27..13ddb233 100644
--- a/src/aig/gia/giaStr.c
+++ b/src/aig/gia/giaStr.c
@@ -43,7 +43,7 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Str_NormalizeTest( Gia_Man_t * p, int nLutSize, int fUseMuxes, int fVerbose )
+Gia_Man_t * Gia_ManLutBalance( Gia_Man_t * p, int nLutSize, int fUseMuxes, int fRecursive, int fOptArea, int fVerbose )
 {
     return Gia_ManDup(p);
 }
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index e37022c3..7bf29b18 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1052,6 +1052,15 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob
     assert( 0 ); // this is not MUX
     return NULL;
 }
+int Gia_ObjRecognizeMuxLits( Gia_Man_t * p, Gia_Obj_t * pNode, int * iLitT, int * iLitE )
+{
+    Gia_Obj_t * pNodeT, * pNodeE;
+    Gia_Obj_t * pCtrl = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
+    assert( pCtrl != NULL );
+    *iLitT = Gia_Obj2Lit( p, pNodeT );
+    *iLitE = Gia_Obj2Lit( p, pNodeE );
+    return Gia_Obj2Lit( p, pCtrl );
+}
 
 
 /**Function*************************************************************
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 8d00ca57..08069f98 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -10422,7 +10422,7 @@ int Abc_CommandTestColor( Abc_Frame_t * pAbc, int argc, char ** argv )
 ***********************************************************************/
 int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-//    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     int nCutMax      =  1;
     int nLeafMax     =  4;
     int nDivMax      =  2;
@@ -10581,7 +10581,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //        extern void Abc_EnumerateFuncs( int nDecMax, int nDivMax, int fVerbose );
 //        Abc_EnumerateFuncs( nDecMax, nDivMax, fVerbose );
     }
-
+/*
     if ( fNewAlgo )
     {
         extern void Abc_SuppTest( int nOnes, int nVars, int fUseSimple, int fCheck, int fVerbose );
@@ -10592,11 +10592,18 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         extern void Bmc_EcoMiterTest();
         Bmc_EcoMiterTest();
     }
-/*
+*/
     if ( pNtk )
     {
         extern Abc_Ntk_t * Abc_NtkBarBufsOnOffTest( Abc_Ntk_t * pNtk );
         Abc_Ntk_t * pNtkRes = Abc_NtkBarBufsOnOffTest( pNtk );
+//        extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
+//        extern Abc_Ntk_t * Abc_NtkPcmTestAig( Abc_Ntk_t * pNtk, int fVerbose );
+//        Abc_Ntk_t * pNtkRes;
+//        if ( Abc_NtkIsLogic(pNtk) )
+//            pNtkRes = Abc_NtkPcmTest( pNtk, fVerbose );
+//        else
+//            pNtkRes = Abc_NtkPcmTestAig( pNtk, fVerbose );
         if ( pNtkRes == NULL )
         {
             Abc_Print( -1, "Command has failed.\n" );
@@ -10604,7 +10611,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
         Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     }
-*/
     return 0;
 usage:
     Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );
@@ -27838,7 +27844,7 @@ usage:
 int Abc_CommandAbc9BalanceLut( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern Gia_Man_t * Gia_ManBalanceLut( Gia_Man_t * p, int nLutSize, int nCutNum, int fVerbose );
-    extern Gia_Man_t * Str_NormalizeTest( Gia_Man_t * p, int nLutSize, int fUseMuxes, int fRecursive, int fOptArea, int fVerbose );
+    extern Gia_Man_t * Gia_ManLutBalance( Gia_Man_t * p, int nLutSize, int fUseMuxes, int fRecursive, int fOptArea, int fVerbose );
     Gia_Man_t * pTemp = NULL;
     int fUseOld      = 0;
     int nLutSize     = 6;
@@ -27907,7 +27913,7 @@ int Abc_CommandAbc9BalanceLut( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( fUseOld )
         pTemp = Gia_ManBalanceLut( pAbc->pGia, nLutSize, nCutNum, fVerbose );
     else
-        pTemp = Str_NormalizeTest( pAbc->pGia, nLutSize, fUseMuxes, fRecursive, fOptArea, fVerbose );
+        pTemp = Gia_ManLutBalance( pAbc->pGia, nLutSize, fUseMuxes, fRecursive, fOptArea, fVerbose );
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
@@ -31122,7 +31128,7 @@ int Abc_CommandAbc9Lf( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_Man_t * pNew; int c;
     Lf_ManSetDefaultPars( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFARLDWaekmupgtvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFARLEDWaekmupgtvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -31198,6 +31204,17 @@ int Abc_CommandAbc9Lf( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nCoarseLimit < 0 ) 
                 goto usage;
             break;
+        case 'E':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( 1, "Command line switch \"-E\" should be followed by a floating point number.\n" );
+                return 0;
+            }
+            pPars->nAreaTuner = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nAreaTuner < 0 ) 
+                goto usage;
+            break;
         case 'D':
             if ( globalUtilOptind >= argc )
             {
@@ -31276,7 +31293,7 @@ usage:
         sprintf(Buffer, "best possible" );
     else
         sprintf(Buffer, "%d", pPars->DelayTarget );
-    Abc_Print( -2, "usage: &lf [-KCFARLD num] [-kmupgtvwh]\n" );
+    Abc_Print( -2, "usage: &lf [-KCFARLED num] [-kmupgtvwh]\n" );
     Abc_Print( -2, "\t           performs technology mapping of the network\n" );
     Abc_Print( -2, "\t-K num   : LUT size for the mapping (2 <= K <= %d) [default = %d]\n", pPars->nLutSizeMax, pPars->nLutSize );
     Abc_Print( -2, "\t-C num   : the max number of priority cuts (1 <= C <= %d) [default = %d]\n", pPars->nCutNumMax, pPars->nCutNum );
@@ -31284,6 +31301,7 @@ usage:
     Abc_Print( -2, "\t-A num   : the number of exact area rounds [default = %d]\n", pPars->nRoundsEla );
     Abc_Print( -2, "\t-R num   : the delay relaxation ratio (num >= 0) [default = %d]\n", pPars->nRelaxRatio );
     Abc_Print( -2, "\t-L num   : the fanout limit for coarsening XOR/MUX (num >= 2) [default = %d]\n", pPars->nCoarseLimit );
+    Abc_Print( -2, "\t-E num   : the area/edge tradeoff parameter (0 <= num <= 100) [default = %d]\n", pPars->nAreaTuner );
     Abc_Print( -2, "\t-D num   : sets the delay constraint for the mapping [default = %s]\n", Buffer );
 //    Abc_Print( -2, "\t-a       : toggles area-oriented mapping [default = %s]\n", pPars->fAreaOnly? "yes": "no" );
     Abc_Print( -2, "\t-e       : toggles edge vs node minimization [default = %s]\n", pPars->fOptEdge? "yes": "no" );
@@ -31317,7 +31335,7 @@ int Abc_CommandAbc9Mf( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_Man_t * pNew; int c;
     Mf_ManSetDefaultPars( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFARLDWaekmcgvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFARLEDWaekmcgvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -31393,6 +31411,17 @@ int Abc_CommandAbc9Mf( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nCoarseLimit < 0 ) 
                 goto usage;
             break;
+        case 'E':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( 1, "Command line switch \"-E\" should be followed by a floating point number.\n" );
+                return 0;
+            }
+            pPars->nAreaTuner = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nAreaTuner < 0 ) 
+                goto usage;
+            break;
         case 'D':
             if ( globalUtilOptind >= argc )
             {
@@ -31467,7 +31496,7 @@ usage:
         sprintf(Buffer, "best possible" );
     else
         sprintf(Buffer, "%d", pPars->DelayTarget );
-    Abc_Print( -2, "usage: &mf [-KCFARLD num] [-akmcgvwh]\n" );
+    Abc_Print( -2, "usage: &mf [-KCFARLED num] [-akmcgvwh]\n" );
     Abc_Print( -2, "\t           performs technology mapping of the network\n" );
     Abc_Print( -2, "\t-K num   : LUT size for the mapping (2 <= K <= %d) [default = %d]\n", pPars->nLutSizeMax, pPars->nLutSize );
     Abc_Print( -2, "\t-C num   : the max number of priority cuts (1 <= C <= %d) [default = %d]\n", pPars->nCutNumMax, pPars->nCutNum );
@@ -31475,6 +31504,7 @@ usage:
     Abc_Print( -2, "\t-A num   : the number of exact area rounds [default = %d]\n", pPars->nRoundsEla );
     Abc_Print( -2, "\t-R num   : the delay relaxation ratio (num >= 0) [default = %d]\n", pPars->nRelaxRatio );
     Abc_Print( -2, "\t-L num   : the fanout limit for coarsening XOR/MUX (num >= 2) [default = %d]\n", pPars->nCoarseLimit );
+    Abc_Print( -2, "\t-E num   : the area/edge tradeoff parameter (0 <= num <= 100) [default = %d]\n", pPars->nAreaTuner );
     Abc_Print( -2, "\t-D num   : sets the delay constraint for the mapping [default = %s]\n", Buffer );
     Abc_Print( -2, "\t-a       : toggles area-oriented mapping [default = %s]\n", pPars->fAreaOnly? "yes": "no" );
     Abc_Print( -2, "\t-e       : toggles edge vs node minimization [default = %s]\n", pPars->fOptEdge? "yes": "no" );
diff --git a/src/base/abci/abcRec3.c b/src/base/abci/abcRec3.c
index 72e7d551..e96a6a52 100644
--- a/src/base/abci/abcRec3.c
+++ b/src/base/abci/abcRec3.c
@@ -478,7 +478,7 @@ void Lms_ManPrintFreqStats( Lms_Man_t * p )
         }
 
         // check the non dec core
-        Status = Dau_DsdCheck1Step( pTruth, nNonDecSize );
+        Status = Dau_DsdCheck1Step( NULL, pTruth, nNonDecSize, NULL );
         if ( Status >= 0 )
         {
             CountStepNpn[1]++;
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h
index 0ccee987..ddffa905 100644
--- a/src/opt/dau/dau.h
+++ b/src/opt/dau/dau.h
@@ -80,6 +80,7 @@ extern unsigned      Abc_TtCanonicizePhase( word * pTruth, int nVars );
 /*=== dauDsd.c  ==========================================================*/
 extern int *         Dau_DsdComputeMatches( char * p );
 extern int           Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char * pRes );
+extern int           Dau_DsdDecomposeLevel( word * pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char * pRes, int * pVarLevels );
 extern void          Dau_DsdPrintFromTruthFile( FILE * pFile, word * pTruth, int nVarsInit );
 extern void          Dau_DsdPrintFromTruth( word * pTruth, int nVarsInit );
 extern word *        Dau_DsdToTruth( char * p, int nVars );
@@ -87,7 +88,7 @@ extern word          Dau_Dsd6ToTruth( char * p );
 extern void          Dau_DsdNormalize( char * p );
 extern int           Dau_DsdCountAnds( char * pDsd );
 extern void          Dau_DsdTruthCompose_rec( word * pFunc, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word * pRes, int nVars, int nWordsR );
-extern int           Dau_DsdCheck1Step( word * pTruth, int nVarsInit );
+extern int           Dau_DsdCheck1Step( void * p, word * pTruth, int nVarsInit, int * pVarLevels );
 
 /*=== dauGia.c  ==========================================================*/
 extern int           Dsm_ManTruthToGia( void * p, word * pTruth, Vec_Int_t * vLeaves, Vec_Int_t * vCover );
diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c
index e5d83d0c..8469da4b 100644
--- a/src/opt/dau/dauDsd.c
+++ b/src/opt/dau/dauDsd.c
@@ -890,24 +890,43 @@ void Dau_DsdTest3()
   SeeAlso     []
 
 ***********************************************************************/
-int Dau_DsdCheck1Step( word * pTruth, int nVarsInit )
+int Dau_DsdCheck1Step( void * p, word * pTruth, int nVarsInit, int * pVarLevels )
 {
     word pCofTemp[DAU_MAX_WORD];
+    int pVarPrios[DAU_MAX_VAR];
     int nWords = Abc_TtWordNum(nVarsInit);
     int nSizeNonDec, nSizeNonDec0, nSizeNonDec1;
-    int v, vBest = -2, nSumCofsBest = ABC_INFINITY, nSumCofs;
+    int i, vBest = -2, nSumCofsBest = ABC_INFINITY, nSumCofs;
     nSizeNonDec = Dau_DsdDecompose( pTruth, nVarsInit, 0, 0, NULL );
     if ( nSizeNonDec == 0 )
         return -1;
     assert( nSizeNonDec > 0 );
-    for ( v = 0; v < nVarsInit; v++ )
+    // find variable priority
+    for ( i = 0; i < nVarsInit; i++ )
+        pVarPrios[i] = i;
+    if ( pVarLevels )
+    {
+        extern int Dau_DsdLevelVar( void * pMan, int iVar );
+        int pVarLevels[DAU_MAX_VAR];
+        for ( i = 0; i < nVarsInit; i++ )
+            pVarLevels[i] = -Dau_DsdLevelVar( p, i );
+//        for ( i = 0; i < nVarsInit; i++ )
+//            printf( "%d ", -pVarLevels[i] );
+//        printf( "\n" );
+        Vec_IntSelectSortCost2( pVarPrios, nVarsInit, pVarLevels );
+//        for ( i = 0; i < nVarsInit; i++ )
+//            printf( "%d ", pVarPrios[i] );
+//        printf( "\n\n" );
+    }
+    for ( i = 0; i < nVarsInit; i++ )
     {
+        assert( pVarPrios[i] >= 0 && pVarPrios[i] < nVarsInit );
         // try first cofactor
-        Abc_TtCofactor0p( pCofTemp, pTruth, nWords, v );
+        Abc_TtCofactor0p( pCofTemp, pTruth, nWords, pVarPrios[i] );
         nSumCofs = Abc_TtSupportSize( pCofTemp, nVarsInit );
         nSizeNonDec0 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, 0, NULL );
         // try second cofactor
-        Abc_TtCofactor1p( pCofTemp, pTruth, nWords, v );
+        Abc_TtCofactor1p( pCofTemp, pTruth, nWords, pVarPrios[i] );
         nSumCofs += Abc_TtSupportSize( pCofTemp, nVarsInit );
         nSizeNonDec1 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, 0, NULL );
         // compare cofactors
@@ -915,7 +934,7 @@ int Dau_DsdCheck1Step( word * pTruth, int nVarsInit )
             continue;
         if ( nSumCofsBest > nSumCofs )
         {
-            vBest = v;
+            vBest = pVarPrios[i];
             nSumCofsBest = nSumCofs;
         }
     }
@@ -944,6 +963,7 @@ struct Dau_Dsd_t_
     int      uConstMask;           // constant decomposition mask
     int      fSplitPrime;          // represent prime function as 1-step DSD
     int      fWriteTruth;          // writing truth table as a hex string
+    int *    pVarLevels;           // variable levels
     char     pVarDefs[32][8];      // variable definitions
     char     Cache[32][32];        // variable cache
     char     pOutput[DAU_MAX_STR]; // output stream
@@ -995,6 +1015,21 @@ static inline void Dau_DsdWriteVar( Dau_Dsd_t * p, int iVar, int fInv )
         else
             p->pOutput[ p->nPos++ ] = *pStr;
 }
+int Dau_DsdLevelVar( void * pMan, int iVar )
+{
+    Dau_Dsd_t * p = (Dau_Dsd_t *)pMan;
+    char * pStr;
+    int LevelMax = 0, Level;
+    for ( pStr = p->pVarDefs[iVar]; *pStr; pStr++ )
+    {
+        if ( *pStr >= 'a' + p->nVarsInit && *pStr < 'a' + p->nVarsUsed )
+            Level = 1 + Dau_DsdLevelVar( p, *pStr - 'a' );
+        else
+            Level = p->pVarLevels[*pStr - 'a'];
+        LevelMax = Abc_MaxInt( LevelMax, Level );
+    }
+    return LevelMax;
+}
 static inline void Dau_DsdTranslate( Dau_Dsd_t * p, int * pVars, int nVars, char * pStr )
 {
     for ( ; *pStr; pStr++ )
@@ -1011,7 +1046,7 @@ static inline int Dau_DsdWritePrime( Dau_Dsd_t * p, word * pTruth, int * pVars,
     {
         word pCofTemp[DAU_MAX_WORD];
         int nWords = Abc_TtWordNum(nVars);
-        int vBest = Dau_DsdCheck1Step( pTruth, nVars );
+        int vBest = Dau_DsdCheck1Step( p, pTruth, nVars, p->pVarLevels );
         assert( vBest != -1 );
         if ( vBest == -2 ) // non-dec
             p->nPos += Abc_TtWriteHexRev( p->pOutput + p->nPos, pTruth, nVars );
@@ -1879,6 +1914,31 @@ int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, int fWriteT
     Dau_Dsd_t P, * p = &P;
     p->fSplitPrime = fSplitPrime;
     p->fWriteTruth = fWriteTruth;
+    p->pVarLevels  = NULL;
+    p->nSizeNonDec = 0;
+    if ( (pTruth[0] & 1) == 0 && Abc_TtIsConst0(pTruth, Abc_TtWordNum(nVarsInit)) )
+        { if ( pRes ) pRes[0] = '0', pRes[1] = 0; }
+    else if ( (pTruth[0] & 1) && Abc_TtIsConst1(pTruth, Abc_TtWordNum(nVarsInit)) )
+        { if ( pRes ) pRes[0] = '1', pRes[1] = 0; }
+    else 
+    {
+        int Status = Dau_DsdDecomposeInt( p, pTruth, nVarsInit );
+        Dau_DsdRemoveBraces( p->pOutput, Dau_DsdComputeMatches(p->pOutput) );
+        if ( pRes )
+            strcpy( pRes, p->pOutput );
+        assert( fSplitPrime || Status != 1 );
+        if ( fSplitPrime && Status == 2 )
+            return -1;
+    }
+//    assert( p->nSizeNonDec == 0 );
+    return p->nSizeNonDec;
+}
+int Dau_DsdDecomposeLevel( word * pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char * pRes, int * pVarLevels )
+{
+    Dau_Dsd_t P, * p = &P;
+    p->fSplitPrime = fSplitPrime;
+    p->fWriteTruth = fWriteTruth;
+    p->pVarLevels  = pVarLevels;
     p->nSizeNonDec = 0;
     if ( (pTruth[0] & 1) == 0 && Abc_TtIsConst0(pTruth, Abc_TtWordNum(nVarsInit)) )
         { if ( pRes ) pRes[0] = '0', pRes[1] = 0; }
diff --git a/src/opt/dau/dauGia.c b/src/opt/dau/dauGia.c
index cf644102..1d821a30 100644
--- a/src/opt/dau/dauGia.c
+++ b/src/opt/dau/dauGia.c
@@ -414,14 +414,23 @@ int Dau_DsdToGia( Gia_Man_t * pGia, char * p, int * pLits, Vec_Int_t * vCover )
 ***********************************************************************/
 int Dsm_ManTruthToGia( void * p, word * pTruth, Vec_Int_t * vLeaves, Vec_Int_t * vCover )
 {
+    int fUseMuxes = 0;
     int fDelayBalance = 1;
     Gia_Man_t * pGia = (Gia_Man_t *)p;
-    char pDsd[1000];
     int nSizeNonDec;
+    char pDsd[1000];
     m_Calls++;
     assert( Vec_IntSize(vLeaves) <= DAU_DSD_MAX_VAR );
-//    static int Counter = 0; Counter++;
-    nSizeNonDec = Dau_DsdDecompose( pTruth, Vec_IntSize(vLeaves), 0, 1, pDsd );
+    // collect delay information
+    if ( fDelayBalance && fUseMuxes )
+    {
+        int i, iLit, pVarLevels[DAU_DSD_MAX_VAR];
+        Vec_IntForEachEntry( vLeaves, iLit, i )
+            pVarLevels[i] = Gia_ObjLevelId( pGia, Abc_Lit2Var(iLit) );
+        nSizeNonDec = Dau_DsdDecomposeLevel( pTruth, Vec_IntSize(vLeaves), fUseMuxes, 1, pDsd, pVarLevels );
+    }
+    else
+        nSizeNonDec = Dau_DsdDecompose( pTruth, Vec_IntSize(vLeaves), fUseMuxes, 1, pDsd );
     if ( nSizeNonDec )
         m_NonDsd++;
 //    printf( "%s\n", pDsd );
@@ -505,6 +514,15 @@ void * Dsm_ManDeriveGia( void * pGia, int fUseMuxes )
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     Vec_IntFree( vLeaves );
     Vec_IntFree( vCover );
+/*
+    Gia_ManForEachAnd( pNew, pObj, i )
+    {
+        int iLev  = Gia_ObjLevelId(pNew, i);
+        int iLev0 = Gia_ObjLevelId(pNew, Gia_ObjFaninId0(pObj, i));
+        int iLev1 = Gia_ObjLevelId(pNew, Gia_ObjFaninId1(pObj, i));
+        assert( iLev == 1 + Abc_MaxInt(iLev0, iLev1) );
+    }
+*/
     // perform cleanup
     pNew = Gia_ManCleanup( pTemp = pNew );
     Gia_ManStop( pTemp );