Merged alanmi/abc into default

16 files changed, 970 insertions, 61 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 58688983..def694fd 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1875,6 +1875,10 @@ SOURCE=.\src\sat\bmc\bmcFx.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\bmc\bmcGen.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\bmc\bmcICheck.c
 # End Source File
 # Begin Source File
@@ -2551,6 +2555,10 @@ SOURCE=.\src\opt\sfm\sfm.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\opt\sfm\sfmArea.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\opt\sfm\sfmCnf.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index dbfe38f3..946f6d4d 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -3747,21 +3747,17 @@ void Gia_ManCollectTopXors_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXo
     else
         Gia_ManCollectTopXors_rec( p, Gia_ObjFanin1(pObj), vXors );
 }
-Vec_Int_t * Gia_ManCollectTopXors( Gia_Man_t * p, Vec_Int_t * vPolar )
+Vec_Int_t * Gia_ManCollectTopXors( Gia_Man_t * p )
 {
     int i, iObj, iObj2, fFlip, * pPerm, Count1 = 0;
     Vec_Int_t * vXors, * vSizes, * vPart[2], * vOrder; 
     Gia_Obj_t * pFan[2], * pObj = Gia_ManCo(p, 0);
     assert( Gia_ManCoNum(p) == 1 );
-    Vec_IntClear( vPolar );
-    if ( !Gia_ObjFaninC0(pObj) )
-        return NULL;
     vXors = Vec_IntAlloc( 100 );
-    pObj = Gia_ObjFanin0(pObj);
-    if ( Gia_ObjIsAnd(pObj) )
-        Gia_ManCollectTopXors_rec( p, pObj, vXors );
+    if ( Gia_ObjFaninC0(pObj) )
+        Gia_ManCollectTopXors_rec( p, Gia_ObjFanin0(pObj), vXors );
     else
-        Vec_IntPush( vXors, Gia_ObjId(p, pObj) );
+        Vec_IntPush( vXors, Gia_ObjId(p, Gia_ObjFanin0(pObj)) );
     // order by support size
     vSizes = Vec_IntAlloc( 100 );
     Vec_IntForEachEntry( vXors, iObj, i )
@@ -3791,7 +3787,6 @@ Vec_Int_t * Gia_ManCollectTopXors( Gia_Man_t * p, Vec_Int_t * vPolar )
             pFan[0] = Gia_Regular(pFan[0]);
             pFan[1] = Gia_Regular(pFan[1]);
         }
-        Vec_IntPushTwo( vPolar, 0, fCompl );
         fFlip = Gia_ManDecideWhereToAdd( p, vPart, pFan );
         Vec_IntPush( vPart[0], Gia_ObjId(p, pFan[fFlip]) );
         Vec_IntPush( vPart[1], Gia_ObjId(p, pFan[!fFlip]) );
@@ -3808,22 +3803,20 @@ Vec_Int_t * Gia_ManCollectTopXors( Gia_Man_t * p, Vec_Int_t * vPolar )
     Vec_IntFree( vPart[0] );
     Vec_IntFree( vPart[1] );
     Vec_IntReverseOrder( vOrder ); // from LSB to MSB
-    Vec_IntReverseOrder( vPolar ); 
     //Vec_IntPrint( vOrder );
     return vOrder;
 }
 Gia_Man_t * Gia_ManDemiterToDual( Gia_Man_t * p )
 {
     Gia_Man_t * pNew; Gia_Obj_t * pObj; int i;
-    Vec_Int_t * vNodes, * vPolar = Vec_IntAlloc( 100 );
-    Vec_Int_t * vOrder = Gia_ManCollectTopXors( p, vPolar );
+    Vec_Int_t * vNodes;
+    Vec_Int_t * vOrder = Gia_ManCollectTopXors( p );
     if ( vOrder == NULL )
     {
-        Vec_IntFree( vPolar );
         printf( "Cannot demiter because the top-most gate is an AND-gate.\n" );
         return NULL;
     }
-    assert( Vec_IntSize(vOrder) == Vec_IntSize(vPolar) );
+    assert( Vec_IntSize(vOrder) % 2 == 0 );
     vNodes = Vec_IntAlloc( Gia_ManObjNum(p) );
     Gia_ManIncrementTravId( p );
     Gia_ManCollectAnds( p, Vec_IntArray(vOrder), Vec_IntSize(vOrder), vNodes, NULL );
@@ -3835,9 +3828,9 @@ Gia_Man_t * Gia_ManDemiterToDual( Gia_Man_t * p )
         pObj->Value = Gia_ManAppendCi( pNew );
     Gia_ManForEachObjVec( vNodes, p, pObj, i )
         pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManSetPhase( p );
     Gia_ManForEachObjVec( vOrder, p, pObj, i )
-        Gia_ManAppendCo( pNew, Abc_LitNotCond(pObj->Value, Vec_IntEntry(vPolar, i)) );
-    Vec_IntFree( vPolar );
+        Gia_ManAppendCo( pNew, Abc_LitNotCond(pObj->Value, pObj->fPhase) );
     Vec_IntFree( vNodes );
     Vec_IntFree( vOrder );
     return pNew;
diff --git a/src/aig/gia/giaNf.c b/src/aig/gia/giaNf.c
index 510e7ddb..6761b617 100644
--- a/src/aig/gia/giaNf.c
+++ b/src/aig/gia/giaNf.c
@@ -178,18 +178,17 @@ int Nf_StoCellIsDominated( Mio_Cell2_t * pCell, int * pFans, int * pProf )
             return 0;
     return 1; // pCell is dominated
 }
-void Nf_StoCreateGateAdd( Nf_Man_t * pMan, word uTruth, int * pFans, int nFans, int CellId, Vec_Wec_t * vProfs, Vec_Int_t * vStore )
+void Nf_StoCreateGateAdd( Vec_Mem_t * vTtMem, Vec_Wec_t * vTt2Match, Mio_Cell2_t * pCell, word uTruth, int * pFans, int nFans, Vec_Wec_t * vProfs, Vec_Int_t * vStore, int fPinFilter, int fPinPerm, int fPinQuick )
 {
     Vec_Int_t * vArray, * vArrayProfs = NULL;
-    Mio_Cell2_t * pCell = Nf_ManCell( pMan, CellId );
     int i, k, GateId, Entry, fCompl = (int)(uTruth & 1);
     word uFunc = fCompl ? ~uTruth : uTruth;
-    int iFunc = Vec_MemHashInsert( pMan->vTtMem, &uFunc );
+    int iFunc = Vec_MemHashInsert( vTtMem, &uFunc );
     Nf_Cfg_t Mat = Nf_Int2Cfg(0);
     // get match array
-    if ( iFunc == Vec_WecSize(pMan->vTt2Match) )
-        Vec_WecPushLevel( pMan->vTt2Match );
-    vArray = Vec_WecEntry( pMan->vTt2Match, iFunc );
+    if ( iFunc == Vec_WecSize(vTt2Match) )
+        Vec_WecPushLevel( vTt2Match );
+    vArray = Vec_WecEntry( vTt2Match, iFunc );
     // create match
     Mat.fCompl = fCompl;
     assert( nFans == (int)pCell->nFanins );
@@ -199,10 +198,10 @@ void Nf_StoCreateGateAdd( Nf_Man_t * pMan, word uTruth, int * pFans, int nFans,
         Mat.Phase |= (unsigned)(Abc_LitIsCompl(pFans[i]) << Abc_Lit2Var(pFans[i]));
     }
     // check other profiles
-    if ( pMan->pPars->fPinFilter )
+    if ( fPinFilter )
     {
         // get profile array
-        assert( Vec_WecSize(pMan->vTt2Match) == Vec_WecSize(vProfs) );
+        assert( Vec_WecSize(vTt2Match) == Vec_WecSize(vProfs) );
         if ( iFunc == Vec_WecSize(vProfs) )
             Vec_WecPushLevel( vProfs );
         vArrayProfs = Vec_WecEntry( vProfs, iFunc );
@@ -218,26 +217,26 @@ void Nf_StoCreateGateAdd( Nf_Man_t * pMan, word uTruth, int * pFans, int nFans,
             }
     }
     // check pin permutation
-    if ( !pMan->pPars->fPinPerm ) // do not use  pin-permutation (improves delay when pin-delays differ)
+    if ( !fPinPerm ) // do not use  pin-permutation (improves delay when pin-delays differ)
     {
-        if ( pMan->pPars->fPinQuick ) // reduce the number of matches agressively
+        if ( fPinQuick ) // reduce the number of matches agressively
         {
             Vec_IntForEachEntryDouble( vArray, GateId, Entry, i )
-                if ( GateId == CellId && Abc_TtBitCount8[Nf_Int2Cfg(Entry).Phase] == Abc_TtBitCount8[Mat.Phase] )
+                if ( GateId == (int)pCell->Id && Abc_TtBitCount8[Nf_Int2Cfg(Entry).Phase] == Abc_TtBitCount8[Mat.Phase] )
                     return;
         }
         else // reduce the number of matches less agressively
         {
             Vec_IntForEachEntryDouble( vArray, GateId, Entry, i )
-                if ( GateId == CellId && Nf_Int2Cfg(Entry).Phase == Mat.Phase )
+                if ( GateId == (int)pCell->Id && Nf_Int2Cfg(Entry).Phase == Mat.Phase )
                     return;
         }
     }
     // save data and profile
-    Vec_IntPush( vArray, CellId );
+    Vec_IntPush( vArray, pCell->Id );
     Vec_IntPush( vArray, Nf_Cfg2Int(Mat) );
     // add delay profile
-    if ( pMan->pPars->fPinFilter )
+    if ( fPinFilter )
     {
         Vec_IntPush( vArrayProfs, Vec_IntSize(vStore) );
         Vec_IntPush( vStore, Abc_Float2Int(pCell->AreaF) );
@@ -245,7 +244,7 @@ void Nf_StoCreateGateAdd( Nf_Man_t * pMan, word uTruth, int * pFans, int nFans,
             Vec_IntPush( vStore, pCell->iDelays[Abc_Lit2Var(pFans[k])] );
     }
 }
-void Nf_StoCreateGateMaches( Nf_Man_t * pMan, Mio_Cell2_t * pCell, int ** pComp, int ** pPerm, int * pnPerms, Vec_Wec_t * vProfs, Vec_Int_t * vStore )
+void Nf_StoCreateGateMaches( Vec_Mem_t * vTtMem, Vec_Wec_t * vTt2Match, Mio_Cell2_t * pCell, int ** pComp, int ** pPerm, int * pnPerms, Vec_Wec_t * vProfs, Vec_Int_t * vStore, int fPinFilter, int fPinPerm, int fPinQuick )
 {
     int Perm[NF_LEAF_MAX], * Perm1, * Perm2;
     int nPerms = pnPerms[pCell->nFanins];
@@ -261,7 +260,7 @@ void Nf_StoCreateGateMaches( Nf_Man_t * pMan, Mio_Cell2_t * pCell, int ** pComp,
         tTemp2 = tCur;
         for ( c = 0; c < nMints; c++ )
         {
-            Nf_StoCreateGateAdd( pMan, tCur, Perm, pCell->nFanins, pCell->Id, vProfs, vStore );
+            Nf_StoCreateGateAdd( vTtMem, vTt2Match, pCell, tCur, Perm, pCell->nFanins, vProfs, vStore, fPinFilter, fPinPerm, fPinQuick );
             // update
             tCur  = Abc_Tt6Flip( tCur, pComp[pCell->nFanins][c] );
             Perm1 = Perm + pComp[pCell->nFanins][c];
@@ -278,12 +277,14 @@ void Nf_StoCreateGateMaches( Nf_Man_t * pMan, Mio_Cell2_t * pCell, int ** pComp,
     }
     assert( tTemp1 == tCur );
 }
-void Nf_StoDeriveMatches( Nf_Man_t * p, int fVerbose )
+Mio_Cell2_t * Nf_StoDeriveMatches( Vec_Mem_t * vTtMem, Vec_Wec_t * vTt2Match, int * pnCells, int fPinFilter, int fPinPerm, int fPinQuick )
 {
-//    abctime clk = Abc_Clock();
+    int fVerbose = 0;
+    //abctime clk = Abc_Clock();
     Vec_Wec_t * vProfs = Vec_WecAlloc( 1000 );
     Vec_Int_t * vStore = Vec_IntAlloc( 10000 );
     int * pComp[7], * pPerm[7], nPerms[7], i;
+    Mio_Cell2_t * pCells;
     Vec_WecPushLevel( vProfs );
     Vec_WecPushLevel( vProfs );
     for ( i = 1; i <= 6; i++ )
@@ -292,18 +293,18 @@ void Nf_StoDeriveMatches( Nf_Man_t * p, int fVerbose )
         pPerm[i] = Extra_PermSchedule( i );
     for ( i = 1; i <= 6; i++ )
         nPerms[i] = Extra_Factorial( i );
-    p->pCells = Mio_CollectRootsNewDefault2( 6, &p->nCells, fVerbose );
-    for ( i = 2; i < p->nCells; i++ )
-        Nf_StoCreateGateMaches( p, p->pCells + i, pComp, pPerm, nPerms, vProfs, vStore );
+    pCells = Mio_CollectRootsNewDefault2( 6, pnCells, fVerbose );
+    for ( i = 2; i < *pnCells; i++ )
+        Nf_StoCreateGateMaches( vTtMem, vTt2Match, pCells+i, pComp, pPerm, nPerms, vProfs, vStore, fPinFilter, fPinPerm, fPinQuick );
     for ( i = 1; i <= 6; i++ )
         ABC_FREE( pComp[i] );
     for ( i = 1; i <= 6; i++ )
         ABC_FREE( pPerm[i] );
     Vec_WecFree( vProfs );
     Vec_IntFree( vStore );
-//    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    //Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    return pCells;
 }
-//void Nf_StoPrintOne( Nf_Man_t * p, int Count, int t, int i, int GateId, Pf_Mat_t Mat )
 void Nf_StoPrintOne( Nf_Man_t * p, int Count, int t, int i, int GateId, Nf_Cfg_t Mat )
 {
     Mio_Cell2_t * pC = p->pCells + GateId;
@@ -398,12 +399,7 @@ Nf_Man_t * Nf_StoCreate( Gia_Man_t * pGia, Jf_Par_t * pPars )
     }
     Vec_IntFree(vFlowRefs);
     // matching
-    p->vTtMem    = Vec_MemAllocForTT( 6, 0 );          
-    p->vTt2Match = Vec_WecAlloc( 1000 ); 
-    Vec_WecPushLevel( p->vTt2Match );
-    Vec_WecPushLevel( p->vTt2Match );
-    assert( Vec_WecSize(p->vTt2Match) == Vec_MemEntryNum(p->vTtMem) );
-    Nf_StoDeriveMatches( p, 0 );//pPars->fVerbose );
+    Mio_LibraryMatchesFetch( (Mio_Library_t *)Abc_FrameReadLibGen(), &p->vTtMem, &p->vTt2Match, &p->pCells, &p->nCells, p->pPars->fPinFilter, p->pPars->fPinPerm, p->pPars->fPinQuick );
     p->InvDelayI = p->pCells[3].iDelays[0];
     p->InvAreaW  = p->pCells[3].AreaW;
     p->InvAreaF  = p->pCells[3].AreaF;
@@ -424,11 +420,6 @@ void Nf_StoDelete( Nf_Man_t * p )
     ABC_FREE( p->vCutDelays.pArray );
     ABC_FREE( p->vBackup.pArray );
     ABC_FREE( p->pNfObjs );
-    // matching
-    Vec_WecFree( p->vTt2Match );
-    Vec_MemHashFree( p->vTtMem );
-    Vec_MemFree( p->vTtMem );
-    ABC_FREE( p->pCells );
     ABC_FREE( p );
 }
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f67bbb09..da3a2d96 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -41422,6 +41422,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Gia_ManCheckFalseTest( pAbc->pGia, nFrames );
 //    Gia_ParTest( pAbc->pGia, nWords, nProcs );
 //    Gia_PolynExplore( pAbc->pGia );
+//    Gia_ManTestSatEnum( pAbc->pGia );
 
 //    printf( "\nThis command is currently disabled.\n\n" );
     return 0;
diff --git a/src/base/wlc/wlc.c b/src/base/wlc/wlc.c
index 8e853181..6f0890e2 100644
--- a/src/base/wlc/wlc.c
+++ b/src/base/wlc/wlc.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "wlc.h"
+#include "sat/bsat/satStore.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -127,6 +128,143 @@ void Wlc_GenerateCodeMax4( int nBits )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_BlastFullAdderCtrlCnf( sat_solver * pSat, int a, int ac, int b, int c, int * pc, int * ps, int * piVars )
+{
+    int Cnf[12][6] = {            // xabc cs   // abc cs
+
+        { -1, 0, 0, 0,  0, 0 },   // -000 00   // 000 00
+        { -1, 0, 0, 1,  0, 1 },   // -001 01   // 001 01
+        { -1, 0, 1, 0,  0, 1 },   // -010 01   // 010 01
+        { -1, 0, 1, 1,  1, 0 },   // -011 10   // 011 10
+
+        {  0,-1, 0, 0,  0, 0 },   // 0-00 00
+        {  0,-1, 0, 1,  0, 1 },   // 0-01 01
+        {  0,-1, 1, 0,  0, 1 },   // 0-10 01
+        {  0,-1, 1, 1,  1, 0 },   // 0-11 10
+
+        {  1, 1, 0, 0,  0, 1 },   // 1100 01   // 100 01
+        {  1, 1, 0, 1,  1, 0 },   // 1101 10   // 101 10
+        {  1, 1, 1, 0,  1, 0 },   // 1110 10   // 110 10
+        {  1, 1, 1, 1,  1, 1 }    // 1111 11   // 111 11
+    };
+
+    int pVars[6] = {a, ac, b, c, *piVars, *piVars+1};
+    int i, v, nLits, pLits[6];
+    for ( i = 0; i < 12; i++ )
+    {
+        nLits = 0;
+        for ( v = 0; v < 6; v++ )
+        {
+            if ( Cnf[i][v] == -1 )
+                continue;
+            if ( pVars[v] == 0 ) // const 0
+            {
+                if ( Cnf[i][v] == 0 )
+                    continue;
+                if ( Cnf[i][v] == 1 )
+                    break;
+            }
+            if ( pVars[v] == -1 ) // const -1
+            {
+                if ( Cnf[i][v] == 0 )
+                    break;
+                if ( Cnf[i][v] == 1 )
+                    continue;
+            }
+            pLits[nLits++] = Abc_Var2Lit( pVars[v], Cnf[i][v] );
+        }
+        if ( v < 6 )
+            continue;
+        assert( nLits > 2 );
+        sat_solver_addclause( pSat, pLits, pLits + nLits );
+    }
+    *pc = (*piVars)++;
+    *ps = (*piVars)++;
+}
+void Wlc_BlastMultiplierCnf( sat_solver * pSat, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vTemp, Vec_Int_t * vRes, int * piVars )
+{
+    int * pRes, * pArgC, * pArgS, a, b, Carry = 0;
+    assert( nArgA > 0 && nArgB > 0 );
+    // prepare result
+    Vec_IntFill( vRes, nArgA + nArgB, 0 );
+    pRes = Vec_IntArray( vRes );
+    // prepare intermediate storage
+    Vec_IntFill( vTemp, 2 * nArgA, 0 );
+    pArgC = Vec_IntArray( vTemp );
+    pArgS = pArgC + nArgA;
+    // create matrix
+    for ( b = 0; b < nArgB; b++ )
+        for ( a = 0; a < nArgA; a++ )
+            Wlc_BlastFullAdderCtrlCnf( pSat, pArgA[a], pArgB[b], pArgS[a], pArgC[a], &pArgC[a], a ? &pArgS[a-1] : &pRes[b], piVars );
+    // final addition
+    pArgS[nArgA-1] = 0;
+    for ( a = 0; a < nArgA; a++ )
+        Wlc_BlastFullAdderCtrlCnf( pSat, -1, pArgC[a], pArgS[a], Carry, &Carry, &pRes[nArgB+a], piVars );
+}
+sat_solver * Wlc_BlastMultiplierCnfMain( int nBits )
+{
+    Vec_Int_t * vRes1 = Vec_IntAlloc( 2*nBits );
+    Vec_Int_t * vRes2 = Vec_IntAlloc( 2*nBits );
+    Vec_Int_t * vTemp = Vec_IntAlloc( 2*nBits );
+
+    int * pArgA = ABC_ALLOC( int, nBits );
+    int * pArgB = ABC_ALLOC( int, nBits );
+    int i, Ent1, Ent2, nVars = 1 + 2*nBits;
+    int nVarsAll = 1 + 4*nBits + 4*nBits*(nBits + 1);
+
+    sat_solver * pSat = sat_solver_new();
+    sat_solver_setnvars( pSat, nVarsAll );
+
+    for ( i = 0; i < nBits; i++ )
+        pArgA[i] = 1 + i, pArgB[i] = 1 + nBits + i;
+    Wlc_BlastMultiplierCnf( pSat, pArgA, pArgB, nBits, nBits, vTemp, vRes1, &nVars );
+
+    for ( i = 0; i < nBits; i++ )
+        pArgA[i] = 1 + nBits + i, pArgB[i] = 1 + i;
+    Wlc_BlastMultiplierCnf( pSat, pArgA, pArgB, nBits, nBits, vTemp, vRes2, &nVars );
+
+    Vec_IntClear( vTemp );
+    Vec_IntForEachEntryTwo( vRes1, vRes2, Ent1, Ent2, i )
+    {
+        Vec_IntPush( vTemp, Abc_Var2Lit(nVars, 0) );
+        sat_solver_add_xor( pSat, Ent1, Ent2, nVars++, 0 );
+    }
+    assert( nVars == nVarsAll );
+    sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+
+    ABC_FREE( pArgA );
+    ABC_FREE( pArgB );
+    Vec_IntFree( vRes1 );
+    Vec_IntFree( vRes2 );
+    Vec_IntFree( vTemp );
+    return pSat;
+}
+void Wlc_BlastMultiplierCnfTest( int nBits )
+{
+    abctime clk = Abc_Clock();
+    sat_solver * pSat = Wlc_BlastMultiplierCnfMain( nBits );
+    int i, status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
+    Sat_SolverWriteDimacs( pSat, "test_mult.cnf", NULL, NULL, 0 );
+    for ( i = 0; i < sat_solver_nvars(pSat); i++ )
+        printf( "%d=%d ", i, sat_solver_var_value(pSat, i) );
+    printf( "\n" );
+
+    printf( "Verifying for %d bits:  %s   ", nBits, status == l_True ? "SAT" : "UNSAT" );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    sat_solver_delete( pSat );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/mio/mio.c b/src/map/mio/mio.c
index 1f7ff612..8648a604 100644
--- a/src/map/mio/mio.c
+++ b/src/map/mio/mio.c
@@ -286,18 +286,14 @@ int Mio_CommandReadGenlib( Abc_Frame_t * pAbc, int argc, char **argv )
     Amap_Lib_t * pLib2;
     char * pFileName;
     char * pExcludeFile = NULL;
-    int fVerbose;
-    double WireDelay;
-    int c;
+    double WireDelay = 0.0;
+    int fShortNames = 0;
+    int c, fVerbose = 1;
 
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
-
-    // set the defaults
-    WireDelay   = 0.0;
-    fVerbose = 1;
     Extra_UtilGetoptReset();
-    while ( (c = Extra_UtilGetopt(argc, argv, "WEvh")) != EOF ) 
+    while ( (c = Extra_UtilGetopt(argc, argv, "WEnvh")) != EOF ) 
     {
         switch (c) 
         {
@@ -321,6 +317,9 @@ int Mio_CommandReadGenlib( Abc_Frame_t * pAbc, int argc, char **argv )
                 pExcludeFile = argv[globalUtilOptind];
                 globalUtilOptind++;
                 break;
+            case 'n':
+                fShortNames ^= 1;
+                break;
             case 'v':
                 fVerbose ^= 1;
                 break;
@@ -358,6 +357,10 @@ int Mio_CommandReadGenlib( Abc_Frame_t * pAbc, int argc, char **argv )
     if ( fVerbose )
         printf( "Entered genlib library with %d gates from file \"%s\".\n", Mio_LibraryReadGateNum(pLib), pFileName );
 
+    // convert the library if needed
+    if ( fShortNames )
+        Mio_LibraryShortNames( pLib );
+
     // add the fixed number (wire delay) to all delays in the library
     if ( WireDelay != 0.0 )
         Mio_LibraryShiftDelay( pLib, WireDelay );
@@ -376,13 +379,14 @@ int Mio_CommandReadGenlib( Abc_Frame_t * pAbc, int argc, char **argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: read_genlib [-W float] [-E filename] [-vh]\n");
+    fprintf( pErr, "usage: read_genlib [-W float] [-E filename] [-nvh]\n");
     fprintf( pErr, "\t           read the library from a genlib file\n" );  
     fprintf( pErr, "\t           (if the library contains more than one gate\n" );  
     fprintf( pErr, "\t           with the same Boolean function, only the gate\n" );  
     fprintf( pErr, "\t           with the smallest area will be used)\n" );  
     fprintf( pErr, "\t-W float : wire delay (added to pin-to-pin gate delays) [default = %g]\n", WireDelay );  
     fprintf( pErr, "\t-E file :  the file name with gates to be excluded [default = none]\n" );
+    fprintf( pErr, "\t-n       : toggle replacing gate/pin names by short strings [default = %s]\n", fShortNames? "yes": "no" );
     fprintf( pErr, "\t-v       : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h       : enable verbose output\n");
     return 1;       
diff --git a/src/map/mio/mio.h b/src/map/mio/mio.h
index 3f5df736..f45cce89 100644
--- a/src/map/mio/mio.h
+++ b/src/map/mio/mio.h
@@ -213,6 +213,11 @@ extern void              Mio_LibraryTransferProfile( Mio_Library_t * pLibDst, Mi
 extern void              Mio_LibraryTransferProfile2( Mio_Library_t * pLibDst, Mio_Library_t * pLibSrc );
 extern int               Mio_LibraryHasProfile( Mio_Library_t * pLib );
 extern void              Mio_LibraryCleanProfile2( Mio_Library_t * pLib );
+extern void              Mio_LibraryShortNames( Mio_Library_t * pLib );
+
+extern void              Mio_LibraryMatchesStop( Mio_Library_t * pLib );
+extern void              Mio_LibraryMatchesStart( Mio_Library_t * pLib, int fPinFilter, int fPinPerm, int fPinQuick );
+extern void              Mio_LibraryMatchesFetch( Mio_Library_t * pLib, Vec_Mem_t ** pvTtMem, Vec_Wec_t ** pvTt2Match, Mio_Cell2_t ** ppCells, int * pnCells, int fPinFilter, int fPinPerm, int fPinQuick );
 
 /*=== sclUtil.c =========================================================*/
 extern Mio_Library_t *   Abc_SclDeriveGenlibSimple( void * pScl );
diff --git a/src/map/mio/mioInt.h b/src/map/mio/mioInt.h
index 541a7a7f..23f48b2f 100644
--- a/src/map/mio/mioInt.h
+++ b/src/map/mio/mioInt.h
@@ -76,6 +76,14 @@ struct  Mio_LibraryStruct_t_
     st__table *         tName2Gate;  // the mapping of gate names into their pointer
     Mem_Flex_t *       pMmFlex;     // the memory manaqer for SOPs
     Vec_Str_t *        vCube;       // temporary cube
+    // matching
+    int                fPinFilter;  // pin filtering
+    int                fPinPerm;    // pin permutation
+    int                fPinQuick;   // pin permutation
+    Vec_Mem_t *        vTtMem;      // truth tables
+    Vec_Wec_t *        vTt2Match;   // matches for truth tables
+    Mio_Cell2_t *      pCells;      // library gates
+    int                nCells;      // library gate count
 }; 
 
 struct  Mio_GateStruct_t_
diff --git a/src/map/mio/mioUtils.c b/src/map/mio/mioUtils.c
index 101d5d0f..7572b27c 100644
--- a/src/map/mio/mioUtils.c
+++ b/src/map/mio/mioUtils.c
@@ -53,6 +53,7 @@ void Mio_LibraryDelete( Mio_Library_t * pLib )
     Mio_Gate_t * pGate, * pGate2;
     if ( pLib == NULL )
         return;
+    Mio_LibraryMatchesStop( pLib );
     // free the bindings of nodes to gates from this library for all networks
     Abc_FrameUnmapAllNetworks( Abc_FrameGetGlobalFrame() );
     // free the library
@@ -732,8 +733,13 @@ Mio_Cell2_t * Mio_CollectRootsNew2( Mio_Library_t * pLib, int nInputs, int * pnG
         assert( Mio_AreaCompare2( ppCells + 4, ppCells + iCell - 1 ) <= 0 );
     }
     // assign IDs
+    Mio_LibraryForEachGate( pLib, pGate0 )
+        Mio_GateSetCell( pGate0, -1 );
     for ( i = 0; i < iCell; i++ )
+    {
         ppCells[i].Id = ppCells[i].pName ? i : -1;
+        Mio_GateSetCell( (Mio_Gate_t *)ppCells[i].pMioGate, i );
+    }
 
     // report
     if ( fVerbose )
@@ -1465,6 +1471,177 @@ void Mio_LibraryCleanProfile2( Mio_Library_t * pLib )
         Mio_GateSetProfile2( pGate, 0 );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mio_LibraryHashGates( Mio_Library_t * pLib )
+{
+    Mio_Gate_t * pGate;    
+    Mio_LibraryForEachGate( pLib, pGate )
+        if ( pGate->pTwin )
+        {
+            printf( "Gates with multiple outputs are not supported.\n" );
+            return;
+        }
+    if ( pLib->tName2Gate )
+        st__free_table( pLib->tName2Gate );
+    pLib->tName2Gate = st__init_table(strcmp, st__strhash);
+    Mio_LibraryForEachGate( pLib, pGate )
+        st__insert( pLib->tName2Gate, pGate->pName, (char *)pGate );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_SclIsChar( char c )
+{
+    return (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z') || c == '_';
+}
+static inline int Abc_SclIsName( char c )
+{
+    return Abc_SclIsChar(c) || (c >= '0' && c <= '9');
+}
+static inline char * Abc_SclFindLimit( char * pName )
+{
+    assert( Abc_SclIsChar(*pName) );
+    while ( Abc_SclIsName(*pName) )
+        pName++;
+    return pName;
+}
+static inline int Abc_SclAreEqual( char * pBase, char * pName, char * pLimit )
+{
+    return !strncmp( pBase, pName, pLimit - pName );
+}
+void Mio_LibraryShortFormula( Mio_Gate_t * pCell, char * pForm, char * pBuffer )
+{
+    Mio_Pin_t * pPin; 
+    char * pTemp, * pLimit; int i;
+    if ( !strncmp(pForm, "CONST", 5) )
+    {
+        sprintf( pBuffer, "%s", pForm );
+        return;
+    }
+    for ( pTemp = pForm; *pTemp; )
+    {
+        if ( !Abc_SclIsChar(*pTemp) )
+        {
+            *pBuffer++ = *pTemp++;
+            continue;
+        }
+        pLimit = Abc_SclFindLimit( pTemp );
+        i = 0;
+        Mio_GateForEachPin( pCell, pPin )
+        {
+            if ( Abc_SclAreEqual( pPin->pName, pTemp, pLimit ) )
+            {
+                *pBuffer++ = 'a' + i;
+                break;
+            }
+            i++;
+        }
+        pTemp = pLimit;
+    }
+    *pBuffer++ = 0;
+}
+void Mio_LibraryShortNames( Mio_Library_t * pLib )
+{
+    char Buffer[10000];
+    Mio_Gate_t * pGate; Mio_Pin_t * pPin;
+    int c = 0, i, nDigits = Abc_Base10Log( Mio_LibraryReadGateNum(pLib) );
+    // itereate through classes
+    Mio_LibraryForEachGate( pLib, pGate )
+    {
+        ABC_FREE( pGate->pName );
+        sprintf( Buffer, "g%0*d", nDigits, ++c );
+        pGate->pName = Abc_UtilStrsav( Buffer );
+        // update formula
+        Mio_LibraryShortFormula( pGate, pGate->pForm, Buffer );
+        ABC_FREE( pGate->pForm );
+        pGate->pForm = Abc_UtilStrsav( Buffer );
+        // pin names
+        i = 0;
+        Mio_GateForEachPin( pGate, pPin )
+        {
+            ABC_FREE( pPin->pName );
+            sprintf( Buffer, "%c", 'a'+i );
+            pPin->pName = Abc_UtilStrsav( Buffer );
+            i++;
+        }
+        // output pin
+        ABC_FREE( pGate->pOutName );
+        sprintf( Buffer, "z" );
+        pGate->pOutName = Abc_UtilStrsav( Buffer );
+    }
+    Mio_LibraryHashGates( pLib );
+    // update library name
+    printf( "Renaming library \"%s\" into \"%s%d\".\n", pLib->pName, "lib", Mio_LibraryReadGateNum(pLib) );
+    ABC_FREE( pLib->pName );
+    sprintf( Buffer, "lib%d", Mio_LibraryReadGateNum(pLib) );
+    pLib->pName = Abc_UtilStrsav( Buffer );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mio_LibraryMatchesStop( Mio_Library_t * pLib )
+{
+    if ( !pLib->vTtMem )
+        return;
+    Vec_WecFree( pLib->vTt2Match );
+    Vec_MemHashFree( pLib->vTtMem );
+    Vec_MemFree( pLib->vTtMem );
+    ABC_FREE( pLib->pCells );
+}
+void Mio_LibraryMatchesStart( Mio_Library_t * pLib, int fPinFilter, int fPinPerm, int fPinQuick )
+{
+    extern Mio_Cell2_t * Nf_StoDeriveMatches( Vec_Mem_t * vTtMem, Vec_Wec_t * vTt2Match, int * pnCells, int fPinFilter, int fPinPerm, int fPinQuick );
+    if ( pLib->vTtMem && pLib->fPinFilter == fPinFilter && pLib->fPinPerm == fPinPerm && pLib->fPinQuick == fPinQuick )
+        return;
+    if ( pLib->vTtMem )
+        Mio_LibraryMatchesStop( pLib );
+    pLib->fPinFilter = fPinFilter;  // pin filtering
+    pLib->fPinPerm   = fPinPerm;    // pin permutation
+    pLib->fPinQuick  = fPinQuick;   // pin permutation
+    pLib->vTtMem     = Vec_MemAllocForTT( 6, 0 );          
+    pLib->vTt2Match  = Vec_WecAlloc( 1000 ); 
+    Vec_WecPushLevel( pLib->vTt2Match );
+    Vec_WecPushLevel( pLib->vTt2Match );
+    assert( Vec_WecSize(pLib->vTt2Match) == Vec_MemEntryNum(pLib->vTtMem) );
+    pLib->pCells = Nf_StoDeriveMatches( pLib->vTtMem, pLib->vTt2Match, &pLib->nCells, fPinFilter, fPinPerm, fPinQuick );
+}
+void Mio_LibraryMatchesFetch( Mio_Library_t * pLib, Vec_Mem_t ** pvTtMem, Vec_Wec_t ** pvTt2Match, Mio_Cell2_t ** ppCells, int * pnCells, int fPinFilter, int fPinPerm, int fPinQuick )
+{
+    Mio_LibraryMatchesStart( pLib, fPinFilter, fPinPerm, fPinQuick );
+    *pvTtMem    = pLib->vTtMem;     // truth tables
+    *pvTt2Match = pLib->vTt2Match;  // matches for truth tables
+    *ppCells    = pLib->pCells;     // library gates
+    *pnCells    = pLib->nCells;     // library gate count
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h
index ec3a70b8..839acdc3 100644
--- a/src/misc/vec/vec.h
+++ b/src/misc/vec/vec.h
@@ -36,6 +36,8 @@
 #include "vecAtt.h"
 #include "vecWrd.h"
 #include "vecBit.h"
+#include "vecMem.h"
+#include "vecWec.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
diff --git a/src/opt/fxch/module.make b/src/opt/fxch/module.make
index 48f36b13..630acb90 100644
--- a/src/opt/fxch/module.make
+++ b/src/opt/fxch/module.make
@@ -1,4 +1,4 @@
 SRC +=  src/opt/fxch/Fxch.c \
     src/opt/fxch/FxchDiv.c \
     src/opt/fxch/FxchMan.c  \
-    src/opt/fxch/FxchSCHashTable.c \
+    src/opt/fxch/FxchSCHashTable.c
diff --git a/src/opt/sfm/module.make b/src/opt/sfm/module.make
index fbdaa2ec..66518e4e 100644
--- a/src/opt/sfm/module.make
+++ b/src/opt/sfm/module.make
@@ -1,4 +1,5 @@
-SRC +=    src/opt/sfm/sfmCnf.c \
+SRC +=    src/opt/sfm/sfmArea.c \
+    src/opt/sfm/sfmCnf.c \
     src/opt/sfm/sfmCore.c \
     src/opt/sfm/sfmDec.c \
     src/opt/sfm/sfmLib.c \
diff --git a/src/opt/sfm/sfmArea.c b/src/opt/sfm/sfmArea.c
new file mode 100644
index 00000000..87f3b511
--- /dev/null
+++ b/src/opt/sfm/sfmArea.c
@@ -0,0 +1,380 @@
+/**CFile****************************************************************
+
+  FileName    [sfmArea.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based optimization using internal don't-cares.]
+
+  Synopsis    [Area optimization.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: sfmArea.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sfmInt.h"
+#include "map/mio/mio.h"
+#include "misc/util/utilTruth.h"
+#include "misc/util/utilNam.h"
+#include "map/scl/sclLib.h"
+#include "map/scl/sclCon.h"
+#include "opt/dau/dau.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Precompute cell parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkPrecomputeCellPairs( Mio_Cell2_t * pCells, int nCells )
+{
+    Vec_Int_t * vInfo = Vec_IntAlloc( 1000 );
+    word iBestArea, tCur, iThis;
+    int * pPerm[7], nPerms[7], Perm[7], * Perm1, * Perm2;
+    int iBestCell, iBestPerm, iBestDiff;
+    int i, k, n, v, p, Count = 0;
+    int iGate1 = -1, iGate2 = -1;
+
+    for ( i = 1; i <= 6; i++ )
+        pPerm[i] = Extra_PermSchedule( i );
+    for ( i = 1; i <= 6; i++ )
+        nPerms[i] = Extra_Factorial( i );
+
+    for ( i = 2; i < nCells; i++ )
+    {
+        int nFanins = pCells[i].nFanins;
+        for ( n = 0; n <= nFanins; n++ )
+        {
+            // get the truth table
+            iThis = (n == nFanins) ? ~pCells[i].uTruth : Abc_Tt6Flip(pCells[i].uTruth, n);
+            // init the comparison
+            iBestArea = ~((word)0);
+            iBestCell = iBestPerm = iBestDiff = -1;
+            // iterate through cells
+            for ( k = 2; k < nCells; k++ )
+            {
+                if ( nFanins != (int)pCells[k].nFanins )
+                    continue;
+                if ( i != k && pCells[i].uTruth == pCells[k].uTruth )
+                {
+                    iGate1 = i;
+                    iGate2 = k;
+                    Count++;
+                    continue;
+                }
+                // set unit permutation
+                for ( v = 0; v < nFanins; v++ )
+                    Perm[v] = v;
+                // go through all permutation of Cell[k]
+                tCur = pCells[k].uTruth;
+                for ( p = 0; p < nPerms[nFanins]; p++ )
+                {
+                    if ( iThis == tCur && iBestArea > pCells[k].AreaW ) 
+                    {
+                        iBestArea = pCells[k].AreaW;
+                        iBestCell = k;
+                        iBestPerm = 0;
+                        for ( v = 0; v < nFanins; v++ )
+                            iBestPerm |= (v << (Perm[v] << 2));
+                        iBestDiff = (pCells[i].AreaW >= pCells[k].AreaW) ? (int)(pCells[i].AreaW - pCells[k].AreaW) : -(int)(pCells[k].AreaW - pCells[i].AreaW);
+                    }
+                    if ( nPerms[nFanins] == 1 )
+                        continue;
+                    // update
+                    tCur  = Abc_Tt6SwapAdjacent( tCur, pPerm[nFanins][p] );
+                    Perm1 = Perm + pPerm[nFanins][p];
+                    Perm2 = Perm1 + 1;
+                    ABC_SWAP( int, *Perm1, *Perm2 );
+                }
+                assert( tCur == pCells[k].uTruth );
+            }
+            Vec_IntPushThree( vInfo, iBestCell, iBestPerm, iBestDiff );
+        }
+    }
+
+    for ( i = 1; i <= 6; i++ )
+        ABC_FREE( pPerm[i] );
+    if ( Count )
+        printf( "In this library, %d cell pairs have equal functions (for example, %s and %s).\n", Count/2, pCells[iGate1].pName, pCells[iGate2].pName );
+    return vInfo;
+}
+Vec_Int_t * Abc_NtkPrecomputeFirsts( Mio_Cell2_t * pCells, int nCells )
+{
+    int i, Index = 0;
+    Vec_Int_t * vFirst = Vec_IntStartFull( 2 ); 
+    for ( i = 2; i < nCells; i++ )
+    {
+        Vec_IntPush( vFirst, Index );
+        Index += 3 * (pCells[i].nFanins + 1);
+    }
+    assert( nCells == Vec_IntSize(vFirst) );
+    return vFirst;
+}
+int Abc_NtkPrecomputePrint( Mio_Cell2_t * pCells, int nCells, Vec_Int_t * vInfo )
+{
+    int i, n, v, Index = 0, nRecUsed = 0;
+    for ( i = 2; i < nCells; i++ )
+    {
+        int nFanins = pCells[i].nFanins;
+        printf( "%3d : %8s   Fanins = %d   ", i, pCells[i].pName, nFanins );
+        Dau_DsdPrintFromTruth( &pCells[i].uTruth, nFanins );
+        for ( n = 0; n <= nFanins; n++, Index += 3 )
+        {
+            int iCellA = Vec_IntEntry( vInfo, Index+0 );
+            int iPerm  = Vec_IntEntry( vInfo, Index+1 );
+            int Diff   = Vec_IntEntry( vInfo, Index+2 );
+            if ( iCellA == -1 )
+                continue;
+            printf( "%d : {", n );
+            for ( v = 0; v < nFanins; v++ )
+                printf( " %d ", (iPerm >> (v << 2)) & 15 );
+            printf( "}  Index = %d  ", Index );
+
+            printf( "Gain = %6.2f  ", Scl_Int2Flt(Diff) );
+            Dau_DsdPrintFromTruth( &pCells[iCellA].uTruth, pCells[iCellA].nFanins );
+            nRecUsed++;
+        }
+    }
+    return nRecUsed;
+}
+
+void Abc_NtkPrecomputeCellPairsTest()
+{
+    int nCells;
+    Mio_Cell2_t * pCells = Mio_CollectRootsNewDefault2( 6, &nCells, 0 );
+    Vec_Int_t * vInfo = Abc_NtkPrecomputeCellPairs( pCells, nCells );
+    int nRecUsed = Abc_NtkPrecomputePrint( pCells, nCells, vInfo );
+    // iterate through the cells
+    Vec_Int_t * vFirst = Abc_NtkPrecomputeFirsts( pCells, nCells );
+    printf( "Used records = %d.  All records = %d.\n", nRecUsed, Vec_IntSize(vInfo)/3 - nRecUsed );
+    assert( nCells == Vec_IntSize(vFirst) );
+    Vec_IntFree( vFirst );
+    Vec_IntFree( vInfo );
+    ABC_FREE( pCells );
+}
+
+int Abc_NodeCheckFanoutHasFanin( Abc_Obj_t * pNode, Abc_Obj_t * pFanin )
+{
+    Abc_Obj_t * pThis;
+    int i;
+    Abc_ObjForEachFanout( pNode, pThis, i )
+        if ( Abc_NodeFindFanin(pThis, pFanin) >= 0 )
+            return i;
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluate changes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjHasDupFanins( Abc_Obj_t * pObj )
+{
+    int * pArray = pObj->vFanins.pArray;
+    int i, k, Limit = Abc_ObjFaninNum(pObj);
+    for ( i = 0; i < Limit; i++ )
+        for ( k = i+1; k < Limit; k++ )
+            if ( pArray[i] == pArray[k] )
+                return 1;
+    return 0;
+}
+int Abc_ObjHasDupFanouts( Abc_Obj_t * pObj )
+{
+    int * pArray = pObj->vFanouts.pArray;
+    int i, k, Limit = Abc_ObjFanoutNum(pObj);
+    for ( i = 0; i < Limit; i++ )
+        for ( k = i+1; k < Limit; k++ )
+            if ( pArray[i] == pArray[k] )
+                return 1;
+    return 0;
+}
+int Abc_ObjChangeEval( Abc_Obj_t * pObj, Vec_Int_t * vInfo, Vec_Int_t * vFirst, int InvArea, int * pfUseInv )
+{
+    Abc_Obj_t * pNext;
+    Mio_Gate_t * pGate = (Mio_Gate_t *)pObj->pData;
+    int iFanCell, iNodeCell = Mio_GateReadCell( (Mio_Gate_t *)pObj->pData );
+    int * pFanInfo, * pNodeInfo = Vec_IntEntryP( vInfo, Vec_IntEntry(vFirst, iNodeCell) );
+    int i, fNeedInv = 0, Gain = 0, iFanin = Abc_ObjFaninNum(pObj), fUseInv = Abc_NodeIsInv(pObj);
+    assert( iFanin > 0 );
+    *pfUseInv = 0;
+    if ( pNodeInfo[3*iFanin] == -1 )
+        return 0;
+    if ( fUseInv )
+        Gain = InvArea;
+    else
+        Gain = pNodeInfo[3*iFanin+2];
+    Abc_ObjForEachFanout( pObj, pNext, i )
+    {
+        if ( fUseInv && Abc_NodeFindFanin(pNext, Abc_ObjFanin0(pObj)) >= 0 )
+            return 0;
+        if ( Abc_ObjHasDupFanins(pNext) )
+            return 0;
+        if ( !Abc_ObjIsNode(pNext) || Abc_NodeIsBuf(pNext) )
+        {
+            fNeedInv = 1;
+            continue;
+        }
+        if ( Abc_NodeIsInv(pNext) )
+        {
+            if ( Abc_NodeCheckFanoutHasFanin(pNext, pObj) >= 0 )
+                return 0;
+            Gain += InvArea;
+            continue;
+        }
+        iFanCell = Mio_GateReadCell( (Mio_Gate_t *)pNext->pData );
+        pFanInfo = Vec_IntEntryP( vInfo, Vec_IntEntry(vFirst, iFanCell) );
+        iFanin   = Abc_NodeFindFanin( pNext, pObj );
+        if ( pFanInfo[3*iFanin] == -1 )
+        {
+            fNeedInv = 1;
+            continue;
+        }
+        Gain += pFanInfo[3*iFanin+2];
+    }
+    if ( fNeedInv )
+        Gain -= InvArea;
+    *pfUseInv = fNeedInv;
+    return Gain;
+}
+void Abc_ObjChangeUpdate( Abc_Obj_t * pObj, int iFanin, Mio_Cell2_t * pCells, int * pNodeInfo, Vec_Int_t * vTemp )
+{
+    int v, Perm, iNodeCell = pNodeInfo[3*iFanin];
+    Mio_Gate_t * pGate = (Mio_Gate_t *)pObj->pData;
+    //Abc_ObjPrint( stdout, pObj );
+    //printf( "Replacing fanout %d with %s by %s with fanin %d.\n", Abc_ObjId(pObj), Mio_GateReadName(pGate), Mio_GateReadName((Mio_Gate_t *)pCells[iNodeCell].pMioGate), iFanin );
+    pObj->pData = (Mio_Gate_t *)pCells[iNodeCell].pMioGate;
+    Perm = pNodeInfo[3*iFanin+1];
+    Vec_IntClear( vTemp );
+    for ( v = 0; v < Abc_ObjFaninNum(pObj); v++ )
+        Vec_IntPush( vTemp, Abc_ObjFaninId(pObj, (Perm >> (v << 2)) & 15) );
+    Vec_IntClear( &pObj->vFanins );
+    Vec_IntAppend( &pObj->vFanins, vTemp );
+}
+void Abc_ObjChangePerform( Abc_Obj_t * pObj, Vec_Int_t * vInfo, Vec_Int_t * vFirst, int fUseInv, Vec_Int_t * vTemp, Vec_Ptr_t * vFanout, Vec_Ptr_t * vFanout2, Mio_Cell2_t * pCells )
+{
+    Abc_Obj_t * pNext, * pNext2, * pNodeInv = NULL;
+    int iFanCell, iNodeCell = Mio_GateReadCell( (Mio_Gate_t *)pObj->pData );
+    int * pFanInfo, * pNodeInfo = Vec_IntEntryP( vInfo, Vec_IntEntry(vFirst, iNodeCell) );
+    int i, k, iFanin = Abc_ObjFaninNum(pObj);
+    assert( iFanin > 0 && pNodeInfo[3*iFanin] != -1 );
+    // update the node
+    Abc_NodeCollectFanouts( pObj, vFanout );
+    if ( Abc_NodeIsInv(pObj) )
+    {
+        Abc_Obj_t * pFanin = Abc_ObjFanin0(pObj);
+        Vec_PtrForEachEntry( Abc_Obj_t *, vFanout, pNext, k )
+            Abc_ObjPatchFanin( pNext, pObj, pFanin );
+        assert( Abc_ObjFanoutNum(pObj) == 0 );
+        Abc_NtkDeleteObj(pObj);
+        pObj = pFanin;
+        assert( fUseInv == 0 );
+    }
+    else
+        Abc_ObjChangeUpdate( pObj, iFanin, pCells, pNodeInfo, vTemp );
+    // add inverter if needed
+    if ( fUseInv )
+        pNodeInv = Abc_NtkCreateNodeInv(pObj->pNtk, pObj);
+    // update the fanouts
+    Vec_PtrForEachEntry( Abc_Obj_t *, vFanout, pNext, i )
+    {
+        if ( !Abc_ObjIsNode(pNext) || Abc_NodeIsBuf(pNext) )
+        {
+            Abc_ObjPatchFanin( pNext, pObj, pNodeInv );
+            continue;
+        }
+        if ( Abc_NodeIsInv(pNext) )
+        {
+            Abc_NodeCollectFanouts( pNext, vFanout2 );
+            Vec_PtrForEachEntry( Abc_Obj_t *, vFanout2, pNext2, k )
+                Abc_ObjPatchFanin( pNext2, pNext, pObj );
+            assert( Abc_ObjFanoutNum(pNext) == 0 );
+            Abc_NtkDeleteObj(pNext);
+            continue;
+        }
+        iFanin   = Abc_NodeFindFanin( pNext, pObj );
+        iFanCell = Mio_GateReadCell( (Mio_Gate_t *)pNext->pData );
+        pFanInfo = Vec_IntEntryP( vInfo, Vec_IntEntry(vFirst, iFanCell) );
+        if ( pFanInfo[3*iFanin] == -1 )
+        {
+            Abc_ObjPatchFanin( pNext, pObj, pNodeInv );
+            continue;
+        }
+        Abc_ObjChangeUpdate( pNext, iFanin, pCells, pFanInfo, vTemp );
+    }
+}
+void Abc_NtkChangePerform( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    abctime clk = Abc_Clock();
+    int i, fNeedInv, nCells, Gain, GainAll = 0, Count = 0, CountInv = 0;
+    Mio_Cell2_t * pCells = Mio_CollectRootsNewDefault2( 6, &nCells, 0 );
+    Vec_Int_t * vInfo = Abc_NtkPrecomputeCellPairs( pCells, nCells );
+    Vec_Int_t * vFirst = Abc_NtkPrecomputeFirsts( pCells, nCells );
+
+    Vec_Ptr_t * vFanout = Vec_PtrAlloc( 100 );
+    Vec_Ptr_t * vFanout2 = Vec_PtrAlloc( 100 );
+    Vec_Int_t * vTemp = Vec_IntAlloc( 100 );
+    Abc_Obj_t * pObj;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( Abc_ObjFaninNum(pObj) < 2 && !Abc_NodeIsInv(pObj) )
+            continue;
+        if ( Abc_ObjHasDupFanouts(pObj) )
+            continue;
+        Gain = Abc_ObjChangeEval( pObj, vInfo, vFirst, (int)pCells[3].AreaW, &fNeedInv );
+        if ( Gain <= 0 )
+            continue;
+        //printf( "Obj %d\n", Abc_ObjId(pObj) );
+        Count++;
+        CountInv += Abc_NodeIsInv(pObj);
+        GainAll += Gain;
+        Abc_ObjChangePerform( pObj, vInfo, vFirst, fNeedInv, vTemp, vFanout, vFanout2, pCells );
+    }
+    Vec_PtrFree( vFanout2 );
+    Vec_PtrFree( vFanout );
+    Vec_IntFree( vTemp );
+
+    Vec_IntFree( vFirst );
+    Vec_IntFree( vInfo );
+    ABC_FREE( pCells );
+
+    if ( fVerbose )
+        printf( "Total gain in area = %6.2f after %d changes (including %d inverters). ", Scl_Int2Flt(GainAll), Count, CountInv );
+    if ( fVerbose )
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/sfm/sfmDec.c b/src/opt/sfm/sfmDec.c
index bce20624..c5af0ac0 100644
--- a/src/opt/sfm/sfmDec.c
+++ b/src/opt/sfm/sfmDec.c
@@ -2152,6 +2152,11 @@ void Abc_NtkPerformMfs3( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
     if ( pPars->fLibVerbose )
         Sfm_LibPrint( p->pLib );
     Sfm_DecStop( p );
+    if ( pPars->fArea )
+    {
+        extern void Abc_NtkChangePerform( Abc_Ntk_t * pNtk, int fVerbose );
+        Abc_NtkChangePerform( pNtk, pPars->fVerbose );
+    }
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/bmc/bmcGen.c b/src/sat/bmc/bmcGen.c
new file mode 100644
index 00000000..74af1b78
--- /dev/null
+++ b/src/sat/bmc/bmcGen.c
@@ -0,0 +1,195 @@
+/**CFile****************************************************************
+
+  FileName    [bmcGen.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based bounded model checking.]
+
+  Synopsis    [Generating satisfying assignments.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bmcGen.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bmc.h"
+#include "sat/cnf/cnf.h"
+#include "sat/bsat/satStore.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline word * Gia_ManMoObj( Gia_Man_t * p, int iObj )
+{
+    return Vec_WrdEntryP( p->vSims, iObj * p->iPatsPi );
+}
+static inline void Gia_ManMoSetCi( Gia_Man_t * p, int iObj )
+{
+    int w;
+    word * pSims = Gia_ManMoObj( p, iObj );
+    for ( w = 0; w < p->iPatsPi; w++ )
+        pSims[w] = Gia_ManRandomW( 0 );
+}
+static inline void Gia_ManMoSimAnd( Gia_Man_t * p, int iObj )
+{
+    int w;
+    Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+    word * pSims  = Gia_ManMoObj( p, iObj );
+    word * pSims0 = Gia_ManMoObj( p, Gia_ObjFaninId0(pObj, iObj) );
+    word * pSims1 = Gia_ManMoObj( p, Gia_ObjFaninId1(pObj, iObj) );
+    if ( Gia_ObjFaninC0(pObj) )
+    {
+        if (  Gia_ObjFaninC1(pObj) )
+            for ( w = 0; w < p->iPatsPi; w++ )
+                pSims[w] = ~(pSims0[w] | pSims1[w]);
+        else 
+            for ( w = 0; w < p->iPatsPi; w++ )
+                pSims[w] = ~pSims0[w] & pSims1[w];
+    }
+    else 
+    {
+        if (  Gia_ObjFaninC1(pObj) )
+            for ( w = 0; w < p->iPatsPi; w++ )
+                pSims[w] = pSims0[w] & ~pSims1[w];
+        else 
+            for ( w = 0; w < p->iPatsPi; w++ )
+                pSims[w] = pSims0[w] & pSims1[w];
+    }
+}
+static inline void Gia_ManMoSetCo( Gia_Man_t * p, int iObj )
+{
+    int w;
+    Gia_Obj_t * pObj  = Gia_ManObj( p, iObj );
+    word * pSims  = Gia_ManMoObj( p, iObj );
+    word * pSims0 = Gia_ManMoObj( p, Gia_ObjFaninId0(pObj, iObj) );
+    if ( Gia_ObjFaninC0(pObj) )
+    {
+        for ( w = 0; w < p->iPatsPi; w++ )
+            pSims[w] = ~pSims0[w];
+    }
+    else 
+    {
+        for ( w = 0; w < p->iPatsPi; w++ )
+            pSims[w] = pSims0[w];
+    }
+}
+void Gia_ManMoFindSimulate( Gia_Man_t * p, int nWords )
+{
+    int i, iObj;
+    Gia_ManRandomW( 1 );
+    p->iPatsPi = nWords;
+    if ( p->vSims )
+        Vec_WrdFill( p->vSims, nWords * Gia_ManObjNum(p), 0 );
+    else
+        p->vSims = Vec_WrdStart( nWords * Gia_ManObjNum(p) );
+    Gia_ManForEachCiId( p, iObj, i )
+        Gia_ManMoSetCi( p, iObj );
+    Gia_ManForEachAndId( p, iObj )
+        Gia_ManMoSimAnd( p, iObj );
+    Gia_ManForEachCoId( p, iObj, i )
+        Gia_ManMoSetCo( p, iObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManTestSatEnum( Gia_Man_t * p )
+{
+    abctime clk = Abc_Clock(), clk2, clkTotal = 0;
+    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+    sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
+    int i, v, status, iLit, nWords = 1, iOutVar = 1, Count = 0;
+    Vec_Int_t * vVars = Vec_IntAlloc( 1000 );
+    word * pSimInfo;
+
+    // add literals to the solver
+    iLit  = Abc_Var2Lit( iOutVar, 0 ); 
+    status = sat_solver_addclause( pSat, &iLit, &iLit + 1 );
+    assert( status );
+
+    // simulate the AIG
+    Gia_ManMoFindSimulate( p, nWords );
+
+    // print outputs
+    pSimInfo = Gia_ManMoObj( p, Gia_ObjId(p, Gia_ManCo(p, 0)) );
+    for ( i = 0; i < 64*nWords; i++ )
+        printf( "%d", Abc_InfoHasBit( (unsigned *)pSimInfo, i ) );
+    printf( "\n" );
+
+    // iterate through the assignments
+    for ( i = 0; i < 64*nWords; i++ )
+    {
+        Vec_IntClear( vVars );
+        for ( v = 0; v < Gia_ManObjNum(p); v++ )
+        {
+            if ( pCnf->pVarNums[v] == -1 )
+                continue;
+            pSimInfo = Gia_ManMoObj( p, v );
+            if ( !Abc_InfoHasBit( (unsigned *)pSimInfo, i ) )
+                continue;
+            Vec_IntPush( vVars, pCnf->pVarNums[v] );
+        }
+        //sat_solver_act_var_clear( pSat );
+        //sat_solver_set_polarity( pSat, Vec_IntArray(vVars), Vec_IntSize(vVars) );
+
+        clk2 = Abc_Clock();
+        status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
+        clkTotal += Abc_Clock() - clk2;
+        printf( "%c", status == l_True ? '+' : '-' );
+        if ( status == l_True )
+            Count++;
+    }
+    printf( "\n" );
+    printf( "Finished generating %d assignments.  ", Count );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    Abc_PrintTime( 1, "SAT solver time", clkTotal );
+
+    Vec_WrdFreeP( &p->vSims );
+    Vec_IntFree( vVars );
+    sat_solver_delete( pSat );
+    Cnf_DataFree( pCnf );
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
index e1777df8..40402bf3 100644
--- a/src/sat/bmc/module.make
+++ b/src/sat/bmc/module.make
@@ -16,6 +16,7 @@ SRC +=    src/sat/bmc/bmcBCore.c \
     src/sat/bmc/bmcExpand.c \
     src/sat/bmc/bmcFault.c \
     src/sat/bmc/bmcFx.c \
+    src/sat/bmc/bmcGen.c \
     src/sat/bmc/bmcICheck.c \
     src/sat/bmc/bmcInse.c \
     src/sat/bmc/bmcLoad.c \