path: root/src/opt/fxu/fxuUpdate.c

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

////////////////////////////////////////////////////////////////////////
///                        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 = 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 >= 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;
    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                                ///
////////////////////////////////////////////////////////////////////////