25 files changed, 1347 insertions, 91 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 12151343..cd810b5e 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -471,6 +471,7 @@ extern Aig_Man_t *     Aig_ManStart( int nNodesMax );
 extern Aig_Man_t *     Aig_ManStartFrom( Aig_Man_t * p );
 extern Aig_Obj_t *     Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj );
 extern Aig_Man_t *     Aig_ManDup( Aig_Man_t * p, int fOrdered );
+extern Aig_Man_t *     Aig_ManDupWithoutPos( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
 extern void            Aig_ManStop( Aig_Man_t * p );
 extern int             Aig_ManCleanup( Aig_Man_t * p );
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 1979f4f9..57032703 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -217,6 +217,40 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    // duplicate internal nodes
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        assert( !Aig_ObjIsBuf(pObj) );
+        if ( Aig_ObjIsNode(pObj) )
+            pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    }
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Extracts the miter composed of XOR of the two nodes.]
 
   Description []
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c
index 7929b25d..a35e1169 100644
--- a/src/aig/fra/fraClaus.c
+++ b/src/aig/fra/fraClaus.c
@@ -1496,6 +1496,79 @@ void Fra_ClausPrintIndClauses( Clu_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Writes the clauses into an AIGER file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Fra_ClausGetLiteral( Clu_Man_t * p, int * pVar2Id, int Lit )
+{
+    Aig_Obj_t * pLiteral;
+    int NodeId = pVar2Id[ lit_var(Lit) ];
+    assert( NodeId >= 0 );
+    pLiteral = Aig_ManObj( p->pAig, NodeId )->pData;
+    return Aig_NotCond( pLiteral, lit_sign(Lit) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the clauses into an AIGER file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClausWriteIndClauses( Clu_Man_t * p )
+{
+    extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pClause, * pLiteral;
+    char Buffer[500];
+    int * pStart, * pVar2Id; 
+    int Beg, End, i, k;
+    // create mapping from SAT vars to node IDs
+    pVar2Id = ALLOC( int, p->pCnf->nVars );
+    memset( pVar2Id, 0xFF, sizeof(int) * p->pCnf->nVars );
+    for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
+        if ( p->pCnf->pVarNums[i] >= 0 )
+        {
+            assert( p->pCnf->pVarNums[i] < p->pCnf->nVars );
+            pVar2Id[ p->pCnf->pVarNums[i] ] = i;
+        }
+    // start the manager
+    pNew = Aig_ManDupWithoutPos( p->pAig );
+    // add the clauses
+    Beg = 0;
+    pStart = Vec_IntArray( p->vLitsProven );
+    Vec_IntForEachEntry( p->vClausesProven, End, i )
+    {
+        pClause = Fra_ClausGetLiteral( p, pVar2Id, pStart[Beg] );
+        for ( k = Beg + 1; k < End; k++ )
+        {
+            pLiteral = Fra_ClausGetLiteral( p, pVar2Id, pStart[k] );
+            pClause = Aig_Or( pNew, pClause, pLiteral );
+        }
+        Aig_ObjCreatePo( pNew, pClause );
+        Beg = End;
+    }
+    free( pVar2Id );
+    Aig_ManCleanup( pNew );
+    // write the manager into a file
+    sprintf( Buffer, "%s_care.aig", p->pAig->pName );
+    printf( "Care clauses are written into file \"%s\".\n", Buffer );
+    Ioa_WriteAiger( pNew, Buffer, 0, 1 );
+    Aig_ManStop( pNew );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Checks if the clause holds using the given simulation info.]
 
   Description []
@@ -1751,6 +1824,11 @@ clk = clock();
         Fra_ClausPrintIndClauses( p );
         Fra_ClausEstimateCoverage( p );
     }
+
+    if ( !p->fTarget )
+    {
+        Fra_ClausWriteIndClauses( p );
+    }
 /*
     // print the statistic into a file
     {
diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c
index 6783b459..4a3f9b03 100644
--- a/src/aig/fra/fraHot.c
+++ b/src/aig/fra/fraHot.c
@@ -395,25 +395,28 @@ Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots )
 {
     Aig_Man_t * pNew;
     Aig_Obj_t * pObj1, * pObj2, * pObj;
-    int i, Out1, Out2;
+    int i, Out1, Out2, nTruePis;
     pNew = Aig_ManStart( Vec_IntSize(vOneHots)/2 );
-    for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ )
+//    for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ )
+//        Aig_ObjCreatePi(pNew);
+    Aig_ManForEachPi( p->pManAig, pObj, i )
         Aig_ObjCreatePi(pNew);
+    nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
     for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
     {
         Out1 = Vec_IntEntry( vOneHots, i );
         Out2 = Vec_IntEntry( vOneHots, i+1 );
         if ( Out1 == 0 && Out2 == 0 )
             continue;
-        pObj1 = Aig_ManPi( pNew, Fra_LitReg(Out1) );
-        pObj2 = Aig_ManPi( pNew, Fra_LitReg(Out2) );
+        pObj1 = Aig_ManPi( pNew, nTruePis + Fra_LitReg(Out1) );
+        pObj2 = Aig_ManPi( pNew, nTruePis + Fra_LitReg(Out2) );
         pObj1 = Aig_NotCond( pObj1, Fra_LitSign(Out1) );
         pObj2 = Aig_NotCond( pObj2, Fra_LitSign(Out2) );
         pObj  = Aig_Or( pNew, pObj1, pObj2 );
         Aig_ObjCreatePo( pNew, pObj );
     }
     Aig_ManCleanup(pNew);
-    printf( "Created AIG with %d nodes and %d outputs.\n", Aig_ManNodeNum(pNew), Aig_ManPoNum(pNew) );
+//    printf( "Created AIG with %d nodes and %d outputs.\n", Aig_ManNodeNum(pNew), Aig_ManPoNum(pNew) );
     return pNew;
 }
 
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index f345b6d1..07044b52 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -470,8 +470,16 @@ clk2 = clock();
 clk2 = clock();
     if ( p->pPars->fWriteImps && p->vOneHots && Fra_OneHotCount(p, p->vOneHots) )
     {
+        extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
+        char Buffer[500];
+        Aig_Man_t * pNew;
         pManAigNew = Aig_ManDup( pManAig, 1 );
-        pManAigNew->pManExdc = Fra_OneHotCreateExdc( p, p->vOneHots );
+//        pManAigNew->pManExdc = Fra_OneHotCreateExdc( p, p->vOneHots );
+        pNew = Fra_OneHotCreateExdc( p, p->vOneHots );
+        sprintf( Buffer, "%s_care.aig", p->pManAig->pName );
+        printf( "Care one-hotness clauses are written into file \"%s\".\n", Buffer );
+        Ioa_WriteAiger( pNew, Buffer, 0, 1 );
+        Aig_ManStop( pNew );
     }
     else 
     {
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index e6f8b8f2..f09d7626 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -199,7 +199,7 @@ struct Abc_Ntk_t_
     int *             pModel;        // counter-example (for miters)
     void *            pSeqModel;     // counter-example (for sequential miters)
     Abc_Ntk_t *       pExdc;         // the EXDC network (if given)
-    void *            pManExdc;      // the EXDC network (if given)
+    void *            pExcare;       // the EXDC network (if given)
     void *            pData;         // misc
     Abc_Ntk_t *       pCopy;
     Hop_Man_t *       pHaig;         // history AIG
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index af23f18a..de517705 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -677,7 +677,7 @@ void Abc_NtkNodeSupport_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
     // mark the node as visited
     Abc_NodeSetTravIdCurrent( pNode );
     // collect the CI
-    if ( Abc_ObjIsCi(pNode) || Abc_ObjFaninNum(pNode) == 0 )
+    if ( Abc_ObjIsCi(pNode) )//|| Abc_ObjFaninNum(pNode) == 0 )
     {
         Vec_PtrPush( vNodes, pNode );
         return;
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 85cb1569..b1f75ab6 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -23,8 +23,6 @@
 #include "main.h"
 #include "mio.h"
 
-#include "aig.h"
-
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -348,8 +346,8 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
     // duplicate the EXDC Ntk
     if ( pNtk->pExdc )
         pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
-    if ( pNtk->pManExdc )
-        pNtkNew->pManExdc = Aig_ManDup( pNtk->pManExdc, 0 );
+    if ( pNtk->pExcare )
+        pNtkNew->pExcare = Abc_NtkDup( pNtk->pExcare );
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkDup(): Network check has failed.\n" );
     pNtk->pCopy = pNtkNew;
@@ -941,11 +939,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     // free EXDC Ntk
     if ( pNtk->pExdc )
         Abc_NtkDelete( pNtk->pExdc );
-    if ( pNtk->pManExdc )
-    {
-        Aig_ManStop( pNtk->pManExdc );
-        pNtk->pManExdc = NULL;
-    }
+    if ( pNtk->pExcare )
+        Abc_NtkDelete( pNtk->pExcare );
     // dereference the BDDs
     if ( Abc_NtkHasBdd(pNtk) )
     {
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 338f38fc..266f8075 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -101,6 +101,7 @@ static int Abc_CommandShortNames     ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandExdcFree       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExdcGet        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExdcSet        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCareSet        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCut            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandEspresso       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandGen            ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -280,6 +281,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "exdc_free",     Abc_CommandExdcFree,         1 );
     Cmd_CommandAdd( pAbc, "Various",      "exdc_get",      Abc_CommandExdcGet,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "exdc_set",      Abc_CommandExdcSet,          1 );
+    Cmd_CommandAdd( pAbc, "Various",      "care_set",      Abc_CommandCareSet,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "cut",           Abc_CommandCut,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "espresso",      Abc_CommandEspresso,         1 );
     Cmd_CommandAdd( pAbc, "Various",      "gen",           Abc_CommandGen,              0 );
@@ -3257,14 +3259,18 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    pPars->nWinTfoLevs  =  2;
-    pPars->nFanoutsMax  = 10;
-    pPars->nGrowthLevel =  0;
-    pPars->fArea        =  0;
-    pPars->fVerbose     =  0;
-    pPars->fVeryVerbose =  0;
+    pPars->nWinTfoLevs  =   2;
+    pPars->nFanoutsMax  =  10;
+    pPars->nDepthMax    =  20;
+    pPars->nDivMax      = 200;
+    pPars->nWinSizeMax  = 300;
+    pPars->nGrowthLevel =   0;
+    pPars->fResub       =   1;
+    pPars->fArea        =   0;
+    pPars->fVerbose     =   0;
+    pPars->fVeryVerbose =   0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WFLavwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLravwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -3276,7 +3282,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
             }
             pPars->nWinTfoLevs = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( pPars->nWinTfoLevs < 1 || pPars->nWinTfoLevs > 99 ) 
+            if ( pPars->nWinTfoLevs < 0 ) 
                 goto usage;
             break;
         case 'F':
@@ -3290,6 +3296,28 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nFanoutsMax < 1 ) 
                 goto usage;
             break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "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 )
+            {
+                fprintf( pErr, "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 'L':
             if ( globalUtilOptind >= argc )
             {
@@ -3301,6 +3329,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY ) 
                 goto usage;
             break;
+        case 'r':
+            pPars->fResub ^= 1;
+            break;
         case 'a':
             pPars->fArea ^= 1;
             break;
@@ -3337,14 +3368,17 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: mfs [-W <num>] [-F <num>] [-L <num>] [-vh]\n" );
+    fprintf( pErr, "usage: mfs [-WFDML <num>] [-arvh]\n" );
     fprintf( pErr, "\t           performs don't-care-based optimization of logic networks\n" );
-    fprintf( pErr, "\t-W <num> : the number of levels in the TFO cone (0 <= NM <= 100) [default = %d]\n", pPars->nWinTfoLevs );
-    fprintf( pErr, "\t-F <num> : the max number of fanouts to skip (1 <= n) [default = %d]\n", pPars->nFanoutsMax );
+    fprintf( pErr, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs );
+    fprintf( pErr, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax );
+    fprintf( pErr, "\t-D <num> : the max depth nodes to try (0 = no limit) [default = %d]\n", pPars->nDepthMax );
+    fprintf( pErr, "\t-M <num> : the max size of  window to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );
     fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
-//    fprintf( pErr, "\t-a       : toggle optimization for area only [default = %s]\n", pPars->fArea? "yes": "no" );
-    fprintf( pErr, "\t-v       : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
-//    fprintf( pErr, "\t-w       : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
+    fprintf( pErr, "\t-a       : toggle minimizing area or edges [default = %s]\n", pPars->fArea? "area": "edges" );
+    fprintf( pErr, "\t-r       : toggle resubstitution and dc-minimization [default = %s]\n", pPars->fResub? "resub": "dc-min" );
+    fprintf( pErr, "\t-v       : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-w       : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     fprintf( pErr, "\t-h       : print the command usage\n");
     return 1;
 } 
@@ -5750,6 +5784,93 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandCareSet( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr, * pFile;
+    Abc_Ntk_t * pNtk, * pNtkNew, * pNtkRes;
+    char * FileName;
+    int c;
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( argc != globalUtilOptind + 1 )
+    {
+        goto usage;
+    }
+
+    // get the input file name
+    FileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( FileName, "r" )) == NULL )
+    {
+        fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+            fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+        fprintf( pAbc->Err, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+
+    // set the new network
+    pNtkNew = Io_Read( FileName, Io_ReadFileType(FileName), 1 );
+    if ( pNtkNew == NULL )
+    {
+        fprintf( pAbc->Err, "Reading network from file has failed.\n" );
+        return 1;
+    }
+
+    // replace the EXDC
+    if ( pNtk->pExcare )
+    {
+        Abc_NtkDelete( pNtk->pExcare );
+        pNtk->pExcare = NULL;
+    }
+    pNtkRes = Abc_NtkDup( pNtk );
+    pNtkRes->pExcare = pNtkNew;
+
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: care_set [-h] <file>\n" );
+    fprintf( pErr, "\t         sets the network from file as a care for the current network\n" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    fprintf( pErr, "\t<file> : file with the new care network\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Cut_Params_t Params, * pParams = &Params;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 2a15c3a4..72606dcf 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -184,11 +184,6 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
             Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) );
             Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
         }
-    if ( pMan->pManExdc )
-    {
-        pNtkNew->pManExdc = pMan->pManExdc;
-        pMan->pManExdc = NULL;
-    }
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
     return pNtkNew;
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index bb56c22c..5d24398b 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -21,6 +21,7 @@
 #include "abc.h"
 #include "if.h"
 #include "kit.h"
+#include "aig.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -87,7 +88,6 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
     // duplicate EXDC
     if ( pNtk->pExdc )
         pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
-
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
deleted file mode 100644
index e69de29b..00000000
--- a/src/map/pcm/module.make
+++ /dev/null
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
deleted file mode 100644
index e69de29b..00000000
--- a/src/map/ply/module.make
+++ /dev/null
diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h
index a7ca3819..9fc6a253 100644
--- a/src/opt/mfs/mfs.h
+++ b/src/opt/mfs/mfs.h
@@ -43,7 +43,11 @@ struct Mfs_Par_t_
     // general parameters
     int           nWinTfoLevs;   // the maximum fanout levels
     int           nFanoutsMax;   // the maximum number of fanouts
-    int           nGrowthLevel;  // the maximum allowed growth in level after one iteration of resynthesis
+    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           fResub;        // performs resubstitution
     int           fArea;         // performs optimization for area
     int           fDelay;        // performs optimization for delay
     int           fVerbose;      // enable basic stats
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index fe0d84c3..332a6ad9 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -6,7 +6,7 @@
 
   PackageName [The good old minimization with complete don't-cares.]
 
-  Synopsis    []
+  Synopsis    [Core procedures of this package.]
 
   Author      [Alan Mishchenko]
   
@@ -39,9 +39,64 @@
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_NtkMfsResub( Mfs_Man_t * p, Abc_Obj_t * pNode )
+{
+    int clk;
+    p->nNodesTried++;
+    // prepare data structure for this node
+    Mfs_ManClean( p ); 
+    // compute window roots, window support, and window nodes
+clk = clock();
+    p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
+    p->vSupp  = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
+    p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
+p->timeWin += clock() - clk;
+    if ( p->pPars->nWinSizeMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinSizeMax )
+        return 1;
+    // compute the divisors of the window
+clk = clock();
+    p->vDivs  = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
+p->timeDiv += clock() - clk;
+    // construct AIG for the window
+clk = clock();
+    p->pAigWin = Abc_NtkConstructAig( p, pNode );
+p->timeAig += clock() - clk;
+    // translate it into CNF
+clk = clock();
+    p->pCnf = Cnf_DeriveSimple( p->pAigWin, 1 + Vec_PtrSize(p->vDivs) );
+p->timeCnf += clock() - clk;
+    // create the SAT problem
+clk = clock();
+    p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0 );
+    if ( p->pSat == NULL )
+    {
+        p->nNodesBad++;
+        return 1;
+    }
+    // solve the SAT problem
+    if ( p->pPars->fArea )
+        Abc_NtkMfsResubArea( p, pNode );
+    else
+        Abc_NtkMfsResubEdge( p, pNode );
+p->timeSat += clock() - clk;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
 {
     int clk;
+    p->nNodesTried++;
     // prepare data structure for this node
     Mfs_ManClean( p );
     // compute window roots, window support, and window nodes
@@ -80,9 +135,14 @@ p->timeSat += clock() - clk;
 ***********************************************************************/
 int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
 {
+    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters );
+
+    ProgressBar * pProgress;
     Mfs_Man_t * p;
     Abc_Obj_t * pObj;
-    int i, Counter;
+    int i, clk = clock();
+    int nTotalNodesBeg = Abc_NtkNodeNum(pNtk);
+    int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk);
 
     assert( Abc_NtkIsLogic(pNtk) );
     if ( Abc_NtkGetFaninMax(pNtk) > MFS_FANIN_MAX )
@@ -99,30 +159,57 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
         return 0;
     }
     assert( Abc_NtkHasAig(pNtk) );
-    if ( pNtk->pManExdc != NULL )
-        printf( "Performing don't-care computation with don't-cares.\n" );
 
     // start the manager
-    p = Mfs_ManAlloc();
-    p->pPars = pPars;
+    p = Mfs_ManAlloc( pPars );
     p->pNtk  = pNtk;
-    p->pCare = pNtk->pManExdc;
+    if ( pNtk->pExcare )
+    {
+        Abc_Ntk_t * pTemp;
+        pTemp = Abc_NtkStrash( pNtk->pExcare, 0, 0, 0 );
+        p->pCare = Abc_NtkToDar( pTemp, 0 );
+        Abc_NtkDelete( pTemp );
+    }
+    if ( pPars->fVerbose )
+    {
+        if ( p->pCare != NULL )
+            printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) );
+        else
+            printf( "Performing optimization without constraints.\n" );
+    }
+    if ( !pPars->fResub )
+        printf( "Currently don't-cares are not used but the stats are printed.\n" );
 
     // label the register outputs
     if ( p->pCare )
     {
-        Counter = 1;
         Abc_NtkForEachCi( pNtk, pObj, i )
-            if ( Abc_ObjFaninNum(pObj) == 0 )
-                pObj->pData = NULL;
-            else
-                pObj->pData = (void *)Counter++;
-        assert( Counter == Abc_NtkLatchNum(pNtk) + 1 );
+            pObj->pData = (void *)i;
     }
+ 
+    // compute levels
+    Abc_NtkLevel( pNtk );
+    Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
 
     // compute don't-cares for each node
+    p->nTotalNodesBeg = nTotalNodesBeg;
+    p->nTotalEdgesBeg = nTotalEdgesBeg;
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
     Abc_NtkForEachNode( pNtk, pObj, i )
-        Abc_NtkMfsNode( p, pObj );
+    {
+        if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
+            continue;
+        if ( !p->pPars->fVeryVerbose )
+            Extra_ProgressBarUpdate( pProgress, i, NULL );
+        if ( pPars->fResub )
+            Abc_NtkMfsResub( p, pObj );
+        else
+            Abc_NtkMfsNode( p, pObj );
+    }
+    Extra_ProgressBarStop( pProgress );
+    Abc_NtkStopReverseLevels( pNtk );
+    p->nTotalNodesEnd = Abc_NtkNodeNum(pNtk);
+    p->nTotalEdgesEnd = Abc_NtkGetTotalFanins(pNtk);
 
     // undo labesl
     if ( p->pCare )
@@ -132,6 +219,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
     }
 
     // free the manager
+    p->timeTotal = clock() - clk;
     Mfs_ManStop( p );
     return 1;
 }
diff --git a/src/opt/mfs/mfsDiv.c b/src/opt/mfs/mfsDiv.c
new file mode 100644
index 00000000..7b156b97
--- /dev/null
+++ b/src/opt/mfs/mfsDiv.c
@@ -0,0 +1,303 @@
+/**CFile****************************************************************
+
+  FileName    [mfsDiv.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    [Procedures to compute candidate divisors.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfsDiv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfsInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Marks and collects the TFI cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_MfsWinMarkTfi_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vCone )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    if ( Abc_NodeIsTravIdCurrent(pObj) )
+        return;
+    Abc_NodeSetTravIdCurrent( pObj );
+    if ( Abc_ObjIsCi(pObj) )
+    {
+        Vec_PtrPush( vCone, pObj );
+        return;
+    }
+    assert( Abc_ObjIsNode(pObj) );
+    // visit the fanins of the node
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        Abc_MfsWinMarkTfi_rec( pFanin, vCone );
+    Vec_PtrPush( vCone, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks and collects the TFI cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_MfsWinMarkTfi( Abc_Obj_t * pNode )
+{
+    Vec_Ptr_t * vCone;
+    vCone = Vec_PtrAlloc( 100 );
+    Abc_MfsWinMarkTfi_rec( pNode, vCone );
+    return vCone;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFO of the collected nodes up to the given level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_MfsWinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit )
+        return;
+    if ( Abc_NodeIsTravIdCurrent(pObj) )
+        return;
+    Abc_NodeSetTravIdCurrent( pObj );
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        Abc_MfsWinSweepLeafTfo_rec( pFanout, nLevelLimit );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Dereferences the node's MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_MfsNodeDeref_rec( Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin;
+    int i, Counter = 1;
+    if ( Abc_ObjIsCi(pNode) )
+        return 0;
+    Abc_NodeSetTravIdCurrent( pNode );
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+    {
+        assert( pFanin->vFanouts.nSize > 0 );
+        if ( --pFanin->vFanouts.nSize == 0 )
+            Counter += Abc_MfsNodeDeref_rec( pFanin );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [References the node's MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_MfsNodeRef_rec( Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin;
+    int i, Counter = 1;
+    if ( Abc_ObjIsCi(pNode) )
+        return 0;
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+    {
+        if ( pFanin->vFanouts.nSize++ == 0 )
+            Counter += Abc_MfsNodeRef_rec( pFanin );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Labels MFFC of the node with the current trav ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_MfsWinVisitMffc( Abc_Obj_t * pNode )
+{
+    int Count1, Count2;
+    assert( Abc_ObjIsNode(pNode) );
+    // dereference the node (mark with the current trav ID)
+    Count1 = Abc_MfsNodeDeref_rec( pNode );
+    // reference it back
+    Count2 = Abc_MfsNodeRef_rec( pNode );
+    assert( Count1 == Count2 );
+    return Count1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes divisors and add them to nodes in the window.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDivMax )
+{
+    Vec_Ptr_t * vCone, * vDivs;
+    Abc_Obj_t * pObj, * pFanout, * pFanin;
+    int k, f, m;
+    int nDivsPlus = 0, nTrueSupp;
+    assert( p->vDivs == NULL );
+
+    // mark the TFI with the current trav ID
+    Abc_NtkIncrementTravId( pNode->pNtk );
+    vCone = Abc_MfsWinMarkTfi( pNode );
+
+    // count the number of PIs
+    nTrueSupp = 0;
+    Vec_PtrForEachEntry( vCone, pObj, k )
+        nTrueSupp += Abc_ObjIsCi(pObj);
+//    printf( "%d(%d) ", Vec_PtrSize(p->vSupp), m );
+
+    // mark with the current trav ID those nodes that should not be divisors:
+    // (1) the node and its TFO
+    // (2) the MFFC of the node
+    // (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_ObjForEachFanin( pNode, pObj, k )
+        Abc_NodeSetTravIdCurrent( pObj );
+
+    // at this point the nodes are marked with two trav IDs:
+    // nodes to be collected as divisors are marked with previous trav ID
+    // nodes to be avoided as divisors are marked with current trav ID
+
+    // start collecting the divisors
+    vDivs = Vec_PtrAlloc( p->pPars->nDivMax );
+    Vec_PtrForEachEntry( vCone, pObj, k )
+    {
+        if ( !Abc_NodeIsTravIdPrevious(pObj) )
+            continue;
+        if ( (int)pObj->Level > nLevDivMax )
+            continue;
+        Vec_PtrPush( vDivs, pObj );
+        if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
+            break;
+    }
+    Vec_PtrFree( vCone );
+
+    // explore the fanouts of already collected divisors
+    if ( Vec_PtrSize(vDivs) < p->pPars->nDivMax )
+    Vec_PtrForEachEntry( vDivs, pObj, k )
+    {
+        // consider fanouts of this node
+        Abc_ObjForEachFanout( pObj, pFanout, f )
+        {
+            // stop if there are too many fanouts
+            if ( f > 20 )
+                break;
+            // skip nodes that are already added
+            if ( Abc_NodeIsTravIdPrevious(pFanout) )
+                continue;
+            // skip nodes in the TFO or in the MFFC of node
+            if ( Abc_NodeIsTravIdCurrent(pFanout) )
+                continue;
+            // skip COs
+            if ( !Abc_ObjIsNode(pFanout) ) 
+                continue;
+            // skip nodes with large level
+            if ( (int)pFanout->Level >= nLevDivMax )
+                continue;
+            // skip nodes whose fanins are not divisors
+            Abc_ObjForEachFanin( pFanout, pFanin, m )
+                if ( !Abc_NodeIsTravIdPrevious(pFanin) )
+                    break;
+            if ( m < Abc_ObjFaninNum(pFanout) )
+                continue;
+            // make sure this divisor in not among the nodes
+//            Vec_PtrForEachEntry( p->vNodes, pFanin, m )
+//                assert( pFanout != pFanin );
+            // add the node to the divisors
+            Vec_PtrPush( vDivs, pFanout );
+//            Vec_PtrPush( p->vNodes, pFanout );
+            Vec_PtrPushUnique( p->vNodes, pFanout );
+            Abc_NodeSetTravIdPrevious( pFanout );
+            nDivsPlus++;
+            if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
+                break;
+        }
+        if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
+            break;
+    }
+
+    // sort the divisors by level in the increasing order
+    Vec_PtrSort( vDivs, Abc_NodeCompareLevelsIncrease );
+
+    // add the fanins of the node
+    Abc_ObjForEachFanin( pNode, pFanin, k )
+        Vec_PtrPush( vDivs, pFanin );
+
+/*
+    printf( "Node level = %d.  ", Abc_ObjLevel(p->pNode) );
+    Vec_PtrForEachEntryStart( vDivs, pObj, k, Vec_PtrSize(vDivs)-p->nDivsPlus )
+        printf( "%d ", Abc_ObjLevel(pObj) );
+    printf( "\n" );
+*/
+//printf( "%d ", p->nDivsPlus );
+//    printf( "(%d+%d)(%d+%d+%d) ", Vec_PtrSize(p->vSupp), Vec_PtrSize(p->vNodes), 
+//        nTrueSupp, Vec_PtrSize(vDivs)-nTrueSupp-nDivsPlus, nDivsPlus );
+    return vDivs;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index 6ba5903e..54826bc1 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -34,6 +34,7 @@ extern "C" {
 #include "aig.h"
 #include "cnf.h"
 #include "satSolver.h"
+#include "satStore.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -52,11 +53,23 @@ struct Mfs_Man_t_
     Vec_Ptr_t *         vRoots;    // the roots of the window
     Vec_Ptr_t *         vSupp;     // the support of the window
     Vec_Ptr_t *         vNodes;    // the internal nodes of the window
+    Vec_Ptr_t *         vDivs;     // the divisors of the node
+    Vec_Int_t *         vDivLits;  // the SAT literals of divisor nodes
     Vec_Int_t *         vProjVars; // the projection variables
+    // intermediate simulation data
+    Vec_Ptr_t *         vDivCexes; // the counter-example for dividors
+    int                 nDivWords; // the number of words
+    int                 nCexes;    // the numbe rof current counter-examples
+    int                 nSatCalls; 
+    int                 nSatCexes;
     // solving data
     Aig_Man_t *         pAigWin;   // window AIG with constraints
     Cnf_Dat_t *         pCnf;      // the CNF for the window
     sat_solver *        pSat;      // the SAT solver used 
+    Int_Man_t *         pMan;      // interpolation manager;
+    Vec_Int_t *         vMem;      // memory for intermediate SOPs
+    Vec_Vec_t *         vLevels;   // levelized structure for updating
+    Vec_Ptr_t *         vFanins;   // the new set of fanins
     // the result of solving
     int                 nFanins;   // the number of fanins
     int                 nWords;    // the number of words
@@ -64,14 +77,24 @@ struct Mfs_Man_t_
     unsigned            uCare[(MFS_FANIN_MAX<=5)?1:1<<(MFS_FANIN_MAX-5)];  // the computed care-set
     // performance statistics
     int                 nNodesTried;
-    int                 nNodesBad;
+    int                 nNodesResub;
+    int                 nNodesGained;
     int                 nMintsCare;
     int                 nMintsTotal;
+    int                 nNodesBad;
+    // node/edge stats
+    int                 nTotalNodesBeg;
+    int                 nTotalNodesEnd;
+    int                 nTotalEdgesBeg;
+    int                 nTotalEdgesEnd;
     // statistics
     int                 timeWin;
+    int                 timeDiv;
     int                 timeAig;
     int                 timeCnf;
     int                 timeSat;
+    int                 timeInt;
+    int                 timeTotal;
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -86,10 +109,18 @@ struct Mfs_Man_t_
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== mfsDiv.c ==========================================================*/
+extern Vec_Ptr_t *      Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDivMax );
+/*=== mfsInter.c ==========================================================*/
+extern sat_solver *     Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands );
+extern Hop_Obj_t *      Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands );
 /*=== mfsMan.c ==========================================================*/
-extern Mfs_Man_t *      Mfs_ManAlloc();
+extern Mfs_Man_t *      Mfs_ManAlloc( Mfs_Par_t * pPars );
 extern void             Mfs_ManStop( Mfs_Man_t * p );
 extern void             Mfs_ManClean( Mfs_Man_t * p );
+/*=== mfsResub.c ==========================================================*/
+extern int              Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode );
+extern int              Abc_NtkMfsResubEdge( Mfs_Man_t * p, Abc_Obj_t * pNode );
 /*=== mfsSat.c ==========================================================*/
 extern void             Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode );
 /*=== mfsStrash.c ==========================================================*/
diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c
new file mode 100644
index 00000000..16db5061
--- /dev/null
+++ b/src/opt/mfs/mfsInter.c
@@ -0,0 +1,254 @@
+/**CFile****************************************************************
+
+  FileName    [mfsInter.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    [Procedures for computing resub function by interpolation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfsInter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfsInt.h"
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Adds constraints for the two-input AND-gate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_MfsSatAddXor( sat_solver * pSat, int iVarA, int iVarB, int iVarC )
+{
+    lit Lits[3];
+
+    Lits[0] = toLitCond( iVarA, 1 );
+    Lits[1] = toLitCond( iVarB, 1 );
+    Lits[2] = toLitCond( iVarC, 1 );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
+        return 0;
+
+    Lits[0] = toLitCond( iVarA, 1 );
+    Lits[1] = toLitCond( iVarB, 0 );
+    Lits[2] = toLitCond( iVarC, 0 );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
+        return 0;
+
+    Lits[0] = toLitCond( iVarA, 0 );
+    Lits[1] = toLitCond( iVarB, 1 );
+    Lits[2] = toLitCond( iVarC, 0 );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
+        return 0;
+
+    Lits[0] = toLitCond( iVarA, 0 );
+    Lits[1] = toLitCond( iVarB, 0 );
+    Lits[2] = toLitCond( iVarC, 1 );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
+        return 0;
+
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates miter for checking resubsitution.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands )
+{
+    sat_solver * pSat;
+    Aig_Obj_t * pObjPo;
+    int Lits[2], status, iVar, i, c;
+
+    // get the literal for the output of F
+    pObjPo = Aig_ManPo( p->pAigWin, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) - 1 );
+    Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], 0 );
+
+    // collect the outputs of the divisors
+    Vec_IntClear( p->vProjVars );
+    Vec_PtrForEachEntryStart( p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) )
+    {
+        assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
+        Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] );
+    }
+    assert( Vec_IntSize(p->vProjVars) == Vec_PtrSize(p->vDivs) );
+
+    // start the solver
+    pSat = sat_solver_new();
+    sat_solver_setnvars( pSat, 2 * p->pCnf->nVars + Vec_PtrSize(p->vDivs) );
+    if ( pCands )
+        sat_solver_store_alloc( pSat );
+
+    // load the first copy of the clauses
+    for ( i = 0; i < p->pCnf->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, p->pCnf->pClauses[i], p->pCnf->pClauses[i+1] ) )
+        {
+            sat_solver_delete( pSat );
+            return NULL;
+        }
+    }
+    // add the clause for the first output of F
+    if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
+    {
+        sat_solver_delete( pSat );
+        return NULL;
+    }
+
+    // bookmark the clauses of A
+    if ( pCands )
+        sat_solver_store_mark_clauses_a( pSat );
+
+    // transform the literals
+    for ( i = 0; i < p->pCnf->nLiterals; i++ )
+        p->pCnf->pClauses[0][i] += 2 * p->pCnf->nVars;
+    // load the second copy of the clauses
+    for ( i = 0; i < p->pCnf->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, p->pCnf->pClauses[i], p->pCnf->pClauses[i+1] ) )
+        {
+            sat_solver_delete( pSat );
+            return NULL;
+        }
+    }
+    // transform the literals
+    for ( i = 0; i < p->pCnf->nLiterals; i++ )
+        p->pCnf->pClauses[0][i] -= 2 * p->pCnf->nVars;
+    // add the clause for the second output of F
+    Lits[0] = 2 * p->pCnf->nVars + lit_neg( Lits[0] );
+    if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
+    {
+        sat_solver_delete( pSat );
+        return NULL;
+    }
+
+    if ( pCands )
+    {
+        // add relevant clauses for EXOR gates
+        for ( c = 0; c < nCands; c++ )
+        {
+            // get the variable number of this divisor
+            i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
+            // get the corresponding SAT variable
+            iVar = Vec_IntEntry( p->vProjVars, i );
+            // add the corresponding EXOR gate
+            if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
+            {
+                sat_solver_delete( pSat );
+                return NULL;
+            }
+            // add the corresponding clause
+            if ( !sat_solver_addclause( pSat, pCands + c, pCands + c + 1 ) )
+            {
+                sat_solver_delete( pSat );
+                return NULL;
+            }
+        }
+        // bookmark the roots
+        sat_solver_store_mark_roots( pSat );
+    }
+    else
+    {
+        // add the clauses for the EXOR gates - and remember their outputs
+        Vec_IntForEachEntry( p->vProjVars, iVar, i )
+        {
+            if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
+            {
+                sat_solver_delete( pSat );
+                return NULL;
+            }
+            Vec_IntWriteEntry( p->vProjVars, i, 2 * p->pCnf->nVars + i );
+        }
+        // simplify the solver
+        status = sat_solver_simplify(pSat);
+        if ( status == 0 )
+        {
+//            printf( "Abc_MfsCreateSolverResub(): SAT solver construction has failed. Skipping node.\n" );
+            sat_solver_delete( pSat );
+            return NULL;
+        }
+    }
+    return pSat;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs interpolation.]
+
+  Description [Derives the new function of the node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
+{
+    extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
+
+    sat_solver * pSat;
+    Sto_Man_t * pCnf = NULL;
+    unsigned * puTruth;
+    Kit_Graph_t * pGraph;
+    Hop_Obj_t * pFunc;
+    int nFanins, status;
+
+    // derive the SAT solver for interpolation
+    pSat = Abc_MfsCreateSolverResub( p, pCands, nCands );
+
+    // solve the problem
+    status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+    if ( status != l_False )
+    {
+        printf( "Abc_NtkMfsInterplate(): Internal error. The problem is not UNSAT.\n" );
+        return NULL;
+    }
+    // get the learned clauses
+    pCnf = sat_solver_store_release( pSat );
+    sat_solver_delete( pSat );
+
+    // derive the interpolant
+    nFanins = Int_ManInterpolate( p->pMan, pCnf, 0, &puTruth );
+    Sto_ManFree( pCnf );
+    assert( nFanins == nCands );
+
+    // transform interpolant into AIG
+    pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem );
+    pFunc = Kit_GraphToHop( p->pNtk->pManFunc, pGraph );
+    Kit_GraphFree( pGraph );
+    return pFunc;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index 1341e373..67981d5a 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -6,7 +6,7 @@
 
   PackageName [The good old minimization with complete don't-cares.]
 
-  Synopsis    [Procedure to manipulation the manager.]
+  Synopsis    [Procedures working with the manager.]
 
   Author      [Alan Mishchenko]
   
@@ -28,7 +28,6 @@
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-
 /**Function*************************************************************
 
   Synopsis    []
@@ -40,13 +39,21 @@
   SeeAlso     []
 
 ***********************************************************************/
-Mfs_Man_t * Mfs_ManAlloc()
+Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars )
 {
     Mfs_Man_t * p;
     // start the manager
     p = ALLOC( Mfs_Man_t, 1 );
     memset( p, 0, sizeof(Mfs_Man_t) );
+    p->pPars     = pPars;
     p->vProjVars = Vec_IntAlloc( 100 );
+    p->vDivLits  = Vec_IntAlloc( 100 );
+    p->nDivWords = Aig_BitWordNum(p->pPars->nDivMax + MFS_FANIN_MAX);
+    p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFS_FANIN_MAX+1, p->nDivWords );
+    p->pMan      = Int_ManAlloc();
+    p->vMem      = Vec_IntAlloc( 0 );
+    p->vLevels   = Vec_VecStart( 32 );
+    p->vFanins   = Vec_PtrAlloc( 32 );
     return p;
 }
 
@@ -75,12 +82,15 @@ void Mfs_ManClean( Mfs_Man_t * p )
         Vec_PtrFree( p->vSupp );
     if ( p->vNodes )
         Vec_PtrFree( p->vNodes );
+    if ( p->vDivs )
+        Vec_PtrFree( p->vDivs );
     p->pAigWin = NULL;
-    p->pCnf = NULL;
-    p->pSat = NULL;
+    p->pCnf   = NULL;
+    p->pSat   = NULL;
     p->vRoots = NULL;
-    p->vSupp = NULL;
+    p->vSupp  = NULL;
     p->vNodes = NULL;
+    p->vDivs  = NULL;
 }
 
 /**Function*************************************************************
@@ -96,14 +106,31 @@ void Mfs_ManClean( Mfs_Man_t * p )
 ***********************************************************************/
 void Mfs_ManPrint( Mfs_Man_t * p )
 {
-    printf( "Nodes tried = %d. Bad nodes = %d.\n", 
-        p->nNodesTried, p->nNodesBad );
-    printf( "Total mints = %d. Care mints = %d. Ratio = %5.2f.\n", 
-        p->nMintsTotal, p->nMintsCare, 1.0 * p->nMintsCare / p->nMintsTotal );
-    PRT( "Win", p->timeWin );
-    PRT( "Aig", p->timeAig );
-    PRT( "Cnf", p->timeCnf );
-    PRT( "Sat", p->timeSat );
+    if ( p->pPars->fResub )
+    {
+        printf( "Reduction in nodes = %5d. (%.2f %%) ", 
+            p->nTotalNodesBeg-p->nTotalNodesEnd, 
+            100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/p->nTotalNodesBeg );
+        printf( "Reduction in edges = %5d. (%.2f %%) ", 
+            p->nTotalEdgesBeg-p->nTotalEdgesEnd, 
+            100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg );
+        printf( "\n" );
+        printf( "Nodes = %d. Tried = %d. Resub = %d. Skipped = %d. SAT calls = %d.\n", 
+            Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nNodesBad, p->nSatCalls );
+    }
+    else
+    {
+        printf( "Nodes = %d.  Care mints = %d. Total mints = %d. Ratio = %5.2f.\n", 
+            p->nNodesTried, p->nMintsCare, p->nMintsTotal, 1.0 * p->nMintsCare / p->nMintsTotal );
+    }
+    PRTP( "Win", p->timeWin            ,  p->timeTotal );
+    PRTP( "Div", p->timeDiv            ,  p->timeTotal );
+    PRTP( "Aig", p->timeAig            ,  p->timeTotal );
+    PRTP( "Cnf", p->timeCnf            ,  p->timeTotal );
+    PRTP( "Sat", p->timeSat-p->timeInt ,  p->timeTotal );
+    PRTP( "Int", p->timeInt            ,  p->timeTotal );
+    PRTP( "ALL", p->timeTotal          ,  p->timeTotal );
+
 }
 
 /**Function*************************************************************
@@ -119,9 +146,18 @@ void Mfs_ManPrint( Mfs_Man_t * p )
 ***********************************************************************/
 void Mfs_ManStop( Mfs_Man_t * p )
 {
-    Mfs_ManPrint( p );
+    if ( p->pPars->fVerbose )
+        Mfs_ManPrint( p );
+    if ( p->pCare )
+        Aig_ManStop( p->pCare );
     Mfs_ManClean( p );
+    Int_ManFree( p->pMan );
+    Vec_IntFree( p->vMem );
+    Vec_VecFree( p->vLevels );
+    Vec_PtrFree( p->vFanins );
     Vec_IntFree( p->vProjVars );
+    Vec_IntFree( p->vDivLits );
+    Vec_PtrFree( p->vDivCexes );
     free( p );
 }
 
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
new file mode 100644
index 00000000..ae1132f2
--- /dev/null
+++ b/src/opt/mfs/mfsResub.c
@@ -0,0 +1,276 @@
+/**CFile****************************************************************
+
+  FileName    [mfsResub.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    [Procedures to perform resubstitution.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfsResub.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfsInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the network after resubstitution.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc )
+{
+    Abc_Obj_t * pObjNew, * pFanin;
+    int k;
+    // create the new node
+    pObjNew = Abc_NtkCreateNode( pObj->pNtk );
+    pObjNew->pData = pFunc;
+    Vec_PtrForEachEntry( vFanins, pFanin, k )
+        Abc_ObjAddFanin( pObjNew, pFanin );
+    // replace the old node by the new node
+//printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj );
+//printf( "Inserting node " ); Abc_ObjPrint( stdout, pObjNew );
+    // update the level of the node
+    Abc_NtkUpdate( pObj, pObjNew, p->vLevels );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Tries resubstitution.]
+
+  Description [Returns 1 if it is feasible, or 0 if c-ex is found.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
+{
+    unsigned * pData, * pDataTot;
+    int RetValue, iVar, i;
+    p->nSatCalls++;
+    RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+    assert( RetValue == l_False || RetValue == l_True );
+    if ( RetValue == l_False )
+        return 1;
+    p->nSatCexes++;
+    // store the counter-example
+    pData = Vec_PtrEntry( p->vDivCexes, p->nCexes++ );
+    assert( pData[0] == 0 );
+    Vec_IntForEachEntry( p->vProjVars, iVar, i )
+    {
+        if ( sat_solver_var_value( p->pSat, iVar ) )
+            Aig_InfoSetBit( pData, i );
+    }
+    // AND the result with the previous ones
+    pDataTot = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
+    for ( i = 0; i < p->nDivWords; i++ )
+        pDataTot[i] &= pData[i];
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs resubstitution for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove )
+{
+    int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
+    unsigned * pData;
+    int pCands[MFS_FANIN_MAX];
+    int iVar, i, nCands, clk;
+    Abc_Obj_t * pFanin;
+    Hop_Obj_t * pFunc;
+    assert( iFanin >= 0 );
+
+    // clean simulation info
+    Vec_PtrCleanSimInfo( p->vDivCexes, 0, p->nDivWords ); 
+    pData = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
+    memset( pData, 0xFF, sizeof(unsigned) * p->nDivWords );
+    p->nCexes = 0;
+
+    if ( 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), 
+            Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 );
+    }
+
+    // try fanins without the critical fanin
+    nCands = 0;
+    Vec_PtrClear( p->vFanins );
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+    {
+        if ( i == iFanin )
+            continue;
+        Vec_PtrPush( p->vFanins, pFanin );
+        iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
+        pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
+    }
+    if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands ) )
+    {
+        if ( fVeryVerbose )
+        printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin );
+        p->nNodesResub++;
+//        p->nNodesGained += Abc_NodeMffcLabel(pNode);
+clk = clock();
+        // derive the function
+        pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
+        // update the network
+        Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
+p->timeInt += clock() - clk;
+        return 1;
+    }
+
+    if ( fOnlyRemove )
+        return 0;
+
+    // shift variables by 1
+    for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- )
+        p->vFanins->pArray[i] = p->vFanins->pArray[i-1];
+    p->vFanins->nSize++;
+
+    if ( fVeryVerbose )
+    {
+        for ( i = 0; i < 8; i++ )
+            printf( " " );
+        for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ )
+            printf( "%d", i % 10 );
+        for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
+            if ( i == iFanin )
+                printf( "*" );
+            else
+                printf( "%c", 'a' + i );
+        printf( "\n" );
+    }
+    iVar = -1;
+    while ( 1 )
+    {
+        if ( fVeryVerbose )
+        {
+            printf( "%3d: %2d ", p->nCexes, iVar );
+            pData = Vec_PtrEntry( p->vDivCexes, p->nCexes-1 );
+//            Extra_PrintBinary( stdout, pData, Vec_PtrSize(p->vDivs) );
+            for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
+                printf( "%d", Aig_InfoHasBit(pData, i) );
+            printf( "\n" );
+        }
+
+        // find the next divisor to try
+        pData = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
+        for ( iVar = 0; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
+            if ( Aig_InfoHasBit( pData, iVar ) )
+                break;
+        if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
+            return 0;
+        pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
+        if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 ) )
+        {
+            if ( fVeryVerbose )
+            printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar );
+            p->nNodesResub++;
+//            p->nNodesGained += Abc_NodeMffcLabel(pNode);
+clk = clock();
+            // derive the function
+            pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 );
+            // update the network
+//            Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) );
+            Vec_PtrWriteEntry( p->vFanins, 0, Vec_PtrEntry(p->vDivs, iVar) );
+            Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
+p->timeInt += clock() - clk;
+            return 1;
+        }
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs resubstitution for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
+        {
+            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0 ) )
+                return 1;
+        }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs resubstitution for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMfsResubEdge( Mfs_Man_t * p, Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
+        {
+            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0 ) )
+                return 1;
+        }
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) != 1 )
+        {
+            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1 ) )
+                return 1;
+        }
+    return 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c
index d995000f..efb09b39 100644
--- a/src/opt/mfs/mfsSat.c
+++ b/src/opt/mfs/mfsSat.c
@@ -6,7 +6,7 @@
 
   PackageName [The good old minimization with complete don't-cares.]
 
-  Synopsis    []
+  Synopsis    [Procedures to compute don't-cares using SAT.]
 
   Author      [Alan Mishchenko]
   
@@ -43,9 +43,11 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p )
 {
     int Lits[MFS_FANIN_MAX];
     int RetValue, iVar, b, Mint;
-    RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
-    if ( RetValue != l_True )
+    RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+    assert( RetValue == l_False || RetValue == l_True );
+    if ( RetValue == l_False )
         return 0;
+    p->nCares++;
     // add SAT assignment to the solver
     Mint = 0;
     Vec_IntForEachEntry( p->vProjVars, iVar, b )
@@ -95,15 +97,19 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
     memset( p->uCare, 0, sizeof(unsigned) * p->nWords );
 
     // iterate through the SAT assignments
-    while ( Abc_NtkMfsSolveSat_iter( p ) );
-
-    // write statistics
     p->nCares = 0;
-    for ( i = 0; i < p->nWords; i++ )
-        p->nCares += Aig_WordCountOnes( p->uCare[i] );
+    while ( Abc_NtkMfsSolveSat_iter(p) );
 
+    // write statistics
     p->nMintsCare  += p->nCares;
-    p->nMintsTotal += 32 * p->nWords;
+    p->nMintsTotal += (1<<p->nFanins);
+
+    if ( p->pPars->fVeryVerbose )
+    {
+        printf( "Node %4d : Care = %2d. Total = %2d.  ", pNode->Id, p->nCares, (1<<p->nFanins) );
+        Extra_PrintBinary( stdout, p->uCare, (1<<p->nFanins) );
+        printf( "\n" );
+    }
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/mfs/mfsStrash.c b/src/opt/mfs/mfsStrash.c
index 7b467936..8e945045 100644
--- a/src/opt/mfs/mfsStrash.c
+++ b/src/opt/mfs/mfsStrash.c
@@ -144,18 +144,18 @@ Aig_Obj_t * Abc_NtkConstructAig_rec( Mfs_Man_t * p, Abc_Obj_t * pNode, Aig_Man_t
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Obj_t * Abc_NtkConstructCare_rec( Mfs_Man_t * p, Aig_Obj_t * pObj, Aig_Man_t * pMan )
+Aig_Obj_t * Abc_NtkConstructCare_rec( Aig_Man_t * pCare, Aig_Obj_t * pObj, Aig_Man_t * pMan )
 {
     Aig_Obj_t * pObj0, * pObj1;
-    if ( Aig_ObjIsTravIdCurrent( pMan, pObj ) )
+    if ( Aig_ObjIsTravIdCurrent( pCare, pObj ) )
         return pObj->pData;
-    Aig_ObjSetTravIdCurrent( pMan, pObj );
+    Aig_ObjSetTravIdCurrent( pCare, pObj );
     if ( Aig_ObjIsPi(pObj) )
         return pObj->pData = NULL;
-    pObj0 = Abc_NtkConstructCare_rec( p, Aig_ObjFanin0(pObj), pMan );
+    pObj0 = Abc_NtkConstructCare_rec( pCare, Aig_ObjFanin0(pObj), pMan );
     if ( pObj0 == NULL )
         return pObj->pData = NULL;
-    pObj1 = Abc_NtkConstructCare_rec( p, Aig_ObjFanin1(pObj), pMan );
+    pObj1 = Abc_NtkConstructCare_rec( pCare, Aig_ObjFanin1(pObj), pMan );
     if ( pObj1 == NULL )
         return pObj->pData = NULL;
     pObj0 = Aig_NotCond( pObj0, Aig_ObjFaninC0(pObj) );
@@ -184,6 +184,7 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode )
     pMan = Aig_ManStart( 1000 );
     // construct the root node's AIG cone
     pObjAig = Abc_NtkConstructAig_rec( p, pNode, pMan );
+//    assert( Aig_ManConst1(pMan) == pObjAig );
     Aig_ObjCreatePo( pMan, pObjAig );
     if ( p->pCare )
     {
@@ -191,27 +192,43 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode )
         Aig_ManIncrementTravId( p->pCare );
         Vec_PtrForEachEntry( p->vSupp, pFanin, i )
         {
-            if ( pFanin->pData == NULL )
-                continue;
-            pPi = Aig_ManPi( p->pCare, ((int)pFanin->pData) - 1 );
+            pPi = Aig_ManPi( p->pCare, (int)pFanin->pData );
             Aig_ObjSetTravIdCurrent( p->pCare, pPi );
             pPi->pData = pFanin->pCopy;
         }
         // construct the constraints
         Aig_ManForEachPo( p->pCare, pPo, i )
         {
-            pObjAig = Abc_NtkConstructCare_rec( p, Aig_ObjFanin0(pPo), pMan );
+//            assert( Aig_ObjFanin0(pPo) != Aig_ManConst1(p->pCare) );
+            if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) )
+                continue;
+            pObjAig = Abc_NtkConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan );
             if ( pObjAig == NULL )
                 continue;
             pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
             Aig_ObjCreatePo( pMan, pObjAig );
         }
     }
-    // construct the fanins
-    Abc_ObjForEachFanin( pNode, pFanin, i )
+    if ( p->pPars->fResub )
     {
-        pObjAig = (Aig_Obj_t *)pFanin->pCopy;
+        // construct the node
+        pObjAig = (Aig_Obj_t *)pNode->pCopy;
         Aig_ObjCreatePo( pMan, pObjAig );
+        // construct the divisors
+        Vec_PtrForEachEntry( p->vDivs, pFanin, i )
+        {
+            pObjAig = (Aig_Obj_t *)pFanin->pCopy;
+            Aig_ObjCreatePo( pMan, pObjAig );
+        }
+    }
+    else
+    {
+        // construct the fanins
+        Abc_ObjForEachFanin( pNode, pFanin, i )
+        {
+            pObjAig = (Aig_Obj_t *)pFanin->pCopy;
+            Aig_ObjCreatePo( pMan, pObjAig );
+        }
     }
     Aig_ManCleanup( pMan );
     return pMan;
diff --git a/src/opt/mfs/mfsWin.c b/src/opt/mfs/mfsWin.c
index b812d44d..e3e5e24e 100644
--- a/src/opt/mfs/mfsWin.c
+++ b/src/opt/mfs/mfsWin.c
@@ -6,7 +6,7 @@
 
   PackageName [The good old minimization with complete don't-cares.]
 
-  Synopsis    []
+  Synopsis    [Procedures to compute windows stretching to the PIs.]
 
   Author      [Alan Mishchenko]
   
diff --git a/src/opt/mfs/module.make b/src/opt/mfs/module.make
index 7b9f1260..544accec 100644
--- a/src/opt/mfs/module.make
+++ b/src/opt/mfs/module.make
@@ -1,5 +1,8 @@
 SRC +=  src/opt/mfs/mfsCore.c \
+    src/opt/mfs/mfsDiv.c \
+    src/opt/mfs/mfsInter.c \
     src/opt/mfs/mfsMan.c \
+    src/opt/mfs/mfsResub.c \
     src/opt/mfs/mfsSat.c \
     src/opt/mfs/mfsStrash.c \
     src/opt/mfs/mfsWin.c
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index cb448fc0..a19a1573 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -183,12 +183,15 @@ void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc
 {
     Abc_Obj_t * pObjNew, * pFanin;
     int k;
+
     // create the new node
     pObjNew = Abc_NtkCreateNode( pObj->pNtk );
     pObjNew->pData = pFunc;
     Vec_PtrForEachEntry( vFanins, pFanin, k )
         Abc_ObjAddFanin( pObjNew, pFanin );
     // replace the old node by the new node
+//printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj );
+//printf( "Inserting node " ); Abc_ObjPrint( stdout, pObjNew );
     // update the level of the node
     Abc_NtkUpdate( pObj, pObjNew, vLevels );
 }