luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
abc/src/opt/fxu/fxuUpdate.c

812 lines
26 KiB
C
Raw Blame History

/**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, (size_t)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
Reference in New Issue View Git Blame Copy Permalink