distr/sis/cuddBddPort.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddBddPort.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [SIS interface to the Decision Diagram Package of the
   8   University of Colorado.]
   9
  10   Description [This file implements an interface between the functions in
  11     the Berkeley BDD package and the functions provided by the CUDD (decision
  12     diagram) package from the University of Colorado. The CUDD package is a
  13     generic implementation of a decision diagram data structure. For the time
  14     being, only Boole expansion is implemented and the leaves in the
  15     in the nodes can be the constants zero, one or any arbitrary value.]
  16
  17   Author      [Abelardo Pardo]
  18
  19   Copyright   [Copyright (c) 1994-1996 The Univ. of Colorado.
  20   All rights reserved.
  21
  22   Permission is hereby granted, without written agreement and without license
  23   or royalty fees, to use, copy, modify, and distribute this software and its
  24   documentation for any purpose, provided that the above copyright notice and
  25   the following two paragraphs appear in all copies of this software.
  26
  27   IN NO EVENT SHALL THE UNIVERSITY OF COLORADO BE LIABLE TO ANY PARTY FOR
  28   DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
  29   OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
  30   COLORADO HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  31
  32   THE UNIVERSITY OF COLORADO SPECIFICALLY DISCLAIMS ANY WARRANTIES,
  33   INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
  34   FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
  35   "AS IS" BASIS, AND THE UNIVERSITY OF COLORADO HAS NO OBLIGATION TO PROVIDE
  36   MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
  37
  38 ******************************************************************************/
  39
  40 #include "util.h"
  41 #include "array.h"
  42 #include "st.h"
  43
  44 #ifdef EXTERN
  45 #undef EXTERN
  46 #endif
  47 #define EXTERN
  48 #include "cuddInt.h"
  49 #include "cuddBdd.h"
  50
  51
  52 /*---------------------------------------------------------------------------*/
  53 /* Constant declarations                                                     */
  54 /*---------------------------------------------------------------------------*/
  55
  56 /*---------------------------------------------------------------------------*/
  57 /* Stucture declarations                                                     */
  58 /*---------------------------------------------------------------------------*/
  59
  60 struct bdd_gen {
  61     bdd_manager *manager;
  62     DdGen       *ddGen;
  63     array_t     *cube;
  64 };
  65
  66 /*---------------------------------------------------------------------------*/
  67 /* Type declarations                                                         */
  68 /*---------------------------------------------------------------------------*/
  69
  70 /*---------------------------------------------------------------------------*/
  71 /* Variable declarations                                                     */
  72 /*---------------------------------------------------------------------------*/
  73
  74 #ifndef lint
  75 static char rcsid[] DD_UNUSED = "$Id: cuddBddPort.c,v 1.11 1996/05/08 06:13:08 fabio Exp $";
  76 #endif
  77
  78 /*---------------------------------------------------------------------------*/
  79 /* Macro declarations                                                        */
  80 /*---------------------------------------------------------------------------*/
  81
  82
  83 /**AutomaticStart*************************************************************/
  84
  85 /*---------------------------------------------------------------------------*/
  86 /* Static function prototypes                                                */
  87 /*---------------------------------------------------------------------------*/
  88
  89 static bdd_t * bdd_construct_bdd_t (DdManager *mgr, DdNode * fn);
  90
  91 /**AutomaticEnd***************************************************************/
  92
  93
  94 /*---------------------------------------------------------------------------*/
  95 /* Definition of exported functions                                          */
  96 /*---------------------------------------------------------------------------*/
  97
  98
  99 /**Function********************************************************************
 100
 101   Synopsis    [Terminates the bdd package.]
 102
 103   SideEffects []
 104
 105 ******************************************************************************/
 106 void
 107 bdd_end(mgr)
 108 bdd_manager *mgr;
 109 {
 110     if (mgr->hooks != NULL) FREE(mgr->hooks);
 111     Cudd_Quit(mgr);
 112
 113 } /* end of bdd_end */
 114
 115
 116 /**Function********************************************************************
 117
 118   Synopsis    [Initialize manager with the options given in mgr_init.]
 119
 120   SideEffects []
 121
 122 ******************************************************************************/
 123 void
 124 bdd_set_mgr_init_dflts(mgr_init)
 125 bdd_mgr_init *mgr_init;
 126 {
 127     fprintf(stderr,"CU DD Package: bdd_set_mgr_init_dflts translated to no-op\n");
 128     return;
 129
 130 } /* end of bdd_set_mgr_init_dflts */
 131
 132
 133 /**Function********************************************************************
 134
 135   Synopsis    [Starts the manager with nvariables variables.]
 136
 137   SideEffects []
 138
 139 ******************************************************************************/
 140 bdd_manager *
 141 bdd_start(nvariables)
 142 int nvariables;
 143 {
 144     DdManager *mgr;
 145     bdd_external_hooks *hooks;
 146
 147     mgr =  Cudd_Init((unsigned int)nvariables,0,CUDD_UNIQUE_SLOTS,
 148                      CUDD_CACHE_SLOTS,0);
 149
 150     hooks = ALLOC(bdd_external_hooks,1);
 151     hooks->mdd = hooks->network = hooks->undef1 = (char *) 0;
 152     mgr->hooks = (char *) hooks;
 153
 154     return (bdd_manager *)mgr;
 155
 156 } /* end of bdd_start */
 157
 158
 159 /**Function********************************************************************
 160
 161   Synopsis    [Starts the manager with parameters.]
 162
 163   SideEffects []
 164
 165 ******************************************************************************/
 166 bdd_manager *
 167 bdd_start_with_params(nvariables, mgr_init)
 168 int nvariables;
 169 bdd_mgr_init *mgr_init;
 170 {
 171     fprintf(stderr,"CU DD Package: bdd_start_with_parameters bypassed\n");
 172     return (bdd_manager *)Cudd_Init((unsigned int)nvariables,0,
 173         CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0);
 174
 175 } /* end of bdd_start_with_params */
 176
 177
 178 /**Function********************************************************************
 179
 180   Synopsis    [Creates a new variable in the manager.]
 181
 182   SideEffects []
 183
 184 ******************************************************************************/
 185 bdd_t *
 186 bdd_create_variable(mgr)
 187 bdd_manager *mgr;
 188 {
 189     DdNode *var;
 190     DdManager *dd = (DdManager *) mgr;
 191     DdNode *one = DD_ONE(dd);
 192
 193     if (dd->size >= CUDD_MAXINDEX -1) return(NULL);
 194     do {
 195         dd->reordered = 0;
 196         var = cuddUniqueInter(dd,dd->size,one,Cudd_Not(one));
 197     } while (dd->reordered == 1);
 198
 199     if (var == NULL) return(NULL);
 200     cuddRef(var);
 201     return(bdd_construct_bdd_t(dd,var));
 202
 203 } /* end of bdd_create_variable */
 204
 205
 206 /**Function********************************************************************
 207
 208   Synopsis    [Creates a new variable and positions it after the
 209   variable with the specified index.]
 210
 211   SideEffects []
 212
 213 ******************************************************************************/
 214 bdd_t *
 215 bdd_create_variable_after(mgr, after_id)
 216 bdd_manager *mgr;
 217 bdd_variableId after_id;
 218 {
 219     DdNode *var;
 220     DdManager *dd = (DdManager *) mgr;
 221     int level;
 222
 223     if (after_id >= dd->size) return(NULL);
 224     level = 1 + dd->perm[after_id];
 225     var = Cudd_bddNewVarAtLevel(dd,level);
 226     if (var == NULL) return(NULL);
 227     cuddRef(var);
 228     return(bdd_construct_bdd_t(dd,var));
 229
 230 } /* end of bdd_create_variable_after */
 231
 232
 233 /**Function********************************************************************
 234
 235   Synopsis    [Returns the BDD representing the variable with given ID.]
 236
 237   SideEffects []
 238
 239 ******************************************************************************/
 240 bdd_t *
 241 bdd_get_variable(mgr, variable_ID)
 242 bdd_manager *mgr;
 243 bdd_variableId variable_ID;            /* unsigned int */
 244 {
 245     DdNode *var;
 246     DdManager *dd = (DdManager *) mgr;
 247     DdNode *one = DD_ONE(dd);
 248
 249     if (variable_ID >= CUDD_MAXINDEX -1) return(NULL);
 250     do {
 251         dd->reordered = 0;
 252         var = cuddUniqueInter(dd,(int)variable_ID,one,Cudd_Not(one));
 253     } while (dd->reordered == 1);
 254
 255     if (var == NULL) return(NULL);
 256     cuddRef(var);
 257     return(bdd_construct_bdd_t(dd,var));
 258
 259 } /* end of bdd_get_variable */
 260
 261
 262 /**Function********************************************************************
 263
 264   Synopsis    [Creates a copy of the BDD.]
 265
 266   SideEffects []
 267
 268 ******************************************************************************/
 269 bdd_t *
 270 bdd_dup(f)
 271 bdd_t *f;
 272 {
 273     cuddRef(f->node);
 274     return(bdd_construct_bdd_t((DdManager *)f->mgr,f->node));
 275
 276 } /* end of bdd_dup */
 277
 278
 279 /**Function********************************************************************
 280
 281   Synopsis    [Deletes the BDD of f.]
 282
 283   SideEffects []
 284
 285 ******************************************************************************/
 286 void
 287 bdd_free(f)
 288 bdd_t *f;
 289 {
 290     if (f == NULL) {
 291         fail("bdd_free: trying to free a NULL bdd_t");
 292     }
 293
 294     if (f->free == TRUE) {
 295         fail("bdd_free: trying to free a freed bdd_t");
 296     }
 297
 298     Cudd_RecursiveDeref((DdManager *)f->mgr,f->node);
 299     /* This is a bit overconservative. */
 300     f->node = 0;
 301     f->mgr = 0;
 302     f->free = 0;
 303     FREE(f);
 304     return;
 305
 306 } /* end of bdd_free */
 307
 308
 309 /**Function********************************************************************
 310
 311   Synopsis    [And of two BDDs.]
 312
 313   SideEffects []
 314
 315 ******************************************************************************/
 316 bdd_t *
 317 bdd_and(f, g, f_phase, g_phase)
 318 bdd_t *f;
 319 bdd_t *g;
 320 boolean f_phase;
 321 boolean g_phase;
 322 {
 323     DdManager *dd;
 324     DdNode *newf,*newg,*fandg;
 325     bdd_t *result;
 326
 327     /* Make sure both BDDs belong to the same manager. */
 328     assert(f->mgr == g->mgr);
 329
 330     /* Modify the phases of the operands according to the parameters. */
 331     if (!f_phase) {
 332         newf = Cudd_Not(f->node);
 333     } else {
 334         newf = f->node;
 335     }
 336     if (!g_phase) {
 337         newg = Cudd_Not(g->node);
 338     } else {
 339         newg = g->node;
 340     }
 341
 342     /* Perform the AND operation */
 343     dd = (DdManager *)f->mgr;
 344     fandg = Cudd_bddAnd((DdManager *)f->mgr,newf,newg);
 345     if (fandg == NULL) return(NULL);
 346     cuddRef(fandg);
 347     result = bdd_construct_bdd_t(dd,fandg);
 348
 349     return(result);
 350
 351 } /* end of bdd_and */
 352
 353
 354 /**Function********************************************************************
 355
 356   Synopsis    [Abstracts variables from the product of two BDDs.]
 357
 358   SideEffects []
 359
 360 ******************************************************************************/
 361 bdd_t *
 362 bdd_and_smooth(f, g, smoothing_vars)
 363 bdd_t *f;
 364 bdd_t *g;
 365 array_t *smoothing_vars;        /* of bdd_t *'s */
 366 {
 367     int i;
 368     bdd_t *variable;
 369     DdNode *cube,*tmpDd,*result;
 370     DdManager *mgr;
 371
 372     /* Make sure both operands belong to the same manager. */
 373     assert(f->mgr == g->mgr);
 374
 375     /* The Boulder package needs the smothing variables passed as a cube.
 376     ** Therefore we must build that cube from the indices of variables
 377     ** in the array before calling the procedure.
 378     */
 379     mgr = (DdManager *)f->mgr;
 380     Cudd_Ref(cube = DD_ONE(mgr));
 381     for (i = 0; i < array_n(smoothing_vars); i++) {
 382         variable = array_fetch(bdd_t *,smoothing_vars,i);
 383
 384         /* Make sure the variable belongs to the same manager. */
 385         assert(mgr == variable->mgr);
 386
 387         tmpDd = Cudd_bddAnd(mgr,cube,variable->node);
 388         if (tmpDd == NULL) {
 389             Cudd_RecursiveDeref(mgr,cube);
 390             return(NULL);
 391         }
 392         cuddRef(tmpDd);
 393         Cudd_RecursiveDeref(mgr, cube);
 394         cube = tmpDd;
 395     }
 396
 397     /* Perform the smoothing */
 398     result = Cudd_bddAndAbstract(mgr,f->node,g->node,cube);
 399     if (result == NULL) {
 400         Cudd_RecursiveDeref(mgr, cube);
 401         return(NULL);
 402     }
 403     cuddRef(result);
 404     /* Get rid of temporary results. */
 405     Cudd_RecursiveDeref(mgr, cube);
 406
 407     /* Build the bdd_t structure for the result */
 408     return(bdd_construct_bdd_t(mgr,result));
 409
 410 } /* end of bdd_and_smooth */
 411
 412
 413 /**Function********************************************************************
 414
 415   Synopsis    [Return a minimum size BDD between bounds.]
 416
 417   SideEffects []
 418
 419 ******************************************************************************/
 420 bdd_t *
 421 bdd_between(f_min, f_max)
 422 bdd_t *f_min;
 423 bdd_t *f_max;
 424 {
 425     bdd_t *temp, *ret;
 426
 427     temp = bdd_or(f_min, f_max, 1, 0);
 428     ret = bdd_minimize(f_min, temp);
 429     bdd_free(temp);
 430     return(ret);
 431
 432 } /* end of bdd_between */
 433
 434
 435 /**Function********************************************************************
 436
 437   Synopsis    [Computes the cofactor of f with respect to g.]
 438
 439   SideEffects []
 440
 441 ******************************************************************************/
 442 bdd_t *
 443 bdd_cofactor(f, g)
 444 bdd_t *f;
 445 bdd_t *g;
 446 {
 447     DdNode *result;
 448
 449     /* Make sure both operands belong to the same manager */
 450     assert(f->mgr == g->mgr);
 451
 452     /* We use Cudd_bddConstrain instead of Cudd_Cofactor for generality. */
 453     result = Cudd_bddConstrain((DdManager *)f->mgr,f->node,g->node);
 454     if (result == NULL) return(NULL);
 455     cuddRef(result);
 456     return(bdd_construct_bdd_t((DdManager *)f->mgr,result));
 457
 458 } /* end of bdd_cofactor */
 459
 460
 461 /**Function********************************************************************
 462
 463   Synopsis    [Functional composition of a function by a variable.]
 464
 465   SideEffects []
 466
 467 ******************************************************************************/
 468 bdd_t *
 469 bdd_compose(f, v, g)
 470 bdd_t *f;
 471 bdd_t *v;
 472 bdd_t *g;
 473 {
 474     DdNode *result;
 475
 476     /* Make sure all operands belong to the same manager. */
 477     assert(f->mgr == g->mgr);
 478     assert(f->mgr == v->mgr);
 479
 480     result = Cudd_bddCompose(f->mgr,f->node,g->node,(int)Cudd_Regular(v->node)->index);
 481     if (result == NULL) return(NULL);
 482     cuddRef(result);
 483     return(bdd_construct_bdd_t(f->mgr,result));
 484
 485 } /* end of bdd_compose */
 486
 487
 488 /**Function********************************************************************
 489
 490   Synopsis    [Universal Abstraction of Variables.]
 491
 492   SideEffects []
 493
 494 ******************************************************************************/
 495 bdd_t *
 496 bdd_consensus(f, quantifying_vars)
 497 bdd_t *f;
 498 array_t *quantifying_vars;      /* of bdd_t *'s */
 499 {
 500     int i;
 501     bdd_t *variable;
 502     DdNode *cube,*tmpDd,*result;
 503     bdd_manager *mgr;
 504
 505     /* The Boulder package needs the smothing variables passed as a cube.
 506     ** Therefore we must build that cube from the indices of the variables
 507     ** in the array before calling the procedure.
 508     */
 509     mgr = f->mgr;
 510     Cudd_Ref(cube = DD_ONE(mgr));
 511     for (i = 0; i < array_n(quantifying_vars); i++) {
 512         variable = array_fetch(bdd_t *,quantifying_vars,i);
 513
 514         /* Make sure the variable belongs to the same manager */
 515         assert(mgr == variable->mgr);
 516
 517         tmpDd = Cudd_bddAnd(mgr,cube,variable->node);
 518         if (tmpDd == NULL) {
 519             Cudd_RecursiveDeref(mgr, cube);
 520             return(NULL);
 521         }
 522         cuddRef(tmpDd);
 523         Cudd_RecursiveDeref(mgr, cube);
 524         cube = tmpDd;
 525     }
 526
 527     /* Perform the consensus */
 528     result = Cudd_bddUnivAbstract(mgr,f->node,cube);
 529     if (result == NULL) {
 530         Cudd_RecursiveDeref(mgr, cube);
 531         return(NULL);
 532     }
 533     cuddRef(result);
 534     /* Get rid of temporary results */
 535     Cudd_RecursiveDeref(mgr, cube);
 536
 537     /* Build the bdd_t structure for the result */
 538     return(bdd_construct_bdd_t(mgr,result));
 539
 540 } /* end of bdd_consensus */
 541
 542
 543 /**Function********************************************************************
 544
 545   Synopsis    [The compatible projection function.]
 546
 547   Description [The compatible projection function. The reference minterm
 548   is chosen based on the phases of the quantifying variables. If all
 549   variables are in positive phase, the minterm 111...111 is used as
 550   reference.]
 551
 552   SideEffects []
 553
 554 ******************************************************************************/
 555 bdd_t *
 556 bdd_cproject(f, quantifying_vars)
 557 bdd_t *f;
 558 array_t *quantifying_vars;      /* of bdd_t* */
 559 {
 560     DdManager *dd;
 561     DdNode *cube;
 562     DdNode *res;
 563     bdd_t *fi;
 564     int nvars, i;
 565
 566     if (f == NULL) {
 567         fail ("bdd_cproject: invalid BDD");
 568     }
 569
 570     nvars = array_n(quantifying_vars);
 571     if (nvars <= 0) {
 572         fail("bdd_cproject: no projection variables");
 573     }
 574     dd = f->mgr;
 575
 576     cube = DD_ONE(dd);
 577     cuddRef(cube);
 578     for (i = nvars - 1; i >= 0; i--) {
 579         DdNode *tmpp;
 580         fi = array_fetch(bdd_t *, quantifying_vars, i);
 581         tmpp = Cudd_bddAnd(dd,fi->node,cube);
 582         if (tmpp == NULL) {
 583             Cudd_RecursiveDeref(dd,cube);
 584             return(NULL);
 585         }
 586         cuddRef(tmpp);
 587         Cudd_RecursiveDeref(dd,cube);
 588         cube = tmpp;
 589     }
 590
 591     res = Cudd_CProjection(dd,f->node,cube);
 592     if (res == NULL) {
 593         Cudd_RecursiveDeref(dd,cube);
 594         return(NULL);
 595     }
 596     cuddRef(res);
 597     Cudd_RecursiveDeref(dd,cube);
 598
 599     return(bdd_construct_bdd_t(dd,res));
 600
 601 } /* end of bdd_cproject */
 602
 603
 604 /**Function********************************************************************
 605
 606   Synopsis    [ITE.]
 607
 608   SideEffects []
 609
 610 ******************************************************************************/
 611 bdd_t *
 612 bdd_ite(i, t, e, i_phase, t_phase, e_phase)
 613 bdd_t *i;
 614 bdd_t *t;
 615 bdd_t *e;
 616 boolean i_phase;
 617 boolean t_phase;
 618 boolean e_phase;
 619 {
 620     DdNode *newi,*newt,*newe,*ite;
 621
 622     /* Make sure both bdds belong to the same mngr */
 623     assert(i->mgr == t->mgr);
 624     assert(i->mgr == e->mgr);
 625
 626     /* Modify the phases of the operands according to the parameters */
 627     if (!i_phase) {
 628         newi = Cudd_Not(i->node);
 629     } else {
 630         newi = i->node;
 631     }
 632     if (!t_phase) {
 633         newt = Cudd_Not(t->node);
 634     } else {
 635         newt = t->node;
 636     }
 637     if (!e_phase) {
 638         newe = Cudd_Not(e->node);
 639     } else {
 640         newe = e->node;
 641     }
 642
 643     /* Perform the ITE operation */
 644     ite = Cudd_bddIte(i->mgr,newi,newt,newe);
 645     if (ite == NULL) return(NULL);
 646     cuddRef(ite);
 647     return(bdd_construct_bdd_t(i->mgr,ite));
 648
 649 } /* end of bdd_ite */
 650
 651
 652 /**Function********************************************************************
 653
 654   Synopsis    [Restric operator as described in Coudert et al. ICCAD90.]
 655
 656   SideEffects []
 657
 658 ******************************************************************************/
 659 bdd_t *
 660 bdd_minimize(f, c)
 661 bdd_t *f;
 662 bdd_t *c;
 663 {
 664     DdNode *result;
 665
 666     /* Make sure both operands belong to the same manager. */
 667     assert(f->mgr == c->mgr);
 668
 669     result = Cudd_bddRestrict(f->mgr,f->node,c->node);
 670     if (result == NULL) return(NULL);
 671     cuddRef(result);
 672
 673     return(bdd_construct_bdd_t(f->mgr,result));
 674
 675 } /* end of bdd_minimize */
 676
 677
 678 /**Function********************************************************************
 679
 680   Synopsis    [Parametrized version of the Restrict operator.]
 681
 682   Description [Parametrized version of the Restrict operator. Currently
 683   defaults to bdd_minimize.]
 684
 685   SideEffects []
 686
 687 ******************************************************************************/
 688 /*ARGSUSED*/
 689 bdd_t *
 690 bdd_minimize_with_params(f, c, match_type, compl, no_new_vars, return_min)
 691 bdd_t *f;
 692 bdd_t *c;
 693 bdd_min_match_type_t match_type;
 694 boolean compl;
 695 boolean no_new_vars;
 696 boolean return_min;
 697 {
 698     return(bdd_minimize(f,c));
 699
 700 } /* end of bdd_minimize_with_params */
 701
 702
 703 /**Function********************************************************************
 704
 705   Synopsis    [Negation.]
 706
 707   SideEffects []
 708
 709 ******************************************************************************/
 710 bdd_t *
 711 bdd_not(f)
 712 bdd_t *f;
 713 {
 714     DdNode *result;
 715
 716     Cudd_Ref(result = Cudd_Not(f->node));
 717     return(bdd_construct_bdd_t((DdManager *)f->mgr,result));
 718
 719 } /* end of bdd_not */
 720
 721
 722 /**Function********************************************************************
 723
 724   Synopsis    [Returns the one BDD.]
 725
 726   SideEffects []
 727
 728 ******************************************************************************/
 729 bdd_t *
 730 bdd_one(mgr)
 731 bdd_manager *mgr;
 732 {
 733     DdNode *result;
 734
 735     Cudd_Ref(result = DD_ONE((DdManager *)mgr));
 736     return(bdd_construct_bdd_t((DdManager *)mgr,result));
 737
 738 } /* end of bdd_one */
 739
 740
 741 /**Function********************************************************************
 742
 743   Synopsis    [Or of two BDDs.]
 744
 745   SideEffects []
 746
 747 ******************************************************************************/
 748 bdd_t *
 749 bdd_or(f, g, f_phase, g_phase)
 750 bdd_t *f;
 751 bdd_t *g;
 752 boolean f_phase;
 753 boolean g_phase;
 754 {
 755     DdNode *newf,*newg,*forg;
 756     bdd_t *result;
 757
 758     /* Make sure both bdds belong to the same mngr */
 759     assert(f->mgr == g->mgr);
 760
 761     /* Modify the phases of the operands according to the parameters */
 762     if (f_phase) {
 763         newf = Cudd_Not(f->node);
 764     } else {
 765         newf = f->node;
 766     }
 767     if (g_phase) {
 768         newg = Cudd_Not(g->node);
 769     } else {
 770         newg = g->node;
 771     }
 772
 773     /* Perform the OR operation */
 774     forg = Cudd_bddAnd(f->mgr,newf,newg);
 775     if (forg == NULL) return(NULL);
 776     forg = Cudd_Not(forg);
 777     cuddRef(forg);
 778     result = bdd_construct_bdd_t(f->mgr,forg);
 779
 780     return(result);
 781
 782 } /* end of bdd_or */
 783
 784
 785 /**Function********************************************************************
 786
 787   Synopsis    [Existential abstraction of variables.]
 788
 789   SideEffects []
 790
 791 ******************************************************************************/
 792 bdd_t *
 793 bdd_smooth(f, smoothing_vars)
 794 bdd_t *f;
 795 array_t *smoothing_vars;        /* of bdd_t *'s */
 796 {
 797     int i;
 798     bdd_t *variable;
 799     DdNode *cube,*tmpDd,*result;
 800     bdd_manager *mgr;
 801
 802     /* The Boulder package needs the smothing variables passed as a cube.
 803     ** Therefore we must build that cube from the indices of the variables
 804     ** in the array before calling the procedure.
 805     */
 806     mgr = f->mgr;
 807     Cudd_Ref(cube = DD_ONE(mgr));
 808     for (i = 0; i < array_n(smoothing_vars); i++) {
 809         variable = array_fetch(bdd_t *,smoothing_vars,i);
 810
 811         /* Make sure the variable belongs to the same manager. */
 812         assert(mgr == variable->mgr);
 813
 814         tmpDd = Cudd_bddAnd(mgr,cube,variable->node);
 815         if (tmpDd == NULL) {
 816             Cudd_RecursiveDeref(mgr, cube);
 817             return(NULL);
 818         }
 819         cuddRef(tmpDd);
 820         Cudd_RecursiveDeref(mgr, cube);
 821         cube = tmpDd;
 822     }
 823
 824     /* Perform the smoothing */
 825     result = Cudd_bddExistAbstract(mgr,f->node,cube);
 826     if (result == NULL) {
 827         Cudd_RecursiveDeref(mgr, cube);
 828         return(NULL);
 829     }
 830     cuddRef(result);
 831
 832     /* Get rid of temporary results */
 833     Cudd_RecursiveDeref(mgr, cube);
 834
 835     /* Build the bdd_t structure for the result */
 836     return(bdd_construct_bdd_t(mgr,result));
 837
 838 } /* end of bdd_smooth */
 839
 840
 841 /**Function********************************************************************
 842
 843   Synopsis    [Permutes the variables.]
 844
 845   SideEffects []
 846
 847 ******************************************************************************/
 848 bdd_t *
 849 bdd_substitute(f, old_array, new_array)
 850 bdd_t *f;
 851 array_t *old_array;     /* of bdd_t *'s */
 852 array_t *new_array;     /* of bdd_t *'s */
 853 {
 854     int maxOld;
 855     int i,varIndex,from,to;
 856     int *permut;
 857     bdd_t *variable;
 858     DdNode *result;
 859
 860     /* Make sure both arrays have the same number of elements. */
 861     assert(array_n(old_array) == array_n(new_array));
 862
 863     /* Detect what is the highest index of variable to rename. */
 864     maxOld = 0;
 865     for (i = 0; i < array_n(old_array); i++) {
 866         variable = array_fetch(bdd_t *, old_array, i);
 867         /* Make sure the variable belongs to this manager. */
 868         assert(f->mgr == variable->mgr);
 869
 870         varIndex = Cudd_Regular(variable->node)->index;
 871         if (varIndex > maxOld) {
 872             maxOld = varIndex;
 873         }
 874     }
 875     maxOld++;
 876
 877     /* Allocate and fill the array with the trivial permutation. */
 878     permut = ALLOC(int, maxOld);
 879     for (i = 0; i < maxOld; i++) permut[i] = i;
 880
 881     /* Modify the permutation by looking at both arrays old and new. */
 882     for (i = 0; i < array_n(old_array); i++) {
 883         variable = array_fetch(bdd_t *, old_array, i);
 884         from = Cudd_Regular(variable->node)->index;
 885         variable = array_fetch(bdd_t *, new_array, i);
 886         /* Make sure the variable belongs to this manager. */
 887         assert(f->mgr == variable->mgr);
 888
 889         to = Cudd_Regular(variable->node)->index;
 890         permut[from] = to;
 891     }
 892
 893     result = Cudd_bddPermute(f->mgr,f->node,permut);
 894     FREE(permut);
 895     if (result == NULL) return(NULL);
 896     cuddRef(result);
 897     return(bdd_construct_bdd_t(f->mgr,result));
 898
 899 } /* end of bdd_substitute */
 900
 901
 902 /**Function********************************************************************
 903
 904   Synopsis    [Returns the Then branch of the BDD.]
 905
 906   SideEffects []
 907
 908 ******************************************************************************/
 909 bdd_t *
 910 bdd_then(f)
 911 bdd_t *f;
 912 {
 913     DdNode *result;
 914
 915     result = Cudd_T(f->node);
 916     result =  Cudd_NotCond(result,Cudd_IsComplement(f->node));
 917     cuddRef(result);
 918     return(bdd_construct_bdd_t(f->mgr,result));
 919
 920 } /* end of bdd_then */
 921
 922
 923 /**Function********************************************************************
 924
 925   Synopsis    [Returns the else branch of a BDD.]
 926
 927   SideEffects []
 928
 929 ******************************************************************************/
 930 bdd_t *
 931 bdd_else(f)
 932 bdd_t *f;
 933 {
 934     DdNode *result;
 935
 936     result = Cudd_E(f->node);
 937     result =  Cudd_NotCond(result,Cudd_IsComplement(f->node));
 938     cuddRef(result);
 939     return(bdd_construct_bdd_t(f->mgr,result));
 940
 941 } /* end of bdd_else */
 942
 943
 944 /**Function********************************************************************
 945
 946   Synopsis    [Returns the BDD of the top variable.]
 947
 948   Description [Returns the BDD of the top variable of the argument. If
 949   the argument is constant, it returns the constant function itself.]
 950
 951   SideEffects []
 952
 953 ******************************************************************************/
 954 bdd_t *
 955 bdd_top_var(f)
 956 bdd_t *f;
 957 {
 958     DdNode *result;
 959
 960     if (Cudd_IsConstant(f->node)) {
 961         result = f->node;
 962     } else {
 963         result = f->mgr->vars[Cudd_Regular(f->node)->index];
 964     }
 965     cuddRef(result);
 966     return(bdd_construct_bdd_t(f->mgr,result));
 967
 968 } /* end of bdd_top_var */
 969
 970
 971 /**Function********************************************************************
 972
 973   Synopsis    [Computes the exclusive nor of two BDDs.]
 974
 975   SideEffects []
 976
 977 ******************************************************************************/
 978 bdd_t *
 979 bdd_xnor(f, g)
 980 bdd_t *f;
 981 bdd_t *g;
 982 {
 983     DdNode *result;
 984
 985     /* Make sure both operands belong to the same manager. */
 986     assert(f->mgr == g->mgr);
 987
 988     result = Cudd_bddIte(f->mgr,f->node,g->node,Cudd_Not(g->node));
 989     if (result == NULL) return(NULL);
 990     cuddRef(result);
 991     return(bdd_construct_bdd_t(f->mgr,result));
 992
 993 } /* end of bdd_xnor */
 994
 995
 996 /**Function********************************************************************
 997
 998   Synopsis    [Computes the exclusive or of two BDDs.]
 999
1000   SideEffects []
1001
1002 ******************************************************************************/
1003 bdd_t *
1004 bdd_xor(f, g)
1005 bdd_t *f;
1006 bdd_t *g;
1007 {
1008     DdNode *result;
1009
1010     /* Make sure both operands belong to the same manager. */
1011     assert(f->mgr == g->mgr);
1012
1013     result = Cudd_bddIte(f->mgr,f->node,Cudd_Not(g->node),g->node);
1014     if (result == NULL) return(NULL);
1015     cuddRef(result);
1016     return(bdd_construct_bdd_t(f->mgr,result));
1017
1018 } /* end of bdd_xor */
1019
1020
1021 /**Function********************************************************************
1022
1023   Synopsis    [Returns the constant zero BDD.]
1024
1025   SideEffects []
1026
1027 ******************************************************************************/
1028 bdd_t *
1029 bdd_zero(mgr)
1030 bdd_manager *mgr;
1031 {
1032     DdNode *result;
1033
1034     Cudd_Ref(result = Cudd_Not(DD_ONE((mgr))));
1035     return(bdd_construct_bdd_t(mgr,result));
1036
1037 } /* end of bdd_zero */
1038
1039
1040 /**Function********************************************************************
1041
1042   Synopsis    [Equality check.]
1043
1044   SideEffects []
1045
1046 ******************************************************************************/
1047 boolean
1048 bdd_equal(f, g)
1049 bdd_t *f;
1050 bdd_t *g;
1051 {
1052     return(f->node == g->node);
1053
1054 } /* end of bdd_equal */
1055
1056
1057 /**Function********************************************************************
1058
1059   Synopsis    [Returns a BDD included in the intersection of f and g.]
1060
1061   SideEffects []
1062
1063 ******************************************************************************/
1064 bdd_t *
1065 bdd_intersects(f, g)
1066 bdd_t *f;
1067 bdd_t *g;
1068 {
1069     DdNode *result;
1070
1071     /* Make sure both operands belong to the same manager. */
1072     assert(f->mgr == g->mgr);
1073
1074     result = Cudd_bddIntersect(f->mgr,f->node,g->node);
1075     if (result == NULL) return(NULL);
1076     cuddRef(result);
1077     return(bdd_construct_bdd_t(f->mgr,result));
1078
1079 } /* end of bdd_intersects */
1080
1081
1082 /**Function********************************************************************
1083
1084   Synopsis    [Checks a BDD for tautology.]
1085
1086   SideEffects []
1087
1088 ******************************************************************************/
1089 boolean
1090 bdd_is_tautology(f, phase)
1091 bdd_t *f;
1092 boolean phase;
1093 {
1094     if (phase) {
1095         return(f->node == DD_ONE(f->mgr));
1096     } else {
1097         return(f->node == Cudd_Not(DD_ONE(f->mgr)));
1098     }
1099
1100 } /* end of bdd_is_tautology */
1101
1102
1103 /**Function********************************************************************
1104
1105   Synopsis    [Tests for containment of f in g.]
1106
1107   SideEffects []
1108
1109 ******************************************************************************/
1110 boolean
1111 bdd_leq(f, g, f_phase, g_phase)
1112 bdd_t *f;
1113 bdd_t *g;
1114 boolean f_phase;
1115 boolean g_phase;
1116 {
1117     DdNode *newf, *newg;
1118
1119     /* Make sure both operands belong to the same manager. */
1120     assert(f->mgr == g->mgr);
1121
1122     if (f_phase) {
1123         newf = f->node;
1124     } else {
1125         newf = Cudd_Not(f->node);
1126     }
1127     if (g_phase) {
1128         newg = g->node;
1129     } else {
1130         newg = Cudd_Not(g->node);
1131     }
1132
1133     return(Cudd_bddLeq(f->mgr,newf,newg));
1134
1135 } /* end of bdd_leq */
1136
1137
1138 /**Function********************************************************************
1139
1140   Synopsis    [Counts the number of minterms in the on set.]
1141
1142   SideEffects []
1143
1144 ******************************************************************************/
1145 double
1146 bdd_count_onset(f, var_array)
1147 bdd_t *f;
1148 array_t *var_array;     /* of bdd_t *'s */
1149 {
1150     return(Cudd_CountMinterm(f->mgr,f->node,array_n(var_array)));
1151
1152 } /* end of bdd_count_onset */
1153
1154
1155 /**Function********************************************************************
1156
1157   Synopsis    [Obtains the manager of the BDD.]
1158
1159   SideEffects []
1160
1161 ******************************************************************************/
1162 bdd_manager *
1163 bdd_get_manager(f)
1164 bdd_t *f;
1165 {
1166     return(f->mgr);
1167
1168 } /* end of bdd_get_manager */
1169
1170
1171 /**Function********************************************************************
1172
1173   Synopsis    [Returns the node of the BDD.]
1174
1175   SideEffects [Sets is_complemented.]
1176
1177 ******************************************************************************/
1178 bdd_node *
1179 bdd_get_node(f, is_complemented)
1180 bdd_t *f;
1181 boolean *is_complemented;    /* return */
1182 {
1183     if (Cudd_IsComplement(f->node)) {
1184         *is_complemented = TRUE;
1185         return(Cudd_Regular(f->node));
1186     }
1187     *is_complemented = FALSE;
1188     return(f->node);
1189
1190 } /* end of bdd_get_node */
1191
1192
1193 /**Function********************************************************************
1194
1195   Synopsis    [Returns the free field of the BDD.]
1196
1197   SideEffects []
1198
1199 ******************************************************************************/
1200 int
1201 bdd_get_free(f)
1202 bdd_t *f;
1203 {
1204     return (f->free);
1205
1206 } /* end of bdd_get_free */
1207
1208
1209 /**Function********************************************************************
1210
1211   Synopsis    [Obtains some statistics of the BDD package.]
1212
1213   SideEffects [Sets stats.]
1214
1215 ******************************************************************************/
1216 /*ARGSUSED*/
1217 void
1218 bdd_get_stats(mgr, stats)
1219 bdd_manager *mgr;
1220 bdd_stats *stats;       /* return */
1221 {
1222     stats->nodes.total = mgr->keys;
1223     stats->nodes.used = mgr->keys - mgr->dead;
1224     stats->nodes.unused = mgr->dead;
1225     stats->cache.itetable.hits = (unsigned int) Cudd_ReadCacheHits(mgr);
1226     stats->cache.itetable.misses = (unsigned int)
1227         (Cudd_ReadCacheLookUps(mgr) - Cudd_ReadCacheHits(mgr));
1228     stats->cache.itetable.collisions = mgr->cachecollisions;
1229     stats->cache.itetable.inserts = mgr->cacheinserts;
1230     stats->gc.times = Cudd_ReadGarbageCollections(mgr);
1231     return;
1232
1233 } /* end of bdd_get_stats */
1234
1235
1236 /**Function********************************************************************
1237
1238   Synopsis    [Obtains the support of the BDD.]
1239
1240   SideEffects []
1241
1242 ******************************************************************************/
1243 var_set_t *
1244 bdd_get_support(f)
1245 bdd_t *f;
1246 {
1247     DdNode *support, *scan;
1248     var_set_t *result;
1249
1250     support = Cudd_Support(f->mgr,f->node);
1251     if (support == NULL) return(NULL);
1252     cuddRef(support);
1253
1254     result = var_set_new((int) f->mgr->size);
1255     scan = support;
1256     while (!cuddIsConstant(scan)) {
1257         var_set_set_elt(result, scan->index);
1258         scan = cuddT(scan);
1259     }
1260     Cudd_RecursiveDeref(f->mgr,support);
1261
1262     return(result);
1263
1264 } /* end of bdd_get_support */
1265
1266
1267 /**Function********************************************************************
1268
1269   Synopsis    [Obtains the array of indices of an array of variables.]
1270
1271   SideEffects []
1272
1273 ******************************************************************************/
1274 array_t *
1275 bdd_get_varids(var_array)
1276 array_t *var_array;
1277 {
1278     int i;
1279     int index;
1280     bdd_t *var;
1281     array_t *result = array_alloc(int,array_n(var_array));
1282
1283     for (i = 0; i < array_n(var_array); i++) {
1284         var = array_fetch(bdd_t *, var_array, i);
1285         index = Cudd_Regular(var->node)->index;
1286         (void) array_insert_last(int, result, index);
1287     }
1288     return(result);
1289
1290 } /* end of bdd_get_varids */
1291
1292
1293 /**Function********************************************************************
1294
1295   Synopsis    [Returns the number of variables in the manager.]
1296
1297   SideEffects []
1298
1299 ******************************************************************************/
1300 unsigned int
1301 bdd_num_vars(mgr)
1302 bdd_manager *mgr;
1303 {
1304     return(mgr->size);
1305
1306 } /* end of bdd_num_vars */
1307
1308
1309 /**Function********************************************************************
1310
1311   Synopsis    [Prints the BDD.]
1312
1313   SideEffects []
1314
1315 ******************************************************************************/
1316 void
1317 bdd_print(f)
1318 bdd_t *f;
1319 {
1320     (void) cuddP(f->mgr,f->node);
1321
1322 } /* end of bdd_print */
1323
1324
1325 /**Function********************************************************************
1326
1327   Synopsis    [Prints statistics about the package.]
1328
1329   SideEffects []
1330
1331 ******************************************************************************/
1332 void
1333 bdd_print_stats(stats, file)
1334 bdd_stats stats;
1335 FILE *file;
1336 {
1337 #ifndef DD_STATS
1338     fprintf(stderr,"CU DD package: bdd_print_stats: Statistics turned off. No output\n");
1339 #else
1340     fprintf(file,"CU DD Package Statistics\n");
1341     fprintf(file,"  Cache hits : %d\n",stats.cache.itetable.hits);
1342     fprintf(file,"  Cache misses : %d\n",stats.cache.itetable.misses);
1343     fprintf(file,"  Cache collisions : %d\n",stats.cache.itetable.collisions);
1344     fprintf(file,"  Cache inserts: %d\n",stats.cache.itetable.inserts);
1345 #endif
1346     return;
1347
1348 } /* end of bdd_print_stats */
1349
1350
1351 /**Function********************************************************************
1352
1353   Synopsis    [Computes the number of nodes of a BDD.]
1354
1355   SideEffects []
1356
1357 ******************************************************************************/
1358 int
1359 bdd_size(f)
1360 bdd_t *f;
1361 {
1362     return(Cudd_DagSize(f->node));
1363
1364 } /* end of bdd_size */
1365
1366
1367 /**Function********************************************************************
1368
1369   Synopsis    [Accesses the id of the top variable.]
1370
1371   SideEffects []
1372
1373 ******************************************************************************/
1374 bdd_variableId
1375 bdd_top_var_id(f)
1376 bdd_t *f;
1377 {
1378     return(Cudd_Regular(f->node)->index);
1379
1380 } /* end of bdd_top_var_id */
1381
1382
1383 /**Function********************************************************************
1384
1385   Synopsis    [Accesses the external_hooks field of the manager.]
1386
1387   SideEffects []
1388
1389 ******************************************************************************/
1390 bdd_external_hooks *
1391 bdd_get_external_hooks(mgr)
1392 bdd_manager *mgr;
1393 {
1394     return((bdd_external_hooks *)(mgr->hooks));
1395
1396 } /* end of bdd_get_external_hooks */
1397
1398
1399 /**Function********************************************************************
1400
1401   Synopsis    [Registers a new hook with the manager.]
1402
1403   SideEffects []
1404
1405 ******************************************************************************/
1406 /*ARGSUSED*/
1407 void
1408 bdd_register_daemon(mgr, daemon)
1409 bdd_manager *mgr;
1410 void (*daemon)();
1411 {
1412     fprintf(stderr,"CU DD Package: bdd_register_daemon translated to no-op.\n");
1413     return;
1414
1415 } /* end of bdd_register_daemon */
1416
1417
1418 /**Function********************************************************************
1419
1420   Synopsis    [Turns on or off garbage collection.]
1421
1422   SideEffects []
1423
1424 ******************************************************************************/
1425 void
1426 bdd_set_gc_mode(mgr, no_gc)
1427 bdd_manager *mgr;
1428 boolean no_gc;
1429 {
1430     if (no_gc) {
1431         Cudd_DisableGarbageCollection(mgr);
1432     } else {
1433         Cudd_EnableGarbageCollection(mgr);
1434     }
1435     return;
1436
1437 } /* end of bdd_set_gc_mode */
1438
1439
1440 /**Function********************************************************************
1441
1442   Synopsis    [Reorders the BDD pool.]
1443
1444   SideEffects []
1445
1446 ******************************************************************************/
1447 void
1448 bdd_dynamic_reordering(mgr, algorithm_type)
1449 bdd_manager *mgr;
1450 bdd_reorder_type_t algorithm_type;
1451 {
1452     switch (algorithm_type) {
1453       case BDD_REORDER_SIFT:
1454         mgr->autoMethod = CUDD_REORDER_SIFT;
1455         mgr->autoDyn = 1;
1456         break;
1457       case BDD_REORDER_WINDOW:
1458       case BDD_REORDER_WINDOW4:
1459         mgr->autoMethod = CUDD_REORDER_WINDOW4;
1460         mgr->autoDyn = 1;
1461         break;
1462       case BDD_REORDER_NONE:
1463         mgr->autoDyn = 0;
1464         break;
1465       case BDD_REORDER_SAME:
1466         mgr->autoDyn = 1;
1467         break;
1468       case BDD_REORDER_RANDOM:
1469         mgr->autoMethod = CUDD_REORDER_RANDOM;
1470         mgr->autoDyn = 1;
1471         break;
1472       case BDD_REORDER_RANDOM_PIVOT:
1473         mgr->autoMethod = CUDD_REORDER_RANDOM_PIVOT;
1474         mgr->autoDyn = 1;
1475         break;
1476       case BDD_REORDER_SIFT_CONVERGE:
1477         mgr->autoMethod = CUDD_REORDER_SIFT_CONVERGE;
1478         mgr->autoDyn = 1;
1479         break;
1480       case BDD_REORDER_SYMM_SIFT:
1481         mgr->autoMethod = CUDD_REORDER_SYMM_SIFT;
1482         mgr->autoDyn = 1;
1483         break;
1484       case BDD_REORDER_SYMM_SIFT_CONV:
1485         mgr->autoMethod = CUDD_REORDER_SYMM_SIFT_CONV;
1486         mgr->autoDyn = 1;
1487         break;
1488       case BDD_REORDER_WINDOW2:
1489         mgr->autoMethod = CUDD_REORDER_WINDOW2;
1490         mgr->autoDyn = 1;
1491         break;
1492       case BDD_REORDER_WINDOW3:
1493         mgr->autoMethod = CUDD_REORDER_WINDOW3;
1494         mgr->autoDyn = 1;
1495         break;
1496       case BDD_REORDER_WINDOW2_CONV:
1497         mgr->autoMethod = CUDD_REORDER_WINDOW2_CONV;
1498         mgr->autoDyn = 1;
1499         break;
1500       case BDD_REORDER_WINDOW3_CONV:
1501         mgr->autoMethod = CUDD_REORDER_WINDOW3_CONV;
1502         mgr->autoDyn = 1;
1503         break;
1504       case BDD_REORDER_WINDOW4_CONV:
1505         mgr->autoMethod = CUDD_REORDER_WINDOW4_CONV;
1506         mgr->autoDyn = 1;
1507         break;
1508       case BDD_REORDER_GROUP_SIFT:
1509         mgr->autoMethod = CUDD_REORDER_GROUP_SIFT;
1510         mgr->autoDyn = 1;
1511         break;
1512       case BDD_REORDER_GROUP_SIFT_CONV:
1513         mgr->autoMethod = CUDD_REORDER_GROUP_SIFT_CONV;
1514         mgr->autoDyn = 1;
1515         break;
1516       case BDD_REORDER_ANNEALING:
1517         mgr->autoMethod = CUDD_REORDER_ANNEALING;
1518         mgr->autoDyn = 1;
1519         break;
1520       case BDD_REORDER_GENETIC:
1521         mgr->autoMethod = CUDD_REORDER_GENETIC;
1522         mgr->autoDyn = 1;
1523         break;
1524       default:
1525         fprintf(stderr,"CU DD Package: Reordering algorithm not considered\n");
1526     }
1527
1528 } /* end of bdd_dynamic_reordering */
1529
1530
1531 /**Function********************************************************************
1532
1533   Synopsis    [Calls reordering explicitly.]
1534
1535   SideEffects []
1536
1537 ******************************************************************************/
1538 void
1539 bdd_reorder(mgr)
1540 bdd_manager *mgr;
1541 {
1542     (void) Cudd_ReduceHeap(mgr,mgr->autoMethod,10); /* 10 = whatever (Verbatim from file ddTable.c) */
1543     return;
1544
1545 } /* end of bdd_reorder */
1546
1547
1548 /**Function********************************************************************
1549
1550   Synopsis    [Read the number of reorderings the package has performed
1551   so far.]
1552
1553   SideEffects []
1554
1555 ******************************************************************************/
1556 int
1557 bdd_read_reorderings(mgr)
1558 bdd_manager *mgr;
1559 {
1560     return Cudd_ReadReorderings((DdManager *)mgr);
1561
1562 } /* end of bdd_read_reorderings */
1563
1564
1565 /**Function********************************************************************
1566
1567   Synopsis    [Gets the id variable for one level in the BDD.]
1568
1569   SideEffects []
1570
1571 ******************************************************************************/
1572 bdd_variableId
1573 bdd_get_id_from_level(mgr, level)
1574 bdd_manager *mgr;
1575 long level;
1576 {
1577     return(mgr->invperm[level]);
1578
1579 } /* end of bdd_get_id_from_level */
1580
1581
1582 /**Function********************************************************************
1583
1584   Synopsis    [Gets the level of the top variable of the BDD.]
1585
1586   SideEffects []
1587
1588 ******************************************************************************/
1589 long
1590 bdd_top_var_level(mgr, fn)
1591 bdd_manager *mgr;
1592 bdd_t *fn;
1593 {
1594     return((long) cuddI(mgr,Cudd_Regular(fn->node)->index));
1595
1596 } /* end of bdd_top_var_level */
1597
1598
1599 /**Function********************************************************************
1600
1601   Synopsis    [Returns TRUE if the argument BDD is a cube; FALSE
1602   otherwise.]
1603
1604   SideEffects []
1605
1606 ******************************************************************************/
1607 boolean
1608 bdd_is_cube(f)
1609 bdd_t *f;
1610 {
1611     struct DdManager *manager;
1612
1613     if (f == NULL) {
1614         fail("bdd_is_cube: invalid BDD");
1615     }
1616     if (f->free) fail ("Freed BDD passed to bdd_is_cube");
1617     manager = (DdManager *) f->mgr;
1618     return((boolean)cuddCheckCube(manager,f->node));
1619
1620 } /* end of bdd_is_cube */
1621
1622
1623 /**Function********************************************************************
1624
1625   Synopsis    [Calls the garbage collector explicitly.]
1626
1627   SideEffects []
1628
1629 ******************************************************************************/
1630 void
1631 bdd_gc(mgr)
1632 bdd_manager *mgr;
1633 {
1634     cuddGarbageCollect(mgr,1);
1635
1636 } /* end of bdd_gc */
1637
1638
1639 /**Function********************************************************************
1640
1641   Synopsis    [Computes the shared size of an array of BDDs.]
1642
1643   Description [Computes the shared size of an array of BDDs. Returns
1644   CUDD_OUT_OF_MEM in case of failure.]
1645
1646   SideEffects []
1647
1648 ******************************************************************************/
1649 long
1650 bdd_size_multiple(bddArray)
1651 array_t *bddArray;
1652 {
1653     DdNode **nodeArray;
1654     bdd_t *bddUnit;
1655     long result;
1656     int i;
1657
1658     nodeArray = ALLOC(DdNode *, array_n(bddArray));
1659     if (nodeArray == NULL) return(CUDD_OUT_OF_MEM);
1660     for (i = 0; i < array_n(bddArray); i++) {
1661         bddUnit = array_fetch(bdd_t *, bddArray, i);
1662         nodeArray[i] = bddUnit->node;
1663     }
1664
1665     result = Cudd_SharingSize(nodeArray,array_n(bddArray));
1666
1667     /* Clean up */
1668     FREE(nodeArray);
1669
1670     return(result);
1671
1672 } /* end of bdd_size_multiple */
1673
1674
1675 /**Function********************************************************************
1676
1677   Synopsis    [Returns the first cube of the function.
1678   A generator is also returned, which will iterate over the rest.]
1679
1680   Description [Defines an iterator on the onset of a BDD.  Two routines
1681   are provided: bdd_first_cube, which extracts one cube from a BDD and
1682   returns a bdd_gen structure containing the information necessary to
1683   continue the enumeration; and bdd_next_cube, which returns 1 if
1684   another cube was found, and 0 otherwise. A cube is represented as an
1685   array of bdd_literal (which are integers in {0, 1, 2}), where 0
1686   represents negated literal, 1 for literal, and 2 for don't care.
1687   Returns a disjoint cover.  A third routine is there to clean up.]
1688
1689   SideEffects []
1690
1691   SeeAlso [bdd_next_cube bdd_gen_free]
1692
1693 ******************************************************************************/
1694 bdd_gen *
1695 bdd_first_cube(fn, cube)
1696 bdd_t *fn;
1697 array_t **cube; /* of bdd_literal */
1698 {
1699     bdd_manager *manager;
1700     bdd_gen *gen;
1701     int i;
1702     int *icube;
1703     CUDD_VALUE_TYPE value;
1704
1705     /* Make sure we receive a valid bdd_t. (So to speak.) */
1706     assert(fn != 0);
1707
1708     manager = fn->mgr;
1709
1710     /* Initialize the generator. */
1711     gen = ALLOC(bdd_gen,1);
1712     if (gen == NULL) return(NULL);
1713     gen->manager = manager;
1714
1715     gen->cube = array_alloc(bdd_literal, manager->size);
1716     if (gen->cube == NULL) {
1717         fail("Bdd Package: Out of memory in bdd_first_cube");
1718     }
1719
1720     gen->ddGen = Cudd_FirstCube(manager,fn->node,&icube,&value);
1721     if (gen->ddGen == NULL) {
1722         fail("Cudd Package: Out of memory in bdd_first_cube");
1723     }
1724
1725     if (!Cudd_IsGenEmpty(gen->ddGen)) {
1726         /* Copy icube to the array_t cube. */
1727         for (i = 0; i < manager->size; i++) {
1728             int myconst = icube[i];
1729             array_insert(bdd_literal, gen->cube, i, myconst);
1730         }
1731         *cube = gen->cube;
1732     }
1733
1734     return(gen);
1735
1736 } /* end of bdd_first_cube */
1737
1738
1739 /**Function********************************************************************
1740
1741   Synopsis    [Gets the next cube on the generator. Returns {TRUE,
1742   FALSE} when {more, no more}.]
1743
1744   SideEffects []
1745
1746   SeeAlso     [bdd_first_cube bdd_gen_free]
1747
1748 ******************************************************************************/
1749 boolean
1750 bdd_next_cube(gen, cube)
1751 bdd_gen *gen;
1752 array_t **cube;         /* of bdd_literal */
1753 {
1754     int retval;
1755     int *icube;
1756     CUDD_VALUE_TYPE value;
1757     int i;
1758
1759     retval = Cudd_NextCube(gen->ddGen,&icube,&value);
1760     if (!Cudd_IsGenEmpty(gen->ddGen)) {
1761         /* Copy icube to the array_t cube. */
1762         for (i = 0; i < gen->manager->size; i++) {
1763             int myconst = icube[i];
1764             array_insert(bdd_literal, gen->cube, i, myconst);
1765         }
1766         *cube = gen->cube;
1767     }
1768
1769     return(retval);
1770
1771 } /* end of bdd_next_cube */
1772
1773
1774 /**Function********************************************************************
1775
1776   Synopsis    [Gets the first node in the BDD and returns a generator.]
1777
1778   SideEffects []
1779
1780   SeeAlso [bdd_next_node]
1781
1782 ******************************************************************************/
1783 bdd_gen *
1784 bdd_first_node(fn, node)
1785 bdd_t *fn;
1786 bdd_node **node;        /* return */
1787 {
1788     bdd_manager *manager;
1789     bdd_gen *gen;
1790
1791     /* Make sure we receive a valid bdd_t. (So to speak.) */
1792     assert(fn != 0);
1793
1794     manager = fn->mgr;
1795
1796     /* Initialize the generator. */
1797     gen = ALLOC(bdd_gen,1);
1798     if (gen == NULL) return(NULL);
1799     gen->manager = manager;
1800     gen->cube = NULL;
1801
1802     gen->ddGen = Cudd_FirstNode(manager,fn->node,node);
1803     if (gen->ddGen == NULL) {
1804         fail("Cudd Package: Out of memory in bdd_first_node");
1805     }
1806
1807     return(gen);
1808
1809 } /* end of bdd_first_node */
1810
1811
1812 /**Function********************************************************************
1813
1814   Synopsis    [Gets the next node in the BDD. Returns {TRUE, FALSE} when
1815   {more, no more}.]
1816
1817   SideEffects []
1818
1819   SeeAlso [bdd_first_node]
1820
1821 ******************************************************************************/
1822 boolean
1823 bdd_next_node(gen, node)
1824 bdd_gen *gen;
1825 bdd_node **node;        /* return */
1826 {
1827     return(Cudd_NextNode(gen->ddGen,node));
1828
1829 } /* end of bdd_next_node */
1830
1831
1832 /**Function********************************************************************
1833
1834   Synopsis    [Frees up the space used by the generator. Returns an int
1835   so that it is easier to fit in a foreach macro. Returns 0 (to make it
1836   easy to put in expressions).]
1837
1838   SideEffects []
1839
1840   SeeAlso []
1841
1842 ******************************************************************************/
1843 int
1844 bdd_gen_free(gen)
1845 bdd_gen *gen;
1846 {
1847     if (gen->cube != NULL) array_free(gen->cube);
1848     Cudd_GenFree(gen->ddGen);
1849     FREE(gen);
1850     return(0);
1851
1852 } /* end of bdd_gen_free */
1853
1854
1855 /**Function********************************************************************
1856
1857   Synopsis    [Queries the status of a generator.]
1858
1859   Description [Queries the status of a generator. Returns 1 if the
1860   generator is empty or NULL; 0 otherswise.]
1861
1862   SideEffects []
1863
1864   SeeAlso [bdd_first_cube bdd_next_cube bdd_first_node bdd_next_node
1865   bdd_gen_free]
1866
1867 ******************************************************************************/
1868 boolean
1869 bdd_is_gen_empty(gen)
1870 bdd_gen *gen;
1871 {
1872     return(Cudd_IsGenEmpty(gen->ddGen));
1873
1874 } /* end of bdd_is_gen_empty */
1875
1876
1877 /**Function********************************************************************
1878
1879   Synopsis    [Function that creates a variable of a given index.]
1880
1881   SideEffects []
1882
1883 ******************************************************************************/
1884 bdd_t *
1885 bdd_var_with_index(manager, index)
1886 bdd_manager *manager;
1887 int index;
1888 {
1889     DdNode *var;
1890
1891     var = Cudd_bddIthVar(manager, index);
1892     cuddRef(var);
1893     return(bdd_construct_bdd_t(manager, var));
1894
1895 } /* end of bdd_var_with_index */
1896
1897
1898 /**Function********************************************************************
1899
1900   Synopsis    [Temporary function that is empty.]
1901
1902   SideEffects []
1903
1904 ******************************************************************************/
1905 /*ARGSUSED*/
1906 void
1907 bdd_new_var_block(f, n)
1908 bdd_t *f;
1909 long n;
1910 {
1911     return;
1912
1913 } /* end of bdd_new_var_block */
1914
1915
1916 /*---------------------------------------------------------------------------*/
1917 /* Definition of internal functions                                          */
1918 /*---------------------------------------------------------------------------*/
1919
1920
1921 /*---------------------------------------------------------------------------*/
1922 /* Definition of static functions                                            */
1923 /*---------------------------------------------------------------------------*/
1924
1925
1926 /**Function********************************************************************
1927
1928   Synopsis    [Builds the bdd_t structure.]
1929
1930   Description [Builds the bdd_t structure from manager and node.
1931   Assumes that the reference count of the node has already been
1932   increased.]
1933
1934   SideEffects []
1935
1936 ******************************************************************************/
1937 static bdd_t *
1938 bdd_construct_bdd_t(mgr,fn)
1939 DdManager *mgr;
1940 DdNode * fn;
1941 {
1942     bdd_t *result;
1943
1944     result = ALLOC(bdd_t, 1);
1945     if (result == NULL) {
1946         Cudd_RecursiveDeref(mgr,fn);
1947         return(NULL);
1948     }
1949     result->mgr = mgr;
1950     result->node = fn;
1951     result->free = FALSE;
1952     return(result);
1953
1954 } /* end of bdd_construct_bdd_t */