00001
00019 #ifndef __FXU_INT_H__
00020 #define __FXU_INT_H__
00021
00025
00026 #include "extra.h"
00027 #include "vec.h"
00028
00032
00033
00034
00035
00039
00040
00041
00042
00043
00044
00045
00046
00047
00048
00049
00050
00051
00052
00053
00054
00055
00056
00057
00058
00059
00060 typedef struct FxuMatrix Fxu_Matrix;
00061
00062
00063 typedef struct FxuCube Fxu_Cube;
00064 typedef struct FxuVar Fxu_Var;
00065 typedef struct FxuLit Fxu_Lit;
00066
00067
00068 typedef struct FxuPair Fxu_Pair;
00069 typedef struct FxuDouble Fxu_Double;
00070 typedef struct FxuSingle Fxu_Single;
00071
00072
00073 typedef struct FxuListCube Fxu_ListCube;
00074 typedef struct FxuListVar Fxu_ListVar;
00075 typedef struct FxuListLit Fxu_ListLit;
00076 typedef struct FxuListPair Fxu_ListPair;
00077 typedef struct FxuListDouble Fxu_ListDouble;
00078 typedef struct FxuListSingle Fxu_ListSingle;
00079
00080
00081 typedef struct FxuHeapDouble Fxu_HeapDouble;
00082 typedef struct FxuHeapSingle Fxu_HeapSingle;
00083
00084
00085
00086
00087
00088 struct FxuListCube
00089 {
00090 Fxu_Cube * pHead;
00091 Fxu_Cube * pTail;
00092 int nItems;
00093 };
00094
00095
00096 struct FxuListVar
00097 {
00098 Fxu_Var * pHead;
00099 Fxu_Var * pTail;
00100 int nItems;
00101 };
00102
00103
00104 struct FxuListLit
00105 {
00106 Fxu_Lit * pHead;
00107 Fxu_Lit * pTail;
00108 int nItems;
00109 };
00110
00111
00112 struct FxuListPair
00113 {
00114 Fxu_Pair * pHead;
00115 Fxu_Pair * pTail;
00116 int nItems;
00117 };
00118
00119
00120 struct FxuListDouble
00121 {
00122 Fxu_Double * pHead;
00123 Fxu_Double * pTail;
00124 int nItems;
00125 };
00126
00127
00128 struct FxuListSingle
00129 {
00130 Fxu_Single * pHead;
00131 Fxu_Single * pTail;
00132 int nItems;
00133 };
00134
00135
00136
00137
00138
00139 struct FxuHeapDouble
00140 {
00141 Fxu_Double ** pTree;
00142 int nItems;
00143 int nItemsAlloc;
00144 int i;
00145 };
00146
00147
00148 struct FxuHeapSingle
00149 {
00150 Fxu_Single ** pTree;
00151 int nItems;
00152 int nItemsAlloc;
00153 int i;
00154 };
00155
00156
00157
00158
00159 struct FxuMatrix
00160 {
00161
00162 Fxu_ListCube lCubes;
00163
00164 Fxu_ListVar lVars;
00165 Fxu_Var ** ppVars;
00166
00167 Fxu_ListDouble * pTable;
00168 int nTableSize;
00169 int nDivs;
00170 int nDivsTotal;
00171 Fxu_HeapDouble * pHeapDouble;
00172
00173 Fxu_ListSingle lSingles;
00174 Fxu_HeapSingle * pHeapSingle;
00175 int nWeightLimit;
00176 int nSingleTotal;
00177
00178 Fxu_Pair *** pppPairs;
00179 Fxu_Pair ** ppPairs;
00180
00181 Fxu_Cube * pOrderCubes;
00182 Fxu_Cube ** ppTailCubes;
00183
00184 Fxu_Var * pOrderVars;
00185 Fxu_Var ** ppTailVars;
00186
00187 Vec_Ptr_t * vPairs;
00188
00189 int nEntries;
00190 int nDivs1;
00191 int nDivs2;
00192 int nDivs3;
00193
00194 Extra_MmFixed_t * pMemMan;
00195 };
00196
00197
00198 struct FxuCube
00199 {
00200 int iCube;
00201 Fxu_Cube * pFirst;
00202 Fxu_Var * pVar;
00203 Fxu_ListLit lLits;
00204 Fxu_Cube * pPrev;
00205 Fxu_Cube * pNext;
00206 Fxu_Cube * pOrder;
00207 };
00208
00209
00210 struct FxuVar
00211 {
00212 int iVar;
00213 int nCubes;
00214 Fxu_Cube * pFirst;
00215 Fxu_Pair *** ppPairs;
00216 Fxu_ListLit lLits;
00217 Fxu_Var * pPrev;
00218 Fxu_Var * pNext;
00219 Fxu_Var * pOrder;
00220 };
00221
00222
00223 struct FxuLit
00224 {
00225 int iVar;
00226 int iCube;
00227 Fxu_Cube * pCube;
00228 Fxu_Var * pVar;
00229 Fxu_Lit * pHPrev;
00230 Fxu_Lit * pHNext;
00231 Fxu_Lit * pVPrev;
00232 Fxu_Lit * pVNext;
00233 };
00234
00235
00236 struct FxuPair
00237 {
00238 int nLits1;
00239 int nLits2;
00240 int nBase;
00241 Fxu_Double * pDiv;
00242 Fxu_Cube * pCube1;
00243 Fxu_Cube * pCube2;
00244 int iCube1;
00245 int iCube2;
00246 Fxu_Pair * pDPrev;
00247 Fxu_Pair * pDNext;
00248 };
00249
00250
00251 struct FxuDouble
00252 {
00253 int Num;
00254 int HNum;
00255 int Weight;
00256 unsigned Key;
00257 Fxu_ListPair lPairs;
00258 Fxu_Double * pPrev;
00259 Fxu_Double * pNext;
00260 Fxu_Double * pOrder;
00261 };
00262
00263
00264 struct FxuSingle
00265 {
00266 int Num;
00267 int HNum;
00268 int Weight;
00269 Fxu_Var * pVar1;
00270 Fxu_Var * pVar2;
00271 Fxu_Single * pPrev;
00272 Fxu_Single * pNext;
00273 };
00274
00278
00279
00280 #define Fxu_Min( a, b ) ( ((a)<(b))? (a):(b) )
00281 #define Fxu_Max( a, b ) ( ((a)>(b))? (a):(b) )
00282
00283
00284 #define Fxu_PairMinCube( pPair ) (((pPair)->iCube1 < (pPair)->iCube2)? (pPair)->pCube1: (pPair)->pCube2)
00285 #define Fxu_PairMaxCube( pPair ) (((pPair)->iCube1 > (pPair)->iCube2)? (pPair)->pCube1: (pPair)->pCube2)
00286 #define Fxu_PairMinCubeInt( pPair ) (((pPair)->iCube1 < (pPair)->iCube2)? (pPair)->iCube1: (pPair)->iCube2)
00287 #define Fxu_PairMaxCubeInt( pPair ) (((pPair)->iCube1 > (pPair)->iCube2)? (pPair)->iCube1: (pPair)->iCube2)
00288
00289
00290
00291 #define Fxu_MatrixForEachCube( Matrix, Cube )\
00292 for ( Cube = (Matrix)->lCubes.pHead;\
00293 Cube;\
00294 Cube = Cube->pNext )
00295 #define Fxu_MatrixForEachCubeSafe( Matrix, Cube, Cube2 )\
00296 for ( Cube = (Matrix)->lCubes.pHead, Cube2 = (Cube? Cube->pNext: NULL);\
00297 Cube;\
00298 Cube = Cube2, Cube2 = (Cube? Cube->pNext: NULL) )
00299
00300 #define Fxu_MatrixForEachVariable( Matrix, Var )\
00301 for ( Var = (Matrix)->lVars.pHead;\
00302 Var;\
00303 Var = Var->pNext )
00304 #define Fxu_MatrixForEachVariableSafe( Matrix, Var, Var2 )\
00305 for ( Var = (Matrix)->lVars.pHead, Var2 = (Var? Var->pNext: NULL);\
00306 Var;\
00307 Var = Var2, Var2 = (Var? Var->pNext: NULL) )
00308
00309 #define Fxu_MatrixForEachSingle( Matrix, Single )\
00310 for ( Single = (Matrix)->lSingles.pHead;\
00311 Single;\
00312 Single = Single->pNext )
00313 #define Fxu_MatrixForEachSingleSafe( Matrix, Single, Single2 )\
00314 for ( Single = (Matrix)->lSingles.pHead, Single2 = (Single? Single->pNext: NULL);\
00315 Single;\
00316 Single = Single2, Single2 = (Single? Single->pNext: NULL) )
00317
00318 #define Fxu_TableForEachDouble( Matrix, Key, Div )\
00319 for ( Div = (Matrix)->pTable[Key].pHead;\
00320 Div;\
00321 Div = Div->pNext )
00322 #define Fxu_TableForEachDoubleSafe( Matrix, Key, Div, Div2 )\
00323 for ( Div = (Matrix)->pTable[Key].pHead, Div2 = (Div? Div->pNext: NULL);\
00324 Div;\
00325 Div = Div2, Div2 = (Div? Div->pNext: NULL) )
00326
00327 #define Fxu_MatrixForEachDouble( Matrix, Div, Index )\
00328 for ( Index = 0; Index < (Matrix)->nTableSize; Index++ )\
00329 Fxu_TableForEachDouble( Matrix, Index, Div )
00330 #define Fxu_MatrixForEachDoubleSafe( Matrix, Div, Div2, Index )\
00331 for ( Index = 0; Index < (Matrix)->nTableSize; Index++ )\
00332 Fxu_TableForEachDoubleSafe( Matrix, Index, Div, Div2 )
00333
00334
00335 #define Fxu_CubeForEachLiteral( Cube, Lit )\
00336 for ( Lit = (Cube)->lLits.pHead;\
00337 Lit;\
00338 Lit = Lit->pHNext )
00339 #define Fxu_CubeForEachLiteralSafe( Cube, Lit, Lit2 )\
00340 for ( Lit = (Cube)->lLits.pHead, Lit2 = (Lit? Lit->pHNext: NULL);\
00341 Lit;\
00342 Lit = Lit2, Lit2 = (Lit? Lit->pHNext: NULL) )
00343
00344 #define Fxu_VarForEachLiteral( Var, Lit )\
00345 for ( Lit = (Var)->lLits.pHead;\
00346 Lit;\
00347 Lit = Lit->pVNext )
00348
00349 #define Fxu_CubeForEachDivisor( Cube, Div )\
00350 for ( Div = (Cube)->lDivs.pHead;\
00351 Div;\
00352 Div = Div->pCNext )
00353
00354 #define Fxu_DoubleForEachPair( Div, Pair )\
00355 for ( Pair = (Div)->lPairs.pHead;\
00356 Pair;\
00357 Pair = Pair->pDNext )
00358 #define Fxu_DoubleForEachPairSafe( Div, Pair, Pair2 )\
00359 for ( Pair = (Div)->lPairs.pHead, Pair2 = (Pair? Pair->pDNext: NULL);\
00360 Pair;\
00361 Pair = Pair2, Pair2 = (Pair? Pair->pDNext: NULL) )
00362
00363
00364
00365 #define Fxu_CubeForEachPair( pCube, pPair, i )\
00366 for ( i = 0;\
00367 i < pCube->pVar->nCubes &&\
00368 (((unsigned)(pPair = pCube->pVar->ppPairs[pCube->iCube][i])) >= 0);\
00369 i++ )\
00370 if ( pPair )
00371
00372
00373 #define Fxu_HeapDoubleForEachItem( Heap, Div )\
00374 for ( Heap->i = 1;\
00375 Heap->i <= Heap->nItems && (Div = Heap->pTree[Heap->i]);\
00376 Heap->i++ )
00377 #define Fxu_HeapSingleForEachItem( Heap, Single )\
00378 for ( Heap->i = 1;\
00379 Heap->i <= Heap->nItems && (Single = Heap->pTree[Heap->i]);\
00380 Heap->i++ )
00381
00382
00383 #define Fxu_MatrixRingCubesStart( Matrix ) (((Matrix)->ppTailCubes = &((Matrix)->pOrderCubes)), ((Matrix)->pOrderCubes = NULL))
00384 #define Fxu_MatrixRingVarsStart( Matrix ) (((Matrix)->ppTailVars = &((Matrix)->pOrderVars)), ((Matrix)->pOrderVars = NULL))
00385
00386 #define Fxu_MatrixRingCubesStop( Matrix )
00387 #define Fxu_MatrixRingVarsStop( Matrix )
00388
00389 #define Fxu_MatrixRingCubesReset( Matrix ) (((Matrix)->pOrderCubes = NULL), ((Matrix)->ppTailCubes = NULL))
00390 #define Fxu_MatrixRingVarsReset( Matrix ) (((Matrix)->pOrderVars = NULL), ((Matrix)->ppTailVars = NULL))
00391
00392 #define Fxu_MatrixRingCubesAdd( Matrix, Cube) ((*((Matrix)->ppTailCubes) = Cube), ((Matrix)->ppTailCubes = &(Cube)->pOrder), ((Cube)->pOrder = (Fxu_Cube *)1))
00393 #define Fxu_MatrixRingVarsAdd( Matrix, Var ) ((*((Matrix)->ppTailVars ) = Var ), ((Matrix)->ppTailVars = &(Var)->pOrder ), ((Var)->pOrder = (Fxu_Var *)1))
00394
00395 #define Fxu_MatrixForEachCubeInRing( Matrix, Cube )\
00396 if ( (Matrix)->pOrderCubes )\
00397 for ( Cube = (Matrix)->pOrderCubes;\
00398 Cube != (Fxu_Cube *)1;\
00399 Cube = Cube->pOrder )
00400 #define Fxu_MatrixForEachCubeInRingSafe( Matrix, Cube, Cube2 )\
00401 if ( (Matrix)->pOrderCubes )\
00402 for ( Cube = (Matrix)->pOrderCubes, Cube2 = ((Cube != (Fxu_Cube *)1)? Cube->pOrder: (Fxu_Cube *)1);\
00403 Cube != (Fxu_Cube *)1;\
00404 Cube = Cube2, Cube2 = ((Cube != (Fxu_Cube *)1)? Cube->pOrder: (Fxu_Cube *)1) )
00405 #define Fxu_MatrixForEachVarInRing( Matrix, Var )\
00406 if ( (Matrix)->pOrderVars )\
00407 for ( Var = (Matrix)->pOrderVars;\
00408 Var != (Fxu_Var *)1;\
00409 Var = Var->pOrder )
00410 #define Fxu_MatrixForEachVarInRingSafe( Matrix, Var, Var2 )\
00411 if ( (Matrix)->pOrderVars )\
00412 for ( Var = (Matrix)->pOrderVars, Var2 = ((Var != (Fxu_Var *)1)? Var->pOrder: (Fxu_Var *)1);\
00413 Var != (Fxu_Var *)1;\
00414 Var = Var2, Var2 = ((Var != (Fxu_Var *)1)? Var->pOrder: (Fxu_Var *)1) )
00415
00416 extern void Fxu_MatrixRingCubesUnmark( Fxu_Matrix * p );
00417 extern void Fxu_MatrixRingVarsUnmark( Fxu_Matrix * p );
00418
00419
00420
00421
00422
00423 #ifdef USE_SYSTEM_MEMORY_MANAGEMENT
00424 #define MEM_ALLOC_FXU( Manager, Type, Size ) ((Type *)malloc( (Size) * sizeof(Type) ))
00425 #define MEM_FREE_FXU( Manager, Type, Size, Pointer ) if ( Pointer ) { free(Pointer); Pointer = NULL; }
00426 #else
00427 #define MEM_ALLOC_FXU( Manager, Type, Size )\
00428 ((Type *)Fxu_MemFetch( Manager, (Size) * sizeof(Type) ))
00429 #define MEM_FREE_FXU( Manager, Type, Size, Pointer )\
00430 if ( Pointer ) { Fxu_MemRecycle( Manager, (char *)(Pointer), (Size) * sizeof(Type) ); Pointer = NULL; }
00431 #endif
00432
00436
00437
00438 extern char * Fxu_MemFetch( Fxu_Matrix * p, int nBytes );
00439 extern void Fxu_MemRecycle( Fxu_Matrix * p, char * pItem, int nBytes );
00440
00441
00442
00443 extern void Fxu_MatrixPrint( FILE * pFile, Fxu_Matrix * p );
00444 extern void Fxu_MatrixPrintDivisorProfile( FILE * pFile, Fxu_Matrix * p );
00445
00446 extern int Fxu_Select( Fxu_Matrix * p, Fxu_Single ** ppSingle, Fxu_Double ** ppDouble );
00447 extern int Fxu_SelectSCD( Fxu_Matrix * p, int Weight, Fxu_Var ** ppVar1, Fxu_Var ** ppVar2 );
00448
00449 extern void Fxu_Update( Fxu_Matrix * p, Fxu_Single * pSingle, Fxu_Double * pDouble );
00450 extern void Fxu_UpdateDouble( Fxu_Matrix * p );
00451 extern void Fxu_UpdateSingle( Fxu_Matrix * p );
00452
00453 extern void Fxu_PairCanonicize( Fxu_Cube ** ppCube1, Fxu_Cube ** ppCube2 );
00454 extern unsigned Fxu_PairHashKeyArray( Fxu_Matrix * p, int piVarsC1[], int piVarsC2[], int nVarsC1, int nVarsC2 );
00455 extern unsigned Fxu_PairHashKey( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2, int * pnBase, int * pnLits1, int * pnLits2 );
00456 extern unsigned Fxu_PairHashKeyMv( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2, int * pnBase, int * pnLits1, int * pnLits2 );
00457 extern int Fxu_PairCompare( Fxu_Pair * pPair1, Fxu_Pair * pPair2 );
00458 extern void Fxu_PairAllocStorage( Fxu_Var * pVar, int nCubes );
00459 extern void Fxu_PairFreeStorage( Fxu_Var * pVar );
00460 extern void Fxu_PairClearStorage( Fxu_Cube * pCube );
00461 extern Fxu_Pair * Fxu_PairAlloc( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2 );
00462 extern void Fxu_PairAdd( Fxu_Pair * pPair );
00463
00464 extern void Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax );
00465 extern void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar );
00466 extern int Fxu_SingleCountCoincidence( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVar2 );
00467
00468
00469 extern Fxu_Matrix * Fxu_MatrixAllocate();
00470 extern void Fxu_MatrixDelete( Fxu_Matrix * p );
00471
00472 extern void Fxu_MatrixAddDivisor( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2 );
00473 extern void Fxu_MatrixDelDivisor( Fxu_Matrix * p, Fxu_Double * pDiv );
00474
00475 extern void Fxu_MatrixAddSingle( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVar2, int Weight );
00476
00477 extern Fxu_Var * Fxu_MatrixAddVar( Fxu_Matrix * p );
00478
00479 extern Fxu_Cube * Fxu_MatrixAddCube( Fxu_Matrix * p, Fxu_Var * pVar, int iCube );
00480
00481 extern void Fxu_MatrixAddLiteral( Fxu_Matrix * p, Fxu_Cube * pCube, Fxu_Var * pVar );
00482 extern void Fxu_MatrixDelLiteral( Fxu_Matrix * p, Fxu_Lit * pLit );
00483
00484
00485 extern void Fxu_ListMatrixAddVariable( Fxu_Matrix * p, Fxu_Var * pVar );
00486 extern void Fxu_ListMatrixDelVariable( Fxu_Matrix * p, Fxu_Var * pVar );
00487
00488 extern void Fxu_ListMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube );
00489 extern void Fxu_ListMatrixDelCube( Fxu_Matrix * p, Fxu_Cube * pCube );
00490
00491 extern void Fxu_ListMatrixAddSingle( Fxu_Matrix * p, Fxu_Single * pSingle );
00492 extern void Fxu_ListMatrixDelSingle( Fxu_Matrix * p, Fxu_Single * pSingle );
00493
00494 extern void Fxu_ListTableAddDivisor( Fxu_Matrix * p, Fxu_Double * pDiv );
00495 extern void Fxu_ListTableDelDivisor( Fxu_Matrix * p, Fxu_Double * pDiv );
00496
00497 extern void Fxu_ListCubeAddLiteral( Fxu_Cube * pCube, Fxu_Lit * pLit );
00498 extern void Fxu_ListCubeDelLiteral( Fxu_Cube * pCube, Fxu_Lit * pLit );
00499
00500 extern void Fxu_ListVarAddLiteral( Fxu_Var * pVar, Fxu_Lit * pLit );
00501 extern void Fxu_ListVarDelLiteral( Fxu_Var * pVar, Fxu_Lit * pLit );
00502
00503 extern void Fxu_ListDoubleAddPairLast( Fxu_Double * pDiv, Fxu_Pair * pLink );
00504 extern void Fxu_ListDoubleAddPairFirst( Fxu_Double * pDiv, Fxu_Pair * pLink );
00505 extern void Fxu_ListDoubleAddPairMiddle( Fxu_Double * pDiv, Fxu_Pair * pSpot, Fxu_Pair * pLink );
00506 extern void Fxu_ListDoubleDelPair( Fxu_Double * pDiv, Fxu_Pair * pPair );
00507
00508 extern Fxu_HeapDouble * Fxu_HeapDoubleStart();
00509 extern void Fxu_HeapDoubleStop( Fxu_HeapDouble * p );
00510 extern void Fxu_HeapDoublePrint( FILE * pFile, Fxu_HeapDouble * p );
00511 extern void Fxu_HeapDoubleCheck( Fxu_HeapDouble * p );
00512 extern void Fxu_HeapDoubleCheckOne( Fxu_HeapDouble * p, Fxu_Double * pDiv );
00513
00514 extern void Fxu_HeapDoubleInsert( Fxu_HeapDouble * p, Fxu_Double * pDiv );
00515 extern void Fxu_HeapDoubleUpdate( Fxu_HeapDouble * p, Fxu_Double * pDiv );
00516 extern void Fxu_HeapDoubleDelete( Fxu_HeapDouble * p, Fxu_Double * pDiv );
00517 extern int Fxu_HeapDoubleReadMaxWeight( Fxu_HeapDouble * p );
00518 extern Fxu_Double * Fxu_HeapDoubleReadMax( Fxu_HeapDouble * p );
00519 extern Fxu_Double * Fxu_HeapDoubleGetMax( Fxu_HeapDouble * p );
00520
00521 extern Fxu_HeapSingle * Fxu_HeapSingleStart();
00522 extern void Fxu_HeapSingleStop( Fxu_HeapSingle * p );
00523 extern void Fxu_HeapSinglePrint( FILE * pFile, Fxu_HeapSingle * p );
00524 extern void Fxu_HeapSingleCheck( Fxu_HeapSingle * p );
00525 extern void Fxu_HeapSingleCheckOne( Fxu_HeapSingle * p, Fxu_Single * pSingle );
00526
00527 extern void Fxu_HeapSingleInsert( Fxu_HeapSingle * p, Fxu_Single * pSingle );
00528 extern void Fxu_HeapSingleUpdate( Fxu_HeapSingle * p, Fxu_Single * pSingle );
00529 extern void Fxu_HeapSingleDelete( Fxu_HeapSingle * p, Fxu_Single * pSingle );
00530 extern int Fxu_HeapSingleReadMaxWeight( Fxu_HeapSingle * p );
00531 extern Fxu_Single * Fxu_HeapSingleReadMax( Fxu_HeapSingle * p );
00532 extern Fxu_Single * Fxu_HeapSingleGetMax( Fxu_HeapSingle * p );
00533
00534 #endif
00535
00539