Priority functions. More...

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

Include dependency graph for cuddPriority.c:

Functions
DdNode *	Cudd_PrioritySelect (DdManager dd, DdNode R, DdNode x, DdNode y, DdNode *z, DdNode Pi, int n, DD_PRFP Pifunc)
	Selects pairs from R using a priority function. More...

DdNode *	Cudd_Xgty (DdManager dd, int N, DdNode z, DdNode x, DdNode *y)
	Generates a BDD for the function x > y. More...

DdNode *	Cudd_Xeqy (DdManager dd, int N, DdNode x, DdNode *y)
	Generates a BDD for the function x==y. More...

DdNode *	Cudd_addXeqy (DdManager dd, int N, DdNode x, DdNode *y)
	Generates an ADD for the function x==y. More...

DdNode *	Cudd_Dxygtdxz (DdManager dd, int N, DdNode x, DdNode y, DdNode *z)
	Generates a BDD for the function d(x,y) > d(x,z). More...

DdNode *	Cudd_Dxygtdyz (DdManager dd, int N, DdNode x, DdNode y, DdNode *z)
	Generates a BDD for the function d(x,y) > d(y,z). More...

DdNode *	Cudd_Inequality (DdManager dd, int N, int c, DdNode x, DdNode *y)
	Generates a BDD for the function x - y ≥ c. More...

DdNode *	Cudd_Disequality (DdManager dd, int N, int c, DdNode x, DdNode *y)
	Generates a BDD for the function x - y != c. More...

DdNode *	Cudd_bddInterval (DdManager dd, int N, DdNode *x, unsigned int lowerB, unsigned int upperB)
	Generates a BDD for the function lowerB ≤ x ≤ upperB. More...

DdNode *	Cudd_CProjection (DdManager dd, DdNode R, DdNode *Y)
	Computes the compatible projection of R w.r.t. cube Y. More...

DdNode *	Cudd_addHamming (DdManager dd, DdNode xVars, DdNode *yVars, int nVars)
	Computes the Hamming distance ADD. More...

int	Cudd_MinHammingDist (DdManager dd, DdNode f, int *minterm, int upperBound)
	Returns the minimum Hamming distance between f and minterm. More...

DdNode *	Cudd_bddClosestCube (DdManager dd, DdNode f, DdNode g, int distance)
	Finds a cube of f at minimum Hamming distance from the minterms of g. More...

DdNode *	cuddCProjectionRecur (DdManager dd, DdNode R, DdNode Y, DdNode Ysupp)
	Performs the recursive step of Cudd_CProjection. More...

DdNode *	cuddBddClosestCube (DdManager dd, DdNode f, DdNode *g, CUDD_VALUE_TYPE bound)
	Performs the recursive step of Cudd_bddClosestCube. More...

static int	cuddMinHammingDistRecur (DdNode f, int minterm, DdHashTable *table, int upperBound)
	Performs the recursive step of Cudd_MinHammingDist. More...

static DdNode *	separateCube (DdManager dd, DdNode f, CUDD_VALUE_TYPE *distance)
	Separates cube from distance. More...

static DdNode *	createResult (DdManager dd, unsigned int index, unsigned int phase, DdNode cube, CUDD_VALUE_TYPE distance)
	Builds a result for cache storage. More...

Detailed Description

Priority functions.

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.

Function Documentation

◆ createResult()

static DdNode* createResult	(	DdManager *	dd,
		unsigned int	index,
		unsigned int	phase,
		DdNode *	cube,
		CUDD_VALUE_TYPE	distance
	)

static

Builds a result for cache storage.

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

Side effects None

See also: cuddBddClosestCube separateCube

◆ Cudd_addHamming()

DdNode* Cudd_addHamming	(	DdManager *	dd,
		DdNode **	xVars,
		DdNode **	yVars,
		int	nVars
	)

Computes the Hamming distance ADD.

The two vectors xVars and yVars identify the variables that form the two arguments.

Returns: an ADD that gives the Hamming distance between its two arguments if successful; NULL otherwise.

Side effects None

◆ Cudd_addXeqy()

DdNode* Cudd_addXeqy	(	DdManager *	dd,
		int	N,
		DdNode **	x,
		DdNode **	y
	)

Generates an ADD for the function x==y.

This function generates an ADD for the function x==y. Both x and y are N-bit numbers, x[0] x[1] ... x[N-1] and y[0] y[1] ... y[N-1]. The ADD is built bottom-up. It has 3*N-1 internal nodes, if the variables are ordered as follows: x[0] y[0] x[1] y[1] ... x[N-1] y[N-1].

Side effects None

See also: Cudd_Xeqy

Parameters

dd	DD manager
N	number of x and y variables
x	array of x variables
y	array of y variables

◆ Cudd_bddClosestCube()

DdNode* Cudd_bddClosestCube	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	g,
		int *	distance
	)

Finds a cube of f at minimum Hamming distance from the minterms of g.

All the minterms of the cube are at the minimum distance. If the distance is 0, the cube belongs to the intersection of f and g.

Returns: the cube if successful; NULL otherwise.

Side effects The distance is returned as a side effect.

See also: Cudd_MinHammingDist

◆ Cudd_bddInterval()

DdNode* Cudd_bddInterval	(	DdManager *	dd,
		int	N,
		DdNode **	x,
		unsigned int	lowerB,
		unsigned int	upperB
	)

Generates a BDD for the function lowerB ≤ x ≤ upperB.

This function generates a BDD for the function lowerB ≤ x ≤ upperB, where x is an N-bit number, x[0] x[1] ... x[N-1], with 0 the most significant bit (important!). The number of variables N should be sufficient to represent the bounds; otherwise, the bounds are truncated to their N least significant bits. Two BDDs are built bottom-up for lowerB ≤ x and x ≤ upperB, and they are finally conjoined.

Side effects None

See also: Cudd_Xgty

Parameters

dd	DD manager
N	number of x variables
x	array of x variables
lowerB	lower bound
upperB	upper bound

◆ Cudd_CProjection()

DdNode* Cudd_CProjection	(	DdManager *	dd,
		DdNode *	R,
		DdNode *	Y
	)

Computes the compatible projection of R w.r.t. cube Y.

Computes the compatible projection of relation R with respect to cube Y. For a comparison between Cudd_CProjection and Cudd_PrioritySelect, see the documentation of the latter.

Returns: a pointer to the c-projection if successful; NULL otherwise.

Side effects None

See also: Cudd_PrioritySelect

◆ Cudd_Disequality()

DdNode* Cudd_Disequality	(	DdManager *	dd,
		int	N,
		int	c,
		DdNode **	x,
		DdNode **	y
	)

Generates a BDD for the function x - y != c.

This function generates a BDD for the function x -y != c. Both x and y are N-bit numbers, x[0] x[1] ... x[N-1] and y[0] y[1] ... y[N-1], with 0 the most significant bit. The BDD is built bottom-up. It has a linear number of nodes if the variables are ordered as follows: x[0] y[0] x[1] y[1] ... x[N-1] y[N-1].

Side effects None

See also: Cudd_Xgty

Parameters

dd	DD manager
N	number of x and y variables
c	right-hand side constant
x	array of x variables
y	array of y variables

◆ Cudd_Dxygtdxz()

DdNode* Cudd_Dxygtdxz	(	DdManager *	dd,
		int	N,
		DdNode **	x,
		DdNode **	y,
		DdNode **	z
	)

Generates a BDD for the function d(x,y) > d(x,z).

This function generates a BDD for the function d(x,y) > d(x,z); x, y, and z are N-bit numbers, x[0] x[1] ... x[N-1], y[0] y[1] ... y[N-1], and z[0] z[1] ... z[N-1], with 0 the most significant bit. The distance d(x,y) is defined as: $\sum_{i=0}^{N-1}(|x_i - y_i| \cdot 2^{N-i-1})$ . The BDD is built bottom-up. It has 7*N-3 internal nodes, if the variables are ordered as follows: x[0] y[0] z[0] x[1] y[1] z[1] ... x[N-1] y[N-1] z[N-1].

Side effects None

See also: Cudd_PrioritySelect Cudd_Dxygtdyz Cudd_Xgty Cudd_bddAdjPermuteX

Parameters

dd	DD manager
N	number of x, y, and z variables
x	array of x variables
y	array of y variables
z	array of z variables

◆ Cudd_Dxygtdyz()

DdNode* Cudd_Dxygtdyz	(	DdManager *	dd,
		int	N,
		DdNode **	x,
		DdNode **	y,
		DdNode **	z
	)

Generates a BDD for the function d(x,y) > d(y,z).

This function generates a BDD for the function d(x,y) > d(y,z); x, y, and z are N-bit numbers, x[0] x[1] ... x[N-1], y[0] y[1] ... y[N-1], and z[0] z[1] ... z[N-1], with 0 the most significant bit. The distance d(x,y) is defined as: $\sum_{i=0}^{N-1}(|x_i - y_i| \cdot 2^{N-i-1})$ . The BDD is built bottom-up. It has 7*N-3 internal nodes, if the variables are ordered as follows: x[0] y[0] z[0] x[1] y[1] z[1] ... x[N-1] y[N-1] z[N-1].

Side effects None

See also: Cudd_PrioritySelect Cudd_Dxygtdxz Cudd_Xgty Cudd_bddAdjPermuteX

Parameters

dd	DD manager
N	number of x, y, and z variables
x	array of x variables
y	array of y variables
z	array of z variables

◆ Cudd_Inequality()

DdNode* Cudd_Inequality	(	DdManager *	dd,
		int	N,
		int	c,
		DdNode **	x,
		DdNode **	y
	)

Generates a BDD for the function x - y ≥ c.

This function generates a BDD for the function x -y ≥ c. Both x and y are N-bit numbers, x[0] x[1] ... x[N-1] and y[0] y[1] ... y[N-1], with 0 the most significant bit. The BDD is built bottom-up. It has a linear number of nodes if the variables are ordered as follows: x[0] y[0] x[1] y[1] ... x[N-1] y[N-1].

Side effects None

See also: Cudd_Xgty

Parameters

dd	DD manager
N	number of x and y variables
c	right-hand side constant
x	array of x variables
y	array of y variables

◆ Cudd_MinHammingDist()

int Cudd_MinHammingDist	(	DdManager *	dd,
		DdNode *	f,
		int *	minterm,
		int	upperBound
	)

Returns the minimum Hamming distance between f and minterm.

Returns the minimum Hamming distance between the minterms of a function f and a reference minterm. The function is given as a BDD; the minterm is given as an array of integers, one for each variable in the manager.

Returns: the minimum distance if it is less than the upper bound; the upper bound if the minimum distance is at least as large; CUDD_OUT_OF_MEM in case of failure.

Side effects None

See also: Cudd_addHamming Cudd_bddClosestCube

Parameters

dd	DD manager
f	function to examine
minterm	reference minterm
upperBound	distance above which an approximate answer is OK

◆ Cudd_PrioritySelect()

DdNode* Cudd_PrioritySelect	(	DdManager *	dd,
		DdNode *	R,
		DdNode **	x,
		DdNode **	y,
		DdNode **	z,
		DdNode *	Pi,
		int	n,
		DD_PRFP	Pifunc
	)

Selects pairs from R using a priority function.

Selects pairs from a relation R(x,y) (given as a BDD) in such a way that a given x appears in one pair only. Uses a priority function to determine which y should be paired to a given x. Three of the arguments–x, y, and z–are vectors of BDD variables. The first two are the variables on which R depends. The third vector is a vector of auxiliary variables, used during the computation. This vector is optional. If a NULL value is passed instead, Cudd_PrioritySelect will create the working variables on the fly. The sizes of x and y (and z if it is not NULL) should equal n. The priority function Pi can be passed as a BDD, or can be built by Cudd_PrioritySelect. If NULL is passed instead of a DdNode *, parameter Pifunc is used by Cudd_PrioritySelect to build a BDD for the priority function. (Pifunc is a pointer to a C function.) If Pi is not NULL, then Pifunc is ignored. Pifunc should have the same interface as the standard priority functions (e.g., Cudd_Dxygtdxz). Cudd_PrioritySelect and Cudd_CProjection can sometimes be used interchangeably. Specifically, calling Cudd_PrioritySelect with Cudd_Xgty as Pifunc produces the same result as calling Cudd_CProjection with the all-zero minterm as reference minterm. However, depending on the application, one or the other may be preferable:

When extracting representatives from an equivalence relation, Cudd_CProjection has the advantage of nor requiring the auxiliary variables.
When computing matchings in general bipartite graphs, Cudd_PrioritySelect normally obtains better results because it can use more powerful matching schemes (e.g., Cudd_Dxygtdxz).

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

Side effects If called with z == NULL, will create new variables in: the manager.

See also: Cudd_Dxygtdxz Cudd_Dxygtdyz Cudd_Xgty Cudd_bddAdjPermuteX Cudd_CProjection

Parameters

dd	manager
R	BDD of the relation
x	array of x variables
y	array of y variables
z	array of z variables (optional: may be NULL)
Pi	BDD of the priority function (optional: may be NULL)
n	size of x, y, and z
Pifunc	function used to build Pi if it is NULL

◆ Cudd_Xeqy()

DdNode* Cudd_Xeqy	(	DdManager *	dd,
		int	N,
		DdNode **	x,
		DdNode **	y
	)

Generates a BDD for the function x==y.

This function generates a BDD for the function x==y. Both x and y are N-bit numbers, x[0] x[1] ... x[N-1] and y[0] y[1] ... y[N-1]. The BDD is built bottom-up. It has 3*N-1 internal nodes, if the variables are ordered as follows: x[0] y[0] x[1] y[1] ... x[N-1] y[N-1].

Side effects None

See also: Cudd_addXeqy

Parameters

dd	DD manager
N	number of x and y variables
x	array of x variables
y	array of y variables

◆ Cudd_Xgty()

DdNode* Cudd_Xgty	(	DdManager *	dd,
		int	N,
		DdNode **	z,
		DdNode **	x,
		DdNode **	y
	)

Generates a BDD for the function x > y.

This function generates a BDD for the function x > y. Both x and y are N-bit numbers, x[0] x[1] ... x[N-1] and y[0] y[1] ... y[N-1], with 0 the most significant bit. The BDD is built bottom-up. It has 3*N-1 internal nodes, if the variables are ordered as follows: x[0] y[0] x[1] y[1] ... x[N-1] y[N-1]. Argument z is not used by Cudd_Xgty: it is included to make it call-compatible to Cudd_Dxygtdxz and Cudd_Dxygtdyz.

Side effects None

See also: Cudd_PrioritySelect Cudd_Dxygtdxz Cudd_Dxygtdyz

Parameters

dd	DD manager
N	number of x and y variables
z	array of z variables: unused
x	array of x variables
y	array of y variables

◆ cuddBddClosestCube()

DdNode* cuddBddClosestCube	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	g,
		CUDD_VALUE_TYPE	bound
	)

Performs the recursive step of Cudd_bddClosestCube.

The procedure uses a four-way recursion to examine all four combinations of cofactors of f and g according to the following formula.

H(f,g) = min(H(ft,gt), H(fe,ge), H(ft,ge)+1, H(fe,gt)+1)

Bounding is based on the following observations.

If we already found two points at distance 0, there is no point in continuing. Furthermore,
If F == not(G) then the best we can hope for is a minimum distance of 1. If we have already found two points at distance 1, there is no point in continuing. (Indeed, H(F,G) == 1 in this case. We have to continue, though, to find the cube.)

The variable bound is set at the largest value of the distance that we are still interested in. Therefore, we desist when

(bound == -1) and (F != not(G)) or (bound == 0) and (F == not(G)).

If we were maximally aggressive in using the bound, we would always set the bound to the minimum distance seen thus far minus one. That is, we would maintain the invariant

bound < minD,

except at the very beginning, when we have no value for minD.

However, we do not use bound < minD when examining the two negative cofactors, because we try to find a large cube at minimum distance. To do so, we try to find a cube in the negative cofactors at the same or smaller distance from the cube found in the positive cofactors.

When we compute H(ft,ge) and H(fe,gt) we know that we are going to add 1 to the result of the recursive call to account for the difference in the splitting variable. Therefore, we decrease the bound correspondingly.

Another important observation concerns the need of examining all four pairs of cofators only when both f and g depend on the top variable.

Suppose gt == ge == g. (That is, g does not depend on the top variable.) Then

H(f,g) = min(H(ft,g), H(fe,g), H(ft,g)+1, H(fe,g)+1)
       = min(H(ft,g), H(fe,g)) .

Therefore, under these circumstances, we skip the two "cross" cases.

An interesting feature of this function is the scheme used for caching the results in the global computed table. Since we have a cube and a distance, we combine them to form an ADD. The combination replaces the zero child of the top node of the cube with the negative of the distance. (The use of the negative is to avoid ambiguity with 1.) The degenerate cases (zero and one) are treated specially because the distance is known (0 for one, and infinity for zero).

Returns: the cube if succesful; NULL otherwise.

Side effects None

See also: Cudd_bddClosestCube

◆ cuddCProjectionRecur()

DdNode* cuddCProjectionRecur	(	DdManager *	dd,
		DdNode *	R,
		DdNode *	Y,
		DdNode *	Ysupp
	)

Performs the recursive step of Cudd_CProjection.

Returns: the projection if successful; NULL otherwise.

Side effects None

See also: Cudd_CProjection

◆ cuddMinHammingDistRecur()

static int cuddMinHammingDistRecur	(	DdNode *	f,
		int *	minterm,
		DdHashTable *	table,
		int	upperBound
	)

static

Performs the recursive step of Cudd_MinHammingDist.

It is based on the following identity. Let H(f) be the minimum Hamming distance of the minterms of f from the reference minterm. Then:

H(f) = min(H(f0)+h0,H(f1)+h1)

where f0 and f1 are the two cofactors of f with respect to its top variable; h0 is 1 if the minterm assigns 1 to the top variable of f; h1 is 1 if the minterm assigns 0 to the top variable of f. The upper bound on the distance is used to bound the depth of the recursion.

Returns: the minimum distance unless it exceeds the upper bound or computation fails.

Side effects None

See also: Cudd_MinHammingDist

◆ separateCube()

static DdNode* separateCube	(	DdManager *	dd,
		DdNode *	f,
		CUDD_VALUE_TYPE *	distance
	)

static

Separates cube from distance.

Returns: the cube if successful; NULL otherwise.

Side effects The distance is returned as a side effect.

See also: cuddBddClosestCube createResult

Functions

Detailed Description

Function Documentation

◆ createResult()

◆ Cudd_addHamming()

◆ Cudd_addXeqy()

◆ Cudd_bddClosestCube()

◆ Cudd_bddInterval()

◆ Cudd_CProjection()

◆ Cudd_Disequality()

◆ Cudd_Dxygtdxz()

◆ Cudd_Dxygtdyz()

◆ Cudd_Inequality()

◆ Cudd_MinHammingDist()

◆ Cudd_PrioritySelect()

◆ Cudd_Xeqy()

◆ Cudd_Xgty()

◆ cuddBddClosestCube()

◆ cuddCProjectionRecur()

◆ cuddMinHammingDistRecur()

◆ separateCube()