|
abc-master
|
|
abc-master
|
Go to the source code of this file.
Data Structures | |
| 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.1 |
| #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 | 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 | cuddF2L(f) ((Cudd_Regular(f)->Id << 1) | Cudd_IsComplement(f)) |
| #define | ddHash(f, g, s) ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s)) |
| #define | ddCHash2(o, f, g, s) (((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s)) |
| #define | ddCHash2_(o, f, g) (((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2)) |
| #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 ABC_PTRINT_T | ptrint |
| typedef ABC_PTRUINT_T | 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 cuddF2L | ( | f | ) | ((Cudd_Regular(f)->Id << 1) | Cudd_IsComplement(f)) |
| #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-2004, 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 ddCHash2 | ( | o, | |
| f, | |||
| g, | |||
| s | |||
| ) | (((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s)) |
Macro***********************************************************************
Synopsis [Hash function for the cache.]
Description []
SideEffects [none]
SeeAlso [ddHash ddCHash2] Macro***********************************************************************
Synopsis [Hash function for the cache for functions with two operands.]
Description []
SideEffects [none]
SeeAlso [ddHash ddCHash]
| #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 for Cudd_addBddPattern.]
Description [Performs the recursive step for Cudd_addBddPattern. Returns a pointer to the resulting BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 493 of file cuddBridge.c.
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 562 of file cuddAddIte.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_addCompose.]
Description [Performs the recursive step of Cudd_addCompose. Returns the composed BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addCompose]
Definition at line 952 of file cuddCompose.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_addConstrain.]
Description [Performs the recursive step of Cudd_addConstrain. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addConstrain]
Definition at line 1203 of file cuddGenCof.c.
AutomaticStart
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_addExistAbstract.]
Description [Performs the recursive step of Cudd_addExistAbstract. Returns the ADD obtained by abstracting the variables of cube from f, if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 256 of file cuddAddAbs.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 445 of file cuddAddIte.c.
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_addNegate.]
Description [Implements the recursive step of Cudd_addNegate. Returns a pointer to the result.]
SideEffects [None]
Definition at line 180 of file cuddAddNeg.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_addOrAbstract.]
Description [Performs the recursive step of Cudd_addOrAbstract. Returns the ADD obtained by abstracting the variables of cube from f, if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 469 of file cuddAddAbs.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_addRestrict.]
Description [Performs the recursive step of Cudd_addRestrict. Returns the restricted ADD if successful; otherwise NULL.]
SideEffects [None]
SeeAlso [Cudd_addRestrict]
Definition at line 1307 of file cuddGenCof.c.
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_addRoundOff.]
Description [Implements the recursive step of Cudd_addRoundOff. Returns a pointer to the result.]
SideEffects [None]
Definition at line 240 of file cuddAddNeg.c.
Function********************************************************************
Synopsis [Performs the recursive step of addScalarInverse.]
Description [Returns a pointer to the resulting ADD in case of success. Returns NULL if any discriminants smaller than epsilon is encountered.]
SideEffects [None]
Definition at line 156 of file cuddAddInv.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_addUnivAbstract.]
Description [Performs the recursive step of Cudd_addUnivAbstract. Returns the ADD obtained by abstracting the variables of cube from f, if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 361 of file cuddAddAbs.c.
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 235 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 158 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 1251 of file cuddReorder.c.
Function********************************************************************
Synopsis [Takes the AND of two BDDs and simultaneously abstracts the variables in cube.]
Description [Takes the AND 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 200 of file cuddAndAbs.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 886 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 636 of file cuddBddAbs.c.
Function********************************************************************
Synopsis [Approximates the conjunction of two BDDs f and g.]
Description [Approximates the conjunction of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.]
SideEffects [None]
SeeAlso [Cudd_bddClippingAnd]
Definition at line 201 of file cuddClip.c.
| DdNode* cuddBddClippingAndAbstract | ( | DdManager * | dd, |
| DdNode * | f, | ||
| DdNode * | g, | ||
| DdNode * | cube, | ||
| int | maxDepth, | ||
| int | direction | ||
| ) |
Function********************************************************************
Synopsis [Approximates the conjunction of two BDDs f and g and simultaneously abstracts the variables in cube.]
Description [Approximates the conjunction of two BDDs f and g and simultaneously abstracts the variables in cube. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.]
SideEffects [None]
SeeAlso [Cudd_bddClippingAndAbstract]
Definition at line 233 of file cuddClip.c.
| DdNode* cuddBddClosestCube | ( | DdManager * | dd, |
| DdNode * | f, | ||
| DdNode * | g, | ||
| CUDD_VALUE_TYPE | bound | ||
| ) |
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_bddClosestCube.]
Description [Performs the recursive step of Cudd_bddClosestCube. Returns the cube if succesful; NULL otherwise. The procedure uses a four-way recursion to examine all four combinations of cofactors of f and g according to the following formula.
H(f,g) = min(H(ft,gt), H(fe,ge), H(ft,ge)+1, H(fe,gt)+1)
Bounding is based on the following observations.
The variable bound is set at the largest value of the distance that we are still interested in. Therefore, we desist when
(bound == -1) and (F != not(G)) or (bound == 0) and (F == not(G)).
If we were maximally aggressive in using the bound, we would always set the bound to the minimum distance seen thus far minus one. That is, we would maintain the invariant
bound < minD,
except at the very beginning, when we have no value for minD.
However, we do not use bound < minD when examining the two negative cofactors, because we try to find a large cube at minimum distance. To do so, we try to find a cube in the negative cofactors at the same or smaller distance from the cube found in the positive cofactors.
When we compute H(ft,ge) and H(fe,gt) we know that we are going to add 1 to the result of the recursive call to account for the difference in the splitting variable. Therefore, we decrease the bound correspondingly.
Another important observation concerns the need of examining all four pairs of cofators only when both f and g depend on the top variable.
Suppose gt == ge == g. (That is, g does not depend on the top variable.) Then
H(f,g) = min(H(ft,g), H(fe,g), H(ft,g)+1, H(fe,g)+1)
= min(H(ft,g), H(fe,g)) .
Therefore, under these circumstances, we skip the two "cross" cases.
An interesting feature of this function is the scheme used for caching the results in the global computed table. Since we have a cube and a distance, we combine them to form an ADD. The combination replaces the zero child of the top node of the cube with the negative of the distance. (The use of the negative is to avoid ambiguity with 1.) The degenerate cases (zero and one) are treated specially because the distance is known (0 for one, and infinity for zero).]
SideEffects [None]
SeeAlso [Cudd_bddClosestCube]
Definition at line 1646 of file cuddPriority.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_bddCompose.]
Description [Performs the recursive step of Cudd_bddCompose. Exploits the fact that the composition of f' with g produces the complement of the composition of f with g to better utilize the cache. Returns the composed BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddCompose]
Definition at line 850 of file cuddCompose.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_bddConstrain.]
Description [Performs the recursive step of Cudd_bddConstrain. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddConstrain]
Definition at line 783 of file cuddGenCof.c.
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 352 of file cuddBddAbs.c.
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_bddIntersect.]
Description []
SideEffects [None]
SeeAlso [Cudd_bddIntersect]
Definition at line 771 of file cuddBddIte.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_bddIsop.]
Description []
SideEffects [None]
SeeAlso [Cudd_bddIsop]
Definition at line 575 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 633 of file cuddBddIte.c.
Function********************************************************************
Synopsis [Performs safe minimization of a BDD.]
Description [Performs safe minimization of a BDD. Given the BDD f of a function to be minimized and a BDD c representing the care set, Cudd_bddLICompaction produces the BDD of a function that agrees with f wherever c is 1. Safe minimization means that the size of the result is guaranteed not to exceed the size of f. This function is based on the DAC97 paper by Hong et al.. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddLICompaction]
Definition at line 1434 of file cuddGenCof.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_bddLiteralSetIntersection.]
Description [Performs the recursive step of Cudd_bddLiteralSetIntersection. Scans the cubes for common variables, and checks whether they agree in phase. Returns a pointer to the resulting cube if successful; NULL otherwise.]
SideEffects [None]
Definition at line 153 of file cuddLiteral.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 900 of file cuddSat.c.
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_bddAnd.]
Description [Implements the recursive step of Cudd_bddNPAnd. Returns a pointer to the result is successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddNPAnd]
Definition at line 1062 of file cuddGenCof.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_bddRestrict.]
Description [Performs the recursive step of Cudd_bddRestrict. Returns the restricted BDD if successful; otherwise NULL.]
SideEffects [None]
SeeAlso [Cudd_bddRestrict]
Definition at line 912 of file cuddGenCof.c.
Function********************************************************************
Synopsis [Convert a BDD from a manager to another one.]
Description [Convert a BDD from a manager to another one. Returns a pointer to the BDD in the destination manager if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddTransfer]
Definition at line 443 of file cuddBridge.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 464 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 1017 of file cuddBddIte.c.
| DdNode* cuddBiasedUnderApprox | ( | DdManager * | dd, |
| DdNode * | f, | ||
| DdNode * | b, | ||
| int | numVars, | ||
| int | threshold, | ||
| double | quality1, | ||
| double | quality0 | ||
| ) |
Function********************************************************************
Synopsis [Applies the biased remapping underappoximation algorithm.]
Description [Applies the biased remapping underappoximation algorithm. Proceeds in three phases:
Returns the approximated BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_BiasedUnderApprox]
Definition at line 691 of file cuddApprox.c.
| void cuddCacheFlush | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Flushes the cache.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 1047 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.]
Description []
SideEffects [None]
SeeAlso [cuddCacheInsert2 cuddCacheInsert1]
Definition at line 222 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 369 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 435 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 785 of file cuddCache.c.
| void cuddCacheResize | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Resizes the cache.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 925 of file cuddCache.c.
Function********************************************************************
Synopsis [Checks whether g is the BDD of a cube.]
Description [Checks whether g is the BDD of a cube. Returns 1 in case of success; 0 otherwise. The constant 1 is a valid cube, but all other constant functions cause cuddCheckCube to return 0.]
SideEffects [None]
SeeAlso []
Definition at line 193 of file cuddCof.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 230 of file cuddCof.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 1079 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 721 of file cuddCache.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_CProjection.]
Description [Performs the recursive step of Cudd_CProjection. Returns the projection if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_CProjection]
Definition at line 1425 of file cuddPriority.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 2108 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 406 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 153 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 659 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 192 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 729 of file cuddTable.c.
Function********************************************************************
Synopsis [Computes the children of g.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 162 of file cuddCof.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 538 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 648 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 767 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 874 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 984 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 703 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 819 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 928 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 1040 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 595 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 639 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 136 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 237 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 759 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 351 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 1795 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 762 of file cuddRef.c.
| void cuddLevelQueueDequeue | ( | DdLevelQueue * | queue, |
| int | level | ||
| ) |
Function********************************************************************
Synopsis [Remove an item from the front of a level queue.]
Description [Remove an item from the front of a level queue.]
SideEffects [None]
SeeAlso [cuddLevelQueueEnqueue]
Definition at line 354 of file cuddLevelQ.c.
| void* cuddLevelQueueEnqueue | ( | DdLevelQueue * | queue, |
| void * | key, | ||
| int | level | ||
| ) |
Function********************************************************************
Synopsis [Inserts a new key in a level queue.]
Description [Inserts a new key in a level queue. A new entry is created in the queue only if the node is not already enqueued. Returns a pointer to the queue item if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [cuddLevelQueueInit cuddLevelQueueDequeue]
Definition at line 282 of file cuddLevelQ.c.
| DdLevelQueue* cuddLevelQueueInit | ( | int | levels, |
| int | itemSize, | ||
| int | numBuckets | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Initializes a level queue.]
Description [Initializes a level queue. A level queue is a queue where inserts are based on the levels of the nodes. Within each level the policy is FIFO. Level queues are useful in traversing a BDD top-down. Queue items are kept in a free list when dequeued for efficiency. Returns a pointer to the new queue if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [cuddLevelQueueQuit cuddLevelQueueEnqueue cuddLevelQueueDequeue]
Definition at line 169 of file cuddLevelQ.c.
| void cuddLevelQueueQuit | ( | DdLevelQueue * | queue | ) |
Function********************************************************************
Synopsis [Shuts down a level queue.]
Description [Shuts down a level queue and releases all the associated memory.]
SideEffects [None]
SeeAlso [cuddLevelQueueInit]
Definition at line 244 of file cuddLevelQ.c.
| 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 240 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 364 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 404 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 352 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 183 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 272 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 305 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 246 of file cuddLCache.c.
Function********************************************************************
Synopsis [Converts a ZDD cover to a BDD graph.]
Description [Converts a ZDD cover to a BDD graph. If successful, it returns a BDD node, otherwise it returns NULL. It is a recursive algorithm as the following. First computes 3 cofactors of a ZDD cover; f1, f0 and fd. Second, compute BDDs(b1, b0 and bd) of f1, f0 and fd. Third, compute T=b1+bd and E=b0+bd. Fourth, compute 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 one of T or one of E, cuddUniqueInterIVO is called, here IVO stands for independent variable ordering.]
SideEffects []
SeeAlso [Cudd_MakeBddFromZddCover]
Definition at line 800 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 716 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 738 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 2979 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 2866 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 710 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 747 of file cuddCheck.c.
Function********************************************************************
Synopsis [Brings children of a dead node back.]
Description []
SideEffects [None]
SeeAlso [cuddReclaimZdd]
Definition at line 584 of file cuddRef.c.
Function********************************************************************
Synopsis [Brings children of a dead ZDD node back.]
Description []
SideEffects [None]
SeeAlso [cuddReclaim]
Definition at line 638 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 1530 of file cuddTable.c.
| DdNode* cuddRemapUnderApprox | ( | DdManager * | dd, |
| DdNode * | f, | ||
| int | numVars, | ||
| int | threshold, | ||
| double | quality | ||
| ) |
Function********************************************************************
Synopsis [Applies the remapping underappoximation algorithm.]
Description [Applies the remapping underappoximation algorithm. Proceeds in three phases:
Returns the approximated BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_RemapUnderApprox]
Definition at line 601 of file cuddApprox.c.
| 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 804 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 2241 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 156 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 688 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 1702 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 508 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 2385 of file cuddTable.c.
| DdNode* cuddSolveEqnRecur | ( | DdManager * | bdd, |
| DdNode * | F, | ||
| DdNode * | Y, | ||
| DdNode ** | G, | ||
| int | n, | ||
| int * | yIndex, | ||
| int | i | ||
| ) |
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_SolveEqn.]
Description [Implements the recursive step of Cudd_SolveEqn. Returns NULL if the intermediate solution blows up or reordering occurs. The parametric solutions are stored in the array G.]
SideEffects [none]
SeeAlso [Cudd_SolveEqn, Cudd_VerifySol]
Definition at line 210 of file cuddSolve.c.
Function********************************************************************
Synopsis [The main procedure that returns a subset by choosing the heavier branch in the BDD.]
Description [Here a subset BDD is built by throwing away one of the children. Starting at root, annotate each node with the number of minterms (in terms of the total number of variables specified - numVars), number of nodes taken by the DAG rooted at this node and number of additional nodes taken by the child that has the lesser minterms. The child with the lower number of minterms is thrown away and a dyanmic count of the nodes of the subset is kept. Once the threshold is reached the subset is returned to the calling procedure.]
SideEffects [None]
SeeAlso [Cudd_SubsetHeavyBranch]
Definition at line 305 of file cuddSubsetHB.c.
| DdNode* cuddSubsetShortPaths | ( | DdManager * | dd, |
| DdNode * | f, | ||
| int | numVars, | ||
| int | threshold, | ||
| int | hardlimit | ||
| ) |
Function********************************************************************
Synopsis [The outermost procedure to return a subset of the given BDD with the shortest path lengths.]
Description [The outermost procedure to return a subset of the given BDD with the largest cubes. The path lengths are calculated, the maximum allowable path length is determined and the number of nodes of this path length that can be used to build a subset. If the threshold is larger than the size of the original BDD, the original BDD is returned. ]
SideEffects [None]
SeeAlso [Cudd_SubsetShortPaths]
Definition at line 316 of file cuddSubsetSP.c.
| 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 761 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 605 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 192 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 322 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 442 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 191 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 274 of file cuddGroup.c.
| DdNode* cuddUnderApprox | ( | DdManager * | dd, |
| DdNode * | f, | ||
| int | numVars, | ||
| int | threshold, | ||
| int | safe, | ||
| double | quality | ||
| ) |
Function********************************************************************
Synopsis [Applies Tom Shiple's underappoximation algorithm.]
Description [Applies Tom Shiple's underappoximation algorithm. Proceeds in three phases:
Returns the approximated BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_UnderApprox]
Definition at line 511 of file cuddApprox.c.
| 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 1450 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 1128 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 1304 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 1343 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 718 of file cuddLinear.c.
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_VerifySol. ]
Description []
SideEffects [none]
SeeAlso [Cudd_VerifySol]
Definition at line 336 of file cuddSolve.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 142 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 352 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 971 of file cuddZddSetop.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddChange.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 799 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 1522 of file cuddZddFuncs.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddDiff.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 717 of file cuddZddSetop.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddDivide.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddDivide]
Definition at line 1159 of file cuddZddFuncs.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddDivideF.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddDivideF]
Definition at line 1259 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 301 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 1487 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 1360 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 1586 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 1628 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 1041 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 1074 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 1565 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 1607 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 252 of file cuddInit.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddIntersect.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 642 of file cuddZddSetop.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddIsop.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddIsop]
Definition at line 234 of file cuddZddIsop.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddIte.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 427 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 156 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 413 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 435 of file cuddZddReord.c.
Function********************************************************************
Synopsis [Prints a ZDD to the standard output. One line per node is printed.]
Description [Prints a ZDD to the standard output. One line per node is printed. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_zddPrintDebug]
Definition at line 822 of file cuddZddUtil.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddProduct.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddProduct]
Definition at line 380 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 867 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 923 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 874 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 484 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 746 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 197 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 302 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 232 of file cuddZddGroup.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddUnateProduct.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddUnateProduct]
Definition at line 617 of file cuddZddFuncs.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddUnion.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 553 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 459 of file cuddZddReord.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddWeakDiv.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddWeakDiv]
Definition at line 761 of file cuddZddFuncs.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddWeakDivF.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddWeakDivF]
Definition at line 922 of file cuddZddFuncs.c.
1.8.6