src/opt/fxu/fxuMatrix.c File Reference

#include "fxuInt.h"
Include dependency graph for fxuMatrix.c:

Go to the source code of this file.

Functions

unsigned int Cudd_Prime (unsigned int p)
Fxu_Matrix * Fxu_MatrixAllocate ()
void Fxu_MatrixDelete (Fxu_Matrix *p)
Fxu_Var * Fxu_MatrixAddVar (Fxu_Matrix *p)
Fxu_Cube * Fxu_MatrixAddCube (Fxu_Matrix *p, Fxu_Var *pVar, int iCube)
void Fxu_MatrixAddLiteral (Fxu_Matrix *p, Fxu_Cube *pCube, Fxu_Var *pVar)
void Fxu_MatrixDelDivisor (Fxu_Matrix *p, Fxu_Double *pDiv)
void Fxu_MatrixDelLiteral (Fxu_Matrix *p, Fxu_Lit *pLit)
void Fxu_MatrixAddSingle (Fxu_Matrix *p, Fxu_Var *pVar1, Fxu_Var *pVar2, int Weight)
void Fxu_MatrixAddDivisor (Fxu_Matrix *p, Fxu_Cube *pCube1, Fxu_Cube *pCube2)

Function Documentation

unsigned int Cudd_Prime ( unsigned int  p  ) 

CFile****************************************************************

FileName [fxuMatrix.c]

PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]

Synopsis [Procedures to manipulate the sparse matrix.]

Author [MVSIS Group]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - February 1, 2003.]

Revision [

Id
fxuMatrix.c,v 1.0 2003/02/01 00:00:00 alanmi Exp

] DECLARATIONS ///

AutomaticEnd Function********************************************************************

Synopsis [Returns the next prime >= p.]

Description []

SideEffects [None]

Definition at line 152 of file cuddTable.c.

00154 {
00155     int i,pn;
00156 
00157     p--;
00158     do {
00159         p++;
00160         if (p&1) {
00161             pn = 1;
00162             i = 3;
00163             while ((unsigned) (i * i) <= p) {
00164                 if (p % i == 0) {
00165                     pn = 0;
00166                     break;
00167                 }
00168                 i += 2;
00169             }
00170         } else {
00171             pn = 0;
00172         }
00173     } while (!pn);
00174     return(p);
00175 
00176 } /* end of Cudd_Prime */

Fxu_Cube* Fxu_MatrixAddCube ( Fxu_Matrix *  p,
Fxu_Var *  pVar,
int  iCube 
)

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

Synopsis [Adds a literal to the matrix.]

Description []

SideEffects []

SeeAlso []

Definition at line 182 of file fxuMatrix.c.

00183 {
00184         Fxu_Cube * pCube;
00185         pCube = MEM_ALLOC_FXU( p, Fxu_Cube, 1 );
00186         memset( pCube, 0, sizeof(Fxu_Cube) );
00187         pCube->pVar  = pVar;
00188         pCube->iCube = iCube;
00189         Fxu_ListMatrixAddCube( p, pCube );
00190         return pCube;
00191 }

void Fxu_MatrixAddDivisor ( Fxu_Matrix *  p,
Fxu_Cube *  pCube1,
Fxu_Cube *  pCube2 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 300 of file fxuMatrix.c.

00301 {
00302         Fxu_Pair * pPair;
00303         Fxu_Double * pDiv;
00304     int nBase, nLits1, nLits2;
00305     int fFound;
00306         unsigned Key;
00307 
00308     // canonicize the pair
00309     Fxu_PairCanonicize( &pCube1, &pCube2 );
00310     // compute the hash key
00311     Key = Fxu_PairHashKey( p, pCube1, pCube2, &nBase, &nLits1, &nLits2 );
00312 
00313     // create the cube pair
00314     pPair = Fxu_PairAlloc( p, pCube1, pCube2 );
00315     pPair->nBase  = nBase;
00316     pPair->nLits1 = nLits1;
00317     pPair->nLits2 = nLits2;
00318 
00319     // check if the divisor for this pair already exists
00320     fFound = 0;
00321     Key %= p->nTableSize;
00322         Fxu_TableForEachDouble( p, Key, pDiv )
00323     {
00324                 if ( Fxu_PairCompare( pPair, pDiv->lPairs.pTail ) ) // they are equal
00325         {
00326             fFound = 1;
00327             break;
00328         }
00329     }
00330 
00331     if ( !fFound )
00332     {   // create the new divisor
00333             pDiv = MEM_ALLOC_FXU( p, Fxu_Double, 1 );
00334             memset( pDiv, 0, sizeof(Fxu_Double) );
00335             pDiv->Key = Key;
00336             // set the number of this divisor
00337             pDiv->Num = p->nDivsTotal++; // p->nDivs;
00338             // insert the divisor in the table
00339             Fxu_ListTableAddDivisor( p, pDiv );
00340             // set the initial cost of the divisor
00341             pDiv->Weight -= pPair->nLits1 + pPair->nLits2;
00342     }
00343 
00344         // link the pair to the cubes
00345         Fxu_PairAdd( pPair );
00346         // connect the pair and the divisor
00347         pPair->pDiv = pDiv;
00348         Fxu_ListDoubleAddPairLast( pDiv, pPair );       
00349     // update the max number of pairs in a divisor
00350 //    if ( p->nPairsMax < pDiv->lPairs.nItems )
00351 //        p->nPairsMax = pDiv->lPairs.nItems;
00352         // update the divisor's weight
00353         pDiv->Weight += pPair->nLits1 + pPair->nLits2 - 1 + pPair->nBase;
00354     if ( fFound ) // update the divisor in the heap
00355         Fxu_HeapDoubleUpdate( p->pHeapDouble, pDiv );
00356     else  // add the new divisor to the heap
00357         Fxu_HeapDoubleInsert( p->pHeapDouble, pDiv );
00358 }

void Fxu_MatrixAddLiteral ( Fxu_Matrix *  p,
Fxu_Cube *  pCube,
Fxu_Var *  pVar 
)

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

Synopsis [Adds a literal to the matrix.]

Description []

SideEffects []

SeeAlso []

Definition at line 204 of file fxuMatrix.c.

00205 {
00206         Fxu_Lit * pLit;
00207         pLit = MEM_ALLOC_FXU( p, Fxu_Lit, 1 );
00208         memset( pLit, 0, sizeof(Fxu_Lit) );
00209         // insert the literal into two linked lists
00210         Fxu_ListCubeAddLiteral( pCube, pLit );
00211         Fxu_ListVarAddLiteral( pVar, pLit );
00212         // set the back pointers
00213         pLit->pCube = pCube;
00214         pLit->pVar  = pVar;
00215         pLit->iCube = pCube->iCube;
00216         pLit->iVar  = pVar->iVar;
00217         // increment the literal counter
00218         p->nEntries++;
00219 }

void Fxu_MatrixAddSingle ( Fxu_Matrix *  p,
Fxu_Var *  pVar1,
Fxu_Var *  pVar2,
int  Weight 
)

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

Synopsis [Creates and adds a single cube divisor.]

Description []

SideEffects []

SeeAlso []

Definition at line 273 of file fxuMatrix.c.

00274 {
00275     Fxu_Single * pSingle;
00276     assert( pVar1->iVar < pVar2->iVar );
00277         pSingle = MEM_ALLOC_FXU( p, Fxu_Single, 1 );
00278         memset( pSingle, 0, sizeof(Fxu_Single) );
00279     pSingle->Num = p->lSingles.nItems;
00280     pSingle->Weight = Weight;
00281     pSingle->HNum = 0;
00282     pSingle->pVar1 = pVar1;
00283     pSingle->pVar2 = pVar2;
00284     Fxu_ListMatrixAddSingle( p, pSingle );
00285     // add to the heap
00286     Fxu_HeapSingleInsert( p->pHeapSingle, pSingle );
00287 }

Fxu_Var* Fxu_MatrixAddVar ( Fxu_Matrix *  p  ) 

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

Synopsis [Adds a variable to the matrix.]

Description [This procedure always adds variables at the end of the matrix. It assigns the var's node and number. It adds the var to the linked list of all variables and to the table of all nodes.]

SideEffects []

SeeAlso []

Definition at line 160 of file fxuMatrix.c.

00161 {
00162         Fxu_Var * pVar;
00163         pVar = MEM_ALLOC_FXU( p, Fxu_Var, 1 );
00164         memset( pVar, 0, sizeof(Fxu_Var) );
00165         pVar->iVar = p->lVars.nItems;
00166     p->ppVars[pVar->iVar] = pVar;
00167         Fxu_ListMatrixAddVariable( p, pVar );
00168         return pVar;
00169 }

Fxu_Matrix* Fxu_MatrixAllocate (  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file fxuMatrix.c.

00043 {
00044         Fxu_Matrix * p;
00045         p = ALLOC( Fxu_Matrix, 1 );
00046         memset( p, 0, sizeof(Fxu_Matrix) );
00047         p->nTableSize = Cudd_Prime(10000);
00048         p->pTable = ALLOC( Fxu_ListDouble, p->nTableSize );
00049         memset( p->pTable, 0, sizeof(Fxu_ListDouble) * p->nTableSize );
00050 #ifndef USE_SYSTEM_MEMORY_MANAGEMENT
00051     {
00052         // get the largest size in bytes for the following structures:
00053         // Fxu_Cube, Fxu_Var, Fxu_Lit, Fxu_Pair, Fxu_Double, Fxu_Single
00054         // (currently, Fxu_Var, Fxu_Pair, Fxu_Double take 10 machine words)
00055         int nSizeMax, nSizeCur;
00056         nSizeMax = -1;
00057         nSizeCur = sizeof(Fxu_Cube);
00058         if ( nSizeMax < nSizeCur )
00059              nSizeMax = nSizeCur;
00060         nSizeCur = sizeof(Fxu_Var);
00061         if ( nSizeMax < nSizeCur )
00062              nSizeMax = nSizeCur;
00063         nSizeCur = sizeof(Fxu_Lit);
00064         if ( nSizeMax < nSizeCur )
00065              nSizeMax = nSizeCur;
00066         nSizeCur = sizeof(Fxu_Pair);
00067         if ( nSizeMax < nSizeCur )
00068              nSizeMax = nSizeCur;
00069         nSizeCur = sizeof(Fxu_Double);
00070         if ( nSizeMax < nSizeCur )
00071              nSizeMax = nSizeCur;
00072         nSizeCur = sizeof(Fxu_Single);
00073         if ( nSizeMax < nSizeCur )
00074              nSizeMax = nSizeCur;
00075         p->pMemMan  = Extra_MmFixedStart( nSizeMax ); 
00076     }
00077 #endif
00078         p->pHeapDouble = Fxu_HeapDoubleStart();
00079         p->pHeapSingle = Fxu_HeapSingleStart();
00080     p->vPairs = Vec_PtrAlloc( 100 );
00081         return p;
00082 }

void Fxu_MatrixDelDivisor ( Fxu_Matrix *  p,
Fxu_Double *  pDiv 
)

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

Synopsis [Deletes the divisor from the matrix.]

Description []

SideEffects []

SeeAlso []

Definition at line 232 of file fxuMatrix.c.

00233 {
00234         // delete divisor from the table
00235         Fxu_ListTableDelDivisor( p, pDiv );
00236         // recycle the divisor
00237         MEM_FREE_FXU( p, Fxu_Double, 1, pDiv );
00238 }

void Fxu_MatrixDelete ( Fxu_Matrix *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 95 of file fxuMatrix.c.

00096 {
00097         Fxu_HeapDoubleCheck( p->pHeapDouble );
00098         Fxu_HeapDoubleStop( p->pHeapDouble );
00099     Fxu_HeapSingleStop( p->pHeapSingle );
00100 
00101         // delete other things
00102 #ifdef USE_SYSTEM_MEMORY_MANAGEMENT
00103         // this code is not needed when the custom memory manager is used
00104     {
00105             Fxu_Cube * pCube, * pCube2;
00106             Fxu_Var * pVar, * pVar2;
00107             Fxu_Lit * pLit, * pLit2;
00108             Fxu_Double * pDiv, * pDiv2;
00109             Fxu_Single * pSingle, * pSingle2;
00110             Fxu_Pair * pPair, * pPair2;
00111         int i;
00112             // delete the divisors
00113             Fxu_MatrixForEachDoubleSafe( p, pDiv, pDiv2, i )
00114             {
00115                     Fxu_DoubleForEachPairSafe( pDiv, pPair, pPair2 )
00116                             MEM_FREE_FXU( p, Fxu_Pair, 1, pPair );
00117                     MEM_FREE_FXU( p, Fxu_Double, 1, pDiv );
00118             }
00119             Fxu_MatrixForEachSingleSafe( p, pSingle, pSingle2 )
00120                     MEM_FREE_FXU( p, Fxu_Single, 1, pSingle );
00121             // delete the entries
00122             Fxu_MatrixForEachCube( p, pCube )
00123                     Fxu_CubeForEachLiteralSafe( pCube, pLit, pLit2 )
00124                             MEM_FREE_FXU( p, Fxu_Lit, 1, pLit );
00125             // delete the cubes
00126             Fxu_MatrixForEachCubeSafe( p, pCube, pCube2 )
00127                     MEM_FREE_FXU( p, Fxu_Cube, 1, pCube );
00128             // delete the vars
00129             Fxu_MatrixForEachVariableSafe( p, pVar, pVar2 )
00130                     MEM_FREE_FXU( p, Fxu_Var, 1, pVar );
00131     }
00132 #else
00133         Extra_MmFixedStop( p->pMemMan );
00134 #endif
00135 
00136     Vec_PtrFree( p->vPairs );
00137         FREE( p->pppPairs );
00138         FREE( p->ppPairs );
00139 //    FREE( p->pPairsTemp );
00140         FREE( p->pTable );
00141         FREE( p->ppVars );
00142         FREE( p );
00143 }

void Fxu_MatrixDelLiteral ( Fxu_Matrix *  p,
Fxu_Lit *  pLit 
)

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

Synopsis [Deletes the literal fromthe matrix.]

Description []

SideEffects []

SeeAlso []

Definition at line 251 of file fxuMatrix.c.

00252 {
00253     // delete the literal
00254         Fxu_ListCubeDelLiteral( pLit->pCube, pLit );
00255         Fxu_ListVarDelLiteral( pLit->pVar, pLit );
00256         MEM_FREE_FXU( p, Fxu_Lit, 1, pLit );
00257         // increment the literal counter
00258         p->nEntries--;
00259 }

Generated on Tue Jan 5 12:19:26 2010 for abc70930 by  doxygen 1.6.1