Version abc61205

2 files changed, 489 insertions, 540 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                              ///