Version abc61205

10 files changed, 750 insertions, 616 deletions

diff --git a/src/map/if/if.h b/src/map/if/if.h
index 31c07528..32bb07f8 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -70,21 +70,27 @@ typedef struct If_Cut_t_     If_Cut_t;
 // parameters
 struct If_Par_t_
 {
+    // user-controlable paramters
     int                Mode;          // the mapping mode
     int                nLutSize;      // the LUT size
-    If_Lib_t *         pLutLib;       // the LUT library
     int                nCutsMax;      // the max number of cuts
-    int                fVerbose;      // the verbosity flag
+    float              DelayTarget;   // delay target
     int                fPreprocess;   // preprossing
     int                fArea;         // area-oriented mapping
     int                fFancy;        // a fancy feature
     int                fExpRed;       // expand/reduce of the best cuts
     int                fLatchPaths;   // reset timing on latch paths
     int                fSeq;          // sequential mapping
-    int                nLatches;      // the number of latches
-    float              DelayTarget;   // delay target
+    int                fVerbose;      // the verbosity flag
+    // internal parameters
+    int                fTruth;        // truth table computation enabled
+    int                fUseBdds;      // sets local BDDs at the nodes
+    int                nLatches;      // the number of latches in seq mapping
+    If_Lib_t *         pLutLib;       // the LUT library
     float *            pTimesArr;     // arrival times
     float *            pTimesReq;     // required times
+    int(*pFuncCost)(unsigned *, int); // procedure the user's cost of a cut
+    void *             pReoMan;       // reordering manager
 };
 
 // the LUT library
@@ -118,10 +124,13 @@ struct If_Man_t_
     int                nCutsMerged;   // the total number of cuts merged
     int                nCutsMax;      // the maximum number of cuts at a node
     float              Fi;            // the current value of the clock period (for seq mapping)
+    unsigned *         puTemp[4];     // used for the truth table computation
     // memory management
     Mem_Fixed_t *      pMem;          // memory manager
     int                nEntrySize;    // the size of the entry
     int                nEntryBase;    // the size of the entry minus cut leaf arrays
+    int                nTruthSize;    // the size of the truth table if allocated
+    int                nCutSize;      // the size of the cut
     // temporary cut storage
     int                nCuts;         // the number of cuts used
     If_Cut_t **        ppCuts;        // the storage space for cuts
@@ -132,14 +141,14 @@ struct If_Cut_t_
 {
     float              Delay;         // delay of the cut
     float              Area;          // area (or area-flow) of the cut
-    If_Cut_t *         pOne;          // parent cut
-    If_Cut_t *         pTwo;          // parent cut
     unsigned           uSign;         // cut signature
-    char               fCompl0;       // complemented attribute
-    char               fCompl1;       // complemented attribute
-    char               Phase;         // complemented attribute
-    char               nLeaves;       // number of leaves
+    unsigned           Cost    : 10;  // the user's cost of the cut
+    unsigned           Depth   :  9;  // the user's depth of the cut
+    unsigned           fCompl  :  1;  // the complemented attribute 
+    unsigned           nLimit  :  6;  // the maximum number of leaves
+    unsigned           nLeaves :  6;  // the number of leaves
     int *              pLeaves;       // array of fanins
+    unsigned *         pTruth;        // the truth table
 };
 
 // node extension
@@ -197,8 +206,11 @@ static inline unsigned   If_ObjCutSign( unsigned ObjId )                     { r
 static inline void *     If_CutData( If_Cut_t * pCut )                       { return *(void **)pCut;                }
 static inline void       If_CutSetData( If_Cut_t * pCut, void * pData )      { *(void **)pCut = pData;               }
 
-static inline float      If_CutLutDelay( If_Man_t * p, If_Cut_t * pCut )     { return p->pPars->pLutLib? p->pPars->pLutLib->pLutDelays[pCut->nLeaves] : (float)1.0;  }
-static inline float      If_CutLutArea( If_Man_t * p, If_Cut_t * pCut )      { return p->pPars->pLutLib? p->pPars->pLutLib->pLutAreas[pCut->nLeaves]  : (float)1.0;  }
+static inline int        If_CutTruthWords( int nVarsMax )                    { return nVarsMax <= 5 ? 1 : (1 << (nVarsMax - 5)); }
+static inline unsigned * If_CutTruth( If_Cut_t * pCut )                      { return pCut->pTruth;                              }
+
+static inline float      If_CutLutDelay( If_Man_t * p, If_Cut_t * pCut )     { return pCut->Depth? (float)pCut->Depth : (p->pPars->pLutLib? p->pPars->pLutLib->pLutDelays[pCut->nLeaves] : (float)1.0);  }
+static inline float      If_CutLutArea( If_Man_t * p, If_Cut_t * pCut )      { return pCut->Cost?  (float)pCut->Cost  : (p->pPars->pLutLib? p->pPars->pLutLib->pLutAreas[pCut->nLeaves]  : (float)1.0);  }
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
@@ -244,14 +256,7 @@ static inline float      If_CutLutArea( If_Man_t * p, If_Cut_t * pCut )      { r
 /*=== ifCore.c ==========================================================*/
 extern int             If_ManPerformMapping( If_Man_t * p );
 extern int             If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fRequired );
-/*=== ifMan.c ==========================================================*/
-extern If_Man_t *      If_ManStart( If_Par_t * pPars );
-extern void            If_ManStop( If_Man_t * p );
-extern If_Obj_t *      If_ManCreatePi( If_Man_t * p );
-extern If_Obj_t *      If_ManCreatePo( If_Man_t * p, If_Obj_t * pDriver, int fCompl0 );
-extern If_Obj_t *      If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_t * pFan1, int fCompl1 );
-/*=== ifMap.c ==========================================================*/
-extern void            If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode );
+/*=== ifCut.c ==========================================================*/
 extern float           If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut, int nLevels );
 extern float           If_CutAreaRefed( If_Man_t * p, If_Cut_t * pCut, int nLevels );
 extern float           If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels );
@@ -259,12 +264,26 @@ extern float           If_CutRef( If_Man_t * p, If_Cut_t * pCut, int nLevels );
 extern void            If_CutPrint( If_Man_t * p, If_Cut_t * pCut );
 extern float           If_CutDelay( If_Man_t * p, If_Cut_t * pCut );
 extern float           If_CutFlow( If_Man_t * p, If_Cut_t * pCut );
-extern int             If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut, int nLimit );
+extern int             If_CutFilter( If_Man_t * p, If_Cut_t * pCut );
+extern int             If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut );
 extern void            If_CutCopy( If_Cut_t * pCutDest, If_Cut_t * pCutSrc );
+extern void            If_ManSortCuts( If_Man_t * p, int Mode );
+/*=== ifMan.c ==========================================================*/
+extern If_Man_t *      If_ManStart( If_Par_t * pPars );
+extern void            If_ManStop( If_Man_t * p );
+extern If_Obj_t *      If_ManCreatePi( If_Man_t * p );
+extern If_Obj_t *      If_ManCreatePo( If_Man_t * p, If_Obj_t * pDriver, int fCompl0 );
+extern If_Obj_t *      If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_t * pFan1, int fCompl1 );
+/*=== ifMap.c ==========================================================*/
+extern void            If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode );
+/*=== ifPrepro.c ==========================================================*/
+extern void            If_ManPerformMappingPreprocess( If_Man_t * p );
 /*=== ifReduce.c ==========================================================*/
 extern void            If_ManImproveMapping( If_Man_t * p );
-/*=== ifSelect.c ==========================================================*/
-extern void            If_ManPerformMappingPreprocess( If_Man_t * p );
+/*=== ifSeq.c ==========================================================*/
+extern int             If_ManPerformMappingSeq( If_Man_t * p );
+/*=== ifTruth.c ==========================================================*/
+extern void            If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
 /*=== ifUtil.c ==========================================================*/
 extern float           If_ManDelayMax( If_Man_t * p );
 extern void            If_ManCleanNodeCopy( If_Man_t * p );
diff --git a/src/map/if/ifCore.c b/src/map/if/ifCore.c
index e139e14b..c5000dbe 100644
--- a/src/map/if/ifCore.c
+++ b/src/map/if/ifCore.c
@@ -59,20 +59,20 @@ int If_ManPerformMapping( If_Man_t * p )
     else
         If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 1 );
     // try to improve area by expanding and reducing the cuts
-    if ( p->pPars->fExpRed )
+    if ( p->pPars->fExpRed && !p->pPars->fTruth )
         If_ManImproveMapping( p );
     // area flow oriented mapping
     for ( i = 0; i < nItersFlow; i++ )
     {
         If_ManPerformMappingRound( p, p->pPars->nCutsMax, 1, 1 );
-        if ( p->pPars->fExpRed )
+        if ( p->pPars->fExpRed && !p->pPars->fTruth )
             If_ManImproveMapping( p );
     }
     // area oriented mapping
     for ( i = 0; i < nItersArea; i++ )
     {
         If_ManPerformMappingRound( p, p->pPars->nCutsMax, 2, 1 );
-        if ( p->pPars->fExpRed )
+        if ( p->pPars->fExpRed && !p->pPars->fTruth )
             If_ManImproveMapping( p );
     }
     if ( p->pPars->fVerbose )
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index 0318e5e5..56e354ce 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -28,9 +28,405 @@
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pDom is contained in pCut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int If_CutCheckDominance( If_Cut_t * pDom, If_Cut_t * pCut )
+{
+    int i, k;
+    for ( i = 0; i < (int)pDom->nLeaves; i++ )
+    {
+        for ( k = 0; k < (int)pCut->nLeaves; k++ )
+            if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
+                break;
+        if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut
+            return 0;
+    }
+    // every node in pDom is contained in pCut
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pDom is equal to pCut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int If_CutCheckEquality( If_Cut_t * pDom, If_Cut_t * pCut )
+{
+    int i;
+    if ( (int)pDom->nLeaves != (int)pCut->nLeaves )
+        return 0;
+    for ( i = 0; i < (int)pDom->nLeaves; i++ )
+        if ( pDom->pLeaves[i] != pCut->pLeaves[i] )
+            return 0;
+    return 1;
+}
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the cut is contained.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_CutFilter( If_Man_t * p, If_Cut_t * pCut )
+{
+    If_Cut_t * pTemp;
+    int i;
+    for ( i = 0; i < p->nCuts; i++ )
+    {
+        pTemp = p->ppCuts[i];
+        if ( pTemp->nLeaves > pCut->nLeaves )
+        {
+//            continue;
+            // skip the non-contained cuts
+            if ( (pTemp->uSign & pCut->uSign) != pCut->uSign )
+                continue;
+            // check containment seriously
+            if ( If_CutCheckDominance( pCut, pTemp ) )
+            {
+                // removed contained cut
+                p->ppCuts[i] = p->ppCuts[p->nCuts-1];
+                p->ppCuts[p->nCuts-1] = pTemp;
+                p->nCuts--;
+                i--;
+            }
+         }
+        else
+        {
+            // skip the non-contained cuts
+            if ( (pTemp->uSign & pCut->uSign) != pTemp->uSign )
+                continue;
+            // check containment seriously
+            if ( If_CutCheckDominance( pTemp, pCut ) )
+                return 1;
+        }
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int If_CutMergeOrdered( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC )
+{ 
+    int i, k, c;
+    assert( pC0->nLeaves >= pC1->nLeaves );
+    // the case of the largest cut sizes
+    if ( pC0->nLeaves == pC->nLimit && pC1->nLeaves == pC->nLimit )
+    {
+        for ( i = 0; i < (int)pC0->nLeaves; i++ )
+            if ( pC0->pLeaves[i] != pC1->pLeaves[i] )
+                return 0;
+        for ( i = 0; i < (int)pC0->nLeaves; i++ )
+            pC->pLeaves[i] = pC0->pLeaves[i];
+        pC->nLeaves = pC0->nLeaves;
+        return 1;
+    }
+    // the case when one of the cuts is the largest
+    if ( pC0->nLeaves == pC->nLimit )
+    {
+        for ( i = 0; i < (int)pC1->nLeaves; i++ )
+        {
+            for ( k = (int)pC0->nLeaves - 1; k >= 0; k-- )
+                if ( pC0->pLeaves[k] == pC1->pLeaves[i] )
+                    break;
+            if ( k == -1 ) // did not find
+                return 0;
+        }
+        for ( i = 0; i < (int)pC0->nLeaves; i++ )
+            pC->pLeaves[i] = pC0->pLeaves[i];
+        pC->nLeaves = pC0->nLeaves;
+        return 1;
+    }
+
+    // compare two cuts with different numbers
+    i = k = 0;
+    for ( c = 0; c < (int)pC->nLimit; c++ )
+    {
+        if ( k == (int)pC1->nLeaves )
+        {
+            if ( i == (int)pC0->nLeaves )
+            {
+                pC->nLeaves = c;
+                return 1;
+            }
+            pC->pLeaves[c] = pC0->pLeaves[i++];
+            continue;
+        }
+        if ( i == (int)pC0->nLeaves )
+        {
+            if ( k == (int)pC1->nLeaves )
+            {
+                pC->nLeaves = c;
+                return 1;
+            }
+            pC->pLeaves[c] = pC1->pLeaves[k++];
+            continue;
+        }
+        if ( pC0->pLeaves[i] < pC1->pLeaves[k] )
+        {
+            pC->pLeaves[c] = pC0->pLeaves[i++];
+            continue;
+        }
+        if ( pC0->pLeaves[i] > pC1->pLeaves[k] )
+        {
+            pC->pLeaves[c] = pC1->pLeaves[k++];
+            continue;
+        }
+        pC->pLeaves[c] = pC0->pLeaves[i++]; 
+        k++;
+    }
+    if ( i < (int)pC0->nLeaves || k < (int)pC1->nLeaves )
+        return 0;
+    pC->nLeaves = c;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two cuts.]
+
+  Description [Special case when the cut is known to exist.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int If_CutMergeOrdered2( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC )
+{ 
+    int i, k, c;
+    assert( pC0->nLeaves >= pC1->nLeaves );
+    // copy the first cut
+    for ( i = 0; i < (int)pC0->nLeaves; i++ )
+        pC->pLeaves[i] = pC0->pLeaves[i];
+    pC->nLeaves = pC0->nLeaves;
+    // the case when one of the cuts is the largest
+    if ( pC0->nLeaves == pC->nLimit )
+        return 1;
+    // add nodes of the second cut
+    k = 0;
+    for ( i = 0; i < (int)pC1->nLeaves; i++ )
+    {
+        // find k-th node before which i-th node should be added
+        for ( ; k < (int)pC->nLeaves; k++ )
+            if ( pC->pLeaves[k] >= pC1->pLeaves[i] )
+                break;
+        // check the case when this should be the last node
+        if ( k == (int)pC->nLeaves )
+        {
+            pC->pLeaves[k++] = pC1->pLeaves[i];
+            pC->nLeaves++;
+            continue;
+        }
+        // check the case when equal node is found
+        if ( pC1->pLeaves[i] == pC->pLeaves[k] )
+            continue;
+        // add the node
+        for ( c = (int)pC->nLeaves; c > k; c-- )
+            pC->pLeaves[c] = pC->pLeaves[c-1];
+        pC->pLeaves[k++] = pC1->pLeaves[i];
+        pC->nLeaves++;
+    }
+    assert( pC->nLeaves <= pC->nLimit );
+    for ( i = 1; i < (int)pC->nLeaves; i++ )
+        assert( pC->pLeaves[i-1] < pC->pLeaves[i] );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the object for FPGA mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut )
+{ 
+    assert( pCut->nLimit > 0 );
+    // merge the nodes
+    if ( pCut0->nLeaves < pCut1->nLeaves )
+    {
+        if ( !If_CutMergeOrdered( pCut1, pCut0, pCut ) )
+            return 0;
+    }
+    else
+    {
+        if ( !If_CutMergeOrdered( pCut0, pCut1, pCut ) )
+            return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the object for FPGA mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_CutCompareDelay( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
+{
+    If_Cut_t * pC0 = *ppC0;
+    If_Cut_t * pC1 = *ppC1;
+    if ( pC0->Delay < pC1->Delay - 0.0001 )
+        return -1;
+    if ( pC0->Delay > pC1->Delay + 0.0001 )
+        return 1;
+    if ( pC0->nLeaves < pC1->nLeaves )
+        return -1;
+    if ( pC0->nLeaves > pC1->nLeaves )
+        return 1;
+    if ( pC0->Area < pC1->Area - 0.0001 )
+        return -1;
+    if ( pC0->Area > pC1->Area + 0.0001 )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the object for FPGA mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_CutCompareDelayOld( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
+{
+    If_Cut_t * pC0 = *ppC0;
+    If_Cut_t * pC1 = *ppC1;
+    if ( pC0->Delay < pC1->Delay - 0.0001 )
+        return -1;
+    if ( pC0->Delay > pC1->Delay + 0.0001 )
+        return 1;
+    if ( pC0->Area < pC1->Area - 0.0001 )
+        return -1;
+    if ( pC0->Area > pC1->Area + 0.0001 )
+        return 1;
+    if ( pC0->nLeaves < pC1->nLeaves )
+        return -1;
+    if ( pC0->nLeaves > pC1->nLeaves )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the object for FPGA mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_CutCompareArea( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
+{
+    If_Cut_t * pC0 = *ppC0;
+    If_Cut_t * pC1 = *ppC1;
+    if ( pC0->Area < pC1->Area - 0.0001 )
+        return -1;
+    if ( pC0->Area > pC1->Area + 0.0001 )
+        return 1;
+    if ( pC0->nLeaves < pC1->nLeaves )
+        return -1;
+    if ( pC0->nLeaves > pC1->nLeaves )
+        return 1;
+    if ( pC0->Delay < pC1->Delay - 0.0001 )
+        return -1;
+    if ( pC0->Delay > pC1->Delay + 0.0001 )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorts the cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManSortCuts( If_Man_t * p, int Mode )
+{
+    // sort the cuts
+    if ( Mode || p->pPars->fArea ) // area
+        qsort( p->ppCuts, p->nCuts, sizeof(If_Cut_t *), (int (*)(const void *, const void *))If_CutCompareArea );
+    else if ( p->pPars->fFancy )
+        qsort( p->ppCuts, p->nCuts, sizeof(If_Cut_t *), (int (*)(const void *, const void *))If_CutCompareDelayOld );
+    else
+        qsort( p->ppCuts, p->nCuts, sizeof(If_Cut_t *), (int (*)(const void *, const void *))If_CutCompareDelay );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes delay.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float If_CutDelay( If_Man_t * p, If_Cut_t * pCut )
+{
+    If_Obj_t * pLeaf;
+    float Delay;
+    int i;
+    assert( pCut->nLeaves > 1 );
+    Delay = -IF_FLOAT_LARGE;
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+        Delay = IF_MAX( Delay, If_ObjCutBest(pLeaf)->Delay );
+    return Delay + If_CutLutDelay(p, pCut);
+}
+
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Computes area flow.]
 
   Description []
                
@@ -39,6 +435,166 @@
   SeeAlso     []
 
 ***********************************************************************/
+float If_CutFlow( If_Man_t * p, If_Cut_t * pCut )
+{
+    If_Obj_t * pLeaf;
+    float Flow;
+    int i;
+    assert( pCut->nLeaves > 1 );
+    Flow = If_CutLutArea(p, pCut);
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+    {
+        if ( pLeaf->nRefs == 0 )
+            Flow += If_ObjCutBest(pLeaf)->Area;
+        else
+        {
+            assert( pLeaf->EstRefs > p->fEpsilon );
+            Flow += If_ObjCutBest(pLeaf)->Area / pLeaf->EstRefs;
+        }
+    }
+    return Flow;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area of the first level.]
+
+  Description [The cut need to be derefed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels )
+{
+    If_Obj_t * pLeaf;
+    float Area;
+    int i;
+    Area = If_CutLutArea(p, pCut);
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+    {
+        assert( pLeaf->nRefs > 0 );
+        if ( --pLeaf->nRefs > 0 || !If_ObjIsAnd(pLeaf) || nLevels == 1 )
+            continue;
+        Area += If_CutDeref( p, If_ObjCutBest(pLeaf), nLevels - 1 );
+    }
+    return Area;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area of the first level.]
+
+  Description [The cut need to be derefed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float If_CutRef( If_Man_t * p, If_Cut_t * pCut, int nLevels )
+{
+    If_Obj_t * pLeaf;
+    float Area;
+    int i;
+    Area = If_CutLutArea(p, pCut);
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+    {
+        assert( pLeaf->nRefs >= 0 );
+        if ( pLeaf->nRefs++ > 0 || !If_ObjIsAnd(pLeaf) || nLevels == 1 )
+            continue;
+        Area += If_CutRef( p, If_ObjCutBest(pLeaf), nLevels - 1 );
+    }
+    return Area;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_CutPrint( If_Man_t * p, If_Cut_t * pCut )
+{
+    unsigned i;
+    printf( "{" );
+    for ( i = 0; i < pCut->nLeaves; i++ )
+        printf( " %d", pCut->pLeaves[i] );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area of the first level.]
+
+  Description [The cut need to be derefed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut, int nLevels )
+{
+    float aResult, aResult2;
+    assert( pCut->nLeaves > 1 );
+    aResult2 = If_CutRef( p, pCut, nLevels );
+    aResult  = If_CutDeref( p, pCut, nLevels );
+    assert( aResult == aResult2 );
+    return aResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area of the first level.]
+
+  Description [The cut need to be derefed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float If_CutAreaRefed( If_Man_t * p, If_Cut_t * pCut, int nLevels )
+{
+    float aResult, aResult2;
+    assert( pCut->nLeaves > 1 );
+    aResult2 = If_CutDeref( p, pCut, nLevels );
+    aResult  = If_CutRef( p, pCut, nLevels );
+    assert( aResult == aResult2 );
+    return aResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area of the first level.]
+
+  Description [The cut need to be derefed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_CutCopy( If_Cut_t * pCutDest, If_Cut_t * pCutSrc )
+{
+    int * pLeaves;
+    unsigned * pTruth;
+    pLeaves = pCutDest->pLeaves;
+    pTruth  = pCutDest->pTruth;
+    *pCutDest = *pCutSrc;
+    pCutDest->pLeaves = pLeaves;
+    pCutDest->pTruth  = pTruth;
+    memcpy( pCutDest->pLeaves, pCutSrc->pLeaves, sizeof(int) * pCutSrc->nLeaves );
+    if ( pCutSrc->pTruth )
+    memcpy( pCutDest->pTruth,  pCutSrc->pTruth,  sizeof(unsigned) * If_CutTruthWords(pCutSrc->nLimit) );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index b0c12fea..9e3d8e88 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -57,9 +57,20 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
     p->vMapped = Vec_PtrAlloc( 100 );
     p->vTemp   = Vec_PtrAlloc( 100 );
     // prepare the memory manager
-    p->nEntrySize = sizeof(If_Obj_t) + p->pPars->nCutsMax * (sizeof(If_Cut_t) + sizeof(int) * p->pPars->nLutSize);
-    p->nEntryBase = sizeof(If_Obj_t) + p->pPars->nCutsMax * (sizeof(If_Cut_t));
+    p->nTruthSize = p->pPars->fTruth? If_CutTruthWords( p->pPars->nLutSize ) : 0;
+    p->nCutSize   = sizeof(If_Cut_t) + sizeof(int) * p->pPars->nLutSize + sizeof(unsigned) * p->nTruthSize;
+    p->nEntrySize = sizeof(If_Obj_t) + p->pPars->nCutsMax * p->nCutSize;
+    p->nEntryBase = sizeof(If_Obj_t) + p->pPars->nCutsMax * sizeof(If_Cut_t);
     p->pMem = Mem_FixedStart( p->nEntrySize );
+    // report expected memory usage
+    if ( p->pPars->fVerbose )
+        printf( "Memory (bytes): Truth = %3d. Cut = %3d. Entry = %4d. Total = %.2f Mb / 1K AIG nodes\n", 
+            4 * p->nTruthSize, p->nCutSize, p->nEntrySize, 1000.0 * p->nEntrySize / (1<<20) );
+    // room for temporary truth tables
+    p->puTemp[0] = p->pPars->fTruth? ALLOC( unsigned, 4 * p->nTruthSize ) : NULL;
+    p->puTemp[1] = p->puTemp[0] + p->nTruthSize;
+    p->puTemp[2] = p->puTemp[1] + p->nTruthSize;
+    p->puTemp[3] = p->puTemp[2] + p->nTruthSize;
     // create the constant node
     p->pConst1 = If_ManSetupObj( p );
     p->pConst1->Type = IF_CONST1;
@@ -100,6 +111,7 @@ void If_ManStop( If_Man_t * p )
     for ( i = 1; i < 1 + p->pPars->nCutsMax * p->pPars->nCutsMax; i++ )
         if ( pTemp > p->ppCuts[i] )
             pTemp = p->ppCuts[i];
+    FREE( p->puTemp[0] );
     free( pTemp );
     free( p->ppCuts );
     free( p );
@@ -200,7 +212,12 @@ If_Obj_t * If_ManSetupObj( If_Man_t * p )
     // organize memory
     pArrays = (int *)((char *)pObj + p->nEntryBase);
     for ( i = 0; i < p->pPars->nCutsMax; i++ )
-        pObj->Cuts[i].pLeaves = pArrays + i * p->pPars->nLutSize;
+    {
+        pCut = pObj->Cuts + i;
+        pCut->nLimit  = p->pPars->nLutSize;
+        pCut->pLeaves = pArrays + i * p->pPars->nLutSize;
+        pCut->pTruth  = pArrays + p->pPars->nCutsMax * p->pPars->nLutSize + i * p->nTruthSize;
+    }
     // assign ID and save 
     pObj->Id = Vec_PtrSize(p->vObjs);
     Vec_PtrPush( p->vObjs, pObj );
@@ -230,22 +247,24 @@ If_Obj_t * If_ManSetupObj( If_Man_t * p )
 If_Cut_t ** If_ManSetupCuts( If_Man_t * p )
 {
     If_Cut_t ** pCutStore;
-    int * pArrays, nCutSize, nCutsTotal, i;
+    int * pArrays, nCutsTotal, i;
     // decide how many cuts to alloc
     nCutsTotal = 1 + p->pPars->nCutsMax * p->pPars->nCutsMax;
-    // figure out the cut size
-    nCutSize = sizeof(If_Cut_t) + sizeof(int) * p->pPars->nLutSize;
     // allocate and clean space for cuts
     pCutStore = (If_Cut_t **)ALLOC( If_Cut_t *, (nCutsTotal + 1) );
     memset( pCutStore, 0, sizeof(If_Cut_t *) * (nCutsTotal + 1) );
-    pCutStore[0] = (If_Cut_t *)ALLOC( char, nCutSize * nCutsTotal );
-    memset( pCutStore[0], 0, nCutSize * nCutsTotal );
-    for ( i = 1; i < nCutsTotal; i++ )
-        pCutStore[i] = (If_Cut_t *)((char *)pCutStore[0] + sizeof(If_Cut_t) * i);
-    // assign room for cut leaves
+    pCutStore[0] = (If_Cut_t *)ALLOC( char, p->nCutSize * nCutsTotal );
+    memset( pCutStore[0], 0, p->nCutSize * nCutsTotal );
+    // assign cut paramters and space for the cut leaves
+    assert( sizeof(int) == sizeof(unsigned) );
     pArrays = (int *)((char *)pCutStore[0] + sizeof(If_Cut_t) * nCutsTotal);
     for ( i = 0; i < nCutsTotal; i++ )
+    {
+        pCutStore[i] = (If_Cut_t *)((char *)pCutStore[0] + sizeof(If_Cut_t) * i);
+        pCutStore[i]->nLimit  = p->pPars->nLutSize;
         pCutStore[i]->pLeaves = pArrays + i * p->pPars->nLutSize;
+        pCutStore[i]->pTruth  = pArrays + nCutsTotal * p->pPars->nLutSize + i * p->nTruthSize;
+    }
     return pCutStore;
 }
 
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 9134dc9a..76c524ee 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -59,567 +59,6 @@ static inline int If_WordCountOnes( unsigned uWord )
 
 /**Function*************************************************************
 
-  Synopsis    [Returns 1 if pDom is contained in pCut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int If_CutCheckDominance( If_Cut_t * pDom, If_Cut_t * pCut )
-{
-    int i, k;
-    for ( i = 0; i < (int)pDom->nLeaves; i++ )
-    {
-        for ( k = 0; k < (int)pCut->nLeaves; k++ )
-            if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
-                break;
-        if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut
-            return 0;
-    }
-    // every node in pDom is contained in pCut
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if pDom is equal to pCut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int If_CutCheckEquality( If_Cut_t * pDom, If_Cut_t * pCut )
-{
-    int i;
-    if ( (int)pDom->nLeaves != (int)pCut->nLeaves )
-        return 0;
-    for ( i = 0; i < (int)pDom->nLeaves; i++ )
-        if ( pDom->pLeaves[i] != pCut->pLeaves[i] )
-            return 0;
-    return 1;
-}
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the cut is contained.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int If_CutFilter( If_Man_t * p, If_Cut_t * pCut, int Mode )
-{
-    If_Cut_t * pTemp;
-    int i;
-    for ( i = 0; i < p->nCuts; i++ )
-    {
-        pTemp = p->ppCuts[i];
-        if ( pTemp->nLeaves > pCut->nLeaves )
-        {
-//            continue;
-            // skip the non-contained cuts
-            if ( (pTemp->uSign & pCut->uSign) != pCut->uSign )
-                continue;
-            // check containment seriously
-            if ( If_CutCheckDominance( pCut, pTemp ) )
-            {
-                // removed contained cut
-                p->ppCuts[i] = p->ppCuts[p->nCuts-1];
-                p->ppCuts[p->nCuts-1] = pTemp;
-                p->nCuts--;
-                i--;
-            }
-         }
-        else
-        {
-            // skip the non-contained cuts
-            if ( (pTemp->uSign & pCut->uSign) != pTemp->uSign )
-                continue;
-            // check containment seriously
-            if ( If_CutCheckDominance( pTemp, pCut ) )
-                return 1;
-        }
-    }
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Merges two cuts.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int If_CutMergeOrdered( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC, int nLimit )
-{ 
-    int i, k, c;
-    assert( pC0->nLeaves >= pC1->nLeaves );
-    // the case of the largest cut sizes
-    if ( pC0->nLeaves == nLimit && pC1->nLeaves == nLimit )
-    {
-        for ( i = 0; i < pC0->nLeaves; i++ )
-            if ( pC0->pLeaves[i] != pC1->pLeaves[i] )
-                return 0;
-        for ( i = 0; i < pC0->nLeaves; i++ )
-            pC->pLeaves[i] = pC0->pLeaves[i];
-        pC->nLeaves = pC0->nLeaves;
-        return 1;
-    }
-    // the case when one of the cuts is the largest
-    if ( pC0->nLeaves == nLimit )
-    {
-        for ( i = 0; i < pC1->nLeaves; i++ )
-        {
-            for ( k = pC0->nLeaves - 1; k >= 0; k-- )
-                if ( pC0->pLeaves[k] == pC1->pLeaves[i] )
-                    break;
-            if ( k == -1 ) // did not find
-                return 0;
-        }
-        for ( i = 0; i < pC0->nLeaves; i++ )
-            pC->pLeaves[i] = pC0->pLeaves[i];
-        pC->nLeaves = pC0->nLeaves;
-        return 1;
-    }
-
-    // compare two cuts with different numbers
-    i = k = 0;
-    for ( c = 0; c < nLimit; c++ )
-    {
-        if ( k == pC1->nLeaves )
-        {
-            if ( i == pC0->nLeaves )
-            {
-                pC->nLeaves = c;
-                return 1;
-            }
-            pC->pLeaves[c] = pC0->pLeaves[i++];
-            continue;
-        }
-        if ( i == pC0->nLeaves )
-        {
-            if ( k == pC1->nLeaves )
-            {
-                pC->nLeaves = c;
-                return 1;
-            }
-            pC->pLeaves[c] = pC1->pLeaves[k++];
-            continue;
-        }
-        if ( pC0->pLeaves[i] < pC1->pLeaves[k] )
-        {
-            pC->pLeaves[c] = pC0->pLeaves[i++];
-            continue;
-        }
-        if ( pC0->pLeaves[i] > pC1->pLeaves[k] )
-        {
-            pC->pLeaves[c] = pC1->pLeaves[k++];
-            continue;
-        }
-        pC->pLeaves[c] = pC0->pLeaves[i++]; 
-        k++;
-    }
-    if ( i < pC0->nLeaves || k < pC1->nLeaves )
-        return 0;
-    pC->nLeaves = c;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Merges two cuts.]
-
-  Description [Special case when the cut is known to exist.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int If_CutMergeOrdered2( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC, int nLimit )
-{ 
-    int i, k, c;
-    assert( pC0->nLeaves >= pC1->nLeaves );
-    // copy the first cut
-    for ( i = 0; i < pC0->nLeaves; i++ )
-        pC->pLeaves[i] = pC0->pLeaves[i];
-    pC->nLeaves = pC0->nLeaves;
-    // the case when one of the cuts is the largest
-    if ( pC0->nLeaves == nLimit )
-        return 1;
-    // add nodes of the second cut
-    k = 0;
-    for ( i = 0; i < pC1->nLeaves; i++ )
-    {
-        // find k-th node before which i-th node should be added
-        for ( ; k < pC->nLeaves; k++ )
-            if ( pC->pLeaves[k] >= pC1->pLeaves[i] )
-                break;
-        // check the case when this should be the last node
-        if ( k == pC->nLeaves )
-        {
-            pC->pLeaves[k++] = pC1->pLeaves[i];
-            pC->nLeaves++;
-            continue;
-        }
-        // check the case when equal node is found
-        if ( pC1->pLeaves[i] == pC->pLeaves[k] )
-            continue;
-        // add the node
-        for ( c = pC->nLeaves; c > k; c-- )
-            pC->pLeaves[c] = pC->pLeaves[c-1];
-        pC->pLeaves[k++] = pC1->pLeaves[i];
-        pC->nLeaves++;
-    }
-    assert( pC->nLeaves <= nLimit );
-    for ( i = 1; i < pC->nLeaves; i++ )
-        assert( pC->pLeaves[i-1] < pC->pLeaves[i] );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the object for FPGA mapping.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut, int nLimit )
-{ 
-    // merge the nodes
-    if ( pCut0->nLeaves < pCut1->nLeaves )
-    {
-        if ( !If_CutMergeOrdered( pCut1, pCut0, pCut, nLimit ) )
-            return 0;
-    }
-    else
-    {
-        if ( !If_CutMergeOrdered( pCut0, pCut1, pCut, nLimit ) )
-            return 0;
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the object for FPGA mapping.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int If_CutCompareDelay( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
-{
-    If_Cut_t * pC0 = *ppC0;
-    If_Cut_t * pC1 = *ppC1;
-    if ( pC0->Delay < pC1->Delay - 0.0001 )
-        return -1;
-    if ( pC0->Delay > pC1->Delay + 0.0001 )
-        return 1;
-    if ( pC0->nLeaves < pC1->nLeaves )
-        return -1;
-    if ( pC0->nLeaves > pC1->nLeaves )
-        return 1;
-    if ( pC0->Area < pC1->Area - 0.0001 )
-        return -1;
-    if ( pC0->Area > pC1->Area + 0.0001 )
-        return 1;
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the object for FPGA mapping.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int If_CutCompareDelayOld( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
-{
-    If_Cut_t * pC0 = *ppC0;
-    If_Cut_t * pC1 = *ppC1;
-    if ( pC0->Delay < pC1->Delay - 0.0001 )
-        return -1;
-    if ( pC0->Delay > pC1->Delay + 0.0001 )
-        return 1;
-    if ( pC0->Area < pC1->Area - 0.0001 )
-        return -1;
-    if ( pC0->Area > pC1->Area + 0.0001 )
-        return 1;
-    if ( pC0->nLeaves < pC1->nLeaves )
-        return -1;
-    if ( pC0->nLeaves > pC1->nLeaves )
-        return 1;
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the object for FPGA mapping.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int If_CutCompareArea( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
-{
-    If_Cut_t * pC0 = *ppC0;
-    If_Cut_t * pC1 = *ppC1;
-    if ( pC0->Area < pC1->Area - 0.0001 )
-        return -1;
-    if ( pC0->Area > pC1->Area + 0.0001 )
-        return 1;
-    if ( pC0->nLeaves < pC1->nLeaves )
-        return -1;
-    if ( pC0->nLeaves > pC1->nLeaves )
-        return 1;
-    if ( pC0->Delay < pC1->Delay - 0.0001 )
-        return -1;
-    if ( pC0->Delay > pC1->Delay + 0.0001 )
-        return 1;
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sorts the cuts.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void If_ManSortCuts( If_Man_t * p, int Mode )
-{
-    // sort the cuts
-    if ( Mode || p->pPars->fArea ) // area
-        qsort( p->ppCuts, p->nCuts, sizeof(If_Cut_t *), (int (*)(const void *, const void *))If_CutCompareArea );
-    else if ( p->pPars->fFancy )
-        qsort( p->ppCuts, p->nCuts, sizeof(If_Cut_t *), (int (*)(const void *, const void *))If_CutCompareDelayOld );
-    else
-        qsort( p->ppCuts, p->nCuts, sizeof(If_Cut_t *), (int (*)(const void *, const void *))If_CutCompareDelay );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes delay.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-float If_CutDelay( If_Man_t * p, If_Cut_t * pCut )
-{
-    If_Obj_t * pLeaf;
-    float Delay;
-    int i;
-    assert( pCut->nLeaves > 1 );
-    Delay = -IF_FLOAT_LARGE;
-    If_CutForEachLeaf( p, pCut, pLeaf, i )
-        Delay = IF_MAX( Delay, If_ObjCutBest(pLeaf)->Delay );
-    return Delay + If_CutLutDelay(p, pCut);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes area flow.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-float If_CutFlow( If_Man_t * p, If_Cut_t * pCut )
-{
-    If_Obj_t * pLeaf;
-    float Flow;
-    int i;
-    assert( pCut->nLeaves > 1 );
-    Flow = If_CutLutArea(p, pCut);
-    If_CutForEachLeaf( p, pCut, pLeaf, i )
-    {
-        if ( pLeaf->nRefs == 0 )
-            Flow += If_ObjCutBest(pLeaf)->Area;
-        else
-        {
-            assert( pLeaf->EstRefs > p->fEpsilon );
-            Flow += If_ObjCutBest(pLeaf)->Area / pLeaf->EstRefs;
-        }
-    }
-    return Flow;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes area of the first level.]
-
-  Description [The cut need to be derefed.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-float If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels )
-{
-    If_Obj_t * pLeaf;
-    float Area;
-    int i;
-    Area = If_CutLutArea(p, pCut);
-    If_CutForEachLeaf( p, pCut, pLeaf, i )
-    {
-        assert( pLeaf->nRefs > 0 );
-        if ( --pLeaf->nRefs > 0 || !If_ObjIsAnd(pLeaf) || nLevels == 1 )
-            continue;
-        Area += If_CutDeref( p, If_ObjCutBest(pLeaf), nLevels - 1 );
-    }
-    return Area;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes area of the first level.]
-
-  Description [The cut need to be derefed.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-float If_CutRef( If_Man_t * p, If_Cut_t * pCut, int nLevels )
-{
-    If_Obj_t * pLeaf;
-    float Area;
-    int i;
-    Area = If_CutLutArea(p, pCut);
-    If_CutForEachLeaf( p, pCut, pLeaf, i )
-    {
-        assert( pLeaf->nRefs >= 0 );
-        if ( pLeaf->nRefs++ > 0 || !If_ObjIsAnd(pLeaf) || nLevels == 1 )
-            continue;
-        Area += If_CutRef( p, If_ObjCutBest(pLeaf), nLevels - 1 );
-    }
-    return Area;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints one cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void If_CutPrint( If_Man_t * p, If_Cut_t * pCut )
-{
-    int i;
-    printf( "{" );
-    for ( i = 0; i < pCut->nLeaves; i++ )
-        printf( " %d", pCut->pLeaves[i] );
-    printf( " }\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes area of the first level.]
-
-  Description [The cut need to be derefed.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-float If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut, int nLevels )
-{
-    float aResult, aResult2;
-    assert( pCut->nLeaves > 1 );
-    aResult2 = If_CutRef( p, pCut, nLevels );
-    aResult  = If_CutDeref( p, pCut, nLevels );
-    assert( aResult == aResult2 );
-    return aResult;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes area of the first level.]
-
-  Description [The cut need to be derefed.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-float If_CutAreaRefed( If_Man_t * p, If_Cut_t * pCut, int nLevels )
-{
-    float aResult, aResult2;
-    assert( pCut->nLeaves > 1 );
-    aResult2 = If_CutDeref( p, pCut, nLevels );
-    aResult  = If_CutRef( p, pCut, nLevels );
-    assert( aResult == aResult2 );
-    return aResult;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes area of the first level.]
-
-  Description [The cut need to be derefed.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void If_CutCopy( If_Cut_t * pCutDest, If_Cut_t * pCutSrc )
-{
-    int * pArray;
-    pArray = pCutDest->pLeaves;
-    *pCutDest = *pCutSrc;
-    pCutDest->pLeaves = pArray;
-    memcpy( pCutDest->pLeaves, pCutSrc->pLeaves, sizeof(int) * pCutSrc->nLeaves );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Finds the best cut.]
 
   Description [Mapping modes: delay (0), area flow (1), area (2).]
@@ -632,7 +71,7 @@ void If_CutCopy( If_Cut_t * pCutDest, If_Cut_t * pCutSrc )
 void If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode )
 {
     If_Cut_t * pCut0, * pCut1, * pCut;
-    int i, k, iCut;
+    int i, k, iCut, Temp;
 
     // prepare
     if ( Mode == 0 )
@@ -670,29 +109,34 @@ void If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode )
         if ( Mode && (pCut0->Delay > pObj->Required + p->fEpsilon || pCut1->Delay > pObj->Required + p->fEpsilon) )
             continue;
         // merge the nodes
-        if ( !If_CutMerge( pCut0, pCut1, pCut, p->pPars->nLutSize ) )
+        if ( !If_CutMerge( pCut0, pCut1, pCut ) )
             continue;
         // check if this cut is contained in any of the available cuts
         pCut->uSign = pCut0->uSign | pCut1->uSign;
-        if ( If_CutFilter( p, pCut, Mode ) )
+        if ( If_CutFilter( p, pCut ) )
             continue;
         // check if the cut satisfies the required times
         pCut->Delay = If_CutDelay( p, pCut );
         if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon )
             continue;
         // the cuts have been successfully merged
-        pCut->pOne = pCut0; pCut->fCompl0 = pObj->fCompl0;
-        pCut->pTwo = pCut1; pCut->fCompl1 = pObj->fCompl1;
-//        pCut->Phase = ...
-//        pCut->Phase = (char)(int)If_CutAreaDerefed( p, pCut, 1 );
-        pCut->Area  = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut );
-        p->nCutsMerged++;
+        // compute the truth table
+        if ( p->pPars->fTruth )
+            If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
+        // compute the application-specific cost and depth
+        Temp = p->pPars->pFuncCost? p->pPars->pFuncCost(If_CutTruth(pCut), pCut->nLimit) : 0;
+        pCut->Cost = (Temp & 0xffff); pCut->Depth = (Temp >> 16);
+        // compute area of the cut (this area may depend on the application specific cost)
+        pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut );
         // make sure the cut is the last one (after filtering it may not be so)
         assert( pCut == p->ppCuts[iCut] );
         p->ppCuts[iCut] = p->ppCuts[p->nCuts];
         p->ppCuts[p->nCuts] = pCut;
+        // count the cut
+        p->nCuts++;
+        p->nCutsMerged++;
         // prepare room for the next cut
-        iCut = ++p->nCuts;
+        iCut = p->nCuts;
         pCut = p->ppCuts[iCut];
     } 
 //printf( "%d  ", p->nCuts );
diff --git a/src/map/if/ifSelect.c b/src/map/if/ifPrepro.c
index d54abb29..797e8727 100644
--- a/src/map/if/ifSelect.c
+++ b/src/map/if/ifPrepro.c
@@ -1,12 +1,12 @@
 /**CFile****************************************************************
 
-  FileName    [ifSelect.c]
+  FileName    [ifPrepro.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
   PackageName [FPGA mapping based on priority cuts.]
 
-  Synopsis    [Selects what mapping to use.]
+  Synopsis    [Selects the starting mapping.]
 
   Author      [Alan Mishchenko]
   
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - November 21, 2006.]
 
-  Revision    [$Id: ifSelect.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
+  Revision    [$Id: ifPrepro.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
diff --git a/src/map/if/ifReduce.c b/src/map/if/ifReduce.c
index 5c8da0d0..0b3cf9c2 100644
--- a/src/map/if/ifReduce.c
+++ b/src/map/if/ifReduce.c
@@ -522,11 +522,11 @@ void If_ManImproveNodeReduce( If_Man_t * p, If_Obj_t * pObj, int nLimit )
 
     // merge the cuts
     pCutR = p->ppCuts[0];
-    RetValue = If_CutMerge( pCut0, pCut1, pCutR, nLimit );
+    RetValue = If_CutMerge( pCut0, pCut1, pCutR );
     // try very simple cut
     if ( !RetValue )
     {
-        RetValue = If_CutMerge( If_ObjCutTriv(pFanin0), If_ObjCutTriv(pFanin1), pCutR, nLimit );
+        RetValue = If_CutMerge( If_ObjCutTriv(pFanin0), If_ObjCutTriv(pFanin1), pCutR );
         assert( RetValue == 1 );
     }
     if ( RetValue )
diff --git a/src/map/if/ifSeq.c b/src/map/if/ifSeq.c
index ce353f49..bc4ab806 100644
--- a/src/map/if/ifSeq.c
+++ b/src/map/if/ifSeq.c
@@ -95,7 +95,7 @@ int If_ManPerformMappingSeq( If_Man_t * p )
 ***********************************************************************/
 void If_CutLift( If_Cut_t * pCut )
 {
-    int i;
+    unsigned i;
     for ( i = 0; i < pCut->nLeaves; i++ )
         pCut->pLeaves[i] = ((pCut->pLeaves[i] >> 8) << 8) | ((pCut->pLeaves[i] & 255) + 1);
 }
diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c
new file mode 100644
index 00000000..68affc4a
--- /dev/null
+++ b/src/map/if/ifTruth.c
@@ -0,0 +1,95 @@
+/**CFile****************************************************************
+
+  FileName    [ifTruth.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [FPGA mapping based on priority cuts.]
+
+  Synopsis    [Computation of truth tables of the cuts.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 21, 2006.]
+
+  Revision    [$Id: ifTruth.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "if.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the stretching phase of the cut w.r.t. the merged cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Cut_TruthPhase( If_Cut_t * pCut, If_Cut_t * pCut1 )
+{
+    unsigned uPhase = 0;
+    int i, k;
+    for ( i = k = 0; i < (int)pCut->nLeaves; i++ )
+    {
+        if ( k == (int)pCut1->nLeaves )
+            break;
+        if ( pCut->pLeaves[i] < pCut1->pLeaves[k] )
+            continue;
+        assert( pCut->pLeaves[i] == pCut1->pLeaves[k] );
+        uPhase |= (1 << i);
+        k++;
+    }
+    return uPhase;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs truth table computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 )
+{
+    // permute the first table
+    if ( fCompl0 ) 
+        Extra_TruthNot( p->puTemp[0], If_CutTruth(pCut0), pCut->nLimit );
+    else
+        Extra_TruthCopy( p->puTemp[0], If_CutTruth(pCut0), pCut->nLimit );
+    Extra_TruthStretch( p->puTemp[2], p->puTemp[0], pCut0->nLeaves, pCut->nLimit, Cut_TruthPhase(pCut, pCut0) );
+    // permute the second table
+    if ( fCompl1 ) 
+        Extra_TruthNot( p->puTemp[1], If_CutTruth(pCut1), pCut->nLimit );
+    else
+        Extra_TruthCopy( p->puTemp[1], If_CutTruth(pCut1), pCut->nLimit );
+    Extra_TruthStretch( p->puTemp[3], p->puTemp[1], pCut1->nLeaves, pCut->nLimit, Cut_TruthPhase(pCut, pCut1) );
+    // produce the resulting table
+    if ( pCut->fCompl )
+        Extra_TruthNand( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit );
+    else
+        Extra_TruthAnd( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/if/module.make b/src/map/if/module.make
index 362318da..b7d3185f 100644
--- a/src/map/if/module.make
+++ b/src/map/if/module.make
@@ -2,7 +2,8 @@ SRC +=  src/map/if/ifCore.c \
     src/map/if/ifCut.c \
     src/map/if/ifMan.c \
     src/map/if/ifMap.c \
+    src/map/if/ifPrepro.c \
     src/map/if/ifReduce.c \
-    src/map/if/ifSelect.c \
     src/map/if/ifSeq.c \
+    src/map/if/ifTruth.c \
     src/map/if/ifUtil.c