cudd/cuddUtil.c File Reference

Utility functions. More...

#include <stddef.h>
#include <float.h>
#include "util.h"
#include "epdInt.h"
#include "cuddInt.h"
Include dependency graph for cuddUtil.c:

Defines

#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.
int Cudd_bddPrintCover (DdManager *dd, DdNode *l, DdNode *u)
 Prints a sum of prime implicants of a BDD.
int Cudd_PrintDebug (DdManager *dd, DdNode *f, int n, int pr)
 Prints to the manager standard output a DD and its statistics.
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.
int Cudd_DagSize (DdNode *node)
 Counts the number of nodes in a DD.
int Cudd_EstimateCofactor (DdManager *dd, DdNode *f, int i, int phase)
 Estimates the number of nodes in a cofactor of a DD.
int Cudd_EstimateCofactorSimple (DdNode *node, int i)
 Estimates the number of nodes in a cofactor of a DD.
int Cudd_SharingSize (DdNode **nodeArray, int n)
 Counts the number of nodes in an array of DDs.
double Cudd_CountMinterm (DdManager *manager, DdNode *node, int nvars)
 Counts the minterms of an ADD or BDD.
double Cudd_CountPath (DdNode *node)
 Counts the paths of a DD.
int Cudd_EpdCountMinterm (DdManager const *manager, DdNode *node, int nvars, EpDouble *epd)
 Counts the minterms of an ADD or BDD with extended range.
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.
int Cudd_EpdPrintMinterm (DdManager const *dd, DdNode *node, int nvars)
 Prints the number of minterms of an ADD or BDD with extended range.
double Cudd_CountPathsToNonZero (DdNode *node)
 Counts the paths to a non-zero terminal of a DD.
int Cudd_SupportIndices (DdManager *dd, DdNode *f, int **indices)
 Finds the variables on which a DD depends.
DdNodeCudd_Support (DdManager *dd, DdNode *f)
 Finds the variables on which a DD depends.
int * Cudd_SupportIndex (DdManager *dd, DdNode *f)
 Finds the variables on which a DD depends.
int Cudd_SupportSize (DdManager *dd, DdNode *f)
 Counts the variables on which a DD depends.
int Cudd_VectorSupportIndices (DdManager *dd, DdNode **F, int n, int **indices)
 Finds the variables on which a set of DDs depends.
DdNodeCudd_VectorSupport (DdManager *dd, DdNode **F, int n)
 Finds the variables on which a set of DDs depends.
int * Cudd_VectorSupportIndex (DdManager *dd, DdNode **F, int n)
 Finds the variables on which a set of DDs depends.
int Cudd_VectorSupportSize (DdManager *dd, DdNode **F, int n)
 Counts the variables on which a set of DDs depends.
int Cudd_ClassifySupport (DdManager *dd, DdNode *f, DdNode *g, DdNode **common, DdNode **onlyF, DdNode **onlyG)
 Classifies the variables in the support of two DDs.
int Cudd_CountLeaves (DdNode *node)
 Counts the number of leaves in a DD.
int Cudd_bddPickOneCube (DdManager *ddm, DdNode *node, char *string)
 Picks one on-set cube randomly from the given DD.
DdNodeCudd_bddPickOneMinterm (DdManager *dd, DdNode *f, DdNode **vars, int n)
 Picks one on-set minterm randomly from the given DD.
DdNode ** Cudd_bddPickArbitraryMinterms (DdManager *dd, DdNode *f, DdNode **vars, int n, int k)
 Picks k on-set minterms evenly distributed from given DD.
DdNodeCudd_SubsetWithMaskVars (DdManager *dd, DdNode *f, DdNode **vars, int nvars, DdNode **maskVars, int mvars)
 Extracts a subset from a BDD.
DdGenCudd_FirstCube (DdManager *dd, DdNode *f, int **cube, CUDD_VALUE_TYPE *value)
 Finds the first cube of a decision diagram.
int Cudd_NextCube (DdGen *gen, int **cube, CUDD_VALUE_TYPE *value)
 Generates the next cube of a decision diagram onset.
DdGenCudd_FirstPrime (DdManager *dd, DdNode *l, DdNode *u, int **cube)
 Finds the first prime of a Boolean function.
int Cudd_NextPrime (DdGen *gen, int **cube)
 Generates the next prime of a Boolean function.
DdNodeCudd_bddComputeCube (DdManager *dd, DdNode **vars, int *phase, int n)
 Computes the cube of an array of BDD variables.
DdNodeCudd_addComputeCube (DdManager *dd, DdNode **vars, int *phase, int n)
 Computes the cube of an array of ADD variables.
DdNodeCudd_CubeArrayToBdd (DdManager *dd, int *array)
 Builds the BDD of a cube from a positional array.
int Cudd_BddToCubeArray (DdManager *dd, DdNode *cube, int *array)
 Builds a positional array from the BDD of a cube.
DdGenCudd_FirstNode (DdManager *dd, DdNode *f, DdNode **node)
 Finds the first node of a decision diagram.
int Cudd_NextNode (DdGen *gen, DdNode **node)
 Finds the next node of a decision diagram.
int Cudd_GenFree (DdGen *gen)
 Frees a CUDD generator.
int Cudd_IsGenEmpty (DdGen *gen)
 Queries the status of a generator.
DdNodeCudd_IndicesToCube (DdManager *dd, int *array, int n)
 Builds a cube of BDD variables from an array of indices.
void Cudd_PrintVersion (FILE *fp)
 Prints the package version number.
double Cudd_AverageDistance (DdManager *dd)
 Computes the average distance between adjacent nodes in the manager.
int32_t Cudd_Random (DdManager *dd)
 Portable random number generator.
void Cudd_Srandom (DdManager *dd, int32_t seed)
 Initializer for the portable random number generator.
double Cudd_Density (DdManager *dd, DdNode *f, int nvars)
 Computes the density of a BDD or ADD.
void Cudd_OutOfMem (size_t size)
 Warns that a memory allocation failed.
void Cudd_OutOfMemSilent (size_t size)
 Doesn not warn that a memory allocation failed.
int cuddP (DdManager *dd, DdNode *f)
 Prints a DD to the standard output. One line per node is printed.
enum st_retval cuddStCountfree (void *key, void *value, void *arg)
 Frees the memory used to store the minterm counts recorded in the visited table.
int cuddCollectNodes (DdNode *f, st_table *visited)
 Recursively collects all the nodes of a DD in a symbol table.
DdNodePtrcuddNodeArray (DdNode *f, int *n)
 Recursively collects all the nodes of a DD in an array.
static int dp2 (DdManager *dd, DdNode *f, st_table *t)
 Performs the recursive step of cuddP.
static void ddPrintMintermAux (DdManager *dd, DdNode *node, int *list)
 Performs the recursive step of Cudd_PrintMinterm.
static int ddDagInt (DdNode *n)
 Performs the recursive step of Cudd_DagSize.
static int cuddNodeArrayRecur (DdNode *f, DdNodePtr *table, int index)
 Performs the recursive step of cuddNodeArray.
static int cuddEstimateCofactor (DdManager *dd, st_table *table, DdNode *node, int i, int phase, DdNode **ptr)
 Performs the recursive step of Cudd_CofactorEstimate.
static DdNodecuddUniqueLookup (DdManager *unique, int index, DdNode *T, DdNode *E)
 Checks the unique table for the existence of an internal node.
static int cuddEstimateCofactorSimple (DdNode *node, int i)
 Performs the recursive step of Cudd_CofactorEstimateSimple.
static double ddCountMintermAux (DdManager *dd, DdNode *node, double max, DdHashTable *table)
 Performs the recursive step of Cudd_CountMinterm.
static double ddCountPathAux (DdNode *node, st_table *table)
 Performs the recursive step of Cudd_CountPath.
static int ddEpdCountMintermAux (DdManager const *dd, DdNode *node, EpDouble *max, EpDouble *epd, st_table *table)
 Performs the recursive step of Cudd_EpdCountMinterm.
static long double ddLdblCountMintermAux (DdManager const *manager, DdNode *node, long double max, st_table *table)
 Performs the recursive step of Cudd_LdblCountMinterm.
static double ddCountPathsToNonZero (DdNode *N, st_table *table)
 Performs the recursive step of Cudd_CountPathsToNonZero.
static void ddSupportStep (DdNode *f, int *support)
 Performs the recursive step of Cudd_Support.
static void ddClearFlag (DdNode *f)
 Performs a DFS from f, clearing the LSB of the next pointers.
static int ddLeavesInt (DdNode *n)
 Performs the recursive step of Cudd_CountLeaves.
static int ddPickArbitraryMinterms (DdManager *dd, DdNode *node, int nvars, int nminterms, char **string)
 Performs the recursive step of Cudd_bddPickArbitraryMinterms.
static int ddPickRepresentativeCube (DdManager *dd, DdNode *node, double *weight, char *string)
 Finds a representative cube of a BDD.
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.
static void ddFindSupport (DdManager *dd, DdNode *f, int *SP)
 Recursively find the support of f.
static void ddClearVars (DdManager *dd, int SP)
 Clears visited flags for variables.
static int indexCompare (const void *a, const void *b)
 Compares indices for qsort.
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.
static long double powl (long double base, long double exponent)
 Replacement for standard library powl.

Detailed Description

Utility functions.

Author:
Fabio Somenzi

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

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.


Function Documentation

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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
void Cudd_PrintVersion ( FILE *  fp  ) 

Prints the package version number.

Side effects
None
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
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
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
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. 1. 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) 2. 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. 3. 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. 4. 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
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
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
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
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
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
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
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
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
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
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
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
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
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.
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
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
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
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
static void ddClearVars ( DdManager dd,
int  SP 
) [static]

Clears visited flags for variables.

Side effects
None
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
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
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
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
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
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
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.
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
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
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
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
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
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
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
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
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
static long double powl ( long double  base,
long double  exponent 
) [static]

Replacement for standard library powl.

Some systems' C libraries, notably Cygwin as of 2015, lack an implementation of powl. This simple-minded replacement works for integral powers. It is based on iterative squaring.

Returns:
base raised to the exponent.
 All Data Structures Files Functions Variables Typedefs Enumerations Defines

Generated on 31 Dec 2015 for cudd by  doxygen 1.6.1