Utility functions. More...

#include <stddef.h>
#include <float.h>
#include "util.h"
#include "epdInt.h"
#include "cuddInt.h"

Include dependency graph for cuddUtil.c:

Macros
#define	MODULUS1 2147483563

#define	LEQA1 40014

#define	LEQQ1 53668

#define	LEQR1 12211

#define	MODULUS2 2147483399

#define	LEQA2 40692

#define	LEQQ2 52774

#define	LEQR2 3791

#define	STAB_DIV (1 + (MODULUS1 - 1) / STAB_SIZE)

#define	bang(f) ((Cudd_IsComplement(f)) ? '!' : ' ')

Functions
int	Cudd_PrintMinterm (DdManager manager, DdNode node)
	Prints a disjoint sum of products. More...

int	Cudd_bddPrintCover (DdManager dd, DdNode l, DdNode *u)
	Prints a sum of prime implicants of a BDD. More...

int	Cudd_PrintDebug (DdManager dd, DdNode f, int n, int pr)
	Prints to the manager standard output a DD and its statistics. More...

int	Cudd_PrintSummary (DdManager dd, DdNode f, int n, int mode)
	Prints a one-line summary of an ADD or BDD to the manager stdout. More...

int	Cudd_DagSize (DdNode *node)
	Counts the number of nodes in a DD. More...

int	Cudd_EstimateCofactor (DdManager dd, DdNode f, int i, int phase)
	Estimates the number of nodes in a cofactor of a DD. More...

int	Cudd_EstimateCofactorSimple (DdNode *node, int i)
	Estimates the number of nodes in a cofactor of a DD. More...

int	Cudd_SharingSize (DdNode **nodeArray, int n)
	Counts the number of nodes in an array of DDs. More...

double	Cudd_CountMinterm (DdManager manager, DdNode node, int nvars)
	Counts the minterms of an ADD or BDD. More...

double	Cudd_CountPath (DdNode *node)
	Counts the paths of a DD. More...

int	Cudd_EpdCountMinterm (DdManager const manager, DdNode node, int nvars, EpDouble *epd)
	Counts the minterms of an ADD or BDD with extended range. More...

long double	Cudd_LdblCountMinterm (DdManager const manager, DdNode node, int nvars)
	Returns the number of minterms of aa ADD or BDD as a long double. More...

int	Cudd_EpdPrintMinterm (DdManager const dd, DdNode node, int nvars)
	Prints the number of minterms of an ADD or BDD with extended range. More...

double	Cudd_CountPathsToNonZero (DdNode *node)
	Counts the paths to a non-zero terminal of a DD. More...

int	Cudd_SupportIndices (DdManager dd, DdNode f, int **indices)
	Finds the variables on which a DD depends. More...

DdNode *	Cudd_Support (DdManager dd, DdNode f)
	Finds the variables on which a DD depends. More...

int *	Cudd_SupportIndex (DdManager dd, DdNode f)
	Finds the variables on which a DD depends. More...

int	Cudd_SupportSize (DdManager dd, DdNode f)
	Counts the variables on which a DD depends. More...

int	Cudd_VectorSupportIndices (DdManager dd, DdNode F, int n, int *indices)
	Finds the variables on which a set of DDs depends. More...

DdNode *	Cudd_VectorSupport (DdManager dd, DdNode *F, int n)
	Finds the variables on which a set of DDs depends. More...

int *	Cudd_VectorSupportIndex (DdManager dd, DdNode *F, int n)
	Finds the variables on which a set of DDs depends. More...

int	Cudd_VectorSupportSize (DdManager dd, DdNode *F, int n)
	Counts the variables on which a set of DDs depends. More...

int	Cudd_ClassifySupport (DdManager dd, DdNode f, DdNode g, DdNode common, DdNode onlyF, DdNode *onlyG)
	Classifies the variables in the support of two DDs. More...

int	Cudd_CountLeaves (DdNode *node)
	Counts the number of leaves in a DD. More...

int	Cudd_bddPickOneCube (DdManager ddm, DdNode node, char *string)
	Picks one on-set cube randomly from the given DD. More...

DdNode *	Cudd_bddPickOneMinterm (DdManager dd, DdNode f, DdNode **vars, int n)
	Picks one on-set minterm randomly from the given DD. More...

DdNode **	Cudd_bddPickArbitraryMinterms (DdManager dd, DdNode f, DdNode **vars, int n, int k)
	Picks k on-set minterms evenly distributed from given DD. More...

DdNode *	Cudd_SubsetWithMaskVars (DdManager dd, DdNode f, DdNode vars, int nvars, DdNode maskVars, int mvars)
	Extracts a subset from a BDD. More...

DdGen *	Cudd_FirstCube (DdManager dd, DdNode f, int *cube, CUDD_VALUE_TYPE value)
	Finds the first cube of a decision diagram. More...

int	Cudd_NextCube (DdGen gen, int cube, CUDD_VALUE_TYPE value)
	Generates the next cube of a decision diagram onset. More...

DdGen *	Cudd_FirstPrime (DdManager dd, DdNode l, DdNode u, int *cube)
	Finds the first prime of a Boolean function. More...

int	Cudd_NextPrime (DdGen gen, int *cube)
	Generates the next prime of a Boolean function. More...

DdNode *	Cudd_bddComputeCube (DdManager dd, DdNode vars, int phase, int n)
	Computes the cube of an array of BDD variables. More...

DdNode *	Cudd_addComputeCube (DdManager dd, DdNode vars, int phase, int n)
	Computes the cube of an array of ADD variables. More...

DdNode *	Cudd_CubeArrayToBdd (DdManager dd, int array)
	Builds the BDD of a cube from a positional array. More...

int	Cudd_BddToCubeArray (DdManager dd, DdNode cube, int *array)
	Builds a positional array from the BDD of a cube. More...

DdGen *	Cudd_FirstNode (DdManager dd, DdNode f, DdNode **node)
	Finds the first node of a decision diagram. More...

int	Cudd_NextNode (DdGen gen, DdNode *node)
	Finds the next node of a decision diagram. More...

int	Cudd_GenFree (DdGen *gen)
	Frees a CUDD generator. More...

int	Cudd_IsGenEmpty (DdGen *gen)
	Queries the status of a generator. More...

DdNode *	Cudd_IndicesToCube (DdManager dd, int array, int n)
	Builds a cube of BDD variables from an array of indices. More...

void	Cudd_PrintVersion (FILE *fp)
	Prints the package version number. More...

double	Cudd_AverageDistance (DdManager *dd)
	Computes the average distance between adjacent nodes in the manager. More...

int32_t	Cudd_Random (DdManager *dd)
	Portable random number generator. More...

void	Cudd_Srandom (DdManager *dd, int32_t seed)
	Initializer for the portable random number generator. More...

double	Cudd_Density (DdManager dd, DdNode f, int nvars)
	Computes the density of a BDD or ADD. More...

void	Cudd_OutOfMem (size_t size)
	Warns that a memory allocation failed. More...

void	Cudd_OutOfMemSilent (size_t size)
	Doesn not warn that a memory allocation failed. More...

int	cuddP (DdManager dd, DdNode f)
	Prints a DD to the standard output. One line per node is printed. More...

enum st_retval	cuddStCountfree (void key, void value, void *arg)
	Frees the memory used to store the minterm counts recorded in the visited table. More...

int	cuddCollectNodes (DdNode f, st_table visited)
	Recursively collects all the nodes of a DD in a symbol table. More...

DdNodePtr *	cuddNodeArray (DdNode f, int n)
	Recursively collects all the nodes of a DD in an array. More...

static int	dp2 (DdManager dd, DdNode f, st_table *t)
	Performs the recursive step of cuddP. More...

static void	ddPrintMintermAux (DdManager dd, DdNode node, int *list)
	Performs the recursive step of Cudd_PrintMinterm. More...

static int	ddDagInt (DdNode *n)
	Performs the recursive step of Cudd_DagSize. More...

static int	cuddNodeArrayRecur (DdNode f, DdNodePtr table, int index)
	Performs the recursive step of cuddNodeArray. More...

static int	cuddEstimateCofactor (DdManager dd, st_table table, DdNode node, int i, int phase, DdNode *ptr)
	Performs the recursive step of Cudd_CofactorEstimate. More...

static DdNode *	cuddUniqueLookup (DdManager unique, int index, DdNode T, DdNode *E)
	Checks the unique table for the existence of an internal node. More...

static int	cuddEstimateCofactorSimple (DdNode *node, int i)
	Performs the recursive step of Cudd_CofactorEstimateSimple. More...

static double	ddCountMintermAux (DdManager dd, DdNode node, double max, DdHashTable *table)
	Performs the recursive step of Cudd_CountMinterm. More...

static double	ddCountPathAux (DdNode node, st_table table)
	Performs the recursive step of Cudd_CountPath. More...

static int	ddEpdCountMintermAux (DdManager const dd, DdNode node, EpDouble max, EpDouble epd, st_table *table)
	Performs the recursive step of Cudd_EpdCountMinterm. More...

static long double	ddLdblCountMintermAux (DdManager const manager, DdNode node, long double max, st_table *table)
	Performs the recursive step of Cudd_LdblCountMinterm. More...

static double	ddCountPathsToNonZero (DdNode N, st_table table)
	Performs the recursive step of Cudd_CountPathsToNonZero. More...

static void	ddSupportStep (DdNode f, int support)
	Performs the recursive step of Cudd_Support. More...

static void	ddClearFlag (DdNode *f)
	Performs a DFS from f, clearing the LSB of the next pointers. More...

static int	ddLeavesInt (DdNode *n)
	Performs the recursive step of Cudd_CountLeaves. More...

static int	ddPickArbitraryMinterms (DdManager dd, DdNode node, int nvars, int nminterms, char **string)
	Performs the recursive step of Cudd_bddPickArbitraryMinterms. More...

static int	ddPickRepresentativeCube (DdManager dd, DdNode node, double weight, char string)
	Finds a representative cube of a BDD. More...

static enum st_retval	ddEpdFree (void key, void value, void *arg)
	Frees the memory used to store the minterm counts recorded in the visited table. More...

static void	ddFindSupport (DdManager dd, DdNode f, int *SP)
	Recursively find the support of f. More...

static void	ddClearVars (DdManager *dd, int SP)
	Clears visited flags for variables. More...

static int	indexCompare (const void a, const void b)
	Compares indices for qsort. More...

static enum st_retval	ddLdblFree (void key, void value, void *arg)
	Frees the memory used to store the minterm counts recorded in the visited table by Cudd_LdblCountMinterm. More...

Detailed Description

Utility 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

◆ Cudd_addComputeCube()

DdNode* Cudd_addComputeCube	(	DdManager *	dd,
		DdNode **	vars,
		int *	phase,
		int	n
	)

Computes the cube of an array of ADD variables.

If non-null, the phase argument indicates which literal of each variable should appear in the cube. If phase[i] is nonzero, then the positive literal is used. If phase is NULL, the cube is positive unate.

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

Side effects none

See also: Cudd_bddComputeCube

◆ Cudd_AverageDistance()

double Cudd_AverageDistance ( DdManager * dd )

Computes the average distance between adjacent nodes in the manager.

Adjacent nodes are node pairs such that the second node is the then child, else child, or next node in the collision list.

Side effects None

◆ Cudd_bddComputeCube()

DdNode* Cudd_bddComputeCube	(	DdManager *	dd,
		DdNode **	vars,
		int *	phase,
		int	n
	)

Computes the cube of an array of BDD variables.

If non-null, the phase argument indicates which literal of each variable should appear in the cube. If phase[i] is nonzero, then the positive literal is used. If phase is NULL, the cube is positive unate.

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

Side effects None

See also: Cudd_addComputeCube Cudd_IndicesToCube Cudd_CubeArrayToBdd

◆ Cudd_bddPickArbitraryMinterms()

DdNode** Cudd_bddPickArbitraryMinterms	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	vars,
		int	n,
		int	k
	)

Picks k on-set minterms evenly distributed from given DD.

The minterms are in terms of vars. The array vars should contain at least all variables in the support of f; if this condition is not met the minterms built by this procedure may not be contained in f.

Returns

an array of BDDs for the minterms if successful; NULL otherwise. There are three reasons why the procedure may fail:

It may run out of memory;
the function f may be the constant 0;
the minterms may not be contained in f.

Side effects None

See also: Cudd_bddPickOneMinterm Cudd_bddPickOneCube

Parameters

dd	manager
f	function from which to pick k minterms
vars	array of variables
n	size of `vars`
k	number of minterms to find

◆ Cudd_bddPickOneCube()

int Cudd_bddPickOneCube	(	DdManager *	ddm,
		DdNode *	node,
		char *	string
	)

Picks one on-set cube randomly from the given DD.

The cube is written into an array of characters. The array must have at least as many entries as there are variables.

Returns: 1 if successful; 0 otherwise.

Side effects None

See also: Cudd_bddPickOneMinterm

◆ Cudd_bddPickOneMinterm()

DdNode* Cudd_bddPickOneMinterm	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	vars,
		int	n
	)

Picks one on-set minterm randomly from the given DD.

The minterm is in terms of vars. The array vars should contain at least all variables in the support of f; if this condition is not met the minterm built by this procedure may not be contained in f.

Returns

a pointer to the BDD for the minterm if successful; NULL otherwise. There are three reasons why the procedure may fail:

It may run out of memory;
the function f may be the constant 0;
the minterm may not be contained in f.

Side effects None

See also: Cudd_bddPickOneCube

Parameters

dd	manager
f	function from which to pick one minterm
vars	array of variables
n	size of `vars`

◆ Cudd_bddPrintCover()

int Cudd_bddPrintCover	(	DdManager *	dd,
		DdNode *	l,
		DdNode *	u
	)

Prints a sum of prime implicants of a BDD.

Prints a sum of product cover for an incompletely specified function given by a lower bound and an upper bound. Each product is a prime implicant obtained by expanding the product corresponding to a path from node to the constant one. Uses the package default output file.

Returns: 1 if successful; 0 otherwise.

Side effects None

See also: Cudd_PrintMinterm

◆ Cudd_BddToCubeArray()

int Cudd_BddToCubeArray	(	DdManager *	dd,
		DdNode *	cube,
		int *	array
	)

Builds a positional array from the BDD of a cube.

Array must have one entry for each BDD variable. The positional array has 1 in i-th position if the variable of index i appears in true form in the cube; it has 0 in i-th position if the variable of index i appears in complemented form in the cube; finally, it has 2 in i-th position if the variable of index i does not appear in the cube.

Returns: 1 if successful (the BDD is indeed a cube); 0 otherwise.

Side effects The result is in the array passed by reference.

See also: Cudd_CubeArrayToBdd

◆ Cudd_ClassifySupport()

int Cudd_ClassifySupport	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	g,
		DdNode **	common,
		DdNode **	onlyF,
		DdNode **	onlyG
	)

Classifies the variables in the support of two DDs.

Classifies the variables in the support of two DDs f and g, depending on whether they appear in both DDs, only in f, or only in g.

Returns: 1 if successful; 0 otherwise.

Side effects The cubes of the three classes of variables are: returned as side effects.

See also: Cudd_Support Cudd_VectorSupport

Parameters

dd	manager
f	first DD
g	second DD
common	cube of shared variables
onlyF	cube of variables only in f
onlyG	cube of variables only in g

◆ Cudd_CountLeaves()

int Cudd_CountLeaves ( DdNode * node )

Counts the number of leaves in a DD.

Returns: the number of leaves in the DD rooted at node if successful; CUDD_OUT_OF_MEM otherwise.

Side effects None

See also: Cudd_PrintDebug

◆ Cudd_CountMinterm()

double Cudd_CountMinterm	(	DdManager *	manager,
		DdNode *	node,
		int	nvars
	)

Counts the minterms of an ADD or BDD.

The function is assumed to depend on nvars variables. The minterm count is represented as a double; hence overflow is possible. For functions with many variables (more than 1023 if floating point conforms to IEEE 754), one should consider Cudd_ApaCountMinterm() or Cudd_EpdCountMinterm().

Returns: the number of minterms of the function rooted at node if successful; +infinity if the number of minterms is known to be larger than the maximum value representable as a double; (double) CUDD_OUT_OF_MEM otherwise.

Side effects None

See also: Cudd_ApaCountMinterm Cudd_EpdCountMinterm Cudd_LdblCountMinterm Cudd_PrintDebug Cudd_CountPath

◆ Cudd_CountPath()

double Cudd_CountPath ( DdNode * node )

Counts the paths of a DD.

Paths to all terminal nodes are counted. The path count is represented as a double; hence overflow is possible.

Returns: the number of paths of the function rooted at node if successful; (double) CUDD_OUT_OF_MEM otherwise.

Side effects None

See also: Cudd_CountMinterm

◆ Cudd_CountPathsToNonZero()

double Cudd_CountPathsToNonZero ( DdNode * node )

Counts the paths to a non-zero terminal of a DD.

The path count is represented as a double; hence overflow is possible.

Returns: the number of paths of the function rooted at node.

Side effects None

See also: Cudd_CountMinterm Cudd_CountPath

◆ Cudd_CubeArrayToBdd()

DdNode* Cudd_CubeArrayToBdd	(	DdManager *	dd,
		int *	array
	)

Builds the BDD of a cube from a positional array.

The array must have one integer entry for each BDD variable. If the i-th entry is 1, the variable of index i appears in true form in the cube; If the i-th entry is 0, the variable of index i appears complemented in the cube; otherwise the variable does not appear in the cube.

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

Side effects None

See also: Cudd_bddComputeCube Cudd_IndicesToCube Cudd_BddToCubeArray

◆ Cudd_DagSize()

int Cudd_DagSize ( DdNode * node )

Counts the number of nodes in a DD.

Returns: the number of nodes in the graph rooted at node.

Side effects None

See also: Cudd_SharingSize Cudd_PrintDebug

◆ Cudd_Density()

double Cudd_Density	(	DdManager *	dd,
		DdNode *	f,
		int	nvars
	)

Computes the density of a BDD or ADD.

The density is the ratio of the number of minterms to the number of nodes. If 0 is passed as number of variables, the number of variables existing in the manager is used.

Returns: the density if successful; (double) CUDD_OUT_OF_MEM otherwise.

Side effects None

See also: Cudd_CountMinterm Cudd_DagSize

Parameters

dd	manager
f	function whose density is sought
nvars	size of the support of f

◆ Cudd_EpdCountMinterm()

int Cudd_EpdCountMinterm	(	DdManager const *	manager,
		DdNode *	node,
		int	nvars,
		EpDouble *	epd
	)

Counts the minterms of an ADD or BDD with extended range.

The function is assumed to depend on nvars variables. The minterm count is represented as an EpDouble, to allow for any number of variables.

Returns: 0 if successful; CUDD_OUT_OF_MEM otherwise.

Side effects None

See also: Cudd_CountMinterm Cudd_LdblCountMinterm Cudd_ApaCountMinterm Cudd_PrintDebug Cudd_CountPath

◆ Cudd_EpdPrintMinterm()

int Cudd_EpdPrintMinterm	(	DdManager const *	dd,
		DdNode *	node,
		int	nvars
	)

Prints the number of minterms of an ADD or BDD with extended range.

Returns: 1 if successful; 0 otherwise.

Side effects None

See also: Cudd_EpdCountMinterm Cudd_ApaPrintMintermExp

◆ Cudd_EstimateCofactor()

int Cudd_EstimateCofactor	(	DdManager *	dd,
		DdNode *	f,
		int	i,
		int	phase
	)

Estimates the number of nodes in a cofactor of a DD.

This function uses a refinement of the algorithm of Cabodi et al. (ICCAD96). The refinement allows the procedure to account for part of the recombination that may occur in the part of the cofactor above the cofactoring variable. This procedure does not create any new node. It does keep a small table of results; therefore it may run out of memory. If this is a concern, one should use Cudd_EstimateCofactorSimple, which is faster, does not allocate any memory, but is less accurate.

Returns: an estimate of the number of nodes in a cofactor of the graph rooted at node with respect to the variable whose index is i. In case of failure, returns CUDD_OUT_OF_MEM.

Side effects None

See also: Cudd_DagSize Cudd_EstimateCofactorSimple

Parameters

dd	manager
f	function
i	index of variable
phase	1: positive; 0: negative

◆ Cudd_EstimateCofactorSimple()

int Cudd_EstimateCofactorSimple	(	DdNode *	node,
		int	i
	)

Estimates the number of nodes in a cofactor of a DD.

Returns an estimate of the number of nodes in the positive cofactor of the graph rooted at node with respect to the variable whose index is i. This procedure implements with minor changes the algorithm of Cabodi et al. (ICCAD96). It does not allocate any memory, it does not change the state of the manager, and it is fast. However, it has been observed to overestimate the size of the cofactor by as much as a factor of 2.

Side effects None

See also: Cudd_DagSize

◆ Cudd_FirstCube()

DdGen* Cudd_FirstCube	(	DdManager *	dd,
		DdNode *	f,
		int **	cube,
		CUDD_VALUE_TYPE *	value
	)

Finds the first cube of a decision diagram.

Defines an iterator on the onset of a decision diagram and finds its first cube.

A cube is represented as an array of literals, which are integers in {0, 1, 2}; 0 represents a complemented literal, 1 represents an uncomplemented literal, and 2 stands for don't care. The enumeration produces a disjoint cover of the function associated with the diagram. The size of the array equals the number of variables in the manager at the time Cudd_FirstCube is called.

For each cube, a value is also returned. This value is always 1 for a BDD, while it may be different from 1 for an ADD. For BDDs, the offset is the set of cubes whose value is the logical zero. For ADDs, the offset is the set of cubes whose value is the background value. The cubes of the offset are not enumerated.

Returns: a generator that contains the information necessary to continue the enumeration if successful; NULL otherwise.

Side effects The first cube and its value are returned as side effects.

See also: Cudd_ForeachCube Cudd_NextCube Cudd_GenFree Cudd_IsGenEmpty Cudd_FirstNode

◆ Cudd_FirstNode()

DdGen* Cudd_FirstNode	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	node
	)

Finds the first node of a decision diagram.

Defines an iterator on the nodes of a decision diagram and finds its first node. The nodes are enumerated in a reverse topological order, so that a node is always preceded in the enumeration by its descendants.

Returns: a generator that contains the information necessary to continue the enumeration if successful; NULL otherwise.

Side effects The first node is returned as a side effect.

See also: Cudd_ForeachNode Cudd_NextNode Cudd_GenFree Cudd_IsGenEmpty Cudd_FirstCube

◆ Cudd_FirstPrime()

DdGen* Cudd_FirstPrime	(	DdManager *	dd,
		DdNode *	l,
		DdNode *	u,
		int **	cube
	)

Finds the first prime of a Boolean function.

Defines an iterator on a pair of BDDs describing a (possibly incompletely specified) Boolean functions and finds the first cube of a cover of the function.

The two argument BDDs are the lower and upper bounds of an interval. It is a mistake to call this function with a lower bound that is not less than or equal to the upper bound.

A cube is represented as an array of literals, which are integers in {0, 1, 2}; 0 represents a complemented literal, 1 represents an uncomplemented literal, and 2 stands for don't care. The enumeration produces a prime and irredundant cover of the function associated with the two BDDs. The size of the array equals the number of variables in the manager at the time Cudd_FirstCube is called.

This iterator can only be used on BDDs.

Returns: a generator that contains the information necessary to continue the enumeration if successful; NULL otherwise.

Side effects The first cube is returned as side effect.

See also: Cudd_ForeachPrime Cudd_NextPrime Cudd_GenFree Cudd_IsGenEmpty Cudd_FirstCube Cudd_FirstNode

◆ Cudd_GenFree()

int Cudd_GenFree ( DdGen * gen )

Frees a CUDD generator.

Returns: always 0.

Side effects None

See also: Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube Cudd_FirstNode Cudd_NextNode Cudd_IsGenEmpty

◆ Cudd_IndicesToCube()

DdNode* Cudd_IndicesToCube	(	DdManager *	dd,
		int *	array,
		int	n
	)

Builds a cube of BDD variables from an array of indices.

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

Side effects None

See also: Cudd_bddComputeCube Cudd_CubeArrayToBdd

◆ Cudd_IsGenEmpty()

int Cudd_IsGenEmpty ( DdGen * gen )

Queries the status of a generator.

Returns: 1 if the generator is empty or NULL; 0 otherswise.

Side effects None

See also: Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube Cudd_FirstNode Cudd_NextNode Cudd_GenFree

◆ Cudd_LdblCountMinterm()

long double Cudd_LdblCountMinterm	(	DdManager const *	manager,
		DdNode *	node,
		int	nvars
	)

Returns the number of minterms of aa ADD or BDD as a long double.

On systems where double and long double are the same type, Cudd_CountMinterm() is preferable. On systems where long double values have 15-bit exponents, this function avoids overflow for up to 16383 variables. It applies scaling to try to avoid overflow when the number of variables is larger than 16383, but smaller than 32764.

Returns: The nimterm count if successful; +infinity if the number is known to be too large for representation as a long double; (long double)CUDD_OUT_OF_MEM otherwise.

See also: Cudd_CountMinterm Cudd_EpdCountMinterm Cudd_ApaCountMinterm

◆ Cudd_NextCube()

int Cudd_NextCube	(	DdGen *	gen,
		int **	cube,
		CUDD_VALUE_TYPE *	value
	)

Generates the next cube of a decision diagram onset.

Returns: 0 if the enumeration is completed; 1 otherwise.

Side effects The cube and its value are returned as side effects. The: generator is modified.

See also: Cudd_ForeachCube Cudd_FirstCube Cudd_GenFree Cudd_IsGenEmpty Cudd_NextNode

◆ Cudd_NextNode()

int Cudd_NextNode	(	DdGen *	gen,
		DdNode **	node
	)

Finds the next node of a decision diagram.

Returns: 0 if the enumeration is completed; 1 otherwise.

Side effects The next node is returned as a side effect.

See also: Cudd_ForeachNode Cudd_FirstNode Cudd_GenFree Cudd_IsGenEmpty Cudd_NextCube

◆ Cudd_NextPrime()

int Cudd_NextPrime	(	DdGen *	gen,
		int **	cube
	)

Generates the next prime of a Boolean function.

Returns: 0 if the enumeration is completed; 1 otherwise.

Side effects The cube and is returned as side effects. The: generator is modified.

See also: Cudd_ForeachPrime Cudd_FirstPrime Cudd_GenFree Cudd_IsGenEmpty Cudd_NextCube Cudd_NextNode

◆ Cudd_OutOfMem()

void Cudd_OutOfMem ( size_t size )

Warns that a memory allocation failed.

This function can be used as replacement of MMout_of_memory to prevent the safe_mem functions of the util package from exiting when malloc returns NULL. One possible use is in case of discretionary allocations; for instance, an allocation of memory to enlarge the computed table.

Side effects None

See also: Cudd_OutOfMemSilent Cudd_RegisterOutOfMemoryCallback

Parameters

size	size of the allocation that failed

◆ Cudd_OutOfMemSilent()

void Cudd_OutOfMemSilent ( size_t size )

Doesn not warn that a memory allocation failed.

This function can be used as replacement of MMout_of_memory to prevent the safe_mem functions of the util package from exiting when malloc returns NULL. One possible use is in case of discretionary allocations; for instance, an allocation of memory to enlarge the computed table.

Side effects None

See also: Cudd_OutOfMem Cudd_RegisterOutOfMemoryCallback

Parameters

size	size of the allocation that failed

◆ Cudd_PrintDebug()

int Cudd_PrintDebug	(	DdManager *	dd,
		DdNode *	f,
		int	n,
		int	pr
	)

Prints to the manager standard output a DD and its statistics.

The statistics include the number of nodes, the number of leaves, and the number of minterms. (The number of minterms is the number of assignments to the variables that cause the function to be different from the logical zero (for BDDs) and from the background value (for ADDs.) The statistics are printed if pr > 0. Specifically:

pr = 0 : prints nothing
pr = 1 : prints counts of nodes and minterms
pr = 2 : prints counts + disjoint sum of product
pr = 3 : prints counts + list of nodes
pr > 3 : prints counts + disjoint sum of product + list of nodes

For the purpose of counting the number of minterms, the function is supposed to depend on n variables.

Returns: 1 if successful; 0 otherwise.

Side effects None

See also: Cudd_DagSize Cudd_CountLeaves Cudd_CountMinterm Cudd_PrintMinterm

◆ Cudd_PrintMinterm()

int Cudd_PrintMinterm	(	DdManager *	manager,
		DdNode *	node
	)

Prints a disjoint sum of products.

Prints a disjoint sum of product cover for the function rooted at node. Each product corresponds to a path from node to a leaf node different from the logical zero, and different from the background value. Uses the package default output file.

Returns: 1 if successful; 0 otherwise.

Side effects None

See also: Cudd_PrintDebug Cudd_bddPrintCover

◆ Cudd_PrintSummary()

int Cudd_PrintSummary	(	DdManager *	dd,
		DdNode *	f,
		int	n,
		int	mode
	)

Prints a one-line summary of an ADD or BDD to the manager stdout.

The summary includes the number of nodes, the number of leaves, and the number of minterms. The number of minterms is computed with arbitrary precision unlike Cudd_PrintDebug(). For the purpose of counting minterms, the function f is supposed to depend on n variables.

Returns: 1 if successful; 0 otherwise.

See also: Cudd_PrintDebug Cudd_ApaPrintMinterm Cudd_ApaPrintMintermExp

Parameters

dd	manager
f	DD to be summarized
n	number of variables for minterm computation
mode	integer (0) or exponential (1) format

◆ Cudd_PrintVersion()

void Cudd_PrintVersion ( FILE * fp )

Prints the package version number.

Side effects None

◆ Cudd_Random()

int32_t Cudd_Random ( DdManager * dd )

Portable random number generator.

Based on ran2 from "Numerical Recipes in C." It is a long period (> 2 * 10^18) random number generator of L'Ecuyer with Bays-Durham shuffle. The random generator can be explicitly initialized by calling Cudd_Srandom. If no explicit initialization is performed, then the seed 1 is assumed.

Returns: a long integer uniformly distributed between 0 and 2147483561 (inclusive of the endpoint values).

Side effects None

See also: Cudd_Srandom

◆ Cudd_SharingSize()

int Cudd_SharingSize	(	DdNode **	nodeArray,
		int	n
	)

Counts the number of nodes in an array of DDs.

Shared nodes are counted only once.

Returns: the total number of nodes.

Side effects None

See also: Cudd_DagSize

◆ Cudd_Srandom()

void Cudd_Srandom	(	DdManager *	dd,
		int32_t	seed
	)

Initializer for the portable random number generator.

Based on ran2 in "Numerical Recipes in C." The input is the seed for the generator. If it is negative, its absolute value is taken as seed. If it is 0, then 1 is taken as seed. The initialized sets up the two recurrences used to generate a long-period stream, and sets up the shuffle table.

Side effects None

See also: Cudd_Random

◆ Cudd_SubsetWithMaskVars()

DdNode* Cudd_SubsetWithMaskVars	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	vars,
		int	nvars,
		DdNode **	maskVars,
		int	mvars
	)

Extracts a subset from a BDD.

Extracts a subset from a BDD in the following procedure.

Compute the weight for each mask variable by counting the number of minterms for both positive and negative cofactors of the BDD with respect to each mask variable. (weight = # positive - # negative)
Find a representative cube of the BDD by using the weight. From the top variable of the BDD, for each variable, if the weight is greater than 0.0, choose THEN branch, othereise ELSE branch, until meeting the constant 1.
Quantify out the variables not in maskVars from the representative cube and if a variable in maskVars is don't care, replace the variable with a constant(1 or 0) depending on the weight.
Make a subset of the BDD by multiplying with the modified cube.

Side effects None

Parameters

dd	manager
f	function from which to pick a cube
vars	array of variables
nvars	size of `vars`
maskVars	array of variables
mvars	size of `maskVars`

◆ Cudd_Support()

DdNode* Cudd_Support	(	DdManager *	dd,
		DdNode *	f
	)

Finds the variables on which a DD depends.

Returns: a BDD consisting of the product of the variables if successful; NULL otherwise.

Side effects None

See also: Cudd_VectorSupport Cudd_ClassifySupport

Parameters

dd	manager
f	DD whose support is sought

◆ Cudd_SupportIndex()

int* Cudd_SupportIndex	(	DdManager *	dd,
		DdNode *	f
	)

Finds the variables on which a DD depends.

Returns: an index array of the variables if successful; NULL otherwise. The size of the array equals the number of variables in the manager. Each entry of the array is 1 if the corresponding variable is in the support of the DD and 0 otherwise.

Side effects None

See also: Cudd_Support Cudd_SupportIndices Cudd_ClassifySupport

Parameters

dd	manager
f	DD whose support is sought

◆ Cudd_SupportIndices()

int Cudd_SupportIndices	(	DdManager *	dd,
		DdNode *	f,
		int **	indices
	)

Finds the variables on which a DD depends.

Returns: the number of variables if successful; CUDD_OUT_OF_MEM otherwise.

Side effects The indices of the support variables are returned as: side effects. If the function is constant, no array is allocated.

See also: Cudd_Support Cudd_SupportIndex Cudd_VectorSupportIndices

Parameters

dd	manager
f	DD whose support is sought
indices	array containing (on return) the indices

◆ Cudd_SupportSize()

int Cudd_SupportSize	(	DdManager *	dd,
		DdNode *	f
	)

Counts the variables on which a DD depends.

Returns: the variables on which a DD depends.

Side effects None

See also: Cudd_Support Cudd_SupportIndices

Parameters

dd	manager
f	DD whose support size is sought

◆ Cudd_VectorSupport()

DdNode* Cudd_VectorSupport	(	DdManager *	dd,
		DdNode **	F,
		int	n
	)

Finds the variables on which a set of DDs depends.

The set must contain either BDDs and ADDs, or ZDDs.

Returns: a BDD consisting of the product of the variables if successful; NULL otherwise.

Side effects None

See also: Cudd_Support Cudd_ClassifySupport

Parameters

dd	manager
F	array of DDs whose support is sought
n	size of the array

◆ Cudd_VectorSupportIndex()

int* Cudd_VectorSupportIndex	(	DdManager *	dd,
		DdNode **	F,
		int	n
	)

Finds the variables on which a set of DDs depends.

The set must contain either BDDs and ADDs, or ZDDs.

Returns: an index array of the variables if successful; NULL otherwise.

Side effects None

See also: Cudd_SupportIndex Cudd_VectorSupport Cudd_VectorSupportIndices

Parameters

dd	manager
F	array of DDs whose support is sought
n	size of the array

◆ Cudd_VectorSupportIndices()

int Cudd_VectorSupportIndices	(	DdManager *	dd,
		DdNode **	F,
		int	n,
		int **	indices
	)

Finds the variables on which a set of DDs depends.

The set must contain either BDDs and ADDs, or ZDDs.

Returns: the number of variables if successful; CUDD_OUT_OF_MEM otherwise.

Side effects The indices of the support variables are returned as: side effects. If the function is constant, no array is allocated.

See also: Cudd_Support Cudd_SupportIndex Cudd_VectorSupportIndices

Parameters

dd	manager
F	DD whose support is sought
n	size of the array
indices	array containing (on return) the indices

◆ Cudd_VectorSupportSize()

int Cudd_VectorSupportSize	(	DdManager *	dd,
		DdNode **	F,
		int	n
	)

Counts the variables on which a set of DDs depends.

The set must contain either BDDs and ADDs, or ZDDs.

Returns: the number of variables on which a set of DDs depends.

Side effects None

See also: Cudd_VectorSupport Cudd_SupportSize

Parameters

dd	manager
F	array of DDs whose support is sought
n	size of the array

◆ cuddCollectNodes()

int cuddCollectNodes	(	DdNode *	f,
		st_table *	visited
	)

Recursively collects all the nodes of a DD in a symbol table.

Traverses the DD f and collects all its nodes in a symbol table. f is assumed to be a regular pointer and cuddCollectNodes guarantees this assumption in the recursive calls.

Returns: 1 in case of success; 0 otherwise.

Side effects None

◆ cuddEstimateCofactor()

static int cuddEstimateCofactor	(	DdManager *	dd,
		st_table *	table,
		DdNode *	node,
		int	i,
		int	phase,
		DdNode **	ptr
	)

static

Performs the recursive step of Cudd_CofactorEstimate.

Uses the least significant bit of the next field as visited flag. node is supposed to be regular; the invariant is maintained by this procedure.

Returns: an estimate of the number of nodes in the DD of a cofactor of node.

Side effects None

◆ cuddEstimateCofactorSimple()

static int cuddEstimateCofactorSimple	(	DdNode *	node,
		int	i
	)

static

Performs the recursive step of Cudd_CofactorEstimateSimple.

Uses the least significant bit of the next field as visited flag. node is supposed to be regular; the invariant is maintained by this procedure.

Returns: an estimate of the number of nodes in the DD of the positive cofactor of node.

Side effects None

◆ cuddNodeArray()

DdNodePtr* cuddNodeArray	(	DdNode *	f,
		int *	n
	)

Recursively collects all the nodes of a DD in an array.

Traverses the DD f and collects all its nodes in an array. The caller should free the array returned by cuddNodeArray. The nodes are collected in reverse topological order, so that a node is always preceded in the array by all its descendants.

Returns: a pointer to the array of nodes in case of success; NULL otherwise.

Side effects The number of nodes is returned as a side effect.

See also: Cudd_FirstNode

◆ cuddNodeArrayRecur()

static int cuddNodeArrayRecur	(	DdNode *	f,
		DdNodePtr *	table,
		int	index
	)

static

Performs the recursive step of cuddNodeArray.

node is supposed to be regular; the invariant is maintained by this procedure.

Returns: an the number of nodes in the DD.

Side effects Clears the least significant bit of the next field that: was used as visited flag by cuddNodeArrayRecur when counting the nodes.

◆ cuddP()

int cuddP	(	DdManager *	dd,
		DdNode *	f
	)

Prints a DD to the standard output. One line per node is printed.

Returns: 1 if successful; 0 otherwise.

Side effects None

See also: Cudd_PrintDebug

◆ cuddStCountfree()

enum st_retval cuddStCountfree	(	void *	key,
		void *	value,
		void *	arg
	)

Frees the memory used to store the minterm counts recorded in the visited table.

Returns: ST_CONTINUE.

Side effects None

◆ cuddUniqueLookup()

static DdNode* cuddUniqueLookup	(	DdManager *	unique,
		int	index,
		DdNode *	T,
		DdNode *	E
	)

static

Checks the unique table for the existence of an internal node.

Returns: a pointer to the node if it is in the table; NULL otherwise.

Side effects None

See also: cuddUniqueInter

◆ ddClearFlag()

static void ddClearFlag ( DdNode * f )

static

Performs a DFS from f, clearing the LSB of the next pointers.

Side effects None

See also: ddSupportStep ddFindSupport ddLeavesInt ddDagInt

◆ ddClearVars()

static void ddClearVars	(	DdManager *	dd,
		int	SP
	)

static

Clears visited flags for variables.

Side effects None

◆ ddCountMintermAux()

static double ddCountMintermAux	(	DdManager *	dd,
		DdNode *	node,
		double	max,
		DdHashTable *	table
	)

static

Performs the recursive step of Cudd_CountMinterm.

It is based on the following identity. Let |f| be the number of minterms of f. Then:

|f| = (|f0|+|f1|)/2

where f0 and f1 are the two cofactors of f. Does not use the identity |f'| = max - |f|, to minimize loss of accuracy due to roundoff.

Returns: the number of minterms of the function rooted at node.

Side effects None

◆ ddCountPathAux()

static double ddCountPathAux	(	DdNode *	node,
		st_table *	table
	)

static

Performs the recursive step of Cudd_CountPath.

It is based on the following identity. Let |f| be the number of paths of f. Then:

|f| = |f0|+|f1|

where f0 and f1 are the two cofactors of f. Uses the identity |f'| = |f|, to improve the utilization of the (local) cache.

Returns: the number of paths of the function rooted at node.

Side effects None

◆ ddCountPathsToNonZero()

static double ddCountPathsToNonZero	(	DdNode *	N,
		st_table *	table
	)

static

Performs the recursive step of Cudd_CountPathsToNonZero.

It is based on the following identity. Let |f| be the number of paths of f. Then:

|f| = |f0|+|f1|

where f0 and f1 are the two cofactors of f.

Returns: the number of paths of the function rooted at node.

Side effects None

◆ ddDagInt()

static int ddDagInt ( DdNode * n )

static

Performs the recursive step of Cudd_DagSize.

Returns: the number of nodes in the graph rooted at n.

Side effects None

◆ ddEpdCountMintermAux()

static int ddEpdCountMintermAux	(	DdManager const *	dd,
		DdNode *	node,
		EpDouble *	max,
		EpDouble *	epd,
		st_table *	table
	)

static

Performs the recursive step of Cudd_EpdCountMinterm.

It is based on the following identity. Let |f| be the number of minterms of f. Then:

|f| = (|f0|+|f1|)/2

where f0 and f1 are the two cofactors of f. Does not use the identity |f'| = max - |f|, to minimize loss of accuracy due to roundoff.

Returns: the number of minterms of the function rooted at node.

Side effects None

◆ ddEpdFree()

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

static

Frees the memory used to store the minterm counts recorded in the visited table.

Returns: ST_CONTINUE.

Side effects None

◆ ddFindSupport()

static void ddFindSupport	(	DdManager *	dd,
		DdNode *	f,
		int *	SP
	)

static

Recursively find the support of f.

This function uses the LSB of the next field of the nodes of f as visited flag. It also uses the LSB of the next field of the variables as flag to remember whether a certain index has already been seen. Finally, it uses the manager stack to record all seen indices.

Side effects The stack pointer SP is modified by side-effect. The next: fields are changed and need to be reset.

◆ ddLdblCountMintermAux()

static long double ddLdblCountMintermAux	(	DdManager const *	manager,
		DdNode *	node,
		long double	max,
		st_table *	table
	)

static

Performs the recursive step of Cudd_LdblCountMinterm.

It is based on the following identity. Let |f| be the number of minterms of f. Then:

|f| = (|f0|+|f1|)/2

where f0 and f1 are the two cofactors of f. Does not use the identity |f'| = max - |f|, to minimize loss of accuracy due to roundoff.

Returns: the number of minterms of the function rooted at node.

Side effects None

◆ ddLdblFree()

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

static

Frees the memory used to store the minterm counts recorded in the visited table by Cudd_LdblCountMinterm.

Returns: ST_CONTINUE.

Side effects None

◆ ddLeavesInt()

static int ddLeavesInt ( DdNode * n )

static

Performs the recursive step of Cudd_CountLeaves.

Returns: the number of leaves in the DD rooted at n.

Side effects None

See also: Cudd_CountLeaves

◆ ddPickArbitraryMinterms()

static int ddPickArbitraryMinterms	(	DdManager *	dd,
		DdNode *	node,
		int	nvars,
		int	nminterms,
		char **	string
	)

static

Performs the recursive step of Cudd_bddPickArbitraryMinterms.

Returns: 1 if successful; 0 otherwise.

Side effects none

See also: Cudd_bddPickArbitraryMinterms

◆ ddPickRepresentativeCube()

static int ddPickRepresentativeCube	(	DdManager *	dd,
		DdNode *	node,
		double *	weight,
		char *	string
	)

static

Finds a representative cube of a BDD.

Finds a representative cube of a BDD with the weight of each variable. From the top variable, if the weight is greater than or equal to 0.0, choose THEN branch unless the child is the constant 0. Otherwise, choose ELSE branch unless the child is the constant 0.

Side effects Cudd_SubsetWithMaskVars Cudd_bddPickOneCube

◆ ddPrintMintermAux()

static void ddPrintMintermAux	(	DdManager *	dd,
		DdNode *	node,
		int *	list
	)

static

Performs the recursive step of Cudd_PrintMinterm.

Side effects None

Parameters

dd	manager
node	current node
list	current recursion path

◆ ddSupportStep()

static void ddSupportStep	(	DdNode *	f,
		int *	support
	)

static

Performs the recursive step of Cudd_Support.

Performs a DFS from f. The support is accumulated in supp as a side effect. Uses the LSB of the then pointer as visited flag.

Side effects None

See also: ddClearFlag

◆ dp2()

static int dp2	(	DdManager *	dd,
		DdNode *	f,
		st_table *	t
	)

static

Performs the recursive step of cuddP.

Returns: 1 in case of success; 0 otherwise.

Side effects None

◆ indexCompare()

static int indexCompare	(	const void *	a,
		const void *	b
	)

static

Compares indices for qsort.

Subtracting these integers cannot produce overflow, because they are non-negative.

Side effects None

Macros

Functions

Detailed Description

Function Documentation

◆ Cudd_addComputeCube()

◆ Cudd_AverageDistance()

◆ Cudd_bddComputeCube()

◆ Cudd_bddPickArbitraryMinterms()

◆ Cudd_bddPickOneCube()

◆ Cudd_bddPickOneMinterm()

◆ Cudd_bddPrintCover()

◆ Cudd_BddToCubeArray()

◆ Cudd_ClassifySupport()

◆ Cudd_CountLeaves()

◆ Cudd_CountMinterm()

◆ Cudd_CountPath()

◆ Cudd_CountPathsToNonZero()

◆ Cudd_CubeArrayToBdd()

◆ Cudd_DagSize()

◆ Cudd_Density()

◆ Cudd_EpdCountMinterm()

◆ Cudd_EpdPrintMinterm()

◆ Cudd_EstimateCofactor()

◆ Cudd_EstimateCofactorSimple()

◆ Cudd_FirstCube()

◆ Cudd_FirstNode()

◆ Cudd_FirstPrime()

◆ Cudd_GenFree()

◆ Cudd_IndicesToCube()

◆ Cudd_IsGenEmpty()

◆ Cudd_LdblCountMinterm()

◆ Cudd_NextCube()

◆ Cudd_NextNode()

◆ Cudd_NextPrime()

◆ Cudd_OutOfMem()

◆ Cudd_OutOfMemSilent()

◆ Cudd_PrintDebug()

◆ Cudd_PrintMinterm()

◆ Cudd_PrintSummary()

◆ Cudd_PrintVersion()

◆ Cudd_Random()

◆ Cudd_SharingSize()

◆ Cudd_Srandom()

◆ Cudd_SubsetWithMaskVars()

◆ Cudd_Support()

◆ Cudd_SupportIndex()

◆ Cudd_SupportIndices()

◆ Cudd_SupportSize()

◆ Cudd_VectorSupport()

◆ Cudd_VectorSupportIndex()

◆ Cudd_VectorSupportIndices()

◆ Cudd_VectorSupportSize()

◆ cuddCollectNodes()

◆ cuddEstimateCofactor()

◆ cuddEstimateCofactorSimple()

◆ cuddNodeArray()

◆ cuddNodeArrayRecur()

◆ cuddP()

◆ cuddStCountfree()

◆ cuddUniqueLookup()

◆ ddClearFlag()

◆ ddClearVars()

◆ ddCountMintermAux()

◆ ddCountPathAux()

◆ ddCountPathsToNonZero()

◆ ddDagInt()

◆ ddEpdCountMintermAux()

◆ ddEpdFree()

◆ ddFindSupport()

◆ ddLdblCountMintermAux()

◆ ddLdblFree()

◆ ddLeavesInt()

◆ ddPickArbitraryMinterms()

◆ ddPickRepresentativeCube()

◆ ddPrintMintermAux()

◆ ddSupportStep()

◆ dp2()

◆ indexCompare()