|
SVF
|
Go to the source code of this file.
Classes | |
| struct | DdChildren |
| struct | DdNode |
Macros | |
| #define | CUDD_VERSION "2.5.0" |
| #define | SIZEOF_LONG 4 |
| #define | CUDD_TRUE 1 |
| #define | CUDD_FALSE 0 |
| #define | CUDD_VALUE_TYPE double |
| #define | CUDD_OUT_OF_MEM -1 |
| #define | CUDD_UNIQUE_SLOTS 256 /* initial size of subtables */ |
| #define | CUDD_CACHE_SLOTS 262144 /* default size of the cache */ |
| #define | CUDD_RESIDUE_DEFAULT 0 |
| #define | CUDD_RESIDUE_MSB 1 |
| #define | CUDD_RESIDUE_TC 2 |
| #define | CUDD_MAXINDEX ((DdHalfWord) ~0) |
| #define | CUDD_CONST_INDEX CUDD_MAXINDEX |
| #define | DD_APA_BITS 16 |
| #define | DD_APA_BASE (1 << DD_APA_BITS) |
| #define | DD_APA_HEXPRINT "%04x" |
| #define | DD_APA_MASK (DD_APA_BASE - 1) |
| #define | Cudd_IsConstant(node) ((Cudd_Regular(node))->index == CUDD_CONST_INDEX) |
| #define | Cudd_Not(node) ((DdNode *)((long)(node) ^ 01)) |
| #define | Cudd_NotCond(node, c) ((DdNode *)((long)(node) ^ (c))) |
| #define | Cudd_Regular(node) ((DdNode *)((unsigned long)(node) & ~01)) |
| #define | Cudd_Complement(node) ((DdNode *)((unsigned long)(node) | 01)) |
| #define | Cudd_IsComplement(node) ((int) ((long) (node) & 01)) |
| #define | Cudd_T(node) ((Cudd_Regular(node))->type.kids.T) |
| #define | Cudd_E(node) ((Cudd_Regular(node))->type.kids.E) |
| #define | Cudd_V(node) ((Cudd_Regular(node))->type.value) |
| #define | Cudd_ReadIndex(dd, index) (Cudd_ReadPerm(dd,index)) |
| #define | Cudd_ForeachCube(manager, f, gen, cube, value) |
| #define | Cudd_ForeachPrime(manager, l, u, gen, cube) |
| #define | Cudd_ForeachNode(manager, f, gen, node) |
| #define | Cudd_zddForeachPath(manager, f, gen, path) |
Typedefs | |
| typedef unsigned short | DdHalfWord |
| typedef struct DdNode | DdNode |
| typedef struct DdChildren | DdChildren |
| typedef struct DdManager | DdManager |
| typedef struct DdGen | DdGen |
| typedef unsigned short int | DdApaDigit |
| typedef unsigned int | DdApaDoubleDigit |
| typedef DdApaDigit * | DdApaNumber |
| typedef struct DdTlcInfo | DdTlcInfo |
| typedef int(* | DD_HFP) (DdManager *, const char *, void *) |
| typedef DdNode *(* | DD_PRFP) (DdManager *, int, DdNode **, DdNode **, DdNode **) |
| typedef DdNode *(* | DD_AOP) (DdManager *, DdNode **, DdNode **) |
| typedef DdNode *(* | DD_MAOP) (DdManager *, DdNode *) |
| typedef DdNode *(* | DD_CTFP) (DdManager *, DdNode *, DdNode *) |
| typedef DdNode *(* | DD_CTFP1) (DdManager *, DdNode *) |
| typedef void(* | DD_OOMFP) (long) |
| typedef int(* | DD_QSFP) (const void *, const void *) |
| #define CUDD_CACHE_SLOTS 262144 /* default size of the cache */ |
| #define Cudd_Complement | ( | node | ) | ((DdNode *)((unsigned long)(node) | 01)) |
| #define CUDD_CONST_INDEX CUDD_MAXINDEX |
| #define Cudd_E | ( | node | ) | ((Cudd_Regular(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.]
SideEffects [none]
SeeAlso [Cudd_T Cudd_V]
| #define Cudd_ForeachCube | ( | manager, | |
| f, | |||
| gen, | |||
| cube, | |||
| value | |||
| ) |
Macro***********************************************************************
Synopsis [Iterates over the cubes of a decision diagram.]
Description [Iterates over the cubes of a decision diagram f.
Cudd_ForeachCube allocates and frees the generator. Therefore the application should not try to do that. Also, the cube is freed at the end of Cudd_ForeachCube and hence is not available outside of the loop.
CAUTION: It is assumed that dynamic reordering will not occur while there are open generators. It is the user's responsibility to make sure that dynamic reordering does not occur. As long as new nodes are not created during generation, and dynamic reordering is not called explicitly, dynamic reordering will not occur. Alternatively, it is sufficient to disable dynamic reordering. It is a mistake to dispose of a diagram on which generation is ongoing.]
SideEffects [none]
SeeAlso [Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube Cudd_GenFree Cudd_IsGenEmpty Cudd_AutodynDisable]
| #define Cudd_ForeachNode | ( | manager, | |
| f, | |||
| gen, | |||
| node | |||
| ) |
Macro***********************************************************************
Synopsis [Iterates over the nodes of a decision diagram.]
Description [Iterates over the nodes of a decision diagram f.
The nodes are returned in a seemingly random order. Cudd_ForeachNode allocates and frees the generator. Therefore the application should not try to do that.
CAUTION: It is assumed that dynamic reordering will not occur while there are open generators. It is the user's responsibility to make sure that dynamic reordering does not occur. As long as new nodes are not created during generation, and dynamic reordering is not called explicitly, dynamic reordering will not occur. Alternatively, it is sufficient to disable dynamic reordering. It is a mistake to dispose of a diagram on which generation is ongoing.]
SideEffects [none]
SeeAlso [Cudd_ForeachCube Cudd_FirstNode Cudd_NextNode Cudd_GenFree Cudd_IsGenEmpty Cudd_AutodynDisable]
| #define Cudd_ForeachPrime | ( | manager, | |
| l, | |||
| u, | |||
| gen, | |||
| cube | |||
| ) |
Macro***********************************************************************
Synopsis [Iterates over the primes of a Boolean function.]
Description [Iterates over the primes of a Boolean function producing a prime and irredundant cover.
The Boolean function is described by an upper bound and a lower bound. If the function is completely specified, the two bounds coincide. Cudd_ForeachPrime allocates and frees the generator. Therefore the application should not try to do that. Also, the cube is freed at the end of Cudd_ForeachPrime and hence is not available outside of the loop.
CAUTION: It is a mistake to change a diagram on which generation is ongoing.]
SideEffects [none]
SeeAlso [Cudd_ForeachCube Cudd_FirstPrime Cudd_NextPrime Cudd_GenFree Cudd_IsGenEmpty]
| #define Cudd_IsComplement | ( | node | ) | ((int) ((long) (node) & 01)) |
| #define Cudd_IsConstant | ( | node | ) | ((Cudd_Regular(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 Cudd_IsConstant may be either regular or complemented.]
SideEffects [none]
SeeAlso []
| #define CUDD_MAXINDEX ((DdHalfWord) ~0) |
| #define Cudd_Not | ( | node | ) | ((DdNode *)((long)(node) ^ 01)) |
| #define Cudd_NotCond | ( | node, | |
| c | |||
| ) | ((DdNode *)((long)(node) ^ (c))) |
Macro***********************************************************************
Synopsis [Complements a DD if a condition is true.]
Description [Complements a DD if condition c is true; c should be either 0 or 1, because it is used directly (for efficiency). If in doubt on the values c may take, use "(c) ? Cudd_Not(node) : node".]
SideEffects [none]
SeeAlso [Cudd_Not]
| #define Cudd_ReadIndex | ( | dd, | |
| index | |||
| ) | (Cudd_ReadPerm(dd,index)) |
Macro***********************************************************************
Synopsis [Returns the current position in the order of variable index.]
Description [Returns the current position in the order of variable index. This macro is obsolete and is kept for compatibility. New applications should use Cudd_ReadPerm instead.]
SideEffects [none]
SeeAlso [Cudd_ReadPerm]
| #define Cudd_Regular | ( | node | ) | ((DdNode *)((unsigned long)(node) & ~01)) |
| #define Cudd_T | ( | node | ) | ((Cudd_Regular(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.]
SideEffects [none]
SeeAlso [Cudd_E Cudd_V]
| #define Cudd_V | ( | node | ) | ((Cudd_Regular(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.]
SideEffects [none]
SeeAlso [Cudd_T Cudd_E]
| #define CUDD_VERSION "2.5.0" |
CHeaderFile*****************************************************************
FileName [cudd.h]
PackageName [cudd]
Synopsis [The University of Colorado decision diagram package.]
Description [External functions and data strucures of the CUDD package.
Modified by Abelardo Pardo to interface it to VIS. ]
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 Cudd_zddForeachPath | ( | manager, | |
| f, | |||
| gen, | |||
| path | |||
| ) |
Macro***********************************************************************
Synopsis [Iterates over the paths of a ZDD.]
Description [Iterates over the paths of a ZDD f.
Cudd_zddForeachPath allocates and frees the generator. Therefore the application should not try to do that. Also, the path is freed at the end of Cudd_zddForeachPath and hence is not available outside of the loop.
CAUTION: It is assumed that dynamic reordering will not occur while there are open generators. It is the user's responsibility to make sure that dynamic reordering does not occur. As long as new nodes are not created during generation, and dynamic reordering is not called explicitly, dynamic reordering will not occur. Alternatively, it is sufficient to disable dynamic reordering. It is a mistake to dispose of a diagram on which generation is ongoing.]
SideEffects [none]
SeeAlso [Cudd_zddFirstPath Cudd_zddNextPath Cudd_GenFree Cudd_IsGenEmpty Cudd_AutodynDisable]
| #define DD_APA_BASE (1 << DD_APA_BITS) |
| #define DD_APA_MASK (DD_APA_BASE - 1) |
| typedef unsigned short int DdApaDigit |
| typedef unsigned int DdApaDoubleDigit |
| typedef DdApaDigit* DdApaNumber |
| typedef struct DdChildren DdChildren |
| typedef unsigned short DdHalfWord |
| enum Cudd_AggregationType |
Enum************************************************************************
Synopsis [Type of aggregation methods.]
Description [Type of aggregation methods.]
| Enumerator | |
|---|---|
| CUDD_NO_CHECK | |
| CUDD_GROUP_CHECK | |
| CUDD_GROUP_CHECK2 | |
| CUDD_GROUP_CHECK3 | |
| CUDD_GROUP_CHECK4 | |
| CUDD_GROUP_CHECK5 | |
| CUDD_GROUP_CHECK6 | |
| CUDD_GROUP_CHECK7 | |
| CUDD_GROUP_CHECK8 | |
| CUDD_GROUP_CHECK9 | |
Definition at line 180 of file cudd.h.
| enum Cudd_ErrorType |
Enum************************************************************************
Synopsis [Type of error codes.]
Description [Type of error codes.]
| Enumerator | |
|---|---|
| CUDD_NO_ERROR | |
| CUDD_MEMORY_OUT | |
| CUDD_TOO_MANY_NODES | |
| CUDD_MAX_MEM_EXCEEDED | |
| CUDD_TIMEOUT_EXPIRED | |
| CUDD_INVALID_ARG | |
| CUDD_INTERNAL_ERROR | |
Definition at line 216 of file cudd.h.
| enum Cudd_HookType |
Enum************************************************************************
Synopsis [Type of hooks.]
Description [Type of hooks.]
| Enumerator | |
|---|---|
| CUDD_PRE_GC_HOOK | |
| CUDD_POST_GC_HOOK | |
| CUDD_PRE_REORDERING_HOOK | |
| CUDD_POST_REORDERING_HOOK | |
| enum Cudd_LazyGroupType |
Enum************************************************************************
Synopsis [Group type for lazy sifting.]
Description [Group type for lazy sifting.]
| Enumerator | |
|---|---|
| CUDD_LAZY_NONE | |
| CUDD_LAZY_SOFT_GROUP | |
| CUDD_LAZY_HARD_GROUP | |
| CUDD_LAZY_UNGROUP | |
| enum Cudd_ReorderingType |
Enum************************************************************************
Synopsis [Type of reordering algorithm.]
Description [Type of reordering algorithm.]
Definition at line 147 of file cudd.h.
| enum Cudd_VariableType |
Enum************************************************************************
Synopsis [Variable type.]
Description [Variable type. Currently used only in lazy sifting.]
| Enumerator | |
|---|---|
| CUDD_VAR_PRIMARY_INPUT | |
| CUDD_VAR_PRESENT_STATE | |
| CUDD_VAR_NEXT_STATE | |
| DdNode* Cudd_addApply | ( | DdManager * | dd, |
| DdNode * | *)(DdManager *, DdNode **, DdNode **, | ||
| DdNode * | f, | ||
| DdNode * | g | ||
| ) |
| DdNode* Cudd_addBddInterval | ( | DdManager * | dd, |
| DdNode * | f, | ||
| CUDD_VALUE_TYPE | lower, | ||
| CUDD_VALUE_TYPE | upper | ||
| ) |
| DdNode* Cudd_addBddStrictThreshold | ( | DdManager * | dd, |
| DdNode * | f, | ||
| CUDD_VALUE_TYPE | value | ||
| ) |
| DdNode* Cudd_addBddThreshold | ( | DdManager * | dd, |
| DdNode * | f, | ||
| CUDD_VALUE_TYPE | value | ||
| ) |
Function********************************************************************
Synopsis [Computes the complement of an ADD a la C language.]
Description [Computes the complement of an ADD a la C language: The complement of 0 is 1 and the complement of everything else is 0. Returns a pointer to the resulting ADD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addNegate]
Definition at line 343 of file cuddAddIte.c.
Function********************************************************************
Synopsis [Computes the cube of an array of ADD variables.]
Description [Computes the cube of an array of ADD variables. If non-null, the phase argument indicates which literal of each variable should appear in the cube. If phase[i] is nonzero, then the positive literal is used. If phase is NULL, the cube is positive unate. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects [none]
SeeAlso [Cudd_bddComputeCube]
Definition at line 2254 of file cuddUtil.c.
| DdNode* Cudd_addConst | ( | DdManager * | dd, |
| CUDD_VALUE_TYPE | c | ||
| ) |
Function********************************************************************
Synopsis [Returns the ADD for constant c.]
Description [Retrieves the ADD for constant c if it already exists, or creates a new ADD. Returns a pointer to the ADD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addNewVar Cudd_addIthVar]
Definition at line 634 of file cuddAPI.c.
Function********************************************************************
Synopsis [Checks whether ADD g is constant whenever ADD f is 1.]
Description [Checks whether ADD g is constant whenever ADD f is 1. f must be a 0-1 ADD. Returns a pointer to the resulting ADD (which may or may not be constant) or DD_NON_CONSTANT. If f is identically 0, the check is assumed to be successful, and the background value is returned. No new nodes are created.]
SideEffects [None]
SeeAlso [Cudd_addIteConstant Cudd_addLeq]
Definition at line 256 of file cuddAddIte.c.
| DdNode* Cudd_addGeneralVectorCompose | ( | DdManager * | dd, |
| DdNode * | f, | ||
| DdNode ** | vectorOn, | ||
| DdNode ** | vectorOff | ||
| ) |
| int Cudd_addHarwell | ( | FILE * | fp, |
| DdManager * | dd, | ||
| DdNode ** | E, | ||
| DdNode *** | x, | ||
| DdNode *** | y, | ||
| DdNode *** | xn, | ||
| DdNode *** | yn_, | ||
| int * | nx, | ||
| int * | ny, | ||
| int * | m, | ||
| int * | n, | ||
| int | bx, | ||
| int | sx, | ||
| int | by, | ||
| int | sy, | ||
| int | pr | ||
| ) |
| int Cudd_AddHook | ( | DdManager * | dd, |
| DD_HFP | f, | ||
| Cudd_HookType | where | ||
| ) |
Function********************************************************************
Synopsis [Adds a function to a hook.]
Description [Adds a function to a hook. A hook is a list of application-provided functions called on certain occasions by the package. Returns 1 if the function is successfully added; 2 if the function was already in the list; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_RemoveHook]
Definition at line 3569 of file cuddAPI.c.
AutomaticEnd Function********************************************************************
Synopsis [Implements ITE(f,g,h).]
Description [Implements ITE(f,g,h). This procedure assumes that f is a 0-1 ADD. Returns a pointer to the resulting ADD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddIte Cudd_addIteConstant Cudd_addApply]
Definition at line 125 of file cuddAddIte.c.
Function********************************************************************
Synopsis [Implements ITEconstant for ADDs.]
Description [Implements ITEconstant for ADDs. f must be a 0-1 ADD. Returns a pointer to the resulting ADD (which may or may not be constant) or DD_NON_CONSTANT. No new nodes are created. This function can be used, for instance, to check that g has a constant value (specified by h) whenever f is 1. If the constant value is unknown, then one should use Cudd_addEvalConst.]
SideEffects [None]
SeeAlso [Cudd_addIte Cudd_addEvalConst Cudd_bddIteConstant]
Definition at line 159 of file cuddAddIte.c.
Function********************************************************************
Synopsis [Returns the ADD variable with index i.]
Description [Retrieves the ADD variable with index i if it already exists, or creates a new ADD variable. Returns a pointer to the variable if successful; NULL otherwise. An ADD variable differs from a BDD variable because it points to the arithmetic zero, instead of having a complement pointer to 1. ]
SideEffects [None]
SeeAlso [Cudd_addNewVar Cudd_bddIthVar Cudd_addConst Cudd_addNewVarAtLevel]
Definition at line 398 of file cuddAPI.c.
Function********************************************************************
Synopsis [Determines whether f is less than or equal to g.]
Description [Returns 1 if f is less than or equal to g; 0 otherwise. No new nodes are created. This procedure works for arbitrary ADDs. For 0-1 ADDs Cudd_addEvalConst is more efficient.]
SideEffects [None]
SeeAlso [Cudd_addIteConstant Cudd_addEvalConst Cudd_bddLeq]
Definition at line 372 of file cuddAddIte.c.
AutomaticStart
AutomaticEnd Function********************************************************************
Synopsis [Returns a new ADD variable.]
Description [Creates a new ADD variable. The new variable has an index equal to the largest previous index plus 1. Returns a pointer to the new variable if successful; NULL otherwise. An ADD variable differs from a BDD variable because it points to the arithmetic zero, instead of having a complement pointer to 1. ]
SideEffects [None]
SeeAlso [Cudd_bddNewVar Cudd_addIthVar Cudd_addConst Cudd_addNewVarAtLevel]
Definition at line 273 of file cuddAPI.c.
Function********************************************************************
Synopsis [Returns a new ADD variable at a specified level.]
Description [Creates a new ADD variable. The new variable has an index equal to the largest previous index plus 1 and is positioned at the specified level in the order. Returns a pointer to the new variable if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addNewVar Cudd_addIthVar Cudd_bddNewVarAtLevel]
Definition at line 304 of file cuddAPI.c.
| int Cudd_addRead | ( | FILE * | fp, |
| DdManager * | dd, | ||
| DdNode ** | E, | ||
| DdNode *** | x, | ||
| DdNode *** | y, | ||
| DdNode *** | xn, | ||
| DdNode *** | yn_, | ||
| int * | nx, | ||
| int * | ny, | ||
| int * | m, | ||
| int * | n, | ||
| int | bx, | ||
| int | sx, | ||
| int | by, | ||
| int | sy | ||
| ) |
| DdApaDigit Cudd_ApaAdd | ( | int | digits, |
| DdApaNumber | a, | ||
| DdApaNumber | b, | ||
| DdApaNumber | sum | ||
| ) |
| int Cudd_ApaCompare | ( | int | digitsFirst, |
| DdApaNumber | first, | ||
| int | digitsSecond, | ||
| DdApaNumber | second | ||
| ) |
| int Cudd_ApaCompareRatios | ( | int | digitsFirst, |
| DdApaNumber | firstNum, | ||
| unsigned int | firstDen, | ||
| int | digitsSecond, | ||
| DdApaNumber | secondNum, | ||
| unsigned int | secondDen | ||
| ) |
| void Cudd_ApaCopy | ( | int | digits, |
| DdApaNumber | source, | ||
| DdApaNumber | dest | ||
| ) |
| DdApaNumber Cudd_ApaCountMinterm | ( | DdManager * | manager, |
| DdNode * | node, | ||
| int | nvars, | ||
| int * | digits | ||
| ) |
| unsigned int Cudd_ApaIntDivision | ( | int | digits, |
| DdApaNumber | dividend, | ||
| unsigned int | divisor, | ||
| DdApaNumber | quotient | ||
| ) |
| int Cudd_ApaNumberOfDigits | ( | int | binaryDigits | ) |
| void Cudd_ApaPowerOfTwo | ( | int | digits, |
| DdApaNumber | number, | ||
| int | power | ||
| ) |
| int Cudd_ApaPrintDecimal | ( | FILE * | fp, |
| int | digits, | ||
| DdApaNumber | number | ||
| ) |
| int Cudd_ApaPrintExponential | ( | FILE * | fp, |
| int | digits, | ||
| DdApaNumber | number, | ||
| int | precision | ||
| ) |
| int Cudd_ApaPrintHex | ( | FILE * | fp, |
| int | digits, | ||
| DdApaNumber | number | ||
| ) |
| void Cudd_ApaSetToLiteral | ( | int | digits, |
| DdApaNumber | number, | ||
| DdApaDigit | literal | ||
| ) |
| void Cudd_ApaShiftRight | ( | int | digits, |
| DdApaDigit | in, | ||
| DdApaNumber | a, | ||
| DdApaNumber | b | ||
| ) |
| DdApaDigit Cudd_ApaShortDivision | ( | int | digits, |
| DdApaNumber | dividend, | ||
| DdApaDigit | divisor, | ||
| DdApaNumber | quotient | ||
| ) |
| DdApaDigit Cudd_ApaSubtract | ( | int | digits, |
| DdApaNumber | a, | ||
| DdApaNumber | b, | ||
| DdApaNumber | diff | ||
| ) |
| void Cudd_AutodynDisable | ( | DdManager * | unique | ) |
| void Cudd_AutodynDisableZdd | ( | DdManager * | unique | ) |
| void Cudd_AutodynEnable | ( | DdManager * | unique, |
| Cudd_ReorderingType | method | ||
| ) |
Function********************************************************************
Synopsis [Enables automatic dynamic reordering of BDDs and ADDs.]
Description [Enables automatic dynamic reordering of BDDs and ADDs. Parameter method is used to determine the method used for reordering. If CUDD_REORDER_SAME is passed, the method is unchanged.]
SideEffects [None]
SeeAlso [Cudd_AutodynDisable Cudd_ReorderingStatus Cudd_AutodynEnableZdd]
Definition at line 909 of file cuddAPI.c.
| void Cudd_AutodynEnableZdd | ( | DdManager * | unique, |
| Cudd_ReorderingType | method | ||
| ) |
Function********************************************************************
Synopsis [Enables automatic dynamic reordering of ZDDs.]
Description [Enables automatic dynamic reordering of ZDDs. Parameter method is used to determine the method used for reordering ZDDs. If CUDD_REORDER_SAME is passed, the method is unchanged.]
SideEffects [None]
SeeAlso [Cudd_AutodynDisableZdd Cudd_ReorderingStatusZdd Cudd_AutodynEnable]
Definition at line 1000 of file cuddAPI.c.
| double Cudd_AverageDistance | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Computes the average distance between adjacent nodes.]
Description [Computes the average distance between adjacent nodes in the manager. Adjacent nodes are node pairs such that the second node is the then child, else child, or next node in the collision list.]
SideEffects [None]
SeeAlso []
Definition at line 2622 of file cuddUtil.c.
Function********************************************************************
Synopsis [Computes the conjunction of two BDDs f and g.]
Description [Computes 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_bddIte Cudd_addApply Cudd_bddAndAbstract Cudd_bddIntersect Cudd_bddOr Cudd_bddNand Cudd_bddNor Cudd_bddXor Cudd_bddXnor]
Definition at line 350 of file cuddBddIte.c.
| DdNode* Cudd_bddAndAbstractLimit | ( | DdManager * | manager, |
| DdNode * | f, | ||
| DdNode * | g, | ||
| DdNode * | cube, | ||
| unsigned int | limit | ||
| ) |
Function********************************************************************
Synopsis [Computes the conjunction of two BDDs f and g. Returns NULL if too many nodes are required.]
Description [Computes the conjunction of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up or more new nodes than limit are required.]
SideEffects [None]
SeeAlso [Cudd_bddAnd]
Definition at line 382 of file cuddBddIte.c.
| int Cudd_bddBindVar | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Prevents sifting of a variable.]
Description [This function sets a flag to prevent sifting of a variable. Returns 1 if successful; 0 otherwise (i.e., invalid variable index).]
SideEffects [Changes the "bindVar" flag in DdSubtable.]
SeeAlso [Cudd_bddUnbindVar]
Definition at line 4352 of file cuddAPI.c.
Function********************************************************************
Synopsis [Computes the boolean difference of f with respect to x.]
Description [Computes the boolean difference of f with respect to the variable with index x. Returns the BDD of the boolean difference if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 287 of file cuddBddAbs.c.
| DdNode* Cudd_bddClippingAndAbstract | ( | DdManager * | dd, |
| DdNode * | f, | ||
| DdNode * | g, | ||
| DdNode * | cube, | ||
| int | maxDepth, | ||
| int | direction | ||
| ) |
Function********************************************************************
Synopsis [Computes the cube of an array of BDD variables.]
Description [Computes the cube of an array of BDD variables. If non-null, the phase argument indicates which literal of each variable should appear in the cube. If phase[i] is nonzero, then the positive literal is used. If phase is NULL, the cube is positive unate. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addComputeCube Cudd_IndicesToCube Cudd_CubeArrayToBdd]
Definition at line 2204 of file cuddUtil.c.
AutomaticEnd Function********************************************************************
Synopsis [Existentially abstracts all the variables in cube from f.]
Description [Existentially abstracts all the variables in cube from f. Returns the abstracted BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddUnivAbstract Cudd_addExistAbstract]
Definition at line 127 of file cuddBddAbs.c.
| DdNode* Cudd_bddExistAbstractLimit | ( | DdManager * | manager, |
| DdNode * | f, | ||
| DdNode * | cube, | ||
| unsigned int | limit | ||
| ) |
Function********************************************************************
Synopsis [Existentially abstracts all the variables in cube from f.]
Description [Existentially abstracts all the variables in cube from f. Returns the abstracted BDD if successful; NULL if the intermediate result blows up or more new nodes than limit are required.]
SideEffects [None]
SeeAlso [Cudd_bddExistAbstract]
Definition at line 166 of file cuddBddAbs.c.
Function********************************************************************
Synopsis [Returns a function included in the intersection of f and g.]
Description [Computes a function included in the intersection of f and g. (That is, a witness that the intersection is not empty.) Cudd_bddIntersect tries to build as few new nodes as possible. If the only result of interest is whether f and g intersect, Cudd_bddLeq should be used instead.]
SideEffects [None]
SeeAlso [Cudd_bddLeq Cudd_bddIteConstant]
Definition at line 318 of file cuddBddIte.c.
| DdNode* Cudd_bddInterval | ( | DdManager * | dd, |
| int | N, | ||
| DdNode ** | x, | ||
| unsigned int | lowerB, | ||
| unsigned int | upperB | ||
| ) |
| int Cudd_bddIsNsVar | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Checks whether a variable is next state.]
Description [Checks whether a variable is next state. Returns 1 if the variable's type is present state; 0 if the variable exists but is not a present state; -1 if the variable does not exist.]
SideEffects [none]
SeeAlso [Cudd_bddSetNsVar Cudd_bddIsPiVar Cudd_bddIsPsVar]
Definition at line 4551 of file cuddAPI.c.
Function********************************************************************
Synopsis [Computes a BDD in the interval between L and U with a simple sum-of-product cover.]
Description [Computes a BDD in the interval between L and U with a simple sum-of-product cover. This procedure is similar to Cudd_zddIsop, but it does not return the ZDD for the cover. Returns a pointer to the BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_zddIsop]
Definition at line 170 of file cuddZddIsop.c.
| int Cudd_bddIsPiVar | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Checks whether a variable is primary input.]
Description [Checks whether a variable is primary input. Returns 1 if the variable's type is primary input; 0 if the variable exists but is not a primary input; -1 if the variable does not exist.]
SideEffects [none]
SeeAlso [Cudd_bddSetPiVar Cudd_bddIsPsVar Cudd_bddIsNsVar]
Definition at line 4503 of file cuddAPI.c.
| int Cudd_bddIsPsVar | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Checks whether a variable is present state.]
Description [Checks whether a variable is present state. Returns 1 if the variable's type is present state; 0 if the variable exists but is not a present state; -1 if the variable does not exist.]
SideEffects [none]
SeeAlso [Cudd_bddSetPsVar Cudd_bddIsPiVar Cudd_bddIsNsVar]
Definition at line 4527 of file cuddAPI.c.
| int Cudd_bddIsVarHardGroup | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Checks whether a variable is set to be in a hard group.]
Description [Checks whether a variable is set to be in a hard group. This function is used for lazy sifting. Returns 1 if the variable is marked to be in a hard group; 0 if the variable exists, but it is not marked to be in a hard group; -1 if the variable does not exist.]
SideEffects [none]
SeeAlso [Cudd_bddSetVarHardGroup]
Definition at line 4779 of file cuddAPI.c.
| int Cudd_bddIsVarToBeGrouped | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Checks whether a variable is set to be grouped.]
Description [Checks whether a variable is set to be grouped. This function is used for lazy sifting.]
SideEffects [none]
SeeAlso []
Definition at line 4702 of file cuddAPI.c.
| int Cudd_bddIsVarToBeUngrouped | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Checks whether a variable is set to be ungrouped.]
Description [Checks whether a variable is set to be ungrouped. This function is used for lazy sifting. Returns 1 if the variable is marked to be ungrouped; 0 if the variable exists, but it is not marked to be ungrouped; -1 if the variable does not exist.]
SideEffects [none]
SeeAlso [Cudd_bddSetVarToBeUngrouped]
Definition at line 4754 of file cuddAPI.c.
AutomaticEnd Function********************************************************************
Synopsis [Implements ITE(f,g,h).]
Description [Implements ITE(f,g,h). Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.]
SideEffects [None]
SeeAlso [Cudd_addIte Cudd_bddIteConstant Cudd_bddIntersect]
Definition at line 142 of file cuddBddIte.c.
Function********************************************************************
Synopsis [Implements ITEconstant(f,g,h).]
Description [Implements ITEconstant(f,g,h). Returns a pointer to the resulting BDD (which may or may not be constant) or DD_NON_CONSTANT. No new nodes are created.]
SideEffects [None]
SeeAlso [Cudd_bddIte Cudd_bddIntersect Cudd_bddLeq Cudd_addIteConstant]
Definition at line 210 of file cuddBddIte.c.
Function********************************************************************
Synopsis [Implements ITE(f,g,h). Returns NULL if too many nodes are required.]
Description [Implements ITE(f,g,h). Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up or more new nodes than limit are required.]
SideEffects [None]
SeeAlso [Cudd_bddIte]
Definition at line 175 of file cuddBddIte.c.
Function********************************************************************
Synopsis [Returns the BDD variable with index i.]
Description [Retrieves the BDD variable with index i if it already exists, or creates a new BDD variable. Returns a pointer to the variable if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddNewVar Cudd_addIthVar Cudd_bddNewVarAtLevel Cudd_ReadVars]
Definition at line 430 of file cuddAPI.c.
Function********************************************************************
Synopsis [Find a largest prime of a unate function.]
Description [Find a largest prime implicant of a unate function. Returns the BDD for the prime if succesful; NULL otherwise. The behavior is undefined if f is not unate. The third argument is used to determine whether f is unate positive (increasing) or negative (decreasing) in each of the variables in its support.]
SideEffects [None]
SeeAlso [Cudd_bddMaximallyExpand]
Definition at line 941 of file cuddSat.c.
Function********************************************************************
Synopsis [Determines whether f is less than or equal to g.]
Description [Returns 1 if f is less than or equal to g; 0 otherwise. No new nodes are created.]
SideEffects [None]
SeeAlso [Cudd_bddIteConstant Cudd_addEvalConst]
Definition at line 645 of file cuddBddIte.c.
Function********************************************************************
Synopsis [Tells whether f is less than of equal to G unless D is 1.]
Description [Tells whether f is less than of equal to G unless D is
SideEffects [None]
SeeAlso [Cudd_EquivDC Cudd_bddLeq Cudd_bddIteConstant]
Definition at line 629 of file cuddSat.c.
Function********************************************************************
Synopsis [Expands cube to a prime implicant of f.]
Description [Expands cube to a prime implicant of f. Returns the prime if successful; NULL otherwise. In particular, NULL is returned if cube is not a real cube or is not an implicant of f.]
SideEffects [None]
SeeAlso [Cudd_bddMaximallyExpand]
Definition at line 871 of file cuddSat.c.
Function********************************************************************
Synopsis [Expands lb to prime implicants of (f and ub).]
Description [Expands lb to all prime implicants of (f and ub) that contain lb. Assumes that lb is contained in ub. Returns the disjunction of the primes if lb is contained in f; returns the zero BDD if lb is not contained in f; returns NULL in case of failure. In particular, NULL is returned if cube is not a real cube or is not an implicant of f. Returning the disjunction of all prime implicants works because the resulting function is unate.]
SideEffects [None]
SeeAlso [Cudd_bddMakePrime]
Definition at line 906 of file cuddSat.c.
Function********************************************************************
Synopsis [Computes the NAND of two BDDs f and g.]
Description [Computes the NAND 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_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr Cudd_bddNor Cudd_bddXor Cudd_bddXnor]
Definition at line 486 of file cuddBddIte.c.
Function********************************************************************
Synopsis [Returns a new BDD variable.]
Description [Creates a new BDD variable. The new variable has an index equal to the largest previous index plus 1. Returns a pointer to the new variable if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addNewVar Cudd_bddIthVar Cudd_bddNewVarAtLevel]
Definition at line 337 of file cuddAPI.c.
Function********************************************************************
Synopsis [Returns a new BDD variable at a specified level.]
Description [Creates a new BDD variable. The new variable has an index equal to the largest previous index plus 1 and is positioned at the specified level in the order. Returns a pointer to the new variable if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddNewVar Cudd_bddIthVar Cudd_addNewVarAtLevel]
Definition at line 365 of file cuddAPI.c.
Function********************************************************************
Synopsis [Computes the NOR of two BDDs f and g.]
Description [Computes the NOR 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_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr Cudd_bddNand Cudd_bddXor Cudd_bddXnor]
Definition at line 518 of file cuddBddIte.c.
Function********************************************************************
Synopsis [Computes the disjunction of two BDDs f and g.]
Description [Computes the disjunction 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_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddNand Cudd_bddNor Cudd_bddXor Cudd_bddXnor]
Definition at line 417 of file cuddBddIte.c.
Function********************************************************************
Synopsis [Computes the disjunction of two BDDs f and g. Returns NULL if too many nodes are required.]
Description [Computes the disjunction of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up or more new nodes than limit are required.]
SideEffects [None]
SeeAlso [Cudd_bddOr]
Definition at line 450 of file cuddBddIte.c.
Function********************************************************************
Synopsis [Picks k on-set minterms evenly distributed from given DD.]
Description [Picks k on-set minterms evenly distributed from given DD. The minterms are in terms of vars. The array vars should contain at least all variables in the support of f; if this condition is not met the minterms built by this procedure may not be contained in f. Builds an array of BDDs for the minterms and returns a pointer to it if successful; NULL otherwise. There are three reasons why the procedure may fail:
f may be the constant 0; f. ]
SideEffects [None]
SeeAlso [Cudd_bddPickOneMinterm Cudd_bddPickOneCube]
Definition at line 1401 of file cuddUtil.c.
Function********************************************************************
Synopsis [Picks one on-set cube randomly from the given DD.]
Description [Picks one on-set cube randomly from the given DD. The cube is written into an array of characters. The array must have at least as many entries as there are variables. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddPickOneMinterm]
Definition at line 1229 of file cuddUtil.c.
Function********************************************************************
Synopsis [Picks one on-set minterm randomly from the given DD.]
Description [Picks one on-set minterm randomly from the given DD. The minterm is in terms of vars. The array vars should contain at least all variables in the support of f; if this condition is not met the minterm built by this procedure may not be contained in f. Builds a BDD for the minterm and returns a pointer to it if successful; NULL otherwise. There are three reasons why the procedure may fail:
f may be the constant 0; f. ]
SideEffects [None]
SeeAlso [Cudd_bddPickOneCube]
Definition at line 1299 of file cuddUtil.c.
Function********************************************************************
Synopsis [Prints a sum of prime implicants of a BDD.]
Description [Prints a sum of product cover for an incompletely specified function given by a lower bound and an upper bound. Each product is a prime implicant obtained by expanding the product corresponding to a path from node to the constant one. Uses the package default output file. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_PrintMinterm]
Definition at line 257 of file cuddUtil.c.
| int Cudd_bddRead | ( | FILE * | fp, |
| DdManager * | dd, | ||
| DdNode ** | E, | ||
| DdNode *** | x, | ||
| DdNode *** | y, | ||
| int * | nx, | ||
| int * | ny, | ||
| int * | m, | ||
| int * | n, | ||
| int | bx, | ||
| int | sx, | ||
| int | by, | ||
| int | sy | ||
| ) |
| int Cudd_bddReadPairIndex | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Reads a corresponding pair index for a given index.]
Description [Reads a corresponding pair index for a given index. These pair indices are present and next state variable. Returns the corresponding variable index if the variable exists; -1 otherwise.]
SideEffects [modifies the manager]
SeeAlso [Cudd_bddSetPairIndex]
Definition at line 4601 of file cuddAPI.c.
| void Cudd_bddRealignDisable | ( | DdManager * | unique | ) |
Function********************************************************************
Synopsis [Disables realignment of ZDD order to BDD order.]
Description []
SideEffects [None]
SeeAlso [Cudd_bddRealignEnable Cudd_bddRealignmentEnabled Cudd_zddRealignEnable Cudd_zddRealignmentEnabled]
Definition at line 1205 of file cuddAPI.c.
| void Cudd_bddRealignEnable | ( | DdManager * | unique | ) |
Function********************************************************************
Synopsis [Enables realignment of BDD order to ZDD order.]
Description [Enables realignment of the BDD variable order to the ZDD variable order after the ZDDs have been reordered. The number of ZDD variables must be a multiple of the number of BDD variables for realignment to make sense. If this condition is not met, Cudd_zddReduceHeap will return 0. Let M be the ratio of the two numbers. For the purpose of realignment, the ZDD variables from M*i to (M+1)*i-1 are reagarded as corresponding to BDD variable i. Realignment is initially disabled.]
SideEffects [None]
SeeAlso [Cudd_zddReduceHeap Cudd_bddRealignDisable Cudd_bddRealignmentEnabled Cudd_zddRealignDisable Cudd_zddRealignmentEnabled]
Definition at line 1183 of file cuddAPI.c.
| int Cudd_bddRealignmentEnabled | ( | DdManager * | unique | ) |
Function********************************************************************
Synopsis [Tells whether the realignment of BDD order to ZDD order is enabled.]
Description [Returns 1 if the realignment of BDD order to ZDD order is enabled; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddRealignEnable Cudd_bddRealignDisable Cudd_zddRealignEnable Cudd_zddRealignDisable]
Definition at line 1153 of file cuddAPI.c.
| int Cudd_bddResetVarToBeGrouped | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Resets a variable not to be grouped.]
Description [Resets a variable not to be grouped. This function is used for lazy sifting. Returns 1 if successful; 0 otherwise.]
SideEffects [modifies the manager]
SeeAlso [Cudd_bddSetVarToBeGrouped Cudd_bddSetVarHardGroup]
Definition at line 4675 of file cuddAPI.c.
| int Cudd_bddSetNsVar | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Sets a variable type to next state.]
Description [Sets a variable type to next state. The variable type is used by lazy sifting. Returns 1 if successful; 0 otherwise.]
SideEffects [modifies the manager]
SeeAlso [Cudd_bddSetPiVar Cudd_bddSetPsVar Cudd_bddIsNsVar]
Definition at line 4478 of file cuddAPI.c.
| int Cudd_bddSetPairIndex | ( | DdManager * | dd, |
| int | index, | ||
| int | pairIndex | ||
| ) |
Function********************************************************************
Synopsis [Sets a corresponding pair index for a given index.]
Description [Sets a corresponding pair index for a given index. These pair indices are present and next state variable. Returns 1 if successful; 0 otherwise.]
SideEffects [modifies the manager]
SeeAlso [Cudd_bddReadPairIndex]
Definition at line 4575 of file cuddAPI.c.
| int Cudd_bddSetPiVar | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Sets a variable type to primary input.]
Description [Sets a variable type to primary input. The variable type is used by lazy sifting. Returns 1 if successful; 0 otherwise.]
SideEffects [modifies the manager]
SeeAlso [Cudd_bddSetPsVar Cudd_bddSetNsVar Cudd_bddIsPiVar]
Definition at line 4430 of file cuddAPI.c.
| int Cudd_bddSetPsVar | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Sets a variable type to present state.]
Description [Sets a variable type to present state. The variable type is used by lazy sifting. Returns 1 if successful; 0 otherwise.]
SideEffects [modifies the manager]
SeeAlso [Cudd_bddSetPiVar Cudd_bddSetNsVar Cudd_bddIsPsVar]
Definition at line 4454 of file cuddAPI.c.
| int Cudd_bddSetVarHardGroup | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Sets a variable to be a hard group.]
Description [Sets a variable to be a hard group. This function is used for lazy sifting. Returns 1 if successful; 0 otherwise.]
SideEffects [modifies the manager]
SeeAlso [Cudd_bddSetVarToBeGrouped Cudd_bddResetVarToBeGrouped Cudd_bddIsVarHardGroup]
Definition at line 4651 of file cuddAPI.c.
| int Cudd_bddSetVarToBeGrouped | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Sets a variable to be grouped.]
Description [Sets a variable to be grouped. This function is used for lazy sifting. Returns 1 if successful; 0 otherwise.]
SideEffects [modifies the manager]
SeeAlso [Cudd_bddSetVarHardGroup Cudd_bddResetVarToBeGrouped]
Definition at line 4624 of file cuddAPI.c.
| int Cudd_bddSetVarToBeUngrouped | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Sets a variable to be ungrouped.]
Description [Sets a variable to be ungrouped. This function is used for lazy sifting. Returns 1 if successful; 0 otherwise.]
SideEffects [modifies the manager]
SeeAlso [Cudd_bddIsVarToBeUngrouped]
Definition at line 4728 of file cuddAPI.c.
Function********************************************************************
Synopsis [Builds a positional array from the BDD of a cube.]
Description [Builds a positional array from the BDD of a cube. Array must have one entry for each BDD variable. The positional array has 1 in i-th position if the variable of index i appears in true form in the cube; it has 0 in i-th position if the variable of index i appears in complemented form in the cube; finally, it has 2 in i-th position if the variable of index i does not appear in the cube. Returns 1 if successful (the BDD is indeed a cube); 0 otherwise.]
SideEffects [The result is in the array passed by reference.]
SeeAlso [Cudd_CubeArrayToBdd]
Definition at line 2354 of file cuddUtil.c.
| int Cudd_bddUnbindVar | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Allows the sifting of a variable.]
Description [This function resets the flag that prevents the sifting of a variable. In successive variable reorderings, the variable will NOT be skipped, that is, sifted. Initially all variables can be sifted. It is necessary to call this function only to re-enable sifting after a call to Cudd_bddBindVar. Returns 1 if successful; 0 otherwise (i.e., invalid variable index).]
SideEffects [Changes the "bindVar" flag in DdSubtable.]
SeeAlso [Cudd_bddBindVar]
Definition at line 4380 of file cuddAPI.c.
Function********************************************************************
Synopsis [Universally abstracts all the variables in cube from f.]
Description [Universally abstracts all the variables in cube from f. Returns the abstracted BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddExistAbstract Cudd_addUnivAbstract]
Definition at line 248 of file cuddBddAbs.c.
| int Cudd_bddVarIsBound | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Tells whether a variable can be sifted.]
Description [This function returns 1 if a variable is enabled for sifting. Initially all variables can be sifted. This function returns 0 only if there has been a previous call to Cudd_bddBindVar for that variable not followed by a call to Cudd_bddUnbindVar. The function returns 0 also in the case in which the index of the variable is out of bounds.]
SideEffects [none]
SeeAlso [Cudd_bddBindVar Cudd_bddUnbindVar]
Definition at line 4407 of file cuddAPI.c.
Function********************************************************************
Synopsis [Checks whether a variable is dependent on others in a function.]
Description [Checks whether a variable is dependent on others in a function. Returns 1 if the variable is dependent; 0 otherwise. No new nodes are created.]
SideEffects [None]
SeeAlso []
Definition at line 325 of file cuddBddAbs.c.
Function********************************************************************
Synopsis [Computes the exclusive NOR of two BDDs f and g.]
Description [Computes the exclusive NOR 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_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr Cudd_bddNand Cudd_bddNor Cudd_bddXor]
Definition at line 580 of file cuddBddIte.c.
Function********************************************************************
Synopsis [Computes the exclusive NOR of two BDDs f and g. Returns NULL if too many nodes are required.]
Description [Computes the exclusive NOR of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up or more new nodes than limit are required.]
SideEffects [None]
SeeAlso [Cudd_bddXnor]
Definition at line 612 of file cuddBddIte.c.
Function********************************************************************
Synopsis [Computes the exclusive OR of two BDDs f and g.]
Description [Computes the exclusive OR 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_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr Cudd_bddNand Cudd_bddNor Cudd_bddXnor]
Definition at line 549 of file cuddBddIte.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_bddUnivAbstract Cudd_bddExistAbstract Cudd_bddAndAbstract]
Definition at line 210 of file cuddBddAbs.c.
| DdNode* Cudd_BiasedOverApprox | ( | DdManager * | dd, |
| DdNode * | f, | ||
| DdNode * | b, | ||
| int | numVars, | ||
| int | threshold, | ||
| double | quality1, | ||
| double | quality0 | ||
| ) |
| DdNode* Cudd_BiasedUnderApprox | ( | DdManager * | dd, |
| DdNode * | f, | ||
| DdNode * | b, | ||
| int | numVars, | ||
| int | threshold, | ||
| double | quality1, | ||
| double | quality0 | ||
| ) |
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 155 of file cuddCof.c.
| int Cudd_CheckKeys | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Checks for several conditions that should not occur.]
Description [Checks for the following conditions:
Reports the average length of non-empty lists. Returns the number of subtables for which the number of keys is wrong.]
SideEffects [None]
SeeAlso [Cudd_DebugCheck]
Definition at line 460 of file cuddCheck.c.
| int Cudd_CheckZeroRef | ( | DdManager * | manager | ) |
Function********************************************************************
Synopsis [Checks the unique table for nodes with non-zero reference counts.]
Description [Checks the unique table for nodes with non-zero reference counts. It is normally called before Cudd_Quit to make sure that there are no memory leaks due to missing Cudd_RecursiveDeref's. Takes into account that reference counts may saturate and that the basic constants and the projection functions are referenced by the manager. Returns the number of nodes with non-zero reference count. (Except for the cases mentioned above.)]
SideEffects [None]
SeeAlso []
Definition at line 462 of file cuddRef.c.
| int Cudd_ClassifySupport | ( | DdManager * | dd, |
| DdNode * | f, | ||
| DdNode * | g, | ||
| DdNode ** | common, | ||
| DdNode ** | onlyF, | ||
| DdNode ** | onlyG | ||
| ) |
Function********************************************************************
Synopsis [Classifies the variables in the support of two DDs.]
Description [Classifies the variables in the support of two DDs f and g, depending on whther they appear in both DDs, only in f, or only in g. Returns 1 if successful; 0 otherwise.]
SideEffects [The cubes of the three classes of variables are returned as side effects.]
SeeAlso [Cudd_Support Cudd_VectorSupport]
Definition at line 1101 of file cuddUtil.c.
| void Cudd_ClearErrorCode | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Clear the error code of a manager.]
Description []
SideEffects [None]
SeeAlso [Cudd_ReadErrorCode]
Definition at line 4085 of file cuddAPI.c.
AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Computes the cofactor of f with respect to g.]
Description [Computes the cofactor of f with respect to g; g must be the BDD or the ADD of a cube. Returns a pointer to the cofactor if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddConstrain Cudd_bddRestrict]
Definition at line 119 of file cuddCof.c.
| int Cudd_CountLeaves | ( | DdNode * | node | ) |
Function********************************************************************
Synopsis [Counts the number of leaves in a DD.]
Description [Counts the number of leaves in a DD. Returns the number of leaves in the DD rooted at node if successful; CUDD_OUT_OF_MEM otherwise.]
SideEffects [None]
SeeAlso [Cudd_PrintDebug]
Definition at line 1202 of file cuddUtil.c.
Function********************************************************************
Synopsis [Counts the number of minterms of a DD.]
Description [Counts the number of minterms of a DD. The function is assumed to depend on nvars variables. The minterm count is represented as a double, to allow for a larger number of variables. Returns the number of minterms of the function rooted at node if successful; (double) CUDD_OUT_OF_MEM otherwise.]
SideEffects [None]
SeeAlso [Cudd_PrintDebug Cudd_CountPath]
Definition at line 582 of file cuddUtil.c.
| double Cudd_CountPath | ( | DdNode * | node | ) |
Function********************************************************************
Synopsis [Counts the number of paths of a DD.]
Description [Counts the number of paths of a DD. Paths to all terminal nodes are counted. The path count is represented as a double, to allow for a larger number of variables. Returns the number of paths of the function rooted at node if successful; (double) CUDD_OUT_OF_MEM otherwise.]
SideEffects [None]
SeeAlso [Cudd_CountMinterm]
Definition at line 627 of file cuddUtil.c.
| double Cudd_CountPathsToNonZero | ( | DdNode * | node | ) |
Function********************************************************************
Synopsis [Counts the number of paths to a non-zero terminal of a DD.]
Description [Counts the number of paths to a non-zero terminal of a DD. The path count is represented as a double, to allow for a larger number of variables. Returns the number of paths of the function rooted at node.]
SideEffects [None]
SeeAlso [Cudd_CountMinterm Cudd_CountPath]
Definition at line 711 of file cuddUtil.c.
Function********************************************************************
Synopsis [Builds the BDD of a cube from a positional array.]
Description [Builds a cube from a positional array. The array must have one integer entry for each BDD variable. If the i-th entry is 1, the variable of index i appears in true form in the cube; If the i-th entry is 0, the variable of index i appears complemented in the cube; otherwise the variable does not appear in the cube. Returns a pointer to the BDD for the cube if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddComputeCube Cudd_IndicesToCube Cudd_BddToCubeArray]
Definition at line 2306 of file cuddUtil.c.
| int Cudd_DagSize | ( | DdNode * | node | ) |
Function********************************************************************
Synopsis [Counts the number of nodes in a DD.]
Description [Counts the number of nodes in a DD. Returns the number of nodes in the graph rooted at node.]
SideEffects [None]
SeeAlso [Cudd_SharingSize Cudd_PrintDebug]
Definition at line 446 of file cuddUtil.c.
| int Cudd_DeadAreCounted | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Tells whether dead nodes are counted towards triggering reordering.]
Description [Tells whether dead nodes are counted towards triggering reordering. Returns 1 if dead nodes are counted; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_TurnOnCountDead Cudd_TurnOffCountDead]
Definition at line 2867 of file cuddAPI.c.
| int Cudd_DebugCheck | ( | DdManager * | table | ) |
AutomaticEnd Function********************************************************************
Synopsis [Checks for inconsistencies in the DD heap.]
Description [Checks for inconsistencies in the DD heap:
Returns 0 if no inconsistencies are found; DD_OUT_OF_MEM if there is not enough memory; 1 otherwise.]
SideEffects [None]
SeeAlso [Cudd_CheckKeys]
Definition at line 138 of file cuddCheck.c.
Function********************************************************************
Synopsis [Determines whether a BDD is negative unate in a variable.]
Description [Determines whether the function represented by BDD f is negative unate (monotonic decreasing) in variable i. Returns the constant one is f is unate and the (logical) constant zero if it is not. This function does not generate any new nodes.]
SideEffects [None]
SeeAlso [Cudd_Increasing]
Definition at line 424 of file cuddSat.c.
Function********************************************************************
Synopsis [Decreases the reference count of BDD node n.]
Description [Enqueues node n for later dereferencing. If the queue is full decreases the reference count of the oldest node N to make room for n. If N dies, recursively decreases the reference counts of its children. It is used to dispose of a BDD that is currently not needed, but may be useful again in the near future. The dereferencing proper is done as in Cudd_IterDerefBdd.]
SideEffects [None]
SeeAlso [Cudd_RecursiveDeref Cudd_IterDerefBdd]
Definition at line 270 of file cuddRef.c.
Function********************************************************************
Synopsis [Computes the density of a BDD or ADD.]
Description [Computes the density of a BDD or ADD. The density is the ratio of the number of minterms to the number of nodes. If 0 is passed as number of variables, the number of variables existing in the manager is used. Returns the density if successful; (double) CUDD_OUT_OF_MEM otherwise.]
SideEffects [None]
SeeAlso [Cudd_CountMinterm Cudd_DagSize]
Definition at line 2810 of file cuddUtil.c.
| void Cudd_Deref | ( | DdNode * | node | ) |
Function********************************************************************
Synopsis [Decreases the reference count of node.]
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 Cudd_Ref.]
SideEffects [None]
SeeAlso [Cudd_RecursiveDeref Cudd_RecursiveDerefZdd Cudd_Ref]
Definition at line 434 of file cuddRef.c.
| void Cudd_DisableGarbageCollection | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Disables garbage collection.]
Description [Disables garbage collection. Garbage collection is initially enabled. This function may be called to disable it. However, garbage collection will still occur when a new node must be created and no memory is left, or when garbage collection is required for correctness. (E.g., before reordering.)]
SideEffects [None]
SeeAlso [Cudd_EnableGarbageCollection Cudd_GarbageCollectionEnabled]
Definition at line 2845 of file cuddAPI.c.
| int Cudd_DisableOrderingMonitoring | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Disables monitoring of ordering.]
Description [Disables monitoring of ordering. Returns 1 if successful; 0 otherwise.]
SideEffects [Removes functions from the pre-reordering and post-reordering hooks.]
SeeAlso [Cudd_EnableOrderingMonitoring]
Definition at line 4011 of file cuddAPI.c.
| int Cudd_DisableReorderingReporting | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Disables reporting of reordering stats.]
Description [Disables reporting of reordering stats. Returns 1 if successful; 0 otherwise.]
SideEffects [Removes functions from the pre-reordering and post-reordering hooks.]
SeeAlso [Cudd_EnableReorderingReporting Cudd_ReorderingReporting]
Definition at line 3889 of file cuddAPI.c.
| int Cudd_DumpBlif | ( | DdManager * | dd, |
| int | n, | ||
| DdNode ** | f, | ||
| char ** | inames, | ||
| char ** | onames, | ||
| char * | mname, | ||
| FILE * | fp, | ||
| int | mv | ||
| ) |
| int Cudd_DumpBlifBody | ( | DdManager * | dd, |
| int | n, | ||
| DdNode ** | f, | ||
| char ** | inames, | ||
| char ** | onames, | ||
| FILE * | fp, | ||
| int | mv | ||
| ) |
| int Cudd_DumpDaVinci | ( | DdManager * | dd, |
| int | n, | ||
| DdNode ** | f, | ||
| char ** | inames, | ||
| char ** | onames, | ||
| FILE * | fp | ||
| ) |
| int Cudd_DumpDDcal | ( | DdManager * | dd, |
| int | n, | ||
| DdNode ** | f, | ||
| char ** | inames, | ||
| char ** | onames, | ||
| FILE * | fp | ||
| ) |
| int Cudd_DumpFactoredForm | ( | DdManager * | dd, |
| int | n, | ||
| DdNode ** | f, | ||
| char ** | inames, | ||
| char ** | onames, | ||
| FILE * | fp | ||
| ) |
| void Cudd_EnableGarbageCollection | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Enables garbage collection.]
Description [Enables garbage collection. Garbage collection is initially enabled. Therefore it is necessary to call this function only if garbage collection has been explicitly disabled.]
SideEffects [None]
SeeAlso [Cudd_DisableGarbageCollection Cudd_GarbageCollectionEnabled]
Definition at line 2821 of file cuddAPI.c.
| int Cudd_EnableOrderingMonitoring | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Enables monitoring of ordering.]
Description [Enables monitoring of ordering. Returns 1 if successful; 0 otherwise.]
SideEffects [Installs functions in the pre-reordering and post-reordering hooks.]
SeeAlso [Cudd_EnableReorderingReporting]
Definition at line 3977 of file cuddAPI.c.
| int Cudd_EnableReorderingReporting | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Enables reporting of reordering stats.]
Description [Enables reporting of reordering stats. Returns 1 if successful; 0 otherwise.]
SideEffects [Installs functions in the pre-reordering and post-reordering hooks.]
SeeAlso [Cudd_DisableReorderingReporting Cudd_ReorderingReporting]
Definition at line 3861 of file cuddAPI.c.
Function********************************************************************
Synopsis [Counts the number of minterms of a DD with extended precision.]
Description [Counts the number of minterms of a DD with extended precision. The function is assumed to depend on nvars variables. The minterm count is represented as an EpDouble, to allow any number of variables. Returns 0 if successful; CUDD_OUT_OF_MEM otherwise.]
SideEffects [None]
SeeAlso [Cudd_PrintDebug Cudd_CountPath]
Definition at line 661 of file cuddUtil.c.
| int Cudd_EqualSupNorm | ( | DdManager * | dd, |
| DdNode * | f, | ||
| DdNode * | g, | ||
| CUDD_VALUE_TYPE | tolerance, | ||
| int | pr | ||
| ) |
Function********************************************************************
Synopsis [Compares two ADDs for equality within tolerance.]
Description [Compares two ADDs for equality within tolerance. Two ADDs are reported to be equal if the maximum difference between them (the sup norm of their difference) is less than or equal to the tolerance parameter. Returns 1 if the two ADDs are equal (within tolerance); 0 otherwise. If parameter pr is positive the first failure is reported to the standard output.]
SideEffects [None]
SeeAlso []
Definition at line 803 of file cuddSat.c.
Function********************************************************************
Synopsis [Tells whether F and G are identical wherever D is 0.]
Description [Tells whether F and G are identical wherever D is 0. F and G are either two ADDs or two BDDs. D is either a 0-1 ADD or a BDD. The function returns 1 if F and G are equivalent, and 0 otherwise. No new nodes are created.]
SideEffects [None]
SeeAlso [Cudd_bddLeqUnless]
Definition at line 529 of file cuddSat.c.
Function********************************************************************
Synopsis [Estimates the number of nodes in a cofactor of a DD.]
Description [Estimates the number of nodes in a cofactor of a DD. Returns an estimate of the number of nodes in a cofactor of the graph rooted at node with respect to the variable whose index is i. In case of failure, returns CUDD_OUT_OF_MEM. This function uses a refinement of the algorithm of Cabodi et al. (ICCAD96). The refinement allows the procedure to account for part of the recombination that may occur in the part of the cofactor above the cofactoring variable. This procedure does not create any new node. It does keep a small table of results; therefore it may run out of memory. If this is a concern, one should use Cudd_EstimateCofactorSimple, which is faster, does not allocate any memory, but is less accurate.]
SideEffects [None]
SeeAlso [Cudd_DagSize Cudd_EstimateCofactorSimple]
Definition at line 481 of file cuddUtil.c.
| int Cudd_EstimateCofactorSimple | ( | DdNode * | node, |
| int | i | ||
| ) |
Function********************************************************************
Synopsis [Estimates the number of nodes in a cofactor of a DD.]
Description [Estimates the number of nodes in a cofactor of a DD. Returns an estimate of the number of nodes in the positive cofactor of the graph rooted at node with respect to the variable whose index is i. This procedure implements with minor changes the algorithm of Cabodi et al. (ICCAD96). It does not allocate any memory, it does not change the state of the manager, and it is fast. However, it has been observed to overestimate the size of the cofactor by as much as a factor of 2.]
SideEffects [None]
SeeAlso [Cudd_DagSize]
Definition at line 521 of file cuddUtil.c.
AutomaticEnd Function********************************************************************
Synopsis [Returns the value of a DD for a given variable assignment.]
Description [Finds the value of a DD for a given variable assignment. The variable assignment is passed in an array of int's, that should specify a zero or a one for each variable in the support of the function. Returns a pointer to a constant node. No new nodes are produced.]
SideEffects [None]
SeeAlso [Cudd_bddLeq Cudd_addEvalConst]
Definition at line 159 of file cuddSat.c.
| double Cudd_ExpectedUsedSlots | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Computes the expected fraction of used slots in the unique table.]
Description [Computes the fraction of slots in the unique table that should be in use. This expected value is based on the assumption that the hash function distributes the keys randomly; it can be compared with the result of Cudd_ReadUsedSlots to monitor the performance of the unique table hash function.]
SideEffects [None]
SeeAlso [Cudd_ReadSlots Cudd_ReadUsedSlots]
Definition at line 1812 of file cuddAPI.c.
| DdGen* Cudd_FirstCube | ( | DdManager * | dd, |
| DdNode * | f, | ||
| int ** | cube, | ||
| CUDD_VALUE_TYPE * | value | ||
| ) |
Function********************************************************************
Synopsis [Finds the first cube of a decision diagram.]
Description [Defines an iterator on the onset of a decision diagram and finds its first cube. Returns a generator that contains the information necessary to continue the enumeration if successful; NULL otherwise.
A cube is represented as an array of literals, which are integers in {0, 1, 2}; 0 represents a complemented literal, 1 represents an uncomplemented literal, and 2 stands for don't care. The enumeration produces a disjoint cover of the function associated with the diagram. The size of the array equals the number of variables in the manager at the time Cudd_FirstCube is called.
For each cube, a value is also returned. This value is always 1 for a BDD, while it may be different from 1 for an ADD. For BDDs, the offset is the set of cubes whose value is the logical zero. For ADDs, the offset is the set of cubes whose value is the background value. The cubes of the offset are not enumerated.]
SideEffects [The first cube and its value are returned as side effects.]
SeeAlso [Cudd_ForeachCube Cudd_NextCube Cudd_GenFree Cudd_IsGenEmpty Cudd_FirstNode]
Definition at line 1806 of file cuddUtil.c.
Function********************************************************************
Synopsis [Finds the first node of a decision diagram.]
Description [Defines an iterator on the nodes of a decision diagram and finds its first node. Returns a generator that contains the information necessary to continue the enumeration if successful; NULL otherwise. The nodes are enumerated in a reverse topological order, so that a node is always preceded in the enumeration by its descendants.]
SideEffects [The first node is returned as a side effect.]
SeeAlso [Cudd_ForeachNode Cudd_NextNode Cudd_GenFree Cudd_IsGenEmpty Cudd_FirstCube]
Definition at line 2408 of file cuddUtil.c.
Function********************************************************************
Synopsis [Finds the first prime of a Boolean function.]
Description [Defines an iterator on a pair of BDDs describing a (possibly incompletely specified) Boolean functions and finds the first cube of a cover of the function. Returns a generator that contains the information necessary to continue the enumeration if successful; NULL otherwise.
The two argument BDDs are the lower and upper bounds of an interval. It is a mistake to call this function with a lower bound that is not less than or equal to the upper bound.
A cube is represented as an array of literals, which are integers in {0, 1, 2}; 0 represents a complemented literal, 1 represents an uncomplemented literal, and 2 stands for don't care. The enumeration produces a prime and irredundant cover of the function associated with the two BDDs. The size of the array equals the number of variables in the manager at the time Cudd_FirstCube is called.
This iterator can only be used on BDDs.]
SideEffects [The first cube is returned as side effect.]
SeeAlso [Cudd_ForeachPrime Cudd_NextPrime Cudd_GenFree Cudd_IsGenEmpty Cudd_FirstCube Cudd_FirstNode]
Definition at line 2036 of file cuddUtil.c.
| void Cudd_FreeTree | ( | DdManager * | dd | ) |
| void Cudd_FreeZddTree | ( | DdManager * | dd | ) |
| int Cudd_GarbageCollectionEnabled | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Tells whether garbage collection is enabled.]
Description [Returns 1 if garbage collection is enabled; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_EnableGarbageCollection Cudd_DisableGarbageCollection]
Definition at line 2799 of file cuddAPI.c.
| int Cudd_GenFree | ( | DdGen * | gen | ) |
Function********************************************************************
Synopsis [Frees a CUDD generator.]
Description [Frees a CUDD generator. Always returns 0, so that it can be used in mis-like foreach constructs.]
SideEffects [None]
SeeAlso [Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube Cudd_FirstNode Cudd_NextNode Cudd_IsGenEmpty]
Definition at line 2499 of file cuddUtil.c.
| void Cudd_IncreaseTimeLimit | ( | DdManager * | unique, |
| unsigned long | increase | ||
| ) |
Function********************************************************************
Synopsis [Increases the time limit for the manager.]
Description [Increases the time limit for the manager.]
SideEffects [None]
SeeAlso [Cudd_ReadTimeLimit Cudd_SetTimeLimit Cudd_UnsetTimeLimit Cudd_UpdateTimeLimit Cudd_TimeLimited Cudd_SetStartTime]
Definition at line 838 of file cuddAPI.c.
Function********************************************************************
Synopsis [Determines whether a BDD is positive unate in a variable.]
Description [Determines whether the function represented by BDD f is positive unate (monotonic increasing) in variable i. It is based on Cudd_Decreasing and the fact that f is monotonic increasing in i if and only if its complement is monotonic decreasing in i.]
SideEffects [None]
SeeAlso [Cudd_Decreasing]
Definition at line 504 of file cuddSat.c.
Function********************************************************************
Synopsis [Builds a cube of BDD variables from an array of indices.]
Description [Builds a cube of BDD variables from an array of indices. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddComputeCube Cudd_CubeArrayToBdd]
Definition at line 2561 of file cuddUtil.c.
| DdManager* Cudd_Init | ( | unsigned int | numVars, |
| unsigned int | numVarsZ, | ||
| unsigned int | numSlots, | ||
| unsigned int | cacheSize, | ||
| unsigned long | maxMemory | ||
| ) |
AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Creates a new DD manager.]
Description [Creates a new DD manager, initializes the table, the basic constants and the projection functions. If maxMemory is 0, Cudd_Init decides suitable values for the maximum size of the cache and for the limit for fast unique table growth based on the available memory. Returns a pointer to the manager if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_Quit]
Definition at line 121 of file cuddInit.c.
| int Cudd_IsGenEmpty | ( | DdGen * | gen | ) |
Function********************************************************************
Synopsis [Queries the status of a generator.]
Description [Queries the status of a generator. Returns 1 if the generator is empty or NULL; 0 otherswise.]
SideEffects [None]
SeeAlso [Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube Cudd_FirstNode Cudd_NextNode Cudd_GenFree]
Definition at line 2539 of file cuddUtil.c.
| int Cudd_IsInHook | ( | DdManager * | dd, |
| DD_HFP | f, | ||
| Cudd_HookType | where | ||
| ) |
Function********************************************************************
Synopsis [Checks whether a function is in a hook.]
Description [Checks whether a function is in a hook. A hook is a list of application-provided functions called on certain occasions by the package. Returns 1 if the function is found; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_AddHook Cudd_RemoveHook]
Definition at line 3684 of file cuddAPI.c.
| int Cudd_IsNonConstant | ( | DdNode * | f | ) |
Function********************************************************************
Synopsis [Returns 1 if a DD node is not constant.]
Description [Returns 1 if a DD node is not constant. This function is useful to test the results of Cudd_bddIteConstant, Cudd_addIteConstant, Cudd_addEvalConst. These results may be a special value signifying non-constant. In the other cases the macro Cudd_IsConstant can be used.]
SideEffects [None]
SeeAlso [Cudd_IsConstant Cudd_bddIteConstant Cudd_addIteConstant Cudd_addEvalConst]
Definition at line 659 of file cuddAPI.c.
Function********************************************************************
Synopsis [Decreases the reference count of BDD node n.]
Description [Decreases the reference count of node n. If n dies, recursively decreases the reference counts of its children. It is used to dispose of a BDD that is no longer needed. It is more efficient than Cudd_RecursiveDeref, but it cannot be used on ADDs. The greater efficiency comes from being able to assume that no constant node will ever die as a result of a call to this procedure.]
SideEffects [None]
SeeAlso [Cudd_RecursiveDeref Cudd_DelayedDerefBdd]
Definition at line 213 of file cuddRef.c.
Function********************************************************************
Synopsis [Finds a largest cube in a DD.]
Description [Finds a largest cube in a DD. f is the DD we want to get the largest cube for. The problem is translated into the one of finding a shortest path in f, when both THEN and ELSE arcs are assumed to have unit length. This yields a largest cube in the disjoint cover corresponding to the DD. Therefore, it is not necessarily the largest implicant of f. Returns the largest cube as a BDD.]
SideEffects [The number of literals of the cube is returned in the location pointed by length if it is non-null.]
SeeAlso [Cudd_ShortestPath]
Definition at line 288 of file cuddSat.c.
Function********************************************************************
Synopsis [Converts a ZDD cover to a BDD.]
Description [Converts a ZDD cover to a BDD for the function represented by the cover. If successful, it returns a BDD node, otherwise it returns NULL.]
SideEffects []
SeeAlso [Cudd_zddIsop]
Definition at line 200 of file cuddZddIsop.c.
| MtrNode* Cudd_MakeTreeNode | ( | DdManager * | dd, |
| unsigned int | low, | ||
| unsigned int | size, | ||
| unsigned int | type | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Creates a new variable group.]
Description [Creates a new variable group. The group starts at variable low and contains size variables. The parameter low is the index of the first variable. If the variable already exists, its current position in the order is known to the manager. If the variable does not exist yet, the position is assumed to be the same as the index. The group tree is created if it does not exist yet. Returns a pointer to the group if successful; NULL otherwise.]
SideEffects [The variable tree is changed.]
SeeAlso [Cudd_MakeZddTreeNode]
Definition at line 203 of file cuddGroup.c.
| MtrNode* Cudd_MakeZddTreeNode | ( | DdManager * | dd, |
| unsigned int | low, | ||
| unsigned int | size, | ||
| unsigned int | type | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Creates a new ZDD variable group.]
Description [Creates a new ZDD variable group. The group starts at variable and contains size variables. The parameter low is the index of the first variable. If the variable already exists, its current position in the order is known to the manager. If the variable does not exist yet, the position is assumed to be the same as the index. The group tree is created if it does not exist yet. Returns a pointer to the group if successful; NULL otherwise.]
SideEffects [The ZDD variable tree is changed.]
SeeAlso [Cudd_MakeTreeNode]
Definition at line 159 of file cuddZddGroup.c.
| DdApaNumber Cudd_NewApaNumber | ( | int | digits | ) |
| int Cudd_NextCube | ( | DdGen * | gen, |
| int ** | cube, | ||
| CUDD_VALUE_TYPE * | value | ||
| ) |
Function********************************************************************
Synopsis [Generates the next cube of a decision diagram onset.]
Description [Generates the next cube of a decision diagram onset, using generator gen. Returns 0 if the enumeration is completed; 1 otherwise.]
SideEffects [The cube and its value are returned as side effects. The generator is modified.]
SeeAlso [Cudd_ForeachCube Cudd_FirstCube Cudd_GenFree Cudd_IsGenEmpty Cudd_NextNode]
Definition at line 1925 of file cuddUtil.c.
Function********************************************************************
Synopsis [Finds the next node of a decision diagram.]
Description [Finds the node of a decision diagram, using generator gen. Returns 0 if the enumeration is completed; 1 otherwise.]
SideEffects [The next node is returned as a side effect.]
SeeAlso [Cudd_ForeachNode Cudd_FirstNode Cudd_GenFree Cudd_IsGenEmpty Cudd_NextCube]
Definition at line 2467 of file cuddUtil.c.
| int Cudd_NextPrime | ( | DdGen * | gen, |
| int ** | cube | ||
| ) |
Function********************************************************************
Synopsis [Generates the next prime of a Boolean function.]
Description [Generates the next cube of a Boolean function, using generator gen. Returns 0 if the enumeration is completed; 1 otherwise.]
SideEffects [The cube and is returned as side effects. The generator is modified.]
SeeAlso [Cudd_ForeachPrime Cudd_FirstPrime Cudd_GenFree Cudd_IsGenEmpty Cudd_NextCube Cudd_NextNode]
Definition at line 2138 of file cuddUtil.c.
| unsigned int Cudd_NodeReadIndex | ( | DdNode * | node | ) |
Function********************************************************************
Synopsis [Returns the index of the node.]
Description [Returns the index of the node. The node pointer can be either regular or complemented.]
SideEffects [None]
SeeAlso [Cudd_ReadIndex]
Definition at line 2559 of file cuddAPI.c.
| int Cudd_OrderingMonitoring | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns 1 if monitoring of ordering is enabled.]
Description [Returns 1 if monitoring of ordering is enabled; 0 otherwise.]
SideEffects [none]
SeeAlso [Cudd_EnableOrderingMonitoring Cudd_DisableOrderingMonitoring]
Definition at line 4044 of file cuddAPI.c.
| void Cudd_OutOfMem | ( | long | size | ) |
Function********************************************************************
Synopsis [Warns that a memory allocation failed.]
Description [Warns that a memory allocation failed. This function can be used as replacement of MMout_of_memory to prevent the safe_mem functions of the util package from exiting when malloc returns NULL. One possible use is in case of discretionary allocations; for instance, the allocation of memory to enlarge the computed table.]
SideEffects [None]
SeeAlso []
Definition at line 2845 of file cuddUtil.c.
| DdNode* Cudd_OverApprox | ( | DdManager * | dd, |
| DdNode * | f, | ||
| int | numVars, | ||
| int | threshold, | ||
| int | safe, | ||
| double | quality | ||
| ) |
| unsigned int Cudd_Prime | ( | unsigned int | p | ) |
AutomaticEnd Function********************************************************************
Synopsis [Returns the next prime >= p.]
Description []
SideEffects [None]
Definition at line 185 of file cuddTable.c.
Function********************************************************************
Synopsis [Prints to the standard output a DD and its statistics.]
Description [Prints to the standard output a DD and its statistics. The statistics include the number of nodes, the number of leaves, and the number of minterms. (The number of minterms is the number of assignments to the variables that cause the function to be different from the logical zero (for BDDs) and from the background value (for ADDs.) The statistics are printed if pr > 0. Specifically:
For the purpose of counting the number of minterms, the function is supposed to depend on n variables. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_DagSize Cudd_CountLeaves Cudd_CountMinterm Cudd_PrintMinterm]
Definition at line 386 of file cuddUtil.c.
| int Cudd_PrintGroupedOrder | ( | DdManager * | dd, |
| const char * | str, | ||
| void * | data | ||
| ) |
Function********************************************************************
Synopsis [Hook function to print the current variable order.]
Description [Hook function to print the current variable order. It may be called before or after reordering. Prints on the manager's stdout a parenthesized list that describes the variable groups. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_StdPreReordHook]
Definition at line 3939 of file cuddAPI.c.
| int Cudd_PrintInfo | ( | DdManager * | dd, |
| FILE * | fp | ||
| ) |
Function********************************************************************
Synopsis [Prints out statistics and settings for a CUDD manager.]
Description [Prints out statistics and settings for a CUDD manager. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 3263 of file cuddAPI.c.
| int Cudd_PrintLinear | ( | DdManager * | table | ) |
AutomaticEnd Function********************************************************************
Synopsis [Prints the linear transform matrix.]
Description [Prints the linear transform matrix. Returns 1 in case of success; 0 otherwise.]
SideEffects [none]
SeeAlso []
Definition at line 149 of file cuddLinear.c.
AutomaticEnd Function********************************************************************
Synopsis [Prints a disjoint sum of products.]
Description [Prints a disjoint sum of product cover for the function rooted at node. Each product corresponds to a path from node to a leaf node different from the logical zero, and different from the background value. Uses the package default output file. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_PrintDebug Cudd_bddPrintCover]
Definition at line 220 of file cuddUtil.c.
| void Cudd_PrintVersion | ( | FILE * | fp | ) |
Function********************************************************************
Synopsis [Prints the package version number.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 2600 of file cuddUtil.c.
| DdNode* Cudd_PrioritySelect | ( | DdManager * | dd, |
| DdNode * | R, | ||
| DdNode ** | x, | ||
| DdNode ** | y, | ||
| DdNode ** | z, | ||
| DdNode * | Pi, | ||
| int | n, | ||
| DdNode * | *)(DdManager *, int, DdNode **, DdNode **, DdNode ** | ||
| ) |
| void Cudd_Quit | ( | DdManager * | unique | ) |
Function********************************************************************
Synopsis [Deletes resources associated with a DD manager.]
Description [Deletes resources associated with a DD manager and resets the global statistical counters. (Otherwise, another manaqger subsequently created would inherit the stats of this one.)]
SideEffects [None]
SeeAlso [Cudd_Init]
Definition at line 218 of file cuddInit.c.
| long Cudd_Random | ( | void | ) |
Function********************************************************************
Synopsis [Portable random number generator.]
Description [Portable number generator based on ran2 from "Numerical Recipes in C." It is a long period (> 2 * 10^18) random number generator of L'Ecuyer with Bays-Durham shuffle. Returns a long integer uniformly distributed between 0 and 2147483561 (inclusive of the endpoint values). The random generator can be explicitly initialized by calling Cudd_Srandom. If no explicit initialization is performed, then the seed 1 is assumed.]
SideEffects [None]
SeeAlso [Cudd_Srandom]
Definition at line 2710 of file cuddUtil.c.
| int Cudd_ReadArcviolation | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the current value of the arcviolation parameter used in group sifting.]
Description [Returns the current value of the arcviolation parameter. This parameter is used in group sifting to decide how many arcs into y not coming from x are tolerable when checking for aggregation due to extended symmetry. The value should be between 0 and 100. A small value causes fewer variables to be aggregated. The default value is 0.]
SideEffects [None]
SeeAlso [Cudd_SetArcviolation]
Definition at line 3046 of file cuddAPI.c.
| double Cudd_ReadCacheHits | ( | DdManager * | dd | ) |
| double Cudd_ReadCacheLookUps | ( | DdManager * | dd | ) |
| unsigned int Cudd_ReadCacheSlots | ( | DdManager * | dd | ) |
| double Cudd_ReadCacheUsedSlots | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reads the fraction of used slots in the cache.]
Description [Reads the fraction of used slots in the cache. The unused slots are those in which no valid data is stored. Garbage collection, variable reordering, and cache resizing may cause used slots to become unused.]
SideEffects [None]
SeeAlso [Cudd_ReadCacheSlots]
Definition at line 1415 of file cuddAPI.c.
| unsigned int Cudd_ReadDead | ( | DdManager * | dd | ) |
| unsigned long Cudd_ReadElapsedTime | ( | DdManager * | unique | ) |
Function********************************************************************
Synopsis [Returns the time elapsed since the start time of the manager.]
Description [Returns the time elapsed since the start time of the manager.]
SideEffects [None]
SeeAlso [Cudd_ReadStartTime Cudd_SetStartTime]
Definition at line 701 of file cuddAPI.c.
| CUDD_VALUE_TYPE Cudd_ReadEpsilon | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reads the epsilon parameter of the manager.]
Description [Reads the epsilon parameter of the manager. The epsilon parameter control the comparison between floating point numbers.]
SideEffects [None]
SeeAlso [Cudd_SetEpsilon]
Definition at line 2712 of file cuddAPI.c.
| Cudd_ErrorType Cudd_ReadErrorCode | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the code of the last error.]
Description [Returns the code of the last error. The error codes are defined in cudd.h.]
SideEffects [None]
SeeAlso [Cudd_ClearErrorCode]
Definition at line 4065 of file cuddAPI.c.
| int Cudd_ReadGarbageCollections | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the number of times garbage collection has occurred.]
Description [Returns the number of times garbage collection has occurred in the manager. The number includes both the calls from reordering procedures and those caused by requests to create new nodes.]
SideEffects [None]
SeeAlso [Cudd_ReadGarbageCollectionTime]
Definition at line 2023 of file cuddAPI.c.
| long Cudd_ReadGarbageCollectionTime | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the time spent in garbage collection.]
Description [Returns the number of milliseconds spent doing garbage collection since the manager was initialized.]
SideEffects [None]
SeeAlso [Cudd_ReadGarbageCollections]
Definition at line 2044 of file cuddAPI.c.
| Cudd_AggregationType Cudd_ReadGroupcheck | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reads the groupcheck parameter of the manager.]
Description [Reads the groupcheck parameter of the manager. The groupcheck parameter determines the aggregation criterion in group sifting.]
SideEffects [None]
SeeAlso [Cudd_SetGroupcheck]
Definition at line 2756 of file cuddAPI.c.
| int Cudd_ReadInvPerm | ( | DdManager * | dd, |
| int | i | ||
| ) |
Function********************************************************************
Synopsis [Returns the index of the variable currently in the i-th position of the order.]
Description [Returns the index of the variable currently in the i-th position of the order. If the index is CUDD_CONST_INDEX, returns CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.]
SideEffects [None]
SeeAlso [Cudd_ReadPerm Cudd_ReadInvPermZdd]
Definition at line 2636 of file cuddAPI.c.
| int Cudd_ReadInvPermZdd | ( | DdManager * | dd, |
| int | i | ||
| ) |
Function********************************************************************
Synopsis [Returns the index of the ZDD variable currently in the i-th position of the order.]
Description [Returns the index of the ZDD variable currently in the i-th position of the order. If the index is CUDD_CONST_INDEX, returns CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.]
SideEffects [None]
SeeAlso [Cudd_ReadPerm Cudd_ReadInvPermZdd]
Definition at line 2662 of file cuddAPI.c.
| int Cudd_ReadIthClause | ( | DdTlcInfo * | tlc, |
| int | i, | ||
| DdHalfWord * | var1, | ||
| DdHalfWord * | var2, | ||
| int * | phase1, | ||
| int * | phase2 | ||
| ) |
| unsigned int Cudd_ReadKeys | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the number of nodes in the unique table.]
Description [Returns the total number of nodes currently in the unique table, including the dead nodes.]
SideEffects [None]
SeeAlso [Cudd_ReadDead]
Definition at line 1866 of file cuddAPI.c.
| int Cudd_ReadLinear | ( | DdManager * | table, |
| int | x, | ||
| int | y | ||
| ) |
Function********************************************************************
Synopsis [Reads an entry of the linear transform matrix.]
Description [Reads an entry of the linear transform matrix.]
SideEffects [none]
SeeAlso []
Definition at line 187 of file cuddLinear.c.
Function********************************************************************
Synopsis [Returns the logic zero constant of the manager.]
Description [Returns the zero constant of the manager. The logic zero constant is the complement of the one constant, and is distinct from the arithmetic zero.]
SideEffects [None]
SeeAlso [Cudd_ReadOne Cudd_ReadZero]
Definition at line 1298 of file cuddAPI.c.
| unsigned int Cudd_ReadLooseUpTo | ( | DdManager * | dd | ) |
| unsigned int Cudd_ReadMaxCache | ( | DdManager * | dd | ) |
| unsigned int Cudd_ReadMaxCacheHard | ( | DdManager * | dd | ) |
| double Cudd_ReadMaxGrowth | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reads the maxGrowth parameter of the manager.]
Description [Reads the maxGrowth parameter of the manager. This parameter determines how much the number of nodes can grow during sifting of a variable. Overall, sifting never increases the size of the decision diagrams. This parameter only refers to intermediate results. A lower value will speed up sifting, possibly at the expense of quality.]
SideEffects [None]
SeeAlso [Cudd_SetMaxGrowth Cudd_ReadMaxGrowthAlternate]
Definition at line 2270 of file cuddAPI.c.
| double Cudd_ReadMaxGrowthAlternate | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reads the maxGrowthAlt parameter of the manager.]
Description [Reads the maxGrowthAlt parameter of the manager. This parameter is analogous to the maxGrowth paramter, and is used every given number of reorderings instead of maxGrowth. The number of reorderings is set with Cudd_SetReorderingCycle. If the number of reorderings is 0 (default) maxGrowthAlt is never used.]
SideEffects [None]
SeeAlso [Cudd_ReadMaxGrowth Cudd_SetMaxGrowthAlternate Cudd_SetReorderingCycle Cudd_ReadReorderingCycle]
Definition at line 2321 of file cuddAPI.c.
| unsigned int Cudd_ReadMaxLive | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reads the maximum allowed number of live nodes.]
Description [Reads the maximum allowed number of live nodes. When this number is exceeded, the package returns NULL.]
SideEffects [none]
SeeAlso [Cudd_SetMaxLive]
Definition at line 4265 of file cuddAPI.c.
| unsigned long Cudd_ReadMaxMemory | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reads the maximum allowed memory.]
Description [Reads the maximum allowed memory. When this number is exceeded, the package returns NULL.]
SideEffects [none]
SeeAlso [Cudd_SetMaxMemory]
Definition at line 4308 of file cuddAPI.c.
| unsigned int Cudd_ReadMaxReorderings | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the maximum number of times reordering may be invoked.]
Description [Returns the maximum number of times reordering may be invoked in this manager.]
SideEffects [None]
SeeAlso [Cudd_ReadReorderings Cudd_SetMaxReorderings Cudd_ReduceHeap]
Definition at line 1957 of file cuddAPI.c.
| unsigned long Cudd_ReadMemoryInUse | ( | DdManager * | dd | ) |
| unsigned int Cudd_ReadMinDead | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reads the minDead parameter of the manager.]
Description [Reads the minDead parameter of the manager. The minDead parameter is used by the package to decide whether to collect garbage or resize a subtable of the unique table when the subtable becomes too full. The application can indirectly control the value of minDead by setting the looseUpTo parameter.]
SideEffects [None]
SeeAlso [Cudd_ReadDead Cudd_ReadLooseUpTo Cudd_SetLooseUpTo]
Definition at line 1910 of file cuddAPI.c.
| unsigned int Cudd_ReadMinHit | ( | DdManager * | dd | ) |
| unsigned int Cudd_ReadNextReordering | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the threshold for the next dynamic reordering.]
Description [Returns the threshold for the next dynamic reordering. The threshold is in terms of number of nodes and is in effect only if reordering is enabled. The count does not include the dead nodes, unless the countDead parameter of the manager has been changed from its default setting.]
SideEffects [None]
SeeAlso [Cudd_SetNextReordering]
Definition at line 4195 of file cuddAPI.c.
| long Cudd_ReadNodeCount | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reports the number of nodes in BDDs and ADDs.]
Description [Reports the number of live nodes in BDDs and ADDs. This number does not include the isolated projection functions and the unused constants. These nodes that are not counted are not part of the DDs manipulated by the application.]
SideEffects [None]
SeeAlso [Cudd_ReadPeakNodeCount Cudd_zddReadNodeCount]
Definition at line 3504 of file cuddAPI.c.
| double Cudd_ReadNodesDropped | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the number of nodes dropped.]
Description [Returns the number of nodes killed by dereferencing if the keeping of this statistic is enabled; -1 otherwise. This statistic is enabled only if the package is compiled with DD_STATS defined.]
SideEffects [None]
SeeAlso [Cudd_ReadNodesFreed]
| double Cudd_ReadNodesFreed | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the number of nodes freed.]
Description [Returns the number of nodes returned to the free list if the keeping of this statistic is enabled; -1 otherwise. This statistic is enabled only if the package is compiled with DD_STATS defined.]
SideEffects [None]
SeeAlso [Cudd_ReadNodesDropped]
| int Cudd_ReadNumberXovers | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reads the current number of crossovers used by the genetic algorithm for reordering.]
Description [Reads the current number of crossovers used by the genetic algorithm for variable reordering. A larger number of crossovers will cause the genetic algorithm to take more time, but will generally produce better results. The default value is 0, in which case the package uses three times the number of variables as number of crossovers, with a maximum of 60.]
SideEffects [None]
SeeAlso [Cudd_SetNumberXovers]
Definition at line 3152 of file cuddAPI.c.
Function********************************************************************
Synopsis [Returns the one constant of the manager.]
Description [Returns the one constant of the manager. The one constant is common to ADDs and BDDs.]
SideEffects [None]
SeeAlso [Cudd_ReadZero Cudd_ReadLogicZero Cudd_ReadZddOne]
Definition at line 1227 of file cuddAPI.c.
| unsigned int Cudd_ReadOrderRandomization | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the order randomization factor.]
Description [Returns the order randomization factor. If non-zero this factor is used to determine a perturbation of the next reordering threshold. Larger factors cause larger perturbations.]
SideEffects [None]
SeeAlso [Cudd_SetOrderRandomization]
Definition at line 3201 of file cuddAPI.c.
| int Cudd_ReadPeakLiveNodeCount | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reports the peak number of live nodes.]
Description [Reports the peak number of live nodes.]
SideEffects [None]
SeeAlso [Cudd_ReadNodeCount Cudd_PrintInfo Cudd_ReadPeakNodeCount]
Definition at line 3476 of file cuddAPI.c.
| long Cudd_ReadPeakNodeCount | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reports the peak number of nodes.]
Description [Reports the peak number of nodes. This number includes node on the free list. At the peak, the number of nodes on the free list is guaranteed to be less than DD_MEM_CHUNK.]
SideEffects [None]
SeeAlso [Cudd_ReadNodeCount Cudd_PrintInfo]
Definition at line 3449 of file cuddAPI.c.
| int Cudd_ReadPerm | ( | DdManager * | dd, |
| int | i | ||
| ) |
Function********************************************************************
Synopsis [Returns the current position of the i-th variable in the order.]
Description [Returns the current position of the i-th variable in the order. If the index is CUDD_CONST_INDEX, returns CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.]
SideEffects [None]
SeeAlso [Cudd_ReadInvPerm Cudd_ReadPermZdd]
Definition at line 2583 of file cuddAPI.c.
| int Cudd_ReadPermZdd | ( | DdManager * | dd, |
| int | i | ||
| ) |
Function********************************************************************
Synopsis [Returns the current position of the i-th ZDD variable in the order.]
Description [Returns the current position of the i-th ZDD variable in the order. If the index is CUDD_CONST_INDEX, returns CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.]
SideEffects [None]
SeeAlso [Cudd_ReadInvPermZdd Cudd_ReadPerm]
Definition at line 2610 of file cuddAPI.c.
| int Cudd_ReadPopulationSize | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reads the current size of the population used by the genetic algorithm for reordering.]
Description [Reads the current size of the population used by the genetic algorithm for variable reordering. A larger population size will cause the genetic algorithm to take more time, but will generally produce better results. The default value is 0, in which case the package uses three times the number of variables as population size, with a maximum of 120.]
SideEffects [None]
SeeAlso [Cudd_SetPopulationSize]
Definition at line 3099 of file cuddAPI.c.
| int Cudd_ReadRecomb | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the current value of the recombination parameter used in group sifting.]
Description [Returns the current value of the recombination parameter used in group sifting. A larger (positive) value makes the aggregation of variables due to the second difference criterion more likely. A smaller (negative) value makes aggregation less likely.]
SideEffects [None]
SeeAlso [Cudd_SetRecomb]
Definition at line 2939 of file cuddAPI.c.
| double Cudd_ReadRecursiveCalls | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the number of recursive calls.]
Description [Returns the number of recursive calls if the package is compiled with DD_COUNT defined.]
SideEffects [None]
SeeAlso []
| int Cudd_ReadReorderingCycle | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reads the reordCycle parameter of the manager.]
Description [Reads the reordCycle parameter of the manager. This parameter determines how often the alternate threshold on maximum growth is used in reordering.]
SideEffects [None]
SeeAlso [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowthAlternate Cudd_SetReorderingCycle]
Definition at line 2370 of file cuddAPI.c.
| unsigned int Cudd_ReadReorderings | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the number of times reordering has occurred.]
Description [Returns the number of times reordering has occurred in the manager. The number includes both the calls to Cudd_ReduceHeap from the application program and those automatically performed by the package. However, calls that do not even initiate reordering are not counted. A call may not initiate reordering if there are fewer than minsize live nodes in the manager, or if CUDD_REORDER_NONE is specified as reordering method. The calls to Cudd_ShuffleHeap are not counted.]
SideEffects [None]
SeeAlso [Cudd_ReduceHeap Cudd_ReadReorderingTime]
Definition at line 1936 of file cuddAPI.c.
| long Cudd_ReadReorderingTime | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the time spent in reordering.]
Description [Returns the number of milliseconds spent reordering variables since the manager was initialized. The time spent in collecting garbage before reordering is included.]
SideEffects [None]
SeeAlso [Cudd_ReadReorderings]
Definition at line 2000 of file cuddAPI.c.
| int Cudd_ReadSiftMaxSwap | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reads the siftMaxSwap parameter of the manager.]
Description [Reads the siftMaxSwap parameter of the manager. This parameter gives the maximum number of swaps that will be attempted for each invocation of sifting. The real number of swaps may exceed the set limit because the package will always complete the sifting of the variable that causes the limit to be reached.]
SideEffects [None]
SeeAlso [Cudd_ReadSiftMaxVar Cudd_SetSiftMaxSwap]
Definition at line 2220 of file cuddAPI.c.
| int Cudd_ReadSiftMaxVar | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reads the siftMaxVar parameter of the manager.]
Description [Reads the siftMaxVar parameter of the manager. This parameter gives the maximum number of variables that will be sifted for each invocation of sifting.]
SideEffects [None]
SeeAlso [Cudd_ReadSiftMaxSwap Cudd_SetSiftMaxVar]
Definition at line 2173 of file cuddAPI.c.
| int Cudd_ReadSize | ( | DdManager * | dd | ) |
| unsigned int Cudd_ReadSlots | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the total number of slots of the unique table.]
Description [Returns the total number of slots of the unique table. This number ismainly for diagnostic purposes.]
SideEffects [None]
Definition at line 1720 of file cuddAPI.c.
| unsigned long Cudd_ReadStartTime | ( | DdManager * | unique | ) |
Function********************************************************************
Synopsis [Returns the start time of the manager.]
Description [Returns the start time of the manager. This is initially set to the number of milliseconds since the program started, but may be reset by the application.]
SideEffects [None]
SeeAlso [Cudd_SetStartTime Cudd_ResetStartTime Cudd_ReadTimeLimit]
Definition at line 681 of file cuddAPI.c.
| FILE* Cudd_ReadStderr | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reads the stderr of a manager.]
Description [Reads the stderr of a manager. This is the file pointer to which messages normally going to stderr are written. It is initialized to stderr. Cudd_SetStderr allows the application to redirect it.]
SideEffects [None]
SeeAlso [Cudd_SetStderr Cudd_ReadStdout]
Definition at line 4150 of file cuddAPI.c.
| FILE* Cudd_ReadStdout | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reads the stdout of a manager.]
Description [Reads the stdout of a manager. This is the file pointer to which messages normally going to stdout are written. It is initialized to stdout. Cudd_SetStdout allows the application to redirect it.]
SideEffects [None]
SeeAlso [Cudd_SetStdout Cudd_ReadStderr]
Definition at line 4107 of file cuddAPI.c.
| double Cudd_ReadSwapSteps | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reads the number of elementary reordering steps.]
Description []
SideEffects [none]
SeeAlso []
| int Cudd_ReadSymmviolation | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the current value of the symmviolation parameter used in group sifting.]
Description [Returns the current value of the symmviolation parameter. This parameter is used in group sifting to decide how many violations to the symmetry conditions f10 = f01 or f11 = f00 are tolerable when checking for aggregation due to extended symmetry. The value should be between 0 and 100. A small value causes fewer variables to be aggregated. The default value is 0.]
SideEffects [None]
SeeAlso [Cudd_SetSymmviolation]
Definition at line 2992 of file cuddAPI.c.
| unsigned long Cudd_ReadTimeLimit | ( | DdManager * | unique | ) |
Function********************************************************************
Synopsis [Returns the time limit for the manager.]
Description [Returns the time limit for the manager. This is initially set to a very large number, but may be reset by the application.]
SideEffects [None]
SeeAlso [Cudd_SetTimeLimit Cudd_UpdateTimeLimit Cudd_UnsetTimeLimit Cudd_IncreaseTimeLimit Cudd_TimeLimited Cudd_ReadStartTime]
Definition at line 765 of file cuddAPI.c.
| double Cudd_ReadUniqueLinks | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the number of links followed in the unique table.]
Description [Returns the number of links followed during look-ups in the unique table if the keeping of this statistic is enabled; -1 otherwise. If an item is found in the first position of its collision list, the number of links followed is taken to be 0. If it is in second position, the number of links is 1, and so on. This statistic is enabled only if the package is compiled with DD_UNIQUE_PROFILE defined.]
SideEffects [None]
SeeAlso [Cudd_ReadUniqueLookUps]
| double Cudd_ReadUniqueLookUps | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the number of look-ups in the unique table.]
Description [Returns the number of look-ups in the unique table if the keeping of this statistic is enabled; -1 otherwise. This statistic is enabled only if the package is compiled with DD_UNIQUE_PROFILE defined.]
SideEffects [None]
SeeAlso [Cudd_ReadUniqueLinks]
| double Cudd_ReadUsedSlots | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reads the fraction of used slots in the unique table.]
Description [Reads the fraction of used slots in the unique table. The unused slots are those in which no valid data is stored. Garbage collection, variable reordering, and subtable resizing may cause used slots to become unused.]
SideEffects [None]
SeeAlso [Cudd_ReadSlots]
Definition at line 1743 of file cuddAPI.c.
Function********************************************************************
Synopsis [Returns the i-th element of the vars array.]
Description [Returns the i-th element of the vars array if it falls within the array bounds; NULL otherwise. If i is the index of an existing variable, this function produces the same result as Cudd_bddIthVar. However, if the i-th var does not exist yet, Cudd_bddIthVar will create it, whereas Cudd_ReadVars will not.]
SideEffects [None]
SeeAlso [Cudd_bddIthVar]
Definition at line 2689 of file cuddAPI.c.
Function********************************************************************
Synopsis [Returns the ZDD for the constant 1 function.]
Description [Returns the ZDD for the constant 1 function. The representation of the constant 1 function as a ZDD depends on how many variables it (nominally) depends on. The index of the topmost variable in the support is given as argument i.]
SideEffects [None]
SeeAlso [Cudd_ReadOne]
Definition at line 1250 of file cuddAPI.c.
| int Cudd_ReadZddSize | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns the zero constant of the manager.]
Description [Returns the zero constant of the manager. The zero constant is the arithmetic zero, rather than the logic zero. The latter is the complement of the one constant.]
SideEffects [None]
SeeAlso [Cudd_ReadOne Cudd_ReadLogicZero]
Definition at line 1276 of file cuddAPI.c.
Function********************************************************************
Synopsis [Decreases the reference count of node n.]
Description [Decreases the reference count of node n. If n dies, recursively decreases the reference counts of its children. It is used to dispose of a DD that is no longer needed.]
SideEffects [None]
SeeAlso [Cudd_Deref Cudd_Ref Cudd_RecursiveDerefZdd]
Definition at line 150 of file cuddRef.c.
Function********************************************************************
Synopsis [Decreases the reference count of ZDD node n.]
Description [Decreases the reference count of ZDD node n. If n dies, recursively decreases the reference counts of its children. It is used to dispose of a ZDD that is no longer needed.]
SideEffects [None]
SeeAlso [Cudd_Deref Cudd_Ref Cudd_RecursiveDeref]
Definition at line 381 of file cuddRef.c.
| int Cudd_ReduceHeap | ( | DdManager * | table, |
| Cudd_ReorderingType | heuristic, | ||
| int | minsize | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Main dynamic reordering routine.]
Description [Main dynamic reordering routine. Calls one of the possible reordering procedures:
For sifting, symmetric sifting, group sifting, and window permutation it is possible to request reordering to convergence.
The core of all methods is the reordering procedure cuddSwapInPlace() which swaps two adjacent variables and is based on Rudell's paper. Returns 1 in case of success; 0 otherwise. In the case of symmetric sifting (with and without convergence) returns 1 plus the number of symmetric variables, in case of success.]
SideEffects [Changes the variable order for all diagrams and clears the cache.]
Definition at line 172 of file cuddReorder.c.
| void Cudd_Ref | ( | DdNode * | n | ) |
| DdNode* Cudd_RemapOverApprox | ( | DdManager * | dd, |
| DdNode * | f, | ||
| int | numVars, | ||
| int | threshold, | ||
| double | quality | ||
| ) |
| DdNode* Cudd_RemapUnderApprox | ( | DdManager * | dd, |
| DdNode * | f, | ||
| int | numVars, | ||
| int | threshold, | ||
| double | quality | ||
| ) |
| int Cudd_RemoveHook | ( | DdManager * | dd, |
| DD_HFP | f, | ||
| Cudd_HookType | where | ||
| ) |
Function********************************************************************
Synopsis [Removes a function from a hook.]
Description [Removes a function from a hook. A hook is a list of application-provided functions called on certain occasions by the package. Returns 1 if successful; 0 the function was not in the list.]
SideEffects [None]
SeeAlso [Cudd_AddHook]
Definition at line 3631 of file cuddAPI.c.
| int Cudd_ReorderingReporting | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Returns 1 if reporting of reordering stats is enabled.]
Description [Returns 1 if reporting of reordering stats is enabled; 0 otherwise.]
SideEffects [none]
SeeAlso [Cudd_EnableReorderingReporting Cudd_DisableReorderingReporting]
Definition at line 3916 of file cuddAPI.c.
| int Cudd_ReorderingStatus | ( | DdManager * | unique, |
| Cudd_ReorderingType * | method | ||
| ) |
Function********************************************************************
Synopsis [Reports the status of automatic dynamic reordering of BDDs and ADDs.]
Description [Reports the status of automatic dynamic reordering of BDDs and ADDs. Parameter method is set to the reordering method currently selected. Returns 1 if automatic reordering is enabled; 0 otherwise.]
SideEffects [Parameter method is set to the reordering method currently selected.]
SeeAlso [Cudd_AutodynEnable Cudd_AutodynDisable Cudd_ReorderingStatusZdd]
Definition at line 975 of file cuddAPI.c.
| int Cudd_ReorderingStatusZdd | ( | DdManager * | unique, |
| Cudd_ReorderingType * | method | ||
| ) |
Function********************************************************************
Synopsis [Reports the status of automatic dynamic reordering of ZDDs.]
Description [Reports the status of automatic dynamic reordering of ZDDs. Parameter method is set to the ZDD reordering method currently selected. Returns 1 if automatic reordering is enabled; 0 otherwise.]
SideEffects [Parameter method is set to the ZDD reordering method currently selected.]
SeeAlso [Cudd_AutodynEnableZdd Cudd_AutodynDisableZdd Cudd_ReorderingStatus]
Definition at line 1052 of file cuddAPI.c.
| int Cudd_Reserve | ( | DdManager * | manager, |
| int | amount | ||
| ) |
Function********************************************************************
Synopsis [Expand manager without creating variables.]
Description [Expand a manager by a specified number of subtables without actually creating new variables. This function can be used to reduce the frequency of resizing when an estimate of the number of variables is available. One would call this function instead of passing the number of variables to Cudd_Init if variables should not be created right away of if the estimate on their number became available only after the manager has been created. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_Init]
Definition at line 230 of file cuddTable.c.
| void Cudd_ResetStartTime | ( | DdManager * | unique | ) |
Function********************************************************************
Synopsis [Resets the start time of the manager.]
Description [Resets the start time of the manager.]
SideEffects [None]
SeeAlso [Cudd_ReadStartTime Cudd_SetStartTime Cudd_SetTimeLimit]
Definition at line 743 of file cuddAPI.c.
| void Cudd_SetArcviolation | ( | DdManager * | dd, |
| int | arcviolation | ||
| ) |
Function********************************************************************
Synopsis [Sets the value of the arcviolation parameter used in group sifting.]
Description [Sets the value of the arcviolation parameter. This parameter is used in group sifting to decide how many arcs into y not coming from x are tolerable when checking for aggregation due to extended symmetry. The value should be between 0 and 100. A small value causes fewer variables to be aggregated. The default value is 0.]
SideEffects [None]
SeeAlso [Cudd_ReadArcviolation]
Definition at line 3072 of file cuddAPI.c.
Function********************************************************************
Synopsis [Sets the background constant of the manager.]
Description [Sets the background constant of the manager. It assumes that the DdNode pointer bck is already referenced.]
SideEffects [None]
Definition at line 1371 of file cuddAPI.c.
| void Cudd_SetEpsilon | ( | DdManager * | dd, |
| CUDD_VALUE_TYPE | ep | ||
| ) |
Function********************************************************************
Synopsis [Sets the epsilon parameter of the manager to ep.]
Description [Sets the epsilon parameter of the manager to ep. The epsilon parameter control the comparison between floating point numbers.]
SideEffects [None]
SeeAlso [Cudd_ReadEpsilon]
Definition at line 2733 of file cuddAPI.c.
| void Cudd_SetGroupcheck | ( | DdManager * | dd, |
| Cudd_AggregationType | gc | ||
| ) |
Function********************************************************************
Synopsis [Sets the parameter groupcheck of the manager to gc.]
Description [Sets the parameter groupcheck of the manager to gc. The groupcheck parameter determines the aggregation criterion in group sifting.]
SideEffects [None]
SeeAlso [Cudd_ReadGroupCheck]
Definition at line 2778 of file cuddAPI.c.
| void Cudd_SetLooseUpTo | ( | DdManager * | dd, |
| unsigned int | lut | ||
| ) |
Function********************************************************************
Synopsis [Sets the looseUpTo parameter of the manager.]
Description [Sets the looseUpTo parameter of the manager. This parameter of the manager controls the threshold beyond which no fast growth of the unique table is allowed. The threshold is given as a number of slots. If the value passed to this function is 0, the function determines a suitable value based on the available memory.]
SideEffects [None]
SeeAlso [Cudd_ReadLooseUpTo Cudd_SetMinHit]
Definition at line 1585 of file cuddAPI.c.
| void Cudd_SetMaxCacheHard | ( | DdManager * | dd, |
| unsigned int | mc | ||
| ) |
Function********************************************************************
Synopsis [Sets the maxCacheHard parameter of the manager.]
Description [Sets the maxCacheHard parameter of the manager. The cache cannot grow larger than maxCacheHard entries. This parameter allows an application to control the trade-off of memory versus speed. If the value passed to this function is 0, the function determines a suitable maximum cache size based on the available memory.]
SideEffects [None]
SeeAlso [Cudd_ReadMaxCacheHard Cudd_SetMaxCache]
Definition at line 1655 of file cuddAPI.c.
| void Cudd_SetMaxGrowth | ( | DdManager * | dd, |
| double | mg | ||
| ) |
Function********************************************************************
Synopsis [Sets the maxGrowth parameter of the manager.]
Description [Sets the maxGrowth parameter of the manager. This parameter determines how much the number of nodes can grow during sifting of a variable. Overall, sifting never increases the size of the decision diagrams. This parameter only refers to intermediate results. A lower value will speed up sifting, possibly at the expense of quality.]
SideEffects [None]
SeeAlso [Cudd_ReadMaxGrowth Cudd_SetMaxGrowthAlternate]
Definition at line 2295 of file cuddAPI.c.
| void Cudd_SetMaxGrowthAlternate | ( | DdManager * | dd, |
| double | mg | ||
| ) |
Function********************************************************************
Synopsis [Sets the maxGrowthAlt parameter of the manager.]
Description [Sets the maxGrowthAlt parameter of the manager. This parameter is analogous to the maxGrowth paramter, and is used every given number of reorderings instead of maxGrowth. The number of reorderings is set with Cudd_SetReorderingCycle. If the number of reorderings is 0 (default) maxGrowthAlt is never used.]
SideEffects [None]
SeeAlso [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowth Cudd_SetReorderingCycle Cudd_ReadReorderingCycle]
Definition at line 2346 of file cuddAPI.c.
| void Cudd_SetMaxLive | ( | DdManager * | dd, |
| unsigned int | maxLive | ||
| ) |
Function********************************************************************
Synopsis [Sets the maximum allowed number of live nodes.]
Description [Sets the maximum allowed number of live nodes. When this number is exceeded, the package returns NULL.]
SideEffects [none]
SeeAlso [Cudd_ReadMaxLive]
Definition at line 4286 of file cuddAPI.c.
| void Cudd_SetMaxMemory | ( | DdManager * | dd, |
| unsigned long | maxMemory | ||
| ) |
Function********************************************************************
Synopsis [Sets the maximum allowed memory.]
Description [Sets the maximum allowed memory. When this number is exceeded, the package returns NULL.]
SideEffects [none]
SeeAlso [Cudd_ReadMaxMemory]
Definition at line 4329 of file cuddAPI.c.
| void Cudd_SetMaxReorderings | ( | DdManager * | dd, |
| unsigned int | mr | ||
| ) |
Function********************************************************************
Synopsis [Sets the maximum number of times reordering may be invoked.]
Description [Sets the maximum number of times reordering may be invoked in this manager. The default value is (practically) infinite.]
SideEffects [None]
SeeAlso [Cudd_ReadReorderings Cudd_ReadMaxReorderings Cudd_ReduceHeap]
Definition at line 1978 of file cuddAPI.c.
| void Cudd_SetMinHit | ( | DdManager * | dd, |
| unsigned int | hr | ||
| ) |
Function********************************************************************
Synopsis [Sets the hit rate that causes resizinig of the computed table.]
Description [Sets the minHit parameter of the manager. This parameter controls the resizing of the computed table. If the hit rate is larger than the specified value, and the cache is not already too large, then its size is doubled.]
SideEffects [None]
SeeAlso [Cudd_ReadMinHit]
Definition at line 1538 of file cuddAPI.c.
| void Cudd_SetNextReordering | ( | DdManager * | dd, |
| unsigned int | next | ||
| ) |
Function********************************************************************
Synopsis [Sets the threshold for the next dynamic reordering.]
Description [Sets the threshold for the next dynamic reordering. The threshold is in terms of number of nodes and is in effect only if reordering is enabled. The count does not include the dead nodes, unless the countDead parameter of the manager has been changed from its default setting.]
SideEffects [None]
SeeAlso [Cudd_ReadNextReordering]
Definition at line 4219 of file cuddAPI.c.
| void Cudd_SetNumberXovers | ( | DdManager * | dd, |
| int | numberXovers | ||
| ) |
Function********************************************************************
Synopsis [Sets the number of crossovers used by the genetic algorithm for reordering.]
Description [Sets the number of crossovers used by the genetic algorithm for variable reordering. A larger number of crossovers will cause the genetic algorithm to take more time, but will generally produce better results. The default value is 0, in which case the package uses three times the number of variables as number of crossovers, with a maximum of 60.]
SideEffects [None]
SeeAlso [Cudd_ReadNumberXovers]
Definition at line 3178 of file cuddAPI.c.
| void Cudd_SetOrderRandomization | ( | DdManager * | dd, |
| unsigned int | factor | ||
| ) |
| void Cudd_SetPopulationSize | ( | DdManager * | dd, |
| int | populationSize | ||
| ) |
Function********************************************************************
Synopsis [Sets the size of the population used by the genetic algorithm for reordering.]
Description [Sets the size of the population used by the genetic algorithm for variable reordering. A larger population size will cause the genetic algorithm to take more time, but will generally produce better results. The default value is 0, in which case the package uses three times the number of variables as population size, with a maximum of 120.]
SideEffects [Changes the manager.]
SeeAlso [Cudd_ReadPopulationSize]
Definition at line 3125 of file cuddAPI.c.
| void Cudd_SetRecomb | ( | DdManager * | dd, |
| int | recomb | ||
| ) |
Function********************************************************************
Synopsis [Sets the value of the recombination parameter used in group sifting.]
Description [Sets the value of the recombination parameter used in group sifting. A larger (positive) value makes the aggregation of variables due to the second difference criterion more likely. A smaller (negative) value makes aggregation less likely. The default value is 0.]
SideEffects [Changes the manager.]
SeeAlso [Cudd_ReadRecomb]
Definition at line 2964 of file cuddAPI.c.
| void Cudd_SetReorderingCycle | ( | DdManager * | dd, |
| int | cycle | ||
| ) |
Function********************************************************************
Synopsis [Sets the reordCycle parameter of the manager.]
Description [Sets the reordCycle parameter of the manager. This parameter determines how often the alternate threshold on maximum growth is used in reordering.]
SideEffects [None]
SeeAlso [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowthAlternate Cudd_ReadReorderingCycle]
Definition at line 2393 of file cuddAPI.c.
| void Cudd_SetSiftMaxSwap | ( | DdManager * | dd, |
| int | sms | ||
| ) |
Function********************************************************************
Synopsis [Sets the siftMaxSwap parameter of the manager.]
Description [Sets the siftMaxSwap parameter of the manager. This parameter gives the maximum number of swaps that will be attempted for each invocation of sifting. The real number of swaps may exceed the set limit because the package will always complete the sifting of the variable that causes the limit to be reached.]
SideEffects [None]
SeeAlso [Cudd_SetSiftMaxVar Cudd_ReadSiftMaxSwap]
Definition at line 2244 of file cuddAPI.c.
| void Cudd_SetSiftMaxVar | ( | DdManager * | dd, |
| int | smv | ||
| ) |
Function********************************************************************
Synopsis [Sets the siftMaxVar parameter of the manager.]
Description [Sets the siftMaxVar parameter of the manager. This parameter gives the maximum number of variables that will be sifted for each invocation of sifting.]
SideEffects [None]
SeeAlso [Cudd_SetSiftMaxSwap Cudd_ReadSiftMaxVar]
Definition at line 2195 of file cuddAPI.c.
| void Cudd_SetStartTime | ( | DdManager * | unique, |
| unsigned long | st | ||
| ) |
Function********************************************************************
Synopsis [Sets the start time of the manager.]
Description [Sets the start time of the manager.]
SideEffects [None]
SeeAlso [Cudd_ReadStartTime Cudd_ResetStartTime Cudd_ReadElapsedTime Cudd_SetTimeLimit]
Definition at line 722 of file cuddAPI.c.
| void Cudd_SetStderr | ( | DdManager * | dd, |
| FILE * | fp | ||
| ) |
| void Cudd_SetStdout | ( | DdManager * | dd, |
| FILE * | fp | ||
| ) |
| void Cudd_SetSymmviolation | ( | DdManager * | dd, |
| int | symmviolation | ||
| ) |
Function********************************************************************
Synopsis [Sets the value of the symmviolation parameter used in group sifting.]
Description [Sets the value of the symmviolation parameter. This parameter is used in group sifting to decide how many violations to the symmetry conditions f10 = f01 or f11 = f00 are tolerable when checking for aggregation due to extended symmetry. The value should be between 0 and 100. A small value causes fewer variables to be aggregated. The default value is 0.]
SideEffects [Changes the manager.]
SeeAlso [Cudd_ReadSymmviolation]
Definition at line 3019 of file cuddAPI.c.
| void Cudd_SetTimeLimit | ( | DdManager * | unique, |
| unsigned long | tl | ||
| ) |
Function********************************************************************
Synopsis [Sets the time limit for the manager.]
Description [Sets the time limit for the manager.]
SideEffects [None]
SeeAlso [Cudd_ReadTimeLimit Cudd_UnsetTimeLimit Cudd_UpdateTimeLimit Cudd_IncreaseTimeLimit Cudd_TimeLimited Cudd_SetStartTime]
Definition at line 786 of file cuddAPI.c.
| int Cudd_SharingSize | ( | DdNode ** | nodeArray, |
| int | n | ||
| ) |
Function********************************************************************
Synopsis [Counts the number of nodes in an array of DDs.]
Description [Counts the number of nodes in an array of DDs. Shared nodes are counted only once. Returns the total number of nodes.]
SideEffects [None]
SeeAlso [Cudd_DagSize]
Definition at line 548 of file cuddUtil.c.
Function********************************************************************
Synopsis [Find the length of the shortest path(s) in a DD.]
Description [Find the length of the shortest path(s) in a DD. f is the DD we want to get the shortest path for; weight[i] is the weight of the THEN edge coming from the node whose index is i. All ELSE edges have 0 weight. Returns the length of the shortest path(s) if such a path is found; a large number if the function is identically 0, and CUDD_OUT_OF_MEM in case of failure.]
SideEffects [None]
SeeAlso [Cudd_ShortestPath]
Definition at line 364 of file cuddSat.c.
| DdNode* Cudd_ShortestPath | ( | DdManager * | manager, |
| DdNode * | f, | ||
| int * | weight, | ||
| int * | support, | ||
| int * | length | ||
| ) |
Function********************************************************************
Synopsis [Finds a shortest path in a DD.]
Description [Finds a shortest path in a DD. f is the DD we want to get the shortest path for; weight[i] is the weight of the THEN arc coming from the node whose index is i. If weight is NULL, then unit weights are assumed for all THEN arcs. All ELSE arcs have 0 weight. If non-NULL, both weight and support should point to arrays with at least as many entries as there are variables in the manager. Returns the shortest path as the BDD of a cube.]
SideEffects [support contains on return the true support of f. If support is NULL on entry, then Cudd_ShortestPath does not compute the true support info. length contains the length of the path.]
SeeAlso [Cudd_ShortestLength Cudd_LargestCube]
Definition at line 203 of file cuddSat.c.
| int Cudd_ShuffleHeap | ( | DdManager * | table, |
| int * | permutation | ||
| ) |
Function********************************************************************
Synopsis [Reorders variables according to given permutation.]
Description [Reorders variables according to given permutation. The i-th entry of the permutation array contains the index of the variable that should be brought to the i-th level. The size of the array should be equal or greater to the number of variables currently in use. Returns 1 in case of success; 0 otherwise.]
SideEffects [Changes the variable order for all diagrams and clears the cache.]
SeeAlso [Cudd_ReduceHeap]
Definition at line 337 of file cuddReorder.c.
| DdNode* Cudd_SolveEqn | ( | DdManager * | bdd, |
| DdNode * | F, | ||
| DdNode * | Y, | ||
| DdNode ** | G, | ||
| int ** | yIndex, | ||
| int | n | ||
| ) |
| void Cudd_Srandom | ( | long | seed | ) |
Function********************************************************************
Synopsis [Initializer for the portable random number generator.]
Description [Initializer for the portable number generator based on ran2 in "Numerical Recipes in C." The input is the seed for the generator. If it is negative, its absolute value is taken as seed. If it is 0, then 1 is taken as seed. The initialized sets up the two recurrences used to generate a long-period stream, and sets up the shuffle table.]
SideEffects [None]
SeeAlso [Cudd_Random]
Definition at line 2772 of file cuddUtil.c.
| int Cudd_StdPostReordHook | ( | DdManager * | dd, |
| const char * | str, | ||
| void * | data | ||
| ) |
Function********************************************************************
Synopsis [Sample hook function to call after reordering.]
Description [Sample hook function to call after reordering. Prints on the manager's stdout final size and reordering time. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_StdPreReordHook]
Definition at line 3826 of file cuddAPI.c.
| int Cudd_StdPreReordHook | ( | DdManager * | dd, |
| const char * | str, | ||
| void * | data | ||
| ) |
Function********************************************************************
Synopsis [Sample hook function to call before reordering.]
Description [Sample hook function to call before reordering. Prints on the manager's stdout reordering method and initial size. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_StdPostReordHook]
Definition at line 3733 of file cuddAPI.c.
| DdNode* Cudd_SubsetShortPaths | ( | DdManager * | dd, |
| DdNode * | f, | ||
| int | numVars, | ||
| int | threshold, | ||
| int | hardlimit | ||
| ) |
| DdNode* Cudd_SubsetWithMaskVars | ( | DdManager * | dd, |
| DdNode * | f, | ||
| DdNode ** | vars, | ||
| int | nvars, | ||
| DdNode ** | maskVars, | ||
| int | mvars | ||
| ) |
Function********************************************************************
Synopsis [Extracts a subset from a BDD.]
Description [Extracts a subset from a BDD in the following procedure.
SideEffects [None]
SeeAlso []
Definition at line 1610 of file cuddUtil.c.
| DdNode* Cudd_SupersetShortPaths | ( | DdManager * | dd, |
| DdNode * | f, | ||
| int | numVars, | ||
| int | threshold, | ||
| int | hardlimit | ||
| ) |
Function********************************************************************
Synopsis [Finds the variables on which a DD depends.]
Description [Finds the variables on which a DD depends. Returns a BDD consisting of the product of the variables if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_VectorSupport Cudd_ClassifySupport]
Definition at line 789 of file cuddUtil.c.
Function********************************************************************
Synopsis [Finds the variables on which a DD depends.]
Description [Finds the variables on which a DD depends. Returns an index array of the variables if successful; NULL otherwise. The size of the array equals the number of variables in the manager. Each entry of the array is 1 if the corresponding variable is in the support of the DD and 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_Support Cudd_SupportIndices Cudd_ClassifySupport]
Definition at line 842 of file cuddUtil.c.
Function********************************************************************
Synopsis [Finds the variables on which a DD depends.]
Description [Finds the variables on which a DD depends. Returns the number of variables if successful; CUDD_OUT_OF_MEM otherwise.]
SideEffects [The indices of the support variables are returned as side effects. If the function is constant, no array is allocated.]
SeeAlso [Cudd_Support Cudd_SupportIndex Cudd_VectorSupportIndices]
Definition at line 744 of file cuddUtil.c.
Function********************************************************************
Synopsis [Counts the variables on which a DD depends.]
Description [Returns the variables on which a DD depends.]
SideEffects [None]
SeeAlso [Cudd_Support Cudd_SupportIndices]
Definition at line 882 of file cuddUtil.c.
| void Cudd_SymmProfile | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Prints statistics on symmetric variables.]
Description []
SideEffects [None]
Definition at line 138 of file cuddSymmetry.c.
| int Cudd_TimeLimited | ( | DdManager * | unique | ) |
Function********************************************************************
Synopsis [Returns true if the time limit for the manager is set.]
Description [Returns true if the time limit for the manager is set.]
SideEffects [None]
SeeAlso [Cudd_ReadTimeLimit Cudd_SetTimeLimit Cudd_UpdateTimeLimit Cudd_UnsetTimeLimit Cudd_IncreaseTimeLimit]
Definition at line 885 of file cuddAPI.c.
| void Cudd_tlcInfoFree | ( | DdTlcInfo * | t | ) |
| void Cudd_TurnOffCountDead | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Causes the dead nodes not to be counted towards triggering reordering.]
Description [Causes the dead nodes not to be counted towards triggering reordering. This causes less frequent reorderings. By default dead nodes are not counted. Therefore there is no need to call this function unless Cudd_TurnOnCountDead has been previously called.]
SideEffects [Changes the manager.]
SeeAlso [Cudd_TurnOnCountDead Cudd_DeadAreCounted]
Definition at line 2915 of file cuddAPI.c.
| void Cudd_TurnOnCountDead | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Causes the dead nodes to be counted towards triggering reordering.]
Description [Causes the dead nodes to be counted towards triggering reordering. This causes more frequent reorderings. By default dead nodes are not counted.]
SideEffects [Changes the manager.]
SeeAlso [Cudd_TurnOffCountDead Cudd_DeadAreCounted]
Definition at line 2890 of file cuddAPI.c.
| DdNode* Cudd_UnderApprox | ( | DdManager * | dd, |
| DdNode * | f, | ||
| int | numVars, | ||
| int | threshold, | ||
| int | safe, | ||
| double | quality | ||
| ) |
| void Cudd_UnsetTimeLimit | ( | DdManager * | unique | ) |
Function********************************************************************
Synopsis [Unsets the time limit for the manager.]
Description [Unsets the time limit for the manager. Actually, sets it to a very large value.]
SideEffects [None]
SeeAlso [Cudd_ReadTimeLimit Cudd_SetTimeLimit Cudd_UpdateTimeLimit Cudd_IncreaseTimeLimit Cudd_TimeLimited Cudd_SetStartTime]
Definition at line 864 of file cuddAPI.c.
| void Cudd_UpdateTimeLimit | ( | DdManager * | unique | ) |
Function********************************************************************
Synopsis [Updates the time limit for the manager.]
Description [Updates the time limit for the manager by subtracting the elapsed time from it.]
SideEffects [None]
SeeAlso [Cudd_ReadTimeLimit Cudd_SetTimeLimit Cudd_UnsetTimeLimit Cudd_IncreaseTimeLimit Cudd_TimeLimited Cudd_SetStartTime]
Definition at line 809 of file cuddAPI.c.
Function********************************************************************
Synopsis [Finds the variables on which a set of DDs depends.]
Description [Finds the variables on which a set of DDs depends. The set must contain either BDDs and ADDs, or ZDDs. Returns a BDD consisting of the product of the variables if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_Support Cudd_ClassifySupport]
Definition at line 966 of file cuddUtil.c.
Function********************************************************************
Synopsis [Finds the variables on which a set of DDs depends.]
Description [Finds the variables on which a set of DDs depends. The set must contain either BDDs and ADDs, or ZDDs. Returns an index array of the variables if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_SupportIndex Cudd_VectorSupport Cudd_VectorSupportIndices]
Definition at line 1017 of file cuddUtil.c.
Function********************************************************************
Synopsis [Finds the variables on which a set of DDs depends.]
Description [Finds the variables on which a set of DDs depends. The set must contain either BDDs and ADDs, or ZDDs. Returns the number of variables if successful; CUDD_OUT_OF_MEM otherwise.]
SideEffects [The indices of the support variables are returned as side effects. If the function is constant, no array is allocated.]
SeeAlso [Cudd_Support Cudd_SupportIndex Cudd_VectorSupportIndices]
Definition at line 912 of file cuddUtil.c.
Function********************************************************************
Synopsis [Counts the variables on which a set of DDs depends.]
Description [Returns the variables on which a set of DDs depends. The set must contain either BDDs and ADDs, or ZDDs.]
SideEffects [None]
SeeAlso [Cudd_VectorSupport Cudd_SupportSize]
Definition at line 1063 of file cuddUtil.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.]
SideEffects [None]
SeeAlso []
Definition at line 388 of file cuddZddSetop.c.
Function********************************************************************
Synopsis [Computes a complement cover for a ZDD node.]
Description [Computes a complement cover for a ZDD node. For lack of a better method, we first extract the function BDD from the ZDD cover, then make the complement of the ZDD cover from the complement of the BDD node by using ISOP. Returns a pointer to the resulting cover if successful; NULL otherwise. The result depends on current variable order.]
SideEffects [The result depends on current variable order.]
SeeAlso []
Definition at line 328 of file cuddZddFuncs.c.
| char* Cudd_zddCoverPathToString | ( | DdManager * | zdd, |
| int * | path, | ||
| char * | str | ||
| ) |
| int Cudd_zddDagSize | ( | DdNode * | p_node | ) |
Function********************************************************************
Synopsis [Computes the difference of two ZDDs.]
Description [Computes the difference of two ZDDs. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_zddDiffConst]
Definition at line 232 of file cuddZddSetop.c.
Function********************************************************************
Synopsis [Performs the inclusion test for ZDDs (P implies Q).]
Description [Inclusion test for ZDDs (P implies Q). No new nodes are generated by this procedure. Returns empty if true; a valid pointer different from empty or DD_NON_CONSTANT otherwise.]
SideEffects [None]
SeeAlso [Cudd_zddDiff]
Definition at line 262 of file cuddZddSetop.c.
Function********************************************************************
Synopsis [Computes the quotient of two unate covers.]
Description [Computes the quotient of two unate covers represented by ZDDs. Unate covers use one ZDD variable for each BDD variable. Returns a pointer to the resulting ZDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_zddWeakDiv]
Definition at line 237 of file cuddZddFuncs.c.
Function********************************************************************
Synopsis [Modified version of Cudd_zddDivide.]
Description [Modified version of Cudd_zddDivide. This function may disappear in future releases.]
SideEffects [None]
SeeAlso []
Definition at line 295 of file cuddZddFuncs.c.
| int Cudd_zddDumpDot | ( | DdManager * | dd, |
| int | n, | ||
| DdNode ** | f, | ||
| char ** | inames, | ||
| char ** | onames, | ||
| FILE * | fp | ||
| ) |
Function********************************************************************
Synopsis [Computes the intersection of two ZDDs.]
Description [Computes the intersection of two ZDDs. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 203 of file cuddZddSetop.c.
AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Computes an ISOP in ZDD form from BDDs.]
Description [Computes an irredundant sum of products (ISOP) in ZDD form from BDDs. The two BDDs L and U represent the lower bound and the upper bound, respectively, of the function. The ISOP uses two ZDD variables for each BDD variable: One for the positive literal, and one for the negative literal. These two variables should be adjacent in the ZDD order. The two ZDD variables corresponding to BDD variable i should have indices 2i and 2i+1. The result of this procedure depends on the variable order. If successful, Cudd_zddIsop returns the BDD for the function chosen from the interval. The ZDD representing the irredundant cover is returned as a side effect in zdd_I. In case of failure, NULL is returned.]
SideEffects [zdd_I holds the pointer to the ZDD for the ISOP on successful return.]
SeeAlso [Cudd_bddIsop Cudd_zddVarsFromBddVars]
Definition at line 132 of file cuddZddIsop.c.
AutomaticEnd Function********************************************************************
Synopsis [Computes the ITE of three ZDDs.]
Description [Computes the ITE of three ZDDs. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 144 of file cuddZddSetop.c.
Function********************************************************************
Synopsis [Returns the ZDD variable with index i.]
Description [Retrieves the ZDD variable with index i if it already exists, or creates a new ZDD variable. Returns a pointer to the variable if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddIthVar Cudd_addIthVar]
Definition at line 462 of file cuddAPI.c.
| int Cudd_zddNextPath | ( | DdGen * | gen, |
| int ** | path | ||
| ) |
| void Cudd_zddPrintSubtable | ( | DdManager * | table | ) |
AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Computes the product of two covers represented by ZDDs.]
Description [Computes the product of two covers represented by ZDDs. The result is also a ZDD. Returns a pointer to the result if successful; NULL otherwise. The covers on which Cudd_zddProduct operates use two ZDD variables for each function variable (one ZDD variable for each literal of the variable). Those two ZDD variables should be adjacent in the order.]
SideEffects [None]
SeeAlso [Cudd_zddUnateProduct]
Definition at line 141 of file cuddZddFuncs.c.
| long Cudd_zddReadNodeCount | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reports the number of nodes in ZDDs.]
Description [Reports the number of nodes in ZDDs. This number always includes the two constants 1 and 0.]
SideEffects [None]
SeeAlso [Cudd_ReadPeakNodeCount Cudd_ReadNodeCount]
Definition at line 3546 of file cuddAPI.c.
| void Cudd_zddRealignDisable | ( | DdManager * | unique | ) |
Function********************************************************************
Synopsis [Disables realignment of ZDD order to BDD order.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddRealignEnable Cudd_zddRealignmentEnabled Cudd_bddRealignEnable Cudd_bddRealignmentEnabled]
Definition at line 1129 of file cuddAPI.c.
| void Cudd_zddRealignEnable | ( | DdManager * | unique | ) |
Function********************************************************************
Synopsis [Enables realignment of ZDD order to BDD order.]
Description [Enables realignment of the ZDD variable order to the BDD variable order after the BDDs and ADDs have been reordered. The number of ZDD variables must be a multiple of the number of BDD variables for realignment to make sense. If this condition is not met, Cudd_ReduceHeap will return 0. Let M be the ratio of the two numbers. For the purpose of realignment, the ZDD variables from M*i to (M+1)*i-1 are reagarded as corresponding to BDD variable i. Realignment is initially disabled.]
SideEffects [None]
SeeAlso [Cudd_ReduceHeap Cudd_zddRealignDisable Cudd_zddRealignmentEnabled Cudd_bddRealignDisable Cudd_bddRealignmentEnabled]
Definition at line 1107 of file cuddAPI.c.
| int Cudd_zddRealignmentEnabled | ( | DdManager * | unique | ) |
Function********************************************************************
Synopsis [Tells whether the realignment of ZDD order to BDD order is enabled.]
Description [Returns 1 if the realignment of ZDD order to BDD order is enabled; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_zddRealignEnable Cudd_zddRealignDisable Cudd_bddRealignEnable Cudd_bddRealignDisable]
Definition at line 1077 of file cuddAPI.c.
| int Cudd_zddReduceHeap | ( | DdManager * | table, |
| Cudd_ReorderingType | heuristic, | ||
| int | minsize | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Main dynamic reordering routine for ZDDs.]
Description [Main dynamic reordering routine for ZDDs. Calls one of the possible reordering procedures:
For sifting and symmetric sifting it is possible to request reordering to convergence.
The core of all methods is the reordering procedure cuddZddSwapInPlace() which swaps two adjacent variables. Returns 1 in case of success; 0 otherwise. In the case of symmetric sifting (with and without convergence) returns 1 plus the number of symmetric variables, in case of success.]
SideEffects [Changes the variable order for all ZDDs and clears the cache.]
Definition at line 167 of file cuddZddReord.c.
| int Cudd_zddShuffleHeap | ( | DdManager * | table, |
| int * | permutation | ||
| ) |
Function********************************************************************
Synopsis [Reorders ZDD variables according to given permutation.]
Description [Reorders ZDD variables according to given permutation. The i-th entry of the permutation array contains the index of the variable that should be brought to the i-th level. The size of the array should be equal or greater to the number of variables currently in use. Returns 1 in case of success; 0 otherwise.]
SideEffects [Changes the ZDD variable order for all diagrams and clears the cache.]
SeeAlso [Cudd_zddReduceHeap]
Definition at line 300 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.]
SideEffects [None]
SeeAlso [Cudd_zddSubset1]
Definition at line 358 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.]
SideEffects [None]
SeeAlso [Cudd_zddSubset0]
Definition at line 326 of file cuddZddSetop.c.
| void Cudd_zddSymmProfile | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Prints statistics on symmetric ZDD variables.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 141 of file cuddZddSymm.c.
Function********************************************************************
Synopsis [Computes the product of two unate covers.]
Description [Computes the product of two unate covers represented as ZDDs. Unate covers use one ZDD variable for each BDD variable. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_zddProduct]
Definition at line 172 of file cuddZddFuncs.c.
Function********************************************************************
Synopsis [Computes the union of two ZDDs.]
Description [Computes the union of two ZDDs. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 174 of file cuddZddSetop.c.
| int Cudd_zddVarsFromBddVars | ( | DdManager * | dd, |
| int | multiplicity | ||
| ) |
Function********************************************************************
Synopsis [Creates one or more ZDD variables for each BDD variable.]
Description [Creates one or more ZDD variables for each BDD variable. If some ZDD variables already exist, only the missing variables are created. Parameter multiplicity allows the caller to control how many variables are created for each BDD variable in existence. For instance, if ZDDs are used to represent covers, two ZDD variables are required for each BDD variable. The order of the BDD variables is transferred to the ZDD variables. If a variable group tree exists for the BDD variables, a corresponding ZDD variable group tree is created by expanding the BDD variable tree. In any case, the ZDD variables derived from the same BDD variable are merged in a ZDD variable group. If a ZDD variable group tree exists, it is freed. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddNewVar Cudd_bddIthVar Cudd_bddNewVarAtLevel]
Definition at line 533 of file cuddAPI.c.
Function********************************************************************
Synopsis [Applies weak division to two covers.]
Description [Applies weak division to two ZDDs representing two covers. Returns a pointer to the ZDD representing the result if successful; NULL otherwise. The result of weak division depends on the variable order. The covers on which Cudd_zddWeakDiv operates use two ZDD variables for each function variable (one ZDD variable for each literal of the variable). Those two ZDD variables should be adjacent in the order.]
SideEffects [None]
SeeAlso [Cudd_zddDivide]
Definition at line 206 of file cuddZddFuncs.c.
Function********************************************************************
Synopsis [Modified version of Cudd_zddWeakDiv.]
Description [Modified version of Cudd_zddWeakDiv. This function may disappear in future releases.]
SideEffects [None]
SeeAlso [Cudd_zddWeakDiv]
Definition at line 266 of file cuddZddFuncs.c.
1.8.13