|
SVF
|
Go to the source code of this file.
Classes | |
| struct | DdGen |
| struct | DdHook |
| struct | DdLocalCacheItem |
| struct | DdLocalCache |
| struct | DdHashItem |
| struct | DdHashTable |
| struct | DdCache |
| struct | DdSubtable |
| struct | DdManager |
| struct | Move |
| struct | DdQueueItem |
| struct | DdLevelQueue |
Macros | |
| #define | DD_INLINE |
| #define | DD_UNUSED |
| #define | DD_MAXREF ((DdHalfWord) ~0) |
| #define | DD_DEFAULT_RESIZE 10 /* how many extra variables */ |
| #define | DD_MEM_CHUNK 1022 |
| #define | DD_ONE_VAL (1.0) |
| #define | DD_ZERO_VAL (0.0) |
| #define | DD_EPSILON (1.0e-12) |
| #define | DD_PLUS_INF_VAL (10e301) |
| #define | DD_CRI_HI_MARK (10e150) |
| #define | DD_CRI_LO_MARK (-(DD_CRI_HI_MARK)) |
| #define | DD_MINUS_INF_VAL (-(DD_PLUS_INF_VAL)) |
| #define | DD_NON_CONSTANT ((DdNode *) 1) /* for Cudd_bddIteConstant */ |
| #define | DD_MAX_SUBTABLE_DENSITY 4 /* tells when to resize a subtable */ |
| #define | DD_GC_FRAC_LO DD_MAX_SUBTABLE_DENSITY * 0.25 |
| #define | DD_GC_FRAC_HI DD_MAX_SUBTABLE_DENSITY * 1.0 |
| #define | DD_GC_FRAC_MIN 0.2 |
| #define | DD_MIN_HIT |
| #define | DD_MAX_LOOSE_FRACTION |
| #define | DD_MAX_CACHE_FRACTION |
| #define | DD_STASH_FRACTION |
| #define | DD_MAX_CACHE_TO_SLOTS_RATIO 4 /* used to limit the cache size */ |
| #define | DD_SIFT_MAX_VAR 1000 |
| #define | DD_SIFT_MAX_SWAPS 2000000 |
| #define | DD_DEFAULT_RECOMB 0 |
| #define | DD_MAX_REORDER_GROWTH 1.2 |
| #define | DD_FIRST_REORDER 4004 /* 4 for the constants */ |
| #define | DD_DYN_RATIO 2 /* when to dynamically reorder */ |
| #define | DD_P1 12582917 |
| #define | DD_P2 4256249 |
| #define | DD_P3 741457 |
| #define | DD_P4 1618033999 |
| #define | DD_ADD_ITE_TAG 0x02 |
| #define | DD_BDD_AND_ABSTRACT_TAG 0x06 |
| #define | DD_BDD_XOR_EXIST_ABSTRACT_TAG 0x0a |
| #define | DD_BDD_ITE_TAG 0x0e |
| #define | DD_ADD_BDD_DO_INTERVAL_TAG 0x22 |
| #define | DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG 0x26 |
| #define | DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG 0x2a |
| #define | DD_BDD_COMPOSE_RECUR_TAG 0x2e |
| #define | DD_ADD_COMPOSE_RECUR_TAG 0x42 |
| #define | DD_ADD_NON_SIM_COMPOSE_TAG 0x46 |
| #define | DD_EQUIV_DC_TAG 0x4a |
| #define | DD_ZDD_ITE_TAG 0x4e |
| #define | DD_ADD_ITE_CONSTANT_TAG 0x62 |
| #define | DD_ADD_EVAL_CONST_TAG 0x66 |
| #define | DD_BDD_ITE_CONSTANT_TAG 0x6a |
| #define | DD_ADD_OUT_SUM_TAG 0x6e |
| #define | DD_BDD_LEQ_UNLESS_TAG 0x82 |
| #define | DD_ADD_TRIANGLE_TAG 0x86 |
| #define | DD_BDD_MAX_EXP_TAG 0x8a |
| #define | CUDD_GEN_CUBES 0 |
| #define | CUDD_GEN_PRIMES 1 |
| #define | CUDD_GEN_NODES 2 |
| #define | CUDD_GEN_ZDD_PATHS 3 |
| #define | CUDD_GEN_EMPTY 0 |
| #define | CUDD_GEN_NONEMPTY 1 |
| #define | cuddDeallocNode(unique, node) |
| #define | cuddDeallocMove(unique, node) |
| #define | cuddRef(n) cuddSatInc(Cudd_Regular(n)->ref) |
| #define | cuddDeref(n) cuddSatDec(Cudd_Regular(n)->ref) |
| #define | cuddIsConstant(node) ((node)->index == CUDD_CONST_INDEX) |
| #define | cuddT(node) ((node)->type.kids.T) |
| #define | cuddE(node) ((node)->type.kids.E) |
| #define | cuddV(node) ((node)->type.value) |
| #define | cuddI(dd, index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->perm[(index)]) |
| #define | cuddIZ(dd, index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->permZ[(index)]) |
| #define | ddHash(f, g, s) ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s)) |
| #define | ddCHash(o, f, g, h, s) |
| #define | ddCHash2(o, f, g, s) (((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s)) |
| #define | cuddClean(p) ((DdNode *)((ptruint)(p) & ~0xf)) |
| #define | ddMin(x, y) (((y) < (x)) ? (y) : (x)) |
| #define | ddMax(x, y) (((y) > (x)) ? (y) : (x)) |
| #define | ddAbs(x) (((x)<0) ? -(x) : (x)) |
| #define | ddEqualVal(x, y, e) (ddAbs((x)-(y))<(e)) |
| #define | cuddSatInc(x) ((x) += (x) != (DdHalfWord)DD_MAXREF) |
| #define | cuddSatDec(x) ((x) -= (x) != (DdHalfWord)DD_MAXREF) |
| #define | DD_ONE(dd) ((dd)->one) |
| #define | DD_ZERO(dd) ((dd)->zero) |
| #define | DD_PLUS_INFINITY(dd) ((dd)->plusinfinity) |
| #define | DD_MINUS_INFINITY(dd) ((dd)->minusinfinity) |
| #define | cuddAdjust(x) ((x) = ((x) >= DD_CRI_HI_MARK) ? DD_PLUS_INF_VAL : (((x) <= DD_CRI_LO_MARK) ? DD_MINUS_INF_VAL : (x))) |
| #define | DD_LSDIGIT(x) ((x) & DD_APA_MASK) |
| #define | DD_MSDIGIT(x) ((x) >> DD_APA_BITS) |
| #define | statLine(dd) |
Typedefs | |
| typedef struct DdHook | DdHook |
| typedef int | ptrint |
| typedef unsigned int | ptruint |
| typedef DdNode * | DdNodePtr |
| typedef struct DdLocalCacheItem | DdLocalCacheItem |
| typedef struct DdLocalCache | DdLocalCache |
| typedef struct DdHashItem | DdHashItem |
| typedef struct DdHashTable | DdHashTable |
| typedef struct DdCache | DdCache |
| typedef struct DdSubtable | DdSubtable |
| typedef struct Move | Move |
| typedef struct DdQueueItem | DdQueueItem |
| typedef struct DdLevelQueue | DdLevelQueue |
| #define cuddAdjust | ( | x | ) | ((x) = ((x) >= DD_CRI_HI_MARK) ? DD_PLUS_INF_VAL : (((x) <= DD_CRI_LO_MARK) ? DD_MINUS_INF_VAL : (x))) |
Macro***********************************************************************
Synopsis [Enforces DD_MINUS_INF_VAL <= x <= DD_PLUS_INF_VAL.]
Description [Enforces DD_MINUS_INF_VAL <= x <= DD_PLUS_INF_VAL. Furthermore, if x <= DD_MINUS_INF_VAL/2, x is set to DD_MINUS_INF_VAL. Similarly, if DD_PLUS_INF_VAL/2 <= x, x is set to DD_PLUS_INF_VAL. Normally this macro is a NOOP. However, if HAVE_IEEE_754 is not defined, it makes sure that a value does not get larger than infinity in absolute value, and once it gets to infinity, stays there. If the value overflows before this macro is applied, no recovery is possible.]
SideEffects [none]
SeeAlso []
| #define cuddDeallocMove | ( | unique, | |
| node | |||
| ) |
Macro***********************************************************************
Synopsis [Adds node to the head of the free list.]
Description [Adds node to the head of the free list. Does not deallocate memory chunks that become free. This function is also used by the dynamic reordering functions.]
SideEffects [None]
SeeAlso [cuddDeallocNode cuddDynamicAllocNode]
| #define cuddDeallocNode | ( | unique, | |
| node | |||
| ) |
Macro***********************************************************************
Synopsis [Adds node to the head of the free list.]
Description [Adds node to the head of the free list. Does not deallocate memory chunks that become free. This function is also used by the dynamic reordering functions.]
SideEffects [None]
SeeAlso [cuddAllocNode cuddDynamicAllocNode cuddDeallocMove]
| #define cuddDeref | ( | n | ) | cuddSatDec(Cudd_Regular(n)->ref) |
Macro***********************************************************************
Synopsis [Decreases the reference count of a node, if it is not saturated.]
Description [Decreases the reference count of node. It is primarily used in recursive procedures to decrease the ref count of a result node before returning it. This accomplishes the goal of removing the protection applied by a previous cuddRef. This being a macro, it is faster than Cudd_Deref, but it cannot be used in constructs like cuddDeref(a = b()).]
SideEffects [none]
SeeAlso [Cudd_Deref]
| #define cuddE | ( | node | ) | ((node)->type.kids.E) |
Macro***********************************************************************
Synopsis [Returns the else child of an internal node.]
Description [Returns the else child of an internal node. If node is a constant node, the result is unpredictable. The pointer passed to cuddE must be regular.]
SideEffects [none]
SeeAlso [Cudd_E]
| #define cuddI | ( | dd, | |
| index | |||
| ) | (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->perm[(index)]) |
Macro***********************************************************************
Synopsis [Finds the current position of variable index in the order.]
Description [Finds the current position of variable index in the order. This macro duplicates the functionality of Cudd_ReadPerm, but it does not check for out-of-bounds indices and it is more efficient.]
SideEffects [none]
SeeAlso [Cudd_ReadPerm]
| #define cuddIsConstant | ( | node | ) | ((node)->index == CUDD_CONST_INDEX) |
Macro***********************************************************************
Synopsis [Returns 1 if the node is a constant node.]
Description [Returns 1 if the node is a constant node (rather than an internal node). All constant nodes have the same index (CUDD_CONST_INDEX). The pointer passed to cuddIsConstant must be regular.]
SideEffects [none]
SeeAlso [Cudd_IsConstant]
| #define cuddIZ | ( | dd, | |
| index | |||
| ) | (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->permZ[(index)]) |
Macro***********************************************************************
Synopsis [Finds the current position of ZDD variable index in the order.]
Description [Finds the current position of ZDD variable index in the order. This macro duplicates the functionality of Cudd_ReadPermZdd, but it does not check for out-of-bounds indices and it is more efficient.]
SideEffects [none]
SeeAlso [Cudd_ReadPermZdd]
| #define cuddRef | ( | n | ) | cuddSatInc(Cudd_Regular(n)->ref) |
Macro***********************************************************************
Synopsis [Increases the reference count of a node, if it is not saturated.]
Description [Increases the reference count of a node, if it is not saturated. This being a macro, it is faster than Cudd_Ref, but it cannot be used in constructs like cuddRef(a = b()).]
SideEffects [none]
SeeAlso [Cudd_Ref]
| #define cuddSatDec | ( | x | ) | ((x) -= (x) != (DdHalfWord)DD_MAXREF) |
| #define cuddSatInc | ( | x | ) | ((x) += (x) != (DdHalfWord)DD_MAXREF) |
| #define cuddT | ( | node | ) | ((node)->type.kids.T) |
Macro***********************************************************************
Synopsis [Returns the then child of an internal node.]
Description [Returns the then child of an internal node. If node is a constant node, the result is unpredictable. The pointer passed to cuddT must be regular.]
SideEffects [none]
SeeAlso [Cudd_T]
| #define cuddV | ( | node | ) | ((node)->type.value) |
Macro***********************************************************************
Synopsis [Returns the value of a constant node.]
Description [Returns the value of a constant node. If node is an internal node, the result is unpredictable. The pointer passed to cuddV must be regular.]
SideEffects [none]
SeeAlso [Cudd_V]
| #define DD_CRI_LO_MARK (-(DD_CRI_HI_MARK)) |
| #define DD_DEFAULT_RESIZE 10 /* how many extra variables */ |
| #define DD_GC_FRAC_HI DD_MAX_SUBTABLE_DENSITY * 1.0 |
| #define DD_GC_FRAC_LO DD_MAX_SUBTABLE_DENSITY * 0.25 |
| #define DD_INLINE |
CHeaderFile*****************************************************************
FileName [cuddInt.h]
PackageName [cudd]
Synopsis [Internal data structures of the CUDD package.]
Description []
SeeAlso []
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, 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.]
Revision [
]
| #define DD_LSDIGIT | ( | x | ) | ((x) & DD_APA_MASK) |
Macro***********************************************************************
Synopsis [Extract the least significant digit of a double digit.]
Description [Extract the least significant digit of a double digit. Used in the manipulation of arbitrary precision integers.]
SideEffects [None]
SeeAlso [DD_MSDIGIT]
| #define DD_MAX_CACHE_FRACTION |
| #define DD_MAX_CACHE_TO_SLOTS_RATIO 4 /* used to limit the cache size */ |
| #define DD_MAX_LOOSE_FRACTION |
| #define DD_MAX_SUBTABLE_DENSITY 4 /* tells when to resize a subtable */ |
| #define DD_MAXREF ((DdHalfWord) ~0) |
| #define DD_MIN_HIT |
| #define DD_MINUS_INF_VAL (-(DD_PLUS_INF_VAL)) |
| #define DD_MINUS_INFINITY | ( | dd | ) | ((dd)->minusinfinity) |
| #define DD_MSDIGIT | ( | x | ) | ((x) >> DD_APA_BITS) |
Macro***********************************************************************
Synopsis [Extract the most significant digit of a double digit.]
Description [Extract the most significant digit of a double digit. Used in the manipulation of arbitrary precision integers.]
SideEffects [None]
SeeAlso [DD_LSDIGIT]
| #define DD_NON_CONSTANT ((DdNode *) 1) /* for Cudd_bddIteConstant */ |
| #define DD_ONE | ( | dd | ) | ((dd)->one) |
| #define DD_PLUS_INFINITY | ( | dd | ) | ((dd)->plusinfinity) |
| #define DD_STASH_FRACTION |
| #define DD_ZERO | ( | dd | ) | ((dd)->zero) |
Macro***********************************************************************
Synopsis [Returns the arithmetic 0 constant node.]
Description [Returns the arithmetic 0 constant node. This is different from the logical zero. The latter is obtained by Cudd_Not(DD_ONE(dd)).]
SideEffects [none]
SeeAlso [DD_ONE Cudd_Not DD_PLUS_INFINITY DD_MINUS_INFINITY]
| #define ddAbs | ( | x | ) | (((x)<0) ? -(x) : (x)) |
| #define ddCHash | ( | o, | |
| f, | |||
| g, | |||
| h, | |||
| s | |||
| ) |
Macro***********************************************************************
Synopsis [Hash function for the cache.]
Description []
SideEffects [none]
SeeAlso [ddHash ddCHash2]
| #define ddEqualVal | ( | x, | |
| y, | |||
| e | |||
| ) | (ddAbs((x)-(y))<(e)) |
| #define ddMax | ( | x, | |
| y | |||
| ) | (((y) > (x)) ? (y) : (x)) |
| #define ddMin | ( | x, | |
| y | |||
| ) | (((y) < (x)) ? (y) : (x)) |
| #define statLine | ( | dd | ) |
Macro***********************************************************************
Synopsis [Outputs a line of stats.]
Description [Outputs a line of stats if DD_COUNT and DD_STATS are defined. Increments the number of recursive calls if DD_COUNT is defined.]
SideEffects [None]
SeeAlso []
| typedef struct DdHashItem DdHashItem |
| typedef struct DdHashTable DdHashTable |
| typedef struct DdLevelQueue DdLevelQueue |
| typedef struct DdLocalCache DdLocalCache |
| typedef struct DdLocalCacheItem DdLocalCacheItem |
| typedef struct DdQueueItem DdQueueItem |
| typedef struct DdSubtable DdSubtable |
| DdNode* cuddAddApplyRecur | ( | DdManager * | dd, |
| DdNode * | *)(DdManager *, DdNode **, DdNode **, | ||
| DdNode * | f, | ||
| DdNode * | g | ||
| ) |
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_addCmpl.]
Description [Performs the recursive step of Cudd_addCmpl. Returns a pointer to the resulting ADD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addCmpl]
Definition at line 558 of file cuddAddIte.c.
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_addIte(f,g,h).]
Description [Implements the recursive step of Cudd_addIte(f,g,h). Returns a pointer to the resulting ADD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addIte]
Definition at line 441 of file cuddAddIte.c.
| DdNode* cuddAddMonadicApplyRecur | ( | DdManager * | dd, |
| DdNode *(*)(DdManager *, DdNode *) | op, | ||
| DdNode * | f | ||
| ) |
Function********************************************************************
Synopsis [Fast storage allocation for DdNodes in the table.]
Description [Fast storage allocation for DdNodes in the table. The first 4 bytes of a chunk contain a pointer to the next block; the rest contains DD_MEM_CHUNK spaces for DdNodes. Returns a pointer to a new node if successful; NULL is memory is full.]
SideEffects [None]
SeeAlso [cuddDynamicAllocNode]
Definition at line 266 of file cuddTable.c.
| int cuddAnnealing | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Get new variable-order by simulated annealing algorithm.]
Description [Get x, y by random selection. Choose either exchange or jump randomly. In case of jump, choose between jump_up and jump_down randomly. Do exchange or jump and get optimal case. Loop until there is no improvement or temperature reaches minimum. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 154 of file cuddAnneal.c.
| int cuddBddAlignToZdd | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Reorders BDD variables according to the order of the ZDD variables.]
Description [Reorders BDD variables according to the order of the ZDD variables. This function can be called at the end of ZDD reordering to insure that the order of the BDD variables is consistent with the order of the ZDD variables. The number of ZDD variables must be a multiple of the number of BDD variables. Let M be the ratio of the two numbers. cuddBddAlignToZdd then considers the ZDD variables from M*i to (M+1)*i-1 as corresponding to BDD variable i. This function should be normally called from Cudd_zddReduceHeap, which clears the cache. Returns 1 in case of success; 0 otherwise.]
SideEffects [Changes the BDD variable order for all diagrams and performs garbage collection of the BDD unique table.]
SeeAlso [Cudd_ShuffleHeap Cudd_zddReduceHeap]
Definition at line 1250 of file cuddReorder.c.
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_bddAnd.]
Description [Implements the recursive step of Cudd_bddAnd by taking the conjunction of two BDDs. Returns a pointer to the result is successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddAnd]
Definition at line 995 of file cuddBddIte.c.
Function********************************************************************
Synopsis [Performs the recursive steps of Cudd_bddBoleanDiff.]
Description [Performs the recursive steps of Cudd_bddBoleanDiff. Returns the BDD obtained by XORing the cofactors of f with respect to var if successful; NULL otherwise. Exploits the fact that dF/dx = dF'/dx.]
SideEffects [None]
SeeAlso []
Definition at line 675 of file cuddBddAbs.c.
| DdNode* cuddBddClippingAndAbstract | ( | DdManager * | dd, |
| DdNode * | f, | ||
| DdNode * | g, | ||
| DdNode * | cube, | ||
| int | maxDepth, | ||
| int | direction | ||
| ) |
| DdNode* cuddBddClosestCube | ( | DdManager * | dd, |
| DdNode * | f, | ||
| DdNode * | g, | ||
| CUDD_VALUE_TYPE | bound | ||
| ) |
Function********************************************************************
Synopsis [Performs the recursive steps of Cudd_bddExistAbstract.]
Description [Performs the recursive steps of Cudd_bddExistAbstract. Returns the BDD obtained by abstracting the variables of cube from f if successful; NULL otherwise. It is also used by Cudd_bddUnivAbstract.]
SideEffects [None]
SeeAlso [Cudd_bddExistAbstract Cudd_bddUnivAbstract]
Definition at line 393 of file cuddBddAbs.c.
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_bddIntersect.]
Description []
SideEffects [None]
SeeAlso [Cudd_bddIntersect]
Definition at line 880 of file cuddBddIte.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_bddIsop.]
Description []
SideEffects [None]
SeeAlso [Cudd_bddIsop]
Definition at line 572 of file cuddZddIsop.c.
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_bddIte.]
Description [Implements the recursive step of Cudd_bddIte. Returns a pointer to the resulting BDD. NULL if the intermediate result blows up or if reordering occurs.]
SideEffects [None]
SeeAlso []
Definition at line 742 of file cuddBddIte.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_bddMakePrime.]
Description [Performs the recursive step of Cudd_bddMakePrime. Returns the prime if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 995 of file cuddSat.c.
Function********************************************************************
Synopsis [Takes the exclusive OR of two BDDs and simultaneously abstracts the variables in cube.]
Description [Takes the exclusive OR of two BDDs and simultaneously abstracts the variables in cube. The variables are existentially abstracted. Returns a pointer to the result is successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddAndAbstract]
Definition at line 503 of file cuddBddAbs.c.
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_bddXor.]
Description [Implements the recursive step of Cudd_bddXor by taking the exclusive OR of two BDDs. Returns a pointer to the result is successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddXor]
Definition at line 1123 of file cuddBddIte.c.
| DdNode* cuddBiasedUnderApprox | ( | DdManager * | dd, |
| DdNode * | f, | ||
| DdNode * | b, | ||
| int | numVars, | ||
| int | threshold, | ||
| double | quality1, | ||
| double | quality0 | ||
| ) |
| void cuddCacheFlush | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Flushes the cache.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 1004 of file cuddCache.c.
| void cuddCacheInsert | ( | DdManager * | table, |
| ptruint | op, | ||
| DdNode * | f, | ||
| DdNode * | g, | ||
| DdNode * | h, | ||
| DdNode * | data | ||
| ) |
Function********************************************************************
Synopsis [Inserts a result in the cache for a function with three operands.]
Description [Inserts a result in the cache for a function with three operands. The operator tag (see CUDD/cuddInt.h for details) is split and stored into unused bits of the first two pointers.]
SideEffects [None]
SeeAlso [cuddCacheInsert2 cuddCacheInsert1]
Definition at line 217 of file cuddCache.c.
| void cuddCacheInsert1 | ( | DdManager * | table, |
| DdNode * | *)(DdManager *, DdNode *, | ||
| DdNode * | f, | ||
| DdNode * | data | ||
| ) |
| void cuddCacheInsert2 | ( | DdManager * | table, |
| DdNode * | *)(DdManager *, DdNode *, DdNode *, | ||
| DdNode * | f, | ||
| DdNode * | g, | ||
| DdNode * | data | ||
| ) |
Function********************************************************************
Synopsis [Looks up in the cache for the result of op applied to f, g, and h.]
Description [Returns the result if found; it returns NULL if no result is found.]
SideEffects [None]
SeeAlso [cuddCacheLookup2 cuddCacheLookup1]
Definition at line 347 of file cuddCache.c.
| DdNode* cuddCacheLookup2 | ( | DdManager * | table, |
| DdNode * | *)(DdManager *, DdNode *, DdNode *, | ||
| DdNode * | f, | ||
| DdNode * | g | ||
| ) |
| DdNode* cuddCacheLookup2Zdd | ( | DdManager * | table, |
| DdNode * | *)(DdManager *, DdNode *, DdNode *, | ||
| DdNode * | f, | ||
| DdNode * | g | ||
| ) |
Function********************************************************************
Synopsis [Looks up in the cache for the result of op applied to f, g, and h.]
Description [Returns the result if found; it returns NULL if no result is found.]
SideEffects [None]
SeeAlso [cuddCacheLookup2Zdd cuddCacheLookup1Zdd]
Definition at line 409 of file cuddCache.c.
| int cuddCacheProfile | ( | DdManager * | table, |
| FILE * | fp | ||
| ) |
Function********************************************************************
Synopsis [Computes and prints a profile of the cache usage.]
Description [Computes and prints a profile of the cache usage. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 749 of file cuddCache.c.
| void cuddCacheResize | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Resizes the cache.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 889 of file cuddCache.c.
| void cuddClearDeathRow | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_Cofactor.]
Description [Performs the recursive step of Cudd_Cofactor. Returns a pointer to the cofactor if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_Cofactor]
Definition at line 226 of file cuddCof.c.
Function********************************************************************
Synopsis [Recursively collects all the nodes of a DD in a symbol table.]
Description [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.]
SideEffects [None]
SeeAlso []
Definition at line 2933 of file cuddUtil.c.
| int cuddComputeFloorLog2 | ( | unsigned int | value | ) |
Function********************************************************************
Synopsis [Returns the floor of the logarithm to the base 2.]
Description [Returns the floor of the logarithm to the base 2. The input value is assumed to be greater than 0.]
SideEffects [None]
SeeAlso []
Definition at line 1036 of file cuddCache.c.
Function********************************************************************
Synopsis [Looks up in the cache for the result of op applied to f, g, and h.]
Description [Looks up in the cache for the result of op applied to f, g, and h. Assumes that the calling procedure (e.g., Cudd_bddIteConstant) is only interested in whether the result is constant or not. Returns the result if found (possibly DD_NON_CONSTANT); otherwise it returns NULL.]
SideEffects [None]
SeeAlso [cuddCacheLookup]
Definition at line 690 of file cuddCache.c.
| int cuddDestroySubtables | ( | DdManager * | unique, |
| int | n | ||
| ) |
Function********************************************************************
Synopsis [Destroys the n most recently created subtables in a unique table.]
Description [Destroys the n most recently created subtables in a unique table. n should be positive. The subtables should not contain any live nodes, except the (isolated) projection function. The projection functions are freed. Returns 1 if successful; 0 otherwise.]
SideEffects [The variable map used for fast variable substitution is destroyed if it exists. In this case the cache is also cleared.]
SeeAlso [cuddInsertSubtables Cudd_SetVarMap]
Definition at line 2137 of file cuddTable.c.
Function********************************************************************
Synopsis [Dynamically allocates a Node.]
Description [Dynamically allocates a Node. This procedure is similar to cuddAllocNode in Cudd_Table.c, but it does not attempt garbage collection, because during reordering there are no dead nodes. Returns a pointer to a new node if successful; NULL is memory is full.]
SideEffects [None]
SeeAlso [cuddAllocNode]
Definition at line 405 of file cuddReorder.c.
| int cuddExact | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Exact variable ordering algorithm.]
Description [Exact variable ordering algorithm. Finds an optimum order for the variables between lower and upper. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 149 of file cuddExact.c.
| void cuddFreeTable | ( | DdManager * | unique | ) |
Function********************************************************************
Synopsis [Frees the resources associated to a unique table.]
Description []
SideEffects [None]
SeeAlso [cuddInitTable]
Definition at line 692 of file cuddTable.c.
| int cuddGa | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Genetic algorithm for DD reordering.]
Description [Genetic algorithm for DD reordering. The two children of a crossover will be stored in storedd[popsize] and storedd[popsize+1] — the last two slots in the storedd array. (This will make comparisons and replacement easy.) Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 188 of file cuddGenetic.c.
| int cuddGarbageCollect | ( | DdManager * | unique, |
| int | clearCache | ||
| ) |
Function********************************************************************
Synopsis [Performs garbage collection on the unique tables.]
Description [Performs garbage collection on the BDD and ZDD unique tables. If clearCache is 0, the cache is not cleared. This should only be specified if the cache has been cleared right before calling cuddGarbageCollect. (As in the case of dynamic reordering.) Returns the total number of deleted nodes.]
SideEffects [None]
SeeAlso []
Definition at line 762 of file cuddTable.c.
Function********************************************************************
Synopsis [Computes the children of g.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 196 of file cuddCof.c.
| int cuddHashTableGenericInsert | ( | DdHashTable * | hash, |
| DdNode * | f, | ||
| void * | value | ||
| ) |
Function********************************************************************
Synopsis [Inserts an item in a hash table.]
Description [Inserts an item in a hash table when the key is one pointer and the value is not a DdNode pointer. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddHashTableInsert1 cuddHashTableGenericLookup]
Definition at line 919 of file cuddLCache.c.
| void* cuddHashTableGenericLookup | ( | DdHashTable * | hash, |
| DdNode * | f | ||
| ) |
Function********************************************************************
Synopsis [Looks up a key consisting of one pointer in a hash table.]
Description [Looks up a key consisting of one pointer in a hash table when the value is not a DdNode pointer. Returns the value associated to the key if there is an entry for the given key in the table; NULL otherwise.]
SideEffects [None]
SeeAlso [cuddHashTableLookup1 cuddHashTableGenericInsert]
Definition at line 966 of file cuddLCache.c.
| void cuddHashTableGenericQuit | ( | DdHashTable * | hash | ) |
Function********************************************************************
Synopsis [Shuts down a hash table.]
Description [Shuts down a hash table, when the values are not DdNode pointers.]
SideEffects [None]
SeeAlso [cuddHashTableInit]
Definition at line 652 of file cuddLCache.c.
| DdHashTable* cuddHashTableInit | ( | DdManager * | manager, |
| unsigned int | keySize, | ||
| unsigned int | initSize | ||
| ) |
Function********************************************************************
Synopsis [Initializes a hash table.]
Description [Initializes a hash table. Returns a pointer to the new table if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [cuddHashTableQuit]
Definition at line 557 of file cuddLCache.c.
| int cuddHashTableInsert | ( | DdHashTable * | hash, |
| DdNodePtr * | key, | ||
| DdNode * | value, | ||
| ptrint | count | ||
| ) |
Function********************************************************************
Synopsis [Inserts an item in a hash table.]
Description [Inserts an item in a hash table when the key has more than three pointers. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [[cuddHashTableInsert1 cuddHashTableInsert2 cuddHashTableInsert3 cuddHashTableLookup]
Definition at line 693 of file cuddLCache.c.
| int cuddHashTableInsert1 | ( | DdHashTable * | hash, |
| DdNode * | f, | ||
| DdNode * | value, | ||
| ptrint | count | ||
| ) |
Function********************************************************************
Synopsis [Inserts an item in a hash table.]
Description [Inserts an item in a hash table when the key is one pointer. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddHashTableInsert cuddHashTableInsert2 cuddHashTableInsert3 cuddHashTableLookup1]
Definition at line 812 of file cuddLCache.c.
| int cuddHashTableInsert2 | ( | DdHashTable * | hash, |
| DdNode * | f, | ||
| DdNode * | g, | ||
| DdNode * | value, | ||
| ptrint | count | ||
| ) |
Function********************************************************************
Synopsis [Inserts an item in a hash table.]
Description [Inserts an item in a hash table when the key is composed of two pointers. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddHashTableInsert cuddHashTableInsert1 cuddHashTableInsert3 cuddHashTableLookup2]
Definition at line 1005 of file cuddLCache.c.
| int cuddHashTableInsert3 | ( | DdHashTable * | hash, |
| DdNode * | f, | ||
| DdNode * | g, | ||
| DdNode * | h, | ||
| DdNode * | value, | ||
| ptrint | count | ||
| ) |
Function********************************************************************
Synopsis [Inserts an item in a hash table.]
Description [Inserts an item in a hash table when the key is composed of three pointers. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddHashTableInsert cuddHashTableInsert1 cuddHashTableInsert2 cuddHashTableLookup3]
Definition at line 1115 of file cuddLCache.c.
| DdNode* cuddHashTableLookup | ( | DdHashTable * | hash, |
| DdNodePtr * | key | ||
| ) |
Function********************************************************************
Synopsis [Looks up a key in a hash table.]
Description [Looks up a key consisting of more than three pointers in a hash table. Returns the value associated to the key if there is an entry for the given key in the table; NULL otherwise. If the entry is present, its reference counter is decremented if not saturated. If the counter reaches 0, the value of the entry is dereferenced, and the entry is returned to the free list.]
SideEffects [None]
SeeAlso [cuddHashTableLookup1 cuddHashTableLookup2 cuddHashTableLookup3 cuddHashTableInsert]
Definition at line 748 of file cuddLCache.c.
| DdNode* cuddHashTableLookup1 | ( | DdHashTable * | hash, |
| DdNode * | f | ||
| ) |
Function********************************************************************
Synopsis [Looks up a key consisting of one pointer in a hash table.]
Description [Looks up a key consisting of one pointer in a hash table. Returns the value associated to the key if there is an entry for the given key in the table; NULL otherwise. If the entry is present, its reference counter is decremented if not saturated. If the counter reaches 0, the value of the entry is dereferenced, and the entry is returned to the free list.]
SideEffects [None]
SeeAlso [cuddHashTableLookup cuddHashTableLookup2 cuddHashTableLookup3 cuddHashTableInsert1]
Definition at line 864 of file cuddLCache.c.
| DdNode* cuddHashTableLookup2 | ( | DdHashTable * | hash, |
| DdNode * | f, | ||
| DdNode * | g | ||
| ) |
Function********************************************************************
Synopsis [Looks up a key consisting of two pointers in a hash table.]
Description [Looks up a key consisting of two pointer in a hash table. Returns the value associated to the key if there is an entry for the given key in the table; NULL otherwise. If the entry is present, its reference counter is decremented if not saturated. If the counter reaches 0, the value of the entry is dereferenced, and the entry is returned to the free list.]
SideEffects [None]
SeeAlso [cuddHashTableLookup cuddHashTableLookup1 cuddHashTableLookup3 cuddHashTableInsert2]
Definition at line 1059 of file cuddLCache.c.
| DdNode* cuddHashTableLookup3 | ( | DdHashTable * | hash, |
| DdNode * | f, | ||
| DdNode * | g, | ||
| DdNode * | h | ||
| ) |
Function********************************************************************
Synopsis [Looks up a key consisting of three pointers in a hash table.]
Description [Looks up a key consisting of three pointers in a hash table. Returns the value associated to the key if there is an entry for the given key in the table; NULL otherwise. If the entry is present, its reference counter is decremented if not saturated. If the counter reaches 0, the value of the entry is dereferenced, and the entry is returned to the free list.]
SideEffects [None]
SeeAlso [cuddHashTableLookup cuddHashTableLookup1 cuddHashTableLookup2 cuddHashTableInsert3]
Definition at line 1171 of file cuddLCache.c.
| void cuddHashTableQuit | ( | DdHashTable * | hash | ) |
Function********************************************************************
Synopsis [Shuts down a hash table.]
Description [Shuts down a hash table, dereferencing all the values.]
SideEffects [None]
SeeAlso [cuddHashTableInit]
Definition at line 607 of file cuddLCache.c.
| int cuddHeapProfile | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Prints information about the heap.]
Description [Prints to the manager's stdout the number of live nodes for each level of the DD heap that contains at least one live node. It also prints a summary containing:
If more than one table contains the maximum number of live nodes, only the one of lowest index is reported. Returns 1 in case of success and 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 641 of file cuddCheck.c.
| int cuddInitCache | ( | DdManager * | unique, |
| unsigned int | cacheSize, | ||
| unsigned int | maxCacheSize | ||
| ) |
AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Initializes the computed table.]
Description [Initializes the computed table. It is called by Cudd_Init. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_Init]
Definition at line 132 of file cuddCache.c.
| int cuddInitInteract | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Initializes the interaction matrix.]
Description [Initializes the interaction matrix. The interaction matrix is implemented as a bit vector storing the upper triangle of the symmetric interaction matrix. The bit vector is kept in an array of long integers. The computation is based on a series of depth-first searches, one for each root of the DAG. Two flags are needed: The local visited flag uses the LSB of the then pointer. The global visited flag uses the LSB of the next pointer. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 234 of file cuddInteract.c.
| int cuddInitLinear | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Initializes the linear transform matrix.]
Description [Initializes the linear transform matrix. Returns 1 if successful; 0 otherwise.]
SideEffects [none]
SeeAlso []
Definition at line 755 of file cuddLinear.c.
| DdManager* cuddInitTable | ( | unsigned int | numVars, |
| unsigned int | numVarsZ, | ||
| unsigned int | numSlots, | ||
| unsigned int | looseUpTo | ||
| ) |
Function********************************************************************
Synopsis [Creates and initializes the unique table.]
Description [Creates and initializes the unique table. Returns a pointer to the table if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_Init cuddFreeTable]
Definition at line 380 of file cuddTable.c.
| int cuddInsertSubtables | ( | DdManager * | unique, |
| int | n, | ||
| int | level | ||
| ) |
Function********************************************************************
Synopsis [Inserts n new subtables in a unique table at level.]
Description [Inserts n new subtables in a unique table at level. The number n should be positive, and level should be an existing level. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddDestroySubtables]
Definition at line 1824 of file cuddTable.c.
Function********************************************************************
Synopsis [Checks whether a node is in the death row.]
Description [Checks whether a node is in the death row. Returns the position of the first occurrence if the node is present; -1 otherwise.]
SideEffects [None]
SeeAlso [Cudd_DelayedDerefBdd cuddClearDeathRow]
Definition at line 758 of file cuddRef.c.
| void cuddLevelQueueDequeue | ( | DdLevelQueue * | queue, |
| int | level | ||
| ) |
| void* cuddLevelQueueEnqueue | ( | DdLevelQueue * | queue, |
| void * | key, | ||
| int | level | ||
| ) |
| void* cuddLevelQueueFirst | ( | DdLevelQueue * | queue, |
| void * | key, | ||
| int | level | ||
| ) |
| DdLevelQueue* cuddLevelQueueInit | ( | int | levels, |
| int | itemSize, | ||
| int | numBuckets | ||
| ) |
| void cuddLevelQueueQuit | ( | DdLevelQueue * | queue | ) |
| int cuddLinearAndSifting | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
Function********************************************************************
Synopsis [BDD reduction based on combination of sifting and linear transformations.]
Description [BDD reduction based on combination of sifting and linear transformations. Assumes that no dead nodes are present.
Returns 1 if successful; 0 otherwise.]
SideEffects [None]
Definition at line 236 of file cuddLinear.c.
| int cuddLinearInPlace | ( | DdManager * | table, |
| int | x, | ||
| int | y | ||
| ) |
Function********************************************************************
Synopsis [Linearly combines two adjacent variables.]
Description [Linearly combines two adjacent variables. Specifically, replaces the top variable with the exclusive nor of the two variables. It assumes that no dead nodes are present on entry to this procedure. The procedure then guarantees that no dead nodes will be present when it terminates. cuddLinearInPlace assumes that x < y. Returns the number of keys in the table if successful; 0 otherwise.]
SideEffects [The two subtables corrresponding to variables x and y are modified. The global counters of the unique table are also affected.]
SeeAlso [cuddSwapInPlace]
Definition at line 360 of file cuddLinear.c.
| void cuddLocalCacheClearAll | ( | DdManager * | manager | ) |
Function********************************************************************
Synopsis [Clears the local caches of a manager.]
Description [Clears the local caches of a manager. Used before reordering.]
SideEffects [None]
SeeAlso []
Definition at line 423 of file cuddLCache.c.
| void cuddLocalCacheClearDead | ( | DdManager * | manager | ) |
Function********************************************************************
Synopsis [Clears the dead entries of the local caches of a manager.]
Description [Clears the dead entries of the local caches of a manager. Used during garbage collection.]
SideEffects [None]
SeeAlso []
Definition at line 371 of file cuddLCache.c.
| DdLocalCache* cuddLocalCacheInit | ( | DdManager * | manager, |
| unsigned int | keySize, | ||
| unsigned int | cacheSize, | ||
| unsigned int | maxCacheSize | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Initializes a local computed table.]
Description [Initializes a computed table. Returns a pointer the the new local cache in case of success; NULL otherwise.]
SideEffects [None]
SeeAlso [cuddInitCache]
Definition at line 202 of file cuddLCache.c.
| void cuddLocalCacheInsert | ( | DdLocalCache * | cache, |
| DdNodePtr * | key, | ||
| DdNode * | value | ||
| ) |
Function********************************************************************
Synopsis [Inserts a result in a local cache.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 291 of file cuddLCache.c.
| DdNode* cuddLocalCacheLookup | ( | DdLocalCache * | cache, |
| DdNodePtr * | key | ||
| ) |
Function********************************************************************
Synopsis [Looks up in a local cache.]
Description [Looks up in a local cache. Returns the result if found; it returns NULL if no result is found.]
SideEffects [None]
SeeAlso []
Definition at line 324 of file cuddLCache.c.
| void cuddLocalCacheQuit | ( | DdLocalCache * | cache | ) |
Function********************************************************************
Synopsis [Shuts down a local computed table.]
Description [Initializes the computed table. It is called by Cudd_Init. Returns a pointer the the new local cache in case of success; NULL otherwise.]
SideEffects [None]
SeeAlso [cuddLocalCacheInit]
Definition at line 265 of file cuddLCache.c.
Function********************************************************************
Synopsis [Converts a ZDD cover to a BDD.]
Description [Converts a ZDD cover to a BDD. If successful, it returns a BDD node, otherwise it returns NULL. It is a recursive algorithm that works as follows. First it computes 3 cofactors of a ZDD cover: f1, f0 and fd. Second, it compute BDDs (b1, b0 and bd) of f1, f0 and fd. Third, it computes T=b1+bd and E=b0+bd. Fourth, it computes ITE(v,T,E) where v is the variable which has the index of the top node of the ZDD cover. In this case, since the index of v can be larger than either the one of T or the one of E, cuddUniqueInterIVO is called, where IVO stands for independent from variable ordering.]
SideEffects []
SeeAlso [Cudd_MakeBddFromZddCover]
Definition at line 797 of file cuddZddIsop.c.
| int cuddNextHigh | ( | DdManager * | table, |
| int | x | ||
| ) |
Function********************************************************************
Synopsis [Finds the next subtable with a larger index.]
Description [Finds the next subtable with a larger index. Returns the index.]
SideEffects [None]
SeeAlso [cuddNextLow]
Definition at line 715 of file cuddReorder.c.
| int cuddNextLow | ( | DdManager * | table, |
| int | x | ||
| ) |
Function********************************************************************
Synopsis [Finds the next subtable with a smaller index.]
Description [Finds the next subtable with a smaller index. Returns the index.]
SideEffects [None]
SeeAlso [cuddNextHigh]
Definition at line 737 of file cuddReorder.c.
Function********************************************************************
Synopsis [Recursively collects all the nodes of a DD in an array.]
Description [Traverses the DD f and collects all its nodes in an array. The caller should free the array returned by cuddNodeArray. Returns a pointer to the array of nodes in case of success; NULL otherwise. The nodes are collected in reverse topological order, so that a node is always preceded in the array by all its descendants.]
SideEffects [The number of nodes is returned as a side effect.]
SeeAlso [Cudd_FirstNode]
Definition at line 2987 of file cuddUtil.c.
Function********************************************************************
Synopsis [Prints a DD to the standard output. One line per node is printed.]
Description [Prints a DD to the standard output. One line per node is printed. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_PrintDebug]
Definition at line 2874 of file cuddUtil.c.
| void cuddPrintNode | ( | DdNode * | f, |
| FILE * | fp | ||
| ) |
Function********************************************************************
Synopsis [Prints out information on a node.]
Description [Prints out information on a node.]
SideEffects [None]
SeeAlso []
Definition at line 712 of file cuddCheck.c.
Function********************************************************************
Synopsis [Prints the variable groups as a parenthesized list.]
Description [Prints the variable groups as a parenthesized list. For each group the level range that it represents is printed. After each group, the group's flags are printed, preceded by a `|'. For each flag (except MTR_TERMINAL) a character is printed.
The second argument, silent, if different from 0, causes Cudd_PrintVarGroups to only check the syntax of the group tree.]
SideEffects [None]
SeeAlso []
Definition at line 749 of file cuddCheck.c.
Function********************************************************************
Synopsis [Brings children of a dead node back.]
Description []
SideEffects [None]
SeeAlso [cuddReclaimZdd]
Definition at line 580 of file cuddRef.c.
Function********************************************************************
Synopsis [Brings children of a dead ZDD node back.]
Description []
SideEffects [None]
SeeAlso [cuddReclaim]
Definition at line 634 of file cuddRef.c.
| void cuddRehash | ( | DdManager * | unique, |
| int | i | ||
| ) |
Function********************************************************************
Synopsis [Rehashes a unique subtable.]
Description [Doubles the size of a unique subtable and rehashes its contents.]
SideEffects [None]
SeeAlso []
Definition at line 1559 of file cuddTable.c.
| DdNode* cuddRemapUnderApprox | ( | DdManager * | dd, |
| DdNode * | f, | ||
| int | numVars, | ||
| int | threshold, | ||
| double | quality | ||
| ) |
| int cuddResizeLinear | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Resizes the linear transform matrix.]
Description [Resizes the linear transform matrix. Returns 1 if successful; 0 otherwise.]
SideEffects [none]
SeeAlso []
Definition at line 800 of file cuddLinear.c.
| int cuddResizeTableZdd | ( | DdManager * | unique, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Increases the number of ZDD subtables in a unique table so that it meets or exceeds index.]
Description [Increases the number of ZDD subtables in a unique table so that it meets or exceeds index. When new ZDD variables are created, it is possible to preserve the functions unchanged, or it is possible to preserve the covers unchanged, but not both. cuddResizeTableZdd preserves the covers. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [ddResizeTable]
Definition at line 2270 of file cuddTable.c.
| void cuddSetInteract | ( | DdManager * | table, |
| int | x, | ||
| int | y | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Set interaction matrix entries.]
Description [Given a pair of variables 0 <= x < y < table->size, sets the corresponding bit of the interaction matrix to 1.]
SideEffects [None]
SeeAlso []
Definition at line 153 of file cuddInteract.c.
| void cuddShrinkDeathRow | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Shrinks the death row.]
Description [Shrinks the death row by a factor of four.]
SideEffects [None]
SeeAlso [cuddClearDeathRow]
Definition at line 684 of file cuddRef.c.
| void cuddShrinkSubtable | ( | DdManager * | unique, |
| int | i | ||
| ) |
Function********************************************************************
Synopsis [Shrinks a subtable.]
Description [Shrinks a subtable.]
SideEffects [None]
SeeAlso [cuddRehash]
Definition at line 1731 of file cuddTable.c.
| int cuddSifting | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
Function********************************************************************
Synopsis [Implementation of Rudell's sifting algorithm.]
Description [Implementation of Rudell's sifting algorithm. Assumes that no dead nodes are present.
Returns 1 if successful; 0 otherwise.]
SideEffects [None]
Definition at line 502 of file cuddReorder.c.
| void cuddSlowTableGrowth | ( | DdManager * | unique | ) |
Function********************************************************************
Synopsis [Adjusts parameters of a table to slow down its growth.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 2414 of file cuddTable.c.
| DdNode* cuddSolveEqnRecur | ( | DdManager * | bdd, |
| DdNode * | F, | ||
| DdNode * | Y, | ||
| DdNode ** | G, | ||
| int | n, | ||
| int * | yIndex, | ||
| int | i | ||
| ) |
| DdNode* cuddSplitSetRecur | ( | DdManager * | manager, |
| st_table * | mtable, | ||
| int * | varSeen, | ||
| DdNode * | p, | ||
| double | n, | ||
| double | max, | ||
| int | index | ||
| ) |
| enum st_retval cuddStCountfree | ( | char * | key, |
| char * | value, | ||
| char * | arg | ||
| ) |
Function********************************************************************
Synopsis [Frees the memory used to store the minterm counts recorded in the visited table.]
Description [Frees the memory used to store the minterm counts recorded in the visited table. Returns ST_CONTINUE.]
SideEffects [None]
Definition at line 2903 of file cuddUtil.c.
| DdNode* cuddSubsetShortPaths | ( | DdManager * | dd, |
| DdNode * | f, | ||
| int | numVars, | ||
| int | threshold, | ||
| int | hardlimit | ||
| ) |
| int cuddSwapInPlace | ( | DdManager * | table, |
| int | x, | ||
| int | y | ||
| ) |
Function********************************************************************
Synopsis [Swaps two adjacent variables.]
Description [Swaps two adjacent variables. It assumes that no dead nodes are present on entry to this procedure. The procedure then guarantees that no dead nodes will be present when it terminates. cuddSwapInPlace assumes that x < y. Returns the number of keys in the table if successful; 0 otherwise.]
SideEffects [None]
Definition at line 760 of file cuddReorder.c.
| int cuddSwapping | ( | DdManager * | table, |
| int | lower, | ||
| int | upper, | ||
| Cudd_ReorderingType | heuristic | ||
| ) |
Function********************************************************************
Synopsis [Reorders variables by a sequence of (non-adjacent) swaps.]
Description [Implementation of Plessier's algorithm that reorders variables by a sequence of (non-adjacent) swaps.
Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 604 of file cuddReorder.c.
| int cuddSymmCheck | ( | DdManager * | table, |
| int | x, | ||
| int | y | ||
| ) |
Function********************************************************************
Synopsis [Checks for symmetry of x and y.]
Description [Checks for symmetry of x and y. Ignores projection functions, unless they are isolated. Returns 1 in case of symmetry; 0 otherwise.]
SideEffects [None]
Definition at line 188 of file cuddSymmetry.c.
| int cuddSymmSifting | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
Function********************************************************************
Synopsis [Symmetric sifting algorithm.]
Description [Symmetric sifting algorithm. Assumes that no dead nodes are present.
Returns 1 plus the number of symmetric variables if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddSymmSiftingConv]
Definition at line 318 of file cuddSymmetry.c.
| int cuddSymmSiftingConv | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
Function********************************************************************
Synopsis [Symmetric sifting to convergence algorithm.]
Description [Symmetric sifting to convergence algorithm. Assumes that no dead nodes are present.
Returns 1 plus the number of symmetric variables if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddSymmSifting]
Definition at line 439 of file cuddSymmetry.c.
| int cuddTestInteract | ( | DdManager * | table, |
| int | x, | ||
| int | y | ||
| ) |
Function********************************************************************
Synopsis [Test interaction matrix entries.]
Description [Given a pair of variables 0 <= x < y < table->size, tests whether the corresponding bit of the interaction matrix is 1. Returns the value of the bit.]
SideEffects [None]
SeeAlso []
Definition at line 188 of file cuddInteract.c.
| int cuddTreeSifting | ( | DdManager * | table, |
| Cudd_ReorderingType | method | ||
| ) |
Function********************************************************************
Synopsis [Tree sifting algorithm.]
Description [Tree sifting algorithm. Assumes that a tree representing a group hierarchy is passed as a parameter. It then reorders each group in postorder fashion by calling ddTreeSiftingAux. Assumes that no dead nodes are present. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
Definition at line 271 of file cuddGroup.c.
| DdNode* cuddUnderApprox | ( | DdManager * | dd, |
| DdNode * | f, | ||
| int | numVars, | ||
| int | threshold, | ||
| int | safe, | ||
| double | quality | ||
| ) |
| DdNode* cuddUniqueConst | ( | DdManager * | unique, |
| CUDD_VALUE_TYPE | value | ||
| ) |
Function********************************************************************
Synopsis [Checks the unique table for the existence of a constant node.]
Description [Checks the unique table for the existence of a constant node. If it does not exist, it creates a new one. Does not modify the reference count of whatever is returned. A newly created internal node comes back with a reference count 0. Returns a pointer to the new node.]
SideEffects [None]
Definition at line 1479 of file cuddTable.c.
Function********************************************************************
Synopsis [Checks the unique table for the existence of an internal node.]
Description [Checks the unique table for the existence of an internal node. If it does not exist, it creates a new one. Does not modify the reference count of whatever is returned. A newly created internal node comes back with a reference count 0. For a newly created node, increments the reference counts of what T and E point to. Returns a pointer to the new node if successful; NULL if memory is exhausted or if reordering took place.]
SideEffects [None]
SeeAlso [cuddUniqueInterZdd]
Definition at line 1137 of file cuddTable.c.
Function********************************************************************
Synopsis [Wrapper for cuddUniqueInter that is independent of variable ordering.]
Description [Wrapper for cuddUniqueInter that is independent of variable ordering (IVO). This function does not require parameter index to precede the indices of the top nodes of T and E in the variable order. Returns a pointer to the result node under normal conditions; NULL if reordering occurred or memory was exhausted.]
SideEffects [None]
SeeAlso [cuddUniqueInter Cudd_MakeBddFromZddCover]
Definition at line 1333 of file cuddTable.c.
Function********************************************************************
Synopsis [Checks the unique table for the existence of an internal ZDD node.]
Description [Checks the unique table for the existence of an internal ZDD node. If it does not exist, it creates a new one. Does not modify the reference count of whatever is returned. A newly created internal node comes back with a reference count 0. For a newly created node, increments the reference counts of what T and E point to. Returns a pointer to the new node if successful; NULL if memory is exhausted or if reordering took place.]
SideEffects [None]
SeeAlso [cuddUniqueInter]
Definition at line 1372 of file cuddTable.c.
| void cuddUpdateInteractionMatrix | ( | DdManager * | table, |
| int | xindex, | ||
| int | yindex | ||
| ) |
Function********************************************************************
Synopsis [Updates the interaction matrix.]
Description []
SideEffects [none]
SeeAlso []
Definition at line 714 of file cuddLinear.c.
| int cuddWindowReorder | ( | DdManager * | table, |
| int | low, | ||
| int | high, | ||
| Cudd_ReorderingType | submethod | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Reorders by applying the method of the sliding window.]
Description [Reorders by applying the method of the sliding window. Tries all possible permutations to the variables in a window that slides from low to high. The size of the window is determined by submethod. Assumes that no dead nodes are present. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 138 of file cuddWindow.c.
| int cuddZddAlignToBdd | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Reorders ZDD variables according to the order of the BDD variables.]
Description [Reorders ZDD variables according to the order of the BDD variables. This function can be called at the end of BDD reordering to insure that the order of the ZDD variables is consistent with the order of the BDD variables. The number of ZDD variables must be a multiple of the number of BDD variables. Let M be the ratio of the two numbers. cuddZddAlignToBdd then considers the ZDD variables from M*i to (M+1)*i-1 as corresponding to BDD variable i. This function should be normally called from Cudd_ReduceHeap, which clears the cache. Returns 1 in case of success; 0 otherwise.]
SideEffects [Changes the ZDD variable order for all diagrams and performs garbage collection of the ZDD unique table.]
SeeAlso [Cudd_zddShuffleHeap Cudd_ReduceHeap]
Definition at line 348 of file cuddZddReord.c.
Function********************************************************************
Synopsis [Substitutes a variable with its complement in a ZDD.]
Description [Substitutes a variable with its complement in a ZDD. returns a pointer to the result if successful; NULL otherwise. cuddZddChange performs the same function as Cudd_zddChange, but does not restart if reordering has taken place. Therefore it can be called from within a recursive procedure.]
SideEffects [None]
SeeAlso [Cudd_zddChange]
Definition at line 967 of file cuddZddSetop.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddChange.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 795 of file cuddZddSetop.c.
Function********************************************************************
Synopsis [Computes a complement of a ZDD node.]
Description [Computes the complement of a ZDD node. So far, since we couldn't find a direct way to get the complement of a ZDD cover, we first convert a ZDD cover to a BDD, then make the complement of the ZDD cover from the complement of the BDD node by using ISOP.]
SideEffects [The result depends on current variable order.]
SeeAlso []
Definition at line 1518 of file cuddZddFuncs.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddDiff.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 713 of file cuddZddSetop.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddDivide.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddDivide]
Definition at line 1155 of file cuddZddFuncs.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddDivideF.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddDivideF]
Definition at line 1255 of file cuddZddFuncs.c.
| void cuddZddFreeUniv | ( | DdManager * | zdd | ) |
Function********************************************************************
Synopsis [Frees the ZDD universe.]
Description [Frees the ZDD universe.]
SideEffects [None]
SeeAlso [cuddZddInitUniv]
Definition at line 294 of file cuddInit.c.
Function********************************************************************
Synopsis [Computes the two-way decomposition of f w.r.t. v.]
Description []
SideEffects [The results are returned in f1 and f0.]
SeeAlso [cuddZddGetCofactors3]
Definition at line 1483 of file cuddZddFuncs.c.
| int cuddZddGetCofactors3 | ( | DdManager * | dd, |
| DdNode * | f, | ||
| int | v, | ||
| DdNode ** | f1, | ||
| DdNode ** | f0, | ||
| DdNode ** | fd | ||
| ) |
Function********************************************************************
Synopsis [Computes the three-way decomposition of f w.r.t. v.]
Description [Computes the three-way decomposition of function f (represented by a ZDD) wit respect to variable v. Returns 0 if successful; 1 otherwise.]
SideEffects [The results are returned in f1, f0, and fd.]
SeeAlso [cuddZddGetCofactors2]
Definition at line 1356 of file cuddZddFuncs.c.
| int cuddZddGetNegVarIndex | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Returns the index of negative ZDD variable.]
Description [Returns the index of negative ZDD variable.]
SideEffects []
SeeAlso []
Definition at line 1582 of file cuddZddFuncs.c.
| int cuddZddGetNegVarLevel | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Returns the level of negative ZDD variable.]
Description [Returns the level of negative ZDD variable.]
SideEffects []
SeeAlso []
Definition at line 1624 of file cuddZddFuncs.c.
Function********************************************************************
Synopsis [Wrapper for cuddUniqueInterZdd.]
Description [Wrapper for cuddUniqueInterZdd, which applies the ZDD reduction rule. Returns a pointer to the result node under normal conditions; NULL if reordering occurred or memory was exhausted.]
SideEffects [None]
SeeAlso [cuddUniqueInterZdd]
Definition at line 1050 of file cuddTable.c.
Function********************************************************************
Synopsis [Wrapper for cuddUniqueInterZdd that is independent of variable ordering.]
Description [Wrapper for cuddUniqueInterZdd that is independent of variable ordering (IVO). This function does not require parameter index to precede the indices of the top nodes of g and h in the variable order. Returns a pointer to the result node under normal conditions; NULL if reordering occurred or memory was exhausted.]
SideEffects [None]
SeeAlso [cuddZddGetNode cuddZddIsop]
Definition at line 1083 of file cuddTable.c.
| int cuddZddGetPosVarIndex | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Returns the index of positive ZDD variable.]
Description [Returns the index of positive ZDD variable.]
SideEffects []
SeeAlso []
Definition at line 1561 of file cuddZddFuncs.c.
| int cuddZddGetPosVarLevel | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Returns the level of positive ZDD variable.]
Description [Returns the level of positive ZDD variable.]
SideEffects []
SeeAlso []
Definition at line 1603 of file cuddZddFuncs.c.
| int cuddZddInitUniv | ( | DdManager * | zdd | ) |
Function********************************************************************
Synopsis [Initializes the ZDD universe.]
Description [Initializes the ZDD universe. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddZddFreeUniv]
Definition at line 245 of file cuddInit.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddIntersect.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 638 of file cuddZddSetop.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddIsop.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddIsop]
Definition at line 231 of file cuddZddIsop.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddIte.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 423 of file cuddZddSetop.c.
| int cuddZddLinearSifting | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Implementation of the linear sifting algorithm for ZDDs.]
Description [Implementation of the linear sifting algorithm for ZDDs. Assumes that no dead nodes are present.
Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 152 of file cuddZddLin.c.
| int cuddZddNextHigh | ( | DdManager * | table, |
| int | x | ||
| ) |
Function********************************************************************
Synopsis [Finds the next subtable with a larger index.]
Description [Finds the next subtable with a larger index. Returns the index.]
SideEffects [None]
SeeAlso []
Definition at line 409 of file cuddZddReord.c.
| int cuddZddNextLow | ( | DdManager * | table, |
| int | x | ||
| ) |
Function********************************************************************
Synopsis [Finds the next subtable with a smaller index.]
Description [Finds the next subtable with a smaller index. Returns the index.]
SideEffects [None]
SeeAlso []
Definition at line 431 of file cuddZddReord.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddProduct.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddProduct]
Definition at line 376 of file cuddZddFuncs.c.
| int cuddZddSifting | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
Function********************************************************************
Synopsis [Implementation of Rudell's sifting algorithm.]
Description [Implementation of Rudell's sifting algorithm. Assumes that no dead nodes are present.
Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 863 of file cuddZddReord.c.
Function********************************************************************
Synopsis [Computes the negative cofactor of a ZDD w.r.t. a variable.]
Description [Computes the negative cofactor of a ZDD w.r.t. a variable. In terms of combinations, the result is the set of all combinations in which the variable is negated. Returns a pointer to the result if successful; NULL otherwise. cuddZddSubset0 performs the same function as Cudd_zddSubset0, but does not restart if reordering has taken place. Therefore it can be called from within a recursive procedure.]
SideEffects [None]
SeeAlso [cuddZddSubset1 Cudd_zddSubset0]
Definition at line 919 of file cuddZddSetop.c.
Function********************************************************************
Synopsis [Computes the positive cofactor of a ZDD w.r.t. a variable.]
Description [Computes the positive cofactor of a ZDD w.r.t. a variable. In terms of combinations, the result is the set of all combinations in which the variable is asserted. Returns a pointer to the result if successful; NULL otherwise. cuddZddSubset1 performs the same function as Cudd_zddSubset1, but does not restart if reordering has taken place. Therefore it can be called from within a recursive procedure.]
SideEffects [None]
SeeAlso [cuddZddSubset0 Cudd_zddSubset1]
Definition at line 870 of file cuddZddSetop.c.
| int cuddZddSwapInPlace | ( | DdManager * | table, |
| int | x, | ||
| int | y | ||
| ) |
Function********************************************************************
Synopsis [Swaps two adjacent variables.]
Description [Swaps two adjacent variables. It assumes that no dead nodes are present on entry to this procedure. The procedure then guarantees that no dead nodes will be present when it terminates. cuddZddSwapInPlace assumes that x < y. Returns the number of keys in the table if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 480 of file cuddZddReord.c.
| int cuddZddSwapping | ( | DdManager * | table, |
| int | lower, | ||
| int | upper, | ||
| Cudd_ReorderingType | heuristic | ||
| ) |
Function********************************************************************
Synopsis [Reorders variables by a sequence of (non-adjacent) swaps.]
Description [Implementation of Plessier's algorithm that reorders variables by a sequence of (non-adjacent) swaps.
Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 742 of file cuddZddReord.c.
| int cuddZddSymmCheck | ( | DdManager * | table, |
| int | x, | ||
| int | y | ||
| ) |
Function********************************************************************
Synopsis [Checks for symmetry of x and y.]
Description [Checks for symmetry of x and y. Ignores projection functions, unless they are isolated. Returns 1 in case of symmetry; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 193 of file cuddZddSymm.c.
| int cuddZddSymmSifting | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
Function********************************************************************
Synopsis [Symmetric sifting algorithm for ZDDs.]
Description [Symmetric sifting algorithm. Assumes that no dead nodes are present.
Returns 1 plus the number of symmetric variables if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddZddSymmSiftingConv]
Definition at line 298 of file cuddZddSymm.c.
| int cuddZddSymmSiftingConv | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
Function********************************************************************
Synopsis [Symmetric sifting to convergence algorithm for ZDDs.]
Description [Symmetric sifting to convergence algorithm for ZDDs. Assumes that no dead nodes are present.
Returns 1 plus the number of symmetric variables if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddZddSymmSifting]
Definition at line 423 of file cuddZddSymm.c.
| int cuddZddTreeSifting | ( | DdManager * | table, |
| Cudd_ReorderingType | method | ||
| ) |
Function********************************************************************
Synopsis [Tree sifting algorithm for ZDDs.]
Description [Tree sifting algorithm for ZDDs. Assumes that a tree representing a group hierarchy is passed as a parameter. It then reorders each group in postorder fashion by calling zddTreeSiftingAux. Assumes that no dead nodes are present. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
Definition at line 228 of file cuddZddGroup.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddUnateProduct.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddUnateProduct]
Definition at line 613 of file cuddZddFuncs.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddUnion.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 549 of file cuddZddSetop.c.
| int cuddZddUniqueCompare | ( | int * | ptr_x, |
| int * | ptr_y | ||
| ) |
Function********************************************************************
Synopsis [Comparison function used by qsort.]
Description [Comparison function used by qsort to order the variables according to the number of keys in the subtables. Returns the difference in number of keys between the two variables being compared.]
SideEffects [None]
SeeAlso []
Definition at line 455 of file cuddZddReord.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddWeakDiv.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddWeakDiv]
Definition at line 757 of file cuddZddFuncs.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddWeakDivF.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddWeakDivF]
Definition at line 918 of file cuddZddFuncs.c.
1.8.13