Version abc71218

6 files changed, 457 insertions, 56 deletions

diff --git a/src/map/if/if.h b/src/map/if/if.h
index 706f8552..3f3badf6 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -74,7 +74,7 @@ typedef struct If_Set_t_     If_Set_t;
 // parameters
 struct If_Par_t_
 {
-    // user-controlable paramters
+    // user-controlable parameters
     int                nLutSize;      // the LUT size
     int                nCutsMax;      // the max number of cuts
     int                nFlowIters;    // the number of iterations of area recovery
@@ -85,6 +85,8 @@ struct If_Par_t_
     int                fFancy;        // a fancy feature
     int                fExpRed;       // expand/reduce of the best cuts
     int                fLatchPaths;   // reset timing on latch paths
+    int                fEdge;         // uses edge-based cut selection heuristics
+    int                fCutMin;       // performs cut minimization by removing functionally reducdant variables
     int                fSeqMap;       // sequential mapping
     int                fVerbose;      // the verbosity flag
     // internal parameters
@@ -158,6 +160,7 @@ struct If_Man_t_
     If_Set_t *         pMemCi;        // memory for CI cutsets
     If_Set_t *         pMemAnd;       // memory for AND cutsets
     If_Set_t *         pFreeList;     // the list of free cutsets
+    int                nSmallSupp;    // the small support
 };
 
 // priority cut
@@ -166,6 +169,7 @@ struct If_Cut_t_
     float              Delay;         // delay of the cut
     float              Area;          // area (or area-flow) of the cut
     float              AveRefs;       // the average number of leaf references
+    float              Edge;          // the edge flow
     unsigned           uSign;         // cut signature
     unsigned           Cost    : 14;  // the user's cost of the cut
     unsigned           fCompl  :  1;  // the complemented attribute 
@@ -258,6 +262,7 @@ static inline void       If_CutSetData( If_Cut_t * pCut, void * pData )      { *
 
 static inline int        If_CutLeaveNum( If_Cut_t * pCut )                   { return pCut->nLeaves;                             }
 static inline unsigned * If_CutTruth( If_Cut_t * pCut )                      { return pCut->pTruth;                              }
+static inline unsigned   If_CutSuppMask( If_Cut_t * pCut )                   { return (~(unsigned)0) >> (32-pCut->nLeaves);      }
 static inline int        If_CutTruthWords( int nVarsMax )                    { return nVarsMax <= 5 ? 1 : (1 << (nVarsMax - 5)); }
 static inline int        If_CutPermWords( int nVarsMax )                     { return nVarsMax / sizeof(int) + ((nVarsMax % sizeof(int)) > 0); }
 
@@ -320,14 +325,19 @@ static inline float      If_CutLutArea( If_Man_t * p, If_Cut_t * pCut )      { r
 extern int             If_ManPerformMapping( If_Man_t * p );
 extern int             If_ManPerformMappingComb( If_Man_t * p );
 /*=== 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 );
-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 void            If_CutPrintTiming( If_Man_t * p, If_Cut_t * pCut );
-extern float           If_CutFlow( If_Man_t * p, If_Cut_t * pCut );
+extern float           If_CutAreaFlow( If_Man_t * p, If_Cut_t * pCut );
+extern float           If_CutEdgeFlow( If_Man_t * p, If_Cut_t * pCut );
 extern float           If_CutAverageRefs( If_Man_t * p, If_Cut_t * pCut );
+extern float           If_CutAreaDeref( If_Man_t * p, If_Cut_t * pCut );
+extern float           If_CutAreaRef( If_Man_t * p, If_Cut_t * pCut );
+extern float           If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut );
+extern float           If_CutAreaRefed( If_Man_t * p, If_Cut_t * pCut );
+extern float           If_CutEdgeDeref( If_Man_t * p, If_Cut_t * pCut );
+extern float           If_CutEdgeRef( If_Man_t * p, If_Cut_t * pCut );
+extern float           If_CutEdgeDerefed( If_Man_t * p, If_Cut_t * pCut );
+extern float           If_CutEdgeRefed( If_Man_t * p, If_Cut_t * pCut );
 extern int             If_CutFilter( If_Set_t * pCutSet, If_Cut_t * pCut );
 extern void            If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut );
 extern int             If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut );
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index 1a7ecc2c..915cedf9 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -28,7 +28,6 @@
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-
 /**Function*************************************************************
 
   Synopsis    [Returns 1 if pDom is contained in pCut.]
@@ -438,6 +437,83 @@ static inline int If_ManSortCompare( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC
             return -1;
         if ( pC0->Area > pC1->Area + 0.0001 )
             return 1;
+        if ( pC0->Edge < pC1->Edge - 0.0001 )
+            return -1;
+        if ( pC0->Edge > pC1->Edge + 0.0001 )
+            return 1;
+        if ( pC0->AveRefs > pC1->AveRefs )
+            return -1;
+        if ( pC0->AveRefs < pC1->AveRefs )
+            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;
+    }
+    if ( p->SortMode == 0 ) // delay
+    {
+        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;
+        if ( pC0->Edge < pC1->Edge - 0.0001 )
+            return -1;
+        if ( pC0->Edge > pC1->Edge + 0.0001 )
+            return 1;
+        return 0;
+    }
+    assert( p->SortMode == 2 ); // delay old
+    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->Edge < pC1->Edge - 0.0001 )
+        return -1;
+    if ( pC0->Edge > pC1->Edge + 0.0001 )
+        return 1;
+    if ( pC0->nLeaves < pC1->nLeaves )
+        return -1;
+    if ( pC0->nLeaves > pC1->nLeaves )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison function for two cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int If_ManSortCompare_old( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC1 )
+{
+    if ( p->SortMode == 1 ) // area
+    {
+        if ( pC0->Area < pC1->Area - 0.0001 )
+            return -1;
+        if ( pC0->Area > pC1->Area + 0.0001 )
+            return 1;
         if ( pC0->AveRefs > pC1->AveRefs )
             return -1;
         if ( pC0->AveRefs < pC1->AveRefs )
@@ -529,6 +605,47 @@ void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut )
 
 /**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    [Prints one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_CutPrintTiming( If_Man_t * p, If_Cut_t * pCut )
+{
+    If_Obj_t * pLeaf;
+    unsigned i;
+    printf( "{" );
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+        printf( " %d(%.2f/%.2f)", pLeaf->Id, If_ObjCutBest(pLeaf)->Delay, pLeaf->Required );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes area flow.]
 
   Description []
@@ -538,7 +655,7 @@ void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-float If_CutFlow( If_Man_t * p, If_Cut_t * pCut )
+float If_CutAreaFlow( If_Man_t * p, If_Cut_t * pCut )
 {
     If_Obj_t * pLeaf;
     float Flow;
@@ -562,6 +679,39 @@ float If_CutFlow( If_Man_t * p, If_Cut_t * pCut )
 
 /**Function*************************************************************
 
+  Synopsis    [Computes area flow.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float If_CutEdgeFlow( If_Man_t * p, If_Cut_t * pCut )
+{
+    If_Obj_t * pLeaf;
+    float Flow;
+    int i;
+    assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+    Flow = pCut->nLeaves;
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+    {
+        if ( pLeaf->nRefs == 0 )
+            Flow += If_ObjCutBest(pLeaf)->Edge;
+        else if ( p->pPars->fSeqMap ) // seq
+            Flow += If_ObjCutBest(pLeaf)->Edge / pLeaf->nRefs;
+        else 
+        {
+            assert( pLeaf->EstRefs > p->fEpsilon );
+            Flow += If_ObjCutBest(pLeaf)->Edge / pLeaf->EstRefs;
+        }
+    }
+    return Flow;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Average number of references of the leaves.]
 
   Description []
@@ -582,6 +732,7 @@ float If_CutAverageRefs( If_Man_t * p, If_Cut_t * pCut )
     return ((float)nRefsTotal)/pCut->nLeaves;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Computes area of the first level.]
@@ -593,7 +744,7 @@ float If_CutAverageRefs( If_Man_t * p, If_Cut_t * pCut )
   SeeAlso     []
  
 ***********************************************************************/
-float If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels )
+float If_CutAreaDeref( If_Man_t * p, If_Cut_t * pCut )
 {
     If_Obj_t * pLeaf;
     float Area;
@@ -602,9 +753,9 @@ float If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels )
     If_CutForEachLeaf( p, pCut, pLeaf, i )
     {
         assert( pLeaf->nRefs > 0 );
-        if ( --pLeaf->nRefs > 0 || !If_ObjIsAnd(pLeaf) || nLevels == 1 )
+        if ( --pLeaf->nRefs > 0 || !If_ObjIsAnd(pLeaf) )
             continue;
-        Area += If_CutDeref( p, If_ObjCutBest(pLeaf), nLevels - 1 );
+        Area += If_CutAreaDeref( p, If_ObjCutBest(pLeaf) );
     }
     return Area;
 }
@@ -620,7 +771,7 @@ float If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels )
   SeeAlso     []
 
 ***********************************************************************/
-float If_CutRef( If_Man_t * p, If_Cut_t * pCut, int nLevels )
+float If_CutAreaRef( If_Man_t * p, If_Cut_t * pCut )
 {
     If_Obj_t * pLeaf;
     float Area;
@@ -629,52 +780,83 @@ float If_CutRef( If_Man_t * p, If_Cut_t * pCut, int nLevels )
     If_CutForEachLeaf( p, pCut, pLeaf, i )
     {
         assert( pLeaf->nRefs >= 0 );
-        if ( pLeaf->nRefs++ > 0 || !If_ObjIsAnd(pLeaf) || nLevels == 1 )
+        if ( pLeaf->nRefs++ > 0 || !If_ObjIsAnd(pLeaf) )
             continue;
-        Area += If_CutRef( p, If_ObjCutBest(pLeaf), nLevels - 1 );
+        Area += If_CutAreaRef( p, If_ObjCutBest(pLeaf) );
     }
     return Area;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Prints one cut.]
+  Synopsis    [Computes area of the first level.]
 
-  Description []
+  Description [The cut need to be derefed.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void If_CutPrint( If_Man_t * p, If_Cut_t * pCut )
+float If_CutAreaDerefed( 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" );
+    float aResult, aResult2;
+    assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+    aResult2 = If_CutAreaRef( p, pCut );
+    aResult  = If_CutAreaDeref( p, pCut );
+    assert( aResult > aResult2 - p->fEpsilon );
+    assert( aResult < aResult2 + p->fEpsilon );
+    return aResult;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Prints one cut.]
+  Synopsis    [Computes area of the first level.]
 
-  Description []
+  Description [The cut need to be derefed.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void If_CutPrintTiming( If_Man_t * p, If_Cut_t * pCut )
+float If_CutAreaRefed( If_Man_t * p, If_Cut_t * pCut )
+{
+    float aResult, aResult2;
+    assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+    aResult2 = If_CutAreaDeref( p, pCut );
+    aResult  = If_CutAreaRef( p, pCut );
+    assert( aResult > aResult2 - p->fEpsilon );
+    assert( aResult < aResult2 + p->fEpsilon );
+    return aResult;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area of the first level.]
+
+  Description [The cut need to be derefed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+float If_CutEdgeDeref( If_Man_t * p, If_Cut_t * pCut )
 {
     If_Obj_t * pLeaf;
-    unsigned i;
-    printf( "{" );
+    float Edge;
+    int i;
+    Edge = pCut->nLeaves;
     If_CutForEachLeaf( p, pCut, pLeaf, i )
-        printf( " %d(%.2f/%.2f)", pLeaf->Id, If_ObjCutBest(pLeaf)->Delay, pLeaf->Required );
-    printf( " }\n" );
+    {
+        assert( pLeaf->nRefs > 0 );
+        if ( --pLeaf->nRefs > 0 || !If_ObjIsAnd(pLeaf) )
+            continue;
+        Edge += If_CutEdgeDeref( p, If_ObjCutBest(pLeaf) );
+    }
+    return Edge;
 }
 
 /**Function*************************************************************
@@ -688,12 +870,39 @@ void If_CutPrintTiming( If_Man_t * p, If_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-float If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut, int nLevels )
+float If_CutEdgeRef( If_Man_t * p, If_Cut_t * pCut )
+{
+    If_Obj_t * pLeaf;
+    float Edge;
+    int i;
+    Edge = pCut->nLeaves;
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+    {
+        assert( pLeaf->nRefs >= 0 );
+        if ( pLeaf->nRefs++ > 0 || !If_ObjIsAnd(pLeaf) )
+            continue;
+        Edge += If_CutEdgeRef( p, If_ObjCutBest(pLeaf) );
+    }
+    return Edge;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes edge of the first level.]
+
+  Description [The cut need to be derefed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float If_CutEdgeDerefed( If_Man_t * p, If_Cut_t * pCut )
 {
     float aResult, aResult2;
     assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
-    aResult2 = If_CutRef( p, pCut, nLevels );
-    aResult  = If_CutDeref( p, pCut, nLevels );
+    aResult2 = If_CutEdgeRef( p, pCut );
+    aResult  = If_CutEdgeDeref( p, pCut );
     assert( aResult > aResult2 - p->fEpsilon );
     assert( aResult < aResult2 + p->fEpsilon );
     return aResult;
@@ -710,17 +919,18 @@ float If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut, int nLevels )
   SeeAlso     []
 
 ***********************************************************************/
-float If_CutAreaRefed( If_Man_t * p, If_Cut_t * pCut, int nLevels )
+float If_CutEdgeRefed( If_Man_t * p, If_Cut_t * pCut )
 {
     float aResult, aResult2;
     assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
-    aResult2 = If_CutDeref( p, pCut, nLevels );
-    aResult  = If_CutRef( p, pCut, nLevels );
+    aResult2 = If_CutEdgeDeref( p, pCut );
+    aResult  = If_CutEdgeRef( p, pCut );
     assert( aResult > aResult2 - p->fEpsilon );
     assert( aResult < aResult2 + p->fEpsilon );
     return aResult;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Moves the cut over the latch.]
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index b713d80d..50ce63e9 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -124,6 +124,7 @@ void If_ManRestart( If_Man_t * p )
 ***********************************************************************/
 void If_ManStop( If_Man_t * p )
 {
+//    printf( "Small support = %d.\n", p->nSmallSupp );
     Vec_PtrFree( p->vCis );
     Vec_PtrFree( p->vCos );
     Vec_PtrFree( p->vObjs );
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 06ed4d1e..7228480a 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -77,7 +77,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
             pObj->EstRefs = (float)((2.0 * pObj->EstRefs + pObj->nRefs) / 3.0);
     }
     if ( Mode && pObj->nRefs > 0 )
-        If_CutDeref( p, If_ObjCutBest(pObj), IF_INFINITY );
+        If_CutAreaDeref( p, If_ObjCutBest(pObj) );
 
     // prepare the cutset
     pCutSet = If_ManSetupNodeCutSet( p, pObj );
@@ -89,7 +89,9 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
         // recompute the parameters of the best cut
         pCut->Delay = If_CutDelay( p, pCut );
         assert( pCut->Delay <= pObj->Required + p->fEpsilon );
-        pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, IF_INFINITY ) : If_CutFlow( p, pCut );
+        pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut ) : If_CutAreaFlow( p, pCut );
+        if ( p->pPars->fEdge )
+            pCut->Edge = (Mode == 2)? If_CutEdgeDerefed( p, pCut ) : If_CutEdgeFlow( p, pCut );
         // save the best cut from the previous iteration
         if ( !fPreprocess )
             If_CutCopy( p, pCutSet->ppCuts[pCutSet->nCuts++], pCut );
@@ -129,7 +131,9 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
         if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon )
             continue;
         // compute area of the cut (this area may depend on the application specific cost)
-        pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, IF_INFINITY ) : If_CutFlow( p, pCut );
+        pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut ) : If_CutAreaFlow( p, pCut );
+        if ( p->pPars->fEdge )
+            pCut->Edge = (Mode == 2)? If_CutEdgeDerefed( p, pCut ) : If_CutEdgeFlow( p, pCut );
         pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut );
         // insert the cut into storage
         If_CutSort( p, pCutSet, pCut );
@@ -147,7 +151,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
 
     // ref the selected cut
     if ( Mode && pObj->nRefs > 0 )
-        If_CutRef( p, If_ObjCutBest(pObj), IF_INFINITY );
+        If_CutAreaRef( p, If_ObjCutBest(pObj) );
 
     // call the user specified function for each cut
     if ( p->pPars->pFuncUser )
@@ -179,7 +183,7 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP
 
     // prepare
     if ( Mode && pObj->nRefs > 0 )
-        If_CutDeref( p, If_ObjCutBest(pObj), IF_INFINITY );
+        If_CutAreaDeref( p, If_ObjCutBest(pObj) );
 
     // remove elementary cuts
     for ( pTemp = pObj; pTemp; pTemp = pTemp->pEquiv )
@@ -213,7 +217,9 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP
             assert( pCut->fCompl == 0 );
             pCut->fCompl ^= (pObj->fPhase ^ pTemp->fPhase); // why ^= ?
             // compute area of the cut (this area may depend on the application specific cost)
-            pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, IF_INFINITY ) : If_CutFlow( p, pCut );
+            pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut ) : If_CutAreaFlow( p, pCut );
+            if ( p->pPars->fEdge )
+                pCut->Edge = (Mode == 2)? If_CutEdgeDerefed( p, pCut ) : If_CutEdgeFlow( p, pCut );
             pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut );
             // insert the cut into storage
             If_CutSort( p, pCutSet, pCut );
@@ -232,7 +238,7 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP
 
     // ref the selected cut
     if ( Mode && pObj->nRefs > 0 )
-        If_CutRef( p, If_ObjCutBest(pObj), IF_INFINITY );
+        If_CutAreaRef( p, If_ObjCutBest(pObj) );
 
     // free the cuts
     If_ManDerefChoiceCutSet( p, pObj );
diff --git a/src/map/if/ifReduce.c b/src/map/if/ifReduce.c
index 5dfda661..ab7de609 100644
--- a/src/map/if/ifReduce.c
+++ b/src/map/if/ifReduce.c
@@ -156,17 +156,17 @@ void If_ManImproveNodeExpand( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr
     // get the delay
     DelayOld = pCut->Delay;
     // get the area
-    AreaBef = If_CutAreaRefed( p, pCut, IF_INFINITY );
+    AreaBef = If_CutAreaRefed( p, pCut );
 //    if ( AreaBef == 1 )
 //        return;
     // the cut is non-trivial
     If_ManImproveNodePrepare( p, pObj, nLimit, vFront, vFrontOld, vVisited );
     // iteratively modify the cut
-    If_CutDeref( p, pCut, IF_INFINITY );
+    If_CutAreaDeref( p, pCut );
     CostBef = If_ManImproveCutCost( p, vFront );
     If_ManImproveNodeFaninCompact( p, pObj, nLimit, vFront, vVisited );
     CostAft = If_ManImproveCutCost( p, vFront );
-    If_CutRef( p, pCut, IF_INFINITY );
+    If_CutAreaRef( p, pCut );
     assert( CostBef >= CostAft );
     // clean up
     Vec_PtrForEachEntry( vVisited, pFanin, i )
@@ -175,11 +175,11 @@ void If_ManImproveNodeExpand( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr
     If_ManImproveNodeUpdate( p, pObj, vFront );
     pCut->Delay = If_CutDelay( p, pCut );
     // get the new area
-    AreaAft = If_CutAreaRefed( p, pCut, IF_INFINITY );
+    AreaAft = If_CutAreaRefed( p, pCut );
     if ( AreaAft > AreaBef || pCut->Delay > pObj->Required + p->fEpsilon )
     {
         If_ManImproveNodeUpdate( p, pObj, vFrontOld );
-        AreaAft = If_CutAreaRefed( p, pCut, IF_INFINITY );
+        AreaAft = If_CutAreaRefed( p, pCut );
         assert( AreaAft == AreaBef );
         pCut->Delay = DelayOld;
     }
@@ -257,13 +257,13 @@ void If_ManImproveNodeUpdate( If_Man_t * p, If_Obj_t * pObj, Vec_Ptr_t * vFront
     int i;
     pCut = If_ObjCutBest(pObj);
     // deref node's cut
-    If_CutDeref( p, pCut, IF_INFINITY );
+    If_CutAreaDeref( p, pCut );
     // update the node's cut
     pCut->nLeaves = Vec_PtrSize(vFront);
     Vec_PtrForEachEntry( vFront, pFanin, i )
         pCut->pLeaves[i] = pFanin->Id;
     // ref the new cut
-    If_CutRef( p, pCut, IF_INFINITY );
+    If_CutAreaRef( p, pCut );
 }
 
 
@@ -507,9 +507,9 @@ void If_ManImproveNodeReduce( If_Man_t * p, If_Obj_t * pObj, int nLimit )
 
     // deref the cut if the node is refed
     if ( pObj->nRefs > 0 )
-        If_CutDeref( p, pCut, IF_INFINITY );
+        If_CutAreaDeref( p, pCut );
     // get the area
-    AreaBef = If_CutAreaDerefed( p, pCut, IF_INFINITY );
+    AreaBef = If_CutAreaDerefed( p, pCut );
     // get the fanin support
     if ( pFanin0->nRefs > 2 && pCut0->Delay < pObj->Required + p->fEpsilon )
 //    if ( pSupp0->nRefs > 0 && pSupp0->Delay < pSupp->DelayR ) // this leads to 2% worse results
@@ -535,7 +535,7 @@ void If_ManImproveNodeReduce( If_Man_t * p, If_Obj_t * pObj, int nLimit )
     if ( RetValue )
     {
         pCutR->Delay = If_CutDelay( p, pCutR );
-        AreaAft = If_CutAreaDerefed( p, pCutR, IF_INFINITY );
+        AreaAft = If_CutAreaDerefed( p, pCutR );
         // update the best cut
         if ( AreaAft < AreaBef - p->fEpsilon && pCutR->Delay < pObj->Required + p->fEpsilon )
             If_CutCopy( p, pCut, pCutR );
@@ -544,7 +544,7 @@ void If_ManImproveNodeReduce( If_Man_t * p, If_Obj_t * pObj, int nLimit )
     pCut->Delay = If_CutDelay( p, pCut );
     // ref the cut if the node is refed
     if ( pObj->nRefs > 0 )
-        If_CutRef( p, pCut, IF_INFINITY );
+        If_CutRef( p, pCut );
 */
 }
 
diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c
index 5587e3ff..f18d8308 100644
--- a/src/map/if/ifTruth.c
+++ b/src/map/if/ifTruth.c
@@ -24,6 +24,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static int If_CutTruthMinimize( If_Man_t * p, If_Cut_t * pCut );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -158,6 +160,123 @@ void If_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll,
 
 /**Function*************************************************************
 
+  Synopsis    [Shrinks the truth table according to the phase.]
+
+  Description [The input and output truth tables are in pIn/pOut. The current number
+  of variables is nVars. The total number of variables in nVarsAll. The last argument
+  (Phase) contains shows what variables should remain.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn )
+{
+    unsigned * pTemp;
+    int i, k, Var = 0, Counter = 0;
+    for ( i = 0; i < nVarsAll; i++ )
+        if ( Phase & (1 << i) )
+        {
+            for ( k = i-1; k >= Var; k-- )
+            {
+                If_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
+                pTemp = pIn; pIn = pOut; pOut = pTemp;
+                Counter++;
+            }
+            Var++;
+        }
+    assert( Var == nVars );
+    // swap if it was moved an even number of times
+    if ( fReturnIn ^ !(Counter & 1) )
+        If_TruthCopy( pOut, pIn, nVarsAll );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if TT depends on the given variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_CutTruthVarInSupport( unsigned * pTruth, int nVars, int iVar )
+{
+    int nWords = If_TruthWordNum( nVars );
+    int i, k, Step;
+
+    assert( iVar < nVars );
+    switch ( iVar )
+    {
+    case 0:
+        for ( i = 0; i < nWords; i++ )
+            if ( (pTruth[i] & 0x55555555) != ((pTruth[i] & 0xAAAAAAAA) >> 1) )
+                return 1;
+        return 0;
+    case 1:
+        for ( i = 0; i < nWords; i++ )
+            if ( (pTruth[i] & 0x33333333) != ((pTruth[i] & 0xCCCCCCCC) >> 2) )
+                return 1;
+        return 0;
+    case 2:
+        for ( i = 0; i < nWords; i++ )
+            if ( (pTruth[i] & 0x0F0F0F0F) != ((pTruth[i] & 0xF0F0F0F0) >> 4) )
+                return 1;
+        return 0;
+    case 3:
+        for ( i = 0; i < nWords; i++ )
+            if ( (pTruth[i] & 0x00FF00FF) != ((pTruth[i] & 0xFF00FF00) >> 8) )
+                return 1;
+        return 0;
+    case 4:
+        for ( i = 0; i < nWords; i++ )
+            if ( (pTruth[i] & 0x0000FFFF) != ((pTruth[i] & 0xFFFF0000) >> 16) )
+                return 1;
+        return 0;
+    default:
+        Step = (1 << (iVar - 5));
+        for ( k = 0; k < nWords; k += 2*Step )
+        {
+            for ( i = 0; i < Step; i++ )
+                if ( pTruth[i] != pTruth[Step+i] )
+                    return 1;
+            pTruth += 2*Step;
+        }
+        return 0;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns support of the function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned If_CutTruthSupport( unsigned * pTruth, int nVars, int * pnSuppSize )
+{
+    int i, Support = 0;
+    int nSuppSize = 0;
+    for ( i = 0; i < nVars; i++ )
+        if ( If_CutTruthVarInSupport( pTruth, nVars, i ) )
+        {
+            Support |= (1 << i);
+            nSuppSize++;
+        }
+    *pnSuppSize = nSuppSize;
+    return Support;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Computes the stretching phase of the cut w.r.t. the merged cut.]
 
   Description []
@@ -197,7 +316,7 @@ static inline unsigned If_CutTruthPhase( If_Cut_t * pCut, If_Cut_t * pCut1 )
 ***********************************************************************/
 void If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 )
 {
-    extern void Kit_FactorTest( unsigned * pTruth, int nVars );
+    extern void If_CutFactorTest( unsigned * pTruth, int nVars );
 
     // permute the first table
     if ( fCompl0 ^ pCut0->fCompl ) 
@@ -218,11 +337,66 @@ void If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut
     else
         If_TruthAnd( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit );
 
+    // minimize the support of the cut
+    if ( p->pPars->fCutMin )
+        If_CutTruthMinimize( p, pCut );
+
     // perform 
-//    Kit_FactorTest( If_CutTruth(pCut), pCut->nLimit );
-//    printf( "%d ", If_CutLeaveNum(pCut) - Kit_TruthSupportSize(If_CutTruth(pCut), If_CutLeaveNum(pCut)) );
+//    If_CutFactorTest( If_CutTruth(pCut), pCut->nLimit );
+//    printf( "%d ", If_CutLeaveNum(pCut) - If_CutTruthSupportSize(If_CutTruth(pCut), If_CutLeaveNum(pCut)) );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Minimize support of the cut.]
+
+  Description [Returns 1 if the node's support has changed]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_CutTruthMinimize( If_Man_t * p, If_Cut_t * pCut )
+{
+    unsigned uSupport;
+    int nSuppSize, i, k;
+    // compute the support of the cut's function
+    uSupport = If_CutTruthSupport( If_CutTruth(pCut), If_CutLeaveNum(pCut), &nSuppSize );
+    if ( nSuppSize == If_CutLeaveNum(pCut) )
+        return 0;
+
+// TEMPORARY
+    if ( nSuppSize < 2 )
+    {
+        p->nSmallSupp++;
+        return 0;
+    }
+//    if ( If_CutLeaveNum(pCut) - nSuppSize > 1 )
+//        return 0;
+//printf( "%d %d  ", If_CutLeaveNum(pCut), nSuppSize );
+
+    // shrink the truth table
+    If_TruthShrink( p->puTemp[0], If_CutTruth(pCut), nSuppSize, pCut->nLimit, uSupport, 1 );
+    // update leaves and signature
+    pCut->uSign = 0;
+    for ( i = k = 0; i < If_CutLeaveNum(pCut); i++ )
+    {
+        if ( !(uSupport & (1 << i)) )
+            continue;    
+        pCut->pLeaves[k++] = pCut->pLeaves[i];
+        pCut->uSign |= If_ObjCutSign( pCut->pLeaves[i] );
+    }
+    assert( k == nSuppSize );
+    pCut->nLeaves = nSuppSize;
+    // verify the result
+//    uSupport = If_CutTruthSupport( If_CutTruth(pCut), If_CutLeaveNum(pCut), &nSuppSize );
+//    assert( nSuppSize == If_CutLeaveNum(pCut) );
+    return 1;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////