Version abc80402

0080244a · Alan Mishchenko · 2c7f6e39 · 0080244a · 0080244a · 0080244a
Commit 0080244a authored Apr 02, 2008 by Alan Mishchenko
44 changed files
--- a/abc.dsp
+++ b/abc.dsp
@@ -42,7 +42,7 @@ RSC=rc.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
-# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
+# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
 # ADD BASE RSC /l 0x409 /d "NDEBUG"
 # ADD RSC /l 0x409 /d "NDEBUG"
 BSC32=bscmake.exe
@@ -66,7 +66,7 @@ LINK32=link.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
-# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
+# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
 # SUBTRACT CPP /X
 # ADD BASE RSC /l 0x409 /d "_DEBUG"
 # ADD RSC /l 0x409 /d "_DEBUG"

--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -444,6 +444,7 @@ extern void            Aig_ManCheckPhase( Aig_Man_t * p );
 extern Aig_ManCut_t *  Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fTruth, int fVerbose );
 extern void            Aig_ManCutStop( Aig_ManCut_t * p );
 /*=== aigDfs.c ==========================================================*/
+extern int             Aig_ManVerifyTopoOrder( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManDfs( Aig_Man_t * p );
 extern Vec_Vec_t *     Aig_ManLevelize( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManDfsPio( Aig_Man_t * p );

--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 #include "aig.h"
+#include "tim.h"
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -30,6 +31,79 @@
 /**Function*************************************************************
+  Synopsis    [Verifies that the objects are in a topo order.]
+  Description []
+  SideEffects []
+  SeeAlso     []
+***********************************************************************/
+int Aig_ManVerifyTopoOrder( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj, * pNext;
+    int i, iBox, iTerm1, nTerms;
+    Aig_ManSetPioNumbers( p );
+    Aig_ManIncrementTravId( p );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjIsNode(pObj) )
+        {
+            pNext = Aig_ObjFanin0(pObj);
+            if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
+            {
+                printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id );
+                return 0;
+            }
+            pNext = Aig_ObjFanin1(pObj);
+            if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
+            {
+                printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id );
+                return 0;
+            }
+        }
+        else if ( Aig_ObjIsPo(pObj) )
+        {
+            pNext = Aig_ObjFanin0(pObj);
+            if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
+            {
+                printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id );
+                return 0;
+            }
+        }
+        else if ( Aig_ObjIsPi(pObj) )
+        {
+            if ( p->pManTime )
+            {
+                iBox = Tim_ManBoxForCi( p->pManTime, Aig_ObjPioNum(pObj) );
+                if ( iBox >= 0 ) // this is not a true PI
+                {
+                    iTerm1 = Tim_ManBoxInputFirst( p->pManTime, iBox );
+                    nTerms = Tim_ManBoxInputNum( p->pManTime, iBox );
+                    for ( i = 0; i < nTerms; i++ )
+                    {
+                        pNext = Aig_ManPo( p, iTerm1 + i );
+                        assert( Tim_ManBoxForCo( p->pManTime, Aig_ObjPioNum(pNext) ) == iBox ); 
+                        if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
+                        {
+                            printf( "Box %d has input %d that is not in a topological order.\n", iBox, pNext->Id );
+                            return 0;
+                        }
+                    }
+                }
+            }
+        }
+        else
+            assert( 0 );
+        Aig_ObjSetTravIdCurrent( p, pObj );
+    }
+    Aig_ManCleanPioNumbers( p );
+    return 1;
+}
+/**Function*************************************************************
  Synopsis    [Collects internal nodes in the DFS order.]
  Description []

--- a/src/aig/aig/aigFrames.c
+++ b/src/aig/aig/aigFrames.c
@@ -59,6 +59,7 @@ Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int 
    // start the fraig package
    pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFs );
    pFrames->pName = Aig_UtilStrsav( pAig->pName );
+    pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec );
    // map constant nodes
    for ( f = 0; f < nFs; f++ )
        Aig_ObjSetFrames( pObjMap, nFs, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );

--- a/src/aig/aig/aigHaig.c
+++ b/src/aig/aig/aigHaig.c
@@ -101,6 +101,7 @@ Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames )
    // start the frames
    pFrames = Aig_ManStart( Aig_ManObjNumMax(pHaig) * nFrames );
    pFrames->pName = Aig_UtilStrsav( pHaig->pName );
+    pFrames->pSpec = Aig_UtilStrsav( pHaig->pSpec );
    pFrames->nRegs = pHaig->nRegs;
    // create PI nodes for the frames

--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -90,6 +90,7 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
    // create the new manager
    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
    // create the PIs
    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
    Aig_ManForEachPi( p, pObj, i )
@@ -122,6 +123,7 @@ Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p )
    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
    pNew->fCatchExor = 1;
    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
    pNew->nRegs = p->nRegs;
    pNew->nAsserts = p->nAsserts;
    if ( p->vFlopNums )
@@ -213,6 +215,7 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
    // create the new manager
    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
    pNew->nRegs = p->nRegs;
    pNew->nAsserts = p->nAsserts;
    if ( p->vFlopNums )
@@ -254,7 +257,6 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
    else
    {
 /*
        Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
        Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
        Aig_ManForEachObj( p, pObj, i )
@@ -276,6 +278,7 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
            }
        }
 */
        Vec_Vec_t * vLevels;
        int k;
@@ -399,6 +402,7 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
    // create the new manager
    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
    pNew->nRegs = p->nRegs;
    pNew->nAsserts = p->nAsserts;
    if ( p->vFlopNums )
@@ -481,6 +485,7 @@ Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p )
    // create the new manager
    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
    // create the PIs
    Aig_ManCleanData( p );
    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@@ -515,6 +520,7 @@ Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * 
    // create the new manager
    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
    // create the PIs
    Aig_ManCleanData( p );
    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);

--- a/src/aig/aig/aigMem.c
+++ b/src/aig/aig/aigMem.c
@@ -68,6 +68,10 @@ struct Aig_MmStep_t_
    Aig_MmFixed_t **  pMems;    // memory managers: 2^1 words, 2^2 words, etc
    int               nMapSize; // the size of the memory array
    Aig_MmFixed_t **  pMap;     // maps the number of bytes into its memory manager
+    // additional memory chunks
+    int           nChunksAlloc;  // the maximum number of memory chunks 
+    int           nChunks;       // the current number of memory chunks 
+    char **       pChunks;       // the allocated memory
 };
 #define ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
@@ -486,6 +490,9 @@ Aig_MmStep_t * Aig_MmStepStart( int nSteps )
            p->pMap[k] = p->pMems[i];
 //for ( i = 1; i < 100; i ++ )
 //printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize );
+    p->nChunksAlloc  = 64;
+    p->nChunks       = 0;
+    p->pChunks       = ALLOC( char *, p->nChunksAlloc );
    return p;
 }
@@ -505,12 +512,12 @@ void Aig_MmStepStop( Aig_MmStep_t * p, int fVerbose )
    int i;
    for ( i = 0; i < p->nMems; i++ )
        Aig_MmFixedStop( p->pMems[i], fVerbose );
-//    if ( p->pLargeChunks ) 
+    if ( p->nChunksAlloc )
-//    {
+    {
-//      for ( i = 0; i < p->nLargeChunks; i++ )
+        for ( i = 0; i < p->nChunks; i++ )
-//          free( p->pLargeChunks[i] );
+            free( p->pChunks[i] );
-//      free( p->pLargeChunks );
+        free( p->pChunks );
-//    }
+    }
    free( p->pMems );
    free( p->pMap );
    free( p );
@@ -533,19 +540,13 @@ char * Aig_MmStepEntryFetch( Aig_MmStep_t * p, int nBytes )
        return NULL;
    if ( nBytes > p->nMapSize )
    {
-//        printf( "Allocating %d bytes.\n", nBytes );
+        if ( p->nChunks == p->nChunksAlloc )
-/*
-        if ( p->nLargeChunks == p->nLargeChunksAlloc )
        {
-            if ( p->nLargeChunksAlloc == 0 )
+            p->nChunksAlloc *= 2;
-                p->nLargeChunksAlloc = 5;
+            p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
-            p->nLargeChunksAlloc *= 2;
-            p->pLargeChunks = REALLOC( char *, p->pLargeChunks, p->nLargeChunksAlloc ); 
        }
-        p->pLargeChunks[ p->nLargeChunks++ ] = ALLOC( char, nBytes );
+        p->pChunks[ p->nChunks++ ] = ALLOC( char, nBytes );
-        return p->pLargeChunks[ p->nLargeChunks - 1 ];
+        return p->pChunks[p->nChunks-1];
-*/
-        return ALLOC( char, nBytes );
    }
    return Aig_MmFixedEntryFetch( p->pMap[nBytes] );
 }
@@ -568,7 +569,7 @@ void Aig_MmStepEntryRecycle( Aig_MmStep_t * p, char * pEntry, int nBytes )
        return;
    if ( nBytes > p->nMapSize )
    {
-        free( pEntry );
+//        free( pEntry );
        return;
    }
    Aig_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );

--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -142,6 +142,7 @@ void Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFan0, Aig_Obj
    // add the node to the dynamically updated topological order
 //    if ( p->pOrderData && Aig_ObjIsNode(pObj) )
 //        Aig_ObjOrderInsert( p, pObj->Id );
+    assert( !Aig_ObjIsNode(pObj) || pObj->Level > 0 );
 }
 /**Function*************************************************************

--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -1494,7 +1494,7 @@ void Aig_ManChoiceLevel_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
        LevelMax++;
        // get the level of the nodes in the choice node
-        if ( pNew->pEquivs && (pNext = pNew->pEquivs[pObj->iData]) )
+        if ( pNew->pEquivs && (pNext = pNew->pEquivs[pObj->Id]) )
        {
            Aig_ManChoiceLevel_rec( pNew, pNext );
            if ( LevelMax < Aig_ObjLevel(pNext) )
@@ -1504,6 +1504,7 @@ void Aig_ManChoiceLevel_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
    else
        assert( 0 );
    Aig_ObjSetLevel( pObj, LevelMax );
+    assert( !Aig_ObjIsNode(pObj) || LevelMax > 0 );
 }
 /**Function*************************************************************
@@ -1546,6 +1547,46 @@ int Aig_ManChoiceLevel( Aig_Man_t * pNew )
  SeeAlso     []
 ***********************************************************************/
+void Aig_ManChoiceEval( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vSupp;
+    Aig_Obj_t * pNode, * pTemp;
+    int i, Counter;
+    vSupp = Vec_PtrAlloc( 100 );
+    Aig_ManForEachNode( p, pNode, i )
+    {
+        if ( !Aig_ObjIsChoice(p, pNode) )
+            continue; 
+        if ( pNode->Id == 4225 )
+        {
+            int x = 0;
+        }
+        Counter = 0;
+        for ( pTemp = pNode; pTemp; pTemp = p->pEquivs[pTemp->Id] )
+            Counter++;
+        printf( "Choice node = %5d. Level = %2d. Choices = %d. { ", pNode->Id, pNode->Level, Counter );
+        for ( pTemp = pNode; pTemp; pTemp = p->pEquivs[pTemp->Id] )
+        {
+            Counter = Aig_NodeMffsSupp( p, pTemp, 0, vSupp );
+            printf( "S=%d N=%d L=%d  ", Vec_PtrSize(vSupp), Counter, pTemp->Level );
+        }
+        printf( "}\n" );
+    }
+    Vec_PtrFree( vSupp );
+}
+/**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;
@@ -1573,6 +1614,7 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
 //Aig_ManPrintStats( pNew );
    // reset levels
    Aig_ManChoiceLevel( pNew );
+//    Aig_ManChoiceEval( pNew );
    return pNew;
 }

--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -269,6 +269,7 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered )
    // start the HOP package
    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
    pNew->nRegs = p->nRegs;
    if ( p->vFlopNums )
        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );

--- a/src/aig/aig/aigRet.c
+++ b/src/aig/aig/aigRet.c
@@ -950,6 +950,7 @@ clk = clock();
    // get the new manager
    pNew = Rtm_ManToAig( pRtm );
    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
    Rtm_ManFree( pRtm );
    // group the registers
 clk = clock();

--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -48,6 +48,7 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
    // create the new manager
    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
    pNew->nRegs = p->nRegs;
    pNew->nAsserts = p->nAsserts;
    if ( p->vFlopNums )

--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -80,6 +80,7 @@ extern void            Dar_LibStart();
 extern void            Dar_LibStop();
 /*=== darBalance.c ========================================================*/
 extern Aig_Man_t *     Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel );
+extern Aig_Man_t *     Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose );
 extern void            Dar_BalancePrintStats( Aig_Man_t * p );
 /*=== darCore.c ========================================================*/
 extern void            Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars );
@@ -94,7 +95,6 @@ extern Aig_Man_t *     Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbos
 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 fConstruct, int nConfMax, int nLevelMax, int fVerbose );
-extern Aig_Man_t *     Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose );
 #ifdef __cplusplus
 }

--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -333,7 +333,7 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * 
    if ( vSuper->nSize == 0 )
        return pObjOld->pData = Aig_ManConst0(pNew);
    if ( Vec_PtrSize(vSuper) < 2 )
-        printf( "BUG!\n" );
+        printf( "Dar_Balance_rec: Internal error!\n" );
    // for each old node, derive the new well-balanced node
    for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
    {
@@ -366,9 +366,11 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
    Aig_Obj_t * pObj, * pDriver, * pObjNew;
    Vec_Vec_t * vStore;
    int i;
+    assert( Aig_ManVerifyTopoOrder(p) );
    // create the new manager 
    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
    pNew->nRegs = p->nRegs;
    pNew->nAsserts = p->nAsserts;
    if ( p->vFlopNums )
@@ -439,6 +441,35 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
 /**Function*************************************************************
+  Synopsis    [Reproduces script "compress2".]
+  Description []
+  SideEffects []
+  SeeAlso     []
+***********************************************************************/
+Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose )
+{
+    Aig_Man_t * pAigXor, * pRes;
+    if ( fExor )
+    {
+        pAigXor = Aig_ManDupExor( pAig );
+        if ( fVerbose )
+            Dar_BalancePrintStats( pAigXor );
+        pRes = Dar_ManBalance( pAigXor, fUpdateLevel );
+        Aig_ManStop( pAigXor );
+    }
+    else
+    {
+        pRes = Dar_ManBalance( pAig, fUpdateLevel );
+    }
+    return pRes;
+}
+/**Function*************************************************************
  Synopsis    [Inserts a new node in the order by levels.]
  Description []

--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -341,11 +341,19 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL
 //Aig_ManPrintStats( pAig );
    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        pObj->pNext = pObj->pHaig;
        pObj->pHaig = pObj;
+    }
    pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fVerbose);
    Vec_PtrPush( vAigs, pAig );
 //Aig_ManPrintStats( pAig );
+    pAig = Vec_PtrEntry( vAigs, 1 );
+    Aig_ManForEachObj( pAig, pObj, i )
+        pObj->pHaig = pObj->pNext;
    return vAigs;
 }
@@ -399,35 +407,6 @@ PRT( "Choicing time ", clock() - clk );
 //    return NULL;
 }
-/**Function*************************************************************
-  Synopsis    [Reproduces script "compress2".]
-  Description []
-  SideEffects []
-  SeeAlso     []
-***********************************************************************/
-Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose )
-{
-    Aig_Man_t * pAigXor, * pRes;
-    if ( fExor )
-    {
-        pAigXor = Aig_ManDupExor( pAig );
-        if ( fVerbose )
-            Dar_BalancePrintStats( pAigXor );
-        pRes = Dar_ManBalance( pAigXor, fUpdateLevel );
-        Aig_ManStop( pAigXor );
-    }
-    else
-    {
-        pRes = Dar_ManBalance( pAig, fUpdateLevel );
-    }
-    return pRes;
-}
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

--- a/src/aig/fra/fraBmc.c
+++ b/src/aig/fra/fraBmc.c
@@ -241,6 +241,7 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos )
    // start the fraig package
    pAigFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFramesAll );
    pAigFrames->pName = Aig_UtilStrsav( p->pAig->pName );
+    pAigFrames->pSpec = Aig_UtilStrsav( p->pAig->pSpec );
    // create PI nodes for the frames
    for ( f = 0; f < p->nFramesAll; f++ )
        Bmc_ObjSetFrames( Aig_ManConst1(p->pAig), f, Aig_ManConst1(pAigFrames) );

--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -801,6 +801,7 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
    // start the fraig package
    pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * nFramesAll );
    pManFraig->pName = Aig_UtilStrsav( p->pAig->pName );
+    pManFraig->pSpec = Aig_UtilStrsav( p->pAig->pSpec );
    // allocate place for the node mapping
    ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
    Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) );

--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -134,6 +134,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
    // start the fraig package
    pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) * p->nFramesAll );
    pManFraig->pName = Aig_UtilStrsav( p->pManAig->pName );
+    pManFraig->pSpec = Aig_UtilStrsav( p->pManAig->pSpec );
    pManFraig->nRegs = p->pManAig->nRegs;
    // create PI nodes for the frames
    for ( f = 0; f < p->nFramesAll; f++ )

--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -178,6 +178,7 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p )
    // start the fraig package
    pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) );
    pManFraig->pName = Aig_UtilStrsav( p->pManAig->pName );
+    pManFraig->pSpec = Aig_UtilStrsav( p->pManAig->pSpec );
    pManFraig->nRegs    = p->pManAig->nRegs;
    pManFraig->nAsserts = p->pManAig->nAsserts;
    // set the pointers to the available fraig nodes

--- a/src/aig/kit/kitDsd.c
+++ b/src/aig/kit/kitDsd.c
@@ -2111,8 +2111,8 @@ void Kit_DsdTest( unsigned * pTruth, int nVars )
 //    if ( Kit_DsdNtkRoot(pNtk)->nFans == (unsigned)nVars && nVars == 6 )
-    printf( "\n" );
+//    printf( "\n" );
-    Kit_DsdPrint( stdout, pNtk );
+//    Kit_DsdPrint( stdout, pNtk );
    pNtk = Kit_DsdExpand( pTemp = pNtk );
    Kit_DsdNtkFree( pTemp );

--- a/src/aig/mem/mem.c
+++ b/src/aig/mem/mem.c
@@ -574,7 +574,7 @@ void Mem_StepEntryRecycle( Mem_Step_t * p, char * pEntry, int nBytes )
        return;
    if ( nBytes > p->nMapSize )
    {
-        free( pEntry );
+//        free( pEntry );
        return;
    }
    Mem_FixedEntryRecycle( p->pMap[nBytes], pEntry );

--- a/src/aig/mfx/mfxCore.c
+++ b/src/aig/mfx/mfxCore.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 #include "mfxInt.h"
+#include "bar.h"
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -83,8 +84,8 @@ p->timeWin += clock() - clk;
        return 1;
    // compute the divisors of the window
 clk = clock();
-//    p->vDivs  = Mfx_ComputeDivisors( p, pNode, Nwk_ObjRequired(pNode) - If_LutLibSlowestPinDelay(pNode->pMan->pLutLib) );
+    p->vDivs  = Mfx_ComputeDivisors( p, pNode, Nwk_ObjRequired(pNode) - If_LutLibSlowestPinDelay(pNode->pMan->pLutLib) );
-    p->vDivs  = Mfx_ComputeDivisors( p, pNode, AIG_INFINITY );
+//    p->vDivs  = Mfx_ComputeDivisors( p, pNode, AIG_INFINITY );
    p->nTotalDivs += Vec_PtrSize(p->vDivs);
 p->timeDiv += clock() - clk;
    // construct AIG for the window
@@ -192,10 +193,10 @@ p->timeSat += clock() - clk;
  SeeAlso     []
 ***********************************************************************/
-int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars )
+int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib )
 {
    Bdc_Par_t Pars = {0}, * pDecPars = &Pars;
-//    ProgressBar * pProgress;
+    Bar_Progress_t * pProgress;
    Mfx_Man_t * p;
    Tim_Man_t * pManTimeOld = NULL;
    Nwk_Obj_t * pObj;
@@ -223,23 +224,19 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars )
            nFaninMax = MFX_FANIN_MAX;
        }
    }
+    if ( pLutLib && pLutLib->LutMax < nFaninMax )
-/*
-    // prepare timing information
-    if ( pNtk->pManTime )
    {
+        printf( "The selected LUT library with max LUT size (%d) cannot be used to compute timing for network with %d-input nodes. Using unit-delay model.\n", pLutLib->LutMax, nFaninMax );
+        pLutLib = NULL;
+    }
+    pNtk->pLutLib = pLutLib;
    // compute levels
    Nwk_ManLevel( pNtk );
+    assert( Nwk_ManVerifyLevel( pNtk ) );
    // compute delay trace with white-boxes
-        Nwk_ManDelayTraceLut( pNtk, pNtk->pLutLib );
+    Nwk_ManDelayTraceLut( pNtk );
-        // save the general timing manager
+    assert( Nwk_ManVerifyTiming( pNtk ) );
-        pManTimeOld = pNtk->pManTime;
-        // derive an approximate timing manager without white-boxes
-        pNtk->pManTime = Tim_ManDupApprox( pNtk->pManTime );
-    }
-    // compute delay trace with the given timing manager
-    Nwk_ManDelayTraceLut( pNtk, pNtk->pLutLib );
-*/
    // start the manager
    p = Mfx_ManAlloc( pPars );
@@ -259,27 +256,27 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars )
    p->nTotalEdgesBeg = nTotalEdgesBeg;
    if ( pPars->fResub )
    {
-//        pProgress = Extra_ProgressBarStart( stdout, Nwk_ObjNumMax(pNtk) );
+        pProgress = Bar_ProgressStart( stdout, Nwk_ManObjNumMax(pNtk) );
        Nwk_ManForEachNode( pNtk, pObj, i )
        {
            if ( p->pPars->nDepthMax && pObj->Level > p->pPars->nDepthMax )
                continue;
            if ( Nwk_ObjFaninNum(pObj) < 2 || Nwk_ObjFaninNum(pObj) > nFaninMax )
                continue;
-//            if ( !p->pPars->fVeryVerbose )
+            if ( !p->pPars->fVeryVerbose )
-//                Extra_ProgressBarUpdate( pProgress, i, NULL );
+                Bar_ProgressUpdate( pProgress, i, NULL );
            Mfx_Resub( p, pObj );
        }
-//        Extra_ProgressBarStop( pProgress );
+        Bar_ProgressStop( pProgress );
    }
    else
    {
-//        pProgress = Extra_ProgressBarStart( stdout, Nwk_NodeNum(pNtk) );
+        pProgress = Bar_ProgressStart( stdout, Nwk_ManNodeNum(pNtk) );
        vLevels = Nwk_ManLevelize( pNtk );
        Vec_VecForEachLevelStart( vLevels, vNodes, k, 1 )
        {
-//            if ( !p->pPars->fVeryVerbose )
+            if ( !p->pPars->fVeryVerbose )
-//                Extra_ProgressBarUpdate( pProgress, nNodes, NULL );
+                Bar_ProgressUpdate( pProgress, nNodes, NULL );
            p->nNodesGainedLevel = 0;
            p->nTotConfLevel = 0;
            p->nTimeOutsLevel = 0;
@@ -303,20 +300,15 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars )
            PRT( "Time", clock() - clk2 );
            }
        }
-//        Extra_ProgressBarStop( pProgress );
+        Bar_ProgressStop( pProgress );
        Vec_VecFree( vLevels );
    }
    p->nTotalNodesEnd = Nwk_ManNodeNum(pNtk);
    p->nTotalEdgesEnd = Nwk_ManGetTotalFanins(pNtk);
-/*
-    // reset the timing manager
+    assert( Nwk_ManVerifyLevel( pNtk ) );
-    if ( pNtk->pManTime )
+    assert( Nwk_ManVerifyTiming( pNtk ) );
-    {
-        Tim_ManStop( pNtk->pManTime );
-        pNtk->pManTime = pManTimeOld;
-    }
-    Nwk_ManVerifyLevel( pNtk );
-*/
    // free the manager
    p->timeTotal = clock() - clk;
    Mfx_ManStop( p );

--- a/src/aig/mfx/mfxDiv.c
+++ b/src/aig/mfx/mfxDiv.c
@@ -88,17 +88,17 @@ Vec_Ptr_t * Abc_MfxWinMarkTfi( Nwk_Obj_t * pNode )
  SeeAlso     []
 ***********************************************************************/
-void Abc_MfxWinSweepLeafTfo_rec( Nwk_Obj_t * pObj, int nLevelLimit )
+void Abc_MfxWinSweepLeafTfo_rec( Nwk_Obj_t * pObj, float tArrivalMax )
 {
    Nwk_Obj_t * pFanout;
    int i;
-    if ( Nwk_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit )
+    if ( Nwk_ObjIsCo(pObj) || Nwk_ObjArrival(pObj) > tArrivalMax )
        return;
    if ( Nwk_ObjIsTravIdCurrent(pObj) )
        return;
    Nwk_ObjSetTravIdCurrent( pObj );
    Nwk_ObjForEachFanout( pObj, pFanout, i )
-        Abc_MfxWinSweepLeafTfo_rec( pFanout, nLevelLimit );
+        Abc_MfxWinSweepLeafTfo_rec( pFanout, tArrivalMax );
 }
 /**Function*************************************************************
@@ -187,7 +187,7 @@ int Abc_MfxWinVisitMffc( Nwk_Obj_t * pNode )
  SeeAlso     []
 ***********************************************************************/
-Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMax )
+Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, float tArrivalMax )
 {
    Vec_Ptr_t * vCone, * vDivs;
    Nwk_Obj_t * pObj, * pFanout, * pFanin;
@@ -210,7 +210,7 @@ Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMa
    // (2) the MFFC of the node
    // (3) the node's fanins (these are treated as a special case)
    Nwk_ManIncrementTravId( pNode->pMan );
-    Abc_MfxWinSweepLeafTfo_rec( pNode, nLevDivMax );
+    Abc_MfxWinSweepLeafTfo_rec( pNode, tArrivalMax );
    Abc_MfxWinVisitMffc( pNode );
    Nwk_ObjForEachFanin( pNode, pObj, k )
        Nwk_ObjSetTravIdCurrent( pObj );
@@ -225,7 +225,7 @@ Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMa
    {
        if ( !Nwk_ObjIsTravIdPrevious(pObj) )
            continue;
-        if ( (int)pObj->Level > nLevDivMax )
+        if ( Nwk_ObjArrival(pObj) > tArrivalMax )
            continue;
        Vec_PtrPush( vDivs, pObj );
        if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
@@ -253,7 +253,7 @@ Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMa
            if ( !Nwk_ObjIsNode(pFanout) ) 
                continue;
            // skip nodes with large level
-            if ( (int)pFanout->Level > nLevDivMax )
+            if ( Nwk_ObjArrival(pFanout) > tArrivalMax )
                continue;
            // skip nodes whose fanins are not divisors
            Nwk_ObjForEachFanin( pFanout, pFanin, m )

--- a/src/aig/mfx/mfxInt.h
+++ b/src/aig/mfx/mfxInt.h
@@ -125,7 +125,7 @@ struct Mfx_Man_t_
 ////////////////////////////////////////////////////////////////////////
 /*=== mfxDiv.c ==========================================================*/
-extern Vec_Ptr_t *      Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMax );
+extern Vec_Ptr_t *      Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, float tArrivalMax );
 /*=== mfxInter.c ==========================================================*/
 extern sat_solver *     Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int fInvert );
 extern Hop_Obj_t *      Mfx_Interplate( Mfx_Man_t * p, int * pCands, int nCands );

--- a/src/aig/mfx/mfxMan.c
+++ b/src/aig/mfx/mfxMan.c
@@ -120,8 +120,8 @@ void Mfx_ManPrint( Mfx_Man_t * p )
        if ( p->pPars->fSwapEdge )
            printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n", 
                p->nNodesResub, Nwk_ManGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Nwk_ManGetTotalFanins(p->pNtk) );
-        else
+//        else
-            Mfx_PrintResubStats( p );
+//            Mfx_PrintResubStats( p );
 //        printf( "Average ratio of DCs in the resubed nodes = %.2f.\n", 1.0*p->nDcMints/(64 * p->nNodesResub) );
    }
    else

--- a/src/aig/mfx/mfxResub.c
+++ b/src/aig/mfx/mfxResub.c
@@ -45,17 +45,10 @@ void Mfx_UpdateNetwork( Mfx_Man_t * p, Nwk_Obj_t * pObj, Vec_Ptr_t * vFanins, Ho
    int k;
    // create the new node
    pObjNew = Nwk_ManCreateNode( pObj->pMan, Vec_PtrSize(vFanins), Nwk_ObjFanoutNum(pObj) );
-if ( pObjNew->Id == 19969 )
-{
-    int x = 0;
-}
    pObjNew->pFunc = pFunc;
    Vec_PtrForEachEntry( vFanins, pFanin, k )
        Nwk_ObjAddFanin( pObjNew, pFanin );
    // replace the old node by the new node
-//printf( "Replacing node " ); Nwk_ObjPrint( stdout, pObj );
-//printf( "Inserting node " ); Nwk_ObjPrint( stdout, pObjNew );
-    // update the level of the node
    Nwk_ManUpdate( pObj, pObjNew, p->vLevels );
 }

--- a/src/aig/nwk/nwk.h
+++ b/src/aig/nwk/nwk.h
@@ -131,6 +131,7 @@ static inline Nwk_Obj_t * Nwk_ObjFanout0( Nwk_Obj_t * p )         { return p->pF
 static inline Nwk_Obj_t * Nwk_ObjFanin( Nwk_Obj_t * p, int i )    { return p->pFanio[i];                        } 
 static inline Nwk_Obj_t * Nwk_ObjFanout( Nwk_Obj_t * p, int i )   { return p->pFanio[p->nFanins+1];             } 
+static inline int         Nwk_ObjIsNone( Nwk_Obj_t * p )          { return p->Type == NWK_OBJ_NONE;             } 
 static inline int         Nwk_ObjIsCi( Nwk_Obj_t * p )            { return p->Type == NWK_OBJ_CI;               } 
 static inline int         Nwk_ObjIsCo( Nwk_Obj_t * p )            { return p->Type == NWK_OBJ_CO;               } 
 static inline int         Nwk_ObjIsNode( Nwk_Obj_t * p )          { return p->Type == NWK_OBJ_NODE;             } 
@@ -154,6 +155,10 @@ static inline void        Nwk_ObjSetTravIdPrevious( Nwk_Obj_t * pObj )       { p
 static inline int         Nwk_ObjIsTravIdCurrent( Nwk_Obj_t * pObj )         { return pObj->TravId == pObj->pMan->nTravIds;     }
 static inline int         Nwk_ObjIsTravIdPrevious( Nwk_Obj_t * pObj )        { return pObj->TravId == pObj->pMan->nTravIds - 1; }
+static inline int         Nwk_ManTimeEqual( float f1, float f2, float Eps )  { return (f1 < f2 + Eps) && (f2 < f1 + Eps);  }
+static inline int         Nwk_ManTimeLess( float f1, float f2, float Eps )   { return (f1 < f2 + Eps);                     }
+static inline int         Nwk_ManTimeMore( float f1, float f2, float Eps )   { return (f1 + Eps > f2);                     }
 ////////////////////////////////////////////////////////////////////////
 ///                         ITERATORS                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -191,8 +196,10 @@ static inline int         Nwk_ObjIsTravIdPrevious( Nwk_Obj_t * pObj )        { r
 extern void            Nwk_ManBidecResyn( Nwk_Man_t * pNtk, int fVerbose );
 extern Hop_Obj_t *     Nwk_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare );
 /*=== nwkDfs.c ==========================================================*/
+extern int             Nwk_ManVerifyTopoOrder( Nwk_Man_t * pNtk );
+extern int             Nwk_ManLevelBackup( Nwk_Man_t * pNtk );
 extern int             Nwk_ManLevel( Nwk_Man_t * pNtk );
-extern int             Nwk_ManLevel2( Nwk_Man_t * pNtk );
+extern int             Nwk_ManLevelMax( Nwk_Man_t * pNtk );
 extern Vec_Vec_t *     Nwk_ManLevelize( Nwk_Man_t * pNtk );
 extern Vec_Ptr_t *     Nwk_ManDfs( Nwk_Man_t * pNtk );
 extern Vec_Ptr_t *     Nwk_ManDfsNodes( Nwk_Man_t * pNtk, Nwk_Obj_t ** ppNodes, int nNodes );
@@ -203,9 +210,12 @@ extern int             Nwk_ObjMffcLabel( Nwk_Obj_t * pNode );
 /*=== nwkFanio.c ==========================================================*/
 extern void            Nwk_ObjCollectFanins( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes );
 extern void            Nwk_ObjCollectFanouts( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes );
+extern int             Nwk_ObjFindFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
+extern int             Nwk_ObjFindFanout( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanout );
 extern void            Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
 extern void            Nwk_ObjDeleteFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
 extern void            Nwk_ObjPatchFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFaninOld, Nwk_Obj_t * pFaninNew );
+extern void            Nwk_ObjTransferFanout( Nwk_Obj_t * pNodeFrom, Nwk_Obj_t * pNodeTo );
 extern void            Nwk_ObjReplace( Nwk_Obj_t * pNodeOld, Nwk_Obj_t * pNodeNew );
 /*=== nwkMan.c ============================================================*/
 extern Nwk_Man_t *     Nwk_ManAlloc();
@@ -222,10 +232,11 @@ extern Nwk_Obj_t *     Nwk_ManCreateLatch( Nwk_Man_t * pMan );
 extern void            Nwk_ManDeleteNode( Nwk_Obj_t * pObj );
 extern void            Nwk_ManDeleteNode_rec( Nwk_Obj_t * pObj );
 /*=== nwkTiming.c ============================================================*/
-extern float           Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib );
+extern int             Nwk_ManVerifyTiming(  Nwk_Man_t * pNtk );
-extern void            Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk, If_Lib_t * pLutLib );
+extern float           Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk );
+extern void            Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk );
 extern void            Nwk_ManUpdate( Nwk_Obj_t * pObj, Nwk_Obj_t * pObjNew, Vec_Vec_t * vLevels );
-extern void            Nwk_ManVerifyLevel( Nwk_Man_t * pNtk );
+extern int             Nwk_ManVerifyLevel( Nwk_Man_t * pNtk );
 /*=== nwkUtil.c ============================================================*/
 extern void            Nwk_ManIncrementTravId( Nwk_Man_t * pNtk );
 extern int             Nwk_ManGetFaninMax( Nwk_Man_t * pNtk );
@@ -235,6 +246,7 @@ extern int             Nwk_ManPoNum( Nwk_Man_t * pNtk );
 extern int             Nwk_ManGetAigNodeNum( Nwk_Man_t * pNtk );
 extern int             Nwk_NodeCompareLevelsIncrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 );
 extern int             Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 );
+extern void            Nwk_ObjPrint( Nwk_Obj_t * pObj );
 #ifdef __cplusplus
 }

--- a/src/aig/nwk/nwkDfs.c
+++ b/src/aig/nwk/nwkDfs.c
@@ -30,6 +30,63 @@
 /**Function*************************************************************
+  Synopsis    [Verifies that the objects are in a topo order.]
+  Description []
+  SideEffects []
+  SeeAlso     []
+***********************************************************************/
+int Nwk_ManVerifyTopoOrder( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pObj, * pNext;
+    int i, k, iBox, iTerm1, nTerms;
+    Nwk_ManIncrementTravId( pNtk );
+    Nwk_ManForEachObj( pNtk, pObj, i )
+    {
+        if ( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCo(pObj) )
+        {
+            Nwk_ObjForEachFanin( pObj, pNext, k )
+            {
+                if ( !Nwk_ObjIsTravIdCurrent(pNext) )
+                {
+                    printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id );
+                    return 0;
+                }
+            }
+        }
+        else if ( Nwk_ObjIsCi(pObj) )
+        {
+            if ( pNtk->pManTime )
+            {
+                iBox = Tim_ManBoxForCi( pNtk->pManTime, pObj->PioId );
+                if ( iBox >= 0 ) // this is not a true PI
+                {
+                    iTerm1 = Tim_ManBoxInputFirst( pNtk->pManTime, iBox );
+                    nTerms = Tim_ManBoxInputNum( pNtk->pManTime, iBox );
+                    for ( i = 0; i < nTerms; i++ )
+                    {
+                        pNext = Nwk_ManCo( pNtk, iTerm1 + i );
+                        if ( !Nwk_ObjIsTravIdCurrent(pNext) )
+                        {
+                            printf( "Box %d has input %d that is not in a topological order.\n", iBox, pNext->Id );
+                            return 0;
+                        }
+                    }
+                }
+            }
+        }
+        else
+            assert( 0 );
+        Nwk_ObjSetTravIdCurrent( pObj );
+    }
+    return 1;
+}
+/**Function*************************************************************
  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
  Description [Assumes that white boxes have unit level.]
@@ -39,11 +96,12 @@
  SeeAlso     []
 ***********************************************************************/
-int Nwk_ManLevel( Nwk_Man_t * pNtk )
+int Nwk_ManLevelBackup( Nwk_Man_t * pNtk )
 {
    Tim_Man_t * pManTimeUnit;
    Nwk_Obj_t * pObj, * pFanin;
    int i, k, LevelMax, Level;
+    assert( Nwk_ManVerifyTopoOrder(pNtk) );
    // clean the levels
    Nwk_ManForEachObj( pNtk, pObj, i )
        Nwk_ObjSetLevel( pObj, 0 );
@@ -85,11 +143,9 @@ int Nwk_ManLevel( Nwk_Man_t * pNtk )
    return LevelMax;
 }
 /**Function*************************************************************
-  Synopsis    [Performs DFS for one node.]
+  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
  Description []
@@ -98,8 +154,9 @@ int Nwk_ManLevel( Nwk_Man_t * pNtk )
  SeeAlso     []
 ***********************************************************************/
-void Nwk_ManLevel2_rec( Nwk_Obj_t * pObj )
+void Nwk_ManLevel_rec( Nwk_Obj_t * pObj )
 {
+    Tim_Man_t * pManTime = pObj->pMan->pManTime;
    Nwk_Obj_t * pNext;
    int i, iBox, iTerm1, nTerms, LevelMax = 0;
    if ( Nwk_ObjIsTravIdCurrent( pObj ) )
@@ -107,30 +164,33 @@ void Nwk_ManLevel2_rec( Nwk_Obj_t * pObj )
    Nwk_ObjSetTravIdCurrent( pObj );
    if ( Nwk_ObjIsCi(pObj) )
    {
-        iBox = Tim_ManBoxForCi( pObj->pMan->pManTime, pObj->PioId );
+        if ( pManTime ) 
+        {
+            iBox = Tim_ManBoxForCi( pManTime, pObj->PioId );
            if ( iBox >= 0 ) // this is not a true PI
            {
-            iTerm1 = Tim_ManBoxInputFirst( pObj->pMan->pManTime, iBox );
+                iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
-            nTerms = Tim_ManBoxInputNum( pObj->pMan->pManTime, iBox );
+                nTerms = Tim_ManBoxInputNum( pManTime, iBox );
                for ( i = 0; i < nTerms; i++ )
                {
                    pNext = Nwk_ManCo(pObj->pMan, iTerm1 + i);
-                Nwk_ManLevel2_rec( pNext );
+                    Nwk_ManLevel_rec( pNext );
                    if ( LevelMax < Nwk_ObjLevel(pNext) )
                        LevelMax = Nwk_ObjLevel(pNext);
                }
                LevelMax++;
            }
        }
+    }
    else if ( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCo(pObj) )
    {
        Nwk_ObjForEachFanin( pObj, pNext, i )
        {
-            Nwk_ManLevel2_rec( pNext );
+            Nwk_ManLevel_rec( pNext );
            if ( LevelMax < Nwk_ObjLevel(pNext) )
                LevelMax = Nwk_ObjLevel(pNext);
        }
-        if ( Nwk_ObjIsNode(pObj) )
+        if ( Nwk_ObjIsNode(pObj) && Nwk_ObjFaninNum(pObj) > 0 )
            LevelMax++;
    }
    else
@@ -140,16 +200,16 @@ void Nwk_ManLevel2_rec( Nwk_Obj_t * pObj )
 /**Function*************************************************************
-  Synopsis    [Returns the DFS ordered array of all objects except latches.]
+  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
-  Description []
+  Description [Does not assume that the objects are in a topo order.]
  SideEffects []
  SeeAlso     []
 ***********************************************************************/
-int Nwk_ManLevel2( Nwk_Man_t * pNtk )
+int Nwk_ManLevel( Nwk_Man_t * pNtk )
 {
    Nwk_Obj_t * pObj;
    int i, LevelMax = 0;
@@ -158,7 +218,7 @@ int Nwk_ManLevel2( Nwk_Man_t * pNtk )
    Nwk_ManIncrementTravId( pNtk );
    Nwk_ManForEachPo( pNtk, pObj, i )
    {
-        Nwk_ManLevel2_rec( pObj );
+        Nwk_ManLevel_rec( pObj );
        if ( LevelMax < Nwk_ObjLevel(pObj) )
            LevelMax = Nwk_ObjLevel(pObj);
    }
@@ -169,6 +229,27 @@ int Nwk_ManLevel2( Nwk_Man_t * pNtk )
  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
+  Description [Does not assume that the objects are in a topo order.]
+  SideEffects []
+  SeeAlso     []
+***********************************************************************/
+int Nwk_ManLevelMax( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pObj;
+    int i, LevelMax = 0;
+    Nwk_ManForEachPo( pNtk, pObj, i )
+        if ( LevelMax < Nwk_ObjLevel(pObj) )
+            LevelMax = Nwk_ObjLevel(pObj);
+    return LevelMax;
+}
+/**Function*************************************************************
+  Synopsis    [Returns the array of objects in the AIG manager ordered by level.]
  Description []
  SideEffects []
@@ -181,7 +262,8 @@ Vec_Vec_t * Nwk_ManLevelize( Nwk_Man_t * pNtk )
    Nwk_Obj_t * pObj;
    Vec_Vec_t * vLevels;
    int nLevels, i;
-    nLevels = Nwk_ManLevel( pNtk );
+    assert( Nwk_ManVerifyLevel(pNtk) );
+    nLevels = Nwk_ManLevelMax( pNtk );
    vLevels = Vec_VecStart( nLevels + 1 );
    Nwk_ManForEachNode( pNtk, pObj, i )
    {

--- a/src/aig/nwk/nwkMan.c
+++ b/src/aig/nwk/nwkMan.c
@@ -93,6 +93,7 @@ void Nwk_ManFree( Nwk_Man_t * p )
 ***********************************************************************/
 void Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib )
 {
+    p->pLutLib = pLutLib;
    printf( "%-15s : ",      p->pName );
    printf( "pi = %5d  ",    Nwk_ManPiNum(p) );
    printf( "po = %5d  ",    Nwk_ManPoNum(p) );
@@ -102,8 +103,8 @@ void Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib )
    printf( "node = %5d  ",  Nwk_ManNodeNum(p) );
    printf( "aig = %6d  ",   Nwk_ManGetAigNodeNum(p) );
    printf( "lev = %3d  ",   Nwk_ManLevel(p) );
-//    printf( "lev2 = %3d  ",  Nwk_ManLevel2(p) );
+//    printf( "lev2 = %3d  ",  Nwk_ManLevelBackup(p) );
-    printf( "delay = %5.2f", Nwk_ManDelayTraceLut(p, pLutLib) );
+    printf( "delay = %5.2f", Nwk_ManDelayTraceLut(p) );
    printf( "\n" );
 //    Nwk_ManDelayTracePrint( p, pLutLib );
    fflush( stdout );

--- a/src/aig/nwk/nwkMap.c
+++ b/src/aig/nwk/nwkMap.c
@@ -96,50 +96,45 @@ void Nwk_ManSetIfParsDefault( If_Par_t * pPars )
  SeeAlso     []
 ***********************************************************************/
-If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
+If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
 {
    If_Man_t * pIfMan;
-    Aig_Obj_t * pNode;//, * pFanin, * pPrev;
+    If_Obj_t * pIfObj;
+    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, 
+            pIfObj = If_ManCreateAnd( pIfMan, 
-                If_NotCond( (If_Obj_t *)Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ), 
+                If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ), 
-                If_NotCond( (If_Obj_t *)Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) );
+                If_NotCond( Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) );
        else if ( Aig_ObjIsPi(pNode) )
        {
-            pNode->pData = If_ManCreateCi( pIfMan );
+            pIfObj = If_ManCreateCi( pIfMan );
-            ((If_Obj_t *)pNode->pData)->Level = pNode->Level;
+            If_ObjSetLevel( pIfObj, Aig_ObjLevel(pNode) );
-            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) ) );
+            pIfObj = If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
        else if ( Aig_ObjIsConst1(pNode) )
-            Aig_ManConst1(p)->pData = If_ManConst1( pIfMan );
+            pIfObj = If_ManConst1( pIfMan );
        else // add the node to the mapper
            assert( 0 );
+        // save the result
+        assert( Vec_PtrEntry(vAigToIf, i) == NULL );
+        Vec_PtrWriteEntry( vAigToIf, i, pIfObj );
+        pNode->pData = pIfObj;
        // set up the choice node
-//        if ( Aig_AigNodeIsChoice( pNode ) )
+        if ( Aig_ObjIsChoice( p, 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;
+            pIfMan->nChoices++;
-            assert( !If_IsComplement(pIfObj) );
+            for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
-            assert( pIfObj->Id == pNode->Id );
+                If_ObjSetChoice( pPrev->pData, pFanin->pData );
+            If_ManCreateChoice( pIfMan, pNode->pData );
        }
+        assert( If_ObjLevel(pIfObj) == Aig_ObjLevel(pNode) );
    }
    return pIfMan;
 }
@@ -243,7 +238,7 @@ Hop_Obj_t * Nwk_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * 
  SeeAlso     []
 ***********************************************************************/
-Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p )
+Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToIf )
 {
    Nwk_Man_t * pNtk;
    Nwk_Obj_t * pObjNew;
@@ -261,7 +256,7 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p )
    pNtk->pSpec = Aig_UtilStrsav( p->pSpec );
    Aig_ManForEachObj( p, pObj, i )
    {
-        pIfObj = If_ManObj( pIfMan, i );
+        pIfObj = Vec_PtrEntry( vAigToIf, i );
        if ( pIfObj->nRefs == 0 && !If_ObjIsTerm(pIfObj) )
            continue;
        if ( Aig_ObjIsNode(pObj) )
@@ -312,12 +307,13 @@ Nwk_Man_t * Nwk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars
 {
    Nwk_Man_t * pNtk;
    If_Man_t * pIfMan;
-    // perform FPGA mapping
+    Vec_Ptr_t * vAigToIf;
    // 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 = Nwk_ManToIf( p, pPars );    
+    vAigToIf = Vec_PtrStart( Aig_ManObjNumMax(p) );
+    pIfMan = Nwk_ManToIf( p, pPars, vAigToIf );    
    if ( pIfMan == NULL )
        return NULL;
    pIfMan->pManTim = Tim_ManDup( pManTime, 0 );
@@ -327,8 +323,9 @@ Nwk_Man_t * Nwk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars
        return NULL;
    }
    // transform the result of mapping into the new network
-    pNtk = Nwk_ManFromIf( pIfMan, p );
+    pNtk = Nwk_ManFromIf( pIfMan, p, vAigToIf );
    If_ManStop( pIfMan );
+    Vec_PtrFree( vAigToIf );
    return pNtk;
 }

--- a/src/aig/nwk/nwkObj.c
+++ b/src/aig/nwk/nwkObj.c
@@ -194,7 +194,6 @@ void Nwk_ManDeleteNode_rec( Nwk_Obj_t * pObj )
    Vec_PtrFree( vNodes );
 }
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

--- a/src/aig/nwk/nwkStrash.c
+++ b/src/aig/nwk/nwkStrash.c
@@ -95,11 +95,13 @@ Aig_Obj_t * Nwk_ManStrashNode( Aig_Man_t * p, Nwk_Obj_t * pObj )
 ***********************************************************************/
 Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk )
 {
-    Aig_Man_t * pMan;
+    Aig_Man_t * pMan;//, * pTemp;
    Aig_Obj_t * pObjNew;
    Nwk_Obj_t * pObj;
    int i, Level;
    pMan = Aig_ManStart( Nwk_ManGetAigNodeNum(pNtk) );
+    pMan->pName = Aig_UtilStrsav( pNtk->pName );
+    pMan->pSpec = Aig_UtilStrsav( pNtk->pSpec );
    pMan->pManTime = Tim_ManDup( pNtk->pManTime, 1 );
    Tim_ManIncrementTravId( pMan->pManTime );
    Nwk_ManForEachObj( pNtk, pObj, i )
@@ -125,6 +127,8 @@ Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk )
        pObj->pCopy = pObjNew;
    }
    Aig_ManCleanup( pMan );
+//    pMan = Aig_ManDup( pTemp = pMan, 1 );
+//    Aig_ManStop( pTemp );
    return pMan;
 }

--- a/src/aig/nwk/nwkTiming.c
+++ b/src/aig/nwk/nwkTiming.c
--- a/src/aig/nwk/nwkUtil.c
+++ b/src/aig/nwk/nwkUtil.c
@@ -207,6 +207,38 @@ int Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 )
    return 0; 
 }
+/**Function*************************************************************
+  Synopsis    [Deletes the node.]
+  Description []
+  SideEffects []
+  SeeAlso     []
+***********************************************************************/
+void Nwk_ObjPrint( Nwk_Obj_t * pObj )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    printf( "ObjId = %5d.  ", pObj->Id );
+    if ( Nwk_ObjIsPi(pObj) )
+        printf( "PI" );
+    if ( Nwk_ObjIsPo(pObj) )
+        printf( "PO" );
+    if ( Nwk_ObjIsNode(pObj) )
+        printf( "Node" );
+    printf( "   Fanins = " );
+    Nwk_ObjForEachFanin( pObj, pNext, i )
+        printf( "%d ", pNext->Id );
+    printf( "   Fanouts = " );
+    Nwk_ObjForEachFanout( pObj, pNext, i )
+        printf( "%d ", pNext->Id );
+    printf( "\n" );
+}
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

--- a/src/aig/tim/tim.c
+++ b/src/aig/tim/tim.c
@@ -78,6 +78,7 @@ struct Tim_Obj_t_
 static inline Tim_Obj_t * Tim_ManPi( Tim_Man_t * p, int i )                           { assert( i < p->nPis ); return p->pPis + i;    }
 static inline Tim_Obj_t * Tim_ManPo( Tim_Man_t * p, int i )                           { assert( i < p->nPos ); return p->pPos + i;    }
+static inline Tim_Box_t * Tim_ManBox( Tim_Man_t * p, int i )                          { return Vec_PtrEntry(p->vBoxes, i);            }
 static inline Tim_Box_t * Tim_ManPiBox( Tim_Man_t * p, int i )                        { return Tim_ManPi(p,i)->iObj2Box < 0 ? NULL : Vec_PtrEntry( p->vBoxes, Tim_ManPi(p,i)->iObj2Box ); }
 static inline Tim_Box_t * Tim_ManPoBox( Tim_Man_t * p, int i )                        { return Tim_ManPo(p,i)->iObj2Box < 0 ? NULL : Vec_PtrEntry( p->vBoxes, Tim_ManPo(p,i)->iObj2Box ); }
@@ -363,6 +364,48 @@ void Tim_ManTravIdEnable( Tim_Man_t * p )
 /**Function*************************************************************
+  Synopsis    [Label box inputs.]
+  Description []
+  SideEffects []
+  SeeAlso     []
+***********************************************************************/
+void Tim_ManSetCurrentTravIdBoxInputs( Tim_Man_t * p, int iBox )
+{
+    Tim_Box_t * pBox;
+    Tim_Obj_t * pObj;
+    int i;
+    pBox = Tim_ManBox( p, iBox );
+    Tim_ManBoxForEachInput( p, pBox, pObj, i )
+        pObj->TravId = p->nTravIds;
+}
+/**Function*************************************************************
+  Synopsis    [Label box outputs.]
+  Description []
+  SideEffects []
+  SeeAlso     []
+***********************************************************************/
+void Tim_ManSetCurrentTravIdBoxOutputs( Tim_Man_t * p, int iBox )
+{
+    Tim_Box_t * pBox;
+    Tim_Obj_t * pObj;
+    int i;
+    pBox = Tim_ManBox( p, iBox );
+    Tim_ManBoxForEachOutput( p, pBox, pObj, i )
+        pObj->TravId = p->nTravIds;
+}
+/**Function*************************************************************
  Synopsis    [Sets the vector of timing tables associated with the manager.]
  Description []
@@ -469,6 +512,16 @@ void Tim_ManCreateBoxFirst( Tim_Man_t * p, int firstIn, int nIns, int firstOut, 
 ***********************************************************************/
 void Tim_ManIncrementTravId( Tim_Man_t * p )
 {
+    int i;
+    if ( p->nTravIds >= (1<<30)-1 )
+    {
+        p->nTravIds = 0;
+        for ( i = 0; i < p->nPis; i++ )
+            p->pPis[i].TravId = 0;
+        for ( i = 0; i < p->nPos; i++ )
+            p->pPos[i].TravId = 0;
+    }
+    assert( p->nTravIds < (1<<30)-1 );
    p->nTravIds++;
 }

--- a/src/aig/tim/tim.h
+++ b/src/aig/tim/tim.h
@@ -65,6 +65,8 @@ extern void            Tim_ManStop( Tim_Man_t * p );
 extern void            Tim_ManPrint( Tim_Man_t * p );
 extern void            Tim_ManTravIdDisable( Tim_Man_t * p );
 extern void            Tim_ManTravIdEnable( Tim_Man_t * p );
+extern void            Tim_ManSetCurrentTravIdBoxInputs( Tim_Man_t * p, int iBox );
+extern void            Tim_ManSetCurrentTravIdBoxOutputs( Tim_Man_t * p, int iBox );
 extern void            Tim_ManSetDelayTables( Tim_Man_t * p, Vec_Ptr_t * vDelayTables );
 extern void            Tim_ManCreateBox( Tim_Man_t * p, int * pIns, int nIns, int * pOuts, int nOuts, float * pDelayTable );
 extern void            Tim_ManCreateBoxFirst( Tim_Man_t * p, int firstIn, int nIns, int firstOut, int nOuts, float * pDelayTable );

--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -154,10 +154,7 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
    if ( Abc_NtkIsNetlist(pNtk) )
    {
        if ( Abc_NtkNetNum(pNtk) == 0 )
-        {
+            fprintf( stdout, "NetworkCheck: Warning! Netlist has no nets.\n" );
-            fprintf( stdout, "NetworkCheck: Netlist has no nets.\n" );
-            return 0;
-        }
        // check the nets
        Abc_NtkForEachNet( pNtk, pNet, i )
            if ( !Abc_NtkCheckNet( pNtk, pNet ) )

--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -953,8 +953,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
    Abc_NtkForEachObj( pNtk, pObj, i )
    {
        // free large fanout arrays
-        if ( pNtk->pMmObj && pObj->vFanouts.nCap * 4 > LargePiece )
+//        if ( pNtk->pMmObj && pObj->vFanouts.nCap * 4 > LargePiece )
-            FREE( pObj->vFanouts.pArray );
+//            FREE( pObj->vFanouts.pArray );
        // these flags should be always zero
        // if this is not true, something is wrong somewhere
        assert( pObj->fMarkA == 0 );

--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -1781,8 +1781,8 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
        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) );
+//        Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) );
-        printf( "\n" );
+//        printf( "\n" );
        if ( fCofactor )
            Kit_DsdPrintCofactors( pTruth, Abc_ObjFaninNum(pObj), nCofLevel, 1 );
        else
@@ -7108,7 +7108,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern void Abc_NtkDarTestBlif( char * pFileName );
 //    extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk );
 //    extern Abc_Ntk_t * Abc_NtkTestExor( Abc_Ntk_t * pNtk, int fVerbose );
-    extern Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk );
+    extern Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib );
@@ -7295,7 +7295,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Abc_NtkDarPartition( pNtk );
-    pNtkRes = Abc_NtkNtkTest( pNtk );
+    pNtkRes = Abc_NtkNtkTest( pNtk, Abc_FrameReadLibLut() );
    if ( pNtkRes == NULL )
    {
        fprintf( pErr, "Command has failed.\n" );
@@ -15343,7 +15343,7 @@ int Abc_CommandAbc8Mfs( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
    Mfx_Par_t Pars, * pPars = &Pars;
    int c;
-    extern int Mfx_Perform( void * pNtk, Mfx_Par_t * pPars );
+    extern int Mfx_Perform( void * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib );
    // set defaults
    Mfx_ParsDefault( pPars );
@@ -15449,7 +15449,7 @@ int Abc_CommandAbc8Mfs( Abc_Frame_t * pAbc, int argc, char ** argv )
    }
    // modify the current network
-    if ( !Mfx_Perform( pAbc->pAbc8Nwk, pPars ) )
+    if ( !Mfx_Perform( pAbc->pAbc8Nwk, pPars, pAbc->pAbc8Lib ) )
    {
        fprintf( stdout, "Abc_CommandAbc8Mfs(): Command has failed.\n" );
        return 1;

--- a/src/base/abci/abcAbc8.c
+++ b/src/base/abci/abcAbc8.c
@@ -198,8 +198,9 @@ clk = clock();
 PRT( "Time", clock() - clk );
    pMan = Abc_NtkToNtkNew( pNtk );
+    pMan->pLutLib = Abc_FrameReadLibLut();
 clk = clock();
-    printf( "%6.2f\n", Nwk_ManDelayTraceLut( pMan, Abc_FrameReadLibLut() ) );
+    printf( "%6.2f\n", Nwk_ManDelayTraceLut( pMan ) );
 PRT( "Time", clock() - clk );
    pNtkNew = Abc_NtkFromNtkNew( pNtk, pMan );
@@ -218,9 +219,9 @@ PRT( "Time", clock() - clk );
  SeeAlso     []
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk ) 
+Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib ) 
 {
-    extern int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars );
+    extern int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib );
    Mfx_Par_t Pars, * pPars = &Pars;
    Abc_Ntk_t * pNtkNew;
@@ -228,7 +229,7 @@ Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk )
    pMan = Abc_NtkToNtkNew( pNtk );
    Mfx_ParsDefault( pPars );
-    Mfx_Perform( pMan, pPars );
+    Mfx_Perform( pMan, pPars, pLutLib );
    pNtkNew = Abc_NtkFromNtkNew( pNtk, pMan );
    Nwk_ManFree( pMan );

--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -255,6 +255,8 @@ static inline If_Obj_t * If_ObjFanin1( If_Obj_t * pObj )                     { r
 static inline int        If_ObjFaninC0( If_Obj_t * pObj )                    { return pObj->fCompl0;                 }
 static inline int        If_ObjFaninC1( If_Obj_t * pObj )                    { return pObj->fCompl1;                 }
 static inline void *     If_ObjCopy( If_Obj_t * pObj )                       { return pObj->pCopy;                   }
+static inline int        If_ObjLevel( If_Obj_t * pObj )                      { return pObj->Level;                   }
+static inline void       If_ObjSetLevel( If_Obj_t * pObj, int Level )        { pObj->Level = Level;                  }
 static inline void       If_ObjSetCopy( If_Obj_t * pObj, void * pCopy )      { pObj->pCopy = pCopy;                  }
 static inline void       If_ObjSetChoice( If_Obj_t * pObj, If_Obj_t * pEqu ) { pObj->pEquiv = pEqu;                  }

--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -191,6 +191,8 @@ If_Obj_t * If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver )
    pObj->fCompl0 = If_IsComplement(pDriver); pDriver = If_Regular(pDriver);
    pObj->pFanin0 = pDriver; pDriver->nRefs++; 
    pObj->Level   = pDriver->Level;
+    if ( p->nLevelMax < (int)pObj->Level )
+        p->nLevelMax = (int)pObj->Level;
    p->nObjs[IF_CO]++;
    return pObj;
 }

--- a/src/misc/extra/extraUtilMemory.c
+++ b/src/misc/extra/extraUtilMemory.c
@@ -527,12 +527,12 @@ void Extra_MmStepStop( Extra_MmStep_t * p )
    int i;
    for ( i = 0; i < p->nMems; i++ )
        Extra_MmFixedStop( p->pMems[i] );
-//    if ( p->pLargeChunks ) 
+    if ( p->pLargeChunks ) 
-//    {
+    {
-//      for ( i = 0; i < p->nLargeChunks; i++ )
+      for ( i = 0; i < p->nLargeChunks; i++ )
-//          free( p->pLargeChunks[i] );
+          free( p->pLargeChunks[i] );
-//      free( p->pLargeChunks );
+      free( p->pLargeChunks );
-//    }
+    }
    free( p->pMems );
    free( p->pMap );
    free( p );
@@ -556,18 +556,16 @@ char * Extra_MmStepEntryFetch( Extra_MmStep_t * p, int nBytes )
    if ( nBytes > p->nMapSize )
    {
 //        printf( "Allocating %d bytes.\n", nBytes );
-/*
+//        return ALLOC( char, nBytes );
        if ( p->nLargeChunks == p->nLargeChunksAlloc )
        {
            if ( p->nLargeChunksAlloc == 0 )
-                p->nLargeChunksAlloc = 5;
+                p->nLargeChunksAlloc = 32;
            p->nLargeChunksAlloc *= 2;
            p->pLargeChunks = REALLOC( char *, p->pLargeChunks, p->nLargeChunksAlloc ); 
        }
        p->pLargeChunks[ p->nLargeChunks++ ] = ALLOC( char, nBytes );
        return p->pLargeChunks[ p->nLargeChunks - 1 ];
-*/
-        return ALLOC( char, nBytes );
    }
    return Extra_MmFixedEntryFetch( p->pMap[nBytes] );
 }
@@ -590,7 +588,7 @@ void Extra_MmStepEntryRecycle( Extra_MmStep_t * p, char * pEntry, int nBytes )
        return;
    if ( nBytes > p->nMapSize )
    {
-        free( pEntry );
+//        free( pEntry );
        return;
    }
    Extra_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );

--- a/src/sat/bsat/satMem.c
+++ b/src/sat/bsat/satMem.c
@@ -67,6 +67,10 @@ struct Sat_MmStep_t_
    Sat_MmFixed_t **  pMems;     // memory managers: 2^1 words, 2^2 words, etc
    int               nMapSize;  // the size of the memory array
    Sat_MmFixed_t **  pMap;      // maps the number of bytes into its memory manager
+    // additional memory chunks
+    int           nChunksAlloc;  // the maximum number of memory chunks 
+    int           nChunks;       // the current number of memory chunks 
+    char **       pChunks;       // the allocated memory
 };
 ////////////////////////////////////////////////////////////////////////
@@ -291,7 +295,7 @@ Sat_MmFlex_t * Sat_MmFlexStart()
    p->pCurrent      = NULL;
    p->pEnd          = NULL;
-    p->nChunkSize    = (1 << 12);
+    p->nChunkSize    = (1 << 16);
    p->nChunksAlloc  = 64;
    p->nChunks       = 0;
    p->pChunks       = ALLOC( char *, p->nChunksAlloc );
@@ -436,6 +440,9 @@ Sat_MmStep_t * Sat_MmStepStart( int nSteps )
            p->pMap[k] = p->pMems[i];
 //for ( i = 1; i < 100; i ++ )
 //printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize );
+    p->nChunksAlloc  = 64;
+    p->nChunks       = 0;
+    p->pChunks       = ALLOC( char *, p->nChunksAlloc );
    return p;
 }
@@ -453,6 +460,12 @@ Sat_MmStep_t * Sat_MmStepStart( int nSteps )
 void Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose )
 {
    int i;
+    if ( p->nChunksAlloc )
+    {
+        for ( i = 0; i < p->nChunks; i++ )
+            free( p->pChunks[i] );
+        free( p->pChunks );
+    }
    for ( i = 0; i < p->nMems; i++ )
        Sat_MmFixedStop( p->pMems[i], fVerbose );
    free( p->pMems );
@@ -477,8 +490,13 @@ char * Sat_MmStepEntryFetch( Sat_MmStep_t * p, int nBytes )
        return NULL;
    if ( nBytes > p->nMapSize )
    {
-//        printf( "Allocating %d bytes.\n", nBytes );
+        if ( p->nChunks == p->nChunksAlloc )
-        return ALLOC( char, nBytes );
+        {
+            p->nChunksAlloc *= 2;
+            p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
+        }
+        p->pChunks[ p->nChunks++ ] = ALLOC( char, nBytes );
+        return p->pChunks[p->nChunks-1];
    }
    return Sat_MmFixedEntryFetch( p->pMap[nBytes] );
 }
@@ -501,7 +519,7 @@ void Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes )
        return;
    if ( nBytes > p->nMapSize )
    {
-        free( pEntry );
+//        free( pEntry );
        return;
    }
    Sat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );