Version abc70115_2

16 files changed, 470 insertions, 232 deletions

diff --git a/abc.dsp b/abc.dsp
index 63a43722..5efea956 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -1666,6 +1666,10 @@ SOURCE=.\src\opt\res\resCore.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\opt\res\resDivs.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\opt\res\resFilter.c
 # End Source File
 # Begin Source File
diff --git a/abc.rc b/abc.rc
index d5f1675a..54748696 100644
--- a/abc.rc
+++ b/abc.rc
@@ -1,8 +1,8 @@
 # global parameters
 set check         # checks intermediate networks
 #set checkfio      # prints warnings when fanins/fanouts are duplicated
-set checkread     # checks new networks after reading from file
-set backup        # saves backup networks retrived by "undo" and "recall"
+#set checkread     # checks new networks after reading from file
+#set backup        # saves backup networks retrived by "undo" and "recall"
 set savesteps 1   # sets the maximum number of backup networks to save 
 set progressbar   # display the progress bar
 
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 1ec21986..5774afbc 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -232,6 +232,16 @@ static inline int         Abc_TruthWordNum( int nVars )              { return nV
 static inline int         Abc_InfoHasBit( unsigned * p, int i )      { return (p[(i)>>5] & (1<<((i) & 31))) > 0;    }
 static inline void        Abc_InfoSetBit( unsigned * p, int i )      { p[(i)>>5] |= (1<<((i) & 31));                }
 static inline void        Abc_InfoXorBit( unsigned * p, int i )      { p[(i)>>5] ^= (1<<((i) & 31));                }
+static inline unsigned    Abc_InfoRandom()                           { return ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand())); } // #define RAND_MAX 0x7fff
+static inline void        Abc_InfoClear( unsigned * p, int nWords )  { memset( p, 0, sizeof(unsigned) * nWords );   } 
+static inline void        Abc_InfoFill( unsigned * p, int nWords )   { memset( p, 0xff, sizeof(unsigned) * nWords );} 
+static inline void        Abc_InfoNot( unsigned * p, int nWords )    { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = ~p[i];   } 
+static inline int         Abc_InfoIsZero( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) if ( p[i] ) return 0; return 1;  } 
+static inline int         Abc_InfoIsOne( unsigned * p, int nWords )  { int i; for ( i = nWords - 1; i >= 0; i-- ) if ( !p[i] ) return 0; return 1; } 
+static inline void        Abc_InfoCopy( unsigned * p, unsigned * q, int nWords )  { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = q[i];   } 
+static inline void        Abc_InfoAnd( unsigned * p, unsigned * q, int nWords )   { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] &= q[i];  } 
+static inline void        Abc_InfoOr( unsigned * p, unsigned * q, int nWords )    { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= q[i];  } 
+static inline void        Abc_InfoXor( unsigned * p, unsigned * q, int nWords )   { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] ^= q[i];  } 
 
 // checking the network type
 static inline bool        Abc_NtkIsNetlist( Abc_Ntk_t * pNtk )       { return pNtk->ntkType == ABC_NTK_NETLIST;     }
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 99c62504..1761e10e 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -139,6 +139,7 @@ Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig )
     assert( pNtkAig->vObjs->nSize == 0 );
     pMan->pConst1 = Abc_NtkCreateObj( pNtkAig, ABC_OBJ_NODE );
     pMan->pConst1->Type = ABC_OBJ_CONST1;
+    pMan->pConst1->fPhase = 1;
     pNtkAig->nObjCounts[ABC_OBJ_NODE]--;
     // save the current network
     pMan->pNtkAig = pNtkAig;
diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c
index fea98c53..154fe149 100644
--- a/src/base/abc/abcFanio.c
+++ b/src/base/abc/abcFanio.c
@@ -263,7 +263,7 @@ void Abc_ObjReplace( Abc_Obj_t * pNodeOld, Abc_Obj_t * pNodeNew )
     // transfer the fanouts to the old node
     Abc_ObjTransferFanout( pNodeOld, pNodeNew );
     // remove the old node
-    Abc_NtkDeleteObj( pNodeOld );
+    Abc_NtkDeleteObj_rec( pNodeOld, 1 );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index fe218fb7..59f736e5 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -221,7 +221,8 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
     else
         fMode = -1;
 
-    assert( Abc_NtkIsBddLogic(pNtk) ); 
+    assert( Abc_NtkIsBddLogic(pNtk) );
+    if ( dd->size > 0 )
     Cudd_zddVarsFromBddVars( dd, 2 );
     // create the new manager
     pManNew = Extra_MmFlexStart();
diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h
index 6bfc49d5..eef33501 100644
--- a/src/misc/vec/vecVec.h
+++ b/src/misc/vec/vecVec.h
@@ -56,6 +56,8 @@ struct Vec_Vec_t_
     for ( i = LevelStart; (i <= LevelStop) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
 #define Vec_VecForEachLevelReverse( vGlob, vVec, i )                                          \
     for ( i = Vec_VecSize(vGlob) - 1; (i >= 0) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i-- )
+#define Vec_VecForEachLevelReverseStartStop( vGlob, vVec, i, LevelStart, LevelStop )                                          \
+    for ( i = LevelStart; (i >= LevelStop) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i-- )
 
 // iteratores through entries
 #define Vec_VecForEachEntry( vGlob, pEntry, i, k )                                            \
diff --git a/src/opt/res/module.make b/src/opt/res/module.make
index 9d632385..85936f5b 100644
--- a/src/opt/res/module.make
+++ b/src/opt/res/module.make
@@ -1,4 +1,5 @@
 SRC +=  src/opt/res/resCore.c \
+    src/opt/res/resDivs.c \
     src/opt/res/resFilter.c \
     src/opt/res/resSat.c \
     src/opt/res/resSim.c \
diff --git a/src/opt/res/res.h b/src/opt/res/res.h
index ab5dede1..91171d3b 100644
--- a/src/opt/res/res.h
+++ b/src/opt/res/res.h
@@ -43,8 +43,8 @@ struct Res_Win_t_
     // the general data
     int              nWinTfiMax; // the fanin levels
     int              nWinTfoMax; // the fanout levels
-    int              nLevDivMax; // the maximum divisor level
     int              nLevLeaves; // the level where leaves begin
+    int              nLevDivMax; // the maximum divisor level
     Abc_Obj_t *      pNode;      // the node in the center
     // the window data
     Vec_Vec_t *      vLevels;    // nodes by level
@@ -73,6 +73,14 @@ struct Res_Sim_t_
     Vec_Vec_t *      vCands;     // resubstitution candidates
 };
 
+// adds one node to the window
+static inline void Res_WinAddNode( Res_Win_t * p, Abc_Obj_t * pObj )
+{
+    assert( !pObj->fMarkA );
+    pObj->fMarkA = 1;
+    Vec_VecPush( p->vLevels, pObj->Level, pObj );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -81,6 +89,9 @@ struct Res_Sim_t_
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== resDivs.c ==========================================================*/
+extern void          Res_WinDivisors( Res_Win_t * p, int nLevDivMax );
+extern int           Res_WinVisitMffc( Res_Win_t * p );
 /*=== resFilter.c ==========================================================*/
 extern Vec_Ptr_t *   Res_FilterCandidates( Res_Win_t * pWin, Res_Sim_t * pSim );
 /*=== resSat.c ==========================================================*/
@@ -92,11 +103,11 @@ extern int           Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig );
 /*=== resStrash.c ==========================================================*/
 extern Abc_Ntk_t *   Res_WndStrash( Res_Win_t * p );
 /*=== resWnd.c ==========================================================*/
-extern void          Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc );
+extern void          Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels );
 /*=== resWnd.c ==========================================================*/
 extern Res_Win_t *   Res_WinAlloc();
 extern void          Res_WinFree( Res_Win_t * p );
-extern int           Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, int nLevDivMax, Res_Win_t * p );
+extern int           Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p );
 extern void          Res_WinVisitNodeTfo( Res_Win_t * p );
 
 
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index 2ef547e3..0335712d 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -12,9 +12,9 @@
   
   Affiliation [UC Berkeley]
 
-  Date        [Ver. 1.0. Started - June 20, 2005.]
+  Date        [Ver. 1.0. Started - January 15, 2007.]
 
-  Revision    [$Id: resCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: resCore.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -65,25 +65,24 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, int nWindow, int nSimWords, int fVerb
         if ( pObj->Id > nNodesOld )
             break;
         // create the window for this node
-        if ( !Res_WinCompute(pObj, nWindow/10, nWindow%10, pObj->Level - 1, pWin) )
+        if ( !Res_WinCompute(pObj, nWindow/10, nWindow%10, pWin) )
             continue;
+        // collect the divisors
+        Res_WinDivisors( pWin, pObj->Level - 1 );
         // create the AIG for the window
         pAig = Res_WndStrash( pWin );
         // prepare simulation info
-        if ( !Res_SimPrepare( pSim, pAig ) )
+        if ( Res_SimPrepare( pSim, pAig ) )
         {
-            Abc_NtkDelete( pAig );
-            continue;
+            // find resub candidates for the node
+            vFanins = Res_FilterCandidates( pWin, pSim );
+            // check using SAT
+            pFunc = Res_SatFindFunction( pNtk->pManFunc, pWin, vFanins, pAig );
+            // update the network
+            if ( pFunc == NULL )
+                Res_UpdateNetwork( pObj, vFanins, pFunc, pWin->vLevels );
         }
-        // find resub candidates for the node
-        vFanins = Res_FilterCandidates( pWin, pSim );
-        // check using SAT
-        pFunc = Res_SatFindFunction( pNtk->pManFunc, pWin, vFanins, pAig );
         Abc_NtkDelete( pAig );
-        if ( pFunc == NULL )
-            continue;
-        // update the network
-        Res_UpdateNetwork( pObj, vFanins, pFunc );
     }
     Res_WinFree( pWin );
     Res_SimFree( pSim );
diff --git a/src/opt/res/resDivs.c b/src/opt/res/resDivs.c
new file mode 100644
index 00000000..42ec8955
--- /dev/null
+++ b/src/opt/res/resDivs.c
@@ -0,0 +1,199 @@
+/**CFile****************************************************************
+
+  FileName    [resDivs.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  Synopsis    [Collect divisors for the given window.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: resDivs.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "res.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static int Res_WinVisitMffc( Res_Win_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Adds candidate divisors of the node to its window.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
+{
+    Abc_Obj_t * pObj, * pFanout, * pFanin;
+    int i, k, f, m;
+
+    p->nLevDivMax = nLevDivMax;
+
+    // mark the leaves and the internal nodes
+    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
+        pObj->fMarkA = 1;
+    Vec_VecForEachEntry( p->vLevels, pObj, i, k )
+        pObj->fMarkA = 1;
+
+    // prepare the new trav ID
+    Abc_NtkIncrementTravId( p->pNode->pNtk );
+    // mark the TFO of the node (does not increment trav ID)
+    Res_WinVisitNodeTfo( p );
+    // mark the MFFC of the node (does not increment trav ID)
+    Res_WinVisitMffc( p );
+
+    // go through all the legal levels and check if their fanouts can be divisors
+    Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevDivMax - 1 )
+    {
+        // skip nodes in the TFO or in the MFFC of node
+        if ( Abc_NodeIsTravIdCurrent(pObj) )
+            continue;
+        // consider fanouts of this node
+        Abc_ObjForEachFanout( pObj, pFanout, f )
+        {
+            // skip COs
+            if ( !Abc_ObjIsNode(pFanout) ) 
+                continue;
+            // skip nodes in the TFO or in the MFFC of node
+            if ( Abc_NodeIsTravIdCurrent(pFanout) )
+                continue;
+            // skip nodes that are already added
+            if ( pFanout->fMarkA )
+                continue;
+            // skip nodes with large level
+            if ( (int)pFanout->Level > p->nLevDivMax )
+                continue;
+            // skip nodes whose fanins are not in the cone
+            Abc_ObjForEachFanin( pFanout, pFanin, m )
+                if ( !pFanin->fMarkA )
+                    break;
+            if ( m < Abc_ObjFaninNum(pFanin) )
+                continue;
+            // add the node
+            Res_WinAddNode( p, pFanout );
+        }
+    }
+
+    // unmark the leaves and the internal nodes
+    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
+        pObj->fMarkA = 0;
+    Vec_VecForEachEntry( p->vLevels, pObj, i, k )
+        pObj->fMarkA = 0;
+
+    // collect the divisors below the line
+    Vec_PtrClear( p->vDivs );
+    // collect the node fanins first
+    Abc_ObjForEachFanin( pObj, pFanin, m )
+    {
+        Vec_PtrPush( p->vDivs, pFanin );
+        Abc_NodeSetTravIdCurrent( pFanin );
+    }
+    // collect the remaining leaves
+    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
+        if ( !Abc_NodeIsTravIdCurrent(pObj) )
+            Vec_PtrPush( p->vDivs, pObj );
+    // collect remaining unvisited divisors 
+    Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->nLevLeaves, p->nLevDivMax )
+        if ( !Abc_NodeIsTravIdCurrent(pObj) )
+            Vec_PtrPush( p->vDivs, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Dereferences the node's MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_NodeDeref_rec( Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin;
+    int i, Counter = 1;
+    if ( Abc_ObjIsCi(pNode) )
+        return 0;
+    Abc_NodeSetTravIdCurrent( pNode );
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+    {
+        assert( pFanin->vFanouts.nSize > 0 );
+        if ( --pFanin->vFanouts.nSize == 0 )
+            Counter += Res_NodeDeref_rec( pFanin );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [References the node's MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_NodeRef_rec( Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin;
+    int i, Counter = 1;
+    if ( Abc_ObjIsCi(pNode) )
+        return 0;
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+    {
+        if ( pFanin->vFanouts.nSize++ == 0 )
+            Counter += Res_NodeRef_rec( pFanin );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Labels MFFC of the node with the current trav ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_WinVisitMffc( Res_Win_t * p )
+{
+    int Count1, Count2;
+    // dereference the node (mark with the current trav ID)
+    Count1 = Res_NodeDeref_rec( p->pNode );
+    // reference it back
+    Count2 = Res_NodeRef_rec( p->pNode );
+    assert( Count1 == Count2 );
+    return Count1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/res/resFilter.c b/src/opt/res/resFilter.c
index c9615c1e..e2e295a0 100644
--- a/src/opt/res/resFilter.c
+++ b/src/opt/res/resFilter.c
@@ -6,7 +6,7 @@
 
   PackageName [Resynthesis package.]
 
-  Synopsis    []
+  Synopsis    [Filtering resubstitution candidates.]
 
   Author      [Alan Mishchenko]
   
@@ -42,6 +42,23 @@
 ***********************************************************************/
 Vec_Ptr_t * Res_FilterCandidates( Res_Win_t * pWin, Res_Sim_t * pSim )
 {
+    unsigned * pInfo;
+    Abc_Obj_t * pFanin;
+    int i, RetValue;
+    // check that the info the node is one
+    pInfo = Vec_PtrEntry( pSim->vOuts, 1 );
+    RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
+    if ( RetValue == 0 )
+        printf( "Failed 1!" );
+    // collect the fanin info
+    pInfo = Vec_PtrEntry( pSim->vOuts, 0 );
+    Abc_InfoClear( pInfo, pSim->nWordsOut );
+    Abc_ObjForEachFanin( pWin->pNode, pFanin, i )
+        Abc_InfoOr( pInfo, Vec_PtrEntry( pSim->vOuts, 2+i ), pSim->nWordsOut );
+    // check that the simulation info is constant 1
+    RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
+    if ( RetValue == 0 )
+        printf( "Failed 2!" );
     return NULL;
 }
 
diff --git a/src/opt/res/resSim.c b/src/opt/res/resSim.c
index 091c376d..27ce7b6c 100644
--- a/src/opt/res/resSim.c
+++ b/src/opt/res/resSim.c
@@ -25,9 +25,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-// generating random unsigned (#define RAND_MAX 0x7fff)
-#define SIM_RANDOM_UNSIGNED   ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()))
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -48,19 +45,20 @@ Res_Sim_t * Res_SimAlloc( int nWords )
     Res_Sim_t * p;
     p = ALLOC( Res_Sim_t, 1 );
     memset( p, 0, sizeof(Res_Sim_t) );
-    // simulation info
-    p->nWords = nWords;
-    p->nPats = 8 * sizeof(unsigned) * p->nWords;
+    // simulation parameters
+    p->nWords    = nWords;
+    p->nPats     = 8 * sizeof(unsigned) * p->nWords;
     p->nWordsOut = p->nPats * p->nWords;
-    p->nPatsOut = p->nPats * p->nPats;
+    p->nPatsOut  = p->nPats * p->nPats;
+    // simulation info
+    p->vPats     = Vec_PtrAllocSimInfo( 1024, p->nWords );
+    p->vPats0    = Vec_PtrAllocSimInfo( 128,  p->nWords );
+    p->vPats1    = Vec_PtrAllocSimInfo( 128,  p->nWords );
+    p->vOuts     = Vec_PtrAllocSimInfo( 128,  p->nWordsOut );
     // resub candidates
-    p->vPats = Vec_PtrAllocSimInfo( 1024, p->nWords );
-    p->vPats0 = Vec_PtrAllocSimInfo( 128, p->nWords );
-    p->vPats1 = Vec_PtrAllocSimInfo( 128, p->nWords );
-    p->vOuts = Vec_PtrAllocSimInfo( 128, p->nWordsOut );
-    p->vCands = Vec_VecStart( 16 );
+    p->vCands    = Vec_VecStart( 16 );
     // set siminfo for the constant node
-    memset( Vec_PtrEntry(p->vPats,0), 0xff, sizeof(unsigned) * p->nWords );
+    Abc_InfoFill( Vec_PtrEntry(p->vPats,0), p->nWords );
     return p;
 }
 
@@ -100,8 +98,8 @@ void Res_SimAdjust( Res_Sim_t * p, Abc_Ntk_t * pAig )
         p->vOuts = Vec_PtrAllocSimInfo( Abc_NtkPoNum(pAig), p->nWordsOut );
     }
     // clean storage info for patterns
-    memset( Vec_PtrEntry(p->vPats0,0), 0, sizeof(unsigned) * p->nWords * Abc_NtkPiNum(pAig) );
-    memset( Vec_PtrEntry(p->vPats1,0), 0, sizeof(unsigned) * p->nWords * Abc_NtkPiNum(pAig) );
+    Abc_InfoClear( Vec_PtrEntry(p->vPats0,0), p->nWords * Abc_NtkPiNum(pAig) );
+    Abc_InfoClear( Vec_PtrEntry(p->vPats1,0), p->nWords * Abc_NtkPiNum(pAig) );
     p->nPats0 = 0;
     p->nPats1 = 0;
 }
@@ -127,6 +125,44 @@ void Res_SimFree( Res_Sim_t * p )
     free( p );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Free simulation engine.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimReportOne( Res_Sim_t * p )
+{
+    unsigned * pInfoCare, * pInfoNode;
+    int i, nDcs, nOnes, nZeros;
+    pInfoCare = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
+    pInfoNode = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
+    nDcs = nOnes = nZeros = 0;
+    for ( i = 0; i < p->nPats; i++ )
+    {
+        // skip don't-care patterns
+        if ( !Abc_InfoHasBit(pInfoCare, i) )
+        {
+            nDcs++;
+            continue;
+        }
+        // separate offset and onset patterns
+        if ( !Abc_InfoHasBit(pInfoNode, i) )
+            nZeros++;
+        else
+            nOnes++;
+    }
+    printf( "Onset = %3d (%6.2f %%)  ",  nOnes,  100.0*nOnes/p->nPats );
+    printf( "Offset = %3d (%6.2f %%)  ", nZeros, 100.0*nZeros/p->nPats );
+    printf( "Dcset = %3d (%6.2f %%)  ",  nDcs,   100.0*nDcs/p->nPats );
+    printf( "\n" );
+}
+
 
 /**Function*************************************************************
 
@@ -148,7 +184,7 @@ void Res_SimSetRandom( Res_Sim_t * p )
     {
         pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
         for ( w = 0; w < p->nWords; w++ )
-            pInfo[w] = SIM_RANDOM_UNSIGNED;
+            pInfo[w] = Abc_InfoRandom();
     }
 }
 
@@ -215,7 +251,7 @@ void Res_SimPerformOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords )
 
 /**Function*************************************************************
 
-  Synopsis    [Simulates one PO node.]
+  Synopsis    [Simulates one CO node.]
 
   Description []
                
@@ -275,43 +311,41 @@ void Res_SimPerformRound( Res_Sim_t * p )
 ***********************************************************************/
 void Res_SimProcessPats( Res_Sim_t * p )
 {
-    Abc_Obj_t * pCare, * pNode, * pObj;
+    Abc_Obj_t * pObj;
     unsigned * pInfoCare, * pInfoNode;
     int i, j;
-    pCare = Abc_NtkPo( p->pAig, 0 );
-    pNode = Abc_NtkPo( p->pAig, 0 );
-    pInfoCare = Vec_PtrEntry( p->vPats, pCare->Id );
-    pInfoNode = Vec_PtrEntry( p->vPats, pNode->Id );
+    pInfoCare = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
+    pInfoNode = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
     for ( i = 0; i < p->nPats; i++ )
     {
+        // skip don't-care patterns
         if ( !Abc_InfoHasBit(pInfoCare, i) )
             continue;
+        // separate offset and onset patterns
         if ( !Abc_InfoHasBit(pInfoNode, i) )
         {
-            if ( p->nPats0 < p->nPats )
-            {
-                Abc_NtkForEachPi( p->pAig, pObj, j )
-                    if ( Abc_InfoHasBit( Vec_PtrEntry(p->vPats, pObj->Id), i ) )
-                        Abc_InfoSetBit( Vec_PtrEntry(p->vPats0, j), p->nPats0 );
-                p->nPats0++;
-            }
+            if ( p->nPats0 >= p->nPats )
+                continue;
+            Abc_NtkForEachPi( p->pAig, pObj, j )
+                if ( Abc_InfoHasBit( Vec_PtrEntry(p->vPats, pObj->Id), i ) )
+                    Abc_InfoSetBit( Vec_PtrEntry(p->vPats0, j), p->nPats0 );
+            p->nPats0++;
         }
         else
         {
-            if ( p->nPats1 < p->nPats )
-            {
-                Abc_NtkForEachPi( p->pAig, pObj, j )
-                    if ( Abc_InfoHasBit( Vec_PtrEntry(p->vPats, pObj->Id), i ) )
-                        Abc_InfoSetBit( Vec_PtrEntry(p->vPats1, j), p->nPats1 );
-                p->nPats1++;
-            }
+            if ( p->nPats1 >= p->nPats )
+                continue;
+            Abc_NtkForEachPi( p->pAig, pObj, j )
+                if ( Abc_InfoHasBit( Vec_PtrEntry(p->vPats, pObj->Id), i ) )
+                    Abc_InfoSetBit( Vec_PtrEntry(p->vPats1, j), p->nPats1 );
+            p->nPats1++;
         }
     }
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Duplicates the simulation info to fill the space.]
+  Synopsis    [Pads the extra space with duplicated simulation info.]
 
   Description []
                
@@ -323,13 +357,16 @@ void Res_SimProcessPats( Res_Sim_t * p )
 void Res_SimPadSimInfo( Vec_Ptr_t * vPats, int nPats, int nWords )
 {
     unsigned * pInfo;
-    int i, w, iWords;
+    int i, w, iWords, nBits;
     iWords = nPats / (8 * sizeof(unsigned));
+    nBits = nPats % (8 * sizeof(unsigned));
     if ( iWords == nWords )
         return;
     Vec_PtrForEachEntry( vPats, pInfo, i )
+    {
         for ( w = iWords; w < nWords; i++ )
             pInfo[w] = pInfo[0];
+    }
 }
 
 /**Function*************************************************************
@@ -343,7 +380,7 @@ void Res_SimPadSimInfo( Vec_Ptr_t * vPats, int nPats, int nWords )
   SeeAlso     []
 
 ***********************************************************************/
-void Res_SimDeriveInfoDuplicate( Res_Sim_t * p )
+void Res_SimDeriveInfoReplicate( Res_Sim_t * p )
 {
     unsigned * pInfo, * pInfo2;
     Abc_Obj_t * pObj;
@@ -407,6 +444,8 @@ int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig )
         Res_SimSetRandom( p );
         Res_SimPerformRound( p );
         Res_SimProcessPats( p );
+        if ( Limit == 19 )
+            Res_SimReportOne( p );
     }
     if ( p->nPats0 < 32 || p->nPats1 < 32 )
         return 0;
@@ -418,7 +457,7 @@ int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig )
     // resimulate 0-patterns
     Res_SimSetGiven( p, p->vPats0 );
     Res_SimPerformRound( p );
-    Res_SimDeriveInfoDuplicate( p );
+    Res_SimDeriveInfoReplicate( p );
     // resimulate 1-patterns
     Res_SimSetGiven( p, p->vPats1 );
     Res_SimPerformRound( p );
diff --git a/src/opt/res/resStrash.c b/src/opt/res/resStrash.c
index 22244df3..2c112642 100644
--- a/src/opt/res/resStrash.c
+++ b/src/opt/res/resStrash.c
@@ -6,7 +6,7 @@
 
   PackageName [Resynthesis package.]
 
-  Synopsis    [Strashes the window.]
+  Synopsis    [Structural hashing of the nodes in the window.]
 
   Author      [Alan Mishchenko]
   
@@ -52,7 +52,6 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p )
     assert( Abc_NtkHasAig(p->pNode->pNtk) );
     // create the network
     pAig = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
-    // duplicate the name and the spec
     pAig->pName = Extra_UtilStrsav( "window" );
     // create the inputs
     Vec_PtrForEachEntry( p->vLeaves, pObj, i )
@@ -61,7 +60,8 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p )
     Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->nLevLeaves + 1, (int)p->pNode->Level + p->nWinTfoMax )
     {
         pObj->pCopy = Abc_ConvertAigToAig( pAig, pObj );
-        pObj->pCopy = Abc_ObjNotCond( pObj->pCopy, pObj == p->pNode );
+        if ( pObj == p->pNode )
+            pObj->pCopy = Abc_ObjNot( pObj->pCopy );
     }
     // collect the PO outputs
     vPairs = Vec_PtrAlloc( 2 * Vec_PtrSize(p->vRoots) );
@@ -71,6 +71,7 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p )
         Vec_PtrPush( vPairs, NULL );
     }
     // mark the TFO of the node
+    Abc_NtkIncrementTravId( p->pNode->pNtk );
     Res_WinVisitNodeTfo( p );
     // redo strashing in the TFO
     p->pNode->pCopy = Abc_ObjNot( p->pNode->pCopy );
diff --git a/src/opt/res/resUpdate.c b/src/opt/res/resUpdate.c
index cb76e01a..f79176bc 100644
--- a/src/opt/res/resUpdate.c
+++ b/src/opt/res/resUpdate.c
@@ -25,13 +25,63 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Incrementally updates level of the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels )
+{
+    Abc_Obj_t * pObjNew, * pFanin, * pFanout, * pTemp;
+    int i, k, m;
+    // create the new node
+    pObjNew = Abc_NtkCreateNode( pObj->pNtk );
+    pObjNew->pData = pFunc;
+    Vec_PtrForEachEntry( vFanins, pFanin, i )
+        Abc_ObjAddFanin( pObjNew, pFanin );
+    // replace the old node by the new node
+    pObjNew->Level = pObj->Level;
+    Abc_ObjReplace( pObj, pObjNew );
+    // check if level has changed
+    if ( (int)pObjNew->Level == Res_UpdateNetworkLevelNew(pObjNew) )
+        return;
+    // start the data structure for level update
+    Vec_VecClear( vLevels );
+    Vec_VecPush( vLevels, pObjNew->Level, pObjNew );
+    pObjNew->fMarkA = 1;
+    // recursively update level
+    Vec_VecForEachEntryStart( vLevels, pTemp, i, k, pObjNew->Level )
+    {
+        pTemp->fMarkA = 0;
+        pTemp->Level = Res_UpdateNetworkLevelNew( pTemp );
+        // if the level did not change, to need to check the fanout levels
+        if ( (int)pTemp->Level == i )
+            continue;
+        // schedule fanout for level update
+        Abc_ObjForEachFanout( pTemp, pFanout, m )
+            if ( !Abc_ObjIsCo(pFanout) && !pFanout->fMarkA )
+            {
+                Vec_VecPush( vLevels, pFanout->Level, pFanout );
+                pFanout->fMarkA = 1;
+            }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the level of the node using its fanin levels.]
 
   Description []
                
@@ -40,8 +90,13 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc )
+int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj )
 {
+    Abc_Obj_t * pFanin;
+    int i, Level = 0;
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        Level = ABC_MAX( Level, (int)pFanin->Level );
+    return Level + 1;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/res/resWin.c b/src/opt/res/resWin.c
index b50d3274..a2504d50 100644
--- a/src/opt/res/resWin.c
+++ b/src/opt/res/resWin.c
@@ -74,73 +74,60 @@ void Res_WinFree( Res_Win_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Adds one node to the window.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Res_WinAddNode( Res_Win_t * p, Abc_Obj_t * pObj )
-{
-    assert( !pObj->fMarkA );
-    pObj->fMarkA = 1;
-    Vec_VecPush( p->vLevels, pObj->Level, pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Expands the frontier by one level.]
+  Synopsis    [Collects nodes in the limited TFI of the node.]
 
-  Description []
+  Description [Marks the collected nodes.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Res_WinCollectTfiOne( Res_Win_t * p, int Level )
+void Res_WinCollectNodeTfi( Res_Win_t * p )
 {
     Vec_Ptr_t * vFront;
     Abc_Obj_t * pObj, * pFanin;
-    int i, k;
-    assert( Level > 0 );
-    vFront = Vec_VecEntry( p->vLevels, Level );
-    Vec_PtrForEachEntry( vFront, pObj, i )
+    int i, k, m;
+    // expand storage for levels
+    if ( Vec_VecSize( p->vLevels ) <= (int)p->pNode->Level + p->nWinTfoMax )
+        Vec_VecExpand( p->vLevels, (int)p->pNode->Level + p->nWinTfoMax );
+    // start the frontier
+    Vec_VecClear( p->vLevels );
+    Res_WinAddNode( p, p->pNode );
+    // add one level at a time
+    Vec_VecForEachLevelReverseStartStop( p->vLevels, vFront, i, p->pNode->Level, p->nLevLeaves -1 )
     {
-        Abc_ObjForEachFanin( pObj, pFanin, k )
-        {
-            if ( !pFanin->fMarkA )
-                Res_WinAddNode( p, pFanin );
-        }
+        Vec_PtrForEachEntry( vFront, pObj, k )
+            Abc_ObjForEachFanin( pObj, pFanin, m )
+                if ( !pFanin->fMarkA )
+                    Res_WinAddNode( p, pFanin );
     }
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Collects nodes in the limited TFI of the node.]
+  Synopsis    [Collect all the nodes that fanin into the window nodes.]
 
-  Description [Marks the collected nodes with the current trav ID.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Res_WinCollectTfi( Res_Win_t * p )
+void Res_WinCollectLeaves( Res_Win_t * p )
 {
-    int i;
-    // expand storage for levels
-    if ( Vec_VecSize( p->vLevels ) <= (int)p->pNode->Level + p->nWinTfoMax )
-        Vec_VecExpand( p->vLevels, (int)p->pNode->Level + p->nWinTfoMax );
-    // start the frontier
-    Vec_VecClear( p->vLevels );
-    Res_WinAddNode( p, p->pNode );
-    // add one level at a time
-    for ( i = p->pNode->Level; i > p->nLevLeaves; i-- )
-        Res_WinCollectTfiOne( p, i );
+    Vec_Ptr_t * vLevel;
+    Abc_Obj_t * pObj;
+    int i, k;
+    // add the leaves
+    Vec_PtrClear( p->vLeaves );
+    // collect the nodes below the given level
+    Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevLeaves )
+        Vec_PtrPush( p->vLeaves, pObj );
+    // remove leaves from the set
+    Vec_VecForEachLevelStartStop( p->vLevels, vLevel, i, 0, p->nLevLeaves )
+        Vec_PtrClear( vLevel );
 }
 
 /**Function*************************************************************
@@ -154,7 +141,7 @@ void Res_WinCollectTfi( Res_Win_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Res_WinSweepTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNode )
+void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNode )
 {
     Abc_Obj_t * pFanout;
     int i;
@@ -164,7 +151,7 @@ void Res_WinSweepTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNode )
         return;
     Abc_NodeSetTravIdCurrent( pObj );
     Abc_ObjForEachFanout( pObj, pFanout, i )
-        Res_WinSweepTfo_rec( pFanout, nLevelLimit, pNode );
+        Res_WinSweepLeafTfo_rec( pFanout, nLevelLimit, pNode );
 }
 
 /**Function*************************************************************
@@ -178,13 +165,13 @@ void Res_WinSweepTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-void Res_WinSweepTfo( Res_Win_t * p )
+void Res_WinSweepLeafTfo( Res_Win_t * p )
 {
     Abc_Obj_t * pObj;
-    int i, k;
+    int i;
     Abc_NtkIncrementTravId( p->pNode->pNtk );
-    Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevLeaves )
-        Res_WinSweepTfo_rec( pObj, p->pNode->Level + p->nWinTfoMax, p->pNode );
+    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
+        Res_WinSweepLeafTfo_rec( pObj, p->pNode->Level + p->nWinTfoMax, p->pNode );
 }
 
 /**Function*************************************************************
@@ -239,7 +226,7 @@ void Res_WinCollectRoots( Res_Win_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Recursively augments the window.]
+  Synopsis    [Recursively adds missing nodes and leaves.]
 
   Description []
                
@@ -252,10 +239,14 @@ void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pFanin;
     int i;
-    if ( !Abc_NodeIsTravIdCurrent(pObj) )
-        return;
     if ( pObj->fMarkA )
         return;
+    if ( !Abc_NodeIsTravIdCurrent(pObj) )
+    {
+        Vec_PtrPush( p->vLeaves, pObj );
+        pObj->fMarkA = 1;
+        return;
+    }
     Res_WinAddNode( p, pObj );
     // visit the fanins of the node
     Abc_ObjForEachFanin( pObj, pFanin, i )
@@ -264,7 +255,7 @@ void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj )
 
 /**Function*************************************************************
 
-  Synopsis    [Adds to the window visited nodes in the TFI of the roots.]
+  Synopsis    [Adds to the window nodes and leaves in the TFI of the roots.]
 
   Description []
                
@@ -283,7 +274,7 @@ void Res_WinAddMissing( Res_Win_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Collect all the nodes that fanin into the window nodes.]
+  Synopsis    [Unmarks the leaves and nodes of the window.]
 
   Description []
                
@@ -292,32 +283,19 @@ void Res_WinAddMissing( Res_Win_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Res_WinCollectLeaves( Res_Win_t * p )
+void Res_WinUnmark( Res_Win_t * p )
 {
-    Abc_Obj_t * pObj, * pFanin;
-    int i, k, f;
-    // add the leaves
-    Vec_PtrClear( p->vLeaves );
-    // collect the nodes below the given level
-    Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevLeaves )
-        Vec_PtrPush( p->vLeaves, pObj );
-    // add to leaves the fanins of the nodes above the given level
-    Vec_VecForEachEntryStart( p->vLevels, pObj, i, k, p->nLevLeaves + 1 )
-    {
-        Abc_ObjForEachFanin( pObj, pFanin, f )
-        {
-            if ( !pFanin->fMarkA )
-            {
-                pFanin->fMarkA = 1;
-                Vec_PtrPush( p->vLeaves, pFanin );
-            }
-        }
-    }
+    Abc_Obj_t * pObj;
+    int i, k;
+    Vec_VecForEachEntry( p->vLevels, pObj, i, k )
+        pObj->fMarkA = 0;
+    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
+        pObj->fMarkA = 0;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Labels the TFO of the node with the current trav ID.]
 
   Description []
                
@@ -329,83 +307,7 @@ void Res_WinCollectLeaves( Res_Win_t * p )
 void Res_WinVisitNodeTfo( Res_Win_t * p )
 {
     // mark the TFO of the node
-    Abc_NtkIncrementTravId( p->pNode->pNtk );
-    Res_WinSweepTfo_rec( p->pNode, p->nLevDivMax, NULL );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Res_WinCollectDivisors( Res_Win_t * p )
-{
-    Abc_Obj_t * pObj, * pFanout, * pFanin;
-    int i, k, f, m;
-    // mark the TFO of the node
-    Res_WinVisitNodeTfo( p );
-    // go through all the legal levels and check if their fanouts can be divisors
-    Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevDivMax - 1 )
-    {
-        Abc_ObjForEachFanout( pObj, pFanout, f )
-        {
-            // skip COs
-            if ( !Abc_ObjIsNode(pFanout) ) 
-                continue;
-            // skip nodes in the TFO of node
-            if ( Abc_NodeIsTravIdCurrent(pFanout) )
-                continue;
-            // skip nodes that are already added
-            if ( pFanout->fMarkA )
-                continue;
-            // skip nodes with large level
-            if ( (int)pFanout->Level > p->nLevDivMax )
-                continue;
-            // skip nodes whose fanins are not in the cone
-            Abc_ObjForEachFanin( pFanout, pFanin, m )
-                if ( !pFanin->fMarkA )
-                    break;
-            if ( m < Abc_ObjFaninNum(pFanin) )
-                continue;
-            // add the node
-            Res_WinAddNode( p, pFanout );
-        }
-    }
-    // collect the divisors below the line
-    Vec_PtrClear( p->vDivs );
-    Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevDivMax )
-        Vec_PtrPush( p->vDivs, pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Res_WinUnmark( Res_Win_t * p )
-{
-    Vec_Ptr_t * vLevel;
-    Abc_Obj_t * pObj;
-    int i, k;
-    Vec_VecForEachEntry( p->vLevels, pObj, i, k )
-        pObj->fMarkA = 0;
-    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
-        pObj->fMarkA = 0;
-    // remove leaves from the set
-    Vec_VecForEachLevelStartStop( p->vLevels, vLevel, i, 0, p->nLevLeaves )
-        Vec_PtrClear( vLevel );
+    Res_WinSweepLeafTfo_rec( p->pNode, p->nLevDivMax, NULL );
 }
 
 /**Function*************************************************************
@@ -419,7 +321,7 @@ void Res_WinUnmark( Res_Win_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, int nLevDivMax, Res_Win_t * p )
+int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p )
 {
     assert( Abc_ObjIsNode(pNode) );
     assert( nWinTfiMax > 0 && nWinTfoMax > 0 );
@@ -427,23 +329,19 @@ int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, int nLevD
     p->pNode = pNode;
     p->nWinTfiMax = nWinTfiMax;
     p->nWinTfoMax = nWinTfoMax;
-    p->nLevDivMax = nLevDivMax;
     p->nLevLeaves = ABC_MAX( 0, p->pNode->Level - p->nWinTfiMax - 1 );
-    // collect the nodes in TFI cone of pNode down to the given level (nWinTfiMax)
-    Res_WinCollectTfi( p );
-    // mark the TFO of the collected nodes up to the given level (nWinTfoMax)
-    Res_WinSweepTfo( p );
+    p->nLevDivMax = 0;
+    Vec_PtrClear( p->vDivs );
+    // collect the nodes in TFI cone of pNode above the level of leaves (p->nLevLeaves)
+    Res_WinCollectNodeTfi( p );
+    // find the leaves of the window
+    Res_WinCollectLeaves( p );
+    // mark the TFO of the collected nodes up to the given level (p->pNode->Level + p->nWinTfoMax)
+    Res_WinSweepLeafTfo( p );
     // find the roots of the window
     Res_WinCollectRoots( p );
     // add the nodes in the TFI of the roots that are not yet in the window
     Res_WinAddMissing( p );
-    // find the leaves of the window
-    Res_WinCollectLeaves( p );
-    // collect the divisors up to the given maximum divisor level (nLevDivMax)
-    if ( nLevDivMax >= 0 )
-        Res_WinCollectDivisors( p );
-    else
-        Vec_PtrClear( p->vDivs );
     // unmark window nodes
     Res_WinUnmark( p );
     return 1;