New MFS package.

9 files changed, 598 insertions, 180 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f8404f19..b5e1ebee 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -4469,7 +4469,7 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Sfm_ParSetDefault( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMClaevwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMNClaevwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -4517,6 +4517,17 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nWinSizeMax < 0 )
                 goto usage;
             break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nDivNumMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nDivNumMax < 0 )
+                goto usage;
+            break;
         case 'C':
             if ( globalUtilOptind >= argc )
             {
@@ -4573,12 +4584,13 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: mfs2 [-WFDMC <num>] [-laevwh]\n" );
+    Abc_Print( -2, "usage: mfs2 [-WFDMNC <num>] [-laevwh]\n" );
     Abc_Print( -2, "\t           performs don't-care-based optimization of logic networks\n" );
     Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevMax );
     Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutMax );
     Abc_Print( -2, "\t-D <num> : the max depth nodes to try (0 = no limit) [default = %d]\n", pPars->nDepthMax );
     Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );
+    Abc_Print( -2, "\t-N <num> : the max number of divisors to consider (0 = no limit) [default = %d]\n", pPars->nDivNumMax );
     Abc_Print( -2, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-l       : allow logic level to increase [default = %s]\n", !pPars->fFixLevel? "yes": "no" );
     Abc_Print( -2, "\t-a       : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index 54f40721..7e34e1c3 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -164,7 +164,7 @@ p->timeGia += clock() - clk;
 ***********************************************************************/
 int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove, int fSkipUpdate )
 {
-    int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;// || pNode->Id == 556;
+    int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 200;// || pNode->Id == 556;
     unsigned * pData;
     int pCands[MFS_FANIN_MAX];
     int RetValue, iVar, i, nCands, nWords, w;
@@ -176,9 +176,9 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
     // clean simulation info
     Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords ); 
     p->nCexes = 0;
-    if ( fVeryVerbose )
+    if ( p->pPars->fVeryVerbose )
     {
-        printf( "\n" );
+//        printf( "\n" );
         printf( "Node %5d : Level = %2d. Divs = %3d.  Fanin = %d (out of %d). MFFC = %d\n", 
             pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode), 
             iFanin, Abc_ObjFaninNum(pNode), 
@@ -201,8 +201,8 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
         return 0;
     if ( RetValue == 1 )
     {
-        if ( fVeryVerbose )
-        printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin );
+        if ( p->pPars->fVeryVerbose )
+            printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin );
         p->nNodesResub++;
         p->nNodesGainedLevel++;
         if ( fSkipUpdate )
@@ -223,7 +223,7 @@ p->timeInt += clock() - clk;
 
     if ( fVeryVerbose )
     {
-        for ( i = 0; i < 8; i++ )
+        for ( i = 0; i < 9; i++ )
             printf( " " );
         for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ )
             printf( "%d", i % 10 );
@@ -239,7 +239,7 @@ p->timeInt += clock() - clk;
     {
         if ( fVeryVerbose )
         {
-            printf( "%3d: %2d ", p->nCexes, iVar );
+            printf( "%3d: %3d ", p->nCexes, iVar );
             for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
             {
                 pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
@@ -276,8 +276,8 @@ p->timeInt += clock() - clk;
             return 0;
         if ( RetValue == 1 )
         {
-            if ( fVeryVerbose )
-            printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar );
+            if ( p->pPars->fVeryVerbose )
+                printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar );
             p->nNodesResub++;
             p->nNodesGainedLevel++;
             if ( fSkipUpdate )
@@ -296,6 +296,8 @@ p->timeInt += clock() - clk;
         if ( p->nCexes >= p->pPars->nDivMax )
             break;
     }
+    if ( p->pPars->fVeryVerbose )
+        printf( "Node %d: Cannot find replacement for fanin %d.\n", pNode->Id, iFanin );
     return 0;
 }
 
diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index deb055c5..5f266c68 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -45,7 +45,8 @@ struct Sfm_Par_t_
     int           nTfoLevMax;    // the maximum fanout levels
     int           nFanoutMax;    // the maximum number of fanouts
     int           nDepthMax;     // the maximum depth to try
-    int           nWinSizeMax;   // the maximum number of divisors
+    int           nDivNumMax;    // the maximum number of divisors
+    int           nWinSizeMax;   // the maximum window size
     int           nBTLimit;      // the maximum number of conflicts in one SAT run
     int           fFixLevel;     // does not allow level to increase
     int           fArea;         // performs optimization for area
diff --git a/src/opt/sfm/sfmCnf.c b/src/opt/sfm/sfmCnf.c
index 825c336b..09dce50c 100644
--- a/src/opt/sfm/sfmCnf.c
+++ b/src/opt/sfm/sfmCnf.c
@@ -117,6 +117,37 @@ int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf
   SeeAlso     []
 
 ***********************************************************************/
+Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p )
+{
+    Vec_Wec_t * vCnfs;
+    Vec_Str_t * vCnf, * vCnfBase;
+    word uTruth;
+    int i;
+    vCnf = Vec_StrAlloc( 100 );
+    vCnfs = Vec_WecStart( p->nObjs );
+    Vec_WrdForEachEntryStartStop( p->vTruths, uTruth, i, p->nPis, Vec_WrdSize(p->vTruths)-p->nPos )
+    {
+        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) );
+        vCnfBase->nSize = Vec_StrSize(vCnf);
+    }
+    Vec_StrFree( vCnf );
+    return vCnfs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap )
 {
     Vec_Int_t * vClause;
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
index 965d03cc..7d206fa2 100644
--- a/src/opt/sfm/sfmCore.c
+++ b/src/opt/sfm/sfmCore.c
@@ -47,8 +47,9 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
     memset( pPars, 0, sizeof(Sfm_Par_t) );
     pPars->nTfoLevMax   =    2;  // the maximum fanout levels
     pPars->nFanoutMax   =   10;  // the maximum number of fanouts
-    pPars->nDepthMax    =    0;  // the maximum depth to try
-    pPars->nWinSizeMax  =  500;  // the maximum number of divisors
+    pPars->nDepthMax    =    0;  // the maximum depth to try  
+    pPars->nDivNumMax   =  200;  // the maximum number of divisors
+    pPars->nWinSizeMax  =  500;  // the maximum window size
     pPars->nBTLimit     =    0;  // the maximum number of conflicts in one SAT run
     pPars->fFixLevel    =    0;  // does not allow level to increase
     pPars->fArea        =    0;  // performs optimization for area
@@ -62,26 +63,169 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
   Synopsis    []
 
   Description []
-               
+
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Sfm_NtkPrepare( Sfm_Ntk_t * p )
+void Sfm_NtkPrintStats( Sfm_Ntk_t * p )
 {
-    p->vLeaves = Vec_IntAlloc( 1000 );
-    p->vRoots  = Vec_IntAlloc( 1000 );
-    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 );
+    printf( "Attempts :  " );
+    printf( "Remove %5d (%6.2f%%)  ", p->nRemoves, 100.0*p->nRemoves/p->nTryRemoves );
+    printf( "Resub  %5d (%6.2f%%)  ", p->nResubs,  100.0*p->nResubs /p->nTryResubs  );
+    printf( "\n" );
+
+    printf( "Reduction:  " );
+    printf( "Nodes  %5d (%6.2f%%)  ", p->nTotalNodesBeg-p->nTotalNodesEnd, 100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/p->nTotalNodesBeg );
+    printf( "Edges  %5d (%6.2f%%)  ", p->nTotalEdgesBeg-p->nTotalEdgesEnd, 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg );
+    printf( "\n" );
+
+    ABC_PRTP( "Win", p->timeWin  ,  p->timeTotal );
+    ABC_PRTP( "Div", p->timeDiv  ,  p->timeTotal );
+    ABC_PRTP( "Cnf", p->timeCnf  ,  p->timeTotal );
+    ABC_PRTP( "Sat", p->timeSat  ,  p->timeTotal );
+    ABC_PRTP( "ALL", p->timeTotal,  p->timeTotal );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs resubstitution for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly )
+{
+    int fSkipUpdate  = 1;
+    int fVeryVerbose = p->pPars->fVeryVerbose && Vec_IntSize(p->vDivs) < 200;// || pNode->Id == 556;
+    int i, iFanin, iVar = -1;
+    word uTruth, uSign, uMask;
+    clock_t clk;
+    assert( Sfm_ObjIsNode(p, iNode) );
+    assert( f >= 0 && f < Sfm_ObjFaninNum(p, iNode) );
+    if ( fRemoveOnly )
+        p->nTryRemoves++;
+    else
+        p->nTryResubs++;
+    // report init stats
+    if ( p->pPars->fVeryVerbose )
+        printf( "Node %5d : Level = %2d. Divs = %3d.  Fanin = %d (out of %d). MFFC = %d\n", 
+            iNode, Sfm_ObjLevel(p, iNode), Vec_IntSize(p->vDivs), f, Sfm_ObjFaninNum(p, iNode), 
+            Sfm_ObjFanoutNum(p, Sfm_ObjFanin(p, iNode, f)) == 1 ? Sfm_ObjMffcSize(p, iNode) : 0 );
+    // clean simulation info
+    p->nCexes = 0;
+    Vec_WrdFill( p->vDivCexes, Vec_IntSize(p->vDivs), 0 );
+    // try removing the critical fanin
+clk = clock();
+    Vec_IntClear( p->vDivIds );
+    Sfm_ObjForEachFanin( p, iNode, iFanin, i )
+        if ( i != f )
+            Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, iFanin) );
+    uTruth = Sfm_ComputeInterpolant( p );
+p->timeSat += clock() - clk;
+    // analyze outcomes
+    if ( uTruth == SFM_SAT_UNDEC )
+        return 0;
+    if ( uTruth == SFM_SAT_SAT )
+        goto finish;
+    if ( fRemoveOnly )
+        return 0;
+    if ( fVeryVerbose )
+    {
+        for ( i = 0; i < 9; i++ )
+            printf( " " );
+        for ( i = 0; i < Vec_IntSize(p->vDivs); i++ )
+            printf( "%d", i % 10 );
+        printf( "\n" );
+    }
+    while ( 1 ) 
+    {
+        if ( fVeryVerbose )
+        {
+            printf( "%3d: %3d ", p->nCexes, iVar );
+            Vec_WrdForEachEntry( p->vDivCexes, uSign, i )
+                printf( "%d", Abc_InfoHasBit((unsigned *)&uSign, p->nCexes-1) );
+            printf( "\n" );
+        }
+        // find the next divisor to try
+        uMask = (~(word)0) >> (64 - p->nCexes);
+        Vec_WrdForEachEntry( p->vDivCexes, uSign, iVar )
+            if ( uSign == uMask )
+                break;
+        if ( iVar == Vec_IntSize(p->vDivs) )
+            return 0;
+        // try replacing the critical fanin
+clk = clock();
+        Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, Vec_IntEntry(p->vDivs, iVar)) );
+        uTruth = Sfm_ComputeInterpolant( p );
+p->timeSat += clock() - clk;
+        // analyze outcomes
+        if ( uTruth == SFM_SAT_UNDEC )
+            return 0;
+        if ( uTruth == SFM_SAT_SAT )
+            goto finish;
+        if ( p->nCexes == 64 )
+            return 0;
+        // remove the last variable
+        Vec_IntPop( p->vDivIds );
+    }
+finish:
+    if ( p->pPars->fVeryVerbose )
+    {
+        if ( iVar == -1 )
+            printf( "Node %d: Fanin %d can be removed.  ", iNode, f );
+        else
+            printf( "Node %d: Fanin %d can be replaced by divisor %d.   ", iNode, f, iVar );
+        Kit_DsdPrintFromTruth( (unsigned *)&uTruth, Vec_IntSize(p->vDivIds) ); printf( "\n" );
+    }
+    if ( iVar == -1 )
+        p->nRemoves++;
+    else
+        p->nResubs++;
+    if ( fSkipUpdate )
+        return 1;
+    // update the network
+    Sfm_NtkUpdate( p, iNode, f, (iVar == -1 ? iVar : Vec_IntEntry(p->vDivs, iVar)), uTruth );
+    return 1;
+ }
+int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
+{
+    int i, iFanin;
+    // prepare SAT solver
+    Sfm_NtkCreateWindow( p, iNode, p->pPars->fVeryVerbose );
+    Sfm_NtkWindowToSolver( p );
+    Sfm_NtkPrepareDivisors( p, iNode );
+    // try replacing area critical fanins
+    Sfm_ObjForEachFanin( p, iNode, iFanin, i )
+        if ( Sfm_ObjIsNode(p, iFanin) && Sfm_ObjFanoutNum(p, iFanin) == 1 )
+        {
+            if ( Sfm_NodeResubSolve( p, iNode, i, 0 ) )
+                return 1;
+        }
+    // try removing redundant edges
+    Sfm_ObjForEachFanin( p, iNode, iFanin, i )
+        if ( !(Sfm_ObjIsNode(p, iFanin) && Sfm_ObjFanoutNum(p, iFanin) == 1) )
+        {
+            if ( Sfm_NodeResubSolve( p, iNode, i, 1 ) )
+                return 1;
+        }
+/*
+    // try replacing area critical fanins while adding two new fanins
+    if ( Sfm_ObjFaninNum(p, iNode) < p->nFaninMax )
+        Abc_ObjForEachFanin( pNode, pFanin, i )
+            if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
+            {
+                if ( Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
+                    return 1;
+            }
+*/
+    return 0;
+}
 
 /**Function*************************************************************
 
@@ -96,19 +240,25 @@ void Sfm_NtkPrepare( Sfm_Ntk_t * p )
 ***********************************************************************/
 int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
 {
-//    int i;
+    int i;
+    p->timeTotal = clock();
     p->pPars = pPars;
     Sfm_NtkPrepare( p );
-    Sfm_ComputeInterpolantCheck( p );
-/*
+    p->nTotalNodesBeg = Vec_WecSizeUsed(&p->vFanins) - Sfm_NtkPoNum(p);
+    p->nTotalEdgesBeg = Vec_WecSizeSize(&p->vFanins);
     Sfm_NtkForEachNode( p, i )
     {
-//        printf( "Node %d:\n", i );
-//        Sfm_PrintCnf( (Vec_Str_t *)Vec_WecEntry(p->vCnfs, i) );
-//        printf( "\n" );
-        Sfm_NtkWindow( p, i, 1 );
+        if ( p->pPars->nDepthMax && Sfm_ObjLevel(p, i) > p->pPars->nDepthMax )
+            continue;
+        if ( Sfm_ObjFaninNum(p, i) < 2 || Sfm_ObjFaninNum(p, i) > 6 )
+            continue;
+        Sfm_NodeResub( p, i );
     }
-*/
+    p->nTotalNodesEnd = Vec_WecSizeUsed(&p->vFanins) - Sfm_NtkPoNum(p);
+    p->nTotalEdgesEnd = Vec_WecSizeSize(&p->vFanins);
+    p->timeTotal = clock() - p->timeTotal;
+    if ( pPars->fVerbose )
+        Sfm_NtkPrintStats( p );
     return 0;
 }
 
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index e2833121..57c5e352 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -41,6 +41,8 @@
 
 ABC_NAMESPACE_HEADER_START
 
+#define SFM_FANIN_MAX 6
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -48,52 +50,76 @@ ABC_NAMESPACE_HEADER_START
 struct Sfm_Ntk_t_
 {
     // parameters
-    Sfm_Par_t *       pPars;    // parameters
+    Sfm_Par_t *       pPars;       // parameters
     // objects
-    int               nPis;     // PI count (PIs should be first objects)
-    int               nPos;     // PO count (POs should be last objects)
-    int               nNodes;   // internal nodes
-    int               nObjs;    // total objects
+    int               nPis;        // PI count (PIs should be first objects)
+    int               nPos;        // PO count (POs should be last objects)
+    int               nNodes;      // internal nodes
+    int               nObjs;       // total objects
     // user data
-    Vec_Str_t *       vFixed;   // persistent objects
-    Vec_Wrd_t *       vTruths;  // truth tables
-    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         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
+    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
+    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
+    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
+    sat_solver *      pSat0;       // SAT solver for the off-set
+    sat_solver *      pSat1;       // SAT solver for the on-set
+    int               nSatVars;    // the number of variables
+    int               nTryRemoves; // number of fanin removals
+    int               nTryResubs;  // number of resubstitutions
+    int               nRemoves;    // number of fanin removals
+    int               nResubs;     // number of resubstitutions
+    // counter-examples
+    int               nCexes;      // number of CEXes
+    Vec_Wrd_t *       vDivCexes;   // counter-examples
     // intermediate data
-    Vec_Int_t *       vDivIds;  // divisors indexes
-    Vec_Int_t *       vLits;    // literals
-    Vec_Int_t *       vDiffs;   // differences
-    Vec_Wec_t *       vClauses; // CNF clauses for the node
-    Vec_Int_t *       vFaninMap;// mapping fanins into their SAT vars
+    Vec_Int_t *       vFans;       // current fanins
+    Vec_Int_t *       vOrder;      // object order
+    Vec_Int_t *       vDivVars;    // divisor SAT variables
+    Vec_Int_t *       vDivIds;     // divisors indexes
+    Vec_Int_t *       vLits;       // literals
+    Vec_Wec_t *       vClauses;    // CNF clauses for the node
+    Vec_Int_t *       vFaninMap;   // mapping fanins into their SAT vars
+    // nodes
+    int               nTotalNodesBeg;
+    int               nTotalEdgesBeg;
+    int               nTotalNodesEnd;
+    int               nTotalEdgesEnd;
+    // runtime
+    clock_t           timeWin;
+    clock_t           timeDiv;
+    clock_t           timeCnf;
+    clock_t           timeSat;
+    clock_t           timeTotal;
 };
 
 #define SFM_SAT_UNDEC 0x1234567812345678
 #define SFM_SAT_SAT   0x8765432187654321
 
 
+static inline int  Sfm_NtkPiNum( Sfm_Ntk_t * p )                        { return p->nPis;                                   }
+static inline int  Sfm_NtkPoNum( Sfm_Ntk_t * p )                        { return p->nPos;                                   }
+static inline int  Sfm_NtkNodeNum( Sfm_Ntk_t * p )                      { return p->nObjs - p->nPis - p->nPos;              }
+
 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;    }
@@ -104,6 +130,9 @@ static inline Vec_Int_t * Sfm_ObjFoArray( Sfm_Ntk_t * p, int i )        { return
 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_ObjRefIncrement( Sfm_Ntk_t * p, int iObj )       { return ++Sfm_ObjFiArray(p, iObj)->nSize;          } 
+static inline int  Sfm_ObjRefDecrement( Sfm_Ntk_t * p, int iObj )       { return --Sfm_ObjFiArray(p, iObj)->nSize;          } 
+
 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);     }
 
@@ -112,7 +141,8 @@ static inline void Sfm_ObjSetSatVar( Sfm_Ntk_t * p, int iObj, int Num ) { assert
 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_ObjLevel( Sfm_Ntk_t * p, int iObj )              { return Vec_IntEntry( &p->vLevels, iObj );                         }
+static inline void Sfm_ObjSetLevel( Sfm_Ntk_t * p, int iObj, int Lev )  { Vec_IntWriteEntry( &p->vLevels, iObj, Lev );                      }
 
 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); }
@@ -123,8 +153,8 @@ static inline void Sfm_ObjResetFaninCount( Sfm_Ntk_t * p, int iObj )    { Vec_In
 ////////////////////////////////////////////////////////////////////////
 
 #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++ )
+#define Sfm_ObjForEachFanin( p, Node, Fan, i )   for ( i = 0; i < Sfm_ObjFaninNum(p, Node)  && ((Fan = Sfm_ObjFanin(p, Node, i)), 1);  i++ )
+#define Sfm_ObjForEachFanout( p, Node, Fan, i )  for ( i = 0; i < Sfm_ObjFanoutNum(p, Node) && ((Fan = Sfm_ObjFanout(p, Node, i)), 1); i++ )
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
@@ -133,15 +163,20 @@ static inline void Sfm_ObjResetFaninCount( Sfm_Ntk_t * p, int iObj )    { Vec_In
 /*=== sfmCnf.c ==========================================================*/
 extern void         Sfm_PrintCnf( Vec_Str_t * vCnf );
 extern int          Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf );
+extern Vec_Wec_t *  Sfm_CreateCnf( Sfm_Ntk_t * p );
 extern void         Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap );
 /*=== sfmCore.c ==========================================================*/
 /*=== sfmNtk.c ==========================================================*/
 extern Sfm_Ntk_t *  Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPos );
+extern void         Sfm_NtkPrepare( Sfm_Ntk_t * p );
+extern void         Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth );
 /*=== 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 );
+extern void         Sfm_NtkWindowToSolver( Sfm_Ntk_t * p );
+extern word         Sfm_ComputeInterpolant( Sfm_Ntk_t * p );
 /*=== sfmWin.c ==========================================================*/
-extern int          Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode, int fVerbose );
-extern void         Sfm_NtkWin2Sat( Sfm_Ntk_t * p );
+extern int          Sfm_ObjMffcSize( Sfm_Ntk_t * p, int iObj );
+extern int          Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose );
+extern void         Sfm_NtkPrepareDivisors( Sfm_Ntk_t * p, int iNode );
 
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c
index d9b17799..3098d72f 100644
--- a/src/opt/sfm/sfmNtk.c
+++ b/src/opt/sfm/sfmNtk.c
@@ -107,46 +107,21 @@ void Sfm_CreateFanout( Vec_Wec_t * vFanins, Vec_Wec_t * vFanouts )
   SeeAlso     []
 
 ***********************************************************************/
-void Sfm_CreateLevel( Vec_Wec_t * vFanins, Vec_Int_t * vLevels )
+static inline int Sfm_ObjCreateLevel( Vec_Int_t * vArray, Vec_Int_t * vLevels )
 {
-    Vec_Int_t * vArray;
-    int i, k, Fanin, * pLevels;
-    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 );
+    int k, Fanin, Level = 0;
+    Vec_IntForEachEntry( vArray, Fanin, k )
+        Level = Abc_MaxInt( Level, Vec_IntEntry(vLevels, Fanin) + 1 );
+    return Level;
 }
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p )
+void Sfm_CreateLevel( Vec_Wec_t * vFanins, Vec_Int_t * vLevels )
 {
-    Vec_Wec_t * vCnfs;
-    Vec_Str_t * vCnf, * vCnfBase;
-    word uTruth;
+    Vec_Int_t * vArray;
     int i;
-    vCnf = Vec_StrAlloc( 100 );
-    vCnfs = Vec_WecStart( p->nObjs );
-    Vec_WrdForEachEntryStartStop( p->vTruths, uTruth, i, p->nPis, Vec_WrdSize(p->vTruths)-p->nPos )
-    {
-        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) );
-        vCnfBase->nSize = Vec_StrSize(vCnf);
-    }
-    Vec_StrFree( vCnf );
-    return vCnfs;
+    assert( Vec_IntSize(vLevels) == 0 );
+    Vec_IntGrow( vLevels, Vec_WecSize(vFanins) );
+    Vec_WecForEachLevel( vFanins, vArray, i )
+        Vec_IntPush( vLevels, Sfm_ObjCreateLevel(vArray, vLevels) );
 }
 
 /**Function*************************************************************
@@ -177,15 +152,31 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
     // attributes
     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 );
+    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 );
     p->vCnfs    = Sfm_CreateCnf( p );
     return p;
 }
+void Sfm_NtkPrepare( Sfm_Ntk_t * p )
+{
+    p->vDivCexes = Vec_WrdStart( p->pPars->nDivNumMax );
+    p->vLeaves   = Vec_IntAlloc( 1000 );
+    p->vRoots    = Vec_IntAlloc( 1000 );
+    p->vNodes    = Vec_IntAlloc( 1000 );
+    p->vTfo      = Vec_IntAlloc( 1000 );
+    p->vFans     = Vec_IntAlloc( 100 );
+    p->vOrder    = Vec_IntAlloc( 100 );
+    p->vDivVars  = Vec_IntAlloc( 100 );
+    p->vDivs     = Vec_IntAlloc( 100 );
+    p->vDivIds   = Vec_IntAlloc( 1000 );
+    p->vLits     = Vec_IntAlloc( 100 );
+    p->vClauses  = Vec_WecAlloc( 100 );
+    p->vFaninMap = Vec_IntAlloc( 10 );
+}
 void Sfm_NtkFree( Sfm_Ntk_t * p )
 {
     // user data
@@ -203,14 +194,17 @@ void Sfm_NtkFree( Sfm_Ntk_t * p )
     Vec_WecFree( p->vCnfs );
     Vec_IntFree( p->vCover );
     // other data
+    Vec_WrdFreeP( &p->vDivCexes );
     Vec_IntFreeP( &p->vLeaves );
     Vec_IntFreeP( &p->vRoots );
     Vec_IntFreeP( &p->vNodes );
     Vec_IntFreeP( &p->vTfo   );
+    Vec_IntFreeP( &p->vFans );
+    Vec_IntFreeP( &p->vOrder );
+    Vec_IntFreeP( &p->vDivVars );
     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 );
@@ -220,6 +214,72 @@ void Sfm_NtkFree( Sfm_Ntk_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Performs resubstitution for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sfm_NtkRemoveFanin( Sfm_Ntk_t * p, int iNode, int iFanin )
+{
+    int RetValue;
+    RetValue = Vec_IntRemove( Sfm_ObjFiArray(p, iNode), iFanin );
+    assert( RetValue );
+    RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode );
+    assert( RetValue );
+}
+void Sfm_NtkAddFanin( Sfm_Ntk_t * p, int iNode, int iFanin )
+{
+    if ( iFanin < 0 )
+        return;
+    assert( Vec_IntFind( Sfm_ObjFiArray(p, iNode), iFanin ) == -1 );
+    assert( Vec_IntFind( Sfm_ObjFoArray(p, iFanin), iNode ) == -1 );
+    Vec_IntPush( Sfm_ObjFiArray(p, iNode), iFanin );
+    Vec_IntPush( Sfm_ObjFoArray(p, iFanin), iNode );
+}
+void Sfm_NtkDeleteObj_rec( Sfm_Ntk_t * p, int iNode )
+{
+    int i, iFanin;
+    if ( Sfm_ObjFanoutNum(p, iNode) > 0 )
+        return;
+    Sfm_ObjForEachFanin( p, iNode, iFanin, i )
+    {
+        int RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode );  assert( RetValue );
+        if ( Sfm_ObjFanoutNum(p, iFanin) == 0 )
+            Sfm_NtkDeleteObj_rec( p, iFanin );
+    }
+    Vec_IntClear( Sfm_ObjFiArray(p, iNode) );
+}
+void Sfm_NtkUpdateLevel_rec( Sfm_Ntk_t * p, int iNode )
+{
+    int i, iFanout;
+    int LevelNew = Sfm_ObjCreateLevel( Sfm_ObjFiArray(p, iNode), &p->vLevels );
+    if ( LevelNew == Sfm_ObjLevel(p, iNode) )
+        return;
+    Sfm_ObjSetLevel( p, iNode, LevelNew );
+    Sfm_ObjForEachFanout( p, iNode, iFanout, i )
+        Sfm_NtkUpdateLevel_rec( p, iFanout );
+}
+void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth )
+{
+    int iFanin = Sfm_ObjFanin( p, iNode, f );
+    // replace old fanin by new fanin
+    Sfm_NtkRemoveFanin( p, iNode, iFanin );
+    Sfm_NtkAddFanin( p, iNode, iFaninNew );
+    // recursively remove MFFC
+    Sfm_NtkDeleteObj_rec( p, iFanin );
+    // update logic level
+    Sfm_NtkUpdateLevel_rec( p, iNode );
+    // update truth table
+    Vec_WrdWriteEntry( p->vTruths, iNode, uTruth );
+    Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Public APIs of this network.]
 
   Description []
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c
index 3ad97503..86564744 100644
--- a/src/opt/sfm/sfmSat.c
+++ b/src/opt/sfm/sfmSat.c
@@ -42,6 +42,28 @@ static word s_Truths6[6] = {
 
 /**Function*************************************************************
 
+  Synopsis    [Creates order of objects in the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sfm_NtkOrderObjects( Sfm_Ntk_t * p )
+{
+    int i, iNode;
+    assert( Vec_IntEntryLast(p->vNodes) == Vec_IntEntry(p->vDivs, Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes)) );
+    Vec_IntClear( p->vOrder );
+    Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
+        Vec_IntPush( p->vOrder, iNode );
+    Vec_IntForEachEntryStart( p->vDivs, iNode, i, Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) )
+        Vec_IntPush( p->vOrder, iNode );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Converts a window into a SAT solver.]
 
   Description []
@@ -51,14 +73,15 @@ static word s_Truths6[6] = {
   SeeAlso     []
 
 ***********************************************************************/
-void Sfm_NtkWin2Sat( Sfm_Ntk_t * p )
+void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
 {
     Vec_Int_t * vClause;
-    int RetValue, Lit, iNode = -1, iFanin, i, k, c;
+    int RetValue, Lit, iNode = -1, iFanin, i, k;
+    clock_t clk = clock();
     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) );
+    sat_solver_setnvars( pSat0, 1 + Vec_IntSize(p->vDivs) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) + 100 );
+    sat_solver_setnvars( pSat1, 1 + Vec_IntSize(p->vDivs) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) + 100 );
     // create SAT variables
     p->nSatVars = 1;
     Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
@@ -67,29 +90,26 @@ void Sfm_NtkWin2Sat( Sfm_Ntk_t * p )
         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++ )
+    // add CNF clauses for the TFI
+    Sfm_NtkOrderObjects( p );
+    Vec_IntForEachEntry( p->vOrder, iNode, i )
     {
-        Vec_Int_t * vObjs = c ? p->vDivs : p->vNodes;
-        Vec_IntForEachEntryReverse( vObjs, iNode, i )
+        // collect fanin variables
+        Vec_IntClear( p->vFaninMap );
+        Sfm_ObjForEachFanin( 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 )
         {
-            // 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 );
-            }
+            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
@@ -110,70 +130,73 @@ void Sfm_NtkWin2Sat( Sfm_Ntk_t * p )
     assert( p->pSat1 == NULL );
     p->pSat0 = pSat0;
     p->pSat1 = pSat1;
+    p->timeCnf += clock() - clk;
 }
 
 /**Function*************************************************************
 
   Synopsis    [Takes SAT solver and returns interpolant.]
 
-  Description [If interpolant does not exist, returns diff SAT variables.]
+  Description [If interpolant does not exist, records difference variables.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-word Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_t * vDivIds, Vec_Int_t * vLits, Vec_Int_t * vDiffs, int nBTLimit )
+word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
 {
-    word uTruth = 0, uCube;
+    word * pSign, uCube, uTruth = 0;
     int status, i, Div, iVar, nFinal, * pFinal;
-    int nVars = sat_solver_nvars(pSatOn);
+    int nVars = sat_solver_nvars( p->pSat1 );
     int iNewLit = Abc_Var2Lit( nVars, 0 );
-    int RetValue;
-    sat_solver_setnvars( pSatOn, nVars + 1 );
+    sat_solver_setnvars( p->pSat1, nVars + 1 );
     while ( 1 ) 
     {
         // find onset minterm
-        status = sat_solver_solve( pSatOn, &iNewLit, &iNewLit + 1, nBTLimit, 0, 0, 0 );
+        status = sat_solver_solve( p->pSat1, &iNewLit, &iNewLit + 1, p->pPars->nBTLimit, 0, 0, 0 );
         if ( status == l_Undef )
             return SFM_SAT_UNDEC;
         if ( status == l_False )
             return uTruth;
         assert( status == l_True );
-        // collect literals
-        Vec_IntClear( vLits );
-        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) );
+        // collect divisor literals
+        Vec_IntClear( p->vLits );
+        Vec_IntForEachEntry( p->vDivIds, Div, i )
+            Vec_IntPush( p->vLits, sat_solver_var_literal(p->pSat1, Div) );
         // check against offset
-        status = sat_solver_solve( pSatOff, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
+        status = sat_solver_solve( p->pSat0, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits), p->pPars->nBTLimit, 0, 0, 0 );
         if ( status == l_Undef )
             return SFM_SAT_UNDEC;
         if ( status == l_True )
-        {
-            Vec_IntClear( vDiffs );
-            for ( i = 0; i < nVars; i++ )
-                Vec_IntPush( vDiffs, sat_solver_var_value(pSatOn, i) ^ sat_solver_var_value(pSatOff, i) );
-            return SFM_SAT_SAT;
-        }
+            break;
         assert( status == l_False );
         // compute cube and add clause
-        nFinal = sat_solver_final( pSatOff, &pFinal );
+        nFinal = sat_solver_final( p->pSat0, &pFinal );
         uCube = ~(word)0;
-        Vec_IntClear( vLits );
-        Vec_IntPush( vLits, Abc_LitNot(iNewLit) );
+        Vec_IntClear( p->vLits );
+        Vec_IntPush( p->vLits, Abc_LitNot(iNewLit) );
         for ( i = 0; i < nFinal; i++ )
         {
-            Vec_IntPush( vLits, pFinal[i] );
-            iVar = Vec_IntFind( vDivIds, Abc_Lit2Var(pFinal[i]) );   assert( iVar >= 0 );
+            Vec_IntPush( p->vLits, pFinal[i] );
+            iVar = Vec_IntFind( p->vDivIds, Abc_Lit2Var(pFinal[i]) );   assert( iVar >= 0 );
             uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
         }
         uTruth |= uCube;
-        RetValue = sat_solver_addclause( pSatOn, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
-        assert( RetValue );
+        status = sat_solver_addclause( p->pSat1, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) );
+        assert( status );
     }
-    assert( 0 );
-    return 0;
+    assert( status == l_True );
+    // store the counter-example
+    Vec_IntForEachEntry( p->vDivVars, iVar, i )
+        if ( sat_solver_var_value(p->pSat1, iVar) ^ sat_solver_var_value(p->pSat0, iVar) ) // insert 1
+        {
+            pSign = Vec_WrdEntryP( p->vDivCexes, i );
+            assert( !Abc_InfoHasBit( (unsigned *)pSign, p->nCexes) );
+            Abc_InfoXorBit( (unsigned *)pSign, p->nCexes );
+        }
+    p->nCexes++;
+    return SFM_SAT_SAT;
 }
 
 /**Function*************************************************************
@@ -187,6 +210,7 @@ word Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_
   SeeAlso     []
 
 ***********************************************************************/
+/*
 void Sfm_ComputeInterpolantCheck( Sfm_Ntk_t * p )
 {
     int iNode = 3;
@@ -196,8 +220,8 @@ void Sfm_ComputeInterpolantCheck( Sfm_Ntk_t * p )
 //    int i;
 //    Sfm_NtkForEachNode( p, i )
     {
-        Sfm_NtkWindow( p, iNode, 1 );
-        Sfm_NtkWin2Sat( p );
+        Sfm_NtkCreateWindow( p, iNode, 1 );
+        Sfm_NtkWindowToSolver( p );
 
         // collect SAT variables of divisors
         Vec_IntClear( p->vDivIds );
@@ -218,6 +242,7 @@ void Sfm_ComputeInterpolantCheck( Sfm_Ntk_t * p )
         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 078406ba..e0baa96f 100644
--- a/src/opt/sfm/sfmWin.c
+++ b/src/opt/sfm/sfmWin.c
@@ -33,6 +33,71 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the MFFC size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sfm_ObjRef_rec( Sfm_Ntk_t * p, int iObj )
+{
+    int i, iFanin, Value, Count;
+    if ( Sfm_ObjIsPi(p, iObj) )
+        return 0;
+    assert( Sfm_ObjIsNode(p, iObj) );
+    Value = Sfm_ObjRefIncrement(p, iObj);
+    if ( Value > 1 )
+        return 0;
+    assert( Value == 1 );
+    Count = 1;
+    Sfm_ObjForEachFanin( p, iObj, iFanin, i )
+        Count += Sfm_ObjRef_rec( p, iFanin );
+    return Count;
+}
+int Sfm_ObjRef( Sfm_Ntk_t * p, int iObj )
+{
+    int i, iFanin, Count = 1;
+    Sfm_ObjForEachFanin( p, iObj, iFanin, i )
+        Count += Sfm_ObjRef_rec( p, iFanin );
+    return Count;
+}
+int Sfm_ObjDeref_rec( Sfm_Ntk_t * p, int iObj )
+{
+    int i, iFanin, Value, Count;
+    if ( Sfm_ObjIsPi(p, iObj) )
+        return 0;
+    assert( Sfm_ObjIsNode(p, iObj) );
+    Value = Sfm_ObjRefDecrement(p, iObj);
+    if ( Value > 0 )
+        return 0;
+    assert( Value == 0 );
+    Count = 1;
+    Sfm_ObjForEachFanin( p, iObj, iFanin, i )
+        Count += Sfm_ObjDeref_rec( p, iFanin );
+    return Count;
+}
+int Sfm_ObjDeref( Sfm_Ntk_t * p, int iObj )
+{
+    int i, iFanin, Count = 1;
+    Sfm_ObjForEachFanin( p, iObj, iFanin, i )
+        Count += Sfm_ObjDeref_rec( p, iFanin );
+    return Count;
+}
+int Sfm_ObjMffcSize( Sfm_Ntk_t * p, int iObj )
+{
+    int Count1, Count2;
+    assert( Sfm_ObjIsNode( p, iObj ) );
+    Count1 = Sfm_ObjDeref( p, iObj );
+    Count2 = Sfm_ObjRef( p, iObj );
+    assert( Count1 == Count2 );
+    return Count1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Working with traversal IDs.]
 
   Description []
@@ -70,7 +135,7 @@ int Sfm_NtkCheckOverlap_rec( Sfm_Ntk_t * p, int iThis, int iNode )
     if ( Sfm_ObjIsTravIdCurrent(p, iThis) )
         return 1;
     Sfm_ObjSetTravIdCurrent2(p, iThis);
-    Sfm_NodeForEachFanin( p, iThis, iFanin, i )
+    Sfm_ObjForEachFanin( p, iThis, iFanin, i )
         if ( Sfm_NtkCheckOverlap_rec(p, iFanin, iNode) )
             return 1;
     return 0;
@@ -97,7 +162,7 @@ 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 )
+    Sfm_ObjForEachFanout( p, iNode, iFanout, i )
         if ( !Sfm_NtkCheckOverlap( p, iFanout, iNode ) )
             return 0;
     return 1;
@@ -117,7 +182,7 @@ int Sfm_NtkCheckFanouts( Sfm_Ntk_t * p, int iNode )
 void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode )
 {
     int i, iFanout;
-    Sfm_NodeForEachFanout( p, iNode, iFanout, i )
+    Sfm_ObjForEachFanout( 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) || 
@@ -162,13 +227,14 @@ void Sfm_NtkCollectTfi_rec( Sfm_Ntk_t * p, int iNode )
         Vec_IntPush( p->vLeaves, iNode );
         return;
     }
-    Sfm_NodeForEachFanin( p, iNode, iFanin, i )
+    Sfm_ObjForEachFanin( p, iNode, iFanin, i )
         Sfm_NtkCollectTfi_rec( p, iFanin );
     Vec_IntPush( p->vNodes, iNode );
 }
-int Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
+int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
 {
     int i, iTemp;
+    clock_t clk = clock();
 /*
     if ( iNode == 7 )
     {
@@ -187,7 +253,7 @@ int Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
     Vec_IntClear( p->vTfo );    // roots
     if ( Sfm_NtkCheckFanouts(p, iNode) )
     {
-        Sfm_NodeForEachFanout( p, iNode, iTemp, i )
+        Sfm_ObjForEachFanout( p, iNode, iTemp, i )
         {
             if ( Sfm_ObjIsPo(p, iTemp) )
                 continue;
@@ -197,15 +263,16 @@ int Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
     }
     else
         Vec_IntPush( p->vRoots, iNode );
+    p->timeWin += clock() - clk;
     // collect divisors of the TFI nodes
+    clk = clock();
     Vec_IntClear( p->vDivs );
+    Vec_IntAppend( p->vDivs, p->vLeaves );
+    Vec_IntAppend( p->vDivs, p->vNodes );
     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 );
+    p->timeDiv += clock() - clk;
     if ( !fVerbose )
         return 1;
 
@@ -222,7 +289,42 @@ void Sfm_NtkWindowTest( Sfm_Ntk_t * p, int iNode )
 {
     int i;
     Sfm_NtkForEachNode( p, i )
-        Sfm_NtkWindow( p, i, 1 );
+        Sfm_NtkCreateWindow( p, i, 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes node and its fanins from the array of divisors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sfm_NtkPrepareDivisors( Sfm_Ntk_t * p, int iNode )
+{
+    int i, iFanin, k = 0;
+    // mark fanins
+    Sfm_NtkIncrementTravId( p );
+    Sfm_ObjSetTravIdCurrent( p, iNode );
+    Sfm_ObjForEachFanin( p, iNode, iFanin, i )
+        Sfm_ObjSetTravIdCurrent( p, iFanin );
+    // compact divisors
+    Vec_IntClear( p->vDivVars );
+    Vec_IntForEachEntry( p->vDivs, iFanin, i )
+        if ( !Sfm_ObjIsTravIdCurrent( p, iFanin ) )
+        {
+            Vec_IntPush( p->vDivVars, Sfm_ObjSatVar(p, iFanin) );
+            Vec_IntWriteEntry( p->vDivs, k++, iFanin );
+        }
+    assert( Vec_IntSize(p->vDivs) == k + Sfm_ObjFaninNum(p, iNode) + 1 );
+    Vec_IntShrink( p->vDivs, k );
+    // collect fanins
+//    Vec_IntClear( p->vFans );
+//    Sfm_ObjForEachFanin( p, iNode, iFanin, i )
+//        Vec_IntPush( p->vFans, iFanin );
 }
 
 ////////////////////////////////////////////////////////////////////////