Version abc70930

15 files changed, 0 insertions, 5761 deletions

diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c
deleted file mode 100644
index d11fd793..00000000
--- a/src/opt/fxu/fxu.c
+++ /dev/null
@@ -1,254 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fxu.c]
-
-  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
-
-  Synopsis    [The entrance into the fast extract module.]
-
-  Author      [MVSIS Group]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - February 1, 2003.]
-
-  Revision    [$Id: fxu.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fxuInt.h" 
-#include "fxu.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-/*===== fxuCreate.c ====================================================*/
-extern Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData );
-extern void         Fxu_CreateCovers( Fxu_Matrix * p, Fxu_Data_t * pData );
-
-static int s_MemoryTotal;
-static int s_MemoryPeak;
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Performs fast_extract on a set of covers.]
-
-  Description [All the covers are given in the array p->vSops. 
-  The resulting covers are returned in the array p->vSopsNew.
-  The entries in these arrays correspond to objects in the network.
-  The entries corresponding to the PI and objects with trivial covers are NULL.
-  The number of extracted covers (not exceeding p->nNodesExt) is returned. 
-  Two other things are important for the correct operation of this procedure:
-  (1) The input covers do not have duplicated fanins and are SCC-free. 
-  (2) The fanins array contains the numbers of the fanin objects.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fxu_FastExtract( Fxu_Data_t * pData )
-{
-    Fxu_Matrix * p;
-    Fxu_Single * pSingle;
-    Fxu_Double * pDouble;
-    int Weight1, Weight2, Weight3;
-    int Counter = 0;
-
-    s_MemoryTotal = 0;
-    s_MemoryPeak  = 0;
-
-    // create the matrix
-    p = Fxu_CreateMatrix( pData );
-    if ( p == NULL )
-        return -1;
-//    if ( pData->fVerbose )
-//        printf( "Memory usage after construction: Total = %d. Peak = %d.\n", s_MemoryTotal, s_MemoryPeak );
-//Fxu_MatrixPrint( NULL, p );
-
-    if ( pData->fOnlyS )
-    {
-        pData->nNodesNew = 0;
-        do
-        {
-            Weight1 = Fxu_HeapSingleReadMaxWeight( p->pHeapSingle );
-            if ( pData->fVerbose )
-                printf( "Div %5d : Best single = %5d.\r", Counter++, Weight1 );
-            if ( Weight1 > 0 || Weight1 == 0 && pData->fUse0 )
-                Fxu_UpdateSingle( p );
-            else
-                break;
-        }
-        while ( ++pData->nNodesNew < pData->nNodesExt );
-    }
-    else if ( pData->fOnlyD )
-    {
-        pData->nNodesNew = 0;
-        do
-        {
-            Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
-            if ( pData->fVerbose )
-                printf( "Div %5d : Best double = %5d.\r", Counter++, Weight2 );
-            if ( Weight2 > 0 || Weight2 == 0 && pData->fUse0 )
-                Fxu_UpdateDouble( p );
-            else
-                break;
-        }
-        while ( ++pData->nNodesNew < pData->nNodesExt );
-    }
-    else if ( !pData->fUseCompl )
-    {
-        pData->nNodesNew = 0;
-        do
-        {
-            Weight1 = Fxu_HeapSingleReadMaxWeight( p->pHeapSingle );
-            Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
-
-            if ( pData->fVerbose )
-                printf( "Div %5d : Best double = %5d. Best single = %5d.\r", Counter++, Weight2, Weight1 );
-//Fxu_Select( p, &pSingle, &pDouble );
-
-            if ( Weight1 >= Weight2 )
-            {
-                if ( Weight1 > 0 || Weight1 == 0 && pData->fUse0 )
-                    Fxu_UpdateSingle( p );
-                else
-                    break;
-            }
-            else
-            {
-                if ( Weight2 > 0 || Weight2 == 0 && pData->fUse0 )
-                    Fxu_UpdateDouble( p );
-                else
-                    break;
-            }
-        }
-        while ( ++pData->nNodesNew < pData->nNodesExt );
-    }
-    else
-    { // use the complement
-        pData->nNodesNew = 0;
-        do
-        {
-            Weight1 = Fxu_HeapSingleReadMaxWeight( p->pHeapSingle );
-            Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
-
-            // select the best single and double
-            Weight3 = Fxu_Select( p, &pSingle, &pDouble );
-            if ( pData->fVerbose )
-                printf( "Div %5d : Best double = %5d. Best single = %5d. Best complement = %5d.\r", 
-                    Counter++, Weight2, Weight1, Weight3 );
-
-            if ( Weight3 > 0 || Weight3 == 0 && pData->fUse0 )
-                Fxu_Update( p, pSingle, pDouble );
-            else
-                break;
-        }
-        while ( ++pData->nNodesNew < pData->nNodesExt );
-    }
-
-    if ( pData->fVerbose )
-        printf( "Total single = %3d. Total double = %3d. Total compl = %3d.                    \n", 
-        p->nDivs1, p->nDivs2, p->nDivs3 );
-
-    // create the new covers
-    if ( pData->nNodesNew )
-        Fxu_CreateCovers( p, pData );
-    Fxu_MatrixDelete( p );
-//    printf( "Memory usage after deallocation:   Total = %d. Peak = %d.\n", s_MemoryTotal, s_MemoryPeak );
-    if ( pData->nNodesNew == pData->nNodesExt )
-        printf( "Warning: The limit on the number of extracted divisors has been reached.\n" );
-    return pData->nNodesNew;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Unmarks the cubes in the ring.]
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_MatrixRingCubesUnmark( Fxu_Matrix * p )
-{
-    Fxu_Cube * pCube, * pCube2;
-    // unmark the cubes
-    Fxu_MatrixForEachCubeInRingSafe( p, pCube, pCube2 )
-        pCube->pOrder = NULL;
-    Fxu_MatrixRingCubesReset( p );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Unmarks the vars in the ring.]
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_MatrixRingVarsUnmark( Fxu_Matrix * p )
-{
-    Fxu_Var * pVar, * pVar2;
-    // unmark the vars
-    Fxu_MatrixForEachVarInRingSafe( p, pVar, pVar2 )
-        pVar->pOrder = NULL;
-    Fxu_MatrixRingVarsReset( p );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-char * Fxu_MemFetch( Fxu_Matrix * p, int nBytes )
-{
-    s_MemoryTotal += nBytes;
-    if ( s_MemoryPeak < s_MemoryTotal )
-        s_MemoryPeak = s_MemoryTotal;
-//    return malloc( nBytes );
-    return Extra_MmFixedEntryFetch( p->pMemMan );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_MemRecycle( Fxu_Matrix * p, char * pItem, int nBytes )
-{
-    s_MemoryTotal -= nBytes;
-//    free( pItem );
-    Extra_MmFixedEntryRecycle( p->pMemMan, pItem );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/fxu/fxu.h b/src/opt/fxu/fxu.h
deleted file mode 100644
index e6d0b69e..00000000
--- a/src/opt/fxu/fxu.h
+++ /dev/null
@@ -1,93 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fxu.h]
-
-  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
-
-  Synopsis    [External declarations of fast extract for unate covers.]
-
-  Author      [MVSIS Group]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - February 1, 2003.]
-
-  Revision    [$Id: fxu.h,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __FXU_H__
-#define __FXU_H__
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-#include "vec.h"
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                    STRUCTURE DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-#ifndef __cplusplus
-#ifndef bool
-#define bool int
-#endif
-#endif
-
-typedef struct FxuDataStruct   Fxu_Data_t;
-
-// structure for the FX input/output data 
-struct FxuDataStruct
-{
-    // user specified parameters
-    bool              fOnlyS;           // set to 1 to have only single-cube divs
-    bool              fOnlyD;           // set to 1 to have only double-cube divs
-    bool              fUse0;            // set to 1 to have 0-weight also extracted
-    bool              fUseCompl;        // set to 1 to have complement taken into account
-    bool              fVerbose;         // set to 1 to have verbose output
-    int               nNodesExt;        // the number of divisors to extract
-    int               nSingleMax;       // the max number of single-cube divisors to consider
-    int               nPairsMax;        // the max number of double-cube divisors to consider
-    // the input information
-    Vec_Ptr_t *       vSops;            // the SOPs for each node in the network
-    Vec_Ptr_t *       vFanins;          // the fanins of each node in the network
-    // output information
-    Vec_Ptr_t *       vSopsNew;         // the SOPs for each node in the network after extraction
-    Vec_Ptr_t *       vFaninsNew;       // the fanins of each node in the network after extraction
-    // the SOP manager
-    Extra_MmFlex_t *  pManSop;
-    // statistics   
-    int               nNodesOld;        // the old number of nodes
-    int               nNodesNew;        // the number of divisors actually extracted
-};
-
-////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFINITIONS                          ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/*===== fxu.c ==========================================================*/
-extern int          Fxu_FastExtract( Fxu_Data_t * pData );
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c
deleted file mode 100644
index e3300df9..00000000
--- a/src/opt/fxu/fxuCreate.c
+++ /dev/null
@@ -1,431 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fxuCreate.c]
-
-  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
-
-  Synopsis    [Create matrix from covers and covers from matrix.]
-
-  Author      [MVSIS Group]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - February 1, 2003.]
-
-  Revision    [$Id: fxuCreate.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "fxuInt.h"
-#include "fxu.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static void        Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Int_t * vFanins, int * pOrder );
-static int         Fxu_CreateMatrixLitCompare( int * ptrX, int * ptrY );
-static void        Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cube * pCubeFirst, Fxu_Cube * pCubeNext );
-static Fxu_Cube *  Fxu_CreateCoversFirstCube( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode );
-static int * s_pLits;
-
-extern int         Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the sparse matrix from the array of SOPs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
-{
-    Fxu_Matrix * p;
-    Fxu_Var * pVar;
-    Fxu_Cube * pCubeFirst, * pCubeNew;
-    Fxu_Cube * pCube1, * pCube2;
-    Vec_Int_t * vFanins;
-    char * pSopCover;
-    char * pSopCube;
-    int * pOrder, nBitsMax;
-    int i, v, c;
-    int nCubesTotal;
-    int nPairsTotal;
-    int nPairsStore;
-    int nCubes;
-    int iCube, iPair;
-    int nFanins;
-
-    // collect all sorts of statistics
-    nCubesTotal =  0;
-    nPairsTotal =  0;
-    nPairsStore =  0;
-    nBitsMax    = -1;
-    for ( i = 0; i < pData->nNodesOld; i++ )
-        if ( pSopCover = pData->vSops->pArray[i] )
-        {
-            nCubes       = Abc_SopGetCubeNum( pSopCover );
-            nFanins      = Abc_SopGetVarNum( pSopCover );
-            assert( nFanins > 1 && nCubes > 0 );
-
-            nCubesTotal += nCubes;
-            nPairsTotal += nCubes * (nCubes - 1) / 2;
-            nPairsStore += nCubes * nCubes;
-            if ( nBitsMax < nFanins )
-                nBitsMax = nFanins;
-        }
-    if ( nBitsMax <= 0 )
-    {
-        printf( "The current network does not have SOPs to perform extraction.\n" );
-        return NULL;
-    }
-/*
-    if ( nPairsStore > 10000000 )
-    {
-        printf( "The problem is too large to be solved by \"fxu\" (%d cubes and %d cube pairs)\n", nCubesTotal, nPairsStore );
-        return NULL;
-    }
-*/
-    // start the matrix
-    p = Fxu_MatrixAllocate();
-    // create the column labels 
-    p->ppVars = ALLOC( Fxu_Var *, 2 * (pData->nNodesOld + pData->nNodesExt) );
-    for ( i = 0; i < 2 * pData->nNodesOld; i++ )
-        p->ppVars[i] = Fxu_MatrixAddVar( p );
-
-    // allocate storage for all cube pairs at once
-    p->pppPairs = ALLOC( Fxu_Pair **, nCubesTotal + 100 );
-    p->ppPairs  = ALLOC( Fxu_Pair *,  nPairsStore + 100 );
-    memset( p->ppPairs, 0, sizeof(Fxu_Pair *) * nPairsStore );
-    iCube = 0;
-    iPair = 0;
-    for ( i = 0; i < pData->nNodesOld; i++ )
-        if ( pSopCover = pData->vSops->pArray[i] )
-        {
-            // get the number of cubes
-            nCubes = Abc_SopGetCubeNum( pSopCover );
-            // get the new var in the matrix
-            pVar = p->ppVars[2*i+1];
-            // assign the pair storage
-            pVar->nCubes     = nCubes;
-            if ( nCubes > 0 )
-            {
-                pVar->ppPairs    = p->pppPairs + iCube;
-                pVar->ppPairs[0] = p->ppPairs  + iPair;
-                for ( v = 1; v < nCubes; v++ )
-                    pVar->ppPairs[v] = pVar->ppPairs[v-1] + nCubes;
-            }
-            // update
-            iCube += nCubes;
-            iPair += nCubes * nCubes;
-        }
-    assert( iCube == nCubesTotal );
-    assert( iPair == nPairsStore );
-
-
-    // allocate room for the reordered literals
-    pOrder = ALLOC( int, nBitsMax );
-    // create the rows
-    for ( i = 0; i < pData->nNodesOld; i++ )
-    if ( pSopCover = pData->vSops->pArray[i] )
-    {
-        // get the new var in the matrix
-        pVar = p->ppVars[2*i+1];
-        // here we sort the literals of the cover
-        // in the increasing order of the numbers of the corresponding nodes
-        // because literals should be added to the matrix in this order
-        vFanins = pData->vFanins->pArray[i];
-        s_pLits = vFanins->pArray;
-        // start the variable order
-        nFanins = Abc_SopGetVarNum( pSopCover );
-        for ( v = 0; v < nFanins; v++ )
-            pOrder[v] = v;
-        // reorder the fanins
-        qsort( (void *)pOrder, nFanins, sizeof(int),(int (*)(const void *, const void *))Fxu_CreateMatrixLitCompare);
-        assert( s_pLits[ pOrder[0] ] < s_pLits[ pOrder[nFanins-1] ] );
-        // create the corresponding cubes in the matrix
-        pCubeFirst = NULL;
-        c = 0;
-        Abc_SopForEachCube( pSopCover, nFanins, pSopCube )
-        {
-            // create the cube
-            pCubeNew = Fxu_MatrixAddCube( p, pVar, c++ );
-            Fxu_CreateMatrixAddCube( p, pCubeNew, pSopCube, vFanins, pOrder );
-            if ( pCubeFirst == NULL )
-                pCubeFirst = pCubeNew;
-            pCubeNew->pFirst = pCubeFirst;
-        }
-        // set the first cube of this var
-        pVar->pFirst = pCubeFirst;
-        // create the divisors without preprocessing
-        if ( nPairsTotal <= pData->nPairsMax )
-        {
-            for ( pCube1 = pCubeFirst; pCube1; pCube1 = pCube1->pNext )
-                for ( pCube2 = pCube1? pCube1->pNext: NULL; pCube2; pCube2 = pCube2->pNext )
-                    Fxu_MatrixAddDivisor( p, pCube1, pCube2 );
-        }
-    }
-    FREE( pOrder );
-
-    // consider the case when cube pairs should be preprocessed
-    // before adding them to the set of divisors
-//    if ( pData->fVerbose )
-//        printf( "The total number of cube pairs is %d.\n", nPairsTotal );
-    if ( nPairsTotal > 10000000 )
-    {
-        printf( "The total number of cube pairs of the network is more than 10,000,000.\n" );
-        printf( "Command \"fx\" takes a long time to run in such cases. It is suggested\n" );
-        printf( "that the user changes the network by reducing the size of logic node and\n" );
-        printf( "consequently the number of cube pairs to be processed by this command.\n" );
-        printf( "One way to achieve this is to run the commands \"st; multi -m -F <num>\"\n" );
-        printf( "as a proprocessing step, while selecting <num> as approapriate.\n" );
-        return NULL;
-    }
-    if ( nPairsTotal > pData->nPairsMax )
-        if ( !Fxu_PreprocessCubePairs( p, pData->vSops, nPairsTotal, pData->nPairsMax ) )
-            return NULL;
-//    if ( pData->fVerbose )
-//        printf( "Only %d best cube pairs will be used by the fast extract command.\n", pData->nPairsMax );
-
-    // add the var pairs to the heap
-    Fxu_MatrixComputeSingles( p, pData->fUse0, pData->nSingleMax );
-
-    // print stats
-    if ( pData->fVerbose )
-    {
-        double Density;
-        Density = ((double)p->nEntries) / p->lVars.nItems / p->lCubes.nItems;
-        fprintf( stdout, "Matrix: [vars x cubes] = [%d x %d]  ",
-            p->lVars.nItems, p->lCubes.nItems );
-        fprintf( stdout, "Lits = %d  Density = %.5f%%\n", 
-            p->nEntries, Density );
-        fprintf( stdout, "1-cube divs = %6d. (Total = %6d)  ",  p->lSingles.nItems, p->nSingleTotal );
-        fprintf( stdout, "2-cube divs = %6d. (Total = %6d)",  p->nDivsTotal, nPairsTotal );
-        fprintf( stdout, "\n" );
-    }
-//    Fxu_MatrixPrint( stdout, p );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds one cube with literals to the matrix.]
-
-  Description [Create the cube and literals in the matrix corresponding 
-  to the given cube in the SOP cover. Co-singleton transform is performed here.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Int_t * vFanins, int * pOrder )
-{
-    Fxu_Var * pVar;
-    int Value, i;
-    // add literals to the matrix
-    Abc_CubeForEachVar( pSopCube, Value, i )
-    {
-        Value = pSopCube[pOrder[i]];
-        if ( Value == '0' )
-        {
-            pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]] + 1 ];  // CST
-            Fxu_MatrixAddLiteral( p, pCube, pVar );
-        }
-        else if ( Value == '1' )
-        {
-            pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]] ];  // CST
-            Fxu_MatrixAddLiteral( p, pCube, pVar );
-        }
-    }
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the new array of Sop covers from the sparse matrix.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_CreateCovers( Fxu_Matrix * p, Fxu_Data_t * pData )
-{
-    Fxu_Cube * pCube, * pCubeFirst, * pCubeNext;
-    char * pSopCover;
-    int iNode, n;
-
-    // get the first cube of the first internal node 
-    pCubeFirst = Fxu_CreateCoversFirstCube( p, pData, 0 );
-
-    // go through the internal nodes
-    for ( n = 0; n < pData->nNodesOld; n++ )
-    if ( pSopCover = pData->vSops->pArray[n] )
-    {
-        // get the number of this node
-        iNode = n;
-        // get the next first cube
-        pCubeNext = Fxu_CreateCoversFirstCube(  p, pData, iNode + 1 );
-        // check if there any new variables in these cubes
-        for ( pCube = pCubeFirst; pCube != pCubeNext; pCube = pCube->pNext )
-            if ( pCube->lLits.pTail && pCube->lLits.pTail->iVar >= 2 * pData->nNodesOld )
-                break;
-        if ( pCube != pCubeNext )
-            Fxu_CreateCoversNode( p, pData, iNode, pCubeFirst, pCubeNext );
-        // update the first cube
-        pCubeFirst = pCubeNext;
-    }
-
-    // add the covers for the extracted nodes
-    for ( n = 0; n < pData->nNodesNew; n++ )
-    {
-        // get the number of this node
-        iNode = pData->nNodesOld + n;
-        // get the next first cube
-        pCubeNext = Fxu_CreateCoversFirstCube( p, pData, iNode + 1 );
-        // the node should be added
-        Fxu_CreateCoversNode( p, pData, iNode, pCubeFirst, pCubeNext );
-        // update the first cube
-        pCubeFirst = pCubeNext;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Create Sop covers for one node that has changed.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cube * pCubeFirst, Fxu_Cube * pCubeNext )
-{
-    Vec_Int_t * vInputsNew;
-    char * pSopCover, * pSopCube;
-    Fxu_Var * pVar;
-    Fxu_Cube * pCube;
-    Fxu_Lit * pLit;
-    int iNum, nCubes, v;
-
-    // collect positive polarity variable in the cubes between pCubeFirst and pCubeNext
-    Fxu_MatrixRingVarsStart( p );
-    for ( pCube = pCubeFirst; pCube != pCubeNext; pCube = pCube->pNext )
-        for ( pLit = pCube->lLits.pHead; pLit; pLit = pLit->pHNext )
-        {
-            pVar = p->ppVars[ 2 * (pLit->pVar->iVar/2) + 1 ];
-            if ( pVar->pOrder == NULL )
-                Fxu_MatrixRingVarsAdd( p, pVar );
-        }
-    Fxu_MatrixRingVarsStop( p );
-
-    // collect the variable numbers
-    vInputsNew = Vec_IntAlloc( 4 );
-    Fxu_MatrixForEachVarInRing( p, pVar )
-        Vec_IntPush( vInputsNew, pVar->iVar / 2 );
-    Fxu_MatrixRingVarsUnmark( p );
-
-    // sort the vars by their number
-    Vec_IntSort( vInputsNew, 0 );
-
-    // mark the vars with their numbers in the sorted array
-    for ( v = 0; v < vInputsNew->nSize; v++ )
-    {
-        p->ppVars[ 2 * vInputsNew->pArray[v] + 0 ]->lLits.nItems = v; // hack - reuse lLits.nItems
-        p->ppVars[ 2 * vInputsNew->pArray[v] + 1 ]->lLits.nItems = v; // hack - reuse lLits.nItems
-    }
-
-    // count the number of cubes
-    nCubes = 0;
-    for ( pCube = pCubeFirst; pCube != pCubeNext; pCube = pCube->pNext )
-        if ( pCube->lLits.nItems )
-            nCubes++;
-
-    // allocate room for the new cover
-    pSopCover = Abc_SopStart( pData->pManSop, nCubes, vInputsNew->nSize );
-    // set the correct polarity of the cover
-    if ( iNode < pData->nNodesOld && Abc_SopGetPhase( pData->vSops->pArray[iNode] ) == 0 )
-        Abc_SopComplement( pSopCover );
-
-    // add the cubes
-    nCubes = 0;
-    for ( pCube = pCubeFirst; pCube != pCubeNext; pCube = pCube->pNext )
-    {
-        if ( pCube->lLits.nItems == 0 )
-            continue;
-        // get hold of the SOP cube
-        pSopCube = pSopCover + nCubes * (vInputsNew->nSize + 3);
-        // insert literals
-        for ( pLit = pCube->lLits.pHead; pLit; pLit = pLit->pHNext )
-        {
-            iNum = pLit->pVar->lLits.nItems; // hack - reuse lLits.nItems
-            assert( iNum < vInputsNew->nSize );
-            if ( pLit->pVar->iVar / 2 < pData->nNodesOld )
-                pSopCube[iNum] = (pLit->pVar->iVar & 1)? '0' : '1';   // reverse CST
-            else
-                pSopCube[iNum] = (pLit->pVar->iVar & 1)? '1' : '0';   // no CST
-        }
-        // count the cube
-        nCubes++;
-    }
-    assert( nCubes == Abc_SopGetCubeNum(pSopCover) );
-
-    // set the new cover and the array of fanins
-    pData->vSopsNew->pArray[iNode]   = pSopCover;
-    pData->vFaninsNew->pArray[iNode] = vInputsNew;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Adds the var to storage.]
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fxu_Cube * Fxu_CreateCoversFirstCube( Fxu_Matrix * p, Fxu_Data_t * pData, int iVar )
-{
-    int v;
-    for ( v = iVar; v < pData->nNodesOld + pData->nNodesNew; v++ )
-        if ( p->ppVars[ 2*v + 1 ]->pFirst )
-            return p->ppVars[ 2*v + 1 ]->pFirst;
-    return NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Compares the vars by their number.]
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fxu_CreateMatrixLitCompare( int * ptrX, int * ptrY )
-{
-    return s_pLits[*ptrX] - s_pLits[*ptrY];
-} 
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/fxu/fxuHeapD.c b/src/opt/fxu/fxuHeapD.c
deleted file mode 100644
index c81ad818..00000000
--- a/src/opt/fxu/fxuHeapD.c
+++ /dev/null
@@ -1,445 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fxuHeapD.c]
-
-  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
-
-  Synopsis    [The priority queue for double cube divisors.]
-
-  Author      [MVSIS Group]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - February 1, 2003.]
-
-  Revision    [$Id: fxuHeapD.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fxuInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-#define FXU_HEAP_DOUBLE_WEIGHT(pDiv)           ((pDiv)->Weight)
-#define FXU_HEAP_DOUBLE_CURRENT(p, pDiv)       ((p)->pTree[(pDiv)->HNum])
-#define FXU_HEAP_DOUBLE_PARENT_EXISTS(p, pDiv) ((pDiv)->HNum > 1)
-#define FXU_HEAP_DOUBLE_CHILD1_EXISTS(p, pDiv) (((pDiv)->HNum << 1) <= p->nItems)
-#define FXU_HEAP_DOUBLE_CHILD2_EXISTS(p, pDiv) ((((pDiv)->HNum << 1)+1) <= p->nItems)
-#define FXU_HEAP_DOUBLE_PARENT(p, pDiv)        ((p)->pTree[(pDiv)->HNum >> 1])
-#define FXU_HEAP_DOUBLE_CHILD1(p, pDiv)        ((p)->pTree[(pDiv)->HNum << 1])
-#define FXU_HEAP_DOUBLE_CHILD2(p, pDiv)        ((p)->pTree[((pDiv)->HNum << 1)+1])
-#define FXU_HEAP_DOUBLE_ASSERT(p, pDiv)        assert( (pDiv)->HNum >= 1 && (pDiv)->HNum <= p->nItemsAlloc )
-
-static void Fxu_HeapDoubleResize( Fxu_HeapDouble * p );                  
-static void Fxu_HeapDoubleSwap( Fxu_Double ** pDiv1, Fxu_Double ** pDiv2 );  
-static void Fxu_HeapDoubleMoveUp( Fxu_HeapDouble * p, Fxu_Double * pDiv );  
-static void Fxu_HeapDoubleMoveDn( Fxu_HeapDouble * p, Fxu_Double * pDiv );  
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fxu_HeapDouble * Fxu_HeapDoubleStart()
-{
-    Fxu_HeapDouble * p;
-    p = ALLOC( Fxu_HeapDouble, 1 );
-    memset( p, 0, sizeof(Fxu_HeapDouble) );
-    p->nItems      = 0;
-    p->nItemsAlloc = 10000;
-    p->pTree       = ALLOC( Fxu_Double *, p->nItemsAlloc + 1 );
-    p->pTree[0]    = NULL;
-    return p;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapDoubleResize( Fxu_HeapDouble * p )
-{
-    p->nItemsAlloc *= 2;
-    p->pTree = REALLOC( Fxu_Double *, p->pTree, p->nItemsAlloc + 1 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapDoubleStop( Fxu_HeapDouble * p )
-{
-    free( p->pTree );
-    free( p );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapDoublePrint( FILE * pFile, Fxu_HeapDouble * p )
-{
-    Fxu_Double * pDiv;
-    int Counter = 1;
-    int Degree  = 1;
-
-    Fxu_HeapDoubleCheck( p );
-    fprintf( pFile, "The contents of the heap:\n" );
-    fprintf( pFile, "Level %d:  ", Degree );
-    Fxu_HeapDoubleForEachItem( p, pDiv )
-    {
-        assert( Counter == p->pTree[Counter]->HNum );
-        fprintf( pFile, "%2d=%3d  ", Counter, FXU_HEAP_DOUBLE_WEIGHT(p->pTree[Counter]) );
-        if ( ++Counter == (1 << Degree) )
-        {
-            fprintf( pFile, "\n" );
-            Degree++;
-            fprintf( pFile, "Level %d:  ", Degree );
-        }
-    }
-    fprintf( pFile, "\n" );
-    fprintf( pFile, "End of the heap printout.\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapDoubleCheck( Fxu_HeapDouble * p )
-{
-    Fxu_Double * pDiv;
-    Fxu_HeapDoubleForEachItem( p, pDiv )
-    {
-        assert( pDiv->HNum == p->i );
-        Fxu_HeapDoubleCheckOne( p, pDiv );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapDoubleCheckOne( Fxu_HeapDouble * p, Fxu_Double * pDiv )
-{
-    int Weight1, Weight2;
-    if ( FXU_HEAP_DOUBLE_CHILD1_EXISTS(p,pDiv) )
-    {
-        Weight1 = FXU_HEAP_DOUBLE_WEIGHT(pDiv);
-        Weight2 = FXU_HEAP_DOUBLE_WEIGHT( FXU_HEAP_DOUBLE_CHILD1(p,pDiv) );
-        assert( Weight1 >= Weight2 );
-    }
-    if ( FXU_HEAP_DOUBLE_CHILD2_EXISTS(p,pDiv) )
-    {
-        Weight1 = FXU_HEAP_DOUBLE_WEIGHT(pDiv);
-        Weight2 = FXU_HEAP_DOUBLE_WEIGHT( FXU_HEAP_DOUBLE_CHILD2(p,pDiv) );
-        assert( Weight1 >= Weight2 );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapDoubleInsert( Fxu_HeapDouble * p, Fxu_Double * pDiv )
-{
-    if ( p->nItems == p->nItemsAlloc )
-        Fxu_HeapDoubleResize( p );
-    // put the last entry to the last place and move up
-    p->pTree[++p->nItems] = pDiv;
-    pDiv->HNum = p->nItems;
-    // move the last entry up if necessary
-    Fxu_HeapDoubleMoveUp( p, pDiv );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapDoubleUpdate( Fxu_HeapDouble * p, Fxu_Double * pDiv )
-{
-//printf( "Updating divisor %d.\n", pDiv->Num );
-
-    FXU_HEAP_DOUBLE_ASSERT(p,pDiv);
-    if ( FXU_HEAP_DOUBLE_PARENT_EXISTS(p,pDiv) && 
-         FXU_HEAP_DOUBLE_WEIGHT(pDiv) > FXU_HEAP_DOUBLE_WEIGHT( FXU_HEAP_DOUBLE_PARENT(p,pDiv) ) )
-        Fxu_HeapDoubleMoveUp( p, pDiv );
-    else if ( FXU_HEAP_DOUBLE_CHILD1_EXISTS(p,pDiv) && 
-        FXU_HEAP_DOUBLE_WEIGHT(pDiv) < FXU_HEAP_DOUBLE_WEIGHT( FXU_HEAP_DOUBLE_CHILD1(p,pDiv) ) )
-        Fxu_HeapDoubleMoveDn( p, pDiv );
-    else if ( FXU_HEAP_DOUBLE_CHILD2_EXISTS(p,pDiv) && 
-        FXU_HEAP_DOUBLE_WEIGHT(pDiv) < FXU_HEAP_DOUBLE_WEIGHT( FXU_HEAP_DOUBLE_CHILD2(p,pDiv) ) )
-        Fxu_HeapDoubleMoveDn( p, pDiv );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapDoubleDelete( Fxu_HeapDouble * p, Fxu_Double * pDiv )
-{
-    FXU_HEAP_DOUBLE_ASSERT(p,pDiv);
-    // put the last entry to the deleted place
-    // decrement the number of entries
-    p->pTree[pDiv->HNum] = p->pTree[p->nItems--];
-    p->pTree[pDiv->HNum]->HNum = pDiv->HNum;
-    // move the top entry down if necessary
-    Fxu_HeapDoubleUpdate( p, p->pTree[pDiv->HNum] );
-    pDiv->HNum = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fxu_Double * Fxu_HeapDoubleReadMax( Fxu_HeapDouble * p )
-{
-    if ( p->nItems == 0 )
-        return NULL;
-    return p->pTree[1];     
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fxu_Double * Fxu_HeapDoubleGetMax( Fxu_HeapDouble * p )
-{
-    Fxu_Double * pDiv;
-    if ( p->nItems == 0 )
-        return NULL;
-    // prepare the return value
-    pDiv = p->pTree[1];
-    pDiv->HNum = 0;
-    // put the last entry on top
-    // decrement the number of entries
-    p->pTree[1] = p->pTree[p->nItems--];
-    p->pTree[1]->HNum = 1;
-    // move the top entry down if necessary
-    Fxu_HeapDoubleMoveDn( p, p->pTree[1] );
-    return pDiv;     
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int  Fxu_HeapDoubleReadMaxWeight( Fxu_HeapDouble * p )
-{
-    if ( p->nItems == 0 )
-        return -1;
-    else
-        return FXU_HEAP_DOUBLE_WEIGHT(p->pTree[1]);
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapDoubleSwap( Fxu_Double ** pDiv1, Fxu_Double ** pDiv2 )
-{
-    Fxu_Double * pDiv;
-    int Temp;
-    pDiv   = *pDiv1;
-    *pDiv1 = *pDiv2;
-    *pDiv2 = pDiv;
-    Temp          = (*pDiv1)->HNum;
-    (*pDiv1)->HNum = (*pDiv2)->HNum;
-    (*pDiv2)->HNum = Temp;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapDoubleMoveUp( Fxu_HeapDouble * p, Fxu_Double * pDiv )
-{
-    Fxu_Double ** ppDiv, ** ppPar;
-    ppDiv = &FXU_HEAP_DOUBLE_CURRENT(p, pDiv);
-    while ( FXU_HEAP_DOUBLE_PARENT_EXISTS(p,*ppDiv) )
-    {
-        ppPar = &FXU_HEAP_DOUBLE_PARENT(p,*ppDiv);
-        if ( FXU_HEAP_DOUBLE_WEIGHT(*ppDiv) > FXU_HEAP_DOUBLE_WEIGHT(*ppPar) )
-        {
-            Fxu_HeapDoubleSwap( ppDiv, ppPar );
-            ppDiv = ppPar;
-        }
-        else
-            break;
-    }
-}
- 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapDoubleMoveDn( Fxu_HeapDouble * p, Fxu_Double * pDiv )
-{
-    Fxu_Double ** ppChild1, ** ppChild2, ** ppDiv;
-    ppDiv = &FXU_HEAP_DOUBLE_CURRENT(p, pDiv);
-    while ( FXU_HEAP_DOUBLE_CHILD1_EXISTS(p,*ppDiv) )
-    { // if Child1 does not exist, Child2 also does not exists
-
-        // get the children
-        ppChild1 = &FXU_HEAP_DOUBLE_CHILD1(p,*ppDiv);
-        if ( FXU_HEAP_DOUBLE_CHILD2_EXISTS(p,*ppDiv) )
-        {
-            ppChild2 = &FXU_HEAP_DOUBLE_CHILD2(p,*ppDiv);
-
-            // consider two cases
-            if ( FXU_HEAP_DOUBLE_WEIGHT(*ppDiv) >= FXU_HEAP_DOUBLE_WEIGHT(*ppChild1) &&
-                 FXU_HEAP_DOUBLE_WEIGHT(*ppDiv) >= FXU_HEAP_DOUBLE_WEIGHT(*ppChild2) )
-            { // Div is larger than both, skip
-                break;
-            }
-            else
-            { // Div is smaller than one of them, then swap it with larger 
-                if ( FXU_HEAP_DOUBLE_WEIGHT(*ppChild1) >= FXU_HEAP_DOUBLE_WEIGHT(*ppChild2) )
-                {
-                    Fxu_HeapDoubleSwap( ppDiv, ppChild1 );
-                    // update the pointer
-                    ppDiv = ppChild1;
-                }
-                else
-                {
-                    Fxu_HeapDoubleSwap( ppDiv, ppChild2 );
-                    // update the pointer
-                    ppDiv = ppChild2;
-                }
-            }
-        }
-        else // Child2 does not exist
-        {
-            // consider two cases
-            if ( FXU_HEAP_DOUBLE_WEIGHT(*ppDiv) >= FXU_HEAP_DOUBLE_WEIGHT(*ppChild1) )
-            { // Div is larger than Child1, skip
-                break;
-            }
-            else
-            { // Div is smaller than Child1, then swap them
-                Fxu_HeapDoubleSwap( ppDiv, ppChild1 );
-                // update the pointer
-                ppDiv = ppChild1;
-            }
-        }
-    }
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/fxu/fxuHeapS.c b/src/opt/fxu/fxuHeapS.c
deleted file mode 100644
index eaca8363..00000000
--- a/src/opt/fxu/fxuHeapS.c
+++ /dev/null
@@ -1,444 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fxuHeapS.c]
-
-  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
-
-  Synopsis    [The priority queue for variables.]
-
-  Author      [MVSIS Group]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - February 1, 2003.]
-
-  Revision    [$Id: fxuHeapS.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fxuInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-#define FXU_HEAP_SINGLE_WEIGHT(pSingle)           ((pSingle)->Weight)
-#define FXU_HEAP_SINGLE_CURRENT(p, pSingle)       ((p)->pTree[(pSingle)->HNum])
-#define FXU_HEAP_SINGLE_PARENT_EXISTS(p, pSingle) ((pSingle)->HNum > 1)
-#define FXU_HEAP_SINGLE_CHILD1_EXISTS(p, pSingle) (((pSingle)->HNum << 1) <= p->nItems)
-#define FXU_HEAP_SINGLE_CHILD2_EXISTS(p, pSingle) ((((pSingle)->HNum << 1)+1) <= p->nItems)
-#define FXU_HEAP_SINGLE_PARENT(p, pSingle)        ((p)->pTree[(pSingle)->HNum >> 1])
-#define FXU_HEAP_SINGLE_CHILD1(p, pSingle)        ((p)->pTree[(pSingle)->HNum << 1])
-#define FXU_HEAP_SINGLE_CHILD2(p, pSingle)        ((p)->pTree[((pSingle)->HNum << 1)+1])
-#define FXU_HEAP_SINGLE_ASSERT(p, pSingle)        assert( (pSingle)->HNum >= 1 && (pSingle)->HNum <= p->nItemsAlloc )
-
-static void Fxu_HeapSingleResize( Fxu_HeapSingle * p );                  
-static void Fxu_HeapSingleSwap( Fxu_Single ** pSingle1, Fxu_Single ** pSingle2 );  
-static void Fxu_HeapSingleMoveUp( Fxu_HeapSingle * p, Fxu_Single * pSingle );  
-static void Fxu_HeapSingleMoveDn( Fxu_HeapSingle * p, Fxu_Single * pSingle );  
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fxu_HeapSingle * Fxu_HeapSingleStart()
-{
-    Fxu_HeapSingle * p;
-    p = ALLOC( Fxu_HeapSingle, 1 );
-    memset( p, 0, sizeof(Fxu_HeapSingle) );
-    p->nItems      = 0;
-    p->nItemsAlloc = 2000;
-    p->pTree       = ALLOC( Fxu_Single *, p->nItemsAlloc + 10 );
-    p->pTree[0]    = NULL;
-    return p;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapSingleResize( Fxu_HeapSingle * p )
-{
-    p->nItemsAlloc *= 2;
-    p->pTree = REALLOC( Fxu_Single *, p->pTree, p->nItemsAlloc + 10 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapSingleStop( Fxu_HeapSingle * p )
-{
-    int i;
-    i = 0;
-    free( p->pTree );
-    i = 1;
-    free( p );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapSinglePrint( FILE * pFile, Fxu_HeapSingle * p )
-{
-    Fxu_Single * pSingle;
-    int Counter = 1;
-    int Degree  = 1;
-
-    Fxu_HeapSingleCheck( p );
-    fprintf( pFile, "The contents of the heap:\n" );
-    fprintf( pFile, "Level %d:  ", Degree );
-    Fxu_HeapSingleForEachItem( p, pSingle )
-    {
-        assert( Counter == p->pTree[Counter]->HNum );
-        fprintf( pFile, "%2d=%3d  ", Counter, FXU_HEAP_SINGLE_WEIGHT(p->pTree[Counter]) );
-        if ( ++Counter == (1 << Degree) )
-        {
-            fprintf( pFile, "\n" );
-            Degree++;
-            fprintf( pFile, "Level %d:  ", Degree );
-        }
-    }
-    fprintf( pFile, "\n" );
-    fprintf( pFile, "End of the heap printout.\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapSingleCheck( Fxu_HeapSingle * p )
-{
-    Fxu_Single * pSingle;
-    Fxu_HeapSingleForEachItem( p, pSingle )
-    {
-        assert( pSingle->HNum == p->i );
-        Fxu_HeapSingleCheckOne( p, pSingle );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapSingleCheckOne( Fxu_HeapSingle * p, Fxu_Single * pSingle )
-{
-    int Weight1, Weight2;
-    if ( FXU_HEAP_SINGLE_CHILD1_EXISTS(p,pSingle) )
-    {
-        Weight1 = FXU_HEAP_SINGLE_WEIGHT(pSingle);
-        Weight2 = FXU_HEAP_SINGLE_WEIGHT( FXU_HEAP_SINGLE_CHILD1(p,pSingle) );
-        assert( Weight1 >= Weight2 );
-    }
-    if ( FXU_HEAP_SINGLE_CHILD2_EXISTS(p,pSingle) )
-    {
-        Weight1 = FXU_HEAP_SINGLE_WEIGHT(pSingle);
-        Weight2 = FXU_HEAP_SINGLE_WEIGHT( FXU_HEAP_SINGLE_CHILD2(p,pSingle) );
-        assert( Weight1 >= Weight2 );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapSingleInsert( Fxu_HeapSingle * p, Fxu_Single * pSingle )
-{
-    if ( p->nItems == p->nItemsAlloc )
-        Fxu_HeapSingleResize( p );
-    // put the last entry to the last place and move up
-    p->pTree[++p->nItems] = pSingle;
-    pSingle->HNum = p->nItems;
-    // move the last entry up if necessary
-    Fxu_HeapSingleMoveUp( p, pSingle );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapSingleUpdate( Fxu_HeapSingle * p, Fxu_Single * pSingle )
-{
-    FXU_HEAP_SINGLE_ASSERT(p,pSingle);
-    if ( FXU_HEAP_SINGLE_PARENT_EXISTS(p,pSingle) && 
-         FXU_HEAP_SINGLE_WEIGHT(pSingle) > FXU_HEAP_SINGLE_WEIGHT( FXU_HEAP_SINGLE_PARENT(p,pSingle) ) )
-        Fxu_HeapSingleMoveUp( p, pSingle );
-    else if ( FXU_HEAP_SINGLE_CHILD1_EXISTS(p,pSingle) && 
-        FXU_HEAP_SINGLE_WEIGHT(pSingle) < FXU_HEAP_SINGLE_WEIGHT( FXU_HEAP_SINGLE_CHILD1(p,pSingle) ) )
-        Fxu_HeapSingleMoveDn( p, pSingle );
-    else if ( FXU_HEAP_SINGLE_CHILD2_EXISTS(p,pSingle) && 
-        FXU_HEAP_SINGLE_WEIGHT(pSingle) < FXU_HEAP_SINGLE_WEIGHT( FXU_HEAP_SINGLE_CHILD2(p,pSingle) ) )
-        Fxu_HeapSingleMoveDn( p, pSingle );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapSingleDelete( Fxu_HeapSingle * p, Fxu_Single * pSingle )
-{
-    int Place = pSingle->HNum;
-    FXU_HEAP_SINGLE_ASSERT(p,pSingle);
-    // put the last entry to the deleted place
-    // decrement the number of entries
-    p->pTree[Place] = p->pTree[p->nItems--];
-    p->pTree[Place]->HNum = Place;
-    // move the top entry down if necessary
-    Fxu_HeapSingleUpdate( p, p->pTree[Place] );
-    pSingle->HNum = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fxu_Single * Fxu_HeapSingleReadMax( Fxu_HeapSingle * p )
-{
-    if ( p->nItems == 0 )
-        return NULL;
-    return p->pTree[1];
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fxu_Single * Fxu_HeapSingleGetMax( Fxu_HeapSingle * p )
-{
-    Fxu_Single * pSingle;
-    if ( p->nItems == 0 )
-        return NULL;
-    // prepare the return value
-    pSingle = p->pTree[1];
-    pSingle->HNum = 0;
-    // put the last entry on top
-    // decrement the number of entries
-    p->pTree[1] = p->pTree[p->nItems--];
-    p->pTree[1]->HNum = 1;
-    // move the top entry down if necessary
-    Fxu_HeapSingleMoveDn( p, p->pTree[1] );
-    return pSingle;     
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int  Fxu_HeapSingleReadMaxWeight( Fxu_HeapSingle * p )
-{
-    if ( p->nItems == 0 )
-        return -1;
-    return FXU_HEAP_SINGLE_WEIGHT(p->pTree[1]);
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapSingleSwap( Fxu_Single ** pSingle1, Fxu_Single ** pSingle2 )
-{
-    Fxu_Single * pSingle;
-    int Temp;
-    pSingle   = *pSingle1;
-    *pSingle1 = *pSingle2;
-    *pSingle2 = pSingle;
-    Temp          = (*pSingle1)->HNum;
-    (*pSingle1)->HNum = (*pSingle2)->HNum;
-    (*pSingle2)->HNum = Temp;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapSingleMoveUp( Fxu_HeapSingle * p, Fxu_Single * pSingle )
-{
-    Fxu_Single ** ppSingle, ** ppPar;
-    ppSingle = &FXU_HEAP_SINGLE_CURRENT(p, pSingle);
-    while ( FXU_HEAP_SINGLE_PARENT_EXISTS(p,*ppSingle) )
-    {
-        ppPar = &FXU_HEAP_SINGLE_PARENT(p,*ppSingle);
-        if ( FXU_HEAP_SINGLE_WEIGHT(*ppSingle) > FXU_HEAP_SINGLE_WEIGHT(*ppPar) )
-        {
-            Fxu_HeapSingleSwap( ppSingle, ppPar );
-            ppSingle = ppPar;
-        }
-        else
-            break;
-    }
-}
- 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_HeapSingleMoveDn( Fxu_HeapSingle * p, Fxu_Single * pSingle )
-{
-    Fxu_Single ** ppChild1, ** ppChild2, ** ppSingle;
-    ppSingle = &FXU_HEAP_SINGLE_CURRENT(p, pSingle);
-    while ( FXU_HEAP_SINGLE_CHILD1_EXISTS(p,*ppSingle) )
-    { // if Child1 does not exist, Child2 also does not exists
-
-        // get the children
-        ppChild1 = &FXU_HEAP_SINGLE_CHILD1(p,*ppSingle);
-        if ( FXU_HEAP_SINGLE_CHILD2_EXISTS(p,*ppSingle) )
-        {
-            ppChild2 = &FXU_HEAP_SINGLE_CHILD2(p,*ppSingle);
-
-            // consider two cases
-            if ( FXU_HEAP_SINGLE_WEIGHT(*ppSingle) >= FXU_HEAP_SINGLE_WEIGHT(*ppChild1) &&
-                 FXU_HEAP_SINGLE_WEIGHT(*ppSingle) >= FXU_HEAP_SINGLE_WEIGHT(*ppChild2) )
-            { // Var is larger than both, skip
-                break;
-            }
-            else
-            { // Var is smaller than one of them, then swap it with larger 
-                if ( FXU_HEAP_SINGLE_WEIGHT(*ppChild1) >= FXU_HEAP_SINGLE_WEIGHT(*ppChild2) )
-                {
-                    Fxu_HeapSingleSwap( ppSingle, ppChild1 );
-                    // update the pointer
-                    ppSingle = ppChild1;
-                }
-                else
-                {
-                    Fxu_HeapSingleSwap( ppSingle, ppChild2 );
-                    // update the pointer
-                    ppSingle = ppChild2;
-                }
-            }
-        }
-        else // Child2 does not exist
-        {
-            // consider two cases
-            if ( FXU_HEAP_SINGLE_WEIGHT(*ppSingle) >= FXU_HEAP_SINGLE_WEIGHT(*ppChild1) )
-            { // Var is larger than Child1, skip
-                break;
-            }
-            else
-            { // Var is smaller than Child1, then swap them
-                Fxu_HeapSingleSwap( ppSingle, ppChild1 );
-                // update the pointer
-                ppSingle = ppChild1;
-            }
-        }
-    }
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/fxu/fxuInt.h b/src/opt/fxu/fxuInt.h
deleted file mode 100644
index ea85cb79..00000000
--- a/src/opt/fxu/fxuInt.h
+++ /dev/null
@@ -1,539 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fxuInt.h]
-
-  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
-
-  Synopsis    [Internal declarations of fast extract for unate covers.]
-
-  Author      [MVSIS Group]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - February 1, 2003.]
-
-  Revision    [$Id: fxuInt.h,v 1.3 2003/04/10 05:42:44 donald Exp $]
-
-***********************************************************************/
- 
-#ifndef __FXU_INT_H__
-#define __FXU_INT_H__
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-#include "extra.h"
-#include "vec.h"
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-// uncomment this macro to switch to standard memory management
-//#define USE_SYSTEM_MEMORY_MANAGEMENT 
-
-////////////////////////////////////////////////////////////////////////
-///                    STRUCTURE DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/*  
-    Here is an informal description of the FX data structure.
-    (1) The sparse matrix is filled with literals, associated with 
-        cubes (row) and variables (columns). The matrix contains 
-        all the cubes of all the nodes in the network.
-    (2) A cube is associated with 
-        (a) its literals in the matrix,
-        (b) the output variable of the node, to which this cube belongs,
-    (3) A variable is associated with 
-        (a) its literals in the matrix and
-        (b) the list of cube pairs in the cover, for which it is the output
-    (4) A cube pair is associated with two cubes and contains the counters
-        of literals in the base and in the cubes without the base
-    (5) A double-cube divisor is associated with list of all cube pairs 
-        that produce it and its current weight (which is updated automatically 
-        each time a new pair is added or an old pair is removed). 
-    (6) A single-cube divisor is associated the pair of variables. 
-*/
-
-// sparse matrix
-typedef struct FxuMatrix        Fxu_Matrix;     // the sparse matrix
-
-// sparse matrix contents: cubes (rows), vars (columns), literals (entries)
-typedef struct FxuCube          Fxu_Cube;       // one cube in the sparse matrix
-typedef struct FxuVar           Fxu_Var;        // one literal in the sparse matrix
-typedef struct FxuLit           Fxu_Lit;        // one entry in the sparse matrix
-
-// double cube divisors
-typedef struct FxuPair          Fxu_Pair;       // the pair of cubes
-typedef struct FxuDouble        Fxu_Double;     // the double-cube divisor
-typedef struct FxuSingle        Fxu_Single;     // the two-literal single-cube divisor
-
-// various lists
-typedef struct FxuListCube      Fxu_ListCube;   // the list of cubes
-typedef struct FxuListVar       Fxu_ListVar;    // the list of literals
-typedef struct FxuListLit       Fxu_ListLit;    // the list of entries
-typedef struct FxuListPair      Fxu_ListPair;   // the list of pairs
-typedef struct FxuListDouble    Fxu_ListDouble; // the list of divisors
-typedef struct FxuListSingle    Fxu_ListSingle; // the list of single-cube divisors
-
-// various heaps
-typedef struct FxuHeapDouble    Fxu_HeapDouble; // the heap of divisors
-typedef struct FxuHeapSingle    Fxu_HeapSingle; // the heap of variables
-
-
-// various lists
-
-// the list of cubes in the sparse matrix 
-struct FxuListCube
-{
-    Fxu_Cube *       pHead;
-    Fxu_Cube *       pTail;
-    int              nItems;
-};
-
-// the list of literals in the sparse matrix 
-struct FxuListVar
-{
-    Fxu_Var *        pHead;
-    Fxu_Var *        pTail;
-    int              nItems;
-};
-
-// the list of entries in the sparse matrix 
-struct FxuListLit
-{
-    Fxu_Lit *        pHead;
-    Fxu_Lit *        pTail;
-    int              nItems;
-};
-
-// the list of cube pair in the sparse matrix 
-struct FxuListPair
-{
-    Fxu_Pair *       pHead;
-    Fxu_Pair *       pTail;
-    int              nItems;
-};
-
-// the list of divisors in the sparse matrix 
-struct FxuListDouble
-{
-    Fxu_Double *     pHead;
-    Fxu_Double *     pTail;
-    int              nItems;
-};
-
-// the list of divisors in the sparse matrix 
-struct FxuListSingle
-{
-    Fxu_Single *     pHead;
-    Fxu_Single *     pTail;
-    int              nItems;
-};
-
-
-// various heaps
-
-// the heap of double cube divisors by weight
-struct FxuHeapDouble
-{
-    Fxu_Double **    pTree;
-    int              nItems;
-    int              nItemsAlloc;
-    int              i;
-};
-
-// the heap of variable by their occurrence in the cubes
-struct FxuHeapSingle
-{
-    Fxu_Single **    pTree;
-    int              nItems;
-    int              nItemsAlloc;
-    int              i;
-};
-
-
-
-// sparse matrix
-struct FxuMatrix // ~ 30 words
-{
-    // the cubes
-    Fxu_ListCube     lCubes;      // the double linked list of cubes
-    // the values (binary literals)
-    Fxu_ListVar      lVars;       // the double linked list of variables
-      Fxu_Var **       ppVars;      // the array of variables
-    // the double cube divisors
-    Fxu_ListDouble * pTable;      // the hash table of divisors
-    int              nTableSize;  // the hash table size
-    int              nDivs;       // the number of divisors in the table
-    int              nDivsTotal;  // the number of divisors in the table
-    Fxu_HeapDouble * pHeapDouble;    // the heap of divisors by weight
-    // the single cube divisors
-    Fxu_ListSingle   lSingles;    // the linked list of single cube divisors  
-    Fxu_HeapSingle * pHeapSingle; // the heap of variables by the number of literals in the matrix
-    int              nWeightLimit;// the limit on weight of single cube divisors collected
-    int              nSingleTotal;// the total number of single cube divisors
-    // storage for cube pairs
-    Fxu_Pair ***     pppPairs;
-    Fxu_Pair **      ppPairs;
-    // temporary storage for cubes 
-    Fxu_Cube *       pOrderCubes;
-    Fxu_Cube **      ppTailCubes;
-    // temporary storage for variables 
-    Fxu_Var *        pOrderVars;
-    Fxu_Var **       ppTailVars;
-    // temporary storage for pairs
-    Vec_Ptr_t *      vPairs;
-    // statistics
-    int              nEntries;    // the total number of entries in the sparse matrix
-    int              nDivs1;      // the single cube divisors taken
-    int              nDivs2;      // the double cube divisors taken
-    int              nDivs3;      // the double cube divisors with complement
-    // memory manager
-    Extra_MmFixed_t * pMemMan;     // the memory manager for all small sized entries
-};
-
-// the cube in the sparse matrix
-struct FxuCube // 9 words
-{
-    int              iCube;       // the number of this cube in the cover
-    Fxu_Cube *       pFirst;      // the pointer to the first cube of this cover
-    Fxu_Var *        pVar;        // the variable representing the output of the cover
-    Fxu_ListLit      lLits;       // the row in the table 
-    Fxu_Cube *       pPrev;       // the previous cube
-    Fxu_Cube *       pNext;       // the next cube
-    Fxu_Cube *       pOrder;      // the specialized linked list of cubes
-};
-
-// the variable in the sparse matrix
-struct FxuVar // 10 words
-{
-    int              iVar;        // the number of this variable
-    int              nCubes;      // the number of cubes assoc with this var
-    Fxu_Cube *       pFirst;      // the first cube assoc with this var
-    Fxu_Pair ***     ppPairs;     // the pairs of cubes assoc with this var
-    Fxu_ListLit      lLits;       // the column in the table 
-    Fxu_Var *        pPrev;       // the previous variable
-    Fxu_Var *        pNext;       // the next variable
-    Fxu_Var *        pOrder;      // the specialized linked list of variables
-};
-
-// the literal entry in the sparse matrix 
-struct FxuLit // 8 words
-{
-    int              iVar;        // the number of this variable
-    int              iCube;       // the number of this cube
-    Fxu_Cube *       pCube;       // the cube of this literal
-    Fxu_Var *        pVar;        // the variable of this literal
-    Fxu_Lit *        pHPrev;      // prev lit in the cube
-    Fxu_Lit *        pHNext;      // next lit in the cube
-    Fxu_Lit *        pVPrev;      // prev lit of the var     
-    Fxu_Lit *        pVNext;      // next lit of the var   
-};
-
-// the cube pair
-struct FxuPair // 10 words
-{
-    int              nLits1;      // the number of literals in the two cubes
-    int              nLits2;      // the number of literals in the two cubes
-    int              nBase;       // the number of literals in the base
-    Fxu_Double *     pDiv;        // the divisor of this pair
-    Fxu_Cube *       pCube1;      // the first cube of the pair
-    Fxu_Cube *       pCube2;      // the second cube of the pair
-    int              iCube1;      // the first cube of the pair
-    int              iCube2;      // the second cube of the pair
-    Fxu_Pair *       pDPrev;      // the previous pair in the divisor
-    Fxu_Pair *       pDNext;      // the next pair in the divisor
-};
-
-// the double cube divisor
-struct FxuDouble // 10 words
-{
-    int              Num;         // the unique number of this divisor
-    int              HNum;        // the heap number of this divisor
-    int              Weight;      // the weight of this divisor
-    unsigned         Key;         // the hash key of this divisor
-    Fxu_ListPair     lPairs;      // the pairs of cubes, which produce this divisor
-    Fxu_Double *     pPrev;       // the previous divisor in the table
-    Fxu_Double *     pNext;       // the next divisor in the table
-    Fxu_Double *     pOrder;      // the specialized linked list of divisors
-};
-
-// the single cube divisor
-struct FxuSingle // 7 words
-{
-    int              Num;         // the unique number of this divisor
-    int              HNum;        // the heap number of this divisor
-    int              Weight;      // the weight of this divisor
-    Fxu_Var *        pVar1;       // the first variable of the single-cube divisor
-    Fxu_Var *        pVar2;       // the second variable of the single-cube divisor
-    Fxu_Single *     pPrev;       // the previous divisor in the list
-    Fxu_Single *     pNext;       // the next divisor in the list
-};
-
-////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFINITIONS                          ///
-////////////////////////////////////////////////////////////////////////
-
-// minimum/maximum
-#define Fxu_Min( a, b ) ( ((a)<(b))? (a):(b) )
-#define Fxu_Max( a, b ) ( ((a)>(b))? (a):(b) )
-
-// selection of the minimum/maximum cube in the pair
-#define Fxu_PairMinCube( pPair )    (((pPair)->iCube1 < (pPair)->iCube2)? (pPair)->pCube1: (pPair)->pCube2)
-#define Fxu_PairMaxCube( pPair )    (((pPair)->iCube1 > (pPair)->iCube2)? (pPair)->pCube1: (pPair)->pCube2)
-#define Fxu_PairMinCubeInt( pPair ) (((pPair)->iCube1 < (pPair)->iCube2)? (pPair)->iCube1: (pPair)->iCube2)
-#define Fxu_PairMaxCubeInt( pPair ) (((pPair)->iCube1 > (pPair)->iCube2)? (pPair)->iCube1: (pPair)->iCube2)
-
-// iterators
-
-#define Fxu_MatrixForEachCube( Matrix, Cube )\
-    for ( Cube = (Matrix)->lCubes.pHead;\
-          Cube;\
-          Cube = Cube->pNext )
-#define Fxu_MatrixForEachCubeSafe( Matrix, Cube, Cube2 )\
-    for ( Cube = (Matrix)->lCubes.pHead, Cube2 = (Cube? Cube->pNext: NULL);\
-          Cube;\
-          Cube = Cube2, Cube2 = (Cube? Cube->pNext: NULL) )
-
-#define Fxu_MatrixForEachVariable( Matrix, Var )\
-    for ( Var = (Matrix)->lVars.pHead;\
-          Var;\
-          Var = Var->pNext )
-#define Fxu_MatrixForEachVariableSafe( Matrix, Var, Var2 )\
-    for ( Var = (Matrix)->lVars.pHead, Var2 = (Var? Var->pNext: NULL);\
-          Var;\
-          Var = Var2, Var2 = (Var? Var->pNext: NULL) )
-
-#define Fxu_MatrixForEachSingle( Matrix, Single )\
-    for ( Single = (Matrix)->lSingles.pHead;\
-          Single;\
-          Single = Single->pNext )
-#define Fxu_MatrixForEachSingleSafe( Matrix, Single, Single2 )\
-    for ( Single = (Matrix)->lSingles.pHead, Single2 = (Single? Single->pNext: NULL);\
-          Single;\
-          Single = Single2, Single2 = (Single? Single->pNext: NULL) )
-
-#define Fxu_TableForEachDouble( Matrix, Key, Div )\
-    for ( Div = (Matrix)->pTable[Key].pHead;\
-          Div;\
-          Div = Div->pNext )
-#define Fxu_TableForEachDoubleSafe( Matrix, Key, Div, Div2 )\
-    for ( Div = (Matrix)->pTable[Key].pHead, Div2 = (Div? Div->pNext: NULL);\
-          Div;\
-          Div = Div2, Div2 = (Div? Div->pNext: NULL) )
-
-#define Fxu_MatrixForEachDouble( Matrix, Div, Index )\
-    for ( Index = 0; Index < (Matrix)->nTableSize; Index++ )\
-        Fxu_TableForEachDouble( Matrix, Index, Div )
-#define Fxu_MatrixForEachDoubleSafe( Matrix, Div, Div2, Index )\
-    for ( Index = 0; Index < (Matrix)->nTableSize; Index++ )\
-        Fxu_TableForEachDoubleSafe( Matrix, Index, Div, Div2 )
-
-
-#define Fxu_CubeForEachLiteral( Cube, Lit )\
-    for ( Lit = (Cube)->lLits.pHead;\
-          Lit;\
-          Lit = Lit->pHNext )
-#define Fxu_CubeForEachLiteralSafe( Cube, Lit, Lit2 )\
-    for ( Lit = (Cube)->lLits.pHead, Lit2 = (Lit? Lit->pHNext: NULL);\
-          Lit;\
-          Lit = Lit2, Lit2 = (Lit? Lit->pHNext: NULL) )
-
-#define Fxu_VarForEachLiteral( Var, Lit )\
-    for ( Lit = (Var)->lLits.pHead;\
-          Lit;\
-          Lit = Lit->pVNext )
-
-#define Fxu_CubeForEachDivisor( Cube, Div )\
-    for ( Div = (Cube)->lDivs.pHead;\
-          Div;\
-          Div = Div->pCNext )
-
-#define Fxu_DoubleForEachPair( Div, Pair )\
-    for ( Pair = (Div)->lPairs.pHead;\
-          Pair;\
-          Pair = Pair->pDNext )
-#define Fxu_DoubleForEachPairSafe( Div, Pair, Pair2 )\
-    for ( Pair = (Div)->lPairs.pHead, Pair2 = (Pair? Pair->pDNext: NULL);\
-          Pair;\
-          Pair = Pair2, Pair2 = (Pair? Pair->pDNext: NULL) )
-
-
-// iterator through the cube pairs belonging to the given cube 
-#define Fxu_CubeForEachPair( pCube, pPair, i )\
-  for ( i = 0;\
-        i < pCube->pVar->nCubes &&\
-        (((unsigned)(pPair = pCube->pVar->ppPairs[pCube->iCube][i])) >= 0);\
-        i++ )\
-        if ( pPair )
-
-// iterator through all the items in the heap
-#define Fxu_HeapDoubleForEachItem( Heap, Div )\
-    for ( Heap->i = 1;\
-          Heap->i <= Heap->nItems && (Div = Heap->pTree[Heap->i]);\
-          Heap->i++ )
-#define Fxu_HeapSingleForEachItem( Heap, Single )\
-    for ( Heap->i = 1;\
-          Heap->i <= Heap->nItems && (Single = Heap->pTree[Heap->i]);\
-          Heap->i++ )
-
-// starting the rings
-#define Fxu_MatrixRingCubesStart( Matrix )    (((Matrix)->ppTailCubes = &((Matrix)->pOrderCubes)), ((Matrix)->pOrderCubes = NULL))
-#define Fxu_MatrixRingVarsStart(  Matrix )    (((Matrix)->ppTailVars  = &((Matrix)->pOrderVars)),  ((Matrix)->pOrderVars  = NULL))
-// stopping the rings
-#define Fxu_MatrixRingCubesStop(  Matrix )
-#define Fxu_MatrixRingVarsStop(   Matrix )
-// resetting the rings
-#define Fxu_MatrixRingCubesReset( Matrix )    (((Matrix)->pOrderCubes = NULL), ((Matrix)->ppTailCubes = NULL))
-#define Fxu_MatrixRingVarsReset(  Matrix )    (((Matrix)->pOrderVars  = NULL), ((Matrix)->ppTailVars  = NULL))
-// adding to the rings
-#define Fxu_MatrixRingCubesAdd( Matrix, Cube) ((*((Matrix)->ppTailCubes) = Cube), ((Matrix)->ppTailCubes = &(Cube)->pOrder), ((Cube)->pOrder = (Fxu_Cube *)1))
-#define Fxu_MatrixRingVarsAdd(  Matrix, Var ) ((*((Matrix)->ppTailVars ) = Var ), ((Matrix)->ppTailVars  = &(Var)->pOrder ), ((Var)->pOrder  = (Fxu_Var *)1))
-// iterating through the rings
-#define Fxu_MatrixForEachCubeInRing( Matrix, Cube )\
-    if ( (Matrix)->pOrderCubes )\
-    for ( Cube = (Matrix)->pOrderCubes;\
-          Cube != (Fxu_Cube *)1;\
-          Cube = Cube->pOrder )
-#define Fxu_MatrixForEachCubeInRingSafe( Matrix, Cube, Cube2 )\
-    if ( (Matrix)->pOrderCubes )\
-    for ( Cube = (Matrix)->pOrderCubes, Cube2 = ((Cube != (Fxu_Cube *)1)? Cube->pOrder: (Fxu_Cube *)1);\
-          Cube != (Fxu_Cube *)1;\
-          Cube = Cube2, Cube2 = ((Cube != (Fxu_Cube *)1)? Cube->pOrder: (Fxu_Cube *)1) )
-#define Fxu_MatrixForEachVarInRing( Matrix, Var )\
-    if ( (Matrix)->pOrderVars )\
-    for ( Var = (Matrix)->pOrderVars;\
-          Var != (Fxu_Var *)1;\
-          Var = Var->pOrder )
-#define Fxu_MatrixForEachVarInRingSafe( Matrix, Var, Var2 )\
-    if ( (Matrix)->pOrderVars )\
-    for ( Var = (Matrix)->pOrderVars, Var2 = ((Var != (Fxu_Var *)1)? Var->pOrder: (Fxu_Var *)1);\
-          Var != (Fxu_Var *)1;\
-          Var = Var2, Var2 = ((Var != (Fxu_Var *)1)? Var->pOrder: (Fxu_Var *)1) )
-// the procedures are related to the above macros
-extern void Fxu_MatrixRingCubesUnmark( Fxu_Matrix * p );
-extern void Fxu_MatrixRingVarsUnmark( Fxu_Matrix * p );
-
-
-// macros working with memory
-// MEM_ALLOC: allocate the given number (Size) of items of type (Type)
-// MEM_FREE:  deallocate the pointer (Pointer) to the given number (Size) of items of type (Type)
-#ifdef USE_SYSTEM_MEMORY_MANAGEMENT
-#define MEM_ALLOC_FXU( Manager, Type, Size )          ((Type *)malloc( (Size) * sizeof(Type) ))
-#define MEM_FREE_FXU( Manager, Type, Size, Pointer )  if ( Pointer ) { free(Pointer); Pointer = NULL; }
-#else
-#define MEM_ALLOC_FXU( Manager, Type, Size )\
-        ((Type *)Fxu_MemFetch( Manager, (Size) * sizeof(Type) ))
-#define MEM_FREE_FXU( Manager, Type, Size, Pointer )\
-         if ( Pointer ) { Fxu_MemRecycle( Manager, (char *)(Pointer), (Size) * sizeof(Type) ); Pointer = NULL; }
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/*===== fxu.c ====================================================*/
-extern char *       Fxu_MemFetch( Fxu_Matrix * p, int nBytes );
-extern void         Fxu_MemRecycle( Fxu_Matrix * p, char * pItem, int nBytes );
-/*===== fxuCreate.c ====================================================*/
-/*===== fxuReduce.c ====================================================*/
-/*===== fxuPrint.c ====================================================*/
-extern void         Fxu_MatrixPrint( FILE * pFile, Fxu_Matrix * p );
-extern void         Fxu_MatrixPrintDivisorProfile( FILE * pFile, Fxu_Matrix * p );
-/*===== fxuSelect.c ====================================================*/
-extern int          Fxu_Select( Fxu_Matrix * p, Fxu_Single ** ppSingle, Fxu_Double ** ppDouble );
-extern int          Fxu_SelectSCD( Fxu_Matrix * p, int Weight, Fxu_Var ** ppVar1, Fxu_Var ** ppVar2 );
-/*===== fxuUpdate.c ====================================================*/
-extern void         Fxu_Update( Fxu_Matrix * p, Fxu_Single * pSingle, Fxu_Double * pDouble );
-extern void         Fxu_UpdateDouble( Fxu_Matrix * p );
-extern void         Fxu_UpdateSingle( Fxu_Matrix * p );
-/*===== fxuPair.c ====================================================*/
-extern void         Fxu_PairCanonicize( Fxu_Cube ** ppCube1, Fxu_Cube ** ppCube2 );
-extern unsigned     Fxu_PairHashKeyArray( Fxu_Matrix * p, int piVarsC1[], int piVarsC2[], int nVarsC1, int nVarsC2 );
-extern unsigned     Fxu_PairHashKey( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2, int * pnBase, int * pnLits1, int * pnLits2 );
-extern unsigned     Fxu_PairHashKeyMv( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2, int * pnBase, int * pnLits1, int * pnLits2 );
-extern int          Fxu_PairCompare( Fxu_Pair * pPair1, Fxu_Pair * pPair2 );
-extern void         Fxu_PairAllocStorage( Fxu_Var * pVar, int nCubes );
-extern void         Fxu_PairFreeStorage( Fxu_Var * pVar );
-extern void         Fxu_PairClearStorage( Fxu_Cube * pCube );
-extern Fxu_Pair *   Fxu_PairAlloc( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2 );
-extern void         Fxu_PairAdd( Fxu_Pair * pPair );
-/*===== fxuSingle.c ====================================================*/
-extern void         Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax );
-extern void         Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar );
-extern int          Fxu_SingleCountCoincidence( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVar2 );
-/*===== fxuMatrix.c ====================================================*/
-// matrix
-extern Fxu_Matrix * Fxu_MatrixAllocate();
-extern void         Fxu_MatrixDelete( Fxu_Matrix * p );
-// double-cube divisor
-extern void         Fxu_MatrixAddDivisor( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2 );
-extern void         Fxu_MatrixDelDivisor( Fxu_Matrix * p, Fxu_Double * pDiv );
-// single-cube divisor
-extern void          Fxu_MatrixAddSingle( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVar2, int Weight );
-// variable
-extern Fxu_Var *    Fxu_MatrixAddVar( Fxu_Matrix * p );
-// cube
-extern Fxu_Cube *   Fxu_MatrixAddCube( Fxu_Matrix * p, Fxu_Var * pVar, int iCube );
-// literal
-extern void         Fxu_MatrixAddLiteral( Fxu_Matrix * p, Fxu_Cube * pCube, Fxu_Var * pVar );
-extern void         Fxu_MatrixDelLiteral( Fxu_Matrix * p, Fxu_Lit * pLit );
-/*===== fxuList.c ====================================================*/
-// matrix -> variable 
-extern void         Fxu_ListMatrixAddVariable( Fxu_Matrix * p, Fxu_Var * pVar );
-extern void         Fxu_ListMatrixDelVariable( Fxu_Matrix * p, Fxu_Var * pVar );
-// matrix -> cube
-extern void         Fxu_ListMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube );
-extern void         Fxu_ListMatrixDelCube( Fxu_Matrix * p, Fxu_Cube * pCube );
-// matrix -> single
-extern void         Fxu_ListMatrixAddSingle( Fxu_Matrix * p, Fxu_Single * pSingle );
-extern void         Fxu_ListMatrixDelSingle( Fxu_Matrix * p, Fxu_Single * pSingle );
-// table -> divisor
-extern void         Fxu_ListTableAddDivisor( Fxu_Matrix * p, Fxu_Double * pDiv );
-extern void         Fxu_ListTableDelDivisor( Fxu_Matrix * p, Fxu_Double * pDiv );
-// cube -> literal 
-extern void         Fxu_ListCubeAddLiteral( Fxu_Cube * pCube, Fxu_Lit * pLit );
-extern void         Fxu_ListCubeDelLiteral( Fxu_Cube * pCube, Fxu_Lit * pLit );
-// var -> literal
-extern void         Fxu_ListVarAddLiteral( Fxu_Var * pVar, Fxu_Lit * pLit );
-extern void         Fxu_ListVarDelLiteral( Fxu_Var * pVar, Fxu_Lit * pLit );
-// divisor -> pair
-extern void         Fxu_ListDoubleAddPairLast( Fxu_Double * pDiv, Fxu_Pair * pLink );
-extern void         Fxu_ListDoubleAddPairFirst( Fxu_Double * pDiv, Fxu_Pair * pLink );
-extern void         Fxu_ListDoubleAddPairMiddle( Fxu_Double * pDiv, Fxu_Pair * pSpot, Fxu_Pair * pLink );
-extern void         Fxu_ListDoubleDelPair( Fxu_Double * pDiv, Fxu_Pair * pPair );
-/*===== fxuHeapDouble.c ====================================================*/
-extern Fxu_HeapDouble * Fxu_HeapDoubleStart();
-extern void         Fxu_HeapDoubleStop( Fxu_HeapDouble * p );
-extern void         Fxu_HeapDoublePrint( FILE * pFile, Fxu_HeapDouble * p );
-extern void         Fxu_HeapDoubleCheck( Fxu_HeapDouble * p );
-extern void         Fxu_HeapDoubleCheckOne( Fxu_HeapDouble * p, Fxu_Double * pDiv );
-
-extern void         Fxu_HeapDoubleInsert( Fxu_HeapDouble * p, Fxu_Double * pDiv );  
-extern void         Fxu_HeapDoubleUpdate( Fxu_HeapDouble * p, Fxu_Double * pDiv );  
-extern void         Fxu_HeapDoubleDelete( Fxu_HeapDouble * p, Fxu_Double * pDiv );  
-extern int          Fxu_HeapDoubleReadMaxWeight( Fxu_HeapDouble * p );  
-extern Fxu_Double * Fxu_HeapDoubleReadMax( Fxu_HeapDouble * p );  
-extern Fxu_Double * Fxu_HeapDoubleGetMax( Fxu_HeapDouble * p );  
-/*===== fxuHeapSingle.c ====================================================*/
-extern Fxu_HeapSingle * Fxu_HeapSingleStart();
-extern void         Fxu_HeapSingleStop( Fxu_HeapSingle * p );
-extern void         Fxu_HeapSinglePrint( FILE * pFile, Fxu_HeapSingle * p );
-extern void         Fxu_HeapSingleCheck( Fxu_HeapSingle * p );
-extern void         Fxu_HeapSingleCheckOne( Fxu_HeapSingle * p, Fxu_Single * pSingle );
-
-extern void         Fxu_HeapSingleInsert( Fxu_HeapSingle * p, Fxu_Single * pSingle );  
-extern void         Fxu_HeapSingleUpdate( Fxu_HeapSingle * p, Fxu_Single * pSingle );  
-extern void         Fxu_HeapSingleDelete( Fxu_HeapSingle * p, Fxu_Single * pSingle );  
-extern int          Fxu_HeapSingleReadMaxWeight( Fxu_HeapSingle * p );  
-extern Fxu_Single * Fxu_HeapSingleReadMax( Fxu_HeapSingle * p );
-extern Fxu_Single * Fxu_HeapSingleGetMax( Fxu_HeapSingle * p );  
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                         END OF FILE                              ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/opt/fxu/fxuList.c b/src/opt/fxu/fxuList.c
deleted file mode 100644
index 52995804..00000000
--- a/src/opt/fxu/fxuList.c
+++ /dev/null
@@ -1,522 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fxuList.c]
-
-  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
-
-  Synopsis    [Operations on lists.]
-
-  Author      [MVSIS Group]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - February 1, 2003.]
-
-  Revision    [$Id: fxuList.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fxuInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-// matrix -> var
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_ListMatrixAddVariable( Fxu_Matrix * p, Fxu_Var * pLink ) 
-{
-    Fxu_ListVar * pList = &p->lVars;
-    if ( pList->pHead == NULL )
-    {
-        pList->pHead = pLink;
-        pList->pTail = pLink;
-        pLink->pPrev = NULL;
-        pLink->pNext = NULL;
-    }
-    else
-    {
-        pLink->pNext = NULL;
-        pList->pTail->pNext = pLink;
-        pLink->pPrev = pList->pTail;
-        pList->pTail = pLink;
-    }
-    pList->nItems++;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_ListMatrixDelVariable( Fxu_Matrix * p, Fxu_Var * pLink )
-{
-    Fxu_ListVar * pList = &p->lVars;
-    if ( pList->pHead == pLink )
-         pList->pHead = pLink->pNext;
-    if ( pList->pTail == pLink )
-         pList->pTail = pLink->pPrev;
-    if ( pLink->pPrev )
-         pLink->pPrev->pNext = pLink->pNext;
-    if ( pLink->pNext )
-         pLink->pNext->pPrev = pLink->pPrev;
-    pList->nItems--;
-}
-
-
-// matrix -> cube
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_ListMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pLink )
-{
-    Fxu_ListCube * pList = &p->lCubes;
-    if ( pList->pHead == NULL )
-    {
-        pList->pHead = pLink;
-        pList->pTail = pLink;
-        pLink->pPrev = NULL;
-        pLink->pNext = NULL;
-    }
-    else
-    {
-        pLink->pNext = NULL;
-        pList->pTail->pNext = pLink;
-        pLink->pPrev = pList->pTail;
-        pList->pTail = pLink;
-    }
-    pList->nItems++;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_ListMatrixDelCube( Fxu_Matrix * p, Fxu_Cube * pLink )
-{
-    Fxu_ListCube * pList = &p->lCubes;
-    if ( pList->pHead == pLink )
-         pList->pHead = pLink->pNext;
-    if ( pList->pTail == pLink )
-         pList->pTail = pLink->pPrev;
-    if ( pLink->pPrev )
-         pLink->pPrev->pNext = pLink->pNext;
-    if ( pLink->pNext )
-         pLink->pNext->pPrev = pLink->pPrev;
-    pList->nItems--;
-}
-
-
-// matrix -> single
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_ListMatrixAddSingle( Fxu_Matrix * p, Fxu_Single * pLink )
-{
-    Fxu_ListSingle * pList = &p->lSingles;
-    if ( pList->pHead == NULL )
-    {
-        pList->pHead = pLink;
-        pList->pTail = pLink;
-        pLink->pPrev = NULL;
-        pLink->pNext = NULL;
-    }
-    else
-    {
-        pLink->pNext = NULL;
-        pList->pTail->pNext = pLink;
-        pLink->pPrev = pList->pTail;
-        pList->pTail = pLink;
-    }
-    pList->nItems++;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_ListMatrixDelSingle( Fxu_Matrix * p, Fxu_Single * pLink )
-{
-    Fxu_ListSingle * pList = &p->lSingles;
-    if ( pList->pHead == pLink )
-         pList->pHead = pLink->pNext;
-    if ( pList->pTail == pLink )
-         pList->pTail = pLink->pPrev;
-    if ( pLink->pPrev )
-         pLink->pPrev->pNext = pLink->pNext;
-    if ( pLink->pNext )
-         pLink->pNext->pPrev = pLink->pPrev;
-    pList->nItems--;
-}
-
-
-// table -> divisor
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_ListTableAddDivisor( Fxu_Matrix * p, Fxu_Double * pLink ) 
-{
-    Fxu_ListDouble * pList = &(p->pTable[pLink->Key]);
-    if ( pList->pHead == NULL )
-    {
-        pList->pHead = pLink;
-        pList->pTail = pLink;
-        pLink->pPrev = NULL;
-        pLink->pNext = NULL;
-    }
-    else
-    {
-        pLink->pNext = NULL;
-        pList->pTail->pNext = pLink;
-        pLink->pPrev = pList->pTail;
-        pList->pTail = pLink;
-    }
-    pList->nItems++;
-    p->nDivs++;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_ListTableDelDivisor( Fxu_Matrix * p, Fxu_Double * pLink ) 
-{
-    Fxu_ListDouble * pList = &(p->pTable[pLink->Key]);
-    if ( pList->pHead == pLink )
-         pList->pHead = pLink->pNext;
-    if ( pList->pTail == pLink )
-         pList->pTail = pLink->pPrev;
-    if ( pLink->pPrev )
-         pLink->pPrev->pNext = pLink->pNext;
-    if ( pLink->pNext )
-         pLink->pNext->pPrev = pLink->pPrev;
-    pList->nItems--;
-    p->nDivs--;
-}
-
-
-// cube -> literal 
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_ListCubeAddLiteral( Fxu_Cube * pCube, Fxu_Lit * pLink )
-{
-    Fxu_ListLit * pList = &(pCube->lLits);
-    if ( pList->pHead == NULL )
-    {
-        pList->pHead = pLink;
-        pList->pTail = pLink;
-        pLink->pHPrev = NULL;
-        pLink->pHNext = NULL;
-    }
-    else
-    {
-        pLink->pHNext = NULL;
-        pList->pTail->pHNext = pLink;
-        pLink->pHPrev = pList->pTail;
-        pList->pTail = pLink;
-    }
-    pList->nItems++;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_ListCubeDelLiteral( Fxu_Cube * pCube, Fxu_Lit * pLink )
-{
-    Fxu_ListLit * pList = &(pCube->lLits);
-    if ( pList->pHead == pLink )
-         pList->pHead = pLink->pHNext;
-    if ( pList->pTail == pLink )
-         pList->pTail = pLink->pHPrev;
-    if ( pLink->pHPrev )
-         pLink->pHPrev->pHNext = pLink->pHNext;
-    if ( pLink->pHNext )
-         pLink->pHNext->pHPrev = pLink->pHPrev;
-    pList->nItems--;
-}
-
-
-// var -> literal
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_ListVarAddLiteral( Fxu_Var * pVar, Fxu_Lit * pLink )
-{
-    Fxu_ListLit * pList = &(pVar->lLits);
-    if ( pList->pHead == NULL )
-    {
-        pList->pHead = pLink;
-        pList->pTail = pLink;
-        pLink->pVPrev = NULL;
-        pLink->pVNext = NULL;
-    }
-    else
-    {
-        pLink->pVNext = NULL;
-        pList->pTail->pVNext = pLink;
-        pLink->pVPrev = pList->pTail;
-        pList->pTail = pLink;
-    }
-    pList->nItems++;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_ListVarDelLiteral( Fxu_Var * pVar, Fxu_Lit * pLink )
-{
-    Fxu_ListLit * pList = &(pVar->lLits);
-    if ( pList->pHead == pLink )
-         pList->pHead = pLink->pVNext;
-    if ( pList->pTail == pLink )
-         pList->pTail = pLink->pVPrev;
-    if ( pLink->pVPrev )
-         pLink->pVPrev->pVNext = pLink->pVNext;
-    if ( pLink->pVNext )
-         pLink->pVNext->pVPrev = pLink->pVPrev;
-    pList->nItems--;
-}
-
-
-
-// divisor -> pair
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_ListDoubleAddPairLast( Fxu_Double * pDiv, Fxu_Pair * pLink )
-{
-    Fxu_ListPair * pList = &pDiv->lPairs;
-    if ( pList->pHead == NULL )
-    {
-        pList->pHead = pLink;
-        pList->pTail = pLink;
-        pLink->pDPrev = NULL;
-        pLink->pDNext = NULL;
-    }
-    else
-    {
-        pLink->pDNext = NULL;
-        pList->pTail->pDNext = pLink;
-        pLink->pDPrev = pList->pTail;
-        pList->pTail = pLink;
-    }
-    pList->nItems++;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_ListDoubleAddPairFirst( Fxu_Double * pDiv, Fxu_Pair * pLink )
-{
-    Fxu_ListPair * pList = &pDiv->lPairs;
-    if ( pList->pHead == NULL )
-    {
-        pList->pHead = pLink;
-        pList->pTail = pLink;
-        pLink->pDPrev = NULL;
-        pLink->pDNext = NULL;
-    }
-    else
-    {
-        pLink->pDPrev = NULL;
-        pList->pHead->pDPrev = pLink;
-        pLink->pDNext = pList->pHead;
-        pList->pHead = pLink;
-    }
-    pList->nItems++;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds the entry in the middle of the list after the spot.]
-
-  Description [Assumes that spot points to the link, after which the given
-  link should be added. Spot cannot be NULL or the tail of the list.
-  Therefore, the head and the tail of the list are not changed.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_ListDoubleAddPairMiddle( Fxu_Double * pDiv, Fxu_Pair * pSpot, Fxu_Pair * pLink )
-{
-    Fxu_ListPair * pList = &pDiv->lPairs;
-    assert( pSpot );
-    assert( pSpot != pList->pTail );
-    pLink->pDPrev = pSpot;
-    pLink->pDNext = pSpot->pDNext;
-    pLink->pDPrev->pDNext = pLink;
-    pLink->pDNext->pDPrev = pLink;
-    pList->nItems++;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_ListDoubleDelPair( Fxu_Double * pDiv, Fxu_Pair * pLink )
-{
-    Fxu_ListPair * pList = &pDiv->lPairs;
-    if ( pList->pHead == pLink )
-         pList->pHead = pLink->pDNext;
-    if ( pList->pTail == pLink )
-         pList->pTail = pLink->pDPrev;
-    if ( pLink->pDPrev )
-         pLink->pDPrev->pDNext = pLink->pDNext;
-    if ( pLink->pDNext )
-         pLink->pDNext->pDPrev = pLink->pDPrev;
-    pList->nItems--;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_ListDoubleAddPairPlace( Fxu_Double * pDiv, Fxu_Pair * pPair, Fxu_Pair * pPairSpot )
-{
-    printf( "Fxu_ListDoubleAddPairPlace() is called!\n" );
-}
-
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/fxu/fxuMatrix.c b/src/opt/fxu/fxuMatrix.c
deleted file mode 100644
index 93ec7b90..00000000
--- a/src/opt/fxu/fxuMatrix.c
+++ /dev/null
@@ -1,374 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fxuMatrix.c]
-
-  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
-
-  Synopsis    [Procedures to manipulate the sparse matrix.]
-
-  Author      [MVSIS Group]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - February 1, 2003.]
-
-  Revision    [$Id: fxuMatrix.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fxuInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-extern unsigned int Cudd_Prime( unsigned int p );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fxu_Matrix * Fxu_MatrixAllocate()
-{
-    Fxu_Matrix * p;
-    p = ALLOC( Fxu_Matrix, 1 );
-    memset( p, 0, sizeof(Fxu_Matrix) );
-    p->nTableSize = Cudd_Prime(10000);
-    p->pTable = ALLOC( Fxu_ListDouble, p->nTableSize );
-    memset( p->pTable, 0, sizeof(Fxu_ListDouble) * p->nTableSize );
-#ifndef USE_SYSTEM_MEMORY_MANAGEMENT
-    {
-        // get the largest size in bytes for the following structures:
-        // Fxu_Cube, Fxu_Var, Fxu_Lit, Fxu_Pair, Fxu_Double, Fxu_Single
-        // (currently, Fxu_Var, Fxu_Pair, Fxu_Double take 10 machine words)
-        int nSizeMax, nSizeCur;
-        nSizeMax = -1;
-        nSizeCur = sizeof(Fxu_Cube);
-        if ( nSizeMax < nSizeCur )
-             nSizeMax = nSizeCur;
-        nSizeCur = sizeof(Fxu_Var);
-        if ( nSizeMax < nSizeCur )
-             nSizeMax = nSizeCur;
-        nSizeCur = sizeof(Fxu_Lit);
-        if ( nSizeMax < nSizeCur )
-             nSizeMax = nSizeCur;
-        nSizeCur = sizeof(Fxu_Pair);
-        if ( nSizeMax < nSizeCur )
-             nSizeMax = nSizeCur;
-        nSizeCur = sizeof(Fxu_Double);
-        if ( nSizeMax < nSizeCur )
-             nSizeMax = nSizeCur;
-        nSizeCur = sizeof(Fxu_Single);
-        if ( nSizeMax < nSizeCur )
-             nSizeMax = nSizeCur;
-        p->pMemMan  = Extra_MmFixedStart( nSizeMax ); 
-    }
-#endif
-    p->pHeapDouble = Fxu_HeapDoubleStart();
-    p->pHeapSingle = Fxu_HeapSingleStart();
-    p->vPairs = Vec_PtrAlloc( 100 );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_MatrixDelete( Fxu_Matrix * p )
-{
-    Fxu_HeapDoubleCheck( p->pHeapDouble );
-    Fxu_HeapDoubleStop( p->pHeapDouble );
-    Fxu_HeapSingleStop( p->pHeapSingle );
-
-    // delete other things
-#ifdef USE_SYSTEM_MEMORY_MANAGEMENT
-    // this code is not needed when the custom memory manager is used
-    {
-        Fxu_Cube * pCube, * pCube2;
-        Fxu_Var * pVar, * pVar2;
-        Fxu_Lit * pLit, * pLit2;
-        Fxu_Double * pDiv, * pDiv2;
-        Fxu_Single * pSingle, * pSingle2;
-        Fxu_Pair * pPair, * pPair2;
-        int i;
-        // delete the divisors
-        Fxu_MatrixForEachDoubleSafe( p, pDiv, pDiv2, i )
-        {
-            Fxu_DoubleForEachPairSafe( pDiv, pPair, pPair2 )
-                MEM_FREE_FXU( p, Fxu_Pair, 1, pPair );
-               MEM_FREE_FXU( p, Fxu_Double, 1, pDiv );
-        }
-        Fxu_MatrixForEachSingleSafe( p, pSingle, pSingle2 )
-               MEM_FREE_FXU( p, Fxu_Single, 1, pSingle );
-        // delete the entries
-        Fxu_MatrixForEachCube( p, pCube )
-            Fxu_CubeForEachLiteralSafe( pCube, pLit, pLit2 )
-                MEM_FREE_FXU( p, Fxu_Lit, 1, pLit );
-        // delete the cubes
-        Fxu_MatrixForEachCubeSafe( p, pCube, pCube2 )
-            MEM_FREE_FXU( p, Fxu_Cube, 1, pCube );
-        // delete the vars
-        Fxu_MatrixForEachVariableSafe( p, pVar, pVar2 )
-            MEM_FREE_FXU( p, Fxu_Var, 1, pVar );
-    }
-#else
-    Extra_MmFixedStop( p->pMemMan );
-#endif
-
-    Vec_PtrFree( p->vPairs );
-    FREE( p->pppPairs );
-    FREE( p->ppPairs );
-//    FREE( p->pPairsTemp );
-    FREE( p->pTable );
-    FREE( p->ppVars );
-    FREE( p );
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Adds a variable to the matrix.]
-
-  Description [This procedure always adds variables at the end of the matrix.
-  It assigns the var's node and number. It adds the var to the linked list of
-  all variables and to the table of all nodes.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fxu_Var * Fxu_MatrixAddVar( Fxu_Matrix * p )
-{
-    Fxu_Var * pVar;
-    pVar = MEM_ALLOC_FXU( p, Fxu_Var, 1 );
-    memset( pVar, 0, sizeof(Fxu_Var) );
-    pVar->iVar = p->lVars.nItems;
-    p->ppVars[pVar->iVar] = pVar;
-    Fxu_ListMatrixAddVariable( p, pVar );
-    return pVar;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds a literal to the matrix.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fxu_Cube * Fxu_MatrixAddCube( Fxu_Matrix * p, Fxu_Var * pVar, int iCube )
-{
-    Fxu_Cube * pCube;
-    pCube = MEM_ALLOC_FXU( p, Fxu_Cube, 1 );
-    memset( pCube, 0, sizeof(Fxu_Cube) );
-    pCube->pVar  = pVar;
-    pCube->iCube = iCube;
-    Fxu_ListMatrixAddCube( p, pCube );
-    return pCube;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds a literal to the matrix.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_MatrixAddLiteral( Fxu_Matrix * p, Fxu_Cube * pCube, Fxu_Var * pVar )
-{
-    Fxu_Lit * pLit;
-    pLit = MEM_ALLOC_FXU( p, Fxu_Lit, 1 );
-    memset( pLit, 0, sizeof(Fxu_Lit) );
-    // insert the literal into two linked lists
-    Fxu_ListCubeAddLiteral( pCube, pLit );
-    Fxu_ListVarAddLiteral( pVar, pLit );
-    // set the back pointers
-    pLit->pCube = pCube;
-    pLit->pVar  = pVar;
-    pLit->iCube = pCube->iCube;
-    pLit->iVar  = pVar->iVar;
-    // increment the literal counter
-    p->nEntries++;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deletes the divisor from the matrix.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_MatrixDelDivisor( Fxu_Matrix * p, Fxu_Double * pDiv )
-{
-    // delete divisor from the table
-    Fxu_ListTableDelDivisor( p, pDiv );
-    // recycle the divisor
-    MEM_FREE_FXU( p, Fxu_Double, 1, pDiv );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deletes the literal fromthe matrix.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_MatrixDelLiteral( Fxu_Matrix * p, Fxu_Lit * pLit )
-{
-    // delete the literal
-    Fxu_ListCubeDelLiteral( pLit->pCube, pLit );
-    Fxu_ListVarDelLiteral( pLit->pVar, pLit );
-    MEM_FREE_FXU( p, Fxu_Lit, 1, pLit );
-    // increment the literal counter
-    p->nEntries--;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Creates and adds a single cube divisor.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_MatrixAddSingle( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVar2, int Weight )
-{
-    Fxu_Single * pSingle;
-    assert( pVar1->iVar < pVar2->iVar );
-    pSingle = MEM_ALLOC_FXU( p, Fxu_Single, 1 );
-    memset( pSingle, 0, sizeof(Fxu_Single) );
-    pSingle->Num = p->lSingles.nItems;
-    pSingle->Weight = Weight;
-    pSingle->HNum = 0;
-    pSingle->pVar1 = pVar1;
-    pSingle->pVar2 = pVar2;
-    Fxu_ListMatrixAddSingle( p, pSingle );
-    // add to the heap
-    Fxu_HeapSingleInsert( p->pHeapSingle, pSingle );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_MatrixAddDivisor( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2 )
-{
-    Fxu_Pair * pPair;
-    Fxu_Double * pDiv;
-    int nBase, nLits1, nLits2;
-    int fFound;
-    unsigned Key;
-
-    // canonicize the pair
-    Fxu_PairCanonicize( &pCube1, &pCube2 );
-    // compute the hash key
-    Key = Fxu_PairHashKey( p, pCube1, pCube2, &nBase, &nLits1, &nLits2 );
-
-    // create the cube pair
-    pPair = Fxu_PairAlloc( p, pCube1, pCube2 );
-    pPair->nBase  = nBase;
-    pPair->nLits1 = nLits1;
-    pPair->nLits2 = nLits2;
-
-    // check if the divisor for this pair already exists
-    fFound = 0;
-    Key %= p->nTableSize;
-    Fxu_TableForEachDouble( p, Key, pDiv )
-    {
-        if ( Fxu_PairCompare( pPair, pDiv->lPairs.pTail ) ) // they are equal
-        {
-            fFound = 1;
-            break;
-        }
-    }
-
-    if ( !fFound )
-    {   // create the new divisor
-        pDiv = MEM_ALLOC_FXU( p, Fxu_Double, 1 );
-        memset( pDiv, 0, sizeof(Fxu_Double) );
-        pDiv->Key = Key;
-        // set the number of this divisor
-        pDiv->Num = p->nDivsTotal++; // p->nDivs;
-        // insert the divisor in the table
-        Fxu_ListTableAddDivisor( p, pDiv );
-        // set the initial cost of the divisor
-        pDiv->Weight -= pPair->nLits1 + pPair->nLits2;
-    }
-
-    // link the pair to the cubes
-    Fxu_PairAdd( pPair );
-    // connect the pair and the divisor
-    pPair->pDiv = pDiv;
-    Fxu_ListDoubleAddPairLast( pDiv, pPair );    
-    // update the max number of pairs in a divisor
-//    if ( p->nPairsMax < pDiv->lPairs.nItems )
-//        p->nPairsMax = pDiv->lPairs.nItems;
-    // update the divisor's weight
-    pDiv->Weight += pPair->nLits1 + pPair->nLits2 - 1 + pPair->nBase;
-    if ( fFound ) // update the divisor in the heap
-        Fxu_HeapDoubleUpdate( p->pHeapDouble, pDiv );
-    else  // add the new divisor to the heap
-        Fxu_HeapDoubleInsert( p->pHeapDouble, pDiv );
-}
-
-/*
-    {
-        int piVarsC1[100], piVarsC2[100], nVarsC1, nVarsC2;
-        Fxu_Double * pDivCur;
-        Fxu_MatrixGetDoubleVars( p, pDiv, piVarsC1, piVarsC2, &nVarsC1, &nVarsC2 );
-        pDivCur = Fxu_MatrixFindDouble( p, piVarsC1, piVarsC2, nVarsC1, nVarsC2 );
-        assert( pDivCur == pDiv );
-    }
-*/
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/fxu/fxuPair.c b/src/opt/fxu/fxuPair.c
deleted file mode 100644
index 3c031ce8..00000000
--- a/src/opt/fxu/fxuPair.c
+++ /dev/null
@@ -1,555 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fxuPair.c]
-
-  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
-
-  Synopsis    [Operations on cube pairs.]
-
-  Author      [MVSIS Group]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - February 1, 2003.]
-
-  Revision    [$Id: fxuPair.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fxuInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-#define MAX_PRIMES      304
-
-static s_Primes[MAX_PRIMES] =
-{
-    2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 
-    41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 
-    97, 101, 103, 107, 109, 113, 127, 131, 137, 139, 149, 151, 
-    157, 163, 167, 173, 179, 181, 191, 193, 197, 199, 211, 223, 
-    227, 229, 233, 239, 241, 251, 257, 263, 269, 271, 277, 281, 
-    283, 293, 307, 311, 313, 317, 331, 337, 347, 349, 353, 359, 
-    367, 373, 379, 383, 389, 397, 401, 409, 419, 421, 431, 433, 
-    439, 443, 449, 457, 461, 463, 467, 479, 487, 491, 499, 503, 
-    509, 521, 523, 541, 547, 557, 563, 569, 571, 577, 587, 593, 
-    599, 601, 607, 613, 617, 619, 631, 641, 643, 647, 653, 659, 
-    661, 673, 677, 683, 691, 701, 709, 719, 727, 733, 739, 743, 
-    751, 757, 761, 769, 773, 787, 797, 809, 811, 821, 823, 827, 
-    829, 839, 853, 857, 859, 863, 877, 881, 883, 887, 907, 911, 
-    919, 929, 937, 941, 947, 953, 967, 971, 977, 983, 991, 997, 
-    1009, 1013, 1019, 1021, 1031, 1033, 1039, 1049, 1051, 1061, 1063, 1069, 
-    1087, 1091, 1093, 1097, 1103, 1109, 1117, 1123, 1129, 1151, 1153, 1163, 
-    1171, 1181, 1187, 1193, 1201, 1213, 1217, 1223, 1229, 1231, 1237, 1249, 
-    1259, 1277, 1279, 1283, 1289, 1291, 1297, 1301, 1303, 1307, 1319, 1321, 
-    1327, 1361, 1367, 1373, 1381, 1399, 1409, 1423, 1427, 1429, 1433, 1439, 
-    1447, 1451, 1453, 1459, 1471, 1481, 1483, 1487, 1489, 1493, 1499, 1511, 
-    1523, 1531, 1543, 1549, 1553, 1559, 1567, 1571, 1579, 1583, 1597, 1601, 
-    1607, 1609, 1613, 1619, 1621, 1627, 1637, 1657, 1663, 1667, 1669, 1693, 
-    1697, 1699, 1709, 1721, 1723, 1733, 1741, 1747, 1753, 1759, 1777, 1783, 
-    1787, 1789, 1801, 1811, 1823, 1831, 1847, 1861, 1867, 1871, 1873, 1877, 
-    1879, 1889, 1901, 1907, 1913, 1931, 1933, 1949, 1951, 1973, 1979, 1987, 
-    1993, 1997, 1999, 2003 
-};
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Find the canonical permutation of two cubes in the pair.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_PairCanonicize( Fxu_Cube ** ppCube1, Fxu_Cube ** ppCube2 )
-{
-    Fxu_Lit * pLit1, * pLit2;
-    Fxu_Cube * pCubeTemp;
-
-    // walk through the cubes to determine 
-    // the one that has higher first variable
-    pLit1 = (*ppCube1)->lLits.pHead;
-    pLit2 = (*ppCube2)->lLits.pHead;
-    while ( 1 )
-    {
-        if ( pLit1->iVar == pLit2->iVar )
-        {
-            pLit1 = pLit1->pHNext;
-            pLit2 = pLit2->pHNext;
-            continue;
-        }
-        assert( pLit1 && pLit2 ); // this is true if the covers are SCC-free
-        if ( pLit1->iVar > pLit2->iVar )
-        { // swap the cubes
-            pCubeTemp = *ppCube1;
-            *ppCube1  = *ppCube2;
-            *ppCube2  = pCubeTemp;
-        }
-        break;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Find the canonical permutation of two cubes in the pair.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_PairCanonicize2( Fxu_Cube ** ppCube1, Fxu_Cube ** ppCube2 )
-{
-    Fxu_Cube * pCubeTemp;
-    // canonicize the pair by ordering the cubes
-    if ( (*ppCube1)->iCube > (*ppCube2)->iCube )
-    { // swap the cubes
-        pCubeTemp = *ppCube1;
-        *ppCube1  = *ppCube2;
-        *ppCube2  = pCubeTemp;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned Fxu_PairHashKeyArray( Fxu_Matrix * p, int piVarsC1[], int piVarsC2[], int nVarsC1, int nVarsC2 )
-{
-    int Offset1 = 100, Offset2 = 200, i;
-    unsigned Key;
-    // compute the hash key
-    Key = 0;
-    for ( i = 0; i < nVarsC1; i++ )
-        Key ^= s_Primes[Offset1+i] * piVarsC1[i];
-    for ( i = 0; i < nVarsC2; i++ )
-        Key ^= s_Primes[Offset2+i] * piVarsC2[i];
-    return Key;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the hash key of the divisor represented by the pair of cubes.]
-
-  Description [Goes through the variables in both cubes. Skips the identical
-  ones (this corresponds to making the cubes cube-free). Computes the hash 
-  value of the cubes. Assigns the number of literals in the base and in the 
-  cubes without base.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned Fxu_PairHashKey( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2, 
-                         int * pnBase, int * pnLits1, int * pnLits2 )
-{
-    int Offset1 = 100, Offset2 = 200;
-    int nBase, nLits1, nLits2;
-    Fxu_Lit * pLit1, * pLit2;
-    unsigned Key;
-
-    // compute the hash key
-    Key    = 0;
-    nLits1 = 0;
-    nLits2 = 0;
-    nBase  = 0;
-    pLit1  = pCube1->lLits.pHead;
-    pLit2  = pCube2->lLits.pHead;
-    while ( 1 )
-    {
-        if ( pLit1 && pLit2 )
-        {
-            if ( pLit1->iVar == pLit2->iVar )
-            { // ensure cube-free
-                pLit1 = pLit1->pHNext;
-                pLit2 = pLit2->pHNext;
-                // add this literal to the base
-                nBase++;
-            }
-            else if ( pLit1->iVar < pLit2->iVar )
-            {
-                Key  ^= s_Primes[Offset1+nLits1] * pLit1->iVar;
-                pLit1 = pLit1->pHNext;
-                nLits1++;
-            }
-            else
-            {
-                Key  ^= s_Primes[Offset2+nLits2] * pLit2->iVar;
-                pLit2 = pLit2->pHNext;
-                nLits2++;
-            }
-        }
-        else if ( pLit1 && !pLit2 )
-        {
-            Key  ^= s_Primes[Offset1+nLits1] * pLit1->iVar;
-            pLit1 = pLit1->pHNext;
-            nLits1++;
-        }
-        else if ( !pLit1 && pLit2 )
-        {
-            Key  ^= s_Primes[Offset2+nLits2] * pLit2->iVar;
-            pLit2 = pLit2->pHNext;
-            nLits2++;
-        }
-        else
-            break;
-    }
-    *pnBase  = nBase;
-    *pnLits1 = nLits1;
-    *pnLits2 = nLits2;
-    return Key;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Compares the two pairs.]
-
-  Description [Returns 1 if the divisors represented by these pairs
-  are equal.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fxu_PairCompare( Fxu_Pair * pPair1, Fxu_Pair * pPair2 )
-{
-    Fxu_Lit * pD1C1, * pD1C2;
-    Fxu_Lit * pD2C1, * pD2C2;
-    int TopVar1, TopVar2;
-    int Code;
-
-    if ( pPair1->nLits1 != pPair2->nLits1 )
-        return 0;
-    if ( pPair1->nLits2 != pPair2->nLits2 )
-        return 0;
-
-    pD1C1 = pPair1->pCube1->lLits.pHead;
-    pD1C2 = pPair1->pCube2->lLits.pHead;
-
-    pD2C1 = pPair2->pCube1->lLits.pHead;
-    pD2C2 = pPair2->pCube2->lLits.pHead;
-
-    Code  = pD1C1? 8: 0;
-    Code |= pD1C2? 4: 0;
-    Code |= pD2C1? 2: 0;
-    Code |= pD2C2? 1: 0;
-    assert( Code == 15 );
-
-    while ( 1 )
-    {
-        switch ( Code )
-        {
-        case 0:  // -- --      NULL   NULL     NULL   NULL 
-            return 1;
-        case 1:  // -- -1      NULL   NULL     NULL   pD2C2
-            return 0;
-        case 2:  // -- 1-      NULL   NULL     pD2C1  NULL 
-            return 0;
-        case 3:  // -- 11      NULL   NULL     pD2C1  pD2C2
-            if ( pD2C1->iVar != pD2C2->iVar )
-                return 0;
-            pD2C1 = pD2C1->pHNext;
-            pD2C2 = pD2C2->pHNext;
-            break;
-        case 4:  // -1 --      NULL   pD1C2    NULL   NULL 
-            return 0;
-        case 5:  // -1 -1      NULL   pD1C2    NULL   pD2C2
-            if ( pD1C2->iVar != pD2C2->iVar )
-                return 0;
-            pD1C2 = pD1C2->pHNext;
-            pD2C2 = pD2C2->pHNext;
-            break;
-        case 6:  // -1 1-      NULL   pD1C2    pD2C1  NULL 
-            return 0;
-        case 7:  // -1 11      NULL   pD1C2    pD2C1  pD2C2
-            TopVar2 = Fxu_Min( pD2C1->iVar, pD2C2->iVar );
-            if ( TopVar2 == pD1C2->iVar )
-            {
-                if ( pD2C1->iVar <= pD2C2->iVar )
-                    return 0;
-                pD1C2 = pD1C2->pHNext;
-                pD2C2 = pD2C2->pHNext;
-            }
-            else if ( TopVar2 < pD1C2->iVar )
-            {
-                if ( pD2C1->iVar != pD2C2->iVar )
-                    return 0;
-                pD2C1 = pD2C1->pHNext;
-                pD2C2 = pD2C2->pHNext;
-            }
-            else
-                return 0;
-            break;
-        case 8:  // 1- --      pD1C1  NULL     NULL   NULL 
-            return 0;
-        case 9:  // 1- -1      pD1C1  NULL     NULL   pD2C2
-            return 0;
-        case 10: // 1- 1-      pD1C1  NULL     pD2C1  NULL 
-            if ( pD1C1->iVar != pD2C1->iVar )
-                return 0;
-            pD1C1 = pD1C1->pHNext;
-            pD2C1 = pD2C1->pHNext;
-            break;
-        case 11: // 1- 11      pD1C1  NULL     pD2C1  pD2C2
-            TopVar2 = Fxu_Min( pD2C1->iVar, pD2C2->iVar );
-            if ( TopVar2 == pD1C1->iVar )
-            {
-                if ( pD2C1->iVar >= pD2C2->iVar )
-                    return 0;
-                pD1C1 = pD1C1->pHNext;
-                pD2C1 = pD2C1->pHNext;
-            }
-            else if ( TopVar2 < pD1C1->iVar )
-            {
-                if ( pD2C1->iVar != pD2C2->iVar )
-                    return 0;
-                pD2C1 = pD2C1->pHNext;
-                pD2C2 = pD2C2->pHNext;
-            }
-            else
-                return 0;
-            break;
-        case 12: // 11 --      pD1C1  pD1C2    NULL   NULL 
-            if ( pD1C1->iVar != pD1C2->iVar )
-                return 0;
-            pD1C1 = pD1C1->pHNext;
-            pD1C2 = pD1C2->pHNext;
-            break;
-        case 13: // 11 -1      pD1C1  pD1C2    NULL   pD2C2
-            TopVar1 = Fxu_Min( pD1C1->iVar, pD1C2->iVar );
-            if ( TopVar1 == pD2C2->iVar )
-            {
-                if ( pD1C1->iVar <= pD1C2->iVar )
-                    return 0;
-                pD1C2 = pD1C2->pHNext;
-                pD2C2 = pD2C2->pHNext;
-            }
-            else if ( TopVar1 < pD2C2->iVar )
-            {
-                if ( pD1C1->iVar != pD1C2->iVar )
-                    return 0;
-                pD1C1 = pD1C1->pHNext;
-                pD1C2 = pD1C2->pHNext;
-            }
-            else
-                return 0;
-            break;
-        case 14: // 11 1-      pD1C1  pD1C2    pD2C1  NULL 
-            TopVar1 = Fxu_Min( pD1C1->iVar, pD1C2->iVar );
-            if ( TopVar1 == pD2C1->iVar )
-            {
-                if ( pD1C1->iVar >= pD1C2->iVar )
-                    return 0;
-                pD1C1 = pD1C1->pHNext;
-                pD2C1 = pD2C1->pHNext;
-            }
-            else if ( TopVar1 < pD2C1->iVar )
-            {
-                if ( pD1C1->iVar != pD1C2->iVar )
-                    return 0;
-                pD1C1 = pD1C1->pHNext;
-                pD1C2 = pD1C2->pHNext;
-            }
-            else
-                return 0;
-            break;
-        case 15: // 11 11      pD1C1  pD1C2    pD2C1  pD2C2
-            TopVar1 = Fxu_Min( pD1C1->iVar, pD1C2->iVar );
-            TopVar2 = Fxu_Min( pD2C1->iVar, pD2C2->iVar );
-            if ( TopVar1 == TopVar2 )
-            {
-                if ( pD1C1->iVar == pD1C2->iVar )
-                {
-                    if ( pD2C1->iVar != pD2C2->iVar )
-                        return 0;
-                    pD1C1 = pD1C1->pHNext;
-                    pD1C2 = pD1C2->pHNext;
-                    pD2C1 = pD2C1->pHNext;
-                    pD2C2 = pD2C2->pHNext;
-                }
-                else
-                {
-                    if ( pD2C1->iVar == pD2C2->iVar )
-                        return 0;
-                    if ( pD1C1->iVar < pD1C2->iVar )
-                    {
-                        if ( pD2C1->iVar > pD2C2->iVar )
-                            return 0;
-                        pD1C1 = pD1C1->pHNext;
-                        pD2C1 = pD2C1->pHNext;
-                    }
-                    else
-                    {
-                        if ( pD2C1->iVar < pD2C2->iVar )
-                            return 0;
-                        pD1C2 = pD1C2->pHNext;
-                        pD2C2 = pD2C2->pHNext;
-                    }
-                }
-            }
-            else if ( TopVar1 < TopVar2 )
-            {
-                if ( pD1C1->iVar != pD1C2->iVar )
-                    return 0;
-                pD1C1 = pD1C1->pHNext;
-                pD1C2 = pD1C2->pHNext;
-            }
-            else 
-            {
-                if ( pD2C1->iVar != pD2C2->iVar )
-                    return 0;
-                pD2C1 = pD2C1->pHNext;
-                pD2C2 = pD2C2->pHNext;
-            }
-            break;
-        default:
-            assert( 0 );
-            break;
-        }
-
-        Code  = pD1C1? 8: 0;
-        Code |= pD1C2? 4: 0;
-        Code |= pD2C1? 2: 0;
-        Code |= pD2C2? 1: 0;
-    }
-    return 1;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates the storage for cubes pairs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_PairAllocStorage( Fxu_Var * pVar, int nCubes )
-{
-    int k;
-//    assert( pVar->nCubes == 0 );
-    pVar->nCubes  = nCubes;
-    // allocate memory for all the pairs
-    pVar->ppPairs    = ALLOC( Fxu_Pair **, nCubes );
-    pVar->ppPairs[0] = ALLOC( Fxu_Pair *,  nCubes * nCubes );
-    memset( pVar->ppPairs[0], 0, sizeof(Fxu_Pair *) * nCubes * nCubes );
-    for ( k = 1; k < nCubes; k++ )
-        pVar->ppPairs[k] = pVar->ppPairs[k-1] + nCubes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Clears all pairs associated with this cube.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_PairClearStorage( Fxu_Cube * pCube )
-{
-    Fxu_Var * pVar;
-    int i;
-    pVar = pCube->pVar;
-    for ( i = 0; i < pVar->nCubes; i++ )
-    {
-        pVar->ppPairs[pCube->iCube][i] = NULL;
-        pVar->ppPairs[i][pCube->iCube] = NULL;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Clears all pairs associated with this cube.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_PairFreeStorage( Fxu_Var * pVar )
-{
-    if ( pVar->ppPairs )
-    {
-        FREE( pVar->ppPairs[0] );
-        FREE( pVar->ppPairs );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds the pair to storage.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fxu_Pair * Fxu_PairAlloc( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2 )
-{
-    Fxu_Pair * pPair;
-       assert( pCube1->pVar == pCube2->pVar );
-    pPair = MEM_ALLOC_FXU( p, Fxu_Pair, 1 );
-    memset( pPair, 0, sizeof(Fxu_Pair) );
-    pPair->pCube1 = pCube1;
-    pPair->pCube2 = pCube2;
-    pPair->iCube1 = pCube1->iCube;
-    pPair->iCube2 = pCube2->iCube;
-    return pPair;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds the pair to storage.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_PairAdd( Fxu_Pair * pPair )
-{
-    Fxu_Var * pVar;
-
-    pVar = pPair->pCube1->pVar;
-    assert( pVar == pPair->pCube2->pVar );
-
-    pVar->ppPairs[pPair->iCube1][pPair->iCube2] = pPair;
-    pVar->ppPairs[pPair->iCube2][pPair->iCube1] = pPair;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/fxu/fxuPrint.c b/src/opt/fxu/fxuPrint.c
deleted file mode 100644
index 232b109a..00000000
--- a/src/opt/fxu/fxuPrint.c
+++ /dev/null
@@ -1,195 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fxuPrint.c]
-
-  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
-
-  Synopsis    [Various printing procedures.]
-
-  Author      [MVSIS Group]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - February 1, 2003.]
-
-  Revision    [$Id: fxuPrint.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fxuInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_MatrixPrint( FILE * pFile, Fxu_Matrix * p )
-{
-    Fxu_Var * pVar;
-    Fxu_Cube * pCube;
-    Fxu_Double * pDiv;
-    Fxu_Single * pSingle;
-    Fxu_Lit * pLit;
-    Fxu_Pair * pPair;
-    int i, LastNum;
-    int fStdout;
-
-    fStdout = 1;
-    if ( pFile == NULL )
-    {
-        pFile = fopen( "matrix.txt", "w" );
-        fStdout = 0;
-    }
-
-    fprintf( pFile, "Matrix has %d vars, %d cubes, %d literals, %d divisors.\n", 
-        p->lVars.nItems, p->lCubes.nItems, p->nEntries, p->nDivs );
-    fprintf( pFile, "Divisors selected so far: single = %d, double = %d.\n", 
-        p->nDivs1, p->nDivs2 );
-    fprintf( pFile, "\n" );
-
-    // print the numbers on top of the matrix
-    for ( i = 0; i < 12; i++ )
-        fprintf( pFile, " " );
-    Fxu_MatrixForEachVariable( p, pVar )
-        fprintf( pFile, "%d", pVar->iVar % 10 );
-    fprintf( pFile, "\n" );
-
-    // print the rows
-    Fxu_MatrixForEachCube( p, pCube )
-    {
-        fprintf( pFile, "%4d", pCube->iCube );
-        fprintf( pFile, "  " );
-        fprintf( pFile, "%4d", pCube->pVar->iVar );
-        fprintf( pFile, "  " );
-
-        // print the literals
-        LastNum = -1;
-        Fxu_CubeForEachLiteral( pCube, pLit )
-        {
-            for ( i = LastNum + 1; i < pLit->pVar->iVar; i++ )
-                fprintf( pFile, "." );
-            fprintf( pFile, "1" );
-            LastNum = i;
-        }
-        for ( i = LastNum + 1; i < p->lVars.nItems; i++ )
-            fprintf( pFile, "." );
-        fprintf( pFile, "\n" );
-    }
-    fprintf( pFile, "\n" );
-
-    // print the double-cube divisors
-    fprintf( pFile, "The double divisors are:\n" );
-    Fxu_MatrixForEachDouble( p, pDiv, i )
-    {
-        fprintf( pFile, "Divisor #%3d (lit=%d,%d) (w=%2d):  ", 
-            pDiv->Num, pDiv->lPairs.pHead->nLits1, 
-            pDiv->lPairs.pHead->nLits2, pDiv->Weight );
-        Fxu_DoubleForEachPair( pDiv, pPair )
-            fprintf( pFile, " <%d, %d> (b=%d)", 
-                pPair->pCube1->iCube, pPair->pCube2->iCube, pPair->nBase );
-        fprintf( pFile, "\n" );
-    }
-    fprintf( pFile, "\n" );
-
-    // print the divisors associated with each cube
-    fprintf( pFile, "The cubes are:\n" );
-    Fxu_MatrixForEachCube( p, pCube )
-    {
-        fprintf( pFile, "Cube #%3d: ", pCube->iCube );
-        if ( pCube->pVar->ppPairs )
-            Fxu_CubeForEachPair( pCube, pPair, i )
-                fprintf( pFile, " <%d %d> (d=%d) (b=%d)", 
-                    pPair->iCube1, pPair->iCube2, pPair->pDiv->Num, pPair->nBase );
-        fprintf( pFile, "\n" );
-    }
-    fprintf( pFile, "\n" );
-
-    // print the single-cube divisors
-    fprintf( pFile, "The single divisors are:\n" );
-    Fxu_MatrixForEachSingle( p, pSingle )
-    {
-        fprintf( pFile, "Single-cube divisor #%5d: Var1 = %4d. Var2 = %4d. Weight = %2d\n", 
-            pSingle->Num, pSingle->pVar1->iVar, pSingle->pVar2->iVar, pSingle->Weight );
-    }
-    fprintf( pFile, "\n" );
-
-/*
-    {
-        int Index;
-        fprintf( pFile, "Distribution of divisors in the hash table:\n" );
-        for ( Index = 0; Index < p->nTableSize; Index++ )
-            fprintf( pFile, " %d", p->pTable[Index].nItems );
-        fprintf( pFile, "\n" );
-    }
-*/
-    if ( !fStdout )
-        fclose( pFile );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_MatrixPrintDivisorProfile( FILE * pFile, Fxu_Matrix * p )
-{
-    Fxu_Double * pDiv;
-    int WeightMax;
-    int * pProfile;
-    int Counter1; // the number of -1 weight
-    int CounterL; // the number of less than -1 weight
-    int i;
-
-    WeightMax = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
-    pProfile = ALLOC( int, (WeightMax + 1) );
-    memset( pProfile, 0, sizeof(int) * (WeightMax + 1) );
-
-    Counter1 = 0;
-    CounterL = 0;
-    Fxu_MatrixForEachDouble( p, pDiv, i )
-    {
-        assert( pDiv->Weight <= WeightMax );
-        if ( pDiv->Weight == -1 )
-            Counter1++;
-        else if ( pDiv->Weight < 0 )
-            CounterL++;
-        else
-            pProfile[ pDiv->Weight ]++;
-    }
-
-    fprintf( pFile, "The double divisors profile:\n" );
-    fprintf( pFile, "Weight  < -1 divisors = %6d\n", CounterL );
-    fprintf( pFile, "Weight    -1 divisors = %6d\n", Counter1 );
-    for ( i = 0; i <= WeightMax; i++ )
-        if ( pProfile[i] )
-            fprintf( pFile, "Weight   %3d divisors = %6d\n", i, pProfile[i] );
-    fprintf( pFile, "End of divisor profile printout\n" );
-    FREE( pProfile );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/fxu/fxuReduce.c b/src/opt/fxu/fxuReduce.c
deleted file mode 100644
index 0ab8a157..00000000
--- a/src/opt/fxu/fxuReduce.c
+++ /dev/null
@@ -1,204 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fxuReduce.c]
-
-  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
-
-  Synopsis    [Procedures to reduce the number of considered cube pairs.]
-
-  Author      [MVSIS Group]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - February 1, 2003.]
-
-  Revision    [$Id: fxuReduce.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "fxuInt.h"
-#include "fxu.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static int Fxu_CountPairDiffs( char * pCover, unsigned char pDiffs[] );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Precomputes the pairs to use for creating two-cube divisors.]
-
-  Description [This procedure takes the matrix with variables and cubes 
-  allocated (p), the original covers of the nodes (i-sets) and their number 
-  (ppCovers,nCovers). The maximum number of pairs to compute and the total 
-  number of pairs in existence. This procedure adds to the storage of
-  divisors exactly the given number of pairs (nPairsMax) while taking
-  first those pairs that have the smallest number of literals in their
-  cube-free form.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax )
-{
-    unsigned char * pnLitsDiff;   // storage for the counters of diff literals
-    int * pnPairCounters;         // the counters of pairs for each number of diff literals
-    Fxu_Cube * pCubeFirst, * pCubeLast;
-    Fxu_Cube * pCube1, * pCube2;
-    Fxu_Var * pVar;
-    int nCubes, nBitsMax, nSum;
-    int CutOffNum, CutOffQuant;
-    int iPair, iQuant, k, c;
-    int clk = clock();
-    char * pSopCover;
-    int nFanins;
-
-    assert( nPairsMax < nPairsTotal );
-
-    // allocate storage for counter of diffs
-    pnLitsDiff = ALLOC( unsigned char, nPairsTotal );
-    // go through the covers and precompute the distances between the pairs
-    iPair    =  0;
-    nBitsMax = -1;
-    for ( c = 0; c < vCovers->nSize; c++ )
-        if ( pSopCover = vCovers->pArray[c] )
-        {
-            nFanins = Abc_SopGetVarNum(pSopCover);
-            // precompute the differences
-            Fxu_CountPairDiffs( pSopCover, pnLitsDiff + iPair );
-            // update the counter
-            nCubes = Abc_SopGetCubeNum( pSopCover );
-            iPair += nCubes * (nCubes - 1) / 2;
-            if ( nBitsMax < nFanins )
-                nBitsMax = nFanins;
-        }
-    assert( iPair == nPairsTotal );
-
-    // allocate storage for counters of cube pairs by difference
-    pnPairCounters = ALLOC( int, 2 * nBitsMax );
-    memset( pnPairCounters, 0, sizeof(int) * 2 * nBitsMax );
-    // count the number of different pairs
-    for ( k = 0; k < nPairsTotal; k++ )
-        pnPairCounters[ pnLitsDiff[k] ]++;
-    // determine what pairs to take starting from the lower
-    // so that there would be exactly pPairsMax pairs
-    if ( pnPairCounters[0] != 0 )
-    {
-        printf( "The SOPs of the nodes are not cube-free. Run \"bdd; sop\" before \"fx\".\n" );
-        return 0;
-    }
-    if ( pnPairCounters[1] != 0 )
-    {
-        printf( "The SOPs of the nodes are not SCC-free. Run \"bdd; sop\" before \"fx\".\n" );
-        return 0;
-    }
-    assert( pnPairCounters[0] == 0 ); // otherwise, covers are not dup-free
-    assert( pnPairCounters[1] == 0 ); // otherwise, covers are not SCC-free
-    nSum = 0;
-    for ( k = 0; k < 2 * nBitsMax; k++ )
-    {
-        nSum += pnPairCounters[k];
-        if ( nSum >= nPairsMax )
-        {
-            CutOffNum   = k;
-            CutOffQuant = pnPairCounters[k] - (nSum - nPairsMax);
-            break;
-        }
-    }
-    FREE( pnPairCounters );
-
-    // set to 0 all the pairs above the cut-off number and quantity
-    iQuant = 0;
-    iPair  = 0;
-    for ( k = 0; k < nPairsTotal; k++ )
-        if ( pnLitsDiff[k] > CutOffNum ) 
-            pnLitsDiff[k] = 0;
-        else if ( pnLitsDiff[k] == CutOffNum )
-        {
-            if ( iQuant++ >= CutOffQuant )
-                pnLitsDiff[k] = 0;
-            else
-                iPair++;
-        }
-        else
-            iPair++;
-    assert( iPair == nPairsMax );
-
-    // collect the corresponding pairs and add the divisors
-    iPair = 0;
-    for ( c = 0; c < vCovers->nSize; c++ )
-        if ( pSopCover = vCovers->pArray[c] )
-        {
-            // get the var
-            pVar = p->ppVars[2*c+1];
-            // get the first cube
-            pCubeFirst = pVar->pFirst;
-            // get the last cube
-            pCubeLast = pCubeFirst;
-            for ( k = 0; k < pVar->nCubes; k++ )
-                pCubeLast = pCubeLast->pNext;
-            assert( pCubeLast == NULL || pCubeLast->pVar != pVar );
-
-            // go through the cube pairs
-            for ( pCube1 = pCubeFirst; pCube1 != pCubeLast; pCube1 = pCube1->pNext )
-                for ( pCube2 = pCube1->pNext; pCube2 != pCubeLast; pCube2 = pCube2->pNext )
-                    if ( pnLitsDiff[iPair++] )
-                    {   // create the divisors for this pair
-                        Fxu_MatrixAddDivisor( p, pCube1, pCube2 );
-                    }
-        }
-    assert( iPair == nPairsTotal );
-    FREE( pnLitsDiff );
-//PRT( "Preprocess", clock() - clk );
-    return 1;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the differences in each cube pair in the cover.]
-
-  Description [Takes the cover (pCover) and the array where the
-  diff counters go (pDiffs). The array pDiffs should have as many
-  entries as there are different pairs of cubes in the cover: n(n-1)/2.
-  Fills out the array pDiffs with the following info: For each cube
-  pair, included in the array is the number of literals in both cubes
-  after they are made cube free.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fxu_CountPairDiffs( char * pCover, unsigned char pDiffs[] )
-{
-    char * pCube1, * pCube2;
-    int nOnes, nCubePairs, nFanins, v;
-    nCubePairs = 0;
-    nFanins = Abc_SopGetVarNum(pCover);
-    Abc_SopForEachCube( pCover, nFanins, pCube1 )
-    Abc_SopForEachCube( pCube1, nFanins, pCube2 )
-    {
-        if ( pCube1 == pCube2 )
-            continue;
-        nOnes = 0;
-        for ( v = 0; v < nFanins; v++ )
-            nOnes += (pCube1[v] != pCube2[v]);
-        pDiffs[nCubePairs++] = nOnes;
-    }
-    return 1;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/fxu/fxuSelect.c b/src/opt/fxu/fxuSelect.c
deleted file mode 100644
index b9265487..00000000
--- a/src/opt/fxu/fxuSelect.c
+++ /dev/null
@@ -1,603 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fxuSelect.c]
-
-  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
-
-  Synopsis    [Procedures to select the best divisor/complement pair.]
-
-  Author      [MVSIS Group]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - February 1, 2003.]
-
-  Revision    [$Id: fxuSelect.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fxuInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-#define MAX_SIZE_LOOKAHEAD      20
-
-static int Fxu_MatrixFindComplement( Fxu_Matrix * p, int iVar );
-
-static Fxu_Double * Fxu_MatrixFindComplementSingle( Fxu_Matrix * p, Fxu_Single * pSingle );
-static Fxu_Single * Fxu_MatrixFindComplementDouble2( Fxu_Matrix * p, Fxu_Double * pDouble );
-static Fxu_Double * Fxu_MatrixFindComplementDouble4( Fxu_Matrix * p, Fxu_Double * pDouble );
-
-Fxu_Double * Fxu_MatrixFindDouble( Fxu_Matrix * p, 
-     int piVarsC1[], int piVarsC2[], int nVarsC1, int nVarsC2 );
-void Fxu_MatrixGetDoubleVars( Fxu_Matrix * p, Fxu_Double * pDouble, 
-    int piVarsC1[], int piVarsC2[], int * pnVarsC1, int * pnVarsC2 );
-
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Selects the best pair (Single,Double) and returns their weight.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fxu_Select( Fxu_Matrix * p, Fxu_Single ** ppSingle, Fxu_Double ** ppDouble )
-{
-    // the top entries
-    Fxu_Single * pSingles[MAX_SIZE_LOOKAHEAD];
-    Fxu_Double * pDoubles[MAX_SIZE_LOOKAHEAD];
-    // the complements
-    Fxu_Double * pSCompl[MAX_SIZE_LOOKAHEAD];
-    Fxu_Single * pDComplS[MAX_SIZE_LOOKAHEAD];
-    Fxu_Double * pDComplD[MAX_SIZE_LOOKAHEAD];
-    Fxu_Pair * pPair;
-    int nSingles;
-    int nDoubles;
-    int i;
-    int WeightBest;
-    int WeightCur;
-    int iNum, fBestS;
-
-    // collect the top entries from the queues
-    for ( nSingles = 0; nSingles < MAX_SIZE_LOOKAHEAD; nSingles++ )
-    {
-        pSingles[nSingles] = Fxu_HeapSingleGetMax( p->pHeapSingle );
-        if ( pSingles[nSingles] == NULL )
-            break;
-    }
-    // put them back into the queue
-    for ( i = 0; i < nSingles; i++ )
-        if ( pSingles[i] )
-            Fxu_HeapSingleInsert( p->pHeapSingle, pSingles[i] );
-        
-    // the same for doubles
-    // collect the top entries from the queues
-    for ( nDoubles = 0; nDoubles < MAX_SIZE_LOOKAHEAD; nDoubles++ )
-    {
-        pDoubles[nDoubles] = Fxu_HeapDoubleGetMax( p->pHeapDouble );
-        if ( pDoubles[nDoubles] == NULL )
-            break;
-    }
-    // put them back into the queue
-    for ( i = 0; i < nDoubles; i++ )
-        if ( pDoubles[i] )
-            Fxu_HeapDoubleInsert( p->pHeapDouble, pDoubles[i] );
-
-    // for each single, find the complement double (if any)
-    for ( i = 0; i < nSingles; i++ )
-        if ( pSingles[i] )
-            pSCompl[i] = Fxu_MatrixFindComplementSingle( p, pSingles[i] );
-
-    // for each double, find the complement single or double (if any)
-    for ( i = 0; i < nDoubles; i++ )
-        if ( pDoubles[i] )
-        {
-            pPair = pDoubles[i]->lPairs.pHead;
-            if ( pPair->nLits1 == 1 && pPair->nLits2 == 1 )
-            {
-                pDComplS[i] = Fxu_MatrixFindComplementDouble2( p, pDoubles[i] );
-                pDComplD[i] = NULL;
-            }
-//            else if ( pPair->nLits1 == 2 && pPair->nLits2 == 2 )
-//            {
-//                pDComplS[i] = NULL;
-//                pDComplD[i] = Fxu_MatrixFindComplementDouble4( p, pDoubles[i] );
-//            }
-            else
-            {
-                pDComplS[i] = NULL;
-                pDComplD[i] = NULL;
-            }
-        }
-
-    // select the best pair
-    WeightBest = -1;
-    for ( i = 0; i < nSingles; i++ )
-    {
-        WeightCur = pSingles[i]->Weight;
-        if ( pSCompl[i] )
-        {
-            // add the weight of the double
-            WeightCur += pSCompl[i]->Weight;
-            // there is no need to implement this double, so...
-            pPair      = pSCompl[i]->lPairs.pHead;
-            WeightCur += pPair->nLits1 + pPair->nLits2;
-        }
-        if ( WeightBest < WeightCur )
-        {
-            WeightBest = WeightCur;
-            *ppSingle = pSingles[i];
-            *ppDouble = pSCompl[i];
-            fBestS = 1;
-            iNum = i;
-        }
-    }
-    for ( i = 0; i < nDoubles; i++ )
-    {
-        WeightCur = pDoubles[i]->Weight;
-        if ( pDComplS[i] )
-        {
-            // add the weight of the single
-            WeightCur += pDComplS[i]->Weight;
-            // there is no need to implement this double, so...
-            pPair      = pDoubles[i]->lPairs.pHead;
-            WeightCur += pPair->nLits1 + pPair->nLits2;
-        }
-        if ( WeightBest < WeightCur )
-        {
-            WeightBest = WeightCur;
-            *ppSingle = pDComplS[i];
-            *ppDouble = pDoubles[i];
-            fBestS = 0;
-            iNum = i;
-        }
-    }
-/*
-    // print the statistics
-    printf( "\n" );
-    for ( i = 0; i < nSingles; i++ )
-    {
-        printf( "Single #%d: Weight = %3d. ", i, pSingles[i]->Weight );
-        printf( "Compl: " );
-        if ( pSCompl[i] == NULL )
-            printf( "None." );
-        else
-            printf( "D  Weight = %3d  Sum = %3d", 
-                pSCompl[i]->Weight, pSCompl[i]->Weight + pSingles[i]->Weight );
-        printf( "\n" );
-    }
-    printf( "\n" );
-    for ( i = 0; i < nDoubles; i++ )
-    {
-        printf( "Double #%d: Weight = %3d. ", i, pDoubles[i]->Weight );
-        printf( "Compl: " );
-        if ( pDComplS[i] == NULL && pDComplD[i] == NULL )
-            printf( "None." );
-        else if ( pDComplS[i] )
-            printf( "S  Weight = %3d  Sum = %3d", 
-                pDComplS[i]->Weight, pDComplS[i]->Weight + pDoubles[i]->Weight );
-        else if ( pDComplD[i] )
-            printf( "D  Weight = %3d  Sum = %3d", 
-                pDComplD[i]->Weight, pDComplD[i]->Weight + pDoubles[i]->Weight );
-        printf( "\n" );
-    }
-    if ( WeightBest == -1 )
-        printf( "Selected NONE\n" );
-    else
-    {
-        printf( "Selected = %s.  ", fBestS? "S": "D" );
-        printf( "Number = %d.  ", iNum );
-        printf( "Weight = %d.\n", WeightBest );
-    }
-    printf( "\n" );
-*/
-    return WeightBest;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fxu_Double * Fxu_MatrixFindComplementSingle( Fxu_Matrix * p, Fxu_Single * pSingle )
-{
-//    int * pValue2Node = p->pValue2Node;
-    int iVar1,  iVar2;
-    int iVar1C, iVar2C;
-    // get the variables of this single div
-    iVar1  = pSingle->pVar1->iVar;
-    iVar2  = pSingle->pVar2->iVar;
-    iVar1C = Fxu_MatrixFindComplement( p, iVar1 );
-    iVar2C = Fxu_MatrixFindComplement( p, iVar2 );
-    if ( iVar1C == -1 || iVar2C == -1 )
-        return NULL;
-    assert( iVar1C < iVar2C );
-    return Fxu_MatrixFindDouble( p, &iVar1C, &iVar2C, 1, 1 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fxu_Single * Fxu_MatrixFindComplementDouble2( Fxu_Matrix * p, Fxu_Double * pDouble )
-{
-//    int * pValue2Node = p->pValue2Node;
-    int piVarsC1[10], piVarsC2[10];
-    int nVarsC1, nVarsC2;
-    int iVar1,  iVar2, iVarTemp;
-    int iVar1C, iVar2C;
-    Fxu_Single * pSingle;
-
-    // get the variables of this double div
-    Fxu_MatrixGetDoubleVars( p, pDouble, piVarsC1, piVarsC2, &nVarsC1, &nVarsC2 );
-    assert( nVarsC1 == 1 );
-    assert( nVarsC2 == 1 );
-    iVar1 = piVarsC1[0];
-    iVar2 = piVarsC2[0];
-    assert( iVar1 < iVar2 );
-
-    iVar1C = Fxu_MatrixFindComplement( p, iVar1 );
-    iVar2C = Fxu_MatrixFindComplement( p, iVar2 );
-    if ( iVar1C == -1 || iVar2C == -1 )
-        return NULL;
- 
-    // go through the queque and find this one
-//    assert( iVar1C < iVar2C );
-    if ( iVar1C > iVar2C )
-    {
-        iVarTemp = iVar1C;
-        iVar1C = iVar2C;
-        iVar2C = iVarTemp;
-    }
-
-    Fxu_MatrixForEachSingle( p, pSingle )
-        if ( pSingle->pVar1->iVar == iVar1C && pSingle->pVar2->iVar == iVar2C )
-            return pSingle;
-    return NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fxu_Double * Fxu_MatrixFindComplementDouble4( Fxu_Matrix * p, Fxu_Double * pDouble )
-{
-//    int * pValue2Node = p->pValue2Node;
-    int piVarsC1[10], piVarsC2[10];
-    int nVarsC1, nVarsC2;
-    int iVar11,  iVar12,  iVar21,  iVar22;
-    int iVar11C, iVar12C, iVar21C, iVar22C;
-    int RetValue;
-
-    // get the variables of this double div
-    Fxu_MatrixGetDoubleVars( p, pDouble, piVarsC1, piVarsC2, &nVarsC1, &nVarsC2 );
-    assert( nVarsC1 == 2 && nVarsC2 == 2 );
-
-    iVar11 = piVarsC1[0];
-    iVar12 = piVarsC1[1];
-    iVar21 = piVarsC2[0];
-    iVar22 = piVarsC2[1];
-    assert( iVar11 < iVar21 );
-
-    iVar11C = Fxu_MatrixFindComplement( p, iVar11 );
-    iVar12C = Fxu_MatrixFindComplement( p, iVar12 );
-    iVar21C = Fxu_MatrixFindComplement( p, iVar21 );
-    iVar22C = Fxu_MatrixFindComplement( p, iVar22 );
-    if ( iVar11C == -1 || iVar12C == -1 || iVar21C == -1 || iVar22C == -1 )
-        return NULL;
-    if ( iVar11C != iVar21 || iVar12C != iVar22 || 
-         iVar21C != iVar11 || iVar22C != iVar12 )
-         return NULL;
-
-    // a'b' + ab   =>  a'b  + ab'
-    // a'b  + ab'  =>  a'b' + ab
-    // swap the second pair in each cube
-    RetValue    = piVarsC1[1];
-    piVarsC1[1] = piVarsC2[1];
-    piVarsC2[1] = RetValue;
-
-    return Fxu_MatrixFindDouble( p, piVarsC1, piVarsC2, 2, 2 );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fxu_MatrixFindComplement( Fxu_Matrix * p, int iVar )
-{
-    return iVar ^ 1;
-/*
-//    int * pValue2Node = p->pValue2Node;
-    int iVarC;
-    int iNode;
-    int Beg, End;
-
-    // get the nodes
-    iNode = pValue2Node[iVar];
-    // get the first node with the same var
-    for ( Beg = iVar; Beg >= 0; Beg-- )
-        if ( pValue2Node[Beg] != iNode )
-        {
-            Beg++;
-            break;
-        }
-    // get the last node with the same var
-    for ( End = iVar;          ; End++ )
-        if ( pValue2Node[End] != iNode )
-        {
-            End--;
-            break;
-        }
-
-    // if one of the vars is not binary, quit
-    if ( End - Beg > 1 )
-        return -1;
-
-    // get the complements
-    if ( iVar == Beg )
-        iVarC = End;
-    else if ( iVar == End ) 
-        iVarC = Beg;
-    else
-    {
-        assert( 0 );
-    }
-    return iVarC;
-*/
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_MatrixGetDoubleVars( Fxu_Matrix * p, Fxu_Double * pDouble, 
-    int piVarsC1[], int piVarsC2[], int * pnVarsC1, int * pnVarsC2 )
-{
-    Fxu_Pair * pPair;
-    Fxu_Lit * pLit1, * pLit2;
-    int nLits1, nLits2;
-
-    // get the first pair
-    pPair = pDouble->lPairs.pHead;
-    // init the parameters
-    nLits1 = 0;
-    nLits2 = 0;
-    pLit1 = pPair->pCube1->lLits.pHead;
-    pLit2 = pPair->pCube2->lLits.pHead;
-    while ( 1 )
-    {
-        if ( pLit1 && pLit2 )
-        {
-            if ( pLit1->iVar == pLit2->iVar )
-            { // ensure cube-free
-                pLit1 = pLit1->pHNext;
-                pLit2 = pLit2->pHNext;
-            }
-            else if ( pLit1->iVar < pLit2->iVar )
-            {
-                piVarsC1[nLits1++] = pLit1->iVar;
-                 pLit1 = pLit1->pHNext;
-           }
-            else
-            {
-                piVarsC2[nLits2++] = pLit2->iVar;
-                pLit2 = pLit2->pHNext;
-            }
-        }
-        else if ( pLit1 && !pLit2 )
-        {
-            piVarsC1[nLits1++] = pLit1->iVar;
-            pLit1 = pLit1->pHNext;
-        }
-        else if ( !pLit1 && pLit2 )
-        {
-            piVarsC2[nLits2++] = pLit2->iVar;
-            pLit2 = pLit2->pHNext;
-        }
-        else
-            break;
-    }
-    *pnVarsC1 = nLits1;
-    *pnVarsC2 = nLits2;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fxu_Double * Fxu_MatrixFindDouble( Fxu_Matrix * p, 
-     int piVarsC1[], int piVarsC2[], int nVarsC1, int nVarsC2 )
-{
-    int piVarsC1_[100], piVarsC2_[100];
-    int nVarsC1_, nVarsC2_, i;
-    Fxu_Double * pDouble;
-    Fxu_Pair * pPair;
-    unsigned Key;
-
-    assert( nVarsC1 > 0 );
-    assert( nVarsC2 > 0 );
-    assert( piVarsC1[0] < piVarsC2[0] );
-
-    // get the hash key
-    Key = Fxu_PairHashKeyArray( p, piVarsC1, piVarsC2, nVarsC1, nVarsC2 );
-    
-    // check if the divisor for this pair already exists
-    Key %= p->nTableSize;
-    Fxu_TableForEachDouble( p, Key, pDouble )
-    {
-        pPair = pDouble->lPairs.pHead;
-        if ( pPair->nLits1 != nVarsC1 )
-            continue;
-        if ( pPair->nLits2 != nVarsC2 )
-            continue;
-        // get the cubes of this divisor
-        Fxu_MatrixGetDoubleVars( p, pDouble, piVarsC1_, piVarsC2_, &nVarsC1_, &nVarsC2_ );
-        // compare lits of the first cube
-        for ( i = 0; i < nVarsC1; i++ )
-            if ( piVarsC1[i] != piVarsC1_[i] )
-                break;
-        if ( i != nVarsC1 )
-            continue;
-        // compare lits of the second cube
-        for ( i = 0; i < nVarsC2; i++ )
-            if ( piVarsC2[i] != piVarsC2_[i] )
-                break;
-        if ( i != nVarsC2 )
-            continue;
-        return pDouble;
-    }
-    return NULL;
-}
-
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fxu_SelectSCD( Fxu_Matrix * p, int WeightLimit, Fxu_Var ** ppVar1, Fxu_Var ** ppVar2 )
-{
-//    int * pValue2Node = p->pValue2Node;
-    Fxu_Var * pVar1;
-    Fxu_Var * pVar2, * pVarTemp;
-    Fxu_Lit * pLitV, * pLitH;
-    int Coin;
-    int CounterAll;
-    int CounterTest;
-    int WeightCur;
-    int WeightBest;
-
-    CounterAll = 0;
-    CounterTest = 0;
-
-    WeightBest = -10;
-    
-    // iterate through the columns in the matrix
-    Fxu_MatrixForEachVariable( p, pVar1 )
-    {
-        // start collecting the affected vars
-        Fxu_MatrixRingVarsStart( p );
-
-        // go through all the literals of this variable
-        for ( pLitV = pVar1->lLits.pHead; pLitV; pLitV = pLitV->pVNext )
-        {
-            // for this literal, go through all the horizontal literals
-            for ( pLitH = pLitV->pHNext; pLitH; pLitH = pLitH->pHNext )
-            {
-                // get another variable
-                pVar2 = pLitH->pVar;
-                CounterAll++;
-                // skip the var if it is already used
-                if ( pVar2->pOrder )
-                    continue;
-                // skip the var if it belongs to the same node
-//                if ( pValue2Node[pVar1->iVar] == pValue2Node[pVar2->iVar] )
-//                    continue;
-                // collect the var
-                Fxu_MatrixRingVarsAdd( p, pVar2 );
-            }
-        }
-        // stop collecting the selected vars
-        Fxu_MatrixRingVarsStop( p );
-
-        // iterate through the selected vars
-        Fxu_MatrixForEachVarInRing( p, pVar2 )
-        {
-            CounterTest++;
-
-            // count the coincidence
-            Coin = Fxu_SingleCountCoincidence( p, pVar1, pVar2 );
-            assert( Coin > 0 );
-
-            // get the new weight
-            WeightCur = Coin - 2;
-
-            // compare the weights
-            if ( WeightBest < WeightCur )
-            {
-                WeightBest = WeightCur;
-                *ppVar1 = pVar1;
-                *ppVar2 = pVar2;
-            }
-        }
-        // unmark the vars
-        Fxu_MatrixForEachVarInRingSafe( p, pVar2, pVarTemp )
-            pVar2->pOrder = NULL;
-        Fxu_MatrixRingVarsReset( p );
-    }
-
-//    if ( WeightBest == WeightLimit )
-//        return -1;
-    return WeightBest;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/fxu/fxuSingle.c b/src/opt/fxu/fxuSingle.c
deleted file mode 100644
index 73d9a76c..00000000
--- a/src/opt/fxu/fxuSingle.c
+++ /dev/null
@@ -1,284 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fxuSingle.c]
-
-  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
-
-  Synopsis    [Procedures to compute the set of single-cube divisors.]
-
-  Author      [MVSIS Group]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - February 1, 2003.]
-
-  Revision    [$Id: fxuSingle.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fxuInt.h"
-#include "vec.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static void Fxu_MatrixComputeSinglesOneCollect( Fxu_Matrix * p, Fxu_Var * pVar, Vec_Ptr_t * vSingles );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Computes and adds all single-cube divisors to storage.]
-
-  Description [This procedure should be called once when the matrix is
-  already contructed before the process of logic extraction begins..]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax )
-{
-    Fxu_Var * pVar;
-    Vec_Ptr_t * vSingles;
-    int i, k;
-    // set the weight limit
-    p->nWeightLimit = 1 - fUse0;
-    // iterate through columns in the matrix and collect single-cube divisors
-    vSingles = Vec_PtrAlloc( 10000 );
-    Fxu_MatrixForEachVariable( p, pVar )
-        Fxu_MatrixComputeSinglesOneCollect( p, pVar, vSingles );
-    p->nSingleTotal = Vec_PtrSize(vSingles) / 3;
-    // check if divisors should be filtered
-    if ( Vec_PtrSize(vSingles) > nSingleMax )
-    {
-        int * pWeigtCounts, nDivCount, Weight, i, c;;
-        assert( Vec_PtrSize(vSingles) % 3 == 0 );
-        // count how many divisors have the given weight
-        pWeigtCounts = ALLOC( int, 1000 );
-        memset( pWeigtCounts, 0, sizeof(int) * 1000 );
-        for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 )
-        {
-            Weight = (int)Vec_PtrEntry(vSingles, i);
-            if ( Weight >= 999 )
-                pWeigtCounts[999]++;
-            else
-                pWeigtCounts[Weight]++;
-        }
-        // select the bound on the weight (above this bound, singles will be included)
-        nDivCount = 0;
-        for ( c = 999; c >= 0; c-- )
-        {
-            nDivCount += pWeigtCounts[c];
-            if ( nDivCount >= nSingleMax )
-                break;
-        }
-        free( pWeigtCounts );
-        // collect singles with the given costs
-        k = 0;
-        for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 )
-        {
-            Weight = (int)Vec_PtrEntry(vSingles, i);
-            if ( Weight < c )
-                continue;
-            Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-2) );
-            Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-1) );
-            Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i) );
-            if ( k/3 == nSingleMax )
-                break;
-        }
-        Vec_PtrShrink( vSingles, k );
-        // adjust the weight limit
-        p->nWeightLimit = c;
-    }
-    // collect the selected divisors
-    assert( Vec_PtrSize(vSingles) % 3 == 0 );
-    for ( i = 0; i < Vec_PtrSize(vSingles); i += 3 )
-    {
-        Fxu_MatrixAddSingle( p, 
-            Vec_PtrEntry(vSingles,i), 
-            Vec_PtrEntry(vSingles,i+1), 
-            (int)Vec_PtrEntry(vSingles,i+2) );
-    }
-    Vec_PtrFree( vSingles );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds the single-cube divisors associated with a new column.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_MatrixComputeSinglesOneCollect( Fxu_Matrix * p, Fxu_Var * pVar, Vec_Ptr_t * vSingles )
-{
-    Fxu_Lit * pLitV, * pLitH;
-    Fxu_Var * pVar2;
-    int Coin;
-    int WeightCur;
-
-    // start collecting the affected vars
-    Fxu_MatrixRingVarsStart( p );
-    // go through all the literals of this variable
-    for ( pLitV = pVar->lLits.pHead; pLitV; pLitV = pLitV->pVNext )
-        // for this literal, go through all the horizontal literals
-        for ( pLitH = pLitV->pHPrev; pLitH; pLitH = pLitH->pHPrev )
-        {
-            // get another variable
-            pVar2 = pLitH->pVar;
-            // skip the var if it is already used
-            if ( pVar2->pOrder )
-                continue;
-            // skip the var if it belongs to the same node
-//            if ( pValue2Node[pVar->iVar] == pValue2Node[pVar2->iVar] )
-//                continue;
-            // collect the var
-            Fxu_MatrixRingVarsAdd( p, pVar2 );
-        }
-    // stop collecting the selected vars
-    Fxu_MatrixRingVarsStop( p );
-
-    // iterate through the selected vars
-    Fxu_MatrixForEachVarInRing( p, pVar2 )
-    {
-        // count the coincidence
-        Coin = Fxu_SingleCountCoincidence( p, pVar2, pVar );
-        assert( Coin > 0 );
-        // get the new weight
-        WeightCur = Coin - 2;
-        // peformance fix (August 24, 2007)
-        if ( WeightCur >= p->nWeightLimit )
-        {
-            Vec_PtrPush( vSingles, pVar2 );
-            Vec_PtrPush( vSingles, pVar );
-            Vec_PtrPush( vSingles, (void *)WeightCur );
-        }
-    }
-
-    // unmark the vars
-    Fxu_MatrixRingVarsUnmark( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds the single-cube divisors associated with a new column.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar )
-{
-    Fxu_Lit * pLitV, * pLitH;
-    Fxu_Var * pVar2;
-    int Coin;
-    int WeightCur;
-
-    // start collecting the affected vars
-    Fxu_MatrixRingVarsStart( p );
-    // go through all the literals of this variable
-    for ( pLitV = pVar->lLits.pHead; pLitV; pLitV = pLitV->pVNext )
-        // for this literal, go through all the horizontal literals
-        for ( pLitH = pLitV->pHPrev; pLitH; pLitH = pLitH->pHPrev )
-        {
-            // get another variable
-            pVar2 = pLitH->pVar;
-            // skip the var if it is already used
-            if ( pVar2->pOrder )
-                continue;
-            // skip the var if it belongs to the same node
-//            if ( pValue2Node[pVar->iVar] == pValue2Node[pVar2->iVar] )
-//                continue;
-            // collect the var
-            Fxu_MatrixRingVarsAdd( p, pVar2 );
-        }
-    // stop collecting the selected vars
-    Fxu_MatrixRingVarsStop( p );
-
-    // iterate through the selected vars
-    Fxu_MatrixForEachVarInRing( p, pVar2 )
-    {
-        // count the coincidence
-        Coin = Fxu_SingleCountCoincidence( p, pVar2, pVar );
-        assert( Coin > 0 );
-        // get the new weight
-        WeightCur = Coin - 2;
-        // peformance fix (August 24, 2007)
-//        if ( WeightCur >= 0 )
-//        Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur );
-        if ( WeightCur >= p->nWeightLimit )
-            Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur );
-    }
-    // unmark the vars
-    Fxu_MatrixRingVarsUnmark( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the coincidence count of two columns.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fxu_SingleCountCoincidence( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVar2 )
-{
-    Fxu_Lit * pLit1, * pLit2;
-    int Result;
-
-    // compute the coincidence count
-    Result = 0;
-    pLit1  = pVar1->lLits.pHead;
-    pLit2  = pVar2->lLits.pHead;
-    while ( 1 )
-    {
-        if ( pLit1 && pLit2 )
-        {
-            if ( pLit1->pCube->pVar->iVar == pLit2->pCube->pVar->iVar )
-            { // the variables are the same
-                if ( pLit1->iCube == pLit2->iCube )
-                { // the literals are the same
-                    pLit1 = pLit1->pVNext;
-                    pLit2 = pLit2->pVNext;
-                    // add this literal to the coincidence
-                    Result++;
-                }
-                else if ( pLit1->iCube < pLit2->iCube )
-                    pLit1 = pLit1->pVNext;
-                else
-                    pLit2 = pLit2->pVNext;
-            }
-            else if ( pLit1->pCube->pVar->iVar < pLit2->pCube->pVar->iVar )
-                pLit1 = pLit1->pVNext;
-            else
-                pLit2 = pLit2->pVNext;
-        }
-        else if ( pLit1 && !pLit2 )
-            pLit1 = pLit1->pVNext;
-        else if ( !pLit1 && pLit2 )
-            pLit2 = pLit2->pVNext;
-        else
-            break;
-    }
-    return Result;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/fxu/fxuUpdate.c b/src/opt/fxu/fxuUpdate.c
deleted file mode 100644
index 274f79f6..00000000
--- a/src/opt/fxu/fxuUpdate.c
+++ /dev/null
@@ -1,806 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fxuUpdate.c]
-
-  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
-
-  Synopsis    [Updating the sparse matrix when divisors are accepted.]
-
-  Author      [MVSIS Group]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - February 1, 2003.]
-
-  Revision    [$Id: fxuUpdate.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fxuInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static void Fxu_UpdateDoublePairs( Fxu_Matrix * p, Fxu_Double * pDouble, Fxu_Var * pVar );
-static void Fxu_UpdateMatrixDoubleCreateCubes( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2, Fxu_Double * pDiv );
-static void Fxu_UpdateMatrixDoubleClean( Fxu_Matrix * p, Fxu_Cube * pCubeUse, Fxu_Cube * pCubeRem );
-static void Fxu_UpdateMatrixSingleClean( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVar2, Fxu_Var * pVarNew );
-
-static void Fxu_UpdateCreateNewVars( Fxu_Matrix * p, Fxu_Var ** ppVarC, Fxu_Var ** ppVarD, int nCubes );
-static int  Fxu_UpdatePairCompare( Fxu_Pair ** ppP1, Fxu_Pair ** ppP2 );
-static void Fxu_UpdatePairsSort( Fxu_Matrix * p, Fxu_Double * pDouble );
-
-static void Fxu_UpdateCleanOldDoubles( Fxu_Matrix * p, Fxu_Double * pDiv, Fxu_Cube * pCube );
-static void Fxu_UpdateAddNewDoubles( Fxu_Matrix * p, Fxu_Cube * pCube );
-static void Fxu_UpdateCleanOldSingles( Fxu_Matrix * p );
-static void Fxu_UpdateAddNewSingles( Fxu_Matrix * p, Fxu_Var * pVar );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Updates the matrix after selecting two divisors.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_Update( Fxu_Matrix * p, Fxu_Single * pSingle, Fxu_Double * pDouble )
-{
-    Fxu_Cube * pCube, * pCubeNew;
-    Fxu_Var * pVarC, * pVarD;
-    Fxu_Var * pVar1, * pVar2;
-
-    // consider trivial cases
-    if ( pSingle == NULL )
-    {
-        assert( pDouble->Weight == Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble ) );
-        Fxu_UpdateDouble( p );
-        return;
-    }
-    if ( pDouble == NULL )
-    {
-        assert( pSingle->Weight == Fxu_HeapSingleReadMaxWeight( p->pHeapSingle ) );
-        Fxu_UpdateSingle( p );
-        return;
-    }
-
-    // get the variables of the single
-    pVar1 = pSingle->pVar1;
-    pVar2 = pSingle->pVar2;
-
-    // remove the best double from the heap
-    Fxu_HeapDoubleDelete( p->pHeapDouble, pDouble );
-    // remove the best divisor from the table
-    Fxu_ListTableDelDivisor( p, pDouble );
-
-    // create two new columns (vars)
-    Fxu_UpdateCreateNewVars( p, &pVarC, &pVarD, 1 );
-    // create one new row (cube)
-    pCubeNew = Fxu_MatrixAddCube( p, pVarD, 0 );
-    pCubeNew->pFirst = pCubeNew;
-    // set the first cube of the positive var
-    pVarD->pFirst = pCubeNew;
-
-    // start collecting the affected vars and cubes
-    Fxu_MatrixRingCubesStart( p );
-    Fxu_MatrixRingVarsStart( p );
-    // add the vars
-    Fxu_MatrixRingVarsAdd( p, pVar1 );
-    Fxu_MatrixRingVarsAdd( p, pVar2 );
-    // remove the literals and collect the affected cubes
-    // remove the divisors associated with this cube
-       // add to the affected cube the literal corresponding to the new column
-    Fxu_UpdateMatrixSingleClean( p, pVar1, pVar2, pVarD );
-    // replace each two cubes of the pair by one new cube
-    // the new cube contains the base and the new literal
-    Fxu_UpdateDoublePairs( p, pDouble, pVarC );
-    // stop collecting the affected vars and cubes
-    Fxu_MatrixRingCubesStop( p );
-    Fxu_MatrixRingVarsStop( p );
-
-    // add the literals to the new cube
-    assert( pVar1->iVar < pVar2->iVar );
-    assert( Fxu_SingleCountCoincidence( p, pVar1, pVar2 ) == 0 );
-    Fxu_MatrixAddLiteral( p, pCubeNew, pVar1 );
-    Fxu_MatrixAddLiteral( p, pCubeNew, pVar2 );
-
-    // create new doubles; we cannot add them in the same loop
-    // because we first have to create *all* new cubes for each node
-    Fxu_MatrixForEachCubeInRing( p, pCube )
-           Fxu_UpdateAddNewDoubles( p, pCube );
-    // update the singles after removing some literals
-    Fxu_UpdateCleanOldSingles( p );
-
-    // undo the temporary rings with cubes and vars
-    Fxu_MatrixRingCubesUnmark( p );
-    Fxu_MatrixRingVarsUnmark( p );
-    // we should undo the rings before creating new singles
-
-    // create new singles
-    Fxu_UpdateAddNewSingles( p, pVarC );
-    Fxu_UpdateAddNewSingles( p, pVarD );
-
-    // recycle the divisor
-    MEM_FREE_FXU( p, Fxu_Double, 1, pDouble );
-    p->nDivs3++;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Updates after accepting single cube divisor.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_UpdateSingle( Fxu_Matrix * p )
-{
-    Fxu_Single * pSingle;
-    Fxu_Cube * pCube, * pCubeNew;
-    Fxu_Var * pVarC, * pVarD;
-    Fxu_Var * pVar1, * pVar2;
-
-    // read the best divisor from the heap
-    pSingle = Fxu_HeapSingleReadMax( p->pHeapSingle );
-    // get the variables of this single-cube divisor
-    pVar1 = pSingle->pVar1;
-    pVar2 = pSingle->pVar2;
-
-    // create two new columns (vars)
-    Fxu_UpdateCreateNewVars( p, &pVarC, &pVarD, 1 );
-    // create one new row (cube)
-    pCubeNew = Fxu_MatrixAddCube( p, pVarD, 0 );
-    pCubeNew->pFirst = pCubeNew;
-    // set the first cube
-    pVarD->pFirst = pCubeNew;
-
-    // start collecting the affected vars and cubes
-    Fxu_MatrixRingCubesStart( p );
-    Fxu_MatrixRingVarsStart( p );
-    // add the vars
-    Fxu_MatrixRingVarsAdd( p, pVar1 );
-    Fxu_MatrixRingVarsAdd( p, pVar2 );
-    // remove the literals and collect the affected cubes
-    // remove the divisors associated with this cube
-       // add to the affected cube the literal corresponding to the new column
-    Fxu_UpdateMatrixSingleClean( p, pVar1, pVar2, pVarD );
-    // stop collecting the affected vars and cubes
-    Fxu_MatrixRingCubesStop( p );
-    Fxu_MatrixRingVarsStop( p );
-
-    // add the literals to the new cube
-    assert( pVar1->iVar < pVar2->iVar );
-    assert( Fxu_SingleCountCoincidence( p, pVar1, pVar2 ) == 0 );
-    Fxu_MatrixAddLiteral( p, pCubeNew, pVar1 );
-    Fxu_MatrixAddLiteral( p, pCubeNew, pVar2 );
-
-    // create new doubles; we cannot add them in the same loop
-    // because we first have to create *all* new cubes for each node
-    Fxu_MatrixForEachCubeInRing( p, pCube )
-           Fxu_UpdateAddNewDoubles( p, pCube );
-    // update the singles after removing some literals
-    Fxu_UpdateCleanOldSingles( p );
-    // we should undo the rings before creating new singles
-
-    // unmark the cubes
-    Fxu_MatrixRingCubesUnmark( p );
-    Fxu_MatrixRingVarsUnmark( p );
-
-    // create new singles
-    Fxu_UpdateAddNewSingles( p, pVarC );
-    Fxu_UpdateAddNewSingles( p, pVarD );
-    p->nDivs1++;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Updates the matrix after accepting a double cube divisor.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_UpdateDouble( Fxu_Matrix * p )
-{
-    Fxu_Double * pDiv;
-    Fxu_Cube * pCube, * pCubeNew1, * pCubeNew2;
-    Fxu_Var * pVarC, * pVarD;
-
-    // remove the best divisor from the heap
-    pDiv = Fxu_HeapDoubleGetMax( p->pHeapDouble );
-    // remove the best divisor from the table
-    Fxu_ListTableDelDivisor( p, pDiv );
-
-    // create two new columns (vars)
-    Fxu_UpdateCreateNewVars( p, &pVarC, &pVarD, 2 );
-    // create two new rows (cubes)
-    pCubeNew1 = Fxu_MatrixAddCube( p, pVarD, 0 );
-    pCubeNew1->pFirst = pCubeNew1;
-    pCubeNew2 = Fxu_MatrixAddCube( p, pVarD, 1 );
-    pCubeNew2->pFirst = pCubeNew1;
-    // set the first cube
-    pVarD->pFirst = pCubeNew1;
-
-    // add the literals to the new cubes
-    Fxu_UpdateMatrixDoubleCreateCubes( p, pCubeNew1, pCubeNew2, pDiv );
-
-    // start collecting the affected cubes and vars
-    Fxu_MatrixRingCubesStart( p );
-    Fxu_MatrixRingVarsStart( p );
-    // replace each two cubes of the pair by one new cube
-    // the new cube contains the base and the new literal
-    Fxu_UpdateDoublePairs( p, pDiv, pVarD );
-    // stop collecting the affected cubes and vars
-    Fxu_MatrixRingCubesStop( p );
-    Fxu_MatrixRingVarsStop( p );
-    
-    // create new doubles; we cannot add them in the same loop
-    // because we first have to create *all* new cubes for each node
-    Fxu_MatrixForEachCubeInRing( p, pCube )
-           Fxu_UpdateAddNewDoubles( p, pCube );
-    // update the singles after removing some literals
-    Fxu_UpdateCleanOldSingles( p );
-
-    // undo the temporary rings with cubes and vars
-    Fxu_MatrixRingCubesUnmark( p );
-    Fxu_MatrixRingVarsUnmark( p );
-    // we should undo the rings before creating new singles
-
-    // create new singles
-    Fxu_UpdateAddNewSingles( p, pVarC );
-    Fxu_UpdateAddNewSingles( p, pVarD );
-
-    // recycle the divisor
-    MEM_FREE_FXU( p, Fxu_Double, 1, pDiv );
-    p->nDivs2++;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Update the pairs.]
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_UpdateDoublePairs( Fxu_Matrix * p, Fxu_Double * pDouble, Fxu_Var * pVar )
-{
-    Fxu_Pair * pPair;
-    Fxu_Cube * pCubeUse, * pCubeRem;
-    int i;
-
-    // collect and sort the pairs
-    Fxu_UpdatePairsSort( p, pDouble );
-//    for ( i = 0; i < p->nPairsTemp; i++ )
-    for ( i = 0; i < p->vPairs->nSize; i++ )
-    {
-        // get the pair
-//        pPair = p->pPairsTemp[i];
-        pPair = p->vPairs->pArray[i];
-        // out of the two cubes, select the one which comes earlier
-        pCubeUse = Fxu_PairMinCube( pPair );
-        pCubeRem = Fxu_PairMaxCube( pPair );
-        // collect the affected cube
-        assert( pCubeUse->pOrder == NULL );
-        Fxu_MatrixRingCubesAdd( p, pCubeUse );
-
-        // remove some literals from pCubeUse and all literals from pCubeRem
-        Fxu_UpdateMatrixDoubleClean( p, pCubeUse, pCubeRem );
-        // add a literal that depends on the new variable
-        Fxu_MatrixAddLiteral( p, pCubeUse, pVar );    
-        // check the literal count
-        assert( pCubeUse->lLits.nItems == pPair->nBase + 1 );
-        assert( pCubeRem->lLits.nItems == 0 );
-
-        // update the divisors by removing useless pairs
-        Fxu_UpdateCleanOldDoubles( p, pDouble, pCubeUse );
-        Fxu_UpdateCleanOldDoubles( p, pDouble, pCubeRem );
-        // remove the pair
-        MEM_FREE_FXU( p, Fxu_Pair, 1, pPair );
-    }
-    p->vPairs->nSize = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Add two cubes corresponding to the given double-cube divisor.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_UpdateMatrixDoubleCreateCubes( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2, Fxu_Double * pDiv )
-{
-    Fxu_Lit * pLit1, * pLit2;
-    Fxu_Pair * pPair;
-    int nBase, nLits1, nLits2;
-
-    // fill in the SOP and copy the fanins
-    nBase = nLits1 = nLits2 = 0;
-    pPair = pDiv->lPairs.pHead;
-    pLit1 = pPair->pCube1->lLits.pHead;
-    pLit2 = pPair->pCube2->lLits.pHead;
-    while ( 1 )
-    {
-        if ( pLit1 && pLit2 )
-        {
-            if ( pLit1->iVar == pLit2->iVar )
-            { // skip the cube free part
-                pLit1 = pLit1->pHNext;
-                pLit2 = pLit2->pHNext;
-                nBase++;
-            }
-            else if ( pLit1->iVar < pLit2->iVar )
-            {    // add literal to the first cube
-                Fxu_MatrixAddLiteral( p, pCube1, pLit1->pVar );
-                // move to the next literal in this cube
-                pLit1 = pLit1->pHNext;
-                nLits1++;
-            }
-            else
-            {    // add literal to the second cube
-                Fxu_MatrixAddLiteral( p, pCube2, pLit2->pVar );
-                // move to the next literal in this cube
-                pLit2 = pLit2->pHNext;
-                nLits2++;
-            }
-        }
-        else if ( pLit1 && !pLit2 )
-        {    // add literal to the first cube
-            Fxu_MatrixAddLiteral( p, pCube1, pLit1->pVar );
-            // move to the next literal in this cube
-            pLit1 = pLit1->pHNext;
-            nLits1++;
-        }
-        else if ( !pLit1 && pLit2 )
-        {    // add literal to the second cube
-            Fxu_MatrixAddLiteral( p, pCube2, pLit2->pVar );
-            // move to the next literal in this cube
-            pLit2 = pLit2->pHNext;
-            nLits2++;
-        }
-        else
-            break;
-    }
-    assert( pPair->nLits1 == nLits1 );
-    assert( pPair->nLits2 == nLits2 );
-    assert( pPair->nBase == nBase );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Create the node equal to double-cube divisor.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_UpdateMatrixDoubleClean( Fxu_Matrix * p, Fxu_Cube * pCubeUse, Fxu_Cube * pCubeRem )
-{
-    Fxu_Lit * pLit1, * bLit1Next;
-    Fxu_Lit * pLit2, * bLit2Next;
-
-    // initialize the starting literals
-    pLit1     = pCubeUse->lLits.pHead;
-    pLit2     = pCubeRem->lLits.pHead;
-    bLit1Next = pLit1? pLit1->pHNext: NULL;
-    bLit2Next = pLit2? pLit2->pHNext: NULL;
-    // go through the pair and remove the literals in the base
-    // from the first cube and all literals from the second cube
-    while ( 1 )
-    {
-        if ( pLit1 && pLit2 )
-        {
-            if ( pLit1->iVar == pLit2->iVar )
-            {  // this literal is present in both cubes - it belongs to the base
-                // mark the affected var
-                if ( pLit1->pVar->pOrder == NULL )
-                    Fxu_MatrixRingVarsAdd( p, pLit1->pVar );
-                // leave the base in pCubeUse; delete it from pCubeRem
-                Fxu_MatrixDelLiteral( p, pLit2 );
-                // step to the next literals
-                pLit1     = bLit1Next;
-                pLit2     = bLit2Next;
-                bLit1Next = pLit1? pLit1->pHNext: NULL;
-                bLit2Next = pLit2? pLit2->pHNext: NULL;
-            }
-            else if ( pLit1->iVar < pLit2->iVar )
-            { // this literal is present in pCubeUse - remove it
-                // mark the affected var
-                if ( pLit1->pVar->pOrder == NULL )
-                    Fxu_MatrixRingVarsAdd( p, pLit1->pVar );
-                // delete this literal
-                Fxu_MatrixDelLiteral( p, pLit1 );
-                // step to the next literals
-                pLit1     = bLit1Next;
-                bLit1Next = pLit1? pLit1->pHNext: NULL;
-            }
-            else
-            { // this literal is present in pCubeRem - remove it
-                // mark the affected var
-                if ( pLit2->pVar->pOrder == NULL )
-                    Fxu_MatrixRingVarsAdd( p, pLit2->pVar );
-                // delete this literal
-                Fxu_MatrixDelLiteral( p, pLit2 );
-                // step to the next literals
-                pLit2     = bLit2Next;
-                bLit2Next = pLit2? pLit2->pHNext: NULL;
-            }
-        }
-        else if ( pLit1 && !pLit2 )
-        { // this literal is present in pCubeUse - leave it
-            // mark the affected var
-            if ( pLit1->pVar->pOrder == NULL )
-                Fxu_MatrixRingVarsAdd( p, pLit1->pVar );
-            // delete this literal
-            Fxu_MatrixDelLiteral( p, pLit1 );
-            // step to the next literals
-            pLit1     = bLit1Next;
-            bLit1Next = pLit1? pLit1->pHNext: NULL;
-        }
-        else if ( !pLit1 && pLit2 )
-        { // this literal is present in pCubeRem - remove it
-            // mark the affected var
-            if ( pLit2->pVar->pOrder == NULL )
-                Fxu_MatrixRingVarsAdd( p, pLit2->pVar );
-            // delete this literal
-            Fxu_MatrixDelLiteral( p, pLit2 );
-            // step to the next literals
-            pLit2     = bLit2Next;
-            bLit2Next = pLit2? pLit2->pHNext: NULL;
-        }
-        else
-            break;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Updates the matrix after selecting a single cube divisor.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_UpdateMatrixSingleClean( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVar2, Fxu_Var * pVarNew )
-{
-    Fxu_Lit * pLit1, * bLit1Next;
-    Fxu_Lit * pLit2, * bLit2Next;
-
-    // initialize the starting literals
-    pLit1     = pVar1->lLits.pHead;
-    pLit2     = pVar2->lLits.pHead;
-    bLit1Next = pLit1? pLit1->pVNext: NULL;
-    bLit2Next = pLit2? pLit2->pVNext: NULL;
-    while ( 1 )
-    {
-        if ( pLit1 && pLit2 )
-        {
-            if ( pLit1->pCube->pVar->iVar == pLit2->pCube->pVar->iVar )
-            { // these literals coincide 
-                if ( pLit1->iCube == pLit2->iCube )
-                { // these literals coincide 
-                
-                    // collect the affected cube
-                    assert( pLit1->pCube->pOrder == NULL );
-                    Fxu_MatrixRingCubesAdd( p, pLit1->pCube );
-
-                    // add the literal to this cube corresponding to the new column
-                    Fxu_MatrixAddLiteral( p, pLit1->pCube, pVarNew );
-                    // clean the old cubes
-                    Fxu_UpdateCleanOldDoubles( p, NULL, pLit1->pCube );
-
-                    // remove the literals 
-                    Fxu_MatrixDelLiteral( p, pLit1 );
-                    Fxu_MatrixDelLiteral( p, pLit2 );
-
-                    // go to the next literals
-                    pLit1     = bLit1Next;
-                    pLit2     = bLit2Next;
-                    bLit1Next = pLit1? pLit1->pVNext: NULL;
-                    bLit2Next = pLit2? pLit2->pVNext: NULL;
-                }
-                else if ( pLit1->iCube < pLit2->iCube )
-                {
-                    pLit1     = bLit1Next;
-                    bLit1Next = pLit1? pLit1->pVNext: NULL;
-                }
-                else
-                {
-                    pLit2     = bLit2Next;
-                    bLit2Next = pLit2? pLit2->pVNext: NULL;
-                }
-            }
-            else if ( pLit1->pCube->pVar->iVar < pLit2->pCube->pVar->iVar )
-            {
-                pLit1     = bLit1Next;
-                bLit1Next = pLit1? pLit1->pVNext: NULL;
-            }
-            else
-            {
-                pLit2     = bLit2Next;
-                bLit2Next = pLit2? pLit2->pVNext: NULL;
-            }
-        }
-        else if ( pLit1 && !pLit2 )
-        {
-            pLit1     = bLit1Next;
-            bLit1Next = pLit1? pLit1->pVNext: NULL;
-        }
-        else if ( !pLit1 && pLit2 )
-        {
-            pLit2     = bLit2Next;
-            bLit2Next = pLit2? pLit2->pVNext: NULL;
-        }
-        else
-            break;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sort the pairs.]
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_UpdatePairsSort( Fxu_Matrix * p, Fxu_Double * pDouble )
-{
-    Fxu_Pair * pPair;
-    // order the pairs by the first cube to ensure that new literals are added 
-    // to the matrix from top to bottom - collect pairs into the array
-    p->vPairs->nSize = 0;
-    Fxu_DoubleForEachPair( pDouble, pPair )
-        Vec_PtrPush( p->vPairs, pPair );
-    if ( p->vPairs->nSize < 2 )
-        return;
-    // sort
-    qsort( (void *)p->vPairs->pArray, p->vPairs->nSize, sizeof(Fxu_Pair *), 
-        (int (*)(const void *, const void *)) Fxu_UpdatePairCompare );
-    assert( Fxu_UpdatePairCompare( (Fxu_Pair**)p->vPairs->pArray, (Fxu_Pair**)p->vPairs->pArray + p->vPairs->nSize - 1 ) < 0 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Compares the vars by their number.]
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fxu_UpdatePairCompare( Fxu_Pair ** ppP1, Fxu_Pair ** ppP2 )
-{
-    Fxu_Cube * pC1 = (*ppP1)->pCube1;
-    Fxu_Cube * pC2 = (*ppP2)->pCube1;
-    int iP1CubeMin, iP2CubeMin;
-    if ( pC1->pVar->iVar < pC2->pVar->iVar )
-        return -1;
-    if ( pC1->pVar->iVar > pC2->pVar->iVar )
-        return 1;
-    iP1CubeMin = Fxu_PairMinCubeInt( *ppP1 );
-    iP2CubeMin = Fxu_PairMinCubeInt( *ppP2 );
-    if ( iP1CubeMin < iP2CubeMin )
-        return -1;
-    if ( iP1CubeMin > iP2CubeMin )
-        return 1;
-    assert( 0 );
-    return 0;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Create new variables.]
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_UpdateCreateNewVars( Fxu_Matrix * p, Fxu_Var ** ppVarC, Fxu_Var ** ppVarD, int nCubes )
-{
-    Fxu_Var * pVarC, * pVarD;
-
-    // add a new column for the complement
-    pVarC = Fxu_MatrixAddVar( p );
-    pVarC->nCubes = 0;
-    // add a new column for the divisor
-    pVarD = Fxu_MatrixAddVar( p );
-    pVarD->nCubes = nCubes;
-
-    // mark this entry in the Value2Node array
-//    assert( p->pValue2Node[pVarC->iVar] > 0 );
-//    p->pValue2Node[pVarD->iVar  ] = p->pValue2Node[pVarC->iVar];
-//    p->pValue2Node[pVarD->iVar+1] = p->pValue2Node[pVarC->iVar]+1;
-
-    *ppVarC = pVarC;
-    *ppVarD = pVarD;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_UpdateCleanOldDoubles( Fxu_Matrix * p, Fxu_Double * pDiv, Fxu_Cube * pCube )
-{
-    Fxu_Double * pDivCur;
-    Fxu_Pair * pPair;
-    int i;
-
-    // if the cube is a recently introduced one
-    // it does not have pairs allocated
-    // in this case, there is nothing to update
-    if ( pCube->pVar->ppPairs == NULL )
-        return;
-
-    // go through all the pairs of this cube
-    Fxu_CubeForEachPair( pCube, pPair, i )
-    {
-         // get the divisor of this pair
-        pDivCur = pPair->pDiv;
-        // skip the current divisor
-        if ( pDivCur == pDiv )
-            continue;
-        // remove this pair
-        Fxu_ListDoubleDelPair( pDivCur, pPair );    
-        // the divisor may have become useless by now
-        if ( pDivCur->lPairs.nItems == 0 )
-        {
-            assert( pDivCur->Weight == pPair->nBase - 1 );
-              Fxu_HeapDoubleDelete( p->pHeapDouble, pDivCur );
-            Fxu_MatrixDelDivisor( p, pDivCur );
-        }
-        else
-        {
-            // update the divisor's weight
-            pDivCur->Weight -= pPair->nLits1 + pPair->nLits2 - 1 + pPair->nBase;
-              Fxu_HeapDoubleUpdate( p->pHeapDouble, pDivCur );
-        }
-        MEM_FREE_FXU( p, Fxu_Pair, 1, pPair );
-    }
-    // finally erase all the pair info associated with this cube
-    Fxu_PairClearStorage( pCube );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds the new divisors that depend on the cube.]
-
-  Description [Go through all the non-empty cubes of this cover 
-  (except the given cube) and, for each of them, add the new divisor 
-  with the given cube.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_UpdateAddNewDoubles( Fxu_Matrix * p, Fxu_Cube * pCube )
-{
-    Fxu_Cube * pTemp;
-    assert( pCube->pOrder );
-
-    // if the cube is a recently introduced one
-    // it does not have pairs allocated
-    // in this case, there is nothing to update
-    if ( pCube->pVar->ppPairs == NULL )
-        return;
-
-    for ( pTemp = pCube->pFirst; pTemp->pVar == pCube->pVar; pTemp = pTemp->pNext )
-    {
-        // do not add pairs with the empty cubes
-        if ( pTemp->lLits.nItems == 0 )
-            continue;
-        // to prevent adding duplicated pairs of the new cubes
-        // do not add the pair, if the current cube is marked 
-        if ( pTemp->pOrder && pTemp >= pCube )
-            continue;
-        Fxu_MatrixAddDivisor( p, pTemp, pCube );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Removes old single cube divisors.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_UpdateCleanOldSingles( Fxu_Matrix * p )
-{ 
-    Fxu_Single * pSingle, * pSingle2;
-    int WeightNew;
-    int Counter = 0;
-
-    Fxu_MatrixForEachSingleSafe( p, pSingle, pSingle2 )
-    {
-        // if at least one of the variables is marked, recalculate
-        if ( pSingle->pVar1->pOrder || pSingle->pVar2->pOrder )
-        {
-            Counter++;
-            // get the new weight
-            WeightNew = -2 + Fxu_SingleCountCoincidence( p, pSingle->pVar1, pSingle->pVar2 );
-            if ( WeightNew >= 0 )
-            {
-                pSingle->Weight = WeightNew;
-                Fxu_HeapSingleUpdate( p->pHeapSingle, pSingle );
-            }
-            else
-            {
-                Fxu_HeapSingleDelete( p->pHeapSingle, pSingle );
-                Fxu_ListMatrixDelSingle( p, pSingle );
-                MEM_FREE_FXU( p, Fxu_Single, 1, pSingle );
-            }
-        }
-    }
-//    printf( "Called procedure %d times.\n", Counter );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Updates the single cube divisors.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fxu_UpdateAddNewSingles( Fxu_Matrix * p, Fxu_Var * pVar )
-{
-    Fxu_MatrixComputeSinglesOne( p, pVar );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/fxu/module.make b/src/opt/fxu/module.make
deleted file mode 100644
index dd8acd40..00000000
--- a/src/opt/fxu/module.make
+++ /dev/null
@@ -1,12 +0,0 @@
-SRC +=  src/opt/fxu/fxu.c \
-    src/opt/fxu/fxuCreate.c \
-    src/opt/fxu/fxuHeapD.c \
-    src/opt/fxu/fxuHeapS.c \
-    src/opt/fxu/fxuList.c \
-    src/opt/fxu/fxuMatrix.c \
-    src/opt/fxu/fxuPair.c \
-    src/opt/fxu/fxuPrint.c \
-    src/opt/fxu/fxuReduce.c \
-    src/opt/fxu/fxuSelect.c \
-    src/opt/fxu/fxuSingle.c \
-    src/opt/fxu/fxuUpdate.c