src/opt/fxu/fxuInt.h File Reference

#include "extra.h"
#include "vec.h"
Include dependency graph for fxuInt.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Data Structures

struct  FxuListCube
struct  FxuListVar
struct  FxuListLit
struct  FxuListPair
struct  FxuListDouble
struct  FxuListSingle
struct  FxuHeapDouble
struct  FxuHeapSingle
struct  FxuMatrix
struct  FxuCube
struct  FxuVar
struct  FxuLit
struct  FxuPair
struct  FxuDouble
struct  FxuSingle

Defines

#define Fxu_Min(a, b)   ( ((a)<(b))? (a):(b) )
#define Fxu_Max(a, b)   ( ((a)>(b))? (a):(b) )
#define Fxu_PairMinCube(pPair)   (((pPair)->iCube1 < (pPair)->iCube2)? (pPair)->pCube1: (pPair)->pCube2)
#define Fxu_PairMaxCube(pPair)   (((pPair)->iCube1 > (pPair)->iCube2)? (pPair)->pCube1: (pPair)->pCube2)
#define Fxu_PairMinCubeInt(pPair)   (((pPair)->iCube1 < (pPair)->iCube2)? (pPair)->iCube1: (pPair)->iCube2)
#define Fxu_PairMaxCubeInt(pPair)   (((pPair)->iCube1 > (pPair)->iCube2)? (pPair)->iCube1: (pPair)->iCube2)
#define Fxu_MatrixForEachCube(Matrix, Cube)
#define Fxu_MatrixForEachCubeSafe(Matrix, Cube, Cube2)
#define Fxu_MatrixForEachVariable(Matrix, Var)
#define Fxu_MatrixForEachVariableSafe(Matrix, Var, Var2)
#define Fxu_MatrixForEachSingle(Matrix, Single)
#define Fxu_MatrixForEachSingleSafe(Matrix, Single, Single2)
#define Fxu_TableForEachDouble(Matrix, Key, Div)
#define Fxu_TableForEachDoubleSafe(Matrix, Key, Div, Div2)
#define Fxu_MatrixForEachDouble(Matrix, Div, Index)
#define Fxu_MatrixForEachDoubleSafe(Matrix, Div, Div2, Index)
#define Fxu_CubeForEachLiteral(Cube, Lit)
#define Fxu_CubeForEachLiteralSafe(Cube, Lit, Lit2)
#define Fxu_VarForEachLiteral(Var, Lit)
#define Fxu_CubeForEachDivisor(Cube, Div)
#define Fxu_DoubleForEachPair(Div, Pair)
#define Fxu_DoubleForEachPairSafe(Div, Pair, Pair2)
#define Fxu_CubeForEachPair(pCube, pPair, i)
#define Fxu_HeapDoubleForEachItem(Heap, Div)
#define Fxu_HeapSingleForEachItem(Heap, Single)
#define Fxu_MatrixRingCubesStart(Matrix)   (((Matrix)->ppTailCubes = &((Matrix)->pOrderCubes)), ((Matrix)->pOrderCubes = NULL))
#define Fxu_MatrixRingVarsStart(Matrix)   (((Matrix)->ppTailVars = &((Matrix)->pOrderVars)), ((Matrix)->pOrderVars = NULL))
#define Fxu_MatrixRingCubesStop(Matrix)
#define Fxu_MatrixRingVarsStop(Matrix)
#define Fxu_MatrixRingCubesReset(Matrix)   (((Matrix)->pOrderCubes = NULL), ((Matrix)->ppTailCubes = NULL))
#define Fxu_MatrixRingVarsReset(Matrix)   (((Matrix)->pOrderVars = NULL), ((Matrix)->ppTailVars = NULL))
#define Fxu_MatrixRingCubesAdd(Matrix, Cube)   ((*((Matrix)->ppTailCubes) = Cube), ((Matrix)->ppTailCubes = &(Cube)->pOrder), ((Cube)->pOrder = (Fxu_Cube *)1))
#define Fxu_MatrixRingVarsAdd(Matrix, Var)   ((*((Matrix)->ppTailVars ) = Var ), ((Matrix)->ppTailVars = &(Var)->pOrder ), ((Var)->pOrder = (Fxu_Var *)1))
#define Fxu_MatrixForEachCubeInRing(Matrix, Cube)
#define Fxu_MatrixForEachCubeInRingSafe(Matrix, Cube, Cube2)
#define Fxu_MatrixForEachVarInRing(Matrix, Var)
#define Fxu_MatrixForEachVarInRingSafe(Matrix, Var, Var2)
#define MEM_ALLOC_FXU(Manager, Type, Size)   ((Type *)Fxu_MemFetch( Manager, (Size) * sizeof(Type) ))
#define MEM_FREE_FXU(Manager, Type, Size, Pointer)   if ( Pointer ) { Fxu_MemRecycle( Manager, (char *)(Pointer), (Size) * sizeof(Type) ); Pointer = NULL; }

Typedefs

typedef struct FxuMatrix Fxu_Matrix
typedef struct FxuCube Fxu_Cube
typedef struct FxuVar Fxu_Var
typedef struct FxuLit Fxu_Lit
typedef struct FxuPair Fxu_Pair
typedef struct FxuDouble Fxu_Double
typedef struct FxuSingle Fxu_Single
typedef struct FxuListCube Fxu_ListCube
typedef struct FxuListVar Fxu_ListVar
typedef struct FxuListLit Fxu_ListLit
typedef struct FxuListPair Fxu_ListPair
typedef struct FxuListDouble Fxu_ListDouble
typedef struct FxuListSingle Fxu_ListSingle
typedef struct FxuHeapDouble Fxu_HeapDouble
typedef struct FxuHeapSingle Fxu_HeapSingle

Functions

void Fxu_MatrixRingCubesUnmark (Fxu_Matrix *p)
void Fxu_MatrixRingVarsUnmark (Fxu_Matrix *p)
char * Fxu_MemFetch (Fxu_Matrix *p, int nBytes)
void Fxu_MemRecycle (Fxu_Matrix *p, char *pItem, int nBytes)
void Fxu_MatrixPrint (FILE *pFile, Fxu_Matrix *p)
void Fxu_MatrixPrintDivisorProfile (FILE *pFile, Fxu_Matrix *p)
int Fxu_Select (Fxu_Matrix *p, Fxu_Single **ppSingle, Fxu_Double **ppDouble)
int Fxu_SelectSCD (Fxu_Matrix *p, int Weight, Fxu_Var **ppVar1, Fxu_Var **ppVar2)
void Fxu_Update (Fxu_Matrix *p, Fxu_Single *pSingle, Fxu_Double *pDouble)
void Fxu_UpdateDouble (Fxu_Matrix *p)
void Fxu_UpdateSingle (Fxu_Matrix *p)
void Fxu_PairCanonicize (Fxu_Cube **ppCube1, Fxu_Cube **ppCube2)
unsigned Fxu_PairHashKeyArray (Fxu_Matrix *p, int piVarsC1[], int piVarsC2[], int nVarsC1, int nVarsC2)
unsigned Fxu_PairHashKey (Fxu_Matrix *p, Fxu_Cube *pCube1, Fxu_Cube *pCube2, int *pnBase, int *pnLits1, int *pnLits2)
unsigned Fxu_PairHashKeyMv (Fxu_Matrix *p, Fxu_Cube *pCube1, Fxu_Cube *pCube2, int *pnBase, int *pnLits1, int *pnLits2)
int Fxu_PairCompare (Fxu_Pair *pPair1, Fxu_Pair *pPair2)
void Fxu_PairAllocStorage (Fxu_Var *pVar, int nCubes)
void Fxu_PairFreeStorage (Fxu_Var *pVar)
void Fxu_PairClearStorage (Fxu_Cube *pCube)
Fxu_Pair * Fxu_PairAlloc (Fxu_Matrix *p, Fxu_Cube *pCube1, Fxu_Cube *pCube2)
void Fxu_PairAdd (Fxu_Pair *pPair)
void Fxu_MatrixComputeSingles (Fxu_Matrix *p, int fUse0, int nSingleMax)
void Fxu_MatrixComputeSinglesOne (Fxu_Matrix *p, Fxu_Var *pVar)
int Fxu_SingleCountCoincidence (Fxu_Matrix *p, Fxu_Var *pVar1, Fxu_Var *pVar2)
Fxu_Matrix * Fxu_MatrixAllocate ()
void Fxu_MatrixDelete (Fxu_Matrix *p)
void Fxu_MatrixAddDivisor (Fxu_Matrix *p, Fxu_Cube *pCube1, Fxu_Cube *pCube2)
void Fxu_MatrixDelDivisor (Fxu_Matrix *p, Fxu_Double *pDiv)
void Fxu_MatrixAddSingle (Fxu_Matrix *p, Fxu_Var *pVar1, Fxu_Var *pVar2, int Weight)
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_MatrixDelLiteral (Fxu_Matrix *p, Fxu_Lit *pLit)
void Fxu_ListMatrixAddVariable (Fxu_Matrix *p, Fxu_Var *pVar)
void Fxu_ListMatrixDelVariable (Fxu_Matrix *p, Fxu_Var *pVar)
void Fxu_ListMatrixAddCube (Fxu_Matrix *p, Fxu_Cube *pCube)
void Fxu_ListMatrixDelCube (Fxu_Matrix *p, Fxu_Cube *pCube)
void Fxu_ListMatrixAddSingle (Fxu_Matrix *p, Fxu_Single *pSingle)
void Fxu_ListMatrixDelSingle (Fxu_Matrix *p, Fxu_Single *pSingle)
void Fxu_ListTableAddDivisor (Fxu_Matrix *p, Fxu_Double *pDiv)
void Fxu_ListTableDelDivisor (Fxu_Matrix *p, Fxu_Double *pDiv)
void Fxu_ListCubeAddLiteral (Fxu_Cube *pCube, Fxu_Lit *pLit)
void Fxu_ListCubeDelLiteral (Fxu_Cube *pCube, Fxu_Lit *pLit)
void Fxu_ListVarAddLiteral (Fxu_Var *pVar, Fxu_Lit *pLit)
void Fxu_ListVarDelLiteral (Fxu_Var *pVar, Fxu_Lit *pLit)
void Fxu_ListDoubleAddPairLast (Fxu_Double *pDiv, Fxu_Pair *pLink)
void Fxu_ListDoubleAddPairFirst (Fxu_Double *pDiv, Fxu_Pair *pLink)
void Fxu_ListDoubleAddPairMiddle (Fxu_Double *pDiv, Fxu_Pair *pSpot, Fxu_Pair *pLink)
void Fxu_ListDoubleDelPair (Fxu_Double *pDiv, Fxu_Pair *pPair)
Fxu_HeapDouble * Fxu_HeapDoubleStart ()
void Fxu_HeapDoubleStop (Fxu_HeapDouble *p)
void Fxu_HeapDoublePrint (FILE *pFile, Fxu_HeapDouble *p)
void Fxu_HeapDoubleCheck (Fxu_HeapDouble *p)
void Fxu_HeapDoubleCheckOne (Fxu_HeapDouble *p, Fxu_Double *pDiv)
void Fxu_HeapDoubleInsert (Fxu_HeapDouble *p, Fxu_Double *pDiv)
void Fxu_HeapDoubleUpdate (Fxu_HeapDouble *p, Fxu_Double *pDiv)
void Fxu_HeapDoubleDelete (Fxu_HeapDouble *p, Fxu_Double *pDiv)
int Fxu_HeapDoubleReadMaxWeight (Fxu_HeapDouble *p)
Fxu_Double * Fxu_HeapDoubleReadMax (Fxu_HeapDouble *p)
Fxu_Double * Fxu_HeapDoubleGetMax (Fxu_HeapDouble *p)
Fxu_HeapSingle * Fxu_HeapSingleStart ()
void Fxu_HeapSingleStop (Fxu_HeapSingle *p)
void Fxu_HeapSinglePrint (FILE *pFile, Fxu_HeapSingle *p)
void Fxu_HeapSingleCheck (Fxu_HeapSingle *p)
void Fxu_HeapSingleCheckOne (Fxu_HeapSingle *p, Fxu_Single *pSingle)
void Fxu_HeapSingleInsert (Fxu_HeapSingle *p, Fxu_Single *pSingle)
void Fxu_HeapSingleUpdate (Fxu_HeapSingle *p, Fxu_Single *pSingle)
void Fxu_HeapSingleDelete (Fxu_HeapSingle *p, Fxu_Single *pSingle)
int Fxu_HeapSingleReadMaxWeight (Fxu_HeapSingle *p)
Fxu_Single * Fxu_HeapSingleReadMax (Fxu_HeapSingle *p)
Fxu_Single * Fxu_HeapSingleGetMax (Fxu_HeapSingle *p)

Define Documentation

#define Fxu_CubeForEachDivisor ( Cube,
Div   ) 
Value:
for ( Div = (Cube)->lDivs.pHead;\
          Div;\
                  Div = Div->pCNext )

Definition at line 349 of file fxuInt.h.

#define Fxu_CubeForEachLiteral ( Cube,
Lit   ) 
Value:
for ( Lit = (Cube)->lLits.pHead;\
          Lit;\
                  Lit = Lit->pHNext )

Definition at line 335 of file fxuInt.h.

#define Fxu_CubeForEachLiteralSafe ( Cube,
Lit,
Lit2   ) 
Value:
for ( Lit = (Cube)->lLits.pHead, Lit2 = (Lit? Lit->pHNext: NULL);\
          Lit;\
                  Lit = Lit2, Lit2 = (Lit? Lit->pHNext: NULL) )

Definition at line 339 of file fxuInt.h.

#define Fxu_CubeForEachPair ( pCube,
pPair,
i   ) 
Value:
for ( i = 0;\
        i < pCube->pVar->nCubes &&\
        (((unsigned)(pPair = pCube->pVar->ppPairs[pCube->iCube][i])) >= 0);\
                i++ )\
            if ( pPair )

Definition at line 365 of file fxuInt.h.

#define Fxu_DoubleForEachPair ( Div,
Pair   ) 
Value:
for ( Pair = (Div)->lPairs.pHead;\
          Pair;\
                  Pair = Pair->pDNext )

Definition at line 354 of file fxuInt.h.

#define Fxu_DoubleForEachPairSafe ( Div,
Pair,
Pair2   ) 
Value:
for ( Pair = (Div)->lPairs.pHead, Pair2 = (Pair? Pair->pDNext: NULL);\
          Pair;\
                  Pair = Pair2, Pair2 = (Pair? Pair->pDNext: NULL) )

Definition at line 358 of file fxuInt.h.

#define Fxu_HeapDoubleForEachItem ( Heap,
Div   ) 
Value:
for ( Heap->i = 1;\
                  Heap->i <= Heap->nItems && (Div = Heap->pTree[Heap->i]);\
                  Heap->i++ )

Definition at line 373 of file fxuInt.h.

#define Fxu_HeapSingleForEachItem ( Heap,
Single   ) 
Value:
for ( Heap->i = 1;\
                  Heap->i <= Heap->nItems && (Single = Heap->pTree[Heap->i]);\
                  Heap->i++ )

Definition at line 377 of file fxuInt.h.

#define Fxu_MatrixForEachCube ( Matrix,
Cube   ) 
Value:
for ( Cube = (Matrix)->lCubes.pHead;\
          Cube;\
                  Cube = Cube->pNext )

Definition at line 291 of file fxuInt.h.

#define Fxu_MatrixForEachCubeInRing ( Matrix,
Cube   ) 
Value:
if ( (Matrix)->pOrderCubes )\
        for ( Cube = (Matrix)->pOrderCubes;\
          Cube != (Fxu_Cube *)1;\
                  Cube = Cube->pOrder )

Definition at line 395 of file fxuInt.h.

#define Fxu_MatrixForEachCubeInRingSafe ( Matrix,
Cube,
Cube2   ) 
Value:
if ( (Matrix)->pOrderCubes )\
        for ( Cube = (Matrix)->pOrderCubes, Cube2 = ((Cube != (Fxu_Cube *)1)? Cube->pOrder: (Fxu_Cube *)1);\
          Cube != (Fxu_Cube *)1;\
                  Cube = Cube2, Cube2 = ((Cube != (Fxu_Cube *)1)? Cube->pOrder: (Fxu_Cube *)1) )

Definition at line 400 of file fxuInt.h.

#define Fxu_MatrixForEachCubeSafe ( Matrix,
Cube,
Cube2   ) 
Value:
for ( Cube = (Matrix)->lCubes.pHead, Cube2 = (Cube? Cube->pNext: NULL);\
          Cube;\
                  Cube = Cube2, Cube2 = (Cube? Cube->pNext: NULL) )

Definition at line 295 of file fxuInt.h.

#define Fxu_MatrixForEachDouble ( Matrix,
Div,
Index   ) 
Value:
for ( Index = 0; Index < (Matrix)->nTableSize; Index++ )\
        Fxu_TableForEachDouble( Matrix, Index, Div )

Definition at line 327 of file fxuInt.h.

#define Fxu_MatrixForEachDoubleSafe ( Matrix,
Div,
Div2,
Index   ) 
Value:
for ( Index = 0; Index < (Matrix)->nTableSize; Index++ )\
        Fxu_TableForEachDoubleSafe( Matrix, Index, Div, Div2 )

Definition at line 330 of file fxuInt.h.

#define Fxu_MatrixForEachSingle ( Matrix,
Single   ) 
Value:
for ( Single = (Matrix)->lSingles.pHead;\
          Single;\
                  Single = Single->pNext )

Definition at line 309 of file fxuInt.h.

#define Fxu_MatrixForEachSingleSafe ( Matrix,
Single,
Single2   ) 
Value:
for ( Single = (Matrix)->lSingles.pHead, Single2 = (Single? Single->pNext: NULL);\
          Single;\
                  Single = Single2, Single2 = (Single? Single->pNext: NULL) )

Definition at line 313 of file fxuInt.h.

#define Fxu_MatrixForEachVariable ( Matrix,
Var   ) 
Value:
for ( Var = (Matrix)->lVars.pHead;\
          Var;\
                  Var = Var->pNext )

Definition at line 300 of file fxuInt.h.

#define Fxu_MatrixForEachVariableSafe ( Matrix,
Var,
Var2   ) 
Value:
for ( Var = (Matrix)->lVars.pHead, Var2 = (Var? Var->pNext: NULL);\
          Var;\
                  Var = Var2, Var2 = (Var? Var->pNext: NULL) )

Definition at line 304 of file fxuInt.h.

#define Fxu_MatrixForEachVarInRing ( Matrix,
Var   ) 
Value:
if ( (Matrix)->pOrderVars )\
        for ( Var = (Matrix)->pOrderVars;\
          Var != (Fxu_Var *)1;\
                  Var = Var->pOrder )

Definition at line 405 of file fxuInt.h.

#define Fxu_MatrixForEachVarInRingSafe ( Matrix,
Var,
Var2   ) 
Value:
if ( (Matrix)->pOrderVars )\
        for ( Var = (Matrix)->pOrderVars, Var2 = ((Var != (Fxu_Var *)1)? Var->pOrder: (Fxu_Var *)1);\
          Var != (Fxu_Var *)1;\
                  Var = Var2, Var2 = ((Var != (Fxu_Var *)1)? Var->pOrder: (Fxu_Var *)1) )

Definition at line 410 of file fxuInt.h.

#define Fxu_MatrixRingCubesAdd ( Matrix,
Cube   )     ((*((Matrix)->ppTailCubes) = Cube), ((Matrix)->ppTailCubes = &(Cube)->pOrder), ((Cube)->pOrder = (Fxu_Cube *)1))

Definition at line 392 of file fxuInt.h.

#define Fxu_MatrixRingCubesReset ( Matrix   )     (((Matrix)->pOrderCubes = NULL), ((Matrix)->ppTailCubes = NULL))

Definition at line 389 of file fxuInt.h.

#define Fxu_MatrixRingCubesStart ( Matrix   )     (((Matrix)->ppTailCubes = &((Matrix)->pOrderCubes)), ((Matrix)->pOrderCubes = NULL))

Definition at line 383 of file fxuInt.h.

#define Fxu_MatrixRingCubesStop ( Matrix   ) 

Definition at line 386 of file fxuInt.h.

#define Fxu_MatrixRingVarsAdd ( Matrix,
Var   )     ((*((Matrix)->ppTailVars ) = Var ), ((Matrix)->ppTailVars = &(Var)->pOrder ), ((Var)->pOrder = (Fxu_Var *)1))

Definition at line 393 of file fxuInt.h.

#define Fxu_MatrixRingVarsReset ( Matrix   )     (((Matrix)->pOrderVars = NULL), ((Matrix)->ppTailVars = NULL))

Definition at line 390 of file fxuInt.h.

#define Fxu_MatrixRingVarsStart ( Matrix   )     (((Matrix)->ppTailVars = &((Matrix)->pOrderVars)), ((Matrix)->pOrderVars = NULL))

Definition at line 384 of file fxuInt.h.

#define Fxu_MatrixRingVarsStop ( Matrix   ) 

Definition at line 387 of file fxuInt.h.

#define Fxu_Max ( a,
b   )     ( ((a)>(b))? (a):(b) )

Definition at line 281 of file fxuInt.h.

#define Fxu_Min ( a,
b   )     ( ((a)<(b))? (a):(b) )

MACRO DEFINITIONS ///

Definition at line 280 of file fxuInt.h.

#define Fxu_PairMaxCube ( pPair   )     (((pPair)->iCube1 > (pPair)->iCube2)? (pPair)->pCube1: (pPair)->pCube2)

Definition at line 285 of file fxuInt.h.

#define Fxu_PairMaxCubeInt ( pPair   )     (((pPair)->iCube1 > (pPair)->iCube2)? (pPair)->iCube1: (pPair)->iCube2)

Definition at line 287 of file fxuInt.h.

#define Fxu_PairMinCube ( pPair   )     (((pPair)->iCube1 < (pPair)->iCube2)? (pPair)->pCube1: (pPair)->pCube2)

Definition at line 284 of file fxuInt.h.

#define Fxu_PairMinCubeInt ( pPair   )     (((pPair)->iCube1 < (pPair)->iCube2)? (pPair)->iCube1: (pPair)->iCube2)

Definition at line 286 of file fxuInt.h.

#define Fxu_TableForEachDouble ( Matrix,
Key,
Div   ) 
Value:
for ( Div = (Matrix)->pTable[Key].pHead;\
          Div;\
                  Div = Div->pNext )

Definition at line 318 of file fxuInt.h.

#define Fxu_TableForEachDoubleSafe ( Matrix,
Key,
Div,
Div2   ) 
Value:
for ( Div = (Matrix)->pTable[Key].pHead, Div2 = (Div? Div->pNext: NULL);\
          Div;\
                  Div = Div2, Div2 = (Div? Div->pNext: NULL) )

Definition at line 322 of file fxuInt.h.

#define Fxu_VarForEachLiteral ( Var,
Lit   ) 
Value:
for ( Lit = (Var)->lLits.pHead;\
          Lit;\
                  Lit = Lit->pVNext )

Definition at line 344 of file fxuInt.h.

#define MEM_ALLOC_FXU ( Manager,
Type,
Size   )     ((Type *)Fxu_MemFetch( Manager, (Size) * sizeof(Type) ))

Definition at line 427 of file fxuInt.h.

#define MEM_FREE_FXU ( Manager,
Type,
Size,
Pointer   )     if ( Pointer ) { Fxu_MemRecycle( Manager, (char *)(Pointer), (Size) * sizeof(Type) ); Pointer = NULL; }

Definition at line 429 of file fxuInt.h.

Typedef Documentation

typedef struct FxuCube Fxu_Cube

Definition at line 63 of file fxuInt.h.

typedef struct FxuDouble Fxu_Double

Definition at line 69 of file fxuInt.h.

typedef struct FxuHeapDouble Fxu_HeapDouble

Definition at line 81 of file fxuInt.h.

typedef struct FxuHeapSingle Fxu_HeapSingle

Definition at line 82 of file fxuInt.h.

typedef struct FxuListCube Fxu_ListCube

Definition at line 73 of file fxuInt.h.

typedef struct FxuListDouble Fxu_ListDouble

Definition at line 77 of file fxuInt.h.

typedef struct FxuListLit Fxu_ListLit

Definition at line 75 of file fxuInt.h.

typedef struct FxuListPair Fxu_ListPair

Definition at line 76 of file fxuInt.h.

typedef struct FxuListSingle Fxu_ListSingle

Definition at line 78 of file fxuInt.h.

typedef struct FxuListVar Fxu_ListVar

Definition at line 74 of file fxuInt.h.

typedef struct FxuLit Fxu_Lit

Definition at line 65 of file fxuInt.h.

typedef struct FxuMatrix Fxu_Matrix

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

FileName [fxuInt.h]

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

Synopsis [Internal declarations of fast extract for unate covers.]

Author [MVSIS Group]

Affiliation [UC Berkeley]

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

Revision [

Id
fxuInt.h,v 1.3 2003/04/10 05:42:44 donald Exp

] INCLUDES /// PARAMETERS /// STRUCTURE DEFINITIONS ///

Definition at line 60 of file fxuInt.h.

typedef struct FxuPair Fxu_Pair

Definition at line 68 of file fxuInt.h.

typedef struct FxuSingle Fxu_Single

Definition at line 70 of file fxuInt.h.

typedef struct FxuVar Fxu_Var

Definition at line 64 of file fxuInt.h.

Function Documentation

void Fxu_HeapDoubleCheck ( Fxu_HeapDouble *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 149 of file fxuHeapD.c.

00150 {
00151         Fxu_Double * pDiv;
00152         Fxu_HeapDoubleForEachItem( p, pDiv )
00153         {
00154                 assert( pDiv->HNum == p->i );
00155         Fxu_HeapDoubleCheckOne( p, pDiv );
00156         }
00157 }

void Fxu_HeapDoubleCheckOne ( Fxu_HeapDouble *  p,
Fxu_Double *  pDiv 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 170 of file fxuHeapD.c.

00171 {
00172     int Weight1, Weight2;
00173         if ( FXU_HEAP_DOUBLE_CHILD1_EXISTS(p,pDiv) )
00174         {
00175         Weight1 = FXU_HEAP_DOUBLE_WEIGHT(pDiv);
00176         Weight2 = FXU_HEAP_DOUBLE_WEIGHT( FXU_HEAP_DOUBLE_CHILD1(p,pDiv) );
00177         assert( Weight1 >= Weight2 );
00178         }
00179         if ( FXU_HEAP_DOUBLE_CHILD2_EXISTS(p,pDiv) )
00180         {
00181         Weight1 = FXU_HEAP_DOUBLE_WEIGHT(pDiv);
00182         Weight2 = FXU_HEAP_DOUBLE_WEIGHT( FXU_HEAP_DOUBLE_CHILD2(p,pDiv) );
00183         assert( Weight1 >= Weight2 );
00184         }
00185 }

void Fxu_HeapDoubleDelete ( Fxu_HeapDouble *  p,
Fxu_Double *  pDiv 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 247 of file fxuHeapD.c.

00248 {
00249         FXU_HEAP_DOUBLE_ASSERT(p,pDiv);
00250         // put the last entry to the deleted place
00251         // decrement the number of entries
00252         p->pTree[pDiv->HNum] = p->pTree[p->nItems--];
00253         p->pTree[pDiv->HNum]->HNum = pDiv->HNum;
00254         // move the top entry down if necessary
00255         Fxu_HeapDoubleUpdate( p, p->pTree[pDiv->HNum] );
00256     pDiv->HNum = 0;
00257 }

Fxu_Double* Fxu_HeapDoubleGetMax ( Fxu_HeapDouble *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 288 of file fxuHeapD.c.

00289 {
00290         Fxu_Double * pDiv;
00291         if ( p->nItems == 0 )
00292                 return NULL;
00293         // prepare the return value
00294         pDiv = p->pTree[1];
00295         pDiv->HNum = 0;
00296         // put the last entry on top
00297         // decrement the number of entries
00298         p->pTree[1] = p->pTree[p->nItems--];
00299         p->pTree[1]->HNum = 1;
00300         // move the top entry down if necessary
00301         Fxu_HeapDoubleMoveDn( p, p->pTree[1] );
00302         return pDiv;     
00303 }

void Fxu_HeapDoubleInsert ( Fxu_HeapDouble *  p,
Fxu_Double *  pDiv 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 198 of file fxuHeapD.c.

00199 {
00200         if ( p->nItems == p->nItemsAlloc )
00201                 Fxu_HeapDoubleResize( p );
00202         // put the last entry to the last place and move up
00203         p->pTree[++p->nItems] = pDiv;
00204         pDiv->HNum = p->nItems;
00205         // move the last entry up if necessary
00206         Fxu_HeapDoubleMoveUp( p, pDiv );
00207 }

void Fxu_HeapDoublePrint ( FILE *  pFile,
Fxu_HeapDouble *  p 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 114 of file fxuHeapD.c.

00115 {
00116         Fxu_Double * pDiv;
00117         int Counter = 1;
00118         int Degree  = 1;
00119 
00120         Fxu_HeapDoubleCheck( p );
00121         fprintf( pFile, "The contents of the heap:\n" );
00122         fprintf( pFile, "Level %d:  ", Degree );
00123         Fxu_HeapDoubleForEachItem( p, pDiv )
00124         {
00125                 assert( Counter == p->pTree[Counter]->HNum );
00126                 fprintf( pFile, "%2d=%3d  ", Counter, FXU_HEAP_DOUBLE_WEIGHT(p->pTree[Counter]) );
00127                 if ( ++Counter == (1 << Degree) )
00128                 {
00129                         fprintf( pFile, "\n" );
00130                         Degree++;
00131                         fprintf( pFile, "Level %d:  ", Degree );
00132                 }
00133         }
00134         fprintf( pFile, "\n" );
00135         fprintf( pFile, "End of the heap printout.\n" );
00136 }

Fxu_Double* Fxu_HeapDoubleReadMax ( Fxu_HeapDouble *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 270 of file fxuHeapD.c.

00271 {
00272         if ( p->nItems == 0 )
00273                 return NULL;
00274         return p->pTree[1];      
00275 }

int Fxu_HeapDoubleReadMaxWeight ( Fxu_HeapDouble *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 316 of file fxuHeapD.c.

00317 {
00318         if ( p->nItems == 0 )
00319                 return -1;
00320         else
00321                 return FXU_HEAP_DOUBLE_WEIGHT(p->pTree[1]);
00322 }

Fxu_HeapDouble* Fxu_HeapDoubleStart (  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 55 of file fxuHeapD.c.

00056 {
00057         Fxu_HeapDouble * p;
00058         p = ALLOC( Fxu_HeapDouble, 1 );
00059         memset( p, 0, sizeof(Fxu_HeapDouble) );
00060         p->nItems      = 0;
00061         p->nItemsAlloc = 10000;
00062         p->pTree       = ALLOC( Fxu_Double *, p->nItemsAlloc + 1 );
00063         p->pTree[0]    = NULL;
00064         return p;
00065 }

void Fxu_HeapDoubleStop ( Fxu_HeapDouble *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 96 of file fxuHeapD.c.

00097 {
00098         free( p->pTree );
00099         free( p );
00100 }

void Fxu_HeapDoubleUpdate ( Fxu_HeapDouble *  p,
Fxu_Double *  pDiv 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 220 of file fxuHeapD.c.

00221 {
00222 //printf( "Updating divisor %d.\n", pDiv->Num );
00223 
00224         FXU_HEAP_DOUBLE_ASSERT(p,pDiv);
00225         if ( FXU_HEAP_DOUBLE_PARENT_EXISTS(p,pDiv) && 
00226          FXU_HEAP_DOUBLE_WEIGHT(pDiv) > FXU_HEAP_DOUBLE_WEIGHT( FXU_HEAP_DOUBLE_PARENT(p,pDiv) ) )
00227                 Fxu_HeapDoubleMoveUp( p, pDiv );
00228         else if ( FXU_HEAP_DOUBLE_CHILD1_EXISTS(p,pDiv) && 
00229         FXU_HEAP_DOUBLE_WEIGHT(pDiv) < FXU_HEAP_DOUBLE_WEIGHT( FXU_HEAP_DOUBLE_CHILD1(p,pDiv) ) )
00230                 Fxu_HeapDoubleMoveDn( p, pDiv );
00231         else if ( FXU_HEAP_DOUBLE_CHILD2_EXISTS(p,pDiv) && 
00232         FXU_HEAP_DOUBLE_WEIGHT(pDiv) < FXU_HEAP_DOUBLE_WEIGHT( FXU_HEAP_DOUBLE_CHILD2(p,pDiv) ) )
00233                 Fxu_HeapDoubleMoveDn( p, pDiv );
00234 }

void Fxu_HeapSingleCheck ( Fxu_HeapSingle *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 152 of file fxuHeapS.c.

00153 {
00154         Fxu_Single * pSingle;
00155         Fxu_HeapSingleForEachItem( p, pSingle )
00156         {
00157                 assert( pSingle->HNum == p->i );
00158         Fxu_HeapSingleCheckOne( p, pSingle );
00159         }
00160 }

void Fxu_HeapSingleCheckOne ( Fxu_HeapSingle *  p,
Fxu_Single *  pSingle 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 173 of file fxuHeapS.c.

00174 {
00175     int Weight1, Weight2;
00176         if ( FXU_HEAP_SINGLE_CHILD1_EXISTS(p,pSingle) )
00177         {
00178         Weight1 = FXU_HEAP_SINGLE_WEIGHT(pSingle);
00179         Weight2 = FXU_HEAP_SINGLE_WEIGHT( FXU_HEAP_SINGLE_CHILD1(p,pSingle) );
00180         assert( Weight1 >= Weight2 );
00181         }
00182         if ( FXU_HEAP_SINGLE_CHILD2_EXISTS(p,pSingle) )
00183         {
00184         Weight1 = FXU_HEAP_SINGLE_WEIGHT(pSingle);
00185         Weight2 = FXU_HEAP_SINGLE_WEIGHT( FXU_HEAP_SINGLE_CHILD2(p,pSingle) );
00186         assert( Weight1 >= Weight2 );
00187         }
00188 }

void Fxu_HeapSingleDelete ( Fxu_HeapSingle *  p,
Fxu_Single *  pSingle 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 248 of file fxuHeapS.c.

00249 {
00250     int Place = pSingle->HNum;
00251         FXU_HEAP_SINGLE_ASSERT(p,pSingle);
00252         // put the last entry to the deleted place
00253         // decrement the number of entries
00254         p->pTree[Place] = p->pTree[p->nItems--];
00255         p->pTree[Place]->HNum = Place;
00256         // move the top entry down if necessary
00257         Fxu_HeapSingleUpdate( p, p->pTree[Place] );
00258     pSingle->HNum = 0;
00259 }

Fxu_Single* Fxu_HeapSingleGetMax ( Fxu_HeapSingle *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 290 of file fxuHeapS.c.

00291 {
00292         Fxu_Single * pSingle;
00293         if ( p->nItems == 0 )
00294                 return NULL;
00295         // prepare the return value
00296         pSingle = p->pTree[1];
00297         pSingle->HNum = 0;
00298         // put the last entry on top
00299         // decrement the number of entries
00300         p->pTree[1] = p->pTree[p->nItems--];
00301         p->pTree[1]->HNum = 1;
00302         // move the top entry down if necessary
00303         Fxu_HeapSingleMoveDn( p, p->pTree[1] );
00304         return pSingle;  
00305 }

void Fxu_HeapSingleInsert ( Fxu_HeapSingle *  p,
Fxu_Single *  pSingle 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 201 of file fxuHeapS.c.

00202 {
00203         if ( p->nItems == p->nItemsAlloc )
00204                 Fxu_HeapSingleResize( p );
00205         // put the last entry to the last place and move up
00206         p->pTree[++p->nItems] = pSingle;
00207         pSingle->HNum = p->nItems;
00208         // move the last entry up if necessary
00209         Fxu_HeapSingleMoveUp( p, pSingle );
00210 }

void Fxu_HeapSinglePrint ( FILE *  pFile,
Fxu_HeapSingle *  p 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 117 of file fxuHeapS.c.

00118 {
00119         Fxu_Single * pSingle;
00120         int Counter = 1;
00121         int Degree  = 1;
00122 
00123         Fxu_HeapSingleCheck( p );
00124         fprintf( pFile, "The contents of the heap:\n" );
00125         fprintf( pFile, "Level %d:  ", Degree );
00126         Fxu_HeapSingleForEachItem( p, pSingle )
00127         {
00128                 assert( Counter == p->pTree[Counter]->HNum );
00129                 fprintf( pFile, "%2d=%3d  ", Counter, FXU_HEAP_SINGLE_WEIGHT(p->pTree[Counter]) );
00130                 if ( ++Counter == (1 << Degree) )
00131                 {
00132                         fprintf( pFile, "\n" );
00133                         Degree++;
00134                         fprintf( pFile, "Level %d:  ", Degree );
00135                 }
00136         }
00137         fprintf( pFile, "\n" );
00138         fprintf( pFile, "End of the heap printout.\n" );
00139 }

Fxu_Single* Fxu_HeapSingleReadMax ( Fxu_HeapSingle *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 272 of file fxuHeapS.c.

00273 {
00274         if ( p->nItems == 0 )
00275                 return NULL;
00276         return p->pTree[1];
00277 }

int Fxu_HeapSingleReadMaxWeight ( Fxu_HeapSingle *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 318 of file fxuHeapS.c.

00319 {
00320         if ( p->nItems == 0 )
00321                 return -1;
00322         return FXU_HEAP_SINGLE_WEIGHT(p->pTree[1]);
00323 }

Fxu_HeapSingle* Fxu_HeapSingleStart (  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 55 of file fxuHeapS.c.

00056 {
00057         Fxu_HeapSingle * p;
00058         p = ALLOC( Fxu_HeapSingle, 1 );
00059         memset( p, 0, sizeof(Fxu_HeapSingle) );
00060         p->nItems      = 0;
00061         p->nItemsAlloc = 2000;
00062         p->pTree       = ALLOC( Fxu_Single *, p->nItemsAlloc + 10 );
00063         p->pTree[0]    = NULL;
00064         return p;
00065 }

void Fxu_HeapSingleStop ( Fxu_HeapSingle *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 96 of file fxuHeapS.c.

00097 {
00098     int i;
00099     i = 0;
00100         free( p->pTree );
00101     i = 1;
00102         free( p );
00103 }

void Fxu_HeapSingleUpdate ( Fxu_HeapSingle *  p,
Fxu_Single *  pSingle 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 223 of file fxuHeapS.c.

00224 {
00225         FXU_HEAP_SINGLE_ASSERT(p,pSingle);
00226         if ( FXU_HEAP_SINGLE_PARENT_EXISTS(p,pSingle) && 
00227          FXU_HEAP_SINGLE_WEIGHT(pSingle) > FXU_HEAP_SINGLE_WEIGHT( FXU_HEAP_SINGLE_PARENT(p,pSingle) ) )
00228                 Fxu_HeapSingleMoveUp( p, pSingle );
00229         else if ( FXU_HEAP_SINGLE_CHILD1_EXISTS(p,pSingle) && 
00230         FXU_HEAP_SINGLE_WEIGHT(pSingle) < FXU_HEAP_SINGLE_WEIGHT( FXU_HEAP_SINGLE_CHILD1(p,pSingle) ) )
00231                 Fxu_HeapSingleMoveDn( p, pSingle );
00232         else if ( FXU_HEAP_SINGLE_CHILD2_EXISTS(p,pSingle) && 
00233         FXU_HEAP_SINGLE_WEIGHT(pSingle) < FXU_HEAP_SINGLE_WEIGHT( FXU_HEAP_SINGLE_CHILD2(p,pSingle) ) )
00234                 Fxu_HeapSingleMoveDn( p, pSingle );
00235 }

void Fxu_ListCubeAddLiteral ( Fxu_Cube *  pCube,
Fxu_Lit *  pLink 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 280 of file fxuList.c.

00281 {
00282         Fxu_ListLit * pList = &(pCube->lLits);
00283         if ( pList->pHead == NULL )
00284         {
00285                 pList->pHead = pLink;
00286                 pList->pTail = pLink;
00287                 pLink->pHPrev = NULL;
00288                 pLink->pHNext = NULL;
00289         }
00290         else
00291         {
00292                 pLink->pHNext = NULL;
00293                 pList->pTail->pHNext = pLink;
00294                 pLink->pHPrev = pList->pTail;
00295                 pList->pTail = pLink;
00296         }
00297         pList->nItems++;
00298 }

void Fxu_ListCubeDelLiteral ( Fxu_Cube *  pCube,
Fxu_Lit *  pLink 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 311 of file fxuList.c.

00312 {
00313         Fxu_ListLit * pList = &(pCube->lLits);
00314         if ( pList->pHead == pLink )
00315                  pList->pHead = pLink->pHNext;
00316         if ( pList->pTail == pLink )
00317                  pList->pTail = pLink->pHPrev;
00318         if ( pLink->pHPrev )
00319                  pLink->pHPrev->pHNext = pLink->pHNext;
00320         if ( pLink->pHNext )
00321                  pLink->pHNext->pHPrev = pLink->pHPrev;
00322         pList->nItems--;
00323 }

void Fxu_ListDoubleAddPairFirst ( Fxu_Double *  pDiv,
Fxu_Pair *  pLink 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 430 of file fxuList.c.

00431 {
00432         Fxu_ListPair * pList = &pDiv->lPairs;
00433         if ( pList->pHead == NULL )
00434         {
00435                 pList->pHead = pLink;
00436                 pList->pTail = pLink;
00437                 pLink->pDPrev = NULL;
00438                 pLink->pDNext = NULL;
00439         }
00440         else
00441         {
00442                 pLink->pDPrev = NULL;
00443                 pList->pHead->pDPrev = pLink;
00444                 pLink->pDNext = pList->pHead;
00445                 pList->pHead = pLink;
00446         }
00447         pList->nItems++;
00448 }

void Fxu_ListDoubleAddPairLast ( Fxu_Double *  pDiv,
Fxu_Pair *  pLink 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 399 of file fxuList.c.

00400 {
00401         Fxu_ListPair * pList = &pDiv->lPairs;
00402         if ( pList->pHead == NULL )
00403         {
00404                 pList->pHead = pLink;
00405                 pList->pTail = pLink;
00406                 pLink->pDPrev = NULL;
00407                 pLink->pDNext = NULL;
00408         }
00409         else
00410         {
00411                 pLink->pDNext = NULL;
00412                 pList->pTail->pDNext = pLink;
00413                 pLink->pDPrev = pList->pTail;
00414                 pList->pTail = pLink;
00415         }
00416         pList->nItems++;
00417 }

void Fxu_ListDoubleAddPairMiddle ( Fxu_Double *  pDiv,
Fxu_Pair *  pSpot,
Fxu_Pair *  pLink 
)

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

Synopsis [Adds the entry in the middle of the list after the spot.]

Description [Assumes that spot points to the link, after which the given link should be added. Spot cannot be NULL or the tail of the list. Therefore, the head and the tail of the list are not changed.]

SideEffects []

SeeAlso []

Definition at line 463 of file fxuList.c.

00464 {
00465         Fxu_ListPair * pList = &pDiv->lPairs;
00466         assert( pSpot );
00467         assert( pSpot != pList->pTail );
00468         pLink->pDPrev = pSpot;
00469         pLink->pDNext = pSpot->pDNext;
00470         pLink->pDPrev->pDNext = pLink;
00471         pLink->pDNext->pDPrev = pLink;
00472         pList->nItems++;
00473 }

void Fxu_ListDoubleDelPair ( Fxu_Double *  pDiv,
Fxu_Pair *  pLink 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 486 of file fxuList.c.

00487 {
00488         Fxu_ListPair * pList = &pDiv->lPairs;
00489         if ( pList->pHead == pLink )
00490                  pList->pHead = pLink->pDNext;
00491         if ( pList->pTail == pLink )
00492                  pList->pTail = pLink->pDPrev;
00493         if ( pLink->pDPrev )
00494                  pLink->pDPrev->pDNext = pLink->pDNext;
00495         if ( pLink->pDNext )
00496                  pLink->pDNext->pDPrev = pLink->pDPrev;
00497         pList->nItems--;
00498 }

void Fxu_ListMatrixAddCube ( Fxu_Matrix *  p,
Fxu_Cube *  pLink 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 101 of file fxuList.c.

00102 {
00103         Fxu_ListCube * pList = &p->lCubes;
00104         if ( pList->pHead == NULL )
00105         {
00106                 pList->pHead = pLink;
00107                 pList->pTail = pLink;
00108                 pLink->pPrev = NULL;
00109                 pLink->pNext = NULL;
00110         }
00111         else
00112         {
00113                 pLink->pNext = NULL;
00114                 pList->pTail->pNext = pLink;
00115                 pLink->pPrev = pList->pTail;
00116                 pList->pTail = pLink;
00117         }
00118         pList->nItems++;
00119 }

void Fxu_ListMatrixAddSingle ( Fxu_Matrix *  p,
Fxu_Single *  pLink 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 160 of file fxuList.c.

00161 {
00162         Fxu_ListSingle * pList = &p->lSingles;
00163         if ( pList->pHead == NULL )
00164         {
00165                 pList->pHead = pLink;
00166                 pList->pTail = pLink;
00167                 pLink->pPrev = NULL;
00168                 pLink->pNext = NULL;
00169         }
00170         else
00171         {
00172                 pLink->pNext = NULL;
00173                 pList->pTail->pNext = pLink;
00174                 pLink->pPrev = pList->pTail;
00175                 pList->pTail = pLink;
00176         }
00177         pList->nItems++;
00178 }

void Fxu_ListMatrixAddVariable ( Fxu_Matrix *  p,
Fxu_Var *  pLink 
)

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

FileName [fxuList.c]

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

Synopsis [Operations on lists.]

Author [MVSIS Group]

Affiliation [UC Berkeley]

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

Revision [

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file fxuList.c.

00043 {
00044         Fxu_ListVar * pList = &p->lVars;
00045         if ( pList->pHead == NULL )
00046         {
00047                 pList->pHead = pLink;
00048                 pList->pTail = pLink;
00049                 pLink->pPrev = NULL;
00050                 pLink->pNext = NULL;
00051         }
00052         else
00053         {
00054                 pLink->pNext = NULL;
00055                 pList->pTail->pNext = pLink;
00056                 pLink->pPrev = pList->pTail;
00057                 pList->pTail = pLink;
00058         }
00059         pList->nItems++;
00060 }

void Fxu_ListMatrixDelCube ( Fxu_Matrix *  p,
Fxu_Cube *  pLink 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 132 of file fxuList.c.

00133 {
00134         Fxu_ListCube * pList = &p->lCubes;
00135         if ( pList->pHead == pLink )
00136                  pList->pHead = pLink->pNext;
00137         if ( pList->pTail == pLink )
00138                  pList->pTail = pLink->pPrev;
00139         if ( pLink->pPrev )
00140                  pLink->pPrev->pNext = pLink->pNext;
00141         if ( pLink->pNext )
00142                  pLink->pNext->pPrev = pLink->pPrev;
00143         pList->nItems--;
00144 }

void Fxu_ListMatrixDelSingle ( Fxu_Matrix *  p,
Fxu_Single *  pLink 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 191 of file fxuList.c.

00192 {
00193         Fxu_ListSingle * pList = &p->lSingles;
00194         if ( pList->pHead == pLink )
00195                  pList->pHead = pLink->pNext;
00196         if ( pList->pTail == pLink )
00197                  pList->pTail = pLink->pPrev;
00198         if ( pLink->pPrev )
00199                  pLink->pPrev->pNext = pLink->pNext;
00200         if ( pLink->pNext )
00201                  pLink->pNext->pPrev = pLink->pPrev;
00202         pList->nItems--;
00203 }

void Fxu_ListMatrixDelVariable ( Fxu_Matrix *  p,
Fxu_Var *  pLink 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 73 of file fxuList.c.

00074 {
00075         Fxu_ListVar * pList = &p->lVars;
00076         if ( pList->pHead == pLink )
00077                  pList->pHead = pLink->pNext;
00078         if ( pList->pTail == pLink )
00079                  pList->pTail = pLink->pPrev;
00080         if ( pLink->pPrev )
00081                  pLink->pPrev->pNext = pLink->pNext;
00082         if ( pLink->pNext )
00083                  pLink->pNext->pPrev = pLink->pPrev;
00084         pList->nItems--;
00085 }

void Fxu_ListTableAddDivisor ( Fxu_Matrix *  p,
Fxu_Double *  pLink 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 219 of file fxuList.c.

00220 {
00221         Fxu_ListDouble * pList = &(p->pTable[pLink->Key]);
00222         if ( pList->pHead == NULL )
00223         {
00224                 pList->pHead = pLink;
00225                 pList->pTail = pLink;
00226                 pLink->pPrev = NULL;
00227                 pLink->pNext = NULL;
00228         }
00229         else
00230         {
00231                 pLink->pNext = NULL;
00232                 pList->pTail->pNext = pLink;
00233                 pLink->pPrev = pList->pTail;
00234                 pList->pTail = pLink;
00235         }
00236         pList->nItems++;
00237     p->nDivs++;
00238 }

void Fxu_ListTableDelDivisor ( Fxu_Matrix *  p,
Fxu_Double *  pLink 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 251 of file fxuList.c.

00252 {
00253         Fxu_ListDouble * pList = &(p->pTable[pLink->Key]);
00254         if ( pList->pHead == pLink )
00255                  pList->pHead = pLink->pNext;
00256         if ( pList->pTail == pLink )
00257                  pList->pTail = pLink->pPrev;
00258         if ( pLink->pPrev )
00259                  pLink->pPrev->pNext = pLink->pNext;
00260         if ( pLink->pNext )
00261                  pLink->pNext->pPrev = pLink->pPrev;
00262         pList->nItems--;
00263     p->nDivs--;
00264 }

void Fxu_ListVarAddLiteral ( Fxu_Var *  pVar,
Fxu_Lit *  pLink 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 339 of file fxuList.c.

00340 {
00341         Fxu_ListLit * pList = &(pVar->lLits);
00342         if ( pList->pHead == NULL )
00343         {
00344                 pList->pHead = pLink;
00345                 pList->pTail = pLink;
00346                 pLink->pVPrev = NULL;
00347                 pLink->pVNext = NULL;
00348         }
00349         else
00350         {
00351                 pLink->pVNext = NULL;
00352                 pList->pTail->pVNext = pLink;
00353                 pLink->pVPrev = pList->pTail;
00354                 pList->pTail = pLink;
00355         }
00356         pList->nItems++;
00357 }

void Fxu_ListVarDelLiteral ( Fxu_Var *  pVar,
Fxu_Lit *  pLink 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 370 of file fxuList.c.

00371 {
00372         Fxu_ListLit * pList = &(pVar->lLits);
00373         if ( pList->pHead == pLink )
00374                  pList->pHead = pLink->pVNext;
00375         if ( pList->pTail == pLink )
00376                  pList->pTail = pLink->pVPrev;
00377         if ( pLink->pVPrev )
00378                  pLink->pVPrev->pVNext = pLink->pVNext;
00379         if ( pLink->pVNext )
00380                  pLink->pVNext->pVPrev = pLink->pVPrev;
00381         pList->nItems--;
00382 }

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_MatrixComputeSingles ( Fxu_Matrix *  p,
int  fUse0,
int  nSingleMax 
)

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

Synopsis [Computes and adds all single-cube divisors to storage.]

Description [This procedure should be called once when the matrix is already contructed before the process of logic extraction begins..]

SideEffects []

SeeAlso []

Definition at line 44 of file fxuSingle.c.

00045 {
00046     Fxu_Var * pVar;
00047     Vec_Ptr_t * vSingles;
00048     int i, k;
00049     // set the weight limit
00050     p->nWeightLimit = 1 - fUse0;
00051     // iterate through columns in the matrix and collect single-cube divisors
00052     vSingles = Vec_PtrAlloc( 10000 );
00053     Fxu_MatrixForEachVariable( p, pVar )
00054         Fxu_MatrixComputeSinglesOneCollect( p, pVar, vSingles );
00055     p->nSingleTotal = Vec_PtrSize(vSingles) / 3;
00056     // check if divisors should be filtered
00057     if ( Vec_PtrSize(vSingles) > nSingleMax )
00058     {
00059         int * pWeigtCounts, nDivCount, Weight, i, c;;
00060         assert( Vec_PtrSize(vSingles) % 3 == 0 );
00061         // count how many divisors have the given weight
00062         pWeigtCounts = ALLOC( int, 1000 );
00063         memset( pWeigtCounts, 0, sizeof(int) * 1000 );
00064         for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 )
00065         {
00066             Weight = (int)Vec_PtrEntry(vSingles, i);
00067             if ( Weight >= 999 )
00068                 pWeigtCounts[999]++;
00069             else
00070                 pWeigtCounts[Weight]++;
00071         }
00072         // select the bound on the weight (above this bound, singles will be included)
00073         nDivCount = 0;
00074         for ( c = 999; c >= 0; c-- )
00075         {
00076             nDivCount += pWeigtCounts[c];
00077             if ( nDivCount >= nSingleMax )
00078                 break;
00079         }
00080         free( pWeigtCounts );
00081         // collect singles with the given costs
00082         k = 0;
00083         for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 )
00084         {
00085             Weight = (int)Vec_PtrEntry(vSingles, i);
00086             if ( Weight < c )
00087                 continue;
00088             Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-2) );
00089             Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-1) );
00090             Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i) );
00091             if ( k/3 == nSingleMax )
00092                 break;
00093         }
00094         Vec_PtrShrink( vSingles, k );
00095         // adjust the weight limit
00096         p->nWeightLimit = c;
00097     }
00098     // collect the selected divisors
00099     assert( Vec_PtrSize(vSingles) % 3 == 0 );
00100     for ( i = 0; i < Vec_PtrSize(vSingles); i += 3 )
00101     {
00102         Fxu_MatrixAddSingle( p, 
00103             Vec_PtrEntry(vSingles,i), 
00104             Vec_PtrEntry(vSingles,i+1), 
00105             (int)Vec_PtrEntry(vSingles,i+2) );
00106     }
00107     Vec_PtrFree( vSingles );
00108 }

void Fxu_MatrixComputeSinglesOne ( Fxu_Matrix *  p,
Fxu_Var *  pVar 
)

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

Synopsis [Adds the single-cube divisors associated with a new column.]

Description []

SideEffects []

SeeAlso []

Definition at line 181 of file fxuSingle.c.

00182 {
00183     Fxu_Lit * pLitV, * pLitH;
00184     Fxu_Var * pVar2;
00185     int Coin;
00186     int WeightCur;
00187 
00188     // start collecting the affected vars
00189     Fxu_MatrixRingVarsStart( p );
00190     // go through all the literals of this variable
00191     for ( pLitV = pVar->lLits.pHead; pLitV; pLitV = pLitV->pVNext )
00192         // for this literal, go through all the horizontal literals
00193         for ( pLitH = pLitV->pHPrev; pLitH; pLitH = pLitH->pHPrev )
00194         {
00195             // get another variable
00196             pVar2 = pLitH->pVar;
00197             // skip the var if it is already used
00198             if ( pVar2->pOrder )
00199                 continue;
00200             // skip the var if it belongs to the same node
00201 //            if ( pValue2Node[pVar->iVar] == pValue2Node[pVar2->iVar] )
00202 //                continue;
00203             // collect the var
00204             Fxu_MatrixRingVarsAdd( p, pVar2 );
00205         }
00206     // stop collecting the selected vars
00207     Fxu_MatrixRingVarsStop( p );
00208 
00209     // iterate through the selected vars
00210     Fxu_MatrixForEachVarInRing( p, pVar2 )
00211     {
00212         // count the coincidence
00213         Coin = Fxu_SingleCountCoincidence( p, pVar2, pVar );
00214         assert( Coin > 0 );
00215         // get the new weight
00216         WeightCur = Coin - 2;
00217         // peformance fix (August 24, 2007)
00218 //        if ( WeightCur >= 0 )
00219 //        Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur );
00220         if ( WeightCur >= p->nWeightLimit )
00221             Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur );
00222     }
00223     // unmark the vars
00224     Fxu_MatrixRingVarsUnmark( p );
00225 }

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 }

void Fxu_MatrixPrint ( FILE *  pFile,
Fxu_Matrix *  p 
)

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

FileName [fxuPrint.c]

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

Synopsis [Various printing procedures.]

Author [MVSIS Group]

Affiliation [UC Berkeley]

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

Revision [

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 40 of file fxuPrint.c.

00041 {
00042         Fxu_Var * pVar;
00043         Fxu_Cube * pCube;
00044         Fxu_Double * pDiv;
00045     Fxu_Single * pSingle;
00046         Fxu_Lit * pLit;
00047         Fxu_Pair * pPair;
00048         int i, LastNum;
00049         int fStdout;
00050 
00051         fStdout = 1;
00052         if ( pFile == NULL )
00053         {
00054                 pFile = fopen( "matrix.txt", "w" );
00055                 fStdout = 0;
00056         }
00057 
00058         fprintf( pFile, "Matrix has %d vars, %d cubes, %d literals, %d divisors.\n", 
00059                 p->lVars.nItems, p->lCubes.nItems, p->nEntries, p->nDivs );
00060         fprintf( pFile, "Divisors selected so far: single = %d, double = %d.\n", 
00061                 p->nDivs1, p->nDivs2 );
00062         fprintf( pFile, "\n" );
00063 
00064         // print the numbers on top of the matrix
00065         for ( i = 0; i < 12; i++ )
00066                 fprintf( pFile, " " );
00067         Fxu_MatrixForEachVariable( p, pVar )
00068                 fprintf( pFile, "%d", pVar->iVar % 10 );
00069         fprintf( pFile, "\n" );
00070 
00071         // print the rows
00072         Fxu_MatrixForEachCube( p, pCube )
00073         {
00074                 fprintf( pFile, "%4d", pCube->iCube );
00075                 fprintf( pFile, "  " );
00076                 fprintf( pFile, "%4d", pCube->pVar->iVar );
00077                 fprintf( pFile, "  " );
00078 
00079                 // print the literals
00080                 LastNum = -1;
00081                 Fxu_CubeForEachLiteral( pCube, pLit )
00082                 {
00083                         for ( i = LastNum + 1; i < pLit->pVar->iVar; i++ )
00084                                 fprintf( pFile, "." );
00085                         fprintf( pFile, "1" );
00086                         LastNum = i;
00087                 }
00088                 for ( i = LastNum + 1; i < p->lVars.nItems; i++ )
00089                         fprintf( pFile, "." );
00090                 fprintf( pFile, "\n" );
00091         }
00092         fprintf( pFile, "\n" );
00093 
00094         // print the double-cube divisors
00095         fprintf( pFile, "The double divisors are:\n" );
00096         Fxu_MatrixForEachDouble( p, pDiv, i )
00097         {
00098                 fprintf( pFile, "Divisor #%3d (lit=%d,%d) (w=%2d):  ", 
00099                         pDiv->Num, pDiv->lPairs.pHead->nLits1, 
00100             pDiv->lPairs.pHead->nLits2, pDiv->Weight );
00101                 Fxu_DoubleForEachPair( pDiv, pPair )
00102                         fprintf( pFile, " <%d, %d> (b=%d)", 
00103                                 pPair->pCube1->iCube, pPair->pCube2->iCube, pPair->nBase );
00104                 fprintf( pFile, "\n" );
00105         }
00106     fprintf( pFile, "\n" );
00107 
00108         // print the divisors associated with each cube
00109         fprintf( pFile, "The cubes are:\n" );
00110         Fxu_MatrixForEachCube( p, pCube )
00111         {
00112                 fprintf( pFile, "Cube #%3d: ", pCube->iCube );
00113         if ( pCube->pVar->ppPairs )
00114                     Fxu_CubeForEachPair( pCube, pPair, i )
00115                                 fprintf( pFile, " <%d %d> (d=%d) (b=%d)", 
00116                                         pPair->iCube1, pPair->iCube2, pPair->pDiv->Num, pPair->nBase );
00117                 fprintf( pFile, "\n" );
00118         }
00119     fprintf( pFile, "\n" );
00120 
00121         // print the single-cube divisors
00122         fprintf( pFile, "The single divisors are:\n" );
00123         Fxu_MatrixForEachSingle( p, pSingle )
00124         {
00125                 fprintf( pFile, "Single-cube divisor #%5d: Var1 = %4d. Var2 = %4d. Weight = %2d\n", 
00126                         pSingle->Num, pSingle->pVar1->iVar, pSingle->pVar2->iVar, pSingle->Weight );
00127         }
00128     fprintf( pFile, "\n" );
00129 
00130 /*
00131     {
00132         int Index;
00133                 fprintf( pFile, "Distribution of divisors in the hash table:\n" );
00134         for ( Index = 0; Index < p->nTableSize; Index++ )
00135             fprintf( pFile, " %d", p->pTable[Index].nItems );
00136                 fprintf( pFile, "\n" );
00137     }
00138 */
00139         if ( !fStdout )
00140                 fclose( pFile );
00141 }

void Fxu_MatrixPrintDivisorProfile ( FILE *  pFile,
Fxu_Matrix *  p 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 154 of file fxuPrint.c.

00155 {
00156     Fxu_Double * pDiv;
00157     int WeightMax;
00158     int * pProfile;
00159     int Counter1; // the number of -1 weight
00160     int CounterL; // the number of less than -1 weight
00161     int i;
00162 
00163     WeightMax = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
00164     pProfile = ALLOC( int, (WeightMax + 1) );
00165     memset( pProfile, 0, sizeof(int) * (WeightMax + 1) );
00166 
00167     Counter1 = 0;
00168     CounterL = 0;
00169         Fxu_MatrixForEachDouble( p, pDiv, i )
00170     {
00171         assert( pDiv->Weight <= WeightMax );
00172         if ( pDiv->Weight == -1 )
00173             Counter1++;
00174         else if ( pDiv->Weight < 0 )
00175             CounterL++;
00176         else
00177             pProfile[ pDiv->Weight ]++;
00178     }
00179 
00180         fprintf( pFile, "The double divisors profile:\n" );
00181         fprintf( pFile, "Weight  < -1 divisors = %6d\n", CounterL );
00182         fprintf( pFile, "Weight    -1 divisors = %6d\n", Counter1 );
00183     for ( i = 0; i <= WeightMax; i++ )
00184         if ( pProfile[i] )
00185                 fprintf( pFile, "Weight   %3d divisors = %6d\n", i, pProfile[i] );
00186         fprintf( pFile, "End of divisor profile printout\n" );
00187     FREE( pProfile );
00188 }

void Fxu_MatrixRingCubesUnmark ( Fxu_Matrix *  p  ) 

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

Synopsis [Unmarks the cubes in the ring.]

Description []

SideEffects []

SeeAlso []

Definition at line 181 of file fxu.c.

00182 {
00183         Fxu_Cube * pCube, * pCube2;
00184     // unmark the cubes
00185     Fxu_MatrixForEachCubeInRingSafe( p, pCube, pCube2 )
00186         pCube->pOrder = NULL;
00187     Fxu_MatrixRingCubesReset( p );
00188 }

void Fxu_MatrixRingVarsUnmark ( Fxu_Matrix *  p  ) 

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

Synopsis [Unmarks the vars in the ring.]

Description []

SideEffects []

SeeAlso []

Definition at line 202 of file fxu.c.

00203 {
00204         Fxu_Var * pVar, * pVar2;
00205     // unmark the vars
00206     Fxu_MatrixForEachVarInRingSafe( p, pVar, pVar2 )
00207         pVar->pOrder = NULL;
00208     Fxu_MatrixRingVarsReset( p );
00209 }

char* Fxu_MemFetch ( Fxu_Matrix *  p,
int  nBytes 
)

FUNCTION DEFINITIONS ///

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 223 of file fxu.c.

00224 {
00225     s_MemoryTotal += nBytes;
00226     if ( s_MemoryPeak < s_MemoryTotal )
00227         s_MemoryPeak = s_MemoryTotal;
00228 //    return malloc( nBytes );
00229     return Extra_MmFixedEntryFetch( p->pMemMan );
00230 }

void Fxu_MemRecycle ( Fxu_Matrix *  p,
char *  pItem,
int  nBytes 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 243 of file fxu.c.

00244 {
00245     s_MemoryTotal -= nBytes;
00246 //    free( pItem );
00247     Extra_MmFixedEntryRecycle( p->pMemMan, pItem );
00248 }

void Fxu_PairAdd ( Fxu_Pair *  pPair  ) 

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

Synopsis [Adds the pair to storage.]

Description []

SideEffects []

SeeAlso []

Definition at line 540 of file fxuPair.c.

00541 {
00542     Fxu_Var * pVar;
00543 
00544     pVar = pPair->pCube1->pVar;
00545         assert( pVar == pPair->pCube2->pVar );
00546 
00547         pVar->ppPairs[pPair->iCube1][pPair->iCube2] = pPair;
00548         pVar->ppPairs[pPair->iCube2][pPair->iCube1] = pPair;
00549 }

Fxu_Pair* Fxu_PairAlloc ( Fxu_Matrix *  p,
Fxu_Cube *  pCube1,
Fxu_Cube *  pCube2 
)

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

Synopsis [Adds the pair to storage.]

Description []

SideEffects []

SeeAlso []

Definition at line 516 of file fxuPair.c.

00517 {
00518     Fxu_Pair * pPair;
00519         assert( pCube1->pVar == pCube2->pVar );
00520         pPair = MEM_ALLOC_FXU( p, Fxu_Pair, 1 );
00521         memset( pPair, 0, sizeof(Fxu_Pair) );
00522         pPair->pCube1 = pCube1;
00523         pPair->pCube2 = pCube2;
00524         pPair->iCube1 = pCube1->iCube;
00525         pPair->iCube2 = pCube2->iCube;
00526     return pPair;
00527 }

void Fxu_PairAllocStorage ( Fxu_Var *  pVar,
int  nCubes 
)

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

Synopsis [Allocates the storage for cubes pairs.]

Description []

SideEffects []

SeeAlso []

Definition at line 449 of file fxuPair.c.

00450 {
00451     int k;
00452 //    assert( pVar->nCubes == 0 );
00453     pVar->nCubes  = nCubes;
00454         // allocate memory for all the pairs
00455         pVar->ppPairs    = ALLOC( Fxu_Pair **, nCubes );
00456         pVar->ppPairs[0] = ALLOC( Fxu_Pair *,  nCubes * nCubes );
00457     memset( pVar->ppPairs[0], 0, sizeof(Fxu_Pair *) * nCubes * nCubes );
00458     for ( k = 1; k < nCubes; k++ )
00459         pVar->ppPairs[k] = pVar->ppPairs[k-1] + nCubes;
00460 }

void Fxu_PairCanonicize ( Fxu_Cube **  ppCube1,
Fxu_Cube **  ppCube2 
)

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

Synopsis [Find the canonical permutation of two cubes in the pair.]

Description []

SideEffects []

SeeAlso []

Definition at line 72 of file fxuPair.c.

00073 {
00074         Fxu_Lit * pLit1, * pLit2;
00075         Fxu_Cube * pCubeTemp;
00076 
00077         // walk through the cubes to determine 
00078         // the one that has higher first variable
00079         pLit1 = (*ppCube1)->lLits.pHead;
00080         pLit2 = (*ppCube2)->lLits.pHead;
00081         while ( 1 )
00082         {
00083                 if ( pLit1->iVar == pLit2->iVar )
00084                 {
00085                         pLit1 = pLit1->pHNext;
00086                         pLit2 = pLit2->pHNext;
00087                         continue;
00088                 }
00089                 assert( pLit1 && pLit2 ); // this is true if the covers are SCC-free
00090                 if ( pLit1->iVar > pLit2->iVar )
00091                 { // swap the cubes
00092                         pCubeTemp = *ppCube1;
00093                         *ppCube1  = *ppCube2;
00094                         *ppCube2  = pCubeTemp;
00095                 }
00096                 break;
00097         }
00098 }

void Fxu_PairClearStorage ( Fxu_Cube *  pCube  ) 

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

Synopsis [Clears all pairs associated with this cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 473 of file fxuPair.c.

00474 {
00475     Fxu_Var * pVar;
00476         int i;
00477     pVar = pCube->pVar;
00478         for ( i = 0; i < pVar->nCubes; i++ )
00479         {
00480                 pVar->ppPairs[pCube->iCube][i] = NULL;
00481                 pVar->ppPairs[i][pCube->iCube] = NULL;
00482         }
00483 }

int Fxu_PairCompare ( Fxu_Pair *  pPair1,
Fxu_Pair *  pPair2 
)

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

Synopsis [Compares the two pairs.]

Description [Returns 1 if the divisors represented by these pairs are equal.]

SideEffects []

SeeAlso []

Definition at line 233 of file fxuPair.c.

00234 {
00235         Fxu_Lit * pD1C1, * pD1C2;
00236         Fxu_Lit * pD2C1, * pD2C2;
00237         int TopVar1, TopVar2;
00238         int Code;
00239 
00240         if ( pPair1->nLits1 != pPair2->nLits1 )
00241                 return 0;
00242         if ( pPair1->nLits2 != pPair2->nLits2 )
00243                 return 0;
00244 
00245         pD1C1 = pPair1->pCube1->lLits.pHead;
00246         pD1C2 = pPair1->pCube2->lLits.pHead;
00247 
00248         pD2C1 = pPair2->pCube1->lLits.pHead;
00249         pD2C2 = pPair2->pCube2->lLits.pHead;
00250 
00251         Code  = pD1C1? 8: 0;
00252         Code |= pD1C2? 4: 0;
00253         Code |= pD2C1? 2: 0;
00254         Code |= pD2C2? 1: 0;
00255         assert( Code == 15 );
00256 
00257         while ( 1 )
00258         {
00259                 switch ( Code )
00260                 {
00261                 case 0:  // -- --      NULL   NULL     NULL   NULL 
00262                         return 1;
00263                 case 1:  // -- -1      NULL   NULL     NULL   pD2C2
00264                         return 0;
00265                 case 2:  // -- 1-      NULL   NULL     pD2C1  NULL 
00266                         return 0;
00267                 case 3:  // -- 11      NULL   NULL     pD2C1  pD2C2
00268                         if ( pD2C1->iVar != pD2C2->iVar )
00269                                 return 0;
00270                         pD2C1 = pD2C1->pHNext;
00271                         pD2C2 = pD2C2->pHNext;
00272                         break;
00273                 case 4:  // -1 --      NULL   pD1C2    NULL   NULL 
00274                         return 0;
00275                 case 5:  // -1 -1      NULL   pD1C2    NULL   pD2C2
00276                         if ( pD1C2->iVar != pD2C2->iVar )
00277                                 return 0;
00278                         pD1C2 = pD1C2->pHNext;
00279                         pD2C2 = pD2C2->pHNext;
00280                         break;
00281                 case 6:  // -1 1-      NULL   pD1C2    pD2C1  NULL 
00282                         return 0;
00283                 case 7:  // -1 11      NULL   pD1C2    pD2C1  pD2C2
00284                         TopVar2 = Fxu_Min( pD2C1->iVar, pD2C2->iVar );
00285                         if ( TopVar2 == pD1C2->iVar )
00286                         {
00287                                 if ( pD2C1->iVar <= pD2C2->iVar )
00288                                         return 0;
00289                                 pD1C2 = pD1C2->pHNext;
00290                                 pD2C2 = pD2C2->pHNext;
00291                         }
00292                         else if ( TopVar2 < pD1C2->iVar )
00293                         {
00294                                 if ( pD2C1->iVar != pD2C2->iVar )
00295                                         return 0;
00296                                 pD2C1 = pD2C1->pHNext;
00297                                 pD2C2 = pD2C2->pHNext;
00298                         }
00299                         else
00300                                 return 0;
00301                         break;
00302                 case 8:  // 1- --      pD1C1  NULL     NULL   NULL 
00303                         return 0;
00304                 case 9:  // 1- -1      pD1C1  NULL     NULL   pD2C2
00305                         return 0;
00306                 case 10: // 1- 1-      pD1C1  NULL     pD2C1  NULL 
00307                         if ( pD1C1->iVar != pD2C1->iVar )
00308                                 return 0;
00309                         pD1C1 = pD1C1->pHNext;
00310                         pD2C1 = pD2C1->pHNext;
00311                         break;
00312                 case 11: // 1- 11      pD1C1  NULL     pD2C1  pD2C2
00313                         TopVar2 = Fxu_Min( pD2C1->iVar, pD2C2->iVar );
00314                         if ( TopVar2 == pD1C1->iVar )
00315                         {
00316                                 if ( pD2C1->iVar >= pD2C2->iVar )
00317                                         return 0;
00318                                 pD1C1 = pD1C1->pHNext;
00319                                 pD2C1 = pD2C1->pHNext;
00320                         }
00321                         else if ( TopVar2 < pD1C1->iVar )
00322                         {
00323                                 if ( pD2C1->iVar != pD2C2->iVar )
00324                                         return 0;
00325                                 pD2C1 = pD2C1->pHNext;
00326                                 pD2C2 = pD2C2->pHNext;
00327                         }
00328                         else
00329                                 return 0;
00330                         break;
00331                 case 12: // 11 --      pD1C1  pD1C2    NULL   NULL 
00332                         if ( pD1C1->iVar != pD1C2->iVar )
00333                                 return 0;
00334                         pD1C1 = pD1C1->pHNext;
00335                         pD1C2 = pD1C2->pHNext;
00336                         break;
00337                 case 13: // 11 -1      pD1C1  pD1C2    NULL   pD2C2
00338                         TopVar1 = Fxu_Min( pD1C1->iVar, pD1C2->iVar );
00339                         if ( TopVar1 == pD2C2->iVar )
00340                         {
00341                                 if ( pD1C1->iVar <= pD1C2->iVar )
00342                                         return 0;
00343                                 pD1C2 = pD1C2->pHNext;
00344                                 pD2C2 = pD2C2->pHNext;
00345                         }
00346                         else if ( TopVar1 < pD2C2->iVar )
00347                         {
00348                                 if ( pD1C1->iVar != pD1C2->iVar )
00349                                         return 0;
00350                                 pD1C1 = pD1C1->pHNext;
00351                                 pD1C2 = pD1C2->pHNext;
00352                         }
00353                         else
00354                                 return 0;
00355                         break;
00356                 case 14: // 11 1-      pD1C1  pD1C2    pD2C1  NULL 
00357                         TopVar1 = Fxu_Min( pD1C1->iVar, pD1C2->iVar );
00358                         if ( TopVar1 == pD2C1->iVar )
00359                         {
00360                                 if ( pD1C1->iVar >= pD1C2->iVar )
00361                                         return 0;
00362                                 pD1C1 = pD1C1->pHNext;
00363                                 pD2C1 = pD2C1->pHNext;
00364                         }
00365                         else if ( TopVar1 < pD2C1->iVar )
00366                         {
00367                                 if ( pD1C1->iVar != pD1C2->iVar )
00368                                         return 0;
00369                                 pD1C1 = pD1C1->pHNext;
00370                                 pD1C2 = pD1C2->pHNext;
00371                         }
00372                         else
00373                                 return 0;
00374                         break;
00375                 case 15: // 11 11      pD1C1  pD1C2    pD2C1  pD2C2
00376                         TopVar1 = Fxu_Min( pD1C1->iVar, pD1C2->iVar );
00377                         TopVar2 = Fxu_Min( pD2C1->iVar, pD2C2->iVar );
00378                         if ( TopVar1 == TopVar2 )
00379                         {
00380                                 if ( pD1C1->iVar == pD1C2->iVar )
00381                                 {
00382                                         if ( pD2C1->iVar != pD2C2->iVar )
00383                                                 return 0;
00384                                         pD1C1 = pD1C1->pHNext;
00385                                         pD1C2 = pD1C2->pHNext;
00386                                         pD2C1 = pD2C1->pHNext;
00387                                         pD2C2 = pD2C2->pHNext;
00388                                 }
00389                                 else
00390                                 {
00391                                         if ( pD2C1->iVar == pD2C2->iVar )
00392                                                 return 0;
00393                                         if ( pD1C1->iVar < pD1C2->iVar )
00394                                         {
00395                                                 if ( pD2C1->iVar > pD2C2->iVar )
00396                                                         return 0;
00397                                                 pD1C1 = pD1C1->pHNext;
00398                                                 pD2C1 = pD2C1->pHNext;
00399                                         }
00400                                         else
00401                                         {
00402                                                 if ( pD2C1->iVar < pD2C2->iVar )
00403                                                         return 0;
00404                                                 pD1C2 = pD1C2->pHNext;
00405                                                 pD2C2 = pD2C2->pHNext;
00406                                         }
00407                                 }
00408                         }
00409                         else if ( TopVar1 < TopVar2 )
00410                         {
00411                                 if ( pD1C1->iVar != pD1C2->iVar )
00412                                         return 0;
00413                                 pD1C1 = pD1C1->pHNext;
00414                                 pD1C2 = pD1C2->pHNext;
00415                         }
00416                         else 
00417                         {
00418                                 if ( pD2C1->iVar != pD2C2->iVar )
00419                                         return 0;
00420                                 pD2C1 = pD2C1->pHNext;
00421                                 pD2C2 = pD2C2->pHNext;
00422                         }
00423                         break;
00424                 default:
00425                         assert( 0 );
00426                         break;
00427                 }
00428 
00429                 Code  = pD1C1? 8: 0;
00430                 Code |= pD1C2? 4: 0;
00431                 Code |= pD2C1? 2: 0;
00432                 Code |= pD2C2? 1: 0;
00433         }
00434         return 1;
00435 }

void Fxu_PairFreeStorage ( Fxu_Var *  pVar  ) 

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

Synopsis [Clears all pairs associated with this cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 496 of file fxuPair.c.

00497 {
00498     if ( pVar->ppPairs )
00499     {
00500         FREE( pVar->ppPairs[0] );
00501         FREE( pVar->ppPairs );
00502     }
00503 }

unsigned Fxu_PairHashKey ( Fxu_Matrix *  p,
Fxu_Cube *  pCube1,
Fxu_Cube *  pCube2,
int *  pnBase,
int *  pnLits1,
int *  pnLits2 
)

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

Synopsis [Computes the hash key of the divisor represented by the pair of cubes.]

Description [Goes through the variables in both cubes. Skips the identical ones (this corresponds to making the cubes cube-free). Computes the hash value of the cubes. Assigns the number of literals in the base and in the cubes without base.]

SideEffects []

SeeAlso []

Definition at line 161 of file fxuPair.c.

00163 {
00164         int Offset1 = 100, Offset2 = 200;
00165     int nBase, nLits1, nLits2;
00166         Fxu_Lit * pLit1, * pLit2;
00167         unsigned Key;
00168 
00169         // compute the hash key
00170         Key    = 0;
00171         nLits1 = 0;
00172         nLits2 = 0;
00173         nBase  = 0;
00174         pLit1  = pCube1->lLits.pHead;
00175         pLit2  = pCube2->lLits.pHead;
00176         while ( 1 )
00177         {
00178                 if ( pLit1 && pLit2 )
00179                 {
00180                         if ( pLit1->iVar == pLit2->iVar )
00181                         { // ensure cube-free
00182                                 pLit1 = pLit1->pHNext;
00183                                 pLit2 = pLit2->pHNext;
00184                                 // add this literal to the base
00185                                 nBase++;
00186                         }
00187                         else if ( pLit1->iVar < pLit2->iVar )
00188                         {
00189                                 Key  ^= s_Primes[Offset1+nLits1] * pLit1->iVar;
00190                                 pLit1 = pLit1->pHNext;
00191                                 nLits1++;
00192                         }
00193                         else
00194                         {
00195                                 Key  ^= s_Primes[Offset2+nLits2] * pLit2->iVar;
00196                                 pLit2 = pLit2->pHNext;
00197                                 nLits2++;
00198                         }
00199                 }
00200                 else if ( pLit1 && !pLit2 )
00201                 {
00202                         Key  ^= s_Primes[Offset1+nLits1] * pLit1->iVar;
00203                         pLit1 = pLit1->pHNext;
00204                         nLits1++;
00205                 }
00206                 else if ( !pLit1 && pLit2 )
00207                 {
00208                         Key  ^= s_Primes[Offset2+nLits2] * pLit2->iVar;
00209                         pLit2 = pLit2->pHNext;
00210                         nLits2++;
00211                 }
00212                 else
00213                         break;
00214         }
00215     *pnBase  = nBase;
00216     *pnLits1 = nLits1;
00217     *pnLits2 = nLits2;
00218         return Key;
00219 }

unsigned Fxu_PairHashKeyArray ( Fxu_Matrix *  p,
int  piVarsC1[],
int  piVarsC2[],
int  nVarsC1,
int  nVarsC2 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 134 of file fxuPair.c.

00135 {
00136         int Offset1 = 100, Offset2 = 200, i;
00137         unsigned Key;
00138         // compute the hash key
00139         Key = 0;
00140     for ( i = 0; i < nVarsC1; i++ )
00141         Key ^= s_Primes[Offset1+i] * piVarsC1[i];
00142     for ( i = 0; i < nVarsC2; i++ )
00143         Key ^= s_Primes[Offset2+i] * piVarsC2[i];
00144         return Key;
00145 }

unsigned Fxu_PairHashKeyMv ( Fxu_Matrix *  p,
Fxu_Cube *  pCube1,
Fxu_Cube *  pCube2,
int *  pnBase,
int *  pnLits1,
int *  pnLits2 
)
int Fxu_Select ( Fxu_Matrix *  p,
Fxu_Single **  ppSingle,
Fxu_Double **  ppDouble 
)

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

Synopsis [Selects the best pair (Single,Double) and returns their weight.]

Description []

SideEffects []

SeeAlso []

Definition at line 54 of file fxuSelect.c.

00055 {
00056     // the top entries
00057     Fxu_Single * pSingles[MAX_SIZE_LOOKAHEAD];
00058     Fxu_Double * pDoubles[MAX_SIZE_LOOKAHEAD];
00059     // the complements
00060     Fxu_Double * pSCompl[MAX_SIZE_LOOKAHEAD];
00061     Fxu_Single * pDComplS[MAX_SIZE_LOOKAHEAD];
00062     Fxu_Double * pDComplD[MAX_SIZE_LOOKAHEAD];
00063     Fxu_Pair * pPair;
00064     int nSingles;
00065     int nDoubles;
00066     int i;
00067     int WeightBest;
00068     int WeightCur;
00069     int iNum, fBestS;
00070 
00071     // collect the top entries from the queues
00072     for ( nSingles = 0; nSingles < MAX_SIZE_LOOKAHEAD; nSingles++ )
00073     {
00074         pSingles[nSingles] = Fxu_HeapSingleGetMax( p->pHeapSingle );
00075         if ( pSingles[nSingles] == NULL )
00076             break;
00077     }
00078     // put them back into the queue
00079     for ( i = 0; i < nSingles; i++ )
00080         if ( pSingles[i] )
00081             Fxu_HeapSingleInsert( p->pHeapSingle, pSingles[i] );
00082         
00083     // the same for doubles
00084     // collect the top entries from the queues
00085     for ( nDoubles = 0; nDoubles < MAX_SIZE_LOOKAHEAD; nDoubles++ )
00086     {
00087         pDoubles[nDoubles] = Fxu_HeapDoubleGetMax( p->pHeapDouble );
00088         if ( pDoubles[nDoubles] == NULL )
00089             break;
00090     }
00091     // put them back into the queue
00092     for ( i = 0; i < nDoubles; i++ )
00093         if ( pDoubles[i] )
00094             Fxu_HeapDoubleInsert( p->pHeapDouble, pDoubles[i] );
00095 
00096     // for each single, find the complement double (if any)
00097     for ( i = 0; i < nSingles; i++ )
00098         if ( pSingles[i] )
00099             pSCompl[i] = Fxu_MatrixFindComplementSingle( p, pSingles[i] );
00100 
00101     // for each double, find the complement single or double (if any)
00102     for ( i = 0; i < nDoubles; i++ )
00103         if ( pDoubles[i] )
00104         {
00105             pPair = pDoubles[i]->lPairs.pHead;
00106             if ( pPair->nLits1 == 1 && pPair->nLits2 == 1 )
00107             {
00108                 pDComplS[i] = Fxu_MatrixFindComplementDouble2( p, pDoubles[i] );
00109                 pDComplD[i] = NULL;
00110             }
00111 //            else if ( pPair->nLits1 == 2 && pPair->nLits2 == 2 )
00112 //            {
00113 //                pDComplS[i] = NULL;
00114 //                pDComplD[i] = Fxu_MatrixFindComplementDouble4( p, pDoubles[i] );
00115 //            }
00116             else
00117             {
00118                 pDComplS[i] = NULL;
00119                 pDComplD[i] = NULL;
00120             }
00121         }
00122 
00123     // select the best pair
00124     WeightBest = -1;
00125     for ( i = 0; i < nSingles; i++ )
00126     {
00127         WeightCur = pSingles[i]->Weight;
00128         if ( pSCompl[i] )
00129         {
00130             // add the weight of the double
00131             WeightCur += pSCompl[i]->Weight;
00132             // there is no need to implement this double, so...
00133             pPair      = pSCompl[i]->lPairs.pHead;
00134             WeightCur += pPair->nLits1 + pPair->nLits2;
00135         }
00136         if ( WeightBest < WeightCur )
00137         {
00138             WeightBest = WeightCur;
00139             *ppSingle = pSingles[i];
00140             *ppDouble = pSCompl[i];
00141             fBestS = 1;
00142             iNum = i;
00143         }
00144     }
00145     for ( i = 0; i < nDoubles; i++ )
00146     {
00147         WeightCur = pDoubles[i]->Weight;
00148         if ( pDComplS[i] )
00149         {
00150             // add the weight of the single
00151             WeightCur += pDComplS[i]->Weight;
00152             // there is no need to implement this double, so...
00153             pPair      = pDoubles[i]->lPairs.pHead;
00154             WeightCur += pPair->nLits1 + pPair->nLits2;
00155         }
00156         if ( WeightBest < WeightCur )
00157         {
00158             WeightBest = WeightCur;
00159             *ppSingle = pDComplS[i];
00160             *ppDouble = pDoubles[i];
00161             fBestS = 0;
00162             iNum = i;
00163         }
00164     }
00165 /*
00166     // print the statistics
00167     printf( "\n" );
00168     for ( i = 0; i < nSingles; i++ )
00169     {
00170         printf( "Single #%d: Weight = %3d. ", i, pSingles[i]->Weight );
00171         printf( "Compl: " );
00172         if ( pSCompl[i] == NULL )
00173             printf( "None." );
00174         else
00175             printf( "D  Weight = %3d  Sum = %3d", 
00176                 pSCompl[i]->Weight, pSCompl[i]->Weight + pSingles[i]->Weight );
00177         printf( "\n" );
00178     }
00179     printf( "\n" );
00180     for ( i = 0; i < nDoubles; i++ )
00181     {
00182         printf( "Double #%d: Weight = %3d. ", i, pDoubles[i]->Weight );
00183         printf( "Compl: " );
00184         if ( pDComplS[i] == NULL && pDComplD[i] == NULL )
00185             printf( "None." );
00186         else if ( pDComplS[i] )
00187             printf( "S  Weight = %3d  Sum = %3d", 
00188                 pDComplS[i]->Weight, pDComplS[i]->Weight + pDoubles[i]->Weight );
00189         else if ( pDComplD[i] )
00190             printf( "D  Weight = %3d  Sum = %3d", 
00191                 pDComplD[i]->Weight, pDComplD[i]->Weight + pDoubles[i]->Weight );
00192         printf( "\n" );
00193     }
00194     if ( WeightBest == -1 )
00195         printf( "Selected NONE\n" );
00196     else
00197     {
00198         printf( "Selected = %s.  ", fBestS? "S": "D" );
00199         printf( "Number = %d.  ", iNum );
00200         printf( "Weight = %d.\n", WeightBest );
00201     }
00202     printf( "\n" );
00203 */
00204     return WeightBest;
00205 }

int Fxu_SelectSCD ( Fxu_Matrix *  p,
int  WeightLimit,
Fxu_Var **  ppVar1,
Fxu_Var **  ppVar2 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 522 of file fxuSelect.c.

00523 {
00524 //    int * pValue2Node = p->pValue2Node;
00525     Fxu_Var * pVar1;
00526     Fxu_Var * pVar2, * pVarTemp;
00527     Fxu_Lit * pLitV, * pLitH;
00528     int Coin;
00529     int CounterAll;
00530     int CounterTest;
00531     int WeightCur;
00532     int WeightBest;
00533 
00534     CounterAll = 0;
00535     CounterTest = 0;
00536 
00537     WeightBest = -10;
00538     
00539     // iterate through the columns in the matrix
00540     Fxu_MatrixForEachVariable( p, pVar1 )
00541     {
00542         // start collecting the affected vars
00543         Fxu_MatrixRingVarsStart( p );
00544 
00545         // go through all the literals of this variable
00546         for ( pLitV = pVar1->lLits.pHead; pLitV; pLitV = pLitV->pVNext )
00547         {
00548             // for this literal, go through all the horizontal literals
00549             for ( pLitH = pLitV->pHNext; pLitH; pLitH = pLitH->pHNext )
00550             {
00551                 // get another variable
00552                 pVar2 = pLitH->pVar;
00553                 CounterAll++;
00554                 // skip the var if it is already used
00555                 if ( pVar2->pOrder )
00556                     continue;
00557                 // skip the var if it belongs to the same node
00558 //                if ( pValue2Node[pVar1->iVar] == pValue2Node[pVar2->iVar] )
00559 //                    continue;
00560                 // collect the var
00561                 Fxu_MatrixRingVarsAdd( p, pVar2 );
00562             }
00563         }
00564         // stop collecting the selected vars
00565         Fxu_MatrixRingVarsStop( p );
00566 
00567         // iterate through the selected vars
00568         Fxu_MatrixForEachVarInRing( p, pVar2 )
00569         {
00570             CounterTest++;
00571 
00572             // count the coincidence
00573             Coin = Fxu_SingleCountCoincidence( p, pVar1, pVar2 );
00574             assert( Coin > 0 );
00575 
00576             // get the new weight
00577             WeightCur = Coin - 2;
00578 
00579             // compare the weights
00580             if ( WeightBest < WeightCur )
00581             {
00582                 WeightBest = WeightCur;
00583                 *ppVar1 = pVar1;
00584                 *ppVar2 = pVar2;
00585             }
00586         }
00587         // unmark the vars
00588         Fxu_MatrixForEachVarInRingSafe( p, pVar2, pVarTemp )
00589             pVar2->pOrder = NULL;
00590         Fxu_MatrixRingVarsReset( p );
00591     }
00592 
00593 //    if ( WeightBest == WeightLimit )
00594 //        return -1;
00595     return WeightBest;
00596 }

int Fxu_SingleCountCoincidence ( Fxu_Matrix *  p,
Fxu_Var *  pVar1,
Fxu_Var *  pVar2 
)

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

Synopsis [Computes the coincidence count of two columns.]

Description []

SideEffects []

SeeAlso []

Definition at line 238 of file fxuSingle.c.

00239 {
00240         Fxu_Lit * pLit1, * pLit2;
00241         int Result;
00242 
00243         // compute the coincidence count
00244         Result = 0;
00245         pLit1  = pVar1->lLits.pHead;
00246         pLit2  = pVar2->lLits.pHead;
00247         while ( 1 )
00248         {
00249                 if ( pLit1 && pLit2 )
00250                 {
00251                         if ( pLit1->pCube->pVar->iVar == pLit2->pCube->pVar->iVar )
00252                         { // the variables are the same
00253                             if ( pLit1->iCube == pLit2->iCube )
00254                             { // the literals are the same
00255                                     pLit1 = pLit1->pVNext;
00256                                     pLit2 = pLit2->pVNext;
00257                                     // add this literal to the coincidence
00258                                     Result++;
00259                             }
00260                             else if ( pLit1->iCube < pLit2->iCube )
00261                                     pLit1 = pLit1->pVNext;
00262                             else
00263                                     pLit2 = pLit2->pVNext;
00264                         }
00265                         else if ( pLit1->pCube->pVar->iVar < pLit2->pCube->pVar->iVar )
00266                                 pLit1 = pLit1->pVNext;
00267                         else
00268                                 pLit2 = pLit2->pVNext;
00269                 }
00270                 else if ( pLit1 && !pLit2 )
00271                         pLit1 = pLit1->pVNext;
00272                 else if ( !pLit1 && pLit2 )
00273                         pLit2 = pLit2->pVNext;
00274                 else
00275                         break;
00276         }
00277         return Result;
00278 }

void Fxu_Update ( Fxu_Matrix *  p,
Fxu_Single *  pSingle,
Fxu_Double *  pDouble 
)

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

Synopsis [Updates the matrix after selecting two divisors.]

Description []

SideEffects []

SeeAlso []

Definition at line 54 of file fxuUpdate.c.

00055 {
00056         Fxu_Cube * pCube, * pCubeNew;
00057         Fxu_Var * pVarC, * pVarD;
00058         Fxu_Var * pVar1, * pVar2;
00059 
00060     // consider trivial cases
00061     if ( pSingle == NULL )
00062     {
00063         assert( pDouble->Weight == Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble ) );
00064         Fxu_UpdateDouble( p );
00065         return;
00066     }
00067     if ( pDouble == NULL )
00068     {
00069         assert( pSingle->Weight == Fxu_HeapSingleReadMaxWeight( p->pHeapSingle ) );
00070         Fxu_UpdateSingle( p );
00071         return;
00072     }
00073 
00074     // get the variables of the single
00075     pVar1 = pSingle->pVar1;
00076     pVar2 = pSingle->pVar2;
00077 
00078     // remove the best double from the heap
00079     Fxu_HeapDoubleDelete( p->pHeapDouble, pDouble );
00080         // remove the best divisor from the table
00081         Fxu_ListTableDelDivisor( p, pDouble );
00082 
00083     // create two new columns (vars)
00084     Fxu_UpdateCreateNewVars( p, &pVarC, &pVarD, 1 );
00085     // create one new row (cube)
00086     pCubeNew = Fxu_MatrixAddCube( p, pVarD, 0 );
00087     pCubeNew->pFirst = pCubeNew;
00088     // set the first cube of the positive var
00089     pVarD->pFirst = pCubeNew;
00090 
00091     // start collecting the affected vars and cubes
00092     Fxu_MatrixRingCubesStart( p );
00093     Fxu_MatrixRingVarsStart( p );
00094     // add the vars
00095     Fxu_MatrixRingVarsAdd( p, pVar1 );
00096     Fxu_MatrixRingVarsAdd( p, pVar2 );
00097     // remove the literals and collect the affected cubes
00098     // remove the divisors associated with this cube
00099         // add to the affected cube the literal corresponding to the new column
00100         Fxu_UpdateMatrixSingleClean( p, pVar1, pVar2, pVarD );
00101         // replace each two cubes of the pair by one new cube
00102         // the new cube contains the base and the new literal
00103     Fxu_UpdateDoublePairs( p, pDouble, pVarC );
00104     // stop collecting the affected vars and cubes
00105     Fxu_MatrixRingCubesStop( p );
00106     Fxu_MatrixRingVarsStop( p );
00107 
00108     // add the literals to the new cube
00109     assert( pVar1->iVar < pVar2->iVar );
00110     assert( Fxu_SingleCountCoincidence( p, pVar1, pVar2 ) == 0 );
00111     Fxu_MatrixAddLiteral( p, pCubeNew, pVar1 );
00112     Fxu_MatrixAddLiteral( p, pCubeNew, pVar2 );
00113 
00114     // create new doubles; we cannot add them in the same loop
00115         // because we first have to create *all* new cubes for each node
00116     Fxu_MatrixForEachCubeInRing( p, pCube )
00117                 Fxu_UpdateAddNewDoubles( p, pCube );
00118     // update the singles after removing some literals
00119     Fxu_UpdateCleanOldSingles( p );
00120 
00121     // undo the temporary rings with cubes and vars
00122     Fxu_MatrixRingCubesUnmark( p );
00123     Fxu_MatrixRingVarsUnmark( p );
00124     // we should undo the rings before creating new singles
00125 
00126     // create new singles
00127     Fxu_UpdateAddNewSingles( p, pVarC );
00128     Fxu_UpdateAddNewSingles( p, pVarD );
00129 
00130         // recycle the divisor
00131         MEM_FREE_FXU( p, Fxu_Double, 1, pDouble );
00132         p->nDivs3++;
00133 }

void Fxu_UpdateDouble ( Fxu_Matrix *  p  ) 

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

Synopsis [Updates the matrix after accepting a double cube divisor.]

Description []

SideEffects []

SeeAlso []

Definition at line 216 of file fxuUpdate.c.

00217 {
00218     Fxu_Double * pDiv;
00219         Fxu_Cube * pCube, * pCubeNew1, * pCubeNew2;
00220         Fxu_Var * pVarC, * pVarD;
00221 
00222     // remove the best divisor from the heap
00223     pDiv = Fxu_HeapDoubleGetMax( p->pHeapDouble );
00224         // remove the best divisor from the table
00225         Fxu_ListTableDelDivisor( p, pDiv );
00226 
00227     // create two new columns (vars)
00228     Fxu_UpdateCreateNewVars( p, &pVarC, &pVarD, 2 );
00229     // create two new rows (cubes)
00230     pCubeNew1 = Fxu_MatrixAddCube( p, pVarD, 0 );
00231     pCubeNew1->pFirst = pCubeNew1;
00232     pCubeNew2 = Fxu_MatrixAddCube( p, pVarD, 1 );
00233     pCubeNew2->pFirst = pCubeNew1;
00234     // set the first cube
00235     pVarD->pFirst = pCubeNew1;
00236 
00237     // add the literals to the new cubes
00238     Fxu_UpdateMatrixDoubleCreateCubes( p, pCubeNew1, pCubeNew2, pDiv );
00239 
00240     // start collecting the affected cubes and vars
00241     Fxu_MatrixRingCubesStart( p );
00242     Fxu_MatrixRingVarsStart( p );
00243         // replace each two cubes of the pair by one new cube
00244         // the new cube contains the base and the new literal
00245     Fxu_UpdateDoublePairs( p, pDiv, pVarD );
00246     // stop collecting the affected cubes and vars
00247     Fxu_MatrixRingCubesStop( p );
00248     Fxu_MatrixRingVarsStop( p );
00249     
00250     // create new doubles; we cannot add them in the same loop
00251         // because we first have to create *all* new cubes for each node
00252     Fxu_MatrixForEachCubeInRing( p, pCube )
00253                 Fxu_UpdateAddNewDoubles( p, pCube );
00254     // update the singles after removing some literals
00255     Fxu_UpdateCleanOldSingles( p );
00256 
00257     // undo the temporary rings with cubes and vars
00258     Fxu_MatrixRingCubesUnmark( p );
00259     Fxu_MatrixRingVarsUnmark( p );
00260     // we should undo the rings before creating new singles
00261 
00262     // create new singles
00263     Fxu_UpdateAddNewSingles( p, pVarC );
00264     Fxu_UpdateAddNewSingles( p, pVarD );
00265 
00266     // recycle the divisor
00267         MEM_FREE_FXU( p, Fxu_Double, 1, pDiv );
00268         p->nDivs2++;
00269 }

void Fxu_UpdateSingle ( Fxu_Matrix *  p  ) 

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

Synopsis [Updates after accepting single cube divisor.]

Description []

SideEffects []

SeeAlso []

Definition at line 146 of file fxuUpdate.c.

00147 {
00148     Fxu_Single * pSingle;
00149         Fxu_Cube * pCube, * pCubeNew;
00150         Fxu_Var * pVarC, * pVarD;
00151         Fxu_Var * pVar1, * pVar2;
00152 
00153     // read the best divisor from the heap
00154     pSingle = Fxu_HeapSingleReadMax( p->pHeapSingle );
00155     // get the variables of this single-cube divisor
00156     pVar1 = pSingle->pVar1;
00157     pVar2 = pSingle->pVar2;
00158 
00159     // create two new columns (vars)
00160     Fxu_UpdateCreateNewVars( p, &pVarC, &pVarD, 1 );
00161     // create one new row (cube)
00162     pCubeNew = Fxu_MatrixAddCube( p, pVarD, 0 );
00163     pCubeNew->pFirst = pCubeNew;
00164     // set the first cube
00165     pVarD->pFirst = pCubeNew;
00166 
00167     // start collecting the affected vars and cubes
00168     Fxu_MatrixRingCubesStart( p );
00169     Fxu_MatrixRingVarsStart( p );
00170     // add the vars
00171     Fxu_MatrixRingVarsAdd( p, pVar1 );
00172     Fxu_MatrixRingVarsAdd( p, pVar2 );
00173     // remove the literals and collect the affected cubes
00174     // remove the divisors associated with this cube
00175         // add to the affected cube the literal corresponding to the new column
00176         Fxu_UpdateMatrixSingleClean( p, pVar1, pVar2, pVarD );
00177     // stop collecting the affected vars and cubes
00178     Fxu_MatrixRingCubesStop( p );
00179     Fxu_MatrixRingVarsStop( p );
00180 
00181     // add the literals to the new cube
00182     assert( pVar1->iVar < pVar2->iVar );
00183     assert( Fxu_SingleCountCoincidence( p, pVar1, pVar2 ) == 0 );
00184     Fxu_MatrixAddLiteral( p, pCubeNew, pVar1 );
00185     Fxu_MatrixAddLiteral( p, pCubeNew, pVar2 );
00186 
00187     // create new doubles; we cannot add them in the same loop
00188         // because we first have to create *all* new cubes for each node
00189     Fxu_MatrixForEachCubeInRing( p, pCube )
00190                 Fxu_UpdateAddNewDoubles( p, pCube );
00191     // update the singles after removing some literals
00192     Fxu_UpdateCleanOldSingles( p );
00193     // we should undo the rings before creating new singles
00194 
00195     // unmark the cubes
00196     Fxu_MatrixRingCubesUnmark( p );
00197     Fxu_MatrixRingVarsUnmark( p );
00198 
00199     // create new singles
00200     Fxu_UpdateAddNewSingles( p, pVarC );
00201     Fxu_UpdateAddNewSingles( p, pVarD );
00202         p->nDivs1++;
00203 }

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