Version abc80327

58 files changed, 2347 insertions, 571 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 8901e8bb..8a61a530 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -103,6 +103,7 @@ struct Aig_Box_t_
 struct Aig_Man_t_
 {
     char *           pName;          // the design name
+    char *           pSpec;          // the input file name
     // AIG nodes
     Vec_Ptr_t *      vPis;           // the array of PIs
     Vec_Ptr_t *      vPos;           // the array of POs
@@ -328,7 +329,6 @@ static inline int          Aig_ObjSetLevel( Aig_Obj_t * pObj, int i ) { assert(
 static inline void         Aig_ObjClean( Aig_Obj_t * pObj )       { memset( pObj, 0, sizeof(Aig_Obj_t) );                                                             }
 static inline Aig_Obj_t *  Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj )  { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); } 
 static inline Aig_Obj_t *  Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj )    { return p->pEquivs? p->pEquivs[pObj->Id] : NULL;             } 
-static inline Aig_Obj_t *  Aig_ObjHaig( Aig_Obj_t * pObj )        { assert( Aig_Regular(pObj)->pHaig ); return Aig_NotCond( Aig_Regular(pObj)->pHaig, Aig_IsComplement(pObj) ); } 
 static inline int          Aig_ObjPioNum( Aig_Obj_t * pObj )      { assert( !Aig_ObjIsNode(pObj) ); return (int)pObj->pNext;                                                    }
 static inline int          Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )    
 { 
@@ -540,6 +540,7 @@ extern Vec_Ptr_t *     Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize );
 extern Vec_Ptr_t *     Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize );
 extern Aig_Man_t *     Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose );
 extern Aig_Man_t *     Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfMax, int nLevelMax, int fVerbose );
+extern Aig_Man_t *     Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose );
 /*=== aigPartReg.c =========================================================*/
 extern Vec_Ptr_t *     Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOverSize );
 extern Vec_Ptr_t *     Aig_ManRegPartitionSmart( Aig_Man_t * pAig, int nPartSize );
@@ -612,6 +613,7 @@ extern void            Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
 extern void            Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName );
 extern void            Aig_ManSetPioNumbers( Aig_Man_t * p );
 extern void            Aig_ManCleanPioNumbers( Aig_Man_t * p );
+extern int             Aig_ManCountChoices( Aig_Man_t * p );
 
 /*=== aigWin.c =========================================================*/
 extern void            Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit );
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 062173e6..665401c3 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -96,6 +96,7 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
     {
         pObjNew = Aig_ObjCreatePi( pNew );
         pObjNew->Level = pObj->Level;
+        pObjNew->pHaig = pObj->pHaig;
         pObj->pData = pObjNew;
     }
     return pNew;
@@ -114,20 +115,16 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
 ***********************************************************************/
 Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
 {
+    Aig_Obj_t * pObjNew;
     if ( pObj->pData )
         return pObj->pData;
     Aig_ManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );
     if ( Aig_ObjIsBuf(pObj) )
         return pObj->pData = Aig_ObjChild0Copy(pObj);
     Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
-    if ( pNew->pManHaig == NULL )
-        return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    else
-    {
-        Aig_Obj_t * pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-        Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig);
-        return pObj->pData = pObjNew;
-    }
+    pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+    return pObj->pData = pObjNew;
 }
 
 /**Function*************************************************************
@@ -156,8 +153,6 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // create the PIs
     Aig_ManCleanData( p );
-    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
     // duplicate internal nodes
     if ( fOrdered )
     {
@@ -165,61 +160,42 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
         {
             if ( Aig_ObjIsBuf(pObj) )
             {
-                if ( pNew->pManHaig == NULL )
-                    pObj->pData = Aig_ObjChild0Copy(pObj);
-                else
-                {
-                    Aig_Obj_t * pObjNew = Aig_ObjChild0Copy(pObj);
-                    Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig);
-                    pObj->pData = pObjNew;
-                }
+                pObjNew = Aig_ObjChild0Copy(pObj);
             }
             else if ( Aig_ObjIsNode(pObj) )
             {
-                if ( pNew->pManHaig == NULL )
-                    pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-                else
-                {
-                    Aig_Obj_t * pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-                    Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig);
-                    pObj->pData = pObjNew;
-                }
+                pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
             }
             else if ( Aig_ObjIsPi(pObj) )
             {
                 pObjNew = Aig_ObjCreatePi( pNew );
-                pObjNew->pHaig = pObj->pHaig;
                 pObjNew->Level = pObj->Level;
-                pObj->pData = pObjNew;
             }
             else if ( Aig_ObjIsPo(pObj) )
             {
                 pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
-                pObjNew->pHaig = pObj->pHaig;
-                pObj->pData = pObjNew;
+            }
+            else if ( Aig_ObjIsConst1(pObj) )
+            {
+                pObjNew = Aig_ManConst1(pNew);
             }
             else
                 assert( 0 );
+            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+            pObj->pData = pObjNew;
         }
     }
     else
     {
-/*
-        Aig_ManForEachPi( p, pObj, i )
-        {
-            pObjNew = Aig_ObjCreatePi( pNew );
-            pObjNew->pHaig = pObj->pHaig;
-            pObjNew->Level = pObj->Level;
-            pObj->pData = pObjNew;
-        }
-*/
+        Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+        Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
         Aig_ManForEachObj( p, pObj, i )
         {
             if ( Aig_ObjIsPi(pObj) )
             {
                 pObjNew = Aig_ObjCreatePi( pNew );
-                pObjNew->pHaig = pObj->pHaig;
                 pObjNew->Level = pObj->Level;
+                Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
                 pObj->pData = pObjNew;
             }
             else if ( Aig_ObjIsPo(pObj) )
@@ -227,18 +203,10 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
                 Aig_ManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );        
 //                assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
                 pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
-                pObjNew->pHaig = pObj->pHaig;
+                Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
                 pObj->pData = pObjNew;
             }
         }
-/*
-        Aig_ManForEachPo( p, pObj, i )
-        {
-            pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
-            pObjNew->pHaig = pObj->pHaig;
-            pObj->pData = pObjNew;
-        }
-*/
     }
     // add the POs
     assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
@@ -372,6 +340,7 @@ void Aig_ManStop( Aig_Man_t * p )
     if ( p->vOnehots ) Vec_VecFree( (Vec_Vec_t *)p->vOnehots );
     FREE( p->pSeqModel );
     FREE( p->pName );
+    FREE( p->pSpec );
     FREE( p->pObjCopies );
     FREE( p->pReprs );
     FREE( p->pEquivs );
@@ -410,6 +379,27 @@ int Aig_ManCleanup( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Performs one iteration of AIG rewriting.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManHaigCounter( Aig_Man_t * pAig )
+{
+    Aig_Obj_t * pObj;
+    int Counter, i;
+    Counter = 0;
+    Aig_ManForEachNode( pAig, pObj, i )
+        Counter += (pObj->pHaig != NULL);
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Stops the AIG manager.]
 
   Description []
@@ -421,8 +411,12 @@ int Aig_ManCleanup( Aig_Man_t * p )
 ***********************************************************************/
 void Aig_ManPrintStats( Aig_Man_t * p )
 {
+    int nChoices = Aig_ManCountChoices(p);
     printf( "PI/PO/Lat = %5d/%5d/%5d   ", Aig_ManPiNum(p), Aig_ManPoNum(p), Aig_ManLatchNum(p) );
-    printf( "A = %7d. ",    Aig_ManAndNum(p) );
+    printf( "A = %7d. ",   Aig_ManAndNum(p) );
+    printf( "Eq = %7d. ",  Aig_ManHaigCounter(p) );
+    if ( nChoices )
+        printf( "Ch = %5d. ",  nChoices );
     if ( Aig_ManExorNum(p) )
         printf( "X = %5d. ",    Aig_ManExorNum(p) );
     if ( Aig_ManBufNum(p) )
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index 80838e19..734f1277 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -97,12 +97,14 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost )
     // update node counters of the manager
     p->nObjs[Aig_ObjType(pObj)]++;
     assert( pObj->pData == NULL );
+/*
     if ( p->pManHaig )
     {
         pGhost->pFanin0 = Aig_ObjHaig( pGhost->pFanin0 );
         pGhost->pFanin1 = Aig_ObjHaig( pGhost->pFanin1 );
         pObj->pHaig = Aig_ObjCreate( p->pManHaig, pGhost );
     }
+*/
     return pObj;
 }
 
@@ -360,6 +362,7 @@ int Aig_ManPropagateBuffers( Aig_Man_t * p, int fNodesOnly, int fUpdateLevel )
 void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly, int fUpdateLevel )
 {
     Aig_Obj_t * pObjNewR = Aig_Regular(pObjNew);
+    Aig_Obj_t * pHaig = pObjNewR->pHaig? pObjNewR->pHaig : pObjOld->pHaig;
     // the object to be replaced cannot be complemented
     assert( !Aig_IsComplement(pObjOld) );
     // the object to be replaced cannot be a terminal
@@ -422,6 +425,7 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
         p->nBufMax = AIG_MAX( p->nBufMax, Vec_PtrSize(p->vBufs) );
         Aig_ManPropagateBuffers( p, fNodesOnly, fUpdateLevel );
     }
+    pObjOld->pHaig = pHaig;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index 1fb93eb7..2a9800cf 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "aig.h"
+#include "tim.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -1346,6 +1347,235 @@ Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfM
 }
 
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Set the representative.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Aig_ObjSetRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 )
+{
+    assert( p->pReprs != NULL );
+    assert( !Aig_IsComplement(pNode1) );
+    assert( !Aig_IsComplement(pNode2) );
+    assert( pNode1->Id < p->nReprsAlloc );
+    assert( pNode2->Id < p->nReprsAlloc );
+    if ( pNode1 == pNode2 )
+        return;
+    if ( pNode1->Id < pNode2->Id )
+        p->pReprs[pNode2->Id] = pNode1;
+    else
+        p->pReprs[pNode1->Id] = pNode2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Constructively accumulates choices.]
+
+  Description [pNew is a new AIG with choices under construction.
+  pPrev is the AIG preceding pThis in the order of deriving choices.
+  pThis is the current AIG to be added to pNew while creating choices.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManChoiceConstructiveOne( Aig_Man_t * pNew, Aig_Man_t * pPrev, Aig_Man_t * pThis )
+{
+    Aig_Obj_t * pObj, * pObjNew;
+    int i;
+    assert( Aig_ManPiNum(pNew) == Aig_ManPiNum(pPrev) );
+    assert( Aig_ManPiNum(pNew) == Aig_ManPiNum(pThis) );
+    assert( Aig_ManPoNum(pNew) == Aig_ManPoNum(pPrev) );
+    assert( Aig_ManPoNum(pNew) == Aig_ManPoNum(pThis) );
+    // make sure the nodes of pPrev point to pNew
+    Aig_ManForEachObj( pNew, pObj, i )
+        pObj->fMarkB = 1;
+    Aig_ManForEachObj( pPrev, pObj, i )
+        assert( Aig_Regular(pObj->pData)->fMarkB );
+    Aig_ManForEachObj( pNew, pObj, i )
+        pObj->fMarkB = 0;
+    // make sure the nodes of pThis point to pPrev
+    Aig_ManForEachObj( pPrev, pObj, i )
+        pObj->fMarkB = 1;
+    Aig_ManForEachObj( pThis, pObj, i )
+        assert( pObj->pHaig == NULL || (!Aig_IsComplement(pObj->pHaig) && pObj->pHaig->fMarkB) );
+    Aig_ManForEachObj( pPrev, pObj, i )
+        pObj->fMarkB = 0;
+    // remap nodes of pThis on top of pNew using pPrev
+    pObj = Aig_ManConst1(pThis);
+    pObj->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( pThis, pObj, i )
+        pObj->pData = Aig_ManPi(pNew, i);
+    Aig_ManForEachPo( pThis, pObj, i )
+        pObj->pData = Aig_ManPo(pNew, i);
+    // go through the nodes in the topological order
+    Aig_ManForEachNode( pThis, pObj, i )
+    {
+        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        if ( pObj->pHaig == NULL )
+            continue;
+        // pObj->pData and pObj->pHaig->pData are equivalent
+        Aig_ObjSetRepr( pNew, Aig_Regular(pObj->pData), Aig_Regular(pObj->pHaig->pData) );
+    }
+    // set the inputs of POs as equivalent
+    Aig_ManForEachPo( pThis, pObj, i )
+    {
+        pObjNew = Aig_ObjFanin0( Aig_ManPo(pNew,i) );
+        // pObjNew and Aig_ObjFanin0(pObj)->pData are equivalent
+        Aig_ObjSetRepr( pNew, pObjNew, Aig_Regular(Aig_ObjFanin0(pObj)->pData) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes levels for AIG with choices and white boxes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManChoiceLevel_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pNext;
+    int i, iBox, iTerm1, nTerms, LevelMax = 0;
+    if ( Aig_ObjIsTravIdCurrent( pNew, pObj ) )
+        return;
+    Aig_ObjSetTravIdCurrent( pNew, pObj );
+    if ( Aig_ObjIsPi(pObj) )
+    {
+        if ( pNew->pManTime )
+        {
+            iBox = Tim_ManBoxForCi( pNew->pManTime, Aig_ObjPioNum(pObj) );
+            if ( iBox >= 0 ) // this is not a true PI
+            {
+                iTerm1 = Tim_ManBoxInputFirst( pNew->pManTime, iBox );
+                nTerms = Tim_ManBoxInputNum( pNew->pManTime, iBox );
+                for ( i = 0; i < nTerms; i++ )
+                {
+                    pNext = Aig_ManPo(pNew, iTerm1 + i);
+                    Aig_ManChoiceLevel_rec( pNew, pNext );
+                    if ( LevelMax < Aig_ObjLevel(pNext) )
+                        LevelMax = Aig_ObjLevel(pNext);
+                }
+                LevelMax++;
+            }
+        }
+    }
+    else if ( Aig_ObjIsPo(pObj) )
+    {
+        pNext = Aig_ObjFanin0(pObj);
+        Aig_ManChoiceLevel_rec( pNew, pNext );
+        if ( LevelMax < Aig_ObjLevel(pNext) )
+            LevelMax = Aig_ObjLevel(pNext);
+    }
+    else if ( Aig_ObjIsNode(pObj) )
+    { 
+        // get the maximum level of the two fanins
+        pNext = Aig_ObjFanin0(pObj);
+        Aig_ManChoiceLevel_rec( pNew, pNext );
+        if ( LevelMax < Aig_ObjLevel(pNext) )
+            LevelMax = Aig_ObjLevel(pNext);
+        pNext = Aig_ObjFanin1(pObj);
+        Aig_ManChoiceLevel_rec( pNew, pNext );
+        if ( LevelMax < Aig_ObjLevel(pNext) )
+            LevelMax = Aig_ObjLevel(pNext);
+        LevelMax++;
+
+        // get the level of the nodes in the choice node
+        if ( pNew->pEquivs && (pNext = pNew->pEquivs[pObj->iData]) )
+        {
+            Aig_ManChoiceLevel_rec( pNew, pNext );
+            if ( LevelMax < Aig_ObjLevel(pNext) )
+                LevelMax = Aig_ObjLevel(pNext);
+        }
+    }
+    else
+        assert( 0 );
+    Aig_ObjSetLevel( pObj, LevelMax );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes levels for AIG with choices and white boxes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManChoiceLevel( Aig_Man_t * pNew )
+{
+    Aig_Obj_t * pObj;
+    int i, LevelMax = 0;
+    Aig_ManForEachObj( pNew, pObj, i )
+        Aig_ObjSetLevel( pObj, 0 );
+    Aig_ManSetPioNumbers( pNew );
+    Aig_ManIncrementTravId( pNew );
+    Aig_ManForEachPo( pNew, pObj, i )
+    {
+        Aig_ManChoiceLevel_rec( pNew, pObj );
+        if ( LevelMax < Aig_ObjLevel(pObj) )
+            LevelMax = Aig_ObjLevel(pObj);
+    }
+    Aig_ManCleanPioNumbers( pNew );
+    return LevelMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Constructively accumulates choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
+{
+    Aig_Man_t * pNew, * pThis, * pPrev;
+    int i;
+    // start AIG with choices
+    pPrev = Vec_PtrEntry( vAigs, 0 );
+    pNew = Aig_ManDup( pPrev, 1 );
+    // create room for equivalent nodes and representatives
+    assert( pNew->pReprs == NULL );
+    pNew->nReprsAlloc = Vec_PtrSize(vAigs) * Aig_ManObjNumMax(pNew);
+    pNew->pReprs = ALLOC( Aig_Obj_t *, pNew->nReprsAlloc );
+    memset( pNew->pReprs, 0, sizeof(Aig_Obj_t *) * pNew->nReprsAlloc );
+    // add other AIGs one by one
+    Vec_PtrForEachEntryStart( vAigs, pThis, i, 1 )
+    {
+        Aig_ManChoiceConstructiveOne( pNew, pPrev, pThis );
+        pPrev = pThis;
+    }
+    // derive the result of choicing
+//Aig_ManPrintStats( pNew );
+    pNew = Aig_ManRehash( pNew );
+//Aig_ManPrintStats( pNew );
+    // create the equivalent nodes lists
+    Aig_ManMarkValidChoices( pNew );
+//Aig_ManPrintStats( pNew );
+    // reset levels
+    Aig_ManChoiceLevel( pNew );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigRetF.c b/src/aig/aig/aigRetF.c
index 8ca4fba1..4318be9d 100644
--- a/src/aig/aig/aigRetF.c
+++ b/src/aig/aig/aigRetF.c
@@ -178,6 +178,7 @@ Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax )
             p->nObjs[AIG_OBJ_BUF]++;
             Aig_ObjConnect( p, pObj, Aig_NotCond(pObjLo, fCompl), NULL );
             // create HAIG if defined
+/*
             if ( p->pManHaig )
             {
                 // create HAIG latch
@@ -188,6 +189,7 @@ Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax )
                 assert( pObjLo->pHaig->pHaig == NULL );
                 pObjLo->pHaig->pHaig = Aig_Regular(pObj->pHaig);
             }
+*/
             // mark the change
             fChange = 1;
             // check the limit
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index 7900da51..dcc0a118 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -890,6 +890,28 @@ void Aig_ManCleanPioNumbers( Aig_Man_t * p )
         pObj->pNext = NULL;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Sets the PI/PO numbers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManCountChoices( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i, Counter = 0;
+    Aig_ManForEachNode( p, pObj, i )
+        Counter += Aig_ObjIsChoice( p, pObj );
+    return Counter;
+}
+
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index b02d3bb5..00a85c26 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -3,7 +3,6 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigDfs.c \
     src/aig/aig/aigFanout.c \
     src/aig/aig/aigFrames.c \
-    src/aig/aig/aigHaig.c \
     src/aig/aig/aigInter.c \
     src/aig/aig/aigMan.c \
     src/aig/aig/aigMem.c \
diff --git a/src/aig/bdc/bdc.h b/src/aig/bdc/bdc.h
index e0c35773..fc476ec6 100644
--- a/src/aig/bdc/bdc.h
+++ b/src/aig/bdc/bdc.h
@@ -37,6 +37,7 @@ extern "C" {
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
+typedef struct Bdc_Fun_t_ Bdc_Fun_t;
 typedef struct Bdc_Man_t_ Bdc_Man_t;
 typedef struct Bdc_Par_t_ Bdc_Par_t;
 struct Bdc_Par_t_
@@ -47,6 +48,12 @@ struct Bdc_Par_t_
     int           fVeryVerbose;  // enable detailed stats
 };
 
+// working with complemented attributes of objects
+static inline int         Bdc_IsComplement( Bdc_Fun_t * p )      { return (int)((PORT_PTRUINT_T)p & (PORT_PTRUINT_T)01);              }
+static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p )           { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p & ~(PORT_PTRUINT_T)01);     }
+static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p )               { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^  (PORT_PTRUINT_T)01);     }
+static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c )    { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^  (PORT_PTRUINT_T)(c!=0)); }
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -59,6 +66,13 @@ struct Bdc_Par_t_
 extern Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars );
 extern void        Bdc_ManFree( Bdc_Man_t * p );
 extern int         Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax );
+extern Bdc_Fun_t * Bdc_ManFunc( Bdc_Man_t * p, int i );
+extern Bdc_Fun_t * Bdc_ManRoot( Bdc_Man_t * p );
+extern int         Bdc_ManNodeNum( Bdc_Man_t * p );
+extern Bdc_Fun_t * Bdc_FuncFanin0( Bdc_Fun_t * p );
+extern Bdc_Fun_t * Bdc_FuncFanin1( Bdc_Fun_t * p );
+extern void *      Bdc_FuncCopy( Bdc_Fun_t * p );
+extern void        Bdc_FuncSetCopy( Bdc_Fun_t * p, void * pCopy );
 
 
 #ifdef __cplusplus
diff --git a/src/aig/bdc/bdcCore.c b/src/aig/bdc/bdcCore.c
index d7811f82..e7675420 100644
--- a/src/aig/bdc/bdcCore.c
+++ b/src/aig/bdc/bdcCore.c
@@ -24,12 +24,32 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    [Accessing contents of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bdc_Fun_t *  Bdc_ManFunc( Bdc_Man_t * p, int i )               { return Bdc_FunWithId(p, i); }
+Bdc_Fun_t *  Bdc_ManRoot( Bdc_Man_t * p )                      { return p->pRoot;            }
+int          Bdc_ManNodeNum( Bdc_Man_t * p )                   { return p->nNodes;           }
+Bdc_Fun_t *  Bdc_FuncFanin0( Bdc_Fun_t * p )                   { return p->pFan0;            }
+Bdc_Fun_t *  Bdc_FuncFanin1( Bdc_Fun_t * p )                   { return p->pFan1;            }
+void *       Bdc_FuncCopy( Bdc_Fun_t * p )                     { return p->pCopy;            }
+void         Bdc_FuncSetCopy( Bdc_Fun_t * p, void * pCopy )    { p->pCopy = pCopy;           }
+
+/**Function*************************************************************
+
   Synopsis    [Allocate resynthesis manager.]
 
   Description []
diff --git a/src/aig/bdc/bdcInt.h b/src/aig/bdc/bdcInt.h
index afba0e67..ab800269 100644
--- a/src/aig/bdc/bdcInt.h
+++ b/src/aig/bdc/bdcInt.h
@@ -54,7 +54,6 @@ typedef enum {
     BDC_TYPE_OTHER      // 7:  unused
 } Bdc_Type_t;
 
-typedef struct Bdc_Fun_t_ Bdc_Fun_t;
 struct Bdc_Fun_t_
 {
     int              Type;         // Const1, PI, AND, XOR, MUX
@@ -122,12 +121,6 @@ struct Bdc_Man_t_
     int              timeTotal;
 };
 
-// working with complemented attributes of objects
-static inline int         Bdc_IsComplement( Bdc_Fun_t * p )             { return (int)((PORT_PTRUINT_T)p & (PORT_PTRUINT_T)01);              }
-static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p )                  { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p & ~(PORT_PTRUINT_T)01);     }
-static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p )                      { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^  (PORT_PTRUINT_T)01);     }
-static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c )           { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^  (PORT_PTRUINT_T)(c!=0)); }
-
 static inline Bdc_Fun_t * Bdc_FunNew( Bdc_Man_t * p )                   { Bdc_Fun_t * pRes; if ( p->nNodes >= p->nNodesAlloc || p->nNodesNew >= p->nNodesMax ) return NULL; pRes = p->pNodes + p->nNodes++; p->nNodesNew++; memset( pRes, 0, sizeof(Bdc_Fun_t) ); return pRes; }
 static inline Bdc_Fun_t * Bdc_FunWithId( Bdc_Man_t * p, int Id )        { assert( Id < p->nNodes ); return p->pNodes + Id; }
 static inline int         Bdc_FunId( Bdc_Man_t * p, Bdc_Fun_t * pFun )  { return pFun - p->pNodes; }
diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index a428f435..d93af02e 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -92,7 +92,7 @@ extern Aig_Man_t *     Dar_ManRewriteDefault( Aig_Man_t * pAig );
 extern Aig_Man_t *     Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose );
 extern Aig_Man_t *     Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
 extern Aig_Man_t *     Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fVerbose );
-extern Aig_Man_t *     Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose );
+extern Aig_Man_t *     Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index 01f75e32..03707481 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -164,6 +164,7 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t *
     // make sure the balanced node is not assigned
 //    assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level );
     assert( pObjOld->pData == NULL );
+    Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig;
     return pObjOld->pData = pObjNew;
 }
 
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index fad4148c..a4ac9082 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -112,6 +112,26 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
     return pAig;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs one iteration of AIG rewriting.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ManHaigPrintStats( Aig_Man_t * pAig )
+{
+    Aig_Obj_t * pObj;
+    int Counter, i;
+    Counter = 0;
+    Aig_ManForEachNode( pAig, pObj, i )
+        Counter += (pObj->pHaig != NULL);
+    printf( "Total nodes = %6d. Equiv nodes = %6d.\n", Aig_ManNodeNum(pAig), Counter );
+}
 
 /**Function*************************************************************
 
@@ -314,42 +334,28 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL
 //alias resyn2   "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
 {
     Vec_Ptr_t * vAigs;
+    Aig_Obj_t * pObj;
+    int i;
+
     vAigs = Vec_PtrAlloc( 3 );
     pAig = Aig_ManDup(pAig, 0);
     Vec_PtrPush( vAigs, pAig );
-    pAig = Dar_ManCompress (pAig, 0, fUpdateLevel, fVerbose);
-    Vec_PtrPush( vAigs, pAig );
-    pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fVerbose);
-    Vec_PtrPush( vAigs, pAig );
-    return vAigs;
-}
 
-/**Function*************************************************************
+    Aig_ManForEachObj( pAig, pObj, i )
+        pObj->pHaig = pObj;
 
-  Synopsis    [Gives the current ABC network to AIG manager for processing.]
-
-  Description []
-               
-  SideEffects []
+    pAig = Dar_ManCompress (pAig, 0, fUpdateLevel, fVerbose);
+    Vec_PtrPush( vAigs, pAig );
+//Aig_ManPrintStats( pAig );
 
-  SeeAlso     []
+    Aig_ManForEachObj( pAig, pObj, i )
+        pObj->pHaig = pObj;
 
-***********************************************************************/
-/*
-Vec_Ptr_t * Dar_ManChoiceSynthesisExt()
-{
-    Vec_Ptr_t * vAigs;
-    Aig_Man_t * pMan;
-    vAigs = Vec_PtrAlloc( 3 );
-    pMan = Ioa_ReadAiger( "i10_1.aig", 1 );
-    Vec_PtrPush( vAigs, pMan );
-    pMan = Ioa_ReadAiger( "i10_2.aig", 1 );
-    Vec_PtrPush( vAigs, pMan );
-    pMan = Ioa_ReadAiger( "i10_3.aig", 1 );
-    Vec_PtrPush( vAigs, pMan );
+    pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fVerbose);
+    Vec_PtrPush( vAigs, pAig );
+//Aig_ManPrintStats( pAig );
     return vAigs;
 }
-*/
 
 /**Function*************************************************************
 
@@ -362,7 +368,7 @@ Vec_Ptr_t * Dar_ManChoiceSynthesisExt()
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose )
+Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose )
 {
     Aig_Man_t * pMan, * pTemp;
     Vec_Ptr_t * vAigs;
@@ -374,16 +380,22 @@ clk = clock();
 
     // swap the first and last network
     // this should lead to the primary choice being "better" because of synthesis
-    pMan = Vec_PtrPop( vAigs );
-    Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
-    Vec_PtrWriteEntry( vAigs, 0, pMan );
+    if ( !fConstruct )
+    {
+        pMan = Vec_PtrPop( vAigs );
+        Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
+        Vec_PtrWriteEntry( vAigs, 0, pMan );
+    }
 
 if ( fVerbose )
 {
 PRT( "Synthesis time", clock() - clk );
 }
 clk = clock();
-    pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
+    if ( fConstruct )
+        pMan = Aig_ManChoiceConstructive( vAigs, fVerbose );
+    else
+        pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
     Vec_PtrForEachEntry( vAigs, pTemp, i )
         Aig_ManStop( pTemp );
     Vec_PtrFree( vAigs );
diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h
index 6390ff70..d7f525a2 100644
--- a/src/aig/hop/hop.h
+++ b/src/aig/hop/hop.h
@@ -321,6 +321,8 @@ extern void            Hop_TableInsert( Hop_Man_t * p, Hop_Obj_t * pObj );
 extern void            Hop_TableDelete( Hop_Man_t * p, Hop_Obj_t * pObj );
 extern int             Hop_TableCountEntries( Hop_Man_t * p );
 extern void            Hop_TableProfile( Hop_Man_t * p );
+/*=== hopTruth.c ========================================================*/
+unsigned *             Hop_ManConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst );
 /*=== hopUtil.c =========================================================*/
 extern void            Hop_ManIncrementTravId( Hop_Man_t * p );
 extern void            Hop_ManCleanData( Hop_Man_t * p );
diff --git a/src/aig/hop/hopTruth.c b/src/aig/hop/hopTruth.c
new file mode 100644
index 00000000..9a2161b6
--- /dev/null
+++ b/src/aig/hop/hopTruth.c
@@ -0,0 +1,210 @@
+/**CFile****************************************************************
+
+  FileName    [hopTruth.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Minimalistic And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: hopTruth.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "hop.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int  Hop_ManTruthWordNum( int nVars )  { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
+
+static inline void Hop_ManTruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
+{
+    int w;
+    for ( w = Hop_ManTruthWordNum(nVars)-1; w >= 0; w-- )
+        pOut[w] = pIn[w];
+}
+static inline void Hop_ManTruthClear( unsigned * pOut, int nVars )
+{
+    int w;
+    for ( w = Hop_ManTruthWordNum(nVars)-1; w >= 0; w-- )
+        pOut[w] = 0;
+}
+static inline void Hop_ManTruthFill( unsigned * pOut, int nVars )
+{
+    int w;
+    for ( w = Hop_ManTruthWordNum(nVars)-1; w >= 0; w-- )
+        pOut[w] = ~(unsigned)0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Construct BDDs and mark AIG nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Hop_ManConvertAigToTruth_rec1( Hop_Obj_t * pObj )
+{
+    int Counter = 0;
+    assert( !Hop_IsComplement(pObj) );
+    if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
+        return 0;
+    Counter += Hop_ManConvertAigToTruth_rec1( Hop_ObjFanin0(pObj) ); 
+    Counter += Hop_ManConvertAigToTruth_rec1( Hop_ObjFanin1(pObj) );
+    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
+    Hop_ObjSetMarkA( pObj );
+    return Counter + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes truth table of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Hop_ManConvertAigToTruth_rec2( Hop_Obj_t * pObj, Vec_Int_t * vTruth, int nWords )
+{
+    unsigned * pTruth, * pTruth0, * pTruth1;
+    int i;
+    assert( !Hop_IsComplement(pObj) );
+    if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
+        return pObj->pData;
+    // compute the truth tables of the fanins
+    pTruth0 = Hop_ManConvertAigToTruth_rec2( Hop_ObjFanin0(pObj), vTruth, nWords );
+    pTruth1 = Hop_ManConvertAigToTruth_rec2( Hop_ObjFanin1(pObj), vTruth, nWords );
+    // creat the truth table of the node
+    pTruth  = Vec_IntFetch( vTruth, nWords );
+    if ( Hop_ObjIsExor(pObj) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = pTruth0[i] ^ pTruth1[i];
+    else if ( !Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = pTruth0[i] & pTruth1[i];
+    else if ( !Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = pTruth0[i] & ~pTruth1[i];
+    else if ( Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = ~pTruth0[i] & pTruth1[i];
+    else // if ( Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = ~pTruth0[i] & ~pTruth1[i];
+    assert( Hop_ObjIsMarkA(pObj) ); // loop detection
+    Hop_ObjClearMarkA( pObj );
+    pObj->pData = pTruth;
+    return pTruth;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes truth table of the node.]
+
+  Description [Assumes that the structural support is no more than 8 inputs.
+  Uses array vTruth to store temporary truth tables. The returned pointer should 
+  be used immediately.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Hop_ManConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst )
+{
+    static unsigned uTruths[8][8] = { // elementary truth tables
+        { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
+        { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
+        { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
+        { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
+        { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, 
+        { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, 
+        { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, 
+        { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } 
+    };
+    Hop_Obj_t * pObj;
+    unsigned * pTruth, * pTruth2;
+    int i, nWords, nNodes;
+    Vec_Ptr_t * vTtElems;
+
+    // if the number of variables is more than 8, allocate truth tables
+    if ( nVars > 8 )
+        vTtElems = Vec_PtrAllocTruthTables( nVars );
+    else
+        vTtElems = NULL;
+
+    // clear the data fields and set marks
+    nNodes = Hop_ManConvertAigToTruth_rec1( pRoot );
+    // prepare memory
+    nWords = Hop_TruthWordNum( nVars );
+    Vec_IntClear( vTruth );
+    Vec_IntGrow( vTruth, nWords * (nNodes+1) );
+    pTruth = Vec_IntFetch( vTruth, nWords );
+    // check the case of a constant
+    if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
+    {
+        assert( nNodes == 0 );
+        if ( Hop_IsComplement(pRoot) )
+            Hop_ManTruthClear( pTruth, nVars );
+        else
+            Hop_ManTruthFill( pTruth, nVars );
+        return pTruth;
+    }
+    // set elementary truth tables at the leaves
+    assert( nVars <= Hop_ManPiNum(p) );
+//    assert( Hop_ManPiNum(p) <= 8 ); 
+    if ( fMsbFirst )
+    {
+        Hop_ManForEachPi( p, pObj, i )
+        {
+            if ( vTtElems )
+                pObj->pData = Vec_PtrEntry(vTtElems, nVars-1-i);
+            else               
+                pObj->pData = (void *)uTruths[nVars-1-i];
+        }
+    }
+    else
+    {
+        Hop_ManForEachPi( p, pObj, i )
+        {
+            if ( vTtElems )
+                pObj->pData = Vec_PtrEntry(vTtElems, i);
+            else               
+                pObj->pData = (void *)uTruths[i];
+        }
+    }
+    // clear the marks and compute the truth table
+    pTruth2 = Hop_ManConvertAigToTruth_rec2( pRoot, vTruth, nWords );
+    // copy the result
+    Hop_ManTruthCopy( pTruth, pTruth2, nVars );
+    if ( vTtElems )
+        Vec_PtrFree( vTtElems );
+    return pTruth;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/hop/hop_.c b/src/aig/hop/hop_.c
index 468413fa..658b8c4e 100644
--- a/src/aig/hop/hop_.c
+++ b/src/aig/hop/hop_.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [ivy_.c]
+  FileName    [hop_.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,11 +14,11 @@
 
   Date        [Ver. 1.0. Started - May 11, 2006.]
 
-  Revision    [$Id: ivy_.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+  Revision    [$Id: hop_.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
-#include "ivy.h"
+#include "hop.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
diff --git a/src/aig/hop/module.make b/src/aig/hop/module.make
index b06d91fd..e60ec4e8 100644
--- a/src/aig/hop/module.make
+++ b/src/aig/hop/module.make
@@ -6,4 +6,5 @@ SRC +=    src/aig/hop/hopBalance.c \
     src/aig/hop/hopObj.c \
     src/aig/hop/hopOper.c \
     src/aig/hop/hopTable.c \
+    src/aig/hop/hopTruth.c \
     src/aig/hop/hopUtil.c 
diff --git a/src/aig/ntk/module.make b/src/aig/ntk/module.make
new file mode 100644
index 00000000..b668de2f
--- /dev/null
+++ b/src/aig/ntk/module.make
@@ -0,0 +1,9 @@
+SRC +=    src/aig/ntk/ntkCheck.c \
+    src/aig/ntk/ntkBidec.c \
+    src/aig/ntk/ntkDfs.c \
+    src/aig/ntk/ntkFanio.c \
+    src/aig/ntk/ntkMan.c \
+    src/aig/ntk/ntkMap.c \
+    src/aig/ntk/ntkObj.c \
+    src/aig/ntk/ntkTiming.c \
+    src/aig/ntk/ntkUtil.c
diff --git a/src/aig/ntk/ntk.h b/src/aig/ntk/ntk.h
index 6ddfac81..2fcb6ddc 100644
--- a/src/aig/ntk/ntk.h
+++ b/src/aig/ntk/ntk.h
@@ -30,7 +30,9 @@ extern "C" {
 ////////////////////////////////////////////////////////////////////////
 
 #include "aig.h"
+#include "hop.h"
 #include "tim.h"
+#include "if.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -66,7 +68,7 @@ struct Ntk_Man_t_
     int                nObjs[NTK_OBJ_VOID]; // counter of objects of each type
     int                nFanioPlus;     // the number of extra fanins/fanouts alloc by default
     // functionality, timing, memory, etc
-    Aig_Man_t *        pAig;           // the functionality representation
+    Hop_Man_t *        pManHop;        // the functionality representation
     Tim_Man_t *        pManTime;       // the timing manager
     Aig_MmFlex_t *     pMemObjs;       // memory for objects
     Vec_Ptr_t *        vTemp;          // array used for incremental updates
@@ -77,9 +79,10 @@ struct Ntk_Obj_t_
 {
     Ntk_Man_t *        pMan;           // the manager  
     void *             pCopy;          // temporary pointer
-    void *             pFunc;          // functionality
+    Hop_Obj_t *        pFunc;          // functionality
     // node information
     int                Id;             // unique ID
+    int                PioId;          // number of this node in the PI/PO list
     unsigned           Type     :  3;  // object type
     unsigned           fCompl   :  1;  // complemented attribute
     unsigned           MarkA    :  1;  // temporary mark  
@@ -113,6 +116,10 @@ static inline int         Ntk_ManLatchNum( Ntk_Man_t * p )        { return p->nO
 static inline int         Ntk_ManBoxNum( Ntk_Man_t * p )          { return p->nObjs[NTK_OBJ_BOX];               } 
 static inline int         Ntk_ManObjNumMax( Ntk_Man_t * p )       { return Vec_PtrSize(p->vObjs);               }
 
+static inline Ntk_Obj_t * Ntk_ManCi( Ntk_Man_t * p, int i )       { return Vec_PtrEntry( p->vCis, i );          } 
+static inline Ntk_Obj_t * Ntk_ManCo( Ntk_Man_t * p, int i )       { return Vec_PtrEntry( p->vCos, i );          } 
+static inline Ntk_Obj_t * Ntk_ManObj( Ntk_Man_t * p, int i )      { return Vec_PtrEntry( p->vObjs, i );         } 
+
 static inline int         Ntk_ObjFaninNum( Ntk_Obj_t * p )        { return p->nFanins;                          } 
 static inline int         Ntk_ObjFanoutNum( Ntk_Obj_t * p )       { return p->nFanouts;                         } 
 
@@ -126,8 +133,8 @@ static inline int         Ntk_ObjIsCo( Ntk_Obj_t * p )            { return p->Ty
 static inline int         Ntk_ObjIsNode( Ntk_Obj_t * p )          { return p->Type == NTK_OBJ_NODE;             } 
 static inline int         Ntk_ObjIsLatch( Ntk_Obj_t * p )         { return p->Type == NTK_OBJ_LATCH;            } 
 static inline int         Ntk_ObjIsBox( Ntk_Obj_t * p )           { return p->Type == NTK_OBJ_BOX;              } 
-static inline int         Ntk_ObjIsPi( Ntk_Obj_t * p )            { return Ntk_ObjFaninNum(p) == 0 || (Ntk_ObjFaninNum(p) == 1 && Ntk_ObjIsLatch(Ntk_ObjFanin0(p)));   } 
-static inline int         Ntk_ObjIsPo( Ntk_Obj_t * p )            { return Ntk_ObjFanoutNum(p)== 0 || (Ntk_ObjFanoutNum(p)== 1 && Ntk_ObjIsLatch(Ntk_ObjFanout0(p)));  } 
+static inline int         Ntk_ObjIsPi( Ntk_Obj_t * p )            { return Ntk_ObjIsCi(p) && Tim_ManBoxForCi(p->pMan->pManTime, p->PioId) == -1; } 
+static inline int         Ntk_ObjIsPo( Ntk_Obj_t * p )            { return Ntk_ObjIsCo(p) && Tim_ManBoxForCo(p->pMan->pManTime, p->PioId) == -1;  }
 
 static inline float       Ntk_ObjArrival( Ntk_Obj_t * pObj )                 { return pObj->tArrival;           }
 static inline float       Ntk_ObjRequired( Ntk_Obj_t * pObj )                { return pObj->tRequired;          }
@@ -181,42 +188,41 @@ static inline int         Ntk_ObjIsTravIdPrevious( Ntk_Obj_t * pObj )        { r
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/*=== ntlDfs.c ==========================================================*/
+/*=== ntkDfs.c ==========================================================*/
+extern int             Ntk_ManLevel( Ntk_Man_t * pNtk );
+extern int             Ntk_ManLevel2( Ntk_Man_t * pNtk );
 extern Vec_Ptr_t *     Ntk_ManDfs( Ntk_Man_t * pNtk );
 extern Vec_Ptr_t *     Ntk_ManDfsReverse( Ntk_Man_t * pNtk );
-/*=== ntlFanio.c ==========================================================*/
+/*=== ntkFanio.c ==========================================================*/
 extern void            Ntk_ObjCollectFanins( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes );
 extern void            Ntk_ObjCollectFanouts( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes );
 extern void            Ntk_ObjAddFanin( Ntk_Obj_t * pObj, Ntk_Obj_t * pFanin );
 extern void            Ntk_ObjDeleteFanin( Ntk_Obj_t * pObj, Ntk_Obj_t * pFanin );
 extern void            Ntk_ObjPatchFanin( Ntk_Obj_t * pObj, Ntk_Obj_t * pFaninOld, Ntk_Obj_t * pFaninNew );
 extern void            Ntk_ObjReplace( Ntk_Obj_t * pNodeOld, Ntk_Obj_t * pNodeNew );
-/*=== ntlMan.c ============================================================*/
+/*=== ntkMan.c ============================================================*/
 extern Ntk_Man_t *     Ntk_ManAlloc();
 extern void            Ntk_ManFree( Ntk_Man_t * p );
-extern void            Ntk_ManPrintStats( Ntk_Man_t * p );
-/*=== ntlMap.c ============================================================*/
-extern Ntk_Man_t *     Ntk_MappingIf( Aig_Man_t * p, void * pPars );
-/*=== ntlObj.c ============================================================*/
-extern Ntk_Obj_t *     Ntk_ManCreatePi( Ntk_Man_t * pMan );
-extern Ntk_Obj_t *     Ntk_ManCreatePo( Ntk_Man_t * pMan );
+extern void            Ntk_ManPrintStats( Ntk_Man_t * p, If_Lib_t * pLutLib );
+/*=== ntkMap.c ============================================================*/
+/*=== ntkObj.c ============================================================*/
+extern Ntk_Obj_t *     Ntk_ManCreateCi( Ntk_Man_t * pMan, int nFanouts );
+extern Ntk_Obj_t *     Ntk_ManCreateCo( Ntk_Man_t * pMan );
 extern Ntk_Obj_t *     Ntk_ManCreateNode( Ntk_Man_t * pMan, int nFanins, int nFanouts );
 extern Ntk_Obj_t *     Ntk_ManCreateBox( Ntk_Man_t * pMan, int nFanins, int nFanouts );
 extern Ntk_Obj_t *     Ntk_ManCreateLatch( Ntk_Man_t * pMan );
 extern void            Ntk_ManDeleteNode( Ntk_Obj_t * pObj );
 extern void            Ntk_ManDeleteNode_rec( Ntk_Obj_t * pObj );
-/*=== ntlUtil.c ============================================================*/
+/*=== ntkTiming.c ============================================================*/
+extern float           Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, If_Lib_t * pLutLib );
+extern void            Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, If_Lib_t * pLutLib );
+/*=== ntkUtil.c ============================================================*/
 extern void            Ntk_ManIncrementTravId( Ntk_Man_t * pNtk );
 extern int             Ntk_ManGetFaninMax( Ntk_Man_t * pNtk );
 extern int             Ntk_ManGetTotalFanins( Ntk_Man_t * pNtk );
-extern int             Ntk_ManLevel( Ntk_Man_t * pNtk );
 extern int             Ntk_ManPiNum( Ntk_Man_t * pNtk );
 extern int             Ntk_ManPoNum( Ntk_Man_t * pNtk );
-
-/*=== ntlReadBlif.c ==========================================================*/
-extern Ntk_Man_t *     Ioa_ReadBlif( char * pFileName, int fCheck );
-/*=== ntlWriteBlif.c ==========================================================*/
-extern void            Ioa_WriteBlif( Ntk_Man_t * p, char * pFileName );
+extern int             Ntk_ManGetAigNodeNum( Ntk_Man_t * pNtk );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/ntk/ntkBidec.c b/src/aig/ntk/ntkBidec.c
new file mode 100644
index 00000000..43426d13
--- /dev/null
+++ b/src/aig/ntk/ntkBidec.c
@@ -0,0 +1,123 @@
+/**CFile****************************************************************
+
+  FileName    [ntkBidec.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Bi-decomposition of local functions.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntkBidec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntk.h"
+#include "bdc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj )  { return Hop_NotCond( Bdc_FuncCopy(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) );  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Resynthesizes nodes using bi-decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Ntk_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare )
+{
+    unsigned * pTruth;
+    Bdc_Fun_t * pFunc;
+    int nNodes, i;
+    assert( nVars <= 16 );
+    // derive truth table
+    pTruth = Hop_ManConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 );
+    if ( Hop_IsComplement(pRoot) )
+        for ( i = Aig_TruthWordNum(nVars)-1; i >= 0; i-- )
+            pTruth[i] = ~pTruth[i];
+    // decompose truth table
+    Bdc_ManDecompose( p, pTruth, puCare, nVars, NULL, 1000 );
+    // convert back into HOP
+    Bdc_FuncSetCopy( Bdc_ManFunc( p, 0 ), Hop_ManConst1( pHop ) );
+    for ( i = 0; i < nVars; i++ )
+        Bdc_FuncSetCopy( Bdc_ManFunc( p, i+1 ), Hop_ManPi( pHop, i ) );
+    nNodes = Bdc_ManNodeNum(p);
+    for ( i = nVars + 1; i < nNodes; i++ )
+    {
+        pFunc = Bdc_ManFunc( p, i );
+        Bdc_FuncSetCopy( pFunc, Hop_And( pHop, Bdc_FunCopyHop(Bdc_FuncFanin0(pFunc)), Bdc_FunCopyHop(Bdc_FuncFanin1(pFunc)) ) );
+    }
+    return Bdc_FunCopyHop( Bdc_ManRoot(p) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resynthesizes nodes using bi-decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ManBidecResyn( Ntk_Man_t * pNtk, int fVerbose )
+{
+    Bdc_Par_t Pars = {0}, * pPars = &Pars;
+    Bdc_Man_t * p;
+    Ntk_Obj_t * pObj;
+    Vec_Int_t * vTruth;
+    int i, nGainTotal = 0, nNodes1, nNodes2;
+    int clk = clock();
+    pPars->nVarsMax = Ntk_ManGetFaninMax( pNtk );
+    pPars->fVerbose = fVerbose;
+    if ( pPars->nVarsMax > 15 )
+    {
+        if ( fVerbose )
+        printf( "Resynthesis is not performed for nodes with more than 15 inputs.\n" );
+        pPars->nVarsMax = 15;
+    }
+    vTruth = Vec_IntAlloc( 0 );
+    p = Bdc_ManAlloc( pPars );
+    Ntk_ManForEachNode( pNtk, pObj, i )
+    {
+        if ( Ntk_ObjFaninNum(pObj) > 15 )
+            continue;
+        nNodes1 = Hop_DagSize(pObj->pFunc);
+        pObj->pFunc = Ntk_NodeIfNodeResyn( p, pNtk->pManHop, pObj->pFunc, Ntk_ObjFaninNum(pObj), vTruth, NULL );
+        nNodes2 = Hop_DagSize(pObj->pFunc);
+        nGainTotal += nNodes1 - nNodes2;
+    }
+    Bdc_ManFree( p );
+    Vec_IntFree( vTruth );
+    if ( fVerbose )
+    {
+    printf( "Total gain in AIG nodes = %d.  ", nGainTotal );
+    PRT( "Total runtime", clock() - clk );
+    }
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntk/ntkCheck.c b/src/aig/ntk/ntkCheck.c
new file mode 100644
index 00000000..6bbb67a6
--- /dev/null
+++ b/src/aig/ntk/ntkCheck.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+  FileName    [ntk_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntk_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntk.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntk/ntkDfs.c b/src/aig/ntk/ntkDfs.c
index ce176898..263a2740 100644
--- a/src/aig/ntk/ntkDfs.c
+++ b/src/aig/ntk/ntkDfs.c
@@ -30,6 +30,62 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
+
+  Description [Assumes that white boxes have unit level.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntk_ManLevel( Ntk_Man_t * pNtk )
+{
+    Tim_Man_t * pManTimeUnit;
+    Ntk_Obj_t * pObj, * pFanin;
+    int i, k, LevelMax, Level;
+    // clean the levels
+    Ntk_ManForEachObj( pNtk, pObj, i )
+        Ntk_ObjSetLevel( pObj, 0 );
+    // perform level computation
+    LevelMax = 0;
+    pManTimeUnit = Tim_ManDupUnit( pNtk->pManTime );
+    Tim_ManIncrementTravId( pManTimeUnit );
+    Ntk_ManForEachObj( pNtk, pObj, i )
+    {
+        if ( Ntk_ObjIsCi(pObj) )
+        {
+            Level = (int)Tim_ManGetPiArrival( pManTimeUnit, pObj->PioId );
+            Ntk_ObjSetLevel( pObj, Level );
+        }
+        else if ( Ntk_ObjIsCo(pObj) )
+        {
+            Level = Ntk_ObjLevel( Ntk_ObjFanin0(pObj) );
+            Tim_ManSetPoArrival( pManTimeUnit, pObj->PioId, (float)Level );
+            Ntk_ObjSetLevel( pObj, Level );
+            if ( LevelMax < Ntk_ObjLevel(pObj) )
+                LevelMax = Ntk_ObjLevel(pObj);
+        }
+        else if ( Ntk_ObjIsNode(pObj) )
+        {
+            Level = 0;
+            Ntk_ObjForEachFanin( pObj, pFanin, k )
+                if ( Level < Ntk_ObjLevel(pFanin) )
+                    Level = Ntk_ObjLevel(pFanin);
+            Ntk_ObjSetLevel( pObj, Level + 1 );
+        }
+        else
+            assert( 0 );
+    }
+    // set the old timing manager
+    Tim_ManStop( pManTimeUnit );
+    return LevelMax;
+}
+
+
+
+/**Function*************************************************************
+
   Synopsis    [Performs DFS for one node.]
 
   Description []
@@ -39,16 +95,96 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Ntk_ManDfs_rec( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes )
+void Ntk_ManLevel2_rec( Ntk_Obj_t * pObj )
+{
+    Ntk_Obj_t * pNext;
+    int i, iBox, iTerm1, nTerms, LevelMax = 0;
+    if ( Ntk_ObjIsTravIdCurrent( pObj ) )
+        return;
+    Ntk_ObjSetTravIdCurrent( pObj );
+    if ( Ntk_ObjIsCi(pObj) )
+    {
+        iBox = Tim_ManBoxForCi( pObj->pMan->pManTime, pObj->PioId );
+        if ( iBox >= 0 ) // this is not a true PI
+        {
+            iTerm1 = Tim_ManBoxInputFirst( pObj->pMan->pManTime, iBox );
+            nTerms = Tim_ManBoxInputNum( pObj->pMan->pManTime, iBox );
+            for ( i = 0; i < nTerms; i++ )
+            {
+                pNext = Ntk_ManCo(pObj->pMan, iTerm1 + i);
+                Ntk_ManLevel2_rec( pNext );
+                if ( LevelMax < Ntk_ObjLevel(pNext) )
+                    LevelMax = Ntk_ObjLevel(pNext);
+            }
+            LevelMax++;
+        }
+    }
+    else if ( Ntk_ObjIsNode(pObj) || Ntk_ObjIsCo(pObj) )
+    {
+        Ntk_ObjForEachFanin( pObj, pNext, i )
+        {
+            Ntk_ManLevel2_rec( pNext );
+            if ( LevelMax < Ntk_ObjLevel(pNext) )
+                LevelMax = Ntk_ObjLevel(pNext);
+        }
+        if ( Ntk_ObjIsNode(pObj) )
+            LevelMax++;
+    }
+    else
+        assert( 0 );
+    Ntk_ObjSetLevel( pObj, LevelMax );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the DFS ordered array of all objects except latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntk_ManLevel2( Ntk_Man_t * pNtk )
+{
+    Ntk_Obj_t * pObj;
+    int i, LevelMax = 0;
+    Ntk_ManForEachObj( pNtk, pObj, i )
+        Ntk_ObjSetLevel( pObj, 0 );
+    Ntk_ManIncrementTravId( pNtk );
+    Ntk_ManForEachPo( pNtk, pObj, i )
+    {
+        Ntk_ManLevel2_rec( pObj );
+        if ( LevelMax < Ntk_ObjLevel(pObj) )
+            LevelMax = Ntk_ObjLevel(pObj);
+    }
+    return LevelMax;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DFS for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ManDfs_rec( Ntk_Obj_t * pObj, Vec_Ptr_t * vNodes )
 {
     Ntk_Obj_t * pNext;
     int i;
-    if ( Ntk_ObjIsTravIdCurrent( pNode ) )
+    if ( Ntk_ObjIsTravIdCurrent( pObj ) )
         return;
-    Ntk_ObjSetTravIdCurrent( pNode );
-    Ntk_ObjForEachFanin( pNode, pNext, i )
+    Ntk_ObjSetTravIdCurrent( pObj );
+    Ntk_ObjForEachFanin( pObj, pNext, i )
         Ntk_ManDfs_rec( pNext, vNodes );
-    Vec_PtrPush( vNodes, pNode );
+    Vec_PtrPush( vNodes, pObj );
 }
 
 /**Function*************************************************************
@@ -69,8 +205,16 @@ Vec_Ptr_t * Ntk_ManDfs( Ntk_Man_t * pNtk )
     int i;
     Ntk_ManIncrementTravId( pNtk );
     vNodes = Vec_PtrAlloc( 100 );
-    Ntk_ManForEachPo( pNtk, pObj, i )
-        Ntk_ManDfs_rec( pObj, vNodes );
+    Ntk_ManForEachObj( pNtk, pObj, i )
+    {
+        if ( Ntk_ObjIsCi(pObj) )
+        {
+            Ntk_ObjSetTravIdCurrent( pObj );
+            Vec_PtrPush( vNodes, pObj );
+        }
+        else if ( Ntk_ObjIsCo(pObj) )
+            Ntk_ManDfs_rec( pObj, vNodes );
+    }
     return vNodes;
 }
 
@@ -85,16 +229,35 @@ Vec_Ptr_t * Ntk_ManDfs( Ntk_Man_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Ntk_ManDfsReverse_rec( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes )
+void Ntk_ManDfsReverse_rec( Ntk_Obj_t * pObj, Vec_Ptr_t * vNodes )
 {
     Ntk_Obj_t * pNext;
-    int i;
-    if ( Ntk_ObjIsTravIdCurrent( pNode ) )
+    int i, iBox, iTerm1, nTerms;
+    if ( Ntk_ObjIsTravIdCurrent( pObj ) )
         return;
-    Ntk_ObjSetTravIdCurrent( pNode );
-    Ntk_ObjForEachFanout( pNode, pNext, i )
-        Ntk_ManDfsReverse_rec( pNext, vNodes );
-    Vec_PtrPush( vNodes, pNode );
+    Ntk_ObjSetTravIdCurrent( pObj );
+    if ( Ntk_ObjIsCo(pObj) )
+    {
+        iBox = Tim_ManBoxForCo( pObj->pMan->pManTime, pObj->PioId );
+        if ( iBox >= 0 ) // this is not a true PO
+        {
+            iTerm1 = Tim_ManBoxOutputFirst( pObj->pMan->pManTime, iBox );
+            nTerms = Tim_ManBoxOutputNum( pObj->pMan->pManTime, iBox );
+            for ( i = 0; i < nTerms; i++ )
+            {
+                pNext = Ntk_ManCi(pObj->pMan, iTerm1 + i);
+                Ntk_ManDfsReverse_rec( pNext, vNodes );
+            }
+        }
+    }
+    else if ( Ntk_ObjIsNode(pObj) || Ntk_ObjIsCi(pObj) )
+    {
+        Ntk_ObjForEachFanout( pObj, pNext, i )
+            Ntk_ManDfsReverse_rec( pNext, vNodes );
+    }
+    else
+        assert( 0 );
+    Vec_PtrPush( vNodes, pObj );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/ntk/ntkFanio.c b/src/aig/ntk/ntkFanio.c
index 73019231..135929af 100644
--- a/src/aig/ntk/ntkFanio.c
+++ b/src/aig/ntk/ntkFanio.c
@@ -279,7 +279,7 @@ void Ntk_ObjTransferFanout( Ntk_Obj_t * pNodeFrom, Ntk_Obj_t * pNodeTo )
     Vec_Ptr_t * vFanouts = pNodeFrom->pMan->vTemp;
     Ntk_Obj_t * pTemp;
     int nFanoutsOld, i;
-    assert( !Ntk_ObjIsPo(pNodeFrom) && !Ntk_ObjIsPo(pNodeTo) );
+    assert( !Ntk_ObjIsCo(pNodeFrom) && !Ntk_ObjIsCo(pNodeTo) );
     assert( pNodeFrom->pMan == pNodeTo->pMan );
     assert( pNodeFrom != pNodeTo );
     assert( Ntk_ObjFanoutNum(pNodeFrom) > 0 );
diff --git a/src/aig/ntk/ntkMan.c b/src/aig/ntk/ntkMan.c
index e302a98c..1a077495 100644
--- a/src/aig/ntk/ntkMan.c
+++ b/src/aig/ntk/ntkMan.c
@@ -50,6 +50,7 @@ Ntk_Man_t * Ntk_ManAlloc()
     p->vTemp = Vec_PtrAlloc( 1000 );
     p->nFanioPlus = 4;
     p->pMemObjs = Aig_MmFlexStart();
+    p->pManHop = Hop_ManStart();
     return p;
 }
 
@@ -72,9 +73,9 @@ void Ntk_ManFree( Ntk_Man_t * p )
     if ( p->vCos )     Vec_PtrFree( p->vCos );
     if ( p->vObjs )    Vec_PtrFree( p->vObjs );
     if ( p->vTemp )    Vec_PtrFree( p->vTemp );
-    if ( p->pAig )     Aig_ManStop( p->pAig );
     if ( p->pManTime ) Tim_ManStop( p->pManTime );
     if ( p->pMemObjs ) Aig_MmFlexStop( p->pMemObjs, 0 );
+    if ( p->pManHop )  Hop_ManStop( p->pManHop );
     free( p );
 }
 
@@ -89,7 +90,7 @@ void Ntk_ManFree( Ntk_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Ntk_ManPrintStats( Ntk_Man_t * p )
+void Ntk_ManPrintStats( Ntk_Man_t * p, If_Lib_t * pLutLib )
 {
     printf( "%-15s : ",      p->pName );
     printf( "pi = %5d  ",    Ntk_ManPiNum(p) );
@@ -97,10 +98,15 @@ void Ntk_ManPrintStats( Ntk_Man_t * p )
     printf( "ci = %5d  ",    Ntk_ManCiNum(p) );
     printf( "co = %5d  ",    Ntk_ManCoNum(p) );
     printf( "lat = %5d  ",   Ntk_ManLatchNum(p) );
-    printf( "box = %5d  ",   Ntk_ManBoxNum(p) );
+//    printf( "box = %5d  ",   Ntk_ManBoxNum(p) );
     printf( "node = %5d  ",  Ntk_ManNodeNum(p) );
-    printf( "aig = %6d  ",   Aig_ManNodeNum(p->pAig) );
+    printf( "aig = %6d  ",   Ntk_ManGetAigNodeNum(p) );
+    printf( "lev = %3d  ",   Ntk_ManLevel(p) );
+    printf( "lev2 = %3d  ",  Ntk_ManLevel2(p) );
+    printf( "delay = %5.2f", Ntk_ManDelayTraceLut(p, pLutLib) );
     printf( "\n" );
+
+    Ntk_ManDelayTracePrint( p, pLutLib );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntk/ntkMap.c b/src/aig/ntk/ntkMap.c
index 7700fc63..9c780498 100644
--- a/src/aig/ntk/ntkMap.c
+++ b/src/aig/ntk/ntkMap.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "ntk.h"
+#include "if.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -30,6 +31,209 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Load the network into FPGA manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ManSetIfParsDefault( If_Par_t * pPars )
+{
+//    extern void * Abc_FrameReadLibLut();
+    // set defaults
+    memset( pPars, 0, sizeof(If_Par_t) );
+    // user-controlable paramters
+//    pPars->nLutSize    = -1;
+    pPars->nLutSize    =  6;
+    pPars->nCutsMax    =  8;
+    pPars->nFlowIters  =  1;
+    pPars->nAreaIters  =  2;
+    pPars->DelayTarget = -1;
+    pPars->Epsilon     =  (float)0.01;
+    pPars->fPreprocess =  1;
+    pPars->fArea       =  0;
+    pPars->fFancy      =  0;
+    pPars->fExpRed     =  0;
+    pPars->fLatchPaths =  0;
+    pPars->fEdge       =  1;
+    pPars->fCutMin     =  1;
+    pPars->fSeqMap     =  0;
+    pPars->fVerbose    =  1;
+    // internal parameters
+    pPars->fTruth      =  0;
+    pPars->nLatches    =  0;
+    pPars->fLiftLeaves =  0;
+//    pPars->pLutLib     =  Abc_FrameReadLibLut();
+    pPars->pLutLib     =  NULL;
+    pPars->pTimesArr   =  NULL; 
+    pPars->pTimesArr   =  NULL;   
+    pPars->pFuncCost   =  NULL;   
+/*
+    if ( pPars->nLutSize == -1 )
+    {
+        if ( pPars->pLutLib == NULL )
+        {
+            printf( "The LUT library is not given.\n" );
+            return;
+        }
+        // get LUT size from the library
+        pPars->nLutSize = pPars->pLutLib->LutMax;
+    }
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Load the network into FPGA manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
+{
+    If_Man_t * pIfMan;
+    Aig_Obj_t * pNode;//, * pFanin, * pPrev;
+    int i;
+    // start the mapping manager and set its parameters
+    pIfMan = If_ManStart( pPars );
+    // print warning about excessive memory usage
+//    if ( 1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30) > 1.0 )
+//        printf( "Warning: The mapper will allocate %.1f Gb for to represent the subject graph with %d AIG nodes.\n", 
+//            1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30), Aig_ManObjNum(p) );
+    // load the AIG into the mapper
+    Aig_ManForEachObj( p, pNode, i )
+    {
+        if ( Aig_ObjIsAnd(pNode) )
+            pNode->pData = (Aig_Obj_t *)If_ManCreateAnd( pIfMan, 
+                If_NotCond( (If_Obj_t *)Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ), 
+                If_NotCond( (If_Obj_t *)Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) );
+        else if ( Aig_ObjIsPi(pNode) )
+        {
+            pNode->pData = If_ManCreateCi( pIfMan );
+            ((If_Obj_t *)pNode->pData)->Level = pNode->Level;
+            if ( pIfMan->nLevelMax < (int)pNode->Level )
+                pIfMan->nLevelMax = (int)pNode->Level;
+        }
+        else if ( Aig_ObjIsPo(pNode) )
+            pNode->pData = If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
+        else if ( Aig_ObjIsConst1(pNode) )
+            Aig_ManConst1(p)->pData = If_ManConst1( pIfMan );
+        else // add the node to the mapper
+            assert( 0 );
+        // set up the choice node
+//        if ( Aig_AigNodeIsChoice( pNode ) )
+//        {
+//            pIfMan->nChoices++;
+//            for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
+//                If_ObjSetChoice( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData );
+//            If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pData );
+//        }
+        {
+            If_Obj_t * pIfObj = pNode->pData;
+            assert( !If_IsComplement(pIfObj) );
+            assert( pIfObj->Id == pNode->Id );
+        }
+    }
+    return pIfMan;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively derives the truth table for the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Ntk_NodeIfToHop2_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited )
+{
+    If_Cut_t * pCut;
+    If_Obj_t * pTemp;
+    Hop_Obj_t * gFunc, * gFunc0, * gFunc1;
+    // get the best cut
+    pCut = If_ObjCutBest(pIfObj);
+    // if the cut is visited, return the result
+    if ( If_CutData(pCut) )
+        return If_CutData(pCut);
+    // mark the node as visited
+    Vec_PtrPush( vVisited, pCut );
+    // insert the worst case
+    If_CutSetData( pCut, (void *)1 );
+    // skip in case of primary input
+    if ( If_ObjIsCi(pIfObj) )
+        return If_CutData(pCut);
+    // compute the functions of the children
+    for ( pTemp = pIfObj; pTemp; pTemp = pTemp->pEquiv )
+    {
+        gFunc0 = Ntk_NodeIfToHop2_rec( pHopMan, pIfMan, pTemp->pFanin0, vVisited );
+        if ( gFunc0 == (void *)1 )
+            continue;
+        gFunc1 = Ntk_NodeIfToHop2_rec( pHopMan, pIfMan, pTemp->pFanin1, vVisited );
+        if ( gFunc1 == (void *)1 )
+            continue;
+        // both branches are solved
+        gFunc = Hop_And( pHopMan, Hop_NotCond(gFunc0, pTemp->fCompl0), Hop_NotCond(gFunc1, pTemp->fCompl1) ); 
+        if ( pTemp->fPhase != pIfObj->fPhase )
+            gFunc = Hop_Not(gFunc);
+        If_CutSetData( pCut, gFunc );
+        break;
+    }
+    return If_CutData(pCut);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the truth table for one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Ntk_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj )
+{
+    If_Cut_t * pCut;
+    Hop_Obj_t * gFunc;
+    If_Obj_t * pLeaf;
+    int i;
+    // get the best cut
+    pCut = If_ObjCutBest(pIfObj);
+    assert( pCut->nLeaves > 1 );
+    // set the leaf variables
+    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
+        If_CutSetData( If_ObjCutBest(pLeaf), Hop_IthVar(pHopMan, i) );
+    // recursively compute the function while collecting visited cuts
+    Vec_PtrClear( pIfMan->vTemp );
+    gFunc = Ntk_NodeIfToHop2_rec( pHopMan, pIfMan, pIfObj, pIfMan->vTemp ); 
+    if ( gFunc == (void *)1 )
+    {
+        printf( "Ntk_NodeIfToHop(): Computing local AIG has failed.\n" );
+        return NULL;
+    }
+//    printf( "%d ", Vec_PtrSize(p->vTemp) );
+    // clean the cuts
+    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
+        If_CutSetData( If_ObjCutBest(pLeaf), NULL );
+    Vec_PtrForEachEntry( pIfMan->vTemp, pCut, i )
+        If_CutSetData( pCut, NULL );
+    return gFunc;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -39,6 +243,95 @@
   SeeAlso     []
 
 ***********************************************************************/
+Ntk_Man_t * Ntk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p )
+{
+    Ntk_Man_t * pNtk;
+    Ntk_Obj_t * pObjNew;
+    Aig_Obj_t * pObj;
+    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) );
+    If_ManCleanCutData( pIfMan );
+    // construct the network
+    pNtk = Ntk_ManAlloc();
+    pNtk->pName = Aig_UtilStrsav( p->pName );
+    pNtk->pSpec = Aig_UtilStrsav( p->pSpec );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        pIfObj = If_ManObj( pIfMan, i );
+        if ( pIfObj->nRefs == 0 && !If_ObjIsTerm(pIfObj) )
+            continue;
+        if ( Aig_ObjIsNode(pObj) )
+        {
+            pCutBest = If_ObjCutBest( pIfObj );
+            nLeaves  = If_CutLeaveNum( pCutBest ); 
+            ppLeaves = If_CutLeaves( pCutBest );
+            // create node
+            pObjNew = Ntk_ManCreateNode( pNtk, nLeaves, pIfObj->nRefs );
+            for ( k = 0; k < nLeaves; k++ )
+                Ntk_ObjAddFanin( pObjNew, Aig_ManObj(p, ppLeaves[k])->pData );
+            // get the functionality
+            pObjNew->pFunc = Ntk_NodeIfToHop( pNtk->pManHop, pIfMan, pIfObj );
+        }
+        else if ( Aig_ObjIsPi(pObj) )
+            pObjNew = Ntk_ManCreateCi( pNtk, pIfObj->nRefs );
+        else if ( Aig_ObjIsPo(pObj) )
+        {
+            pObjNew = Ntk_ManCreateCo( pNtk );
+            pObjNew->fCompl = Aig_ObjFaninC0(pObj);
+            Ntk_ObjAddFanin( pObjNew, Aig_ObjFanin0(pObj)->pData );
+        }
+        else if ( Aig_ObjIsConst1(pObj) )
+        {
+            pObjNew = Ntk_ManCreateNode( pNtk, 0, pIfObj->nRefs );
+            pObjNew->pFunc = Hop_ManConst1( pNtk->pManHop );
+        }
+        else
+            assert( 0 );
+        pObj->pData = pObjNew;
+    }
+    pNtk->pManTime = Tim_ManDup( pIfMan->pManTim, 0 );
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Interface with the FPGA mapping package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntk_Man_t * Ntk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars )
+{
+    Ntk_Man_t * pNtk;
+    If_Man_t * pIfMan;
+    // perform FPGA mapping
+    // set the arrival times
+    pPars->pTimesArr = ALLOC( float, Aig_ManPiNum(p) );
+    memset( pPars->pTimesArr, 0, sizeof(float) * Aig_ManPiNum(p) );
+    // translate into the mapper
+    pIfMan = Ntk_ManToIf( p, pPars );    
+    if ( pIfMan == NULL )
+        return NULL;
+    pIfMan->pManTim = Tim_ManDup( pManTime, 0 );
+    if ( !If_ManPerformMapping( pIfMan ) )
+    {
+        If_ManStop( pIfMan );
+        return NULL;
+    }
+    // transform the result of mapping into the new network
+    pNtk = Ntk_ManFromIf( pIfMan, p );
+    If_ManStop( pIfMan );
+    return pNtk;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/ntk/ntkObj.c b/src/aig/ntk/ntkObj.c
index 259ed79d..7bd2f552 100644
--- a/src/aig/ntk/ntkObj.c
+++ b/src/aig/ntk/ntkObj.c
@@ -63,10 +63,11 @@ Ntk_Obj_t * Ntk_ManCreateObj( Ntk_Man_t * p, int nFanins, int nFanouts )
   SeeAlso     []
 
 ***********************************************************************/
-Ntk_Obj_t * Ntk_ManCreatePi( Ntk_Man_t * p )
+Ntk_Obj_t * Ntk_ManCreateCi( Ntk_Man_t * p, int nFanouts )
 {
     Ntk_Obj_t * pObj;
-    pObj = Ntk_ManCreateObj( p, 1, 1 );
+    pObj = Ntk_ManCreateObj( p, 1, nFanouts );
+    pObj->PioId = Vec_PtrSize( p->vCis );
     Vec_PtrPush( p->vCis, pObj );
     pObj->Type = NTK_OBJ_CI;
     p->nObjs[NTK_OBJ_CI]++;
@@ -84,10 +85,11 @@ Ntk_Obj_t * Ntk_ManCreatePi( Ntk_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Ntk_Obj_t * Ntk_ManCreatePo( Ntk_Man_t * p )
+Ntk_Obj_t * Ntk_ManCreateCo( Ntk_Man_t * p )
 {
     Ntk_Obj_t * pObj;
     pObj = Ntk_ManCreateObj( p, 1, 1 );
+    pObj->PioId = Vec_PtrSize( p->vCos );
     Vec_PtrPush( p->vCos, pObj );
     pObj->Type = NTK_OBJ_CO;
     p->nObjs[NTK_OBJ_CO]++;
@@ -200,7 +202,7 @@ void Ntk_ManDeleteNode_rec( Ntk_Obj_t * pObj )
 {
     Vec_Ptr_t * vNodes;
     int i;
-    assert( !Ntk_ObjIsPi(pObj) );
+    assert( !Ntk_ObjIsCi(pObj) );
     assert( Ntk_ObjFanoutNum(pObj) == 0 );
     vNodes = Vec_PtrAlloc( 100 );
     Ntk_ObjCollectFanins( pObj, vNodes );
diff --git a/src/aig/ntk/ntkTiming.c b/src/aig/ntk/ntkTiming.c
index f57c7987..ff867e02 100644
--- a/src/aig/ntk/ntkTiming.c
+++ b/src/aig/ntk/ntkTiming.c
@@ -19,7 +19,6 @@
 ***********************************************************************/
 
 #include "ntk.h"
-#include "if.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -108,19 +107,17 @@ void Ntk_ManDelayTraceSortPins( Ntk_Obj_t * pNode, int * pPinPerm, float * pPinD
   SeeAlso     []
 
 ***********************************************************************/
-float Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, int fUseLutLib )
+float Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, If_Lib_t * pLutLib )
 {
     int fUseSorting = 1;
     int pPinPerm[32];
     float pPinDelays[32];
-    If_Lib_t * pLutLib;
-    Ntk_Obj_t * pNode, * pFanin;
+    Ntk_Obj_t * pObj, * pFanin;
     Vec_Ptr_t * vNodes;
     float tArrival, tRequired, tSlack, * pDelays;
     int i, k;
 
     // get the library
-    pLutLib = fUseLutLib?  Abc_FrameReadLibLut() : NULL;
     if ( pLutLib && pLutLib->LutMax < Ntk_ManGetFaninMax(pNtk) )
     {
         printf( "The max LUT size (%d) is less than the max fanin count (%d).\n", 
@@ -128,107 +125,138 @@ float Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, int fUseLutLib )
         return -AIG_INFINITY;
     }
 
+    // compute the reverse order of all objects
+    vNodes = Ntk_ManDfsReverse( pNtk );
+
     // initialize the arrival times
     Abc_NtkPrepareTiming( pNtk );
 
     // propagate arrival times
-    vNodes = Ntk_ManDfs( pNtk );
-    Vec_PtrForEachEntry( vNodes, pNode, i )
+    Tim_ManIncrementTravId( pNtk->pManTime );
+    Ntk_ManForEachObj( pNtk, pObj, i )
     {
-        tArrival = -AIG_INFINITY;
-        if ( pLutLib == NULL )
-        {
-            Ntk_ObjForEachFanin( pNode, pFanin, k )
-                if ( tArrival < Ntk_ObjArrival(pFanin) + 1.0 )
-                    tArrival = Ntk_ObjArrival(pFanin) + 1.0;
-        }
-        else if ( !pLutLib->fVarPinDelays )
+        if ( Ntk_ObjIsNode(pObj) )
         {
-            pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)];
-            Ntk_ObjForEachFanin( pNode, pFanin, k )
-                if ( tArrival < Ntk_ObjArrival(pFanin) + pDelays[0] )
-                    tArrival = Ntk_ObjArrival(pFanin) + pDelays[0];
-        }
-        else
-        {
-            pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)];
-            if ( fUseSorting )
+            tArrival = -AIG_INFINITY;
+            if ( pLutLib == NULL )
             {
-                Ntk_ManDelayTraceSortPins( pNode, pPinPerm, pPinDelays );
-                Ntk_ObjForEachFanin( pNode, pFanin, k ) 
-                    if ( tArrival < Ntk_ObjArrival(Ntk_ObjFanin(pNode,pPinPerm[k])) + pDelays[k] )
-                        tArrival = Ntk_ObjArrival(Ntk_ObjFanin(pNode,pPinPerm[k])) + pDelays[k];
+                Ntk_ObjForEachFanin( pObj, pFanin, k )
+                    if ( tArrival < Ntk_ObjArrival(pFanin) + 1.0 )
+                        tArrival = Ntk_ObjArrival(pFanin) + 1.0;
+            }
+            else if ( !pLutLib->fVarPinDelays )
+            {
+                pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pObj)];
+                Ntk_ObjForEachFanin( pObj, pFanin, k )
+                    if ( tArrival < Ntk_ObjArrival(pFanin) + pDelays[0] )
+                        tArrival = Ntk_ObjArrival(pFanin) + pDelays[0];
             }
             else
             {
-                Ntk_ObjForEachFanin( pNode, pFanin, k )
-                    if ( tArrival < Ntk_ObjArrival(pFanin) + pDelays[k] )
-                        tArrival = Ntk_ObjArrival(pFanin) + pDelays[k];
+                pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pObj)];
+                if ( fUseSorting )
+                {
+                    Ntk_ManDelayTraceSortPins( pObj, pPinPerm, pPinDelays );
+                    Ntk_ObjForEachFanin( pObj, pFanin, k ) 
+                        if ( tArrival < Ntk_ObjArrival(Ntk_ObjFanin(pObj,pPinPerm[k])) + pDelays[k] )
+                            tArrival = Ntk_ObjArrival(Ntk_ObjFanin(pObj,pPinPerm[k])) + pDelays[k];
+                }
+                else
+                {
+                    Ntk_ObjForEachFanin( pObj, pFanin, k )
+                        if ( tArrival < Ntk_ObjArrival(pFanin) + pDelays[k] )
+                            tArrival = Ntk_ObjArrival(pFanin) + pDelays[k];
+                }
             }
+            if ( Ntk_ObjFaninNum(pObj) == 0 )
+                tArrival = 0.0;
         }
-        if ( Ntk_ObjFaninNum(pNode) == 0 )
-            tArrival = 0.0;
-        Ntk_ObjSetArrival( pNode, tArrival );
+        else if ( Ntk_ObjIsCi(pObj) )
+        {
+            tArrival = Tim_ManGetPiArrival( pNtk->pManTime, pObj->PioId );
+        }
+        else if ( Ntk_ObjIsCo(pObj) )
+        {
+            tArrival = Ntk_ObjArrival( Ntk_ObjFanin0(pObj) );
+            Tim_ManSetPoArrival( pNtk->pManTime, pObj->PioId, tArrival );
+        }
+        else
+            assert( 0 );
+        Ntk_ObjSetArrival( pObj, tArrival );
     }
-    Vec_PtrFree( vNodes );
 
     // get the latest arrival times
     tArrival = -AIG_INFINITY;
-    Ntk_ManForEachPo( pNtk, pNode, i )
-        if ( tArrival < Ntk_ObjArrival(Ntk_ObjFanin0(pNode)) )
-            tArrival = Ntk_ObjArrival(Ntk_ObjFanin0(pNode));
+    Ntk_ManForEachPo( pNtk, pObj, i )
+        if ( tArrival < Ntk_ObjArrival(Ntk_ObjFanin0(pObj)) )
+            tArrival = Ntk_ObjArrival(Ntk_ObjFanin0(pObj));
 
     // initialize the required times
-    Ntk_ManForEachPo( pNtk, pNode, i )
-        if ( Ntk_ObjRequired(Ntk_ObjFanin0(pNode)) > tArrival )
-            Ntk_ObjSetRequired( Ntk_ObjFanin0(pNode), tArrival );
+    Ntk_ManForEachPo( pNtk, pObj, i )
+        if ( Ntk_ObjRequired(Ntk_ObjFanin0(pObj)) > tArrival )
+            Ntk_ObjSetRequired( Ntk_ObjFanin0(pObj), tArrival );
 
     // propagate the required times
-    vNodes = Ntk_ManDfsReverse( pNtk );
-    Vec_PtrForEachEntry( vNodes, pNode, i )
+    Tim_ManIncrementTravId( pNtk->pManTime );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
     {
-        if ( pLutLib == NULL )
-        {
-            tRequired = Ntk_ObjRequired(pNode) - (float)1.0;
-            Ntk_ObjForEachFanin( pNode, pFanin, k )
-                if ( Ntk_ObjRequired(pFanin) > tRequired )
-                    Ntk_ObjSetRequired( pFanin, tRequired );
-        }
-        else if ( !pLutLib->fVarPinDelays )
-        {
-            pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)];
-            tRequired = Ntk_ObjRequired(pNode) - pDelays[0];
-            Ntk_ObjForEachFanin( pNode, pFanin, k )
-                if ( Ntk_ObjRequired(pFanin) > tRequired )
-                    Ntk_ObjSetRequired( pFanin, tRequired );
-        }
-        else 
+        if ( Ntk_ObjIsNode(pObj) )
         {
-            pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)];
-            if ( fUseSorting )
+            if ( pLutLib == NULL )
             {
-                Ntk_ManDelayTraceSortPins( pNode, pPinPerm, pPinDelays );
-                Ntk_ObjForEachFanin( pNode, pFanin, k )
-                {
-                    tRequired = Ntk_ObjRequired(pNode) - pDelays[k];
-                    if ( Ntk_ObjRequired(Ntk_ObjFanin(pNode,pPinPerm[k])) > tRequired )
-                        Ntk_ObjSetRequired( Ntk_ObjFanin(pNode,pPinPerm[k]), tRequired );
-                }
+                tRequired = Ntk_ObjRequired(pObj) - (float)1.0;
+                Ntk_ObjForEachFanin( pObj, pFanin, k )
+                    if ( Ntk_ObjRequired(pFanin) > tRequired )
+                        Ntk_ObjSetRequired( pFanin, tRequired );
             }
-            else
+            else if ( !pLutLib->fVarPinDelays )
             {
-                Ntk_ObjForEachFanin( pNode, pFanin, k )
-                {
-                    tRequired = Ntk_ObjRequired(pNode) - pDelays[k];
+                pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pObj)];
+                tRequired = Ntk_ObjRequired(pObj) - pDelays[0];
+                Ntk_ObjForEachFanin( pObj, pFanin, k )
                     if ( Ntk_ObjRequired(pFanin) > tRequired )
                         Ntk_ObjSetRequired( pFanin, tRequired );
+            }
+            else 
+            {
+                pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pObj)];
+                if ( fUseSorting )
+                {
+                    Ntk_ManDelayTraceSortPins( pObj, pPinPerm, pPinDelays );
+                    Ntk_ObjForEachFanin( pObj, pFanin, k )
+                    {
+                        tRequired = Ntk_ObjRequired(pObj) - pDelays[k];
+                        if ( Ntk_ObjRequired(Ntk_ObjFanin(pObj,pPinPerm[k])) > tRequired )
+                            Ntk_ObjSetRequired( Ntk_ObjFanin(pObj,pPinPerm[k]), tRequired );
+                    }
+                }
+                else
+                {
+                    Ntk_ObjForEachFanin( pObj, pFanin, k )
+                    {
+                        tRequired = Ntk_ObjRequired(pObj) - pDelays[k];
+                        if ( Ntk_ObjRequired(pFanin) > tRequired )
+                            Ntk_ObjSetRequired( pFanin, tRequired );
+                    }
                 }
             }
         }
+        else if ( Ntk_ObjIsCi(pObj) )
+        {
+            tRequired = Ntk_ObjRequired(pObj);
+            Tim_ManSetPiRequired( pNtk->pManTime, pObj->PioId, tRequired );
+        }
+        else if ( Ntk_ObjIsCo(pObj) )
+        {
+            tRequired = Tim_ManGetPoRequired( pNtk->pManTime, pObj->PioId );
+            if ( Ntk_ObjRequired(Ntk_ObjFanin0(pObj)) > tRequired )
+                Ntk_ObjSetRequired( Ntk_ObjFanin0(pObj), tRequired );
+        }
+
         // set slack for this object
-        tSlack = Ntk_ObjRequired(pNode) - Ntk_ObjArrival(pNode);
+        tSlack = Ntk_ObjRequired(pObj) - Ntk_ObjArrival(pObj);
         assert( tSlack + 0.001 > 0.0 );
-        Ntk_ObjSetSlack( pNode, tSlack < 0.0 ? 0.0 : tSlack );
+        Ntk_ObjSetSlack( pObj, tSlack < 0.0 ? 0.0 : tSlack );
     }
     Vec_PtrFree( vNodes );
     return tArrival;
@@ -236,52 +264,6 @@ float Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, int fUseLutLib )
 
 /**Function*************************************************************
 
-  Synopsis    [Determines timing-critical edges of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned Ntk_ManDelayTraceTCEdges( Ntk_Man_t * pNtk, Ntk_Obj_t * pNode, float tDelta, int fUseLutLib )
-{
-    int pPinPerm[32];
-    float pPinDelays[32];
-    If_Lib_t * pLutLib;
-    Ntk_Obj_t * pFanin;
-    unsigned uResult = 0;
-    float tRequired, * pDelays;
-    int k;
-    pLutLib = fUseLutLib?  Abc_FrameReadLibLut() : NULL;
-    tRequired = Ntk_ObjRequired(pNode);
-    if ( pLutLib == NULL )
-    {
-        Ntk_ObjForEachFanin( pNode, pFanin, k )
-            if ( tRequired < Ntk_ObjArrival(pFanin) + 1.0 + tDelta )
-                uResult |= (1 << k);
-    }
-    else if ( !pLutLib->fVarPinDelays )
-    {
-        pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)];
-        Ntk_ObjForEachFanin( pNode, pFanin, k )
-            if ( tRequired < Ntk_ObjArrival(pFanin) + pDelays[0] + tDelta )
-                uResult |= (1 << k);
-    }
-    else
-    {
-        pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)];
-        Ntk_ManDelayTraceSortPins( pNode, pPinPerm, pPinDelays );
-        Ntk_ObjForEachFanin( pNode, pFanin, k )
-            if ( tRequired < Ntk_ObjArrival(Ntk_ObjFanin(pNode,pPinPerm[k])) + pDelays[k] + tDelta )
-                uResult |= (1 << pPinPerm[k]);
-    }
-    return uResult;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Delay tracing of the LUT mapped network.]
 
   Description []
@@ -291,14 +273,12 @@ unsigned Ntk_ManDelayTraceTCEdges( Ntk_Man_t * pNtk, Ntk_Obj_t * pNode, float tD
   SeeAlso     []
 
 ***********************************************************************/
-void Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, int fUseLutLib, int fVerbose )
+void Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, If_Lib_t * pLutLib )
 {
     Ntk_Obj_t * pNode;
-    If_Lib_t * pLutLib;
     int i, Nodes, * pCounters;
     float tArrival, tDelta, nSteps, Num;
     // get the library
-    pLutLib = fUseLutLib?  Abc_FrameReadLibLut() : NULL;
     if ( pLutLib && pLutLib->LutMax < Ntk_ManGetFaninMax(pNtk) )
     {
         printf( "The max LUT size (%d) is less than the max fanin count (%d).\n", 
@@ -306,11 +286,11 @@ void Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, int fUseLutLib, int fVerbose )
         return;
     }
     // decide how many steps
-    nSteps = fUseLutLib ? 20 : Ntk_ManLevel(pNtk);
+    nSteps = pLutLib ? 20 : Ntk_ManLevel(pNtk);
     pCounters = ALLOC( int, nSteps + 1 );
     memset( pCounters, 0, sizeof(int)*(nSteps + 1) );
     // perform delay trace
-    tArrival = Ntk_ManDelayTraceLut( pNtk, fUseLutLib );
+    tArrival = Ntk_ManDelayTraceLut( pNtk, pLutLib );
     tDelta = tArrival / nSteps;
     // count how many nodes have slack in the corresponding intervals
     Ntk_ManForEachNode( pNtk, pNode, i )
@@ -318,17 +298,19 @@ void Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, int fUseLutLib, int fVerbose )
         if ( Ntk_ObjFaninNum(pNode) == 0 )
             continue;
         Num = Ntk_ObjSlack(pNode) / tDelta;
+        if ( Num > nSteps )
+            continue;
         assert( Num >=0 && Num <= nSteps );
         pCounters[(int)Num]++;
     }
     // print the results
-    printf( "Max delay = %6.2f. Delay trace using %s model:\n", tArrival, fUseLutLib? "LUT library" : "unit-delay" );
+    printf( "Max delay = %6.2f. Delay trace using %s model:\n", tArrival, pLutLib? "LUT library" : "unit-delay" );
     Nodes = 0;
     for ( i = 0; i < nSteps; i++ )
     {
         Nodes += pCounters[i];
-        printf( "%3d %s : %5d  (%6.2f %%)\n", fUseLutLib? 5*(i+1) : i+1, 
-            fUseLutLib? "%":"lev", Nodes, 100.0*Nodes/Ntk_ManNodeNum(pNtk) );
+        printf( "%3d %s : %5d  (%6.2f %%)\n", pLutLib? 5*(i+1) : i+1, 
+            pLutLib? "%":"lev", Nodes, 100.0*Nodes/Ntk_ManNodeNum(pNtk) );
     }
     free( pCounters );
 }
diff --git a/src/aig/ntk/ntkUtil.c b/src/aig/ntk/ntkUtil.c
index 543d1a60..931a26ee 100644
--- a/src/aig/ntk/ntkUtil.c
+++ b/src/aig/ntk/ntkUtil.c
@@ -95,36 +95,25 @@ int Ntk_ManGetTotalFanins( Ntk_Man_t * pNtk )
     return nFanins;
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
+  Synopsis    []
 
-  Description [Assumes topological ordering of the nodes.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_ManLevel( Ntk_Man_t * pNtk )
+int Ntk_ManPiNum( Ntk_Man_t * pNtk )
 {
-    Ntk_Obj_t * pObj, * pFanin;
-    int i, k, LevelMax;
-    Ntk_ManForEachPi( pNtk, pObj, i )
-        Ntk_ObjSetLevel( pObj, 0 );
-    Ntk_ManForEachNode( pNtk, pObj, i )
-    {
-        LevelMax = 0;
-        Ntk_ObjForEachFanin( pObj, pFanin, k )
-            if ( LevelMax < Ntk_ObjLevel(pFanin) )
-                LevelMax = Ntk_ObjLevel(pFanin);
-        Ntk_ObjSetLevel( pFanin, LevelMax+1 );
-    }
-    LevelMax = 0;
-    Ntk_ManForEachPo( pNtk, pObj, i )
-        if ( LevelMax < Ntk_ObjLevel(pObj) )
-            LevelMax = Ntk_ObjLevel(pObj);
-    return LevelMax;
+    Ntk_Obj_t * pNode;
+    int i, Counter = 0;
+    Ntk_ManForEachCi( pNtk, pNode, i )
+        Counter += Ntk_ObjIsPi( pNode );
+    return Counter;
 }
 
 /**Function*************************************************************
@@ -138,18 +127,18 @@ int Ntk_ManLevel( Ntk_Man_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_ManPiNum( Ntk_Man_t * pNtk )
+int Ntk_ManPoNum( Ntk_Man_t * pNtk )
 {
     Ntk_Obj_t * pNode;
     int i, Counter = 0;
-    Ntk_ManForEachPi( pNtk, pNode, i )
-        Counter++;
+    Ntk_ManForEachCo( pNtk, pNode, i )
+        Counter += Ntk_ObjIsPo( pNode );
     return Counter;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Reads the number of BDD nodes.]
 
   Description []
                
@@ -158,13 +147,22 @@ int Ntk_ManPiNum( Ntk_Man_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_ManPoNum( Ntk_Man_t * pNtk )
+int Ntk_ManGetAigNodeNum( Ntk_Man_t * pNtk )
 {
     Ntk_Obj_t * pNode;
-    int i, Counter = 0;
-    Ntk_ManForEachPo( pNtk, pNode, i )
-        Counter++;
-    return Counter;
+    int i, nNodes = 0;
+    Ntk_ManForEachNode( pNtk, pNode, i )
+    {
+        if ( pNode->pFunc == NULL )
+        {
+            printf( "Ntk_ManGetAigNodeNum(): Local AIG of node %d is not assigned.\n", pNode->Id );
+            continue;
+        }
+        if ( Ntk_ObjFaninNum(pNode) < 2 )
+            continue;
+        nNodes += Hop_DagSize( pNode->pFunc );
+    }
+    return nNodes;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index caaa86f8..72a5674b 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -31,6 +31,7 @@ extern "C" {
 
 #include "aig.h"
 #include "tim.h"
+#include "ntk.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -227,6 +228,7 @@ extern Aig_Man_t *     Ntl_ManExtract( Ntl_Man_t * p );
 extern char *          Ntl_SopFromTruth( Ntl_Man_t * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover );
 /*=== ntlInsert.c ==========================================================*/
 extern int             Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig );
+extern int             Ntl_ManInsertNtk( Ntl_Man_t * p, Ntk_Man_t * pNtk );
 /*=== ntlCheck.c ==========================================================*/
 extern int             Ntl_ManCheck( Ntl_Man_t * pMan );
 extern int             Ntl_ModelCheck( Ntl_Mod_t * pModel );
@@ -236,6 +238,7 @@ extern Ntl_Man_t *     Ntl_ManAlloc( char * pFileName );
 extern void            Ntl_ManFree( Ntl_Man_t * p );
 extern Ntl_Mod_t *     Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
 extern void            Ntl_ManPrintStats( Ntl_Man_t * p );
+extern Tim_Man_t *     Ntl_ManReadTimeMan( Ntl_Man_t * p );
 extern Ntl_Mod_t *     Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName );
 extern void            Ntl_ModelFree( Ntl_Mod_t * p );
 /*=== ntlMap.c ============================================================*/
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 72a8bc40..a54618e5 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -438,6 +438,8 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
     // start the AIG manager
     assert( p->pAig == NULL );
     p->pAig = Aig_ManStart( 10000 );
+    p->pAig->pName = Aig_UtilStrsav( p->pName );
+    p->pAig->pSpec = Aig_UtilStrsav( p->pSpec );
     // get the root model
     pRoot = Vec_PtrEntry( p->vModels, 0 );
     // collect primary inputs
diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c
index 971d1278..84a7af84 100644
--- a/src/aig/ntl/ntlInsert.c
+++ b/src/aig/ntl/ntlInsert.c
@@ -123,6 +123,105 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Inserts the given mapping into the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManInsertNtk( Ntl_Man_t * p, Ntk_Man_t * pNtk )
+{
+    char Buffer[100];
+    Vec_Int_t * vTruth;
+    Vec_Int_t * vCover;
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pNode;
+    Ntl_Net_t * pNet, * pNetCo;
+    Ntk_Obj_t * pObj, * pFanin;
+    int i, k, nDigits;
+    unsigned * pTruth;
+    assert( Vec_PtrSize(p->vCis) == Ntk_ManCiNum(pNtk) );
+    assert( Vec_PtrSize(p->vCos) == Ntk_ManCoNum(pNtk) );
+    // set the correspondence between the PI/PO nodes
+    Ntl_ManForEachCiNet( p, pNet, i )
+        Ntk_ManCi( pNtk, i )->pCopy = pNet;
+//    Ntl_ManForEachCoNet( p, pNet, i )
+//        Ntk_ManCo( pNtk, i )->pCopy = pNet;
+    // remove old nodes
+    pRoot = Vec_PtrEntry( p->vModels, 0 );
+    Ntl_ModelForEachNode( pRoot, pNode, i )
+        Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL );
+    // create a new node for each LUT
+    vTruth = Vec_IntAlloc( 1 << 16 );
+    vCover = Vec_IntAlloc( 1 << 16 );
+    nDigits = Aig_Base10Log( Ntk_ManNodeNum(pNtk) );
+    Ntk_ManForEachNode( pNtk, pObj, i )
+    {
+        pNode = Ntl_ModelCreateNode( pRoot, Ntk_ObjFaninNum(pObj) );
+        pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, pObj->pFunc, Ntk_ObjFaninNum(pObj), vTruth, 0 );
+        pNode->pSop = Ntl_SopFromTruth( p, pTruth, Ntk_ObjFaninNum(pObj), vCover );
+        if ( !Kit_TruthIsConst0(pTruth, Ntk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Ntk_ObjFaninNum(pObj)) )
+        {
+            Ntk_ObjForEachFanin( pObj, pFanin, k )
+            {
+                pNet = pFanin->pCopy;
+                if ( pNet == NULL )
+                {
+                    printf( "Ntl_ManInsert(): Internal error: Net not found.\n" );
+                    return 0;
+                }
+                Ntl_ObjSetFanin( pNode, pNet, k );
+            }
+        }
+        sprintf( Buffer, "lut%0*d", nDigits, i );
+        if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
+        {
+            printf( "Ntl_ManInsert(): Internal error: Intermediate net name is not unique.\n" );
+            return 0;
+        }
+        pNet = Ntl_ModelFindOrCreateNet( pRoot, Buffer );
+        if ( !Ntl_ModelSetNetDriver( pNode, pNet ) )
+        {
+            printf( "Ntl_ManInsert(): Internal error: Net has more than one fanin.\n" );
+            return 0;
+        }
+        pObj->pCopy = pNet;
+    }
+    Vec_IntFree( vCover );
+    Vec_IntFree( vTruth );
+    // mark CIs and outputs of the registers
+    Ntl_ManForEachCiNet( p, pNetCo, i )
+        pNetCo->nVisits = 101;
+    // update the CO pointers
+    Ntl_ManForEachCoNet( p, pNetCo, i )
+    {
+        if ( pNetCo->nVisits == 101 )
+            continue;
+        pNetCo->nVisits = 101;
+        // get the corresponding PO and its driver
+        pObj = Ntk_ManCo( pNtk, i );
+        pFanin = Ntk_ObjFanin0( pObj );
+        // get the net driving the driver
+        pNet = pFanin->pCopy; //Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pFunc)->Id );
+        pNode = Ntl_ModelCreateNode( pRoot, 1 );
+        pNode->pSop = pObj->fCompl /*Aig_IsComplement(pNetCo->pFunc)*/? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" );
+        Ntl_ObjSetFanin( pNode, pNet, 0 );
+        // update the CO driver net
+        pNetCo->pDriver = NULL;
+        if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
+        {
+            printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" );
+            return 0;
+        }
+    }
+    return 1;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index b5331ae2..9614a423 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -139,6 +139,22 @@ void Ntl_ManPrintStats( Ntl_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Deallocates the netlist manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p )
+{
+    return p->pManTime;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Allocates the model.]
 
   Description []
diff --git a/src/aig/ntl/ntlMap.c b/src/aig/ntl/ntlMap.c
index 3de74200..20bc79cf 100644
--- a/src/aig/ntl/ntlMap.c
+++ b/src/aig/ntl/ntlMap.c
@@ -117,7 +117,7 @@ Vec_Ptr_t * Ntl_MappingFromAig( Aig_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Ntk_ManSetIfParsDefault( If_Par_t * pPars )
+void Ntl_ManSetIfParsDefault( If_Par_t * pPars )
 {
 //    extern void * Abc_FrameReadLibLut();
     // set defaults
@@ -162,57 +162,6 @@ void Ntk_ManSetIfParsDefault( If_Par_t * pPars )
 */
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Load the network into FPGA manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-If_Man_t * Ntk_ManToIf_old( Aig_Man_t * p, If_Par_t * pPars )
-{
-    If_Man_t * pIfMan;
-    Aig_Obj_t * pNode;//, * pFanin, * pPrev;
-    Vec_Ptr_t * vNodes;
-    int i;
-    // start the mapping manager and set its parameters
-    pIfMan = If_ManStart( pPars );
-    // print warning about excessive memory usage
-    if ( 1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30) > 1.0 )
-        printf( "Warning: The mapper will allocate %.1f Gb for to represent the subject graph with %d AIG nodes.\n", 
-            1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30), Aig_ManObjNum(p) );
-    // load the AIG into the mapper
-    vNodes = Aig_ManDfsPio( p );
-    Vec_PtrForEachEntry( vNodes, pNode, i )
-    {
-        if ( Aig_ObjIsAnd(pNode) )
-            pNode->pData = (Aig_Obj_t *)If_ManCreateAnd( pIfMan, 
-                If_NotCond( (If_Obj_t *)Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ), 
-                If_NotCond( (If_Obj_t *)Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) );
-        else if ( Aig_ObjIsPi(pNode) )
-            pNode->pData = If_ManCreateCi( pIfMan );
-        else if ( Aig_ObjIsPo(pNode) )
-            If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
-        else if ( Aig_ObjIsConst1(pNode) )
-            Aig_ManConst1(p)->pData = If_ManConst1( pIfMan );
-        else // add the node to the mapper
-            assert( 0 );
-        // set up the choice node
-//        if ( Aig_AigNodeIsChoice( pNode ) )
-//        {
-//            pIfMan->nChoices++;
-//            for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
-//                If_ObjSetChoice( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData );
-//            If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pData );
-//        }
-    }
-    Vec_PtrFree( vNodes );
-    return pIfMan;
-}
 
 /**Function*************************************************************
 
@@ -225,7 +174,7 @@ If_Man_t * Ntk_ManToIf_old( Aig_Man_t * p, If_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
+If_Man_t * Ntl_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
 {
     If_Man_t * pIfMan;
     Aig_Obj_t * pNode;//, * pFanin, * pPrev;
@@ -251,7 +200,7 @@ If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
                 pIfMan->nLevelMax = (int)pNode->Level;
         }
         else if ( Aig_ObjIsPo(pNode) )
-            If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
+            pNode->pData = If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
         else if ( Aig_ObjIsConst1(pNode) )
             Aig_ManConst1(p)->pData = If_ManConst1( pIfMan );
         else // add the node to the mapper
@@ -264,6 +213,11 @@ If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
 //                If_ObjSetChoice( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData );
 //            If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pData );
 //        }
+        {
+            If_Obj_t * pIfObj = pNode->pData;
+            assert( !If_IsComplement(pIfObj) );
+            assert( pIfObj->Id == pNode->Id );
+        }
     }
     return pIfMan;
 }
@@ -279,7 +233,7 @@ If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Ntk_ManFromIf( Aig_Man_t * p, If_Man_t * pMan )
+Vec_Ptr_t * Ntl_ManFromIf( Aig_Man_t * p, If_Man_t * pMan )
 {
     Vec_Ptr_t * vIfMap;
     If_Obj_t * pNode, * pLeaf; 
@@ -356,12 +310,12 @@ Vec_Ptr_t * Ntl_MappingIf( Ntl_Man_t * pMan, Aig_Man_t * p )
     If_Par_t Pars, * pPars = &Pars;
     If_Man_t * pIfMan;
     // perform FPGA mapping
-    Ntk_ManSetIfParsDefault( pPars );
+    Ntl_ManSetIfParsDefault( pPars );
     // set the arrival times
     pPars->pTimesArr = ALLOC( float, Aig_ManPiNum(p) );
     memset( pPars->pTimesArr, 0, sizeof(float) * Aig_ManPiNum(p) );
     // translate into the mapper
-    pIfMan = Ntk_ManToIf( p, pPars );    
+    pIfMan = Ntl_ManToIf( p, pPars );    
     if ( pIfMan == NULL )
         return NULL;
     pIfMan->pManTim = Tim_ManDup( pMan->pManTime, 0 );
@@ -371,7 +325,7 @@ Vec_Ptr_t * Ntl_MappingIf( Ntl_Man_t * pMan, Aig_Man_t * p )
         return NULL;
     }
     // transform the result of mapping into the new network
-    vMapping = Ntk_ManFromIf( p, pIfMan );
+    vMapping = Ntl_ManFromIf( p, pIfMan );
     If_ManStop( pIfMan );
     if ( vMapping == NULL )
         return NULL;
diff --git a/src/aig/tim/tim.c b/src/aig/tim/tim.c
index a71e1497..77967ef6 100644
--- a/src/aig/tim/tim.c
+++ b/src/aig/tim/tim.c
@@ -150,7 +150,8 @@ Tim_Man_t * Tim_ManStart( int nPis, int nPos )
 
   Synopsis    [Duplicates the timing manager.]
 
-  Description []
+  Description [Derives discrete-delay-model timing manager. 
+  Useful for AIG optimization with approximate timing information.]
                
   SideEffects []
 
@@ -171,16 +172,21 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fDiscrete )
     for ( k = 0; k < p->nPos; k++ )
         pNew->pPos[k].TravId = 0;
     if ( fDiscrete )
+    {
         for ( k = 0; k < p->nPis; k++ )
             pNew->pPis[k].timeArr = 0.0; // modify here
+        // modify the required times
+    }
     pNew->vDelayTables = Vec_PtrAlloc( 100 );
     Tim_ManForEachBox( p, pBox, i )
     {
         pDelayTableNew = ALLOC( float, pBox->nInputs * pBox->nOutputs );
         Vec_PtrPush( pNew->vDelayTables, pDelayTableNew );
         if ( fDiscrete )
+        {
             for ( k = 0; k < pBox->nInputs * pBox->nOutputs; k++ )
                 pDelayTableNew[k] = 1.0; // modify here
+        }
         else
             memcpy( pDelayTableNew, pBox->pDelayTable, sizeof(float) * pBox->nInputs * pBox->nOutputs );
         Tim_ManCreateBoxFirst( pNew, pBox->Inouts[0], pBox->nInputs, 
@@ -191,6 +197,47 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fDiscrete )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the timing manager.]
+
+  Description [Derives unit-delay-model timing manager. 
+  Useful for levelizing the network.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Tim_Man_t * Tim_ManDupUnit( Tim_Man_t * p )
+{
+    Tim_Man_t * pNew;
+    Tim_Box_t * pBox;
+    float * pDelayTableNew;
+    int i, k;
+    pNew = Tim_ManStart( p->nPis, p->nPos );
+    memcpy( pNew->pPis, p->pPis, sizeof(Tim_Obj_t) * p->nPis );
+    memcpy( pNew->pPos, p->pPos, sizeof(Tim_Obj_t) * p->nPos );
+    for ( k = 0; k < p->nPis; k++ )
+    {
+        pNew->pPis[k].TravId = 0;
+        pNew->pPis[k].timeArr = 0.0; 
+    }
+    for ( k = 0; k < p->nPos; k++ )
+        pNew->pPos[k].TravId = 0;
+    pNew->vDelayTables = Vec_PtrAlloc( 100 );
+    Tim_ManForEachBox( p, pBox, i )
+    {
+        pDelayTableNew = ALLOC( float, pBox->nInputs * pBox->nOutputs );
+        Vec_PtrPush( pNew->vDelayTables, pDelayTableNew );
+        for ( k = 0; k < pBox->nInputs * pBox->nOutputs; k++ )
+            pDelayTableNew[k] = 1.0;
+        Tim_ManCreateBoxFirst( pNew, pBox->Inouts[0], pBox->nInputs, 
+            pBox->Inouts[pBox->nInputs], pBox->nOutputs, pDelayTableNew );
+    }
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Stops the timing manager.]
 
   Description []
@@ -567,6 +614,110 @@ float Tim_ManGetPoRequired( Tim_Man_t * p, int iPo )
     return pObjThis->timeReq;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns the box number for the given input.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManBoxForCi( Tim_Man_t * p, int iCi )
+{
+    if ( iCi >= p->nPis )
+        return -1;
+    return p->pPis[iCi].iObj2Box;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the box number for the given output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManBoxForCo( Tim_Man_t * p, int iCo )
+{
+    if ( iCo >= p->nPos )
+        return -1;
+    return p->pPos[iCo].iObj2Box;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the first input of the box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManBoxInputFirst( Tim_Man_t * p, int iBox )
+{
+    Tim_Box_t * pBox = Vec_PtrEntry( p->vBoxes, iBox );
+    return pBox->Inouts[0];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the first input of the box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManBoxOutputFirst( Tim_Man_t * p, int iBox )
+{
+    Tim_Box_t * pBox = Vec_PtrEntry( p->vBoxes, iBox );
+    return pBox->Inouts[pBox->nInputs];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the first input of the box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManBoxInputNum( Tim_Man_t * p, int iBox )
+{
+    Tim_Box_t * pBox = Vec_PtrEntry( p->vBoxes, iBox );
+    return pBox->nInputs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the first input of the box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManBoxOutputNum( Tim_Man_t * p, int iBox )
+{
+    Tim_Box_t * pBox = Vec_PtrEntry( p->vBoxes, iBox );
+    return pBox->nOutputs;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/tim/tim.h b/src/aig/tim/tim.h
index f1fb992c..f56b0881 100644
--- a/src/aig/tim/tim.h
+++ b/src/aig/tim/tim.h
@@ -59,6 +59,7 @@ typedef struct Tim_Man_t_           Tim_Man_t;
 /*=== time.c ===========================================================*/
 extern Tim_Man_t *     Tim_ManStart( int nPis, int nPos );
 extern Tim_Man_t *     Tim_ManDup( Tim_Man_t * p, int fDiscrete );
+extern Tim_Man_t *     Tim_ManDupUnit( Tim_Man_t * p );
 extern void            Tim_ManStop( Tim_Man_t * p );
 extern void            Tim_ManPrint( Tim_Man_t * p );
 extern void            Tim_ManSetDelayTables( Tim_Man_t * p, Vec_Ptr_t * vDelayTables );
@@ -73,6 +74,12 @@ extern void            Tim_ManSetPoRequired( Tim_Man_t * p, int iPo, float Delay
 extern void            Tim_ManSetPoRequiredAll( Tim_Man_t * p, float Delay );
 extern float           Tim_ManGetPiArrival( Tim_Man_t * p, int iPi );
 extern float           Tim_ManGetPoRequired( Tim_Man_t * p, int iPo );
+extern int             Tim_ManBoxForCi( Tim_Man_t * p, int iCo );
+extern int             Tim_ManBoxForCo( Tim_Man_t * p, int iCi );
+extern int             Tim_ManBoxInputFirst( Tim_Man_t * p, int iBox );
+extern int             Tim_ManBoxOutputFirst( Tim_Man_t * p, int iBox );
+extern int             Tim_ManBoxInputNum( Tim_Man_t * p, int iBox );
+extern int             Tim_ManBoxOutputNum( Tim_Man_t * p, int iBox );
 
 #ifdef __cplusplus
 }
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 1d5195c7..7dce5154 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -582,6 +582,7 @@ extern Vec_Ptr_t *        Abc_NtkSupport( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
 extern Vec_Ptr_t *        Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos );
 extern Vec_Vec_t *        Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi );
+extern Vec_Vec_t *        Abc_NtkLevelize( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkLevel( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkLevelReverse( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk );
@@ -612,7 +613,6 @@ extern int                Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
 extern void               Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkSopToAig( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkAigToBdd( Abc_Ntk_t * pNtk );
-extern unsigned *         Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst );
 extern int                Abc_NtkMapToSop( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect );
 extern int                Abc_NtkToBdd( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index 4c6a7fb0..c82faa15 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -978,6 +978,32 @@ int Abc_NtkLevelReverse_rec( Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
+Vec_Vec_t * Abc_NtkLevelize( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    Vec_Vec_t * vLevels;
+    int nLevels, i;
+    nLevels = Abc_NtkLevel( pNtk );
+    vLevels = Vec_VecStart( nLevels + 1 );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        assert( (int)pObj->Level <= nLevels );
+        Vec_VecPush( vLevels, pObj->Level, pObj );
+    }
+    return vLevels;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_NtkLevel( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index f3297d8f..e99cc88b 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -785,159 +785,6 @@ DdNode * Abc_ConvertAigToBdd( DdManager * dd, Hop_Obj_t * pRoot )
 
 
 
-/**Function*************************************************************
-
-  Synopsis    [Construct BDDs and mark AIG nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_ConvertAigToTruth_rec1( Hop_Obj_t * pObj )
-{
-    int Counter = 0;
-    assert( !Hop_IsComplement(pObj) );
-    if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
-        return 0;
-    Counter += Abc_ConvertAigToTruth_rec1( Hop_ObjFanin0(pObj) ); 
-    Counter += Abc_ConvertAigToTruth_rec1( Hop_ObjFanin1(pObj) );
-    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
-    Hop_ObjSetMarkA( pObj );
-    return Counter + 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes truth table of the cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned * Abc_ConvertAigToTruth_rec2( Hop_Obj_t * pObj, Vec_Int_t * vTruth, int nWords )
-{
-    unsigned * pTruth, * pTruth0, * pTruth1;
-    int i;
-    assert( !Hop_IsComplement(pObj) );
-    if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
-        return pObj->pData;
-    // compute the truth tables of the fanins
-    pTruth0 = Abc_ConvertAigToTruth_rec2( Hop_ObjFanin0(pObj), vTruth, nWords );
-    pTruth1 = Abc_ConvertAigToTruth_rec2( Hop_ObjFanin1(pObj), vTruth, nWords );
-    // creat the truth table of the node
-    pTruth  = Vec_IntFetch( vTruth, nWords );
-    if ( Hop_ObjIsExor(pObj) )
-        for ( i = 0; i < nWords; i++ )
-            pTruth[i] = pTruth0[i] ^ pTruth1[i];
-    else if ( !Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) )
-        for ( i = 0; i < nWords; i++ )
-            pTruth[i] = pTruth0[i] & pTruth1[i];
-    else if ( !Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) )
-        for ( i = 0; i < nWords; i++ )
-            pTruth[i] = pTruth0[i] & ~pTruth1[i];
-    else if ( Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) )
-        for ( i = 0; i < nWords; i++ )
-            pTruth[i] = ~pTruth0[i] & pTruth1[i];
-    else // if ( Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) )
-        for ( i = 0; i < nWords; i++ )
-            pTruth[i] = ~pTruth0[i] & ~pTruth1[i];
-    assert( Hop_ObjIsMarkA(pObj) ); // loop detection
-    Hop_ObjClearMarkA( pObj );
-    pObj->pData = pTruth;
-    return pTruth;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes truth table of the node.]
-
-  Description [Assumes that the structural support is no more than 8 inputs.
-  Uses array vTruth to store temporary truth tables. The returned pointer should 
-  be used immediately.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst )
-{
-    static unsigned uTruths[8][8] = { // elementary truth tables
-        { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
-        { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
-        { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
-        { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
-        { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, 
-        { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, 
-        { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, 
-        { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } 
-    };
-    Hop_Obj_t * pObj;
-    unsigned * pTruth, * pTruth2;
-    int i, nWords, nNodes;
-    Vec_Ptr_t * vTtElems;
-
-    // if the number of variables is more than 8, allocate truth tables
-    if ( nVars > 8 )
-        vTtElems = Vec_PtrAllocTruthTables( nVars );
-    else
-        vTtElems = NULL;
-
-    // clear the data fields and set marks
-    nNodes = Abc_ConvertAigToTruth_rec1( pRoot );
-    // prepare memory
-    nWords = Hop_TruthWordNum( nVars );
-    Vec_IntClear( vTruth );
-    Vec_IntGrow( vTruth, nWords * (nNodes+1) );
-    pTruth = Vec_IntFetch( vTruth, nWords );
-    // check the case of a constant
-    if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
-    {
-        assert( nNodes == 0 );
-        if ( Hop_IsComplement(pRoot) )
-            Extra_TruthClear( pTruth, nVars );
-        else
-            Extra_TruthFill( pTruth, nVars );
-        return pTruth;
-    }
-    // set elementary truth tables at the leaves
-    assert( nVars <= Hop_ManPiNum(p) );
-//    assert( Hop_ManPiNum(p) <= 8 ); 
-    if ( fMsbFirst )
-    {
-        Hop_ManForEachPi( p, pObj, i )
-        {
-            if ( vTtElems )
-                pObj->pData = Vec_PtrEntry(vTtElems, nVars-1-i);
-            else               
-                pObj->pData = (void *)uTruths[nVars-1-i];
-        }
-    }
-    else
-    {
-        Hop_ManForEachPi( p, pObj, i )
-        {
-            if ( vTtElems )
-                pObj->pData = Vec_PtrEntry(vTtElems, i);
-            else               
-                pObj->pData = (void *)uTruths[i];
-        }
-    }
-    // clear the marks and compute the truth table
-    pTruth2 = Abc_ConvertAigToTruth_rec2( pRoot, vTruth, nWords );
-    // copy the result
-    Extra_TruthCopy( pTruth, pTruth2, nVars );
-    if ( vTtElems )
-        Vec_PtrFree( vTtElems );
-    return pTruth;
-}
-
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d9c68bc4..65403609 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -205,6 +205,8 @@ static int Abc_CommandAbc8Write      ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandAbc8Ps         ( 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_CommandAbc8ReadLut    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8PrintLut   ( 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 );
@@ -431,6 +433,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC8",         "*ps",           Abc_CommandAbc8Ps,           0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*if",           Abc_CommandAbc8If,           0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*dchoice",      Abc_CommandAbc8DChoice,      0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*read_lut",     Abc_CommandAbc8ReadLut,      0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*print_lut",    Abc_CommandAbc8PrintLut,     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 );
@@ -473,6 +477,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
 void Abc_End()
 {
     Abc_FrameClearDesign(); 
+    {
+        extern void If_LutLibFree( void * pLutLib );
+        if ( Abc_FrameGetGlobalFrame()->pAbc8Lib )
+            If_LutLibFree( Abc_FrameGetGlobalFrame()->pAbc8Lib );
+    }
 
 //    Dar_LibDumpPriorities();
     {
@@ -1754,7 +1763,7 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
             fprintf( pErr, "Currently works only for up to 16 inputs.\n" );
             return 1;
         }
-        pTruth = Abc_ConvertAigToTruth( pNtk->pManFunc, Hop_Regular(pObj->pData), Abc_ObjFaninNum(pObj), vMemory, 0 );
+        pTruth = Hop_ManConvertAigToTruth( pNtk->pManFunc, Hop_Regular(pObj->pData), Abc_ObjFaninNum(pObj), vMemory, 0 );
         if ( Hop_IsComplement(pObj->pData) )
             Extra_TruthNot( pTruth, pTruth, Abc_ObjFaninNum(pObj) );
         Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) );
@@ -3387,7 +3396,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nDivMax      =  250;
     pPars->nWinSizeMax  =  300;
     pPars->nGrowthLevel =    0;
-    pPars->nBTLimit     =10000;
+    pPars->nBTLimit     = 5000;
     pPars->fResub       =    1;
     pPars->fArea        =    0;
     pPars->fMoreEffort  =    0;
@@ -7073,7 +7082,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
 //    extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
 //    extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
-    extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
+//    extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
 //    extern void Abc_NtkDarTestBlif( char * pFileName );
 //    extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk );
 
@@ -8111,10 +8120,10 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    int fBalance, fVerbose, fUpdateLevel, c;
+    int fBalance, fVerbose, fUpdateLevel, fConstruct, c;
     int nConfMax, nLevelMax;
 
-    extern Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -8123,11 +8132,12 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     fBalance     = 1;
     fUpdateLevel = 1;
+    fConstruct   = 0;
     nConfMax     = 1000;
     nLevelMax    = 0;
     fVerbose     = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CLblvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CLblcvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -8159,6 +8169,9 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'l':
             fUpdateLevel ^= 1;
             break;
+        case 'c':
+            fConstruct ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -8178,7 +8191,7 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "This command works only for strashed networks.\n" );
         return 1;
     }
-    pNtkRes = Abc_NtkDChoice( pNtk, fBalance, fUpdateLevel, nConfMax, nLevelMax, fVerbose );
+    pNtkRes = Abc_NtkDChoice( pNtk, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -8189,12 +8202,13 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dchoice [-C num] [-L num] [-blvh]\n" );
+    fprintf( pErr, "usage: dchoice [-C num] [-L num] [-blcvh]\n" );
     fprintf( pErr, "\t         performs partitioned choicing using a new AIG package\n" );
     fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfMax );
     fprintf( pErr, "\t-L num : the max level of nodes to consider (0 = not used) [default = %d]\n", nLevelMax );
     fprintf( pErr, "\t-b     : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" );
     fprintf( pErr, "\t-l     : toggle updating level [default = %s]\n", fUpdateLevel? "yes": "no" );
+    fprintf( pErr, "\t-c     : toggle constructive computation of choices [default = %s]\n", fConstruct? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -14751,6 +14765,7 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     char * pFileName;
     int c;
     extern void Ioa_WriteBlif( void * p, char * pFileName );
+    extern int Ntl_ManInsertNtk( void * p, void * pNtk );
 
     // set defaults
     Extra_UtilGetoptReset();
@@ -14772,6 +14787,17 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // get the input file name
     pFileName = argv[globalUtilOptind];
+    if ( pAbc->pAbc8Ntk != NULL )
+    {
+        if ( !Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Ntk ) )
+        {
+            printf( "Abc_CommandAbc8Write(): There is no design to write.\n" );
+            return 1;
+        }
+        printf( "Writing the mapped design.\n" );
+    }
+    else
+        printf( "Writing the original design.\n" );
     Ioa_WriteBlif( pAbc->pAbc8Ntl, pFileName );
     return 0;
 
@@ -14797,6 +14823,7 @@ int Abc_CommandAbc8Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     int c;
     extern void Ntl_ManPrintStats( void * p );
+    extern void Ntk_ManPrintStats( void * p, void * pLutLib );
 
     // set defaults
     Extra_UtilGetoptReset();
@@ -14821,6 +14848,8 @@ int Abc_CommandAbc8Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
         Ntl_ManPrintStats( pAbc->pAbc8Ntl );
     if ( pAbc->pAbc8Aig )
         Aig_ManPrintStats( pAbc->pAbc8Aig );
+    if ( pAbc->pAbc8Ntk )
+        Ntk_ManPrintStats( pAbc->pAbc8Ntk, pAbc->pAbc8Lib );
     return 0;
 
 usage:
@@ -14843,11 +14872,26 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    If_Par_t Pars, * pPars = &Pars;
+    void * pNtkNew;
     int c;
     extern int Ntl_ManInsertTest( void * p, Aig_Man_t * pAig );
     extern int Ntl_ManInsertTestIf( void * p, Aig_Man_t * pAig );
+    extern void * Ntk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars );
+    extern Tim_Man_t * Ntl_ManReadTimeMan( void * p );
+    extern void * If_SetSimpleLutLib( int nLutSize );
+    extern void Ntk_ManSetIfParsDefault( If_Par_t * pPars );
+    extern void Ntk_ManFree( void * );
+
+    if ( pAbc->pAbc8Lib == NULL )
+    {
+        printf( "LUT library is not given. Using defaul 6-LUT library.\n" );
+        pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 );
+    }
 
     // set defaults
+    Ntk_ManSetIfParsDefault( pPars );
+    pPars->pLutLib = pAbc->pAbc8Lib;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
     {
@@ -14864,7 +14908,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc8Write(): There is no AIG to map.\n" );
         return 1;
     }
-
+/*
     // get the input file name
     if ( !Ntl_ManInsertTestIf( pAbc->pAbc8Ntl, pAbc->pAbc8Aig ) )
 //    if ( !Ntl_ManInsertTest( pAbc->pAbc8Ntl, pAbc->pAbc8Aig ) )
@@ -14872,6 +14916,16 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc8Write(): Tranformation of the netlist has failed.\n" );
         return 1;
     }
+*/
+    pNtkNew = Ntk_MappingIf( pAbc->pAbc8Aig, Ntl_ManReadTimeMan(pAbc->pAbc8Ntl), pPars );
+    if ( pNtkNew == NULL )
+    {
+        printf( "Abc_CommandAbc8If(): Mapping of the AIG has failed.\n" );
+        return 1;
+    }
+    if ( pAbc->pAbc8Ntk != NULL )
+        Ntk_ManFree( pAbc->pAbc8Ntk );
+    pAbc->pAbc8Ntk = pNtkNew;
     return 0;
 
 usage:
@@ -14937,6 +14991,138 @@ 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 void * If_LutLibRead( char * FileName );
+    extern void If_LutLibFree( void * 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: *read_lut [-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( void * 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: *print_lut [-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 []
diff --git a/src/base/abci/abcBidec.c b/src/base/abci/abcBidec.c
index ad332314..bb114578 100644
--- a/src/base/abci/abcBidec.c
+++ b/src/base/abci/abcBidec.c
@@ -19,15 +19,13 @@
 ***********************************************************************/
 
 #include "abc.h"
-
 #include "bdc.h"
-#include "bdcInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj )  { return Hop_NotCond( Bdc_Regular(pObj)->pCopy, Bdc_IsComplement(pObj) );  }
+static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj )  { return Hop_NotCond( Bdc_FuncCopy(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) );  }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -48,24 +46,25 @@ Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pR
 {
     unsigned * pTruth;
     Bdc_Fun_t * pFunc;
-    int i;
+    int nNodes, i;
     assert( nVars <= 16 );
     // derive truth table
-    pTruth = Abc_ConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 );
+    pTruth = Hop_ManConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 );
     if ( Hop_IsComplement(pRoot) )
         Extra_TruthNot( pTruth, pTruth, nVars );
     // decompose truth table
     Bdc_ManDecompose( p, pTruth, puCare, nVars, NULL, 1000 );
     // convert back into HOP
-    Bdc_FunWithId( p, 0 )->pCopy = Hop_ManConst1( pHop );
+    Bdc_FuncSetCopy( Bdc_ManFunc( p, 0 ), Hop_ManConst1( pHop ) );
     for ( i = 0; i < nVars; i++ )
-        Bdc_FunWithId( p, i+1 )->pCopy = Hop_ManPi( pHop, i );
-    for ( i = nVars + 1; i < p->nNodes; i++ )
+        Bdc_FuncSetCopy( Bdc_ManFunc( p, i+1 ), Hop_ManPi( pHop, i ) );
+    nNodes = Bdc_ManNodeNum(p);
+    for ( i = nVars + 1; i < nNodes; i++ )
     {
-        pFunc = Bdc_FunWithId( p, i );
-        pFunc->pCopy = Hop_And( pHop, Bdc_FunCopyHop(pFunc->pFan0), Bdc_FunCopyHop(pFunc->pFan1) );
+        pFunc = Bdc_ManFunc( p, i );
+        Bdc_FuncSetCopy( pFunc, Hop_And( pHop, Bdc_FunCopyHop(Bdc_FuncFanin0(pFunc)), Bdc_FunCopyHop(Bdc_FuncFanin1(pFunc)) ) );
     }
-    return Bdc_FunCopyHop(p->pRoot);
+    return Bdc_FunCopyHop( Bdc_ManRoot(p) );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 94b6c52b..dd8f8221 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -769,7 +769,7 @@ clk = clock();
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose )
+Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose )
 {
     Aig_Man_t * pMan, * pTemp;
     Abc_Ntk_t * pNtkAig;
@@ -777,7 +777,7 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in
     pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
-    pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, nConfMax, nLevelMax, fVerbose );
+    pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose );
     Aig_ManStop( pTemp );
     pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
     Aig_ManStop( pMan );
@@ -1432,6 +1432,7 @@ Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
 ***********************************************************************/
 void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk )
 {
+/*
     Aig_Man_t * pMan;
     pMan = Abc_NtkToDar( pNtk, 1 );
     if ( pMan == NULL )
@@ -1442,6 +1443,7 @@ void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk )
     pMan->vFlopNums = NULL;
     Aig_ManHaigRecord( pMan );
     Aig_ManStop( pMan );
+*/
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 744d9c95..c1e0faf0 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -383,7 +383,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, int fReco
         extern int Abc_NtkRecStrashNode( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, unsigned * pTruth, int nVars );
         int nVars = Abc_NtkRecVarNum();
         Vec_Int_t * vMemory = Abc_NtkRecMemory();
-        unsigned * pTruth = Abc_ConvertAigToTruth( pMan, Hop_Regular(pRoot), nVars, vMemory, 0 );
+        unsigned * pTruth = Hop_ManConvertAigToTruth( pMan, Hop_Regular(pRoot), nVars, vMemory, 0 );
         assert( Extra_TruthSupportSize(pTruth, nVars) == Abc_ObjFaninNum(pNodeOld) ); // should be swept
         if ( Hop_IsComplement(pRoot) )
             Extra_TruthNot( pTruth, pTruth, nVars );
diff --git a/src/base/io/ioWriteBench.c b/src/base/io/ioWriteBench.c
index 4b766a47..df4a6259 100644
--- a/src/base/io/ioWriteBench.c
+++ b/src/base/io/ioWriteBench.c
@@ -258,7 +258,7 @@ int Io_WriteBenchLutOneNode( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vTruth
     nFanins = Abc_ObjFaninNum(pNode);
     assert( nFanins <= 8 );
     // compute the truth table
-    pTruth = Abc_ConvertAigToTruth( pNode->pNtk->pManFunc, Hop_Regular(pNode->pData), nFanins, vTruth, 0 );
+    pTruth = Hop_ManConvertAigToTruth( pNode->pNtk->pManFunc, Hop_Regular(pNode->pData), nFanins, vTruth, 0 );
     if ( Hop_IsComplement(pNode->pData) )
         Extra_TruthNot( pTruth, pTruth, nFanins );
     // consider simple cases
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 0261d7da..7196b952 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -78,6 +78,7 @@ struct Abc_Frame_t_
     void *          pAbc8Ntl;    // the current design
     void *          pAbc8Ntk;    // the current mapped network
     void *          pAbc8Aig;    // the current AIG
+    void *          pAbc8Lib;    // the current LUT library
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/fpga/fpga.c b/src/map/fpga/fpga.c
index 40423f4f..31edf689 100644
--- a/src/map/fpga/fpga.c
+++ b/src/map/fpga/fpga.c
@@ -146,7 +146,7 @@ int Fpga_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv )
     fclose( pFile );
 
     // set the new network
-    pLib = Fpga_LutLibCreate( FileName, fVerbose );
+    pLib = Fpga_LutLibRead( FileName, fVerbose );
     if ( pLib == NULL )
     {
         fprintf( pErr, "Reading LUT library has failed.\n" );
@@ -228,7 +228,7 @@ int Fpga_CommandPrintLibrary( Abc_Frame_t * pAbc, int argc, char **argv )
     return 0;
 
 usage:
-    fprintf( pErr, "\nusage: read_print [-vh]\n");
+    fprintf( pErr, "\nusage: print_lut [-vh]\n");
     fprintf( pErr, "\t          print the current LUT library\n" );  
     fprintf( pErr, "\t-v      : toggles enabling of verbose output [default = %s]\n", (fVerbose? "yes" : "no") );
     fprintf( pErr, "\t-h      : print the command usage\n");
diff --git a/src/map/fpga/fpgaInt.h b/src/map/fpga/fpgaInt.h
index be790a55..1e4ac1d4 100644
--- a/src/map/fpga/fpgaInt.h
+++ b/src/map/fpga/fpgaInt.h
@@ -314,7 +314,7 @@ extern void              Fpga_NodeAddFaninFanout( Fpga_Node_t * pFanin, Fpga_Nod
 extern void              Fpga_NodeRemoveFaninFanout( Fpga_Node_t * pFanin, Fpga_Node_t * pFanoutToRemove );
 extern int               Fpga_NodeGetFanoutNum( Fpga_Node_t * pNode );
 /*=== fpgaLib.c ============================================================*/
-extern Fpga_LutLib_t *   Fpga_LutLibCreate( char * FileName, int fVerbose );
+extern Fpga_LutLib_t *   Fpga_LutLibRead( char * FileName, int fVerbose );
 extern void              Fpga_LutLibFree( Fpga_LutLib_t * p );
 extern void              Fpga_LutLibPrint( Fpga_LutLib_t * pLutLib );
 extern int               Fpga_LutLibDelaysAreDiscrete( Fpga_LutLib_t * pLutLib );
diff --git a/src/map/fpga/fpgaLib.c b/src/map/fpga/fpgaLib.c
index b1bb4cdc..77fc3a6f 100644
--- a/src/map/fpga/fpgaLib.c
+++ b/src/map/fpga/fpgaLib.c
@@ -52,7 +52,7 @@ float       Fpga_LutLibReadLutArea( Fpga_LutLib_t * p, int Size )    { assert( S
   SeeAlso     []
 
 ***********************************************************************/
-Fpga_LutLib_t * Fpga_LutLibCreate( char * FileName, int fVerbose )
+Fpga_LutLib_t * Fpga_LutLibRead( char * FileName, int fVerbose )
 {
     char pBuffer[1000], * pToken;
     Fpga_LutLib_t * p;
diff --git a/src/map/if/if.h b/src/map/if/if.h
index d42dd0af..d97a1154 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -245,8 +245,9 @@ static inline If_Obj_t * If_ManObj( If_Man_t * p, int i )                    { r
 static inline int        If_ObjIsConst1( If_Obj_t * pObj )                   { return pObj->Type == IF_CONST1;       }
 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_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_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;          }
 
 static inline If_Obj_t * If_ObjFanin0( If_Obj_t * pObj )                     { return pObj->pFanin0;                 }
@@ -402,6 +403,8 @@ extern int             If_ManCrossCut( If_Man_t * p );
 extern Vec_Ptr_t *     If_ManReverseOrder( If_Man_t * p );
 extern void            If_ManMarkMapping( If_Man_t * p );
 extern Vec_Ptr_t *     If_ManCollectMappingDirect( If_Man_t * p );
+extern Vec_Int_t *     If_ManCollectMappingInt( If_Man_t * p );
+
 
 extern int             If_ManCountSpecialPos( If_Man_t * p );
 
diff --git a/src/map/if/ifLib.c b/src/map/if/ifLib.c
new file mode 100644
index 00000000..2089ca3c
--- /dev/null
+++ b/src/map/if/ifLib.c
@@ -0,0 +1,273 @@
+/**CFile****************************************************************
+
+  FileName    [ifLib.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [FPGA mapping based on priority cuts.]
+
+  Synopsis    [LUT library.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 21, 2006.]
+
+  Revision    [$Id: ifLib.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "if.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline char * If_UtilStrsav( char *s ) {  return !s ? s : strcpy(ALLOC(char, strlen(s)+1), s);  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the description of LUTs from the LUT library file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Lib_t * If_LutLibRead( char * FileName )
+{
+    char pBuffer[1000], * pToken;
+    If_Lib_t * p;
+    FILE * pFile;
+    int i, k;
+
+    pFile = fopen( FileName, "r" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open LUT library file \"%s\".\n", FileName );
+        return NULL;
+    }
+
+    p = ALLOC( If_Lib_t, 1 );
+    memset( p, 0, sizeof(If_Lib_t) );
+    p->pName = If_UtilStrsav( FileName );
+
+    i = 1;
+    while ( fgets( pBuffer, 1000, pFile ) != NULL )
+    {
+        pToken = strtok( pBuffer, " \t\n" );
+        if ( pToken == NULL )
+            continue;
+        if ( pToken[0] == '#' )
+            continue;
+        if ( i != atoi(pToken) )
+        {
+            printf( "Error in the LUT library file \"%s\".\n", FileName );
+            free( p );
+            return NULL;
+        }
+
+        // read area
+        pToken = strtok( NULL, " \t\n" );
+        p->pLutAreas[i] = (float)atof(pToken);
+
+        // read delays
+        k = 0;
+        while ( pToken = strtok( NULL, " \t\n" ) )
+            p->pLutDelays[i][k++] = (float)atof(pToken);
+
+        // check for out-of-bound
+        if ( k > i )
+        {
+            printf( "LUT %d has too many pins (%d). Max allowed is %d.\n", i, k, i );
+            return NULL;
+        }
+
+        // check if var delays are specifies
+        if ( k > 1 )
+            p->fVarPinDelays = 1;
+
+        if ( i == IF_MAX_LUTSIZE )
+        {
+            printf( "Skipping LUTs of size more than %d.\n", i );
+            return NULL;
+        }
+        i++;
+    }
+    p->LutMax = i-1;
+
+    // check the library
+    if ( p->fVarPinDelays )
+    {
+        for ( i = 1; i <= p->LutMax; i++ )
+            for ( k = 0; k < i; k++ )
+            {
+                if ( p->pLutDelays[i][k] <= 0.0 )
+                    printf( "Warning: Pin %d of LUT %d has delay %f. Pin delays should be non-negative numbers. Technology mapping may not work correctly.\n", 
+                        k, i, p->pLutDelays[i][k] );
+                if ( k && p->pLutDelays[i][k-1] > p->pLutDelays[i][k] )
+                    printf( "Warning: Pin %d of LUT %d has delay %f. Pin %d of LUT %d has delay %f. Pin delays should be in non-decreasing order. Technology mapping may not work correctly.\n", 
+                        k-1, i, p->pLutDelays[i][k-1], 
+                        k, i, p->pLutDelays[i][k] );
+            }
+    }
+    else
+    {
+        for ( i = 1; i <= p->LutMax; i++ )
+        {
+            if ( p->pLutDelays[i][0] <= 0.0 )
+                printf( "Warning: LUT %d has delay %f. Pin delays should be non-negative numbers. Technology mapping may not work correctly.\n", 
+                    k, i, p->pLutDelays[i][0] );
+        }
+    }
+
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the LUT library.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Lib_t * If_LutLibDup( If_Lib_t * p )
+{
+    If_Lib_t * pNew;
+    pNew = ALLOC( If_Lib_t, 1 );
+    *pNew = *p;
+    pNew->pName = If_UtilStrsav( pNew->pName );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the LUT library.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_LutLibFree( If_Lib_t * pLutLib )
+{
+    if ( pLutLib == NULL )
+        return;
+    FREE( pLutLib->pName );
+    FREE( pLutLib );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the LUT library.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_LutLibPrint( If_Lib_t * pLutLib )
+{
+    int i, k;
+    printf( "# The area/delay of k-variable LUTs:\n" );
+    printf( "# k    area     delay\n" );
+    if ( pLutLib->fVarPinDelays )
+    {
+        for ( i = 1; i <= pLutLib->LutMax; i++ )
+        {
+            printf( "%d   %7.2f  ", i, pLutLib->pLutAreas[i] );
+            for ( k = 0; k < i; k++ )
+                printf( " %7.2f", pLutLib->pLutDelays[i][k] );
+            printf( "\n" );
+        }
+    }
+    else
+        for ( i = 1; i <= pLutLib->LutMax; i++ )
+            printf( "%d   %7.2f   %7.2f\n", i, pLutLib->pLutAreas[i], pLutLib->pLutDelays[i][0] );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the delays are discrete.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_LutLibDelaysAreDiscrete( If_Lib_t * pLutLib )
+{
+    float Delay;
+    int i;
+    for ( i = 1; i <= pLutLib->LutMax; i++ )
+    {
+        Delay = pLutLib->pLutDelays[i][0];
+        if ( ((float)((int)Delay)) != Delay )
+            return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets simple LUT library.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Lib_t * If_SetSimpleLutLib( int nLutSize )
+{
+    If_Lib_t s_LutLib10= { "lutlib",10, 0, {0,1,1,1,1,1,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1},{1},{1},{1},{1},{1}} };
+    If_Lib_t s_LutLib9 = { "lutlib", 9, 0, {0,1,1,1,1,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1},{1},{1},{1},{1}} };
+    If_Lib_t s_LutLib8 = { "lutlib", 8, 0, {0,1,1,1,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1},{1},{1},{1}} };
+    If_Lib_t s_LutLib7 = { "lutlib", 7, 0, {0,1,1,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1},{1},{1}} };
+    If_Lib_t s_LutLib6 = { "lutlib", 6, 0, {0,1,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1},{1}} };
+    If_Lib_t s_LutLib5 = { "lutlib", 5, 0, {0,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1}} };
+    If_Lib_t s_LutLib4 = { "lutlib", 4, 0, {0,1,1,1,1}, {{0},{1},{1},{1},{1}} };
+    If_Lib_t s_LutLib3 = { "lutlib", 3, 0, {0,1,1,1}, {{0},{1},{1},{1}} };
+    If_Lib_t * pLutLib;
+    assert( nLutSize >= 3 && nLutSize <= 10 );
+    switch ( nLutSize )
+    {
+        case 3:  pLutLib = &s_LutLib3; break;
+        case 4:  pLutLib = &s_LutLib4; break;
+        case 5:  pLutLib = &s_LutLib5; break;
+        case 6:  pLutLib = &s_LutLib6; break;
+        case 7:  pLutLib = &s_LutLib7; break;
+        case 8:  pLutLib = &s_LutLib8; break;
+        case 9:  pLutLib = &s_LutLib9; break;
+        case 10: pLutLib = &s_LutLib10; break;
+        default: pLutLib = NULL; break;
+    }
+    if ( pLutLib == NULL )
+        return NULL;
+    return If_LutLibDup(pLutLib);
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index fafd454d..81521abf 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -295,13 +295,6 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPrepr
             {
                 arrTime = Tim_ManGetPiArrival( p->pManTim, pObj->IdPio );
                 If_ObjSetArrTime( pObj, arrTime );
-/*
-    if ( pObj->IdPio >= 2000 )
-    {
-        int x = 0;
-        printf( "+%d %6.3f  ", pObj->IdPio, arrTime );
-    }
-*/
             }
             else if ( If_ObjIsCo(pObj) )
             {
diff --git a/src/map/if/ifUtil.c b/src/map/if/ifUtil.c
index c114236d..74880409 100644
--- a/src/map/if/ifUtil.c
+++ b/src/map/if/ifUtil.c
@@ -653,6 +653,40 @@ Vec_Ptr_t * If_ManCollectMappingDirect( If_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Collects nodes used in the mapping in the topological order.]
+
+  Description [Represents mapping as an array of integers.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * If_ManCollectMappingInt( If_Man_t * p )
+{
+    Vec_Int_t * vOrder;
+    If_Cut_t * pCutBest;
+    If_Obj_t * pObj;
+    int i, k, nLeaves, * ppLeaves;
+    If_ManMarkMapping( p );
+    vOrder = Vec_IntAlloc( If_ManObjNum(p) );
+    If_ManForEachObj( p, pObj, i )
+        if ( If_ObjIsAnd(pObj) && pObj->nRefs )
+        {
+            pCutBest = If_ObjCutBest( pObj );
+            nLeaves  = If_CutLeaveNum( pCutBest ); 
+            ppLeaves = If_CutLeaves( pCutBest );
+            // save the number of leaves, the leaves, and finally, the root
+            Vec_IntPush( vOrder, nLeaves );
+            for ( k = 0; k < nLeaves; k++ )
+                Vec_IntPush( vOrder, ppLeaves[k] );
+            Vec_IntPush( vOrder, pObj->Id );
+        }
+    return vOrder;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns the number of POs pointing to the same internal nodes.]
 
   Description []
diff --git a/src/map/if/module.make b/src/map/if/module.make
index c14428da..7489d3b4 100644
--- a/src/map/if/module.make
+++ b/src/map/if/module.make
@@ -1,5 +1,6 @@
 SRC +=  src/map/if/ifCore.c \
     src/map/if/ifCut.c \
+    src/map/if/ifLib.c \
     src/map/if/ifMan.c \
     src/map/if/ifMap.c \
     src/map/if/ifReduce.c \
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
deleted file mode 100644
index e69de29b..00000000
--- a/src/map/pcm/module.make
+++ /dev/null
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
deleted file mode 100644
index e69de29b..00000000
--- a/src/map/ply/module.make
+++ /dev/null
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 59ee7488..2a2c9d43 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -101,6 +101,7 @@ p->timeSat += clock() - clk;
 int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
 {
     Hop_Obj_t * pObj;
+    int RetValue;
     extern Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare );
 
     int nGain, clk;
@@ -129,8 +130,15 @@ clk = clock();
     if ( p->pSat == NULL )
         return 0;
     // solve the SAT problem
-    Abc_NtkMfsSolveSat( p, pNode );
+    RetValue = Abc_NtkMfsSolveSat( p, pNode );
+    p->nTotConfLevel += p->pSat->stats.conflicts;
 p->timeSat += clock() - clk;
+    if ( RetValue == 0 )
+    {
+        p->nTimeOutsLevel++;
+        p->nTimeOuts++;
+        return 0;
+    }
     // minimize the local function of the node using bi-decomposition
     assert( p->nFanins == Abc_ObjFaninNum(pNode) );
     pObj = Abc_NodeIfNodeResyn( p->pManDec, pNode->pNtk->pManFunc, pNode->pData, p->nFanins, p->vTruth, p->uCare );
@@ -139,6 +147,7 @@ p->timeSat += clock() - clk;
     {
         p->nNodesDec++;
         p->nNodesGained += nGain;
+        p->nNodesGainedLevel += nGain;
         pNode->pData = pObj;    
     }
     return 1;
@@ -163,7 +172,9 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
     ProgressBar * pProgress;
     Mfs_Man_t * p;
     Abc_Obj_t * pObj;
-    int i, nFaninMax, clk = clock();
+    Vec_Vec_t * vLevels;
+    Vec_Ptr_t * vNodes;
+    int i, k, nNodes, nFaninMax, clk = clock(), clk2;
     int nTotalNodesBeg = Abc_NtkNodeNum(pNtk);
     int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk);
 
@@ -223,24 +234,44 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
     Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
 
     // compute don't-cares for each node
+    nNodes = 0;
     p->nTotalNodesBeg = nTotalNodesBeg;
     p->nTotalEdgesBeg = nTotalEdgesBeg;
-    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
-    Abc_NtkForEachNode( pNtk, pObj, i )
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
+    vLevels = Abc_NtkLevelize( pNtk );
+    Vec_VecForEachLevelStart( vLevels, vNodes, k, 1 )
     {
-        if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
-            continue;
-        if ( Abc_ObjFaninNum(pObj) > MFS_FANIN_MAX )
-            continue;
         if ( !p->pPars->fVeryVerbose )
-            Extra_ProgressBarUpdate( pProgress, i, NULL );
-        if ( pPars->fResub )
-            Abc_NtkMfsResub( p, pObj );
-        else if ( Abc_ObjFaninNum(pObj) > 1 && Abc_ObjFaninNum(pObj) <= 12 )
-            Abc_NtkMfsNode( p, pObj );
+            Extra_ProgressBarUpdate( pProgress, nNodes, NULL );
+        p->nNodesGainedLevel = 0;
+        p->nTotConfLevel = 0;
+        p->nTimeOutsLevel = 0;
+        clk2 = clock();
+        Vec_PtrForEachEntry( vNodes, pObj, i )
+        {
+            if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
+                break;
+            if ( Abc_ObjFaninNum(pObj) > MFS_FANIN_MAX )
+                continue;
+            if ( pPars->fResub )
+                Abc_NtkMfsResub( p, pObj );
+            else if ( Abc_ObjFaninNum(pObj) > 1 && Abc_ObjFaninNum(pObj) <= 12 )
+                Abc_NtkMfsNode( p, pObj );
+        }
+        nNodes += Vec_PtrSize(vNodes);
+        if ( pPars->fVerbose )
+        {
+        printf( "Lev = %2d. Node = %4d. Ave gain = %6.2f. Ave conf = %6.2f. Timeouts = %6.2f %%  ", 
+            k, Vec_PtrSize(vNodes),
+            1.0*p->nNodesGainedLevel/Vec_PtrSize(vNodes),
+            1.0*p->nTotConfLevel/Vec_PtrSize(vNodes),
+            100.0*p->nTimeOutsLevel/Vec_PtrSize(vNodes) );
+        PRT( "Time", clock() - clk2 );
+        }
     }
     Extra_ProgressBarStop( pProgress );
     Abc_NtkStopReverseLevels( pNtk );
+    Vec_VecFree( vLevels );
 
     // perform the sweeping
     if ( !pPars->fResub )
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index f4da45ef..37521189 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -70,6 +70,7 @@ struct Mfs_Man_t_
     Bdc_Man_t *         pManDec;
     int                 nNodesDec;
     int                 nNodesGained;
+    int                 nNodesGainedLevel;
     // solving data
     Aig_Man_t *         pAigWin;   // window AIG with constraints
     Cnf_Dat_t *         pCnf;      // the CNF for the window
@@ -78,6 +79,8 @@ struct Mfs_Man_t_
     Vec_Int_t *         vMem;      // memory for intermediate SOPs
     Vec_Vec_t *         vLevels;   // levelized structure for updating
     Vec_Ptr_t *         vFanins;   // the new set of fanins
+    int                 nTotConfLim; // total conflict limit
+    int                 nTotConfLevel; // total conflicts on this level
     // the result of solving
     int                 nFanins;   // the number of fanins
     int                 nWords;    // the number of words
@@ -91,6 +94,7 @@ struct Mfs_Man_t_
     int                 nNodesBad;
     int                 nTotalDivs;
     int                 nTimeOuts;
+    int                 nTimeOutsLevel;
     int                 nDcMints;
     double              dTotalRatios;
     // node/edge stats
@@ -136,7 +140,7 @@ extern int              Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode
 extern int              Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode );
 extern int              Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode );
 /*=== mfsSat.c ==========================================================*/
-extern void             Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode );
+extern int              Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode );
 /*=== mfsStrash.c ==========================================================*/
 extern Aig_Man_t *      Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode );
 extern double           Abc_NtkConstraintRatio( Mfs_Man_t * p, Abc_Obj_t * pNode );
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index f1b3f44c..d0642368 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -126,13 +126,13 @@ void Mfs_ManPrint( Mfs_Man_t * p )
     }
     else
     {
-        printf( "Nodes = %d.  DC mints in local space = %d. Total mints = %d. Ratio = %5.2f.\n", 
-            p->nNodesTried, p->nMintsTotal-p->nMintsCare, p->nMintsTotal, 
+        printf( "Nodes = %d. Try = %d. Total mints = %d. Local DC mints = %d. Ratio = %5.2f.\n", 
+            Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nMintsTotal, p->nMintsTotal-p->nMintsCare, 
             1.0 * (p->nMintsTotal-p->nMintsCare) / p->nMintsTotal );
 //        printf( "Average ratio of sequential DCs in the global space = %5.2f.\n", 
 //            1.0-(p->dTotalRatios/p->nNodesTried) );
-        printf( "Nodes resyn = %d. Ratio = %5.2f.  Total AIG node gain = %d.\n", 
-            p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained );
+        printf( "Nodes resyn = %d. Ratio = %5.2f.  Total AIG node gain = %d. Timeouts = %d.\n", 
+            p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained, p->nTimeOuts );
     }
 /*
     PRTP( "Win", p->timeWin            ,  p->timeTotal );
diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c
index 2529e207..5023bf62 100644
--- a/src/opt/mfs/mfsSat.c
+++ b/src/opt/mfs/mfsSat.c
@@ -42,9 +42,14 @@
 int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p )
 {
     int Lits[MFS_FANIN_MAX];
-    int RetValue, iVar, b, Mint;
-    RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
-    assert( RetValue == l_False || RetValue == l_True );
+    int RetValue, nBTLimit, iVar, b, Mint;
+    if ( p->nTotConfLim && p->nTotConfLim <= p->pSat->stats.conflicts )
+        return -1;
+    nBTLimit = p->nTotConfLim? p->nTotConfLim - p->pSat->stats.conflicts : 0;
+    RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    assert( RetValue == l_Undef || RetValue == l_True || RetValue == l_False );
+    if ( RetValue == l_Undef )
+        return -1;
     if ( RetValue == l_False )
         return 0;
     p->nCares++;
@@ -77,12 +82,12 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p )
   SideEffects []
 
   SeeAlso     []
-
+ 
 ***********************************************************************/
-void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
+int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
 {
     Aig_Obj_t * pObjPo;
-    int i;
+    int RetValue, i;
     // collect projection variables
     Vec_IntClear( p->vProjVars );
     Vec_PtrForEachEntryStart( p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Abc_ObjFaninNum(pNode) )
@@ -98,7 +103,10 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
 
     // iterate through the SAT assignments
     p->nCares = 0;
-    while ( Abc_NtkMfsSolveSat_iter(p) );
+    p->nTotConfLim = p->pPars->nBTLimit;
+    while ( (RetValue = Abc_NtkMfsSolveSat_iter(p)) == 1 );
+    if ( RetValue == -1 )
+        return 0;
 
     // write statistics
     p->nMintsCare  += p->nCares;
@@ -113,7 +121,7 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
 
     // map the care 
     if ( p->nFanins > 4 )
-        return;
+        return 1;
     if ( p->nFanins == 4 )
         p->uCare[0] = p->uCare[0] | (p->uCare[0] << 16);
     if ( p->nFanins == 3 )
@@ -122,6 +130,7 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
         p->uCare[0] = p->uCare[0] | (p->uCare[0] <<  4) | (p->uCare[0] <<  8) | (p->uCare[0] << 12) |
               (p->uCare[0] << 16) | (p->uCare[0] << 20) | (p->uCare[0] << 24) | (p->uCare[0] << 28);
     assert( p->nFanins != 1 );
+    return 1;
 }
 
 ////////////////////////////////////////////////////////////////////////