ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
fxuInt.h
Go to the documentation of this file.
1
18
19#ifndef ABC__opt__fxu__fxuInt_h
20#define ABC__opt__fxu__fxuInt_h
21
22
26
27#include "base/abc/abc.h"
28
30
31
35
36// uncomment this macro to switch to standard memory management
37//#define USE_SYSTEM_MEMORY_MANAGEMENT
38
42
43/*
44 Here is an informal description of the FX data structure.
45 (1) The sparse matrix is filled with literals, associated with
46 cubes (row) and variables (columns). The matrix contains
47 all the cubes of all the nodes in the network.
48 (2) A cube is associated with
49 (a) its literals in the matrix,
50 (b) the output variable of the node, to which this cube belongs,
51 (3) A variable is associated with
52 (a) its literals in the matrix and
53 (b) the list of cube pairs in the cover, for which it is the output
54 (4) A cube pair is associated with two cubes and contains the counters
55 of literals in the base and in the cubes without the base
56 (5) A double-cube divisor is associated with list of all cube pairs
57 that produce it and its current weight (which is updated automatically
58 each time a new pair is added or an old pair is removed).
59 (6) A single-cube divisor is associated the pair of variables.
60*/
61
62// sparse matrix
63typedef struct FxuMatrix Fxu_Matrix; // the sparse matrix
64
65// sparse matrix contents: cubes (rows), vars (columns), literals (entries)
66typedef struct FxuCube Fxu_Cube; // one cube in the sparse matrix
67typedef struct FxuVar Fxu_Var; // one literal in the sparse matrix
68typedef struct FxuLit Fxu_Lit; // one entry in the sparse matrix
69
70// double cube divisors
71typedef struct FxuPair Fxu_Pair; // the pair of cubes
72typedef struct FxuDouble Fxu_Double; // the double-cube divisor
73typedef struct FxuSingle Fxu_Single; // the two-literal single-cube divisor
74
75// various lists
76typedef struct FxuListCube Fxu_ListCube; // the list of cubes
77typedef struct FxuListVar Fxu_ListVar; // the list of literals
78typedef struct FxuListLit Fxu_ListLit; // the list of entries
79typedef struct FxuListPair Fxu_ListPair; // the list of pairs
80typedef struct FxuListDouble Fxu_ListDouble; // the list of divisors
81typedef struct FxuListSingle Fxu_ListSingle; // the list of single-cube divisors
82
83// various heaps
84typedef struct FxuHeapDouble Fxu_HeapDouble; // the heap of divisors
85typedef struct FxuHeapSingle Fxu_HeapSingle; // the heap of variables
86
87
88// various lists
89
90// the list of cubes in the sparse matrix
97
98// the list of literals in the sparse matrix
105
106// the list of entries in the sparse matrix
113
114// the list of cube pair in the sparse matrix
121
122// the list of divisors in the sparse matrix
129
130// the list of divisors in the sparse matrix
137
138
139// various heaps
140
141// the heap of double cube divisors by weight
149
150// the heap of variable by their occurrence in the cubes
158
159
160
161// sparse matrix
162struct FxuMatrix // ~ 30 words
163{
164 // the cubes
165 Fxu_ListCube lCubes; // the double linked list of cubes
166 // the values (binary literals)
167 Fxu_ListVar lVars; // the double linked list of variables
168 Fxu_Var ** ppVars; // the array of variables
169 // the double cube divisors
170 Fxu_ListDouble * pTable; // the hash table of divisors
171 int nTableSize; // the hash table size
172 int nDivs; // the number of divisors in the table
173 int nDivsTotal; // the number of divisors in the table
174 Fxu_HeapDouble * pHeapDouble; // the heap of divisors by weight
175 // the single cube divisors
176 Fxu_ListSingle lSingles; // the linked list of single cube divisors
177 Fxu_HeapSingle * pHeapSingle; // the heap of variables by the number of literals in the matrix
178 int nWeightLimit;// the limit on weight of single cube divisors collected
179 int nSingleTotal;// the total number of single cube divisors
180 // storage for cube pairs
183 // temporary storage for cubes
186 // temporary storage for variables
189 // temporary storage for pairs
191 // statistics
192 int nEntries; // the total number of entries in the sparse matrix
193 int nDivs1; // the single cube divisors taken
194 int nDivs2; // the double cube divisors taken
195 int nDivs3; // the double cube divisors with complement
196 // memory manager
197 Extra_MmFixed_t * pMemMan; // the memory manager for all small sized entries
198};
199
200// the cube in the sparse matrix
201struct FxuCube // 9 words
202{
203 int iCube; // the number of this cube in the cover
204 Fxu_Cube * pFirst; // the pointer to the first cube of this cover
205 Fxu_Var * pVar; // the variable representing the output of the cover
206 Fxu_ListLit lLits; // the row in the table
207 Fxu_Cube * pPrev; // the previous cube
208 Fxu_Cube * pNext; // the next cube
209 Fxu_Cube * pOrder; // the specialized linked list of cubes
210};
211
212// the variable in the sparse matrix
213struct FxuVar // 10 words
214{
215 int iVar; // the number of this variable
216 int nCubes; // the number of cubes assoc with this var
217 Fxu_Cube * pFirst; // the first cube assoc with this var
218 Fxu_Pair *** ppPairs; // the pairs of cubes assoc with this var
219 Fxu_ListLit lLits; // the column in the table
220 Fxu_Var * pPrev; // the previous variable
221 Fxu_Var * pNext; // the next variable
222 Fxu_Var * pOrder; // the specialized linked list of variables
223};
224
225// the literal entry in the sparse matrix
226struct FxuLit // 8 words
227{
228 int iVar; // the number of this variable
229 int iCube; // the number of this cube
230 Fxu_Cube * pCube; // the cube of this literal
231 Fxu_Var * pVar; // the variable of this literal
232 Fxu_Lit * pHPrev; // prev lit in the cube
233 Fxu_Lit * pHNext; // next lit in the cube
234 Fxu_Lit * pVPrev; // prev lit of the var
235 Fxu_Lit * pVNext; // next lit of the var
236};
237
238// the cube pair
239struct FxuPair // 10 words
240{
241 int nLits1; // the number of literals in the two cubes
242 int nLits2; // the number of literals in the two cubes
243 int nBase; // the number of literals in the base
244 Fxu_Double * pDiv; // the divisor of this pair
245 Fxu_Cube * pCube1; // the first cube of the pair
246 Fxu_Cube * pCube2; // the second cube of the pair
247 int iCube1; // the first cube of the pair
248 int iCube2; // the second cube of the pair
249 Fxu_Pair * pDPrev; // the previous pair in the divisor
250 Fxu_Pair * pDNext; // the next pair in the divisor
251};
252
253// the double cube divisor
254struct FxuDouble // 10 words
255{
256 int Num; // the unique number of this divisor
257 int HNum; // the heap number of this divisor
258 int Weight; // the weight of this divisor
259 unsigned Key; // the hash key of this divisor
260 Fxu_ListPair lPairs; // the pairs of cubes, which produce this divisor
261 Fxu_Double * pPrev; // the previous divisor in the table
262 Fxu_Double * pNext; // the next divisor in the table
263 Fxu_Double * pOrder; // the specialized linked list of divisors
264};
265
266// the single cube divisor
267struct FxuSingle // 7 words
268{
269 int Num; // the unique number of this divisor
270 int HNum; // the heap number of this divisor
271 int Weight; // the weight of this divisor
272 Fxu_Var * pVar1; // the first variable of the single-cube divisor
273 Fxu_Var * pVar2; // the second variable of the single-cube divisor
274 Fxu_Single * pPrev; // the previous divisor in the list
275 Fxu_Single * pNext; // the next divisor in the list
276};
277
281
282// minimum/maximum
283#define Fxu_Min( a, b ) ( ((a)<(b))? (a):(b) )
284#define Fxu_Max( a, b ) ( ((a)>(b))? (a):(b) )
285
286// selection of the minimum/maximum cube in the pair
287#define Fxu_PairMinCube( pPair ) (((pPair)->iCube1 < (pPair)->iCube2)? (pPair)->pCube1: (pPair)->pCube2)
288#define Fxu_PairMaxCube( pPair ) (((pPair)->iCube1 > (pPair)->iCube2)? (pPair)->pCube1: (pPair)->pCube2)
289#define Fxu_PairMinCubeInt( pPair ) (((pPair)->iCube1 < (pPair)->iCube2)? (pPair)->iCube1: (pPair)->iCube2)
290#define Fxu_PairMaxCubeInt( pPair ) (((pPair)->iCube1 > (pPair)->iCube2)? (pPair)->iCube1: (pPair)->iCube2)
291
292// iterators
293
294#define Fxu_MatrixForEachCube( Matrix, Cube )\
295 for ( Cube = (Matrix)->lCubes.pHead;\
296 Cube;\
297 Cube = Cube->pNext )
298#define Fxu_MatrixForEachCubeSafe( Matrix, Cube, Cube2 )\
299 for ( Cube = (Matrix)->lCubes.pHead, Cube2 = (Cube? Cube->pNext: NULL);\
300 Cube;\
301 Cube = Cube2, Cube2 = (Cube? Cube->pNext: NULL) )
302
303#define Fxu_MatrixForEachVariable( Matrix, Var )\
304 for ( Var = (Matrix)->lVars.pHead;\
305 Var;\
306 Var = Var->pNext )
307#define Fxu_MatrixForEachVariableSafe( Matrix, Var, Var2 )\
308 for ( Var = (Matrix)->lVars.pHead, Var2 = (Var? Var->pNext: NULL);\
309 Var;\
310 Var = Var2, Var2 = (Var? Var->pNext: NULL) )
311
312#define Fxu_MatrixForEachSingle( Matrix, Single )\
313 for ( Single = (Matrix)->lSingles.pHead;\
314 Single;\
315 Single = Single->pNext )
316#define Fxu_MatrixForEachSingleSafe( Matrix, Single, Single2 )\
317 for ( Single = (Matrix)->lSingles.pHead, Single2 = (Single? Single->pNext: NULL);\
318 Single;\
319 Single = Single2, Single2 = (Single? Single->pNext: NULL) )
320
321#define Fxu_TableForEachDouble( Matrix, Key, Div )\
322 for ( Div = (Matrix)->pTable[Key].pHead;\
323 Div;\
324 Div = Div->pNext )
325#define Fxu_TableForEachDoubleSafe( Matrix, Key, Div, Div2 )\
326 for ( Div = (Matrix)->pTable[Key].pHead, Div2 = (Div? Div->pNext: NULL);\
327 Div;\
328 Div = Div2, Div2 = (Div? Div->pNext: NULL) )
329
330#define Fxu_MatrixForEachDouble( Matrix, Div, Index )\
331 for ( Index = 0; Index < (Matrix)->nTableSize; Index++ )\
332 Fxu_TableForEachDouble( Matrix, Index, Div )
333#define Fxu_MatrixForEachDoubleSafe( Matrix, Div, Div2, Index )\
334 for ( Index = 0; Index < (Matrix)->nTableSize; Index++ )\
335 Fxu_TableForEachDoubleSafe( Matrix, Index, Div, Div2 )
336
337
338#define Fxu_CubeForEachLiteral( Cube, Lit )\
339 for ( Lit = (Cube)->lLits.pHead;\
340 Lit;\
341 Lit = Lit->pHNext )
342#define Fxu_CubeForEachLiteralSafe( Cube, Lit, Lit2 )\
343 for ( Lit = (Cube)->lLits.pHead, Lit2 = (Lit? Lit->pHNext: NULL);\
344 Lit;\
345 Lit = Lit2, Lit2 = (Lit? Lit->pHNext: NULL) )
346
347#define Fxu_VarForEachLiteral( Var, Lit )\
348 for ( Lit = (Var)->lLits.pHead;\
349 Lit;\
350 Lit = Lit->pVNext )
351
352#define Fxu_CubeForEachDivisor( Cube, Div )\
353 for ( Div = (Cube)->lDivs.pHead;\
354 Div;\
355 Div = Div->pCNext )
356
357#define Fxu_DoubleForEachPair( Div, Pair )\
358 for ( Pair = (Div)->lPairs.pHead;\
359 Pair;\
360 Pair = Pair->pDNext )
361#define Fxu_DoubleForEachPairSafe( Div, Pair, Pair2 )\
362 for ( Pair = (Div)->lPairs.pHead, Pair2 = (Pair? Pair->pDNext: NULL);\
363 Pair;\
364 Pair = Pair2, Pair2 = (Pair? Pair->pDNext: NULL) )
365
366
367// iterator through the cube pairs belonging to the given cube
368#define Fxu_CubeForEachPair( pCube, pPair, i )\
369 for ( i = 0;\
370 i < pCube->pVar->nCubes && (((pPair) = (pCube)->pVar->ppPairs[(pCube)->iCube][i]), 1);\
371 i++ )\
372 if ( pPair == NULL ) {} else
373
374// iterator through all the items in the heap
375#define Fxu_HeapDoubleForEachItem( Heap, Div )\
376 for ( Heap->i = 1;\
377 Heap->i <= Heap->nItems && (Div = Heap->pTree[Heap->i]);\
378 Heap->i++ )
379#define Fxu_HeapSingleForEachItem( Heap, Single )\
380 for ( Heap->i = 1;\
381 Heap->i <= Heap->nItems && (Single = Heap->pTree[Heap->i]);\
382 Heap->i++ )
383
384// starting the rings
385#define Fxu_MatrixRingCubesStart( Matrix ) (((Matrix)->ppTailCubes = &((Matrix)->pOrderCubes)), ((Matrix)->pOrderCubes = NULL))
386#define Fxu_MatrixRingVarsStart( Matrix ) (((Matrix)->ppTailVars = &((Matrix)->pOrderVars)), ((Matrix)->pOrderVars = NULL))
387// stopping the rings
388#define Fxu_MatrixRingCubesStop( Matrix )
389#define Fxu_MatrixRingVarsStop( Matrix )
390// resetting the rings
391#define Fxu_MatrixRingCubesReset( Matrix ) (((Matrix)->pOrderCubes = NULL), ((Matrix)->ppTailCubes = NULL))
392#define Fxu_MatrixRingVarsReset( Matrix ) (((Matrix)->pOrderVars = NULL), ((Matrix)->ppTailVars = NULL))
393// adding to the rings
394#define Fxu_MatrixRingCubesAdd( Matrix, Cube) ((*((Matrix)->ppTailCubes) = Cube), ((Matrix)->ppTailCubes = &(Cube)->pOrder), ((Cube)->pOrder = (Fxu_Cube *)1))
395#define Fxu_MatrixRingVarsAdd( Matrix, Var ) ((*((Matrix)->ppTailVars ) = Var ), ((Matrix)->ppTailVars = &(Var)->pOrder ), ((Var)->pOrder = (Fxu_Var *)1))
396// iterating through the rings
397#define Fxu_MatrixForEachCubeInRing( Matrix, Cube )\
398 if ( (Matrix)->pOrderCubes )\
399 for ( Cube = (Matrix)->pOrderCubes;\
400 Cube != (Fxu_Cube *)1;\
401 Cube = Cube->pOrder )
402#define Fxu_MatrixForEachCubeInRingSafe( Matrix, Cube, Cube2 )\
403 if ( (Matrix)->pOrderCubes )\
404 for ( Cube = (Matrix)->pOrderCubes, Cube2 = ((Cube != (Fxu_Cube *)1)? Cube->pOrder: (Fxu_Cube *)1);\
405 Cube != (Fxu_Cube *)1;\
406 Cube = Cube2, Cube2 = ((Cube != (Fxu_Cube *)1)? Cube->pOrder: (Fxu_Cube *)1) )
407#define Fxu_MatrixForEachVarInRing( Matrix, Var )\
408 if ( (Matrix)->pOrderVars )\
409 for ( Var = (Matrix)->pOrderVars;\
410 Var != (Fxu_Var *)1;\
411 Var = Var->pOrder )
412#define Fxu_MatrixForEachVarInRingSafe( Matrix, Var, Var2 )\
413 if ( (Matrix)->pOrderVars )\
414 for ( Var = (Matrix)->pOrderVars, Var2 = ((Var != (Fxu_Var *)1)? Var->pOrder: (Fxu_Var *)1);\
415 Var != (Fxu_Var *)1;\
416 Var = Var2, Var2 = ((Var != (Fxu_Var *)1)? Var->pOrder: (Fxu_Var *)1) )
417// the procedures are related to the above macros
418extern void Fxu_MatrixRingCubesUnmark( Fxu_Matrix * p );
419extern void Fxu_MatrixRingVarsUnmark( Fxu_Matrix * p );
420
421
422// macros working with memory
423// MEM_ALLOC: allocate the given number (Size) of items of type (Type)
424// MEM_FREE: deallocate the pointer (Pointer) to the given number (Size) of items of type (Type)
425#ifdef USE_SYSTEM_MEMORY_MANAGEMENT
426#define MEM_ALLOC_FXU( Manager, Type, Size ) ((Type *)ABC_ALLOC( char, (Size) * sizeof(Type) ))
427#define MEM_FREE_FXU( Manager, Type, Size, Pointer ) if ( Pointer ) { ABC_FREE(Pointer); Pointer = NULL; }
428#else
429#define MEM_ALLOC_FXU( Manager, Type, Size )\
430 ((Type *)Fxu_MemFetch( Manager, (Size) * sizeof(Type) ))
431#define MEM_FREE_FXU( Manager, Type, Size, Pointer )\
432 if ( Pointer ) { Fxu_MemRecycle( Manager, (char *)(Pointer), (Size) * sizeof(Type) ); Pointer = NULL; }
433#endif
434
438
439/*===== fxu.c ====================================================*/
440extern char * Fxu_MemFetch( Fxu_Matrix * p, int nBytes );
441extern void Fxu_MemRecycle( Fxu_Matrix * p, char * pItem, int nBytes );
442/*===== fxuCreate.c ====================================================*/
443/*===== fxuReduce.c ====================================================*/
444/*===== fxuPrint.c ====================================================*/
445extern void Fxu_MatrixPrint( FILE * pFile, Fxu_Matrix * p );
446extern void Fxu_MatrixPrintDivisorProfile( FILE * pFile, Fxu_Matrix * p );
447/*===== fxuSelect.c ====================================================*/
448extern int Fxu_Select( Fxu_Matrix * p, Fxu_Single ** ppSingle, Fxu_Double ** ppDouble );
449extern int Fxu_SelectSCD( Fxu_Matrix * p, int Weight, Fxu_Var ** ppVar1, Fxu_Var ** ppVar2 );
450/*===== fxuUpdate.c ====================================================*/
451extern void Fxu_Update( Fxu_Matrix * p, Fxu_Single * pSingle, Fxu_Double * pDouble );
452extern void Fxu_UpdateDouble( Fxu_Matrix * p );
453extern void Fxu_UpdateSingle( Fxu_Matrix * p );
454/*===== fxuPair.c ====================================================*/
455extern void Fxu_PairCanonicize( Fxu_Cube ** ppCube1, Fxu_Cube ** ppCube2 );
456extern unsigned Fxu_PairHashKeyArray( Fxu_Matrix * p, int piVarsC1[], int piVarsC2[], int nVarsC1, int nVarsC2 );
457extern unsigned Fxu_PairHashKey( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2, int * pnBase, int * pnLits1, int * pnLits2 );
458extern unsigned Fxu_PairHashKeyMv( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2, int * pnBase, int * pnLits1, int * pnLits2 );
459extern int Fxu_PairCompare( Fxu_Pair * pPair1, Fxu_Pair * pPair2 );
460extern void Fxu_PairAllocStorage( Fxu_Var * pVar, int nCubes );
461extern void Fxu_PairFreeStorage( Fxu_Var * pVar );
462extern void Fxu_PairClearStorage( Fxu_Cube * pCube );
463extern Fxu_Pair * Fxu_PairAlloc( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2 );
464extern void Fxu_PairAdd( Fxu_Pair * pPair );
465/*===== fxuSingle.c ====================================================*/
466extern void Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax );
467extern void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar );
468extern int Fxu_SingleCountCoincidence( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVar2 );
469/*===== fxuMatrix.c ====================================================*/
470// matrix
472extern void Fxu_MatrixDelete( Fxu_Matrix * p );
473// double-cube divisor
474extern void Fxu_MatrixAddDivisor( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2 );
475extern void Fxu_MatrixDelDivisor( Fxu_Matrix * p, Fxu_Double * pDiv );
476// single-cube divisor
477extern void Fxu_MatrixAddSingle( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVar2, int Weight );
478// variable
480// cube
481extern Fxu_Cube * Fxu_MatrixAddCube( Fxu_Matrix * p, Fxu_Var * pVar, int iCube );
482// literal
483extern void Fxu_MatrixAddLiteral( Fxu_Matrix * p, Fxu_Cube * pCube, Fxu_Var * pVar );
484extern void Fxu_MatrixDelLiteral( Fxu_Matrix * p, Fxu_Lit * pLit );
485/*===== fxuList.c ====================================================*/
486// matrix -> variable
487extern void Fxu_ListMatrixAddVariable( Fxu_Matrix * p, Fxu_Var * pVar );
488extern void Fxu_ListMatrixDelVariable( Fxu_Matrix * p, Fxu_Var * pVar );
489// matrix -> cube
490extern void Fxu_ListMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube );
491extern void Fxu_ListMatrixDelCube( Fxu_Matrix * p, Fxu_Cube * pCube );
492// matrix -> single
493extern void Fxu_ListMatrixAddSingle( Fxu_Matrix * p, Fxu_Single * pSingle );
494extern void Fxu_ListMatrixDelSingle( Fxu_Matrix * p, Fxu_Single * pSingle );
495// table -> divisor
496extern void Fxu_ListTableAddDivisor( Fxu_Matrix * p, Fxu_Double * pDiv );
497extern void Fxu_ListTableDelDivisor( Fxu_Matrix * p, Fxu_Double * pDiv );
498// cube -> literal
499extern void Fxu_ListCubeAddLiteral( Fxu_Cube * pCube, Fxu_Lit * pLit );
500extern void Fxu_ListCubeDelLiteral( Fxu_Cube * pCube, Fxu_Lit * pLit );
501// var -> literal
502extern void Fxu_ListVarAddLiteral( Fxu_Var * pVar, Fxu_Lit * pLit );
503extern void Fxu_ListVarDelLiteral( Fxu_Var * pVar, Fxu_Lit * pLit );
504// divisor -> pair
505extern void Fxu_ListDoubleAddPairLast( Fxu_Double * pDiv, Fxu_Pair * pLink );
506extern void Fxu_ListDoubleAddPairFirst( Fxu_Double * pDiv, Fxu_Pair * pLink );
507extern void Fxu_ListDoubleAddPairMiddle( Fxu_Double * pDiv, Fxu_Pair * pSpot, Fxu_Pair * pLink );
508extern void Fxu_ListDoubleDelPair( Fxu_Double * pDiv, Fxu_Pair * pPair );
509/*===== fxuHeapDouble.c ====================================================*/
511extern void Fxu_HeapDoubleStop( Fxu_HeapDouble * p );
512extern void Fxu_HeapDoublePrint( FILE * pFile, Fxu_HeapDouble * p );
513extern void Fxu_HeapDoubleCheck( Fxu_HeapDouble * p );
514extern void Fxu_HeapDoubleCheckOne( Fxu_HeapDouble * p, Fxu_Double * pDiv );
515
516extern void Fxu_HeapDoubleInsert( Fxu_HeapDouble * p, Fxu_Double * pDiv );
517extern void Fxu_HeapDoubleUpdate( Fxu_HeapDouble * p, Fxu_Double * pDiv );
518extern void Fxu_HeapDoubleDelete( Fxu_HeapDouble * p, Fxu_Double * pDiv );
522/*===== fxuHeapSingle.c ====================================================*/
524extern void Fxu_HeapSingleStop( Fxu_HeapSingle * p );
525extern void Fxu_HeapSinglePrint( FILE * pFile, Fxu_HeapSingle * p );
526extern void Fxu_HeapSingleCheck( Fxu_HeapSingle * p );
527extern void Fxu_HeapSingleCheckOne( Fxu_HeapSingle * p, Fxu_Single * pSingle );
528
529extern void Fxu_HeapSingleInsert( Fxu_HeapSingle * p, Fxu_Single * pSingle );
530extern void Fxu_HeapSingleUpdate( Fxu_HeapSingle * p, Fxu_Single * pSingle );
531extern void Fxu_HeapSingleDelete( Fxu_HeapSingle * p, Fxu_Single * pSingle );
535
536
537
539
540#endif
541
545
#define ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
Cube * p
Definition exorList.c:222
struct Extra_MmFixed_t_ Extra_MmFixed_t
Definition extra.h:147
Fxu_HeapSingle * Fxu_HeapSingleStart()
FUNCTION DEFINITIONS ///.
Definition fxuHeapS.c:58
struct FxuListLit Fxu_ListLit
Definition fxuInt.h:78
void Fxu_ListTableDelDivisor(Fxu_Matrix *p, Fxu_Double *pDiv)
Definition fxuList.c:254
void Fxu_ListMatrixAddVariable(Fxu_Matrix *p, Fxu_Var *pVar)
DECLARATIONS ///.
Definition fxuList.c:45
void Fxu_HeapDoubleUpdate(Fxu_HeapDouble *p, Fxu_Double *pDiv)
Definition fxuHeapD.c:223
Fxu_Var * Fxu_MatrixAddVar(Fxu_Matrix *p)
Definition fxuMatrix.c:161
void Fxu_MatrixPrintDivisorProfile(FILE *pFile, Fxu_Matrix *p)
Definition fxuPrint.c:159
void Fxu_HeapDoubleStop(Fxu_HeapDouble *p)
Definition fxuHeapD.c:99
int Fxu_SingleCountCoincidence(Fxu_Matrix *p, Fxu_Var *pVar1, Fxu_Var *pVar2)
Definition fxuSingle.c:241
unsigned Fxu_PairHashKeyArray(Fxu_Matrix *p, int piVarsC1[], int piVarsC2[], int nVarsC1, int nVarsC2)
Definition fxuPair.c:137
struct FxuVar Fxu_Var
Definition fxuInt.h:67
Fxu_Single * Fxu_HeapSingleReadMax(Fxu_HeapSingle *p)
Definition fxuHeapS.c:275
void Fxu_ListCubeDelLiteral(Fxu_Cube *pCube, Fxu_Lit *pLit)
Definition fxuList.c:314
void Fxu_HeapDoublePrint(FILE *pFile, Fxu_HeapDouble *p)
Definition fxuHeapD.c:117
void Fxu_ListMatrixAddCube(Fxu_Matrix *p, Fxu_Cube *pCube)
Definition fxuList.c:104
void Fxu_HeapSingleUpdate(Fxu_HeapSingle *p, Fxu_Single *pSingle)
Definition fxuHeapS.c:226
void Fxu_PairClearStorage(Fxu_Cube *pCube)
Definition fxuPair.c:476
void Fxu_PairFreeStorage(Fxu_Var *pVar)
Definition fxuPair.c:499
Fxu_Single * Fxu_HeapSingleGetMax(Fxu_HeapSingle *p)
Definition fxuHeapS.c:293
void Fxu_HeapSingleInsert(Fxu_HeapSingle *p, Fxu_Single *pSingle)
Definition fxuHeapS.c:204
void Fxu_UpdateDouble(Fxu_Matrix *p)
Definition fxuUpdate.c:219
Fxu_HeapDouble * Fxu_HeapDoubleStart()
FUNCTION DEFINITIONS ///.
Definition fxuHeapD.c:58
void Fxu_UpdateSingle(Fxu_Matrix *p)
Definition fxuUpdate.c:149
Fxu_Pair * Fxu_PairAlloc(Fxu_Matrix *p, Fxu_Cube *pCube1, Fxu_Cube *pCube2)
Definition fxuPair.c:519
void Fxu_ListVarDelLiteral(Fxu_Var *pVar, Fxu_Lit *pLit)
Definition fxuList.c:373
void Fxu_MatrixPrint(FILE *pFile, Fxu_Matrix *p)
DECLARATIONS ///.
Definition fxuPrint.c:43
void Fxu_ListMatrixDelVariable(Fxu_Matrix *p, Fxu_Var *pVar)
Definition fxuList.c:76
int Fxu_PairCompare(Fxu_Pair *pPair1, Fxu_Pair *pPair2)
Definition fxuPair.c:236
void Fxu_ListMatrixAddSingle(Fxu_Matrix *p, Fxu_Single *pSingle)
Definition fxuList.c:163
void Fxu_HeapDoubleCheckOne(Fxu_HeapDouble *p, Fxu_Double *pDiv)
Definition fxuHeapD.c:173
void Fxu_ListDoubleAddPairLast(Fxu_Double *pDiv, Fxu_Pair *pLink)
Definition fxuList.c:402
void Fxu_MatrixAddLiteral(Fxu_Matrix *p, Fxu_Cube *pCube, Fxu_Var *pVar)
Definition fxuMatrix.c:205
void Fxu_HeapSingleStop(Fxu_HeapSingle *p)
Definition fxuHeapS.c:99
Fxu_Matrix * Fxu_MatrixAllocate()
DECLARATIONS ///.
Definition fxuMatrix.c:43
struct FxuSingle Fxu_Single
Definition fxuInt.h:73
void Fxu_ListMatrixDelCube(Fxu_Matrix *p, Fxu_Cube *pCube)
Definition fxuList.c:135
void Fxu_HeapDoubleCheck(Fxu_HeapDouble *p)
Definition fxuHeapD.c:152
unsigned Fxu_PairHashKey(Fxu_Matrix *p, Fxu_Cube *pCube1, Fxu_Cube *pCube2, int *pnBase, int *pnLits1, int *pnLits2)
Definition fxuPair.c:164
void Fxu_HeapSingleDelete(Fxu_HeapSingle *p, Fxu_Single *pSingle)
Definition fxuHeapS.c:251
void Fxu_ListDoubleAddPairFirst(Fxu_Double *pDiv, Fxu_Pair *pLink)
Definition fxuList.c:433
int Fxu_HeapDoubleReadMaxWeight(Fxu_HeapDouble *p)
Definition fxuHeapD.c:319
struct FxuHeapDouble Fxu_HeapDouble
Definition fxuInt.h:84
void Fxu_HeapSingleCheckOne(Fxu_HeapSingle *p, Fxu_Single *pSingle)
Definition fxuHeapS.c:176
void Fxu_MatrixDelDivisor(Fxu_Matrix *p, Fxu_Double *pDiv)
Definition fxuMatrix.c:233
void Fxu_MatrixDelete(Fxu_Matrix *p)
Definition fxuMatrix.c:96
void Fxu_PairAllocStorage(Fxu_Var *pVar, int nCubes)
Definition fxuPair.c:452
typedefABC_NAMESPACE_HEADER_START struct FxuMatrix Fxu_Matrix
INCLUDES ///.
Definition fxuInt.h:63
void Fxu_MemRecycle(Fxu_Matrix *p, char *pItem, int nBytes)
Definition fxu.c:247
void Fxu_HeapDoubleDelete(Fxu_HeapDouble *p, Fxu_Double *pDiv)
Definition fxuHeapD.c:250
void Fxu_PairAdd(Fxu_Pair *pPair)
Definition fxuPair.c:543
void Fxu_HeapDoubleInsert(Fxu_HeapDouble *p, Fxu_Double *pDiv)
Definition fxuHeapD.c:201
void Fxu_MatrixDelLiteral(Fxu_Matrix *p, Fxu_Lit *pLit)
Definition fxuMatrix.c:252
struct FxuListDouble Fxu_ListDouble
Definition fxuInt.h:80
struct FxuPair Fxu_Pair
Definition fxuInt.h:71
int Fxu_SelectSCD(Fxu_Matrix *p, int Weight, Fxu_Var **ppVar1, Fxu_Var **ppVar2)
Definition fxuSelect.c:525
void Fxu_ListTableAddDivisor(Fxu_Matrix *p, Fxu_Double *pDiv)
Definition fxuList.c:222
struct FxuListSingle Fxu_ListSingle
Definition fxuInt.h:81
struct FxuCube Fxu_Cube
Definition fxuInt.h:66
void Fxu_PairCanonicize(Fxu_Cube **ppCube1, Fxu_Cube **ppCube2)
FUNCTION DEFINITIONS ///.
Definition fxuPair.c:75
struct FxuDouble Fxu_Double
Definition fxuInt.h:72
void Fxu_ListCubeAddLiteral(Fxu_Cube *pCube, Fxu_Lit *pLit)
Definition fxuList.c:283
int Fxu_Select(Fxu_Matrix *p, Fxu_Single **ppSingle, Fxu_Double **ppDouble)
FUNCTION DEFINITIONS ///.
Definition fxuSelect.c:57
struct FxuListVar Fxu_ListVar
Definition fxuInt.h:77
void Fxu_HeapSingleCheck(Fxu_HeapSingle *p)
Definition fxuHeapS.c:155
int Fxu_HeapSingleReadMaxWeight(Fxu_HeapSingle *p)
Definition fxuHeapS.c:321
struct FxuListPair Fxu_ListPair
Definition fxuInt.h:79
void Fxu_MatrixComputeSingles(Fxu_Matrix *p, int fUse0, int nSingleMax)
FUNCTION DEFINITIONS ///.
Definition fxuSingle.c:47
void Fxu_MatrixRingCubesUnmark(Fxu_Matrix *p)
Definition fxu.c:185
void Fxu_MatrixAddDivisor(Fxu_Matrix *p, Fxu_Cube *pCube1, Fxu_Cube *pCube2)
Definition fxuMatrix.c:301
void Fxu_Update(Fxu_Matrix *p, Fxu_Single *pSingle, Fxu_Double *pDouble)
FUNCTION DEFINITIONS ///.
Definition fxuUpdate.c:57
Fxu_Cube * Fxu_MatrixAddCube(Fxu_Matrix *p, Fxu_Var *pVar, int iCube)
Definition fxuMatrix.c:183
void Fxu_HeapSinglePrint(FILE *pFile, Fxu_HeapSingle *p)
Definition fxuHeapS.c:120
struct FxuListCube Fxu_ListCube
Definition fxuInt.h:76
void Fxu_ListMatrixDelSingle(Fxu_Matrix *p, Fxu_Single *pSingle)
Definition fxuList.c:194
void Fxu_ListDoubleAddPairMiddle(Fxu_Double *pDiv, Fxu_Pair *pSpot, Fxu_Pair *pLink)
Definition fxuList.c:466
char * Fxu_MemFetch(Fxu_Matrix *p, int nBytes)
FUNCTION DEFINITIONS ///.
Definition fxu.c:227
unsigned Fxu_PairHashKeyMv(Fxu_Matrix *p, Fxu_Cube *pCube1, Fxu_Cube *pCube2, int *pnBase, int *pnLits1, int *pnLits2)
Fxu_Double * Fxu_HeapDoubleGetMax(Fxu_HeapDouble *p)
Definition fxuHeapD.c:291
void Fxu_MatrixComputeSinglesOne(Fxu_Matrix *p, Fxu_Var *pVar)
Definition fxuSingle.c:184
void Fxu_ListDoubleDelPair(Fxu_Double *pDiv, Fxu_Pair *pPair)
Definition fxuList.c:489
struct FxuHeapSingle Fxu_HeapSingle
Definition fxuInt.h:85
struct FxuLit Fxu_Lit
Definition fxuInt.h:68
void Fxu_ListVarAddLiteral(Fxu_Var *pVar, Fxu_Lit *pLit)
Definition fxuList.c:342
void Fxu_MatrixRingVarsUnmark(Fxu_Matrix *p)
Definition fxu.c:206
Fxu_Double * Fxu_HeapDoubleReadMax(Fxu_HeapDouble *p)
Definition fxuHeapD.c:273
void Fxu_MatrixAddSingle(Fxu_Matrix *p, Fxu_Var *pVar1, Fxu_Var *pVar2, int Weight)
Definition fxuMatrix.c:274
Fxu_Cube * pOrder
Definition fxuInt.h:209
Fxu_Cube * pFirst
Definition fxuInt.h:204
int iCube
Definition fxuInt.h:203
Fxu_ListLit lLits
Definition fxuInt.h:206
Fxu_Cube * pNext
Definition fxuInt.h:208
Fxu_Cube * pPrev
Definition fxuInt.h:207
Fxu_Var * pVar
Definition fxuInt.h:205
int Num
Definition fxuInt.h:256
Fxu_Double * pPrev
Definition fxuInt.h:261
int Weight
Definition fxuInt.h:258
Fxu_Double * pOrder
Definition fxuInt.h:263
Fxu_ListPair lPairs
Definition fxuInt.h:260
Fxu_Double * pNext
Definition fxuInt.h:262
int HNum
Definition fxuInt.h:257
unsigned Key
Definition fxuInt.h:259
Fxu_Double ** pTree
Definition fxuInt.h:144
int nItemsAlloc
Definition fxuInt.h:146
Fxu_Single ** pTree
Definition fxuInt.h:153
int nItemsAlloc
Definition fxuInt.h:155
Fxu_Cube * pTail
Definition fxuInt.h:94
Fxu_Cube * pHead
Definition fxuInt.h:93
int nItems
Definition fxuInt.h:95
Fxu_Double * pHead
Definition fxuInt.h:125
Fxu_Double * pTail
Definition fxuInt.h:126
int nItems
Definition fxuInt.h:111
Fxu_Lit * pTail
Definition fxuInt.h:110
Fxu_Lit * pHead
Definition fxuInt.h:109
Fxu_Pair * pHead
Definition fxuInt.h:117
Fxu_Pair * pTail
Definition fxuInt.h:118
int nItems
Definition fxuInt.h:119
Fxu_Single * pHead
Definition fxuInt.h:133
Fxu_Single * pTail
Definition fxuInt.h:134
Fxu_Var * pTail
Definition fxuInt.h:102
int nItems
Definition fxuInt.h:103
Fxu_Var * pHead
Definition fxuInt.h:101
Fxu_Lit * pHNext
Definition fxuInt.h:233
Fxu_Lit * pVNext
Definition fxuInt.h:235
Fxu_Lit * pVPrev
Definition fxuInt.h:234
Fxu_Cube * pCube
Definition fxuInt.h:230
Fxu_Lit * pHPrev
Definition fxuInt.h:232
int iVar
Definition fxuInt.h:228
Fxu_Var * pVar
Definition fxuInt.h:231
int iCube
Definition fxuInt.h:229
int nDivsTotal
Definition fxuInt.h:173
Vec_Ptr_t * vPairs
Definition fxuInt.h:190
int nDivs1
Definition fxuInt.h:193
Fxu_Var ** ppTailVars
Definition fxuInt.h:188
int nSingleTotal
Definition fxuInt.h:179
Fxu_ListVar lVars
Definition fxuInt.h:167
int nDivs2
Definition fxuInt.h:194
int nTableSize
Definition fxuInt.h:171
Fxu_Pair *** pppPairs
Definition fxuInt.h:181
Fxu_Cube ** ppTailCubes
Definition fxuInt.h:185
Fxu_Cube * pOrderCubes
Definition fxuInt.h:184
int nWeightLimit
Definition fxuInt.h:178
Fxu_HeapDouble * pHeapDouble
Definition fxuInt.h:174
Fxu_Var * pOrderVars
Definition fxuInt.h:187
Extra_MmFixed_t * pMemMan
Definition fxuInt.h:197
int nEntries
Definition fxuInt.h:192
Fxu_Pair ** ppPairs
Definition fxuInt.h:182
Fxu_ListDouble * pTable
Definition fxuInt.h:170
Fxu_ListSingle lSingles
Definition fxuInt.h:176
Fxu_Var ** ppVars
Definition fxuInt.h:168
Fxu_ListCube lCubes
Definition fxuInt.h:165
int nDivs
Definition fxuInt.h:172
Fxu_HeapSingle * pHeapSingle
Definition fxuInt.h:177
int nDivs3
Definition fxuInt.h:195
int iCube1
Definition fxuInt.h:247
int nBase
Definition fxuInt.h:243
Fxu_Double * pDiv
Definition fxuInt.h:244
int nLits2
Definition fxuInt.h:242
Fxu_Cube * pCube1
Definition fxuInt.h:245
int nLits1
Definition fxuInt.h:241
int iCube2
Definition fxuInt.h:248
Fxu_Cube * pCube2
Definition fxuInt.h:246
Fxu_Pair * pDNext
Definition fxuInt.h:250
Fxu_Pair * pDPrev
Definition fxuInt.h:249
int Weight
Definition fxuInt.h:271
int Num
Definition fxuInt.h:269
Fxu_Var * pVar2
Definition fxuInt.h:273
Fxu_Single * pNext
Definition fxuInt.h:275
int HNum
Definition fxuInt.h:270
Fxu_Single * pPrev
Definition fxuInt.h:274
Fxu_Var * pVar1
Definition fxuInt.h:272
int nCubes
Definition fxuInt.h:216
Fxu_Var * pOrder
Definition fxuInt.h:222
int iVar
Definition fxuInt.h:215
Fxu_ListLit lLits
Definition fxuInt.h:219
Fxu_Pair *** ppPairs
Definition fxuInt.h:218
Fxu_Var * pPrev
Definition fxuInt.h:220
Fxu_Cube * pFirst
Definition fxuInt.h:217
Fxu_Var * pNext
Definition fxuInt.h:221
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42