Version abc71218

27 files changed, 683 insertions, 99 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 03574655..6b34e853 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -160,6 +160,8 @@ struct Aig_Man_t_
 #define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
 #endif
 
+static inline int          Aig_Float2Int( float Val )             { return *((int *)&Val);                                 }
+static inline float        Aig_Int2Float( int Num )               { return *((float *)&Num);                               }
 static inline int          Aig_Base2Log( unsigned n )             { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }
 static inline int          Aig_Base10Log( unsigned n )            { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; }
 static inline char *       Aig_UtilStrsav( char * s )             { return s ? strcpy(ALLOC(char, strlen(s)+1), s) : NULL; }
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index c35e7121..48d29115 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -1,6 +1,8 @@
 SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigDfs.c \
     src/aig/aig/aigFanout.c \
+    src/aig/aig/aigFrames.c \
+    src/aig/aig/aigHaig.c \
     src/aig/aig/aigMan.c \
     src/aig/aig/aigMem.c \
     src/aig/aig/aigMffc.c \
@@ -10,8 +12,10 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigPart.c \
     src/aig/aig/aigRepr.c \
     src/aig/aig/aigRet.c \
+    src/aig/aig/aigRetF.c \
     src/aig/aig/aigScl.c \
     src/aig/aig/aigSeq.c \
+    src/aig/aig/aigShow.c \
     src/aig/aig/aigTable.c \
     src/aig/aig/aigTime.c \
     src/aig/aig/aigTiming.c \
diff --git a/src/aig/dar/darCut.c b/src/aig/dar/darCut.c
index 08bd77a9..b0aff095 100644
--- a/src/aig/dar/darCut.c
+++ b/src/aig/dar/darCut.c
@@ -479,7 +479,7 @@ static inline int Dar_CutSuppMinimize( Dar_Cut_t * pCut )
     unsigned uPhase = 0, uTruth = 0xFFFF & pCut->uTruth;
     int i, k, nLeaves;
     assert( pCut->fUsed );
-    // compute the truth support of the cut's function
+    // compute the support of the cut's function
     nLeaves = pCut->nLeaves;
     for ( i = 0; i < (int)pCut->nLeaves; i++ )
         if ( (uTruth & uMasks[i][0]) == ((uTruth & uMasks[i][1]) >> (1 << i)) )
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 8cd677d1..8d7116c7 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -76,6 +76,7 @@ struct Fra_Par_t_
     int              nFramesP;          // the number of timeframes to in the prefix
     int              nFramesK;          // the number of timeframes to unroll
     int              nMaxImps;          // the maximum number of implications to consider
+    int              nMaxLevs;          // the maximum number of levels to consider
     int              fRewrite;          // use rewriting for constraint reduction
     int              fLatchCorr;        // computes latch correspondence only
     int              fUseImps;          // use implications
@@ -245,7 +246,7 @@ extern Fra_Cla_t *         Fra_ClassesStart( Aig_Man_t * pAig );
 extern void                Fra_ClassesStop( Fra_Cla_t * p );
 extern void                Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed );
 extern void                Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose );
-extern void                Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr );
+extern void                Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs );
 extern int                 Fra_ClassesRefine( Fra_Cla_t * p );
 extern int                 Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped );
 extern int                 Fra_ClassesCountLits( Fra_Cla_t * p );
@@ -274,7 +275,7 @@ extern double              Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p );
 extern int                 Fra_ImpVerifyUsingSimulation( Fra_Man_t * p );
 extern void                Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew );
 /*=== fraInd.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter );
+extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter );
 /*=== fraLcr.c ========================================================*/
 extern Aig_Man_t *         Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter );
 /*=== fraMan.c ========================================================*/
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 962e7f7b..2d03e65d 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -270,7 +270,7 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
+void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
 {
     Aig_Obj_t ** ppTable, ** ppNexts;
     Aig_Obj_t * pObj, * pTemp;
@@ -296,8 +296,8 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
             if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
                 continue;
             // skip the node with more that the given number of levels
-//            if ( pObj->Level > 3 )
-//                continue;
+            if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
+                continue;
         }
         // hash the node by its simulation info
         iEntry = p->pFuncNodeHash( pObj, nTableSize );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index dbc6401f..1c2140bb 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -243,7 +243,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter )
 {
     int fUseSimpleCnf = 0;
     int fUseOldSimulation = 0;
@@ -282,12 +282,13 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
     pPars->nFramesP   = nFramesP;
     pPars->nFramesK   = nFramesK;
     pPars->nMaxImps   = nMaxImps;
+    pPars->nMaxLevs   = nMaxLevs;
     pPars->fVerbose   = fVerbose;
     pPars->fRewrite   = fRewrite;
     pPars->fLatchCorr = fLatchCorr;
     pPars->fUseImps   = fUseImps;
     pPars->fWriteImps = fWriteImps;
-
+ 
     // start the fraig manager for this run
     p = Fra_ManStart( pManAig, pPars );
     // derive and refine e-classes using K initialized frames
@@ -313,7 +314,7 @@ if ( fVerbose )
 {
 PRT( "Time", clock() - clk );
 }
-        Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
+        Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, p->pPars->nMaxLevs );
 //        Fra_ClassesPostprocess( p->pCla );
         // allocate new simulation manager for simulating counter-examples
         Fra_SmlStop( p->pSml );
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index daa789a8..a6460ed7 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -550,7 +550,7 @@ timeSim = clock() - clk2;
 
     // get preliminary info about equivalence classes
     pTemp->pCla = p->pCla = Fra_ClassesStart( p->pAig );
-    Fra_ClassesPrepare( p->pCla, 1 );
+    Fra_ClassesPrepare( p->pCla, 1, 0 );
     p->pCla->pFuncNodeIsConst   = Fra_LcrNodeIsConst;
     p->pCla->pFuncNodesAreEqual = Fra_LcrNodesAreEqual;
     Fra_SmlStop( pTemp->pSml );
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 17a7335c..4ccb48e3 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -49,7 +49,7 @@ int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
     {
         nFrames = nFramesFix;
         // perform seq sweeping for one frame number
-        pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
+        pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
     }
     else
     {
@@ -57,7 +57,7 @@ int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
         for ( nFrames = 1; ; nFrames++ )
         {
 clk = clock();
-            pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
+            pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
             RetValue = Fra_FraigMiterStatus( pNew );
             if ( fVerbose )
             {
@@ -185,7 +185,7 @@ PRT( "Time", clock() - clk );
     for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 )
     {
 clk = clock();
-        pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
+        pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
         Aig_ManStop( pTemp );
         RetValue = Fra_FraigMiterStatus( pNew );
         if ( fVerbose )
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index 3e8f2da1..1ad2d4f7 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -685,7 +685,7 @@ void Fra_SmlSimulate( Fra_Man_t * p, int fInit )
     Fra_SmlSimulateOne( p->pSml );
     if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
         return;
-    Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
+    Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, 0 );
 //    Fra_ClassesPrint( p->pCla, 0 );
 if ( fVerbose )
 printf( "Starting classes = %5d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
diff --git a/src/aig/fra/module.make b/src/aig/fra/module.make
index e7264fdc..ffaca75c 100644
--- a/src/aig/fra/module.make
+++ b/src/aig/fra/module.make
@@ -1,12 +1,15 @@
 SRC +=    src/aig/fra/fraBmc.c \
     src/aig/fra/fraCec.c \
     src/aig/fra/fraClass.c \
+    src/aig/fra/fraClau.c \
+    src/aig/fra/fraClaus.c \
     src/aig/fra/fraCnf.c \
     src/aig/fra/fraCore.c \
     src/aig/fra/fraImp.c \
     src/aig/fra/fraInd.c \
     src/aig/fra/fraLcr.c \
     src/aig/fra/fraMan.c \
+    src/aig/fra/fraPart.c \
     src/aig/fra/fraSat.c \
     src/aig/fra/fraSec.c \
     src/aig/fra/fraSim.c
diff --git a/src/aig/ntl/module.make b/src/aig/ntl/module.make
new file mode 100644
index 00000000..ea6070a4
--- /dev/null
+++ b/src/aig/ntl/module.make
@@ -0,0 +1,10 @@
+SRC +=    src/aig/mem/ntlAig.c \
+    src/aig/mem/ntlCheck.c \
+    src/aig/mem/ntlDfs.c \
+    src/aig/mem/ntlMan.c \
+    src/aig/mem/ntlMap.c \
+    src/aig/mem/ntlObj.c \
+    src/aig/mem/ntlReadBlif.c \
+    src/aig/mem/ntlTable.c \
+    src/aig/mem/ntlWriteBlif.c
+
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index e58047ae..af1e114d 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -86,6 +86,8 @@ struct Ntl_Mod_t_
     Ntl_Net_t **       pTable;         // the hash table of names into nets
     int                nTableSize;     // the allocated table size
     int                nEntries;       // the number of entries in the hash table
+    // delay information
+    Vec_Int_t *        vDelays;
 }; 
 
 struct Ntl_Obj_t_
@@ -242,6 +244,7 @@ extern char *          Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName );
 extern Ntl_Net_t *     Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName );
 extern Ntl_Net_t *     Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName );
 extern int             Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
+extern int             Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber );
 /*=== ntlReadBlif.c ==========================================================*/
 extern Ntl_Man_t *     Ioa_ReadBlif( char * pFileName, int fCheck );
 /*=== ntlWriteBlif.c ==========================================================*/
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index cc9bd029..6d71adb2 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -152,6 +152,7 @@ Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName )
 ***********************************************************************/
 void Ntl_ModelFree( Ntl_Mod_t * p )
 {
+    if ( p->vDelays ) Vec_IntFree( p->vDelays );
     Vec_PtrFree( p->vObjs );
     Vec_PtrFree( p->vPis );
     Vec_PtrFree( p->vPos );
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index feb8e488..7c6ed069 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -36,6 +36,7 @@ struct Ioa_ReadMod_t_
     Vec_Ptr_t *          vLatches;     // .latch lines
     Vec_Ptr_t *          vNames;       // .names lines
     Vec_Ptr_t *          vSubckts;     // .subckt lines
+    Vec_Ptr_t *          vDelays;      // .delay lines
     int                  fBlackBox;    // indicates blackbox model
     // the resulting network
     Ntl_Mod_t *          pNtk;   
@@ -79,6 +80,7 @@ static int               Ioa_ReadParseLineInputs( Ioa_ReadMod_t * p, char * pLin
 static int               Ioa_ReadParseLineOutputs( Ioa_ReadMod_t * p, char * pLine );
 static int               Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine );
 static int               Ioa_ReadParseLineSubckt( Ioa_ReadMod_t * p, char * pLine );
+static int               Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine );
 static int               Ioa_ReadParseLineNamesBlif( Ioa_ReadMod_t * p, char * pLine );
 
 static int               Ioa_ReadCharIsSpace( char s )   { return s == ' ' || s == '\t' || s == '\r' || s == '\n';             }
@@ -245,6 +247,7 @@ static Ioa_ReadMod_t * Ioa_ReadModAlloc()
     p->vLatches = Vec_PtrAlloc( 512 );
     p->vNames   = Vec_PtrAlloc( 512 );
     p->vSubckts = Vec_PtrAlloc( 512 );
+    p->vDelays  = Vec_PtrAlloc( 512 );
     return p;
 }
 
@@ -266,6 +269,7 @@ static void Ioa_ReadModFree( Ioa_ReadMod_t * p )
     Vec_PtrFree( p->vLatches );
     Vec_PtrFree( p->vNames );
     Vec_PtrFree( p->vSubckts );
+    Vec_PtrFree( p->vDelays );
     free( p );
 }
 
@@ -492,6 +496,8 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
             Vec_PtrPush( p->pLatest->vOutputs, pCur );
         else if ( !strncmp(pCur, "subckt", 6) )
             Vec_PtrPush( p->pLatest->vSubckts, pCur );
+        else if ( !strncmp(pCur, "delay", 5) )
+            Vec_PtrPush( p->pLatest->vDelays, pCur );
         else if ( !strncmp(pCur, "blackbox", 8) )
             p->pLatest->fBlackBox = 1;
         else if ( !strncmp(pCur, "model", 5) ) 
@@ -551,6 +557,10 @@ static void Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p )
         Vec_PtrForEachEntry( pMod->vOutputs, pLine, k )
             if ( !Ioa_ReadParseLineOutputs( pMod, pLine ) )
                 return;
+        // parse the delay info
+        Vec_PtrForEachEntry( pMod->vDelays, pLine, k )
+            if ( !Ioa_ReadParseLineDelay( pMod, pLine ) )
+                return;
     }
 }
 
@@ -841,6 +851,82 @@ static int Ioa_ReadParseLineSubckt( Ioa_ReadMod_t * p, char * pLine )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Parses the subckt line.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine )
+{
+    Vec_Ptr_t * vTokens = p->pMan->vTokens;
+    int RetValue1, RetValue2, Number1, Number2, Temp;
+    char * pToken;
+    float Delay;
+    assert( sizeof(float) == sizeof(int) );
+    Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
+    pToken = Vec_PtrEntry(vTokens,0);
+    assert( !strcmp(pToken, "delay") );
+    if ( Vec_PtrSize(vTokens) < 2 && Vec_PtrSize(vTokens) > 4 )
+    {
+        sprintf( p->pMan->sError, "Line %d: Delay line does not have a valid number of parameters (1, 2, or 3).", Ioa_ReadGetLine(p->pMan, pToken) );
+        return 0;
+    }
+    // find the delay number
+    Delay = atof( Vec_PtrEntryLast(vTokens) );
+    if ( Delay < 0.0 )
+    {
+        sprintf( p->pMan->sError, "Line %d: Delay value (%s) appears to be invalid.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntryLast(vTokens) );
+        return 0;
+    }
+    // find the PI/PO numbers
+    RetValue1 = 0; Number1 = -1;
+    if ( Vec_PtrSize(vTokens) > 2 )
+    {
+        RetValue1 = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 1), &Number1 );
+        if ( RetValue1 == 0 )
+        {
+            sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs/POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) );
+            return 0;
+        }
+    }
+    RetValue2 = 0; Number2 = -1;
+    if ( Vec_PtrSize(vTokens) > 3 )
+    {
+        RetValue2 = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 2), &Number2 );
+        if ( RetValue2 == 0 )
+        {
+            sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs/POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 2) );
+            return 0;
+        }
+    }
+    if ( RetValue1 == RetValue2 && RetValue1 )
+    {
+        sprintf( p->pMan->sError, "Line %d: Both signals \"%s\" and \"%s\" listed appear to be PIs or POs.", 
+            Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1), Vec_PtrEntry(vTokens, 2) );
+        return 0;
+    }
+    if ( RetValue2 < RetValue1 )
+    {
+        Temp = RetValue2; RetValue2 = RetValue1; RetValue1 = Temp;
+        Temp = Number2;   Number2 = Number1;     Number1 = Temp;
+    }
+    assert( RetValue1 == 0 || RetValue1 == -1 );
+    assert( RetValue2 == 0 || RetValue2 ==  1 );
+    // store the values
+    if ( p->pNtk->vDelays == NULL )
+        p->pNtk->vDelays = Vec_IntAlloc( 100 );
+    Vec_IntPush( p->pNtk->vDelays, Number1 );
+    Vec_IntPush( p->pNtk->vDelays, Number2 );
+    Vec_IntPush( p->pNtk->vDelays, Aig_Float2Int(Delay) );        
+    return 1;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/aig/ntl/ntlTable.c b/src/aig/ntl/ntlTable.c
index 87048f10..b84ac1a5 100644
--- a/src/aig/ntl/ntlTable.c
+++ b/src/aig/ntl/ntlTable.c
@@ -171,6 +171,45 @@ int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns -1, 0, +1 (when it is PI, not found, or PO).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber )
+{
+    Ntl_Net_t * pNet;
+    Ntl_Obj_t * pObj;
+    int i;
+    *pNumber = -1;
+    pNet = Ntl_ModelFindNet( p, pName );
+    if ( pNet == NULL )
+        return 0;
+    Ntl_ModelForEachPo( p, pObj, i )
+    {
+        if ( Ntl_ObjFanin0(pObj) == pNet )
+        {
+            *pNumber = i;
+            return 1;
+        }
+    }
+    Ntl_ModelForEachPi( p, pObj, i )
+    {
+        if ( Ntl_ObjFanout0(pObj) == pNet )
+        {
+            *pNumber = i;
+            return -1;
+        }
+    }
+    return 0;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 98dcde81..f4ad2eaf 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2865,9 +2865,9 @@ int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     pPars->nWindow      = 62;
-    pPars->nGrowthLevel =  1;
     pPars->nCands       =  5;
     pPars->nSimWords    =  4;
+    pPars->nGrowthLevel =  0;
     pPars->fArea        =  0;
     pPars->fVerbose     =  0;
     pPars->fVeryVerbose =  0;
@@ -2959,9 +2959,9 @@ usage:
     fprintf( pErr, "usage: imfs [-W <NM>] [-L <num>] [-C <num>] [-S <num>] [-avwh]\n" );
     fprintf( pErr, "\t           performs resubstitution-based resynthesis with interpolation\n" );
     fprintf( pErr, "\t-W <NM>  : fanin/fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
-    fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
     fprintf( pErr, "\t-C <num> : the max number of resub candidates (1 <= n) [default = %d]\n", pPars->nCands );
     fprintf( pErr, "\t-S <num> : the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords );
+    fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
     fprintf( pErr, "\t-a       : toggle optimization for area only [default = %s]\n", pPars->fArea? "yes": "no" );
     fprintf( pErr, "\t-v       : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w       : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
@@ -3103,7 +3103,9 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     fprintf( pErr, "usage: lutpack [-N <num>] [-Q <num>] [-S <num>] [-L <num>] [-szfovwh]\n" );
-    fprintf( pErr, "\t           performs \"rewriting\" for LUT networks\n" );
+    fprintf( pErr, "\t           performs \"rewriting\" for LUT networks;\n" );
+    fprintf( pErr, "\t           determines LUT size as the max fanin count of a node;\n" );
+    fprintf( pErr, "\t           if the network is not LUT-mapped, packs it into 6-LUTs\n" );
     fprintf( pErr, "\t-N <num> : the max number of LUTs in the structure (2 <= num) [default = %d]\n", pPars->nLutsMax );
     fprintf( pErr, "\t-Q <num> : the max number of LUTs not in MFFC (0 <= num) [default = %d]\n", pPars->nLutsOver );
     fprintf( pErr, "\t-S <num> : the max number of LUT inputs shared (0 <= num <= 3) [default = %d]\n", pPars->nVarsShared );
@@ -6220,8 +6222,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
-//    printf( "This command is temporarily disabled.\n" );
-//    return 0;
+    printf( "This command is temporarily disabled.\n" );
+    return 0;
 
     // set defaults
     fVeryVerbose = 0;
@@ -10019,13 +10021,15 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nFlowIters  =  1;
     pPars->nAreaIters  =  2;
     pPars->DelayTarget = -1;
-    pPars->fPreprocess =  1;//
+    pPars->fPreprocess =  1;
     pPars->fArea       =  0;
     pPars->fFancy      =  0;
-    pPars->fExpRed     =  1;//
+    pPars->fExpRed     =  1;
     pPars->fLatchPaths =  0;
+    pPars->fEdge       =  0;
+    pPars->fCutMin     =  0;
     pPars->fSeqMap     =  0;
-    pPars->fVerbose    =  0;//
+    pPars->fVerbose    =  0;
     // internal parameters
     pPars->fTruth      =  0;
     pPars->nLatches    =  pNtk? Abc_NtkLatchNum(pNtk) : 0;
@@ -10036,7 +10040,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->pFuncCost   =  NULL;   
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADpaflrstvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADpaflemrstvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -10103,14 +10107,20 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'a':
             pPars->fArea ^= 1;
             break;
+        case 'r':
+            pPars->fExpRed ^= 1;
+            break;
         case 'f':
             pPars->fFancy ^= 1;
             break;
         case 'l':
             pPars->fLatchPaths ^= 1;
             break;
-        case 'r':
-            pPars->fExpRed ^= 1;
+        case 'e':
+            pPars->fEdge ^= 1;
+            break;
+        case 'm':
+            pPars->fCutMin ^= 1;
             break;
         case 's':
             pPars->fSeqMap ^= 1;
@@ -10162,20 +10172,27 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
+    // enable truth table computation if choices are selected
     if ( Abc_NtkGetChoiceNum( pNtk ) )
     {
         printf( "Performing FPGA mapping with choices.\n" );
-//        printf( "Currently mapping with choices is not enabled.\n" );
         pPars->fTruth = 1;
-//        return 1;
     }
+    // enable truth table computation if cut minimization is selected
+    if ( pPars->fCutMin )
+        pPars->fTruth = 1;
 
+    // complain if truth tables are requested but the cut size is too large
     if ( pPars->fTruth && pPars->nLutSize > IF_MAX_FUNC_LUTSIZE )
     {
-        fprintf( pErr, "Mapping with choices requires computing truth tables. In this case, the LUT size cannot be more than %d.\n", IF_MAX_FUNC_LUTSIZE );
+        fprintf( pErr, "Truth tables cannot be computed for LUT larger than %d inputs.\n", IF_MAX_FUNC_LUTSIZE );
         return 1;
     }
 
+    // disable cut-expansion if edge-based heuristics are selected
+    if ( pPars->fEdge )
+        pPars->fExpRed = 0;
+
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         // strash and balance the network
@@ -10226,7 +10243,7 @@ usage:
         sprintf( LutSize, "library" );
     else
         sprintf( LutSize, "%d", pPars->nLutSize );
-    fprintf( pErr, "usage: if [-K num] [-C num] [-F num] [-A num] [-D float] [-pafrsvh]\n" );
+    fprintf( pErr, "usage: if [-K num] [-C num] [-F num] [-A num] [-D float] [-parlemsvh]\n" );
     fprintf( pErr, "\t           performs FPGA technology mapping of the network\n" );
     fprintf( pErr, "\t-K num   : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
     fprintf( pErr, "\t-C num   : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
@@ -10238,6 +10255,8 @@ usage:
 //    fprintf( pErr, "\t-f       : toggles one fancy feature [default = %s]\n", pPars->fFancy? "yes": "no" );
     fprintf( pErr, "\t-r       : enables expansion/reduction of the best cuts [default = %s]\n", pPars->fExpRed? "yes": "no" );
     fprintf( pErr, "\t-l       : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" );
+    fprintf( pErr, "\t-e       : uses edge-based cut selection heuristics [default = %s]\n", pPars->fEdge? "yes": "no" );
+    fprintf( pErr, "\t-m       : enables cut minimization by removing vacuous variables [default = %s]\n", pPars->fCutMin? "yes": "no" );
     fprintf( pErr, "\t-s       : toggles sequential mapping [default = %s]\n", pPars->fSeqMap? "yes": "no" );
 //    fprintf( pErr, "\t-t       : toggles the use of true sequential cuts [default = %s]\n", pPars->fLiftLeaves? "yes": "no" );
     fprintf( pErr, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
@@ -11227,12 +11246,13 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nFramesP;
     int nFramesK;
     int nMaxImps;
+    int nMaxLevs;
     int fUseImps;
     int fRewrite;
     int fLatchCorr;
     int fWriteImps;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -11242,13 +11262,14 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     nFramesP   = 0;
     nFramesK   = 1;
     nMaxImps   = 5000;
+    nMaxLevs   = 0;
     fUseImps   = 0;
     fRewrite   = 0;
     fLatchCorr = 0;
     fWriteImps = 0;
     fVerbose   = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PFIirlevh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PFILirlevh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -11285,6 +11306,17 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nMaxImps <= 0 ) 
                 goto usage;
             break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nMaxLevs = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nMaxLevs <= 0 ) 
+                goto usage;
+            break;
         case 'i':
             fUseImps ^= 1;
             break;
@@ -11326,7 +11358,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose );
+    pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential sweeping has failed.\n" );
@@ -11342,6 +11374,7 @@ usage:
     fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
     fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK );
     fprintf( pErr, "\t-I num : max number of implications to consider [default = %d]\n", nMaxImps );
+    fprintf( pErr, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", nMaxLevs );
     fprintf( pErr, "\t-i     : toggle using implications [default = %s]\n", fUseImps? "yes": "no" );
     fprintf( pErr, "\t-l     : toggle latch correspondence only [default = %s]\n", fLatchCorr? "yes": "no" );
     fprintf( pErr, "\t-r     : toggle AIG rewriting [default = %s]\n", fRewrite? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 62fc869c..3729fef8 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1022,7 +1022,7 @@ PRT( "Time", clock() - clkTotal );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose )
 {
     Fraig_Params_t Params;
     Abc_Ntk_t * pNtkAig, * pNtkFraig;
@@ -1046,7 +1046,7 @@ PRT( "Initial fraiging time", clock() - clk );
     if ( pMan == NULL )
         return NULL;
 
-    pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose, NULL );
+    pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose, NULL );
     Aig_ManStop( pTemp );
 
     if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index bfb380f3..4003a6d6 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -60,9 +60,9 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
 
     fprintf( pFile, "%-13s:",       pNtk->pName );
     if ( Abc_NtkAssertNum(pNtk) )
-        fprintf( pFile, " i/o/a = %4d/%4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk), Abc_NtkAssertNum(pNtk) );
+        fprintf( pFile, " i/o/a = %5d/%5d/%5d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk), Abc_NtkAssertNum(pNtk) );
     else
-        fprintf( pFile, " i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
+        fprintf( pFile, " i/o = %5d/%5d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
     fprintf( pFile, "  lat = %4d", Abc_NtkLatchNum(pNtk) );
     if ( Abc_NtkIsNetlist(pNtk) )
     {
@@ -86,7 +86,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     else 
     {
         fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
-        fprintf( pFile, "  net = %5d", Abc_NtkGetTotalFanins(pNtk) );
+        fprintf( pFile, "  edge = %6d", Abc_NtkGetTotalFanins(pNtk) );
     }
 
     if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsNetlist(pNtk) )
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                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index 8b8028e3..acea4866 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -446,10 +446,6 @@ p->timeTruth3 += clock() - clk;
 //            pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ );
 //            printf( "Saved truth table in file \"%s\".\n", pFileName );
         }
-        if ( p->pObj->Id == 33 && i == 0 )
-        {
-            int x = 0;
-        }
 
         // update the network
         nNodesBef = Abc_NtkNodeNum(p->pNtk);
@@ -512,6 +508,8 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
 
     // get the number of inputs
     pPars->nLutSize = Abc_NtkGetFaninMax( pNtk );
+    if ( pPars->nLutSize > 6 )
+        pPars->nLutSize = 6;
     // adjust the number of crossbars based on LUT size
     if ( pPars->nVarsShared > pPars->nLutSize - 2 )
         pPars->nVarsShared = pPars->nLutSize - 2;
diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c
index b2a743bd..facd330b 100644
--- a/src/opt/lpk/lpkCut.c
+++ b/src/opt/lpk/lpkCut.c
@@ -24,7 +24,7 @@
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
-
+ 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -489,7 +489,7 @@ void Lpk_NodeCutsOne( Lpk_Man_t * p, Lpk_Cut_t * pCut, int Node )
     if ( Abc_ObjIsCi(pObj) )
         return;
     assert( Abc_ObjIsNode(pObj) );
-    assert( Abc_ObjFaninNum(pObj) <= p->pPars->nLutSize );
+//    assert( Abc_ObjFaninNum(pObj) <= p->pPars->nLutSize );
 
     // if the node is not in the MFFC, check the limit
     if ( !Abc_NodeIsTravIdCurrent(pObj) )
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index 27e9b3ea..aa0eaeec 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -246,6 +246,8 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
         Extra_ProgressBarUpdate( pProgress, i, NULL );
         if ( !Abc_ObjIsNode(pObj) )
             continue;
+        if ( Abc_ObjFaninNum(pObj) > 8 )
+            continue;
         if ( pObj->Id > nNodesOld )
             break;