Version abc80130_2

12 files changed, 3727 insertions, 0 deletions

diff --git a/src/opt/res/module.make b/src/opt/res/module.make
new file mode 100644
index 00000000..52d8a315
--- /dev/null
+++ b/src/opt/res/module.make
@@ -0,0 +1,7 @@
+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 \
+    src/opt/res/resStrash.c \
+    src/opt/res/resWin.c
diff --git a/src/opt/res/res.h b/src/opt/res/res.h
new file mode 100644
index 00000000..3c3431bf
--- /dev/null
+++ b/src/opt/res/res.h
@@ -0,0 +1,75 @@
+/**CFile****************************************************************
+
+  FileName    [res.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: res.h,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __RES_H__
+#define __RES_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Res_Par_t_ Res_Par_t;
+struct Res_Par_t_
+{
+    // general parameters
+    int           nWindow;       // window size
+    int           nGrowthLevel;  // the maximum allowed growth in level after one iteration of resynthesis
+    int           nSimWords;     // the number of simulation words 
+    int           nCands;        // the number of candidates to try
+    int           fArea;         // performs optimization for area
+    int           fDelay;        // performs optimization for delay
+    int           fVerbose;      // enable basic stats
+    int           fVeryVerbose;  // enable detailed stats
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== resCore.c ==========================================================*/
+extern int        Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars );
+
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
new file mode 100644
index 00000000..cb448fc0
--- /dev/null
+++ b/src/opt/res/resCore.c
@@ -0,0 +1,419 @@
+/**CFile****************************************************************
+
+  FileName    [resCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  Synopsis    [Top-level resynthesis procedure.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: resCore.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "resInt.h"
+#include "kit.h"
+#include "satStore.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Res_Man_t_ Res_Man_t;
+struct Res_Man_t_
+{
+    // general parameters
+    Res_Par_t *   pPars;
+    // specialized manager
+    Res_Win_t *   pWin;          // windowing manager
+    Abc_Ntk_t *   pAig;          // the strashed window
+    Res_Sim_t *   pSim;          // simulation manager
+    Sto_Man_t *   pCnf;          // the CNF of the SAT problem
+    Int_Man_t *   pMan;          // interpolation manager;
+    Vec_Int_t *   vMem;          // memory for intermediate SOPs
+    Vec_Vec_t *   vResubs;       // resubstitution candidates of the AIG
+    Vec_Vec_t *   vResubsW;      // resubstitution candidates of the window
+    Vec_Vec_t *   vLevels;       // levelized structure for updating
+    // statistics
+    int           nWins;         // the number of windows tried
+    int           nWinNodes;     // the total number of window nodes
+    int           nDivNodes;     // the total number of divisors
+    int           nWinsTriv;     // the total number of trivial windows
+    int           nWinsUsed;     // the total number of useful windows (with at least one candidate)
+    int           nConstsUsed;   // the total number of constant nodes under ODC
+    int           nCandSets;     // the total number of candidates
+    int           nProvedSets;   // the total number of proved groups
+    int           nSimEmpty;     // the empty simulation info
+    int           nTotalNets;    // the total number of nets
+    int           nTotalNodes;   // the total number of nodess
+    int           nTotalNets2;   // the total number of nets
+    int           nTotalNodes2;  // the total number of nodess
+    // runtime
+    int           timeWin;       // windowing
+    int           timeDiv;       // divisors
+    int           timeAig;       // strashing
+    int           timeSim;       // simulation
+    int           timeCand;      // resubstitution candidates
+    int           timeSatTotal;  // SAT solving total 
+    int           timeSatSat;    // SAT solving (sat calls)
+    int           timeSatUnsat;  // SAT solving (unsat calls)
+    int           timeSatSim;    // SAT solving (simulation)
+    int           timeInt;       // interpolation 
+    int           timeUpd;       // updating  
+    int           timeTotal;     // total runtime
+};
+
+extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
+
+extern int s_ResynTime;
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocate resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Res_Man_t * Res_ManAlloc( Res_Par_t * pPars )
+{
+    Res_Man_t * p;
+    p = ALLOC( Res_Man_t, 1 );
+    memset( p, 0, sizeof(Res_Man_t) );
+    assert( pPars->nWindow > 0 && pPars->nWindow < 100 );
+    assert( pPars->nCands > 0 && pPars->nCands < 100 );
+    p->pPars = pPars;
+    p->pWin = Res_WinAlloc();
+    p->pSim = Res_SimAlloc( pPars->nSimWords );
+    p->pMan = Int_ManAlloc();
+    p->vMem = Vec_IntAlloc( 0 );
+    p->vResubs  = Vec_VecStart( pPars->nCands );
+    p->vResubsW = Vec_VecStart( pPars->nCands );
+    p->vLevels  = Vec_VecStart( 32 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocate resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_ManFree( Res_Man_t * p )
+{
+    if ( p->pPars->fVerbose )
+    {
+        printf( "Reduction in nodes = %5d. (%.2f %%) ", 
+            p->nTotalNodes-p->nTotalNodes2, 
+            100.0*(p->nTotalNodes-p->nTotalNodes2)/p->nTotalNodes );
+        printf( "Reduction in edges = %5d. (%.2f %%) ", 
+            p->nTotalNets-p->nTotalNets2, 
+            100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets );
+        printf( "\n" );
+
+        printf( "Winds = %d. ", p->nWins );
+        printf( "Nodes = %d. (Ave = %5.1f)  ", p->nWinNodes, 1.0*p->nWinNodes/p->nWins );
+        printf( "Divs = %d. (Ave = %5.1f)  ",  p->nDivNodes, 1.0*p->nDivNodes/p->nWins );
+        printf( "\n" );
+        printf( "WinsTriv = %d. ", p->nWinsTriv );
+        printf( "SimsEmpt = %d. ", p->nSimEmpty );
+        printf( "Const = %d. ", p->nConstsUsed );
+        printf( "WindUsed = %d. ", p->nWinsUsed );
+        printf( "Cands = %d. ", p->nCandSets );
+        printf( "Proved = %d.", p->nProvedSets );
+        printf( "\n" );
+
+        PRTP( "Windowing  ", p->timeWin,      p->timeTotal );
+        PRTP( "Divisors   ", p->timeDiv,      p->timeTotal );
+        PRTP( "Strashing  ", p->timeAig,      p->timeTotal );
+        PRTP( "Simulation ", p->timeSim,      p->timeTotal );
+        PRTP( "Candidates ", p->timeCand,     p->timeTotal );
+        PRTP( "SAT solver ", p->timeSatTotal, p->timeTotal );
+        PRTP( "    sat    ", p->timeSatSat,   p->timeTotal );
+        PRTP( "    unsat  ", p->timeSatUnsat, p->timeTotal );
+        PRTP( "    simul  ", p->timeSatSim,   p->timeTotal );
+        PRTP( "Interpol   ", p->timeInt,      p->timeTotal );
+        PRTP( "Undating   ", p->timeUpd,      p->timeTotal );
+        PRTP( "TOTAL      ", p->timeTotal,    p->timeTotal );
+    }
+    Res_WinFree( p->pWin );
+    if ( p->pAig ) Abc_NtkDelete( p->pAig );
+    Res_SimFree( p->pSim );
+    if ( p->pCnf ) Sto_ManFree( p->pCnf );
+    Int_ManFree( p->pMan );
+    Vec_IntFree( p->vMem );
+    Vec_VecFree( p->vResubs );
+    Vec_VecFree( p->vResubsW );
+    Vec_VecFree( p->vLevels );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  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;
+    int k;
+    // create the new node
+    pObjNew = Abc_NtkCreateNode( pObj->pNtk );
+    pObjNew->pData = pFunc;
+    Vec_PtrForEachEntry( vFanins, pFanin, k )
+        Abc_ObjAddFanin( pObjNew, pFanin );
+    // replace the old node by the new node
+    // update the level of the node
+    Abc_NtkUpdate( pObj, pObjNew, vLevels );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Entrace into the resynthesis package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
+{
+    ProgressBar * pProgress;
+    Res_Man_t * p;
+    Abc_Obj_t * pObj;
+    Hop_Obj_t * pFunc;
+    Kit_Graph_t * pGraph;
+    Vec_Ptr_t * vFanins;
+    unsigned * puTruth;
+    int i, k, RetValue, nNodesOld, nFanins, nFaninsMax;
+    int clk, clkTotal = clock();
+
+    // start the manager
+    p = Res_ManAlloc( pPars );
+    p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
+    p->nTotalNodes = Abc_NtkNodeNum(pNtk);
+    nFaninsMax = Abc_NtkGetFaninMax(pNtk);
+    if ( nFaninsMax > 8 )
+        nFaninsMax = 8;
+
+    // perform the network sweep
+    Abc_NtkSweep( pNtk, 0 );
+
+    // convert into the AIG
+    if ( !Abc_NtkToAig(pNtk) )
+    {
+        fprintf( stdout, "Converting to BDD has failed.\n" );
+        Res_ManFree( p );
+        return 0;
+    }
+    assert( Abc_NtkHasAig(pNtk) );
+
+    // set the number of levels
+    Abc_NtkLevel( pNtk );
+    Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
+
+    // try resynthesizing nodes in the topological order
+    nNodesOld = Abc_NtkObjNumMax(pNtk);
+    pProgress = Extra_ProgressBarStart( stdout, nNodesOld );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        if ( !Abc_ObjIsNode(pObj) )
+            continue;
+        if ( Abc_ObjFaninNum(pObj) > 8 )
+            continue;
+        if ( pObj->Id > nNodesOld )
+            break;
+
+        // create the window for this node
+clk = clock();
+        RetValue = Res_WinCompute( pObj, p->pPars->nWindow/10, p->pPars->nWindow%10, p->pWin );
+p->timeWin += clock() - clk;
+        if ( !RetValue )
+            continue;
+        p->nWinsTriv += Res_WinIsTrivial( p->pWin );
+
+        if ( p->pPars->fVeryVerbose )
+        {
+            printf( "%5d (lev=%2d) : ", pObj->Id, pObj->Level );
+            printf( "Win = %3d/%3d/%4d/%3d   ", 
+                Vec_PtrSize(p->pWin->vLeaves), 
+                Vec_PtrSize(p->pWin->vBranches),
+                Vec_PtrSize(p->pWin->vNodes), 
+                Vec_PtrSize(p->pWin->vRoots) );
+        }
+
+        // collect the divisors
+clk = clock();
+        Res_WinDivisors( p->pWin, Abc_ObjRequiredLevel(pObj) - 1 );
+p->timeDiv += clock() - clk;
+
+        p->nWins++;
+        p->nWinNodes += Vec_PtrSize(p->pWin->vNodes);
+        p->nDivNodes += Vec_PtrSize( p->pWin->vDivs);
+
+        if ( p->pPars->fVeryVerbose )
+        {
+            printf( "D = %3d ", Vec_PtrSize(p->pWin->vDivs) );
+            printf( "D+ = %3d ", p->pWin->nDivsPlus );
+        }
+
+        // create the AIG for the window
+clk = clock();
+        if ( p->pAig ) Abc_NtkDelete( p->pAig );
+        p->pAig = Res_WndStrash( p->pWin );
+p->timeAig += clock() - clk;
+
+        if ( p->pPars->fVeryVerbose )
+        {
+            printf( "AIG = %4d ", Abc_NtkNodeNum(p->pAig) );
+            printf( "\n" );
+        }
+ 
+        // prepare simulation info
+clk = clock();
+        RetValue = Res_SimPrepare( p->pSim, p->pAig, Vec_PtrSize(p->pWin->vLeaves), 0 ); //p->pPars->fVerbose );
+p->timeSim += clock() - clk;
+        if ( !RetValue )
+        {
+            p->nSimEmpty++;
+            continue;
+        }
+
+        // consider the case of constant node
+        if ( p->pSim->fConst0 || p->pSim->fConst1 )
+        {
+            p->nConstsUsed++;
+
+            pFunc = p->pSim->fConst1? Hop_ManConst1(pNtk->pManFunc) : Hop_ManConst0(pNtk->pManFunc);
+            vFanins = Vec_VecEntry( p->vResubsW, 0 );
+            Vec_PtrClear( vFanins );
+            Res_UpdateNetwork( pObj, vFanins, pFunc, p->vLevels );
+            continue;
+        }
+
+//        printf( " " );
+
+        // find resub candidates for the node
+clk = clock();
+        if ( p->pPars->fArea )
+            RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW, nFaninsMax, 1 );
+        else
+            RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW, nFaninsMax, 0 );
+p->timeCand += clock() - clk;
+        p->nCandSets += RetValue;
+        if ( RetValue == 0 )
+            continue;
+
+//        printf( "%d(%d) ", Vec_PtrSize(p->pWin->vDivs), RetValue );
+
+        p->nWinsUsed++;
+
+        // iterate through candidate resubstitutions
+        Vec_VecForEachLevel( p->vResubs, vFanins, k )
+        {
+            if ( Vec_PtrSize(vFanins) == 0 )
+                break;
+
+            // solve the SAT problem and get clauses
+clk = clock();
+            if ( p->pCnf ) Sto_ManFree( p->pCnf );
+            p->pCnf = Res_SatProveUnsat( p->pAig, vFanins );
+            if ( p->pCnf == NULL )
+            {
+p->timeSatSat += clock() - clk;
+//                printf( " Sat\n" );
+//                printf( "-" );
+                continue;
+            }
+p->timeSatUnsat += clock() - clk;
+//            printf( "+" );
+
+            p->nProvedSets++;
+//            printf( " Unsat\n" );
+//            continue;
+//            printf( "Proved %d.\n", k );
+
+            // write it into a file
+//            Sto_ManDumpClauses( p->pCnf, "trace.cnf" );
+
+            // interpolate the problem if it was UNSAT
+clk = clock();
+            nFanins = Int_ManInterpolate( p->pMan, p->pCnf, 0, &puTruth );
+p->timeInt += clock() - clk;
+            if ( nFanins != Vec_PtrSize(vFanins) - 2 )
+                continue;
+            assert( puTruth );
+//            Extra_PrintBinary( stdout, puTruth, 1 << nFanins );  printf( "\n" );
+
+            // transform interpolant into the AIG
+            pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem );
+
+            // derive the AIG for the decomposition tree
+            pFunc = Kit_GraphToHop( pNtk->pManFunc, pGraph );
+            Kit_GraphFree( pGraph );
+
+            // update the network
+clk = clock();
+            Res_UpdateNetwork( pObj, Vec_VecEntry(p->vResubsW, k), pFunc, p->vLevels );
+p->timeUpd += clock() - clk;
+            break;
+        }
+//        printf( "\n" );
+    }
+    Extra_ProgressBarStop( pProgress );
+    Abc_NtkStopReverseLevels( pNtk );
+
+p->timeSatSim += p->pSim->timeSat;
+p->timeSatTotal = p->timeSatSat + p->timeSatUnsat + p->timeSatSim;
+
+    p->nTotalNets2 = Abc_NtkGetTotalFanins(pNtk);
+    p->nTotalNodes2 = Abc_NtkNodeNum(pNtk);
+
+    // quit resubstitution manager
+p->timeTotal = clock() - clkTotal;
+    Res_ManFree( p );
+
+s_ResynTime += clock() - clkTotal;
+    // check the resulting network
+    if ( !Abc_NtkCheck( pNtk ) )
+    {
+        fprintf( stdout, "Abc_NtkResynthesize(): Network check has failed.\n" );
+        return 0;
+    }
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/res/resDivs.c b/src/opt/res/resDivs.c
new file mode 100644
index 00000000..cc75b90f
--- /dev/null
+++ b/src/opt/res/resDivs.c
@@ -0,0 +1,285 @@
+/**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 "resInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Res_WinMarkTfi( 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 k, f, m;
+
+    // set the maximum level of the divisors
+    p->nLevDivMax = nLevDivMax;
+
+    // mark the TFI with the current trav ID
+    Abc_NtkIncrementTravId( p->pNode->pNtk );
+    Res_WinMarkTfi( p );
+
+    // mark with the current trav ID those nodes that should not be divisors:
+    // (1) the node and its TFO
+    // (2) the MFFC of the node
+    // (3) the node's fanins (these are treated as a special case)
+    Abc_NtkIncrementTravId( p->pNode->pNtk );
+    Res_WinSweepLeafTfo_rec( p->pNode, p->nLevDivMax );
+    Res_WinVisitMffc( p->pNode );
+    Abc_ObjForEachFanin( p->pNode, pObj, k )
+        Abc_NodeSetTravIdCurrent( pObj );
+
+    // at this point the nodes are marked with two trav IDs:
+    // nodes to be collected as divisors are marked with previous trav ID
+    // nodes to be avoided as divisors are marked with current trav ID
+
+    // start collecting the divisors
+    Vec_PtrClear( p->vDivs );
+    Vec_PtrForEachEntry( p->vLeaves, pObj, k )
+    {
+        assert( (int)pObj->Level >= p->nLevLeafMin ); 
+        if ( !Abc_NodeIsTravIdPrevious(pObj) )
+            continue;
+        if ( (int)pObj->Level > p->nLevDivMax )
+            continue;
+        Vec_PtrPush( p->vDivs, pObj );
+    }
+    // add the internal nodes to the data structure
+    Vec_PtrForEachEntry( p->vNodes, pObj, k )
+    {
+        if ( !Abc_NodeIsTravIdPrevious(pObj) )
+            continue;
+        if ( (int)pObj->Level > p->nLevDivMax )
+            continue;
+        Vec_PtrPush( p->vDivs, pObj );
+    }
+
+    // explore the fanouts of already collected divisors
+    p->nDivsPlus = 0;
+    Vec_PtrForEachEntry( p->vDivs, pObj, k )
+    {
+        // consider fanouts of this node
+        Abc_ObjForEachFanout( pObj, pFanout, f )
+        {
+            // stop if there are too many fanouts
+            if ( f > 20 )
+                break;
+            // skip nodes that are already added
+            if ( Abc_NodeIsTravIdPrevious(pFanout) )
+                continue;
+            // skip nodes in the TFO or in the MFFC of node
+            if ( Abc_NodeIsTravIdCurrent(pFanout) )
+                continue;
+            // skip COs
+            if ( !Abc_ObjIsNode(pFanout) ) 
+                continue;
+            // skip nodes with large level
+            if ( (int)pFanout->Level >= p->nLevDivMax )
+                continue;
+            // skip nodes whose fanins are not divisors
+            Abc_ObjForEachFanin( pFanout, pFanin, m )
+                if ( !Abc_NodeIsTravIdPrevious(pFanin) )
+                    break;
+            if ( m < Abc_ObjFaninNum(pFanout) )
+                continue;
+            // add the node to the divisors
+            Vec_PtrPush( p->vDivs, pFanout );
+            Vec_PtrPush( p->vNodes, pFanout );
+            Abc_NodeSetTravIdPrevious( pFanout );
+            p->nDivsPlus++;
+        }
+    }
+/*
+    printf( "Node level = %d.  ", Abc_ObjLevel(p->pNode) );
+    Vec_PtrForEachEntryStart( p->vDivs, pObj, k, Vec_PtrSize(p->vDivs)-p->nDivsPlus )
+        printf( "%d ", Abc_ObjLevel(pObj) );
+    printf( "\n" );
+*/
+//printf( "%d ", p->nDivsPlus );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFI cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinMarkTfi_rec( Res_Win_t * p, Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    if ( Abc_NodeIsTravIdCurrent(pObj) )
+        return;
+    Abc_NodeSetTravIdCurrent( pObj );
+    assert( Abc_ObjIsNode(pObj) );
+    // visit the fanins of the node
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        Res_WinMarkTfi_rec( p, pFanin );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFI cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinMarkTfi( Res_Win_t * p )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    // mark the leaves
+    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
+        Abc_NodeSetTravIdCurrent( pObj );
+    // start from the node
+    Res_WinMarkTfi_rec( p, p->pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFO of the collected nodes up to the given level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit )
+        return;
+    if ( Abc_NodeIsTravIdCurrent(pObj) )
+        return;
+    Abc_NodeSetTravIdCurrent( pObj );
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        Res_WinSweepLeafTfo_rec( pFanout, nLevelLimit );
+}
+
+/**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( Abc_Obj_t * pNode )
+{
+    int Count1, Count2;
+    assert( Abc_ObjIsNode(pNode) );
+    // dereference the node (mark with the current trav ID)
+    Count1 = Res_NodeDeref_rec( pNode );
+    // reference it back
+    Count2 = Res_NodeRef_rec( pNode );
+    assert( Count1 == Count2 );
+    return Count1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/res/resFilter.c b/src/opt/res/resFilter.c
new file mode 100644
index 00000000..f2ca41d3
--- /dev/null
+++ b/src/opt/res/resFilter.c
@@ -0,0 +1,434 @@
+/**CFile****************************************************************
+
+  FileName    [resFilter.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  Synopsis    [Filtering resubstitution candidates.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: resFilter.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "resInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim, unsigned uMask );
+static int        Res_FilterCriticalFanin( Abc_Obj_t * pNode );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Finds sets of feasible candidates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW, int nFaninsMax, int fArea )
+{
+    Abc_Obj_t * pFanin, * pFanin2, * pFaninTemp;
+    unsigned * pInfo, * pInfoDiv, * pInfoDiv2;
+    int Counter, RetValue, i, i2, d, d2, iDiv, iDiv2, k;
+
+    // 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!\n" );
+        return 0;
+    }
+
+    // collect the fanin info
+    pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~0 );
+    RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
+    if ( RetValue == 0 )
+    {
+//        printf( "Failed 2!\n" );
+        return 0;
+    }
+
+    // try removing each fanin
+//    printf( "Fanins: " );
+    Counter = 0;
+    Vec_VecClear( vResubs );
+    Vec_VecClear( vResubsW );
+    Abc_ObjForEachFanin( pWin->pNode, pFanin, i )
+    {
+        if ( fArea && Abc_ObjFanoutNum(pFanin) > 1 )
+            continue;
+        // get simulation info without this fanin
+        pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) );
+        RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
+        if ( RetValue )
+        {
+//            printf( "Node %4d. Candidate fanin %4d.\n", pWin->pNode->Id, pFanin->Id );
+            // collect the nodes
+            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
+            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
+            Abc_ObjForEachFanin( pWin->pNode, pFaninTemp, k )
+            {
+                if ( k != i )
+                {
+                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
+                    Vec_VecPush( vResubsW, Counter, pFaninTemp );
+                }
+            }
+            Counter++;
+            if ( Counter == Vec_VecSize(vResubs) )
+                return Counter;    
+        }
+    }
+
+    // try replacing each critical fanin by a non-critical fanin
+    Abc_ObjForEachFanin( pWin->pNode, pFanin, i )
+    {
+        if ( Abc_ObjFanoutNum(pFanin) > 1 )
+            continue;
+        // get simulation info without this fanin
+        pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) );
+        // go over the set of divisors
+        for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ )
+        {
+            pInfoDiv = Vec_PtrEntry( pSim->vOuts, d );
+            iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2);
+            if ( !Abc_InfoIsOrOne( pInfo, pInfoDiv, pSim->nWordsOut ) )
+                continue;
+            // collect the nodes
+            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
+            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
+            // collect the remaning fanins and the divisor
+            Abc_ObjForEachFanin( pWin->pNode, pFaninTemp, k )
+            {
+                if ( k != i )
+                {
+                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
+                    Vec_VecPush( vResubsW, Counter, pFaninTemp );
+                }
+            }
+            // collect the divisor
+            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) );
+            Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) );
+            Counter++;
+            if ( Counter == Vec_VecSize(vResubs) )
+                return Counter;           
+        }
+    }
+
+    // consider the case when two fanins can be added instead of one
+    if ( Abc_ObjFaninNum(pWin->pNode) < nFaninsMax )
+    {
+        // try to replace each critical fanin by two non-critical fanins
+        Abc_ObjForEachFanin( pWin->pNode, pFanin, i )
+        {
+            if ( Abc_ObjFanoutNum(pFanin) > 1 )
+                continue;
+            // get simulation info without this fanin
+            pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) );
+            // go over the set of divisors
+            for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ )
+            {
+                pInfoDiv = Vec_PtrEntry( pSim->vOuts, d );
+                iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2);
+                // go through the second divisor
+                for ( d2 = d + 1; d2 < Abc_NtkPoNum(pAig); d2++ )
+                {
+                    pInfoDiv2 = Vec_PtrEntry( pSim->vOuts, d2 );
+                    iDiv2 = d2 - (Abc_ObjFaninNum(pWin->pNode) + 2);
+                    if ( !Abc_InfoIsOrOne3( pInfo, pInfoDiv, pInfoDiv2, pSim->nWordsOut ) )
+                        continue;
+                    // collect the nodes
+                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
+                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
+                    // collect the remaning fanins and the divisor
+                    Abc_ObjForEachFanin( pWin->pNode, pFaninTemp, k )
+                    {
+                        if ( k != i )
+                        {
+                            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
+                            Vec_VecPush( vResubsW, Counter, pFaninTemp );
+                        }
+                    }
+                    // collect the divisor
+                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) );
+                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d2) );
+                    Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) );
+                    Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv2) );
+                    Counter++;
+                    if ( Counter == Vec_VecSize(vResubs) )
+                        return Counter;           
+                }
+            }
+        }
+    }
+
+    // try to replace two nets by one
+    if ( !fArea )
+    {
+        Abc_ObjForEachFanin( pWin->pNode, pFanin, i )
+        {
+            for ( i2 = i + 1; i2 < Abc_ObjFaninNum(pWin->pNode); i2++ )
+            {
+                pFanin2 = Abc_ObjFanin(pWin->pNode, i2);
+                // get simulation info without these fanins
+                pInfo = Res_FilterCollectFaninInfo( pWin, pSim, (~(1 << i)) & (~(1 << i2)) );
+                // go over the set of divisors
+                for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ )
+                {
+                    pInfoDiv = Vec_PtrEntry( pSim->vOuts, d );
+                    iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2);
+                    if ( !Abc_InfoIsOrOne( pInfo, pInfoDiv, pSim->nWordsOut ) )
+                        continue;
+                    // collect the nodes
+                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
+                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
+                    // collect the remaning fanins and the divisor
+                    Abc_ObjForEachFanin( pWin->pNode, pFaninTemp, k )
+                    {
+                        if ( k != i && k != i2 )
+                        {
+                            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
+                            Vec_VecPush( vResubsW, Counter, pFaninTemp );
+                        }
+                    }
+                    // collect the divisor
+                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) );
+                    Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) );
+                    Counter++;
+                    if ( Counter == Vec_VecSize(vResubs) )
+                        return Counter;           
+                }
+            }
+        }
+    }
+    return Counter;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Finds sets of feasible candidates.]
+
+  Description [This procedure is a special case of the above.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_FilterCandidatesArea( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW, int nFaninsMax )
+{
+    Abc_Obj_t * pFanin;
+    unsigned * pInfo, * pInfoDiv, * pInfoDiv2;
+    int Counter, RetValue, d, d2, k, iDiv, iDiv2, iBest;
+
+    // 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!\n" );
+        return 0;
+    }
+
+    // collect the fanin info
+    pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~0 );
+    RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
+    if ( RetValue == 0 )
+    {
+//        printf( "Failed 2!\n" );
+        return 0;
+    }
+
+    // try removing fanins
+//    printf( "Fanins: " );
+    Counter = 0;
+    Vec_VecClear( vResubs );
+    Vec_VecClear( vResubsW );
+    // get the best fanins
+    iBest = Res_FilterCriticalFanin( pWin->pNode );
+    if ( iBest == -1 )
+        return 0;
+
+    // get the info without the critical fanin
+    pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << iBest) );
+    RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
+    if ( RetValue )
+    {
+//        printf( "Can be done without one!\n" );
+        // collect the nodes
+        Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
+        Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
+        Abc_ObjForEachFanin( pWin->pNode, pFanin, k )
+        {
+            if ( k != iBest )
+            {
+                Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
+                Vec_VecPush( vResubsW, Counter, pFanin );
+            }
+        }
+        Counter++;
+//        printf( "*" );
+        return Counter;
+    }
+
+    // go through the divisors
+    for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ )
+    {
+        pInfoDiv = Vec_PtrEntry( pSim->vOuts, d );
+        iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2);
+        if ( !Abc_InfoIsOrOne( pInfo, pInfoDiv, pSim->nWordsOut ) )
+            continue;
+//if ( Abc_ObjLevel(pWin->pNode) <= Abc_ObjLevel( Vec_PtrEntry(pWin->vDivs, iDiv) ) )
+//    printf( "Node level = %d. Divisor level = %d.\n", Abc_ObjLevel(pWin->pNode), Abc_ObjLevel( Vec_PtrEntry(pWin->vDivs, iDiv) ) );
+        // collect the nodes
+        Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
+        Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
+        // collect the remaning fanins and the divisor
+        Abc_ObjForEachFanin( pWin->pNode, pFanin, k )
+        {
+            if ( k != iBest )
+            {
+                Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
+                Vec_VecPush( vResubsW, Counter, pFanin );
+            }
+        }
+        // collect the divisor
+        Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) );
+        Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) );
+        Counter++;
+
+        if ( Counter == Vec_VecSize(vResubs) )
+            break;            
+    }
+
+    if ( Counter > 0 || Abc_ObjFaninNum(pWin->pNode) >= nFaninsMax )
+        return Counter;
+
+    // try to find the node pairs
+    for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ )
+    {
+        pInfoDiv = Vec_PtrEntry( pSim->vOuts, d );
+        iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2);
+        // go through the second divisor
+        for ( d2 = d + 1; d2 < Abc_NtkPoNum(pAig); d2++ )
+        {
+            pInfoDiv2 = Vec_PtrEntry( pSim->vOuts, d2 );
+            iDiv2 = d2 - (Abc_ObjFaninNum(pWin->pNode) + 2);
+
+            if ( !Abc_InfoIsOrOne3( pInfo, pInfoDiv, pInfoDiv2, pSim->nWordsOut ) )
+                continue;
+            // collect the nodes
+            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
+            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
+            // collect the remaning fanins and the divisor
+            Abc_ObjForEachFanin( pWin->pNode, pFanin, k )
+            {
+                if ( k != iBest )
+                {
+                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
+                    Vec_VecPush( vResubsW, Counter, pFanin );
+                }
+            }
+            // collect the divisor
+            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) );
+            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d2) );
+            Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) );
+            Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv2) );
+            Counter++;
+
+            if ( Counter == Vec_VecSize(vResubs) )
+                break;            
+        }
+        if ( Counter == Vec_VecSize(vResubs) )
+            break;            
+    }
+    return Counter;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Finds sets of feasible candidates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim, unsigned uMask )
+{
+    Abc_Obj_t * pFanin;
+    unsigned * pInfo;
+    int i;
+    pInfo = Vec_PtrEntry( pSim->vOuts, 0 );
+    Abc_InfoClear( pInfo, pSim->nWordsOut );
+    Abc_ObjForEachFanin( pWin->pNode, pFanin, i )
+    {
+        if ( uMask & (1 << i) )
+            Abc_InfoOr( pInfo, Vec_PtrEntry(pSim->vOuts, 2+i), pSim->nWordsOut );
+    }
+    return pInfo;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the index of the most critical fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_FilterCriticalFanin( Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin;
+    int i, iBest = -1, CostMax = 0, CostCur;
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+    {
+        if ( !Abc_ObjIsNode(pFanin) )
+            continue;
+        if ( Abc_ObjFanoutNum(pFanin) > 1 )
+            continue;
+        CostCur = Res_WinVisitMffc( pFanin );
+        if ( CostMax < CostCur )
+        {
+            CostMax = CostCur;
+            iBest = i;
+        }
+    }
+//    if ( CostMax > 0 )
+//        printf( "<%d>", CostMax );
+    return iBest;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/res/resInt.h b/src/opt/res/resInt.h
new file mode 100644
index 00000000..5aae46cc
--- /dev/null
+++ b/src/opt/res/resInt.h
@@ -0,0 +1,137 @@
+/**CFile****************************************************************
+
+  FileName    [resInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: resInt.h,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __RES_INT_H__
+#define __RES_INT_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "res.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Res_Win_t_ Res_Win_t;
+struct Res_Win_t_
+{
+    // windowing parameters
+    Abc_Obj_t *      pNode;        // the node in the center
+    int              nWinTfiMax;   // the fanin levels
+    int              nWinTfoMax;   // the fanout levels
+    int              nLevDivMax;   // the maximum divisor level
+    // internal windowing parameters
+    int              nFanoutLimit; // the limit on the fanout count of a TFO node (if more, the node is treated as a root)
+    int              nLevTfiMinus; // the number of additional levels to search from TFO below the level of leaves
+    // derived windowing parameters
+    int              nLevLeafMin;  // the minimum level of a leaf
+    int              nLevTravMin;  // the minimum level to search from TFO
+    int              nDivsPlus;    // the number of additional divisors
+    // the window data
+    Vec_Ptr_t *      vRoots;       // outputs of the window
+    Vec_Ptr_t *      vLeaves;      // inputs of the window
+    Vec_Ptr_t *      vBranches;    // side nodes of the window
+    Vec_Ptr_t *      vNodes;       // internal nodes of the window
+    Vec_Ptr_t *      vDivs;        // candidate divisors of the node
+    // temporary data
+    Vec_Vec_t *      vMatrix;      // TFI nodes below the given node
+};
+
+typedef struct Res_Sim_t_ Res_Sim_t;
+struct Res_Sim_t_
+{
+    Abc_Ntk_t *      pAig;         // AIG for simulation
+    int              nTruePis;     // the number of true PIs of the window
+    int              fConst0;      // the node can be replaced by constant 0
+    int              fConst1;      // the node can be replaced by constant 0
+    // simulation parameters
+    int              nWords;       // the number of simulation words
+    int              nPats;        // the number of patterns
+    int              nWordsIn;     // the number of simulation words in the input patterns
+    int              nPatsIn;      // the number of patterns in the input patterns 
+    int              nBytesIn;     // the number of bytes in the input patterns
+    int              nWordsOut;    // the number of simulation words in the output patterns
+    int              nPatsOut;     // the number of patterns in the output patterns 
+    // simulation info
+    Vec_Ptr_t *      vPats;        // input simulation patterns
+    Vec_Ptr_t *      vPats0;       // input simulation patterns
+    Vec_Ptr_t *      vPats1;       // input simulation patterns
+    Vec_Ptr_t *      vOuts;        // output simulation info
+    int              nPats0;       // the number of 0-patterns accumulated
+    int              nPats1;       // the number of 1-patterns accumulated
+    // resub candidates
+    Vec_Vec_t *      vCands;       // resubstitution candidates
+    // statistics
+    int              timeSat;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== resDivs.c ==========================================================*/
+extern void          Res_WinDivisors( Res_Win_t * p, int nLevDivMax );
+extern void          Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit );
+extern int           Res_WinVisitMffc( Abc_Obj_t * pNode );
+/*=== resFilter.c ==========================================================*/
+extern int           Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW, int nFaninsMax, int fArea );
+extern int           Res_FilterCandidatesArea( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW, int nFaninsMax );
+/*=== resSat.c ==========================================================*/
+extern void *        Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins );
+extern int           Res_SatSimulate( Res_Sim_t * p, int nPats, int fOnSet );
+/*=== resSim.c ==========================================================*/
+extern Res_Sim_t *   Res_SimAlloc( int nWords );
+extern void          Res_SimFree( Res_Sim_t * p );
+extern int           Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig, int nTruePis, int fVerbose );
+/*=== 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, Vec_Vec_t * vLevels );
+/*=== resWnd.c ==========================================================*/
+extern Res_Win_t *   Res_WinAlloc();
+extern void          Res_WinFree( Res_Win_t * p );
+extern int           Res_WinIsTrivial( Res_Win_t * p );
+extern int           Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p );
+
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c
new file mode 100644
index 00000000..dd0e7a23
--- /dev/null
+++ b/src/opt/res/resSat.c
@@ -0,0 +1,407 @@
+/**CFile****************************************************************
+
+  FileName    [resSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  Synopsis    [Interface with the SAT solver.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: resSat.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "resInt.h"
+#include "hop.h"
+#include "satSolver.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern int Res_SatAddConst1( sat_solver * pSat, int iVar, int fCompl );
+extern int Res_SatAddEqual( sat_solver * pSat, int iVar0, int iVar1, int fCompl );
+extern int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Loads AIG into the SAT solver for checking resubstitution.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
+{
+    void * pCnf = NULL;
+    sat_solver * pSat;
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj;
+    int i, nNodes, status;
+
+    // make sure fanins contain POs of the AIG
+    pObj = Vec_PtrEntry( vFanins, 0 );
+    assert( pObj->pNtk == pAig && Abc_ObjIsPo(pObj) );
+
+    // collect reachable nodes
+    vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize );
+
+    // assign unique numbers to each node
+    nNodes = 0;
+    Abc_AigConst1(pAig)->pCopy = (void *)nNodes++;
+    Abc_NtkForEachPi( pAig, pObj, i )
+        pObj->pCopy = (void *)nNodes++;
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pCopy = (void *)nNodes++;
+    Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs
+        pObj->pCopy = (void *)nNodes++;
+
+    // start the solver
+    pSat = sat_solver_new();
+    sat_solver_store_alloc( pSat );
+
+    // add clause for the constant node
+    Res_SatAddConst1( pSat, (int)Abc_AigConst1(pAig)->pCopy, 0 );
+    // add clauses for AND gates
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        Res_SatAddAnd( pSat, (int)pObj->pCopy, 
+            (int)Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+    Vec_PtrFree( vNodes );
+    // add clauses for POs
+    Vec_PtrForEachEntry( vFanins, pObj, i )
+        Res_SatAddEqual( pSat, (int)pObj->pCopy, 
+            (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+    // add trivial clauses
+    pObj = Vec_PtrEntry(vFanins, 0);
+    Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // care-set
+    pObj = Vec_PtrEntry(vFanins, 1);
+    Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // on-set
+
+    // bookmark the clauses of A
+    sat_solver_store_mark_clauses_a( pSat );
+
+    // duplicate the clauses
+    pObj = Vec_PtrEntry(vFanins, 1);
+    Sat_SolverDoubleClauses( pSat, (int)pObj->pCopy );
+    // add the equality constraints
+    Vec_PtrForEachEntryStart( vFanins, pObj, i, 2 )
+        Res_SatAddEqual( pSat, (int)pObj->pCopy, ((int)pObj->pCopy) + nNodes, 0 );
+
+    // bookmark the roots
+    sat_solver_store_mark_roots( pSat );
+
+    // solve the problem
+    status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
+    if ( status == l_False )
+    {
+        pCnf = sat_solver_store_release( pSat );
+//        printf( "unsat\n" );
+    }
+    else if ( status == l_True )
+    {
+//        printf( "sat\n" );
+    }
+    else
+    {
+//        printf( "undef\n" );
+    }
+    sat_solver_delete( pSat );
+    return pCnf;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Loads AIG into the SAT solver for constrained simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, int fOnSet )
+{
+    sat_solver * pSat;
+    Vec_Ptr_t * vFanins;
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj;
+    int i, nNodes;
+
+    // start the array
+    vFanins = Vec_PtrAlloc( 2 );
+    pObj = Abc_NtkPo( pAig, 0 );
+    Vec_PtrPush( vFanins, pObj );
+    pObj = Abc_NtkPo( pAig, 1 );
+    Vec_PtrPush( vFanins, pObj );
+
+    // collect reachable nodes
+    vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize );
+
+    // assign unique numbers to each node
+    nNodes = 0;
+    Abc_AigConst1(pAig)->pCopy = (void *)nNodes++;
+    Abc_NtkForEachPi( pAig, pObj, i )
+        pObj->pCopy = (void *)nNodes++;
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pCopy = (void *)nNodes++;
+    Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs
+        pObj->pCopy = (void *)nNodes++;
+
+    // start the solver
+    pSat = sat_solver_new();
+
+    // add clause for the constant node
+    Res_SatAddConst1( pSat, (int)Abc_AigConst1(pAig)->pCopy, 0 );
+    // add clauses for AND gates
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        Res_SatAddAnd( pSat, (int)pObj->pCopy, 
+            (int)Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+    Vec_PtrFree( vNodes );
+    // add clauses for the first PO
+    pObj = Abc_NtkPo( pAig, 0 );
+    Res_SatAddEqual( pSat, (int)pObj->pCopy, 
+        (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+    // add clauses for the second PO
+    pObj = Abc_NtkPo( pAig, 1 );
+    Res_SatAddEqual( pSat, (int)pObj->pCopy, 
+        (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+
+    // add trivial clauses
+    pObj = Abc_NtkPo( pAig, 0 );
+    Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // care-set
+
+    pObj = Abc_NtkPo( pAig, 1 );
+    Res_SatAddConst1( pSat, (int)pObj->pCopy, !fOnSet ); // on-set
+
+    Vec_PtrFree( vFanins );
+    return pSat;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Loads AIG into the SAT solver for constrained simulation.]
+
+  Description [Returns 1 if the required number of patterns are found. 
+  Returns 0 if the solver ran out of time or proved a constant. 
+  In the latter, case one of the flags, fConst0 or fConst1, are set to 1.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
+{
+    Vec_Int_t * vLits;
+    Vec_Ptr_t * vPats;
+    sat_solver * pSat;
+    int RetValue, i, k, value, status, Lit, Var, iPat;
+    int clk = clock();
+
+//printf( "Looking for %s:  ", fOnSet? "onset " : "offset" );
+
+    // decide what problem should be solved
+    Lit = toLitCond( (int)Abc_NtkPo(p->pAig,1)->pCopy, !fOnSet );
+    if ( fOnSet )
+    {
+        iPat = p->nPats1;
+        vPats = p->vPats1;
+    }
+    else
+    {
+        iPat = p->nPats0;
+        vPats = p->vPats0;
+    }
+    assert( iPat < nPatsLimit );
+
+    // derive the SAT solver
+    pSat = Res_SatSimulateConstr( p->pAig, fOnSet );
+    pSat->fSkipSimplify = 1;
+    status = sat_solver_simplify( pSat );
+    if ( status == 0 )
+    {
+        if ( iPat == 0 )
+        {
+//            if ( fOnSet )
+//                p->fConst0 = 1;
+//            else
+//                p->fConst1 = 1;
+            RetValue = 0;
+        }
+        goto finish;
+    }
+ 
+    // enumerate through the SAT assignments
+    RetValue = 1;
+    vLits = Vec_IntAlloc( 32 );
+    for ( k = iPat; k < nPatsLimit; k++ )
+    {
+        // solve with the assumption
+//        status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
+        status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
+        if ( status == l_False )
+        {
+//printf( "Const %d\n", !fOnSet );
+            if ( k == 0 )
+            {
+                if ( fOnSet )
+                    p->fConst0 = 1;
+                else
+                    p->fConst1 = 1;
+                RetValue = 0;
+            }
+            break;
+        }
+        else if ( status == l_True )
+        {
+            // save the pattern
+            Vec_IntClear( vLits );
+            for ( i = 0; i < p->nTruePis; i++ )
+            {
+                Var = (int)Abc_NtkPi(p->pAig,i)->pCopy;
+                value = (int)(pSat->model.ptr[Var] == l_True);
+                if ( value )
+                    Abc_InfoSetBit( Vec_PtrEntry(vPats, i), k );
+                Lit = toLitCond( Var, value );
+                Vec_IntPush( vLits, Lit );
+//                printf( "%d", value );
+            }
+//            printf( "\n" );
+
+            status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+            if ( status == 0 )
+            {
+                k++;
+                RetValue = 1; 
+                break;
+            }
+        }
+        else
+        {
+//printf( "Undecided\n" );
+            if ( k == 0 )
+                RetValue = 0;
+            else
+                RetValue = 1; 
+            break;
+        }
+    }
+    Vec_IntFree( vLits );
+//printf( "Found %d patterns\n", k - iPat );
+
+    // set the new number of patterns
+    if ( fOnSet )
+        p->nPats1 = k;
+    else
+        p->nPats0 = k;
+
+finish:
+
+    sat_solver_delete( pSat );
+p->timeSat += clock() - clk;
+    return RetValue;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Asserts equality of the variable to a constant.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_SatAddConst1( sat_solver * pSat, int iVar, int fCompl )
+{
+    lit Lit = toLitCond( iVar, fCompl );
+    if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) )
+        return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Asserts equality of two variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_SatAddEqual( sat_solver * pSat, int iVar0, int iVar1, int fCompl )
+{
+    lit Lits[2];
+
+    Lits[0] = toLitCond( iVar0, 0 );
+    Lits[1] = toLitCond( iVar1, !fCompl );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+        return 0;
+
+    Lits[0] = toLitCond( iVar0, 1 );
+    Lits[1] = toLitCond( iVar1, fCompl );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+        return 0;
+
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds constraints for the two-input AND-gate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 )
+{
+    lit Lits[3];
+
+    Lits[0] = toLitCond( iVar, 1 );
+    Lits[1] = toLitCond( iVar0, fCompl0 );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+        return 0;
+
+    Lits[0] = toLitCond( iVar, 1 );
+    Lits[1] = toLitCond( iVar1, fCompl1 );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+        return 0;
+
+    Lits[0] = toLitCond( iVar, 0 );
+    Lits[1] = toLitCond( iVar0, !fCompl0 );
+    Lits[2] = toLitCond( iVar1, !fCompl1 );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
+        return 0;
+
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/res/resSim.c b/src/opt/res/resSim.c
new file mode 100644
index 00000000..5c1dd2b6
--- /dev/null
+++ b/src/opt/res/resSim.c
@@ -0,0 +1,790 @@
+/**CFile****************************************************************
+
+  FileName    [resSim.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  Synopsis    [Simulation engine.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: resSim.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "resInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocate simulation engine.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+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 parameters
+    p->nWords    = nWords;
+    p->nPats     = p->nWords * 8 * sizeof(unsigned);
+    p->nWordsIn  = p->nPats;
+    p->nBytesIn  = p->nPats * sizeof(unsigned);
+    p->nPatsIn   = p->nPats * 8 * sizeof(unsigned);
+    p->nWordsOut = p->nPats * p->nWords;
+    p->nPatsOut  = p->nPats * p->nPats;
+    // simulation info
+    p->vPats     = Vec_PtrAllocSimInfo( 1024, p->nWordsIn );
+    p->vPats0    = Vec_PtrAllocSimInfo( 128, p->nWords );
+    p->vPats1    = Vec_PtrAllocSimInfo( 128, p->nWords );
+    p->vOuts     = Vec_PtrAllocSimInfo( 128, p->nWordsOut );
+    // resub candidates
+    p->vCands    = Vec_VecStart( 16 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocate simulation engine.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimAdjust( Res_Sim_t * p, Abc_Ntk_t * pAig, int nTruePis )
+{
+    srand( 0xABC );
+
+    assert( Abc_NtkIsStrash(pAig) );
+    p->pAig = pAig;
+    p->nTruePis = nTruePis;
+    if ( Vec_PtrSize(p->vPats) < Abc_NtkObjNumMax(pAig)+1 )
+    {
+        Vec_PtrFree( p->vPats );
+        p->vPats = Vec_PtrAllocSimInfo( Abc_NtkObjNumMax(pAig)+1, p->nWordsIn );
+    }
+    if ( Vec_PtrSize(p->vPats0) < nTruePis )
+    {
+        Vec_PtrFree( p->vPats0 );
+        p->vPats0 = Vec_PtrAllocSimInfo( nTruePis, p->nWords );
+    }
+    if ( Vec_PtrSize(p->vPats1) < nTruePis )
+    {
+        Vec_PtrFree( p->vPats1 );
+        p->vPats1 = Vec_PtrAllocSimInfo( nTruePis, p->nWords );
+    }
+    if ( Vec_PtrSize(p->vOuts) < Abc_NtkPoNum(pAig) )
+    {
+        Vec_PtrFree( p->vOuts );
+        p->vOuts = Vec_PtrAllocSimInfo( Abc_NtkPoNum(pAig), p->nWordsOut );
+    }
+    // clean storage info for patterns
+    Abc_InfoClear( Vec_PtrEntry(p->vPats0,0), p->nWords * nTruePis );
+    Abc_InfoClear( Vec_PtrEntry(p->vPats1,0), p->nWords * nTruePis );
+    p->nPats0 = 0;
+    p->nPats1 = 0;
+    p->fConst0 = 0;
+    p->fConst1 = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Free simulation engine.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimFree( Res_Sim_t * p )
+{
+    Vec_PtrFree( p->vPats );
+    Vec_PtrFree( p->vPats0 );
+    Vec_PtrFree( p->vPats1 );
+    Vec_PtrFree( p->vOuts );
+    Vec_VecFree( p->vCands );
+    free( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Sets random PI simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_InfoRandomBytes( unsigned * p, int nWords ) 
+{ 
+    int i, Num; 
+    for ( i = nWords - 1; i >= 0; i-- ) 
+    { 
+        Num = rand(); 
+        p[i] = (Num & 1)? 0xff : 0;
+        p[i] = (p[i] << 8) | ((Num & 2)? 0xff : 0);
+        p[i] = (p[i] << 8) | ((Num & 4)? 0xff : 0);
+        p[i] = (p[i] << 8) | ((Num & 8)? 0xff : 0);
+    } 
+//    Extra_PrintBinary( stdout, p, 32 ); printf( "\n" );
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Sets random PI simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimSetRandomBytes( Res_Sim_t * p )
+{
+    Abc_Obj_t * pObj;
+    unsigned * pInfo;
+    int i;
+    Abc_NtkForEachPi( p->pAig, pObj, i )
+    {
+        pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+        if ( i < p->nTruePis )
+            Abc_InfoRandomBytes( pInfo, p->nWordsIn );
+        else
+            Abc_InfoRandom( pInfo, p->nWordsIn );
+    }
+/*
+    // double-check that all are byte-patterns
+    Abc_NtkForEachPi( p->pAig, pObj, i )
+    {
+        if ( i == p->nTruePis )
+            break;
+        pInfoC = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+        for ( k = 0; k < p->nBytesIn; k++ )
+            assert( pInfoC[k] == 0 || pInfoC[k] == 0xff );
+    }
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets random PI simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimSetDerivedBytes( Res_Sim_t * p, int fUseWalk )
+{
+    Vec_Ptr_t * vPatsSource[2];
+    int nPatsSource[2];
+    Abc_Obj_t * pObj;
+    unsigned char * pInfo;
+    int i, k, z, s, nPats;
+
+    // set several random patterns
+    assert( p->nBytesIn % 32 == 0 );
+    nPats = p->nBytesIn/8;
+    Abc_NtkForEachPi( p->pAig, pObj, i )
+    {
+        if ( i == p->nTruePis )
+            break;
+        Abc_InfoRandomBytes( Vec_PtrEntry(p->vPats, pObj->Id), nPats/4 );
+    }
+
+    // set special patterns
+    if ( fUseWalk )
+    {
+        for ( z = 0; z < 2; z++ )
+        {
+            // set the zero pattern
+            Abc_NtkForEachPi( p->pAig, pObj, i )
+            {
+                if ( i == p->nTruePis )
+                    break;
+                pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+                pInfo[nPats] = z ? 0xff : 0;
+            }
+            if ( ++nPats == p->nBytesIn )
+                return;
+            // set the walking zero pattern
+            for ( k = 0; k < p->nTruePis; k++ )
+            {
+                Abc_NtkForEachPi( p->pAig, pObj, i )
+                {
+                    if ( i == p->nTruePis )
+                        break;
+                    pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+                    pInfo[nPats] = ((i == k) ^ z) ? 0xff : 0;
+                }
+                if ( ++nPats == p->nBytesIn )
+                    return;
+            }
+        }
+    }
+
+    // decide what patterns to set first
+    if ( p->nPats0 < p->nPats1 )
+    {
+        nPatsSource[0] = p->nPats0;
+        vPatsSource[0] = p->vPats0;
+        nPatsSource[1] = p->nPats1;
+        vPatsSource[1] = p->vPats1;
+    }
+    else
+    {
+        nPatsSource[0] = p->nPats1;
+        vPatsSource[0] = p->vPats1;
+        nPatsSource[1] = p->nPats0;
+        vPatsSource[1] = p->vPats0;
+    }
+    for ( z = 0; z < 2; z++ )
+    {
+        for ( s = nPatsSource[z] - 1; s >= 0; s-- )
+        {
+//            if ( s == 0 )
+//            printf( "Patterns:\n" );
+            // set the given source pattern
+            for ( k = 0; k < p->nTruePis; k++ )
+            {
+                Abc_NtkForEachPi( p->pAig, pObj, i )
+                {
+                    if ( i == p->nTruePis )
+                        break;
+                    pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+                    if ( (i == k) ^ Abc_InfoHasBit( Vec_PtrEntry(vPatsSource[z], i), s ) )
+                    {
+                        pInfo[nPats] = 0xff;
+//                        if ( s == 0 )
+//                        printf( "1" );
+                    }
+                    else
+                    {
+                        pInfo[nPats] = 0;
+//                        if ( s == 0 )
+//                        printf( "0" );
+                    }
+                }
+//                if ( s == 0 )
+//                printf( "\n" );
+                if ( ++nPats == p->nBytesIn )
+                    return;
+            }
+        }
+    }
+    // clean the rest
+    for ( z = nPats; z < p->nBytesIn; z++ )
+    {
+        Abc_NtkForEachPi( p->pAig, pObj, i )
+        {
+            if ( i == p->nTruePis )
+                break;
+            pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+            memset( pInfo + nPats, 0, p->nBytesIn - nPats );
+        }
+    }
+/*
+    // double-check that all are byte-patterns
+    Abc_NtkForEachPi( p->pAig, pObj, i )
+    {
+        if ( i == p->nTruePis )
+            break;
+        pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+        for ( k = 0; k < p->nBytesIn; k++ )
+            assert( pInfo[k] == 0 || pInfo[k] == 0xff );
+    }
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets given PI simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimSetGiven( Res_Sim_t * p, Vec_Ptr_t * vInfo )
+{
+    Abc_Obj_t * pObj;
+    unsigned * pInfo, * pInfo2;
+    int i, w;
+    Abc_NtkForEachPi( p->pAig, pObj, i )
+    {
+        if ( i == p->nTruePis )
+            break;
+        pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+        pInfo2 = Vec_PtrEntry( vInfo, i );
+        for ( w = 0; w < p->nWords; w++ )
+            pInfo[w] = pInfo2[w];
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimPerformOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords )
+{
+    unsigned * pInfo, * pInfo1, * pInfo2;
+    int k, fComp1, fComp2;
+    // simulate the internal nodes
+    assert( Abc_ObjIsNode(pNode) );
+    pInfo  = Vec_PtrEntry(vSimInfo, pNode->Id);
+    pInfo1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
+    pInfo2 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId1(pNode));
+    fComp1 = Abc_ObjFaninC0(pNode);
+    fComp2 = Abc_ObjFaninC1(pNode);
+    if ( fComp1 && fComp2 )
+        for ( k = 0; k < nSimWords; k++ )
+            pInfo[k] = ~pInfo1[k] & ~pInfo2[k];
+    else if ( fComp1 && !fComp2 )
+        for ( k = 0; k < nSimWords; k++ )
+            pInfo[k] = ~pInfo1[k] &  pInfo2[k];
+    else if ( !fComp1 && fComp2 )
+        for ( k = 0; k < nSimWords; k++ )
+            pInfo[k] =  pInfo1[k] & ~pInfo2[k];
+    else // if ( fComp1 && fComp2 )
+        for ( k = 0; k < nSimWords; k++ )
+            pInfo[k] =  pInfo1[k] &  pInfo2[k];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one CO node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimTransferOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords )
+{
+    unsigned * pInfo, * pInfo1;
+    int k, fComp1;
+    // simulate the internal nodes
+    assert( Abc_ObjIsCo(pNode) );
+    pInfo  = Vec_PtrEntry(vSimInfo, pNode->Id);
+    pInfo1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
+    fComp1 = Abc_ObjFaninC0(pNode);
+    if ( fComp1 )
+        for ( k = 0; k < nSimWords; k++ )
+            pInfo[k] = ~pInfo1[k];
+    else 
+        for ( k = 0; k < nSimWords; k++ )
+            pInfo[k] =  pInfo1[k];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one round of simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimPerformRound( Res_Sim_t * p, int nWords )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Abc_InfoFill( Vec_PtrEntry(p->vPats,0), nWords );
+    Abc_AigForEachAnd( p->pAig, pObj, i )
+        Res_SimPerformOne( pObj, p->vPats, nWords );
+    Abc_NtkForEachPo( p->pAig, pObj, i )
+        Res_SimTransferOne( pObj, p->vPats, nWords );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Pads the extra space with duplicated simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimPadSimInfo( Vec_Ptr_t * vPats, int nPats, int nWords )
+{
+    unsigned * pInfo;
+    int i, w, iWords;
+    assert( nPats > 0 && nPats < nWords * 8 * (int) sizeof(unsigned) );
+    // pad the first word
+    if ( nPats < 8 * sizeof(unsigned) )
+    {
+        Vec_PtrForEachEntry( vPats, pInfo, i )
+            if ( pInfo[0] & 1 )
+                pInfo[0] |= ((~0) << nPats);
+        nPats = 8 * sizeof(unsigned);
+    }
+    // pad the empty words
+    iWords = nPats / (8 * sizeof(unsigned));
+    Vec_PtrForEachEntry( vPats, pInfo, i )
+    {
+        for ( w = iWords; w < nWords; w++ )
+            pInfo[w] = pInfo[0];
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the simulation info to fill the space.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimDeriveInfoReplicate( Res_Sim_t * p )
+{
+    unsigned * pInfo, * pInfo2;
+    Abc_Obj_t * pObj;
+    int i, j, w;
+    Abc_NtkForEachPo( p->pAig, pObj, i )
+    {
+        pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+        pInfo2 = Vec_PtrEntry( p->vOuts, i );
+        for ( j = 0; j < p->nPats; j++ )
+            for ( w = 0; w < p->nWords; w++ )
+                *pInfo2++ = pInfo[w];
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Complement the simulation info if necessary.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimDeriveInfoComplement( Res_Sim_t * p )
+{
+    unsigned * pInfo, * pInfo2;
+    Abc_Obj_t * pObj;
+    int i, j, w;
+    Abc_NtkForEachPo( p->pAig, pObj, i )
+    {
+        pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+        pInfo2 = Vec_PtrEntry( p->vOuts, i );
+        for ( j = 0; j < p->nPats; j++, pInfo2 += p->nWords )
+            if ( Abc_InfoHasBit( pInfo, j ) )
+                for ( w = 0; w < p->nWords; w++ )
+                    pInfo2[w] = ~pInfo2[w];
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints output patterns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimPrintOutPatterns( Res_Sim_t * p, Abc_Ntk_t * pAig )
+{
+    Abc_Obj_t * pObj;
+    unsigned * pInfo2;
+    int i;
+    Abc_NtkForEachPo( pAig, pObj, i )
+    {
+        pInfo2 = Vec_PtrEntry( p->vOuts, i );
+        Extra_PrintBinary( stdout, pInfo2, p->nPatsOut );
+        printf( "\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints output patterns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimPrintNodePatterns( Res_Sim_t * p, Abc_Ntk_t * pAig )
+{
+    unsigned * pInfo;
+    pInfo = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
+    Extra_PrintBinary( stdout, pInfo, p->nPats );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of patters of different type.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimCountResults( Res_Sim_t * p, int * pnDcs, int * pnOnes, int * pnZeros, int fVerbose )
+{
+    unsigned char * pInfoCare, * pInfoNode;
+    int i, nTotal = 0;
+    pInfoCare = (unsigned char *)Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
+    pInfoNode = (unsigned char *)Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
+    for ( i = 0; i < p->nBytesIn; i++ )
+    {
+        if ( !pInfoCare[i] )
+            (*pnDcs)++;
+        else if ( !pInfoNode[i] )
+            (*pnZeros)++;
+        else
+            (*pnOnes)++;
+    }
+    nTotal += *pnDcs;
+    nTotal += *pnZeros;
+    nTotal += *pnOnes;
+    if ( fVerbose )
+    {
+        printf( "Dc = %7.2f %%  ",  100.0*(*pnDcs)  /nTotal );
+        printf( "On = %7.2f %%  ",  100.0*(*pnOnes) /nTotal );
+        printf( "Off = %7.2f %%  ", 100.0*(*pnZeros)/nTotal );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of patters of different type.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimCollectPatterns( Res_Sim_t * p, int fVerbose )
+{
+    Abc_Obj_t * pObj;
+    unsigned char * pInfoCare, * pInfoNode, * pInfo;
+    int i, j;
+    pInfoCare = (unsigned char *)Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
+    pInfoNode = (unsigned char *)Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
+    for ( i = 0; i < p->nBytesIn; i++ )
+    {
+        // skip don't-care patterns
+        if ( !pInfoCare[i] )
+            continue;
+        // separate offset and onset patterns
+        assert( pInfoNode[i] == 0 || pInfoNode[i] == 0xff );
+        if ( !pInfoNode[i] )
+        {
+            if ( p->nPats0 >= p->nPats )
+                continue;
+            Abc_NtkForEachPi( p->pAig, pObj, j )
+            {
+                if ( j == p->nTruePis )
+                    break;
+                pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+                assert( pInfo[i] == 0 || pInfo[i] == 0xff );
+                if ( pInfo[i] )
+                    Abc_InfoSetBit( Vec_PtrEntry(p->vPats0, j), p->nPats0 );
+            }
+            p->nPats0++;
+        }
+        else
+        {
+            if ( p->nPats1 >= p->nPats )
+                continue;
+            Abc_NtkForEachPi( p->pAig, pObj, j )
+            {
+                if ( j == p->nTruePis )
+                    break;
+                pInfo = (unsigned char *)Vec_PtrEntry( p->vPats, pObj->Id );
+                assert( pInfo[i] == 0 || pInfo[i] == 0xff );
+                if ( pInfo[i] )
+                    Abc_InfoSetBit( Vec_PtrEntry(p->vPats1, j), p->nPats1 );
+            }
+            p->nPats1++;
+        }
+        if ( p->nPats0 >= p->nPats && p->nPats1 >= p->nPats )
+            break;
+    }
+    if ( fVerbose )
+    {
+        printf( "|  " );
+        printf( "On = %3d  ", p->nPats1 );
+        printf( "Off = %3d  ", p->nPats0 );
+        printf( "\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies the last pattern.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_SimVerifyValue( Res_Sim_t * p, int fOnSet )
+{
+    Abc_Obj_t * pObj;
+    unsigned * pInfo, * pInfo2;
+    int i, value;
+    Abc_NtkForEachPi( p->pAig, pObj, i )
+    {
+        if ( i == p->nTruePis )
+            break;
+        if ( fOnSet )
+        {
+            pInfo2 = Vec_PtrEntry( p->vPats1, i );
+            value = Abc_InfoHasBit( pInfo2, p->nPats1 - 1 );
+        }
+        else
+        {
+            pInfo2 = Vec_PtrEntry( p->vPats0, i );
+            value = Abc_InfoHasBit( pInfo2, p->nPats0 - 1 );
+        }
+        pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+        pInfo[0] = value ? ~0 : 0;
+    }
+    Res_SimPerformRound( p, 1 );
+    pObj = Abc_NtkPo( p->pAig, 1 );
+    pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+    assert( pInfo[0] == 0 || pInfo[0] == ~0 );
+    return pInfo[0] > 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares simulation info for candidate filtering.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig, int nTruePis, int fVerbose )
+{
+    int i, nOnes = 0, nZeros = 0, nDcs = 0;
+    if ( fVerbose )
+        printf( "\n" );
+    // prepare the manager
+    Res_SimAdjust( p, pAig, nTruePis );
+    // estimate the number of patterns
+    Res_SimSetRandomBytes( p );
+    Res_SimPerformRound( p, p->nWordsIn );
+    Res_SimCountResults( p, &nDcs, &nOnes, &nZeros, fVerbose );
+    // collect the patterns
+    Res_SimCollectPatterns( p, fVerbose );
+    // add more patterns using constraint simulation
+    if ( p->nPats0 < 8 )
+    {
+        if ( !Res_SatSimulate( p, 16, 0 ) )
+            return p->fConst0 || p->fConst1;
+//            return 0;
+//        printf( "Value0 = %d\n", Res_SimVerifyValue( p, 0 ) );
+    }
+    if ( p->nPats1 < 8 )
+    {
+        if ( !Res_SatSimulate( p, 16, 1 ) )
+            return p->fConst0 || p->fConst1;
+//            return 0;
+//        printf( "Value1 = %d\n", Res_SimVerifyValue( p, 1 ) );
+    }
+    // generate additional patterns
+    for ( i = 0; i < 2; i++ )
+    {
+        if ( p->nPats0 > p->nPats*7/8 && p->nPats1 > p->nPats*7/8 )
+            break;
+        Res_SimSetDerivedBytes( p, i==0 );
+        Res_SimPerformRound( p, p->nWordsIn );
+        Res_SimCountResults( p, &nDcs, &nOnes, &nZeros, fVerbose );
+        Res_SimCollectPatterns( p, fVerbose );
+    }
+    // create bit-matrix info
+    if ( p->nPats0 < p->nPats )
+        Res_SimPadSimInfo( p->vPats0, p->nPats0, p->nWords );
+    if ( p->nPats1 < p->nPats )
+        Res_SimPadSimInfo( p->vPats1, p->nPats1, p->nWords );
+    // resimulate 0-patterns
+    Res_SimSetGiven( p, p->vPats0 );
+    Res_SimPerformRound( p, p->nWords );
+//Res_SimPrintNodePatterns( p, pAig );
+    Res_SimDeriveInfoReplicate( p );
+    // resimulate 1-patterns
+    Res_SimSetGiven( p, p->vPats1 );
+    Res_SimPerformRound( p, p->nWords );
+//Res_SimPrintNodePatterns( p, pAig );
+    Res_SimDeriveInfoComplement( p );
+    // print output patterns
+//    Res_SimPrintOutPatterns( p, pAig );
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/res/resSim_old.c b/src/opt/res/resSim_old.c
new file mode 100644
index 00000000..23ce29e4
--- /dev/null
+++ b/src/opt/res/resSim_old.c
@@ -0,0 +1,521 @@
+/**CFile****************************************************************
+
+  FileName    [resSim.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  Synopsis    [Simulation engine.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: resSim.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "resInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocate simulation engine.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+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 parameters
+    p->nWords    = nWords;
+    p->nPats     = 8 * sizeof(unsigned) * p->nWords;
+    p->nWordsOut = p->nPats * p->nWords;
+    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->vCands    = Vec_VecStart( 16 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocate simulation engine.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimAdjust( Res_Sim_t * p, Abc_Ntk_t * pAig )
+{
+    srand( 0xABC );
+
+    assert( Abc_NtkIsStrash(pAig) );
+    p->pAig = pAig;
+    if ( Vec_PtrSize(p->vPats) < Abc_NtkObjNumMax(pAig)+1 )
+    {
+        Vec_PtrFree( p->vPats );
+        p->vPats = Vec_PtrAllocSimInfo( Abc_NtkObjNumMax(pAig)+1, p->nWords );
+    }
+    if ( Vec_PtrSize(p->vPats0) < Abc_NtkPiNum(pAig) )
+    {
+        Vec_PtrFree( p->vPats0 );
+        p->vPats0 = Vec_PtrAllocSimInfo( Abc_NtkPiNum(pAig), p->nWords );
+    }
+    if ( Vec_PtrSize(p->vPats1) < Abc_NtkPiNum(pAig) )
+    {
+        Vec_PtrFree( p->vPats1 );
+        p->vPats1 = Vec_PtrAllocSimInfo( Abc_NtkPiNum(pAig), p->nWords );
+    }
+    if ( Vec_PtrSize(p->vOuts) < Abc_NtkPoNum(pAig) )
+    {
+        Vec_PtrFree( p->vOuts );
+        p->vOuts = Vec_PtrAllocSimInfo( Abc_NtkPoNum(pAig), p->nWordsOut );
+    }
+    // clean storage info for patterns
+    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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Free simulation engine.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimFree( Res_Sim_t * p )
+{
+    Vec_PtrFree( p->vPats );
+    Vec_PtrFree( p->vPats0 );
+    Vec_PtrFree( p->vPats1 );
+    Vec_PtrFree( p->vOuts );
+    Vec_VecFree( p->vCands );
+    free( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Sets random PI simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimSetRandom( Res_Sim_t * p )
+{
+    Abc_Obj_t * pObj;
+    unsigned * pInfo;
+    int i;
+    Abc_NtkForEachPi( p->pAig, pObj, i )
+    {
+        pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+        Abc_InfoRandom( pInfo, p->nWords );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets given PI simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimSetGiven( Res_Sim_t * p, Vec_Ptr_t * vInfo )
+{
+    Abc_Obj_t * pObj;
+    unsigned * pInfo, * pInfo2;
+    int i, w;
+    Abc_NtkForEachPi( p->pAig, pObj, i )
+    {
+        pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+        pInfo2 = Vec_PtrEntry( vInfo, i );
+        for ( w = 0; w < p->nWords; w++ )
+            pInfo[w] = pInfo2[w];
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimPerformOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords )
+{
+    unsigned * pInfo, * pInfo1, * pInfo2;
+    int k, fComp1, fComp2;
+    // simulate the internal nodes
+    assert( Abc_ObjIsNode(pNode) );
+    pInfo  = Vec_PtrEntry(vSimInfo, pNode->Id);
+    pInfo1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
+    pInfo2 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId1(pNode));
+    fComp1 = Abc_ObjFaninC0(pNode);
+    fComp2 = Abc_ObjFaninC1(pNode);
+    if ( fComp1 && fComp2 )
+        for ( k = 0; k < nSimWords; k++ )
+            pInfo[k] = ~pInfo1[k] & ~pInfo2[k];
+    else if ( fComp1 && !fComp2 )
+        for ( k = 0; k < nSimWords; k++ )
+            pInfo[k] = ~pInfo1[k] &  pInfo2[k];
+    else if ( !fComp1 && fComp2 )
+        for ( k = 0; k < nSimWords; k++ )
+            pInfo[k] =  pInfo1[k] & ~pInfo2[k];
+    else // if ( fComp1 && fComp2 )
+        for ( k = 0; k < nSimWords; k++ )
+            pInfo[k] =  pInfo1[k] &  pInfo2[k];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one CO node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimTransferOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords )
+{
+    unsigned * pInfo, * pInfo1;
+    int k, fComp1;
+    // simulate the internal nodes
+    assert( Abc_ObjIsCo(pNode) );
+    pInfo  = Vec_PtrEntry(vSimInfo, pNode->Id);
+    pInfo1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
+    fComp1 = Abc_ObjFaninC0(pNode);
+    if ( fComp1 )
+        for ( k = 0; k < nSimWords; k++ )
+            pInfo[k] = ~pInfo1[k];
+    else 
+        for ( k = 0; k < nSimWords; k++ )
+            pInfo[k] =  pInfo1[k];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one round of simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimPerformRound( Res_Sim_t * p )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Abc_InfoFill( Vec_PtrEntry(p->vPats,0), p->nWords );
+    Abc_AigForEachAnd( p->pAig, pObj, i )
+        Res_SimPerformOne( pObj, p->vPats, p->nWords );
+    Abc_NtkForEachPo( p->pAig, pObj, i )
+        Res_SimTransferOne( pObj, p->vPats, p->nWords );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Processes simulation patterns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimProcessPats( Res_Sim_t * p )
+{
+    Abc_Obj_t * pObj;
+    unsigned * pInfoCare, * pInfoNode;
+    int i, j, nDcs = 0;
+    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) )
+        {
+            nDcs++;
+            continue;
+        }
+        // separate offset and onset patterns
+        if ( !Abc_InfoHasBit(pInfoNode, i) )
+        {
+            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 )
+                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    [Pads the extra space with duplicated simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimPadSimInfo( Vec_Ptr_t * vPats, int nPats, int nWords )
+{
+    unsigned * pInfo;
+    int i, w, iWords;
+    assert( nPats > 0 && nPats < nWords * 8 * (int) sizeof(unsigned) );
+    // pad the first word
+    if ( nPats < 8 * sizeof(unsigned) )
+    {
+        Vec_PtrForEachEntry( vPats, pInfo, i )
+            if ( pInfo[0] & 1 )
+                pInfo[0] |= ((~0) << nPats);
+        nPats = 8 * sizeof(unsigned);
+    }
+    // pad the empty words
+    iWords = nPats / (8 * sizeof(unsigned));
+    Vec_PtrForEachEntry( vPats, pInfo, i )
+    {
+        for ( w = iWords; w < nWords; w++ )
+            pInfo[w] = pInfo[0];
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the simulation info to fill the space.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimDeriveInfoReplicate( Res_Sim_t * p )
+{
+    unsigned * pInfo, * pInfo2;
+    Abc_Obj_t * pObj;
+    int i, j, w;
+    Abc_NtkForEachPo( p->pAig, pObj, i )
+    {
+        pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+        pInfo2 = Vec_PtrEntry( p->vOuts, i );
+        for ( j = 0; j < p->nPats; j++ )
+            for ( w = 0; w < p->nWords; w++ )
+                *pInfo2++ = pInfo[w];
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Complement the simulation info if necessary.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimDeriveInfoComplement( Res_Sim_t * p )
+{
+    unsigned * pInfo, * pInfo2;
+    Abc_Obj_t * pObj;
+    int i, j, w;
+    Abc_NtkForEachPo( p->pAig, pObj, i )
+    {
+        pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+        pInfo2 = Vec_PtrEntry( p->vOuts, i );
+        for ( j = 0; j < p->nPats; j++, pInfo2 += p->nWords )
+            if ( Abc_InfoHasBit( pInfo, j ) )
+                for ( w = 0; w < p->nWords; w++ )
+                    pInfo2[w] = ~pInfo2[w];
+    }
+}
+
+/**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( "On = %3d (%7.2f %%)  ",  nOnes,  100.0*nOnes/p->nPats );
+    printf( "Off = %3d (%7.2f %%)  ", nZeros, 100.0*nZeros/p->nPats );
+    printf( "Dc = %3d (%7.2f %%)  ",  nDcs,   100.0*nDcs/p->nPats );
+    printf( "P0 = %3d ", p->nPats0 );
+    printf( "P1 = %3d ", p->nPats1 );
+    if ( p->nPats0 < 4 || p->nPats1 < 4 )
+        printf( "*" );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints output patterns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimPrintOutPatterns( Res_Sim_t * p, Abc_Ntk_t * pAig )
+{
+    Abc_Obj_t * pObj;
+    unsigned * pInfo2;
+    int i;
+    Abc_NtkForEachPo( pAig, pObj, i )
+    {
+        pInfo2 = Vec_PtrEntry( p->vOuts, i );
+        Extra_PrintBinary( stdout, pInfo2, p->nPatsOut );
+        printf( "\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares simulation info for candidate filtering.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig, int nTruePis, int fVerbose )
+{
+    int Limit;
+    // prepare the manager
+    Res_SimAdjust( p, pAig );
+    // collect 0/1 simulation info
+    for ( Limit = 0; Limit < 10; Limit++ )
+    {
+        Res_SimSetRandom( p );
+        Res_SimPerformRound( p );
+        Res_SimProcessPats( p );
+        if ( !(p->nPats0 < p->nPats || p->nPats1 < p->nPats) )
+            break;
+    }
+//    printf( "%d   ", Limit );
+    // report the last set of patterns
+//    Res_SimReportOne( p );
+//    printf( "\n" );
+    // quit if there is not enough
+//    if ( p->nPats0 < 4 || p->nPats1 < 4 )
+    if ( p->nPats0 < 4 || p->nPats1 < 4 )
+    {
+//        Res_SimReportOne( p );
+        return 0;
+    }
+    // create bit-matrix info
+    if ( p->nPats0 < p->nPats )
+        Res_SimPadSimInfo( p->vPats0, p->nPats0, p->nWords );
+    if ( p->nPats1 < p->nPats )
+        Res_SimPadSimInfo( p->vPats1, p->nPats1, p->nWords );
+    // resimulate 0-patterns
+    Res_SimSetGiven( p, p->vPats0 );
+    Res_SimPerformRound( p );
+    Res_SimDeriveInfoReplicate( p );
+    // resimulate 1-patterns
+    Res_SimSetGiven( p, p->vPats1 );
+    Res_SimPerformRound( p );
+    Res_SimDeriveInfoComplement( p );
+    // print output patterns
+//    Res_SimPrintOutPatterns( p, pAig );
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/res/resStrash.c b/src/opt/res/resStrash.c
new file mode 100644
index 00000000..fde842a4
--- /dev/null
+++ b/src/opt/res/resStrash.c
@@ -0,0 +1,117 @@
+/**CFile****************************************************************
+
+  FileName    [resStrash.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  Synopsis    [Structural hashing of the nodes in the window.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: resStrash.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "resInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern Abc_Obj_t * Abc_ConvertAigToAig( Abc_Ntk_t * pAig, Abc_Obj_t * pObjOld );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Structurally hashes the given window.]
+
+  Description [The first PO is the observability condition. The second 
+  is the node's function. The remaining POs are the candidate divisors.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Res_WndStrash( Res_Win_t * p )
+{
+    Vec_Ptr_t * vPairs;
+    Abc_Ntk_t * pAig;
+    Abc_Obj_t * pObj, * pMiter;
+    int i;
+    assert( Abc_NtkHasAig(p->pNode->pNtk) );
+//    Abc_NtkCleanCopy( p->pNode->pNtk );
+    // create the network
+    pAig = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+    pAig->pName = Extra_UtilStrsav( "window" );
+    // create the inputs
+    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
+        pObj->pCopy = Abc_NtkCreatePi( pAig );
+    Vec_PtrForEachEntry( p->vBranches, pObj, i )
+        pObj->pCopy = Abc_NtkCreatePi( pAig );
+    // go through the nodes in the topological order
+    Vec_PtrForEachEntry( p->vNodes, pObj, i )
+    {
+        pObj->pCopy = Abc_ConvertAigToAig( pAig, pObj );
+        if ( pObj == p->pNode )
+            pObj->pCopy = Abc_ObjNot( pObj->pCopy );
+    }
+    // collect the POs
+    vPairs = Vec_PtrAlloc( 2 * Vec_PtrSize(p->vRoots) );
+    Vec_PtrForEachEntry( p->vRoots, pObj, i )
+    {
+        Vec_PtrPush( vPairs, pObj->pCopy );
+        Vec_PtrPush( vPairs, NULL );
+    }
+    // mark the TFO of the node
+    Abc_NtkIncrementTravId( p->pNode->pNtk );
+    Res_WinSweepLeafTfo_rec( p->pNode, (int)p->pNode->Level + p->nWinTfoMax );
+    // update strashing of the node
+    p->pNode->pCopy = Abc_ObjNot( p->pNode->pCopy );
+    Abc_NodeSetTravIdPrevious( p->pNode );
+    // redo strashing in the TFO
+    Vec_PtrForEachEntry( p->vNodes, pObj, i )
+    {
+        if ( Abc_NodeIsTravIdCurrent(pObj) )
+            pObj->pCopy = Abc_ConvertAigToAig( pAig, pObj );
+    }
+    // collect the POs
+    Vec_PtrForEachEntry( p->vRoots, pObj, i )
+        Vec_PtrWriteEntry( vPairs, 2 * i + 1, pObj->pCopy );
+    // add the miter
+    pMiter = Abc_AigMiter( pAig->pManFunc, vPairs );
+    Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pMiter );
+    Vec_PtrFree( vPairs );
+    // add the node
+    Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), p->pNode->pCopy );
+    // add the fanins
+    Abc_ObjForEachFanin( p->pNode, pObj, i )
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pObj->pCopy );
+    // add the divisors
+    Vec_PtrForEachEntry( p->vDivs, pObj, i )
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pObj->pCopy );
+    // add the names
+    Abc_NtkAddDummyPiNames( pAig );
+    Abc_NtkAddDummyPoNames( pAig );
+    // check the resulting network
+    if ( !Abc_NtkCheck( pAig ) )
+        fprintf( stdout, "Res_WndStrash(): Network check has failed.\n" );
+    return pAig;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/res/resWin.c b/src/opt/res/resWin.c
new file mode 100644
index 00000000..a3648925
--- /dev/null
+++ b/src/opt/res/resWin.c
@@ -0,0 +1,485 @@
+/**CFile****************************************************************
+
+  FileName    [resWin.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  Synopsis    [Windowing algorithm.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: resWin.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "resInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the window.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Res_Win_t * Res_WinAlloc()
+{
+    Res_Win_t * p;
+    // start the manager
+    p = ALLOC( Res_Win_t, 1 );
+    memset( p, 0, sizeof(Res_Win_t) );
+    // set internal parameters
+    p->nFanoutLimit = 10;
+    p->nLevTfiMinus =  3;
+    // allocate storage
+    p->vRoots    = Vec_PtrAlloc( 256 );
+    p->vLeaves   = Vec_PtrAlloc( 256 );
+    p->vBranches = Vec_PtrAlloc( 256 );
+    p->vNodes    = Vec_PtrAlloc( 256 );
+    p->vDivs     = Vec_PtrAlloc( 256 );
+    p->vMatrix   = Vec_VecStart( 128 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the window.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinFree( Res_Win_t * p )
+{
+    Vec_PtrFree( p->vRoots  );
+    Vec_PtrFree( p->vLeaves );
+    Vec_PtrFree( p->vBranches );
+    Vec_PtrFree( p->vNodes  );
+    Vec_PtrFree( p->vDivs   );
+    Vec_VecFree( p->vMatrix );
+    free( p );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collect the limited TFI cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_WinCollectLeavesAndNodes( Res_Win_t * p )
+{
+    Vec_Ptr_t * vFront;
+    Abc_Obj_t * pObj, * pTemp;
+    int i, k, m;
+
+    assert( p->nWinTfiMax > 0 );
+    assert( Vec_VecSize(p->vMatrix) > p->nWinTfiMax );
+
+    // start matrix with the node
+    Vec_VecClear( p->vMatrix );
+    Vec_VecPush( p->vMatrix, 0, p->pNode );
+    Abc_NtkIncrementTravId( p->pNode->pNtk );
+    Abc_NodeSetTravIdCurrent( p->pNode );
+
+    // collect the leaves (nodes pTemp such that "p->pNode->Level - pTemp->Level > p->nWinTfiMax")
+    Vec_PtrClear( p->vLeaves );
+    Vec_VecForEachLevelStartStop( p->vMatrix, vFront, i, 0, p->nWinTfiMax )
+    {
+        Vec_PtrForEachEntry( vFront, pObj, k )
+        {
+            Abc_ObjForEachFanin( pObj, pTemp, m )
+            {
+                if ( Abc_NodeIsTravIdCurrent( pTemp ) )
+                    continue;
+                Abc_NodeSetTravIdCurrent( pTemp );
+                if ( Abc_ObjIsCi(pTemp) || (int)(p->pNode->Level - pTemp->Level) > p->nWinTfiMax )                    
+                    Vec_PtrPush( p->vLeaves, pTemp );
+                else
+                    Vec_VecPush( p->vMatrix, p->pNode->Level - pTemp->Level, pTemp );
+            }
+        }
+    }
+    if ( Vec_PtrSize(p->vLeaves) == 0 )
+        return 0;
+
+    // collect the nodes in the reverse order
+    Vec_PtrClear( p->vNodes );
+    Vec_VecForEachLevelReverseStartStop( p->vMatrix, vFront, i, p->nWinTfiMax, 0 )
+    {
+        Vec_PtrForEachEntry( vFront, pObj, k )
+            Vec_PtrPush( p->vNodes, pObj );
+        Vec_PtrClear( vFront );
+    }
+
+    // get the lowest leaf level
+    p->nLevLeafMin = ABC_INFINITY;
+    Vec_PtrForEachEntry( p->vLeaves, pObj, k )
+        p->nLevLeafMin = ABC_MIN( p->nLevLeafMin, (int)pObj->Level );
+
+    // set minimum traversal level
+    p->nLevTravMin = ABC_MAX( ((int)p->pNode->Level) - p->nWinTfiMax - p->nLevTfiMinus, p->nLevLeafMin );
+    assert( p->nLevTravMin >= 0 );
+    return 1;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the node should be a root.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Res_WinComputeRootsCheck( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    // the node is the root if one of the following is true:
+    // (1) the node has more than fanouts than the limit
+    if ( Abc_ObjFanoutNum(pNode) > nFanoutLimit )
+        return 1;
+    // (2) the node has CO fanouts
+    // (3) the node has fanouts above the cutoff level
+    Abc_ObjForEachFanout( pNode, pFanout, i )
+        if ( Abc_ObjIsCo(pFanout) || (int)pFanout->Level > nLevelMax )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively collects the root candidates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinComputeRoots_rec( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit, Vec_Ptr_t * vRoots )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    assert( Abc_ObjIsNode(pNode) );
+    if ( Abc_NodeIsTravIdCurrent(pNode) )
+        return;
+    Abc_NodeSetTravIdCurrent( pNode );
+    // check if the node should be the root
+    if ( Res_WinComputeRootsCheck( pNode, nLevelMax, nFanoutLimit ) )
+        Vec_PtrPush( vRoots, pNode );
+    else // if not, explore its fanouts
+        Abc_ObjForEachFanout( pNode, pFanout, i )
+            Res_WinComputeRoots_rec( pFanout, nLevelMax, nFanoutLimit, vRoots );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively collects the root candidates.]
+
+  Description [Returns 1 if the only root is this node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_WinComputeRoots( Res_Win_t * p )
+{
+    Vec_PtrClear( p->vRoots );
+    Abc_NtkIncrementTravId( p->pNode->pNtk );
+    Res_WinComputeRoots_rec( p->pNode, p->pNode->Level + p->nWinTfoMax, p->nFanoutLimit, p->vRoots );
+    assert( Vec_PtrSize(p->vRoots) > 0 );
+    if ( Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode )
+        return 0;
+    return 1;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the paths from the roots to the leaves.]
+
+  Description [Returns 1 if the the node can reach a leaf.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_WinMarkPaths_rec( Abc_Obj_t * pNode, Abc_Obj_t * pPivot, int nLevelMin )
+{
+    Abc_Obj_t * pFanin;
+    int i, RetValue;
+    // skip visited nodes
+    if ( Abc_NodeIsTravIdCurrent(pNode) )
+        return 1;
+    if ( Abc_NodeIsTravIdPrevious(pNode) )
+        return 0;
+    // assume that the node does not have access to the leaves
+    Abc_NodeSetTravIdPrevious( pNode );
+    // skip nodes below the given level
+    if ( pNode == pPivot || (int)pNode->Level <= nLevelMin )
+        return 0;
+    assert( Abc_ObjIsNode(pNode) );
+    // check if the fanins have access to the leaves
+    RetValue = 0;
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        RetValue |= Res_WinMarkPaths_rec( pFanin, pPivot, nLevelMin );
+    // relabel the node if it has access to the leaves
+    if ( RetValue )
+        Abc_NodeSetTravIdCurrent( pNode );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the paths from the roots to the leaves.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinMarkPaths( Res_Win_t * p )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    // mark the leaves
+    Abc_NtkIncrementTravId( p->pNode->pNtk );
+    Abc_NtkIncrementTravId( p->pNode->pNtk );
+    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
+        Abc_NodeSetTravIdCurrent( pObj );
+    // traverse from the roots and mark the nodes that can reach leaves
+    // the nodes that do not reach leaves have previous trav ID
+    // the nodes that reach leaves have current trav ID
+    Vec_PtrForEachEntry( p->vRoots, pObj, i )
+        Res_WinMarkPaths_rec( pObj, p->pNode, p->nLevTravMin );
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively collects the roots.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinFinalizeRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    assert( Abc_ObjIsNode(pObj) );
+    assert( Abc_NodeIsTravIdCurrent(pObj) );
+    // check if the node has all fanouts marked
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        if ( !Abc_NodeIsTravIdCurrent(pFanout) )
+            break;
+    // if some of the fanouts are unmarked, add the node to the roots
+    if ( i < Abc_ObjFanoutNum(pObj) ) 
+        Vec_PtrPushUnique( vRoots, pObj );
+    else  // otherwise, call recursively
+        Abc_ObjForEachFanout( pObj, pFanout, i )
+            Res_WinFinalizeRoots_rec( pFanout, vRoots );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finalizes the roots of the window.]
+
+  Description [Roots of the window are the nodes that have at least
+  one fanout that it not in the TFO of the leaves.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_WinFinalizeRoots( Res_Win_t * p )
+{
+    assert( !Abc_NodeIsTravIdCurrent(p->pNode) );
+    // mark the node with the old traversal ID
+    Abc_NodeSetTravIdCurrent( p->pNode ); 
+    // recollect the roots
+    Vec_PtrClear( p->vRoots );
+    Res_WinFinalizeRoots_rec( p->pNode, p->vRoots );
+    assert( Vec_PtrSize(p->vRoots) > 0 );
+    if ( Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode )
+        return 0;
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively adds missing nodes and leaves.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj, int nLevTravMin )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    // skip the already collected leaves, nodes, and branches
+    if ( Abc_NodeIsTravIdCurrent(pObj) )
+        return;
+    // if this is not an internal node - make it a new branch
+    if ( !Abc_NodeIsTravIdPrevious(pObj) )
+    {
+        assert( Vec_PtrFind(p->vLeaves, pObj) == -1 );
+        Abc_NodeSetTravIdCurrent( pObj );
+        Vec_PtrPush( p->vBranches, pObj );
+        return;
+    }
+    assert( Abc_ObjIsNode(pObj) ); // if this is a CI, then the window is incorrect!
+    Abc_NodeSetTravIdCurrent( pObj );
+    // visit the fanins of the node
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        Res_WinAddMissing_rec( p, pFanin, nLevTravMin );
+    // collect the node
+    Vec_PtrPush( p->vNodes, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds to the window nodes and leaves in the TFI of the roots.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinAddMissing( Res_Win_t * p )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    // mark the leaves
+    Abc_NtkIncrementTravId( p->pNode->pNtk );
+    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
+        Abc_NodeSetTravIdCurrent( pObj );        
+    // mark the already collected nodes
+    Vec_PtrForEachEntry( p->vNodes, pObj, i )
+        Abc_NodeSetTravIdCurrent( pObj );        
+    // explore from the roots
+    Vec_PtrClear( p->vBranches );
+    Vec_PtrForEachEntry( p->vRoots, pObj, i )
+        Res_WinAddMissing_rec( p, pObj, p->nLevTravMin );
+}
+
+
+
+ 
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the window is trivial (without TFO).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_WinIsTrivial( Res_Win_t * p )
+{
+    return Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the window.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p )
+{
+    assert( Abc_ObjIsNode(pNode) );
+    assert( nWinTfiMax > 0 && nWinTfiMax < 10 );
+    assert( nWinTfoMax >= 0 && nWinTfoMax < 10 );
+
+    // initialize the window
+    p->pNode      = pNode;
+    p->nWinTfiMax = nWinTfiMax;
+    p->nWinTfoMax = nWinTfoMax;
+
+    Vec_PtrClear( p->vBranches );
+    Vec_PtrClear( p->vDivs );
+    Vec_PtrClear( p->vRoots );
+    Vec_PtrPush( p->vRoots, pNode );
+
+    // compute the leaves
+    if ( !Res_WinCollectLeavesAndNodes( p ) )
+        return 0;
+
+    // compute the candidate roots
+    if ( p->nWinTfoMax > 0 && Res_WinComputeRoots(p) )
+    {
+        // mark the paths from the roots to the leaves
+        Res_WinMarkPaths( p );
+        // refine the roots and add branches and missing nodes
+        if ( Res_WinFinalizeRoots( p ) )
+            Res_WinAddMissing( p );
+    }
+
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/res/res_.c b/src/opt/res/res_.c
new file mode 100644
index 00000000..a50affd7
--- /dev/null
+++ b/src/opt/res/res_.c
@@ -0,0 +1,50 @@
+/**CFile****************************************************************
+
+  FileName    [res_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: res_.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "res.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+