Windowing for technology mapping.

7 files changed, 450 insertions, 183 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index a6ff65f2..ef80d814 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -32,6 +32,7 @@
 #include <assert.h>
 
 #include "misc/vec/vec.h"
+#include "misc/vec/vecWec.h"
 #include "misc/util/utilCex.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -130,7 +131,9 @@ struct Gia_Man_t_
     Vec_Int_t *    vFanoutNums;   // static fanout
     Vec_Int_t *    vFanout;       // static fanout
     Vec_Int_t *    vMapping;      // mapping for each node
+    Vec_Wec_t *    vMapping2;     // mapping for each node
     Vec_Int_t *    vCellMapping;  // mapping for each node
+    void *         pSatlutWinman; // windowing for SAT-based mapping
     Vec_Int_t *    vPacking;      // packing information
     Vec_Int_t *    vConfigs;      // cell configurations
     char *         pCellStr;      // cell description
@@ -986,6 +989,12 @@ static inline int         Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i )   { re
 static inline int         Gia_ObjLutMuxId( Gia_Man_t * p, int Id )          { return Gia_ObjLutFanins(p, Id)[Gia_ObjLutSize(p, Id)];                        }
 static inline int         Gia_ObjLutIsMux( Gia_Man_t * p, int Id )          { return (int)(Gia_ObjLutMuxId(p, Id) < 0);                                     }
 
+static inline int         Gia_ManHasMapping2( Gia_Man_t * p )               { return p->vMapping2 != NULL;                                                  }
+static inline int         Gia_ObjIsLut2( Gia_Man_t * p, int Id )            { return Vec_IntSize(Vec_WecEntry(p->vMapping2, Id)) != 0;                      }
+static inline int         Gia_ObjLutSize2( Gia_Man_t * p, int Id )          { return Vec_IntSize(Vec_WecEntry(p->vMapping2, Id));                           }
+static inline Vec_Int_t * Gia_ObjLutFanins2( Gia_Man_t * p, int Id )        { return Vec_WecEntry(p->vMapping2, Id);                                        }
+static inline int         Gia_ObjLutFanin2( Gia_Man_t * p, int Id, int i )  { return Vec_IntEntry(Vec_WecEntry(p->vMapping2, Id), i);                       }
+
 static inline int         Gia_ManHasCellMapping( Gia_Man_t * p )            { return p->vCellMapping != NULL;                                               }
 static inline int         Gia_ObjIsCell( Gia_Man_t * p, int iLit )          { return Vec_IntEntry(p->vCellMapping, iLit) != 0;                              }
 static inline int         Gia_ObjIsCellInv( Gia_Man_t * p, int iLit )       { return Vec_IntEntry(p->vCellMapping, iLit) == -1;                             }
@@ -1002,6 +1011,15 @@ static inline int         Gia_ObjCellId( Gia_Man_t * p, int iLit )          { re
 #define Gia_LutForEachFaninObj( p, i, pFanin, k )                       \
     for ( k = 0; k < Gia_ObjLutSize(p,i) && ((pFanin = Gia_ManObj(p, Gia_ObjLutFanins(p,i)[k])),1); k++ )
 
+#define Gia_ManForEachLut2( p, i )                                      \
+    for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsLut2(p, i) ) {} else
+#define Gia_LutForEachFanin2( p, i, iFan, k )                           \
+    for ( k = 0; k < Gia_ObjLutSize2(p,i) && ((iFan = Gia_ObjLutFanin2(p,i,k)),1); k++ )
+#define Gia_ManForEachLut2Vec( vIds, p, vVec, iObj, i )                 \
+    for ( i = 0; i < Vec_IntSize(vIds) && (vVec = Vec_WecEntry(p->vMapping2, (iObj = Vec_IntEntry(vIds, i)))); i++ )
+#define Gia_ManForEachLut2VecReverse( vIds, p, vVec, iObj, i )          \
+    for ( i = Vec_IntSize(vIds)-1; i >= 0 && (vVec = Vec_WecEntry(p->vMapping2, (iObj = Vec_IntEntry(vIds, i)))); i-- )
+
 #define Gia_ManForEachCell( p, i )                                      \
     for ( i = 2; i < 2*Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsCell(p, i) ) {} else
 #define Gia_CellForEachFanin( p, i, iFanLit, k )                        \
@@ -1118,7 +1136,7 @@ extern Gia_Man_t *         Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs
 extern Gia_Man_t *         Gia_ManDupCofAll( Gia_Man_t * p, int nFanLim, int fVerbose );
 /*=== giaDfs.c ============================================================*/
 extern void                Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vSupp );
-extern void                Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes );
+extern void                Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes, Vec_Int_t * vLeaves );
 extern Vec_Int_t *         Gia_ManCollectNodesCis( Gia_Man_t * p, int * pNodes, int nNodes );
 extern int                 Gia_ManSuppSize( Gia_Man_t * p, int * pNodes, int nNodes );
 extern int                 Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes );
@@ -1359,6 +1377,9 @@ extern void                Gia_ManSimulateRound( Gia_ManSim_t * p );
 extern float               Gia_ManDelayTraceLut( Gia_Man_t * p );
 extern float               Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose );
 extern Gia_Man_t *         Gia_ManSpeedup( Gia_Man_t * p, int Percentage, int Degree, int fVerbose, int fVeryVerbose );
+/*=== giaSplit.c ============================================================*/
+extern void                Gia_ManComputeOneWinStart( Gia_Man_t * p, int fReverse );
+extern int                 Gia_ManComputeOneWin( Gia_Man_t * p, int iPivot, Vec_Int_t ** pvRoots, Vec_Int_t ** pvNodes, Vec_Int_t ** pvLeaves, Vec_Int_t ** pvAnds );
 /*=== giaStg.c ============================================================*/
 extern void                Gia_ManStgPrint( FILE * pFile, Vec_Int_t * vLines, int nIns, int nOuts, int nStates );
 extern Gia_Man_t *         Gia_ManStgRead( char * pFileName, int kHot, int fVerbose );
diff --git a/src/aig/gia/giaDfs.c b/src/aig/gia/giaDfs.c
index 940eaf46..0dd0ac8e 100644
--- a/src/aig/gia/giaDfs.c
+++ b/src/aig/gia/giaDfs.c
@@ -96,17 +96,19 @@ void Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vSu
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManCollectAnds_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
+void Gia_ManCollectAnds_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vNodes )
 {
-    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+    Gia_Obj_t * pObj;
+    if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
         return;
-    Gia_ObjSetTravIdCurrent(p, pObj);
+    Gia_ObjSetTravIdCurrentId(p, iObj);
+    pObj = Gia_ManObj( p, iObj );
     if ( Gia_ObjIsCi(pObj) )
         return;
     assert( Gia_ObjIsAnd(pObj) );
-    Gia_ManCollectAnds_rec( p, Gia_ObjFanin0(pObj), vNodes );
-    Gia_ManCollectAnds_rec( p, Gia_ObjFanin1(pObj), vNodes );
-    Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
+    Gia_ManCollectAnds_rec( p, Gia_ObjFaninId0(pObj, iObj), vNodes );
+    Gia_ManCollectAnds_rec( p, Gia_ObjFaninId1(pObj, iObj), vNodes );
+    Vec_IntPush( vNodes, iObj );
 }
 
 /**Function*************************************************************
@@ -120,20 +122,22 @@ void Gia_ManCollectAnds_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes )
+void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes, Vec_Int_t * vLeaves )
 {
-    Gia_Obj_t * pObj;
-    int i; 
-    Vec_IntClear( vNodes );
+    int i, iLeaf; 
 //    Gia_ManIncrementTravId( p );
-    Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
+    Gia_ObjSetTravIdCurrentId( p, 0 );
+    if ( vLeaves )
+        Vec_IntForEachEntry( vLeaves, iLeaf, i )
+            Gia_ObjSetTravIdCurrentId( p, iLeaf );
+    Vec_IntClear( vNodes );
     for ( i = 0; i < nNodes; i++ )
     {
-        pObj = Gia_ManObj( p, pNodes[i] );
+        Gia_Obj_t * pObj = Gia_ManObj( p, pNodes[i] );
         if ( Gia_ObjIsCo(pObj) )
-            Gia_ManCollectAnds_rec( p, Gia_ObjFanin0(pObj), vNodes );
+            Gia_ManCollectAnds_rec( p, Gia_ObjFaninId0(pObj, pNodes[i]), vNodes );
         else
-            Gia_ManCollectAnds_rec( p, pObj, vNodes );
+            Gia_ManCollectAnds_rec( p, pNodes[i], vNodes );
     }
 }
 
@@ -216,7 +220,7 @@ void Gia_ManCollectTest( Gia_Man_t * p )
     Gia_ManForEachCo( p, pObj, i )
     {
         iNode = Gia_ObjId(p, pObj);
-        Gia_ManCollectAnds( p, &iNode, 1, vNodes );
+        Gia_ManCollectAnds( p, &iNode, 1, vNodes, NULL );
     }
     Vec_IntFree( vNodes );
     ABC_PRT( "DFS from each output", Abc_Clock() - clk );
diff --git a/src/aig/gia/giaFrames.c b/src/aig/gia/giaFrames.c
index ebe2c139..3b33e3de 100644
--- a/src/aig/gia/giaFrames.c
+++ b/src/aig/gia/giaFrames.c
@@ -706,7 +706,7 @@ void Gia_ManFraSupports( Gia_ManFra_t * p )
         vIns = Vec_IntAlloc( 100 );
         Gia_ManCollectCis( p->pAig, Vec_IntArray(vOuts), Vec_IntSize(vOuts), vIns );
         vAnds = Vec_IntAlloc( 100 );
-        Gia_ManCollectAnds( p->pAig, Vec_IntArray(vOuts), Vec_IntSize(vOuts), vAnds );
+        Gia_ManCollectAnds( p->pAig, Vec_IntArray(vOuts), Vec_IntSize(vOuts), vAnds, NULL );
         Vec_PtrWriteEntry( p->vIns,  f, vIns );
         Vec_PtrWriteEntry( p->vAnds, f, vAnds );
         Vec_PtrWriteEntry( p->vOuts, f, vOuts );
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index d93390e3..f5071929 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -249,10 +249,10 @@ void Gia_ManSetRefsMapped( Gia_Man_t * p )
     ABC_FREE( p->pRefs );
     p->pRefs = ABC_CALLOC( int, Gia_ManObjNum(p) );
     Gia_ManForEachCo( p, pObj, i )
-        Gia_ObjRefInc( p, Gia_ObjFanin0(pObj) );
+        Gia_ObjRefIncId( p, Gia_ObjFaninId0p(p, pObj) );
     Gia_ManForEachLut( p, i )
         Gia_LutForEachFanin( p, i, iFan, k )
-            Gia_ObjRefInc( p, Gia_ManObj(p, iFan) );
+            Gia_ObjRefIncId( p, iFan );
 }
 
 /**Function*************************************************************
@@ -273,10 +273,10 @@ void Gia_ManSetLutRefs( Gia_Man_t * p )
     ABC_FREE( p->pLutRefs );
     p->pLutRefs = ABC_CALLOC( int, Gia_ManObjNum(p) );
     Gia_ManForEachCo( p, pObj, i )
-        Gia_ObjLutRefInc( p, Gia_ObjFanin0(pObj) );
+        Gia_ObjLutRefIncId( p, Gia_ObjFaninId0p(p, pObj) );
     Gia_ManForEachLut( p, i )
         Gia_LutForEachFanin( p, i, iFan, k )
-            Gia_ObjLutRefInc( p, Gia_ManObj(p, iFan) );
+            Gia_ObjLutRefIncId( p, iFan );
 }
 
 /**Function*************************************************************
@@ -1568,7 +1568,7 @@ int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, Gia_Man_t *
         // collect nodes
         Gia_ManIncrementTravId( pTemp );
         Id = Abc_Lit2Var( iLit );
-        Gia_ManCollectAnds( pTemp, &Id, 1, vCover );
+        Gia_ManCollectAnds( pTemp, &Id, 1, vCover, NULL );
         Vec_IntPrint( vCover );
         Gia_ManForEachObjVec( vCover, pTemp, pObj, i )
             Gia_ObjPrint( pTemp, pObj );
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index cba58b3c..ea25c4ab 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -113,6 +113,7 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_WrdFreeP( &p->vTtMemory );
     Vec_PtrFreeP( &p->vTtInputs );
     Vec_IntFreeP( &p->vMapping );
+    Vec_WecFreeP( &p->vMapping2 );
     Vec_IntFreeP( &p->vCellMapping );
     Vec_IntFreeP( &p->vPacking );
     Vec_IntFreeP( &p->vConfigs );
diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c
index 7f18a485..f985eb50 100644
--- a/src/aig/gia/giaSatLut.c
+++ b/src/aig/gia/giaSatLut.c
@@ -20,7 +20,6 @@
 
 #include "gia.h"
 #include "sat/bsat/satStore.h"
-#include "misc/vec/vecWec.h"
 #include "misc/util/utilNam.h"
 #include "map/scl/sclCon.h"
 
@@ -40,13 +39,12 @@ struct Sbl_Man_t_
     int              FirstVar;   // first variable to be used
     int              LitShift;   // shift in terms of literals (2*Gia_ManCiNum(pGia)+2)
     int              nInputs;    // the number of inputs
-    // mapping 
-    Vec_Wec_t *      vMapping;   // current mapping
     // window
     Gia_Man_t *      pGia;
     Vec_Int_t *      vLeaves;    // leaf nodes
-    Vec_Int_t *      vNodes;     // internal nodes
-    Vec_Int_t *      vRoots;     // driver nodes (a subset of vNodes)
+    Vec_Int_t *      vAnds;      // AND-gates
+    Vec_Int_t *      vNodes;     // internal LUTs
+    Vec_Int_t *      vRoots;     // driver nodes (a subset of vAnds)
     Vec_Int_t *      vRootVars;  // driver nodes (as SAT variables)
     // cuts
     Vec_Wrd_t *      vCutsI;     // input bit patterns
@@ -79,55 +77,55 @@ struct Sbl_Man_t_
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Wec_t * Sbl_ManToMapping( Gia_Man_t * p )
-{
-    Vec_Wec_t * vMapping = Vec_WecStart( Gia_ManObjNum(p) );
-    int Obj, Fanin, k;
-    Gia_ManForEachLut( p, Obj )
-        Gia_LutForEachFanin( p, Obj, Fanin, k )
-            Vec_WecPush( vMapping, Obj, Fanin );
-    return vMapping;
-}
-Vec_Int_t * Sbl_ManFromMapping( Gia_Man_t * p, Vec_Wec_t * vMap )
-{
-    Vec_Int_t * vMapping, * vVec; int i, k, Obj;
-    vMapping = Vec_IntAlloc( Gia_ManObjNum(p) + Vec_WecSizeSize(vMap) + 2*Vec_WecSizeUsed(vMap) );
-    Vec_IntFill( vMapping, Gia_ManObjNum(p), 0 );
-    Vec_WecForEachLevel( vMap, vVec, i )
-        if ( Vec_IntSize(vVec) > 0 )
-        {
-            Vec_IntWriteEntry( vMapping, i, Vec_IntSize(vMapping) );
-            Vec_IntPush( vMapping, Vec_IntSize(vVec) );
-            Vec_IntForEachEntry( vVec, Obj, k )
-                Vec_IntPush( vMapping, Obj );
-            Vec_IntPush( vMapping, i );
-        }
-    assert( Vec_IntSize(vMapping) < 16 || Vec_IntSize(vMapping) == Vec_IntCap(vMapping) );
-    return vMapping;
-}
 void Sbl_ManUpdateMapping( Sbl_Man_t * p )
 {
+//    Gia_Obj_t * pObj;
     Vec_Int_t * vObj;
-    int i, c, b, iObj; 
     word CutI, CutN;
+    int i, c, b, iObj, iTemp; 
     assert( Vec_IntSize(p->vSolCuts2) < Vec_IntSize(p->vSolCuts) );
-    Vec_IntForEachEntry( p->vNodes, iObj, i )
-        Vec_IntClear( Vec_WecEntry(p->vMapping, iObj) );
+    Vec_IntForEachEntry( p->vAnds, iObj, i )
+    {
+        vObj = Vec_WecEntry(p->pGia->vMapping2, iObj);
+        Vec_IntForEachEntry( vObj, iTemp, b )
+            Gia_ObjLutRefDecId( p->pGia, iTemp );
+        Vec_IntClear( vObj );
+    }
     Vec_IntForEachEntry( p->vSolCuts2, c, i )
     {
         CutI = Vec_WrdEntry( p->vCutsI, c );
         CutN = Vec_WrdEntry( p->vCutsN, c );
         iObj = Vec_IntEntry( p->vCutsObj, c );
-        iObj = Vec_IntEntry( p->vNodes, iObj );
-        vObj = Vec_WecEntry( p->vMapping, iObj );
+        iObj = Vec_IntEntry( p->vAnds, iObj );
+        vObj = Vec_WecEntry( p->pGia->vMapping2, iObj );
         assert( Vec_IntSize(vObj) == 0 );
         for ( b = 0; b < 64; b++ )
             if ( (CutI >> b) & 1 )
                 Vec_IntPush( vObj, Vec_IntEntry(p->vLeaves, b) );
         for ( b = 0; b < 64; b++ )
             if ( (CutN >> b) & 1 )
-                Vec_IntPush( vObj, Vec_IntEntry(p->vNodes, b) );
+                Vec_IntPush( vObj, Vec_IntEntry(p->vAnds, b) );
+        Vec_IntForEachEntry( vObj, iTemp, b )
+            Gia_ObjLutRefIncId( p->pGia, iTemp );
     }
+/*
+    // verify
+    Gia_ManForEachLut2Vec( p->pGia, vObj, i )
+        Vec_IntForEachEntry( vObj, iTemp, b )
+            Gia_ObjLutRefDecId( p->pGia, iTemp );
+    Gia_ManForEachCo( p->pGia, pObj, i )
+        Gia_ObjLutRefDecId( p->pGia, Gia_ObjFaninId0p(p->pGia, pObj) );
+
+    for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
+        if ( p->pGia->pLutRefs[i] )
+            printf( "Object %d has %d refs\n", i, p->pGia->pLutRefs[i] );
+
+    Gia_ManForEachCo( p->pGia, pObj, i )
+        Gia_ObjLutRefIncId( p->pGia, Gia_ObjFaninId0p(p->pGia, pObj) );
+    Gia_ManForEachLut2Vec( p->pGia, vObj, i )
+        Vec_IntForEachEntry( vObj, iTemp, b )
+            Gia_ObjLutRefIncId( p->pGia, iTemp );
+*/
 }
 
 /**Function*************************************************************
@@ -147,11 +145,11 @@ static int Sbl_ManPrintCut( word CutI, word CutN, int nInputs )
     printf( "{ " );
     for ( b = 0; b < 64; b++ )
         if ( (CutI >> b) & 1 )
-            printf( "i%d ", b + 1 ), Count++;
+            printf( "i%d ", b ), Count++;
     printf( " " );
     for ( b = 0; b < 64; b++ )
         if ( (CutN >> b) & 1 )
-            printf( "n%d ", nInputs + b + 1 ), Count++;
+            printf( "n%d ", b ), Count++;
     printf( "};\n" );
     return Count;
 }
@@ -219,12 +217,12 @@ static inline int Sbl_ManFindCut( Sbl_Man_t * p, int Obj, word CutI, word CutN )
     int Start0 = Vec_IntEntry( p->vCutsStart, Obj );
     int Limit0 = Start0 + Vec_IntEntry( p->vCutsNum, Obj );
     int i;
-//    printf( "Looking for:\n" );
-//    Sbl_ManPrintCut( CutI, CutN, p->nInputs );
-//    printf( "\n" );
+    //printf( "\nLooking for:\n" );
+    //Sbl_ManPrintCut( CutI, CutN, p->nInputs );
+    //printf( "\n" );
     for ( i = Start0; i < Limit0; i++ )
     {
-//        Sbl_ManPrintCut( pCutsI[i], pCutsN[i], p->nInputs );
+        //Sbl_ManPrintCut( pCutsI[i], pCutsN[i], p->nInputs );
         if ( pCutsI[i] == CutI && pCutsN[i] == CutN )
             return i;
     }
@@ -232,9 +230,9 @@ static inline int Sbl_ManFindCut( Sbl_Man_t * p, int Obj, word CutI, word CutN )
 }
 int Sbl_ManComputeCuts( Sbl_Man_t * p )
 {
-    Gia_Obj_t * pObj, * pFanin; 
-    int i, k, Index, nObjs = Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes);
-    assert( Vec_IntSize(p->vLeaves) <= 64 && Vec_IntSize(p->vNodes) <= 64 );
+    Gia_Obj_t * pObj; Vec_Int_t * vFanins;
+    int i, k, Index, Fanin, nObjs = Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vAnds);
+    assert( Vec_IntSize(p->vLeaves) <= 64 && Vec_IntSize(p->vAnds) <= 64 );
     // assign leaf cuts
     Vec_IntClear( p->vCutsStart );
     Vec_IntClear( p->vCutsObj );
@@ -251,7 +249,7 @@ int Sbl_ManComputeCuts( Sbl_Man_t * p )
         pObj->Value = i;
     }
     // assign internal cuts
-    Gia_ManForEachObjVec( p->vNodes, p->pGia, pObj, i )
+    Gia_ManForEachObjVec( p->vAnds, p->pGia, pObj, i )
     {
         assert( Gia_ObjIsAnd(pObj) );
         assert( ~Gia_ObjFanin0(pObj)->Value );
@@ -270,27 +268,30 @@ int Sbl_ManComputeCuts( Sbl_Man_t * p )
         int Obj = Gia_ObjId(p->pGia, pObj);
         if ( Gia_ObjIsCi(pObj) )
             continue;
-        assert( Gia_ObjIsLut(p->pGia, Obj) );
+        assert( Gia_ObjIsLut2(p->pGia, Obj) );
         assert( ~pObj->Value );
         Vec_IntPush( p->vRootVars, pObj->Value - Vec_IntSize(p->vLeaves) );
     }
     // create current solution
     Vec_IntClear( p->vPolar );
     Vec_IntClear( p->vSolCuts );
-    Gia_ManForEachObjVec( p->vNodes, p->pGia, pObj, i )
+    Gia_ManForEachObjVec( p->vAnds, p->pGia, pObj, i )
     {
         word CutI = 0, CutN = 0;
         int Obj = Gia_ObjId(p->pGia, pObj);
-        if ( !Gia_ObjIsLut(p->pGia, Obj) )
+        if ( !Gia_ObjIsLut2(p->pGia, Obj) )
             continue;
         assert( (int)pObj->Value == Vec_IntSize(p->vLeaves) + i );
         // add node
         Vec_IntPush( p->vPolar, i );
         Vec_IntPush( p->vSolCuts, i );
         // add its cut
-        Gia_LutForEachFaninObj( p->pGia, Obj, pFanin, k )
+        //Gia_LutForEachFaninObj( p->pGia, Obj, pFanin, k )
+        vFanins = Gia_ObjLutFanins2( p->pGia, Obj );
+        Vec_IntForEachEntry( vFanins, Fanin, k )
         {
-            assert( (int)pFanin->Value < Vec_IntSize(p->vLeaves) || Gia_ObjIsLut(p->pGia, Gia_ObjId(p->pGia, pFanin)) );
+            Gia_Obj_t * pFanin = Gia_ManObj( p->pGia, Fanin );
+            assert( (int)pFanin->Value < Vec_IntSize(p->vLeaves) || Gia_ObjIsLut2(p->pGia, Fanin) );
             assert( ~pFanin->Value );
             if ( (int)pFanin->Value < Vec_IntSize(p->vLeaves) )
                 CutI |= ((word)1 << pFanin->Value);
@@ -299,13 +300,18 @@ int Sbl_ManComputeCuts( Sbl_Man_t * p )
         }
         // find the new cut
         Index = Sbl_ManFindCut( p, Vec_IntSize(p->vLeaves) + i, CutI, CutN );
+        if ( Index < 0 )
+        {
+            printf( "Cannot find the available cut.\n" );
+            continue;
+        }
         assert( Index >= 0 );
         Vec_IntPush( p->vPolar, p->FirstVar+Index );
     }
     // clean value
     Gia_ManForEachObjVec( p->vLeaves, p->pGia, pObj, i )
         pObj->Value = ~0;
-    Gia_ManForEachObjVec( p->vNodes, p->pGia, pObj, i )
+    Gia_ManForEachObjVec( p->vAnds, p->pGia, pObj, i )
         pObj->Value = ~0;
     return Vec_WrdSize(p->vCutsI);
 }
@@ -316,7 +322,7 @@ int Sbl_ManCreateCnf( Sbl_Man_t * p )
     assert( p->FirstVar == sat_solver_nvars(p->pSat) );
     sat_solver_setnvars( p->pSat, sat_solver_nvars(p->pSat) + Vec_WrdSize(p->vCutsI) );
     //printf( "\n" );
-    for ( i = 0; i < Vec_IntSize(p->vNodes); i++ )
+    for ( i = 0; i < Vec_IntSize(p->vAnds); i++ )
     {
         int Start0 = Vec_IntEntry( p->vCutsStart, Vec_IntSize(p->vLeaves) + i );
         int Limit0 = Start0 + Vec_IntEntry( p->vCutsNum, Vec_IntSize(p->vLeaves) + i ) - 1;
@@ -380,6 +386,7 @@ Sbl_Man_t * Sbl_ManAlloc( Gia_Man_t * pGia, int LogN )
     // window
     p->pGia       = pGia;
     p->vLeaves    = Vec_IntAlloc( 64 );
+    p->vAnds      = Vec_IntAlloc( 64 );
     p->vNodes     = Vec_IntAlloc( 64 );
     p->vRoots     = Vec_IntAlloc( 64 );
     p->vRootVars  = Vec_IntAlloc( 64 );
@@ -399,7 +406,6 @@ Sbl_Man_t * Sbl_ManAlloc( Gia_Man_t * pGia, int LogN )
     p->vPolar     = Vec_IntAlloc( 1000 );
     // other
     Gia_ManFillValue( pGia );
-    p->vMapping   = Sbl_ManToMapping( pGia );
     return p;
 }
 
@@ -407,9 +413,9 @@ void Sbl_ManStop( Sbl_Man_t * p )
 {
     sat_solver_delete( p->pSat );
     Vec_IntFree( p->vCardVars );
-    Vec_WecFree( p->vMapping );
     // internal
     Vec_IntFree( p->vLeaves );
+    Vec_IntFree( p->vAnds );
     Vec_IntFree( p->vNodes );
     Vec_IntFree( p->vRoots );
     Vec_IntFree( p->vRootVars );
@@ -439,25 +445,68 @@ void Sbl_ManWindow( Sbl_Man_t * p )
     Gia_ManForEachCiId( p->pGia, ObjId, i )
         Vec_IntPush( p->vLeaves, ObjId );
     // collect internal
-    Vec_IntClear( p->vNodes );
+    Vec_IntClear( p->vAnds );
     Gia_ManForEachAndId( p->pGia, ObjId )
-        Vec_IntPush( p->vNodes, ObjId );
+        Vec_IntPush( p->vAnds, ObjId );
     // collect roots
     Vec_IntClear( p->vRoots );
     Gia_ManForEachCoDriverId( p->pGia, ObjId, i )
         Vec_IntPush( p->vRoots, ObjId );
 }
 
-int Sbl_ManTestSat( Gia_Man_t * pGia, int fVerbose )
+int Sbl_ManWindow2( Sbl_Man_t * p, int iPivot )
 {
+    Vec_Int_t * vRoots, * vNodes, * vLeaves, * vAnds;
+    int Count = Gia_ManComputeOneWin( p->pGia, iPivot, &vRoots, &vNodes, &vLeaves, &vAnds );
+    if ( Count == 0 )
+        return 0;
+    Vec_IntClear( p->vRoots );   Vec_IntAppend( p->vRoots,  vRoots );
+    Vec_IntClear( p->vNodes );   Vec_IntAppend( p->vNodes,  vNodes );
+    Vec_IntClear( p->vLeaves );  Vec_IntAppend( p->vLeaves, vLeaves );
+    Vec_IntClear( p->vAnds );    Vec_IntAppend( p->vAnds,   vAnds );
+//Vec_IntPrint( vRoots );
+//Vec_IntPrint( vAnds );
+//Vec_IntPrint( vLeaves );
+    // recompute internal nodes
+//    Gia_ManIncrementTravId( p->pGia );
+//    Gia_ManCollectAnds( p->pGia, Vec_IntArray(p->vRoots), Vec_IntSize(p->vRoots), p->vAnds, p->vLeaves );
+    return Count;
+}
+
+int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int fVerbose )
+{
+    int fKeepTrying = 1;
     abctime clk = Abc_Clock(), clk2;
     int i, LogN = 6, nVars = 1 << LogN, status, Root;
     Sbl_Man_t * p = Sbl_ManAlloc( pGia, LogN );
-    int fKeepTrying = 1;
-    int StartSol;
+    int StartSol, Count, nConfTotal = 0;
+
+    // compute one window
+    Count = Sbl_ManWindow2( p, iPivot );
+    if ( Count == 0 )
+    {
+        printf( "Obj %d: Window with less than %d inputs does not exist.\n", iPivot, 64 );
+        Sbl_ManStop( p );
+        return 0;
+    }
+    if ( fVerbose )
+    printf( "\nObj = %6d : Leaf = %2d.  LUT = %2d.  AND = %2d.  Root = %2d.\n", 
+        iPivot, Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vAnds), Vec_IntSize(p->vRoots) ); 
+    if ( Vec_IntSize(p->vLeaves) > 64 || Vec_IntSize(p->vAnds) > 64 )
+    {
+        printf( "Obj %d: Encountered window with %d inputs and %d internal nodes.\n", iPivot, Vec_IntSize(p->vLeaves), Vec_IntSize(p->vAnds) );
+        Sbl_ManStop( p );
+        return 0;
+    }
+
+    if ( Vec_IntSize(p->vAnds) < 20 )
+    {
+        if ( fVerbose )
+        printf( "Skipping.\n" );
+        Sbl_ManStop( p );
+        return 0;
+    }
 
-    // derive window
-    Sbl_ManWindow( p );
     // derive cuts
     Sbl_ManComputeCuts( p );
     // derive SAT instance
@@ -468,7 +517,7 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int fVerbose )
 
     if ( fVerbose )
     printf( "All clauses = %d.  Multi clauses = %d.  Binary clauses = %d.  Other clauses = %d.\n\n", 
-        sat_solver_nclauses(p->pSat), Vec_IntSize(p->vNodes), Vec_WrdSize(p->vCutsI) - Vec_IntSize(p->vNodes), 
+        sat_solver_nclauses(p->pSat), Vec_IntSize(p->vAnds), Vec_WrdSize(p->vCutsI) - Vec_IntSize(p->vAnds), 
         sat_solver_nclauses(p->pSat) - Vec_WrdSize(p->vCutsI) );
 
     // create assumptions
@@ -476,17 +525,19 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int fVerbose )
     Vec_IntClear( p->vAssump );
     Vec_IntPush( p->vAssump, -1 );
     // unused variables
-    for ( i = Vec_IntSize(p->vNodes); i < nVars; i++ )
+    for ( i = Vec_IntSize(p->vAnds); i < nVars; i++ )
         Vec_IntPush( p->vAssump, Abc_Var2Lit(i, 1) );
     // root variables
     Vec_IntForEachEntry( p->vRootVars, Root, i )
         Vec_IntPush( p->vAssump, Abc_Var2Lit(Root, 0) );
 //    Vec_IntPrint( p->vAssump );
 
+    Vec_IntClear( p->vSolCuts2 );
     StartSol = Vec_IntSize(p->vSolCuts) + 1;
 //    StartSol = 30;
     while ( fKeepTrying && StartSol-fKeepTrying > 0 )
     {
+        int nConfBef, nConfAft;
         if ( fVerbose )
             printf( "Trying to find mapping with %d gates.\n", StartSol-fKeepTrying );
     //    for ( i = Vec_IntSize(p->vSolCuts)-5; i < nVars; i++ )
@@ -494,19 +545,24 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int fVerbose )
         Vec_IntWriteEntry( p->vAssump, 0, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, StartSol-fKeepTrying), 1) );
         // solve the problem
         clk2 = Abc_Clock();
-        status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), 0, 0, 0, 0 );
+        nConfBef = (int)p->pSat->stats.conflicts;
+        status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), nBTLimit, 0, 0, 0 );
+        nConfAft = (int)p->pSat->stats.conflicts;
+        nConfTotal += nConfAft - nConfBef;
+        if ( status == l_Undef )
+            break;
         if ( status == l_True )
         {
             int Count = 0, LitCount = 0;
             if ( fVerbose )
             {
                 printf( "Inputs = %d.  ANDs = %d.  Total = %d. All vars = %d.\n", 
-                    Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), 
-                    Vec_IntSize(p->vLeaves)+Vec_IntSize(p->vNodes), nVars );
-                for ( i = 0; i < Vec_IntSize(p->vNodes); i++ )
+                    Vec_IntSize(p->vLeaves), Vec_IntSize(p->vAnds), 
+                    Vec_IntSize(p->vLeaves)+Vec_IntSize(p->vAnds), nVars );
+                for ( i = 0; i < Vec_IntSize(p->vAnds); i++ )
                     printf( "%d", sat_solver_var_value(p->pSat, i) );
                 printf( "\n" );
-                for ( i = 0; i < Vec_IntSize(p->vNodes); i++ )
+                for ( i = 0; i < Vec_IntSize(p->vAnds); i++ )
                     if ( sat_solver_var_value(p->pSat, i) )
                     {
                         printf( "%d=%d ", i, sat_solver_var_value(p->pSat, i) );
@@ -523,13 +579,18 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int fVerbose )
                 if ( sat_solver_var_value(p->pSat, i) )
                 {
                     if ( fVerbose )
-                        printf( "Cut %3d : ", Count++ );
+                        printf( "Cut %3d : Node = %3d  Node = %6d  ", Count++, Vec_IntEntry(p->vCutsObj, i-p->FirstVar), Vec_IntEntry(p->vAnds, Vec_IntEntry(p->vCutsObj, i-p->FirstVar)) );
                     if ( fVerbose )
                         LitCount += Sbl_ManFindAndPrintCut( p, i-p->FirstVar );
                     Vec_IntPush( p->vSolCuts2, i-p->FirstVar );
                 }
             if ( fVerbose )
-                printf( "LitCount = %d.\n", LitCount );
+            printf( "LitCount = %d.\n", LitCount );
+            if ( fVerbose )
+            Vec_IntPrint( p->vRootVars );
+            //Vec_IntPrint( p->vRoots );
+            //Vec_IntPrint( p->vAnds );
+            //Vec_IntPrint( p->vLeaves );
         }
         fKeepTrying = status == l_True ? fKeepTrying + 1 : 0;
         if ( fVerbose )
@@ -547,18 +608,30 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int fVerbose )
     }
 
     // update solution
-    Sbl_ManUpdateMapping( p );
-
-    Vec_IntFreeP( &pGia->vMapping );
-    pGia->vMapping = Sbl_ManFromMapping( pGia, p->vMapping );
-
+    if ( Vec_IntSize(p->vSolCuts2) > 0 && Vec_IntSize(p->vSolCuts2) < Vec_IntSize(p->vSolCuts) )
+    {
+        Sbl_ManUpdateMapping( p );
+        printf( "Object %d : Saved %d nodes.  (Conf = %d.)\n", iPivot, Vec_IntSize(p->vSolCuts)-Vec_IntSize(p->vSolCuts2), nConfTotal );
+        Sbl_ManStop( p );
+        return 2;
+    }
     Sbl_ManStop( p );
     return 1;
 }
 
-void Gia_ManLutSat( Gia_Man_t * p, int nNumber, int nConfl, int fVerbose )
+void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nConfl, int fReverse, int fVerbose )
 {
-    Sbl_ManTestSat( p, fVerbose );
+    int iLut;
+    Gia_ManComputeOneWinStart( pGia, fReverse );
+    Gia_ManForEachLut2( pGia, iLut )
+    {
+//        if ( iLut > 259 )
+//            break;
+        if ( Sbl_ManTestSat( pGia, nConfl, iLut, fVerbose ) != 2 )
+            continue;
+//        break;
+    }
+    Gia_ManComputeOneWin( pGia, -1, NULL, NULL, NULL, NULL );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaSplit.c b/src/aig/gia/giaSplit.c
index c2e2d448..8bb5d3c0 100644
--- a/src/aig/gia/giaSplit.c
+++ b/src/aig/gia/giaSplit.c
@@ -35,14 +35,16 @@ struct Spl_Man_t_
     Gia_Man_t *      pGia;       // user AIG with nodes marked
     int              iObj;       // object ID
     int              Limit;      // limit on AIG nodes
-    int              Count;      // count of AIG nodes
+    int              fReverse;   // enable reverse search
     // intermediate
     Vec_Bit_t *      vMarksCIO;  // CI/CO marks
     Vec_Bit_t *      vMarksIn;   // input marks
     Vec_Bit_t *      vMarksNo;   // node marks
-    Vec_Int_t *      vNodes;     // nodes used in the window
+    Vec_Bit_t *      vMarksAnd;  // AND node marks
     Vec_Int_t *      vRoots;     // nodes pointing to Nodes
+    Vec_Int_t *      vNodes;     // nodes used in the window
     Vec_Int_t *      vLeaves;    // nodes pointed by Nodes
+    Vec_Int_t *      vAnds;      // AND nodes used in the window
     // temporary 
     Vec_Int_t *      vFanouts;   // fanouts of the node
     Vec_Int_t *      vCands;     // candidate nodes
@@ -55,7 +57,48 @@ struct Spl_Man_t_
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Transforming to the internal LUT representation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wec_t * Spl_ManToWecMapping( Gia_Man_t * p )
+{
+    Vec_Wec_t * vMapping = Vec_WecStart( Gia_ManObjNum(p) );
+    int Obj, Fanin, k;
+    assert( Gia_ManHasMapping(p) );
+    Gia_ManForEachLut( p, Obj )
+        Gia_LutForEachFanin( p, Obj, Fanin, k )
+            Vec_WecPush( vMapping, Obj, Fanin );
+    return vMapping;
+}
+Vec_Int_t * Spl_ManFromWecMapping( Gia_Man_t * p, Vec_Wec_t * vMap )
+{
+    Vec_Int_t * vMapping, * vVec; int i, k, Obj;
+    assert( Gia_ManHasMapping2(p) );
+    vMapping = Vec_IntAlloc( Gia_ManObjNum(p) + Vec_WecSizeSize(vMap) + 2*Vec_WecSizeUsed(vMap) );
+    Vec_IntFill( vMapping, Gia_ManObjNum(p), 0 );
+    Vec_WecForEachLevel( vMap, vVec, i )
+        if ( Vec_IntSize(vVec) > 0 )
+        {
+            Vec_IntWriteEntry( vMapping, i, Vec_IntSize(vMapping) );
+            Vec_IntPush( vMapping, Vec_IntSize(vVec) );
+            Vec_IntForEachEntry( vVec, Obj, k )
+                Vec_IntPush( vMapping, Obj );
+            Vec_IntPush( vMapping, i );
+        }
+    assert( Vec_IntSize(vMapping) < 16 || Vec_IntSize(vMapping) == Vec_IntCap(vMapping) );
+    return vMapping;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creating manager.]
 
   Description []
                
@@ -64,45 +107,62 @@ struct Spl_Man_t_
   SeeAlso     []
 
 ***********************************************************************/
-Spl_Man_t * Spl_ManAlloc( Gia_Man_t * pGia, int Limit )
+Spl_Man_t * Spl_ManAlloc( Gia_Man_t * pGia, int Limit, int fReverse )
 {
     int i, iObj;
     Spl_Man_t * p = ABC_CALLOC( Spl_Man_t, 1 );
-    assert( Gia_ManHasMapping(pGia) );
     p->pGia       = pGia;
     p->Limit      = Limit;
+    p->fReverse   = fReverse;
     // intermediate
     p->vMarksCIO  = Vec_BitStart( Gia_ManObjNum(pGia) );
     p->vMarksIn   = Vec_BitStart( Gia_ManObjNum(pGia) );
     p->vMarksNo   = Vec_BitStart( Gia_ManObjNum(pGia) );
+    p->vMarksAnd  = Vec_BitStart( Gia_ManObjNum(pGia) );
     p->vRoots     = Vec_IntAlloc( 100 );
     p->vNodes     = Vec_IntAlloc( 100 );
     p->vLeaves    = Vec_IntAlloc( 100 );
+    p->vAnds      = Vec_IntAlloc( 100 );
     // temporary 
     p->vFanouts   = Vec_IntAlloc( 100 );
     p->vCands     = Vec_IntAlloc( 100 );
     p->vInputs    = Vec_IntAlloc( 100 );
     // mark CIs/COs
+    Vec_BitWriteEntry( p->vMarksCIO, 0, 1 );
     Gia_ManForEachCiId( pGia, iObj, i )
         Vec_BitWriteEntry( p->vMarksCIO, iObj, 1 );
     Gia_ManForEachCoId( pGia, iObj, i )
         Vec_BitWriteEntry( p->vMarksCIO, iObj, 1 );
-    // prepare AIG
-    Gia_ManStaticFanoutStart( pGia );
-    Gia_ManSetLutRefs( pGia );
+    // mapping
+    ABC_FREE( pGia->pRefs );
     Gia_ManCreateRefs( pGia );
+    Gia_ManSetLutRefs( pGia );
+    assert( Gia_ManHasMapping(pGia) );
+    assert( !Gia_ManHasMapping2(pGia) );
+    pGia->vMapping2 = Spl_ManToWecMapping( pGia );
+    Vec_IntFreeP( &pGia->vMapping );
+    // fanout
+    Gia_ManStaticFanoutStart( pGia );
     return p;
 }
 void Spl_ManStop( Spl_Man_t * p )
 {
+    // fanout
     Gia_ManStaticFanoutStop( p->pGia );
+    // mapping
+    assert( !Gia_ManHasMapping(p->pGia) );
+    assert( Gia_ManHasMapping2(p->pGia) );
+    p->pGia->vMapping = Spl_ManFromWecMapping( p->pGia, p->pGia->vMapping2 );
+    Vec_WecFreeP( &p->pGia->vMapping2 );
     // intermediate
     Vec_BitFree( p->vMarksCIO );
     Vec_BitFree( p->vMarksIn );
     Vec_BitFree( p->vMarksNo );
+    Vec_BitFree( p->vMarksAnd );
     Vec_IntFree( p->vRoots );
     Vec_IntFree( p->vNodes );
     Vec_IntFree( p->vLeaves );
+    Vec_IntFree( p->vAnds );
     // temporary 
     Vec_IntFree( p->vFanouts );
     Vec_IntFree( p->vCands );
@@ -123,31 +183,55 @@ void Spl_ManStop( Spl_Man_t * p )
 ***********************************************************************/
 void Spl_ManWinFindLeavesRoots( Spl_Man_t * p )
 {
+    Vec_Int_t * vVec;
     int iObj, iFan, i, k;
     // collect leaves
+/*
     Vec_IntClear( p->vLeaves );
-    Vec_IntForEachEntry( p->vNodes, iObj, i )
+    Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i )
     {
         assert( Vec_BitEntry(p->vMarksNo, iObj) );
-        Gia_LutForEachFanin( p->pGia, iObj, iFan, k )
+        Vec_IntForEachEntry( vVec, iFan, k )
             if ( !Vec_BitEntry(p->vMarksNo, iFan) )
             {
                 Vec_BitWriteEntry(p->vMarksNo, iFan, 1);
                 Vec_IntPush( p->vLeaves, iFan );
             }
     }
-    Vec_IntForEachEntry( p->vLeaves, iObj, i )
-        Vec_BitWriteEntry(p->vMarksNo, iObj, 0);
+    Vec_IntForEachEntry( p->vLeaves, iFan, i )
+        Vec_BitWriteEntry(p->vMarksNo, iFan, 0);
+*/
+    Vec_IntClear( p->vLeaves );
+    Vec_IntForEachEntry( p->vAnds, iObj, i )
+    {
+        Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj );
+        assert( Vec_BitEntry(p->vMarksAnd, iObj) );
+        iFan = Gia_ObjFaninId0( pObj, iObj );
+        if ( !Vec_BitEntry(p->vMarksAnd, iFan) )
+        {
+            Vec_BitWriteEntry(p->vMarksAnd, iFan, 1);
+            Vec_IntPush( p->vLeaves, iFan );
+        }
+        iFan = Gia_ObjFaninId1( pObj, iObj );
+        if ( !Vec_BitEntry(p->vMarksAnd, iFan) )
+        {
+            Vec_BitWriteEntry(p->vMarksAnd, iFan, 1);
+            Vec_IntPush( p->vLeaves, iFan );
+        }
+    }
+    Vec_IntForEachEntry( p->vLeaves, iFan, i )
+        Vec_BitWriteEntry(p->vMarksAnd, iFan, 0);
+
     // collect roots
     Vec_IntClear( p->vRoots );
-    Vec_IntForEachEntry( p->vNodes, iObj, i )
-        Gia_LutForEachFanin( p->pGia, iObj, iFan, k )
+    Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i )
+        Vec_IntForEachEntry( vVec, iFan, k )
             Gia_ObjLutRefDecId( p->pGia, iFan );
-    Vec_IntForEachEntry( p->vNodes, iObj, i )
+    Vec_IntForEachEntry( p->vAnds, iObj, i )
         if ( Gia_ObjLutRefNumId(p->pGia, iObj) )
             Vec_IntPush( p->vRoots, iObj );
-    Vec_IntForEachEntry( p->vNodes, iObj, i )
-        Gia_LutForEachFanin( p->pGia, iObj, iFan, k )
+    Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i )
+        Vec_IntForEachEntry( vVec, iFan, k )
             Gia_ObjLutRefIncId( p->pGia, iFan );
 }
 
@@ -170,7 +254,7 @@ void Spl_ManLutFanouts_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vFanouts, Vec_B
     int iFanout, i;
     if ( Vec_BitEntry(vMarksNo, iObj) || Vec_BitEntry(vMarksCIO, iObj) )
         return;
-    if ( Gia_ObjIsLut(p, iObj) )
+    if ( Gia_ObjIsLut2(p, iObj) )
     {
         Vec_BitWriteEntry( vMarksCIO, iObj, 1 );
         Vec_IntPush( vFanouts, iObj );
@@ -182,7 +266,7 @@ void Spl_ManLutFanouts_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vFanouts, Vec_B
 int Spl_ManLutFanouts( Gia_Man_t * p, int iObj, Vec_Int_t * vFanouts, Vec_Bit_t * vMarksNo, Vec_Bit_t * vMarksCIO )
 {
     int i, iFanout;
-    assert( Gia_ObjIsLut(p, iObj) );
+    assert( Gia_ObjIsLut2(p, iObj) );
     Vec_IntClear( vFanouts );
     Gia_ObjForEachFanoutStaticId( p, iObj, iFanout, i )
         Spl_ManLutFanouts_rec( p, iFanout, vFanouts, vMarksNo, vMarksCIO );
@@ -195,30 +279,7 @@ int Spl_ManLutFanouts( Gia_Man_t * p, int iObj, Vec_Int_t * vFanouts, Vec_Bit_t
 
 /**Function*************************************************************
 
-  Synopsis    [Compute MFFC size of one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Spl_ManLutMffcSize( Gia_Man_t * p, int iObj )
-{
-    int Res, iFan, i;
-    assert( Gia_ObjIsLut(p, iObj) );
-    Gia_LutForEachFanin( p, iObj, iFan, i )
-        Gia_ObjRefIncId( p, iFan );
-    Res = Gia_NodeMffcSize( p, Gia_ManObj(p, iObj) );
-    Gia_LutForEachFanin( p, iObj, iFan, i )
-        Gia_ObjRefDecId( p, iFan );
-    return Res;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the number of fanins not beloning to the set.]
+  Synopsis    [Returns the number of fanins beloning to the set.]
 
   Description []
                
@@ -229,8 +290,9 @@ int Spl_ManLutMffcSize( Gia_Man_t * p, int iObj )
 ***********************************************************************/
 int Spl_ManCountMarkedFanins( Gia_Man_t * p, int iObj, Vec_Bit_t * vMarks )
 {
-    int k, iFan, Count = 0;
-    Gia_LutForEachFanin( p, iObj, iFan, k )
+    int i, iFan, Count = 0;
+    Vec_Int_t * vFanins = Gia_ObjLutFanins2(p, iObj);
+    Vec_IntForEachEntry( vFanins, iFan, i )
         if ( Vec_BitEntry(vMarks, iFan) )
             Count++;
     return Count;
@@ -249,27 +311,46 @@ int Spl_ManCountMarkedFanins( Gia_Man_t * p, int iObj, Vec_Bit_t * vMarks )
 ***********************************************************************/
 int Spl_ManFindOne( Spl_Man_t * p )
 {
+    Vec_Int_t * vVec;
     int nFanouts, iObj, iFan, i, k;
     int Res = 0, InCount, InCountMax = -1; 
     Vec_IntClear( p->vCands );
     Vec_IntClear( p->vInputs );
     // deref
-    Vec_IntForEachEntry( p->vNodes, iObj, i )
-        Gia_LutForEachFanin( p->pGia, iObj, iFan, k )
+    Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i )
+        Vec_IntForEachEntry( vVec, iFan, k )
             Gia_ObjLutRefDecId( p->pGia, iFan );
     // consider LUT inputs - get one that has no refs
-    Vec_IntForEachEntry( p->vNodes, iObj, i )
-        Gia_LutForEachFanin( p->pGia, iObj, iFan, k )
-            if ( !Vec_BitEntry(p->vMarksNo, iFan) && !Vec_BitEntry(p->vMarksCIO, iFan) )
-            {
-                if ( !Gia_ObjLutRefNumId(p->pGia, iFan) )
+    if ( p->fReverse )
+    {
+        Gia_ManForEachLut2VecReverse( p->vNodes, p->pGia, vVec, iObj, i )
+            Vec_IntForEachEntry( vVec, iFan, k )
+                if ( !Vec_BitEntry(p->vMarksNo, iFan) && !Vec_BitEntry(p->vMarksCIO, iFan) )
                 {
-                    Res = iFan;
-                    goto finish;
+                    if ( !Gia_ObjLutRefNumId(p->pGia, iFan) )
+                    {
+                        Res = iFan;
+                        goto finish;
+                    }
+                    Vec_IntPush( p->vCands, iFan );
+                    Vec_IntPush( p->vInputs, iFan );
                 }
-                Vec_IntPush( p->vCands, iFan );
-                Vec_IntPush( p->vInputs, iFan );
-            }
+    }
+    else
+    {
+        Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i )
+            Vec_IntForEachEntry( vVec, iFan, k )
+                if ( !Vec_BitEntry(p->vMarksNo, iFan) && !Vec_BitEntry(p->vMarksCIO, iFan) )
+                {
+                    if ( !Gia_ObjLutRefNumId(p->pGia, iFan) )
+                    {
+                        Res = iFan;
+                        goto finish;
+                    }
+                    Vec_IntPush( p->vCands, iFan );
+                    Vec_IntPush( p->vInputs, iFan );
+                }
+    }
 
     // all inputs have refs - collect external nodes
     Vec_IntForEachEntry( p->vNodes, iObj, i )
@@ -277,7 +358,7 @@ int Spl_ManFindOne( Spl_Man_t * p )
         if ( Gia_ObjLutRefNumId(p->pGia, iObj) == 0 )
             continue;
         assert( Gia_ObjLutRefNumId(p->pGia, iObj) > 0 );
-        if ( Gia_ObjLutRefNumId(p->pGia, iObj) >= 5 )
+        if ( Gia_ObjLutRefNumId(p->pGia, iObj) >= 5 )  // skip nodes with high fanout!
             continue;
         nFanouts = Spl_ManLutFanouts( p->pGia, iObj, p->vFanouts, p->vMarksNo, p->vMarksCIO );
         if ( Gia_ObjLutRefNumId(p->pGia, iObj) == 1 && nFanouts == 1 )
@@ -310,9 +391,9 @@ int Spl_ManFindOne( Spl_Man_t * p )
         Res = Vec_IntEntry( p->vCands, 0 );
 
 finish:
-    // deref
-    Vec_IntForEachEntry( p->vNodes, iObj, i )
-        Gia_LutForEachFanin( p->pGia, iObj, iFan, k )
+    // ref
+    Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i )
+        Vec_IntForEachEntry( vVec, iFan, k )
             Gia_ObjLutRefIncId( p->pGia, iFan );
     return Res;
 }
@@ -321,7 +402,7 @@ finish:
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Computing window for one pivot node.]
 
   Description []
                
@@ -330,50 +411,137 @@ finish:
   SeeAlso     []
 
 ***********************************************************************/
-void Spl_ManComputeOne( Spl_Man_t * p, int iPivot )
+int Spl_ManLutMffcSize( Gia_Man_t * p, int iObj, Vec_Int_t * vTemp, Vec_Bit_t * vMarksAnd )
+{
+    int iTemp, i, k = 0;
+    assert( Gia_ObjIsLut2(p, iObj) );
+//Vec_IntPrint( Gia_ObjLutFanins2(p, iObj) );
+    Gia_ManIncrementTravId( p );
+    Gia_ManCollectAnds( p, &iObj, 1, vTemp, Gia_ObjLutFanins2(p, iObj) );
+    Vec_IntForEachEntry( vTemp, iTemp, i )
+        if ( !Vec_BitEntry(vMarksAnd, iTemp) )
+            Vec_IntWriteEntry( vTemp, k++, iTemp );
+    Vec_IntShrink( vTemp, k );
+    return k;
+}
+void Spl_ManAddNode( Spl_Man_t * p, int iPivot, Vec_Int_t * vCands )
+{
+    int i, iObj;
+    Vec_IntPush( p->vNodes, iPivot );
+    Vec_BitWriteEntry( p->vMarksNo, iPivot, 1 );
+    Vec_IntAppend( p->vAnds, vCands );
+    Vec_IntForEachEntry( vCands, iObj, i )
+        Vec_BitWriteEntry( p->vMarksAnd, iObj, 1 );
+}
+int Spl_ManComputeOne( Spl_Man_t * p, int iPivot )
 {
     int CountAdd, iObj, i;
-    assert( Gia_ObjIsLut(p->pGia, iPivot) );
+    assert( Gia_ObjIsLut2(p->pGia, iPivot) );
+//Gia_ManPrintCone2( p->pGia, Gia_ManObj(p->pGia, iPivot) );
     // assume it was previously filled in
     Vec_IntForEachEntry( p->vNodes, iObj, i )
         Vec_BitWriteEntry( p->vMarksNo, iObj, 0 );
+    Vec_IntForEachEntry( p->vAnds, iObj, i )
+        Vec_BitWriteEntry( p->vMarksAnd, iObj, 0 );
     // double check that it is empty
-    //Gia_ManForEachLut( p->pGia, iObj )
+    //Gia_ManForEachLut2( p->pGia, iObj )
     //    assert( !Vec_BitEntry(p->vMarksNo, iObj) );
+    //Gia_ManForEachLut2( p->pGia, iObj )
+    //    assert( !Vec_BitEntry(p->vMarksAnd, iObj) );
+    // clean arrays
+    Vec_IntClear( p->vNodes );
+    Vec_IntClear( p->vAnds );
     // add root node
-    Vec_IntFill( p->vNodes, 1, iPivot );
-    Vec_BitWriteEntry( p->vMarksNo, iPivot, 1 );
+    Spl_ManLutMffcSize( p->pGia, iPivot, p->vCands, p->vMarksAnd );
+    Spl_ManAddNode( p, iPivot, p->vCands );
+    if ( Vec_IntSize(p->vAnds) > p->Limit )
+        return 0;
     //printf( "%d ", iPivot );
     // add one node at a time
-    p->Count = Spl_ManLutMffcSize( p->pGia, iPivot );
     while ( (iObj = Spl_ManFindOne(p)) )
     {
-        assert( Gia_ObjIsLut(p->pGia, iObj) );
-        CountAdd = Spl_ManLutMffcSize( p->pGia, iObj );
-        if ( p->Count + CountAdd > p->Limit )
+        assert( Gia_ObjIsLut2(p->pGia, iObj) );
+        assert( !Vec_BitEntry(p->vMarksNo, iObj) );
+        CountAdd = Spl_ManLutMffcSize( p->pGia, iObj, p->vCands, p->vMarksAnd );
+        if ( Vec_IntSize(p->vAnds) + CountAdd > p->Limit )
             break;
-        p->Count += CountAdd;
-        Vec_IntPush( p->vNodes, iObj );
-        Vec_BitWriteEntry( p->vMarksNo, iObj, 1 );
+        Spl_ManAddNode( p, iObj, p->vCands );
         //printf( "+%d ", iObj );
     }
     //printf( "\n" );
     Vec_IntSort( p->vNodes, 0 );
+    Vec_IntSort( p->vAnds, 0 );
+    Spl_ManWinFindLeavesRoots( p );
+    Vec_IntSort( p->vLeaves, 0 );
+    Vec_IntSort( p->vRoots, 0 );
+    return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [External procedures.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManComputeOneWin( Gia_Man_t * pGia, int iPivot, Vec_Int_t ** pvRoots, Vec_Int_t ** pvNodes, Vec_Int_t ** pvLeaves, Vec_Int_t ** pvAnds )
+{
+    Spl_Man_t * p = (Spl_Man_t *)pGia->pSatlutWinman;
+    assert( p != NULL );
+    if ( iPivot == -1 )
+    {
+        Spl_ManStop( p );
+        pGia->pSatlutWinman = NULL;
+        return 0;
+    }
+    if ( !Spl_ManComputeOne( p, iPivot ) )
+    {
+        *pvRoots  = NULL;
+        *pvNodes  = NULL;
+        *pvLeaves = NULL;
+        *pvAnds   = NULL;
+        return 0;
+    }
+    *pvRoots  = p->vRoots;
+    *pvNodes  = p->vNodes;
+    *pvLeaves = p->vLeaves;
+    *pvAnds   = p->vAnds;
+    // Vec_IntPrint( p->vNodes );
+    return Vec_IntSize(p->vAnds);
+}
+void Gia_ManComputeOneWinStart( Gia_Man_t * pGia, int fReverse )
+{
+    assert( pGia->pSatlutWinman == NULL );
+    pGia->pSatlutWinman = Spl_ManAlloc( pGia, 64, fReverse );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Testing procedure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Spl_ManComputeOneTest( Gia_Man_t * pGia )
 {
-    int iLut;
-    Spl_Man_t * p = Spl_ManAlloc( pGia, 64 );
-    Gia_ManForEachLut( pGia, iLut )
+    int iLut, Count;
+    Gia_ManComputeOneWinStart( pGia, 0 );
+    Gia_ManForEachLut2( pGia, iLut )
     {
-        Spl_ManComputeOne( p, iLut );
-        Spl_ManWinFindLeavesRoots( p );
-        // Vec_IntPrint( p->vNodes );
+        Vec_Int_t * vRoots, * vNodes, * vLeaves, * vAnds;
+        Count = Gia_ManComputeOneWin( pGia, iLut, &vRoots, &vNodes, &vLeaves, &vAnds );
         printf( "Obj = %6d : Leaf = %2d.  Node = %2d.  Root = %2d.    AND = %3d.\n", 
-            iLut, Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vRoots), p->Count ); 
+            iLut, Vec_IntSize(vLeaves), Vec_IntSize(vNodes), Vec_IntSize(vRoots), Count ); 
     }
-    Spl_ManStop( p );
+    Gia_ManComputeOneWin( pGia, -1, NULL, NULL, NULL, NULL );
 }
 
 ////////////////////////////////////////////////////////////////////////