source: vis_dev/glu-2.1/src/mdd/mdd.h @ 8

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

src glu
File size: 16.5 KB
RevLine 
[8]1/*
2 * $Id: mdd.h,v 1.29 2002/08/27 16:30:25 fabio Exp $
3 */
4
5#ifndef MDD_DEFINED
6#define MDD_DEFINED
7
8
9#include "util.h"
10#include "array.h"
11#include "st.h"
12#include "var_set.h"
13
14#include "bdd.h"
15
16/*    #include "bdd_int.h"   */
17
18/************************************************************************/
19#define str_len         10
20#define MONITOR         0
21#define MDD_VERBOSE     0
22#define SOLUTION        0
23#define BDD_SIZE        1
24#define USE_ITE         1
25#define BYPASS          1
26/* code may not be fully debugged for interleaving */
27#define INTERLEAVE      0
28
29#define mdd_and bdd_and
30#define mdd_and_with_limit bdd_and_with_limit
31#define mdd_and_array bdd_and_array
32#define mdd_cofactor_minterm bdd_cofactor
33#define mdd_constant bdd_constant
34#define mdd_dup bdd_dup
35/* mdd_equal returns 1 if two MDD's are identical */
36/* mdd_eq is a totally different function */
37/* which returns an MDD instead */
38#define mdd_equal bdd_equal
39#define mdd_equal_mod_care_set bdd_equal_mod_care_set
40#define mdd_closest_cube bdd_closest_cube
41#define mdd_free bdd_free
42#define mdd_get_manager bdd_get_manager
43#define mdd_is_tautology bdd_is_tautology
44#define mdd_ite bdd_ite
45/* mdd_lequal checks for implication, */
46/* mdd_lequal(f,g,1,0) returns the value of (f => g') */
47/* mdd_leq is a totally different function */
48#define mdd_lequal bdd_leq
49#define mdd_lequal_mod_care_set bdd_lequal_mod_care_set
50#define mdd_lequal_array bdd_leq_array
51#define mdd_multiway_and bdd_multiway_and
52#define mdd_multiway_or bdd_multiway_or
53#define mdd_multiway_xor bdd_multiway_xor
54#define mdd_not bdd_not
55#define mdd_one bdd_one
56#define mdd_or bdd_or
57#define mdd_size bdd_size
58#define mdd_size_multiple bdd_size_multiple
59#define mdd_top_var_id bdd_top_var_id
60#define mdd_xor bdd_xor
61#define mdd_xnor bdd_xnor
62#define mdd_zero bdd_zero
63#define mdd_EMPTY bdd_EMPTY
64
65#define mdd_first_solution mdd_first_cube
66#define mdd_next_solution mdd_next_cube
67
68#define mdd_eq_c(m,a,b)         mdd_func1c(m,a,b,eq2)
69#define mdd_geq_c(m,a,b)        mdd_func1c(m,a,b,geq2)
70#define mdd_gt_c(m,a,b)         mdd_func1c(m,a,b,gt2)
71#define mdd_leq_c(m,a,b)        mdd_func1c(m,a,b,leq2)
72#define mdd_lt_c(m,a,b)         mdd_func1c(m,a,b,lt2)
73#define mdd_neq_c(m,a,b)        mdd_func1c(m,a,b,neq2)
74
75#define mdd_eq(m,a,b)           mdd_func2(m,a,b,eq2)
76#define mdd_geq(m,a,b)          mdd_func2(m,a,b,geq2)
77#define mdd_gt(m,a,b)           mdd_func2(m,a,b,gt2)
78#define mdd_leq(m,a,b)          mdd_func2(m,a,b,leq2)
79#define mdd_lt(m,a,b)           mdd_func2(m,a,b,lt2)
80#define mdd_neq(m,a,b)          mdd_func2(m,a,b,neq2)
81#define mdd_unary_minus(m,a,b)  mdd_func2(m,a,b,unary_minus2)
82
83#define mdd_eq_plus(m,a,b,c)    mdd_func3(m,a,b,c,eq_plus3)
84#define mdd_geq_plus(m,a,b,c)   mdd_func3(m,a,b,c,geq_plus3)
85#define mdd_gt_plus(m,a,b,c)    mdd_func3(m,a,b,c,gt_plus3)
86#define mdd_leq_plus(m,a,b,c)   mdd_func3(m,a,b,c,leq_plus3)
87#define mdd_lt_plus(m,a,b,c)    mdd_func3(m,a,b,c,lt_plus3)
88#define mdd_neq_plus(m,a,b,c)   mdd_func3(m,a,b,c,neq_plus3)
89
90#define mdd_eq_minus(m,a,b,c)   mdd_func3(m,a,b,c,eq_minus3)
91#define mdd_geq_minus(m,a,b,c)  mdd_func3(m,a,b,c,geq_minus3)
92#define mdd_gt_minus(m,a,b,c)   mdd_func3(m,a,b,c,gt_minus3)
93#define mdd_leq_minus(m,a,b,c)  mdd_func3(m,a,b,c,leq_minus3)
94#define mdd_lt_minus(m,a,b,c)   mdd_func3(m,a,b,c,lt_minus3)
95#define mdd_neq_minus(m,a,b,c)  mdd_func3(m,a,b,c,neq_minus3)
96
97#define mdd_eq_plus_c(m,a,b,c)  mdd_func2c(m,a,b,c,eq_plus3)
98#define mdd_geq_plus_c(m,a,b,c) mdd_func2c(m,a,b,c,geq_plus3)
99#define mdd_gt_plus_c(m,a,b,c)  mdd_func2c(m,a,b,c,gt_plus3)
100#define mdd_leq_plus_c(m,a,b,c) mdd_func2c(m,a,b,c,leq_plus3)
101#define mdd_lt_plus_c(m,a,b,c)  mdd_func2c(m,a,b,c,lt_plus3)
102#define mdd_neq_plus_c(m,a,b,c) mdd_func2c(m,a,b,c,neq_plus3)
103
104
105#define mdd_eq_plus_c_mod(m,a,b,c)      mdd_func2c_mod(m,a,b,c,eq_plus3mod)
106#define mdd_geq_plus_c_mod(m,a,b,c)     mdd_func2c_mod(m,a,b,c,geq_plus3mod)
107#define mdd_gt_plus_c_mod(m,a,b,c)      mdd_func2c_mod(m,a,b,c,gt_plus3mod)
108#define mdd_leq_plus_c_mod(m,a,b,c)     mdd_func2c_mod(m,a,b,c,leq_plus3mod)
109#define mdd_lt_plus_c_mod(m,a,b,c)      mdd_func2c_mod(m,a,b,c,lt_plus3mod)
110#define mdd_neq_plus_c_mod(m,a,b,c)     mdd_func2c_mod(m,a,b,c,neq_plus3mod)
111
112#define mdd_eq_minus_c_mod(m,a,b,c)     mdd_func2c_mod(m,a,b,c,eq_minus3mod)
113#define mdd_geq_minus_c_mod(m,a,b,c)    mdd_func2c_mod(m,a,b,c,geq_minus3mod)
114#define mdd_gt_minus_c_mod(m,a,b,c)     mdd_func2c_mod(m,a,b,c,gt_minus3mod)
115#define mdd_leq_minus_c_mod(m,a,b,c)    mdd_func2c_mod(m,a,b,c,leq_minus3mod)
116#define mdd_lt_minus_c_mod(m,a,b,c)     mdd_func2c_mod(m,a,b,c,lt_minus3mod)
117#define mdd_neq_minus_c_mod(m,a,b,c)    mdd_func2c_mod(m,a,b,c,neq_minus3mod)
118
119#define mdd_eq_s(m,a,b)         mdd_ineq_template_s(m,a,b,0,0,1)
120#define mdd_geq_s(m,a,b)        mdd_ineq_template_s(m,a,b,0,1,1)
121#define mdd_gt_s(m,a,b)         mdd_ineq_template_s(m,a,b,0,1,0)
122#define mdd_neq_s(m,a,b)        mdd_ineq_template_s(m,a,b,1,1,0)
123#define mdd_leq_s(m,a,b)        mdd_ineq_template_s(m,a,b,1,0,1)
124#define mdd_lt_s(m,a,b)         mdd_ineq_template_s(m,a,b,1,0,0)
125
126/**** for backward compatibility only ****/
127#define mdd_eq_g(m,a,b)         mdd_func2(m,a,b,eq2)
128#define mdd_geq_g(m,a,b)        mdd_func2(m,a,b,geq2)
129#define mdd_gt_g(m,a,b)         mdd_func2(m,a,b,gt2)
130#define mdd_leq_g(m,a,b)        mdd_func2(m,a,b,leq2)
131#define mdd_lt_g(m,a,b)         mdd_func2(m,a,b,lt2)
132#define mdd_neq_g(m,a,b)        mdd_func2(m,a,b,neq2)
133#define mdd_init_name(v,n,s)    mdd_init(v,n,s)
134
135/* mdd_int.h */
136#define MDD_NOT(node)           ((bdd_node *) ((int) (node) ^ 01))
137#define MDD_REGULAR(node)       ((bdd_node *) ((int) (node) & ~01))
138#define MDD_IS_COMPLEMENT(node) ((int) (node) & 01)
139
140#define MDD_ONE(bdd)            (bdd)->one
141#define MDD_ZERO(bdd)           (MDD_NOT(MDD_ONE(bdd)))
142
143#ifndef MAX
144#define MAX(a,b) (a) > (b) ? (a) : (b)
145#endif
146
147#ifndef MIN
148#define MIN(a,b) (a) < (b) ? (a) : (b)
149#endif
150
151    typedef bdd_t mdd_t;
152    typedef bdd_manager mdd_manager;
153
154typedef enum {
155        MDD_ACTIVE,
156        MDD_BUNDLED
157} mvar_status;
158
159struct mvar_type {
160    int mvar_id;                /* mvar id */
161    mvar_status status;         /* Whether the mvar is currently being used or
162                                   has been bundled into another mvar */
163    char *name;                 /* name of mvar */
164    int values;                 /* no. of values mvar can take */
165    int encode_length;          /* no. of binary variables, bvar's, */
166                                /* needed to encode mvar */
167    array_t *bvars;             /* array of bvar_id's from most significant bit to least
168                                   significant bit, has size encode_length */
169    int *encoding;              /* internal use only */
170};
171typedef struct mvar_type mvar_type;
172
173struct bvar_type {
174    mdd_t *node;
175    int mvar_id;
176};
177typedef struct bvar_type bvar_type;
178
179struct mdd_hook_type {
180    array_t *mvar_list;
181    array_t *bvar_list; 
182};
183
184typedef struct mdd_hook_type mdd_hook_type;
185
186struct mdd_gen {
187    mdd_manager *manager;
188    bdd_gen *bdd_generator;
189    bdd_gen_status status;
190    array_t *cube;              /* array of literals {0,1,2} of all vars */
191    array_t *minterm;           /* current minterm */
192    array_t *var_list;          /* list of var id's */
193    boolean out_of_range;
194}; 
195
196typedef struct mdd_gen mdd_gen;
197
198#define foreach_mdd_minterm(fn, gen, minterm, var_list)\
199  for((gen) = mdd_first_minterm(fn, &minterm, var_list);\
200      ((gen)->status != bdd_EMPTY) ? TRUE: mdd_gen_free(gen);\
201      (void) mdd_next_minterm(gen, &minterm))
202                                                                     
203
204extern mdd_hook_type mdd_hook;
205
206
207/*---------------------------------------------------------------------------*/
208/* Function prototypes                                                       */
209/*---------------------------------------------------------------------------*/
210
211EXTERN mdd_manager *mdd_init ARGS((array_t *mvar_values, array_t *mvar_names, array_t *mvar_strides));
212EXTERN mdd_manager *mdd_init_empty ARGS((void));
213EXTERN unsigned int mdd_create_variables ARGS((mdd_manager *mgr, array_t *mvar_values, array_t *mvar_names, array_t *mvar_strides));
214EXTERN unsigned int mdd_create_variables_after ARGS((mdd_manager*, int, array_t*, array_t*, array_t* ));
215EXTERN unsigned int mdd_create_variables_interleaved ARGS((mdd_manager*, int, int, array_t*));
216EXTERN void mdd_quit ARGS((mdd_manager *mgr));
217EXTERN mdd_t *mdd_case ARGS((mdd_manager *mgr, int mvar, array_t *child_list));
218EXTERN mdd_t *mdd_consensus ARGS((mdd_manager *mgr, mdd_t *fn, array_t *mvars));
219EXTERN mdd_t *mdd_encode ARGS((mdd_manager *mgr, array_t *child_list, mvar_type *mv_ptr, int index));
220EXTERN mdd_t *mdd_literal ARGS((mdd_manager *mgr, int mddid, array_t *values));
221EXTERN void   mdd_search ARGS((mdd_manager *mgr, bdd_t *top, int phase, boolean minterms));
222EXTERN mdd_t *mdd_cofactor ARGS((mdd_manager *mgr, mdd_t *fn, mdd_t *cube));
223EXTERN mdd_t *mdd_smooth ARGS((mdd_manager *mgr, mdd_t *fn, array_t *mvars));
224EXTERN mdd_t *mdd_and_smooth ARGS((mdd_manager *mgr, mdd_t *f, mdd_t *g, array_t *mvars));
225EXTERN mdd_t *mdd_and_smooth_with_limit ARGS((mdd_manager *mgr, mdd_t *f, mdd_t *g, array_t *mvars, unsigned int limit));
226EXTERN mdd_t *mdd_substitute ARGS((mdd_manager *mgr, mdd_t *fn, array_t *old_mvars, array_t *new_mvars));
227EXTERN array_t *mdd_substitute_array ARGS((mdd_manager *mgr, array_t *fn_array, array_t *old_mvars, array_t *new_mvars));
228EXTERN array_t *mdd_get_support ARGS((mdd_manager *mdd_mgr, mdd_t *f));
229EXTERN array_t *mdd_get_bdd_support_ids ARGS((mdd_manager *mdd_mgr, mdd_t *f));
230EXTERN array_t *mdd_get_bdd_support_vars ARGS((mdd_manager *mdd_mgr, mdd_t *f));
231EXTERN mdd_t *mdd_interval ARGS((mdd_manager *mgr, int mvar_id, int low, int high)); 
232EXTERN double mdd_count_onset ARGS((mdd_manager *mddMgr, mdd_t *aMdd, array_t *mddIdArr));
233EXTERN mdd_t *mdd_onset_bdd ARGS((mdd_manager *mddMgr, mdd_t *aMdd, array_t *mddIdArr));
234EXTERN int mdd_epd_count_onset ARGS((mdd_manager *mddMgr, mdd_t *aMdd, array_t *mddIdArr, EpDouble *epd));
235EXTERN array_t  * mdd_ret_bvars_of_mvar ARGS((mvar_type *mvar_ptr));
236EXTERN mdd_t *mdd_cproject ARGS((mdd_manager *mgr, mdd_t *T, array_t *mvars));
237EXTERN mdd_t *mdd_mod ARGS((mdd_manager *mgr, int a_mvar_id, int b_mvar_id, int M));
238EXTERN mdd_t *mdd_ineq_template_s ARGS((mdd_manager *mgr, int mvar1, int mvar2, int zero_then_val, int one_else_val, int bottom_val));
239EXTERN mdd_t *mdd_add_s ARGS((mdd_manager *mgr, int sum_id, int mvar_id1, int mvar_id2 ));
240/* mdd_iter.c */
241EXTERN mdd_gen *mdd_first_minterm ARGS((mdd_t *f, array_t **minterm_p, array_t *var_list));
242EXTERN boolean mdd_next_minterm ARGS((mdd_gen *mgen, array_t **minterm_p));
243EXTERN void mdd_print_array ARGS((array_t *array));
244EXTERN int mdd_gen_free ARGS((mdd_gen *mgen));
245EXTERN mdd_t *mdd_func1c ARGS((mdd_manager *mgr, int mvar1, int mvar2, boolean (*func1c) (int, int)));
246EXTERN mdd_t *mdd_func2 ARGS((mdd_manager *mgr, int mvar1, int mvar2, boolean (*func2) (int, int)));
247/* functions of 2 variables used by mdd_func2 ARGS(()) */
248EXTERN boolean eq2 ARGS((int x, int y));
249EXTERN boolean geq2 ARGS((int x, int y));
250EXTERN boolean gt2 ARGS((int x, int y));
251EXTERN boolean leq2 ARGS((int x, int y));
252EXTERN boolean lt2 ARGS((int x, int y));
253EXTERN boolean neq2 ARGS((int x, int y));
254EXTERN boolean unary_minus2 ARGS((int x, int y));
255EXTERN mdd_t *mdd_func2c ARGS((mdd_manager *mgr,int mvar1, int mvar2, int constant, boolean (*func3)(int, int, int)));
256EXTERN mdd_t *mdd_func2c_mod ARGS((mdd_manager *mgr,int mvar1, int mvar2, int constant, boolean (*func4)(int, int, int, int)));
257
258/* should be in ../test */
259EXTERN mdd_t *mdd_func3 ARGS((mdd_manager *mgr, int mvar1, int mvar2, int mvar3, boolean (*func3)(int, int, int)));
260/* functions of 3 variables used by mdd_func3 ARGS(()) */
261EXTERN boolean eq_plus3 ARGS((int x, int y, int z));
262EXTERN boolean geq_plus3 ARGS((int x, int y, int z));
263EXTERN boolean gt_plus3 ARGS((int x, int y, int z));
264EXTERN boolean leq_plus3 ARGS((int x, int y, int z));
265EXTERN boolean lt_plus3 ARGS((int x, int y, int z));
266EXTERN boolean neq_plus3 ARGS((int x, int y, int z));
267/* actually functions below can be obtained from the set above */
268/* by just suppling the negation of the constant value */
269EXTERN boolean eq_minus3 ARGS((int x, int y, int z));
270EXTERN boolean geq_minus3 ARGS((int x, int y, int z));
271EXTERN boolean gt_minus3 ARGS((int x, int y, int z));
272EXTERN boolean leq_minus3 ARGS((int x, int y, int z));
273EXTERN boolean lt_minus3 ARGS((int x, int y, int z));
274EXTERN boolean neq_minus3 ARGS((int x, int y, int z));
275
276EXTERN array_t *mdd_id_to_bdd_id_array ARGS((mdd_manager *mddManager, int mddId));
277EXTERN array_t *mdd_id_to_bdd_array ARGS((mdd_manager *mddManager, int mddId));
278EXTERN array_t *mdd_id_array_to_bdd_array ARGS((mdd_manager *mddManager, array_t *mddIdArray));
279EXTERN array_t *mdd_id_array_to_bdd_id_array ARGS((mdd_manager *mddManager, array_t *mddIdArray));
280EXTERN mdd_t *mdd_id_array_to_bdd_cube ARGS((mdd_manager *mddManager, array_t *mddIdArray));
281EXTERN int mdd_get_number_of_bdd_vars ARGS((mdd_manager *mddManager, array_t *mddIdArray));
282EXTERN int mdd_get_number_of_bdd_support ARGS((mdd_manager *mddManager, mdd_t *f));
283EXTERN array_t *mdd_fn_array_to_bdd_rel_array ARGS((mdd_manager *mddManager, int mddId, array_t *mddFnArray));
284EXTERN array_t *mdd_fn_array_to_bdd_fn_array ARGS((mdd_manager *mddManager, int mddId, array_t *mddFnArray));
285EXTERN array_t *mdd_pick_arbitrary_minterms ARGS((mdd_manager *mgr, mdd_t *f, array_t *mddIdArr, int n));
286EXTERN mdd_t *mdd_subset_with_mask_vars ARGS((mdd_manager *mgr, mdd_t *f, array_t *mddIdArr, array_t *maskIdArr));
287EXTERN mvar_type mdd_get_var_by_id ARGS((mdd_manager *mddMgr, int id));
288EXTERN void mdd_print_support ARGS((mdd_t *f));
289EXTERN void mdd_print_support_to_file ARGS((FILE *fout, char *format, mdd_t *f));
290EXTERN char *mdd_read_var_name ARGS((mdd_t *f));
291EXTERN int mdd_read_mdd_id ARGS((mdd_t *f));
292EXTERN int mdd_check_support ARGS((mdd_manager *mddMgr, mdd_t *mdd, array_t *supportIdArray));
293EXTERN int mdd_equal_mod_care_set_array ARGS((mdd_t *aSet, mdd_t *bSet, array_t *CareSetArray));
294EXTERN int mdd_lequal_mod_care_set_array ARGS((mdd_t *aSet, mdd_t *bSet, boolean aPhase, boolean bPhase, array_t *CareSetArray));
295
296EXTERN boolean eq_plus3mod ARGS((int x, int y, int z, int range));
297EXTERN boolean geq_plus3mod ARGS((int x, int y, int z, int range));
298EXTERN boolean gt_plus3mod ARGS((int x, int y, int z, int range));
299EXTERN boolean leq_plus3mod ARGS((int x, int y, int z, int range));
300EXTERN boolean lt_plus3mod ARGS((int x, int y, int z, int range));
301EXTERN boolean neq_plus3mod ARGS((int x, int y, int z, int range));
302/* actually functions below can be obtained from the set above */
303/* by just suppling the negation of the constant value */
304EXTERN boolean eq_minus3mod ARGS((int x, int y, int z, int range));
305EXTERN boolean geq_minus3mod ARGS((int x, int y, int z, int range));
306EXTERN boolean gt_minus3mod ARGS((int x, int y, int z, int range));
307EXTERN boolean leq_minus3mod ARGS((int x, int y, int z, int range));
308EXTERN boolean lt_minus3mod ARGS((int x, int y, int z, int range));
309EXTERN boolean neq_minus3mod ARGS((int x, int y, int z, int range));
310
311/* should be in mdd_int.h */
312EXTERN int toggle ARGS((int x));
313EXTERN int no_bit_encode ARGS((int n));
314EXTERN void print_strides ARGS((array_t *mvar_strides));
315EXTERN void print_mvar_list ARGS((mdd_manager *mgr));
316EXTERN void print_bdd_list_id ARGS((array_t *bdd_list));
317EXTERN void print_bvar_list_id ARGS((mdd_manager *mgr));
318EXTERN void print_bdd ARGS((bdd_manager *mgr, bdd_t *top));
319EXTERN mvar_type find_mvar_id ARGS((mdd_manager *mgr, unsigned short id));
320EXTERN void clear_all_marks ARGS((mdd_manager *mgr));
321EXTERN void mdd_mark ARGS((mdd_manager *mgr, bdd_t *top, int phase));
322EXTERN void mdd_unmark ARGS((mdd_manager *mgr, bdd_t *top));
323EXTERN mvar_type find_mvar ARGS((mdd_manager *mgr, char *name));
324EXTERN array_t *mdd_ret_mvar_list ARGS((mdd_manager *mgr));
325EXTERN void mdd_set_mvar_list ARGS((mdd_manager *mgr, array_t *mvar_list));
326EXTERN array_t *mdd_ret_bvar_list ARGS((mdd_manager *mgr));
327EXTERN mdd_t *build_lt_c ARGS((mdd_manager *mgr, int mvar_id, int c));
328EXTERN mdd_t *build_leq_c ARGS((mdd_manager *mgr, int mvar_id, int c));
329EXTERN mdd_t *build_gt_c ARGS((mdd_manager *mgr, int mvar_id, int c));
330EXTERN mdd_t *build_geq_c ARGS((mdd_manager *mgr, int mvar_id, int c));
331EXTERN int getbit ARGS((int number, int position));
332EXTERN int integer_get_num_of_digits ARGS((int value));
333EXTERN int mdd_ret_bvar_id ARGS((mvar_type *mvar_ptr, int i));
334EXTERN bvar_type mdd_ret_bvar ARGS((mvar_type *mvar_ptr, int i, array_t *bvar_list));
335EXTERN void mdd_array_free ARGS((array_t *mddArray));
336EXTERN void mdd_array_array_free ARGS((array_t *arrayBddArray));
337EXTERN array_t *mdd_array_duplicate ARGS((array_t *mddArray));
338EXTERN boolean mdd_array_equal ARGS((array_t *array1, array_t *array2));
339EXTERN mdd_t *mdd_range_mdd ARGS((mdd_manager *mgr, array_t *support));
340
341/* unsupported */
342EXTERN int mdd_bundle_variables ARGS((mdd_manager *mgr, array_t *bundle_vars, char *mdd_var_name, int *mdd_id));
343EXTERN mdd_t * mdd_unary_minus_s ARGS((mdd_manager *mgr, int mvar1, int mvar2));
344EXTERN array_t * mvar2bdds ARGS((mdd_manager *mgr, array_t *mvars));
345#endif
Note: See TracBrowser for help on using the repository browser.