Version abc70714

26 files changed, 1274 insertions, 234 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 4d9f9819..6725f4a6 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -89,6 +89,7 @@ struct Aig_Man_t_
     Vec_Ptr_t *      vPis;           // the array of PIs
     Vec_Ptr_t *      vPos;           // the array of POs
     Vec_Ptr_t *      vObjs;          // the array of all nodes (optional)
+    Vec_Ptr_t *      vBufs;          // the array of buffers
     Aig_Obj_t *      pConst1;        // the constant 1 node
     Aig_Obj_t        Ghost;          // the ghost node
     // AIG node counters
@@ -98,9 +99,16 @@ struct Aig_Man_t_
     // structural hash table
     Aig_Obj_t **     pTable;         // structural hash table
     int              nTableSize;     // structural hash table size
+    // representation of fanouts
+    int *            pFanData;       // the database to store fanout information
+    int              nFansAlloc;     // the size of fanout representation
+    Vec_Vec_t *      vLevels;        // used to update timing information
+    int              nBufReplaces;   // the number of times replacement led to a buffer
+    int              nBufFixes;      // the number of times buffers were propagated
+    int              nBufMax;        // the maximum number of buffers during computation
     // various data members
     Aig_MmFixed_t *  pMemObjs;       // memory manager for objects
-    Vec_Int_t *      vRequired;      // the required times
+    Vec_Int_t *      vLevelR;        // the reverse level of the nodes
     int              nLevelMax;      // maximum number of levels
     void *           pData;          // the temporary data
     int              nTravIds;       // the current traversal ID
@@ -190,9 +198,10 @@ static inline Aig_Obj_t *  Aig_ObjChild1( Aig_Obj_t * pObj )      { return pObj-
 static inline Aig_Obj_t *  Aig_ObjChild0Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL;  }
 static inline Aig_Obj_t *  Aig_ObjChild1Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL;  }
 static inline int          Aig_ObjLevel( Aig_Obj_t * pObj )       { return pObj->nRefs;                            }
-static inline int          Aig_ObjLevelNew( Aig_Obj_t * pObj )    { return 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level);       }
-static inline int          Aig_ObjFaninPhase( Aig_Obj_t * pObj )  { return Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj); }
-static inline void         Aig_ObjClean( Aig_Obj_t * pObj )       { memset( pObj, 0, sizeof(Aig_Obj_t) ); }
+static inline int          Aig_ObjLevelNew( Aig_Obj_t * pObj )    { return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; }
+static inline int          Aig_ObjFaninPhase( Aig_Obj_t * pObj )  { return pObj? Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) : 0;                              }
+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 int          Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )    
 { 
     if ( Aig_ObjFanin0(pObj) == pFanin ) return 0; 
@@ -263,9 +272,18 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry )
 #define Aig_ManForEachObj( p, pObj, i )                                         \
     Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
 // iterator over all nodes
-#define Aig_ManForEachNode( p, pObj, i )                                         \
+#define Aig_ManForEachNode( p, pObj, i )                                        \
     Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else
 
+// these two procedures are only here for the use inside the iterator
+static inline int     Aig_ObjFanout0Int( Aig_Man_t * p, int ObjId )  { assert(ObjId < p->nFansAlloc);  return p->pFanData[5*ObjId];                         }
+static inline int     Aig_ObjFanoutNext( Aig_Man_t * p, int iFan )   { assert(iFan/2 < p->nFansAlloc); return p->pFanData[5*(iFan >> 1) + 3 + (iFan & 1)];  }
+// iterator over the fanouts
+#define Aig_ObjForEachFanout( p, pObj, pFanout, iFan, i )                       \
+    for ( assert(p->pFanData), i = 0; (i < (int)(pObj)->nRefs) &&               \
+          (((iFan) = i? Aig_ObjFanoutNext(p, iFan) : Aig_ObjFanout0Int(p, pObj->Id)), 1) && \
+          (((pFanout) = Aig_ManObj(p, iFan>>1)), 1); i++ )
+
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -275,16 +293,21 @@ extern int             Aig_ManCheck( Aig_Man_t * p );
 /*=== aigDfs.c ==========================================================*/
 extern Vec_Ptr_t *     Aig_ManDfs( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes );
+extern Vec_Ptr_t *     Aig_ManDfsReverse( Aig_Man_t * p );
 extern int             Aig_ManCountLevels( Aig_Man_t * p );
-extern void            Aig_ManCreateRefs( Aig_Man_t * p );
 extern int             Aig_DagSize( Aig_Obj_t * pObj );
 extern void            Aig_ConeUnmark_rec( Aig_Obj_t * pObj );
 extern Aig_Obj_t *     Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars );
 extern Aig_Obj_t *     Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar );
+/*=== aigFanout.c ==========================================================*/
+extern void            Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
+extern void            Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
+extern void            Aig_ManCreateFanout( Aig_Man_t * p );
+extern void            Aig_ManDeleteFanout( Aig_Man_t * p );
 /*=== aigMan.c ==========================================================*/
 extern Aig_Man_t *     Aig_ManStart();
 extern Aig_Man_t *     Aig_ManStartFrom( Aig_Man_t * p );
-extern Aig_Man_t *     Aig_ManDup( Aig_Man_t * p );
+extern Aig_Man_t *     Aig_ManDup( Aig_Man_t * p, int fOrdered );
 extern void            Aig_ManStop( Aig_Man_t * p );
 extern int             Aig_ManCleanup( Aig_Man_t * p );
 extern void            Aig_ManPrintStats( Aig_Man_t * p );
@@ -300,7 +323,7 @@ extern void            Aig_ObjDisconnect( Aig_Man_t * p, Aig_Obj_t * pObj );
 extern void            Aig_ObjDelete( Aig_Man_t * p, Aig_Obj_t * pObj );
 extern void            Aig_ObjDelete_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int fFreeTop );
 extern void            Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew );
-extern void            Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly );
+extern void            Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly, int fUpdateLevel );
 /*=== aigOper.c =========================================================*/
 extern Aig_Obj_t *     Aig_IthVar( Aig_Man_t * p, int i );
 extern Aig_Obj_t *     Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type );
@@ -322,6 +345,12 @@ extern void            Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj );
 extern void            Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj );
 extern int             Aig_TableCountEntries( Aig_Man_t * p );
 extern void            Aig_TableProfile( Aig_Man_t * p );
+/*=== aigTiming.c ========================================================*/
+extern int             Aig_ObjRequiredLevel( Aig_Man_t * p, Aig_Obj_t * pObj );
+extern void            Aig_ManStartReverseLevels( Aig_Man_t * p, int nMaxLevelIncrease );
+extern void            Aig_ManStopReverseLevels( Aig_Man_t * p );
+extern void            Aig_ManUpdateLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew );
+extern void            Aig_ManUpdateReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew );
 /*=== aigUtil.c =========================================================*/
 extern unsigned        Aig_PrimeCudd( unsigned p );
 extern void            Aig_ManIncrementTravId( Aig_Man_t * p );
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index 0f2d9401..a71afec6 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -119,6 +119,65 @@ Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes )
 
 /**Function*************************************************************
 
+  Synopsis    [Collects internal nodes in the reverse DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManDfsReverse_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+    Aig_Obj_t * pFanout;
+    int iFanout, i;
+    assert( !Aig_IsComplement(pObj) );
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
+    Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
+        Aig_ManDfsReverse_rec( p, pFanout, vNodes );
+    assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    Vec_PtrPush( vNodes, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects internal nodes in the reverse DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vNodes;
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManIncrementTravId( p );
+    // mark POs
+    Aig_ManForEachPo( p, pObj, i )
+        Aig_ObjSetTravIdCurrent( p, pObj );
+    // if there are latches, mark them
+    if ( Aig_ManLatchNum(p) > 0 )
+        Aig_ManForEachObj( p, pObj, i )
+            if ( Aig_ObjIsLatch(pObj) )
+                Aig_ObjSetTravIdCurrent( p, pObj );
+    // go through the nodes
+    vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
+    Aig_ManForEachObj( p, pObj, i )
+        if ( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) )
+            Aig_ManDfsReverse_rec( p, pObj, vNodes );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes the max number of levels in the manager.]
 
   Description []
diff --git a/src/aig/aig/aigFanout.c b/src/aig/aig/aigFanout.c
new file mode 100644
index 00000000..e7d5f216
--- /dev/null
+++ b/src/aig/aig/aigFanout.c
@@ -0,0 +1,189 @@
+/**CFile****************************************************************
+
+  FileName    [aigFanout.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Fanout manipulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigFanout.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+// 0: first iFan
+// 1: prev iFan0
+// 2: prev iFan1
+// 3: next iFan0
+// 4: next iFan1
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int   Aig_FanoutCreate( int FanId, int Num )    { assert( Num < 2 ); return (FanId << 1) | Num;   } 
+static inline int * Aig_FanoutObj( int * pData, int ObjId )   { return pData + 5*ObjId;                         }
+static inline int * Aig_FanoutPrev( int * pData, int iFan )   { return pData + 5*(iFan >> 1) + 1 + (iFan & 1);  }
+static inline int * Aig_FanoutNext( int * pData, int iFan )   { return pData + 5*(iFan >> 1) + 3 + (iFan & 1);  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Adds fanout (pFanout) of node (pObj).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout )
+{
+    int iFan, * pFirst, * pPrevC, * pNextC, * pPrev, * pNext;
+    assert( p->pFanData );
+    assert( !Aig_IsComplement(pObj) && !Aig_IsComplement(pFanout) );
+    assert( pFanout->Id > 0 );
+    if ( pObj->Id >= p->nFansAlloc || pFanout->Id >= p->nFansAlloc )
+    {
+        int nFansAlloc = 2 * AIG_MAX( pObj->Id, pFanout->Id ); 
+        p->pFanData = REALLOC( int, p->pFanData, 5 * nFansAlloc );
+        memset( p->pFanData + 5 * p->nFansAlloc, 0, sizeof(int) * 5 * (nFansAlloc - p->nFansAlloc) );
+        p->nFansAlloc = nFansAlloc;
+    }
+    assert( pObj->Id < p->nFansAlloc && pFanout->Id < p->nFansAlloc );
+    iFan   = Aig_FanoutCreate( pFanout->Id, Aig_ObjWhatFanin(pFanout, pObj) );
+    pPrevC = Aig_FanoutPrev( p->pFanData, iFan );
+    pNextC = Aig_FanoutNext( p->pFanData, iFan );
+    pFirst = Aig_FanoutObj( p->pFanData, pObj->Id );
+    if ( *pFirst == 0 )
+    {
+        *pFirst = iFan;
+        *pPrevC = iFan;
+        *pNextC = iFan;
+    }
+    else
+    {
+        pPrev = Aig_FanoutPrev( p->pFanData, *pFirst );
+        pNext = Aig_FanoutNext( p->pFanData, *pPrev );
+        assert( *pNext == *pFirst );
+        *pPrevC = *pPrev;
+        *pNextC = *pFirst;
+        *pPrev  = iFan;
+        *pNext  = iFan;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes fanout (pFanout) of node (pObj).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout )
+{
+    int iFan, * pFirst, * pPrevC, * pNextC, * pPrev, * pNext;
+    assert( p->pFanData && pObj->Id < p->nFansAlloc && pFanout->Id < p->nFansAlloc );
+    assert( !Aig_IsComplement(pObj) && !Aig_IsComplement(pFanout) );
+    assert( pFanout->Id > 0 );
+    iFan   = Aig_FanoutCreate( pFanout->Id, Aig_ObjWhatFanin(pFanout, pObj) );
+    pPrevC = Aig_FanoutPrev( p->pFanData, iFan );
+    pNextC = Aig_FanoutNext( p->pFanData, iFan );
+    pPrev  = Aig_FanoutPrev( p->pFanData, *pNextC );
+    pNext  = Aig_FanoutNext( p->pFanData, *pPrevC );
+    assert( *pPrev == iFan );
+    assert( *pNext == iFan );
+    pFirst = Aig_FanoutObj( p->pFanData, pObj->Id );
+    assert( *pFirst > 0 );
+    if ( *pFirst == iFan )
+    {
+        if ( *pNextC == iFan )
+        {
+            *pFirst = 0;
+            *pPrev  = 0;
+            *pNext  = 0;
+            *pPrevC = 0;
+            *pNextC = 0;
+            return;
+        }
+        *pFirst = *pNextC;
+    }
+    *pPrev  = *pPrevC;
+    *pNext  = *pNextC;
+    *pPrevC = 0;
+    *pNextC = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create fanout for all objects in the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManCreateFanout( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    // allocate fanout datastructure
+    assert( p->pFanData == NULL );
+    p->nFansAlloc = 2 * Aig_ManObjIdMax(p);
+    if ( p->nFansAlloc < (1<<12) )
+        p->nFansAlloc = (1<<12);
+    p->pFanData = ALLOC( int, 5 * p->nFansAlloc );
+    memset( p->pFanData, 0, sizeof(int) * 5 * p->nFansAlloc );
+    // add fanouts for all objects
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjChild0(pObj) )
+            Aig_ObjAddFanout( p, Aig_ObjFanin0(pObj), pObj );
+        if ( Aig_ObjChild1(pObj) )
+            Aig_ObjAddFanout( p, Aig_ObjFanin1(pObj), pObj );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes fanout for all objects in the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManDeleteFanout( Aig_Man_t * p )
+{
+    assert( p->pFanData != NULL );
+    FREE( p->pFanData );
+    p->nFansAlloc = 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 1b0ea548..562260d3 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -55,6 +55,7 @@ Aig_Man_t * Aig_ManStart( int nNodesMax )
     p->vPis = Vec_PtrAlloc( 100 );
     p->vPos = Vec_PtrAlloc( 100 );
     p->vObjs = Vec_PtrAlloc( 1000 );
+    p->vBufs = Vec_PtrAlloc( 100 );
     // prepare the internal memory manager
     p->pMemObjs = Aig_MmFixedStart( sizeof(Aig_Obj_t), nNodesMax );
     // create the constant node
@@ -96,6 +97,28 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the AIG manager recursively.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    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) );
+    return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates the AIG manager.]
 
   Description []
@@ -105,7 +128,7 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Aig_ManDup( Aig_Man_t * p )
+Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
 {
     Aig_Man_t * pNew;
     Aig_Obj_t * pObj;
@@ -113,15 +136,25 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p )
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
     // create the PIs
+    Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
     Aig_ManForEachPi( p, pObj, i )
         pObj->pData = Aig_ObjCreatePi(pNew);
     // duplicate internal nodes
-    Aig_ManForEachObj( p, pObj, i )
-        if ( Aig_ObjIsBuf(pObj) )
-            pObj->pData = Aig_ObjChild0Copy(pObj);
-        else if ( Aig_ObjIsNode(pObj) )
-            pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    if ( fOrdered )
+    {
+        Aig_ManForEachObj( p, pObj, i )
+            if ( Aig_ObjIsBuf(pObj) )
+                pObj->pData = Aig_ObjChild0Copy(pObj);
+            else if ( Aig_ObjIsNode(pObj) )
+                pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    }
+    else
+    {
+        Aig_ManForEachObj( p, pObj, i )
+            if ( !Aig_ObjIsPo(pObj) )
+                Aig_ManDup_rec( pNew, p, pObj );        
+    }
     // add the POs
     Aig_ManForEachPo( p, pObj, i )
         Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
@@ -149,15 +182,20 @@ void Aig_ManStop( Aig_Man_t * p )
     // print time
     if ( p->time1 ) { PRT( "time1", p->time1 ); }
     if ( p->time2 ) { PRT( "time2", p->time2 ); }
+    // delete fanout
+    if ( p->pFanData ) 
+        Aig_ManDeleteFanout( p );
     // make sure the nodes have clean marks
     Aig_ManForEachObj( p, pObj, i )
         assert( !pObj->fMarkA && !pObj->fMarkB );
 //    Aig_TableProfile( p );
     Aig_MmFixedStop( p->pMemObjs, 0 );
-    if ( p->vPis )        Vec_PtrFree( p->vPis );
-    if ( p->vPos )        Vec_PtrFree( p->vPos );
-    if ( p->vObjs )       Vec_PtrFree( p->vObjs );
-    if ( p->vRequired )   Vec_IntFree( p->vRequired );
+    if ( p->vPis )     Vec_PtrFree( p->vPis );
+    if ( p->vPos )     Vec_PtrFree( p->vPos );
+    if ( p->vObjs )    Vec_PtrFree( p->vObjs );
+    if ( p->vBufs )    Vec_PtrFree( p->vBufs );
+    if ( p->vLevelR )  Vec_IntFree( p->vLevelR );
+    if ( p->vLevels )  Vec_VecFree( p->vLevels );
     free( p->pTable );
     free( p );
 }
@@ -205,14 +243,16 @@ int Aig_ManCleanup( Aig_Man_t * p )
 void Aig_ManPrintStats( Aig_Man_t * p )
 {
     printf( "PI/PO/Lat = %5d/%5d/%5d   ", Aig_ManPiNum(p), Aig_ManPoNum(p), Aig_ManLatchNum(p) );
-    printf( "A = %6d. ",    Aig_ManAndNum(p) );
+    printf( "A = %7d. ",    Aig_ManAndNum(p) );
     if ( Aig_ManExorNum(p) )
         printf( "X = %5d. ",    Aig_ManExorNum(p) );
 //    if ( Aig_ManBufNum(p) )
-        printf( "B = %3d. ",    Aig_ManBufNum(p) );
-    printf( "Cre = %6d. ",  p->nCreated );
-    printf( "Del = %6d. ",  p->nDeleted );
+        printf( "B = %5d. ",    Aig_ManBufNum(p) );
+//    printf( "Cre = %6d. ",  p->nCreated );
+//    printf( "Del = %6d. ",  p->nDeleted );
 //    printf( "Lev = %3d. ",  Aig_ManCountLevels(p) );
+    printf( "Max = %7d. ",  Aig_ManObjIdMax(p) );
+    printf( "Lev = %3d. ",  Aig_ManLevels(p) );
     printf( "\n" );
 }
 
diff --git a/src/aig/aig/aigMem.c b/src/aig/aig/aigMem.c
index 20663e6f..dab90777 100644
--- a/src/aig/aig/aigMem.c
+++ b/src/aig/aig/aigMem.c
@@ -232,7 +232,8 @@ void Aig_MmFixedRestart( Aig_MmFixed_t * p )
 {
     int i;
     char * pTemp;
-
+    if ( p->nChunks == 0 )
+        return;
     // deallocate all chunks except the first one
     for ( i = 1; i < p->nChunks; i++ )
         free( p->pChunks[i] );
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index a261ab40..542b90f9 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -66,9 +66,7 @@ Aig_Obj_t * Aig_ObjCreatePo( Aig_Man_t * p, Aig_Obj_t * pDriver )
     pObj = Aig_ManFetchMemory( p );
     pObj->Type = AIG_OBJ_PO;
     Vec_PtrPush( p->vPos, pObj );
-    // add connections
     Aig_ObjConnect( p, pObj, pDriver, NULL );
-    // update node counters of the manager
     p->nObjs[AIG_OBJ_PO]++;
     return pObj;
 }
@@ -125,23 +123,19 @@ void Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFan0, Aig_Obj
     {
         assert( Aig_ObjFanin0(pObj)->Type > 0 );
         Aig_ObjRef( Aig_ObjFanin0(pObj) );
+        if ( p->pFanData )
+            Aig_ObjAddFanout( p, Aig_ObjFanin0(pObj), pObj );
     }
     if ( pFan1 != NULL )
     {
         assert( Aig_ObjFanin1(pObj)->Type > 0 );
         Aig_ObjRef( Aig_ObjFanin1(pObj) );
+        if ( p->pFanData )
+            Aig_ObjAddFanout( p, Aig_ObjFanin1(pObj), pObj );
     }
     // set level and phase
-    if ( pFan1 != NULL )
-    {
-        pObj->Level = Aig_ObjLevelNew( pObj );
-        pObj->fPhase = Aig_ObjFaninPhase(pFan0) & Aig_ObjFaninPhase(pFan1);
-    }
-    else
-    {
-        pObj->Level = pFan0->Level;
-        pObj->fPhase = Aig_ObjFaninPhase(pFan0);
-    }
+    pObj->Level = Aig_ObjLevelNew( pObj );
+    pObj->fPhase = Aig_ObjFaninPhase(pFan0) & Aig_ObjFaninPhase(pFan1);
     // add the node to the structural hash table
     if ( Aig_ObjIsHash(pObj) )
         Aig_TableInsert( p, pObj );
@@ -163,9 +157,17 @@ void Aig_ObjDisconnect( Aig_Man_t * p, Aig_Obj_t * pObj )
     assert( !Aig_IsComplement(pObj) );
     // remove connections
     if ( pObj->pFanin0 != NULL )
+    {
+        if ( p->pFanData )
+            Aig_ObjRemoveFanout( p, Aig_ObjFanin0(pObj), pObj );
         Aig_ObjDeref(Aig_ObjFanin0(pObj));
+    }
     if ( pObj->pFanin1 != NULL )
+    {
+        if ( p->pFanData )
+            Aig_ObjRemoveFanout( p, Aig_ObjFanin1(pObj), pObj );
         Aig_ObjDeref(Aig_ObjFanin1(pObj));
+    }
     // remove the node from the structural hash table
     if ( Aig_ObjIsHash(pObj) )
         Aig_TableDelete( p, pObj );
@@ -190,6 +192,8 @@ void Aig_ObjDelete( Aig_Man_t * p, Aig_Obj_t * pObj )
     assert( !Aig_IsComplement(pObj) );
     assert( !Aig_ObjIsTerm(pObj) );
     assert( Aig_ObjRefs(pObj) == 0 );
+    if ( p->pFanData && Aig_ObjIsBuf(pObj) )
+        Vec_PtrRemove( p->vBufs, pObj );
     p->nObjs[pObj->Type]--;
     Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
     Aig_ManRecycleMemory( p, pObj );
@@ -241,11 +245,15 @@ void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew
     assert( !Aig_IsComplement(pObj) );
     pFaninOld = Aig_ObjFanin0(pObj);
     // decrement ref and remove fanout
+    if ( p->pFanData )
+        Aig_ObjRemoveFanout( p, pFaninOld, pObj );
     Aig_ObjDeref( pFaninOld );
     // update the fanin
     pObj->pFanin0 = pFaninNew;
     // increment ref and add fanout
-    Aig_ObjRef( Aig_Regular(pFaninNew) );
+    if ( p->pFanData )
+        Aig_ObjAddFanout( p, Aig_ObjFanin0(pObj), pObj );
+    Aig_ObjRef( Aig_ObjFanin0(pObj) );
     // get rid of old fanin
     if ( !Aig_ObjIsPi(pFaninOld) && !Aig_ObjIsConst1(pFaninOld) && Aig_ObjRefs(pFaninOld) == 0 )
         Aig_ObjDelete_rec( p, pFaninOld, 1 );
@@ -253,18 +261,89 @@ void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew
 
 /**Function*************************************************************
 
+  Synopsis    [Replaces node with a buffer fanin by a node without them.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_NodeFixBufferFanins( Aig_Man_t * p, Aig_Obj_t * pObj, int fNodesOnly, int fUpdateLevel )
+{
+    Aig_Obj_t * pFanReal0, * pFanReal1, * pResult;
+    p->nBufFixes++;
+    if ( Aig_ObjIsPo(pObj) )
+    {
+        assert( Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) );
+        pFanReal0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
+        Aig_ObjPatchFanin0( p, pObj, pFanReal0 );
+        return;
+    }
+    assert( Aig_ObjIsNode(pObj) );
+    assert( Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) || Aig_ObjIsBuf(Aig_ObjFanin1(pObj)) );
+    // get the real fanins
+    pFanReal0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
+    pFanReal1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
+    // get the new node
+    if ( Aig_ObjIsNode(pObj) )
+        pResult = Aig_Oper( p, pFanReal0, pFanReal1, Aig_ObjType(pObj) );
+//    else if ( Aig_ObjIsLatch(pObj) )
+//        pResult = Aig_Latch( p, pFanReal0, Aig_ObjInit(pObj) );
+    else 
+        assert( 0 );
+    // replace the node with buffer by the node without buffer
+    Aig_ObjReplace( p, pObj, pResult, fNodesOnly, fUpdateLevel );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of dangling nodes removed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     [] 
+
+***********************************************************************/
+int Aig_ManPropagateBuffers( Aig_Man_t * p, int fNodesOnly, int fUpdateLevel )
+{
+    Aig_Obj_t * pObj;
+    int nSteps;
+    assert( p->pFanData );
+    for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ )
+    {
+        // get the node with a buffer fanin
+        for ( pObj = Vec_PtrEntryLast(p->vBufs); Aig_ObjIsBuf(pObj); pObj = Aig_ObjFanout0(p, pObj) );
+        // replace this node by a node without buffer
+        Aig_NodeFixBufferFanins( p, pObj, fNodesOnly, fUpdateLevel );
+        // stop if a cycle occured
+        if ( nSteps > 1000000 )
+        {
+            printf( "Error: A cycle is encountered while propagating buffers.\n" );
+            break;
+        }
+    }
+    return nSteps;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Replaces one object by another.]
 
-  Description [Both objects are currently in the manager. The new object
-  (pObjNew) should be used instead of the old object (pObjOld). If the 
-  new object is complemented or used, the buffer is added.]
+  Description [The new object (pObjNew) should be used instead of the old 
+  object (pObjOld). If the new object is complemented or used, the buffer 
+  is added and the new object remains in the manager; otherwise, the new
+  object is deleted.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly )
+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);
     // the object to be replaced cannot be complemented
@@ -288,17 +367,34 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
     {
         pObjOld->Type = AIG_OBJ_BUF;
         Aig_ObjConnect( p, pObjOld, pObjNew, NULL );
+        p->nBufReplaces++;
     }
     else
     {
         Aig_Obj_t * pFanin0 = pObjNew->pFanin0;
         Aig_Obj_t * pFanin1 = pObjNew->pFanin1;
+        int LevelOld = pObjOld->Level;
         pObjOld->Type = pObjNew->Type;
         Aig_ObjDisconnect( p, pObjNew );
         Aig_ObjConnect( p, pObjOld, pFanin0, pFanin1 );
+        // delete the new object
         Aig_ObjDelete( p, pObjNew );
+        // update levels
+        if ( fUpdateLevel )
+        {
+            pObjOld->Level = LevelOld;
+            Aig_ManUpdateLevel( p, pObjOld );
+            Aig_ManUpdateReverseLevel( p, pObjOld );
+        }
     }
     p->nObjs[pObjOld->Type]++;
+    // store buffers if fanout is allocated
+    if ( p->pFanData && Aig_ObjIsBuf(pObjOld) )
+    {
+        Vec_PtrPush( p->vBufs, pObjOld );
+        p->nBufMax = AIG_MAX( p->nBufMax, Vec_PtrSize(p->vBufs) );
+        Aig_ManPropagateBuffers( p, fNodesOnly, fUpdateLevel );
+    }
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigSeq.c b/src/aig/aig/aigSeq.c
index 98b7d195..19466996 100644
--- a/src/aig/aig/aigSeq.c
+++ b/src/aig/aig/aigSeq.c
@@ -43,6 +43,7 @@ void Aig_ManSeqStrashConvert( Aig_Man_t * p, int nLatches, int * pInits )
 {
     Aig_Obj_t * pObjLi, * pObjLo, * pLatch;
     int i;
+    assert( Vec_PtrSize( p->vBufs ) == 0 );
     // collect the POs to be converted into latches
     for ( i = 0; i < nLatches; i++ )
     {
@@ -58,6 +59,8 @@ void Aig_ManSeqStrashConvert( Aig_Man_t * p, int nLatches, int * pInits )
         // convert the corresponding PI to be a buffer and connect it to the latch
         pObjLo->Type = AIG_OBJ_BUF;
         Aig_ObjConnect( p, pObjLo, pLatch, NULL );
+        // save the buffer
+//        Vec_PtrPush( p->vBufs, pObjLo );
     }
     // shrink the arrays
     Vec_PtrShrink( p->vPis, Aig_ManPiNum(p) - nLatches );
@@ -353,7 +356,7 @@ int Aig_ManSeqRehashOne( Aig_Man_t * p, Vec_Ptr_t * vNodes, Vec_Ptr_t * vUnreach
                 continue;
             pObjNew = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
             pObjNew = Aig_Latch( p, pObjNew, 0 );
-            Aig_ObjReplace( p, pObj, pObjNew, 1 );
+            Aig_ObjReplace( p, pObj, pObjNew, 1, 0 );
             RetValue = 1;
             Counter++;
             continue;
@@ -365,7 +368,7 @@ int Aig_ManSeqRehashOne( Aig_Man_t * p, Vec_Ptr_t * vNodes, Vec_Ptr_t * vUnreach
             pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
             pFanin1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
             pObjNew = Aig_And( p, pFanin0, pFanin1 );
-            Aig_ObjReplace( p, pObj, pObjNew, 1 );
+            Aig_ObjReplace( p, pObj, pObjNew, 1, 0 );
             RetValue = 1;
             Counter++;
             continue;
@@ -407,7 +410,7 @@ void Aig_ManRemoveBuffers( Aig_Man_t * p )
                 continue;
             pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
             pObjNew = Aig_Latch( p, pFanin0, 0 );
-            Aig_ObjReplace( p, pObj, pObjNew, 0 );
+            Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
         }
         else if ( Aig_ObjIsAnd(pObj) )
         {
@@ -416,7 +419,7 @@ void Aig_ManRemoveBuffers( Aig_Man_t * p )
             pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
             pFanin1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
             pObjNew = Aig_And( p, pFanin0, pFanin1 );
-            Aig_ObjReplace( p, pObj, pObjNew, 0 );
+            Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
         }
     }
     assert( Aig_ManBufNum(p) == 0 );
diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c
index e8cfb480..bba7650a 100644
--- a/src/aig/aig/aigTable.c
+++ b/src/aig/aig/aigTable.c
@@ -28,8 +28,8 @@
 static unsigned long Aig_Hash( Aig_Obj_t * pObj, int TableSize ) 
 {
     unsigned long Key = Aig_ObjIsExor(pObj) * 1699;
-    Key ^= (long)Aig_ObjFanin0(pObj) * 7937;
-    Key ^= (long)Aig_ObjFanin1(pObj) * 2971;
+    Key ^= Aig_ObjFanin0(pObj)->Id * 7937;
+    Key ^= Aig_ObjFanin1(pObj)->Id * 2971;
     Key ^= Aig_ObjFaninC0(pObj) * 911;
     Key ^= Aig_ObjFaninC1(pObj) * 353;
     return Key % TableSize;
@@ -55,15 +55,58 @@ static Aig_Obj_t ** Aig_TableFind( Aig_Man_t * p, Aig_Obj_t * pObj )
     return ppEntry;
 }
 
-static void         Aig_TableResize( Aig_Man_t * p );
-static unsigned int Cudd_PrimeAig( unsigned int  p );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
  
 /**Function*************************************************************
 
+  Synopsis    [Resizes the table.]
+
+  Description [Typically this procedure should not be called.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TableResize( Aig_Man_t * p )
+{
+    Aig_Obj_t * pEntry, * pNext;
+    Aig_Obj_t ** pTableOld, ** ppPlace;
+    int nTableSizeOld, Counter, nEntries, i, clk;
+clk = clock();
+    // save the old table
+    pTableOld = p->pTable;
+    nTableSizeOld = p->nTableSize;
+    // get the new table
+    p->nTableSize = Aig_PrimeCudd( 2 * Aig_ManNodeNum(p) ); 
+    p->pTable = ALLOC( Aig_Obj_t *, p->nTableSize );
+    memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize );
+    // rehash the entries from the old table
+    Counter = 0;
+    for ( i = 0; i < nTableSizeOld; i++ )
+    for ( pEntry = pTableOld[i], pNext = pEntry? pEntry->pNext : NULL; 
+          pEntry; pEntry = pNext, pNext = pEntry? pEntry->pNext : NULL )
+    {
+        // get the place where this entry goes in the table 
+        ppPlace = Aig_TableFind( p, pEntry );
+        assert( *ppPlace == NULL ); // should not be there
+        // add the entry to the list
+        *ppPlace = pEntry;
+        pEntry->pNext = NULL;
+        Counter++;
+    }
+    nEntries = Aig_ManNodeNum(p);
+    assert( Counter == nEntries );
+    printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
+    PRT( "Time", clock() - clk );
+    // replace the table and the parameters
+    free( pTableOld );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Checks if node with the given attributes is in the hash table.]
 
   Description []
@@ -167,51 +210,6 @@ int Aig_TableCountEntries( Aig_Man_t * p )
     return Counter;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Resizes the table.]
-
-  Description [Typically this procedure should not be called.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_TableResize( Aig_Man_t * p )
-{
-    Aig_Obj_t * pEntry, * pNext;
-    Aig_Obj_t ** pTableOld, ** ppPlace;
-    int nTableSizeOld, Counter, nEntries, i, clk;
-clk = clock();
-    // save the old table
-    pTableOld = p->pTable;
-    nTableSizeOld = p->nTableSize;
-    // get the new table
-    p->nTableSize = Cudd_PrimeAig( 2 * Aig_ManNodeNum(p) ); 
-    p->pTable = ALLOC( Aig_Obj_t *, p->nTableSize );
-    memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize );
-    // rehash the entries from the old table
-    Counter = 0;
-    for ( i = 0; i < nTableSizeOld; i++ )
-    for ( pEntry = pTableOld[i], pNext = pEntry? pEntry->pNext : NULL; pEntry; pEntry = pNext, pNext = pEntry? pEntry->pNext : NULL )
-    {
-        // get the place where this entry goes in the table 
-        ppPlace = Aig_TableFind( p, pEntry );
-        assert( *ppPlace == NULL ); // should not be there
-        // add the entry to the list
-        *ppPlace = pEntry;
-        pEntry->pNext = NULL;
-        Counter++;
-    }
-    nEntries = Aig_ManNodeNum(p);
-    assert( Counter == nEntries );
-    printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
-    PRT( "Time", clock() - clk );
-    // replace the table and the parameters
-    free( pTableOld );
-}
-
 /**Function********************************************************************
 
   Synopsis    [Profiles the hash table.]
@@ -237,41 +235,6 @@ void Aig_TableProfile( Aig_Man_t * p )
     }
 }
 
-/**Function********************************************************************
-
-  Synopsis    [Returns the next prime &gt;= p.]
-
-  Description [Copied from CUDD, for stand-aloneness.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-unsigned int Cudd_PrimeAig( unsigned int  p)
-{
-    int i,pn;
-    p--;
-    do {
-        p++;
-        if (p&1) {
-        pn = 1;
-        i = 3;
-        while ((unsigned) (i * i) <= p) {
-        if (p % i == 0) {
-            pn = 0;
-            break;
-        }
-        i += 2;
-        }
-    } else {
-        pn = 0;
-    }
-    } while (!pn);
-    return(p);
-
-} /* end of Cudd_Prime */
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigTiming.c b/src/aig/aig/aigTiming.c
new file mode 100644
index 00000000..dfb4c306
--- /dev/null
+++ b/src/aig/aig/aigTiming.c
@@ -0,0 +1,275 @@
+/**CFile****************************************************************
+
+  FileName    [aigTiming.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Incremental updating of direct/reverse AIG levels.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigTiming.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the reverse level of the node.]
+
+  Description [The reverse level is the level of the node in reverse
+  topological order, starting from the COs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Aig_ObjReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    assert( p->vLevelR );
+    Vec_IntFillExtra( p->vLevelR, pObj->Id + 1, 0 );
+    return Vec_IntEntry(p->vLevelR, pObj->Id);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the reverse level of the node.]
+
+  Description [The reverse level is the level of the node in reverse
+  topological order, starting from the COs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Aig_ObjSetReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObj, int LevelR )
+{
+    assert( p->vLevelR );
+    Vec_IntFillExtra( p->vLevelR, pObj->Id + 1, 0 );
+    Vec_IntWriteEntry( p->vLevelR, pObj->Id, LevelR );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns required level of the node.]
+
+  Description [Converts the reverse levels of the node into its required 
+  level as follows: ReqLevel(Node) = MaxLevels(Ntk) + 1 - LevelR(Node).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ObjRequiredLevel( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    assert( p->vLevelR );
+    return p->nLevelMax + 1 - Aig_ObjReverseLevel(p, pObj);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the reverse level of the node using its fanout levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ObjReverseLevelNew( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pFanout;
+    int i, iFanout, LevelCur, Level = 0;
+    Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
+    {
+        LevelCur = Aig_ObjReverseLevel( p, pFanout );
+        Level = AIG_MAX( Level, LevelCur );
+    }
+    return Level + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares for the computation of required levels.]
+
+  Description [This procedure should be called before the required times
+  are used. It starts internal data structures, which records the level 
+  from the COs of the network nodes in reverse topologogical order.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManStartReverseLevels( Aig_Man_t * p, int nMaxLevelIncrease )
+{
+    Vec_Ptr_t * vNodes;
+    Aig_Obj_t * pObj;
+    int i;
+    assert( p->pFanData != NULL );
+    assert( p->vLevelR == NULL );
+    // remember the maximum number of direct levels
+    p->nLevelMax = Aig_ManLevels(p) + nMaxLevelIncrease;
+    // start the reverse levels
+    p->vLevelR = Vec_IntAlloc( 0 );
+    Vec_IntFill( p->vLevelR, 1 + Aig_ManObjIdMax(p), 0 );
+    // compute levels in reverse topological order
+    vNodes = Aig_ManDfsReverse( p );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        assert( pObj->fMarkA == 0 );
+        Aig_ObjSetReverseLevel( p, pObj, Aig_ObjReverseLevelNew(p, pObj) );
+    }
+    Vec_PtrFree( vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans the data structures used to compute required levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManStopReverseLevels( Aig_Man_t * p )
+{
+    assert( p->vLevelR != NULL );
+    Vec_IntFree( p->vLevelR );
+    p->vLevelR = NULL;
+    p->nLevelMax = 0;
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Incrementally updates level of the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManUpdateLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew )
+{
+    Aig_Obj_t * pFanout, * pTemp;
+    int iFanout, LevelOld, Lev, k, m;
+    assert( p->pFanData != NULL );
+    // allocate level if needed
+    if ( p->vLevels == NULL )
+        p->vLevels = Vec_VecAlloc( Aig_ManLevels(p) + 8 );
+    // check if level has changed
+    LevelOld = Aig_ObjLevel(pObjNew);
+    if ( LevelOld == Aig_ObjLevelNew(pObjNew) )
+        return;
+    // start the data structure for level update
+    // we cannot fail to visit a node when using this structure because the 
+    // nodes are stored by their _old_ levels, which are assumed to be correct
+    Vec_VecClear( p->vLevels );
+    Vec_VecPush( p->vLevels, LevelOld, pObjNew );
+    pObjNew->fMarkA = 1;
+    // recursively update level
+    Vec_VecForEachEntryStart( p->vLevels, pTemp, Lev, k, LevelOld )
+    {
+        pTemp->fMarkA = 0;
+        assert( Aig_ObjLevel(pTemp) == Lev );
+        pTemp->Level = Aig_ObjLevelNew(pTemp);
+        // if the level did not change, no need to check the fanout levels
+        if ( Aig_ObjLevel(pTemp) == Lev )
+            continue;
+        // schedule fanout for level update
+        Aig_ObjForEachFanout( p, pTemp, pFanout, iFanout, m )
+        {
+            if ( !Aig_ObjIsPo(pFanout) && !pFanout->fMarkA )
+            {
+                Vec_VecPush( p->vLevels, Aig_ObjLevel(pFanout), pFanout );
+                pFanout->fMarkA = 1;
+            }
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Incrementally updates level of the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManUpdateReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew )
+{
+    Aig_Obj_t * pFanin, * pTemp;
+    int LevelOld, Lev, k;
+    assert( p->vLevelR != NULL );
+    // allocate level if needed
+    if ( p->vLevels == NULL )
+        p->vLevels = Vec_VecAlloc( Aig_ManLevels(p) + 8 );
+    // check if level has changed
+    LevelOld = Aig_ObjReverseLevel(p, pObjNew);
+    if ( LevelOld == Aig_ObjReverseLevelNew(p, pObjNew) )
+        return;
+    // start the data structure for level update
+    // we cannot fail to visit a node when using this structure because the 
+    // nodes are stored by their _old_ levels, which are assumed to be correct
+    Vec_VecClear( p->vLevels );
+    Vec_VecPush( p->vLevels, LevelOld, pObjNew );
+    pObjNew->fMarkA = 1;
+    // recursively update level
+    Vec_VecForEachEntryStart( p->vLevels, pTemp, Lev, k, LevelOld )
+    {
+        pTemp->fMarkA = 0;
+        LevelOld = Aig_ObjReverseLevel(p, pTemp); 
+        assert( LevelOld == Lev );
+        Aig_ObjSetReverseLevel( p, pTemp, Aig_ObjReverseLevelNew(p, pTemp) );
+        // if the level did not change, to need to check the fanout levels
+        if ( Aig_ObjReverseLevel(p, pTemp) == Lev )
+            continue;
+        // schedule fanins for level update
+        pFanin = Aig_ObjFanin0(pTemp);
+        if ( pFanin && !Aig_ObjIsPi(pFanin) && !pFanin->fMarkA )
+        {
+            Vec_VecPush( p->vLevels, Aig_ObjReverseLevel(p, pFanin), pFanin );
+            pFanin->fMarkA = 1;
+        }
+        pFanin = Aig_ObjFanin1(pTemp);
+        if ( pFanin && !Aig_ObjIsPi(pFanin) && !pFanin->fMarkA )
+        {
+            Vec_VecPush( p->vLevels, Aig_ObjReverseLevel(p, pFanin), pFanin );
+            pFanin->fMarkA = 1;
+        }
+    }
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index f1e83fe6..f9afc4ee 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -1,9 +1,11 @@
 SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigDfs.c \
+    src/aig/aig/aigFanout.c \
     src/aig/aig/aigMan.c \
     src/aig/aig/aigMem.c \
     src/aig/aig/aigObj.c \
     src/aig/aig/aigOper.c \
     src/aig/aig/aigSeq.c \
     src/aig/aig/aigTable.c \
+    src/aig/aig/aigTiming.c \
     src/aig/aig/aigUtil.c 
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index a1502382..969e5253 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -49,7 +49,7 @@ static Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig
 Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
 {
     Aig_Man_t * pNew;
-    Aig_Obj_t * pObj, * pObjNew;
+    Aig_Obj_t * pObj, * pDriver, * pObjNew;
     Vec_Vec_t * vStore;
     int i;
     // create the new manager 
@@ -63,14 +63,15 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
     vStore = Vec_VecAlloc( 50 );
     Aig_ManForEachPo( p, pObj, i )
     {
-        pObjNew = Dar_Balance_rec( pNew, Aig_ObjFanin0(pObj), vStore, 0, fUpdateLevel );
-        Aig_ObjCreatePo( pNew, Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) ) );
+        pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
+        pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
+        pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
+        Aig_ObjCreatePo( pNew, pObjNew );
     }
     Vec_VecFree( vStore );
     // remove dangling nodes
-//    Aig_ManCreateRefs( pNew );
-//    if ( i = Aig_ManCleanup( pNew ) )
-//        printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
+    if ( i = Aig_ManCleanup( pNew ) )
+        printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
     // check the resulting AIG
     if ( !Aig_ManCheck(pNew) )
         printf( "Dar_ManBalance(): The check has failed.\n" );
@@ -94,6 +95,7 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t *
     Vec_Ptr_t * vSuper;
     int i;
     assert( !Aig_IsComplement(pObjOld) );
+    assert( !Aig_ObjIsBuf(pObjOld) );
     // return if the result is known
     if ( pObjOld->pData )
         return pObjOld->pData;
@@ -157,8 +159,8 @@ int Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper
     assert( !Aig_IsComplement(pObj) );
     assert( Aig_ObjIsNode(pObj) );
     // go through the branches
-    RetValue1 = Dar_BalanceCone_rec( pRoot, Aig_ObjChild0(pObj), vSuper );
-    RetValue2 = Dar_BalanceCone_rec( pRoot, Aig_ObjChild1(pObj), vSuper );
+    RetValue1 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper );
+    RetValue2 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper );
     if ( RetValue1 == -1 || RetValue2 == -1 )
         return -1;
     // return 1 if at least one branch has a duplicate
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index a617f5d6..e7186e83 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -43,7 +43,7 @@ void Dar_ManDefaultParams( Dar_Par_t * pPars )
 {
     memset( pPars, 0, sizeof(Dar_Par_t) );
     pPars->nCutsMax     = 8;
-    pPars->nSubgMax     = 4;
+    pPars->nSubgMax     = 5; // 5 is a "magic number"
     pPars->fUpdateLevel = 0;
     pPars->fUseZeros    = 0;
     pPars->fVerbose     = 0;
@@ -69,18 +69,18 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_Par_t * pPars )
     Aig_Obj_t * pObj, * pObjNew;
     int i, k, nNodesOld, nNodeBefore, nNodeAfter, Required;
     int clk = 0, clkStart;
+    // prepare the library
+    Dar_LibPrepare( pPars->nSubgMax ); 
     // create rewriting manager
     p = Dar_ManStart( pAig, pPars );
     // remove dangling nodes
     Aig_ManCleanup( pAig );
+    // if updating levels is requested, start fanout and timing
+    Aig_ManCreateFanout( pAig );
+    if ( p->pPars->fUpdateLevel )
+        Aig_ManStartReverseLevels( pAig, 0 );
     // set elementary cuts for the PIs
-//    Dar_ManSetupPis( p );
-    Aig_ManCleanData( pAig );
-    Dar_ObjPrepareCuts( p, Aig_ManConst1(pAig) );
-    Aig_ManForEachPi( pAig, pObj, i )
-        Dar_ObjPrepareCuts( p, pObj );
-//    if ( p->pPars->fUpdateLevel )
-//        Aig_NtkStartReverseLevels( p );
+    Dar_ManCutsStart( p );
     // resynthesize each node once
     clkStart = clock();
     p->nNodesInit = Aig_ManNodeNum(pAig);
@@ -93,6 +93,10 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_Par_t * pPars )
             continue;
         if ( i > nNodesOld )
             break;
+        // consider freeing the cuts
+//        if ( (i & 0xFFF) == 0 && Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) > 100 )
+//            Dar_ManCutsStart( p );
+
         // compute cuts for the node
 clk = clock();
         Dar_ObjComputeCuts_rec( p, pObj );
@@ -100,7 +104,7 @@ p->timeCuts += clock() - clk;
 
         // check if there is a trivial cut
         Dar_ObjForEachCut( pObj, pCut, k )
-            if ( pCut->nLeaves == 0 || (pCut->nLeaves == 1 && pCut->pLeaves[0] != pObj->Id) )
+            if ( pCut->nLeaves == 0 || (pCut->nLeaves == 1 && pCut->pLeaves[0] != pObj->Id && Aig_ManObj(p->pAig, pCut->pLeaves[0])) )
                 break;
         if ( k < (int)pObj->nCuts )
         {
@@ -115,10 +119,10 @@ p->timeCuts += clock() - clk;
                 assert( pCut->uTruth == 0xAAAA || pCut->uTruth == 0x5555 );
                 pObjNew = Aig_NotCond( Aig_ManObj(p->pAig, pCut->pLeaves[0]), pCut->uTruth==0x5555 );
             }
-            // replace the node
-            Aig_ObjReplace( pAig, pObj, pObjNew, 1 );
             // remove the old cuts
             Dar_ObjSetCuts( pObj, NULL );
+            // replace the node
+            Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
             continue;
         }
 
@@ -128,17 +132,17 @@ p->timeCuts += clock() - clk;
         Dar_ObjForEachCut( pObj, pCut, k )
             Dar_LibEval( p, pObj, pCut, Required );
         // check the best gain
-        if ( !(p->GainBest > 0 || p->GainBest == 0 && p->pPars->fUseZeros) )
+        if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) )
             continue;
+        // remove the old cuts
+        Dar_ObjSetCuts( pObj, NULL );
         // if we end up here, a rewriting step is accepted
         nNodeBefore = Aig_ManNodeNum( pAig );
         pObjNew = Dar_LibBuildBest( p );
         pObjNew = Aig_NotCond( pObjNew, pObjNew->fPhase ^ pObj->fPhase );
         assert( (int)Aig_Regular(pObjNew)->Level <= Required );
         // replace the node
-        Aig_ObjReplace( pAig, pObj, pObjNew, 1 );
-        // remove the old cuts
-        Dar_ObjSetCuts( pObj, NULL );
+        Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
         // compare the gains
         nNodeAfter = Aig_ManNodeNum( pAig );
         assert( p->GainBest <= nNodeBefore - nNodeAfter );
@@ -151,13 +155,14 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
     Extra_ProgressBarStop( pProgress );
     p->nCutMemUsed = Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20);
     Dar_ManCutsFree( p );
-    // stop the rewriting manager
-    Dar_ManStop( p );
     // put the nodes into the DFS order and reassign their IDs
 //    Aig_NtkReassignIds( p );
     // fix the levels
-//    if ( p->pPars->fUpdateLevel )
-//        Aig_NtkStopReverseLevels( p );
+    Aig_ManDeleteFanout( pAig );
+    if ( p->pPars->fUpdateLevel )
+        Aig_ManStopReverseLevels( pAig );
+    // stop the rewriting manager
+    Dar_ManStop( p );
     // check
     if ( !Aig_ManCheck( pAig ) )
     {
@@ -190,9 +195,7 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig )
     // remove dangling nodes
     Aig_ManCleanup( pAig );
     // set elementary cuts for the PIs
-//    Dar_ManSetupPis( p );
-    Aig_ManForEachPi( pAig, pObj, i )
-        Dar_ObjPrepareCuts( p, pObj );
+    Dar_ManCutsStart( p );
     // compute cuts for each nodes in the topological order
     Aig_ManForEachObj( pAig, pObj, i )
     {
diff --git a/src/aig/dar/darCut.c b/src/aig/dar/darCut.c
index af9d1227..08bd77a9 100644
--- a/src/aig/dar/darCut.c
+++ b/src/aig/dar/darCut.c
@@ -62,20 +62,25 @@ static inline int Dar_WordCountOnes( unsigned uWord )
 static inline int Dar_CutFindValue( Dar_Man_t * p, Dar_Cut_t * pCut )
 {
     Aig_Obj_t * pLeaf;
-    int i, Value;
+    int i, Value, nOnes;
     assert( pCut->fUsed );
-    if ( pCut->nLeaves < 2 )
-        return 1001;
     Value = 0;
+    nOnes = 0;
     Dar_CutForEachLeaf( p->pAig, pCut, pLeaf, i )
     {
         if ( pLeaf == NULL )
             return 0;
         assert( pLeaf != NULL );
         Value += pLeaf->nRefs;
+        nOnes += (pLeaf->nRefs == 1);
     }
+    if ( pCut->nLeaves < 2 )
+        return 1001;
+//    Value = Value * 100 / pCut->nLeaves;
     if ( Value > 1000 )
         Value = 1000;
+    if ( nOnes > 3 )
+        Value = 5 - nOnes;
     return Value;
 }
 
@@ -83,7 +88,7 @@ static inline int Dar_CutFindValue( Dar_Man_t * p, Dar_Cut_t * pCut )
 
   Synopsis    [Returns the next free cut to use.]
 
-  Description []
+  Description [Uses the cut with the smallest value.]
                
   SideEffects []
 
@@ -114,6 +119,14 @@ static inline Dar_Cut_t * Dar_CutFindFree( Dar_Man_t * p, Aig_Obj_t * pObj )
                 pCutMax = pCut;
         }
     }
+    if ( pCutMax == NULL )
+    {
+        Dar_ObjForEachCutAll( pObj, pCut, i )
+        {
+            if ( pCutMax == NULL || pCutMax->Value > pCut->Value )
+                pCutMax = pCut;
+        }
+    }
     assert( pCutMax != NULL );
     pCutMax->fUsed = 0;
     return pCutMax;
@@ -466,7 +479,6 @@ static inline int Dar_CutSuppMinimize( Dar_Cut_t * pCut )
     unsigned uPhase = 0, uTruth = 0xFFFF & pCut->uTruth;
     int i, k, nLeaves;
     assert( pCut->fUsed );
-    assert( pCut->nLeaves > 0 );
     // compute the truth support of the cut's function
     nLeaves = pCut->nLeaves;
     for ( i = 0; i < (int)pCut->nLeaves; i++ )
@@ -566,6 +578,28 @@ Dar_Cut_t * Dar_ObjPrepareCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
+void Dar_ManCutsStart( Dar_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManCleanData( p->pAig );
+    Aig_MmFixedRestart( p->pMemCuts );
+    Dar_ObjPrepareCuts( p, Aig_ManConst1(p->pAig) );
+    Aig_ManForEachPi( p->pAig, pObj, i )
+        Dar_ObjPrepareCuts( p, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
 {
     Aig_Obj_t * pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
@@ -612,10 +646,6 @@ Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
         // minimize support of the cut
         if ( Dar_CutSuppMinimize( pCut ) )
         {
-            // if a simple cut is found return immediately
-            if ( pCut->nLeaves < 2 )
-                return pCutSet;
-            // otherwise, filter the cuts again
             RetValue = Dar_CutFilter( pObj, pCut );
             assert( !RetValue );
         }
@@ -628,6 +658,8 @@ Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
             p->nCutsSkipped++;
             pCut->fUsed = 0;
         }
+        else if ( pCut->nLeaves < 2 )
+            return pCutSet;
     }
     // count the number of nontrivial cuts cuts
     Dar_ObjForEachCut( pObj, pCut, i )
diff --git a/src/aig/dar/darInt.h b/src/aig/dar/darInt.h
index 0eb8f9fe..f496a73f 100644
--- a/src/aig/dar/darInt.h
+++ b/src/aig/dar/darInt.h
@@ -101,7 +101,7 @@ struct Dar_Man_t_
 };
 
 static inline Dar_Cut_t *  Dar_ObjCuts( Aig_Obj_t * pObj )                         { return pObj->pData;    }
-static inline void         Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts )   { pObj->pData = pCuts;   }
+static inline void         Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts )   { assert( !Aig_ObjIsNone(pObj) ); pObj->pData = pCuts;   }
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
@@ -126,22 +126,24 @@ static inline void         Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts )
 
 /*=== darBalance.c ========================================================*/
 extern Aig_Man_t *     Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel );
-/*=== darCore.c ========================================================*/
-/*=== darCut.c ========================================================*/
-extern Dar_Cut_t *     Dar_ObjPrepareCuts( Dar_Man_t * p, Aig_Obj_t * pObj );
+/*=== darCore.c ===========================================================*/
+/*=== darCut.c ============================================================*/
+extern void            Dar_ManCutsStart( Dar_Man_t * p );
 extern void            Dar_ManCutsFree( Dar_Man_t * p );
 extern Dar_Cut_t *     Dar_ObjComputeCuts_rec( Dar_Man_t * p, Aig_Obj_t * pObj );
 extern Dar_Cut_t *     Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj );
-/*=== darData.c ========================================================*/
+/*=== darData.c ===========================================================*/
 extern Vec_Int_t *     Dar_LibReadNodes();
 extern Vec_Int_t *     Dar_LibReadOuts();
 extern Vec_Int_t *     Dar_LibReadPrios();
-/*=== darLib.c ==========================================================*/
+/*=== darLib.c ============================================================*/
 extern void            Dar_LibStart();
 extern void            Dar_LibStop();
+extern void            Dar_LibPrepare( int nSubgraphs );
+extern void            Dar_LibReturnCanonicals( unsigned * pCanons );
 extern void            Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Required );
 extern Aig_Obj_t *     Dar_LibBuildBest( Dar_Man_t * p );
-/*=== darMan.c ==========================================================*/
+/*=== darMan.c ============================================================*/
 extern Dar_Man_t *     Dar_ManStart( Aig_Man_t * pAig, Dar_Par_t * pPars );
 extern void            Dar_ManStop( Dar_Man_t * p );
 extern void            Dar_ManPrintStats( Dar_Man_t * p );
diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c
index fce6155b..c3d57b52 100644
--- a/src/aig/dar/darLib.c
+++ b/src/aig/dar/darLib.c
@@ -44,7 +44,7 @@ struct Dar_LibDat_t_ // library object data
     Aig_Obj_t *      pFunc;         // the corresponding AIG node if it exists
     int              Level;         // level of this node after it is constructured
     int              TravId;        // traversal ID of the library object data
-    unsigned char    Area;          // area of the node
+    unsigned char    fMffc;         // set to one if node is part of MFFC
     unsigned char    nLats[3];      // the number of latches on the input/output stem
 };
 
@@ -54,9 +54,6 @@ struct Dar_Lib_t_ // library
     Dar_LibObj_t *   pObjs;         // the set of library objects
     int              nObjs;         // the number of objects used
     int              iObj;          // the current object
-    // object data
-    Dar_LibDat_t *   pDatas;
-    int              nDatas;
     // structures by class
     int              nSubgr[222];   // the number of subgraphs by class
     int *            pSubgr[222];   // the subgraphs for each class
@@ -75,8 +72,24 @@ struct Dar_Lib_t_ // library
     int              nNodes[222];   // the number of nodes by class
     int *            pNodes[222];   // the nodes for each class
     int *            pNodesMem;     // memory for nodes pointers
-    int              pNodesTotal;   // the total number of nodes
-    // information by NPN classes
+    int              nNodesTotal;   // the total number of nodes
+    // prepared library
+    int              nSubgraphs;
+    int              nNodes0Max;
+    // nodes by class
+    int              nNodes0[222];   // the number of nodes by class
+    int *            pNodes0[222];   // the nodes for each class
+    int *            pNodes0Mem;     // memory for nodes pointers
+    int              nNodes0Total;   // the total number of nodes
+    // structures by class
+    int              nSubgr0[222];   // the number of subgraphs by class
+    int *            pSubgr0[222];   // the subgraphs for each class
+    int *            pSubgr0Mem;     // memory for subgraph pointers
+    int              nSubgr0Total;   // the total number of subgraph
+    // object data
+    Dar_LibDat_t *   pDatas;
+    int              nDatas;
+    // information about NPN classes
     char **          pPerms4;
     unsigned short * puCanons; 
     char *           pPhases; 
@@ -104,7 +117,7 @@ static inline int            Dar_LibObjTruth( Dar_LibObj_t * pObj ) { return pOb
   SeeAlso     []
 
 ***********************************************************************/
-Dar_Lib_t * Dar_LibAlloc( int nObjs, int nDatas )
+Dar_Lib_t * Dar_LibAlloc( int nObjs )
 {
     unsigned uTruths[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
     Dar_Lib_t * p;
@@ -115,10 +128,6 @@ Dar_Lib_t * Dar_LibAlloc( int nObjs, int nDatas )
     p->nObjs = nObjs;
     p->pObjs = ALLOC( Dar_LibObj_t, nObjs );
     memset( p->pObjs, 0, sizeof(Dar_LibObj_t) * nObjs );
-    // allocate datas
-    p->nDatas = nDatas;
-    p->pDatas = ALLOC( Dar_LibDat_t, nDatas );
-    memset( p->pObjs, 0, sizeof(Dar_LibDat_t) * nDatas );
     // allocate canonical data
     p->pPerms4 = Extra_Permutations( 4 );
     Extra_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap );
@@ -149,7 +158,9 @@ void Dar_LibFree( Dar_Lib_t * p )
     free( p->pObjs );
     free( p->pDatas );
     free( p->pNodesMem );
+    free( p->pNodes0Mem );
     free( p->pSubgrMem );
+    free( p->pSubgr0Mem );
     free( p->pPriosMem );
     FREE( p->pPlaceMem );
     FREE( p->pScoreMem );
@@ -163,6 +174,31 @@ void Dar_LibFree( Dar_Lib_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns canonical truth tables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_LibReturnCanonicals( unsigned * pCanons )
+{
+    int Visits[222] = {0};
+    int i, k;
+    // find canonical truth tables
+    for ( i = k = 0; i < (1<<16); i++ )
+        if ( !Visits[s_DarLib->pMap[i]] )
+        {
+            Visits[s_DarLib->pMap[i]] = 1;
+            pCanons[k++] = ((i<<16) | i);
+        }
+    assert( k == 222 );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Adds one AND to the library.]
 
   Description []
@@ -196,14 +232,14 @@ void Dar_LibAddNode( Dar_Lib_t * p, int Id0, int Id1, int fCompl0, int fCompl1 )
   SeeAlso     []
 
 ***********************************************************************/
-void Dar_LibSetup_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class )
+void Dar_LibSetup_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class, int fCollect )
 {
     if ( pObj->fTerm || (int)pObj->Num == Class )
         return;
     pObj->Num = Class;
-    Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan0), Class );
-    Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan1), Class );
-    if ( p->pNodesMem )
+    Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan0), Class, fCollect );
+    Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan1), Class, fCollect );
+    if ( fCollect )
         p->pNodes[Class][ p->nNodes[Class]++ ] = pObj-p->pObjs;
     else
         p->nNodes[Class]++;
@@ -239,10 +275,12 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios )
     }
     // allocate memory for the roots of each class
     p->pSubgrMem = ALLOC( int, Vec_IntSize(vOuts) );
+    p->pSubgr0Mem = ALLOC( int, Vec_IntSize(vOuts) );
     p->nSubgrTotal = 0;
     for ( i = 0; i < 222; i++ )
     {
         p->pSubgr[i] = p->pSubgrMem + p->nSubgrTotal;
+        p->pSubgr0[i] = p->pSubgr0Mem + p->nSubgrTotal;
         p->nSubgrTotal += p->nSubgr[i];
         p->nSubgr[i] = 0;
     }
@@ -321,18 +359,20 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios )
     // count nodes in each class
     for ( i = 0; i < 222; i++ )
         for ( k = 0; k < p->nSubgr[i]; k++ )
-            Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i );
+            Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i, 0 );
     // count the total number of nodes
-    p->pNodesTotal = 0;
+    p->nNodesTotal = 0;
     for ( i = 0; i < 222; i++ )
-        p->pNodesTotal += p->nNodes[i];
+        p->nNodesTotal += p->nNodes[i];
     // allocate memory for the nodes of each class
-    p->pNodesMem = ALLOC( int, p->pNodesTotal );
-    p->pNodesTotal = 0;
+    p->pNodesMem = ALLOC( int, p->nNodesTotal );
+    p->pNodes0Mem = ALLOC( int, p->nNodesTotal );
+    p->nNodesTotal = 0;
     for ( i = 0; i < 222; i++ )
     {
-        p->pNodes[i] = p->pNodesMem + p->pNodesTotal;
-        p->pNodesTotal += p->nNodes[i];
+        p->pNodes[i] = p->pNodesMem + p->nNodesTotal;
+        p->pNodes0[i] = p->pNodes0Mem + p->nNodesTotal;
+        p->nNodesTotal += p->nNodes[i];
         p->nNodes[i] = 0;
     }
     // create traversal IDs
@@ -343,11 +383,11 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios )
     for ( i = 0; i < 222; i++ )
     {
          for ( k = 0; k < p->nSubgr[i]; k++ )
-            Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i );
+            Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i, 1 );
          nNodesTotal += p->nNodes[i];
 //printf( "Class %3d : Subgraphs = %4d. Nodes = %5d.\n", i, p->nSubgr[i], p->nNodes[i] );
     }
-    assert( nNodesTotal == p->pNodesTotal );
+    assert( nNodesTotal == p->nNodesTotal );
      // prepare the number of the PI nodes
     for ( i = 0; i < 4; i++ )
         Dar_LibObj(p, i)->Num = i;
@@ -355,6 +395,133 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios )
 
 /**Function*************************************************************
 
+  Synopsis    [Starts the library.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_LibCreateData( Dar_Lib_t * p, int nDatas )
+{
+    if ( p->nDatas == nDatas )
+        return;
+    FREE( p->pDatas );
+    // allocate datas
+    p->nDatas = nDatas;
+    p->pDatas = ALLOC( Dar_LibDat_t, nDatas );
+    memset( p->pDatas, 0, sizeof(Dar_LibDat_t) * nDatas );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one AND to the library.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_LibSetup0_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class, int fCollect )
+{
+    if ( pObj->fTerm || (int)pObj->Num == Class )
+        return;
+    pObj->Num = Class;
+    Dar_LibSetup0_rec( p, Dar_LibObj(p, pObj->Fan0), Class, fCollect );
+    Dar_LibSetup0_rec( p, Dar_LibObj(p, pObj->Fan1), Class, fCollect );
+    if ( fCollect )
+        p->pNodes0[Class][ p->nNodes0[Class]++ ] = pObj-p->pObjs;
+    else
+        p->nNodes0[Class]++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the library.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_LibPrepare( int nSubgraphs )
+{
+    Dar_Lib_t * p = s_DarLib;
+    int i, k, nNodes0Total;
+    if ( p->nSubgraphs == nSubgraphs )
+        return;
+
+    // favor special classes:
+    //  1 : F = (!d*!c*!b*!a)
+    //  4 : F = (!d*!c*!(b*a))
+    // 12 : F = (!d*!(c*!(!b*!a)))
+    // 20 : F = (!d*!(c*b*a))
+
+    // set the subgraph counters 
+    p->nSubgr0Total = 0;
+    for ( i = 0; i < 222; i++ )
+    {
+//        if ( i == 1 || i == 4 || i == 12 || i == 20 ) // special classes 
+        if ( i == 1 ) // special classes 
+            p->nSubgr0[i] = p->nSubgr[i];
+        else
+            p->nSubgr0[i] = AIG_MIN( p->nSubgr[i], nSubgraphs );
+        p->nSubgr0Total += p->nSubgr0[i];
+        for ( k = 0; k < p->nSubgr0[i]; k++ )
+            p->pSubgr0[i][k] = p->pSubgr[i][ p->pPrios[i][k] ];
+    }
+
+    // count the number of nodes
+    // clean node counters
+    for ( i = 0; i < 222; i++ )
+        p->nNodes0[i] = 0;
+    // create traversal IDs
+    for ( i = 0; i < p->iObj; i++ )
+        Dar_LibObj(p, i)->Num = 0xff;
+    // count nodes in each class
+    // count the total number of nodes and the largest class
+    p->nNodes0Total = 0;
+    p->nNodes0Max = 0;
+    for ( i = 0; i < 222; i++ )
+    {
+        for ( k = 0; k < p->nSubgr0[i]; k++ )
+            Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 0 );
+        p->nNodes0Total += p->nNodes0[i];
+        p->nNodes0Max = AIG_MAX( p->nNodes0Max, p->nNodes0[i] );
+    }
+
+    // clean node counters
+    for ( i = 0; i < 222; i++ )
+        p->nNodes0[i] = 0;
+    // create traversal IDs
+    for ( i = 0; i < p->iObj; i++ )
+        Dar_LibObj(p, i)->Num = 0xff;
+    // add the nodes to storage
+    nNodes0Total = 0;
+    for ( i = 0; i < 222; i++ )
+    {
+        for ( k = 0; k < p->nSubgr0[i]; k++ )
+            Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 1 );
+         nNodes0Total += p->nNodes0[i];
+    }
+    assert( nNodes0Total == p->nNodes0Total );
+     // prepare the number of the PI nodes
+    for ( i = 0; i < 4; i++ )
+        Dar_LibObj(p, i)->Num = i;
+
+    // realloc the datas
+    Dar_LibCreateData( p, p->nNodes0Max + 32 ); 
+    // allocated more because Dar_LibBuildBest() sometimes requires more entries
+}
+
+/**Function*************************************************************
+
   Synopsis    [Reads library from array.]
 
   Description []
@@ -374,7 +541,7 @@ Dar_Lib_t * Dar_LibRead()
     vOuts  = Dar_LibReadOuts();
     vPrios = Dar_LibReadPrios();
     // create library
-    p = Dar_LibAlloc( Vec_IntSize(vObjs)/2 + 4, 6000 );
+    p = Dar_LibAlloc( Vec_IntSize(vObjs)/2 + 4 );
     // create nodes
     for ( i = 0; i < vObjs->nSize; i += 2 )
         Dar_LibAddNode( p, vObjs->pArray[i] >> 1, vObjs->pArray[i+1] >> 1,
@@ -383,6 +550,7 @@ Dar_Lib_t * Dar_LibRead()
     Dar_LibSetup( p, vOuts, vPrios );
     Vec_IntFree( vObjs );
     Vec_IntFree( vOuts );
+    Vec_IntFree( vPrios );
     return p;
 }
 
@@ -670,15 +838,20 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class )
     Dar_LibDat_t * pData, * pData0, * pData1;
     Aig_Obj_t * pGhost, * pFanin0, * pFanin1;
     int i;
-    for ( i = 0; i < s_DarLib->nNodes[Class]; i++ )
+    for ( i = 0; i < s_DarLib->nNodes0[Class]; i++ )
     {
         // get one class node, assign its temporary number and set its data
-        pObj = Dar_LibObj(s_DarLib, s_DarLib->pNodes[Class][i]);
+        pObj = Dar_LibObj(s_DarLib, s_DarLib->pNodes0[Class][i]);
         pObj->Num = 4 + i;
+        assert( (int)pObj->Num < s_DarLib->nNodes0Max + 4 );
         pData = s_DarLib->pDatas + pObj->Num;
+        pData->fMffc = 0;
         pData->pFunc = NULL;
         pData->TravId = 0xFFFF;
+
         // explore the fanins
+        assert( (int)Dar_LibObj(s_DarLib, pObj->Fan0)->Num < s_DarLib->nNodes0Max + 4 );
+        assert( (int)Dar_LibObj(s_DarLib, pObj->Fan1)->Num < s_DarLib->nNodes0Max + 4 );
         pData0 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan0)->Num;
         pData1 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan1)->Num;
         pData->Level = 1 + AIG_MAX(pData0->Level, pData1->Level);
@@ -704,9 +877,7 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class )
 
         // clear the node if it is part of MFFC
         if ( pData->pFunc != NULL && Aig_ObjIsTravIdCurrent(p->pAig, pData->pFunc) )
-            pData->pFunc = NULL;
-//if ( Class == 7 )
-//printf( "Evaling node %d at data %d\n", pData->pFunc? pData->pFunc->Id : -1, pObj->Num );
+            pData->fMffc = 1;
     }
 }
 
@@ -729,20 +900,22 @@ int Dar_LibEval_rec( Dar_LibObj_t * pObj, int Out, int nNodesSaved, int Required
         return 0;
     assert( pObj->Num > 3 );
     pData = s_DarLib->pDatas + pObj->Num;
-    if ( pData->pFunc )
+    if ( pData->pFunc && !pData->fMffc )
         return 0;
     if ( pData->Level > Required )
         return 0xff;
     if ( pData->TravId == Out )
-        return pData->Area;
+        return 0;
     pData->TravId = Out;
-    Area = 1 + Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out, nNodesSaved, Required );
+    // this is a new node - get a bound on the area of its branches
+    nNodesSaved--;
+    Area = Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out, nNodesSaved, Required+1 );
     if ( Area > nNodesSaved )
-        return pData->Area = 0xff;
-    Area += Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out, nNodesSaved, Required );
+        return 0xff;
+    Area += Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out, nNodesSaved, Required+1 );
     if ( Area > nNodesSaved )
-        return pData->Area = 0xff;
-    return pData->Area = Area;
+        return 0xff;
+    return Area + 1;
 }
 
 /**Function*************************************************************
@@ -773,25 +946,27 @@ void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Requir
     Class = s_DarLib->pMap[pCut->uTruth];
     Dar_LibEvalAssignNums( p, Class );
     // profile outputs by their savings
-    p->nTotalSubgs += s_DarLib->nSubgr[Class];
-    p->ClassSubgs[Class] += s_DarLib->nSubgr[Class];
-    for ( Out = 0; Out < s_DarLib->nSubgr[Class]; Out++ )
+    p->nTotalSubgs += s_DarLib->nSubgr0[Class];
+    p->ClassSubgs[Class] += s_DarLib->nSubgr0[Class];
+    for ( Out = 0; Out < s_DarLib->nSubgr0[Class]; Out++ )
     {
-        pObj = Dar_LibObj(s_DarLib, s_DarLib->pSubgr[Class][Out]);
-        nNodesAdded = Dar_LibEval_rec( pObj, Out, nNodesSaved, Required );
+        pObj = Dar_LibObj(s_DarLib, s_DarLib->pSubgr0[Class][Out]);
+        if ( Aig_Regular(s_DarLib->pDatas[pObj->Num].pFunc) == pRoot )
+            continue;
+        nNodesAdded = Dar_LibEval_rec( pObj, Out, nNodesSaved - !p->pPars->fUseZeros, Required );
         nNodesGained = nNodesSaved - nNodesAdded;
         if ( fTraining && nNodesGained >= 0 )
             Dar_LibIncrementScore( Class, Out, nNodesGained + 1 );
-        if ( nNodesGained <= 0 )
+        if ( nNodesGained < 0 || (nNodesGained == 0 && !p->pPars->fUseZeros) )
             continue;
-        if ( nNodesGained < p->GainBest || 
-            (nNodesGained == p->GainBest && s_DarLib->pDatas[pObj->Num].Level >= p->GainBest) )
+        if ( nNodesGained <  p->GainBest || 
+            (nNodesGained == p->GainBest && s_DarLib->pDatas[pObj->Num].Level >= p->LevelBest) )
             continue;
         // remember this possibility
         Vec_PtrClear( p->vLeavesBest );
         for ( k = 0; k < (int)pCut->nLeaves; k++ )
             Vec_PtrPush( p->vLeavesBest, s_DarLib->pDatas[k].pFunc );
-        p->OutBest    = s_DarLib->pSubgr[Class][Out];
+        p->OutBest    = s_DarLib->pSubgr0[Class][Out];
         p->OutNumBest = Out;
         p->LevelBest  = s_DarLib->pDatas[pObj->Num].Level;
         p->GainBest   = nNodesGained;
@@ -845,7 +1020,6 @@ Aig_Obj_t * Dar_LibBuildBest_rec( Dar_Man_t * p, Dar_LibObj_t * pObj )
     pFanin0 = Aig_NotCond( pFanin0, pObj->fCompl0 );
     pFanin1 = Aig_NotCond( pFanin1, pObj->fCompl1 );
     pData->pFunc = Aig_And( p->pAig, pFanin0, pFanin1 );
-//printf( "Adding node %d for data %d\n", pData->pFunc->Id, pObj->Num );
     return pData->pFunc;
 }
 
diff --git a/src/aig/dar/darMan.c b/src/aig/dar/darMan.c
index a209503a..8b7c5afb 100644
--- a/src/aig/dar/darMan.c
+++ b/src/aig/dar/darMan.c
@@ -48,7 +48,7 @@ Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_Par_t * pPars )
     p->pPars = pPars;
     p->pAig  = pAig;
     // prepare the internal memory manager
-    p->pMemCuts = Aig_MmFixedStart( p->pPars->nCutsMax * sizeof(Dar_Cut_t), 512 );
+    p->pMemCuts = Aig_MmFixedStart( p->pPars->nCutsMax * sizeof(Dar_Cut_t), 1024 );
     // other data
     p->vLeavesBest = Vec_PtrAlloc( 4 );
     return p;
@@ -89,18 +89,27 @@ void Dar_ManStop( Dar_Man_t * p )
 ***********************************************************************/
 void Dar_ManPrintStats( Dar_Man_t * p )
 {
-    int i, Gain;
+    unsigned pCanons[222];
+    int Gain, i;
+    extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
+
     Gain = p->nNodesInit - Aig_ManNodeNum(p->pAig);
     printf( "NodesBeg = %8d. NodesEnd = %8d. Gain = %6d. (%6.2f %%).  Cut mem = %d Mb\n", 
         p->nNodesInit, Aig_ManNodeNum(p->pAig), Gain, 100.0*Gain/p->nNodesInit, p->nCutMemUsed );
     printf( "Cuts = %8d. Tried = %8d. Used = %8d. Bad = %5d. Skipped = %5d. Ave = %.2f.\n", 
         p->nCutsAll, p->nCutsTried, p->nCutsUsed, p->nCutsBad, p->nCutsSkipped,
         (float)p->nCutsUsed/Aig_ManNodeNum(p->pAig) );
+
+    printf( "Bufs = %5d. BufMax = %5d. BufReplace = %6d. BufFix = %6d.\n", 
+        Aig_ManBufNum(p->pAig), p->pAig->nBufMax, p->pAig->nBufReplaces, p->pAig->nBufFixes );
     PRT( "Cuts  ", p->timeCuts );
     PRT( "Eval  ", p->timeEval );
     PRT( "Other ", p->timeOther );
     PRT( "TOTAL ", p->timeTotal );
-/*
+
+    if ( !p->pPars->fVeryVerbose )
+        return;
+    Dar_LibReturnCanonicals( pCanons );
     for ( i = 0; i < 222; i++ )
     {
         if ( p->ClassGains[i] == 0 && p->ClassTimes[i] == 0 )
@@ -108,10 +117,10 @@ void Dar_ManPrintStats( Dar_Man_t * p )
         printf( "%3d : ", i );
         printf( "G = %6d (%5.2f %%)  ", p->ClassGains[i], Gain? 100.0*p->ClassGains[i]/Gain : 0.0 );
         printf( "S = %8d (%5.2f %%)  ", p->ClassSubgs[i], p->nTotalSubgs? 100.0*p->ClassSubgs[i]/p->nTotalSubgs : 0.0 );
-        printf( "R = %7d  ", p->ClassGains[i]? p->ClassSubgs[i]/p->ClassGains[i] : 9999999 );
-        PRTP( "T", p->ClassTimes[i], p->timeEval );
+        printf( "R = %7d   ", p->ClassGains[i]? p->ClassSubgs[i]/p->ClassGains[i] : 9999999 );
+        Kit_DsdPrintFromTruth( pCanons + i, 4 );
+//        PRTP( "T", p->ClassTimes[i], p->timeEval );
     }
-*/
 }
 
 
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
new file mode 100644
index 00000000..1bcc0466
--- /dev/null
+++ b/src/aig/dar/darRefact.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+  FileName    [darRefact.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting.]
+
+  Synopsis    [Refactoring.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: darRefact.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "darInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/dar/darResub.c b/src/aig/dar/darResub.c
new file mode 100644
index 00000000..f819934e
--- /dev/null
+++ b/src/aig/dar/darResub.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+  FileName    [darResub.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: darResub.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "darInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
new file mode 100644
index 00000000..c98a263e
--- /dev/null
+++ b/src/aig/dar/darScript.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+  FileName    [darScript.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting.]
+
+  Synopsis    [Rewriting scripts.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: darScript.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "darInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/dar/dar_.c b/src/aig/dar/dar_.c
index 08bd8c3e..12fd7d17 100644
--- a/src/aig/dar/dar_.c
+++ b/src/aig/dar/dar_.c
@@ -18,7 +18,7 @@
 
 ***********************************************************************/
 
-#include "dar.h"
+#include "darInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
diff --git a/src/aig/dar/module.make b/src/aig/dar/module.make
index bcf9a2e6..09b45171 100644
--- a/src/aig/dar/module.make
+++ b/src/aig/dar/module.make
@@ -4,4 +4,7 @@ SRC +=    src/aig/dar/darBalance.c \
     src/aig/dar/darData.c \
     src/aig/dar/darLib.c \
     src/aig/dar/darMan.c \
+    src/aig/dar/darRefact.c \
+    src/aig/dar/darResub.c \
+    src/aig/dar/darScript.c \
     src/aig/dar/darTruth.c
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 5338d662..9e1a9a1a 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -45,7 +45,7 @@ Aig_Man_t * Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
     Aig_Man_t * pManAigNew;
     int clk;
     if ( Aig_ManNodeNum(pManAig) == 0 )
-        return Aig_ManDup(pManAig);
+        return Aig_ManDup(pManAig, 1);
 clk = clock();
     assert( Aig_ManLatchNum(pManAig) == 0 );
     p = Fra_ManStart( pManAig, pPars );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 6b305033..c9761783 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -1532,7 +1532,7 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     nCofLevel = 1;
-    fCofactor = 1;
+    fCofactor = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "Nch" ) ) != EOF )
     {
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index c4020127..ba0705ed 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -521,14 +521,24 @@ Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVe
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_Par_t * pPars )
 {
-    Aig_Man_t * pMan;
+    Aig_Man_t * pMan, * pTemp;
     Abc_Ntk_t * pNtkAig;
+    int clk;
     assert( Abc_NtkIsStrash(pNtk) );
     pMan = Abc_NtkToDar( pNtk );
     if ( pMan == NULL )
         return NULL;
 //    Aig_ManPrintStats( pMan );
+
     Dar_ManRewrite( pMan, pPars );
+//    pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
+//    Aig_ManStop( pTemp );
+
+clk = clock();
+    pMan = Aig_ManDup( pTemp = pMan, 0 ); 
+    Aig_ManStop( pTemp );
+PRT( "time", clock() - clk );
+
 //    Aig_ManPrintStats( pMan );
     pNtkAig = Abc_NtkFromDar( pNtk, pMan );
     Aig_ManStop( pMan );
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index 7760b2d1..613741a8 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -155,7 +155,11 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
     }
 
     // put the nodes into the DFS order and reassign their IDs
+    {
+//        int clk = clock();
     Abc_NtkReassignIds( pNtk );
+//        PRT( "time", clock() - clk );
+    }
 //    Abc_AigCheckFaninOrder( pNtk->pManFunc );
     // fix the levels
     if ( fUpdateLevel )
diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c
index fd54f519..5d5e6e93 100644
--- a/src/base/abci/abcTiming.c
+++ b/src/base/abci/abcTiming.c
@@ -811,7 +811,7 @@ void Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
         pTemp->fMarkA = 0;
         assert( Abc_ObjLevel(pTemp) == Lev );
         Abc_ObjSetLevel( pTemp, Abc_ObjLevelNew(pTemp) );
-        // if the level did not change, to need to check the fanout levels
+        // if the level did not change, no need to check the fanout levels
         if ( Abc_ObjLevel(pTemp) == Lev )
             continue;
         // schedule fanout for level update
@@ -858,7 +858,7 @@ void Abc_NtkUpdateReverseLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
         LevelOld = Abc_ObjReverseLevel(pTemp); 
         assert( LevelOld == Lev );
         Abc_ObjSetReverseLevel( pTemp, Abc_ObjReverseLevelNew(pTemp) );
-        // if the level did not change, to need to check the fanout levels
+        // if the level did not change, no need to check the fanout levels
         if ( Abc_ObjReverseLevel(pTemp) == Lev )
             continue;
         // schedule fanins for level update