fxuupdate.c

主要进行大规模的电路综合

	Fxu_Lit * pLit2, * bLit2Next;

	// initialize the starting literals
	pLit1     = pCubeUse->lLits.pHead;
	pLit2     = pCubeRem->lLits.pHead;
	bLit1Next = pLit1? pLit1->pHNext: NULL;
	bLit2Next = pLit2? pLit2->pHNext: NULL;
	// go through the pair and remove the literals in the base
	// from the first cube and all literals from the second cube
	while ( 1 )
	{
		if ( pLit1 && pLit2 )
		{
			if ( pLit1->iVar == pLit2->iVar )
            {  // this literal is present in both cubes - it belongs to the base
                // mark the affected var
                if ( pLit1->pVar->pOrder == NULL )
                    Fxu_MatrixRingVarsAdd( p, pLit1->pVar );
                // leave the base in pCubeUse; delete it from pCubeRem
				Fxu_MatrixDelLiteral( p, pLit2 );
				// step to the next literals
				pLit1     = bLit1Next;
				pLit2     = bLit2Next;
				bLit1Next = pLit1? pLit1->pHNext: NULL;
				bLit2Next = pLit2? pLit2->pHNext: NULL;
			}
			else if ( pLit1->iVar < pLit2->iVar )
			{ // this literal is present in pCubeUse - remove it
                // mark the affected var
                if ( pLit1->pVar->pOrder == NULL )
                    Fxu_MatrixRingVarsAdd( p, pLit1->pVar );
                // delete this literal
                Fxu_MatrixDelLiteral( p, pLit1 );
				// step to the next literals
				pLit1     = bLit1Next;
				bLit1Next = pLit1? pLit1->pHNext: NULL;
			}
			else
			{ // this literal is present in pCubeRem - remove it
                // mark the affected var
                if ( pLit2->pVar->pOrder == NULL )
                    Fxu_MatrixRingVarsAdd( p, pLit2->pVar );
                // delete this literal
				Fxu_MatrixDelLiteral( p, pLit2 );
				// step to the next literals
				pLit2     = bLit2Next;
				bLit2Next = pLit2? pLit2->pHNext: NULL;
			}
		}
		else if ( pLit1 && !pLit2 )
		{ // this literal is present in pCubeUse - leave it
            // mark the affected var
            if ( pLit1->pVar->pOrder == NULL )
                Fxu_MatrixRingVarsAdd( p, pLit1->pVar );
            // delete this literal
			Fxu_MatrixDelLiteral( p, pLit1 );
			// step to the next literals
			pLit1     = bLit1Next;
			bLit1Next = pLit1? pLit1->pHNext: NULL;
		}
		else if ( !pLit1 && pLit2 )
		{ // this literal is present in pCubeRem - remove it
            // mark the affected var
            if ( pLit2->pVar->pOrder == NULL )
                Fxu_MatrixRingVarsAdd( p, pLit2->pVar );
            // delete this literal
			Fxu_MatrixDelLiteral( p, pLit2 );
			// step to the next literals
			pLit2     = bLit2Next;
			bLit2Next = pLit2? pLit2->pHNext: NULL;
		}
		else
			break;
	}
}

/**Function*************************************************************

  Synopsis    [Updates the matrix after selecting a single cube divisor.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fxu_UpdateMatrixSingleClean( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVar2, Fxu_Var * pVarNew )
{
	Fxu_Lit * pLit1, * bLit1Next;
	Fxu_Lit * pLit2, * bLit2Next;

    // initialize the starting literals
	pLit1     = pVar1->lLits.pHead;
	pLit2     = pVar2->lLits.pHead;
	bLit1Next = pLit1? pLit1->pVNext: NULL;
	bLit2Next = pLit2? pLit2->pVNext: NULL;
	while ( 1 )
	{
		if ( pLit1 && pLit2 )
		{
    		if ( pLit1->pCube->pVar->iVar == pLit2->pCube->pVar->iVar )
			{ // these literals coincide 
			    if ( pLit1->iCube == pLit2->iCube )
			    { // these literals coincide 
                
                    // collect the affected cube
                    assert( pLit1->pCube->pOrder == NULL );
                    Fxu_MatrixRingCubesAdd( p, pLit1->pCube );

                    // add the literal to this cube corresponding to the new column
		            Fxu_MatrixAddLiteral( p, pLit1->pCube, pVarNew );
                    // clean the old cubes
		            Fxu_UpdateCleanOldDoubles( p, NULL, pLit1->pCube );

				    // remove the literals 
				    Fxu_MatrixDelLiteral( p, pLit1 );
				    Fxu_MatrixDelLiteral( p, pLit2 );

				    // go to the next literals
				    pLit1     = bLit1Next;
				    pLit2     = bLit2Next;
				    bLit1Next = pLit1? pLit1->pVNext: NULL;
				    bLit2Next = pLit2? pLit2->pVNext: NULL;
			    }
			    else if ( pLit1->iCube < pLit2->iCube )
			    {
				    pLit1     = bLit1Next;
				    bLit1Next = pLit1? pLit1->pVNext: NULL;
			    }
			    else
			    {
				    pLit2     = bLit2Next;
				    bLit2Next = pLit2? pLit2->pVNext: NULL;
			    }
            }
			else if ( pLit1->pCube->pVar->iVar < pLit2->pCube->pVar->iVar )
			{
				pLit1     = bLit1Next;
				bLit1Next = pLit1? pLit1->pVNext: NULL;
			}
			else
			{
				pLit2     = bLit2Next;
				bLit2Next = pLit2? pLit2->pVNext: NULL;
			}
		}
		else if ( pLit1 && !pLit2 )
		{
			pLit1     = bLit1Next;
			bLit1Next = pLit1? pLit1->pVNext: NULL;
		}
		else if ( !pLit1 && pLit2 )
		{
			pLit2     = bLit2Next;
			bLit2Next = pLit2? pLit2->pVNext: NULL;
		}
		else
			break;
	}
}

/**Function*************************************************************

  Synopsis    [Sort the pairs.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fxu_UpdatePairsSort( Fxu_Matrix * p, Fxu_Double * pDouble )
{
    Fxu_Pair * pPair;
    // order the pairs by the first cube to ensure that 
    // new literals are added to the matrix from top to bottom
    // collect pairs into the array
    p->nPairsTemp = 0;
	Fxu_DoubleForEachPair( pDouble, pPair )
        p->pPairsTemp[ p->nPairsTemp++ ] = pPair;
    if ( p->nPairsTemp > 1 )
    {   // sort
        qsort( (void *)p->pPairsTemp, p->nPairsTemp, sizeof(Fxu_Pair *), 
            (int (*)(const void *, const void *)) Fxu_UpdatePairCompare );
        assert( Fxu_UpdatePairCompare( p->pPairsTemp, p->pPairsTemp + p->nPairsTemp - 1 ) < 0 );
    }
}

/**Function*************************************************************

  Synopsis    [Compares the vars by their number.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fxu_UpdatePairCompare( Fxu_Pair ** ppP1, Fxu_Pair ** ppP2 )
{
    Fxu_Cube * pC1 = (*ppP1)->pCube1;
    Fxu_Cube * pC2 = (*ppP2)->pCube1;
    int iP1CubeMin, iP2CubeMin;
    if ( pC1->pVar->iVar < pC2->pVar->iVar )
        return -1;
    if ( pC1->pVar->iVar > pC2->pVar->iVar )
        return 1;
    iP1CubeMin = Fxu_PairMinCubeInt( *ppP1 );
    iP2CubeMin = Fxu_PairMinCubeInt( *ppP2 );
    if ( iP1CubeMin < iP2CubeMin )
        return -1;
    if ( iP1CubeMin > iP2CubeMin )
        return 1;
    assert( 0 );
    return 0;
}


/**Function*************************************************************

  Synopsis    [Create new variables.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fxu_UpdateCreateNewVars( Fxu_Matrix * p, Fxu_Var ** ppVarC, Fxu_Var ** ppVarD, int nCubes )
{
    Fxu_Var * pVarC, * pVarD;

	// add a new column for the complement
	pVarC = Fxu_MatrixAddVar( p );
    pVarC->nCubes = 0;
	// add a new column for the divisor
	pVarD = Fxu_MatrixAddVar( p );
    pVarD->nCubes = nCubes;
    // mark this entry in the Value2Node array
    assert( p->pValue2Node[pVarC->iVar] > 0 );
    p->pValue2Node[pVarD->iVar  ] = p->pValue2Node[pVarC->iVar];
    p->pValue2Node[pVarD->iVar+1] = p->pValue2Node[pVarC->iVar]+1;

    *ppVarC = pVarC;
    *ppVarD = pVarD;
}


/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fxu_UpdateCleanOldDoubles( Fxu_Matrix * p, Fxu_Double * pDiv, Fxu_Cube * pCube )
{
    Fxu_Double * pDivCur;
	Fxu_Pair * pPair;
    int i;

    // if the cube is a recently introduced one
    // it does not have pairs allocated
    // in this case, there is nothing to update
    if ( pCube->pVar->ppPairs == NULL )
        return;

	// go through all the pairs of this cube
	Fxu_CubeForEachPair( pCube, pPair, i )
	{
         // get the divisor of this pair
        pDivCur = pPair->pDiv;
		// skip the current divisor
		if ( pDivCur == pDiv )
			continue;
		// remove this pair
	    Fxu_ListDoubleDelPair( pDivCur, pPair );	
		// the divisor may have become useless by now
		if ( pDivCur->lPairs.nItems == 0 )
        {
            assert( pDivCur->Weight == pPair->nBase - 1 );
      		Fxu_HeapDoubleDelete( p->pHeapDouble, pDivCur );
			Fxu_MatrixDelDivisor( p, pDivCur );
        }
        else
        {
	        // update the divisor's weight
	        pDivCur->Weight -= pPair->nLits1 + pPair->nLits2 - 1 + pPair->nBase;
      	    Fxu_HeapDoubleUpdate( p->pHeapDouble, pDivCur );
        }
		MEM_FREE_FXU( p, Fxu_Pair, 1, pPair );
	}
	// finally erase all the pair info associated with this cube
	Fxu_PairClearStorage( pCube );
}

/**Function*************************************************************

  Synopsis    [Adds the new divisors that depend on the cube.]

  Description [Go through all the non-empty cubes of this cover 
  (except the given cube) and, for each of them, add the new divisor 
  with the given cube.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fxu_UpdateAddNewDoubles( Fxu_Matrix * p, Fxu_Cube * pCube )
{
	Fxu_Cube * pTemp;
    assert( pCube->pOrder );

    // if the cube is a recently introduced one
    // it does not have pairs allocated
    // in this case, there is nothing to update
    if ( pCube->pVar->ppPairs == NULL )
        return;

	for ( pTemp = pCube->pFirst; pTemp->pVar == pCube->pVar; pTemp = pTemp->pNext )
    {
        // do not add pairs with the empty cubes
		if ( pTemp->lLits.nItems == 0 )
            continue;
        // to prevent adding duplicated pairs of the new cubes
        // do not add the pair, if the current cube is marked 
        if ( pTemp->pOrder && pTemp >= pCube )
            continue;
		Fxu_MatrixAddDivisor( p, pTemp, pCube );
    }
}

/**Function*************************************************************

  Synopsis    [Removes old single cube divisors.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fxu_UpdateCleanOldSingles( Fxu_Matrix * p )
{ 
    Fxu_Single * pSingle, * pSingle2;
    int WeightNew;

    Fxu_MatrixForEachSingleSafe( p, pSingle, pSingle2 )
    {
        // if at least one of the variables is marked, recalculate
        if ( pSingle->pVar1->pOrder || pSingle->pVar2->pOrder )
        {
            // get the new weight
            WeightNew = -2 + Fxu_SingleCountCoincidence( p, pSingle->pVar1, pSingle->pVar2 );
            if ( WeightNew >= 0 )
            {
                pSingle->Weight = WeightNew;
                Fxu_HeapSingleUpdate( p->pHeapSingle, pSingle );
            }
            else
            {
                Fxu_HeapSingleDelete( p->pHeapSingle, pSingle );
                Fxu_ListMatrixDelSingle( p, pSingle );
		        MEM_FREE_FXU( p, Fxu_Single, 1, pSingle );
            }
        }
    }
}

/**Function*************************************************************

  Synopsis    [Updates the single cube divisors.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fxu_UpdateAddNewSingles( Fxu_Matrix * p, Fxu_Var * pVar )
{
    Fxu_MatrixComputeSinglesOne( p, pVar );
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////