fxuInt.h File Reference

#include "base/abc/abc.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.

Classes
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)
	MACRO DEFINITIONS ///.
#define	Fxu_Max(a, b)
#define	Fxu_PairMinCube(pPair)
#define	Fxu_PairMaxCube(pPair)
#define	Fxu_PairMinCubeInt(pPair)
#define	Fxu_PairMaxCubeInt(pPair)
#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)
#define	Fxu_MatrixRingVarsStart( Matrix)
#define	Fxu_MatrixRingCubesStop( Matrix)
#define	Fxu_MatrixRingVarsStop( Matrix)
#define	Fxu_MatrixRingCubesReset(Matrix)
#define	Fxu_MatrixRingVarsReset( Matrix)
#define	Fxu_MatrixRingCubesAdd(Matrix, Cube)
#define	Fxu_MatrixRingVarsAdd( Matrix, Var)
#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)
#define	MEM_FREE_FXU(Manager, Type, Size, Pointer)

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct FxuMatrix	Fxu_Matrix
	INCLUDES ///.
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 ///.
void	Fxu_MemRecycle (Fxu_Matrix *p, char *pItem, int nBytes)
void	Fxu_MatrixPrint (FILE *pFile, Fxu_Matrix *p)
	DECLARATIONS ///.
void	Fxu_MatrixPrintDivisorProfile (FILE *pFile, Fxu_Matrix *p)
int	Fxu_Select (Fxu_Matrix *p, Fxu_Single **ppSingle, Fxu_Double **ppDouble)
	FUNCTION DEFINITIONS ///.
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 ///.
void	Fxu_UpdateDouble (Fxu_Matrix *p)
void	Fxu_UpdateSingle (Fxu_Matrix *p)
void	Fxu_PairCanonicize (Fxu_Cube **ppCube1, Fxu_Cube **ppCube2)
	FUNCTION DEFINITIONS ///.
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 ///.
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 ///.
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 ///.
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 ///.
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 ///.
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

Fxu_CubeForEachDivisor

#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_CubeForEachDivisor( Cube, Div )\
    for ( Div = (Cube)->lDivs.pHead;\
          Div;\
          Div = Div->pCNext )

Fxu_CubeForEachLiteral

#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_CubeForEachLiteral( Cube, Lit )\
    for ( Lit = (Cube)->lLits.pHead;\
          Lit;\
          Lit = Lit->pHNext )

Fxu_CubeForEachLiteralSafe

#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_CubeForEachLiteralSafe( Cube, Lit, Lit2 )\
    for ( Lit = (Cube)->lLits.pHead, Lit2 = (Lit? Lit->pHNext: NULL);\
          Lit;\
          Lit = Lit2, Lit2 = (Lit? Lit->pHNext: NULL) )

Fxu_CubeForEachPair

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

Fxu_DoubleForEachPair

#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_DoubleForEachPair( Div, Pair )\
    for ( Pair = (Div)->lPairs.pHead;\
          Pair;\
          Pair = Pair->pDNext )

Fxu_DoubleForEachPairSafe

#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_DoubleForEachPairSafe( Div, Pair, Pair2 )\
    for ( Pair = (Div)->lPairs.pHead, Pair2 = (Pair? Pair->pDNext: NULL);\
          Pair;\
          Pair = Pair2, Pair2 = (Pair? Pair->pDNext: NULL) )

Fxu_HeapDoubleForEachItem

#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_HeapDoubleForEachItem( Heap, Div )\
    for ( Heap->i = 1;\
          Heap->i <= Heap->nItems && (Div = Heap->pTree[Heap->i]);\
          Heap->i++ )

Fxu_HeapSingleForEachItem

#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_HeapSingleForEachItem( Heap, Single )\
    for ( Heap->i = 1;\
          Heap->i <= Heap->nItems && (Single = Heap->pTree[Heap->i]);\
          Heap->i++ )

Fxu_MatrixForEachCube

#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_MatrixForEachCube( Matrix, Cube )\
    for ( Cube = (Matrix)->lCubes.pHead;\
          Cube;\
          Cube = Cube->pNext )

Fxu_MatrixForEachCubeInRing

#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_MatrixForEachCubeInRing( Matrix, Cube )\
    if ( (Matrix)->pOrderCubes )\
    for ( Cube = (Matrix)->pOrderCubes;\
          Cube != (Fxu_Cube *)1;\
          Cube = Cube->pOrder )

Fxu_MatrixForEachCubeInRingSafe

#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_MatrixForEachCubeInRingSafe( Matrix, Cube, Cube2 )\
    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) )

Fxu_MatrixForEachCubeSafe

#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_MatrixForEachCubeSafe( Matrix, Cube, Cube2 )\
    for ( Cube = (Matrix)->lCubes.pHead, Cube2 = (Cube? Cube->pNext: NULL);\
          Cube;\
          Cube = Cube2, Cube2 = (Cube? Cube->pNext: NULL) )

Fxu_MatrixForEachDouble

#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_MatrixForEachDouble( Matrix, Div, Index )\
    for ( Index = 0; Index < (Matrix)->nTableSize; Index++ )\
        Fxu_TableForEachDouble( Matrix, Index, Div )

Fxu_MatrixForEachDoubleSafe

#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_MatrixForEachDoubleSafe( Matrix, Div, Div2, Index )\
    for ( Index = 0; Index < (Matrix)->nTableSize; Index++ )\
        Fxu_TableForEachDoubleSafe( Matrix, Index, Div, Div2 )

Fxu_MatrixForEachSingle

#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_MatrixForEachSingle( Matrix, Single )\
    for ( Single = (Matrix)->lSingles.pHead;\
          Single;\
          Single = Single->pNext )

Fxu_MatrixForEachSingleSafe

#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_MatrixForEachSingleSafe( Matrix, Single, Single2 )\
    for ( Single = (Matrix)->lSingles.pHead, Single2 = (Single? Single->pNext: NULL);\
          Single;\
          Single = Single2, Single2 = (Single? Single->pNext: NULL) )

Fxu_MatrixForEachVariable

#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_MatrixForEachVariable( Matrix, Var )\
    for ( Var = (Matrix)->lVars.pHead;\
          Var;\
          Var = Var->pNext )

Fxu_MatrixForEachVariableSafe

#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_MatrixForEachVariableSafe( Matrix, Var, Var2 )\
    for ( Var = (Matrix)->lVars.pHead, Var2 = (Var? Var->pNext: NULL);\
          Var;\
          Var = Var2, Var2 = (Var? Var->pNext: NULL) )

Fxu_MatrixForEachVarInRing

#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_MatrixForEachVarInRing( Matrix, Var )\
    if ( (Matrix)->pOrderVars )\
    for ( Var = (Matrix)->pOrderVars;\
          Var != (Fxu_Var *)1;\
          Var = Var->pOrder )

Fxu_MatrixForEachVarInRingSafe

#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_MatrixForEachVarInRingSafe( Matrix, Var, Var2 )\
    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) )

Fxu_MatrixRingCubesAdd

#define Fxu_MatrixRingCubesAdd	(		Matrix,
			Cube )

Value:

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

Definition at line 394 of file fxuInt.h.

Fxu_MatrixRingCubesReset

#define Fxu_MatrixRingCubesReset

(

Matrix

)

Value:

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

Definition at line 391 of file fxuInt.h.

Fxu_MatrixRingCubesStart

#define Fxu_MatrixRingCubesStart

(

Matrix

)

Value:

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

Definition at line 385 of file fxuInt.h.

Fxu_MatrixRingCubesStop

#define Fxu_MatrixRingCubesStop

(

Matrix

)

Definition at line 388 of file fxuInt.h.

Fxu_MatrixRingVarsAdd

#define Fxu_MatrixRingVarsAdd	(		Matrix,
			Var )

Value:

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

Definition at line 395 of file fxuInt.h.

Fxu_MatrixRingVarsReset

#define Fxu_MatrixRingVarsReset

(

Matrix

)

Value:

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

Definition at line 392 of file fxuInt.h.

Fxu_MatrixRingVarsStart

#define Fxu_MatrixRingVarsStart

(

Matrix

)

Value:

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

Definition at line 386 of file fxuInt.h.

Fxu_MatrixRingVarsStop

#define Fxu_MatrixRingVarsStop

(

Matrix

)

Definition at line 389 of file fxuInt.h.

Fxu_Max

#define Fxu_Max	(		a,
			b )

Value:

( ((a)>(b))? (a):(b) )

Definition at line 284 of file fxuInt.h.

Fxu_Min

#define Fxu_Min	(		a,
			b )

Value:

( ((a)<(b))? (a):(b) )

MACRO DEFINITIONS ///.

Definition at line 283 of file fxuInt.h.

Fxu_PairMaxCube

#define Fxu_PairMaxCube

(

pPair

)

Value:

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

Definition at line 288 of file fxuInt.h.

Fxu_PairMaxCubeInt

#define Fxu_PairMaxCubeInt

(

pPair

)

Value:

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

Definition at line 290 of file fxuInt.h.

Fxu_PairMinCube

#define Fxu_PairMinCube

(

pPair

)

Value:

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

Definition at line 287 of file fxuInt.h.

Fxu_PairMinCubeInt

#define Fxu_PairMinCubeInt

(

pPair

)

Value:

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

Definition at line 289 of file fxuInt.h.

Fxu_TableForEachDouble

#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_TableForEachDouble( Matrix, Key, Div )\
    for ( Div = (Matrix)->pTable[Key].pHead;\
          Div;\
          Div = Div->pNext )

Fxu_TableForEachDoubleSafe

#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_TableForEachDoubleSafe( Matrix, Key, Div, Div2 )\
    for ( Div = (Matrix)->pTable[Key].pHead, Div2 = (Div? Div->pNext: NULL);\
          Div;\
          Div = Div2, Div2 = (Div? Div->pNext: NULL) )

Fxu_VarForEachLiteral

#define Fxu_VarForEachLiteral	(		Var,
			Lit )

Value:

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

Definition at line 347 of file fxuInt.h.

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

MEM_ALLOC_FXU

#define MEM_ALLOC_FXU	(		Manager,
			Type,
			Size )

Value:

        ((Type *)Fxu_MemFetch( Manager, (Size) * sizeof(Type) ))

Definition at line 429 of file fxuInt.h.

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

MEM_FREE_FXU

#define MEM_FREE_FXU	(		Manager,
			Type,
			Size,
			Pointer )

Value:

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

Definition at line 431 of file fxuInt.h.

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

Typedef Documentation

Fxu_Cube

typedef struct FxuCube Fxu_Cube

Definition at line 66 of file fxuInt.h.

Fxu_Double

typedef struct FxuDouble Fxu_Double

Definition at line 72 of file fxuInt.h.

Fxu_HeapDouble

typedef struct FxuHeapDouble Fxu_HeapDouble

Definition at line 84 of file fxuInt.h.

Fxu_HeapSingle

typedef struct FxuHeapSingle Fxu_HeapSingle

Definition at line 85 of file fxuInt.h.

Fxu_ListCube

typedef struct FxuListCube Fxu_ListCube

Definition at line 76 of file fxuInt.h.

Fxu_ListDouble

typedef struct FxuListDouble Fxu_ListDouble

Definition at line 80 of file fxuInt.h.

Fxu_ListLit

typedef struct FxuListLit Fxu_ListLit

Definition at line 78 of file fxuInt.h.

Fxu_ListPair

typedef struct FxuListPair Fxu_ListPair

Definition at line 79 of file fxuInt.h.

Fxu_ListSingle

typedef struct FxuListSingle Fxu_ListSingle

Definition at line 81 of file fxuInt.h.

Fxu_ListVar

typedef struct FxuListVar Fxu_ListVar

Definition at line 77 of file fxuInt.h.

Fxu_Lit

typedef struct FxuLit Fxu_Lit

Definition at line 68 of file fxuInt.h.

Fxu_Matrix

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.

Fxu_Pair

typedef struct FxuPair Fxu_Pair

Definition at line 71 of file fxuInt.h.

Fxu_Single

typedef struct FxuSingle Fxu_Single

Definition at line 73 of file fxuInt.h.

Fxu_Var

typedef struct FxuVar Fxu_Var

Definition at line 67 of file fxuInt.h.

Function Documentation

Fxu_HeapDoubleCheck()

void Fxu_HeapDoubleCheck ( Fxu_HeapDouble * p )

extern

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 );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fxu_HeapDoubleCheckOne()

void Fxu_HeapDoubleCheckOne ( Fxu_HeapDouble * p, Fxu_Double * pDiv )

extern

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 );
    }
}

Here is the caller graph for this function:

Fxu_HeapDoubleDelete()

void Fxu_HeapDoubleDelete ( Fxu_HeapDouble * p, Fxu_Double * pDiv )

extern

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fxu_HeapDoubleGetMax()

Fxu_Double * Fxu_HeapDoubleGetMax ( Fxu_HeapDouble * p )

extern

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;     
}

Here is the caller graph for this function:

Fxu_HeapDoubleInsert()

void Fxu_HeapDoubleInsert ( Fxu_HeapDouble * p, Fxu_Double * pDiv )

extern

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 );
}

Here is the caller graph for this function:

Fxu_HeapDoublePrint()

void Fxu_HeapDoublePrint ( FILE * pFile, Fxu_HeapDouble * p )

extern

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" );
}

Here is the call graph for this function:

Fxu_HeapDoubleReadMax()

Fxu_Double * Fxu_HeapDoubleReadMax ( Fxu_HeapDouble * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 273 of file fxuHeapD.c.

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

Fxu_HeapDoubleReadMaxWeight()

int Fxu_HeapDoubleReadMaxWeight ( Fxu_HeapDouble * p )

extern

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]);
}

Here is the caller graph for this function:

Fxu_HeapDoubleStart()

Fxu_HeapDouble * Fxu_HeapDoubleStart ( )

extern

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fxu_HeapDoubleStop()

void Fxu_HeapDoubleStop ( Fxu_HeapDouble * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 99 of file fxuHeapD.c.

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

Here is the caller graph for this function:

Fxu_HeapDoubleUpdate()

void Fxu_HeapDoubleUpdate ( Fxu_HeapDouble * p, Fxu_Double * pDiv )

extern

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 );
}

Here is the caller graph for this function:

Fxu_HeapSingleCheck()

void Fxu_HeapSingleCheck ( Fxu_HeapSingle * p )

extern

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 );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fxu_HeapSingleCheckOne()

void Fxu_HeapSingleCheckOne ( Fxu_HeapSingle * p, Fxu_Single * pSingle )

extern

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 );
    }
}

Here is the caller graph for this function:

Fxu_HeapSingleDelete()

void Fxu_HeapSingleDelete ( Fxu_HeapSingle * p, Fxu_Single * pSingle )

extern

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;
}

Here is the call graph for this function:

Fxu_HeapSingleGetMax()

Fxu_Single * Fxu_HeapSingleGetMax ( Fxu_HeapSingle * p )

extern

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;     
}

Here is the caller graph for this function:

Fxu_HeapSingleInsert()

void Fxu_HeapSingleInsert ( Fxu_HeapSingle * p, Fxu_Single * pSingle )

extern

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 );
}

Here is the caller graph for this function:

Fxu_HeapSinglePrint()

void Fxu_HeapSinglePrint ( FILE * pFile, Fxu_HeapSingle * p )

extern

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" );
}

Here is the call graph for this function:

Fxu_HeapSingleReadMax()

Fxu_Single * Fxu_HeapSingleReadMax ( Fxu_HeapSingle * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 275 of file fxuHeapS.c.

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

Here is the caller graph for this function:

Fxu_HeapSingleReadMaxWeight()

int Fxu_HeapSingleReadMaxWeight ( Fxu_HeapSingle * p )

extern

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]);
}

Here is the caller graph for this function:

Fxu_HeapSingleStart()

Fxu_HeapSingle * Fxu_HeapSingleStart ( )

extern

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fxu_HeapSingleStop()

void Fxu_HeapSingleStop ( Fxu_HeapSingle * p )

extern

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 );
}

Here is the caller graph for this function:

Fxu_HeapSingleUpdate()

void Fxu_HeapSingleUpdate ( Fxu_HeapSingle * p, Fxu_Single * pSingle )

extern

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 );
}

Here is the caller graph for this function:

Fxu_ListCubeAddLiteral()

void Fxu_ListCubeAddLiteral ( Fxu_Cube * pCube, Fxu_Lit * pLink )

extern

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++;
}

Here is the caller graph for this function:

Fxu_ListCubeDelLiteral()

void Fxu_ListCubeDelLiteral ( Fxu_Cube * pCube, Fxu_Lit * pLink )

extern

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--;
}

Here is the caller graph for this function:

Fxu_ListDoubleAddPairFirst()

void Fxu_ListDoubleAddPairFirst ( Fxu_Double * pDiv, Fxu_Pair * pLink )

extern

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++;
}

Fxu_ListDoubleAddPairLast()

void Fxu_ListDoubleAddPairLast ( Fxu_Double * pDiv, Fxu_Pair * pLink )

extern

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++;
}

Here is the caller graph for this function:

Fxu_ListDoubleAddPairMiddle()

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

extern

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++;
}

Fxu_ListDoubleDelPair()

void Fxu_ListDoubleDelPair ( Fxu_Double * pDiv, Fxu_Pair * pLink )

extern

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--;
}

Fxu_ListMatrixAddCube()

void Fxu_ListMatrixAddCube ( Fxu_Matrix * p, Fxu_Cube * pLink )

extern

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++;
}

Here is the caller graph for this function:

Fxu_ListMatrixAddSingle()

void Fxu_ListMatrixAddSingle ( Fxu_Matrix * p, Fxu_Single * pLink )

extern

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++;
}

Here is the caller graph for this function:

Fxu_ListMatrixAddVariable()

void Fxu_ListMatrixAddVariable ( Fxu_Matrix * p, Fxu_Var * pLink )

extern

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++;
}

Here is the caller graph for this function:

Fxu_ListMatrixDelCube()

void Fxu_ListMatrixDelCube ( Fxu_Matrix * p, Fxu_Cube * pLink )

extern

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--;
}

Fxu_ListMatrixDelSingle()

void Fxu_ListMatrixDelSingle ( Fxu_Matrix * p, Fxu_Single * pLink )

extern

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--;
}

Fxu_ListMatrixDelVariable()

void Fxu_ListMatrixDelVariable ( Fxu_Matrix * p, Fxu_Var * pLink )

extern

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--;
}

Fxu_ListTableAddDivisor()

void Fxu_ListTableAddDivisor ( Fxu_Matrix * p, Fxu_Double * pLink )

extern

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++;
}

Here is the caller graph for this function:

Fxu_ListTableDelDivisor()

void Fxu_ListTableDelDivisor ( Fxu_Matrix * p, Fxu_Double * pLink )

extern

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--;
}

Here is the caller graph for this function:

Fxu_ListVarAddLiteral()

void Fxu_ListVarAddLiteral ( Fxu_Var * pVar, Fxu_Lit * pLink )

extern

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++;
}

Here is the caller graph for this function:

Fxu_ListVarDelLiteral()

void Fxu_ListVarDelLiteral ( Fxu_Var * pVar, Fxu_Lit * pLink )

extern

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--;
}

Here is the caller graph for this function:

Fxu_MatrixAddCube()

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

extern

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fxu_MatrixAddDivisor()

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

extern

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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fxu_MatrixAddLiteral()

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

extern

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++;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fxu_MatrixAddSingle()

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

extern

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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fxu_MatrixAddVar()

Fxu_Var * Fxu_MatrixAddVar ( Fxu_Matrix * p )

extern

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fxu_MatrixAllocate()

Fxu_Matrix * Fxu_MatrixAllocate ( )

extern

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fxu_MatrixComputeSingles()

void Fxu_MatrixComputeSingles ( Fxu_Matrix * p, int fUse0, int nSingleMax )

extern

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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fxu_MatrixComputeSinglesOne()

void Fxu_MatrixComputeSinglesOne ( Fxu_Matrix * p, Fxu_Var * pVar )

extern

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 );
}

Here is the call graph for this function:

Fxu_MatrixDelDivisor()

void Fxu_MatrixDelDivisor ( Fxu_Matrix * p, Fxu_Double * pDiv )

extern

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 );
}

Here is the call graph for this function:

Fxu_MatrixDelete()

void Fxu_MatrixDelete ( Fxu_Matrix * p )

extern

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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fxu_MatrixDelLiteral()

void Fxu_MatrixDelLiteral ( Fxu_Matrix * p, Fxu_Lit * pLit )

extern

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--;
}

Here is the call graph for this function:

Fxu_MatrixPrint()

void Fxu_MatrixPrint ( FILE * pFile, Fxu_Matrix * p )

extern

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 );
}

Fxu_MatrixPrintDivisorProfile()

void Fxu_MatrixPrintDivisorProfile ( FILE * pFile, Fxu_Matrix * p )

extern

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 );
}

Here is the call graph for this function:

Fxu_MatrixRingCubesUnmark()

void Fxu_MatrixRingCubesUnmark ( Fxu_Matrix * p )

extern

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 );
}

Here is the caller graph for this function:

Fxu_MatrixRingVarsUnmark()

void Fxu_MatrixRingVarsUnmark ( Fxu_Matrix * p )

extern

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 );
}

Here is the caller graph for this function:

Fxu_MemFetch()

char * Fxu_MemFetch ( Fxu_Matrix * p, int nBytes )

extern

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 );
}

Here is the call graph for this function:

Fxu_MemRecycle()

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

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 247 of file fxu.c.

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

Here is the call graph for this function:

Fxu_PairAdd()

void Fxu_PairAdd ( Fxu_Pair * pPair )

extern

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;
}

Here is the caller graph for this function:

Fxu_PairAlloc()

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

extern

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fxu_PairAllocStorage()

void Fxu_PairAllocStorage ( Fxu_Var * pVar, int nCubes )

extern

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;
}

Here is the call graph for this function:

Fxu_PairCanonicize()

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

extern

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;
    }
}

Here is the caller graph for this function:

Fxu_PairClearStorage()

void Fxu_PairClearStorage ( Fxu_Cube * pCube )

extern

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;
    }
}

Fxu_PairCompare()

int Fxu_PairCompare ( Fxu_Pair * pPair1, Fxu_Pair * pPair2 )

extern

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;
}

Here is the caller graph for this function:

Fxu_PairFreeStorage()

void Fxu_PairFreeStorage ( Fxu_Var * pVar )

extern

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 );
    }
}

Fxu_PairHashKey()

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

extern

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;
}

Here is the caller graph for this function:

Fxu_PairHashKeyArray()

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

extern

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;
}

Here is the caller graph for this function:

Fxu_PairHashKeyMv()

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

extern

Fxu_Select()

int Fxu_Select ( Fxu_Matrix * p, Fxu_Single ** ppSingle, Fxu_Double ** ppDouble )

extern

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fxu_SelectSCD()

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

extern

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;
}

Here is the call graph for this function:

Fxu_SingleCountCoincidence()

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

extern

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;
}

Here is the caller graph for this function:

Fxu_Update()

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

extern

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++;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fxu_UpdateDouble()

void Fxu_UpdateDouble ( Fxu_Matrix * p )

extern

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++;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fxu_UpdateSingle()

void Fxu_UpdateSingle ( Fxu_Matrix * p )

extern

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++;
}

Here is the call graph for this function:

Here is the caller graph for this function: