Utility functions. More...
#include <stddef.h>
#include <float.h>
#include "util.h"
#include "epdInt.h"
#include "cuddInt.h"
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. | |
DdNode * | Cudd_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. | |
DdNode * | Cudd_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. | |
DdNode * | Cudd_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. | |
DdNode * | Cudd_SubsetWithMaskVars (DdManager *dd, DdNode *f, DdNode **vars, int nvars, DdNode **maskVars, int mvars) |
Extracts a subset from a BDD. | |
DdGen * | Cudd_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. | |
DdGen * | Cudd_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. | |
DdNode * | Cudd_bddComputeCube (DdManager *dd, DdNode **vars, int *phase, int n) |
Computes the cube of an array of BDD variables. | |
DdNode * | Cudd_addComputeCube (DdManager *dd, DdNode **vars, int *phase, int n) |
Computes the cube of an array of ADD variables. | |
DdNode * | Cudd_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. | |
DdGen * | Cudd_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. | |
DdNode * | Cudd_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. | |
DdNodePtr * | cuddNodeArray (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 DdNode * | cuddUniqueLookup (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. |
Utility functions.
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.
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.
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.
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.
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
.
f
may be the constant 0; f
. dd | manager | |
f | function from which to pick k minterms | |
vars | array of variables | |
n | size of vars | |
k | number of minterms to find |
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.
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
.
f
may be the constant 0; f
. dd | manager | |
f | function from which to pick one minterm | |
vars | array of variables | |
n | size of vars |
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.
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.
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
.
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.
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().
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.
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.
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.
int Cudd_DagSize | ( | DdNode * | node | ) |
Counts the number of nodes in a DD.
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.
dd | manager | |
f | function whose density is sought | |
nvars | size of the support of f |
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.
Prints the number of minterms of an ADD or BDD with extended range.
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.
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.
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.
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.
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.
int Cudd_GenFree | ( | DdGen * | gen | ) |
Frees a CUDD generator.
Builds a cube of BDD variables from an array of indices.
int Cudd_IsGenEmpty | ( | DdGen * | gen | ) |
Queries the status of a generator.
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.
int Cudd_NextCube | ( | DdGen * | gen, | |
int ** | cube, | |||
CUDD_VALUE_TYPE * | value | |||
) |
Generates the next cube of a decision diagram onset.
Finds the next node of a decision diagram.
int Cudd_NextPrime | ( | DdGen * | gen, | |
int ** | cube | |||
) |
Generates the next prime of a Boolean function.
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.
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.
size | size of the allocation that failed |
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:
For the purpose of counting the number of minterms, the function is supposed to depend on n variables.
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.
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.
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.
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.
int Cudd_SharingSize | ( | DdNode ** | nodeArray, | |
int | n | |||
) |
Counts the number of nodes in an array of DDs.
Shared nodes are counted only once.
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.
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.
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 |
Finds the variables on which a DD depends.
dd | manager | |
f | DD whose support is sought |
Finds the variables on which a DD depends.
dd | manager | |
f | DD whose support is sought |
Finds the variables on which a DD depends.
dd | manager | |
f | DD whose support is sought | |
indices | array containing (on return) the indices |
Counts the variables on which a DD depends.
dd | manager | |
f | DD whose support size is sought |
Finds the variables on which a set of DDs depends.
The set must contain either BDDs and ADDs, or ZDDs.
dd | manager | |
F | array of DDs whose support is sought | |
n | size of the array |
Finds the variables on which a set of DDs depends.
The set must contain either BDDs and ADDs, or ZDDs.
dd | manager | |
F | array of DDs whose support is sought | |
n | size of the array |
Finds the variables on which a set of DDs depends.
The set must contain either BDDs and ADDs, or ZDDs.
dd | manager | |
F | DD whose support is sought | |
n | size of the array | |
indices | array containing (on return) the indices |
Counts the variables on which a set of DDs depends.
The set must contain either BDDs and ADDs, or ZDDs.
dd | manager | |
F | array of DDs whose support is sought | |
n | size of the array |
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.
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.
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.
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.
Performs the recursive step of cuddNodeArray.
node is supposed to be regular; the invariant is maintained by this procedure.
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.
Checks the unique table for the existence of an internal node.
static void ddClearFlag | ( | DdNode * | f | ) | [static] |
Performs a DFS from f, clearing the LSB of the next pointers.
static void ddClearVars | ( | DdManager * | dd, | |
int | SP | |||
) | [static] |
Clears visited flags for variables.
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.
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.
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.
static int ddDagInt | ( | DdNode * | n | ) | [static] |
Performs the recursive step of Cudd_DagSize.
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.
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.
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.
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.
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.
static int ddLeavesInt | ( | DdNode * | n | ) | [static] |
Performs the recursive step of Cudd_CountLeaves.
static int ddPickArbitraryMinterms | ( | DdManager * | dd, | |
DdNode * | node, | |||
int | nvars, | |||
int | nminterms, | |||
char ** | string | |||
) | [static] |
Performs the recursive step of 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.
Performs the recursive step of Cudd_PrintMinterm.
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.
Performs the recursive step of cuddP.
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.
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.