source: vis_dev/glu-2.3/src/cmuBdd/bdduser.h @ 104

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

library glu 2.3
File size: 8.4 KB
Line 
1/* BDD user-visible definitions */
2
3
4#if !defined(_BDDUSERH)
5#define _BDDUSERH
6
7
8#include <stdio.h>
9#include <memuser.h>
10
11
12#define ARGS(args) args
13
14
15/* Types */
16
17typedef struct bdd_ *bdd;
18typedef struct bdd_manager_ *cmu_bdd_manager;
19typedef struct block_ *block;
20
21
22/* Return values for cmu_bdd_type */
23
24#define BDD_TYPE_NONTERMINAL 0
25#define BDD_TYPE_ZERO 1
26#define BDD_TYPE_ONE 2
27#define BDD_TYPE_POSVAR 3
28#define BDD_TYPE_NEGVAR 4
29#define BDD_TYPE_OVERFLOW 5
30#define BDD_TYPE_CONSTANT 6
31
32
33/* Error codes for cmu_bdd_undump_bdd */
34
35#define BDD_UNDUMP_FORMAT 1
36#define BDD_UNDUMP_OVERFLOW 2
37#define BDD_UNDUMP_IOERROR 3
38#define BDD_UNDUMP_EOF 4
39
40
41/* Basic BDD routine declarations */
42
43extern bdd cmu_bdd_one ARGS((cmu_bdd_manager));
44extern bdd cmu_bdd_zero ARGS((cmu_bdd_manager));
45extern bdd cmu_bdd_new_var_first ARGS((cmu_bdd_manager));
46extern bdd cmu_bdd_new_var_last ARGS((cmu_bdd_manager));
47extern bdd cmu_bdd_new_var_before ARGS((cmu_bdd_manager, bdd));
48extern bdd cmu_bdd_new_var_after ARGS((cmu_bdd_manager, bdd));
49extern bdd cmu_bdd_var_with_index ARGS((cmu_bdd_manager, long));
50extern bdd cmu_bdd_var_with_id ARGS((cmu_bdd_manager, long));
51extern bdd cmu_bdd_ite ARGS((cmu_bdd_manager, bdd, bdd, bdd));
52extern bdd cmu_bdd_and ARGS((cmu_bdd_manager, bdd, bdd));
53extern bdd cmu_bdd_nand ARGS((cmu_bdd_manager, bdd, bdd));
54extern bdd cmu_bdd_or ARGS((cmu_bdd_manager, bdd, bdd));
55extern bdd cmu_bdd_nor ARGS((cmu_bdd_manager, bdd, bdd));
56extern bdd cmu_bdd_xor ARGS((cmu_bdd_manager, bdd, bdd));
57extern bdd cmu_bdd_xnor ARGS((cmu_bdd_manager, bdd, bdd));
58extern bdd cmu_bdd_identity ARGS((cmu_bdd_manager, bdd));
59extern bdd cmu_bdd_not ARGS((cmu_bdd_manager, bdd));
60extern bdd cmu_bdd_if ARGS((cmu_bdd_manager, bdd));
61extern long cmu_bdd_if_index ARGS((cmu_bdd_manager, bdd));
62extern long cmu_bdd_if_id ARGS((cmu_bdd_manager, bdd));
63extern bdd cmu_bdd_then ARGS((cmu_bdd_manager, bdd));
64extern bdd cmu_bdd_else ARGS((cmu_bdd_manager, bdd));
65extern bdd cmu_bdd_intersects ARGS((cmu_bdd_manager, bdd, bdd));
66extern bdd cmu_bdd_implies ARGS((cmu_bdd_manager, bdd, bdd));
67extern int cmu_bdd_type ARGS((cmu_bdd_manager, bdd));
68extern void cmu_bdd_unfree ARGS((cmu_bdd_manager, bdd));
69extern void cmu_bdd_free ARGS((cmu_bdd_manager, bdd));
70extern long cmu_bdd_vars ARGS((cmu_bdd_manager));
71extern long cmu_bdd_total_size ARGS((cmu_bdd_manager));
72extern int cmu_bdd_cache_ratio ARGS((cmu_bdd_manager, int));
73extern long cmu_bdd_node_limit ARGS((cmu_bdd_manager, long));
74extern int cmu_bdd_overflow ARGS((cmu_bdd_manager));
75extern void cmu_bdd_overflow_closure ARGS((cmu_bdd_manager, void (*) ARGS((cmu_bdd_manager, pointer)), pointer));
76extern void cmu_bdd_abort_closure ARGS((cmu_bdd_manager, void (*) ARGS((cmu_bdd_manager, pointer)), pointer));
77extern void cmu_bdd_stats ARGS((cmu_bdd_manager, FILE *));
78extern cmu_bdd_manager cmu_bdd_init ARGS((void));
79extern void cmu_bdd_quit ARGS((cmu_bdd_manager));
80
81
82/* Variable association routine declarations */
83
84extern int cmu_bdd_new_assoc ARGS((cmu_bdd_manager, bdd *, int));
85extern void cmu_bdd_free_assoc ARGS((cmu_bdd_manager, int));
86extern void cmu_bdd_temp_assoc ARGS((cmu_bdd_manager, bdd *, int));
87extern void cmu_bdd_augment_temp_assoc ARGS((cmu_bdd_manager, bdd *, int));
88extern int cmu_bdd_assoc ARGS((cmu_bdd_manager, int));
89
90
91/* Comparison routine declarations */
92
93extern int cmu_bdd_compare ARGS((cmu_bdd_manager, bdd, bdd, bdd));
94
95
96/* Composition routine declarations */
97
98extern bdd cmu_bdd_compose ARGS((cmu_bdd_manager, bdd, bdd, bdd));
99extern bdd cmu_bdd_substitute ARGS((cmu_bdd_manager, bdd));
100
101
102/* Variable exchange routine declarations */
103
104extern bdd cmu_bdd_swap_vars ARGS((cmu_bdd_manager, bdd, bdd, bdd));
105
106
107/* Quantification routine declarations */
108
109extern bdd cmu_bdd_exists ARGS((cmu_bdd_manager, bdd));
110extern bdd cmu_bdd_forall ARGS((cmu_bdd_manager, bdd));
111
112
113/* Reduce routine declarations */
114
115extern bdd cmu_bdd_reduce ARGS((cmu_bdd_manager, bdd, bdd));
116extern bdd cmu_bdd_cofactor ARGS((cmu_bdd_manager, bdd, bdd));
117
118
119/* Relational product routine declarations */
120
121extern bdd cmu_bdd_rel_prod ARGS((cmu_bdd_manager, bdd, bdd));
122
123
124/* Satisfying valuation routine declarations */
125
126extern bdd cmu_bdd_satisfy ARGS((cmu_bdd_manager, bdd));
127extern bdd cmu_bdd_satisfy_support ARGS((cmu_bdd_manager, bdd));
128extern double cmu_bdd_satisfying_fraction ARGS((cmu_bdd_manager, bdd));
129
130
131/* Generic apply routine declarations */
132
133extern bdd bdd_apply2 ARGS((cmu_bdd_manager, bdd (*) ARGS((cmu_bdd_manager, bdd *, bdd *, pointer)), bdd, bdd, pointer));
134extern bdd bdd_apply1 ARGS((cmu_bdd_manager, bdd (*) ARGS((cmu_bdd_manager, bdd *, pointer)), bdd, pointer));
135
136
137/* Size and profile routine declarations */
138
139extern long cmu_bdd_size ARGS((cmu_bdd_manager, bdd, int));
140extern long cmu_bdd_size_multiple ARGS((cmu_bdd_manager, bdd *, int));
141extern void cmu_bdd_profile ARGS((cmu_bdd_manager, bdd, long *, int));
142extern void cmu_bdd_profile_multiple ARGS((cmu_bdd_manager, bdd *, long *, int));
143extern void cmu_bdd_function_profile ARGS((cmu_bdd_manager, bdd, long *));
144extern void cmu_bdd_function_profile_multiple ARGS((cmu_bdd_manager, bdd *, long *));
145
146
147/* Print routine declarations */
148
149#define bdd_naming_fn_none ((char *(*)(cmu_bdd_manager, bdd, pointer))0)
150#define bdd_terminal_id_fn_none ((char *(*)(cmu_bdd_manager, INT_PTR, INT_PTR, pointer))0)
151
152extern void cmu_bdd_print_bdd ARGS((cmu_bdd_manager,
153                                bdd,
154                                char *(*) ARGS((cmu_bdd_manager, bdd, pointer)),
155                                char *(*) ARGS((cmu_bdd_manager, INT_PTR, INT_PTR, pointer)),
156                                pointer,
157                                FILE *));
158extern void cmu_bdd_print_profile_aux ARGS((cmu_bdd_manager,
159                                        long *,
160                                        char *(*) ARGS((cmu_bdd_manager, bdd, pointer)),
161                                        pointer,
162                                        int,
163                                        FILE *));
164extern void cmu_bdd_print_profile ARGS((cmu_bdd_manager,
165                                    bdd,
166                                    char *(*) ARGS((cmu_bdd_manager, bdd, pointer)),
167                                    pointer,
168                                    int,
169                                    FILE *));
170extern void cmu_bdd_print_profile_multiple ARGS((cmu_bdd_manager,
171                                             bdd *,
172                                             char *(*) ARGS((cmu_bdd_manager, bdd, pointer)),
173                                             pointer,
174                                             int,
175                                             FILE *));
176extern void cmu_bdd_print_function_profile ARGS((cmu_bdd_manager,
177                                             bdd,
178                                             char *(*) ARGS((cmu_bdd_manager, bdd, pointer)),
179                                             pointer,
180                                             int,
181                                             FILE *));
182extern void cmu_bdd_print_function_profile_multiple ARGS((cmu_bdd_manager,
183                                                      bdd *,
184                                                      char *(*) ARGS((cmu_bdd_manager, bdd, pointer)),
185                                                      pointer,
186                                                      int,
187                                                      FILE *));
188
189
190/* Dump/undump routine declarations */
191
192extern int cmu_bdd_dump_bdd ARGS((cmu_bdd_manager, bdd, bdd *, FILE *));
193extern bdd cmu_bdd_undump_bdd ARGS((cmu_bdd_manager, bdd *, FILE *, int *));
194
195
196/* Support routine declarations */
197
198extern int cmu_bdd_depends_on ARGS((cmu_bdd_manager, bdd, bdd));
199extern void cmu_bdd_support ARGS((cmu_bdd_manager, bdd, bdd *));
200
201
202/* Unique table routine declarations */
203
204extern void cmu_bdd_gc ARGS((cmu_bdd_manager));
205extern void cmu_bdd_clear_refs ARGS((cmu_bdd_manager));
206
207
208/* Dynamic reordering routines */
209
210#define cmu_bdd_reorder_none ((void (*)(cmu_bdd_manager))0)
211
212extern void cmu_bdd_reorder_stable_window3 ARGS((cmu_bdd_manager));
213extern void cmu_bdd_reorder_sift ARGS((cmu_bdd_manager));
214extern void cmu_bdd_reorder_hybrid ARGS((cmu_bdd_manager));
215extern void cmu_bdd_var_block_reorderable ARGS((cmu_bdd_manager, block, int));
216extern void cmu_bdd_dynamic_reordering ARGS((cmu_bdd_manager, void (*) ARGS((cmu_bdd_manager))));
217extern void cmu_bdd_reorder ARGS((cmu_bdd_manager));
218
219extern bdd cmu_bdd_project ARGS((cmu_bdd_manager, bdd));
220
221/* Variable block routines */
222
223extern block cmu_bdd_new_var_block ARGS((cmu_bdd_manager, bdd, long));
224
225
226/* Multi-terminal BDD routine declarations */
227
228extern void mtbdd_transform_closure ARGS((cmu_bdd_manager,
229                                          int (*) ARGS((cmu_bdd_manager, INT_PTR, INT_PTR, pointer)),
230                                          void (*) ARGS((cmu_bdd_manager, INT_PTR, INT_PTR, INT_PTR *, INT_PTR *, pointer)),
231                                          pointer));
232extern void mtcmu_bdd_one_data ARGS((cmu_bdd_manager, INT_PTR, INT_PTR));
233extern void cmu_mtbdd_free_terminal_closure ARGS((cmu_bdd_manager,
234                                              void (*) ARGS((cmu_bdd_manager, INT_PTR, INT_PTR, pointer)),
235                                              pointer));
236extern bdd cmu_mtbdd_get_terminal ARGS((cmu_bdd_manager, INT_PTR, INT_PTR));
237extern void cmu_mtbdd_terminal_value ARGS((cmu_bdd_manager, bdd, INT_PTR *, INT_PTR *));
238extern bdd mtcmu_bdd_ite ARGS((cmu_bdd_manager, bdd, bdd, bdd));
239extern bdd cmu_mtbdd_equal ARGS((cmu_bdd_manager, bdd, bdd));
240extern bdd mtcmu_bdd_substitute ARGS((cmu_bdd_manager, bdd));
241#define mtbdd_transform(bddm, f) (cmu_bdd_not(bddm, f))
242
243
244#undef ARGS
245
246#endif
Note: See TracBrowser for help on using the repository browser.