assets/doxygen-cudd-documentation/cudd_8h_source.html

 #ifndef CUDD_H_
 #define CUDD_H_

 /*---------------------------------------------------------------------------*/
 /* Nested includes                                                           */
 /*---------------------------------------------------------------------------*/

 #include <inttypes.h>

 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/

 #define CUDD_TRUE 1
 #define CUDD_FALSE 0
 #define CUDD_OUT_OF_MEM     -1
 /* The sizes of the subtables and the cache must be powers of two. */
 #define CUDD_UNIQUE_SLOTS   256
 #define CUDD_CACHE_SLOTS    262144
 /* Constants for residue functions. */
 #define CUDD_RESIDUE_DEFAULT    0
 #define CUDD_RESIDUE_MSB    1
 #define CUDD_RESIDUE_TC     2

 /*---------------------------------------------------------------------------*/
 /* Stucture declarations                                                     */
 /*---------------------------------------------------------------------------*/


 /*---------------------------------------------------------------------------*/
 /* Type declarations                                                         */
 /*---------------------------------------------------------------------------*/

 typedef enum {
     CUDD_REORDER_SAME,
     CUDD_REORDER_NONE,
     CUDD_REORDER_RANDOM,
     CUDD_REORDER_RANDOM_PIVOT,
     CUDD_REORDER_SIFT,
     CUDD_REORDER_SIFT_CONVERGE,
     CUDD_REORDER_SYMM_SIFT,
     CUDD_REORDER_SYMM_SIFT_CONV,
     CUDD_REORDER_WINDOW2,
     CUDD_REORDER_WINDOW3,
     CUDD_REORDER_WINDOW4,
     CUDD_REORDER_WINDOW2_CONV,
     CUDD_REORDER_WINDOW3_CONV,
     CUDD_REORDER_WINDOW4_CONV,
     CUDD_REORDER_GROUP_SIFT,
     CUDD_REORDER_GROUP_SIFT_CONV,
     CUDD_REORDER_ANNEALING,
     CUDD_REORDER_GENETIC,
     CUDD_REORDER_LINEAR,
     CUDD_REORDER_LINEAR_CONVERGE,
     CUDD_REORDER_LAZY_SIFT,
     CUDD_REORDER_EXACT
 } Cudd_ReorderingType;


 typedef enum {
     CUDD_NO_CHECK,
     CUDD_GROUP_CHECK,
     CUDD_GROUP_CHECK2,
     CUDD_GROUP_CHECK3,
     CUDD_GROUP_CHECK4,
     CUDD_GROUP_CHECK5,
     CUDD_GROUP_CHECK6,
     CUDD_GROUP_CHECK7,
     CUDD_GROUP_CHECK8,
     CUDD_GROUP_CHECK9
 } Cudd_AggregationType;


 typedef enum {
     CUDD_PRE_GC_HOOK,
     CUDD_POST_GC_HOOK,
     CUDD_PRE_REORDERING_HOOK,
     CUDD_POST_REORDERING_HOOK
 } Cudd_HookType;


 typedef enum {
     CUDD_NO_ERROR,
     CUDD_MEMORY_OUT,
     CUDD_TOO_MANY_NODES,
     CUDD_MAX_MEM_EXCEEDED,
     CUDD_TIMEOUT_EXPIRED,
     CUDD_TERMINATION,
     CUDD_INVALID_ARG,
     CUDD_INTERNAL_ERROR
 } Cudd_ErrorType;


 typedef enum {
     CUDD_LAZY_NONE,
     CUDD_LAZY_SOFT_GROUP,
     CUDD_LAZY_HARD_GROUP,
     CUDD_LAZY_UNGROUP
 } Cudd_LazyGroupType;


 typedef enum {
     CUDD_VAR_PRIMARY_INPUT,
     CUDD_VAR_PRESENT_STATE,
     CUDD_VAR_NEXT_STATE
 } Cudd_VariableType;

 typedef double CUDD_VALUE_TYPE;

 typedef struct DdNode DdNode;

 typedef DdNode *DdNodePtr;

 typedef struct DdManager DdManager;

 typedef struct DdGen DdGen;

 typedef uint32_t DdApaDigit;

 typedef DdApaDigit * DdApaNumber;

 typedef DdApaDigit const * DdConstApaNumber;

 typedef struct DdTlcInfo DdTlcInfo;

 typedef int (*DD_HFP)(DdManager *, const char *, void *);
 typedef DdNode * (*DD_PRFP)(DdManager * , int, DdNode **, DdNode **, DdNode **);
 typedef DdNode * (*DD_AOP)(DdManager *, DdNode **, DdNode **);
 typedef DdNode * (*DD_MAOP)(DdManager *, DdNode *);
 typedef DdNode * (*DD_CTFP)(DdManager *, DdNode *, DdNode *);
 typedef DdNode * (*DD_CTFP1)(DdManager *, DdNode *);
 typedef void (*DD_OOMFP)(size_t);
 typedef int (*DD_QSFP)(const void *, const void *);
 typedef int (*DD_THFP)(const void *);
 typedef void (*DD_TOHFP)(DdManager *, void *);

 /*---------------------------------------------------------------------------*/
 /* Variable declarations                                                     */
 /*---------------------------------------------------------------------------*/


 /*---------------------------------------------------------------------------*/
 /* Macro declarations                                                        */
 /*---------------------------------------------------------------------------*/


 #define Cudd_Not(node) ((DdNode *)((uintptr_t)(node) ^ (uintptr_t) 01))


 #define Cudd_NotCond(node,c) ((DdNode *)((uintptr_t)(node) ^ (uintptr_t) (c)))


 #define Cudd_Regular(node) ((DdNode *)((uintptr_t)(node) & ~(uintptr_t) 01))


 #define Cudd_Complement(node) ((DdNode *)((uintptr_t)(node) | (uintptr_t) 01))


 #define Cudd_IsComplement(node) ((int) ((uintptr_t) (node) & (uintptr_t) 01))


 #define Cudd_ReadIndex(dd,index) (Cudd_ReadPerm(dd,index))


 #define Cudd_ForeachCube(manager, f, gen, cube, value)\
     for((gen) = Cudd_FirstCube(manager, f, &cube, &value);\
     Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : CUDD_TRUE;\
     (void) Cudd_NextCube(gen, &cube, &value))


 #define Cudd_ForeachPrime(manager, l, u, gen, cube)\
     for((gen) = Cudd_FirstPrime(manager, l, u, &cube);\
     Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : CUDD_TRUE;\
     (void) Cudd_NextPrime(gen, &cube))


 #define Cudd_ForeachNode(manager, f, gen, node)\
     for((gen) = Cudd_FirstNode(manager, f, &node);\
     Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : CUDD_TRUE;\
     (void) Cudd_NextNode(gen, &node))


 #define Cudd_zddForeachPath(manager, f, gen, path)\
     for((gen) = Cudd_zddFirstPath(manager, f, &path);\
     Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : CUDD_TRUE;\
     (void) Cudd_zddNextPath(gen, &path))


 /*---------------------------------------------------------------------------*/
 /* Function prototypes                                                       */
 /*---------------------------------------------------------------------------*/

 #ifdef __cplusplus
 extern "C" {
 #endif

 extern DdNode * Cudd_addNewVar(DdManager *dd);
 extern DdNode * Cudd_addNewVarAtLevel(DdManager *dd, int level);
 extern DdNode * Cudd_bddNewVar(DdManager *dd);
 extern DdNode * Cudd_bddNewVarAtLevel(DdManager *dd, int level);
 extern int Cudd_bddIsVar(DdManager * dd, DdNode * f);
 extern DdNode * Cudd_addIthVar(DdManager *dd, int i);
 extern DdNode * Cudd_bddIthVar(DdManager *dd, int i);
 extern DdNode * Cudd_zddIthVar(DdManager *dd, int i);
 extern int Cudd_zddVarsFromBddVars(DdManager *dd, int multiplicity);
 extern unsigned int Cudd_ReadMaxIndex(void);
 extern DdNode * Cudd_addConst(DdManager *dd, CUDD_VALUE_TYPE c);
 extern int Cudd_IsConstant(DdNode *node);
 extern int Cudd_IsNonConstant(DdNode *f);
 extern DdNode * Cudd_T(DdNode *node);
 extern DdNode * Cudd_E(DdNode *node);
 extern CUDD_VALUE_TYPE Cudd_V(DdNode *node);
 extern unsigned long Cudd_ReadStartTime(DdManager *unique);
 extern unsigned long Cudd_ReadElapsedTime(DdManager *unique);
 extern void Cudd_SetStartTime(DdManager *unique, unsigned long st);
 extern void Cudd_ResetStartTime(DdManager *unique);
 extern unsigned long Cudd_ReadTimeLimit(DdManager *unique);
 extern unsigned long Cudd_SetTimeLimit(DdManager *unique, unsigned long tl);
 extern void Cudd_UpdateTimeLimit(DdManager * unique);
 extern void Cudd_IncreaseTimeLimit(DdManager * unique, unsigned long increase);
 extern void Cudd_UnsetTimeLimit(DdManager *unique);
 extern int Cudd_TimeLimited(DdManager *unique);
 extern void Cudd_RegisterTerminationCallback(DdManager *unique, DD_THFP callback, void * callback_arg);
 extern void Cudd_UnregisterTerminationCallback(DdManager *unique);
 extern DD_OOMFP Cudd_RegisterOutOfMemoryCallback(DdManager *unique, DD_OOMFP callback);
 extern void Cudd_UnregisterOutOfMemoryCallback(DdManager *unique);
 extern void Cudd_RegisterTimeoutHandler(DdManager *unique, DD_TOHFP handler, void *arg);
 extern DD_TOHFP Cudd_ReadTimeoutHandler(DdManager *unique, void **argp);
 extern void Cudd_AutodynEnable(DdManager *unique, Cudd_ReorderingType method);
 extern void Cudd_AutodynDisable(DdManager *unique);
 extern int Cudd_ReorderingStatus(DdManager *unique, Cudd_ReorderingType *method);
 extern void Cudd_AutodynEnableZdd(DdManager *unique, Cudd_ReorderingType method);
 extern void Cudd_AutodynDisableZdd(DdManager *unique);
 extern int Cudd_ReorderingStatusZdd(DdManager *unique, Cudd_ReorderingType *method);
 extern int Cudd_zddRealignmentEnabled(DdManager *unique);
 extern void Cudd_zddRealignEnable(DdManager *unique);
 extern void Cudd_zddRealignDisable(DdManager *unique);
 extern int Cudd_bddRealignmentEnabled(DdManager *unique);
 extern void Cudd_bddRealignEnable(DdManager *unique);
 extern void Cudd_bddRealignDisable(DdManager *unique);
 extern DdNode * Cudd_ReadOne(DdManager *dd);
 extern DdNode * Cudd_ReadZddOne(DdManager *dd, int i);
 extern DdNode * Cudd_ReadZero(DdManager *dd);
 extern DdNode * Cudd_ReadLogicZero(DdManager *dd);
 extern DdNode * Cudd_ReadPlusInfinity(DdManager *dd);
 extern DdNode * Cudd_ReadMinusInfinity(DdManager *dd);
 extern DdNode * Cudd_ReadBackground(DdManager *dd);
 extern void Cudd_SetBackground(DdManager *dd, DdNode *bck);
 extern unsigned int Cudd_ReadCacheSlots(DdManager *dd);
 extern double Cudd_ReadCacheUsedSlots(DdManager * dd);
 extern double Cudd_ReadCacheLookUps(DdManager *dd);
 extern double Cudd_ReadCacheHits(DdManager *dd);
 extern double Cudd_ReadRecursiveCalls(DdManager * dd);
 extern unsigned int Cudd_ReadMinHit(DdManager *dd);
 extern void Cudd_SetMinHit(DdManager *dd, unsigned int hr);
 extern unsigned int Cudd_ReadLooseUpTo(DdManager *dd);
 extern void Cudd_SetLooseUpTo(DdManager *dd, unsigned int lut);
 extern unsigned int Cudd_ReadMaxCache(DdManager *dd);
 extern unsigned int Cudd_ReadMaxCacheHard(DdManager *dd);
 extern void Cudd_SetMaxCacheHard(DdManager *dd, unsigned int mc);
 extern int Cudd_ReadSize(DdManager *dd);
 extern int Cudd_ReadZddSize(DdManager *dd);
 extern unsigned int Cudd_ReadSlots(DdManager *dd);
 extern double Cudd_ReadUsedSlots(DdManager * dd);
 extern double Cudd_ExpectedUsedSlots(DdManager * dd);
 extern unsigned int Cudd_ReadKeys(DdManager *dd);
 extern unsigned int Cudd_ReadDead(DdManager *dd);
 extern unsigned int Cudd_ReadMinDead(DdManager *dd);
 extern unsigned int Cudd_ReadReorderings(DdManager *dd);
 extern unsigned int Cudd_ReadMaxReorderings(DdManager *dd);
 extern void Cudd_SetMaxReorderings(DdManager *dd, unsigned int mr);
 extern long Cudd_ReadReorderingTime(DdManager * dd);
 extern int Cudd_ReadGarbageCollections(DdManager * dd);
 extern long Cudd_ReadGarbageCollectionTime(DdManager * dd);
 extern double Cudd_ReadNodesFreed(DdManager * dd);
 extern double Cudd_ReadNodesDropped(DdManager * dd);
 extern double Cudd_ReadUniqueLookUps(DdManager * dd);
 extern double Cudd_ReadUniqueLinks(DdManager * dd);
 extern int Cudd_ReadSiftMaxVar(DdManager *dd);
 extern void Cudd_SetSiftMaxVar(DdManager *dd, int smv);
 extern int Cudd_ReadSiftMaxSwap(DdManager *dd);
 extern void Cudd_SetSiftMaxSwap(DdManager *dd, int sms);
 extern double Cudd_ReadMaxGrowth(DdManager *dd);
 extern void Cudd_SetMaxGrowth(DdManager *dd, double mg);
 extern double Cudd_ReadMaxGrowthAlternate(DdManager * dd);
 extern void Cudd_SetMaxGrowthAlternate(DdManager * dd, double mg);
 extern int Cudd_ReadReorderingCycle(DdManager * dd);
 extern void Cudd_SetReorderingCycle(DdManager * dd, int cycle);
 extern unsigned int Cudd_NodeReadIndex(DdNode *node);
 extern int Cudd_ReadPerm(DdManager *dd, int i);
 extern int Cudd_ReadPermZdd(DdManager *dd, int i);
 extern int Cudd_ReadInvPerm(DdManager *dd, int i);
 extern int Cudd_ReadInvPermZdd(DdManager *dd, int i);
 extern DdNode * Cudd_ReadVars(DdManager *dd, int i);
 extern CUDD_VALUE_TYPE Cudd_ReadEpsilon(DdManager *dd);
 extern void Cudd_SetEpsilon(DdManager *dd, CUDD_VALUE_TYPE ep);
 extern Cudd_AggregationType Cudd_ReadGroupcheck(DdManager *dd);
 extern void Cudd_SetGroupcheck(DdManager *dd, Cudd_AggregationType gc);
 extern int Cudd_GarbageCollectionEnabled(DdManager *dd);
 extern void Cudd_EnableGarbageCollection(DdManager *dd);
 extern void Cudd_DisableGarbageCollection(DdManager *dd);
 extern int Cudd_DeadAreCounted(DdManager *dd);
 extern void Cudd_TurnOnCountDead(DdManager *dd);
 extern void Cudd_TurnOffCountDead(DdManager *dd);
 extern int Cudd_ReadRecomb(DdManager *dd);
 extern void Cudd_SetRecomb(DdManager *dd, int recomb);
 extern int Cudd_ReadSymmviolation(DdManager *dd);
 extern void Cudd_SetSymmviolation(DdManager *dd, int symmviolation);
 extern int Cudd_ReadArcviolation(DdManager *dd);
 extern void Cudd_SetArcviolation(DdManager *dd, int arcviolation);
 extern int Cudd_ReadPopulationSize(DdManager *dd);
 extern void Cudd_SetPopulationSize(DdManager *dd, int populationSize);
 extern int Cudd_ReadNumberXovers(DdManager *dd);
 extern void Cudd_SetNumberXovers(DdManager *dd, int numberXovers);
 extern unsigned int Cudd_ReadOrderRandomization(DdManager * dd);
 extern void Cudd_SetOrderRandomization(DdManager * dd, unsigned int factor);
 extern size_t Cudd_ReadMemoryInUse(DdManager *dd);
 extern int Cudd_PrintInfo(DdManager *dd, FILE *fp);
 extern long Cudd_ReadPeakNodeCount(DdManager *dd);
 extern int Cudd_ReadPeakLiveNodeCount(DdManager * dd);
 extern long Cudd_ReadNodeCount(DdManager *dd);
 extern long Cudd_zddReadNodeCount(DdManager *dd);
 extern int Cudd_AddHook(DdManager *dd, DD_HFP f, Cudd_HookType where);
 extern int Cudd_RemoveHook(DdManager *dd, DD_HFP f, Cudd_HookType where);
 extern int Cudd_IsInHook(DdManager * dd, DD_HFP f, Cudd_HookType where);
 extern int Cudd_StdPreReordHook(DdManager *dd, const char *str, void *data);
 extern int Cudd_StdPostReordHook(DdManager *dd, const char *str, void *data);
 extern int Cudd_EnableReorderingReporting(DdManager *dd);
 extern int Cudd_DisableReorderingReporting(DdManager *dd);
 extern int Cudd_ReorderingReporting(DdManager *dd);
 extern int Cudd_PrintGroupedOrder(DdManager * dd, const char *str, void *data);
 extern int Cudd_EnableOrderingMonitoring(DdManager *dd);
 extern int Cudd_DisableOrderingMonitoring(DdManager *dd);
 extern int Cudd_OrderingMonitoring(DdManager *dd);
 extern void Cudd_SetApplicationHook(DdManager *dd, void * value);
 extern void * Cudd_ReadApplicationHook(DdManager *dd);
 extern Cudd_ErrorType Cudd_ReadErrorCode(DdManager *dd);
 extern void Cudd_ClearErrorCode(DdManager *dd);
 extern DD_OOMFP Cudd_InstallOutOfMemoryHandler(DD_OOMFP newHandler);
 extern FILE * Cudd_ReadStdout(DdManager *dd);
 extern void Cudd_SetStdout(DdManager *dd, FILE *fp);
 extern FILE * Cudd_ReadStderr(DdManager *dd);
 extern void Cudd_SetStderr(DdManager *dd, FILE *fp);
 extern unsigned int Cudd_ReadNextReordering(DdManager *dd);
 extern void Cudd_SetNextReordering(DdManager *dd, unsigned int next);
 extern double Cudd_ReadSwapSteps(DdManager *dd);
 extern unsigned int Cudd_ReadMaxLive(DdManager *dd);
 extern void Cudd_SetMaxLive(DdManager *dd, unsigned int maxLive);
 extern size_t Cudd_ReadMaxMemory(DdManager *dd);
 extern size_t Cudd_SetMaxMemory(DdManager *dd, size_t maxMemory);
 extern int Cudd_bddBindVar(DdManager *dd, int index);
 extern int Cudd_bddUnbindVar(DdManager *dd, int index);
 extern int Cudd_bddVarIsBound(DdManager *dd, int index);
 extern DdNode * Cudd_addExistAbstract(DdManager *manager, DdNode *f, DdNode *cube);
 extern DdNode * Cudd_addUnivAbstract(DdManager *manager, DdNode *f, DdNode *cube);
 extern DdNode * Cudd_addOrAbstract(DdManager *manager, DdNode *f, DdNode *cube);
 extern DdNode * Cudd_addApply(DdManager *dd, DD_AOP op, DdNode *f, DdNode *g);
 extern DdNode * Cudd_addPlus(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addTimes(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addThreshold(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addSetNZ(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addDivide(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addMinus(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addMinimum(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addMaximum(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addOneZeroMaximum(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addDiff(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addAgreement(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addOr(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addNand(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addNor(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addXor(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addXnor(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addMonadicApply(DdManager * dd, DD_MAOP op, DdNode * f);
 extern DdNode * Cudd_addLog(DdManager * dd, DdNode * f);
 extern DdNode * Cudd_addFindMax(DdManager *dd, DdNode *f);
 extern DdNode * Cudd_addFindMin(DdManager *dd, DdNode *f);
 extern DdNode * Cudd_addIthBit(DdManager *dd, DdNode *f, int bit);
 extern DdNode * Cudd_addScalarInverse(DdManager *dd, DdNode *f, DdNode *epsilon);
 extern DdNode * Cudd_addIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
 extern DdNode * Cudd_addIteConstant(DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
 extern DdNode * Cudd_addEvalConst(DdManager *dd, DdNode *f, DdNode *g);
 extern int Cudd_addLeq(DdManager * dd, DdNode * f, DdNode * g);
 extern DdNode * Cudd_addCmpl(DdManager *dd, DdNode *f);
 extern DdNode * Cudd_addNegate(DdManager *dd, DdNode *f);
 extern DdNode * Cudd_addRoundOff(DdManager *dd, DdNode *f, int N);
 extern DdNode * Cudd_addWalsh(DdManager *dd, DdNode **x, DdNode **y, int n);
 extern DdNode * Cudd_addResidue(DdManager *dd, int n, int m, int options, int top);
 extern DdNode * Cudd_bddAndAbstract(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube);
 extern DdNode * Cudd_bddAndAbstractLimit(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, unsigned int limit);
 extern int Cudd_ApaNumberOfDigits(int binaryDigits);
 extern DdApaNumber Cudd_NewApaNumber(int digits);
 extern void Cudd_FreeApaNumber(DdApaNumber number);
 extern void Cudd_ApaCopy(int digits, DdConstApaNumber source, DdApaNumber dest);
 extern DdApaDigit Cudd_ApaAdd(int digits, DdConstApaNumber a, DdConstApaNumber b, DdApaNumber sum);
 extern DdApaDigit Cudd_ApaSubtract(int digits, DdConstApaNumber a, DdConstApaNumber b, DdApaNumber diff);
 extern DdApaDigit Cudd_ApaShortDivision(int digits, DdConstApaNumber dividend, DdApaDigit divisor, DdApaNumber quotient);
 extern unsigned int Cudd_ApaIntDivision(int  digits, DdConstApaNumber dividend, unsigned int  divisor, DdApaNumber  quotient);
 extern void Cudd_ApaShiftRight(int digits, DdApaDigit in, DdConstApaNumber a, DdApaNumber b);
 extern void Cudd_ApaSetToLiteral(int digits, DdApaNumber number, DdApaDigit literal);
 extern void Cudd_ApaPowerOfTwo(int digits, DdApaNumber number, int power);
 extern int Cudd_ApaCompare(int digitsFirst, DdConstApaNumber first, int digitsSecond, DdConstApaNumber second);
 extern int Cudd_ApaCompareRatios(int digitsFirst, DdConstApaNumber firstNum, unsigned int firstDen, int digitsSecond, DdConstApaNumber secondNum, unsigned int secondDen);
 extern int Cudd_ApaPrintHex(FILE *fp, int digits, DdConstApaNumber number);
 extern int Cudd_ApaPrintDecimal(FILE *fp, int digits, DdConstApaNumber number);
 extern char * Cudd_ApaStringDecimal(int digits, DdConstApaNumber number);
 extern int Cudd_ApaPrintExponential(FILE * fp, int  digits, DdConstApaNumber number, int precision);
 extern DdApaNumber Cudd_ApaCountMinterm(DdManager const *manager, DdNode *node, int nvars, int *digits);
 extern int Cudd_ApaPrintMinterm(FILE *fp, DdManager const *dd, DdNode *node, int nvars);
 extern int Cudd_ApaPrintMintermExp(FILE * fp, DdManager const * dd, DdNode *node, int  nvars, int precision);
 extern int Cudd_ApaPrintDensity(FILE * fp, DdManager * dd, DdNode * node, int  nvars);
 extern DdNode * Cudd_UnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality);
 extern DdNode * Cudd_OverApprox(DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality);
 extern DdNode * Cudd_RemapUnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, double quality);
 extern DdNode * Cudd_RemapOverApprox(DdManager *dd, DdNode *f, int numVars, int threshold, double quality);
 extern DdNode * Cudd_BiasedUnderApprox(DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0);
 extern DdNode * Cudd_BiasedOverApprox(DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0);
 extern DdNode * Cudd_bddExistAbstract(DdManager *manager, DdNode *f, DdNode *cube);
 extern DdNode * Cudd_bddExistAbstractLimit(DdManager * manager, DdNode * f, DdNode * cube, unsigned int limit);
 extern DdNode * Cudd_bddXorExistAbstract(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube);
 extern DdNode * Cudd_bddUnivAbstract(DdManager *manager, DdNode *f, DdNode *cube);
 extern DdNode * Cudd_bddBooleanDiff(DdManager *manager, DdNode *f, int x);
 extern int Cudd_bddVarIsDependent(DdManager *dd, DdNode *f, DdNode *var);
 extern double Cudd_bddCorrelation(DdManager *manager, DdNode *f, DdNode *g);
 extern double Cudd_bddCorrelationWeights(DdManager *manager, DdNode *f, DdNode *g, double *prob);
 extern DdNode * Cudd_bddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
 extern DdNode * Cudd_bddIteLimit(DdManager *dd, DdNode *f, DdNode *g, DdNode *h, unsigned int limit);
 extern DdNode * Cudd_bddIteConstant(DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
 extern DdNode * Cudd_bddIntersect(DdManager *dd, DdNode *f, DdNode *g);
 extern DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g);
 extern DdNode * Cudd_bddAndLimit(DdManager *dd, DdNode *f, DdNode *g, unsigned int limit);
 extern DdNode * Cudd_bddOr(DdManager *dd, DdNode *f, DdNode *g);
 extern DdNode * Cudd_bddOrLimit(DdManager *dd, DdNode *f, DdNode *g, unsigned int limit);
 extern DdNode * Cudd_bddNand(DdManager *dd, DdNode *f, DdNode *g);
 extern DdNode * Cudd_bddNor(DdManager *dd, DdNode *f, DdNode *g);
 extern DdNode * Cudd_bddXor(DdManager *dd, DdNode *f, DdNode *g);
 extern DdNode * Cudd_bddXnor(DdManager *dd, DdNode *f, DdNode *g);
 extern DdNode * Cudd_bddXnorLimit(DdManager *dd, DdNode *f, DdNode *g, unsigned int limit);
 extern int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g);
 extern DdNode * Cudd_addBddThreshold(DdManager *dd, DdNode *f, CUDD_VALUE_TYPE value);
 extern DdNode * Cudd_addBddStrictThreshold(DdManager *dd, DdNode *f, CUDD_VALUE_TYPE value);
 extern DdNode * Cudd_addBddInterval(DdManager *dd, DdNode *f, CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper);
 extern DdNode * Cudd_addBddIthBit(DdManager *dd, DdNode *f, int bit);
 extern DdNode * Cudd_BddToAdd(DdManager *dd, DdNode *B);
 extern DdNode * Cudd_addBddPattern(DdManager *dd, DdNode *f);
 extern DdNode * Cudd_bddTransfer(DdManager *ddSource, DdManager *ddDestination, DdNode *f);
 extern int Cudd_DebugCheck(DdManager *table);
 extern int Cudd_CheckKeys(DdManager *table);
 extern DdNode * Cudd_bddClippingAnd(DdManager *dd, DdNode *f, DdNode *g, int maxDepth, int direction);
 extern DdNode * Cudd_bddClippingAndAbstract(DdManager *dd, DdNode *f, DdNode *g, DdNode *cube, int maxDepth, int direction);
 extern DdNode * Cudd_Cofactor(DdManager *dd, DdNode *f, DdNode *g);
 extern int Cudd_CheckCube(DdManager *dd, DdNode *g);
 extern int Cudd_VarsAreSymmetric(DdManager * dd, DdNode * f, int index1, int index2);
 extern DdNode * Cudd_bddCompose(DdManager *dd, DdNode *f, DdNode *g, int v);
 extern DdNode * Cudd_addCompose(DdManager *dd, DdNode *f, DdNode *g, int v);
 extern DdNode * Cudd_addPermute(DdManager *manager, DdNode *node, int *permut);
 extern DdNode * Cudd_addSwapVariables(DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n);
 extern DdNode * Cudd_bddPermute(DdManager *manager, DdNode *node, int *permut);
 extern DdNode * Cudd_bddVarMap(DdManager *manager, DdNode *f);
 extern int Cudd_SetVarMap(DdManager *manager, DdNode **x, DdNode **y, int n);
 extern DdNode * Cudd_bddSwapVariables(DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n);
 extern DdNode * Cudd_bddAdjPermuteX(DdManager *dd, DdNode *B, DdNode **x, int n);
 extern DdNode * Cudd_addVectorCompose(DdManager *dd, DdNode *f, DdNode **vector);
 extern DdNode * Cudd_addGeneralVectorCompose(DdManager *dd, DdNode *f, DdNode **vectorOn, DdNode **vectorOff);
 extern DdNode * Cudd_addNonSimCompose(DdManager *dd, DdNode *f, DdNode **vector);
 extern DdNode * Cudd_bddVectorCompose(DdManager *dd, DdNode *f, DdNode **vector);
 extern int Cudd_bddApproxConjDecomp(DdManager *dd, DdNode *f, DdNode ***conjuncts);
 extern int Cudd_bddApproxDisjDecomp(DdManager *dd, DdNode *f, DdNode ***disjuncts);
 extern int Cudd_bddIterConjDecomp(DdManager *dd, DdNode *f, DdNode ***conjuncts);
 extern int Cudd_bddIterDisjDecomp(DdManager *dd, DdNode *f, DdNode ***disjuncts);
 extern int Cudd_bddGenConjDecomp(DdManager *dd, DdNode *f, DdNode ***conjuncts);
 extern int Cudd_bddGenDisjDecomp(DdManager *dd, DdNode *f, DdNode ***disjuncts);
 extern int Cudd_bddVarConjDecomp(DdManager *dd, DdNode * f, DdNode ***conjuncts);
 extern int Cudd_bddVarDisjDecomp(DdManager *dd, DdNode * f, DdNode ***disjuncts);
 extern DdNode * Cudd_FindEssential(DdManager *dd, DdNode *f);
 extern int Cudd_bddIsVarEssential(DdManager *manager, DdNode *f, int id, int phase);
 extern DdTlcInfo * Cudd_FindTwoLiteralClauses(DdManager * dd, DdNode * f);
 extern int Cudd_PrintTwoLiteralClauses(DdManager * dd, DdNode * f, char **names, FILE *fp);
 extern int Cudd_ReadIthClause(DdTlcInfo * tlc, int i, unsigned *var1, unsigned *var2, int *phase1, int *phase2);
 extern void Cudd_tlcInfoFree(DdTlcInfo * t);
 extern int Cudd_DumpBlif(DdManager *dd, int n, DdNode **f, char const * const *inames, char const * const *onames, char *mname, FILE *fp, int mv);
 extern int Cudd_DumpBlifBody(DdManager *dd, int n, DdNode **f, char const * const *inames, char const * const *onames, FILE *fp, int mv);
 extern int Cudd_DumpDot(DdManager *dd, int n, DdNode **f, char const * const *inames, char const * const *onames, FILE *fp);
 extern int Cudd_DumpDaVinci(DdManager *dd, int n, DdNode **f, char const * const *inames, char const * const *onames, FILE *fp);
 extern int Cudd_DumpDDcal(DdManager *dd, int n, DdNode **f, char const * const *inames, char const * const *onames, FILE *fp);
 extern int Cudd_DumpFactoredForm(DdManager *dd, int n, DdNode **f, char const * const *inames, char const * const *onames, FILE *fp);
 extern char * Cudd_FactoredFormString(DdManager *dd, DdNode *f, char const * const * inames);
 extern DdNode * Cudd_bddConstrain(DdManager *dd, DdNode *f, DdNode *c);
 extern DdNode * Cudd_bddRestrict(DdManager *dd, DdNode *f, DdNode *c);
 extern DdNode * Cudd_bddNPAnd(DdManager *dd, DdNode *f, DdNode *c);
 extern DdNode * Cudd_addConstrain(DdManager *dd, DdNode *f, DdNode *c);
 extern DdNode ** Cudd_bddConstrainDecomp(DdManager *dd, DdNode *f);
 extern DdNode * Cudd_addRestrict(DdManager *dd, DdNode *f, DdNode *c);
 extern DdNode ** Cudd_bddCharToVect(DdManager *dd, DdNode *f);
 extern DdNode * Cudd_bddLICompaction(DdManager *dd, DdNode *f, DdNode *c);
 extern DdNode * Cudd_bddSqueeze(DdManager *dd, DdNode *l, DdNode *u);
 extern DdNode * Cudd_bddInterpolate(DdManager * dd, DdNode * l, DdNode * u);
 extern DdNode * Cudd_bddMinimize(DdManager *dd, DdNode *f, DdNode *c);
 extern DdNode * Cudd_SubsetCompress(DdManager *dd, DdNode *f, int nvars, int threshold);
 extern DdNode * Cudd_SupersetCompress(DdManager *dd, DdNode *f, int nvars, int threshold);
 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);
 extern DdManager * Cudd_Init(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, size_t maxMemory);
 extern void Cudd_Quit(DdManager *unique);
 extern int Cudd_PrintLinear(DdManager *table);
 extern int Cudd_ReadLinear(DdManager *table, int x, int y);
 extern DdNode * Cudd_bddLiteralSetIntersection(DdManager *dd, DdNode *f, DdNode *g);
 extern DdNode * Cudd_addMatrixMultiply(DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz);
 extern DdNode * Cudd_addTimesPlus(DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz);
 extern DdNode * Cudd_addTriangle(DdManager *dd, DdNode *f, DdNode *g, DdNode **z, int nz);
 extern DdNode * Cudd_addOuterSum(DdManager *dd, DdNode *M, DdNode *r, DdNode *c);
 extern DdNode * Cudd_PrioritySelect(DdManager *dd, DdNode *R, DdNode **x, DdNode **y, DdNode **z, DdNode *Pi, int n, DD_PRFP PiFunc);
 extern DdNode * Cudd_Xgty(DdManager *dd, int N, DdNode **z, DdNode **x, DdNode **y);
 extern DdNode * Cudd_Xeqy(DdManager *dd, int N, DdNode **x, DdNode **y);
 extern DdNode * Cudd_addXeqy(DdManager *dd, int N, DdNode **x, DdNode **y);
 extern DdNode * Cudd_Dxygtdxz(DdManager *dd, int N, DdNode **x, DdNode **y, DdNode **z);
 extern DdNode * Cudd_Dxygtdyz(DdManager *dd, int N, DdNode **x, DdNode **y, DdNode **z);
 extern DdNode * Cudd_Inequality(DdManager * dd, int  N, int c, DdNode ** x, DdNode ** y);
 extern DdNode * Cudd_Disequality(DdManager * dd, int  N, int c, DdNode ** x, DdNode ** y);
 extern DdNode * Cudd_bddInterval(DdManager * dd, int  N, DdNode ** x, unsigned int lowerB, unsigned int upperB);
 extern DdNode * Cudd_CProjection(DdManager *dd, DdNode *R, DdNode *Y);
 extern DdNode * Cudd_addHamming(DdManager *dd, DdNode **xVars, DdNode **yVars, int nVars);
 extern int Cudd_MinHammingDist(DdManager *dd, DdNode *f, int *minterm, int upperBound);
 extern DdNode * Cudd_bddClosestCube(DdManager *dd, DdNode * f, DdNode *g, int *distance);
 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);
 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);
 extern void Cudd_Ref(DdNode *n);
 extern void Cudd_RecursiveDeref(DdManager *table, DdNode *n);
 extern void Cudd_IterDerefBdd(DdManager *table, DdNode *n);
 extern void Cudd_DelayedDerefBdd(DdManager * table, DdNode * n);
 extern void Cudd_RecursiveDerefZdd(DdManager *table, DdNode *n);
 extern void Cudd_Deref(DdNode *node);
 extern int Cudd_CheckZeroRef(DdManager *manager);
 extern int Cudd_ReduceHeap(DdManager *table, Cudd_ReorderingType heuristic, int minsize);
 extern int Cudd_ShuffleHeap(DdManager *table, int *permutation);
 extern DdNode * Cudd_Eval(DdManager *dd, DdNode *f, int *inputs);
 extern DdNode * Cudd_ShortestPath(DdManager *manager, DdNode *f, int *weight, int *support, int *length);
 extern DdNode * Cudd_LargestCube(DdManager *manager, DdNode *f, int *length);
 extern int Cudd_ShortestLength(DdManager *manager, DdNode *f, int *weight);
 extern DdNode * Cudd_Decreasing(DdManager *dd, DdNode *f, int i);
 extern DdNode * Cudd_Increasing(DdManager *dd, DdNode *f, int i);
 extern int Cudd_EquivDC(DdManager *dd, DdNode *F, DdNode *G, DdNode *D);
 extern int Cudd_bddLeqUnless(DdManager *dd, DdNode *f, DdNode *g, DdNode *D);
 extern int Cudd_EqualSupNorm(DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr);
 extern DdNode * Cudd_bddMakePrime(DdManager *dd, DdNode *cube, DdNode *f);
 extern DdNode * Cudd_bddMaximallyExpand(DdManager *dd, DdNode *lb, DdNode *ub, DdNode *f);
 extern DdNode * Cudd_bddLargestPrimeUnate(DdManager *dd , DdNode *f, DdNode *phaseBdd);
 extern double * Cudd_CofMinterm(DdManager *dd, DdNode *node);
 extern DdNode * Cudd_SolveEqn(DdManager * bdd, DdNode *F, DdNode *Y, DdNode **G, int **yIndex, int n);
 extern DdNode * Cudd_VerifySol(DdManager * bdd, DdNode *F, DdNode **G, int *yIndex, int n);
 extern DdNode * Cudd_SplitSet(DdManager *manager, DdNode *S, DdNode **xVars, int n, double m);
 extern DdNode * Cudd_SubsetHeavyBranch(DdManager *dd, DdNode *f, int numVars, int threshold);
 extern DdNode * Cudd_SupersetHeavyBranch(DdManager *dd, DdNode *f, int numVars, int threshold);
 extern DdNode * Cudd_SubsetShortPaths(DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit);
 extern DdNode * Cudd_SupersetShortPaths(DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit);
 extern void Cudd_SymmProfile(DdManager *table, int lower, int upper);
 extern unsigned int Cudd_Prime(unsigned int p);
 extern int Cudd_Reserve(DdManager *manager, int amount);
 extern int Cudd_PrintMinterm(DdManager *manager, DdNode *node);
 extern int Cudd_bddPrintCover(DdManager *dd, DdNode *l, DdNode *u);
 extern int Cudd_PrintDebug(DdManager *dd, DdNode *f, int n, int pr);
 extern int Cudd_PrintSummary(DdManager * dd, DdNode * f, int n, int mode);
 extern int Cudd_DagSize(DdNode *node);
 extern int Cudd_EstimateCofactor(DdManager *dd, DdNode * node, int i, int phase);
 extern int Cudd_EstimateCofactorSimple(DdNode * node, int i);
 extern int Cudd_SharingSize(DdNode **nodeArray, int n);
 extern double Cudd_CountMinterm(DdManager *manager, DdNode *node, int nvars);
 #ifdef EPD_H_
 extern int Cudd_EpdCountMinterm(DdManager const *manager, DdNode *node, int nvars, EpDouble *epd);
 #endif
 extern long double Cudd_LdblCountMinterm(DdManager const *manager, DdNode *node, int nvars);
 extern int Cudd_EpdPrintMinterm(DdManager const * dd, DdNode * node, int nvars);
 extern double Cudd_CountPath(DdNode *node);
 extern double Cudd_CountPathsToNonZero(DdNode *node);
 extern int Cudd_SupportIndices(DdManager * dd, DdNode * f, int **indices);
 extern DdNode * Cudd_Support(DdManager *dd, DdNode *f);
 extern int * Cudd_SupportIndex(DdManager *dd, DdNode *f);
 extern int Cudd_SupportSize(DdManager *dd, DdNode *f);
 extern int Cudd_VectorSupportIndices(DdManager * dd, DdNode ** F, int n, int **indices);
 extern DdNode * Cudd_VectorSupport(DdManager *dd, DdNode **F, int n);
 extern int * Cudd_VectorSupportIndex(DdManager *dd, DdNode **F, int n);
 extern int Cudd_VectorSupportSize(DdManager *dd, DdNode **F, int n);
 extern int Cudd_ClassifySupport(DdManager *dd, DdNode *f, DdNode *g, DdNode **common, DdNode **onlyF, DdNode **onlyG);
 extern int Cudd_CountLeaves(DdNode *node);
 extern int Cudd_bddPickOneCube(DdManager *ddm, DdNode *node, char *string);
 extern DdNode * Cudd_bddPickOneMinterm(DdManager *dd, DdNode *f, DdNode **vars, int n);
 extern DdNode ** Cudd_bddPickArbitraryMinterms(DdManager *dd, DdNode *f, DdNode **vars, int n, int k);
 extern DdNode * Cudd_SubsetWithMaskVars(DdManager *dd, DdNode *f, DdNode **vars, int nvars, DdNode **maskVars, int mvars);
 extern DdGen * Cudd_FirstCube(DdManager *dd, DdNode *f, int **cube, CUDD_VALUE_TYPE *value);
 extern int Cudd_NextCube(DdGen *gen, int **cube, CUDD_VALUE_TYPE *value);
 extern DdGen * Cudd_FirstPrime(DdManager *dd, DdNode *l, DdNode *u, int **cube);
 extern int Cudd_NextPrime(DdGen *gen, int **cube);
 extern DdNode * Cudd_bddComputeCube(DdManager *dd, DdNode **vars, int *phase, int n);
 extern DdNode * Cudd_addComputeCube(DdManager *dd, DdNode **vars, int *phase, int n);
 extern DdNode * Cudd_CubeArrayToBdd(DdManager *dd, int *array);
 extern int Cudd_BddToCubeArray(DdManager *dd, DdNode *cube, int *array);
 extern DdGen * Cudd_FirstNode(DdManager *dd, DdNode *f, DdNode **node);
 extern int Cudd_NextNode(DdGen *gen, DdNode **node);
 extern int Cudd_GenFree(DdGen *gen);
 extern int Cudd_IsGenEmpty(DdGen *gen);
 extern DdNode * Cudd_IndicesToCube(DdManager *dd, int *array, int n);
 extern void Cudd_PrintVersion(FILE *fp);
 extern double Cudd_AverageDistance(DdManager *dd);
 extern int32_t Cudd_Random(DdManager * dd);
 extern void Cudd_Srandom(DdManager * dd, int32_t seed);
 extern double Cudd_Density(DdManager *dd, DdNode *f, int nvars);
 extern void Cudd_OutOfMem(size_t size);
 extern void Cudd_OutOfMemSilent(size_t size);
 extern int Cudd_zddCount(DdManager *zdd, DdNode *P);
 extern double Cudd_zddCountDouble(DdManager *zdd, DdNode *P);
 extern DdNode * Cudd_zddProduct(DdManager *dd, DdNode *f, DdNode *g);
 extern DdNode * Cudd_zddUnateProduct(DdManager *dd, DdNode *f, DdNode *g);
 extern DdNode * Cudd_zddWeakDiv(DdManager *dd, DdNode *f, DdNode *g);
 extern DdNode * Cudd_zddDivide(DdManager *dd, DdNode *f, DdNode *g);
 extern DdNode * Cudd_zddWeakDivF(DdManager *dd, DdNode *f, DdNode *g);
 extern DdNode * Cudd_zddDivideF(DdManager *dd, DdNode *f, DdNode *g);
 extern DdNode * Cudd_zddComplement(DdManager *dd, DdNode *node);
 extern DdNode * Cudd_zddIsop(DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I);
 extern DdNode * Cudd_bddIsop(DdManager *dd, DdNode *L, DdNode *U);
 extern DdNode * Cudd_MakeBddFromZddCover(DdManager *dd, DdNode *node);
 extern int Cudd_zddDagSize(DdNode *p_node);
 extern double Cudd_zddCountMinterm(DdManager *zdd, DdNode *node, int path);
 extern void Cudd_zddPrintSubtable(DdManager *table);
 extern DdNode * Cudd_zddPortFromBdd(DdManager *dd, DdNode *B);
 extern DdNode * Cudd_zddPortToBdd(DdManager *dd, DdNode *f);
 extern int Cudd_zddReduceHeap(DdManager *table, Cudd_ReorderingType heuristic, int minsize);
 extern int Cudd_zddShuffleHeap(DdManager *table, int *permutation);
 extern DdNode * Cudd_zddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
 extern DdNode * Cudd_zddUnion(DdManager *dd, DdNode *P, DdNode *Q);
 extern DdNode * Cudd_zddIntersect(DdManager *dd, DdNode *P, DdNode *Q);
 extern DdNode * Cudd_zddDiff(DdManager *dd, DdNode *P, DdNode *Q);
 extern DdNode * Cudd_zddDiffConst(DdManager *zdd, DdNode *P, DdNode *Q);
 extern DdNode * Cudd_zddSubset1(DdManager *dd, DdNode *P, int var);
 extern DdNode * Cudd_zddSubset0(DdManager *dd, DdNode *P, int var);
 extern DdNode * Cudd_zddChange(DdManager *dd, DdNode *P, int var);
 extern void Cudd_zddSymmProfile(DdManager *table, int lower, int upper);
 extern int Cudd_zddPrintMinterm(DdManager *zdd, DdNode *node);
 extern int Cudd_zddPrintCover(DdManager *zdd, DdNode *node);
 extern int Cudd_zddPrintDebug(DdManager *zdd, DdNode *f, int n, int pr);
 extern DdGen * Cudd_zddFirstPath(DdManager *zdd, DdNode *f, int **path);
 extern int Cudd_zddNextPath(DdGen *gen, int **path);
 extern char * Cudd_zddCoverPathToString(DdManager *zdd, int *path, char *str);
 extern DdNode * Cudd_zddSupport(DdManager * dd, DdNode * f);
 extern int Cudd_zddDumpDot(DdManager *dd, int n, DdNode **f, char const * const *inames, char const * const *onames, FILE *fp);
 extern int Cudd_bddSetPiVar(DdManager *dd, int index);
 extern int Cudd_bddSetPsVar(DdManager *dd, int index);
 extern int Cudd_bddSetNsVar(DdManager *dd, int index);
 extern int Cudd_bddIsPiVar(DdManager *dd, int index);
 extern int Cudd_bddIsPsVar(DdManager *dd, int index);
 extern int Cudd_bddIsNsVar(DdManager *dd, int index);
 extern int Cudd_bddSetPairIndex(DdManager *dd, int index, int pairIndex);
 extern int Cudd_bddReadPairIndex(DdManager *dd, int index);
 extern int Cudd_bddSetVarToBeGrouped(DdManager *dd, int index);
 extern int Cudd_bddSetVarHardGroup(DdManager *dd, int index);
 extern int Cudd_bddResetVarToBeGrouped(DdManager *dd, int index);
 extern int Cudd_bddIsVarToBeGrouped(DdManager *dd, int index);
 extern int Cudd_bddSetVarToBeUngrouped(DdManager *dd, int index);
 extern int Cudd_bddIsVarToBeUngrouped(DdManager *dd, int index);
 extern int Cudd_bddIsVarHardGroup(DdManager *dd, int index);
 #ifdef MTR_H_
 extern MtrNode * Cudd_ReadTree(DdManager *dd);
 extern void Cudd_SetTree(DdManager *dd, MtrNode *tree);
 extern void Cudd_FreeTree(DdManager *dd);
 extern MtrNode * Cudd_ReadZddTree(DdManager *dd);
 extern void Cudd_SetZddTree(DdManager *dd, MtrNode *tree);
 extern void Cudd_FreeZddTree(DdManager *dd);
 extern MtrNode * Cudd_MakeTreeNode(DdManager *dd, unsigned int low, unsigned int size, unsigned int type);
 extern MtrNode * Cudd_MakeZddTreeNode(DdManager *dd, unsigned int low, unsigned int size, unsigned int type);
 #endif

 #ifdef __cplusplus
 } /* end of extern "C" */
 #endif

 #endif /* CUDD_H_ */
Cudd_UnsetTimeLimit
void Cudd_UnsetTimeLimit(DdManager *unique)
Unsets the time limit for the manager.
Definition: cuddAPI.c:825

Cudd_ReadLinear
int Cudd_ReadLinear(DdManager *table, int x, int y)
Reads an entry of the linear transform matrix.
Definition: cuddLinear.c:145

Cudd_IterDerefBdd
void Cudd_IterDerefBdd(DdManager *table, DdNode *n)
Decreases the reference count of BDD node n.
Definition: cuddRef.c:181

Cudd_ApaShortDivision
DdApaDigit Cudd_ApaShortDivision(int digits, DdConstApaNumber dividend, DdApaDigit divisor, DdApaNumber quotient)
Divides an arbitrary precision integer by a digit.
Definition: cuddApa.c:269

Cudd_OutOfMemSilent
void Cudd_OutOfMemSilent(size_t size)
Doesn not warn that a memory allocation failed.
Definition: cuddUtil.c:2919

Cudd_bddApproxDisjDecomp
int Cudd_bddApproxDisjDecomp(DdManager *dd, DdNode *f, DdNode ***disjuncts)
Performs two-way disjunctive decomposition of a BDD.
Definition: cuddDecomp.c:250

Cudd_bddSetVarHardGroup
int Cudd_bddSetVarHardGroup(DdManager *dd, int index)
Sets a variable to be a hard group.
Definition: cuddAPI.c:4539

Cudd_SubsetHeavyBranch
DdNode * Cudd_SubsetHeavyBranch(DdManager *dd, DdNode *f, int numVars, int threshold)
Extracts a dense subset from a BDD with the heavy branch heuristic.
Definition: cuddSubsetHB.c:180

Cudd_SetOrderRandomization
void Cudd_SetOrderRandomization(DdManager *dd, unsigned int factor)
Sets the order randomization factor.
Definition: cuddAPI.c:3115

Cudd_addBddThreshold
DdNode * Cudd_addBddThreshold(DdManager *dd, DdNode *f, CUDD_VALUE_TYPE value)
Converts an ADD to a BDD.
Definition: cuddBridge.c:110

Cudd_tlcInfoFree
void Cudd_tlcInfoFree(DdTlcInfo *t)
Frees a DdTlcInfo Structure.
Definition: cuddEssent.c:420

Cudd_ReadMaxIndex
unsigned int Cudd_ReadMaxIndex(void)
Returns the maximum possible index for a variable.
Definition: cuddAPI.c:511

DD_MAOP
DdNode *(* DD_MAOP)(DdManager *, DdNode *)
Type of monadic apply operator.
Definition: cudd.h:246

Cudd_ReadTimeLimit
unsigned long Cudd_ReadTimeLimit(DdManager *unique)
Returns the time limit for the manager.
Definition: cuddAPI.c:727

Cudd_addOrAbstract
DdNode * Cudd_addOrAbstract(DdManager *manager, DdNode *f, DdNode *cube)
Disjunctively abstracts all the variables in cube from the 0-1 ADD f.
Definition: cuddAddAbs.c:184

Cudd_bddSetVarToBeUngrouped
int Cudd_bddSetVarToBeUngrouped(DdManager *dd, int index)
Sets a variable to be ungrouped.
Definition: cuddAPI.c:4612

Cudd_bddNPAnd
DdNode * Cudd_bddNPAnd(DdManager *dd, DdNode *f, DdNode *c)
Computes f non-polluting-and g.
Definition: cuddGenCof.c:257

Cudd_NewApaNumber
DdApaNumber Cudd_NewApaNumber(int digits)
Allocates memory for an arbitrary precision integer.
Definition: cuddApa.c:160

Cudd_AverageDistance
double Cudd_AverageDistance(DdManager *dd)
Computes the average distance between adjacent nodes in the manager.
Definition: cuddUtil.c:2673

Cudd_addMonadicApply
DdNode * Cudd_addMonadicApply(DdManager *dd, DD_MAOP op, DdNode *f)
Applies op to the discriminants of f.
Definition: cuddAddApply.c:690

Cudd_ReadZddTree
MtrNode * Cudd_ReadZddTree(DdManager *dd)
Returns the variable group tree of the manager.
Definition: cuddAPI.c:2441

Cudd_SubsetWithMaskVars
DdNode * Cudd_SubsetWithMaskVars(DdManager *dd, DdNode *f, DdNode **vars, int nvars, DdNode **maskVars, int mvars)
Extracts a subset from a BDD.
Definition: cuddUtil.c:1685

Cudd_RecursiveDerefZdd
void Cudd_RecursiveDerefZdd(DdManager *table, DdNode *n)
Decreases the reference count of ZDD node n.
Definition: cuddRef.c:347

Cudd_SetNumberXovers
void Cudd_SetNumberXovers(DdManager *dd, int numberXovers)
Sets the number of crossovers used by the genetic algorithm for variable reordering.
Definition: cuddAPI.c:3076

Cudd_bddNewVar
DdNode * Cudd_bddNewVar(DdManager *dd)
Returns a new BDD variable.
Definition: cuddAPI.c:180

Cudd_ReadMaxCache
unsigned int Cudd_ReadMaxCache(DdManager *dd)
Returns the soft limit for the cache size.
Definition: cuddAPI.c:1631

Cudd_zddReadNodeCount
long Cudd_zddReadNodeCount(DdManager *dd)
Reports the number of nodes in ZDDs.
Definition: cuddAPI.c:3424

Cudd_Init
DdManager * Cudd_Init(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, size_t maxMemory)
Creates a new DD manager.
Definition: cuddInit.c:102

Cudd_FindEssential
DdNode * Cudd_FindEssential(DdManager *dd, DdNode *f)
Finds the essential variables of a DD.
Definition: cuddEssent.c:174

Cudd_FreeApaNumber
void Cudd_FreeApaNumber(DdApaNumber number)
Frees an arbitrary precision integer.
Definition: cuddApa.c:176

Cudd_bddSetPiVar
int Cudd_bddSetPiVar(DdManager *dd, int index)
Sets a variable type to primary input.
Definition: cuddAPI.c:4322

Cudd_bddUnivAbstract
DdNode * Cudd_bddUnivAbstract(DdManager *manager, DdNode *f, DdNode *cube)
Universally abstracts all the variables in cube from f.
Definition: cuddBddAbs.c:226

Cudd_CProjection
DdNode * Cudd_CProjection(DdManager *dd, DdNode *R, DdNode *Y)
Computes the compatible projection of R w.r.t. cube Y.
Definition: cuddPriority.c:1151

Cudd_Xeqy
DdNode * Cudd_Xeqy(DdManager *dd, int N, DdNode **x, DdNode **y)
Generates a BDD for the function x==y.
Definition: cuddPriority.c:303

Cudd_ReadIthClause
int Cudd_ReadIthClause(DdTlcInfo *tlc, int i, unsigned *var1, unsigned *var2, int *phase1, int *phase2)
Accesses the i-th clause of a DD.
Definition: cuddEssent.c:328

Cudd_bddVarConjDecomp
int Cudd_bddVarConjDecomp(DdManager *dd, DdNode *f, DdNode ***conjuncts)
Performs two-way conjunctive decomposition of a BDD.
Definition: cuddDecomp.c:590

Cudd_CheckCube
int Cudd_CheckCube(DdManager *dd, DdNode *g)
Checks whether g is the BDD of a cube.
Definition: cuddCof.c:140

Cudd_ReadTimeoutHandler
DD_TOHFP Cudd_ReadTimeoutHandler(DdManager *unique, void **argp)
Read the current timeout handler function.
Definition: cuddAPI.c:964

Cudd_VerifySol
DdNode * Cudd_VerifySol(DdManager *bdd, DdNode *F, DdNode **G, int *yIndex, int n)
Checks the solution of F(x,y) = 0.
Definition: cuddSolve.c:148

Cudd_ApaPrintDecimal
int Cudd_ApaPrintDecimal(FILE *fp, int digits, DdConstApaNumber number)
Prints an arbitrary precision integer in decimal format.
Definition: cuddApa.c:526

Cudd_CofMinterm
double * Cudd_CofMinterm(DdManager *dd, DdNode *node)
Computes the fraction of minterms in the on-set of all the positive cofactors of a BDD or ADD...
Definition: cuddSign.c:101

Cudd_ReorderingStatusZdd
int Cudd_ReorderingStatusZdd(DdManager *unique, Cudd_ReorderingType *method)
Reports the status of automatic dynamic reordering of ZDDs.
Definition: cuddAPI.c:1123

Cudd_addConstrain
DdNode * Cudd_addConstrain(DdManager *dd, DdNode *f, DdNode *c)
Computes f constrain c for ADDs.
Definition: cuddGenCof.c:297

Cudd_ReadCacheSlots
unsigned int Cudd_ReadCacheSlots(DdManager *dd)
Reads the number of slots in the cache.
Definition: cuddAPI.c:1433

Cudd_addScalarInverse
DdNode * Cudd_addScalarInverse(DdManager *dd, DdNode *f, DdNode *epsilon)
Computes the scalar inverse of an ADD.
Definition: cuddAddInv.c:102

Cudd_AggregationType
Cudd_AggregationType
Type of aggregation methods.
Definition: cudd.h:123

Cudd_addSwapVariables
DdNode * Cudd_addSwapVariables(DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n)
Swaps two sets of variables of the same size (x and y) in the ADD f.
Definition: cuddCompose.c:241

Cudd_bddPickOneMinterm
DdNode * Cudd_bddPickOneMinterm(DdManager *dd, DdNode *f, DdNode **vars, int n)
Picks one on-set minterm randomly from the given DD.
Definition: cuddUtil.c:1379

Cudd_zddDiffConst
DdNode * Cudd_zddDiffConst(DdManager *zdd, DdNode *P, DdNode *Q)
Performs the inclusion test for ZDDs (P implies Q).
Definition: cuddZddSetop.c:217

Cudd_RegisterTerminationCallback
void Cudd_RegisterTerminationCallback(DdManager *unique, DD_THFP callback, void *callback_arg)
Installs a termination callback.
Definition: cuddAPI.c:863

Cudd_SetMaxCacheHard
void Cudd_SetMaxCacheHard(DdManager *dd, unsigned int mc)
Sets the maxCacheHard parameter of the manager.
Definition: cuddAPI.c:1671

Cudd_zddPortFromBdd
DdNode * Cudd_zddPortFromBdd(DdManager *dd, DdNode *B)
Converts a BDD into a ZDD.
Definition: cuddZddPort.c:107

Cudd_bddComputeCube
DdNode * Cudd_bddComputeCube(DdManager *dd, DdNode **vars, int *phase, int n)
Computes the cube of an array of BDD variables.
Definition: cuddUtil.c:2272

Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Decreases the reference count of node n.
Definition: cuddRef.c:120

Cudd_bddIsVarHardGroup
int Cudd_bddIsVarHardGroup(DdManager *dd, int index)
Checks whether a variable is set to be in a hard group.
Definition: cuddAPI.c:4663

Cudd_CountMinterm
double Cudd_CountMinterm(DdManager *manager, DdNode *node, int nvars)
Counts the minterms of an ADD or BDD.
Definition: cuddUtil.c:581

DdNode
Decision diagram node.
Definition: cuddInt.h:261

Cudd_bddMaximallyExpand
DdNode * Cudd_bddMaximallyExpand(DdManager *dd, DdNode *lb, DdNode *ub, DdNode *f)
Expands lb to prime implicants of (f and ub).
Definition: cuddSat.c:872

Cudd_addLog
DdNode * Cudd_addLog(DdManager *dd, DdNode *f)
Natural logarithm of an ADD.
Definition: cuddAddApply.c:723

Cudd_Dxygtdyz
DdNode * Cudd_Dxygtdyz(DdManager *dd, int N, DdNode **x, DdNode **y, DdNode **z)
Generates a BDD for the function d(x,y) > d(y,z).
Definition: cuddPriority.c:575

Cudd_IsNonConstant
int Cudd_IsNonConstant(DdNode *f)
Returns 1 if a DD node is not constant.
Definition: cuddAPI.c:572

Cudd_ReadSymmviolation
int Cudd_ReadSymmviolation(DdManager *dd)
Returns the current value of the symmviolation parameter used in group sifting.
Definition: cuddAPI.c:2906

Cudd_EpdCountMinterm
int Cudd_EpdCountMinterm(DdManager const *manager, DdNode *node, int nvars, EpDouble *epd)
Counts the minterms of an ADD or BDD with extended range.
Definition: cuddUtil.c:673

Cudd_bddIterDisjDecomp
int Cudd_bddIterDisjDecomp(DdManager *dd, DdNode *f, DdNode ***disjuncts)
Performs two-way disjunctive decomposition of a BDD.
Definition: cuddDecomp.c:432

Cudd_zddComplement
DdNode * Cudd_zddComplement(DdManager *dd, DdNode *node)
Computes a complement cover for a ZDD node.
Definition: cuddZddFuncs.c:299

Cudd_ResetStartTime
void Cudd_ResetStartTime(DdManager *unique)
Resets the start time of the manager.
Definition: cuddAPI.c:706

Cudd_ReadMinDead
unsigned int Cudd_ReadMinDead(DdManager *dd)
Reads the minDead parameter of the manager.
Definition: cuddAPI.c:1908

DD_QSFP
int(* DD_QSFP)(const void *, const void *)
Type of comparison function for qsort.
Definition: cudd.h:262

Cudd_addCmpl
DdNode * Cudd_addCmpl(DdManager *dd, DdNode *f)
Computes the complement of an ADD a la C language.
Definition: cuddAddIte.c:324

Cudd_ShortestPath
DdNode * Cudd_ShortestPath(DdManager *manager, DdNode *f, int *weight, int *support, int *length)
Finds a shortest path in a DD.
Definition: cuddSat.c:164

Cudd_SupportIndices
int Cudd_SupportIndices(DdManager *dd, DdNode *f, int **indices)
Finds the variables on which a DD depends.
Definition: cuddUtil.c:833

Cudd_bddConstrainDecomp
DdNode ** Cudd_bddConstrainDecomp(DdManager *dd, DdNode *f)
BDD conjunctive decomposition as in McMillan&#39;s CAV96 paper.
Definition: cuddGenCof.c:334

Cudd_addOr
DdNode * Cudd_addOr(DdManager *dd, DdNode **f, DdNode **g)
Disjunction of two 0-1 ADDs.
Definition: cuddAddApply.c:534

Cudd_SetTree
void Cudd_SetTree(DdManager *dd, MtrNode *tree)
Sets the variable group tree of the manager.
Definition: cuddAPI.c:2395

Cudd_bddPickOneCube
int Cudd_bddPickOneCube(DdManager *ddm, DdNode *node, char *string)
Picks one on-set cube randomly from the given DD.
Definition: cuddUtil.c:1308

Cudd_zddSubset1
DdNode * Cudd_zddSubset1(DdManager *dd, DdNode *P, int var)
Computes the positive cofactor of a ZDD w.r.t. a variable.
Definition: cuddZddSetop.c:280

Cudd_MakeTreeNode
MtrNode * Cudd_MakeTreeNode(DdManager *dd, unsigned int low, unsigned int size, unsigned int type)
Creates a new variable group.
Definition: cuddGroup.c:136

Cudd_FirstNode
DdGen * Cudd_FirstNode(DdManager *dd, DdNode *f, DdNode **node)
Finds the first node of a decision diagram.
Definition: cuddUtil.c:2476

Cudd_ReadMaxCacheHard
unsigned int Cudd_ReadMaxCacheHard(DdManager *dd)
Reads the maxCacheHard parameter of the manager.
Definition: cuddAPI.c:1648

Cudd_ApaPrintDensity
int Cudd_ApaPrintDensity(FILE *fp, DdManager *dd, DdNode *node, int nvars)
Prints the density of a BDD or ADD using arbitrary precision arithmetic.
Definition: cuddApa.c:906

Cudd_Support
DdNode * Cudd_Support(DdManager *dd, DdNode *f)
Finds the variables on which a DD depends.
Definition: cuddUtil.c:876

Cudd_RegisterTimeoutHandler
void Cudd_RegisterTimeoutHandler(DdManager *unique, DD_TOHFP handler, void *arg)
Register a timeout handler function.
Definition: cuddAPI.c:944

Cudd_Deref
void Cudd_Deref(DdNode *node)
Decreases the reference count of node.
Definition: cuddRef.c:399

Cudd_addNewVarAtLevel
DdNode * Cudd_addNewVarAtLevel(DdManager *dd, int level)
Returns a new ADD variable at a specified level.
Definition: cuddAPI.c:141

Cudd_EquivDC
int Cudd_EquivDC(DdManager *dd, DdNode *F, DdNode *G, DdNode *D)
Tells whether F and G are identical wherever D is 0.
Definition: cuddSat.c:496

Cudd_Xgty
DdNode * Cudd_Xgty(DdManager *dd, int N, DdNode **z, DdNode **x, DdNode **y)
Generates a BDD for the function x > y.
Definition: cuddPriority.c:239

Cudd_addComputeCube
DdNode * Cudd_addComputeCube(DdManager *dd, DdNode **vars, int *phase, int n)
Computes the cube of an array of ADD variables.
Definition: cuddUtil.c:2322

Cudd_NextPrime
int Cudd_NextPrime(DdGen *gen, int **cube)
Generates the next prime of a Boolean function.
Definition: cuddUtil.c:2206

Cudd_addConst
DdNode * Cudd_addConst(DdManager *dd, CUDD_VALUE_TYPE c)
Returns the ADD for constant c.
Definition: cuddAPI.c:532

Cudd_SetStdout
void Cudd_SetStdout(DdManager *dd, FILE *fp)
Sets the stdout of a manager.
Definition: cuddAPI.c:4035

Cudd_bddAdjPermuteX
DdNode * Cudd_bddAdjPermuteX(DdManager *dd, DdNode *B, DdNode **x, int n)
Rearranges a set of variables in the BDD B.
Definition: cuddCompose.c:475

Cudd_bddIteLimit
DdNode * Cudd_bddIteLimit(DdManager *dd, DdNode *f, DdNode *g, DdNode *h, unsigned int limit)
Implements ITE(f,g,h) unless too many nodes are required.
Definition: cuddBddIte.c:137

Cudd_bddVarIsBound
int Cudd_bddVarIsBound(DdManager *dd, int index)
Tells whether a variable can be sifted.
Definition: cuddAPI.c:4299

Cudd_Reserve
int Cudd_Reserve(DdManager *manager, int amount)
Expand manager without creating variables.
Definition: cuddTable.c:189

Cudd_addBddPattern
DdNode * Cudd_addBddPattern(DdManager *dd, DdNode *f)
Converts an ADD to a BDD.
Definition: cuddBridge.c:348

Cudd_ApaIntDivision
unsigned int Cudd_ApaIntDivision(int digits, DdConstApaNumber dividend, unsigned int divisor, DdApaNumber quotient)
Divides an arbitrary precision integer by an integer.
Definition: cuddApa.c:313

Cudd_PrintTwoLiteralClauses
int Cudd_PrintTwoLiteralClauses(DdManager *dd, DdNode *f, char **names, FILE *fp)
Prints the one- and two-literal clauses of a DD.
Definition: cuddEssent.c:362

Cudd_zddCountMinterm
double Cudd_zddCountMinterm(DdManager *zdd, DdNode *node, int path)
Counts the number of minterms of a ZDD.
Definition: cuddZddMisc.c:134

Cudd_ReadNextReordering
unsigned int Cudd_ReadNextReordering(DdManager *dd)
Returns the threshold for the next dynamic reordering.
Definition: cuddAPI.c:4097

MtrNode_
multi-way tree node.
Definition: mtrInt.h:109

Cudd_TurnOffCountDead
void Cudd_TurnOffCountDead(DdManager *dd)
Causes the dead nodes not to be counted towards triggering reordering.
Definition: cuddAPI.c:2835

Cudd_bddResetVarToBeGrouped
int Cudd_bddResetVarToBeGrouped(DdManager *dd, int index)
Resets a variable not to be grouped.
Definition: cuddAPI.c:4563

Cudd_RemapOverApprox
DdNode * Cudd_RemapOverApprox(DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
Extracts a dense superset from a BDD with the remapping underapproximation method.
Definition: cuddApprox.c:342

Cudd_NextNode
int Cudd_NextNode(DdGen *gen, DdNode **node)
Finds the next node of a decision diagram.
Definition: cuddUtil.c:2533

Cudd_LdblCountMinterm
long double Cudd_LdblCountMinterm(DdManager const *manager, DdNode *node, int nvars)
Returns the number of minterms of aa ADD or BDD as a long double.
Definition: cuddUtil.c:721

Cudd_ErrorType
Cudd_ErrorType
Type of error codes.
Definition: cudd.h:151

Cudd_ReadLogicZero
DdNode * Cudd_ReadLogicZero(DdManager *dd)
Returns the logic zero constant of the manager.
Definition: cuddAPI.c:1352

Cudd_zddDagSize
int Cudd_zddDagSize(DdNode *p_node)
Counts the number of nodes in a ZDD.
Definition: cuddZddMisc.c:102

Cudd_addEvalConst
DdNode * Cudd_addEvalConst(DdManager *dd, DdNode *f, DdNode *g)
Checks whether ADD g is constant whenever ADD f is 1.
Definition: cuddAddIte.c:237

Cudd_bddPickArbitraryMinterms
DdNode ** Cudd_bddPickArbitraryMinterms(DdManager *dd, DdNode *f, DdNode **vars, int n, int k)
Picks k on-set minterms evenly distributed from given DD.
Definition: cuddUtil.c:1479

Cudd_bddExistAbstract
DdNode * Cudd_bddExistAbstract(DdManager *manager, DdNode *f, DdNode *cube)
Existentially abstracts all the variables in cube from f.
Definition: cuddBddAbs.c:101

Cudd_AutodynDisableZdd
void Cudd_AutodynDisableZdd(DdManager *unique)
Disables automatic dynamic reordering of ZDDs.
Definition: cuddAPI.c:1098

Cudd_bddNor
DdNode * Cudd_bddNor(DdManager *dd, DdNode *f, DdNode *g)
Computes the NOR of two BDDs f and g.
Definition: cuddBddIte.c:487

Cudd_addNor
DdNode * Cudd_addNor(DdManager *dd, DdNode **f, DdNode **g)
NOR of two 0-1 ADDs.
Definition: cuddAddApply.c:596

Cudd_ReadMinHit
unsigned int Cudd_ReadMinHit(DdManager *dd)
Reads the hit rate that causes resizinig of the computed table.
Definition: cuddAPI.c:1540

Cudd_zddWeakDivF
DdNode * Cudd_zddWeakDivF(DdManager *dd, DdNode *f, DdNode *g)
Modified version of Cudd_zddWeakDiv.
Definition: cuddZddFuncs.c:237

Cudd_SetRecomb
void Cudd_SetRecomb(DdManager *dd, int recomb)
Sets the value of the recombination parameter used in group sifting.
Definition: cuddAPI.c:2880

Cudd_SetZddTree
void Cudd_SetZddTree(DdManager *dd, MtrNode *tree)
Sets the ZDD variable group tree of the manager.
Definition: cuddAPI.c:2458

Cudd_ReadPlusInfinity
DdNode * Cudd_ReadPlusInfinity(DdManager *dd)
Reads the plus-infinity constant from the manager.
Definition: cuddAPI.c:1367

Cudd_ReadMaxReorderings
unsigned int Cudd_ReadMaxReorderings(DdManager *dd)
Returns the maximum number of times reordering may be invoked.
Definition: cuddAPI.c:1949

Cudd_Decreasing
DdNode * Cudd_Decreasing(DdManager *dd, DdNode *f, int i)
Checks whether a BDD is negative unate in a variable.
Definition: cuddSat.c:392

Cudd_SetStartTime
void Cudd_SetStartTime(DdManager *unique, unsigned long st)
Sets the start time of the manager.
Definition: cuddAPI.c:688

Cudd_BiasedOverApprox
DdNode * Cudd_BiasedOverApprox(DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
Extracts a dense superset from a BDD with the biased underapproximation method.
Definition: cuddApprox.c:443

Cudd_SetVarMap
int Cudd_SetVarMap(DdManager *manager, DdNode **x, DdNode **y, int n)
Registers a variable mapping with the manager.
Definition: cuddCompose.c:380

Cudd_addFindMin
DdNode * Cudd_addFindMin(DdManager *dd, DdNode *f)
Finds the minimum discriminant of f.
Definition: cuddAddFind.c:138

Cudd_ApaAdd
DdApaDigit Cudd_ApaAdd(int digits, DdConstApaNumber a, DdConstApaNumber b, DdApaNumber sum)
Adds two arbitrary precision integers.
Definition: cuddApa.c:214

Cudd_OverApprox
DdNode * Cudd_OverApprox(DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)
Extracts a dense superset from a BDD with Shiple&#39;s underapproximation method.
Definition: cuddApprox.c:247

Cudd_SetBackground
void Cudd_SetBackground(DdManager *dd, DdNode *bck)
Sets the background constant of the manager.
Definition: cuddAPI.c:1415

Cudd_SetMaxGrowthAlternate
void Cudd_SetMaxGrowthAlternate(DdManager *dd, double mg)
Sets the maxGrowthAlt parameter of the manager.
Definition: cuddAPI.c:2317

Cudd_ShortestLength
int Cudd_ShortestLength(DdManager *manager, DdNode *f, int *weight)
Find the length of the shortest path(s) in a DD.
Definition: cuddSat.c:331

Cudd_CubeArrayToBdd
DdNode * Cudd_CubeArrayToBdd(DdManager *dd, int *array)
Builds the BDD of a cube from a positional array.
Definition: cuddUtil.c:2375

Cudd_bddSetVarToBeGrouped
int Cudd_bddSetVarToBeGrouped(DdManager *dd, int index)
Sets a variable to be grouped.
Definition: cuddAPI.c:4512

Cudd_ReadMaxMemory
size_t Cudd_ReadMaxMemory(DdManager *dd)
Reads the maximum allowed memory.
Definition: cuddAPI.c:4198

Cudd_FreeZddTree
void Cudd_FreeZddTree(DdManager *dd)
Frees the variable group tree of the manager.
Definition: cuddAPI.c:2483

Cudd_zddPortToBdd
DdNode * Cudd_zddPortToBdd(DdManager *dd, DdNode *f)
Converts a ZDD into a BDD.
Definition: cuddZddPort.c:138

Cudd_zddRealignmentEnabled
int Cudd_zddRealignmentEnabled(DdManager *unique)
Tells whether the realignment of ZDD order to BDD order is enabled.
Definition: cuddAPI.c:1147

Cudd_bddIsNsVar
int Cudd_bddIsNsVar(DdManager *dd, int index)
Checks whether a variable is next state.
Definition: cuddAPI.c:4440

Cudd_bddLargestPrimeUnate
DdNode * Cudd_bddLargestPrimeUnate(DdManager *dd, DdNode *f, DdNode *phaseBdd)
Find a largest prime implicant of a unate function.
Definition: cuddSat.c:910

Cudd_PrintSummary
int Cudd_PrintSummary(DdManager *dd, DdNode *f, int n, int mode)
Prints a one-line summary of an ADD or BDD to the manager stdout.
Definition: cuddUtil.c:375

Cudd_ReadNodesDropped
double Cudd_ReadNodesDropped(DdManager *dd)
Returns the number of nodes dropped.
Definition: cuddAPI.c:2076

DdManager
Specialized DD symbol table.
Definition: cuddInt.h:399

Cudd_ReadGroupcheck
Cudd_AggregationType Cudd_ReadGroupcheck(DdManager *dd)
Reads the groupcheck parameter of the manager.
Definition: cuddAPI.c:2688

Cudd_bddAndAbstractLimit
DdNode * Cudd_bddAndAbstractLimit(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, unsigned int limit)
Takes the AND of two BDDs and simultaneously abstracts variables unless too many nodes are needed...
Definition: cuddAndAbs.c:140

Cudd_TimeLimited
int Cudd_TimeLimited(DdManager *unique)
Returns true if the time limit for the manager is set.
Definition: cuddAPI.c:843

Cudd_addIteConstant
DdNode * Cudd_addIteConstant(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Implements ITEconstant for ADDs.
Definition: cuddAddIte.c:140

Cudd_ApaPrintHex
int Cudd_ApaPrintHex(FILE *fp, int digits, DdConstApaNumber number)
Prints an arbitrary precision integer in hexadecimal format.
Definition: cuddApa.c:498

Cudd_SupersetShortPaths
DdNode * Cudd_SupersetShortPaths(DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit)
Extracts a dense superset from a BDD with the shortest paths heuristic.
Definition: cuddSubsetSP.c:238

Cudd_ReorderingReporting
int Cudd_ReorderingReporting(DdManager *dd)
Returns 1 if reporting of reordering stats is enabled; 0 otherwise.
Definition: cuddAPI.c:3786

Cudd_zddDiff
DdNode * Cudd_zddDiff(DdManager *dd, DdNode *P, DdNode *Q)
Computes the difference of two ZDDs.
Definition: cuddZddSetop.c:184

Cudd_addHarwell
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)
Reads in a matrix in the format of the Harwell-Boeing benchmark suite.
Definition: cuddHarwell.c:109

Cudd_bddAndLimit
DdNode * Cudd_bddAndLimit(DdManager *dd, DdNode *f, DdNode *g, unsigned int limit)
Computes the conjunction of two BDDs f and g unless too many nodes are required.
Definition: cuddBddIte.c:347

Cudd_bddSwapVariables
DdNode * Cudd_bddSwapVariables(DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n)
Swaps two sets of variables of the same size (x and y) in the BDD f.
Definition: cuddCompose.c:428

Cudd_addMaximum
DdNode * Cudd_addMaximum(DdManager *dd, DdNode **f, DdNode **g)
Integer and floating point max.
Definition: cuddAddApply.c:388

DdGen
CUDD generator.
Definition: cuddInt.h:274

Cudd_ReadZero
DdNode * Cudd_ReadZero(DdManager *dd)
Returns the zero constant of the manager.
Definition: cuddAPI.c:1332

Cudd_Random
int32_t Cudd_Random(DdManager *dd)
Portable random number generator.
Definition: cuddUtil.c:2761

Cudd_IsGenEmpty
int Cudd_IsGenEmpty(DdGen *gen)
Queries the status of a generator.
Definition: cuddUtil.c:2601

Cudd_bddLICompaction
DdNode * Cudd_bddLICompaction(DdManager *dd, DdNode *f, DdNode *c)
Performs safe minimization of a BDD.
Definition: cuddGenCof.c:541

Cudd_bddClosestCube
DdNode * Cudd_bddClosestCube(DdManager *dd, DdNode *f, DdNode *g, int *distance)
Finds a cube of f at minimum Hamming distance from the minterms of g.
Definition: cuddPriority.c:1311

Cudd_OutOfMem
void Cudd_OutOfMem(size_t size)
Warns that a memory allocation failed.
Definition: cuddUtil.c:2894

Cudd_bddGenConjDecomp
int Cudd_bddGenConjDecomp(DdManager *dd, DdNode *f, DdNode ***conjuncts)
Performs two-way conjunctive decomposition of a BDD.
Definition: cuddDecomp.c:471

Cudd_bddIte
DdNode * Cudd_bddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Implements ITE(f,g,h).
Definition: cuddBddIte.c:104

Cudd_addResidue
DdNode * Cudd_addResidue(DdManager *dd, int n, int m, int options, int top)
Builds an ADD for the residue modulo m of an n-bit number.
Definition: cuddAddWalsh.c:141

Cudd_bddOrLimit
DdNode * Cudd_bddOrLimit(DdManager *dd, DdNode *f, DdNode *g, unsigned int limit)
Computes the disjunction of two BDDs f and g unless too many nodes are required.
Definition: cuddBddIte.c:417

Cudd_addXor
DdNode * Cudd_addXor(DdManager *dd, DdNode **f, DdNode **g)
XOR of two 0-1 ADDs.
Definition: cuddAddApply.c:626

Cudd_ReadMemoryInUse
size_t Cudd_ReadMemoryInUse(DdManager *dd)
Returns the memory in use by the manager measured in bytes.
Definition: cuddAPI.c:3131

Cudd_PrioritySelect
DdNode * Cudd_PrioritySelect(DdManager *dd, DdNode *R, DdNode **x, DdNode **y, DdNode **z, DdNode *Pi, int n, DD_PRFP PiFunc)
Selects pairs from R using a priority function.
Definition: cuddPriority.c:135

Cudd_zddDivide
DdNode * Cudd_zddDivide(DdManager *dd, DdNode *f, DdNode *g)
Computes the quotient of two unate covers.
Definition: cuddZddFuncs.c:207

Cudd_CountLeaves
int Cudd_CountLeaves(DdNode *node)
Counts the number of leaves in a DD.
Definition: cuddUtil.c:1282

Cudd_SolveEqn
DdNode * Cudd_SolveEqn(DdManager *bdd, DdNode *F, DdNode *Y, DdNode **G, int **yIndex, int n)
Implements the solution of F(x,y) = 0.
Definition: cuddSolve.c:104

Cudd_SetApplicationHook
void Cudd_SetApplicationHook(DdManager *dd, void *value)
Sets the application hook.
Definition: cuddAPI.c:3924

Cudd_MakeBddFromZddCover
DdNode * Cudd_MakeBddFromZddCover(DdManager *dd, DdNode *node)
Converts a ZDD cover to a BDD.
Definition: cuddZddIsop.c:182

Cudd_zddChange
DdNode * Cudd_zddChange(DdManager *dd, DdNode *P, int var)
Substitutes a variable with its complement in a ZDD.
Definition: cuddZddSetop.c:343

Cudd_BiasedUnderApprox
DdNode * Cudd_BiasedUnderApprox(DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
Extracts a dense subset from a BDD with the biased underapproximation method.
Definition: cuddApprox.c:391

Cudd_ReadPeakLiveNodeCount
int Cudd_ReadPeakLiveNodeCount(DdManager *dd)
Reports the peak number of live nodes.
Definition: cuddAPI.c:3358

Cudd_zddNextPath
int Cudd_zddNextPath(DdGen *gen, int **path)
Generates the next path of a ZDD.
Definition: cuddZddUtil.c:350

Cudd_DeadAreCounted
int Cudd_DeadAreCounted(DdManager *dd)
Tells whether dead nodes are counted towards triggering reordering.
Definition: cuddAPI.c:2792

Cudd_SetLooseUpTo
void Cudd_SetLooseUpTo(DdManager *dd, unsigned int lut)
Sets the looseUpTo parameter of the manager.
Definition: cuddAPI.c:1608

Cudd_zddIntersect
DdNode * Cudd_zddIntersect(DdManager *dd, DdNode *P, DdNode *Q)
Computes the intersection of two ZDDs.
Definition: cuddZddSetop.c:156

Cudd_SetSiftMaxVar
void Cudd_SetSiftMaxVar(DdManager *dd, int smv)
Sets the siftMaxVar parameter of the manager.
Definition: cuddAPI.c:2176

Cudd_ReadVars
DdNode * Cudd_ReadVars(DdManager *dd, int i)
Returns the i-th element of the vars array.
Definition: cuddAPI.c:2625

Cudd_ReadGarbageCollectionTime
long Cudd_ReadGarbageCollectionTime(DdManager *dd)
Returns the time spent in garbage collection.
Definition: cuddAPI.c:2029

Cudd_SubsetCompress
DdNode * Cudd_SubsetCompress(DdManager *dd, DdNode *f, int nvars, int threshold)
Find a dense subset of BDD f.
Definition: cuddGenCof.c:711

Cudd_bddRead
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)
Reads in a graph (without labels) given as a list of arcs.
Definition: cuddRead.c:375

Cudd_ReadSize
int Cudd_ReadSize(DdManager *dd)
Returns the number of BDD variables in existance.
Definition: cuddAPI.c:1694

Cudd_addDivide
DdNode * Cudd_addDivide(DdManager *dd, DdNode **f, DdNode **g)
Integer and floating point division.
Definition: cuddAddApply.c:272

Cudd_bddInterval
DdNode * Cudd_bddInterval(DdManager *dd, int N, DdNode **x, unsigned int lowerB, unsigned int upperB)
Generates a BDD for the function lowerB ≤ x ≤ upperB.
Definition: cuddPriority.c:1072

Cudd_addAgreement
DdNode * Cudd_addAgreement(DdManager *dd, DdNode **f, DdNode **g)
f if f==g; background if f!=g.
Definition: cuddAddApply.c:506

Cudd_NextCube
int Cudd_NextCube(DdGen *gen, int **cube, CUDD_VALUE_TYPE *value)
Generates the next cube of a decision diagram onset.
Definition: cuddUtil.c:1996

Cudd_VariableType
Cudd_VariableType
Variable type.
Definition: cudd.h:180

Cudd_ReadInvPerm
int Cudd_ReadInvPerm(DdManager *dd, int i)
Returns the index of the variable currently in the i-th position of the order.
Definition: cuddAPI.c:2575

Cudd_bddIsVarEssential
int Cudd_bddIsVarEssential(DdManager *manager, DdNode *f, int id, int phase)
Determines whether a given variable is essential with a given phase in a BDD.
Definition: cuddEssent.c:205

Cudd_V
CUDD_VALUE_TYPE Cudd_V(DdNode *node)
Returns the value of a constant node.
Definition: cuddAPI.c:630

Cudd_zddIte
DdNode * Cudd_zddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Computes the ITE of three ZDDs.
Definition: cuddZddSetop.c:99

Cudd_zddFirstPath
DdGen * Cudd_zddFirstPath(DdManager *zdd, DdNode *f, int **path)
Finds the first path of a ZDD.
Definition: cuddZddUtil.c:238

Cudd_bddTransfer
DdNode * Cudd_bddTransfer(DdManager *ddSource, DdManager *ddDestination, DdNode *f)
Convert a BDD from a manager to another one.
Definition: cuddBridge.c:379

Cudd_T
DdNode * Cudd_T(DdNode *node)
Returns the then child of an internal node.
Definition: cuddAPI.c:592

Cudd_zddProduct
DdNode * Cudd_zddProduct(DdManager *dd, DdNode *f, DdNode *g)
Computes the product of two covers represented by ZDDs.
Definition: cuddZddFuncs.c:103

Cudd_DumpDDcal
int Cudd_DumpDDcal(DdManager *dd, int n, DdNode **f, char const *const *inames, char const *const *onames, FILE *fp)
Writes a DDcal file representing the argument BDDs.
Definition: cuddExport.c:707

Cudd_bddVectorCompose
DdNode * Cudd_bddVectorCompose(DdManager *dd, DdNode *f, DdNode **vector)
Composes a BDD with a vector of BDDs.
Definition: cuddCompose.c:764

Cudd_ReadReorderingTime
long Cudd_ReadReorderingTime(DdManager *dd)
Returns the time spent in reordering.
Definition: cuddAPI.c:1989

Cudd_addNonSimCompose
DdNode * Cudd_addNonSimCompose(DdManager *dd, DdNode *f, DdNode **vector)
Composes an ADD with a vector of 0-1 ADDs.
Definition: cuddCompose.c:652

Cudd_LargestCube
DdNode * Cudd_LargestCube(DdManager *manager, DdNode *f, int *length)
Finds a largest cube in a DD.
Definition: cuddSat.c:252

Cudd_ReadElapsedTime
unsigned long Cudd_ReadElapsedTime(DdManager *unique)
Returns the time elapsed since the start time of the manager.
Definition: cuddAPI.c:668

DdConstApaNumber
DdApaDigit const  * DdConstApaNumber
Type of a const-qualified arbitrary precision integer.
Definition: cudd.h:224

Cudd_bddNand
DdNode * Cudd_bddNand(DdManager *dd, DdNode *f, DdNode *g)
Computes the NAND of two BDDs f and g.
Definition: cuddBddIte.c:454

Cudd_ReadBackground
DdNode * Cudd_ReadBackground(DdManager *dd)
Reads the background constant of the manager.
Definition: cuddAPI.c:1397

Cudd_addCompose
DdNode * Cudd_addCompose(DdManager *dd, DdNode *f, DdNode *g, int v)
Substitutes g for x_v in the ADD for f.
Definition: cuddCompose.c:155

Cudd_addLeq
int Cudd_addLeq(DdManager *dd, DdNode *f, DdNode *g)
Determines whether f is less than or equal to g.
Definition: cuddAddIte.c:356

Cudd_bddIteConstant
DdNode * Cudd_bddIteConstant(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Implements ITEconstant(f,g,h).
Definition: cuddBddIte.c:175

Cudd_ClearErrorCode
void Cudd_ClearErrorCode(DdManager *dd)
Clear the error code of a manager.
Definition: cuddAPI.c:3978

Cudd_addApply
DdNode * Cudd_addApply(DdManager *dd, DD_AOP op, DdNode *f, DdNode *g)
Applies op to the corresponding discriminants of f and g.
Definition: cuddAddApply.c:100

Cudd_bddMinimize
DdNode * Cudd_bddMinimize(DdManager *dd, DdNode *f, DdNode *c)
Finds a small BDD that agrees with f over c.
Definition: cuddGenCof.c:665

Cudd_ApaSubtract
DdApaDigit Cudd_ApaSubtract(int digits, DdConstApaNumber a, DdConstApaNumber b, DdApaNumber diff)
Subtracts two arbitrary precision integers.
Definition: cuddApa.c:242

Cudd_zddUnion
DdNode * Cudd_zddUnion(DdManager *dd, DdNode *P, DdNode *Q)
Computes the union of two ZDDs.
Definition: cuddZddSetop.c:128

Cudd_addBddIthBit
DdNode * Cudd_addBddIthBit(DdManager *dd, DdNode *f, int bit)
Converts an ADD to a BDD by extracting the i-th bit from the leaves.
Definition: cuddBridge.c:273

Cudd_addRoundOff
DdNode * Cudd_addRoundOff(DdManager *dd, DdNode *f, int N)
Rounds off the discriminants of an ADD.
Definition: cuddAddNeg.c:128

Cudd_UnregisterOutOfMemoryCallback
void Cudd_UnregisterOutOfMemoryCallback(DdManager *unique)
Unregister an out-of-memory callback.
Definition: cuddAPI.c:926

DD_TOHFP
void(* DD_TOHFP)(DdManager *, void *)
Type of timeout handler.
Definition: cudd.h:270

Cudd_ReadNodesFreed
double Cudd_ReadNodesFreed(DdManager *dd)
Returns the number of nodes freed.
Definition: cuddAPI.c:2050

Cudd_SetReorderingCycle
void Cudd_SetReorderingCycle(DdManager *dd, int cycle)
Sets the reordCycle parameter of the manager.
Definition: cuddAPI.c:2360

DD_OOMFP
void(* DD_OOMFP)(size_t)
Type of memory-out function.
Definition: cudd.h:258

Cudd_EpdPrintMinterm
int Cudd_EpdPrintMinterm(DdManager const *dd, DdNode *node, int nvars)
Prints the number of minterms of an ADD or BDD with extended range.
Definition: cuddUtil.c:769

Cudd_ReadNumberXovers
int Cudd_ReadNumberXovers(DdManager *dd)
Reads the current number of crossovers used by the genetic algorithm for variable reordering...
Definition: cuddAPI.c:3052

Cudd_UnregisterTerminationCallback
void Cudd_UnregisterTerminationCallback(DdManager *unique)
Unregisters a termination callback.
Definition: cuddAPI.c:883

Cudd_Eval
DdNode * Cudd_Eval(DdManager *dd, DdNode *f, int *inputs)
Returns the value of a DD for a given variable assignment.
Definition: cuddSat.c:119

Cudd_bddIsPiVar
int Cudd_bddIsPiVar(DdManager *dd, int index)
Checks whether a variable is primary input.
Definition: cuddAPI.c:4394

Cudd_bddVarMap
DdNode * Cudd_bddVarMap(DdManager *manager, DdNode *f)
Remaps the variables of a BDD using the default variable map.
Definition: cuddCompose.c:333

Cudd_addThreshold
DdNode * Cudd_addThreshold(DdManager *dd, DdNode **f, DdNode **g)
f if f≥g; 0 if f<g.
Definition: cuddAddApply.c:212

Cudd_bddLiteralSetIntersection
DdNode * Cudd_bddLiteralSetIntersection(DdManager *dd, DdNode *f, DdNode *g)
Computes the intesection of two sets of literals represented as BDDs.
Definition: cuddLiteral.c:100

Cudd_bddBindVar
int Cudd_bddBindVar(DdManager *dd, int index)
Prevents sifting of a variable.
Definition: cuddAPI.c:4244

Cudd_IndicesToCube
DdNode * Cudd_IndicesToCube(DdManager *dd, int *array, int n)
Builds a cube of BDD variables from an array of indices.
Definition: cuddUtil.c:2621

Cudd_EnableGarbageCollection
void Cudd_EnableGarbageCollection(DdManager *dd)
Enables garbage collection.
Definition: cuddAPI.c:2749

Cudd_addPermute
DdNode * Cudd_addPermute(DdManager *manager, DdNode *node, int *permut)
Permutes the variables of an ADD.
Definition: cuddCompose.c:197

Cudd_EstimateCofactorSimple
int Cudd_EstimateCofactorSimple(DdNode *node, int i)
Estimates the number of nodes in a cofactor of a DD.
Definition: cuddUtil.c:515

Cudd_FirstPrime
DdGen * Cudd_FirstPrime(DdManager *dd, DdNode *l, DdNode *u, int **cube)
Finds the first prime of a Boolean function.
Definition: cuddUtil.c:2107

Cudd_DumpFactoredForm
int Cudd_DumpFactoredForm(DdManager *dd, int n, DdNode **f, char const *const *inames, char const *const *onames, FILE *fp)
Writes factored forms representing the argument BDDs.
Definition: cuddExport.c:867

Cudd_InstallOutOfMemoryHandler
DD_OOMFP Cudd_InstallOutOfMemoryHandler(DD_OOMFP newHandler)
Installs a handler for failed memory allocations.
Definition: cuddAPI.c:3995

Cudd_SetEpsilon
void Cudd_SetEpsilon(DdManager *dd, CUDD_VALUE_TYPE ep)
Sets the epsilon parameter of the manager to ep.
Definition: cuddAPI.c:2667

Cudd_ApaShiftRight
void Cudd_ApaShiftRight(int digits, DdApaDigit in, DdConstApaNumber a, DdApaNumber b)
Shifts right an arbitrary precision integer by one binary place.
Definition: cuddApa.c:346

Cudd_addIthVar
DdNode * Cudd_addIthVar(DdManager *dd, int i)
Returns the ADD variable with index i.
Definition: cuddAPI.c:263

Cudd_bddMakePrime
DdNode * Cudd_bddMakePrime(DdManager *dd, DdNode *cube, DdNode *f)
Expands cube to a prime implicant of f.
Definition: cuddSat.c:833

Cudd_zddShuffleHeap
int Cudd_zddShuffleHeap(DdManager *table, int *permutation)
Reorders ZDD variables according to given permutation.
Definition: cuddZddReord.c:259

Cudd_SupersetHeavyBranch
DdNode * Cudd_SupersetHeavyBranch(DdManager *dd, DdNode *f, int numVars, int threshold)
Extracts a dense superset from a BDD with the heavy branch heuristic.
Definition: cuddSubsetHB.c:231

Cudd_HookType
Cudd_HookType
Type of hooks.
Definition: cudd.h:140

Cudd_addXnor
DdNode * Cudd_addXnor(DdManager *dd, DdNode **f, DdNode **g)
XNOR of two 0-1 ADDs.
Definition: cuddAddApply.c:658

Cudd_Cofactor
DdNode * Cudd_Cofactor(DdManager *dd, DdNode *f, DdNode *g)
Computes the cofactor of f with respect to g.
Definition: cuddCof.c:103

Cudd_bddExistAbstractLimit
DdNode * Cudd_bddExistAbstractLimit(DdManager *manager, DdNode *f, DdNode *cube, unsigned int limit)
Existentially abstracts all the variables in cube from f.
Definition: cuddBddAbs.c:141

Cudd_ReadPerm
int Cudd_ReadPerm(DdManager *dd, int i)
Returns the current position of the i-th variable in the order.
Definition: cuddAPI.c:2527

Cudd_SetMaxMemory
size_t Cudd_SetMaxMemory(DdManager *dd, size_t maxMemory)
Sets the maximum allowed memory.
Definition: cuddAPI.c:4219

Cudd_PrintLinear
int Cudd_PrintLinear(DdManager *table)
Prints the linear transform matrix.
Definition: cuddLinear.c:112

Cudd_bddNewVarAtLevel
DdNode * Cudd_bddNewVarAtLevel(DdManager *dd, int level)
Returns a new BDD variable at a specified level.
Definition: cuddAPI.c:210

Cudd_ShuffleHeap
int Cudd_ShuffleHeap(DdManager *table, int *permutation)
Reorders variables according to given permutation.
Definition: cuddReorder.c:293

Cudd_ReorderingStatus
int Cudd_ReorderingStatus(DdManager *unique, Cudd_ReorderingType *method)
Reports the status of automatic dynamic reordering of BDDs and ADDs.
Definition: cuddAPI.c:1050

Cudd_PrintInfo
int Cudd_PrintInfo(DdManager *dd, FILE *fp)
Prints out statistics and settings for a CUDD manager.
Definition: cuddAPI.c:3148

Cudd_bddConstrain
DdNode * Cudd_bddConstrain(DdManager *dd, DdNode *f, DdNode *c)
Computes f constrain c.
Definition: cuddGenCof.c:134

Cudd_zddSubset0
DdNode * Cudd_zddSubset0(DdManager *dd, DdNode *P, int var)
Computes the negative cofactor of a ZDD w.r.t. a variable.
Definition: cuddZddSetop.c:314

Cudd_bddCorrelation
double Cudd_bddCorrelation(DdManager *manager, DdNode *f, DdNode *g)
Computes the correlation of f and g.
Definition: cuddBddCorr.c:117

Cudd_bddPermute
DdNode * Cudd_bddPermute(DdManager *manager, DdNode *node, int *permut)
Permutes the variables of a BDD.
Definition: cuddCompose.c:290

Cudd_ApaPrintMintermExp
int Cudd_ApaPrintMintermExp(FILE *fp, DdManager const *dd, DdNode *node, int nvars, int precision)
Prints the number of minterms of a BDD or ADD in exponential format using arbitrary precision arithme...
Definition: cuddApa.c:872

Cudd_bddGenDisjDecomp
int Cudd_bddGenDisjDecomp(DdManager *dd, DdNode *f, DdNode ***disjuncts)
Performs two-way disjunctive decomposition of a BDD.
Definition: cuddDecomp.c:550

Cudd_bddCompose
DdNode * Cudd_bddCompose(DdManager *dd, DdNode *f, DdNode *g, int v)
Substitutes g for x_v in the BDD for f.
Definition: cuddCompose.c:116

Cudd_Srandom
void Cudd_Srandom(DdManager *dd, int32_t seed)
Initializer for the portable random number generator.
Definition: cuddUtil.c:2821

Cudd_ApaSetToLiteral
void Cudd_ApaSetToLiteral(int digits, DdApaNumber number, DdApaDigit literal)
Sets an arbitrary precision integer to a one-digit literal.
Definition: cuddApa.c:369

Cudd_addVectorCompose
DdNode * Cudd_addVectorCompose(DdManager *dd, DdNode *f, DdNode **vector)
Composes an ADD with a vector of 0-1 ADDs.
Definition: cuddCompose.c:526

Cudd_bddRealignEnable
void Cudd_bddRealignEnable(DdManager *unique)
Enables realignment of BDD order to ZDD order.
Definition: cuddAPI.c:1247

Cudd_ReadCacheHits
double Cudd_ReadCacheHits(DdManager *dd)
Returns the number of cache hits.
Definition: cuddAPI.c:1498

Cudd_bddLeqUnless
int Cudd_bddLeqUnless(DdManager *dd, DdNode *f, DdNode *g, DdNode *D)
Tells whether f is less than of equal to G unless D is 1.
Definition: cuddSat.c:595

Cudd_ReadInvPermZdd
int Cudd_ReadInvPermZdd(DdManager *dd, int i)
Returns the index of the ZDD variable currently in the i-th position of the order.
Definition: cuddAPI.c:2599

Cudd_CountPath
double Cudd_CountPath(DdNode *node)
Counts the paths of a DD.
Definition: cuddUtil.c:638

Cudd_SetTimeLimit
unsigned long Cudd_SetTimeLimit(DdManager *unique, unsigned long tl)
Sets the time limit for the manager.
Definition: cuddAPI.c:749

Cudd_FindTwoLiteralClauses
DdTlcInfo * Cudd_FindTwoLiteralClauses(DdManager *dd, DdNode *f)
Finds the two literal clauses of a DD.
Definition: cuddEssent.c:244

Cudd_zddPrintDebug
int Cudd_zddPrintDebug(DdManager *zdd, DdNode *f, int n, int pr)
Prints to the standard output a ZDD and its statistics.
Definition: cuddZddUtil.c:178

Cudd_bddIsVar
int Cudd_bddIsVar(DdManager *dd, DdNode *f)
Returns 1 if the given node is a BDD variable; 0 otherwise.
Definition: cuddAPI.c:236

Cudd_SetNextReordering
void Cudd_SetNextReordering(DdManager *dd, unsigned int next)
Sets the threshold for the next dynamic reordering.
Definition: cuddAPI.c:4119

Cudd_PrintMinterm
int Cudd_PrintMinterm(DdManager *manager, DdNode *node)
Prints a disjoint sum of products.
Definition: cuddUtil.c:141

DD_HFP
int(* DD_HFP)(DdManager *, const char *, void *)
Type of hook function.
Definition: cudd.h:234

Cudd_ReadUsedSlots
double Cudd_ReadUsedSlots(DdManager *dd)
Reads the fraction of used slots in the unique table.
Definition: cuddAPI.c:1749

Cudd_addPlus
DdNode * Cudd_addPlus(DdManager *dd, DdNode **f, DdNode **g)
Integer and floating point addition.
Definition: cuddAddApply.c:132

Cudd_SymmProfile
void Cudd_SymmProfile(DdManager *table, int lower, int upper)
Prints statistics on symmetric variables.
Definition: cuddSymmetry.c:106

Cudd_ReadCacheUsedSlots
double Cudd_ReadCacheUsedSlots(DdManager *dd)
Reads the fraction of used slots in the cache.
Definition: cuddAPI.c:1454

Cudd_addBddInterval
DdNode * Cudd_addBddInterval(DdManager *dd, DdNode *f, CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper)
Converts an ADD to a BDD.
Definition: cuddBridge.c:207

Cudd_ReadZddSize
int Cudd_ReadZddSize(DdManager *dd)
Returns the number of ZDD variables in existance.
Definition: cuddAPI.c:1711

Cudd_RemapUnderApprox
DdNode * Cudd_RemapUnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
Extracts a dense subset from a BDD with the remapping underapproximation method.
Definition: cuddApprox.c:294

Cudd_bddIsPsVar
int Cudd_bddIsPsVar(DdManager *dd, int index)
Checks whether a variable is present state.
Definition: cuddAPI.c:4417

Cudd_addIthBit
DdNode * Cudd_addIthBit(DdManager *dd, DdNode *f, int bit)
Extracts the i-th bit from an ADD.
Definition: cuddAddFind.c:190

Cudd_zddRealignEnable
void Cudd_zddRealignEnable(DdManager *unique)
Enables realignment of ZDD order to BDD order.
Definition: cuddAPI.c:1176

Cudd_bddSetNsVar
int Cudd_bddSetNsVar(DdManager *dd, int index)
Sets a variable type to next state.
Definition: cuddAPI.c:4370

Cudd_ReadRecomb
int Cudd_ReadRecomb(DdManager *dd)
Returns the current value of the recombination parameter used in group sifting.
Definition: cuddAPI.c:2857

Cudd_E
DdNode * Cudd_E(DdNode *node)
Returns the else child of an internal node.
Definition: cuddAPI.c:611

Cudd_BddToAdd
DdNode * Cudd_BddToAdd(DdManager *dd, DdNode *B)
Converts a BDD to a 0-1 ADD.
Definition: cuddBridge.c:318

Cudd_ReadErrorCode
Cudd_ErrorType Cudd_ReadErrorCode(DdManager *dd)
Returns the code of the last error.
Definition: cuddAPI.c:3961

Cudd_zddWeakDiv
DdNode * Cudd_zddWeakDiv(DdManager *dd, DdNode *f, DdNode *g)
Applies weak division to two covers.
Definition: cuddZddFuncs.c:173

Cudd_bddXorExistAbstract
DdNode * Cudd_bddXorExistAbstract(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
Takes the exclusive OR of two BDDs and simultaneously abstracts the variables in cube.
Definition: cuddBddAbs.c:187

Cudd_MakeZddTreeNode
MtrNode * Cudd_MakeZddTreeNode(DdManager *dd, unsigned int low, unsigned int size, unsigned int type)
Creates a new ZDD variable group.
Definition: cuddZddGroup.c:118

Cudd_StdPreReordHook
int Cudd_StdPreReordHook(DdManager *dd, const char *str, void *data)
Sample hook function to call before reordering.
Definition: cuddAPI.c:3611

Cudd_zddCount
int Cudd_zddCount(DdManager *zdd, DdNode *P)
Counts the number of minterms in a ZDD.
Definition: cuddZddCount.c:103

Cudd_ClassifySupport
int Cudd_ClassifySupport(DdManager *dd, DdNode *f, DdNode *g, DdNode **common, DdNode **onlyF, DdNode **onlyG)
Classifies the variables in the support of two DDs.
Definition: cuddUtil.c:1183

Cudd_DebugCheck
int Cudd_DebugCheck(DdManager *table)
Checks for inconsistencies in the DD heap.
Definition: cuddCheck.c:117

Cudd_bddVarDisjDecomp
int Cudd_bddVarDisjDecomp(DdManager *dd, DdNode *f, DdNode ***disjuncts)
Performs two-way disjunctive decomposition of a BDD.
Definition: cuddDecomp.c:711

Cudd_IsConstant
int Cudd_IsConstant(DdNode *node)
Returns 1 if the node is a constant node.
Definition: cuddAPI.c:550

Cudd_zddIsop
DdNode * Cudd_zddIsop(DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I)
Computes an ISOP in ZDD form from BDDs.
Definition: cuddZddIsop.c:111

Cudd_addSetNZ
DdNode * Cudd_addSetNZ(DdManager *dd, DdNode **f, DdNode **g)
This operator sets f to the value of g wherever g != 0.
Definition: cuddAddApply.c:244

Cudd_ApaPowerOfTwo
void Cudd_ApaPowerOfTwo(int digits, DdApaNumber number, int power)
Sets an arbitrary precision integer to a power of two.
Definition: cuddApa.c:393

Cudd_bddAndAbstract
DdNode * Cudd_bddAndAbstract(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
Takes the AND of two BDDs and simultaneously abstracts the variables in cube.
Definition: cuddAndAbs.c:104

Cudd_SetMaxReorderings
void Cudd_SetMaxReorderings(DdManager *dd, unsigned int mr)
Sets the maximum number of times reordering may be invoked.
Definition: cuddAPI.c:1968

Cudd_addRead
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)
Reads in a sparse matrix.
Definition: cuddRead.c:132

Cudd_bddClippingAnd
DdNode * Cudd_bddClippingAnd(DdManager *dd, DdNode *f, DdNode *g, int maxDepth, int direction)
Approximates the conjunction of two BDDs f and g.
Definition: cuddClip.c:102

Cudd_ReadSwapSteps
double Cudd_ReadSwapSteps(DdManager *dd)
Reads the number of elementary reordering steps.
Definition: cuddAPI.c:4135

Cudd_bddRestrict
DdNode * Cudd_bddRestrict(DdManager *dd, DdNode *f, DdNode *c)
BDD restrict according to Coudert and Madre&#39;s algorithm (ICCAD90).
Definition: cuddGenCof.c:168

DdNodePtr
DdNode * DdNodePtr
Type of a pointer to a decision diagram node.
Definition: cudd.h:199

Cudd_bddBooleanDiff
DdNode * Cudd_bddBooleanDiff(DdManager *manager, DdNode *f, int x)
Computes the boolean difference of f with respect to x.
Definition: cuddBddAbs.c:267

Cudd_SetMinHit
void Cudd_SetMinHit(DdManager *dd, unsigned int hr)
Sets the hit rate that causes resizinig of the computed table.
Definition: cuddAPI.c:1565

Cudd_bddInterpolate
DdNode * Cudd_bddInterpolate(DdManager *dd, DdNode *l, DdNode *u)
Finds an interpolant of two functions.
Definition: cuddGenCof.c:635

Cudd_bddXnor
DdNode * Cudd_bddXnor(DdManager *dd, DdNode *f, DdNode *g)
Computes the exclusive NOR of two BDDs f and g.
Definition: cuddBddIte.c:551

Cudd_AutodynEnableZdd
void Cudd_AutodynEnableZdd(DdManager *unique, Cudd_ReorderingType method)
Enables automatic dynamic reordering of ZDDs.
Definition: cuddAPI.c:1075

Cudd_bddOr
DdNode * Cudd_bddOr(DdManager *dd, DdNode *f, DdNode *g)
Computes the disjunction of two BDDs f and g.
Definition: cuddBddIte.c:383

Cudd_SetPopulationSize
void Cudd_SetPopulationSize(DdManager *dd, int populationSize)
Sets the size of the population used by the genetic algorithm for variable reordering.
Definition: cuddAPI.c:3027

Cudd_bddIsVarToBeUngrouped
int Cudd_bddIsVarToBeUngrouped(DdManager *dd, int index)
Checks whether a variable is set to be ungrouped.
Definition: cuddAPI.c:4638

Cudd_addNegate
DdNode * Cudd_addNegate(DdManager *dd, DdNode *f)
Computes the additive inverse of an ADD.
Definition: cuddAddNeg.c:98

Cudd_EnableOrderingMonitoring
int Cudd_EnableOrderingMonitoring(DdManager *dd)
Enables monitoring of ordering.
Definition: cuddAPI.c:3846

Cudd_SetArcviolation
void Cudd_SetArcviolation(DdManager *dd, int arcviolation)
Sets the value of the arcviolation parameter used in group sifting.
Definition: cuddAPI.c:2980

Cudd_SetSymmviolation
void Cudd_SetSymmviolation(DdManager *dd, int symmviolation)
Sets the value of the symmviolation parameter used in group sifting.
Definition: cuddAPI.c:2931

Cudd_EqualSupNorm
int Cudd_EqualSupNorm(DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr)
Compares two ADDs for equality within tolerance.
Definition: cuddSat.c:766

Cudd_EstimateCofactor
int Cudd_EstimateCofactor(DdManager *dd, DdNode *node, int i, int phase)
Estimates the number of nodes in a cofactor of a DD.
Definition: cuddUtil.c:471

Cudd_UpdateTimeLimit
void Cudd_UpdateTimeLimit(DdManager *unique)
Updates the time limit for the manager.
Definition: cuddAPI.c:773

Cudd_Increasing
DdNode * Cudd_Increasing(DdManager *dd, DdNode *f, int i)
Checks whether a BDD is positive unate in a variable.
Definition: cuddSat.c:472

Cudd_bddVarIsDependent
int Cudd_bddVarIsDependent(DdManager *dd, DdNode *f, DdNode *var)
Checks whether a variable is dependent on others in a function.
Definition: cuddBddAbs.c:305

Cudd_ApaStringDecimal
char * Cudd_ApaStringDecimal(int digits, DdConstApaNumber number)
converts an arbitrary precision integer to a string in decimal format.
Definition: cuddApa.c:581

Cudd_zddPrintSubtable
void Cudd_zddPrintSubtable(DdManager *table)
Prints the ZDD table for debugging purposes.
Definition: cuddZddMisc.c:155

Cudd_ReadOrderRandomization
unsigned int Cudd_ReadOrderRandomization(DdManager *dd)
Returns the order randomization factor.
Definition: cuddAPI.c:3098

Cudd_ApaCountMinterm
DdApaNumber Cudd_ApaCountMinterm(DdManager const *manager, DdNode *node, int nvars, int *digits)
Counts the number of minterms of a DD.
Definition: cuddApa.c:762

Cudd_PrintDebug
int Cudd_PrintDebug(DdManager *dd, DdNode *f, int n, int pr)
Prints to the manager standard output a DD and its statistics.
Definition: cuddUtil.c:306

DdApaNumber
DdApaDigit * DdApaNumber
Type of an arbitrary precision intger, which is an array of digits.
Definition: cudd.h:219

Cudd_RemoveHook
int Cudd_RemoveHook(DdManager *dd, DD_HFP f, Cudd_HookType where)
Removes a function from a hook.
Definition: cuddAPI.c:3510

EpDoubleStruct
Extended precision double to keep very large value.
Definition: epdInt.h:129

Cudd_bddClippingAndAbstract
DdNode * Cudd_bddClippingAndAbstract(DdManager *dd, DdNode *f, DdNode *g, DdNode *cube, int maxDepth, int direction)
Approximates the conjunction of two BDDs f and g and simultaneously abstracts the variables in cube...
Definition: cuddClip.c:138

Cudd_bddPrintCover
int Cudd_bddPrintCover(DdManager *dd, DdNode *l, DdNode *u)
Prints a sum of prime implicants of a BDD.
Definition: cuddUtil.c:177

Cudd_CheckZeroRef
int Cudd_CheckZeroRef(DdManager *manager)
Checks the unique table for nodes with non-zero reference counts.
Definition: cuddRef.c:425

Cudd_AutodynDisable
void Cudd_AutodynDisable(DdManager *unique)
Disables automatic dynamic reordering.
Definition: cuddAPI.c:1024

Cudd_zddUnateProduct
DdNode * Cudd_zddUnateProduct(DdManager *dd, DdNode *f, DdNode *g)
Computes the product of two unate covers represented as ZDDs.
Definition: cuddZddFuncs.c:136

Cudd_ApaPrintMinterm
int Cudd_ApaPrintMinterm(FILE *fp, DdManager const *dd, DdNode *node, int nvars)
Prints the number of minterms of a BDD or ADD using arbitrary precision arithmetic.
Definition: cuddApa.c:834

Cudd_bddCharToVect
DdNode ** Cudd_bddCharToVect(DdManager *dd, DdNode *f)
Computes a vector of BDDs whose image equals a non-zero function.
Definition: cuddGenCof.c:480

Cudd_ReadZddOne
DdNode * Cudd_ReadZddOne(DdManager *dd, int i)
Returns the ZDD for the constant 1 function.
Definition: cuddAPI.c:1308

Cudd_addGeneralVectorCompose
DdNode * Cudd_addGeneralVectorCompose(DdManager *dd, DdNode *f, DdNode **vectorOn, DdNode **vectorOff)
Composes an ADD with a vector of ADDs.
Definition: cuddCompose.c:588

Cudd_ReadLooseUpTo
unsigned int Cudd_ReadLooseUpTo(DdManager *dd)
Reads the looseUpTo parameter of the manager.
Definition: cuddAPI.c:1585

Cudd_ReadStartTime
unsigned long Cudd_ReadStartTime(DdManager *unique)
Returns the start time of the manager.
Definition: cuddAPI.c:649

DD_THFP
int(* DD_THFP)(const void *)
Type of termination handler.
Definition: cudd.h:266

Cudd_bddIsop
DdNode * Cudd_bddIsop(DdManager *dd, DdNode *L, DdNode *U)
Computes a BDD in the interval between L and U with a simple sum-of-product cover.
Definition: cuddZddIsop.c:151

Cudd_VarsAreSymmetric
int Cudd_VarsAreSymmetric(DdManager *dd, DdNode *f, int index1, int index2)
Checks whether two variables are symmetric in a BDD.
Definition: cuddCof.c:174

Cudd_zddReduceHeap
int Cudd_zddReduceHeap(DdManager *table, Cudd_ReorderingType heuristic, int minsize)
Main dynamic reordering routine for ZDDs.
Definition: cuddZddReord.c:127

Cudd_Dxygtdxz
DdNode * Cudd_Dxygtdxz(DdManager *dd, int N, DdNode **x, DdNode **y, DdNode **z)
Generates a BDD for the function d(x,y) > d(x,z).
Definition: cuddPriority.c:449

Cudd_EnableReorderingReporting
int Cudd_EnableReorderingReporting(DdManager *dd)
Enables reporting of reordering stats.
Definition: cuddAPI.c:3736

Cudd_bddIsVarToBeGrouped
int Cudd_bddIsVarToBeGrouped(DdManager *dd, int index)
Checks whether a variable is set to be grouped.
Definition: cuddAPI.c:4586

Cudd_ReadOne
DdNode * Cudd_ReadOne(DdManager *dd)
Returns the one constant of the manager.
Definition: cuddAPI.c:1286

Cudd_bddLeq
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Checks whether f is less than or equal to g.
Definition: cuddBddIte.c:620

Cudd_ReadNodeCount
long Cudd_ReadNodeCount(DdManager *dd)
Reports the number of nodes in BDDs and ADDs.
Definition: cuddAPI.c:3384

Cudd_ApaCompare
int Cudd_ApaCompare(int digitsFirst, DdConstApaNumber first, int digitsSecond, DdConstApaNumber second)
Compares two arbitrary precision integers.
Definition: cuddApa.c:421

Cudd_ReadUniqueLinks
double Cudd_ReadUniqueLinks(DdManager *dd)
Returns the number of links followed in the unique table.
Definition: cuddAPI.c:2131

Cudd_ReadMinusInfinity
DdNode * Cudd_ReadMinusInfinity(DdManager *dd)
Reads the minus-infinity constant from the manager.
Definition: cuddAPI.c:1382

Cudd_CountPathsToNonZero
double Cudd_CountPathsToNonZero(DdNode *node)
Counts the paths to a non-zero terminal of a DD.
Definition: cuddUtil.c:801

Cudd_addIte
DdNode * Cudd_addIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Implements ITE(f,g,h).
Definition: cuddAddIte.c:103

Cudd_Inequality
DdNode * Cudd_Inequality(DdManager *dd, int N, int c, DdNode **x, DdNode **y)
Generates a BDD for the function x - y ≥ c.
Definition: cuddPriority.c:697

Cudd_addFindMax
DdNode * Cudd_addFindMax(DdManager *dd, DdNode *f)
Finds the maximum discriminant of f.
Definition: cuddAddFind.c:97

DdApaDigit
uint32_t DdApaDigit
Type of an arbitrary precision integer "digit.".
Definition: cudd.h:214

Cudd_DisableGarbageCollection
void Cudd_DisableGarbageCollection(DdManager *dd)
Disables garbage collection.
Definition: cuddAPI.c:2772

Cudd_zddDivideF
DdNode * Cudd_zddDivideF(DdManager *dd, DdNode *f, DdNode *g)
Modified version of Cudd_zddDivide.
Definition: cuddZddFuncs.c:265

Cudd_ReadCacheLookUps
double Cudd_ReadCacheLookUps(DdManager *dd)
Returns the number of cache look-ups.
Definition: cuddAPI.c:1480

Cudd_bddApproxConjDecomp
int Cudd_bddApproxConjDecomp(DdManager *dd, DdNode *f, DdNode ***conjuncts)
Performs two-way conjunctive decomposition of a BDD.
Definition: cuddDecomp.c:152

Cudd_ReadStderr
FILE * Cudd_ReadStderr(DdManager *dd)
Reads the stderr of a manager.
Definition: cuddAPI.c:4057

Cudd_addRestrict
DdNode * Cudd_addRestrict(DdManager *dd, DdNode *f, DdNode *c)
ADD restrict according to Coudert and Madre&#39;s algorithm (ICCAD90).
Definition: cuddGenCof.c:396

DdTlcInfo
This structure holds the set of clauses for a node.
Definition: cuddEssent.c:94

Cudd_addTriangle
DdNode * Cudd_addTriangle(DdManager *dd, DdNode *f, DdNode *g, DdNode **z, int nz)
Performs the triangulation step for the shortest path computation.
Definition: cuddMatMult.c:224

Cudd_SubsetShortPaths
DdNode * Cudd_SubsetShortPaths(DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit)
Extracts a dense subset from a BDD with the shortest paths heuristic.
Definition: cuddSubsetSP.c:186

Cudd_addMinus
DdNode * Cudd_addMinus(DdManager *dd, DdNode **f, DdNode **g)
Integer and floating point subtraction.
Definition: cuddAddApply.c:307

Cudd_bddSetPsVar
int Cudd_bddSetPsVar(DdManager *dd, int index)
Sets a variable type to present state.
Definition: cuddAPI.c:4346

Cudd_Density
double Cudd_Density(DdManager *dd, DdNode *f, int nvars)
Computes the density of a BDD or ADD.
Definition: cuddUtil.c:2860

Cudd_RegisterOutOfMemoryCallback
DD_OOMFP Cudd_RegisterOutOfMemoryCallback(DdManager *unique, DD_OOMFP callback)
Installs an out-of-memory callback.
Definition: cuddAPI.c:906

Cudd_ReadMaxLive
unsigned int Cudd_ReadMaxLive(DdManager *dd)
Reads the maximum allowed number of live nodes.
Definition: cuddAPI.c:4159

Cudd_ReadTree
MtrNode * Cudd_ReadTree(DdManager *dd)
Returns the variable group tree of the manager.
Definition: cuddAPI.c:2378

Cudd_UnderApprox
DdNode * Cudd_UnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)
Extracts a dense subset from a BDD with Shiple&#39;s underapproximation method.
Definition: cuddApprox.c:198

Cudd_NodeReadIndex
unsigned int Cudd_NodeReadIndex(DdNode *node)
Returns the index of the node.
Definition: cuddAPI.c:2506

Cudd_Prime
unsigned int Cudd_Prime(unsigned int p)
Returns the next prime ≥ p.
Definition: cuddTable.c:143

Cudd_zddPrintMinterm
int Cudd_zddPrintMinterm(DdManager *zdd, DdNode *node)
Prints a disjoint sum of product form for a ZDD.
Definition: cuddZddUtil.c:104

Cudd_AddHook
int Cudd_AddHook(DdManager *dd, DD_HFP f, Cudd_HookType where)
Adds a function to a hook.
Definition: cuddAPI.c:3448

Cudd_ReadReorderingCycle
int Cudd_ReadReorderingCycle(DdManager *dd)
Reads the reordCycle parameter of the manager.
Definition: cuddAPI.c:2339

Cudd_VectorSupportIndices
int Cudd_VectorSupportIndices(DdManager *dd, DdNode **F, int n, int **indices)
Finds the variables on which a set of DDs depends.
Definition: cuddUtil.c:996

Cudd_bddIthVar
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Returns the BDD variable with index i.
Definition: cuddAPI.c:301

Cudd_bddSetPairIndex
int Cudd_bddSetPairIndex(DdManager *dd, int index, int pairIndex)
Sets a corresponding pair index for a given index.
Definition: cuddAPI.c:4463

Cudd_ReadApplicationHook
void * Cudd_ReadApplicationHook(DdManager *dd)
Reads the application hook.
Definition: cuddAPI.c:3942

Cudd_IncreaseTimeLimit
void Cudd_IncreaseTimeLimit(DdManager *unique, unsigned long increase)
Increases the time limit for the manager.
Definition: cuddAPI.c:801

Cudd_CheckKeys
int Cudd_CheckKeys(DdManager *table)
Checks for several conditions that should not occur.
Definition: cuddCheck.c:431

Cudd_bddXor
DdNode * Cudd_bddXor(DdManager *dd, DdNode *f, DdNode *g)
Computes the exclusive OR of two BDDs f and g.
Definition: cuddBddIte.c:519

Cudd_ReadReorderings
unsigned int Cudd_ReadReorderings(DdManager *dd)
Returns the number of times reordering has occurred.
Definition: cuddAPI.c:1932

Cudd_addOuterSum
DdNode * Cudd_addOuterSum(DdManager *dd, DdNode *M, DdNode *r, DdNode *c)
Takes the minimum of a matrix and the outer sum of two vectors.
Definition: cuddMatMult.c:278

Cudd_SetGroupcheck
void Cudd_SetGroupcheck(DdManager *dd, Cudd_AggregationType gc)
Sets the parameter groupcheck of the manager to gc.
Definition: cuddAPI.c:2708

Cudd_GenFree
int Cudd_GenFree(DdGen *gen)
Frees a CUDD generator.
Definition: cuddUtil.c:2563

Cudd_addTimesPlus
DdNode * Cudd_addTimesPlus(DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz)
Calculates the product of two matrices represented as ADDs.
Definition: cuddMatMult.c:166

DD_AOP
DdNode *(* DD_AOP)(DdManager *, DdNode **, DdNode **)
Type of apply operator.
Definition: cudd.h:242

Cudd_bddRealignDisable
void Cudd_bddRealignDisable(DdManager *unique)
Disables realignment of ZDD order to BDD order.
Definition: cuddAPI.c:1266

Cudd_FirstCube
DdGen * Cudd_FirstCube(DdManager *dd, DdNode *f, int **cube, CUDD_VALUE_TYPE *value)
Finds the first cube of a decision diagram.
Definition: cuddUtil.c:1881

Cudd_SupportIndex
int * Cudd_SupportIndex(DdManager *dd, DdNode *f)
Finds the variables on which a DD depends.
Definition: cuddUtil.c:927

Cudd_VectorSupportSize
int Cudd_VectorSupportSize(DdManager *dd, DdNode **F, int n)
Counts the variables on which a set of DDs depends.
Definition: cuddUtil.c:1145

Cudd_ReadKeys
unsigned int Cudd_ReadKeys(DdManager *dd)
Returns the number of nodes in the unique table.
Definition: cuddAPI.c:1869

Cudd_SetMaxGrowth
void Cudd_SetMaxGrowth(DdManager *dd, double mg)
Sets the maxGrowth parameter of the manager.
Definition: cuddAPI.c:2270

Cudd_IsInHook
int Cudd_IsInHook(DdManager *dd, DD_HFP f, Cudd_HookType where)
Checks whether a function is in a hook.
Definition: cuddAPI.c:3563

Cudd_bddUnbindVar
int Cudd_bddUnbindVar(DdManager *dd, int index)
Allows the sifting of a variable.
Definition: cuddAPI.c:4272

Cudd_bddReadPairIndex
int Cudd_bddReadPairIndex(DdManager *dd, int index)
Reads a corresponding pair index for a given index.
Definition: cuddAPI.c:4489

Cudd_ApaPrintExponential
int Cudd_ApaPrintExponential(FILE *fp, int digits, DdConstApaNumber number, int precision)
Prints an arbitrary precision integer in exponential format.
Definition: cuddApa.c:643

Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Computes the conjunction of two BDDs f and g.
Definition: cuddBddIte.c:314

Cudd_bddRealignmentEnabled
int Cudd_bddRealignmentEnabled(DdManager *unique)
Tells whether the realignment of BDD order to ZDD order is enabled.
Definition: cuddAPI.c:1218

Cudd_DelayedDerefBdd
void Cudd_DelayedDerefBdd(DdManager *table, DdNode *n)
Decreases the reference count of BDD node n.
Definition: cuddRef.c:237

Cudd_zddIthVar
DdNode * Cudd_zddIthVar(DdManager *dd, int i)
Returns the ZDD variable with index i.
Definition: cuddAPI.c:336

Cudd_ReadPopulationSize
int Cudd_ReadPopulationSize(DdManager *dd)
Reads the current size of the population used by the genetic algorithm for variable reordering...
Definition: cuddAPI.c:3004

Cudd_DumpDaVinci
int Cudd_DumpDaVinci(DdManager *dd, int n, DdNode **f, char const *const *inames, char const *const *onames, FILE *fp)
Writes a daVinci file representing the argument BDDs.
Definition: cuddExport.c:592

Cudd_PrintGroupedOrder
int Cudd_PrintGroupedOrder(DdManager *dd, const char *str, void *data)
Hook function to print the current variable order.
Definition: cuddAPI.c:3809

Cudd_addDiff
DdNode * Cudd_addDiff(DdManager *dd, DdNode **f, DdNode **g)
Returns plusinfinity if f=g; returns min(f,g) if f!=g.
Definition: cuddAddApply.c:467

Cudd_zddSymmProfile
void Cudd_zddSymmProfile(DdManager *table, int lower, int upper)
Prints statistics on symmetric ZDD variables.
Definition: cuddZddSymm.c:104

Cudd_SupersetCompress
DdNode * Cudd_SupersetCompress(DdManager *dd, DdNode *f, int nvars, int threshold)
Find a dense superset of BDD f.
Definition: cuddGenCof.c:760

DD_PRFP
DdNode *(* DD_PRFP)(DdManager *, int, DdNode **, DdNode **, DdNode **)
Type of priority function.
Definition: cudd.h:238

Cudd_zddVarsFromBddVars
int Cudd_zddVarsFromBddVars(DdManager *dd, int multiplicity)
Creates one or more ZDD variables for each BDD variable.
Definition: cuddAPI.c:415

Cudd_FreeTree
void Cudd_FreeTree(DdManager *dd)
Frees the variable group tree of the manager.
Definition: cuddAPI.c:2420

Cudd_zddPrintCover
int Cudd_zddPrintCover(DdManager *zdd, DdNode *node)
Prints a sum of products from a ZDD representing a cover.
Definition: cuddZddUtil.c:136

Cudd_VectorSupportIndex
int * Cudd_VectorSupportIndex(DdManager *dd, DdNode **F, int n)
Finds the variables on which a set of DDs depends.
Definition: cuddUtil.c:1099

Cudd_DumpBlif
int Cudd_DumpBlif(DdManager *dd, int n, DdNode **f, char const *const *inames, char const *const *onames, char *mname, FILE *fp, int mv)
Writes a blif file representing the argument BDDs.
Definition: cuddExport.c:110

Cudd_ReadPermZdd
int Cudd_ReadPermZdd(DdManager *dd, int i)
Returns the current position of the i-th ZDD variable in the order.
Definition: cuddAPI.c:2551

Cudd_ApaCopy
void Cudd_ApaCopy(int digits, DdConstApaNumber source, DdApaNumber dest)
Makes a copy of an arbitrary precision integer.
Definition: cuddApa.c:191

Cudd_zddCountDouble
double Cudd_zddCountDouble(DdManager *zdd, DdNode *P)
Counts the number of minterms of a ZDD.
Definition: cuddZddCount.c:141

Cudd_Quit
void Cudd_Quit(DdManager *unique)
Deletes resources associated with a DD manager.
Definition: cuddInit.c:196

Cudd_ReduceHeap
int Cudd_ReduceHeap(DdManager *table, Cudd_ReorderingType heuristic, int minsize)
Main dynamic reordering routine.
Definition: cuddReorder.c:127

Cudd_AutodynEnable
void Cudd_AutodynEnable(DdManager *unique, Cudd_ReorderingType method)
Enables automatic dynamic reordering of BDDs and ADDs.
Definition: cuddAPI.c:988

Cudd_ReadMaxGrowthAlternate
double Cudd_ReadMaxGrowthAlternate(DdManager *dd)
Reads the maxGrowthAlt parameter of the manager.
Definition: cuddAPI.c:2294

Cudd_addExistAbstract
DdNode * Cudd_addExistAbstract(DdManager *manager, DdNode *f, DdNode *cube)
Existentially Abstracts all the variables in cube from f.
Definition: cuddAddAbs.c:103

Cudd_ApaNumberOfDigits
int Cudd_ApaNumberOfDigits(int binaryDigits)
Returns the number of digits for an arbitrary precision integer.
Definition: cuddApa.c:136

Cudd_addUnivAbstract
DdNode * Cudd_addUnivAbstract(DdManager *manager, DdNode *f, DdNode *cube)
Universally Abstracts all the variables in cube from f.
Definition: cuddAddAbs.c:143

Cudd_TurnOnCountDead
void Cudd_TurnOnCountDead(DdManager *dd)
Causes the dead nodes to be counted towards triggering reordering.
Definition: cuddAPI.c:2813

Cudd_bddCorrelationWeights
double Cudd_bddCorrelationWeights(DdManager *manager, DdNode *f, DdNode *g, double *prob)
Computes the correlation of f and g for given input probabilities.
Definition: cuddBddCorr.c:157

Cudd_addHamming
DdNode * Cudd_addHamming(DdManager *dd, DdNode **xVars, DdNode **yVars, int nVars)
Computes the Hamming distance ADD.
Definition: cuddPriority.c:1207

Cudd_ApaCompareRatios
int Cudd_ApaCompareRatios(int digitsFirst, DdConstApaNumber firstNum, unsigned int firstDen, int digitsSecond, DdConstApaNumber secondNum, unsigned int secondDen)
Compares the ratios of two arbitrary precision integers to two unsigned ints.
Definition: cuddApa.c:457

Cudd_ReadPeakNodeCount
long Cudd_ReadPeakNodeCount(DdManager *dd)
Reports the peak number of nodes.
Definition: cuddAPI.c:3334

Cudd_Ref
void Cudd_Ref(DdNode *n)
Increases the reference count of a node, if it is not saturated.
Definition: cuddRef.c:96

onames
static char const  * onames[]
Definition: ntr.c:67

Cudd_addMatrixMultiply
DdNode * Cudd_addMatrixMultiply(DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz)
Calculates the product of two matrices represented as ADDs.
Definition: cuddMatMult.c:110

Cudd_ReadSiftMaxSwap
int Cudd_ReadSiftMaxSwap(DdManager *dd)
Reads the siftMaxSwap parameter of the manager.
Definition: cuddAPI.c:2200

Cudd_addNand
DdNode * Cudd_addNand(DdManager *dd, DdNode **f, DdNode **g)
NAND of two 0-1 ADDs.
Definition: cuddAddApply.c:566

Cudd_ReadDead
unsigned int Cudd_ReadDead(DdManager *dd)
Returns the number of dead nodes in the unique table.
Definition: cuddAPI.c:1886

Cudd_addTimes
DdNode * Cudd_addTimes(DdManager *dd, DdNode **f, DdNode **g)
Integer and floating point multiplication.
Definition: cuddAddApply.c:172

Cudd_StdPostReordHook
int Cudd_StdPostReordHook(DdManager *dd, const char *str, void *data)
Sample hook function to call after reordering.
Definition: cuddAPI.c:3703

Cudd_addNewVar
DdNode * Cudd_addNewVar(DdManager *dd)
Returns a new ADD variable.
Definition: cuddAPI.c:105

Cudd_DisableOrderingMonitoring
int Cudd_DisableOrderingMonitoring(DdManager *dd)
Disables monitoring of ordering.
Definition: cuddAPI.c:3878

Cudd_ReadSiftMaxVar
int Cudd_ReadSiftMaxVar(DdManager *dd)
Reads the siftMaxVar parameter of the manager.
Definition: cuddAPI.c:2156

Cudd_ReadMaxGrowth
double Cudd_ReadMaxGrowth(DdManager *dd)
Reads the maxGrowth parameter of the manager.
Definition: cuddAPI.c:2247

Cudd_GarbageCollectionEnabled
int Cudd_GarbageCollectionEnabled(DdManager *dd)
Tells whether garbage collection is enabled.
Definition: cuddAPI.c:2728

Cudd_ReorderingType
Cudd_ReorderingType
Type of reordering algorithm.
Definition: cudd.h:94

Cudd_SupportSize
int Cudd_SupportSize(DdManager *dd, DdNode *f)
Counts the variables on which a DD depends.
Definition: cuddUtil.c:966

Cudd_SetSiftMaxSwap
void Cudd_SetSiftMaxSwap(DdManager *dd, int sms)
Sets the siftMaxSwap parameter of the manager.
Definition: cuddAPI.c:2223

Cudd_ReadSlots
unsigned int Cudd_ReadSlots(DdManager *dd)
Returns the total number of slots of the unique table.
Definition: cuddAPI.c:1728

Cudd_MinHammingDist
int Cudd_MinHammingDist(DdManager *dd, DdNode *f, int *minterm, int upperBound)
Returns the minimum Hamming distance between f and minterm.
Definition: cuddPriority.c:1271

Cudd_ReadStdout
FILE * Cudd_ReadStdout(DdManager *dd)
Reads the stdout of a manager.
Definition: cuddAPI.c:4018

Cudd_SplitSet
DdNode * Cudd_SplitSet(DdManager *manager, DdNode *S, DdNode **xVars, int n, double m)
Returns m minterms from a BDD.
Definition: cuddSplit.c:106

Cudd_bddIntersect
DdNode * Cudd_bddIntersect(DdManager *dd, DdNode *f, DdNode *g)
Returns a function included in the intersection of f and g.
Definition: cuddBddIte.c:281

Cudd_addWalsh
DdNode * Cudd_addWalsh(DdManager *dd, DdNode **x, DdNode **y, int n)
Generates a Walsh matrix in ADD form.
Definition: cuddAddWalsh.c:100

Cudd_SharingSize
int Cudd_SharingSize(DdNode **nodeArray, int n)
Counts the number of nodes in an array of DDs.
Definition: cuddUtil.c:542

Cudd_Disequality
DdNode * Cudd_Disequality(DdManager *dd, int N, int c, DdNode **x, DdNode **y)
Generates a BDD for the function x - y != c.
Definition: cuddPriority.c:884

Cudd_addMinimum
DdNode * Cudd_addMinimum(DdManager *dd, DdNode **f, DdNode **g)
Integer and floating point min.
Definition: cuddAddApply.c:343

Cudd_LazyGroupType
Cudd_LazyGroupType
Group type for lazy sifting.
Definition: cudd.h:166

Cudd_SetMaxLive
void Cudd_SetMaxLive(DdManager *dd, unsigned int maxLive)
Sets the maximum allowed number of live nodes.
Definition: cuddAPI.c:4178

Cudd_SetStderr
void Cudd_SetStderr(DdManager *dd, FILE *fp)
Sets the stderr of a manager.
Definition: cuddAPI.c:4074

Cudd_ReadGarbageCollections
int Cudd_ReadGarbageCollections(DdManager *dd)
Returns the number of times garbage collection has occurred.
Definition: cuddAPI.c:2009

Cudd_ReadEpsilon
CUDD_VALUE_TYPE Cudd_ReadEpsilon(DdManager *dd)
Reads the epsilon parameter of the manager.
Definition: cuddAPI.c:2647

Cudd_zddSupport
DdNode * Cudd_zddSupport(DdManager *dd, DdNode *f)
Finds the variables on which a ZDD depends.
Definition: cuddZddUtil.c:495

Cudd_DumpBlifBody
int Cudd_DumpBlifBody(DdManager *dd, int n, DdNode **f, char const *const *inames, char const *const *onames, FILE *fp, int mv)
Writes a blif body representing the argument BDDs.
Definition: cuddExport.c:226

CUDD_VALUE_TYPE
double CUDD_VALUE_TYPE
Type of the value of a terminal node.
Definition: cudd.h:189

Cudd_DumpDot
int Cudd_DumpDot(DdManager *dd, int n, DdNode **f, char const *const *inames, char const *const *onames, FILE *fp)
Writes a dot file representing the argument DDs.
Definition: cuddExport.c:309

Cudd_addOneZeroMaximum
DdNode * Cudd_addOneZeroMaximum(DdManager *dd, DdNode **f, DdNode **g)
Returns 1 if f > g and 0 otherwise.
Definition: cuddAddApply.c:433

Cudd_addBddStrictThreshold
DdNode * Cudd_addBddStrictThreshold(DdManager *dd, DdNode *f, CUDD_VALUE_TYPE value)
Converts an ADD to a BDD.
Definition: cuddBridge.c:158

Cudd_zddRealignDisable
void Cudd_zddRealignDisable(DdManager *unique)
Disables realignment of ZDD order to BDD order.
Definition: cuddAPI.c:1195

Cudd_VectorSupport
DdNode * Cudd_VectorSupport(DdManager *dd, DdNode **F, int n)
Finds the variables on which a set of DDs depends.
Definition: cuddUtil.c:1048

Cudd_DisableReorderingReporting
int Cudd_DisableReorderingReporting(DdManager *dd)
Disables reporting of reordering stats.
Definition: cuddAPI.c:3762

Cudd_ExpectedUsedSlots
double Cudd_ExpectedUsedSlots(DdManager *dd)
Computes the expected fraction of used slots in the unique table.
Definition: cuddAPI.c:1816

Cudd_bddSqueeze
DdNode * Cudd_bddSqueeze(DdManager *dd, DdNode *l, DdNode *u)
Finds a small BDD in a function interval.
Definition: cuddGenCof.c:575

Cudd_BddToCubeArray
int Cudd_BddToCubeArray(DdManager *dd, DdNode *cube, int *array)
Builds a positional array from the BDD of a cube.
Definition: cuddUtil.c:2422

Cudd_bddIterConjDecomp
int Cudd_bddIterConjDecomp(DdManager *dd, DdNode *f, DdNode ***conjuncts)
Performs two-way conjunctive decomposition of a BDD.
Definition: cuddDecomp.c:289

Cudd_addXeqy
DdNode * Cudd_addXeqy(DdManager *dd, int N, DdNode **x, DdNode **y)
Generates an ADD for the function x==y.
Definition: cuddPriority.c:364

Cudd_DagSize
int Cudd_DagSize(DdNode *node)
Counts the number of nodes in a DD.
Definition: cuddUtil.c:436

Cudd_bddXnorLimit
DdNode * Cudd_bddXnorLimit(DdManager *dd, DdNode *f, DdNode *g, unsigned int limit)
Computes the exclusive NOR of two BDDs f and g unless too many nodes are required.
Definition: cuddBddIte.c:584

Cudd_zddCoverPathToString
char * Cudd_zddCoverPathToString(DdManager *zdd, int *path, char *str)
Converts a path of a ZDD representing a cover to a string.
Definition: cuddZddUtil.c:437

Cudd_OrderingMonitoring
int Cudd_OrderingMonitoring(DdManager *dd)
Returns 1 if monitoring of ordering is enabled; 0 otherwise.
Definition: cuddAPI.c:3907

Cudd_ReadUniqueLookUps
double Cudd_ReadUniqueLookUps(DdManager *dd)
Returns the number of look-ups in the unique table.
Definition: cuddAPI.c:2102

Cudd_zddDumpDot
int Cudd_zddDumpDot(DdManager *dd, int n, DdNode **f, char const *const *inames, char const *const *onames, FILE *fp)
Writes a dot file representing the argument ZDDs.
Definition: cuddZddUtil.c:584

Cudd_PrintVersion
void Cudd_PrintVersion(FILE *fp)
Prints the package version number.
Definition: cuddUtil.c:2655

Cudd_FactoredFormString
char * Cudd_FactoredFormString(DdManager *dd, DdNode *f, char const *const *inames)
Returns a string with the factored form of the argument BDDs.
Definition: cuddExport.c:932

Cudd_ReadRecursiveCalls
double Cudd_ReadRecursiveCalls(DdManager *dd)
Returns the number of recursive calls.
Definition: cuddAPI.c:1516

Cudd_ReadArcviolation
int Cudd_ReadArcviolation(DdManager *dd)
Returns the current value of the arcviolation parameter used in group sifting.
Definition: cuddAPI.c:2956