00001
00030 #ifndef _CUDD
00031 #define _CUDD
00032
00033
00034
00035
00036
00037 #include "mtr.h"
00038 #include "epd.h"
00039
00040
00041
00042
00043
00044 #define CUDD_VERSION "2.3.1"
00045
00046 #ifndef SIZEOF_VOID_P
00047 #define SIZEOF_VOID_P 4
00048 #endif
00049 #ifndef SIZEOF_INT
00050 #define SIZEOF_INT 4
00051 #endif
00052 #ifndef SIZEOF_LONG
00053 #define SIZEOF_LONG 4
00054 #endif
00055
00056 #ifndef TRUE
00057 #define TRUE 1
00058 #endif
00059 #ifndef FALSE
00060 #define FALSE 0
00061 #endif
00062
00063 #define CUDD_VALUE_TYPE double
00064 #define CUDD_OUT_OF_MEM -1
00065
00066 #define CUDD_UNIQUE_SLOTS 256
00067 #define CUDD_CACHE_SLOTS 262144
00068
00069
00070 #define CUDD_RESIDUE_DEFAULT 0
00071 #define CUDD_RESIDUE_MSB 1
00072 #define CUDD_RESIDUE_TC 2
00073
00074
00075
00076
00077
00078 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00079 #define CUDD_MAXINDEX (((DdHalfWord) ~0) >> 1)
00080 #else
00081 #define CUDD_MAXINDEX ((DdHalfWord) ~0)
00082 #endif
00083
00084
00085
00086 #define CUDD_CONST_INDEX CUDD_MAXINDEX
00087
00088
00089
00090
00091
00092
00093 #define DD_APA_BITS 16
00094 #define DD_APA_BASE (1 << DD_APA_BITS)
00095 #define DD_APA_MASK (DD_APA_BASE - 1)
00096 #define DD_APA_HEXPRINT "%04x"
00097
00098
00099
00100
00101
00102
00103
00104
00105
00106
00114 typedef enum {
00115 CUDD_REORDER_SAME,
00116 CUDD_REORDER_NONE,
00117 CUDD_REORDER_RANDOM,
00118 CUDD_REORDER_RANDOM_PIVOT,
00119 CUDD_REORDER_SIFT,
00120 CUDD_REORDER_SIFT_CONVERGE,
00121 CUDD_REORDER_SYMM_SIFT,
00122 CUDD_REORDER_SYMM_SIFT_CONV,
00123 CUDD_REORDER_WINDOW2,
00124 CUDD_REORDER_WINDOW3,
00125 CUDD_REORDER_WINDOW4,
00126 CUDD_REORDER_WINDOW2_CONV,
00127 CUDD_REORDER_WINDOW3_CONV,
00128 CUDD_REORDER_WINDOW4_CONV,
00129 CUDD_REORDER_GROUP_SIFT,
00130 CUDD_REORDER_GROUP_SIFT_CONV,
00131 CUDD_REORDER_ANNEALING,
00132 CUDD_REORDER_GENETIC,
00133 CUDD_REORDER_LINEAR,
00134 CUDD_REORDER_LINEAR_CONVERGE,
00135 CUDD_REORDER_LAZY_SIFT,
00136 CUDD_REORDER_EXACT
00137 } Cudd_ReorderingType;
00138
00139
00147 typedef enum {
00148 CUDD_NO_CHECK,
00149 CUDD_GROUP_CHECK,
00150 CUDD_GROUP_CHECK2,
00151 CUDD_GROUP_CHECK3,
00152 CUDD_GROUP_CHECK4,
00153 CUDD_GROUP_CHECK5,
00154 CUDD_GROUP_CHECK6,
00155 CUDD_GROUP_CHECK7,
00156 CUDD_GROUP_CHECK8,
00157 CUDD_GROUP_CHECK9
00158 } Cudd_AggregationType;
00159
00160
00168 typedef enum {
00169 CUDD_PRE_GC_HOOK,
00170 CUDD_POST_GC_HOOK,
00171 CUDD_PRE_REORDERING_HOOK,
00172 CUDD_POST_REORDERING_HOOK
00173 } Cudd_HookType;
00174
00175
00183 typedef enum {
00184 CUDD_NO_ERROR,
00185 CUDD_MEMORY_OUT,
00186 CUDD_TOO_MANY_NODES,
00187 CUDD_MAX_MEM_EXCEEDED,
00188 CUDD_INVALID_ARG,
00189 CUDD_INTERNAL_ERROR
00190 } Cudd_ErrorType;
00191
00192
00200 typedef enum {
00201 CUDD_LAZY_NONE,
00202 CUDD_LAZY_SOFT_GROUP,
00203 CUDD_LAZY_HARD_GROUP,
00204 CUDD_LAZY_UNGROUP
00205 } Cudd_LazyGroupType;
00206
00207
00215 typedef enum {
00216 CUDD_VAR_PRIMARY_INPUT,
00217 CUDD_VAR_PRESENT_STATE,
00218 CUDD_VAR_NEXT_STATE
00219 } Cudd_VariableType;
00220
00221
00222 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00223 typedef unsigned int DdHalfWord;
00224 #else
00225 typedef unsigned short DdHalfWord;
00226 #endif
00227
00228 #ifdef __osf__
00229 #pragma pointer_size save
00230 #pragma pointer_size short
00231 #endif
00232
00233 typedef struct DdNode DdNode;
00234
00235 typedef struct DdChildren {
00236 struct DdNode *T;
00237 struct DdNode *E;
00238 } DdChildren;
00239
00240
00241 struct DdNode {
00242 DdHalfWord index;
00243 DdHalfWord ref;
00244 DdNode *next;
00245 union {
00246 CUDD_VALUE_TYPE value;
00247 DdChildren kids;
00248 } type;
00249 };
00250
00251 #ifdef __osf__
00252 #pragma pointer_size restore
00253 #endif
00254
00255 typedef struct DdManager DdManager;
00256
00257 typedef struct DdGen DdGen;
00258
00259
00260
00261 typedef unsigned short int DdApaDigit;
00262 typedef unsigned long int DdApaDoubleDigit;
00263 typedef DdApaDigit * DdApaNumber;
00264
00265
00266
00267
00268
00269
00270
00271
00272
00273
00274
00289 #define Cudd_IsConstant(node) ((Cudd_Regular(node))->index == CUDD_CONST_INDEX)
00290
00291
00304 #define Cudd_Not(node) ((DdNode *)((long)(node) ^ 01))
00305
00306
00320 #define Cudd_NotCond(node,c) ((DdNode *)((long)(node) ^ (c)))
00321
00322
00334 #define Cudd_Regular(node) ((DdNode *)((unsigned long)(node) & ~01))
00335
00336
00348 #define Cudd_Complement(node) ((DdNode *)((unsigned long)(node) | 01))
00349
00350
00362 #define Cudd_IsComplement(node) ((int) ((long) (node) & 01))
00363
00364
00377 #define Cudd_T(node) ((Cudd_Regular(node))->type.kids.T)
00378
00379
00392 #define Cudd_E(node) ((Cudd_Regular(node))->type.kids.E)
00393
00394
00407 #define Cudd_V(node) ((Cudd_Regular(node))->type.value)
00408
00409
00424 #define Cudd_ReadIndex(dd,index) (Cudd_ReadPerm(dd,index))
00425
00426
00456 #define Cudd_ForeachCube(manager, f, gen, cube, value)\
00457 for((gen) = Cudd_FirstCube(manager, f, &cube, &value);\
00458 Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
00459 (void) Cudd_NextCube(gen, &cube, &value))
00460
00461
00490 #define Cudd_ForeachNode(manager, f, gen, node)\
00491 for((gen) = Cudd_FirstNode(manager, f, &node);\
00492 Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
00493 (void) Cudd_NextNode(gen, &node))
00494
00495
00524 #define Cudd_zddForeachPath(manager, f, gen, path)\
00525 for((gen) = Cudd_zddFirstPath(manager, f, &path);\
00526 Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
00527 (void) Cudd_zddNextPath(gen, &path))
00528
00529
00530
00531 #ifndef EXTERN
00532 # ifdef __cplusplus
00533 # define EXTERN extern "C"
00534 # else
00535 # define EXTERN extern
00536 # endif
00537 #endif
00538 #ifndef ARGS
00539 # if defined(__STDC__) || defined(__cplusplus)
00540 # define ARGS(protos) protos
00541 # else
00542 # define ARGS(protos) ()
00543 # endif
00544 #endif
00545
00546
00549
00550
00551
00552
00553 EXTERN DdNode * Cudd_addNewVar ARGS((DdManager *dd));
00554 EXTERN DdNode * Cudd_addNewVarAtLevel ARGS((DdManager *dd, int level));
00555 EXTERN DdNode * Cudd_bddNewVar ARGS((DdManager *dd));
00556 EXTERN DdNode * Cudd_bddNewVarAtLevel ARGS((DdManager *dd, int level));
00557 EXTERN DdNode * Cudd_addIthVar ARGS((DdManager *dd, int i));
00558 EXTERN DdNode * Cudd_bddIthVar ARGS((DdManager *dd, int i));
00559 EXTERN DdNode * Cudd_zddIthVar ARGS((DdManager *dd, int i));
00560 EXTERN int Cudd_zddVarsFromBddVars ARGS((DdManager *dd, int multiplicity));
00561 EXTERN DdNode * Cudd_addConst ARGS((DdManager *dd, CUDD_VALUE_TYPE c));
00562 EXTERN int Cudd_IsNonConstant ARGS((DdNode *f));
00563 EXTERN void Cudd_AutodynEnable ARGS((DdManager *unique, Cudd_ReorderingType method));
00564 EXTERN void Cudd_AutodynDisable ARGS((DdManager *unique));
00565 EXTERN int Cudd_ReorderingStatus ARGS((DdManager *unique, Cudd_ReorderingType *method));
00566 EXTERN void Cudd_AutodynEnableZdd ARGS((DdManager *unique, Cudd_ReorderingType method));
00567 EXTERN void Cudd_AutodynDisableZdd ARGS((DdManager *unique));
00568 EXTERN int Cudd_ReorderingStatusZdd ARGS((DdManager *unique, Cudd_ReorderingType *method));
00569 EXTERN int Cudd_zddRealignmentEnabled ARGS((DdManager *unique));
00570 EXTERN void Cudd_zddRealignEnable ARGS((DdManager *unique));
00571 EXTERN void Cudd_zddRealignDisable ARGS((DdManager *unique));
00572 EXTERN int Cudd_bddRealignmentEnabled ARGS((DdManager *unique));
00573 EXTERN void Cudd_bddRealignEnable ARGS((DdManager *unique));
00574 EXTERN void Cudd_bddRealignDisable ARGS((DdManager *unique));
00575 EXTERN DdNode * Cudd_ReadOne ARGS((DdManager *dd));
00576 EXTERN DdNode * Cudd_ReadZddOne ARGS((DdManager *dd, int i));
00577 EXTERN DdNode * Cudd_ReadZero ARGS((DdManager *dd));
00578 EXTERN DdNode * Cudd_ReadLogicZero ARGS((DdManager *dd));
00579 EXTERN DdNode * Cudd_ReadPlusInfinity ARGS((DdManager *dd));
00580 EXTERN DdNode * Cudd_ReadMinusInfinity ARGS((DdManager *dd));
00581 EXTERN DdNode * Cudd_ReadBackground ARGS((DdManager *dd));
00582 EXTERN void Cudd_SetBackground ARGS((DdManager *dd, DdNode *bck));
00583 EXTERN unsigned int Cudd_ReadCacheSlots ARGS((DdManager *dd));
00584 EXTERN double Cudd_ReadCacheUsedSlots ARGS((DdManager * dd));
00585 EXTERN double Cudd_ReadCacheLookUps ARGS((DdManager *dd));
00586 EXTERN double Cudd_ReadCacheHits ARGS((DdManager *dd));
00587 EXTERN double Cudd_ReadRecursiveCalls ARGS ((DdManager * dd));
00588 EXTERN unsigned int Cudd_ReadMinHit ARGS((DdManager *dd));
00589 EXTERN void Cudd_SetMinHit ARGS((DdManager *dd, unsigned int hr));
00590 EXTERN unsigned int Cudd_ReadLooseUpTo ARGS((DdManager *dd));
00591 EXTERN void Cudd_SetLooseUpTo ARGS((DdManager *dd, unsigned int lut));
00592 EXTERN unsigned int Cudd_ReadMaxCache ARGS((DdManager *dd));
00593 EXTERN unsigned int Cudd_ReadMaxCacheHard ARGS((DdManager *dd));
00594 EXTERN void Cudd_SetMaxCacheHard ARGS((DdManager *dd, unsigned int mc));
00595 EXTERN int Cudd_ReadSize ARGS((DdManager *dd));
00596 EXTERN int Cudd_ReadZddSize ARGS((DdManager *dd));
00597 EXTERN unsigned int Cudd_ReadSlots ARGS((DdManager *dd));
00598 EXTERN double Cudd_ReadUsedSlots ARGS((DdManager * dd));
00599 EXTERN double Cudd_ExpectedUsedSlots ARGS((DdManager * dd));
00600 EXTERN unsigned int Cudd_ReadKeys ARGS((DdManager *dd));
00601 EXTERN unsigned int Cudd_ReadDead ARGS((DdManager *dd));
00602 EXTERN unsigned int Cudd_ReadMinDead ARGS((DdManager *dd));
00603 EXTERN int Cudd_ReadReorderings ARGS((DdManager *dd));
00604 EXTERN long Cudd_ReadReorderingTime ARGS((DdManager * dd));
00605 EXTERN int Cudd_ReadGarbageCollections ARGS((DdManager * dd));
00606 EXTERN long Cudd_ReadGarbageCollectionTime ARGS((DdManager * dd));
00607 EXTERN double Cudd_ReadNodesFreed ARGS((DdManager * dd));
00608 EXTERN double Cudd_ReadNodesDropped ARGS((DdManager * dd));
00609 EXTERN double Cudd_ReadUniqueLookUps ARGS((DdManager * dd));
00610 EXTERN double Cudd_ReadUniqueLinks ARGS((DdManager * dd));
00611 EXTERN int Cudd_ReadSiftMaxVar ARGS((DdManager *dd));
00612 EXTERN void Cudd_SetSiftMaxVar ARGS((DdManager *dd, int smv));
00613 EXTERN int Cudd_ReadSiftMaxSwap ARGS((DdManager *dd));
00614 EXTERN void Cudd_SetSiftMaxSwap ARGS((DdManager *dd, int sms));
00615 EXTERN double Cudd_ReadMaxGrowth ARGS((DdManager *dd));
00616 EXTERN void Cudd_SetMaxGrowth ARGS((DdManager *dd, double mg));
00617 EXTERN double Cudd_ReadMaxGrowthAlternate ARGS((DdManager * dd));
00618 EXTERN void Cudd_SetMaxGrowthAlternate ARGS((DdManager * dd, double mg));
00619 EXTERN int Cudd_ReadReorderingCycle ARGS((DdManager * dd));
00620 EXTERN void Cudd_SetReorderingCycle ARGS((DdManager * dd, int cycle));
00621 EXTERN MtrNode * Cudd_ReadTree ARGS((DdManager *dd));
00622 EXTERN void Cudd_SetTree ARGS((DdManager *dd, MtrNode *tree));
00623 EXTERN void Cudd_FreeTree ARGS((DdManager *dd));
00624 EXTERN MtrNode * Cudd_ReadZddTree ARGS((DdManager *dd));
00625 EXTERN void Cudd_SetZddTree ARGS((DdManager *dd, MtrNode *tree));
00626 EXTERN void Cudd_FreeZddTree ARGS((DdManager *dd));
00627 EXTERN unsigned int Cudd_NodeReadIndex ARGS((DdNode *node));
00628 EXTERN int Cudd_ReadPerm ARGS((DdManager *dd, int i));
00629 EXTERN int Cudd_ReadPermZdd ARGS((DdManager *dd, int i));
00630 EXTERN int Cudd_ReadInvPerm ARGS((DdManager *dd, int i));
00631 EXTERN int Cudd_ReadInvPermZdd ARGS((DdManager *dd, int i));
00632 EXTERN DdNode * Cudd_ReadVars ARGS((DdManager *dd, int i));
00633 EXTERN CUDD_VALUE_TYPE Cudd_ReadEpsilon ARGS((DdManager *dd));
00634 EXTERN void Cudd_SetEpsilon ARGS((DdManager *dd, CUDD_VALUE_TYPE ep));
00635 EXTERN Cudd_AggregationType Cudd_ReadGroupcheck ARGS((DdManager *dd));
00636 EXTERN void Cudd_SetGroupcheck ARGS((DdManager *dd, Cudd_AggregationType gc));
00637 EXTERN int Cudd_GarbageCollectionEnabled ARGS((DdManager *dd));
00638 EXTERN void Cudd_EnableGarbageCollection ARGS((DdManager *dd));
00639 EXTERN void Cudd_DisableGarbageCollection ARGS((DdManager *dd));
00640 EXTERN int Cudd_DeadAreCounted ARGS((DdManager *dd));
00641 EXTERN void Cudd_TurnOnCountDead ARGS((DdManager *dd));
00642 EXTERN void Cudd_TurnOffCountDead ARGS((DdManager *dd));
00643 EXTERN int Cudd_ReadRecomb ARGS((DdManager *dd));
00644 EXTERN void Cudd_SetRecomb ARGS((DdManager *dd, int recomb));
00645 EXTERN int Cudd_ReadSymmviolation ARGS((DdManager *dd));
00646 EXTERN void Cudd_SetSymmviolation ARGS((DdManager *dd, int symmviolation));
00647 EXTERN int Cudd_ReadArcviolation ARGS((DdManager *dd));
00648 EXTERN void Cudd_SetArcviolation ARGS((DdManager *dd, int arcviolation));
00649 EXTERN int Cudd_ReadPopulationSize ARGS((DdManager *dd));
00650 EXTERN void Cudd_SetPopulationSize ARGS((DdManager *dd, int populationSize));
00651 EXTERN int Cudd_ReadNumberXovers ARGS((DdManager *dd));
00652 EXTERN void Cudd_SetNumberXovers ARGS((DdManager *dd, int numberXovers));
00653 EXTERN long Cudd_ReadMemoryInUse ARGS((DdManager *dd));
00654 EXTERN int Cudd_PrintInfo ARGS((DdManager *dd, FILE *fp));
00655 EXTERN long Cudd_ReadPeakNodeCount ARGS((DdManager *dd));
00656 EXTERN int Cudd_ReadPeakLiveNodeCount ARGS((DdManager * dd));
00657 EXTERN long Cudd_ReadNodeCount ARGS((DdManager *dd));
00658 EXTERN long Cudd_zddReadNodeCount ARGS((DdManager *dd));
00659 EXTERN int Cudd_AddHook ARGS((DdManager *dd, int (*f)(DdManager *, char *, void *), Cudd_HookType where));
00660 EXTERN int Cudd_RemoveHook ARGS((DdManager *dd, int (*f)(DdManager *, char *, void *), Cudd_HookType where));
00661 EXTERN int Cudd_IsInHook ARGS((DdManager * dd, int (*f)(DdManager *, char *, void *), Cudd_HookType where));
00662 EXTERN int Cudd_StdPreReordHook ARGS((DdManager *dd, char *str, void *data));
00663 EXTERN int Cudd_StdPostReordHook ARGS((DdManager *dd, char *str, void *data));
00664 EXTERN int Cudd_EnableReorderingReporting ARGS((DdManager *dd));
00665 EXTERN int Cudd_DisableReorderingReporting ARGS((DdManager *dd));
00666 EXTERN int Cudd_ReorderingReporting ARGS((DdManager *dd));
00667 EXTERN Cudd_ErrorType Cudd_ReadErrorCode ARGS((DdManager *dd));
00668 EXTERN void Cudd_ClearErrorCode ARGS((DdManager *dd));
00669 EXTERN FILE * Cudd_ReadStdout ARGS((DdManager *dd));
00670 EXTERN void Cudd_SetStdout ARGS((DdManager *dd, FILE *fp));
00671 EXTERN FILE * Cudd_ReadStderr ARGS((DdManager *dd));
00672 EXTERN void Cudd_SetStderr ARGS((DdManager *dd, FILE *fp));
00673 EXTERN unsigned int Cudd_ReadNextReordering ARGS((DdManager *dd));
00674 EXTERN void Cudd_SetNextReordering ARGS((DdManager *dd, unsigned int next));
00675 EXTERN double Cudd_ReadSwapSteps ARGS((DdManager *dd));
00676 EXTERN unsigned int Cudd_ReadMaxLive ARGS((DdManager *dd));
00677 EXTERN void Cudd_SetMaxLive ARGS((DdManager *dd, unsigned int maxLive));
00678 EXTERN long Cudd_ReadMaxMemory ARGS((DdManager *dd));
00679 EXTERN void Cudd_SetMaxMemory ARGS((DdManager *dd, long maxMemory));
00680 EXTERN int Cudd_bddBindVar ARGS((DdManager *dd, int index));
00681 EXTERN int Cudd_bddUnbindVar ARGS((DdManager *dd, int index));
00682 EXTERN int Cudd_bddVarIsBound ARGS((DdManager *dd, int index));
00683 EXTERN DdNode * Cudd_addExistAbstract ARGS((DdManager *manager, DdNode *f, DdNode *cube));
00684 EXTERN DdNode * Cudd_addUnivAbstract ARGS((DdManager *manager, DdNode *f, DdNode *cube));
00685 EXTERN DdNode * Cudd_addOrAbstract ARGS((DdManager *manager, DdNode *f, DdNode *cube));
00686 EXTERN DdNode * Cudd_addApply ARGS((DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g));
00687 EXTERN DdNode * Cudd_addPlus ARGS((DdManager *dd, DdNode **f, DdNode **g));
00688 EXTERN DdNode * Cudd_addTimes ARGS((DdManager *dd, DdNode **f, DdNode **g));
00689 EXTERN DdNode * Cudd_addThreshold ARGS((DdManager *dd, DdNode **f, DdNode **g));
00690 EXTERN DdNode * Cudd_addSetNZ ARGS((DdManager *dd, DdNode **f, DdNode **g));
00691 EXTERN DdNode * Cudd_addDivide ARGS((DdManager *dd, DdNode **f, DdNode **g));
00692 EXTERN DdNode * Cudd_addMinus ARGS((DdManager *dd, DdNode **f, DdNode **g));
00693 EXTERN DdNode * Cudd_addMinimum ARGS((DdManager *dd, DdNode **f, DdNode **g));
00694 EXTERN DdNode * Cudd_addMaximum ARGS((DdManager *dd, DdNode **f, DdNode **g));
00695 EXTERN DdNode * Cudd_addOneZeroMaximum ARGS((DdManager *dd, DdNode **f, DdNode **g));
00696 EXTERN DdNode * Cudd_addDiff ARGS((DdManager *dd, DdNode **f, DdNode **g));
00697 EXTERN DdNode * Cudd_addAgreement ARGS((DdManager *dd, DdNode **f, DdNode **g));
00698 EXTERN DdNode * Cudd_addOr ARGS((DdManager *dd, DdNode **f, DdNode **g));
00699 EXTERN DdNode * Cudd_addNand ARGS((DdManager *dd, DdNode **f, DdNode **g));
00700 EXTERN DdNode * Cudd_addNor ARGS((DdManager *dd, DdNode **f, DdNode **g));
00701 EXTERN DdNode * Cudd_addXor ARGS((DdManager *dd, DdNode **f, DdNode **g));
00702 EXTERN DdNode * Cudd_addXnor ARGS((DdManager *dd, DdNode **f, DdNode **g));
00703 EXTERN DdNode * Cudd_addMonadicApply ARGS((DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f));
00704 EXTERN DdNode * Cudd_addLog ARGS((DdManager * dd, DdNode * f));
00705 EXTERN DdNode * Cudd_addFindMax ARGS((DdManager *dd, DdNode *f));
00706 EXTERN DdNode * Cudd_addFindMin ARGS((DdManager *dd, DdNode *f));
00707 EXTERN DdNode * Cudd_addIthBit ARGS((DdManager *dd, DdNode *f, int bit));
00708 EXTERN DdNode * Cudd_addScalarInverse ARGS((DdManager *dd, DdNode *f, DdNode *epsilon));
00709 EXTERN DdNode * Cudd_addIte ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *h));
00710 EXTERN DdNode * Cudd_addIteConstant ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *h));
00711 EXTERN DdNode * Cudd_addEvalConst ARGS((DdManager *dd, DdNode *f, DdNode *g));
00712 EXTERN int Cudd_addLeq ARGS((DdManager * dd, DdNode * f, DdNode * g));
00713 EXTERN DdNode * Cudd_addCmpl ARGS((DdManager *dd, DdNode *f));
00714 EXTERN DdNode * Cudd_addNegate ARGS((DdManager *dd, DdNode *f));
00715 EXTERN DdNode * Cudd_addRoundOff ARGS((DdManager *dd, DdNode *f, int N));
00716 EXTERN DdNode * Cudd_addWalsh ARGS((DdManager *dd, DdNode **x, DdNode **y, int n));
00717 EXTERN DdNode * Cudd_addResidue ARGS((DdManager *dd, int n, int m, int options, int top));
00718 EXTERN DdNode * Cudd_bddAndAbstract ARGS((DdManager *manager, DdNode *f, DdNode *g, DdNode *cube));
00719 EXTERN int Cudd_ApaNumberOfDigits ARGS((int binaryDigits));
00720 EXTERN DdApaNumber Cudd_NewApaNumber ARGS((int digits));
00721 EXTERN void Cudd_ApaCopy ARGS((int digits, DdApaNumber source, DdApaNumber dest));
00722 EXTERN DdApaDigit Cudd_ApaAdd ARGS((int digits, DdApaNumber a, DdApaNumber b, DdApaNumber sum));
00723 EXTERN DdApaDigit Cudd_ApaSubtract ARGS((int digits, DdApaNumber a, DdApaNumber b, DdApaNumber diff));
00724 EXTERN DdApaDigit Cudd_ApaShortDivision ARGS((int digits, DdApaNumber dividend, DdApaDigit divisor, DdApaNumber quotient));
00725 EXTERN unsigned int Cudd_ApaIntDivision ARGS((int digits, DdApaNumber dividend, unsigned int divisor, DdApaNumber quotient));
00726 EXTERN void Cudd_ApaShiftRight ARGS((int digits, DdApaDigit in, DdApaNumber a, DdApaNumber b));
00727 EXTERN void Cudd_ApaSetToLiteral ARGS((int digits, DdApaNumber number, DdApaDigit literal));
00728 EXTERN void Cudd_ApaPowerOfTwo ARGS((int digits, DdApaNumber number, int power));
00729 EXTERN int Cudd_ApaCompare ARGS((int digitsFirst, DdApaNumber first, int digitsSecond, DdApaNumber second));
00730 EXTERN int Cudd_ApaCompareRatios ARGS ((int digitsFirst, DdApaNumber firstNum, unsigned int firstDen, int digitsSecond, DdApaNumber secondNum, unsigned int secondDen));
00731 EXTERN int Cudd_ApaPrintHex ARGS((FILE *fp, int digits, DdApaNumber number));
00732 EXTERN int Cudd_ApaPrintDecimal ARGS((FILE *fp, int digits, DdApaNumber number));
00733 EXTERN int Cudd_ApaPrintExponential ARGS((FILE * fp, int digits, DdApaNumber number, int precision));
00734 EXTERN DdApaNumber Cudd_ApaCountMinterm ARGS((DdManager *manager, DdNode *node, int nvars, int *digits));
00735 EXTERN int Cudd_ApaPrintMinterm ARGS((FILE *fp, DdManager *dd, DdNode *node, int nvars));
00736 EXTERN int Cudd_ApaPrintMintermExp ARGS((FILE * fp, DdManager * dd, DdNode * node, int nvars, int precision));
00737 EXTERN int Cudd_ApaPrintDensity ARGS((FILE * fp, DdManager * dd, DdNode * node, int nvars));
00738 EXTERN DdNode * Cudd_UnderApprox ARGS((DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality));
00739 EXTERN DdNode * Cudd_OverApprox ARGS((DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality));
00740 EXTERN DdNode * Cudd_RemapUnderApprox ARGS((DdManager *dd, DdNode *f, int numVars, int threshold, double quality));
00741 EXTERN DdNode * Cudd_RemapOverApprox ARGS((DdManager *dd, DdNode *f, int numVars, int threshold, double quality));
00742 EXTERN DdNode * Cudd_BiasedUnderApprox ARGS((DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0));
00743 EXTERN DdNode * Cudd_BiasedOverApprox ARGS((DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0));
00744 EXTERN DdNode * Cudd_bddExistAbstract ARGS((DdManager *manager, DdNode *f, DdNode *cube));
00745 EXTERN DdNode * Cudd_bddXorExistAbstract ARGS((DdManager *manager, DdNode *f, DdNode *g, DdNode *cube));
00746 EXTERN DdNode * Cudd_bddUnivAbstract ARGS((DdManager *manager, DdNode *f, DdNode *cube));
00747 EXTERN DdNode * Cudd_bddBooleanDiff ARGS((DdManager *manager, DdNode *f, int x));
00748 EXTERN int Cudd_bddVarIsDependent ARGS((DdManager *dd, DdNode *f, DdNode *var));
00749 EXTERN double Cudd_bddCorrelation ARGS((DdManager *manager, DdNode *f, DdNode *g));
00750 EXTERN double Cudd_bddCorrelationWeights ARGS((DdManager *manager, DdNode *f, DdNode *g, double *prob));
00751 EXTERN DdNode * Cudd_bddIte ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *h));
00752 EXTERN DdNode * Cudd_bddIteConstant ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *h));
00753 EXTERN DdNode * Cudd_bddIntersect ARGS((DdManager *dd, DdNode *f, DdNode *g));
00754 EXTERN DdNode * Cudd_bddAnd ARGS((DdManager *dd, DdNode *f, DdNode *g));
00755 EXTERN DdNode * Cudd_bddOr ARGS((DdManager *dd, DdNode *f, DdNode *g));
00756 EXTERN DdNode * Cudd_bddNand ARGS((DdManager *dd, DdNode *f, DdNode *g));
00757 EXTERN DdNode * Cudd_bddNor ARGS((DdManager *dd, DdNode *f, DdNode *g));
00758 EXTERN DdNode * Cudd_bddXor ARGS((DdManager *dd, DdNode *f, DdNode *g));
00759 EXTERN DdNode * Cudd_bddXnor ARGS((DdManager *dd, DdNode *f, DdNode *g));
00760 EXTERN int Cudd_bddLeq ARGS((DdManager *dd, DdNode *f, DdNode *g));
00761 EXTERN DdNode * Cudd_addBddThreshold ARGS((DdManager *dd, DdNode *f, CUDD_VALUE_TYPE value));
00762 EXTERN DdNode * Cudd_addBddStrictThreshold ARGS((DdManager *dd, DdNode *f, CUDD_VALUE_TYPE value));
00763 EXTERN DdNode * Cudd_addBddInterval ARGS((DdManager *dd, DdNode *f, CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper));
00764 EXTERN DdNode * Cudd_addBddIthBit ARGS((DdManager *dd, DdNode *f, int bit));
00765 EXTERN DdNode * Cudd_BddToAdd ARGS((DdManager *dd, DdNode *B));
00766 EXTERN DdNode * Cudd_addBddPattern ARGS((DdManager *dd, DdNode *f));
00767 EXTERN DdNode * Cudd_bddTransfer ARGS((DdManager *ddSource, DdManager *ddDestination, DdNode *f));
00768 EXTERN int Cudd_DebugCheck ARGS((DdManager *table));
00769 EXTERN int Cudd_CheckKeys ARGS((DdManager *table));
00770 EXTERN DdNode * Cudd_bddClippingAnd ARGS((DdManager *dd, DdNode *f, DdNode *g, int maxDepth, int direction));
00771 EXTERN DdNode * Cudd_bddClippingAndAbstract ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *cube, int maxDepth, int direction));
00772 EXTERN DdNode * Cudd_Cofactor ARGS((DdManager *dd, DdNode *f, DdNode *g));
00773 EXTERN DdNode * Cudd_bddCompose ARGS((DdManager *dd, DdNode *f, DdNode *g, int v));
00774 EXTERN DdNode * Cudd_addCompose ARGS((DdManager *dd, DdNode *f, DdNode *g, int v));
00775 EXTERN DdNode * Cudd_addPermute ARGS((DdManager *manager, DdNode *node, int *permut));
00776 EXTERN DdNode * Cudd_addSwapVariables ARGS((DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n));
00777 EXTERN DdNode * Cudd_bddPermute ARGS((DdManager *manager, DdNode *node, int *permut));
00778 EXTERN DdNode * Cudd_bddVarMap ARGS((DdManager *manager, DdNode *f));
00779 EXTERN int Cudd_SetVarMap ARGS((DdManager *manager, DdNode **x, DdNode **y, int n));
00780 EXTERN DdNode * Cudd_bddSwapVariables ARGS((DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n));
00781 EXTERN DdNode * Cudd_bddAdjPermuteX ARGS((DdManager *dd, DdNode *B, DdNode **x, int n));
00782 EXTERN DdNode * Cudd_addVectorCompose ARGS((DdManager *dd, DdNode *f, DdNode **vector));
00783 EXTERN DdNode * Cudd_addGeneralVectorCompose ARGS((DdManager *dd, DdNode *f, DdNode **vectorOn, DdNode **vectorOff));
00784 EXTERN DdNode * Cudd_addNonSimCompose ARGS((DdManager *dd, DdNode *f, DdNode **vector));
00785 EXTERN DdNode * Cudd_bddVectorCompose ARGS((DdManager *dd, DdNode *f, DdNode **vector));
00786 EXTERN int Cudd_bddApproxConjDecomp ARGS((DdManager *dd, DdNode *f, DdNode ***conjuncts));
00787 EXTERN int Cudd_bddApproxDisjDecomp ARGS((DdManager *dd, DdNode *f, DdNode ***disjuncts));
00788 EXTERN int Cudd_bddIterConjDecomp ARGS((DdManager *dd, DdNode *f, DdNode ***conjuncts));
00789 EXTERN int Cudd_bddIterDisjDecomp ARGS((DdManager *dd, DdNode *f, DdNode ***disjuncts));
00790 EXTERN int Cudd_bddGenConjDecomp ARGS((DdManager *dd, DdNode *f, DdNode ***conjuncts));
00791 EXTERN int Cudd_bddGenDisjDecomp ARGS((DdManager *dd, DdNode *f, DdNode ***disjuncts));
00792 EXTERN int Cudd_bddVarConjDecomp ARGS((DdManager *dd, DdNode * f, DdNode ***conjuncts));
00793 EXTERN int Cudd_bddVarDisjDecomp ARGS((DdManager *dd, DdNode * f, DdNode ***disjuncts));
00794 EXTERN DdNode * Cudd_FindEssential ARGS((DdManager *dd, DdNode *f));
00795 EXTERN int Cudd_bddIsVarEssential ARGS((DdManager *manager, DdNode *f, int id, int phase));
00796 EXTERN int Cudd_DumpBlif ARGS((DdManager *dd, int n, DdNode **f, char **inames, char **onames, char *mname, FILE *fp));
00797 EXTERN int Cudd_DumpBlifBody ARGS((DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp));
00798 EXTERN int Cudd_DumpDot ARGS((DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp));
00799 EXTERN int Cudd_DumpDaVinci ARGS((DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp));
00800 EXTERN int Cudd_DumpDDcal ARGS((DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp));
00801 EXTERN int Cudd_DumpFactoredForm ARGS((DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp));
00802 EXTERN DdNode * Cudd_bddConstrain ARGS((DdManager *dd, DdNode *f, DdNode *c));
00803 EXTERN DdNode * Cudd_bddRestrict ARGS((DdManager *dd, DdNode *f, DdNode *c));
00804 EXTERN DdNode * Cudd_addConstrain ARGS((DdManager *dd, DdNode *f, DdNode *c));
00805 EXTERN DdNode ** Cudd_bddConstrainDecomp ARGS((DdManager *dd, DdNode *f));
00806 EXTERN DdNode * Cudd_addRestrict ARGS((DdManager *dd, DdNode *f, DdNode *c));
00807 EXTERN DdNode ** Cudd_bddCharToVect ARGS((DdManager *dd, DdNode *f));
00808 EXTERN DdNode * Cudd_bddLICompaction ARGS((DdManager *dd, DdNode *f, DdNode *c));
00809 EXTERN DdNode * Cudd_bddSqueeze ARGS((DdManager *dd, DdNode *l, DdNode *u));
00810 EXTERN DdNode * Cudd_bddMinimize ARGS((DdManager *dd, DdNode *f, DdNode *c));
00811 EXTERN DdNode * Cudd_SubsetCompress ARGS((DdManager *dd, DdNode *f, int nvars, int threshold));
00812 EXTERN DdNode * Cudd_SupersetCompress ARGS((DdManager *dd, DdNode *f, int nvars, int threshold));
00813 EXTERN MtrNode * Cudd_MakeTreeNode ARGS((DdManager *dd, unsigned int low, unsigned int size, unsigned int type));
00814 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));
00815 EXTERN DdManager * Cudd_Init ARGS((unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory));
00816 EXTERN void Cudd_Quit ARGS((DdManager *unique));
00817 EXTERN int Cudd_PrintLinear ARGS((DdManager *table));
00818 EXTERN int Cudd_ReadLinear ARGS((DdManager *table, int x, int y));
00819 EXTERN DdNode * Cudd_bddLiteralSetIntersection ARGS((DdManager *dd, DdNode *f, DdNode *g));
00820 EXTERN DdNode * Cudd_addMatrixMultiply ARGS((DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz));
00821 EXTERN DdNode * Cudd_addTimesPlus ARGS((DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz));
00822 EXTERN DdNode * Cudd_addTriangle ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode **z, int nz));
00823 EXTERN DdNode * Cudd_addOuterSum ARGS((DdManager *dd, DdNode *M, DdNode *r, DdNode *c));
00824 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 **)));
00825 EXTERN DdNode * Cudd_Xgty ARGS((DdManager *dd, int N, DdNode **z, DdNode **x, DdNode **y));
00826 EXTERN DdNode * Cudd_Xeqy ARGS((DdManager *dd, int N, DdNode **x, DdNode **y));
00827 EXTERN DdNode * Cudd_addXeqy ARGS((DdManager *dd, int N, DdNode **x, DdNode **y));
00828 EXTERN DdNode * Cudd_Dxygtdxz ARGS((DdManager *dd, int N, DdNode **x, DdNode **y, DdNode **z));
00829 EXTERN DdNode * Cudd_Dxygtdyz ARGS((DdManager *dd, int N, DdNode **x, DdNode **y, DdNode **z));
00830 EXTERN DdNode * Cudd_CProjection ARGS((DdManager *dd, DdNode *R, DdNode *Y));
00831 EXTERN DdNode * Cudd_addHamming ARGS((DdManager *dd, DdNode **xVars, DdNode **yVars, int nVars));
00832 EXTERN int Cudd_MinHammingDist ARGS((DdManager *dd, DdNode *f, int *minterm, int upperBound));
00833 EXTERN DdNode * Cudd_bddClosestCube ARGS((DdManager *dd, DdNode * f, DdNode *g, int *distance));
00834 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));
00835 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));
00836 EXTERN void Cudd_Ref ARGS((DdNode *n));
00837 EXTERN void Cudd_RecursiveDeref ARGS((DdManager *table, DdNode *n));
00838 EXTERN void Cudd_IterDerefBdd ARGS((DdManager *table, DdNode *n));
00839 EXTERN void Cudd_DelayedDerefBdd ARGS((DdManager * table, DdNode * n));
00840 EXTERN void Cudd_RecursiveDerefZdd ARGS((DdManager *table, DdNode *n));
00841 EXTERN void Cudd_Deref ARGS((DdNode *node));
00842 EXTERN int Cudd_CheckZeroRef ARGS((DdManager *manager));
00843 EXTERN int Cudd_ReduceHeap ARGS((DdManager *table, Cudd_ReorderingType heuristic, int minsize));
00844 EXTERN int Cudd_ShuffleHeap ARGS((DdManager *table, int *permutation));
00845 EXTERN DdNode * Cudd_Eval ARGS((DdManager *dd, DdNode *f, int *inputs));
00846 EXTERN DdNode * Cudd_ShortestPath ARGS((DdManager *manager, DdNode *f, int *weight, int *support, int *length));
00847 EXTERN DdNode * Cudd_LargestCube ARGS((DdManager *manager, DdNode *f, int *length));
00848 EXTERN int Cudd_ShortestLength ARGS((DdManager *manager, DdNode *f, int *weight));
00849 EXTERN DdNode * Cudd_Decreasing ARGS((DdManager *dd, DdNode *f, int i));
00850 EXTERN DdNode * Cudd_Increasing ARGS((DdManager *dd, DdNode *f, int i));
00851 EXTERN int Cudd_EquivDC ARGS((DdManager *dd, DdNode *F, DdNode *G, DdNode *D));
00852 EXTERN int Cudd_bddLeqUnless ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *D));
00853 EXTERN int Cudd_EqualSupNorm ARGS((DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr));
00854 EXTERN DdNode * Cudd_bddMakePrime ARGS ((DdManager *dd, DdNode *cube, DdNode *f));
00855 EXTERN double * Cudd_CofMinterm ARGS((DdManager *dd, DdNode *node));
00856 EXTERN DdNode * Cudd_SolveEqn ARGS((DdManager * bdd, DdNode *F, DdNode *Y, DdNode **G, int **yIndex, int n));
00857 EXTERN DdNode * Cudd_VerifySol ARGS((DdManager * bdd, DdNode *F, DdNode **G, int *yIndex, int n));
00858 EXTERN DdNode * Cudd_SplitSet ARGS((DdManager *manager, DdNode *S, DdNode **xVars, int n, double m));
00859 EXTERN DdNode * Cudd_SubsetHeavyBranch ARGS((DdManager *dd, DdNode *f, int numVars, int threshold));
00860 EXTERN DdNode * Cudd_SupersetHeavyBranch ARGS((DdManager *dd, DdNode *f, int numVars, int threshold));
00861 EXTERN DdNode * Cudd_SubsetShortPaths ARGS((DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit));
00862 EXTERN DdNode * Cudd_SupersetShortPaths ARGS((DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit));
00863 EXTERN void Cudd_SymmProfile ARGS((DdManager *table, int lower, int upper));
00864 EXTERN unsigned int Cudd_Prime ARGS((unsigned int p));
00865 EXTERN int Cudd_PrintMinterm ARGS((DdManager *manager, DdNode *node));
00866 EXTERN int Cudd_bddPrintCover ARGS((DdManager *dd, DdNode *l, DdNode *u));
00867 EXTERN int Cudd_PrintDebug ARGS((DdManager *dd, DdNode *f, int n, int pr));
00868 EXTERN int Cudd_DagSize ARGS((DdNode *node));
00869 EXTERN int Cudd_EstimateCofactor ARGS((DdManager *dd, DdNode * node, int i, int phase));
00870 EXTERN int Cudd_EstimateCofactorSimple ARGS((DdNode * node, int i));
00871 EXTERN int Cudd_SharingSize ARGS((DdNode **nodeArray, int n));
00872 EXTERN double Cudd_CountMinterm ARGS((DdManager *manager, DdNode *node, int nvars));
00873 EXTERN int Cudd_EpdCountMinterm ARGS((DdManager *manager, DdNode *node, int nvars, EpDouble *epd));
00874 EXTERN double Cudd_CountPath ARGS((DdNode *node));
00875 EXTERN double Cudd_CountPathsToNonZero ARGS((DdNode *node));
00876 EXTERN DdNode * Cudd_Support ARGS((DdManager *dd, DdNode *f));
00877 EXTERN int * Cudd_SupportIndex ARGS((DdManager *dd, DdNode *f));
00878 EXTERN int Cudd_SupportSize ARGS((DdManager *dd, DdNode *f));
00879 EXTERN DdNode * Cudd_VectorSupport ARGS((DdManager *dd, DdNode **F, int n));
00880 EXTERN int * Cudd_VectorSupportIndex ARGS((DdManager *dd, DdNode **F, int n));
00881 EXTERN int Cudd_VectorSupportSize ARGS((DdManager *dd, DdNode **F, int n));
00882 EXTERN int Cudd_ClassifySupport ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode **common, DdNode **onlyF, DdNode **onlyG));
00883 EXTERN int Cudd_CountLeaves ARGS((DdNode *node));
00884 EXTERN int Cudd_bddPickOneCube ARGS((DdManager *ddm, DdNode *node, char *string));
00885 EXTERN DdNode * Cudd_bddPickOneMinterm ARGS((DdManager *dd, DdNode *f, DdNode **vars, int n));
00886 EXTERN DdNode ** Cudd_bddPickArbitraryMinterms ARGS((DdManager *dd, DdNode *f, DdNode **vars, int n, int k));
00887 EXTERN DdNode * Cudd_SubsetWithMaskVars ARGS((DdManager *dd, DdNode *f, DdNode **vars, int nvars, DdNode **maskVars, int mvars));
00888 EXTERN DdGen * Cudd_FirstCube ARGS((DdManager *dd, DdNode *f, int **cube, CUDD_VALUE_TYPE *value));
00889 EXTERN int Cudd_NextCube ARGS((DdGen *gen, int **cube, CUDD_VALUE_TYPE *value));
00890 EXTERN DdNode * Cudd_bddComputeCube ARGS((DdManager *dd, DdNode **vars, int *phase, int n));
00891 EXTERN DdNode * Cudd_addComputeCube ARGS((DdManager *dd, DdNode **vars, int *phase, int n));
00892 EXTERN DdNode * Cudd_CubeArrayToBdd ARGS((DdManager *dd, int *array));
00893 EXTERN int Cudd_BddToCubeArray ARGS((DdManager *dd, DdNode *cube, int *array));
00894 EXTERN DdGen * Cudd_FirstNode ARGS((DdManager *dd, DdNode *f, DdNode **node));
00895 EXTERN int Cudd_NextNode ARGS((DdGen *gen, DdNode **node));
00896 EXTERN int Cudd_GenFree ARGS((DdGen *gen));
00897 EXTERN int Cudd_IsGenEmpty ARGS((DdGen *gen));
00898 EXTERN DdNode * Cudd_IndicesToCube ARGS((DdManager *dd, int *array, int n));
00899 EXTERN void Cudd_PrintVersion ARGS((FILE *fp));
00900 EXTERN double Cudd_AverageDistance ARGS((DdManager *dd));
00901 EXTERN long Cudd_Random ARGS(());
00902 EXTERN void Cudd_Srandom ARGS((long seed));
00903 EXTERN double Cudd_Density ARGS((DdManager *dd, DdNode *f, int nvars));
00904 EXTERN void Cudd_OutOfMem ARGS((long size));
00905 EXTERN int Cudd_zddCount ARGS((DdManager *zdd, DdNode *P));
00906 EXTERN double Cudd_zddCountDouble ARGS((DdManager *zdd, DdNode *P));
00907 EXTERN DdNode * Cudd_zddProduct ARGS((DdManager *dd, DdNode *f, DdNode *g));
00908 EXTERN DdNode * Cudd_zddUnateProduct ARGS((DdManager *dd, DdNode *f, DdNode *g));
00909 EXTERN DdNode * Cudd_zddWeakDiv ARGS((DdManager *dd, DdNode *f, DdNode *g));
00910 EXTERN DdNode * Cudd_zddDivide ARGS((DdManager *dd, DdNode *f, DdNode *g));
00911 EXTERN DdNode * Cudd_zddWeakDivF ARGS((DdManager *dd, DdNode *f, DdNode *g));
00912 EXTERN DdNode * Cudd_zddDivideF ARGS((DdManager *dd, DdNode *f, DdNode *g));
00913 EXTERN DdNode * Cudd_zddComplement ARGS((DdManager *dd, DdNode *node));
00914 EXTERN MtrNode * Cudd_MakeZddTreeNode ARGS((DdManager *dd, unsigned int low, unsigned int size, unsigned int type));
00915 EXTERN DdNode * Cudd_zddIsop ARGS((DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I));
00916 EXTERN DdNode * Cudd_bddIsop ARGS((DdManager *dd, DdNode *L, DdNode *U));
00917 EXTERN DdNode * Cudd_MakeBddFromZddCover ARGS((DdManager *dd, DdNode *node));
00918 EXTERN int Cudd_zddDagSize ARGS((DdNode *p_node));
00919 EXTERN double Cudd_zddCountMinterm ARGS((DdManager *zdd, DdNode *node, int path));
00920 EXTERN void Cudd_zddPrintSubtable ARGS((DdManager *table));
00921 EXTERN DdNode * Cudd_zddPortFromBdd ARGS((DdManager *dd, DdNode *B));
00922 EXTERN DdNode * Cudd_zddPortToBdd ARGS((DdManager *dd, DdNode *f));
00923 EXTERN int Cudd_zddReduceHeap ARGS((DdManager *table, Cudd_ReorderingType heuristic, int minsize));
00924 EXTERN int Cudd_zddShuffleHeap ARGS((DdManager *table, int *permutation));
00925 EXTERN DdNode * Cudd_zddIte ARGS((DdManager *dd, DdNode *f, DdNode *g, DdNode *h));
00926 EXTERN DdNode * Cudd_zddUnion ARGS((DdManager *dd, DdNode *P, DdNode *Q));
00927 EXTERN DdNode * Cudd_zddIntersect ARGS((DdManager *dd, DdNode *P, DdNode *Q));
00928 EXTERN DdNode * Cudd_zddDiff ARGS((DdManager *dd, DdNode *P, DdNode *Q));
00929 EXTERN DdNode * Cudd_zddDiffConst ARGS((DdManager *zdd, DdNode *P, DdNode *Q));
00930 EXTERN DdNode * Cudd_zddSubset1 ARGS((DdManager *dd, DdNode *P, int var));
00931 EXTERN DdNode * Cudd_zddSubset0 ARGS((DdManager *dd, DdNode *P, int var));
00932 EXTERN DdNode * Cudd_zddChange ARGS((DdManager *dd, DdNode *P, int var));
00933 EXTERN void Cudd_zddSymmProfile ARGS((DdManager *table, int lower, int upper));
00934 EXTERN int Cudd_zddPrintMinterm ARGS((DdManager *zdd, DdNode *node));
00935 EXTERN int Cudd_zddPrintCover ARGS((DdManager *zdd, DdNode *node));
00936 EXTERN int Cudd_zddPrintDebug ARGS((DdManager *zdd, DdNode *f, int n, int pr));
00937 EXTERN DdGen * Cudd_zddFirstPath ARGS((DdManager *zdd, DdNode *f, int **path));
00938 EXTERN int Cudd_zddNextPath ARGS((DdGen *gen, int **path));
00939 EXTERN char * Cudd_zddCoverPathToString ARGS((DdManager *zdd, int *path, char *str));
00940 EXTERN int Cudd_zddDumpDot ARGS((DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp));
00941 EXTERN int Cudd_bddSetPiVar ARGS((DdManager *dd, int index));
00942 EXTERN int Cudd_bddSetPsVar ARGS((DdManager *dd, int index));
00943 EXTERN int Cudd_bddSetNsVar ARGS((DdManager *dd, int index));
00944 EXTERN int Cudd_bddIsPiVar ARGS((DdManager *dd, int index));
00945 EXTERN int Cudd_bddIsPsVar ARGS((DdManager *dd, int index));
00946 EXTERN int Cudd_bddIsNsVar ARGS((DdManager *dd, int index));
00947 EXTERN int Cudd_bddSetPairIndex ARGS((DdManager *dd, int index, int pairIndex));
00948 EXTERN int Cudd_bddReadPairIndex ARGS((DdManager *dd, int index));
00949 EXTERN int Cudd_bddSetVarToBeGrouped ARGS((DdManager *dd, int index));
00950 EXTERN int Cudd_bddSetVarHardGroup ARGS((DdManager *dd, int index));
00951 EXTERN int Cudd_bddResetVarToBeGrouped ARGS((DdManager *dd, int index));
00952 EXTERN int Cudd_bddIsVarToBeGrouped ARGS((DdManager *dd, int index));
00953 EXTERN int Cudd_bddSetVarToBeUngrouped ARGS((DdManager *dd, int index));
00954 EXTERN int Cudd_bddIsVarToBeUngrouped ARGS((DdManager *dd, int index));
00955 EXTERN int Cudd_bddIsVarHardGroup ARGS((DdManager *dd, int index));
00956
00959 #endif
