[13] | 1 | #include "mdd.h" |
---|
| 2 | |
---|
| 3 | /* |
---|
| 4 | * MDD Package |
---|
| 5 | * |
---|
| 6 | * $Id: mdd_init.c,v 1.21 2009/04/11 02:07:47 fabio Exp $ |
---|
| 7 | * |
---|
| 8 | * Author: Timothy Kam |
---|
| 9 | * |
---|
| 10 | * Copyright 1992 by the Regents of the University of California. |
---|
| 11 | * |
---|
| 12 | * All rights reserved. Permission to use, copy, modify and distribute |
---|
| 13 | * this software is hereby granted, provided that the above copyright |
---|
| 14 | * notice and this permission notice appear in all copies. This software |
---|
| 15 | * is made available as is, with no warranties. |
---|
| 16 | */ |
---|
| 17 | |
---|
| 18 | int |
---|
| 19 | integer_get_num_of_digits(int value) |
---|
| 20 | { |
---|
| 21 | double x; |
---|
| 22 | int num_of_digits; |
---|
| 23 | |
---|
| 24 | if (value > 0) x = log10((double) value); |
---|
| 25 | else if (value == 0) x = 0; |
---|
| 26 | else fail("mdd_init: internal error, value less than 0\n"); |
---|
| 27 | |
---|
| 28 | /* |
---|
| 29 | * Notice that floor(x) return a double, |
---|
| 30 | * so it needs to be cast into an integer using |
---|
| 31 | * this following expression. |
---|
| 32 | */ |
---|
| 33 | num_of_digits = (int) floor(x) + 1; |
---|
| 34 | |
---|
| 35 | return num_of_digits; |
---|
| 36 | } |
---|
| 37 | |
---|
| 38 | static void |
---|
| 39 | mdd_name_variables( |
---|
| 40 | array_t *mvar_list, |
---|
| 41 | int no_mvars, |
---|
| 42 | array_t **mvar_names_ptr) |
---|
| 43 | { |
---|
| 44 | |
---|
| 45 | char *istr; |
---|
| 46 | int i; |
---|
| 47 | |
---|
| 48 | if (*mvar_names_ptr == NIL(array_t)) { |
---|
| 49 | /* if no variable names are given, use generic naming */ |
---|
| 50 | /* mv_0, mv_1, ... for variable 0, 1, ... */ |
---|
| 51 | *mvar_names_ptr = array_alloc(char *, 0); |
---|
| 52 | for (i=0; i<no_mvars; i++) { |
---|
| 53 | /* compose a name for the mvar */ |
---|
| 54 | istr = ALLOC(char, integer_get_num_of_digits(i + array_n(mvar_list)) + 4); |
---|
| 55 | sprintf(istr, "mv_%d", (i + array_n(mvar_list))); |
---|
| 56 | array_insert_last(char *, *mvar_names_ptr, istr); |
---|
| 57 | |
---|
| 58 | } |
---|
| 59 | } |
---|
| 60 | else { |
---|
| 61 | if (no_mvars != array_n(*mvar_names_ptr)) |
---|
| 62 | fail("mdd_init: inconsistent size of mvar_names\n"); |
---|
| 63 | } |
---|
| 64 | } |
---|
| 65 | |
---|
| 66 | |
---|
| 67 | static void |
---|
| 68 | mdd_record_variables( |
---|
| 69 | mdd_manager *mgr, |
---|
| 70 | int current_vertex_before, |
---|
| 71 | int start_mvar, |
---|
| 72 | int no_mvars, |
---|
| 73 | array_t *mvar_names, |
---|
| 74 | array_t *mvar_values, |
---|
| 75 | array_t *mvar_strides) |
---|
| 76 | { |
---|
| 77 | |
---|
| 78 | array_t *mvar_list = mdd_ret_mvar_list(mgr); |
---|
| 79 | array_t *bvar_list = mdd_ret_bvar_list(mgr); |
---|
| 80 | int stride_count = 1; |
---|
| 81 | int prev_stride = -1; |
---|
| 82 | int current_vertex = current_vertex_before; |
---|
| 83 | int stride, i, j, |
---|
| 84 | bits, n_bytes; |
---|
| 85 | mvar_type mv; |
---|
| 86 | bvar_type bv; |
---|
| 87 | char *name_str, *mv_name; |
---|
| 88 | |
---|
| 89 | #if MDD_VERBOSE |
---|
| 90 | printf("bdd variable insertion ordering: "); |
---|
| 91 | #endif |
---|
| 92 | |
---|
| 93 | /* mvar_values -> mvar_list */ |
---|
| 94 | for (i=0; i<no_mvars; i++) { |
---|
| 95 | mv.mvar_id = start_mvar + i; |
---|
| 96 | |
---|
| 97 | /* compose a name for the mvar */ |
---|
| 98 | name_str = array_fetch(char *, mvar_names, i); |
---|
| 99 | n_bytes = strlen (name_str) + 1; |
---|
| 100 | mv_name = ALLOC(char, n_bytes); |
---|
| 101 | strcpy(mv_name, name_str); |
---|
| 102 | mv.name = mv_name; |
---|
| 103 | |
---|
| 104 | /* register no. of values for the mvar */ |
---|
| 105 | mv.values = array_fetch(int, mvar_values, i); |
---|
| 106 | |
---|
| 107 | /* length of ecoding bits for mvar */ |
---|
| 108 | bits = no_bit_encode(mv.values); |
---|
| 109 | mv.encode_length = bits; |
---|
| 110 | |
---|
| 111 | /* register the starting bdd vertex no. for the mvar */ |
---|
| 112 | mv.bvars = array_alloc(int, 0); |
---|
| 113 | |
---|
| 114 | if (bits > 0) |
---|
| 115 | stride = array_fetch(int, mvar_strides, i); |
---|
| 116 | else |
---|
| 117 | stride = 1; |
---|
| 118 | for(j=0; j<bits; j++) array_insert_last(int, mv.bvars, current_vertex + (j * stride) ); |
---|
| 119 | |
---|
| 120 | |
---|
| 121 | /* create place-holder for bit-encoding of the mvar */ |
---|
| 122 | mv.encoding = ALLOC(int, bits); |
---|
| 123 | |
---|
| 124 | /* create bdd variables and put them in bvar_list */ |
---|
| 125 | for (j=0; j<bits; j++) { |
---|
| 126 | bv.node = bdd_get_variable(mgr, current_vertex + stride*j); |
---|
| 127 | bv.mvar_id = mv.mvar_id; |
---|
| 128 | |
---|
| 129 | #if MDD_VERBOSE |
---|
| 130 | printf("%d ", current_vertex + stride*j); |
---|
| 131 | #endif |
---|
| 132 | |
---|
| 133 | array_insert(bvar_type, bvar_list, current_vertex + stride*j, bv); |
---|
| 134 | } |
---|
| 135 | |
---|
| 136 | /* insert the completed mvar_type element to mvar_list */ |
---|
| 137 | mv.status = MDD_ACTIVE; |
---|
| 138 | array_insert_last(mvar_type, mvar_list, mv); |
---|
| 139 | |
---|
| 140 | if ((prev_stride != -1 ) && (stride != prev_stride)) { |
---|
| 141 | printf("mdd_record_variables: processing %s\n", mv.name); |
---|
| 142 | fail("mdd_record_variables: inconsistency found in mvar_stride\n"); |
---|
| 143 | } |
---|
| 144 | |
---|
| 145 | /* register the stride for mvar interleaving */ |
---|
| 146 | /* and update current bdd vertex count */ |
---|
| 147 | if (stride_count == stride) { |
---|
| 148 | stride_count = 1; |
---|
| 149 | current_vertex = current_vertex + stride*(bits-1) + 1; |
---|
| 150 | prev_stride = -1; |
---|
| 151 | } |
---|
| 152 | else { |
---|
| 153 | stride_count++; |
---|
| 154 | current_vertex++; |
---|
| 155 | prev_stride = stride; |
---|
| 156 | } |
---|
| 157 | } |
---|
| 158 | |
---|
| 159 | #if MDD_VERBOSE |
---|
| 160 | printf("\n"); |
---|
| 161 | #endif |
---|
| 162 | |
---|
| 163 | /* init all encodings to 2's */ |
---|
| 164 | clear_all_marks(mgr); |
---|
| 165 | |
---|
| 166 | #if MONITOR |
---|
| 167 | print_mvar_list(mgr); |
---|
| 168 | (void) printf("%d bdd variables created\n", array_n(bvar_list)); |
---|
| 169 | print_bvar_list_id(mgr); |
---|
| 170 | #endif |
---|
| 171 | |
---|
| 172 | } |
---|
| 173 | |
---|
| 174 | |
---|
| 175 | mdd_manager * |
---|
| 176 | mdd_init( |
---|
| 177 | array_t *mvar_values, |
---|
| 178 | array_t *mvar_names, |
---|
| 179 | array_t *mvar_strides) |
---|
| 180 | { |
---|
| 181 | array_t *mvar_list; |
---|
| 182 | array_t *bvar_list; |
---|
| 183 | int i, no_mvars, current_vertex; |
---|
| 184 | int vertex_sum; |
---|
| 185 | mdd_manager *mgr; |
---|
| 186 | mdd_hook_type *mdd_hook; |
---|
| 187 | bdd_external_hooks *hook; |
---|
| 188 | boolean free_mvar_strides_flag; |
---|
| 189 | boolean free_mvar_names_flag; |
---|
| 190 | |
---|
| 191 | mdd_hook = ALLOC(mdd_hook_type, 1); |
---|
| 192 | |
---|
| 193 | /* global information about all mvar for mdd_manager */ |
---|
| 194 | mvar_list = array_alloc(mvar_type, 0); |
---|
| 195 | |
---|
| 196 | /* global information about all bvar for mdd_manager */ |
---|
| 197 | bvar_list = array_alloc(bvar_type, 0); |
---|
| 198 | |
---|
| 199 | /* create the hook to the bdd_manager */ |
---|
| 200 | mdd_hook->mvar_list = mvar_list; |
---|
| 201 | mdd_hook->bvar_list = bvar_list; |
---|
| 202 | |
---|
| 203 | /* if some array arguments are NIL */ |
---|
| 204 | no_mvars = array_n(mvar_values); |
---|
| 205 | |
---|
| 206 | free_mvar_names_flag = (mvar_names == NIL(array_t)); |
---|
| 207 | mdd_name_variables(mvar_list, no_mvars, &mvar_names); |
---|
| 208 | |
---|
| 209 | /* create mdd manager */ |
---|
| 210 | vertex_sum = 0; |
---|
| 211 | for (i=0; i<no_mvars; i++) { |
---|
| 212 | vertex_sum = vertex_sum + no_bit_encode(array_fetch(int,mvar_values,i)); |
---|
| 213 | } |
---|
| 214 | mgr = bdd_start(vertex_sum); |
---|
| 215 | |
---|
| 216 | hook = bdd_get_external_hooks(mgr); |
---|
| 217 | |
---|
| 218 | hook->mdd = (char *) mdd_hook; |
---|
| 219 | |
---|
| 220 | current_vertex = 0; |
---|
| 221 | |
---|
| 222 | if (mvar_strides == NIL(array_t)) { |
---|
| 223 | /* if no strides are specified, the variables are not interleaved */ |
---|
| 224 | /* i.e. mvar_strides = 1 */ |
---|
| 225 | /* must set a flag to know that this array needs to be freed */ |
---|
| 226 | free_mvar_strides_flag = TRUE; |
---|
| 227 | mvar_strides = array_alloc(int, 0); |
---|
| 228 | for (i=0; i<no_mvars; i++) { |
---|
| 229 | array_insert_last(int, mvar_strides, 1); |
---|
| 230 | } |
---|
| 231 | } |
---|
| 232 | else { |
---|
| 233 | free_mvar_strides_flag = FALSE; |
---|
| 234 | if (no_mvars != array_n(mvar_strides)) |
---|
| 235 | fail("mdd_init: inconsistent size of mvar_strides\n"); |
---|
| 236 | } |
---|
| 237 | |
---|
| 238 | |
---|
| 239 | mdd_record_variables(mgr, current_vertex, 0, no_mvars, mvar_names, mvar_values, mvar_strides); |
---|
| 240 | |
---|
| 241 | if (free_mvar_strides_flag) { |
---|
| 242 | array_free(mvar_strides); |
---|
| 243 | } |
---|
| 244 | |
---|
| 245 | if (free_mvar_names_flag) { |
---|
| 246 | for (i = 0; i < array_n(mvar_names); i++) { |
---|
| 247 | char *name = array_fetch(char *, mvar_names, i); |
---|
| 248 | FREE(name); |
---|
| 249 | } |
---|
| 250 | array_free(mvar_names); |
---|
| 251 | } |
---|
| 252 | |
---|
| 253 | return mgr; |
---|
| 254 | } |
---|
| 255 | |
---|
| 256 | |
---|
| 257 | unsigned int |
---|
| 258 | mdd_create_variables( |
---|
| 259 | mdd_manager *mgr, |
---|
| 260 | array_t *mvar_values, |
---|
| 261 | array_t *mvar_names, |
---|
| 262 | array_t *mvar_strides) |
---|
| 263 | { |
---|
| 264 | array_t *mvar_list = mdd_ret_mvar_list(mgr); |
---|
| 265 | array_t *bvar_list = mdd_ret_bvar_list(mgr); |
---|
| 266 | int i, no_mvars, current_vertex, start_mvar; |
---|
| 267 | int vertex_sum; |
---|
| 268 | bdd_t *temp; |
---|
| 269 | boolean free_mvar_strides_flag; |
---|
| 270 | boolean free_mvar_names_flag; |
---|
| 271 | |
---|
| 272 | |
---|
| 273 | /* if some array arguments are NIL */ |
---|
| 274 | no_mvars = array_n(mvar_values); |
---|
| 275 | |
---|
| 276 | free_mvar_names_flag = (mvar_names == NIL(array_t)); |
---|
| 277 | mdd_name_variables(mvar_list, no_mvars, &mvar_names); |
---|
| 278 | |
---|
| 279 | if (mvar_strides == NIL(array_t)) { |
---|
| 280 | /* if no strides are specified, the variables are not interleaved */ |
---|
| 281 | /* i.e. mvar_strides = 1 */ |
---|
| 282 | /* must set a flag to know that this array needs to be freed */ |
---|
| 283 | free_mvar_strides_flag = TRUE; |
---|
| 284 | mvar_strides = array_alloc(int, 0); |
---|
| 285 | for (i=0; i<no_mvars; i++) { |
---|
| 286 | array_insert_last(int, mvar_strides, 1); |
---|
| 287 | } |
---|
| 288 | } |
---|
| 289 | else { |
---|
| 290 | free_mvar_strides_flag = FALSE; |
---|
| 291 | if (no_mvars != array_n(mvar_strides)) |
---|
| 292 | fail("mdd_init: inconsistent size of mvar_strides\n"); |
---|
| 293 | } |
---|
| 294 | |
---|
| 295 | vertex_sum = 0; |
---|
| 296 | for (i=0; i<no_mvars; i++) { |
---|
| 297 | vertex_sum = vertex_sum + no_bit_encode(array_fetch(int,mvar_values,i)); |
---|
| 298 | } |
---|
| 299 | current_vertex = array_n(bvar_list); |
---|
| 300 | for (i=0; i<vertex_sum; i++) { |
---|
| 301 | temp = bdd_get_variable(mgr, i+current_vertex); |
---|
| 302 | bdd_free(temp); |
---|
| 303 | } |
---|
| 304 | |
---|
| 305 | start_mvar = array_n(mvar_list); |
---|
| 306 | |
---|
| 307 | mdd_record_variables(mgr, current_vertex, start_mvar, no_mvars, mvar_names, mvar_values, mvar_strides); |
---|
| 308 | |
---|
| 309 | if (free_mvar_strides_flag) { |
---|
| 310 | array_free(mvar_strides); |
---|
| 311 | } |
---|
| 312 | |
---|
| 313 | if (free_mvar_names_flag) { |
---|
| 314 | for (i = 0; i < array_n(mvar_names); i++) { |
---|
| 315 | char *name = array_fetch(char *, mvar_names, i); |
---|
| 316 | FREE(name); |
---|
| 317 | } |
---|
| 318 | array_free(mvar_names); |
---|
| 319 | } |
---|
| 320 | |
---|
| 321 | return start_mvar; |
---|
| 322 | } |
---|
| 323 | |
---|
| 324 | |
---|
| 325 | unsigned int |
---|
| 326 | mdd_create_variables_after( |
---|
| 327 | mdd_manager *mgr, |
---|
| 328 | int after_mvar_id, |
---|
| 329 | array_t *mvar_values, |
---|
| 330 | array_t *mvar_names, |
---|
| 331 | array_t *mvar_strides) |
---|
| 332 | { |
---|
| 333 | array_t *mvar_list = mdd_ret_mvar_list(mgr); |
---|
| 334 | array_t *bvar_list = mdd_ret_bvar_list(mgr); |
---|
| 335 | mvar_type after_mv, fol_mv; |
---|
| 336 | int i, no_mvars, current_vertex, start_mvar; |
---|
| 337 | int vertex_sum; |
---|
| 338 | int after_bv_id; |
---|
| 339 | bdd_t *temp; |
---|
| 340 | bvar_type sec_bit_of_mv; |
---|
| 341 | int sec_bit_level, fol_id; |
---|
| 342 | boolean free_mvar_strides_flag; |
---|
| 343 | boolean free_mvar_names_flag; |
---|
| 344 | |
---|
| 345 | after_mv = array_fetch( mvar_type, mvar_list, after_mvar_id ); |
---|
| 346 | |
---|
| 347 | if (after_mv.encode_length > 1) { |
---|
| 348 | sec_bit_of_mv = mdd_ret_bvar(&after_mv, 1, bvar_list); |
---|
| 349 | sec_bit_level = bdd_top_var_level( mgr, sec_bit_of_mv.node ); |
---|
| 350 | /* first_bit_of_last_interleaved_mvar */ |
---|
| 351 | fol_id = bdd_get_id_from_level( mgr, sec_bit_level - 1 ); |
---|
| 352 | } |
---|
| 353 | else |
---|
| 354 | fol_id = mdd_ret_bvar_id(&after_mv, 0); |
---|
| 355 | |
---|
| 356 | fol_mv = array_fetch( mvar_type, mvar_list, fol_id ); |
---|
| 357 | |
---|
| 358 | after_bv_id = mdd_ret_bvar_id(&fol_mv, fol_mv.encode_length - 1); |
---|
| 359 | |
---|
| 360 | /* if some array arguments are NIL */ |
---|
| 361 | no_mvars = array_n(mvar_values); |
---|
| 362 | |
---|
| 363 | free_mvar_names_flag = (mvar_names == NIL(array_t)); |
---|
| 364 | mdd_name_variables(mvar_list, no_mvars, &mvar_names); |
---|
| 365 | |
---|
| 366 | if (mvar_strides == NIL(array_t)) { |
---|
| 367 | /* if no strides are specified, the variables are not interleaved */ |
---|
| 368 | /* i.e. mvar_strides = 1 */ |
---|
| 369 | /* must set a flag to know that this array needs to be freed */ |
---|
| 370 | free_mvar_strides_flag = TRUE; |
---|
| 371 | mvar_strides = array_alloc(int, 0); |
---|
| 372 | for (i=0; i<no_mvars; i++) { |
---|
| 373 | array_insert_last(int, mvar_strides, 1); |
---|
| 374 | } |
---|
| 375 | } |
---|
| 376 | else { |
---|
| 377 | free_mvar_strides_flag = FALSE; |
---|
| 378 | if (no_mvars != array_n(mvar_strides)) |
---|
| 379 | fail("mdd_init: inconsistent size of mvar_strides\n"); |
---|
| 380 | } |
---|
| 381 | |
---|
| 382 | vertex_sum = 0; |
---|
| 383 | for (i=0; i<no_mvars; i++) { |
---|
| 384 | vertex_sum = vertex_sum + no_bit_encode(array_fetch(int,mvar_values,i)); |
---|
| 385 | } |
---|
| 386 | for (i=0; i<vertex_sum; i++) { |
---|
| 387 | temp = bdd_create_variable_after(mgr, after_bv_id + i); |
---|
| 388 | bdd_free(temp); |
---|
| 389 | } |
---|
| 390 | |
---|
| 391 | current_vertex = array_n(bvar_list); |
---|
| 392 | start_mvar = array_n(mvar_list); |
---|
| 393 | |
---|
| 394 | mdd_record_variables(mgr, current_vertex, start_mvar, no_mvars, mvar_names, mvar_values, mvar_strides); |
---|
| 395 | |
---|
| 396 | if (free_mvar_strides_flag) { |
---|
| 397 | array_free(mvar_strides); |
---|
| 398 | } |
---|
| 399 | |
---|
| 400 | if (free_mvar_names_flag) { |
---|
| 401 | for (i = 0; i < array_n(mvar_names); i++) { |
---|
| 402 | char *name = array_fetch(char *, mvar_names, i); |
---|
| 403 | FREE(name); |
---|
| 404 | } |
---|
| 405 | array_free(mvar_names); |
---|
| 406 | } |
---|
| 407 | |
---|
| 408 | return start_mvar; |
---|
| 409 | |
---|
| 410 | } |
---|
| 411 | |
---|
| 412 | |
---|
| 413 | unsigned int |
---|
| 414 | mdd_create_variables_interleaved( |
---|
| 415 | mdd_manager *mgr, |
---|
| 416 | int inter_var_id, |
---|
| 417 | int no_mvars, |
---|
| 418 | array_t *mvar_names) |
---|
| 419 | { |
---|
| 420 | array_t *mvar_list = mdd_ret_mvar_list(mgr); |
---|
| 421 | array_t *bvar_list = mdd_ret_bvar_list(mgr); |
---|
| 422 | mvar_type inter_var; |
---|
| 423 | int i, j, current_vertex, start_mvar; |
---|
| 424 | bdd_t *temp; |
---|
| 425 | array_t *mvar_values; |
---|
| 426 | array_t *mvar_strides; |
---|
| 427 | boolean free_mvar_names_flag; |
---|
| 428 | |
---|
| 429 | inter_var = array_fetch( mvar_type, mvar_list, inter_var_id ); |
---|
| 430 | |
---|
| 431 | /* if some array arguments are NIL */ |
---|
| 432 | free_mvar_names_flag = (mvar_names == NIL(array_t)); |
---|
| 433 | mdd_name_variables(mvar_list, no_mvars, &mvar_names); |
---|
| 434 | |
---|
| 435 | |
---|
| 436 | for (j=0; j<inter_var.encode_length; j++) { |
---|
| 437 | for (i=0; i<no_mvars; i++) { |
---|
| 438 | temp = bdd_create_variable_after( mgr, mdd_ret_bvar_id(&inter_var, j) ); |
---|
| 439 | bdd_free( temp ); |
---|
| 440 | } |
---|
| 441 | } |
---|
| 442 | |
---|
| 443 | current_vertex = array_n(bvar_list); |
---|
| 444 | start_mvar = array_n(mvar_list); |
---|
| 445 | |
---|
| 446 | mvar_values = array_alloc(int, 0); |
---|
| 447 | mvar_strides = array_alloc(int, 0); |
---|
| 448 | for(i=0; i<no_mvars; i++) { |
---|
| 449 | array_insert_last(int, mvar_values, inter_var.values); |
---|
| 450 | array_insert_last(int, mvar_strides, no_mvars); |
---|
| 451 | } |
---|
| 452 | |
---|
| 453 | mdd_record_variables(mgr, current_vertex, start_mvar, no_mvars, mvar_names, mvar_values, mvar_strides); |
---|
| 454 | |
---|
| 455 | array_free(mvar_values); |
---|
| 456 | array_free(mvar_strides); |
---|
| 457 | |
---|
| 458 | if (free_mvar_names_flag) { |
---|
| 459 | for (i = 0; i < array_n(mvar_names); i++) { |
---|
| 460 | char *name = array_fetch(char *, mvar_names, i); |
---|
| 461 | FREE(name); |
---|
| 462 | } |
---|
| 463 | array_free(mvar_names); |
---|
| 464 | } |
---|
| 465 | |
---|
| 466 | return start_mvar; |
---|
| 467 | } |
---|
| 468 | |
---|
| 469 | |
---|
| 470 | void |
---|
| 471 | mdd_array_free(array_t *mddArray) |
---|
| 472 | { |
---|
| 473 | int i; |
---|
| 474 | |
---|
| 475 | if (mddArray != NIL(array_t)) { |
---|
| 476 | for (i = 0; i < array_n(mddArray); i++) { |
---|
| 477 | mdd_t *tempMdd = array_fetch(mdd_t *, mddArray, i); |
---|
| 478 | mdd_free(tempMdd); |
---|
| 479 | } |
---|
| 480 | array_free(mddArray); |
---|
| 481 | } |
---|
| 482 | } |
---|
| 483 | |
---|
| 484 | void |
---|
| 485 | mdd_array_array_free(array_t *arrayBddArray) |
---|
| 486 | { |
---|
| 487 | int i; |
---|
| 488 | array_t *bddArray; |
---|
| 489 | |
---|
| 490 | if (arrayBddArray != NIL(array_t)) { |
---|
| 491 | for (i = 0; i < array_n(arrayBddArray); i++) { |
---|
| 492 | bddArray = array_fetch(array_t *, arrayBddArray, i); |
---|
| 493 | mdd_array_free(bddArray); |
---|
| 494 | } |
---|
| 495 | array_free(arrayBddArray); |
---|
| 496 | } |
---|
| 497 | } |
---|
| 498 | |
---|
| 499 | array_t * |
---|
| 500 | mdd_array_duplicate(array_t *mddArray) |
---|
| 501 | { |
---|
| 502 | int i; |
---|
| 503 | int length = array_n(mddArray); |
---|
| 504 | array_t *result = array_alloc(mdd_t *, length); |
---|
| 505 | for (i = 0; i < length; i++) { |
---|
| 506 | mdd_t *tempMdd = array_fetch(mdd_t *, mddArray, i); |
---|
| 507 | array_insert(mdd_t *, result, i, mdd_dup(tempMdd)); |
---|
| 508 | } |
---|
| 509 | |
---|
| 510 | return (result); |
---|
| 511 | } |
---|
| 512 | |
---|
| 513 | |
---|
| 514 | /* Return true iff two arrays of mdds are identical, i.e., they contain |
---|
| 515 | identical mdds in the same order */ |
---|
| 516 | boolean |
---|
| 517 | mdd_array_equal(array_t *array1, array_t *array2) |
---|
| 518 | { |
---|
| 519 | int i; |
---|
| 520 | |
---|
| 521 | assert(array1 != NIL(array_t) && array2 != NIL(array_t)); |
---|
| 522 | |
---|
| 523 | if(array_n(array1) != array_n(array2)) |
---|
| 524 | return FALSE; |
---|
| 525 | |
---|
| 526 | for(i = 0; i < array_n(array1); i++) { |
---|
| 527 | mdd_t *mdd1 = array_fetch(mdd_t *, array1, i); |
---|
| 528 | mdd_t *mdd2 = array_fetch(mdd_t *, array2, i); |
---|
| 529 | if(!mdd_equal(mdd1, mdd2)) |
---|
| 530 | return FALSE; |
---|
| 531 | } |
---|
| 532 | |
---|
| 533 | return TRUE; |
---|
| 534 | } |
---|
| 535 | |
---|
| 536 | /* wrapper for mdd_init, to create a manager with no variables */ |
---|
| 537 | mdd_manager * |
---|
| 538 | mdd_init_empty(void) |
---|
| 539 | { |
---|
| 540 | array_t *empty_array = array_alloc(int, 0); |
---|
| 541 | mdd_manager *mdd_mgr = mdd_init(empty_array, NIL(array_t), NIL(array_t)); |
---|
| 542 | |
---|
| 543 | array_free(empty_array); |
---|
| 544 | return mdd_mgr; |
---|
| 545 | } |
---|
| 546 | |
---|
| 547 | /* This function re-encodes an MDD variable when a BDD variable in |
---|
| 548 | its encoding has a fixed value. |
---|
| 549 | */ |
---|
| 550 | void |
---|
| 551 | mdd_var_expunge_bdd_variable( |
---|
| 552 | mdd_manager *mgr /* MDD manager */, |
---|
| 553 | int bddId /* variable that has constant value */, |
---|
| 554 | int val /* value at which variable is fixed */ |
---|
| 555 | ) |
---|
| 556 | { |
---|
| 557 | array_t *mvar_list = mdd_ret_mvar_list(mgr); |
---|
| 558 | array_t *bvar_list = mdd_ret_bvar_list(mgr); |
---|
| 559 | array_t *bvars; |
---|
| 560 | |
---|
| 561 | bvar_type bddVar; |
---|
| 562 | mvar_type mvVar; |
---|
| 563 | int position, i, id, shift, values; |
---|
| 564 | |
---|
| 565 | /* Check arguments. */ |
---|
| 566 | if (val != 0 && val != 1) fail("value must be either 0 or 1"); |
---|
| 567 | if (bddId < 0 || bddId >= array_n(bvar_list)) fail("bddId out of range"); |
---|
| 568 | |
---|
| 569 | /* Extract info. */ |
---|
| 570 | bddVar = array_fetch(bvar_type, bvar_list, bddId); |
---|
| 571 | mvVar = array_fetch(mvar_type, mvar_list, bddVar.mvar_id); |
---|
| 572 | bvars = array_alloc(int,array_n(mvVar.bvars)-1); |
---|
| 573 | |
---|
| 574 | /* Expunge fixed variable from list of BDD variables. */ |
---|
| 575 | position = array_n(mvVar.bvars); /* initialization for later checking */ |
---|
| 576 | arrayForEachItem(int, mvVar.bvars, i, id) { |
---|
| 577 | if (id != bddId) |
---|
| 578 | array_insert_last(int, bvars, id); |
---|
| 579 | else |
---|
| 580 | position = i; |
---|
| 581 | } |
---|
| 582 | /* Make sure we wrote position in the loop. */ |
---|
| 583 | assert(position < array_n(mvVar.bvars)); |
---|
| 584 | |
---|
| 585 | /* Count number of surviving values. */ |
---|
| 586 | shift = (mvVar.encode_length - position - 1); |
---|
| 587 | |
---|
| 588 | for (i = 0, values = 0; i < mvVar.values; i++) { |
---|
| 589 | values += (i >> shift) ^ ~val; |
---|
| 590 | } |
---|
| 591 | |
---|
| 592 | /* Update mvar_list */ |
---|
| 593 | array_free(mvVar.bvars); |
---|
| 594 | mvVar.bvars = bvars; |
---|
| 595 | mvVar.values = values; |
---|
| 596 | mvVar.encode_length--; |
---|
| 597 | array_insert(mvar_type, mvar_list, bddVar.mvar_id, mvVar); |
---|
| 598 | |
---|
| 599 | /* Update bvar_list. */ |
---|
| 600 | bvar_type bv = array_fetch(bvar_type, bvar_list, bddId); |
---|
| 601 | bv.mvar_id = -1; |
---|
| 602 | array_insert(bvar_type, bvar_list, bddId, bv); |
---|
| 603 | |
---|
| 604 | } /* mdd_var_expunge_bdd_variable */ |
---|
| 605 | |
---|
| 606 | /*---------------------------------------------------------------------------*/ |
---|
| 607 | /* Static function prototypes */ |
---|
| 608 | /*---------------------------------------------------------------------------*/ |
---|