Procedure to subset the given BDD choosing the shortest paths (largest cubes) in the BDD. More...

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

Include dependency graph for cuddSubsetSP.c:

Data Structures
struct	NodeDist
	structure created to store subset results for each node and distances with odd and even parity of the node from the root and sink. More...

struct	AssortedInfo
	assorted information needed by the BuildSubsetBdd procedure. More...

struct	GlobalInfo
	Bookkeeping data structure for subsetting algorithm. More...

Macros
#define	DEFAULT_PAGE_SIZE 2048 /* page size to store the BFS queue element type */

#define	DEFAULT_NODE_DIST_PAGE_SIZE 2048 /* page size to store NodeDist_t type */

#define	MAXSHORTINT

#define	INITIAL_PAGES

Typedefs
typedef struct NodeDist	NodeDist_t

typedef struct GlobalInfo	GlobalInfo_t

Functions
DdNode *	Cudd_SubsetShortPaths (DdManager dd, DdNode f, int numVars, int threshold, int hardlimit)
	Extracts a dense subset from a BDD with the shortest paths heuristic. More...

DdNode *	Cudd_SupersetShortPaths (DdManager dd, DdNode f, int numVars, int threshold, int hardlimit)
	Extracts a dense superset from a BDD with the shortest paths heuristic. More...

DdNode *	cuddSubsetShortPaths (DdManager dd, DdNode f, int numVars, int threshold, int hardlimit)
	The outermost procedure to return a subset of the given BDD with the shortest path lengths. More...

static void	ResizeNodeDistPages (DdManager dd, GlobalInfo_t gInfo)
	Resize the number of pages allocated to store the distances related to each node. More...

static void	ResizeQueuePages (DdManager dd, GlobalInfo_t gInfo)
	Resize the number of pages allocated to store nodes in the BFS traversal of the BDD. More...

static void	CreateTopDist (DdManager dd, GlobalInfo_t gInfo, st_table pathTable, int parentPage, int parentQueueIndex, int topLen, DdNode childPage, int childQueueIndex, int numParents, FILE fp)
	Labels each node with its shortest distance from the root. More...

static int	CreateBotDist (DdNode node, st_table pathTable, unsigned int pathLengthArray, FILE fp)
	Labels each node with the shortest distance from the constant. More...

static st_table *	CreatePathTable (DdManager dd, GlobalInfo_t gInfo, DdNode node, unsigned int pathLengthArray, FILE *fp)
	The outer procedure to label each node with its shortest distance from the root and constant. More...

static unsigned int	AssessPathLength (unsigned int pathLengthArray, int threshold, int numVars, unsigned int excess, FILE *fp)
	Chooses the maximum allowable path length of nodes under the threshold. More...

static DdNode *	BuildSubsetBdd (DdManager dd, GlobalInfo_t gInfo, st_table pathTable, DdNode node, struct AssortedInfo info, st_table subsetNodeTable)
	Builds the BDD with nodes labeled with path length less than or equal to maxpath. More...

static enum st_retval	stPathTableDdFree (void key, void value, void *arg)
	Procedure to free the result dds stored in the NodeDist pages. More...

Detailed Description

Procedure to subset the given BDD choosing the shortest paths (largest cubes) in the BDD.

See also: cuddSubsetHB.c

Author: Kavita Ravi

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.

Macro Definition Documentation

◆ INITIAL_PAGES

#define INITIAL_PAGES

Value:

128 /* number of initial pages for the

* queue/NodeDist_t type */

◆ MAXSHORTINT

#define MAXSHORTINT

Value:

((DdHalfWord) ~0) /* constant defined to store
                       * maximum distance of a node
                       * from the root or the constant
                       */

Function Documentation

◆ AssessPathLength()

static unsigned int AssessPathLength	(	unsigned int *	pathLengthArray,
		int	threshold,
		int	numVars,
		unsigned int *	excess,
		FILE *	fp
	)

static

Chooses the maximum allowable path length of nodes under the threshold.

The corner cases are when the threshold is larger than the number of nodes in the BDD iself, in which case 'numVars + 1' is returned. If all nodes of a particular path length are needed, then the maxpath returned is the next one with excess nodes = 0.

Side effects None

◆ BuildSubsetBdd()

static DdNode* BuildSubsetBdd	(	DdManager *	dd,
		GlobalInfo_t *	gInfo,
		st_table *	pathTable,
		DdNode *	node,
		struct AssortedInfo *	info,
		st_table *	subsetNodeTable
	)

static

Builds the BDD with nodes labeled with path length less than or equal to maxpath.

Builds the BDD with nodes labeled with path length under maxpath and as many nodes labeled maxpath as determined by the threshold. The procedure uses the path table to determine which nodes in the original bdd need to be retained. This procedure picks a shortest path (tie break decided by taking the child with the shortest distance to the constant) and recurs down the path till it reaches the constant. the procedure then starts building the subset upward from the constant. All nodes labeled by path lengths less than the given maxpath are used to build the subset. However, in the case of nodes that have label equal to maxpath, as many are chosen as required by the threshold. This number is stored in the info structure in the field thresholdReached. This field is decremented whenever a node labeled maxpath is encountered and the nodes labeled maxpath are aggregated in a maxpath table. As soon as the thresholdReached count goes to 0, the shortest path from this node to the constant is found. The extraction of nodes with the above labeling is based on the fact that each node, labeled with a path length, P, has at least one child labeled P or less. So extracting all nodes labeled a given path length P ensures complete paths between the root and the constant. Extraction of a partial number of nodes with a given path length may result in incomplete paths and hence the additional number of nodes are grabbed to complete the path. Since the Bdd is built bottom-up, other nodes labeled maxpath do lie on complete paths. The procedure may cause the subset to have a larger or smaller number of nodes than the specified threshold. The increase in the number of nodes is caused by the building of a subset and the reduction by recombination. However in most cases, the recombination overshadows the increase and the procedure returns a result with lower number of nodes than specified. The subsetNodeTable is NIL when there is no hard limit on the number of nodes. Further efforts towards keeping the subset closer to the threshold number were abandoned in favour of keeping the procedure simple and fast.

Side effects SubsetNodeTable is changed if it is not NIL.

Parameters

dd	DD manager
gInfo	global information
pathTable	path table with path lengths and computed results
node	current node
info	assorted information structure
subsetNodeTable	table storing computed results

◆ CreateBotDist()

static int CreateBotDist	(	DdNode *	node,
		st_table *	pathTable,
		unsigned int *	pathLengthArray,
		FILE *	fp
	)

static

Labels each node with the shortest distance from the constant.

This is done in a DFS search of the BDD. Each node has an odd and even parity distance from the sink (since there exists paths to both zero and one) which is less than MAXSHORTINT. At each node these distances are updated using the minimum distance of its children from the constant. SInce now both the length from the root and child is known, the minimum path length(length of the shortest path between the root and the constant that this node lies on) of this node can be calculated and used to update the pathLengthArray.

Side effects Updates Path Table and path length array

See also: CreatePathTable CreateTopDist AssessPathLength

◆ CreatePathTable()

static st_table* CreatePathTable	(	DdManager *	dd,
		GlobalInfo_t *	gInfo,
		DdNode *	node,
		unsigned int *	pathLengthArray,
		FILE *	fp
	)

static

The outer procedure to label each node with its shortest distance from the root and constant.

Calls CreateTopDist and CreateBotDist. The basis for computing the distance between root and constant is that the distance may be the sum of even distances from the node to the root and constant or the sum of odd distances from the node to the root and constant. Both CreateTopDist and CreateBotDist create the odd and even parity distances from the root and constant respectively.

Side effects None

See also: CreateTopDist CreateBotDist

Parameters

dd	DD manager
gInfo	global information
node	root of function
pathLengthArray	array of path lengths to store nodes labeled with the various path lengths
fp	where to write messages

◆ CreateTopDist()

static void CreateTopDist	(	DdManager *	dd,
		GlobalInfo_t *	gInfo,
		st_table *	pathTable,
		int	parentPage,
		int	parentQueueIndex,
		int	topLen,
		DdNode **	childPage,
		int	childQueueIndex,
		int	numParents,
		FILE *	fp
	)

static

Labels each node with its shortest distance from the root.

This is done in a BFS search of the BDD. The nodes are processed in a queue implemented as pages(array) to reduce memory fragmentation. An entry is created for each node visited. The distance from the root to the node with the corresponding parity is updated. The procedure is called recursively each recusion level handling nodes at a given level from the root.

Side effects Creates entries in the pathTable

See also: CreatePathTable CreateBotDist

Parameters

dd	DD manager
gInfo	global information
pathTable	hash table to store path lengths
parentPage	the pointer to the page on which the first parent in the queue is to be found.
parentQueueIndex	pointer to the first parent on the page
topLen	current distance from the root
childPage	pointer to the page on which the first child is to be added.
childQueueIndex	pointer to the first child
numParents	number of parents to process in this recursive call
fp	where to write messages

◆ Cudd_SubsetShortPaths()

DdNode* Cudd_SubsetShortPaths	(	DdManager *	dd,
		DdNode *	f,
		int	numVars,
		int	threshold,
		int	hardlimit
	)

Extracts a dense subset from a BDD with the shortest paths heuristic.

This procedure tries to preserve the shortest paths of the input BDD, because they give many minterms and contribute few nodes. This procedure may increase the number of nodes in trying to create the subset or reduce the number of nodes due to recombination as compared to the original BDD. Hence the threshold may not be strictly adhered to. In practice, recombination overshadows the increase in the number of nodes and results in small BDDs as compared to the threshold. The hardlimit specifies whether threshold needs to be strictly adhered to. If it is set to 1, the procedure ensures that result is never larger than the specified limit but may be considerably less than the threshold. The value for numVars should be as close as possible to the size of the support of f for better efficiency. However, it is safe to pass the value returned by Cudd_ReadSize for numVars. If 0 is passed, then the value returned by Cudd_ReadSize is used.

Returns: a pointer to the BDD for the subset if successful; NULL otherwise.

Side effects None

See also: Cudd_SupersetShortPaths Cudd_SubsetHeavyBranch Cudd_ReadSize

Parameters

dd	manager
f	function to be subset
numVars	number of variables in the support of f
threshold	maximum number of nodes in the subset
hardlimit	flag: 1 if threshold is a hard limit

◆ Cudd_SupersetShortPaths()

DdNode* Cudd_SupersetShortPaths	(	DdManager *	dd,
		DdNode *	f,
		int	numVars,
		int	threshold,
		int	hardlimit
	)

Extracts a dense superset from a BDD with the shortest paths heuristic.

The procedure is identical to the subset procedure except for the fact that it receives the complement of the given function. Extracting the subset of the complement function is equivalent to extracting the superset of the function. This procedure tries to preserve the shortest paths of the complement BDD, because they give many minterms and contribute few nodes. This procedure may increase the number of nodes in trying to create the superset or reduce the number of nodes due to recombination as compared to the original BDD. Hence the threshold may not be strictly adhered to. In practice, recombination overshadows the increase in the number of nodes and results in small BDDs as compared to the threshold. The hardlimit specifies whether threshold needs to be strictly adhered to. If it is set to 1, the procedure ensures that result is never larger than the specified limit but may be considerably less than the threshold. The value for numVars should be as close as possible to the size of the support of f for better efficiency. However, it is safe to pass the value returned by Cudd_ReadSize for numVar. If 0 is passed, then the value returned by Cudd_ReadSize is used.

Returns: a pointer to the BDD for the superset if successful; NULL otherwise.

Side effects None

See also: Cudd_SubsetShortPaths Cudd_SupersetHeavyBranch Cudd_ReadSize

Parameters

dd	manager
f	function to be superset
numVars	number of variables in the support of f
threshold	maximum number of nodes in the subset
hardlimit	flag: 1 if threshold is a hard limit

◆ cuddSubsetShortPaths()

DdNode* cuddSubsetShortPaths	(	DdManager *	dd,
		DdNode *	f,
		int	numVars,
		int	threshold,
		int	hardlimit
	)

The outermost procedure to return a subset of the given BDD with the shortest path lengths.

The path lengths are calculated, the maximum allowable path length is determined and the number of nodes of this path length that can be used to build a subset. If the threshold is larger than the size of the original BDD, the original BDD is returned.

Side effects None

See also: Cudd_SubsetShortPaths

Parameters

dd	DD manager
f	function to be subset
numVars	total number of variables in consideration
threshold	maximum number of nodes allowed in the subset
hardlimit	flag determining whether threshold should be respected strictly

◆ ResizeNodeDistPages()

static void ResizeNodeDistPages	(	DdManager *	dd,
		GlobalInfo_t *	gInfo
	)

static

Resize the number of pages allocated to store the distances related to each node.

The procedure moves the counter to the next page when the end of the page is reached and allocates new pages when necessary.

Side effects Changes the size of pages, page, page index, maximum: number of pages freeing stuff in case of memory out.

Parameters

dd	DD manager
gInfo	global information

◆ ResizeQueuePages()

static void ResizeQueuePages	(	DdManager *	dd,
		GlobalInfo_t *	gInfo
	)

static

Resize the number of pages allocated to store nodes in the BFS traversal of the BDD.

The procedure moves the counter to the next page when the end of the page is reached and allocates new pages when necessary.

Side effects Changes the size of pages, page, page index, maximum: number of pages freeing stuff in case of memory out.

Parameters

dd	DD manager
gInfo	global information

◆ stPathTableDdFree()

static enum st_retval stPathTableDdFree	(	void *	key,
		void *	value,
		void *	arg
	)

static

Procedure to free the result dds stored in the NodeDist pages.

Side effects None

Data Structures

Macros

Typedefs

Functions

Detailed Description

Macro Definition Documentation

◆ INITIAL_PAGES

◆ MAXSHORTINT

Function Documentation

◆ AssessPathLength()

◆ BuildSubsetBdd()

◆ CreateBotDist()

◆ CreatePathTable()

◆ CreateTopDist()

◆ Cudd_SubsetShortPaths()

◆ Cudd_SupersetShortPaths()

◆ cuddSubsetShortPaths()

◆ ResizeNodeDistPages()

◆ ResizeQueuePages()

◆ stPathTableDdFree()