cudd/cuddZddGroup.c File Reference

Functions for ZDD group sifting. More...

#include "util.h"
#include "mtrInt.h"
#include "cuddInt.h"
Include dependency graph for cuddZddGroup.c:

Functions

MtrNodeCudd_MakeZddTreeNode (DdManager *dd, unsigned int low, unsigned int size, unsigned int type)
 Creates a new ZDD variable group.
int cuddZddTreeSifting (DdManager *table, Cudd_ReorderingType method)
 Tree sifting algorithm for ZDDs.
static int zddTreeSiftingAux (DdManager *table, MtrNode *treenode, Cudd_ReorderingType method)
 Visits the group tree and reorders each group.
static int zddReorderChildren (DdManager *table, MtrNode *treenode, Cudd_ReorderingType method)
 Reorders the children of a group tree node according to the options.
static void zddFindNodeHiLo (DdManager *table, MtrNode *treenode, int *lower, int *upper)
 Finds the lower and upper bounds of the group represented by treenode.
static int zddUniqueCompareGroup (void const *ptrX, void const *ptrY)
 Comparison function used by qsort.
static int zddGroupSifting (DdManager *table, int lower, int upper)
 Sifts from treenode->low to treenode->high.
static int zddGroupSiftingAux (DdManager *table, int x, int xLow, int xHigh)
 Sifts one variable up and down until it has taken all positions. Checks for aggregation.
static int zddGroupSiftingUp (DdManager *table, int y, int xLow, Move **moves)
 Sifts up a variable until either it reaches position xLow or the size of the DD heap increases too much.
static int zddGroupSiftingDown (DdManager *table, int x, int xHigh, Move **moves)
 Sifts down a variable until it reaches position xHigh.
static int zddGroupMove (DdManager *table, int x, int y, Move **moves)
 Swaps two groups and records the move.
static int zddGroupMoveBackward (DdManager *table, int x, int y)
 Undoes the swap two groups.
static int zddGroupSiftingBackward (DdManager *table, Move *moves, int size)
 Determines the best position for a variables and returns it there.
static void zddMergeGroups (DdManager *table, MtrNode *treenode, int low, int high)
 Merges groups in the DD table.

Detailed Description

Functions for ZDD group sifting.

Author:
Fabio Somenzi

Copyright (c) 1995-2015, Regents of the University of Colorado

All rights reserved.

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

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

Creates a new ZDD variable group.

The group starts at variable 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 ZDD variable tree is changed.
See also:
Cudd_MakeTreeNode
Parameters:
dd manager
low index of the first group variable
size number of variables in the group
type MTR_DEFAULT or MTR_FIXED
int cuddZddTreeSifting ( DdManager table,
Cudd_ReorderingType  method 
)

Tree sifting algorithm for ZDDs.

Assumes that a tree representing a group hierarchy is passed as a parameter. It then reorders each group in postorder fashion by calling zddTreeSiftingAux. 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
static void zddFindNodeHiLo ( DdManager table,
MtrNode treenode,
int *  lower,
int *  upper 
) [static]

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

The high and low fields of treenode are indices. From those we need to derive the current positions, and find maximum and minimum.

Side effects
The bounds are returned as side effects.
static int zddGroupMove ( 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
static int zddGroupMoveBackward ( DdManager table,
int  x,
int  y 
) [static]

Undoes the swap two groups.

Returns:
1 in case of success; 0 otherwise.
Side effects
None
static int zddGroupSifting ( DdManager table,
int  lower,
int  upper 
) [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
static int zddGroupSiftingAux ( DdManager table,
int  x,
int  xLow,
int  xHigh 
) [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
static int zddGroupSiftingBackward ( DdManager table,
Move moves,
int  size 
) [static]

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

Returns:
1 in case of success; 0 otherwise.
Side effects
None
static int zddGroupSiftingDown ( DdManager table,
int  x,
int  xHigh,
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
static int zddGroupSiftingUp ( DdManager table,
int  y,
int  xLow,
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
static void zddMergeGroups ( 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 idex field of the tree node.

Side effects
None
static int zddReorderChildren ( 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
static int zddTreeSiftingAux ( 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
static int zddUniqueCompareGroup ( 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
 All Data Structures Files Functions Variables Typedefs Enumerations Defines

Generated on 31 Dec 2015 for cudd by  doxygen 1.6.1