source: vis_dev/glu-2.1/src/cuBdd/cuddEssent.c @ 8

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

src glu
File size: 43.8 KB
RevLine 
[8]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.21 2004/08/13 18:04:48 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, int size);
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 >= 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, dd->size);
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, dd->size);
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  int size /* number of variables in the manager */)
1069{
1070    DdHalfWord *Ccv = Cres->vars; /* variables of clauses for child */
1071    BitVector *Ccp = Cres->phases; /* phases of clauses for child */
1072    DdHalfWord *Vcv = NULL; /* pointer to the variables of the clauses for v */
1073    BitVector *Vcp = NULL; /* pointer to the phases of the clauses for v */
1074    DdTlcInfo *res = NULL; /* the set of clauses to be returned */
1075    int i;
1076
1077    /* Initialize result. */
1078    res = tlcInfoAlloc();
1079    if (res == NULL) goto cleanup;
1080    /* Count entries for new list and allocate accordingly. */
1081    for (i = 0; !sentinelp(Ccv[i], Ccv[i+1]); i += 2);
1082    /* At this point, i is twice the number of clauses in the child's
1083    ** list.  We need four more entries for this node: 2 for the one-literal
1084    ** clause for the label, and 2 for the sentinel. */
1085    Vcv = ALLOC(DdHalfWord,i+4);
1086    if (Vcv == NULL) goto cleanup;
1087    Vcp = bitVectorAlloc(i+4);
1088    if (Vcp == NULL) goto cleanup;
1089    res->vars = Vcv;
1090    res->phases = Vcp;
1091    /* Copy old list into new. */
1092    for (i = 0; !sentinelp(Ccv[i], Ccv[i+1]); i += 2) {
1093        Vcv[i] = Ccv[i];
1094        Vcv[i+1] = Ccv[i+1];
1095        bitVectorSet(Vcp, i, bitVectorRead(Ccp, i));
1096        bitVectorSet(Vcp, i+1, bitVectorRead(Ccp, i+1));
1097    }
1098    /* Add clause corresponding to label. */
1099    Vcv[i] = label;
1100    bitVectorSet(Vcp, i, phase);
1101    i++;
1102    Vcv[i] = CUDD_MAXINDEX;
1103    bitVectorSet(Vcp, i, 1);
1104    i++;
1105    /* Add sentinel. */
1106    Vcv[i] = 0;
1107    Vcv[i+1] = 0;
1108    bitVectorSet(Vcp, i, 0);
1109    bitVectorSet(Vcp, i+1, 0);
1110
1111    return(res);
1112
1113 cleanup:
1114    if (Vcv != NULL) FREE(Vcv);
1115    if (Vcp != NULL) bitVectorFree(Vcp);
1116    if (res != NULL) Cudd_tlcInfoFree(res);
1117
1118    return(NULL);
1119
1120} /* end of computeClausesWithUniverse */
1121
1122
1123/**Function********************************************************************
1124
1125  Synopsis    [Returns an enpty set of clauses.]
1126
1127  Description [Returns a pointer to an empty set of clauses if
1128  successful; NULL otherwise.  No bit vector for the phases is
1129  allocated.]
1130
1131  SideEffects [None]
1132
1133  SeeAlso     []
1134
1135******************************************************************************/
1136static DdTlcInfo *
1137emptyClauseSet(void)
1138{
1139    DdTlcInfo *eset;
1140
1141    eset = ALLOC(DdTlcInfo,1);
1142    if (eset == NULL) return(NULL);
1143    eset->vars = ALLOC(DdHalfWord,2);
1144    if (eset->vars == NULL) {
1145        FREE(eset);
1146        return(NULL);
1147    }
1148    /* Sentinel */
1149    eset->vars[0] = 0;
1150    eset->vars[1] = 0;
1151    eset->phases = NULL; /* does not matter */
1152    eset->cnt = 0;
1153    return(eset);
1154
1155} /* end of emptyClauseSet */
1156
1157
1158/**Function********************************************************************
1159
1160  Synopsis    [Returns true iff the argument is the sentinel clause.]
1161
1162  Description [Returns true iff the argument is the sentinel clause.
1163  A sentinel clause has both variables equal to 0.]
1164
1165  SideEffects [None]
1166
1167  SeeAlso     []
1168
1169******************************************************************************/
1170static int
1171sentinelp(
1172  DdHalfWord var1,
1173  DdHalfWord var2)
1174{
1175    return(var1 == 0 && var2 == 0);
1176
1177} /* end of sentinelp */
1178
1179
1180/**Function********************************************************************
1181
1182  Synopsis    [Returns true iff the two arguments are identical clauses.]
1183
1184  Description [Returns true iff the two arguments are identical
1185  clauses.  Since literals are sorted, we only need to compare
1186  literals in the same position.]
1187
1188  SideEffects [None]
1189
1190  SeeAlso     [beforep]
1191
1192******************************************************************************/
1193static int
1194equalp(
1195  DdHalfWord var1a,
1196  short phase1a,
1197  DdHalfWord var1b,
1198  short phase1b,
1199  DdHalfWord var2a,
1200  short phase2a,
1201  DdHalfWord var2b,
1202  short phase2b)
1203{
1204    return(var1a == var2a && phase1a == phase2a &&
1205           var1b == var2b && phase1b == phase2b);
1206
1207} /* end of equalp */
1208
1209
1210/**Function********************************************************************
1211
1212  Synopsis    [Returns true iff the first argument precedes the second in
1213  the clause order.]
1214
1215  Description [Returns true iff the first argument precedes the second
1216  in the clause order.  A clause precedes another if its first lieral
1217  precedes the first literal of the other, or if the first literals
1218  are the same, and its second literal precedes the second literal of
1219  the other clause.  A literal precedes another if it has a higher
1220  index, of if it has the same index, but it has lower phase.  Phase 0
1221  is the positive phase, and it is lower than Phase 1 (negative
1222  phase).]
1223
1224  SideEffects [None]
1225
1226  SeeAlso     [equalp]
1227
1228******************************************************************************/
1229static int
1230beforep(
1231  DdHalfWord var1a,
1232  short phase1a,
1233  DdHalfWord var1b,
1234  short phase1b,
1235  DdHalfWord var2a,
1236  short phase2a,
1237  DdHalfWord var2b,
1238  short phase2b)
1239{
1240    return(var1a > var2a || (var1a == var2a &&
1241           (phase1a < phase2a || (phase1a == phase2a &&
1242            (var1b > var2b || (var1b == var2b && phase1b < phase2b))))));
1243
1244} /* end of beforep */
1245
1246
1247/**Function********************************************************************
1248
1249  Synopsis    [Returns true iff the argument is a one-literal clause.]
1250
1251  Description [Returns true iff the argument is a one-literal clause.
1252  A one-litaral clause has the constant FALSE as second literal.
1253  Since the constant TRUE is never used, it is sufficient to test for
1254  a constant.]
1255
1256  SideEffects [None]
1257
1258  SeeAlso     []
1259
1260******************************************************************************/
1261static int
1262oneliteralp(
1263  DdHalfWord var)
1264{
1265    return(var == CUDD_MAXINDEX);
1266
1267} /* end of oneliteralp */
1268
1269
1270/**Function********************************************************************
1271
1272  Synopsis [Returns true iff either literal of a clause is in a set of
1273  literals.]
1274
1275  Description [Returns true iff either literal of a clause is in a set
1276  of literals.  The first four arguments specify the clause.  The
1277  remaining two arguments specify the literal set.]
1278
1279  SideEffects [None]
1280
1281  SeeAlso     []
1282
1283******************************************************************************/
1284static int
1285impliedp(
1286  DdHalfWord var1,
1287  short phase1,
1288  DdHalfWord var2,
1289  short phase2,
1290  BitVector *olv,
1291  BitVector *olp)
1292{
1293    return((bitVectorRead(olv, var1) &&
1294            bitVectorRead(olp, var1) == phase1) ||
1295           (bitVectorRead(olv, var2) &&
1296            bitVectorRead(olp, var2) == phase2));
1297
1298} /* end of impliedp */
1299
1300
1301/**Function********************************************************************
1302
1303  Synopsis    [Allocates a bit vector.]
1304
1305  Description [Allocates a bit vector.  The parameter size gives the
1306  number of bits.  This procedure allocates enough long's to hold the
1307  specified number of bits.  Returns a pointer to the allocated vector
1308  if successful; NULL otherwise.]
1309
1310  SideEffects [None]
1311
1312  SeeAlso     [bitVectorClear bitVectorFree]
1313
1314******************************************************************************/
1315static BitVector *
1316bitVectorAlloc(
1317  int size)
1318{
1319    int allocSize;
1320    BitVector *vector;
1321
1322    /* Find out how many long's we need.
1323    ** There are sizeof(long) * 8 bits in a long.
1324    ** The ceiling of the ratio of two integers m and n is given
1325    ** by ((n-1)/m)+1.  Putting all this together, we get... */
1326    allocSize = ((size - 1) / (sizeof(BitVector) * 8)) + 1;
1327    vector = ALLOC(BitVector, allocSize);
1328    if (vector == NULL) return(NULL);
1329    /* Clear the whole array. */
1330    (void) memset(vector, 0, allocSize * sizeof(BitVector));
1331    return(vector);
1332   
1333} /* end of bitVectorAlloc */
1334
1335
1336/**Function********************************************************************
1337
1338  Synopsis    [Clears a bit vector.]
1339
1340  Description [Clears a bit vector.  The parameter size gives the
1341  number of bits.]
1342
1343  SideEffects [None]
1344
1345  SeeAlso     [bitVectorAlloc]
1346
1347******************************************************************************/
1348DD_INLINE
1349static void
1350bitVectorClear(
1351  BitVector *vector,
1352  int size)
1353{
1354    int allocSize;
1355
1356    /* Find out how many long's we need.
1357    ** There are sizeof(long) * 8 bits in a long.
1358    ** The ceiling of the ratio of two integers m and n is given
1359    ** by ((n-1)/m)+1.  Putting all this together, we get... */
1360    allocSize = ((size - 1) / (sizeof(BitVector) * 8)) + 1;
1361    /* Clear the whole array. */
1362    (void) memset(vector, 0, allocSize * sizeof(BitVector));
1363    return;
1364   
1365} /* end of bitVectorClear */
1366
1367
1368/**Function********************************************************************
1369
1370  Synopsis    [Frees a bit vector.]
1371
1372  Description [Frees a bit vector.]
1373
1374  SideEffects [None]
1375
1376  SeeAlso     [bitVectorAlloc]
1377
1378******************************************************************************/
1379static void
1380bitVectorFree(
1381  BitVector *vector)
1382{
1383    FREE(vector);
1384
1385} /* end of bitVectorFree */
1386
1387
1388/**Function********************************************************************
1389
1390  Synopsis    [Returns the i-th entry of a bit vector.]
1391
1392  Description [Returns the i-th entry of a bit vector.]
1393
1394  SideEffects [None]
1395
1396  SeeAlso     [bitVectorSet]
1397
1398******************************************************************************/
1399DD_INLINE
1400static short
1401bitVectorRead(
1402  BitVector *vector,
1403  int i)
1404{
1405    int word, bit;
1406    short result;
1407
1408    if (vector == NULL) return((short) 0);
1409
1410    word = i >> LOGBPL;
1411    bit = i & (BPL - 1);
1412    result = (short) ((vector[word] >> bit) & 1L);
1413    return(result);
1414
1415} /* end of bitVectorRead */
1416
1417
1418/**Function********************************************************************
1419
1420  Synopsis    [Sets the i-th entry of a bit vector to a value.]
1421
1422  Description [Sets the i-th entry of a bit vector to a value.]
1423
1424  SideEffects [None]
1425
1426  SeeAlso     [bitVectorRead]
1427
1428******************************************************************************/
1429DD_INLINE
1430static void
1431bitVectorSet(
1432  BitVector * vector,
1433  int i,
1434  short val)
1435{
1436    int word, bit;
1437
1438    word = i >> LOGBPL;
1439    bit = i & (BPL - 1);
1440    vector[word] &= ~(1L << bit);
1441    vector[word] |= (((long) val) << bit);
1442
1443} /* end of bitVectorSet */
1444
1445
1446/**Function********************************************************************
1447
1448  Synopsis    [Allocates a DdTlcInfo Structure.]
1449
1450  Description [Returns a pointer to a DdTlcInfo Structure if successful;
1451  NULL otherwise.]
1452
1453  SideEffects [None]
1454
1455  SeeAlso     [Cudd_tlcInfoFree]
1456
1457******************************************************************************/
1458static DdTlcInfo *
1459tlcInfoAlloc(void)
1460{
1461    DdTlcInfo *res = ALLOC(DdTlcInfo,1);
1462    if (res == NULL) return(NULL);
1463    res->vars = NULL;
1464    res->phases = NULL;
1465    res->cnt = 0;
1466    return(res);
1467
1468} /* end of tlcInfoAlloc */
Note: See TracBrowser for help on using the repository browser.