Functions for group sifting. More...

#include "util.h"
#include "mtrInt.h"
#include "cuddInt.h"

Include dependency graph for cuddGroup.c:

Macros
#define	DD_NORMAL_SIFT 0

#define	DD_LAZY_SIFT 1

#define	DD_SIFT_DOWN 0

#define	DD_SIFT_UP 1

Typedefs
typedef int(*	DD_CHKFP) (DdManager *, int, int)

Functions
MtrNode *	Cudd_MakeTreeNode (DdManager *dd, unsigned int low, unsigned int size, unsigned int type)
	Creates a new variable group. More...

int	cuddTreeSifting (DdManager *table, Cudd_ReorderingType method)
	Tree sifting algorithm. More...

static int	ddTreeSiftingAux (DdManager table, MtrNode treenode, Cudd_ReorderingType method)
	Visits the group tree and reorders each group. More...

static int	ddReorderChildren (DdManager table, MtrNode treenode, Cudd_ReorderingType method)
	Reorders the children of a group tree node according to the options. More...

static void	ddFindNodeHiLo (DdManager table, MtrNode treenode, int lower, int upper)
	Finds the lower and upper bounds of the group represented by treenode. More...

static int	ddUniqueCompareGroup (void const ptrX, void const ptrY)
	Comparison function used by qsort. More...

static int	ddGroupSifting (DdManager *table, int lower, int upper, DD_CHKFP checkFunction, int lazyFlag)
	Sifts from treenode->low to treenode->high. More...

static void	ddCreateGroup (DdManager *table, int x, int y)
	Creates a group encompassing variables from x to y in the DD table. More...

static int	ddGroupSiftingAux (DdManager *table, int x, int xLow, int xHigh, DD_CHKFP checkFunction, int lazyFlag)
	Sifts one variable up and down until it has taken all positions. Checks for aggregation. More...

static int	ddGroupSiftingUp (DdManager table, int y, int xLow, DD_CHKFP checkFunction, Move *moves)
	Sifts up a variable until either it reaches position xLow or the size of the DD heap increases too much. More...

static int	ddGroupSiftingDown (DdManager table, int x, int xHigh, DD_CHKFP checkFunction, Move *moves)
	Sifts down a variable until it reaches position xHigh. More...

static int	ddGroupMove (DdManager table, int x, int y, Move *moves)
	Swaps two groups and records the move. More...

static int	ddGroupMoveBackward (DdManager *table, int x, int y)
	Undoes the swap two groups. More...

static int	ddGroupSiftingBackward (DdManager table, Move moves, int size, int upFlag, int lazyFlag)
	Determines the best position for a variables and returns it there. More...

static void	ddMergeGroups (DdManager table, MtrNode treenode, int low, int high)
	Merges groups in the DD table. More...

static void	ddDissolveGroup (DdManager *table, int x, int y)
	Dissolves a group in the DD table. More...

static int	ddNoCheck (DdManager *table, int x, int y)
	Pretends to check two variables for aggregation. More...

static int	ddSecDiffCheck (DdManager *table, int x, int y)
	Checks two variables for aggregation. More...

static int	ddExtSymmCheck (DdManager *table, int x, int y)
	Checks for extended symmetry of x and y. More...

static int	ddVarGroupCheck (DdManager *table, int x, int y)
	Checks for grouping of x and y. More...

static int	ddSetVarHandled (DdManager *dd, int index)
	Sets a variable to already handled. More...

static int	ddResetVarHandled (DdManager *dd, int index)
	Resets a variable to be processed. More...

static int	ddIsVarHandled (DdManager *dd, int index)
	Checks whether a variables is already handled. More...

Detailed Description

Functions for group sifting.

Author: Shipra Panda, Fabio Somenzi

Copyright

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

Function Documentation

◆ Cudd_MakeTreeNode()

MtrNode* Cudd_MakeTreeNode	(	DdManager *	dd,
		unsigned int	low,
		unsigned int	size,
		unsigned int	type
	)

Creates a new variable group.

The group starts at variable low and contains size variables. The parameter low is the index of the first variable. If the variable already exists, its current position in the order is known to the manager. If the variable does not exist yet, the position is assumed to be the same as the index. The group tree is created if it does not exist yet.

Returns: a pointer to the group if successful; NULL otherwise.

Side effects The variable tree is changed.

See also: Cudd_MakeZddTreeNode

Parameters

dd	manager
low	index of the first group variable
size	number of variables in the group
type	MTR_DEFAULT or MTR_FIXED

◆ cuddTreeSifting()

int cuddTreeSifting	(	DdManager *	table,
		Cudd_ReorderingType	method
	)

Tree sifting algorithm.

Assumes that a tree representing a group hierarchy is passed as a parameter. It then reorders each group in postorder fashion by calling ddTreeSiftingAux. Assumes that no dead nodes are present.

Returns: 1 if successful; 0 otherwise.

Side effects None

Parameters

table	DD table
method	reordering method for the groups of leaves

◆ ddCreateGroup()

static void ddCreateGroup	(	DdManager *	table,
		int	x,
		int	y
	)

static

Creates a group encompassing variables from x to y in the DD table.

In the current implementation it must be y == x+1.

Side effects None

◆ ddDissolveGroup()

static void ddDissolveGroup	(	DdManager *	table,
		int	x,
		int	y
	)

static

Dissolves a group in the DD table.

x and y are variables in a group to be cut in two. The cut is to pass between x and y.

Side effects None

◆ ddExtSymmCheck()

static int ddExtSymmCheck	(	DdManager *	table,
		int	x,
		int	y
	)

static

Checks for extended symmetry of x and y.

Returns: 1 in case of extended symmetry; 0 otherwise.

Side effects None

◆ ddFindNodeHiLo()

static void ddFindNodeHiLo	(	DdManager *	table,
		MtrNode *	treenode,
		int *	lower,
		int *	upper
	)

static

Finds the lower and upper bounds of the group represented by treenode.

From the index and size fields we need to derive the current positions, and find maximum and minimum.

Side effects The bounds are returned as side effects.

◆ ddGroupMove()

static int ddGroupMove	(	DdManager *	table,
		int	x,
		int	y,
		Move **	moves
	)

static

Swaps two groups and records the move.

Returns: the number of keys in the DD table in case of success; 0 otherwise.

Side effects None

◆ ddGroupMoveBackward()

static int ddGroupMoveBackward	(	DdManager *	table,
		int	x,
		int	y
	)

static

Undoes the swap two groups.

Returns: 1 in case of success; 0 otherwise.

Side effects None

◆ ddGroupSifting()

static int ddGroupSifting	(	DdManager *	table,
		int	lower,
		int	upper,
		DD_CHKFP	checkFunction,
		int	lazyFlag
	)

static

Sifts from treenode->low to treenode->high.

If croupcheck == CUDD_GROUP_CHECK7, it checks for group creation at the end of the initial sifting. If a group is created, it is then sifted again. After sifting one variable, the group that contains it is dissolved.

Returns: 1 in case of success; 0 otherwise.

Side effects None

◆ ddGroupSiftingAux()

static int ddGroupSiftingAux	(	DdManager *	table,
		int	x,
		int	xLow,
		int	xHigh,
		DD_CHKFP	checkFunction,
		int	lazyFlag
	)

static

Sifts one variable up and down until it has taken all positions. Checks for aggregation.

There may be at most two sweeps, even if the group grows. Assumes that x is either an isolated variable, or it is the bottom of a group. All groups may not have been found. The variable being moved is returned to the best position seen during sifting.

Returns: 1 in case of success; 0 otherwise.

Side effects None

◆ ddGroupSiftingBackward()

static int ddGroupSiftingBackward	(	DdManager *	table,
		Move *	moves,
		int	size,
		int	upFlag,
		int	lazyFlag
	)

static

Determines the best position for a variables and returns it there.

Returns: 1 in case of success; 0 otherwise.

Side effects None

◆ ddGroupSiftingDown()

static int ddGroupSiftingDown	(	DdManager *	table,
		int	x,
		int	xHigh,
		DD_CHKFP	checkFunction,
		Move **	moves
	)

static

Sifts down a variable until it reaches position xHigh.

Assumes that x is the bottom of a group (or a singleton). Records all the moves.

Returns: 1 in case of success; 0 otherwise.

Side effects None

◆ ddGroupSiftingUp()

static int ddGroupSiftingUp	(	DdManager *	table,
		int	y,
		int	xLow,
		DD_CHKFP	checkFunction,
		Move **	moves
	)

static

Sifts up a variable until either it reaches position xLow or the size of the DD heap increases too much.

Assumes that y is the top of a group (or a singleton). Checks y for aggregation to the adjacent variables. Records all the moves that are appended to the list of moves received as input and returned as a side effect.

Returns: 1 in case of success; 0 otherwise.

Side effects None

◆ ddIsVarHandled()

static int ddIsVarHandled	(	DdManager *	dd,
		int	index
	)

static

Checks whether a variables is already handled.

This function is used for lazy sifting.

Side effects none

◆ ddMergeGroups()

static void ddMergeGroups	(	DdManager *	table,
		MtrNode *	treenode,
		int	low,
		int	high
	)

static

Merges groups in the DD table.

Creates a single group from low to high and adjusts the index field of the tree node.

Side effects None

◆ ddNoCheck()

static int ddNoCheck	(	DdManager *	table,
		int	x,
		int	y
	)

static

Pretends to check two variables for aggregation.

Returns: always 0.

Side effects None

◆ ddReorderChildren()

static int ddReorderChildren	(	DdManager *	table,
		MtrNode *	treenode,
		Cudd_ReorderingType	method
	)

static

Reorders the children of a group tree node according to the options.

After reordering puts all the variables in the group and/or its descendents in a single group. This allows hierarchical reordering. If the variables in the group do not exist yet, simply does nothing.

Returns: 1 if successful; 0 otherwise.

Side effects None

◆ ddResetVarHandled()

static int ddResetVarHandled	(	DdManager *	dd,
		int	index
	)

static

Resets a variable to be processed.

This function is used for lazy sifting.

Side effects none

◆ ddSecDiffCheck()

static int ddSecDiffCheck	(	DdManager *	table,
		int	x,
		int	y
	)

static

Checks two variables for aggregation.

The check is based on the second difference of the number of nodes as a function of the layer. If the second difference is lower than a given threshold (typically negative) then the two variables should be aggregated.

Returns: 1 if the two variables pass the test; 0 otherwise.

Side effects None

◆ ddSetVarHandled()

static int ddSetVarHandled	(	DdManager *	dd,
		int	index
	)

static

Sets a variable to already handled.

This function is used for lazy sifting.

Side effects none

◆ ddTreeSiftingAux()

static int ddTreeSiftingAux	(	DdManager *	table,
		MtrNode *	treenode,
		Cudd_ReorderingType	method
	)

static

Visits the group tree and reorders each group.

Recursively visits the group tree and reorders each group in postorder fashion.

Returns: 1 if successful; 0 otherwise.

Side effects None

◆ ddUniqueCompareGroup()

static int ddUniqueCompareGroup	(	void const *	ptrX,
		void const *	ptrY
	)

static

Comparison function used by qsort.

Comparison function used by qsort to order the variables according to the number of keys in the subtables.

Returns: the difference in number of keys between the two variables being compared.

Side effects None

◆ ddVarGroupCheck()

static int ddVarGroupCheck	(	DdManager *	table,
		int	x,
		int	y
	)

static

Checks for grouping of x and y.

This function is used for lazy sifting.

Returns: 1 in case of grouping; 0 otherwise.

Side effects None

Macros

Typedefs

Functions

Detailed Description

Function Documentation

◆ Cudd_MakeTreeNode()

◆ cuddTreeSifting()

◆ ddCreateGroup()

◆ ddDissolveGroup()

◆ ddExtSymmCheck()

◆ ddFindNodeHiLo()

◆ ddGroupMove()

◆ ddGroupMoveBackward()

◆ ddGroupSifting()

◆ ddGroupSiftingAux()

◆ ddGroupSiftingBackward()

◆ ddGroupSiftingDown()

◆ ddGroupSiftingUp()

◆ ddIsVarHandled()

◆ ddMergeGroups()

◆ ddNoCheck()

◆ ddReorderChildren()

◆ ddResetVarHandled()

◆ ddSecDiffCheck()

◆ ddSetVarHandled()

◆ ddTreeSiftingAux()

◆ ddUniqueCompareGroup()

◆ ddVarGroupCheck()