Version abc61205

22 files changed, 2211 insertions, 1874 deletions

diff --git a/src/aig/ivy/ivyFactor.c b/src/aig/ivy/ivyFactor.c
index d8323931..19a40b3f 100644
--- a/src/aig/ivy/ivyFactor.c
+++ b/src/aig/ivy/ivyFactor.c
@@ -25,16 +25,398 @@
 ///                        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 );
+// ISOP computation fails if intermediate memory usage exceed this limit
+#define IVY_FACTOR_MEM_LIMIT  16*4096
+
+// intermediate ISOP representation
+typedef struct Ivy_Sop_t_ Ivy_Sop_t;
+struct Ivy_Sop_t_
+{
+    unsigned * uCubes;
+    int        nCubes;
+};
+
+static inline int          Ivy_CubeHasLit( unsigned uCube, int i )              { return (uCube &  (unsigned)(1<<i)) > 0;}
+static inline unsigned     Ivy_CubeSetLit( unsigned uCube, int i )              { return  uCube |  (unsigned)(1<<i);     }
+static inline unsigned     Ivy_CubeXorLit( unsigned uCube, int i )              { return  uCube ^  (unsigned)(1<<i);     }
+static inline unsigned     Ivy_CubeRemLit( unsigned uCube, int i )              { return  uCube & ~(unsigned)(1<<i);     }
+
+static inline int          Ivy_CubeContains( unsigned uLarge, unsigned uSmall ) { return (uLarge & uSmall) == uSmall;    }
+static inline unsigned     Ivy_CubeSharp( unsigned uCube, unsigned uPart )      { return uCube & ~uPart;                 }
+static inline unsigned     Ivy_CubeMask( int nVar )                             { return (~(unsigned)0) >> (32-nVar);    }
+
+static inline int          Ivy_CubeIsMarked( unsigned uCube )                   { return Ivy_CubeHasLit( uCube, 31 );    }
+static inline void         Ivy_CubeMark( unsigned uCube )                       { Ivy_CubeSetLit( uCube, 31 );           }
+static inline void         Ivy_CubeUnmark( unsigned uCube )                     { Ivy_CubeRemLit( uCube, 31 );           }
+
+static inline int          Ivy_SopCubeNum( Ivy_Sop_t * cSop )                   { return cSop->nCubes;                   }
+static inline unsigned     Ivy_SopCube( Ivy_Sop_t * cSop, int i )               { return cSop->uCubes[i];                }
+static inline void         Ivy_SopAddCube( Ivy_Sop_t * cSop, unsigned uCube )   { cSop->uCubes[cSop->nCubes++] = uCube;  }
+static inline void         Ivy_SopSetCube( Ivy_Sop_t * cSop, unsigned uCube, int i ) { cSop->uCubes[i] = uCube;          }
+static inline void         Ivy_SopShrink( Ivy_Sop_t * cSop, int nCubesNew )     { cSop->nCubes = nCubesNew;              }
+
+// iterators
+#define Ivy_SopForEachCube( cSop, uCube, i )                                      \
+    for ( i = 0; (i < Ivy_SopCubeNum(cSop)) && ((uCube) = Ivy_SopCube(cSop, i)); i++ )
+#define Ivy_CubeForEachLiteral( uCube, Lit, nLits, i )                            \
+    for ( i = 0; (i < (nLits)) && ((Lit) = Ivy_CubeHasLit(uCube, i)); i++ )
+
+/**Function*************************************************************
+
+  Synopsis    [Divides cover by one cube.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_SopDivideByCube( Vec_Int_t * vStore, int nVars, Ivy_Sop_t * cSop, Ivy_Sop_t * cDiv, Ivy_Sop_t * vQuo, Ivy_Sop_t * vRem )
+{
+    unsigned uCube, uDiv;
+    int i;
+    // get the only cube
+    assert( Ivy_SopCubeNum(cDiv) == 1 );
+    uDiv = Ivy_SopCube(cDiv, 0);
+    // allocate covers
+    vQuo->nCubes = 0;
+    vQuo->uCubes = Vec_IntFetch( vStore, Ivy_SopCubeNum(cSop) );
+    vRem->nCubes = 0;
+    vRem->uCubes = Vec_IntFetch( vStore, Ivy_SopCubeNum(cSop) );
+    // sort the cubes
+    Ivy_SopForEachCube( cSop, uCube, i )
+    {
+        if ( Ivy_CubeContains( uCube, uDiv ) )
+            Ivy_SopAddCube( vQuo, Ivy_CubeSharp(uCube, uDiv) );
+        else
+            Ivy_SopAddCube( vRem, uCube );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Divides cover by one cube.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_SopDivideInternal( Vec_Int_t * vStore, int nVars, Ivy_Sop_t * cSop, Ivy_Sop_t * cDiv, Ivy_Sop_t * vQuo, Ivy_Sop_t * vRem )
+{
+    unsigned uCube, uCube2, uDiv, uDiv2, uQuo;
+    int i, i2, k, k2;
+    assert( Ivy_SopCubeNum(cSop) >= Ivy_SopCubeNum(cDiv) );
+    if ( Ivy_SopCubeNum(cDiv) == 1 )
+    {
+        Ivy_SopDivideByCube( cSop, cDiv, vQuo, vRem );
+        return;
+    }
+    // allocate quotient
+    vQuo->nCubes = 0;
+    vQuo->uCubes = Vec_IntFetch( vStore, Ivy_SopCubeNum(cSop) / Ivy_SopCubeNum(cDiv) );
+    // for each cube of the cover
+    // it either belongs to the quotient or to the remainder
+    Ivy_SopForEachCube( cSop, uCube, i )
+    {
+        // skip taken cubes
+        if ( Ivy_CubeIsMarked(uCube) )
+            continue;
+        // mark the cube
+        Ivy_SopSetCube( cSop, Ivy_CubeMark(uCube), i );
+        // find a matching cube in the divisor
+        Ivy_SopForEachCube( cDiv, uDiv, k )
+            if ( Ivy_CubeContains( uCube, uDiv ) )
+                break;
+        // the case when the cube is not found
+        // (later we will add marked cubes to the remainder)
+        if ( k == Ivy_SopCubeNum(cDiv) )
+            continue;
+        // if the quotient cube exist, it will be 
+        uQuo = Ivy_CubeSharp( uCube, uDiv );
+        // try to find other cubes of the divisor
+        Ivy_SopForEachCube( cDiv, uDiv2, k2 )
+        {
+            if ( k2 == k )
+                continue;
+            // find a matching cube
+            Ivy_SopForEachCube( cSop, uCube2, i2 )
+            {
+                // skip taken cubes
+                if ( Ivy_CubeIsMarked(uCube2) )
+                    continue;
+                // check if the cube can be used
+                if ( Ivy_CubeContains( uCube2, uDiv2 ) && uQuo == Ivy_CubeSharp( uCube2, uDiv2 ) )
+                    break;
+            }
+            // the case when the cube is not found
+            if ( i2 == Ivy_SopCubeNum(cSop) )
+                break;
+            // the case when the cube is found - mark it and keep going
+            Ivy_SopSetCube( cSop, Ivy_CubeMark(uCube2), i2 );
+        }
+        // if we did not find some cube, continue 
+        // (later we will add marked cubes to the remainder)
+        if ( k2 != Ivy_SopCubeNum(cDiv) )
+            continue;
+        // we found all cubes - add the quotient cube
+        Ivy_SopAddCube( vQuo, uQuo );
+    }
+    // allocate remainder
+    vRem->nCubes = 0;
+    vRem->uCubes = Vec_IntFetch( vStore, Ivy_SopCubeNum(cSop) - Ivy_SopCubeNum(vQuo) * Ivy_SopCubeNum(cDiv) );
+    // finally add the remaining cubes to the remainder 
+    // and clean the marked cubes in the cover
+    Ivy_SopForEachCube( cSop, uCube, i )
+    {
+        if ( !Ivy_CubeIsMarked(uCube) )
+            continue;
+        Ivy_SopSetCube( cSop, Ivy_CubeUnmark(uCube), i );
+        Ivy_SopAddCube( vRem, Ivy_CubeUnmark(uCube) );
+    }
+}
+
+/**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 []
 
-extern Vec_Int_t * Mvc_CoverCommonCubeCover( Vec_Int_t * vCover );
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_SopDivideByLiteralQuo( Ivy_Sop_t * cSop, int iLit )
+{
+    unsigned uCube;
+    int i, k = 0;
+    Ivy_SopForEachCube( cSop, uCube, i )
+    {
+        if ( Ivy_CubeHasLit(uCube, iLit) )
+            Ivy_SopSetCube( cSop, Ivy_CubeRemLit(uCube, iLit), k++ );
+    }
+    Ivy_SopShrink( cSop, k );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_SopCommonCubeCover( Ivy_Sop_t * cSop, Ivy_Sop_t * vCommon, Vec_Int_t * vStore )
+{
+    unsigned uTemp, uCube;
+    int i;
+    uCube = ~(unsigned)0;
+    Ivy_SopForEachCube( cSop, uTemp, i )
+        uCube &= uTemp;
+    vCommon->nCubes = 0;
+    vCommon->uCubes = Vec_IntFetch( vStore, 1 );
+    Ivy_SopPush( vCommon, uCube );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_SopCreateInverse( Ivy_Sop_t * cSop, Vec_Int_t * vInput, int nVars, Vec_Int_t * vStore )
+{
+    unsigned uCube, uMask;
+    int i;
+    // start the cover
+    cSop->nCubes = 0;
+    cSop->uCubes = Vec_IntFetch( vStore, Vec_IntSize(vInput) );
+    // add the cubes
+    uMask = Ivy_CubeMask( nVars );
+    Vec_IntForEachEntry( vInput, uCube, i )
+        Vec_IntPush( cSop, Ivy_CubeSharp(uMask, uCube) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_SopDup( Ivy_Sop_t * cSop, Ivy_Sop_t * vCopy, Vec_Int_t * vStore )
+{
+    unsigned uCube;
+    int i;
+    // start the cover
+    vCopy->nCubes = 0;
+    vCopy->uCubes = Vec_IntFetch( vStore, Vec_IntSize(cSop) );
+    // add the cubes
+    Ivy_SopForEachCube( cSop, uTemp, i )
+        Ivy_SopPush( vCopy, uTemp );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Find the least often occurring literal.]
+
+  Description [Find the least often occurring literal among those
+  that occur more than once.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_SopWorstLiteral( Ivy_Sop_t * cSop, int nLits )
+{
+    unsigned uCube;
+    int nWord, nBit;
+    int i, k, iMin, nLitsMin, nLitsCur;
+    int fUseFirst = 1;
+
+    // go through each literal
+    iMin = -1;
+    nLitsMin = 1000000;
+    for ( i = 0; i < nLits; i++ )
+    {
+        // go through all the cubes
+        nLitsCur = 0;
+        Ivy_SopForEachCube( cSop, uCube, k )
+            if ( Ivy_CubeHasLit(uCube, i) )
+                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    [Computes a level-zero kernel.]
+
+  Description [Modifies the cover to contain one level-zero kernel.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_SopMakeCubeFree( Ivy_Sop_t * cSop )
+{
+    unsigned uMask;
+    int i;
+    assert( Ivy_SopCubeNum(cSop) > 0 );
+    // find the common cube
+    uMask = ~(unsigned)0;
+    Ivy_SopForEachCube( cSop, uCube, i )
+        uMask &= uCube;
+    if ( uMask == 0 )
+        return;
+    // remove the common cube
+    Ivy_SopForEachCube( cSop, uCube, i )
+        Ivy_SopSetCube( cSop, Ivy_CubeSharp(uCube, uMask), i );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes a level-zero kernel.]
+
+  Description [Modifies the cover to contain one level-zero kernel.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_SopDivisorZeroKernel_rec( Ivy_Sop_t * cSop, int nLits )
+{
+    int iLit;
+    // find any literal that occurs at least two times
+    iLit = Ivy_SopWorstLiteral( cSop, nLits );
+    if ( iLit == -1 )
+        return;
+    // derive the cube-free quotient
+    Ivy_SopDivideByLiteralQuo( cSop, iLit ); // the same cover
+    Ivy_SopMakeCubeFree( cSop );             // the same cover
+    // call recursively
+    Ivy_SopDivisorZeroKernel_rec( cSop );    // the same cover
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the quick divisor of the cover.]
+
+  Description [Returns NULL, if there is not divisor other than
+  trivial.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_SopDivisor( Ivy_Sop_t * cSop, int nLits, Ivy_Sop_t * cDiv, Vec_Int_t * vStore )
+{
+    if ( Ivy_SopCubeNum(cSop) <= 1 )
+        return 0;
+    if ( Ivy_SopWorstLiteral( cSop, nLits ) == -1 )
+        return 0;
+    // duplicate the cover
+    Ivy_SopDup( cSop, cDiv, vStore );
+    // perform the kerneling
+    Ivy_SopDivisorZeroKernel_rec( cDiv, int nLits );
+    assert( Ivy_SopCubeNum(cDiv) > 0 );
+    return 1;
+}
+
+
+
+
+
+extern Dec_Edge_t  Dec_Factor32_rec( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nVars );
+extern Dec_Edge_t  Dec_Factor32LF_rec( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nVars, Vec_Int_t * vSimple );
+extern Dec_Edge_t  Dec_Factor32Trivial( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nVars );
+extern Dec_Edge_t  Dec_Factor32TrivialCube( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nVars, unsigned uCube, Vec_Int_t * vEdgeLits );
+extern Dec_Edge_t  Dec_Factor32TrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr );
+extern int         Dec_Factor32Verify( Vec_Int_t * cSop, Dec_Graph_t * pFForm )
 
 
 ////////////////////////////////////////////////////////////////////////
@@ -52,29 +434,38 @@ extern Vec_Int_t * Mvc_CoverCommonCubeCover( Vec_Int_t * vCover );
   SeeAlso     []
 
 ***********************************************************************/
-Dec_Graph_t * Dec_Factor32( Vec_Int_t * vCover, int nVars )
+Dec_Graph_t * Dec_Factor32( Vec_Int_t * cSop, int nVars, Vec_Int_t * vStore )
 {
+    Ivy_Sop_t cSop, cRes;
+    Ivy_Sop_t * pcSop = &cSop, * pcRes = &cRes;
     Dec_Graph_t * pFForm;
     Dec_Edge_t eRoot;
 
+    assert( nVars < 16 );
+
     // check for trivial functions
-    if ( Vec_IntSize(vCover) == 0 )
+    if ( Vec_IntSize(cSop) == 0 )
         return Dec_GraphCreateConst0();
-    if ( Vec_IntSize(vCover) == 1 && /* tautology */ )
+    if ( Vec_IntSize(cSop) == 1 && Vec_IntEntry(cSop, 0) == Ivy_CubeMask(nVars) )
         return Dec_GraphCreateConst1();
 
+    // prepare memory manager
+    Vec_IntClear( vStore );
+    Vec_IntGrow( vStore, IVY_FACTOR_MEM_LIMIT );
+
     // perform CST
-    Mvc_CoverInverse( vCover ); // CST
+    Ivy_SopCreateInverse( cSop, pcSop, nVars, vStore ); // CST
+
     // start the factored form
-    pFForm = Dec_GraphCreate( Abc_SopGetVarNum(pSop) );
+    pFForm = Dec_GraphCreate( nVars );
     // factor the cover
-    eRoot = Dec_Factor32_rec( pFForm, vCover, nVars );
+    eRoot = Dec_Factor32_rec( pFForm, cSop, 2 * 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
+    if ( !Dec_Factor32Verify( pSop, pFForm, nVars ) )
+        printf( "Verification has failed.\n" );
     return pFForm;
 }
 
@@ -89,47 +480,47 @@ Dec_Graph_t * Dec_Factor32( Vec_Int_t * vCover, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-Dec_Edge_t Dec_Factor32_rec( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars )
+Dec_Edge_t Dec_Factor32_rec( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nLits )
 {
-    Vec_Int_t * vDiv, * vQuo, * vRem, * vCom;
+    Vec_Int_t * cDiv, * 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) );
+    assert( Vec_IntSize(cSop) );
 
     // get the divisor
-    vDiv = Dec_Factor32Divisor( vCover, nVars );
-    if ( vDiv == NULL )
-        return Dec_Factor32Trivial( pFForm, vCover, nVars );
+    cDiv = Ivy_SopDivisor( cSop, nLits );
+    if ( cDiv == NULL )
+        return Dec_Factor32Trivial( pFForm, cSop, nLits );
 
     // divide the cover by the divisor
-    Mvc_CoverDivideInternal( vCover, nVars, vDiv, &vQuo, &vRem );
+    Ivy_SopDivideInternal( cSop, nLits, cDiv, &vQuo, &vRem );
     assert( Vec_IntSize(vQuo) );
 
-    Vec_IntFree( vDiv );
+    Vec_IntFree( cDiv );
     Vec_IntFree( vRem );
 
     // check the trivial case
     if ( Vec_IntSize(vQuo) == 1 )
     {
-        eNode = Dec_Factor32LF_rec( pFForm, vCover, nVars, vQuo );
+        eNode = Dec_Factor32LF_rec( pFForm, cSop, nLits, vQuo );
         Vec_IntFree( vQuo );
         return eNode;
     }
 
     // make the quotient cube free
-    Mvc_CoverMakeCubeFree( vQuo );
+    Ivy_SopMakeCubeFree( vQuo );
 
     // divide the cover by the quotient
-    Mvc_CoverDivideInternal( vCover, nVars, vQuo, &vDiv, &vRem );
+    Ivy_SopDivideInternal( cSop, nLits, vQuo, &cDiv, &vRem );
 
     // check the trivial case
-    if ( Mvc_CoverIsCubeFree( vDiv ) )
+    if ( Ivy_SopIsCubeFree( cDiv ) )
     {
-        eNodeDiv = Dec_Factor32_rec( pFForm, vDiv );
+        eNodeDiv = Dec_Factor32_rec( pFForm, cDiv );
         eNodeQuo = Dec_Factor32_rec( pFForm, vQuo );
-        Vec_IntFree( vDiv );
+        Vec_IntFree( cDiv );
         Vec_IntFree( vQuo );
         eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
         if ( Vec_IntSize(vRem) == 0 )
@@ -146,13 +537,13 @@ Dec_Edge_t Dec_Factor32_rec( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars
     }
 
     // get the common cube
-    vCom = Mvc_CoverCommonCubeCover( vDiv );
-    Vec_IntFree( vDiv );
+    vCom = Ivy_SopCommonCubeCover( cDiv );
+    Vec_IntFree( cDiv );
     Vec_IntFree( vQuo );
     Vec_IntFree( vRem );
 
     // solve the simple problem
-    eNode = Dec_Factor32LF_rec( pFForm, vCover, nVars, vCom );
+    eNode = Dec_Factor32LF_rec( pFForm, cSop, nLits, vCom );
     Vec_IntFree( vCom );
     return eNode;
 }
@@ -169,21 +560,21 @@ Dec_Edge_t Dec_Factor32_rec( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars
   SeeAlso     []
 
 ***********************************************************************/
-Dec_Edge_t Dec_Factor32LF_rec( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars, Vec_Int_t * vSimple )
+Dec_Edge_t Dec_Factor32LF_rec( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nLits, Vec_Int_t * vSimple )
 {
     Dec_Man_t * pManDec = Abc_FrameReadManDec();
     Vec_Int_t * vEdgeLits  = pManDec->vLits;
-    Vec_Int_t * vDiv, * vQuo, * vRem;
+    Vec_Int_t * cDiv, * vQuo, * vRem;
     Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem;
     Dec_Edge_t eNodeAnd;
 
     // get the most often occurring literal
-    vDiv = Mvc_CoverBestLiteralCover( vCover, nVars, vSimple );
+    cDiv = Ivy_SopBestLiteralCover( cSop, nLits, vSimple );
     // divide the cover by the literal
-    Mvc_CoverDivideByLiteral( vCover, nVars, vDiv, &vQuo, &vRem );
+    Ivy_SopDivideByLiteral( cSop, nLits, cDiv, &vQuo, &vRem );
     // get the node pointer for the literal
-    eNodeDiv = Dec_Factor32TrivialCube( pFForm, vDiv, Mvc_CoverReadCubeHead(vDiv), vEdgeLits );
-    Vec_IntFree( vDiv );
+    eNodeDiv = Dec_Factor32TrivialCube( pFForm, cDiv, Ivy_SopReadCubeHead(cDiv), vEdgeLits );
+    Vec_IntFree( cDiv );
     // factor the quotient and remainder
     eNodeQuo = Dec_Factor32_rec( pFForm, vQuo );
     Vec_IntFree( vQuo );
@@ -214,20 +605,20 @@ Dec_Edge_t Dec_Factor32LF_rec( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVa
   SeeAlso     []
 
 ***********************************************************************/
-Dec_Edge_t Dec_Factor32Trivial( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars )
+Dec_Edge_t Dec_Factor32Trivial( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nLits )
 {
     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;
+    unsigned uCube;
     int i;
     // create the factored form for each cube
     Vec_IntClear( vEdgeCubes );
-    Mvc_CoverForEachCube( vCover, pCube )
+    Ivy_SopForEachCube( cSop, uCube )
     {
-        eNode = Dec_Factor32TrivialCube( pFForm, vCover, nVars, pCube, vEdgeLits );
+        eNode = Dec_Factor32TrivialCube( pFForm, cSop, nLits, uCube, vEdgeLits );
         Vec_IntPush( vEdgeCubes, Dec_EdgeToInt_(eNode) );
     }
     // balance the factored forms
@@ -245,13 +636,13 @@ Dec_Edge_t Dec_Factor32Trivial( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nV
   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 Dec_Factor32TrivialCube( Dec_Graph_t * pFForm, Vec_Int_t * cSop, unsigned uCube, int nLits, 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 )
+    Mvc_CubeForEachLit( cSop, uCube, iBit, Value )
         if ( Value )
         {
             eNode = Dec_EdgeCreate( iBit/2, iBit%2 ); // CST
@@ -296,126 +687,15 @@ Dec_Edge_t Dec_Factor32TrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNod
         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;
-}
 
+// verification using temporary BDD package
+#include "cuddInt.h"
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Verifies that the factoring is correct.]
 
   Description []
                
@@ -424,326 +704,43 @@ int Dec_Factor32WorstLiteral( Vec_Int_t * vCover, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Mvc_CoverCommonCubeCover( Vec_Int_t * vCover )
+DdNode * Ivy_SopCoverToBdd( DdManager * dd, Vec_Int_t * cSop, int nVars )
 {
-    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 ) )
+    DdNode * bSum, * bCube, * bTemp, * bVar;
+    unsigned uCube;
+    int Value, v;
+    assert( nVars < 16 );
+    // start the cover
+    bSum = Cudd_ReadLogicZero(dd);   Cudd_Ref( bSum );
+   // check the logic function of the node
+    Vec_IntForEachEntry( cSop, uCube, i )
     {
-        *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 )
+        bCube = Cudd_ReadOne(dd);   Cudd_Ref( bCube );
+        for ( v = 0; v < nVars; v++ )
         {
-            // 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++];
+            Value = ((uCube >> 2*v) & 3);
+            if ( Value == 1 )
+                bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) );
+            else if ( Value == 2 )
+                bVar = Cudd_bddIthVar( dd, v );
+            else
                 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 );
+            bCube  = Cudd_bddAnd( dd, bTemp = bCube, bVar );   Cudd_Ref( bCube );
+            Cudd_RecursiveDeref( dd, bTemp );
         }
+        bSum = Cudd_bddOr( dd, bTemp = bSum, bCube );   
+        Cudd_Ref( bSum );
+        Cudd_RecursiveDeref( dd, bTemp );
+        Cudd_RecursiveDeref( dd, bCube );
     }
-    // return the results
-    *pvRem = vRem;
-    *pvQuo = vQuo;
+    // complement the result if necessary
+    Cudd_Deref( bSum );
+    return bSum;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Divides the cover by a literal.]
+  Synopsis    [Verifies that the factoring is correct.]
 
   Description []
                
@@ -752,80 +749,33 @@ void Mvc_CoverDivideByCube( Vec_Int_t * vCover, Vec_Int_t * vDiv, Vec_Int_t ** p
   SeeAlso     []
 
 ***********************************************************************/
-void Mvc_CoverDivideByLiteral( Vec_Int_t * vCover, Vec_Int_t * vDiv, Vec_Int_t ** pvQuo, Vec_Int_t ** pvRem )
+int Dec_Factor32Verify( Vec_Int_t * cSop, Dec_Graph_t * pFForm, int nVars )
 {
-    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 )
+    static DdManager * dd = NULL;
+    DdNode * bFunc1, * bFunc2;
+    int RetValue;
+    // get the manager
+    if ( dd == NULL )
+        dd = Cudd_Init( 16, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    // get the functions
+    bFunc1 = Ivy_SopCoverToBdd( dd, cSop, nVars );   Cudd_Ref( bFunc1 );
+    bFunc2 = Dec_GraphDeriveBdd( dd, pFForm );         Cudd_Ref( bFunc2 );
+//Extra_bddPrint( dd, bFunc1 ); printf("\n");
+//Extra_bddPrint( dd, bFunc2 ); printf("\n");
+    RetValue = (bFunc1 == bFunc2);
+    if ( bFunc1 != bFunc2 )
     {
-        // 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 );
-        }
+        int s;
+        Extra_bddPrint( dd, bFunc1 ); printf("\n");
+        Extra_bddPrint( dd, bFunc2 ); printf("\n");
+        s  = 0;
     }
-    // return the results
-    *pvRem = vRem;
-    *pvQuo = vQuo;
+    Cudd_RecursiveDeref( dd, bFunc1 );
+    Cudd_RecursiveDeref( dd, bFunc2 );
+    return RetValue;
 }
 
 
-/**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/ivy/ivyIsop.c b/src/aig/ivy/ivyIsop.c
index 1887eb6a..ae48ca34 100644
--- a/src/aig/ivy/ivyIsop.c
+++ b/src/aig/ivy/ivyIsop.c
@@ -19,7 +19,6 @@
 ***********************************************************************/
 
 #include "ivy.h"
-#include "mem.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 08e1323d..27f82d6e 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -698,9 +698,6 @@ extern int                Abc_NodeMffcLabel( Abc_Obj_t * pNode );
 extern void               Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp );
 extern int                Abc_NodeDeref_rec( Abc_Obj_t * pNode );
 extern int                Abc_NodeRef_rec( Abc_Obj_t * pNode );
-/*=== abcRenode.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
-extern DdNode *           Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld );
 /*=== abcRefactor.c ==========================================================*/
 extern int                Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
 /*=== abcRewrite.c ==========================================================*/
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index dbbe9d7e..77ae4d5a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -53,6 +53,7 @@ static int Abc_CommandShowCut        ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandCollapse       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandStrash         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBalance        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandMulti          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRenode         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCleanup        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSweep          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -184,6 +185,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "collapse",      Abc_CommandCollapse,         1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "strash",        Abc_CommandStrash,           1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "balance",       Abc_CommandBalance,          1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "multi",         Abc_CommandMulti,            1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "renode",        Abc_CommandRenode,           1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "cleanup",       Abc_CommandCleanup,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "sweep",         Abc_CommandSweep,            1 );
@@ -1911,7 +1913,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandMulti( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -1920,6 +1922,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fMulti;
     int fSimple;
     int fFactor;
+    extern Abc_Ntk_t * Abc_NtkMulti( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -1990,7 +1993,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkRenode( pNtk, nThresh, nFaninMax, fCnf, fMulti, fSimple, fFactor );
+    pNtkRes = Abc_NtkMulti( pNtk, nThresh, nFaninMax, fCnf, fMulti, fSimple, fFactor );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Renoding has failed.\n" );
@@ -2001,7 +2004,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: renode [-T num] [-F num] [-msfch]\n" );
+    fprintf( pErr, "usage: multi [-T num] [-F num] [-msfch]\n" );
     fprintf( pErr, "\t          transforms an AIG into a logic network by creating larger nodes\n" );
     fprintf( pErr, "\t-F num  : the maximum fanin size after renoding [default = %d]\n", nFaninMax );
     fprintf( pErr, "\t-T num  : the threshold for AIG node duplication [default = %d]\n", nThresh );
@@ -2027,6 +2030,95 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int nFaninMax, c;
+    int fUseBdds;
+    int fVerbose;
+    extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int fUseBdds, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nFaninMax =  8;
+    fUseBdds  =  0;
+    fVerbose  =  0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Fbvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFaninMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFaninMax < 0 ) 
+                goto usage;
+            break;
+        case 'b':
+            fUseBdds ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Cannot renode a network that is not an AIG (run \"strash\").\n" );
+        return 1;
+    }
+
+    // get the new network
+    pNtkRes = Abc_NtkRenode( pNtk, nFaninMax, fUseBdds, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Renoding has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: renode [-F num] [-bv]\n" );
+    fprintf( pErr, "\t          transforms an AIG into a logic network by creating larger nodes\n" );
+    fprintf( pErr, "\t-F num  : the maximum fanin size after renoding [default = %d]\n", nFaninMax );
+    fprintf( pErr, "\t-b      : toggles cost function (BDD nodes or FF literals) [default = %s]\n", fUseBdds? "BDD nodes": "FF literals" );
+    fprintf( pErr, "\t-v      : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); 
+    fprintf( pErr, "\t-h      : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -7391,19 +7483,26 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     memset( pPars, 0, sizeof(If_Par_t) );
+    // user-controlable paramters
     pPars->Mode        =  0;
     pPars->nLutSize    =  4;
-//    pPars->pLutLib    =  Abc_FrameReadLibLut();
     pPars->nCutsMax    = 20;
+    pPars->DelayTarget = -1;
     pPars->fPreprocess =  1;
     pPars->fArea       =  0;
     pPars->fFancy      =  0;
-    pPars->fLatchPaths =  0;
     pPars->fExpRed     =  1;
+    pPars->fLatchPaths =  0;
     pPars->fSeq        =  0;
-    pPars->nLatches    =  0;
-    pPars->DelayTarget = -1;
     pPars->fVerbose    =  0;
+    // internal parameters
+    pPars->fTruth      =  1;
+    pPars->nLatches    =  pNtk? Abc_NtkLatchNum(pNtk) : 0;
+    pPars->pLutLib     =  NULL; // Abc_FrameReadLibLut();
+    pPars->pTimesArr   =  NULL; 
+    pPars->pTimesArr   =  NULL;   
+    pPars->pFuncCost   =  NULL;   
+
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "MKCDpaflrsvh" ) ) != EOF )
     {
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 704c8ebb..b76385f8 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -28,8 +28,7 @@
 static If_Man_t *  Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
 static Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk );
 static Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj );
-static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Cut_t * pCut );
-static Hop_Obj_t * Abc_NodeIfToHop2( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj );
+static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj );
  
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -75,7 +74,7 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
         return NULL;
     }
 
-    // transform the result of mapping into a BDD network
+    // transform the result of mapping into the new network
     pNtkNew = Abc_NtkFromIf( pIfMan, pNtk );
     if ( pNtkNew == NULL )
         return NULL;
@@ -163,7 +162,10 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     Abc_Obj_t * pNode, * pNodeNew;
     int i, nDupGates;
     // create the new network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_AIG );
+    if ( pIfMan->pPars->fUseBdds )
+        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
+    else
+        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_AIG );
     // prepare the mapping manager
     If_ManCleanNodeCopy( pIfMan );
     If_ManCleanCutData( pIfMan );
@@ -221,75 +223,37 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
     If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, i )
         Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf) );
     // derive the function of this node
-//    pNodeNew->pData = Abc_NodeIfToHop( pNtkNew->pManFunc, pIfMan, pCutBest );
-    pNodeNew->pData = Abc_NodeIfToHop2( pNtkNew->pManFunc, pIfMan, pIfObj );
-    If_ObjSetCopy( pIfObj, pNodeNew );
-    return pNodeNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively derives the truth table for the cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Abc_NodeIfToHop_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Cut_t * pCut, Vec_Ptr_t * vVisited )
-{
-    Hop_Obj_t * gFunc, * gFunc0, * gFunc1;
-    // if the cut is visited, return the result
-    if ( If_CutData(pCut) )
-        return If_CutData(pCut);
-    // compute the functions of the children
-    gFunc0 = Abc_NodeIfToHop_rec( pHopMan, pIfMan, pCut->pOne, vVisited );
-    gFunc1 = Abc_NodeIfToHop_rec( pHopMan, pIfMan, pCut->pTwo, vVisited );
-    // get the function of the cut
-    gFunc  = Hop_And( pHopMan, Hop_NotCond(gFunc0, pCut->fCompl0), Hop_NotCond(gFunc1, pCut->fCompl1) );  
-    gFunc  = Hop_NotCond( gFunc, pCut->Phase );
-    assert( If_CutData(pCut) == NULL );
-    If_CutSetData( pCut, gFunc );
-    // add this cut to the visited list
-    Vec_PtrPush( vVisited, pCut );
-    return gFunc;
-}
-
-/**Function*************************************************************
 
-  Synopsis    [Derives the truth table for one cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
+    if ( pIfMan->pPars->fTruth )
+    {
+        if ( pIfMan->pPars->fUseBdds )
+        { 
+            extern void Abc_NodeBddReorder( void * p, Abc_Obj_t * pNode );
+            extern DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars );
+            // transform truth table into the BDD 
+            pNodeNew->pData = Kit_TruthToBdd( pNtkNew->pManFunc, If_CutTruth(pCutBest), pCutBest->nLimit );
+            // reorder the fanins to minimize the BDD size
+            Abc_NodeBddReorder( pIfMan->pPars->pReoMan, pNodeNew );
+        }
+        else
+        {
+            typedef int Kit_Graph_t;
+            extern Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars );
+            extern Hop_Obj_t * Dec_GraphToNetworkAig( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
+            // transform truth table into the decomposition tree
+            Kit_Graph_t * pGraph = Kit_TruthToGraph( If_CutTruth(pCutBest), pCutBest->nLimit );
+            // derive the AIG for that tree
+            pNodeNew->pData = Dec_GraphToNetworkAig( pNtkNew->pManFunc, pGraph );
+            Kit_GraphFree( pGraph );
+        }
+    }
+    else
 
-***********************************************************************/
-Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Cut_t * pCut )
-{
-    Hop_Obj_t * gFunc;
-    If_Obj_t * pLeaf;
-    int i;
-    assert( pCut->nLeaves > 1 );
-    // set the leaf variables
-    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
-        If_CutSetData( If_ObjCutTriv(pLeaf), Hop_IthVar(pHopMan, i) );
-    // recursively compute the function while collecting visited cuts
-    Vec_PtrClear( pIfMan->vTemp );
-    gFunc = Abc_NodeIfToHop_rec( pHopMan, pIfMan, pCut, pIfMan->vTemp ); 
-//    printf( "%d ", Vec_PtrSize(p->vTemp) );
-    // clean the cuts
-    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
-        If_CutSetData( If_ObjCutTriv(pLeaf), NULL );
-    Vec_PtrForEachEntry( pIfMan->vTemp, pCut, i )
-        If_CutSetData( pCut, NULL );
-    return gFunc;
+        pNodeNew->pData = Abc_NodeIfToHop( pNtkNew->pManFunc, pIfMan, pIfObj );
+    If_ObjSetCopy( pIfObj, pNodeNew );
+    return pNodeNew;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Recursively derives the truth table for the cut.]
@@ -301,7 +265,7 @@ Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Cut_t *
   SeeAlso     []
 
 ***********************************************************************/
-Hop_Obj_t * Abc_NodeIfToHop2_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited )
+Hop_Obj_t * Abc_NodeIfToHop_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited )
 {
     If_Cut_t * pCut;
     Hop_Obj_t * gFunc, * gFunc0, * gFunc1;
@@ -311,11 +275,10 @@ Hop_Obj_t * Abc_NodeIfToHop2_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj
     if ( If_CutData(pCut) )
         return If_CutData(pCut);
     // compute the functions of the children
-    gFunc0 = Abc_NodeIfToHop2_rec( pHopMan, pIfMan, pIfObj->pFanin0, vVisited );
-    gFunc1 = Abc_NodeIfToHop2_rec( pHopMan, pIfMan, pIfObj->pFanin1, vVisited );
+    gFunc0 = Abc_NodeIfToHop_rec( pHopMan, pIfMan, pIfObj->pFanin0, vVisited );
+    gFunc1 = Abc_NodeIfToHop_rec( pHopMan, pIfMan, pIfObj->pFanin1, vVisited );
     // get the function of the cut
     gFunc  = Hop_And( pHopMan, Hop_NotCond(gFunc0, pIfObj->fCompl0), Hop_NotCond(gFunc1, pIfObj->fCompl1) );  
-    gFunc  = Hop_NotCond( gFunc, pCut->Phase );
     assert( If_CutData(pCut) == NULL );
     If_CutSetData( pCut, gFunc );
     // add this cut to the visited list
@@ -334,7 +297,7 @@ Hop_Obj_t * Abc_NodeIfToHop2_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj
   SeeAlso     []
 
 ***********************************************************************/
-Hop_Obj_t * Abc_NodeIfToHop2( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj )
+Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj )
 {
     If_Cut_t * pCut;
     Hop_Obj_t * gFunc;
@@ -348,7 +311,7 @@ Hop_Obj_t * Abc_NodeIfToHop2( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t *
         If_CutSetData( If_ObjCutTriv(pLeaf), Hop_IthVar(pHopMan, i) );
     // recursively compute the function while collecting visited cuts
     Vec_PtrClear( pIfMan->vTemp );
-    gFunc = Abc_NodeIfToHop2_rec( pHopMan, pIfMan, pIfObj, pIfMan->vTemp ); 
+    gFunc = Abc_NodeIfToHop_rec( pHopMan, pIfMan, pIfObj, pIfMan->vTemp ); 
 //    printf( "%d ", Vec_PtrSize(p->vTemp) );
     // clean the cuts
     If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index c4f9850a..d4d50923 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -469,6 +469,7 @@ Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
 {
+    extern Abc_Ntk_t * Abc_NtkMulti( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
     ProgressBar * pProgress;
     Abc_Ntk_t * pNtkNew, * pNtkNew2;
     Abc_Obj_t * pNode;
@@ -484,7 +485,7 @@ Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
 
     // duplicate the network
     pNtkNew2 = Abc_NtkDup( pNtk );
-    pNtkNew  = Abc_NtkRenode( pNtkNew2, 0, 20, 0, 0, 1, 0 );
+    pNtkNew  = Abc_NtkMulti( pNtkNew2, 0, 20, 0, 0, 1, 0 );
     if ( !Abc_NtkBddToSop( pNtkNew, 0 ) )
     {
         printf( "Abc_NtkFromMapSuperChoice(): Converting to SOPs has failed.\n" );
diff --git a/src/base/abci/abcMulti.c b/src/base/abci/abcMulti.c
new file mode 100644
index 00000000..e93360a0
--- /dev/null
+++ b/src/base/abci/abcMulti.c
@@ -0,0 +1,643 @@
+/**CFile****************************************************************
+
+  FileName    [abcMulti.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Procedures which transform an AIG into multi-input AND-graph.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcMulti.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void        Abc_NtkMultiInt( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+static Abc_Obj_t * Abc_NtkMulti_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld );
+
+static DdNode *    Abc_NtkMultiDeriveBdd_rec( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFanins );
+static DdNode *    Abc_NtkMultiDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld );
+
+static void        Abc_NtkMultiSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax );
+static void        Abc_NtkMultiSetBoundsCnf( Abc_Ntk_t * pNtk );
+static void        Abc_NtkMultiSetBoundsMulti( Abc_Ntk_t * pNtk, int nThresh );
+static void        Abc_NtkMultiSetBoundsSimple( Abc_Ntk_t * pNtk );
+static void        Abc_NtkMultiSetBoundsFactor( Abc_Ntk_t * pNtk );
+static void        Abc_NtkMultiCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the AIG into nodes.]
+
+  Description [Threhold is the max number of nodes duplicated at a node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkMulti( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor )
+{
+    Abc_Ntk_t * pNtkNew;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( nThresh >= 0 );
+    assert( nFaninMax > 1 );
+
+    // print a warning about choice nodes
+    if ( Abc_NtkGetChoiceNum( pNtk ) )
+        printf( "Warning: The choice nodes in the AIG are removed by renoding.\n" );
+
+    // define the boundary
+    if ( fCnf )
+        Abc_NtkMultiSetBoundsCnf( pNtk );
+    else if ( fMulti )
+        Abc_NtkMultiSetBoundsMulti( pNtk, nThresh );
+    else if ( fSimple )
+        Abc_NtkMultiSetBoundsSimple( pNtk );
+    else if ( fFactor )
+        Abc_NtkMultiSetBoundsFactor( pNtk );
+    else
+        Abc_NtkMultiSetBounds( pNtk, nThresh, nFaninMax );
+
+    // perform renoding for this boundary
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
+    Abc_NtkMultiInt( pNtk, pNtkNew );
+    Abc_NtkFinalize( pNtk, pNtkNew );
+
+    // make the network minimum base
+    Abc_NtkMinimumBase( pNtkNew );
+
+    // fix the problem with complemented and duplicated CO edges
+    Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
+
+    // report the number of CNF objects
+    if ( fCnf )
+    {
+//        int nClauses = Abc_NtkGetClauseNum(pNtkNew) + 2*Abc_NtkPoNum(pNtkNew) + 2*Abc_NtkLatchNum(pNtkNew);
+//        printf( "CNF variables = %d. CNF clauses = %d.\n",  Abc_NtkNodeNum(pNtkNew), nClauses );
+    }
+//printf( "Maximum fanin = %d.\n", Abc_NtkGetFaninMax(pNtkNew) );
+
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkMulti: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the AIG into nodes.]
+
+  Description [Threhold is the max number of nodes duplicated at a node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMultiInt( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
+{
+    ProgressBar * pProgress;
+    Abc_Obj_t * pNode, * pConst1, * pNodeNew;
+    int i;
+
+    // set the constant node
+    pConst1 = Abc_AigConst1(pNtk);
+    if ( Abc_ObjFanoutNum(pConst1) > 0 )
+    {
+        pNodeNew = Abc_NtkCreateNode( pNtkNew );  
+        pNodeNew->pData = Cudd_ReadOne( pNtkNew->pManFunc );   Cudd_Ref( pNodeNew->pData );
+        pConst1->pCopy = pNodeNew;
+    }
+
+    // perform renoding for POs
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        if ( Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
+            continue;
+        Abc_NtkMulti_rec( pNtkNew, Abc_ObjFanin0(pNode) );
+    }
+    Extra_ProgressBarStop( pProgress );
+
+    // clean the boundaries and data field in the old network
+    Abc_NtkForEachObj( pNtk, pNode, i )
+    {
+        pNode->fMarkA = 0;
+        pNode->pData = NULL;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find the best multi-input node rooted at the given node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkMulti_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld )
+{
+    Vec_Ptr_t * vCone;
+    Abc_Obj_t * pNodeNew;
+    int i;
+
+    assert( !Abc_ObjIsComplement(pNodeOld) );
+    // return if the result if known
+    if ( pNodeOld->pCopy )
+        return pNodeOld->pCopy;
+    assert( Abc_ObjIsNode(pNodeOld) );
+    assert( !Abc_AigNodeIsConst(pNodeOld) );
+    assert( pNodeOld->fMarkA );
+
+//printf( "%d ", Abc_NodeMffcSizeSupp(pNodeOld) );
+
+    // collect the renoding cone
+    vCone = Vec_PtrAlloc( 10 );
+    Abc_NtkMultiCone( pNodeOld, vCone );
+
+    // create a new node 
+    pNodeNew = Abc_NtkCreateNode( pNtkNew ); 
+    for ( i = 0; i < vCone->nSize; i++ )
+        Abc_ObjAddFanin( pNodeNew, Abc_NtkMulti_rec(pNtkNew, vCone->pArray[i]) );
+
+    // derive the function of this node
+    pNodeNew->pData = Abc_NtkMultiDeriveBdd( pNtkNew->pManFunc, pNodeOld, vCone );    
+    Cudd_Ref( pNodeNew->pData );
+    Vec_PtrFree( vCone );
+
+    // remember the node
+    pNodeOld->pCopy = pNodeNew;
+    return pNodeOld->pCopy;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the local BDD of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NtkMultiDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld )
+{
+    Abc_Obj_t * pFaninOld;
+    DdNode * bFunc;
+    int i;
+    assert( !Abc_AigNodeIsConst(pNodeOld) );
+    assert( Abc_ObjIsNode(pNodeOld) );
+    // set the elementary BDD variables for the input nodes
+    for ( i = 0; i < vFaninsOld->nSize; i++ )
+    {
+        pFaninOld = vFaninsOld->pArray[i];
+        pFaninOld->pData = Cudd_bddIthVar( dd, i );    Cudd_Ref( pFaninOld->pData );
+        pFaninOld->fMarkC = 1;
+    }
+    // call the recursive BDD computation
+    bFunc = Abc_NtkMultiDeriveBdd_rec( dd, pNodeOld, vFaninsOld );  Cudd_Ref( bFunc );
+    // dereference the intermediate nodes
+    for ( i = 0; i < vFaninsOld->nSize; i++ )
+    {
+        pFaninOld = vFaninsOld->pArray[i];
+        Cudd_RecursiveDeref( dd, pFaninOld->pData );
+        pFaninOld->fMarkC = 0;
+    }
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the local BDD of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NtkMultiDeriveBdd_rec( DdManager * dd, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins )
+{
+    DdNode * bFunc, * bFunc0, * bFunc1;
+    assert( !Abc_ObjIsComplement(pNode) );
+    // if the result is available return
+    if ( pNode->fMarkC )
+    {
+        assert( pNode->pData ); // network has a cycle
+        return pNode->pData;
+    }
+    // mark the node as visited
+    pNode->fMarkC = 1;
+    Vec_PtrPush( vFanins, pNode );
+    // compute the result for both branches
+    bFunc0 = Abc_NtkMultiDeriveBdd_rec( dd, Abc_ObjFanin(pNode,0), vFanins ); Cudd_Ref( bFunc0 );
+    bFunc1 = Abc_NtkMultiDeriveBdd_rec( dd, Abc_ObjFanin(pNode,1), vFanins ); Cudd_Ref( bFunc1 );
+    bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pNode) );
+    bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pNode) );
+    // get the final result
+    bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( bFunc );
+    Cudd_RecursiveDeref( dd, bFunc0 );
+    Cudd_RecursiveDeref( dd, bFunc1 );
+    // set the result
+    pNode->pData = bFunc;
+    assert( pNode->pData );
+    return bFunc;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Limits the cones to be no more than the given size.]
+
+  Description [Returns 1 if the last cone was limited. Returns 0 if no changes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMultiLimit_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, int nFaninMax, int fCanStop, int fFirst )
+{
+    int nNodes0, nNodes1;
+    assert( !Abc_ObjIsComplement(pNode) );
+    // check if the node should be added to the fanins
+    if ( !fFirst && (pNode->fMarkA || !Abc_ObjIsNode(pNode)) )
+    {
+        Vec_PtrPushUnique( vCone, pNode );
+        return 0;
+    }
+    // if we cannot stop in this branch, collect all nodes
+    if ( !fCanStop )
+    {
+        Abc_NtkMultiLimit_rec( Abc_ObjFanin(pNode,0), vCone, nFaninMax, 0, 0 );
+        Abc_NtkMultiLimit_rec( Abc_ObjFanin(pNode,1), vCone, nFaninMax, 0, 0 );
+        return 0;
+    }
+    // if we can stop, try the left branch first, and return if we stopped
+    assert( vCone->nSize == 0 );
+    if ( Abc_NtkMultiLimit_rec( Abc_ObjFanin(pNode,0), vCone, nFaninMax, 1, 0 ) )
+        return 1;
+    // save the number of nodes in the left branch and call for the right branch
+    nNodes0 = vCone->nSize;
+    assert( nNodes0 <= nFaninMax );
+    Abc_NtkMultiLimit_rec( Abc_ObjFanin(pNode,1), vCone, nFaninMax, 0, 0 );
+    // check the number of nodes
+    if ( vCone->nSize <= nFaninMax )
+        return 0;
+    // the number of nodes exceeds the limit
+
+    // get the number of nodes in the right branch
+    vCone->nSize = 0;
+    Abc_NtkMultiLimit_rec( Abc_ObjFanin(pNode,1), vCone, nFaninMax, 0, 0 );
+    // if this number exceeds the limit, solve the problem for this branch
+    if ( vCone->nSize > nFaninMax )
+    {
+        int RetValue;
+        vCone->nSize = 0;
+        RetValue = Abc_NtkMultiLimit_rec( Abc_ObjFanin(pNode,1), vCone, nFaninMax, 1, 0 );
+        assert( RetValue == 1 );
+        return 1;
+    }
+
+    nNodes1 = vCone->nSize; 
+    assert( nNodes1 <= nFaninMax );
+    if ( nNodes0 >= nNodes1 )
+    { // the left branch is larger - cut it
+        assert( Abc_ObjFanin(pNode,0)->fMarkA == 0 );
+        Abc_ObjFanin(pNode,0)->fMarkA = 1;
+    }
+    else
+    { // the right branch is larger - cut it
+        assert( Abc_ObjFanin(pNode,1)->fMarkA == 0 );
+        Abc_ObjFanin(pNode,1)->fMarkA = 1;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Limits the cones to be no more than the given size.]
+
+  Description [Returns 1 if the last cone was limited. Returns 0 if no changes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMultiLimit( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, int nFaninMax )
+{
+    vCone->nSize = 0;
+    return Abc_NtkMultiLimit_rec( pNode, vCone, nFaninMax, 1, 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the expansion boundary for multi-input nodes.]
+
+  Description [The boundary includes the set of PIs and all nodes such that 
+  when expanding over the node we duplicate no more than nThresh nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMultiSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax )
+{
+    Vec_Ptr_t * vCone = Vec_PtrAlloc(10);
+    Abc_Obj_t * pNode;
+    int i, nFanouts, nConeSize;
+
+    // make sure the mark is not set
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        assert( pNode->fMarkA == 0 );
+
+    // mark the nodes where expansion stops using pNode->fMarkA
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        // skip PI/PO nodes
+//        if ( Abc_NodeIsConst(pNode) )
+//            continue;
+        // mark the nodes with multiple fanouts
+        nFanouts = Abc_ObjFanoutNum(pNode);
+        nConeSize = Abc_NodeMffcSize(pNode);
+        if ( (nFanouts - 1) * nConeSize > nThresh )
+            pNode->fMarkA = 1;
+    }
+
+    // mark the PO drivers
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        Abc_ObjFanin0(pNode)->fMarkA = 1;
+
+    // make sure the fanin limit is met
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        // skip PI/PO nodes
+//        if ( Abc_NodeIsConst(pNode) )
+//            continue;
+        if ( pNode->fMarkA == 0 )
+            continue;
+        // continue cutting branches until it meets the fanin limit
+        while ( Abc_NtkMultiLimit(pNode, vCone, nFaninMax) );
+        assert( vCone->nSize <= nFaninMax );  
+    }
+    Vec_PtrFree(vCone);
+/*
+    // make sure the fanin limit is met
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        // skip PI/PO nodes
+//        if ( Abc_NodeIsConst(pNode) )
+//            continue;
+        if ( pNode->fMarkA == 0 )
+            continue;
+        Abc_NtkMultiCone( pNode, vCone );
+        assert( vCone->nSize <= nFaninMax );    
+    }
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the expansion boundary for conversion into CNF.]
+
+  Description [The boundary includes the set of PIs, the roots of MUXes,
+  the nodes with multiple fanouts and the nodes with complemented outputs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMultiSetBoundsCnf( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i, nMuxes;
+
+    // make sure the mark is not set
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        assert( pNode->fMarkA == 0 );
+
+    // mark the nodes where expansion stops using pNode->fMarkA
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        // skip PI/PO nodes
+//        if ( Abc_NodeIsConst(pNode) )
+//            continue;
+        // mark the nodes with multiple fanouts
+        if ( Abc_ObjFanoutNum(pNode) > 1 )
+            pNode->fMarkA = 1;
+        // mark the nodes that are roots of MUXes
+        if ( Abc_NodeIsMuxType( pNode ) )
+        {
+            pNode->fMarkA = 1;
+            Abc_ObjFanin0( Abc_ObjFanin0(pNode) )->fMarkA = 1;
+            Abc_ObjFanin0( Abc_ObjFanin1(pNode) )->fMarkA = 1;
+            Abc_ObjFanin1( Abc_ObjFanin0(pNode) )->fMarkA = 1;
+            Abc_ObjFanin1( Abc_ObjFanin1(pNode) )->fMarkA = 1;
+        }
+        else  // mark the complemented edges
+        {
+            if ( Abc_ObjFaninC0(pNode) )
+                Abc_ObjFanin0(pNode)->fMarkA = 1;
+            if ( Abc_ObjFaninC1(pNode) )
+                Abc_ObjFanin1(pNode)->fMarkA = 1;
+        }
+    }
+
+    // mark the PO drivers
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        Abc_ObjFanin0(pNode)->fMarkA = 1;
+
+    // count the number of MUXes
+    nMuxes = 0;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        // skip PI/PO nodes
+//        if ( Abc_NodeIsConst(pNode) )
+//            continue;
+        if ( Abc_NodeIsMuxType(pNode) && 
+            Abc_ObjFanin0(pNode)->fMarkA == 0 &&
+            Abc_ObjFanin1(pNode)->fMarkA == 0 )
+            nMuxes++;
+    }
+//    printf( "The number of MUXes detected = %d (%5.2f %% of logic).\n", nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) );
+} 
+ 
+/**Function*************************************************************
+
+  Synopsis    [Sets the expansion boundary for conversion into multi-input AND graph.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMultiSetBoundsMulti( Abc_Ntk_t * pNtk, int nThresh )
+{
+    Abc_Obj_t * pNode;
+    int i, nFanouts, nConeSize;
+
+    // make sure the mark is not set
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        assert( pNode->fMarkA == 0 );
+
+    // mark the nodes where expansion stops using pNode->fMarkA
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        // skip PI/PO nodes
+//        if ( Abc_NodeIsConst(pNode) )
+//            continue;
+        // mark the nodes with multiple fanouts
+//        if ( Abc_ObjFanoutNum(pNode) > 1 )
+//            pNode->fMarkA = 1;
+        // mark the nodes with multiple fanouts
+        nFanouts = Abc_ObjFanoutNum(pNode);
+        nConeSize = Abc_NodeMffcSizeStop(pNode);
+        if ( (nFanouts - 1) * nConeSize > nThresh )
+            pNode->fMarkA = 1;
+        // mark the children if they are pointed by the complemented edges
+        if ( Abc_ObjFaninC0(pNode) )
+            Abc_ObjFanin0(pNode)->fMarkA = 1;
+        if ( Abc_ObjFaninC1(pNode) )
+            Abc_ObjFanin1(pNode)->fMarkA = 1;
+    }
+
+    // mark the PO drivers
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        Abc_ObjFanin0(pNode)->fMarkA = 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets a simple boundary.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMultiSetBoundsSimple( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    // make sure the mark is not set
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        assert( pNode->fMarkA == 0 );
+    // mark the nodes where expansion stops using pNode->fMarkA
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        pNode->fMarkA = 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets a factor-cut boundary.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMultiSetBoundsFactor( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    // make sure the mark is not set
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        assert( pNode->fMarkA == 0 );
+    // mark the nodes where expansion stops using pNode->fMarkA
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        pNode->fMarkA = (pNode->vFanouts.nSize > 1 && !Abc_NodeIsMuxControlType(pNode));
+    // mark the PO drivers
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        Abc_ObjFanin0(pNode)->fMarkA = 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the fanins of a large node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMultiCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone )
+{
+    assert( !Abc_ObjIsComplement(pNode) );
+    if ( pNode->fMarkA || !Abc_ObjIsNode(pNode) )
+    {
+        Vec_PtrPushUnique( vCone, pNode );
+        return;
+    }
+    Abc_NtkMultiCone_rec( Abc_ObjFanin(pNode,0), vCone );
+    Abc_NtkMultiCone_rec( Abc_ObjFanin(pNode,1), vCone );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the fanins of a large node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMultiCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone )
+{
+    assert( !Abc_ObjIsComplement(pNode) );
+    assert( Abc_ObjIsNode(pNode) );
+    vCone->nSize = 0;
+    Abc_NtkMultiCone_rec( Abc_ObjFanin(pNode,0), vCone );
+    Abc_NtkMultiCone_rec( Abc_ObjFanin(pNode,1), vCone );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index fd5a38e1..8793ce53 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -536,73 +536,6 @@ double Abc_NtkSpacePercentage( Abc_Obj_t * pNode )
 
 
 
-#include "reo.h"
-
-/**Function*************************************************************
-
-  Synopsis    [Reorders BDD of the local function of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NodeBddReorder( reo_man * p, Abc_Obj_t * pNode )
-{
-    Abc_Obj_t * pFanin;
-    DdNode * bFunc;
-    int * pOrder, i;
-    // create the temporary array for the variable order
-    pOrder = ALLOC( int, Abc_ObjFaninNum(pNode) );
-    for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
-        pOrder[i] = -1;
-    // reorder the BDD
-    bFunc = Extra_Reorder( p, pNode->pNtk->pManFunc, pNode->pData, pOrder ); Cudd_Ref( bFunc );
-    Cudd_RecursiveDeref( pNode->pNtk->pManFunc, pNode->pData );
-    pNode->pData = bFunc;
-    // update the fanin order
-    Abc_ObjForEachFanin( pNode, pFanin, i )
-        pOrder[i] = pNode->vFanins.pArray[ pOrder[i] ];
-    Abc_ObjForEachFanin( pNode, pFanin, i )
-        pNode->vFanins.pArray[i] = pOrder[i];
-    free( pOrder );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reorders BDDs of the local functions.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose )
-{
-    reo_man * p;
-    Abc_Obj_t * pNode;
-    int i;
-    p = Extra_ReorderInit( Abc_NtkGetFaninMax(pNtk), 100 );
-    Abc_NtkForEachNode( pNtk, pNode, i )
-    {
-        if ( Abc_ObjFaninNum(pNode) < 3 )
-            continue;
-        if ( fVerbose )
-            fprintf( stdout, "%10s: ", Abc_ObjName(pNode) );
-        if ( fVerbose )
-            fprintf( stdout, "Before = %5d  BDD nodes.  ", Cudd_DagSize(pNode->pData) );
-        Abc_NodeBddReorder( p, pNode );
-        if ( fVerbose )
-            fprintf( stdout, "After = %5d  BDD nodes.\n", Cudd_DagSize(pNode->pData) );
-    }
-    Extra_ReorderQuit( p );
-}
-
-
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index 2e448ce5..a3360953 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -6,7 +6,7 @@
 
   PackageName [Network and node package.]
 
-  Synopsis    [Procedures which transform an AIG into the network of SOP logic nodes.]
+  Synopsis    []
 
   Author      [Alan Mishchenko]
   
@@ -19,22 +19,22 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "reo.h"
+#include "if.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void        Abc_NtkRenodeInt( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
-static Abc_Obj_t * Abc_NtkRenode_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld );
+static int Abc_NtkRenodeEvalBdd( unsigned * pTruth, int nVars );
+static int Abc_NtkRenodeEvalSop( unsigned * pTruth, int nVars );
 
-static DdNode *    Abc_NtkRenodeDeriveBdd_rec( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFanins );
+static reo_man * s_pReo = NULL;
+static DdManager * s_pDd  = NULL;
 
-static void        Abc_NtkRenodeSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax );
-static void        Abc_NtkRenodeSetBoundsCnf( Abc_Ntk_t * pNtk );
-static void        Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk, int nThresh );
-static void        Abc_NtkRenodeSetBoundsSimple( Abc_Ntk_t * pNtk );
-static void        Abc_NtkRenodeSetBoundsFactor( Abc_Ntk_t * pNtk );
-static void        Abc_NtkRenodeCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone );
+typedef int Kit_Graph_t;
+extern DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars );
+extern Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -42,165 +42,70 @@ static void        Abc_NtkRenodeCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone );
 
 /**Function*************************************************************
 
-  Synopsis    [Transforms the AIG into nodes.]
+  Synopsis    [Performs renoding as technology mapping.]
 
-  Description [Threhold is the max number of nodes duplicated at a node.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor )
+Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int fUseBdds, int fVerbose )
 {
+    extern Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
+    If_Par_t Pars, * pPars = &Pars;
     Abc_Ntk_t * pNtkNew;
 
-    assert( Abc_NtkIsStrash(pNtk) );
-    assert( nThresh >= 0 );
-    assert( nFaninMax > 1 );
-
-    // print a warning about choice nodes
-    if ( Abc_NtkGetChoiceNum( pNtk ) )
-        printf( "Warning: The choice nodes in the AIG are removed by renoding.\n" );
-
-    // define the boundary
-    if ( fCnf )
-        Abc_NtkRenodeSetBoundsCnf( pNtk );
-    else if ( fMulti )
-        Abc_NtkRenodeSetBoundsMulti( pNtk, nThresh );
-    else if ( fSimple )
-        Abc_NtkRenodeSetBoundsSimple( pNtk );
-    else if ( fFactor )
-        Abc_NtkRenodeSetBoundsFactor( pNtk );
-    else
-        Abc_NtkRenodeSetBounds( pNtk, nThresh, nFaninMax );
-
-    // perform renoding for this boundary
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
-    Abc_NtkRenodeInt( pNtk, pNtkNew );
-    Abc_NtkFinalize( pNtk, pNtkNew );
-
-    // make the network minimum base
-    Abc_NtkMinimumBase( pNtkNew );
-
-    // fix the problem with complemented and duplicated CO edges
-    Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
-
-    // report the number of CNF objects
-    if ( fCnf )
-    {
-//        int nClauses = Abc_NtkGetClauseNum(pNtkNew) + 2*Abc_NtkPoNum(pNtkNew) + 2*Abc_NtkLatchNum(pNtkNew);
-//        printf( "CNF variables = %d. CNF clauses = %d.\n",  Abc_NtkNodeNum(pNtkNew), nClauses );
-    }
-//printf( "Maximum fanin = %d.\n", Abc_NtkGetFaninMax(pNtkNew) );
-
-    if ( pNtk->pExdc )
-        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
-    // make sure everything is okay
-    if ( !Abc_NtkCheck( pNtkNew ) )
-    {
-        printf( "Abc_NtkRenode: The network check has failed.\n" );
-        Abc_NtkDelete( pNtkNew );
-        return NULL;
+    // set defaults
+    memset( pPars, 0, sizeof(If_Par_t) );
+    // user-controlable paramters
+    pPars->Mode        =  0;
+    pPars->nLutSize    =  nFaninMax;
+    pPars->nCutsMax    = 10;
+    pPars->DelayTarget = -1;
+    pPars->fPreprocess =  1;
+    pPars->fArea       =  0;
+    pPars->fFancy      =  0;
+    pPars->fExpRed     =  0; //
+    pPars->fLatchPaths =  0;
+    pPars->fSeq        =  0;
+    pPars->fVerbose    =  0;
+    // internal parameters
+    pPars->fTruth      =  1;
+    pPars->nLatches    =  0;
+    pPars->pLutLib     =  NULL; // Abc_FrameReadLibLut();
+    pPars->pTimesArr   =  NULL; 
+    pPars->pTimesArr   =  NULL;   
+    pPars->pFuncCost   =  fUseBdds? Abc_NtkRenodeEvalBdd : Abc_NtkRenodeEvalSop;   
+
+    // start the manager
+    if ( fUseBdds )
+    {
+        assert( s_pReo == NULL );
+        s_pDd  = Cudd_Init( nFaninMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+        s_pReo = Extra_ReorderInit( nFaninMax, 100 );
+        pPars->fUseBdds = 1;
+        pPars->pReoMan  = s_pReo;
+    }
+
+    // perform mapping/renoding
+    pNtkNew = Abc_NtkIf( pNtk, pPars );
+
+    // start the manager
+    if ( fUseBdds )
+    {
+        Extra_StopManager( s_pDd );
+        Extra_ReorderQuit( s_pReo );
+        s_pReo = NULL;
+        s_pDd = NULL;
     }
     return pNtkNew;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Transforms the AIG into nodes.]
-
-  Description [Threhold is the max number of nodes duplicated at a node.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkRenodeInt( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
-{
-    ProgressBar * pProgress;
-    Abc_Obj_t * pNode, * pConst1, * pNodeNew;
-    int i;
-
-    // set the constant node
-    pConst1 = Abc_AigConst1(pNtk);
-    if ( Abc_ObjFanoutNum(pConst1) > 0 )
-    {
-        pNodeNew = Abc_NtkCreateNode( pNtkNew );  
-        pNodeNew->pData = Cudd_ReadOne( pNtkNew->pManFunc );   Cudd_Ref( pNodeNew->pData );
-        pConst1->pCopy = pNodeNew;
-    }
-
-    // perform renoding for POs
-    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
-    Abc_NtkForEachCo( pNtk, pNode, i )
-    {
-        Extra_ProgressBarUpdate( pProgress, i, NULL );
-        if ( Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
-            continue;
-        Abc_NtkRenode_rec( pNtkNew, Abc_ObjFanin0(pNode) );
-    }
-    Extra_ProgressBarStop( pProgress );
-
-    // clean the boundaries and data field in the old network
-    Abc_NtkForEachObj( pNtk, pNode, i )
-    {
-        pNode->fMarkA = 0;
-        pNode->pData = NULL;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Find the best multi-input node rooted at the given node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkRenode_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld )
-{
-    Vec_Ptr_t * vCone;
-    Abc_Obj_t * pNodeNew;
-    int i;
-
-    assert( !Abc_ObjIsComplement(pNodeOld) );
-    // return if the result if known
-    if ( pNodeOld->pCopy )
-        return pNodeOld->pCopy;
-    assert( Abc_ObjIsNode(pNodeOld) );
-    assert( !Abc_AigNodeIsConst(pNodeOld) );
-    assert( pNodeOld->fMarkA );
-
-//printf( "%d ", Abc_NodeMffcSizeSupp(pNodeOld) );
-
-    // collect the renoding cone
-    vCone = Vec_PtrAlloc( 10 );
-    Abc_NtkRenodeCone( pNodeOld, vCone );
-
-    // create a new node 
-    pNodeNew = Abc_NtkCreateNode( pNtkNew ); 
-    for ( i = 0; i < vCone->nSize; i++ )
-        Abc_ObjAddFanin( pNodeNew, Abc_NtkRenode_rec(pNtkNew, vCone->pArray[i]) );
-
-    // derive the function of this node
-    pNodeNew->pData = Abc_NtkRenodeDeriveBdd( pNtkNew->pManFunc, pNodeOld, vCone );    
-    Cudd_Ref( pNodeNew->pData );
-    Vec_PtrFree( vCone );
-
-    // remember the node
-    pNodeOld->pCopy = pNodeNew;
-    return pNodeOld->pCopy;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the local BDD of the node.]
+  Synopsis    [Derives the BDD after reordering.]
 
   Description []
                
@@ -209,415 +114,22 @@ Abc_Obj_t * Abc_NtkRenode_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld )
   SeeAlso     []
 
 ***********************************************************************/
-DdNode * Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld )
+int Abc_NtkRenodeEvalBdd( unsigned * pTruth, int nVars )
 {
-    Abc_Obj_t * pFaninOld;
-    DdNode * bFunc;
-    int i;
-    assert( !Abc_AigNodeIsConst(pNodeOld) );
-    assert( Abc_ObjIsNode(pNodeOld) );
-    // set the elementary BDD variables for the input nodes
-    for ( i = 0; i < vFaninsOld->nSize; i++ )
-    {
-        pFaninOld = vFaninsOld->pArray[i];
-        pFaninOld->pData = Cudd_bddIthVar( dd, i );    Cudd_Ref( pFaninOld->pData );
-        pFaninOld->fMarkC = 1;
-    }
-    // call the recursive BDD computation
-    bFunc = Abc_NtkRenodeDeriveBdd_rec( dd, pNodeOld, vFaninsOld );  Cudd_Ref( bFunc );
-    // dereference the intermediate nodes
-    for ( i = 0; i < vFaninsOld->nSize; i++ )
-    {
-        pFaninOld = vFaninsOld->pArray[i];
-        Cudd_RecursiveDeref( dd, pFaninOld->pData );
-        pFaninOld->fMarkC = 0;
-    }
-    Cudd_Deref( bFunc );
-    return bFunc;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the local BDD of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Abc_NtkRenodeDeriveBdd_rec( DdManager * dd, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins )
-{
-    DdNode * bFunc, * bFunc0, * bFunc1;
-    assert( !Abc_ObjIsComplement(pNode) );
-    // if the result is available return
-    if ( pNode->fMarkC )
-    {
-        assert( pNode->pData ); // network has a cycle
-        return pNode->pData;
-    }
-    // mark the node as visited
-    pNode->fMarkC = 1;
-    Vec_PtrPush( vFanins, pNode );
-    // compute the result for both branches
-    bFunc0 = Abc_NtkRenodeDeriveBdd_rec( dd, Abc_ObjFanin(pNode,0), vFanins ); Cudd_Ref( bFunc0 );
-    bFunc1 = Abc_NtkRenodeDeriveBdd_rec( dd, Abc_ObjFanin(pNode,1), vFanins ); Cudd_Ref( bFunc1 );
-    bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pNode) );
-    bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pNode) );
-    // get the final result
-    bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( bFunc );
-    Cudd_RecursiveDeref( dd, bFunc0 );
-    Cudd_RecursiveDeref( dd, bFunc1 );
-    // set the result
-    pNode->pData = bFunc;
-    assert( pNode->pData );
-    return bFunc;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Limits the cones to be no more than the given size.]
-
-  Description [Returns 1 if the last cone was limited. Returns 0 if no changes.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkRenodeLimit_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, int nFaninMax, int fCanStop, int fFirst )
-{
-    int nNodes0, nNodes1;
-    assert( !Abc_ObjIsComplement(pNode) );
-    // check if the node should be added to the fanins
-    if ( !fFirst && (pNode->fMarkA || !Abc_ObjIsNode(pNode)) )
-    {
-        Vec_PtrPushUnique( vCone, pNode );
-        return 0;
-    }
-    // if we cannot stop in this branch, collect all nodes
-    if ( !fCanStop )
-    {
-        Abc_NtkRenodeLimit_rec( Abc_ObjFanin(pNode,0), vCone, nFaninMax, 0, 0 );
-        Abc_NtkRenodeLimit_rec( Abc_ObjFanin(pNode,1), vCone, nFaninMax, 0, 0 );
-        return 0;
-    }
-    // if we can stop, try the left branch first, and return if we stopped
-    assert( vCone->nSize == 0 );
-    if ( Abc_NtkRenodeLimit_rec( Abc_ObjFanin(pNode,0), vCone, nFaninMax, 1, 0 ) )
-        return 1;
-    // save the number of nodes in the left branch and call for the right branch
-    nNodes0 = vCone->nSize;
-    assert( nNodes0 <= nFaninMax );
-    Abc_NtkRenodeLimit_rec( Abc_ObjFanin(pNode,1), vCone, nFaninMax, 0, 0 );
-    // check the number of nodes
-    if ( vCone->nSize <= nFaninMax )
-        return 0;
-    // the number of nodes exceeds the limit
-
-    // get the number of nodes in the right branch
-    vCone->nSize = 0;
-    Abc_NtkRenodeLimit_rec( Abc_ObjFanin(pNode,1), vCone, nFaninMax, 0, 0 );
-    // if this number exceeds the limit, solve the problem for this branch
-    if ( vCone->nSize > nFaninMax )
-    {
-        int RetValue;
-        vCone->nSize = 0;
-        RetValue = Abc_NtkRenodeLimit_rec( Abc_ObjFanin(pNode,1), vCone, nFaninMax, 1, 0 );
-        assert( RetValue == 1 );
-        return 1;
-    }
-
-    nNodes1 = vCone->nSize; 
-    assert( nNodes1 <= nFaninMax );
-    if ( nNodes0 >= nNodes1 )
-    { // the left branch is larger - cut it
-        assert( Abc_ObjFanin(pNode,0)->fMarkA == 0 );
-        Abc_ObjFanin(pNode,0)->fMarkA = 1;
-    }
-    else
-    { // the right branch is larger - cut it
-        assert( Abc_ObjFanin(pNode,1)->fMarkA == 0 );
-        Abc_ObjFanin(pNode,1)->fMarkA = 1;
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Limits the cones to be no more than the given size.]
-
-  Description [Returns 1 if the last cone was limited. Returns 0 if no changes.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkRenodeLimit( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, int nFaninMax )
-{
-    vCone->nSize = 0;
-    return Abc_NtkRenodeLimit_rec( pNode, vCone, nFaninMax, 1, 1 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the expansion boundary for multi-input nodes.]
-
-  Description [The boundary includes the set of PIs and all nodes such that 
-  when expanding over the node we duplicate no more than nThresh nodes.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkRenodeSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax )
-{
-    Vec_Ptr_t * vCone = Vec_PtrAlloc(10);
-    Abc_Obj_t * pNode;
-    int i, nFanouts, nConeSize;
-
-    // make sure the mark is not set
-    Abc_NtkForEachObj( pNtk, pNode, i )
-        assert( pNode->fMarkA == 0 );
-
-    // mark the nodes where expansion stops using pNode->fMarkA
-    Abc_NtkForEachNode( pNtk, pNode, i )
-    {
-        // skip PI/PO nodes
-//        if ( Abc_NodeIsConst(pNode) )
-//            continue;
-        // mark the nodes with multiple fanouts
-        nFanouts = Abc_ObjFanoutNum(pNode);
-        nConeSize = Abc_NodeMffcSize(pNode);
-        if ( (nFanouts - 1) * nConeSize > nThresh )
-            pNode->fMarkA = 1;
-    }
-
-    // mark the PO drivers
-    Abc_NtkForEachCo( pNtk, pNode, i )
-        Abc_ObjFanin0(pNode)->fMarkA = 1;
-
-    // make sure the fanin limit is met
-    Abc_NtkForEachNode( pNtk, pNode, i )
-    {
-        // skip PI/PO nodes
-//        if ( Abc_NodeIsConst(pNode) )
-//            continue;
-        if ( pNode->fMarkA == 0 )
-            continue;
-        // continue cutting branches until it meets the fanin limit
-        while ( Abc_NtkRenodeLimit(pNode, vCone, nFaninMax) );
-        assert( vCone->nSize <= nFaninMax );  
-    }
-    Vec_PtrFree(vCone);
-/*
-    // make sure the fanin limit is met
-    Abc_NtkForEachNode( pNtk, pNode, i )
-    {
-        // skip PI/PO nodes
-//        if ( Abc_NodeIsConst(pNode) )
-//            continue;
-        if ( pNode->fMarkA == 0 )
-            continue;
-        Abc_NtkRenodeCone( pNode, vCone );
-        assert( vCone->nSize <= nFaninMax );    
-    }
-*/
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the expansion boundary for conversion into CNF.]
-
-  Description [The boundary includes the set of PIs, the roots of MUXes,
-  the nodes with multiple fanouts and the nodes with complemented outputs.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkRenodeSetBoundsCnf( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pNode;
-    int i, nMuxes;
-
-    // make sure the mark is not set
-    Abc_NtkForEachObj( pNtk, pNode, i )
-        assert( pNode->fMarkA == 0 );
-
-    // mark the nodes where expansion stops using pNode->fMarkA
-    Abc_NtkForEachNode( pNtk, pNode, i )
-    {
-        // skip PI/PO nodes
-//        if ( Abc_NodeIsConst(pNode) )
-//            continue;
-        // mark the nodes with multiple fanouts
-        if ( Abc_ObjFanoutNum(pNode) > 1 )
-            pNode->fMarkA = 1;
-        // mark the nodes that are roots of MUXes
-        if ( Abc_NodeIsMuxType( pNode ) )
-        {
-            pNode->fMarkA = 1;
-            Abc_ObjFanin0( Abc_ObjFanin0(pNode) )->fMarkA = 1;
-            Abc_ObjFanin0( Abc_ObjFanin1(pNode) )->fMarkA = 1;
-            Abc_ObjFanin1( Abc_ObjFanin0(pNode) )->fMarkA = 1;
-            Abc_ObjFanin1( Abc_ObjFanin1(pNode) )->fMarkA = 1;
-        }
-        else  // mark the complemented edges
-        {
-            if ( Abc_ObjFaninC0(pNode) )
-                Abc_ObjFanin0(pNode)->fMarkA = 1;
-            if ( Abc_ObjFaninC1(pNode) )
-                Abc_ObjFanin1(pNode)->fMarkA = 1;
-        }
-    }
-
-    // mark the PO drivers
-    Abc_NtkForEachCo( pNtk, pNode, i )
-        Abc_ObjFanin0(pNode)->fMarkA = 1;
-
-    // count the number of MUXes
-    nMuxes = 0;
-    Abc_NtkForEachNode( pNtk, pNode, i )
-    {
-        // skip PI/PO nodes
-//        if ( Abc_NodeIsConst(pNode) )
-//            continue;
-        if ( Abc_NodeIsMuxType(pNode) && 
-            Abc_ObjFanin0(pNode)->fMarkA == 0 &&
-            Abc_ObjFanin1(pNode)->fMarkA == 0 )
-            nMuxes++;
-    }
-//    printf( "The number of MUXes detected = %d (%5.2f %% of logic).\n", nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) );
-} 
- 
-/**Function*************************************************************
-
-  Synopsis    [Sets the expansion boundary for conversion into multi-input AND graph.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk, int nThresh )
-{
-    Abc_Obj_t * pNode;
-    int i, nFanouts, nConeSize;
-
-    // make sure the mark is not set
-    Abc_NtkForEachObj( pNtk, pNode, i )
-        assert( pNode->fMarkA == 0 );
-
-    // mark the nodes where expansion stops using pNode->fMarkA
-    Abc_NtkForEachNode( pNtk, pNode, i )
-    {
-        // skip PI/PO nodes
-//        if ( Abc_NodeIsConst(pNode) )
-//            continue;
-        // mark the nodes with multiple fanouts
-//        if ( Abc_ObjFanoutNum(pNode) > 1 )
-//            pNode->fMarkA = 1;
-        // mark the nodes with multiple fanouts
-        nFanouts = Abc_ObjFanoutNum(pNode);
-        nConeSize = Abc_NodeMffcSizeStop(pNode);
-        if ( (nFanouts - 1) * nConeSize > nThresh )
-            pNode->fMarkA = 1;
-        // mark the children if they are pointed by the complemented edges
-        if ( Abc_ObjFaninC0(pNode) )
-            Abc_ObjFanin0(pNode)->fMarkA = 1;
-        if ( Abc_ObjFaninC1(pNode) )
-            Abc_ObjFanin1(pNode)->fMarkA = 1;
-    }
-
-    // mark the PO drivers
-    Abc_NtkForEachCo( pNtk, pNode, i )
-        Abc_ObjFanin0(pNode)->fMarkA = 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets a simple boundary.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkRenodeSetBoundsSimple( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pNode;
-    int i;
-    // make sure the mark is not set
-    Abc_NtkForEachObj( pNtk, pNode, i )
-        assert( pNode->fMarkA == 0 );
-    // mark the nodes where expansion stops using pNode->fMarkA
-    Abc_NtkForEachNode( pNtk, pNode, i )
-        pNode->fMarkA = 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets a factor-cut boundary.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkRenodeSetBoundsFactor( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pNode;
-    int i;
-    // make sure the mark is not set
-    Abc_NtkForEachObj( pNtk, pNode, i )
-        assert( pNode->fMarkA == 0 );
-    // mark the nodes where expansion stops using pNode->fMarkA
-    Abc_NtkForEachNode( pNtk, pNode, i )
-        pNode->fMarkA = (pNode->vFanouts.nSize > 1 && !Abc_NodeIsMuxControlType(pNode));
-    // mark the PO drivers
-    Abc_NtkForEachCo( pNtk, pNode, i )
-        Abc_ObjFanin0(pNode)->fMarkA = 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the fanins of a large node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkRenodeCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone )
-{
-    assert( !Abc_ObjIsComplement(pNode) );
-    if ( pNode->fMarkA || !Abc_ObjIsNode(pNode) )
-    {
-        Vec_PtrPushUnique( vCone, pNode );
-        return;
-    }
-    Abc_NtkRenodeCone_rec( Abc_ObjFanin(pNode,0), vCone );
-    Abc_NtkRenodeCone_rec( Abc_ObjFanin(pNode,1), vCone );
+    DdNode * bFunc, * bFuncNew;
+    int nNodes, nSupport;
+    bFunc = Kit_TruthToBdd( s_pDd, pTruth, nVars );           Cudd_Ref( bFunc );
+    bFuncNew = Extra_Reorder( s_pReo, s_pDd, bFunc, NULL );   Cudd_Ref( bFuncNew );
+    nSupport = Cudd_SupportSize( s_pDd, bFuncNew );
+    nNodes = Cudd_DagSize( bFuncNew );
+    Cudd_RecursiveDeref( s_pDd, bFuncNew );
+    Cudd_RecursiveDeref( s_pDd, bFunc );
+    return (nSupport << 16) | nNodes;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Collects the fanins of a large node.]
+  Synopsis    [Derives the BDD after reordering.]
 
   Description []
                
@@ -626,13 +138,15 @@ void Abc_NtkRenodeCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkRenodeCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone )
+int Abc_NtkRenodeEvalSop( unsigned * pTruth, int nVars )
 {
-    assert( !Abc_ObjIsComplement(pNode) );
-    assert( Abc_ObjIsNode(pNode) );
-    vCone->nSize = 0;
-    Abc_NtkRenodeCone_rec( Abc_ObjFanin(pNode,0), vCone );
-    Abc_NtkRenodeCone_rec( Abc_ObjFanin(pNode,1), vCone );
+    Kit_Graph_t * pGraph;
+    int nNodes, nDepth;
+    pGraph = Kit_TruthToGraph( pTruth, nVars );
+    nNodes = Kit_GraphNodeNum( pGraph );
+    nDepth = Kit_GraphLevelNum( pGraph );
+    Kit_GraphFree( pGraph );
+    return (nDepth << 16) | nNodes;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcReorder.c b/src/base/abci/abcReorder.c
new file mode 100644
index 00000000..d6dee49b
--- /dev/null
+++ b/src/base/abci/abcReorder.c
@@ -0,0 +1,100 @@
+/**CFile****************************************************************
+
+  FileName    [abcReorder.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Reordering local BDDs of the nodes.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcReorder.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "reo.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Reorders BDD of the local function of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeBddReorder( reo_man * p, Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin;
+    DdNode * bFunc;
+    int * pOrder, i;
+    // create the temporary array for the variable order
+    pOrder = ALLOC( int, Abc_ObjFaninNum(pNode) );
+    for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
+        pOrder[i] = -1;
+    // reorder the BDD
+    bFunc = Extra_Reorder( p, pNode->pNtk->pManFunc, pNode->pData, pOrder ); Cudd_Ref( bFunc );
+    Cudd_RecursiveDeref( pNode->pNtk->pManFunc, pNode->pData );
+    pNode->pData = bFunc;
+    // update the fanin order
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        pOrder[i] = pNode->vFanins.pArray[ pOrder[i] ];
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        pNode->vFanins.pArray[i] = pOrder[i];
+    free( pOrder );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reorders BDDs of the local functions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    reo_man * p;
+    Abc_Obj_t * pNode;
+    int i;
+    p = Extra_ReorderInit( Abc_NtkGetFaninMax(pNtk), 100 );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        if ( Abc_ObjFaninNum(pNode) < 3 )
+            continue;
+        if ( fVerbose )
+            fprintf( stdout, "%10s: ", Abc_ObjName(pNode) );
+        if ( fVerbose )
+            fprintf( stdout, "Before = %5d  BDD nodes.  ", Cudd_DagSize(pNode->pData) );
+        Abc_NodeBddReorder( p, pNode );
+        if ( fVerbose )
+            fprintf( stdout, "After = %5d  BDD nodes.\n", Cudd_DagSize(pNode->pData) );
+    }
+    Extra_ReorderQuit( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index ad58e35c..f4717eda 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -46,6 +46,7 @@ static void  Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2,
 ***********************************************************************/
 void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit )
 {
+    extern Abc_Ntk_t * Abc_NtkMulti( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
     Abc_Ntk_t * pMiter;
     Abc_Ntk_t * pCnf;
     int RetValue;
@@ -76,7 +77,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // convert the miter into a CNF
-    pCnf = Abc_NtkRenode( pMiter, 0, 100, 1, 0, 0, 0 );
+    pCnf = Abc_NtkMulti( pMiter, 0, 100, 1, 0, 0, 0 );
     Abc_NtkDelete( pMiter );
     if ( pCnf == NULL )
     {
@@ -207,6 +208,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
 ***********************************************************************/
 void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit, int nFrames )
 {
+    extern Abc_Ntk_t * Abc_NtkMulti( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
     Abc_Ntk_t * pMiter;
     Abc_Ntk_t * pFrames;
     Abc_Ntk_t * pCnf;
@@ -256,7 +258,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // convert the miter into a CNF
-    pCnf = Abc_NtkRenode( pFrames, 0, 100, 1, 0, 0, 0 );
+    pCnf = Abc_NtkMulti( pFrames, 0, 100, 1, 0, 0, 0 );
     Abc_NtkDelete( pFrames );
     if ( pCnf == NULL )
     {
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 04ed07a7..7e674fbe 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -21,6 +21,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcMap.c \
     src/base/abci/abcMini.c \
     src/base/abci/abcMiter.c \
+    src/base/abci/abcMulti.c \
     src/base/abci/abcNtbdd.c \
     src/base/abci/abcOrder.c \
     src/base/abci/abcPrint.c \
@@ -28,6 +29,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcReconv.c \
     src/base/abci/abcRefactor.c \
     src/base/abci/abcRenode.c \
+    src/base/abci/abcReorder.c \
     src/base/abci/abcRestruct.c \
     src/base/abci/abcResub.c \
     src/base/abci/abcRewrite.c \
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 31c07528..32bb07f8 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -70,21 +70,27 @@ typedef struct If_Cut_t_     If_Cut_t;
 // parameters
 struct If_Par_t_
 {
+    // user-controlable paramters
     int                Mode;          // the mapping mode
     int                nLutSize;      // the LUT size
-    If_Lib_t *         pLutLib;       // the LUT library
     int                nCutsMax;      // the max number of cuts
-    int                fVerbose;      // the verbosity flag
+    float              DelayTarget;   // delay target
     int                fPreprocess;   // preprossing
     int                fArea;         // area-oriented mapping
     int                fFancy;        // a fancy feature
     int                fExpRed;       // expand/reduce of the best cuts
     int                fLatchPaths;   // reset timing on latch paths
     int                fSeq;          // sequential mapping
-    int                nLatches;      // the number of latches
-    float              DelayTarget;   // delay target
+    int                fVerbose;      // the verbosity flag
+    // internal parameters
+    int                fTruth;        // truth table computation enabled
+    int                fUseBdds;      // sets local BDDs at the nodes
+    int                nLatches;      // the number of latches in seq mapping
+    If_Lib_t *         pLutLib;       // the LUT library
     float *            pTimesArr;     // arrival times
     float *            pTimesReq;     // required times
+    int(*pFuncCost)(unsigned *, int); // procedure the user's cost of a cut
+    void *             pReoMan;       // reordering manager
 };
 
 // the LUT library
@@ -118,10 +124,13 @@ struct If_Man_t_
     int                nCutsMerged;   // the total number of cuts merged
     int                nCutsMax;      // the maximum number of cuts at a node
     float              Fi;            // the current value of the clock period (for seq mapping)
+    unsigned *         puTemp[4];     // used for the truth table computation
     // memory management
     Mem_Fixed_t *      pMem;          // memory manager
     int                nEntrySize;    // the size of the entry
     int                nEntryBase;    // the size of the entry minus cut leaf arrays
+    int                nTruthSize;    // the size of the truth table if allocated
+    int                nCutSize;      // the size of the cut
     // temporary cut storage
     int                nCuts;         // the number of cuts used
     If_Cut_t **        ppCuts;        // the storage space for cuts
@@ -132,14 +141,14 @@ struct If_Cut_t_
 {
     float              Delay;         // delay of the cut
     float              Area;          // area (or area-flow) of the cut
-    If_Cut_t *         pOne;          // parent cut
-    If_Cut_t *         pTwo;          // parent cut
     unsigned           uSign;         // cut signature
-    char               fCompl0;       // complemented attribute
-    char               fCompl1;       // complemented attribute
-    char               Phase;         // complemented attribute
-    char               nLeaves;       // number of leaves
+    unsigned           Cost    : 10;  // the user's cost of the cut
+    unsigned           Depth   :  9;  // the user's depth of the cut
+    unsigned           fCompl  :  1;  // the complemented attribute 
+    unsigned           nLimit  :  6;  // the maximum number of leaves
+    unsigned           nLeaves :  6;  // the number of leaves
     int *              pLeaves;       // array of fanins
+    unsigned *         pTruth;        // the truth table
 };
 
 // node extension
@@ -197,8 +206,11 @@ static inline unsigned   If_ObjCutSign( unsigned ObjId )                     { r
 static inline void *     If_CutData( If_Cut_t * pCut )                       { return *(void **)pCut;                }
 static inline void       If_CutSetData( If_Cut_t * pCut, void * pData )      { *(void **)pCut = pData;               }
 
-static inline float      If_CutLutDelay( If_Man_t * p, If_Cut_t * pCut )     { return p->pPars->pLutLib? p->pPars->pLutLib->pLutDelays[pCut->nLeaves] : (float)1.0;  }
-static inline float      If_CutLutArea( If_Man_t * p, If_Cut_t * pCut )      { return p->pPars->pLutLib? p->pPars->pLutLib->pLutAreas[pCut->nLeaves]  : (float)1.0;  }
+static inline int        If_CutTruthWords( int nVarsMax )                    { return nVarsMax <= 5 ? 1 : (1 << (nVarsMax - 5)); }
+static inline unsigned * If_CutTruth( If_Cut_t * pCut )                      { return pCut->pTruth;                              }
+
+static inline float      If_CutLutDelay( If_Man_t * p, If_Cut_t * pCut )     { return pCut->Depth? (float)pCut->Depth : (p->pPars->pLutLib? p->pPars->pLutLib->pLutDelays[pCut->nLeaves] : (float)1.0);  }
+static inline float      If_CutLutArea( If_Man_t * p, If_Cut_t * pCut )      { return pCut->Cost?  (float)pCut->Cost  : (p->pPars->pLutLib? p->pPars->pLutLib->pLutAreas[pCut->nLeaves]  : (float)1.0);  }
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
@@ -244,14 +256,7 @@ static inline float      If_CutLutArea( If_Man_t * p, If_Cut_t * pCut )      { r
 /*=== ifCore.c ==========================================================*/
 extern int             If_ManPerformMapping( If_Man_t * p );
 extern int             If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fRequired );
-/*=== ifMan.c ==========================================================*/
-extern If_Man_t *      If_ManStart( If_Par_t * pPars );
-extern void            If_ManStop( If_Man_t * p );
-extern If_Obj_t *      If_ManCreatePi( If_Man_t * p );
-extern If_Obj_t *      If_ManCreatePo( If_Man_t * p, If_Obj_t * pDriver, int fCompl0 );
-extern If_Obj_t *      If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_t * pFan1, int fCompl1 );
-/*=== ifMap.c ==========================================================*/
-extern void            If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode );
+/*=== ifCut.c ==========================================================*/
 extern float           If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut, int nLevels );
 extern float           If_CutAreaRefed( If_Man_t * p, If_Cut_t * pCut, int nLevels );
 extern float           If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels );
@@ -259,12 +264,26 @@ extern float           If_CutRef( If_Man_t * p, If_Cut_t * pCut, int nLevels );
 extern void            If_CutPrint( If_Man_t * p, If_Cut_t * pCut );
 extern float           If_CutDelay( If_Man_t * p, If_Cut_t * pCut );
 extern float           If_CutFlow( If_Man_t * p, If_Cut_t * pCut );
-extern int             If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut, int nLimit );
+extern int             If_CutFilter( If_Man_t * p, If_Cut_t * pCut );
+extern int             If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut );
 extern void            If_CutCopy( If_Cut_t * pCutDest, If_Cut_t * pCutSrc );
+extern void            If_ManSortCuts( If_Man_t * p, int Mode );
+/*=== ifMan.c ==========================================================*/
+extern If_Man_t *      If_ManStart( If_Par_t * pPars );
+extern void            If_ManStop( If_Man_t * p );
+extern If_Obj_t *      If_ManCreatePi( If_Man_t * p );
+extern If_Obj_t *      If_ManCreatePo( If_Man_t * p, If_Obj_t * pDriver, int fCompl0 );
+extern If_Obj_t *      If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_t * pFan1, int fCompl1 );
+/*=== ifMap.c ==========================================================*/
+extern void            If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode );
+/*=== ifPrepro.c ==========================================================*/
+extern void            If_ManPerformMappingPreprocess( If_Man_t * p );
 /*=== ifReduce.c ==========================================================*/
 extern void            If_ManImproveMapping( If_Man_t * p );
-/*=== ifSelect.c ==========================================================*/
-extern void            If_ManPerformMappingPreprocess( If_Man_t * p );
+/*=== ifSeq.c ==========================================================*/
+extern int             If_ManPerformMappingSeq( If_Man_t * p );
+/*=== ifTruth.c ==========================================================*/
+extern void            If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
 /*=== ifUtil.c ==========================================================*/
 extern float           If_ManDelayMax( If_Man_t * p );
 extern void            If_ManCleanNodeCopy( If_Man_t * p );
diff --git a/src/map/if/ifCore.c b/src/map/if/ifCore.c
index e139e14b..c5000dbe 100644
--- a/src/map/if/ifCore.c
+++ b/src/map/if/ifCore.c
@@ -59,20 +59,20 @@ int If_ManPerformMapping( If_Man_t * p )
     else
         If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 1 );
     // try to improve area by expanding and reducing the cuts
-    if ( p->pPars->fExpRed )
+    if ( p->pPars->fExpRed && !p->pPars->fTruth )
         If_ManImproveMapping( p );
     // area flow oriented mapping
     for ( i = 0; i < nItersFlow; i++ )
     {
         If_ManPerformMappingRound( p, p->pPars->nCutsMax, 1, 1 );
-        if ( p->pPars->fExpRed )
+        if ( p->pPars->fExpRed && !p->pPars->fTruth )
             If_ManImproveMapping( p );
     }
     // area oriented mapping
     for ( i = 0; i < nItersArea; i++ )
     {
         If_ManPerformMappingRound( p, p->pPars->nCutsMax, 2, 1 );
-        if ( p->pPars->fExpRed )
+        if ( p->pPars->fExpRed && !p->pPars->fTruth )
             If_ManImproveMapping( p );
     }
     if ( p->pPars->fVerbose )
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index 0318e5e5..56e354ce 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -28,9 +28,405 @@
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pDom is contained in pCut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int If_CutCheckDominance( If_Cut_t * pDom, If_Cut_t * pCut )
+{
+    int i, k;
+    for ( i = 0; i < (int)pDom->nLeaves; i++ )
+    {
+        for ( k = 0; k < (int)pCut->nLeaves; k++ )
+            if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
+                break;
+        if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut
+            return 0;
+    }
+    // every node in pDom is contained in pCut
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pDom is equal to pCut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int If_CutCheckEquality( If_Cut_t * pDom, If_Cut_t * pCut )
+{
+    int i;
+    if ( (int)pDom->nLeaves != (int)pCut->nLeaves )
+        return 0;
+    for ( i = 0; i < (int)pDom->nLeaves; i++ )
+        if ( pDom->pLeaves[i] != pCut->pLeaves[i] )
+            return 0;
+    return 1;
+}
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the cut is contained.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_CutFilter( If_Man_t * p, If_Cut_t * pCut )
+{
+    If_Cut_t * pTemp;
+    int i;
+    for ( i = 0; i < p->nCuts; i++ )
+    {
+        pTemp = p->ppCuts[i];
+        if ( pTemp->nLeaves > pCut->nLeaves )
+        {
+//            continue;
+            // skip the non-contained cuts
+            if ( (pTemp->uSign & pCut->uSign) != pCut->uSign )
+                continue;
+            // check containment seriously
+            if ( If_CutCheckDominance( pCut, pTemp ) )
+            {
+                // removed contained cut
+                p->ppCuts[i] = p->ppCuts[p->nCuts-1];
+                p->ppCuts[p->nCuts-1] = pTemp;
+                p->nCuts--;
+                i--;
+            }
+         }
+        else
+        {
+            // skip the non-contained cuts
+            if ( (pTemp->uSign & pCut->uSign) != pTemp->uSign )
+                continue;
+            // check containment seriously
+            if ( If_CutCheckDominance( pTemp, pCut ) )
+                return 1;
+        }
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int If_CutMergeOrdered( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC )
+{ 
+    int i, k, c;
+    assert( pC0->nLeaves >= pC1->nLeaves );
+    // the case of the largest cut sizes
+    if ( pC0->nLeaves == pC->nLimit && pC1->nLeaves == pC->nLimit )
+    {
+        for ( i = 0; i < (int)pC0->nLeaves; i++ )
+            if ( pC0->pLeaves[i] != pC1->pLeaves[i] )
+                return 0;
+        for ( i = 0; i < (int)pC0->nLeaves; i++ )
+            pC->pLeaves[i] = pC0->pLeaves[i];
+        pC->nLeaves = pC0->nLeaves;
+        return 1;
+    }
+    // the case when one of the cuts is the largest
+    if ( pC0->nLeaves == pC->nLimit )
+    {
+        for ( i = 0; i < (int)pC1->nLeaves; i++ )
+        {
+            for ( k = (int)pC0->nLeaves - 1; k >= 0; k-- )
+                if ( pC0->pLeaves[k] == pC1->pLeaves[i] )
+                    break;
+            if ( k == -1 ) // did not find
+                return 0;
+        }
+        for ( i = 0; i < (int)pC0->nLeaves; i++ )
+            pC->pLeaves[i] = pC0->pLeaves[i];
+        pC->nLeaves = pC0->nLeaves;
+        return 1;
+    }
+
+    // compare two cuts with different numbers
+    i = k = 0;
+    for ( c = 0; c < (int)pC->nLimit; c++ )
+    {
+        if ( k == (int)pC1->nLeaves )
+        {
+            if ( i == (int)pC0->nLeaves )
+            {
+                pC->nLeaves = c;
+                return 1;
+            }
+            pC->pLeaves[c] = pC0->pLeaves[i++];
+            continue;
+        }
+        if ( i == (int)pC0->nLeaves )
+        {
+            if ( k == (int)pC1->nLeaves )
+            {
+                pC->nLeaves = c;
+                return 1;
+            }
+            pC->pLeaves[c] = pC1->pLeaves[k++];
+            continue;
+        }
+        if ( pC0->pLeaves[i] < pC1->pLeaves[k] )
+        {
+            pC->pLeaves[c] = pC0->pLeaves[i++];
+            continue;
+        }
+        if ( pC0->pLeaves[i] > pC1->pLeaves[k] )
+        {
+            pC->pLeaves[c] = pC1->pLeaves[k++];
+            continue;
+        }
+        pC->pLeaves[c] = pC0->pLeaves[i++]; 
+        k++;
+    }
+    if ( i < (int)pC0->nLeaves || k < (int)pC1->nLeaves )
+        return 0;
+    pC->nLeaves = c;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two cuts.]
+
+  Description [Special case when the cut is known to exist.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int If_CutMergeOrdered2( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC )
+{ 
+    int i, k, c;
+    assert( pC0->nLeaves >= pC1->nLeaves );
+    // copy the first cut
+    for ( i = 0; i < (int)pC0->nLeaves; i++ )
+        pC->pLeaves[i] = pC0->pLeaves[i];
+    pC->nLeaves = pC0->nLeaves;
+    // the case when one of the cuts is the largest
+    if ( pC0->nLeaves == pC->nLimit )
+        return 1;
+    // add nodes of the second cut
+    k = 0;
+    for ( i = 0; i < (int)pC1->nLeaves; i++ )
+    {
+        // find k-th node before which i-th node should be added
+        for ( ; k < (int)pC->nLeaves; k++ )
+            if ( pC->pLeaves[k] >= pC1->pLeaves[i] )
+                break;
+        // check the case when this should be the last node
+        if ( k == (int)pC->nLeaves )
+        {
+            pC->pLeaves[k++] = pC1->pLeaves[i];
+            pC->nLeaves++;
+            continue;
+        }
+        // check the case when equal node is found
+        if ( pC1->pLeaves[i] == pC->pLeaves[k] )
+            continue;
+        // add the node
+        for ( c = (int)pC->nLeaves; c > k; c-- )
+            pC->pLeaves[c] = pC->pLeaves[c-1];
+        pC->pLeaves[k++] = pC1->pLeaves[i];
+        pC->nLeaves++;
+    }
+    assert( pC->nLeaves <= pC->nLimit );
+    for ( i = 1; i < (int)pC->nLeaves; i++ )
+        assert( pC->pLeaves[i-1] < pC->pLeaves[i] );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the object for FPGA mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut )
+{ 
+    assert( pCut->nLimit > 0 );
+    // merge the nodes
+    if ( pCut0->nLeaves < pCut1->nLeaves )
+    {
+        if ( !If_CutMergeOrdered( pCut1, pCut0, pCut ) )
+            return 0;
+    }
+    else
+    {
+        if ( !If_CutMergeOrdered( pCut0, pCut1, pCut ) )
+            return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the object for FPGA mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_CutCompareDelay( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
+{
+    If_Cut_t * pC0 = *ppC0;
+    If_Cut_t * pC1 = *ppC1;
+    if ( pC0->Delay < pC1->Delay - 0.0001 )
+        return -1;
+    if ( pC0->Delay > pC1->Delay + 0.0001 )
+        return 1;
+    if ( pC0->nLeaves < pC1->nLeaves )
+        return -1;
+    if ( pC0->nLeaves > pC1->nLeaves )
+        return 1;
+    if ( pC0->Area < pC1->Area - 0.0001 )
+        return -1;
+    if ( pC0->Area > pC1->Area + 0.0001 )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the object for FPGA mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_CutCompareDelayOld( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
+{
+    If_Cut_t * pC0 = *ppC0;
+    If_Cut_t * pC1 = *ppC1;
+    if ( pC0->Delay < pC1->Delay - 0.0001 )
+        return -1;
+    if ( pC0->Delay > pC1->Delay + 0.0001 )
+        return 1;
+    if ( pC0->Area < pC1->Area - 0.0001 )
+        return -1;
+    if ( pC0->Area > pC1->Area + 0.0001 )
+        return 1;
+    if ( pC0->nLeaves < pC1->nLeaves )
+        return -1;
+    if ( pC0->nLeaves > pC1->nLeaves )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the object for FPGA mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_CutCompareArea( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
+{
+    If_Cut_t * pC0 = *ppC0;
+    If_Cut_t * pC1 = *ppC1;
+    if ( pC0->Area < pC1->Area - 0.0001 )
+        return -1;
+    if ( pC0->Area > pC1->Area + 0.0001 )
+        return 1;
+    if ( pC0->nLeaves < pC1->nLeaves )
+        return -1;
+    if ( pC0->nLeaves > pC1->nLeaves )
+        return 1;
+    if ( pC0->Delay < pC1->Delay - 0.0001 )
+        return -1;
+    if ( pC0->Delay > pC1->Delay + 0.0001 )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorts the cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManSortCuts( If_Man_t * p, int Mode )
+{
+    // sort the cuts
+    if ( Mode || p->pPars->fArea ) // area
+        qsort( p->ppCuts, p->nCuts, sizeof(If_Cut_t *), (int (*)(const void *, const void *))If_CutCompareArea );
+    else if ( p->pPars->fFancy )
+        qsort( p->ppCuts, p->nCuts, sizeof(If_Cut_t *), (int (*)(const void *, const void *))If_CutCompareDelayOld );
+    else
+        qsort( p->ppCuts, p->nCuts, sizeof(If_Cut_t *), (int (*)(const void *, const void *))If_CutCompareDelay );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes delay.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float If_CutDelay( If_Man_t * p, If_Cut_t * pCut )
+{
+    If_Obj_t * pLeaf;
+    float Delay;
+    int i;
+    assert( pCut->nLeaves > 1 );
+    Delay = -IF_FLOAT_LARGE;
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+        Delay = IF_MAX( Delay, If_ObjCutBest(pLeaf)->Delay );
+    return Delay + If_CutLutDelay(p, pCut);
+}
+
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Computes area flow.]
 
   Description []
                
@@ -39,6 +435,166 @@
   SeeAlso     []
 
 ***********************************************************************/
+float If_CutFlow( If_Man_t * p, If_Cut_t * pCut )
+{
+    If_Obj_t * pLeaf;
+    float Flow;
+    int i;
+    assert( pCut->nLeaves > 1 );
+    Flow = If_CutLutArea(p, pCut);
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+    {
+        if ( pLeaf->nRefs == 0 )
+            Flow += If_ObjCutBest(pLeaf)->Area;
+        else
+        {
+            assert( pLeaf->EstRefs > p->fEpsilon );
+            Flow += If_ObjCutBest(pLeaf)->Area / pLeaf->EstRefs;
+        }
+    }
+    return Flow;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area of the first level.]
+
+  Description [The cut need to be derefed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels )
+{
+    If_Obj_t * pLeaf;
+    float Area;
+    int i;
+    Area = If_CutLutArea(p, pCut);
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+    {
+        assert( pLeaf->nRefs > 0 );
+        if ( --pLeaf->nRefs > 0 || !If_ObjIsAnd(pLeaf) || nLevels == 1 )
+            continue;
+        Area += If_CutDeref( p, If_ObjCutBest(pLeaf), nLevels - 1 );
+    }
+    return Area;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area of the first level.]
+
+  Description [The cut need to be derefed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float If_CutRef( If_Man_t * p, If_Cut_t * pCut, int nLevels )
+{
+    If_Obj_t * pLeaf;
+    float Area;
+    int i;
+    Area = If_CutLutArea(p, pCut);
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+    {
+        assert( pLeaf->nRefs >= 0 );
+        if ( pLeaf->nRefs++ > 0 || !If_ObjIsAnd(pLeaf) || nLevels == 1 )
+            continue;
+        Area += If_CutRef( p, If_ObjCutBest(pLeaf), nLevels - 1 );
+    }
+    return Area;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_CutPrint( If_Man_t * p, If_Cut_t * pCut )
+{
+    unsigned i;
+    printf( "{" );
+    for ( i = 0; i < pCut->nLeaves; i++ )
+        printf( " %d", pCut->pLeaves[i] );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area of the first level.]
+
+  Description [The cut need to be derefed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut, int nLevels )
+{
+    float aResult, aResult2;
+    assert( pCut->nLeaves > 1 );
+    aResult2 = If_CutRef( p, pCut, nLevels );
+    aResult  = If_CutDeref( p, pCut, nLevels );
+    assert( aResult == aResult2 );
+    return aResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area of the first level.]
+
+  Description [The cut need to be derefed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float If_CutAreaRefed( If_Man_t * p, If_Cut_t * pCut, int nLevels )
+{
+    float aResult, aResult2;
+    assert( pCut->nLeaves > 1 );
+    aResult2 = If_CutDeref( p, pCut, nLevels );
+    aResult  = If_CutRef( p, pCut, nLevels );
+    assert( aResult == aResult2 );
+    return aResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area of the first level.]
+
+  Description [The cut need to be derefed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_CutCopy( If_Cut_t * pCutDest, If_Cut_t * pCutSrc )
+{
+    int * pLeaves;
+    unsigned * pTruth;
+    pLeaves = pCutDest->pLeaves;
+    pTruth  = pCutDest->pTruth;
+    *pCutDest = *pCutSrc;
+    pCutDest->pLeaves = pLeaves;
+    pCutDest->pTruth  = pTruth;
+    memcpy( pCutDest->pLeaves, pCutSrc->pLeaves, sizeof(int) * pCutSrc->nLeaves );
+    if ( pCutSrc->pTruth )
+    memcpy( pCutDest->pTruth,  pCutSrc->pTruth,  sizeof(unsigned) * If_CutTruthWords(pCutSrc->nLimit) );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index b0c12fea..9e3d8e88 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -57,9 +57,20 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
     p->vMapped = Vec_PtrAlloc( 100 );
     p->vTemp   = Vec_PtrAlloc( 100 );
     // prepare the memory manager
-    p->nEntrySize = sizeof(If_Obj_t) + p->pPars->nCutsMax * (sizeof(If_Cut_t) + sizeof(int) * p->pPars->nLutSize);
-    p->nEntryBase = sizeof(If_Obj_t) + p->pPars->nCutsMax * (sizeof(If_Cut_t));
+    p->nTruthSize = p->pPars->fTruth? If_CutTruthWords( p->pPars->nLutSize ) : 0;
+    p->nCutSize   = sizeof(If_Cut_t) + sizeof(int) * p->pPars->nLutSize + sizeof(unsigned) * p->nTruthSize;
+    p->nEntrySize = sizeof(If_Obj_t) + p->pPars->nCutsMax * p->nCutSize;
+    p->nEntryBase = sizeof(If_Obj_t) + p->pPars->nCutsMax * sizeof(If_Cut_t);
     p->pMem = Mem_FixedStart( p->nEntrySize );
+    // report expected memory usage
+    if ( p->pPars->fVerbose )
+        printf( "Memory (bytes): Truth = %3d. Cut = %3d. Entry = %4d. Total = %.2f Mb / 1K AIG nodes\n", 
+            4 * p->nTruthSize, p->nCutSize, p->nEntrySize, 1000.0 * p->nEntrySize / (1<<20) );
+    // room for temporary truth tables
+    p->puTemp[0] = p->pPars->fTruth? ALLOC( unsigned, 4 * p->nTruthSize ) : NULL;
+    p->puTemp[1] = p->puTemp[0] + p->nTruthSize;
+    p->puTemp[2] = p->puTemp[1] + p->nTruthSize;
+    p->puTemp[3] = p->puTemp[2] + p->nTruthSize;
     // create the constant node
     p->pConst1 = If_ManSetupObj( p );
     p->pConst1->Type = IF_CONST1;
@@ -100,6 +111,7 @@ void If_ManStop( If_Man_t * p )
     for ( i = 1; i < 1 + p->pPars->nCutsMax * p->pPars->nCutsMax; i++ )
         if ( pTemp > p->ppCuts[i] )
             pTemp = p->ppCuts[i];
+    FREE( p->puTemp[0] );
     free( pTemp );
     free( p->ppCuts );
     free( p );
@@ -200,7 +212,12 @@ If_Obj_t * If_ManSetupObj( If_Man_t * p )
     // organize memory
     pArrays = (int *)((char *)pObj + p->nEntryBase);
     for ( i = 0; i < p->pPars->nCutsMax; i++ )
-        pObj->Cuts[i].pLeaves = pArrays + i * p->pPars->nLutSize;
+    {
+        pCut = pObj->Cuts + i;
+        pCut->nLimit  = p->pPars->nLutSize;
+        pCut->pLeaves = pArrays + i * p->pPars->nLutSize;
+        pCut->pTruth  = pArrays + p->pPars->nCutsMax * p->pPars->nLutSize + i * p->nTruthSize;
+    }
     // assign ID and save 
     pObj->Id = Vec_PtrSize(p->vObjs);
     Vec_PtrPush( p->vObjs, pObj );
@@ -230,22 +247,24 @@ If_Obj_t * If_ManSetupObj( If_Man_t * p )
 If_Cut_t ** If_ManSetupCuts( If_Man_t * p )
 {
     If_Cut_t ** pCutStore;
-    int * pArrays, nCutSize, nCutsTotal, i;
+    int * pArrays, nCutsTotal, i;
     // decide how many cuts to alloc
     nCutsTotal = 1 + p->pPars->nCutsMax * p->pPars->nCutsMax;
-    // figure out the cut size
-    nCutSize = sizeof(If_Cut_t) + sizeof(int) * p->pPars->nLutSize;
     // allocate and clean space for cuts
     pCutStore = (If_Cut_t **)ALLOC( If_Cut_t *, (nCutsTotal + 1) );
     memset( pCutStore, 0, sizeof(If_Cut_t *) * (nCutsTotal + 1) );
-    pCutStore[0] = (If_Cut_t *)ALLOC( char, nCutSize * nCutsTotal );
-    memset( pCutStore[0], 0, nCutSize * nCutsTotal );
-    for ( i = 1; i < nCutsTotal; i++ )
-        pCutStore[i] = (If_Cut_t *)((char *)pCutStore[0] + sizeof(If_Cut_t) * i);
-    // assign room for cut leaves
+    pCutStore[0] = (If_Cut_t *)ALLOC( char, p->nCutSize * nCutsTotal );
+    memset( pCutStore[0], 0, p->nCutSize * nCutsTotal );
+    // assign cut paramters and space for the cut leaves
+    assert( sizeof(int) == sizeof(unsigned) );
     pArrays = (int *)((char *)pCutStore[0] + sizeof(If_Cut_t) * nCutsTotal);
     for ( i = 0; i < nCutsTotal; i++ )
+    {
+        pCutStore[i] = (If_Cut_t *)((char *)pCutStore[0] + sizeof(If_Cut_t) * i);
+        pCutStore[i]->nLimit  = p->pPars->nLutSize;
         pCutStore[i]->pLeaves = pArrays + i * p->pPars->nLutSize;
+        pCutStore[i]->pTruth  = pArrays + nCutsTotal * p->pPars->nLutSize + i * p->nTruthSize;
+    }
     return pCutStore;
 }
 
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 9134dc9a..76c524ee 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -59,567 +59,6 @@ static inline int If_WordCountOnes( unsigned uWord )
 
 /**Function*************************************************************
 
-  Synopsis    [Returns 1 if pDom is contained in pCut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int If_CutCheckDominance( If_Cut_t * pDom, If_Cut_t * pCut )
-{
-    int i, k;
-    for ( i = 0; i < (int)pDom->nLeaves; i++ )
-    {
-        for ( k = 0; k < (int)pCut->nLeaves; k++ )
-            if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
-                break;
-        if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut
-            return 0;
-    }
-    // every node in pDom is contained in pCut
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if pDom is equal to pCut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int If_CutCheckEquality( If_Cut_t * pDom, If_Cut_t * pCut )
-{
-    int i;
-    if ( (int)pDom->nLeaves != (int)pCut->nLeaves )
-        return 0;
-    for ( i = 0; i < (int)pDom->nLeaves; i++ )
-        if ( pDom->pLeaves[i] != pCut->pLeaves[i] )
-            return 0;
-    return 1;
-}
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the cut is contained.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int If_CutFilter( If_Man_t * p, If_Cut_t * pCut, int Mode )
-{
-    If_Cut_t * pTemp;
-    int i;
-    for ( i = 0; i < p->nCuts; i++ )
-    {
-        pTemp = p->ppCuts[i];
-        if ( pTemp->nLeaves > pCut->nLeaves )
-        {
-//            continue;
-            // skip the non-contained cuts
-            if ( (pTemp->uSign & pCut->uSign) != pCut->uSign )
-                continue;
-            // check containment seriously
-            if ( If_CutCheckDominance( pCut, pTemp ) )
-            {
-                // removed contained cut
-                p->ppCuts[i] = p->ppCuts[p->nCuts-1];
-                p->ppCuts[p->nCuts-1] = pTemp;
-                p->nCuts--;
-                i--;
-            }
-         }
-        else
-        {
-            // skip the non-contained cuts
-            if ( (pTemp->uSign & pCut->uSign) != pTemp->uSign )
-                continue;
-            // check containment seriously
-            if ( If_CutCheckDominance( pTemp, pCut ) )
-                return 1;
-        }
-    }
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Merges two cuts.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int If_CutMergeOrdered( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC, int nLimit )
-{ 
-    int i, k, c;
-    assert( pC0->nLeaves >= pC1->nLeaves );
-    // the case of the largest cut sizes
-    if ( pC0->nLeaves == nLimit && pC1->nLeaves == nLimit )
-    {
-        for ( i = 0; i < pC0->nLeaves; i++ )
-            if ( pC0->pLeaves[i] != pC1->pLeaves[i] )
-                return 0;
-        for ( i = 0; i < pC0->nLeaves; i++ )
-            pC->pLeaves[i] = pC0->pLeaves[i];
-        pC->nLeaves = pC0->nLeaves;
-        return 1;
-    }
-    // the case when one of the cuts is the largest
-    if ( pC0->nLeaves == nLimit )
-    {
-        for ( i = 0; i < pC1->nLeaves; i++ )
-        {
-            for ( k = pC0->nLeaves - 1; k >= 0; k-- )
-                if ( pC0->pLeaves[k] == pC1->pLeaves[i] )
-                    break;
-            if ( k == -1 ) // did not find
-                return 0;
-        }
-        for ( i = 0; i < pC0->nLeaves; i++ )
-            pC->pLeaves[i] = pC0->pLeaves[i];
-        pC->nLeaves = pC0->nLeaves;
-        return 1;
-    }
-
-    // compare two cuts with different numbers
-    i = k = 0;
-    for ( c = 0; c < nLimit; c++ )
-    {
-        if ( k == pC1->nLeaves )
-        {
-            if ( i == pC0->nLeaves )
-            {
-                pC->nLeaves = c;
-                return 1;
-            }
-            pC->pLeaves[c] = pC0->pLeaves[i++];
-            continue;
-        }
-        if ( i == pC0->nLeaves )
-        {
-            if ( k == pC1->nLeaves )
-            {
-                pC->nLeaves = c;
-                return 1;
-            }
-            pC->pLeaves[c] = pC1->pLeaves[k++];
-            continue;
-        }
-        if ( pC0->pLeaves[i] < pC1->pLeaves[k] )
-        {
-            pC->pLeaves[c] = pC0->pLeaves[i++];
-            continue;
-        }
-        if ( pC0->pLeaves[i] > pC1->pLeaves[k] )
-        {
-            pC->pLeaves[c] = pC1->pLeaves[k++];
-            continue;
-        }
-        pC->pLeaves[c] = pC0->pLeaves[i++]; 
-        k++;
-    }
-    if ( i < pC0->nLeaves || k < pC1->nLeaves )
-        return 0;
-    pC->nLeaves = c;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Merges two cuts.]
-
-  Description [Special case when the cut is known to exist.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int If_CutMergeOrdered2( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC, int nLimit )
-{ 
-    int i, k, c;
-    assert( pC0->nLeaves >= pC1->nLeaves );
-    // copy the first cut
-    for ( i = 0; i < pC0->nLeaves; i++ )
-        pC->pLeaves[i] = pC0->pLeaves[i];
-    pC->nLeaves = pC0->nLeaves;
-    // the case when one of the cuts is the largest
-    if ( pC0->nLeaves == nLimit )
-        return 1;
-    // add nodes of the second cut
-    k = 0;
-    for ( i = 0; i < pC1->nLeaves; i++ )
-    {
-        // find k-th node before which i-th node should be added
-        for ( ; k < pC->nLeaves; k++ )
-            if ( pC->pLeaves[k] >= pC1->pLeaves[i] )
-                break;
-        // check the case when this should be the last node
-        if ( k == pC->nLeaves )
-        {
-            pC->pLeaves[k++] = pC1->pLeaves[i];
-            pC->nLeaves++;
-            continue;
-        }
-        // check the case when equal node is found
-        if ( pC1->pLeaves[i] == pC->pLeaves[k] )
-            continue;
-        // add the node
-        for ( c = pC->nLeaves; c > k; c-- )
-            pC->pLeaves[c] = pC->pLeaves[c-1];
-        pC->pLeaves[k++] = pC1->pLeaves[i];
-        pC->nLeaves++;
-    }
-    assert( pC->nLeaves <= nLimit );
-    for ( i = 1; i < pC->nLeaves; i++ )
-        assert( pC->pLeaves[i-1] < pC->pLeaves[i] );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the object for FPGA mapping.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut, int nLimit )
-{ 
-    // merge the nodes
-    if ( pCut0->nLeaves < pCut1->nLeaves )
-    {
-        if ( !If_CutMergeOrdered( pCut1, pCut0, pCut, nLimit ) )
-            return 0;
-    }
-    else
-    {
-        if ( !If_CutMergeOrdered( pCut0, pCut1, pCut, nLimit ) )
-            return 0;
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the object for FPGA mapping.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int If_CutCompareDelay( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
-{
-    If_Cut_t * pC0 = *ppC0;
-    If_Cut_t * pC1 = *ppC1;
-    if ( pC0->Delay < pC1->Delay - 0.0001 )
-        return -1;
-    if ( pC0->Delay > pC1->Delay + 0.0001 )
-        return 1;
-    if ( pC0->nLeaves < pC1->nLeaves )
-        return -1;
-    if ( pC0->nLeaves > pC1->nLeaves )
-        return 1;
-    if ( pC0->Area < pC1->Area - 0.0001 )
-        return -1;
-    if ( pC0->Area > pC1->Area + 0.0001 )
-        return 1;
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the object for FPGA mapping.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int If_CutCompareDelayOld( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
-{
-    If_Cut_t * pC0 = *ppC0;
-    If_Cut_t * pC1 = *ppC1;
-    if ( pC0->Delay < pC1->Delay - 0.0001 )
-        return -1;
-    if ( pC0->Delay > pC1->Delay + 0.0001 )
-        return 1;
-    if ( pC0->Area < pC1->Area - 0.0001 )
-        return -1;
-    if ( pC0->Area > pC1->Area + 0.0001 )
-        return 1;
-    if ( pC0->nLeaves < pC1->nLeaves )
-        return -1;
-    if ( pC0->nLeaves > pC1->nLeaves )
-        return 1;
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the object for FPGA mapping.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int If_CutCompareArea( If_Cut_t ** ppC0, If_Cut_t ** ppC1 )
-{
-    If_Cut_t * pC0 = *ppC0;
-    If_Cut_t * pC1 = *ppC1;
-    if ( pC0->Area < pC1->Area - 0.0001 )
-        return -1;
-    if ( pC0->Area > pC1->Area + 0.0001 )
-        return 1;
-    if ( pC0->nLeaves < pC1->nLeaves )
-        return -1;
-    if ( pC0->nLeaves > pC1->nLeaves )
-        return 1;
-    if ( pC0->Delay < pC1->Delay - 0.0001 )
-        return -1;
-    if ( pC0->Delay > pC1->Delay + 0.0001 )
-        return 1;
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sorts the cuts.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void If_ManSortCuts( If_Man_t * p, int Mode )
-{
-    // sort the cuts
-    if ( Mode || p->pPars->fArea ) // area
-        qsort( p->ppCuts, p->nCuts, sizeof(If_Cut_t *), (int (*)(const void *, const void *))If_CutCompareArea );
-    else if ( p->pPars->fFancy )
-        qsort( p->ppCuts, p->nCuts, sizeof(If_Cut_t *), (int (*)(const void *, const void *))If_CutCompareDelayOld );
-    else
-        qsort( p->ppCuts, p->nCuts, sizeof(If_Cut_t *), (int (*)(const void *, const void *))If_CutCompareDelay );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes delay.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-float If_CutDelay( If_Man_t * p, If_Cut_t * pCut )
-{
-    If_Obj_t * pLeaf;
-    float Delay;
-    int i;
-    assert( pCut->nLeaves > 1 );
-    Delay = -IF_FLOAT_LARGE;
-    If_CutForEachLeaf( p, pCut, pLeaf, i )
-        Delay = IF_MAX( Delay, If_ObjCutBest(pLeaf)->Delay );
-    return Delay + If_CutLutDelay(p, pCut);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes area flow.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-float If_CutFlow( If_Man_t * p, If_Cut_t * pCut )
-{
-    If_Obj_t * pLeaf;
-    float Flow;
-    int i;
-    assert( pCut->nLeaves > 1 );
-    Flow = If_CutLutArea(p, pCut);
-    If_CutForEachLeaf( p, pCut, pLeaf, i )
-    {
-        if ( pLeaf->nRefs == 0 )
-            Flow += If_ObjCutBest(pLeaf)->Area;
-        else
-        {
-            assert( pLeaf->EstRefs > p->fEpsilon );
-            Flow += If_ObjCutBest(pLeaf)->Area / pLeaf->EstRefs;
-        }
-    }
-    return Flow;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes area of the first level.]
-
-  Description [The cut need to be derefed.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-float If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels )
-{
-    If_Obj_t * pLeaf;
-    float Area;
-    int i;
-    Area = If_CutLutArea(p, pCut);
-    If_CutForEachLeaf( p, pCut, pLeaf, i )
-    {
-        assert( pLeaf->nRefs > 0 );
-        if ( --pLeaf->nRefs > 0 || !If_ObjIsAnd(pLeaf) || nLevels == 1 )
-            continue;
-        Area += If_CutDeref( p, If_ObjCutBest(pLeaf), nLevels - 1 );
-    }
-    return Area;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes area of the first level.]
-
-  Description [The cut need to be derefed.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-float If_CutRef( If_Man_t * p, If_Cut_t * pCut, int nLevels )
-{
-    If_Obj_t * pLeaf;
-    float Area;
-    int i;
-    Area = If_CutLutArea(p, pCut);
-    If_CutForEachLeaf( p, pCut, pLeaf, i )
-    {
-        assert( pLeaf->nRefs >= 0 );
-        if ( pLeaf->nRefs++ > 0 || !If_ObjIsAnd(pLeaf) || nLevels == 1 )
-            continue;
-        Area += If_CutRef( p, If_ObjCutBest(pLeaf), nLevels - 1 );
-    }
-    return Area;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints one cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void If_CutPrint( If_Man_t * p, If_Cut_t * pCut )
-{
-    int i;
-    printf( "{" );
-    for ( i = 0; i < pCut->nLeaves; i++ )
-        printf( " %d", pCut->pLeaves[i] );
-    printf( " }\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes area of the first level.]
-
-  Description [The cut need to be derefed.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-float If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut, int nLevels )
-{
-    float aResult, aResult2;
-    assert( pCut->nLeaves > 1 );
-    aResult2 = If_CutRef( p, pCut, nLevels );
-    aResult  = If_CutDeref( p, pCut, nLevels );
-    assert( aResult == aResult2 );
-    return aResult;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes area of the first level.]
-
-  Description [The cut need to be derefed.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-float If_CutAreaRefed( If_Man_t * p, If_Cut_t * pCut, int nLevels )
-{
-    float aResult, aResult2;
-    assert( pCut->nLeaves > 1 );
-    aResult2 = If_CutDeref( p, pCut, nLevels );
-    aResult  = If_CutRef( p, pCut, nLevels );
-    assert( aResult == aResult2 );
-    return aResult;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes area of the first level.]
-
-  Description [The cut need to be derefed.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void If_CutCopy( If_Cut_t * pCutDest, If_Cut_t * pCutSrc )
-{
-    int * pArray;
-    pArray = pCutDest->pLeaves;
-    *pCutDest = *pCutSrc;
-    pCutDest->pLeaves = pArray;
-    memcpy( pCutDest->pLeaves, pCutSrc->pLeaves, sizeof(int) * pCutSrc->nLeaves );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Finds the best cut.]
 
   Description [Mapping modes: delay (0), area flow (1), area (2).]
@@ -632,7 +71,7 @@ void If_CutCopy( If_Cut_t * pCutDest, If_Cut_t * pCutSrc )
 void If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode )
 {
     If_Cut_t * pCut0, * pCut1, * pCut;
-    int i, k, iCut;
+    int i, k, iCut, Temp;
 
     // prepare
     if ( Mode == 0 )
@@ -670,29 +109,34 @@ void If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode )
         if ( Mode && (pCut0->Delay > pObj->Required + p->fEpsilon || pCut1->Delay > pObj->Required + p->fEpsilon) )
             continue;
         // merge the nodes
-        if ( !If_CutMerge( pCut0, pCut1, pCut, p->pPars->nLutSize ) )
+        if ( !If_CutMerge( pCut0, pCut1, pCut ) )
             continue;
         // check if this cut is contained in any of the available cuts
         pCut->uSign = pCut0->uSign | pCut1->uSign;
-        if ( If_CutFilter( p, pCut, Mode ) )
+        if ( If_CutFilter( p, pCut ) )
             continue;
         // check if the cut satisfies the required times
         pCut->Delay = If_CutDelay( p, pCut );
         if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon )
             continue;
         // the cuts have been successfully merged
-        pCut->pOne = pCut0; pCut->fCompl0 = pObj->fCompl0;
-        pCut->pTwo = pCut1; pCut->fCompl1 = pObj->fCompl1;
-//        pCut->Phase = ...
-//        pCut->Phase = (char)(int)If_CutAreaDerefed( p, pCut, 1 );
-        pCut->Area  = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut );
-        p->nCutsMerged++;
+        // compute the truth table
+        if ( p->pPars->fTruth )
+            If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
+        // compute the application-specific cost and depth
+        Temp = p->pPars->pFuncCost? p->pPars->pFuncCost(If_CutTruth(pCut), pCut->nLimit) : 0;
+        pCut->Cost = (Temp & 0xffff); pCut->Depth = (Temp >> 16);
+        // compute area of the cut (this area may depend on the application specific cost)
+        pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut );
         // make sure the cut is the last one (after filtering it may not be so)
         assert( pCut == p->ppCuts[iCut] );
         p->ppCuts[iCut] = p->ppCuts[p->nCuts];
         p->ppCuts[p->nCuts] = pCut;
+        // count the cut
+        p->nCuts++;
+        p->nCutsMerged++;
         // prepare room for the next cut
-        iCut = ++p->nCuts;
+        iCut = p->nCuts;
         pCut = p->ppCuts[iCut];
     } 
 //printf( "%d  ", p->nCuts );
diff --git a/src/map/if/ifSelect.c b/src/map/if/ifPrepro.c
index d54abb29..797e8727 100644
--- a/src/map/if/ifSelect.c
+++ b/src/map/if/ifPrepro.c
@@ -1,12 +1,12 @@
 /**CFile****************************************************************
 
-  FileName    [ifSelect.c]
+  FileName    [ifPrepro.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
   PackageName [FPGA mapping based on priority cuts.]
 
-  Synopsis    [Selects what mapping to use.]
+  Synopsis    [Selects the starting mapping.]
 
   Author      [Alan Mishchenko]
   
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - November 21, 2006.]
 
-  Revision    [$Id: ifSelect.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
+  Revision    [$Id: ifPrepro.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
diff --git a/src/map/if/ifReduce.c b/src/map/if/ifReduce.c
index 5c8da0d0..0b3cf9c2 100644
--- a/src/map/if/ifReduce.c
+++ b/src/map/if/ifReduce.c
@@ -522,11 +522,11 @@ void If_ManImproveNodeReduce( If_Man_t * p, If_Obj_t * pObj, int nLimit )
 
     // merge the cuts
     pCutR = p->ppCuts[0];
-    RetValue = If_CutMerge( pCut0, pCut1, pCutR, nLimit );
+    RetValue = If_CutMerge( pCut0, pCut1, pCutR );
     // try very simple cut
     if ( !RetValue )
     {
-        RetValue = If_CutMerge( If_ObjCutTriv(pFanin0), If_ObjCutTriv(pFanin1), pCutR, nLimit );
+        RetValue = If_CutMerge( If_ObjCutTriv(pFanin0), If_ObjCutTriv(pFanin1), pCutR );
         assert( RetValue == 1 );
     }
     if ( RetValue )
diff --git a/src/map/if/ifSeq.c b/src/map/if/ifSeq.c
index ce353f49..bc4ab806 100644
--- a/src/map/if/ifSeq.c
+++ b/src/map/if/ifSeq.c
@@ -95,7 +95,7 @@ int If_ManPerformMappingSeq( If_Man_t * p )
 ***********************************************************************/
 void If_CutLift( If_Cut_t * pCut )
 {
-    int i;
+    unsigned i;
     for ( i = 0; i < pCut->nLeaves; i++ )
         pCut->pLeaves[i] = ((pCut->pLeaves[i] >> 8) << 8) | ((pCut->pLeaves[i] & 255) + 1);
 }
diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c
new file mode 100644
index 00000000..68affc4a
--- /dev/null
+++ b/src/map/if/ifTruth.c
@@ -0,0 +1,95 @@
+/**CFile****************************************************************
+
+  FileName    [ifTruth.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [FPGA mapping based on priority cuts.]
+
+  Synopsis    [Computation of truth tables of the cuts.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 21, 2006.]
+
+  Revision    [$Id: ifTruth.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "if.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the stretching phase of the cut w.r.t. the merged cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Cut_TruthPhase( If_Cut_t * pCut, If_Cut_t * pCut1 )
+{
+    unsigned uPhase = 0;
+    int i, k;
+    for ( i = k = 0; i < (int)pCut->nLeaves; i++ )
+    {
+        if ( k == (int)pCut1->nLeaves )
+            break;
+        if ( pCut->pLeaves[i] < pCut1->pLeaves[k] )
+            continue;
+        assert( pCut->pLeaves[i] == pCut1->pLeaves[k] );
+        uPhase |= (1 << i);
+        k++;
+    }
+    return uPhase;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs truth table computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 )
+{
+    // permute the first table
+    if ( fCompl0 ) 
+        Extra_TruthNot( p->puTemp[0], If_CutTruth(pCut0), pCut->nLimit );
+    else
+        Extra_TruthCopy( p->puTemp[0], If_CutTruth(pCut0), pCut->nLimit );
+    Extra_TruthStretch( p->puTemp[2], p->puTemp[0], pCut0->nLeaves, pCut->nLimit, Cut_TruthPhase(pCut, pCut0) );
+    // permute the second table
+    if ( fCompl1 ) 
+        Extra_TruthNot( p->puTemp[1], If_CutTruth(pCut1), pCut->nLimit );
+    else
+        Extra_TruthCopy( p->puTemp[1], If_CutTruth(pCut1), pCut->nLimit );
+    Extra_TruthStretch( p->puTemp[3], p->puTemp[1], pCut1->nLeaves, pCut->nLimit, Cut_TruthPhase(pCut, pCut1) );
+    // produce the resulting table
+    if ( pCut->fCompl )
+        Extra_TruthNand( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit );
+    else
+        Extra_TruthAnd( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/if/module.make b/src/map/if/module.make
index 362318da..b7d3185f 100644
--- a/src/map/if/module.make
+++ b/src/map/if/module.make
@@ -2,7 +2,8 @@ SRC +=  src/map/if/ifCore.c \
     src/map/if/ifCut.c \
     src/map/if/ifMan.c \
     src/map/if/ifMap.c \
+    src/map/if/ifPrepro.c \
     src/map/if/ifReduce.c \
-    src/map/if/ifSelect.c \
     src/map/if/ifSeq.c \
+    src/map/if/ifTruth.c \
     src/map/if/ifUtil.c