reo.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include "misc/extra/extraBdd.h"

Go to the source code of this file.

Data Structures
struct	_reo_unit
struct	_reo_plane
struct	_reo_hash
struct	_reo_man

Macros
#define	REO_REORDER_LIMIT   1.15
	MACRO DEFINITIONS ///. More...
#define	REO_QUAL_PAR   3
#define	REO_CONST_LEVEL   30000
#define	REO_TOPREF_UNDEF   30000
#define	REO_CHUNK_SIZE   5000
#define	REO_COST_EPSILON   0.0000001
#define	REO_HIGH_VALUE   10000000
#define	REO_ENABLE   1
#define	REO_DISABLE   0
#define	Unit_Regular(u)   ((reo_unit *)((ABC_PTRUINT_T)(u) & ~01))
#define	Unit_Not(u)   ((reo_unit *)((ABC_PTRUINT_T)(u) ^ 01))
#define	Unit_NotCond(u, c)   ((reo_unit *)((ABC_PTRUINT_T)(u) ^ (c)))
#define	Unit_IsConstant(u)   ((int)((u)->lev == REO_CONST_LEVEL))

Typedefs
typedef struct _reo_unit	reo_unit
	DATA STRUCTURES ///. More...
typedef struct _reo_plane	reo_plane
typedef struct _reo_hash	reo_hash
typedef struct _reo_man	reo_man
typedef struct _reo_test	reo_test

Enumerations
enum	reo_min_type { REO_MINIMIZE_NODES, REO_MINIMIZE_WIDTH, REO_MINIMIZE_APL }

Functions
reo_man *	Extra_ReorderInit (int nDdVarsMax, int nNodesMax)
	FUNCTION DECLARATIONS ///. More...
void	Extra_ReorderQuit (reo_man *p)
void	Extra_ReorderSetMinimizationType (reo_man *p, reo_min_type fMinType)
void	Extra_ReorderSetRemapping (reo_man *p, int fRemapUp)
void	Extra_ReorderSetIterations (reo_man *p, int nIters)
void	Extra_ReorderSetVerbosity (reo_man *p, int fVerbose)
void	Extra_ReorderSetVerification (reo_man *p, int fVerify)
DdNode *	Extra_Reorder (reo_man *p, DdManager *dd, DdNode *Func, int *pOrder)
void	Extra_ReorderArray (reo_man *p, DdManager *dd, DdNode *Funcs[], DdNode *FuncsRes[], int nFuncs, int *pOrder)
void	reoReorderArray (reo_man *p, DdManager *dd, DdNode *Funcs[], DdNode *FuncsRes[], int nFuncs, int *pOrder)
	FUNCTION DEFINITIONS ///. More...
void	reoResizeStructures (reo_man *p, int nDdVarsMax, int nNodesMax, int nFuncs)
void	reoProfileNodesStart (reo_man *p)
	DECLARATIONS ///. More...
void	reoProfileAplStart (reo_man *p)
void	reoProfileWidthStart (reo_man *p)
void	reoProfileWidthStart2 (reo_man *p)
void	reoProfileAplPrint (reo_man *p)
void	reoProfileNodesPrint (reo_man *p)
void	reoProfileWidthPrint (reo_man *p)
void	reoProfileWidthVerifyLevel (reo_plane *pPlane, int Level)
void	reoReorderSift (reo_man *p)
	DECLARATIONS ///. More...
double	reoReorderSwapAdjacentVars (reo_man *p, int Level, int fMovingUp)
	FUNCTION DEFINITIONS ///. More...
reo_unit *	reoTransferNodesToUnits_rec (reo_man *p, DdNode *F)
	DECLARATIONS ///. More...
DdNode *	reoTransferUnitsToNodes_rec (reo_man *p, reo_unit *pUnit)
reo_unit *	reoUnitsGetNextUnit (reo_man *p)
	FUNCTION DEFINITIONS ///. More...
void	reoUnitsRecycleUnit (reo_man *p, reo_unit *pUnit)
void	reoUnitsRecycleUnitList (reo_man *p, reo_plane *pPlane)
void	reoUnitsAddUnitToPlane (reo_plane *pPlane, reo_unit *pUnit)
void	reoUnitsStopDispenser (reo_man *p)
void	Extra_ReorderTest (DdManager *dd, DdNode *Func)
	DECLARATIONS ///. More...
DdNode *	Extra_ReorderCudd (DdManager *dd, DdNode *aFunc, int pPermuteReo[])
int	Extra_bddReorderTest (DdManager *dd, DdNode *bF)
int	Extra_addReorderTest (DdManager *dd, DdNode *aF)

Macro Definition Documentation

#define REO_CHUNK_SIZE   5000

Definition at line 42 of file reo.h.

#define REO_CONST_LEVEL   30000

Definition at line 40 of file reo.h.

#define REO_COST_EPSILON   0.0000001

Definition at line 43 of file reo.h.

#define REO_DISABLE   0

Definition at line 47 of file reo.h.

#define REO_ENABLE   1

Definition at line 46 of file reo.h.

#define REO_HIGH_VALUE   10000000

Definition at line 44 of file reo.h.

#define REO_QUAL_PAR   3

Definition at line 38 of file reo.h.

#define REO_REORDER_LIMIT   1.15

MACRO DEFINITIONS ///.

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

FileName [reo.h]

PackageName [REO: A specialized DD reordering engine.]

Synopsis [External and internal declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - October 15, 2002.]

Revision [

Id:

reo.h,v 1.0 2002/15/10 03:00:00 alanmi Exp

]

Definition at line 37 of file reo.h.

#define REO_TOPREF_UNDEF   30000

Definition at line 41 of file reo.h.

#define Unit_IsConstant

(

u

)

((int)((u)->lev == REO_CONST_LEVEL))

Definition at line 177 of file reo.h.

#define Unit_Not

(

u

)

((reo_unit *)((ABC_PTRUINT_T)(u) ^ 01))

Definition at line 175 of file reo.h.

#define Unit_NotCond	(		u,
			c
	)		((reo_unit *)((ABC_PTRUINT_T)(u) ^ (c)))

Definition at line 176 of file reo.h.

#define Unit_Regular

(

u

)

((reo_unit *)((ABC_PTRUINT_T)(u) & ~01))

Definition at line 174 of file reo.h.

Typedef Documentation

typedef struct _reo_hash reo_hash

Definition at line 62 of file reo.h.

typedef struct _reo_man reo_man

Definition at line 63 of file reo.h.

typedef struct _reo_plane reo_plane

Definition at line 61 of file reo.h.

typedef struct _reo_test reo_test

Definition at line 64 of file reo.h.

typedef struct _reo_unit reo_unit

DATA STRUCTURES ///.

Definition at line 60 of file reo.h.

Enumeration Type Documentation

enum reo_min_type

Enumerator
REO_MINIMIZE_NODES
REO_MINIMIZE_WIDTH
REO_MINIMIZE_APL

Definition at line 50 of file reo.h.

             {
    REO_MINIMIZE_NODES,
    REO_MINIMIZE_WIDTH,   // may not work for BDDs with complemented edges
    REO_MINIMIZE_APL
} reo_min_type;

Function Documentation

int Extra_addReorderTest	(	DdManager *	dd,
		DdNode *	aF
	)

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

Synopsis []

Description [Transfers the ADD into another manager minimizes it and returns the min number of nodes; disposes of the BDD in the new manager. Useful for debugging or comparing the performance of other reordering procedures.]

SideEffects []

SeeAlso []

Definition at line 217 of file reoTest.c.

{
    static DdManager * s_ddmin;
    DdNode * bF;
    DdNode * bFmin;
    DdNode * aFmin;
    int  nNodesBeg;
    int  nNodesEnd;
    abctime clk1;

    if ( s_ddmin == NULL )
        s_ddmin = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);

//  Cudd_ShuffleHeap( s_ddmin, dd->invperm );

    clk1 = Abc_Clock();
    bF    = Cudd_addBddPattern( dd, aF );         Cudd_Ref( bF );
    bFmin = Cudd_bddTransfer( dd, s_ddmin, bF );  Cudd_Ref( bFmin );
    Cudd_RecursiveDeref( dd, bF );
    aFmin = Cudd_BddToAdd( s_ddmin, bFmin );      Cudd_Ref( aFmin );
    Cudd_RecursiveDeref( s_ddmin, bFmin );

    nNodesBeg = Cudd_DagSize( aFmin );
    Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SIFT,1);
//  Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SYMM_SIFT,1);
    nNodesEnd = Cudd_DagSize( aFmin );
    Cudd_RecursiveDeref( s_ddmin, aFmin );

    printf( "Classical reordering of ADDs: Before = %d. After = %d.\n", nNodesBeg, nNodesEnd );
    printf( "Classical variable reordering time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
    return nNodesEnd;
}

int Extra_bddReorderTest	(	DdManager *	dd,
		DdNode *	bF
	)

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

Synopsis []

Description [Transfers the BDD into another manager minimizes it and returns the min number of nodes; disposes of the BDD in the new manager. Useful for debugging or comparing the performance of other reordering procedures.]

SideEffects []

SeeAlso []

Definition at line 180 of file reoTest.c.

{
    static DdManager * s_ddmin;
    DdNode * bFmin;
    int  nNodes;
//  abctime clk1;

    if ( s_ddmin == NULL )
        s_ddmin = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);

//  Cudd_ShuffleHeap( s_ddmin, dd->invperm );

//  clk1 = Abc_Clock();
    bFmin = Cudd_bddTransfer( dd, s_ddmin, bF );  Cudd_Ref( bFmin );
    Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SIFT,1);
//  Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SYMM_SIFT,1);
    nNodes = Cudd_DagSize( bFmin );
    Cudd_RecursiveDeref( s_ddmin, bFmin );

//  printf( "Classical variable reordering time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
    return nNodes;
}

DdNode* Extra_Reorder	(	reo_man *	p,
		DdManager *	dd,
		DdNode *	Func,
		int *	pOrder
	)

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

Synopsis [Performs reordering of the function.]

Description [Returns the DD minimized by variable reordering in the REO engine. Takes the CUDD decision diagram manager (dd) and the function (Func) represented as a BDD or ADD (MTBDD). If the variable array (pOrder) is not NULL, returns the resulting variable permutation. The permutation is such that if the resulting function is permuted by Cudd_(add,bdd)Permute() using pOrder as the permutation array, the initial function (Func) results. Several flag set by other interface functions specify reordering options:

• Remappig can be set by Extra_ReorderSetRemapping(). Then the resulting DD after reordering is remapped into the topmost levels of the DD manager. Otherwise, the resulting DD after reordering is mapped using the same variables, on which it originally depended, only (possibly) permuted as a result of reordering.
• Minimization type can be set by Extra_ReorderSetMinimizationType(). Note that when the BDD is minimized for the total width of the total APL, the number BDD nodes can increase. The total width is defines as sum total of widths on each level. The width on one level is defined as the number of distinct BDD nodes pointed by the nodes situated above the given level.
• The number of iterations of sifting can be set by Extra_ReorderSetIterations(). The decision diagram returned by this procedure is not referenced.]

SideEffects []

SeeAlso []

Definition at line 262 of file reoApi.c.

{
    DdNode * FuncRes;
    Extra_ReorderArray( p, dd, &Func, &FuncRes, 1, pOrder );
    Cudd_Deref( FuncRes );
    return FuncRes;
}

void Extra_ReorderArray	(	reo_man *	p,
		DdManager *	dd,
		DdNode *	Funcs[],
		DdNode *	FuncsRes[],
		int	nFuncs,
		int *	pOrder
	)

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

Synopsis [Performs reordering of the array of functions.]

Description [The options are similar to the procedure Extra_Reorder(), except that the user should also provide storage for the resulting DDs, which are returned referenced.]

SideEffects []

SeeAlso []

Definition at line 283 of file reoApi.c.

{
    reoReorderArray( p, dd, Funcs, FuncsRes, nFuncs, pOrder );
}

DdNode* Extra_ReorderCudd	(	DdManager *	dd,
		DdNode *	aFunc,
		int	pPermuteReo[]
	)

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

Synopsis [Reorders the DD using CUDD package.]

Description [Transfers the DD into a temporary manager in such a way that the level correspondence is preserved. Reorders the manager and transfers the DD back into the original manager using the topmost levels of the manager, in such a way that the ordering of levels is preserved. The resulting permutation is returned in the array given by the user.]

SideEffects []

SeeAlso []

Definition at line 109 of file reoTest.c.

{
    static DdManager * ddReorder = NULL;
    static int * Permute     = NULL;
    static int * PermuteReo1 = NULL;
    static int * PermuteReo2 = NULL;
    DdNode * aFuncReorder, * aFuncNew;
    int lev, var;

    // start the reordering manager
    if ( ddReorder == NULL )
    {
        Permute       = ABC_ALLOC( int, dd->size );
        PermuteReo1   = ABC_ALLOC( int, dd->size );
        PermuteReo2   = ABC_ALLOC( int, dd->size );
        ddReorder = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
        Cudd_AutodynDisable(ddReorder);
    }

    // determine the permutation of variable to make sure that var order in bFunc
    // will not change when this function is transfered into the new manager
    for ( lev = 0; lev < dd->size; lev++ )
    {
        Permute[ dd->invperm[lev] ] = ddReorder->invperm[lev];
        PermuteReo1[ ddReorder->invperm[lev] ] = dd->invperm[lev];
    }
    // transfer this function into the new manager in such a way that ordering of vars does not change
    aFuncReorder = Extra_TransferPermute( dd, ddReorder, aFunc, Permute );  Cudd_Ref( aFuncReorder );
//  assert( Cudd_DagSize(aFunc) == Cudd_DagSize(aFuncReorder)  );

    // perform the reordering
printf( "Nodes before = %d.\n", Cudd_DagSize(aFuncReorder) );
    Cudd_ReduceHeap( ddReorder, CUDD_REORDER_SYMM_SIFT, 1 );
printf( "Nodes before = %d.\n", Cudd_DagSize(aFuncReorder) );

    // determine the reverse variable permutation
    for ( lev = 0; lev < dd->size; lev++ )
    {
        Permute[ ddReorder->invperm[lev] ] = dd->invperm[lev];
        PermuteReo2[ dd->invperm[lev] ] = ddReorder->invperm[lev];
    }

    // transfer this function into the new manager in such a way that ordering of vars does not change
    aFuncNew = Extra_TransferPermute( ddReorder, dd, aFuncReorder, Permute );  Cudd_Ref( aFuncNew );
//  assert( Cudd_DagSize(aFuncNew) == Cudd_DagSize(aFuncReorder)  );
    Cudd_RecursiveDeref( ddReorder, aFuncReorder );

    // derive the resulting variable ordering
    if ( pPermuteReo )
        for ( var = 0; var < dd->size; var++ )
            pPermuteReo[var] = PermuteReo1[ PermuteReo2[var] ];

    Cudd_Deref( aFuncNew );
    return aFuncNew;
}

reo_man* Extra_ReorderInit	(	int	nDdVarsMax,
		int	nNodesMax
	)

FUNCTION DECLARATIONS ///.

FUNCTION DECLARATIONS ///.

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

FileName [reoApi.c]

PackageName [REO: A specialized DD reordering engine.]

Synopsis [Implementation of API functions.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - October 15, 2002.]

Revision [

Id:

reoApi.c,v 1.0 2002/15/10 03:00:00 alanmi Exp

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

Synopsis [Initializes the reordering engine.]

Description [The first argument is the max number of variables in the CUDD DD manager which will be used with the reordering engine (this number of should be the maximum of BDD and ZDD parts). The second argument is the maximum number of BDD nodes in the BDDs to be reordered. These limits are soft. Setting lower limits will later cause the reordering manager to resize internal data structures. However, setting the exact values will make reordering more efficient because resizing will be not necessary.]

SideEffects []

SeeAlso []

Definition at line 50 of file reoApi.c.

{
    reo_man * p;
    // allocate and clean the data structure
    p = ABC_ALLOC( reo_man, 1 );
    memset( p, 0, sizeof(reo_man) );
    // resize the manager to meet user's needs  
    reoResizeStructures( p, nDdVarsMax, nNodesMax, 100 );
    // set the defaults
    p->fMinApl   = 0;
    p->fMinWidth = 0;
    p->fRemapUp  = 0;
    p->fVerbose  = 0;
    p->fVerify   = 0;
    p->nIters    = 1;
    return p;
}

void Extra_ReorderQuit

(

reo_man *

p

)

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

Synopsis [Disposes of the reordering engine.]

Description [Removes all memory associated with the reordering engine.]

SideEffects []

SeeAlso []

Definition at line 79 of file reoApi.c.

{
    ABC_FREE( p->pTops );
    ABC_FREE( p->pSupp );
    ABC_FREE( p->pOrderInt );
    ABC_FREE( p->pWidthCofs );
    ABC_FREE( p->pMapToPlanes );
    ABC_FREE( p->pMapToDdVarsOrig );
    ABC_FREE( p->pMapToDdVarsFinal );
    ABC_FREE( p->pPlanes );
    ABC_FREE( p->pVarCosts );
    ABC_FREE( p->pLevelOrder );
    ABC_FREE( p->HTable );
    ABC_FREE( p->pRefNodes );
    reoUnitsStopDispenser( p );
    ABC_FREE( p->pMemChunks );
    ABC_FREE( p );
}

void Extra_ReorderSetIterations	(	reo_man *	p,
		int	nIters
	)

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

Synopsis [Sets the number of iterations of sifting performed.]

Description [The default is one iteration. But a higher minimization quality is desired, it is possible to set the number of iterations to any number larger than 1. Convergence is often reached after several iterations, so typically it make no sense to set the number of iterations higher than 3.]

SideEffects []

SeeAlso []

Definition at line 192 of file reoApi.c.

{
    p->nIters = nIters;
}

void Extra_ReorderSetMinimizationType	(	reo_man *	p,
		reo_min_type	fMinType
	)

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

Synopsis [Sets the type of DD minimizationl that will be performed.]

Description [Currently, three different types of minimization are supported. It is possible to minimize the number of BDD nodes. This is a classical type of minimization, which is attempting to reduce the total number of nodes in the (shared) BDD of the given Boolean functions. It is also possible to minimize the BDD width, defined as the sum total of the number of cofactors on each level in the (shared) BDD (note that the number of cofactors on the given level may be larger than the number of nodes appearing on the given level). It is also possible to minimize the average path length in the (shared) BDD defined as the sum of products, for all BDD paths from the top node to any terminal node, of the number of minterms on the path by the number of nodes on the path. The default reordering type is minimization for the number of BDD nodes. Calling this function with REO_MINIMIZE_WIDTH or REO_MINIMIZE_APL as the second argument, changes the default minimization option for all the reorder calls performed afterwards.]

SideEffects []

SeeAlso []

Definition at line 122 of file reoApi.c.

{
    if ( fMinType == REO_MINIMIZE_NODES ) 
    {
        p->fMinWidth = 0;
        p->fMinApl   = 0;
    }
    else if ( fMinType == REO_MINIMIZE_WIDTH )
    {
        p->fMinWidth = 1;
        p->fMinApl   = 0;
    }
    else if ( fMinType == REO_MINIMIZE_APL )
    {
        p->fMinWidth = 0;
        p->fMinApl   = 1;
    }
    else 
    {
        assert( 0 );
    }
}

void Extra_ReorderSetRemapping	(	reo_man *	p,
		int	fRemapUp
	)

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

Synopsis [Sets the type of remapping performed by the engine.]

Description [The remapping refers to the way the resulting BDD is expressed using the elementary variables of the CUDD BDD manager. Currently, two types possibilities are supported: remapping and no remapping. Remapping means that the function(s) after reordering depend on the topmost variables in the manager. No remapping means that the function(s) after reordering depend on the same variables as before. Consider the following example. Suppose the initial four variable function depends on variables 2,4,5, and 9 on the CUDD BDD manager, which may be found anywhere in the current variable order. If remapping is set, the function after ordering depends on the topmost variables in the manager, which may or may not be the same as the variables 2,4,5, and 9. If no remapping is set, then the reordered function depend on the same variables 2,4,5, and 9, but the meaning of each variale has changed according to the new ordering. The resulting ordering is returned in the array "pOrder" filled out by the reordering engine in the call to Extra_Reorder(). The default is no remapping.]

SideEffects []

SeeAlso []

Definition at line 172 of file reoApi.c.

{
    p->fRemapUp = fRemapUp;
}

void Extra_ReorderSetVerbosity	(	reo_man *	p,
		int	fVerbose
	)

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

Synopsis [Sets the verbosity level.]

Description [Setting the level to 1 results in printing statistics before and after the reordering.]

SideEffects []

SeeAlso []

Definition at line 229 of file reoApi.c.

{
    p->fVerbose = fVerbose;
}

void Extra_ReorderSetVerification	(	reo_man *	p,
		int	fVerify
	)

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

Synopsis [Sets the verification mode.]

Description [Setting the level to 1 results in verifying the results of variable reordering. Verification is performed by remapping the resulting functions into the original variable order and comparing them with the original functions given by the user. Enabling verification typically leads to 20-30% increase in the total runtime of REO.]

SideEffects []

SeeAlso []

Definition at line 212 of file reoApi.c.

{
    p->fVerify = fVerify;
}

void Extra_ReorderTest	(	DdManager *	dd,
		DdNode *	Func
	)

DECLARATIONS ///.

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

FileName [reoTest.c]

PackageName [REO: A specialized DD reordering engine.]

Synopsis [Various testing procedures (may be outdated).]

Author [Alan Mishchenko alanm.nosp@m.i@ec.nosp@m.e.pdx.nosp@m..edu]

Affiliation [ECE Department. Portland State University, Portland, Oregon.]

Date [Ver. 1.0. Started - October 15, 2002.]

Revision [

Id:

reoTest.c,v 1.0 2002/15/10 03:00:00 alanmi Exp

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

Synopsis [Reorders the DD using REO and CUDD.]

Description [This function can be used to test the performance of the reordering package.]

SideEffects []

SeeAlso []

Definition at line 43 of file reoTest.c.

{
    reo_man * pReo;
    DdNode * Temp, * Temp1;
    int pOrder[1000];

    pReo = Extra_ReorderInit( 100, 100 );

//Extra_DumpDot( dd, &Func, 1, "beforReo.dot", 0 );
    Temp  = Extra_Reorder( pReo, dd, Func, pOrder );  Cudd_Ref( Temp );
//Extra_DumpDot( dd, &Temp, 1, "afterReo.dot", 0 );

    Temp1 = Extra_ReorderCudd(dd, Func, NULL );           Cudd_Ref( Temp1 );
printf( "Initial = %d. Final = %d. Cudd = %d.\n", Cudd_DagSize(Func), Cudd_DagSize(Temp), Cudd_DagSize(Temp1)  );
    Cudd_RecursiveDeref( dd, Temp1 );
    Cudd_RecursiveDeref( dd, Temp );
 
    Extra_ReorderQuit( pReo );
}

void reoProfileAplPrint

(

reo_man *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 305 of file reoProfile.c.

{
    printf( "APL: Total = %8.2f. Average =%6.2f.\n", p->nAplCur, p->nAplCur / (float)p->nSupp );
}

void reoProfileAplStart

(

reo_man *

p

)

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

Synopsis [Start the profile for the APL.]

Description [Computes the total path length. The path length is normalized by dividing it by 2^|supp(f)|. To get the "real" APL, multiply by 2^|supp(f)|. This procedure assumes that Weight field of all nodes has been set to 0.0 before the call, except for the weight of the topmost node, which is set to 1.0 (1.0 is the probability of traversing the topmost node). This procedure assigns the edge weights. Because of the equal probability of selecting 0 and 1 assignment at a node, the edge weights are the same for the node. Instead of storing them, we store the weight of the node, which is the probability of traversing the node (pUnit->Weight) during the top down evalation of the BDD. ]

SideEffects []

SeeAlso []

Definition at line 78 of file reoProfile.c.

{
    reo_unit * pER, * pTR;
    reo_unit * pUnit;
    double Res, Half;
    int i;

    // clean the weights of all nodes
    for ( i = 0; i < p->nSupp; i++ )
        for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next )
            pUnit->Weight = 0.0;
    // to assign the node weights (the probability of visiting each node)
    // we visit the node after visiting its predecessors

    // set the probability of visits to the top nodes
    for ( i = 0; i < p->nTops; i++ )
        Unit_Regular(p->pTops[i])->Weight += 1.0;

    // to compute the path length (the sum of products of edge weight by edge length)
    // we visit the nodes in any order (the above order will do)
    Res = 0.0;
    for ( i = 0; i < p->nSupp; i++ )
    {
        p->pPlanes[i].statsCost = 0.0;
        for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next )
        {
            pER  = Unit_Regular(pUnit->pE);
            pTR  = Unit_Regular(pUnit->pT);
            Half = 0.5 * pUnit->Weight;
            pER->Weight += Half;
            pTR->Weight += Half;
            // add to the path length
            p->pPlanes[i].statsCost += pUnit->Weight;
        }
        Res += p->pPlanes[i].statsCost;
    }
    p->pPlanes[p->nSupp].statsCost = 0.0;
    p->nAplBeg = p->nAplCur = Res;
}

void reoProfileNodesPrint

(

reo_man *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 289 of file reoProfile.c.

{
    printf( "NODES: Total = %6d. Average = %6.2f.\n", p->nNodesCur, p->nNodesCur / (float)p->nSupp );
}

void reoProfileNodesStart

(

reo_man *

p

)

DECLARATIONS ///.

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

FileName [reoProfile.c]

PackageName [REO: A specialized DD reordering engine.]

Synopsis [Procudures that compute variables profiles (nodes, width, APL).]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - October 15, 2002.]

Revision [

Id:

reoProfile.c,v 1.0 2002/15/10 03:00:00 alanmi Exp

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

Synopsis [Start the profile for the BDD nodes.]

Description [TopRef is the first level, on this the given node counts towards the width of the BDDs. (In other words, it is the level of the referencing node plus 1.)]

SideEffects []

SeeAlso []

Definition at line 46 of file reoProfile.c.

{
    int Total, i;
    Total = 0;
    for ( i = 0; i <= p->nSupp; i++ )
    {
        p->pPlanes[i].statsCost = p->pPlanes[i].statsNodes;
        Total += p->pPlanes[i].statsNodes;
    }
    assert( Total == p->nNodesCur );
    p->nNodesBeg = p->nNodesCur;
}

void reoProfileWidthPrint

(

reo_man *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 321 of file reoProfile.c.

{
    int WidthMax;
    int TotalWidth;
    int i;

    WidthMax   = 0;
    TotalWidth = 0;
    for ( i = 0; i <= p->nSupp; i++ )
    {
        printf( "Level = %2d. Width = %3d.\n", i, p->pPlanes[i].statsWidth );
        if ( WidthMax < p->pPlanes[i].statsWidth )
             WidthMax = p->pPlanes[i].statsWidth;
        TotalWidth += p->pPlanes[i].statsWidth;
    }
    assert( p->nWidthCur == TotalWidth );
    printf( "WIDTH: " );
    printf( "Maximum = %5d.  ", WidthMax );
    printf( "Total = %7d.  ", p->nWidthCur );
    printf( "Average = %6.2f.\n", TotalWidth / (float)p->nSupp );
}

void reoProfileWidthStart

(

reo_man *

p

)

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

Synopsis [Start the profile for the BDD width. Complexity of the algorithm is O(N + n).]

Description [TopRef is the first level, on which the given node counts towards the width of the BDDs. (In other words, it is the level of the referencing node plus 1.)]

SideEffects []

SeeAlso []

Definition at line 130 of file reoProfile.c.

{
    reo_unit * pUnit;
    int * pWidthStart;
    int * pWidthStop;
    int v;

    // allocate and clean the storage for starting and stopping levels
    pWidthStart = ABC_ALLOC( int, p->nSupp + 1 );
    pWidthStop  = ABC_ALLOC( int, p->nSupp + 1 );
    memset( pWidthStart, 0, sizeof(int) * (p->nSupp + 1) );
    memset( pWidthStop, 0, sizeof(int) * (p->nSupp + 1) );

    // go through the non-constant nodes and set the topmost level of their cofactors
    for ( v = 0; v <= p->nSupp; v++ )
    for ( pUnit = p->pPlanes[v].pHead; pUnit; pUnit = pUnit->Next )
    {
        pUnit->TopRef = REO_TOPREF_UNDEF;
        pUnit->Sign   = 0;
    }

    // add the topmost level of the width profile
    for ( v = 0; v < p->nTops; v++ )
    {
        pUnit = Unit_Regular(p->pTops[v]);
        if ( pUnit->TopRef == REO_TOPREF_UNDEF )
        {
            // set the starting level
            pUnit->TopRef = 0;
            pWidthStart[pUnit->TopRef]++;
            // set the stopping level
            if ( pUnit->lev != REO_CONST_LEVEL )
                pWidthStop[pUnit->lev+1]++;
        }
    }

    for ( v = 0; v < p->nSupp; v++ )
    for ( pUnit = p->pPlanes[v].pHead; pUnit; pUnit = pUnit->Next )
    {
        if ( pUnit->pE->TopRef == REO_TOPREF_UNDEF )
        {
            // set the starting level
            pUnit->pE->TopRef = pUnit->lev + 1;
            pWidthStart[pUnit->pE->TopRef]++;
            // set the stopping level
            if ( pUnit->pE->lev != REO_CONST_LEVEL )
                pWidthStop[pUnit->pE->lev+1]++;
        }
        if ( pUnit->pT->TopRef == REO_TOPREF_UNDEF )
        {
            // set the starting level
            pUnit->pT->TopRef = pUnit->lev + 1;
            pWidthStart[pUnit->pT->TopRef]++;
            // set the stopping level
            if ( pUnit->pT->lev != REO_CONST_LEVEL )
                pWidthStop[pUnit->pT->lev+1]++;
        }
    }

    // verify the top reference
    for ( v = 0; v < p->nSupp; v++ )
        reoProfileWidthVerifyLevel( p->pPlanes + v, v );

    // derive the profile
    p->nWidthCur = 0;
    for ( v = 0; v <= p->nSupp; v++ )
    {
        if ( v == 0 )
            p->pPlanes[v].statsWidth = pWidthStart[v] - pWidthStop[v];
        else
            p->pPlanes[v].statsWidth = p->pPlanes[v-1].statsWidth + pWidthStart[v] - pWidthStop[v];
        p->pPlanes[v].statsCost = p->pPlanes[v].statsWidth;
        p->nWidthCur += p->pPlanes[v].statsWidth;
        printf( "Level %2d: Width = %5d.\n", v, p->pPlanes[v].statsWidth );
    }
    p->nWidthBeg = p->nWidthCur;
    ABC_FREE( pWidthStart );
    ABC_FREE( pWidthStop );
}

void reoProfileWidthStart2

(

reo_man *

p

)

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

Synopsis [Start the profile for the BDD width. Complexity of the algorithm is O(N * n).]

Description [TopRef is the first level, on which the given node counts towards the width of the BDDs. (In other words, it is the level of the referencing node plus 1.)]

SideEffects []

SeeAlso []

Definition at line 222 of file reoProfile.c.

{
    reo_unit * pUnit;
    int i, v;

    // clean the profile
    for ( i = 0; i <= p->nSupp; i++ )
        p->pPlanes[i].statsWidth = 0;
    
    // clean the node structures
    for ( v = 0; v <= p->nSupp; v++ )
    for ( pUnit = p->pPlanes[v].pHead; pUnit; pUnit = pUnit->Next )
    {
        pUnit->TopRef = REO_TOPREF_UNDEF;
        pUnit->Sign   = 0;
    }

    // set the topref to the topmost nodes
    for ( i = 0; i < p->nTops; i++ )
        Unit_Regular(p->pTops[i])->TopRef = 0;

    // go through the non-constant nodes and set the topmost level of their cofactors
    for ( i = 0; i < p->nSupp; i++ )
        for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next )
        {
            if ( pUnit->pE->TopRef > i+1 )
                 pUnit->pE->TopRef = i+1;
            if ( pUnit->pT->TopRef > i+1 )
                 pUnit->pT->TopRef = i+1;
        }

    // verify the top reference
    for ( i = 0; i < p->nSupp; i++ )
        reoProfileWidthVerifyLevel( p->pPlanes + i, i );

    // compute the profile for the internal nodes
    for ( i = 0; i < p->nSupp; i++ )
        for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next )
            for ( v = pUnit->TopRef; v <= pUnit->lev; v++ )
                p->pPlanes[v].statsWidth++;

    // compute the profile for the constant nodes
    for ( pUnit = p->pPlanes[p->nSupp].pHead; pUnit; pUnit = pUnit->Next )
        for ( v = pUnit->TopRef; v <= p->nSupp; v++ )
            p->pPlanes[v].statsWidth++;

    // get the width cost
    p->nWidthCur = 0;
    for ( i = 0; i <= p->nSupp; i++ )
    {
        p->pPlanes[i].statsCost = p->pPlanes[i].statsWidth;
        p->nWidthCur           += p->pPlanes[i].statsWidth;
    }
    p->nWidthBeg = p->nWidthCur;
}

void reoProfileWidthVerifyLevel	(	reo_plane *	pPlane,
		int	Level
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 354 of file reoProfile.c.

{
    reo_unit * pUnit;
    for ( pUnit = pPlane->pHead; pUnit; pUnit = pUnit->Next )
    {
        assert( pUnit->TopRef     <= Level );
        assert( pUnit->pE->TopRef <= Level + 1 );
        assert( pUnit->pT->TopRef <= Level + 1 );
    }
}

void reoReorderArray	(	reo_man *	p,
		DdManager *	dd,
		DdNode *	Funcs[],
		DdNode *	FuncsRes[],
		int	nFuncs,
		int *	pOrder
	)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 50 of file reoCore.c.

{
    int Counter, i;

    // set the initial parameters
    p->dd     = dd;
    p->pOrder = pOrder;
    p->nTops  = nFuncs;
    // get the initial number of nodes
    p->nNodesBeg = Cudd_SharingSize( Funcs, nFuncs );     
    // resize the internal data structures of the manager if necessary
    reoResizeStructures( p, ddMax(dd->size,dd->sizeZ), p->nNodesBeg, nFuncs );
    // compute the support
    p->pSupp = Extra_VectorSupportArray( dd, Funcs, nFuncs, p->pSupp );
    // get the number of support variables
    p->nSupp = 0;
    for ( i = 0; i < dd->size; i++ )
        p->nSupp += p->pSupp[i];

    // if it is the constant function, no need to reorder
    if ( p->nSupp == 0 )
    {
        for ( i = 0; i < nFuncs; i++ )
        {
            FuncsRes[i] = Funcs[i]; Cudd_Ref( FuncsRes[i] );
        }
        return;
    }

    // create the internal variable maps
    // go through variable levels in the manager
    Counter = 0;
    for ( i = 0; i < dd->size; i++ )
        if ( p->pSupp[ dd->invperm[i] ] )
        {
            p->pMapToPlanes[ dd->invperm[i] ] = Counter;
            p->pMapToDdVarsOrig[Counter]      = dd->invperm[i];
            if ( !p->fRemapUp )
                p->pMapToDdVarsFinal[Counter] = dd->invperm[i];
            else
                p->pMapToDdVarsFinal[Counter] = dd->invperm[Counter];
            p->pOrderInt[Counter]        = Counter;
            Counter++;
        }

    // set the initial parameters
    p->nUnitsUsed = 0;
    p->nNodesCur  = 0;
    p->fThisIsAdd = 0;
    p->Signature++;
    // transfer the function from the CUDD package into REO"s internal data structure
    for ( i = 0; i < nFuncs; i++ )
        p->pTops[i] = reoTransferNodesToUnits_rec( p, Funcs[i] );
    assert( p->nNodesBeg == p->nNodesCur );

    if ( !p->fThisIsAdd && p->fMinWidth )
    {
        printf( "An important message from the REO reordering engine:\n" );
        printf( "The BDD given to the engine for reordering contains complemented edges.\n" );
        printf( "Currently, such BDDs cannot be reordered for the minimum width.\n" );
        printf( "Therefore, minimization for the number of BDD nodes is performed.\n" );
        fflush( stdout );
        p->fMinApl   = 0;
        p->fMinWidth = 0;
    }

    if ( p->fMinWidth )
        reoProfileWidthStart(p);
    else if ( p->fMinApl )
        reoProfileAplStart(p);
    else 
        reoProfileNodesStart(p);

    if ( p->fVerbose )
    {
        printf( "INITIAL:\n" );
        if ( p->fMinWidth )
            reoProfileWidthPrint(p);
        else if ( p->fMinApl )
            reoProfileAplPrint(p);
        else
            reoProfileNodesPrint(p);
    }
 
    ///////////////////////////////////////////////////////////////////
    // performs the reordering
    p->nSwaps   = 0;
    p->nNISwaps = 0;
    for ( i = 0; i < p->nIters; i++ )
    {
        reoReorderSift( p );
        // print statistics after each iteration
        if ( p->fVerbose )
        {
            printf( "ITER #%d:\n", i+1 );
            if ( p->fMinWidth )
                reoProfileWidthPrint(p);
            else if ( p->fMinApl )
                reoProfileAplPrint(p);
            else
                reoProfileNodesPrint(p);
        }
        // if the cost function did not change, stop iterating
        if ( p->fMinWidth )
        {
            p->nWidthEnd = p->nWidthCur;
            assert( p->nWidthEnd <= p->nWidthBeg );
            if ( p->nWidthEnd == p->nWidthBeg )
                break;
        }
        else if ( p->fMinApl )
        {
            p->nAplEnd = p->nAplCur;
            assert( p->nAplEnd <= p->nAplBeg );
            if ( p->nAplEnd == p->nAplBeg )
                break;
        }
        else
        {
            p->nNodesEnd = p->nNodesCur;
            assert( p->nNodesEnd <= p->nNodesBeg );
            if ( p->nNodesEnd == p->nNodesBeg )
                break;
        }
    }
    assert( reoCheckLevels( p ) );
    ///////////////////////////////////////////////////////////////////

s_AplBefore = p->nAplBeg;
s_AplAfter  = p->nAplEnd;

    // set the initial parameters
    p->nRefNodes  = 0;
    p->nNodesCur  = 0;
    p->Signature++;
    // transfer the BDDs from REO's internal data structure to CUDD
    for ( i = 0; i < nFuncs; i++ )
    {
        FuncsRes[i] = reoTransferUnitsToNodes_rec( p, p->pTops[i] ); Cudd_Ref( FuncsRes[i] );
    }
    // undo the DDs referenced for storing in the cache
    for ( i = 0; i < p->nRefNodes; i++ )
        Cudd_RecursiveDeref( dd, p->pRefNodes[i] );
    // verify zero refs of the terminal nodes
    for ( i = 0; i < nFuncs; i++ )
    {
        assert( reoRecursiveDeref( p->pTops[i] ) );
    }
    assert( reoCheckZeroRefs( &(p->pPlanes[p->nSupp]) ) );

    // prepare the variable map to return to the user
    if ( p->pOrder )
    {
        // i is the current level in the planes data structure
        // p->pOrderInt[i] is the original level in the planes data structure
        // p->pMapToDdVarsOrig[i] is the variable, into which we remap when we construct the BDD from planes
        // p->pMapToDdVarsOrig[ p->pOrderInt[i] ] is the original BDD variable corresponding to this level
        // Therefore, p->pOrder[ p->pMapToDdVarsFinal[i] ] = p->pMapToDdVarsOrig[ p->pOrderInt[i] ]
        // creates the permutation, which remaps the resulting BDD variable into the original BDD variable
        for ( i = 0; i < p->nSupp; i++ )
            p->pOrder[ p->pMapToDdVarsFinal[i] ] = p->pMapToDdVarsOrig[ p->pOrderInt[i] ]; 
    }

    if ( p->fVerify )
    {
        int fVerification;
        DdNode * FuncRemapped;
        int * pOrder;

        if ( p->pOrder == NULL )
        {
            pOrder = ABC_ALLOC( int, p->nSupp );
            for ( i = 0; i < p->nSupp; i++ )
                pOrder[ p->pMapToDdVarsFinal[i] ] = p->pMapToDdVarsOrig[ p->pOrderInt[i] ]; 
        }
        else
            pOrder = p->pOrder;

        fVerification = 1;
        for ( i = 0; i < nFuncs; i++ )
        {
            // verify the result
            if ( p->fThisIsAdd )
                FuncRemapped = Cudd_addPermute( dd, FuncsRes[i], pOrder );
            else
                FuncRemapped = Cudd_bddPermute( dd, FuncsRes[i], pOrder );
            Cudd_Ref( FuncRemapped );

            if ( FuncRemapped != Funcs[i] )
            {
                fVerification = 0;
                printf( "REO: Internal verification has failed!\n" );
                fflush( stdout );
            }
            Cudd_RecursiveDeref( dd, FuncRemapped );
        }
        if ( fVerification )
            printf( "REO: Internal verification is okay!\n" );

        if ( p->pOrder == NULL )
            ABC_FREE( pOrder );
    }

    // recycle the data structure
    for ( i = 0; i <= p->nSupp; i++ )
        reoUnitsRecycleUnitList( p, p->pPlanes + i );
}

void reoReorderSift

(

reo_man *

p

)

DECLARATIONS ///.

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

FileName [reoSift.c]

PackageName [REO: A specialized DD reordering engine.]

Synopsis [Implementation of the sifting algorihtm.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - October 15, 2002.]

Revision [

Id:

reoSift.c,v 1.0 2002/15/10 03:00:00 alanmi Exp

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

Synopsis [Implements the variable sifting algorithm.]

Description [Performs a sequence of adjacent variable swaps known as "sifting". Uses the cost functions determined by the flag.]

SideEffects []

SeeAlso []

Definition at line 44 of file reoSift.c.

{
    double CostCurrent;  // the cost of the current permutation
    double CostLimit;    // the maximum increase in cost that can be tolerated
    double CostBest;     // the best cost
    int BestQ;           // the best position
    int VarCurrent;      // the current variable to move   
    int q;               // denotes the current position of the variable
    int c;               // performs the loops over variables until all of them are sifted
    int v;               // used for other purposes

    assert( p->nSupp > 0 );

    // set the current cost depending on the minimization criteria
    if ( p->fMinWidth )
        CostCurrent = p->nWidthCur;
    else if ( p->fMinApl )
        CostCurrent = p->nAplCur;
    else
        CostCurrent = p->nNodesCur;

    // find the upper bound on tbe cost growth
    CostLimit = 1 + (int)(REO_REORDER_LIMIT * CostCurrent);

    // perform sifting for each of p->nSupp variables
    for ( c = 0; c < p->nSupp; c++ )
    {
        // select the current variable to be the one with the largest number of nodes that is not sifted yet
        VarCurrent = -1;
        CostBest   = -1.0;
        for ( v = 0; v < p->nSupp; v++ )
        {
            p->pVarCosts[v] = REO_HIGH_VALUE;
            if ( !p->pPlanes[v].fSifted )
            {
//              VarCurrent = v;
//              if ( CostBest < p->pPlanes[v].statsCost )
                if ( CostBest < p->pPlanes[v].statsNodes )
                {
//                  CostBest   = p->pPlanes[v].statsCost;
                    CostBest   = p->pPlanes[v].statsNodes;
                    VarCurrent = v;
                }

            }
        }
        assert( VarCurrent != -1 );
        // mark this variable as sifted
        p->pPlanes[VarCurrent].fSifted = 1;

        // set the current value
        p->pVarCosts[VarCurrent] = CostCurrent;

        // set the best cost
        CostBest = CostCurrent;
        BestQ    = VarCurrent; 

        // determine which way to move the variable first (up or down)
        // the rationale is that if we move the shorter way first
        // it is more likely that the best position will be found on the longer way
        // and the reverse movement (to take the best position) will be faster
        if ( VarCurrent < p->nSupp/2 ) // move up first, then down
        {
            // set the total cost on all levels above the current level
            p->pPlanes[0].statsCostAbove = 0;
            for ( v = 1; v <= VarCurrent; v++ )
                p->pPlanes[v].statsCostAbove = p->pPlanes[v-1].statsCostAbove + p->pPlanes[v-1].statsCost;
            // set the total cost on all levels below the current level
            p->pPlanes[p->nSupp].statsCostBelow = 0;
            for ( v = p->nSupp - 1; v >= VarCurrent; v-- )
                p->pPlanes[v].statsCostBelow = p->pPlanes[v+1].statsCostBelow + p->pPlanes[v+1].statsCost;

            assert( CostCurrent == p->pPlanes[VarCurrent].statsCostAbove + 
                                    p->pPlanes[VarCurrent].statsCost +
                                    p->pPlanes[VarCurrent].statsCostBelow );

            // move up
            for ( q = VarCurrent-1; q >= 0; q-- )
            {
                CostCurrent -= reoReorderSwapAdjacentVars( p, q, 1 );
                // now q points to the position of this var in the order
                p->pVarCosts[q] = CostCurrent;
                // update the lower bound (assuming that for level q+1 it is set correctly)
                p->pPlanes[q].statsCostBelow = p->pPlanes[q+1].statsCostBelow + p->pPlanes[q+1].statsCost;
                // check the upper bound
                if ( CostCurrent >= CostLimit )
                    break;
                // check the lower bound
                if ( p->pPlanes[q].statsCostBelow + (REO_QUAL_PAR-1)*p->pPlanes[q].statsCostAbove/REO_QUAL_PAR >= CostBest )
                    break;
                // update the best cost
                if ( CostBest > CostCurrent )
                {
                    CostBest = CostCurrent;
                    BestQ    = q;
                    // adjust node limit
                    CostLimit = ddMin( CostLimit, 1 + (int)(REO_REORDER_LIMIT * CostCurrent) );
                }

                // when we are reordering for width or APL, it may happen that
                // the number of nodes has grown above certain limit,
                // in which case we have to resize the data structures
                if ( p->fMinWidth || p->fMinApl )
                {
                    if ( p->nNodesCur >= 2 * p->nNodesMaxAlloc )
                    {
//                      printf( "Resizing data structures. Old size = %6d. New size = %6d.\n",  p->nNodesMaxAlloc, p->nNodesCur );
                        reoResizeStructures( p, 0, p->nNodesCur, 0 );
                    }
                }
            }
            // fix the plane index
            if ( q == -1 )
                q++;
            // now p points to the position of this var in the order

            // move down
            for ( ; q < p->nSupp-1; )
            {
                CostCurrent -= reoReorderSwapAdjacentVars( p, q, 0 );
                q++;    // change q to point to the position of this var in the order
                // sanity check: the number of nodes on the back pass should be the same
                if ( p->pVarCosts[q] != REO_HIGH_VALUE && fabs( p->pVarCosts[q] - CostCurrent ) > REO_COST_EPSILON )
                    printf("reoReorderSift(): Error! On the backward move, the costs are different.\n");
                p->pVarCosts[q] = CostCurrent;
                // update the lower bound (assuming that for level q-1 it is set correctly)
                p->pPlanes[q].statsCostAbove = p->pPlanes[q-1].statsCostAbove + p->pPlanes[q-1].statsCost;
                // check the bounds only if the variable already reached its previous position
                if ( q >= BestQ )
                {
                    // check the upper bound
                    if ( CostCurrent >= CostLimit )
                        break;
                    // check the lower bound
                    if ( p->pPlanes[q].statsCostAbove + (REO_QUAL_PAR-1)*p->pPlanes[q].statsCostBelow/REO_QUAL_PAR >= CostBest )
                        break;
                }
                // update the best cost
                if ( CostBest >= CostCurrent )
                {
                    CostBest = CostCurrent;
                    BestQ    = q;
                    // adjust node limit
                    CostLimit = ddMin( CostLimit, 1 + (int)(REO_REORDER_LIMIT * CostCurrent) );
                }

                // when we are reordering for width or APL, it may happen that
                // the number of nodes has grown above certain limit,
                // in which case we have to resize the data structures
                if ( p->fMinWidth || p->fMinApl )
                {
                    if ( p->nNodesCur >= 2 * p->nNodesMaxAlloc )
                    {
//                      printf( "Resizing data structures. Old size = %6d. New size = %6d.\n",  p->nNodesMaxAlloc, p->nNodesCur );
                        reoResizeStructures( p, 0, p->nNodesCur, 0 );
                    }
                }
            }
            // move the variable up from the given position (q) to the best position (BestQ)
            assert( q >= BestQ );
            for ( ; q > BestQ; q-- )
            {
                CostCurrent -= reoReorderSwapAdjacentVars( p, q-1, 1 );
                // sanity check: the number of nodes on the back pass should be the same
                if ( fabs( p->pVarCosts[q-1] - CostCurrent ) > REO_COST_EPSILON )
                {
                    printf("reoReorderSift():  Error! On the return move, the costs are different.\n" );
                    fflush(stdout);
                }
            }
        }
        else // move down first, then up
        {
            // set the current number of nodes on all levels above the given level
            p->pPlanes[0].statsCostAbove = 0;
            for ( v = 1; v <= VarCurrent; v++ )
                p->pPlanes[v].statsCostAbove = p->pPlanes[v-1].statsCostAbove + p->pPlanes[v-1].statsCost;
            // set the current number of nodes on all levels below the given level
            p->pPlanes[p->nSupp].statsCostBelow = 0;
            for ( v = p->nSupp - 1; v >= VarCurrent; v-- )
                p->pPlanes[v].statsCostBelow = p->pPlanes[v+1].statsCostBelow + p->pPlanes[v+1].statsCost;
            
            assert( CostCurrent == p->pPlanes[VarCurrent].statsCostAbove + 
                                    p->pPlanes[VarCurrent].statsCost +
                                    p->pPlanes[VarCurrent].statsCostBelow );

            // move down
            for ( q = VarCurrent; q < p->nSupp-1; )
            {
                CostCurrent -= reoReorderSwapAdjacentVars( p, q, 0 );
                q++;    // change q to point to the position of this var in the order
                p->pVarCosts[q] = CostCurrent;
                // update the lower bound (assuming that for level q-1 it is set correctly)
                p->pPlanes[q].statsCostAbove = p->pPlanes[q-1].statsCostAbove + p->pPlanes[q-1].statsCost;
                // check the upper bound
                if ( CostCurrent >= CostLimit )
                    break;
                // check the lower bound
                if ( p->pPlanes[q].statsCostAbove + (REO_QUAL_PAR-1)*p->pPlanes[q].statsCostBelow/REO_QUAL_PAR >= CostBest )
                    break;
                // update the best cost
                if ( CostBest > CostCurrent )
                {
                    CostBest = CostCurrent;
                    BestQ    = q;
                    // adjust node limit
                    CostLimit = ddMin( CostLimit, 1 + (int)(REO_REORDER_LIMIT * CostCurrent) );
                }

                // when we are reordering for width or APL, it may happen that
                // the number of nodes has grown above certain limit,
                // in which case we have to resize the data structures
                if ( p->fMinWidth || p->fMinApl )
                {
                    if ( p->nNodesCur >= 2 * p->nNodesMaxAlloc )
                    {
//                      printf( "Resizing data structures. Old size = %6d. New size = %6d.\n",  p->nNodesMaxAlloc, p->nNodesCur );
                        reoResizeStructures( p, 0, p->nNodesCur, 0 );
                    }
                }
            }

            // move up
            for ( --q; q >= 0; q-- )
            {
                CostCurrent -= reoReorderSwapAdjacentVars( p, q, 1 );
                // now q points to the position of this var in the order
                // sanity check: the number of nodes on the back pass should be the same
                if ( p->pVarCosts[q] != REO_HIGH_VALUE && fabs( p->pVarCosts[q] - CostCurrent ) > REO_COST_EPSILON )
                    printf("reoReorderSift(): Error! On the backward move, the costs are different.\n");
                p->pVarCosts[q] = CostCurrent;
                // update the lower bound (assuming that for level q+1 it is set correctly)
                p->pPlanes[q].statsCostBelow = p->pPlanes[q+1].statsCostBelow + p->pPlanes[q+1].statsCost;
                // check the bounds only if the variable already reached its previous position
                if ( q <= BestQ )
                {
                    // check the upper bound
                    if ( CostCurrent >= CostLimit )
                        break;
                    // check the lower bound
                    if ( p->pPlanes[q].statsCostBelow + (REO_QUAL_PAR-1)*p->pPlanes[q].statsCostAbove/REO_QUAL_PAR >= CostBest )
                        break;
                }
                // update the best cost
                if ( CostBest >= CostCurrent )
                {
                    CostBest = CostCurrent;
                    BestQ    = q;
                    // adjust node limit
                    CostLimit = ddMin( CostLimit, 1 + (int)(REO_REORDER_LIMIT * CostCurrent) );
                }

                // when we are reordering for width or APL, it may happen that
                // the number of nodes has grown above certain limit,
                // in which case we have to resize the data structures
                if ( p->fMinWidth || p->fMinApl )
                {
                    if ( p->nNodesCur >= 2 * p->nNodesMaxAlloc )
                    {
//                      printf( "Resizing data structures. Old size = %6d. New size = %6d.\n",  p->nNodesMaxAlloc, p->nNodesCur );
                        reoResizeStructures( p, 0, p->nNodesCur, 0 );
                    }
                }
            }
            // fix the plane index
            if ( q == -1 )
                q++;
            // now q points to the position of this var in the order
            // move the variable down from the given position (q) to the best position (BestQ)
            assert( q <= BestQ );
            for ( ; q < BestQ; q++ )
            {
                CostCurrent -= reoReorderSwapAdjacentVars( p, q, 0 );
                // sanity check: the number of nodes on the back pass should be the same
                if ( fabs( p->pVarCosts[q+1] - CostCurrent ) > REO_COST_EPSILON )
                {
                    printf("reoReorderSift(): Error! On the return move, the costs are different.\n" );
                    fflush(stdout);
                }
            }
        }
        assert( fabs( CostBest - CostCurrent ) < REO_COST_EPSILON );

        // update the cost 
        if ( p->fMinWidth )
            p->nWidthCur = (int)CostBest;
        else if ( p->fMinApl )
            p->nAplCur = CostCurrent;
        else
            p->nNodesCur = (int)CostBest;
    }

    // remove the sifted attributes if any
    for ( v = 0; v < p->nSupp; v++ )
        p->pPlanes[v].fSifted = 0;
}

double reoReorderSwapAdjacentVars	(	reo_man *	p,
		int	lev0,
		int	fMovingUp
	)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description [Takes the level (lev0) of the plane, which should be swapped with the next plane. Returns the gain using the current cost function.]

SideEffects []

SeeAlso []

Definition at line 46 of file reoSwap.c.

{
    // the levels in the decision diagram
    int lev1 = lev0 + 1, lev2 = lev0 + 2;
    // the new nodes on lev0
    reo_unit * pLoop, * pUnit;
    // the new nodes on lev1
    reo_unit * pNewPlane20 = NULL, * pNewPlane21 = NULL; // Suppress "might be used uninitialized"
        reo_unit * pNewPlane20R;
    reo_unit * pUnitE, * pUnitER, * pUnitT;
    // the nodes below lev1
    reo_unit * pNew1E, * pNew1T, * pNew2E, * pNew2T;
    reo_unit * pNew1ER, * pNew2ER;
    // the old linked lists
    reo_unit * pListOld0 = p->pPlanes[lev0].pHead;
    reo_unit * pListOld1 = p->pPlanes[lev1].pHead;
    // working planes and one more temporary plane
    reo_unit * pListNew0 = NULL, ** ppListNew0 = &pListNew0;
    reo_unit * pListNew1 = NULL, ** ppListNew1 = &pListNew1; 
    reo_unit * pListTemp = NULL, ** ppListTemp = &pListTemp; 
    // various integer variables
    int fComp, fCompT, fFound, HKey, fInteract, temp, c;
        int nWidthCofs = -1; // Suppress "might be used uninitialized"
    // statistical variables
    int nNodesUpMovedDown  = 0;
    int nNodesDownMovedUp  = 0;
    int nNodesUnrefRemoved = 0;
    int nNodesUnrefAdded   = 0;
    int nWidthReduction    = 0;
    double AplWeightTotalLev0 = 0.0; // Suppress "might be used uninitialized"
    double AplWeightTotalLev1 = 0.0; // Suppress "might be used uninitialized"
    double AplWeightHalf      = 0.0; // Suppress "might be used uninitialized"
    double AplWeightPrev      = 0.0; // Suppress "might be used uninitialized"
    double AplWeightAfter     = 0.0; // Suppress "might be used uninitialized"
    double nCostGain;     

    // set the old lists
    assert( lev0 >= 0 && lev1 < p->nSupp );
    pListOld0 = p->pPlanes[lev0].pHead;
    pListOld1 = p->pPlanes[lev1].pHead;

    // make sure the planes have nodes
    assert( p->pPlanes[lev0].statsNodes && p->pPlanes[lev1].statsNodes );
    assert( pListOld0 && pListOld1 );

    if ( p->fMinWidth )
    {
        // verify that the width parameters are set correctly
        reoProfileWidthVerifyLevel( p->pPlanes + lev0, lev0 );
        reoProfileWidthVerifyLevel( p->pPlanes + lev1, lev1 );
        // start the storage for cofactors
        nWidthCofs = 0;
    }
    else if ( p->fMinApl )
    {
        AplWeightPrev      = p->nAplCur;
        AplWeightAfter     = p->nAplCur;
        AplWeightTotalLev0 = 0.0;
        AplWeightTotalLev1 = 0.0;
    }

    // check if the planes interact
    fInteract = 0; // assume that they do not interact
    for ( pUnit = pListOld0; pUnit; pUnit = pUnit->Next )
    {
        if ( pUnit->pT->lev == lev1 || Unit_Regular(pUnit->pE)->lev == lev1 )
        {
            fInteract = 1;
            break;
        }
        // change the level now, this is done for efficiency reasons
        pUnit->lev = lev1;
    }

    // set the new signature for hashing
    p->nSwaps++;
    if ( !fInteract )
//  if ( 0 )
    {
        // perform the swap without interaction
        p->nNISwaps++;

        // change the levels
        if ( p->fMinWidth )
        {
            // go through the current lower level, which will become upper
            for ( pUnit = pListOld1; pUnit; pUnit = pUnit->Next )
            {
                pUnit->lev = lev0;

                pUnitER = Unit_Regular(pUnit->pE);
                if ( pUnitER->TopRef > lev0 )
                {
                    if ( pUnitER->Sign != p->nSwaps )
                    {
                        if ( pUnitER->TopRef == lev2 )
                        {
                            pUnitER->TopRef = lev1;
                            nWidthReduction--;
                        }
                        else
                        {
                            assert( pUnitER->TopRef == lev1 );
                        }
                        pUnitER->Sign   = p->nSwaps;
                    }
                }

                pUnitT  = pUnit->pT;
                if ( pUnitT->TopRef > lev0 )
                {
                    if ( pUnitT->Sign != p->nSwaps )
                    {
                        if ( pUnitT->TopRef == lev2 )
                        {
                            pUnitT->TopRef = lev1;
                            nWidthReduction--;
                        }
                        else
                        {
                            assert( pUnitT->TopRef == lev1 );
                        }
                        pUnitT->Sign   = p->nSwaps;
                    }
                }

            }

            // go through the current upper level, which will become lower
            for ( pUnit = pListOld0; pUnit; pUnit = pUnit->Next )
            {
                pUnit->lev = lev1;

                pUnitER = Unit_Regular(pUnit->pE);
                if ( pUnitER->TopRef > lev0 )
                {
                    if ( pUnitER->Sign != p->nSwaps )
                    {
                        assert( pUnitER->TopRef == lev1 );
                        pUnitER->TopRef = lev2;
                        pUnitER->Sign   = p->nSwaps;
                        nWidthReduction++;
                    }
                }

                pUnitT  = pUnit->pT;
                if ( pUnitT->TopRef > lev0 )
                {
                    if ( pUnitT->Sign != p->nSwaps )
                    {
                        assert( pUnitT->TopRef == lev1 );
                        pUnitT->TopRef = lev2;
                        pUnitT->Sign   = p->nSwaps;
                        nWidthReduction++;
                    }
                }
            }
        }
        else
        {
//          for ( pUnit = pListOld0; pUnit; pUnit = pUnit->Next )
//              pUnit->lev = lev1;
            for ( pUnit = pListOld1; pUnit; pUnit = pUnit->Next )
                pUnit->lev = lev0;
        }

        // set the new linked lists, which will be attached to the planes
        pListNew0 = pListOld1;
        pListNew1 = pListOld0;

        if ( p->fMinApl )
        {
            AplWeightTotalLev0 = p->pPlanes[lev1].statsCost;
            AplWeightTotalLev1 = p->pPlanes[lev0].statsCost;
        }
        
        // set the changes in terms of nodes
        nNodesUpMovedDown = p->pPlanes[lev0].statsNodes; 
        nNodesDownMovedUp = p->pPlanes[lev1].statsNodes; 
        goto finish;
    }
    p->Signature++;


    // two-variable swap is done in three easy steps
    // previously I thought that steps (1) and (2) can be merged into one step
    // now it is clear that this cannot be done without changing a lot of other stuff...

    // (1) walk through the upper level, find units without cofactors in the lower level 
    //     and move them to the new lower level (while adding to the cache)
    // (2) walk through the uppoer level, and tranform all the remaning nodes 
    //     while employing cache for the new lower level
    // (3) walk through the old lower level, find those nodes whose ref counters are not zero, 
    //     and move them to the new uppoer level, free other nodes

    // (1) walk through the upper level, find units without cofactors in the lower level 
    //     and move them to the new lower level (while adding to the cache)
    for ( pLoop = pListOld0; pLoop; )
    {
        pUnit = pLoop;
        pLoop = pLoop->Next;

        pUnitE  = pUnit->pE;
        pUnitER = Unit_Regular(pUnitE);
        pUnitT  = pUnit->pT;

        if ( pUnitER->lev != lev1 && pUnitT->lev != lev1 )
        {
            //                before                        after
            //
            //                 <p1>                                 .
            //              0 /    \ 1                              .
            //               /      \                               .
            //              /        \                              .
            //             /          \                     <p2n>   .
            //            /            \                  0 /  \ 1  .
            //           /              \                  /    \   .
            //          /                \                /      \  .
            //         F0                F1              F0      F1

            // move to plane-2-new
            // nothing changes in the process (cofactors, ref counter, APL weight)
            pUnit->lev = lev1;
            AddToLinkedList( ppListNew1, pUnit );
            if ( p->fMinApl )
                AplWeightTotalLev1 += pUnit->Weight;

            // add to cache - find the cell with different signature (not the current one!)
            for (  HKey = hashKey3(p->Signature, pUnitE, pUnitT, p->nTableSize);
                   p->HTable[HKey].Sign == p->Signature;
                   HKey = (HKey+1) % p->nTableSize );
            assert( p->HTable[HKey].Sign != p->Signature );
            p->HTable[HKey].Sign = p->Signature;
            p->HTable[HKey].Arg1 = pUnitE;
            p->HTable[HKey].Arg2 = pUnitT;
            p->HTable[HKey].Arg3 = pUnit;

            nNodesUpMovedDown++;

            if ( p->fMinWidth )
            {
                // update the cofactors's top ref
                if ( pUnitER->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels
                {
                    assert( pUnitER->TopRef == lev1 );
                    pUnitER->TopRefNew = lev2;
                    if ( pUnitER->Sign != p->nSwaps )
                    {
                        pUnitER->Sign      = p->nSwaps;  // set the current signature
                        p->pWidthCofs[ nWidthCofs++ ] = pUnitER;
                    }
                }
                if ( pUnitT->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels
                {
                    assert( pUnitT->TopRef == lev1 );
                    pUnitT->TopRefNew = lev2;
                    if ( pUnitT->Sign != p->nSwaps )
                    {
                        pUnitT->Sign      = p->nSwaps;  // set the current signature
                        p->pWidthCofs[ nWidthCofs++ ] = pUnitT;
                    }
                }
            }
        }
        else
        {
            // add to the temporary plane
            AddToLinkedList( ppListTemp, pUnit );
        }
    }


    // (2) walk through the uppoer level, and tranform all the remaning nodes 
    //     while employing cache for the new lower level
    for ( pLoop = pListTemp; pLoop; )
    {
        pUnit = pLoop;
        pLoop = pLoop->Next;

        pUnitE  = pUnit->pE;
        pUnitER = Unit_Regular(pUnitE);
        pUnitT  = pUnit->pT;
        fComp   = (int)(pUnitER != pUnitE);

        // count the amount of weight to reduce the APL of the children of this node
        if ( p->fMinApl )
            AplWeightHalf = 0.5 * pUnit->Weight;

        // determine what situation is this
        if ( pUnitER->lev == lev1 && pUnitT->lev == lev1 )
        {
            if ( fComp == 0 )
            {
                //                before                        after
                //
                //                 <p1>                          <p1n>              .
                //              0 /    \ 1                    0 /    \ 1            .
                //               /      \                      /      \             .
                //              /        \                    /        \            .
                //           <p2>        <p2>              <p2n>       <p2n>        .
                //        0 /   \ 1    0 /  \ 1          0 /  \ 1    0 /   \ 1      .
                //         /     \      /    \            /    \      /     \       .
                //        /       \    /      \          /      \    /       \      .
                //       F0       F1  F2      F3        F0      F2  F1       F3     .
                //                                 pNew1E   pNew1T  pNew2E   pNew2T
                //
                pNew1E = pUnitE->pE;   // F0
                pNew1T = pUnitT->pE;   // F2

                pNew2E = pUnitE->pT;   // F1
                pNew2T = pUnitT->pT;   // F3
            }
            else
            {
                //                before                        after
                //
                //                 <p1>                          <p1n>           .
                //              0 .    \ 1                    0 /    \ 1         .
                //               .      \                      /      \          .
                //              .        \                    /        \         .
                //           <p2>        <p2>              <p2n>       <p2n>     .
                //        0 /   \ 1    0 /  \ 1          0 .  \ 1    0 .   \ 1   .
                //         /     \      /    \            .    \      .     \    .
                //        /       \    /      \          .      \    .       \   .
                //       F0       F1  F2      F3        F0      F2  F1       F3  .
                //                                 pNew1E   pNew1T  pNew2E   pNew2T
                //
                pNew1E = Unit_Not(pUnitER->pE);  // F0
                pNew1T =          pUnitT->pE;    // F2

                pNew2E = Unit_Not(pUnitER->pT);  // F1
                pNew2T =          pUnitT->pT;    // F3
            }
            // subtract ref counters - on the level P2
            pUnitER->n--;
            pUnitT->n--;

            // mark the change in the APL weights
            if ( p->fMinApl )
            {
                pUnitER->Weight -= AplWeightHalf;
                pUnitT->Weight  -= AplWeightHalf;
                AplWeightAfter  -= pUnit->Weight;
            }
        }
        else if ( pUnitER->lev == lev1 )
        {
            if ( fComp == 0 )
            {
                //                before                        after
                //
                //                 <p1>                          <p1n>          .
                //              0 /    \ 1                    0 /    \ 1        .
                //               /      \                      /      \         .
                //              /        \                    /        \        .
                //           <p2>         \               <p2n>       <p2n>     .
                //        0 /   \ 1        \            0 /  \ 1    0 /   \ 1   .
                //         /     \          \            /    \      /     \    .
                //        /       \          \          /      \    /       \   .
                //       F0       F1         F3        F0      F3  F1       F3  .
                //                                 pNew1E   pNew1T  pNew2E   pNew2T
                //
                pNew1E = pUnitER->pE;     // F0
                pNew1T = pUnitT;          // F3

                pNew2E = pUnitER->pT;     // F1
                pNew2T = pUnitT;          // F3
            }
            else
            {
                //                before                        after
                //
                //                 <p1>                          <p1n>          .
                //              0 .    \ 1                    0 /    \ 1        .
                //               .      \                      /      \         .
                //              .        \                    /        \        .
                //           <p2>         \                <p2n>       <p2n>    .
                //        0 /   \ 1        \            0 .  \ 1    0 .   \ 1   .
                //         /     \          \            .    \      .     \    .
                //        /       \          \          .      \    .       \   .
                //       F0       F1         F3        F0      F3  F1       F3  .
                //                                 pNew1E   pNew1T  pNew2E   pNew2T
                //
                pNew1E = Unit_Not(pUnitER->pE);  // F0
                pNew1T =          pUnitT;        // F3

                pNew2E = Unit_Not(pUnitER->pT);  // F1
                pNew2T =          pUnitT;        // F3
            }
            // subtract ref counter - on the level P2
            pUnitER->n--;
            // subtract ref counter - on other levels
            pUnitT->n--;  ///

            // mark the change in the APL weights
            if ( p->fMinApl )
            {
                pUnitER->Weight -= AplWeightHalf;
                AplWeightAfter  -= AplWeightHalf;
            }
        }
        else if ( pUnitT->lev == lev1 )
        {
            //                before                        after
            //
            //                 <p1>                          <p1n>           .
            //              0 /    \ 1                    0 /    \ 1         .
            //               /      \                      /      \          .
            //              /        \                    /        \         .
            //             /         <p2>              <p2n>       <p2n>     .
            //            /       0 /   \ 1          0 /  \ 1    0 /   \ 1   .
            //           /         /     \            /    \      /     \    .
            //          /         /       \          /      \    /       \   .
            //         F0        F2       F3        F0      F2  F0       F3  .
            //                                 pNew1E   pNew1T  pNew2E   pNew2T
            //
            pNew1E =     pUnitE;    // F0
            pNew1T = pUnitT->pE;    // F2

            pNew2E =     pUnitE;    // F0
            pNew2T = pUnitT->pT;    // F3

            // subtract incoming edge counter - on the level P2
            pUnitT->n--;
            // subtract ref counter - on other levels
            pUnitER->n--;  ///

            // mark the change in the APL weights
            if ( p->fMinApl )
            {
                pUnitT->Weight  -= AplWeightHalf;
                AplWeightAfter  -= AplWeightHalf;
            }
        }
        else 
        {
            assert( 0 ); // should never happen
        }


        // consider all the cases except the last one
        if ( pNew1E == pNew1T )
        {
            pNewPlane20 = pNew1T;
            
            if ( p->fMinWidth )
            {
                // update the cofactors's top ref
                if ( pNew1T->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels
                {
                    pNew1T->TopRefNew = lev1;
                    if ( pNew1T->Sign  != p->nSwaps )
                    {
                        pNew1T->Sign      = p->nSwaps;  // set the current signature
                        p->pWidthCofs[ nWidthCofs++ ] = pNew1T;
                    }
                }
            }
        }
        else
        {
            // pNew1T can be complemented
            fCompT = Cudd_IsComplement(pNew1T);
            if ( fCompT )
            {
                pNew1E = Unit_Not(pNew1E);
                pNew1T = Unit_Not(pNew1T);
            }

            // check the hash-table 
            fFound = 0;
            for (  HKey = hashKey3(p->Signature, pNew1E, pNew1T, p->nTableSize);
                   p->HTable[HKey].Sign == p->Signature;
                   HKey = (HKey+1) % p->nTableSize )
            if ( p->HTable[HKey].Arg1 == pNew1E && p->HTable[HKey].Arg2 == pNew1T )
            { // the entry is present 
                // assign this entry
                pNewPlane20 = p->HTable[HKey].Arg3;
                assert( pNewPlane20->lev == lev1 );
                fFound = 1;
                p->HashSuccess++;
                break;
            }

            if ( !fFound )
            { // create the new entry
                pNewPlane20 = reoUnitsGetNextUnit( p ); // increments the unit counter
                pNewPlane20->pE  = pNew1E;
                pNewPlane20->pT  = pNew1T;
                pNewPlane20->n   = 0;       // ref will be added later
                pNewPlane20->lev = lev1; 
                if ( p->fMinWidth )
                {
                    pNewPlane20->TopRef = lev1;
                    pNewPlane20->Sign   = 0;
                }
                // set the weight of this node
                if ( p->fMinApl )
                    pNewPlane20->Weight = 0.0;

                // increment ref counters of children
                pNew1ER = Unit_Regular(pNew1E);
                pNew1ER->n++;  //
                pNew1T->n++;   //

                // insert into the data structure
                AddToLinkedList( ppListNew1, pNewPlane20 );

                // add this entry to cache
                assert( p->HTable[HKey].Sign != p->Signature );
                p->HTable[HKey].Sign = p->Signature;
                p->HTable[HKey].Arg1 = pNew1E;
                p->HTable[HKey].Arg2 = pNew1T;
                p->HTable[HKey].Arg3 = pNewPlane20;

                nNodesUnrefAdded++;
                        
                if ( p->fMinWidth )
                {
                    // update the cofactors's top ref
                    if ( pNew1ER->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels
                    {
                        if ( pNew1ER->Sign != p->nSwaps )
                        {
                            pNew1ER->TopRefNew = lev2;
                            if ( pNew1ER->Sign != p->nSwaps )
                            {
                                pNew1ER->Sign      = p->nSwaps;  // set the current signature
                                p->pWidthCofs[ nWidthCofs++ ] = pNew1ER;
                            }
                        }
                        // otherwise the level is already set correctly
                        else
                        {
                            assert( pNew1ER->TopRefNew == lev1 || pNew1ER->TopRefNew == lev2 );
                        }
                    }
                    // update the cofactors's top ref
                    if ( pNew1T->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels
                    {
                        if ( pNew1T->Sign != p->nSwaps )
                        {
                            pNew1T->TopRefNew = lev2;
                            if ( pNew1T->Sign  != p->nSwaps )
                            {
                                pNew1T->Sign      = p->nSwaps;  // set the current signature
                                p->pWidthCofs[ nWidthCofs++ ] = pNew1T;
                            }
                        }
                        // otherwise the level is already set correctly
                        else
                        {
                            assert( pNew1T->TopRefNew == lev1 || pNew1T->TopRefNew == lev2 );
                        }
                    }
                }
            }

            if ( p->fMinApl )
            {
                // increment the weight of this node
                pNewPlane20->Weight += AplWeightHalf;
                // mark the change in the APL weight
                AplWeightAfter      += AplWeightHalf;
                // update the total weight of this level
                AplWeightTotalLev1  += AplWeightHalf;
            }

            if ( fCompT )
                pNewPlane20 = Unit_Not(pNewPlane20);
        }

        if ( pNew2E == pNew2T )
        {
            pNewPlane21 = pNew2T;
            
            if ( p->fMinWidth )
            {
                // update the cofactors's top ref
                if ( pNew2T->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels
                {
                    pNew2T->TopRefNew = lev1;
                    if ( pNew2T->Sign != p->nSwaps )
                    {
                        pNew2T->Sign      = p->nSwaps;  // set the current signature
                        p->pWidthCofs[ nWidthCofs++ ] = pNew2T;
                    }
                }
            }
        }
        else
        {
            assert( !Cudd_IsComplement(pNew2T) );

            // check the hash-table
            fFound = 0;
            for (  HKey = hashKey3(p->Signature, pNew2E, pNew2T, p->nTableSize);
                   p->HTable[HKey].Sign == p->Signature;
                   HKey = (HKey+1) % p->nTableSize )
            if ( p->HTable[HKey].Arg1 == pNew2E && p->HTable[HKey].Arg2 == pNew2T )
            { // the entry is present 
                // assign this entry
                pNewPlane21 = p->HTable[HKey].Arg3;
                assert( pNewPlane21->lev == lev1 );
                fFound = 1;
                p->HashSuccess++;
                break;
            }

            if ( !fFound )
            { // create the new entry
                pNewPlane21 = reoUnitsGetNextUnit( p ); // increments the unit counter
                pNewPlane21->pE  = pNew2E;
                pNewPlane21->pT  = pNew2T;
                pNewPlane21->n   = 0;       // ref will be added later
                pNewPlane21->lev = lev1; 
                if ( p->fMinWidth )
                {
                    pNewPlane21->TopRef = lev1;
                    pNewPlane21->Sign   = 0;
                }
                // set the weight of this node
                if ( p->fMinApl )
                    pNewPlane21->Weight = 0.0;

                // increment ref counters of children
                pNew2ER = Unit_Regular(pNew2E);
                pNew2ER->n++; //
                pNew2T->n++;  //

                // insert into the data structure
//              reoUnitsAddUnitToPlane( &P2new, pNewPlane21 );
                AddToLinkedList( ppListNew1, pNewPlane21 );

                // add this entry to cache
                assert( p->HTable[HKey].Sign != p->Signature );
                p->HTable[HKey].Sign = p->Signature;
                p->HTable[HKey].Arg1 = pNew2E;
                p->HTable[HKey].Arg2 = pNew2T;
                p->HTable[HKey].Arg3 = pNewPlane21;

                nNodesUnrefAdded++;

                        
                if ( p->fMinWidth )
                {
                    // update the cofactors's top ref
                    if ( pNew2ER->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels
                    {
                        if ( pNew2ER->Sign != p->nSwaps )
                        {
                            pNew2ER->TopRefNew = lev2;
                            if ( pNew2ER->Sign != p->nSwaps )
                            {
                                pNew2ER->Sign      = p->nSwaps;  // set the current signature
                                p->pWidthCofs[ nWidthCofs++ ] = pNew2ER;
                            }
                        }
                        // otherwise the level is already set correctly
                        else
                        {
                            assert( pNew2ER->TopRefNew == lev1 || pNew2ER->TopRefNew == lev2 );
                        }
                    }
                    // update the cofactors's top ref
                    if ( pNew2T->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels
                    {
                        if ( pNew2T->Sign != p->nSwaps )
                        {
                            pNew2T->TopRefNew = lev2;
                            if ( pNew2T->Sign != p->nSwaps )
                            {
                                pNew2T->Sign      = p->nSwaps;  // set the current signature
                                p->pWidthCofs[ nWidthCofs++ ] = pNew2T;
                            }
                        }
                        // otherwise the level is already set correctly
                        else
                        {
                            assert( pNew2T->TopRefNew == lev1 || pNew2T->TopRefNew == lev2 );
                        }
                    }
                }
            }

            if ( p->fMinApl )
            {
                // increment the weight of this node
                pNewPlane21->Weight += AplWeightHalf;
                // mark the change in the APL weight
                AplWeightAfter      += AplWeightHalf;
                // update the total weight of this level
                AplWeightTotalLev1  += AplWeightHalf;
            }
        }
        // in all cases, the node will be added to the plane-1
        // this should be the same node (pUnit) as was originally there
        // because it is referenced by the above nodes

        assert( !Cudd_IsComplement(pNewPlane21) );
        // should be the case; otherwise reordering is not a local operation

        pUnit->pE  = pNewPlane20;
        pUnit->pT  = pNewPlane21;
        assert( pUnit->lev == lev0 ); 
        // reference counter remains the same; the APL weight remains the same

        // increment ref counters of children
        pNewPlane20R = Unit_Regular(pNewPlane20);
        pNewPlane20R->n++; ///
        pNewPlane21->n++;  ///

        // insert into the data structure
        AddToLinkedList( ppListNew0, pUnit );
        if ( p->fMinApl )
            AplWeightTotalLev0 += pUnit->Weight;
    }

    // (3) walk through the old lower level, find those nodes whose ref counters are not zero, 
    //     and move them to the new uppoer level, free other nodes
    for ( pLoop = pListOld1; pLoop; )
    {
        pUnit = pLoop;
        pLoop = pLoop->Next;
        if ( pUnit->n )
        { 
            assert( !p->fMinApl || pUnit->Weight > 0.0 );
            // the node should be added to the new level
            // no need to check the hash table
            pUnit->lev = lev0;
            AddToLinkedList( ppListNew0, pUnit );
            if ( p->fMinApl )
                AplWeightTotalLev0 += pUnit->Weight;

            nNodesDownMovedUp++;

            if ( p->fMinWidth )
            {
                pUnitER = Unit_Regular(pUnit->pE);
                pUnitT  = pUnit->pT;

                // update the cofactors's top ref
                if ( pUnitER->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels
                {
                    pUnitER->TopRefNew = lev1;
                    if ( pUnitER->Sign != p->nSwaps )
                    {
                        pUnitER->Sign      = p->nSwaps;  // set the current signature
                        p->pWidthCofs[ nWidthCofs++ ] = pUnitER;
                    }
                }
                if ( pUnitT->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels
                {
                    pUnitT->TopRefNew = lev1;
                    if ( pUnitT->Sign != p->nSwaps )
                    {
                        pUnitT->Sign      = p->nSwaps;  // set the current signature
                        p->pWidthCofs[ nWidthCofs++ ] = pUnitT;
                    }
                }
            }
        }
        else
        {
            assert( !p->fMinApl || pUnit->Weight == 0.0 );
            // decrement reference counters of children
            pUnitER = Unit_Regular(pUnit->pE);
            pUnitT  = pUnit->pT;
            pUnitER->n--;  ///
            pUnitT->n--;   ///
            // the node should be thrown away
            reoUnitsRecycleUnit( p, pUnit );
            nNodesUnrefRemoved++;
        }
    }

finish:

    // attach the new levels to the planes
    p->pPlanes[lev0].pHead = pListNew0;
    p->pPlanes[lev1].pHead = pListNew1;

    // swap the sift status
    temp                     = p->pPlanes[lev0].fSifted;
    p->pPlanes[lev0].fSifted = p->pPlanes[lev1].fSifted;
    p->pPlanes[lev1].fSifted = temp;

    // swap variables in the variable map
    if ( p->pOrderInt )
    {
        temp               = p->pOrderInt[lev0];
        p->pOrderInt[lev0] = p->pOrderInt[lev1];
        p->pOrderInt[lev1] = temp;
    }

    // adjust the node profile
    p->pPlanes[lev0].statsNodes  -= (nNodesUpMovedDown - nNodesDownMovedUp);
    p->pPlanes[lev1].statsNodes  -= (nNodesDownMovedUp - nNodesUpMovedDown) + nNodesUnrefRemoved - nNodesUnrefAdded;
    p->nNodesCur                 -=  nNodesUnrefRemoved - nNodesUnrefAdded;

    // adjust the node profile on this level
    if ( p->fMinWidth )
    {
        for ( c = 0; c < nWidthCofs; c++ )
        {
            if ( p->pWidthCofs[c]->TopRefNew < p->pWidthCofs[c]->TopRef )
            {
                p->pWidthCofs[c]->TopRef = p->pWidthCofs[c]->TopRefNew;
                nWidthReduction--;
            }
            else if ( p->pWidthCofs[c]->TopRefNew > p->pWidthCofs[c]->TopRef )
            {
                p->pWidthCofs[c]->TopRef = p->pWidthCofs[c]->TopRefNew;
                nWidthReduction++;
            }
        }
        // verify that the profile is okay
        reoProfileWidthVerifyLevel( p->pPlanes + lev0, lev0 );
        reoProfileWidthVerifyLevel( p->pPlanes + lev1, lev1 );

        // compute the total gain in terms of width
        nCostGain = (nNodesDownMovedUp - nNodesUpMovedDown + nNodesUnrefRemoved - nNodesUnrefAdded) + nWidthReduction;
        // adjust the width on this level
        p->pPlanes[lev1].statsWidth -= (int)nCostGain; 
        // set the cost
        p->pPlanes[lev1].statsCost   = p->pPlanes[lev1].statsWidth;
    }
    else if ( p->fMinApl )
    {
        // compute the total gain in terms of APL
        nCostGain = AplWeightPrev - AplWeightAfter;
        // make sure that the ALP is updated correctly
//      assert( p->pPlanes[lev0].statsCost + p->pPlanes[lev1].statsCost - nCostGain ==
//              AplWeightTotalLev0 + AplWeightTotalLev1 );              
        // adjust the profile 
        p->pPlanes[lev0].statsApl  = AplWeightTotalLev0;
        p->pPlanes[lev1].statsApl  = AplWeightTotalLev1;
        // set the cost
        p->pPlanes[lev0].statsCost = p->pPlanes[lev0].statsApl;
        p->pPlanes[lev1].statsCost = p->pPlanes[lev1].statsApl;
    }
    else
    {
        // compute the total gain in terms of the number of nodes
        nCostGain = nNodesUnrefRemoved - nNodesUnrefAdded;
        // adjust the profile (adjusted above)
        // set the cost
        p->pPlanes[lev0].statsCost   = p->pPlanes[lev0].statsNodes;
        p->pPlanes[lev1].statsCost   = p->pPlanes[lev1].statsNodes;
    }

    return nCostGain;
}

void reoResizeStructures	(	reo_man *	p,
		int	nDdVarsMax,
		int	nNodesMax,
		int	nFuncs
	)

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

Synopsis [Resizes the internal manager data structures.]

Description []

SideEffects []

SeeAlso []

Definition at line 269 of file reoCore.c.

{
    // resize data structures depending on the number of variables in the DD manager
    if ( p->nSuppAlloc == 0 )
    {
        p->pSupp             = ABC_ALLOC( int,        nDdVarsMax + 1 );
        p->pOrderInt         = ABC_ALLOC( int,        nDdVarsMax + 1 );
        p->pMapToPlanes      = ABC_ALLOC( int,        nDdVarsMax + 1 );
        p->pMapToDdVarsOrig  = ABC_ALLOC( int,        nDdVarsMax + 1 );
        p->pMapToDdVarsFinal = ABC_ALLOC( int,        nDdVarsMax + 1 );
        p->pPlanes           = ABC_CALLOC( reo_plane, nDdVarsMax + 1 );
        p->pVarCosts         = ABC_ALLOC( double,     nDdVarsMax + 1 );
        p->pLevelOrder       = ABC_ALLOC( int,        nDdVarsMax + 1 );
        p->nSuppAlloc        = nDdVarsMax + 1;
    }
    else if ( p->nSuppAlloc < nDdVarsMax )
    {
        ABC_FREE( p->pSupp );
        ABC_FREE( p->pOrderInt );
        ABC_FREE( p->pMapToPlanes );
        ABC_FREE( p->pMapToDdVarsOrig );
        ABC_FREE( p->pMapToDdVarsFinal );
        ABC_FREE( p->pPlanes );
        ABC_FREE( p->pVarCosts );
        ABC_FREE( p->pLevelOrder );

        p->pSupp             = ABC_ALLOC( int,        nDdVarsMax + 1 );
        p->pOrderInt         = ABC_ALLOC( int,        nDdVarsMax + 1 );
        p->pMapToPlanes      = ABC_ALLOC( int,        nDdVarsMax + 1 );
        p->pMapToDdVarsOrig  = ABC_ALLOC( int,        nDdVarsMax + 1 );
        p->pMapToDdVarsFinal = ABC_ALLOC( int,        nDdVarsMax + 1 );
        p->pPlanes           = ABC_CALLOC( reo_plane, nDdVarsMax + 1 );
        p->pVarCosts         = ABC_ALLOC( double,     nDdVarsMax + 1 );
        p->pLevelOrder       = ABC_ALLOC( int,        nDdVarsMax + 1 );
        p->nSuppAlloc        = nDdVarsMax + 1;
    }

    // resize the data structures depending on the number of nodes
    if ( p->nRefNodesAlloc == 0 )
    {
        p->nNodesMaxAlloc  = nNodesMax;
        p->nTableSize      = 3*nNodesMax + 1;
        p->nRefNodesAlloc  = 3*nNodesMax + 1;
        p->nMemChunksAlloc = (10*nNodesMax + 1)/REO_CHUNK_SIZE + 1;

        p->HTable          = ABC_CALLOC( reo_hash,  p->nTableSize );
        p->pRefNodes       = ABC_ALLOC( DdNode *,   p->nRefNodesAlloc );
        p->pWidthCofs      = ABC_ALLOC( reo_unit *, p->nRefNodesAlloc );
        p->pMemChunks      = ABC_ALLOC( reo_unit *, p->nMemChunksAlloc );
    }
    else if ( p->nNodesMaxAlloc < nNodesMax )
    {
        reo_unit ** pTemp;
        int nMemChunksAllocPrev = p->nMemChunksAlloc;

        p->nNodesMaxAlloc  = nNodesMax;
        p->nTableSize      = 3*nNodesMax + 1;
        p->nRefNodesAlloc  = 3*nNodesMax + 1;
        p->nMemChunksAlloc = (10*nNodesMax + 1)/REO_CHUNK_SIZE + 1;

        ABC_FREE( p->HTable );
        ABC_FREE( p->pRefNodes );
        ABC_FREE( p->pWidthCofs );
        p->HTable          = ABC_CALLOC( reo_hash,    p->nTableSize );
        p->pRefNodes       = ABC_ALLOC(  DdNode *,    p->nRefNodesAlloc );
        p->pWidthCofs      = ABC_ALLOC(  reo_unit *,  p->nRefNodesAlloc );
        // p->pMemChunks should be reallocated because it contains pointers currently in use
        pTemp              = ABC_ALLOC(  reo_unit *,  p->nMemChunksAlloc );
        memmove( pTemp, p->pMemChunks, sizeof(reo_unit *) * nMemChunksAllocPrev );
        ABC_FREE( p->pMemChunks );
        p->pMemChunks      = pTemp;
    }

    // resize the data structures depending on the number of functions
    if ( p->nTopsAlloc == 0 )
    {
        p->pTops      = ABC_ALLOC( reo_unit *, nFuncs );
        p->nTopsAlloc = nFuncs;
    }
    else if ( p->nTopsAlloc < nFuncs )
    {
        ABC_FREE( p->pTops );
        p->pTops      = ABC_ALLOC( reo_unit *, nFuncs );
        p->nTopsAlloc = nFuncs;
    }
}

reo_unit* reoTransferNodesToUnits_rec	(	reo_man *	p,
		DdNode *	F
	)

DECLARATIONS ///.

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

FileName [reoTransfer.c]

PackageName [REO: A specialized DD reordering engine.]

Synopsis [Transfering a DD from the CUDD manager into REO"s internal data structures and back.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - October 15, 2002.]

Revision [

Id:

reoTransfer.c,v 1.0 2002/15/10 03:00:00 alanmi Exp

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

Synopsis [Transfers the DD into the internal reordering data structure.]

Description [It is important that the hash table is lossless.]

SideEffects []

SeeAlso []

Definition at line 43 of file reoTransfer.c.

{
    DdManager * dd = p->dd;
    reo_unit * pUnit;
    int HKey = -1; // Suppress "might be used uninitialized"
        int fComp;
    
    fComp = Cudd_IsComplement(F);
    F = Cudd_Regular(F);

    // check the hash-table
    if ( F->ref != 1 )
    {
        // search cache - use linear probing
        for ( HKey = hashKey2(p->Signature,F,p->nTableSize); p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize )
            if ( p->HTable[HKey].Arg1 == (reo_unit *)F )
            {
                pUnit = p->HTable[HKey].Arg2;  
                assert( pUnit );
                // increment the edge counter
                pUnit->n++;
                return Unit_NotCond( pUnit, fComp );
            }
    }
    // the entry in not found in the cache
    
    // create a new entry
    pUnit         = reoUnitsGetNextUnit( p );
    pUnit->n      = 1;
    if ( cuddIsConstant(F) )
    {
        pUnit->lev    = REO_CONST_LEVEL;
        pUnit->pE     = (reo_unit*)(ABC_PTRUINT_T)(cuddV(F));
        pUnit->pT     = NULL;
        // check if the diagram that is being reordering has complement edges
        if ( F != dd->one )
            p->fThisIsAdd = 1;
        // insert the unit into the corresponding plane
        reoUnitsAddUnitToPlane( &(p->pPlanes[p->nSupp]), pUnit ); // increments the unit counter
    }
    else
    {
        pUnit->lev    = p->pMapToPlanes[F->index];
        pUnit->pE     = reoTransferNodesToUnits_rec( p, cuddE(F) );
        pUnit->pT     = reoTransferNodesToUnits_rec( p, cuddT(F) );
        // insert the unit into the corresponding plane
        reoUnitsAddUnitToPlane( &(p->pPlanes[pUnit->lev]), pUnit ); // increments the unit counter
    }

    // add to the hash table
    if ( F->ref != 1 )
    {
        // the next free entry is already found - it is pointed to by HKey
        // while we traversed the diagram, the hash entry to which HKey points,
        // might have been used. Make sure that its signature is different.
        for ( ; p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize );
        p->HTable[HKey].Sign = p->Signature;
        p->HTable[HKey].Arg1 = (reo_unit *)F;
        p->HTable[HKey].Arg2 = pUnit;
    }

    // increment the counter of nodes
    p->nNodesCur++;
    return Unit_NotCond( pUnit, fComp );
}

DdNode* reoTransferUnitsToNodes_rec	(	reo_man *	p,
		reo_unit *	pUnit
	)

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

Synopsis [Creates the DD from the internal reordering data structure.]

Description [It is important that the hash table is lossless.]

SideEffects []

SeeAlso []

Definition at line 120 of file reoTransfer.c.

{
    DdManager * dd = p->dd;
    DdNode * bRes, * E, * T;
    int HKey = -1; // Suppress "might be used uninitialized"
        int fComp;

    fComp = Cudd_IsComplement(pUnit);
    pUnit = Unit_Regular(pUnit);

    // check the hash-table
    if ( pUnit->n != 1 )
    {
        for ( HKey = hashKey2(p->Signature,pUnit,p->nTableSize); p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize )
            if ( p->HTable[HKey].Arg1 == pUnit )
            {
                bRes = (DdNode*) p->HTable[HKey].Arg2;  
                assert( bRes );
                return Cudd_NotCond( bRes, fComp );
            }
    }

    // treat the case of constants
    if ( Unit_IsConstant(pUnit) )
    {
        bRes = cuddUniqueConst( dd, ((double)((int)(ABC_PTRUINT_T)(pUnit->pE))) );
        cuddRef( bRes );
    }
    else
    {
        // split and recur on children of this node
        E = reoTransferUnitsToNodes_rec( p, pUnit->pE );
        if ( E == NULL )
            return NULL;
        cuddRef(E);

        T = reoTransferUnitsToNodes_rec( p, pUnit->pT );
        if ( T == NULL )
        {
            Cudd_RecursiveDeref(dd, E);
            return NULL;
        }
        cuddRef(T);
        
        // consider the case when Res0 and Res1 are the same node
        assert( E != T );
        assert( !Cudd_IsComplement(T) );

        bRes = cuddUniqueInter( dd, p->pMapToDdVarsFinal[pUnit->lev], T, E );
        if ( bRes == NULL ) 
        {
            Cudd_RecursiveDeref(dd,E);
            Cudd_RecursiveDeref(dd,T);
            return NULL;
        }
        cuddRef( bRes );
        cuddDeref( E );
        cuddDeref( T );
    }

    // do not keep the result if the ref count is only 1, since it will not be visited again
    if ( pUnit->n != 1 )
    {
         // while we traversed the diagram, the hash entry to which HKey points,
         // might have been used. Make sure that its signature is different.
         for ( ; p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize );
         p->HTable[HKey].Sign = p->Signature;
         p->HTable[HKey].Arg1 = pUnit;
         p->HTable[HKey].Arg2 = (reo_unit *)bRes;  

         // add the DD to the referenced DD list in order to be able to store it in cache
         p->pRefNodes[p->nRefNodes++] = bRes;  Cudd_Ref( bRes ); 
         // no need to do this, because the garbage collection will not take bRes away
         // it is held by the diagram in the making
    }
    // increment the counter of nodes
    p->nNodesCur++;
    cuddDeref( bRes );
    return Cudd_NotCond( bRes, fComp );
}

void reoUnitsAddUnitToPlane	(	reo_plane *	pPlane,
		reo_unit *	pUnit
	)

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

Synopsis [Adds one unit to the list of units which constitutes the plane.]

Description []

SideEffects []

SeeAlso []

Definition at line 135 of file reoUnits.c.

{
    if ( pPlane->pHead == NULL )
    {
        pPlane->pHead = pUnit;
        pUnit->Next   = NULL;
    }
    else
    {
        pUnit->Next   = pPlane->pHead;
        pPlane->pHead = pUnit;
    }
    pPlane->statsNodes++;
}

reo_unit* reoUnitsGetNextUnit

(

reo_man *

p

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Extract the next unit from the free unit list.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file reoUnits.c.

{
    reo_unit * pUnit;
    // check there are stil units to extract
    if ( p->pUnitFreeList == NULL )
        reoUnitsAddToFreeUnitList( p );
    // extract the next unit from the linked list
    pUnit            = p->pUnitFreeList;
    p->pUnitFreeList = pUnit->Next;
    p->nUnitsUsed++;
    return pUnit;
}

void reoUnitsRecycleUnit	(	reo_man *	p,
		reo_unit *	pUnit
	)

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

Synopsis [Returns the unit to the free unit list.]

Description []

SideEffects []

SeeAlso []

Definition at line 69 of file reoUnits.c.

{
    pUnit->Next      = p->pUnitFreeList;
    p->pUnitFreeList = pUnit;
    p->nUnitsUsed--;
}

void reoUnitsRecycleUnitList	(	reo_man *	p,
		reo_plane *	pPlane
	)

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

Synopsis [Returns the list of units to the free unit list.]

Description []

SideEffects []

SeeAlso []

Definition at line 87 of file reoUnits.c.

{
    reo_unit * pUnit;
    reo_unit * pTail = NULL; // Suppress "might be used uninitialized"

    if ( pPlane->pHead == NULL )
        return;

    // find the tail
    for ( pUnit = pPlane->pHead; pUnit; pUnit = pUnit->Next )
        pTail = pUnit;
    pTail->Next = p->pUnitFreeList;
    p->pUnitFreeList    = pPlane->pHead;
    memset( pPlane, 0, sizeof(reo_plane) );
//    pPlane->pHead = NULL;
}

void reoUnitsStopDispenser

(

reo_man *

p

)

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

Synopsis [Stops the unit dispenser.]

Description []

SideEffects []

SeeAlso []

Definition at line 115 of file reoUnits.c.

{
    int i;
    for ( i = 0; i < p->nMemChunks; i++ )
        ABC_FREE( p->pMemChunks[i] );
//  printf("\nThe number of chunks used is %d, each of them %d units\n", p->nMemChunks, REO_CHUNK_SIZE );
    p->nMemChunks = 0;
}