Version abc50806

1 files changed, 802 insertions, 0 deletions

diff --git a/src/opt/fxu/fxuUpdate.c b/src/opt/fxu/fxuUpdate.c
new file mode 100644
index 00000000..b781e0b1
--- /dev/null
+++ b/src/opt/fxu/fxuUpdate.c
@@ -0,0 +1,802 @@
+/**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 DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**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++ )
+    {
+        // get the pair
+        pPair = p->pPairsTemp[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->nPairsTemp = 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->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                                ///
+////////////////////////////////////////////////////////////////////////
+
+