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