cudd  3.0.0
The University of Colorado Decision Diagram Package
cuddInt.h
Go to the documentation of this file.
1 
46 #ifndef CUDD_INT_H_
47 #define CUDD_INT_H_
48 
49 
50 /*---------------------------------------------------------------------------*/
51 /* Nested includes */
52 /*---------------------------------------------------------------------------*/
53 
54 #include <math.h>
55 #include "config.h"
56 #include "st.h"
57 #include "mtr.h"
58 #include "epd.h"
59 #include "cudd.h"
60 
61 /*---------------------------------------------------------------------------*/
62 /* Constant declarations */
63 /*---------------------------------------------------------------------------*/
64 
65 #define CUDD_VERSION PACKAGE_VERSION
66 
67 #define DD_MAXREF ((DdHalfWord) ~0)
68 
69 #define DD_DEFAULT_RESIZE 10 /* how many extra variables */
70  /* should be added when resizing */
71 #define DD_MEM_CHUNK 1022
72 
73 /* These definitions work for CUDD_VALUE_TYPE == double */
74 #define DD_ONE_VAL (1.0)
75 #define DD_ZERO_VAL (0.0)
76 #define DD_EPSILON (1.0e-12)
77 
78 /* The definitions of +/- infinity in terms of HUGE_VAL work on
79 ** the DECstations and on many other combinations of OS/compiler.
80 */
81 #ifdef HAVE_IEEE_754
82 # define DD_PLUS_INF_VAL (HUGE_VAL)
83 #else
84 # define DD_PLUS_INF_VAL (10e301)
85 # define DD_CRI_HI_MARK (10e150)
86 # define DD_CRI_LO_MARK (-(DD_CRI_HI_MARK))
87 #endif
88 #define DD_MINUS_INF_VAL (-(DD_PLUS_INF_VAL))
89 
90 #define DD_NON_CONSTANT ((DdNode *) 1) /* for Cudd_bddIteConstant */
91 
92 /* Unique table and cache management constants. */
93 #define DD_MAX_SUBTABLE_DENSITY 4 /* tells when to resize a subtable */
94 /* gc when this percent are dead (measured w.r.t. slots, not keys)
95 ** The first limit (LO) applies normally. The second limit applies when
96 ** the package believes more space for the unique table (i.e., more dead
97 ** nodes) would improve performance, and the unique table is not already
98 ** too large. The third limit applies when memory is low.
99 */
100 #define DD_GC_FRAC_LO DD_MAX_SUBTABLE_DENSITY * 0.25
101 #define DD_GC_FRAC_HI DD_MAX_SUBTABLE_DENSITY * 1.0
102 #define DD_GC_FRAC_MIN 0.2
103 #define DD_MIN_HIT 30 /* resize cache when hit ratio
104  above this percentage (default) */
105 #define DD_MAX_LOOSE_FRACTION 5 /* 1 / (max fraction of memory used for
106  unique table in fast growth mode) */
107 #define DD_MAX_CACHE_FRACTION 3 /* 1 / (max fraction of memory used for
108  computed table if resizing enabled) */
109 #define DD_STASH_FRACTION 64 /* 1 / (fraction of memory set
110  aside for emergencies) */
111 #define DD_MAX_CACHE_TO_SLOTS_RATIO 4 /* used to limit the cache size */
112 
113 /* Variable ordering default parameter values. */
114 #define DD_SIFT_MAX_VAR 1000
115 #define DD_SIFT_MAX_SWAPS 2000000
116 #define DD_DEFAULT_RECOMB 0
117 #define DD_MAX_REORDER_GROWTH 1.2
118 #define DD_FIRST_REORDER 4004 /* 4 for the constants */
119 #define DD_DYN_RATIO 2 /* when to dynamically reorder */
120 
121 /* Primes for cache hash functions. */
122 #define DD_P1 12582917
123 #define DD_P2 4256249
124 #define DD_P3 741457
125 #define DD_P4 1618033999
126 
127 /* Cache tags for 3-operand operators. These tags are stored in the
128 ** least significant bits of the cache operand pointers according to
129 ** the following scheme. The tag consists of two hex digits. Both digits
130 ** must be even, so that they do not interfere with complementation bits.
131 ** The least significant one is stored in Bits 3:1 of the f operand in the
132 ** cache entry. Bit 1 is always 1, so that we can differentiate
133 ** three-operand operations from one- and two-operand operations.
134 ** Therefore, the least significant digit is one of {2,6,a,e}. The most
135 ** significant digit occupies Bits 3:1 of the g operand in the cache
136 ** entry. It can by any even digit between 0 and e. This gives a total
137 ** of 5 bits for the tag proper, which means a maximum of 32 three-operand
138 ** operations. */
139 #define DD_ADD_ITE_TAG 0x02
140 #define DD_BDD_AND_ABSTRACT_TAG 0x06
141 #define DD_BDD_XOR_EXIST_ABSTRACT_TAG 0x0a
142 #define DD_BDD_ITE_TAG 0x0e
143 #define DD_ADD_BDD_DO_INTERVAL_TAG 0x22
144 #define DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG 0x26
145 #define DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG 0x2a
146 #define DD_BDD_COMPOSE_RECUR_TAG 0x2e
147 #define DD_ADD_COMPOSE_RECUR_TAG 0x42
148 #define DD_ADD_NON_SIM_COMPOSE_TAG 0x46
149 #define DD_EQUIV_DC_TAG 0x4a
150 #define DD_ZDD_ITE_TAG 0x4e
151 #define DD_ADD_ITE_CONSTANT_TAG 0x62
152 #define DD_ADD_EVAL_CONST_TAG 0x66
153 #define DD_BDD_ITE_CONSTANT_TAG 0x6a
154 #define DD_ADD_OUT_SUM_TAG 0x6e
155 #define DD_BDD_LEQ_UNLESS_TAG 0x82
156 #define DD_ADD_TRIANGLE_TAG 0x86
157 #define DD_BDD_MAX_EXP_TAG 0x8a
158 #define DD_VARS_SYMM_BEFORE_TAG 0x8e
159 #define DD_VARS_SYMM_BETWEEN_TAG 0xa2
160 
161 /* Generator constants. */
162 #define CUDD_GEN_CUBES 0
163 #define CUDD_GEN_PRIMES 1
164 #define CUDD_GEN_NODES 2
165 #define CUDD_GEN_ZDD_PATHS 3
166 #define CUDD_GEN_EMPTY 0
167 #define CUDD_GEN_NONEMPTY 1
168 
176 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
177 #define CUDD_MAXINDEX (((DdHalfWord) ~0) >> 1)
178 #else
179 #define CUDD_MAXINDEX ((DdHalfWord) ~0)
180 #endif
181 
187 #define CUDD_CONST_INDEX CUDD_MAXINDEX
188 
192 #define STAB_SIZE 64
193 
199 #define CUDD_CHECK_MASK 0x7ff
200 
201 /*---------------------------------------------------------------------------*/
202 /* Type declarations */
203 /*---------------------------------------------------------------------------*/
204 
208 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
209 typedef uint32_t DdHalfWord;
210 #else
211 typedef uint16_t DdHalfWord;
212 #endif
213 
224 typedef intptr_t ptrint;
225 
231 typedef uintptr_t ptruint;
232 
233 typedef struct DdChildren DdChildren;
234 typedef struct DdHook DdHook;
235 typedef struct DdSubtable DdSubtable;
236 typedef struct DdCache DdCache;
237 typedef struct DdLocalCacheItem DdLocalCacheItem;
238 typedef struct DdLocalCache DdLocalCache;
239 typedef struct DdHashItem DdHashItem;
240 typedef struct DdHashTable DdHashTable;
241 typedef struct Move Move;
242 typedef struct IndexKey IndexKey;
243 typedef struct DdQueueItem DdQueueItem;
244 typedef struct DdLevelQueue DdLevelQueue;
245 
246 /*---------------------------------------------------------------------------*/
247 /* Stucture declarations */
248 /*---------------------------------------------------------------------------*/
249 
253 struct DdChildren {
254  struct DdNode *T;
255  struct DdNode *E;
256 };
257 
261 struct DdNode {
264  DdNode *next;
265  union {
267  DdChildren kids;
268  } type;
269 };
270 
274 struct DdGen {
275  DdManager *manager;
276  int type;
277  int status;
278  union {
279  struct {
280  int *cube;
281  CUDD_VALUE_TYPE value;
282  } cubes;
283  struct {
284  int *cube;
285  DdNode *ub;
286  } primes;
287  struct {
288  int size;
289  } nodes;
290  } gen;
291  struct {
292  int sp;
293  DdNode **stack;
294  } stack;
295  DdNode *node;
296 };
297 
306 struct DdHook {
307  DD_HFP f;
308  struct DdHook *next;
309 };
310 
314 struct DdLocalCacheItem {
315  DdNode *value;
316 #ifdef DD_CACHE_PROFILE
317  ptrint count;
318 #endif
319  DdNode *key[1];
320 };
321 
325 struct DdLocalCache {
326  DdLocalCacheItem *item;
327  unsigned int itemsize;
328  unsigned int keysize;
329  unsigned int slots;
330  int shift;
331  double lookUps;
332  double minHit;
333  double hits;
334  unsigned int maxslots;
335  DdManager *manager;
336  struct DdLocalCache *next;
337 };
338 
342 struct DdHashItem {
343  struct DdHashItem *next;
344  ptrint count;
345  DdNode *value;
346  DdNode *key[1];
347 };
348 
352 struct DdHashTable {
353  unsigned int keysize;
354  unsigned int itemsize;
358  unsigned int numBuckets;
359  int shift;
360  unsigned int size;
361  unsigned int maxsize;
362  DdManager *manager;
363 };
364 
368 struct DdCache {
369  DdNode *f,*g;
370  ptruint h;
371  DdNode *data;
372 #ifdef DD_CACHE_PROFILE
373  ptrint count;
374 #endif
375 };
376 
380 struct DdSubtable {
382  int shift;
383  unsigned int slots;
384  unsigned int keys;
385  unsigned int maxKeys;
386  unsigned int dead;
387  unsigned int next;
388  int bindVar;
389  /* Fields for lazy sifting. */
391  int pairIndex;
392  int varHandled;
394 };
395 
399 struct DdManager {
400  /* Constants */
403  DdNode *zero;
407  /* Computed Table */
410  unsigned int cacheSlots;
412  double cacheMisses;
413  double cacheHits;
414  double minHit;
416  unsigned int maxCacheHard;
417  /* Unique Table */
418  int size;
419  int sizeZ;
420  int maxSize;
421  int maxSizeZ;
425  unsigned int slots;
426  unsigned int keys;
427  unsigned int keysZ;
428  unsigned int dead;
429  unsigned int deadZ;
430  unsigned int maxLive;
431  unsigned int minDead;
432  int gcEnabled;
433  double gcFrac;
434  unsigned int looseUpTo;
436  unsigned int initSlots;
438  double allocated;
440  double reclaimed;
441  int *perm;
442  int *permZ;
443  int *invperm;
444  int *invpermZ;
446  int *map;
448  unsigned int isolated;
449  unsigned int originalSize;
453  /* Memory Management */
456  char *stash;
457 #ifndef DD_NO_DEATH_ROW
458  DdNode **deathRow;
459  int deathRowDepth;
460  int nextDead;
461  unsigned deadMask;
462 #endif
463  /* General Parameters */
465  /* Dynamic Reordering Parameters */
466  int reordered;
467  unsigned int reorderings;
468  unsigned int maxReorderings;
474  double maxGrowth;
475  double maxGrowthAlt;
476  int autoDyn;
477  int autoDynZ;
480  int realign;
481  int realignZ;
482  unsigned int nextDyn;
483  unsigned int countDead;
487  int recomb;
492  unsigned int randomizeOrder;
494  void *hooks;
499  FILE *out;
500  FILE *err;
502  unsigned long startTime;
503  unsigned long timeLimit;
505  void * tcbArg;
508  void * tohArg;
509  /* Statistical counters. */
510  size_t memused;
511  size_t maxmem;
512  size_t maxmemhard;
514  unsigned long GCTime;
515  unsigned long reordTime;
516  double totCachehits;
517  double totCacheMisses;
519  double cacheinserts;
521  double cachedeletions;
522  unsigned int peakLiveNodes;
523  /* Random number generator. */
524  int32_t cuddRand;
525  int32_t cuddRand2;
526  int32_t shuffleSelect;
527  int32_t shuffleTable[STAB_SIZE];
528 #ifdef DD_STATS
529  double nodesFreed;
530  double nodesDropped;
531  int totalNISwaps;
532  int extsymmcalls;
533  int extsymm;
534  int secdiffcalls;
535  int secdiff;
536  int secdiffmisfire;
537  int tosses;
538  int acceptances;
539  int totalShuffles;
540  int totalNumberLinearTr;
541  int num_calls;
542 #endif
543 #ifdef DD_UNIQUE_PROFILE
544  double uniqueLookUps;
545  double uniqueLinks;
546 #endif
547 #ifdef DD_COUNT
548  double recursiveCalls;
549 #ifdef DD_STATS
550  double nextSample;
551 #endif
552  double swapSteps;
553 #endif
554 #ifdef DD_DEBUG
555  int addPermuteRecurHits;
556  int bddPermuteRecurHits;
557  int bddVectorComposeHits;
558  int addVectorComposeHits;
559  int addGeneralVectorComposeHits;
560  int enableExtraDebug;
561 #endif
562 };
563 
567 struct Move {
568  DdHalfWord x;
569  DdHalfWord y;
570  unsigned int flags;
571  int size;
572  struct Move *next;
573 };
574 
578 struct IndexKey {
579  int index;
580  int keys;
581 };
582 
586 struct DdQueueItem {
587  struct DdQueueItem *next;
588  struct DdQueueItem *cnext;
589  void *key;
590 };
591 
595 struct DdLevelQueue {
596  void *first;
597  DdQueueItem **last;
598  DdQueueItem *freelist;
599  DdQueueItem **buckets;
600  int levels;
601  int itemsize;
602  int size;
603  int maxsize;
604  int numBuckets;
605  int shift;
606  DdManager *manager;
607 };
608 
609 /*---------------------------------------------------------------------------*/
610 /* Variable declarations */
611 /*---------------------------------------------------------------------------*/
612 
613 
614 /*---------------------------------------------------------------------------*/
615 /* Macro declarations */
616 /*---------------------------------------------------------------------------*/
617 
629 #define cuddDeallocNode(unique,node) \
630  (node)->next = (unique)->nextFree; \
631  (unique)->nextFree = node;
632 
644 #define cuddDeallocMove(unique,node) \
645  ((DdNode *)(node))->ref = 0; \
646  ((DdNode *)(node))->next = (unique)->nextFree; \
647  (unique)->nextFree = (DdNode *)(node);
648 
649 
662 #define cuddRef(n) cuddSatInc(Cudd_Regular(n)->ref)
663 
664 
680 #define cuddDeref(n) cuddSatDec(Cudd_Regular(n)->ref)
681 
682 
696 #define Cudd_IsConstantInt(node) ((Cudd_Regular(node))->index == CUDD_CONST_INDEX)
697 
698 
711 #define cuddIsConstant(node) ((node)->index == CUDD_CONST_INDEX)
712 
713 
725 #define cuddT(node) ((node)->type.kids.T)
726 
727 
739 #define cuddE(node) ((node)->type.kids.E)
740 
741 
753 #define cuddV(node) ((node)->type.value)
754 
755 
769 #define cuddI(dd,index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->perm[(index)])
770 
771 
785 #define cuddIZ(dd,index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->permZ[(index)])
786 
787 
798 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
799 #define ddHash(f,g,s) \
800 ((((unsigned)(ptruint)(f) * DD_P1 + \
801  (unsigned)(ptruint)(g)) * DD_P2) >> (s))
802 #else
803 #define ddHash(f,g,s) \
804 ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))
805 #endif
806 
807 
816 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
817 #define ddCHash(o,f,g,h,s) \
818 ((((((unsigned)(ptruint)(f) + (unsigned)(ptruint)(o)) * DD_P1 + \
819  (unsigned)(ptruint)(g)) * DD_P2 + \
820  (unsigned)(ptruint)(h)) * DD_P3) >> (s))
821 #else
822 #define ddCHash(o,f,g,h,s) \
823 ((((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2 + \
824  (unsigned)(h)) * DD_P3) >> (s))
825 #endif
826 
827 
836 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
837 #define ddCHash2(o,f,g,s) \
838 (((((unsigned)(ptruint)(f) + (unsigned)(ptruint)(o)) * DD_P1 + \
839  (unsigned)(ptruint)(g)) * DD_P2) >> (s))
840 #else
841 #define ddCHash2(o,f,g,s) \
842 (((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))
843 #endif
844 
845 
852 #define cuddClean(p) ((DdNode *)((ptruint)(p) & ~ (ptruint) 0xf))
853 
854 
863 #define ddMin(x,y) (((y) < (x)) ? (y) : (x))
864 
865 
874 #define ddMax(x,y) (((y) > (x)) ? (y) : (x))
875 
876 
883 #define ddAbs(x) (((x)<0) ? -(x) : (x))
884 
885 
893 #define ddEqualVal(x,y,e) (ddAbs((x)-(y))<(e))
894 
895 
907 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
908 #define cuddSatInc(x) ((x)++)
909 #else
910 #define cuddSatInc(x) ((x) += (x) != (DdHalfWord)DD_MAXREF)
911 #endif
912 
913 
925 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
926 #define cuddSatDec(x) ((x)--)
927 #else
928 #define cuddSatDec(x) ((x) -= (x) != (DdHalfWord)DD_MAXREF)
929 #endif
930 
931 
940 #define DD_ONE(dd) ((dd)->one)
941 
942 
954 #define DD_ZERO(dd) ((dd)->zero)
955 
956 
965 #define DD_PLUS_INFINITY(dd) ((dd)->plusinfinity)
966 
967 
976 #define DD_MINUS_INFINITY(dd) ((dd)->minusinfinity)
977 
978 
993 #ifdef HAVE_IEEE_754
994 #define cuddAdjust(x)
995 #else
996 #define cuddAdjust(x) ((x) = ((x) >= DD_CRI_HI_MARK) ? DD_PLUS_INF_VAL : (((x) <= DD_CRI_LO_MARK) ? DD_MINUS_INF_VAL : (x)))
997 #endif
998 
999 
1010 #ifdef DD_COUNT
1011 #ifdef DD_STATS
1012 #define statLine(dd) \
1013  do { \
1014  (dd)->recursiveCalls++; \
1015  if ((dd)->recursiveCalls == (dd)->nextSample) { \
1016  (void) fprintf((dd)->err, \
1017  "@%.0f: %u nodes %u live %.0f dropped" \
1018  " %.0f reclaimed\n", \
1019  (dd)->recursiveCalls, (dd)->keys, \
1020  (dd)->keys - (dd)->dead, \
1021  (dd)->nodesDropped, (dd)->reclaimed); \
1022  (dd)->nextSample += 250000;} \
1023  } while (0)
1024 #else
1025 #define statLine(dd) (dd)->recursiveCalls++
1026 #endif
1027 #else
1028 #define statLine(dd)
1029 #endif
1030 
1035 #define checkWhetherToGiveUp(dd) \
1036  do { \
1037  if (((int64_t) CUDD_CHECK_MASK & (int64_t) (dd)->cacheMisses) == 0) { \
1038  if ((dd)->terminationCallback != NULL && \
1039  (dd)->terminationCallback((dd)->tcbArg)) { \
1040  (dd)->errorCode = CUDD_TERMINATION; \
1041  return(NULL); \
1042  } \
1043  if (util_cpu_time() - (dd)->startTime > (dd)->timeLimit) { \
1044  (dd)->errorCode = CUDD_TIMEOUT_EXPIRED; \
1045  return(NULL); \
1046  } \
1047  } \
1048  } while (0)
1049 
1050 
1053 /*---------------------------------------------------------------------------*/
1054 /* Function prototypes */
1055 /*---------------------------------------------------------------------------*/
1056 
1057 #ifdef __cplusplus
1058 extern "C" {
1059 #endif
1060 
1061 extern DdNode * cuddAddExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube);
1062 extern DdNode * cuddAddUnivAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube);
1063 extern DdNode * cuddAddOrAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube);
1064 extern DdNode * cuddAddApplyRecur(DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g);
1065 extern DdNode * cuddAddMonadicApplyRecur(DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f);
1066 extern DdNode * cuddAddScalarInverseRecur(DdManager *dd, DdNode *f, DdNode *epsilon);
1067 extern DdNode * cuddAddIteRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
1068 extern DdNode * cuddAddCmplRecur(DdManager *dd, DdNode *f);
1069 extern DdNode * cuddAddNegateRecur(DdManager *dd, DdNode *f);
1070 extern DdNode * cuddAddRoundOffRecur(DdManager *dd, DdNode *f, double trunc);
1071 extern DdNode * cuddUnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality);
1072 extern DdNode * cuddRemapUnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, double quality);
1073 extern DdNode * cuddBiasedUnderApprox(DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0);
1074 extern DdNode * cuddBddAndAbstractRecur(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube);
1075 extern int cuddAnnealing(DdManager *table, int lower, int upper);
1076 extern DdNode * cuddBddExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube);
1077 extern DdNode * cuddBddXorExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube);
1078 extern DdNode * cuddBddBooleanDiffRecur(DdManager *manager, DdNode *f, DdNode *var);
1079 extern DdNode * cuddBddIteRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
1080 extern DdNode * cuddBddIntersectRecur(DdManager *dd, DdNode *f, DdNode *g);
1081 extern DdNode * cuddBddAndRecur(DdManager *manager, DdNode *f, DdNode *g);
1082 extern DdNode * cuddBddXorRecur(DdManager *manager, DdNode *f, DdNode *g);
1083 extern DdNode * cuddBddTransfer(DdManager *ddS, DdManager *ddD, DdNode *f);
1084 extern DdNode * cuddAddBddDoPattern(DdManager *dd, DdNode *f);
1085 extern int cuddInitCache(DdManager *unique, unsigned int cacheSize, unsigned int maxCacheSize);
1086 extern void cuddCacheInsert(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h, DdNode *data);
1087 extern void cuddCacheInsert2(DdManager *table, DdNode * (*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g, DdNode *data);
1088 extern void cuddCacheInsert1(DdManager *table, DdNode * (*)(DdManager *, DdNode *), DdNode *f, DdNode *data);
1089 extern DdNode * cuddCacheLookup(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h);
1090 extern DdNode * cuddCacheLookupZdd(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h);
1091 extern DdNode * cuddCacheLookup2(DdManager *table, DdNode * (*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g);
1092 extern DdNode * cuddCacheLookup1(DdManager *table, DdNode * (*)(DdManager *, DdNode *), DdNode *f);
1093 extern DdNode * cuddCacheLookup2Zdd(DdManager *table, DdNode * (*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g);
1094 extern DdNode * cuddCacheLookup1Zdd(DdManager *table, DdNode * (*)(DdManager *, DdNode *), DdNode *f);
1095 extern DdNode * cuddConstantLookup(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h);
1096 extern int cuddCacheProfile(DdManager *table, FILE *fp);
1097 extern void cuddCacheResize(DdManager *table);
1098 extern void cuddCacheFlush(DdManager *table);
1099 extern int cuddComputeFloorLog2(unsigned int value);
1100 extern int cuddHeapProfile(DdManager *dd);
1101 extern void cuddPrintNode(DdNode *f, FILE *fp);
1102 extern void cuddPrintVarGroups(DdManager * dd, MtrNode * root, int zdd, int silent);
1103 extern DdNode * cuddBddClippingAnd(DdManager *dd, DdNode *f, DdNode *g, int maxDepth, int direction);
1104 extern DdNode * cuddBddClippingAndAbstract(DdManager *dd, DdNode *f, DdNode *g, DdNode *cube, int maxDepth, int direction);
1105 extern void cuddGetBranches(DdNode *g, DdNode **g1, DdNode **g0);
1106 extern DdNode * cuddCofactorRecur(DdManager *dd, DdNode *f, DdNode *g);
1107 extern DdNode * cuddBddComposeRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *proj);
1108 extern DdNode * cuddAddComposeRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *proj);
1109 extern int cuddExact(DdManager *table, int lower, int upper);
1110 extern DdNode * cuddBddConstrainRecur(DdManager *dd, DdNode *f, DdNode *c);
1111 extern DdNode * cuddBddRestrictRecur(DdManager *dd, DdNode *f, DdNode *c);
1112 extern DdNode * cuddBddNPAndRecur(DdManager *dd, DdNode *f, DdNode *c);
1113 extern DdNode * cuddAddConstrainRecur(DdManager *dd, DdNode *f, DdNode *c);
1114 extern DdNode * cuddAddRestrictRecur(DdManager *dd, DdNode *f, DdNode *c);
1115 extern DdNode * cuddBddLICompaction(DdManager *dd, DdNode *f, DdNode *c);
1116 extern int cuddGa(DdManager *table, int lower, int upper);
1117 extern int cuddTreeSifting(DdManager *table, Cudd_ReorderingType method);
1118 extern int cuddZddInitUniv(DdManager *zdd);
1119 extern void cuddZddFreeUniv(DdManager *zdd);
1120 extern void cuddSetInteract(DdManager *table, int x, int y);
1121 extern int cuddTestInteract(DdManager *table, int x, int y);
1122 extern int cuddInitInteract(DdManager *table);
1123 extern DdLocalCache * cuddLocalCacheInit(DdManager *manager, unsigned int keySize, unsigned int cacheSize, unsigned int maxCacheSize);
1124 extern void cuddLocalCacheQuit(DdLocalCache *cache);
1125 extern void cuddLocalCacheInsert(DdLocalCache *cache, DdNodePtr *key, DdNode *value);
1126 extern DdNode * cuddLocalCacheLookup(DdLocalCache *cache, DdNodePtr *key);
1127 extern void cuddLocalCacheClearDead(DdManager *manager);
1128 extern int cuddIsInDeathRow(DdManager *dd, DdNode *f);
1129 extern int cuddTimesInDeathRow(DdManager *dd, DdNode *f);
1130 extern void cuddLocalCacheClearAll(DdManager *manager);
1131 #ifdef DD_CACHE_PROFILE
1132 extern int cuddLocalCacheProfile(DdLocalCache *cache);
1133 #endif
1134 extern DdHashTable * cuddHashTableInit(DdManager *manager, unsigned int keySize, unsigned int initSize);
1135 extern void cuddHashTableQuit(DdHashTable *hash);
1136 extern void cuddHashTableGenericQuit(DdHashTable *hash);
1137 extern int cuddHashTableInsert(DdHashTable *hash, DdNodePtr *key, DdNode *value, ptrint count);
1138 extern DdNode * cuddHashTableLookup(DdHashTable *hash, DdNodePtr *key);
1139 extern int cuddHashTableInsert1(DdHashTable *hash, DdNode *f, DdNode *value, ptrint count);
1140 extern DdNode * cuddHashTableLookup1(DdHashTable *hash, DdNode *f);
1141 extern int cuddHashTableInsert2(DdHashTable *hash, DdNode *f, DdNode *g, DdNode *value, ptrint count);
1142 extern DdNode * cuddHashTableLookup2(DdHashTable *hash, DdNode *f, DdNode *g);
1143 extern int cuddHashTableInsert3(DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h, DdNode *value, ptrint count);
1144 extern DdNode * cuddHashTableLookup3(DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h);
1145 extern int cuddHashTableGenericInsert(DdHashTable * hash, DdNode * f, void * value);
1146 extern void * cuddHashTableGenericLookup(DdHashTable * hash, DdNode * f);
1147 extern DdLevelQueue * cuddLevelQueueInit(int levels, int itemSize, int numBuckets, DdManager * manager);
1148 extern void cuddLevelQueueQuit(DdLevelQueue *queue);
1149 extern void * cuddLevelQueueFirst(DdLevelQueue * queue, void * key, int level);
1150 extern void * cuddLevelQueueEnqueue(DdLevelQueue *queue, void *key, int level);
1151 extern void cuddLevelQueueDequeue(DdLevelQueue *queue, int level);
1152 extern int cuddLinearAndSifting(DdManager *table, int lower, int upper);
1153 extern int cuddLinearInPlace(DdManager * table, int x, int y);
1154 extern void cuddUpdateInteractionMatrix(DdManager * table, int xindex, int yindex);
1155 extern int cuddInitLinear(DdManager *table);
1156 extern int cuddResizeLinear(DdManager *table);
1158 extern DdNode * cuddCProjectionRecur(DdManager *dd, DdNode *R, DdNode *Y, DdNode *Ysupp);
1159 extern DdNode * cuddBddClosestCube(DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE bound);
1160 extern void cuddReclaim(DdManager *table, DdNode *n);
1161 extern void cuddReclaimZdd(DdManager *table, DdNode *n);
1162 extern void cuddClearDeathRow(DdManager *table);
1163 extern void cuddShrinkDeathRow(DdManager *table);
1164 extern DdNode * cuddDynamicAllocNode(DdManager *table);
1165 extern int cuddSifting(DdManager *table, int lower, int upper);
1166 extern int cuddSwapping(DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic);
1167 extern int cuddNextHigh(DdManager *table, int x);
1168 extern int cuddNextLow(DdManager *table, int x);
1169 extern int cuddSwapInPlace(DdManager *table, int x, int y);
1170 extern int cuddBddAlignToZdd(DdManager *table);
1171 extern DdNode * cuddBddMakePrime(DdManager *dd, DdNode *cube, DdNode *f);
1172 extern DdNode * cuddSolveEqnRecur(DdManager *bdd, DdNode *F, DdNode *Y, DdNode **G, int n, int *yIndex, int i);
1173 extern DdNode * cuddVerifySol(DdManager *bdd, DdNode *F, DdNode **G, int *yIndex, int n);
1174 #ifdef ST_H_
1175 extern DdNode* cuddSplitSetRecur(DdManager *manager, st_table *mtable, int *varSeen, DdNode *p, double n, double max, int index);
1176 #endif
1177 extern DdNode * cuddSubsetHeavyBranch(DdManager *dd, DdNode *f, int numVars, int threshold);
1178 extern DdNode * cuddSubsetShortPaths(DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit);
1179 extern int cuddSymmCheck(DdManager *table, int x, int y);
1180 extern int cuddSymmSifting(DdManager *table, int lower, int upper);
1181 extern int cuddSymmSiftingConv(DdManager *table, int lower, int upper);
1182 extern DdNode * cuddAllocNode(DdManager *unique);
1183 extern DdManager * cuddInitTable(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int looseUpTo);
1184 extern void cuddFreeTable(DdManager *unique);
1185 extern int cuddGarbageCollect(DdManager *unique, int clearCache);
1186 extern DdNode * cuddZddGetNode(DdManager *zdd, int id, DdNode *T, DdNode *E);
1187 extern DdNode * cuddZddGetNodeIVO(DdManager *dd, int index, DdNode *g, DdNode *h);
1188 extern DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E);
1189 extern DdNode * cuddUniqueInterIVO(DdManager *unique, int index, DdNode *T, DdNode *E);
1190 extern DdNode * cuddUniqueInterZdd(DdManager *unique, int index, DdNode *T, DdNode *E);
1191 extern DdNode * cuddUniqueConst(DdManager *unique, CUDD_VALUE_TYPE value);
1192 extern void cuddRehash(DdManager *unique, int i);
1193 extern void cuddShrinkSubtable(DdManager *unique, int i);
1194 extern int cuddInsertSubtables(DdManager *unique, int n, int level);
1195 extern int cuddDestroySubtables(DdManager *unique, int n);
1196 extern int cuddResizeTableZdd(DdManager *unique, int index);
1197 extern void cuddSlowTableGrowth(DdManager *unique);
1198 extern int cuddP(DdManager *dd, DdNode *f);
1199 #ifdef ST_H_
1200 extern enum st_retval cuddStCountfree(void *key, void *value, void *arg);
1201 extern int cuddCollectNodes(DdNode *f, st_table *visited);
1202 #endif
1203 extern DdNodePtr * cuddNodeArray(DdNode *f, int *n);
1204 extern int cuddWindowReorder(DdManager *table, int low, int high, Cudd_ReorderingType submethod);
1205 extern DdNode * cuddZddProduct(DdManager *dd, DdNode *f, DdNode *g);
1206 extern DdNode * cuddZddUnateProduct(DdManager *dd, DdNode *f, DdNode *g);
1207 extern DdNode * cuddZddWeakDiv(DdManager *dd, DdNode *f, DdNode *g);
1208 extern DdNode * cuddZddWeakDivF(DdManager *dd, DdNode *f, DdNode *g);
1209 extern DdNode * cuddZddDivide(DdManager *dd, DdNode *f, DdNode *g);
1210 extern DdNode * cuddZddDivideF(DdManager *dd, DdNode *f, DdNode *g);
1211 extern int cuddZddGetCofactors3(DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0, DdNode **fd);
1212 extern int cuddZddGetCofactors2(DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0);
1213 extern DdNode * cuddZddComplement(DdManager *dd, DdNode *node);
1214 extern int cuddZddGetPosVarIndex(DdManager * dd, int index);
1215 extern int cuddZddGetNegVarIndex(DdManager * dd, int index);
1216 extern int cuddZddGetPosVarLevel(DdManager * dd, int index);
1217 extern int cuddZddGetNegVarLevel(DdManager * dd, int index);
1218 extern int cuddZddTreeSifting(DdManager *table, Cudd_ReorderingType method);
1219 extern DdNode * cuddZddIsop(DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I);
1220 extern DdNode * cuddBddIsop(DdManager *dd, DdNode *L, DdNode *U);
1221 extern DdNode * cuddMakeBddFromZddCover(DdManager *dd, DdNode *node);
1222 extern int cuddZddLinearSifting(DdManager *table, int lower, int upper);
1223 extern int cuddZddAlignToBdd(DdManager *table);
1224 extern int cuddZddNextHigh(DdManager *table, int x);
1225 extern int cuddZddNextLow(DdManager *table, int x);
1226 extern int cuddZddUniqueCompare(void const *ptr_x, void const *ptr_y);
1227 extern int cuddZddSwapInPlace(DdManager *table, int x, int y);
1228 extern int cuddZddSwapping(DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic);
1229 extern int cuddZddSifting(DdManager *table, int lower, int upper);
1230 extern DdNode * cuddZddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
1231 extern DdNode * cuddZddUnion(DdManager *zdd, DdNode *P, DdNode *Q);
1232 extern DdNode * cuddZddIntersect(DdManager *zdd, DdNode *P, DdNode *Q);
1233 extern DdNode * cuddZddDiff(DdManager *zdd, DdNode *P, DdNode *Q);
1234 extern DdNode * cuddZddChangeAux(DdManager *zdd, DdNode *P, DdNode *zvar);
1235 extern DdNode * cuddZddSubset1(DdManager *dd, DdNode *P, int var);
1236 extern DdNode * cuddZddSubset0(DdManager *dd, DdNode *P, int var);
1237 extern DdNode * cuddZddChange(DdManager *dd, DdNode *P, int var);
1238 extern int cuddZddSymmCheck(DdManager *table, int x, int y);
1239 extern int cuddZddSymmSifting(DdManager *table, int lower, int upper);
1240 extern int cuddZddSymmSiftingConv(DdManager *table, int lower, int upper);
1241 extern int cuddZddP(DdManager *zdd, DdNode *f);
1242 
1243 #ifdef __cplusplus
1244 } /* end of extern "C" */
1245 #endif
1246 
1249 #endif /* CUDD_INT_H_ */
DdChildren
The two children of a non-terminal node.
Definition: cuddInt.h:249
DdManager::deathRow
DdNode ** deathRow
Definition: cuddInt.h:454
DdManager
Specialized DD symbol table.
Definition: cuddInt.h:395
DdLocalCache
Local cache.
Definition: cuddInt.h:321
cuddHashTableInsert1
int cuddHashTableInsert1(DdHashTable *hash, DdNode *f, DdNode *value, ptrint count)
Inserts an item in a hash table.
Definition: cuddLCache.c:737
cuddReclaim
void cuddReclaim(DdManager *table, DdNode *n)
Brings children of a dead node back.
Definition: cuddRef.c:540
DdNode::ref
DdHalfWord ref
Definition: cuddInt.h:259
cuddAddIteRecur
DdNode * cuddAddIteRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Implements the recursive step of Cudd_addIte(f,g,h).
Definition: cuddAddIte.c:423
cuddSymmSiftingConv
int cuddSymmSiftingConv(DdManager *table, int lower, int upper)
Symmetric sifting to convergence algorithm.
Definition: cuddSymmetry.c:401
DdManager::tohArg
void * tohArg
Definition: cuddInt.h:504
cuddCProjectionRecur
DdNode * cuddCProjectionRecur(DdManager *dd, DdNode *R, DdNode *Y, DdNode *Ysupp)
Performs the recursive step of Cudd_CProjection.
Definition: cuddPriority.c:1386
cuddSetInteract
void cuddSetInteract(DdManager *table, int x, int y)
Set interaction matrix entries.
Definition: cuddInteract.c:133
cuddZddTreeSifting
int cuddZddTreeSifting(DdManager *table, Cudd_ReorderingType method)
Tree sifting algorithm for ZDDs.
Definition: cuddZddGroup.c:187
DdHook
CUDD hook.
Definition: cuddInt.h:302
DdManager::looseUpTo
unsigned int looseUpTo
Definition: cuddInt.h:430
DdManager::cacheMisses
double cacheMisses
Definition: cuddInt.h:408
cuddAnnealing
int cuddAnnealing(DdManager *table, int lower, int upper)
Get new variable-order by simulated annealing algorithm.
Definition: cuddAnneal.c:119
Move
Reordering move record.
Definition: cuddInt.h:563
cuddHashTableInsert2
int cuddHashTableInsert2(DdHashTable *hash, DdNode *f, DdNode *g, DdNode *value, ptrint count)
Inserts an item in a hash table.
Definition: cuddLCache.c:933
DdNode::kids
DdChildren kids
Definition: cuddInt.h:263
DdManager::autoMethodZ
Cudd_ReorderingType autoMethodZ
Definition: cuddInt.h:475
cuddBddClippingAndAbstract
DdNode * cuddBddClippingAndAbstract(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:206
DdManager::postGCHook
DdHook * postGCHook
Definition: cuddInt.h:492
DdSubtable::shift
int shift
Definition: cuddInt.h:378
cuddBddComposeRecur
DdNode * cuddBddComposeRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *proj)
Performs the recursive step of Cudd_bddCompose.
Definition: cuddCompose.c:825
cuddClearDeathRow
void cuddClearDeathRow(DdManager *table)
Clears the death row.
Definition: cuddRef.c:675
DdManager::reordered
int reordered
Definition: cuddInt.h:462
DdNode::type
union DdNode::@0 type
cuddP
int cuddP(DdManager *dd, DdNode *f)
Prints a DD to the standard output. One line per node is printed.
Definition: cuddUtil.c:2944
cuddZddP
int cuddZddP(DdManager *zdd, DdNode *f)
Prints a ZDD to the standard output. One line per node is printed.
Definition: cuddZddUtil.c:852
cuddHashTableLookup3
DdNode * cuddHashTableLookup3(DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h)
Looks up a key consisting of three pointers in a hash table.
Definition: cuddLCache.c:1100
DdManager::plusinfinity
DdNode * plusinfinity
Definition: cuddInt.h:400
DdManager::cacheSlots
unsigned int cacheSlots
Definition: cuddInt.h:406
cuddBddClosestCube
DdNode * cuddBddClosestCube(DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE bound)
Performs the recursive step of Cudd_bddClosestCube.
Definition: cuddPriority.c:1612
cuddCacheInsert1
void cuddCacheInsert1(DdManager *table, DD_CTFP1 op, DdNode *f, DdNode *data)
Inserts a result in the cache for a function with two operands.
Definition: cuddCache.c:272
DdSubtable::keys
unsigned int keys
Definition: cuddInt.h:380
Cudd_VariableType
Cudd_VariableType
Variable type.
Definition: cudd.h:180
DdManager::postReorderingHook
DdHook * postReorderingHook
Definition: cuddInt.h:494
DdManager::keys
unsigned int keys
Definition: cuddInt.h:422
cuddBddExistAbstractRecur
DdNode * cuddBddExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube)
Performs the recursive steps of Cudd_bddExistAbstract.
Definition: cuddBddAbs.c:372
DdHashItem::next
struct DdHashItem * next
Definition: cuddInt.h:339
cuddHashTableLookup1
DdNode * cuddHashTableLookup1(DdHashTable *hash, DdNode *f)
Looks up a key consisting of one pointer in a hash table.
Definition: cuddLCache.c:789
cuddLocalCacheLookup
DdNode * cuddLocalCacheLookup(DdLocalCache *cache, DdNodePtr *key)
Looks up in a local cache.
Definition: cuddLCache.c:265
cuddZddSymmCheck
int cuddZddSymmCheck(DdManager *table, int x, int y)
Checks for symmetry of x and y.
Definition: cuddZddSymm.c:153
DdManager::totCachehits
double totCachehits
Definition: cuddInt.h:512
DdManager::garbageCollections
int garbageCollections
Definition: cuddInt.h:509
DdManager::constants
DdSubtable constants
Definition: cuddInt.h:420
cuddHashTableInsert3
int cuddHashTableInsert3(DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h, DdNode *value, ptrint count)
Inserts an item in a hash table.
Definition: cuddLCache.c:1044
DdHashTable::keysize
unsigned int keysize
Definition: cuddInt.h:349
cuddZddIsop
DdNode * cuddZddIsop(DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I)
Performs the recursive step of Cudd_zddIsop.
Definition: cuddZddIsop.c:214
DdManager::maxmemhard
size_t maxmemhard
Definition: cuddInt.h:508
cuddZddGetNodeIVO
DdNode * cuddZddGetNodeIVO(DdManager *dd, int index, DdNode *g, DdNode *h)
Wrapper for cuddUniqueInterZdd that is independent of variable ordering.
Definition: cuddTable.c:1063
DdManager::minusinfinity
DdNode * minusinfinity
Definition: cuddInt.h:401
cuddBddAndAbstractRecur
DdNode * cuddBddAndAbstractRecur(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
Takes the AND of two BDDs and simultaneously abstracts the variables in cube.
Definition: cuddAndAbs.c:184
DdManager::minHit
double minHit
Definition: cuddInt.h:410
DdManager::gcFrac
double gcFrac
Definition: cuddInt.h:429
DdManager::zero
DdNode * zero
Definition: cuddInt.h:399
DdManager::shuffleSelect
int32_t shuffleSelect
Definition: cuddInt.h:522
cuddCacheFlush
void cuddCacheFlush(DdManager *table)
Flushes the cache.
Definition: cuddCache.c:945
cuddAddComposeRecur
DdNode * cuddAddComposeRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *proj)
Performs the recursive step of Cudd_addCompose.
Definition: cuddCompose.c:928
DdHashTable::numBuckets
unsigned int numBuckets
Definition: cuddInt.h:354
DdCache::g
DdNode * g
Definition: cuddInt.h:365
cuddLevelQueueDequeue
void cuddLevelQueueDequeue(DdLevelQueue *queue, int level)
Remove an item from the front of a level queue.
Definition: cuddLevelQ.c:355
cuddBddXorExistAbstractRecur
DdNode * cuddBddXorExistAbstractRecur(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:483
cuddResizeLinear
int cuddResizeLinear(DdManager *table)
Resizes the linear transform matrix.
Definition: cuddLinear.c:740
DdHashTable::memoryList
DdHashItem ** memoryList
Definition: cuddInt.h:353
cuddZddSwapping
int cuddZddSwapping(DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic)
Reorders variables by a sequence of (non-adjacent) swaps.
Definition: cuddZddReord.c:687
cuddSlowTableGrowth
void cuddSlowTableGrowth(DdManager *unique)
Adjusts parameters of a table to slow down its growth.
Definition: cuddTable.c:2451
DdManager::arcviolation
int arcviolation
Definition: cuddInt.h:485
cuddInitTable
DdManager * cuddInitTable(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int looseUpTo)
Creates and initializes the unique table.
Definition: cuddTable.c:342
cuddComputeFloorLog2
int cuddComputeFloorLog2(unsigned int value)
Returns the floor of the logarithm to the base 2.
Definition: cuddCache.c:973
DdManager::timeLimit
unsigned long timeLimit
Definition: cuddInt.h:499
cuddInitLinear
int cuddInitLinear(DdManager *table)
Initializes the linear transform matrix.
Definition: cuddLinear.c:699
DdManager::minDead
unsigned int minDead
Definition: cuddInt.h:427
st_retval
st_retval
Type of return values for iterators.
Definition: st.h:130
cuddZddChange
DdNode * cuddZddChange(DdManager *dd, DdNode *P, int var)
Substitutes a variable with its complement in a ZDD.
Definition: cuddZddSetop.c:896
DdHashTable::itemsize
unsigned int itemsize
Definition: cuddInt.h:350
cuddRehash
void cuddRehash(DdManager *unique, int i)
Rehashes a unique subtable.
Definition: cuddTable.c:1595
DdManager::size
int size
Definition: cuddInt.h:414
DdManager::symmviolation
int symmviolation
Definition: cuddInt.h:484
DdManager::invperm
int * invperm
Definition: cuddInt.h:439
DdManager::err
FILE * err
Definition: cuddInt.h:496
DdManager::maxCacheHard
unsigned int maxCacheHard
Definition: cuddInt.h:412
DdHashTable::bucket
DdHashItem ** bucket
Definition: cuddInt.h:351
DdManager::localCaches
DdLocalCache * localCaches
Definition: cuddInt.h:489
Cudd_LazyGroupType
Cudd_LazyGroupType
Group type for lazy sifting.
Definition: cudd.h:166
cuddInsertSubtables
int cuddInsertSubtables(DdManager *unique, int n, int level)
Inserts n new subtables in a unique table at level.
Definition: cuddTable.c:1857
cuddBddMakePrime
DdNode * cuddBddMakePrime(DdManager *dd, DdNode *cube, DdNode *f)
Performs the recursive step of Cudd_bddMakePrime.
Definition: cuddSat.c:963
DdLevelQueue
Level queue.
Definition: cuddInt.h:591
cuddZddWeakDivF
DdNode * cuddZddWeakDivF(DdManager *dd, DdNode *f, DdNode *g)
Performs the recursive step of Cudd_zddWeakDivF.
Definition: cuddZddFuncs.c:879
DdGen
CUDD generator.
Definition: cuddInt.h:270
cuddAllocNode
DdNode * cuddAllocNode(DdManager *unique)
Fast storage allocation for DdNodes in the table.
Definition: cuddTable.c:225
MtrNode_
multi-way tree node.
Definition: mtrInt.h:109
cuddAddOrAbstractRecur
DdNode * cuddAddOrAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube)
Performs the recursive step of Cudd_addOrAbstract.
Definition: cuddAddAbs.c:432
cuddInitInteract
int cuddInitInteract(DdManager *table)
Initializes the interaction matrix.
Definition: cuddInteract.c:210
cuddZddGetPosVarLevel
int cuddZddGetPosVarLevel(DdManager *dd, int index)
Returns the level of positive ZDD variable.
Definition: cuddZddFuncs.c:1530
cuddCacheLookup
DdNode * cuddCacheLookup(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h)
Looks up in the cache for the result of op applied to f, g, and h.
Definition: cuddCache.c:312
DdManager::reordCycle
int reordCycle
Definition: cuddInt.h:469
DdManager::preGCHook
DdHook * preGCHook
Definition: cuddInt.h:491
cuddZddGetCofactors3
int cuddZddGetCofactors3(DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0, DdNode **fd)
Computes the three-way decomposition of f w.r.t. v.
Definition: cuddZddFuncs.c:1313
cuddLocalCacheInsert
void cuddLocalCacheInsert(DdLocalCache *cache, DdNodePtr *key, DdNode *value)
Inserts a result in a local cache.
Definition: cuddLCache.c:236
DdManager::perm
int * perm
Definition: cuddInt.h:437
cuddLocalCacheClearDead
void cuddLocalCacheClearDead(DdManager *manager)
Clears the dead entries of the local caches of a manager.
Definition: cuddLCache.c:308
ptrint
intptr_t ptrint
Signed integer that is the size of a pointer.
Definition: cuddInt.h:220
cuddRemapUnderApprox
DdNode * cuddRemapUnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
Applies the remapping underappoximation algorithm.
Definition: cuddApprox.c:582
st.h
Symbol table package.
cuddIsInDeathRow
int cuddIsInDeathRow(DdManager *dd, DdNode *f)
Checks whether a node is in the death row.
Definition: cuddRef.c:709
DdManager::linearSize
int linearSize
Definition: cuddInt.h:446
cuddZddComplement
DdNode * cuddZddComplement(DdManager *dd, DdNode *node)
Computes a complement of a ZDD node.
Definition: cuddZddFuncs.c:1467
cuddAddExistAbstractRecur
DdNode * cuddAddExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube)
Performs the recursive step of Cudd_addExistAbstract.
Definition: cuddAddAbs.c:223
DdNode
Decision diagram node.
Definition: cuddInt.h:257
DdManager::maxReorderings
unsigned int maxReorderings
Definition: cuddInt.h:464
DdManager::cuddRand2
int32_t cuddRand2
Definition: cuddInt.h:521
cuddZddAlignToBdd
int cuddZddAlignToBdd(DdManager *table)
Reorders ZDD variables according to the order of the BDD variables.
Definition: cuddZddReord.c:304
cuddSplitSetRecur
DdNode * cuddSplitSetRecur(DdManager *manager, st_table *mtable, int *varSeen, DdNode *p, double n, double max, int index)
Implements the recursive step of Cudd_SplitSet.
Definition: cuddSplit.c:224
DdManager::stash
char * stash
Definition: cuddInt.h:452
DdManager::maxGrowth
double maxGrowth
Definition: cuddInt.h:470
DdManager::subtableZ
DdSubtable * subtableZ
Definition: cuddInt.h:419
cuddZddGetNode
DdNode * cuddZddGetNode(DdManager *zdd, int id, DdNode *T, DdNode *E)
Wrapper for cuddUniqueInterZdd.
Definition: cuddTable.c:1029
DdManager::autoMethod
Cudd_ReorderingType autoMethod
Definition: cuddInt.h:474
Cudd_ErrorType
Cudd_ErrorType
Type of error codes.
Definition: cudd.h:151
DdSubtable::bindVar
int bindVar
Definition: cuddInt.h:384
mtr.h
Multiway-branch tree manipulation.
cuddZddIte
DdNode * cuddZddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Performs the recursive step of Cudd_zddIte.
Definition: cuddZddSetop.c:376
cuddAddUnivAbstractRecur
DdNode * cuddAddUnivAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube)
Performs the recursive step of Cudd_addUnivAbstract.
Definition: cuddAddAbs.c:326
DdManager::deathRowDepth
int deathRowDepth
Definition: cuddInt.h:455
DdManager::nextFree
DdNode * nextFree
Definition: cuddInt.h:451
Cudd_AggregationType
Cudd_AggregationType
Type of aggregation methods.
Definition: cudd.h:123
cuddSifting
int cuddSifting(DdManager *table, int lower, int upper)
Implementation of Rudell's sifting algorithm.
Definition: cuddReorder.c:457
cuddZddDiff
DdNode * cuddZddDiff(DdManager *zdd, DdNode *P, DdNode *Q)
Performs the recursive step of Cudd_zddDiff.
Definition: cuddZddSetop.c:651
DdSubtable::varToBeGrouped
Cudd_LazyGroupType varToBeGrouped
Definition: cuddInt.h:389
DdHashItem::count
ptrint count
Definition: cuddInt.h:340
DdManager::tcbArg
void * tcbArg
Definition: cuddInt.h:501
cuddLevelQueueInit
DdLevelQueue * cuddLevelQueueInit(int levels, int itemSize, int numBuckets, DdManager *manager)
Initializes a level queue.
Definition: cuddLevelQ.c:143
DdManager::hooks
void * hooks
Definition: cuddInt.h:490
DdManager::groupcheck
Cudd_AggregationType groupcheck
Definition: cuddInt.h:482
DdManager::sizeZ
int sizeZ
Definition: cuddInt.h:415
cuddUniqueInterZdd
DdNode * cuddUniqueInterZdd(DdManager *unique, int index, DdNode *T, DdNode *E)
Checks the unique table for the existence of an internal ZDD node.
Definition: cuddTable.c:1374
DD_THFP
int(* DD_THFP)(const void *)
Type of termination handler.
Definition: cudd.h:266
DdManager::vars
DdNode ** vars
Definition: cuddInt.h:441
DdManager::preReorderingHook
DdHook * preReorderingHook
Definition: cuddInt.h:493
DdManager::startTime
unsigned long startTime
Definition: cuddInt.h:498
ptruint
uintptr_t ptruint
Unsigned integer that is the size of a pointer.
Definition: cuddInt.h:227
cuddInitCache
int cuddInitCache(DdManager *unique, unsigned int cacheSize, unsigned int maxCacheSize)
Initializes the computed table.
Definition: cuddCache.c:107
cuddBddIntersectRecur
DdNode * cuddBddIntersectRecur(DdManager *dd, DdNode *f, DdNode *g)
Implements the recursive step of Cudd_bddIntersect.
Definition: cuddBddIte.c:853
cuddWindowReorder
int cuddWindowReorder(DdManager *table, int low, int high, Cudd_ReorderingType submethod)
Reorders by applying the method of the sliding window.
Definition: cuddWindow.c:109
cuddLevelQueueQuit
void cuddLevelQueueQuit(DdLevelQueue *queue)
Shuts down a level queue.
Definition: cuddLevelQ.c:197
DdHook::f
DD_HFP f
Definition: cuddInt.h:303
DdHook::next
struct DdHook * next
Definition: cuddInt.h:304
DdManager::subtables
DdSubtable * subtables
Definition: cuddInt.h:418
DdManager::initSlots
unsigned int initSlots
Definition: cuddInt.h:432
DdManager::recomb
int recomb
Definition: cuddInt.h:483
DdManager::cacheLastInserts
double cacheLastInserts
Definition: cuddInt.h:516
DdNode::next
DdNode * next
Definition: cuddInt.h:260
cuddNodeArray
DdNodePtr * cuddNodeArray(DdNode *f, int *n)
Recursively collects all the nodes of a DD in an array.
Definition: cuddUtil.c:3055
DdManager::nextDyn
unsigned int nextDyn
Definition: cuddInt.h:478
cuddSubsetShortPaths
DdNode * cuddSubsetShortPaths(DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit)
The outermost procedure to return a subset of the given BDD with the shortest path lengths.
Definition: cuddSubsetSP.c:274
cuddBddLiteralSetIntersectionRecur
DdNode * cuddBddLiteralSetIntersectionRecur(DdManager *dd, DdNode *f, DdNode *g)
Performs the recursive step of Cudd_bddLiteralSetIntersection.
Definition: cuddLiteral.c:138
cuddZddDivide
DdNode * cuddZddDivide(DdManager *dd, DdNode *f, DdNode *g)
Performs the recursive step of Cudd_zddDivide.
Definition: cuddZddFuncs.c:1114
DdManager::cacheShift
int cacheShift
Definition: cuddInt.h:407
cuddBddIteRecur
DdNode * cuddBddIteRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Implements the recursive step of Cudd_bddIte.
Definition: cuddBddIte.c:716
DdManager::allocated
double allocated
Definition: cuddInt.h:434
DdManager::cache
DdCache * cache
Definition: cuddInt.h:405
cuddCacheResize
void cuddCacheResize(DdManager *table)
Resizes the cache.
Definition: cuddCache.c:835
cuddUpdateInteractionMatrix
void cuddUpdateInteractionMatrix(DdManager *table, int xindex, int yindex)
Updates the interaction matrix.
Definition: cuddLinear.c:662
cuddAddConstrainRecur
DdNode * cuddAddConstrainRecur(DdManager *dd, DdNode *f, DdNode *c)
Performs the recursive step of Cudd_addConstrain.
Definition: cuddGenCof.c:1212
DdManager::stack
DdNode ** stack
Definition: cuddInt.h:433
DdSubtable::varHandled
int varHandled
Definition: cuddInt.h:388
DdManager::zddTotalNumberSwapping
int zddTotalNumberSwapping
Definition: cuddInt.h:468
DdManager::maxLive
unsigned int maxLive
Definition: cuddInt.h:426
cuddCacheLookup1Zdd
DdNode * cuddCacheLookup1Zdd(DdManager *table, DD_CTFP1 op, DdNode *f)
Looks up in the cache for the result of op applied to f.
Definition: cuddCache.c:588
cuddZddUnateProduct
DdNode * cuddZddUnateProduct(DdManager *dd, DdNode *f, DdNode *g)
Performs the recursive step of Cudd_zddUnateProduct.
Definition: cuddZddFuncs.c:579
DdManager::originalSize
unsigned int originalSize
Definition: cuddInt.h:445
DdSubtable::dead
unsigned int dead
Definition: cuddInt.h:382
cuddSolveEqnRecur
DdNode * cuddSolveEqnRecur(DdManager *bdd, DdNode *F, DdNode *Y, DdNode **G, int n, int *yIndex, int i)
Implements the recursive step of Cudd_SolveEqn.
Definition: cuddSolve.c:189
DdManager::cuddRand
int32_t cuddRand
Definition: cuddInt.h:520
DdManager::invpermZ
int * invpermZ
Definition: cuddInt.h:440
cuddZddUnion
DdNode * cuddZddUnion(DdManager *zdd, DdNode *P, DdNode *Q)
Performs the recursive step of Cudd_zddUnion.
Definition: cuddZddSetop.c:497
DdManager::ddTotalNumberSwapping
int ddTotalNumberSwapping
Definition: cuddInt.h:467
cuddTestInteract
int cuddTestInteract(DdManager *table, int x, int y)
Test interaction matrix entries.
Definition: cuddInteract.c:165
DdManager::populationSize
int populationSize
Definition: cuddInt.h:486
cuddZddSubset1
DdNode * cuddZddSubset1(DdManager *dd, DdNode *P, int var)
Computes the positive cofactor of a ZDD w.r.t. a variable.
Definition: cuddZddSetop.c:802
cuddZddProduct
DdNode * cuddZddProduct(DdManager *dd, DdNode *f, DdNode *g)
Performs the recursive step of Cudd_zddProduct.
Definition: cuddZddFuncs.c:344
DdManager::isolated
unsigned int isolated
Definition: cuddInt.h:444
cuddAddMonadicApplyRecur
DdNode * cuddAddMonadicApplyRecur(DdManager *dd, DD_MAOP op, DdNode *f)
Performs the recursive step of Cudd_addMonadicApply.
Definition: cuddAddApply.c:837
cuddPrintVarGroups
void cuddPrintVarGroups(DdManager *dd, MtrNode *root, int zdd, int silent)
Prints the variable groups as a parenthesized list.
Definition: cuddCheck.c:700
DdManager::epsilon
CUDD_VALUE_TYPE epsilon
Definition: cuddInt.h:460
cuddZddSymmSifting
int cuddZddSymmSifting(DdManager *table, int lower, int upper)
Symmetric sifting algorithm for ZDDs.
Definition: cuddZddSymm.c:256
DdManager::acache
DdCache * acache
Definition: cuddInt.h:404
cuddZddNextHigh
int cuddZddNextHigh(DdManager *table, int x)
Finds the next subtable with a larger index.
Definition: cuddZddReord.c:360
cuddExact
int cuddExact(DdManager *table, int lower, int upper)
Exact variable ordering algorithm.
Definition: cuddExact.c:114
DdManager::memoryList
DdNode ** memoryList
Definition: cuddInt.h:450
cuddBddIsop
DdNode * cuddBddIsop(DdManager *dd, DdNode *L, DdNode *U)
Performs the recursive step of Cudd_bddIsop.
Definition: cuddZddIsop.c:552
DdManager::slots
unsigned int slots
Definition: cuddInt.h:421
DdSubtable::varType
Cudd_VariableType varType
Definition: cuddInt.h:386
DdLocalCacheItem
Generic local cache item.
Definition: cuddInt.h:310
cuddCollectNodes
int cuddCollectNodes(DdNode *f, st_table *visited)
Recursively collects all the nodes of a DD in a symbol table.
Definition: cuddUtil.c:3000
DdNode::index
DdHalfWord index
Definition: cuddInt.h:258
cuddZddLinearSifting
int cuddZddLinearSifting(DdManager *table, int lower, int upper)
Implementation of the linear sifting algorithm for ZDDs.
Definition: cuddZddLin.c:125
cuddTreeSifting
int cuddTreeSifting(DdManager *table, Cudd_ReorderingType method)
Tree sifting algorithm.
Definition: cuddGroup.c:205
DdManager::dead
unsigned int dead
Definition: cuddInt.h:424
cuddReclaimZdd
void cuddReclaimZdd(DdManager *table, DdNode *n)
Brings children of a dead ZDD node back.
Definition: cuddRef.c:591
DdHalfWord
uint32_t DdHalfWord
Type that is half the size of a pointer.
Definition: cuddInt.h:205
DdManager::cachecollisions
double cachecollisions
Definition: cuddInt.h:514
cuddAddApplyRecur
DdNode * cuddAddApplyRecur(DdManager *dd, DD_AOP op, DdNode *f, DdNode *g)
Performs the recursive step of Cudd_addApply.
Definition: cuddAddApply.c:753
DdSubtable::maxKeys
unsigned int maxKeys
Definition: cuddInt.h:381
cuddBiasedUnderApprox
DdNode * cuddBiasedUnderApprox(DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
Applies the biased remapping underappoximation algorithm.
Definition: cuddApprox.c:671
DdManager::numberXovers
int numberXovers
Definition: cuddInt.h:487
DdHashTable::nextFree
DdHashItem * nextFree
Definition: cuddInt.h:352
cuddResizeTableZdd
int cuddResizeTableZdd(DdManager *unique, int index)
Increases the number of ZDD subtables in a unique table so that it meets or exceeds index.
Definition: cuddTable.c:2309
cuddAddRestrictRecur
DdNode * cuddAddRestrictRecur(DdManager *dd, DdNode *f, DdNode *c)
Performs the recursive step of Cudd_addRestrict.
Definition: cuddGenCof.c:1316
cuddShrinkDeathRow
void cuddShrinkDeathRow(DdManager *table)
Shrinks the death row.
Definition: cuddRef.c:640
cuddLocalCacheInit
DdLocalCache * cuddLocalCacheInit(DdManager *manager, unsigned int keySize, unsigned int cacheSize, unsigned int maxCacheSize)
Initializes a local computed table.
Definition: cuddLCache.c:157
DdHashTable::manager
DdManager * manager
Definition: cuddInt.h:358
cuddLinearAndSifting
int cuddLinearAndSifting(DdManager *table, int lower, int upper)
BDD reduction based on combination of sifting and linear transformations.
Definition: cuddLinear.c:193
DdHashTable::size
unsigned int size
Definition: cuddInt.h:356
DdChildren::E
struct DdNode * E
Definition: cuddInt.h:251
DdCache::h
ptruint h
Definition: cuddInt.h:366
cuddLinearInPlace
int cuddLinearInPlace(DdManager *table, int x, int y)
Linearly combines two adjacent variables.
Definition: cuddLinear.c:308
DdSubtable
Subtable for one index.
Definition: cuddInt.h:376
cuddAddBddDoPattern
DdNode * cuddAddBddDoPattern(DdManager *dd, DdNode *f)
Performs the recursive step for Cudd_addBddPattern.
Definition: cuddBridge.c:462
cuddSymmSifting
int cuddSymmSifting(DdManager *table, int lower, int upper)
Symmetric sifting algorithm.
Definition: cuddSymmetry.c:284
cuddZddGetCofactors2
int cuddZddGetCofactors2(DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0)
Computes the two-way decomposition of f w.r.t. v.
Definition: cuddZddFuncs.c:1437
cuddVerifySol
DdNode * cuddVerifySol(DdManager *bdd, DdNode *F, DdNode **G, int *yIndex, int n)
Implements the recursive step of Cudd_VerifySol.
Definition: cuddSolve.c:312
cuddBddNPAndRecur
DdNode * cuddBddNPAndRecur(DdManager *manager, DdNode *f, DdNode *g)
Implements the recursive step of Cudd_bddAnd.
Definition: cuddGenCof.c:1070
cuddGetBranches
void cuddGetBranches(DdNode *g, DdNode **g1, DdNode **g0)
Computes the children of g.
Definition: cuddCof.c:225
cuddZddInitUniv
int cuddZddInitUniv(DdManager *zdd)
Initializes the ZDD universe.
Definition: cuddInit.c:221
DdCache::data
DdNode * data
Definition: cuddInt.h:367
DdManager::cachedeletions
double cachedeletions
Definition: cuddInt.h:517
DdManager::terminationCallback
DD_THFP terminationCallback
Definition: cuddInt.h:500
DdHashTable::maxsize
unsigned int maxsize
Definition: cuddInt.h:357
cuddBddTransfer
DdNode * cuddBddTransfer(DdManager *ddS, DdManager *ddD, DdNode *f)
Convert a BDD from a manager to another one.
Definition: cuddBridge.c:415
cuddAddCmplRecur
DdNode * cuddAddCmplRecur(DdManager *dd, DdNode *f)
Performs the recursive step of Cudd_addCmpl.
Definition: cuddAddIte.c:541
cuddCacheInsert2
void cuddCacheInsert2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g, DdNode *data)
Inserts a result in the cache for a function with two operands.
Definition: cuddCache.c:233
DdManager::cacheinserts
double cacheinserts
Definition: cuddInt.h:515
cuddHashTableGenericLookup
void * cuddHashTableGenericLookup(DdHashTable *hash, DdNode *f)
Looks up a key consisting of one pointer in a hash table.
Definition: cuddLCache.c:893
cuddZddGetNegVarLevel
int cuddZddGetNegVarLevel(DdManager *dd, int index)
Returns the level of negative ZDD variable.
Definition: cuddZddFuncs.c:1543
DdSubtable::nodelist
DdNode ** nodelist
Definition: cuddInt.h:377
DdManager::timeoutHandler
DD_TOHFP timeoutHandler
Definition: cuddInt.h:503
cuddBddClippingAnd
DdNode * cuddBddClippingAnd(DdManager *dd, DdNode *f, DdNode *g, int maxDepth, int direction)
Approximates the conjunction of two BDDs f and g.
Definition: cuddClip.c:177
cuddLocalCacheClearAll
void cuddLocalCacheClearAll(DdManager *manager)
Clears the local caches of a manager.
Definition: cuddLCache.c:356
cuddHashTableLookup
DdNode * cuddHashTableLookup(DdHashTable *hash, DdNodePtr *key)
Looks up a key in a hash table.
Definition: cuddLCache.c:673
DdManager::linear
ptruint * linear
Definition: cuddInt.h:448
cuddZddSifting
int cuddZddSifting(DdManager *table, int lower, int upper)
Implementation of Rudell's sifting algorithm.
Definition: cuddZddReord.c:805
DdManager::countDead
unsigned int countDead
Definition: cuddInt.h:479
cuddAddRoundOffRecur
DdNode * cuddAddRoundOffRecur(DdManager *dd, DdNode *f, double trunc)
Implements the recursive step of Cudd_addRoundOff.
Definition: cuddAddNeg.c:222
DdManager::siftMaxVar
int siftMaxVar
Definition: cuddInt.h:465
epd.h
The University of Colorado extended double precision package.
cuddTimesInDeathRow
int cuddTimesInDeathRow(DdManager *dd, DdNode *f)
Counts how many times a node is in the death row.
Definition: cuddRef.c:737
DdManager::tree
MtrNode * tree
Definition: cuddInt.h:480
cuddGa
int cuddGa(DdManager *table, int lower, int upper)
Genetic algorithm for DD reordering.
Definition: cuddGenetic.c:165
DdManager::randomizeOrder
unsigned int randomizeOrder
Definition: cuddInt.h:488
cuddCofactorRecur
DdNode * cuddCofactorRecur(DdManager *dd, DdNode *f, DdNode *g)
Performs the recursive step of Cudd_Cofactor.
Definition: cuddCof.c:253
cuddAddNegateRecur
DdNode * cuddAddNegateRecur(DdManager *dd, DdNode *f)
Implements the recursive step of Cudd_addNegate.
Definition: cuddAddNeg.c:162
cuddUniqueConst
DdNode * cuddUniqueConst(DdManager *unique, CUDD_VALUE_TYPE value)
Checks the unique table for the existence of a constant node.
Definition: cuddTable.c:1509
cuddCacheLookup2
DdNode * cuddCacheLookup2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
Looks up in the cache for the result of op applied to f and g.
Definition: cuddCache.c:432
cuddHeapProfile
int cuddHeapProfile(DdManager *dd)
Prints information about the heap.
Definition: cuddCheck.c:610
cuddDynamicAllocNode
DdNode * cuddDynamicAllocNode(DdManager *table)
Dynamically allocates a Node.
Definition: cuddReorder.c:361
DD_HFP
int(* DD_HFP)(DdManager *, const char *, void *)
Type of hook function.
Definition: cudd.h:234
cuddLevelQueueEnqueue
void * cuddLevelQueueEnqueue(DdLevelQueue *queue, void *key, int level)
Inserts a new key in a level queue.
Definition: cuddLevelQ.c:234
cuddBddRestrictRecur
DdNode * cuddBddRestrictRecur(DdManager *dd, DdNode *f, DdNode *c)
Performs the recursive step of Cudd_bddRestrict.
Definition: cuddGenCof.c:920
cuddSubsetHeavyBranch
DdNode * cuddSubsetHeavyBranch(DdManager *dd, DdNode *f, int numVars, int threshold)
The main procedure that returns a subset by choosing the heavier branch in the BDD.
Definition: cuddSubsetHB.c:278
DdManager::autoDynZ
int autoDynZ
Definition: cuddInt.h:473
cuddZddGetNegVarIndex
int cuddZddGetNegVarIndex(DdManager *dd, int index)
Returns the index of negative ZDD variable.
Definition: cuddZddFuncs.c:1516
cuddCacheInsert
void cuddCacheInsert(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h, DdNode *data)
Inserts a result in the cache for a function with three operands.
Definition: cuddCache.c:190
cuddSymmCheck
int cuddSymmCheck(DdManager *table, int x, int y)
Checks for symmetry of x and y.
Definition: cuddSymmetry.c:155
DD_OOMFP
void(* DD_OOMFP)(size_t)
Type of memory-out function.
Definition: cudd.h:258
CUDD_VALUE_TYPE
double CUDD_VALUE_TYPE
Type of the value of a terminal node.
Definition: cudd.h:189
DdManager::cacheHits
double cacheHits
Definition: cuddInt.h:409
cuddCacheLookup2Zdd
DdNode * cuddCacheLookup2Zdd(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
Looks up in the cache for the result of op applied to f and g.
Definition: cuddCache.c:536
DdManager::sentinel
DdNode sentinel
Definition: cuddInt.h:397
cuddMakeBddFromZddCover
DdNode * cuddMakeBddFromZddCover(DdManager *dd, DdNode *node)
Converts a ZDD cover to a BDD.
Definition: cuddZddIsop.c:775
cuddSwapping
int cuddSwapping(DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic)
Reorders variables by a sequence of (non-adjacent) swaps.
Definition: cuddReorder.c:556
DdManager::peakLiveNodes
unsigned int peakLiveNodes
Definition: cuddInt.h:518
DdSubtable::next
unsigned int next
Definition: cuddInt.h:383
DdManager::background
DdNode * background
Definition: cuddInt.h:402
DdNode::value
CUDD_VALUE_TYPE value
Definition: cuddInt.h:262
DdManager::maxmem
size_t maxmem
Definition: cuddInt.h:507
DdManager::realignZ
int realignZ
Definition: cuddInt.h:477
cuddZddNextLow
int cuddZddNextLow(DdManager *table, int x)
Finds the next subtable with a smaller index.
Definition: cuddZddReord.c:379
cuddNextHigh
int cuddNextHigh(DdManager *table, int x)
Finds the next subtable with a larger index.
Definition: cuddReorder.c:665
DdManager::univ
DdNode ** univ
Definition: cuddInt.h:443
DdManager::map
int * map
Definition: cuddInt.h:442
cuddUniqueInterIVO
DdNode * cuddUniqueInterIVO(DdManager *unique, int index, DdNode *T, DdNode *E)
Wrapper for cuddUniqueInter that is independent of variable ordering.
Definition: cuddTable.c:1334
cuddStCountfree
enum st_retval cuddStCountfree(void *key, void *value, void *arg)
Frees the memory used to store the minterm counts recorded in the visited table.
Definition: cuddUtil.c:2971
cuddZddUniqueCompare
int cuddZddUniqueCompare(void const *ptr_x, void const *ptr_y)
Comparison function used by qsort.
Definition: cuddZddReord.c:402
cuddCacheLookup1
DdNode * cuddCacheLookup1(DdManager *table, DD_CTFP1 op, DdNode *f)
Looks up in the cache for the result of op applied to f.
Definition: cuddCache.c:484
Cudd_ReorderingType
Cudd_ReorderingType
Type of reordering algorithm.
Definition: cudd.h:94
DdManager::deadMask
unsigned deadMask
Definition: cuddInt.h:457
DdManager::outOfMemCallback
DD_OOMFP outOfMemCallback
Definition: cuddInt.h:502
DdHashItem::key
DdNode * key[1]
Definition: cuddInt.h:342
DdManager::totCacheMisses
double totCacheMisses
Definition: cuddInt.h:513
cuddGarbageCollect
int cuddGarbageCollect(DdManager *unique, int clearCache)
Performs garbage collection on the BDD and ZDD unique tables.
Definition: cuddTable.c:736
cuddBddLICompaction
DdNode * cuddBddLICompaction(DdManager *dd, DdNode *f, DdNode *c)
Performs safe minimization of a BDD.
Definition: cuddGenCof.c:1443
cuddLocalCacheQuit
void cuddLocalCacheQuit(DdLocalCache *cache)
Shuts down a local computed table.
Definition: cuddLCache.c:215
cuddPrintNode
void cuddPrintNode(DdNode *f, FILE *fp)
Prints out information on a node.
Definition: cuddCheck.c:671
DdManager::keysZ
unsigned int keysZ
Definition: cuddInt.h:423
cuddNextLow
int cuddNextLow(DdManager *table, int x)
Finds the next subtable with a smaller index.
Definition: cuddReorder.c:686
cuddBddAndRecur
DdNode * cuddBddAndRecur(DdManager *manager, DdNode *f, DdNode *g)
Implements the recursive step of Cudd_bddAnd.
Definition: cuddBddIte.c:970
DdManager::reorderings
unsigned int reorderings
Definition: cuddInt.h:463
cuddHashTableInsert
int cuddHashTableInsert(DdHashTable *hash, DdNodePtr *key, DdNode *value, ptrint count)
Inserts an item in a hash table.
Definition: cuddLCache.c:617
DD_TOHFP
void(* DD_TOHFP)(DdManager *, void *)
Type of timeout handler.
Definition: cudd.h:270
cuddZddIntersect
DdNode * cuddZddIntersect(DdManager *zdd, DdNode *P, DdNode *Q)
Performs the recursive step of Cudd_zddIntersect.
Definition: cuddZddSetop.c:581
DdManager::gcEnabled
int gcEnabled
Definition: cuddInt.h:428
cuddZddDivideF
DdNode * cuddZddDivideF(DdManager *dd, DdNode *f, DdNode *g)
Performs the recursive step of Cudd_zddDivideF.
Definition: cuddZddFuncs.c:1211
DdHashItem
Local hash table item.
Definition: cuddInt.h:338
STAB_SIZE
#define STAB_SIZE
Size of the random number generator shuffle table.
Definition: cuddInt.h:188
cuddLevelQueueFirst
void * cuddLevelQueueFirst(DdLevelQueue *queue, void *key, int level)
Inserts the first key in a level queue.
Definition: cuddLevelQ.c:304
cuddBddXorRecur
DdNode * cuddBddXorRecur(DdManager *manager, DdNode *f, DdNode *g)
Implements the recursive step of Cudd_bddXor.
Definition: cuddBddIte.c:1100
DdManager::reordTime
unsigned long reordTime
Definition: cuddInt.h:511
DdManager::interact
ptruint * interact
Definition: cuddInt.h:447
DdSubtable::slots
unsigned int slots
Definition: cuddInt.h:379
cuddCacheProfile
int cuddCacheProfile(DdManager *table, FILE *fp)
Computes and prints a profile of the cache usage.
Definition: cuddCache.c:700
DdManager::out
FILE * out
Definition: cuddInt.h:495
DdManager::shuffleTable
int32_t shuffleTable[64]
Definition: cuddInt.h:523
cuddBddAlignToZdd
int cuddBddAlignToZdd(DdManager *table)
Reorders BDD variables according to the order of the ZDD variables.
Definition: cuddReorder.c:1195
DdSubtable::pairIndex
int pairIndex
Definition: cuddInt.h:387
DdManager::maxGrowthAlt
double maxGrowthAlt
Definition: cuddInt.h:471
DdManager::deadZ
unsigned int deadZ
Definition: cuddInt.h:425
DdManager::reclaimed
double reclaimed
Definition: cuddInt.h:436
cuddZddWeakDiv
DdNode * cuddZddWeakDiv(DdManager *dd, DdNode *f, DdNode *g)
Performs the recursive step of Cudd_zddWeakDiv.
Definition: cuddZddFuncs.c:721
cuddZddFreeUniv
void cuddZddFreeUniv(DdManager *zdd)
Frees the ZDD universe.
Definition: cuddInit.c:267
cuddZddSymmSiftingConv
int cuddZddSymmSiftingConv(DdManager *table, int lower, int upper)
Symmetric sifting to convergence algorithm for ZDDs.
Definition: cuddZddSymm.c:376
cuddZddGetPosVarIndex
int cuddZddGetPosVarIndex(DdManager *dd, int index)
Returns the index of positive ZDD variable.
Definition: cuddZddFuncs.c:1502
DdManager::realign
int realign
Definition: cuddInt.h:476
DdManager::autoDyn
int autoDyn
Definition: cuddInt.h:472
cuddZddSubset0
DdNode * cuddZddSubset0(DdManager *dd, DdNode *P, int var)
Computes the negative cofactor of a ZDD w.r.t. a variable.
Definition: cuddZddSetop.c:850
cuddZddSwapInPlace
int cuddZddSwapInPlace(DdManager *table, int x, int y)
Swaps two adjacent variables.
Definition: cuddZddReord.c:426
DdManager::maxSize
int maxSize
Definition: cuddInt.h:416
cuddSwapInPlace
int cuddSwapInPlace(DdManager *table, int x, int y)
Swaps two adjacent variables.
Definition: cuddReorder.c:709
cuddCacheLookupZdd
DdNode * cuddCacheLookupZdd(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h)
Looks up in the cache for the result of op applied to f, g, and h.
Definition: cuddCache.c:372
DdManager::nextDead
int nextDead
Definition: cuddInt.h:456
DdQueueItem
Generic level queue item.
Definition: cuddInt.h:582
DdChildren::T
struct DdNode * T
Definition: cuddInt.h:250
DdManager::GCTime
unsigned long GCTime
Definition: cuddInt.h:510
DdHashItem::value
DdNode * value
Definition: cuddInt.h:341
cuddShrinkSubtable
void cuddShrinkSubtable(DdManager *unique, int i)
Shrinks a subtable.
Definition: cuddTable.c:1764
cuddHashTableQuit
void cuddHashTableQuit(DdHashTable *hash)
Shuts down a hash table.
Definition: cuddLCache.c:538
DdManager::one
DdNode * one
Definition: cuddInt.h:398
cuddFreeTable
void cuddFreeTable(DdManager *unique)
Frees the resources associated to a unique table.
Definition: cuddTable.c:668
DdCache
Computed table.
Definition: cuddInt.h:364
cuddConstantLookup
DdNode * cuddConstantLookup(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h)
Looks up in the cache for the result of op applied to f, g, and h.
Definition: cuddCache.c:645
IndexKey
Used to sort variables for reordering.
Definition: cuddInt.h:574
cuddDestroySubtables
int cuddDestroySubtables(DdManager *unique, int n)
Destroys the n most recently created subtables in a unique table.
Definition: cuddTable.c:2176
DdManager::permZ
int * permZ
Definition: cuddInt.h:438
cuddBddConstrainRecur
DdNode * cuddBddConstrainRecur(DdManager *dd, DdNode *f, DdNode *c)
Performs the recursive step of Cudd_bddConstrain.
Definition: cuddGenCof.c:791
DdManager::treeZ
MtrNode * treeZ
Definition: cuddInt.h:481
st_table
Symbol table header.
Definition: st.c:101
DdHashTable
Local hash table.
Definition: cuddInt.h:348
cuddBddBooleanDiffRecur
DdNode * cuddBddBooleanDiffRecur(DdManager *manager, DdNode *f, DdNode *var)
Performs the recursive steps of Cudd_bddBoleanDiff.
Definition: cuddBddAbs.c:655
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:497
cuddHashTableInit
DdHashTable * cuddHashTableInit(DdManager *manager, unsigned int keySize, unsigned int initSize)
Initializes a hash table.
Definition: cuddLCache.c:489
cuddHashTableGenericQuit
void cuddHashTableGenericQuit(DdHashTable *hash)
Shuts down a hash table.
Definition: cuddLCache.c:582
DdManager::cacheSlack
int cacheSlack
Definition: cuddInt.h:411
DdManager::maxSizeZ
int maxSizeZ
Definition: cuddInt.h:417
cuddZddChangeAux
DdNode * cuddZddChangeAux(DdManager *zdd, DdNode *P, DdNode *zvar)
Performs the recursive step of Cudd_zddChange.
Definition: cuddZddSetop.c:728
cudd.h
The University of Colorado decision diagram package.
DdManager::memused
size_t memused
Definition: cuddInt.h:506
cuddHashTableLookup2
DdNode * cuddHashTableLookup2(DdHashTable *hash, DdNode *f, DdNode *g)
Looks up a key consisting of two pointers in a hash table.
Definition: cuddLCache.c:987
cuddAddScalarInverseRecur
DdNode * cuddAddScalarInverseRecur(DdManager *dd, DdNode *f, DdNode *epsilon)
Performs the recursive step of addScalarInverse.
Definition: cuddAddInv.c:139
DdHashTable::shift
int shift
Definition: cuddInt.h:355
cuddHashTableGenericInsert
int cuddHashTableGenericInsert(DdHashTable *hash, DdNode *f, void *value)
Inserts a generic item in a hash table.
Definition: cuddLCache.c:846
DdManager::siftMaxSwap
int siftMaxSwap
Definition: cuddInt.h:466
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Checks the unique table for the existence of an internal node.
Definition: cuddTable.c:1118
cuddUnderApprox
DdNode * cuddUnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)
Applies Tom Shiple's underappoximation algorithm.
Definition: cuddApprox.c:493