glu-2.2: src/cmuPort/cmuPort.c Source File

00001 
00038 #include "cmuPortInt.h" 
00039 #ifndef EPD_MAX_BIN
00040 #include "epd.h" 
00041 #endif
00042 
00043 /*---------------------------------------------------------------------------*/
00044 /* Constant declarations                                                     */
00045 /*---------------------------------------------------------------------------*/
00046 
00047 
00048 /*---------------------------------------------------------------------------*/
00049 /* Type declarations                                                         */
00050 /*---------------------------------------------------------------------------*/
00051 
00052 
00053 /*---------------------------------------------------------------------------*/
00054 /* Structure declarations                                                    */
00055 /*---------------------------------------------------------------------------*/
00056 
00057 
00058 /*---------------------------------------------------------------------------*/
00059 /* Variable declarations                                                     */
00060 /*---------------------------------------------------------------------------*/
00061 
00062 
00063 /*---------------------------------------------------------------------------*/
00064 /* Macro declarations                                                        */
00065 /*---------------------------------------------------------------------------*/
00066 
00067 
00070 /*---------------------------------------------------------------------------*/
00071 /* Static function prototypes                                                */
00072 /*---------------------------------------------------------------------------*/
00073 
00077 /*---------------------------------------------------------------------------*/
00078 /* Definition of exported functions                                          */
00079 /*---------------------------------------------------------------------------*/
00080 
00092 bdd_t *
00093 bdd_construct_bdd_t(bdd_manager *manager, bdd_node *func)
00094 {
00095     bdd_t *result;
00096     cmu_bdd_manager mgr = (cmu_bdd_manager)manager;
00097     bdd fn = (bdd)func;
00098 
00099     if (fn == (struct bdd_ *) 0) {
00100         cmu_bdd_fatal("bdd_construct_bdd_t: possible memory overflow");
00101     }
00102 
00103     result = ALLOC(bdd_t, 1);
00104     result->mgr = mgr;
00105     result->node = fn;
00106     result->free = FALSE;
00107     return result;
00108 }
00109 
00119 bdd_package_type_t
00120 bdd_get_package_name(void)
00121 {
00122   return CMU;
00123 }
00124 
00125 /*
00126 BDD Manager Allocation And Destruction ----------------------------------------
00127 */
00128 void
00129 bdd_end(bdd_manager *manager)
00130 {
00131     bdd_external_hooks *hooks;
00132     cmu_bdd_manager mgr = (cmu_bdd_manager)manager;
00133     hooks = (bdd_external_hooks *) mgr->hooks;
00134     FREE(hooks); 
00135     cmu_bdd_quit(mgr);
00136 }
00137 
00138 
00139 bdd_manager *
00140 bdd_start(int nvariables)
00141 {
00142     struct bdd_manager_ *mgr;
00143     int i;
00144     bdd_external_hooks *hooks;
00145    
00146     mgr = cmu_bdd_init();    /*no args*/
00147 
00148     /*
00149      * Calls to UCB bdd_get_variable are translated into cmu_bdd_var_with_id calls.  However,
00150      * cmu_bdd_var_with_id assumes that single variable BDDs have already been created for 
00151      * all the variables that we wish to access.  Thus, following, we explicitly create n
00152      * variables.  We do not care about the return value of cmu_bdd_new_var_last; in the 
00153      * CMU package, the single variable BDDs are NEVER garbage collected.
00154      */
00155     for (i = 0; i < nvariables; i++) {
00156         (void) cmu_bdd_new_var_last(mgr);
00157     }
00158 
00159     hooks = ALLOC(bdd_external_hooks, 1);
00160     hooks->mdd = hooks->network = hooks->undef1 = (char *) 0;
00161     mgr->hooks = (char *) hooks;  /* new field added to CMU manager */
00162 
00163     return (bdd_manager *) mgr;
00164 }
00165 
00166 /*
00167 BDD Variable Allocation -------------------------------------------------------
00168 */
00169 
00170 bdd_t *
00171 bdd_create_variable(bdd_manager *manager)
00172 {
00173   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00174   return bdd_construct_bdd_t(mgr, cmu_bdd_new_var_last(mgr));
00175 }
00176 
00177 bdd_t *
00178 bdd_create_variable_after(bdd_manager *manager, bdd_variableId after_id)
00179 {
00180   struct bdd_ *after_var;
00181   bdd_t         *result;
00182   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00183 
00184   after_var = cmu_bdd_var_with_id(mgr, (long)after_id + 1);
00185   
00186   result =  bdd_construct_bdd_t(mgr, cmu_bdd_new_var_after(mgr, after_var));
00187   
00188   /* No need to free after_var, since single variable BDDs are never garbage collected */
00189   
00190   return result;
00191 }
00192 
00193 
00194 
00195 bdd_t *
00196 bdd_get_variable(bdd_manager *manager, bdd_variableId variable_ID)
00197 {
00198   struct bdd_ *fn;
00199   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00200   fn = cmu_bdd_var_with_id(mgr, (long) (variable_ID + 1));
00201 
00202   if (fn == (struct bdd_ *) 0) {
00203     int i;
00204     for (i=cmu_bdd_vars(mgr); i < variable_ID + 1; i++) {
00205       fn = cmu_bdd_new_var_last(mgr);
00206     }
00207   }
00208   
00209   return bdd_construct_bdd_t(mgr, fn);
00210 }
00211 
00212 /*
00213 BDD Formula Management --------------------------------------------------------
00214 */
00215 
00216 bdd_t *
00217 bdd_dup(bdd_t *f)
00218 {
00219   return bdd_construct_bdd_t(f->mgr, cmu_bdd_identity(f->mgr, f->node));
00220 }
00221 
00222 void
00223 bdd_free(bdd_t *f)
00224 {
00225   if (f == NIL(bdd_t)) {
00226         fail("bdd_free: trying to free a NIL bdd_t");                   
00227   }
00228   
00229   if (f->free == TRUE) {
00230         fail("bdd_free: trying to free a freed bdd_t");                 
00231   }     
00232   
00233   cmu_bdd_free(f->mgr, f->node);
00234   
00235   /*
00236    * In case the user tries to free this bdd_t again, set the free field to TRUE, 
00237      * and NIL out the other fields.  Then free the bdd_t structure itself.
00238      */
00239   f->free = TRUE;
00240   f->node = NIL(struct bdd_);
00241   f->mgr = NIL(struct bdd_manager_);
00242   FREE(f);  
00243 }
00244 
00245 /*
00246   Operations on BDD Formulas ----------------------------------------------------
00247   */
00248 
00249 bdd_t *
00250 bdd_and(
00251   bdd_t *f,
00252   bdd_t *g,
00253   boolean f_phase,
00254   boolean g_phase)
00255 {
00256   struct bdd_ *temp1, *temp2;
00257   bdd_t *result;
00258   struct bdd_manager_ *mgr;
00259   
00260   mgr = f->mgr;
00261   temp1 = ( (f_phase == TRUE) ? cmu_bdd_identity(mgr, f->node) : cmu_bdd_not(mgr, f->node));
00262   temp2 = ( (g_phase == TRUE) ? cmu_bdd_identity(mgr, g->node) : cmu_bdd_not(mgr, g->node));
00263   result = bdd_construct_bdd_t(mgr, cmu_bdd_and(mgr, temp1, temp2));
00264   cmu_bdd_free(mgr, temp1);
00265   cmu_bdd_free(mgr, temp2);
00266   return result;
00267 }
00268 
00269 bdd_t *
00270 bdd_and_with_limit(
00271   bdd_t *f,
00272   bdd_t *g,
00273   boolean f_phase,
00274   boolean g_phase,
00275   unsigned int limit)
00276 {
00277   /* Unsupported: fall back on standard AND. */
00278   return bdd_and(f, g, f_phase, g_phase);
00279 }
00280 
00281 bdd_t *
00282 bdd_and_array(
00283   bdd_t *f,
00284   array_t *g_array,
00285   boolean f_phase,
00286   boolean g_phase)
00287 {
00288   struct bdd_ *temp1, *temp2, *result;
00289   bdd_t *g;
00290   struct bdd_manager_ *mgr;
00291   int i;
00292 
00293   mgr = f->mgr;
00294   result = ((f_phase == TRUE) ? cmu_bdd_identity(mgr, f->node) :
00295             cmu_bdd_not(mgr, f->node)); 
00296 
00297   for (i = 0; i < array_n(g_array); i++) {
00298     g = array_fetch(bdd_t *, g_array, i);
00299     temp1 = result;
00300     temp2 = ((g_phase == TRUE) ? cmu_bdd_identity(mgr, g->node) :
00301              cmu_bdd_not(mgr, g->node));
00302     result = cmu_bdd_and(mgr, temp1, temp2);
00303     cmu_bdd_free(mgr, temp1);
00304     cmu_bdd_free(mgr, temp2);
00305     if (result == NULL)
00306       return(NULL);
00307   }
00308 
00309   return(bdd_construct_bdd_t(mgr, result));
00310 }
00311 
00312 bdd_t *
00313 bdd_multiway_and(bdd_manager *manager, array_t *bddArray)
00314 {
00315   int i;
00316   bdd temp, result;
00317   bdd_t *operand;
00318   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00319   result = cmu_bdd_one(mgr);
00320   for (i=0; i<array_n(bddArray); i++){
00321     operand = array_fetch(bdd_t *, bddArray, i);
00322     temp = cmu_bdd_and(mgr, result, operand->node);
00323     cmu_bdd_free(mgr, result);
00324     result = temp;
00325   }
00326   return bdd_construct_bdd_t(mgr, result);
00327 }
00328 
00329 bdd_t *
00330 bdd_multiway_or(bdd_manager *manager, array_t *bddArray)
00331 {
00332   int i;
00333   bdd temp, result;
00334   bdd_t *operand;
00335   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00336   result = cmu_bdd_zero(mgr);
00337   for (i=0; i<array_n(bddArray); i++){
00338     operand = array_fetch(bdd_t *, bddArray, i);
00339     temp = cmu_bdd_or(mgr, result, operand->node);
00340     cmu_bdd_free(mgr, result);
00341     result = temp;
00342   }
00343   return bdd_construct_bdd_t(mgr, result);
00344 }
00345 
00346 bdd_t *
00347 bdd_multiway_xor(bdd_manager *manager, array_t *bddArray)
00348 {
00349   int i;
00350   bdd temp, result;
00351   bdd_t *operand;
00352   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00353   result = cmu_bdd_zero(mgr);
00354   for (i=0; i<array_n(bddArray); i++){
00355     operand = array_fetch(bdd_t *, bddArray, i);
00356     temp = cmu_bdd_xor(mgr, result, operand->node);
00357     cmu_bdd_free(mgr, result);
00358     result = temp;
00359   }
00360   return bdd_construct_bdd_t(mgr, result);
00361 }
00362 
00363 array_t *
00364 bdd_pairwise_or(bdd_manager *manager, array_t *bddArray1, array_t
00365                 *bddArray2) 
00366 {
00367   int i;
00368   bdd_t *operand1, *operand2;
00369   array_t *resultArray;
00370   bdd result;
00371   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00372   if (array_n(bddArray1) != array_n(bddArray2)){
00373     fprintf(stderr, "bdd_pairwise_or: Arrays of different lengths.\n");
00374     return NIL(array_t);
00375   }
00376   resultArray = array_alloc(bdd_t *, 0);
00377   for (i=0; i<array_n(bddArray1); i++){
00378     operand1 = array_fetch(bdd_t *, bddArray1, i);
00379     operand2 = array_fetch(bdd_t *, bddArray2, i);
00380     result = cmu_bdd_or(mgr, operand1->node, operand2->node);
00381     array_insert_last(bdd_t*, resultArray,
00382                       bdd_construct_bdd_t(mgr, result)); 
00383   }
00384   return resultArray;
00385 }
00386 
00387 array_t *
00388 bdd_pairwise_and(bdd_manager *manager, array_t *bddArray1, array_t
00389                  *bddArray2) 
00390 {
00391   int i;
00392   bdd_t *operand1, *operand2;
00393   array_t *resultArray;
00394   bdd result;
00395   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00396   if (array_n(bddArray1) != array_n(bddArray2)){
00397     fprintf(stderr, "bdd_pairwise_and: Arrays of different lengths.\n");
00398     return NIL(array_t);
00399   }
00400   resultArray = array_alloc(bdd_t *, 0);
00401   for (i=0; i<array_n(bddArray1); i++){
00402     operand1 = array_fetch(bdd_t *, bddArray1, i);
00403     operand2 = array_fetch(bdd_t *, bddArray2, i);
00404     result = cmu_bdd_and(mgr, operand1->node, operand2->node);
00405     array_insert_last(bdd_t*, resultArray,
00406                       bdd_construct_bdd_t(mgr, result)); 
00407   }
00408   return resultArray;
00409 }
00410 
00411 array_t *
00412 bdd_pairwise_xor(bdd_manager *manager, array_t *bddArray1, array_t
00413                  *bddArray2) 
00414 {
00415   int i;
00416   bdd_t *operand1, *operand2;
00417   array_t *resultArray;
00418   bdd result;
00419   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00420   if (array_n(bddArray1) != array_n(bddArray2)){
00421     fprintf(stderr, "bdd_pairwise_xor: Arrays of different lengths.\n");
00422     return NIL(array_t);
00423   }
00424   resultArray = array_alloc(bdd_t *, 0);
00425   for (i=0; i<array_n(bddArray1); i++){
00426     operand1 = array_fetch(bdd_t *, bddArray1, i);
00427     operand2 = array_fetch(bdd_t *, bddArray2, i);
00428     result = cmu_bdd_xor(mgr, operand1->node, operand2->node);
00429     array_insert_last(bdd_t*, resultArray,
00430                       bdd_construct_bdd_t(mgr, result)); 
00431   }
00432   return resultArray;
00433 }
00434 
00435 bdd_t *
00436 bdd_and_smooth(
00437   bdd_t *f,
00438   bdd_t *g,
00439   array_t *smoothing_vars /* of bdd_t *'s */)
00440 {
00441   int num_vars, i;
00442   bdd_t *fn, *result;
00443   struct bdd_ **assoc;
00444   struct bdd_manager_ *mgr;
00445   
00446   num_vars = array_n(smoothing_vars);
00447   if (num_vars <= 0) {
00448         cmu_bdd_fatal("bdd_and_smooth: no smoothing variables");
00449   }
00450   
00451   assoc = ALLOC(struct bdd_ *, num_vars+1);
00452   
00453   for (i = 0; i < num_vars; i++) {
00454         fn = array_fetch(bdd_t *, smoothing_vars, i);
00455         assoc[i] = fn->node;
00456   }
00457   assoc[num_vars] = (struct bdd_ *) 0;
00458   
00459   mgr = f->mgr;
00460   cmu_bdd_temp_assoc(mgr, assoc, 0);
00461   (void) cmu_bdd_assoc(mgr, -1);  /* set the temp association as the current association */
00462   
00463   result = bdd_construct_bdd_t(mgr, cmu_bdd_rel_prod(mgr, f->node, g->node));
00464   FREE(assoc);
00465   return result;
00466 }
00467 
00468 bdd_t *
00469 bdd_and_smooth_with_limit(
00470   bdd_t *f,
00471   bdd_t *g,
00472   array_t *smoothing_vars /* of bdd_t *'s */,
00473   unsigned int limit)
00474 {
00475   /* Unsupported: fall back to standard and_smooth */
00476   return bdd_and_smooth(f, g, smoothing_vars);
00477 }
00478 
00479 bdd_t *
00480 bdd_between(bdd_t *f_min, bdd_t *f_max)
00481 {
00482   bdd_t *temp, *ret;
00483   long size1, size2, size3; 
00484   temp = bdd_or(f_min, f_max, 1, 0);
00485   ret = bdd_minimize(f_min, temp);
00486   bdd_free(temp);
00487   size1 = bdd_size(f_min);
00488   size2 = bdd_size(f_max);
00489   size3 = bdd_size(ret);
00490   if (size3 < size1) {
00491         if (size3 < size2){
00492       return ret;
00493     }
00494     else {
00495       bdd_free(ret);
00496       return bdd_dup(f_max);
00497     }
00498   }
00499   else {
00500     bdd_free(ret);
00501     if (size1 < size2){
00502       return bdd_dup(f_min);
00503     }
00504     else {
00505       return bdd_dup(f_max);
00506     }
00507   }
00508 }
00509 
00510 bdd_t *
00511 bdd_cofactor(bdd_t *f, bdd_t *g)
00512 {
00513   return bdd_construct_bdd_t(f->mgr, cmu_bdd_cofactor(f->mgr, f->node, g->node));
00514 }
00515 
00516 bdd_t *
00517 bdd_cofactor_array(bdd_t *f, array_t *bddArray)
00518 {
00519   bdd_t *operand;
00520   struct bdd_ *result, *temp;
00521   int i;
00522 
00523   result = cmu_bdd_identity(f->mgr, f->node);
00524 
00525   for (i = 0; i < array_n(bddArray); i++) {
00526     operand = array_fetch(bdd_t *, bddArray, i);
00527     temp = cmu_bdd_cofactor(f->mgr, result, operand->node);
00528     if (temp == NULL) {
00529       cmu_bdd_free(f->mgr, result);
00530       return(NULL);
00531     }
00532     cmu_bdd_free(f->mgr, result);
00533     result = temp;
00534   }
00535 
00536   return(bdd_construct_bdd_t(f->mgr, result));
00537 }
00538 
00539 bdd_t *
00540 bdd_compose(
00541   bdd_t *f,
00542   bdd_t *v,
00543   bdd_t *g)
00544 {
00545   return bdd_construct_bdd_t(f->mgr, cmu_bdd_compose(f->mgr, f->node, v->node, g->node));
00546 }
00547 
00548 bdd_t *
00549 bdd_consensus(
00550   bdd_t *f,
00551   array_t *quantifying_vars /* of bdd_t *'s */)
00552 {
00553   int num_vars, i;
00554   bdd_t *fn, *result;
00555   struct bdd_ **assoc;
00556   struct bdd_manager_ *mgr;
00557   
00558   num_vars = array_n(quantifying_vars);
00559   if (num_vars <= 0) {
00560         cmu_bdd_fatal("bdd_consensus: no quantifying variables");
00561   }
00562   
00563   assoc = ALLOC(struct bdd_ *, num_vars+1);
00564   
00565   for (i = 0; i < num_vars; i++) {
00566         fn = array_fetch(bdd_t *, quantifying_vars, i);
00567         assoc[i] = fn->node;
00568   }
00569   assoc[num_vars] = (struct bdd_ *) 0;
00570   
00571   mgr = f->mgr;
00572   cmu_bdd_temp_assoc(mgr, assoc, 0);
00573   (void) cmu_bdd_assoc(mgr, -1);  /* set the temp association as the current association */
00574   
00575   result = bdd_construct_bdd_t(mgr, cmu_bdd_forall(mgr, f->node));
00576   FREE(assoc);
00577   return result;
00578 }
00579 
00580 
00581 bdd_t *
00582 bdd_cproject(
00583   bdd_t *f,
00584   array_t *quantifying_vars /* of bdd_t* */)
00585 {
00586   int num_vars, i;
00587   bdd_t *fn, *result;
00588   struct bdd_ **assoc;
00589   struct bdd_manager_ *mgr;
00590   
00591   if (f == NIL(bdd_t)) fail ("bdd_cproject: invalid BDD");
00592   
00593   num_vars = array_n(quantifying_vars);
00594   if (num_vars <= 0) {
00595     printf("Warning: bdd_cproject: no projection variables\n");
00596     result = bdd_dup(f);
00597   }
00598   else {
00599     assoc = ALLOC(struct bdd_ *, num_vars+1);
00600     for (i = 0; i < num_vars; i++) {
00601       fn = array_fetch(bdd_t *, quantifying_vars, i);
00602       assoc[i] = fn->node;
00603     }
00604     assoc[num_vars] = (struct bdd_ *) 0;
00605     mgr = f->mgr;
00606     cmu_bdd_temp_assoc(mgr, assoc, 0);
00607     (void) cmu_bdd_assoc(mgr, -1);  /* set the temp association as the current a
00608                                        ssociation */
00609     
00610     result = bdd_construct_bdd_t(mgr, cmu_bdd_project(mgr, f->node));
00611     FREE(assoc);
00612   }
00613   return result;
00614 }
00615 
00616 
00617 bdd_t *
00618 bdd_else(bdd_t *f)
00619 {
00620   return bdd_construct_bdd_t(f->mgr, cmu_bdd_else(f->mgr, f->node));
00621 }
00622 
00623 
00624 bdd_t *
00625 bdd_ite(
00626   bdd_t *i,
00627   bdd_t *t,
00628   bdd_t *e,
00629   boolean i_phase,
00630   boolean t_phase,
00631   boolean e_phase)
00632 {
00633   struct bdd_ *temp1, *temp2, *temp3;
00634   bdd_t *result;
00635   struct bdd_manager_ *mgr;
00636   
00637   mgr = i->mgr;
00638   temp1 = ( (i_phase == TRUE) ? cmu_bdd_identity(mgr, i->node) : cmu_bdd_not(mgr, i->node));
00639   temp2 = ( (t_phase == TRUE) ? cmu_bdd_identity(mgr, t->node) : cmu_bdd_not(mgr, t->node));
00640   temp3 = ( (e_phase == TRUE) ? cmu_bdd_identity(mgr, e->node) : cmu_bdd_not(mgr, e->node));
00641   result = bdd_construct_bdd_t(mgr, cmu_bdd_ite(mgr, temp1, temp2, temp3));
00642   cmu_bdd_free(mgr, temp1);
00643   cmu_bdd_free(mgr, temp2);
00644   cmu_bdd_free(mgr, temp3);
00645   return result;
00646 }
00647 
00648 bdd_t *
00649 bdd_minimize(bdd_t *f, bdd_t *c)
00650 {
00651   bdd_t *result = bdd_construct_bdd_t(f->mgr, cmu_bdd_reduce(f->mgr,
00652                                                              f->node,
00653                                                              c->node)); 
00654   if (bdd_size(result) < bdd_size(f)){
00655     return result;
00656   }
00657   else{
00658     bdd_free(result);
00659     return bdd_dup(f);
00660   }
00661 }
00662 
00663 bdd_t *
00664 bdd_minimize_array(bdd_t *f, array_t *bddArray)
00665 {
00666   bdd_t *operand;
00667   struct bdd_ *result, *temp;
00668   bdd_t *final;
00669   int i;
00670 
00671   result = cmu_bdd_identity(f->mgr, f->node);
00672   for (i = 0; i < array_n(bddArray); i++) {
00673     operand = array_fetch(bdd_t *, bddArray, i);
00674     temp = cmu_bdd_reduce(f->mgr, result, operand->node);
00675     if (temp == NULL) {
00676       cmu_bdd_free(f->mgr, result);
00677       return(NULL);
00678     }
00679     cmu_bdd_free(f->mgr, result);
00680     result = temp;
00681   }
00682 
00683   final = bdd_construct_bdd_t(f->mgr, result);
00684 
00685   if (bdd_size(final) < bdd_size(f)){
00686     return final;
00687   }
00688   else{
00689     bdd_free(final);
00690     return bdd_dup(f);
00691   }
00692 }
00693 
00694 
00695 bdd_t *
00696 bdd_not(bdd_t *f)
00697 {
00698   return bdd_construct_bdd_t(f->mgr, cmu_bdd_not(f->mgr, f->node));
00699 }
00700 
00701 bdd_t *
00702 bdd_one(bdd_manager *manager)
00703 {
00704   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00705   return bdd_construct_bdd_t(mgr, cmu_bdd_one(mgr));
00706 }
00707 
00708 bdd_t *
00709 bdd_or(
00710   bdd_t *f,
00711   bdd_t *g,
00712   boolean f_phase,
00713   boolean g_phase)
00714 {
00715   struct bdd_ *temp1, *temp2;
00716   bdd_t *result;
00717   struct bdd_manager_ *mgr;
00718   
00719   mgr = f->mgr;
00720   temp1 = ( (f_phase == TRUE) ? cmu_bdd_identity(mgr, f->node) : cmu_bdd_not(mgr, f->node));
00721   temp2 = ( (g_phase == TRUE) ? cmu_bdd_identity(mgr, g->node) : cmu_bdd_not(mgr, g->node));
00722   result = bdd_construct_bdd_t(mgr, cmu_bdd_or(mgr, temp1, temp2));
00723   cmu_bdd_free(mgr, temp1);
00724   cmu_bdd_free(mgr, temp2);
00725   return result;
00726 }
00727 
00728 bdd_t *
00729 bdd_smooth(
00730   bdd_t *f,
00731   array_t *smoothing_vars /* of bdd_t *'s */)
00732 {
00733   int num_vars, i;
00734   bdd_t *fn, *result;
00735   struct bdd_ **assoc;
00736   struct bdd_manager_ *mgr;
00737   
00738   num_vars = array_n(smoothing_vars);
00739   if (num_vars <= 0) {
00740         cmu_bdd_fatal("bdd_smooth: no smoothing variables");
00741   }
00742   
00743   assoc = ALLOC(struct bdd_ *, num_vars+1);
00744   
00745   for (i = 0; i < num_vars; i++) {
00746         fn = array_fetch(bdd_t *, smoothing_vars, i);
00747         assoc[i] = fn->node;
00748   }
00749   assoc[num_vars] = (struct bdd_ *) 0;
00750   
00751   mgr = f->mgr;
00752   cmu_bdd_temp_assoc(mgr, assoc, 0);
00753   (void) cmu_bdd_assoc(mgr, -1);  /* set the temp association as the current association */
00754   
00755   result = bdd_construct_bdd_t(mgr, cmu_bdd_exists(mgr, f->node));
00756   FREE(assoc);
00757   return result;
00758 }
00759 
00760 bdd_t *
00761 bdd_substitute(
00762   bdd_t *f,
00763   array_t *old_array /* of bdd_t *'s */,
00764   array_t *new_array /* of bdd_t *'s */)
00765 {
00766     int num_old_vars, num_new_vars, i;
00767     bdd_t *fn_old, *fn_new, *result;
00768     struct bdd_ **assoc;
00769     struct bdd_manager_ *mgr;
00770 
00771     num_old_vars = array_n(old_array);
00772     num_new_vars = array_n(new_array);
00773     if (num_old_vars != num_new_vars) {
00774         cmu_bdd_fatal("bdd_substitute: mismatch of number of new and old variables");
00775     }
00776 
00777     assoc = ALLOC(struct bdd_ *, 2*(num_old_vars+1));
00778 
00779     for (i = 0; i < num_old_vars; i++) {
00780         fn_old = array_fetch(bdd_t *, old_array, i);
00781         fn_new = array_fetch(bdd_t *, new_array, i);
00782         assoc[2*i]   = fn_old->node;
00783         assoc[2*i+1] = fn_new->node;
00784     }
00785     assoc[2*num_old_vars]   = (struct bdd_ *) 0;
00786     assoc[2*num_old_vars+1] = (struct bdd_ *) 0;  /* not sure if we need this second 0 */
00787 
00788     mgr = f->mgr;
00789     cmu_bdd_temp_assoc(mgr, assoc, 1);
00790     (void) cmu_bdd_assoc(mgr, -1);  /* set the temp association as the current association */
00791 
00792     result = bdd_construct_bdd_t(mgr, cmu_bdd_substitute(mgr, f->node));
00793     FREE(assoc);
00794     return result;
00795 }
00796 
00797 array_t *
00798 bdd_substitute_array(
00799   array_t *f_array,
00800   array_t *old_array /* of bdd_t *'s */,
00801   array_t *new_array /* of bdd_t *'s */)
00802 {
00803   int   i;
00804   bdd_t *f, *new_;
00805   array_t *substitute_array = array_alloc(bdd_t *, 0);
00806 
00807   arrayForEachItem(bdd_t *, f_array, i, f) {
00808     new_ = bdd_substitute(f, old_array, new_array);
00809     array_insert_last(bdd_t *, substitute_array, new_);
00810   }
00811   return(substitute_array);
00812 }
00813 
00814 void *
00815 bdd_pointer(bdd_t *f)
00816 {
00817     return((void *)f->node);
00818 }
00819 
00820 bdd_t *
00821 bdd_then(bdd_t *f)
00822 {
00823     return bdd_construct_bdd_t(f->mgr, cmu_bdd_then(f->mgr, f->node));
00824 }
00825 
00826 bdd_t *
00827 bdd_top_var(bdd_t *f)
00828 {
00829     return bdd_construct_bdd_t(f->mgr, cmu_bdd_if(f->mgr, f->node));
00830 }
00831 
00832 bdd_t *
00833 bdd_xnor(bdd_t *f, bdd_t *g)
00834 {
00835     return bdd_construct_bdd_t(f->mgr, cmu_bdd_xnor(f->mgr, f->node, g->node));
00836 }
00837 
00838 bdd_t *
00839 bdd_xor(bdd_t *f, bdd_t *g)
00840 {
00841     return bdd_construct_bdd_t(f->mgr, cmu_bdd_xor(f->mgr, f->node, g->node));
00842 }
00843 
00844 bdd_t *
00845 bdd_zero(bdd_manager *manager)
00846 {
00847   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00848   return bdd_construct_bdd_t(mgr, cmu_bdd_zero(mgr));
00849 }
00850 
00851 /*
00852 Queries about BDD Formulas ----------------------------------------------------
00853 */
00854 
00855 boolean
00856 bdd_equal(bdd_t *f, bdd_t *g)
00857 {
00858     return (f->node == g->node);
00859 }
00860 
00861 boolean
00862 bdd_equal_mod_care_set(bdd_t *f, bdd_t *g, bdd_t *CareSet)
00863 {
00864   bdd_t *diffBdd;
00865   boolean result;
00866 
00867   if (bdd_equal(f, g))
00868     return 1;
00869 
00870   diffBdd = bdd_xor(f, g);
00871 
00872   result = bdd_leq(diffBdd, CareSet, 1, 0);
00873   bdd_free(diffBdd);
00874 
00875   return(result);
00876 }
00877 
00878 bdd_t *
00879 bdd_intersects(bdd_t *f, bdd_t *g)
00880 {
00881     return bdd_construct_bdd_t(f->mgr, cmu_bdd_intersects(f->mgr, f->node, g->node));
00882 }
00883 
00884 bdd_t *
00885 bdd_closest_cube(bdd_t *f, bdd_t *g, int *dist)
00886 {
00887     return (NULL);
00888 }
00889 
00890 boolean
00891 bdd_is_tautology(bdd_t *f, boolean phase)
00892 {
00893     return ((phase == TRUE) ? (f->node == cmu_bdd_one(f->mgr)) : (f->node == cmu_bdd_zero(f->mgr)));
00894 }
00895 
00896 boolean
00897 bdd_leq(
00898   bdd_t *f,
00899   bdd_t *g,
00900   boolean f_phase,
00901   boolean g_phase)
00902 {
00903     struct bdd_ *temp1, *temp2, *implies_fn;
00904     struct bdd_manager_ *mgr;
00905     boolean result_value;
00906 
00907     mgr = f->mgr;
00908     temp1 = ( (f_phase == TRUE) ? cmu_bdd_identity(mgr, f->node) : cmu_bdd_not(mgr, f->node));
00909     temp2 = ( (g_phase == TRUE) ? cmu_bdd_identity(mgr, g->node) : cmu_bdd_not(mgr, g->node));
00910     implies_fn = cmu_bdd_implies(mgr, temp1, temp2); /* returns a minterm of temp1*!temp2 */
00911     result_value = (implies_fn == cmu_bdd_zero(mgr));
00912     cmu_bdd_free(mgr, temp1);
00913     cmu_bdd_free(mgr, temp2);
00914     cmu_bdd_free(mgr, implies_fn);
00915     return result_value;
00916 }
00917 
00918 boolean
00919 bdd_lequal_mod_care_set(
00920   bdd_t *f,
00921   bdd_t *g,
00922   boolean f_phase,
00923   boolean g_phase,
00924   bdd_t *careSet)
00925 {
00926   bdd_t *temp;
00927   boolean result;
00928 
00929   if (bdd_leq(f, g, f_phase, g_phase))
00930     return 1;
00931 
00932   temp = bdd_and(f, careSet, f_phase, 1);
00933 
00934   result = bdd_leq(temp, g, 1, g_phase);
00935   bdd_free(temp);
00936 
00937   return(result);
00938 }
00939 
00940 boolean
00941 bdd_leq_array(
00942   bdd_t *f,
00943   array_t *g_array,
00944   boolean f_phase,
00945   boolean g_phase)
00946 {
00947   int   i;
00948   bdd_t *g;
00949   boolean result;
00950 
00951   arrayForEachItem(bdd_t *, g_array, i, g) {
00952     result = bdd_leq(f, g, f_phase, g_phase);
00953     if (g_phase) {
00954       if (!result)
00955         return(0);
00956     } else {
00957       if (result)
00958         return(1);
00959     }
00960   }
00961   if (g_phase)
00962     return(1);
00963   else
00964     return(0);
00965 }
00966 
00967 /*
00968 Statistics and Other Queries --------------------------------------------------
00969 */
00970 
00971 double 
00972 bdd_count_onset(
00973   bdd_t *f,
00974   array_t *var_array /* of bdd_t *'s */)
00975 {
00976     int num_vars;
00977     double fraction;
00978 
00979     num_vars = array_n(var_array);
00980     fraction = cmu_bdd_satisfying_fraction(f->mgr, f->node); /* cannot give support vars */
00981     return (fraction * pow((double) 2, (double) num_vars));
00982 }
00983 
00991 int
00992 bdd_epd_count_onset(
00993   bdd_t *f,
00994   array_t *var_array /* of bdd_t *'s */,
00995   EpDouble *epd)
00996 {
00997   double nMinterms;
00998 
00999   nMinterms = bdd_count_onset(f, var_array);
01000   EpdConvert(nMinterms, epd);
01001   return 0;
01002 } /* end of bdd_epd_count_onset */
01003 
01004 int
01005 bdd_get_free(bdd_t *f)
01006 {
01007     return (f->free);
01008 }
01009 
01010 bdd_manager *
01011 bdd_get_manager(bdd_t *f)
01012 {
01013     return (bdd_manager *) (f->mgr);
01014 }
01015 
01016 bdd_node *
01017 bdd_get_node(
01018   bdd_t *f,
01019   boolean *is_complemented /* return */)
01020 {
01021     *is_complemented = (boolean) TAG0(f->node);  /* using bddint.h */
01022     return ((bdd_node *) BDD_POINTER(f->node));  /* using bddint.h */
01023 }
01024 
01025 var_set_t *
01026 bdd_get_support(bdd_t *f)
01027 {
01028     struct bdd_ **support, *var;
01029     struct bdd_manager_ *mgr;
01030     long num_vars;
01031     var_set_t *result;
01032     int id, i;
01033 
01034     mgr = f->mgr;
01035     num_vars = cmu_bdd_vars(mgr);
01036 
01037     result = var_set_new((int) num_vars);
01038     support = (struct bdd_ **) mem_get_block((num_vars+1) * sizeof(struct bdd_ *));
01039     (void) cmu_bdd_support(mgr, f->node, support);
01040 
01041     for (i = 0; i < num_vars; ++i) {  /* can never have more than num_var non-zero entries in array */
01042         var = support[i]; 
01043         if (var == (struct bdd_ *) 0) {
01044             break;  /* have reach end of null-terminated array */
01045         }
01046         id = (int) (cmu_bdd_if_id(mgr, var) - 1);  /* a variable is never garbage collected, so no need to free */
01047         var_set_set_elt(result, id);
01048     }
01049 
01050     mem_free_block((pointer)support);
01051 
01052     return result;
01053 }
01054 
01055 int
01056 bdd_is_support_var(bdd_t *f, bdd_t *var)
01057 {
01058     return(bdd_is_support_var_id(f, bdd_top_var_id(var)));
01059 }
01060 
01061 int
01062 bdd_is_support_var_id(bdd_t *f, int index)
01063 {
01064     struct bdd_ **support, *var;
01065     struct bdd_manager_ *mgr;
01066     long num_vars;
01067     int id, i;
01068 
01069     mgr = f->mgr;
01070     num_vars = cmu_bdd_vars(mgr);
01071 
01072     support = (struct bdd_ **) mem_get_block((num_vars+1) * sizeof(struct bdd_ *));
01073     (void) cmu_bdd_support(mgr, f->node, support);
01074 
01075     for (i = 0; i < num_vars; ++i) {  /* can never have more than num_var non-zero entries in array */
01076         var = support[i]; 
01077         if (var == (struct bdd_ *) 0) {
01078             break;  /* have reach end of null-terminated array */
01079         }
01080         id = (int) (cmu_bdd_if_id(mgr, var) - 1);  /* a variable is never garbage collected, so no need to free */
01081         if (id == index) {
01082             mem_free_block((pointer)support);
01083             return 1;
01084         }
01085     }
01086 
01087     mem_free_block((pointer)support);
01088 
01089     return 0;
01090 }
01091 
01092 array_t *
01093 bdd_get_varids(array_t *var_array)
01094 {
01095   int i;
01096   bdd_t *var;
01097   array_t *result;
01098  
01099   result = array_alloc(bdd_variableId, 0);
01100   for (i = 0; i < array_n(var_array); i++) {
01101     var = array_fetch(bdd_t *, var_array, i);
01102     array_insert_last(bdd_variableId, result, bdd_top_var_id(var));
01103   }
01104   return result;
01105 }
01106 
01107 unsigned int 
01108 bdd_num_vars(bdd_manager *manager)
01109 {
01110   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
01111   return (cmu_bdd_vars(mgr));
01112 }
01113 
01114 void
01115 bdd_print(bdd_t *f)
01116 {
01117     cmu_bdd_print_bdd(f->mgr, f->node, bdd_naming_fn_none, bdd_terminal_id_fn_none, (pointer) 0, stdout);
01118 }
01119 
01120 void
01121 bdd_print_stats(bdd_manager *manager, FILE *file)
01122 {
01123   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
01124   cmu_bdd_stats(mgr, file);
01125 }
01126 
01134 int
01135 bdd_set_parameters(
01136   bdd_manager *mgr,
01137   avl_tree *valueTable,
01138   FILE *file)
01139 {
01140   (void) fprintf(file, "Functionality not supported yet in the CMU package\n");
01141   return 1;
01142 } /* End of bdd_set_parameters */
01143 
01144 int
01145 bdd_size(bdd_t *f)
01146 {
01147     return ((int) cmu_bdd_size(f->mgr, f->node, 1));
01148 }
01149 
01150 int
01151 bdd_node_size(bdd_node *f)
01152 {
01153   return(0);
01154 }
01155 
01156 long
01157 bdd_size_multiple(array_t *bdd_array)
01158 {
01159     long result;
01160     struct bdd_ **vector_bdd;
01161     bdd_t *f;
01162     int i;
01163     struct bdd_manager_ *mgr;
01164 
01165     if ((bdd_array == NIL(array_t)) || (array_n(bdd_array) == 0))
01166         return 0;
01167 
01168     f = array_fetch(bdd_t*, bdd_array, 0);
01169     mgr = f->mgr;
01170 
01171     vector_bdd = (struct bdd_ **)
01172                         malloc((array_n(bdd_array)+1)*sizeof(struct bdd_ *));
01173 
01174     for(i=0; i<array_n(bdd_array);i++){
01175         f = array_fetch(bdd_t*, bdd_array, i);
01176         vector_bdd[i] = f->node;
01177     }
01178     vector_bdd[array_n(bdd_array)] = 0;
01179     result =  cmu_bdd_size_multiple(mgr, vector_bdd,1);
01180     FREE(vector_bdd);
01181     return result;
01182 }
01183 
01184 bdd_variableId
01185 bdd_top_var_id(bdd_t *f)
01186 {
01187     return ((bdd_variableId) (cmu_bdd_if_id(f->mgr, f->node) - 1));
01188 }
01189 
01190 /*
01191 Miscellaneous -----------------------------------------------------------------
01192 */
01193 
01194 bdd_external_hooks *
01195 bdd_get_external_hooks(bdd_manager *manager)
01196 {
01197   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
01198   return ((bdd_external_hooks *) mgr->hooks);
01199 }
01200 
01201 
01202 void
01203 bdd_set_gc_mode(bdd_manager *manager, boolean no_gc)
01204 {
01205   cmu_bdd_warning("bdd_set_gc_mode: translated to no-op in CMU package");
01206 }
01207 
01208 void 
01209 bdd_dynamic_reordering(bdd_manager *manager, bdd_reorder_type_t
01210                        algorithm_type, bdd_reorder_verbosity_t verbosity) 
01211 {
01212   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
01213     switch(algorithm_type) {
01214     case BDD_REORDER_SIFT:
01215         cmu_bdd_dynamic_reordering(mgr, cmu_bdd_reorder_sift);
01216         break;
01217     case BDD_REORDER_WINDOW:
01218         cmu_bdd_dynamic_reordering(mgr, cmu_bdd_reorder_stable_window3);
01219         break;
01220     case BDD_REORDER_NONE:
01221         cmu_bdd_dynamic_reordering(mgr, cmu_bdd_reorder_none);
01222         break;
01223     default:
01224       fprintf(stderr,"CMU: bdd_dynamic_reordering: unknown algorithm type\n");
01225       fprintf(stderr,"Using SIFT method instead\n");
01226       cmu_bdd_dynamic_reordering(mgr, cmu_bdd_reorder_sift);
01227     }
01228 }
01229 
01230 void 
01231 bdd_dynamic_reordering_zdd(bdd_manager *manager, bdd_reorder_type_t
01232                        algorithm_type, bdd_reorder_verbosity_t verbosity) 
01233 {
01234     return;
01235 }
01236 
01237 void 
01238 bdd_reorder(bdd_manager *manager)
01239 {
01240   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
01241   cmu_bdd_reorder(mgr);
01242 }
01243 
01244 bdd_variableId
01245 bdd_get_id_from_level(bdd_manager *manager, long level)
01246 {
01247   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
01248   struct bdd_ *fn;
01249 
01250   fn = cmu_bdd_var_with_index(mgr, level);
01251   
01252   if (fn == (struct bdd_ *) 0) {
01253     /* variable should always be found, since they are created at bdd_start */
01254     cmu_bdd_fatal("bdd_get_id_from_level: assumption violated");
01255   }
01256   
01257   return ((bdd_variableId)(cmu_bdd_if_id(mgr, fn) - 1 ));
01258   
01259 }
01260 
01261 long
01262 bdd_top_var_level(bdd_manager *manager, bdd_t *fn)
01263 {
01264   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
01265   return cmu_bdd_if_index(mgr, fn->node);
01266 }
01267 
01268 /*
01269  * Return TRUE if f is a cube, else return FALSE.
01270  */
01271 boolean
01272 bdd_is_cube(bdd_t *f)
01273 {
01274   struct bdd_manager_ *manager;
01275 
01276   if (f == NIL(bdd_t)) {
01277         fail("bdd_is_cube: invalid BDD");
01278   }
01279   if(  f->free ) fail ("Freed Bdd passed to bdd_is_cube");
01280   manager = f->mgr;
01281   return ((boolean)cmu_bdd_is_cube(manager, f->node));
01282 }
01283 
01284 bdd_block *
01285 bdd_new_var_block(bdd_t *f, long length)
01286 {
01287   struct bdd_manager_ *manager;
01288   if (f == NIL(bdd_t)) {
01289         fail("bdd_new_var_block: invalid BDD");
01290   }
01291   manager = f->mgr;
01292   return (bdd_block *)cmu_bdd_new_var_block(manager, f->node, length);
01293 }
01294 
01295 bdd_t *
01296 bdd_var_with_index(bdd_manager *manager, int index)
01297 {
01298   return bdd_construct_bdd_t(manager, 
01299                             cmu_bdd_var_with_index((cmu_bdd_manager) manager,
01300                                                    index));
01301 }
01302 
01303 bdd_t *
01304 bdd_compact(bdd_t *f, bdd_t *g)
01305 {
01306     return (NULL);
01307 }
01308 
01309 
01310 bdd_t *
01311 bdd_squeeze(bdd_t *f, bdd_t *g)
01312 {
01313     return (NULL);
01314 }
01315 
01316 double
01317 bdd_correlation(bdd_t *f, bdd_t *g)
01318 {
01319     return (0.0);
01320 }
01321 
01329 int
01330 bdd_reordering_status(
01331   bdd_manager *mgr,
01332   bdd_reorder_type_t *method)
01333 {
01334   return 0;
01335 }
01336 
01345 bdd_t *
01346 bdd_compute_cube(
01347   bdd_manager *mgr,
01348   array_t *vars)
01349 {
01350   return NIL(bdd_t);
01351 }
01352 
01353 bdd_t *
01354 bdd_compute_cube_with_phase(
01355   bdd_manager *mgr,
01356   array_t *vars,
01357   array_t *phase)
01358 {
01359   return NIL(bdd_t);
01360 }
01361 
01362 bdd_t *
01363 bdd_clipping_and_smooth(
01364   bdd_t *f,
01365   bdd_t *g,
01366   array_t *smoothing_vars /* of bdd_t *'s */,
01367   int maxDepth,
01368   int over)
01369 {
01370   return NIL(bdd_t);
01371 }
01372 
01373 bdd_t *
01374 bdd_approx_hb(
01375   bdd_t *f,
01376   bdd_approx_dir_t approxDir,
01377   int numVars,
01378   int threshold)
01379 {
01380   return NIL(bdd_t);
01381 }
01382 
01383 bdd_t *
01384 bdd_approx_sp(
01385   bdd_t *f,
01386   bdd_approx_dir_t approxDir,
01387   int numVars,
01388   int threshold,
01389   int hardlimit)
01390 {
01391   return NIL(bdd_t);
01392 }
01393 
01394 bdd_t *
01395 bdd_approx_ua(
01396   bdd_t *f,
01397   bdd_approx_dir_t approxDir,
01398   int numVars,
01399   int threshold,
01400   int safe,
01401   double quality)
01402 {
01403   return NIL(bdd_t);
01404 }
01405 
01406 bdd_t *
01407 bdd_approx_remap_ua(
01408   bdd_t *f,
01409   bdd_approx_dir_t approxDir,
01410   int numVars,
01411   int threshold,
01412   double quality)
01413 {
01414   return NIL(bdd_t);
01415 }
01416 
01417 bdd_t *
01418 bdd_approx_biased_rua(
01419   bdd_t *f,
01420   bdd_approx_dir_t approxDir,
01421   bdd_t *bias,
01422   int numVars,
01423   int threshold,
01424   double quality,
01425   double quality1)
01426 {
01427   return NIL(bdd_t);
01428 }
01429 
01430 bdd_t *
01431 bdd_approx_compress(
01432   bdd_t *f,
01433   bdd_approx_dir_t approxDir,
01434   int numVars,
01435   int threshold)
01436 {
01437   return NIL(bdd_t);
01438 }
01439 
01440 int
01441 bdd_gen_decomp(
01442   bdd_t *f,
01443   bdd_partition_type_t partType,
01444   bdd_t ***conjArray)
01445 {
01446   return 0;
01447 }
01448 
01449 int
01450 bdd_var_decomp(
01451   bdd_t *f,
01452   bdd_partition_type_t partType,
01453   bdd_t ***conjArray)
01454 {
01455   return 0;
01456 }
01457 
01458 int 
01459 bdd_approx_decomp(
01460   bdd_t *f,
01461   bdd_partition_type_t partType,
01462   bdd_t ***conjArray)
01463 {
01464   return 0;
01465 }
01466 
01467 int
01468 bdd_iter_decomp(
01469   bdd_t *f,
01470   bdd_partition_type_t partType,
01471   bdd_t  ***conjArray)
01472 {
01473   return 0;
01474 }
01475 
01476 bdd_t *
01477 bdd_solve_eqn(
01478   bdd_t *f,
01479   array_t *g,
01480   array_t *unknowns)
01481 {
01482   return NIL(bdd_t);
01483 }
01484 
01485 int
01486 bdd_add_hook(
01487   bdd_manager *mgr,
01488   int (*procedure)(bdd_manager *, char *, void *),
01489   bdd_hook_type_t whichHook)
01490 {
01491   return 0;
01492 }
01493 
01494 int
01495 bdd_remove_hook(
01496   bdd_manager *mgr,
01497   int (*procedure)(bdd_manager *, char *, void *),
01498   bdd_hook_type_t whichHook)
01499 {
01500   return 0;
01501 }
01502 
01503 int
01504 bdd_enable_reordering_reporting(bdd_manager *mgr)
01505 {
01506   return 0;
01507 }
01508 
01509 int
01510 bdd_disable_reordering_reporting(bdd_manager *mgr)
01511 {
01512   return 0;
01513 }
01514 
01515 bdd_reorder_verbosity_t 
01516 bdd_reordering_reporting(bdd_manager *mgr)
01517 {
01518   return BDD_REORDER_VERBOSITY_DEFAULT;
01519 }
01520 
01521 int 
01522 bdd_print_apa_minterm(
01523   FILE *fp,
01524   bdd_t *f,
01525   int nvars,
01526   int precision)
01527 {
01528   return 0;
01529 }
01530 
01531 int 
01532 bdd_apa_compare_ratios(
01533   int nvars,
01534   bdd_t *f1,
01535   bdd_t *f2,
01536   int f1Num,
01537   int f2Num)
01538 {
01539   return 0;
01540 }
01541 
01542 int
01543 bdd_read_node_count(bdd_manager *mgr)
01544 {
01545   return 0;
01546 }
01547 
01548 
01549 int
01550 bdd_reordering_zdd_status(
01551   bdd_manager *mgr,
01552   bdd_reorder_type_t *method)
01553 {
01554   return 0;
01555 }
01556 
01557 
01558 bdd_node *
01559 bdd_bdd_to_add(
01560   bdd_manager *mgr,
01561   bdd_node *fn)
01562 {
01563   return NIL(bdd_node);
01564 }
01565 
01566 bdd_node *
01567 bdd_add_permute(
01568   bdd_manager *mgr,
01569   bdd_node *fn,
01570   int *permut)
01571 {
01572   return NIL(bdd_node);
01573 }
01574 
01575 bdd_node *
01576 bdd_bdd_permute(
01577   bdd_manager *mgr,
01578   bdd_node *fn,
01579   int *permut)
01580 {
01581   return NIL(bdd_node);
01582 }
01583 
01584 void
01585 bdd_ref(bdd_node *fn)
01586 {
01587   return ;
01588 }
01589 
01590 
01591 void
01592 bdd_recursive_deref(bdd_manager *mgr, bdd_node *f)
01593 {
01594   return;
01595 }
01596 
01597 
01598 bdd_node *
01599 bdd_add_exist_abstract(
01600   bdd_manager *mgr,
01601   bdd_node *fn,
01602   bdd_node *vars)
01603 {
01604   return NIL(bdd_node);
01605 }
01606 
01607 
01608 bdd_node *
01609 bdd_add_apply(
01610   bdd_manager *mgr,
01611   bdd_node *(*operation)(bdd_manager *, bdd_node **, bdd_node **),
01612   bdd_node *fn1,
01613   bdd_node *fn2)
01614 {
01615   return NIL(bdd_node);
01616 }
01617 
01618 
01619 bdd_node *
01620 bdd_add_nonsim_compose(
01621   bdd_manager *mgr,
01622   bdd_node *fn,
01623   bdd_node **vector)
01624 {
01625   return NIL(bdd_node);
01626 }
01627 
01628 
01629 bdd_node *
01630 bdd_add_residue(
01631   bdd_manager *mgr,
01632   int n,
01633   int m,
01634   int options,
01635   int top)
01636 {
01637   return NIL(bdd_node);
01638 }
01639 
01640 
01641 bdd_node *
01642 bdd_add_vector_compose(
01643   bdd_manager *mgr,
01644   bdd_node *fn,
01645   bdd_node **vector)
01646 {
01647   return NIL(bdd_node);
01648 }
01649 
01650 
01651 bdd_node *
01652 bdd_add_times(
01653   bdd_manager *mgr,
01654   bdd_node **fn1,
01655   bdd_node **fn2)
01656 {
01657   return NIL(bdd_node);
01658 }
01659   
01660 
01661 int
01662 bdd_check_zero_ref(bdd_manager *mgr)
01663 {
01664   return 0;
01665 }
01666 
01667 
01668 void
01669 bdd_dynamic_reordering_disable(bdd_manager *mgr)
01670 {
01671   return;
01672 }
01673 
01674 void
01675 bdd_dynamic_reordering_zdd_disable(bdd_manager *mgr)
01676 {
01677   return;
01678 }
01679 
01680 
01681 bdd_node *
01682 bdd_add_xnor(
01683   bdd_manager *mgr,
01684   bdd_node **fn1,
01685   bdd_node **fn2)
01686 {
01687   return NIL(bdd_node);
01688 }
01689 
01690 
01691 int
01692 bdd_shuffle_heap(
01693   bdd_manager *mgr,
01694   int *permut)
01695 {
01696   return 0;
01697 }
01698 
01699 
01700 bdd_node *
01701 bdd_add_compose(
01702   bdd_manager *mgr,
01703   bdd_node *fn1,
01704   bdd_node *fn2,
01705   int var)
01706 {
01707   return NIL(bdd_node);
01708 }
01709 
01710 
01711 bdd_node *
01712 bdd_add_ith_var(
01713   bdd_manager *mgr,
01714   int i)
01715 {
01716   return NIL(bdd_node);
01717 }
01718 
01719 
01720 int
01721 bdd_get_level_from_id(
01722   bdd_manager *mgr,
01723   int id)
01724 {
01725   return 0;
01726 }
01727 
01728 
01729 bdd_node *
01730 bdd_bdd_exist_abstract(
01731   bdd_manager *mgr,
01732   bdd_node *fn,
01733   bdd_node *cube)
01734 {
01735   return NIL(bdd_node);
01736 }
01737 
01738 
01739 int
01740 bdd_equal_sup_norm(
01741   bdd_manager *mgr,
01742   bdd_node *fn,
01743   bdd_node *gn,
01744   BDD_VALUE_TYPE tolerance,
01745   int pr)
01746 {
01747   return 0;
01748 }
01749 
01750 
01751 bdd_node *
01752 bdd_read_logic_zero(bdd_manager *mgr)
01753 {
01754     return NIL(bdd_node);
01755 }
01756 
01757 
01758 bdd_node *
01759 bdd_bdd_ith_var(bdd_manager *mgr, int i)
01760 {
01761     return NIL(bdd_node);
01762 }
01763 
01764 
01765 bdd_node *
01766 bdd_add_divide(
01767   bdd_manager *mgr,
01768   bdd_node **fn1,
01769   bdd_node **fn2)
01770 {
01771   return NIL(bdd_node);
01772 }
01773 
01774 
01775 bdd_node *
01776 bdd_bdd_constrain(
01777   bdd_manager *mgr,
01778   bdd_node *f,
01779   bdd_node *c)
01780 {
01781     return NIL(bdd_node);
01782 }
01783 
01784 bdd_node *
01785 bdd_bdd_restrict(
01786   bdd_manager *mgr,
01787   bdd_node *f,
01788   bdd_node *c)
01789 {
01790     return NIL(bdd_node);
01791 }
01792 
01793 
01794 bdd_node *
01795 bdd_add_hamming(
01796   bdd_manager *mgr,
01797   bdd_node **xVars,
01798   bdd_node **yVars,
01799   int nVars)
01800 {
01801     return NIL(bdd_node);
01802 }
01803 
01804 
01805 bdd_node *
01806 bdd_add_ite(
01807   bdd_manager *mgr,
01808   bdd_node *f,
01809   bdd_node *g,
01810   bdd_node *h)
01811 {
01812     return NIL(bdd_node);
01813 }
01814 
01815 
01816 bdd_node *
01817 bdd_add_find_max(
01818   bdd_manager *mgr,
01819   bdd_node *f)
01820 {
01821     return NIL(bdd_node);
01822 }
01823 
01824 
01825 int
01826 bdd_bdd_pick_one_cube(
01827   bdd_manager *mgr,
01828   bdd_node *node,
01829   char *string)
01830 {
01831     return 0;
01832 }
01833 
01834 
01835 bdd_node *
01836 bdd_add_swap_variables(
01837   bdd_manager *mgr,
01838   bdd_node *f,
01839   bdd_node **x,
01840   bdd_node **y,
01841   int n)
01842 {
01843     return NIL(bdd_node);
01844 }
01845 
01846 bdd_node *
01847 bdd_bdd_swap_variables(
01848   bdd_manager *mgr,
01849   bdd_node *f,
01850   bdd_node **x,
01851   bdd_node **y,
01852   int n)
01853 {
01854     return NIL(bdd_node);
01855 }
01856 
01857 
01858 bdd_node *
01859 bdd_bdd_or(
01860   bdd_manager *mgr,
01861   bdd_node *f,
01862   bdd_node *g)
01863 {
01864     return NIL(bdd_node);
01865 }
01866 
01867 
01868 bdd_node *
01869 bdd_bdd_compute_cube(
01870   bdd_manager *mgr,
01871   bdd_node **vars,
01872   int *phase,
01873   int n)
01874 {
01875     return NIL(bdd_node);
01876 }
01877 
01878 
01879 bdd_node *
01880 bdd_indices_to_cube(
01881   bdd_manager *mgr,
01882   int *idArray,
01883   int n)
01884 {
01885     return NIL(bdd_node);
01886 }
01887 
01888 bdd_node *
01889 bdd_bdd_and(
01890   bdd_manager *mgr,
01891   bdd_node *f,
01892   bdd_node *g)
01893 {
01894     return NIL(bdd_node);
01895 }
01896 
01897 
01898 bdd_node *
01899 bdd_add_matrix_multiply(
01900   bdd_manager *mgr,
01901   bdd_node *A,
01902   bdd_node *B,
01903   bdd_node **z,
01904   int nz)
01905 {
01906     return NIL(bdd_node);
01907 }
01908 
01909 
01910 bdd_node *
01911 bdd_add_compute_cube(
01912   bdd_manager *mgr,
01913   bdd_node **vars,
01914   int *phase,
01915   int n)
01916 {
01917     return NIL(bdd_node);
01918 }
01919 
01920 
01921 bdd_node *
01922 bdd_add_const(
01923   bdd_manager *mgr,
01924   BDD_VALUE_TYPE c)
01925 {
01926     return NIL(bdd_node);
01927 }
01928 
01929 
01930 double
01931 bdd_count_minterm(
01932   bdd_manager *mgr,
01933   bdd_node *f,
01934   int n)
01935 {
01936     return 0;
01937 }
01938 
01939 
01940 bdd_node *
01941 bdd_add_bdd_threshold(
01942   bdd_manager *mgr,
01943   bdd_node *f,
01944   BDD_VALUE_TYPE value)
01945 {
01946     return NIL(bdd_node);
01947 }
01948 
01949 
01950 bdd_node *
01951 bdd_add_bdd_strict_threshold(
01952   bdd_manager *mgr,
01953   bdd_node *f,
01954   BDD_VALUE_TYPE value)
01955 {
01956     return NIL(bdd_node);
01957 }
01958 
01959 BDD_VALUE_TYPE
01960 bdd_read_epsilon(bdd_manager *mgr)
01961 {
01962     return 0;
01963 }
01964 
01965 bdd_node *
01966 bdd_read_one(bdd_manager *mgr)
01967 {
01968     return NIL(bdd_node);
01969 }
01970 
01971 
01972 bdd_node *
01973 bdd_bdd_pick_one_minterm(
01974   bdd_manager *mgr,
01975   bdd_node *f,
01976   bdd_node **vars,
01977   int n)
01978 {
01979     return NIL(bdd_node);
01980 }
01981 
01982 
01983 bdd_t *
01984 bdd_pick_one_minterm(
01985   bdd_t *f,
01986   array_t *varsArray)
01987 {
01988     return NIL(bdd_t);
01989 }
01990 
01991 
01992 array_t *
01993 bdd_bdd_pick_arbitrary_minterms(
01994   bdd_t *f,
01995   array_t *varsArray,
01996   int n,
01997   int k)
01998 {
01999     return NIL(array_t);
02000 }
02001 
02002 bdd_node *
02003 bdd_read_zero(bdd_manager *mgr)
02004 {
02005     return NIL(bdd_node);
02006 }
02007 
02008 
02009 bdd_node *
02010 bdd_bdd_new_var(bdd_manager *mgr)
02011 {
02012     return NIL(bdd_node);
02013 }
02014 
02015 
02016 bdd_node *
02017 bdd_bdd_and_abstract(
02018   bdd_manager *mgr,
02019   bdd_node *f,
02020   bdd_node *g,
02021   bdd_node *cube)
02022 {
02023     return NIL(bdd_node);
02024 }
02025 
02026 void
02027 bdd_deref(bdd_node *f)
02028 {
02029 }
02030 
02031 bdd_node *
02032 bdd_add_plus(
02033   bdd_manager *mgr,
02034   bdd_node **fn1,
02035   bdd_node **fn2)
02036 {
02037   return NIL(bdd_node);
02038 }
02039 
02040 
02041 int
02042 bdd_read_reorderings(bdd_manager *mgr)
02043 {
02044     return 0;
02045 }
02046 
02047 int
02048 bdd_read_next_reordering(bdd_manager *mgr)
02049 {
02050     return 0;
02051 }
02052 
02053 void
02054 bdd_set_next_reordering(bdd_manager *mgr, int next)
02055 {
02056 }
02057 
02058 
02059 bdd_node *
02060 bdd_bdd_xnor(
02061   bdd_manager *mgr,
02062   bdd_node *f,
02063   bdd_node *g)
02064 {
02065     return NIL(bdd_node);
02066 }
02067 
02068 bdd_node *
02069 bdd_bdd_vector_compose(
02070   bdd_manager *mgr,
02071   bdd_node *f,
02072   bdd_node **vector)
02073 {
02074     return NIL(bdd_node);
02075 }
02076 
02077 bdd_node *
02078 bdd_extract_node_as_is(bdd_t *fn)
02079 {
02080   return NIL(bdd_node);
02081 }
02082 
02083 
02084 bdd_node *
02085 bdd_zdd_get_node(
02086   bdd_manager *mgr,
02087   int id,
02088   bdd_node *g,
02089   bdd_node *h)
02090 {
02091     return NIL(bdd_node);
02092 }
02093 
02094 bdd_node *
02095 bdd_zdd_product(
02096   bdd_manager *mgr,
02097   bdd_node *f,
02098   bdd_node *g)
02099 {
02100     return NIL(bdd_node);
02101 }
02102 
02103 bdd_node *
02104 bdd_zdd_product_recur(
02105   bdd_manager *mgr,
02106   bdd_node *f,
02107   bdd_node *g)
02108 {
02109     return NIL(bdd_node);
02110 }
02111 
02112 
02113 bdd_node *
02114 bdd_zdd_union(
02115   bdd_manager *mgr,
02116   bdd_node *f,
02117   bdd_node *g)
02118 {
02119   return NIL(bdd_node);
02120 }
02121 
02122 
02123 bdd_node *
02124 bdd_zdd_weak_div(
02125   bdd_manager *mgr,
02126   bdd_node *f,
02127   bdd_node *g)
02128 {
02129     return NIL(bdd_node);
02130 }
02131 
02132 bdd_node *
02133 bdd_zdd_weak_div_recur(
02134   bdd_manager *mgr,
02135   bdd_node *f,
02136   bdd_node *g)
02137 {
02138     return NIL(bdd_node);
02139 }
02140 
02141 bdd_node *
02142 bdd_zdd_isop_recur(
02143   bdd_manager *mgr,
02144   bdd_node *L,
02145   bdd_node *U,
02146   bdd_node **zdd_I)
02147 {
02148     return NIL(bdd_node);
02149 }
02150 
02151 
02152 bdd_node *
02153 bdd_zdd_isop(
02154   bdd_manager *mgr,
02155   bdd_node *L,
02156   bdd_node *U,
02157   bdd_node **zdd_I)
02158 {
02159     return NIL(bdd_node);
02160 }
02161 
02162 int
02163 bdd_zdd_get_cofactors3(
02164   bdd_manager *mgr,
02165   bdd_node *f,
02166   int v,
02167   bdd_node **f1,
02168   bdd_node **f0,
02169   bdd_node **fd)
02170 {
02171     return 0;
02172 }
02173 
02174 bdd_node *
02175 bdd_bdd_and_recur(
02176   bdd_manager *mgr,
02177   bdd_node *f,
02178   bdd_node *g)
02179 {
02180      return NIL(bdd_node);
02181 }
02182 
02183 bdd_node *
02184 bdd_unique_inter(
02185   bdd_manager *mgr,
02186   int v,
02187   bdd_node *f,
02188   bdd_node *g)
02189 {
02190      return NIL(bdd_node);
02191 }
02192 
02193 bdd_node *
02194 bdd_unique_inter_ivo(
02195   bdd_manager *mgr,
02196   int v,
02197   bdd_node *f,
02198   bdd_node *g)
02199 {
02200      return NIL(bdd_node);
02201 }
02202 
02203 
02204 bdd_node *
02205 bdd_zdd_diff(
02206   bdd_manager *mgr,
02207   bdd_node *f,
02208   bdd_node *g)
02209 {
02210     return NIL(bdd_node);
02211 } 
02212 
02213 bdd_node *
02214 bdd_zdd_diff_recur(
02215   bdd_manager *mgr,
02216   bdd_node *f,
02217   bdd_node *g)
02218 {
02219     return NIL(bdd_node);
02220 } 
02221 
02222 int
02223 bdd_num_zdd_vars(bdd_manager *mgr)
02224 {
02225     return -1;
02226 }
02227 
02228 bdd_node *
02229 bdd_regular(bdd_node *f)
02230 {
02231     return NIL(bdd_node);
02232 }
02233 
02234 int
02235 bdd_is_constant(bdd_node *f)
02236 {
02237     return 0;
02238 }
02239 
02240 int
02241 bdd_is_complement(bdd_node *f)
02242 {
02243     return 0;
02244 }
02245 
02246 bdd_node *
02247 bdd_bdd_T(bdd_node *f)
02248 {
02249     return NIL(bdd_node);
02250 }
02251 
02252 bdd_node *
02253 bdd_bdd_E(bdd_node *f)
02254 {
02255     return NIL(bdd_node);
02256 }
02257 
02258 bdd_node *
02259 bdd_not_bdd_node(bdd_node *f)
02260 {
02261     return NIL(bdd_node);
02262 } 
02263 
02264 void
02265 bdd_recursive_deref_zdd(bdd_manager *mgr, bdd_node *f)
02266 {
02267     return;
02268 } 
02269 
02270 int
02271 bdd_zdd_count(bdd_manager *mgr, bdd_node *f)
02272 {
02273     return 0;
02274 }
02275 
02276 int
02277 bdd_read_zdd_level(bdd_manager *mgr, int index)
02278 {
02279     return -1;
02280 } 
02281 
02282 int
02283 bdd_zdd_vars_from_bdd_vars(bdd_manager *mgr, int multiplicity)
02284 {
02285    return 0;
02286 } 
02287 
02288 void
02289 bdd_zdd_realign_enable(bdd_manager *mgr)
02290 {
02291     return;
02292 } 
02293 
02294 void
02295 bdd_zdd_realign_disable(bdd_manager *mgr)
02296 {
02297     return;
02298 } 
02299 
02300 int
02301 bdd_zdd_realignment_enabled(bdd_manager *mgr)
02302 {
02303     return 0;
02304 } 
02305 
02306 void
02307 bdd_realign_enable(bdd_manager *mgr)
02308 {
02309     return;
02310 } 
02311 
02312 void
02313 bdd_realign_disable(bdd_manager *mgr)
02314 {
02315     return;
02316 } 
02317 
02318 int
02319 bdd_realignment_enabled(bdd_manager *mgr)
02320 {
02321     return 0;
02322 } 
02323 
02324 int
02325 bdd_node_read_index(bdd_node *f)
02326 {
02327     return -1;
02328 }
02329 
02330 bdd_node *
02331 bdd_read_next(bdd_node *f)
02332 {
02333     return NIL(bdd_node);
02334 }
02335 
02336 
02337 void
02338 bdd_set_next(bdd_node *f, bdd_node *g)
02339 {
02340     return;
02341 }
02342 
02343 
02344 int
02345 bdd_read_reordered_field(bdd_manager *mgr)
02346 {
02347     return -1;
02348 }
02349 
02350 void
02351 bdd_set_reordered_field(bdd_manager *mgr, int n)
02352 {
02353     return;
02354 }
02355 
02356 bdd_node *
02357 bdd_add_apply_recur(
02358   bdd_manager *mgr,
02359   bdd_node *(*operation)(bdd_manager *, bdd_node **, bdd_node **),
02360   bdd_node *fn1,
02361   bdd_node *fn2)
02362 {
02363     return NIL(bdd_node);
02364 }
02365 
02366 BDD_VALUE_TYPE
02367 bdd_add_value(bdd_node *f)
02368 {
02369     return 0.0; 
02370 }
02371 
02372 int
02373 bdd_print_minterm(bdd_t *f)
02374 {
02375   return 0;
02376 }
02377 
02378 int
02379 bdd_print_cover(bdd_t *f)
02380 {
02381   return 0;
02382 }
02383 
02384 bdd_t *
02385 bdd_xor_smooth(
02386   bdd_t *f,
02387   bdd_t *g,
02388   array_t *smoothing_vars)
02389 {
02390     return NIL(bdd_t);
02391 }
02392 
02393 
02394 bdd_node *
02395 bdd_read_plus_infinity(bdd_manager *mgr)
02396 {
02397     return NIL(bdd_node);
02398 
02399 } /* end of bdd_read_plus_infinity */
02400 
02401 
02402 bdd_node *
02403 bdd_priority_select(
02404   bdd_manager *mgr,
02405   bdd_node *R,
02406   bdd_node **x,
02407   bdd_node **y,
02408   bdd_node **z,
02409   bdd_node *Pi,
02410   int n,
02411   bdd_node *(*Pifunc)(bdd_manager *, int, bdd_node **, bdd_node **, bdd_node **))
02412 {
02413     return NIL(bdd_node);
02414 
02415 } /* end of bdd_priority_select */
02416 
02417 
02418 void
02419 bdd_set_background(
02420   bdd_manager *mgr,
02421   bdd_node *f)
02422 {
02423     return;
02424  
02425 } /* end of bdd_set_background */
02426 
02427 
02428 bdd_node *
02429 bdd_read_background(bdd_manager *mgr)
02430 {
02431   return NIL(bdd_node);
02432 
02433 } /* end of bdd_read_background */
02434 
02435 
02436 bdd_node *
02437 bdd_bdd_cofactor(
02438   bdd_manager *mgr,
02439   bdd_node *f,
02440   bdd_node *g)
02441 {
02442     return NIL(bdd_node);
02443 
02444 } /* end of bdd_bdd_cofactor */
02445 
02446 
02447 bdd_node *
02448 bdd_bdd_ite(
02449   bdd_manager *mgr,
02450   bdd_node *f,
02451   bdd_node *g,
02452   bdd_node *h)
02453 {
02454     return NIL(bdd_node);
02455 
02456 } /* end of bdd_bdd_ite */
02457 
02458 
02459 bdd_node *
02460 bdd_add_minus(
02461   bdd_manager *mgr,
02462   bdd_node **fn1,
02463   bdd_node **fn2)
02464 {
02465     return NIL(bdd_node);
02466 
02467 } /* end of bdd_add_plus */
02468 
02469 
02470 bdd_node *
02471 bdd_dxygtdxz(
02472   bdd_manager *mgr,
02473   int N,
02474   bdd_node **x,
02475   bdd_node **y,
02476   bdd_node **z)
02477 {
02478     return NIL(bdd_node);
02479 
02480 } /* end of bdd_dxygtdxz */
02481 
02482 
02483 bdd_node *
02484 bdd_bdd_univ_abstract(
02485   bdd_manager *mgr,
02486   bdd_node *fn,
02487   bdd_node *vars)
02488 {
02489     return NIL(bdd_node);
02490 
02491 } /* end of bdd_bdd_univ_abstract */
02492 
02493 
02494 bdd_node *
02495 bdd_bdd_cprojection(
02496   bdd_manager *mgr,
02497   bdd_node *R,
02498   bdd_node *Y)
02499 {
02500     return NIL(bdd_node);
02501 
02502 } /* end of bdd_bdd_cprojection */
02503 
02504 bdd_node *
02505 bdd_xeqy(
02506   bdd_manager *mgr,
02507   int N,
02508   bdd_node **x,
02509   bdd_node **y)
02510 {
02511   return NIL(bdd_node);
02512 
02513 } /* end of bdd_xeqy */
02514 
02515 bdd_node *
02516 bdd_add_roundoff(
02517   bdd_manager *mgr,
02518   bdd_node *f,
02519   int N)
02520 {
02521   return NIL(bdd_node);
02522 
02523 } /* end of bdd_add_roundoff */
02524 
02525 bdd_node *
02526 bdd_xgty(
02527   bdd_manager *mgr,
02528   int N,
02529   bdd_node **x,
02530   bdd_node **y)
02531 {
02532   return NIL(bdd_node);
02533 
02534 } /* end of bdd_xgty */
02535 
02536 bdd_node *
02537 bdd_add_cmpl(
02538   bdd_manager *mgr,
02539   bdd_node *f)
02540 {
02541   return NIL(bdd_node);
02542 
02543 } /* end of bdd_add_cmpl */
02544 
02545 bdd_node *
02546 bdd_split_set(
02547   bdd_manager *mgr,
02548   bdd_node *f,
02549   bdd_node **x,
02550   int n,
02551   double m)
02552 {
02553   return NIL(bdd_node);
02554 
02555 } /* end of bdd_split_set */
02556 
02557 
02558 int
02559 bdd_debug_check(bdd_manager *mgr)
02560 {
02561     return (-1);
02562 
02563 } /* end of bdd_debug_check */
02564 
02565 bdd_node *
02566 bdd_bdd_xor(
02567   bdd_manager *mgr,
02568   bdd_node *f,
02569   bdd_node *g)
02570 {
02571     return NIL(bdd_node);
02572 }
02573 
02574 void 
02575 bdd_dump_blif(
02576   bdd_manager *mgr,
02577   int nBdds,
02578   bdd_node **bdds,
02579   char **inames,
02580   char **onames,
02581   char *model,
02582   FILE *fp)
02583 {
02584   return;
02585 }
02586 
02587 void 
02588 bdd_dump_blif_body(
02589   bdd_manager *mgr,
02590   int nBdds,
02591   bdd_node **bdds,
02592   char **inames,
02593   char **onames,
02594   FILE *fp)
02595 {
02596   return;
02597 }
02598 
02599 void 
02600 bdd_dump_dot(
02601   bdd_manager *mgr,
02602   int nBdds,
02603   bdd_node **bdds,
02604   char **inames,
02605   char **onames,
02606   FILE *fp)
02607 {
02608   return;
02609 }
02610 
02611 bdd_node *
02612 bdd_make_bdd_from_zdd_cover(bdd_manager *mgr, bdd_node *node)
02613 {
02614     return(NIL(bdd_node));
02615 }
02616 
02617 bdd_node *
02618 bdd_zdd_complement(bdd_manager *mgr, bdd_node *node)
02619 {
02620     return(NIL(bdd_node));
02621 }
02622 
02623 bdd_node *
02624 bdd_bdd_vector_support(
02625   bdd_manager *mgr,
02626   bdd_node **F,
02627   int n)
02628 {
02629   return NIL(bdd_node);
02630 }
02631 
02632 int
02633 bdd_bdd_vector_support_size(
02634   bdd_manager *mgr,
02635   bdd_node **F,
02636   int n)
02637 {
02638   return -1;
02639 }
02640 
02641 int
02642 bdd_bdd_support_size(
02643   bdd_manager *mgr,
02644   bdd_node *F)
02645 {
02646   return -1;
02647 }
02648 
02649 bdd_node *
02650 bdd_bdd_support(
02651   bdd_manager *mgr,
02652   bdd_node *F)
02653 {
02654   return NIL(bdd_node);
02655 }
02656 
02657 bdd_node *
02658 bdd_add_general_vector_compose(
02659   bdd_manager *mgr,
02660   bdd_node *f,
02661   bdd_node **vectorOn,
02662   bdd_node **vectorOff)
02663 {
02664   return NIL(bdd_node);
02665 }
02666 
02667 int
02668 bdd_bdd_leq(
02669   bdd_manager *mgr,
02670   bdd_node *f,
02671   bdd_node *g)
02672 {
02673   return -1;
02674 } 
02675 
02676 bdd_node *
02677 bdd_bdd_boolean_diff(
02678   bdd_manager *mgr,
02679   bdd_node *f,
02680   int x)
02681 {
02682   return NIL(bdd_node);
02683 }
02684 
02692 int
02693 bdd_ptrcmp(bdd_t *f, bdd_t *g)
02694 {
02695   if (f->node == g->node)
02696     return(0);
02697   else
02698     return(1);
02699 }
02700 
02701 
02709 int
02710 bdd_ptrhash(bdd_t *f, int size)
02711 {
02712   int hash;
02713 
02714   hash = (int)((unsigned long)f->node >> 2) % size;
02715   return(hash);
02716 }
02717 
02718 bdd_t *
02719 bdd_subset_with_mask_vars(
02720   bdd_t *f,
02721   array_t *varsArray,
02722   array_t *maskVarsArray)
02723 {
02724   return NIL(bdd_t);
02725 }
02726 
02727 bdd_t *
02728 bdd_and_smooth_with_cube(
02729   bdd_t *f,
02730   bdd_t *g,
02731   bdd_t *cube)
02732 {
02733   return NIL(bdd_t);
02734 }
02735 
02736 bdd_t *
02737 bdd_smooth_with_cube(bdd_t *f, bdd_t *cube)
02738 {
02739   int i;
02740   bdd_t *var, *res;
02741   array_t *smoothingVars;
02742   var_set_t *supportVarSet;
02743 
02744   smoothingVars = array_alloc(bdd_t *, 0);
02745   supportVarSet = bdd_get_support(f);
02746   for (i = 0; i < supportVarSet->n_elts; i++) {
02747     if (var_set_get_elt(supportVarSet, i) == 1) {
02748       var = bdd_var_with_index(f->mgr, i);
02749       array_insert_last(bdd_t *, smoothingVars, var);
02750     }
02751   }
02752   var_set_free(supportVarSet);
02753 
02754   res = bdd_smooth(f, smoothingVars);
02755 
02756   for (i = 0; i < array_n(smoothingVars); i++) {
02757     var = array_fetch(bdd_t *, smoothingVars, i);
02758     bdd_free(var);
02759   }
02760   array_free(smoothingVars);
02761   return res;
02762 }
02763 
02764 bdd_t *
02765 bdd_substitute_with_permut(bdd_t *f, int *permut)
02766 {
02767   return NIL(bdd_t);
02768 }
02769 
02770 array_t *
02771 bdd_substitute_array_with_permut(
02772   array_t *f_array,
02773   int *permut)
02774 {
02775   return NIL(array_t);
02776 }
02777 
02778 bdd_t *
02779 bdd_vector_compose(
02780   bdd_t *f,
02781   array_t *varArray,
02782   array_t *funcArray)
02783 {
02784   return NIL(bdd_t);
02785 }
02786 
02787 double *
02788 bdd_cof_minterm(bdd_t *f)
02789 {
02790   return(NIL(double));
02791 }
02792 
02793 int
02794 bdd_var_is_dependent(bdd_t *f, bdd_t *var)
02795 {
02796   return(0);
02797 }
02798 
02799 array_t *
02800 bdd_find_essential(bdd_t *f)
02801 {
02802   return(NIL(array_t));
02803 }
02804 
02805 bdd_t *
02806 bdd_find_essential_cube(bdd_t *f)
02807 {
02808   return(NIL(bdd_t));
02809 }
02810 
02811 int
02812 bdd_estimate_cofactor(bdd_t *f, bdd_t *var, int phase)
02813 {
02814   return(0);
02815 }
02816 
02817 long
02818 bdd_read_peak_memory(bdd_manager *mgr)
02819 {
02820   return(0);
02821 }
02822 
02823 int
02824 bdd_read_peak_live_node(bdd_manager *mgr)
02825 {
02826   return(0);
02827 }
02828 
02829 int
02830 bdd_set_pi_var(bdd_manager *mgr, int index)
02831 {
02832     return(0);
02833 }
02834 
02835 int
02836 bdd_set_ps_var(bdd_manager *mgr, int index)
02837 {
02838     return(0);
02839 }
02840 
02841 int
02842 bdd_set_ns_var(bdd_manager *mgr, int index)
02843 {
02844     return(0);
02845 }
02846 
02847 int
02848 bdd_is_pi_var(bdd_manager *mgr, int index)
02849 {
02850     return(0);
02851 }
02852 
02853 int
02854 bdd_is_ps_var(bdd_manager *mgr, int index)
02855 {
02856     return(0);
02857 }
02858 
02859 int
02860 bdd_is_ns_var(bdd_manager *mgr, int index)
02861 {
02862     return(0);
02863 }
02864 
02865 int
02866 bdd_set_pair_index(bdd_manager *mgr, int index, int pairIndex)
02867 {
02868     return(0);
02869 }
02870 
02871 int
02872 bdd_read_pair_index(bdd_manager *mgr, int index)
02873 {
02874     return(0);
02875 }
02876 
02877 int
02878 bdd_set_var_to_be_grouped(bdd_manager *mgr, int index)
02879 {
02880     return(0);
02881 }
02882 
02883 int
02884 bdd_set_var_hard_group(bdd_manager *mgr, int index)
02885 {
02886     return(0);
02887 }
02888 
02889 int
02890 bdd_reset_var_to_be_grouped(bdd_manager *mgr, int index)
02891 {
02892     return(0);
02893 }
02894 
02895 int
02896 bdd_is_var_to_be_grouped(bdd_manager *mgr, int index)
02897 {
02898     return(0);
02899 }
02900 
02901 int
02902 bdd_is_var_hard_group(bdd_manager *mgr, int index)
02903 {
02904     return(0);
02905 }
02906 
02907 int
02908 bdd_is_var_to_be_ungrouped(bdd_manager *mgr, int index)
02909 {
02910     return(0);
02911 }
02912 
02913 int
02914 bdd_set_var_to_be_ungrouped(bdd_manager *mgr, int index)
02915 {
02916     return(0);
02917 }
02918 
02919 int
02920 bdd_bind_var(bdd_manager *mgr, int index)
02921 {
02922     return(0);
02923 }
02924 
02925 int
02926 bdd_unbind_var(bdd_manager *mgr, int index)
02927 {
02928     return(0);
02929 }
02930 
02931 int
02932 bdd_is_lazy_sift(bdd_manager *mgr)
02933 {
02934     return(0);
02935 }
02936 
02937 void
02938 bdd_discard_all_var_groups(bdd_manager *mgr)
02939 {
02940     return;
02941 }
02942 
02943 /*---------------------------------------------------------------------------*/
02944 /* Definition of internal functions                                          */
02945 /*---------------------------------------------------------------------------*/
02946 
02947 
02948 /*---------------------------------------------------------------------------*/
02949 /* Definition of static functions                                            */
02950 /*---------------------------------------------------------------------------*/
02951 
02952 
02953