Version abc50806

15 files changed, 5654 insertions, 0 deletions

diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c
new file mode 100644
index 00000000..4b95b5a5
--- /dev/null
+++ b/src/opt/fxu/fxu.c
@@ -0,0 +1,260 @@
+/**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 "mvc.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 DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fast_extract on a set of covers.]
+
+  Description [All the covers are given in the array p->ppCovers. 
+  The resulting covers are returned in the array p->ppCoversNew.
+  The number of entries in both cover arrays is equal to the number
+  of all values in the current nodes plus the max expected number 
+  of extracted nodes (p->nValuesCi + p->nValuesInt + p->nValuesExtMax). 
+  The first p->nValuesCi entries, corresponding to the CI nodes, are NULL.
+  The next p->nValuesInt entries, corresponding to the int nodes, are covers
+  from which the divisors are extracted. The last p->nValuesExtMax entries  
+  are reserved for the new covers to be extracted. The number of extracted 
+  covers is returned. This number does not exceed the given number (p->nNodesExt). 
+  Two other things are important for the correct operation of this procedure:
+  (1) The input covers should be SCC-free. (2) The literal array (pCover->pLits) 
+  is allocated in each cover. The i-th entry in the literal array of a cover
+  is the number of the cover in the array p->ppCovers, which represents this
+  literal (variable value) in the given cover.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fxu_FastExtract( Fxu_Data_t * pData )
+{
+    Fxu_Matrix * p;
+    Fxu_Single * pSingle;
+    Fxu_Double * pDouble;
+    int Weight1, Weight2, Weight3;
+
+    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( "Best single = %3d.\n", 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( "Best double = %3d.\n", 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( "Best double = %3d. Best single = %3d.\n", 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( "Best double = %3d. Best single = %3d. Best complement = %3d.\n", 
+                    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 delocation:   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
new file mode 100644
index 00000000..5bc1e75f
--- /dev/null
+++ b/src/opt/fxu/fxu.h
@@ -0,0 +1,108 @@
+/**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__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "vec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+#ifndef bool
+#define bool int
+#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               nPairsMax;        // the maximum number of cube pairs to consider
+/*
+    // parameters of the network
+    int               fMvNetwork;       // the network has some MV nodes
+    // the information about nodes
+    int               nNodesCi;         // the number of CI nodes of the network
+    int               nNodesInt;        // the number of internal nodes of the network
+    int               nNodesOld;        // the number of CI and int nodes
+    int               nNodesNew;        // the number of added nodes
+    int               nNodesExt;        // the max number of (binary) nodes to be added by FX
+    int               nNodesAlloc;      // the total number of all nodes
+    int *             pNode2Value;      // for each node, the number of its first value
+    // the information about values
+    int               nValuesCi;        // the total number of values of CI nodes
+    int               nValuesInt;       // the total number of values of int nodes
+    int               nValuesOld;       // the number of CI and int values
+    int               nValuesNew;       // the number of values added nodes
+    int               nValuesExt;       // the total number of values of the added nodes
+    int               nValuesAlloc;     // the total number of all values of all nodes
+    int *             pValue2Node;      // for each value, the number of its node
+    // the information about covers
+    Mvc_Cover_t **    ppCovers;         // for each value, the corresponding cover
+    Mvc_Cover_t **    ppCoversNew;      // for each value, the corresponding cover after FX
+    // the MVC manager
+    Mvc_Manager_t *   pManMvc;
+*/
+    // statistics   
+    int               nNodesOld;        // the old number of nodes
+    int               nNodesExt;        // the number of divisors to extract
+    int               nNodesNew;        // the number of divisors extracted
+
+    // 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;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                       MACRO DEFITIONS                            ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/*===== fxu.c ==========================================================*/
+extern int          Fxu_FastExtract( Fxu_Data_t * pData );
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c
new file mode 100644
index 00000000..04b23fce
--- /dev/null
+++ b/src/opt/fxu/fxuCreate.c
@@ -0,0 +1,425 @@
+/**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                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern int         Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax );
+
+static void        Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Fan_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 Abc_Fan_t * s_pLits;
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the sparse matrix from the array of Sop covers.]
+
+  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;
+    char * pSopCover;
+    char * pSopCube;
+    int * pOrder, nBitsMax;
+    int i, v, c;
+    int nCubesTotal;
+    int nPairsTotal;
+    int nPairsStore;
+    int nCubes;
+    int iCube, iPair;
+    int nFanins;
+    Vec_Fan_t * vFanins;
+
+    // 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] ].iFan < s_pLits[ pOrder[nFanins-1] ].iFan );
+        // 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;
+            c++;
+        }
+        // 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 ( nPairsTotal > pData->nPairsMax )
+        Fxu_PreprocessCubePairs( p, pData->vSops, nPairsTotal, pData->nPairsMax );
+
+    // add the var pairs to the heap
+    Fxu_MatrixComputeSingles( p );
+
+    // allocate temporary storage for pairs
+    if ( pData->nPairsMax < 1000 )
+        pData->nPairsMax = 1000;
+    p->pPairsTemp = ALLOC( Fxu_Pair *, pData->nPairsMax * 10 + 100 );
+    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 divisors = %6d.  ",  p->lSingles.nItems );
+        fprintf( stdout, "2-cube divisors = %6d.  ",  p->nDivsTotal );
+        fprintf( stdout, "Cube pairs = %6d.",    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_Fan_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]].iFan + 1 ];  // CST
+            Fxu_MatrixAddLiteral( p, pCube, pVar );
+        }
+        else if ( Value == '1' )
+        {
+            pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]].iFan ];  // 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;
+    int iNode, n;
+    char * pSopCover;
+
+    // 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;
+    char * pSopCube;
+    Fxu_Var * pVar;
+    Fxu_Cube * pCube;
+    Fxu_Lit * pLit;
+    int iNum, nCubes, v;
+    int fEmptyCube;
+
+    // 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
+        fEmptyCube = 1;
+        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
+            fEmptyCube = 0;
+        }
+        assert( !fEmptyCube );
+        // count the cube
+        nCubes++;
+    }
+    assert( nCubes == Abc_SopGetCubeNum(pSopCover) );
+
+    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].iFan - s_pLits[*ptrY].iFan;
+} 
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/fxu/fxuHeapD.c b/src/opt/fxu/fxuHeapD.c
new file mode 100644
index 00000000..7c123249
--- /dev/null
+++ b/src/opt/fxu/fxuHeapD.c
@@ -0,0 +1,445 @@
+/**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 DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**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
new file mode 100644
index 00000000..dbd66055
--- /dev/null
+++ b/src/opt/fxu/fxuHeapS.c
@@ -0,0 +1,444 @@
+/**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 DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**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
new file mode 100644
index 00000000..1f5a19b8
--- /dev/null
+++ b/src/opt/fxu/fxuInt.h
@@ -0,0 +1,541 @@
+/**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 "util.h"
+#include "extra.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
+{
+    // information about the network
+//    int              fMvNetwork;  // set to 1 if the network has MV nodes
+//    int *            pValue2Node; // the mapping of values into nodes
+    // 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
+    // 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
+    Fxu_Pair **      pPairsTemp;
+    int              nPairsTemp;
+//    int              nPairsMax;
+    // 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 DEFITIONS                            ///
+////////////////////////////////////////////////////////////////////////
+
+// 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 DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/*===== 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 );
+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 );  
+
+////////////////////////////////////////////////////////////////////////
+///                         END OF FILE                              ///
+////////////////////////////////////////////////////////////////////////
+#endif
+
diff --git a/src/opt/fxu/fxuList.c b/src/opt/fxu/fxuList.c
new file mode 100644
index 00000000..bb081d80
--- /dev/null
+++ b/src/opt/fxu/fxuList.c
@@ -0,0 +1,522 @@
+/**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 DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+// 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
new file mode 100644
index 00000000..0b732aef
--- /dev/null
+++ b/src/opt/fxu/fxuMatrix.c
@@ -0,0 +1,382 @@
+/**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 DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**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();
+    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, 0 );
+#endif
+
+    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
+    if ( p->fMvNetwork )
+//    if ( 0 )
+    {   // in case of MV network, if all the values in the cube-free divisor
+        // belong to the same MV variable, this cube pair is not a divisor
+        Key = Fxu_PairHashKeyMv( p, pCube1, pCube2, &nBase, &nLits1, &nLits2 );
+        if ( Key == 0 )
+            return;
+    }
+    else
+*/
+        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
new file mode 100644
index 00000000..be6be5e9
--- /dev/null
+++ b/src/opt/fxu/fxuPair.c
@@ -0,0 +1,555 @@
+/**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 DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**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
new file mode 100644
index 00000000..2d25c0e9
--- /dev/null
+++ b/src/opt/fxu/fxuPrint.c
@@ -0,0 +1,195 @@
+/**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 DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**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
new file mode 100644
index 00000000..652d807b
--- /dev/null
+++ b/src/opt/fxu/fxuReduce.c
@@ -0,0 +1,194 @@
+/**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 DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**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
+    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
new file mode 100644
index 00000000..b56407a9
--- /dev/null
+++ b/src/opt/fxu/fxuSelect.c
@@ -0,0 +1,603 @@
+/**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 DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**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
new file mode 100644
index 00000000..5af5c341
--- /dev/null
+++ b/src/opt/fxu/fxuSingle.c
@@ -0,0 +1,166 @@
+/**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"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**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 )
+{
+    Fxu_Var * pVar;
+    // iterate through the columns in the matrix
+    Fxu_MatrixForEachVariable( p, pVar )
+        Fxu_MatrixComputeSinglesOne( p, pVar );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the single-cube divisors associated with a new column.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar )
+{
+//    int * pValue2Node = p->pValue2Node;
+    Fxu_Lit * pLitV, * pLitH;
+    Fxu_Var * pVar2;
+    int Coin;
+//    int CounterAll;
+//    int CounterTest;
+    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;
+//            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[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 )
+    {
+//        CounterTest++;
+        // count the coincidence
+        Coin = Fxu_SingleCountCoincidence( p, pVar2, pVar );
+        assert( Coin > 0 );
+        // get the new weight
+        WeightCur = Coin - 2;
+        if ( WeightCur >= 0 )
+            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
new file mode 100644
index 00000000..b781e0b1
--- /dev/null
+++ b/src/opt/fxu/fxuUpdate.c
@@ -0,0 +1,802 @@
+/**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 DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**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++ )
+    {
+        // get the pair
+        pPair = p->pPairsTemp[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->nPairsTemp = 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->nPairsTemp = 0;
+    Fxu_DoubleForEachPair( pDouble, pPair )
+        p->pPairsTemp[ p->nPairsTemp++ ] = pPair;
+    if ( p->nPairsTemp > 1 )
+    {   // sort
+        qsort( (void *)p->pPairsTemp, p->nPairsTemp, sizeof(Fxu_Pair *), 
+            (int (*)(const void *, const void *)) Fxu_UpdatePairCompare );
+        assert( Fxu_UpdatePairCompare( p->pPairsTemp, p->pPairsTemp + p->nPairsTemp - 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;
+
+    Fxu_MatrixForEachSingleSafe( p, pSingle, pSingle2 )
+    {
+        // if at least one of the variables is marked, recalculate
+        if ( pSingle->pVar1->pOrder || pSingle->pVar2->pOrder )
+        {
+            // 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 );
+            }
+        }
+    }
+}
+
+/**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
new file mode 100644
index 00000000..331712d1
--- /dev/null
+++ b/src/opt/fxu/module.make
@@ -0,0 +1,12 @@
+SRC +=  fxu.c \
+    fxuCreate.c \
+    fxuHeapD.c \
+    fxuHeapS.c \
+    fxuList.c \
+    fxuMatrix.c \
+    fxuPair.c \
+    fxuPrint.c \
+    fxuReduce.c \
+    fxuSelect.c \
+    fxuSingle.c \
+    fxuUpdate.c