distr/cudd/cuddSat.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddSat.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Functions for the solution of satisfiability related
   8   problems.]
   9
  10   Description [External procedures included in this file:
  11                 <ul>
  12                 <li> Cudd_Eval()
  13                 <li> Cudd_ShortestPath()
  14                 <li> Cudd_LargestCube()
  15                 <li> Cudd_ShortestLength()
  16                 <li> Cudd_Decreasing()
  17                 <li> Cudd_Increasing()
  18                 <li> Cudd_EquivDC()
  19                 <li> Cudd_bddLeqUnless()
  20                 <li> Cudd_EqualSupNorm()
  21                 <li> Cudd_bddMakePrime()
  22                 </ul>
  23         Internal procedures included in this module:
  24                 <ul>
  25                 <li> cuddBddMakePrime()
  26                 </ul>
  27         Static procedures included in this module:
  28                 <ul>
  29                 <li> freePathPair()
  30                 <li> getShortest()
  31                 <li> getPath()
  32                 <li> getLargest()
  33                 <li> getCube()
  34                 </ul>]
  35
  36   Author      [Seh-Woong Jeong, Fabio Somenzi]
  37
  38   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  39
  40   All rights reserved.
  41
  42   Redistribution and use in source and binary forms, with or without
  43   modification, are permitted provided that the following conditions
  44   are met:
  45
  46   Redistributions of source code must retain the above copyright
  47   notice, this list of conditions and the following disclaimer.
  48
  49   Redistributions in binary form must reproduce the above copyright
  50   notice, this list of conditions and the following disclaimer in the
  51   documentation and/or other materials provided with the distribution.
  52
  53   Neither the name of the University of Colorado nor the names of its
  54   contributors may be used to endorse or promote products derived from
  55   this software without specific prior written permission.
  56
  57   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  58   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  59   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  60   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  61   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  62   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  63   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  64   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  65   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  66   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  67   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  68   POSSIBILITY OF SUCH DAMAGE.]
  69
  70 ******************************************************************************/
  71
  72 #include "util.h"
  73 #include "cuddInt.h"
  74
  75 /*---------------------------------------------------------------------------*/
  76 /* Constant declarations                                                     */
  77 /*---------------------------------------------------------------------------*/
  78
  79 #define DD_BIGGY        1000000
  80
  81 /*---------------------------------------------------------------------------*/
  82 /* Stucture declarations                                                     */
  83 /*---------------------------------------------------------------------------*/
  84
  85 /*---------------------------------------------------------------------------*/
  86 /* Type declarations                                                         */
  87 /*---------------------------------------------------------------------------*/
  88
  89 typedef struct cuddPathPair {
  90     int pos;
  91     int neg;
  92 } cuddPathPair;
  93
  94 /*---------------------------------------------------------------------------*/
  95 /* Variable declarations                                                     */
  96 /*---------------------------------------------------------------------------*/
  97
  98 #ifndef lint
  99 static char rcsid[] DD_UNUSED = "$Id: cuddSat.c,v 1.36 2009/03/08 02:49:02 fabio Exp $";
 100 #endif
 101
 102 static  DdNode  *one, *zero;
 103
 104 /*---------------------------------------------------------------------------*/
 105 /* Macro declarations                                                        */
 106 /*---------------------------------------------------------------------------*/
 107
 108 #define WEIGHT(weight, col)     ((weight) == NULL ? 1 : weight[col])
 109
 110 #ifdef __cplusplus
 111 extern "C" {
 112 #endif
 113
 114 /**AutomaticStart*************************************************************/
 115
 116 /*---------------------------------------------------------------------------*/
 117 /* Static function prototypes                                                */
 118 /*---------------------------------------------------------------------------*/
 119
 120 static enum st_retval freePathPair (char *key, char *value, char *arg);
 121 static cuddPathPair getShortest (DdNode *root, int *cost, int *support, st_table *visited);
 122 static DdNode * getPath (DdManager *manager, st_table *visited, DdNode *f, int *weight, int cost);
 123 static cuddPathPair getLargest (DdNode *root, st_table *visited);
 124 static DdNode * getCube (DdManager *manager, st_table *visited, DdNode *f, int cost);
 125
 126 /**AutomaticEnd***************************************************************/
 127
 128 #ifdef __cplusplus
 129 }
 130 #endif
 131
 132 /*---------------------------------------------------------------------------*/
 133 /* Definition of exported functions                                          */
 134 /*---------------------------------------------------------------------------*/
 135
 136
 137 /**Function********************************************************************
 138
 139   Synopsis    [Returns the value of a DD for a given variable assignment.]
 140
 141   Description [Finds the value of a DD for a given variable
 142   assignment. The variable assignment is passed in an array of int's,
 143   that should specify a zero or a one for each variable in the support
 144   of the function. Returns a pointer to a constant node. No new nodes
 145   are produced.]
 146
 147   SideEffects [None]
 148
 149   SeeAlso     [Cudd_bddLeq Cudd_addEvalConst]
 150
 151 ******************************************************************************/
 152 DdNode *
 153 Cudd_Eval(
 154   DdManager * dd,
 155   DdNode * f,
 156   int * inputs)
 157 {
 158     int comple;
 159     DdNode *ptr;
 160
 161     comple = Cudd_IsComplement(f);
 162     ptr = Cudd_Regular(f);
 163
 164     while (!cuddIsConstant(ptr)) {
 165         if (inputs[ptr->index] == 1) {
 166             ptr = cuddT(ptr);
 167         } else {
 168             comple ^= Cudd_IsComplement(cuddE(ptr));
 169             ptr = Cudd_Regular(cuddE(ptr));
 170         }
 171     }
 172     return(Cudd_NotCond(ptr,comple));
 173
 174 } /* end of Cudd_Eval */
 175
 176
 177 /**Function********************************************************************
 178
 179   Synopsis    [Finds a shortest path in a DD.]
 180
 181   Description [Finds a shortest path in a DD. f is the DD we want to
 182   get the shortest path for; weight\[i\] is the weight of the THEN arc
 183   coming from the node whose index is i. If weight is NULL, then unit
 184   weights are assumed for all THEN arcs. All ELSE arcs have 0 weight.
 185   If non-NULL, both weight and support should point to arrays with at
 186   least as many entries as there are variables in the manager.
 187   Returns the shortest path as the BDD of a cube.]
 188
 189   SideEffects [support contains on return the true support of f.
 190   If support is NULL on entry, then Cudd_ShortestPath does not compute
 191   the true support info. length contains the length of the path.]
 192
 193   SeeAlso     [Cudd_ShortestLength Cudd_LargestCube]
 194
 195 ******************************************************************************/
 196 DdNode *
 197 Cudd_ShortestPath(
 198   DdManager * manager,
 199   DdNode * f,
 200   int * weight,
 201   int * support,
 202   int * length)
 203 {
 204     DdNode      *F;
 205     st_table    *visited;
 206     DdNode      *sol;
 207     cuddPathPair *rootPair;
 208     int         complement, cost;
 209     int         i;
 210
 211     one = DD_ONE(manager);
 212     zero = DD_ZERO(manager);
 213
 214     /* Initialize support. Support does not depend on variable order.
 215     ** Hence, it does not need to be reinitialized if reordering occurs.
 216     */
 217     if (support) {
 218       for (i = 0; i < manager->size; i++) {
 219         support[i] = 0;
 220       }
 221     }
 222
 223     if (f == Cudd_Not(one) || f == zero) {
 224       *length = DD_BIGGY;
 225       return(Cudd_Not(one));
 226     }
 227     /* From this point on, a path exists. */
 228
 229     do {
 230         manager->reordered = 0;
 231
 232         /* Initialize visited table. */
 233         visited = st_init_table(st_ptrcmp, st_ptrhash);
 234
 235         /* Now get the length of the shortest path(s) from f to 1. */
 236         (void) getShortest(f, weight, support, visited);
 237
 238         complement = Cudd_IsComplement(f);
 239
 240         F = Cudd_Regular(f);
 241
 242         if (!st_lookup(visited, F, &rootPair)) return(NULL);
 243
 244         if (complement) {
 245           cost = rootPair->neg;
 246         } else {
 247           cost = rootPair->pos;
 248         }
 249
 250         /* Recover an actual shortest path. */
 251         sol = getPath(manager,visited,f,weight,cost);
 252
 253         st_foreach(visited, freePathPair, NULL);
 254         st_free_table(visited);
 255
 256     } while (manager->reordered == 1);
 257
 258     *length = cost;
 259     return(sol);
 260
 261 } /* end of Cudd_ShortestPath */
 262
 263
 264 /**Function********************************************************************
 265
 266   Synopsis    [Finds a largest cube in a DD.]
 267
 268   Description [Finds a largest cube in a DD. f is the DD we want to
 269   get the largest cube for. The problem is translated into the one of
 270   finding a shortest path in f, when both THEN and ELSE arcs are assumed to
 271   have unit length. This yields a largest cube in the disjoint cover
 272   corresponding to the DD. Therefore, it is not necessarily the largest
 273   implicant of f.  Returns the largest cube as a BDD.]
 274
 275   SideEffects [The number of literals of the cube is returned in length.]
 276
 277   SeeAlso     [Cudd_ShortestPath]
 278
 279 ******************************************************************************/
 280 DdNode *
 281 Cudd_LargestCube(
 282   DdManager * manager,
 283   DdNode * f,
 284   int * length)
 285 {
 286     register    DdNode  *F;
 287     st_table    *visited;
 288     DdNode      *sol;
 289     cuddPathPair *rootPair;
 290     int         complement, cost;
 291
 292     one = DD_ONE(manager);
 293     zero = DD_ZERO(manager);
 294
 295     if (f == Cudd_Not(one) || f == zero) {
 296         *length = DD_BIGGY;
 297         return(Cudd_Not(one));
 298     }
 299     /* From this point on, a path exists. */
 300
 301     do {
 302         manager->reordered = 0;
 303
 304         /* Initialize visited table. */
 305         visited = st_init_table(st_ptrcmp, st_ptrhash);
 306
 307         /* Now get the length of the shortest path(s) from f to 1. */
 308         (void) getLargest(f, visited);
 309
 310         complement = Cudd_IsComplement(f);
 311
 312         F = Cudd_Regular(f);
 313
 314         if (!st_lookup(visited, F, &rootPair)) return(NULL);
 315
 316         if (complement) {
 317           cost = rootPair->neg;
 318         } else {
 319           cost = rootPair->pos;
 320         }
 321
 322         /* Recover an actual shortest path. */
 323         sol = getCube(manager,visited,f,cost);
 324
 325         st_foreach(visited, freePathPair, NULL);
 326         st_free_table(visited);
 327
 328     } while (manager->reordered == 1);
 329
 330     *length = cost;
 331     return(sol);
 332
 333 } /* end of Cudd_LargestCube */
 334
 335
 336 /**Function********************************************************************
 337
 338   Synopsis    [Find the length of the shortest path(s) in a DD.]
 339
 340   Description [Find the length of the shortest path(s) in a DD. f is
 341   the DD we want to get the shortest path for; weight\[i\] is the
 342   weight of the THEN edge coming from the node whose index is i. All
 343   ELSE edges have 0 weight. Returns the length of the shortest
 344   path(s) if such a path is found; a large number if the function is
 345   identically 0, and CUDD_OUT_OF_MEM in case of failure.]
 346
 347   SideEffects [None]
 348
 349   SeeAlso     [Cudd_ShortestPath]
 350
 351 ******************************************************************************/
 352 int
 353 Cudd_ShortestLength(
 354   DdManager * manager,
 355   DdNode * f,
 356   int * weight)
 357 {
 358     register    DdNode  *F;
 359     st_table    *visited;
 360     cuddPathPair *my_pair;
 361     int         complement, cost;
 362
 363     one = DD_ONE(manager);
 364     zero = DD_ZERO(manager);
 365
 366     if (f == Cudd_Not(one) || f == zero) {
 367         return(DD_BIGGY);
 368     }
 369
 370     /* From this point on, a path exists. */
 371     /* Initialize visited table and support. */
 372     visited = st_init_table(st_ptrcmp, st_ptrhash);
 373
 374     /* Now get the length of the shortest path(s) from f to 1. */
 375     (void) getShortest(f, weight, NULL, visited);
 376
 377     complement = Cudd_IsComplement(f);
 378
 379     F = Cudd_Regular(f);
 380
 381     if (!st_lookup(visited, F, &my_pair)) return(CUDD_OUT_OF_MEM);
 382
 383     if (complement) {
 384         cost = my_pair->neg;
 385     } else {
 386         cost = my_pair->pos;
 387     }
 388
 389     st_foreach(visited, freePathPair, NULL);
 390     st_free_table(visited);
 391
 392     return(cost);
 393
 394 } /* end of Cudd_ShortestLength */
 395
 396
 397 /**Function********************************************************************
 398
 399   Synopsis    [Determines whether a BDD is negative unate in a
 400   variable.]
 401
 402   Description [Determines whether the function represented by BDD f is
 403   negative unate (monotonic decreasing) in variable i. Returns the
 404   constant one is f is unate and the (logical) constant zero if it is not.
 405   This function does not generate any new nodes.]
 406
 407   SideEffects [None]
 408
 409   SeeAlso     [Cudd_Increasing]
 410
 411 ******************************************************************************/
 412 DdNode *
 413 Cudd_Decreasing(
 414   DdManager * dd,
 415   DdNode * f,
 416   int  i)
 417 {
 418     unsigned int topf, level;
 419     DdNode *F, *fv, *fvn, *res;
 420     DD_CTFP cacheOp;
 421
 422     statLine(dd);
 423 #ifdef DD_DEBUG
 424     assert(0 <= i && i < dd->size);
 425 #endif
 426
 427     F = Cudd_Regular(f);
 428     topf = cuddI(dd,F->index);
 429
 430     /* Check terminal case. If topf > i, f does not depend on var.
 431     ** Therefore, f is unate in i.
 432     */
 433     level = (unsigned) dd->perm[i];
 434     if (topf > level) {
 435         return(DD_ONE(dd));
 436     }
 437
 438     /* From now on, f is not constant. */
 439
 440     /* Check cache. */
 441     cacheOp = (DD_CTFP) Cudd_Decreasing;
 442     res = cuddCacheLookup2(dd,cacheOp,f,dd->vars[i]);
 443     if (res != NULL) {
 444         return(res);
 445     }
 446
 447     /* Compute cofactors. */
 448     fv = cuddT(F); fvn = cuddE(F);
 449     if (F != f) {
 450         fv = Cudd_Not(fv);
 451         fvn = Cudd_Not(fvn);
 452     }
 453
 454     if (topf == (unsigned) level) {
 455         /* Special case: if fv is regular, fv(1,...,1) = 1;
 456         ** If in addition fvn is complemented, fvn(1,...,1) = 0.
 457         ** But then f(1,1,...,1) > f(0,1,...,1). Hence f is not
 458         ** monotonic decreasing in i.
 459         */
 460         if (!Cudd_IsComplement(fv) && Cudd_IsComplement(fvn)) {
 461             return(Cudd_Not(DD_ONE(dd)));
 462         }
 463         res = Cudd_bddLeq(dd,fv,fvn) ? DD_ONE(dd) : Cudd_Not(DD_ONE(dd));
 464     } else {
 465         res = Cudd_Decreasing(dd,fv,i);
 466         if (res == DD_ONE(dd)) {
 467             res = Cudd_Decreasing(dd,fvn,i);
 468         }
 469     }
 470
 471     cuddCacheInsert2(dd,cacheOp,f,dd->vars[i],res);
 472     return(res);
 473
 474 } /* end of Cudd_Decreasing */
 475
 476
 477 /**Function********************************************************************
 478
 479   Synopsis    [Determines whether a BDD is positive unate in a
 480   variable.]
 481
 482   Description [Determines whether the function represented by BDD f is
 483   positive unate (monotonic increasing) in variable i. It is based on
 484   Cudd_Decreasing and the fact that f is monotonic increasing in i if
 485   and only if its complement is monotonic decreasing in i.]
 486
 487   SideEffects [None]
 488
 489   SeeAlso     [Cudd_Decreasing]
 490
 491 ******************************************************************************/
 492 DdNode *
 493 Cudd_Increasing(
 494   DdManager * dd,
 495   DdNode * f,
 496   int  i)
 497 {
 498     return(Cudd_Decreasing(dd,Cudd_Not(f),i));
 499
 500 } /* end of Cudd_Increasing */
 501
 502
 503 /**Function********************************************************************
 504
 505   Synopsis    [Tells whether F and G are identical wherever D is 0.]
 506
 507   Description [Tells whether F and G are identical wherever D is 0.  F
 508   and G are either two ADDs or two BDDs.  D is either a 0-1 ADD or a
 509   BDD.  The function returns 1 if F and G are equivalent, and 0
 510   otherwise.  No new nodes are created.]
 511
 512   SideEffects [None]
 513
 514   SeeAlso     [Cudd_bddLeqUnless]
 515
 516 ******************************************************************************/
 517 int
 518 Cudd_EquivDC(
 519   DdManager * dd,
 520   DdNode * F,
 521   DdNode * G,
 522   DdNode * D)
 523 {
 524     DdNode *tmp, *One, *Gr, *Dr;
 525     DdNode *Fv, *Fvn, *Gv, *Gvn, *Dv, *Dvn;
 526     int res;
 527     unsigned int flevel, glevel, dlevel, top;
 528
 529     One = DD_ONE(dd);
 530
 531     statLine(dd);
 532     /* Check terminal cases. */
 533     if (D == One || F == G) return(1);
 534     if (D == Cudd_Not(One) || D == DD_ZERO(dd) || F == Cudd_Not(G)) return(0);
 535
 536     /* From now on, D is non-constant. */
 537
 538     /* Normalize call to increase cache efficiency. */
 539     if (F > G) {
 540         tmp = F;
 541         F = G;
 542         G = tmp;
 543     }
 544     if (Cudd_IsComplement(F)) {
 545         F = Cudd_Not(F);
 546         G = Cudd_Not(G);
 547     }
 548
 549     /* From now on, F is regular. */
 550
 551     /* Check cache. */
 552     tmp = cuddCacheLookup(dd,DD_EQUIV_DC_TAG,F,G,D);
 553     if (tmp != NULL) return(tmp == One);
 554
 555     /* Find splitting variable. */
 556     flevel = cuddI(dd,F->index);
 557     Gr = Cudd_Regular(G);
 558     glevel = cuddI(dd,Gr->index);
 559     top = ddMin(flevel,glevel);
 560     Dr = Cudd_Regular(D);
 561     dlevel = dd->perm[Dr->index];
 562     top = ddMin(top,dlevel);
 563
 564     /* Compute cofactors. */
 565     if (top == flevel) {
 566         Fv = cuddT(F);
 567         Fvn = cuddE(F);
 568     } else {
 569         Fv = Fvn = F;
 570     }
 571     if (top == glevel) {
 572         Gv = cuddT(Gr);
 573         Gvn = cuddE(Gr);
 574         if (G != Gr) {
 575             Gv = Cudd_Not(Gv);
 576             Gvn = Cudd_Not(Gvn);
 577         }
 578     } else {
 579         Gv = Gvn = G;
 580     }
 581     if (top == dlevel) {
 582         Dv = cuddT(Dr);
 583         Dvn = cuddE(Dr);
 584         if (D != Dr) {
 585             Dv = Cudd_Not(Dv);
 586             Dvn = Cudd_Not(Dvn);
 587         }
 588     } else {
 589         Dv = Dvn = D;
 590     }
 591
 592     /* Solve recursively. */
 593     res = Cudd_EquivDC(dd,Fv,Gv,Dv);
 594     if (res != 0) {
 595         res = Cudd_EquivDC(dd,Fvn,Gvn,Dvn);
 596     }
 597     cuddCacheInsert(dd,DD_EQUIV_DC_TAG,F,G,D,(res) ? One : Cudd_Not(One));
 598
 599     return(res);
 600
 601 } /* end of Cudd_EquivDC */
 602
 603
 604 /**Function********************************************************************
 605
 606   Synopsis    [Tells whether f is less than of equal to G unless D is 1.]
 607
 608   Description [Tells whether f is less than of equal to G unless D is
 609   1.  f, g, and D are BDDs.  The function returns 1 if f is less than
 610   of equal to G, and 0 otherwise.  No new nodes are created.]
 611
 612   SideEffects [None]
 613
 614   SeeAlso     [Cudd_EquivDC Cudd_bddLeq Cudd_bddIteConstant]
 615
 616 ******************************************************************************/
 617 int
 618 Cudd_bddLeqUnless(
 619   DdManager *dd,
 620   DdNode *f,
 621   DdNode *g,
 622   DdNode *D)
 623 {
 624     DdNode *tmp, *One, *F, *G;
 625     DdNode *Ft, *Fe, *Gt, *Ge, *Dt, *De;
 626     int res;
 627     unsigned int flevel, glevel, dlevel, top;
 628
 629     statLine(dd);
 630
 631     One = DD_ONE(dd);
 632
 633     /* Check terminal cases. */
 634     if (f == g || g == One || f == Cudd_Not(One) || D == One ||
 635         D == f || D == Cudd_Not(g)) return(1);
 636     /* Check for two-operand cases. */
 637     if (D == Cudd_Not(One) || D == g || D == Cudd_Not(f))
 638         return(Cudd_bddLeq(dd,f,g));
 639     if (g == Cudd_Not(One) || g == Cudd_Not(f)) return(Cudd_bddLeq(dd,f,D));
 640     if (f == One) return(Cudd_bddLeq(dd,Cudd_Not(g),D));
 641
 642     /* From now on, f, g, and D are non-constant, distinct, and
 643     ** non-complementary. */
 644
 645     /* Normalize call to increase cache efficiency.  We rely on the
 646     ** fact that f <= g unless D is equivalent to not(g) <= not(f)
 647     ** unless D and to f <= D unless g.  We make sure that D is
 648     ** regular, and that at most one of f and g is complemented.  We also
 649     ** ensure that when two operands can be swapped, the one with the
 650     ** lowest address comes first. */
 651
 652     if (Cudd_IsComplement(D)) {
 653         if (Cudd_IsComplement(g)) {
 654             /* Special case: if f is regular and g is complemented,
 655             ** f(1,...,1) = 1 > 0 = g(1,...,1).  If D(1,...,1) = 0, return 0.
 656             */
 657             if (!Cudd_IsComplement(f)) return(0);
 658             /* !g <= D unless !f  or  !D <= g unless !f */
 659             tmp = D;
 660             D = Cudd_Not(f);
 661             if (g < tmp) {
 662                 f = Cudd_Not(g);
 663                 g = tmp;
 664             } else {
 665                 f = Cudd_Not(tmp);
 666             }
 667         } else {
 668             if (Cudd_IsComplement(f)) {
 669                 /* !D <= !f unless g  or  !D <= g unless !f */
 670                 tmp = f;
 671                 f = Cudd_Not(D);
 672                 if (tmp < g) {
 673                     D = g;
 674                     g = Cudd_Not(tmp);
 675                 } else {
 676                     D = Cudd_Not(tmp);
 677                 }
 678             } else {
 679                 /* f <= D unless g  or  !D <= !f unless g */
 680                 tmp = D;
 681                 D = g;
 682                 if (tmp < f) {
 683                     g = Cudd_Not(f);
 684                     f = Cudd_Not(tmp);
 685                 } else {
 686                     g = tmp;
 687                 }
 688             }
 689         }
 690     } else {
 691         if (Cudd_IsComplement(g)) {
 692             if (Cudd_IsComplement(f)) {
 693                 /* !g <= !f unless D  or  !g <= D unless !f */
 694                 tmp = f;
 695                 f = Cudd_Not(g);
 696                 if (D < tmp) {
 697                     g = D;
 698                     D = Cudd_Not(tmp);
 699                 } else {
 700                     g = Cudd_Not(tmp);
 701                 }
 702             } else {
 703                 /* f <= g unless D  or  !g <= !f unless D */
 704                 if (g < f) {
 705                     tmp = g;
 706                     g = Cudd_Not(f);
 707                     f = Cudd_Not(tmp);
 708                 }
 709             }
 710         } else {
 711             /* f <= g unless D  or  f <= D unless g */
 712             if (D < g) {
 713                 tmp = D;
 714                 D = g;
 715                 g = tmp;
 716             }
 717         }
 718     }
 719
 720     /* From now on, D is regular. */
 721
 722     /* Check cache. */
 723     tmp = cuddCacheLookup(dd,DD_BDD_LEQ_UNLESS_TAG,f,g,D);
 724     if (tmp != NULL) return(tmp == One);
 725
 726     /* Find splitting variable. */
 727     F = Cudd_Regular(f);
 728     flevel = dd->perm[F->index];
 729     G = Cudd_Regular(g);
 730     glevel = dd->perm[G->index];
 731     top = ddMin(flevel,glevel);
 732     dlevel = dd->perm[D->index];
 733     top = ddMin(top,dlevel);
 734
 735     /* Compute cofactors. */
 736     if (top == flevel) {
 737         Ft = cuddT(F);
 738         Fe = cuddE(F);
 739         if (F != f) {
 740             Ft = Cudd_Not(Ft);
 741             Fe = Cudd_Not(Fe);
 742         }
 743     } else {
 744         Ft = Fe = f;
 745     }
 746     if (top == glevel) {
 747         Gt = cuddT(G);
 748         Ge = cuddE(G);
 749         if (G != g) {
 750             Gt = Cudd_Not(Gt);
 751             Ge = Cudd_Not(Ge);
 752         }
 753     } else {
 754         Gt = Ge = g;
 755     }
 756     if (top == dlevel) {
 757         Dt = cuddT(D);
 758         De = cuddE(D);
 759     } else {
 760         Dt = De = D;
 761     }
 762
 763     /* Solve recursively. */
 764     res = Cudd_bddLeqUnless(dd,Ft,Gt,Dt);
 765     if (res != 0) {
 766         res = Cudd_bddLeqUnless(dd,Fe,Ge,De);
 767     }
 768     cuddCacheInsert(dd,DD_BDD_LEQ_UNLESS_TAG,f,g,D,Cudd_NotCond(One,!res));
 769
 770     return(res);
 771
 772 } /* end of Cudd_bddLeqUnless */
 773
 774
 775 /**Function********************************************************************
 776
 777   Synopsis    [Compares two ADDs for equality within tolerance.]
 778
 779   Description [Compares two ADDs for equality within tolerance. Two
 780   ADDs are reported to be equal if the maximum difference between them
 781   (the sup norm of their difference) is less than or equal to the
 782   tolerance parameter. Returns 1 if the two ADDs are equal (within
 783   tolerance); 0 otherwise. If parameter <code>pr</code> is positive
 784   the first failure is reported to the standard output.]
 785
 786   SideEffects [None]
 787
 788   SeeAlso     []
 789
 790 ******************************************************************************/
 791 int
 792 Cudd_EqualSupNorm(
 793   DdManager * dd /* manager */,
 794   DdNode * f /* first ADD */,
 795   DdNode * g /* second ADD */,
 796   CUDD_VALUE_TYPE  tolerance /* maximum allowed difference */,
 797   int  pr /* verbosity level */)
 798 {
 799     DdNode *fv, *fvn, *gv, *gvn, *r;
 800     unsigned int topf, topg;
 801
 802     statLine(dd);
 803     /* Check terminal cases. */
 804     if (f == g) return(1);
 805     if (Cudd_IsConstant(f) && Cudd_IsConstant(g)) {
 806         if (ddEqualVal(cuddV(f),cuddV(g),tolerance)) {
 807             return(1);
 808         } else {
 809             if (pr>0) {
 810                 (void) fprintf(dd->out,"Offending nodes:\n");
 811                 (void) fprintf(dd->out,
 812                                "f: address = %p\t value = %40.30f\n",
 813                                (void *) f, cuddV(f));
 814                 (void) fprintf(dd->out,
 815                                "g: address = %p\t value = %40.30f\n",
 816                                (void *) g, cuddV(g));
 817             }
 818             return(0);
 819         }
 820     }
 821
 822     /* We only insert the result in the cache if the comparison is
 823     ** successful. Therefore, if we hit we return 1. */
 824     r = cuddCacheLookup2(dd,(DD_CTFP)Cudd_EqualSupNorm,f,g);
 825     if (r != NULL) {
 826         return(1);
 827     }
 828
 829     /* Compute the cofactors and solve the recursive subproblems. */
 830     topf = cuddI(dd,f->index);
 831     topg = cuddI(dd,g->index);
 832
 833     if (topf <= topg) {fv = cuddT(f); fvn = cuddE(f);} else {fv = fvn = f;}
 834     if (topg <= topf) {gv = cuddT(g); gvn = cuddE(g);} else {gv = gvn = g;}
 835
 836     if (!Cudd_EqualSupNorm(dd,fv,gv,tolerance,pr)) return(0);
 837     if (!Cudd_EqualSupNorm(dd,fvn,gvn,tolerance,pr)) return(0);
 838
 839     cuddCacheInsert2(dd,(DD_CTFP)Cudd_EqualSupNorm,f,g,DD_ONE(dd));
 840
 841     return(1);
 842
 843 } /* end of Cudd_EqualSupNorm */
 844
 845
 846 /**Function********************************************************************
 847
 848   Synopsis    [Expands cube to a prime implicant of f.]
 849
 850   Description [Expands cube to a prime implicant of f. Returns the prime
 851   if successful; NULL otherwise.  In particular, NULL is returned if cube
 852   is not a real cube or is not an implicant of f.]
 853
 854   SideEffects [None]
 855
 856   SeeAlso     []
 857
 858 ******************************************************************************/
 859 DdNode *
 860 Cudd_bddMakePrime(
 861   DdManager *dd /* manager */,
 862   DdNode *cube /* cube to be expanded */,
 863   DdNode *f /* function of which the cube is to be made a prime */)
 864 {
 865     DdNode *res;
 866
 867     if (!Cudd_bddLeq(dd,cube,f)) return(NULL);
 868
 869     do {
 870         dd->reordered = 0;
 871         res = cuddBddMakePrime(dd,cube,f);
 872     } while (dd->reordered == 1);
 873     return(res);
 874
 875 } /* end of Cudd_bddMakePrime */
 876
 877
 878 /*---------------------------------------------------------------------------*/
 879 /* Definition of internal functions                                          */
 880 /*---------------------------------------------------------------------------*/
 881
 882
 883 /**Function********************************************************************
 884
 885   Synopsis    [Performs the recursive step of Cudd_bddMakePrime.]
 886
 887   Description [Performs the recursive step of Cudd_bddMakePrime.
 888   Returns the prime if successful; NULL otherwise.]
 889
 890   SideEffects [None]
 891
 892   SeeAlso     []
 893
 894 ******************************************************************************/
 895 DdNode *
 896 cuddBddMakePrime(
 897   DdManager *dd /* manager */,
 898   DdNode *cube /* cube to be expanded */,
 899   DdNode *f /* function of which the cube is to be made a prime */)
 900 {
 901     DdNode *scan;
 902     DdNode *t, *e;
 903     DdNode *res = cube;
 904     DdNode *zero = Cudd_Not(DD_ONE(dd));
 905
 906     Cudd_Ref(res);
 907     scan = cube;
 908     while (!Cudd_IsConstant(scan)) {
 909         DdNode *reg = Cudd_Regular(scan);
 910         DdNode *var = dd->vars[reg->index];
 911         DdNode *expanded = Cudd_bddExistAbstract(dd,res,var);
 912         if (expanded == NULL) {
 913             return(NULL);
 914         }
 915         Cudd_Ref(expanded);
 916         if (Cudd_bddLeq(dd,expanded,f)) {
 917             Cudd_RecursiveDeref(dd,res);
 918             res = expanded;
 919         } else {
 920             Cudd_RecursiveDeref(dd,expanded);
 921         }
 922         cuddGetBranches(scan,&t,&e);
 923         if (t == zero) {
 924             scan = e;
 925         } else if (e == zero) {
 926             scan = t;
 927         } else {
 928             Cudd_RecursiveDeref(dd,res);
 929             return(NULL);       /* cube is not a cube */
 930         }
 931     }
 932
 933     if (scan == DD_ONE(dd)) {
 934         Cudd_Deref(res);
 935         return(res);
 936     } else {
 937         Cudd_RecursiveDeref(dd,res);
 938         return(NULL);
 939     }
 940
 941 } /* end of cuddBddMakePrime */
 942
 943
 944 /*---------------------------------------------------------------------------*/
 945 /* Definition of static functions                                            */
 946 /*---------------------------------------------------------------------------*/
 947
 948
 949 /**Function********************************************************************
 950
 951   Synopsis    [Frees the entries of the visited symbol table.]
 952
 953   Description [Frees the entries of the visited symbol table. Returns
 954   ST_CONTINUE.]
 955
 956   SideEffects [None]
 957
 958 ******************************************************************************/
 959 static enum st_retval
 960 freePathPair(
 961   char * key,
 962   char * value,
 963   char * arg)
 964 {
 965     cuddPathPair *pair;
 966
 967     pair = (cuddPathPair *) value;
 968         FREE(pair);
 969     return(ST_CONTINUE);
 970
 971 } /* end of freePathPair */
 972
 973
 974 /**Function********************************************************************
 975
 976   Synopsis    [Finds the length of the shortest path(s) in a DD.]
 977
 978   Description [Finds the length of the shortest path(s) in a DD.
 979   Uses a local symbol table to store the lengths for each
 980   node. Only the lengths for the regular nodes are entered in the table,
 981   because those for the complement nodes are simply obtained by swapping
 982   the two lenghts.
 983   Returns a pair of lengths: the length of the shortest path to 1;
 984   and the length of the shortest path to 0. This is done so as to take
 985   complement arcs into account.]
 986
 987   SideEffects [Accumulates the support of the DD in support.]
 988
 989   SeeAlso     []
 990
 991 ******************************************************************************/
 992 static cuddPathPair
 993 getShortest(
 994   DdNode * root,
 995   int * cost,
 996   int * support,
 997   st_table * visited)
 998 {
 999     cuddPathPair *my_pair, res_pair, pair_T, pair_E;
1000     DdNode      *my_root, *T, *E;
1001     int         weight;
1002
1003     my_root = Cudd_Regular(root);
1004
1005     if (st_lookup(visited, my_root, &my_pair)) {
1006         if (Cudd_IsComplement(root)) {
1007             res_pair.pos = my_pair->neg;
1008             res_pair.neg = my_pair->pos;
1009         } else {
1010             res_pair.pos = my_pair->pos;
1011             res_pair.neg = my_pair->neg;
1012         }
1013         return(res_pair);
1014     }
1015
1016     /* In the case of a BDD the following test is equivalent to
1017     ** testing whether the BDD is the constant 1. This formulation,
1018     ** however, works for ADDs as well, by assuming the usual
1019     ** dichotomy of 0 and != 0.
1020     */
1021     if (cuddIsConstant(my_root)) {
1022         if (my_root != zero) {
1023             res_pair.pos = 0;
1024             res_pair.neg = DD_BIGGY;
1025         } else {
1026             res_pair.pos = DD_BIGGY;
1027             res_pair.neg = 0;
1028         }
1029     } else {
1030         T = cuddT(my_root);
1031         E = cuddE(my_root);
1032
1033         pair_T = getShortest(T, cost, support, visited);
1034         pair_E = getShortest(E, cost, support, visited);
1035         weight = WEIGHT(cost, my_root->index);
1036         res_pair.pos = ddMin(pair_T.pos+weight, pair_E.pos);
1037         res_pair.neg = ddMin(pair_T.neg+weight, pair_E.neg);
1038
1039         /* Update support. */
1040         if (support != NULL) {
1041             support[my_root->index] = 1;
1042         }
1043     }
1044
1045     my_pair = ALLOC(cuddPathPair, 1);
1046     if (my_pair == NULL) {
1047         if (Cudd_IsComplement(root)) {
1048             int tmp = res_pair.pos;
1049             res_pair.pos = res_pair.neg;
1050             res_pair.neg = tmp;
1051         }
1052         return(res_pair);
1053     }
1054     my_pair->pos = res_pair.pos;
1055     my_pair->neg = res_pair.neg;
1056
1057     st_insert(visited, (char *)my_root, (char *)my_pair);
1058     if (Cudd_IsComplement(root)) {
1059         res_pair.pos = my_pair->neg;
1060         res_pair.neg = my_pair->pos;
1061     } else {
1062         res_pair.pos = my_pair->pos;
1063         res_pair.neg = my_pair->neg;
1064     }
1065     return(res_pair);
1066
1067 } /* end of getShortest */
1068
1069
1070 /**Function********************************************************************
1071
1072   Synopsis    [Build a BDD for a shortest path of f.]
1073
1074   Description [Build a BDD for a shortest path of f.
1075   Given the minimum length from the root, and the minimum
1076   lengths for each node (in visited), apply triangulation at each node.
1077   Of the two children of each node on a shortest path, at least one is
1078   on a shortest path. In case of ties the procedure chooses the THEN
1079   children.
1080   Returns a pointer to the cube BDD representing the path if
1081   successful; NULL otherwise.]
1082
1083   SideEffects [None]
1084
1085   SeeAlso     []
1086
1087 ******************************************************************************/
1088 static DdNode *
1089 getPath(
1090   DdManager * manager,
1091   st_table * visited,
1092   DdNode * f,
1093   int * weight,
1094   int  cost)
1095 {
1096     DdNode      *sol, *tmp;
1097     DdNode      *my_dd, *T, *E;
1098     cuddPathPair *T_pair, *E_pair;
1099     int         Tcost, Ecost;
1100     int         complement;
1101
1102     my_dd = Cudd_Regular(f);
1103     complement = Cudd_IsComplement(f);
1104
1105     sol = one;
1106     cuddRef(sol);
1107
1108     while (!cuddIsConstant(my_dd)) {
1109         Tcost = cost - WEIGHT(weight, my_dd->index);
1110         Ecost = cost;
1111
1112         T = cuddT(my_dd);
1113         E = cuddE(my_dd);
1114
1115         if (complement) {T = Cudd_Not(T); E = Cudd_Not(E);}
1116
1117         st_lookup(visited, Cudd_Regular(T), &T_pair);
1118         if ((Cudd_IsComplement(T) && T_pair->neg == Tcost) ||
1119         (!Cudd_IsComplement(T) && T_pair->pos == Tcost)) {
1120             tmp = cuddBddAndRecur(manager,manager->vars[my_dd->index],sol);
1121             if (tmp == NULL) {
1122                 Cudd_RecursiveDeref(manager,sol);
1123                 return(NULL);
1124             }
1125             cuddRef(tmp);
1126             Cudd_RecursiveDeref(manager,sol);
1127             sol = tmp;
1128
1129             complement =  Cudd_IsComplement(T);
1130             my_dd = Cudd_Regular(T);
1131             cost = Tcost;
1132             continue;
1133         }
1134         st_lookup(visited, Cudd_Regular(E), &E_pair);
1135         if ((Cudd_IsComplement(E) && E_pair->neg == Ecost) ||
1136         (!Cudd_IsComplement(E) && E_pair->pos == Ecost)) {
1137             tmp = cuddBddAndRecur(manager,Cudd_Not(manager->vars[my_dd->index]),sol);
1138             if (tmp == NULL) {
1139                 Cudd_RecursiveDeref(manager,sol);
1140                 return(NULL);
1141             }
1142             cuddRef(tmp);
1143             Cudd_RecursiveDeref(manager,sol);
1144             sol = tmp;
1145             complement = Cudd_IsComplement(E);
1146             my_dd = Cudd_Regular(E);
1147             cost = Ecost;
1148             continue;
1149         }
1150         (void) fprintf(manager->err,"We shouldn't be here!!\n");
1151         manager->errorCode = CUDD_INTERNAL_ERROR;
1152         return(NULL);
1153     }
1154
1155     cuddDeref(sol);
1156     return(sol);
1157
1158 } /* end of getPath */
1159
1160
1161 /**Function********************************************************************
1162
1163   Synopsis    [Finds the size of the largest cube(s) in a DD.]
1164
1165   Description [Finds the size of the largest cube(s) in a DD.
1166   This problem is translated into finding the shortest paths from a node
1167   when both THEN and ELSE arcs have unit lengths.
1168   Uses a local symbol table to store the lengths for each
1169   node. Only the lengths for the regular nodes are entered in the table,
1170   because those for the complement nodes are simply obtained by swapping
1171   the two lenghts.
1172   Returns a pair of lengths: the length of the shortest path to 1;
1173   and the length of the shortest path to 0. This is done so as to take
1174   complement arcs into account.]
1175
1176   SideEffects [none]
1177
1178   SeeAlso     []
1179
1180 ******************************************************************************/
1181 static cuddPathPair
1182 getLargest(
1183   DdNode * root,
1184   st_table * visited)
1185 {
1186     cuddPathPair *my_pair, res_pair, pair_T, pair_E;
1187     DdNode      *my_root, *T, *E;
1188
1189     my_root = Cudd_Regular(root);
1190
1191     if (st_lookup(visited, my_root, &my_pair)) {
1192         if (Cudd_IsComplement(root)) {
1193             res_pair.pos = my_pair->neg;
1194             res_pair.neg = my_pair->pos;
1195         } else {
1196             res_pair.pos = my_pair->pos;
1197             res_pair.neg = my_pair->neg;
1198         }
1199         return(res_pair);
1200     }
1201
1202     /* In the case of a BDD the following test is equivalent to
1203     ** testing whether the BDD is the constant 1. This formulation,
1204     ** however, works for ADDs as well, by assuming the usual
1205     ** dichotomy of 0 and != 0.
1206     */
1207     if (cuddIsConstant(my_root)) {
1208         if (my_root != zero) {
1209             res_pair.pos = 0;
1210             res_pair.neg = DD_BIGGY;
1211         } else {
1212             res_pair.pos = DD_BIGGY;
1213             res_pair.neg = 0;
1214         }
1215     } else {
1216         T = cuddT(my_root);
1217         E = cuddE(my_root);
1218
1219         pair_T = getLargest(T, visited);
1220         pair_E = getLargest(E, visited);
1221         res_pair.pos = ddMin(pair_T.pos, pair_E.pos) + 1;
1222         res_pair.neg = ddMin(pair_T.neg, pair_E.neg) + 1;
1223     }
1224
1225     my_pair = ALLOC(cuddPathPair, 1);
1226     if (my_pair == NULL) {      /* simply do not cache this result */
1227         if (Cudd_IsComplement(root)) {
1228             int tmp = res_pair.pos;
1229             res_pair.pos = res_pair.neg;
1230             res_pair.neg = tmp;
1231         }
1232         return(res_pair);
1233     }
1234     my_pair->pos = res_pair.pos;
1235     my_pair->neg = res_pair.neg;
1236
1237     /* Caching may fail without affecting correctness. */
1238     st_insert(visited, (char *)my_root, (char *)my_pair);
1239     if (Cudd_IsComplement(root)) {
1240         res_pair.pos = my_pair->neg;
1241         res_pair.neg = my_pair->pos;
1242     } else {
1243         res_pair.pos = my_pair->pos;
1244         res_pair.neg = my_pair->neg;
1245     }
1246     return(res_pair);
1247
1248 } /* end of getLargest */
1249
1250
1251 /**Function********************************************************************
1252
1253   Synopsis    [Build a BDD for a largest cube of f.]
1254
1255   Description [Build a BDD for a largest cube of f.
1256   Given the minimum length from the root, and the minimum
1257   lengths for each node (in visited), apply triangulation at each node.
1258   Of the two children of each node on a shortest path, at least one is
1259   on a shortest path. In case of ties the procedure chooses the THEN
1260   children.
1261   Returns a pointer to the cube BDD representing the path if
1262   successful; NULL otherwise.]
1263
1264   SideEffects [None]
1265
1266   SeeAlso     []
1267
1268 ******************************************************************************/
1269 static DdNode *
1270 getCube(
1271   DdManager * manager,
1272   st_table * visited,
1273   DdNode * f,
1274   int  cost)
1275 {
1276     DdNode      *sol, *tmp;
1277     DdNode      *my_dd, *T, *E;
1278     cuddPathPair *T_pair, *E_pair;
1279     int         Tcost, Ecost;
1280     int         complement;
1281
1282     my_dd = Cudd_Regular(f);
1283     complement = Cudd_IsComplement(f);
1284
1285     sol = one;
1286     cuddRef(sol);
1287
1288     while (!cuddIsConstant(my_dd)) {
1289         Tcost = cost - 1;
1290         Ecost = cost - 1;
1291
1292         T = cuddT(my_dd);
1293         E = cuddE(my_dd);
1294
1295         if (complement) {T = Cudd_Not(T); E = Cudd_Not(E);}
1296
1297         if (!st_lookup(visited, Cudd_Regular(T), &T_pair)) return(NULL);
1298         if ((Cudd_IsComplement(T) && T_pair->neg == Tcost) ||
1299         (!Cudd_IsComplement(T) && T_pair->pos == Tcost)) {
1300             tmp = cuddBddAndRecur(manager,manager->vars[my_dd->index],sol);
1301             if (tmp == NULL) {
1302                 Cudd_RecursiveDeref(manager,sol);
1303                 return(NULL);
1304             }
1305             cuddRef(tmp);
1306             Cudd_RecursiveDeref(manager,sol);
1307             sol = tmp;
1308
1309             complement =  Cudd_IsComplement(T);
1310             my_dd = Cudd_Regular(T);
1311             cost = Tcost;
1312             continue;
1313         }
1314         if (!st_lookup(visited, Cudd_Regular(E), &E_pair)) return(NULL);
1315         if ((Cudd_IsComplement(E) && E_pair->neg == Ecost) ||
1316         (!Cudd_IsComplement(E) && E_pair->pos == Ecost)) {
1317             tmp = cuddBddAndRecur(manager,Cudd_Not(manager->vars[my_dd->index]),sol);
1318             if (tmp == NULL) {
1319                 Cudd_RecursiveDeref(manager,sol);
1320                 return(NULL);
1321             }
1322             cuddRef(tmp);
1323             Cudd_RecursiveDeref(manager,sol);
1324             sol = tmp;
1325             complement = Cudd_IsComplement(E);
1326             my_dd = Cudd_Regular(E);
1327             cost = Ecost;
1328             continue;
1329         }
1330         (void) fprintf(manager->err,"We shouldn't be here!\n");
1331         manager->errorCode = CUDD_INTERNAL_ERROR;
1332         return(NULL);
1333     }
1334
1335     cuddDeref(sol);
1336     return(sol);
1337
1338 } /* end of getCube */