source: vis_dev/glu-2.3/src/cuBdd/cuddEssent.c @ 88

Last change on this file since 88 was 13, checked in by cecile, 13 years ago

library glu 2.3
File size: 43.6 KB
RevLine 
[13]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*/
118struct 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. */
128struct TlClause {
129    DdHalfWord v1, v2;
130    short p1, p2;
131    struct TlClause *next;
132};
133
134/*---------------------------------------------------------------------------*/
135/* Type declarations                                                         */
136/*---------------------------------------------------------------------------*/
137
138typedef long BitVector;
139typedef struct TlClause TlClause;
140
141/*---------------------------------------------------------------------------*/
142/* Variable declarations                                                     */
143/*---------------------------------------------------------------------------*/
144
145#ifndef lint
146static char rcsid[] DD_UNUSED = "$Id: cuddEssent.c,v 1.24 2009/02/21 18:24:10 fabio Exp $";
147#endif
148
149static BitVector *Tolv;
150static BitVector *Tolp;
151static BitVector *Eolv;
152static BitVector *Eolp;
153
154/*---------------------------------------------------------------------------*/
155/* Macro declarations                                                        */
156/*---------------------------------------------------------------------------*/
157
158/**AutomaticStart*************************************************************/
159
160/*---------------------------------------------------------------------------*/
161/* Static function prototypes                                                */
162/*---------------------------------------------------------------------------*/
163
164static DdNode * ddFindEssentialRecur (DdManager *dd, DdNode *f);
165static DdTlcInfo * ddFindTwoLiteralClausesRecur (DdManager * dd, DdNode * f, st_table *table);
166static DdTlcInfo * computeClauses (DdTlcInfo *Tres, DdTlcInfo *Eres, DdHalfWord label, int size);
167static DdTlcInfo * computeClausesWithUniverse (DdTlcInfo *Cres, DdHalfWord label, short phase);
168static DdTlcInfo * emptyClauseSet (void);
169static int sentinelp (DdHalfWord var1, DdHalfWord var2);
170static int equalp (DdHalfWord var1a, short phase1a, DdHalfWord var1b, short phase1b, DdHalfWord var2a, short phase2a, DdHalfWord var2b, short phase2b);
171static int beforep (DdHalfWord var1a, short phase1a, DdHalfWord var1b, short phase1b, DdHalfWord var2a, short phase2a, DdHalfWord var2b, short phase2b);
172static int oneliteralp (DdHalfWord var);
173static int impliedp (DdHalfWord var1, short phase1, DdHalfWord var2, short phase2, BitVector *olv, BitVector *olp);
174static BitVector * bitVectorAlloc (int size);
175DD_INLINE static void bitVectorClear (BitVector *vector, int size);
176static void bitVectorFree (BitVector *vector);
177DD_INLINE static short bitVectorRead (BitVector *vector, int i);
178DD_INLINE static void bitVectorSet (BitVector * vector, int i, short val);
179static 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******************************************************************************/
204DdNode *
205Cudd_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******************************************************************************/
234int
235Cudd_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******************************************************************************/
272DdTlcInfo *
273Cudd_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******************************************************************************/
354int
355Cudd_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******************************************************************************/
388int
389Cudd_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******************************************************************************/
450void
451Cudd_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******************************************************************************/
481static DdNode *
482ddFindEssentialRecur(
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******************************************************************************/
615static DdTlcInfo *
616ddFindTwoLiteralClausesRecur(
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******************************************************************************/
763static DdTlcInfo *
764computeClauses(
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******************************************************************************/
1063static DdTlcInfo *
1064computeClausesWithUniverse(
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******************************************************************************/
1135static DdTlcInfo *
1136emptyClauseSet(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******************************************************************************/
1169static int
1170sentinelp(
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******************************************************************************/
1192static int
1193equalp(
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******************************************************************************/
1228static int
1229beforep(
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******************************************************************************/
1260static int
1261oneliteralp(
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******************************************************************************/
1283static int
1284impliedp(
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******************************************************************************/
1314static BitVector *
1315bitVectorAlloc(
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******************************************************************************/
1347DD_INLINE
1348static void
1349bitVectorClear(
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******************************************************************************/
1378static void
1379bitVectorFree(
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******************************************************************************/
1398DD_INLINE
1399static short
1400bitVectorRead(
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******************************************************************************/
1428DD_INLINE
1429static void
1430bitVectorSet(
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******************************************************************************/
1457static DdTlcInfo *
1458tlcInfoAlloc(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 */
Note: See TracBrowser for help on using the repository browser.