/**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" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// 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 = (Fxu_Pair *)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->iCube >= pCube->iCube ) 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 /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END