src/opt/fxu/fxuUpdate.c File Reference

#include "fxuInt.h"

Include dependency graph for fxuUpdate.c:

Go to the source code of this file.

Functions
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)
void	Fxu_Update (Fxu_Matrix *p, Fxu_Single *pSingle, Fxu_Double *pDouble)
void	Fxu_UpdateSingle (Fxu_Matrix *p)
void	Fxu_UpdateDouble (Fxu_Matrix *p)

---

Function Documentation

void Fxu_Update	(	Fxu_Matrix *	p,
		Fxu_Single *	pSingle,
		Fxu_Double *	pDouble
	)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Updates the matrix after selecting two divisors.]

Description []

SideEffects []

SeeAlso []

Definition at line 54 of file fxuUpdate.c.

{
        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++;
}

void Fxu_UpdateAddNewDoubles	(	Fxu_Matrix *	p,
		Fxu_Cube *	pCube
	)			[static]

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 []

Definition at line 721 of file fxuUpdate.c.

{
        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 );
    }
}

void Fxu_UpdateAddNewSingles	(	Fxu_Matrix *	p,
		Fxu_Var *	pVar
	)			[static]

Function*************************************************************

Synopsis [Updates the single cube divisors.]

Description []

SideEffects []

SeeAlso []

Definition at line 797 of file fxuUpdate.c.

{
    Fxu_MatrixComputeSinglesOne( p, pVar );
}

void Fxu_UpdateCleanOldDoubles	(	Fxu_Matrix *	p,
		Fxu_Double *	pDiv,
		Fxu_Cube *	pCube
	)			[static]

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 667 of file fxuUpdate.c.

{
    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 );
}

void Fxu_UpdateCleanOldSingles

(

Fxu_Matrix *

p

)

[static]

Function*************************************************************

Synopsis [Removes old single cube divisors.]

Description []

SideEffects []

SeeAlso []

Definition at line 756 of file fxuUpdate.c.

{ 
    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 );
}

void Fxu_UpdateCreateNewVars	(	Fxu_Matrix *	p,
		Fxu_Var **	ppVarC,
		Fxu_Var **	ppVarD,
		int	nCubes
	)			[static]

Function*************************************************************

Synopsis [Create new variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 635 of file fxuUpdate.c.

{
    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;
}

void Fxu_UpdateDouble

(

Fxu_Matrix *

p

)

Function*************************************************************

Synopsis [Updates the matrix after accepting a double cube divisor.]

Description []

SideEffects []

SeeAlso []

Definition at line 216 of file fxuUpdate.c.

{
    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++;
}

void Fxu_UpdateDoublePairs	(	Fxu_Matrix *	p,
		Fxu_Double *	pDouble,
		Fxu_Var *	pVar
	)			[static]

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

] DECLARATIONS ///

Function*************************************************************

Synopsis [Update the pairs.]

Description []

SideEffects []

SeeAlso []

Definition at line 282 of file fxuUpdate.c.

{
    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;
}

void Fxu_UpdateMatrixDoubleClean	(	Fxu_Matrix *	p,
		Fxu_Cube *	pCubeUse,
		Fxu_Cube *	pCubeRem
	)			[static]

Function*************************************************************

Synopsis [Create the node equal to double-cube divisor.]

Description []

SideEffects []

SeeAlso []

Definition at line 401 of file fxuUpdate.c.

{
        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;
        }
}

void Fxu_UpdateMatrixDoubleCreateCubes	(	Fxu_Matrix *	p,
		Fxu_Cube *	pCube1,
		Fxu_Cube *	pCube2,
		Fxu_Double *	pDiv
	)			[static]

Function*************************************************************

Synopsis [Add two cubes corresponding to the given double-cube divisor.]

Description []

SideEffects []

SeeAlso []

Definition at line 331 of file fxuUpdate.c.

{
        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 );
}

void Fxu_UpdateMatrixSingleClean	(	Fxu_Matrix *	p,
		Fxu_Var *	pVar1,
		Fxu_Var *	pVar2,
		Fxu_Var *	pVarNew
	)			[static]

Function*************************************************************

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

Description []

SideEffects []

SeeAlso []

Definition at line 491 of file fxuUpdate.c.

{
        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;
        }
}

int Fxu_UpdatePairCompare	(	Fxu_Pair **	ppP1,
		Fxu_Pair **	ppP2
	)			[static]

Function*************************************************************

Synopsis [Compares the vars by their number.]

Description []

SideEffects []

SeeAlso []

Definition at line 604 of file fxuUpdate.c.

{
    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;
}

void Fxu_UpdatePairsSort	(	Fxu_Matrix *	p,
		Fxu_Double *	pDouble
	)			[static]

Function*************************************************************

Synopsis [Sort the pairs.]

Description []

SideEffects []

SeeAlso []

Definition at line 577 of file fxuUpdate.c.

{
    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 );
}

void Fxu_UpdateSingle

(

Fxu_Matrix *

p

)

Function*************************************************************

Synopsis [Updates after accepting single cube divisor.]

Description []

SideEffects []

SeeAlso []

Definition at line 146 of file fxuUpdate.c.

{
    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++;
}