Experiments with precomputation and matching.

8 files changed, 625 insertions, 81 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 18239440..cbfb7b31 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -5160,7 +5160,7 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Sfm_ParSetDefault3( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "OIFXMLCNdavwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "OIFXMLCNdaovwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -5258,6 +5258,9 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'a':
             pPars->fArea ^= 1;
             break;
+        case 'o':
+            pPars->fRrOnly ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -5285,7 +5288,7 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: mfs3 [-OIFXMLCN <num>] [-avwh]\n" );
+    Abc_Print( -2, "usage: mfs3 [-OIFXMLCN <num>] [-aovwh]\n" );
     Abc_Print( -2, "\t           performs don't-care-based optimization of mapped networks\n" );
     Abc_Print( -2, "\t-O <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n",             pPars->nTfoLevMax );
     Abc_Print( -2, "\t-I <num> : the number of levels in the TFI cone (1 <= num) [default = %d]\n",             pPars->nTfiLevMax );
@@ -5296,6 +5299,7 @@ usage:
     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-N <num> : the max number of nodes to try (0 = all) [default = %d]\n",                    pPars->nNodesMax );
     Abc_Print( -2, "\t-a       : toggle minimizing area or area+edges [default = %s]\n",                        pPars->fArea? "area": "area+edges" );
+    Abc_Print( -2, "\t-o       : toggle using old implementation for comparison [default = %s]\n",              pPars->fRrOnly? "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");
diff --git a/src/map/mio/mio.c b/src/map/mio/mio.c
index d99d267a..6dd6e93f 100644
--- a/src/map/mio/mio.c
+++ b/src/map/mio/mio.c
@@ -443,7 +443,7 @@ int Mio_CommandWriteGenlib( Abc_Frame_t * pAbc, int argc, char **argv )
         printf( "Error! Cannot open file \"%s\" for writing the library.\n", pFileName );
         return 1;
     }
-    Mio_WriteLibrary( pFile, (Mio_Library_t *)Abc_FrameReadLibGen(), 0 );
+    Mio_WriteLibrary( pFile, (Mio_Library_t *)Abc_FrameReadLibGen(), 0, 0 );
     fclose( pFile );
     printf( "The current genlib library is written into file \"%s\".\n", pFileName );
     return 0;
@@ -472,7 +472,8 @@ int Mio_CommandPrintGenlib( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNet;
-    int fVerbose;
+    int fShort = 0;
+    int fVerbose = 0;
     int c;
 
     pNet = Abc_FrameReadNtk(pAbc);
@@ -480,12 +481,14 @@ int Mio_CommandPrintGenlib( Abc_Frame_t * pAbc, int argc, char **argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set the defaults
-    fVerbose = 1;
     Extra_UtilGetoptReset();
-    while ( (c = Extra_UtilGetopt(argc, argv, "vh")) != EOF ) 
+    while ( (c = Extra_UtilGetopt(argc, argv, "svh")) != EOF ) 
     {
         switch (c) 
         {
+            case 's':
+                fShort ^= 1;
+                break;
             case 'v':
                 fVerbose ^= 1;
                 break;
@@ -501,12 +504,13 @@ int Mio_CommandPrintGenlib( Abc_Frame_t * pAbc, int argc, char **argv )
         printf( "Library is not available.\n" );
         return 1;
     }
-    Mio_WriteLibrary( stdout, (Mio_Library_t *)Abc_FrameReadLibGen(), 0 );
+    Mio_WriteLibrary( stdout, (Mio_Library_t *)Abc_FrameReadLibGen(), 0, fShort );
     return 0;
 
 usage:
-    fprintf( pErr, "\nusage: print_genlib [-vh]\n");
+    fprintf( pErr, "\nusage: print_genlib [-svh]\n");
     fprintf( pErr, "\t          print the current genlib library\n" );  
+    fprintf( pErr, "\t-s      : toggles writing short form [default = %s]\n", fShort? "yes" : "no" );
     fprintf( pErr, "\t-v      : toggles enabling of verbose output [default = %s]\n", fVerbose? "yes" : "no" );
     fprintf( pErr, "\t-h      : print the command usage\n");
     return 1;       
diff --git a/src/map/mio/mio.h b/src/map/mio/mio.h
index e7b1c05e..9dd72d93 100644
--- a/src/map/mio/mio.h
+++ b/src/map/mio/mio.h
@@ -58,6 +58,7 @@ typedef struct Mio_Cell2_t_ Mio_Cell2_t;
 struct Mio_Cell2_t_
 {
     char *          pName;          // name
+    Vec_Int_t *     vExpr;          // expression
     unsigned        Id       : 28;  // gate ID
     unsigned        nFanins  :  4;  // gate fanins
     word            Area;           // area
@@ -177,7 +178,7 @@ extern void              Mio_LibraryDelete( Mio_Library_t * pLib );
 extern void              Mio_GateDelete( Mio_Gate_t * pGate );
 extern void              Mio_PinDelete( Mio_Pin_t * pPin );
 extern Mio_Pin_t *       Mio_PinDup( Mio_Pin_t * pPin );
-extern void              Mio_WriteLibrary( FILE * pFile, Mio_Library_t * pLib, int fPrintSops );
+extern void              Mio_WriteLibrary( FILE * pFile, Mio_Library_t * pLib, int fPrintSops, int fShort );
 extern Mio_Gate_t **     Mio_CollectRoots( Mio_Library_t * pLib, int nInputs, float tDelay, int fSkipInv, int * pnGates, int fVerbose );
 extern Mio_Cell_t *      Mio_CollectRootsNew( Mio_Library_t * pLib, int nInputs, int * pnGates, int fVerbose );
 extern Mio_Cell_t *      Mio_CollectRootsNewDefault( int nInputs, int * pnGates, int fVerbose );
diff --git a/src/map/mio/mioRead.c b/src/map/mio/mioRead.c
index 6e067fa7..0364d363 100644
--- a/src/map/mio/mioRead.c
+++ b/src/map/mio/mioRead.c
@@ -329,6 +329,16 @@ int Mio_LibraryReadInternal( Mio_Library_t * pLib, char * pBuffer, int fExtended
   SeeAlso     []
 
 ***********************************************************************/
+char * Mio_LibraryCleanStr( char * p )
+{
+    int i, k;
+    char * pRes = Abc_UtilStrsav( p );
+    for ( i = k = 0; pRes[i]; i++ )
+        if ( pRes[i] != ' ' && pRes[i] != '\t' && pRes[i] != '\r' && pRes[i] != '\n' )
+            pRes[k++] = pRes[i];
+    pRes[k] = 0;
+    return pRes;
+}
 Mio_Gate_t * Mio_LibraryReadGate( char ** ppToken, int fExtendedFormat )
 {
     Mio_Gate_t * pGate;
@@ -354,7 +364,7 @@ Mio_Gate_t * Mio_LibraryReadGate( char ** ppToken, int fExtendedFormat )
 
     // then rest of the expression 
     pToken = strtok( NULL, ";" );
-    pGate->pForm = chomp( pToken );
+    pGate->pForm = Mio_LibraryCleanStr( pToken );
 
     // read the pin info
     // start the linked list of pins
diff --git a/src/map/mio/mioUtils.c b/src/map/mio/mioUtils.c
index a67aa5a1..bb24c7c8 100644
--- a/src/map/mio/mioUtils.c
+++ b/src/map/mio/mioUtils.c
@@ -200,10 +200,10 @@ void Mio_WritePin( FILE * pFile, Mio_Pin_t * pPin, int NameLen, int fAllPins )
     fprintf( pFile, "%7s ",   pPhaseNames[pPin->Phase] );
     fprintf( pFile, "%3d ",   (int)pPin->dLoadInput );
     fprintf( pFile, "%3d ",   (int)pPin->dLoadMax );
-    fprintf( pFile, "%6.2f ", pPin->dDelayBlockRise );
-    fprintf( pFile, "%6.2f ", pPin->dDelayFanoutRise );
-    fprintf( pFile, "%6.2f ", pPin->dDelayBlockFall );
-    fprintf( pFile, "%6.2f",  pPin->dDelayFanoutFall );
+    fprintf( pFile, "%8.2f ", pPin->dDelayBlockRise );
+    fprintf( pFile, "%8.2f ", pPin->dDelayFanoutRise );
+    fprintf( pFile, "%8.2f ", pPin->dDelayBlockFall );
+    fprintf( pFile, "%8.2f",  pPin->dDelayFanoutFall );
 }
 
 /**Function*************************************************************
@@ -225,7 +225,7 @@ void Mio_WriteGate( FILE * pFile, Mio_Gate_t * pGate, int GateLen, int NameLen,
     sprintf( Buffer, "%s=%s;",    pGate->pOutName, pGate->pForm );
     fprintf( pFile, "GATE %-*s ", GateLen, pGate->pName );
     fprintf( pFile, "%8.2f  ",    pGate->dArea );
-    fprintf( pFile, "%-*s ",      Abc_MinInt(NameLen+FormLen+2, 30), Buffer );
+    fprintf( pFile, "%-*s ",      Abc_MinInt(NameLen+FormLen+2, 60), Buffer );
     // print the pins
     if ( fPrintSops )
         fprintf( pFile, "%s",       pGate->pSop? pGate->pSop : "unspecified\n" );
@@ -248,12 +248,12 @@ void Mio_WriteGate( FILE * pFile, Mio_Gate_t * pGate, int GateLen, int NameLen,
   SeeAlso     []
 
 ***********************************************************************/
-void Mio_WriteLibrary( FILE * pFile, Mio_Library_t * pLib, int fPrintSops )
+void Mio_WriteLibrary( FILE * pFile, Mio_Library_t * pLib, int fPrintSops, int fShort )
 {
     Mio_Gate_t * pGate;
     Mio_Pin_t * pPin;
     int i, GateLen = 0, NameLen = 0, FormLen = 0;
-    int fAllPins = Mio_CheckGates( pLib );
+    int fAllPins = fShort || Mio_CheckGates( pLib );
     Mio_LibraryForEachGate( pLib, pGate )
     {
         GateLen = Abc_MaxInt( GateLen, strlen(pGate->pName) );
@@ -631,6 +631,7 @@ static inline void Mio_CollectCopy2( Mio_Cell2_t * pCell, Mio_Gate_t * pGate )
 {
     Mio_Pin_t * pPin;  int k;
     pCell->pName    = pGate->pName;
+    pCell->vExpr    = pGate->vExpr;
     pCell->uTruth   = pGate->uTruth;
     pCell->Area     = (word)(MIO_NUM * pGate->dArea);
     pCell->nFanins  = pGate->nInputs;
diff --git a/src/opt/sfm/sfmDec.c b/src/opt/sfm/sfmDec.c
index 962e29d5..ed3f7942 100644
--- a/src/opt/sfm/sfmDec.c
+++ b/src/opt/sfm/sfmDec.c
@@ -22,6 +22,8 @@
 #include "misc/st/st.h"
 #include "map/mio/mio.h"
 #include "base/abc/abc.h"
+#include "misc/util/utilTruth.h"
+#include "opt/dau/dau.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -30,13 +32,12 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-#define SFM_FAN_MAX 6
-
 typedef struct Sfm_Dec_t_ Sfm_Dec_t;
 struct Sfm_Dec_t_
 {
-    // parameters
+    // external
     Sfm_Par_t *       pPars;       // parameters
+    Sfm_Lib_t *       pLib;        // library
     // library
     Vec_Int_t         vGateSizes;  // fanin counts
     Vec_Wrd_t         vGateFuncs;  // gate truth tables
@@ -52,6 +53,7 @@ struct Sfm_Dec_t_
     int               nDivs;       // the number of divisors
     int               nMffc;       // the number of divisors
     int               iTarget;     // target node
+    int               fUseLast;    // internal switch
     Vec_Int_t         vObjRoots;   // roots of the window
     Vec_Int_t         vObjGates;   // functionality
     Vec_Wec_t         vObjFanins;  // fanin IDs
@@ -61,10 +63,11 @@ struct Sfm_Dec_t_
     sat_solver *      pSat;        // reusable solver 
     Vec_Wec_t         vClauses;    // CNF clauses for the node
     Vec_Int_t         vImpls[2];   // onset/offset implications
-    Vec_Int_t         vCounts[2];  // onset/offset counters
     Vec_Wrd_t         vSets[2];    // onset/offset patterns
     int               nPats[2];    // CEX count
     word              uMask[2];    // mask count
+    word              TtElems[SFM_SUPP_MAX][SFM_WORD_MAX];
+    word *            pTtElems[SFM_SUPP_MAX];
     // temporary
     Vec_Int_t         vTemp;
     Vec_Int_t         vTemp2;
@@ -138,14 +141,21 @@ void Sfm_ParSetDefault3( Sfm_Par_t * pPars )
 ***********************************************************************/
 Sfm_Dec_t * Sfm_DecStart( Sfm_Par_t * pPars )
 {
-    Sfm_Dec_t * p = ABC_CALLOC( Sfm_Dec_t, 1 );
+    Sfm_Dec_t * p = ABC_CALLOC( Sfm_Dec_t, 1 ); int i;
     p->pPars = pPars;
     p->pSat = sat_solver_new();
     p->timeStart = Abc_Clock();
+    for ( i = 0; i < SFM_SUPP_MAX; i++ )
+        p->pTtElems[i] = p->TtElems[i];
+    Abc_TtElemInit( p->pTtElems, SFM_SUPP_MAX );
+    p->pLib = Sfm_LibPrepare( pPars->nMffcMax + 1, 1, pPars->fVerbose );
+    if ( pPars->fVeryVerbose )
+        Sfm_LibPrint( p->pLib );
     return p;
 }
 void Sfm_DecStop( Sfm_Dec_t * p )
 {
+    Sfm_LibStop( p->pLib );
     // library
     Vec_IntErase( &p->vGateSizes );
     Vec_WrdErase( &p->vGateFuncs );
@@ -162,8 +172,6 @@ void Sfm_DecStop( Sfm_Dec_t * p )
     Vec_WecErase( &p->vClauses );
     Vec_IntErase( &p->vImpls[0] );
     Vec_IntErase( &p->vImpls[1] );
-    Vec_IntErase( &p->vCounts[0] );
-    Vec_IntErase( &p->vCounts[1] );
     Vec_WrdErase( &p->vSets[0] );
     Vec_WrdErase( &p->vSets[1] );
     // temporary
@@ -270,25 +278,59 @@ int Sfm_DecPrepareSolver( Sfm_Dec_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Sfm_DecFindWeight( Sfm_Dec_t * p, int c, int iLit )
+int Sfm_DecFindWeight( Sfm_Dec_t * p, int c, int iLit, word Mask )
+{
+    int Value0 = Abc_TtCountOnes( Vec_WrdEntry(&p->vSets[!c], Abc_Lit2Var(iLit)) & Mask );
+    int Weight0 = Abc_LitIsCompl(iLit) ? Abc_TtCountOnes( p->uMask[!c] & Mask ) - Value0 : Value0;
+    return Weight0;
+}
+void Sfm_DecPrint( Sfm_Dec_t * p, word * Masks )
 {
-    int Value = Vec_IntEntry( &p->vCounts[!c], Abc_Lit2Var(iLit) );
-    return Abc_LitIsCompl(iLit) ? Value : p->nPats[!c] - Value;
+    int c, i, k, Entry;
+    for ( c = 0; c < 2; c++ )
+    {
+        Vec_Int_t * vLevel = Vec_WecEntry( &p->vObjFanins, p->iTarget );
+        printf( "\n%s-SET of object %d (divs = %d) with gate \"%s\" and fanins: ", 
+            c ? "OFF": "ON", p->iTarget, p->nDivs, 
+            Mio_GateReadName((Mio_Gate_t *)Vec_PtrEntry(&p->vGateHands, Vec_IntEntry(&p->vObjGates,p->iTarget))) );
+        Vec_IntForEachEntry( vLevel, Entry, i )
+            printf( "%d ", Entry );
+        printf( "\n" );
+
+        printf( "Implications: " );
+        Vec_IntForEachEntry( &p->vImpls[c], Entry, i )
+            printf( "%s%d(%d) ", Abc_LitIsCompl(Entry)? "!":"", Abc_Lit2Var(Entry), Sfm_DecFindWeight(p, c, Entry, Masks ? Masks[!c] : ~(word)0) );
+        printf( "\n" );
+        printf( "     " );
+        for ( i = 0; i <= p->iTarget; i++ )
+            printf( "%d", i / 10 );
+        printf( "\n" );
+        printf( "     " );
+        for ( i = 0; i <= p->iTarget; i++ )
+            printf( "%d", i % 10 );
+        printf( "\n" );
+        for ( k = 0; k < p->nPats[c]; k++ )
+        {
+            printf( "%2d : ", k );
+            for ( i = 0; i <= p->iTarget; i++ )
+                printf( "%d", (int)((Vec_WrdEntry(&p->vSets[c], i) >> k) & 1) );
+            printf( "\n" );
+        }
+        printf( "\n" );
+    }
 }
 int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst )
 {
     int fVerbose = p->pPars->fVeryVerbose;
     int nBTLimit = 0;
     int i, k, c, Entry, status, Lits[3], RetValue;
-    int iLitBest = -1, iCBest = -1, WeightBest = -1, Weight;
+    int iLitBest = -1, iCBest = -1, WeightBest = ABC_INFINITY, Weight;
     *pfConst = -1;
     // check stuck-at-0/1 (on/off-set empty)
     p->nPats[0] = p->nPats[1] = 0;
     p->uMask[0] = p->uMask[1] = 0;
     Vec_IntClear( &p->vImpls[0] );
     Vec_IntClear( &p->vImpls[1] );
-    Vec_IntClear( &p->vCounts[0] );
-    Vec_IntClear( &p->vCounts[1] );
     Vec_WrdClear( &p->vSets[0] );
     Vec_WrdClear( &p->vSets[1] );
     for ( c = 0; c < 2; c++ )
@@ -309,11 +351,7 @@ int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst )
         assert( status == l_True );
         // record this status
         for ( i = 0; i <= p->iTarget; i++ )
-        {
-            Entry = sat_solver_var_value(p->pSat, i);
-            Vec_IntPush( &p->vCounts[c], Entry );
-            Vec_WrdPush( &p->vSets[c], (word)Entry );
-        }
+            Vec_WrdPush( &p->vSets[c], (word)sat_solver_var_value(p->pSat, i) );
         p->nPats[c]++;
         p->uMask[c] = 1;
     }
@@ -342,10 +380,7 @@ int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst )
             // record this status
             for ( k = 0; k <= p->iTarget; k++ )
                 if ( sat_solver_var_value(p->pSat, k) )
-                {
-                    Vec_IntAddToEntry( &p->vCounts[c], k, 1 );
                     *Vec_WrdEntryP(&p->vSets[c], k) |= ((word)1 << p->nPats[c]);
-                }
             p->uMask[c] |= ((word)1 << p->nPats[c]++);
         }
     }
@@ -354,8 +389,8 @@ int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst )
     {
         Vec_IntForEachEntry( &p->vImpls[c], Entry, i )
         {
-            Weight = Sfm_DecFindWeight(p, c, Entry);
-            if ( WeightBest < Weight )
+            Weight = Sfm_DecFindWeight(p, c, Entry, (~(word)0));
+            if ( WeightBest > Weight )
             {
                 WeightBest = Weight;
                 iLitBest = Entry;
@@ -363,7 +398,7 @@ int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst )
             }
         }
     }
-    if ( WeightBest == -1 )
+    if ( WeightBest == ABC_INFINITY )
     {
         p->nNoDecs++;
         return -2;
@@ -376,43 +411,11 @@ int Sfm_DecPeformDecOne( Sfm_Dec_t * p, int * pfConst )
     if ( RetValue == 0 )
         return -1;
 
-
     // print the results
-    if ( !fVerbose )
-        return Abc_Var2Lit( iLitBest, iCBest );
-
-    printf( "\nBest literal (%d; %s%d) with weight %d.\n\n", iCBest, Abc_LitIsCompl(iLitBest)? "!":"", Abc_Lit2Var(iLitBest), WeightBest );
-
-    for ( c = 0; c < 2; c++ )
+    if ( fVerbose )
     {
-        Vec_Int_t * vLevel = Vec_WecEntry( &p->vObjFanins, p->iTarget );
-        printf( "\n%s-SET of object %d (divs = %d) with gate \"%s\" and fanins: ", 
-            c ? "OFF": "ON", p->iTarget, p->nDivs, 
-            Mio_GateReadName((Mio_Gate_t *)Vec_PtrEntry(&p->vGateHands, Vec_IntEntry(&p->vObjGates,p->iTarget))) );
-        Vec_IntForEachEntry( vLevel, Entry, i )
-            printf( "%d ", Entry );
-        printf( "\n" );
-
-        printf( "Implications: " );
-        Vec_IntForEachEntry( &p->vImpls[c], Entry, i )
-            printf( "%s%d(%d) ", Abc_LitIsCompl(Entry)? "!":"", Abc_Lit2Var(Entry), Sfm_DecFindWeight(p, c, Entry) );
-        printf( "\n" );
-        printf( "     " );
-        for ( i = 0; i <= p->iTarget; i++ )
-            printf( "%d", i / 10 );
-        printf( "\n" );
-        printf( "     " );
-        for ( i = 0; i <= p->iTarget; i++ )
-            printf( "%d", i % 10 );
-        printf( "\n" );
-        for ( k = 0; k < p->nPats[c]; k++ )
-        {
-            printf( "%2d : ", k );
-            for ( i = 0; i <= p->iTarget; i++ )
-                printf( "%d", (int)((Vec_WrdEntry(&p->vSets[c], i) >> k) & 1) );
-            printf( "\n" );
-        }
-        printf( "\n" );
+        printf( "\nBest literal (%d; %s%d) with weight %d.\n\n", iCBest, Abc_LitIsCompl(iLitBest)? "!":"", Abc_Lit2Var(iLitBest), WeightBest );
+        Sfm_DecPrint( p, NULL );
     }
     return Abc_Var2Lit( iLitBest, iCBest );
 }
@@ -507,6 +510,216 @@ int Sfm_DecPeformDec( Sfm_Dec_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sfm_DecCombineDec( Sfm_Dec_t * p, word * pTruth0, word * pTruth1, int * pSupp0, int * pSupp1, int nSupp0, int nSupp1, word * pTruth, int * pSupp, int Var )
+{
+    Vec_Int_t vVec0 = { 2*SFM_SUPP_MAX, nSupp0, pSupp0 };
+    Vec_Int_t vVec1 = { 2*SFM_SUPP_MAX, nSupp1, pSupp1 };
+    Vec_Int_t vVec  = { 2*SFM_SUPP_MAX, 0,      pSupp  };
+    int nWords0 = Abc_TtWordNum(nSupp0);
+    int nWords1 = Abc_TtWordNum(nSupp1);
+    int nSupp, iSuppVar;
+    // check the case of equal cofactors
+    if ( nSupp0 == nSupp1 && !memcmp(pSupp0, pSupp1, sizeof(int)*nSupp0) && !memcmp(pTruth0, pTruth1, sizeof(word)*nWords0) )
+    {
+        memcpy( pSupp,  pSupp0,  sizeof(int)*nSupp0   );
+        memcpy( pTruth, pTruth0, sizeof(word)*nWords0 );
+        return nSupp0;
+    }
+    // merge support variables
+    Vec_IntTwoMerge2Int( &vVec0, &vVec1, &vVec );
+    Vec_IntPushOrder( &vVec, Var );
+    nSupp = Vec_IntSize( &vVec );
+    if ( nSupp > SFM_SUPP_MAX )
+        return -2;
+    // expand truth tables
+    Abc_TtStretch6( pTruth0, nSupp0, nSupp );
+    Abc_TtStretch6( pTruth1, nSupp1, nSupp );
+    Abc_TtExpand( pTruth0, nSupp, pSupp0, nSupp0, pSupp, nSupp );
+    Abc_TtExpand( pTruth1, nSupp, pSupp1, nSupp1, pSupp, nSupp );
+    // perform operation
+    iSuppVar = Vec_IntFind( &vVec, Var );
+    Abc_TtMux( pTruth, p->pTtElems[iSuppVar], pTruth1, pTruth0, Abc_TtWordNum(nSupp) );
+    return nSupp;
+}
+int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssump, int nAssump, word Masks[2], int fCofactor )
+{
+    int nBTLimit = 0;
+    int fVerbose = p->pPars->fVeryVerbose;
+    int c, i, d, Var, WeightBest, status;
+    Vec_Int_t vAss = { SFM_SUPP_MAX, nAssump, pAssump };
+//    if ( nAssump > SFM_SUPP_MAX )
+    if ( nAssump > p->nMffc )
+        return -2;
+    // check constant
+    for ( c = 0; c < 2; c++ )
+    {
+        if ( p->uMask[c] & Masks[c] ) // there are some patterns
+            continue;
+        p->nSatCalls++;
+        pAssump[nAssump] = Abc_Var2Lit( p->iTarget, c );
+        status = sat_solver_solve( p->pSat, pAssump, pAssump + nAssump + 1, nBTLimit, 0, 0, 0 );
+        if ( status == l_Undef )
+            return -2;
+        if ( status == l_False )
+        {
+            pTruth[0] = c ? ~((word)0) : 0;
+            return 0;
+        }
+        assert( status == l_True );
+        if ( p->nPats[c] == 64 )
+            return -2;//continue;
+        for ( i = 0; i <= p->iTarget; i++ )
+            if ( sat_solver_var_value(p->pSat, i) )
+                *Vec_WrdEntryP(&p->vSets[c], i) |= ((word)1 << p->nPats[c]);
+        p->uMask[c] |= ((word)1 << p->nPats[c]++);
+    }
+    // check implications
+    Vec_IntClear( &p->vImpls[0] );
+    Vec_IntClear( &p->vImpls[1] );
+    for ( d = 0; d < p->nDivs; d++ )
+    {
+        int Impls[2] = {-1, -1};
+        for ( c = 0; c < 2; c++ )
+        {
+            word MaskAll = p->uMask[c] & Masks[c];
+            word MaskCur = Vec_WrdEntry(&p->vSets[c], d) & Masks[c];
+            assert( MaskAll );
+            if ( MaskCur != 0 && MaskCur != MaskAll ) // has both ones and zeros
+                continue;
+            pAssump[nAssump]   = Abc_Var2Lit( p->iTarget, c );
+            pAssump[nAssump+1] = Abc_Var2Lit( d, MaskCur != 0 );
+            p->nSatCalls++;
+            status = sat_solver_solve( p->pSat, pAssump, pAssump + nAssump + 2, nBTLimit, 0, 0, 0 );
+            if ( status == l_Undef )
+                return -2;
+            if ( status == l_False )
+            {
+                Impls[c] = Abc_LitNot(pAssump[nAssump+1]);
+                Vec_IntPush( &p->vImpls[c], Abc_LitNot(pAssump[nAssump+1]) );
+                continue;
+            }
+            assert( status == l_True );
+            if ( p->nPats[c] == 64 )
+                return -2;//continue;
+            // record this status
+            for ( i = 0; i <= p->iTarget; i++ )
+                if ( sat_solver_var_value(p->pSat, i) )
+                    *Vec_WrdEntryP(&p->vSets[c], i) |= ((word)1 << p->nPats[c]);
+            p->uMask[c] |= ((word)1 << p->nPats[c]++);
+        }
+        if ( Impls[0] == -1 || Impls[1] == -1 || Impls[0] == Impls[1] )
+            continue;
+        assert( Abc_Lit2Var(Impls[0]) == Abc_Lit2Var(Impls[1]) );
+        // found buffer/inverter
+        pTruth[0] = Abc_LitIsCompl(Impls[0]) ? ~p->pTtElems[0][0] : p->pTtElems[0][0];
+        pSupp[0] = Abc_Lit2Var(Impls[0]);
+        return 1;        
+    }
+
+    // find the best cofactoring variable
+    Var = -1, WeightBest = ABC_INFINITY;
+    for ( c = 0; c < 2; c++ )
+    {
+        int iLit, Weight;
+        Vec_IntForEachEntry( &p->vImpls[c], iLit, i )
+        {
+            Weight = Sfm_DecFindWeight( p, c, iLit, Masks[!c] );
+            if ( WeightBest > Weight )
+            {
+                WeightBest = Weight;
+                Var = Abc_Lit2Var(iLit);
+            }
+        }
+    }
+    if ( Var == -1 && fCofactor )
+    {
+        if ( p->fUseLast )
+            Var = p->nDivs - 1;
+        else
+            Var = p->nDivs - 2;
+        fCofactor = 0;
+    }
+
+//    printf( "Assumptions: " );
+//    Vec_IntPrint( &vAss );
+//    Sfm_DecPrint( p, Masks );
+//printf( "Best var %d with weight %d.\n", Var, WeightBest );
+
+    // cofactor the problem
+    if ( Var >= 0 )
+    {
+        word uTruth[2][SFM_WORD_MAX], MasksNext[2];
+        int Supp[2][2*SFM_SUPP_MAX], nSupp[2], nSuppAll;
+        //if ( Abc_TtCountOnes(
+
+        for ( i = 0; i < 2; i++ )
+        {
+            for ( c = 0; c < 2; c++ )
+            {
+                word MaskVar = Vec_WrdEntry(&p->vSets[c], Var);
+                MasksNext[c] = Masks[c] & (i ? MaskVar | ~p->uMask[c] : ~MaskVar);
+            }
+            pAssump[nAssump] = Abc_Var2Lit( Var, !i );
+            nSupp[i] = Sfm_DecPeformDec_rec( p, uTruth[i], Supp[i], pAssump, nAssump+1, MasksNext, fCofactor );
+            if ( nSupp[i] == -2 )
+                return -2;
+        }
+        // combine solutions
+        nSuppAll = Sfm_DecCombineDec( p, uTruth[0], uTruth[1], Supp[0], Supp[1], nSupp[0], nSupp[1], pTruth, pSupp, Var );
+        //if ( nSuppAll > p->nMffc )
+        //    return -2;
+        return nSuppAll;
+    }
+    return -2;
+}
+int Sfm_DecPeformDec2Int( Sfm_Dec_t * p )
+{
+    word uTruth[SFM_WORD_MAX];
+    word Masks[2] = { ~((word)0), ~((word)0) };
+    int pAssump[2*SFM_SUPP_MAX];
+    int pSupp[2*SFM_SUPP_MAX], nSupp;
+    p->nPats[0] = p->nPats[1] = 0;
+    p->uMask[0] = p->uMask[1] = 0;
+    Vec_WrdFill( &p->vSets[0], p->iTarget+1, 0 );
+    Vec_WrdFill( &p->vSets[1], p->iTarget+1, 0 );
+    nSupp = Sfm_DecPeformDec_rec( p, uTruth, pSupp, pAssump, 0, Masks, 1 );
+//printf( "%d %d  ", p->nPats[0], p->nPats[1] );
+
+//    printf( "Node %4d : ", p->iTarget );
+//    printf( "MFFC %2d  ", p->nMffc );
+    if ( nSupp == -2 )
+    {
+//        printf( "NO DEC.\n" );
+        p->nNoDecs++;
+        return -2;
+    }
+    // transform truth table
+    Dau_DsdPrintFromTruth( uTruth, nSupp );
+    return -1;
+}
+int Sfm_DecPeformDec2( Sfm_Dec_t * p )
+{
+    p->fUseLast = 1;
+    Sfm_DecPeformDec2Int( p );
+//    p->fUseLast = 0;
+//    Sfm_DecPeformDec2Int( p );
+//    printf( "\n" );
+
+    //Sfm_LibImplement( p->pLib, uTruth, pSupp, nSupp, &p->vObjGates, &p->vObjFanins );
+    return -1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Incremental level update.]
 
   Description []
@@ -790,8 +1003,8 @@ void Abc_NtkPerformMfs3( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
     Sfm_Dec_t * p = Sfm_DecStart( pPars );
     Abc_Obj_t * pObj; 
     abctime clk;
-    int i, Limit, RetValue, Count = 0, nStop = Abc_NtkObjNumMax(pNtk);
-    //int iNode = 2341;//8;//70;
+    int i = 0, Limit, RetValue, Count = 0, nStop = Abc_NtkObjNumMax(pNtk);
+    int iNode = 70; //2341;//8;//70;
     printf( "Running remapping with parameters: " );
     printf( "TFO = %d. ", pPars->nTfoLevMax );
     printf( "TFI = %d. ", pPars->nTfiLevMax );
@@ -844,11 +1057,18 @@ p->timeCnf += Abc_Clock() - clk;
         if ( !RetValue )
             continue;
 clk = Abc_Clock();
-        RetValue = Sfm_DecPeformDec( p );
+        
+        if ( pPars->fRrOnly )
+            RetValue = Sfm_DecPeformDec( p );
+        else
+            RetValue = Sfm_DecPeformDec2( p );
 p->timeSat += Abc_Clock() - clk;
-        if ( RetValue == -1 )
+
+//break;
+        if ( RetValue < 0 )
             continue;
-        Sfm_DecInsert( pNtk, pObj, Limit, &p->vObjGates, &p->vObjFanins, &p->vObjMap, &p->vGateHands );
+        if ( pPars->fRrOnly )
+            Sfm_DecInsert( pNtk, pObj, Limit, &p->vObjGates, &p->vObjFanins, &p->vObjMap, &p->vGateHands );
 if ( pPars->fVeryVerbose )
 printf( "This was modification %d\n", Count );
         //if ( Count == 2 )
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index 84a4491a..285ab2a6 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -45,10 +45,16 @@ ABC_NAMESPACE_HEADER_START
 #define SFM_SAT_UNDEC 0x1234567812345678
 #define SFM_SAT_SAT   0x8765432187654321
 
+#define SFM_SUPP_MAX  6
+#define SFM_WORD_MAX ((SFM_SUPP_MAX>6) ? (1<<(SFM_SUPP_MAX-6)) : 1)
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
+typedef struct Sfm_Fun_t_ Sfm_Fun_t; 
+typedef struct Sfm_Lib_t_ Sfm_Lib_t; 
+
 struct Sfm_Ntk_t_
 {
     // parameters
@@ -182,6 +188,11 @@ extern int          Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, V
 extern Vec_Wec_t *  Sfm_CreateCnf( Sfm_Ntk_t * p );
 extern void         Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap, int iPivotVar );
 /*=== sfmCore.c ==========================================================*/
+/*=== sfmLib.c ==========================================================*/
+extern Sfm_Lib_t *  Sfm_LibPrepare( int nVars, int fTwo, int fVerbose );
+extern void         Sfm_LibPrint( Sfm_Lib_t * p );
+extern void         Sfm_LibStop( Sfm_Lib_t * p );
+extern int          Sfm_LibImplement( Sfm_Lib_t * p, word uTruth, int * pFanins, int nFanins, Vec_Int_t * vGates, Vec_Wec_t * vFanins );
 /*=== sfmNtk.c ==========================================================*/
 extern Sfm_Ntk_t *  Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPos );
 extern void         Sfm_NtkPrepare( Sfm_Ntk_t * p );
diff --git a/src/opt/sfm/sfmLib.c b/src/opt/sfm/sfmLib.c
index fefa21bb..97fd9af3 100644
--- a/src/opt/sfm/sfmLib.c
+++ b/src/opt/sfm/sfmLib.c
@@ -21,6 +21,11 @@
 #include "sfmInt.h"
 #include "misc/st/st.h"
 #include "map/mio/mio.h"
+#include "misc/vec/vecMem.h"
+#include "misc/util/utilTruth.h"
+#include "misc/extra/extra.h"
+#include "map/mio/exp.h"
+#include "opt/dau/dau.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -29,6 +34,31 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+struct Sfm_Fun_t_
+{
+    int             Next;          // next function in the list
+    int             Area;          // area of this function
+    char            pFansT[8];     // top gate ID, followed by fanin perm
+    char            pFansB[8];     // bottom gate ID, followed by fanin perm
+};
+struct Sfm_Lib_t_
+{
+    Mio_Cell2_t *   pCells;        // library gates
+    int             nCells;        // library gate count
+    int             nObjs;         // object count
+    int             nObjsAlloc;    // object count
+    Sfm_Fun_t *     pObjs;         // objects  
+    Vec_Mem_t *     vTtMem;        // truth tables
+    Vec_Int_t       vLists;        // lists of funcs for each truth table
+    Vec_Int_t       vCounts;       // counters of functions for each truth table
+};
+
+static inline Sfm_Fun_t * Sfm_LibFun( Sfm_Lib_t * p, int i ) { return i == -1 ? NULL : p->pObjs + i; }
+
+#define Sfm_LibForEachSuper( p, pObj, Func ) \
+    for ( pObj = Sfm_LibFun(p, Vec_IntEntry(&p->vLists, Func)); pObj; pObj = Sfm_LibFun(p, pObj->Next) )
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -93,6 +123,269 @@ void Sfm_LibPreprocess( Mio_Library_t * pLib, Vec_Int_t * vGateSizes, Vec_Wrd_t
     Sfm_DecCreateCnf( vGateSizes, vGateFuncs, vGateCnfs );
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Sfm_Lib_t * Sfm_LibStart( int nVars )
+{
+    Sfm_Lib_t * p = ABC_CALLOC( Sfm_Lib_t, 1 );
+    p->vTtMem = Vec_MemAllocForTT( nVars, 0 );   
+    Vec_IntGrow( &p->vLists,  (1 << 16) );
+    Vec_IntGrow( &p->vCounts, (1 << 16) );
+    Vec_IntFill( &p->vLists,  2, -1 );
+    Vec_IntFill( &p->vCounts, 2, -1 );
+    p->nObjsAlloc = (1 << 16);
+    p->pObjs = ABC_CALLOC( Sfm_Fun_t, p->nObjsAlloc );
+    return p;
+}
+void Sfm_LibStop( Sfm_Lib_t * p )
+{
+    Vec_MemHashFree( p->vTtMem );
+    Vec_MemFree( p->vTtMem );
+    Vec_IntErase( &p->vLists );
+    Vec_IntErase( &p->vCounts );
+    ABC_FREE( p->pCells );
+    ABC_FREE( p->pObjs );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+word Sfm_LibTruthTwo( Mio_Cell2_t * pCellBot, Mio_Cell2_t * pCellTop, int InTop )
+{
+    word uTruthBot = Exp_Truth6( pCellBot->nFanins, pCellBot->vExpr, NULL );
+    word uFanins[6]; int i, k;
+    assert( InTop >= 0 && InTop < (int)pCellTop->nFanins );
+    for ( i = 0, k = pCellBot->nFanins; i < (int)pCellTop->nFanins; i++ )
+        uFanins[i] = (i == InTop) ? uTruthBot : s_Truths6[k++];
+    assert( (int)pCellBot->nFanins + (int)pCellTop->nFanins == k + 1 );
+    uTruthBot = Exp_Truth6( pCellTop->nFanins, pCellTop->vExpr, uFanins );
+    return uTruthBot;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sfm_LibPrepareAdd( Sfm_Lib_t * p, word uTruth, int * Perm, int nFanins, Mio_Cell2_t * pCellBot, Mio_Cell2_t * pCellTop, int InTop )
+{
+    Sfm_Fun_t * pObj;
+    int Area = (int)(pCellBot->Area / 1000) + (pCellTop ? (int)(pCellTop->Area / 1000) : 0);
+    int i, k, iFunc = Vec_MemHashInsert( p->vTtMem, &uTruth );
+    if ( iFunc == Vec_IntSize(&p->vLists) )
+    {
+        Vec_IntPush( &p->vLists, -1 );
+        Vec_IntPush( &p->vCounts, 0 );
+    }
+    assert( pCellBot != NULL );
+    // iterate through the supergates of this truth table
+    Sfm_LibForEachSuper( p, pObj, iFunc )
+    {
+        if ( Area >= pObj->Area )
+            return;
+    }
+    // create new object
+    if ( p->nObjs == p->nObjsAlloc )
+    {
+        int nObjsAlloc = 2 * p->nObjsAlloc;
+        p->pObjs = ABC_REALLOC( Sfm_Fun_t, p->pObjs, nObjsAlloc );
+        memset( p->pObjs + p->nObjsAlloc, 0, sizeof(Sfm_Fun_t) * p->nObjsAlloc );
+        p->nObjsAlloc = nObjsAlloc;
+    }
+    pObj = p->pObjs + p->nObjs;
+    pObj->Area = Area;
+    pObj->Next = Vec_IntEntry(&p->vLists, iFunc);
+    Vec_IntWriteEntry( &p->vLists, iFunc, p->nObjs++ );
+    Vec_IntAddToEntry( &p->vCounts, iFunc, 1 );
+    // create gate
+    assert( pCellBot->Id < 128 );
+    pObj->pFansB[0] = (char)pCellBot->Id;
+    for ( k = 0; k < (int)pCellBot->nFanins; k++ )
+        pObj->pFansB[k+1] = Perm[k];
+    if ( pCellTop == NULL )
+        return;
+    assert( pCellTop->Id < 128 );
+    pObj->pFansT[0] = (char)pCellTop->Id;
+    for ( i = 0; i < (int)pCellTop->nFanins; i++ )
+        pObj->pFansT[i+1] = (char)(i == InTop ? 16 : Perm[k++]);
+    assert( k == nFanins );
+}
+Sfm_Lib_t * Sfm_LibPrepare( int nVars, int fTwo, int fVerbose )
+{
+    abctime clk = Abc_Clock();
+    Sfm_Lib_t * p = Sfm_LibStart( nVars );
+    Mio_Cell2_t * pCell1, * pCell2, * pLimit;
+    int * pPerm[7], * Perm1, * Perm2, Perm[6];
+    int nPerms[7], i, f, n;
+    Vec_Int_t * vUseful;
+    word tTemp1, tCur;
+    char pRes[1000];
+    assert( nVars <= 6 );
+    // precompute gates
+    p->pCells = Mio_CollectRootsNewDefault2( nVars, &p->nCells, 0 );
+    pLimit = p->pCells + p->nCells;
+    // find useful ones
+    vUseful = Vec_IntStart( p->nCells );
+//    vUseful = Vec_IntStartFull( p->nCells );
+    for ( pCell1 = p->pCells + 4; pCell1 < pLimit; pCell1++ )
+    {
+        word uTruth = pCell1->uTruth;
+        if ( Dau_DsdDecompose(&uTruth, pCell1->nFanins, 0, 0, pRes) <= 3 )
+            Vec_IntWriteEntry( vUseful, pCell1 - p->pCells, 1 );
+        else
+            printf( "Skipping gate \"%s\" with non-DSD function %s\n", pCell1->pName, pRes );
+    }
+    // generate permutations
+    for ( i = 2; i <= nVars; i++ )
+        pPerm[i] = Extra_PermSchedule( i );
+    for ( i = 2; i <= nVars; i++ )
+        nPerms[i] = Extra_Factorial( i );
+    // add single cells
+    for ( pCell1 = p->pCells + 4; pCell1 < pLimit; pCell1++ )
+    if ( Vec_IntEntry(vUseful, pCell1 - p->pCells) )
+    {
+        int nFanins = pCell1->nFanins;
+        assert( nFanins >= 2 && nFanins <= 6 );
+        for ( i = 0; i < nFanins; i++ )
+            Perm[i] = i;
+        // permute truth table
+        tCur = tTemp1 = pCell1->uTruth;
+        for ( n = 0; n < nPerms[nFanins]; n++ )
+        {
+            Sfm_LibPrepareAdd( p, tCur, Perm, nFanins, pCell1, NULL, -1 );
+            // update
+            tCur = Abc_Tt6SwapAdjacent( tCur, pPerm[nFanins][n] );
+            Perm1 = Perm + pPerm[nFanins][n];
+            Perm2 = Perm1 + 1;
+            ABC_SWAP( int, *Perm1, *Perm2 );
+        }
+        assert( tTemp1 == tCur );
+    }
+    // add double cells
+    if ( fTwo )
+    for ( pCell1 = p->pCells + 4; pCell1 < pLimit; pCell1++ )
+    if ( Vec_IntEntry(vUseful, pCell1 - p->pCells) )
+    for ( pCell2 = p->pCells + 4; pCell2 < pLimit; pCell2++ )
+    if ( Vec_IntEntry(vUseful, pCell2 - p->pCells) )
+    if ( (int)pCell1->nFanins + (int)pCell2->nFanins <= nVars + 1 )
+    for ( f = 0; f < (int)pCell2->nFanins; f++ )
+    {
+        int nFanins = pCell1->nFanins + pCell2->nFanins - 1;
+        assert( nFanins >= 2 && nFanins <= nVars );
+        for ( i = 0; i < nFanins; i++ )
+            Perm[i] = i;
+        // permute truth table
+        tCur = tTemp1 = Sfm_LibTruthTwo( pCell1, pCell2, f );
+        for ( n = 0; n < nPerms[nFanins]; n++ )
+        {
+            Sfm_LibPrepareAdd( p, tCur, Perm, nFanins, pCell1, pCell2, f );
+            // update
+            tCur = Abc_Tt6SwapAdjacent( tCur, pPerm[nFanins][n] );
+            Perm1 = Perm + pPerm[nFanins][n];
+            Perm2 = Perm1 + 1;
+            ABC_SWAP( int, *Perm1, *Perm2 );
+        }
+        assert( tTemp1 == tCur );
+    }
+    // cleanup
+    for ( i = 2; i <= nVars; i++ )
+        ABC_FREE( pPerm[i] );
+    Vec_IntFree( vUseful );
+    if ( fVerbose )
+    {
+        printf( "Library processing: Var = %d.  Cells = %d.  Func = %6d.  Obj = %8d.  Ave = %8.2f  ", nVars, p->nCells, Vec_MemEntryNum(p->vTtMem), p->nObjs, 1.0*p->nObjs/Vec_MemEntryNum(p->vTtMem) );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    }
+    return p;
+}
+void Sfm_LibPrintGate( Mio_Cell2_t * pCell, char * pFanins, Mio_Cell2_t * pCell2, char * pFanins2 )
+{
+    int k;
+    printf( " %s(", pCell->pName );
+    for ( k = 0; k < (int)pCell->nFanins; k++ )
+        if ( pFanins[k] == (char)16 )
+            Sfm_LibPrintGate( pCell2, pFanins2, NULL, NULL );
+        else
+            printf( " %c", 'a' + pFanins[k] );
+    printf( " )" );
+}
+void Sfm_LibPrintObj( Sfm_Lib_t * p, Sfm_Fun_t * pObj )
+{
+    Mio_Cell2_t * pCellB = p->pCells + (int)pObj->pFansB[0];
+    Mio_Cell2_t * pCellT = p->pCells + (int)pObj->pFansT[0];
+    int nFanins = pCellB->nFanins + (pCellT == p->pCells ? 0 : pCellT->nFanins);
+    printf( "     Area = %6.2f  Fanins = %d  ", 0.001*pObj->Area, nFanins );
+    if ( pCellT == p->pCells )
+        Sfm_LibPrintGate( pCellB, pObj->pFansB + 1, NULL, NULL );
+    else
+        Sfm_LibPrintGate( pCellT, pObj->pFansT + 1, pCellB, pObj->pFansB + 1 );
+    printf( "\n" );
+}
+void Sfm_LibPrint( Sfm_Lib_t * p )
+{
+    word * pTruth; Sfm_Fun_t * pObj; int iFunc; 
+    Vec_MemForEachEntry( p->vTtMem, pTruth, iFunc )
+    {
+        if ( iFunc < 2 ) 
+            continue;
+        //if ( iFunc % 10000 )
+        //    continue;
+        printf( "%d : Count = %d   ", iFunc, Vec_IntEntry(&p->vCounts, iFunc) );
+        Dau_DsdPrintFromTruth( pTruth, Abc_TtSupportSize(pTruth, 6) );
+        Sfm_LibForEachSuper( p, pObj, iFunc )
+            Sfm_LibPrintObj( p, pObj );
+    }
+}
+void Sfm_LibTest( int nVars, int fTwo, int fVerbose )
+{
+    Sfm_Lib_t * p = Sfm_LibPrepare( nVars, fTwo, 1 );
+    if ( fVerbose )
+        Sfm_LibPrint( p );
+    Sfm_LibStop( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sfm_LibImplement( Sfm_Lib_t * p, word uTruth, int * pFanins, int nFanins, Vec_Int_t * vGates, Vec_Wec_t * vFanins )
+{
+    return 0;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////