glu-2.2: src/mdd/mdd.h Source File

00001 /*
00002  * $Id: mdd.h,v 1.33 2009/01/18 02:26:49 fabio Exp $
00003  */
00004 
00005 #ifndef MDD_DEFINED
00006 #define MDD_DEFINED
00007 
00008 
00009 #include "util.h"
00010 #include "array.h"
00011 #include "st.h"
00012 #include "var_set.h"
00013 
00014 #include "bdd.h" 
00015 
00016 /*    #include "bdd_int.h"   */
00017 
00018 /************************************************************************/
00019 #define str_len         10
00020 #define MONITOR         0
00021 #define MDD_VERBOSE     0
00022 #define SOLUTION        0
00023 #define BDD_SIZE        1
00024 #define USE_ITE         1
00025 #define BYPASS          1
00026 /* code may not be fully debugged for interleaving */
00027 #define INTERLEAVE      0
00028 
00029 #define mdd_and bdd_and
00030 #define mdd_and_with_limit bdd_and_with_limit
00031 #define mdd_and_array bdd_and_array
00032 #define mdd_cofactor_minterm bdd_cofactor
00033 #define mdd_constant bdd_constant
00034 #define mdd_dup bdd_dup
00035 /* mdd_equal returns 1 if two MDD's are identical */
00036 /* mdd_eq is a totally different function */
00037 /* which returns an MDD instead */
00038 #define mdd_equal bdd_equal
00039 #define mdd_equal_mod_care_set bdd_equal_mod_care_set
00040 #define mdd_closest_cube bdd_closest_cube
00041 #define mdd_free bdd_free
00042 #define mdd_get_manager bdd_get_manager
00043 #define mdd_is_tautology bdd_is_tautology
00044 #define mdd_ite bdd_ite
00045 /* mdd_lequal checks for implication, */
00046 /* mdd_lequal(f,g,1,0) returns the value of (f => g') */
00047 /* mdd_leq is a totally different function */
00048 #define mdd_lequal bdd_leq
00049 #define mdd_lequal_mod_care_set bdd_lequal_mod_care_set
00050 #define mdd_lequal_array bdd_leq_array
00051 #define mdd_multiway_and bdd_multiway_and
00052 #define mdd_multiway_or bdd_multiway_or
00053 #define mdd_multiway_xor bdd_multiway_xor
00054 #define mdd_not bdd_not
00055 #define mdd_one bdd_one
00056 #define mdd_or bdd_or
00057 #define mdd_size bdd_size
00058 #define mdd_size_multiple bdd_size_multiple
00059 #define mdd_top_var_id bdd_top_var_id
00060 #define mdd_xor bdd_xor
00061 #define mdd_xnor bdd_xnor
00062 #define mdd_zero bdd_zero
00063 #define mdd_EMPTY bdd_EMPTY
00064 
00065 #define mdd_first_solution mdd_first_cube
00066 #define mdd_next_solution mdd_next_cube
00067 
00068 #define mdd_eq_c(m,a,b)         mdd_func1c(m,a,b,eq2)
00069 #define mdd_geq_c(m,a,b)        mdd_func1c(m,a,b,geq2)
00070 #define mdd_gt_c(m,a,b)         mdd_func1c(m,a,b,gt2)
00071 #define mdd_leq_c(m,a,b)        mdd_func1c(m,a,b,leq2)
00072 #define mdd_lt_c(m,a,b)         mdd_func1c(m,a,b,lt2)
00073 #define mdd_neq_c(m,a,b)        mdd_func1c(m,a,b,neq2)
00074 
00075 #define mdd_eq(m,a,b)           mdd_func2(m,a,b,eq2)
00076 #define mdd_geq(m,a,b)          mdd_func2(m,a,b,geq2)
00077 #define mdd_gt(m,a,b)           mdd_func2(m,a,b,gt2)
00078 #define mdd_leq(m,a,b)          mdd_func2(m,a,b,leq2)
00079 #define mdd_lt(m,a,b)           mdd_func2(m,a,b,lt2)
00080 #define mdd_neq(m,a,b)          mdd_func2(m,a,b,neq2)
00081 #define mdd_unary_minus(m,a,b)  mdd_func2(m,a,b,unary_minus2)
00082 
00083 #define mdd_eq_plus(m,a,b,c)    mdd_func3(m,a,b,c,eq_plus3)
00084 #define mdd_geq_plus(m,a,b,c)   mdd_func3(m,a,b,c,geq_plus3)
00085 #define mdd_gt_plus(m,a,b,c)    mdd_func3(m,a,b,c,gt_plus3)
00086 #define mdd_leq_plus(m,a,b,c)   mdd_func3(m,a,b,c,leq_plus3)
00087 #define mdd_lt_plus(m,a,b,c)    mdd_func3(m,a,b,c,lt_plus3)
00088 #define mdd_neq_plus(m,a,b,c)   mdd_func3(m,a,b,c,neq_plus3)
00089 
00090 #define mdd_eq_minus(m,a,b,c)   mdd_func3(m,a,b,c,eq_minus3)
00091 #define mdd_geq_minus(m,a,b,c)  mdd_func3(m,a,b,c,geq_minus3)
00092 #define mdd_gt_minus(m,a,b,c)   mdd_func3(m,a,b,c,gt_minus3)
00093 #define mdd_leq_minus(m,a,b,c)  mdd_func3(m,a,b,c,leq_minus3)
00094 #define mdd_lt_minus(m,a,b,c)   mdd_func3(m,a,b,c,lt_minus3)
00095 #define mdd_neq_minus(m,a,b,c)  mdd_func3(m,a,b,c,neq_minus3)
00096 
00097 #define mdd_eq_plus_c(m,a,b,c)  mdd_func2c(m,a,b,c,eq_plus3)
00098 #define mdd_geq_plus_c(m,a,b,c) mdd_func2c(m,a,b,c,geq_plus3)
00099 #define mdd_gt_plus_c(m,a,b,c)  mdd_func2c(m,a,b,c,gt_plus3)
00100 #define mdd_leq_plus_c(m,a,b,c) mdd_func2c(m,a,b,c,leq_plus3)
00101 #define mdd_lt_plus_c(m,a,b,c)  mdd_func2c(m,a,b,c,lt_plus3)
00102 #define mdd_neq_plus_c(m,a,b,c) mdd_func2c(m,a,b,c,neq_plus3)
00103 
00104 
00105 #define mdd_eq_plus_c_mod(m,a,b,c)      mdd_func2c_mod(m,a,b,c,eq_plus3mod)
00106 #define mdd_geq_plus_c_mod(m,a,b,c)     mdd_func2c_mod(m,a,b,c,geq_plus3mod)
00107 #define mdd_gt_plus_c_mod(m,a,b,c)      mdd_func2c_mod(m,a,b,c,gt_plus3mod)
00108 #define mdd_leq_plus_c_mod(m,a,b,c)     mdd_func2c_mod(m,a,b,c,leq_plus3mod)
00109 #define mdd_lt_plus_c_mod(m,a,b,c)      mdd_func2c_mod(m,a,b,c,lt_plus3mod)
00110 #define mdd_neq_plus_c_mod(m,a,b,c)     mdd_func2c_mod(m,a,b,c,neq_plus3mod)
00111 
00112 #define mdd_eq_minus_c_mod(m,a,b,c)     mdd_func2c_mod(m,a,b,c,eq_minus3mod)
00113 #define mdd_geq_minus_c_mod(m,a,b,c)    mdd_func2c_mod(m,a,b,c,geq_minus3mod)
00114 #define mdd_gt_minus_c_mod(m,a,b,c)     mdd_func2c_mod(m,a,b,c,gt_minus3mod)
00115 #define mdd_leq_minus_c_mod(m,a,b,c)    mdd_func2c_mod(m,a,b,c,leq_minus3mod)
00116 #define mdd_lt_minus_c_mod(m,a,b,c)     mdd_func2c_mod(m,a,b,c,lt_minus3mod)
00117 #define mdd_neq_minus_c_mod(m,a,b,c)    mdd_func2c_mod(m,a,b,c,neq_minus3mod)
00118 
00119 #define mdd_eq_s(m,a,b)         mdd_ineq_template_s(m,a,b,0,0,1)
00120 #define mdd_geq_s(m,a,b)        mdd_ineq_template_s(m,a,b,0,1,1)
00121 #define mdd_gt_s(m,a,b)         mdd_ineq_template_s(m,a,b,0,1,0)
00122 #define mdd_neq_s(m,a,b)        mdd_ineq_template_s(m,a,b,1,1,0)
00123 #define mdd_leq_s(m,a,b)        mdd_ineq_template_s(m,a,b,1,0,1)
00124 #define mdd_lt_s(m,a,b)         mdd_ineq_template_s(m,a,b,1,0,0)
00125 
00126 /**** for backward compatibility only ****/
00127 #define mdd_eq_g(m,a,b)         mdd_func2(m,a,b,eq2)
00128 #define mdd_geq_g(m,a,b)        mdd_func2(m,a,b,geq2)
00129 #define mdd_gt_g(m,a,b)         mdd_func2(m,a,b,gt2)
00130 #define mdd_leq_g(m,a,b)        mdd_func2(m,a,b,leq2)
00131 #define mdd_lt_g(m,a,b)         mdd_func2(m,a,b,lt2)
00132 #define mdd_neq_g(m,a,b)        mdd_func2(m,a,b,neq2)
00133 #define mdd_init_name(v,n,s)    mdd_init(v,n,s)
00134 
00135 /* mdd_int.h */
00136 #define MDD_NOT(node)           ((bdd_node *) ((int) (node) ^ 01))
00137 #define MDD_REGULAR(node)       ((bdd_node *) ((int) (node) & ~01))
00138 #define MDD_IS_COMPLEMENT(node) ((int) (node) & 01)
00139 
00140 #define MDD_ONE(bdd)            (bdd)->one
00141 #define MDD_ZERO(bdd)           (MDD_NOT(MDD_ONE(bdd)))
00142 
00143 #ifndef MAX
00144 #define MAX(a,b) (a) > (b) ? (a) : (b)
00145 #endif
00146 
00147 #ifndef MIN
00148 #define MIN(a,b) (a) < (b) ? (a) : (b)
00149 #endif
00150 
00151     typedef bdd_t mdd_t;
00152     typedef bdd_manager mdd_manager;
00153 
00154 typedef enum {
00155         MDD_ACTIVE,
00156         MDD_BUNDLED
00157 } mvar_status;
00158 
00159 struct mvar_type {
00160     int mvar_id;                /* mvar id */
00161     mvar_status status;         /* Whether the mvar is currently being used or 
00162                                    has been bundled into another mvar */
00163     char *name;                 /* name of mvar */
00164     int values;                 /* no. of values mvar can take */
00165     int encode_length;          /* no. of binary variables, bvar's, */
00166                                 /* needed to encode mvar */
00167     array_t *bvars;             /* array of bvar_id's from most significant bit to least 
00168                                    significant bit, has size encode_length */
00169     int *encoding;              /* internal use only */
00170 };
00171 typedef struct mvar_type mvar_type;
00172 
00173 struct bvar_type {
00174     mdd_t *node;
00175     int mvar_id;
00176 };
00177 typedef struct bvar_type bvar_type;
00178 
00179 struct mdd_hook_type {
00180     array_t *mvar_list;
00181     array_t *bvar_list; 
00182 };
00183 
00184 typedef struct mdd_hook_type mdd_hook_type;
00185 
00186 struct mdd_gen {
00187     mdd_manager *manager;
00188     bdd_gen *bdd_generator;
00189     bdd_gen_status status;
00190     array_t *cube;              /* array of literals {0,1,2} of all vars */
00191     array_t *minterm;           /* current minterm */
00192     array_t *var_list;          /* list of var id's */
00193     boolean out_of_range;
00194 }; 
00195 
00196 typedef struct mdd_gen mdd_gen;
00197 
00198 #define foreach_mdd_minterm(fn, gen, minterm, var_list)\
00199   for((gen) = mdd_first_minterm(fn, &minterm, var_list);\
00200       ((gen)->status != bdd_EMPTY) ? TRUE: mdd_gen_free(gen);\
00201       (void) mdd_next_minterm(gen, &minterm))
00202                                                                       
00203 
00204 extern mdd_hook_type mdd_hook;
00205 
00206 
00207 /*---------------------------------------------------------------------------*/
00208 /* Function prototypes                                                       */
00209 /*---------------------------------------------------------------------------*/
00210 
00211 EXTERN mdd_manager *mdd_init ARGS((array_t *mvar_values, array_t *mvar_names, array_t *mvar_strides));
00212 EXTERN mdd_manager *mdd_init_empty ARGS((void));
00213 EXTERN unsigned int mdd_create_variables ARGS((mdd_manager *mgr, array_t *mvar_values, array_t *mvar_names, array_t *mvar_strides));
00214 EXTERN unsigned int mdd_create_variables_after ARGS((mdd_manager*, int, array_t*, array_t*, array_t* ));
00215 EXTERN unsigned int mdd_create_variables_interleaved ARGS((mdd_manager*, int, int, array_t*));
00216 EXTERN void mdd_quit ARGS((mdd_manager *mgr));
00217 EXTERN void mdd_restart ARGS((mdd_manager *mgr));
00218 EXTERN void mdd_var_expunge_bdd_variable ARGS((mdd_manager *mgr, int bddId, int val));
00219 EXTERN mdd_t *mdd_case ARGS((mdd_manager *mgr, int mvar, array_t *child_list));
00220 EXTERN mdd_t *mdd_consensus ARGS((mdd_manager *mgr, mdd_t *fn, array_t *mvars));
00221 EXTERN mdd_t *mdd_encode ARGS((mdd_manager *mgr, array_t *child_list, mvar_type *mv_ptr, int index));
00222 EXTERN mdd_t *mdd_literal ARGS((mdd_manager *mgr, int mddid, array_t *values));
00223 EXTERN void   mdd_search ARGS((mdd_manager *mgr, bdd_t *top, int phase, boolean minterms));
00224 EXTERN mdd_t *mdd_cofactor ARGS((mdd_manager *mgr, mdd_t *fn, mdd_t *cube));
00225 EXTERN mdd_t *mdd_smooth ARGS((mdd_manager *mgr, mdd_t *fn, array_t *mvars));
00226 EXTERN mdd_t *mdd_and_smooth ARGS((mdd_manager *mgr, mdd_t *f, mdd_t *g, array_t *mvars));
00227 EXTERN mdd_t *mdd_and_smooth_with_limit ARGS((mdd_manager *mgr, mdd_t *f, mdd_t *g, array_t *mvars, unsigned int limit));
00228 EXTERN mdd_t *mdd_substitute ARGS((mdd_manager *mgr, mdd_t *fn, array_t *old_mvars, array_t *new_mvars));
00229 EXTERN array_t *mdd_substitute_array ARGS((mdd_manager *mgr, array_t *fn_array, array_t *old_mvars, array_t *new_mvars));
00230 EXTERN array_t *mdd_get_support ARGS((mdd_manager *mdd_mgr, mdd_t *f));
00231 EXTERN array_t *mdd_get_bdd_support_ids ARGS((mdd_manager *mdd_mgr, mdd_t *f));
00232 EXTERN array_t *mdd_get_bdd_support_vars ARGS((mdd_manager *mdd_mgr, mdd_t *f));
00233 EXTERN mdd_t *mdd_interval ARGS((mdd_manager *mgr, int mvar_id, int low, int high)); 
00234 EXTERN double mdd_count_onset ARGS((mdd_manager *mddMgr, mdd_t *aMdd, array_t *mddIdArr));
00235 EXTERN mdd_t *mdd_onset_bdd ARGS((mdd_manager *mddMgr, mdd_t *aMdd, array_t *mddIdArr));
00236 EXTERN int mdd_epd_count_onset ARGS((mdd_manager *mddMgr, mdd_t *aMdd, array_t *mddIdArr, EpDouble *epd));
00237 EXTERN array_t  * mdd_ret_bvars_of_mvar ARGS((mvar_type *mvar_ptr));
00238 EXTERN mdd_t *mdd_cproject ARGS((mdd_manager *mgr, mdd_t *T, array_t *mvars));
00239 EXTERN mdd_t *mdd_mod ARGS((mdd_manager *mgr, int a_mvar_id, int b_mvar_id, int M));
00240 EXTERN 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));
00241 EXTERN mdd_t *mdd_add_s ARGS((mdd_manager *mgr, int sum_id, int mvar_id1, int mvar_id2 ));
00242 /* mdd_iter.c */
00243 EXTERN mdd_gen *mdd_first_minterm ARGS((mdd_t *f, array_t **minterm_p, array_t *var_list));
00244 EXTERN boolean mdd_next_minterm ARGS((mdd_gen *mgen, array_t **minterm_p));
00245 EXTERN void mdd_print_array ARGS((array_t *array));
00246 EXTERN int mdd_gen_free ARGS((mdd_gen *mgen));
00247 EXTERN mdd_t *mdd_func1c ARGS((mdd_manager *mgr, int mvar1, int mvar2, boolean (*func1c) (int, int)));
00248 EXTERN mdd_t *mdd_func2 ARGS((mdd_manager *mgr, int mvar1, int mvar2, boolean (*func2) (int, int)));
00249 /* functions of 2 variables used by mdd_func2 ARGS(()) */
00250 EXTERN boolean eq2 ARGS((int x, int y));
00251 EXTERN boolean geq2 ARGS((int x, int y));
00252 EXTERN boolean gt2 ARGS((int x, int y));
00253 EXTERN boolean leq2 ARGS((int x, int y));
00254 EXTERN boolean lt2 ARGS((int x, int y));
00255 EXTERN boolean neq2 ARGS((int x, int y));
00256 EXTERN boolean unary_minus2 ARGS((int x, int y));
00257 EXTERN mdd_t *mdd_func2c ARGS((mdd_manager *mgr,int mvar1, int mvar2, int constant, boolean (*func3)(int, int, int)));
00258 EXTERN mdd_t *mdd_func2c_mod ARGS((mdd_manager *mgr,int mvar1, int mvar2, int constant, boolean (*func4)(int, int, int, int)));
00259 
00260 /* should be in ../test */
00261 EXTERN mdd_t *mdd_func3 ARGS((mdd_manager *mgr, int mvar1, int mvar2, int mvar3, boolean (*func3)(int, int, int)));
00262 /* functions of 3 variables used by mdd_func3 ARGS(()) */
00263 EXTERN boolean eq_plus3 ARGS((int x, int y, int z));
00264 EXTERN boolean geq_plus3 ARGS((int x, int y, int z));
00265 EXTERN boolean gt_plus3 ARGS((int x, int y, int z));
00266 EXTERN boolean leq_plus3 ARGS((int x, int y, int z));
00267 EXTERN boolean lt_plus3 ARGS((int x, int y, int z));
00268 EXTERN boolean neq_plus3 ARGS((int x, int y, int z));
00269 /* actually functions below can be obtained from the set above */
00270 /* by just suppling the negation of the constant value */
00271 EXTERN boolean eq_minus3 ARGS((int x, int y, int z));
00272 EXTERN boolean geq_minus3 ARGS((int x, int y, int z));
00273 EXTERN boolean gt_minus3 ARGS((int x, int y, int z));
00274 EXTERN boolean leq_minus3 ARGS((int x, int y, int z));
00275 EXTERN boolean lt_minus3 ARGS((int x, int y, int z));
00276 EXTERN boolean neq_minus3 ARGS((int x, int y, int z));
00277 
00278 EXTERN array_t *mdd_id_to_bdd_id_array ARGS((mdd_manager *mddManager, int mddId));
00279 EXTERN array_t *mdd_id_to_bdd_array ARGS((mdd_manager *mddManager, int mddId));
00280 EXTERN array_t *mdd_id_array_to_bdd_array ARGS((mdd_manager *mddManager, array_t *mddIdArray));
00281 EXTERN array_t *mdd_id_array_to_bdd_id_array ARGS((mdd_manager *mddManager, array_t *mddIdArray));
00282 EXTERN mdd_t *mdd_id_array_to_bdd_cube ARGS((mdd_manager *mddManager, array_t *mddIdArray));
00283 EXTERN int mdd_get_number_of_bdd_vars ARGS((mdd_manager *mddManager, array_t *mddIdArray));
00284 EXTERN int mdd_get_number_of_bdd_support ARGS((mdd_manager *mddManager, mdd_t *f));
00285 EXTERN array_t *mdd_fn_array_to_bdd_rel_array ARGS((mdd_manager *mddManager, int mddId, array_t *mddFnArray));
00286 EXTERN array_t *mdd_fn_array_to_bdd_fn_array ARGS((mdd_manager *mddManager, int mddId, array_t *mddFnArray));
00287 EXTERN array_t *mdd_pick_arbitrary_minterms ARGS((mdd_manager *mgr, mdd_t *f, array_t *mddIdArr, int n));
00288 EXTERN mdd_t *mdd_subset_with_mask_vars ARGS((mdd_manager *mgr, mdd_t *f, array_t *mddIdArr, array_t *maskIdArr));
00289 EXTERN mvar_type mdd_get_var_by_id ARGS((mdd_manager *mddMgr, int id));
00290 EXTERN void mdd_print_support ARGS((mdd_t *f));
00291 EXTERN void mdd_print_support_to_file ARGS((FILE *fout, char *format, mdd_t *f));
00292 EXTERN char *mdd_read_var_name ARGS((mdd_t *f));
00293 EXTERN int mdd_read_mdd_id ARGS((mdd_t *f));
00294 EXTERN int mdd_check_support ARGS((mdd_manager *mddMgr, mdd_t *mdd, array_t *supportIdArray));
00295 EXTERN int mdd_equal_mod_care_set_array ARGS((mdd_t *aSet, mdd_t *bSet, array_t *CareSetArray));
00296 EXTERN int mdd_lequal_mod_care_set_array ARGS((mdd_t *aSet, mdd_t *bSet, boolean aPhase, boolean bPhase, array_t *CareSetArray));
00297 
00298 EXTERN boolean eq_plus3mod ARGS((int x, int y, int z, int range));
00299 EXTERN boolean geq_plus3mod ARGS((int x, int y, int z, int range));
00300 EXTERN boolean gt_plus3mod ARGS((int x, int y, int z, int range));
00301 EXTERN boolean leq_plus3mod ARGS((int x, int y, int z, int range));
00302 EXTERN boolean lt_plus3mod ARGS((int x, int y, int z, int range));
00303 EXTERN boolean neq_plus3mod ARGS((int x, int y, int z, int range));
00304 /* actually functions below can be obtained from the set above */
00305 /* by just suppling the negation of the constant value */
00306 EXTERN boolean eq_minus3mod ARGS((int x, int y, int z, int range));
00307 EXTERN boolean geq_minus3mod ARGS((int x, int y, int z, int range));
00308 EXTERN boolean gt_minus3mod ARGS((int x, int y, int z, int range));
00309 EXTERN boolean leq_minus3mod ARGS((int x, int y, int z, int range));
00310 EXTERN boolean lt_minus3mod ARGS((int x, int y, int z, int range));
00311 EXTERN boolean neq_minus3mod ARGS((int x, int y, int z, int range));
00312 EXTERN void mdd_array_dump_dot ARGS((array_t *mdds, char *name, FILE *fp));
00313 EXTERN void mdd_dump_dot ARGS((mdd_t *mdd, char *name, FILE *fp));
00314 EXTERN void mdd_array_print_cover ARGS((array_t *mdds, char *name, boolean disjoint));
00315 EXTERN void mdd_print_cover ARGS((mdd_t *f, char *name, boolean disjoint));
00316 
00317 /* should be in mdd_int.h */
00318 EXTERN int toggle ARGS((int x));
00319 EXTERN int no_bit_encode ARGS((int n));
00320 EXTERN void print_strides ARGS((array_t *mvar_strides));
00321 EXTERN void print_mvar_list ARGS((mdd_manager *mgr));
00322 EXTERN void print_bdd_list_id ARGS((array_t *bdd_list));
00323 EXTERN void print_bvar_list_id ARGS((mdd_manager *mgr));
00324 EXTERN void print_bdd ARGS((bdd_manager *mgr, bdd_t *top));
00325 EXTERN mvar_type find_mvar_id ARGS((mdd_manager *mgr, unsigned short id));
00326 EXTERN void clear_all_marks ARGS((mdd_manager *mgr));
00327 EXTERN void mdd_mark ARGS((mdd_manager *mgr, bdd_t *top, int phase));
00328 EXTERN void mdd_unmark ARGS((mdd_manager *mgr, bdd_t *top));
00329 EXTERN mvar_type find_mvar ARGS((mdd_manager *mgr, char *name));
00330 EXTERN array_t *mdd_ret_mvar_list ARGS((mdd_manager *mgr));
00331 EXTERN void mdd_set_mvar_list ARGS((mdd_manager *mgr, array_t *mvar_list));
00332 EXTERN array_t *mdd_ret_bvar_list ARGS((mdd_manager *mgr));
00333 EXTERN void mdd_set_bvar_list ARGS((mdd_manager *mgr, array_t *bvar_list));
00334 EXTERN mdd_t *build_lt_c ARGS((mdd_manager *mgr, int mvar_id, int c));
00335 EXTERN mdd_t *build_leq_c ARGS((mdd_manager *mgr, int mvar_id, int c));
00336 EXTERN mdd_t *build_gt_c ARGS((mdd_manager *mgr, int mvar_id, int c));
00337 EXTERN mdd_t *build_geq_c ARGS((mdd_manager *mgr, int mvar_id, int c));
00338 EXTERN int getbit ARGS((int number, int position));
00339 EXTERN int integer_get_num_of_digits ARGS((int value));
00340 EXTERN int mdd_ret_bvar_id ARGS((mvar_type *mvar_ptr, int i));
00341 EXTERN bvar_type mdd_ret_bvar ARGS((mvar_type *mvar_ptr, int i, array_t *bvar_list));
00342 EXTERN void mdd_array_free ARGS((array_t *mddArray));
00343 EXTERN void mdd_array_array_free ARGS((array_t *arrayBddArray));
00344 EXTERN array_t *mdd_array_duplicate ARGS((array_t *mddArray));
00345 EXTERN boolean mdd_array_equal ARGS((array_t *array1, array_t *array2));
00346 EXTERN mdd_t *mdd_range_mdd ARGS((mdd_manager *mgr, array_t *support));
00347 
00348 /* unsupported */
00349 EXTERN int mdd_bundle_variables ARGS((mdd_manager *mgr, array_t *bundle_vars, char *mdd_var_name, int *mdd_id));
00350 EXTERN mdd_t * mdd_unary_minus_s ARGS((mdd_manager *mgr, int mvar1, int mvar2));
00351 EXTERN array_t * mvar2bdds ARGS((mdd_manager *mgr, array_t *mvars));
00352 #endif