Procedures to approximate a given BDD. More...

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

Include dependency graph for cuddApprox.c:

Data Structures
struct	NodeData
	Data structure to store the information on each node. More...

struct	ApproxInfo
	Main bookkeeping data structure for approximation algorithms. More...

struct	GlobalQueueItem
	Item of the queue used in the levelized traversal of the BDD. More...

struct	LocalQueueItem
	Type of the item of the local queue. More...

Macros
#define	DBL_MAX_EXP 1024

#define	NOTHING 0

#define	REPLACE_T 1

#define	REPLACE_E 2

#define	REPLACE_N 3

#define	REPLACE_TT 4

#define	REPLACE_TE 5

#define	DONT_CARE 0

#define	CARE 1

#define	TOTAL_CARE 2

#define	CARE_ERROR 3

Typedefs
typedef struct NodeData	NodeData
	Data structure to store the information on each node. More...

typedef struct ApproxInfo	ApproxInfo
	Main bookkeeping data structure for approximation algorithms.

typedef struct GlobalQueueItem	GlobalQueueItem
	Item of the queue used in the levelized traversal of the BDD.

typedef struct LocalQueueItem	LocalQueueItem
	Type of the item of the local queue.

Functions
DdNode *	Cudd_UnderApprox (DdManager dd, DdNode f, int numVars, int threshold, int safe, double quality)
	Extracts a dense subset from a BDD with Shiple's underapproximation method. More...

DdNode *	Cudd_OverApprox (DdManager dd, DdNode f, int numVars, int threshold, int safe, double quality)
	Extracts a dense superset from a BDD with Shiple's underapproximation method. More...

DdNode *	Cudd_RemapUnderApprox (DdManager dd, DdNode f, int numVars, int threshold, double quality)
	Extracts a dense subset from a BDD with the remapping underapproximation method. More...

DdNode *	Cudd_RemapOverApprox (DdManager dd, DdNode f, int numVars, int threshold, double quality)
	Extracts a dense superset from a BDD with the remapping underapproximation method. More...

DdNode *	Cudd_BiasedUnderApprox (DdManager dd, DdNode f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
	Extracts a dense subset from a BDD with the biased underapproximation method. More...

DdNode *	Cudd_BiasedOverApprox (DdManager dd, DdNode f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
	Extracts a dense superset from a BDD with the biased underapproximation method. More...

DdNode *	cuddUnderApprox (DdManager dd, DdNode f, int numVars, int threshold, int safe, double quality)
	Applies Tom Shiple's underappoximation algorithm. More...

DdNode *	cuddRemapUnderApprox (DdManager dd, DdNode f, int numVars, int threshold, double quality)
	Applies the remapping underappoximation algorithm. More...

DdNode *	cuddBiasedUnderApprox (DdManager dd, DdNode f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
	Applies the biased remapping underappoximation algorithm. More...

static void	updateParity (DdNode node, ApproxInfo info, int newparity)
	Recursively update the parity of the paths reaching a node. More...

static NodeData *	gatherInfoAux (DdNode node, ApproxInfo info, int parity)
	Recursively counts minterms and computes reference counts of each node in the BDD. More...

static ApproxInfo *	gatherInfo (DdManager dd, DdNode node, int numVars, int parity)
	Gathers information about each node. More...

static int	computeSavings (DdManager dd, DdNode f, DdNode skip, ApproxInfo info, DdLevelQueue *queue)
	Counts the nodes that would be eliminated if a given node were replaced by zero. More...

static int	updateRefs (DdManager dd, DdNode f, DdNode skip, ApproxInfo info, DdLevelQueue *queue)
	Update function reference counts to account for replacement. More...

static int	UAmarkNodes (DdManager dd, DdNode f, ApproxInfo *info, int threshold, int safe, double quality)
	Marks nodes for replacement by zero. More...

static DdNode *	UAbuildSubset (DdManager dd, DdNode node, ApproxInfo *info)
	Builds the subset BDD. More...

static int	RAmarkNodes (DdManager dd, DdNode f, ApproxInfo *info, int threshold, double quality)
	Marks nodes for remapping. More...

static int	BAmarkNodes (DdManager dd, DdNode f, ApproxInfo *info, int threshold, double quality1, double quality0)
	Marks nodes for remapping. More...

static DdNode *	RAbuildSubset (DdManager dd, DdNode node, ApproxInfo *info)
	Builds the subset BDD for cuddRemapUnderApprox. More...

static int	BAapplyBias (DdManager dd, DdNode f, DdNode b, ApproxInfo info, DdHashTable *cache)
	Finds don't care nodes by traversing f and b in parallel. More...

Detailed Description

Procedures to approximate a given BDD.

See also: cuddSubsetHB.c cuddSubsetSP.c cuddGenCof.c

Author: 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.

Typedef Documentation

◆ NodeData

typedef struct NodeData NodeData

Data structure to store the information on each node.

It keeps the number of minterms of the function rooted at this node in terms of the number of variables specified by the user; the number of minterms of the complement; the impact of the number of minterms of this function on the number of minterms of the root function; the reference count of the node from within the root function; the flag that says whether the node intersects the care set; the flag that says whether the node should be replaced and how; the results of subsetting in both phases.

Function Documentation

◆ BAapplyBias()

static int BAapplyBias	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	b,
		ApproxInfo *	info,
		DdHashTable *	cache
	)

static

Finds don't care nodes by traversing f and b in parallel.

Returns: the care status of the visited f node if successful; CARE_ERROR otherwise.

Side effects None

See also: cuddBiasedUnderApprox

◆ BAmarkNodes()

static int BAmarkNodes	(	DdManager *	dd,
		DdNode *	f,
		ApproxInfo *	info,
		int	threshold,
		double	quality1,
		double	quality0
	)

static

Marks nodes for remapping.

Returns: 1 if successful; 0 otherwise.

Side effects None

See also: cuddBiasedUnderApprox

Parameters

dd	manager
f	function to be analyzed
info	info on BDD
threshold	when to stop approximating
quality1	minimum improvement for accepted changes when b=1
quality0	minimum improvement for accepted changes when b=0

◆ computeSavings()

static int computeSavings	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	skip,
		ApproxInfo *	info,
		DdLevelQueue *	queue
	)

static

Counts the nodes that would be eliminated if a given node were replaced by zero.

This procedure uses a queue passed by the caller for efficiency: since the queue is left empty at the endof the search, it can be reused as is by the next search.

Returns: the count (always striclty positive) if successful; 0 otherwise.

Side effects None

See also: UAmarkNodes RAmarkNodes BAmarkNodes

◆ Cudd_BiasedOverApprox()

DdNode* Cudd_BiasedOverApprox	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	b,
		int	numVars,
		int	threshold,
		double	quality1,
		double	quality0
	)

Extracts a dense superset from a BDD with the biased underapproximation method.

The procedure is identical to the underapproximation procedure except for the fact that it works on the complement of the given function. Extracting the subset of the complement function is equivalent to extracting the superset of the function. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.

Returns: a pointer to the BDD of the superset if successful. NULL if intermediate result causes the procedure to run out of memory.

Side effects None

See also: Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths Cudd_RemapOverApprox Cudd_BiasedUnderApprox Cudd_ReadSize

Parameters

dd	manager
f	function to be superset
b	bias function
numVars	number of variables in the support of f
threshold	when to stop approximation
quality1	minimum improvement for accepted changes when b=1
quality0	minimum improvement for accepted changes when b=0

◆ Cudd_BiasedUnderApprox()

DdNode* Cudd_BiasedUnderApprox	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	b,
		int	numVars,
		int	threshold,
		double	quality1,
		double	quality0
	)

Extracts a dense subset from a BDD with the biased underapproximation method.

This procedure uses a biased remapping technique and density as the cost function. The bias is a function. This procedure tries to approximate where the bias is 0 and preserve the given function where the bias is 1. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will cause overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.

Returns: a pointer to the BDD of the subset if successful. NULL if the procedure runs out of memory.

Side effects None

See also: Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_UnderApprox Cudd_RemapUnderApprox Cudd_ReadSize

Parameters

dd	manager
f	function to be subset
b	bias function
numVars	number of variables in the support of f
threshold	when to stop approximation
quality1	minimum improvement for accepted changes when b=1
quality0	minimum improvement for accepted changes when b=0

◆ Cudd_OverApprox()

DdNode* Cudd_OverApprox	(	DdManager *	dd,
		DdNode *	f,
		int	numVars,
		int	threshold,
		int	safe,
		double	quality
	)

Extracts a dense superset from a BDD with Shiple's underapproximation method.

The procedure is identical to the underapproximation procedure except for the fact that it works on the complement of the given function. Extracting the subset of the complement function is equivalent to extracting the superset of the function. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.

Returns: a pointer to the BDD of the superset if successful. NULL if intermediate result causes the procedure to run out of memory.

Side effects None

See also: Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths Cudd_ReadSize

Parameters

dd	manager
f	function to be superset
numVars	number of variables in the support of f
threshold	when to stop approximation
safe	enforce safe approximation
quality	minimum improvement for accepted changes

◆ Cudd_RemapOverApprox()

DdNode* Cudd_RemapOverApprox	(	DdManager *	dd,
		DdNode *	f,
		int	numVars,
		int	threshold,
		double	quality
	)

Extracts a dense superset from a BDD with the remapping underapproximation method.

The procedure is identical to the underapproximation procedure except for the fact that it works on the complement of the given function. Extracting the subset of the complement function is equivalent to extracting the superset of the function. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.

Returns: a pointer to the BDD of the superset if successful. NULL if intermediate result causes the procedure to run out of memory.

Side effects None

See also: Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths Cudd_ReadSize

Parameters

dd	manager
f	function to be superset
numVars	number of variables in the support of f
threshold	when to stop approximation
quality	minimum improvement for accepted changes

◆ Cudd_RemapUnderApprox()

DdNode* Cudd_RemapUnderApprox	(	DdManager *	dd,
		DdNode *	f,
		int	numVars,
		int	threshold,
		double	quality
	)

Extracts a dense subset from a BDD with the remapping underapproximation method.

This procedure uses a remapping technique and density as the cost function. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will cause overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.

Returns: a pointer to the BDD of the subset if successful. NULL if the procedure runs out of memory.

Side effects None

See also: Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_UnderApprox Cudd_ReadSize

Parameters

dd	manager
f	function to be subset
numVars	number of variables in the support of f
threshold	when to stop approximation
quality	minimum improvement for accepted changes

◆ Cudd_UnderApprox()

DdNode* Cudd_UnderApprox	(	DdManager *	dd,
		DdNode *	f,
		int	numVars,
		int	threshold,
		int	safe,
		double	quality
	)

Extracts a dense subset from a BDD with Shiple's underapproximation method.

This procedure uses a variant of Tom Shiple's underapproximation method. The main difference from the original method is that density is used as cost function. The parameter numVars is the maximum number of variables to be used in minterm calculation. The optimal number should be as close as possible to the size of the support of f. However, it is safe to pass the value returned by Cudd_ReadSize for numVars when the number of variables is under 1023. If numVars is larger than 1023, it will cause overflow. If a 0 parameter is passed then the procedure will compute a value which will avoid overflow but will cause underflow with 2046 variables or more.

Returns: a pointer to the BDD of the subset if successful; NULL if the procedure runs out of memory.

Side effects None

See also: Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_ReadSize

Parameters

dd	manager
f	function to be subset
numVars	number of variables in the support of f
threshold	when to stop approximation
safe	enforce safe approximation
quality	minimum improvement for accepted changes

◆ cuddBiasedUnderApprox()

DdNode* cuddBiasedUnderApprox	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	b,
		int	numVars,
		int	threshold,
		double	quality1,
		double	quality0
	)

Applies the biased remapping underappoximation algorithm.

Proceeds in three phases:

collect information on each node in the BDD; this is done via DFS.
traverse the BDD in top-down fashion and compute for each node whether remapping increases density.
traverse the BDD via DFS and actually perform the elimination.

Returns: the approximated BDD if successful; NULL otherwise.

Side effects None

See also: Cudd_BiasedUnderApprox

< readable true

Parameters

dd	DD manager
f	current DD
b	bias function
numVars	maximum number of variables
threshold	threshold under which approximation stops
quality1	minimum improvement for accepted changes when b=1
quality0	minimum improvement for accepted changes when b=0

◆ cuddRemapUnderApprox()

DdNode* cuddRemapUnderApprox	(	DdManager *	dd,
		DdNode *	f,
		int	numVars,
		int	threshold,
		double	quality
	)

Applies the remapping underappoximation algorithm.

Proceeds in three phases:

collect information on each node in the BDD; this is done via DFS.
traverse the BDD in top-down fashion and compute for each node whether remapping increases density.
traverse the BDD via DFS and actually perform the elimination.

Returns: the approximated BDD if successful; NULL otherwise.

Side effects None

See also: Cudd_RemapUnderApprox

< readable true

Parameters

dd	DD manager
f	current DD
numVars	maximum number of variables
threshold	threshold under which approximation stops
quality	minimum improvement for accepted changes

◆ cuddUnderApprox()

DdNode* cuddUnderApprox	(	DdManager *	dd,
		DdNode *	f,
		int	numVars,
		int	threshold,
		int	safe,
		double	quality
	)

Applies Tom Shiple's underappoximation algorithm.

Proceeds in three phases:

collect information on each node in the BDD; this is done via DFS.
traverse the BDD in top-down fashion and compute for each node whether its elimination increases density.
traverse the BDD via DFS and actually perform the elimination.

Returns: the approximated BDD if successful; NULL otherwise.

Side effects None

See also: Cudd_UnderApprox

Parameters

dd	DD manager
f	current DD
numVars	maximum number of variables
threshold	threshold under which approximation stops
safe	enforce safe approximation
quality	minimum improvement for accepted changes

◆ gatherInfo()

static ApproxInfo* gatherInfo	(	DdManager *	dd,
		DdNode *	node,
		int	numVars,
		int	parity
	)

static

Gathers information about each node.

Counts minterms and computes reference counts of each node in the BDD. The minterm count is separately computed for the node and its complement. This is to avoid cancellation errors.

Returns: a pointer to the data structure holding the information gathered if successful; NULL otherwise.

Side effects None

See also: cuddUnderApprox gatherInfoAux

◆ gatherInfoAux()

static NodeData* gatherInfoAux	(	DdNode *	node,
		ApproxInfo *	info,
		int	parity
	)

static

Recursively counts minterms and computes reference counts of each node in the BDD.

Similar to the cuddCountMintermAux which recursively counts the number of minterms for the dag rooted at each node in terms of the total number of variables (max). It assumes that the node pointer passed to it is regular and it maintains the invariant.

Side effects None

See also: gatherInfo

Parameters

node	function to analyze
info	info on BDD
parity	gather parity information

◆ RAbuildSubset()

static DdNode* RAbuildSubset	(	DdManager *	dd,
		DdNode *	node,
		ApproxInfo *	info
	)

static

Builds the subset BDD for cuddRemapUnderApprox.

Based on the info table, performs remapping or replacement at selected nodes.

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

Side effects None

See also: cuddRemapUnderApprox

Parameters

dd	DD manager
node	current node
info	node info

◆ RAmarkNodes()

static int RAmarkNodes	(	DdManager *	dd,
		DdNode *	f,
		ApproxInfo *	info,
		int	threshold,
		double	quality
	)

static

Marks nodes for remapping.

Returns: 1 if successful; 0 otherwise.

Side effects None

See also: cuddRemapUnderApprox

Parameters

dd	manager
f	function to be analyzed
info	info on BDD
threshold	when to stop approximating
quality	minimum improvement for accepted changes

◆ UAbuildSubset()

static DdNode* UAbuildSubset	(	DdManager *	dd,
		DdNode *	node,
		ApproxInfo *	info
	)

static

Builds the subset BDD.

Based on the info table, replaces selected nodes by zero.

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

Side effects None

See also: cuddUnderApprox

< readable true

Parameters

dd	DD manager
node	current node
info	node info

◆ UAmarkNodes()

static int UAmarkNodes	(	DdManager *	dd,
		DdNode *	f,
		ApproxInfo *	info,
		int	threshold,
		int	safe,
		double	quality
	)

static

Marks nodes for replacement by zero.

Returns: 1 if successful; 0 otherwise.

Side effects None

See also: cuddUnderApprox

< readable true

Parameters

dd	manager
f	function to be analyzed
info	info on BDD
threshold	when to stop approximating
safe	enforce safe approximation
quality	minimum improvement for accepted changes

◆ updateParity()

static void updateParity	(	DdNode *	node,
		ApproxInfo *	info,
		int	newparity
	)

static

Recursively update the parity of the paths reaching a node.

Assumes that node is regular and propagates the invariant.

Side effects None

See also: gatherInfoAux

Parameters

node	function to analyze
info	info on BDD
newparity	new parity for node

◆ updateRefs()

static int updateRefs	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	skip,
		ApproxInfo *	info,
		DdLevelQueue *	queue
	)

static

Update function reference counts to account for replacement.

Returns: the number of nodes saved if successful; 0 otherwise.

Side effects None

See also: UAmarkNodes RAmarkNodes BAmarkNodes

Data Structures

Macros

Typedefs

Functions

Detailed Description

Typedef Documentation

◆ NodeData

Function Documentation

◆ BAapplyBias()

◆ BAmarkNodes()

◆ computeSavings()

◆ Cudd_BiasedOverApprox()

◆ Cudd_BiasedUnderApprox()

◆ Cudd_OverApprox()

◆ Cudd_RemapOverApprox()

◆ Cudd_RemapUnderApprox()

◆ Cudd_UnderApprox()

◆ cuddBiasedUnderApprox()

◆ cuddRemapUnderApprox()

◆ cuddUnderApprox()

◆ gatherInfo()

◆ gatherInfoAux()

◆ RAbuildSubset()

◆ RAmarkNodes()

◆ UAbuildSubset()

◆ UAmarkNodes()

◆ updateParity()

◆ updateRefs()