distr/cudd/cuddEssent.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddEssent.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Functions for the detection of essential variables.]
   8
   9   Description [External procedures included in this file:
  10                 <ul>
  11                 <li> Cudd_FindEssential()
  12                 <li> Cudd_bddIsVarEssential()
  13                 <li> Cudd_FindTwoLiteralClauses()
  14                 <li> Cudd_ReadIthClause()
  15                 <li> Cudd_PrintTwoLiteralClauses()
  16                 <li> Cudd_tlcInfoFree()
  17                 </ul>
  18         Static procedures included in this module:
  19                 <ul>
  20                 <li> ddFindEssentialRecur()
  21                 <li> ddFindTwoLiteralClausesRecur()
  22                 <li> computeClauses()
  23                 <li> computeClausesWithUniverse()
  24                 <li> emptyClauseSet()
  25                 <li> sentinelp()
  26                 <li> equalp()
  27                 <li> beforep()
  28                 <li> oneliteralp()
  29                 <li> impliedp()
  30                 <li> bitVectorAlloc()
  31                 <li> bitVectorClear()
  32                 <li> bitVectorFree()
  33                 <li> bitVectorRead()
  34                 <li> bitVectorSet()
  35                 <li> tlcInfoAlloc()
  36                 </ul>]
  37
  38   Author      [Fabio Somenzi]
  39
  40   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  41
  42   All rights reserved.
  43
  44   Redistribution and use in source and binary forms, with or without
  45   modification, are permitted provided that the following conditions
  46   are met:
  47
  48   Redistributions of source code must retain the above copyright
  49   notice, this list of conditions and the following disclaimer.
  50
  51   Redistributions in binary form must reproduce the above copyright
  52   notice, this list of conditions and the following disclaimer in the
  53   documentation and/or other materials provided with the distribution.
  54
  55   Neither the name of the University of Colorado nor the names of its
  56   contributors may be used to endorse or promote products derived from
  57   this software without specific prior written permission.
  58
  59   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  60   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  61   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  62   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  63   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  64   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  65   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  66   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  67   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  68   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  69   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  70   POSSIBILITY OF SUCH DAMAGE.]
  71
  72 ******************************************************************************/
  73
  74 #include "util.h"
  75 #include "cuddInt.h"
  76
  77 /*---------------------------------------------------------------------------*/
  78 /* Constant declarations                                                     */
  79 /*---------------------------------------------------------------------------*/
  80
  81 /* These definitions are for the bit vectors. */
  82 #if SIZEOF_LONG == 8
  83 #define BPL 64
  84 #define LOGBPL 6
  85 #else
  86 #define BPL 32
  87 #define LOGBPL 5
  88 #endif
  89
  90 /*---------------------------------------------------------------------------*/
  91 /* Stucture declarations                                                     */
  92 /*---------------------------------------------------------------------------*/
  93
  94 /* This structure holds the set of clauses for a node.  Each clause consists
  95 ** of two literals.  For one-literal clauses, the second lietral is FALSE.
  96 ** Each literal is composed of a variable and a phase.  A variable is a node
  97 ** index, and requires sizeof(DdHalfWord) bytes.  The constant literals use
  98 ** CUDD_MAXINDEX as variable indicator.  Each phase is a bit: 0 for positive
  99 ** phase, and 1 for negative phase.
 100 ** Variables and phases are stored separately for the sake of compactness.
 101 ** The variables are stored in an array of DdHalfWord's terminated by a
 102 ** sentinel (a pair of zeroes).  The phases are stored in a bit vector.
 103 ** The cnt field holds, at the end, the number of clauses.
 104 ** The clauses of the set are kept sorted.  For each clause, the first literal
 105 ** is the one of least index.  So, the clause with literals +2 and -4 is stored
 106 ** as (+2,-4).  A one-literal clause with literal +3 is stored as
 107 ** (+3,-CUDD_MAXINDEX).  Clauses are sorted in decreasing order as follows:
 108 **      (+5,-7)
 109 **      (+5,+6)
 110 **      (-5,+7)
 111 **      (-4,FALSE)
 112 **      (-4,+8)
 113 **      ...
 114 ** That is, one first looks at the variable of the first literal, then at the
 115 ** phase of the first litral, then at the variable of the second literal,
 116 ** and finally at the phase of the second literal.
 117 */
 118 struct DdTlcInfo {
 119     DdHalfWord *vars;
 120     long *phases;
 121     DdHalfWord cnt;
 122 };
 123
 124 /* This structure is for temporary representation of sets of clauses.  It is
 125 ** meant to be used in link lists, when the number of clauses is not yet
 126 ** known. The encoding of a clause is the same as in DdTlcInfo, though
 127 ** the phase information is not stored in a bit array. */
 128 struct TlClause {
 129     DdHalfWord v1, v2;
 130     short p1, p2;
 131     struct TlClause *next;
 132 };
 133
 134 /*---------------------------------------------------------------------------*/
 135 /* Type declarations                                                         */
 136 /*---------------------------------------------------------------------------*/
 137
 138 typedef long BitVector;
 139 typedef struct TlClause TlClause;
 140
 141 /*---------------------------------------------------------------------------*/
 142 /* Variable declarations                                                     */
 143 /*---------------------------------------------------------------------------*/
 144
 145 #ifndef lint
 146 static char rcsid[] DD_UNUSED = "$Id: cuddEssent.c,v 1.24 2009/02/21 18:24:10 fabio Exp $";
 147 #endif
 148
 149 static BitVector *Tolv;
 150 static BitVector *Tolp;
 151 static BitVector *Eolv;
 152 static BitVector *Eolp;
 153
 154 /*---------------------------------------------------------------------------*/
 155 /* Macro declarations                                                        */
 156 /*---------------------------------------------------------------------------*/
 157
 158 /**AutomaticStart*************************************************************/
 159
 160 /*---------------------------------------------------------------------------*/
 161 /* Static function prototypes                                                */
 162 /*---------------------------------------------------------------------------*/
 163
 164 static DdNode * ddFindEssentialRecur (DdManager *dd, DdNode *f);
 165 static DdTlcInfo * ddFindTwoLiteralClausesRecur (DdManager * dd, DdNode * f, st_table *table);
 166 static DdTlcInfo * computeClauses (DdTlcInfo *Tres, DdTlcInfo *Eres, DdHalfWord label, int size);
 167 static DdTlcInfo * computeClausesWithUniverse (DdTlcInfo *Cres, DdHalfWord label, short phase);
 168 static DdTlcInfo * emptyClauseSet (void);
 169 static int sentinelp (DdHalfWord var1, DdHalfWord var2);
 170 static int equalp (DdHalfWord var1a, short phase1a, DdHalfWord var1b, short phase1b, DdHalfWord var2a, short phase2a, DdHalfWord var2b, short phase2b);
 171 static int beforep (DdHalfWord var1a, short phase1a, DdHalfWord var1b, short phase1b, DdHalfWord var2a, short phase2a, DdHalfWord var2b, short phase2b);
 172 static int oneliteralp (DdHalfWord var);
 173 static int impliedp (DdHalfWord var1, short phase1, DdHalfWord var2, short phase2, BitVector *olv, BitVector *olp);
 174 static BitVector * bitVectorAlloc (int size);
 175 DD_INLINE static void bitVectorClear (BitVector *vector, int size);
 176 static void bitVectorFree (BitVector *vector);
 177 DD_INLINE static short bitVectorRead (BitVector *vector, int i);
 178 DD_INLINE static void bitVectorSet (BitVector * vector, int i, short val);
 179 static DdTlcInfo * tlcInfoAlloc (void);
 180
 181 /**AutomaticEnd***************************************************************/
 182
 183
 184 /*---------------------------------------------------------------------------*/
 185 /* Definition of exported functions                                          */
 186 /*---------------------------------------------------------------------------*/
 187
 188
 189 /**Function********************************************************************
 190
 191   Synopsis    [Finds the essential variables of a DD.]
 192
 193   Description [Returns the cube of the essential variables. A positive
 194   literal means that the variable must be set to 1 for the function to be
 195   1. A negative literal means that the variable must be set to 0 for the
 196   function to be 1. Returns a pointer to the cube BDD if successful;
 197   NULL otherwise.]
 198
 199   SideEffects [None]
 200
 201   SeeAlso     [Cudd_bddIsVarEssential]
 202
 203 ******************************************************************************/
 204 DdNode *
 205 Cudd_FindEssential(
 206   DdManager * dd,
 207   DdNode * f)
 208 {
 209     DdNode *res;
 210
 211     do {
 212         dd->reordered = 0;
 213         res = ddFindEssentialRecur(dd,f);
 214     } while (dd->reordered == 1);
 215     return(res);
 216
 217 } /* end of Cudd_FindEssential */
 218
 219
 220 /**Function********************************************************************
 221
 222   Synopsis    [Determines whether a given variable is essential with a
 223   given phase in a BDD.]
 224
 225   Description [Determines whether a given variable is essential with a
 226   given phase in a BDD. Uses Cudd_bddIteConstant. Returns 1 if phase == 1
 227   and f-->x_id, or if phase == 0 and f-->x_id'.]
 228
 229   SideEffects [None]
 230
 231   SeeAlso     [Cudd_FindEssential]
 232
 233 ******************************************************************************/
 234 int
 235 Cudd_bddIsVarEssential(
 236   DdManager * manager,
 237   DdNode * f,
 238   int  id,
 239   int  phase)
 240 {
 241     DdNode      *var;
 242     int         res;
 243
 244     var = Cudd_bddIthVar(manager, id);
 245
 246     var = Cudd_NotCond(var,phase == 0);
 247
 248     res = Cudd_bddLeq(manager, f, var);
 249
 250     return(res);
 251
 252 } /* end of Cudd_bddIsVarEssential */
 253
 254
 255 /**Function********************************************************************
 256
 257   Synopsis    [Finds the two literal clauses of a DD.]
 258
 259   Description [Returns the one- and two-literal clauses of a DD.
 260   Returns a pointer to the structure holding the clauses if
 261   successful; NULL otherwise.  For a constant DD, the empty set of clauses
 262   is returned.  This is obviously correct for a non-zero constant.  For the
 263   constant zero, it is based on the assumption that only those clauses
 264   containing variables in the support of the function are considered.  Since
 265   the support of a constant function is empty, no clauses are returned.]
 266
 267   SideEffects [None]
 268
 269   SeeAlso     [Cudd_FindEssential]
 270
 271 ******************************************************************************/
 272 DdTlcInfo *
 273 Cudd_FindTwoLiteralClauses(
 274   DdManager * dd,
 275   DdNode * f)
 276 {
 277     DdTlcInfo *res;
 278     st_table *table;
 279     st_generator *gen;
 280     DdTlcInfo *tlc;
 281     DdNode *node;
 282     int size = dd->size;
 283
 284     if (Cudd_IsConstant(f)) {
 285         res = emptyClauseSet();
 286         return(res);
 287     }
 288     table = st_init_table(st_ptrcmp,st_ptrhash);
 289     if (table == NULL) return(NULL);
 290     Tolv = bitVectorAlloc(size);
 291     if (Tolv == NULL) {
 292         st_free_table(table);
 293         return(NULL);
 294     }
 295     Tolp = bitVectorAlloc(size);
 296     if (Tolp == NULL) {
 297         st_free_table(table);
 298         bitVectorFree(Tolv);
 299         return(NULL);
 300     }
 301     Eolv = bitVectorAlloc(size);
 302     if (Eolv == NULL) {
 303         st_free_table(table);
 304         bitVectorFree(Tolv);
 305         bitVectorFree(Tolp);
 306         return(NULL);
 307     }
 308     Eolp = bitVectorAlloc(size);
 309     if (Eolp == NULL) {
 310         st_free_table(table);
 311         bitVectorFree(Tolv);
 312         bitVectorFree(Tolp);
 313         bitVectorFree(Eolv);
 314         return(NULL);
 315     }
 316
 317     res = ddFindTwoLiteralClausesRecur(dd,f,table);
 318     /* Dispose of table contents and free table. */
 319     st_foreach_item(table, gen, &node, &tlc) {
 320         if (node != f) {
 321             Cudd_tlcInfoFree(tlc);
 322         }
 323     }
 324     st_free_table(table);
 325     bitVectorFree(Tolv);
 326     bitVectorFree(Tolp);
 327     bitVectorFree(Eolv);
 328     bitVectorFree(Eolp);
 329
 330     if (res != NULL) {
 331         int i;
 332         for (i = 0; !sentinelp(res->vars[i], res->vars[i+1]); i += 2);
 333         res->cnt = i >> 1;
 334     }
 335
 336     return(res);
 337
 338 } /* end of Cudd_FindTwoLiteralClauses */
 339
 340
 341 /**Function********************************************************************
 342
 343   Synopsis    [Accesses the i-th clause of a DD.]
 344
 345   Description [Accesses the i-th clause of a DD given the clause set which
 346   must be already computed.  Returns 1 if successful; 0 if i is out of range,
 347   or in case of error.]
 348
 349   SideEffects [the four components of a clause are returned as side effects.]
 350
 351   SeeAlso     [Cudd_FindTwoLiteralClauses]
 352
 353 ******************************************************************************/
 354 int
 355 Cudd_ReadIthClause(
 356   DdTlcInfo * tlc,
 357   int i,
 358   DdHalfWord *var1,
 359   DdHalfWord *var2,
 360   int *phase1,
 361   int *phase2)
 362 {
 363     if (tlc == NULL) return(0);
 364     if (tlc->vars == NULL || tlc->phases == NULL) return(0);
 365     if (i < 0 || (unsigned) i >= tlc->cnt) return(0);
 366     *var1 = tlc->vars[2*i];
 367     *var2 = tlc->vars[2*i+1];
 368     *phase1 = (int) bitVectorRead(tlc->phases, 2*i);
 369     *phase2 = (int) bitVectorRead(tlc->phases, 2*i+1);
 370     return(1);
 371
 372 } /* end of Cudd_ReadIthClause */
 373
 374
 375 /**Function********************************************************************
 376
 377   Synopsis    [Prints the two literal clauses of a DD.]
 378
 379   Description [Prints the one- and two-literal clauses. Returns 1 if
 380   successful; 0 otherwise.  The argument "names" can be NULL, in which case
 381   the variable indices are printed.]
 382
 383   SideEffects [None]
 384
 385   SeeAlso     [Cudd_FindTwoLiteralClauses]
 386
 387 ******************************************************************************/
 388 int
 389 Cudd_PrintTwoLiteralClauses(
 390   DdManager * dd,
 391   DdNode * f,
 392   char **names,
 393   FILE *fp)
 394 {
 395     DdHalfWord *vars;
 396     BitVector *phases;
 397     int i;
 398     DdTlcInfo *res = Cudd_FindTwoLiteralClauses(dd, f);
 399     FILE *ifp = fp == NULL ? dd->out : fp;
 400
 401     if (res == NULL) return(0);
 402     vars = res->vars;
 403     phases = res->phases;
 404     for (i = 0; !sentinelp(vars[i], vars[i+1]); i += 2) {
 405         if (names != NULL) {
 406             if (vars[i+1] == CUDD_MAXINDEX) {
 407                 (void) fprintf(ifp, "%s%s\n",
 408                                bitVectorRead(phases, i) ? "~" : " ",
 409                                names[vars[i]]);
 410             } else {
 411                 (void) fprintf(ifp, "%s%s | %s%s\n",
 412                                bitVectorRead(phases, i) ? "~" : " ",
 413                                names[vars[i]],
 414                                bitVectorRead(phases, i+1) ? "~" : " ",
 415                                names[vars[i+1]]);
 416             }
 417         } else {
 418             if (vars[i+1] == CUDD_MAXINDEX) {
 419                 (void) fprintf(ifp, "%s%d\n",
 420                                bitVectorRead(phases, i) ? "~" : " ",
 421                                (int) vars[i]);
 422             } else {
 423                 (void) fprintf(ifp, "%s%d | %s%d\n",
 424                                bitVectorRead(phases, i) ? "~" : " ",
 425                                (int) vars[i],
 426                                bitVectorRead(phases, i+1) ? "~" : " ",
 427                                (int) vars[i+1]);
 428             }
 429         }
 430     }
 431     Cudd_tlcInfoFree(res);
 432
 433     return(1);
 434
 435 } /* end of Cudd_PrintTwoLiteralClauses */
 436
 437
 438 /**Function********************************************************************
 439
 440   Synopsis    [Frees a DdTlcInfo Structure.]
 441
 442   Description [Frees a DdTlcInfo Structure as well as the memory pointed
 443   by it.]
 444
 445   SideEffects [None]
 446
 447   SeeAlso     []
 448
 449 ******************************************************************************/
 450 void
 451 Cudd_tlcInfoFree(
 452   DdTlcInfo * t)
 453 {
 454     if (t->vars != NULL) FREE(t->vars);
 455     if (t->phases != NULL) FREE(t->phases);
 456     FREE(t);
 457
 458 } /* end of Cudd_tlcInfoFree */
 459
 460
 461 /*---------------------------------------------------------------------------*/
 462 /* Definition of internal functions                                          */
 463 /*---------------------------------------------------------------------------*/
 464
 465
 466 /*---------------------------------------------------------------------------*/
 467 /* Definition of static functions                                            */
 468 /*---------------------------------------------------------------------------*/
 469
 470
 471 /**Function********************************************************************
 472
 473   Synopsis    [Implements the recursive step of Cudd_FindEssential.]
 474
 475   Description [Implements the recursive step of Cudd_FindEssential.
 476   Returns a pointer to the cube BDD if successful; NULL otherwise.]
 477
 478   SideEffects [None]
 479
 480 ******************************************************************************/
 481 static DdNode *
 482 ddFindEssentialRecur(
 483   DdManager * dd,
 484   DdNode * f)
 485 {
 486     DdNode      *T, *E, *F;
 487     DdNode      *essT, *essE, *res;
 488     int         index;
 489     DdNode      *one, *lzero, *azero;
 490
 491     one = DD_ONE(dd);
 492     F = Cudd_Regular(f);
 493     /* If f is constant the set of essential variables is empty. */
 494     if (cuddIsConstant(F)) return(one);
 495
 496     res = cuddCacheLookup1(dd,Cudd_FindEssential,f);
 497     if (res != NULL) {
 498         return(res);
 499     }
 500
 501     lzero = Cudd_Not(one);
 502     azero = DD_ZERO(dd);
 503     /* Find cofactors: here f is non-constant. */
 504     T = cuddT(F);
 505     E = cuddE(F);
 506     if (Cudd_IsComplement(f)) {
 507         T = Cudd_Not(T); E = Cudd_Not(E);
 508     }
 509
 510     index = F->index;
 511     if (Cudd_IsConstant(T) && T != lzero && T != azero) {
 512         /* if E is zero, index is essential, otherwise there are no
 513         ** essentials, because index is not essential and no other variable
 514         ** can be, since setting index = 1 makes the function constant and
 515         ** different from 0.
 516         */
 517         if (E == lzero || E == azero) {
 518             res = dd->vars[index];
 519         } else {
 520             res = one;
 521         }
 522     } else if (T == lzero || T == azero) {
 523         if (Cudd_IsConstant(E)) { /* E cannot be zero here */
 524             res = Cudd_Not(dd->vars[index]);
 525         } else { /* E == non-constant */
 526             /* find essentials in the else branch */
 527             essE = ddFindEssentialRecur(dd,E);
 528             if (essE == NULL) {
 529                 return(NULL);
 530             }
 531             cuddRef(essE);
 532
 533             /* add index to the set with negative phase */
 534             res = cuddUniqueInter(dd,index,one,Cudd_Not(essE));
 535             if (res == NULL) {
 536                 Cudd_RecursiveDeref(dd,essE);
 537                 return(NULL);
 538             }
 539             res = Cudd_Not(res);
 540             cuddDeref(essE);
 541         }
 542     } else { /* T == non-const */
 543         if (E == lzero || E == azero) {
 544             /* find essentials in the then branch */
 545             essT = ddFindEssentialRecur(dd,T);
 546             if (essT == NULL) {
 547                 return(NULL);
 548             }
 549             cuddRef(essT);
 550
 551             /* add index to the set with positive phase */
 552             /* use And because essT may be complemented */
 553             res = cuddBddAndRecur(dd,dd->vars[index],essT);
 554             if (res == NULL) {
 555                 Cudd_RecursiveDeref(dd,essT);
 556                 return(NULL);
 557             }
 558             cuddDeref(essT);
 559         } else if (!Cudd_IsConstant(E)) {
 560             /* if E is a non-zero constant there are no essentials
 561             ** because T is non-constant.
 562             */
 563             essT = ddFindEssentialRecur(dd,T);
 564             if (essT == NULL) {
 565                 return(NULL);
 566             }
 567             if (essT == one) {
 568                 res = one;
 569             } else {
 570                 cuddRef(essT);
 571                 essE = ddFindEssentialRecur(dd,E);
 572                 if (essE == NULL) {
 573                     Cudd_RecursiveDeref(dd,essT);
 574                     return(NULL);
 575                 }
 576                 cuddRef(essE);
 577
 578                 /* res = intersection(essT, essE) */
 579                 res = cuddBddLiteralSetIntersectionRecur(dd,essT,essE);
 580                 if (res == NULL) {
 581                     Cudd_RecursiveDeref(dd,essT);
 582                     Cudd_RecursiveDeref(dd,essE);
 583                     return(NULL);
 584                 }
 585                 cuddRef(res);
 586                 Cudd_RecursiveDeref(dd,essT);
 587                 Cudd_RecursiveDeref(dd,essE);
 588                 cuddDeref(res);
 589             }
 590         } else {        /* E is a non-zero constant */
 591             res = one;
 592         }
 593     }
 594
 595     cuddCacheInsert1(dd,Cudd_FindEssential, f, res);
 596     return(res);
 597
 598 } /* end of ddFindEssentialRecur */
 599
 600
 601 /**Function********************************************************************
 602
 603   Synopsis    [Implements the recursive step of Cudd_FindTwoLiteralClauses.]
 604
 605   Description [Implements the recursive step of
 606   Cudd_FindTwoLiteralClauses.  The DD node is assumed to be not
 607   constant.  Returns a pointer to a set of clauses if successful; NULL
 608   otherwise.]
 609
 610   SideEffects [None]
 611
 612   SeeAlso     [Cudd_FindTwoLiteralClauses]
 613
 614 ******************************************************************************/
 615 static DdTlcInfo *
 616 ddFindTwoLiteralClausesRecur(
 617   DdManager * dd,
 618   DdNode * f,
 619   st_table *table)
 620 {
 621     DdNode *T, *E, *F;
 622     DdNode *one, *lzero, *azero;
 623     DdTlcInfo *res, *Tres, *Eres;
 624     DdHalfWord index;
 625
 626     F = Cudd_Regular(f);
 627
 628     assert(!cuddIsConstant(F));
 629
 630     /* Check computed table.  Separate entries are necessary for
 631     ** a node and its complement.  We should update the counter here. */
 632     if (st_lookup(table, f, &res)) {
 633         return(res);
 634     }
 635
 636     /* Easy access to the constants for BDDs and ADDs. */
 637     one = DD_ONE(dd);
 638     lzero = Cudd_Not(one);
 639     azero = DD_ZERO(dd);
 640
 641     /* Find cofactors and variable labeling the top node. */
 642     T = cuddT(F); E = cuddE(F);
 643     if (Cudd_IsComplement(f)) {
 644         T = Cudd_Not(T); E = Cudd_Not(E);
 645     }
 646     index = F->index;
 647
 648     if (Cudd_IsConstant(T) && T != lzero && T != azero) {
 649         /* T is a non-zero constant.  If E is zero, then this node's index
 650         ** is a one-literal clause.  Otherwise, if E is a non-zero
 651         ** constant, there are no clauses for this node.  Finally,
 652         ** if E is not constant, we recursively compute its clauses, and then
 653         ** merge using the empty set for T. */
 654         if (E == lzero || E == azero) {
 655             /* Create the clause (index + 0). */
 656             res = tlcInfoAlloc();
 657             if (res == NULL) return(NULL);
 658             res->vars = ALLOC(DdHalfWord,4);
 659             if (res->vars == NULL) {
 660                 FREE(res);
 661                 return(NULL);
 662             }
 663             res->phases = bitVectorAlloc(2);
 664             if (res->phases == NULL) {
 665                 FREE(res->vars);
 666                 FREE(res);
 667                 return(NULL);
 668             }
 669             res->vars[0] = index;
 670             res->vars[1] = CUDD_MAXINDEX;
 671             res->vars[2] = 0;
 672             res->vars[3] = 0;
 673             bitVectorSet(res->phases, 0, 0); /* positive phase */
 674             bitVectorSet(res->phases, 1, 1); /* negative phase */
 675         } else if (Cudd_IsConstant(E)) {
 676             /* If E is a non-zero constant, no clauses. */
 677             res = emptyClauseSet();
 678         } else {
 679             /* E is non-constant */
 680             Tres = emptyClauseSet();
 681             if (Tres == NULL) return(NULL);
 682             Eres = ddFindTwoLiteralClausesRecur(dd, E, table);
 683             if (Eres == NULL) {
 684                 Cudd_tlcInfoFree(Tres);
 685                 return(NULL);
 686             }
 687             res = computeClauses(Tres, Eres, index, dd->size);
 688             Cudd_tlcInfoFree(Tres);
 689         }
 690     } else if (T == lzero || T == azero) {
 691         /* T is zero.  If E is a non-zero constant, then the
 692         ** complement of this node's index is a one-literal clause.
 693         ** Otherwise, if E is not constant, we recursively compute its
 694         ** clauses, and then merge using the universal set for T. */
 695         if (Cudd_IsConstant(E)) { /* E cannot be zero here */
 696             /* Create the clause (!index + 0). */
 697             res = tlcInfoAlloc();
 698             if (res == NULL) return(NULL);
 699             res->vars = ALLOC(DdHalfWord,4);
 700             if (res->vars == NULL) {
 701                 FREE(res);
 702                 return(NULL);
 703             }
 704             res->phases = bitVectorAlloc(2);
 705             if (res->phases == NULL) {
 706                 FREE(res->vars);
 707                 FREE(res);
 708                 return(NULL);
 709             }
 710             res->vars[0] = index;
 711             res->vars[1] = CUDD_MAXINDEX;
 712             res->vars[2] = 0;
 713             res->vars[3] = 0;
 714             bitVectorSet(res->phases, 0, 1); /* negative phase */
 715             bitVectorSet(res->phases, 1, 1); /* negative phase */
 716         } else { /* E == non-constant */
 717             Eres = ddFindTwoLiteralClausesRecur(dd, E, table);
 718             if (Eres == NULL) return(NULL);
 719             res = computeClausesWithUniverse(Eres, index, 1);
 720         }
 721     } else { /* T == non-const */
 722         Tres = ddFindTwoLiteralClausesRecur(dd, T, table);
 723         if (Tres == NULL) return(NULL);
 724         if (Cudd_IsConstant(E)) {
 725             if (E == lzero || E == azero) {
 726                 res = computeClausesWithUniverse(Tres, index, 0);
 727             } else {
 728                 Eres = emptyClauseSet();
 729                 if (Eres == NULL) return(NULL);
 730                 res = computeClauses(Tres, Eres, index, dd->size);
 731                 Cudd_tlcInfoFree(Eres);
 732             }
 733         } else {
 734             Eres = ddFindTwoLiteralClausesRecur(dd, E, table);
 735             if (Eres == NULL) return(NULL);
 736             res = computeClauses(Tres, Eres, index, dd->size);
 737         }
 738     }
 739
 740     /* Cache results. */
 741     if (st_add_direct(table, (char *)f, (char *)res) == ST_OUT_OF_MEM) {
 742         FREE(res);
 743         return(NULL);
 744     }
 745     return(res);
 746
 747 } /* end of ddFindTwoLiteralClausesRecur */
 748
 749
 750 /**Function********************************************************************
 751
 752   Synopsis    [Computes the two-literal clauses for a node.]
 753
 754   Description [Computes the two-literal clauses for a node given the
 755   clauses for its children and the label of the node.  Returns a
 756   pointer to a TclInfo structure if successful; NULL otherwise.]
 757
 758   SideEffects [None]
 759
 760   SeeAlso     [computeClausesWithUniverse]
 761
 762 ******************************************************************************/
 763 static DdTlcInfo *
 764 computeClauses(
 765   DdTlcInfo *Tres /* list of clauses for T child */,
 766   DdTlcInfo *Eres /* list of clauses for E child */,
 767   DdHalfWord label /* variable labeling the current node */,
 768   int size /* number of variables in the manager */)
 769 {
 770     DdHalfWord *Tcv = Tres->vars; /* variables of clauses for the T child */
 771     BitVector *Tcp = Tres->phases; /* phases of clauses for the T child */
 772     DdHalfWord *Ecv = Eres->vars; /* variables of clauses for the E child */
 773     BitVector *Ecp = Eres->phases; /* phases of clauses for the E child */
 774     DdHalfWord *Vcv = NULL; /* pointer to variables of the clauses for v */
 775     BitVector *Vcp = NULL; /* pointer to phases of the clauses for v */
 776     DdTlcInfo *res = NULL; /* the set of clauses to be returned */
 777     int pt = 0; /* index in the list of clauses of T */
 778     int pe = 0; /* index in the list of clauses of E */
 779     int cv = 0; /* counter of the clauses for this node */
 780     TlClause *iclauses = NULL; /* list of inherited clauses */
 781     TlClause *tclauses = NULL; /* list of 1-literal clauses of T */
 782     TlClause *eclauses = NULL; /* list of 1-literal clauses of E */
 783     TlClause *nclauses = NULL; /* list of new (non-inherited) clauses */
 784     TlClause *lnclause = NULL; /* pointer to last new clause */
 785     TlClause *newclause; /* temporary pointer to new clauses */
 786
 787     /* Initialize sets of one-literal clauses.  The one-literal clauses
 788     ** are stored redundantly.  These sets allow constant-time lookup, which
 789     ** we need when we check for implication of a two-literal clause by a
 790     ** one-literal clause.  The linked lists allow fast sequential
 791     ** processing. */
 792     bitVectorClear(Tolv, size);
 793     bitVectorClear(Tolp, size);
 794     bitVectorClear(Eolv, size);
 795     bitVectorClear(Eolp, size);
 796
 797     /* Initialize result structure. */
 798     res = tlcInfoAlloc();
 799     if (res == NULL) goto cleanup;
 800
 801     /* Scan the two input list.  Extract inherited two-literal clauses
 802     ** and set aside one-literal clauses from each list.  The incoming lists
 803     ** are sorted in the order defined by beforep.  The three linked list
 804     ** produced by this loop are sorted in the reverse order because we
 805     ** always append to the front of the lists.
 806     ** The inherited clauses are those clauses (both one- and two-literal)
 807     ** that are common to both children; and the two-literal clauses of
 808     ** one child that are implied by a one-literal clause of the other
 809     ** child. */
 810     while (!sentinelp(Tcv[pt], Tcv[pt+1]) || !sentinelp(Ecv[pe], Ecv[pe+1])) {
 811         if (equalp(Tcv[pt], bitVectorRead(Tcp, pt),
 812                    Tcv[pt+1], bitVectorRead(Tcp, pt+1),
 813                    Ecv[pe], bitVectorRead(Ecp, pe),
 814                    Ecv[pe+1], bitVectorRead(Ecp, pe+1))) {
 815             /* Add clause to inherited list. */
 816             newclause = ALLOC(TlClause,1);
 817             if (newclause == NULL) goto cleanup;
 818             newclause->v1 = Tcv[pt];
 819             newclause->v2 = Tcv[pt+1];
 820             newclause->p1 = bitVectorRead(Tcp, pt);
 821             newclause->p2 = bitVectorRead(Tcp, pt+1);
 822             newclause->next = iclauses;
 823             iclauses = newclause;
 824             pt += 2; pe += 2; cv++;
 825         } else if (beforep(Tcv[pt], bitVectorRead(Tcp, pt),
 826                    Tcv[pt+1], bitVectorRead(Tcp, pt+1),
 827                    Ecv[pe], bitVectorRead(Ecp, pe),
 828                    Ecv[pe+1], bitVectorRead(Ecp, pe+1))) {
 829             if (oneliteralp(Tcv[pt+1])) {
 830                 /* Add this one-literal clause to the T set. */
 831                 newclause = ALLOC(TlClause,1);
 832                 if (newclause == NULL) goto cleanup;
 833                 newclause->v1 = Tcv[pt];
 834                 newclause->v2 = CUDD_MAXINDEX;
 835                 newclause->p1 = bitVectorRead(Tcp, pt);
 836                 newclause->p2 = 1;
 837                 newclause->next = tclauses;
 838                 tclauses = newclause;
 839                 bitVectorSet(Tolv, Tcv[pt], 1);
 840                 bitVectorSet(Tolp, Tcv[pt], bitVectorRead(Tcp, pt));
 841             } else {
 842                 if (impliedp(Tcv[pt], bitVectorRead(Tcp, pt),
 843                              Tcv[pt+1], bitVectorRead(Tcp, pt+1),
 844                              Eolv, Eolp)) {
 845                     /* Add clause to inherited list. */
 846                     newclause = ALLOC(TlClause,1);
 847                     if (newclause == NULL) goto cleanup;
 848                     newclause->v1 = Tcv[pt];
 849                     newclause->v2 = Tcv[pt+1];
 850                     newclause->p1 = bitVectorRead(Tcp, pt);
 851                     newclause->p2 = bitVectorRead(Tcp, pt+1);
 852                     newclause->next = iclauses;
 853                     iclauses = newclause;
 854                     cv++;
 855                 }
 856             }
 857             pt += 2;
 858         } else { /* !beforep() */
 859             if (oneliteralp(Ecv[pe+1])) {
 860                 /* Add this one-literal clause to the E set. */
 861                 newclause = ALLOC(TlClause,1);
 862                 if (newclause == NULL) goto cleanup;
 863                 newclause->v1 = Ecv[pe];
 864                 newclause->v2 = CUDD_MAXINDEX;
 865                 newclause->p1 = bitVectorRead(Ecp, pe);
 866                 newclause->p2 = 1;
 867                 newclause->next = eclauses;
 868                 eclauses = newclause;
 869                 bitVectorSet(Eolv, Ecv[pe], 1);
 870                 bitVectorSet(Eolp, Ecv[pe], bitVectorRead(Ecp, pe));
 871             } else {
 872                 if (impliedp(Ecv[pe], bitVectorRead(Ecp, pe),
 873                              Ecv[pe+1], bitVectorRead(Ecp, pe+1),
 874                              Tolv, Tolp)) {
 875                     /* Add clause to inherited list. */
 876                     newclause = ALLOC(TlClause,1);
 877                     if (newclause == NULL) goto cleanup;
 878                     newclause->v1 = Ecv[pe];
 879                     newclause->v2 = Ecv[pe+1];
 880                     newclause->p1 = bitVectorRead(Ecp, pe);
 881                     newclause->p2 = bitVectorRead(Ecp, pe+1);
 882                     newclause->next = iclauses;
 883                     iclauses = newclause;
 884                     cv++;
 885                 }
 886             }
 887             pe += 2;
 888         }
 889     }
 890
 891     /* Add one-literal clauses for the label variable to the front of
 892     ** the two lists. */
 893     newclause = ALLOC(TlClause,1);
 894     if (newclause == NULL) goto cleanup;
 895     newclause->v1 = label;
 896     newclause->v2 = CUDD_MAXINDEX;
 897     newclause->p1 = 0;
 898     newclause->p2 = 1;
 899     newclause->next = tclauses;
 900     tclauses = newclause;
 901     newclause = ALLOC(TlClause,1);
 902     if (newclause == NULL) goto cleanup;
 903     newclause->v1 = label;
 904     newclause->v2 = CUDD_MAXINDEX;
 905     newclause->p1 = 1;
 906     newclause->p2 = 1;
 907     newclause->next = eclauses;
 908     eclauses = newclause;
 909
 910     /* Produce the non-inherited clauses.  We preserve the "reverse"
 911     ** order of the two input lists by appending to the end of the
 912     ** list.  In this way, iclauses and nclauses are consistent. */
 913     while (tclauses != NULL && eclauses != NULL) {
 914         if (beforep(eclauses->v1, eclauses->p1, eclauses->v2, eclauses->p2,
 915                     tclauses->v1, tclauses->p1, tclauses->v2, tclauses->p2)) {
 916             TlClause *nextclause = tclauses->next;
 917             TlClause *otherclauses = eclauses;
 918             while (otherclauses != NULL) {
 919                 if (tclauses->v1 != otherclauses->v1) {
 920                     newclause = ALLOC(TlClause,1);
 921                     if (newclause == NULL) goto cleanup;
 922                     newclause->v1 = tclauses->v1;
 923                     newclause->v2 = otherclauses->v1;
 924                     newclause->p1 = tclauses->p1;
 925                     newclause->p2 = otherclauses->p1;
 926                     newclause->next = NULL;
 927                     if (nclauses == NULL) {
 928                         nclauses = newclause;
 929                         lnclause = newclause;
 930                     } else {
 931                         lnclause->next = newclause;
 932                         lnclause = newclause;
 933                     }
 934                     cv++;
 935                 }
 936                 otherclauses = otherclauses->next;
 937             }
 938             FREE(tclauses);
 939             tclauses = nextclause;
 940         } else {
 941             TlClause *nextclause = eclauses->next;
 942             TlClause *otherclauses = tclauses;
 943             while (otherclauses != NULL) {
 944                 if (eclauses->v1 != otherclauses->v1) {
 945                     newclause = ALLOC(TlClause,1);
 946                     if (newclause == NULL) goto cleanup;
 947                     newclause->v1 = eclauses->v1;
 948                     newclause->v2 = otherclauses->v1;
 949                     newclause->p1 = eclauses->p1;
 950                     newclause->p2 = otherclauses->p1;
 951                     newclause->next = NULL;
 952                     if (nclauses == NULL) {
 953                         nclauses = newclause;
 954                         lnclause = newclause;
 955                     } else {
 956                         lnclause->next = newclause;
 957                         lnclause = newclause;
 958                     }
 959                     cv++;
 960                 }
 961                 otherclauses = otherclauses->next;
 962             }
 963             FREE(eclauses);
 964             eclauses = nextclause;
 965         }
 966     }
 967     while (tclauses != NULL) {
 968         TlClause *nextclause = tclauses->next;
 969         FREE(tclauses);
 970         tclauses = nextclause;
 971     }
 972     while (eclauses != NULL) {
 973         TlClause *nextclause = eclauses->next;
 974         FREE(eclauses);
 975         eclauses = nextclause;
 976     }
 977
 978     /* Merge inherited and non-inherited clauses.  Now that we know the
 979     ** total number, we allocate the arrays, and we fill them bottom-up
 980     ** to restore the proper ordering. */
 981     Vcv = ALLOC(DdHalfWord, 2*(cv+1));
 982     if (Vcv == NULL) goto cleanup;
 983     if (cv > 0) {
 984         Vcp = bitVectorAlloc(2*cv);
 985         if (Vcp == NULL) goto cleanup;
 986     } else {
 987         Vcp = NULL;
 988     }
 989     res->vars = Vcv;
 990     res->phases = Vcp;
 991     /* Add sentinel. */
 992     Vcv[2*cv] = 0;
 993     Vcv[2*cv+1] = 0;
 994     while (iclauses != NULL || nclauses != NULL) {
 995         TlClause *nextclause;
 996         cv--;
 997         if (nclauses == NULL || (iclauses != NULL &&
 998             beforep(nclauses->v1, nclauses->p1, nclauses->v2, nclauses->p2,
 999                     iclauses->v1, iclauses->p1, iclauses->v2, iclauses->p2))) {
1000             Vcv[2*cv] = iclauses->v1;
1001             Vcv[2*cv+1] = iclauses->v2;
1002             bitVectorSet(Vcp, 2*cv, iclauses->p1);
1003             bitVectorSet(Vcp, 2*cv+1, iclauses->p2);
1004             nextclause = iclauses->next;
1005             FREE(iclauses);
1006             iclauses = nextclause;
1007         } else {
1008             Vcv[2*cv] = nclauses->v1;
1009             Vcv[2*cv+1] = nclauses->v2;
1010             bitVectorSet(Vcp, 2*cv, nclauses->p1);
1011             bitVectorSet(Vcp, 2*cv+1, nclauses->p2);
1012             nextclause = nclauses->next;
1013             FREE(nclauses);
1014             nclauses = nextclause;
1015         }
1016     }
1017     assert(cv == 0);
1018
1019     return(res);
1020
1021  cleanup:
1022     if (res != NULL) Cudd_tlcInfoFree(res);
1023     while (iclauses != NULL) {
1024         TlClause *nextclause = iclauses->next;
1025         FREE(iclauses);
1026         iclauses = nextclause;
1027     }
1028     while (nclauses != NULL) {
1029         TlClause *nextclause = nclauses->next;
1030         FREE(nclauses);
1031         nclauses = nextclause;
1032     }
1033     while (tclauses != NULL) {
1034         TlClause *nextclause = tclauses->next;
1035         FREE(tclauses);
1036         tclauses = nextclause;
1037     }
1038     while (eclauses != NULL) {
1039         TlClause *nextclause = eclauses->next;
1040         FREE(eclauses);
1041         eclauses = nextclause;
1042     }
1043
1044     return(NULL);
1045
1046 } /* end of computeClauses */
1047
1048
1049 /**Function********************************************************************
1050
1051   Synopsis    [Computes the two-literal clauses for a node.]
1052
1053   Description [Computes the two-literal clauses for a node with a zero
1054   child, given the clauses for its other child and the label of the
1055   node.  Returns a pointer to a TclInfo structure if successful; NULL
1056   otherwise.]
1057
1058   SideEffects [None]
1059
1060   SeeAlso     [computeClauses]
1061
1062 ******************************************************************************/
1063 static DdTlcInfo *
1064 computeClausesWithUniverse(
1065   DdTlcInfo *Cres /* list of clauses for child */,
1066   DdHalfWord label /* variable labeling the current node */,
1067   short phase /* 0 if E child is zero; 1 if T child is zero */)
1068 {
1069     DdHalfWord *Ccv = Cres->vars; /* variables of clauses for child */
1070     BitVector *Ccp = Cres->phases; /* phases of clauses for child */
1071     DdHalfWord *Vcv = NULL; /* pointer to the variables of the clauses for v */
1072     BitVector *Vcp = NULL; /* pointer to the phases of the clauses for v */
1073     DdTlcInfo *res = NULL; /* the set of clauses to be returned */
1074     int i;
1075
1076     /* Initialize result. */
1077     res = tlcInfoAlloc();
1078     if (res == NULL) goto cleanup;
1079     /* Count entries for new list and allocate accordingly. */
1080     for (i = 0; !sentinelp(Ccv[i], Ccv[i+1]); i += 2);
1081     /* At this point, i is twice the number of clauses in the child's
1082     ** list.  We need four more entries for this node: 2 for the one-literal
1083     ** clause for the label, and 2 for the sentinel. */
1084     Vcv = ALLOC(DdHalfWord,i+4);
1085     if (Vcv == NULL) goto cleanup;
1086     Vcp = bitVectorAlloc(i+4);
1087     if (Vcp == NULL) goto cleanup;
1088     res->vars = Vcv;
1089     res->phases = Vcp;
1090     /* Copy old list into new. */
1091     for (i = 0; !sentinelp(Ccv[i], Ccv[i+1]); i += 2) {
1092         Vcv[i] = Ccv[i];
1093         Vcv[i+1] = Ccv[i+1];
1094         bitVectorSet(Vcp, i, bitVectorRead(Ccp, i));
1095         bitVectorSet(Vcp, i+1, bitVectorRead(Ccp, i+1));
1096     }
1097     /* Add clause corresponding to label. */
1098     Vcv[i] = label;
1099     bitVectorSet(Vcp, i, phase);
1100     i++;
1101     Vcv[i] = CUDD_MAXINDEX;
1102     bitVectorSet(Vcp, i, 1);
1103     i++;
1104     /* Add sentinel. */
1105     Vcv[i] = 0;
1106     Vcv[i+1] = 0;
1107     bitVectorSet(Vcp, i, 0);
1108     bitVectorSet(Vcp, i+1, 0);
1109
1110     return(res);
1111
1112  cleanup:
1113     /* Vcp is guaranteed to be NULL here.  Hence, we do not try to free it. */
1114     if (Vcv != NULL) FREE(Vcv);
1115     if (res != NULL) Cudd_tlcInfoFree(res);
1116
1117     return(NULL);
1118
1119 } /* end of computeClausesWithUniverse */
1120
1121
1122 /**Function********************************************************************
1123
1124   Synopsis    [Returns an enpty set of clauses.]
1125
1126   Description [Returns a pointer to an empty set of clauses if
1127   successful; NULL otherwise.  No bit vector for the phases is
1128   allocated.]
1129
1130   SideEffects [None]
1131
1132   SeeAlso     []
1133
1134 ******************************************************************************/
1135 static DdTlcInfo *
1136 emptyClauseSet(void)
1137 {
1138     DdTlcInfo *eset;
1139
1140     eset = ALLOC(DdTlcInfo,1);
1141     if (eset == NULL) return(NULL);
1142     eset->vars = ALLOC(DdHalfWord,2);
1143     if (eset->vars == NULL) {
1144         FREE(eset);
1145         return(NULL);
1146     }
1147     /* Sentinel */
1148     eset->vars[0] = 0;
1149     eset->vars[1] = 0;
1150     eset->phases = NULL; /* does not matter */
1151     eset->cnt = 0;
1152     return(eset);
1153
1154 } /* end of emptyClauseSet */
1155
1156
1157 /**Function********************************************************************
1158
1159   Synopsis    [Returns true iff the argument is the sentinel clause.]
1160
1161   Description [Returns true iff the argument is the sentinel clause.
1162   A sentinel clause has both variables equal to 0.]
1163
1164   SideEffects [None]
1165
1166   SeeAlso     []
1167
1168 ******************************************************************************/
1169 static int
1170 sentinelp(
1171   DdHalfWord var1,
1172   DdHalfWord var2)
1173 {
1174     return(var1 == 0 && var2 == 0);
1175
1176 } /* end of sentinelp */
1177
1178
1179 /**Function********************************************************************
1180
1181   Synopsis    [Returns true iff the two arguments are identical clauses.]
1182
1183   Description [Returns true iff the two arguments are identical
1184   clauses.  Since literals are sorted, we only need to compare
1185   literals in the same position.]
1186
1187   SideEffects [None]
1188
1189   SeeAlso     [beforep]
1190
1191 ******************************************************************************/
1192 static int
1193 equalp(
1194   DdHalfWord var1a,
1195   short phase1a,
1196   DdHalfWord var1b,
1197   short phase1b,
1198   DdHalfWord var2a,
1199   short phase2a,
1200   DdHalfWord var2b,
1201   short phase2b)
1202 {
1203     return(var1a == var2a && phase1a == phase2a &&
1204            var1b == var2b && phase1b == phase2b);
1205
1206 } /* end of equalp */
1207
1208
1209 /**Function********************************************************************
1210
1211   Synopsis    [Returns true iff the first argument precedes the second in
1212   the clause order.]
1213
1214   Description [Returns true iff the first argument precedes the second
1215   in the clause order.  A clause precedes another if its first lieral
1216   precedes the first literal of the other, or if the first literals
1217   are the same, and its second literal precedes the second literal of
1218   the other clause.  A literal precedes another if it has a higher
1219   index, of if it has the same index, but it has lower phase.  Phase 0
1220   is the positive phase, and it is lower than Phase 1 (negative
1221   phase).]
1222
1223   SideEffects [None]
1224
1225   SeeAlso     [equalp]
1226
1227 ******************************************************************************/
1228 static int
1229 beforep(
1230   DdHalfWord var1a,
1231   short phase1a,
1232   DdHalfWord var1b,
1233   short phase1b,
1234   DdHalfWord var2a,
1235   short phase2a,
1236   DdHalfWord var2b,
1237   short phase2b)
1238 {
1239     return(var1a > var2a || (var1a == var2a &&
1240            (phase1a < phase2a || (phase1a == phase2a &&
1241             (var1b > var2b || (var1b == var2b && phase1b < phase2b))))));
1242
1243 } /* end of beforep */
1244
1245
1246 /**Function********************************************************************
1247
1248   Synopsis    [Returns true iff the argument is a one-literal clause.]
1249
1250   Description [Returns true iff the argument is a one-literal clause.
1251   A one-litaral clause has the constant FALSE as second literal.
1252   Since the constant TRUE is never used, it is sufficient to test for
1253   a constant.]
1254
1255   SideEffects [None]
1256
1257   SeeAlso     []
1258
1259 ******************************************************************************/
1260 static int
1261 oneliteralp(
1262   DdHalfWord var)
1263 {
1264     return(var == CUDD_MAXINDEX);
1265
1266 } /* end of oneliteralp */
1267
1268
1269 /**Function********************************************************************
1270
1271   Synopsis [Returns true iff either literal of a clause is in a set of
1272   literals.]
1273
1274   Description [Returns true iff either literal of a clause is in a set
1275   of literals.  The first four arguments specify the clause.  The
1276   remaining two arguments specify the literal set.]
1277
1278   SideEffects [None]
1279
1280   SeeAlso     []
1281
1282 ******************************************************************************/
1283 static int
1284 impliedp(
1285   DdHalfWord var1,
1286   short phase1,
1287   DdHalfWord var2,
1288   short phase2,
1289   BitVector *olv,
1290   BitVector *olp)
1291 {
1292     return((bitVectorRead(olv, var1) &&
1293             bitVectorRead(olp, var1) == phase1) ||
1294            (bitVectorRead(olv, var2) &&
1295             bitVectorRead(olp, var2) == phase2));
1296
1297 } /* end of impliedp */
1298
1299
1300 /**Function********************************************************************
1301
1302   Synopsis    [Allocates a bit vector.]
1303
1304   Description [Allocates a bit vector.  The parameter size gives the
1305   number of bits.  This procedure allocates enough long's to hold the
1306   specified number of bits.  Returns a pointer to the allocated vector
1307   if successful; NULL otherwise.]
1308
1309   SideEffects [None]
1310
1311   SeeAlso     [bitVectorClear bitVectorFree]
1312
1313 ******************************************************************************/
1314 static BitVector *
1315 bitVectorAlloc(
1316   int size)
1317 {
1318     int allocSize;
1319     BitVector *vector;
1320
1321     /* Find out how many long's we need.
1322     ** There are sizeof(long) * 8 bits in a long.
1323     ** The ceiling of the ratio of two integers m and n is given
1324     ** by ((n-1)/m)+1.  Putting all this together, we get... */
1325     allocSize = ((size - 1) / (sizeof(BitVector) * 8)) + 1;
1326     vector = ALLOC(BitVector, allocSize);
1327     if (vector == NULL) return(NULL);
1328     /* Clear the whole array. */
1329     (void) memset(vector, 0, allocSize * sizeof(BitVector));
1330     return(vector);
1331
1332 } /* end of bitVectorAlloc */
1333
1334
1335 /**Function********************************************************************
1336
1337   Synopsis    [Clears a bit vector.]
1338
1339   Description [Clears a bit vector.  The parameter size gives the
1340   number of bits.]
1341
1342   SideEffects [None]
1343
1344   SeeAlso     [bitVectorAlloc]
1345
1346 ******************************************************************************/
1347 DD_INLINE
1348 static void
1349 bitVectorClear(
1350   BitVector *vector,
1351   int size)
1352 {
1353     int allocSize;
1354
1355     /* Find out how many long's we need.
1356     ** There are sizeof(long) * 8 bits in a long.
1357     ** The ceiling of the ratio of two integers m and n is given
1358     ** by ((n-1)/m)+1.  Putting all this together, we get... */
1359     allocSize = ((size - 1) / (sizeof(BitVector) * 8)) + 1;
1360     /* Clear the whole array. */
1361     (void) memset(vector, 0, allocSize * sizeof(BitVector));
1362     return;
1363
1364 } /* end of bitVectorClear */
1365
1366
1367 /**Function********************************************************************
1368
1369   Synopsis    [Frees a bit vector.]
1370
1371   Description [Frees a bit vector.]
1372
1373   SideEffects [None]
1374
1375   SeeAlso     [bitVectorAlloc]
1376
1377 ******************************************************************************/
1378 static void
1379 bitVectorFree(
1380   BitVector *vector)
1381 {
1382     FREE(vector);
1383
1384 } /* end of bitVectorFree */
1385
1386
1387 /**Function********************************************************************
1388
1389   Synopsis    [Returns the i-th entry of a bit vector.]
1390
1391   Description [Returns the i-th entry of a bit vector.]
1392
1393   SideEffects [None]
1394
1395   SeeAlso     [bitVectorSet]
1396
1397 ******************************************************************************/
1398 DD_INLINE
1399 static short
1400 bitVectorRead(
1401   BitVector *vector,
1402   int i)
1403 {
1404     int word, bit;
1405     short result;
1406
1407     if (vector == NULL) return((short) 0);
1408
1409     word = i >> LOGBPL;
1410     bit = i & (BPL - 1);
1411     result = (short) ((vector[word] >> bit) & 1L);
1412     return(result);
1413
1414 } /* end of bitVectorRead */
1415
1416
1417 /**Function********************************************************************
1418
1419   Synopsis    [Sets the i-th entry of a bit vector to a value.]
1420
1421   Description [Sets the i-th entry of a bit vector to a value.]
1422
1423   SideEffects [None]
1424
1425   SeeAlso     [bitVectorRead]
1426
1427 ******************************************************************************/
1428 DD_INLINE
1429 static void
1430 bitVectorSet(
1431   BitVector * vector,
1432   int i,
1433   short val)
1434 {
1435     int word, bit;
1436
1437     word = i >> LOGBPL;
1438     bit = i & (BPL - 1);
1439     vector[word] &= ~(1L << bit);
1440     vector[word] |= (((long) val) << bit);
1441
1442 } /* end of bitVectorSet */
1443
1444
1445 /**Function********************************************************************
1446
1447   Synopsis    [Allocates a DdTlcInfo Structure.]
1448
1449   Description [Returns a pointer to a DdTlcInfo Structure if successful;
1450   NULL otherwise.]
1451
1452   SideEffects [None]
1453
1454   SeeAlso     [Cudd_tlcInfoFree]
1455
1456 ******************************************************************************/
1457 static DdTlcInfo *
1458 tlcInfoAlloc(void)
1459 {
1460     DdTlcInfo *res = ALLOC(DdTlcInfo,1);
1461     if (res == NULL) return(NULL);
1462     res->vars = NULL;
1463     res->phases = NULL;
1464     res->cnt = 0;
1465     return(res);
1466
1467 } /* end of tlcInfoAlloc */