fxuInt.h File Reference

#include "base/abc/abc.h"

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

Macros
#define	Fxu_Min(a, b)   ( ((a)<(b))? (a):(b) )
	MACRO DEFINITIONS ///. More...
#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 typedefABC_NAMESPACE_HEADER_START struct FxuMatrix	Fxu_Matrix
	INCLUDES ///. More...
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)
	FUNCTION DEFINITIONS ///. More...
void	Fxu_MemRecycle (Fxu_Matrix *p, char *pItem, int nBytes)
void	Fxu_MatrixPrint (FILE *pFile, Fxu_Matrix *p)
	DECLARATIONS ///. More...
void	Fxu_MatrixPrintDivisorProfile (FILE *pFile, Fxu_Matrix *p)
int	Fxu_Select (Fxu_Matrix *p, Fxu_Single **ppSingle, Fxu_Double **ppDouble)
	FUNCTION DEFINITIONS ///. More...
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)
	FUNCTION DEFINITIONS ///. More...
void	Fxu_UpdateDouble (Fxu_Matrix *p)
void	Fxu_UpdateSingle (Fxu_Matrix *p)
void	Fxu_PairCanonicize (Fxu_Cube **ppCube1, Fxu_Cube **ppCube2)
	FUNCTION DEFINITIONS ///. More...
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)
	FUNCTION DEFINITIONS ///. More...
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 ()
	DECLARATIONS ///. More...
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)
	DECLARATIONS ///. More...
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 ()
	FUNCTION DEFINITIONS ///. More...
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 ()
	FUNCTION DEFINITIONS ///. More...
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)

Macro Definition Documentation

#define Fxu_CubeForEachDivisor	(		Cube,
			Div
	)

Value:

for ( Div = (Cube)->lDivs.pHead;\
          Div;\
          Div = Div->pCNext )

Definition at line 352 of file fxuInt.h.

#define Fxu_CubeForEachLiteral	(		Cube,
			Lit
	)

Value:

for ( Lit = (Cube)->lLits.pHead;\
          Lit;\
          Lit = Lit->pHNext )

Definition at line 338 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 342 of file fxuInt.h.

#define Fxu_CubeForEachPair	(		pCube,
			pPair,
			i
	)

Value:

for ( i = 0;\
        i < pCube->pVar->nCubes && (((pPair) = (pCube)->pVar->ppPairs[(pCube)->iCube][i]), 1);\
        i++ )\
        if ( pPair == NULL ) {} else

Definition at line 368 of file fxuInt.h.

#define Fxu_DoubleForEachPair	(		Div,
			Pair
	)

Value:

for ( Pair = (Div)->lPairs.pHead;\
          Pair;\
          Pair = Pair->pDNext )

Definition at line 357 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 361 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 375 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 379 of file fxuInt.h.

#define Fxu_MatrixForEachCube	(		Matrix,
			Cube
	)

Value:

for ( Cube = (Matrix)->lCubes.pHead;\
          Cube;\
          Cube = Cube->pNext )

Definition at line 294 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 397 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 402 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 298 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 330 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 333 of file fxuInt.h.

#define Fxu_MatrixForEachSingle	(		Matrix,
			Single
	)

Value:

for ( Single = (Matrix)->lSingles.pHead;\
          Single;\
          Single = Single->pNext )

Definition at line 312 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 316 of file fxuInt.h.

#define Fxu_MatrixForEachVariable	(		Matrix,
			Var
	)

Value:

for ( Var = (Matrix)->lVars.pHead;\
          Var;\
          Var = Var->pNext )

Definition at line 303 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 307 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 407 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 412 of file fxuInt.h.

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

Definition at line 394 of file fxuInt.h.

#define Fxu_MatrixRingCubesReset

(

Matrix

)

(((Matrix)->pOrderCubes = NULL), ((Matrix)->ppTailCubes = NULL))

Definition at line 391 of file fxuInt.h.

#define Fxu_MatrixRingCubesStart

(

Matrix

)

(((Matrix)->ppTailCubes = &((Matrix)->pOrderCubes)), ((Matrix)->pOrderCubes = NULL))

Definition at line 385 of file fxuInt.h.

#define Fxu_MatrixRingCubesStop

(

Matrix

)

Definition at line 388 of file fxuInt.h.

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

Definition at line 395 of file fxuInt.h.

#define Fxu_MatrixRingVarsReset

(

Matrix

)

(((Matrix)->pOrderVars = NULL), ((Matrix)->ppTailVars = NULL))

Definition at line 392 of file fxuInt.h.

#define Fxu_MatrixRingVarsStart

(

Matrix

)

(((Matrix)->ppTailVars = &((Matrix)->pOrderVars)), ((Matrix)->pOrderVars = NULL))

Definition at line 386 of file fxuInt.h.

#define Fxu_MatrixRingVarsStop

(

Matrix

)

Definition at line 389 of file fxuInt.h.

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

Definition at line 284 of file fxuInt.h.

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

MACRO DEFINITIONS ///.

Definition at line 283 of file fxuInt.h.

#define Fxu_PairMaxCube

(

pPair

)

(((pPair)->iCube1 > (pPair)->iCube2)? (pPair)->pCube1: (pPair)->pCube2)

Definition at line 288 of file fxuInt.h.

#define Fxu_PairMaxCubeInt

(

pPair

)

(((pPair)->iCube1 > (pPair)->iCube2)? (pPair)->iCube1: (pPair)->iCube2)

Definition at line 290 of file fxuInt.h.

#define Fxu_PairMinCube

(

pPair

)

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

Definition at line 287 of file fxuInt.h.

#define Fxu_PairMinCubeInt

(

pPair

)

(((pPair)->iCube1 < (pPair)->iCube2)? (pPair)->iCube1: (pPair)->iCube2)

Definition at line 289 of file fxuInt.h.

#define Fxu_TableForEachDouble	(		Matrix,
			Key,
			Div
	)

Value:

for ( Div = (Matrix)->pTable[Key].pHead;\
          Div;\
          Div = Div->pNext )

Definition at line 321 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 325 of file fxuInt.h.

#define Fxu_VarForEachLiteral	(		Var,
			Lit
	)

Value:

for ( Lit = (Var)->lLits.pHead;\
          Lit;\
          Lit = Lit->pVNext )

Definition at line 347 of file fxuInt.h.

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

Definition at line 429 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 431 of file fxuInt.h.

Typedef Documentation

typedef struct FxuCube Fxu_Cube

Definition at line 66 of file fxuInt.h.

typedef struct FxuDouble Fxu_Double

Definition at line 72 of file fxuInt.h.

typedef struct FxuHeapDouble Fxu_HeapDouble

Definition at line 84 of file fxuInt.h.

typedef struct FxuHeapSingle Fxu_HeapSingle

Definition at line 85 of file fxuInt.h.

typedef struct FxuListCube Fxu_ListCube

Definition at line 76 of file fxuInt.h.

typedef struct FxuListDouble Fxu_ListDouble

Definition at line 80 of file fxuInt.h.

typedef struct FxuListLit Fxu_ListLit

Definition at line 78 of file fxuInt.h.

typedef struct FxuListPair Fxu_ListPair

Definition at line 79 of file fxuInt.h.

typedef struct FxuListSingle Fxu_ListSingle

Definition at line 81 of file fxuInt.h.

typedef struct FxuListVar Fxu_ListVar

Definition at line 77 of file fxuInt.h.

typedef struct FxuLit Fxu_Lit

Definition at line 68 of file fxuInt.h.

typedef typedefABC_NAMESPACE_HEADER_START struct FxuMatrix Fxu_Matrix

INCLUDES ///.

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

]PARAMETERS ///STRUCTURE DEFINITIONS ///

Definition at line 63 of file fxuInt.h.

typedef struct FxuPair Fxu_Pair

Definition at line 71 of file fxuInt.h.

typedef struct FxuSingle Fxu_Single

Definition at line 73 of file fxuInt.h.

typedef struct FxuVar Fxu_Var

Definition at line 67 of file fxuInt.h.

Function Documentation

void Fxu_HeapDoubleCheck

(

Fxu_HeapDouble *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 152 of file fxuHeapD.c.

{
    Fxu_Double * pDiv;
    Fxu_HeapDoubleForEachItem( p, pDiv )
    {
        assert( pDiv->HNum == p->i );
        Fxu_HeapDoubleCheckOne( p, pDiv );
    }
}

void Fxu_HeapDoubleCheckOne	(	Fxu_HeapDouble *	p,
		Fxu_Double *	pDiv
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 173 of file fxuHeapD.c.

{
    int Weight1, Weight2;
    if ( FXU_HEAP_DOUBLE_CHILD1_EXISTS(p,pDiv) )
    {
        Weight1 = FXU_HEAP_DOUBLE_WEIGHT(pDiv);
        Weight2 = FXU_HEAP_DOUBLE_WEIGHT( FXU_HEAP_DOUBLE_CHILD1(p,pDiv) );
        assert( Weight1 >= Weight2 );
    }
    if ( FXU_HEAP_DOUBLE_CHILD2_EXISTS(p,pDiv) )
    {
        Weight1 = FXU_HEAP_DOUBLE_WEIGHT(pDiv);
        Weight2 = FXU_HEAP_DOUBLE_WEIGHT( FXU_HEAP_DOUBLE_CHILD2(p,pDiv) );
        assert( Weight1 >= Weight2 );
    }
}

void Fxu_HeapDoubleDelete	(	Fxu_HeapDouble *	p,
		Fxu_Double *	pDiv
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 250 of file fxuHeapD.c.

{
    FXU_HEAP_DOUBLE_ASSERT(p,pDiv);
    // put the last entry to the deleted place
    // decrement the number of entries
    p->pTree[pDiv->HNum] = p->pTree[p->nItems--];
    p->pTree[pDiv->HNum]->HNum = pDiv->HNum;
    // move the top entry down if necessary
    Fxu_HeapDoubleUpdate( p, p->pTree[pDiv->HNum] );
    pDiv->HNum = 0;
}

Fxu_Double* Fxu_HeapDoubleGetMax

(

Fxu_HeapDouble *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 291 of file fxuHeapD.c.

{
    Fxu_Double * pDiv;
    if ( p->nItems == 0 )
        return NULL;
    // prepare the return value
    pDiv = p->pTree[1];
    pDiv->HNum = 0;
    // put the last entry on top
    // decrement the number of entries
    p->pTree[1] = p->pTree[p->nItems--];
    p->pTree[1]->HNum = 1;
    // move the top entry down if necessary
    Fxu_HeapDoubleMoveDn( p, p->pTree[1] );
    return pDiv;     
}

void Fxu_HeapDoubleInsert	(	Fxu_HeapDouble *	p,
		Fxu_Double *	pDiv
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 201 of file fxuHeapD.c.

{
    if ( p->nItems == p->nItemsAlloc )
        Fxu_HeapDoubleResize( p );
    // put the last entry to the last place and move up
    p->pTree[++p->nItems] = pDiv;
    pDiv->HNum = p->nItems;
    // move the last entry up if necessary
    Fxu_HeapDoubleMoveUp( p, pDiv );
}

void Fxu_HeapDoublePrint	(	FILE *	pFile,
		Fxu_HeapDouble *	p
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 117 of file fxuHeapD.c.

{
    Fxu_Double * pDiv;
    int Counter = 1;
    int Degree  = 1;

    Fxu_HeapDoubleCheck( p );
    fprintf( pFile, "The contents of the heap:\n" );
    fprintf( pFile, "Level %d:  ", Degree );
    Fxu_HeapDoubleForEachItem( p, pDiv )
    {
        assert( Counter == p->pTree[Counter]->HNum );
        fprintf( pFile, "%2d=%3d  ", Counter, FXU_HEAP_DOUBLE_WEIGHT(p->pTree[Counter]) );
        if ( ++Counter == (1 << Degree) )
        {
            fprintf( pFile, "\n" );
            Degree++;
            fprintf( pFile, "Level %d:  ", Degree );
        }
    }
    fprintf( pFile, "\n" );
    fprintf( pFile, "End of the heap printout.\n" );
}

Fxu_Double* Fxu_HeapDoubleReadMax

(

Fxu_HeapDouble *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 273 of file fxuHeapD.c.

{
    if ( p->nItems == 0 )
        return NULL;
    return p->pTree[1];  
}

int Fxu_HeapDoubleReadMaxWeight

(

Fxu_HeapDouble *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 319 of file fxuHeapD.c.

{
    if ( p->nItems == 0 )
        return -1;
    else
        return FXU_HEAP_DOUBLE_WEIGHT(p->pTree[1]);
}

Fxu_HeapDouble* Fxu_HeapDoubleStart

(

)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 58 of file fxuHeapD.c.

{
    Fxu_HeapDouble * p;
    p = ABC_ALLOC( Fxu_HeapDouble, 1 );
    memset( p, 0, sizeof(Fxu_HeapDouble) );
    p->nItems      = 0;
    p->nItemsAlloc = 10000;
    p->pTree       = ABC_ALLOC( Fxu_Double *, p->nItemsAlloc + 1 );
    p->pTree[0]    = NULL;
    return p;
}

void Fxu_HeapDoubleStop

(

Fxu_HeapDouble *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 99 of file fxuHeapD.c.

{
    ABC_FREE( p->pTree );
    ABC_FREE( p );
}

void Fxu_HeapDoubleUpdate	(	Fxu_HeapDouble *	p,
		Fxu_Double *	pDiv
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 223 of file fxuHeapD.c.

{
//printf( "Updating divisor %d.\n", pDiv->Num );

    FXU_HEAP_DOUBLE_ASSERT(p,pDiv);
    if ( FXU_HEAP_DOUBLE_PARENT_EXISTS(p,pDiv) && 
         FXU_HEAP_DOUBLE_WEIGHT(pDiv) > FXU_HEAP_DOUBLE_WEIGHT( FXU_HEAP_DOUBLE_PARENT(p,pDiv) ) )
        Fxu_HeapDoubleMoveUp( p, pDiv );
    else if ( FXU_HEAP_DOUBLE_CHILD1_EXISTS(p,pDiv) && 
        FXU_HEAP_DOUBLE_WEIGHT(pDiv) < FXU_HEAP_DOUBLE_WEIGHT( FXU_HEAP_DOUBLE_CHILD1(p,pDiv) ) )
        Fxu_HeapDoubleMoveDn( p, pDiv );
    else if ( FXU_HEAP_DOUBLE_CHILD2_EXISTS(p,pDiv) && 
        FXU_HEAP_DOUBLE_WEIGHT(pDiv) < FXU_HEAP_DOUBLE_WEIGHT( FXU_HEAP_DOUBLE_CHILD2(p,pDiv) ) )
        Fxu_HeapDoubleMoveDn( p, pDiv );
}

void Fxu_HeapSingleCheck

(

Fxu_HeapSingle *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 155 of file fxuHeapS.c.

{
    Fxu_Single * pSingle;
    Fxu_HeapSingleForEachItem( p, pSingle )
    {
        assert( pSingle->HNum == p->i );
        Fxu_HeapSingleCheckOne( p, pSingle );
    }
}

void Fxu_HeapSingleCheckOne	(	Fxu_HeapSingle *	p,
		Fxu_Single *	pSingle
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 176 of file fxuHeapS.c.

{
    int Weight1, Weight2;
    if ( FXU_HEAP_SINGLE_CHILD1_EXISTS(p,pSingle) )
    {
        Weight1 = FXU_HEAP_SINGLE_WEIGHT(pSingle);
        Weight2 = FXU_HEAP_SINGLE_WEIGHT( FXU_HEAP_SINGLE_CHILD1(p,pSingle) );
        assert( Weight1 >= Weight2 );
    }
    if ( FXU_HEAP_SINGLE_CHILD2_EXISTS(p,pSingle) )
    {
        Weight1 = FXU_HEAP_SINGLE_WEIGHT(pSingle);
        Weight2 = FXU_HEAP_SINGLE_WEIGHT( FXU_HEAP_SINGLE_CHILD2(p,pSingle) );
        assert( Weight1 >= Weight2 );
    }
}

void Fxu_HeapSingleDelete	(	Fxu_HeapSingle *	p,
		Fxu_Single *	pSingle
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 251 of file fxuHeapS.c.

{
    int Place = pSingle->HNum;
    FXU_HEAP_SINGLE_ASSERT(p,pSingle);
    // put the last entry to the deleted place
    // decrement the number of entries
    p->pTree[Place] = p->pTree[p->nItems--];
    p->pTree[Place]->HNum = Place;
    // move the top entry down if necessary
    Fxu_HeapSingleUpdate( p, p->pTree[Place] );
    pSingle->HNum = 0;
}

Fxu_Single* Fxu_HeapSingleGetMax

(

Fxu_HeapSingle *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 293 of file fxuHeapS.c.

{
    Fxu_Single * pSingle;
    if ( p->nItems == 0 )
        return NULL;
    // prepare the return value
    pSingle = p->pTree[1];
    pSingle->HNum = 0;
    // put the last entry on top
    // decrement the number of entries
    p->pTree[1] = p->pTree[p->nItems--];
    p->pTree[1]->HNum = 1;
    // move the top entry down if necessary
    Fxu_HeapSingleMoveDn( p, p->pTree[1] );
    return pSingle;  
}

void Fxu_HeapSingleInsert	(	Fxu_HeapSingle *	p,
		Fxu_Single *	pSingle
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 204 of file fxuHeapS.c.

{
    if ( p->nItems == p->nItemsAlloc )
        Fxu_HeapSingleResize( p );
    // put the last entry to the last place and move up
    p->pTree[++p->nItems] = pSingle;
    pSingle->HNum = p->nItems;
    // move the last entry up if necessary
    Fxu_HeapSingleMoveUp( p, pSingle );
}

void Fxu_HeapSinglePrint	(	FILE *	pFile,
		Fxu_HeapSingle *	p
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 120 of file fxuHeapS.c.

{
    Fxu_Single * pSingle;
    int Counter = 1;
    int Degree  = 1;

    Fxu_HeapSingleCheck( p );
    fprintf( pFile, "The contents of the heap:\n" );
    fprintf( pFile, "Level %d:  ", Degree );
    Fxu_HeapSingleForEachItem( p, pSingle )
    {
        assert( Counter == p->pTree[Counter]->HNum );
        fprintf( pFile, "%2d=%3d  ", Counter, FXU_HEAP_SINGLE_WEIGHT(p->pTree[Counter]) );
        if ( ++Counter == (1 << Degree) )
        {
            fprintf( pFile, "\n" );
            Degree++;
            fprintf( pFile, "Level %d:  ", Degree );
        }
    }
    fprintf( pFile, "\n" );
    fprintf( pFile, "End of the heap printout.\n" );
}

Fxu_Single* Fxu_HeapSingleReadMax

(

Fxu_HeapSingle *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 275 of file fxuHeapS.c.

{
    if ( p->nItems == 0 )
        return NULL;
    return p->pTree[1];
}

int Fxu_HeapSingleReadMaxWeight

(

Fxu_HeapSingle *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 321 of file fxuHeapS.c.

{
    if ( p->nItems == 0 )
        return -1;
    return FXU_HEAP_SINGLE_WEIGHT(p->pTree[1]);
}

Fxu_HeapSingle* Fxu_HeapSingleStart

(

)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 58 of file fxuHeapS.c.

{
    Fxu_HeapSingle * p;
    p = ABC_ALLOC( Fxu_HeapSingle, 1 );
    memset( p, 0, sizeof(Fxu_HeapSingle) );
    p->nItems      = 0;
    p->nItemsAlloc = 2000;
    p->pTree       = ABC_ALLOC( Fxu_Single *, p->nItemsAlloc + 10 );
    p->pTree[0]    = NULL;
    return p;
}

void Fxu_HeapSingleStop

(

Fxu_HeapSingle *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 99 of file fxuHeapS.c.

{
    int i;
    i = 0;
    ABC_FREE( p->pTree );
    i = 1;
    ABC_FREE( p );
}

void Fxu_HeapSingleUpdate	(	Fxu_HeapSingle *	p,
		Fxu_Single *	pSingle
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 226 of file fxuHeapS.c.

{
    FXU_HEAP_SINGLE_ASSERT(p,pSingle);
    if ( FXU_HEAP_SINGLE_PARENT_EXISTS(p,pSingle) && 
         FXU_HEAP_SINGLE_WEIGHT(pSingle) > FXU_HEAP_SINGLE_WEIGHT( FXU_HEAP_SINGLE_PARENT(p,pSingle) ) )
        Fxu_HeapSingleMoveUp( p, pSingle );
    else if ( FXU_HEAP_SINGLE_CHILD1_EXISTS(p,pSingle) && 
        FXU_HEAP_SINGLE_WEIGHT(pSingle) < FXU_HEAP_SINGLE_WEIGHT( FXU_HEAP_SINGLE_CHILD1(p,pSingle) ) )
        Fxu_HeapSingleMoveDn( p, pSingle );
    else if ( FXU_HEAP_SINGLE_CHILD2_EXISTS(p,pSingle) && 
        FXU_HEAP_SINGLE_WEIGHT(pSingle) < FXU_HEAP_SINGLE_WEIGHT( FXU_HEAP_SINGLE_CHILD2(p,pSingle) ) )
        Fxu_HeapSingleMoveDn( p, pSingle );
}

void Fxu_ListCubeAddLiteral	(	Fxu_Cube *	pCube,
		Fxu_Lit *	pLink
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 283 of file fxuList.c.

{
    Fxu_ListLit * pList = &(pCube->lLits);
    if ( pList->pHead == NULL )
    {
        pList->pHead = pLink;
        pList->pTail = pLink;
        pLink->pHPrev = NULL;
        pLink->pHNext = NULL;
    }
    else
    {
        pLink->pHNext = NULL;
        pList->pTail->pHNext = pLink;
        pLink->pHPrev = pList->pTail;
        pList->pTail = pLink;
    }
    pList->nItems++;
}

void Fxu_ListCubeDelLiteral	(	Fxu_Cube *	pCube,
		Fxu_Lit *	pLink
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 314 of file fxuList.c.

{
    Fxu_ListLit * pList = &(pCube->lLits);
    if ( pList->pHead == pLink )
         pList->pHead = pLink->pHNext;
    if ( pList->pTail == pLink )
         pList->pTail = pLink->pHPrev;
    if ( pLink->pHPrev )
         pLink->pHPrev->pHNext = pLink->pHNext;
    if ( pLink->pHNext )
         pLink->pHNext->pHPrev = pLink->pHPrev;
    pList->nItems--;
}

void Fxu_ListDoubleAddPairFirst	(	Fxu_Double *	pDiv,
		Fxu_Pair *	pLink
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 433 of file fxuList.c.

{
    Fxu_ListPair * pList = &pDiv->lPairs;
    if ( pList->pHead == NULL )
    {
        pList->pHead = pLink;
        pList->pTail = pLink;
        pLink->pDPrev = NULL;
        pLink->pDNext = NULL;
    }
    else
    {
        pLink->pDPrev = NULL;
        pList->pHead->pDPrev = pLink;
        pLink->pDNext = pList->pHead;
        pList->pHead = pLink;
    }
    pList->nItems++;
}

void Fxu_ListDoubleAddPairLast	(	Fxu_Double *	pDiv,
		Fxu_Pair *	pLink
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 402 of file fxuList.c.

{
    Fxu_ListPair * pList = &pDiv->lPairs;
    if ( pList->pHead == NULL )
    {
        pList->pHead = pLink;
        pList->pTail = pLink;
        pLink->pDPrev = NULL;
        pLink->pDNext = NULL;
    }
    else
    {
        pLink->pDNext = NULL;
        pList->pTail->pDNext = pLink;
        pLink->pDPrev = pList->pTail;
        pList->pTail = pLink;
    }
    pList->nItems++;
}

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 466 of file fxuList.c.

{
    Fxu_ListPair * pList = &pDiv->lPairs;
    assert( pSpot );
    assert( pSpot != pList->pTail );
    pLink->pDPrev = pSpot;
    pLink->pDNext = pSpot->pDNext;
    pLink->pDPrev->pDNext = pLink;
    pLink->pDNext->pDPrev = pLink;
    pList->nItems++;
}

void Fxu_ListDoubleDelPair	(	Fxu_Double *	pDiv,
		Fxu_Pair *	pLink
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 489 of file fxuList.c.

{
    Fxu_ListPair * pList = &pDiv->lPairs;
    if ( pList->pHead == pLink )
         pList->pHead = pLink->pDNext;
    if ( pList->pTail == pLink )
         pList->pTail = pLink->pDPrev;
    if ( pLink->pDPrev )
         pLink->pDPrev->pDNext = pLink->pDNext;
    if ( pLink->pDNext )
         pLink->pDNext->pDPrev = pLink->pDPrev;
    pList->nItems--;
}

void Fxu_ListMatrixAddCube	(	Fxu_Matrix *	p,
		Fxu_Cube *	pLink
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 104 of file fxuList.c.

{
    Fxu_ListCube * pList = &p->lCubes;
    if ( pList->pHead == NULL )
    {
        pList->pHead = pLink;
        pList->pTail = pLink;
        pLink->pPrev = NULL;
        pLink->pNext = NULL;
    }
    else
    {
        pLink->pNext = NULL;
        pList->pTail->pNext = pLink;
        pLink->pPrev = pList->pTail;
        pList->pTail = pLink;
    }
    pList->nItems++;
}

void Fxu_ListMatrixAddSingle	(	Fxu_Matrix *	p,
		Fxu_Single *	pLink
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 163 of file fxuList.c.

{
    Fxu_ListSingle * pList = &p->lSingles;
    if ( pList->pHead == NULL )
    {
        pList->pHead = pLink;
        pList->pTail = pLink;
        pLink->pPrev = NULL;
        pLink->pNext = NULL;
    }
    else
    {
        pLink->pNext = NULL;
        pList->pTail->pNext = pLink;
        pLink->pPrev = pList->pTail;
        pList->pTail = pLink;
    }
    pList->nItems++;
}

void Fxu_ListMatrixAddVariable	(	Fxu_Matrix *	p,
		Fxu_Var *	pLink
	)

DECLARATIONS ///.

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file fxuList.c.

{
    Fxu_ListVar * pList = &p->lVars;
    if ( pList->pHead == NULL )
    {
        pList->pHead = pLink;
        pList->pTail = pLink;
        pLink->pPrev = NULL;
        pLink->pNext = NULL;
    }
    else
    {
        pLink->pNext = NULL;
        pList->pTail->pNext = pLink;
        pLink->pPrev = pList->pTail;
        pList->pTail = pLink;
    }
    pList->nItems++;
}

void Fxu_ListMatrixDelCube	(	Fxu_Matrix *	p,
		Fxu_Cube *	pLink
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 135 of file fxuList.c.

{
    Fxu_ListCube * pList = &p->lCubes;
    if ( pList->pHead == pLink )
         pList->pHead = pLink->pNext;
    if ( pList->pTail == pLink )
         pList->pTail = pLink->pPrev;
    if ( pLink->pPrev )
         pLink->pPrev->pNext = pLink->pNext;
    if ( pLink->pNext )
         pLink->pNext->pPrev = pLink->pPrev;
    pList->nItems--;
}

void Fxu_ListMatrixDelSingle	(	Fxu_Matrix *	p,
		Fxu_Single *	pLink
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 194 of file fxuList.c.

{
    Fxu_ListSingle * pList = &p->lSingles;
    if ( pList->pHead == pLink )
         pList->pHead = pLink->pNext;
    if ( pList->pTail == pLink )
         pList->pTail = pLink->pPrev;
    if ( pLink->pPrev )
         pLink->pPrev->pNext = pLink->pNext;
    if ( pLink->pNext )
         pLink->pNext->pPrev = pLink->pPrev;
    pList->nItems--;
}

void Fxu_ListMatrixDelVariable	(	Fxu_Matrix *	p,
		Fxu_Var *	pLink
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 76 of file fxuList.c.

{
    Fxu_ListVar * pList = &p->lVars;
    if ( pList->pHead == pLink )
         pList->pHead = pLink->pNext;
    if ( pList->pTail == pLink )
         pList->pTail = pLink->pPrev;
    if ( pLink->pPrev )
         pLink->pPrev->pNext = pLink->pNext;
    if ( pLink->pNext )
         pLink->pNext->pPrev = pLink->pPrev;
    pList->nItems--;
}

void Fxu_ListTableAddDivisor	(	Fxu_Matrix *	p,
		Fxu_Double *	pLink
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 222 of file fxuList.c.

{
    Fxu_ListDouble * pList = &(p->pTable[pLink->Key]);
    if ( pList->pHead == NULL )
    {
        pList->pHead = pLink;
        pList->pTail = pLink;
        pLink->pPrev = NULL;
        pLink->pNext = NULL;
    }
    else
    {
        pLink->pNext = NULL;
        pList->pTail->pNext = pLink;
        pLink->pPrev = pList->pTail;
        pList->pTail = pLink;
    }
    pList->nItems++;
    p->nDivs++;
}

void Fxu_ListTableDelDivisor	(	Fxu_Matrix *	p,
		Fxu_Double *	pLink
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 254 of file fxuList.c.

{
    Fxu_ListDouble * pList = &(p->pTable[pLink->Key]);
    if ( pList->pHead == pLink )
         pList->pHead = pLink->pNext;
    if ( pList->pTail == pLink )
         pList->pTail = pLink->pPrev;
    if ( pLink->pPrev )
         pLink->pPrev->pNext = pLink->pNext;
    if ( pLink->pNext )
         pLink->pNext->pPrev = pLink->pPrev;
    pList->nItems--;
    p->nDivs--;
}

void Fxu_ListVarAddLiteral	(	Fxu_Var *	pVar,
		Fxu_Lit *	pLink
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 342 of file fxuList.c.

{
    Fxu_ListLit * pList = &(pVar->lLits);
    if ( pList->pHead == NULL )
    {
        pList->pHead = pLink;
        pList->pTail = pLink;
        pLink->pVPrev = NULL;
        pLink->pVNext = NULL;
    }
    else
    {
        pLink->pVNext = NULL;
        pList->pTail->pVNext = pLink;
        pLink->pVPrev = pList->pTail;
        pList->pTail = pLink;
    }
    pList->nItems++;
}

void Fxu_ListVarDelLiteral	(	Fxu_Var *	pVar,
		Fxu_Lit *	pLink
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 373 of file fxuList.c.

{
    Fxu_ListLit * pList = &(pVar->lLits);
    if ( pList->pHead == pLink )
         pList->pHead = pLink->pVNext;
    if ( pList->pTail == pLink )
         pList->pTail = pLink->pVPrev;
    if ( pLink->pVPrev )
         pLink->pVPrev->pVNext = pLink->pVNext;
    if ( pLink->pVNext )
         pLink->pVNext->pVPrev = pLink->pVPrev;
    pList->nItems--;
}

Fxu_Cube* Fxu_MatrixAddCube	(	Fxu_Matrix *	p,
		Fxu_Var *	pVar,
		int	iCube
	)

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

Synopsis [Adds a literal to the matrix.]

Description []

SideEffects []

SeeAlso []

Definition at line 183 of file fxuMatrix.c.

{
    Fxu_Cube * pCube;
    pCube = MEM_ALLOC_FXU( p, Fxu_Cube, 1 );
    memset( pCube, 0, sizeof(Fxu_Cube) );
    pCube->pVar  = pVar;
    pCube->iCube = iCube;
    Fxu_ListMatrixAddCube( p, pCube );
    return pCube;
}

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 301 of file fxuMatrix.c.

{
    Fxu_Pair * pPair;
    Fxu_Double * pDiv;
    int nBase, nLits1, nLits2;
    int fFound;
    unsigned Key;

    // canonicize the pair
    Fxu_PairCanonicize( &pCube1, &pCube2 );
    // compute the hash key
    Key = Fxu_PairHashKey( p, pCube1, pCube2, &nBase, &nLits1, &nLits2 );

    // create the cube pair
    pPair = Fxu_PairAlloc( p, pCube1, pCube2 );
    pPair->nBase  = nBase;
    pPair->nLits1 = nLits1;
    pPair->nLits2 = nLits2;

    // check if the divisor for this pair already exists
    fFound = 0;
    Key %= p->nTableSize;
    Fxu_TableForEachDouble( p, Key, pDiv )
    {
        if ( Fxu_PairCompare( pPair, pDiv->lPairs.pTail ) ) // they are equal
        {
            fFound = 1;
            break;
        }
    }

    if ( !fFound )
    {   // create the new divisor
        pDiv = MEM_ALLOC_FXU( p, Fxu_Double, 1 );
        memset( pDiv, 0, sizeof(Fxu_Double) );
        pDiv->Key = Key;
        // set the number of this divisor
        pDiv->Num = p->nDivsTotal++; // p->nDivs;
        // insert the divisor in the table
        Fxu_ListTableAddDivisor( p, pDiv );
        // set the initial cost of the divisor
        pDiv->Weight -= pPair->nLits1 + pPair->nLits2;
    }

    // link the pair to the cubes
    Fxu_PairAdd( pPair );
    // connect the pair and the divisor
    pPair->pDiv = pDiv;
    Fxu_ListDoubleAddPairLast( pDiv, pPair );   
    // update the max number of pairs in a divisor
//    if ( p->nPairsMax < pDiv->lPairs.nItems )
//        p->nPairsMax = pDiv->lPairs.nItems;
    // update the divisor's weight
    pDiv->Weight += pPair->nLits1 + pPair->nLits2 - 1 + pPair->nBase;
    if ( fFound ) // update the divisor in the heap
        Fxu_HeapDoubleUpdate( p->pHeapDouble, pDiv );
    else  // add the new divisor to the heap
        Fxu_HeapDoubleInsert( p->pHeapDouble, pDiv );
}

void Fxu_MatrixAddLiteral	(	Fxu_Matrix *	p,
		Fxu_Cube *	pCube,
		Fxu_Var *	pVar
	)

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

Synopsis [Adds a literal to the matrix.]

Description []

SideEffects []

SeeAlso []

Definition at line 205 of file fxuMatrix.c.

{
    Fxu_Lit * pLit;
    pLit = MEM_ALLOC_FXU( p, Fxu_Lit, 1 );
    memset( pLit, 0, sizeof(Fxu_Lit) );
    // insert the literal into two linked lists
    Fxu_ListCubeAddLiteral( pCube, pLit );
    Fxu_ListVarAddLiteral( pVar, pLit );
    // set the back pointers
    pLit->pCube = pCube;
    pLit->pVar  = pVar;
    pLit->iCube = pCube->iCube;
    pLit->iVar  = pVar->iVar;
    // increment the literal counter
    p->nEntries++;
}

void Fxu_MatrixAddSingle	(	Fxu_Matrix *	p,
		Fxu_Var *	pVar1,
		Fxu_Var *	pVar2,
		int	Weight
	)

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

Synopsis [Creates and adds a single cube divisor.]

Description []

SideEffects []

SeeAlso []

Definition at line 274 of file fxuMatrix.c.

{
    Fxu_Single * pSingle;
    assert( pVar1->iVar < pVar2->iVar );
    pSingle = MEM_ALLOC_FXU( p, Fxu_Single, 1 );
    memset( pSingle, 0, sizeof(Fxu_Single) );
    pSingle->Num = p->lSingles.nItems;
    pSingle->Weight = Weight;
    pSingle->HNum = 0;
    pSingle->pVar1 = pVar1;
    pSingle->pVar2 = pVar2;
    Fxu_ListMatrixAddSingle( p, pSingle );
    // add to the heap
    Fxu_HeapSingleInsert( p->pHeapSingle, pSingle );
}

Fxu_Var* Fxu_MatrixAddVar

(

Fxu_Matrix *

p

)

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

Synopsis [Adds a variable to the matrix.]

Description [This procedure always adds variables at the end of the matrix. It assigns the var's node and number. It adds the var to the linked list of all variables and to the table of all nodes.]

SideEffects []

SeeAlso []

Definition at line 161 of file fxuMatrix.c.

{
    Fxu_Var * pVar;
    pVar = MEM_ALLOC_FXU( p, Fxu_Var, 1 );
    memset( pVar, 0, sizeof(Fxu_Var) );
    pVar->iVar = p->lVars.nItems;
    p->ppVars[pVar->iVar] = pVar;
    Fxu_ListMatrixAddVariable( p, pVar );
    return pVar;
}

Fxu_Matrix* Fxu_MatrixAllocate

(

)

DECLARATIONS ///.

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

FileName [fxuMatrix.c]

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

Synopsis [Procedures to manipulate the sparse matrix.]

Author [MVSIS Group]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 43 of file fxuMatrix.c.

{
    Fxu_Matrix * p;
    p = ABC_ALLOC( Fxu_Matrix, 1 );
    memset( p, 0, sizeof(Fxu_Matrix) );
    p->nTableSize = Abc_PrimeCudd(10000);
    p->pTable = ABC_ALLOC( Fxu_ListDouble, p->nTableSize );
    memset( p->pTable, 0, sizeof(Fxu_ListDouble) * p->nTableSize );
#ifndef USE_SYSTEM_MEMORY_MANAGEMENT
    {
        // get the largest size in bytes for the following structures:
        // Fxu_Cube, Fxu_Var, Fxu_Lit, Fxu_Pair, Fxu_Double, Fxu_Single
        // (currently, Fxu_Var, Fxu_Pair, Fxu_Double take 10 machine words)
        int nSizeMax, nSizeCur;
        nSizeMax = -1;
        nSizeCur = sizeof(Fxu_Cube);
        if ( nSizeMax < nSizeCur )
             nSizeMax = nSizeCur;
        nSizeCur = sizeof(Fxu_Var);
        if ( nSizeMax < nSizeCur )
             nSizeMax = nSizeCur;
        nSizeCur = sizeof(Fxu_Lit);
        if ( nSizeMax < nSizeCur )
             nSizeMax = nSizeCur;
        nSizeCur = sizeof(Fxu_Pair);
        if ( nSizeMax < nSizeCur )
             nSizeMax = nSizeCur;
        nSizeCur = sizeof(Fxu_Double);
        if ( nSizeMax < nSizeCur )
             nSizeMax = nSizeCur;
        nSizeCur = sizeof(Fxu_Single);
        if ( nSizeMax < nSizeCur )
             nSizeMax = nSizeCur;
        p->pMemMan  = Extra_MmFixedStart( nSizeMax ); 
    }
#endif
    p->pHeapDouble = Fxu_HeapDoubleStart();
    p->pHeapSingle = Fxu_HeapSingleStart();
    p->vPairs = Vec_PtrAlloc( 100 );
    return p;
}

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 47 of file fxuSingle.c.

{
    Fxu_Var * pVar;
    Vec_Ptr_t * vSingles;
    int i, k;
    // set the weight limit
    p->nWeightLimit = 1 - fUse0;
    // iterate through columns in the matrix and collect single-cube divisors
    vSingles = Vec_PtrAlloc( 10000 );
    Fxu_MatrixForEachVariable( p, pVar )
        Fxu_MatrixComputeSinglesOneCollect( p, pVar, vSingles );
    p->nSingleTotal = Vec_PtrSize(vSingles) / 3;
    // check if divisors should be filtered
    if ( Vec_PtrSize(vSingles) > nSingleMax )
    {
        int * pWeigtCounts, nDivCount, Weight, i, c;;
        assert( Vec_PtrSize(vSingles) % 3 == 0 );
        // count how many divisors have the given weight
        pWeigtCounts = ABC_ALLOC( int, 1000 );
        memset( pWeigtCounts, 0, sizeof(int) * 1000 );
        for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 )
        {
            Weight = (int)(ABC_PTRUINT_T)Vec_PtrEntry(vSingles, i);
            if ( Weight >= 999 )
                pWeigtCounts[999]++;
            else
                pWeigtCounts[Weight]++;
        }
        // select the bound on the weight (above this bound, singles will be included)
        nDivCount = 0;
        for ( c = 999; c >= 0; c-- )
        {
            nDivCount += pWeigtCounts[c];
            if ( nDivCount >= nSingleMax )
                break;
        }
        ABC_FREE( pWeigtCounts );
        // collect singles with the given costs
        k = 0;
        for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 )
        {
            Weight = (int)(ABC_PTRUINT_T)Vec_PtrEntry(vSingles, i);
            if ( Weight < c )
                continue;
            Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-2) );
            Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-1) );
            Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i) );
            if ( k/3 == nSingleMax )
                break;
        }
        Vec_PtrShrink( vSingles, k );
        // adjust the weight limit
        p->nWeightLimit = c;
    }
    // collect the selected divisors
    assert( Vec_PtrSize(vSingles) % 3 == 0 );
    for ( i = 0; i < Vec_PtrSize(vSingles); i += 3 )
    {
        Fxu_MatrixAddSingle( p, 
            (Fxu_Var *)Vec_PtrEntry(vSingles,i), 
            (Fxu_Var *)Vec_PtrEntry(vSingles,i+1), 
            (int)(ABC_PTRUINT_T)Vec_PtrEntry(vSingles,i+2) );
    }
    Vec_PtrFree( vSingles );
}

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 184 of file fxuSingle.c.

{
    Fxu_Lit * pLitV, * pLitH;
    Fxu_Var * pVar2;
    int Coin;
    int WeightCur;

    // start collecting the affected vars
    Fxu_MatrixRingVarsStart( p );
    // go through all the literals of this variable
    for ( pLitV = pVar->lLits.pHead; pLitV; pLitV = pLitV->pVNext )
        // for this literal, go through all the horizontal literals
        for ( pLitH = pLitV->pHPrev; pLitH; pLitH = pLitH->pHPrev )
        {
            // get another variable
            pVar2 = pLitH->pVar;
            // skip the var if it is already used
            if ( pVar2->pOrder )
                continue;
            // skip the var if it belongs to the same node
//            if ( pValue2Node[pVar->iVar] == pValue2Node[pVar2->iVar] )
//                continue;
            // collect the var
            Fxu_MatrixRingVarsAdd( p, pVar2 );
        }
    // stop collecting the selected vars
    Fxu_MatrixRingVarsStop( p );

    // iterate through the selected vars
    Fxu_MatrixForEachVarInRing( p, pVar2 )
    {
        // count the coincidence
        Coin = Fxu_SingleCountCoincidence( p, pVar2, pVar );
        assert( Coin > 0 );
        // get the new weight
        WeightCur = Coin - 2;
        // peformance fix (August 24, 2007)
//        if ( WeightCur >= 0 )
//        Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur );
        if ( WeightCur >= p->nWeightLimit )
            Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur );
    }
    // unmark the vars
    Fxu_MatrixRingVarsUnmark( p );
}

void Fxu_MatrixDelDivisor	(	Fxu_Matrix *	p,
		Fxu_Double *	pDiv
	)

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

Synopsis [Deletes the divisor from the matrix.]

Description []

SideEffects []

SeeAlso []

Definition at line 233 of file fxuMatrix.c.

{
    // delete divisor from the table
    Fxu_ListTableDelDivisor( p, pDiv );
    // recycle the divisor
    MEM_FREE_FXU( p, Fxu_Double, 1, pDiv );
}

void Fxu_MatrixDelete

(

Fxu_Matrix *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 96 of file fxuMatrix.c.

{
    Fxu_HeapDoubleCheck( p->pHeapDouble );
    Fxu_HeapDoubleStop( p->pHeapDouble );
    Fxu_HeapSingleStop( p->pHeapSingle );

    // delete other things
#ifdef USE_SYSTEM_MEMORY_MANAGEMENT
    // this code is not needed when the custom memory manager is used
    {
        Fxu_Cube * pCube, * pCube2;
        Fxu_Var * pVar, * pVar2;
        Fxu_Lit * pLit, * pLit2;
        Fxu_Double * pDiv, * pDiv2;
        Fxu_Single * pSingle, * pSingle2;
        Fxu_Pair * pPair, * pPair2;
        int i;
        // delete the divisors
        Fxu_MatrixForEachDoubleSafe( p, pDiv, pDiv2, i )
        {
            Fxu_DoubleForEachPairSafe( pDiv, pPair, pPair2 )
                MEM_FREE_FXU( p, Fxu_Pair, 1, pPair );
            MEM_FREE_FXU( p, Fxu_Double, 1, pDiv );
        }
        Fxu_MatrixForEachSingleSafe( p, pSingle, pSingle2 )
            MEM_FREE_FXU( p, Fxu_Single, 1, pSingle );
        // delete the entries
        Fxu_MatrixForEachCube( p, pCube )
            Fxu_CubeForEachLiteralSafe( pCube, pLit, pLit2 )
                MEM_FREE_FXU( p, Fxu_Lit, 1, pLit );
        // delete the cubes
        Fxu_MatrixForEachCubeSafe( p, pCube, pCube2 )
            MEM_FREE_FXU( p, Fxu_Cube, 1, pCube );
        // delete the vars
        Fxu_MatrixForEachVariableSafe( p, pVar, pVar2 )
            MEM_FREE_FXU( p, Fxu_Var, 1, pVar );
    }
#else
    Extra_MmFixedStop( p->pMemMan );
#endif

    Vec_PtrFree( p->vPairs );
    ABC_FREE( p->pppPairs );
    ABC_FREE( p->ppPairs );
//    ABC_FREE( p->pPairsTemp );
    ABC_FREE( p->pTable );
    ABC_FREE( p->ppVars );
    ABC_FREE( p );
}

void Fxu_MatrixDelLiteral	(	Fxu_Matrix *	p,
		Fxu_Lit *	pLit
	)

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

Synopsis [Deletes the literal fromthe matrix.]

Description []

SideEffects []

SeeAlso []

Definition at line 252 of file fxuMatrix.c.

{
    // delete the literal
    Fxu_ListCubeDelLiteral( pLit->pCube, pLit );
    Fxu_ListVarDelLiteral( pLit->pVar, pLit );
    MEM_FREE_FXU( p, Fxu_Lit, 1, pLit );
    // increment the literal counter
    p->nEntries--;
}

void Fxu_MatrixPrint	(	FILE *	pFile,
		Fxu_Matrix *	p
	)

DECLARATIONS ///.

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 43 of file fxuPrint.c.

{
    Fxu_Var * pVar;
    Fxu_Cube * pCube;
    Fxu_Double * pDiv;
    Fxu_Single * pSingle;
    Fxu_Lit * pLit;
    Fxu_Pair * pPair;
    int i, LastNum;
    int fStdout;

    fStdout = 1;
    if ( pFile == NULL )
    {
        pFile = fopen( "matrix.txt", "w" );
        fStdout = 0;
    }

    fprintf( pFile, "Matrix has %d vars, %d cubes, %d literals, %d divisors.\n", 
        p->lVars.nItems, p->lCubes.nItems, p->nEntries, p->nDivs );
    fprintf( pFile, "Divisors selected so far: single = %d, double = %d.\n", 
        p->nDivs1, p->nDivs2 );
    fprintf( pFile, "\n" );

    // print the numbers on top of the matrix
    for ( i = 0; i < 12; i++ )
        fprintf( pFile, " " );
    Fxu_MatrixForEachVariable( p, pVar )
        fprintf( pFile, "%d", pVar->iVar % 10 );
    fprintf( pFile, "\n" );

    // print the rows
    Fxu_MatrixForEachCube( p, pCube )
    {
        fprintf( pFile, "%4d", pCube->iCube );
        fprintf( pFile, "  " );
        fprintf( pFile, "%4d", pCube->pVar->iVar );
        fprintf( pFile, "  " );

        // print the literals
        LastNum = -1;
        Fxu_CubeForEachLiteral( pCube, pLit )
        {
            for ( i = LastNum + 1; i < pLit->pVar->iVar; i++ )
                fprintf( pFile, "." );
            fprintf( pFile, "1" );
            LastNum = i;
        }
        for ( i = LastNum + 1; i < p->lVars.nItems; i++ )
            fprintf( pFile, "." );
        fprintf( pFile, "\n" );
    }
    fprintf( pFile, "\n" );

    // print the double-cube divisors
    fprintf( pFile, "The double divisors are:\n" );
    Fxu_MatrixForEachDouble( p, pDiv, i )
    {
        fprintf( pFile, "Divisor #%3d (lit=%d,%d) (w=%2d):  ", 
            pDiv->Num, pDiv->lPairs.pHead->nLits1, 
            pDiv->lPairs.pHead->nLits2, pDiv->Weight );
        Fxu_DoubleForEachPair( pDiv, pPair )
            fprintf( pFile, " <%d, %d> (b=%d)", 
                pPair->pCube1->iCube, pPair->pCube2->iCube, pPair->nBase );
        fprintf( pFile, "\n" );
    }
    fprintf( pFile, "\n" );

    // print the divisors associated with each cube
    fprintf( pFile, "The cubes are:\n" );
    Fxu_MatrixForEachCube( p, pCube )
    {
        fprintf( pFile, "Cube #%3d: ", pCube->iCube );
        if ( pCube->pVar->ppPairs )
        {
            Fxu_CubeForEachPair( pCube, pPair, i )
                fprintf( pFile, " <%d %d> (d=%d) (b=%d)", 
                    pPair->iCube1, pPair->iCube2, pPair->pDiv->Num, pPair->nBase );
        }
        fprintf( pFile, "\n" );
    }
    fprintf( pFile, "\n" );

    // print the single-cube divisors
    fprintf( pFile, "The single divisors are:\n" );
    Fxu_MatrixForEachSingle( p, pSingle )
    {
        fprintf( pFile, "Single-cube divisor #%5d: Var1 = %4d. Var2 = %4d. Weight = %2d\n", 
            pSingle->Num, pSingle->pVar1->iVar, pSingle->pVar2->iVar, pSingle->Weight );
    }
    fprintf( pFile, "\n" );

/*
    {
        int Index;
        fprintf( pFile, "Distribution of divisors in the hash table:\n" );
        for ( Index = 0; Index < p->nTableSize; Index++ )
            fprintf( pFile, " %d", p->pTable[Index].nItems );
        fprintf( pFile, "\n" );
    }
*/
    if ( !fStdout )
        fclose( pFile );
}

void Fxu_MatrixPrintDivisorProfile	(	FILE *	pFile,
		Fxu_Matrix *	p
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 159 of file fxuPrint.c.

{
    Fxu_Double * pDiv;
    int WeightMax;
    int * pProfile;
    int Counter1; // the number of -1 weight
    int CounterL; // the number of less than -1 weight
    int i;

    WeightMax = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
    pProfile = ABC_ALLOC( int, (WeightMax + 1) );
    memset( pProfile, 0, sizeof(int) * (WeightMax + 1) );

    Counter1 = 0;
    CounterL = 0;
    Fxu_MatrixForEachDouble( p, pDiv, i )
    {
        assert( pDiv->Weight <= WeightMax );
        if ( pDiv->Weight == -1 )
            Counter1++;
        else if ( pDiv->Weight < 0 )
            CounterL++;
        else
            pProfile[ pDiv->Weight ]++;
    }

    fprintf( pFile, "The double divisors profile:\n" );
    fprintf( pFile, "Weight  < -1 divisors = %6d\n", CounterL );
    fprintf( pFile, "Weight    -1 divisors = %6d\n", Counter1 );
    for ( i = 0; i <= WeightMax; i++ )
        if ( pProfile[i] )
            fprintf( pFile, "Weight   %3d divisors = %6d\n", i, pProfile[i] );
    fprintf( pFile, "End of divisor profile printout\n" );
    ABC_FREE( pProfile );
}

void Fxu_MatrixRingCubesUnmark

(

Fxu_Matrix *

p

)

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

Synopsis [Unmarks the cubes in the ring.]

Description []

SideEffects []

SeeAlso []

Definition at line 185 of file fxu.c.

{
    Fxu_Cube * pCube, * pCube2;
    // unmark the cubes
    Fxu_MatrixForEachCubeInRingSafe( p, pCube, pCube2 )
        pCube->pOrder = NULL;
    Fxu_MatrixRingCubesReset( p );
}

void Fxu_MatrixRingVarsUnmark

(

Fxu_Matrix *

p

)

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

Synopsis [Unmarks the vars in the ring.]

Description []

SideEffects []

SeeAlso []

Definition at line 206 of file fxu.c.

{
    Fxu_Var * pVar, * pVar2;
    // unmark the vars
    Fxu_MatrixForEachVarInRingSafe( p, pVar, pVar2 )
        pVar->pOrder = NULL;
    Fxu_MatrixRingVarsReset( p );
}

char* Fxu_MemFetch	(	Fxu_Matrix *	p,
		int	nBytes
	)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 227 of file fxu.c.

{
    s_MemoryTotal += nBytes;
    if ( s_MemoryPeak < s_MemoryTotal )
        s_MemoryPeak = s_MemoryTotal;
//    return ABC_ALLOC( char, nBytes );
    return Extra_MmFixedEntryFetch( p->pMemMan );
}

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 247 of file fxu.c.

{
    s_MemoryTotal -= nBytes;
//    ABC_FREE( pItem );
    Extra_MmFixedEntryRecycle( p->pMemMan, pItem );
}

void Fxu_PairAdd

(

Fxu_Pair *

pPair

)

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

Synopsis [Adds the pair to storage.]

Description []

SideEffects []

SeeAlso []

Definition at line 543 of file fxuPair.c.

{
    Fxu_Var * pVar;

    pVar = pPair->pCube1->pVar;
    assert( pVar == pPair->pCube2->pVar );

    pVar->ppPairs[pPair->iCube1][pPair->iCube2] = pPair;
    pVar->ppPairs[pPair->iCube2][pPair->iCube1] = pPair;
}

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 519 of file fxuPair.c.

{
    Fxu_Pair * pPair;
    assert( pCube1->pVar == pCube2->pVar );
    pPair = MEM_ALLOC_FXU( p, Fxu_Pair, 1 );
    memset( pPair, 0, sizeof(Fxu_Pair) );
    pPair->pCube1 = pCube1;
    pPair->pCube2 = pCube2;
    pPair->iCube1 = pCube1->iCube;
    pPair->iCube2 = pCube2->iCube;
    return pPair;
}

void Fxu_PairAllocStorage	(	Fxu_Var *	pVar,
		int	nCubes
	)

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

Synopsis [Allocates the storage for cubes pairs.]

Description []

SideEffects []

SeeAlso []

Definition at line 452 of file fxuPair.c.

{
    int k;
//    assert( pVar->nCubes == 0 );
    pVar->nCubes  = nCubes;
    // allocate memory for all the pairs
    pVar->ppPairs    = ABC_ALLOC( Fxu_Pair **, nCubes );
    pVar->ppPairs[0] = ABC_ALLOC( Fxu_Pair *,  nCubes * nCubes );
    memset( pVar->ppPairs[0], 0, sizeof(Fxu_Pair *) * nCubes * nCubes );
    for ( k = 1; k < nCubes; k++ )
        pVar->ppPairs[k] = pVar->ppPairs[k-1] + nCubes;
}

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 75 of file fxuPair.c.

{
    Fxu_Lit * pLit1, * pLit2;
    Fxu_Cube * pCubeTemp;

    // walk through the cubes to determine 
    // the one that has higher first variable
    pLit1 = (*ppCube1)->lLits.pHead;
    pLit2 = (*ppCube2)->lLits.pHead;
    while ( 1 )
    {
        if ( pLit1->iVar == pLit2->iVar )
        {
            pLit1 = pLit1->pHNext;
            pLit2 = pLit2->pHNext;
            continue;
        }
        assert( pLit1 && pLit2 ); // this is true if the covers are SCC-free
        if ( pLit1->iVar > pLit2->iVar )
        { // swap the cubes
            pCubeTemp = *ppCube1;
            *ppCube1  = *ppCube2;
            *ppCube2  = pCubeTemp;
        }
        break;
    }
}

void Fxu_PairClearStorage

(

Fxu_Cube *

pCube

)

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

Synopsis [Clears all pairs associated with this cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 476 of file fxuPair.c.

{
    Fxu_Var * pVar;
    int i;
    pVar = pCube->pVar;
    for ( i = 0; i < pVar->nCubes; i++ )
    {
        pVar->ppPairs[pCube->iCube][i] = NULL;
        pVar->ppPairs[i][pCube->iCube] = NULL;
    }
}

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 236 of file fxuPair.c.

{
    Fxu_Lit * pD1C1, * pD1C2;
    Fxu_Lit * pD2C1, * pD2C2;
    int TopVar1, TopVar2;
    int Code;

    if ( pPair1->nLits1 != pPair2->nLits1 )
        return 0;
    if ( pPair1->nLits2 != pPair2->nLits2 )
        return 0;

    pD1C1 = pPair1->pCube1->lLits.pHead;
    pD1C2 = pPair1->pCube2->lLits.pHead;

    pD2C1 = pPair2->pCube1->lLits.pHead;
    pD2C2 = pPair2->pCube2->lLits.pHead;

    Code  = pD1C1? 8: 0;
    Code |= pD1C2? 4: 0;
    Code |= pD2C1? 2: 0;
    Code |= pD2C2? 1: 0;
    assert( Code == 15 );

    while ( 1 )
    {
        switch ( Code )
        {
        case 0:  // -- --      NULL   NULL     NULL   NULL 
            return 1;
        case 1:  // -- -1      NULL   NULL     NULL   pD2C2
            return 0;
        case 2:  // -- 1-      NULL   NULL     pD2C1  NULL 
            return 0;
        case 3:  // -- 11      NULL   NULL     pD2C1  pD2C2
            if ( pD2C1->iVar != pD2C2->iVar )
                return 0;
            pD2C1 = pD2C1->pHNext;
            pD2C2 = pD2C2->pHNext;
            break;
        case 4:  // -1 --      NULL   pD1C2    NULL   NULL 
            return 0;
        case 5:  // -1 -1      NULL   pD1C2    NULL   pD2C2
            if ( pD1C2->iVar != pD2C2->iVar )
                return 0;
            pD1C2 = pD1C2->pHNext;
            pD2C2 = pD2C2->pHNext;
            break;
        case 6:  // -1 1-      NULL   pD1C2    pD2C1  NULL 
            return 0;
        case 7:  // -1 11      NULL   pD1C2    pD2C1  pD2C2
            TopVar2 = Fxu_Min( pD2C1->iVar, pD2C2->iVar );
            if ( TopVar2 == pD1C2->iVar )
            {
                if ( pD2C1->iVar <= pD2C2->iVar )
                    return 0;
                pD1C2 = pD1C2->pHNext;
                pD2C2 = pD2C2->pHNext;
            }
            else if ( TopVar2 < pD1C2->iVar )
            {
                if ( pD2C1->iVar != pD2C2->iVar )
                    return 0;
                pD2C1 = pD2C1->pHNext;
                pD2C2 = pD2C2->pHNext;
            }
            else
                return 0;
            break;
        case 8:  // 1- --      pD1C1  NULL     NULL   NULL 
            return 0;
        case 9:  // 1- -1      pD1C1  NULL     NULL   pD2C2
            return 0;
        case 10: // 1- 1-      pD1C1  NULL     pD2C1  NULL 
            if ( pD1C1->iVar != pD2C1->iVar )
                return 0;
            pD1C1 = pD1C1->pHNext;
            pD2C1 = pD2C1->pHNext;
            break;
        case 11: // 1- 11      pD1C1  NULL     pD2C1  pD2C2
            TopVar2 = Fxu_Min( pD2C1->iVar, pD2C2->iVar );
            if ( TopVar2 == pD1C1->iVar )
            {
                if ( pD2C1->iVar >= pD2C2->iVar )
                    return 0;
                pD1C1 = pD1C1->pHNext;
                pD2C1 = pD2C1->pHNext;
            }
            else if ( TopVar2 < pD1C1->iVar )
            {
                if ( pD2C1->iVar != pD2C2->iVar )
                    return 0;
                pD2C1 = pD2C1->pHNext;
                pD2C2 = pD2C2->pHNext;
            }
            else
                return 0;
            break;
        case 12: // 11 --      pD1C1  pD1C2    NULL   NULL 
            if ( pD1C1->iVar != pD1C2->iVar )
                return 0;
            pD1C1 = pD1C1->pHNext;
            pD1C2 = pD1C2->pHNext;
            break;
        case 13: // 11 -1      pD1C1  pD1C2    NULL   pD2C2
            TopVar1 = Fxu_Min( pD1C1->iVar, pD1C2->iVar );
            if ( TopVar1 == pD2C2->iVar )
            {
                if ( pD1C1->iVar <= pD1C2->iVar )
                    return 0;
                pD1C2 = pD1C2->pHNext;
                pD2C2 = pD2C2->pHNext;
            }
            else if ( TopVar1 < pD2C2->iVar )
            {
                if ( pD1C1->iVar != pD1C2->iVar )
                    return 0;
                pD1C1 = pD1C1->pHNext;
                pD1C2 = pD1C2->pHNext;
            }
            else
                return 0;
            break;
        case 14: // 11 1-      pD1C1  pD1C2    pD2C1  NULL 
            TopVar1 = Fxu_Min( pD1C1->iVar, pD1C2->iVar );
            if ( TopVar1 == pD2C1->iVar )
            {
                if ( pD1C1->iVar >= pD1C2->iVar )
                    return 0;
                pD1C1 = pD1C1->pHNext;
                pD2C1 = pD2C1->pHNext;
            }
            else if ( TopVar1 < pD2C1->iVar )
            {
                if ( pD1C1->iVar != pD1C2->iVar )
                    return 0;
                pD1C1 = pD1C1->pHNext;
                pD1C2 = pD1C2->pHNext;
            }
            else
                return 0;
            break;
        case 15: // 11 11      pD1C1  pD1C2    pD2C1  pD2C2
            TopVar1 = Fxu_Min( pD1C1->iVar, pD1C2->iVar );
            TopVar2 = Fxu_Min( pD2C1->iVar, pD2C2->iVar );
            if ( TopVar1 == TopVar2 )
            {
                if ( pD1C1->iVar == pD1C2->iVar )
                {
                    if ( pD2C1->iVar != pD2C2->iVar )
                        return 0;
                    pD1C1 = pD1C1->pHNext;
                    pD1C2 = pD1C2->pHNext;
                    pD2C1 = pD2C1->pHNext;
                    pD2C2 = pD2C2->pHNext;
                }
                else
                {
                    if ( pD2C1->iVar == pD2C2->iVar )
                        return 0;
                    if ( pD1C1->iVar < pD1C2->iVar )
                    {
                        if ( pD2C1->iVar > pD2C2->iVar )
                            return 0;
                        pD1C1 = pD1C1->pHNext;
                        pD2C1 = pD2C1->pHNext;
                    }
                    else
                    {
                        if ( pD2C1->iVar < pD2C2->iVar )
                            return 0;
                        pD1C2 = pD1C2->pHNext;
                        pD2C2 = pD2C2->pHNext;
                    }
                }
            }
            else if ( TopVar1 < TopVar2 )
            {
                if ( pD1C1->iVar != pD1C2->iVar )
                    return 0;
                pD1C1 = pD1C1->pHNext;
                pD1C2 = pD1C2->pHNext;
            }
            else 
            {
                if ( pD2C1->iVar != pD2C2->iVar )
                    return 0;
                pD2C1 = pD2C1->pHNext;
                pD2C2 = pD2C2->pHNext;
            }
            break;
        default:
            assert( 0 );
            break;
        }

        Code  = pD1C1? 8: 0;
        Code |= pD1C2? 4: 0;
        Code |= pD2C1? 2: 0;
        Code |= pD2C2? 1: 0;
    }
    return 1;
}

void Fxu_PairFreeStorage

(

Fxu_Var *

pVar

)

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

Synopsis [Clears all pairs associated with this cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 499 of file fxuPair.c.

{
    if ( pVar->ppPairs )
    {
        ABC_FREE( pVar->ppPairs[0] );
        ABC_FREE( pVar->ppPairs );
    }
}

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 164 of file fxuPair.c.

{
    int Offset1 = 100, Offset2 = 200;
    int nBase, nLits1, nLits2;
    Fxu_Lit * pLit1, * pLit2;
    unsigned Key;

    // compute the hash key
    Key    = 0;
    nLits1 = 0;
    nLits2 = 0;
    nBase  = 0;
    pLit1  = pCube1->lLits.pHead;
    pLit2  = pCube2->lLits.pHead;
    while ( 1 )
    {
        if ( pLit1 && pLit2 )
        {
            if ( pLit1->iVar == pLit2->iVar )
            { // ensure cube-free
                pLit1 = pLit1->pHNext;
                pLit2 = pLit2->pHNext;
                // add this literal to the base
                nBase++;
            }
            else if ( pLit1->iVar < pLit2->iVar )
            {
                Key  ^= s_Primes[Offset1+nLits1] * pLit1->iVar;
                pLit1 = pLit1->pHNext;
                nLits1++;
            }
            else
            {
                Key  ^= s_Primes[Offset2+nLits2] * pLit2->iVar;
                pLit2 = pLit2->pHNext;
                nLits2++;
            }
        }
        else if ( pLit1 && !pLit2 )
        {
            Key  ^= s_Primes[Offset1+nLits1] * pLit1->iVar;
            pLit1 = pLit1->pHNext;
            nLits1++;
        }
        else if ( !pLit1 && pLit2 )
        {
            Key  ^= s_Primes[Offset2+nLits2] * pLit2->iVar;
            pLit2 = pLit2->pHNext;
            nLits2++;
        }
        else
            break;
    }
    *pnBase  = nBase;
    *pnLits1 = nLits1;
    *pnLits2 = nLits2;
    return Key;
}

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 137 of file fxuPair.c.

{
    int Offset1 = 100, Offset2 = 200, i;
    unsigned Key;
    // compute the hash key
    Key = 0;
    for ( i = 0; i < nVarsC1; i++ )
        Key ^= s_Primes[Offset1+i] * piVarsC1[i];
    for ( i = 0; i < nVarsC2; i++ )
        Key ^= s_Primes[Offset2+i] * piVarsC2[i];
    return Key;
}

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 57 of file fxuSelect.c.

{
    // the top entries
    Fxu_Single * pSingles[MAX_SIZE_LOOKAHEAD] = {0};
    Fxu_Double * pDoubles[MAX_SIZE_LOOKAHEAD] = {0};
    // the complements
    Fxu_Double * pSCompl[MAX_SIZE_LOOKAHEAD] = {0};
    Fxu_Single * pDComplS[MAX_SIZE_LOOKAHEAD] = {0};
    Fxu_Double * pDComplD[MAX_SIZE_LOOKAHEAD] = {0};
    Fxu_Pair * pPair;
    int nSingles;
    int nDoubles;
    int i;
    int WeightBest;
    int WeightCur;
    int iNum, fBestS;

    // collect the top entries from the queues
    for ( nSingles = 0; nSingles < MAX_SIZE_LOOKAHEAD; nSingles++ )
    {
        pSingles[nSingles] = Fxu_HeapSingleGetMax( p->pHeapSingle );
        if ( pSingles[nSingles] == NULL )
            break;
    }
    // put them back into the queue
    for ( i = 0; i < nSingles; i++ )
        if ( pSingles[i] )
            Fxu_HeapSingleInsert( p->pHeapSingle, pSingles[i] );
        
    // the same for doubles
    // collect the top entries from the queues
    for ( nDoubles = 0; nDoubles < MAX_SIZE_LOOKAHEAD; nDoubles++ )
    {
        pDoubles[nDoubles] = Fxu_HeapDoubleGetMax( p->pHeapDouble );
        if ( pDoubles[nDoubles] == NULL )
            break;
    }
    // put them back into the queue
    for ( i = 0; i < nDoubles; i++ )
        if ( pDoubles[i] )
            Fxu_HeapDoubleInsert( p->pHeapDouble, pDoubles[i] );

    // for each single, find the complement double (if any)
    for ( i = 0; i < nSingles; i++ )
        if ( pSingles[i] )
            pSCompl[i] = Fxu_MatrixFindComplementSingle( p, pSingles[i] );

    // for each double, find the complement single or double (if any)
    for ( i = 0; i < nDoubles; i++ )
        if ( pDoubles[i] )
        {
            pPair = pDoubles[i]->lPairs.pHead;
            if ( pPair->nLits1 == 1 && pPair->nLits2 == 1 )
            {
                pDComplS[i] = Fxu_MatrixFindComplementDouble2( p, pDoubles[i] );
                pDComplD[i] = NULL;
            }
//            else if ( pPair->nLits1 == 2 && pPair->nLits2 == 2 )
//            {
//                pDComplS[i] = NULL;
//                pDComplD[i] = Fxu_MatrixFindComplementDouble4( p, pDoubles[i] );
//            }
            else
            {
                pDComplS[i] = NULL;
                pDComplD[i] = NULL;
            }
        }

    // select the best pair
    WeightBest = -1;
    for ( i = 0; i < nSingles; i++ )
    {
        WeightCur = pSingles[i]->Weight;
        if ( pSCompl[i] )
        {
            // add the weight of the double
            WeightCur += pSCompl[i]->Weight;
            // there is no need to implement this double, so...
            pPair      = pSCompl[i]->lPairs.pHead;
            WeightCur += pPair->nLits1 + pPair->nLits2;
        }
        if ( WeightBest < WeightCur )
        {
            WeightBest = WeightCur;
            *ppSingle = pSingles[i];
            *ppDouble = pSCompl[i];
            fBestS = 1;
            iNum = i;
        }
    }
    for ( i = 0; i < nDoubles; i++ )
    {
        WeightCur = pDoubles[i]->Weight;
        if ( pDComplS[i] )
        {
            // add the weight of the single
            WeightCur += pDComplS[i]->Weight;
            // there is no need to implement this double, so...
            pPair      = pDoubles[i]->lPairs.pHead;
            WeightCur += pPair->nLits1 + pPair->nLits2;
        }
        if ( WeightBest < WeightCur )
        {
            WeightBest = WeightCur;
            *ppSingle = pDComplS[i];
            *ppDouble = pDoubles[i];
            fBestS = 0;
            iNum = i;
        }
    }
/*
    // print the statistics
    printf( "\n" );
    for ( i = 0; i < nSingles; i++ )
    {
        printf( "Single #%d: Weight = %3d. ", i, pSingles[i]->Weight );
        printf( "Compl: " );
        if ( pSCompl[i] == NULL )
            printf( "None." );
        else
            printf( "D  Weight = %3d  Sum = %3d", 
                pSCompl[i]->Weight, pSCompl[i]->Weight + pSingles[i]->Weight );
        printf( "\n" );
    }
    printf( "\n" );
    for ( i = 0; i < nDoubles; i++ )
    {
        printf( "Double #%d: Weight = %3d. ", i, pDoubles[i]->Weight );
        printf( "Compl: " );
        if ( pDComplS[i] == NULL && pDComplD[i] == NULL )
            printf( "None." );
        else if ( pDComplS[i] )
            printf( "S  Weight = %3d  Sum = %3d", 
                pDComplS[i]->Weight, pDComplS[i]->Weight + pDoubles[i]->Weight );
        else if ( pDComplD[i] )
            printf( "D  Weight = %3d  Sum = %3d", 
                pDComplD[i]->Weight, pDComplD[i]->Weight + pDoubles[i]->Weight );
        printf( "\n" );
    }
    if ( WeightBest == -1 )
        printf( "Selected NONE\n" );
    else
    {
        printf( "Selected = %s.  ", fBestS? "S": "D" );
        printf( "Number = %d.  ", iNum );
        printf( "Weight = %d.\n", WeightBest );
    }
    printf( "\n" );
*/
    return WeightBest;
}

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 525 of file fxuSelect.c.

{
//    int * pValue2Node = p->pValue2Node;
    Fxu_Var * pVar1;
    Fxu_Var * pVar2, * pVarTemp;
    Fxu_Lit * pLitV, * pLitH;
    int Coin;
    int CounterAll;
    int CounterTest;
    int WeightCur;
    int WeightBest;

    CounterAll = 0;
    CounterTest = 0;

    WeightBest = -10;
    
    // iterate through the columns in the matrix
    Fxu_MatrixForEachVariable( p, pVar1 )
    {
        // start collecting the affected vars
        Fxu_MatrixRingVarsStart( p );

        // go through all the literals of this variable
        for ( pLitV = pVar1->lLits.pHead; pLitV; pLitV = pLitV->pVNext )
        {
            // for this literal, go through all the horizontal literals
            for ( pLitH = pLitV->pHNext; pLitH; pLitH = pLitH->pHNext )
            {
                // get another variable
                pVar2 = pLitH->pVar;
                CounterAll++;
                // skip the var if it is already used
                if ( pVar2->pOrder )
                    continue;
                // skip the var if it belongs to the same node
//                if ( pValue2Node[pVar1->iVar] == pValue2Node[pVar2->iVar] )
//                    continue;
                // collect the var
                Fxu_MatrixRingVarsAdd( p, pVar2 );
            }
        }
        // stop collecting the selected vars
        Fxu_MatrixRingVarsStop( p );

        // iterate through the selected vars
        Fxu_MatrixForEachVarInRing( p, pVar2 )
        {
            CounterTest++;

            // count the coincidence
            Coin = Fxu_SingleCountCoincidence( p, pVar1, pVar2 );
            assert( Coin > 0 );

            // get the new weight
            WeightCur = Coin - 2;

            // compare the weights
            if ( WeightBest < WeightCur )
            {
                WeightBest = WeightCur;
                *ppVar1 = pVar1;
                *ppVar2 = pVar2;
            }
        }
        // unmark the vars
        Fxu_MatrixForEachVarInRingSafe( p, pVar2, pVarTemp )
            pVar2->pOrder = NULL;
        Fxu_MatrixRingVarsReset( p );
    }

//    if ( WeightBest == WeightLimit )
//        return -1;
    return WeightBest;
}

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 241 of file fxuSingle.c.

{
    Fxu_Lit * pLit1, * pLit2;
    int Result;

    // compute the coincidence count
    Result = 0;
    pLit1  = pVar1->lLits.pHead;
    pLit2  = pVar2->lLits.pHead;
    while ( 1 )
    {
        if ( pLit1 && pLit2 )
        {
            if ( pLit1->pCube->pVar->iVar == pLit2->pCube->pVar->iVar )
            { // the variables are the same
                if ( pLit1->iCube == pLit2->iCube )
                { // the literals are the same
                    pLit1 = pLit1->pVNext;
                    pLit2 = pLit2->pVNext;
                    // add this literal to the coincidence
                    Result++;
                }
                else if ( pLit1->iCube < pLit2->iCube )
                    pLit1 = pLit1->pVNext;
                else
                    pLit2 = pLit2->pVNext;
            }
            else if ( pLit1->pCube->pVar->iVar < pLit2->pCube->pVar->iVar )
                pLit1 = pLit1->pVNext;
            else
                pLit2 = pLit2->pVNext;
        }
        else if ( pLit1 && !pLit2 )
            pLit1 = pLit1->pVNext;
        else if ( !pLit1 && pLit2 )
            pLit2 = pLit2->pVNext;
        else
            break;
    }
    return Result;
}

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 57 of file fxuUpdate.c.

{
    Fxu_Cube * pCube, * pCubeNew;
    Fxu_Var * pVarC, * pVarD;
    Fxu_Var * pVar1, * pVar2;

    // consider trivial cases
    if ( pSingle == NULL )
    {
        assert( pDouble->Weight == Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble ) );
        Fxu_UpdateDouble( p );
        return;
    }
    if ( pDouble == NULL )
    {
        assert( pSingle->Weight == Fxu_HeapSingleReadMaxWeight( p->pHeapSingle ) );
        Fxu_UpdateSingle( p );
        return;
    }

    // get the variables of the single
    pVar1 = pSingle->pVar1;
    pVar2 = pSingle->pVar2;

    // remove the best double from the heap
    Fxu_HeapDoubleDelete( p->pHeapDouble, pDouble );
    // remove the best divisor from the table
    Fxu_ListTableDelDivisor( p, pDouble );

    // create two new columns (vars)
    Fxu_UpdateCreateNewVars( p, &pVarC, &pVarD, 1 );
    // create one new row (cube)
    pCubeNew = Fxu_MatrixAddCube( p, pVarD, 0 );
    pCubeNew->pFirst = pCubeNew;
    // set the first cube of the positive var
    pVarD->pFirst = pCubeNew;

    // start collecting the affected vars and cubes
    Fxu_MatrixRingCubesStart( p );
    Fxu_MatrixRingVarsStart( p );
    // add the vars
    Fxu_MatrixRingVarsAdd( p, pVar1 );
    Fxu_MatrixRingVarsAdd( p, pVar2 );
    // remove the literals and collect the affected cubes
    // remove the divisors associated with this cube
    // add to the affected cube the literal corresponding to the new column
    Fxu_UpdateMatrixSingleClean( p, pVar1, pVar2, pVarD );
    // replace each two cubes of the pair by one new cube
    // the new cube contains the base and the new literal
    Fxu_UpdateDoublePairs( p, pDouble, pVarC );
    // stop collecting the affected vars and cubes
    Fxu_MatrixRingCubesStop( p );
    Fxu_MatrixRingVarsStop( p );

    // add the literals to the new cube
    assert( pVar1->iVar < pVar2->iVar );
    assert( Fxu_SingleCountCoincidence( p, pVar1, pVar2 ) == 0 );
    Fxu_MatrixAddLiteral( p, pCubeNew, pVar1 );
    Fxu_MatrixAddLiteral( p, pCubeNew, pVar2 );

    // create new doubles; we cannot add them in the same loop
    // because we first have to create *all* new cubes for each node
    Fxu_MatrixForEachCubeInRing( p, pCube )
        Fxu_UpdateAddNewDoubles( p, pCube );
    // update the singles after removing some literals
    Fxu_UpdateCleanOldSingles( p );

    // undo the temporary rings with cubes and vars
    Fxu_MatrixRingCubesUnmark( p );
    Fxu_MatrixRingVarsUnmark( p );
    // we should undo the rings before creating new singles

    // create new singles
    Fxu_UpdateAddNewSingles( p, pVarC );
    Fxu_UpdateAddNewSingles( p, pVarD );

    // recycle the divisor
    MEM_FREE_FXU( p, Fxu_Double, 1, pDouble );
    p->nDivs3++;
}

void Fxu_UpdateDouble

(

Fxu_Matrix *

p

)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 219 of file fxuUpdate.c.

{
    Fxu_Double * pDiv;
    Fxu_Cube * pCube, * pCubeNew1, * pCubeNew2;
    Fxu_Var * pVarC, * pVarD;

    // remove the best divisor from the heap
    pDiv = Fxu_HeapDoubleGetMax( p->pHeapDouble );
    // remove the best divisor from the table
    Fxu_ListTableDelDivisor( p, pDiv );

    // create two new columns (vars)
    Fxu_UpdateCreateNewVars( p, &pVarC, &pVarD, 2 );
    // create two new rows (cubes)
    pCubeNew1 = Fxu_MatrixAddCube( p, pVarD, 0 );
    pCubeNew1->pFirst = pCubeNew1;
    pCubeNew2 = Fxu_MatrixAddCube( p, pVarD, 1 );
    pCubeNew2->pFirst = pCubeNew1;
    // set the first cube
    pVarD->pFirst = pCubeNew1;

    // add the literals to the new cubes
    Fxu_UpdateMatrixDoubleCreateCubes( p, pCubeNew1, pCubeNew2, pDiv );

    // start collecting the affected cubes and vars
    Fxu_MatrixRingCubesStart( p );
    Fxu_MatrixRingVarsStart( p );
    // replace each two cubes of the pair by one new cube
    // the new cube contains the base and the new literal
    Fxu_UpdateDoublePairs( p, pDiv, pVarD );
    // stop collecting the affected cubes and vars
    Fxu_MatrixRingCubesStop( p );
    Fxu_MatrixRingVarsStop( p );
    
    // create new doubles; we cannot add them in the same loop
    // because we first have to create *all* new cubes for each node
    Fxu_MatrixForEachCubeInRing( p, pCube )
        Fxu_UpdateAddNewDoubles( p, pCube );
    // update the singles after removing some literals
    Fxu_UpdateCleanOldSingles( p );

    // undo the temporary rings with cubes and vars
    Fxu_MatrixRingCubesUnmark( p );
    Fxu_MatrixRingVarsUnmark( p );
    // we should undo the rings before creating new singles

    // create new singles
    Fxu_UpdateAddNewSingles( p, pVarC );
    Fxu_UpdateAddNewSingles( p, pVarD );

    // recycle the divisor
    MEM_FREE_FXU( p, Fxu_Double, 1, pDiv );
    p->nDivs2++;
}

void Fxu_UpdateSingle

(

Fxu_Matrix *

p

)

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

Synopsis [Updates after accepting single cube divisor.]

Description []

SideEffects []

SeeAlso []

Definition at line 149 of file fxuUpdate.c.

{
    Fxu_Single * pSingle;
    Fxu_Cube * pCube, * pCubeNew;
    Fxu_Var * pVarC, * pVarD;
    Fxu_Var * pVar1, * pVar2;

    // read the best divisor from the heap
    pSingle = Fxu_HeapSingleReadMax( p->pHeapSingle );
    // get the variables of this single-cube divisor
    pVar1 = pSingle->pVar1;
    pVar2 = pSingle->pVar2;

    // create two new columns (vars)
    Fxu_UpdateCreateNewVars( p, &pVarC, &pVarD, 1 );
    // create one new row (cube)
    pCubeNew = Fxu_MatrixAddCube( p, pVarD, 0 );
    pCubeNew->pFirst = pCubeNew;
    // set the first cube
    pVarD->pFirst = pCubeNew;

    // start collecting the affected vars and cubes
    Fxu_MatrixRingCubesStart( p );
    Fxu_MatrixRingVarsStart( p );
    // add the vars
    Fxu_MatrixRingVarsAdd( p, pVar1 );
    Fxu_MatrixRingVarsAdd( p, pVar2 );
    // remove the literals and collect the affected cubes
    // remove the divisors associated with this cube
    // add to the affected cube the literal corresponding to the new column
    Fxu_UpdateMatrixSingleClean( p, pVar1, pVar2, pVarD );
    // stop collecting the affected vars and cubes
    Fxu_MatrixRingCubesStop( p );
    Fxu_MatrixRingVarsStop( p );

    // add the literals to the new cube
    assert( pVar1->iVar < pVar2->iVar );
    assert( Fxu_SingleCountCoincidence( p, pVar1, pVar2 ) == 0 );
    Fxu_MatrixAddLiteral( p, pCubeNew, pVar1 );
    Fxu_MatrixAddLiteral( p, pCubeNew, pVar2 );

    // create new doubles; we cannot add them in the same loop
    // because we first have to create *all* new cubes for each node
    Fxu_MatrixForEachCubeInRing( p, pCube )
        Fxu_UpdateAddNewDoubles( p, pCube );
    // update the singles after removing some literals
    Fxu_UpdateCleanOldSingles( p );
    // we should undo the rings before creating new singles

    // unmark the cubes
    Fxu_MatrixRingCubesUnmark( p );
    Fxu_MatrixRingVarsUnmark( p );

    // create new singles
    Fxu_UpdateAddNewSingles( p, pVarC );
    Fxu_UpdateAddNewSingles( p, pVarD );
    p->nDivs1++;
}