src/mdd/mdd_iter.c File Reference

#include "mdd.h"
Include dependency graph for mdd_iter.c:

Go to the source code of this file.

Functions

static array_t * first_minterm (mdd_gen *mgen)
static array_t * next_minterm (mdd_gen *mgen)
static array_t * next_valid_minterm (mdd_gen *mgen)
mdd_gen * mdd_first_minterm (mdd_t *f, array_t **solution_p, array_t *variable_list)
boolean mdd_next_minterm (mdd_gen *mgen, array_t **solution_p)
void mdd_print_array (array_t *array)
int mdd_gen_free (mdd_gen *mgen)

Function Documentation

static array_t* first_minterm ( mdd_gen *  mgen  )  [static]

Definition at line 23 of file mdd_iter.c.

00024 {
00025     array_t *minterm;
00026     bdd_literal literal;
00027     int i, j;
00028 
00029     array_t *mvar_list = mdd_ret_mvar_list(mgen->manager);
00030     int mv_id;
00031     mvar_type mv;
00032     boolean out_of_range;  /* a minterm is out of range if one variable is */
00033     array_t *solution;
00034     int value;
00035 
00036     out_of_range = 0;
00037                                                                                 
00038     minterm = array_alloc(bdd_literal, 0);
00039     solution = array_alloc(int, 0);
00040     /* loop once for each mvar */
00041     for (i=0; i<array_n(mgen->var_list); i++) {
00042         mv_id = array_fetch(int, mgen->var_list, i);
00043         mv = array_fetch(mvar_type, mvar_list, mv_id);
00044         /* loop for each bvar */
00045         value = 0;
00046         for (j=0; j<mv.encode_length; j++) {
00047             literal = array_fetch(bdd_literal, mgen->cube, mdd_ret_bvar_id(&mv, j) ); 
00048             if (literal == 0) {
00049                 array_insert_last(bdd_literal, minterm, 0);
00050                 value = value*2 + 0;
00051             }
00052             else if (literal == 1) {
00053                 array_insert_last(bdd_literal, minterm, 1);
00054                 value = value*2 + 1;
00055             }
00056             else { /*if (literal == 2) */
00057                 array_insert_last(bdd_literal, minterm, 0);
00058                 value = value*2 + 0;
00059             }
00060         }
00061         (void) array_insert_last(int, solution, value);
00062         if (value >= mv.values) out_of_range = 1;
00063     }
00064     mgen->minterm = minterm;
00065     mgen->out_of_range = out_of_range;
00066 
00067     return (solution);
00068 }

mdd_gen* mdd_first_minterm ( mdd_t *  f,
array_t **  solution_p,
array_t *  variable_list 
)

Definition at line 175 of file mdd_iter.c.

00179 {
00180     mdd_gen *mgen;      /* mdd generator */
00181     bdd_gen *bgen;      /* bdd generator for bdd_first_cube, bdd_next_cube */
00182     array_t *cube;      /* array of literals {0,1,2} */
00183     array_t *allvar_list; 
00184     array_t *mvar_list;
00185     array_t *smoothing_list;
00186     int i, j, k;
00187     array_t *solution = NIL(array_t); /* initialize for lint */
00188     array_t *var_list;
00189     boolean i_is_present;
00190     mdd_t *mdd_tmp, *f_copy;
00191     bdd_manager *mgr;
00192 
00193     if ( f != NIL(mdd_t) ) {
00194         /* new code added by Timothy */
00195         /* f is first smoothed by all variables NOT present in var_list */
00196 
00197         f_copy = mdd_dup(f); 
00198 
00199         smoothing_list = array_alloc(int, 0);
00200     
00201     
00202         mgr = bdd_get_manager(f_copy);
00203         mvar_list = mdd_ret_mvar_list(mgr);                                                                           
00204 
00205         for (i = 0; i < array_n(mvar_list); i++) {
00206             i_is_present = FALSE;
00207             for (j = 0; j < array_n(variable_list); j++) {
00208                 k = array_fetch(int, variable_list, j);
00209                 if (k == i) i_is_present = TRUE;
00210             }
00211             if (i_is_present == FALSE) array_insert_last(int, smoothing_list, i);
00212         }
00213         if (array_n(smoothing_list) > 0) {
00214             mdd_tmp = mdd_smooth(mgr, f_copy, smoothing_list);
00215             (void) mdd_free(f_copy);
00216             f_copy = mdd_dup(mdd_tmp);
00217             (void) mdd_free(mdd_tmp);
00218     
00219         }
00220 
00221         (void) array_free(smoothing_list);
00222 
00223         bgen = bdd_first_cube(f_copy, &cube);
00224         (void) mdd_free(f_copy);
00225     
00226         mgen = ALLOC(mdd_gen, 1);
00227         mgen->manager = mgr;
00228         mgen->bdd_generator = bgen;
00229         mgen->status = bdd_gen_read_status(mgen->bdd_generator);
00230         mgen->cube = cube;              /* store in mdd gen for later use */
00231         mgen->out_of_range = 0;
00232         if (mgen->status != bdd_EMPTY) {
00233             if (variable_list != NIL(array_t)) {
00234                 var_list = array_dup(variable_list);
00235                 mgen->var_list = var_list;
00236             }
00237             else {
00238                 allvar_list = array_alloc(int, 0);
00239                 for (i=0; i<array_n(mvar_list); i++) 
00240                     array_insert_last(int, allvar_list, i);
00241                 mgen->var_list = allvar_list;
00242             }
00243             solution = first_minterm(mgen);
00244             while (mgen->out_of_range) {
00245                 array_free(solution);
00246                 solution = next_valid_minterm(mgen);
00247             }
00248         }
00249         else {
00250 
00251             /* mgen->status == bdd_EMPTY */
00252             if (variable_list != NIL(array_t)) {
00253                 var_list = array_dup(variable_list);
00254                 mgen->var_list = var_list;
00255             }
00256             else {
00257                 allvar_list = array_alloc(int, 0);
00258                 for (i=0; i<array_n(mvar_list); i++)
00259                     array_insert_last(int, allvar_list, i);
00260                 mgen->var_list = allvar_list;
00261             }
00262 
00263             mgen->minterm = NIL(array_t);
00264             mgen->cube = NIL(array_t);
00265             /* previous solution will not be freed here */
00266             /* but by the calling procedure */
00267         }
00268         *solution_p = solution;
00269     }
00270     else /* f = NIL */{
00271       mgen = ALLOC(mdd_gen, 1);
00272       mgen->manager = NIL(mdd_manager);
00273       mgen->bdd_generator = NIL(bdd_gen);
00274       mgen->status = bdd_EMPTY;
00275       mgen->cube = NIL(array_t);
00276       mgen->minterm = NIL(array_t);
00277       mgen->out_of_range = 0;
00278       mgen->var_list = NIL(array_t);
00279     }
00280 
00281     return (mgen);
00282 }

int mdd_gen_free ( mdd_gen *  mgen  ) 

Definition at line 317 of file mdd_iter.c.

00318 {
00319     if (mgen->minterm != NIL(array_t)) array_free(mgen->minterm);
00320 /*  if (mgen->cube != NIL(array_t)) array_free(mgen->cube); */
00321 /*  mgen->cube gets freed in bdd_gen_free(mgen->bdd_generator) below */
00322     if (mgen->var_list != NIL(array_t)) array_free(mgen->var_list);
00323     bdd_gen_free(mgen->bdd_generator);
00324     FREE(mgen);
00325 
00326     return (0);
00327 }

boolean mdd_next_minterm ( mdd_gen *  mgen,
array_t **  solution_p 
)

Definition at line 286 of file mdd_iter.c.

00289 {
00290     array_t *solution;
00291     solution = next_valid_minterm(mgen);
00292     while ((mgen->out_of_range) && (mgen->status != bdd_EMPTY)) {
00293         array_free(solution);
00294         solution = next_valid_minterm(mgen);
00295     }
00296     *solution_p = solution;
00297     if (mgen->status != bdd_EMPTY)
00298         return (1);
00299     else
00300         return (0);
00301 }

void mdd_print_array ( array_t *  array  ) 

Definition at line 305 of file mdd_iter.c.

00306 {
00307     int i, value;
00308     for (i=0; i<array_n(array); i++) {
00309         value = array_fetch(int, array, i);
00310         printf("%d ",value);
00311     }
00312     printf("\n");
00313 }

static array_t* next_minterm ( mdd_gen *  mgen  )  [static]

Definition at line 76 of file mdd_iter.c.

00077 {
00078     int carry;
00079     int i, j, k;
00080     array_t *minterm;
00081     bdd_literal literal;
00082     bdd_literal prev_literal;
00083     array_t *mvar_list = mdd_ret_mvar_list(mgen->manager);
00084     int mv_id;
00085     mvar_type mv;
00086     boolean out_of_range;
00087     array_t *solution;
00088     int value;
00089 
00090     out_of_range = 0;
00091 
00092     carry = 1;
00093     k = 0;
00094 
00095     minterm = array_alloc(bdd_literal, array_n(mgen->minterm)); 
00096     solution = array_alloc(int, 0);
00097     /* loop once for each mvar */
00098     for (i=0; i<array_n(mgen->var_list); i++) {
00099         mv_id = array_fetch(int, mgen->var_list, i);
00100         mv = array_fetch(mvar_type, mvar_list, mv_id);
00101         value = 0;
00102         /* loop for each bvar */
00103         for (j=0; j<mv.encode_length; j++) {
00104             literal = array_fetch(bdd_literal, mgen->cube, mdd_ret_bvar_id(&mv, j) );
00105 
00106             prev_literal = array_fetch(bdd_literal, mgen->minterm, k);
00107             if ((literal == 2) && (carry == 1)) {
00108                 if (prev_literal == 0) {
00109                     array_insert(bdd_literal, minterm, k, 1);
00110                     carry = 0;
00111                     value = value*2 + 1;
00112                 }
00113                 else if (prev_literal == 1) {
00114                     array_insert(bdd_literal, minterm, k, 0);
00115                     carry = 1;
00116                     value = value*2 + 0;
00117                 }
00118             }
00119             else if ((literal == 2) && (carry == 0)) {
00120                     array_insert(bdd_literal, minterm, k, prev_literal);
00121                     value = value*2 + prev_literal;
00122             }
00123             else { /* if literal == 0 or 1 */
00124                     array_insert(bdd_literal, minterm, k, literal);
00125                     value = value*2 + literal;
00126             }
00127             k++;
00128         }
00129         array_insert_last(int, solution, value);
00130         if (value >= mv.values) out_of_range = 1;
00131     }
00132 
00133     if (carry == 1) {
00134         /* no more minterms */
00135         array_free(minterm);
00136         minterm = NIL(array_t);
00137         array_free(solution);
00138         solution = NIL(array_t);
00139     }
00140     array_free(mgen->minterm);
00141     mgen->minterm = minterm;
00142     mgen->out_of_range = out_of_range;
00143 
00144     return (solution);
00145 }

static array_t* next_valid_minterm ( mdd_gen *  mgen  )  [static]

Definition at line 149 of file mdd_iter.c.

00150 {
00151     array_t *solution;
00152     array_t *cube;
00153 
00154     solution = next_minterm(mgen);
00155 
00156     /* check if done with current cube */
00157     if (mgen->minterm == NIL(array_t)) {
00158         (void) bdd_next_cube(mgen->bdd_generator, &cube);
00159         mgen->status = bdd_gen_read_status(mgen->bdd_generator);
00160         mgen->cube = cube;
00161         if (mgen->status != bdd_EMPTY) {
00162             if (solution != NIL(array_t) ) array_free(solution);
00163             solution = first_minterm(mgen);
00164         }
00165         else {
00166             mgen->minterm = NIL(array_t);
00167             mgen->cube = NIL(array_t);
00168         }
00169     }
00170     return (solution);
00171 }

Generated on Tue Jan 12 13:57:26 2010 for glu-2.2 by  doxygen 1.6.1