distr/cudd/cuddDecomp.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddDecomp.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Functions for BDD decomposition.]
   8
   9   Description [External procedures included in this file:
  10                 <ul>
  11                 <li> Cudd_bddApproxConjDecomp()
  12                 <li> Cudd_bddApproxDisjDecomp()
  13                 <li> Cudd_bddIterConjDecomp()
  14                 <li> Cudd_bddIterDisjDecomp()
  15                 <li> Cudd_bddGenConjDecomp()
  16                 <li> Cudd_bddGenDisjDecomp()
  17                 <li> Cudd_bddVarConjDecomp()
  18                 <li> Cudd_bddVarDisjDecomp()
  19                 </ul>
  20         Static procedures included in this module:
  21                 <ul>
  22                 <li> cuddConjunctsAux()
  23                 <li> CreateBotDist()
  24                 <li> BuildConjuncts()
  25                 <li> ConjunctsFree()
  26                 </ul>]
  27
  28   Author      [Kavita Ravi, Fabio Somenzi]
  29
  30   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  31
  32   All rights reserved.
  33
  34   Redistribution and use in source and binary forms, with or without
  35   modification, are permitted provided that the following conditions
  36   are met:
  37
  38   Redistributions of source code must retain the above copyright
  39   notice, this list of conditions and the following disclaimer.
  40
  41   Redistributions in binary form must reproduce the above copyright
  42   notice, this list of conditions and the following disclaimer in the
  43   documentation and/or other materials provided with the distribution.
  44
  45   Neither the name of the University of Colorado nor the names of its
  46   contributors may be used to endorse or promote products derived from
  47   this software without specific prior written permission.
  48
  49   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  50   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  51   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  52   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  53   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  54   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  55   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  56   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  57   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  58   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  59   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  60   POSSIBILITY OF SUCH DAMAGE.]
  61
  62 ******************************************************************************/
  63
  64 #include "util.h"
  65 #include "cuddInt.h"
  66
  67 /*---------------------------------------------------------------------------*/
  68 /* Constant declarations                                                     */
  69 /*---------------------------------------------------------------------------*/
  70 #define DEPTH 5
  71 #define THRESHOLD 10
  72 #define NONE 0
  73 #define PAIR_ST 1
  74 #define PAIR_CR 2
  75 #define G_ST 3
  76 #define G_CR 4
  77 #define H_ST 5
  78 #define H_CR 6
  79 #define BOTH_G 7
  80 #define BOTH_H 8
  81
  82 /*---------------------------------------------------------------------------*/
  83 /* Stucture declarations                                                     */
  84 /*---------------------------------------------------------------------------*/
  85
  86 /*---------------------------------------------------------------------------*/
  87 /* Type declarations                                                         */
  88 /*---------------------------------------------------------------------------*/
  89 typedef struct Conjuncts {
  90     DdNode *g;
  91     DdNode *h;
  92 } Conjuncts;
  93
  94 typedef struct  NodeStat {
  95     int distance;
  96     int localRef;
  97 } NodeStat;
  98
  99
 100 /*---------------------------------------------------------------------------*/
 101 /* Variable declarations                                                     */
 102 /*---------------------------------------------------------------------------*/
 103
 104 #ifndef lint
 105 static char rcsid[] DD_UNUSED = "$Id: cuddDecomp.c,v 1.44 2004/08/13 18:04:47 fabio Exp $";
 106 #endif
 107
 108 static  DdNode  *one, *zero;
 109 long lastTimeG;
 110
 111 /*---------------------------------------------------------------------------*/
 112 /* Macro declarations                                                        */
 113 /*---------------------------------------------------------------------------*/
 114
 115
 116 #define FactorsNotStored(factors)  ((int)((long)(factors) & 01))
 117
 118 #define FactorsComplement(factors) ((Conjuncts *)((long)(factors) | 01))
 119
 120 #define FactorsUncomplement(factors) ((Conjuncts *)((long)(factors) ^ 01))
 121
 122 /**AutomaticStart*************************************************************/
 123
 124 /*---------------------------------------------------------------------------*/
 125 /* Static function prototypes                                                */
 126 /*---------------------------------------------------------------------------*/
 127
 128 static NodeStat * CreateBotDist (DdNode * node, st_table * distanceTable);
 129 static double CountMinterms (DdNode * node, double max, st_table * mintermTable, FILE *fp);
 130 static void ConjunctsFree (DdManager * dd, Conjuncts * factors);
 131 static int PairInTables (DdNode * g, DdNode * h, st_table * ghTable);
 132 static Conjuncts * CheckTablesCacheAndReturn (DdNode * node, DdNode * g, DdNode * h, st_table * ghTable, st_table * cacheTable);
 133 static Conjuncts * PickOnePair (DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st_table * ghTable, st_table * cacheTable);
 134 static Conjuncts * CheckInTables (DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st_table * ghTable, st_table * cacheTable, int * outOfMem);
 135 static Conjuncts * ZeroCase (DdManager * dd, DdNode * node, Conjuncts * factorsNv, st_table * ghTable, st_table * cacheTable, int switched);
 136 static Conjuncts * BuildConjuncts (DdManager * dd, DdNode * node, st_table * distanceTable, st_table * cacheTable, int approxDistance, int maxLocalRef, st_table * ghTable, st_table * mintermTable);
 137 static int cuddConjunctsAux (DdManager * dd, DdNode * f, DdNode ** c1, DdNode ** c2);
 138
 139 /**AutomaticEnd***************************************************************/
 140
 141
 142 /*---------------------------------------------------------------------------*/
 143 /* Definition of exported functions                                          */
 144 /*---------------------------------------------------------------------------*/
 145
 146
 147 /**Function********************************************************************
 148
 149   Synopsis    [Performs two-way conjunctive decomposition of a BDD.]
 150
 151   Description [Performs two-way conjunctive decomposition of a
 152   BDD. This procedure owes its name to the use of supersetting to
 153   obtain an initial factor of the given function. Returns the number
 154   of conjuncts produced, that is, 2 if successful; 1 if no meaningful
 155   decomposition was found; 0 otherwise. The conjuncts produced by this
 156   procedure tend to be imbalanced.]
 157
 158   SideEffects [The factors are returned in an array as side effects.
 159   The array is allocated by this function. It is the caller's responsibility
 160   to free it. On successful completion, the conjuncts are already
 161   referenced. If the function returns 0, the array for the conjuncts is
 162   not allocated. If the function returns 1, the only factor equals the
 163   function to be decomposed.]
 164
 165   SeeAlso     [Cudd_bddApproxDisjDecomp Cudd_bddIterConjDecomp
 166   Cudd_bddGenConjDecomp Cudd_bddVarConjDecomp Cudd_RemapOverApprox
 167   Cudd_bddSqueeze Cudd_bddLICompaction]
 168
 169 ******************************************************************************/
 170 int
 171 Cudd_bddApproxConjDecomp(
 172   DdManager * dd /* manager */,
 173   DdNode * f /* function to be decomposed */,
 174   DdNode *** conjuncts /* address of the first factor */)
 175 {
 176     DdNode *superset1, *superset2, *glocal, *hlocal;
 177     int nvars = Cudd_SupportSize(dd,f);
 178
 179     /* Find a tentative first factor by overapproximation and minimization. */
 180     superset1 = Cudd_RemapOverApprox(dd,f,nvars,0,1.0);
 181     if (superset1 == NULL) return(0);
 182     cuddRef(superset1);
 183     superset2 = Cudd_bddSqueeze(dd,f,superset1);
 184     if (superset2 == NULL) {
 185         Cudd_RecursiveDeref(dd,superset1);
 186         return(0);
 187     }
 188     cuddRef(superset2);
 189     Cudd_RecursiveDeref(dd,superset1);
 190
 191     /* Compute the second factor by minimization. */
 192     hlocal = Cudd_bddLICompaction(dd,f,superset2);
 193     if (hlocal == NULL) {
 194         Cudd_RecursiveDeref(dd,superset2);
 195         return(0);
 196     }
 197     cuddRef(hlocal);
 198
 199     /* Refine the first factor by minimization. If h turns out to be f, this
 200     ** step guarantees that g will be 1. */
 201     glocal = Cudd_bddLICompaction(dd,superset2,hlocal);
 202     if (glocal == NULL) {
 203         Cudd_RecursiveDeref(dd,superset2);
 204         Cudd_RecursiveDeref(dd,hlocal);
 205         return(0);
 206     }
 207     cuddRef(glocal);
 208     Cudd_RecursiveDeref(dd,superset2);
 209
 210     if (glocal != DD_ONE(dd)) {
 211         if (hlocal != DD_ONE(dd)) {
 212             *conjuncts = ALLOC(DdNode *,2);
 213             if (*conjuncts == NULL) {
 214                 Cudd_RecursiveDeref(dd,glocal);
 215                 Cudd_RecursiveDeref(dd,hlocal);
 216                 dd->errorCode = CUDD_MEMORY_OUT;
 217                 return(0);
 218             }
 219             (*conjuncts)[0] = glocal;
 220             (*conjuncts)[1] = hlocal;
 221             return(2);
 222         } else {
 223             Cudd_RecursiveDeref(dd,hlocal);
 224             *conjuncts = ALLOC(DdNode *,1);
 225             if (*conjuncts == NULL) {
 226                 Cudd_RecursiveDeref(dd,glocal);
 227                 dd->errorCode = CUDD_MEMORY_OUT;
 228                 return(0);
 229             }
 230             (*conjuncts)[0] = glocal;
 231             return(1);
 232         }
 233     } else {
 234         Cudd_RecursiveDeref(dd,glocal);
 235         *conjuncts = ALLOC(DdNode *,1);
 236         if (*conjuncts == NULL) {
 237             Cudd_RecursiveDeref(dd,hlocal);
 238             dd->errorCode = CUDD_MEMORY_OUT;
 239             return(0);
 240         }
 241         (*conjuncts)[0] = hlocal;
 242         return(1);
 243     }
 244
 245 } /* end of Cudd_bddApproxConjDecomp */
 246
 247
 248 /**Function********************************************************************
 249
 250   Synopsis    [Performs two-way disjunctive decomposition of a BDD.]
 251
 252   Description [Performs two-way disjunctive decomposition of a BDD.
 253   Returns the number of disjuncts produced, that is, 2 if successful;
 254   1 if no meaningful decomposition was found; 0 otherwise. The
 255   disjuncts produced by this procedure tend to be imbalanced.]
 256
 257   SideEffects [The two disjuncts are returned in an array as side effects.
 258   The array is allocated by this function. It is the caller's responsibility
 259   to free it. On successful completion, the disjuncts are already
 260   referenced. If the function returns 0, the array for the disjuncts is
 261   not allocated. If the function returns 1, the only factor equals the
 262   function to be decomposed.]
 263
 264   SeeAlso     [Cudd_bddApproxConjDecomp Cudd_bddIterDisjDecomp
 265   Cudd_bddGenDisjDecomp Cudd_bddVarDisjDecomp]
 266
 267 ******************************************************************************/
 268 int
 269 Cudd_bddApproxDisjDecomp(
 270   DdManager * dd /* manager */,
 271   DdNode * f /* function to be decomposed */,
 272   DdNode *** disjuncts /* address of the array of the disjuncts */)
 273 {
 274     int result, i;
 275
 276     result = Cudd_bddApproxConjDecomp(dd,Cudd_Not(f),disjuncts);
 277     for (i = 0; i < result; i++) {
 278         (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
 279     }
 280     return(result);
 281
 282 } /* end of Cudd_bddApproxDisjDecomp */
 283
 284
 285 /**Function********************************************************************
 286
 287   Synopsis    [Performs two-way conjunctive decomposition of a BDD.]
 288
 289   Description [Performs two-way conjunctive decomposition of a
 290   BDD. This procedure owes its name to the iterated use of
 291   supersetting to obtain a factor of the given function. Returns the
 292   number of conjuncts produced, that is, 2 if successful; 1 if no
 293   meaningful decomposition was found; 0 otherwise. The conjuncts
 294   produced by this procedure tend to be imbalanced.]
 295
 296   SideEffects [The factors are returned in an array as side effects.
 297   The array is allocated by this function. It is the caller's responsibility
 298   to free it. On successful completion, the conjuncts are already
 299   referenced. If the function returns 0, the array for the conjuncts is
 300   not allocated. If the function returns 1, the only factor equals the
 301   function to be decomposed.]
 302
 303   SeeAlso     [Cudd_bddIterDisjDecomp Cudd_bddApproxConjDecomp
 304   Cudd_bddGenConjDecomp Cudd_bddVarConjDecomp Cudd_RemapOverApprox
 305   Cudd_bddSqueeze Cudd_bddLICompaction]
 306
 307 ******************************************************************************/
 308 int
 309 Cudd_bddIterConjDecomp(
 310   DdManager * dd /* manager */,
 311   DdNode * f /* function to be decomposed */,
 312   DdNode *** conjuncts /* address of the array of conjuncts */)
 313 {
 314     DdNode *superset1, *superset2, *old[2], *res[2];
 315     int sizeOld, sizeNew;
 316     int nvars = Cudd_SupportSize(dd,f);
 317
 318     old[0] = DD_ONE(dd);
 319     cuddRef(old[0]);
 320     old[1] = f;
 321     cuddRef(old[1]);
 322     sizeOld = Cudd_SharingSize(old,2);
 323
 324     do {
 325         /* Find a tentative first factor by overapproximation and
 326         ** minimization. */
 327         superset1 = Cudd_RemapOverApprox(dd,old[1],nvars,0,1.0);
 328         if (superset1 == NULL) {
 329             Cudd_RecursiveDeref(dd,old[0]);
 330             Cudd_RecursiveDeref(dd,old[1]);
 331             return(0);
 332         }
 333         cuddRef(superset1);
 334         superset2 = Cudd_bddSqueeze(dd,old[1],superset1);
 335         if (superset2 == NULL) {
 336             Cudd_RecursiveDeref(dd,old[0]);
 337             Cudd_RecursiveDeref(dd,old[1]);
 338             Cudd_RecursiveDeref(dd,superset1);
 339             return(0);
 340         }
 341         cuddRef(superset2);
 342         Cudd_RecursiveDeref(dd,superset1);
 343         res[0] = Cudd_bddAnd(dd,old[0],superset2);
 344         if (res[0] == NULL) {
 345             Cudd_RecursiveDeref(dd,superset2);
 346             Cudd_RecursiveDeref(dd,old[0]);
 347             Cudd_RecursiveDeref(dd,old[1]);
 348             return(0);
 349         }
 350         cuddRef(res[0]);
 351         Cudd_RecursiveDeref(dd,superset2);
 352         if (res[0] == old[0]) {
 353             Cudd_RecursiveDeref(dd,res[0]);
 354             break;      /* avoid infinite loop */
 355         }
 356
 357         /* Compute the second factor by minimization. */
 358         res[1] = Cudd_bddLICompaction(dd,old[1],res[0]);
 359         if (res[1] == NULL) {
 360             Cudd_RecursiveDeref(dd,old[0]);
 361             Cudd_RecursiveDeref(dd,old[1]);
 362             return(0);
 363         }
 364         cuddRef(res[1]);
 365
 366         sizeNew = Cudd_SharingSize(res,2);
 367         if (sizeNew <= sizeOld) {
 368             Cudd_RecursiveDeref(dd,old[0]);
 369             old[0] = res[0];
 370             Cudd_RecursiveDeref(dd,old[1]);
 371             old[1] = res[1];
 372             sizeOld = sizeNew;
 373         } else {
 374             Cudd_RecursiveDeref(dd,res[0]);
 375             Cudd_RecursiveDeref(dd,res[1]);
 376             break;
 377         }
 378
 379     } while (1);
 380
 381     /* Refine the first factor by minimization. If h turns out to
 382     ** be f, this step guarantees that g will be 1. */
 383     superset1 = Cudd_bddLICompaction(dd,old[0],old[1]);
 384     if (superset1 == NULL) {
 385         Cudd_RecursiveDeref(dd,old[0]);
 386         Cudd_RecursiveDeref(dd,old[1]);
 387         return(0);
 388     }
 389     cuddRef(superset1);
 390     Cudd_RecursiveDeref(dd,old[0]);
 391     old[0] = superset1;
 392
 393     if (old[0] != DD_ONE(dd)) {
 394         if (old[1] != DD_ONE(dd)) {
 395             *conjuncts = ALLOC(DdNode *,2);
 396             if (*conjuncts == NULL) {
 397                 Cudd_RecursiveDeref(dd,old[0]);
 398                 Cudd_RecursiveDeref(dd,old[1]);
 399                 dd->errorCode = CUDD_MEMORY_OUT;
 400                 return(0);
 401             }
 402             (*conjuncts)[0] = old[0];
 403             (*conjuncts)[1] = old[1];
 404             return(2);
 405         } else {
 406             Cudd_RecursiveDeref(dd,old[1]);
 407             *conjuncts = ALLOC(DdNode *,1);
 408             if (*conjuncts == NULL) {
 409                 Cudd_RecursiveDeref(dd,old[0]);
 410                 dd->errorCode = CUDD_MEMORY_OUT;
 411                 return(0);
 412             }
 413             (*conjuncts)[0] = old[0];
 414             return(1);
 415         }
 416     } else {
 417         Cudd_RecursiveDeref(dd,old[0]);
 418         *conjuncts = ALLOC(DdNode *,1);
 419         if (*conjuncts == NULL) {
 420             Cudd_RecursiveDeref(dd,old[1]);
 421             dd->errorCode = CUDD_MEMORY_OUT;
 422             return(0);
 423         }
 424         (*conjuncts)[0] = old[1];
 425         return(1);
 426     }
 427
 428 } /* end of Cudd_bddIterConjDecomp */
 429
 430
 431 /**Function********************************************************************
 432
 433   Synopsis    [Performs two-way disjunctive decomposition of a BDD.]
 434
 435   Description [Performs two-way disjunctive decomposition of a BDD.
 436   Returns the number of disjuncts produced, that is, 2 if successful;
 437   1 if no meaningful decomposition was found; 0 otherwise. The
 438   disjuncts produced by this procedure tend to be imbalanced.]
 439
 440   SideEffects [The two disjuncts are returned in an array as side effects.
 441   The array is allocated by this function. It is the caller's responsibility
 442   to free it. On successful completion, the disjuncts are already
 443   referenced. If the function returns 0, the array for the disjuncts is
 444   not allocated. If the function returns 1, the only factor equals the
 445   function to be decomposed.]
 446
 447   SeeAlso     [Cudd_bddIterConjDecomp Cudd_bddApproxDisjDecomp
 448   Cudd_bddGenDisjDecomp Cudd_bddVarDisjDecomp]
 449
 450 ******************************************************************************/
 451 int
 452 Cudd_bddIterDisjDecomp(
 453   DdManager * dd /* manager */,
 454   DdNode * f /* function to be decomposed */,
 455   DdNode *** disjuncts /* address of the array of the disjuncts */)
 456 {
 457     int result, i;
 458
 459     result = Cudd_bddIterConjDecomp(dd,Cudd_Not(f),disjuncts);
 460     for (i = 0; i < result; i++) {
 461         (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
 462     }
 463     return(result);
 464
 465 } /* end of Cudd_bddIterDisjDecomp */
 466
 467
 468 /**Function********************************************************************
 469
 470   Synopsis    [Performs two-way conjunctive decomposition of a BDD.]
 471
 472   Description [Performs two-way conjunctive decomposition of a
 473   BDD. This procedure owes its name to the fact tht it generalizes the
 474   decomposition based on the cofactors with respect to one
 475   variable. Returns the number of conjuncts produced, that is, 2 if
 476   successful; 1 if no meaningful decomposition was found; 0
 477   otherwise. The conjuncts produced by this procedure tend to be
 478   balanced.]
 479
 480   SideEffects [The two factors are returned in an array as side effects.
 481   The array is allocated by this function. It is the caller's responsibility
 482   to free it. On successful completion, the conjuncts are already
 483   referenced. If the function returns 0, the array for the conjuncts is
 484   not allocated. If the function returns 1, the only factor equals the
 485   function to be decomposed.]
 486
 487   SeeAlso     [Cudd_bddGenDisjDecomp Cudd_bddApproxConjDecomp
 488   Cudd_bddIterConjDecomp Cudd_bddVarConjDecomp]
 489
 490 ******************************************************************************/
 491 int
 492 Cudd_bddGenConjDecomp(
 493   DdManager * dd /* manager */,
 494   DdNode * f /* function to be decomposed */,
 495   DdNode *** conjuncts /* address of the array of conjuncts */)
 496 {
 497     int result;
 498     DdNode *glocal, *hlocal;
 499
 500     one = DD_ONE(dd);
 501     zero = Cudd_Not(one);
 502
 503     do {
 504         dd->reordered = 0;
 505         result = cuddConjunctsAux(dd, f, &glocal, &hlocal);
 506     } while (dd->reordered == 1);
 507
 508     if (result == 0) {
 509         return(0);
 510     }
 511
 512     if (glocal != one) {
 513         if (hlocal != one) {
 514             *conjuncts = ALLOC(DdNode *,2);
 515             if (*conjuncts == NULL) {
 516                 Cudd_RecursiveDeref(dd,glocal);
 517                 Cudd_RecursiveDeref(dd,hlocal);
 518                 dd->errorCode = CUDD_MEMORY_OUT;
 519                 return(0);
 520             }
 521             (*conjuncts)[0] = glocal;
 522             (*conjuncts)[1] = hlocal;
 523             return(2);
 524         } else {
 525             Cudd_RecursiveDeref(dd,hlocal);
 526             *conjuncts = ALLOC(DdNode *,1);
 527             if (*conjuncts == NULL) {
 528                 Cudd_RecursiveDeref(dd,glocal);
 529                 dd->errorCode = CUDD_MEMORY_OUT;
 530                 return(0);
 531             }
 532             (*conjuncts)[0] = glocal;
 533             return(1);
 534         }
 535     } else {
 536         Cudd_RecursiveDeref(dd,glocal);
 537         *conjuncts = ALLOC(DdNode *,1);
 538         if (*conjuncts == NULL) {
 539             Cudd_RecursiveDeref(dd,hlocal);
 540             dd->errorCode = CUDD_MEMORY_OUT;
 541             return(0);
 542         }
 543         (*conjuncts)[0] = hlocal;
 544         return(1);
 545     }
 546
 547 } /* end of Cudd_bddGenConjDecomp */
 548
 549
 550 /**Function********************************************************************
 551
 552   Synopsis    [Performs two-way disjunctive decomposition of a BDD.]
 553
 554   Description [Performs two-way disjunctive decomposition of a BDD.
 555   Returns the number of disjuncts produced, that is, 2 if successful;
 556   1 if no meaningful decomposition was found; 0 otherwise. The
 557   disjuncts produced by this procedure tend to be balanced.]
 558
 559   SideEffects [The two disjuncts are returned in an array as side effects.
 560   The array is allocated by this function. It is the caller's responsibility
 561   to free it. On successful completion, the disjuncts are already
 562   referenced. If the function returns 0, the array for the disjuncts is
 563   not allocated. If the function returns 1, the only factor equals the
 564   function to be decomposed.]
 565
 566   SeeAlso     [Cudd_bddGenConjDecomp Cudd_bddApproxDisjDecomp
 567   Cudd_bddIterDisjDecomp Cudd_bddVarDisjDecomp]
 568
 569 ******************************************************************************/
 570 int
 571 Cudd_bddGenDisjDecomp(
 572   DdManager * dd /* manager */,
 573   DdNode * f /* function to be decomposed */,
 574   DdNode *** disjuncts /* address of the array of the disjuncts */)
 575 {
 576     int result, i;
 577
 578     result = Cudd_bddGenConjDecomp(dd,Cudd_Not(f),disjuncts);
 579     for (i = 0; i < result; i++) {
 580         (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
 581     }
 582     return(result);
 583
 584 } /* end of Cudd_bddGenDisjDecomp */
 585
 586
 587 /**Function********************************************************************
 588
 589   Synopsis    [Performs two-way conjunctive decomposition of a BDD.]
 590
 591   Description [Conjunctively decomposes one BDD according to a
 592   variable.  If <code>f</code> is the function of the BDD and
 593   <code>x</code> is the variable, the decomposition is
 594   <code>(f+x)(f+x')</code>.  The variable is chosen so as to balance
 595   the sizes of the two conjuncts and to keep them small.  Returns the
 596   number of conjuncts produced, that is, 2 if successful; 1 if no
 597   meaningful decomposition was found; 0 otherwise.]
 598
 599   SideEffects [The two factors are returned in an array as side effects.
 600   The array is allocated by this function. It is the caller's responsibility
 601   to free it. On successful completion, the conjuncts are already
 602   referenced. If the function returns 0, the array for the conjuncts is
 603   not allocated. If the function returns 1, the only factor equals the
 604   function to be decomposed.]
 605
 606   SeeAlso     [Cudd_bddVarDisjDecomp Cudd_bddGenConjDecomp
 607   Cudd_bddApproxConjDecomp Cudd_bddIterConjDecomp]
 608
 609 *****************************************************************************/
 610 int
 611 Cudd_bddVarConjDecomp(
 612   DdManager * dd /* manager */,
 613   DdNode * f /* function to be decomposed */,
 614   DdNode *** conjuncts /* address of the array of conjuncts */)
 615 {
 616     int best;
 617     int min;
 618     DdNode *support, *scan, *var, *glocal, *hlocal;
 619
 620     /* Find best cofactoring variable. */
 621     support = Cudd_Support(dd,f);
 622     if (support == NULL) return(0);
 623     if (Cudd_IsConstant(support)) {
 624         *conjuncts = ALLOC(DdNode *,1);
 625         if (*conjuncts == NULL) {
 626             dd->errorCode = CUDD_MEMORY_OUT;
 627             return(0);
 628         }
 629         (*conjuncts)[0] = f;
 630         cuddRef((*conjuncts)[0]);
 631         return(1);
 632     }
 633     cuddRef(support);
 634     min = 1000000000;
 635     best = -1;
 636     scan = support;
 637     while (!Cudd_IsConstant(scan)) {
 638         int i = scan->index;
 639         int est1 = Cudd_EstimateCofactor(dd,f,i,1);
 640         int est0 = Cudd_EstimateCofactor(dd,f,i,0);
 641         /* Minimize the size of the larger of the two cofactors. */
 642         int est = (est1 > est0) ? est1 : est0;
 643         if (est < min) {
 644             min = est;
 645             best = i;
 646         }
 647         scan = cuddT(scan);
 648     }
 649 #ifdef DD_DEBUG
 650     assert(best >= 0 && best < dd->size);
 651 #endif
 652     Cudd_RecursiveDeref(dd,support);
 653
 654     var = Cudd_bddIthVar(dd,best);
 655     glocal = Cudd_bddOr(dd,f,var);
 656     if (glocal == NULL) {
 657         return(0);
 658     }
 659     cuddRef(glocal);
 660     hlocal = Cudd_bddOr(dd,f,Cudd_Not(var));
 661     if (hlocal == NULL) {
 662         Cudd_RecursiveDeref(dd,glocal);
 663         return(0);
 664     }
 665     cuddRef(hlocal);
 666
 667     if (glocal != DD_ONE(dd)) {
 668         if (hlocal != DD_ONE(dd)) {
 669             *conjuncts = ALLOC(DdNode *,2);
 670             if (*conjuncts == NULL) {
 671                 Cudd_RecursiveDeref(dd,glocal);
 672                 Cudd_RecursiveDeref(dd,hlocal);
 673                 dd->errorCode = CUDD_MEMORY_OUT;
 674                 return(0);
 675             }
 676             (*conjuncts)[0] = glocal;
 677             (*conjuncts)[1] = hlocal;
 678             return(2);
 679         } else {
 680             Cudd_RecursiveDeref(dd,hlocal);
 681             *conjuncts = ALLOC(DdNode *,1);
 682             if (*conjuncts == NULL) {
 683                 Cudd_RecursiveDeref(dd,glocal);
 684                 dd->errorCode = CUDD_MEMORY_OUT;
 685                 return(0);
 686             }
 687             (*conjuncts)[0] = glocal;
 688             return(1);
 689         }
 690     } else {
 691         Cudd_RecursiveDeref(dd,glocal);
 692         *conjuncts = ALLOC(DdNode *,1);
 693         if (*conjuncts == NULL) {
 694             Cudd_RecursiveDeref(dd,hlocal);
 695             dd->errorCode = CUDD_MEMORY_OUT;
 696             return(0);
 697         }
 698         (*conjuncts)[0] = hlocal;
 699         return(1);
 700     }
 701
 702 } /* end of Cudd_bddVarConjDecomp */
 703
 704
 705 /**Function********************************************************************
 706
 707   Synopsis    [Performs two-way disjunctive decomposition of a BDD.]
 708
 709   Description [Performs two-way disjunctive decomposition of a BDD
 710   according to a variable. If <code>f</code> is the function of the
 711   BDD and <code>x</code> is the variable, the decomposition is
 712   <code>f*x + f*x'</code>.  The variable is chosen so as to balance
 713   the sizes of the two disjuncts and to keep them small.  Returns the
 714   number of disjuncts produced, that is, 2 if successful; 1 if no
 715   meaningful decomposition was found; 0 otherwise.]
 716
 717   SideEffects [The two disjuncts are returned in an array as side effects.
 718   The array is allocated by this function. It is the caller's responsibility
 719   to free it. On successful completion, the disjuncts are already
 720   referenced. If the function returns 0, the array for the disjuncts is
 721   not allocated. If the function returns 1, the only factor equals the
 722   function to be decomposed.]
 723
 724   SeeAlso     [Cudd_bddVarConjDecomp Cudd_bddApproxDisjDecomp
 725   Cudd_bddIterDisjDecomp Cudd_bddGenDisjDecomp]
 726
 727 ******************************************************************************/
 728 int
 729 Cudd_bddVarDisjDecomp(
 730   DdManager * dd /* manager */,
 731   DdNode * f /* function to be decomposed */,
 732   DdNode *** disjuncts /* address of the array of the disjuncts */)
 733 {
 734     int result, i;
 735
 736     result = Cudd_bddVarConjDecomp(dd,Cudd_Not(f),disjuncts);
 737     for (i = 0; i < result; i++) {
 738         (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
 739     }
 740     return(result);
 741
 742 } /* end of Cudd_bddVarDisjDecomp */
 743
 744
 745 /*---------------------------------------------------------------------------*/
 746 /* Definition of internal functions                                          */
 747 /*---------------------------------------------------------------------------*/
 748
 749 /*---------------------------------------------------------------------------*/
 750 /* Definition of static functions                                            */
 751 /*---------------------------------------------------------------------------*/
 752
 753
 754 /**Function********************************************************************
 755
 756   Synopsis    [Get longest distance of node from constant.]
 757
 758   Description [Get longest distance of node from constant. Returns the
 759   distance of the root from the constant if successful; CUDD_OUT_OF_MEM
 760   otherwise.]
 761
 762   SideEffects [None]
 763
 764   SeeAlso     []
 765
 766 ******************************************************************************/
 767 static NodeStat *
 768 CreateBotDist(
 769   DdNode * node,
 770   st_table * distanceTable)
 771 {
 772     DdNode *N, *Nv, *Nnv;
 773     int distance, distanceNv, distanceNnv;
 774     NodeStat *nodeStat, *nodeStatNv, *nodeStatNnv;
 775
 776 #if 0
 777     if (Cudd_IsConstant(node)) {
 778         return(0);
 779     }
 780 #endif
 781
 782     /* Return the entry in the table if found. */
 783     N = Cudd_Regular(node);
 784     if (st_lookup(distanceTable, N, &nodeStat)) {
 785         nodeStat->localRef++;
 786         return(nodeStat);
 787     }
 788
 789     Nv = cuddT(N);
 790     Nnv = cuddE(N);
 791     Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
 792     Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
 793
 794     /* Recur on the children. */
 795     nodeStatNv = CreateBotDist(Nv, distanceTable);
 796     if (nodeStatNv == NULL) return(NULL);
 797     distanceNv = nodeStatNv->distance;
 798
 799     nodeStatNnv = CreateBotDist(Nnv, distanceTable);
 800     if (nodeStatNnv == NULL) return(NULL);
 801     distanceNnv = nodeStatNnv->distance;
 802     /* Store max distance from constant; note sometimes this distance
 803     ** may be to 0.
 804     */
 805     distance = (distanceNv > distanceNnv) ? (distanceNv+1) : (distanceNnv + 1);
 806
 807     nodeStat = ALLOC(NodeStat, 1);
 808     if (nodeStat == NULL) {
 809         return(0);
 810     }
 811     nodeStat->distance = distance;
 812     nodeStat->localRef = 1;
 813
 814     if (st_insert(distanceTable, (char *)N, (char *)nodeStat) ==
 815         ST_OUT_OF_MEM) {
 816         return(0);
 817
 818     }
 819     return(nodeStat);
 820
 821 } /* end of CreateBotDist */
 822
 823
 824 /**Function********************************************************************
 825
 826   Synopsis    [Count the number of minterms of each node ina a BDD and
 827   store it in a hash table.]
 828
 829   Description []
 830
 831   SideEffects [None]
 832
 833   SeeAlso     []
 834
 835 ******************************************************************************/
 836 static double
 837 CountMinterms(
 838   DdNode * node,
 839   double  max,
 840   st_table * mintermTable,
 841   FILE *fp)
 842 {
 843     DdNode *N, *Nv, *Nnv;
 844     double min, minNv, minNnv;
 845     double *dummy;
 846
 847     N = Cudd_Regular(node);
 848
 849     if (cuddIsConstant(N)) {
 850         if (node == zero) {
 851             return(0);
 852         } else {
 853             return(max);
 854         }
 855     }
 856
 857     /* Return the entry in the table if found. */
 858     if (st_lookup(mintermTable, node, &dummy)) {
 859         min = *dummy;
 860         return(min);
 861     }
 862
 863     Nv = cuddT(N);
 864     Nnv = cuddE(N);
 865     Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
 866     Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
 867
 868     /* Recur on the children. */
 869     minNv = CountMinterms(Nv, max, mintermTable, fp);
 870     if (minNv == -1.0) return(-1.0);
 871     minNnv = CountMinterms(Nnv, max, mintermTable, fp);
 872     if (minNnv == -1.0) return(-1.0);
 873     min = minNv / 2.0 + minNnv / 2.0;
 874     /* store
 875      */
 876
 877     dummy = ALLOC(double, 1);
 878     if (dummy == NULL) return(-1.0);
 879     *dummy = min;
 880     if (st_insert(mintermTable, (char *)node, (char *)dummy) == ST_OUT_OF_MEM) {
 881         (void) fprintf(fp, "st table insert failed\n");
 882     }
 883     return(min);
 884
 885 } /* end of CountMinterms */
 886
 887
 888 /**Function********************************************************************
 889
 890   Synopsis    [Free factors structure]
 891
 892   Description []
 893
 894   SideEffects [None]
 895
 896   SeeAlso     []
 897
 898 ******************************************************************************/
 899 static void
 900 ConjunctsFree(
 901   DdManager * dd,
 902   Conjuncts * factors)
 903 {
 904     Cudd_RecursiveDeref(dd, factors->g);
 905     Cudd_RecursiveDeref(dd, factors->h);
 906     FREE(factors);
 907     return;
 908
 909 } /* end of ConjunctsFree */
 910
 911
 912 /**Function********************************************************************
 913
 914   Synopsis    [Check whether the given pair is in the tables.]
 915
 916   Description [.Check whether the given pair is in the tables.  gTable
 917   and hTable are combined.
 918   absence in both is indicated by 0,
 919   presence in gTable is indicated by 1,
 920   presence in hTable by 2 and
 921   presence in both by 3.
 922   The values returned by this function are PAIR_ST,
 923   PAIR_CR, G_ST, G_CR, H_ST, H_CR, BOTH_G, BOTH_H, NONE.
 924   PAIR_ST implies g in gTable and h in hTable
 925   PAIR_CR implies g in hTable and h in gTable
 926   G_ST implies g in gTable and h not in any table
 927   G_CR implies g in hTable and h not in any table
 928   H_ST implies h in hTable and g not in any table
 929   H_CR implies h in gTable and g not in any table
 930   BOTH_G implies both in gTable
 931   BOTH_H implies both in hTable
 932   NONE implies none in table; ]
 933
 934   SideEffects []
 935
 936   SeeAlso     [CheckTablesCacheAndReturn CheckInTables]
 937
 938 ******************************************************************************/
 939 static int
 940 PairInTables(
 941   DdNode * g,
 942   DdNode * h,
 943   st_table * ghTable)
 944 {
 945     int valueG, valueH, gPresent, hPresent;
 946
 947     valueG = valueH = gPresent = hPresent = 0;
 948
 949     gPresent = st_lookup_int(ghTable, (char *)Cudd_Regular(g), &valueG);
 950     hPresent = st_lookup_int(ghTable, (char *)Cudd_Regular(h), &valueH);
 951
 952     if (!gPresent && !hPresent) return(NONE);
 953
 954     if (!hPresent) {
 955         if (valueG & 1) return(G_ST);
 956         if (valueG & 2) return(G_CR);
 957     }
 958     if (!gPresent) {
 959         if (valueH & 1) return(H_CR);
 960         if (valueH & 2) return(H_ST);
 961     }
 962     /* both in tables */
 963     if ((valueG & 1) && (valueH & 2)) return(PAIR_ST);
 964     if ((valueG & 2) && (valueH & 1)) return(PAIR_CR);
 965
 966     if (valueG & 1) {
 967         return(BOTH_G);
 968     } else {
 969         return(BOTH_H);
 970     }
 971
 972 } /* end of PairInTables */
 973
 974
 975 /**Function********************************************************************
 976
 977   Synopsis    [Check the tables for the existence of pair and return one
 978   combination, cache the result.]
 979
 980   Description [Check the tables for the existence of pair and return
 981   one combination, cache the result. The assumption is that one of the
 982   conjuncts is already in the tables.]
 983
 984   SideEffects [g and h referenced for the cache]
 985
 986   SeeAlso     [ZeroCase]
 987
 988 ******************************************************************************/
 989 static Conjuncts *
 990 CheckTablesCacheAndReturn(
 991   DdNode * node,
 992   DdNode * g,
 993   DdNode * h,
 994   st_table * ghTable,
 995   st_table * cacheTable)
 996 {
 997     int pairValue;
 998     int value;
 999     Conjuncts *factors;
1000
1001     value = 0;
1002     /* check tables */
1003     pairValue = PairInTables(g, h, ghTable);
1004     assert(pairValue != NONE);
1005     /* if both dont exist in table, we know one exists(either g or h).
1006      * Therefore store the other and proceed
1007      */
1008     factors = ALLOC(Conjuncts, 1);
1009     if (factors == NULL) return(NULL);
1010     if ((pairValue == BOTH_H) || (pairValue == H_ST)) {
1011         if (g != one) {
1012             value = 0;
1013             if (st_lookup_int(ghTable, (char *)Cudd_Regular(g), &value)) {
1014                 value |= 1;
1015             } else {
1016                 value = 1;
1017             }
1018             if (st_insert(ghTable, (char *)Cudd_Regular(g),
1019                           (char *)(long)value) == ST_OUT_OF_MEM) {
1020                 return(NULL);
1021             }
1022         }
1023         factors->g = g;
1024         factors->h = h;
1025     } else  if ((pairValue == BOTH_G) || (pairValue == G_ST)) {
1026         if (h != one) {
1027             value = 0;
1028             if (st_lookup_int(ghTable, (char *)Cudd_Regular(h), &value)) {
1029                 value |= 2;
1030             } else {
1031                 value = 2;
1032             }
1033             if (st_insert(ghTable, (char *)Cudd_Regular(h),
1034                           (char *)(long)value) == ST_OUT_OF_MEM) {
1035                 return(NULL);
1036             }
1037         }
1038         factors->g = g;
1039         factors->h = h;
1040     } else if (pairValue == H_CR) {
1041         if (g != one) {
1042             value = 2;
1043             if (st_insert(ghTable, (char *)Cudd_Regular(g),
1044                           (char *)(long)value) == ST_OUT_OF_MEM) {
1045                 return(NULL);
1046             }
1047         }
1048         factors->g = h;
1049         factors->h = g;
1050     } else if (pairValue == G_CR) {
1051         if (h != one) {
1052             value = 1;
1053             if (st_insert(ghTable, (char *)Cudd_Regular(h),
1054                           (char *)(long)value) == ST_OUT_OF_MEM) {
1055                 return(NULL);
1056             }
1057         }
1058         factors->g = h;
1059         factors->h = g;
1060     } else if (pairValue == PAIR_CR) {
1061     /* pair exists in table */
1062         factors->g = h;
1063         factors->h = g;
1064     } else if (pairValue == PAIR_ST) {
1065         factors->g = g;
1066         factors->h = h;
1067     }
1068
1069     /* cache the result for this node */
1070     if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
1071         FREE(factors);
1072         return(NULL);
1073     }
1074
1075     return(factors);
1076
1077 } /* end of CheckTablesCacheAndReturn */
1078
1079 /**Function********************************************************************
1080
1081   Synopsis    [Check the tables for the existence of pair and return one
1082   combination, store in cache.]
1083
1084   Description [Check the tables for the existence of pair and return
1085   one combination, store in cache. The pair that has more pointers to
1086   it is picked. An approximation of the number of local pointers is
1087   made by taking the reference count of the pairs sent. ]
1088
1089   SideEffects []
1090
1091   SeeAlso     [ZeroCase BuildConjuncts]
1092
1093 ******************************************************************************/
1094 static Conjuncts *
1095 PickOnePair(
1096   DdNode * node,
1097   DdNode * g1,
1098   DdNode * h1,
1099   DdNode * g2,
1100   DdNode * h2,
1101   st_table * ghTable,
1102   st_table * cacheTable)
1103 {
1104     int value;
1105     Conjuncts *factors;
1106     int oneRef, twoRef;
1107
1108     factors = ALLOC(Conjuncts, 1);
1109     if (factors == NULL) return(NULL);
1110
1111     /* count the number of pointers to pair 2 */
1112     if (h2 == one) {
1113         twoRef = (Cudd_Regular(g2))->ref;
1114     } else if (g2 == one) {
1115         twoRef = (Cudd_Regular(h2))->ref;
1116     } else {
1117         twoRef = ((Cudd_Regular(g2))->ref + (Cudd_Regular(h2))->ref)/2;
1118     }
1119
1120     /* count the number of pointers to pair 1 */
1121     if (h1 == one) {
1122         oneRef  = (Cudd_Regular(g1))->ref;
1123     } else if (g1 == one) {
1124         oneRef  = (Cudd_Regular(h1))->ref;
1125     } else {
1126         oneRef = ((Cudd_Regular(g1))->ref + (Cudd_Regular(h1))->ref)/2;
1127     }
1128
1129     /* pick the pair with higher reference count */
1130     if (oneRef >= twoRef) {
1131         factors->g = g1;
1132         factors->h = h1;
1133     } else {
1134         factors->g = g2;
1135         factors->h = h2;
1136     }
1137
1138     /*
1139      * Store computed factors in respective tables to encourage
1140      * recombination.
1141      */
1142     if (factors->g != one) {
1143         /* insert g in htable */
1144         value = 0;
1145         if (st_lookup_int(ghTable, (char *)Cudd_Regular(factors->g), &value)) {
1146             if (value == 2) {
1147                 value |= 1;
1148                 if (st_insert(ghTable, (char *)Cudd_Regular(factors->g),
1149                               (char *)(long)value) == ST_OUT_OF_MEM) {
1150                     FREE(factors);
1151                     return(NULL);
1152                 }
1153             }
1154         } else {
1155             value = 1;
1156             if (st_insert(ghTable, (char *)Cudd_Regular(factors->g),
1157                           (char *)(long)value) == ST_OUT_OF_MEM) {
1158                 FREE(factors);
1159                 return(NULL);
1160             }
1161         }
1162     }
1163
1164     if (factors->h != one) {
1165         /* insert h in htable */
1166         value = 0;
1167         if (st_lookup_int(ghTable, (char *)Cudd_Regular(factors->h), &value)) {
1168             if (value == 1) {
1169                 value |= 2;
1170                 if (st_insert(ghTable, (char *)Cudd_Regular(factors->h),
1171                               (char *)(long)value) == ST_OUT_OF_MEM) {
1172                     FREE(factors);
1173                     return(NULL);
1174                 }
1175             }
1176         } else {
1177             value = 2;
1178             if (st_insert(ghTable, (char *)Cudd_Regular(factors->h),
1179                           (char *)(long)value) == ST_OUT_OF_MEM) {
1180                 FREE(factors);
1181                 return(NULL);
1182             }
1183         }
1184     }
1185
1186     /* Store factors in cache table for later use. */
1187     if (st_insert(cacheTable, (char *)node, (char *)factors) ==
1188             ST_OUT_OF_MEM) {
1189         FREE(factors);
1190         return(NULL);
1191     }
1192
1193     return(factors);
1194
1195 } /* end of PickOnePair */
1196
1197
1198 /**Function********************************************************************
1199
1200   Synopsis [Check if the two pairs exist in the table, If any of the
1201   conjuncts do exist, store in the cache and return the corresponding pair.]
1202
1203   Description [Check if the two pairs exist in the table. If any of
1204   the conjuncts do exist, store in the cache and return the
1205   corresponding pair.]
1206
1207   SideEffects []
1208
1209   SeeAlso     [ZeroCase BuildConjuncts]
1210
1211 ******************************************************************************/
1212 static Conjuncts *
1213 CheckInTables(
1214   DdNode * node,
1215   DdNode * g1,
1216   DdNode * h1,
1217   DdNode * g2,
1218   DdNode * h2,
1219   st_table * ghTable,
1220   st_table * cacheTable,
1221   int * outOfMem)
1222 {
1223     int pairValue1,  pairValue2;
1224     Conjuncts *factors;
1225     int value;
1226
1227     *outOfMem = 0;
1228
1229     /* check existence of pair in table */
1230     pairValue1 = PairInTables(g1, h1, ghTable);
1231     pairValue2 = PairInTables(g2, h2, ghTable);
1232
1233     /* if none of the 4 exist in the gh tables, return NULL */
1234     if ((pairValue1 == NONE) && (pairValue2 == NONE)) {
1235         return NULL;
1236     }
1237
1238     factors = ALLOC(Conjuncts, 1);
1239     if (factors == NULL) {
1240         *outOfMem = 1;
1241         return NULL;
1242     }
1243
1244     /* pairs that already exist in the table get preference. */
1245     if (pairValue1 == PAIR_ST) {
1246         factors->g = g1;
1247         factors->h = h1;
1248     } else if (pairValue2 == PAIR_ST) {
1249         factors->g = g2;
1250         factors->h = h2;
1251     } else if (pairValue1 == PAIR_CR) {
1252         factors->g = h1;
1253         factors->h = g1;
1254     } else if (pairValue2 == PAIR_CR) {
1255         factors->g = h2;
1256         factors->h = g2;
1257     } else if (pairValue1 == G_ST) {
1258         /* g exists in the table, h is not found in either table */
1259         factors->g = g1;
1260         factors->h = h1;
1261         if (h1 != one) {
1262             value = 2;
1263             if (st_insert(ghTable, (char *)Cudd_Regular(h1),
1264                           (char *)(long)value) == ST_OUT_OF_MEM) {
1265                 *outOfMem = 1;
1266                 FREE(factors);
1267                 return(NULL);
1268             }
1269         }
1270     } else if (pairValue1 == BOTH_G) {
1271         /* g and h are  found in the g table */
1272         factors->g = g1;
1273         factors->h = h1;
1274         if (h1 != one) {
1275             value = 3;
1276             if (st_insert(ghTable, (char *)Cudd_Regular(h1),
1277                           (char *)(long)value) == ST_OUT_OF_MEM) {
1278                 *outOfMem = 1;
1279                 FREE(factors);
1280                 return(NULL);
1281             }
1282         }
1283     } else if (pairValue1 == H_ST) {
1284         /* h exists in the table, g is not found in either table */
1285         factors->g = g1;
1286         factors->h = h1;
1287         if (g1 != one) {
1288             value = 1;
1289             if (st_insert(ghTable, (char *)Cudd_Regular(g1),
1290                           (char *)(long)value) == ST_OUT_OF_MEM) {
1291                 *outOfMem = 1;
1292                 FREE(factors);
1293                 return(NULL);
1294             }
1295         }
1296     } else if (pairValue1 == BOTH_H) {
1297         /* g and h are  found in the h table */
1298         factors->g = g1;
1299         factors->h = h1;
1300         if (g1 != one) {
1301             value = 3;
1302             if (st_insert(ghTable, (char *)Cudd_Regular(g1),
1303                           (char *)(long)value) == ST_OUT_OF_MEM) {
1304                 *outOfMem = 1;
1305                 FREE(factors);
1306                 return(NULL);
1307             }
1308         }
1309     } else if (pairValue2 == G_ST) {
1310         /* g exists in the table, h is not found in either table */
1311         factors->g = g2;
1312         factors->h = h2;
1313         if (h2 != one) {
1314             value = 2;
1315             if (st_insert(ghTable, (char *)Cudd_Regular(h2),
1316                           (char *)(long)value) == ST_OUT_OF_MEM) {
1317                 *outOfMem = 1;
1318                 FREE(factors);
1319                 return(NULL);
1320             }
1321         }
1322     } else if  (pairValue2 == BOTH_G) {
1323         /* g and h are  found in the g table */
1324         factors->g = g2;
1325         factors->h = h2;
1326         if (h2 != one) {
1327             value = 3;
1328             if (st_insert(ghTable, (char *)Cudd_Regular(h2),
1329                           (char *)(long)value) == ST_OUT_OF_MEM) {
1330                 *outOfMem = 1;
1331                 FREE(factors);
1332                 return(NULL);
1333             }
1334         }
1335     } else if (pairValue2 == H_ST) {
1336         /* h exists in the table, g is not found in either table */
1337         factors->g = g2;
1338         factors->h = h2;
1339         if (g2 != one) {
1340             value = 1;
1341             if (st_insert(ghTable, (char *)Cudd_Regular(g2),
1342                           (char *)(long)value) == ST_OUT_OF_MEM) {
1343                 *outOfMem = 1;
1344                 FREE(factors);
1345                 return(NULL);
1346             }
1347         }
1348     } else if (pairValue2 == BOTH_H) {
1349         /* g and h are  found in the h table */
1350         factors->g = g2;
1351         factors->h = h2;
1352         if (g2 != one) {
1353             value = 3;
1354             if (st_insert(ghTable, (char *)Cudd_Regular(g2),
1355                           (char *)(long)value) == ST_OUT_OF_MEM) {
1356                 *outOfMem = 1;
1357                 FREE(factors);
1358                 return(NULL);
1359             }
1360         }
1361     } else if (pairValue1 == G_CR) {
1362         /* g found in h table and h in none */
1363         factors->g = h1;
1364         factors->h = g1;
1365         if (h1 != one) {
1366             value = 1;
1367             if (st_insert(ghTable, (char *)Cudd_Regular(h1),
1368                           (char *)(long)value) == ST_OUT_OF_MEM) {
1369                 *outOfMem = 1;
1370                 FREE(factors);
1371                 return(NULL);
1372             }
1373         }
1374     } else if (pairValue1 == H_CR) {
1375         /* h found in g table and g in none */
1376         factors->g = h1;
1377         factors->h = g1;
1378         if (g1 != one) {
1379             value = 2;
1380             if (st_insert(ghTable, (char *)Cudd_Regular(g1),
1381                           (char *)(long)value) == ST_OUT_OF_MEM) {
1382                 *outOfMem = 1;
1383                 FREE(factors);
1384                 return(NULL);
1385             }
1386         }
1387     } else if (pairValue2 == G_CR) {
1388         /* g found in h table and h in none */
1389         factors->g = h2;
1390         factors->h = g2;
1391         if (h2 != one) {
1392             value = 1;
1393             if (st_insert(ghTable, (char *)Cudd_Regular(h2),
1394                           (char *)(long)value) == ST_OUT_OF_MEM) {
1395                 *outOfMem = 1;
1396                 FREE(factors);
1397                 return(NULL);
1398             }
1399         }
1400     } else if (pairValue2 == H_CR) {
1401         /* h found in g table and g in none */
1402         factors->g = h2;
1403         factors->h = g2;
1404         if (g2 != one) {
1405             value = 2;
1406             if (st_insert(ghTable, (char *)Cudd_Regular(g2),
1407                           (char *)(long)value) == ST_OUT_OF_MEM) {
1408                 *outOfMem = 1;
1409                 FREE(factors);
1410                 return(NULL);
1411             }
1412         }
1413     }
1414
1415     /* Store factors in cache table for later use. */
1416     if (st_insert(cacheTable, (char *)node, (char *)factors) ==
1417             ST_OUT_OF_MEM) {
1418         *outOfMem = 1;
1419         FREE(factors);
1420         return(NULL);
1421     }
1422     return factors;
1423 } /* end of CheckInTables */
1424
1425
1426
1427 /**Function********************************************************************
1428
1429   Synopsis    [If one child is zero, do explicitly what Restrict does or better]
1430
1431   Description [If one child is zero, do explicitly what Restrict does or better.
1432   First separate a variable and its child in the base case. In case of a cube
1433   times a function, separate the cube and function. As a last resort, look in
1434   tables.]
1435
1436   SideEffects [Frees the BDDs in factorsNv. factorsNv itself is not freed
1437   because it is freed above.]
1438
1439   SeeAlso     [BuildConjuncts]
1440
1441 ******************************************************************************/
1442 static Conjuncts *
1443 ZeroCase(
1444   DdManager * dd,
1445   DdNode * node,
1446   Conjuncts * factorsNv,
1447   st_table * ghTable,
1448   st_table * cacheTable,
1449   int switched)
1450 {
1451     int topid;
1452     DdNode *g, *h, *g1, *g2, *h1, *h2, *x, *N, *G, *H, *Gv, *Gnv;
1453     DdNode *Hv, *Hnv;
1454     int value;
1455     int outOfMem;
1456     Conjuncts *factors;
1457
1458     /* get var at this node */
1459     N = Cudd_Regular(node);
1460     topid = N->index;
1461     x = dd->vars[topid];
1462     x = (switched) ? Cudd_Not(x): x;
1463     cuddRef(x);
1464
1465     /* Seprate variable and child */
1466     if (factorsNv->g == one) {
1467         Cudd_RecursiveDeref(dd, factorsNv->g);
1468         factors = ALLOC(Conjuncts, 1);
1469         if (factors == NULL) {
1470             dd->errorCode = CUDD_MEMORY_OUT;
1471             Cudd_RecursiveDeref(dd, factorsNv->h);
1472             Cudd_RecursiveDeref(dd, x);
1473             return(NULL);
1474         }
1475         factors->g = x;
1476         factors->h = factorsNv->h;
1477         /* cache the result*/
1478         if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
1479             dd->errorCode = CUDD_MEMORY_OUT;
1480             Cudd_RecursiveDeref(dd, factorsNv->h);
1481             Cudd_RecursiveDeref(dd, x);
1482             FREE(factors);
1483             return NULL;
1484         }
1485
1486         /* store  x in g table, the other node is already in the table */
1487         if (st_lookup_int(ghTable, (char *)Cudd_Regular(x), &value)) {
1488             value |= 1;
1489         } else {
1490             value = 1;
1491         }
1492         if (st_insert(ghTable, (char *)Cudd_Regular(x), (char *)(long)value) == ST_OUT_OF_MEM) {
1493             dd->errorCode = CUDD_MEMORY_OUT;
1494             return NULL;
1495         }
1496         return(factors);
1497     }
1498
1499     /* Seprate variable and child */
1500     if (factorsNv->h == one) {
1501         Cudd_RecursiveDeref(dd, factorsNv->h);
1502         factors = ALLOC(Conjuncts, 1);
1503         if (factors == NULL) {
1504             dd->errorCode = CUDD_MEMORY_OUT;
1505             Cudd_RecursiveDeref(dd, factorsNv->g);
1506             Cudd_RecursiveDeref(dd, x);
1507             return(NULL);
1508         }
1509         factors->g = factorsNv->g;
1510         factors->h = x;
1511         /* cache the result. */
1512         if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
1513             dd->errorCode = CUDD_MEMORY_OUT;
1514             Cudd_RecursiveDeref(dd, factorsNv->g);
1515             Cudd_RecursiveDeref(dd, x);
1516             FREE(factors);
1517             return(NULL);
1518         }
1519         /* store x in h table,  the other node is already in the table */
1520         if (st_lookup_int(ghTable, (char *)Cudd_Regular(x), &value)) {
1521             value |= 2;
1522         } else {
1523             value = 2;
1524         }
1525         if (st_insert(ghTable, (char *)Cudd_Regular(x), (char *)(long)value) == ST_OUT_OF_MEM) {
1526             dd->errorCode = CUDD_MEMORY_OUT;
1527             return NULL;
1528         }
1529         return(factors);
1530     }
1531
1532     G = Cudd_Regular(factorsNv->g);
1533     Gv = cuddT(G);
1534     Gnv = cuddE(G);
1535     Gv = Cudd_NotCond(Gv, Cudd_IsComplement(node));
1536     Gnv = Cudd_NotCond(Gnv, Cudd_IsComplement(node));
1537     /* if the child below is a variable */
1538     if ((Gv == zero) || (Gnv == zero)) {
1539         h = factorsNv->h;
1540         g = cuddBddAndRecur(dd, x, factorsNv->g);
1541         if (g != NULL)  cuddRef(g);
1542         Cudd_RecursiveDeref(dd, factorsNv->g);
1543         Cudd_RecursiveDeref(dd, x);
1544         if (g == NULL) {
1545             Cudd_RecursiveDeref(dd, factorsNv->h);
1546             return NULL;
1547         }
1548         /* CheckTablesCacheAndReturn responsible for allocating
1549          * factors structure., g,h referenced for cache store  the
1550          */
1551         factors = CheckTablesCacheAndReturn(node,
1552                                             g,
1553                                             h,
1554                                             ghTable,
1555                                             cacheTable);
1556         if (factors == NULL) {
1557             dd->errorCode = CUDD_MEMORY_OUT;
1558             Cudd_RecursiveDeref(dd, g);
1559             Cudd_RecursiveDeref(dd, h);
1560         }
1561         return(factors);
1562     }
1563
1564     H = Cudd_Regular(factorsNv->h);
1565     Hv = cuddT(H);
1566     Hnv = cuddE(H);
1567     Hv = Cudd_NotCond(Hv, Cudd_IsComplement(node));
1568     Hnv = Cudd_NotCond(Hnv, Cudd_IsComplement(node));
1569     /* if the child below is a variable */
1570     if ((Hv == zero) || (Hnv == zero)) {
1571         g = factorsNv->g;
1572         h = cuddBddAndRecur(dd, x, factorsNv->h);
1573         if (h!= NULL) cuddRef(h);
1574         Cudd_RecursiveDeref(dd, factorsNv->h);
1575         Cudd_RecursiveDeref(dd, x);
1576         if (h == NULL) {
1577             Cudd_RecursiveDeref(dd, factorsNv->g);
1578             return NULL;
1579         }
1580         /* CheckTablesCacheAndReturn responsible for allocating
1581          * factors structure.g,h referenced for table store
1582          */
1583         factors = CheckTablesCacheAndReturn(node,
1584                                             g,
1585                                             h,
1586                                             ghTable,
1587                                             cacheTable);
1588         if (factors == NULL) {
1589             dd->errorCode = CUDD_MEMORY_OUT;
1590             Cudd_RecursiveDeref(dd, g);
1591             Cudd_RecursiveDeref(dd, h);
1592         }
1593         return(factors);
1594     }
1595
1596     /* build g1 = x*g; h1 = h */
1597     /* build g2 = g; h2 = x*h */
1598     Cudd_RecursiveDeref(dd, x);
1599     h1 = factorsNv->h;
1600     g1 = cuddBddAndRecur(dd, x, factorsNv->g);
1601     if (g1 != NULL) cuddRef(g1);
1602     if (g1 == NULL) {
1603         Cudd_RecursiveDeref(dd, factorsNv->g);
1604         Cudd_RecursiveDeref(dd, factorsNv->h);
1605         return NULL;
1606     }
1607
1608     g2 = factorsNv->g;
1609     h2 = cuddBddAndRecur(dd, x, factorsNv->h);
1610     if (h2 != NULL) cuddRef(h2);
1611     if (h2 == NULL) {
1612         Cudd_RecursiveDeref(dd, factorsNv->h);
1613         Cudd_RecursiveDeref(dd, factorsNv->g);
1614         return NULL;
1615     }
1616
1617     /* check whether any pair is in tables */
1618     factors = CheckInTables(node, g1, h1, g2, h2, ghTable, cacheTable, &outOfMem);
1619     if (outOfMem) {
1620         dd->errorCode = CUDD_MEMORY_OUT;
1621         Cudd_RecursiveDeref(dd, g1);
1622         Cudd_RecursiveDeref(dd, h1);
1623         Cudd_RecursiveDeref(dd, g2);
1624         Cudd_RecursiveDeref(dd, h2);
1625         return NULL;
1626     }
1627     if (factors != NULL) {
1628         if ((factors->g == g1) || (factors->g == h1)) {
1629             Cudd_RecursiveDeref(dd, g2);
1630             Cudd_RecursiveDeref(dd, h2);
1631         } else {
1632             Cudd_RecursiveDeref(dd, g1);
1633             Cudd_RecursiveDeref(dd, h1);
1634         }
1635         return factors;
1636     }
1637
1638     /* check for each pair in tables and choose one */
1639     factors = PickOnePair(node,g1, h1, g2, h2, ghTable, cacheTable);
1640     if (factors == NULL) {
1641         dd->errorCode = CUDD_MEMORY_OUT;
1642         Cudd_RecursiveDeref(dd, g1);
1643         Cudd_RecursiveDeref(dd, h1);
1644         Cudd_RecursiveDeref(dd, g2);
1645         Cudd_RecursiveDeref(dd, h2);
1646     } else {
1647         /* now free what was created and not used */
1648         if ((factors->g == g1) || (factors->g == h1)) {
1649             Cudd_RecursiveDeref(dd, g2);
1650             Cudd_RecursiveDeref(dd, h2);
1651         } else {
1652             Cudd_RecursiveDeref(dd, g1);
1653             Cudd_RecursiveDeref(dd, h1);
1654         }
1655     }
1656
1657     return(factors);
1658 } /* end of ZeroCase */
1659
1660
1661 /**Function********************************************************************
1662
1663   Synopsis    [Builds the conjuncts recursively, bottom up.]
1664
1665   Description [Builds the conjuncts recursively, bottom up. Constants
1666   are returned as (f, f). The cache is checked for previously computed
1667   result. The decomposition points are determined by the local
1668   reference count of this node and the longest distance from the
1669   constant. At the decomposition point, the factors returned are (f,
1670   1). Recur on the two children. The order is determined by the
1671   heavier branch. Combine the factors of the two children and pick the
1672   one that already occurs in the gh table. Occurence in g is indicated
1673   by value 1, occurence in h by 2, occurence in both 3.]
1674
1675   SideEffects []
1676
1677   SeeAlso     [cuddConjunctsAux]
1678
1679 ******************************************************************************/
1680 static Conjuncts *
1681 BuildConjuncts(
1682   DdManager * dd,
1683   DdNode * node,
1684   st_table * distanceTable,
1685   st_table * cacheTable,
1686   int approxDistance,
1687   int maxLocalRef,
1688   st_table * ghTable,
1689   st_table * mintermTable)
1690 {
1691     int topid, distance;
1692     Conjuncts *factorsNv, *factorsNnv, *factors;
1693     Conjuncts *dummy;
1694     DdNode *N, *Nv, *Nnv, *temp, *g1, *g2, *h1, *h2, *topv;
1695     double minNv = 0.0, minNnv = 0.0;
1696     double *doubleDummy;
1697     int switched =0;
1698     int outOfMem;
1699     int freeNv = 0, freeNnv = 0, freeTemp;
1700     NodeStat *nodeStat;
1701     int value;
1702
1703     /* if f is constant, return (f,f) */
1704     if (Cudd_IsConstant(node)) {
1705         factors = ALLOC(Conjuncts, 1);
1706         if (factors == NULL) {
1707             dd->errorCode = CUDD_MEMORY_OUT;
1708             return(NULL);
1709         }
1710         factors->g = node;
1711         factors->h = node;
1712         return(FactorsComplement(factors));
1713     }
1714
1715     /* If result (a pair of conjuncts) in cache, return the factors. */
1716     if (st_lookup(cacheTable, node, &dummy)) {
1717         factors = dummy;
1718         return(factors);
1719     }
1720
1721     /* check distance and local reference count of this node */
1722     N = Cudd_Regular(node);
1723     if (!st_lookup(distanceTable, N, &nodeStat)) {
1724         (void) fprintf(dd->err, "Not in table, Something wrong\n");
1725         dd->errorCode = CUDD_INTERNAL_ERROR;
1726         return(NULL);
1727     }
1728     distance = nodeStat->distance;
1729
1730     /* at or below decomposition point, return (f, 1) */
1731     if (((nodeStat->localRef > maxLocalRef*2/3) &&
1732          (distance < approxDistance*2/3)) ||
1733             (distance <= approxDistance/4)) {
1734         factors = ALLOC(Conjuncts, 1);
1735         if (factors == NULL) {
1736             dd->errorCode = CUDD_MEMORY_OUT;
1737             return(NULL);
1738         }
1739         /* alternate assigning (f,1) */
1740         value = 0;
1741         if (st_lookup_int(ghTable, (char *)Cudd_Regular(node), &value)) {
1742             if (value == 3) {
1743                 if (!lastTimeG) {
1744                     factors->g = node;
1745                     factors->h = one;
1746                     lastTimeG = 1;
1747                 } else {
1748                     factors->g = one;
1749                     factors->h = node;
1750                     lastTimeG = 0;
1751                 }
1752             } else if (value == 1) {
1753                 factors->g = node;
1754                 factors->h = one;
1755             } else {
1756                 factors->g = one;
1757                 factors->h = node;
1758             }
1759         } else if (!lastTimeG) {
1760             factors->g = node;
1761             factors->h = one;
1762             lastTimeG = 1;
1763             value = 1;
1764             if (st_insert(ghTable, (char *)Cudd_Regular(node), (char *)(long)value) == ST_OUT_OF_MEM) {
1765                 dd->errorCode = CUDD_MEMORY_OUT;
1766                 FREE(factors);
1767                 return NULL;
1768             }
1769         } else {
1770             factors->g = one;
1771             factors->h = node;
1772             lastTimeG = 0;
1773             value = 2;
1774             if (st_insert(ghTable, (char *)Cudd_Regular(node), (char *)(long)value) == ST_OUT_OF_MEM) {
1775                 dd->errorCode = CUDD_MEMORY_OUT;
1776                 FREE(factors);
1777                 return NULL;
1778             }
1779         }
1780         return(FactorsComplement(factors));
1781     }
1782
1783     /* get the children and recur */
1784     Nv = cuddT(N);
1785     Nnv = cuddE(N);
1786     Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
1787     Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
1788
1789     /* Choose which subproblem to solve first based on the number of
1790      * minterms. We go first where there are more minterms.
1791      */
1792     if (!Cudd_IsConstant(Nv)) {
1793         if (!st_lookup(mintermTable, Nv, &doubleDummy)) {
1794             (void) fprintf(dd->err, "Not in table: Something wrong\n");
1795             dd->errorCode = CUDD_INTERNAL_ERROR;
1796             return(NULL);
1797         }
1798         minNv = *doubleDummy;
1799     }
1800
1801     if (!Cudd_IsConstant(Nnv)) {
1802         if (!st_lookup(mintermTable, Nnv, &doubleDummy)) {
1803             (void) fprintf(dd->err, "Not in table: Something wrong\n");
1804             dd->errorCode = CUDD_INTERNAL_ERROR;
1805             return(NULL);
1806         }
1807         minNnv = *doubleDummy;
1808     }
1809
1810     if (minNv < minNnv) {
1811         temp = Nv;
1812         Nv = Nnv;
1813         Nnv = temp;
1814         switched = 1;
1815     }
1816
1817     /* build gt, ht recursively */
1818     if (Nv != zero) {
1819         factorsNv = BuildConjuncts(dd, Nv, distanceTable,
1820                                    cacheTable, approxDistance, maxLocalRef,
1821                                    ghTable, mintermTable);
1822         if (factorsNv == NULL) return(NULL);
1823         freeNv = FactorsNotStored(factorsNv);
1824         factorsNv = (freeNv) ? FactorsUncomplement(factorsNv) : factorsNv;
1825         cuddRef(factorsNv->g);
1826         cuddRef(factorsNv->h);
1827
1828         /* Deal with the zero case */
1829         if (Nnv == zero) {
1830             /* is responsible for freeing factorsNv */
1831             factors = ZeroCase(dd, node, factorsNv, ghTable,
1832                                cacheTable, switched);
1833             if (freeNv) FREE(factorsNv);
1834             return(factors);
1835         }
1836     }
1837
1838     /* build ge, he recursively */
1839     if (Nnv != zero) {
1840         factorsNnv = BuildConjuncts(dd, Nnv, distanceTable,
1841                                     cacheTable, approxDistance, maxLocalRef,
1842                                     ghTable, mintermTable);
1843         if (factorsNnv == NULL) {
1844             Cudd_RecursiveDeref(dd, factorsNv->g);
1845             Cudd_RecursiveDeref(dd, factorsNv->h);
1846             if (freeNv) FREE(factorsNv);
1847             return(NULL);
1848         }
1849         freeNnv = FactorsNotStored(factorsNnv);
1850         factorsNnv = (freeNnv) ? FactorsUncomplement(factorsNnv) : factorsNnv;
1851         cuddRef(factorsNnv->g);
1852         cuddRef(factorsNnv->h);
1853
1854         /* Deal with the zero case */
1855         if (Nv == zero) {
1856             /* is responsible for freeing factorsNv */
1857             factors = ZeroCase(dd, node, factorsNnv, ghTable,
1858                                cacheTable, switched);
1859             if (freeNnv) FREE(factorsNnv);
1860             return(factors);
1861         }
1862     }
1863
1864     /* construct the 2 pairs */
1865     /* g1 = x*gt + x'*ge; h1 = x*ht + x'*he; */
1866     /* g2 = x*gt + x'*he; h2 = x*ht + x'*ge */
1867     if (switched) {
1868         factors = factorsNnv;
1869         factorsNnv = factorsNv;
1870         factorsNv = factors;
1871         freeTemp = freeNv;
1872         freeNv = freeNnv;
1873         freeNnv = freeTemp;
1874     }
1875
1876     /* Build the factors for this node. */
1877     topid = N->index;
1878     topv = dd->vars[topid];
1879
1880     g1 = cuddBddIteRecur(dd, topv, factorsNv->g, factorsNnv->g);
1881     if (g1 == NULL) {
1882         Cudd_RecursiveDeref(dd, factorsNv->g);
1883         Cudd_RecursiveDeref(dd, factorsNv->h);
1884         Cudd_RecursiveDeref(dd, factorsNnv->g);
1885         Cudd_RecursiveDeref(dd, factorsNnv->h);
1886         if (freeNv) FREE(factorsNv);
1887         if (freeNnv) FREE(factorsNnv);
1888         return(NULL);
1889     }
1890
1891     cuddRef(g1);
1892
1893     h1 = cuddBddIteRecur(dd, topv, factorsNv->h, factorsNnv->h);
1894     if (h1 == NULL) {
1895         Cudd_RecursiveDeref(dd, factorsNv->g);
1896         Cudd_RecursiveDeref(dd, factorsNv->h);
1897         Cudd_RecursiveDeref(dd, factorsNnv->g);
1898         Cudd_RecursiveDeref(dd, factorsNnv->h);
1899         Cudd_RecursiveDeref(dd, g1);
1900         if (freeNv) FREE(factorsNv);
1901         if (freeNnv) FREE(factorsNnv);
1902         return(NULL);
1903     }
1904
1905     cuddRef(h1);
1906
1907     g2 = cuddBddIteRecur(dd, topv, factorsNv->g, factorsNnv->h);
1908     if (g2 == NULL) {
1909         Cudd_RecursiveDeref(dd, factorsNv->h);
1910         Cudd_RecursiveDeref(dd, factorsNv->g);
1911         Cudd_RecursiveDeref(dd, factorsNnv->g);
1912         Cudd_RecursiveDeref(dd, factorsNnv->h);
1913         Cudd_RecursiveDeref(dd, g1);
1914         Cudd_RecursiveDeref(dd, h1);
1915         if (freeNv) FREE(factorsNv);
1916         if (freeNnv) FREE(factorsNnv);
1917         return(NULL);
1918     }
1919     cuddRef(g2);
1920     Cudd_RecursiveDeref(dd, factorsNv->g);
1921     Cudd_RecursiveDeref(dd, factorsNnv->h);
1922
1923     h2 = cuddBddIteRecur(dd, topv, factorsNv->h, factorsNnv->g);
1924     if (h2 == NULL) {
1925         Cudd_RecursiveDeref(dd, factorsNv->g);
1926         Cudd_RecursiveDeref(dd, factorsNv->h);
1927         Cudd_RecursiveDeref(dd, factorsNnv->g);
1928         Cudd_RecursiveDeref(dd, factorsNnv->h);
1929         Cudd_RecursiveDeref(dd, g1);
1930         Cudd_RecursiveDeref(dd, h1);
1931         Cudd_RecursiveDeref(dd, g2);
1932         if (freeNv) FREE(factorsNv);
1933         if (freeNnv) FREE(factorsNnv);
1934         return(NULL);
1935     }
1936     cuddRef(h2);
1937     Cudd_RecursiveDeref(dd, factorsNv->h);
1938     Cudd_RecursiveDeref(dd, factorsNnv->g);
1939     if (freeNv) FREE(factorsNv);
1940     if (freeNnv) FREE(factorsNnv);
1941
1942     /* check for each pair in tables and choose one */
1943     factors = CheckInTables(node, g1, h1, g2, h2, ghTable, cacheTable, &outOfMem);
1944     if (outOfMem) {
1945         dd->errorCode = CUDD_MEMORY_OUT;
1946         Cudd_RecursiveDeref(dd, g1);
1947         Cudd_RecursiveDeref(dd, h1);
1948         Cudd_RecursiveDeref(dd, g2);
1949         Cudd_RecursiveDeref(dd, h2);
1950         return(NULL);
1951     }
1952     if (factors != NULL) {
1953         if ((factors->g == g1) || (factors->g == h1)) {
1954             Cudd_RecursiveDeref(dd, g2);
1955             Cudd_RecursiveDeref(dd, h2);
1956         } else {
1957             Cudd_RecursiveDeref(dd, g1);
1958             Cudd_RecursiveDeref(dd, h1);
1959         }
1960         return(factors);
1961     }
1962
1963     /* if not in tables, pick one pair */
1964     factors = PickOnePair(node,g1, h1, g2, h2, ghTable, cacheTable);
1965     if (factors == NULL) {
1966         dd->errorCode = CUDD_MEMORY_OUT;
1967         Cudd_RecursiveDeref(dd, g1);
1968         Cudd_RecursiveDeref(dd, h1);
1969         Cudd_RecursiveDeref(dd, g2);
1970         Cudd_RecursiveDeref(dd, h2);
1971     } else {
1972         /* now free what was created and not used */
1973         if ((factors->g == g1) || (factors->g == h1)) {
1974             Cudd_RecursiveDeref(dd, g2);
1975             Cudd_RecursiveDeref(dd, h2);
1976         } else {
1977             Cudd_RecursiveDeref(dd, g1);
1978             Cudd_RecursiveDeref(dd, h1);
1979         }
1980     }
1981
1982     return(factors);
1983
1984 } /* end of BuildConjuncts */
1985
1986
1987 /**Function********************************************************************
1988
1989   Synopsis    [Procedure to compute two conjunctive factors of f and place in *c1 and *c2.]
1990
1991   Description [Procedure to compute two conjunctive factors of f and
1992   place in *c1 and *c2. Sets up the required data - table of distances
1993   from the constant and local reference count. Also minterm table. ]
1994
1995   SideEffects []
1996
1997   SeeAlso     []
1998
1999 ******************************************************************************/
2000 static int
2001 cuddConjunctsAux(
2002   DdManager * dd,
2003   DdNode * f,
2004   DdNode ** c1,
2005   DdNode ** c2)
2006 {
2007     st_table *distanceTable = NULL;
2008     st_table *cacheTable = NULL;
2009     st_table *mintermTable = NULL;
2010     st_table *ghTable = NULL;
2011     st_generator *stGen;
2012     char *key, *value;
2013     Conjuncts *factors;
2014     int distance, approxDistance;
2015     double max, minterms;
2016     int freeFactors;
2017     NodeStat *nodeStat;
2018     int maxLocalRef;
2019
2020     /* initialize */
2021     *c1 = NULL;
2022     *c2 = NULL;
2023
2024     /* initialize distances table */
2025     distanceTable = st_init_table(st_ptrcmp,st_ptrhash);
2026     if (distanceTable == NULL) goto outOfMem;
2027
2028     /* make the entry for the constant */
2029     nodeStat = ALLOC(NodeStat, 1);
2030     if (nodeStat == NULL) goto outOfMem;
2031     nodeStat->distance = 0;
2032     nodeStat->localRef = 1;
2033     if (st_insert(distanceTable, (char *)one, (char *)nodeStat) == ST_OUT_OF_MEM) {
2034         goto outOfMem;
2035     }
2036
2037     /* Count node distances from constant. */
2038     nodeStat = CreateBotDist(f, distanceTable);
2039     if (nodeStat == NULL) goto outOfMem;
2040
2041     /* set the distance for the decomposition points */
2042     approxDistance = (DEPTH < nodeStat->distance) ? nodeStat->distance : DEPTH;
2043     distance = nodeStat->distance;
2044
2045     if (distance < approxDistance) {
2046         /* Too small to bother. */
2047         *c1 = f;
2048         *c2 = DD_ONE(dd);
2049         cuddRef(*c1); cuddRef(*c2);
2050         stGen = st_init_gen(distanceTable);
2051         if (stGen == NULL) goto outOfMem;
2052         while(st_gen(stGen, (char **)&key, (char **)&value)) {
2053             FREE(value);
2054         }
2055         st_free_gen(stGen); stGen = NULL;
2056         st_free_table(distanceTable);
2057         return(1);
2058     }
2059
2060     /* record the maximum local reference count */
2061     maxLocalRef = 0;
2062     stGen = st_init_gen(distanceTable);
2063     if (stGen == NULL) goto outOfMem;
2064     while(st_gen(stGen, (char **)&key, (char **)&value)) {
2065         nodeStat = (NodeStat *)value;
2066         maxLocalRef = (nodeStat->localRef > maxLocalRef) ?
2067             nodeStat->localRef : maxLocalRef;
2068     }
2069     st_free_gen(stGen); stGen = NULL;
2070
2071
2072     /* Count minterms for each node. */
2073     max = pow(2.0, (double)Cudd_SupportSize(dd,f)); /* potential overflow */
2074     mintermTable = st_init_table(st_ptrcmp,st_ptrhash);
2075     if (mintermTable == NULL) goto outOfMem;
2076     minterms = CountMinterms(f, max, mintermTable, dd->err);
2077     if (minterms == -1.0) goto outOfMem;
2078
2079     lastTimeG = Cudd_Random() & 1;
2080     cacheTable = st_init_table(st_ptrcmp, st_ptrhash);
2081     if (cacheTable == NULL) goto outOfMem;
2082     ghTable = st_init_table(st_ptrcmp, st_ptrhash);
2083     if (ghTable == NULL) goto outOfMem;
2084
2085     /* Build conjuncts. */
2086     factors = BuildConjuncts(dd, f, distanceTable, cacheTable,
2087                              approxDistance, maxLocalRef, ghTable, mintermTable);
2088     if (factors == NULL) goto outOfMem;
2089
2090     /* free up tables */
2091     stGen = st_init_gen(distanceTable);
2092     if (stGen == NULL) goto outOfMem;
2093     while(st_gen(stGen, (char **)&key, (char **)&value)) {
2094         FREE(value);
2095     }
2096     st_free_gen(stGen); stGen = NULL;
2097     st_free_table(distanceTable); distanceTable = NULL;
2098     st_free_table(ghTable); ghTable = NULL;
2099
2100     stGen = st_init_gen(mintermTable);
2101     if (stGen == NULL) goto outOfMem;
2102     while(st_gen(stGen, (char **)&key, (char **)&value)) {
2103         FREE(value);
2104     }
2105     st_free_gen(stGen); stGen = NULL;
2106     st_free_table(mintermTable); mintermTable = NULL;
2107
2108     freeFactors = FactorsNotStored(factors);
2109     factors = (freeFactors) ? FactorsUncomplement(factors) : factors;
2110     if (factors != NULL) {
2111         *c1 = factors->g;
2112         *c2 = factors->h;
2113         cuddRef(*c1);
2114         cuddRef(*c2);
2115         if (freeFactors) FREE(factors);
2116
2117 #if 0
2118         if ((*c1 == f) && (!Cudd_IsConstant(f))) {
2119             assert(*c2 == one);
2120         }
2121         if ((*c2 == f) && (!Cudd_IsConstant(f))) {
2122             assert(*c1 == one);
2123         }
2124
2125         if ((*c1 != one) && (!Cudd_IsConstant(f))) {
2126             assert(!Cudd_bddLeq(dd, *c2, *c1));
2127         }
2128         if ((*c2 != one) && (!Cudd_IsConstant(f))) {
2129             assert(!Cudd_bddLeq(dd, *c1, *c2));
2130         }
2131 #endif
2132     }
2133
2134     stGen = st_init_gen(cacheTable);
2135     if (stGen == NULL) goto outOfMem;
2136     while(st_gen(stGen, (char **)&key, (char **)&value)) {
2137         ConjunctsFree(dd, (Conjuncts *)value);
2138     }
2139     st_free_gen(stGen); stGen = NULL;
2140
2141     st_free_table(cacheTable); cacheTable = NULL;
2142
2143     return(1);
2144
2145 outOfMem:
2146     if (distanceTable != NULL) {
2147         stGen = st_init_gen(distanceTable);
2148         if (stGen == NULL) goto outOfMem;
2149         while(st_gen(stGen, (char **)&key, (char **)&value)) {
2150             FREE(value);
2151         }
2152         st_free_gen(stGen); stGen = NULL;
2153         st_free_table(distanceTable); distanceTable = NULL;
2154     }
2155     if (mintermTable != NULL) {
2156         stGen = st_init_gen(mintermTable);
2157         if (stGen == NULL) goto outOfMem;
2158         while(st_gen(stGen, (char **)&key, (char **)&value)) {
2159             FREE(value);
2160         }
2161         st_free_gen(stGen); stGen = NULL;
2162         st_free_table(mintermTable); mintermTable = NULL;
2163     }
2164     if (ghTable != NULL) st_free_table(ghTable);
2165     if (cacheTable != NULL) {
2166         stGen = st_init_gen(cacheTable);
2167         if (stGen == NULL) goto outOfMem;
2168         while(st_gen(stGen, (char **)&key, (char **)&value)) {
2169             ConjunctsFree(dd, (Conjuncts *)value);
2170         }
2171         st_free_gen(stGen); stGen = NULL;
2172         st_free_table(cacheTable); cacheTable = NULL;
2173     }
2174     dd->errorCode = CUDD_MEMORY_OUT;
2175     return(0);
2176
2177 } /* end of cuddConjunctsAux */