New MFS package.

6 files changed, 349 insertions, 125 deletions

diff --git a/src/misc/vec/vecWec.h b/src/misc/vec/vecWec.h
index ece7b0a1..a70d92ad 100644
--- a/src/misc/vec/vecWec.h
+++ b/src/misc/vec/vecWec.h
@@ -122,6 +122,11 @@ static inline void Vec_WecGrow( Vec_Wec_t * p, int nCapMin )
     memset( p->pArray + p->nCap, 0, sizeof(Vec_Int_t) * (nCapMin - p->nCap) );
     p->nCap   = nCapMin;
 }
+static inline void Vec_WecInit( Vec_Wec_t * p, int nSize )
+{
+    Vec_WecGrow( p, nSize );
+    p->nSize = nSize;
+}
 
 /**Function*************************************************************
 
@@ -314,12 +319,24 @@ static inline double Vec_WecMemory( Vec_Wec_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Vec_WecFree( Vec_Wec_t * p )
+static inline void Vec_WecZero( Vec_Wec_t * p )
+{
+    p->pArray = NULL;
+    p->nSize = 0;
+    p->nCap = 0;
+}
+static inline void Vec_WecErase( Vec_Wec_t * p )
 {
     int i;
     for ( i = 0; i < p->nCap; i++ )
         ABC_FREE( p->pArray[i].pArray );
     ABC_FREE( p->pArray );
+    p->nSize = 0;
+    p->nCap = 0;
+}
+static inline void Vec_WecFree( Vec_Wec_t * p )
+{
+    Vec_WecErase( p );
     ABC_FREE( p );
 }
 static inline void Vec_WecFreeP( Vec_Wec_t ** p )
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
index a8ff1e21..965d03cc 100644
--- a/src/opt/sfm/sfmCore.c
+++ b/src/opt/sfm/sfmCore.c
@@ -75,6 +75,8 @@ void Sfm_NtkPrepare( Sfm_Ntk_t * p )
     p->vNodes  = Vec_IntAlloc( 1000 );
     p->vTfo    = Vec_IntAlloc( 1000 );
     p->vDivs   = Vec_IntAlloc( 100 );
+    p->vDivIds = Vec_IntAlloc( 1000 );
+    p->vDiffs  = Vec_IntAlloc( 1000 );
     p->vLits   = Vec_IntAlloc( 100 );
     p->vClauses  = Vec_WecAlloc( 100 );
     p->vFaninMap = Vec_IntAlloc( 10 );
@@ -94,15 +96,19 @@ void Sfm_NtkPrepare( Sfm_Ntk_t * p )
 ***********************************************************************/
 int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
 {
-    int i;
+//    int i;
     p->pPars = pPars;
     Sfm_NtkPrepare( p );
+    Sfm_ComputeInterpolantCheck( p );
+/*
     Sfm_NtkForEachNode( p, i )
     {
-        printf( "Node %d:\n", i );
-        Sfm_PrintCnf( (Vec_Str_t *)Vec_WecEntry(p->vCnfs, i) );
-        printf( "\n" );
+//        printf( "Node %d:\n", i );
+//        Sfm_PrintCnf( (Vec_Str_t *)Vec_WecEntry(p->vCnfs, i) );
+//        printf( "\n" );
+        Sfm_NtkWindow( p, i, 1 );
     }
+*/
     return 0;
 }
 
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index d52b46e4..e2833121 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -55,33 +55,37 @@ struct Sfm_Ntk_t_
     int               nNodes;   // internal nodes
     int               nObjs;    // total objects
     // user data
-    Vec_Wec_t *       vFanins;  // fanins
     Vec_Str_t *       vFixed;   // persistent objects
     Vec_Wrd_t *       vTruths;  // truth tables
+    Vec_Wec_t         vFanins;  // fanins
     // attributes
-    Vec_Wec_t *       vFanouts; // fanouts
-    Vec_Int_t *       vLevels;  // logic level
-    Vec_Int_t         vTravIds; // traversal IDs
+    Vec_Wec_t         vFanouts; // fanouts
+    Vec_Int_t         vLevels;  // logic level
+    Vec_Int_t         vCounts;  // fanin counters
     Vec_Int_t         vId2Var;  // ObjId -> SatVar
     Vec_Int_t         vVar2Id;  // SatVar -> ObjId
     Vec_Wec_t *       vCnfs;    // CNFs
     Vec_Int_t *       vCover;   // temporary
+    // traversal IDs
+    Vec_Int_t         vTravIds; // traversal IDs
+    Vec_Int_t         vTravIds2;// traversal IDs
     int               nTravIds; // traversal IDs
+    int               nTravIds2;// traversal IDs
     // window
     int               iNode;
     Vec_Int_t *       vLeaves;  // leaves 
     Vec_Int_t *       vRoots;   // roots
     Vec_Int_t *       vNodes;   // internal
     Vec_Int_t *       vTfo;     // TFO (excluding iNode)
+    Vec_Int_t *       vDivs;    // divisors
     // SAT solving
     int               nSatVars; // the number of variables
     sat_solver *      pSat1;    // SAT solver for the on-set
     sat_solver *      pSat0;    // SAT solver for the off-set
     // intermediate data
-    Vec_Int_t *       vDivs;    // divisors
+    Vec_Int_t *       vDivIds;  // divisors indexes
     Vec_Int_t *       vLits;    // literals
-    Vec_Int_t *       vFani;    // iterator fanins
-    Vec_Int_t *       vFano;    // iterator fanouts
+    Vec_Int_t *       vDiffs;   // differences
     Vec_Wec_t *       vClauses; // CNF clauses for the node
     Vec_Int_t *       vFaninMap;// mapping fanins into their SAT vars
 };
@@ -89,26 +93,38 @@ struct Sfm_Ntk_t_
 #define SFM_SAT_UNDEC 0x1234567812345678
 #define SFM_SAT_SAT   0x8765432187654321
 
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
-////////////////////////////////////////////////////////////////////////
 
-#define Sfm_NtkForEachNode( p, i )                for ( i = p->nPis; i + p->nPos < p->nObjs; i++ )
-#define Sfm_NodeForEachFanin( p, Node, Fan, i )   for ( p->vFani = Vec_WecEntry(p->vFanins,  Node), i = 0; i < Vec_IntSize(p->vFani) && ((Fan = Vec_IntEntry(p->vFani, i)), 1); i++ )
-#define Sfm_NodeForEachFanout( p, Node, Fan, i )  for ( p->vFano = Vec_WecEntry(p->vFanouts, Node), i = 0; i < Vec_IntSize(p->vFani) && ((Fan = Vec_IntEntry(p->vFano, i)), 1); i++ )
+static inline int  Sfm_ObjIsPi( Sfm_Ntk_t * p, int i )                  { return i < p->nPis;                               }
+static inline int  Sfm_ObjIsPo( Sfm_Ntk_t * p, int i )                  { return i + p->nPos >= p->nObjs;                   }
+static inline int  Sfm_ObjIsNode( Sfm_Ntk_t * p, int i )                { return i >= p->nPis && i + p->nPos < p->nObjs;    }
+
+static inline Vec_Int_t * Sfm_ObjFiArray( Sfm_Ntk_t * p, int i )        { return Vec_WecEntry(&p->vFanins, i);              }
+static inline Vec_Int_t * Sfm_ObjFoArray( Sfm_Ntk_t * p, int i )        { return Vec_WecEntry(&p->vFanouts, i);             }
 
-static inline int  Sfm_ObjIsPi( Sfm_Ntk_t * p, int i )      { return i < p->nPis;                               }
-static inline int  Sfm_ObjIsPo( Sfm_Ntk_t * p, int i )      { return i + p->nPos < p->nObjs;                    }
-static inline int  Sfm_ObjIsNode( Sfm_Ntk_t * p, int i )    { return i >= p->nPis && i + p->nPos < p->nObjs;    }
+static inline int  Sfm_ObjFaninNum( Sfm_Ntk_t * p, int i )              { return Vec_IntSize(Sfm_ObjFiArray(p, i));         }
+static inline int  Sfm_ObjFanoutNum( Sfm_Ntk_t * p, int i )             { return Vec_IntSize(Sfm_ObjFoArray(p, i));         }
 
-static inline int  Sfm_ObjFaninNum( Sfm_Ntk_t * p, int i )  { return Vec_IntSize(Vec_WecEntry(p->vFanins, i));  }
-static inline int  Sfm_ObjFanoutNum( Sfm_Ntk_t * p, int i ) { return Vec_IntSize(Vec_WecEntry(p->vFanouts, i)); }
+static inline int  Sfm_ObjFanin( Sfm_Ntk_t * p, int i, int k )          { return Vec_IntEntry(Sfm_ObjFiArray(p, i), k);     }
+static inline int  Sfm_ObjFanout( Sfm_Ntk_t * p, int i, int k )         { return Vec_IntEntry(Sfm_ObjFoArray(p, i), k);     }
 
-static inline int  Sfm_ObjSatVar( Sfm_Ntk_t * p, int iObj )             { return Vec_IntEntry(&p->vId2Var, iObj);     }
+static inline int  Sfm_ObjSatVar( Sfm_Ntk_t * p, int iObj )             { return Vec_IntEntry(&p->vId2Var, iObj);           }
 static inline void Sfm_ObjSetSatVar( Sfm_Ntk_t * p, int iObj, int Num ) { assert(Sfm_ObjSatVar(p, iObj) == -1); Vec_IntWriteEntry(&p->vId2Var, iObj, Num);  Vec_IntWriteEntry(&p->vVar2Id, Num, iObj);                            }
 static inline void Sfm_ObjCleanSatVar( Sfm_Ntk_t * p, int Num )         { assert(Sfm_ObjSatVar(p, Vec_IntEntry(&p->vVar2Id, Num)) != -1); Vec_IntWriteEntry(&p->vId2Var, Vec_IntEntry(&p->vVar2Id, Num), Num);  Vec_IntWriteEntry(&p->vVar2Id, Num, -1);    }
 static inline void Sfm_NtkCleanVars( Sfm_Ntk_t * p, int nSize )         { int i; for ( i = 1; i < nSize; i++ )  Sfm_ObjCleanSatVar( p, i ); }
 
+static inline int  Sfm_ObjLevel( Sfm_Ntk_t * p, int iObj )              { return Vec_IntEntry(&p->vLevels, iObj);                           }
+
+static inline int  Sfm_ObjUpdateFaninCount( Sfm_Ntk_t * p, int iObj )   { return Vec_IntAddToEntry(&p->vCounts, iObj, -1);                  }
+static inline void Sfm_ObjResetFaninCount( Sfm_Ntk_t * p, int iObj )    { Vec_IntWriteEntry(&p->vCounts, iObj, Sfm_ObjFaninNum(p, iObj)-1); }
+
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+#define Sfm_NtkForEachNode( p, i )                for ( i = p->nPis; i + p->nPos < p->nObjs; i++ )
+#define Sfm_NodeForEachFanin( p, Node, Fan, i )   for ( i = 0; i < Sfm_ObjFaninNum(p, Node)  && ((Fan = Sfm_ObjFanin(p, Node, i)), 1);  i++ )
+#define Sfm_NodeForEachFanout( p, Node, Fan, i )  for ( i = 0; i < Sfm_ObjFanoutNum(p, Node) && ((Fan = Sfm_ObjFanout(p, Node, i)), 1); i++ )
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
@@ -124,7 +140,7 @@ extern Sfm_Ntk_t *  Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPo
 /*=== sfmSat.c ==========================================================*/
 extern word         Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_t * vDivs, Vec_Int_t * vLits, Vec_Int_t * vDiffs, int nBTLimit );
 /*=== sfmWin.c ==========================================================*/
-extern int          Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode );
+extern int          Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode, int fVerbose );
 extern void         Sfm_NtkWin2Sat( Sfm_Ntk_t * p );
 
 
diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c
index 602f6d75..d9b17799 100644
--- a/src/opt/sfm/sfmNtk.c
+++ b/src/opt/sfm/sfmNtk.c
@@ -72,13 +72,12 @@ void Sfm_CheckConsistency( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t *
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Wec_t * Sfm_CreateFanout( Vec_Wec_t * vFanins )
+void Sfm_CreateFanout( Vec_Wec_t * vFanins, Vec_Wec_t * vFanouts )
 {
-    Vec_Wec_t * vFanouts;
     Vec_Int_t * vArray;
     int i, k, Fanin;
     // count fanouts
-    vFanouts = Vec_WecStart( Vec_WecSize(vFanins) );
+    Vec_WecInit( vFanouts, Vec_WecSize(vFanins) );
     Vec_WecForEachLevel( vFanins, vArray, i )
         Vec_IntForEachEntry( vArray, Fanin, k )
             Vec_WecEntry( vFanouts, Fanin )->nSize++;
@@ -93,9 +92,8 @@ Vec_Wec_t * Sfm_CreateFanout( Vec_Wec_t * vFanins )
         Vec_IntForEachEntry( vArray, Fanin, k )
             Vec_IntPush( Vec_WecEntry( vFanouts, Fanin ), i );
     // verify
-    Vec_WecForEachLevel( vFanins, vArray, i )
+    Vec_WecForEachLevel( vFanouts, vArray, i )
         assert( Vec_IntSize(vArray) == Vec_IntCap(vArray) );
-    return vFanouts;
 }
 
 /**Function*************************************************************
@@ -109,17 +107,15 @@ Vec_Wec_t * Sfm_CreateFanout( Vec_Wec_t * vFanins )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Sfm_CreateLevel( Vec_Wec_t * vFanins )
+void Sfm_CreateLevel( Vec_Wec_t * vFanins, Vec_Int_t * vLevels )
 {
-    Vec_Int_t * vLevels;
     Vec_Int_t * vArray;
     int i, k, Fanin, * pLevels;
-    vLevels = Vec_IntStart( Vec_WecSize(vFanins) );
+    Vec_IntFill( vLevels, Vec_WecSize(vFanins), 0 );
     pLevels = Vec_IntArray( vLevels );
     Vec_WecForEachLevel( vFanins, vArray, i )
         Vec_IntForEachEntry( vArray, Fanin, k )
             pLevels[i] = Abc_MaxInt( pLevels[i], pLevels[Fanin] + 1 );
-    return vLevels;
 }
 
 /**Function*************************************************************
@@ -143,7 +139,7 @@ Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p )
     vCnfs = Vec_WecStart( p->nObjs );
     Vec_WrdForEachEntryStartStop( p->vTruths, uTruth, i, p->nPis, Vec_WrdSize(p->vTruths)-p->nPos )
     {
-        Sfm_TruthToCnf( uTruth, Vec_IntSize(Vec_WecEntry(p->vFanins, i)), p->vCover, vCnf );
+        Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, i), p->vCover, vCnf );
         vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, i );
         Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) );
         memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), Vec_StrSize(vCnf) );
@@ -173,14 +169,17 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
     p->nPis     = nPis;
     p->nPos     = nPos;
     p->nNodes   = p->nObjs - p->nPis - p->nPos;
-    p->vFanins  = vFanins;
     // user data
     p->vFixed   = vFixed;
     p->vTruths  = vTruths;
+    p->vFanins  = *vFanins;
+    ABC_FREE( vFanins );
     // attributes
-    p->vFanouts = Sfm_CreateFanout( vFanins );
-    p->vLevels  = Sfm_CreateLevel( vFanins );
+    Sfm_CreateFanout( &p->vFanins, &p->vFanouts );
+    Sfm_CreateLevel( &p->vFanins, &p->vLevels );
+    Vec_IntFill( &p->vCounts, p->nObjs, 0 );
     Vec_IntFill( &p->vTravIds, p->nObjs, 0 );
+    Vec_IntFill( &p->vTravIds2, p->nObjs, 0 );
     Vec_IntFill( &p->vId2Var, p->nObjs, -1 );
     Vec_IntFill( &p->vVar2Id, p->nObjs, -1 );
     p->vCover   = Vec_IntAlloc( 1 << 16 );
@@ -190,13 +189,15 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
 void Sfm_NtkFree( Sfm_Ntk_t * p )
 {
     // user data
-    Vec_WecFree( p->vFanins );
     Vec_StrFree( p->vFixed );
     Vec_WrdFree( p->vTruths );
+    Vec_WecErase( &p->vFanins );
     // attributes
-    Vec_WecFree( p->vFanouts );
-    Vec_IntFree( p->vLevels );
+    Vec_WecErase( &p->vFanouts );
+    ABC_FREE( p->vLevels.pArray );
+    ABC_FREE( p->vCounts.pArray );
     ABC_FREE( p->vTravIds.pArray );
+    ABC_FREE( p->vTravIds2.pArray );
     ABC_FREE( p->vId2Var.pArray );
     ABC_FREE( p->vVar2Id.pArray );
     Vec_WecFree( p->vCnfs );
@@ -207,7 +208,9 @@ void Sfm_NtkFree( Sfm_Ntk_t * p )
     Vec_IntFreeP( &p->vNodes );
     Vec_IntFreeP( &p->vTfo   );
     Vec_IntFreeP( &p->vDivs  );
+    Vec_IntFreeP( &p->vDivIds );
     Vec_IntFreeP( &p->vLits  );
+    Vec_IntFreeP( &p->vDiffs  );
     Vec_WecFreeP( &p->vClauses );
     Vec_IntFreeP( &p->vFaninMap );
     if ( p->pSat0 ) sat_solver_delete( p->pSat0 );
@@ -228,7 +231,7 @@ void Sfm_NtkFree( Sfm_Ntk_t * p )
 ***********************************************************************/
 Vec_Int_t *  Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i )
 {
-    return Vec_WecEntry( p->vFanins, i );
+    return Vec_WecEntry( &p->vFanins, i );
 }
 word Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i )
 {
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c
index 6431cd50..3ad97503 100644
--- a/src/opt/sfm/sfmSat.c
+++ b/src/opt/sfm/sfmSat.c
@@ -42,6 +42,78 @@ static word s_Truths6[6] = {
 
 /**Function*************************************************************
 
+  Synopsis    [Converts a window into a SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sfm_NtkWin2Sat( Sfm_Ntk_t * p )
+{
+    Vec_Int_t * vClause;
+    int RetValue, Lit, iNode = -1, iFanin, i, k, c;
+    sat_solver * pSat0 = sat_solver_new();
+    sat_solver * pSat1 = sat_solver_new();
+    sat_solver_setnvars( pSat0, 1 + Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) );
+    sat_solver_setnvars( pSat1, 1 + Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) );
+    // create SAT variables
+    p->nSatVars = 1;
+    Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
+        Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
+    Vec_IntForEachEntryReverse( p->vLeaves, iNode, i )
+        Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
+    Vec_IntForEachEntryReverse( p->vDivs, iNode, i )
+        Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
+    // add CNF clauses
+    for ( c = 0; c < 2; c++ )
+    {
+        Vec_Int_t * vObjs = c ? p->vDivs : p->vNodes;
+        Vec_IntForEachEntryReverse( vObjs, iNode, i )
+        {
+            // collect fanin variables
+            Vec_IntClear( p->vFaninMap );
+            Sfm_NodeForEachFanin( p, iNode, iFanin, k )
+                Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iFanin) );
+            Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iNode) );
+            // generate CNF 
+            Sfm_TranslateCnf( p->vClauses, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode), p->vFaninMap );
+            // add clauses
+            Vec_WecForEachLevel( p->vClauses, vClause, k )
+            {
+                if ( Vec_IntSize(vClause) == 0 )
+                    break;
+                RetValue = sat_solver_addclause( pSat0, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
+                assert( RetValue );
+                RetValue = sat_solver_addclause( pSat1, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
+                assert( RetValue );
+            }
+        }
+    }
+    // get the last node
+    iNode = Vec_IntEntryLast( p->vNodes );
+    // add unit clause
+    Lit = Abc_Var2Lit( Sfm_ObjSatVar(p, iNode), 1 );
+    RetValue = sat_solver_addclause( pSat0, &Lit, &Lit + 1 );
+    assert( RetValue );
+    // add unit clause
+    Lit = Abc_Var2Lit( Sfm_ObjSatVar(p, iNode), 0 );
+    RetValue = sat_solver_addclause( pSat1, &Lit, &Lit + 1 );
+    assert( RetValue );
+    // finalize
+    sat_solver_compress( pSat0 );
+    sat_solver_compress( pSat1 );
+    // return the result
+    assert( p->pSat0 == NULL );
+    assert( p->pSat1 == NULL );
+    p->pSat0 = pSat0;
+    p->pSat1 = pSat1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Takes SAT solver and returns interpolant.]
 
   Description [If interpolant does not exist, returns diff SAT variables.]
@@ -51,12 +123,14 @@ static word s_Truths6[6] = {
   SeeAlso     []
 
 ***********************************************************************/
-word Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_t * vDivs, Vec_Int_t * vLits, Vec_Int_t * vDiffs, int nBTLimit )
+word Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_t * vDivIds, Vec_Int_t * vLits, Vec_Int_t * vDiffs, int nBTLimit )
 {
     word uTruth = 0, uCube;
     int status, i, Div, iVar, nFinal, * pFinal;
     int nVars = sat_solver_nvars(pSatOn);
     int iNewLit = Abc_Var2Lit( nVars, 0 );
+    int RetValue;
+    sat_solver_setnvars( pSatOn, nVars + 1 );
     while ( 1 ) 
     {
         // find onset minterm
@@ -68,8 +142,9 @@ word Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_
         assert( status == l_True );
         // collect literals
         Vec_IntClear( vLits );
-        Vec_IntForEachEntry( vDivs, Div, i )
-            Vec_IntPush( vLits, Abc_LitNot(sat_solver_var_literal(pSatOn, Div)) );
+        Vec_IntForEachEntry( vDivIds, Div, i )
+//            Vec_IntPush( vLits, Abc_LitNot(sat_solver_var_literal(pSatOn, Div)) );
+            Vec_IntPush( vLits, sat_solver_var_literal(pSatOn, Div) );
         // check against offset
         status = sat_solver_solve( pSatOff, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
         if ( status == l_Undef )
@@ -90,16 +165,60 @@ word Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_
         for ( i = 0; i < nFinal; i++ )
         {
             Vec_IntPush( vLits, pFinal[i] );
-            iVar = Vec_IntFind( vDivs, Abc_Lit2Var(pFinal[i]) );   assert( iVar >= 0 );
+            iVar = Vec_IntFind( vDivIds, Abc_Lit2Var(pFinal[i]) );   assert( iVar >= 0 );
             uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
         }
         uTruth |= uCube;
-        sat_solver_addclause( pSatOn, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+        RetValue = sat_solver_addclause( pSatOn, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+        assert( RetValue );
     }
     assert( 0 );
     return 0;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Checks resubstitution.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sfm_ComputeInterpolantCheck( Sfm_Ntk_t * p )
+{
+    int iNode = 3;
+    int iDiv0 = 6;
+    int iDiv1 = 7;
+    word uTruth;
+//    int i;
+//    Sfm_NtkForEachNode( p, i )
+    {
+        Sfm_NtkWindow( p, iNode, 1 );
+        Sfm_NtkWin2Sat( p );
+
+        // collect SAT variables of divisors
+        Vec_IntClear( p->vDivIds );
+        Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, iDiv0) );
+        Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, iDiv1) );
+
+        uTruth = Sfm_ComputeInterpolant( p->pSat1, p->pSat0, p->vDivIds, p->vLits, p->vDiffs, 0 );
+
+        if ( uTruth == SFM_SAT_SAT )
+            printf( "The problem is SAT.\n" );
+        else if ( uTruth == SFM_SAT_UNDEC )
+            printf( "The problem is UNDEC.\n" );
+        else
+            Kit_DsdPrintFromTruth( (unsigned *)&uTruth, 2 ); printf( "\n" );
+
+        Sfm_NtkCleanVars( p, p->nSatVars );
+        sat_solver_delete( p->pSat0 );  p->pSat0 = NULL;
+        sat_solver_delete( p->pSat1 );  p->pSat1 = NULL;
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c
index c8f0af61..078406ba 100644
--- a/src/opt/sfm/sfmWin.c
+++ b/src/opt/sfm/sfmWin.c
@@ -42,9 +42,103 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-static inline void  Sfm_NtkIncrementTravId( Sfm_Ntk_t * p )            { p->nTravIds++;                                           }       
-static inline void  Sfm_ObjSetTravIdCurrent( Sfm_Ntk_t * p, int Id )   { Vec_IntWriteEntry( &p->vTravIds, Id, p->nTravIds );      }
-static inline int   Sfm_ObjIsTravIdCurrent( Sfm_Ntk_t * p, int Id )    { return (Vec_IntEntry(&p->vTravIds, Id) == p->nTravIds);  }   
+static inline void  Sfm_NtkIncrementTravId( Sfm_Ntk_t * p )            { p->nTravIds++;                                            }       
+static inline void  Sfm_ObjSetTravIdCurrent( Sfm_Ntk_t * p, int Id )   { Vec_IntWriteEntry( &p->vTravIds, Id, p->nTravIds );       }
+static inline int   Sfm_ObjIsTravIdCurrent( Sfm_Ntk_t * p, int Id )    { return (Vec_IntEntry(&p->vTravIds, Id) == p->nTravIds);   }   
+
+static inline void  Sfm_NtkIncrementTravId2( Sfm_Ntk_t * p )           { p->nTravIds2++;                                           }       
+static inline void  Sfm_ObjSetTravIdCurrent2( Sfm_Ntk_t * p, int Id )  { Vec_IntWriteEntry( &p->vTravIds2, Id, p->nTravIds2 );     }
+static inline int   Sfm_ObjIsTravIdCurrent2( Sfm_Ntk_t * p, int Id )   { return (Vec_IntEntry(&p->vTravIds2, Id) == p->nTravIds2); }   
+
+
+/**Function*************************************************************
+
+  Synopsis    [Check if this fanout overlaps with TFI cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sfm_NtkCheckOverlap_rec( Sfm_Ntk_t * p, int iThis, int iNode )
+{
+    int i, iFanin;
+    if ( Sfm_ObjIsTravIdCurrent2(p, iThis) || iThis == iNode )
+        return 0;
+    if ( Sfm_ObjIsTravIdCurrent(p, iThis) )
+        return 1;
+    Sfm_ObjSetTravIdCurrent2(p, iThis);
+    Sfm_NodeForEachFanin( p, iThis, iFanin, i )
+        if ( Sfm_NtkCheckOverlap_rec(p, iFanin, iNode) )
+            return 1;
+    return 0;
+}
+int Sfm_NtkCheckOverlap( Sfm_Ntk_t * p, int iFan, int iNode )
+{
+    Sfm_NtkIncrementTravId2( p );
+    return Sfm_NtkCheckOverlap_rec( p, iFan, iNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Check fanouts of the node.]
+
+  Description [Returns 1 if they can be used instead of the node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sfm_NtkCheckFanouts( Sfm_Ntk_t * p, int iNode )
+{
+    int i, iFanout;
+    if ( Sfm_ObjFanoutNum(p, iNode) >= p->pPars->nFanoutMax )
+        return 0;
+    Sfm_NodeForEachFanout( p, iNode, iFanout, i )
+        if ( !Sfm_NtkCheckOverlap( p, iFanout, iNode ) )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects divisors of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode )
+{
+    int i, iFanout;
+    Sfm_NodeForEachFanout( p, iNode, iFanout, i )
+    {
+        // skip TFI nodes, PO nodes, and nodes with high fanout or nodes with high logic level
+        if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) || 
+            Sfm_ObjFanoutNum(p, iFanout) >= p->pPars->nFanoutMax ||
+            (p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) >= Sfm_ObjLevel(p, iNode)) )
+            continue;
+        // handle single-input nodes
+        if ( Sfm_ObjFaninNum(p, iFanout) == 1 )
+            Vec_IntPush( p->vDivs, iFanout );
+        // visit node for the first time
+        else if ( !Sfm_ObjIsTravIdCurrent2(p, iFanout) )
+        {
+            assert( Sfm_ObjFaninNum(p, iFanout) > 1 );
+            Sfm_ObjSetTravIdCurrent2( p, iFanout );
+            Sfm_ObjResetFaninCount( p, iFanout );
+        }
+        // visit node again
+        else if ( Sfm_ObjUpdateFaninCount(p, iFanout) == 0 )
+            Vec_IntPush( p->vDivs, iFanout );
+    }
+}
 
 /**Function*************************************************************
 
@@ -72,94 +166,63 @@ void Sfm_NtkCollectTfi_rec( Sfm_Ntk_t * p, int iNode )
         Sfm_NtkCollectTfi_rec( p, iFanin );
     Vec_IntPush( p->vNodes, iNode );
 }
-int Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode )
+int Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
 {
-//    int i, iRoot;
+    int i, iTemp;
+/*
+    if ( iNode == 7 )
+    {
+        int iLevel = Sfm_ObjLevel(p, iNode);
+        int s = 0;
+    }
+*/
     assert( Sfm_ObjIsNode( p, iNode ) );
-    Sfm_NtkIncrementTravId( p );
     Vec_IntClear( p->vLeaves ); // leaves 
     Vec_IntClear( p->vNodes );  // internal
     // collect transitive fanin
+    Sfm_NtkIncrementTravId( p );
     Sfm_NtkCollectTfi_rec( p, iNode );
-    // collect TFO
+    // collect TFO (currently use only one level of TFO)
     Vec_IntClear( p->vRoots );  // roots
     Vec_IntClear( p->vTfo );    // roots
-    Vec_IntPush( p->vRoots, iNode );
-/*
-    Vec_IntForEachEntry( p->vRoots, iRoot, i )
+    if ( Sfm_NtkCheckFanouts(p, iNode) )
     {
-        assert( Sfm_ObjIsNode(p, iRoot) );
-        if ( Sfm_ObjIsTravIdCurrent(p, iRoot) )
-            continue;
-        if ( Sfm_ObjFanoutNum(p, iRoot) >= p->pPars->nFanoutMax )
-            continue;
+        Sfm_NodeForEachFanout( p, iNode, iTemp, i )
+        {
+            if ( Sfm_ObjIsPo(p, iTemp) )
+                continue;
+            Vec_IntPush( p->vRoots, iTemp );
+            Vec_IntPush( p->vTfo, iTemp );
+        }
     }
-*/
+    else
+        Vec_IntPush( p->vRoots, iNode );
+    // collect divisors of the TFI nodes
+    Vec_IntClear( p->vDivs );
+    Sfm_NtkIncrementTravId2( p );
+    Vec_IntForEachEntry( p->vLeaves, iTemp, i )
+        Sfm_NtkAddDivisors( p, iTemp );
+    Vec_IntForEachEntry( p->vNodes, iTemp, i )
+        Sfm_NtkAddDivisors( p, iTemp );
+    Vec_IntForEachEntry( p->vDivs, iTemp, i )
+        Sfm_NtkAddDivisors( p, iTemp );
+    if ( !fVerbose )
+        return 1;
+
+    // print stats about the window
+    printf( "%6d : ", iNode );
+    printf( "Leaves = %5d. ", Vec_IntSize(p->vLeaves) );
+    printf( "Nodes = %5d. ",  Vec_IntSize(p->vNodes) );
+    printf( "Roots = %5d. ",  Vec_IntSize(p->vRoots) );
+    printf( "Divs = %5d. ",   Vec_IntSize(p->vDivs) );
+    printf( "\n" );
     return 1;
 }
-
-/**Function*************************************************************
-
-  Synopsis    [Converts a window into a SAT solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sfm_NtkWin2Sat( Sfm_Ntk_t * p )
+void Sfm_NtkWindowTest( Sfm_Ntk_t * p, int iNode )
 {
-    Vec_Int_t * vClause;
-    int RetValue, Lit, iNode = -1, iFanin, i, k;
-    sat_solver * pSat0 = sat_solver_new();
-    sat_solver * pSat1 = sat_solver_new();
-    sat_solver_setnvars( pSat0, 1 + Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) );
-    sat_solver_setnvars( pSat1, 1 + Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) );
-    // create SAT variables
-    p->nSatVars = 1;
-    Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
-        Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
-    Vec_IntForEachEntryReverse( p->vLeaves, iNode, i )
-        Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
-    // add CNF clauses
-    Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
-    {
-        // collect fanin variables
-        Vec_IntClear( p->vFaninMap );
-        Sfm_NodeForEachFanin( p, iNode, iFanin, k )
-            Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iFanin) );
-        Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iNode) );
-        // generate CNF 
-        Sfm_TranslateCnf( p->vClauses, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode), p->vFaninMap );
-        // add clauses
-        Vec_WecForEachLevel( p->vClauses, vClause, k )
-        {
-            if ( Vec_IntSize(vClause) == 0 )
-                break;
-            RetValue = sat_solver_addclause( pSat0, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
-            assert( RetValue );
-            RetValue = sat_solver_addclause( pSat1, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
-            assert( RetValue );
-        }
-    }
-    // add unit clause
-    Lit = Abc_Var2Lit( Sfm_ObjSatVar(p, iNode), 1 );
-    RetValue = sat_solver_addclause( pSat0, &Lit, &Lit + 1 );
-    assert( RetValue );
-    // add unit clause
-    Lit = Abc_Var2Lit( Sfm_ObjSatVar(p, iNode), 0 );
-    RetValue = sat_solver_addclause( pSat1, &Lit, &Lit + 1 );
-    assert( RetValue );
-    // finalize
-    sat_solver_compress( p->pSat0 );
-    sat_solver_compress( p->pSat1 );
-    // return the result
-    assert( p->pSat0 == NULL );
-    assert( p->pSat1 == NULL );
-    p->pSat0 = pSat0;
-    p->pSat1 = pSat1;
+    int i;
+    Sfm_NtkForEachNode( p, i )
+        Sfm_NtkWindow( p, i, 1 );
 }
 
 ////////////////////////////////////////////////////////////////////////