From d0e834d1a615f8e0e9d04c2ac97811f63562bd0b Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sat, 6 Aug 2005 08:01:00 -0700
Subject: Version abc50806
---
src/opt/fxu/fxu.c | 260 ++++++++++++++++
src/opt/fxu/fxu.h | 108 +++++++
src/opt/fxu/fxuCreate.c | 425 +++++++++++++++++++++++++
src/opt/fxu/fxuHeapD.c | 445 +++++++++++++++++++++++++++
src/opt/fxu/fxuHeapS.c | 444 +++++++++++++++++++++++++++
src/opt/fxu/fxuInt.h | 541 ++++++++++++++++++++++++++++++++
src/opt/fxu/fxuList.c | 522 +++++++++++++++++++++++++++++++
src/opt/fxu/fxuMatrix.c | 382 +++++++++++++++++++++++
src/opt/fxu/fxuPair.c | 555 +++++++++++++++++++++++++++++++++
src/opt/fxu/fxuPrint.c | 195 ++++++++++++
src/opt/fxu/fxuReduce.c | 194 ++++++++++++
src/opt/fxu/fxuSelect.c | 603 ++++++++++++++++++++++++++++++++++++
src/opt/fxu/fxuSingle.c | 166 ++++++++++
src/opt/fxu/fxuUpdate.c | 802 ++++++++++++++++++++++++++++++++++++++++++++++++
src/opt/fxu/module.make | 12 +
15 files changed, 5654 insertions(+)
create mode 100644 src/opt/fxu/fxu.c
create mode 100644 src/opt/fxu/fxu.h
create mode 100644 src/opt/fxu/fxuCreate.c
create mode 100644 src/opt/fxu/fxuHeapD.c
create mode 100644 src/opt/fxu/fxuHeapS.c
create mode 100644 src/opt/fxu/fxuInt.h
create mode 100644 src/opt/fxu/fxuList.c
create mode 100644 src/opt/fxu/fxuMatrix.c
create mode 100644 src/opt/fxu/fxuPair.c
create mode 100644 src/opt/fxu/fxuPrint.c
create mode 100644 src/opt/fxu/fxuReduce.c
create mode 100644 src/opt/fxu/fxuSelect.c
create mode 100644 src/opt/fxu/fxuSingle.c
create mode 100644 src/opt/fxu/fxuUpdate.c
create mode 100644 src/opt/fxu/module.make
(limited to 'src/opt')
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
--
cgit v1.2.3