00001
00057 #ifndef _CUDD
00058 #define _CUDD
00059
00060
00061
00062
00063
00064 #include "mtr.h"
00065 #include "epd.h"
00066
00067 #ifdef __cplusplus
00068 extern "C" {
00069 #endif
00070
00071
00072
00073
00074
00075 #define CUDD_VERSION "2.4.2"
00076
00077 #ifndef SIZEOF_VOID_P
00078 #define SIZEOF_VOID_P 4
00079 #endif
00080 #ifndef SIZEOF_INT
00081 #define SIZEOF_INT 4
00082 #endif
00083 #ifndef SIZEOF_LONG
00084 #define SIZEOF_LONG 4
00085 #endif
00086
00087 #ifndef TRUE
00088 #define TRUE 1
00089 #endif
00090 #ifndef FALSE
00091 #define FALSE 0
00092 #endif
00093
00094 #define CUDD_VALUE_TYPE double
00095 #define CUDD_OUT_OF_MEM -1
00096
00097 #define CUDD_UNIQUE_SLOTS 256
00098 #define CUDD_CACHE_SLOTS 262144
00099
00100
00101 #define CUDD_RESIDUE_DEFAULT 0
00102 #define CUDD_RESIDUE_MSB 1
00103 #define CUDD_RESIDUE_TC 2
00104
00105
00106
00107
00108
00109 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00110 #define CUDD_MAXINDEX (((DdHalfWord) ~0) >> 1)
00111 #else
00112 #define CUDD_MAXINDEX ((DdHalfWord) ~0)
00113 #endif
00114
00115
00116
00117 #define CUDD_CONST_INDEX CUDD_MAXINDEX
00118
00119
00120
00121
00122
00123
00124 #if SIZEOF_LONG == 8
00125 #define DD_APA_BITS 32
00126 #define DD_APA_BASE (1L << DD_APA_BITS)
00127 #define DD_APA_HEXPRINT "%08x"
00128 #else
00129 #define DD_APA_BITS 16
00130 #define DD_APA_BASE (1 << DD_APA_BITS)
00131 #define DD_APA_HEXPRINT "%04x"
00132 #endif
00133 #define DD_APA_MASK (DD_APA_BASE - 1)
00134
00135
00136
00137
00138
00139
00140
00141
00142
00143
00151 typedef enum {
00152 CUDD_REORDER_SAME,
00153 CUDD_REORDER_NONE,
00154 CUDD_REORDER_RANDOM,
00155 CUDD_REORDER_RANDOM_PIVOT,
00156 CUDD_REORDER_SIFT,
00157 CUDD_REORDER_SIFT_CONVERGE,
00158 CUDD_REORDER_SYMM_SIFT,
00159 CUDD_REORDER_SYMM_SIFT_CONV,
00160 CUDD_REORDER_WINDOW2,
00161 CUDD_REORDER_WINDOW3,
00162 CUDD_REORDER_WINDOW4,
00163 CUDD_REORDER_WINDOW2_CONV,
00164 CUDD_REORDER_WINDOW3_CONV,
00165 CUDD_REORDER_WINDOW4_CONV,
00166 CUDD_REORDER_GROUP_SIFT,
00167 CUDD_REORDER_GROUP_SIFT_CONV,
00168 CUDD_REORDER_ANNEALING,
00169 CUDD_REORDER_GENETIC,
00170 CUDD_REORDER_LINEAR,
00171 CUDD_REORDER_LINEAR_CONVERGE,
00172 CUDD_REORDER_LAZY_SIFT,
00173 CUDD_REORDER_EXACT
00174 } Cudd_ReorderingType;
00175
00176
00184 typedef enum {
00185 CUDD_NO_CHECK,
00186 CUDD_GROUP_CHECK,
00187 CUDD_GROUP_CHECK2,
00188 CUDD_GROUP_CHECK3,
00189 CUDD_GROUP_CHECK4,
00190 CUDD_GROUP_CHECK5,
00191 CUDD_GROUP_CHECK6,
00192 CUDD_GROUP_CHECK7,
00193 CUDD_GROUP_CHECK8,
00194 CUDD_GROUP_CHECK9
00195 } Cudd_AggregationType;
00196
00197
00205 typedef enum {
00206 CUDD_PRE_GC_HOOK,
00207 CUDD_POST_GC_HOOK,
00208 CUDD_PRE_REORDERING_HOOK,
00209 CUDD_POST_REORDERING_HOOK
00210 } Cudd_HookType;
00211
00212
00220 typedef enum {
00221 CUDD_NO_ERROR,
00222 CUDD_MEMORY_OUT,
00223 CUDD_TOO_MANY_NODES,
00224 CUDD_MAX_MEM_EXCEEDED,
00225 CUDD_INVALID_ARG,
00226 CUDD_INTERNAL_ERROR
00227 } Cudd_ErrorType;
00228
00229
00237 typedef enum {
00238 CUDD_LAZY_NONE,
00239 CUDD_LAZY_SOFT_GROUP,
00240 CUDD_LAZY_HARD_GROUP,
00241 CUDD_LAZY_UNGROUP
00242 } Cudd_LazyGroupType;
00243
00244
00252 typedef enum {
00253 CUDD_VAR_PRIMARY_INPUT,
00254 CUDD_VAR_PRESENT_STATE,
00255 CUDD_VAR_NEXT_STATE
00256 } Cudd_VariableType;
00257
00258
00259 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00260 typedef unsigned int DdHalfWord;
00261 #else
00262 typedef unsigned short DdHalfWord;
00263 #endif
00264
00265 #ifdef __osf__
00266 #pragma pointer_size save
00267 #pragma pointer_size short
00268 #endif
00269
00270 typedef struct DdNode DdNode;
00271
00272 typedef struct DdChildren {
00273 struct DdNode *T;
00274 struct DdNode *E;
00275 } DdChildren;
00276
00277
00278 struct DdNode {
00279 DdHalfWord index;
00280 DdHalfWord ref;
00281 DdNode *next;
00282 union {
00283 CUDD_VALUE_TYPE value;
00284 DdChildren kids;
00285 } type;
00286 };
00287
00288 #ifdef __osf__
00289 #pragma pointer_size restore
00290 #endif
00291
00292 typedef struct DdManager DdManager;
00293
00294 typedef struct DdGen DdGen;
00295
00296
00297
00298 #if SIZEOF_LONG == 8
00299 typedef unsigned int DdApaDigit;
00300 typedef unsigned long int DdApaDoubleDigit;
00301 #else
00302 typedef unsigned short int DdApaDigit;
00303 typedef unsigned int DdApaDoubleDigit;
00304 #endif
00305 typedef DdApaDigit * DdApaNumber;
00306
00307
00308 typedef struct DdTlcInfo DdTlcInfo;
00309
00310
00311 typedef int (*DD_HFP)(DdManager *, const char *, void *);
00312
00313 typedef DdNode * (*DD_PRFP)(DdManager * , int, DdNode **, DdNode **,
00314 DdNode **);
00315
00316 typedef DdNode * (*DD_AOP)(DdManager *, DdNode **, DdNode **);
00317
00318 typedef DdNode * (*DD_MAOP)(DdManager *, DdNode *);
00319
00320 typedef DdNode * (*DD_CTFP)(DdManager *, DdNode *, DdNode *);
00321 typedef DdNode * (*DD_CTFP1)(DdManager *, DdNode *);
00322
00323 typedef void (*DD_OOMFP)(long);
00324
00325 typedef int (*DD_QSFP)(const void *, const void *);
00326
00327
00328
00329
00330
00331
00332
00333
00334
00335
00336
00351 #define Cudd_IsConstant(node) ((Cudd_Regular(node))->index == CUDD_CONST_INDEX)
00352
00353
00366 #define Cudd_Not(node) ((DdNode *)((long)(node) ^ 01))
00367
00368
00382 #define Cudd_NotCond(node,c) ((DdNode *)((long)(node) ^ (c)))
00383
00384
00396 #define Cudd_Regular(node) ((DdNode *)((unsigned long)(node) & ~01))
00397
00398
00410 #define Cudd_Complement(node) ((DdNode *)((unsigned long)(node) | 01))
00411
00412
00424 #define Cudd_IsComplement(node) ((int) ((long) (node) & 01))
00425
00426
00439 #define Cudd_T(node) ((Cudd_Regular(node))->type.kids.T)
00440
00441
00454 #define Cudd_E(node) ((Cudd_Regular(node))->type.kids.E)
00455
00456
00469 #define Cudd_V(node) ((Cudd_Regular(node))->type.value)
00470
00471
00486 #define Cudd_ReadIndex(dd,index) (Cudd_ReadPerm(dd,index))
00487
00488
00518 #define Cudd_ForeachCube(manager, f, gen, cube, value)\
00519 for((gen) = Cudd_FirstCube(manager, f, &cube, &value);\
00520 Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
00521 (void) Cudd_NextCube(gen, &cube, &value))
00522
00523
00550 #define Cudd_ForeachPrime(manager, l, u, gen, cube)\
00551 for((gen) = Cudd_FirstPrime(manager, l, u, &cube);\
00552 Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
00553 (void) Cudd_NextPrime(gen, &cube))
00554
00555
00584 #define Cudd_ForeachNode(manager, f, gen, node)\
00585 for((gen) = Cudd_FirstNode(manager, f, &node);\
00586 Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
00587 (void) Cudd_NextNode(gen, &node))
00588
00589
00618 #define Cudd_zddForeachPath(manager, f, gen, path)\
00619 for((gen) = Cudd_zddFirstPath(manager, f, &path);\
00620 Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
00621 (void) Cudd_zddNextPath(gen, &path))
00622
00623
00624
00627
00628
00629
00630
00631 extern DdNode * Cudd_addNewVar (DdManager *dd);
00632 extern DdNode * Cudd_addNewVarAtLevel (DdManager *dd, int level);
00633 extern DdNode * Cudd_bddNewVar (DdManager *dd);
00634 extern DdNode * Cudd_bddNewVarAtLevel (DdManager *dd, int level);
00635 extern DdNode * Cudd_addIthVar (DdManager *dd, int i);
00636 extern DdNode * Cudd_bddIthVar (DdManager *dd, int i);
00637 extern DdNode * Cudd_zddIthVar (DdManager *dd, int i);
00638 extern int Cudd_zddVarsFromBddVars (DdManager *dd, int multiplicity);
00639 extern DdNode * Cudd_addConst (DdManager *dd, CUDD_VALUE_TYPE c);
00640 extern int Cudd_IsNonConstant (DdNode *f);
00641 extern void Cudd_AutodynEnable (DdManager *unique, Cudd_ReorderingType method);
00642 extern void Cudd_AutodynDisable (DdManager *unique);
00643 extern int Cudd_ReorderingStatus (DdManager *unique, Cudd_ReorderingType *method);
00644 extern void Cudd_AutodynEnableZdd (DdManager *unique, Cudd_ReorderingType method);
00645 extern void Cudd_AutodynDisableZdd (DdManager *unique);
00646 extern int Cudd_ReorderingStatusZdd (DdManager *unique, Cudd_ReorderingType *method);
00647 extern int Cudd_zddRealignmentEnabled (DdManager *unique);
00648 extern void Cudd_zddRealignEnable (DdManager *unique);
00649 extern void Cudd_zddRealignDisable (DdManager *unique);
00650 extern int Cudd_bddRealignmentEnabled (DdManager *unique);
00651 extern void Cudd_bddRealignEnable (DdManager *unique);
00652 extern void Cudd_bddRealignDisable (DdManager *unique);
00653 extern DdNode * Cudd_ReadOne (DdManager *dd);
00654 extern DdNode * Cudd_ReadZddOne (DdManager *dd, int i);
00655 extern DdNode * Cudd_ReadZero (DdManager *dd);
00656 extern DdNode * Cudd_ReadLogicZero (DdManager *dd);
00657 extern DdNode * Cudd_ReadPlusInfinity (DdManager *dd);
00658 extern DdNode * Cudd_ReadMinusInfinity (DdManager *dd);
00659 extern DdNode * Cudd_ReadBackground (DdManager *dd);
00660 extern void Cudd_SetBackground (DdManager *dd, DdNode *bck);
00661 extern unsigned int Cudd_ReadCacheSlots (DdManager *dd);
00662 extern double Cudd_ReadCacheUsedSlots (DdManager * dd);
00663 extern double Cudd_ReadCacheLookUps (DdManager *dd);
00664 extern double Cudd_ReadCacheHits (DdManager *dd);
00665 extern double Cudd_ReadRecursiveCalls (DdManager * dd);
00666 extern unsigned int Cudd_ReadMinHit (DdManager *dd);
00667 extern void Cudd_SetMinHit (DdManager *dd, unsigned int hr);
00668 extern unsigned int Cudd_ReadLooseUpTo (DdManager *dd);
00669 extern void Cudd_SetLooseUpTo (DdManager *dd, unsigned int lut);
00670 extern unsigned int Cudd_ReadMaxCache (DdManager *dd);
00671 extern unsigned int Cudd_ReadMaxCacheHard (DdManager *dd);
00672 extern void Cudd_SetMaxCacheHard (DdManager *dd, unsigned int mc);
00673 extern int Cudd_ReadSize (DdManager *dd);
00674 extern int Cudd_ReadZddSize (DdManager *dd);
00675 extern unsigned int Cudd_ReadSlots (DdManager *dd);
00676 extern double Cudd_ReadUsedSlots (DdManager * dd);
00677 extern double Cudd_ExpectedUsedSlots (DdManager * dd);
00678 extern unsigned int Cudd_ReadKeys (DdManager *dd);
00679 extern unsigned int Cudd_ReadDead (DdManager *dd);
00680 extern unsigned int Cudd_ReadMinDead (DdManager *dd);
00681 extern int Cudd_ReadReorderings (DdManager *dd);
00682 extern long Cudd_ReadReorderingTime (DdManager * dd);
00683 extern int Cudd_ReadGarbageCollections (DdManager * dd);
00684 extern long Cudd_ReadGarbageCollectionTime (DdManager * dd);
00685 extern double Cudd_ReadNodesFreed (DdManager * dd);
00686 extern double Cudd_ReadNodesDropped (DdManager * dd);
00687 extern double Cudd_ReadUniqueLookUps (DdManager * dd);
00688 extern double Cudd_ReadUniqueLinks (DdManager * dd);
00689 extern int Cudd_ReadSiftMaxVar (DdManager *dd);
00690 extern void Cudd_SetSiftMaxVar (DdManager *dd, int smv);
00691 extern int Cudd_ReadSiftMaxSwap (DdManager *dd);
00692 extern void Cudd_SetSiftMaxSwap (DdManager *dd, int sms);
00693 extern double Cudd_ReadMaxGrowth (DdManager *dd);
00694 extern void Cudd_SetMaxGrowth (DdManager *dd, double mg);
00695 extern double Cudd_ReadMaxGrowthAlternate (DdManager * dd);
00696 extern void Cudd_SetMaxGrowthAlternate (DdManager * dd, double mg);
00697 extern int Cudd_ReadReorderingCycle (DdManager * dd);
00698 extern void Cudd_SetReorderingCycle (DdManager * dd, int cycle);
00699 extern MtrNode * Cudd_ReadTree (DdManager *dd);
00700 extern void Cudd_SetTree (DdManager *dd, MtrNode *tree);
00701 extern void Cudd_FreeTree (DdManager *dd);
00702 extern MtrNode * Cudd_ReadZddTree (DdManager *dd);
00703 extern void Cudd_SetZddTree (DdManager *dd, MtrNode *tree);
00704 extern void Cudd_FreeZddTree (DdManager *dd);
00705 extern unsigned int Cudd_NodeReadIndex (DdNode *node);
00706 extern int Cudd_ReadPerm (DdManager *dd, int i);
00707 extern int Cudd_ReadPermZdd (DdManager *dd, int i);
00708 extern int Cudd_ReadInvPerm (DdManager *dd, int i);
00709 extern int Cudd_ReadInvPermZdd (DdManager *dd, int i);
00710 extern DdNode * Cudd_ReadVars (DdManager *dd, int i);
00711 extern CUDD_VALUE_TYPE Cudd_ReadEpsilon (DdManager *dd);
00712 extern void Cudd_SetEpsilon (DdManager *dd, CUDD_VALUE_TYPE ep);
00713 extern Cudd_AggregationType Cudd_ReadGroupcheck (DdManager *dd);
00714 extern void Cudd_SetGroupcheck (DdManager *dd, Cudd_AggregationType gc);
00715 extern int Cudd_GarbageCollectionEnabled (DdManager *dd);
00716 extern void Cudd_EnableGarbageCollection (DdManager *dd);
00717 extern void Cudd_DisableGarbageCollection (DdManager *dd);
00718 extern int Cudd_DeadAreCounted (DdManager *dd);
00719 extern void Cudd_TurnOnCountDead (DdManager *dd);
00720 extern void Cudd_TurnOffCountDead (DdManager *dd);
00721 extern int Cudd_ReadRecomb (DdManager *dd);
00722 extern void Cudd_SetRecomb (DdManager *dd, int recomb);
00723 extern int Cudd_ReadSymmviolation (DdManager *dd);
00724 extern void Cudd_SetSymmviolation (DdManager *dd, int symmviolation);
00725 extern int Cudd_ReadArcviolation (DdManager *dd);
00726 extern void Cudd_SetArcviolation (DdManager *dd, int arcviolation);
00727 extern int Cudd_ReadPopulationSize (DdManager *dd);
00728 extern void Cudd_SetPopulationSize (DdManager *dd, int populationSize);
00729 extern int Cudd_ReadNumberXovers (DdManager *dd);
00730 extern void Cudd_SetNumberXovers (DdManager *dd, int numberXovers);
00731 extern unsigned long Cudd_ReadMemoryInUse (DdManager *dd);
00732 extern int Cudd_PrintInfo (DdManager *dd, FILE *fp);
00733 extern long Cudd_ReadPeakNodeCount (DdManager *dd);
00734 extern int Cudd_ReadPeakLiveNodeCount (DdManager * dd);
00735 extern long Cudd_ReadNodeCount (DdManager *dd);
00736 extern long Cudd_zddReadNodeCount (DdManager *dd);
00737 extern int Cudd_AddHook (DdManager *dd, DD_HFP f, Cudd_HookType where);
00738 extern int Cudd_RemoveHook (DdManager *dd, DD_HFP f, Cudd_HookType where);
00739 extern int Cudd_IsInHook (DdManager * dd, DD_HFP f, Cudd_HookType where);
00740 extern int Cudd_StdPreReordHook (DdManager *dd, const char *str, void *data);
00741 extern int Cudd_StdPostReordHook (DdManager *dd, const char *str, void *data);
00742 extern int Cudd_EnableReorderingReporting (DdManager *dd);
00743 extern int Cudd_DisableReorderingReporting (DdManager *dd);
00744 extern int Cudd_ReorderingReporting (DdManager *dd);
00745 extern Cudd_ErrorType Cudd_ReadErrorCode (DdManager *dd);
00746 extern void Cudd_ClearErrorCode (DdManager *dd);
00747 extern FILE * Cudd_ReadStdout (DdManager *dd);
00748 extern void Cudd_SetStdout (DdManager *dd, FILE *fp);
00749 extern FILE * Cudd_ReadStderr (DdManager *dd);
00750 extern void Cudd_SetStderr (DdManager *dd, FILE *fp);
00751 extern unsigned int Cudd_ReadNextReordering (DdManager *dd);
00752 extern void Cudd_SetNextReordering (DdManager *dd, unsigned int next);
00753 extern double Cudd_ReadSwapSteps (DdManager *dd);
00754 extern unsigned int Cudd_ReadMaxLive (DdManager *dd);
00755 extern void Cudd_SetMaxLive (DdManager *dd, unsigned int maxLive);
00756 extern unsigned long Cudd_ReadMaxMemory (DdManager *dd);
00757 extern void Cudd_SetMaxMemory (DdManager *dd, unsigned long maxMemory);
00758 extern int Cudd_bddBindVar (DdManager *dd, int index);
00759 extern int Cudd_bddUnbindVar (DdManager *dd, int index);
00760 extern int Cudd_bddVarIsBound (DdManager *dd, int index);
00761 extern DdNode * Cudd_addExistAbstract (DdManager *manager, DdNode *f, DdNode *cube);
00762 extern DdNode * Cudd_addUnivAbstract (DdManager *manager, DdNode *f, DdNode *cube);
00763 extern DdNode * Cudd_addOrAbstract (DdManager *manager, DdNode *f, DdNode *cube);
00764 extern DdNode * Cudd_addApply (DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g);
00765 extern DdNode * Cudd_addPlus (DdManager *dd, DdNode **f, DdNode **g);
00766 extern DdNode * Cudd_addTimes (DdManager *dd, DdNode **f, DdNode **g);
00767 extern DdNode * Cudd_addThreshold (DdManager *dd, DdNode **f, DdNode **g);
00768 extern DdNode * Cudd_addSetNZ (DdManager *dd, DdNode **f, DdNode **g);
00769 extern DdNode * Cudd_addDivide (DdManager *dd, DdNode **f, DdNode **g);
00770 extern DdNode * Cudd_addMinus (DdManager *dd, DdNode **f, DdNode **g);
00771 extern DdNode * Cudd_addMinimum (DdManager *dd, DdNode **f, DdNode **g);
00772 extern DdNode * Cudd_addMaximum (DdManager *dd, DdNode **f, DdNode **g);
00773 extern DdNode * Cudd_addOneZeroMaximum (DdManager *dd, DdNode **f, DdNode **g);
00774 extern DdNode * Cudd_addDiff (DdManager *dd, DdNode **f, DdNode **g);
00775 extern DdNode * Cudd_addAgreement (DdManager *dd, DdNode **f, DdNode **g);
00776 extern DdNode * Cudd_addOr (DdManager *dd, DdNode **f, DdNode **g);
00777 extern DdNode * Cudd_addNand (DdManager *dd, DdNode **f, DdNode **g);
00778 extern DdNode * Cudd_addNor (DdManager *dd, DdNode **f, DdNode **g);
00779 extern DdNode * Cudd_addXor (DdManager *dd, DdNode **f, DdNode **g);
00780 extern DdNode * Cudd_addXnor (DdManager *dd, DdNode **f, DdNode **g);
00781 extern DdNode * Cudd_addMonadicApply (DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f);
00782 extern DdNode * Cudd_addLog (DdManager * dd, DdNode * f);
00783 extern DdNode * Cudd_addFindMax (DdManager *dd, DdNode *f);
00784 extern DdNode * Cudd_addFindMin (DdManager *dd, DdNode *f);
00785 extern DdNode * Cudd_addIthBit (DdManager *dd, DdNode *f, int bit);
00786 extern DdNode * Cudd_addScalarInverse (DdManager *dd, DdNode *f, DdNode *epsilon);
00787 extern DdNode * Cudd_addIte (DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
00788 extern DdNode * Cudd_addIteConstant (DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
00789 extern DdNode * Cudd_addEvalConst (DdManager *dd, DdNode *f, DdNode *g);
00790 extern int Cudd_addLeq (DdManager * dd, DdNode * f, DdNode * g);
00791 extern DdNode * Cudd_addCmpl (DdManager *dd, DdNode *f);
00792 extern DdNode * Cudd_addNegate (DdManager *dd, DdNode *f);
00793 extern DdNode * Cudd_addRoundOff (DdManager *dd, DdNode *f, int N);
00794 extern DdNode * Cudd_addWalsh (DdManager *dd, DdNode **x, DdNode **y, int n);
00795 extern DdNode * Cudd_addResidue (DdManager *dd, int n, int m, int options, int top);
00796 extern DdNode * Cudd_bddAndAbstract (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube);
00797 extern DdNode * Cudd_bddAndAbstractLimit (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, unsigned int limit);
00798 extern int Cudd_ApaNumberOfDigits (int binaryDigits);
00799 extern DdApaNumber Cudd_NewApaNumber (int digits);
00800 extern void Cudd_ApaCopy (int digits, DdApaNumber source, DdApaNumber dest);
00801 extern DdApaDigit Cudd_ApaAdd (int digits, DdApaNumber a, DdApaNumber b, DdApaNumber sum);
00802 extern DdApaDigit Cudd_ApaSubtract (int digits, DdApaNumber a, DdApaNumber b, DdApaNumber diff);
00803 extern DdApaDigit Cudd_ApaShortDivision (int digits, DdApaNumber dividend, DdApaDigit divisor, DdApaNumber quotient);
00804 extern unsigned int Cudd_ApaIntDivision (int digits, DdApaNumber dividend, unsigned int divisor, DdApaNumber quotient);
00805 extern void Cudd_ApaShiftRight (int digits, DdApaDigit in, DdApaNumber a, DdApaNumber b);
00806 extern void Cudd_ApaSetToLiteral (int digits, DdApaNumber number, DdApaDigit literal);
00807 extern void Cudd_ApaPowerOfTwo (int digits, DdApaNumber number, int power);
00808 extern int Cudd_ApaCompare (int digitsFirst, DdApaNumber first, int digitsSecond, DdApaNumber second);
00809 extern int Cudd_ApaCompareRatios (int digitsFirst, DdApaNumber firstNum, unsigned int firstDen, int digitsSecond, DdApaNumber secondNum, unsigned int secondDen);
00810 extern int Cudd_ApaPrintHex (FILE *fp, int digits, DdApaNumber number);
00811 extern int Cudd_ApaPrintDecimal (FILE *fp, int digits, DdApaNumber number);
00812 extern int Cudd_ApaPrintExponential (FILE * fp, int digits, DdApaNumber number, int precision);
00813 extern DdApaNumber Cudd_ApaCountMinterm (DdManager *manager, DdNode *node, int nvars, int *digits);
00814 extern int Cudd_ApaPrintMinterm (FILE *fp, DdManager *dd, DdNode *node, int nvars);
00815 extern int Cudd_ApaPrintMintermExp (FILE * fp, DdManager * dd, DdNode * node, int nvars, int precision);
00816 extern int Cudd_ApaPrintDensity (FILE * fp, DdManager * dd, DdNode * node, int nvars);
00817 extern DdNode * Cudd_UnderApprox (DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality);
00818 extern DdNode * Cudd_OverApprox (DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality);
00819 extern DdNode * Cudd_RemapUnderApprox (DdManager *dd, DdNode *f, int numVars, int threshold, double quality);
00820 extern DdNode * Cudd_RemapOverApprox (DdManager *dd, DdNode *f, int numVars, int threshold, double quality);
00821 extern DdNode * Cudd_BiasedUnderApprox (DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0);
00822 extern DdNode * Cudd_BiasedOverApprox (DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0);
00823 extern DdNode * Cudd_bddExistAbstract (DdManager *manager, DdNode *f, DdNode *cube);
00824 extern DdNode * Cudd_bddXorExistAbstract (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube);
00825 extern DdNode * Cudd_bddUnivAbstract (DdManager *manager, DdNode *f, DdNode *cube);
00826 extern DdNode * Cudd_bddBooleanDiff (DdManager *manager, DdNode *f, int x);
00827 extern int Cudd_bddVarIsDependent (DdManager *dd, DdNode *f, DdNode *var);
00828 extern double Cudd_bddCorrelation (DdManager *manager, DdNode *f, DdNode *g);
00829 extern double Cudd_bddCorrelationWeights (DdManager *manager, DdNode *f, DdNode *g, double *prob);
00830 extern DdNode * Cudd_bddIte (DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
00831 extern DdNode * Cudd_bddIteConstant (DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
00832 extern DdNode * Cudd_bddIntersect (DdManager *dd, DdNode *f, DdNode *g);
00833 extern DdNode * Cudd_bddAnd (DdManager *dd, DdNode *f, DdNode *g);
00834 extern DdNode * Cudd_bddAndLimit (DdManager *dd, DdNode *f, DdNode *g, unsigned int limit);
00835 extern DdNode * Cudd_bddOr (DdManager *dd, DdNode *f, DdNode *g);
00836 extern DdNode * Cudd_bddNand (DdManager *dd, DdNode *f, DdNode *g);
00837 extern DdNode * Cudd_bddNor (DdManager *dd, DdNode *f, DdNode *g);
00838 extern DdNode * Cudd_bddXor (DdManager *dd, DdNode *f, DdNode *g);
00839 extern DdNode * Cudd_bddXnor (DdManager *dd, DdNode *f, DdNode *g);
00840 extern int Cudd_bddLeq (DdManager *dd, DdNode *f, DdNode *g);
00841 extern DdNode * Cudd_addBddThreshold (DdManager *dd, DdNode *f, CUDD_VALUE_TYPE value);
00842 extern DdNode * Cudd_addBddStrictThreshold (DdManager *dd, DdNode *f, CUDD_VALUE_TYPE value);
00843 extern DdNode * Cudd_addBddInterval (DdManager *dd, DdNode *f, CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper);
00844 extern DdNode * Cudd_addBddIthBit (DdManager *dd, DdNode *f, int bit);
00845 extern DdNode * Cudd_BddToAdd (DdManager *dd, DdNode *B);
00846 extern DdNode * Cudd_addBddPattern (DdManager *dd, DdNode *f);
00847 extern DdNode * Cudd_bddTransfer (DdManager *ddSource, DdManager *ddDestination, DdNode *f);
00848 extern int Cudd_DebugCheck (DdManager *table);
00849 extern int Cudd_CheckKeys (DdManager *table);
00850 extern DdNode * Cudd_bddClippingAnd (DdManager *dd, DdNode *f, DdNode *g, int maxDepth, int direction);
00851 extern DdNode * Cudd_bddClippingAndAbstract (DdManager *dd, DdNode *f, DdNode *g, DdNode *cube, int maxDepth, int direction);
00852 extern DdNode * Cudd_Cofactor (DdManager *dd, DdNode *f, DdNode *g);
00853 extern DdNode * Cudd_bddCompose (DdManager *dd, DdNode *f, DdNode *g, int v);
00854 extern DdNode * Cudd_addCompose (DdManager *dd, DdNode *f, DdNode *g, int v);
00855 extern DdNode * Cudd_addPermute (DdManager *manager, DdNode *node, int *permut);
00856 extern DdNode * Cudd_addSwapVariables (DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n);
00857 extern DdNode * Cudd_bddPermute (DdManager *manager, DdNode *node, int *permut);
00858 extern DdNode * Cudd_bddVarMap (DdManager *manager, DdNode *f);
00859 extern int Cudd_SetVarMap (DdManager *manager, DdNode **x, DdNode **y, int n);
00860 extern DdNode * Cudd_bddSwapVariables (DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n);
00861 extern DdNode * Cudd_bddAdjPermuteX (DdManager *dd, DdNode *B, DdNode **x, int n);
00862 extern DdNode * Cudd_addVectorCompose (DdManager *dd, DdNode *f, DdNode **vector);
00863 extern DdNode * Cudd_addGeneralVectorCompose (DdManager *dd, DdNode *f, DdNode **vectorOn, DdNode **vectorOff);
00864 extern DdNode * Cudd_addNonSimCompose (DdManager *dd, DdNode *f, DdNode **vector);
00865 extern DdNode * Cudd_bddVectorCompose (DdManager *dd, DdNode *f, DdNode **vector);
00866 extern int Cudd_bddApproxConjDecomp (DdManager *dd, DdNode *f, DdNode ***conjuncts);
00867 extern int Cudd_bddApproxDisjDecomp (DdManager *dd, DdNode *f, DdNode ***disjuncts);
00868 extern int Cudd_bddIterConjDecomp (DdManager *dd, DdNode *f, DdNode ***conjuncts);
00869 extern int Cudd_bddIterDisjDecomp (DdManager *dd, DdNode *f, DdNode ***disjuncts);
00870 extern int Cudd_bddGenConjDecomp (DdManager *dd, DdNode *f, DdNode ***conjuncts);
00871 extern int Cudd_bddGenDisjDecomp (DdManager *dd, DdNode *f, DdNode ***disjuncts);
00872 extern int Cudd_bddVarConjDecomp (DdManager *dd, DdNode * f, DdNode ***conjuncts);
00873 extern int Cudd_bddVarDisjDecomp (DdManager *dd, DdNode * f, DdNode ***disjuncts);
00874 extern DdNode * Cudd_FindEssential (DdManager *dd, DdNode *f);
00875 extern int Cudd_bddIsVarEssential (DdManager *manager, DdNode *f, int id, int phase);
00876 extern DdTlcInfo * Cudd_FindTwoLiteralClauses (DdManager * dd, DdNode * f);
00877 extern int Cudd_PrintTwoLiteralClauses (DdManager * dd, DdNode * f, char **names, FILE *fp);
00878 extern int Cudd_ReadIthClause (DdTlcInfo * tlc, int i, DdHalfWord *var1, DdHalfWord *var2, int *phase1, int *phase2);
00879 extern void Cudd_tlcInfoFree (DdTlcInfo * t);
00880 extern int Cudd_DumpBlif (DdManager *dd, int n, DdNode **f, char **inames, char **onames, char *mname, FILE *fp, int mv);
00881 extern int Cudd_DumpBlifBody (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp, int mv);
00882 extern int Cudd_DumpDot (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
00883 extern int Cudd_DumpDaVinci (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
00884 extern int Cudd_DumpDDcal (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
00885 extern int Cudd_DumpFactoredForm (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
00886 extern DdNode * Cudd_bddConstrain (DdManager *dd, DdNode *f, DdNode *c);
00887 extern DdNode * Cudd_bddRestrict (DdManager *dd, DdNode *f, DdNode *c);
00888 extern DdNode * Cudd_bddNPAnd (DdManager *dd, DdNode *f, DdNode *c);
00889 extern DdNode * Cudd_addConstrain (DdManager *dd, DdNode *f, DdNode *c);
00890 extern DdNode ** Cudd_bddConstrainDecomp (DdManager *dd, DdNode *f);
00891 extern DdNode * Cudd_addRestrict (DdManager *dd, DdNode *f, DdNode *c);
00892 extern DdNode ** Cudd_bddCharToVect (DdManager *dd, DdNode *f);
00893 extern DdNode * Cudd_bddLICompaction (DdManager *dd, DdNode *f, DdNode *c);
00894 extern DdNode * Cudd_bddSqueeze (DdManager *dd, DdNode *l, DdNode *u);
00895 extern DdNode * Cudd_bddMinimize (DdManager *dd, DdNode *f, DdNode *c);
00896 extern DdNode * Cudd_SubsetCompress (DdManager *dd, DdNode *f, int nvars, int threshold);
00897 extern DdNode * Cudd_SupersetCompress (DdManager *dd, DdNode *f, int nvars, int threshold);
00898 extern MtrNode * Cudd_MakeTreeNode (DdManager *dd, unsigned int low, unsigned int size, unsigned int type);
00899 extern 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);
00900 extern DdManager * Cudd_Init (unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory);
00901 extern void Cudd_Quit (DdManager *unique);
00902 extern int Cudd_PrintLinear (DdManager *table);
00903 extern int Cudd_ReadLinear (DdManager *table, int x, int y);
00904 extern DdNode * Cudd_bddLiteralSetIntersection (DdManager *dd, DdNode *f, DdNode *g);
00905 extern DdNode * Cudd_addMatrixMultiply (DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz);
00906 extern DdNode * Cudd_addTimesPlus (DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz);
00907 extern DdNode * Cudd_addTriangle (DdManager *dd, DdNode *f, DdNode *g, DdNode **z, int nz);
00908 extern DdNode * Cudd_addOuterSum (DdManager *dd, DdNode *M, DdNode *r, DdNode *c);
00909 extern DdNode * Cudd_PrioritySelect (DdManager *dd, DdNode *R, DdNode **x, DdNode **y, DdNode **z, DdNode *Pi, int n, DdNode * (*)(DdManager *, int, DdNode **, DdNode **, DdNode **));
00910 extern DdNode * Cudd_Xgty (DdManager *dd, int N, DdNode **z, DdNode **x, DdNode **y);
00911 extern DdNode * Cudd_Xeqy (DdManager *dd, int N, DdNode **x, DdNode **y);
00912 extern DdNode * Cudd_addXeqy (DdManager *dd, int N, DdNode **x, DdNode **y);
00913 extern DdNode * Cudd_Dxygtdxz (DdManager *dd, int N, DdNode **x, DdNode **y, DdNode **z);
00914 extern DdNode * Cudd_Dxygtdyz (DdManager *dd, int N, DdNode **x, DdNode **y, DdNode **z);
00915 extern DdNode * Cudd_Inequality (DdManager * dd, int N, int c, DdNode ** x, DdNode ** y);
00916 extern DdNode * Cudd_Disequality (DdManager * dd, int N, int c, DdNode ** x, DdNode ** y);
00917 extern DdNode * Cudd_bddInterval (DdManager * dd, int N, DdNode ** x, unsigned int lowerB, unsigned int upperB);
00918 extern DdNode * Cudd_CProjection (DdManager *dd, DdNode *R, DdNode *Y);
00919 extern DdNode * Cudd_addHamming (DdManager *dd, DdNode **xVars, DdNode **yVars, int nVars);
00920 extern int Cudd_MinHammingDist (DdManager *dd, DdNode *f, int *minterm, int upperBound);
00921 extern DdNode * Cudd_bddClosestCube (DdManager *dd, DdNode * f, DdNode *g, int *distance);
00922 extern 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);
00923 extern 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);
00924 extern void Cudd_Ref (DdNode *n);
00925 extern void Cudd_RecursiveDeref (DdManager *table, DdNode *n);
00926 extern void Cudd_IterDerefBdd (DdManager *table, DdNode *n);
00927 extern void Cudd_DelayedDerefBdd (DdManager * table, DdNode * n);
00928 extern void Cudd_RecursiveDerefZdd (DdManager *table, DdNode *n);
00929 extern void Cudd_Deref (DdNode *node);
00930 extern int Cudd_CheckZeroRef (DdManager *manager);
00931 extern int Cudd_ReduceHeap (DdManager *table, Cudd_ReorderingType heuristic, int minsize);
00932 extern int Cudd_ShuffleHeap (DdManager *table, int *permutation);
00933 extern DdNode * Cudd_Eval (DdManager *dd, DdNode *f, int *inputs);
00934 extern DdNode * Cudd_ShortestPath (DdManager *manager, DdNode *f, int *weight, int *support, int *length);
00935 extern DdNode * Cudd_LargestCube (DdManager *manager, DdNode *f, int *length);
00936 extern int Cudd_ShortestLength (DdManager *manager, DdNode *f, int *weight);
00937 extern DdNode * Cudd_Decreasing (DdManager *dd, DdNode *f, int i);
00938 extern DdNode * Cudd_Increasing (DdManager *dd, DdNode *f, int i);
00939 extern int Cudd_EquivDC (DdManager *dd, DdNode *F, DdNode *G, DdNode *D);
00940 extern int Cudd_bddLeqUnless (DdManager *dd, DdNode *f, DdNode *g, DdNode *D);
00941 extern int Cudd_EqualSupNorm (DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr);
00942 extern DdNode * Cudd_bddMakePrime (DdManager *dd, DdNode *cube, DdNode *f);
00943 extern double * Cudd_CofMinterm (DdManager *dd, DdNode *node);
00944 extern DdNode * Cudd_SolveEqn (DdManager * bdd, DdNode *F, DdNode *Y, DdNode **G, int **yIndex, int n);
00945 extern DdNode * Cudd_VerifySol (DdManager * bdd, DdNode *F, DdNode **G, int *yIndex, int n);
00946 extern DdNode * Cudd_SplitSet (DdManager *manager, DdNode *S, DdNode **xVars, int n, double m);
00947 extern DdNode * Cudd_SubsetHeavyBranch (DdManager *dd, DdNode *f, int numVars, int threshold);
00948 extern DdNode * Cudd_SupersetHeavyBranch (DdManager *dd, DdNode *f, int numVars, int threshold);
00949 extern DdNode * Cudd_SubsetShortPaths (DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit);
00950 extern DdNode * Cudd_SupersetShortPaths (DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit);
00951 extern void Cudd_SymmProfile (DdManager *table, int lower, int upper);
00952 extern unsigned int Cudd_Prime (unsigned int p);
00953 extern int Cudd_PrintMinterm (DdManager *manager, DdNode *node);
00954 extern int Cudd_bddPrintCover (DdManager *dd, DdNode *l, DdNode *u);
00955 extern int Cudd_PrintDebug (DdManager *dd, DdNode *f, int n, int pr);
00956 extern int Cudd_DagSize (DdNode *node);
00957 extern int Cudd_EstimateCofactor (DdManager *dd, DdNode * node, int i, int phase);
00958 extern int Cudd_EstimateCofactorSimple (DdNode * node, int i);
00959 extern int Cudd_SharingSize (DdNode **nodeArray, int n);
00960 extern double Cudd_CountMinterm (DdManager *manager, DdNode *node, int nvars);
00961 extern int Cudd_EpdCountMinterm (DdManager *manager, DdNode *node, int nvars, EpDouble *epd);
00962 extern double Cudd_CountPath (DdNode *node);
00963 extern double Cudd_CountPathsToNonZero (DdNode *node);
00964 extern DdNode * Cudd_Support (DdManager *dd, DdNode *f);
00965 extern int * Cudd_SupportIndex (DdManager *dd, DdNode *f);
00966 extern int Cudd_SupportSize (DdManager *dd, DdNode *f);
00967 extern DdNode * Cudd_VectorSupport (DdManager *dd, DdNode **F, int n);
00968 extern int * Cudd_VectorSupportIndex (DdManager *dd, DdNode **F, int n);
00969 extern int Cudd_VectorSupportSize (DdManager *dd, DdNode **F, int n);
00970 extern int Cudd_ClassifySupport (DdManager *dd, DdNode *f, DdNode *g, DdNode **common, DdNode **onlyF, DdNode **onlyG);
00971 extern int Cudd_CountLeaves (DdNode *node);
00972 extern int Cudd_bddPickOneCube (DdManager *ddm, DdNode *node, char *string);
00973 extern DdNode * Cudd_bddPickOneMinterm (DdManager *dd, DdNode *f, DdNode **vars, int n);
00974 extern DdNode ** Cudd_bddPickArbitraryMinterms (DdManager *dd, DdNode *f, DdNode **vars, int n, int k);
00975 extern DdNode * Cudd_SubsetWithMaskVars (DdManager *dd, DdNode *f, DdNode **vars, int nvars, DdNode **maskVars, int mvars);
00976 extern DdGen * Cudd_FirstCube (DdManager *dd, DdNode *f, int **cube, CUDD_VALUE_TYPE *value);
00977 extern int Cudd_NextCube (DdGen *gen, int **cube, CUDD_VALUE_TYPE *value);
00978 extern DdGen * Cudd_FirstPrime(DdManager *dd, DdNode *l, DdNode *u, int **cube);
00979 extern int Cudd_NextPrime(DdGen *gen, int **cube);
00980 extern DdNode * Cudd_bddComputeCube (DdManager *dd, DdNode **vars, int *phase, int n);
00981 extern DdNode * Cudd_addComputeCube (DdManager *dd, DdNode **vars, int *phase, int n);
00982 extern DdNode * Cudd_CubeArrayToBdd (DdManager *dd, int *array);
00983 extern int Cudd_BddToCubeArray (DdManager *dd, DdNode *cube, int *array);
00984 extern DdGen * Cudd_FirstNode (DdManager *dd, DdNode *f, DdNode **node);
00985 extern int Cudd_NextNode (DdGen *gen, DdNode **node);
00986 extern int Cudd_GenFree (DdGen *gen);
00987 extern int Cudd_IsGenEmpty (DdGen *gen);
00988 extern DdNode * Cudd_IndicesToCube (DdManager *dd, int *array, int n);
00989 extern void Cudd_PrintVersion (FILE *fp);
00990 extern double Cudd_AverageDistance (DdManager *dd);
00991 extern long Cudd_Random (void);
00992 extern void Cudd_Srandom (long seed);
00993 extern double Cudd_Density (DdManager *dd, DdNode *f, int nvars);
00994 extern void Cudd_OutOfMem (long size);
00995 extern int Cudd_zddCount (DdManager *zdd, DdNode *P);
00996 extern double Cudd_zddCountDouble (DdManager *zdd, DdNode *P);
00997 extern DdNode * Cudd_zddProduct (DdManager *dd, DdNode *f, DdNode *g);
00998 extern DdNode * Cudd_zddUnateProduct (DdManager *dd, DdNode *f, DdNode *g);
00999 extern DdNode * Cudd_zddWeakDiv (DdManager *dd, DdNode *f, DdNode *g);
01000 extern DdNode * Cudd_zddDivide (DdManager *dd, DdNode *f, DdNode *g);
01001 extern DdNode * Cudd_zddWeakDivF (DdManager *dd, DdNode *f, DdNode *g);
01002 extern DdNode * Cudd_zddDivideF (DdManager *dd, DdNode *f, DdNode *g);
01003 extern DdNode * Cudd_zddComplement (DdManager *dd, DdNode *node);
01004 extern MtrNode * Cudd_MakeZddTreeNode (DdManager *dd, unsigned int low, unsigned int size, unsigned int type);
01005 extern DdNode * Cudd_zddIsop (DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I);
01006 extern DdNode * Cudd_bddIsop (DdManager *dd, DdNode *L, DdNode *U);
01007 extern DdNode * Cudd_MakeBddFromZddCover (DdManager *dd, DdNode *node);
01008 extern int Cudd_zddDagSize (DdNode *p_node);
01009 extern double Cudd_zddCountMinterm (DdManager *zdd, DdNode *node, int path);
01010 extern void Cudd_zddPrintSubtable (DdManager *table);
01011 extern DdNode * Cudd_zddPortFromBdd (DdManager *dd, DdNode *B);
01012 extern DdNode * Cudd_zddPortToBdd (DdManager *dd, DdNode *f);
01013 extern int Cudd_zddReduceHeap (DdManager *table, Cudd_ReorderingType heuristic, int minsize);
01014 extern int Cudd_zddShuffleHeap (DdManager *table, int *permutation);
01015 extern DdNode * Cudd_zddIte (DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
01016 extern DdNode * Cudd_zddUnion (DdManager *dd, DdNode *P, DdNode *Q);
01017 extern DdNode * Cudd_zddIntersect (DdManager *dd, DdNode *P, DdNode *Q);
01018 extern DdNode * Cudd_zddDiff (DdManager *dd, DdNode *P, DdNode *Q);
01019 extern DdNode * Cudd_zddDiffConst (DdManager *zdd, DdNode *P, DdNode *Q);
01020 extern DdNode * Cudd_zddSubset1 (DdManager *dd, DdNode *P, int var);
01021 extern DdNode * Cudd_zddSubset0 (DdManager *dd, DdNode *P, int var);
01022 extern DdNode * Cudd_zddChange (DdManager *dd, DdNode *P, int var);
01023 extern void Cudd_zddSymmProfile (DdManager *table, int lower, int upper);
01024 extern int Cudd_zddPrintMinterm (DdManager *zdd, DdNode *node);
01025 extern int Cudd_zddPrintCover (DdManager *zdd, DdNode *node);
01026 extern int Cudd_zddPrintDebug (DdManager *zdd, DdNode *f, int n, int pr);
01027 extern DdGen * Cudd_zddFirstPath (DdManager *zdd, DdNode *f, int **path);
01028 extern int Cudd_zddNextPath (DdGen *gen, int **path);
01029 extern char * Cudd_zddCoverPathToString (DdManager *zdd, int *path, char *str);
01030 extern int Cudd_zddDumpDot (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
01031 extern int Cudd_bddSetPiVar (DdManager *dd, int index);
01032 extern int Cudd_bddSetPsVar (DdManager *dd, int index);
01033 extern int Cudd_bddSetNsVar (DdManager *dd, int index);
01034 extern int Cudd_bddIsPiVar (DdManager *dd, int index);
01035 extern int Cudd_bddIsPsVar (DdManager *dd, int index);
01036 extern int Cudd_bddIsNsVar (DdManager *dd, int index);
01037 extern int Cudd_bddSetPairIndex (DdManager *dd, int index, int pairIndex);
01038 extern int Cudd_bddReadPairIndex (DdManager *dd, int index);
01039 extern int Cudd_bddSetVarToBeGrouped (DdManager *dd, int index);
01040 extern int Cudd_bddSetVarHardGroup (DdManager *dd, int index);
01041 extern int Cudd_bddResetVarToBeGrouped (DdManager *dd, int index);
01042 extern int Cudd_bddIsVarToBeGrouped (DdManager *dd, int index);
01043 extern int Cudd_bddSetVarToBeUngrouped (DdManager *dd, int index);
01044 extern int Cudd_bddIsVarToBeUngrouped (DdManager *dd, int index);
01045 extern int Cudd_bddIsVarHardGroup (DdManager *dd, int index);
01046
01049 #ifdef __cplusplus
01050 }
01051 #endif
01052
01053 #endif
