Version abc71001

1 files changed, 374 insertions, 0 deletions

diff --git a/src/opt/fxu/fxuMatrix.c b/src/opt/fxu/fxuMatrix.c
new file mode 100644
index 00000000..93ec7b90
--- /dev/null
+++ b/src/opt/fxu/fxuMatrix.c
@@ -0,0 +1,374 @@
+/**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 $]
+
+***********************************************************************/
+
+#include "fxuInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern unsigned int Cudd_Prime( unsigned int p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 );
+}
+
+
+
+/**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     []
+
+***********************************************************************/
+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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds a literal to the matrix.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds a literal to the matrix.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the divisor from the matrix.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the literal fromthe matrix.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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--;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates and adds a single cube divisor.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 );
+    }
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+