[13] | 1 | #include "mdd.h" |
---|
| 2 | |
---|
| 3 | /* |
---|
| 4 | * MDD Package |
---|
| 5 | * |
---|
| 6 | * $Id: mdd_iter.c,v 1.8 2002/08/27 16:30:26 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 | /* this routine returns the first minterm (2's in cube becomes 0's), */ |
---|
| 19 | /* given an mdd generator, containing a cube and a list of variables */ |
---|
| 20 | /* to be included in the minterm */ |
---|
| 21 | |
---|
| 22 | static array_t * |
---|
| 23 | first_minterm(mdd_gen *mgen) |
---|
| 24 | { |
---|
| 25 | array_t *minterm; |
---|
| 26 | bdd_literal literal; |
---|
| 27 | int i, j; |
---|
| 28 | |
---|
| 29 | array_t *mvar_list = mdd_ret_mvar_list(mgen->manager); |
---|
| 30 | int mv_id; |
---|
| 31 | mvar_type mv; |
---|
| 32 | boolean out_of_range; /* a minterm is out of range if one variable is */ |
---|
| 33 | array_t *solution; |
---|
| 34 | int value; |
---|
| 35 | |
---|
| 36 | out_of_range = 0; |
---|
| 37 | |
---|
| 38 | minterm = array_alloc(bdd_literal, 0); |
---|
| 39 | solution = array_alloc(int, 0); |
---|
| 40 | /* loop once for each mvar */ |
---|
| 41 | for (i=0; i<array_n(mgen->var_list); i++) { |
---|
| 42 | mv_id = array_fetch(int, mgen->var_list, i); |
---|
| 43 | mv = array_fetch(mvar_type, mvar_list, mv_id); |
---|
| 44 | /* loop for each bvar */ |
---|
| 45 | value = 0; |
---|
| 46 | for (j=0; j<mv.encode_length; j++) { |
---|
| 47 | literal = array_fetch(bdd_literal, mgen->cube, mdd_ret_bvar_id(&mv, j) ); |
---|
| 48 | if (literal == 0) { |
---|
| 49 | array_insert_last(bdd_literal, minterm, 0); |
---|
| 50 | value = value*2 + 0; |
---|
| 51 | } |
---|
| 52 | else if (literal == 1) { |
---|
| 53 | array_insert_last(bdd_literal, minterm, 1); |
---|
| 54 | value = value*2 + 1; |
---|
| 55 | } |
---|
| 56 | else { /*if (literal == 2) */ |
---|
| 57 | array_insert_last(bdd_literal, minterm, 0); |
---|
| 58 | value = value*2 + 0; |
---|
| 59 | } |
---|
| 60 | } |
---|
| 61 | (void) array_insert_last(int, solution, value); |
---|
| 62 | if (value >= mv.values) out_of_range = 1; |
---|
| 63 | } |
---|
| 64 | mgen->minterm = minterm; |
---|
| 65 | mgen->out_of_range = out_of_range; |
---|
| 66 | |
---|
| 67 | return (solution); |
---|
| 68 | } |
---|
| 69 | |
---|
| 70 | |
---|
| 71 | /* this routine returns the next minterm, given a current minterm, */ |
---|
| 72 | /* a cube and a list of variables to be included in the minterm */ |
---|
| 73 | /* if no more, return NIL(array_t). */ |
---|
| 74 | |
---|
| 75 | static array_t * |
---|
| 76 | next_minterm(mdd_gen *mgen) |
---|
| 77 | { |
---|
| 78 | int carry; |
---|
| 79 | int i, j, k; |
---|
| 80 | array_t *minterm; |
---|
| 81 | bdd_literal literal; |
---|
| 82 | bdd_literal prev_literal; |
---|
| 83 | array_t *mvar_list = mdd_ret_mvar_list(mgen->manager); |
---|
| 84 | int mv_id; |
---|
| 85 | mvar_type mv; |
---|
| 86 | boolean out_of_range; |
---|
| 87 | array_t *solution; |
---|
| 88 | int value; |
---|
| 89 | |
---|
| 90 | out_of_range = 0; |
---|
| 91 | |
---|
| 92 | carry = 1; |
---|
| 93 | k = 0; |
---|
| 94 | |
---|
| 95 | minterm = array_alloc(bdd_literal, array_n(mgen->minterm)); |
---|
| 96 | solution = array_alloc(int, 0); |
---|
| 97 | /* loop once for each mvar */ |
---|
| 98 | for (i=0; i<array_n(mgen->var_list); i++) { |
---|
| 99 | mv_id = array_fetch(int, mgen->var_list, i); |
---|
| 100 | mv = array_fetch(mvar_type, mvar_list, mv_id); |
---|
| 101 | value = 0; |
---|
| 102 | /* loop for each bvar */ |
---|
| 103 | for (j=0; j<mv.encode_length; j++) { |
---|
| 104 | literal = array_fetch(bdd_literal, mgen->cube, mdd_ret_bvar_id(&mv, j) ); |
---|
| 105 | |
---|
| 106 | prev_literal = array_fetch(bdd_literal, mgen->minterm, k); |
---|
| 107 | if ((literal == 2) && (carry == 1)) { |
---|
| 108 | if (prev_literal == 0) { |
---|
| 109 | array_insert(bdd_literal, minterm, k, 1); |
---|
| 110 | carry = 0; |
---|
| 111 | value = value*2 + 1; |
---|
| 112 | } |
---|
| 113 | else if (prev_literal == 1) { |
---|
| 114 | array_insert(bdd_literal, minterm, k, 0); |
---|
| 115 | carry = 1; |
---|
| 116 | value = value*2 + 0; |
---|
| 117 | } |
---|
| 118 | } |
---|
| 119 | else if ((literal == 2) && (carry == 0)) { |
---|
| 120 | array_insert(bdd_literal, minterm, k, prev_literal); |
---|
| 121 | value = value*2 + prev_literal; |
---|
| 122 | } |
---|
| 123 | else { /* if literal == 0 or 1 */ |
---|
| 124 | array_insert(bdd_literal, minterm, k, literal); |
---|
| 125 | value = value*2 + literal; |
---|
| 126 | } |
---|
| 127 | k++; |
---|
| 128 | } |
---|
| 129 | array_insert_last(int, solution, value); |
---|
| 130 | if (value >= mv.values) out_of_range = 1; |
---|
| 131 | } |
---|
| 132 | |
---|
| 133 | if (carry == 1) { |
---|
| 134 | /* no more minterms */ |
---|
| 135 | array_free(minterm); |
---|
| 136 | minterm = NIL(array_t); |
---|
| 137 | array_free(solution); |
---|
| 138 | solution = NIL(array_t); |
---|
| 139 | } |
---|
| 140 | array_free(mgen->minterm); |
---|
| 141 | mgen->minterm = minterm; |
---|
| 142 | mgen->out_of_range = out_of_range; |
---|
| 143 | |
---|
| 144 | return (solution); |
---|
| 145 | } |
---|
| 146 | |
---|
| 147 | |
---|
| 148 | static array_t * |
---|
| 149 | next_valid_minterm(mdd_gen *mgen) |
---|
| 150 | { |
---|
| 151 | array_t *solution; |
---|
| 152 | array_t *cube; |
---|
| 153 | |
---|
| 154 | solution = next_minterm(mgen); |
---|
| 155 | |
---|
| 156 | /* check if done with current cube */ |
---|
| 157 | if (mgen->minterm == NIL(array_t)) { |
---|
| 158 | (void) bdd_next_cube(mgen->bdd_generator, &cube); |
---|
| 159 | mgen->status = bdd_gen_read_status(mgen->bdd_generator); |
---|
| 160 | mgen->cube = cube; |
---|
| 161 | if (mgen->status != bdd_EMPTY) { |
---|
| 162 | if (solution != NIL(array_t) ) array_free(solution); |
---|
| 163 | solution = first_minterm(mgen); |
---|
| 164 | } |
---|
| 165 | else { |
---|
| 166 | mgen->minterm = NIL(array_t); |
---|
| 167 | mgen->cube = NIL(array_t); |
---|
| 168 | } |
---|
| 169 | } |
---|
| 170 | return (solution); |
---|
| 171 | } |
---|
| 172 | |
---|
| 173 | |
---|
| 174 | mdd_gen * |
---|
| 175 | mdd_first_minterm( |
---|
| 176 | mdd_t *f, |
---|
| 177 | array_t **solution_p /* minterm = array of values */, |
---|
| 178 | array_t *variable_list) |
---|
| 179 | { |
---|
| 180 | mdd_gen *mgen; /* mdd generator */ |
---|
| 181 | bdd_gen *bgen; /* bdd generator for bdd_first_cube, bdd_next_cube */ |
---|
| 182 | array_t *cube; /* array of literals {0,1,2} */ |
---|
| 183 | array_t *allvar_list; |
---|
| 184 | array_t *mvar_list; |
---|
| 185 | array_t *smoothing_list; |
---|
| 186 | int i, j, k; |
---|
| 187 | array_t *solution = NIL(array_t); /* initialize for lint */ |
---|
| 188 | array_t *var_list; |
---|
| 189 | boolean i_is_present; |
---|
| 190 | mdd_t *mdd_tmp, *f_copy; |
---|
| 191 | bdd_manager *mgr; |
---|
| 192 | |
---|
| 193 | if ( f != NIL(mdd_t) ) { |
---|
| 194 | /* new code added by Timothy */ |
---|
| 195 | /* f is first smoothed by all variables NOT present in var_list */ |
---|
| 196 | |
---|
| 197 | f_copy = mdd_dup(f); |
---|
| 198 | |
---|
| 199 | smoothing_list = array_alloc(int, 0); |
---|
| 200 | |
---|
| 201 | |
---|
| 202 | mgr = bdd_get_manager(f_copy); |
---|
| 203 | mvar_list = mdd_ret_mvar_list(mgr); |
---|
| 204 | |
---|
| 205 | for (i = 0; i < array_n(mvar_list); i++) { |
---|
| 206 | i_is_present = FALSE; |
---|
| 207 | for (j = 0; j < array_n(variable_list); j++) { |
---|
| 208 | k = array_fetch(int, variable_list, j); |
---|
| 209 | if (k == i) i_is_present = TRUE; |
---|
| 210 | } |
---|
| 211 | if (i_is_present == FALSE) array_insert_last(int, smoothing_list, i); |
---|
| 212 | } |
---|
| 213 | if (array_n(smoothing_list) > 0) { |
---|
| 214 | mdd_tmp = mdd_smooth(mgr, f_copy, smoothing_list); |
---|
| 215 | (void) mdd_free(f_copy); |
---|
| 216 | f_copy = mdd_dup(mdd_tmp); |
---|
| 217 | (void) mdd_free(mdd_tmp); |
---|
| 218 | |
---|
| 219 | } |
---|
| 220 | |
---|
| 221 | (void) array_free(smoothing_list); |
---|
| 222 | |
---|
| 223 | bgen = bdd_first_cube(f_copy, &cube); |
---|
| 224 | (void) mdd_free(f_copy); |
---|
| 225 | |
---|
| 226 | mgen = ALLOC(mdd_gen, 1); |
---|
| 227 | mgen->manager = mgr; |
---|
| 228 | mgen->bdd_generator = bgen; |
---|
| 229 | mgen->status = bdd_gen_read_status(mgen->bdd_generator); |
---|
| 230 | mgen->cube = cube; /* store in mdd gen for later use */ |
---|
| 231 | mgen->out_of_range = 0; |
---|
| 232 | if (mgen->status != bdd_EMPTY) { |
---|
| 233 | if (variable_list != NIL(array_t)) { |
---|
| 234 | var_list = array_dup(variable_list); |
---|
| 235 | mgen->var_list = var_list; |
---|
| 236 | } |
---|
| 237 | else { |
---|
| 238 | allvar_list = array_alloc(int, 0); |
---|
| 239 | for (i=0; i<array_n(mvar_list); i++) |
---|
| 240 | array_insert_last(int, allvar_list, i); |
---|
| 241 | mgen->var_list = allvar_list; |
---|
| 242 | } |
---|
| 243 | solution = first_minterm(mgen); |
---|
| 244 | while (mgen->out_of_range) { |
---|
| 245 | array_free(solution); |
---|
| 246 | solution = next_valid_minterm(mgen); |
---|
| 247 | } |
---|
| 248 | } |
---|
| 249 | else { |
---|
| 250 | |
---|
| 251 | /* mgen->status == bdd_EMPTY */ |
---|
| 252 | if (variable_list != NIL(array_t)) { |
---|
| 253 | var_list = array_dup(variable_list); |
---|
| 254 | mgen->var_list = var_list; |
---|
| 255 | } |
---|
| 256 | else { |
---|
| 257 | allvar_list = array_alloc(int, 0); |
---|
| 258 | for (i=0; i<array_n(mvar_list); i++) |
---|
| 259 | array_insert_last(int, allvar_list, i); |
---|
| 260 | mgen->var_list = allvar_list; |
---|
| 261 | } |
---|
| 262 | |
---|
| 263 | mgen->minterm = NIL(array_t); |
---|
| 264 | mgen->cube = NIL(array_t); |
---|
| 265 | /* previous solution will not be freed here */ |
---|
| 266 | /* but by the calling procedure */ |
---|
| 267 | } |
---|
| 268 | *solution_p = solution; |
---|
| 269 | } |
---|
| 270 | else /* f = NIL */{ |
---|
| 271 | mgen = ALLOC(mdd_gen, 1); |
---|
| 272 | mgen->manager = NIL(mdd_manager); |
---|
| 273 | mgen->bdd_generator = NIL(bdd_gen); |
---|
| 274 | mgen->status = bdd_EMPTY; |
---|
| 275 | mgen->cube = NIL(array_t); |
---|
| 276 | mgen->minterm = NIL(array_t); |
---|
| 277 | mgen->out_of_range = 0; |
---|
| 278 | mgen->var_list = NIL(array_t); |
---|
| 279 | } |
---|
| 280 | |
---|
| 281 | return (mgen); |
---|
| 282 | } |
---|
| 283 | |
---|
| 284 | |
---|
| 285 | boolean |
---|
| 286 | mdd_next_minterm( |
---|
| 287 | mdd_gen *mgen, |
---|
| 288 | array_t **solution_p /* minterm = array of values */) |
---|
| 289 | { |
---|
| 290 | array_t *solution; |
---|
| 291 | solution = next_valid_minterm(mgen); |
---|
| 292 | while ((mgen->out_of_range) && (mgen->status != bdd_EMPTY)) { |
---|
| 293 | array_free(solution); |
---|
| 294 | solution = next_valid_minterm(mgen); |
---|
| 295 | } |
---|
| 296 | *solution_p = solution; |
---|
| 297 | if (mgen->status != bdd_EMPTY) |
---|
| 298 | return (1); |
---|
| 299 | else |
---|
| 300 | return (0); |
---|
| 301 | } |
---|
| 302 | |
---|
| 303 | |
---|
| 304 | void |
---|
| 305 | mdd_print_array(array_t *array) |
---|
| 306 | { |
---|
| 307 | int i, value; |
---|
| 308 | for (i=0; i<array_n(array); i++) { |
---|
| 309 | value = array_fetch(int, array, i); |
---|
| 310 | printf("%d ",value); |
---|
| 311 | } |
---|
| 312 | printf("\n"); |
---|
| 313 | } |
---|
| 314 | |
---|
| 315 | |
---|
| 316 | int |
---|
| 317 | mdd_gen_free(mdd_gen *mgen) |
---|
| 318 | { |
---|
| 319 | if (mgen->minterm != NIL(array_t)) array_free(mgen->minterm); |
---|
| 320 | /* if (mgen->cube != NIL(array_t)) array_free(mgen->cube); */ |
---|
| 321 | /* mgen->cube gets freed in bdd_gen_free(mgen->bdd_generator) below */ |
---|
| 322 | if (mgen->var_list != NIL(array_t)) array_free(mgen->var_list); |
---|
| 323 | bdd_gen_free(mgen->bdd_generator); |
---|
| 324 | FREE(mgen); |
---|
| 325 | |
---|
| 326 | return (0); |
---|
| 327 | } |
---|
| 328 | |
---|
| 329 | /*---------------------------------------------------------------------------*/ |
---|
| 330 | /* Static function prototypes */ |
---|
| 331 | /*---------------------------------------------------------------------------*/ |
---|
| 332 | |
---|