Version abc80411

22 files changed, 899 insertions, 386 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 88d7aa50..9d6bde98 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -548,6 +548,7 @@ extern void            Aig_ManReprStop( Aig_Man_t * p );
 extern void            Aig_ObjCreateRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
 extern void            Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupRepr( Aig_Man_t * p, int fOrdered );
+extern int             Aig_ManCountReprs( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManRehash( Aig_Man_t * p );
 extern int             Aig_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pNew, Aig_Obj_t * pOld );
 extern void            Aig_ManMarkValidChoices( Aig_Man_t * p );
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index 94a1c844..88cdbf17 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -329,6 +329,28 @@ int Aig_ManRemapRepr( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Transfer representatives and return the number of critical fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManCountReprs( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i, Counter = 0;
+    if ( p->pReprs == NULL )
+        return 0;
+    Aig_ManForEachObj( p, pObj, i )
+        Counter += (p->pReprs[i] != NULL);
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if pOld is in the TFI of pNew.]
 
   Description []
diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h
index d7f525a2..12374a49 100644
--- a/src/aig/hop/hop.h
+++ b/src/aig/hop/hop.h
@@ -166,11 +166,11 @@ static inline int          Hop_ObjIsMarkA( Hop_Obj_t * pObj )     { return pObj-
 static inline void         Hop_ObjSetMarkA( Hop_Obj_t * pObj )    { pObj->fMarkA = 1;     }
 static inline void         Hop_ObjClearMarkA( Hop_Obj_t * pObj )  { pObj->fMarkA = 0;     }
  
-static inline void         Hop_ObjSetTravId( Hop_Obj_t * pObj, int TravId )                { pObj->pData = (void *)TravId;                       }
-static inline void         Hop_ObjSetTravIdCurrent( Hop_Man_t * p, Hop_Obj_t * pObj )      { pObj->pData = (void *)p->nTravIds;                  }
-static inline void         Hop_ObjSetTravIdPrevious( Hop_Man_t * p, Hop_Obj_t * pObj )     { pObj->pData = (void *)(p->nTravIds - 1);            }
-static inline int          Hop_ObjIsTravIdCurrent( Hop_Man_t * p, Hop_Obj_t * pObj )       { return (int )((int)pObj->pData == p->nTravIds);     }
-static inline int          Hop_ObjIsTravIdPrevious( Hop_Man_t * p, Hop_Obj_t * pObj )      { return (int )((int)pObj->pData == p->nTravIds - 1); }
+static inline void         Hop_ObjSetTravId( Hop_Obj_t * pObj, int TravId )                { pObj->pData = (void *)(long)TravId;                      }
+static inline void         Hop_ObjSetTravIdCurrent( Hop_Man_t * p, Hop_Obj_t * pObj )      { pObj->pData = (void *)(long)p->nTravIds;                 }
+static inline void         Hop_ObjSetTravIdPrevious( Hop_Man_t * p, Hop_Obj_t * pObj )     { pObj->pData = (void *)(long)(p->nTravIds - 1);           }
+static inline int          Hop_ObjIsTravIdCurrent( Hop_Man_t * p, Hop_Obj_t * pObj )       { return (int)((int)(long)pObj->pData == p->nTravIds);     }
+static inline int          Hop_ObjIsTravIdPrevious( Hop_Man_t * p, Hop_Obj_t * pObj )      { return (int)((int)(long)pObj->pData == p->nTravIds - 1); }
 
 static inline int          Hop_ObjTravId( Hop_Obj_t * pObj )      { return (int)pObj->pData;                       }
 static inline int          Hop_ObjPhase( Hop_Obj_t * pObj )       { return pObj->fPhase;                           }
diff --git a/src/aig/mfx/mfxCore.c b/src/aig/mfx/mfxCore.c
index bea7c6b0..8867f7c1 100644
--- a/src/aig/mfx/mfxCore.c
+++ b/src/aig/mfx/mfxCore.c
@@ -206,6 +206,7 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib )
     int nTotalNodesBeg = Nwk_ManNodeNum(pNtk);
     int nTotalEdgesBeg = Nwk_ManGetTotalFanins(pNtk);
 
+//    assert( Nwk_ManCheck( pNtk ) );
     // check limits on the number of fanins
     nFaninMax = Nwk_ManGetFaninMax(pNtk);
     if ( pPars->fResub )
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 9c3666ab..b3d099c9 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -364,7 +364,7 @@ Aig_Obj_t * Ntl_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph )
 Aig_Obj_t * Ntl_ManBuildNodeAig( Ntl_Obj_t * pNode )
 {
     Aig_Man_t * pMan = pNode->pModel->pMan->pAig;
-    int fUseFactor = 0;
+    int fUseFactor = 1;
     // consider the constant node
     if ( Ntl_SopGetVarNum(pNode->pSop) == 0 )
         return Aig_NotCond( Aig_ManConst1(pMan), Ntl_SopIsConst0(pNode->pSop) );
@@ -957,8 +957,8 @@ Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
 ***********************************************************************/
 static inline void Ntl_NetIncrementRefs( Ntl_Net_t * pNet )
 {
-    int nRefs = (int)pNet->pCopy;
-    pNet->pCopy = (void *)(nRefs + 1);
+    int nRefs = (int)(long)pNet->pCopy;
+    pNet->pCopy = (void *)(long)(nRefs + 1);
 }
 
 /**Function*************************************************************
@@ -981,7 +981,7 @@ Nwk_Obj_t * Ntl_ManExtractNwk_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, Nwk_Man_t *
     if ( pNet->fMark )
         return pNet->pCopy;
     pNet->fMark = 1;
-    pNode = Nwk_ManCreateNode( pNtk, Ntl_ObjFaninNum(pNet->pDriver), (int)pNet->pCopy );
+    pNode = Nwk_ManCreateNode( pNtk, Ntl_ObjFaninNum(pNet->pDriver), (int)(long)pNet->pCopy );
     Ntl_ObjForEachFanin( pNet->pDriver, pFaninNet, i )
     {
         Ntl_ManExtractNwk_rec( p, pFaninNet, pNtk, vCover, vMemory );
@@ -1046,7 +1046,7 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig )
             pObj = Ntl_ModelPi( pRoot, Aig_ObjPioNum(pAnd) );
             pNet = Ntl_ObjFanout0(pObj);
             pNet->fMark = 1;
-            pNet->pCopy = Nwk_ManCreateCi( pNtk, (int)pNet->pCopy ); 
+            pNet->pCopy = Nwk_ManCreateCi( pNtk, (int)(long)pNet->pCopy ); 
         }
         else if ( Aig_ObjIsPo(pAnd) )
         {
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 8a172e6c..98f14d3d 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -192,6 +192,8 @@ Aig_Man_t * Ntl_ManScl( Ntl_Man_t * p, Aig_Man_t * pAig, int fLatchConst, int fL
 
     // derive the new AIG
     pTemp = Aig_ManDupRepresDfs( pAig );
+printf( "Intermediate:\n" );
+Aig_ManPrintStats( pTemp );
     // duplicate the timing manager
     if ( pAig->pManTime )
         pTemp->pManTime = Tim_ManDup( pAig->pManTime, 0 );
@@ -230,17 +232,21 @@ Aig_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, Aig_Man_t * pAig, int nConfMax, int fVe
     // perform fraiging for the given design
     pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
     pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL );
+//printf( "Reprs = %d.\n", Aig_ManCountReprs(pAigCol) );
     Aig_ManStop( pTemp );
 
     // transfer equivalence classes to the original AIG
     pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol );
     pAig->nReprsAlloc = Aig_ManObjNumMax(pAig);
+//printf( "Reprs = %d.\n", Aig_ManCountReprs(pAig) );
     // cleanup
     Aig_ManStop( pAigCol );
     Ntl_ManFree( pNew );
 
     // derive the new AIG
     pTemp = Aig_ManDupRepresDfs( pAig );
+//printf( "Intermediate LCORR:\n" );
+//Aig_ManPrintStats( pTemp );
     // duplicate the timing manager
     if ( pAig->pManTime )
         pTemp->pManTime = Tim_ManDup( pAig->pManTime, 0 );
diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c
index fddd4167..cefa38d3 100644
--- a/src/aig/ntl/ntlWriteBlif.c
+++ b/src/aig/ntl/ntlWriteBlif.c
@@ -45,7 +45,7 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet;
     float Delay;
-    int i, k;
+    int i, k, fClockAdded = 0;
     fprintf( pFile, ".model %s\n", pModel->pName );
     fprintf( pFile, ".inputs" );
     Ntl_ModelForEachPi( pModel, pObj, i )
@@ -117,8 +117,10 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
             fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName );
             if ( pObj->LatchId >> 2 )
                 fprintf( pFile, " %d", pObj->LatchId >> 2 );
-            if ( pObj->pFanio[1] != NULL )
+            if ( Ntl_ObjFanin(pObj, 1) != NULL )
                 fprintf( pFile, " %s", Ntl_ObjFanin(pObj, 1)->pName );
+            else if ( pObj->LatchId >> 2 )
+                fprintf( pFile, " clock" ), fClockAdded = 1;
             fprintf( pFile, " %d", pObj->LatchId & 3 );
             fprintf( pFile, "\n" );
         }
@@ -132,6 +134,8 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
             fprintf( pFile, "\n" );
         }
     }
+    if ( fClockAdded )
+        fprintf( pFile, ".names clock\n 0\n" );
     fprintf( pFile, ".end\n\n" );
 }
 
diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h
index 4c99c3a9..6fc84893 100644
--- a/src/aig/nwk/nwk.h
+++ b/src/aig/nwk/nwk.h
@@ -195,6 +195,8 @@ static inline int         Nwk_ManTimeMore( float f1, float f2, float Eps )   { r
 /*=== nwkBidec.c ==========================================================*/
 extern void            Nwk_ManBidecResyn( Nwk_Man_t * pNtk, int fVerbose );
 extern Hop_Obj_t *     Nwk_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare );
+/*=== nwkCheck.c ==========================================================*/
+extern int             Nwk_ManCheck( Nwk_Man_t * p );
 /*=== nwkDfs.c ==========================================================*/
 extern int             Nwk_ManVerifyTopoOrder( Nwk_Man_t * pNtk );
 extern int             Nwk_ManLevelBackup( Nwk_Man_t * pNtk );
@@ -253,6 +255,7 @@ extern int             Nwk_NodeCompareLevelsIncrease( Nwk_Obj_t ** pp1, Nwk_Obj_
 extern int             Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 );
 extern void            Nwk_ObjPrint( Nwk_Obj_t * pObj );
 extern void            Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vCiNames, Vec_Ptr_t * vCoNames );
+extern void            Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/nwk/nwkCheck.c b/src/aig/nwk/nwkCheck.c
index 5c547dbe..6922e439 100644
--- a/src/aig/nwk/nwkCheck.c
+++ b/src/aig/nwk/nwkCheck.c
@@ -30,7 +30,7 @@
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Checking the logic network for consistency.]
 
   Description []
                
@@ -39,6 +39,32 @@
   SeeAlso     []
 
 ***********************************************************************/
+int Nwk_ManCheck( Nwk_Man_t * p )
+{
+    Nwk_Obj_t * pObj;
+    int i, k, m;
+    // check if the nodes have duplicated fanins
+    Nwk_ManForEachNode( p, pObj, i )
+    {
+        for ( k = 0; k < pObj->nFanins; k++ )
+            for ( m = k + 1; m < pObj->nFanins; m++ )
+                if ( pObj->pFanio[k] == pObj->pFanio[m] )
+                    printf( "Node %d has duplicated fanin %d.\n", pObj->Id, pObj->pFanio[k]->Id );
+    }
+/*
+    // check if all nodes are in the correct fanin/fanout relationship
+    Nwk_ManForEachObj( p, pObj, i )
+    {
+        Nwk_ObjForEachFanin( pObj, pNext, k )
+            if ( Nwk_ObjFindFanout( pNext, pObj ) == -1 )
+                printf( "Nwk_ManCheck(): Object %d has fanin %d which does not have a corresponding fanout.\n", pObj->Id, pNext->Id );
+        Nwk_ObjForEachFanout( pObj, pNext, k )
+            if ( Nwk_ObjFindFanin( pNext, pObj ) == -1 )
+                printf( "Nwk_ManCheck(): Object %d has fanout %d which does not have a corresponding fanin.\n", pObj->Id, pNext->Id );
+    }
+*/
+    return 1;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/nwk/nwkFanio.c b/src/aig/nwk/nwkFanio.c
index f338d07d..1b701e9e 100644
--- a/src/aig/nwk/nwkFanio.c
+++ b/src/aig/nwk/nwkFanio.c
@@ -221,7 +221,7 @@ void Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin )
         Nwk_ManReallocNode( pObj );
     if ( Nwk_ObjReallocIsNeeded(pFanin) )
         Nwk_ManReallocNode( pFanin );
-    for ( i = pObj->nFanins + pObj->nFanouts; i > (int)pObj->nFanins; i-- )
+    for ( i = pObj->nFanins + pObj->nFanouts; i > pObj->nFanins; i-- )
         pObj->pFanio[i] = pObj->pFanio[i-1];
     pObj->pFanio[pObj->nFanins++] = pFanin;
     pFanin->pFanio[pFanin->nFanins + pFanin->nFanouts++] = pObj;
@@ -247,15 +247,15 @@ void Nwk_ObjDeleteFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin )
     for ( k = i = 0; i < Limit; i++ )
         if ( pObj->pFanio[i] != pFanin )
             pObj->pFanio[k++] = pObj->pFanio[i];
-    assert( i == k + 1 );
+    assert( i == k + 1 ); // if it fails, likely because of duplicated fanin
     pObj->nFanins--;
     // remove pObj from the fanout list of pFanin
     Limit = pFanin->nFanins + pFanin->nFanouts;
     for ( k = i = pFanin->nFanins; i < Limit; i++ )
         if ( pFanin->pFanio[i] != pObj )
             pFanin->pFanio[k++] = pFanin->pFanio[i];
-    assert( i == k + 1 );
-    pFanin->nFanouts--;
+    assert( i == k + 1 ); // if it fails, likely because of duplicated fanout
+    pFanin->nFanouts--; 
 }
 
 /**Function*************************************************************
diff --git a/src/aig/nwk/nwkMap.c b/src/aig/nwk/nwkMap.c
index 6c1e1330..f5b2b7f8 100644
--- a/src/aig/nwk/nwkMap.c
+++ b/src/aig/nwk/nwkMap.c
@@ -56,7 +56,7 @@ void Nwk_ManSetIfParsDefault( If_Par_t * pPars )
     pPars->fPreprocess =  1;
     pPars->fArea       =  0;
     pPars->fFancy      =  0;
-    pPars->fExpRed     =  0;
+    pPars->fExpRed     =  1; ////
     pPars->fLatchPaths =  0;
     pPars->fEdge       =  1;
     pPars->fCutMin     =  0;
@@ -244,16 +244,25 @@ Hop_Obj_t * Nwk_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t *
 ***********************************************************************/
 Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToIf )
 {
+    Vec_Ptr_t * vIfToAig;
     Nwk_Man_t * pNtk;
     Nwk_Obj_t * pObjNew;
-    Aig_Obj_t * pObj;
+    Aig_Obj_t * pObj, * pObjRepr;
     If_Obj_t * pIfObj;
     If_Cut_t * pCutBest;
     int i, k, nLeaves, * ppLeaves;
     assert( Aig_ManPiNum(p) == If_ManCiNum(pIfMan) );
     assert( Aig_ManPoNum(p) == If_ManCoNum(pIfMan) );
     assert( Aig_ManNodeNum(p) == If_ManAndNum(pIfMan) );
+    Aig_ManCleanData( p );
     If_ManCleanCutData( pIfMan );
+    // create mapping of IF to AIG
+    vIfToAig = Vec_PtrStart( If_ManObjNum(pIfMan) );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        pIfObj = Vec_PtrEntry( vAigToIf, i );
+        Vec_PtrWriteEntry( vIfToAig, pIfObj->Id, pObj );
+    }
     // construct the network
     pNtk = Nwk_ManAlloc();
     pNtk->pName = Aig_UtilStrsav( p->pName );
@@ -271,7 +280,10 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToI
             // create node
             pObjNew = Nwk_ManCreateNode( pNtk, nLeaves, pIfObj->nRefs );
             for ( k = 0; k < nLeaves; k++ )
-                Nwk_ObjAddFanin( pObjNew, Aig_ManObj(p, ppLeaves[k])->pData );
+            {
+                pObjRepr = Vec_PtrEntry( vIfToAig, ppLeaves[k] );
+                Nwk_ObjAddFanin( pObjNew, pObjRepr->pData );
+            }
             // get the functionality
             pObjNew->pFunc = Nwk_NodeIfToHop( pNtk->pManHop, pIfMan, pIfObj );
         }
@@ -292,7 +304,9 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToI
             assert( 0 );
         pObj->pData = pObjNew;
     }
+    Vec_PtrFree( vIfToAig );
     pNtk->pManTime = Tim_ManDup( pIfMan->pManTim, 0 );
+    assert( Nwk_ManCheck( pNtk ) );
     return pNtk;
 }
 
@@ -328,6 +342,8 @@ Nwk_Man_t * Nwk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars
     }
     // transform the result of mapping into the new network
     pNtk = Nwk_ManFromIf( pIfMan, p, vAigToIf );
+    if ( pPars->fBidec && pPars->nLutSize <= 8 )
+        Nwk_ManBidecResyn( pNtk, 0 );
     If_ManStop( pIfMan );
     Vec_PtrFree( vAigToIf );
     return pNtk;
diff --git a/src/aig/nwk/nwkObj.c b/src/aig/nwk/nwkObj.c
index 6d1f0428..58587f07 100644
--- a/src/aig/nwk/nwkObj.c
+++ b/src/aig/nwk/nwkObj.c
@@ -154,10 +154,8 @@ void Nwk_ManDeleteNode( Nwk_Obj_t * pObj )
     Vec_Ptr_t * vNodes = pObj->pMan->vTemp;
     Nwk_Obj_t * pTemp;
     int i;
-    // delete fanins and fanouts
-    Nwk_ObjCollectFanouts( pObj, vNodes );
-    Vec_PtrForEachEntry( vNodes, pTemp, i )
-        Nwk_ObjDeleteFanin( pTemp, pObj );
+    assert( Nwk_ObjFanoutNum(pObj) == 0 );
+    // delete fanins
     Nwk_ObjCollectFanins( pObj, vNodes );
     Vec_PtrForEachEntry( vNodes, pTemp, i )
         Nwk_ObjDeleteFanin( pObj, pTemp );
diff --git a/src/aig/nwk/nwkTiming.c b/src/aig/nwk/nwkTiming.c
index c27f9d61..9ab24467 100644
--- a/src/aig/nwk/nwkTiming.c
+++ b/src/aig/nwk/nwkTiming.c
@@ -427,6 +427,8 @@ int Nwk_ManVerifyTiming(  Nwk_Man_t * pNtk )
     int i;
     Nwk_ManForEachObj( pNtk, pObj, i )
     {
+        if ( Nwk_ObjIsPi(pObj) && Nwk_ObjFanoutNum(pObj) == 0 )
+            continue;
         tArrival = Nwk_NodeComputeArrival( pObj, 1 );
         tRequired = Nwk_NodeComputeRequired( pObj, 1 );
         if ( !Nwk_ManTimeEqual( tArrival, Nwk_ObjArrival(pObj), (float)0.01 ) )
diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c
index 5fb594ec..97c95d27 100644
--- a/src/aig/nwk/nwkUtil.c
+++ b/src/aig/nwk/nwkUtil.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "nwk.h"
+#include "math.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -254,6 +255,114 @@ void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vCiNames,
     printf( "Dumping logic network is currently not supported.\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prints the distribution of fanins/fanouts in the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk )
+{
+    char Buffer[100];
+    Nwk_Obj_t * pNode;
+    Vec_Int_t * vFanins, * vFanouts;
+    int nFanins, nFanouts, nFaninsMax, nFanoutsMax, nFaninsAll, nFanoutsAll;
+    int i, k, nSizeMax;
+
+    // determine the largest fanin and fanout
+    nFaninsMax = nFanoutsMax = 0;
+    nFaninsAll = nFanoutsAll = 0;
+    Nwk_ManForEachNode( pNtk, pNode, i )
+    {
+        nFanins  = Nwk_ObjFaninNum(pNode);
+        nFanouts = Nwk_ObjFanoutNum(pNode);
+        nFaninsAll  += nFanins;
+        nFanoutsAll += nFanouts;
+        nFaninsMax   = AIG_MAX( nFaninsMax, nFanins );
+        nFanoutsMax  = AIG_MAX( nFanoutsMax, nFanouts );
+    }
+
+    // allocate storage for fanin/fanout numbers
+    nSizeMax = AIG_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) );
+    vFanins  = Vec_IntStart( nSizeMax );
+    vFanouts = Vec_IntStart( nSizeMax );
+
+    // count the number of fanins and fanouts
+    Nwk_ManForEachNode( pNtk, pNode, i )
+    {
+        nFanins  = Nwk_ObjFaninNum(pNode);
+        nFanouts = Nwk_ObjFanoutNum(pNode);
+//        nFanouts = Nwk_NodeMffcSize(pNode);
+
+        if ( nFanins < 10 )
+            Vec_IntAddToEntry( vFanins, nFanins, 1 );
+        else if ( nFanins < 100 )
+            Vec_IntAddToEntry( vFanins, 10 + nFanins/10, 1 );
+        else if ( nFanins < 1000 )
+            Vec_IntAddToEntry( vFanins, 20 + nFanins/100, 1 );
+        else if ( nFanins < 10000 )
+            Vec_IntAddToEntry( vFanins, 30 + nFanins/1000, 1 );
+        else if ( nFanins < 100000 )
+            Vec_IntAddToEntry( vFanins, 40 + nFanins/10000, 1 );
+        else if ( nFanins < 1000000 )
+            Vec_IntAddToEntry( vFanins, 50 + nFanins/100000, 1 );
+        else if ( nFanins < 10000000 )
+            Vec_IntAddToEntry( vFanins, 60 + nFanins/1000000, 1 );
+
+        if ( nFanouts < 10 )
+            Vec_IntAddToEntry( vFanouts, nFanouts, 1 );
+        else if ( nFanouts < 100 )
+            Vec_IntAddToEntry( vFanouts, 10 + nFanouts/10, 1 );
+        else if ( nFanouts < 1000 )
+            Vec_IntAddToEntry( vFanouts, 20 + nFanouts/100, 1 );
+        else if ( nFanouts < 10000 )
+            Vec_IntAddToEntry( vFanouts, 30 + nFanouts/1000, 1 );
+        else if ( nFanouts < 100000 )
+            Vec_IntAddToEntry( vFanouts, 40 + nFanouts/10000, 1 );
+        else if ( nFanouts < 1000000 )
+            Vec_IntAddToEntry( vFanouts, 50 + nFanouts/100000, 1 );
+        else if ( nFanouts < 10000000 )
+            Vec_IntAddToEntry( vFanouts, 60 + nFanouts/1000000, 1 );
+    }
+
+    printf( "The distribution of fanins and fanouts in the network:\n" );
+    printf( "         Number   Nodes with fanin  Nodes with fanout\n" );
+    for ( k = 0; k < nSizeMax; k++ )
+    {
+        if ( vFanins->pArray[k] == 0 && vFanouts->pArray[k] == 0 )
+            continue;
+        if ( k < 10 )
+            printf( "%15d : ", k );
+        else
+        {
+            sprintf( Buffer, "%d - %d", (int)pow(10, k/10) * (k%10), (int)pow(10, k/10) * (k%10+1) - 1 ); 
+            printf( "%15s : ", Buffer );
+        }
+        if ( vFanins->pArray[k] == 0 )
+            printf( "              " );
+        else
+            printf( "%12d  ", vFanins->pArray[k] );
+        printf( "    " );
+        if ( vFanouts->pArray[k] == 0 )
+            printf( "              " );
+        else
+            printf( "%12d  ", vFanouts->pArray[k] );
+        printf( "\n" );
+    }
+    Vec_IntFree( vFanins );
+    Vec_IntFree( vFanouts );
+
+    printf( "Fanins: Max = %d. Ave = %.2f.  Fanouts: Max = %d. Ave =  %.2f.\n", 
+        nFaninsMax,  1.0*nFaninsAll/Nwk_ManNodeNum(pNtk), 
+        nFanoutsMax, 1.0*nFanoutsAll/Nwk_ManNodeNum(pNtk)  );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e8ad6610..53b25b63 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -201,28 +201,33 @@ static int Abc_CommandEnlarge        ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandTraceStart     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTraceCheck     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
+
 static int Abc_CommandAbc8Read       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8ReadLogic  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Write      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8WriteLogic ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8ReadLut    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8PrintLut   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
 static int Abc_CommandAbc8Ps         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8Pfan       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8If         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8DChoice    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8DC2        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Bidec      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Strash     ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8ReadLut    ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8PrintLut   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Mfs        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Lutpack    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Balance    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Speedup    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
 static int Abc_CommandAbc8Fraig      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Sweep      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Cec        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Scl        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Lcorr      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Ssw        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8Sweep      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandAbc8Cec        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8DSec       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 
@@ -440,28 +445,33 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "indcut",        Abc_CommandIndcut,           0 );
     Cmd_CommandAdd( pAbc, "Verification", "enlarge",       Abc_CommandEnlarge,          1 );
 
+
     Cmd_CommandAdd( pAbc, "ABC8",         "*r",            Abc_CommandAbc8Read,         0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*rlogic",       Abc_CommandAbc8ReadLogic,    0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*w",            Abc_CommandAbc8Write,        0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*wlogic",       Abc_CommandAbc8WriteLogic,   0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*rlut",         Abc_CommandAbc8ReadLut,      0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*plut",         Abc_CommandAbc8PrintLut,     0 );
+
     Cmd_CommandAdd( pAbc, "ABC8",         "*ps",           Abc_CommandAbc8Ps,           0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*pfan",         Abc_CommandAbc8Pfan,         0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*if",           Abc_CommandAbc8If,           0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*dchoice",      Abc_CommandAbc8DChoice,      0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*dc2",          Abc_CommandAbc8DC2,          0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*bidec",        Abc_CommandAbc8Bidec,        0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*st",           Abc_CommandAbc8Strash,       0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*rlut",         Abc_CommandAbc8ReadLut,      0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*plut",         Abc_CommandAbc8PrintLut,     0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*mfs",          Abc_CommandAbc8Mfs,          0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*lp",           Abc_CommandAbc8Lutpack,      0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*b",            Abc_CommandAbc8Balance,      0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*speedup",      Abc_CommandAbc8Speedup,      0 );
+
     Cmd_CommandAdd( pAbc, "ABC8",         "*fraig",        Abc_CommandAbc8Fraig,        0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*sw",           Abc_CommandAbc8Sweep,        0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*cec",          Abc_CommandAbc8Cec,          0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*scl",          Abc_CommandAbc8Scl,          0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*lcorr",        Abc_CommandAbc8Lcorr,        0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*ssw",          Abc_CommandAbc8Ssw,          0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*sw",           Abc_CommandAbc8Sweep,        0 );
+
+    Cmd_CommandAdd( pAbc, "ABC8",         "*cec",          Abc_CommandAbc8Cec,          0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*dsec",         Abc_CommandAbc8DSec,         0 );
  
 
@@ -3668,7 +3678,7 @@ int Abc_CommandSpeedup( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     fUseLutLib = 0;
-    Percentage = 3;
+    Percentage = 5;
     Degree     = 2;
     fVerbose   = 0;
     fVeryVerbose = 0;
@@ -15027,6 +15037,140 @@ usage:
 
 /**Function*************************************************************
 
+  Synopsis    [Command procedure to read LUT libraries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc8ReadLut( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    FILE * pFile;
+    char * FileName;
+    void * pLib;
+    int c;
+    extern If_Lib_t * If_LutLibRead( char * FileName );
+    extern void If_LutLibFree( If_Lib_t * pLutLib );
+
+    // set the defaults
+    Extra_UtilGetoptReset();
+    while ( (c = Extra_UtilGetopt(argc, argv, "h")) != EOF ) 
+    {
+        switch (c) 
+        {
+            case 'h':
+                goto usage;
+                break;
+            default:
+                goto usage;
+        }
+    }
+
+
+    if ( argc != globalUtilOptind + 1 )
+    {
+        goto usage;
+    }
+
+    // get the input file name
+    FileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( FileName, "r" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open input file \"%s\". ", FileName );
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".lut", NULL, NULL, NULL, NULL ) )
+            fprintf( stdout, "Did you mean \"%s\"?", FileName );
+        fprintf( stdout, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+
+    // set the new network
+    pLib = If_LutLibRead( FileName );
+    if ( pLib == NULL )
+    {
+        fprintf( stdout, "Reading LUT library has failed.\n" );
+        goto usage;
+    }
+    // replace the current library
+    if ( pAbc->pAbc8Lib != NULL )
+        If_LutLibFree( pAbc->pAbc8Lib );
+    pAbc->pAbc8Lib = pLib;
+    return 0;
+
+usage:
+    fprintf( stdout, "\nusage: *rlut [-h]\n");
+    fprintf( stdout, "\t          read the LUT library from the file\n" );  
+    fprintf( stdout, "\t-h      : print the command usage\n");
+    fprintf( stdout, "\t                                        \n");
+    fprintf( stdout, "\t          File format for a LUT library:\n");
+    fprintf( stdout, "\t          (the default library is shown)\n");
+    fprintf( stdout, "\t                                        \n");
+    fprintf( stdout, "\t          # The area/delay of k-variable LUTs:\n");
+    fprintf( stdout, "\t          # k  area   delay\n");
+    fprintf( stdout, "\t          1      1      1\n");
+    fprintf( stdout, "\t          2      2      2\n");
+    fprintf( stdout, "\t          3      4      3\n");
+    fprintf( stdout, "\t          4      8      4\n");
+    fprintf( stdout, "\t          5     16      5\n");
+    fprintf( stdout, "\t          6     32      6\n");
+    return 1;       /* error exit */
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Command procedure to read LUT libraries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc8PrintLut( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    int c;
+    extern void If_LutLibPrint( If_Lib_t * pLutLib );
+
+    // set the defaults
+    Extra_UtilGetoptReset();
+    while ( (c = Extra_UtilGetopt(argc, argv, "h")) != EOF ) 
+    {
+        switch (c) 
+        {
+            case 'h':
+                goto usage;
+                break;
+            default:
+                goto usage;
+        }
+    }
+
+    if ( argc != globalUtilOptind )
+    {
+        goto usage;
+    }
+
+    // set the new network
+    if ( pAbc->pAbc8Lib == NULL )
+        printf( "LUT library is not specified.\n" );
+    else
+        If_LutLibPrint( pAbc->pAbc8Lib );
+    return 0;
+
+usage:
+    fprintf( stdout, "\nusage: *plut [-h]\n");
+    fprintf( stdout, "\t          print the current LUT library\n" );  
+    fprintf( stdout, "\t-h      : print the command usage\n");
+    return 1;       /* error exit */
+}
+
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -15096,8 +15240,53 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc8Pfan( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c;
+    extern void Nwk_ManPrintFanioNew( void * p );
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAbc8Nwk == NULL )
+    {
+        printf( "Abc_CommandAbc8Pfan(): There is no mapped network for print fanin/fanout.\n" );
+        return 1;
+    }
+    Nwk_ManPrintFanioNew( pAbc->pAbc8Nwk );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: *pfan [-h]\n" );
+    fprintf( stdout, "\t        prints fanin/fanout stats of the mapped network\n" );
+    fprintf( stdout, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    char Buffer[200];
+    char LutSize[200];
     If_Par_t Pars, * pPars = &Pars;
     void * pNtkNew;
     int c;
@@ -15109,7 +15298,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( pAbc->pAbc8Lib == NULL )
     {
-        printf( "LUT library is not given. Using defaul 6-LUT library.\n" );
+        printf( "LUT library is not given. Using default 6-LUT library.\n" );
         pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 );
     }
 
@@ -15117,12 +15306,111 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
     Nwk_ManSetIfParsDefault( pPars );
     pPars->pLutLib = pAbc->pAbc8Lib;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEpaflemrstbvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-K\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            pPars->nLutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nLutSize < 0 ) 
+                goto usage;
+            // if the LUT size is specified, disable library
+            pPars->pLutLib = NULL; 
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-C\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            pPars->nCutsMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nCutsMax < 0 ) 
+                goto usage;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-F\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            pPars->nFlowIters = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFlowIters < 0 ) 
+                goto usage;
+            break;
+        case 'A':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-A\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            pPars->nAreaIters = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nAreaIters < 0 ) 
+                goto usage;
+            break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-D\" should be followed by a floating point number.\n" );
+                goto usage;
+            }
+            pPars->DelayTarget = (float)atof(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->DelayTarget <= 0.0 ) 
+                goto usage;
+        case 'E':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-E\" should be followed by a floating point number.\n" );
+                goto usage;
+            }
+            pPars->Epsilon = (float)atof(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->Epsilon < 0.0 || pPars->Epsilon > 1.0 ) 
+                goto usage;
+            break;
+        case 'p':
+            pPars->fPreprocess ^= 1;
+            break;
+        case 'a':
+            pPars->fArea ^= 1;
+            break;
+        case 'r':
+            pPars->fExpRed ^= 1;
+            break;
+        case 'f':
+            pPars->fFancy ^= 1;
+            break;
+        case 'l':
+            pPars->fLatchPaths ^= 1;
+            break;
+        case 'e':
+            pPars->fEdge ^= 1;
+            break;
+        case 'm':
+            pPars->fCutMin ^= 1;
+            break;
+        case 's':
+            pPars->fSeqMap ^= 1;
+            break;
+        case 't':
+            pPars->fLiftLeaves ^= 1;
+            break;
+        case 'b':
+            pPars->fBidec ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
         case 'h':
-            goto usage;
         default:
             goto usage;
         }
@@ -15133,6 +15421,38 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
+    if ( pPars->nLutSize < 3 || pPars->nLutSize > IF_MAX_LUTSIZE )
+    {
+        fprintf( stdout, "Incorrect LUT size (%d).\n", pPars->nLutSize );
+        return 1;
+    }
+
+    if ( pPars->nCutsMax < 1 || pPars->nCutsMax >= (1<<12) )
+    {
+        fprintf( stdout, "Incorrect number of cuts.\n" );
+        return 1;
+    }
+
+    // enable truth table computation if choices are selected
+    if ( (c = Aig_ManCountChoices( pAbc->pAbc8Aig )) )
+    {
+        printf( "Performing LUT mapping with %d choices.\n", c );
+        pPars->fExpRed = 0;
+    }
+    // enable truth table computation if cut minimization is selected
+    if ( pPars->fCutMin )
+    {
+        pPars->fTruth = 1;
+        pPars->fExpRed = 0;
+    }
+
+    // complain if truth tables are requested but the cut size is too large
+    if ( pPars->fTruth && pPars->nLutSize > IF_MAX_FUNC_LUTSIZE )
+    {
+        fprintf( stdout, "Truth tables cannot be computed for LUT larger than %d inputs.\n", IF_MAX_FUNC_LUTSIZE );
+        return 1;
+    }
+
     pNtkNew = Nwk_MappingIf( pAbc->pAbc8Aig, Ntl_ManReadTimeMan(pAbc->pAbc8Ntl), pPars );
     if ( pNtkNew == NULL )
     {
@@ -15145,9 +15465,34 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( stdout, "usage: *if [-h]\n" );
-    fprintf( stdout, "\t        performs mapping for logic extraced from the design\n" );
-    fprintf( stdout, "\t-h    : print the command usage\n");
+    if ( pPars->DelayTarget == -1 ) 
+        sprintf( Buffer, "best possible" );
+    else
+        sprintf( Buffer, "%.2f", pPars->DelayTarget );
+    if ( pPars->nLutSize == -1 ) 
+        sprintf( LutSize, "library" );
+    else
+        sprintf( LutSize, "%d", pPars->nLutSize );
+    fprintf( stdout, "usage: *if [-KCFA num] [-DE float] [-parlembvh]\n" );
+    fprintf( stdout, "\t           performs FPGA technology mapping of the network\n" );
+    fprintf( stdout, "\t-K num   : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
+    fprintf( stdout, "\t-C num   : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
+    fprintf( stdout, "\t-F num   : the number of area flow recovery iterations (num >= 0) [default = %d]\n", pPars->nFlowIters );
+    fprintf( stdout, "\t-A num   : the number of exact area recovery iterations (num >= 0) [default = %d]\n", pPars->nAreaIters );
+    fprintf( stdout, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer );  
+    fprintf( stdout, "\t-E float : sets epsilon used for tie-breaking [default = %f]\n", pPars->Epsilon );  
+    fprintf( stdout, "\t-p       : toggles preprocessing using several starting points [default = %s]\n", pPars->fPreprocess? "yes": "no" );
+    fprintf( stdout, "\t-a       : toggles area-oriented mapping [default = %s]\n", pPars->fArea? "yes": "no" );
+//    fprintf( stdout, "\t-f       : toggles one fancy feature [default = %s]\n", pPars->fFancy? "yes": "no" );
+    fprintf( stdout, "\t-r       : enables expansion/reduction of the best cuts [default = %s]\n", pPars->fExpRed? "yes": "no" );
+    fprintf( stdout, "\t-l       : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" );
+    fprintf( stdout, "\t-e       : uses edge-based cut selection heuristics [default = %s]\n", pPars->fEdge? "yes": "no" );
+    fprintf( stdout, "\t-m       : enables cut minimization by removing vacuous variables [default = %s]\n", pPars->fCutMin? "yes": "no" );
+//    fprintf( stdout, "\t-s       : toggles sequential mapping [default = %s]\n", pPars->fSeqMap? "yes": "no" );
+//    fprintf( stdout, "\t-t       : toggles the use of true sequential cuts [default = %s]\n", pPars->fLiftLeaves? "yes": "no" );
+    fprintf( stdout, "\t-b       : toggles deriving local AIGs using bi-decomposition [default = %s]\n", pPars->fBidec? "yes": "no" );
+    fprintf( stdout, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h       : prints the command usage\n");
     return 1;
 }
 
@@ -15423,140 +15768,6 @@ usage:
 
 /**Function*************************************************************
 
-  Synopsis    [Command procedure to read LUT libraries.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8ReadLut( Abc_Frame_t * pAbc, int argc, char **argv )
-{
-    FILE * pFile;
-    char * FileName;
-    void * pLib;
-    int c;
-    extern If_Lib_t * If_LutLibRead( char * FileName );
-    extern void If_LutLibFree( If_Lib_t * pLutLib );
-
-    // set the defaults
-    Extra_UtilGetoptReset();
-    while ( (c = Extra_UtilGetopt(argc, argv, "h")) != EOF ) 
-    {
-        switch (c) 
-        {
-            case 'h':
-                goto usage;
-                break;
-            default:
-                goto usage;
-        }
-    }
-
-
-    if ( argc != globalUtilOptind + 1 )
-    {
-        goto usage;
-    }
-
-    // get the input file name
-    FileName = argv[globalUtilOptind];
-    if ( (pFile = fopen( FileName, "r" )) == NULL )
-    {
-        fprintf( stdout, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".lut", NULL, NULL, NULL, NULL ) )
-            fprintf( stdout, "Did you mean \"%s\"?", FileName );
-        fprintf( stdout, "\n" );
-        return 1;
-    }
-    fclose( pFile );
-
-    // set the new network
-    pLib = If_LutLibRead( FileName );
-    if ( pLib == NULL )
-    {
-        fprintf( stdout, "Reading LUT library has failed.\n" );
-        goto usage;
-    }
-    // replace the current library
-    if ( pAbc->pAbc8Lib != NULL )
-        If_LutLibFree( pAbc->pAbc8Lib );
-    pAbc->pAbc8Lib = pLib;
-    return 0;
-
-usage:
-    fprintf( stdout, "\nusage: *rlut [-h]\n");
-    fprintf( stdout, "\t          read the LUT library from the file\n" );  
-    fprintf( stdout, "\t-h      : print the command usage\n");
-    fprintf( stdout, "\t                                        \n");
-    fprintf( stdout, "\t          File format for a LUT library:\n");
-    fprintf( stdout, "\t          (the default library is shown)\n");
-    fprintf( stdout, "\t                                        \n");
-    fprintf( stdout, "\t          # The area/delay of k-variable LUTs:\n");
-    fprintf( stdout, "\t          # k  area   delay\n");
-    fprintf( stdout, "\t          1      1      1\n");
-    fprintf( stdout, "\t          2      2      2\n");
-    fprintf( stdout, "\t          3      4      3\n");
-    fprintf( stdout, "\t          4      8      4\n");
-    fprintf( stdout, "\t          5     16      5\n");
-    fprintf( stdout, "\t          6     32      6\n");
-    return 1;       /* error exit */
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Command procedure to read LUT libraries.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8PrintLut( Abc_Frame_t * pAbc, int argc, char **argv )
-{
-    int c;
-    extern void If_LutLibPrint( If_Lib_t * pLutLib );
-
-    // set the defaults
-    Extra_UtilGetoptReset();
-    while ( (c = Extra_UtilGetopt(argc, argv, "h")) != EOF ) 
-    {
-        switch (c) 
-        {
-            case 'h':
-                goto usage;
-                break;
-            default:
-                goto usage;
-        }
-    }
-
-    if ( argc != globalUtilOptind )
-    {
-        goto usage;
-    }
-
-    // set the new network
-    if ( pAbc->pAbc8Lib == NULL )
-        printf( "LUT library is not specified.\n" );
-    else
-        If_LutLibPrint( pAbc->pAbc8Lib );
-    return 0;
-
-usage:
-    fprintf( stdout, "\nusage: *plut [-h]\n");
-    fprintf( stdout, "\t          print the current LUT library\n" );  
-    fprintf( stdout, "\t-h      : print the command usage\n");
-    return 1;       /* error exit */
-}
-
-
-/**Function*************************************************************
-
   Synopsis    []
 
   Description []
@@ -15671,9 +15882,21 @@ int Abc_CommandAbc8Mfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pAbc8Nwk == NULL )
     {
-        printf( "Abc_CommandAbc8Mfs(): There is no mapped network to strash.\n" );
+        printf( "Abc_CommandAbc8Mfs(): There is no mapped network.\n" );
+        return 1;
+    }
+    if ( pAbc->pAbc8Lib == NULL )
+    {
+        printf( "Abc_CommandAbc8Mfs(): There is no LUT library.\n" );
         return 1;
     }
+    if ( If_LutLibDelaysAreDifferent(pAbc->pAbc8Lib) )
+    {
+        printf( "Abc_CommandAbc8Mfs(): Cannot perform don't-care simplication with variable-pin-delay LUT model.\n" );
+        printf( "The delay model should be fixed-pin-delay, for example, the delay of all pins of all LUTs is 0.4.\n" );
+        return 1;
+    }
+
 
     // modify the current network
     if ( !Mfx_Perform( pAbc->pAbc8Nwk, pPars, pAbc->pAbc8Lib ) )
@@ -15858,7 +16081,7 @@ int Abc_CommandAbc8Speedup( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     fUseLutLib = 0;
-    Percentage = 3;
+    Percentage = 5;
     Degree     = 2;
     fVerbose   = 0;
     fVeryVerbose = 0;
@@ -16027,6 +16250,8 @@ int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pAbc->pAbc8Aig )
         Aig_ManStop( pAbc->pAbc8Aig );
     pAbc->pAbc8Aig = pAigNew;
+
+    Abc_CommandAbc8Sweep( pAbc, 0, NULL );
     return 0;
 
 usage:
@@ -16051,212 +16276,6 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandAbc8Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    void * pNtlNew;
-    int fVerbose;
-    int c;
-    extern void * Ntl_ManSweep( void * p, Aig_Man_t * pAig, int fVerbose );
-    extern Aig_Man_t * Ntl_ManExtract( void * p );
-
-    // set defaults
-    fVerbose = 1;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        printf( "Abc_CommandAbc8Sweep(): There is no design to sweep.\n" );
-        return 1;
-    }
-    if ( pAbc->pAbc8Aig == NULL )
-    {
-        printf( "Abc_CommandAbc8Sweep(): There is no AIG to use.\n" );
-        return 1;
-    }
-
-    // sweep the current design
-    pNtlNew = Ntl_ManSweep( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, fVerbose );
-    if ( pNtlNew == NULL )
-    {
-        printf( "Abc_CommandAbc8Sweep(): Sweeping has failed.\n" );
-        return 1;
-    }
-    // replace
-    Abc_FrameClearDesign(); 
-    pAbc->pAbc8Ntl = pNtlNew;
-    pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
-    if ( pAbc->pAbc8Aig == NULL )
-    {
-        printf( "Abc_CommandAbc8Sweep(): AIG extraction has failed.\n" );
-        return 1;
-    }
-    return 0;
-
-usage:
-    fprintf( stdout, "usage: *sw [-h]\n" );
-    fprintf( stdout, "\t        reads the design with whiteboxes\n" );
-    fprintf( stdout, "\t-v    : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
-    fprintf( stdout, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Aig_Man_t * pAig1, * pAig2;
-    void * pTemp;
-    char ** pArgvNew;
-    int nArgcNew;
-    int c;
-    int fVerbose;
-    int nConfLimit;
-    int fSmart;
-    int nPartSize;
-    extern Aig_Man_t * Ntl_ManCollapse( void * p, int fSeq );
-    extern void * Ntl_ManDup( void * pOld );
-    extern void Ntl_ManFree( void * p );
-    extern void * Ntl_ManInsertNtk( void * p, void * pNtk );
-
-    extern void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan1, Aig_Man_t ** ppMan2 );
-    extern int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
-
-    // set defaults
-    nConfLimit = 10000;   
-    nPartSize  = 100;
-    fSmart     = 0;
-    fVerbose   = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CPsvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'C':
-            if ( globalUtilOptind >= argc )
-            {
-                fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nConfLimit = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nConfLimit < 0 ) 
-                goto usage;
-            break;
-        case 'P':
-            if ( globalUtilOptind >= argc )
-            {
-                fprintf( stdout, "Command line switch \"-P\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nPartSize = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nPartSize < 0 ) 
-                goto usage;
-            break;
-        case 's':
-            fSmart ^= 1;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        default:
-            goto usage;
-        }
-    }
-
-    pArgvNew = argv + globalUtilOptind;
-    nArgcNew = argc - globalUtilOptind;
-    if ( nArgcNew != 0 && nArgcNew != 2 )
-    {
-        printf( "Currently can only compare current mapped network against the spec, or designs derived from two files.\n" );
-        return 0;
-    }
-    if ( nArgcNew == 2 )
-    {
-        Ntl_ManPrepareCec( pArgvNew[0], pArgvNew[1], &pAig1, &pAig2 );
-        if ( !pAig1 || !pAig2 )
-            return 1;
-        Fra_FraigCecTop( pAig1, pAig2, nConfLimit, nPartSize, fSmart, fVerbose );
-        Aig_ManStop( pAig1 );
-        Aig_ManStop( pAig2 );
-        return 0;
-    }
-
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        printf( "Abc_CommandAbc8Cec(): There is no design to verify.\n" );
-        return 1;
-    }
-    if ( pAbc->pAbc8Nwk == NULL )
-    {
-        printf( "Abc_CommandAbc8Cec(): There is no mapped network to verify.\n" );
-        return 1;
-    }
-
-    // derive AIGs
-    pAig1 = Ntl_ManCollapse( pAbc->pAbc8Ntl, 0 );
-    pTemp = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk );
-    if ( pTemp == NULL )
-    {
-        printf( "Abc_CommandAbc8Cec(): Inserting the design has failed.\n" );
-        return 1;
-    }
-    pAig2 = Ntl_ManCollapse( pTemp, 0 );
-    Ntl_ManFree( pTemp );
-
-    // perform verification
-    Fra_FraigCecTop( pAig1, pAig2, nConfLimit, nPartSize, fSmart, fVerbose );
-    Aig_ManStop( pAig1 );
-    Aig_ManStop( pAig2 );
-    return 0;
-
-usage:
-    fprintf( stdout, "usage: *cec [-C num] [-P num] [-svh] <file1> <file2>\n" );
-    fprintf( stdout, "\t         performs combinational equivalence checking\n" );
-    fprintf( stdout, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
-    fprintf( stdout, "\t-P num : the partition size for partitioned CEC [default = %d]\n", nPartSize );
-    fprintf( stdout, "\t-s     : toggle smart and natural output partitioning [default = %s]\n", fSmart? "smart": "natural" );
-    fprintf( stdout, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
-    fprintf( stdout, "\t-h     : print the command usage\n");
-    fprintf( stdout, "\tfile1  : (optional) the file with the first network\n");
-    fprintf( stdout, "\tfile2  : (optional) the file with the second network\n");
-    fprintf( stdout, "\t         if no files are given, uses the current network and its spec\n");
-    fprintf( stdout, "\t         if two files are given, compares designs derived from files\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Abc_CommandAbc8Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Aig_Man_t * pAigNew;
@@ -16319,6 +16338,8 @@ int Abc_CommandAbc8Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pAbc->pAbc8Aig )
         Aig_ManStop( pAbc->pAbc8Aig );
     pAbc->pAbc8Aig = pAigNew;
+
+    Abc_CommandAbc8Sweep( pAbc, 0, NULL );
     return 0;
 
 usage:
@@ -16421,6 +16442,8 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pAbc->pAbc8Aig )
         Aig_ManStop( pAbc->pAbc8Aig );
     pAbc->pAbc8Aig = pAigNew;
+
+    Abc_CommandAbc8Sweep( pAbc, 0, NULL );
     return 0;
 
 usage:
@@ -16604,6 +16627,8 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pAbc->pAbc8Aig )
         Aig_ManStop( pAbc->pAbc8Aig );
     pAbc->pAbc8Aig = pAigNew;
+
+    Abc_CommandAbc8Sweep( pAbc, 0, NULL );
     return 0;
 
 usage:
@@ -16637,6 +16662,213 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc8Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    void * pNtlNew;
+    int fVerbose;
+    int c;
+    extern void * Ntl_ManSweep( void * p, Aig_Man_t * pAig, int fVerbose );
+    extern Aig_Man_t * Ntl_ManExtract( void * p );
+
+    // set defaults
+    fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAbc8Ntl == NULL )
+    {
+        printf( "Abc_CommandAbc8Sweep(): There is no design to sweep.\n" );
+        return 1;
+    }
+    if ( pAbc->pAbc8Aig == NULL )
+    {
+        printf( "Abc_CommandAbc8Sweep(): There is no AIG to use.\n" );
+        return 1;
+    }
+
+    // sweep the current design
+    pNtlNew = Ntl_ManSweep( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, fVerbose );
+    if ( pNtlNew == NULL )
+    {
+        printf( "Abc_CommandAbc8Sweep(): Sweeping has failed.\n" );
+        return 1;
+    }
+    // replace
+    Abc_FrameClearDesign(); 
+    pAbc->pAbc8Ntl = pNtlNew;
+    pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
+    if ( pAbc->pAbc8Aig == NULL )
+    {
+        printf( "Abc_CommandAbc8Sweep(): AIG extraction has failed.\n" );
+        return 1;
+    }
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: *sw [-h]\n" );
+    fprintf( stdout, "\t        performs structural sweep of the design\n" );
+    fprintf( stdout, "\t        removes dangling nodes, registers, and white-boxes\n" );
+    fprintf( stdout, "\t-v    : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Aig_Man_t * pAig1, * pAig2;
+    void * pTemp;
+    char ** pArgvNew;
+    int nArgcNew;
+    int c;
+    int fVerbose;
+    int nConfLimit;
+    int fSmart;
+    int nPartSize;
+    extern Aig_Man_t * Ntl_ManCollapse( void * p, int fSeq );
+    extern void * Ntl_ManDup( void * pOld );
+    extern void Ntl_ManFree( void * p );
+    extern void * Ntl_ManInsertNtk( void * p, void * pNtk );
+
+    extern void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan1, Aig_Man_t ** ppMan2 );
+    extern int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
+
+    // set defaults
+    nConfLimit = 10000;   
+    nPartSize  = 100;
+    fSmart     = 0;
+    fVerbose   = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CPsvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nConfLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nConfLimit < 0 ) 
+                goto usage;
+            break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nPartSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nPartSize < 0 ) 
+                goto usage;
+            break;
+        case 's':
+            fSmart ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+
+    pArgvNew = argv + globalUtilOptind;
+    nArgcNew = argc - globalUtilOptind;
+    if ( nArgcNew != 0 && nArgcNew != 2 )
+    {
+        printf( "Currently can only compare current mapped network against the spec, or designs derived from two files.\n" );
+        return 0;
+    }
+    if ( nArgcNew == 2 )
+    {
+        Ntl_ManPrepareCec( pArgvNew[0], pArgvNew[1], &pAig1, &pAig2 );
+        if ( !pAig1 || !pAig2 )
+            return 1;
+        Fra_FraigCecTop( pAig1, pAig2, nConfLimit, nPartSize, fSmart, fVerbose );
+        Aig_ManStop( pAig1 );
+        Aig_ManStop( pAig2 );
+        return 0;
+    }
+
+    if ( pAbc->pAbc8Ntl == NULL )
+    {
+        printf( "Abc_CommandAbc8Cec(): There is no design to verify.\n" );
+        return 1;
+    }
+    if ( pAbc->pAbc8Nwk == NULL )
+    {
+        printf( "Abc_CommandAbc8Cec(): There is no mapped network to verify.\n" );
+        return 1;
+    }
+
+    // derive AIGs
+    pAig1 = Ntl_ManCollapse( pAbc->pAbc8Ntl, 0 );
+    pTemp = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk );
+    if ( pTemp == NULL )
+    {
+        printf( "Abc_CommandAbc8Cec(): Inserting the design has failed.\n" );
+        return 1;
+    }
+    pAig2 = Ntl_ManCollapse( pTemp, 0 );
+    Ntl_ManFree( pTemp );
+
+    // perform verification
+    Fra_FraigCecTop( pAig1, pAig2, nConfLimit, nPartSize, fSmart, fVerbose );
+    Aig_ManStop( pAig1 );
+    Aig_ManStop( pAig2 );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: *cec [-C num] [-P num] [-svh] <file1> <file2>\n" );
+    fprintf( stdout, "\t         performs combinational equivalence checking\n" );
+    fprintf( stdout, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
+    fprintf( stdout, "\t-P num : the partition size for partitioned CEC [default = %d]\n", nPartSize );
+    fprintf( stdout, "\t-s     : toggle smart and natural output partitioning [default = %s]\n", fSmart? "smart": "natural" );
+    fprintf( stdout, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    fprintf( stdout, "\tfile1  : (optional) the file with the first network\n");
+    fprintf( stdout, "\tfile2  : (optional) the file with the second network\n");
+    fprintf( stdout, "\t         if no files are given, uses the current network and its spec\n");
+    fprintf( stdout, "\t         if two files are given, compares designs derived from files\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Aig_Man_t * pAig;
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index fafcb52d..271f94df 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -469,6 +469,7 @@ void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk )
     Vec_IntFree( vFanins );
     Vec_IntFree( vFanouts );
 }
+
 /**Function*************************************************************
 
   Synopsis    [Prints the distribution of fanins/fanouts in the network.]
diff --git a/src/base/main/main.c b/src/base/main/main.c
index 8f43c605..997eeb8e 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -222,7 +222,7 @@ int main( int argc, char * argv[] )
     if ( fStatus < 0 ) 
     {
         Abc_Stop();
-    }
+    } 
     return 0;
 
 usage:
diff --git a/src/map/if/if.h b/src/map/if/if.h
index e0b9584d..8cf5c0e8 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -246,7 +246,6 @@ static inline int        If_ObjIsConst1( If_Obj_t * pObj )                   { r
 static inline int        If_ObjIsCi( If_Obj_t * pObj )                       { return pObj->Type == IF_CI;           }
 static inline int        If_ObjIsCo( If_Obj_t * pObj )                       { return pObj->Type == IF_CO;           }
 static inline int        If_ObjIsTerm( If_Obj_t * pObj )                     { return pObj->Type == IF_CI || pObj->Type == IF_CO; }
-//static inline int        If_ObjIsPi( If_Obj_t * pObj )                       { return If_ObjIsCi(pObj) && pObj->pFanin0 == NULL;  }
 static inline int        If_ObjIsLatch( If_Obj_t * pObj )                    { return If_ObjIsCi(pObj) && pObj->pFanin0 != NULL;  }
 static inline int        If_ObjIsAnd( If_Obj_t * pObj )                      { return pObj->Type == IF_AND;          }
 
@@ -343,8 +342,10 @@ extern int             If_ManPerformMappingComb( If_Man_t * p );
 /*=== ifCut.c ============================================================*/
 extern int             If_CutFilter( If_Set_t * pCutSet, If_Cut_t * pCut );
 extern void            If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut );
+extern void            If_CutOrder( If_Cut_t * pCut );
 extern int             If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut );
-extern void            If_CutPrint( If_Man_t * p, If_Cut_t * pCut );
+extern int             If_CutCheck( If_Cut_t * pCut );
+extern void            If_CutPrint( If_Cut_t * pCut );
 extern void            If_CutPrintTiming( If_Man_t * p, If_Cut_t * pCut );
 extern void            If_CutLift( If_Cut_t * pCut );
 extern void            If_CutCopy( If_Man_t * p, If_Cut_t * pCutDest, If_Cut_t * pCutSrc );
@@ -365,6 +366,7 @@ extern If_Lib_t *      If_LutLibDup( If_Lib_t * p );
 extern void            If_LutLibFree( If_Lib_t * pLutLib );
 extern void            If_LutLibPrint( If_Lib_t * pLutLib );
 extern int             If_LutLibDelaysAreDiscrete( If_Lib_t * pLutLib );
+extern int             If_LutLibDelaysAreDifferent( If_Lib_t * pLutLib );
 extern If_Lib_t *      If_SetSimpleLutLib( int nLutSize );
 extern float           If_LutLibFastestPinDelay( If_Lib_t * p );
 extern float           If_LutLibSlowestPinDelay( If_Lib_t * p );
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index 08653d95..afaae239 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -297,6 +297,7 @@ int If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut )
             return 0;
     }
     pCut->uSign = pCut0->uSign | pCut1->uSign;
+    assert( If_CutCheck( pCut ) );
     return 1;
 }
 
@@ -605,6 +606,63 @@ void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut )
 
 /**Function*************************************************************
 
+  Synopsis    [Orders the leaves of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_CutOrder( If_Cut_t * pCut )
+{
+    int i, Temp, fChanges;
+    do {
+        fChanges = 0;
+        for ( i = 0; i < (int)pCut->nLeaves - 1; i++ )
+        {
+            assert( pCut->pLeaves[i] != pCut->pLeaves[i+1] );
+            if ( pCut->pLeaves[i] <= pCut->pLeaves[i+1] )
+                continue;
+            Temp = pCut->pLeaves[i];
+            pCut->pLeaves[i] = pCut->pLeaves[i+1];
+            pCut->pLeaves[i+1] = Temp;
+            fChanges = 1;
+        }
+    } while ( fChanges );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks correctness of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_CutCheck( If_Cut_t * pCut )
+{
+    int i;
+    assert( pCut->nLeaves <= pCut->nLimit );
+    for ( i = 1; i < (int)pCut->nLeaves; i++ )
+    {
+        if ( pCut->pLeaves[i-1] >= pCut->pLeaves[i] )
+        {
+            printf( "If_CutCheck(): Cut has wrong ordering of inputs.\n" );
+            return 0;
+        }
+        assert( pCut->pLeaves[i-1] < pCut->pLeaves[i] );
+    }
+    return 1;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Prints one cut.]
 
   Description []
@@ -614,7 +672,7 @@ void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-void If_CutPrint( If_Man_t * p, If_Cut_t * pCut )
+void If_CutPrint( If_Cut_t * pCut )
 {
     unsigned i;
     printf( "{" );
diff --git a/src/map/if/ifLib.c b/src/map/if/ifLib.c
index 455f43d9..b3e6ad4c 100644
--- a/src/map/if/ifLib.c
+++ b/src/map/if/ifLib.c
@@ -228,6 +228,37 @@ int If_LutLibDelaysAreDiscrete( If_Lib_t * pLutLib )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns 1 if the delays are discrete.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_LutLibDelaysAreDifferent( If_Lib_t * pLutLib )
+{
+    int i, k;
+    float Delay = pLutLib->pLutDelays[1][0];
+    if ( pLutLib->fVarPinDelays )
+    {
+        for ( i = 2; i <= pLutLib->LutMax; i++ )
+        for ( k = 0; k < i; k++ )
+            if ( pLutLib->pLutDelays[i][k] != Delay )
+                return 1;
+    }
+    else
+    {
+        for ( i = 2; i <= pLutLib->LutMax; i++ )
+            if ( pLutLib->pLutDelays[i][0] != Delay )
+                return 1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Sets simple LUT library.]
 
   Description []
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 5f06b0e9..74557a54 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -88,7 +88,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
     {
         // recompute the parameters of the best cut
         pCut->Delay = If_CutDelay( p, pCut );
-//        assert( pCut->Delay <= pObj->Required + p->fEpsilon );
+        assert( pCut->Delay <= pObj->Required + p->fEpsilon );
         pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut ) : If_CutAreaFlow( p, pCut );
         if ( p->pPars->fEdge )
             pCut->Edge = (Mode == 2)? If_CutEdgeDerefed( p, pCut ) : If_CutEdgeFlow( p, pCut );
diff --git a/src/map/if/ifReduce.c b/src/map/if/ifReduce.c
index 0912a965..fd1af0d7 100644
--- a/src/map/if/ifReduce.c
+++ b/src/map/if/ifReduce.c
@@ -263,6 +263,7 @@ void If_ManImproveNodeUpdate( If_Man_t * p, If_Obj_t * pObj, Vec_Ptr_t * vFront
     pCut->nLeaves = Vec_PtrSize(vFront);
     Vec_PtrForEachEntry( vFront, pFanin, i )
         pCut->pLeaves[i] = pFanin->Id;
+    If_CutOrder( pCut );
     // ref the new cut
     If_CutAreaRef( p, pCut );
 }