src/opt/fxu/fxuMatrix.c

Go to the documentation of this file.

#include "fxuInt.h"


extern unsigned int Cudd_Prime( unsigned int p );


Fxu_Matrix * Fxu_MatrixAllocate()
{
        Fxu_Matrix * p;
        p = ALLOC( Fxu_Matrix, 1 );
        memset( p, 0, sizeof(Fxu_Matrix) );
        p->nTableSize = Cudd_Prime(10000);
        p->pTable = ALLOC( Fxu_ListDouble, p->nTableSize );
        memset( p->pTable, 0, sizeof(Fxu_ListDouble) * p->nTableSize );
#ifndef USE_SYSTEM_MEMORY_MANAGEMENT
    {
        // get the largest size in bytes for the following structures:
        // Fxu_Cube, Fxu_Var, Fxu_Lit, Fxu_Pair, Fxu_Double, Fxu_Single
        // (currently, Fxu_Var, Fxu_Pair, Fxu_Double take 10 machine words)
        int nSizeMax, nSizeCur;
        nSizeMax = -1;
        nSizeCur = sizeof(Fxu_Cube);
        if ( nSizeMax < nSizeCur )
             nSizeMax = nSizeCur;
        nSizeCur = sizeof(Fxu_Var);
        if ( nSizeMax < nSizeCur )
             nSizeMax = nSizeCur;
        nSizeCur = sizeof(Fxu_Lit);
        if ( nSizeMax < nSizeCur )
             nSizeMax = nSizeCur;
        nSizeCur = sizeof(Fxu_Pair);
        if ( nSizeMax < nSizeCur )
             nSizeMax = nSizeCur;
        nSizeCur = sizeof(Fxu_Double);
        if ( nSizeMax < nSizeCur )
             nSizeMax = nSizeCur;
        nSizeCur = sizeof(Fxu_Single);
        if ( nSizeMax < nSizeCur )
             nSizeMax = nSizeCur;
        p->pMemMan  = Extra_MmFixedStart( nSizeMax ); 
    }
#endif
        p->pHeapDouble = Fxu_HeapDoubleStart();
        p->pHeapSingle = Fxu_HeapSingleStart();
    p->vPairs = Vec_PtrAlloc( 100 );
        return p;
}

void Fxu_MatrixDelete( Fxu_Matrix * p )
{
        Fxu_HeapDoubleCheck( p->pHeapDouble );
        Fxu_HeapDoubleStop( p->pHeapDouble );
    Fxu_HeapSingleStop( p->pHeapSingle );

        // delete other things
#ifdef USE_SYSTEM_MEMORY_MANAGEMENT
        // this code is not needed when the custom memory manager is used
    {
            Fxu_Cube * pCube, * pCube2;
            Fxu_Var * pVar, * pVar2;
            Fxu_Lit * pLit, * pLit2;
            Fxu_Double * pDiv, * pDiv2;
            Fxu_Single * pSingle, * pSingle2;
            Fxu_Pair * pPair, * pPair2;
        int i;
            // delete the divisors
            Fxu_MatrixForEachDoubleSafe( p, pDiv, pDiv2, i )
            {
                    Fxu_DoubleForEachPairSafe( pDiv, pPair, pPair2 )
                            MEM_FREE_FXU( p, Fxu_Pair, 1, pPair );
                    MEM_FREE_FXU( p, Fxu_Double, 1, pDiv );
            }
            Fxu_MatrixForEachSingleSafe( p, pSingle, pSingle2 )
                    MEM_FREE_FXU( p, Fxu_Single, 1, pSingle );
            // delete the entries
            Fxu_MatrixForEachCube( p, pCube )
                    Fxu_CubeForEachLiteralSafe( pCube, pLit, pLit2 )
                            MEM_FREE_FXU( p, Fxu_Lit, 1, pLit );
            // delete the cubes
            Fxu_MatrixForEachCubeSafe( p, pCube, pCube2 )
                    MEM_FREE_FXU( p, Fxu_Cube, 1, pCube );
            // delete the vars
            Fxu_MatrixForEachVariableSafe( p, pVar, pVar2 )
                    MEM_FREE_FXU( p, Fxu_Var, 1, pVar );
    }
#else
        Extra_MmFixedStop( p->pMemMan );
#endif

    Vec_PtrFree( p->vPairs );
        FREE( p->pppPairs );
        FREE( p->ppPairs );
//    FREE( p->pPairsTemp );
        FREE( p->pTable );
        FREE( p->ppVars );
        FREE( p );
}



Fxu_Var * Fxu_MatrixAddVar( Fxu_Matrix * p )
{
        Fxu_Var * pVar;
        pVar = MEM_ALLOC_FXU( p, Fxu_Var, 1 );
        memset( pVar, 0, sizeof(Fxu_Var) );
        pVar->iVar = p->lVars.nItems;
    p->ppVars[pVar->iVar] = pVar;
        Fxu_ListMatrixAddVariable( p, pVar );
        return pVar;
}

Fxu_Cube * Fxu_MatrixAddCube( Fxu_Matrix * p, Fxu_Var * pVar, int iCube )
{
        Fxu_Cube * pCube;
        pCube = MEM_ALLOC_FXU( p, Fxu_Cube, 1 );
        memset( pCube, 0, sizeof(Fxu_Cube) );
        pCube->pVar  = pVar;
        pCube->iCube = iCube;
        Fxu_ListMatrixAddCube( p, pCube );
        return pCube;
}

void Fxu_MatrixAddLiteral( Fxu_Matrix * p, Fxu_Cube * pCube, Fxu_Var * pVar )
{
        Fxu_Lit * pLit;
        pLit = MEM_ALLOC_FXU( p, Fxu_Lit, 1 );
        memset( pLit, 0, sizeof(Fxu_Lit) );
        // insert the literal into two linked lists
        Fxu_ListCubeAddLiteral( pCube, pLit );
        Fxu_ListVarAddLiteral( pVar, pLit );
        // set the back pointers
        pLit->pCube = pCube;
        pLit->pVar  = pVar;
        pLit->iCube = pCube->iCube;
        pLit->iVar  = pVar->iVar;
        // increment the literal counter
        p->nEntries++;
}

void Fxu_MatrixDelDivisor( Fxu_Matrix * p, Fxu_Double * pDiv )
{
        // delete divisor from the table
        Fxu_ListTableDelDivisor( p, pDiv );
        // recycle the divisor
        MEM_FREE_FXU( p, Fxu_Double, 1, pDiv );
}

void Fxu_MatrixDelLiteral( Fxu_Matrix * p, Fxu_Lit * pLit )
{
    // delete the literal
        Fxu_ListCubeDelLiteral( pLit->pCube, pLit );
        Fxu_ListVarDelLiteral( pLit->pVar, pLit );
        MEM_FREE_FXU( p, Fxu_Lit, 1, pLit );
        // increment the literal counter
        p->nEntries--;
}


void Fxu_MatrixAddSingle( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVar2, int Weight )
{
    Fxu_Single * pSingle;
    assert( pVar1->iVar < pVar2->iVar );
        pSingle = MEM_ALLOC_FXU( p, Fxu_Single, 1 );
        memset( pSingle, 0, sizeof(Fxu_Single) );
    pSingle->Num = p->lSingles.nItems;
    pSingle->Weight = Weight;
    pSingle->HNum = 0;
    pSingle->pVar1 = pVar1;
    pSingle->pVar2 = pVar2;
    Fxu_ListMatrixAddSingle( p, pSingle );
    // add to the heap
    Fxu_HeapSingleInsert( p->pHeapSingle, pSingle );
}

void Fxu_MatrixAddDivisor( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2 )
{
        Fxu_Pair * pPair;
        Fxu_Double * pDiv;
    int nBase, nLits1, nLits2;
    int fFound;
        unsigned Key;

    // canonicize the pair
    Fxu_PairCanonicize( &pCube1, &pCube2 );
    // compute the hash key
    Key = Fxu_PairHashKey( p, pCube1, pCube2, &nBase, &nLits1, &nLits2 );

    // create the cube pair
    pPair = Fxu_PairAlloc( p, pCube1, pCube2 );
    pPair->nBase  = nBase;
    pPair->nLits1 = nLits1;
    pPair->nLits2 = nLits2;

    // check if the divisor for this pair already exists
    fFound = 0;
    Key %= p->nTableSize;
        Fxu_TableForEachDouble( p, Key, pDiv )
    {
                if ( Fxu_PairCompare( pPair, pDiv->lPairs.pTail ) ) // they are equal
        {
            fFound = 1;
            break;
        }
    }

    if ( !fFound )
    {   // create the new divisor
            pDiv = MEM_ALLOC_FXU( p, Fxu_Double, 1 );
            memset( pDiv, 0, sizeof(Fxu_Double) );
            pDiv->Key = Key;
            // set the number of this divisor
            pDiv->Num = p->nDivsTotal++; // p->nDivs;
            // insert the divisor in the table
            Fxu_ListTableAddDivisor( p, pDiv );
            // set the initial cost of the divisor
            pDiv->Weight -= pPair->nLits1 + pPair->nLits2;
    }

        // link the pair to the cubes
        Fxu_PairAdd( pPair );
        // connect the pair and the divisor
        pPair->pDiv = pDiv;
        Fxu_ListDoubleAddPairLast( pDiv, pPair );       
    // update the max number of pairs in a divisor
//    if ( p->nPairsMax < pDiv->lPairs.nItems )
//        p->nPairsMax = pDiv->lPairs.nItems;
        // update the divisor's weight
        pDiv->Weight += pPair->nLits1 + pPair->nLits2 - 1 + pPair->nBase;
    if ( fFound ) // update the divisor in the heap
        Fxu_HeapDoubleUpdate( p->pHeapDouble, pDiv );
    else  // add the new divisor to the heap
        Fxu_HeapDoubleInsert( p->pHeapDouble, pDiv );
}

/*
    {
        int piVarsC1[100], piVarsC2[100], nVarsC1, nVarsC2;
        Fxu_Double * pDivCur;
        Fxu_MatrixGetDoubleVars( p, pDiv, piVarsC1, piVarsC2, &nVarsC1, &nVarsC2 );
        pDivCur = Fxu_MatrixFindDouble( p, piVarsC1, piVarsC2, nVarsC1, nVarsC2 );
        assert( pDivCur == pDiv );
    }
*/

---