fxuUpdate.c File Reference

#include "fxuInt.h"

Include dependency graph for fxuUpdate.c:

Go to the source code of this file.

Functions
void	Fxu_Update (Fxu_Matrix *p, Fxu_Single *pSingle, Fxu_Double *pDouble)
	FUNCTION DEFINITIONS ///.
void	Fxu_UpdateSingle (Fxu_Matrix *p)
void	Fxu_UpdateDouble (Fxu_Matrix *p)

Function Documentation

Fxu_Update()

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

Here is the call graph for this function:

Here is the caller graph for this function:

Fxu_UpdateDouble()

void Fxu_UpdateDouble

(

Fxu_Matrix *

p

)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 219 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++;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fxu_UpdateSingle()

void Fxu_UpdateSingle

(

Fxu_Matrix *

p

)

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

Synopsis [Updates after accepting single cube divisor.]

Description []

SideEffects []

SeeAlso []

Definition at line 149 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++;
}

Here is the call graph for this function:

Here is the caller graph for this function: