New MFS package.

7 files changed, 87 insertions, 63 deletions

diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index 5f266c68..b67fc8df 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -71,7 +71,7 @@ extern int          Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars );
 extern Sfm_Ntk_t *  Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Wrd_t * vTruths );
 extern void         Sfm_NtkFree( Sfm_Ntk_t * p );
 extern Vec_Int_t *  Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i );
-extern word         Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i );
+extern word *       Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i );
 extern int          Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i );
 /*=== sfmSat.c ==========================================================*/
 
diff --git a/src/opt/sfm/sfmCnf.c b/src/opt/sfm/sfmCnf.c
index 09dce50c..126b6ca0 100644
--- a/src/opt/sfm/sfmCnf.c
+++ b/src/opt/sfm/sfmCnf.c
@@ -151,8 +151,8 @@ Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p )
 void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap )
 {
     Vec_Int_t * vClause;
-    int i, Lit;
     char Entry;
+    int i, Lit;
     Vec_WecClear( vRes );
     vClause = Vec_WecPushLevel( vRes );
     Vec_StrForEachEntry( vCnf, Entry, i )
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
index 7d206fa2..35c092fa 100644
--- a/src/opt/sfm/sfmCore.c
+++ b/src/opt/sfm/sfmCore.c
@@ -51,7 +51,7 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
     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->fFixLevel    =    1;  // does not allow level to increase
     pPars->fArea        =    0;  // performs optimization for area
     pPars->fMoreEffort  =    0;  // performs high-affort minimization
     pPars->fVerbose     =    0;  // enable basic stats
@@ -71,14 +71,17 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
 ***********************************************************************/
 void Sfm_NtkPrintStats( Sfm_Ntk_t * p )
 {
-    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( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n",
+        Sfm_NtkNodeNum(p), p->nNodesTried, p->nRemoves + p->nResubs, p->nTotalDivs, p->nSatCalls, p->nTimeOuts );
+
+    printf( "Attempts :   " );
+    printf( "Remove %6d -> %6d (%6.2f %%)   ", p->nTryRemoves, p->nRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) );
+    printf( "Resub  %6d -> %6d (%6.2f %%)   ", p->nTryResubs,  p->nResubs,  100.0*p->nResubs /Abc_MaxInt(1, 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( "Reduction:   " );
+    printf( "Nodes  %6d -> %6d (%6.2f %%)   ", p->nTotalNodesBeg, p->nTotalNodesEnd, 100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/Abc_MaxInt(1, p->nTotalNodesBeg) );
+    printf( "Edges  %6d -> %6d (%6.2f %%)   ", p->nTotalEdgesBeg, p->nTotalEdgesEnd, 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/Abc_MaxInt(1, p->nTotalEdgesBeg) );
     printf( "\n" );
 
     ABC_PRTP( "Win", p->timeWin  ,  p->timeTotal );
@@ -101,7 +104,7 @@ void Sfm_NtkPrintStats( Sfm_Ntk_t * p )
 ***********************************************************************/
 int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly )
 {
-    int fSkipUpdate  = 1;
+    int fSkipUpdate  = 0;
     int fVeryVerbose = p->pPars->fVeryVerbose && Vec_IntSize(p->vDivs) < 200;// || pNode->Id == 556;
     int i, iFanin, iVar = -1;
     word uTruth, uSign, uMask;
@@ -121,19 +124,22 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly )
     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) );
+clk = clock();
     uTruth = Sfm_ComputeInterpolant( p );
 p->timeSat += clock() - clk;
     // analyze outcomes
     if ( uTruth == SFM_SAT_UNDEC )
+    {
+        p->nTimeOuts++;
         return 0;
-    if ( uTruth == SFM_SAT_SAT )
+    }
+    if ( uTruth != SFM_SAT_SAT )
         goto finish;
-    if ( fRemoveOnly )
+    if ( fRemoveOnly || Vec_IntSize(p->vDivs) == 0 )
         return 0;
     if ( fVeryVerbose )
     {
@@ -160,14 +166,17 @@ p->timeSat += clock() - clk;
         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)) );
+clk = clock();
         uTruth = Sfm_ComputeInterpolant( p );
 p->timeSat += clock() - clk;
         // analyze outcomes
         if ( uTruth == SFM_SAT_UNDEC )
+        {
+            p->nTimeOuts++;
             return 0;
-        if ( uTruth == SFM_SAT_SAT )
+        }
+        if ( uTruth != SFM_SAT_SAT )
             goto finish;
         if ( p->nCexes == 64 )
             return 0;
@@ -188,7 +197,7 @@ finish:
     else
         p->nResubs++;
     if ( fSkipUpdate )
-        return 1;
+        return 0;
     // update the network
     Sfm_NtkUpdate( p, iNode, f, (iVar == -1 ? iVar : Vec_IntEntry(p->vDivs, iVar)), uTruth );
     return 1;
@@ -196,6 +205,7 @@ finish:
 int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
 {
     int i, iFanin;
+    p->nNodesTried++;
     // prepare SAT solver
     Sfm_NtkCreateWindow( p, iNode, p->pPars->fVeryVerbose );
     Sfm_NtkWindowToSolver( p );
@@ -240,26 +250,30 @@ int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
 ***********************************************************************/
 int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
 {
-    int i;
+    int i, Counter = 0;
     p->timeTotal = clock();
     p->pPars = pPars;
     Sfm_NtkPrepare( p );
+//    Sfm_ComputeInterpolantCheck( p );
+//    return 0;
     p->nTotalNodesBeg = Vec_WecSizeUsed(&p->vFanins) - Sfm_NtkPoNum(p);
     p->nTotalEdgesBeg = Vec_WecSizeSize(&p->vFanins);
     Sfm_NtkForEachNode( p, i )
     {
+        if ( Sfm_ObjIsFixed( p, i ) )
+            continue;
         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 );
+        Counter += 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;
+    return Counter;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index 57c5e352..03d03111 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -43,6 +43,9 @@ ABC_NAMESPACE_HEADER_START
 
 #define SFM_FANIN_MAX 6
 
+#define SFM_SAT_UNDEC 0x1234567812345678
+#define SFM_SAT_SAT   0x8765432187654321
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -76,10 +79,10 @@ struct Sfm_Ntk_t_
     // 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 *       vRoots;      // roots
+    Vec_Int_t *       vTfo;        // TFO (excluding iNode)
     // SAT solving
     sat_solver *      pSat0;       // SAT solver for the off-set
     sat_solver *      pSat1;       // SAT solver for the on-set
@@ -92,7 +95,7 @@ struct Sfm_Ntk_t_
     int               nCexes;      // number of CEXes
     Vec_Wrd_t *       vDivCexes;   // counter-examples
     // intermediate data
-    Vec_Int_t *       vFans;       // current fanins
+//    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
@@ -104,6 +107,10 @@ struct Sfm_Ntk_t_
     int               nTotalEdgesBeg;
     int               nTotalNodesEnd;
     int               nTotalEdgesEnd;
+    int               nNodesTried;
+    int               nTotalDivs;
+    int               nSatCalls;
+    int               nTimeOuts;
     // runtime
     clock_t           timeWin;
     clock_t           timeDiv;
@@ -112,10 +119,6 @@ struct Sfm_Ntk_t_
     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;              }
@@ -123,6 +126,7 @@ static inline int  Sfm_NtkNodeNum( Sfm_Ntk_t * p )                      { return
 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_ObjIsFixed( Sfm_Ntk_t * p, int i )               { return Vec_StrEntry(p->vFixed, i);                }
 
 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);             }
@@ -136,10 +140,10 @@ static inline int  Sfm_ObjRefDecrement( Sfm_Ntk_t * p, int iObj )       { return
 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 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_ObjSatVar( Sfm_Ntk_t * p, int iObj )             { assert(Vec_IntEntry(&p->vId2Var, iObj) > 0); return Vec_IntEntry(&p->vId2Var, iObj);  }
+static inline void Sfm_ObjSetSatVar( Sfm_Ntk_t * p, int iObj, int Num ) { assert(Vec_IntEntry(&p->vId2Var, 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 )         { int iObj = Vec_IntEntry(&p->vVar2Id, Num); assert(Vec_IntEntry(&p->vId2Var, iObj) > 0); Vec_IntWriteEntry(&p->vId2Var, iObj, -1);  Vec_IntWriteEntry(&p->vVar2Id, Num, -1); }
+static inline void Sfm_NtkCleanVars( Sfm_Ntk_t * p )                    { int i; for ( i = 1; i < p->nSatVars; i++ )  Sfm_ObjCleanSatVar( p, i ); }
 
 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 );                      }
diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c
index 3098d72f..29463de6 100644
--- a/src/opt/sfm/sfmNtk.c
+++ b/src/opt/sfm/sfmNtk.c
@@ -163,15 +163,15 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
 }
 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->vDivs     = Vec_IntAlloc( 100 );
+    p->vRoots    = Vec_IntAlloc( 1000 );
     p->vTfo      = Vec_IntAlloc( 1000 );
-    p->vFans     = Vec_IntAlloc( 100 );
+    p->vDivCexes = Vec_WrdStart( p->pPars->nDivNumMax );
+//    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 );
@@ -194,15 +194,15 @@ 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->vDivs  );
+    Vec_IntFreeP( &p->vRoots );
     Vec_IntFreeP( &p->vTfo   );
-    Vec_IntFreeP( &p->vFans );
+    Vec_WrdFreeP( &p->vDivCexes );
+//    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_WecFreeP( &p->vClauses );
@@ -243,8 +243,9 @@ void Sfm_NtkAddFanin( Sfm_Ntk_t * p, int iNode, int iFanin )
 void Sfm_NtkDeleteObj_rec( Sfm_Ntk_t * p, int iNode )
 {
     int i, iFanin;
-    if ( Sfm_ObjFanoutNum(p, iNode) > 0 )
+    if ( Sfm_ObjFanoutNum(p, iNode) > 0 || Sfm_ObjIsPi(p, iNode) )
         return;
+    assert( Sfm_ObjIsNode(p, iNode) );
     Sfm_ObjForEachFanin( p, iNode, iFanin, i )
     {
         int RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode );  assert( RetValue );
@@ -260,13 +261,15 @@ void Sfm_NtkUpdateLevel_rec( Sfm_Ntk_t * p, int iNode )
     if ( LevelNew == Sfm_ObjLevel(p, iNode) )
         return;
     Sfm_ObjSetLevel( p, iNode, LevelNew );
-    Sfm_ObjForEachFanout( p, iNode, iFanout, i )
-        Sfm_NtkUpdateLevel_rec( p, iFanout );
+    if ( Sfm_ObjIsNode(p, iNode) )
+        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
+    assert( Sfm_ObjIsNode(p, iNode) );
     Sfm_NtkRemoveFanin( p, iNode, iFanin );
     Sfm_NtkAddFanin( p, iNode, iFaninNew );
     // recursively remove MFFC
@@ -293,9 +296,9 @@ Vec_Int_t *  Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i )
 {
     return Vec_WecEntry( &p->vFanins, i );
 }
-word Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i )
+word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i )
 {
-    return Vec_WrdEntry( p->vTruths, i );
+    return Vec_WrdEntryP( p->vTruths, i );
 }
 int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i )
 {
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c
index 86564744..f5355503 100644
--- a/src/opt/sfm/sfmSat.c
+++ b/src/opt/sfm/sfmSat.c
@@ -54,7 +54,7 @@ static word s_Truths6[6] = {
 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)) );
+    assert( Vec_IntEntryLast(p->vNodes) == Vec_IntEntry(p->vDivs, Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) - 1) );
     Vec_IntClear( p->vOrder );
     Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
         Vec_IntPush( p->vOrder, iNode );
@@ -83,15 +83,14 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
     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
+    Sfm_NtkCleanVars( p );
     p->nSatVars = 1;
-    Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
-        Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
-    Vec_IntForEachEntryReverse( p->vLeaves, iNode, i )
+    Sfm_NtkOrderObjects( p );
+    Vec_IntForEachEntry( p->vOrder, iNode, i )
         Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
-    Vec_IntForEachEntryReverse( p->vDivs, iNode, i )
+    Vec_IntForEachEntry( p->vLeaves, iNode, i )
         Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
     // add CNF clauses for the TFI
-    Sfm_NtkOrderObjects( p );
     Vec_IntForEachEntry( p->vOrder, iNode, i )
     {
         // collect fanin variables
@@ -112,6 +111,7 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
             assert( RetValue );
         }
     }
+//    Sat_SolverWriteDimacs( pSat0, "test.cnf", NULL, NULL, 0 );
     // get the last node
     iNode = Vec_IntEntryLast( p->vNodes );
     // add unit clause
@@ -126,8 +126,8 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
     sat_solver_compress( pSat0 );
     sat_solver_compress( pSat1 );
     // return the result
-    assert( p->pSat0 == NULL );
-    assert( p->pSat1 == NULL );
+    if ( p->pSat0 ) sat_solver_delete( p->pSat0 );
+    if ( p->pSat1 ) sat_solver_delete( p->pSat1 );
     p->pSat0 = pSat0;
     p->pSat1 = pSat1;
     p->timeCnf += clock() - clk;
@@ -147,24 +147,29 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
 word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
 {
     word * pSign, uCube, uTruth = 0;
-    int status, i, Div, iVar, nFinal, * pFinal;
+    int status, i, Div, iVar, nFinal, * pFinal, nIter = 0;
     int nVars = sat_solver_nvars( p->pSat1 );
     int iNewLit = Abc_Var2Lit( nVars, 0 );
     sat_solver_setnvars( p->pSat1, nVars + 1 );
     while ( 1 ) 
     {
         // find onset minterm
+        p->nSatCalls++;
         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 )
+        {
+//            printf( "+%d ", nIter );
             return uTruth;
+        }
         assert( status == l_True );
         // 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
+        p->nSatCalls++;
         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;
@@ -185,7 +190,9 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
         uTruth |= uCube;
         status = sat_solver_addclause( p->pSat1, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) );
         assert( status );
+        nIter++;
     }
+//    printf( "-%d ", nIter );
     assert( status == l_True );
     // store the counter-example
     Vec_IntForEachEntry( p->vDivVars, iVar, i )
@@ -210,12 +217,11 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-/*
 void Sfm_ComputeInterpolantCheck( Sfm_Ntk_t * p )
 {
     int iNode = 3;
-    int iDiv0 = 6;
-    int iDiv1 = 7;
+    int iDiv0 = 5;
+    int iDiv1 = 4;
     word uTruth;
 //    int i;
 //    Sfm_NtkForEachNode( p, i )
@@ -228,7 +234,7 @@ void Sfm_ComputeInterpolantCheck( Sfm_Ntk_t * p )
         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 );
+        uTruth = Sfm_ComputeInterpolant( p );
 
         if ( uTruth == SFM_SAT_SAT )
             printf( "The problem is SAT.\n" );
@@ -236,13 +242,8 @@ void Sfm_ComputeInterpolantCheck( Sfm_Ntk_t * p )
             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 e0baa96f..893a4592 100644
--- a/src/opt/sfm/sfmWin.c
+++ b/src/opt/sfm/sfmWin.c
@@ -245,6 +245,7 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
     assert( Sfm_ObjIsNode( p, iNode ) );
     Vec_IntClear( p->vLeaves ); // leaves 
     Vec_IntClear( p->vNodes );  // internal
+    Vec_IntClear( p->vDivs );   // divisors
     // collect transitive fanin
     Sfm_NtkIncrementTravId( p );
     Sfm_NtkCollectTfi_rec( p, iNode );
@@ -266,12 +267,13 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
     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->vDivs, iTemp, i )
-        Sfm_NtkAddDivisors( p, iTemp );
+        if ( Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax )
+            Sfm_NtkAddDivisors( p, iTemp );
+    p->nTotalDivs += Vec_IntSize(p->vDivs);
     p->timeDiv += clock() - clk;
     if ( !fVerbose )
         return 1;