ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
fxuMatrix.c File Reference
#include "fxuInt.h"
Include dependency graph for fxuMatrix.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START Fxu_MatrixFxu_MatrixAllocate ()
 DECLARATIONS ///.
 
void Fxu_MatrixDelete (Fxu_Matrix *p)
 
Fxu_VarFxu_MatrixAddVar (Fxu_Matrix *p)
 
Fxu_CubeFxu_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

◆ Fxu_MatrixAddCube()

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 183 of file fxuMatrix.c.

184{
185 Fxu_Cube * pCube;
186 pCube = MEM_ALLOC_FXU( p, Fxu_Cube, 1 );
187 memset( pCube, 0, sizeof(Fxu_Cube) );
188 pCube->pVar = pVar;
189 pCube->iCube = iCube;
190 Fxu_ListMatrixAddCube( p, pCube );
191 return pCube;
192}
Cube * p
Definition exorList.c:222
#define MEM_ALLOC_FXU(Manager, Type, Size)
Definition fxuInt.h:429
void Fxu_ListMatrixAddCube(Fxu_Matrix *p, Fxu_Cube *pCube)
Definition fxuList.c:104
struct FxuCube Fxu_Cube
Definition fxuInt.h:66
int iCube
Definition fxuInt.h:203
Fxu_Var * pVar
Definition fxuInt.h:205
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Fxu_MatrixAddDivisor()

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 301 of file fxuMatrix.c.

302{
303 Fxu_Pair * pPair;
304 Fxu_Double * pDiv;
305 int nBase, nLits1, nLits2;
306 int fFound;
307 unsigned Key;
308
309 // canonicize the pair
310 Fxu_PairCanonicize( &pCube1, &pCube2 );
311 // compute the hash key
312 Key = Fxu_PairHashKey( p, pCube1, pCube2, &nBase, &nLits1, &nLits2 );
313
314 // create the cube pair
315 pPair = Fxu_PairAlloc( p, pCube1, pCube2 );
316 pPair->nBase = nBase;
317 pPair->nLits1 = nLits1;
318 pPair->nLits2 = nLits2;
319
320 // check if the divisor for this pair already exists
321 fFound = 0;
322 Key %= p->nTableSize;
323 Fxu_TableForEachDouble( p, Key, pDiv )
324 {
325 if ( Fxu_PairCompare( pPair, pDiv->lPairs.pTail ) ) // they are equal
326 {
327 fFound = 1;
328 break;
329 }
330 }
331
332 if ( !fFound )
333 { // create the new divisor
334 pDiv = MEM_ALLOC_FXU( p, Fxu_Double, 1 );
335 memset( pDiv, 0, sizeof(Fxu_Double) );
336 pDiv->Key = Key;
337 // set the number of this divisor
338 pDiv->Num = p->nDivsTotal++; // p->nDivs;
339 // insert the divisor in the table
340 Fxu_ListTableAddDivisor( p, pDiv );
341 // set the initial cost of the divisor
342 pDiv->Weight -= pPair->nLits1 + pPair->nLits2;
343 }
344
345 // link the pair to the cubes
346 Fxu_PairAdd( pPair );
347 // connect the pair and the divisor
348 pPair->pDiv = pDiv;
349 Fxu_ListDoubleAddPairLast( pDiv, pPair );
350 // update the max number of pairs in a divisor
351// if ( p->nPairsMax < pDiv->lPairs.nItems )
352// p->nPairsMax = pDiv->lPairs.nItems;
353 // update the divisor's weight
354 pDiv->Weight += pPair->nLits1 + pPair->nLits2 - 1 + pPair->nBase;
355 if ( fFound ) // update the divisor in the heap
356 Fxu_HeapDoubleUpdate( p->pHeapDouble, pDiv );
357 else // add the new divisor to the heap
358 Fxu_HeapDoubleInsert( p->pHeapDouble, pDiv );
359}
void Fxu_HeapDoubleUpdate(Fxu_HeapDouble *p, Fxu_Double *pDiv)
Definition fxuHeapD.c:223
void Fxu_HeapDoubleInsert(Fxu_HeapDouble *p, Fxu_Double *pDiv)
Definition fxuHeapD.c:201
Fxu_Pair * Fxu_PairAlloc(Fxu_Matrix *p, Fxu_Cube *pCube1, Fxu_Cube *pCube2)
Definition fxuPair.c:519
int Fxu_PairCompare(Fxu_Pair *pPair1, Fxu_Pair *pPair2)
Definition fxuPair.c:236
void Fxu_ListDoubleAddPairLast(Fxu_Double *pDiv, Fxu_Pair *pLink)
Definition fxuList.c:402
unsigned Fxu_PairHashKey(Fxu_Matrix *p, Fxu_Cube *pCube1, Fxu_Cube *pCube2, int *pnBase, int *pnLits1, int *pnLits2)
Definition fxuPair.c:164
void Fxu_PairAdd(Fxu_Pair *pPair)
Definition fxuPair.c:543
struct FxuPair Fxu_Pair
Definition fxuInt.h:71
void Fxu_ListTableAddDivisor(Fxu_Matrix *p, Fxu_Double *pDiv)
Definition fxuList.c:222
#define Fxu_TableForEachDouble(Matrix, Key, Div)
Definition fxuInt.h:321
void Fxu_PairCanonicize(Fxu_Cube **ppCube1, Fxu_Cube **ppCube2)
FUNCTION DEFINITIONS ///.
Definition fxuPair.c:75
struct FxuDouble Fxu_Double
Definition fxuInt.h:72
int Num
Definition fxuInt.h:256
int Weight
Definition fxuInt.h:258
Fxu_ListPair lPairs
Definition fxuInt.h:260
unsigned Key
Definition fxuInt.h:259
Fxu_Pair * pTail
Definition fxuInt.h:118
int nBase
Definition fxuInt.h:243
Fxu_Double * pDiv
Definition fxuInt.h:244
int nLits2
Definition fxuInt.h:242
int nLits1
Definition fxuInt.h:241
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Fxu_MatrixAddLiteral()

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 205 of file fxuMatrix.c.

206{
207 Fxu_Lit * pLit;
208 pLit = MEM_ALLOC_FXU( p, Fxu_Lit, 1 );
209 memset( pLit, 0, sizeof(Fxu_Lit) );
210 // insert the literal into two linked lists
211 Fxu_ListCubeAddLiteral( pCube, pLit );
212 Fxu_ListVarAddLiteral( pVar, pLit );
213 // set the back pointers
214 pLit->pCube = pCube;
215 pLit->pVar = pVar;
216 pLit->iCube = pCube->iCube;
217 pLit->iVar = pVar->iVar;
218 // increment the literal counter
219 p->nEntries++;
220}
void Fxu_ListCubeAddLiteral(Fxu_Cube *pCube, Fxu_Lit *pLit)
Definition fxuList.c:283
struct FxuLit Fxu_Lit
Definition fxuInt.h:68
void Fxu_ListVarAddLiteral(Fxu_Var *pVar, Fxu_Lit *pLit)
Definition fxuList.c:342
Fxu_Cube * pCube
Definition fxuInt.h:230
int iVar
Definition fxuInt.h:228
Fxu_Var * pVar
Definition fxuInt.h:231
int iCube
Definition fxuInt.h:229
int iVar
Definition fxuInt.h:215
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Fxu_MatrixAddSingle()

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 274 of file fxuMatrix.c.

275{
276 Fxu_Single * pSingle;
277 assert( pVar1->iVar < pVar2->iVar );
278 pSingle = MEM_ALLOC_FXU( p, Fxu_Single, 1 );
279 memset( pSingle, 0, sizeof(Fxu_Single) );
280 pSingle->Num = p->lSingles.nItems;
281 pSingle->Weight = Weight;
282 pSingle->HNum = 0;
283 pSingle->pVar1 = pVar1;
284 pSingle->pVar2 = pVar2;
285 Fxu_ListMatrixAddSingle( p, pSingle );
286 // add to the heap
287 Fxu_HeapSingleInsert( p->pHeapSingle, pSingle );
288}
void Fxu_HeapSingleInsert(Fxu_HeapSingle *p, Fxu_Single *pSingle)
Definition fxuHeapS.c:204
void Fxu_ListMatrixAddSingle(Fxu_Matrix *p, Fxu_Single *pSingle)
Definition fxuList.c:163
struct FxuSingle Fxu_Single
Definition fxuInt.h:73
int Weight
Definition fxuInt.h:271
int Num
Definition fxuInt.h:269
Fxu_Var * pVar2
Definition fxuInt.h:273
int HNum
Definition fxuInt.h:270
Fxu_Var * pVar1
Definition fxuInt.h:272
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Fxu_MatrixAddVar()

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 161 of file fxuMatrix.c.

162{
163 Fxu_Var * pVar;
164 pVar = MEM_ALLOC_FXU( p, Fxu_Var, 1 );
165 memset( pVar, 0, sizeof(Fxu_Var) );
166 pVar->iVar = p->lVars.nItems;
167 p->ppVars[pVar->iVar] = pVar;
169 return pVar;
170}
void Fxu_ListMatrixAddVariable(Fxu_Matrix *p, Fxu_Var *pVar)
DECLARATIONS ///.
Definition fxuList.c:45
struct FxuVar Fxu_Var
Definition fxuInt.h:67
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Fxu_MatrixAllocate()

ABC_NAMESPACE_IMPL_START Fxu_Matrix * Fxu_MatrixAllocate ( )

DECLARATIONS ///.

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 43 of file fxuMatrix.c.

44{
45 Fxu_Matrix * p;
46 p = ABC_ALLOC( Fxu_Matrix, 1 );
47 memset( p, 0, sizeof(Fxu_Matrix) );
48 p->nTableSize = Abc_PrimeCudd(10000);
49 p->pTable = ABC_ALLOC( Fxu_ListDouble, p->nTableSize );
50 memset( p->pTable, 0, sizeof(Fxu_ListDouble) * p->nTableSize );
51#ifndef USE_SYSTEM_MEMORY_MANAGEMENT
52 {
53 // get the largest size in bytes for the following structures:
54 // Fxu_Cube, Fxu_Var, Fxu_Lit, Fxu_Pair, Fxu_Double, Fxu_Single
55 // (currently, Fxu_Var, Fxu_Pair, Fxu_Double take 10 machine words)
56 int nSizeMax, nSizeCur;
57 nSizeMax = -1;
58 nSizeCur = sizeof(Fxu_Cube);
59 if ( nSizeMax < nSizeCur )
60 nSizeMax = nSizeCur;
61 nSizeCur = sizeof(Fxu_Var);
62 if ( nSizeMax < nSizeCur )
63 nSizeMax = nSizeCur;
64 nSizeCur = sizeof(Fxu_Lit);
65 if ( nSizeMax < nSizeCur )
66 nSizeMax = nSizeCur;
67 nSizeCur = sizeof(Fxu_Pair);
68 if ( nSizeMax < nSizeCur )
69 nSizeMax = nSizeCur;
70 nSizeCur = sizeof(Fxu_Double);
71 if ( nSizeMax < nSizeCur )
72 nSizeMax = nSizeCur;
73 nSizeCur = sizeof(Fxu_Single);
74 if ( nSizeMax < nSizeCur )
75 nSizeMax = nSizeCur;
76 p->pMemMan = Extra_MmFixedStart( nSizeMax );
77 }
78#endif
79 p->pHeapDouble = Fxu_HeapDoubleStart();
80 p->pHeapSingle = Fxu_HeapSingleStart();
81 p->vPairs = Vec_PtrAlloc( 100 );
82 return p;
83}
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
Extra_MmFixed_t * Extra_MmFixedStart(int nEntrySize)
Fxu_HeapDouble * Fxu_HeapDoubleStart()
FUNCTION DEFINITIONS ///.
Definition fxuHeapD.c:58
Fxu_HeapSingle * Fxu_HeapSingleStart()
FUNCTION DEFINITIONS ///.
Definition fxuHeapS.c:58
typedefABC_NAMESPACE_HEADER_START struct FxuMatrix Fxu_Matrix
INCLUDES ///.
Definition fxuInt.h:63
struct FxuListDouble Fxu_ListDouble
Definition fxuInt.h:80
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Fxu_MatrixDelDivisor()

void Fxu_MatrixDelDivisor ( Fxu_Matrix * p,
Fxu_Double * pDiv )

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

Synopsis [Deletes the divisor from the matrix.]

Description []

SideEffects []

SeeAlso []

Definition at line 233 of file fxuMatrix.c.

234{
235 // delete divisor from the table
236 Fxu_ListTableDelDivisor( p, pDiv );
237 // recycle the divisor
238 MEM_FREE_FXU( p, Fxu_Double, 1, pDiv );
239}
void Fxu_ListTableDelDivisor(Fxu_Matrix *p, Fxu_Double *pDiv)
Definition fxuList.c:254
#define MEM_FREE_FXU(Manager, Type, Size, Pointer)
Definition fxuInt.h:431
Here is the call graph for this function:

◆ Fxu_MatrixDelete()

void Fxu_MatrixDelete ( Fxu_Matrix * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 96 of file fxuMatrix.c.

97{
98 Fxu_HeapDoubleCheck( p->pHeapDouble );
99 Fxu_HeapDoubleStop( p->pHeapDouble );
100 Fxu_HeapSingleStop( p->pHeapSingle );
101
102 // delete other things
103#ifdef USE_SYSTEM_MEMORY_MANAGEMENT
104 // this code is not needed when the custom memory manager is used
105 {
106 Fxu_Cube * pCube, * pCube2;
107 Fxu_Var * pVar, * pVar2;
108 Fxu_Lit * pLit, * pLit2;
109 Fxu_Double * pDiv, * pDiv2;
110 Fxu_Single * pSingle, * pSingle2;
111 Fxu_Pair * pPair, * pPair2;
112 int i;
113 // delete the divisors
114 Fxu_MatrixForEachDoubleSafe( p, pDiv, pDiv2, i )
115 {
116 Fxu_DoubleForEachPairSafe( pDiv, pPair, pPair2 )
117 MEM_FREE_FXU( p, Fxu_Pair, 1, pPair );
118 MEM_FREE_FXU( p, Fxu_Double, 1, pDiv );
119 }
120 Fxu_MatrixForEachSingleSafe( p, pSingle, pSingle2 )
121 MEM_FREE_FXU( p, Fxu_Single, 1, pSingle );
122 // delete the entries
123 Fxu_MatrixForEachCube( p, pCube )
124 Fxu_CubeForEachLiteralSafe( pCube, pLit, pLit2 )
125 MEM_FREE_FXU( p, Fxu_Lit, 1, pLit );
126 // delete the cubes
127 Fxu_MatrixForEachCubeSafe( p, pCube, pCube2 )
128 MEM_FREE_FXU( p, Fxu_Cube, 1, pCube );
129 // delete the vars
130 Fxu_MatrixForEachVariableSafe( p, pVar, pVar2 )
131 MEM_FREE_FXU( p, Fxu_Var, 1, pVar );
132 }
133#else
134 Extra_MmFixedStop( p->pMemMan );
135#endif
136
137 Vec_PtrFree( p->vPairs );
138 ABC_FREE( p->pppPairs );
139 ABC_FREE( p->ppPairs );
140// ABC_FREE( p->pPairsTemp );
141 ABC_FREE( p->pTable );
142 ABC_FREE( p->ppVars );
143 ABC_FREE( p );
144}
#define ABC_FREE(obj)
Definition abc_global.h:267
void Extra_MmFixedStop(Extra_MmFixed_t *p)
void Fxu_HeapDoubleStop(Fxu_HeapDouble *p)
Definition fxuHeapD.c:99
void Fxu_HeapDoubleCheck(Fxu_HeapDouble *p)
Definition fxuHeapD.c:152
void Fxu_HeapSingleStop(Fxu_HeapSingle *p)
Definition fxuHeapS.c:99
#define Fxu_DoubleForEachPairSafe(Div, Pair, Pair2)
Definition fxuInt.h:361
#define Fxu_MatrixForEachCubeSafe(Matrix, Cube, Cube2)
Definition fxuInt.h:298
#define Fxu_MatrixForEachDoubleSafe(Matrix, Div, Div2, Index)
Definition fxuInt.h:333
#define Fxu_MatrixForEachCube(Matrix, Cube)
Definition fxuInt.h:294
#define Fxu_CubeForEachLiteralSafe(Cube, Lit, Lit2)
Definition fxuInt.h:342
#define Fxu_MatrixForEachSingleSafe(Matrix, Single, Single2)
Definition fxuInt.h:316
#define Fxu_MatrixForEachVariableSafe(Matrix, Var, Var2)
Definition fxuInt.h:307
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Fxu_MatrixDelLiteral()

void Fxu_MatrixDelLiteral ( Fxu_Matrix * p,
Fxu_Lit * pLit )

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

Synopsis [Deletes the literal fromthe matrix.]

Description []

SideEffects []

SeeAlso []

Definition at line 252 of file fxuMatrix.c.

253{
254 // delete the literal
255 Fxu_ListCubeDelLiteral( pLit->pCube, pLit );
256 Fxu_ListVarDelLiteral( pLit->pVar, pLit );
257 MEM_FREE_FXU( p, Fxu_Lit, 1, pLit );
258 // increment the literal counter
259 p->nEntries--;
260}
void Fxu_ListCubeDelLiteral(Fxu_Cube *pCube, Fxu_Lit *pLit)
Definition fxuList.c:314
void Fxu_ListVarDelLiteral(Fxu_Var *pVar, Fxu_Lit *pLit)
Definition fxuList.c:373
Here is the call graph for this function: