Version abc61206

5 files changed, 0 insertions, 1491 deletions

diff --git a/src/aig/ivy/ivy.h b/src/aig/ivy/ivy.h
index 91d4d767..f48466ef 100644
--- a/src/aig/ivy/ivy.h
+++ b/src/aig/ivy/ivy.h
@@ -466,8 +466,6 @@ extern void            Ivy_ManHaigPostprocess( Ivy_Man_t * p, int fVerbose );
 extern void            Ivy_ManHaigCreateObj( Ivy_Man_t * p, Ivy_Obj_t * pObj );
 extern void            Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew );
 extern void            Ivy_ManHaigSimulate( Ivy_Man_t * p );
-/*=== ivyIsop.c ==========================================================*/
-extern int             Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth );
 /*=== ivyMan.c ==========================================================*/
 extern Ivy_Man_t *     Ivy_ManStart();
 extern Ivy_Man_t *     Ivy_ManStartFrom( Ivy_Man_t * p );
diff --git a/src/aig/ivy/ivyFactor.c b/src/aig/ivy/ivyFactor.c
deleted file mode 100644
index 19a40b3f..00000000
--- a/src/aig/ivy/ivyFactor.c
+++ /dev/null
@@ -1,783 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [ivyFactor.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [And-Inverter Graph package.]
-
-  Synopsis    [Factoring the cover up to 16 inputs.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - May 11, 2006.]
-
-  Revision    [$Id: ivyFactor.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "ivy.h"
-#include "dec.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-// 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 []
-
-  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 )
-
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Factors the cover.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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(cSop) == 0 )
-        return Dec_GraphCreateConst0();
-    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
-    Ivy_SopCreateInverse( cSop, pcSop, nVars, vStore ); // CST
-
-    // start the factored form
-    pFForm = Dec_GraphCreate( nVars );
-    // factor the cover
-    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, nVars ) )
-        printf( "Verification has failed.\n" );
-    return pFForm;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Internal recursive factoring procedure.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Edge_t Dec_Factor32_rec( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nLits )
-{
-    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(cSop) );
-
-    // get the divisor
-    cDiv = Ivy_SopDivisor( cSop, nLits );
-    if ( cDiv == NULL )
-        return Dec_Factor32Trivial( pFForm, cSop, nLits );
-
-    // divide the cover by the divisor
-    Ivy_SopDivideInternal( cSop, nLits, cDiv, &vQuo, &vRem );
-    assert( Vec_IntSize(vQuo) );
-
-    Vec_IntFree( cDiv );
-    Vec_IntFree( vRem );
-
-    // check the trivial case
-    if ( Vec_IntSize(vQuo) == 1 )
-    {
-        eNode = Dec_Factor32LF_rec( pFForm, cSop, nLits, vQuo );
-        Vec_IntFree( vQuo );
-        return eNode;
-    }
-
-    // make the quotient cube free
-    Ivy_SopMakeCubeFree( vQuo );
-
-    // divide the cover by the quotient
-    Ivy_SopDivideInternal( cSop, nLits, vQuo, &cDiv, &vRem );
-
-    // check the trivial case
-    if ( Ivy_SopIsCubeFree( cDiv ) )
-    {
-        eNodeDiv = Dec_Factor32_rec( pFForm, cDiv );
-        eNodeQuo = Dec_Factor32_rec( pFForm, vQuo );
-        Vec_IntFree( cDiv );
-        Vec_IntFree( vQuo );
-        eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
-        if ( Vec_IntSize(vRem) == 0 )
-        {
-            Vec_IntFree( vRem );
-            return eNodeAnd;
-        }
-        else
-        {
-            eNodeRem = Dec_Factor32_rec( pFForm, vRem );
-            Vec_IntFree( vRem );
-            return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
-        }
-    }
-
-    // get the common cube
-    vCom = Ivy_SopCommonCubeCover( cDiv );
-    Vec_IntFree( cDiv );
-    Vec_IntFree( vQuo );
-    Vec_IntFree( vRem );
-
-    // solve the simple problem
-    eNode = Dec_Factor32LF_rec( pFForm, cSop, nLits, vCom );
-    Vec_IntFree( vCom );
-    return eNode;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Internal recursive factoring procedure for the leaf case.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Edge_t Dec_Factor32LF_rec( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nLits, Vec_Int_t * vSimple )
-{
-    Dec_Man_t * pManDec = Abc_FrameReadManDec();
-    Vec_Int_t * vEdgeLits  = pManDec->vLits;
-    Vec_Int_t * cDiv, * vQuo, * vRem;
-    Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem;
-    Dec_Edge_t eNodeAnd;
-
-    // get the most often occurring literal
-    cDiv = Ivy_SopBestLiteralCover( cSop, nLits, vSimple );
-    // divide the cover by the literal
-    Ivy_SopDivideByLiteral( cSop, nLits, cDiv, &vQuo, &vRem );
-    // get the node pointer for the literal
-    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 );
-    eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
-    if ( Vec_IntSize(vRem) == 0 )
-    {
-        Vec_IntFree( vRem );
-        return eNodeAnd;
-    }
-    else
-    {
-        eNodeRem = Dec_Factor32_rec( pFForm, vRem );
-        Vec_IntFree( vRem );
-        return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
-    }
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Factoring the cover, which has no algebraic divisors.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Edge_t Dec_Factor32Trivial( Dec_Graph_t * pFForm, Vec_Int_t * 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;
-    unsigned uCube;
-    int i;
-    // create the factored form for each cube
-    Vec_IntClear( vEdgeCubes );
-    Ivy_SopForEachCube( cSop, uCube )
-    {
-        eNode = Dec_Factor32TrivialCube( pFForm, cSop, nLits, uCube, vEdgeLits );
-        Vec_IntPush( vEdgeCubes, Dec_EdgeToInt_(eNode) );
-    }
-    // balance the factored forms
-    return Dec_Factor32TrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeCubes->pArray, vEdgeCubes->nSize, 1 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Factoring the cube.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Edge_t Dec_Factor32TrivialCube( Dec_Graph_t * pFForm, Vec_Int_t * 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_CubeForEachLit( cSop, uCube, iBit, Value )
-        if ( Value )
-        {
-            eNode = Dec_EdgeCreate( iBit/2, iBit%2 ); // CST
-            Vec_IntPush( vEdgeLits, Dec_EdgeToInt_(eNode) );
-        }
-    // balance the factored forms
-    return Dec_Factor32TrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeLits->pArray, vEdgeLits->nSize, 0 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Create the well-balanced tree of nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Edge_t Dec_Factor32TrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr )
-{
-    Dec_Edge_t eNode1, eNode2;
-    int nNodes1, nNodes2;
-
-    if ( nNodes == 1 )
-        return peNodes[0];
-
-    // split the nodes into two parts
-    nNodes1 = nNodes/2;
-    nNodes2 = nNodes - nNodes1;
-//    nNodes2 = nNodes/2;
-//    nNodes1 = nNodes - nNodes2;
-
-    // recursively construct the tree for the parts
-    eNode1 = Dec_Factor32TrivialTree_rec( pFForm, peNodes,           nNodes1, fNodeOr );
-    eNode2 = Dec_Factor32TrivialTree_rec( pFForm, peNodes + nNodes1, nNodes2, fNodeOr );
-
-    if ( fNodeOr )
-        return Dec_GraphAddNodeOr( pFForm, eNode1, eNode2 );
-    else
-        return Dec_GraphAddNodeAnd( pFForm, eNode1, eNode2 );
-}
-
-
-
-
-// verification using temporary BDD package
-#include "cuddInt.h"
-
-/**Function*************************************************************
-
-  Synopsis    [Verifies that the factoring is correct.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Ivy_SopCoverToBdd( DdManager * dd, Vec_Int_t * cSop, int nVars )
-{
-    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 )
-    {
-        bCube = Cudd_ReadOne(dd);   Cudd_Ref( bCube );
-        for ( v = 0; v < nVars; v++ )
-        {
-            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;
-            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 );
-    }
-    // complement the result if necessary
-    Cudd_Deref( bSum );
-    return bSum;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Verifies that the factoring is correct.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Dec_Factor32Verify( Vec_Int_t * cSop, Dec_Graph_t * pFForm, int nVars )
-{
-    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 )
-    {
-        int s;
-        Extra_bddPrint( dd, bFunc1 ); printf("\n");
-        Extra_bddPrint( dd, bFunc2 ); printf("\n");
-        s  = 0;
-    }
-    Cudd_RecursiveDeref( dd, bFunc1 );
-    Cudd_RecursiveDeref( dd, bFunc2 );
-    return RetValue;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/ivy/ivyFpga.c b/src/aig/ivy/ivyFpga.c
deleted file mode 100644
index 122cc0e2..00000000
--- a/src/aig/ivy/ivyFpga.c
+++ /dev/null
@@ -1,378 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [ivyFpga.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [And-Inverter Graph package.]
-
-  Synopsis    [Prepares the AIG package to work as an FPGA mapper.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - May 11, 2006.]
-
-  Revision    [$Id: ivyFpga.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "ivy.h"
-#include "attr.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Ivy_FpgaMan_t_     Ivy_FpgaMan_t;
-typedef struct Ivy_FpgaObj_t_     Ivy_FpgaObj_t;
-typedef struct Ivy_FpgaCut_t_     Ivy_FpgaCut_t;
-
-// manager
-struct Ivy_FpgaMan_t_
-{
-    Ivy_Man_t *        pManIvy;       // the AIG manager
-    Attr_Man_t *       pManAttr;      // the attribute manager
-    int                nLutSize;      // the LUT size
-    int                nCutsMax;      // the max number of cuts
-    int                nEntrySize;    // the size of the entry
-    int                nEntryBase;    // the size of the entry minus cut leaf arrays
-    int                fVerbose;      // the verbosity flag
-    // temporary cut storage
-    Ivy_FpgaCut_t *    pCutStore;     // the temporary cuts
-};
-
-// priority cut
-struct Ivy_FpgaCut_t_
-{
-    float              Delay;         // the delay of the cut
-    float              AreaFlow;      // the area flow of the cut
-    float              Area;          // the area of the cut
-    int                nLeaves;       // the number of leaves
-    int *              pLeaves;       // the array of fanins
-};
-
-// node extension
-struct Ivy_FpgaObj_t_
-{
-    unsigned           Type   :  4;   // type
-    unsigned           nCuts  : 28;   // the number of cuts
-    int                Id;            // integer ID
-    int                nRefs;         // the number of references
-    Ivy_FpgaObj_t *    pFanin0;       // the first fanin 
-    Ivy_FpgaObj_t *    pFanin1;       // the second fanin
-    float              Required;      // required time of the onde
-    Ivy_FpgaCut_t *    pCut;          // the best cut
-    Ivy_FpgaCut_t      Cuts[0];       // the cuts of the node
-};
-
-
-static Ivy_FpgaMan_t * Ivy_ManFpgaPrepare( Ivy_Man_t * p, int nLutSize, int nCutsMax, int fVerbose );
-static void Ivy_ManFpgaUndo( Ivy_FpgaMan_t * pFpga );
-static void Ivy_ObjFpgaCreate( Ivy_FpgaMan_t * pFpga, int ObjId );
-static void Ivy_ManFpgaDelay( Ivy_FpgaMan_t * pFpga );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Performs FPGA mapping.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_ManFpga( Ivy_Man_t * p, int nLutSize, int nCutsMax, int fVerbose )
-{
-    Ivy_FpgaMan_t * pFpga;
-    pFpga = Ivy_ManFpgaPrepare( p, nLutSize, nCutsMax, fVerbose );
-    Ivy_ManFpgaDelay( pFpga );
-    Ivy_ManFpgaUndo( pFpga );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares manager for FPGA mapping.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ivy_FpgaMan_t * Ivy_ManFpgaPrepare( Ivy_Man_t * p, int nLutSize, int nCutsMax, int fVerbose )
-{
-    Ivy_FpgaMan_t * pFpga;
-    Ivy_Obj_t * pObj;
-    int i;
-    pFpga = ALLOC( Ivy_FpgaMan_t, 1 );
-    memset( pFpga, 0, sizeof(Ivy_FpgaMan_t) );
-    // compute the size of the node
-    pFpga->pManIvy    = p;
-    pFpga->nLutSize   = nLutSize; 
-    pFpga->nCutsMax   = nCutsMax; 
-    pFpga->fVerbose   = fVerbose;
-    pFpga->nEntrySize = sizeof(Ivy_FpgaObj_t) + (nCutsMax + 1) * (sizeof(Ivy_FpgaCut_t) + sizeof(int) * nLutSize);
-    pFpga->nEntryBase = sizeof(Ivy_FpgaObj_t) + (nCutsMax + 1) * (sizeof(Ivy_FpgaCut_t));
-    pFpga->pManAttr   = Attr_ManStartPtrMem( Ivy_ManObjIdMax(p) + 1, pFpga->nEntrySize );
-    if ( fVerbose )
-        printf( "Entry size = %d. Total memory = %5.2f Mb.\n", pFpga->nEntrySize, 
-            1.0 * pFpga->nEntrySize * (Ivy_ManObjIdMax(p) + 1) / (1<<20) );
-    // connect memory for cuts
-    Ivy_ManForEachObj( p, pObj, i )
-        Ivy_ObjFpgaCreate( pFpga, pObj->Id );
-    // create temporary cuts
-    pFpga->pCutStore  = (Ivy_FpgaCut_t *)ALLOC( char, pFpga->nEntrySize * (nCutsMax + 1) * (nCutsMax + 1) );
-    memset( pFpga->pCutStore, 0, pFpga->nEntrySize * (nCutsMax + 1) * (nCutsMax + 1) );
-    {
-        int i, * pArrays;
-        pArrays = (int *)((char *)pFpga->pCutStore + sizeof(Ivy_FpgaCut_t) * (nCutsMax + 1) * (nCutsMax + 1));
-        for ( i = 0; i < (nCutsMax + 1) * (nCutsMax + 1); i++ )
-            pFpga->pCutStore[i].pLeaves = pArrays + i * pFpga->nLutSize;
-    }
-    return pFpga;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Quits the manager for FPGA mapping.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_ManFpgaUndo( Ivy_FpgaMan_t * pFpga )
-{
-    Attr_ManStop( pFpga->pManAttr );
-    free( pFpga );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the object for FPGA mapping.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_ObjFpgaCreate( Ivy_FpgaMan_t * pFpga, int ObjId )
-{
-    Ivy_FpgaObj_t * pObjFpga;
-    int i, * pArrays;
-    pObjFpga = Attr_ManReadAttrPtr( pFpga->pManAttr, ObjId );
-    pArrays = (int *)((char *)pObjFpga + pFpga->nEntryBase);
-    for ( i = 0; i <= pFpga->nCutsMax; i++ )
-        pObjFpga->Cuts[i].pLeaves = pArrays + i * pFpga->nLutSize;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the object for FPGA mapping.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ivy_ObjFpgaMerge( Ivy_FpgaCut_t * pC0, Ivy_FpgaCut_t * pC1, Ivy_FpgaCut_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;
-        pC->Delay = 1 + IVY_MAX( pC0->Delay, pC1->Delay );
-        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;
-        pC->Delay = 1 + IVY_MAX( pC0->Delay, pC1->Delay );
-        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;
-                pC->Delay = 1 + IVY_MAX( pC0->Delay, pC1->Delay );
-                return 1;
-            }
-            pC->pLeaves[c] = pC0->pLeaves[i++];
-            continue;
-        }
-        if ( i == pC0->nLeaves )
-        {
-            if ( k == pC1->nLeaves )
-            {
-                pC->nLeaves = c;
-                pC->Delay = 1 + IVY_MAX( pC0->Delay, pC1->Delay );
-                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;
-    pC->Delay = 1 + IVY_MAX( pC0->Delay, pC1->Delay );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the object for FPGA mapping.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ivy_FpgaCutCompare( Ivy_FpgaCut_t * pC0, Ivy_FpgaCut_t * pC1 )
-{
-    if ( pC0->Delay < pC1->Delay )
-        return -1;
-    if ( pC0->Delay > pC1->Delay )
-        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     []
-
-***********************************************************************/
-void Ivy_ObjFpgaDelay( Ivy_FpgaMan_t * pFpga, int ObjId, int Fan0Id, int Fan1Id )
-{
-    Ivy_FpgaObj_t * pObjFpga, * pObjFpga0, * pObjFpga1;
-    int nCuts, i, k;
-    pObjFpga  = Attr_ManReadAttrPtr( pFpga->pManAttr, ObjId );
-    pObjFpga0 = Attr_ManReadAttrPtr( pFpga->pManAttr, Fan0Id );
-    pObjFpga1 = Attr_ManReadAttrPtr( pFpga->pManAttr, Fan1Id );
-    // create cross-product of the cuts
-    nCuts = 0;
-    for ( i = 0; pObjFpga0->Cuts[i].nLeaves > 0 && i < pFpga->nCutsMax; i++ )
-    for ( k = 0; pObjFpga1->Cuts[k].nLeaves > 0 && k < pFpga->nCutsMax; k++ )
-        if ( Ivy_ObjFpgaMerge( pObjFpga0->Cuts + i, pObjFpga1->Cuts + k, pFpga->pCutStore + nCuts, pFpga->nLutSize ) )
-            nCuts++;
-    // sort the cuts
-    qsort( pFpga->pCutStore, nCuts, sizeof(Ivy_FpgaCut_t), (int (*)(const void *, const void *))Ivy_FpgaCutCompare );
-    // take the first
-    pObjFpga->Cuts[0].nLeaves    = 1;
-    pObjFpga->Cuts[0].pLeaves[0] = ObjId;
-    pObjFpga->Cuts[0].Delay      = pFpga->pCutStore[0].Delay;
-    pObjFpga->Cuts[1] = pFpga->pCutStore[0];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Maps the nodes for delay.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_ManFpgaDelay( Ivy_FpgaMan_t * pFpga )
-{
-    Ivy_FpgaObj_t * pObjFpga;
-    Ivy_Obj_t * pObj;
-    int i, DelayBest;
-    int clk = clock();
-    // set arrival times and trivial cuts at const 1 and PIs
-    pObjFpga = Attr_ManReadAttrPtr( pFpga->pManAttr, 0 );
-    pObjFpga->Cuts[0].nLeaves = 1;
-    Ivy_ManForEachPi( pFpga->pManIvy, pObj, i )
-    {
-        pObjFpga = Attr_ManReadAttrPtr( pFpga->pManAttr, pObj->Id );
-        pObjFpga->Cuts[0].nLeaves    = 1;
-        pObjFpga->Cuts[0].pLeaves[0] = pObj->Id;
-    }
-    // map the internal nodes
-    Ivy_ManForEachNode( pFpga->pManIvy, pObj, i )
-    {
-        Ivy_ObjFpgaDelay( pFpga, pObj->Id, Ivy_ObjFaninId0(pObj), Ivy_ObjFaninId1(pObj) );
-    }
-    // get the best arrival time of the POs
-    DelayBest = 0;
-    Ivy_ManForEachPo( pFpga->pManIvy, pObj, i )
-    {
-        pObjFpga = Attr_ManReadAttrPtr( pFpga->pManAttr, Ivy_ObjFanin0(pObj)->Id );
-        if ( DelayBest < (int)pObjFpga->Cuts[1].Delay )
-            DelayBest = (int)pObjFpga->Cuts[1].Delay;
-    }
-    printf( "Best delay = %d. ", DelayBest );
-    PRT( "Time", clock() - clk );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/ivy/ivyIsop.c b/src/aig/ivy/ivyIsop.c
deleted file mode 100644
index ae48ca34..00000000
--- a/src/aig/ivy/ivyIsop.c
+++ /dev/null
@@ -1,327 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [ivyIsop.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [And-Inverter Graph package.]
-
-  Synopsis    [Computing irredundant SOP using truth table.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - May 11, 2006.]
-
-  Revision    [$Id: ivyIsop.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "ivy.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-// ISOP computation fails if intermediate memory usage exceed this limit
-#define IVY_ISOP_MEM_LIMIT  16*4096
-
-// intermediate ISOP representation
-typedef struct Ivy_Sop_t_ Ivy_Sop_t;
-struct Ivy_Sop_t_
-{
-    unsigned * pCubes;
-    int        nCubes;
-};
-
-// static procedures to compute ISOP
-static unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore );
-static unsigned   Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Computes ISOP from TT.]
-
-  Description [Returns the cover in vCover. Uses the rest of array in vCover
-  as an intermediate memory storage. Returns the cover with -1 cubes, if the
-  the computation exceeded the memory limit (IVY_ISOP_MEM_LIMIT words of
-  intermediate data).]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth )
-{
-    Ivy_Sop_t cRes, * pcRes = &cRes;
-    Ivy_Sop_t cRes2, * pcRes2 = &cRes2;
-    unsigned * pResult;
-    int RetValue = 0;
-    assert( nVars >= 0 && nVars < 16 );
-    // if nVars < 5, make sure it does not depend on those vars
-//    for ( i = nVars; i < 5; i++ )
-//        assert( !Extra_TruthVarInSupport(puTruth, 5, i) );
-    // prepare memory manager
-    Vec_IntClear( vCover );
-    Vec_IntGrow( vCover, IVY_ISOP_MEM_LIMIT );
-    // compute ISOP for the direct polarity
-    pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes, vCover );
-    if ( pcRes->nCubes == -1 )
-    {
-        vCover->nSize = -1;
-        return 0;
-    }
-    assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
-    if ( fTryBoth )
-    {
-        // compute ISOP for the complemented polarity
-        Extra_TruthNot( puTruth, puTruth, nVars );
-        pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes2, vCover );
-        if ( pcRes2->nCubes >= 0 )
-        {
-            assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
-            if ( pcRes->nCubes > pcRes2->nCubes )
-            {
-                RetValue = 1;
-                pcRes = pcRes2;
-            }
-        }
-        Extra_TruthNot( puTruth, puTruth, nVars );
-    }
-//    printf( "%d ", vCover->nSize );
-    // move the cover representation to the beginning of the memory buffer
-    memmove( vCover->pArray, pcRes->pCubes, pcRes->nCubes * sizeof(unsigned) );
-    Vec_IntShrink( vCover, pcRes->nCubes );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes ISOP 6 variables or more.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore )
-{
-    Ivy_Sop_t cRes0, cRes1, cRes2;
-    Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
-    unsigned * puRes0, * puRes1, * puRes2;
-    unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp, * pTemp0, * pTemp1;
-    int i, k, Var, nWords, nWordsAll;
-//    assert( Extra_TruthIsImply( puOn, puOnDc, nVars ) );
-    // allocate room for the resulting truth table
-    nWordsAll = Extra_TruthWordNum( nVars );
-    pTemp = Vec_IntFetch( vStore, nWordsAll );
-    if ( pTemp == NULL )
-    {
-        pcRes->nCubes = -1;
-        return NULL;
-    }
-    // check for constants
-    if ( Extra_TruthIsConst0( puOn, nVars ) )
-    {
-        pcRes->nCubes = 0;
-        pcRes->pCubes = NULL;
-        Extra_TruthClear( pTemp, nVars );
-        return pTemp;
-    }
-    if ( Extra_TruthIsConst1( puOnDc, nVars ) )
-    {
-        pcRes->nCubes = 1;
-        pcRes->pCubes = Vec_IntFetch( vStore, 1 );
-        if ( pcRes->pCubes == NULL )
-        {
-            pcRes->nCubes = -1;
-            return NULL;
-        }
-        pcRes->pCubes[0] = 0;
-        Extra_TruthFill( pTemp, nVars );
-        return pTemp;
-    }
-    assert( nVars > 0 );
-    // find the topmost var
-    for ( Var = nVars-1; Var >= 0; Var-- )
-        if ( Extra_TruthVarInSupport( puOn, nVars, Var ) || 
-             Extra_TruthVarInSupport( puOnDc, nVars, Var ) )
-             break;
-    assert( Var >= 0 );
-    // consider a simple case when one-word computation can be used
-    if ( Var < 5 )
-    {
-        unsigned uRes = Ivy_TruthIsop5_rec( puOn[0], puOnDc[0], Var+1, pcRes, vStore );
-        for ( i = 0; i < nWordsAll; i++ )
-            pTemp[i] = uRes;
-        return pTemp;
-    }
-    assert( Var >= 5 );
-    nWords = Extra_TruthWordNum( Var );
-    // cofactor
-    puOn0   = puOn;    puOn1   = puOn + nWords;
-    puOnDc0 = puOnDc;  puOnDc1 = puOnDc + nWords;
-    pTemp0  = pTemp;   pTemp1  = pTemp + nWords;
-    // solve for cofactors
-    Extra_TruthSharp( pTemp0, puOn0, puOnDc1, Var );
-    puRes0 = Ivy_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0, vStore );
-    if ( pcRes0->nCubes == -1 )
-    {
-        pcRes->nCubes = -1;
-        return NULL;
-    }
-    Extra_TruthSharp( pTemp1, puOn1, puOnDc0, Var );
-    puRes1 = Ivy_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1, vStore );
-    if ( pcRes1->nCubes == -1 )
-    {
-        pcRes->nCubes = -1;
-        return NULL;
-    }
-    Extra_TruthSharp( pTemp0, puOn0, puRes0, Var );
-    Extra_TruthSharp( pTemp1, puOn1, puRes1, Var );
-    Extra_TruthOr( pTemp0, pTemp0, pTemp1, Var );
-    Extra_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var );
-    puRes2 = Ivy_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2, vStore );
-    if ( pcRes2->nCubes == -1 )
-    {
-        pcRes->nCubes = -1;
-        return NULL;
-    }
-    // create the resulting cover
-    pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
-    pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes );
-    if ( pcRes->pCubes == NULL )
-    {
-        pcRes->nCubes = -1;
-        return NULL;
-    }
-    k = 0;
-    for ( i = 0; i < pcRes0->nCubes; i++ )
-        pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1));
-    for ( i = 0; i < pcRes1->nCubes; i++ )
-        pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+0));
-    for ( i = 0; i < pcRes2->nCubes; i++ )
-        pcRes->pCubes[k++] = pcRes2->pCubes[i];
-    assert( k == pcRes->nCubes );
-    // create the resulting truth table
-    Extra_TruthOr( pTemp0, puRes0, puRes2, Var );
-    Extra_TruthOr( pTemp1, puRes1, puRes2, Var );
-    // copy the table if needed
-    nWords <<= 1;
-    for ( i = 1; i < nWordsAll/nWords; i++ )
-        for ( k = 0; k < nWords; k++ )
-            pTemp[i*nWords + k] = pTemp[k];
-    // verify in the end
-//    assert( Extra_TruthIsImply( puOn, pTemp, nVars ) );
-//    assert( Extra_TruthIsImply( pTemp, puOnDc, nVars ) );
-    return pTemp;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes ISOP for 5 variables or less.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore )
-{
-    unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
-    Ivy_Sop_t cRes0, cRes1, cRes2;
-    Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
-    unsigned uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
-    int i, k, Var;
-    assert( nVars <= 5 );
-    assert( (uOn & ~uOnDc) == 0 );
-    if ( uOn == 0 )
-    {
-        pcRes->nCubes = 0;
-        pcRes->pCubes = NULL;
-        return 0;
-    }
-    if ( uOnDc == 0xFFFFFFFF )
-    {
-        pcRes->nCubes = 1;
-        pcRes->pCubes = Vec_IntFetch( vStore, 1 );
-        if ( pcRes->pCubes == NULL )
-        {
-            pcRes->nCubes = -1;
-            return 0;
-        }
-        pcRes->pCubes[0] = 0;
-        return 0xFFFFFFFF;
-    }
-    assert( nVars > 0 );
-    // find the topmost var
-    for ( Var = nVars-1; Var >= 0; Var-- )
-        if ( Extra_TruthVarInSupport( &uOn, 5, Var ) || 
-             Extra_TruthVarInSupport( &uOnDc, 5, Var ) )
-             break;
-    assert( Var >= 0 );
-    // cofactor
-    uOn0   = uOn1   = uOn;
-    uOnDc0 = uOnDc1 = uOnDc;
-    Extra_TruthCofactor0( &uOn0, Var + 1, Var );
-    Extra_TruthCofactor1( &uOn1, Var + 1, Var );
-    Extra_TruthCofactor0( &uOnDc0, Var + 1, Var );
-    Extra_TruthCofactor1( &uOnDc1, Var + 1, Var );
-    // solve for cofactors
-    uRes0 = Ivy_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0, vStore );
-    if ( pcRes0->nCubes == -1 )
-    {
-        pcRes->nCubes = -1;
-        return 0;
-    }
-    uRes1 = Ivy_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var, pcRes1, vStore );
-    if ( pcRes1->nCubes == -1 )
-    {
-        pcRes->nCubes = -1;
-        return 0;
-    }
-    uRes2 = Ivy_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pcRes2, vStore );
-    if ( pcRes2->nCubes == -1 )
-    {
-        pcRes->nCubes = -1;
-        return 0;
-    }
-    // create the resulting cover
-    pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
-    pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes );
-    if ( pcRes->pCubes == NULL )
-    {
-        pcRes->nCubes = -1;
-        return 0;
-    }
-    k = 0;
-    for ( i = 0; i < pcRes0->nCubes; i++ )
-        pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1));
-    for ( i = 0; i < pcRes1->nCubes; i++ )
-        pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+0));
-    for ( i = 0; i < pcRes2->nCubes; i++ )
-        pcRes->pCubes[k++] = pcRes2->pCubes[i];
-    assert( k == pcRes->nCubes );
-    // derive the final truth table
-    uRes2 |= (uRes0 & ~uMasks[Var]) | (uRes1 & uMasks[Var]);
-//    assert( (uOn & ~uRes2) == 0 );
-//    assert( (uRes2 & ~uOnDc) == 0 );
-    return uRes2;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/ivy/module.make b/src/aig/ivy/module.make
index c1f7d1b8..daef43df 100644
--- a/src/aig/ivy/module.make
+++ b/src/aig/ivy/module.make
@@ -9,7 +9,6 @@ SRC +=    src/aig/ivy/ivyBalance.c \
     src/aig/ivy/ivyFastMap.c \
     src/aig/ivy/ivyFraig.c \
     src/aig/ivy/ivyHaig.c \
-    src/aig/ivy/ivyIsop.c \
     src/aig/ivy/ivyMan.c \
     src/aig/ivy/ivyMem.c \
     src/aig/ivy/ivyMulti.c \