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