New MFS package.

14 files changed, 930 insertions, 218 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index bd18200c..70646874 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -52,6 +52,7 @@
 #include "proof/abs/abs.h"
 #include "sat/bmc/bmc.h"
 #include "proof/ssc/ssc.h"
+#include "opt/sfm/sfm.h"
 
 #ifndef _WIN32
 #include <unistd.h>
@@ -104,6 +105,7 @@ static int Abc_CommandLutpack                ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandLutmin                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandImfs                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMfs                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandMfs2                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTrace                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSpeedup                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPowerdown              ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -607,6 +609,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "lutmin",        Abc_CommandLutmin,           1 );
 //    Cmd_CommandAdd( pAbc, "Synthesis",    "imfs",          Abc_CommandImfs,             1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "mfs",           Abc_CommandMfs,              1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "mfs2",          Abc_CommandMfs2,             1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "trace",         Abc_CommandTrace,            0 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "speedup",       Abc_CommandSpeedup,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "powerdown",     Abc_CommandPowerdown,        1 );
@@ -4400,6 +4403,146 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern int Abc_NtkPerformMfs( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars );
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    Sfm_Par_t Pars, * pPars = &Pars;
+    int c;
+    // set defaults
+    Sfm_ParSetDefault( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMClaevwh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nTfoLevMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nTfoLevMax < 0 )
+                goto usage;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFanoutMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFanoutMax < 1 )
+                goto usage;
+            break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nDepthMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nDepthMax < 0 )
+                goto usage;
+            break;
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nWinSizeMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nWinSizeMax < 0 )
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBTLimit < 0 )
+                goto usage;
+            break;
+        case 'l':
+            pPars->fFixLevel ^= 1;
+            break;
+        case 'a':
+            pPars->fArea ^= 1;
+            break;
+        case 'e':
+            pPars->fMoreEffort ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'w':
+            pPars->fVeryVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( -1, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsLogic(pNtk) )
+    {
+        Abc_Print( -1, "This command can only be applied to a logic network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsSopLogic(pNtk) )
+    {
+        Abc_Print( -1, "Currently this command works only for SOP logic networks (run \"sop\").\n" );
+        return 1;
+    }
+    // modify the current network
+    if ( !Abc_NtkPerformMfs( pNtk, pPars ) )
+    {
+        Abc_Print( -1, "Resynthesis has failed.\n" );
+        return 1;
+    }
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: mfs2 [-WFDMC <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-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" );
+    Abc_Print( -2, "\t-e       : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" );
+    Abc_Print( -2, "\t-v       : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w       : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : print the command usage\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abcMfs.c b/src/base/abci/abcMfs.c
new file mode 100644
index 00000000..ddc91467
--- /dev/null
+++ b/src/base/abci/abcMfs.c
@@ -0,0 +1,189 @@
+/**CFile****************************************************************
+
+  FileName    [abcMfs.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Optimization with don't-cares.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcMfs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "base/abc/abc.h"
+#include "opt/sfm/sfm.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkAssignIDs( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj;
+    int i;
+    vNodes = Abc_NtkDfs( pNtk, 0 );
+    Abc_NtkCleanCopy( pNtk );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        pObj->iTemp = i;
+    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+        pObj->iTemp = Abc_NtkPiNum(pNtk) + i;
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        pObj->iTemp = Abc_NtkPiNum(pNtk) + Vec_PtrSize(vNodes) + i;
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Extracts information about the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Vec_Wec_t * vFanins;
+    Vec_Str_t * vFixed;
+    Vec_Wrd_t * vTruths;
+    Vec_Int_t * vArray;
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k, nObjs;
+    vNodes  = Abc_NtkAssignIDs( pNtk );
+    nObjs   = Abc_NtkPiNum(pNtk) + Vec_PtrSize(vNodes) + Abc_NtkPoNum(pNtk);
+    vFanins = Vec_WecStart( nObjs );
+    vFixed  = Vec_StrStart( nObjs );
+    vTruths = Vec_WrdStart( nObjs );
+    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+    {
+        vArray = Vec_WecEntry( vFanins, pObj->iTemp );
+        Vec_IntGrow( vArray, Abc_ObjFaninNum(pObj) );
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            Vec_IntPush( vArray, pFanin->iTemp );
+        Vec_WrdWriteEntry( vTruths, pObj->iTemp, Abc_SopToTruth((char *)pObj->pData, Abc_ObjFaninNum(pObj)) );
+    }
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        vArray = Vec_WecEntry( vFanins, pObj->iTemp );
+        Vec_IntGrow( vArray, Abc_ObjFaninNum(pObj) );
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            Vec_IntPush( vArray, pFanin->iTemp );
+    }
+    Vec_PtrFree( vNodes );
+    return Sfm_NtkConstruct( vFanins, Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk), vFixed, vTruths );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p )
+{
+    Vec_Int_t * vMap, * vArray;
+    Abc_Obj_t * pNode;
+    int i, k, Fanin;
+    // map new IDs into old nodes
+    vMap = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
+    Abc_NtkForEachPi( pNtk, pNode, i )
+        Vec_IntWriteEntry( vMap, pNode->iTemp, Abc_ObjId(pNode) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( pNode->iTemp > 0 )
+            Vec_IntWriteEntry( vMap, pNode->iTemp, Abc_ObjId(pNode) );
+    // remove old fanins
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        Abc_ObjRemoveFanins( pNode );
+    // create new fanins
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( pNode->iTemp > 0 && !Sfm_NodeReadFixed(p, pNode->iTemp) )
+        {
+            vArray = Sfm_NodeReadFanins( p, pNode->iTemp );
+            Vec_IntForEachEntry( vArray, Fanin, k )
+                Abc_ObjAddFanin( pNode, Abc_NtkObj(pNtk, Vec_IntEntry(vMap, Fanin)) );
+            pNode->pData = Abc_SopCreateFromTruth( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), (unsigned *)Sfm_NodeReadTruth(p, pNode->iTemp) );
+        }
+    Vec_IntFree( vMap );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkPerformMfs( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
+{
+    Sfm_Ntk_t * p;
+    int nFaninMax, nNodes;
+    assert( Abc_NtkIsSopLogic(pNtk) );
+    // count fanouts
+    nFaninMax = Abc_NtkGetFaninMax( pNtk );
+    if ( nFaninMax > 6 )
+    {
+        Abc_Print( 1, "Currently \"mfs\" cannot process the network containing nodes with more than 6 fanins.\n" );
+        return 0;
+    }
+    // collect information
+    p = Abc_NtkExtractMfs( pNtk );
+    // perform optimization
+    nNodes = Sfm_NtkPerform( p, pPars );
+    // call the fast extract procedure
+    if ( nNodes == 0 )
+        Abc_Print( 1, "The networks is not changed by \"mfs\".\n" );
+    else
+    {
+        Abc_NtkInsertMfs( pNtk, p );
+        Abc_Print( 1, "The networks has %d nodes changed by \"mfs\".\n", nNodes );
+    }
+    Sfm_NtkFree( p );
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 89e1849b..c7645775 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -30,6 +30,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcLutmin.c \
     src/base/abci/abcMap.c \
     src/base/abci/abcMerge.c \
+    src/base/abci/abcMfs.c \
     src/base/abci/abcMini.c \
     src/base/abci/abcMiter.c \
     src/base/abci/abcMulti.c \
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index a99e6f29..c821d121 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -255,6 +255,12 @@ static inline Vec_Int_t * Vec_IntDupArray( Vec_Int_t * pVec )
   SeeAlso     []
 
 ***********************************************************************/
+static inline void Vec_IntZero( Vec_Int_t * p )
+{
+    p->pArray = NULL;
+    p->nSize = 0;
+    p->nCap = 0;
+}
 static inline void Vec_IntErase( Vec_Int_t * p )
 {
     ABC_FREE( p->pArray );
diff --git a/src/misc/vec/vecWec.h b/src/misc/vec/vecWec.h
index 8a924f90..ece7b0a1 100644
--- a/src/misc/vec/vecWec.h
+++ b/src/misc/vec/vecWec.h
@@ -245,6 +245,7 @@ static inline void Vec_WecClear( Vec_Wec_t * p )
     int i;
     Vec_WecForEachLevel( p, vVec, i )
         Vec_IntClear( vVec );
+    p->nSize = 0;
 }
 
 /**Function*************************************************************
@@ -315,10 +316,9 @@ static inline double Vec_WecMemory( Vec_Wec_t * p )
 ***********************************************************************/
 static inline void Vec_WecFree( Vec_Wec_t * p )
 {
-    Vec_Int_t * vVec;
     int i;
-    Vec_WecForEachLevel( p, vVec, i )
-        ABC_FREE( vVec->pArray );
+    for ( i = 0; i < p->nCap; i++ )
+        ABC_FREE( p->pArray[i].pArray );
     ABC_FREE( p->pArray );
     ABC_FREE( p );
 }
@@ -643,6 +643,8 @@ static inline void Vec_WecRemoveEmpty( Vec_Wec_t * vCubes )
             vCubes->pArray[k++] = *vCube;
         else
             ABC_FREE( vCube->pArray );
+    for ( i = k; i < Vec_WecSize(vCubes); i++ )
+        Vec_IntZero( Vec_WecEntry(vCubes, i) );
     Vec_WecShrink( vCubes, k );
 //    Vec_WecSortByFirstInt( vCubes, 0 );
 }
diff --git a/src/opt/sfm/module.make b/src/opt/sfm/module.make
index 9d952aaf..b78355e1 100644
--- a/src/opt/sfm/module.make
+++ b/src/opt/sfm/module.make
@@ -1,5 +1,5 @@
 SRC +=    src/opt/sfm/sfmCnf.c \
     src/opt/sfm/sfmCore.c \
-    src/opt/sfm/sfmMan.c \
     src/opt/sfm/sfmNtk.c \
-    src/opt/sfm/sfmSat.c
+    src/opt/sfm/sfmSat.c \
+    src/opt/sfm/sfmWin.c
diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index 42f8156a..deb055c5 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -26,6 +26,8 @@
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
+#include "misc/vec/vecWec.h"
+
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
@@ -36,26 +38,18 @@ ABC_NAMESPACE_HEADER_START
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Sfm_Man_t_ Sfm_Man_t;
 typedef struct Sfm_Ntk_t_ Sfm_Ntk_t;
 typedef struct Sfm_Par_t_ Sfm_Par_t;
 struct Sfm_Par_t_
 {
-    int           nWinTfoLevs;   // the maximum fanout levels
-    int           nFanoutsMax;   // the maximum number of fanouts
-    int           nDepthMax;     // the maximum number of logic levels
-    int           nDivMax;       // the maximum number of divisors
-    int           nWinSizeMax;   // the maximum size of the window
-    int           nGrowthLevel;  // the maximum allowed growth in level
+    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           nBTLimit;      // the maximum number of conflicts in one SAT run
-    int           fResub;        // performs resubstitution
+    int           fFixLevel;     // does not allow level to increase
     int           fArea;         // performs optimization for area
     int           fMoreEffort;   // performs high-affort minimization
-    int           fSwapEdge;     // performs edge swapping
-    int           fOneHotness;   // adds one-hotness conditions
-    int           fDelay;        // performs optimization for delay
-    int           fPower;        // performs power-aware optimization
-    int           fGiaSat;       // use new SAT solver
     int           fVerbose;      // enable basic stats
     int           fVeryVerbose;  // enable detailed stats
 };
@@ -70,13 +64,14 @@ struct Sfm_Par_t_
 
 /*=== sfmCnf.c ==========================================================*/
 /*=== sfmCore.c ==========================================================*/
-extern int          Sfm_ManPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars );
-/*=== sfmMan.c ==========================================================*/
-extern Sfm_Man_t *  Sfm_ManAlloc( Sfm_Ntk_t * p );
-extern void         Sfm_ManFree( Sfm_Man_t * p );
+extern void         Sfm_ParSetDefault( Sfm_Par_t * pPars );
+extern int          Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars );
 /*=== sfmNtk.c ==========================================================*/
-extern Sfm_Ntk_t *  Sfm_NtkAlloc( int nPis, int nPos, int nNodes, Vec_Int_t * vFanins, Vec_Int_t * vFanouts, Vec_Int_t * vEdges, Vec_Int_t * vOpts );
+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 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 6b152524..825c336b 100644
--- a/src/opt/sfm/sfmCnf.c
+++ b/src/opt/sfm/sfmCnf.c
@@ -43,13 +43,38 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
+void Sfm_PrintCnf( Vec_Str_t * vCnf )
+{
+    char Entry;
+    int i, Lit;
+    Vec_StrForEachEntry( vCnf, Entry, i )
+    {
+        Lit = (int)Entry;
+        if ( Lit == -1 )
+            printf( "\n" );
+        else
+            printf( "%s%d ", Abc_LitIsCompl(Lit) ? "-":"", Abc_Lit2Var(Lit) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
 {
     Vec_StrClear( vCnf );
     if ( Truth == 0 || ~Truth == 0 )
     {
         Vec_StrPush( vCnf, (char)(Truth == 0) );
-        Vec_StrPush( vCnf, -1 );
+        Vec_StrPush( vCnf, (char)-1 );
         return 1;
     }
     else 
@@ -74,7 +99,7 @@ int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf
                         assert( 0 );
                 }
                 Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) );
-                Vec_StrPush( vCnf, -1 );
+                Vec_StrPush( vCnf, (char)-1 );
             }
         }
         return nCubes;
@@ -92,30 +117,25 @@ int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf
   SeeAlso     []
 
 ***********************************************************************/
-int Sfm_DeriveCnfs( Vec_Wrd_t * vTruths, Vec_Int_t * vFanins, Vec_Str_t ** pvCnfs, Vec_Int_t ** pvOffsets )
+void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap )
 {
-    Vec_Str_t * vCnfs, * vCnf;
-    Vec_Int_t * vOffsets, * vCover;
-    int i, k, nFanins, nClauses = 0;
-    vCnf     = Vec_StrAlloc( 1000 );
-    vCnfs    = Vec_StrAlloc( 1000 );
-    vOffsets = Vec_IntAlloc( Vec_IntSize(vFanins) );
-    vCover   = Vec_IntAlloc( 1 << 16 );
-    assert( Vec_WrdSize(vTruths) == Vec_IntSize(vFanins) );
-    Vec_IntForEachEntry( vFanins, nFanins, i )
+    Vec_Int_t * vClause;
+    int i, Lit;
+    char Entry;
+    Vec_WecClear( vRes );
+    vClause = Vec_WecPushLevel( vRes );
+    Vec_StrForEachEntry( vCnf, Entry, i )
     {
-        nClauses += Sfm_TruthToCnf( Vec_WrdEntry(vTruths, i), nFanins, vCover, vCnf );
-        Vec_IntPush( vOffsets, Vec_StrSize(vCnfs) );
-        for ( k = 0; k < Vec_StrSize(vCnf); k++ )
-            Vec_StrPush( vCnfs, Vec_StrEntry(vCnf, k) );
+        Lit = (int)Entry;
+        if ( Lit == -1 )
+        {
+            vClause = Vec_WecPushLevel( vRes );
+            continue;
+        }
+        Vec_IntPush( vClause, Abc_Lit2LitV( Vec_IntArray(vFaninMap), Lit ) );
     }
-    Vec_IntPush( vOffsets, Vec_StrSize(vCnfs) );
-    Vec_StrFree( vCnf );
-    Vec_IntFree( vCover );
-    return nClauses;
 }
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
index 351b4ef9..a8ff1e21 100644
--- a/src/opt/sfm/sfmCore.c
+++ b/src/opt/sfm/sfmCore.c
@@ -36,14 +36,73 @@ ABC_NAMESPACE_IMPL_START
   Synopsis    []
 
   Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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->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
+    pPars->fMoreEffort  =    0;  // performs high-affort minimization
+    pPars->fVerbose     =    0;  // enable basic stats
+    pPars->fVeryVerbose =    0;  // enable detailed stats
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sfm_NtkPrepare( 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->vLits   = Vec_IntAlloc( 100 );
+    p->vClauses  = Vec_WecAlloc( 100 );
+    p->vFaninMap = Vec_IntAlloc( 10 );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Sfm_ManPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
+int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
 {
+    int i;
+    p->pPars = pPars;
+    Sfm_NtkPrepare( p );
+    Sfm_NtkForEachNode( p, i )
+    {
+        printf( "Node %d:\n", i );
+        Sfm_PrintCnf( (Vec_Str_t *)Vec_WecEntry(p->vCnfs, i) );
+        printf( "\n" );
+    }
     return 0;
 }
 
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index 9dad053f..d52b46e4 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -32,6 +32,7 @@
 #include <assert.h>
 
 #include "misc/vec/vec.h"
+#include "sat/bsat/satSolver.h"
 #include "sfm.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -46,72 +47,88 @@ ABC_NAMESPACE_HEADER_START
 
 struct Sfm_Ntk_t_
 {
+    // parameters
+    Sfm_Par_t *       pPars;    // parameters
     // objects
-    int *             pMem;   // memory for objects
-    Vec_Int_t         vObjs;  // ObjId -> Offset
-    Vec_Int_t         vPis;   // PiId -> ObjId
-    Vec_Int_t         vPos;   // PoId -> ObjId
-    // fanins/fanouts
-    Vec_Int_t         vMem;   // memory for overflow fanin/fanouts
+    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_Wec_t *       vFanins;  // fanins
+    Vec_Str_t *       vFixed;   // persistent objects
+    Vec_Wrd_t *       vTruths;  // truth tables
     // attributes
-    Vec_Int_t         vLevels;
-    Vec_Int_t         vTravIds;
-    Vec_Int_t         vSatVars;
-    Vec_Wrd_t         vTruths;
-};
-
-typedef struct Sfm_Obj_t_ Sfm_Obj_t;
-struct Sfm_Obj_t_
-{
-    unsigned          Type   :  2;
-    unsigned          Id     : 30;
-    unsigned          fOpt   :  1;
-    unsigned          fTfo   :  1;
-    unsigned          nFanis :  4;
-    unsigned          nFanos : 26;
-    int               Fanio[0];
-};
-
-struct Sfm_Man_t_
-{
-    Sfm_Ntk_t *       pNtk;
+    Vec_Wec_t *       vFanouts; // fanouts
+    Vec_Int_t *       vLevels;  // logic level
+    Vec_Int_t         vTravIds; // traversal IDs
+    Vec_Int_t         vId2Var;  // ObjId -> SatVar
+    Vec_Int_t         vVar2Id;  // SatVar -> ObjId
+    Vec_Wec_t *       vCnfs;    // CNFs
+    Vec_Int_t *       vCover;   // temporary
+    int               nTravIds; // traversal IDs
     // window
-    Sfm_Obj_t *       pNode;
-    Vec_Int_t *       vLeaves;      // leaves 
-    Vec_Int_t *       vRoots;       // roots
-    Vec_Int_t *       vNodes;       // internal
-    Vec_Int_t *       vTfo;         // TFO (including pNode)
+    int               iNode;
+    Vec_Int_t *       vLeaves;  // leaves 
+    Vec_Int_t *       vRoots;   // roots
+    Vec_Int_t *       vNodes;   // internal
+    Vec_Int_t *       vTfo;     // TFO (excluding iNode)
     // SAT solving
+    int               nSatVars; // the number of variables
+    sat_solver *      pSat1;    // SAT solver for the on-set
+    sat_solver *      pSat0;    // SAT solver for the off-set
+    // intermediate data
+    Vec_Int_t *       vDivs;    // divisors
+    Vec_Int_t *       vLits;    // literals
+    Vec_Int_t *       vFani;    // iterator fanins
+    Vec_Int_t *       vFano;    // iterator fanouts
+    Vec_Wec_t *       vClauses; // CNF clauses for the node
+    Vec_Int_t *       vFaninMap;// mapping fanins into their SAT vars
 };
 
+#define SFM_SAT_UNDEC 0x1234567812345678
+#define SFM_SAT_SAT   0x8765432187654321
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline Sfm_Obj_t * Sfm_ManObj( Sfm_Ntk_t * p, int Id ) { return (Sfm_Obj_t *)Vec_IntEntryP( &p->vObjs, Id ); }
+#define Sfm_NtkForEachNode( p, i )                for ( i = p->nPis; i + p->nPos < p->nObjs; i++ )
+#define Sfm_NodeForEachFanin( p, Node, Fan, i )   for ( p->vFani = Vec_WecEntry(p->vFanins,  Node), i = 0; i < Vec_IntSize(p->vFani) && ((Fan = Vec_IntEntry(p->vFani, i)), 1); i++ )
+#define Sfm_NodeForEachFanout( p, Node, Fan, i )  for ( p->vFano = Vec_WecEntry(p->vFanouts, Node), i = 0; i < Vec_IntSize(p->vFani) && ((Fan = Vec_IntEntry(p->vFano, i)), 1); i++ )
+
+static inline int  Sfm_ObjIsPi( Sfm_Ntk_t * p, int i )      { return i < p->nPis;                               }
+static inline int  Sfm_ObjIsPo( Sfm_Ntk_t * p, int i )      { return i + p->nPos < p->nObjs;                    }
+static inline int  Sfm_ObjIsNode( Sfm_Ntk_t * p, int i )    { return i >= p->nPis && i + p->nPos < p->nObjs;    }
+
+static inline int  Sfm_ObjFaninNum( Sfm_Ntk_t * p, int i )  { return Vec_IntSize(Vec_WecEntry(p->vFanins, i));  }
+static inline int  Sfm_ObjFanoutNum( Sfm_Ntk_t * p, int i ) { return Vec_IntSize(Vec_WecEntry(p->vFanouts, i)); }
+
+static inline int  Sfm_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 ); }
 
-#define Sfm_ManForEachObj( p, pObj, i )                                \
-    for ( i = 0; (i < Vec_IntSize(&p->vObjs) && ((pObj) = Sfm_ManObj(p, i))); i++ )
-#define Sfm_ManForEachPi( p, pObj, i )                                 \
-    for ( i = 0; (i < Vec_IntSize(&p->vPis) && ((pObj) = Sfm_ManObj(p, Vec_IntEntry(&p->vPis, i)))); i++ )
-#define Sfm_ManForEachPo( p, pObj, i )                                 \
-    for ( i = 0; (i < Vec_IntSize(&p->vPos) && ((pObj) = Sfm_ManObj(p, Vec_IntEntry(&p->vPos, i)))); i++ )
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /*=== sfmCnf.c ==========================================================*/
-extern int          Sfm_DeriveCnfs( Vec_Wrd_t * vTruths, Vec_Int_t * vFanins, Vec_Str_t ** pvCnfs, Vec_Int_t ** pvOffsets );
+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 void         Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap );
 /*=== sfmCore.c ==========================================================*/
-/*=== sfmMan.c ==========================================================*/
 /*=== sfmNtk.c ==========================================================*/
+extern Sfm_Ntk_t *  Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPos );
 /*=== sfmSat.c ==========================================================*/
-extern int          Sfm_CreateSatWindow( Sfm_Ntk_t * p );
-
-ABC_NAMESPACE_HEADER_END
+extern word         Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_t * vDivs, Vec_Int_t * vLits, Vec_Int_t * vDiffs, int nBTLimit );
+/*=== sfmWin.c ==========================================================*/
+extern int          Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode );
+extern void         Sfm_NtkWin2Sat( Sfm_Ntk_t * p );
 
 
+ABC_NAMESPACE_HEADER_END
 
 #endif
 
diff --git a/src/opt/sfm/sfmMan.c b/src/opt/sfm/sfmMan.c
deleted file mode 100644
index 90cfe42e..00000000
--- a/src/opt/sfm/sfmMan.c
+++ /dev/null
@@ -1,59 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [sfmMan.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [SAT-based optimization using internal don't-cares.]
-
-  Synopsis    [Manager maintenance.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: sfmMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "sfmInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Sfm_Man_t *  Sfm_ManAlloc( Sfm_Ntk_t * p )
-{
-    return NULL;
-}
-void Sfm_ManFree( Sfm_Man_t * p )
-{
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c
index 21252e60..602f6d75 100644
--- a/src/opt/sfm/sfmNtk.c
+++ b/src/opt/sfm/sfmNtk.c
@@ -42,87 +42,202 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-Sfm_Ntk_t * Sfm_NtkAlloc( int nPis, int nPos, int nNodes, Vec_Int_t * vFanins, Vec_Int_t * vFanouts, Vec_Int_t * vEdges, Vec_Int_t * vOpts )
+void Sfm_CheckConsistency( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed )
 {
-    Sfm_Ntk_t * p;
-    Sfm_Obj_t * pObj, * pFan;
-    int i, k, nObjSize, AddOn = 2;
-    int nStructSize = sizeof(Sfm_Obj_t) / sizeof(int);
-    int iFanin, iOffset = 2, iFanOffset = 0;
-    int nEdges = Vec_IntSize(vEdges);
-    int nObjs  = nPis + nPos + nNodes;
-    int nSize  = 2 + nObjs * (nStructSize + 1) + 2 * nEdges + AddOn * (nPis + Vec_IntSum(vOpts));
-    assert( sizeof(Sfm_Obj_t) % sizeof(int) == 0 );
-    assert( nEdges == Vec_IntSum(vFanins) );
-    assert( nEdges == Vec_IntSum(vFanouts) );
-    p = ABC_CALLOC( Sfm_Ntk_t, 1 );
-    p->pMem = ABC_CALLOC( int, nSize );
-    for ( i = 0; i < nObjs; i++ )
+    Vec_Int_t * vArray;
+    int i, k, Fanin;
+    // check entries
+    Vec_WecForEachLevel( vFanins, vArray, i )
     {
-        Vec_IntPush( &p->vObjs, iOffset );
-        pObj = Sfm_ManObj( p, i );
-        pObj->Id  = i;
+        // PIs have no fanins
         if ( i < nPis )
-        {
-            pObj->Type = 1;
-            assert( Vec_IntEntry(vFanins, i) == 0 );
-            assert( Vec_IntEntry(vOpts, i) == 0 );
-            Vec_IntPush( &p->vPis, iOffset );
-        }
-        else 
-        {
-            pObj->Type = 2;
-            pObj->fOpt = Vec_IntEntry(vOpts, i);
-            if ( i >= nPis + nNodes ) // PO
-            {
-                pObj->Type = 3;
-                assert( Vec_IntEntry(vFanins, i) == 1 );
-                assert( Vec_IntEntry(vFanouts, i) == 0 );
-                assert( Vec_IntEntry(vOpts, i) == 0 );
-                Vec_IntPush( &p->vPos, iOffset );
-            }
-            for ( k = 0; k < Vec_IntEntry(vFanins, i); k++ )
-            {
-                iFanin = Vec_IntEntry( vEdges, iFanOffset++ );
-                pFan = Sfm_ManObj( p, iFanin );
-                assert( iFanin < i );
-                pObj->Fanio[ pObj->nFanis++ ] = iFanin;
-                pFan->Fanio[ pFan->nFanis + pFan->nFanos++ ] = i;
-            }
-        }
-        // add node size
-        nObjSize  = nStructSize + Vec_IntEntry(vFanins, i) + Vec_IntEntry(vFanouts, i) + AddOn * (pObj->Type==1 || pObj->fOpt);
-        nObjSize += (int)( nObjSize & 1 );
-        assert( (nObjSize & 1) == 0 );
-        iOffset  += nObjSize;
+            assert( Vec_IntSize(vArray) == 0 && Vec_StrEntry(vFixed, i) == (char)0 );
+        // nodes are in a topo order; POs cannot be fanins
+        Vec_IntForEachEntry( vArray, Fanin, k )
+            assert( Fanin < i && Fanin + nPos < Vec_WecSize(vFanins) );
+        // POs have one fanout
+        if ( i + nPos >= Vec_WecSize(vFanins) )
+            assert( Vec_IntSize(vArray) == 1 && Vec_StrEntry(vFixed, i) == (char)0 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wec_t * Sfm_CreateFanout( Vec_Wec_t * vFanins )
+{
+    Vec_Wec_t * vFanouts;
+    Vec_Int_t * vArray;
+    int i, k, Fanin;
+    // count fanouts
+    vFanouts = Vec_WecStart( Vec_WecSize(vFanins) );
+    Vec_WecForEachLevel( vFanins, vArray, i )
+        Vec_IntForEachEntry( vArray, Fanin, k )
+            Vec_WecEntry( vFanouts, Fanin )->nSize++;
+    // allocate fanins
+    Vec_WecForEachLevel( vFanouts, vArray, i )
+    {
+        k = vArray->nSize; vArray->nSize = 0;
+        Vec_IntGrow( vArray, k );
     }
-    assert( iOffset <= nSize );
-    assert( iFanOffset == Vec_IntSize(vEdges) );
-    iFanOffset = 0;
-    Sfm_ManForEachObj( p, pObj, i )
+    // add fanouts
+    Vec_WecForEachLevel( vFanins, vArray, i )
+        Vec_IntForEachEntry( vArray, Fanin, k )
+            Vec_IntPush( Vec_WecEntry( vFanouts, Fanin ), i );
+    // verify
+    Vec_WecForEachLevel( vFanins, vArray, i )
+        assert( Vec_IntSize(vArray) == Vec_IntCap(vArray) );
+    return vFanouts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Sfm_CreateLevel( Vec_Wec_t * vFanins )
+{
+    Vec_Int_t * vLevels;
+    Vec_Int_t * vArray;
+    int i, k, Fanin, * pLevels;
+    vLevels = Vec_IntStart( Vec_WecSize(vFanins) );
+    pLevels = Vec_IntArray( vLevels );
+    Vec_WecForEachLevel( vFanins, vArray, i )
+        Vec_IntForEachEntry( vArray, Fanin, k )
+            pLevels[i] = Abc_MaxInt( pLevels[i], pLevels[Fanin] + 1 );
+    return vLevels;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  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 )
     {
-        assert( Vec_IntEntry(vFanins, i)  == (int)pObj->nFanis );
-        assert( Vec_IntEntry(vFanouts, i) == (int)pObj->nFanos );
-        for ( k = 0; k < (int)pObj->nFanis; k++ )
-            assert( pObj->Fanio[k] == Vec_IntEntry(vEdges, iFanOffset++) );
+        Sfm_TruthToCnf( uTruth, Vec_IntSize(Vec_WecEntry(p->vFanins, 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);
     }
-    assert( iFanOffset == Vec_IntSize(vEdges) );
+    Vec_StrFree( vCnf );
+    return vCnfs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Wrd_t * vTruths )
+{
+    Sfm_Ntk_t * p;
+    Sfm_CheckConsistency( vFanins, nPis, nPos, vFixed );
+    p = ABC_CALLOC( Sfm_Ntk_t, 1 );
+    p->nObjs    = Vec_WecSize( vFanins );
+    p->nPis     = nPis;
+    p->nPos     = nPos;
+    p->nNodes   = p->nObjs - p->nPis - p->nPos;
+    p->vFanins  = vFanins;
+    // user data
+    p->vFixed   = vFixed;
+    p->vTruths  = vTruths;
+    // attributes
+    p->vFanouts = Sfm_CreateFanout( vFanins );
+    p->vLevels  = Sfm_CreateLevel( vFanins );
+    Vec_IntFill( &p->vTravIds, 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_NtkFree( Sfm_Ntk_t * p )
 {
-    ABC_FREE( p->pMem );
-    ABC_FREE( p->vObjs.pArray );
-    ABC_FREE( p->vPis.pArray );
-    ABC_FREE( p->vPos.pArray );
-    ABC_FREE( p->vMem.pArray );
-    ABC_FREE( p->vLevels.pArray );
+    // user data
+    Vec_WecFree( p->vFanins );
+    Vec_StrFree( p->vFixed );
+    Vec_WrdFree( p->vTruths );
+    // attributes
+    Vec_WecFree( p->vFanouts );
+    Vec_IntFree( p->vLevels );
     ABC_FREE( p->vTravIds.pArray );
-    ABC_FREE( p->vSatVars.pArray );
-    ABC_FREE( p->vTruths.pArray );
+    ABC_FREE( p->vId2Var.pArray );
+    ABC_FREE( p->vVar2Id.pArray );
+    Vec_WecFree( p->vCnfs );
+    Vec_IntFree( p->vCover );
+    // other data
+    Vec_IntFreeP( &p->vLeaves );
+    Vec_IntFreeP( &p->vRoots );
+    Vec_IntFreeP( &p->vNodes );
+    Vec_IntFreeP( &p->vTfo   );
+    Vec_IntFreeP( &p->vDivs  );
+    Vec_IntFreeP( &p->vLits  );
+    Vec_WecFreeP( &p->vClauses );
+    Vec_IntFreeP( &p->vFaninMap );
+    if ( p->pSat0 ) sat_solver_delete( p->pSat0 );
+    if ( p->pSat1 ) sat_solver_delete( p->pSat1 );
     ABC_FREE( p );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Public APIs of this network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 )
+{
+    return Vec_WrdEntry( p->vTruths, i );
+}
+int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i )
+{
+    return (int)Vec_StrEntry( p->vFixed, i );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c
index ed2a53c4..6431cd50 100644
--- a/src/opt/sfm/sfmSat.c
+++ b/src/opt/sfm/sfmSat.c
@@ -27,23 +27,76 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static word s_Truths6[6] = {
+    ABC_CONST(0xAAAAAAAAAAAAAAAA),
+    ABC_CONST(0xCCCCCCCCCCCCCCCC),
+    ABC_CONST(0xF0F0F0F0F0F0F0F0),
+    ABC_CONST(0xFF00FF00FF00FF00),
+    ABC_CONST(0xFFFF0000FFFF0000),
+    ABC_CONST(0xFFFFFFFF00000000)
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Takes SAT solver and returns interpolant.]
 
-  Description []
+  Description [If interpolant does not exist, returns diff SAT variables.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Sfm_CreateSatWindow( Sfm_Ntk_t * p )
+word Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_t * vDivs, Vec_Int_t * vLits, Vec_Int_t * vDiffs, int nBTLimit )
 {
+    word uTruth = 0, uCube;
+    int status, i, Div, iVar, nFinal, * pFinal;
+    int nVars = sat_solver_nvars(pSatOn);
+    int iNewLit = Abc_Var2Lit( nVars, 0 );
+    while ( 1 ) 
+    {
+        // find onset minterm
+        status = sat_solver_solve( pSatOn, &iNewLit, &iNewLit + 1, 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( vDivs, Div, i )
+            Vec_IntPush( vLits, Abc_LitNot(sat_solver_var_literal(pSatOn, Div)) );
+        // check against offset
+        status = sat_solver_solve( pSatOff, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
+        if ( status == l_Undef )
+            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;
+        }
+        assert( status == l_False );
+        // compute cube and add clause
+        nFinal = sat_solver_final( pSatOff, &pFinal );
+        uCube = ~(word)0;
+        Vec_IntClear( vLits );
+        Vec_IntPush( vLits, Abc_LitNot(iNewLit) );
+        for ( i = 0; i < nFinal; i++ )
+        {
+            Vec_IntPush( vLits, pFinal[i] );
+            iVar = Vec_IntFind( vDivs, Abc_Lit2Var(pFinal[i]) );   assert( iVar >= 0 );
+            uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
+        }
+        uTruth |= uCube;
+        sat_solver_addclause( pSatOn, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+    }
+    assert( 0 );
     return 0;
 }
 
diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c
new file mode 100644
index 00000000..2dd98806
--- /dev/null
+++ b/src/opt/sfm/sfmWin.c
@@ -0,0 +1,171 @@
+/**CFile****************************************************************
+
+  FileName    [sfmWin.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based optimization using internal don't-cares.]
+
+  Synopsis    [Structural window computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: sfmWin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sfmInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Working with traversal IDs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void  Sfm_NtkIncrementTravId( Sfm_Ntk_t * p )            { p->nTravIds++;                                           }       
+static inline void  Sfm_ObjSetTravIdCurrent( Sfm_Ntk_t * p, int Id )   { Vec_IntWriteEntry( &p->vTravIds, Id, p->nTravIds );      }
+static inline int   Sfm_ObjIsTravIdCurrent( Sfm_Ntk_t * p, int Id )    { return (Vec_IntEntry(&p->vTravIds, Id) == p->nTravIds);  }   
+
+/**Function*************************************************************
+
+  Synopsis    [Computes structural window.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sfm_NtkCollectTfi_rec( Sfm_Ntk_t * p, int iNode )
+{
+    int i, iFanin;
+    if ( Sfm_ObjIsTravIdCurrent( p, iNode ) )
+        return;
+    Sfm_ObjSetTravIdCurrent( p, iNode );
+    if ( Sfm_ObjIsPi( p, iNode ) )
+    {
+        Vec_IntPush( p->vLeaves, iNode );
+        return;
+    }
+    Sfm_NodeForEachFanin( p, iNode, iFanin, i )
+        Sfm_NtkCollectTfi_rec( p, iFanin );
+    Vec_IntPush( p->vNodes, iNode );
+}
+int Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode )
+{
+//    int i, iRoot;
+    assert( Sfm_ObjIsNode( p, iNode ) );
+    Sfm_NtkIncrementTravId( p );
+    Vec_IntClear( p->vLeaves ); // leaves 
+    Vec_IntClear( p->vNodes );  // internal
+    // collect transitive fanin
+    Sfm_NtkCollectTfi_rec( p, iNode );
+    // collect TFO
+    Vec_IntClear( p->vRoots );  // roots
+    Vec_IntClear( p->vTfo );    // roots
+    Vec_IntPush( p->vRoots, iNode );
+/*
+    Vec_IntForEachEntry( p->vRoots, iRoot, i )
+    {
+        assert( Sfm_ObjIsNode(p, iRoot) );
+        if ( Sfm_ObjIsTravIdCurrent(p, iRoot) )
+            continue;
+        if ( Sfm_ObjFanoutNum(p, iRoot) >= p->pPars->nFanoutMax )
+            continue;
+    }
+*/
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts a window into a SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sfm_NtkWin2Sat( Sfm_Ntk_t * p )
+{
+    Vec_Int_t * vClause;
+    int RetValue, Lit, iNode, iFanin, i, k;
+    sat_solver * pSat0 = sat_solver_new();
+    sat_solver * pSat1 = sat_solver_new();
+    sat_solver_setnvars( pSat0, 1 + Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) );
+    sat_solver_setnvars( pSat1, 1 + Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) );
+    // create SAT variables
+    p->nSatVars = 1;
+    Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
+        Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
+    Vec_IntForEachEntryReverse( p->vLeaves, iNode, i )
+        Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
+    // add CNF clauses
+    Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
+    {
+        // collect fanin variables
+        Vec_IntClear( p->vFaninMap );
+        Sfm_NodeForEachFanin( p, iNode, iFanin, k )
+            Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iFanin) );
+        Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iNode) );
+        // generate CNF 
+        Sfm_TranslateCnf( p->vClauses, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode), p->vFaninMap );
+        // add clauses
+        Vec_WecForEachLevel( p->vClauses, vClause, k )
+        {
+            if ( Vec_IntSize(vClause) == 0 )
+                break;
+            RetValue = sat_solver_addclause( pSat0, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
+            assert( RetValue );
+            RetValue = sat_solver_addclause( pSat1, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
+            assert( RetValue );
+        }
+    }
+    // add unit clause
+    Lit = Abc_Var2Lit( Sfm_ObjSatVar(p, iNode), 1 );
+    RetValue = sat_solver_addclause( pSat0, &Lit, &Lit + 1 );
+    assert( RetValue );
+    // add unit clause
+    Lit = Abc_Var2Lit( Sfm_ObjSatVar(p, iNode), 0 );
+    RetValue = sat_solver_addclause( pSat1, &Lit, &Lit + 1 );
+    assert( RetValue );
+    // finalize
+    sat_solver_compress( p->pSat0 );
+    sat_solver_compress( p->pSat1 );
+    // return the result
+    assert( p->pSat0 == NULL );
+    assert( p->pSat1 == NULL );
+    p->pSat0 = pSat0;
+    p->pSat1 = pSat1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+