| /**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 | |