cudd.h Source File

00001 
00030 #ifndef _CUDD
00031 #define _CUDD
00032 
00033 /*---------------------------------------------------------------------------*/
00034 /* Nested includes                                                           */
00035 /*---------------------------------------------------------------------------*/
00036 
00037 #include "mtr.h"
00038 
00039 /*---------------------------------------------------------------------------*/
00040 /* Constant declarations                                                     */
00041 /*---------------------------------------------------------------------------*/
00042 
00043 #define CUDD_VERSION "2.3.0"
00044 
00045 #ifndef SIZEOF_VOID_P
00046 #define SIZEOF_VOID_P 4
00047 #endif
00048 #ifndef SIZEOF_INT
00049 #define SIZEOF_INT 4
00050 #endif
00051 #ifndef SIZEOF_LONG
00052 #define SIZEOF_LONG 4
00053 #endif
00054 
00055 #ifndef TRUE
00056 #define TRUE 1
00057 #endif
00058 #ifndef FALSE
00059 #define FALSE 0
00060 #endif
00061 
00062 #define CUDD_VALUE_TYPE   double
00063 #define CUDD_OUT_OF_MEM   -1
00064 /* The sizes of the subtables and the cache must be powers of two. */
00065 #define CUDD_UNIQUE_SLOTS 256 /* initial size of subtables */
00066 #define CUDD_CACHE_SLOTS  262144  /* default size of the cache */
00067 
00068 /* Constants for residue functions. */
00069 #define CUDD_RESIDUE_DEFAULT  0
00070 #define CUDD_RESIDUE_MSB  1
00071 #define CUDD_RESIDUE_TC   2
00072 
00073 /* CUDD_MAXINDEX is defined in such a way that on 32-bit and 64-bit
00074 ** machines one can cast an index to (int) without generating a negative
00075 ** number.
00076 */
00077 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00078 #define CUDD_MAXINDEX             (((DdHalfWord) ~0) >> 1)
00079 #else
00080 #define CUDD_MAXINDEX             ((DdHalfWord) ~0)
00081 #endif
00082 
00083 /* These constants define the digits used in the representation of
00084 ** arbitrary precision integers.  The two configurations tested use 8
00085 ** and 16 bits for each digit.  The typedefs should be in agreement
00086 ** with these definitions.
00087 */
00088 #define DD_APA_BITS 16
00089 #define DD_APA_BASE (1 << DD_APA_BITS)
00090 #define DD_APA_MASK (DD_APA_BASE - 1)
00091 #define DD_APA_HEXPRINT "%04x"
00092 
00093 /*---------------------------------------------------------------------------*/
00094 /* Stucture declarations                                                     */
00095 /*---------------------------------------------------------------------------*/
00096 
00097 
00098 /*---------------------------------------------------------------------------*/
00099 /* Type declarations                                                         */
00100 /*---------------------------------------------------------------------------*/
00101 
00109 typedef enum {
00110     CUDD_REORDER_SAME,
00111     CUDD_REORDER_NONE,
00112     CUDD_REORDER_RANDOM,
00113     CUDD_REORDER_RANDOM_PIVOT,
00114     CUDD_REORDER_SIFT,
00115     CUDD_REORDER_SIFT_CONVERGE,
00116     CUDD_REORDER_SYMM_SIFT,
00117     CUDD_REORDER_SYMM_SIFT_CONV,
00118     CUDD_REORDER_WINDOW2,
00119     CUDD_REORDER_WINDOW3,
00120     CUDD_REORDER_WINDOW4,
00121     CUDD_REORDER_WINDOW2_CONV,
00122     CUDD_REORDER_WINDOW3_CONV,
00123     CUDD_REORDER_WINDOW4_CONV,
00124     CUDD_REORDER_GROUP_SIFT,
00125     CUDD_REORDER_GROUP_SIFT_CONV,
00126     CUDD_REORDER_ANNEALING,
00127     CUDD_REORDER_GENETIC,
00128     CUDD_REORDER_LINEAR,
00129     CUDD_REORDER_LINEAR_CONVERGE,
00130     CUDD_REORDER_EXACT
00131 } Cudd_ReorderingType;
00132 
00133 
00141 typedef enum {
00142     CUDD_NO_CHECK,
00143     CUDD_GROUP_CHECK,
00144     CUDD_GROUP_CHECK2,
00145     CUDD_GROUP_CHECK3,
00146     CUDD_GROUP_CHECK4,
00147     CUDD_GROUP_CHECK5,
00148     CUDD_GROUP_CHECK6,
00149     CUDD_GROUP_CHECK7,
00150     CUDD_GROUP_CHECK8,
00151     CUDD_GROUP_CHECK9
00152 } Cudd_AggregationType;
00153 
00154 
00162 typedef enum {
00163     CUDD_PRE_GC_HOOK,
00164     CUDD_POST_GC_HOOK,
00165     CUDD_PRE_REORDERING_HOOK,
00166     CUDD_POST_REORDERING_HOOK
00167 } Cudd_HookType;
00168 
00169 
00177 typedef enum {
00178     CUDD_NO_ERROR,
00179     CUDD_MEMORY_OUT,
00180     CUDD_TOO_MANY_NODES,
00181     CUDD_MAX_MEM_EXCEEDED,
00182     CUDD_INVALID_ARG,
00183     CUDD_INTERNAL_ERROR
00184 } Cudd_ErrorType;
00185 
00186 
00187 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00188 typedef unsigned int   DdHalfWord;
00189 #else
00190 typedef unsigned short DdHalfWord;
00191 #endif
00192 
00193 #ifdef __osf__
00194 #pragma pointer_size save
00195 #pragma pointer_size short
00196 #endif
00197 
00198 typedef struct DdNode DdNode;
00199 
00200 typedef struct DdChildren {
00201     struct DdNode *T;
00202     struct DdNode *E;
00203 } DdChildren;
00204 
00205 /* The DdNode structure is the only one exported out of the package */
00206 struct DdNode {
00207     DdHalfWord index;
00208     DdHalfWord ref;   /* reference count */
00209     DdNode *next;   /* next pointer for unique table */
00210     union {
00211   CUDD_VALUE_TYPE value;  /* for constant nodes */
00212   DdChildren kids;  /* for internal nodes */
00213     } type;
00214 };
00215 
00216 #ifdef __osf__
00217 #pragma pointer_size restore
00218 #endif
00219 
00220 typedef struct DdManager DdManager;
00221 
00222 typedef struct DdGen DdGen;
00223 
00224 /* These typedefs for arbitrary precision arithmetic should agree with
00225 ** the corresponding constant definitions above. */
00226 typedef unsigned short int DdApaDigit;
00227 typedef unsigned long int DdApaDoubleDigit;
00228 typedef DdApaDigit * DdApaNumber;
00229 
00230 /*---------------------------------------------------------------------------*/
00231 /* Variable declarations                                                     */
00232 /*---------------------------------------------------------------------------*/
00233 
00234 
00235 /*---------------------------------------------------------------------------*/
00236 /* Macro declarations                                                        */
00237 /*---------------------------------------------------------------------------*/
00238 
00239 
00254 #define Cudd_IsConstant(node) ((Cudd_Regular(node))->index == CUDD_MAXINDEX)
00255 
00256 
00269 #define Cudd_Not(node) ((DdNode *)((long)(node) ^ 01))
00270 
00271 
00285 #define Cudd_NotCond(node,c) ((DdNode *)((long)(node) ^ (c)))
00286 
00287 
00299 #define Cudd_Regular(node) ((DdNode *)((unsigned long)(node) & ~01))
00300 
00301 
00313 #define Cudd_Complement(node) ((DdNode *)((unsigned long)(node) | 01))
00314 
00315 
00327 #define Cudd_IsComplement(node) ((int) ((long) (node) & 01))
00328 
00329 
00342 #define Cudd_T(node) ((Cudd_Regular(node))->type.kids.T)
00343 
00344 
00357 #define Cudd_E(node) ((Cudd_Regular(node))->type.kids.E)
00358 
00359 
00372 #define Cudd_V(node) ((Cudd_Regular(node))->type.value)
00373 
00374 
00389 #define Cudd_ReadIndex(dd,index) (Cudd_ReadPerm(dd,index))
00390 
00391 
00421 #define Cudd_ForeachCube(manager, f, gen, cube, value)\
00422     for((gen) = Cudd_FirstCube(manager, f, &cube, &value);\
00423   Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
00424   (void) Cudd_NextCube(gen, &cube, &value))
00425 
00426 
00455 #define Cudd_ForeachNode(manager, f, gen, node)\
00456     for((gen) = Cudd_FirstNode(manager, f, &node);\
00457   Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
00458   (void) Cudd_NextNode(gen, &node))
00459 
00460 
00461 /* These are potential duplicates. */
00462 #ifndef EXTERN
00463 #   ifdef __cplusplus
00464 # define EXTERN extern "C"
00465 #   else
00466 # define EXTERN extern
00467 #   endif
00468 #endif
00469 #ifndef ARGS
00470 #   if defined(__STDC__) || defined(__cplusplus)
00471 # define ARGS(protos) protos    /* ANSI C */
00472 #   else /* !(__STDC__ || __cplusplus) */
00473 # define ARGS(protos) ()    /* K&R C */
00474 #   endif /* !(__STDC__ || __cplusplus) */
00475 #endif
00476 
00477 
00480 /*---------------------------------------------------------------------------*/
00481 /* Function prototypes                                                       */
00482 /*---------------------------------------------------------------------------*/
00483 
00484 EXTERN DdNode * Cudd_addNewVar ARGS((DdManager *dd));
00485 EXTERN DdNode * Cudd_addNewVarAtLevel ARGS((DdManager *dd, int level));
00486 EXTERN DdNode * Cudd_bddNewVar ARGS((DdManager *dd));
00487 EXTERN DdNode * Cudd_bddNewVarAtLevel ARGS((DdManager *dd, int level));
00488 EXTERN DdNode * Cudd_addIthVar ARGS((DdManager *dd, int i));
00489 EXTERN DdNode * Cudd_bddIthVar ARGS((DdManager *dd, int i));
00490 EXTERN DdNode * Cudd_zddIthVar ARGS((DdManager *dd, int i));
00491 EXTERN int Cudd_zddVarsFromBddVars ARGS((DdManager *dd, int multiplicity));
00492 EXTERN DdNode * Cudd_addConst ARGS((DdManager *dd, CUDD_VALUE_TYPE c));
00493 EXTERN int Cudd_IsNonConstant ARGS((DdNode *f));
00494 EXTERN void Cudd_AutodynEnable ARGS((DdManager *unique, Cudd_ReorderingType method));
00495 EXTERN void Cudd_AutodynDisable ARGS((DdManager *unique));
00496 EXTERN int Cudd_ReorderingStatus ARGS((DdManager *unique, Cudd_ReorderingType *method));
00497 EXTERN void Cudd_AutodynEnableZdd ARGS((DdManager *unique, Cudd_ReorderingType method));
00498 EXTERN void Cudd_AutodynDisableZdd ARGS((DdManager *unique));
00499 EXTERN int Cudd_ReorderingStatusZdd ARGS((DdManager *unique, Cudd_ReorderingType *method));
00500 EXTERN int Cudd_zddRealignmentEnabled ARGS((DdManager *unique));
00501 EXTERN void Cudd_zddRealignEnable ARGS((DdManager *unique));
00502 EXTERN void Cudd_zddRealignDisable ARGS((DdManager *unique));
00503 EXTERN int Cudd_bddRealignmentEnabled ARGS((DdManager *unique));
00504 EXTERN void Cudd_bddRealignEnable ARGS((DdManager *unique));
00505 EXTERN void Cudd_bddRealignDisable ARGS((DdManager *unique));
00506 EXTERN DdNode * Cudd_ReadOne ARGS((DdManager *dd));
00507 EXTERN DdNode * Cudd_ReadZddOne ARGS((DdManager *dd, int i));
00508 EXTERN DdNode * Cudd_ReadZero ARGS((DdManager *dd));
00509 EXTERN DdNode * Cudd_ReadLogicZero ARGS((DdManager *dd));
00510 EXTERN DdNode * Cudd_ReadPlusInfinity ARGS((DdManager *dd));
00511 EXTERN DdNode * Cudd_ReadMinusInfinity ARGS((DdManager *dd));
00512 EXTERN DdNode * Cudd_ReadBackground ARGS((DdManager *dd));
00513 EXTERN void Cudd_SetBackground ARGS((DdManager *dd, DdNode *bck));
00514 EXTERN unsigned int Cudd_ReadCacheSlots ARGS((DdManager *dd));
00515 EXTERN double Cudd_ReadCacheUsedSlots ARGS((DdManager * dd));
00516 EXTERN double Cudd_ReadCacheLookUps ARGS((DdManager *dd));
00517 EXTERN double Cudd_ReadCacheHits ARGS((DdManager *dd));
00518 EXTERN double Cudd_ReadRecursiveCalls ARGS ((DdManager * dd));
00519 EXTERN unsigned int Cudd_ReadMinHit ARGS((DdManager *dd));
00520 EXTERN void Cudd_SetMinHit ARGS((DdManager *dd, unsigned int hr));
00521 EXTERN unsigned int Cudd_ReadLooseUpTo ARGS((DdManager *dd));
00522 EXTERN void Cudd_SetLooseUpTo ARGS((DdManager *dd, unsigned int lut));
00523 EXTERN unsigned int Cudd_ReadMaxCache ARGS((DdManager *dd));
00524 EXTERN unsigned int Cudd_ReadMaxCacheHard ARGS((DdManager *dd));
00525 EXTERN void Cudd_SetMaxCacheHard ARGS((DdManager *dd, unsigned int mc));
00526 EXTERN int Cudd_ReadSize ARGS((DdManager *dd));
00527 EXTERN int Cudd_ReadZddSize ARGS((DdManager *dd));
00528 EXTERN unsigned int Cudd_ReadSlots ARGS((DdManager *dd));
00529 EXTERN double Cudd_ReadUsedSlots ARGS((DdManager * dd));
00530 EXTERN double Cudd_ExpectedUsedSlots ARGS((DdManager * dd));
00531 EXTERN unsigned int Cudd_ReadKeys ARGS((DdManager *dd));
00532 EXTERN unsigned int Cudd_ReadDead ARGS((DdManager *dd));
00533 EXTERN unsigned int Cudd_ReadMinDead ARGS((DdManager *dd));
00534 EXTERN int Cudd_ReadReorderings ARGS((DdManager *dd));
00535 EXTERN long Cudd_ReadReorderingTime ARGS((DdManager * dd));
00536 EXTERN int Cudd_ReadGarbageCollections ARGS((DdManager * dd));
00537 EXTERN long Cudd_ReadGarbageCollectionTime ARGS((DdManager * dd));
00538 EXTERN double Cudd_ReadNodesFreed ARGS((DdManager * dd));
00539 EXTERN double Cudd_ReadNodesDropped ARGS((DdManager * dd));
00540 EXTERN double Cudd_ReadUniqueLookUps ARGS((DdManager * dd));
00541 EXTERN double Cudd_ReadUniqueLinks ARGS((DdManager * dd));
00542 EXTERN int Cudd_ReadSiftMaxVar ARGS((DdManager *dd));
00543 EXTERN void Cudd_SetSiftMaxVar ARGS((DdManager *dd, int smv));
00544 EXTERN int Cudd_ReadSiftMaxSwap ARGS((DdManager *dd));
00545 EXTERN void Cudd_SetSiftMaxSwap ARGS((DdManager *dd, int sms));
00546 EXTERN double Cudd_ReadMaxGrowth ARGS((DdManager *dd));
00547 EXTERN void Cudd_SetMaxGrowth ARGS((DdManager *dd, double mg));
00548 EXTERN MtrNode * Cudd_ReadTree ARGS((DdManager *dd));
00549 EXTERN void Cudd_SetTree ARGS((DdManager *dd, MtrNode *tree));
00550 EXTERN void Cudd_FreeTree ARGS((DdManager *dd));
00551 EXTERN MtrNode * Cudd_ReadZddTree ARGS((DdManager *dd));
00552 EXTERN void Cudd_SetZddTree ARGS((DdManager *dd, MtrNode *tree));
00553 EXTERN void Cudd_FreeZddTree ARGS((DdManager *dd));
00554 EXTERN unsigned int Cudd_NodeReadIndex ARGS((DdNode *node));
00555 EXTERN int Cudd_ReadPerm ARGS((DdManager *dd, int i));
00556 EXTERN int Cudd_ReadPermZdd ARGS((DdManager *dd, int i));
00557 EXTERN int Cudd_ReadInvPerm ARGS((DdManager *dd, int i));
00558 EXTERN int Cudd_ReadInvPermZdd ARGS((DdManager *dd, int i));
00559 EXTERN DdNode * Cudd_ReadVars ARGS((DdManager *dd, int i));
00560 EXTERN CUDD_VALUE_TYPE Cudd_ReadEpsilon ARGS((DdManager *dd));
00561 EXTERN void Cudd_SetEpsilon ARGS((DdManager *dd, CUDD_VALUE_TYPE ep));
00562 EXTERN Cudd_AggregationType Cudd_ReadGroupcheck ARGS((DdManager *dd));
00563 EXTERN void Cudd_SetGroupcheck ARGS((DdManager *dd, Cudd_AggregationType gc));
00564 EXTERN int Cudd_GarbageCollectionEnabled ARGS((DdManager *dd));
00565 EXTERN void Cudd_EnableGarbageCollection ARGS((DdManager *dd));
00566 EXTERN void Cudd_DisableGarbageCollection ARGS((DdManager *dd));
00567 EXTERN int Cudd_DeadAreCounted ARGS((DdManager *dd));
00568 EXTERN void Cudd_TurnOnCountDead ARGS((DdManager *dd));
00569 EXTERN void Cudd_TurnOffCountDead ARGS((DdManager *dd));
00570 EXTERN int Cudd_ReadRecomb ARGS((DdManager *dd));
00571 EXTERN void Cudd_SetRecomb ARGS((DdManager *dd, int recomb));
00572 EXTERN int Cudd_ReadSymmviolation ARGS((DdManager *dd));
00573 EXTERN void Cudd_SetSymmviolation ARGS((DdManager *dd, int symmviolation));
00574 EXTERN int Cudd_ReadArcviolation ARGS((DdManager *dd));
00575 EXTERN void Cudd_SetArcviolation ARGS((DdManager *dd, int arcviolation));
00576 EXTERN int Cudd_ReadPopulationSize ARGS((DdManager *dd));
00577 EXTERN void Cudd_SetPopulationSize ARGS((DdManager *dd, int populationSize));
00578 EXTERN int Cudd_ReadNumberXovers ARGS((DdManager *dd));
00579 EXTERN void Cudd_SetNumberXovers ARGS((DdManager *dd, int numberXovers));
00580 EXTERN long Cudd_ReadMemoryInUse ARGS((DdManager *dd));
00581 EXTERN int Cudd_PrintInfo ARGS((DdManager *dd, FILE *fp));
00582 EXTERN long Cudd_ReadPeakNodeCount ARGS((DdManager *dd));
00583 EXTERN int Cudd_ReadPeakLiveNodeCount ARGS((DdManager * dd));
00584 EXTERN long Cudd_ReadNodeCount ARGS((DdManager *dd));
00585 EXTERN long Cudd_zddReadNodeCount ARGS((DdManager *dd));
00586 EXTERN int Cudd_AddHook ARGS((DdManager *dd, int (*f)(DdManager *, char *, void *), Cudd_HookType where));
00587 EXTERN int Cudd_RemoveHook ARGS((DdManager *dd, int (*f)(DdManager *, char *, void *), Cudd_HookType where));
00588 EXTERN int Cudd_IsInHook ARGS((DdManager * dd, int (*f)(DdManager *, char *, void *), Cudd_HookType where));
00589 EXTERN int Cudd_StdPreReordHook ARGS((DdManager *dd, char *str, void *data));
00590 EXTERN int Cudd_StdPostReordHook ARGS((DdManager *dd, char *str, void *data));
00591 EXTERN int Cudd_EnableReorderingReporting ARGS((DdManager *dd));
00592 EXTERN int Cudd_DisableReorderingReporting ARGS((DdManager *dd));
00593 EXTERN int Cudd_ReorderingReporting ARGS((DdManager *dd));
00594 EXTERN Cudd_ErrorType Cudd_ReadErrorCode ARGS((DdManager *dd));
00595 EXTERN void Cudd_ClearErrorCode ARGS((DdManager *dd));
00596 EXTERN FILE * Cudd_ReadStdout ARGS((DdManager *dd));
00597 EXTERN void Cudd_SetStdout ARGS((DdManager *dd, FILE *fp));
00598 EXTERN FILE * Cudd_ReadStderr ARGS((DdManager *dd));
00599 EXTERN void Cudd_SetStderr ARGS((DdManager *dd, FILE *fp));
00600 EXTERN unsigned int Cudd_ReadNextReordering ARGS((DdManager *dd));
00601 EXTERN double Cudd_ReadSwapSteps ARGS((DdManager *dd));
00602 EXTERN unsigned int Cudd_ReadMaxLive ARGS((DdManager *dd));
00603 EXTERN void Cudd_SetMaxLive ARGS((DdManager *dd, unsigned int maxLive));
00604 EXTERN long Cudd_ReadMaxMemory ARGS((DdManager *dd));
00605 EXTERN void Cudd_SetMaxMemory ARGS((DdManager *dd, long maxMemory));
00606 EXTERN void Cudd_SetNextReordering ARGS((DdManager *dd, unsigned int next));
00607 EXTERN DdNode * Cudd_addExistAbstract ARGS((DdManager *manager, DdNode *f, DdNode *cube));
00608 EXTERN DdNode * Cudd_addUnivAbstract ARGS((DdManager *manager, DdNode *f, DdNode *cube));
00609 EXTERN DdNode * Cudd_addOrAbstract ARGS((DdManager *manager, DdNode *f, DdNode *cube));
00610 EXTERN DdNode * Cudd_addApply ARGS((DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g));
00611 EXTERN DdNode * Cudd_addPlus ARGS((DdManager *dd, DdNode **f, DdNode **g));
00612 EXTERN DdNode * Cudd_addTimes ARGS((DdManager *dd, DdNode **f, DdNode **g));
00613 EXTERN DdNode * Cudd_addThreshold ARGS((DdManager *dd, DdNode **f, DdNode **g));
00614 EXTERN DdNode * Cudd_addSetNZ ARGS((DdManager *dd, DdNode **f, DdNode **g));
00615 EXTERN DdNode * Cudd_addDivide ARGS((DdManager *dd, DdNode **f, DdNode **g));
00616 EXTERN DdNode * Cudd_addMinus ARGS((DdManager *dd, DdNode **f, DdNode **g));
00617 EXTERN DdNode * Cudd_addMinimum ARGS((DdManager *dd, DdNode **f, DdNode **g));
00618 EXTERN DdNode * Cudd_addMaximum ARGS((DdManager *dd, DdNode **f, DdNode **g));
00619 EXTERN DdNode * Cudd_addOneZeroMaximum ARGS((DdManager *dd, DdNode **f, DdNode **g));
00620 EXTERN DdNode * Cudd_addDiff ARGS((DdManager *dd, DdNode **f, DdNode **g));
00621 EXTERN DdNode * Cudd_addAgreement ARGS((DdManager *dd, DdNode **f, DdNode **g));
00622 EXTERN DdNode * Cudd_addOr ARGS((DdManager *dd, DdNode **f, DdNode **g));
00623 EXTERN DdNode * Cudd_addNand ARGS((DdManager *dd, DdNode **f, DdNode **g));
00624 EXTERN DdNode * Cudd_addNor ARGS((DdManager *dd, DdNode **f, DdNode **g));
00625 EXTERN DdNode * Cudd_addXor ARGS((DdManager *dd, DdNode **f, DdNode **g));
00626 EXTERN DdNode * Cudd_addXnor ARGS((DdManager *dd, DdNode **f, DdNode **g));
00627 EXTERN DdNode * Cudd_addFindMax ARGS((DdManager *dd, DdNode *f));
00628 EXTERN DdNode * Cudd_addFindMin ARGS((DdManager *dd, DdNode *f));
00629 EXTERN DdNode * Cudd_addIthBit ARGS((DdManager *dd, DdNode *f, int bit));
00630 EXTERN DdNode * Cudd_addScalarInverse ARGS((DdManager *dd, DdNode *f, DdNode *epsilon));
00631 EXTERN DdNode * Cudd_addIte ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *h));
00632 EXTERN DdNode * Cudd_addIteConstant ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *h));
00633 EXTERN DdNode * Cudd_addEvalConst ARGS((DdManager *dd, DdNode *f, DdNode *g));
00634 EXTERN int Cudd_addLeq ARGS((DdManager * dd, DdNode * f, DdNode * g));
00635 EXTERN DdNode * Cudd_addCmpl ARGS((DdManager *dd, DdNode *f));
00636 EXTERN DdNode * Cudd_addNegate ARGS((DdManager *dd, DdNode *f));
00637 EXTERN DdNode * Cudd_addRoundOff ARGS((DdManager *dd, DdNode *f, int N));
00638 EXTERN DdNode * Cudd_addWalsh ARGS((DdManager *dd, DdNode **x, DdNode **y, int n));
00639 EXTERN DdNode * Cudd_addResidue ARGS((DdManager *dd, int n, int m, int options, int top));
00640 EXTERN DdNode * Cudd_bddAndAbstract ARGS((DdManager *manager, DdNode *f, DdNode *g, DdNode *cube));
00641 EXTERN int Cudd_ApaNumberOfDigits ARGS((int binaryDigits));
00642 EXTERN DdApaNumber Cudd_NewApaNumber ARGS((int digits));
00643 EXTERN void Cudd_ApaCopy ARGS((int digits, DdApaNumber source, DdApaNumber dest));
00644 EXTERN DdApaDigit Cudd_ApaAdd ARGS((int digits, DdApaNumber a, DdApaNumber b, DdApaNumber sum));
00645 EXTERN DdApaDigit Cudd_ApaSubtract ARGS((int digits, DdApaNumber a, DdApaNumber b, DdApaNumber diff));
00646 EXTERN DdApaDigit Cudd_ApaShortDivision ARGS((int digits, DdApaNumber dividend, DdApaDigit divisor, DdApaNumber quotient));
00647 EXTERN unsigned int Cudd_ApaIntDivision ARGS((int  digits, DdApaNumber dividend, unsigned int  divisor, DdApaNumber  quotient));
00648 EXTERN void Cudd_ApaShiftRight ARGS((int digits, DdApaDigit in, DdApaNumber a, DdApaNumber b));
00649 EXTERN void Cudd_ApaSetToLiteral ARGS((int digits, DdApaNumber number, DdApaDigit literal));
00650 EXTERN void Cudd_ApaPowerOfTwo ARGS((int digits, DdApaNumber number, int power));
00651 EXTERN int Cudd_ApaCompare ARGS((int digitsFirst, DdApaNumber  first, int digitsSecond, DdApaNumber  second));
00652 EXTERN int Cudd_ApaCompareRatios ARGS ((int digitsFirst, DdApaNumber firstNum, unsigned int firstDen, int digitsSecond, DdApaNumber secondNum, unsigned int secondDen));
00653 EXTERN int Cudd_ApaPrintHex ARGS((FILE *fp, int digits, DdApaNumber number));
00654 EXTERN int Cudd_ApaPrintDecimal ARGS((FILE *fp, int digits, DdApaNumber number));
00655 EXTERN int Cudd_ApaPrintExponential ARGS((FILE * fp, int  digits, DdApaNumber  number, int precision));
00656 EXTERN DdApaNumber Cudd_ApaCountMinterm ARGS((DdManager *manager, DdNode *node, int nvars, int *digits));
00657 EXTERN int Cudd_ApaPrintMinterm ARGS((FILE *fp, DdManager *dd, DdNode *node, int nvars));
00658 EXTERN int Cudd_ApaPrintMintermExp ARGS((FILE * fp, DdManager * dd, DdNode * node, int  nvars, int precision));
00659 EXTERN int Cudd_ApaPrintDensity ARGS((FILE * fp, DdManager * dd, DdNode * node, int  nvars));
00660 EXTERN DdNode * Cudd_UnderApprox ARGS((DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality));
00661 EXTERN DdNode * Cudd_OverApprox ARGS((DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality));
00662 EXTERN DdNode * Cudd_RemapUnderApprox ARGS((DdManager *dd, DdNode *f, int numVars, int threshold, double quality));
00663 EXTERN DdNode * Cudd_RemapOverApprox ARGS((DdManager *dd, DdNode *f, int numVars, int threshold, double quality));
00664 EXTERN DdNode * Cudd_BiasedUnderApprox ARGS((DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0));
00665 EXTERN DdNode * Cudd_BiasedOverApprox ARGS((DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0));
00666 EXTERN DdNode * Cudd_bddExistAbstract ARGS((DdManager *manager, DdNode *f, DdNode *cube));
00667 EXTERN DdNode * Cudd_bddXorExistAbstract ARGS((DdManager *manager, DdNode *f, DdNode *g, DdNode *cube));
00668 EXTERN DdNode * Cudd_bddUnivAbstract ARGS((DdManager *manager, DdNode *f, DdNode *cube));
00669 EXTERN DdNode * Cudd_bddBooleanDiff ARGS((DdManager *manager, DdNode *f, int x));
00670 EXTERN int Cudd_bddVarIsDependent ARGS((DdManager *dd, DdNode *f, DdNode *var));
00671 EXTERN double Cudd_bddCorrelation ARGS((DdManager *manager, DdNode *f, DdNode *g));
00672 EXTERN double Cudd_bddCorrelationWeights ARGS((DdManager *manager, DdNode *f, DdNode *g, double *prob));
00673 EXTERN DdNode * Cudd_bddIte ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *h));
00674 EXTERN DdNode * Cudd_bddIteConstant ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *h));
00675 EXTERN DdNode * Cudd_bddIntersect ARGS((DdManager *dd, DdNode *f, DdNode *g));
00676 EXTERN DdNode * Cudd_bddAnd ARGS((DdManager *dd, DdNode *f, DdNode *g));
00677 EXTERN DdNode * Cudd_bddOr ARGS((DdManager *dd, DdNode *f, DdNode *g));
00678 EXTERN DdNode * Cudd_bddNand ARGS((DdManager *dd, DdNode *f, DdNode *g));
00679 EXTERN DdNode * Cudd_bddNor ARGS((DdManager *dd, DdNode *f, DdNode *g));
00680 EXTERN DdNode * Cudd_bddXor ARGS((DdManager *dd, DdNode *f, DdNode *g));
00681 EXTERN DdNode * Cudd_bddXnor ARGS((DdManager *dd, DdNode *f, DdNode *g));
00682 EXTERN int Cudd_bddLeq ARGS((DdManager *dd, DdNode *f, DdNode *g));
00683 EXTERN DdNode * Cudd_addBddThreshold ARGS((DdManager *dd, DdNode *f, CUDD_VALUE_TYPE value));
00684 EXTERN DdNode * Cudd_addBddStrictThreshold ARGS((DdManager *dd, DdNode *f, CUDD_VALUE_TYPE value));
00685 EXTERN DdNode * Cudd_addBddInterval ARGS((DdManager *dd, DdNode *f, CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper));
00686 EXTERN DdNode * Cudd_addBddIthBit ARGS((DdManager *dd, DdNode *f, int bit));
00687 EXTERN DdNode * Cudd_BddToAdd ARGS((DdManager *dd, DdNode *B));
00688 EXTERN DdNode * Cudd_addBddPattern ARGS((DdManager *dd, DdNode *f));
00689 EXTERN DdNode * Cudd_bddTransfer ARGS((DdManager *ddSource, DdManager *ddDestination, DdNode *f));
00690 EXTERN int Cudd_DebugCheck ARGS((DdManager *table));
00691 EXTERN int Cudd_CheckKeys ARGS((DdManager *table));
00692 EXTERN DdNode * Cudd_bddClippingAnd ARGS((DdManager *dd, DdNode *f, DdNode *g, int maxDepth, int direction));
00693 EXTERN DdNode * Cudd_bddClippingAndAbstract ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *cube, int maxDepth, int direction));
00694 EXTERN DdNode * Cudd_Cofactor ARGS((DdManager *dd, DdNode *f, DdNode *g));
00695 EXTERN DdNode * Cudd_bddCompose ARGS((DdManager *dd, DdNode *f, DdNode *g, int v));
00696 EXTERN DdNode * Cudd_addCompose ARGS((DdManager *dd, DdNode *f, DdNode *g, int v));
00697 EXTERN DdNode * Cudd_addPermute ARGS((DdManager *manager, DdNode *node, int *permut));
00698 EXTERN DdNode * Cudd_addSwapVariables ARGS((DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n));
00699 EXTERN DdNode * Cudd_bddPermute ARGS((DdManager *manager, DdNode *node, int *permut));
00700 EXTERN DdNode * Cudd_bddVarMap ARGS((DdManager *manager, DdNode *f));
00701 EXTERN int Cudd_SetVarMap ARGS((DdManager *manager, DdNode **x, DdNode **y, int n));
00702 EXTERN DdNode * Cudd_bddSwapVariables ARGS((DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n));
00703 EXTERN DdNode * Cudd_bddAdjPermuteX ARGS((DdManager *dd, DdNode *B, DdNode **x, int n));
00704 EXTERN DdNode * Cudd_addVectorCompose ARGS((DdManager *dd, DdNode *f, DdNode **vector));
00705 EXTERN DdNode * Cudd_addNonSimCompose ARGS((DdManager *dd, DdNode *f, DdNode **vector));
00706 EXTERN DdNode * Cudd_bddVectorCompose ARGS((DdManager *dd, DdNode *f, DdNode **vector));
00707 EXTERN int Cudd_bddApproxConjDecomp ARGS((DdManager *dd, DdNode *f, DdNode ***conjuncts));
00708 EXTERN int Cudd_bddApproxDisjDecomp ARGS((DdManager *dd, DdNode *f, DdNode ***disjuncts));
00709 EXTERN int Cudd_bddIterConjDecomp ARGS((DdManager *dd, DdNode *f, DdNode ***conjuncts));
00710 EXTERN int Cudd_bddIterDisjDecomp ARGS((DdManager *dd, DdNode *f, DdNode ***disjuncts));
00711 EXTERN int Cudd_bddGenConjDecomp ARGS((DdManager *dd, DdNode *f, DdNode ***conjuncts));
00712 EXTERN int Cudd_bddGenDisjDecomp ARGS((DdManager *dd, DdNode *f, DdNode ***disjuncts));
00713 EXTERN int Cudd_bddVarConjDecomp ARGS((DdManager *dd, DdNode * f, DdNode ***conjuncts));
00714 EXTERN int Cudd_bddVarDisjDecomp ARGS((DdManager *dd, DdNode * f, DdNode ***disjuncts));
00715 EXTERN DdNode * Cudd_FindEssential ARGS((DdManager *dd, DdNode *f));
00716 EXTERN int Cudd_bddIsVarEssential ARGS((DdManager *manager, DdNode *f, int id, int phase));
00717 EXTERN int Cudd_DumpBlif ARGS((DdManager *dd, int n, DdNode **f, char **inames, char **onames, char *mname, FILE *fp));
00718 EXTERN int Cudd_DumpBlifBody ARGS((DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp));
00719 EXTERN int Cudd_DumpDot ARGS((DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp));
00720 EXTERN int Cudd_DumpDaVinci ARGS((DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp));
00721 EXTERN int Cudd_DumpDDcal ARGS((DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp));
00722 EXTERN int Cudd_DumpFactoredForm ARGS((DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp));
00723 EXTERN DdNode * Cudd_bddConstrain ARGS((DdManager *dd, DdNode *f, DdNode *c));
00724 EXTERN DdNode * Cudd_bddRestrict ARGS((DdManager *dd, DdNode *f, DdNode *c));
00725 EXTERN DdNode * Cudd_addConstrain ARGS((DdManager *dd, DdNode *f, DdNode *c));
00726 EXTERN DdNode ** Cudd_bddConstrainDecomp ARGS((DdManager *dd, DdNode *f));
00727 EXTERN DdNode * Cudd_addRestrict ARGS((DdManager *dd, DdNode *f, DdNode *c));
00728 EXTERN DdNode ** Cudd_bddCharToVect ARGS((DdManager *dd, DdNode *f));
00729 EXTERN DdNode * Cudd_bddLICompaction ARGS((DdManager *dd, DdNode *f, DdNode *c));
00730 EXTERN DdNode * Cudd_bddSqueeze ARGS((DdManager *dd, DdNode *l, DdNode *u));
00731 EXTERN DdNode * Cudd_bddMinimize ARGS((DdManager *dd, DdNode *f, DdNode *c));
00732 EXTERN DdNode * Cudd_SubsetCompress ARGS((DdManager *dd, DdNode *f, int nvars, int threshold));
00733 EXTERN DdNode * Cudd_SupersetCompress ARGS((DdManager *dd, DdNode *f, int nvars, int threshold));
00734 EXTERN MtrNode * Cudd_MakeTreeNode ARGS((DdManager *dd, unsigned int low, unsigned int size, unsigned int type));
00735 EXTERN int Cudd_addHarwell ARGS((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));
00736 EXTERN DdManager * Cudd_Init ARGS((unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory));
00737 EXTERN void Cudd_Quit ARGS((DdManager *unique));
00738 EXTERN int Cudd_PrintLinear ARGS((DdManager *table));
00739 EXTERN int Cudd_ReadLinear ARGS((DdManager *table, int x, int y));
00740 EXTERN DdNode * Cudd_bddLiteralSetIntersection ARGS((DdManager *dd, DdNode *f, DdNode *g));
00741 EXTERN DdNode * Cudd_addMatrixMultiply ARGS((DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz));
00742 EXTERN DdNode * Cudd_addTimesPlus ARGS((DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz));
00743 EXTERN DdNode * Cudd_addTriangle ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode **z, int nz));
00744 EXTERN DdNode * Cudd_PrioritySelect ARGS((DdManager *dd, DdNode *R, DdNode **x, DdNode **y, DdNode **z, DdNode *Pi, int n, DdNode * (*)(DdManager *, int, DdNode **, DdNode **, DdNode **)));
00745 EXTERN DdNode * Cudd_Xgty ARGS((DdManager *dd, int N, DdNode **z, DdNode **x, DdNode **y));
00746 EXTERN DdNode * Cudd_Xeqy ARGS((DdManager *dd, int N, DdNode **x, DdNode **y));
00747 EXTERN DdNode * Cudd_addXeqy ARGS((DdManager *dd, int N, DdNode **x, DdNode **y));
00748 EXTERN DdNode * Cudd_Dxygtdxz ARGS((DdManager *dd, int N, DdNode **x, DdNode **y, DdNode **z));
00749 EXTERN DdNode * Cudd_Dxygtdyz ARGS((DdManager *dd, int N, DdNode **x, DdNode **y, DdNode **z));
00750 EXTERN DdNode * Cudd_CProjection ARGS((DdManager *dd, DdNode *R, DdNode *Y));
00751 EXTERN DdNode * Cudd_addHamming ARGS((DdManager *dd, DdNode **xVars, DdNode **yVars, int nVars));
00752 EXTERN int Cudd_MinHammingDist ARGS((DdManager *dd, DdNode *f, int *minterm, int upperBound));
00753 EXTERN int Cudd_addRead ARGS((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));
00754 EXTERN int Cudd_bddRead ARGS((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));
00755 EXTERN void Cudd_Ref ARGS((DdNode *n));
00756 EXTERN void Cudd_RecursiveDeref ARGS((DdManager *table, DdNode *n));
00757 EXTERN void Cudd_IterDerefBdd ARGS((DdManager *table, DdNode *n));
00758 EXTERN void Cudd_DelayedDerefBdd ARGS((DdManager * table, DdNode * n));
00759 EXTERN void Cudd_RecursiveDerefZdd ARGS((DdManager *table, DdNode *n));
00760 EXTERN void Cudd_Deref ARGS((DdNode *node));
00761 EXTERN int Cudd_CheckZeroRef ARGS((DdManager *manager));
00762 EXTERN int Cudd_ReduceHeap ARGS((DdManager *table, Cudd_ReorderingType heuristic, int minsize));
00763 EXTERN int Cudd_ShuffleHeap ARGS((DdManager *table, int *permutation));
00764 EXTERN DdNode * Cudd_Eval ARGS((DdManager *dd, DdNode *f, int *inputs));
00765 EXTERN DdNode * Cudd_ShortestPath ARGS((DdManager *manager, DdNode *f, int *weight, int *support, int *length));
00766 EXTERN DdNode * Cudd_LargestCube ARGS((DdManager *manager, DdNode *f, int *length));
00767 EXTERN int Cudd_ShortestLength ARGS((DdManager *manager, DdNode *f, int *weight));
00768 EXTERN DdNode * Cudd_Decreasing ARGS((DdManager *dd, DdNode *f, int i));
00769 EXTERN DdNode * Cudd_Increasing ARGS((DdManager *dd, DdNode *f, int i));
00770 EXTERN int Cudd_EquivDC ARGS((DdManager *dd, DdNode *F, DdNode *G, DdNode *D));
00771 EXTERN int Cudd_EqualSupNorm ARGS((DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr));
00772 EXTERN double * Cudd_CofMinterm ARGS((DdManager *dd, DdNode *node));
00773 EXTERN DdNode * Cudd_SolveEqn ARGS((DdManager * bdd, DdNode *F, DdNode *Y, DdNode **G, int **yIndex, int n));
00774 EXTERN DdNode * Cudd_VerifySol ARGS((DdManager * bdd, DdNode *F, DdNode **G, int *yIndex, int n));
00775 EXTERN DdNode * Cudd_SplitSet ARGS((DdManager *manager, DdNode *S, DdNode **xVars, int n, double m));
00776 EXTERN DdNode * Cudd_SubsetHeavyBranch ARGS((DdManager *dd, DdNode *f, int numVars, int threshold));
00777 EXTERN DdNode * Cudd_SupersetHeavyBranch ARGS((DdManager *dd, DdNode *f, int numVars, int threshold));
00778 EXTERN DdNode * Cudd_SubsetShortPaths ARGS((DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit));
00779 EXTERN DdNode * Cudd_SupersetShortPaths ARGS((DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit));
00780 EXTERN void Cudd_SymmProfile ARGS((DdManager *table, int lower, int upper));
00781 EXTERN unsigned int Cudd_Prime ARGS((unsigned int p));
00782 EXTERN int Cudd_PrintMinterm ARGS((DdManager *manager, DdNode *node));
00783 EXTERN int Cudd_PrintDebug ARGS((DdManager *dd, DdNode *f, int n, int pr));
00784 EXTERN int Cudd_DagSize ARGS((DdNode *node));
00785 EXTERN int Cudd_EstimateCofactor ARGS((DdManager *dd, DdNode * node, int i, int phase));
00786 EXTERN int Cudd_EstimateCofactorSimple ARGS((DdNode * node, int i));
00787 EXTERN int Cudd_SharingSize ARGS((DdNode **nodeArray, int n));
00788 EXTERN double Cudd_CountMinterm ARGS((DdManager *manager, DdNode *node, int nvars));
00789 EXTERN double Cudd_CountPath ARGS((DdNode *node));
00790 EXTERN DdNode * Cudd_Support ARGS((DdManager *dd, DdNode *f));
00791 EXTERN int Cudd_SupportSize ARGS((DdManager *dd, DdNode *f));
00792 EXTERN DdNode * Cudd_VectorSupport ARGS((DdManager *dd, DdNode **F, int n));
00793 EXTERN int Cudd_VectorSupportSize ARGS((DdManager *dd, DdNode **F, int n));
00794 EXTERN int Cudd_ClassifySupport ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode **common, DdNode **onlyF, DdNode **onlyG));
00795 EXTERN int Cudd_CountLeaves ARGS((DdNode *node));
00796 EXTERN int Cudd_bddPickOneCube ARGS((DdManager *ddm, DdNode *node, char *string));
00797 EXTERN DdNode * Cudd_bddPickOneMinterm ARGS((DdManager *dd, DdNode *f, DdNode **vars, int n));
00798 EXTERN DdNode ** Cudd_bddPickArbitraryMinterms ARGS((DdManager *dd, DdNode *f, DdNode **vars, int n, int k));
00799 EXTERN DdGen * Cudd_FirstCube ARGS((DdManager *dd, DdNode *f, int **cube, CUDD_VALUE_TYPE *value));
00800 EXTERN int Cudd_NextCube ARGS((DdGen *gen, int **cube, CUDD_VALUE_TYPE *value));
00801 EXTERN DdNode * Cudd_bddComputeCube ARGS((DdManager *dd, DdNode **vars, int *phase, int n));
00802 EXTERN DdNode * Cudd_addComputeCube ARGS((DdManager *dd, DdNode **vars, int *phase, int n));
00803 EXTERN DdGen * Cudd_FirstNode ARGS((DdManager *dd, DdNode *f, DdNode **node));
00804 EXTERN int Cudd_NextNode ARGS((DdGen *gen, DdNode **node));
00805 EXTERN int Cudd_GenFree ARGS((DdGen *gen));
00806 EXTERN int Cudd_IsGenEmpty ARGS((DdGen *gen));
00807 EXTERN DdNode * Cudd_IndicesToCube ARGS((DdManager *dd, int *array, int n));
00808 EXTERN void Cudd_PrintVersion ARGS((FILE *fp));
00809 EXTERN double Cudd_AverageDistance ARGS((DdManager *dd));
00810 EXTERN long Cudd_Random ARGS(());
00811 EXTERN void Cudd_Srandom ARGS((long seed));
00812 EXTERN double Cudd_Density ARGS((DdManager *dd, DdNode *f, int nvars));
00813 EXTERN void Cudd_OutOfMem ARGS((long size));
00814 EXTERN int Cudd_zddCount ARGS((DdManager *zdd, DdNode *P));
00815 EXTERN double Cudd_zddCountDouble ARGS((DdManager *zdd, DdNode *P));
00816 EXTERN DdNode * Cudd_zddProduct ARGS((DdManager *dd, DdNode *f, DdNode *g));
00817 EXTERN DdNode * Cudd_zddUnateProduct ARGS((DdManager *dd, DdNode *f, DdNode *g));
00818 EXTERN DdNode * Cudd_zddWeakDiv ARGS((DdManager *dd, DdNode *f, DdNode *g));
00819 EXTERN DdNode * Cudd_zddDivide ARGS((DdManager *dd, DdNode *f, DdNode *g));
00820 EXTERN DdNode * Cudd_zddWeakDivF ARGS((DdManager *dd, DdNode *f, DdNode *g));
00821 EXTERN DdNode * Cudd_zddDivideF ARGS((DdManager *dd, DdNode *f, DdNode *g));
00822 EXTERN DdNode * Cudd_zddComplement ARGS((DdManager *dd, DdNode *node));
00823 EXTERN MtrNode * Cudd_MakeZddTreeNode ARGS((DdManager *dd, unsigned int low, unsigned int size, unsigned int type));
00824 EXTERN DdNode * Cudd_zddIsop ARGS((DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I));
00825 EXTERN DdNode * Cudd_bddIsop ARGS((DdManager *dd, DdNode *L, DdNode *U));
00826 EXTERN DdNode * Cudd_MakeBddFromZddCover ARGS((DdManager *dd, DdNode *node));
00827 EXTERN int Cudd_zddDagSize ARGS((DdNode *p_node));
00828 EXTERN double Cudd_zddCountMinterm ARGS((DdManager *zdd, DdNode *node, int path));
00829 EXTERN void Cudd_zddPrintSubtable ARGS((DdManager *table));
00830 EXTERN DdNode * Cudd_zddPortFromBdd ARGS((DdManager *dd, DdNode *B));
00831 EXTERN DdNode * Cudd_zddPortToBdd ARGS((DdManager *dd, DdNode *f));
00832 EXTERN int Cudd_zddReduceHeap ARGS((DdManager *table, Cudd_ReorderingType heuristic, int minsize));
00833 EXTERN int Cudd_zddShuffleHeap ARGS((DdManager *table, int *permutation));
00834 EXTERN DdNode * Cudd_zddIte ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *h));
00835 EXTERN DdNode * Cudd_zddUnion ARGS((DdManager *dd, DdNode *P, DdNode *Q));
00836 EXTERN DdNode * Cudd_zddIntersect ARGS((DdManager *dd, DdNode *P, DdNode *Q));
00837 EXTERN DdNode * Cudd_zddDiff ARGS((DdManager *dd, DdNode *P, DdNode *Q));
00838 EXTERN DdNode * Cudd_zddDiffConst ARGS((DdManager *zdd, DdNode *P, DdNode *Q));
00839 EXTERN DdNode * Cudd_zddSubset1 ARGS((DdManager *dd, DdNode *P, int var));
00840 EXTERN DdNode * Cudd_zddSubset0 ARGS((DdManager *dd, DdNode *P, int var));
00841 EXTERN DdNode * Cudd_zddChange ARGS((DdManager *dd, DdNode *P, int var));
00842 EXTERN void Cudd_zddSymmProfile ARGS((DdManager *table, int lower, int upper));
00843 EXTERN int Cudd_zddPrintMinterm ARGS((DdManager *zdd, DdNode *node));
00844 EXTERN int Cudd_zddPrintCover ARGS((DdManager *zdd, DdNode *node));
00845 EXTERN int Cudd_zddPrintDebug ARGS((DdManager *zdd, DdNode *f, int n, int pr));
00846 EXTERN int Cudd_zddDumpDot ARGS((DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp));
00847 
00850 #endif /* _CUDD */