source: vis_dev/glu-2.3/src/cmuBdd/bddint.h @ 15

Last change on this file since 15 was 13, checked in by cecile, 13 years ago

library glu 2.3
File size: 20.7 KB
Line 
1/* BDD package internal definitions */
2
3
4#if !defined(_BDDINTH)
5#define _BDDINTH
6
7
8#include <setjmp.h>
9
10
11/* >>> Configuration things */
12
13/* Define this for cache and unique sizes to be a power of 2. */
14/* Probably not a good idea given the current simplistic hash function. */
15
16/* #define POWER_OF_2_SIZES */
17
18/* Define this if your C preprocessor is broken in such a way that */
19/* token concatenation can be done with something like: */
20/* #define CONCAT(f, g) f/''/g */
21/* where /''/ above would be an empty comment (' => *) if this */
22/* wasn't itself a comment.  Most of the (non-ANSI) UNIX C preprocessors */
23/* do seem to be broken, which is why this is defined.  If your C */
24/* preprocessor is ANSI, this shouldn't have any effect. */
25
26#define BROKEN_CPP
27
28
29
30/* >>> All user-visible stuff */
31
32#include "bdduser.h"
33
34
35#define ARGS(args) args
36
37
38/* Miscellaneous type definitions */
39
40typedef struct hash_table_ *hash_table;
41
42
43/* >>> BDD data structures */
44
45#if !defined(POWER_OF_2_SIZES)
46extern long bdd_primes[];
47#endif
48
49
50/* Pointer tagging stuff */
51
52#define POINTER(p) ((pointer)(((INT_PTR)(p)) & ~(INT_PTR)0x7))
53#define BDD_POINTER(p) ((bdd)POINTER(p))
54#define CACHE_POINTER(p) ((cache_entry)POINTER(p))
55
56#define TAG(p) ((int)(((INT_PTR)(p)) & 0x7))
57#define SET_TAG(p, t) ((pointer)((INT_PTR)POINTER(p) | (t)))
58
59#define TAG0(p) ((int)((INT_PTR)(p) & 0x1))
60#define FLIP_TAG0(p) ((pointer)((INT_PTR)(p) ^ 0x1))
61#define TAG0_HI(p) ((pointer)((INT_PTR)(p) | 0x1))
62#define TAG0_LO(p) ((pointer)((INT_PTR)(p) & ~(INT_PTR)0x1))
63
64#define TAG1(p) ((int)((INT_PTR)(p) & 0x2))
65#define FLIP_TAG1(p) ((pointer)((INT_PTR)(p) ^ 0x2))
66#define TAG1_HI(p) ((pointer)((INT_PTR)(p) | 0x2))
67#define TAG1_LO(p) ((pointer)((INT_PTR)(p) & ~(INT_PTR)0x2))
68
69#define TAG2(p) ((int)((INT_PTR)(p) & 0x4))
70#define FLIP_TAG2(p) ((pointer)((INT_PTR)(p) ^ 0x4))
71#define TAG2_HI(p) ((pointer)((INT_PTR)(p) | 0x4))
72#define TAG2_LO(p) ((pointer)((INT_PTR)(p) & ~(INT_PTR)0x4))
73
74
75/* Indexes */
76
77typedef unsigned short bdd_index_type;
78
79
80/* Types of various BDD node fields */
81
82typedef unsigned short bdd_indexindex_type;
83typedef unsigned char bdd_refcount_type;
84typedef unsigned char bdd_mark_type;
85
86
87/* A BDD node */
88
89struct bdd_
90{
91  bdd_indexindex_type indexindex;
92                                /* Index into indexes table */
93  bdd_refcount_type refs;       /* External reference count */
94  bdd_mark_type mark;           /* Mark and temporary ref count */
95  INT_PTR data[2];              /* Then and else pointers, or data */
96                                /* values for terminals */
97  struct bdd_ *next;
98};
99
100
101/* Maximum reference counts */
102
103#define BDD_MAX_REFS ((bdd_refcount_type)((1l << (8*sizeof(bdd_refcount_type))) - 1))
104#define BDD_MAX_TEMP_REFS ((bdd_mark_type)((1l << (8*sizeof(bdd_mark_type)-1)) - 1))
105
106#define BDD_GC_MARK ((bdd_mark_type)(1l << (8*sizeof(bdd_mark_type)-1)))
107
108
109/* Special indexindexes and indexes */
110
111#define BDD_CONST_INDEXINDEX 0
112#define BDD_MAX_INDEXINDEX ((bdd_indexindex_type)((1l << (8*sizeof(bdd_indexindex_type))) - 1))
113#define BDD_MAX_INDEX ((bdd_index_type)((1l << (8*sizeof(bdd_index_type))) - 1))
114
115
116/* Can this be done legally with a non-ANSI cpp? */
117
118#define CONCAT_PTR(f) f##_ptr
119
120#if defined(CONCAT_PTR)
121/* Field accessing stuff */
122
123#define BDD_SETUP(f) bdd CONCAT_PTR(f)=BDD_POINTER(f)
124#define BDD_RESET(f) CONCAT_PTR(f)=BDD_POINTER(f)
125#define BDD_INDEXINDEX(f) (CONCAT_PTR(f)->indexindex)
126#define BDD_DATA(f) (CONCAT_PTR(f)->data)
127#define BDD_DATA0(f) (CONCAT_PTR(f)->data[0])
128#define BDD_DATA1(f) (CONCAT_PTR(f)->data[1])
129#define BDD_REFS(f) (CONCAT_PTR(f)->refs)
130#define BDD_MARK(f) (CONCAT_PTR(f)->mark)
131#define BDD_TEMP_REFS(f) (CONCAT_PTR(f)->mark)
132
133
134/* Basic stuff stuff for indexes, testing, etc. */
135
136#define BDD_INDEX(bddm, f) ((bddm)->indexes[BDD_INDEXINDEX(f)])
137#define BDD_THEN(f) ((bdd)(BDD_DATA0(f) ^ TAG0(f)))
138#define BDD_ELSE(f) ((bdd)(BDD_DATA1(f) ^ TAG0(f)))
139#define BDD_SAME_OR_NEGATIONS(f, g) (CONCAT_PTR(f) == CONCAT_PTR(g))
140#define BDD_IS_CONST(f) (BDD_INDEXINDEX(f) == BDD_CONST_INDEXINDEX)
141#else
142/* Field accessing stuff */
143
144#define BDD_SETUP(f)
145#define BDD_RESET(f)
146#define BDD_INDEXINDEX(f) (BDD_POINTER(f)->indexindex)
147#define BDD_DATA(f) (BDD_POINTER(f)->data)
148#define BDD_DATA0(f) (BDD_POINTER(f)->data[0])
149#define BDD_DATA1(f) (BDD_POINTER(f)->data[1])
150#define BDD_REFS(f) (BDD_POINTER(f)->refs)
151#define BDD_MARK(f) (BDD_POINTER(f)->mark)
152#define BDD_TEMP_REFS(f) (BDD_POINTER(f)->mark)
153
154
155/* Basic stuff stuff for indexes, testing, etc. */
156
157#define BDD_INDEX(bddm, f) ((bddm)->indexes[BDD_INDEXINDEX(f)])
158#define BDD_THEN(f) ((bdd)(BDD_DATA0(f) ^ TAG0(f)))
159#define BDD_ELSE(f) ((bdd)(BDD_DATA1(f) ^ TAG0(f)))
160#define BDD_SAME_OR_NEGATIONS(f, g) (BDD_POINTER(f) == BDD_POINTER(g))
161#define BDD_IS_CONST(f) (BDD_INDEXINDEX(f) == BDD_CONST_INDEXINDEX)
162#endif
163
164
165/* BDD complement flag stuff */
166
167#define BDD_IS_OUTPOS(f) (!TAG0(f))
168#define BDD_OUTPOS(f) ((bdd)TAG0_LO(f))
169#define BDD_NOT(f) ((bdd)FLIP_TAG0(f))
170
171
172/* Cofactoring stuff */
173
174#define BDD_TOP_VAR2(top_indexindex, bddm, f, g)\
175do\
176  if (BDD_INDEX(bddm, f) < BDD_INDEX(bddm, g))\
177    top_indexindex=BDD_INDEXINDEX(f);\
178  else\
179    top_indexindex=BDD_INDEXINDEX(g);\
180while (0)
181
182#define BDD_TOP_VAR3(top_indexindex, bddm, f, g, h)\
183do\
184  if (BDD_INDEX(bddm, f) < BDD_INDEX(bddm, g))\
185    {\
186      top_indexindex=BDD_INDEXINDEX(f);\
187      if ((bddm)->indexes[top_indexindex] > BDD_INDEX(bddm, h))\
188        top_indexindex=BDD_INDEXINDEX(h);\
189    }\
190  else\
191    {\
192      top_indexindex=BDD_INDEXINDEX(g);\
193      if ((bddm)->indexes[top_indexindex] > BDD_INDEX(bddm, h))\
194        top_indexindex=BDD_INDEXINDEX(h);\
195    }\
196while (0)
197
198#define BDD_COFACTOR(top_indexindex, f, f_then, f_else)\
199do\
200  if (BDD_INDEXINDEX(f) == top_indexindex)\
201    {\
202      f_then=BDD_THEN(f);\
203      f_else=BDD_ELSE(f);\
204    }\
205  else\
206    {\
207      f_then=f;\
208      f_else=f;\
209    }\
210while (0)
211
212
213/* Ordering stuff */
214
215#define BDD_OUT_OF_ORDER(f, g) ((INT_PTR)f > (INT_PTR)g)
216
217#if defined(CONCAT_PTR)
218#define BDD_SWAP(f, g)\
219do\
220  {\
221    bdd _temp;\
222    _temp=f;\
223    f=g;\
224    g=_temp;\
225    _temp=CONCAT_PTR(f);\
226    CONCAT_PTR(f)=CONCAT_PTR(g);\
227    CONCAT_PTR(g)=_temp;\
228  }\
229while (0)
230#else
231#define BDD_SWAP(f, g)\
232do\
233  {\
234    bdd _temp;\
235    _temp=f;\
236    f=g;\
237    g=_temp;\
238  }\
239while (0)
240#endif
241
242
243/* This gets the variable at the top of a node. */
244
245#define BDD_IF(bddm, f) ((bddm)->variables[BDD_INDEXINDEX(f)])
246
247
248/* Reference count stuff */
249
250#define BDD_INCREFS(f)\
251do\
252  {\
253    if (BDD_REFS(f) >= BDD_MAX_REFS-1)\
254      {\
255        BDD_REFS(f)=BDD_MAX_REFS;\
256        BDD_TEMP_REFS(f)=0;\
257      }\
258   else\
259     BDD_REFS(f)++;\
260  }\
261while (0)
262
263#define BDD_DECREFS(f)\
264do\
265  {\
266    if (BDD_REFS(f) < BDD_MAX_REFS)\
267      BDD_REFS(f)--;\
268  }\
269while (0)
270
271#define BDD_TEMP_INCREFS(f)\
272do\
273  {\
274    if (BDD_REFS(f) < BDD_MAX_REFS)\
275      {\
276        BDD_TEMP_REFS(f)++;\
277        if (BDD_TEMP_REFS(f) == BDD_MAX_TEMP_REFS)\
278          {\
279            BDD_REFS(f)=BDD_MAX_REFS;\
280            BDD_TEMP_REFS(f)=0;\
281          }\
282      }\
283  }\
284while (0)
285
286#define BDD_TEMP_DECREFS(f)\
287do\
288  {\
289    if (BDD_REFS(f) < BDD_MAX_REFS)\
290      BDD_TEMP_REFS(f)--;\
291  }\
292while (0)
293
294#define BDD_IS_USED(f) ((BDD_MARK(f) & BDD_GC_MARK) != 0)
295
296
297/* Convert an internal reference to an external one and return. */
298
299#define RETURN_BDD(thing)\
300return (bdd_make_external(thing))
301
302
303/* These return the constants. */
304
305#define BDD_ONE(bddm) ((bddm)->one)
306#define BDD_ZERO(bddm) ((bddm)->zero)
307
308
309/* Cache entries */
310
311struct cache_entry_
312{
313  INT_PTR slot[4];
314};
315
316typedef struct cache_entry_ *cache_entry;
317
318
319/* Cache entry tags; ITE is for IF-THEN-ELSE operations.  TWO is for */
320/* the two argument operations that return a BDD result.  ONEDATA */
321/* and TWODATA are for one and two argument operations that return */
322/* double and single word data results.  Everything else is under */
323/* user control. */
324
325#define CACHE_TYPE_ITE 0x0
326#define CACHE_TYPE_TWO 0x1
327#define CACHE_TYPE_ONEDATA 0x2
328#define CACHE_TYPE_TWODATA 0x3
329#define CACHE_TYPE_USER1 0x4
330
331#define USER_ENTRY_TYPES 4
332
333
334/* Operation numbers (for CACHE_TYPE_TWO) */
335/* OP_RELPROD, OP_QNT and OP_SUBST need a reasonable number of holes */
336/* after them since the variable association number is added to them */
337/* to get the actual op.  OP_COMP, OP_SWAP and OP_CMPTO need */
338/* BDD_MAX_INDEX.  OP_SWAPAUX needs 2*BDD_MAX_INDEX.  Negative */
339/* operation numbers denote temporaries and are generated as needed. */
340
341#define OP_COFACTOR 100l
342#define OP_SATFRAC 200l
343#define OP_FWD 300l
344#define OP_REV 400l
345#define OP_RED 500l
346#define OP_EQUAL 600l
347#define OP_QNT 10000l
348#define OP_RELPROD 20000l
349#define OP_SUBST 30000l
350#define OP_COMP 100000l
351#define OP_CMPTO 200000l
352#define OP_SWAP 300000l
353#define OP_SWAPAUX 400000l
354
355
356/* Variable associations */
357
358struct var_assoc_
359{
360  bdd *assoc;                   /* Array with associated BDDs */
361  long last;                    /* Indexindex for lowest variable */
362};
363
364typedef struct var_assoc_ *var_assoc;
365
366
367struct assoc_list_
368{
369  struct var_assoc_ va;         /* The association */
370  int id;                       /* Identifier for this association */
371  int refs;                     /* Number of outstanding references */
372  struct assoc_list_ *next;     /* The next association */
373};
374
375typedef struct assoc_list_ *assoc_list;
376
377
378/* Variable blocks */
379
380struct block_
381{
382  long num_children;
383  struct block_ **children;
384  int reorderable;
385  long first_index;
386  long last_index;
387};
388
389
390/* A cache bin; the cache is two-way associative. */
391
392struct cache_bin_
393{
394  cache_entry entry[2];         /* LRU has index 1 */
395};
396
397typedef struct cache_bin_ cache_bin;
398
399
400/* The cache */
401
402struct cache_
403{
404  cache_bin *table;             /* The cache itself */
405  int size_index;               /* Index giving number of cache lines */
406  long size;                    /* Number of cache lines */
407  int cache_level;              /* Bin to start search in cache */
408                                /* Cache control functions: */
409  long (*rehash_fn[8]) ARGS((cmu_bdd_manager, cache_entry));
410                                /* Rehashes a cache entry */
411  int (*gc_fn[8]) ARGS((cmu_bdd_manager, cache_entry));
412                                /* Checks to see if an entry needs flushing */
413  void (*purge_fn[8]) ARGS((cmu_bdd_manager, cache_entry));
414                                /* Called when purging an entry */
415  void (*return_fn[8]) ARGS((cmu_bdd_manager, cache_entry));
416                                /* Called before returning from cache hit */
417  int (*flush_fn[8]) ARGS((cmu_bdd_manager, cache_entry, pointer));
418                                /* Called when freeing variable association */
419  int cache_ratio;              /* Cache to unique table size ratio */
420  long entries;                 /* Number of cache entries */
421  long lookups;                 /* Number of cache lookups */
422  long hits;                    /* Number of cache hits */
423  long inserts;                 /* Number of cache inserts */
424  long collisions;              /* Number of cache collisions */
425};
426
427typedef struct cache_ cache;
428
429
430/* One part of the node table */
431
432struct var_table_
433{
434  bdd *table;                   /* Pointers to the start of each bucket */
435  int size_index;               /* Index giving number of buckets */
436  long size;                    /* Number of buckets */
437  long entries;                 /* Number of BDD nodes in table */
438};
439
440typedef struct var_table_ *var_table;
441
442
443/* The BDD node table */
444
445struct unique_
446{
447  var_table *tables;            /* Individual variable tables */
448  void (*free_terminal_fn) ARGS((cmu_bdd_manager, INT_PTR, INT_PTR, pointer));
449                                /* Called when freeing MTBDD terminals */
450  pointer free_terminal_env;    /* Environment for free terminal function */
451  long entries;                 /* Total number of BDD nodes */
452  long gc_limit;                /* Try garbage collection at this point */
453  long node_limit;              /* Maximum number of BDD nodes allowed */
454  long gcs;                     /* Number of garbage collections */
455  long freed;                   /* Number of nodes freed */
456  long finds;                   /* Number of find operations */
457};
458
459typedef struct unique_ unique;
460
461
462/* Record manager size range stuff */
463
464#define MIN_REC_SIZE ALLOC_ALIGNMENT
465#define MAX_REC_SIZE 64
466
467#define REC_MGRS (((MAX_REC_SIZE-MIN_REC_SIZE)/ALLOC_ALIGNMENT)+1)
468
469
470/* Wrapper for jmp_buf since we may need to copy it sometimes and */
471/* we can't easily do it if it happens to be an array. */
472
473struct jump_buf_
474{
475  jmp_buf context;
476};
477
478typedef struct jump_buf_ jump_buf;
479
480
481/* A BDD manager */
482
483struct bdd_manager_
484{
485  unique unique_table;          /* BDD node table */
486  cache op_cache;               /* System result cache */
487  int check;                    /* Number of find calls 'til size checks */
488  bdd one;                      /* BDD for one */
489  bdd zero;                     /* BDD for zero */
490  int overflow;                 /* Nonzero if node limit exceeded */
491  void (*overflow_fn) ARGS((cmu_bdd_manager, pointer));
492                                /* Function to call on overflow */
493  pointer overflow_env;         /* Environment for overflow function */
494  void (*transform_fn) ARGS((cmu_bdd_manager, INT_PTR, INT_PTR, INT_PTR *, INT_PTR *, pointer));
495                                /* Function to transform terminal values */
496  pointer transform_env;        /* Environment for transform_fn */
497  int (*canonical_fn) ARGS((cmu_bdd_manager, INT_PTR, INT_PTR, pointer));
498                                /* Function to check if a terminal value is */
499                                /* canonical */
500  block super_block;            /* Top-level variable block */
501  void (*reorder_fn) ARGS((cmu_bdd_manager));
502                                /* Function to call to reorder variables */
503  pointer reorder_data;         /* For saving information btwn reorderings */
504  int allow_reordering;         /* Nonzero if reordering allowed */
505  long nodes_at_start;          /* Nodes at start of operation */
506  long vars;                    /* Number of variables */
507  long maxvars;                 /* Maximum number of variables w/o resize */
508  bdd *variables;               /* Array of variables, by indexindex */
509  bdd_index_type *indexes;      /* indexindex -> index table */
510  bdd_indexindex_type *indexindexes;
511                                /* index -> indexindex table */
512  int curr_assoc_id;            /* Current variable association number */
513  var_assoc curr_assoc;         /* Current variable association */
514  assoc_list assocs;            /* Variable associations */
515  struct var_assoc_ temp_assoc; /* Temporary variable association */
516  rec_mgr rms[REC_MGRS];        /* Record managers */
517  long temp_op;                 /* Current temporary operation number */
518  jump_buf abort;               /* Jump for out-of-memory cleanup */
519  void (*bag_it_fn) ARGS((cmu_bdd_manager, pointer));
520                                /* Non-null if going to abort at next find */
521  pointer bag_it_env; char *hooks;              /* Environment for bag it function */
522};
523
524
525/* Abort stuff */
526
527#define BDD_ABORTED 1
528#define BDD_OVERFLOWED 2
529#define BDD_REORDERED 3
530
531
532#define FIREWALL(bddm)\
533do\
534  {\
535    int retcode;\
536    (bddm)->allow_reordering=1;\
537    (bddm)->nodes_at_start=(bddm)->unique_table.entries;\
538    while ((retcode=(setjmp((bddm)->abort.context))))\
539      {\
540        bdd_cleanup(bddm, retcode);\
541        if (retcode == BDD_ABORTED || retcode == BDD_OVERFLOWED)\
542          return ((bdd)0);\
543        (bddm)->nodes_at_start=(bddm)->unique_table.entries;\
544      }\
545  }\
546while (0)
547
548
549#define FIREWALL1(bddm, cleanupcode)\
550do\
551  {\
552    int retcode;\
553    (bddm)->allow_reordering=1;\
554    (bddm)->nodes_at_start=(bddm)->unique_table.entries;\
555    while ((retcode=(setjmp((bddm)->abort.context))))\
556      {\
557        bdd_cleanup(bddm, retcode);\
558        cleanupcode\
559        (bddm)->nodes_at_start=(bddm)->unique_table.entries;\
560      }\
561  }\
562while (0)
563
564
565/* Node hash function */
566
567#define HASH_NODE(f, g) (((f) << 1)+(g))
568
569
570/* Table size stuff */
571
572#if defined(POWER_OF_2_SIZES)
573#define TABLE_SIZE(size_index) (1l << (size_index))
574#define BDD_REDUCE(i, size) (i)&=(size)-1
575#else
576#define TABLE_SIZE(size_index) (bdd_primes[size_index])
577#define BDD_REDUCE(i, size)\
578do\
579  {\
580    (i)%=(size);\
581    if ((i) < 0)\
582      (i)= -(i);\
583  }\
584while (0)
585#endif
586
587
588/* Record management */
589
590#define BDD_NEW_REC(bddm, size) mem_new_rec((bddm)->rms[(ROUNDUP(size)-MIN_REC_SIZE)/ALLOC_ALIGNMENT])
591#define BDD_FREE_REC(bddm, rec, size) mem_free_rec((bddm)->rms[(ROUNDUP(size)-MIN_REC_SIZE)/ALLOC_ALIGNMENT], (rec))
592
593
594/* >>> Declarations for random routines */
595
596/* Internal BDD routines */
597
598extern int bdd_check_arguments ARGS((int, ...));
599extern void bdd_check_array ARGS((bdd *));
600extern bdd bdd_make_external ARGS((bdd));
601extern int cmu_bdd_type_aux ARGS((cmu_bdd_manager, bdd));
602extern int cmu_bdd_is_cube ARGS((cmu_bdd_manager, bdd));
603extern void bdd_rehash_var_table ARGS((var_table, int));
604extern bdd bdd_find_aux ARGS((cmu_bdd_manager, bdd_indexindex_type, INT_PTR, INT_PTR));
605extern bdd cmu_bdd_ite_step ARGS((cmu_bdd_manager, bdd, bdd, bdd));
606extern bdd cmu_bdd_exists_temp ARGS((cmu_bdd_manager, bdd, long));
607extern bdd cmu_bdd_compose_temp ARGS((cmu_bdd_manager, bdd, bdd, bdd));
608extern bdd cmu_bdd_substitute_step ARGS((cmu_bdd_manager, bdd, long, bdd (*) ARGS((cmu_bdd_manager, bdd, bdd, bdd)), var_assoc));
609extern bdd cmu_bdd_swap_vars_temp ARGS((cmu_bdd_manager, bdd, bdd, bdd));
610extern int cmu_bdd_compare_temp ARGS((cmu_bdd_manager, bdd, bdd, bdd));
611extern double cmu_bdd_satisfying_fraction_step ARGS((cmu_bdd_manager, bdd));
612extern void bdd_mark_shared_nodes ARGS((cmu_bdd_manager, bdd));
613extern void bdd_number_shared_nodes ARGS((cmu_bdd_manager, bdd, hash_table, long *));
614extern char *bdd_terminal_id ARGS((cmu_bdd_manager, bdd, char *(*) ARGS((cmu_bdd_manager, INT_PTR, INT_PTR, pointer)), pointer));
615extern char *bdd_var_name ARGS((cmu_bdd_manager, bdd, char *(*) ARGS((cmu_bdd_manager, bdd, pointer)), pointer));
616extern long bdd_find_block ARGS((block, long));
617extern void bdd_block_delta ARGS((block, long));
618extern void cmu_bdd_reorder_aux ARGS((cmu_bdd_manager));
619extern void cmu_mtbdd_terminal_value_aux ARGS((cmu_bdd_manager, bdd, INT_PTR *, INT_PTR *));
620
621
622/* System cache routines */
623
624extern void bdd_insert_in_cache31 ARGS((cmu_bdd_manager, int, INT_PTR, INT_PTR, INT_PTR, INT_PTR));
625extern int bdd_lookup_in_cache31 ARGS((cmu_bdd_manager, int, INT_PTR, INT_PTR, INT_PTR, INT_PTR *));
626extern void bdd_insert_in_cache22 ARGS((cmu_bdd_manager, int, INT_PTR, INT_PTR, INT_PTR, INT_PTR));
627extern int bdd_lookup_in_cache22 ARGS((cmu_bdd_manager, int, INT_PTR, INT_PTR, INT_PTR *, INT_PTR *));
628extern void bdd_insert_in_cache13 ARGS((cmu_bdd_manager, int, INT_PTR, INT_PTR, INT_PTR, INT_PTR));
629extern int bdd_lookup_in_cache13 ARGS((cmu_bdd_manager, int, INT_PTR, INT_PTR *, INT_PTR *, INT_PTR *));
630extern void bdd_flush_cache ARGS((cmu_bdd_manager, int (*) ARGS((cmu_bdd_manager, cache_entry, pointer)), pointer));
631extern void bdd_purge_cache ARGS((cmu_bdd_manager));
632extern void bdd_flush_all ARGS((cmu_bdd_manager));
633extern int bdd_cache_functions ARGS((cmu_bdd_manager,
634                                     int,
635                                     int (*) ARGS((cmu_bdd_manager, cache_entry)),
636                                     void (*) ARGS((cmu_bdd_manager, cache_entry)),
637                                     void (*) ARGS((cmu_bdd_manager,cache_entry)),
638                                     int (*) ARGS((cmu_bdd_manager, cache_entry, pointer))));
639extern void cmu_bdd_free_cache_tag ARGS((cmu_bdd_manager, long));
640extern void bdd_rehash_cache ARGS((cmu_bdd_manager, int));
641extern void cmu_bdd_init_cache ARGS((cmu_bdd_manager));
642extern void cmu_bdd_free_cache ARGS((cmu_bdd_manager));
643
644#define bdd_insert_in_cache2(bddm, op, f, g, result)\
645bdd_insert_in_cache31((bddm), CACHE_TYPE_TWO, (INT_PTR)(op), (INT_PTR)(f), (INT_PTR)(g), (INT_PTR)(result))
646#define bdd_lookup_in_cache2(bddm, op, f, g, result)\
647bdd_lookup_in_cache31((bddm), CACHE_TYPE_TWO, (INT_PTR)(op), (INT_PTR)(f), (INT_PTR)(g), (INT_PTR *)(result))
648
649#define bdd_insert_in_cache1(bddm, op, f, result)\
650bdd_insert_in_cache2((bddm), (op), (f), BDD_ONE(bddm), (result))
651#define bdd_lookup_in_cache1(bddm, op, f, result)\
652bdd_lookup_in_cache2((bddm), (op), (f), BDD_ONE(bddm), (result))
653
654#define bdd_insert_in_cache2d(bddm, op, f, g, result)\
655bdd_insert_in_cache31((bddm), CACHE_TYPE_TWODATA, (INT_PTR)(op), (INT_PTR)(f), (INT_PTR)(g), (INT_PTR)(result))
656#define bdd_lookup_in_cache2d(bddm, op, f, g, result)\
657bdd_lookup_in_cache31((bddm), CACHE_TYPE_TWODATA, (INT_PTR)(op), (INT_PTR)(f), (INT_PTR)(g), (INT_PTR *)(result))
658
659#define bdd_insert_in_cache1d(bddm, op, f, result1, result2)\
660bdd_insert_in_cache22((bddm), CACHE_TYPE_ONEDATA, (INT_PTR)(op), (INT_PTR)(f), (INT_PTR)(result1), (INT_PTR)(result2))
661#define bdd_lookup_in_cache1d(bddm, op, f, result1, result2)\
662bdd_lookup_in_cache22((bddm), CACHE_TYPE_ONEDATA, (INT_PTR)(op), (INT_PTR)(f), (INT_PTR *)(result1), (INT_PTR *)(result2))
663
664#define cache_return_fn_none ((void (*)(cmu_bdd_manager, cache_entry))0)
665#define cache_purge_fn_none ((void (*)(cmu_bdd_manager, cache_entry))0)
666#define cache_reclaim_fn_none ((int (*)(cmu_bdd_manager, cache_entry, pointer))0)
667
668
669/* Unique table routines */
670
671extern void bdd_clear_temps ARGS((cmu_bdd_manager));
672extern void bdd_sweep_var_table ARGS((cmu_bdd_manager, long, int));
673extern void bdd_sweep ARGS((cmu_bdd_manager));
674extern void bdd_cleanup ARGS((cmu_bdd_manager, int));
675extern bdd bdd_find ARGS((cmu_bdd_manager, bdd_indexindex_type, bdd, bdd));
676extern bdd bdd_find_terminal ARGS((cmu_bdd_manager, INT_PTR, INT_PTR));
677extern var_table bdd_new_var_table ARGS((cmu_bdd_manager));
678extern void cmu_bdd_init_unique ARGS((cmu_bdd_manager));
679extern void cmu_bdd_free_unique ARGS((cmu_bdd_manager));
680
681
682/* Error routines */
683
684extern void cmu_bdd_fatal ARGS((char *));
685extern void cmu_bdd_warning ARGS((char *));
686
687
688/* >>> Hash table declarations */
689
690struct hash_rec_
691{
692  bdd key;
693  struct hash_rec_ *next;
694};
695
696typedef struct hash_rec_ *hash_rec;
697
698
699struct hash_table_
700{
701  hash_rec *table;
702  int size_index;
703  long size;
704  long entries;
705  int item_size;
706  cmu_bdd_manager bddm;
707};
708
709
710/* Hash table routines */
711
712extern void bdd_insert_in_hash_table ARGS((hash_table, bdd, pointer));
713extern pointer bdd_lookup_in_hash_table ARGS((hash_table, bdd));
714extern hash_table bdd_new_hash_table ARGS((cmu_bdd_manager, int));
715extern void cmu_bdd_free_hash_table ARGS((hash_table));
716
717
718#undef ARGS
719
720#endif
Note: See TracBrowser for help on using the repository browser.