New MFS package.

12 files changed, 111 insertions, 109 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 5f100fb0..cb3e1f1e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -4327,7 +4327,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
             }
             pPars->nFanoutsMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( pPars->nFanoutsMax < 1 )
+            if ( pPars->nFanoutsMax < 0 )
                 goto usage;
             break;
         case 'D':
@@ -4496,7 +4496,7 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
             }
             pPars->nFanoutMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( pPars->nFanoutMax < 1 )
+            if ( pPars->nFanoutMax < 0 )
                 goto usage;
             break;
         case 'D':
diff --git a/src/base/abci/abcMfs.c b/src/base/abci/abcMfs.c
index 9c0513de..7953be15 100644
--- a/src/base/abci/abcMfs.c
+++ b/src/base/abci/abcMfs.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "base/abc/abc.h"
+#include "bool/kit/kit.h"
 #include "opt/sfm/sfm.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -120,6 +121,7 @@ Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p )
 {
+    Vec_Int_t * vCover = Sfm_NodeReadCover(p);
     Vec_Int_t * vMap, * vArray;
     Abc_Obj_t * pNode;
     int i, k, Fanin;
@@ -155,7 +157,14 @@ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p )
         else if ( ~pTruth[0] == 0 )
             pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, " 1\n" );
         else
-            pNode->pData = Abc_SopCreateFromTruth( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), (unsigned *)pTruth );
+        {
+//            pNode->pData = Abc_SopCreateFromTruth( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), (unsigned *)pTruth );
+            int RetValue = Kit_TruthIsop( (unsigned *)pTruth, Vec_IntSize(vArray), vCover, 1 );
+            assert( RetValue == 0 || RetValue == 1 );
+            pNode->pData = Abc_SopCreateFromIsop( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), vCover );
+            if ( RetValue )
+                Abc_SopComplement( (char *)pNode->pData );
+        }
     }
     Vec_IntFree( vMap );
 }
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 22a28e22..d652d8cd 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -48,7 +48,7 @@ void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars )
 {
     memset( pPars, 0, sizeof(Mfs_Par_t) );
     pPars->nWinTfoLevs  =    2;
-    pPars->nFanoutsMax  =   10;
+    pPars->nFanoutsMax  =   30;
     pPars->nDepthMax    =   20;
     pPars->nDivMax      =  250;
     pPars->nWinSizeMax  =  300;
@@ -406,7 +406,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
         }
     }
     // perform the network sweep
-    Abc_NtkSweep( pNtk, 0 );
+//    Abc_NtkSweep( pNtk, 0 );
     // convert into the AIG
     if ( !Abc_NtkToAig(pNtk) )
     {
diff --git a/src/opt/mfs/mfsDiv.c b/src/opt/mfs/mfsDiv.c
index 1473580e..0b29673e 100644
--- a/src/opt/mfs/mfsDiv.c
+++ b/src/opt/mfs/mfsDiv.c
@@ -214,7 +214,7 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
     // (3) the node's fanins (these are treated as a special case)
     Abc_NtkIncrementTravId( pNode->pNtk );
     Abc_MfsWinSweepLeafTfo_rec( pNode, nLevDivMax );
-    Abc_MfsWinVisitMffc( pNode );
+//    Abc_MfsWinVisitMffc( pNode );
     Abc_ObjForEachFanin( pNode, pObj, k )
         Abc_NodeSetTravIdCurrent( pObj );
 
@@ -244,7 +244,7 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
         Abc_ObjForEachFanout( pObj, pFanout, f )
         {
             // stop if there are too many fanouts
-            if ( f > 20 )
+            if ( p->pPars->nFanoutsMax && f > p->pPars->nFanoutsMax )
                 break;
             // skip nodes that are already added
             if ( Abc_NodeIsTravIdPrevious(pFanout) )
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index 3ed6436f..401c6edd 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -113,7 +113,7 @@ void Mfs_ManPrint( Mfs_Man_t * p )
     if ( p->pPars->fResub )
     {
         printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n",
-            Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts );
+            p->nTotalNodesBeg, p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts );
 
         printf( "Attempts :   " );
         printf( "Remove %6d out of %6d (%6.2f %%)   ", p->nRemoves, p->nTryRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) );
@@ -137,7 +137,7 @@ void Mfs_ManPrint( Mfs_Man_t * p )
     else
     {
         printf( "Nodes = %d. Try = %d. Total mints = %d. Local DC mints = %d. Ratio = %5.2f.\n", 
-            Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nMintsTotal, p->nMintsTotal-p->nMintsCare, 
+            p->nTotalNodesBeg, p->nNodesTried, p->nMintsTotal, p->nMintsTotal-p->nMintsCare, 
             1.0 * (p->nMintsTotal-p->nMintsCare) / p->nMintsTotal );
 //        printf( "Average ratio of sequential DCs in the global space = %5.2f.\n", 
 //            1.0-(p->dTotalRatios/p->nNodesTried) );
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index 0ecd0f67..85eb8140 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) < 200;// || pNode->Id == 556;
+    int fVeryVerbose = 0;//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;
@@ -180,9 +180,9 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
     if ( p->pPars->fVeryVerbose )
     {
 //        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), 
+        printf( "%5d : Lev =%3d. Leaf =%3d. Node =%3d. Divs =%3d.  Fanin = %4d (%d/%d), MFFC = %d\n", 
+            pNode->Id, pNode->Level, Vec_PtrSize(p->vSupp), Vec_PtrSize(p->vNodes), Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode), 
+            Abc_ObjFaninId(pNode, iFanin), iFanin, Abc_ObjFaninNum(pNode), 
             Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 );
     }
 
diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index c34ae859..31519c8e 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -42,18 +42,18 @@ typedef struct Sfm_Ntk_t_ Sfm_Ntk_t;
 typedef struct Sfm_Par_t_ Sfm_Par_t;
 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 window size
-    int           nDivNumMax;    // the maximum number of divisors
-    int           nBTLimit;      // the maximum number of conflicts in one SAT run
-    int           fFixLevel;     // does not allow level to increase
-    int           fRrOnly;       // perform redundance removal
-    int           fArea;         // performs optimization for area
-    int           fMoreEffort;   // performs high-affort minimization
-    int           fVerbose;      // enable basic stats
-    int           fVeryVerbose;  // enable detailed stats
+    int             nTfoLevMax;    // the maximum fanout levels
+    int             nFanoutMax;    // the maximum number of fanouts
+    int             nDepthMax;     // the maximum depth to try
+    int             nWinSizeMax;   // the maximum window size
+    int             nDivNumMax;    // the maximum number of divisors
+    int             nBTLimit;      // the maximum number of conflicts in one SAT run
+    int             fFixLevel;     // does not allow level to increase
+    int             fRrOnly;       // perform redundance removal
+    int             fArea;         // performs optimization for area
+    int             fMoreEffort;   // performs high-affort minimization
+    int             fVerbose;      // enable basic stats
+    int             fVeryVerbose;  // enable detailed stats
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -75,6 +75,7 @@ extern Vec_Int_t *  Sfm_NodeReadFanins( 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 );
 extern int          Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i );
+extern Vec_Int_t *  Sfm_NodeReadCover( Sfm_Ntk_t * p );
 /*=== sfmSat.c ==========================================================*/
 
 
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
index 9d96a1ac..67cbaa3a 100644
--- a/src/opt/sfm/sfmCore.c
+++ b/src/opt/sfm/sfmCore.c
@@ -33,7 +33,7 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Setup parameter structure.]
 
   Description []
 
@@ -46,7 +46,7 @@ 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->nFanoutMax   =   30;  // the maximum number of fanouts
     pPars->nDepthMax    =   20;  // the maximum depth to try  
     pPars->nWinSizeMax  =  300;  // the maximum window size
     pPars->nDivNumMax   =  300;  // the maximum number of divisors
@@ -61,7 +61,7 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Prints statistics.]
 
   Description []
 
@@ -73,12 +73,12 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
 void Sfm_NtkPrintStats( Sfm_Ntk_t * p )
 {
     p->timeOther = p->timeTotal - p->timeWin - p->timeDiv - p->timeCnf - p->timeSat;
-    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( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d. MaxDivs = %d.\n",
+        Sfm_NtkNodeNum(p), p->nNodesTried, p->nRemoves + p->nResubs, p->nTotalDivs, p->nSatCalls, p->nTimeOuts, p->nMaxDivs );
 
     printf( "Attempts :   " );
-    printf( "Remove %6d out of %6d (%6.2f %%)   ", p->nRemoves, p->nTryRemoves, p->nRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) );
-    printf( "Resub  %6d out of %6d (%6.2f %%)   ", p->nResubs,  p->nTryResubs,  p->nResubs,  100.0*p->nResubs /Abc_MaxInt(1, p->nTryResubs)  );
+    printf( "Remove %6d out of %6d (%6.2f %%)   ", p->nRemoves, p->nTryRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) );
+    printf( "Resub  %6d out of %6d (%6.2f %%)   ", p->nResubs,  p->nTryResubs,  100.0*p->nResubs /Abc_MaxInt(1, p->nTryResubs)  );
     printf( "\n" );
 
     printf( "Reduction:   " );
@@ -92,6 +92,7 @@ void Sfm_NtkPrintStats( Sfm_Ntk_t * p )
     ABC_PRTP( "Sat", p->timeSat  ,  p->timeTotal );
     ABC_PRTP( "Oth", p->timeOther,  p->timeTotal );
     ABC_PRTP( "ALL", p->timeTotal,  p->timeTotal );
+//    ABC_PRTP( "   ", p->time1    ,  p->timeTotal );
 }
 
 /**Function*************************************************************
@@ -108,22 +109,18 @@ void Sfm_NtkPrintStats( Sfm_Ntk_t * p )
 int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly )
 {
     int fSkipUpdate  = 0;
-    int fVeryVerbose = p->pPars->fVeryVerbose && Vec_IntSize(p->vDivs) < 200;// || pNode->Id == 556;
+    int fVeryVerbose = 0;//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 ( iNode == 211 )
-    {
-        int i = 0;
-    }
     p->nTryRemoves++;
     // report init stats
     if ( p->pPars->fVeryVerbose )
-        printf( "%5d : Lev =%3d. Leaf =%3d.  Node =%3d.  Div=%3d.  Fanin = %d/%d. MFFC = %d\n", 
-            iNode, Sfm_ObjLevel(p, iNode), Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vDivs), f, Sfm_ObjFaninNum(p, iNode), 
-            Sfm_ObjFanoutNum(p, Sfm_ObjFanin(p, iNode, f)) == 1 ? Sfm_ObjMffcSize(p, iNode) : 0 );
+        printf( "%5d : Lev =%3d. Leaf =%3d.  Node =%3d.  Div=%3d.  Fanin =%4d (%d/%d). MFFC = %d\n", 
+            iNode, Sfm_ObjLevel(p, iNode), Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vDivs), 
+            Sfm_ObjFanin(p, iNode, f), f, Sfm_ObjFaninNum(p, iNode), Sfm_ObjMffcSize(p, Sfm_ObjFanin(p, iNode, f)) );
     // clean simulation info
     p->nCexes = 0;
     Vec_WrdFill( p->vDivCexes, Vec_IntSize(p->vDivs), 0 );
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index bdb1c600..8b0072f1 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -84,8 +84,7 @@ struct Sfm_Ntk_t_
     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
+    sat_solver *      pSat;        // SAT solver
     int               nSatVars;    // the number of variables
     int               nTryRemoves; // number of fanin removals
     int               nTryResubs;  // number of resubstitutions
@@ -95,11 +94,11 @@ 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 *       vOrder;      // object order
     Vec_Int_t *       vDivVars;    // divisor SAT variables
     Vec_Int_t *       vDivIds;     // divisors indexes
     Vec_Int_t *       vLits;       // literals
+    Vec_Int_t *       vValues;     // SAT variable values
     Vec_Wec_t *       vClauses;    // CNF clauses for the node
     Vec_Int_t *       vFaninMap;   // mapping fanins into their SAT vars
     // nodes
@@ -111,6 +110,7 @@ struct Sfm_Ntk_t_
     int               nTotalDivs;
     int               nSatCalls;
     int               nTimeOuts;
+    int               nMaxDivs;
     // runtime
     clock_t           timeWin;
     clock_t           timeDiv;
@@ -118,6 +118,7 @@ struct Sfm_Ntk_t_
     clock_t           timeSat;
     clock_t           timeOther;
     clock_t           timeTotal;
+//    clock_t           time1;
 };
 
 static inline int  Sfm_NtkPiNum( Sfm_Ntk_t * p )                        { return p->nPis;                                   }
@@ -135,8 +136,8 @@ 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_ObjRefIncrement( Sfm_Ntk_t * p, int iObj )       { return ++Sfm_ObjFoArray(p, iObj)->nSize;          } 
+static inline int  Sfm_ObjRefDecrement( Sfm_Ntk_t * p, int iObj )       { return --Sfm_ObjFoArray(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);     }
diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c
index 53ec4153..3783e368 100644
--- a/src/opt/sfm/sfmNtk.c
+++ b/src/opt/sfm/sfmNtk.c
@@ -169,13 +169,14 @@ void Sfm_NtkPrepare( Sfm_Ntk_t * p )
     p->vRoots    = Vec_IntAlloc( 1000 );
     p->vTfo      = Vec_IntAlloc( 1000 );
     p->vDivCexes = Vec_WrdStart( p->pPars->nDivNumMax );
-//    p->vFans     = Vec_IntAlloc( 100 );
     p->vOrder    = Vec_IntAlloc( 100 );
     p->vDivVars  = Vec_IntAlloc( 100 );
     p->vDivIds   = Vec_IntAlloc( 1000 );
     p->vLits     = Vec_IntAlloc( 100 );
+    p->vValues   = Vec_IntAlloc( 100 );
     p->vClauses  = Vec_WecAlloc( 100 );
     p->vFaninMap = Vec_IntAlloc( 10 );
+    p->pSat      = sat_solver_new();
 }
 void Sfm_NtkFree( Sfm_Ntk_t * p )
 {
@@ -200,15 +201,14 @@ void Sfm_NtkFree( Sfm_Ntk_t * p )
     Vec_IntFreeP( &p->vRoots );
     Vec_IntFreeP( &p->vTfo   );
     Vec_WrdFreeP( &p->vDivCexes );
-//    Vec_IntFreeP( &p->vFans );
     Vec_IntFreeP( &p->vOrder );
     Vec_IntFreeP( &p->vDivVars );
     Vec_IntFreeP( &p->vDivIds );
     Vec_IntFreeP( &p->vLits  );
+    Vec_IntFreeP( &p->vValues );
     Vec_WecFreeP( &p->vClauses );
     Vec_IntFreeP( &p->vFaninMap );
-    if ( p->pSat0 ) sat_solver_delete( p->pSat0 );
-    if ( p->pSat1 ) sat_solver_delete( p->pSat1 );
+    if ( p->pSat  ) sat_solver_delete( p->pSat );
     ABC_FREE( p );
 }
 
@@ -243,10 +243,6 @@ 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 ( iNode == 202 )
-    {
-        int s = 0;
-    }
     if ( Sfm_ObjFanoutNum(p, iNode) > 0 || Sfm_ObjIsPi(p, iNode) )
         return;
     assert( Sfm_ObjIsNode(p, iNode) );
@@ -272,6 +268,7 @@ void Sfm_NtkUpdateLevel_rec( Sfm_Ntk_t * p, int iNode )
 void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth )
 {
     int iFanin = Sfm_ObjFanin( p, iNode, f );
+    assert( iFanin != iFaninNew );
     // replace old fanin by new fanin
     assert( Sfm_ObjIsNode(p, iNode) );
     Sfm_NtkRemoveFanin( p, iNode, iFanin );
@@ -312,6 +309,10 @@ int Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i )
 {
     return (Sfm_ObjFaninNum(p, i) > 0) || (Sfm_ObjFanoutNum(p, i) > 0);
 }
+Vec_Int_t * Sfm_NodeReadCover( Sfm_Ntk_t * p )
+{
+    return p->vCover;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c
index 228a5fd8..bf6a06b0 100644
--- a/src/opt/sfm/sfmSat.c
+++ b/src/opt/sfm/sfmSat.c
@@ -54,18 +54,18 @@ static word s_Truths6[6] = {
 void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
 {
     Vec_Int_t * vClause;
-    int RetValue, Lit, iNode = -1, iFanin, i, k;
+    int RetValue, 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->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 );
+//    if ( p->pSat )
+//        printf( "%d  ", p->pSat->stats.learnts );
+    sat_solver_restart( p->pSat );
+    sat_solver_setnvars( p->pSat, 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_IntForEachEntry( p->vOrder, iNode, i )
         Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
-    // create divisor variables
+    // collect divisor variables
     Vec_IntClear( p->vDivVars );
     Vec_IntForEachEntry( p->vDivs, iNode, i )
         Vec_IntPush( p->vDivVars, Sfm_ObjSatVar(p, iNode) );
@@ -86,39 +86,15 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
         {
             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) );
+            RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
             assert( RetValue );
         }
     }
-//    Sat_SolverWriteDimacs( pSat0, "test.cnf", NULL, NULL, 0 );
-    // 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
-    RetValue = sat_solver_simplify( pSat0 );
+    RetValue = sat_solver_simplify( p->pSat );
     assert( RetValue );
-    RetValue = sat_solver_simplify( pSat1 );
-    if ( RetValue == 0 )
-    {
-        Sat_SolverWriteDimacs( pSat1, "test.cnf", NULL, NULL, 0 );
-    }
-    assert( RetValue );
-    // return the result
-    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;
-}
+} 
 
 /**Function*************************************************************
 
@@ -135,55 +111,59 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
 {
     word * pSign, uCube, uTruth = 0;
     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 );
+    int pLits[2], nVars = sat_solver_nvars( p->pSat );
+    sat_solver_setnvars( p->pSat, nVars + 1 );
+    pLits[0] = Abc_Var2Lit( Sfm_ObjSatVar(p, Vec_IntEntryLast(p->vNodes)), 0 ); // F = 1
+    pLits[1] = Abc_Var2Lit( nVars, 0 ); // iNewLit
     while ( 1 ) 
     {
         // find onset minterm
         p->nSatCalls++;
-        status = sat_solver_solve( p->pSat1, &iNewLit, &iNewLit + 1, p->pPars->nBTLimit, 0, 0, 0 );
+        status = sat_solver_solve( p->pSat, pLits, pLits + 2, 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 );
+        // remember variable values
+        Vec_IntClear( p->vValues );
+        Vec_IntForEachEntry( p->vDivVars, iVar, i )
+            Vec_IntPush( p->vValues, sat_solver_var_value(p->pSat, iVar) );
         // collect divisor literals
         Vec_IntClear( p->vLits );
+        Vec_IntPush( p->vLits, Abc_LitNot(pLits[0]) ); // F = 0
         Vec_IntForEachEntry( p->vDivIds, Div, i )
-            Vec_IntPush( p->vLits, sat_solver_var_literal(p->pSat1, Div) );
+            Vec_IntPush( p->vLits, sat_solver_var_literal(p->pSat, 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 );
+        status = sat_solver_solve( p->pSat, 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 )
             break;
         assert( status == l_False );
         // compute cube and add clause
-        nFinal = sat_solver_final( p->pSat0, &pFinal );
+        nFinal = sat_solver_final( p->pSat, &pFinal );
         uCube = ~(word)0;
         Vec_IntClear( p->vLits );
-        Vec_IntPush( p->vLits, Abc_LitNot(iNewLit) );
+        Vec_IntPush( p->vLits, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
         for ( i = 0; i < nFinal; i++ )
         {
+            if ( pFinal[i] == pLits[0] )
+                continue;
             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;
-        status = sat_solver_addclause( p->pSat1, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) );
+        status = sat_solver_addclause( p->pSat, 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 )
-        if ( sat_solver_var_value(p->pSat1, iVar) ^ sat_solver_var_value(p->pSat0, iVar) ) // insert 1
+        if ( Vec_IntEntry(p->vValues, i) ^ sat_solver_var_value(p->pSat, iVar) ) // insert 1
         {
             pSign = Vec_WrdEntryP( p->vDivCexes, i );
             assert( !Abc_InfoHasBit( (unsigned *)pSign, p->nCexes) );
@@ -207,8 +187,8 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
 void Sfm_ComputeInterpolantCheck( Sfm_Ntk_t * p )
 {
     int iNode = 3;
-    int iDiv0 = 5;
-    int iDiv1 = 4;
+    int iDiv0 = 6;
+    int iDiv1 = 7;
     word uTruth;
 //    int i;
 //    Sfm_NtkForEachNode( p, i )
diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c
index f96221c0..1d2919f9 100644
--- a/src/opt/sfm/sfmWin.c
+++ b/src/opt/sfm/sfmWin.c
@@ -89,6 +89,10 @@ int Sfm_ObjDeref( Sfm_Ntk_t * p, int iObj )
 int Sfm_ObjMffcSize( Sfm_Ntk_t * p, int iObj )
 {
     int Count1, Count2;
+    if ( Sfm_ObjIsPi(p, iObj) )
+        return 0;
+    if ( Sfm_ObjFanoutNum(p, iObj) != 1 )
+        return 0;
     assert( Sfm_ObjIsNode( p, iObj ) );
     Count1 = Sfm_ObjDeref( p, iObj );
     Count2 = Sfm_ObjRef( p, iObj );
@@ -182,10 +186,11 @@ int Sfm_NtkCheckFanouts( Sfm_Ntk_t * p, int iNode )
 void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode, int nLevelMax )
 {
     int i, iFanout;
-    if ( Sfm_ObjFanoutNum(p, iNode) > p->pPars->nFanoutMax )
-        return;
     Sfm_ObjForEachFanout( p, iNode, iFanout, i )
     {
+        // skip some of the fanouts if the number is large
+        if ( p->pPars->nFanoutMax && i > p->pPars->nFanoutMax )
+            break;
         // skip TFI nodes, PO nodes, or nodes with high logic level
         if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) || 
             (p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) >= nLevelMax) )
@@ -252,7 +257,8 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
         return 0;
     }
     // collect TFO (currently use only one level of TFO)
-    if ( Sfm_NtkCheckFanouts(p, iNode) )
+//    if ( Sfm_NtkCheckFanouts(p, iNode) )
+    if ( 0 )
     {
         Sfm_ObjForEachFanout( p, iNode, iTemp, i )
         {
@@ -268,10 +274,10 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
     clk = clock();
     // create ordering of the nodes
     Vec_IntClear( p->vOrder );
-    Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
-        Vec_IntPush( p->vOrder, iNode );
-    Vec_IntForEachEntry( p->vLeaves, iNode, i )
-        Vec_IntPush( p->vOrder, iNode );
+    Vec_IntForEachEntryReverse( p->vNodes, iTemp, i )
+        Vec_IntPush( p->vOrder, iTemp );
+    Vec_IntForEachEntry( p->vLeaves, iTemp, i )
+        Vec_IntPush( p->vOrder, iTemp );
     // mark fanins
     Sfm_NtkIncrementTravId2( p );
     Sfm_ObjSetTravIdCurrent2( p, iNode );
@@ -294,11 +300,17 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
         Vec_IntShrink( p->vDivs, k );
         assert( Vec_IntSize(p->vDivs) == p->pPars->nDivNumMax );
     }
+//Vec_IntPrint( p->vLeaves );
+//Vec_IntPrint( p->vNodes );
+//Vec_IntPrint( p->vDivs );
     // collect additional divisors of the TFI nodes
     if ( Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax )
     {
         int nStartNew = Vec_IntSize(p->vDivs);
         Sfm_NtkIncrementTravId2( p );
+        Sfm_ObjForEachFanin( p, iNode, iTemp, i )
+            if ( Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax )
+                Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) );
         Vec_IntForEachEntry( p->vDivs, iTemp, i )
             if ( Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax )
                 Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) );
@@ -309,6 +321,7 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
             Vec_IntPush( p->vOrder, iTemp );
     }
     assert( Vec_IntSize(p->vDivs) <= p->pPars->nDivNumMax );
+    p->nMaxDivs += (Vec_IntSize(p->vDivs) == p->pPars->nDivNumMax);
     // statistics
     p->nTotalDivs += Vec_IntSize(p->vDivs);
     p->timeDiv += clock() - clk;