distr/cudd/cuddSplit.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddSplit.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Returns a subset of minterms from a boolean function.]
   8
   9   Description [External functions included in this modoule:
  10                 <ul>
  11                 <li> Cudd_SplitSet()
  12                 </ul>
  13         Internal functions included in this module:
  14                 <ul>
  15                 <li> cuddSplitSetRecur()
  16                 </u>
  17         Static functions included in this module:
  18                 <ul>
  19                 <li> selectMintermsFromUniverse()
  20                 <li> mintermsFromUniverse()
  21                 <li> bddAnnotateMintermCount()
  22                 </ul> ]
  23
  24   SeeAlso     []
  25
  26   Author      [Balakrishna Kumthekar]
  27
  28   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  29
  30   All rights reserved.
  31
  32   Redistribution and use in source and binary forms, with or without
  33   modification, are permitted provided that the following conditions
  34   are met:
  35
  36   Redistributions of source code must retain the above copyright
  37   notice, this list of conditions and the following disclaimer.
  38
  39   Redistributions in binary form must reproduce the above copyright
  40   notice, this list of conditions and the following disclaimer in the
  41   documentation and/or other materials provided with the distribution.
  42
  43   Neither the name of the University of Colorado nor the names of its
  44   contributors may be used to endorse or promote products derived from
  45   this software without specific prior written permission.
  46
  47   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  48   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  49   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  50   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  51   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  52   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  53   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  54   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  55   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  56   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  57   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  58   POSSIBILITY OF SUCH DAMAGE.]
  59
  60 ******************************************************************************/
  61
  62 #include "util.h"
  63 #include "cuddInt.h"
  64
  65 /*---------------------------------------------------------------------------*/
  66 /* Constant declarations                                                     */
  67 /*---------------------------------------------------------------------------*/
  68
  69 /*---------------------------------------------------------------------------*/
  70 /* Type declarations                                                         */
  71 /*---------------------------------------------------------------------------*/
  72
  73
  74 /*---------------------------------------------------------------------------*/
  75 /* Structure declarations                                                    */
  76 /*---------------------------------------------------------------------------*/
  77
  78
  79 /*---------------------------------------------------------------------------*/
  80 /* Variable declarations                                                     */
  81 /*---------------------------------------------------------------------------*/
  82
  83
  84 /*---------------------------------------------------------------------------*/
  85 /* Macro declarations                                                        */
  86 /*---------------------------------------------------------------------------*/
  87
  88
  89 /**AutomaticStart*************************************************************/
  90
  91 /*---------------------------------------------------------------------------*/
  92 /* Static function prototypes                                                */
  93 /*---------------------------------------------------------------------------*/
  94
  95 static DdNode * selectMintermsFromUniverse (DdManager *manager, int *varSeen, double n);
  96 static DdNode * mintermsFromUniverse (DdManager *manager, DdNode **vars, int numVars, double n, int index);
  97 static double bddAnnotateMintermCount (DdManager *manager, DdNode *node, double max, st_table *table);
  98
  99 /**AutomaticEnd***************************************************************/
 100
 101
 102 /*---------------------------------------------------------------------------*/
 103 /* Definition of exported functions                                          */
 104 /*---------------------------------------------------------------------------*/
 105
 106
 107 /**Function********************************************************************
 108
 109   Synopsis    [Returns m minterms from a BDD.]
 110
 111   Description [Returns <code>m</code> minterms from a BDD whose
 112   support has <code>n</code> variables at most.  The procedure tries
 113   to create as few extra nodes as possible. The function represented
 114   by <code>S</code> depends on at most <code>n</code> of the variables
 115   in <code>xVars</code>. Returns a BDD with <code>m</code> minterms
 116   of the on-set of S if successful; NULL otherwise.]
 117
 118   SideEffects [None]
 119
 120   SeeAlso     []
 121
 122 ******************************************************************************/
 123 DdNode *
 124 Cudd_SplitSet(
 125   DdManager * manager,
 126   DdNode * S,
 127   DdNode ** xVars,
 128   int  n,
 129   double  m)
 130 {
 131     DdNode *result;
 132     DdNode *zero, *one;
 133     double  max, num;
 134     st_table *mtable;
 135     int *varSeen;
 136     int i,index, size;
 137
 138     size = manager->size;
 139     one = DD_ONE(manager);
 140     zero = Cudd_Not(one);
 141
 142     /* Trivial cases. */
 143     if (m == 0.0) {
 144         return(zero);
 145     }
 146     if (S == zero) {
 147         return(NULL);
 148     }
 149
 150     max = pow(2.0,(double)n);
 151     if (m > max)
 152         return(NULL);
 153
 154     do {
 155         manager->reordered = 0;
 156         /* varSeen is used to mark the variables that are encountered
 157         ** while traversing the BDD S.
 158         */
 159         varSeen = ALLOC(int, size);
 160         if (varSeen == NULL) {
 161             manager->errorCode = CUDD_MEMORY_OUT;
 162             return(NULL);
 163         }
 164         for (i = 0; i < size; i++) {
 165             varSeen[i] = -1;
 166         }
 167         for (i = 0; i < n; i++) {
 168             index = (xVars[i])->index;
 169             varSeen[manager->invperm[index]] = 0;
 170         }
 171
 172         if (S == one) {
 173             if (m == max) {
 174                 FREE(varSeen);
 175                 return(S);
 176             }
 177             result = selectMintermsFromUniverse(manager,varSeen,m);
 178             if (result)
 179                 cuddRef(result);
 180             FREE(varSeen);
 181         } else {
 182             mtable = st_init_table(st_ptrcmp,st_ptrhash);
 183             if (mtable == NULL) {
 184                 (void) fprintf(manager->out,
 185                                "Cudd_SplitSet: out-of-memory.\n");
 186                 FREE(varSeen);
 187                 manager->errorCode = CUDD_MEMORY_OUT;
 188                 return(NULL);
 189             }
 190             /* The nodes of BDD S are annotated by the number of minterms
 191             ** in their onset. The node and the number of minterms in its
 192             ** onset are stored in mtable.
 193             */
 194             num = bddAnnotateMintermCount(manager,S,max,mtable);
 195             if (m == num) {
 196                 st_foreach(mtable,cuddStCountfree,NIL(char));
 197                 st_free_table(mtable);
 198                 FREE(varSeen);
 199                 return(S);
 200             }
 201
 202             result = cuddSplitSetRecur(manager,mtable,varSeen,S,m,max,0);
 203             if (result)
 204                 cuddRef(result);
 205             st_foreach(mtable,cuddStCountfree,NULL);
 206             st_free_table(mtable);
 207             FREE(varSeen);
 208         }
 209     } while (manager->reordered == 1);
 210
 211     cuddDeref(result);
 212     return(result);
 213
 214 } /* end of Cudd_SplitSet */
 215
 216
 217 /*---------------------------------------------------------------------------*/
 218 /* Definition of internal functions                                          */
 219 /*---------------------------------------------------------------------------*/
 220
 221 /**Function********************************************************************
 222
 223   Synopsis    [Implements the recursive step of Cudd_SplitSet.]
 224
 225   Description [Implements the recursive step of Cudd_SplitSet. The
 226   procedure recursively traverses the BDD and checks to see if any
 227   node satisfies the minterm requirements as specified by 'n'. At any
 228   node X, n is compared to the number of minterms in the onset of X's
 229   children. If either of the child nodes have exactly n minterms, then
 230   that node is returned; else, if n is greater than the onset of one
 231   of the child nodes, that node is retained and the difference in the
 232   number of minterms is extracted from the other child. In case n
 233   minterms can be extracted from constant 1, the algorithm returns the
 234   result with at most log(n) nodes.]
 235
 236   SideEffects [The array 'varSeen' is updated at every recursive call
 237   to set the variables traversed by the procedure.]
 238
 239   SeeAlso     []
 240
 241 ******************************************************************************/
 242 DdNode*
 243 cuddSplitSetRecur(
 244   DdManager * manager,
 245   st_table * mtable,
 246   int * varSeen,
 247   DdNode * p,
 248   double  n,
 249   double  max,
 250   int  index)
 251 {
 252     DdNode *one, *zero, *N, *Nv;
 253     DdNode *Nnv, *q, *r, *v;
 254     DdNode *result;
 255     double *dummy, numT, numE;
 256     int variable, positive;
 257
 258     statLine(manager);
 259     one = DD_ONE(manager);
 260     zero = Cudd_Not(one);
 261
 262     /* If p is constant, extract n minterms from constant 1.  The procedure by
 263     ** construction guarantees that minterms will not be extracted from
 264     ** constant 0.
 265     */
 266     if (Cudd_IsConstant(p)) {
 267         q = selectMintermsFromUniverse(manager,varSeen,n);
 268         return(q);
 269     }
 270
 271     N = Cudd_Regular(p);
 272
 273     /* Set variable as seen. */
 274     variable = N->index;
 275     varSeen[manager->invperm[variable]] = -1;
 276
 277     Nv = cuddT(N);
 278     Nnv = cuddE(N);
 279     if (Cudd_IsComplement(p)) {
 280         Nv = Cudd_Not(Nv);
 281         Nnv = Cudd_Not(Nnv);
 282     }
 283
 284     /* If both the children of 'p' are constants, extract n minterms from a
 285     ** constant node.
 286     */
 287     if (Cudd_IsConstant(Nv) && Cudd_IsConstant(Nnv)) {
 288         q = selectMintermsFromUniverse(manager,varSeen,n);
 289         if (q == NULL) {
 290             return(NULL);
 291         }
 292         cuddRef(q);
 293         r = cuddBddAndRecur(manager,p,q);
 294         if (r == NULL) {
 295             Cudd_RecursiveDeref(manager,q);
 296             return(NULL);
 297         }
 298         cuddRef(r);
 299         Cudd_RecursiveDeref(manager,q);
 300         cuddDeref(r);
 301         return(r);
 302     }
 303
 304     /* Lookup the # of minterms in the onset of the node from the table. */
 305     if (!Cudd_IsConstant(Nv)) {
 306         if (!st_lookup(mtable, Nv, &dummy)) return(NULL);
 307         numT = *dummy/(2*(1<<index));
 308     } else if (Nv == one) {
 309         numT = max/(2*(1<<index));
 310     } else {
 311         numT = 0;
 312     }
 313
 314     if (!Cudd_IsConstant(Nnv)) {
 315         if (!st_lookup(mtable, Nnv, &dummy)) return(NULL);
 316         numE = *dummy/(2*(1<<index));
 317     } else if (Nnv == one) {
 318         numE = max/(2*(1<<index));
 319     } else {
 320         numE = 0;
 321     }
 322
 323     v = cuddUniqueInter(manager,variable,one,zero);
 324     cuddRef(v);
 325
 326     /* If perfect match. */
 327     if (numT == n) {
 328         q = cuddBddAndRecur(manager,v,Nv);
 329         if (q == NULL) {
 330             Cudd_RecursiveDeref(manager,v);
 331             return(NULL);
 332         }
 333         cuddRef(q);
 334         Cudd_RecursiveDeref(manager,v);
 335         cuddDeref(q);
 336         return(q);
 337     }
 338     if (numE == n) {
 339         q = cuddBddAndRecur(manager,Cudd_Not(v),Nnv);
 340         if (q == NULL) {
 341             Cudd_RecursiveDeref(manager,v);
 342             return(NULL);
 343         }
 344         cuddRef(q);
 345         Cudd_RecursiveDeref(manager,v);
 346         cuddDeref(q);
 347         return(q);
 348     }
 349     /* If n is greater than numT, extract the difference from the ELSE child
 350     ** and retain the function represented by the THEN branch.
 351     */
 352     if (numT < n) {
 353         q = cuddSplitSetRecur(manager,mtable,varSeen,
 354                               Nnv,(n-numT),max,index+1);
 355         if (q == NULL) {
 356             Cudd_RecursiveDeref(manager,v);
 357             return(NULL);
 358         }
 359         cuddRef(q);
 360         r = cuddBddIteRecur(manager,v,Nv,q);
 361         if (r == NULL) {
 362             Cudd_RecursiveDeref(manager,q);
 363             Cudd_RecursiveDeref(manager,v);
 364             return(NULL);
 365         }
 366         cuddRef(r);
 367         Cudd_RecursiveDeref(manager,q);
 368         Cudd_RecursiveDeref(manager,v);
 369         cuddDeref(r);
 370         return(r);
 371     }
 372     /* If n is greater than numE, extract the difference from the THEN child
 373     ** and retain the function represented by the ELSE branch.
 374     */
 375     if (numE < n) {
 376         q = cuddSplitSetRecur(manager,mtable,varSeen,
 377                               Nv, (n-numE),max,index+1);
 378         if (q == NULL) {
 379             Cudd_RecursiveDeref(manager,v);
 380             return(NULL);
 381         }
 382         cuddRef(q);
 383         r = cuddBddIteRecur(manager,v,q,Nnv);
 384         if (r == NULL) {
 385             Cudd_RecursiveDeref(manager,q);
 386             Cudd_RecursiveDeref(manager,v);
 387             return(NULL);
 388         }
 389         cuddRef(r);
 390         Cudd_RecursiveDeref(manager,q);
 391         Cudd_RecursiveDeref(manager,v);
 392         cuddDeref(r);
 393         return(r);
 394     }
 395
 396     /* None of the above cases; (n < numT and n < numE) and either of
 397     ** the Nv, Nnv or both are not constants. If possible extract the
 398     ** required minterms the constant branch.
 399     */
 400     if (Cudd_IsConstant(Nv) && !Cudd_IsConstant(Nnv)) {
 401         q = selectMintermsFromUniverse(manager,varSeen,n);
 402         if (q == NULL) {
 403             Cudd_RecursiveDeref(manager,v);
 404             return(NULL);
 405         }
 406         cuddRef(q);
 407         result = cuddBddAndRecur(manager,v,q);
 408         if (result == NULL) {
 409             Cudd_RecursiveDeref(manager,q);
 410             Cudd_RecursiveDeref(manager,v);
 411             return(NULL);
 412         }
 413         cuddRef(result);
 414         Cudd_RecursiveDeref(manager,q);
 415         Cudd_RecursiveDeref(manager,v);
 416         cuddDeref(result);
 417         return(result);
 418     } else if (!Cudd_IsConstant(Nv) && Cudd_IsConstant(Nnv)) {
 419         q = selectMintermsFromUniverse(manager,varSeen,n);
 420         if (q == NULL) {
 421             Cudd_RecursiveDeref(manager,v);
 422             return(NULL);
 423         }
 424         cuddRef(q);
 425         result = cuddBddAndRecur(manager,Cudd_Not(v),q);
 426         if (result == NULL) {
 427             Cudd_RecursiveDeref(manager,q);
 428             Cudd_RecursiveDeref(manager,v);
 429             return(NULL);
 430         }
 431         cuddRef(result);
 432         Cudd_RecursiveDeref(manager,q);
 433         Cudd_RecursiveDeref(manager,v);
 434         cuddDeref(result);
 435         return(result);
 436     }
 437
 438     /* Both Nv and Nnv are not constants. So choose the one which
 439     ** has fewer minterms in its onset.
 440     */
 441     positive = 0;
 442     if (numT < numE) {
 443         q = cuddSplitSetRecur(manager,mtable,varSeen,
 444                               Nv,n,max,index+1);
 445         positive = 1;
 446     } else {
 447         q = cuddSplitSetRecur(manager,mtable,varSeen,
 448                               Nnv,n,max,index+1);
 449     }
 450
 451     if (q == NULL) {
 452         Cudd_RecursiveDeref(manager,v);
 453         return(NULL);
 454     }
 455     cuddRef(q);
 456
 457     if (positive) {
 458         result = cuddBddAndRecur(manager,v,q);
 459     } else {
 460         result = cuddBddAndRecur(manager,Cudd_Not(v),q);
 461     }
 462     if (result == NULL) {
 463         Cudd_RecursiveDeref(manager,q);
 464         Cudd_RecursiveDeref(manager,v);
 465         return(NULL);
 466     }
 467     cuddRef(result);
 468     Cudd_RecursiveDeref(manager,q);
 469     Cudd_RecursiveDeref(manager,v);
 470     cuddDeref(result);
 471
 472     return(result);
 473
 474 } /* end of cuddSplitSetRecur */
 475
 476
 477 /*---------------------------------------------------------------------------*/
 478 /* Definition of static functions                                            */
 479 /*---------------------------------------------------------------------------*/
 480
 481 /**Function********************************************************************
 482
 483   Synopsis [This function prepares an array of variables which have not been
 484   encountered so far when traversing the procedure cuddSplitSetRecur.]
 485
 486   Description [This function prepares an array of variables which have not been
 487   encountered so far when traversing the procedure cuddSplitSetRecur. This
 488   array is then used to extract the required number of minterms from a constant
 489   1. The algorithm guarantees that the size of BDD will be utmost \log(n).]
 490
 491   SideEffects [None]
 492
 493 ******************************************************************************/
 494 static DdNode *
 495 selectMintermsFromUniverse(
 496   DdManager * manager,
 497   int * varSeen,
 498   double  n)
 499 {
 500     int numVars;
 501     int i, size, j;
 502      DdNode *one, *zero, *result;
 503     DdNode **vars;
 504
 505     numVars = 0;
 506     size = manager->size;
 507     one = DD_ONE(manager);
 508     zero = Cudd_Not(one);
 509
 510     /* Count the number of variables not encountered so far in procedure
 511     ** cuddSplitSetRecur.
 512     */
 513     for (i = size-1; i >= 0; i--) {
 514         if(varSeen[i] == 0)
 515             numVars++;
 516     }
 517     vars = ALLOC(DdNode *, numVars);
 518     if (!vars) {
 519         manager->errorCode = CUDD_MEMORY_OUT;
 520         return(NULL);
 521     }
 522
 523     j = 0;
 524     for (i = size-1; i >= 0; i--) {
 525         if(varSeen[i] == 0) {
 526             vars[j] = cuddUniqueInter(manager,manager->perm[i],one,zero);
 527             cuddRef(vars[j]);
 528             j++;
 529         }
 530     }
 531
 532     /* Compute a function which has n minterms and depends on at most
 533     ** numVars variables.
 534     */
 535     result = mintermsFromUniverse(manager,vars,numVars,n, 0);
 536     if (result)
 537         cuddRef(result);
 538
 539     for (i = 0; i < numVars; i++)
 540         Cudd_RecursiveDeref(manager,vars[i]);
 541     FREE(vars);
 542
 543     return(result);
 544
 545 } /* end of selectMintermsFromUniverse */
 546
 547
 548 /**Function********************************************************************
 549
 550   Synopsis    [Recursive procedure to extract n mintems from constant 1.]
 551
 552   Description [Recursive procedure to extract n mintems from constant 1.]
 553
 554   SideEffects [None]
 555
 556 ******************************************************************************/
 557 static DdNode *
 558 mintermsFromUniverse(
 559   DdManager * manager,
 560   DdNode ** vars,
 561   int  numVars,
 562   double  n,
 563   int  index)
 564 {
 565     DdNode *one, *zero;
 566     DdNode *q, *result;
 567     double max, max2;
 568
 569     statLine(manager);
 570     one = DD_ONE(manager);
 571     zero = Cudd_Not(one);
 572
 573     max = pow(2.0, (double)numVars);
 574     max2 = max / 2.0;
 575
 576     if (n == max)
 577         return(one);
 578     if (n == 0.0)
 579         return(zero);
 580     /* if n == 2^(numVars-1), return a single variable */
 581     if (n == max2)
 582         return vars[index];
 583     else if (n > max2) {
 584         /* When n > 2^(numVars-1), a single variable vars[index]
 585         ** contains 2^(numVars-1) minterms. The rest are extracted
 586         ** from a constant with 1 less variable.
 587         */
 588         q = mintermsFromUniverse(manager,vars,numVars-1,(n-max2),index+1);
 589         if (q == NULL)
 590             return(NULL);
 591         cuddRef(q);
 592         result = cuddBddIteRecur(manager,vars[index],one,q);
 593     } else {
 594         /* When n < 2^(numVars-1), a literal of variable vars[index]
 595         ** is selected. The required n minterms are extracted from a
 596         ** constant with 1 less variable.
 597         */
 598         q = mintermsFromUniverse(manager,vars,numVars-1,n,index+1);
 599         if (q == NULL)
 600             return(NULL);
 601         cuddRef(q);
 602         result = cuddBddAndRecur(manager,vars[index],q);
 603     }
 604
 605     if (result == NULL) {
 606         Cudd_RecursiveDeref(manager,q);
 607         return(NULL);
 608     }
 609     cuddRef(result);
 610     Cudd_RecursiveDeref(manager,q);
 611     cuddDeref(result);
 612     return(result);
 613
 614 } /* end of mintermsFromUniverse */
 615
 616
 617 /**Function********************************************************************
 618
 619   Synopsis    [Annotates every node in the BDD node with its minterm count.]
 620
 621   Description [Annotates every node in the BDD node with its minterm count.
 622   In this function, every node and the minterm count represented by it are
 623   stored in a hash table.]
 624
 625   SideEffects [Fills up 'table' with the pair <node,minterm_count>.]
 626
 627 ******************************************************************************/
 628 static double
 629 bddAnnotateMintermCount(
 630   DdManager * manager,
 631   DdNode * node,
 632   double  max,
 633   st_table * table)
 634 {
 635
 636     DdNode *N,*Nv,*Nnv;
 637     register double min_v,min_nv;
 638     register double min_N;
 639     double *pmin;
 640     double *dummy;
 641
 642     statLine(manager);
 643     N = Cudd_Regular(node);
 644     if (cuddIsConstant(N)) {
 645         if (node == DD_ONE(manager)) {
 646             return(max);
 647         } else {
 648             return(0.0);
 649         }
 650     }
 651
 652     if (st_lookup(table, node, &dummy)) {
 653         return(*dummy);
 654     }
 655
 656     Nv = cuddT(N);
 657     Nnv = cuddE(N);
 658     if (N != node) {
 659         Nv = Cudd_Not(Nv);
 660         Nnv = Cudd_Not(Nnv);
 661     }
 662
 663     /* Recur on the two branches. */
 664     min_v  = bddAnnotateMintermCount(manager,Nv,max,table) / 2.0;
 665     if (min_v == (double)CUDD_OUT_OF_MEM)
 666         return ((double)CUDD_OUT_OF_MEM);
 667     min_nv = bddAnnotateMintermCount(manager,Nnv,max,table) / 2.0;
 668     if (min_nv == (double)CUDD_OUT_OF_MEM)
 669         return ((double)CUDD_OUT_OF_MEM);
 670     min_N  = min_v + min_nv;
 671
 672     pmin = ALLOC(double,1);
 673     if (pmin == NULL) {
 674         manager->errorCode = CUDD_MEMORY_OUT;
 675         return((double)CUDD_OUT_OF_MEM);
 676     }
 677     *pmin = min_N;
 678
 679     if (st_insert(table,(char *)node, (char *)pmin) == ST_OUT_OF_MEM) {
 680         FREE(pmin);
 681         return((double)CUDD_OUT_OF_MEM);
 682     }
 683
 684     return(min_N);
 685
 686 } /* end of bddAnnotateMintermCount */