Version abc61204

18 files changed, 2060 insertions, 90 deletions

diff --git a/Makefile b/Makefile
index 3b37b2e6..d0951197 100644
--- a/Makefile
+++ b/Makefile
@@ -7,9 +7,9 @@ CP   := cp
 PROG := abc
 
 MODULES := src/base/abc src/base/abci src/base/cmd src/base/io src/base/main src/base/ver \
-	src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco src/mem/deco src/aig/ec \
+	src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco src/aig/mem src/aig/ec \
 	src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr src/bdd/parse src/bdd/reo \
-	src/map/fpga src/map/pga src/map/mapper src/map/mio src/map/super src/map/if \
+	src/map/fpga src/map/mapper src/map/mio src/map/super src/map/if \
 	src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/espresso src/misc/nm src/misc/vec src/misc/hash \
 	src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/sim src/opt/ret \
 	src/sat/asat src/sat/bsat src/sat/csat src/sat/msat src/sat/fraig 	
diff --git a/abc.dsp b/abc.dsp
index c94c0e6d..12161a33 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -1826,6 +1826,18 @@ SOURCE=.\src\map\if\ifMap.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\map\if\ifReduce.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\if\ifSelect.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\if\ifSeq.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\map\if\ifUtil.c
 # End Source File
 # End Group
diff --git a/src/aig/aig-alan.tar.gz b/src/aig/aig-alan.tar.gz
deleted file mode 100644
index b61827ad..00000000
--- a/src/aig/aig-alan.tar.gz
+++ /dev/null
diff --git a/src/aig/ivy/ivyFactor.c b/src/aig/ivy/ivyFactor.c
new file mode 100644
index 00000000..d8323931
--- /dev/null
+++ b/src/aig/ivy/ivyFactor.c
@@ -0,0 +1,833 @@
+/**CFile****************************************************************
+
+  FileName    [ivyFactor.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Factoring the cover up to 16 inputs.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyFactor.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+#include "dec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern Dec_Edge_t  Dec_Factor32_rec( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars );
+extern Dec_Edge_t  Dec_Factor32LF_rec( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars, Vec_Int_t * vSimple );
+extern Dec_Edge_t  Dec_Factor32Trivial( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars );
+extern Dec_Edge_t  Dec_Factor32TrivialCube( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars, Mvc_Cube_t * pCube, Vec_Int_t * vEdgeLits );
+extern Dec_Edge_t  Dec_Factor32TrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr );
+extern Vec_Int_t * Dec_Factor32Divisor( Vec_Int_t * vCover, int nVars );
+extern void        Dec_Factor32DivisorZeroKernel( Vec_Int_t * vCover, int nVars );
+extern int         Dec_Factor32WorstLiteral( Vec_Int_t * vCover, int nVars );
+
+extern Vec_Int_t * Mvc_CoverCommonCubeCover( Vec_Int_t * vCover );
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Factors the cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Graph_t * Dec_Factor32( Vec_Int_t * vCover, int nVars )
+{
+    Dec_Graph_t * pFForm;
+    Dec_Edge_t eRoot;
+
+    // check for trivial functions
+    if ( Vec_IntSize(vCover) == 0 )
+        return Dec_GraphCreateConst0();
+    if ( Vec_IntSize(vCover) == 1 && /* tautology */ )
+        return Dec_GraphCreateConst1();
+
+    // perform CST
+    Mvc_CoverInverse( vCover ); // CST
+    // start the factored form
+    pFForm = Dec_GraphCreate( Abc_SopGetVarNum(pSop) );
+    // factor the cover
+    eRoot = Dec_Factor32_rec( pFForm, vCover, nVars );
+    // finalize the factored form
+    Dec_GraphSetRoot( pFForm, eRoot );
+    // verify the factored form
+//    if ( !Dec_Factor32Verify( pSop, pFForm ) )
+//        printf( "Verification has failed.\n" );
+//    Mvc_CoverInverse( vCover ); // undo CST
+    return pFForm;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Internal recursive factoring procedure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Edge_t Dec_Factor32_rec( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars )
+{
+    Vec_Int_t * vDiv, * vQuo, * vRem, * vCom;
+    Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem;
+    Dec_Edge_t eNodeAnd, eNode;
+
+    // make sure the cover contains some cubes
+    assert( Vec_IntSize(vCover) );
+
+    // get the divisor
+    vDiv = Dec_Factor32Divisor( vCover, nVars );
+    if ( vDiv == NULL )
+        return Dec_Factor32Trivial( pFForm, vCover, nVars );
+
+    // divide the cover by the divisor
+    Mvc_CoverDivideInternal( vCover, nVars, vDiv, &vQuo, &vRem );
+    assert( Vec_IntSize(vQuo) );
+
+    Vec_IntFree( vDiv );
+    Vec_IntFree( vRem );
+
+    // check the trivial case
+    if ( Vec_IntSize(vQuo) == 1 )
+    {
+        eNode = Dec_Factor32LF_rec( pFForm, vCover, nVars, vQuo );
+        Vec_IntFree( vQuo );
+        return eNode;
+    }
+
+    // make the quotient cube free
+    Mvc_CoverMakeCubeFree( vQuo );
+
+    // divide the cover by the quotient
+    Mvc_CoverDivideInternal( vCover, nVars, vQuo, &vDiv, &vRem );
+
+    // check the trivial case
+    if ( Mvc_CoverIsCubeFree( vDiv ) )
+    {
+        eNodeDiv = Dec_Factor32_rec( pFForm, vDiv );
+        eNodeQuo = Dec_Factor32_rec( pFForm, vQuo );
+        Vec_IntFree( vDiv );
+        Vec_IntFree( vQuo );
+        eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
+        if ( Vec_IntSize(vRem) == 0 )
+        {
+            Vec_IntFree( vRem );
+            return eNodeAnd;
+        }
+        else
+        {
+            eNodeRem = Dec_Factor32_rec( pFForm, vRem );
+            Vec_IntFree( vRem );
+            return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
+        }
+    }
+
+    // get the common cube
+    vCom = Mvc_CoverCommonCubeCover( vDiv );
+    Vec_IntFree( vDiv );
+    Vec_IntFree( vQuo );
+    Vec_IntFree( vRem );
+
+    // solve the simple problem
+    eNode = Dec_Factor32LF_rec( pFForm, vCover, nVars, vCom );
+    Vec_IntFree( vCom );
+    return eNode;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Internal recursive factoring procedure for the leaf case.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Edge_t Dec_Factor32LF_rec( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars, Vec_Int_t * vSimple )
+{
+    Dec_Man_t * pManDec = Abc_FrameReadManDec();
+    Vec_Int_t * vEdgeLits  = pManDec->vLits;
+    Vec_Int_t * vDiv, * vQuo, * vRem;
+    Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem;
+    Dec_Edge_t eNodeAnd;
+
+    // get the most often occurring literal
+    vDiv = Mvc_CoverBestLiteralCover( vCover, nVars, vSimple );
+    // divide the cover by the literal
+    Mvc_CoverDivideByLiteral( vCover, nVars, vDiv, &vQuo, &vRem );
+    // get the node pointer for the literal
+    eNodeDiv = Dec_Factor32TrivialCube( pFForm, vDiv, Mvc_CoverReadCubeHead(vDiv), vEdgeLits );
+    Vec_IntFree( vDiv );
+    // factor the quotient and remainder
+    eNodeQuo = Dec_Factor32_rec( pFForm, vQuo );
+    Vec_IntFree( vQuo );
+    eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
+    if ( Vec_IntSize(vRem) == 0 )
+    {
+        Vec_IntFree( vRem );
+        return eNodeAnd;
+    }
+    else
+    {
+        eNodeRem = Dec_Factor32_rec( pFForm, vRem );
+        Vec_IntFree( vRem );
+        return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
+    }
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Factoring the cover, which has no algebraic divisors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Edge_t Dec_Factor32Trivial( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars )
+{
+    Dec_Man_t * pManDec = Abc_FrameReadManDec();
+    Vec_Int_t * vEdgeCubes = pManDec->vCubes;
+    Vec_Int_t * vEdgeLits  = pManDec->vLits;
+    Mvc_Manager_t * pMem = pManDec->pMvcMem;
+    Dec_Edge_t eNode;
+    Mvc_Cube_t * pCube;
+    int i;
+    // create the factored form for each cube
+    Vec_IntClear( vEdgeCubes );
+    Mvc_CoverForEachCube( vCover, pCube )
+    {
+        eNode = Dec_Factor32TrivialCube( pFForm, vCover, nVars, pCube, vEdgeLits );
+        Vec_IntPush( vEdgeCubes, Dec_EdgeToInt_(eNode) );
+    }
+    // balance the factored forms
+    return Dec_Factor32TrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeCubes->pArray, vEdgeCubes->nSize, 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Factoring the cube.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Edge_t Dec_Factor32TrivialCube( Dec_Graph_t * pFForm, Vec_Int_t * vCover, Mvc_Cube_t * pCube, int nVars, Vec_Int_t * vEdgeLits )
+{
+    Dec_Edge_t eNode;
+    int iBit, Value;
+    // create the factored form for each literal
+    Vec_IntClear( vEdgeLits );
+    Mvc_CubeForEachBit( vCover, pCube, iBit, Value )
+        if ( Value )
+        {
+            eNode = Dec_EdgeCreate( iBit/2, iBit%2 ); // CST
+            Vec_IntPush( vEdgeLits, Dec_EdgeToInt_(eNode) );
+        }
+    // balance the factored forms
+    return Dec_Factor32TrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeLits->pArray, vEdgeLits->nSize, 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create the well-balanced tree of nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Edge_t Dec_Factor32TrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr )
+{
+    Dec_Edge_t eNode1, eNode2;
+    int nNodes1, nNodes2;
+
+    if ( nNodes == 1 )
+        return peNodes[0];
+
+    // split the nodes into two parts
+    nNodes1 = nNodes/2;
+    nNodes2 = nNodes - nNodes1;
+//    nNodes2 = nNodes/2;
+//    nNodes1 = nNodes - nNodes2;
+
+    // recursively construct the tree for the parts
+    eNode1 = Dec_Factor32TrivialTree_rec( pFForm, peNodes,           nNodes1, fNodeOr );
+    eNode2 = Dec_Factor32TrivialTree_rec( pFForm, peNodes + nNodes1, nNodes2, fNodeOr );
+
+    if ( fNodeOr )
+        return Dec_GraphAddNodeOr( pFForm, eNode1, eNode2 );
+    else
+        return Dec_GraphAddNodeAnd( pFForm, eNode1, eNode2 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the quick divisor of the cover.]
+
+  Description [Returns NULL, if there is not divisor other than
+  trivial.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Dec_Factor32Divisor( Vec_Int_t * vCover, int nVars )
+{
+    Vec_Int_t * pKernel;
+    if ( Vec_IntSize(vCover) <= 1 )
+        return NULL;
+    // allocate the literal array and count literals
+    if ( Mvc_CoverAnyLiteral( vCover, NULL ) == -1 )
+        return NULL;
+    // duplicate the cover
+    pKernel = Mvc_CoverDup(vCover);
+    // perform the kerneling
+    Dec_Factor32DivisorZeroKernel( pKernel );
+    assert( Vec_IntSize(pKernel) );
+    return pKernel;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes a level-zero kernel.]
+
+  Description [Modifies the cover to contain one level-zero kernel.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dec_Factor32DivisorZeroKernel( Vec_Int_t * vCover, int nVars )
+{
+    int iLit;
+    // find any literal that occurs at least two times
+//    iLit = Mvc_CoverAnyLiteral( vCover, NULL );
+    iLit = Dec_Factor32WorstLiteral( vCover, NULL );
+//    iLit = Mvc_CoverBestLiteral( vCover, NULL );
+    if ( iLit == -1 )
+        return;
+    // derive the cube-free quotient
+    Mvc_CoverDivideByLiteralQuo( vCover, iLit ); // the same cover
+    Mvc_CoverMakeCubeFree( vCover );             // the same cover
+    // call recursively
+    Dec_Factor32DivisorZeroKernel( vCover );              // the same cover
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find the most often occurring literal.]
+
+  Description [Find the most often occurring literal among those
+  that occur more than once.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dec_Factor32WorstLiteral( Vec_Int_t * vCover, int nVars )
+{
+    Mvc_Cube_t * pCube;
+    int nWord, nBit;
+    int i, iMin, nLitsMin, nLitsCur;
+    int fUseFirst = 1;
+
+    // go through each literal
+    iMin = -1;
+    nLitsMin = 1000000;
+    for ( i = 0; i < vCover->nBits; i++ )
+    {
+        // get the word and bit of this literal
+        nWord = Mvc_CubeWhichWord(i);
+        nBit  = Mvc_CubeWhichBit(i);
+        // go through all the cubes
+        nLitsCur = 0;
+        Mvc_CoverForEachCube( vCover, pCube )
+            if ( pCube->pData[nWord] & (1<<nBit) )
+                nLitsCur++;
+
+        // skip the literal that does not occur or occurs once
+        if ( nLitsCur < 2 )
+            continue;
+
+        // check if this is the best literal
+        if ( fUseFirst )
+        {
+            if ( nLitsMin > nLitsCur )
+            {
+                nLitsMin = nLitsCur;
+                iMin = i;
+            }
+        }
+        else
+        {
+            if ( nLitsMin >= nLitsCur )
+            {
+                nLitsMin = nLitsCur;
+                iMin = i;
+            }
+        }
+    }
+
+    if ( nLitsMin < 1000000 )
+        return iMin;
+    return -1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Mvc_CoverCommonCubeCover( Vec_Int_t * vCover )
+{
+    Vec_Int_t * vRes;
+    unsigned uTemp, uCube;
+    int i;
+    uCube = ~(unsigned)0;
+    Vec_IntForEachEntry( vCover, uTemp, i )
+        uCube &= uTemp;
+    vRes = Vec_IntAlloc( 1 );
+    Vec_IntPush( vRes, uCube );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the support of cover2 is contained in the support of cover1.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CoverCheckSuppContainment( Vec_Int_t * vCover1, Vec_Int_t * vCover2 )
+{
+    unsigned uTemp, uSupp1, uSupp2;
+    int i;
+    // set the supports
+    uSupp1 = 0;
+    Vec_IntForEachEntry( vCover1, uTemp, i )
+        uSupp1 |= uTemp;
+    uSupp2 = 0;
+    Vec_IntForEachEntry( vCover2, uTemp, i )
+        uSupp2 |= uTemp;
+    // return containment
+    return uSupp1 & !uSupp2;
+//    Mvc_CubeBitNotImpl( Result, vCover2->pMask, vCover1->pMask );
+//    return !Result;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverDivide( Vec_Int_t * vCover, Vec_Int_t * vDiv, Vec_Int_t ** pvQuo, Vec_Int_t ** pvRem )
+{
+    // check the number of cubes
+    if ( Vec_IntSize( vCover ) < Vec_IntSize( vDiv ) )
+    {
+        *pvQuo = NULL;
+        *pvRem = NULL;
+        return;
+    }
+
+    // make sure that support of vCover contains that of vDiv
+    if ( !Mvc_CoverCheckSuppContainment( vCover, vDiv ) )
+    {
+        *pvQuo = NULL;
+        *pvRem = NULL;
+        return;
+    }
+
+    // perform the general division
+    Mvc_CoverDivideInternal( vCover, vDiv, pvQuo, pvRem );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Merge the cubes inside the groups.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverDivideInternal( Vec_Int_t * vCover, Vec_Int_t * vDiv, Vec_Int_t ** pvQuo, Vec_Int_t ** pvRem )
+{
+    Vec_Int_t * vQuo, * vRem;
+    Mvc_Cube_t * pCubeC, * pCubeD, * pCubeCopy;
+    Mvc_Cube_t * pCube1, * pCube2;
+    int * pGroups, nGroups;    // the cube groups
+    int nCubesC, nCubesD, nMerges, iCubeC, iCubeD, iMerge;
+    int fSkipG, GroupSize, g, c, RetValue;
+    int nCubes;
+
+    // get cover sizes
+    nCubesD = Vec_IntSize( vDiv );
+    nCubesC = Vec_IntSize( vCover );
+
+    // check trivial cases
+    if ( nCubesD == 1 )
+    {
+        if ( Mvc_CoverIsOneLiteral( vDiv ) )
+            Mvc_CoverDivideByLiteral( vCover, vDiv, pvQuo, pvRem );
+        else
+            Mvc_CoverDivideByCube( vCover, vDiv, pvQuo, pvRem );
+        return;
+    }
+
+    // create the divisor and the remainder 
+    vQuo = Mvc_CoverAlloc( vCover->pMem, vCover->nBits );
+    vRem = Mvc_CoverAlloc( vCover->pMem, vCover->nBits );
+
+    // get the support of the divisor
+    Mvc_CoverAllocateMask( vDiv );
+    Mvc_CoverSupport( vDiv, vDiv->pMask );
+
+    // sort the cubes of the divisor
+    Mvc_CoverSort( vDiv, NULL, Mvc_CubeCompareInt );
+    // sort the cubes of the cover
+    Mvc_CoverSort( vCover, vDiv->pMask, Mvc_CubeCompareIntOutsideAndUnderMask );
+
+    // allocate storage for cube groups
+    pGroups = MEM_ALLOC( vCover->pMem, int, nCubesC + 1 );
+
+    // mask contains variables in the support of Div
+    // split the cubes into groups using the mask
+    Mvc_CoverList2Array( vCover );
+    Mvc_CoverList2Array( vDiv );
+    pGroups[0] = 0;
+    nGroups    = 1;
+    for ( c = 1; c < nCubesC; c++ )
+    {
+        // get the cubes
+        pCube1 = vCover->pCubes[c-1];
+        pCube2 = vCover->pCubes[c  ];
+        // compare the cubes
+        Mvc_CubeBitEqualOutsideMask( RetValue, pCube1, pCube2, vDiv->pMask );
+        if ( !RetValue )
+            pGroups[nGroups++] = c;
+    }
+    // finish off the last group
+    pGroups[nGroups] = nCubesC;
+
+    // consider each group separately and decide
+    // whether it can produce a quotient cube
+    nCubes = 0;
+    for ( g = 0; g < nGroups; g++ )
+    {
+        // if the group has less than nCubesD cubes, 
+        // there is no way it can produce the quotient cube
+        // copy the cubes to the remainder
+        GroupSize = pGroups[g+1] - pGroups[g];
+        if ( GroupSize < nCubesD )
+        {
+            for ( c = pGroups[g]; c < pGroups[g+1]; c++ )
+            {
+                pCubeCopy = Mvc_CubeDup( vRem, vCover->pCubes[c] );
+                Mvc_CoverAddCubeTail( vRem, pCubeCopy );
+                nCubes++;
+            }
+            continue;
+        }
+
+        // mark the cubes as those that should be added to the remainder
+        for ( c = pGroups[g]; c < pGroups[g+1]; c++ )
+            Mvc_CubeSetSize( vCover->pCubes[c], 1 );
+
+        // go through the cubes in the group and at the same time
+        // go through the cubes in the divisor
+        iCubeD  = 0;
+        iCubeC  = 0;
+        pCubeD  = vDiv->pCubes[iCubeD++];
+        pCubeC  = vCover->pCubes[pGroups[g]+iCubeC++];
+        fSkipG  = 0;
+        nMerges = 0;
+
+        while ( 1 )
+        {
+            // compare the topmost cubes in F and in D
+            RetValue = Mvc_CubeCompareIntUnderMask( pCubeC, pCubeD, vDiv->pMask );
+            // cube are ordered in increasing order of their int value
+            if ( RetValue == -1 ) // pCubeC is above pCubeD
+            {  // cube in C should be added to the remainder
+                // check that there is enough cubes in the group
+                if ( GroupSize - iCubeC < nCubesD - nMerges )
+                {
+                    fSkipG = 1;
+                    break;
+                }
+                // get the next cube in the cover
+                pCubeC = vCover->pCubes[pGroups[g]+iCubeC++];
+                continue;
+            }
+            if ( RetValue == 1 ) // pCubeD is above pCubeC
+            { // given cube in D does not have a corresponding cube in the cover
+                fSkipG = 1;
+                break;
+            }
+            // mark the cube as the one that should NOT be added to the remainder
+            Mvc_CubeSetSize( pCubeC, 0 );
+            // remember this merged cube
+            iMerge = iCubeC-1;
+            nMerges++;
+
+            // stop if we considered the last cube of the group
+            if ( iCubeD == nCubesD )
+                break;
+
+            // advance the cube of the divisor
+            assert( iCubeD < nCubesD );
+            pCubeD = vDiv->pCubes[iCubeD++];
+
+            // advance the cube of the group
+            assert( pGroups[g]+iCubeC < nCubesC );
+            pCubeC = vCover->pCubes[pGroups[g]+iCubeC++];
+        }
+
+        if ( fSkipG )
+        { 
+            // the group has failed, add all the cubes to the remainder
+            for ( c = pGroups[g]; c < pGroups[g+1]; c++ )
+            {
+                pCubeCopy = Mvc_CubeDup( vRem, vCover->pCubes[c] );
+                Mvc_CoverAddCubeTail( vRem, pCubeCopy );
+                nCubes++;
+            }
+            continue;
+        }
+
+        // the group has worked, add left-over cubes to the remainder
+        for ( c = pGroups[g]; c < pGroups[g+1]; c++ )
+        {
+            pCubeC = vCover->pCubes[c];
+            if ( Mvc_CubeReadSize(pCubeC) )
+            {
+                pCubeCopy = Mvc_CubeDup( vRem, pCubeC );
+                Mvc_CoverAddCubeTail( vRem, pCubeCopy );
+                nCubes++;
+            }
+        }
+
+        // create the quotient cube
+        pCube1 = Mvc_CubeAlloc( vQuo );
+        Mvc_CubeBitSharp( pCube1, vCover->pCubes[pGroups[g]+iMerge], vDiv->pMask );
+        // add the cube to the quotient
+        Mvc_CoverAddCubeTail( vQuo, pCube1 );
+        nCubes += nCubesD;
+    }
+    assert( nCubes == nCubesC );
+
+    // deallocate the memory
+    MEM_FREE( vCover->pMem, int, nCubesC + 1, pGroups );
+
+    // return the results
+    *pvRem = vRem;
+    *pvQuo = vQuo;
+//    Mvc_CoverVerifyDivision( vCover, vDiv, vQuo, vRem );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Divides the cover by a cube.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverDivideByCube( Vec_Int_t * vCover, Vec_Int_t * vDiv, Vec_Int_t ** pvQuo, Vec_Int_t ** pvRem )
+{
+    Vec_Int_t * vQuo, * vRem;
+    Mvc_Cube_t * pCubeC, * pCubeD, * pCubeCopy;
+    int ComvResult;
+
+    // get the only cube of D
+    assert( Vec_IntSize(vDiv) == 1 );
+
+    // start the quotient and the remainder
+    vQuo = Mvc_CoverAlloc( vCover->pMem, vCover->nBits );
+    vRem = Mvc_CoverAlloc( vCover->pMem, vCover->nBits );
+
+    // get the first and only cube of the divisor
+    pCubeD = Mvc_CoverReadCubeHead( vDiv );
+
+    // iterate through the cubes in the cover
+    Mvc_CoverForEachCube( vCover, pCubeC )
+    {
+        // check the containment of literals from pCubeD in pCube
+        Mvc_Cube2BitNotImpl( ComvResult, pCubeD, pCubeC );
+        if ( !ComvResult )
+        { // this cube belongs to the quotient
+            // alloc the cube
+            pCubeCopy = Mvc_CubeAlloc( vQuo );
+            // clean the support of D
+            Mvc_CubeBitSharp( pCubeCopy, pCubeC, pCubeD );
+            // add the cube to the quotient
+            Mvc_CoverAddCubeTail( vQuo, pCubeCopy );
+        }
+        else
+        { 
+            // copy the cube
+            pCubeCopy = Mvc_CubeDup( vRem, pCubeC );
+            // add the cube to the remainder
+            Mvc_CoverAddCubeTail( vRem, pCubeCopy );
+        }
+    }
+    // return the results
+    *pvRem = vRem;
+    *pvQuo = vQuo;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Divides the cover by a literal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverDivideByLiteral( Vec_Int_t * vCover, Vec_Int_t * vDiv, Vec_Int_t ** pvQuo, Vec_Int_t ** pvRem )
+{
+    Vec_Int_t * vQuo, * vRem;
+    Mvc_Cube_t * pCubeC, * pCubeCopy;
+    int iLit;
+
+    // get the only cube of D
+    assert( Vec_IntSize(vDiv) == 1 );
+
+    // start the quotient and the remainder
+    vQuo = Mvc_CoverAlloc( vCover->pMem, vCover->nBits );
+    vRem = Mvc_CoverAlloc( vCover->pMem, vCover->nBits );
+
+    // get the first and only literal in the divisor cube
+    iLit = Mvc_CoverFirstCubeFirstLit( vDiv );
+
+    // iterate through the cubes in the cover
+    Mvc_CoverForEachCube( vCover, pCubeC )
+    {
+        // copy the cube
+        pCubeCopy = Mvc_CubeDup( vCover, pCubeC );
+        // add the cube to the quotient or to the remainder depending on the literal
+        if ( Mvc_CubeBitValue( pCubeCopy, iLit ) )
+        {   // remove the literal
+            Mvc_CubeBitRemove( pCubeCopy, iLit );
+            // add the cube ot the quotient
+            Mvc_CoverAddCubeTail( vQuo, pCubeCopy );
+        }
+        else
+        {   // add the cube ot the remainder
+            Mvc_CoverAddCubeTail( vRem, pCubeCopy );
+        }
+    }
+    // return the results
+    *pvRem = vRem;
+    *pvQuo = vQuo;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the quotient of division by literal.]
+
+  Description [Reduces the cover to be the equal to the result of
+  division of the given cover by the literal.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverDivideByLiteralQuo( Vec_Int_t * vCover, int iLit )
+{
+    Mvc_Cube_t * pCube, * pCube2, * pPrev;
+    // delete those cubes that do not have this literal
+    // remove this literal from other cubes
+    pPrev = NULL;
+    Mvc_CoverForEachCubeSafe( vCover, pCube, pCube2 )
+    {
+        if ( Mvc_CubeBitValue( pCube, iLit ) == 0 )
+        { // delete the cube from the cover
+            Mvc_CoverDeleteCube( vCover, pPrev, pCube );
+            Mvc_CubeFree( vCover, pCube );
+            // don't update the previous cube
+        }
+        else
+        { // delete this literal from the cube
+            Mvc_CubeBitRemove( pCube, iLit );
+            // update the previous cube
+            pPrev = pCube;
+        }
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/rwt/module.make b/src/aig/rwt/module.make
index 2852f2ba..439d576f 100644
--- a/src/aig/rwt/module.make
+++ b/src/aig/rwt/module.make
@@ -1,3 +1,3 @@
-SRC +=  src/hop/rwt/rwtDec.c \
-    src/hop/rwt/rwtMan.c \
-    src/hop/rwt/rwtUtil.c
+SRC +=  src/aig/rwt/rwtDec.c \
+    src/aig/rwt/rwtMan.c \
+    src/aig/rwt/rwtUtil.c
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4164f67a..dbbe9d7e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -7090,7 +7090,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     fRecovery   = 1;
     fSwitching  = 0;
     fLatchPaths = 0;
-    fVerbose    = 1;
+    fVerbose    = 0;
     DelayTarget =-1;
     nLutSize    =-1;
     Extra_UtilGetoptReset();
@@ -7392,18 +7392,20 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     memset( pPars, 0, sizeof(If_Par_t) );
     pPars->Mode        =  0;
-    pPars->nLutSize    =  5;
+    pPars->nLutSize    =  4;
 //    pPars->pLutLib    =  Abc_FrameReadLibLut();
-    pPars->nCutsMax    = 10;
+    pPars->nCutsMax    = 20;
+    pPars->fPreprocess =  1;
     pPars->fArea       =  0;
     pPars->fFancy      =  0;
     pPars->fLatchPaths =  0;
+    pPars->fExpRed     =  1;
     pPars->fSeq        =  0;
     pPars->nLatches    =  0;
     pPars->DelayTarget = -1;
-    pPars->fVerbose    =  1;
+    pPars->fVerbose    =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "MKCDaflsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MKCDpaflrsvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -7451,6 +7453,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->DelayTarget <= 0.0 ) 
                 goto usage;
             break;
+        case 'p':
+            pPars->fPreprocess ^= 1;
+            break;
         case 'a':
             pPars->fArea ^= 1;
             break;
@@ -7460,6 +7465,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'l':
             pPars->fLatchPaths ^= 1;
             break;
+        case 'r':
+            pPars->fExpRed ^= 1;
+            break;
         case 's':
             pPars->fSeq ^= 1;
             break;
@@ -7478,6 +7486,12 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
+    if ( pPars->fSeq )
+    {
+        fprintf( pErr, "Sequential mapping is currently being implemented.\n" );
+        goto usage;
+    }
+
     if ( pPars->Mode < 0 || pPars->Mode > 4 )
     {
         fprintf( pErr, "Incorrect mapping mode.\n" );
@@ -7547,7 +7561,7 @@ usage:
         sprintf( LutSize, "library" );
     else
         sprintf( LutSize, "%d", pPars->nLutSize );
-    fprintf( pErr, "usage: if [-M num] [-K num] [-C num] [-D float] [-aflsvh]\n" );
+    fprintf( pErr, "usage: if [-M num] [-K num] [-C num] [-D float] [-pafrsvh]\n" );
     fprintf( pErr, "\t           performs FPGA mapping of the network as follows:\n" );
     fprintf( pErr, "\t               1 - delay only\n" );
     fprintf( pErr, "\t               2 - area only\n" );
@@ -7557,9 +7571,11 @@ usage:
     fprintf( pErr, "\t-K num   : the number of LUT inputs (2 < num < 32) [default = %s]\n", LutSize );
     fprintf( pErr, "\t-C num   : the max number of cuts to use (1 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
     fprintf( pErr, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer );  
+    fprintf( pErr, "\t-p       : toggles preprocessing using several starting points [default = %s]\n", pPars->fPreprocess? "yes": "no" );
     fprintf( pErr, "\t-a       : toggles area-oriented mapping [default = %s]\n", pPars->fArea? "yes": "no" );
     fprintf( pErr, "\t-f       : toggles one fancy feature [default = %s]\n", pPars->fFancy? "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-l       : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" );
+    fprintf( pErr, "\t-r       : enables expansion/reduction of the best cuts [default = %s]\n", pPars->fExpRed? "yes": "no" );
     fprintf( pErr, "\t-s       : toggles sequential mapping [default = %s]\n", pPars->fSeq? "yes": "no" );
     fprintf( pErr, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h       : prints the command usage\n");
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 70971952..704c8ebb 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -55,7 +55,11 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
 
     // print a warning about choice nodes
     if ( Abc_NtkGetChoiceNum( pNtk ) )
-        printf( "Performing FPGA mapping with choices.\n" );
+    {
+//        printf( "Performing FPGA mapping with choices.\n" );
+        printf( "Currently mapping with choices is not enabled.\n" );
+        return NULL;
+    }
 
     // get timing information
     pPars->pTimesArr = Abc_NtkGetCiArrivalFloats(pNtk);
@@ -223,7 +227,6 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
     return pNodeNew;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Recursively derives the truth table for the cut.]
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 40bf30a6..002a885c 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -148,18 +148,18 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     // print the statistic into a file
     {
         FILE * pTable;
-        pTable = fopen( "fpga/fpga_stats.txt", "a+" );
+        pTable = fopen( "a/fpga_stats.txt", "a+" );
         fprintf( pTable, "%s ",  pNtk->pName );
         fprintf( pTable, "%d ", Abc_NtkLevel(pNtk) );
         fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) );
-        fprintf( pTable, "%.2f ", (float)(s_MappingMem)/(float)(1<<20) );
-        fprintf( pTable, "%.2f", (float)(s_MappingTime)/(float)(CLOCKS_PER_SEC) );
+//        fprintf( pTable, "%.2f ", (float)(s_MappingMem)/(float)(1<<20) );
+//        fprintf( pTable, "%.2f", (float)(s_MappingTime)/(float)(CLOCKS_PER_SEC) );
         fprintf( pTable, "\n" );
         fclose( pTable );
     }
 */
 
-
+/*
     // print the statistic into a file
     {
         static int Counter = 0;
@@ -176,6 +176,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
             fprintf( pTable, "\n" );
         fclose( pTable );
     }
+*/
 
 /*
     // print the statistic into a file
diff --git a/src/map/fpga/fpga.c b/src/map/fpga/fpga.c
index d7a128b0..d04c9910 100644
--- a/src/map/fpga/fpga.c
+++ b/src/map/fpga/fpga.c
@@ -57,8 +57,8 @@ void Fpga_Init( Abc_Frame_t * pAbc )
 {
     // set the default library
     //Fpga_LutLib_t s_LutLib = { "lutlib", 6, {0,1,2,4,8,16,32}, {0,1,2,3,4,5,6} };
-    Fpga_LutLib_t s_LutLib = { "lutlib", 5, {0,1,1,1,1,1}, {0,1,1,1,1,1} };
-//    Fpga_LutLib_t s_LutLib = { "lutlib", 4, {0,1,1,1,1}, {0,1,1,1,1} };
+//    Fpga_LutLib_t s_LutLib = { "lutlib", 5, {0,1,1,1,1,1}, {0,1,1,1,1,1} };
+    Fpga_LutLib_t s_LutLib = { "lutlib", 4, {0,1,1,1,1}, {0,1,1,1,1} };
     //Fpga_LutLib_t s_LutLib = { "lutlib", 3, {0,1,1,1}, {0,1,1,1} };
 
     Abc_FrameSetLibLut( Fpga_LutLibDup(&s_LutLib) );
diff --git a/src/map/if/if.h b/src/map/if/if.h
index a1d2d41b..31c07528 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -55,7 +55,7 @@ typedef enum {
     IF_BO,       // 6: box output
     IF_BOX,      // 7: box
     IF_VOID      // 8: unused object
-} Hop_Type_t;
+} If_Type_t;
 
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
@@ -75,8 +75,10 @@ struct If_Par_t_
     If_Lib_t *         pLutLib;       // the LUT library
     int                nCutsMax;      // the max number of cuts
     int                fVerbose;      // the verbosity flag
+    int                fPreprocess;   // preprossing
     int                fArea;         // area-oriented mapping
     int                fFancy;        // a fancy feature
+    int                fExpRed;       // expand/reduce of the best cuts
     int                fLatchPaths;   // reset timing on latch paths
     int                fSeq;          // sequential mapping
     int                nLatches;      // the number of latches
@@ -115,6 +117,7 @@ struct If_Man_t_
     int                nCutsUsed;     // the number of cuts currently used
     int                nCutsMerged;   // the total number of cuts merged
     int                nCutsMax;      // the maximum number of cuts at a node
+    float              Fi;            // the current value of the clock period (for seq mapping)
     // memory management
     Mem_Fixed_t *      pMem;          // memory manager
     int                nEntrySize;    // the size of the entry
@@ -127,15 +130,16 @@ struct If_Man_t_
 // priority cut
 struct If_Cut_t_
 {
-    float              Delay;         // the delay of the cut
-    float              Area;          // the area of the cut
-    If_Cut_t *         pOne;          // the parent cut
-    If_Cut_t *         pTwo;          // the parent cut
-    char               fCompl0;       // the complemented attribute
-    char               fCompl1;       // the complemented attribute
-    char               Phase;         // the complemented attribute
-    char               nLeaves;       // the number of leaves
-    int *              pLeaves;       // the array of fanins
+    float              Delay;         // delay of the cut
+    float              Area;          // area (or area-flow) of the cut
+    If_Cut_t *         pOne;          // parent cut
+    If_Cut_t *         pTwo;          // parent cut
+    unsigned           uSign;         // cut signature
+    char               fCompl0;       // complemented attribute
+    char               fCompl1;       // complemented attribute
+    char               Phase;         // complemented attribute
+    char               nLeaves;       // number of leaves
+    int *              pLeaves;       // array of fanins
 };
 
 // node extension
@@ -149,8 +153,7 @@ struct If_Obj_t_
     unsigned           Level   : 24;  // logic level of the node
     int                Id;            // integer ID
     int                nRefs;         // the number of references
-    short              nCuts;         // the number of cuts
-    short              iCut;          // the number of the best cut
+    int                nCuts;         // the number of cuts
     If_Obj_t *         pFanin0;       // the first fanin 
     If_Obj_t *         pFanin1;       // the second fanin
     If_Obj_t *         pEquiv;        // the choice node
@@ -188,7 +191,8 @@ static inline void       If_ObjSetChoice( If_Obj_t * pObj, If_Obj_t * pEqu ) { p
 
 static inline If_Cut_t * If_ObjCut( If_Obj_t * pObj, int iCut )              { return pObj->Cuts + iCut;             }
 static inline If_Cut_t * If_ObjCutTriv( If_Obj_t * pObj )                    { return pObj->Cuts;                    }
-static inline If_Cut_t * If_ObjCutBest( If_Obj_t * pObj )                    { return pObj->Cuts + pObj->iCut;       }
+static inline If_Cut_t * If_ObjCutBest( If_Obj_t * pObj )                    { return pObj->Cuts + 1;                }
+static inline unsigned   If_ObjCutSign( unsigned ObjId )                     { return (1 << (ObjId % 31));           }
 
 static inline void *     If_CutData( If_Cut_t * pCut )                       { return *(void **)pCut;                }
 static inline void       If_CutSetData( If_Cut_t * pCut, void * pData )      { *(void **)pCut = pData;               }
@@ -239,6 +243,7 @@ static inline float      If_CutLutArea( If_Man_t * p, If_Cut_t * pCut )      { r
 
 /*=== ifCore.c ==========================================================*/
 extern int             If_ManPerformMapping( If_Man_t * p );
+extern int             If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fRequired );
 /*=== ifMan.c ==========================================================*/
 extern If_Man_t *      If_ManStart( If_Par_t * pPars );
 extern void            If_ManStop( If_Man_t * p );
@@ -247,6 +252,19 @@ extern If_Obj_t *      If_ManCreatePo( If_Man_t * p, If_Obj_t * pDriver, int fCo
 extern If_Obj_t *      If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_t * pFan1, int fCompl1 );
 /*=== ifMap.c ==========================================================*/
 extern void            If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode );
+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 float           If_CutDelay( If_Man_t * p, If_Cut_t * pCut );
+extern float           If_CutFlow( If_Man_t * p, If_Cut_t * pCut );
+extern int             If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut, int nLimit );
+extern void            If_CutCopy( If_Cut_t * pCutDest, If_Cut_t * pCutSrc );
+/*=== ifReduce.c ==========================================================*/
+extern void            If_ManImproveMapping( If_Man_t * p );
+/*=== ifSelect.c ==========================================================*/
+extern void            If_ManPerformMappingPreprocess( If_Man_t * p );
 /*=== ifUtil.c ==========================================================*/
 extern float           If_ManDelayMax( If_Man_t * p );
 extern void            If_ManCleanNodeCopy( If_Man_t * p );
diff --git a/src/map/if/ifCore.c b/src/map/if/ifCore.c
index 37a22d8b..e139e14b 100644
--- a/src/map/if/ifCore.c
+++ b/src/map/if/ifCore.c
@@ -24,8 +24,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -44,7 +42,7 @@ static int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode );
 int If_ManPerformMapping( If_Man_t * p )
 {
     If_Obj_t * pObj;
-    int nItersFlow = 2;
+    int nItersFlow = 1;
     int nItersArea = 1;
     int clkTotal = clock();
     int i;
@@ -56,13 +54,27 @@ int If_ManPerformMapping( If_Man_t * p )
     If_ManForEachPi( p, pObj, i )
         pObj->EstRefs = (float)1.0;
     // delay oriented mapping
-    If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0 );
+    if ( p->pPars->fPreprocess && !p->pPars->fArea && p->pPars->nCutsMax >= 4  )
+        If_ManPerformMappingPreprocess( p );
+    else
+        If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 1 );
+    // try to improve area by expanding and reducing the cuts
+    if ( p->pPars->fExpRed )
+        If_ManImproveMapping( p );
     // area flow oriented mapping
     for ( i = 0; i < nItersFlow; i++ )
-        If_ManPerformMappingRound( p, p->pPars->nCutsMax, 1 );
+    {
+        If_ManPerformMappingRound( p, p->pPars->nCutsMax, 1, 1 );
+        if ( p->pPars->fExpRed )
+            If_ManImproveMapping( p );
+    }
     // area oriented mapping
     for ( i = 0; i < nItersArea; i++ )
-        If_ManPerformMappingRound( p, p->pPars->nCutsMax, 2 );
+    {
+        If_ManPerformMappingRound( p, p->pPars->nCutsMax, 2, 1 );
+        if ( p->pPars->fExpRed )
+            If_ManImproveMapping( p );
+    }
     if ( p->pPars->fVerbose )
     {
         PRT( "Total time", clock() - clkTotal );
@@ -81,7 +93,7 @@ int If_ManPerformMapping( If_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode )
+int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fRequired )
 {
     If_Obj_t * pObj;
     int i, clk = clock();
@@ -94,15 +106,18 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode )
     If_ManForEachNode( p, pObj, i )
         If_ObjPerformMapping( p, pObj, Mode );
     // compute required times and stats
-    If_ManComputeRequired( p, Mode==0 );
-    if ( p->pPars->fVerbose )
+    if ( fRequired )
     {
-        char Symb = (Mode == 0)? 'D' : ((Mode == 1)? 'F' : 'A');
-        printf( "%c:  Del = %6.2f. Area = %8.2f. Cuts = %6d. Lim = %2d. Ave = %5.2f. ", 
-            Symb, p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
-        PRT( "T", clock() - clk );
+        If_ManComputeRequired( p, Mode==0 );
+        if ( p->pPars->fVerbose )
+        {
+            char Symb = (Mode == 0)? 'D' : ((Mode == 1)? 'F' : 'A');
+            printf( "%c:  Del = %6.2f. Area = %8.2f. Cuts = %6d. Lim = %2d. Ave = %5.2f. ", 
+                Symb, p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
+            PRT( "T", clock() - clk );
 //    printf( "Max number of cuts = %d. Average number of cuts = %5.2f.\n", 
 //        p->nCutsMax, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
+        }
     }
     return 1;
 }
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index bc13c6f0..b0c12fea 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -191,6 +191,7 @@ If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_
 ***********************************************************************/
 If_Obj_t * If_ManSetupObj( If_Man_t * p )
 {
+    If_Cut_t * pCut;
     If_Obj_t * pObj;
     int i, * pArrays;
     // get memory for the object
@@ -204,10 +205,12 @@ If_Obj_t * If_ManSetupObj( If_Man_t * p )
     pObj->Id = Vec_PtrSize(p->vObjs);
     Vec_PtrPush( p->vObjs, pObj );
     // assign elementary cut
+    pCut = pObj->Cuts;
+    pCut->nLeaves    = 1;
+    pCut->pLeaves[0] = p->pPars->fSeq? (pObj->Id << 8) : pObj->Id;
+    pCut->uSign      = If_ObjCutSign( pCut->pLeaves[0] );
+    // set the number of cuts
     pObj->nCuts = 1;
-    pObj->Cuts[0].nLeaves    = 1;
-    pObj->Cuts[0].pLeaves[0] = pObj->Id;
-    pObj->iCut = 0;
     // set the required times
     pObj->Required = IF_FLOAT_LARGE;
     return pObj;
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 0b505062..9134dc9a 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -39,6 +39,26 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Counts the number of 1s in the signature.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int If_WordCountOnes( unsigned uWord )
+{
+    uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
+    uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
+    uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
+    uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
+    return  (uWord & 0x0000FFFF) + (uWord>>16);
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if pDom is contained in pCut.]
 
   Description []
@@ -95,7 +115,7 @@ static inline int If_CutCheckEquality( If_Cut_t * pDom, If_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-int If_CutFilter( If_Man_t * p, If_Cut_t * pCut )
+int If_CutFilter( If_Man_t * p, If_Cut_t * pCut, int Mode )
 {
     If_Cut_t * pTemp;
     int i;
@@ -103,21 +123,37 @@ int If_CutFilter( If_Man_t * p, If_Cut_t * pCut )
     {
         pTemp = p->ppCuts[i];
         if ( pTemp->nLeaves > pCut->nLeaves )
-            continue;
-        // skip the non-contained cuts
-//        if ( (pTemp->uSign & pCut->uSign) != pTemp->uSign )
+        {
 //            continue;
-        // check containment seriously
-        if ( If_CutCheckDominance( pTemp, pCut ) )
-//        if ( If_CutCheckEquality( pTemp, pCut ) )
-            return 1;
+            // skip the non-contained cuts
+            if ( (pTemp->uSign & pCut->uSign) != pCut->uSign )
+                continue;
+            // check containment seriously
+            if ( If_CutCheckDominance( pCut, pTemp ) )
+            {
+                // removed contained cut
+                p->ppCuts[i] = p->ppCuts[p->nCuts-1];
+                p->ppCuts[p->nCuts-1] = pTemp;
+                p->nCuts--;
+                i--;
+            }
+         }
+        else
+        {
+            // skip the non-contained cuts
+            if ( (pTemp->uSign & pCut->uSign) != pTemp->uSign )
+                continue;
+            // check containment seriously
+            if ( If_CutCheckDominance( pTemp, pCut ) )
+                return 1;
+        }
     }
     return 0;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Prepares the object for FPGA mapping.]
+  Synopsis    [Merges two cuts.]
 
   Description []
                
@@ -126,7 +162,7 @@ int If_CutFilter( If_Man_t * p, If_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-int If_CutMergeOrdered( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC, int nLimit )
+static inline int If_CutMergeOrdered( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC, int nLimit )
 { 
     int i, k, c;
     assert( pC0->nLeaves >= pC1->nLeaves );
@@ -203,6 +239,58 @@ int If_CutMergeOrdered( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC, int nLimi
 
 /**Function*************************************************************
 
+  Synopsis    [Merges two cuts.]
+
+  Description [Special case when the cut is known to exist.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int If_CutMergeOrdered2( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC, int nLimit )
+{ 
+    int i, k, c;
+    assert( pC0->nLeaves >= pC1->nLeaves );
+    // copy the first cut
+    for ( i = 0; i < pC0->nLeaves; i++ )
+        pC->pLeaves[i] = pC0->pLeaves[i];
+    pC->nLeaves = pC0->nLeaves;
+    // the case when one of the cuts is the largest
+    if ( pC0->nLeaves == nLimit )
+        return 1;
+    // add nodes of the second cut
+    k = 0;
+    for ( i = 0; i < pC1->nLeaves; i++ )
+    {
+        // find k-th node before which i-th node should be added
+        for ( ; k < pC->nLeaves; k++ )
+            if ( pC->pLeaves[k] >= pC1->pLeaves[i] )
+                break;
+        // check the case when this should be the last node
+        if ( k == pC->nLeaves )
+        {
+            pC->pLeaves[k++] = pC1->pLeaves[i];
+            pC->nLeaves++;
+            continue;
+        }
+        // check the case when equal node is found
+        if ( pC1->pLeaves[i] == pC->pLeaves[k] )
+            continue;
+        // add the node
+        for ( c = pC->nLeaves; c > k; c-- )
+            pC->pLeaves[c] = pC->pLeaves[c-1];
+        pC->pLeaves[k++] = pC1->pLeaves[i];
+        pC->nLeaves++;
+    }
+    assert( pC->nLeaves <= nLimit );
+    for ( i = 1; i < pC->nLeaves; i++ )
+        assert( pC->pLeaves[i-1] < pC->pLeaves[i] );
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Prepares the object for FPGA mapping.]
 
   Description []
@@ -212,7 +300,7 @@ int If_CutMergeOrdered( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC, int nLimi
   SeeAlso     []
 
 ***********************************************************************/
-static inline int If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut, int nLimit )
+int If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut, int nLimit )
 { 
     // merge the nodes
     if ( pCut0->nLeaves < pCut1->nLeaves )
@@ -243,17 +331,17 @@ int If_CutCompareDelay( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
 {
     If_Cut_t * pC0 = *ppC0;
     If_Cut_t * pC1 = *ppC1;
-    if ( pC0->Delay < pC1->Delay )
+    if ( pC0->Delay < pC1->Delay - 0.0001 )
         return -1;
-    if ( pC0->Delay > pC1->Delay )
+    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 )
+    if ( pC0->Area < pC1->Area - 0.0001 )
         return -1;
-    if ( pC0->Area > pC1->Area )
+    if ( pC0->Area > pC1->Area + 0.0001 )
         return 1;
     return 0;
 }
@@ -273,13 +361,13 @@ int If_CutCompareDelayOld( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
 {
     If_Cut_t * pC0 = *ppC0;
     If_Cut_t * pC1 = *ppC1;
-    if ( pC0->Delay < pC1->Delay )
+    if ( pC0->Delay < pC1->Delay - 0.0001 )
         return -1;
-    if ( pC0->Delay > pC1->Delay )
+    if ( pC0->Delay > pC1->Delay + 0.0001 )
         return 1;
-    if ( pC0->Area < pC1->Area )
+    if ( pC0->Area < pC1->Area - 0.0001 )
         return -1;
-    if ( pC0->Area > pC1->Area )
+    if ( pC0->Area > pC1->Area + 0.0001 )
         return 1;
     if ( pC0->nLeaves < pC1->nLeaves )
         return -1;
@@ -303,17 +391,17 @@ int If_CutCompareArea( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
 {
     If_Cut_t * pC0 = *ppC0;
     If_Cut_t * pC1 = *ppC1;
-    if ( pC0->Area < pC1->Area )
+    if ( pC0->Area < pC1->Area - 0.0001 )
         return -1;
-    if ( pC0->Area > pC1->Area )
+    if ( pC0->Area > pC1->Area + 0.0001 )
         return 1;
     if ( pC0->nLeaves < pC1->nLeaves )
         return -1;
     if ( pC0->nLeaves > pC1->nLeaves )
         return 1;
-    if ( pC0->Delay < pC1->Delay )
+    if ( pC0->Delay < pC1->Delay - 0.0001 )
         return -1;
-    if ( pC0->Delay > pC1->Delay )
+    if ( pC0->Delay > pC1->Delay + 0.0001 )
         return 1;
     return 0;
 }
@@ -405,7 +493,7 @@ float If_CutFlow( If_Man_t * p, If_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-float If_CutRef( If_Man_t * p, If_Cut_t * pCut, int nLevels )
+float If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels )
 {
     If_Obj_t * pLeaf;
     float Area;
@@ -413,10 +501,10 @@ float If_CutRef( If_Man_t * p, If_Cut_t * pCut, int nLevels )
     Area = If_CutLutArea(p, pCut);
     If_CutForEachLeaf( p, pCut, pLeaf, i )
     {
-        assert( pLeaf->nRefs >= 0 );
-        if ( pLeaf->nRefs++ > 0 || !If_ObjIsAnd(pLeaf) || nLevels == 1 )
+        assert( pLeaf->nRefs > 0 );
+        if ( --pLeaf->nRefs > 0 || !If_ObjIsAnd(pLeaf) || nLevels == 1 )
             continue;
-        Area += If_CutRef( p, If_ObjCutBest(pLeaf), nLevels - 1 );
+        Area += If_CutDeref( p, If_ObjCutBest(pLeaf), nLevels - 1 );
     }
     return Area;
 }
@@ -432,7 +520,7 @@ float If_CutRef( If_Man_t * p, If_Cut_t * pCut, int nLevels )
   SeeAlso     []
 
 ***********************************************************************/
-float If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels )
+float If_CutRef( If_Man_t * p, If_Cut_t * pCut, int nLevels )
 {
     If_Obj_t * pLeaf;
     float Area;
@@ -440,16 +528,36 @@ float If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels )
     Area = If_CutLutArea(p, pCut);
     If_CutForEachLeaf( p, pCut, pLeaf, i )
     {
-        assert( pLeaf->nRefs > 0 );
-        if ( --pLeaf->nRefs > 0 || !If_ObjIsAnd(pLeaf) || nLevels == 1 )
+        assert( pLeaf->nRefs >= 0 );
+        if ( pLeaf->nRefs++ > 0 || !If_ObjIsAnd(pLeaf) || nLevels == 1 )
             continue;
-        Area += If_CutDeref( p, If_ObjCutBest(pLeaf), nLevels - 1 );
+        Area += If_CutRef( p, If_ObjCutBest(pLeaf), nLevels - 1 );
     }
     return Area;
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Prints one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_CutPrint( If_Man_t * p, If_Cut_t * pCut )
+{
+    int i;
+    printf( "{" );
+    for ( i = 0; i < pCut->nLeaves; i++ )
+        printf( " %d", pCut->pLeaves[i] );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes area of the first level.]
 
   Description [The cut need to be derefed.]
@@ -459,7 +567,7 @@ float If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels )
   SeeAlso     []
 
 ***********************************************************************/
-float If_CutArea( If_Man_t * p, If_Cut_t * pCut, int nLevels )
+float If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut, int nLevels )
 {
     float aResult, aResult2;
     assert( pCut->nLeaves > 1 );
@@ -480,6 +588,27 @@ float If_CutArea( 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 aResult, aResult2;
+    assert( pCut->nLeaves > 1 );
+    aResult2 = If_CutDeref( p, pCut, nLevels );
+    aResult  = If_CutRef( p, pCut, nLevels );
+    assert( aResult == aResult2 );
+    return aResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area of the first level.]
+
+  Description [The cut need to be derefed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void If_CutCopy( If_Cut_t * pCutDest, If_Cut_t * pCutSrc )
 {
     int * pArray;
@@ -503,7 +632,7 @@ void If_CutCopy( If_Cut_t * pCutDest, If_Cut_t * pCutSrc )
 void If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode )
 {
     If_Cut_t * pCut0, * pCut1, * pCut;
-    int i, k;
+    int i, k, iCut;
 
     // prepare
     if ( Mode == 0 )
@@ -521,17 +650,22 @@ void If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode )
         pCut = If_ObjCutBest(pObj);
         pCut->Delay = If_CutDelay( p, pCut );
         assert( pCut->Delay <= pObj->Required + p->fEpsilon );
-        pCut->Area  = (Mode == 2)? If_CutArea( p, pCut, 100 ) : If_CutFlow( p, pCut );
+        pCut->Area  = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut );
         // save the best cut from the previous iteration
         If_CutCopy( p->ppCuts[p->nCuts++], pCut );
         p->nCutsMerged++;
     }
 
+    // prepare room for the next cut
+    iCut = p->nCuts;
+    pCut = p->ppCuts[iCut];
     // generate cuts
-    pCut = p->ppCuts[p->nCuts];
     If_ObjForEachCut( pObj->pFanin0, pCut0, i )
     If_ObjForEachCut( pObj->pFanin1, pCut1, k )
     {
+        // make sure K-feasible cut exists
+        if ( If_WordCountOnes(pCut0->uSign | pCut1->uSign) > p->pPars->nLutSize )
+            continue;
         // prefilter using arrival times
         if ( Mode && (pCut0->Delay > pObj->Required + p->fEpsilon || pCut1->Delay > pObj->Required + p->fEpsilon) )
             continue;
@@ -539,7 +673,8 @@ void If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode )
         if ( !If_CutMerge( pCut0, pCut1, pCut, p->pPars->nLutSize ) )
             continue;
         // check if this cut is contained in any of the available cuts
-        if ( If_CutFilter( p, pCut ) )
+        pCut->uSign = pCut0->uSign | pCut1->uSign;
+        if ( If_CutFilter( p, pCut, Mode ) )
             continue;
         // check if the cut satisfies the required times
         pCut->Delay = If_CutDelay( p, pCut );
@@ -549,18 +684,26 @@ void If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode )
         pCut->pOne = pCut0; pCut->fCompl0 = pObj->fCompl0;
         pCut->pTwo = pCut1; pCut->fCompl1 = pObj->fCompl1;
 //        pCut->Phase = ...
-        pCut->Area  = (Mode == 2)? If_CutArea( p, pCut, 100 ) : If_CutFlow( p, pCut );
+//        pCut->Phase = (char)(int)If_CutAreaDerefed( p, pCut, 1 );
+        pCut->Area  = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut );
         p->nCutsMerged++;
+        // make sure the cut is the last one (after filtering it may not be so)
+        assert( pCut == p->ppCuts[iCut] );
+        p->ppCuts[iCut] = p->ppCuts[p->nCuts];
+        p->ppCuts[p->nCuts] = pCut;
         // prepare room for the next cut
-        pCut = p->ppCuts[++p->nCuts];
+        iCut = ++p->nCuts;
+        pCut = p->ppCuts[iCut];
     } 
+//printf( "%d  ", p->nCuts );
     assert( p->nCuts > 0 );
+    // sort if we have more cuts
     If_ManSortCuts( p, Mode );
-    // take the first
+    // decide how many cuts to use
     pObj->nCuts = IF_MIN( p->nCuts + 1, p->nCutsUsed );
+    // take the first
     If_ObjForEachCutStart( pObj, pCut, i, 1 )
         If_CutCopy( pCut, p->ppCuts[i-1] );
-    pObj->iCut = 1;
     assert( If_ObjCutBest(pObj)->nLeaves > 1 );
     // assign delay of the trivial cut
     If_ObjCutTriv(pObj)->Delay = If_ObjCutBest(pObj)->Delay;
diff --git a/src/map/if/ifReduce.c b/src/map/if/ifReduce.c
new file mode 100644
index 00000000..5c8da0d0
--- /dev/null
+++ b/src/map/if/ifReduce.c
@@ -0,0 +1,576 @@
+/**CFile****************************************************************
+
+  FileName    [ifExpand.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [FPGA mapping based on priority cuts.]
+
+  Synopsis    [Incremental improvement of current mapping.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 21, 2006.]
+
+  Revision    [$Id: ifExpand.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "if.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void If_ManImproveReduce( If_Man_t * p, int nLimit );
+static void If_ManImproveExpand( If_Man_t * p, int nLimit );
+static void If_ManImproveNodeExpand( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vFrontOld, Vec_Ptr_t * vVisited );
+static void If_ManImproveNodePrepare( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vFrontOld, Vec_Ptr_t * vVisited );
+static void If_ManImproveNodeUpdate( If_Man_t * p, If_Obj_t * pObj, Vec_Ptr_t * vFront );
+static void If_ManImproveNodeFaninCompact( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Improves current mapping using expand/Expand of one cut.]
+
+  Description [Assumes current mapping assigned and required times computed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManImproveMapping( If_Man_t * p )
+{
+    int clk;
+
+    clk = clock();
+    If_ManImproveExpand( p, p->pPars->nLutSize );
+    If_ManComputeRequired( p, 0 );
+    if ( p->pPars->fVerbose )
+    {
+        printf( "E:  Del = %6.2f. Area = %8.2f. Cuts = %6d. Lim = %2d. Ave = %5.2f. ", 
+            p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
+        PRT( "T", clock() - clk );
+    }
+/*
+    clk = clock();
+    If_ManImproveReduce( p, p->pPars->nLutSize );
+    If_ManComputeRequired( p, 0 );
+    if ( p->pPars->fVerbose )
+    {
+        printf( "R:  Del = %6.2f. Area = %8.2f. Cuts = %6d. Lim = %2d. Ave = %5.2f. ", 
+            p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
+        PRT( "T", clock() - clk );
+    }
+
+    clk = clock();
+    If_ManImproveExpand( p, p->pPars->nLutSize );
+    If_ManComputeRequired( p, 0 );
+    if ( p->pPars->fVerbose )
+    {
+        printf( "E:  Del = %6.2f. Area = %8.2f. Cuts = %6d. Lim = %2d. Ave = %5.2f. ", 
+            p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
+        PRT( "T", clock() - clk );
+    }
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs area recovery for each node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManImproveExpand( If_Man_t * p, int nLimit )
+{
+    Vec_Ptr_t * vFront, * vFrontOld, * vVisited;
+    If_Obj_t * pObj;
+    int i;
+    vFront    = Vec_PtrAlloc( nLimit );
+    vFrontOld = Vec_PtrAlloc( nLimit );
+    vVisited  = Vec_PtrAlloc( 100 );
+    // iterate through all nodes in the topological order
+    If_ManForEachNode( p, pObj, i )
+        If_ManImproveNodeExpand( p, pObj, nLimit, vFront, vFrontOld, vVisited );
+    Vec_PtrFree( vFront );
+    Vec_PtrFree( vFrontOld );
+    Vec_PtrFree( vVisited );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of nodes with no external fanout.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_ManImproveCutCost( If_Man_t * p, Vec_Ptr_t * vFront )
+{
+    If_Obj_t * pFanin;
+    int i, Counter = 0;
+    Vec_PtrForEachEntry( vFront, pFanin, i )
+        if ( pFanin->nRefs == 0 )
+            Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs area recovery for each node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManImproveNodeExpand( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vFrontOld, Vec_Ptr_t * vVisited )
+{
+    If_Obj_t * pFanin;
+    If_Cut_t * pCut;
+    int CostBef, CostAft, i;
+    float DelayOld, AreaBef, AreaAft;
+    pCut = If_ObjCutBest(pObj);
+    assert( pCut->Delay <= pObj->Required + p->fEpsilon );
+    if ( pObj->nRefs == 0 )
+        return;
+    // get the delay
+    DelayOld = pCut->Delay;
+    // get the area
+    AreaBef = If_CutAreaRefed( p, pCut, 100000 );
+//    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, 100000 );
+    CostBef = If_ManImproveCutCost( p, vFront );
+    If_ManImproveNodeFaninCompact( p, pObj, nLimit, vFront, vVisited );
+    CostAft = If_ManImproveCutCost( p, vFront );
+    If_CutRef( p, pCut, 100000 );
+    assert( CostBef >= CostAft );
+    // clean up
+    Vec_PtrForEachEntry( vVisited, pFanin, i )
+        pFanin->fMark = 0;
+    // update the node
+    If_ManImproveNodeUpdate( p, pObj, vFront );
+    pCut->Delay = If_CutDelay( p, pCut );
+    // get the new area
+    AreaAft = If_CutAreaRefed( p, pCut, 100000 );
+    if ( AreaAft > AreaBef || pCut->Delay > pObj->Required + p->fEpsilon )
+    {
+        If_ManImproveNodeUpdate( p, pObj, vFrontOld );
+        AreaAft = If_CutAreaRefed( p, pCut, 100000 );
+        assert( AreaAft == AreaBef );
+        pCut->Delay = DelayOld;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs area recovery for each node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManImproveMark_rec( If_Man_t * p, If_Obj_t * pObj, Vec_Ptr_t * vVisited )
+{
+    if ( pObj->fMark )
+        return;
+    assert( If_ObjIsAnd(pObj) );
+    If_ManImproveMark_rec( p, If_ObjFanin0(pObj), vVisited );
+    If_ManImproveMark_rec( p, If_ObjFanin1(pObj), vVisited );
+    Vec_PtrPush( vVisited, pObj );
+    pObj->fMark = 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares node mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManImproveNodePrepare( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vFrontOld, Vec_Ptr_t * vVisited )
+{
+    If_Cut_t * pCut;
+    If_Obj_t * pLeaf;
+    int i;
+    Vec_PtrClear( vFront );
+    Vec_PtrClear( vFrontOld );
+    Vec_PtrClear( vVisited );
+    // expand the cut downwards from the given place
+    pCut = If_ObjCutBest(pObj);
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+    {
+        Vec_PtrPush( vFront, pLeaf );
+        Vec_PtrPush( vFrontOld, pLeaf );
+        Vec_PtrPush( vVisited, pLeaf );
+        pLeaf->fMark = 1;
+    }
+    // mark the nodes in the cone
+    If_ManImproveMark_rec( p, pObj, vVisited );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the frontier.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManImproveNodeUpdate( If_Man_t * p, If_Obj_t * pObj, Vec_Ptr_t * vFront )
+{
+    If_Cut_t * pCut;
+    If_Obj_t * pFanin;
+    int i;
+    pCut = If_ObjCutBest(pObj);
+    // deref node's cut
+    If_CutDeref( p, pCut, 10000 );
+    // 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, 10000 );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the number of fanins will grow.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_ManImproveNodeWillGrow( If_Man_t * p, If_Obj_t * pObj )
+{
+    If_Obj_t * pFanin0, * pFanin1;
+    assert( If_ObjIsAnd(pObj) );
+    pFanin0 = If_ObjFanin0(pObj);
+    pFanin1 = If_ObjFanin1(pObj);
+    return !pFanin0->fMark && !pFanin1->fMark;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the increase in the number of fanins with no external refs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_ManImproveNodeFaninCost( If_Man_t * p, If_Obj_t * pObj )
+{
+    int Counter = 0;
+    assert( If_ObjIsAnd(pObj) );
+    // check if the node has external refs
+    if ( pObj->nRefs == 0 )
+        Counter--;
+    // increment the number of fanins without external refs
+    if ( !If_ObjFanin0(pObj)->fMark && If_ObjFanin0(pObj)->nRefs == 0 )
+        Counter++;
+    // increment the number of fanins without external refs
+    if ( !If_ObjFanin1(pObj)->fMark && If_ObjFanin1(pObj)->nRefs == 0 )
+        Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the frontier.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManImproveNodeFaninUpdate( If_Man_t * p, If_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited )
+{
+    If_Obj_t * pFanin;
+    assert( If_ObjIsAnd(pObj) );
+    Vec_PtrRemove( vFront, pObj );
+    pFanin = If_ObjFanin0(pObj);
+    if ( !pFanin->fMark )
+    {
+        Vec_PtrPush( vFront, pFanin );
+        Vec_PtrPush( vVisited, pFanin );
+        pFanin->fMark = 1;
+    }
+    pFanin = If_ObjFanin1(pObj);
+    if ( !pFanin->fMark )
+    {
+        Vec_PtrPush( vFront, pFanin );
+        Vec_PtrPush( vVisited, pFanin );
+        pFanin->fMark = 1;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compacts the number of external refs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_ManImproveNodeFaninCompact0( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited )
+{
+    If_Obj_t * pFanin;
+    int i;
+    Vec_PtrForEachEntry( vFront, pFanin, i )
+    {
+        if ( If_ObjIsPi(pFanin) )
+            continue;
+        if ( If_ManImproveNodeWillGrow(p, pFanin) )
+            continue;
+        if ( If_ManImproveNodeFaninCost(p, pFanin) <= 0 )
+        {
+            If_ManImproveNodeFaninUpdate( p, pFanin, vFront, vVisited );
+            return 1;
+        }
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compacts the number of external refs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_ManImproveNodeFaninCompact1( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited )
+{
+    If_Obj_t * pFanin;
+    int i;
+    Vec_PtrForEachEntry( vFront, pFanin, i )
+    {
+        if ( If_ObjIsPi(pFanin) )
+            continue;
+        if ( If_ManImproveNodeFaninCost(p, pFanin) < 0 )
+        {
+            If_ManImproveNodeFaninUpdate( p, pFanin, vFront, vVisited );
+            return 1;
+        }
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compacts the number of external refs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_ManImproveNodeFaninCompact2( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited )
+{
+    If_Obj_t * pFanin;
+    int i;
+    Vec_PtrForEachEntry( vFront, pFanin, i )
+    {
+        if ( If_ObjIsPi(pFanin) )
+            continue;
+        if ( If_ManImproveNodeFaninCost(p, pFanin) <= 0 )
+        {
+            If_ManImproveNodeFaninUpdate( p, pFanin, vFront, vVisited );
+            return 1;
+        }
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compacts the number of external refs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_ManImproveNodeFaninCompact_int( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited )
+{
+    if ( If_ManImproveNodeFaninCompact0(p, pObj, nLimit, vFront, vVisited) )
+        return 1;
+    if (  Vec_PtrSize(vFront) < nLimit && If_ManImproveNodeFaninCompact1(p, pObj, nLimit, vFront, vVisited) )
+        return 1;
+    if ( Vec_PtrSize(vFront) < nLimit && If_ManImproveNodeFaninCompact2(p, pObj, nLimit, vFront, vVisited) )
+        return 1;
+    assert( Vec_PtrSize(vFront) <= nLimit );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compacts the number of external refs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManImproveNodeFaninCompact( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited )
+{
+    while ( If_ManImproveNodeFaninCompact_int( p, pObj, nLimit, vFront, vVisited ) );
+}
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fast mapping for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManImproveNodeReduce( If_Man_t * p, If_Obj_t * pObj, int nLimit )
+{
+    If_Cut_t * pCut, * pCut0, * pCut1, * pCutR;
+    If_Obj_t * pFanin0, * pFanin1;
+    float AreaBef, AreaAft;
+    int RetValue;
+
+    assert( nLimit <= 32 );
+    assert( If_ObjIsAnd(pObj) );
+    // get the fanins
+    pFanin0 = If_ObjFanin0(pObj);
+    pFanin1 = If_ObjFanin1(pObj);
+    // get the cuts
+    pCut  = If_ObjCutBest(pObj);
+    pCut0 = If_ObjIsPi(pFanin0) ? If_ObjCutTriv(pFanin0) : If_ObjCutBest(pFanin0);
+    pCut1 = If_ObjIsPi(pFanin1) ? If_ObjCutTriv(pFanin1) : If_ObjCutBest(pFanin1);
+    assert( pCut->Delay <= pObj->Required + p->fEpsilon );
+
+    // deref the cut if the node is refed
+    if ( pObj->nRefs > 0 )
+        If_CutDeref( p, pCut, 100000 );
+    // get the area
+    AreaBef = If_CutAreaDerefed( p, pCut, 100000 );
+    // 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
+    {
+        pCut0 = If_ObjCutTriv(pFanin0);
+    }
+    // get the fanin support
+    if ( pFanin1->nRefs > 2 && pCut1->Delay < pObj->Required + p->fEpsilon )
+//    if ( pSupp1->nRefs > 0 && pSupp1->Delay < pSupp->DelayR )
+    {
+        pCut1 = If_ObjCutTriv(pFanin1);
+    }
+
+    // merge the cuts
+    pCutR = p->ppCuts[0];
+    RetValue = If_CutMerge( pCut0, pCut1, pCutR, nLimit );
+    // try very simple cut
+    if ( !RetValue )
+    {
+        RetValue = If_CutMerge( If_ObjCutTriv(pFanin0), If_ObjCutTriv(pFanin1), pCutR, nLimit );
+        assert( RetValue == 1 );
+    }
+    if ( RetValue )
+    {
+        pCutR->Delay = If_CutDelay( p, pCutR );
+        AreaAft = If_CutAreaDerefed( p, pCutR, 100000 );
+        // update the best cut
+        if ( AreaAft < AreaBef - p->fEpsilon && pCutR->Delay < pObj->Required + p->fEpsilon )
+            If_CutCopy( pCut, pCutR );
+    }
+    // recompute the delay of the best cut
+    pCut->Delay = If_CutDelay( p, pCut );
+    // ref the cut if the node is refed
+    if ( pObj->nRefs > 0 )
+        If_CutRef( p, pCut, 100000 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs area recovery for each node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManImproveReduce( If_Man_t * p, int nLimit )
+{
+    If_Obj_t * pObj;
+    int i;
+    If_ManForEachNode( p, pObj, i )
+    {
+        if ( 278 == i )
+        {
+            int s = 0;
+        }
+        If_ManImproveNodeReduce( p, pObj, nLimit );
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/if/ifSelect.c b/src/map/if/ifSelect.c
new file mode 100644
index 00000000..d54abb29
--- /dev/null
+++ b/src/map/if/ifSelect.c
@@ -0,0 +1,175 @@
+/**CFile****************************************************************
+
+  FileName    [ifSelect.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [FPGA mapping based on priority cuts.]
+
+  Synopsis    [Selects what mapping to use.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 21, 2006.]
+
+  Revision    [$Id: ifSelect.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "if.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void If_ManPerformMappingMoveBestCut( If_Man_t * p, int iPosNew, int iPosOld );
+static void If_ManPerformMappingAdjust( If_Man_t * p, int nCuts );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Merges the results of delay, relaxed delay and area-based mapping.]
+
+  Description [Delay target may be different from minimum delay!!!]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManPerformMappingPreprocess( If_Man_t * p )
+{
+    float delayArea, delayDelay, delayPure;
+    int clk = clock();
+    assert( p->pPars->nCutsMax >= 4 );
+
+    // perform min-area mapping and move the cut to the end
+    p->pPars->fArea = 1;
+    If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 0 );
+    p->pPars->fArea = 0;
+    delayArea = If_ManDelayMax( p );
+    if ( p->pPars->DelayTarget != -1 && delayArea < p->pPars->DelayTarget - p->fEpsilon )
+        delayArea = p->pPars->DelayTarget;
+    If_ManPerformMappingMoveBestCut( p, p->pPars->nCutsMax - 1, 1 );
+
+    // perfrom min-delay mapping and move the cut to the end
+    p->pPars->fFancy = 1;
+    If_ManPerformMappingRound( p, p->pPars->nCutsMax - 1, 0, 0 );
+    p->pPars->fFancy = 0;
+    delayDelay = If_ManDelayMax( p );
+    if ( p->pPars->DelayTarget != -1 && delayDelay < p->pPars->DelayTarget - p->fEpsilon )
+        delayDelay = p->pPars->DelayTarget;
+    If_ManPerformMappingMoveBestCut( p, p->pPars->nCutsMax - 2, 1 );
+
+    // perform min-area mapping 
+    If_ManPerformMappingRound( p, p->pPars->nCutsMax - 2, 0, 0 );
+    delayPure = If_ManDelayMax( p );
+    if ( p->pPars->DelayTarget != -1 && delayPure < p->pPars->DelayTarget - p->fEpsilon )
+        delayPure = p->pPars->DelayTarget;
+
+    // decide what to do
+    if ( delayPure < delayDelay - p->fEpsilon && delayPure < delayArea - p->fEpsilon )
+    {
+        // copy the remaining two cuts
+        if ( p->pPars->nCutsMax > 4 )
+        {
+            If_ManPerformMappingMoveBestCut( p, 2, p->pPars->nCutsMax - 2 );
+            If_ManPerformMappingMoveBestCut( p, 3, p->pPars->nCutsMax - 1 );
+        }
+        If_ManComputeRequired( p, 1 );
+        If_ManPerformMappingAdjust( p, 4 );
+    }
+    else if ( delayDelay < delayArea - p->fEpsilon )
+    {
+        If_ManPerformMappingMoveBestCut( p, 1, p->pPars->nCutsMax - 2 );
+        If_ManPerformMappingMoveBestCut( p, 2, p->pPars->nCutsMax - 1 );
+        If_ManComputeRequired( p, 1 );
+        If_ManPerformMappingAdjust( p, 3 );
+    }
+    else
+    {
+        If_ManPerformMappingMoveBestCut( p, 1, p->pPars->nCutsMax - 1 );
+        If_ManComputeRequired( p, 1 );
+        If_ManPerformMappingAdjust( p, 2 );
+    }
+    If_ManComputeRequired( p, 1 );
+    if ( p->pPars->fVerbose )
+    {
+        printf( "S:  Del = %6.2f. Area = %8.2f. Cuts = %6d. Lim = %2d. Ave = %5.2f. ", 
+            p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
+        PRT( "T", clock() - clk );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Moves the best cut to the given position.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManPerformMappingMoveBestCut( If_Man_t * p, int iPosNew, int iPosOld )
+{
+    If_Obj_t * pObj;
+    int i;
+    assert( iPosOld != iPosNew );
+    assert( iPosOld > 0 && iPosOld < p->pPars->nCutsMax );
+    assert( iPosNew > 0 && iPosNew < p->pPars->nCutsMax );
+    If_ManForEachNode( p, pObj, i )
+        If_CutCopy( pObj->Cuts + iPosNew, pObj->Cuts + iPosOld );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adjusts mapping for the given cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManPerformMappingAdjust( If_Man_t * p, int nCuts )
+{
+    If_Cut_t * pCut, * pCutBest;
+    If_Obj_t * pObj;
+    int i, c;
+    assert( nCuts >= 2 && nCuts <= 4 );
+    If_ManForEachNode( p, pObj, i )
+    {
+        pCutBest = NULL;
+        for ( c = 1; c < nCuts; c++ )
+        {
+            pCut = pObj->Cuts + c;
+            pCut->Delay = If_CutDelay( p, pCut );
+            pCut->Area  = If_CutFlow( p, pCut );
+            assert( pCutBest || pCut->Delay < pObj->Required + p->fEpsilon );
+            if ( pCutBest == NULL || 
+                (pCut->Delay < pObj->Required + p->fEpsilon && 
+                 pCut->Area < pCutBest->Area - p->fEpsilon) )
+                pCutBest = pCut;
+        }
+        assert( pCutBest != NULL );
+        // check if we need to move
+        if ( pCutBest != pObj->Cuts + 1 )
+            If_CutCopy( pObj->Cuts + 1, pCutBest );
+        // set the number of cuts
+        pObj->nCuts = 2;
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/if/ifSeq.c b/src/map/if/ifSeq.c
new file mode 100644
index 00000000..ce353f49
--- /dev/null
+++ b/src/map/if/ifSeq.c
@@ -0,0 +1,170 @@
+/**CFile****************************************************************
+
+  FileName    [ifSeq.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [FPGA mapping based on priority cuts.]
+
+  Synopsis    [Sequential mapping.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 21, 2006.]
+
+  Revision    [$Id: ifSeq.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "if.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void If_ObjPerformMappingLI( If_Man_t * p, If_Obj_t * pLatch );
+static void If_ObjPerformMappingLO( If_Man_t * p, If_Obj_t * pLatch, If_Obj_t * pObj );
+static int  If_ManMappingSeqConverged( If_Man_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs sequential mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_ManPerformMappingSeq( If_Man_t * p )
+{
+    If_Obj_t * pObj, * pLatch;
+    int i, clkTotal = clock();
+    // set the number of cuts used
+    p->nCutsUsed = p->pPars->nCutsMax;
+    // set arrival times and trivial cuts at const 1 and PIs
+    If_ManConst1(p)->Cuts[0].Delay = 0.0;
+    If_ManForEachPi( p, pObj, i )
+        pObj->Cuts[0].Delay = p->pPars->pTimesArr[i];
+    // set the fanout estimates of the PIs
+    If_ManForEachPi( p, pObj, i )
+        pObj->EstRefs = (float)1.0;
+    // delay oriented mapping
+    p->pPars->fFancy = 1;
+    If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 0 );
+    p->pPars->fFancy = 0;
+
+    // perform iterations over the circuit
+    while ( !If_ManMappingSeqConverged( p ) )
+    {
+        // assign cuts to latches
+        If_ManForEachLatch( p, pLatch, i )
+            If_ObjPerformMappingLI( p, pLatch );
+        // assign cuts to primary inputs
+        If_ManForEachLatch( p, pLatch, i )
+            If_ObjPerformMappingLO( p, pLatch, If_ManPi(p, If_ManPiNum(p) - If_ManPoNum(p) + i) );
+        // map the nodes
+        If_ManForEachNode( p, pObj, i )
+            If_ObjPerformMapping( p, pObj, 0 );
+    }
+
+    if ( p->pPars->fVerbose )
+    {
+        PRT( "Total time", clock() - clkTotal );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs sequential mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_CutLift( If_Cut_t * pCut )
+{
+    int i;
+    for ( i = 0; i < pCut->nLeaves; i++ )
+        pCut->pLeaves[i] = ((pCut->pLeaves[i] >> 8) << 8) | ((pCut->pLeaves[i] & 255) + 1);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs sequential mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ObjPerformMappingLI( If_Man_t * p, If_Obj_t * pLatch )
+{
+    If_Obj_t * pFanin;
+    int c;
+    assert( If_ObjIsPo(pLatch) );
+    pFanin = If_ObjFanin0(pLatch);
+    for ( c = 0; c < pFanin->nCuts; c++ )
+        If_CutCopy( pLatch->Cuts + c, pFanin->Cuts + c );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs sequential mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ObjPerformMappingLO( If_Man_t * p, If_Obj_t * pLatch, If_Obj_t * pObj )
+{
+    If_Cut_t * pCut;
+    int c, Limit = IF_MIN( p->nCuts + 1, p->nCutsUsed );
+    assert( If_ObjIsPo(pLatch) );
+    for ( c = 1; c < Limit; c++ )
+    {
+        pCut = pObj->Cuts + c;
+        If_CutCopy( pCut, pLatch->Cuts + c - 1 );
+        If_CutLift( pCut );
+        pCut->Delay -= p->Fi;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs sequential mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_ManMappingSeqConverged( If_Man_t * p )
+{
+    return 0;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/if/module.make b/src/map/if/module.make
index be044da2..362318da 100644
--- a/src/map/if/module.make
+++ b/src/map/if/module.make
@@ -1,4 +1,8 @@
 SRC +=  src/map/if/ifCore.c \
+    src/map/if/ifCut.c \
     src/map/if/ifMan.c \
     src/map/if/ifMap.c \
+    src/map/if/ifReduce.c \
+    src/map/if/ifSelect.c \
+    src/map/if/ifSeq.c \
     src/map/if/ifUtil.c 
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index 4e188cf0..4e12dfe4 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -64,7 +64,8 @@ void Prove_ParamsSetDefault( Prove_Params_t * pParams )
     pParams->nBddSizeLimit        = 1000000; // the number of BDD nodes when construction is aborted
     pParams->fBddReorder          = 1;       // enables dynamic BDD variable reordering
     // last-gasp mitering
-    pParams->nMiteringLimitLast   = 1000000; // final mitering limit
+//    pParams->nMiteringLimitLast   = 1000000; // final mitering limit
+    pParams->nMiteringLimitLast   = 0;       // final mitering limit
     // global SAT solver limits
     pParams->nTotalBacktrackLimit = 0;       // global limit on the number of backtracks
     pParams->nTotalInspectLimit   = 0;       // global limit on the number of clause inspects