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

00001 
00035 #include "calPortInt.h"
00036 #ifndef EPD_MAX_BIN
00037 #include "epd.h"
00038 #endif
00039 
00040 /*---------------------------------------------------------------------------*/
00041 /* Constant declarations                                                     */
00042 /*---------------------------------------------------------------------------*/
00043 
00044 
00045 /*---------------------------------------------------------------------------*/
00046 /* Type declarations                                                         */
00047 /*---------------------------------------------------------------------------*/
00048 
00049 
00050 /*---------------------------------------------------------------------------*/
00051 /* Structure declarations                                                    */
00052 /*---------------------------------------------------------------------------*/
00053 
00054 
00055 /*---------------------------------------------------------------------------*/
00056 /* Variable declarations                                                     */
00057 /*---------------------------------------------------------------------------*/
00058 
00059 
00060 /*---------------------------------------------------------------------------*/
00061 /* Macro declarations                                                        */
00062 /*---------------------------------------------------------------------------*/
00063 
00064 
00067 /*---------------------------------------------------------------------------*/
00068 /* Static function prototypes                                                */
00069 /*---------------------------------------------------------------------------*/
00070 
00071 static void InvalidType(FILE *file, char *field, char *expected);
00072 
00076 /*---------------------------------------------------------------------------*/
00077 /* Definition of exported functions                                          */
00078 /*---------------------------------------------------------------------------*/
00079 
00091 bdd_t *
00092 bdd_construct_bdd_t(bdd_manager *mgr, bdd_node *fn)
00093 {
00094   bdd_t *result;
00095   if (!fn){
00096         fail("bdd_construct_bdd_t: possible memory overflow");
00097   }
00098   result = Cal_MemAlloc(bdd_t, 1);
00099   result->bddManager = (Cal_BddManager_t *) mgr;
00100   result->calBdd = (Cal_Bdd) fn;
00101   result->free = 0;
00102   return result;
00103 }
00114 bdd_package_type_t
00115 bdd_get_package_name(void)
00116 {
00117   return CAL;
00118 }
00119 
00120 
00131 void
00132 bdd_end(void *manager)
00133 {
00134   Cal_BddManager mgr = (Cal_BddManager) manager;
00135   void *hooks;
00136   hooks = Cal_BddManagerGetHooks(mgr);
00137   Cal_MemFree(hooks);
00138   Cal_BddManagerQuit(mgr);
00139 }
00140 
00151 bdd_manager *
00152 bdd_start(int nvariables)
00153 {
00154   Cal_BddManager mgr;
00155   int i;
00156   bdd_external_hooks *hooks;
00157 
00158   mgr = Cal_BddManagerInit();
00159   for (i = 0; i < nvariables; i++) {
00160         (void) Cal_BddManagerCreateNewVarLast(mgr);
00161   }
00162   hooks = Cal_MemAlloc(bdd_external_hooks, 1);
00163   hooks->mdd = hooks->network = hooks->undef1 = (char *) 0;
00164   Cal_BddManagerSetHooks(mgr, (void *)hooks);
00165   return (bdd_manager *)mgr;
00166 }
00167 
00168 
00179 bdd_t *
00180 bdd_create_variable(bdd_manager *manager)
00181 {
00182   Cal_BddManager mgr = (Cal_BddManager) manager;
00183   return bdd_construct_bdd_t(mgr, Cal_BddManagerCreateNewVarLast(mgr));
00184 }
00185 
00196 bdd_t *
00197 bdd_create_variable_after(bdd_manager *manager, bdd_variableId afterId)
00198 {
00199   Cal_Bdd afterVar;
00200   bdd_t *result;
00201   Cal_BddManager mgr = (Cal_BddManager) manager;
00202   afterVar = Cal_BddManagerGetVarWithId(mgr, afterId + 1);
00203   result =  bdd_construct_bdd_t(mgr,
00204                                 Cal_BddManagerCreateNewVarAfter(mgr,
00205                                                                 afterVar));
00206 
00207   /* No need to free after_var, since single variable BDDs are never garbage collected */
00208 
00209   return result;
00210 }
00211 
00212 
00213 
00224 bdd_t *
00225 bdd_get_variable(bdd_manager *manager, bdd_variableId varId)
00226 {
00227   Cal_Bdd varBdd;
00228   Cal_BddManager mgr = (Cal_BddManager) manager;
00229   unsigned int numVars = Cal_BddVars(mgr);
00230   if (varId + 1 < numVars) {
00231     varBdd = Cal_BddManagerGetVarWithId(mgr, varId + 1);
00232   } else {
00233     int i;
00234     for (i=numVars, varBdd = NULL; i <= varId + 1; i++) {
00235       varBdd = Cal_BddManagerCreateNewVarLast(mgr);
00236     }
00237   }
00238   return bdd_construct_bdd_t(mgr, varBdd);
00239 }
00240 
00251 bdd_t *
00252 bdd_dup(bdd_t *f)
00253 {
00254   return bdd_construct_bdd_t(f->bddManager, Cal_BddIdentity(f->bddManager, f->calBdd));
00255 }
00256 
00267 void
00268 bdd_free(bdd_t *f)
00269 {
00270   if (f == NIL(bdd_t)) {
00271         fail("bdd_free: trying to free a NIL bdd_t");
00272   }
00273   if (f->free){
00274     fail("bdd_free: Trying to free a freed bdd_t");
00275   }
00276   Cal_BddFree(f->bddManager, f->calBdd);
00277   f->calBdd = (Cal_Bdd) 0;
00278   f->bddManager = NIL(Cal_BddManager_t);
00279   f->free = 1;
00280   Cal_MemFree(f);
00281 }
00282 
00293 bdd_node *
00294 bdd_get_node(bdd_t *f, boolean *isComplemented)
00295 {
00296   *isComplemented = CAL_TAG0(f->calBdd);
00297   return (f->calBdd);
00298 }
00299 
00310 bdd_t *
00311 bdd_and(bdd_t *f,bdd_t *g, boolean f_phase, boolean g_phase)
00312 {
00313   Cal_Bdd temp1, temp2;
00314   bdd_t *result;
00315   Cal_BddManager mgr;
00316 
00317   mgr = f->bddManager;
00318   temp1 = ((f_phase == TRUE) ? Cal_BddIdentity(mgr, f->calBdd) :
00319            Cal_BddNot(mgr, f->calBdd));
00320   temp2 = ((g_phase == TRUE) ? Cal_BddIdentity(mgr, g->calBdd) :
00321            Cal_BddNot(mgr, g->calBdd));
00322   result = bdd_construct_bdd_t(mgr, Cal_BddAnd(mgr, temp1, temp2));
00323   Cal_BddFree(mgr, temp1);
00324   Cal_BddFree(mgr, temp2);
00325   return result;
00326 }
00327 
00339 bdd_t *
00340 bdd_and_with_limit(bdd_t *f, bdd_t *g, boolean f_phase, boolean g_phase, unsigned int limit)
00341 {
00342   return bdd_and(f, g, f_phase, g_phase);
00343 }
00344 
00345 bdd_t *
00346 bdd_and_array(bdd_t *f, array_t *g_array, boolean f_phase, boolean g_phase)
00347 {
00348   Cal_Bdd temp1, temp2, result;
00349   bdd_t *g;
00350   Cal_BddManager mgr;
00351   int i;
00352 
00353   mgr = f->bddManager;
00354   result = ((f_phase == TRUE) ? Cal_BddIdentity(mgr, f->calBdd) :
00355             Cal_BddNot(mgr, f->calBdd));
00356 
00357   for (i = 0; i < array_n(g_array); i++) {
00358     g = array_fetch(bdd_t *, g_array, i);
00359     temp1 = result;
00360     temp2 = ((g_phase == TRUE) ? Cal_BddIdentity(mgr, g->calBdd) :
00361              Cal_BddNot(mgr, g->calBdd));
00362     result = Cal_BddAnd(mgr, temp1, temp2);
00363     Cal_BddFree(mgr, temp1);
00364     Cal_BddFree(mgr, temp2);
00365     if (result == NULL)
00366       return(NULL);
00367   }
00368 
00369   return(bdd_construct_bdd_t(mgr, result));
00370 }
00371 
00382 bdd_t *
00383 bdd_multiway_and(bdd_manager *manager, array_t *bddArray)
00384 {
00385   int i;
00386   Cal_Bdd *calBddArray;
00387   bdd_t *operand, *result;
00388   Cal_BddManager mgr = (Cal_BddManager) manager;
00389 
00390   calBddArray = Cal_MemAlloc(Cal_Bdd, array_n(bddArray)+1);
00391   for (i=0; i<array_n(bddArray); i++){
00392     operand = array_fetch(bdd_t*, bddArray, i);
00393     calBddArray[i] = operand->calBdd;
00394   }
00395   calBddArray[i] = (Cal_Bdd)0;
00396   result = bdd_construct_bdd_t(mgr,
00397                                Cal_BddMultiwayAnd(mgr, calBddArray));
00398   Cal_MemFree(calBddArray);
00399   return result;
00400 }
00401 
00412 bdd_t *
00413 bdd_multiway_or(bdd_manager *manager, array_t *bddArray)
00414 {
00415   int i;
00416   Cal_Bdd *calBddArray;
00417   bdd_t *operand, *result;
00418   Cal_BddManager mgr = (Cal_BddManager) manager;
00419 
00420   calBddArray = Cal_MemAlloc(Cal_Bdd, array_n(bddArray)+1);
00421   for (i=0; i<array_n(bddArray); i++){
00422     operand = array_fetch(bdd_t*, bddArray, i);
00423     calBddArray[i] = operand->calBdd;
00424   }
00425   calBddArray[i] = (Cal_Bdd)0;
00426   result = bdd_construct_bdd_t(mgr,
00427                                Cal_BddMultiwayOr(mgr, calBddArray));
00428   Cal_MemFree(calBddArray);
00429   return result;
00430 }
00431 
00442 bdd_t *
00443 bdd_multiway_xor(bdd_manager *manager, array_t *bddArray)
00444 {
00445   int i;
00446   Cal_Bdd *calBddArray;
00447   bdd_t *operand, *result;
00448   Cal_BddManager mgr = (Cal_BddManager) manager;
00449 
00450   calBddArray = Cal_MemAlloc(Cal_Bdd, array_n(bddArray)+1);
00451   for (i=0; i<array_n(bddArray); i++){
00452     operand = array_fetch(bdd_t*, bddArray, i);
00453     calBddArray[i] = operand->calBdd;
00454   }
00455   calBddArray[i] = (Cal_Bdd)0;
00456   result = bdd_construct_bdd_t(mgr,
00457                                Cal_BddMultiwayXor(mgr, calBddArray));
00458   Cal_MemFree(calBddArray);
00459   return result;
00460 }
00461 
00472 array_t *
00473 bdd_pairwise_and(bdd_manager *manager, array_t *bddArray1,
00474                  array_t *bddArray2)
00475 {
00476   int i;
00477   array_t *resultArray;
00478   Cal_Bdd *calBddArray, *calBddResultArray;
00479   bdd_t *operand;
00480   Cal_BddManager mgr = (Cal_BddManager) manager;
00481 
00482   if (array_n(bddArray1) != array_n(bddArray2)){
00483     fprintf(stderr, "bdd_pairwise_and: Arrays of different lengths.\n");
00484     return NIL(array_t);
00485   }
00486   calBddArray = Cal_MemAlloc(Cal_Bdd, 2*array_n(bddArray1)+1);
00487   for (i=0; i<array_n(bddArray1); i++){
00488     operand = array_fetch(bdd_t*, bddArray1, i);
00489     calBddArray[i<<1] = operand->calBdd;
00490     operand = array_fetch(bdd_t*, bddArray2, i);
00491     calBddArray[(i<<1)+1] = operand->calBdd;
00492   }
00493   calBddArray[i<<1] = (Cal_Bdd)0;
00494   calBddResultArray = Cal_BddPairwiseAnd(mgr, calBddArray);
00495   resultArray = array_alloc(bdd_t*, 0);
00496   for (i=0; i<array_n(bddArray1); i++){
00497     array_insert_last(bdd_t *, resultArray,
00498                       bdd_construct_bdd_t(mgr, calBddResultArray[i]));
00499   }
00500   Cal_MemFree(calBddArray);
00501   Cal_MemFree(calBddResultArray);
00502   return resultArray;
00503 }
00504 
00515 array_t *
00516 bdd_pairwise_or(bdd_manager *manager, array_t *bddArray1,
00517                 array_t *bddArray2)
00518 {
00519   int i;
00520   array_t *resultArray;
00521   Cal_Bdd *calBddArray, *calBddResultArray;
00522   bdd_t *operand;
00523   Cal_BddManager mgr = (Cal_BddManager) manager;
00524 
00525   if (array_n(bddArray1) != array_n(bddArray2)){
00526     fprintf(stderr, "bdd_pairwise_or: Arrays of different lengths.\n");
00527     return NIL(array_t);
00528   }
00529   calBddArray = Cal_MemAlloc(Cal_Bdd, 2*array_n(bddArray1)+1);
00530   for (i=0; i<array_n(bddArray1); i++){
00531     operand = array_fetch(bdd_t*, bddArray1, i);
00532     calBddArray[i<<1] = operand->calBdd;
00533     operand = array_fetch(bdd_t*, bddArray2, i);
00534     calBddArray[(i<<1)+1] = operand->calBdd;
00535   }
00536   calBddArray[i<<1] = (Cal_Bdd)0;
00537   calBddResultArray = Cal_BddPairwiseOr(mgr, calBddArray);
00538   resultArray = array_alloc(bdd_t*, 0);
00539   for (i=0; i<array_n(bddArray1); i++){
00540     array_insert_last(bdd_t *, resultArray,
00541                       bdd_construct_bdd_t(mgr, calBddResultArray[i]));
00542   }
00543   Cal_MemFree(calBddArray);
00544   Cal_MemFree(calBddResultArray);
00545   return resultArray;
00546 }
00547 
00548 
00559 array_t *
00560 bdd_pairwise_xor(bdd_manager *manager, array_t *bddArray1,
00561                  array_t *bddArray2)
00562 {
00563   int i;
00564   array_t *resultArray;
00565   Cal_Bdd *calBddArray, *calBddResultArray;
00566   bdd_t *operand;
00567   Cal_BddManager mgr = (Cal_BddManager) manager;
00568 
00569   if (array_n(bddArray1) != array_n(bddArray2)){
00570     fprintf(stderr, "bdd_pairwise_xor: Arrays of different lengths.\n");
00571     return NIL(array_t);
00572   }
00573   calBddArray = Cal_MemAlloc(Cal_Bdd, 2*array_n(bddArray1)+1);
00574   for (i=0; i<array_n(bddArray1); i++){
00575     operand = array_fetch(bdd_t*, bddArray1, i);
00576     calBddArray[i<<1] = operand->calBdd;
00577     operand = array_fetch(bdd_t*, bddArray2, i);
00578     calBddArray[(i<<1)+1] = operand->calBdd;
00579   }
00580   calBddArray[i<<1] = (Cal_Bdd)0;
00581   calBddResultArray = Cal_BddPairwiseXor(mgr, calBddArray);
00582   resultArray = array_alloc(bdd_t*, 0);
00583   for (i=0; i<array_n(bddArray1); i++){
00584     array_insert_last(bdd_t *, resultArray,
00585                       bdd_construct_bdd_t(mgr, calBddResultArray[i]));
00586   }
00587   Cal_MemFree(calBddArray);
00588   Cal_MemFree(calBddResultArray);
00589   return resultArray;
00590 }
00591 
00602 bdd_t *
00603 bdd_and_smooth(bdd_t *f, bdd_t *g, array_t *smoothingVars)
00604 {
00605   int num_vars, i;
00606   bdd_t *fn, *result;
00607   Cal_Bdd *assoc;
00608   Cal_BddManager mgr;
00609   int assocId;
00610 
00611   num_vars = array_n(smoothingVars);
00612   if (num_vars == 0) {
00613     fprintf(stderr,"bdd_and_smooth: no smoothing variables");
00614     return bdd_and(f, g, 1, 1);
00615   }
00616   mgr = f->bddManager;
00617   assoc = Cal_MemAlloc(Cal_Bdd, num_vars+1);
00618   for (i = 0; i < num_vars; i++) {
00619         fn = array_fetch(bdd_t *, smoothingVars, i);
00620         assoc[i] = fn->calBdd;
00621   }
00622   assoc[num_vars] = 0;
00623   assocId = Cal_AssociationInit(mgr, assoc, 0);
00624   Cal_AssociationSetCurrent(mgr, assocId);
00625   result = bdd_construct_bdd_t(mgr, Cal_BddRelProd(mgr, f->calBdd, g->calBdd));
00626   Cal_MemFree(assoc);
00627   return result;
00628 }
00629 
00641 bdd_t *
00642 bdd_and_smooth_with_limit(bdd_t *f, bdd_t *g, array_t *smoothingVars, unsigned int limit)
00643 {
00644   return bdd_and_smooth(f, g, smoothingVars);
00645 }
00646 
00657 bdd_t *
00658 bdd_between(bdd_t *fMin, bdd_t *fMax)
00659 {
00660   return bdd_construct_bdd_t(fMin->bddManager,
00661                              Cal_BddBetween(fMin->bddManager,
00662                                             fMin->calBdd,
00663                                             fMax->calBdd));
00664 }
00675 bdd_t *
00676 bdd_cofactor(bdd_t *f,bdd_t *g)
00677 {
00678   return bdd_construct_bdd_t(f->bddManager,
00679                              Cal_BddCofactor(f->bddManager,
00680                                              f->calBdd,
00681                                              g->calBdd));
00682 }
00683 
00684 bdd_t *
00685 bdd_cofactor_array(bdd_t *f, array_t *bddArray)
00686 {
00687   bdd_t *operand;
00688   Cal_Bdd result, temp;
00689   int i;
00690 
00691   result = Cal_BddIdentity(f->bddManager, f->calBdd);
00692 
00693   for (i = 0; i < array_n(bddArray); i++) {
00694     operand = array_fetch(bdd_t *, bddArray, i);
00695     temp = Cal_BddCofactor(f->bddManager, result, operand->calBdd);
00696     if (temp == NULL) {
00697       Cal_BddFree(f->bddManager, result);
00698       return(NULL);
00699     }
00700     Cal_BddFree(f->bddManager, result);
00701     result = temp;
00702   }
00703 
00704   return(bdd_construct_bdd_t(f->bddManager, result));
00705 }
00706 
00717 bdd_t *
00718 bdd_compose(bdd_t *f,bdd_t *v,bdd_t *g)
00719 {
00720   return bdd_construct_bdd_t(f->bddManager,
00721                              Cal_BddCompose(f->bddManager,
00722                                             f->calBdd,
00723                                             v->calBdd,
00724                                             g->calBdd));
00725 }
00726 
00737 bdd_t *
00738 bdd_consensus(bdd_t *f, array_t *quantifyingVars)
00739 {
00740   int num_vars, i;
00741   bdd_t *fn, *result;
00742   Cal_Bdd *assoc;
00743   Cal_BddManager mgr;
00744 
00745   num_vars = array_n(quantifyingVars);
00746   if (num_vars == 0) {
00747     fprintf(stderr, "bdd_consensus: no smoothing variables");
00748     return f;
00749   }
00750   mgr = f->bddManager;
00751   assoc = Cal_MemAlloc(Cal_Bdd, num_vars+1);
00752   for (i = 0; i < num_vars; i++) {
00753         fn = array_fetch(bdd_t *, quantifyingVars, i);
00754         assoc[i] = fn->calBdd;
00755   }
00756   assoc[num_vars] = 0;
00757   Cal_TempAssociationInit(mgr, assoc, 0);
00758   Cal_AssociationSetCurrent(mgr, -1);
00759   result = bdd_construct_bdd_t(mgr, Cal_BddForAll(mgr, f->calBdd));
00760   Cal_MemFree(assoc);
00761   Cal_TempAssociationQuit(mgr);
00762   return result;
00763 }
00764 
00775 bdd_t *
00776 bdd_cproject(bdd_t *f,array_t *quantifyingVars)
00777 {
00778   return NIL(bdd_t);
00779 
00780   /*
00781   int num_vars, i;
00782   bdd_t *fn, *result;
00783   Cal_Bdd_t*assoc;
00784   Cal_BddManager mgr;
00785 
00786   if (f == NIL(bdd_t))
00787         fail ("bdd_cproject: invalid BDD");
00788 
00789   num_vars = array_n(quantifying_vars);
00790   if (num_vars <= 0) {
00791       printf("Warning: bdd_cproject: no projection variables\n");
00792       result = bdd_dup(f);
00793   }
00794   else {
00795     assoc = Cal_MemAlloc(Cal_Bdd_t, num_vars+1);
00796     for (i = 0; i < num_vars; i++) {
00797       fn = array_fetch(bdd_t *, quantifying_vars, i);
00798       assoc[i] = fn->calBdd;
00799     }
00800     assoc[num_vars] = (struct bdd_ *) 0;
00801     mgr = f->bddManager;
00802     cmu_bdd_temp_assoc(mgr, assoc, 0);
00803     (void) cmu_bdd_assoc(mgr, -1);
00804     result = bdd_construct_bdd_t(mgr, cmu_bdd_project(mgr, f->calBdd));
00805     Cal_MemFree(assoc);
00806   }
00807   return result;
00808   */
00809 }
00810 
00821 bdd_t *
00822 bdd_else(bdd_t *f)
00823 {
00824   return bdd_construct_bdd_t(f->bddManager, Cal_BddElse(f->bddManager, f->calBdd));
00825 }
00826 
00837 bdd_t *
00838 bdd_ite(bdd_t *i,bdd_t *t,bdd_t *e,boolean i_phase,
00839         boolean t_phase,boolean e_phase)
00840 {
00841   Cal_Bdd temp1, temp2, temp3;
00842   bdd_t *result;
00843   Cal_BddManager mgr;
00844 
00845   mgr = i->bddManager;
00846   temp1 = (i_phase ? Cal_BddIdentity(mgr, i->calBdd) : Cal_BddNot(mgr, i->calBdd));
00847   temp2 = (t_phase ? Cal_BddIdentity(mgr, t->calBdd) : Cal_BddNot(mgr, t->calBdd));
00848   temp3 = (e_phase ? Cal_BddIdentity(mgr, e->calBdd) : Cal_BddNot(mgr, e->calBdd));
00849   result = bdd_construct_bdd_t(mgr, Cal_BddITE(mgr, temp1, temp2, temp3));
00850   Cal_BddFree(mgr, temp1);
00851   Cal_BddFree(mgr, temp2);
00852   Cal_BddFree(mgr, temp3);
00853   return result;
00854 }
00855 
00866 bdd_t *
00867 bdd_minimize(bdd_t *f, bdd_t *c)
00868 {
00869   return bdd_construct_bdd_t(f->bddManager,
00870                              Cal_BddReduce(f->bddManager,
00871                                            f->calBdd, c->calBdd));
00872 }
00873 
00874 bdd_t *
00875 bdd_minimize_array(bdd_t *f, array_t *bddArray)
00876 {
00877   bdd_t *operand;
00878   Cal_Bdd result, temp;
00879   int i;
00880 
00881   result = Cal_BddIdentity(f->bddManager, f->calBdd);
00882   for (i = 0; i < array_n(bddArray); i++) {
00883     operand = array_fetch(bdd_t *, bddArray, i);
00884     temp = Cal_BddReduce(f->bddManager, result, operand->calBdd);
00885     if (temp == NULL) {
00886       Cal_BddFree(f->bddManager, result);
00887       return(NULL);
00888     }
00889     Cal_BddFree(f->bddManager, result);
00890     result = temp;
00891   }
00892 
00893   return(bdd_construct_bdd_t(f->bddManager, result));
00894 }
00895 
00906 bdd_t *
00907 bdd_not(bdd_t *f)
00908 {
00909   return bdd_construct_bdd_t(f->bddManager, Cal_BddNot(f->bddManager, f->calBdd));
00910 }
00911 
00922 bdd_t *
00923 bdd_one(bdd_manager *manager)
00924 {
00925   Cal_BddManager mgr = (Cal_BddManager) manager;
00926   return bdd_construct_bdd_t(mgr, Cal_BddOne(mgr));
00927 }
00928 
00939 bdd_t *
00940 bdd_or(bdd_t *f, bdd_t *g, boolean f_phase, boolean g_phase)
00941 {
00942   Cal_Bdd temp1, temp2;
00943   bdd_t *result;
00944   Cal_BddManager mgr;
00945 
00946   mgr = f->bddManager;
00947   temp1 = (f_phase ? Cal_BddIdentity(mgr, f->calBdd) : Cal_BddNot(mgr, f->calBdd));
00948   temp2 = (g_phase ? Cal_BddIdentity(mgr, g->calBdd) : Cal_BddNot(mgr, g->calBdd));
00949   result = bdd_construct_bdd_t(mgr, Cal_BddOr(mgr, temp1, temp2));
00950   Cal_BddFree(mgr, temp1);
00951   Cal_BddFree(mgr, temp2);
00952   return result;
00953 }
00954 
00965 bdd_t *
00966 bdd_smooth(bdd_t *f, array_t *smoothingVars)
00967 {
00968   int numVars, i;
00969   bdd_t *fn, *result;
00970   Cal_Bdd *assoc;
00971   Cal_BddManager mgr;
00972   int assocId;
00973 
00974   numVars = array_n(smoothingVars);
00975   if (numVars == 0) {
00976         fprintf(stderr,"bdd_smooth: no smoothing variables");
00977     return f;
00978   }
00979   mgr = f->bddManager;
00980   assoc = Cal_MemAlloc(Cal_Bdd, numVars+1);
00981   for (i = 0; i < numVars; i++) {
00982         fn = array_fetch(bdd_t *, smoothingVars, i);
00983         assoc[i] = fn->calBdd;
00984   }
00985   assoc[numVars] = 0;
00986   assocId = Cal_AssociationInit(mgr, assoc, 0);
00987   (void) Cal_AssociationSetCurrent(mgr, assocId);  /* set the temp
00988                                                  association as the
00989                                                  current association
00990                                                  */
00991   result = bdd_construct_bdd_t(mgr, Cal_BddExists(mgr, f->calBdd));
00992   Cal_MemFree(assoc);
00993   return result;
00994 }
00995 
01006 bdd_t *
01007 bdd_substitute(bdd_t *f, array_t *old_array, array_t *new_array)
01008 {
01009   int num_old_vars, num_new_vars, i;
01010   bdd_t *fn_old, *fn_new, *result;
01011   Cal_Bdd *assoc;
01012   Cal_BddManager mgr;
01013   int assocId;
01014 
01015   num_old_vars = array_n(old_array);
01016   num_new_vars = array_n(new_array);
01017   if (num_old_vars != num_new_vars) {
01018         fprintf(stderr,"bdd_substitute: mismatch of number of new and old variables");
01019     exit(-1);
01020   }
01021   mgr = f->bddManager;
01022   assoc = Cal_MemAlloc(Cal_Bdd, 2*num_old_vars+1);
01023   for (i = 0; i < num_old_vars; i++) {
01024         fn_old = array_fetch(bdd_t *, old_array, i);
01025         fn_new = array_fetch(bdd_t *, new_array, i);
01026         assoc[2*i]   = fn_old->calBdd;
01027         assoc[2*i+1] = fn_new->calBdd;
01028   }
01029   assoc[2*num_old_vars] = 0;
01030   assocId = Cal_AssociationInit(mgr, assoc, 1);
01031   (void) Cal_AssociationSetCurrent(mgr, assocId);
01032   result = bdd_construct_bdd_t(mgr, Cal_BddSubstitute(mgr, f->calBdd));
01033   Cal_MemFree(assoc);
01034   Cal_TempAssociationQuit(mgr);
01035   return result;
01036 }
01037 
01038 array_t *
01039 bdd_substitute_array(array_t *f_array, array_t *old_array, array_t *new_array)
01040 {
01041   int   i;
01042   bdd_t *f, *new_;
01043   array_t *substitute_array = array_alloc(bdd_t *, 0);
01044 
01045   arrayForEachItem(bdd_t *, f_array, i, f) {
01046     new_ = bdd_substitute(f, old_array, new_array);
01047     array_insert_last(bdd_t *, substitute_array, new_);
01048   }
01049   return(substitute_array);
01050 }
01051 
01063 void *
01064 bdd_pointer(bdd_t *f)
01065 {
01066     return((void *)f->calBdd);
01067 }
01068 
01079 bdd_t *
01080 bdd_then(bdd_t *f)
01081 {
01082   return bdd_construct_bdd_t(f->bddManager, Cal_BddThen(f->bddManager, f->calBdd));
01083 }
01084 
01095 bdd_t *
01096 bdd_top_var(bdd_t *f)
01097 {
01098   return bdd_construct_bdd_t(f->bddManager, Cal_BddIf(f->bddManager, f->calBdd));
01099 }
01100 
01111 bdd_t *
01112 bdd_xnor(bdd_t *f,bdd_t *g)
01113 {
01114   return bdd_construct_bdd_t(f->bddManager, Cal_BddXnor(f->bddManager, f->calBdd, g->calBdd));
01115 }
01116 
01127 bdd_t *
01128 bdd_xor(bdd_t *f,bdd_t *g)
01129 {
01130   return bdd_construct_bdd_t(f->bddManager, Cal_BddXor(f->bddManager, f->calBdd, g->calBdd));
01131 }
01132 
01143 bdd_t *
01144 bdd_zero(bdd_manager *manager)
01145 {
01146   Cal_BddManager mgr = (Cal_BddManager) manager;
01147   return bdd_construct_bdd_t(mgr, Cal_BddZero(mgr));
01148 }
01149 
01150 /*
01151 Queries about BDD Formulas ----------------------------------------------------
01152 */
01153 
01164 boolean
01165 bdd_equal(bdd_t *f,bdd_t *g)
01166 {
01167   return Cal_BddIsEqual(f->bddManager, f->calBdd, g->calBdd);
01168 }
01169 
01180 boolean
01181 bdd_equal_mod_care_set(bdd_t *f, bdd_t *g, bdd_t *CareSet)
01182 {
01183   bdd_t *diffBdd;
01184   boolean result;
01185 
01186   if (bdd_equal(f, g))
01187     return 1;
01188 
01189   diffBdd = bdd_xor(f, g);
01190 
01191   result = bdd_leq(diffBdd, CareSet, 1, 0);
01192   bdd_free(diffBdd);
01193 
01194   return(result);
01195 }
01196 
01207 bdd_t *
01208 bdd_intersects(bdd_t *f,bdd_t *g)
01209 {
01210   return bdd_construct_bdd_t(f->bddManager, Cal_BddIntersects(f->bddManager,
01211                                                        f->calBdd,
01212                                                        g->calBdd));
01213 }
01214 
01225 bdd_t *
01226 bdd_closest_cube(bdd_t *f,bdd_t *g,int *dist)
01227 {
01228   return NIL(bdd_t);
01229 }
01230 
01241 boolean
01242 bdd_is_tautology(bdd_t *f, boolean phase)
01243 {
01244   return ((phase == TRUE) ? Cal_BddIsBddOne(f->bddManager, f->calBdd):
01245           Cal_BddIsBddZero(f->bddManager, f->calBdd));
01246 
01247 }
01248 
01259 boolean
01260 bdd_leq(bdd_t *f, bdd_t *g, boolean f_phase, boolean g_phase)
01261 {
01262   Cal_Bdd temp1, temp2, impliesFn;
01263   Cal_BddManager mgr;
01264   boolean resultValue;
01265 
01266   mgr = f->bddManager;
01267   temp1 = (f_phase ? Cal_BddIdentity(mgr, f->calBdd) : Cal_BddNot(mgr, f->calBdd));
01268   temp2 = (g_phase ? Cal_BddIdentity(mgr, g->calBdd) : Cal_BddNot(mgr, g->calBdd));
01269   impliesFn = Cal_BddImplies(mgr, temp1, temp2); /* returns a minterm
01270                                                      of temp1*!temp2
01271                                                      */
01272   resultValue = Cal_BddIsBddZero(mgr, impliesFn);
01273   Cal_BddFree(mgr, temp1);
01274   Cal_BddFree(mgr, temp2);
01275   Cal_BddFree(mgr, impliesFn);
01276   return resultValue;
01277 }
01278 
01289 boolean
01290 bdd_lequal_mod_care_set(
01291   bdd_t *f,
01292   bdd_t *g,
01293   boolean f_phase,
01294   boolean g_phase,
01295   bdd_t *careSet)
01296 {
01297   bdd_t *temp;
01298   boolean result;
01299 
01300   if (bdd_leq(f, g, f_phase, g_phase))
01301     return 1;
01302 
01303   temp = bdd_and(f, careSet, f_phase, 1);
01304 
01305   result = bdd_leq(temp, g, 1, g_phase);
01306   bdd_free(temp);
01307 
01308   return(result);
01309 }
01310 
01321 boolean
01322 bdd_leq_array(bdd_t *f, array_t *g_array, boolean f_phase, boolean g_phase)
01323 {
01324   int   i;
01325   bdd_t *g;
01326   boolean result;
01327 
01328   arrayForEachItem(bdd_t *, g_array, i, g) {
01329     result = bdd_leq(f, g, f_phase, g_phase);
01330     if (g_phase) {
01331       if (!result)
01332         return(0);
01333     } else {
01334       if (result)
01335         return(1);
01336     }
01337   }
01338   if (g_phase)
01339     return(1);
01340   else
01341     return(0);
01342 }
01343 
01354 double
01355 bdd_count_onset(bdd_t *f, array_t *var_array)
01356 {
01357   int numVars;
01358   double fraction;
01359   numVars = array_n(var_array);
01360   fraction = Cal_BddSatisfyingFraction(f->bddManager, f->calBdd);
01361   return (fraction * pow((double) 2, (double) numVars));
01362 }
01370 int
01371 bdd_epd_count_onset(
01372   bdd_t *f,
01373   array_t *var_array /* of bdd_t *'s */,
01374   EpDouble *epd)
01375 {
01376   double nMinterms;
01377 
01378   nMinterms = bdd_count_onset(f, var_array);
01379   EpdConvert(nMinterms, epd);
01380   return 0;
01381 } /* end of bdd_epd_count_onset */
01382 
01393 int
01394 bdd_get_free(bdd_t *f)
01395 {
01396     return (f->free);
01397 }
01398 
01409 bdd_manager *
01410 bdd_get_manager(bdd_t *f)
01411 {
01412     return (bdd_manager *) (f->bddManager);
01413 }
01414 
01415 
01426 var_set_t *
01427 bdd_get_support(bdd_t *f)
01428 {
01429   Cal_Bdd *support, var;
01430   Cal_BddManager mgr;
01431   long num_vars;
01432   var_set_t *result;
01433   int id, i;
01434 
01435   mgr = f->bddManager;
01436   num_vars = Cal_BddVars(mgr);
01437   result = var_set_new((int) num_vars);
01438   support = Cal_MemAlloc(Cal_Bdd, (num_vars+1) * sizeof(Cal_Bdd));
01439   for (i = 0; i <= num_vars; ++i) {
01440         support[i] = 0;
01441   }
01442 
01443   (void) Cal_BddSupport(mgr, f->calBdd, support);
01444   for (i = 0; i < num_vars; ++i) {
01445         var = support[i];
01446         if (var) {
01447       id = (int) (Cal_BddGetIfId(mgr, var) - 1);
01448       var_set_set_elt(result, id);
01449     }
01450   }
01451 
01452   Cal_MemFree(support);
01453   return result;
01454 }
01455 
01456 
01464 int
01465 bdd_is_support_var(bdd_t *f, bdd_t *var)
01466 {
01467     return(bdd_is_support_var_id(f, bdd_top_var_id(var)));
01468 }
01469 
01470 
01478 int
01479 bdd_is_support_var_id(bdd_t *f, int index)
01480 {
01481   Cal_Bdd *support, var;
01482   Cal_BddManager mgr;
01483   long num_vars;
01484   int id, i;
01485 
01486   mgr = f->bddManager;
01487   num_vars = Cal_BddVars(mgr);
01488   support = Cal_MemAlloc(Cal_Bdd, (num_vars+1) * sizeof(Cal_Bdd));
01489   for (i = 0; i <= num_vars; ++i) {
01490     support[i] = 0;
01491   }
01492 
01493   (void) Cal_BddSupport(mgr, f->calBdd, support);
01494   for (i = 0; i < num_vars; ++i) {
01495     var = support[i];
01496     if (var) {
01497       id = (int) (Cal_BddGetIfId(mgr, var) - 1);
01498       if (id == index) {
01499         Cal_MemFree(support);
01500         return 1;
01501       }
01502     }
01503   }
01504 
01505   Cal_MemFree(support);
01506   return 0;
01507 }
01508 
01509 
01520 array_t *
01521 bdd_get_varids(array_t *var_array)
01522 {
01523   int i;
01524   bdd_t *var;
01525   array_t *result;
01526   bdd_variableId varId;
01527 
01528   result = array_alloc(bdd_variableId, 0);
01529   for (i = 0; i < array_n(var_array); i++) {
01530     var = array_fetch(bdd_t *, var_array, i);
01531     varId = (int) bdd_top_var_id(var);
01532     array_insert_last(bdd_variableId, result, varId);
01533   }
01534   return result;
01535 }
01536 
01547 unsigned int
01548 bdd_num_vars(bdd_manager *manager)
01549 {
01550   Cal_BddManager mgr = (Cal_BddManager) manager;
01551   return (Cal_BddVars(mgr));
01552 }
01553 
01564 void
01565 bdd_print(bdd_t *f)
01566 {
01567   Cal_BddPrintBdd(f->bddManager, f->calBdd, Cal_BddNamingFnNone,
01568                   Cal_BddTerminalIdFnNone, (Cal_Pointer_t) 0, (FILE *)stdout);
01569 }
01570 
01581 void
01582 bdd_print_stats(bdd_manager *manager, FILE *file)
01583 {
01584   Cal_BddManager mgr = (Cal_BddManager) manager;
01585   Cal_BddManagerGC(mgr);
01586   Cal_BddStats(mgr, file);
01587 }
01588 
01599 int
01600 bdd_size(bdd_t *f)
01601 {
01602   return ((int) Cal_BddSize(f->bddManager, f->calBdd, 1));
01603 }
01604 
01605 
01613 int
01614 bdd_node_size(bdd_node *f)
01615 {
01616     return(0);
01617 
01618 } /* end of bdd_node_size */
01619 
01630 long
01631 bdd_size_multiple(array_t *bdd_array)
01632 {
01633   long result;
01634   Cal_Bdd *vector_bdd;
01635   bdd_t *f;
01636   int i;
01637   Cal_BddManager mgr;
01638 
01639   if ((bdd_array == NIL(array_t)) || (array_n(bdd_array) == 0))
01640     return 0;
01641 
01642   f = array_fetch(bdd_t*, bdd_array, 0);
01643   mgr = f->bddManager;
01644   vector_bdd = Cal_MemAlloc(Cal_Bdd, array_n(bdd_array)+1);
01645   for(i=0; i<array_n(bdd_array);i++){
01646     f = array_fetch(bdd_t*, bdd_array, i);
01647     vector_bdd[i] = f->calBdd;
01648   }
01649   vector_bdd[array_n(bdd_array)] = 0;
01650   result =  Cal_BddSizeMultiple(mgr, vector_bdd,1);
01651   Cal_MemFree(vector_bdd);
01652   return result;
01653 }
01654 
01665 bdd_variableId
01666 bdd_top_var_id(bdd_t *f)
01667 {
01668   return ((bdd_variableId) (Cal_BddGetIfId(f->bddManager, f->calBdd) - 1));
01669 }
01670 
01681 bdd_external_hooks *
01682 bdd_get_external_hooks(bdd_manager *manager)
01683 {
01684   Cal_BddManager mgr = (Cal_BddManager) manager;
01685   return (bdd_external_hooks *) Cal_BddManagerGetHooks(mgr);
01686 }
01687 
01698 void
01699 bdd_set_gc_mode(bdd_manager *manager,boolean no_gc)
01700 {
01701   Cal_BddManager mgr = (Cal_BddManager) manager;
01702   Cal_BddSetGCMode(mgr, (int) no_gc);
01703 }
01704 
01715 void
01716 bdd_dynamic_reordering(bdd_manager *manager, bdd_reorder_type_t
01717                        algorithm_type, bdd_reorder_verbosity_t verbosity)
01718 {
01719   Cal_BddManager mgr = (Cal_BddManager) manager;
01720     switch(algorithm_type) {
01721       case BDD_REORDER_SIFT:
01722         Cal_BddDynamicReordering(mgr, CAL_REORDER_SIFT);
01723       break;
01724       case BDD_REORDER_WINDOW:
01725         Cal_BddDynamicReordering(mgr, CAL_REORDER_WINDOW);
01726       break;
01727       case BDD_REORDER_NONE:
01728         Cal_BddDynamicReordering(mgr, CAL_REORDER_NONE);
01729       break;
01730       default:
01731         fprintf(stderr,"CAL: bdd_dynamic_reordering: unknown algorithm type\n");
01732         fprintf(stderr,"Using SIFT method instead\n");
01733         Cal_BddDynamicReordering(mgr, CAL_REORDER_SIFT);
01734     }
01735 
01736 }
01737 
01738 void
01739 bdd_dynamic_reordering_zdd(bdd_manager *manager, bdd_reorder_type_t
01740                        algorithm_type, bdd_reorder_verbosity_t verbosity)
01741 {
01742     return;
01743 }
01744 
01755 void
01756 bdd_reorder(bdd_manager *manager)
01757 {
01758   Cal_BddManager mgr = (Cal_BddManager) manager;
01759   Cal_BddReorder(mgr);
01760 }
01761 
01772 bdd_variableId
01773 bdd_get_id_from_level(bdd_manager *manager, long level)
01774 {
01775   Cal_Bdd fn;
01776   Cal_BddManager mgr = (Cal_BddManager) manager;
01777   fn = Cal_BddManagerGetVarWithIndex(mgr, level);
01778   if (!fn){
01779     /* variable should always be found, since they are created at bdd_start */
01780     fprintf(stderr, "bdd_get_id_from_level: assumption violated");
01781     exit(-1);
01782   }
01783   return ((bdd_variableId)(Cal_BddGetIfId(mgr, fn) - 1 ));
01784 }
01785 
01796 long
01797 bdd_top_var_level(bdd_manager *manager, bdd_t *fn)
01798 {
01799   Cal_BddManager mgr = (Cal_BddManager) manager;
01800   return (long)Cal_BddGetIfIndex(mgr, fn->calBdd);
01801 }
01802 
01803 /*
01804  */
01815 boolean
01816 bdd_is_cube(bdd_t *f)
01817 {
01818   Cal_BddManager mgr;
01819   if (f == NIL(bdd_t)) {
01820     fail("bdd_is_cube: invalid BDD");
01821   }
01822   if(f->free) fail ("Freed Bdd passed to bdd_is_cube");
01823   mgr = f->bddManager;
01824   return ((boolean)Cal_BddIsCube(mgr, f->calBdd));
01825 }
01826 
01837 bdd_block *
01838 bdd_new_var_block(bdd_t *f, long length)
01839 {
01840         return (bdd_block *) Cal_BddNewVarBlock(f->bddManager, f->calBdd, length);
01841 }
01842 
01853 bdd_t *
01854 bdd_var_with_index(bdd_manager *manager, int index)
01855 {
01856   Cal_BddManager mgr = (Cal_BddManager) manager;
01857   return bdd_construct_bdd_t(mgr,
01858                              Cal_BddManagerGetVarWithIndex(mgr,
01859                                                            index));
01860 }
01861 
01862 
01876 int
01877 bdd_set_parameters(
01878   bdd_manager *mgr,
01879   avl_tree *valueTable,
01880   FILE *file)
01881 {
01882   /* int reorderMethod; */
01883   st_table *newValueTable;
01884   st_generator *stgen;
01885   avl_generator *avlgen;
01886   char *paramName;
01887   char *paramValue;
01888   Cal_BddManager bddManager = (Cal_BddManager)mgr;
01889 
01890 
01891   /* Build a new table with the parameter names but with
01892   ** the prefix removed. */
01893   newValueTable = st_init_table(st_ptrcmp, st_ptrhash);
01894   avl_foreach_item(valueTable, avlgen, AVL_FORWARD, (char **)&paramName,
01895                    (char **)&paramValue) {
01896     if (strncmp(paramName, "BDD.", 4) == 0) {
01897       st_insert(newValueTable, (char *)&paramName[4],
01898                 (char *)paramValue);
01899     }
01900   }
01901 
01902   st_foreach_item(newValueTable, stgen, &paramName, &paramValue) {
01903     unsigned int uvalue;
01904     double value;
01905     char *invalidChar;
01906 
01907     invalidChar = NIL(char);
01908 
01909     if (strcmp(paramName, "Node limit") == 0) {
01910       uvalue = (unsigned int) strtol(paramValue, &invalidChar, 10);
01911       /* RB an unsigned will never be < 0 */
01912       if (*invalidChar /*|| uvalue < 0*/) {
01913         InvalidType(file, "Node limit", "unsigned integer");
01914       }
01915       else {
01916         bddManager->nodeLimit = uvalue;
01917       }
01918     }
01919     else if (strcmp(paramName, "Garbage collection enabled") == 0) {
01920       if (strcmp(paramValue, "yes") == 0) {
01921         bddManager->gcMode = 1;
01922       }
01923       else if (strcmp(paramValue, "no") == 0) {
01924         bddManager->gcMode = 0;
01925       }
01926       else {
01927         InvalidType(file, "Garbage collection enabled", "(yes,no)");
01928       }
01929     }
01930     else if (strcmp(paramName,
01931                     "Maximum number of variables sifted per reordering") == 0) {
01932       uvalue = (unsigned int) strtol(paramValue, &invalidChar, 10);
01933       if (*invalidChar /*|| uvalue < 0*/) {
01934         InvalidType(file, "Maximum number of variables sifted per reordering",
01935                     "unsigned integer");
01936       }
01937       else {
01938         bddManager->maxNumVarsSiftedPerReordering = uvalue;
01939       }
01940     }
01941     else if (strcmp(paramName,
01942                     "Maximum number of variable swaps per reordering") == 0) {
01943       uvalue = (unsigned int) strtol(paramValue, &invalidChar, 10);
01944       if (*invalidChar /*|| uvalue < 0*/) {
01945         InvalidType(file, "Maximum number of variable swaps per reordering",
01946                     "unsigned integer");
01947       }
01948       else {
01949         bddManager->maxNumSwapsPerReordering = uvalue;
01950       }
01951     }
01952     else if (strcmp(paramName,
01953                     "Maximum growth while sifting a variable") == 0) {
01954       value = strtod(paramValue, &invalidChar);
01955       if (*invalidChar) {
01956         InvalidType(file, "Maximum growth while sifting a variable",
01957                     "real");
01958       }
01959       else {
01960         bddManager->maxSiftingGrowth = value;
01961       }
01962     }
01963     else if (strcmp(paramName, "Dynamic reordering of BDDs enabled") == 0) {
01964       if (strcmp(paramValue, "yes") == 0) {
01965         bddManager->dynamicReorderingEnableFlag = 1;
01966       }
01967       else if (strcmp(paramValue, "no") == 0) {
01968         bddManager->dynamicReorderingEnableFlag = 0;
01969       }
01970       else {
01971         InvalidType(file, "Dynamic reordering of BDDs enabled",
01972                     "(yes,no)");
01973       }
01974     }
01975     else if (strcmp(paramName, "Use old reordering")
01976              == 0) {
01977       if (strcmp(paramValue, "yes") == 0) {
01978         bddManager->reorderMethod = CAL_REORDER_METHOD_BF;
01979       }
01980       else if (strcmp(paramValue, "no") == 0) {
01981         bddManager->reorderMethod = CAL_REORDER_METHOD_DF;
01982       }
01983       else {
01984         InvalidType(file, "Dynamic reordering of BDDs enabled",
01985                     "(yes,no)");
01986       }
01987     }
01988     else if (strcmp(paramName, "Dynamic reordering threshold") == 0) {
01989       uvalue = (unsigned int) strtol(paramValue, &invalidChar, 10);
01990       if (*invalidChar /*|| uvalue < 0*/) {
01991         InvalidType(file, "Dynamic reordering threshold", "unsigned integer");
01992       }
01993       else {
01994         bddManager->reorderingThreshold = uvalue;
01995       }
01996     }
01997     else if (strcmp(paramName, "Repacking after GC threshold")
01998              == 0) {
01999       value = strtod(paramValue, &invalidChar);
02000       if (*invalidChar || value < 0) {
02001         InvalidType(file, "Repacking after GC threshold", "unsigned real");
02002       }
02003       else {
02004         bddManager->repackAfterGCThreshold = value;
02005       }
02006     }
02007     else if (strcmp(paramName, "Table repacking threshold")
02008              == 0) {
02009       value = strtod(paramValue, &invalidChar);
02010       if (*invalidChar || value < 0) {
02011         InvalidType(file, "Table repacking threshold", "unsigned real");
02012       }
02013       else {
02014         bddManager->tableRepackThreshold = value;
02015       }
02016     }
02017     else {
02018       (void) fprintf(file, "Warning: Parameter %s not recognized.",
02019                      paramName);
02020       (void) fprintf(file, " Ignored.\n");
02021     }
02022   } /* end of st_foreach_item */
02023 
02024   /* Clean up. */
02025   st_free_table(newValueTable);
02026 
02027   return(1);
02028 
02029 } /* end of bdd_set_parameters */
02030 
02038 bdd_t *
02039 bdd_compact(bdd_t *f, bdd_t *g)
02040 {
02041     return 0;
02042 }
02043 
02044 bdd_t *
02045 bdd_squeeze(bdd_t *f, bdd_t *g)
02046 {
02047     return 0;
02048 }
02049 bdd_t *
02050 bdd_clipping_and_smooth(
02051   bdd_t *f,
02052   bdd_t *g,
02053   array_t *smoothing_vars       /* of bdd_t *'s */,
02054   int maxDepth,
02055   int over)
02056 {
02057   return NIL(bdd_t);
02058 }
02059 
02060 bdd_t *
02061 bdd_approx_hb(
02062   bdd_t *f,
02063   bdd_approx_dir_t approxDir,
02064   int numVars,
02065   int threshold)
02066 {
02067   return NIL(bdd_t);
02068 }
02069 
02070 bdd_t *
02071 bdd_approx_sp(
02072   bdd_t *f,
02073   bdd_approx_dir_t approxDir,
02074   int numVars,
02075   int threshold,
02076   int hardlimit)
02077 {
02078   return NIL(bdd_t);
02079 }
02080 
02081 bdd_t *
02082 bdd_approx_ua(
02083   bdd_t *f,
02084   bdd_approx_dir_t approxDir,
02085   int numVars,
02086   int threshold,
02087   int safe,
02088   double quality)
02089 {
02090   return NIL(bdd_t);
02091 }
02092 
02093 bdd_t *
02094 bdd_approx_remap_ua(
02095   bdd_t *f,
02096   bdd_approx_dir_t approxDir,
02097   int numVars,
02098   int threshold,
02099   double quality)
02100 {
02101   return NIL(bdd_t);
02102 }
02103 
02104 bdd_t *
02105 bdd_approx_biased_rua(
02106   bdd_t *f,
02107   bdd_approx_dir_t approxDir,
02108   bdd_t *bias,
02109   int numVars,
02110   int threshold,
02111   double quality,
02112   double quality1)
02113 {
02114   return NIL(bdd_t);
02115 }
02116 
02117 bdd_t *
02118 bdd_approx_compress(
02119   bdd_t *f,
02120   bdd_approx_dir_t approxDir,
02121   int numVars,
02122   int threshold)
02123 {
02124   return NIL(bdd_t);
02125 }
02126 
02127 int
02128 bdd_gen_decomp(
02129   bdd_t *f,
02130   bdd_partition_type_t partType,
02131   bdd_t ***conjArray)
02132 {
02133   return 0;
02134 }
02135 
02136 int
02137 bdd_var_decomp(
02138   bdd_t *f,
02139   bdd_partition_type_t partType,
02140   bdd_t ***conjArray)
02141 {
02142   return 0;
02143 }
02144 
02145 int
02146 bdd_approx_decomp(
02147   bdd_t *f,
02148   bdd_partition_type_t partType,
02149   bdd_t ***conjArray)
02150 {
02151   return 0;
02152 }
02153 
02154 int
02155 bdd_add_hook(
02156   bdd_manager *mgr,
02157   int (*procedure)(bdd_manager *, char *, void *),
02158   bdd_hook_type_t whichHook)
02159 {
02160   return 0;
02161 }
02162 
02163 int
02164 bdd_remove_hook(
02165   bdd_manager *mgr,
02166   int (*procedure)(bdd_manager *, char *, void *),
02167   bdd_hook_type_t whichHook)
02168 {
02169   return 0;
02170 }
02171 
02172 int
02173 bdd_enable_reordering_reporting(bdd_manager *mgr)
02174 {
02175   return 0;
02176 }
02177 int
02178 bdd_disable_reordering_reporting(bdd_manager *mgr)
02179 {
02180   return 0;
02181 }
02182 
02183 bdd_reorder_verbosity_t
02184 bdd_reordering_reporting(bdd_manager *mgr)
02185 {
02186   return BDD_REORDER_VERBOSITY_DEFAULT;
02187 }
02188 
02189 int
02190 bdd_print_apa_minterm(
02191   FILE *fp,
02192   bdd_t *f,
02193   int nvars,
02194   int precision)
02195 {
02196   return 0;
02197 }
02198 
02199 int
02200 bdd_apa_compare_ratios(
02201   int nvars,
02202   bdd_t *f1,
02203   bdd_t *f2,
02204   int f1Num,
02205   int f2Num)
02206 {
02207   return 0;
02208 }
02209 
02210 int
02211 bdd_iter_decomp(
02212   bdd_t *f,
02213   bdd_partition_type_t partType,
02214   bdd_t  ***conjArray)
02215 {
02216   return 0;
02217 }
02218 
02219 bdd_t *
02220 bdd_solve_eqn(
02221   bdd_t *f,
02222   array_t *g,
02223   array_t *unknowns)
02224 {
02225   return NIL(bdd_t);
02226 }
02227 
02228 int
02229 bdd_reordering_status(
02230   bdd_manager *mgr,
02231   bdd_reorder_type_t *method)
02232 {
02233   return 0;
02234 }
02235 
02236 int
02237 bdd_read_node_count(bdd_manager *mgr)
02238 {
02239   return 0;
02240 }
02241 
02242 double
02243 bdd_correlation(bdd_t *f, bdd_t *g)
02244 {
02245     return 0.0;
02246 }
02247 
02248 
02249 bdd_t *
02250 bdd_pick_one_minterm(bdd_t *f, array_t *varsArray)
02251 {
02252     return NIL(bdd_t);
02253 }
02254 
02255 array_t *
02256 bdd_bdd_pick_arbitrary_minterms(
02257   bdd_t *f,
02258   array_t *varsArray,
02259   int n,
02260   int k)
02261 {
02262     return NIL(array_t);
02263 }
02264 
02265 
02266 int
02267 bdd_reordering_zdd_status(
02268   bdd_manager *mgr,
02269   bdd_reorder_type_t *method)
02270 {
02271   return 0;
02272 }
02273 
02274 
02275 bdd_node *
02276 bdd_bdd_to_add(
02277   bdd_manager *mgr,
02278   bdd_node *fn)
02279 {
02280   return NIL(bdd_node);
02281 }
02282 
02283 bdd_node *
02284 bdd_add_permute(
02285   bdd_manager *mgr,
02286   bdd_node *fn,
02287   int *permut)
02288 {
02289   return NIL(bdd_node);
02290 }
02291 
02292 bdd_node *
02293 bdd_bdd_permute(
02294   bdd_manager *mgr,
02295   bdd_node *fn,
02296   int *permut)
02297 {
02298   return NIL(bdd_node);
02299 }
02300 
02301 
02302 void
02303 bdd_ref(bdd_node *fn)
02304 {
02305   return ;
02306 }
02307 
02308 
02309 void
02310 bdd_recursive_deref(bdd_manager *mgr, bdd_node *f)
02311 {
02312   return;
02313 }
02314 
02315 
02316 bdd_node *
02317 bdd_add_exist_abstract(
02318   bdd_manager *mgr,
02319   bdd_node *fn,
02320   bdd_node *vars)
02321 {
02322   return NIL(bdd_node);
02323 }
02324 
02325 
02326 bdd_node *
02327 bdd_add_apply(
02328   bdd_manager *mgr,
02329   bdd_node *(*operation)(bdd_manager *, bdd_node **, bdd_node **),
02330   bdd_node *fn1,
02331   bdd_node *fn2)
02332 {
02333   return NIL(bdd_node);
02334 }
02335 
02336 
02337 bdd_node *
02338 bdd_add_nonsim_compose(
02339   bdd_manager *mgr,
02340   bdd_node *fn,
02341   bdd_node **vector)
02342 {
02343   return NIL(bdd_node);
02344 }
02345 
02346 
02347 bdd_node *
02348 bdd_add_residue(
02349   bdd_manager *mgr,
02350   int n,
02351   int m,
02352   int options,
02353   int top)
02354 {
02355   return NIL(bdd_node);
02356 }
02357 
02358 
02359 bdd_node *
02360 bdd_add_vector_compose(
02361   bdd_manager *mgr,
02362   bdd_node *fn,
02363   bdd_node **vector)
02364 {
02365   return NIL(bdd_node);
02366 }
02367 
02368 
02369 bdd_node *
02370 bdd_add_times(
02371   bdd_manager *mgr,
02372   bdd_node **fn1,
02373   bdd_node **fn2)
02374 {
02375   return NIL(bdd_node);
02376 }
02377 
02378 
02379 int
02380 bdd_check_zero_ref(bdd_manager *mgr)
02381 {
02382   return 0;
02383 }
02384 
02385 
02386 void
02387 bdd_dynamic_reordering_disable(bdd_manager *mgr)
02388 {
02389   return;
02390 }
02391 
02392 void
02393 bdd_dynamic_reordering_zdd_disable(bdd_manager *mgr)
02394 {
02395   return;
02396 }
02397 
02398 
02399 bdd_node *
02400 bdd_add_xnor(
02401   bdd_manager *mgr,
02402   bdd_node **fn1,
02403   bdd_node **fn2)
02404 {
02405   return NIL(bdd_node);
02406 }
02407 
02408 
02409 int
02410 bdd_shuffle_heap(
02411   bdd_manager *mgr,
02412   int *permut)
02413 {
02414   return 0;
02415 }
02416 
02417 
02418 bdd_node *
02419 bdd_add_compose(
02420   bdd_manager *mgr,
02421   bdd_node *fn1,
02422   bdd_node *fn2,
02423   int var)
02424 {
02425   return NIL(bdd_node);
02426 }
02427 
02428 
02429 bdd_node *
02430 bdd_add_ith_var(
02431   bdd_manager *mgr,
02432   int i)
02433 {
02434   return NIL(bdd_node);
02435 }
02436 
02437 
02438 int
02439 bdd_get_level_from_id(
02440   bdd_manager *mgr,
02441   int id)
02442 {
02443   return 0;
02444 }
02445 
02446 
02447 bdd_node *
02448 bdd_bdd_exist_abstract(
02449   bdd_manager *mgr,
02450   bdd_node *fn,
02451   bdd_node *cube)
02452 {
02453   return NIL(bdd_node);
02454 }
02455 
02456 
02457 int
02458 bdd_equal_sup_norm(
02459   bdd_manager *mgr,
02460   bdd_node *fn,
02461   bdd_node *gn,
02462   BDD_VALUE_TYPE tolerance,
02463   int pr)
02464 {
02465   return 0;
02466 }
02467 
02468 
02469 bdd_node *
02470 bdd_read_logic_zero(bdd_manager *mgr)
02471 {
02472     return NIL(bdd_node);
02473 }
02474 
02475 
02476 bdd_node *
02477 bdd_bdd_ith_var(
02478   bdd_manager *mgr,
02479   int i)
02480 {
02481     return NIL(bdd_node);
02482 }
02483 
02484 
02485 bdd_node *
02486 bdd_add_divide(
02487   bdd_manager *mgr,
02488   bdd_node **fn1,
02489   bdd_node **fn2)
02490 {
02491   return NIL(bdd_node);
02492 }
02493 
02494 
02495 bdd_node *
02496 bdd_bdd_constrain(
02497   bdd_manager *mgr,
02498   bdd_node *f,
02499   bdd_node *c)
02500 {
02501     return NIL(bdd_node);
02502 }
02503 
02504 bdd_node *
02505 bdd_bdd_restrict(
02506   bdd_manager *mgr,
02507   bdd_node *f,
02508   bdd_node *c)
02509 {
02510     return NIL(bdd_node);
02511 }
02512 
02513 
02514 bdd_node *
02515 bdd_add_hamming(
02516   bdd_manager *mgr,
02517   bdd_node **xVars,
02518   bdd_node **yVars,
02519   int nVars)
02520 {
02521     return NIL(bdd_node);
02522 }
02523 
02524 
02525 bdd_node *
02526 bdd_add_ite(
02527   bdd_manager *mgr,
02528   bdd_node *f,
02529   bdd_node *g,
02530   bdd_node *h)
02531 {
02532     return NIL(bdd_node);
02533 }
02534 
02535 
02536 bdd_node *
02537 bdd_add_find_max(
02538   bdd_manager *mgr,
02539   bdd_node *f)
02540 {
02541     return NIL(bdd_node);
02542 }
02543 
02544 
02545 int
02546 bdd_bdd_pick_one_cube(
02547   bdd_manager *mgr,
02548   bdd_node *node,
02549   char *string)
02550 {
02551     return 0;
02552 }
02553 
02554 
02555 bdd_node *
02556 bdd_add_swap_variables(
02557   bdd_manager *mgr,
02558   bdd_node *f,
02559   bdd_node **x,
02560   bdd_node **y,
02561   int n)
02562 {
02563     return NIL(bdd_node);
02564 }
02565 
02566 bdd_node *
02567 bdd_bdd_swap_variables(
02568   bdd_manager *mgr,
02569   bdd_node *f,
02570   bdd_node **x,
02571   bdd_node **y,
02572   int n)
02573 {
02574     return NIL(bdd_node);
02575 }
02576 
02577 
02578 bdd_node *
02579 bdd_bdd_or(
02580   bdd_manager *mgr,
02581   bdd_node *f,
02582   bdd_node *g)
02583 {
02584     return NIL(bdd_node);
02585 }
02586 
02587 bdd_t *
02588 bdd_compute_cube(
02589   bdd_manager *mgr,
02590   array_t *vars)
02591 {
02592   return NIL(bdd_t);
02593 }
02594 
02595 bdd_t *
02596 bdd_compute_cube_with_phase(
02597   bdd_manager *mgr,
02598   array_t *vars,
02599   array_t *phase)
02600 {
02601   return NIL(bdd_t);
02602 }
02603 
02604 
02605 bdd_node *
02606 bdd_bdd_compute_cube(
02607   bdd_manager *mgr,
02608   bdd_node **vars,
02609   int *phase,
02610   int n)
02611 {
02612     return NIL(bdd_node);
02613 }
02614 
02615 
02616 bdd_node *
02617 bdd_indices_to_cube(
02618   bdd_manager *mgr,
02619   int *idArray,
02620   int n)
02621 {
02622     return NIL(bdd_node);
02623 }
02624 
02625 
02626 bdd_node *
02627 bdd_bdd_and(
02628   bdd_manager *mgr,
02629   bdd_node *f,
02630   bdd_node *g)
02631 {
02632     return NIL(bdd_node);
02633 }
02634 
02635 
02636 bdd_node *
02637 bdd_add_matrix_multiply(
02638   bdd_manager *mgr,
02639   bdd_node *A,
02640   bdd_node *B,
02641   bdd_node **z,
02642   int nz)
02643 {
02644     return NIL(bdd_node);
02645 }
02646 
02647 
02648 bdd_node *
02649 bdd_add_compute_cube(
02650   bdd_manager *mgr,
02651   bdd_node **vars,
02652   int *phase,
02653   int n)
02654 {
02655     return NIL(bdd_node);
02656 }
02657 
02658 
02659 bdd_node *
02660 bdd_add_const(
02661   bdd_manager *mgr,
02662   BDD_VALUE_TYPE c)
02663 {
02664     return NIL(bdd_node);
02665 }
02666 
02667 
02668 double
02669 bdd_count_minterm(
02670   bdd_manager *mgr,
02671   bdd_node *f,
02672   int n)
02673 {
02674     return 0;
02675 }
02676 
02677 
02678 bdd_node *
02679 bdd_add_bdd_threshold(
02680   bdd_manager *mgr,
02681   bdd_node *f,
02682   BDD_VALUE_TYPE value)
02683 {
02684     return NIL(bdd_node);
02685 }
02686 
02687 
02688 bdd_node *
02689 bdd_add_bdd_strict_threshold(
02690   bdd_manager *mgr,
02691   bdd_node *f,
02692   BDD_VALUE_TYPE value)
02693 {
02694     return NIL(bdd_node);
02695 }
02696 
02697 BDD_VALUE_TYPE
02698 bdd_read_epsilon(bdd_manager *mgr)
02699 {
02700     return 0;
02701 }
02702 
02703 bdd_node *
02704 bdd_read_one(bdd_manager *mgr)
02705 {
02706     return NIL(bdd_node);
02707 }
02708 
02709 
02710 bdd_node *
02711 bdd_bdd_pick_one_minterm(
02712   bdd_manager *mgr,
02713   bdd_node *f,
02714   bdd_node **vars,
02715   int n)
02716 {
02717     return NIL(bdd_node);
02718 }
02719 
02720 
02721 bdd_node *
02722 bdd_read_zero(bdd_manager *mgr)
02723 {
02724     return NIL(bdd_node);
02725 }
02726 
02727 
02728 bdd_node *
02729 bdd_bdd_new_var(bdd_manager *mgr)
02730 {
02731     return NIL(bdd_node);
02732 }
02733 
02734 
02735 bdd_node *
02736 bdd_bdd_and_abstract(
02737   bdd_manager *mgr,
02738   bdd_node *f,
02739   bdd_node *g,
02740   bdd_node *cube)
02741 {
02742     return NIL(bdd_node);
02743 }
02744 
02745 void
02746 bdd_deref(bdd_node *f)
02747 {
02748     return;
02749 }
02750 
02751 bdd_node *
02752 bdd_add_plus(
02753   bdd_manager *mgr,
02754   bdd_node **fn1,
02755   bdd_node **fn2)
02756 {
02757   return NIL(bdd_node);
02758 }
02759 
02760 
02761 int
02762 bdd_read_reorderings(bdd_manager *mgr)
02763 {
02764     return 0;
02765 }
02766 
02767 int
02768 bdd_read_next_reordering(bdd_manager *mgr)
02769 {
02770     return 0;
02771 }
02772 
02773 void
02774 bdd_set_next_reordering(bdd_manager *mgr, int next)
02775 {
02776 }
02777 
02778 bdd_node *
02779 bdd_bdd_xnor(
02780   bdd_manager *mgr,
02781   bdd_node *f,
02782   bdd_node *g)
02783 {
02784     return NIL(bdd_node);
02785 }
02786 
02787 bdd_node *
02788 bdd_bdd_vector_compose(
02789   bdd_manager *mgr,
02790   bdd_node *f,
02791   bdd_node **vector)
02792 {
02793     return NIL(bdd_node);
02794 }
02795 
02796 bdd_node *
02797 bdd_extract_node_as_is(bdd_t *fn)
02798 {
02799   return NIL(bdd_node);
02800 }
02801 
02802 
02803 bdd_node *
02804 bdd_zdd_get_node(
02805   bdd_manager *mgr,
02806   int id,
02807   bdd_node *g,
02808   bdd_node *h)
02809 {
02810     return NIL(bdd_node);
02811 }
02812 
02813 bdd_node *
02814 bdd_zdd_product(
02815   bdd_manager *mgr,
02816   bdd_node *f,
02817   bdd_node *g)
02818 {
02819     return NIL(bdd_node);
02820 }
02821 
02822 bdd_node *
02823 bdd_zdd_product_recur(
02824   bdd_manager *mgr,
02825   bdd_node *f,
02826   bdd_node *g)
02827 {
02828     return NIL(bdd_node);
02829 }
02830 
02831 bdd_node *
02832 bdd_zdd_union(
02833   bdd_manager *mgr,
02834   bdd_node *f,
02835   bdd_node *g)
02836 {
02837     return(NIL(bdd_node));
02838 }
02839 
02840 
02841 bdd_node *
02842 bdd_zdd_weak_div(
02843   bdd_manager *mgr,
02844   bdd_node *f,
02845   bdd_node *g)
02846 {
02847     return NIL(bdd_node);
02848 }
02849 
02850 bdd_node *
02851 bdd_zdd_weak_div_recur(
02852   bdd_manager *mgr,
02853   bdd_node *f,
02854   bdd_node *g)
02855 {
02856     return NIL(bdd_node);
02857 }
02858 
02859 bdd_node *
02860 bdd_zdd_isop_recur(
02861   bdd_manager *mgr,
02862   bdd_node *L,
02863   bdd_node *U,
02864   bdd_node **zdd_I)
02865 {
02866     return NIL(bdd_node);
02867 }
02868 
02869 bdd_node *
02870 bdd_zdd_isop(
02871   bdd_manager *mgr,
02872   bdd_node *L,
02873   bdd_node *U,
02874   bdd_node **zdd_I)
02875 {
02876     return NIL(bdd_node);
02877 }
02878 
02879 int
02880 bdd_zdd_get_cofactors3(
02881   bdd_manager *mgr,
02882   bdd_node *f,
02883   int v,
02884   bdd_node **f1,
02885   bdd_node **f0,
02886   bdd_node **fd)
02887 {
02888     return 0;
02889 }
02890 
02891 bdd_node *
02892 bdd_bdd_and_recur(
02893   bdd_manager *mgr,
02894   bdd_node *f,
02895   bdd_node *g)
02896 {
02897      return NIL(bdd_node);
02898 }
02899 
02900 bdd_node *
02901 bdd_unique_inter(
02902   bdd_manager *mgr,
02903   int v,
02904   bdd_node *f,
02905   bdd_node *g)
02906 {
02907      return NIL(bdd_node);
02908 }
02909 
02910 bdd_node *
02911 bdd_unique_inter_ivo(
02912   bdd_manager *mgr,
02913   int v,
02914   bdd_node *f,
02915   bdd_node *g)
02916 {
02917      return NIL(bdd_node);
02918 }
02919 
02920 
02921 bdd_node *
02922 bdd_zdd_diff(
02923   bdd_manager *mgr,
02924   bdd_node *f,
02925   bdd_node *g)
02926 {
02927     return NIL(bdd_node);
02928 }
02929 
02930 bdd_node *
02931 bdd_zdd_diff_recur(
02932   bdd_manager *mgr,
02933   bdd_node *f,
02934   bdd_node *g)
02935 {
02936     return NIL(bdd_node);
02937 }
02938 
02939 int
02940 bdd_num_zdd_vars(bdd_manager *mgr)
02941 {
02942     return -1;
02943 }
02944 
02945 bdd_node *
02946 bdd_regular(bdd_node *f)
02947 {
02948     return NIL(bdd_node);
02949 }
02950 
02951 int
02952 bdd_is_constant(bdd_node *f)
02953 {
02954     return 0;
02955 }
02956 
02957 int
02958 bdd_is_complement(bdd_node *f)
02959 {
02960     return 0;
02961 }
02962 
02963 bdd_node *
02964 bdd_bdd_T(bdd_node *f)
02965 {
02966     return NIL(bdd_node);
02967 }
02968 
02969 bdd_node *
02970 bdd_bdd_E(bdd_node *f)
02971 {
02972     return NIL(bdd_node);
02973 }
02974 
02975 bdd_node *
02976 bdd_not_bdd_node(bdd_node *f)
02977 {
02978     return NIL(bdd_node);
02979 }
02980 
02981 void
02982 bdd_recursive_deref_zdd(
02983   bdd_manager *mgr,
02984   bdd_node *f)
02985 {
02986     return;
02987 }
02988 
02989 int
02990 bdd_zdd_count(
02991   bdd_manager *mgr,
02992   bdd_node *f)
02993 {
02994     return 0;
02995 }
02996 
02997 int
02998 bdd_read_zdd_level(
02999   bdd_manager *mgr,
03000   int index)
03001 {
03002     return -1;
03003 }
03004 
03005 int
03006 bdd_zdd_vars_from_bdd_vars(
03007   bdd_manager *mgr,
03008   int multiplicity)
03009 {
03010    return 0;
03011 }
03012 
03013 void
03014 bdd_zdd_realign_enable(bdd_manager *mgr)
03015 {
03016     return;
03017 }
03018 
03019 void
03020 bdd_zdd_realign_disable(bdd_manager *mgr)
03021 {
03022     return;
03023 }
03024 
03025 int
03026 bdd_zdd_realignment_enabled(bdd_manager *mgr)
03027 {
03028     return 0;
03029 }
03030 
03031 void
03032 bdd_realign_enable(bdd_manager *mgr)
03033 {
03034     return;
03035 }
03036 
03037 void
03038 bdd_realign_disable(bdd_manager *mgr)
03039 {
03040     return;
03041 }
03042 
03043 int
03044 bdd_realignment_enabled(bdd_manager *mgr)
03045 {
03046     return 0;
03047 }
03048 
03049 int
03050 bdd_node_read_index(bdd_node *f)
03051 {
03052     return -1;
03053 }
03054 
03055 bdd_node *
03056 bdd_read_next(bdd_node *f)
03057 {
03058     return NIL(bdd_node);
03059 }
03060 
03061 void
03062 bdd_set_next(bdd_node *f, bdd_node *g)
03063 {
03064     return;
03065 }
03066 
03067 int
03068 bdd_read_reordered_field(bdd_manager *mgr)
03069 {
03070     return -1;
03071 }
03072 
03073 void
03074 bdd_set_reordered_field(bdd_manager *mgr, int n)
03075 {
03076     return;
03077 }
03078 
03079 bdd_node *
03080 bdd_add_apply_recur(
03081   bdd_manager *mgr,
03082   bdd_node *(*operation)(bdd_manager *, bdd_node **, bdd_node **),
03083   bdd_node *fn1,
03084   bdd_node *fn2)
03085 {
03086     return NIL(bdd_node);
03087 }
03088 
03089 
03090 BDD_VALUE_TYPE
03091 bdd_add_value(bdd_node *f)
03092 {
03093     return 0.0;
03094 }
03095 
03096 int
03097 bdd_print_minterm(bdd_t *f)
03098 {
03099   return 0;
03100 }
03101 
03102 
03103 int
03104 bdd_print_cover(bdd_t *f)
03105 {
03106   return 0;
03107 }
03108 
03109 
03110 bdd_t *
03111 bdd_xor_smooth(
03112   bdd_t *f,
03113   bdd_t *g,
03114   array_t *smoothing_vars)
03115 {
03116     return NIL(bdd_t);
03117 }
03118 
03119 
03120 bdd_node *
03121 bdd_read_plus_infinity(bdd_manager *mgr)
03122 {
03123     return NIL(bdd_node);
03124 
03125 } /* end of bdd_read_plus_infinity */
03126 
03127 
03128 
03129 bdd_node *
03130 bdd_priority_select(
03131   bdd_manager *mgr,
03132   bdd_node *R,
03133   bdd_node  **x,
03134   bdd_node **y,
03135   bdd_node **z,
03136   bdd_node *Pi,
03137   int n,
03138   bdd_node  *(*Pifunc)(bdd_manager *, int, bdd_node **, bdd_node **, bdd_node **))
03139 {
03140     return NIL(bdd_node);
03141 
03142 } /* end of bdd_priority_select */
03143 
03144 
03145 void
03146 bdd_set_background(
03147   bdd_manager *mgr,
03148   bdd_node *f)
03149 {
03150     return;
03151 
03152 } /* end of bdd_set_background */
03153 
03154 
03155 bdd_node *
03156 bdd_read_background(bdd_manager *mgr)
03157 {
03158   return NIL(bdd_node);
03159 
03160 } /* end of bdd_read_background */
03161 
03162 
03163 bdd_node *
03164 bdd_bdd_cofactor(
03165   bdd_manager *mgr,
03166   bdd_node *f,
03167   bdd_node *g)
03168 {
03169     return NIL(bdd_node);
03170 
03171 } /* end of bdd_bdd_cofactor */
03172 
03173 
03174 bdd_node *
03175 bdd_bdd_ite(
03176   bdd_manager *mgr,
03177   bdd_node *f,
03178   bdd_node *g,
03179   bdd_node *h)
03180 {
03181     return NIL(bdd_node);
03182 
03183 } /* end of bdd_bdd_ite */
03184 
03185 
03186 bdd_node *
03187 bdd_add_minus(
03188   bdd_manager *mgr,
03189   bdd_node **fn1,
03190   bdd_node **fn2)
03191 {
03192     return NIL(bdd_node);
03193 
03194 } /* end of bdd_add_plus */
03195 
03196 
03197 bdd_node *
03198 bdd_dxygtdxz(
03199   bdd_manager *mgr,
03200   int N,
03201   bdd_node **x,
03202   bdd_node **y,
03203   bdd_node **z)
03204 {
03205     return NIL(bdd_node);
03206 
03207 } /* end of bdd_dxygtdxz */
03208 
03209 
03210 bdd_node *
03211 bdd_bdd_univ_abstract(
03212   bdd_manager *mgr,
03213   bdd_node *fn,
03214   bdd_node *vars)
03215 {
03216     return NIL(bdd_node);
03217 
03218 } /* end of bdd_bdd_univ_abstract */
03219 
03220 
03221 bdd_node *
03222 bdd_bdd_cprojection(
03223   bdd_manager *mgr,
03224   bdd_node *R,
03225   bdd_node *Y)
03226 {
03227     return NIL(bdd_node);
03228 
03229 } /* end of bdd_bdd_cprojection */
03230 
03231 bdd_node *
03232 bdd_xeqy(
03233   bdd_manager *mgr,
03234   int N,
03235   bdd_node **x,
03236   bdd_node **y)
03237 {
03238   return NIL(bdd_node);
03239 
03240 } /* end of bdd_xeqy */
03241 
03242 bdd_node *
03243 bdd_add_roundoff(
03244   bdd_manager *mgr,
03245   bdd_node *f,
03246   int N)
03247 {
03248   return NIL(bdd_node);
03249 
03250 } /* end of bdd_add_roundoff */
03251 
03252 bdd_node *
03253 bdd_xgty(
03254   bdd_manager *mgr,
03255   int N,
03256   bdd_node **x,
03257   bdd_node **y)
03258 {
03259   return NIL(bdd_node);
03260 
03261 } /* end of bdd_xgty */
03262 
03263 bdd_node *
03264 bdd_add_cmpl(
03265   bdd_manager *mgr,
03266   bdd_node *f)
03267 {
03268   return NIL(bdd_node);
03269 
03270 } /* end of bdd_add_cmpl */
03271 
03272 bdd_node *
03273 bdd_split_set(
03274   bdd_manager *mgr,
03275   bdd_node *f,
03276   bdd_node **x,
03277   int n,
03278   double m)
03279 {
03280   return NIL(bdd_node);
03281 
03282 } /* end of bdd_split_set */
03283 
03284 
03285 int
03286 bdd_debug_check(bdd_manager *mgr)
03287 {
03288     return -1;
03289 
03290 } /* end of bdd_debug_check */
03291 
03292 bdd_node *
03293 bdd_bdd_xor(
03294   bdd_manager *mgr,
03295   bdd_node *f,
03296   bdd_node *g)
03297 {
03298     return NIL(bdd_node);
03299 }
03300 
03301 void
03302 bdd_dump_blif(
03303   bdd_manager *mgr,
03304   int nBdds,
03305   bdd_node **bdds,
03306   char **inames,
03307   char **onames,
03308   char *model,
03309   FILE *fp)
03310 {
03311   return;
03312 }
03313 
03314 void
03315 bdd_dump_blif_body(
03316   bdd_manager *mgr,
03317   int nBdds,
03318   bdd_node **bdds,
03319   char **inames,
03320   char **onames,
03321   FILE *fp)
03322 {
03323   return;
03324 }
03325 
03326 void
03327 bdd_dump_dot(
03328   bdd_manager *mgr,
03329   int nBdds,
03330   bdd_node **bdds,
03331   char **inames,
03332   char **onames,
03333   FILE *fp)
03334 {
03335   return;
03336 }
03337 
03338 bdd_node *
03339 bdd_make_bdd_from_zdd_cover(bdd_manager *mgr, bdd_node *node)
03340 {
03341     return(NIL(bdd_node));
03342 }
03343 
03344 bdd_node *
03345 bdd_zdd_complement(bdd_manager *mgr, bdd_node *node)
03346 {
03347     return(NIL(bdd_node));
03348 }
03349 
03350 bdd_node *
03351 bdd_bdd_vector_support(
03352   bdd_manager *mgr,
03353   bdd_node **F,
03354   int n)
03355 {
03356   return NIL(bdd_node);
03357 }
03358 
03359 int
03360 bdd_bdd_vector_support_size(
03361   bdd_manager *mgr,
03362   bdd_node **F,
03363   int n)
03364 {
03365   return -1;
03366 }
03367 
03368 
03369 int
03370 bdd_bdd_support_size(
03371   bdd_manager *mgr,
03372   bdd_node *F)
03373 {
03374   return -1;
03375 }
03376 
03377 bdd_node *
03378 bdd_bdd_support(
03379   bdd_manager *mgr,
03380   bdd_node *F)
03381 {
03382   return NIL(bdd_node);
03383 }
03384 
03385 bdd_node *
03386 bdd_add_general_vector_compose(
03387   bdd_manager *mgr,
03388   bdd_node *f,
03389   bdd_node **vectorOn,
03390   bdd_node **vectorOff)
03391 {
03392   return NIL(bdd_node);
03393 }
03394 
03395 int
03396 bdd_bdd_leq(
03397   bdd_manager *mgr,
03398   bdd_node *f,
03399   bdd_node *g)
03400 {
03401   return -1;
03402 }
03403 
03404 bdd_node *
03405 bdd_bdd_boolean_diff(
03406   bdd_manager *mgr,
03407   bdd_node *f,
03408   int x)
03409 {
03410   return NIL(bdd_node);
03411 }
03412 
03420 int
03421 bdd_ptrcmp(bdd_t *f, bdd_t *g)
03422 {
03423   if (f->calBdd == g->calBdd)
03424     return(0);
03425   else
03426     return(1);
03427 }
03428 
03429 
03437 int
03438 bdd_ptrhash(bdd_t *f, int size)
03439 {
03440   int hash;
03441 
03442   hash = (int)((unsigned long)f->calBdd >> 2) % size;
03443   return(hash);
03444 }
03445 
03446 bdd_t *
03447 bdd_subset_with_mask_vars(
03448   bdd_t *f,
03449   array_t *varsArray,
03450   array_t *maskVarsArray)
03451 {
03452   return NIL(bdd_t);
03453 }
03454 
03455 bdd_t *
03456 bdd_and_smooth_with_cube(
03457   bdd_t *f,
03458   bdd_t *g,
03459   bdd_t *cube)
03460 {
03461   return NIL(bdd_t);
03462 }
03463 
03464 bdd_t *
03465 bdd_smooth_with_cube(bdd_t *f, bdd_t *cube)
03466 {
03467   int i;
03468   bdd_t *var, *res;
03469   array_t *smoothingVars;
03470   var_set_t *supportVarSet;
03471 
03472   smoothingVars = array_alloc(bdd_t *, 0);
03473   supportVarSet = bdd_get_support(f);
03474   for (i = 0; i < supportVarSet->n_elts; i++) {
03475     if (var_set_get_elt(supportVarSet, i) == 1) {
03476       var = bdd_var_with_index(f->bddManager, i);
03477       array_insert_last(bdd_t *, smoothingVars, var);
03478     }
03479   }
03480   var_set_free(supportVarSet);
03481 
03482   res = bdd_smooth(f, smoothingVars);
03483 
03484   for (i = 0; i < array_n(smoothingVars); i++) {
03485     var = array_fetch(bdd_t *, smoothingVars, i);
03486     bdd_free(var);
03487   }
03488   array_free(smoothingVars);
03489   return res;
03490 }
03491 
03492 bdd_t *
03493 bdd_substitute_with_permut(bdd_t *f, int *permut)
03494 {
03495   return NIL(bdd_t);
03496 }
03497 
03498 array_t *
03499 bdd_substitute_array_with_permut(array_t *f_array, int *permut)
03500 {
03501   return NIL(array_t);
03502 }
03503 
03504 bdd_t *
03505 bdd_vector_compose(
03506   bdd_t *f,
03507   array_t *varArray,
03508   array_t *funcArray)
03509 {
03510   return NIL(bdd_t);
03511 }
03512 
03513 double *
03514 bdd_cof_minterm(bdd_t *f)
03515 {
03516   return(NIL(double));
03517 }
03518 
03519 int
03520 bdd_var_is_dependent(
03521   bdd_t *f,
03522   bdd_t *var)
03523 {
03524   return(0);
03525 }
03526 
03527 array_t *
03528 bdd_find_essential(bdd_t *f)
03529 {
03530   return(NIL(array_t));
03531 }
03532 
03533 bdd_t *
03534 bdd_find_essential_cube(bdd_t *f)
03535 {
03536   return(NIL(bdd_t));
03537 }
03538 
03539 int
03540 bdd_estimate_cofactor(
03541   bdd_t *f,
03542   bdd_t *var,
03543   int phase)
03544 {
03545   return(0);
03546 }
03547 
03548 long
03549 bdd_read_peak_memory(bdd_manager *mgr)
03550 {
03551   return(0);
03552 }
03553 
03554 int
03555 bdd_read_peak_live_node(bdd_manager *mgr)
03556 {
03557   return(0);
03558 }
03559 
03560 int
03561 bdd_set_pi_var(
03562   bdd_manager *mgr,
03563   int index)
03564 {
03565     return(0);
03566 }
03567 
03568 int
03569 bdd_set_ps_var(
03570   bdd_manager *mgr,
03571   int index)
03572 {
03573     return(0);
03574 }
03575 
03576 int
03577 bdd_set_ns_var(
03578   bdd_manager *mgr,
03579   int index)
03580 {
03581     return(0);
03582 }
03583 
03584 int
03585 bdd_is_pi_var(
03586   bdd_manager *mgr,
03587   int index)
03588 {
03589     return(0);
03590 }
03591 
03592 int
03593 bdd_is_ps_var(
03594   bdd_manager *mgr,
03595   int index)
03596 {
03597     return(0);
03598 }
03599 
03600 int
03601 bdd_is_ns_var(
03602   bdd_manager *mgr,
03603   int index)
03604 {
03605     return(0);
03606 }
03607 
03608 int
03609 bdd_set_pair_index(
03610   bdd_manager *mgr,
03611   int index,
03612   int pairIndex)
03613 {
03614     return(0);
03615 }
03616 
03617 int
03618 bdd_read_pair_index(
03619   bdd_manager *mgr,
03620   int index)
03621 {
03622     return(0);
03623 }
03624 
03625 int
03626 bdd_set_var_to_be_grouped(
03627   bdd_manager *mgr,
03628   int index)
03629 {
03630     return(0);
03631 }
03632 
03633 int
03634 bdd_set_var_hard_group(
03635   bdd_manager *mgr,
03636   int index)
03637 {
03638     return(0);
03639 }
03640 
03641 int
03642 bdd_reset_var_to_be_grouped(
03643   bdd_manager *mgr,
03644   int index)
03645 {
03646     return(0);
03647 }
03648 
03649 int
03650 bdd_is_var_to_be_grouped(
03651   bdd_manager *mgr,
03652   int index)
03653 {
03654     return(0);
03655 }
03656 
03657 int
03658 bdd_is_var_hard_group(
03659   bdd_manager *mgr,
03660   int index)
03661 {
03662     return(0);
03663 }
03664 
03665 int
03666 bdd_is_var_to_be_ungrouped(
03667   bdd_manager *mgr,
03668   int index)
03669 {
03670     return(0);
03671 }
03672 
03673 int
03674 bdd_set_var_to_be_ungrouped(
03675   bdd_manager *mgr,
03676   int index)
03677 {
03678     return(0);
03679 }
03680 
03681 int
03682 bdd_bind_var(
03683   bdd_manager *mgr,
03684   int index)
03685 {
03686     return(0);
03687 }
03688 
03689 int
03690 bdd_unbind_var(
03691   bdd_manager *mgr,
03692   int index)
03693 {
03694     return(0);
03695 }
03696 
03697 int
03698 bdd_is_lazy_sift(bdd_manager *mgr)
03699 {
03700     return(0);
03701 }
03702 
03703 void
03704 bdd_discard_all_var_groups(bdd_manager *mgr)
03705 {
03706     return;
03707 }
03708 
03709 /*---------------------------------------------------------------------------*/
03710 /* Definition of internal functions                                          */
03711 /*---------------------------------------------------------------------------*/
03712 
03713 
03714 /*---------------------------------------------------------------------------*/
03715 /* Definition of static functions                                            */
03716 /*---------------------------------------------------------------------------*/
03717 
03727 static void
03728 InvalidType(
03729   FILE *file,
03730   char *field,
03731   char *expected)
03732 {
03733     (void) fprintf(file, "Warning: In parameter \"%s\"\n", field);
03734     (void) fprintf(file, "Illegal type detected. %s expected\n", expected);
03735 
03736 } /* end of InvalidType */