New technology mapper.

7 files changed, 295 insertions, 134 deletions

diff --git a/src/map/mpm/mpm.h b/src/map/mpm/mpm.h
index a8a600f4..0f5bdcd6 100644
--- a/src/map/mpm/mpm.h
+++ b/src/map/mpm/mpm.h
@@ -56,7 +56,12 @@ struct Mpm_LibLut_t_
 typedef struct Mpm_Par_t_ Mpm_Par_t;
 struct Mpm_Par_t_
 {
+    Mpm_LibLut_t *   pLib;
+    int              nNumCuts;
     int              DelayTarget;
+    int              fUseTruth;
+    int              fCutMin;
+    int              fDeriveLuts;
     int              fVerbose;
 };
 
@@ -71,6 +76,9 @@ struct Mpm_Par_t_
 
 /*=== mpmCore.c ===========================================================*/
 extern void           Mpm_ManSetParsDefault( Mpm_Par_t * p );
+/*=== mpmLib.c ===========================================================*/
+extern Mpm_LibLut_t * Mpm_LibLutSetSimple( int nLutSize );
+extern void           Mpm_LibLutFree( Mpm_LibLut_t * pLib );
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/map/mpm/mpmAbc.c b/src/map/mpm/mpmAbc.c
index 939d7782..9ec439b0 100644
--- a/src/map/mpm/mpmAbc.c
+++ b/src/map/mpm/mpmAbc.c
@@ -20,6 +20,7 @@
 
 #include "aig/gia/gia.h"
 #include "mpmInt.h"
+#include "misc/util/utilTruth.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -182,16 +183,29 @@ void * Mpm_ManFromIfLogic( Mpm_Man_t * pMan )
             pCutBest = Mpm_ObjCutBestP( pMan, pObj );
             Mpm_CutForEachLeaf( pMan->pMig, pCutBest, pFanin, k )
                 Vec_IntPush( vLeaves, Mig_ObjCopy(pFanin) );
-            // perform one of the two types of mapping: with and without structures
-            iLitNew = Mpm_ManNodeIfToGia( pNew, pMan, pObj, vLeaves, 0 );
-            // write mapping
-            Vec_IntSetEntry( vMapping, Abc_Lit2Var(iLitNew), Vec_IntSize(vMapping2) );
-            Vec_IntPush( vMapping2, Vec_IntSize(vLeaves) );
-            Vec_IntForEachEntry( vLeaves, Entry, k )
-                assert( Abc_Lit2Var(Entry) < Abc_Lit2Var(iLitNew) );
-            Vec_IntForEachEntry( vLeaves, Entry, k )
-                Vec_IntPush( vMapping2, Abc_Lit2Var(Entry)  );
-            Vec_IntPush( vMapping2, Abc_Lit2Var(iLitNew) );
+            if ( pMan->pPars->fDeriveLuts && pMan->pPars->fUseTruth )
+            {
+                extern int Gia_ManFromIfLogicNode( Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_Int_t * vLeavesTemp, 
+                    word * pRes, char * pStr, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking );
+                word * pTruth = Mpm_CutTruth(pMan, Abc_Lit2Var(pCutBest->iFunc));
+//                Kit_DsdPrintFromTruth( pTruth, Vec_IntSize(vLeaves) );  printf( "\n" );
+                // perform decomposition of the cut
+                iLitNew = Gia_ManFromIfLogicNode( pNew, Mig_ObjId(pObj), vLeaves, vLeaves2, pTruth, NULL, vCover, vMapping, vMapping2, vPacking );
+                iLitNew = Abc_LitNotCond( iLitNew, pCutBest->fCompl ^ Abc_LitIsCompl(pCutBest->iFunc) );
+            }
+            else
+            {
+                // perform one of the two types of mapping: with and without structures
+                iLitNew = Mpm_ManNodeIfToGia( pNew, pMan, pObj, vLeaves, 0 );
+                // write mapping
+                Vec_IntSetEntry( vMapping, Abc_Lit2Var(iLitNew), Vec_IntSize(vMapping2) );
+                Vec_IntPush( vMapping2, Vec_IntSize(vLeaves) );
+                Vec_IntForEachEntry( vLeaves, Entry, k )
+                    assert( Abc_Lit2Var(Entry) < Abc_Lit2Var(iLitNew) );
+                Vec_IntForEachEntry( vLeaves, Entry, k )
+                    Vec_IntPush( vMapping2, Abc_Lit2Var(Entry)  );
+                Vec_IntPush( vMapping2, Abc_Lit2Var(iLitNew) );
+            }
         }
         else if ( Mig_ObjIsCi(pObj) )
             iLitNew = Gia_ManAppendCi(pNew);
diff --git a/src/map/mpm/mpmCore.c b/src/map/mpm/mpmCore.c
index 605e716c..caebd835 100644
--- a/src/map/mpm/mpmCore.c
+++ b/src/map/mpm/mpmCore.c
@@ -46,8 +46,13 @@ ABC_NAMESPACE_IMPL_START
 void Mpm_ManSetParsDefault( Mpm_Par_t * p )
 {
     memset( p, 0, sizeof(Mpm_Par_t) );
-    p->DelayTarget    =      -1;  // delay target
-    p->fVerbose       =       0;  // verbose output
+    p->pLib           =   NULL;  // LUT library
+    p->nNumCuts       =      8;  // cut number
+    p->fUseTruth      =      0;  // uses truth tables
+    p->fCutMin        =      0;  // enables cut minimization
+    p->DelayTarget    =     -1;  // delay target
+    p->fDeriveLuts    =      0;  // use truth tables to derive AIG structure
+    p->fVerbose       =      0;  // verbose output
 }
 
 /**Function*************************************************************
@@ -61,20 +66,17 @@ void Mpm_ManSetParsDefault( Mpm_Par_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Mpm_ManPerformTest( Mig_Man_t * pMig )
+Gia_Man_t * Mpm_ManPerformTest( Mig_Man_t * pMig, Mpm_Par_t * pPars )
 {
     Gia_Man_t * pNew;
-    Mpm_LibLut_t * pLib;
     Mpm_Man_t * p;
-    pLib = Mpm_LibLutSetSimple( 6 );
-    p = Mpm_ManStart( pMig, pLib, 8 );
+    p = Mpm_ManStart( pMig, pPars );
     Mpm_ManPrintStatsInit( p );
     Mpm_ManPrepare( p );
     Mpm_ManPerform( p );
     Mpm_ManPrintStats( p );
     pNew = (Gia_Man_t *)Mpm_ManFromIfLogic( p );
     Mpm_ManStop( p );
-    Mpm_LibLutFree( pLib );
     return pNew;
 }
 Gia_Man_t * Mpm_ManMappingTest( Gia_Man_t * pGia, Mpm_Par_t * pPars )
@@ -82,7 +84,7 @@ Gia_Man_t * Mpm_ManMappingTest( Gia_Man_t * pGia, Mpm_Par_t * pPars )
     Mig_Man_t * p;
     Gia_Man_t * pNew;
     p = Mig_ManCreate( pGia );
-    pNew = Mpm_ManPerformTest( p );
+    pNew = Mpm_ManPerformTest( p, pPars );
     Mig_ManStop( p );
     return pNew;
 }
diff --git a/src/map/mpm/mpmInt.h b/src/map/mpm/mpmInt.h
index bb235833..307d5d26 100644
--- a/src/map/mpm/mpmInt.h
+++ b/src/map/mpm/mpmInt.h
@@ -33,6 +33,7 @@
 
 //#include "misc/tim/tim.h"
 #include "misc/vec/vec.h"
+#include "misc/vec/vecMem.h"
 #include "misc/mem/mem2.h"
 #include "mpmMig.h"
 #include "mpm.h"
@@ -58,30 +59,23 @@ typedef struct Mpm_Cut_t_ Mpm_Cut_t;  // 8 bytes + NLeaves * 4 bytes
 struct Mpm_Cut_t_
 {
     int              hNext;                    // next cut
-    unsigned         iFunc     : 26;           // function
+    unsigned         iFunc     : 25;           // function
+    unsigned         fCompl    :  1;
     unsigned         fUseless  :  1;           // internal flag
     unsigned         nLeaves   :  5;           // leaves
     int              pLeaves[0];               // leaves
 };
-
-typedef struct Mpm_Inf_t_ Mpm_Inf_t;  // 32 bytes
-struct Mpm_Inf_t_
-{
-    int              hCut;                     // cut handle
-    unsigned         nLeaves   :  6;           // the number of leaves
-    unsigned         mCost     : 26;           // area cost of this cut
+typedef struct Mpm_Uni_t_ Mpm_Uni_t;  // 48 bytes
+struct Mpm_Uni_t_
+{ 
     int              mTime;                    // arrival time
     int              mArea;                    // area (flow)
     int              mEdge;                    // edge (flow)
     int              mAveRefs;                 // area references
     word             uSign;                    // cut signature
-};
-
-typedef struct Mpm_Uni_t_ Mpm_Uni_t;  // 48 bytes
-struct Mpm_Uni_t_
-{
-    Mpm_Inf_t        Inf;                      // information
-    unsigned         iFunc     : 26;           // function
+    int              Cost;                     // user cost
+    unsigned         iFunc     : 25;           // function
+    unsigned         fCompl    :  1;
     unsigned         fUseless  :  1;           // internal flag
     unsigned         nLeaves   :  5;           // leaves
     int              pLeaves[MPM_VAR_MAX];     // leaves
@@ -91,9 +85,11 @@ typedef struct Mpm_Man_t_ Mpm_Man_t;
 struct Mpm_Man_t_
 {
     Mig_Man_t *      pMig;                     // AIG manager
+    Mpm_Par_t *      pPars;                    // mapping parameters
     // mapping parameters
     int              nLutSize;                 // LUT size
     int              nNumCuts;                 // cut count
+    int              nTruWords;                // words in the truth table
     Mpm_LibLut_t *   pLibLut;                  // LUT library
     // mapping attributes  
     int              GloRequired;              // global arrival time
@@ -110,10 +106,13 @@ struct Mpm_Man_t_
     Vec_Ptr_t *      vTemp;                    // storage for cuts
     // object presence
     unsigned char *  pObjPres;                 // object presence
+    int              pObjPresUsed[MPM_VAR_MAX];
+    int              nObjPresUsed;
+
     Mpm_Cut_t *      pCutTemp;                 // temporary cut
     Vec_Str_t        vObjShared;               // object presence
     // cut comparison
-    int (* pCutCmp) (Mpm_Inf_t *, Mpm_Inf_t *);// procedure to compare cuts
+    int (* pCutCmp) (Mpm_Uni_t *, Mpm_Uni_t *);// procedure to compare cuts
     // fanin cuts/signatures
     int              nCuts[3];                 // fanin cut counts
     Mpm_Cut_t *      pCuts[3][MPM_CUT_MAX+1];  // fanin cuts
@@ -122,6 +121,10 @@ struct Mpm_Man_t_
 //    Dsd_Man_t *      pManDsd;
     void *           pManDsd;
     int              pPerm[MPM_VAR_MAX]; 
+    Vec_Mem_t *      vTtMem;                   // truth table memory and hash table
+    int              funcCst0;                 // constant 0
+    int              funcVar0;                 // variable 0
+    unsigned         uPermMask[3];
     // mapping attributes
     Vec_Int_t        vCutBests;                // cut best
     Vec_Int_t        vCutLists;                // cut list
@@ -134,6 +137,7 @@ struct Mpm_Man_t_
     Vec_Int_t        vEdges;                   // edge
     // statistics
     int              nCutsMerged;
+    int              nSmallSupp;
     abctime          timeFanin;
     abctime          timeDerive;
     abctime          timeMerge;
@@ -151,7 +155,7 @@ struct Mpm_Man_t_
 static inline int         Mpm_ObjCutBest( Mpm_Man_t * p, Mig_Obj_t * pObj )              { return Vec_IntEntry(&p->vCutBests, Mig_ObjId(pObj));            }
 static inline void        Mpm_ObjSetCutBest( Mpm_Man_t * p, Mig_Obj_t * pObj, int i )    { Vec_IntWriteEntry(&p->vCutBests, Mig_ObjId(pObj), i);           }
 
-static inline int         Mpm_CutWordNum( int nLeaves )                                  { return (sizeof(Mpm_Cut_t)/sizeof(int) + nLeaves + 1) >> 1;      }
+static inline int         Mpm_CutWordNum( int nLeaves )                                  { return ((sizeof(Mpm_Cut_t)/sizeof(int) + nLeaves + 1) >> 1);    }
 static inline Mpm_Cut_t * Mpm_CutFetch( Mpm_Man_t * p, int h )                           { Mpm_Cut_t * pCut = (Mpm_Cut_t *)Mmr_StepEntry( p->pManCuts, h );  assert( Mpm_CutWordNum(pCut->nLeaves) == (h & p->pManCuts->uMask) ); return pCut; }
 static inline Mpm_Cut_t * Mpm_ObjCutBestP( Mpm_Man_t * p, Mig_Obj_t * pObj )             { return Mpm_CutFetch( p, Mpm_ObjCutBest(p, pObj) );              }
 
@@ -159,6 +163,9 @@ static inline int         Mpm_ObjCutList( Mpm_Man_t * p, Mig_Obj_t * pObj )
 static inline int *       Mpm_ObjCutListP( Mpm_Man_t * p, Mig_Obj_t * pObj )             { return Vec_IntEntryP(&p->vCutLists, Mig_ObjId(pObj));           }
 static inline void        Mpm_ObjSetCutList( Mpm_Man_t * p, Mig_Obj_t * pObj, int i )    { Vec_IntWriteEntry(&p->vCutLists, Mig_ObjId(pObj), i);           }
 
+static inline int         Mpm_CutLeafNum( Mpm_Cut_t * pCut )                             { return pCut->nLeaves;                                           }
+static inline word *      Mpm_CutTruth( Mpm_Man_t * p, int iFunc )                       { return Vec_MemReadEntry(p->vTtMem, iFunc);                      }
+
 static inline void        Mpm_ManSetMigRefs( Mpm_Man_t * p )                             { assert( Vec_IntSize(&p->vMigRefs) == Vec_IntSize(&p->pMig->vRefs) ); memcpy( Vec_IntArray(&p->vMigRefs), Vec_IntArray(&p->pMig->vRefs), sizeof(int) * Mig_ManObjNum(p->pMig) ); }
 static inline int         Mig_ObjMigRefNum( Mpm_Man_t * p, Mig_Obj_t * pObj )            { return Vec_IntEntry(&p->vMigRefs, Mig_ObjId(pObj));             }
 static inline int         Mig_ObjMigRefDec( Mpm_Man_t * p, Mig_Obj_t * pObj )            { return Vec_IntAddToEntry(&p->vMigRefs, Mig_ObjId(pObj), -1);    }
@@ -183,6 +190,9 @@ static inline void        Mpm_ObjSetArea( Mpm_Man_t * p, Mig_Obj_t * pObj, int i
 static inline int         Mpm_ObjEdge( Mpm_Man_t * p, Mig_Obj_t * pObj )                 { return Vec_IntEntry(&p->vEdges, Mig_ObjId(pObj));               }
 static inline void        Mpm_ObjSetEdge( Mpm_Man_t * p, Mig_Obj_t * pObj, int i )       { Vec_IntWriteEntry(&p->vEdges, Mig_ObjId(pObj), i);              }
 
+static inline void        Mpm_VarsClear( int * V2P, int * P2V, int nVars )               { int i; for ( i = 0; i < nVars; i++ ) V2P[i] = P2V[i] = i;       }
+static inline void        Mpm_VarsSwap( int * V2P, int * P2V, int iVar, int jVar )       { V2P[P2V[iVar]] = jVar; V2P[P2V[jVar]] = iVar; P2V[iVar] ^= P2V[jVar]; P2V[jVar] ^= P2V[iVar]; P2V[iVar] ^= P2V[jVar];  }
+
 // iterators over object cuts
 #define Mpm_ObjForEachCut( p, pObj, hCut, pCut )                         \
     for ( hCut = Mpm_ObjCutList(p, pObj); hCut && (pCut = Mpm_CutFetch(p, hCut)); hCut = pCut->hNext )
@@ -203,7 +213,7 @@ static inline void        Mpm_ObjSetEdge( Mpm_Man_t * p, Mig_Obj_t * pObj, int i
 extern Mig_Man_t *           Mig_ManCreate( void * pGia );
 extern void *                Mpm_ManFromIfLogic( Mpm_Man_t * pMan );
 /*=== mpmCore.c ===========================================================*/
-extern Mpm_Man_t *           Mpm_ManStart( Mig_Man_t * pMig, Mpm_LibLut_t * pLib, int nNumCuts );
+extern Mpm_Man_t *           Mpm_ManStart( Mig_Man_t * pMig, Mpm_Par_t * pPars );
 extern void                  Mpm_ManStop( Mpm_Man_t * p );
 extern void                  Mpm_ManPrintStatsInit( Mpm_Man_t * p );
 extern void                  Mpm_ManPrintStats( Mpm_Man_t * p );
@@ -214,6 +224,9 @@ extern void                  Mpm_LibLutFree( Mpm_LibLut_t * pLib );
 /*=== mpmMap.c ===========================================================*/
 extern void                  Mpm_ManPrepare( Mpm_Man_t * p );
 extern void                  Mpm_ManPerform( Mpm_Man_t * p );
+/*=== mpmTruth.c ===========================================================*/
+extern int                   Mpm_CutComputeTruth6( Mpm_Man_t * p, Mpm_Cut_t * pCut, Mpm_Cut_t * pCut0, Mpm_Cut_t * pCut1, Mpm_Cut_t * pCutC, int fCompl0, int fCompl1, int fComplC, int Type );
+
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/map/mpm/mpmMap.c b/src/map/mpm/mpmMap.c
index a876de2c..12421b77 100644
--- a/src/map/mpm/mpmMap.c
+++ b/src/map/mpm/mpmMap.c
@@ -106,6 +106,7 @@ static inline int Mpm_CutAlloc( Mpm_Man_t * p, int nLeaves, Mpm_Cut_t ** ppCut )
     (*ppCut)->nLeaves  = nLeaves;
     (*ppCut)->hNext    = 0;
     (*ppCut)->fUseless = 0;
+    (*ppCut)->fCompl   = 0;
     return hHandle;
 }
 static inline int Mpm_CutCreateZero( Mpm_Man_t * p )  
@@ -119,16 +120,18 @@ static inline int Mpm_CutCreateUnit( Mpm_Man_t * p, int Id )
 { 
     Mpm_Cut_t * pCut;
     int hCut = Mpm_CutAlloc( p, 1, &pCut );
-    pCut->iFunc      = 2; // var
+    pCut->iFunc      = Abc_Var2Lit( p->funcVar0, 0 ); // var
     pCut->pLeaves[0] = Abc_Var2Lit( Id, 0 );
     return hCut;
 }
-static inline int Mpm_CutCreate( Mpm_Man_t * p, int * pLeaves, int nLeaves, int fUseless, Mpm_Cut_t ** ppCut )  
+static inline int Mpm_CutCreate( Mpm_Man_t * p, Mpm_Uni_t * pUni, Mpm_Cut_t ** ppCut )  
 { 
-    int hCutNew = Mpm_CutAlloc( p, nLeaves, ppCut );
-    (*ppCut)->fUseless = fUseless;
-    (*ppCut)->nLeaves  = nLeaves;
-    memcpy( (*ppCut)->pLeaves, pLeaves, sizeof(int) * nLeaves );
+    int hCutNew = Mpm_CutAlloc( p, pUni->nLeaves, ppCut );
+    (*ppCut)->iFunc    = pUni->iFunc;
+    (*ppCut)->fCompl   = pUni->fCompl;
+    (*ppCut)->fUseless = pUni->fUseless;
+    (*ppCut)->nLeaves  = pUni->nLeaves;
+    memcpy( (*ppCut)->pLeaves, pUni->pLeaves, sizeof(int) * pUni->nLeaves );
     return hCutNew;
 }
 static inline int Mpm_CutDup( Mpm_Man_t * p, Mpm_Cut_t * pCut, int fCompl )  
@@ -196,23 +199,25 @@ static inline void Mpm_CutPrintAll( Mpm_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Mpm_Man_t * Mpm_ManStart( Mig_Man_t * pMig, Mpm_LibLut_t * pLib, int nNumCuts )
+Mpm_Man_t * Mpm_ManStart( Mig_Man_t * pMig, Mpm_Par_t * pPars )
 {
     Mpm_Man_t * p;
-    assert( sizeof(Mpm_Inf_t) % sizeof(word) == 0 );      // aligned info to word boundary
-    assert( Mpm_CutWordNum(32) < 32 ); // using 5 bits for word count
-    assert( nNumCuts <= MPM_CUT_MAX );
+    assert( sizeof(Mpm_Uni_t) % sizeof(word) == 0 );      // aligned info to word boundary
+    assert( pPars->nNumCuts <= MPM_CUT_MAX );
     Mig_ManSetRefs( pMig, 1 );
     // alloc
     p = ABC_CALLOC( Mpm_Man_t, 1 );
     p->pMig      = pMig;
-    p->pLibLut   = pLib;
-    p->nLutSize  = pLib->LutMax;
-    p->nNumCuts  = nNumCuts;
+    p->pPars     = pPars;
+    p->pLibLut   = pPars->pLib;
+    p->nLutSize  = pPars->pLib->LutMax;
+    p->nTruWords = pPars->fUseTruth ? Abc_TtWordNum(p->nLutSize) : 0;
+    p->nNumCuts  = pPars->nNumCuts;
     p->timeTotal = Abc_Clock();
     // cuts
+    assert( Mpm_CutWordNum(32) < 32 ); // using 5 bits for word count
     p->pManCuts  = Mmr_StepStart( 13, Abc_Base2Log(Mpm_CutWordNum(p->nLutSize) + 1) );
-    Vec_IntGrow( &p->vFreeUnits, nNumCuts + 1 );
+    Vec_IntGrow( &p->vFreeUnits, p->nNumCuts + 1 );
     p->pObjPres  = ABC_FALLOC( unsigned char, Mig_ManObjNum(pMig) );
     p->pCutTemp  = (Mpm_Cut_t *)ABC_CALLOC( word, Mpm_CutWordNum(p->nLutSize) );
     Vec_StrGrow( &p->vObjShared, 32 );
@@ -230,10 +235,26 @@ Mpm_Man_t * Mpm_ManStart( Mig_Man_t * pMig, Mpm_LibLut_t * pLib, int nNumCuts )
     // start DSD manager
     p->pManDsd   = NULL;
     pMig->pMan   = p;
+    if ( p->pPars->fUseTruth )
+    {
+        word Truth = 0;
+        p->vTtMem = Vec_MemAlloc( p->nTruWords, 12 ); // 32 KB/page for 6-var functions
+        Vec_MemHashAlloc( p->vTtMem, 10000 );
+        p->funcCst0 = Vec_MemHashInsert( p->vTtMem, &Truth );
+        Truth = ABC_CONST(0xAAAAAAAAAAAAAAAA);
+        p->funcVar0 = Vec_MemHashInsert( p->vTtMem, &Truth );
+    }
+    else 
+        p->funcVar0 = 1;
     return p;
 }
 void Mpm_ManStop( Mpm_Man_t * p )
 {
+    if ( p->vTtMem ) 
+    {
+        Vec_MemHashFree( p->vTtMem );
+        Vec_MemFree( p->vTtMem );
+    }
     Vec_PtrFree( p->vTemp );
     Mmr_StepStop( p->pManCuts );
     ABC_FREE( p->vFreeUnits.pArray );
@@ -254,8 +275,10 @@ void Mpm_ManStop( Mpm_Man_t * p )
 }
 void Mpm_ManPrintStatsInit( Mpm_Man_t * p )
 {
-    printf( "K = %d.  C = %d.  Cands = %d.  Choices = %d.\n", 
-        p->nLutSize, p->nNumCuts, Mig_ManCiNum(p->pMig) + Mig_ManNodeNum(p->pMig), 0 );
+    printf( "K = %d.  C = %d.  Cands = %d. Choices = %d.   CutMin = %d. Truth = %d.\n", 
+        p->nLutSize, p->nNumCuts, 
+        Mig_ManCiNum(p->pMig) + Mig_ManNodeNum(p->pMig), 0, 
+        p->pPars->fCutMin, p->pPars->fUseTruth );
 }
 void Mpm_ManPrintStats( Mpm_Man_t * p )
 {
@@ -298,43 +321,6 @@ void Mpm_ManPrintStats( Mpm_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Mig_ManObjPresClean( Mpm_Man_t * p )                
-{ 
-    int i; 
-    for ( i = 0; i < (int)p->pCutTemp->nLeaves; i++ )
-        p->pObjPres[Abc_Lit2Var(p->pCutTemp->pLeaves[i])] = (unsigned char)0xFF; 
-//    for ( i = 0; i < Mig_ManObjNum(p->pMig); i++ )
-//        assert( p->pObjPres[i] == (unsigned char)0xFF );
-    Vec_StrClear(&p->vObjShared);                      
-}
-static inline int Mig_ManObjPres( Mpm_Man_t * p, int k, int iLit ) 
-{ 
-    int iObj = Abc_Lit2Var(iLit);
-//    assert( iLit > 1 && iLit < 2 * Mig_ManObjNum(p->pMig) );
-    if ( p->pObjPres[iObj] != (unsigned char)0xFF )
-        return 1;
-    if ( (int)p->pCutTemp->nLeaves == p->nLutSize )
-        return 0;
-    p->pObjPres[iObj] = p->pCutTemp->nLeaves;        
-    p->pCutTemp->pLeaves[p->pCutTemp->nLeaves++] = iLit;
-    return 1;
-}
-static inline int Mpm_ObjDeriveCut( Mpm_Man_t * p, Mpm_Cut_t ** pCuts, Mpm_Cut_t * pCut )
-{
-    int i, c;
-    pCut->nLeaves = 0;
-    for ( c = 0; pCuts[c] && c < 3; c++ )
-        for ( i = 0; i < (int)pCuts[c]->nLeaves; i++ )
-            if ( !Mig_ManObjPres( p, i, pCuts[c]->pLeaves[i] ) )
-                return 0;
-    pCut->hNext    = 0;
-    pCut->iFunc    = 0;  pCut->iFunc = ~pCut->iFunc;
-    pCut->fUseless = 0;
-    assert( pCut->nLeaves > 0 );
-    p->nCutsMerged++;
-    return 1;
-}
-
 static inline int Mpm_ManSetIsSmaller( Mpm_Man_t * p, int * pLits, int nLits ) // check if pCut is contained in the current one (p->pCutTemp)
 {
     int i, Index;
@@ -399,7 +385,7 @@ static inline int Mpm_CutGetArrTime( Mpm_Man_t * p, Mpm_Cut_t * pCut )
         ArrTime = Abc_MaxInt( ArrTime, pmTimes[iLeaf] + pDelays[i] );
     return ArrTime;
 }
-static inline void Mpm_CutSetupInfo( Mpm_Man_t * p, Mpm_Cut_t * pCut, int ArrTime, Mpm_Inf_t * pInfo )  
+static inline Mpm_Uni_t * Mpm_CutSetupInfo( Mpm_Man_t * p, Mpm_Cut_t * pCut, int ArrTime )  
 {
     int * pMigRefs = Vec_IntArray( &p->vMigRefs );
     int * pMapRefs = Vec_IntArray( &p->vMapRefs );
@@ -407,28 +393,37 @@ static inline void Mpm_CutSetupInfo( Mpm_Man_t * p, Mpm_Cut_t * pCut, int ArrTim
     int * pmArea   = Vec_IntArray( &p->vAreas );
     int * pmEdge   = Vec_IntArray( &p->vEdges );
     int i, iLeaf;
-    memset( pInfo, 0, sizeof(Mpm_Inf_t) );
-    pInfo->nLeaves = pCut->nLeaves;
-    pInfo->mTime   = ArrTime;
-    pInfo->mArea   = p->pLibLut->pLutAreas[pCut->nLeaves];
-    pInfo->mEdge   = MPM_UNIT_EDGE * pCut->nLeaves;
+
+    Mpm_Uni_t * pUnit = p->pCutUnits + Vec_IntPop(&p->vFreeUnits);
+    memset( pUnit, 0, sizeof(Mpm_Uni_t) );
+
+    pUnit->iFunc   = pCut->iFunc;
+    pUnit->fCompl  = pCut->fCompl;
+    pUnit->fUseless= pCut->fUseless;
+    pUnit->nLeaves = pCut->nLeaves;
+    memcpy( pUnit->pLeaves, pCut->pLeaves, sizeof(int) * pCut->nLeaves );
+
+    pUnit->mTime   = ArrTime;
+    pUnit->mArea   = p->pLibLut->pLutAreas[pCut->nLeaves];
+    pUnit->mEdge   = MPM_UNIT_EDGE * pCut->nLeaves;
     Mpm_CutForEachLeafId( pCut, iLeaf, i )
     {
         if ( p->fMainRun && pMapRefs[iLeaf] == 0 ) // not used in the mapping
         {
-            pInfo->mArea += pmArea[iLeaf];
-            pInfo->mEdge += pmEdge[iLeaf];
+            pUnit->mArea += pmArea[iLeaf];
+            pUnit->mEdge += pmEdge[iLeaf];
         }
         else
         {
             assert( pEstRefs[iLeaf] > 0 );
-            pInfo->mArea += MPM_UNIT_REFS * pmArea[iLeaf] / pEstRefs[iLeaf];
-            pInfo->mEdge += MPM_UNIT_REFS * pmEdge[iLeaf] / pEstRefs[iLeaf];
-            pInfo->mAveRefs += p->fMainRun ? pMapRefs[iLeaf] : pMigRefs[iLeaf];
+            pUnit->mArea += MPM_UNIT_REFS * pmArea[iLeaf] / pEstRefs[iLeaf];
+            pUnit->mEdge += MPM_UNIT_REFS * pmEdge[iLeaf] / pEstRefs[iLeaf];
+            pUnit->mAveRefs += p->fMainRun ? pMapRefs[iLeaf] : pMigRefs[iLeaf];
         }
-        pInfo->uSign |= ((word)1 << (iLeaf & 0x3F));
+        pUnit->uSign |= ((word)1 << (iLeaf & 0x3F));
     }
-    pInfo->mAveRefs = pInfo->mAveRefs * MPM_UNIT_EDGE / pCut->nLeaves;
+    pUnit->mAveRefs = pUnit->mAveRefs * MPM_UNIT_EDGE / pCut->nLeaves;
+    return pUnit;
 }
 
 /**Function*************************************************************
@@ -442,15 +437,6 @@ static inline void Mpm_CutSetupInfo( Mpm_Man_t * p, Mpm_Cut_t * pCut, int ArrTim
   SeeAlso     []
 
 ***********************************************************************/
-static inline Mpm_Uni_t * Mpm_CutToUnit( Mpm_Man_t * p, Mpm_Cut_t * pCut )  
-{
-    Mpm_Uni_t * pUnit = p->pCutUnits + Vec_IntPop(&p->vFreeUnits);
-    pUnit->iFunc    = pCut->iFunc;
-    pUnit->fUseless = pCut->fUseless;
-    pUnit->nLeaves  = pCut->nLeaves;
-    memcpy( pUnit->pLeaves, pCut->pLeaves, sizeof(int) * pCut->nLeaves );
-    return pUnit;
-}
 static inline void Mpm_UnitRecycle( Mpm_Man_t * p, Mpm_Uni_t * pUnit )  
 {
     Vec_IntPush( &p->vFreeUnits, pUnit - p->pCutUnits );
@@ -475,8 +461,7 @@ int Mpm_ObjAddCutToStore( Mpm_Man_t * p, Mpm_Cut_t * pCut, int ArrTime )
     abctime clk;
 clk = Abc_Clock();
 #endif
-    pUnitNew = Mpm_CutToUnit( p, pCut );
-    Mpm_CutSetupInfo( p, pCut, ArrTime, &pUnitNew->Inf );
+    pUnitNew = Mpm_CutSetupInfo( p, pCut, ArrTime );
 #ifdef MIG_RUNTIME
 p->timeEval += Abc_Clock() - clk;
 #endif
@@ -487,7 +472,7 @@ p->timeEval += Abc_Clock() - clk;
         return 1;
     }
     // special case when the cut store is full and last cut is better than new cut
-    if ( p->nCutStore == p->nNumCuts-1 && p->pCutCmp(&pUnitNew->Inf, &p->pCutStore[p->nCutStore-1]->Inf) > 0 )
+    if ( p->nCutStore == p->nNumCuts-1 && p->pCutCmp(pUnitNew, p->pCutStore[p->nCutStore-1]) > 0 )
     {
         Mpm_UnitRecycle( p, pUnitNew );
         return 0;
@@ -495,7 +480,7 @@ p->timeEval += Abc_Clock() - clk;
     // find place of the given cut in the store
     assert( p->nCutStore <= p->nNumCuts );
     for ( iPivot = p->nCutStore - 1; iPivot >= 0; iPivot-- )
-        if ( p->pCutCmp(&pUnitNew->Inf, &p->pCutStore[iPivot]->Inf) > 0 ) // iPivot-th cut is better than new cut
+        if ( p->pCutCmp(pUnitNew, p->pCutStore[iPivot]) > 0 ) // iPivot-th cut is better than new cut
             break;
 
     if ( fEnableContainment )
@@ -507,8 +492,8 @@ clk = Abc_Clock();
     for ( k = 0; k <= iPivot; k++ )
     {
         pUnit = p->pCutStore[k];
-        if ( pUnitNew->Inf.nLeaves >= pUnit->Inf.nLeaves && 
-            (pUnitNew->Inf.uSign & pUnit->Inf.uSign) == pUnit->Inf.uSign && 
+        if ( pUnitNew->nLeaves >= pUnit->nLeaves && 
+            (pUnitNew->uSign & pUnit->uSign) == pUnit->uSign && 
              Mpm_ManSetIsSmaller(p, pUnit->pLeaves, pUnit->nLeaves) )
         {
 //            printf( "\n" );
@@ -538,8 +523,8 @@ p->timeCompare += Abc_Clock() - clk;
     for ( k = last = iPivot+1; k < p->nCutStore; k++ )
     {
         pUnit = p->pCutStore[k];
-        if ( pUnitNew->Inf.nLeaves <= pUnit->Inf.nLeaves && 
-            (pUnitNew->Inf.uSign & pUnit->Inf.uSign) == pUnitNew->Inf.uSign && 
+        if ( pUnitNew->nLeaves <= pUnit->nLeaves && 
+            (pUnitNew->uSign & pUnit->uSign) == pUnitNew->uSign && 
              Mpm_ManSetIsBigger(p, pUnit->pLeaves, pUnit->nLeaves) )
         {
 //            printf( "\n" );
@@ -591,7 +576,7 @@ void Mpm_ObjTranslateCutsFromStore( Mpm_Man_t * p, Mig_Obj_t * pObj, int fAddUni
     for ( i = 0; i < p->nCutStore; i++ )
     {
         pUnit  = p->pCutStore[i];
-        *pList = Mpm_CutCreate( p, pUnit->pLeaves, pUnit->nLeaves, pUnit->fUseless, &pCut );
+        *pList = Mpm_CutCreate( p, pUnit, &pCut );
         pList  = &pCut->hNext;
         Mpm_UnitRecycle( p, pUnit );
     }
@@ -669,7 +654,43 @@ static inline void Mpm_ObjPrepareFanins( Mpm_Man_t * p, Mig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Mpm_ManDeriveCutNew( Mpm_Man_t * p, Mpm_Cut_t ** pCuts, int Required )
+static inline int Mpm_ObjDeriveCut( Mpm_Man_t * p, Mpm_Cut_t ** pCuts, Mpm_Cut_t * pCut )
+{
+    int i, c, iObj;
+    // clean present objects
+    for ( i = 0; i < p->nObjPresUsed; i++ )
+        p->pObjPres[p->pObjPresUsed[i]] = (unsigned char)0xFF; 
+    p->nObjPresUsed = 0;
+    Vec_StrClear(&p->vObjShared);   
+    // check present objects
+//    for ( i = 0; i < Mig_ManObjNum(p->pMig); i++ )
+//        assert( p->pObjPres[i] == (unsigned char)0xFF );
+    // collect cuts    
+    pCut->nLeaves = 0;
+    for ( c = 0; pCuts[c] && c < 3; c++ )
+    {
+        for ( i = 0; i < (int)pCuts[c]->nLeaves; i++ )
+        {
+            iObj = Abc_Lit2Var(pCuts[c]->pLeaves[i]);
+            if ( p->pObjPres[iObj] != (unsigned char)0xFF )
+                continue;
+            if ( (int)pCut->nLeaves == p->nLutSize )
+                return 0;
+            p->pObjPresUsed[p->nObjPresUsed++] = iObj;
+            p->pObjPres[iObj] = pCut->nLeaves;        
+            pCut->pLeaves[pCut->nLeaves++] = pCuts[c]->pLeaves[i];
+        }
+    }
+    pCut->hNext    = 0;
+    pCut->iFunc    = 0;  pCut->iFunc = ~pCut->iFunc;
+    pCut->fUseless = 0;
+    assert( pCut->nLeaves > 0 );
+    p->nCutsMerged++;
+    Vec_IntSelectSort( pCut->pLeaves, pCut->nLeaves );
+    return 1;
+}
+
+static inline int Mpm_ManDeriveCutNew( Mpm_Man_t * p, Mig_Obj_t * pObj, Mpm_Cut_t ** pCuts, int Required )
 {
 //    int fUseFunc = 0;
     Mpm_Cut_t * pCut = p->pCutTemp;
@@ -678,7 +699,6 @@ static inline int Mpm_ManDeriveCutNew( Mpm_Man_t * p, Mpm_Cut_t ** pCuts, int Re
 abctime clk = clock();
 #endif
 
-    Mig_ManObjPresClean( p );
     if ( !Mpm_ObjDeriveCut( p, pCuts, pCut ) )
     {
 #ifdef MIG_RUNTIME
@@ -686,6 +706,7 @@ p->timeMerge += clock() - clk;
 #endif
         return 1;
     }
+
 #ifdef MIG_RUNTIME
 p->timeMerge += clock() - clk;
 clk = clock();
@@ -697,6 +718,11 @@ p->timeEval += clock() - clk;
 
     if ( p->fMainRun && ArrTime > Required )
         return 1;
+
+    // derive truth table
+    if ( p->pPars->fUseTruth )
+        Mpm_CutComputeTruth6( p, pCut, pCuts[0], pCuts[1], pCuts[2], Mig_ObjFaninC0(pObj), Mig_ObjFaninC1(pObj), Mig_ObjFaninC2(pObj), Mig_ObjNodeType(pObj) ); 
+
 #ifdef MIG_RUNTIME
 clk = Abc_Clock();
 #endif
@@ -704,6 +730,7 @@ clk = Abc_Clock();
 #ifdef MIG_RUNTIME
 p->timeStore += Abc_Clock() - clk;
 #endif
+
     return 1;
     // return 0 if const or buffer cut is derived - reset all cuts to contain only one
 }
@@ -753,7 +780,7 @@ clk = Abc_Clock();
         for ( c0 = 0; c0 < p->nCuts[0] && (pCuts[0] = p->pCuts[0][c0]); c0++ )
         for ( c1 = 0; c1 < p->nCuts[1] && (pCuts[1] = p->pCuts[1][c1]); c1++ )
             if ( Abc_TtCountOnes(p->pSigns[0][c0] | p->pSigns[1][c1]) <= p->nLutSize )
-                if ( !Mpm_ManDeriveCutNew( p, pCuts, Required ) )
+                if ( !Mpm_ManDeriveCutNew( p, pObj, pCuts, Required ) )
                     goto finish;
     }
     else if ( Mig_ObjIsNode3(pObj) )
@@ -763,7 +790,7 @@ clk = Abc_Clock();
         for ( c1 = 0; c1 < p->nCuts[1] && (pCuts[1] = p->pCuts[1][c1]); c1++ )
         for ( c2 = 0; c2 < p->nCuts[2] && (pCuts[2] = p->pCuts[2][c2]); c2++ )
             if ( Abc_TtCountOnes(p->pSigns[0][c0] | p->pSigns[1][c1] | p->pSigns[2][c2]) <= p->nLutSize )
-                if ( !Mpm_ManDeriveCutNew( p, pCuts, Required ) )
+                if ( !Mpm_ManDeriveCutNew( p, pObj, pCuts, Required ) )
                     goto finish;
     }
     else assert( 0 );
@@ -777,16 +804,16 @@ finish:
 //    printf( "%d ", p->nCutStore );
     // save best cut
     assert( p->nCutStore > 0 );
-    if ( p->pCutStore[0]->Inf.mTime <= Required )
+    if ( p->pCutStore[0]->mTime <= Required )
     {
         Mpm_Cut_t * pCut;
         if ( hCutBest )
             Mmr_StepRecycle( p->pManCuts, hCutBest );
-        hCutBest = Mpm_CutCreate( p, p->pCutStore[0]->pLeaves, p->pCutStore[0]->nLeaves, p->pCutStore[0]->fUseless, &pCut );
+        hCutBest = Mpm_CutCreate( p, p->pCutStore[0], &pCut );
         Mpm_ObjSetCutBest( p, pObj, hCutBest );
-        Mpm_ObjSetTime( p, pObj, p->pCutStore[0]->Inf.mTime );
-        Mpm_ObjSetArea( p, pObj, p->pCutStore[0]->Inf.mArea );
-        Mpm_ObjSetEdge( p, pObj, p->pCutStore[0]->Inf.mEdge );
+        Mpm_ObjSetTime( p, pObj, p->pCutStore[0]->mTime );
+        Mpm_ObjSetArea( p, pObj, p->pCutStore[0]->mArea );
+        Mpm_ObjSetEdge( p, pObj, p->pCutStore[0]->mEdge );
     }
     else assert( !p->fMainRun );
     assert( hCutBest > 0 );
@@ -883,7 +910,7 @@ static inline void Mpm_ManComputeEstRefs( Mpm_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Mpm_CutCompareDelay( Mpm_Inf_t * pOld, Mpm_Inf_t * pNew )
+int Mpm_CutCompareDelay( Mpm_Uni_t * pOld, Mpm_Uni_t * pNew )
 {
     if ( pOld->mTime    != pNew->mTime    ) return pOld->mTime    - pNew->mTime;
     if ( pOld->nLeaves  != pNew->nLeaves  ) return pOld->nLeaves  - pNew->nLeaves;
@@ -891,7 +918,7 @@ int Mpm_CutCompareDelay( Mpm_Inf_t * pOld, Mpm_Inf_t * pNew )
     if ( pOld->mEdge    != pNew->mEdge    ) return pOld->mEdge    - pNew->mEdge;
     return 0;
 }
-int Mpm_CutCompareDelay2( Mpm_Inf_t * pOld, Mpm_Inf_t * pNew )
+int Mpm_CutCompareDelay2( Mpm_Uni_t * pOld, Mpm_Uni_t * pNew )
 {
     if ( pOld->mTime    != pNew->mTime    ) return pOld->mTime    - pNew->mTime;
     if ( pOld->mArea    != pNew->mArea    ) return pOld->mArea    - pNew->mArea;
@@ -899,7 +926,7 @@ int Mpm_CutCompareDelay2( Mpm_Inf_t * pOld, Mpm_Inf_t * pNew )
     if ( pOld->nLeaves  != pNew->nLeaves  ) return pOld->nLeaves  - pNew->nLeaves;
     return 0;
 }
-int Mpm_CutCompareArea( Mpm_Inf_t * pOld, Mpm_Inf_t * pNew )
+int Mpm_CutCompareArea( Mpm_Uni_t * pOld, Mpm_Uni_t * pNew )
 {
     if ( pOld->mArea    != pNew->mArea    ) return pOld->mArea    - pNew->mArea;
     if ( pOld->nLeaves  != pNew->nLeaves  ) return pOld->nLeaves  - pNew->nLeaves;
@@ -908,7 +935,7 @@ int Mpm_CutCompareArea( Mpm_Inf_t * pOld, Mpm_Inf_t * pNew )
     if ( pOld->mTime    != pNew->mTime    ) return pOld->mTime    - pNew->mTime;
     return 0;
 }
-int Mpm_CutCompareArea2( Mpm_Inf_t * pOld, Mpm_Inf_t * pNew )
+int Mpm_CutCompareArea2( Mpm_Uni_t * pOld, Mpm_Uni_t * pNew )
 {
     if ( pOld->mArea    != pNew->mArea    ) return pOld->mArea    - pNew->mArea;
     if ( pOld->mEdge    != pNew->mEdge    ) return pOld->mEdge    - pNew->mEdge;
diff --git a/src/map/mpm/mpmMig.h b/src/map/mpm/mpmMig.h
index 71b0f3ac..7968e38b 100644
--- a/src/map/mpm/mpmMig.h
+++ b/src/map/mpm/mpmMig.h
@@ -140,6 +140,7 @@ static inline int          Mig_ObjIsAnd( Mig_Obj_t * p )                       {
 static inline int          Mig_ObjIsXor( Mig_Obj_t * p )                       { return Mig_ObjIsNode2( p ) && Mig_FanId(p, 0) > Mig_FanId(p, 1); } 
 static inline int          Mig_ObjIsMux( Mig_Obj_t * p )                       { return Mig_ObjIsNode3( p );                                } 
 static inline int          Mig_ObjIsCand( Mig_Obj_t * p )                      { return Mig_ObjIsNode(p) || Mig_ObjIsCi(p);                 } 
+static inline int          Mig_ObjNodeType( Mig_Obj_t * p )                    { return Mig_ObjIsAnd(p) ? 1 : (Mig_ObjIsXor(p) ? 2 : 3);    } 
 
 static inline int          Mig_ObjId( Mig_Obj_t * p )                          { return Mig_FanId( p, 3 );                                  }
 static inline void         Mig_ObjSetId( Mig_Obj_t * p, int v )                { Mig_FanSetId( p, 3, v );                                   }
diff --git a/src/map/mpm/mpmTruth.c b/src/map/mpm/mpmTruth.c
index 0f9e877f..160ccee5 100644
--- a/src/map/mpm/mpmTruth.c
+++ b/src/map/mpm/mpmTruth.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "mpmInt.h"
+#include "misc/util/utilTruth.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -33,7 +34,7 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Performs truth table computation.]
 
   Description []
                
@@ -42,6 +43,101 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
+static inline int Mpm_CutTruthMinimize6( Mpm_Man_t * p, Mpm_Cut_t * pCut )
+{
+    unsigned uSupport;
+    int i, k, nSuppSize;
+    word t = *Mpm_CutTruth( p, Abc_Lit2Var(pCut->iFunc) );
+    // compute the support of the cut's function
+    uSupport = Abc_Tt6SupportAndSize( t, Mpm_CutLeafNum(pCut), &nSuppSize );
+    if ( nSuppSize == Mpm_CutLeafNum(pCut) )
+        return 0;
+    if ( nSuppSize < 2 )
+        p->nSmallSupp++;
+    // update leaves and signature
+    for ( i = k = 0; i < Mpm_CutLeafNum(pCut); i++ )
+    {
+        if ( !(uSupport & (1 << i)) )
+            continue;    
+        if ( k < i )
+        {
+            pCut->pLeaves[k] = pCut->pLeaves[i];
+            Abc_TtSwapVars( &t, p->nLutSize, k, i );
+        }
+        k++;
+    }
+    assert( k == nSuppSize );
+    pCut->nLeaves = nSuppSize;
+    assert( nSuppSize == Abc_TtSupportSize(&t, Mpm_CutLeafNum(pCut)) );
+    // save the result
+    if ( t & 1 )
+    {
+        t = ~t;
+        pCut->iFunc = Abc_Var2Lit( Vec_MemHashInsert( p->vTtMem, &t ), 1 );
+    }
+    else
+        pCut->iFunc = Abc_Var2Lit( Vec_MemHashInsert( p->vTtMem, &t ), 0 );
+    return 1;
+}
+static inline word Mpm_TruthStretch6( word Truth, Mpm_Cut_t * pCut, Mpm_Cut_t * pCut0, int nLimit )
+{
+    int i, k;
+    for ( i = (int)pCut->nLeaves - 1, k = (int)pCut0->nLeaves - 1; i >= 0 && k >= 0; i-- )
+    {
+        if ( pCut0->pLeaves[k] < pCut->pLeaves[i] )
+            continue;
+        assert( pCut0->pLeaves[k] == pCut->pLeaves[i] );
+        if ( k < i )
+            Abc_TtSwapVars( &Truth, nLimit, k, i );
+        k--;
+    }
+    return Truth;
+}
+int Mpm_CutComputeTruth6( Mpm_Man_t * p, Mpm_Cut_t * pCut, Mpm_Cut_t * pCut0, Mpm_Cut_t * pCut1, Mpm_Cut_t * pCutC, int fCompl0, int fCompl1, int fComplC, int Type )
+{
+    word * pTruth0 = Mpm_CutTruth( p, Abc_Lit2Var(pCut0->iFunc) );
+    word * pTruth1 = Mpm_CutTruth( p, Abc_Lit2Var(pCut1->iFunc) );
+    word * pTruthC = NULL;
+    word t0 = (fCompl0 ^ pCut0->fCompl ^ Abc_LitIsCompl(pCut0->iFunc)) ? ~*pTruth0 : *pTruth0;
+    word t1 = (fCompl1 ^ pCut1->fCompl ^ Abc_LitIsCompl(pCut1->iFunc)) ? ~*pTruth1 : *pTruth1;
+    word tC, t;
+    t0 = Mpm_TruthStretch6( t0, pCut, pCut0, p->nLutSize );
+    t1 = Mpm_TruthStretch6( t1, pCut, pCut1, p->nLutSize );
+    if ( pCutC )
+    {
+        pTruthC = Mpm_CutTruth( p, Abc_Lit2Var(pCutC->iFunc) );
+        tC = (fComplC ^ pCutC->fCompl ^ Abc_LitIsCompl(pCutC->iFunc)) ? ~*pTruthC : *pTruthC;
+        tC = Mpm_TruthStretch6( tC, pCut, pCutC, p->nLutSize );
+    }
+    assert( p->nLutSize <= 6 );
+    if ( Type == 1 )
+        t = t0 & t1;
+    else if ( Type == 2 )
+        t = t0 ^ t1;
+    else if ( Type == 3 )
+        t = (tC & t1) | (~tC & t0);
+    else assert( 0 );
+    // save the result
+    if ( t & 1 )
+    {
+        t = ~t;
+        pCut->iFunc = Abc_Var2Lit( Vec_MemHashInsert( p->vTtMem, &t ), 1 );
+    }
+    else
+        pCut->iFunc = Abc_Var2Lit( Vec_MemHashInsert( p->vTtMem, &t ), 0 );
+
+#ifdef MPM_TRY_NEW
+    {
+        word tCopy = t;
+        char pCanonPerm[16];
+        Abc_TtCanonicize( &tCopy, pCut->nLimit, pCanonPerm );
+    }
+#endif
+
+//    if ( p->pPars->fCutMin )
+//        return Mpm_CutTruthMinimize6( p, pCut );
+    return 0;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///