source: vis_dev/glu-2.3/src/mdd/mdd_util.c @ 25

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

library glu 2.3

File size: 38.4 KB
Line 
1#include <stdio.h>
2#include <math.h>
3#include "util.h"
4#include "mdd.h"
5
6/*
7 * MDD Package
8 *
9 * $Id: mdd_util.c,v 1.39 2009/01/18 02:24:46 fabio Exp $
10 *
11 * Author: Timothy Kam
12 *
13 * Copyright 1992 by the Regents of the University of California.
14 *
15 * All rights reserved.  Permission to use, copy, modify and distribute
16 * this software is hereby granted, provided that the above copyright
17 * notice and this permission notice appear in all copies.  This software
18 * is made available as is, with no warranties.
19 */
20
21static  bdd_t*  mddRetOnvalBdd(mdd_manager *mddMgr, int mddId);
22static  bdd_t*  mddIntRetOnvalBdd(mdd_manager *mddMgr, int valNum, int low, int hi, int level, array_t *bddVarArr);
23static  void    mddFreeBddArr(array_t *bddArr);
24       
25/************************************************************************/
26#define         mddGetVarById( mgr, id )        \
27    array_fetch(mvar_type, mdd_ret_mvar_list((mgr)),(id))
28
29
30int
31toggle(int x)
32{
33    if (x == 0) return 1;
34    else {
35        if (x == 1) return 0;
36        else {
37            fail("toggle: invalid boolean value\n");
38            return -1;
39        }
40    }
41}
42
43int
44no_bit_encode(int n)
45{
46    int i = 0;
47    int j = 1;
48
49    if (n < 2) return 1; /* Takes care of mv.values <= 1 */
50
51    while (j < n) {
52        j = j * 2;
53        i++;
54    }
55    return i;
56}
57
58void
59print_mvar_list(mdd_manager *mgr)
60{
61    mvar_type mv;
62    int i;
63    int no_mvar;
64    array_t *mvar_list = mdd_ret_mvar_list(mgr);
65
66    no_mvar = array_n(mvar_list);
67    printf("print_mvar_list:\n");
68    printf("id\tname\tvalues\tbits\tstride\tstart_vertex\n");
69    for (i=0; i<no_mvar; i++) {
70        mv = array_fetch(mvar_type, mvar_list, i);
71        (void) printf("%d\t%s\t%d\t%d\n", 
72                mv.mvar_id, mv.name, mv.values, 
73                mv.encode_length);
74    }
75}
76
77void
78print_strides(array_t *mvar_strides)
79{
80    int i, s;
81
82    (void) printf("mvar_strides: ");
83    for (i=0; i<array_n(mvar_strides); i++) {
84        s = array_fetch(int, mvar_strides, i);
85        (void) printf("%d ", s);
86    }
87    (void) printf("\n");
88}
89
90void
91print_bdd_list_id(array_t *bdd_list)
92{
93    bdd_t *b;
94    int i, is_complemented;
95
96    (void) printf("bdd_list id's: ");
97    for (i=0; i<array_n(bdd_list); i++) {
98        b = array_fetch(bdd_t *, bdd_list, i);
99        (void)bdd_get_node(b, &is_complemented);
100        if (is_complemented) (void) printf("!");
101        (void) printf("%d ", bdd_top_var_id(b));
102    }
103    (void) printf("\n");
104}
105
106void
107print_bvar_list_id(mdd_manager *mgr)
108{
109    bvar_type bv;
110    int i, is_complemented;
111    array_t *bvar_list = mdd_ret_bvar_list(mgr);
112 
113    (void) printf("bvar_list id's: ");
114    for (i=0; i<array_n(bvar_list); i++) {
115        bv = array_fetch(bvar_type, bvar_list, i);
116        (void)bdd_get_node(bv.node,&is_complemented);
117        if (is_complemented) (void) printf("!");
118        (void) printf("%d ", bdd_top_var_id(bv.node));
119    }
120    (void) printf("\n");
121}
122
123void
124print_bdd(bdd_manager *mgr, bdd_t *top)
125{
126
127    int is_complemented;
128    bdd_t *child, *top_uncomp;
129
130    if (bdd_is_tautology(top,1)) {
131        (void) printf("ONE ");
132        return;
133    }
134    if (bdd_is_tautology(top,0)) {
135        (void) printf("ZERO ");
136        return;
137    }
138    (void)bdd_get_node(top, &is_complemented);
139    if (is_complemented != 0) (void) printf("!");
140    (void) printf("%d ", bdd_top_var_id(top));
141    (void) printf("v ");
142    (void) printf("< ");
143
144    if (is_complemented) top_uncomp = bdd_not(top);
145    else top_uncomp = mdd_dup(top);
146
147    child = bdd_then(top);
148
149    print_bdd(mgr, child);
150    (void) printf("> ");
151
152    mdd_free(child);
153    child = bdd_else(top);
154
155    print_bdd(mgr, child);
156    (void) printf("^ ");
157   
158    mdd_free(top_uncomp);
159    mdd_free(child);
160
161    return;
162}
163
164mvar_type
165find_mvar_id(mdd_manager *mgr, unsigned short id)
166{
167    mvar_type mv;
168    bvar_type bv;
169    array_t *mvar_list = mdd_ret_mvar_list(mgr);
170    array_t *bvar_list = mdd_ret_bvar_list(mgr);
171
172    if (id >= array_n(bvar_list))
173        fail("find_mvar_id: invalid parameter range for id\n");
174    bv = array_fetch(bvar_type, bvar_list, id);
175    if ((bv.mvar_id < 0) || (bv.mvar_id >= array_n(mvar_list)))
176        fail("find_mvar_id: bvar contains invalid mvar_id\n");
177    mv = array_fetch(mvar_type, mvar_list, bv.mvar_id);
178    return mv;
179}
180
181void
182clear_all_marks(mdd_manager *mgr)
183{
184    int i, j;
185    mvar_type mv;
186    array_t *mvar_list = mdd_ret_mvar_list(mgr);
187
188
189    for (i=0; i<array_n(mvar_list); i++) {
190        mv = array_fetch(mvar_type, mvar_list, i);
191        for (j=0; j<mv.encode_length; j++)
192            mv.encoding[j] = 2;
193    }
194}
195
196void
197mdd_mark(
198  mdd_manager *mgr,
199  bdd_t *top /**** was bdd_node *bnode; --- changed by Serdar ***/,
200  int phase)
201{
202    int i, top_id, found = 0;
203    int bit_position = 0; /* initialize for lint */
204    mvar_type mv;
205
206    top_id = bdd_top_var_id(top);
207    mv = find_mvar_id(mgr, top_id);
208
209    for (i=0; i<(mv.encode_length); i++){
210                if ( mdd_ret_bvar_id( &mv, i) == top_id ){
211                        bit_position = i;
212                        found = 1;
213                        break;
214                };
215    };
216   
217   
218    if (found == 0)
219        fail("mdd_mark: interleaving error\n");
220
221    mv.encoding[bit_position] = phase;
222   
223}
224
225void
226mdd_unmark(mdd_manager *mgr, bdd_t *top)
227{
228    int i, top_id, found = 0;
229    int bit_position = 0; /* initialize for lint */
230    mvar_type mv;
231
232
233    top_id = bdd_top_var_id(top);
234    mv = find_mvar_id(mgr, top_id);
235
236    for (i=0; i<mv.encode_length; i++) 
237                if ( mdd_ret_bvar_id( &mv, i) == top_id ){
238                        bit_position = i;
239                        found = 1;
240                        break;
241                };
242
243    if (found == 0)
244        fail("mdd_unmark: interleaving error\n");
245    mv.encoding[bit_position] = 2;
246}
247
248mvar_type
249find_mvar(mdd_manager *mgr, char *name)
250{
251    int i;
252    mvar_type mv;
253    array_t *mvar_list = mdd_ret_mvar_list(mgr);
254
255    for (i=0; i<array_n(mvar_list); i++) {
256        mv = array_fetch(mvar_type, mvar_list, i);
257        if (strcmp(mv.name, name) == 0) return mv;
258    }
259    fail("find_mvar: cannot find name in mvar_list\n");
260    return mv;
261}
262
263array_t *
264mdd_ret_mvar_list(mdd_manager *mgr)
265{
266    bdd_external_hooks *hook;   
267    array_t *mvar_list;
268
269    hook =  bdd_get_external_hooks(mgr);
270    mvar_list = ((mdd_hook_type *)(hook->mdd))->mvar_list;
271
272    return mvar_list;
273}
274
275void
276mdd_set_mvar_list(mdd_manager *mgr, array_t *mvar_list)
277{
278    bdd_external_hooks *hook;   
279
280    hook =  bdd_get_external_hooks(mgr);
281    ((mdd_hook_type *)(hook->mdd))->mvar_list = mvar_list;
282}
283
284
285array_t *
286mdd_ret_bvar_list(mdd_manager *mgr)
287{
288    bdd_external_hooks *hook;   
289    array_t *bvar_list;
290
291    hook =  bdd_get_external_hooks(mgr);
292    bvar_list = ((mdd_hook_type *)(hook->mdd))->bvar_list;
293
294    return bvar_list;
295}
296
297
298void
299mdd_set_bvar_list(mdd_manager *mgr, array_t *bvar_list)
300{
301    bdd_external_hooks *hook;   
302
303    hook =  bdd_get_external_hooks(mgr);
304    ((mdd_hook_type *)(hook->mdd))->bvar_list = bvar_list;
305}
306
307
308int
309mdd_ret_bvar_id(mvar_type *mvar_ptr, int i)
310{
311       
312        return ( array_fetch(int, mvar_ptr->bvars, i) );
313}
314
315bvar_type
316mdd_ret_bvar(mvar_type *mvar_ptr, int i, array_t *bvar_list)
317{
318        int bvar_id;
319       
320        bvar_id = array_fetch(int, mvar_ptr->bvars, i);
321       
322        return array_fetch(bvar_type, bvar_list, bvar_id);
323}
324
325/************************************************************************/
326/* Given an Mdd, returns the num of onset points.  By construction of   */
327/* Mdd's, some points not in the range of Mdd vars may be included      */
328/* in the onset. These fake points must first be removed.               */
329/************************************************************************/
330
331double
332mdd_count_onset(
333  mdd_manager   *mddMgr,
334  mdd_t         *aMdd,
335  array_t       *mddIdArr)
336{
337        bdd_t           *onvalBdd, *aOnvalBdd, *onsetBdd, *tmpBdd;
338        double          onsetNum;
339        array_t         *bddVarArr;
340        int             i, arrSize, mddId;
341
342        arrSize = array_n( mddIdArr );
343        onvalBdd = bdd_one( mddMgr );
344
345        for ( i = 0 ; i < arrSize ; i++ ) {
346            mddId = array_fetch( int, mddIdArr, i );
347            aOnvalBdd = mddRetOnvalBdd( mddMgr, mddId );
348
349            tmpBdd = bdd_and( onvalBdd, aOnvalBdd, 1, 1 );
350            bdd_free( onvalBdd );
351            bdd_free( aOnvalBdd );
352            onvalBdd = tmpBdd;
353        }
354        onsetBdd = bdd_and( onvalBdd, aMdd, 1, 1 );
355        bdd_free( onvalBdd );
356
357        bddVarArr = mdd_id_array_to_bdd_array( mddMgr, mddIdArr );
358        onsetNum = bdd_count_onset( onsetBdd, bddVarArr );
359        bdd_free( onsetBdd );
360        mddFreeBddArr( bddVarArr );
361        return( onsetNum );
362}               /* mdd_count_onset */
363
364mdd_t *
365mdd_onset_bdd(
366  mdd_manager   *mddMgr,
367  mdd_t         *aMdd,
368  array_t       *mddIdArr)
369{
370        bdd_t           *onvalBdd, *aOnvalBdd, *onsetBdd, *tmpBdd;
371        int             i, arrSize, mddId;
372
373        arrSize = array_n( mddIdArr );
374        onvalBdd = bdd_one( mddMgr );
375
376        for ( i = 0 ; i < arrSize ; i++ ) {
377            mddId = array_fetch( int, mddIdArr, i );
378            aOnvalBdd = mddRetOnvalBdd( mddMgr, mddId );
379
380            tmpBdd = bdd_and( onvalBdd, aOnvalBdd, 1, 1 );
381            bdd_free( onvalBdd );
382            bdd_free( aOnvalBdd );
383            onvalBdd = tmpBdd;
384        }
385        onsetBdd = bdd_and( onvalBdd, aMdd, 1, 1 );
386        bdd_free( onvalBdd );
387        return( onsetBdd );
388}               /* mdd_onset_bdd */
389
390int
391mdd_epd_count_onset(
392  mdd_manager   *mddMgr,
393  mdd_t         *aMdd,
394  array_t       *mddIdArr,
395  EpDouble      *epd)
396{
397        bdd_t           *onvalBdd, *aOnvalBdd, *onsetBdd, *tmpBdd;
398        array_t         *bddVarArr;
399        int             i, arrSize, mddId;
400        int             status;
401
402        arrSize = array_n( mddIdArr );
403        onvalBdd = bdd_one( mddMgr );
404
405        for ( i = 0 ; i < arrSize ; i++ ) {
406            mddId = array_fetch( int, mddIdArr, i );
407            aOnvalBdd = mddRetOnvalBdd( mddMgr, mddId );
408
409            tmpBdd = bdd_and( onvalBdd, aOnvalBdd, 1, 1 );
410            bdd_free( onvalBdd );
411            bdd_free( aOnvalBdd );
412            onvalBdd = tmpBdd;
413        }
414        onsetBdd = bdd_and( onvalBdd, aMdd, 1, 1 );
415        bdd_free( onvalBdd );
416
417        bddVarArr = mdd_id_array_to_bdd_array( mddMgr, mddIdArr );
418        status = bdd_epd_count_onset( onsetBdd, bddVarArr, epd );
419        if (status)
420            return(status);
421        bdd_free( onsetBdd );
422        mddFreeBddArr( bddVarArr );
423        return(0);
424}               /* mdd_epd_count_onset */
425
426/************************************************************************/
427static  bdd_t*
428mddRetOnvalBdd(
429  mdd_manager   *mddMgr,
430  int           mddId)
431{
432        bdd_t           *onvalBdd;
433        mvar_type       mVar;
434        int             valNum, high;
435        array_t         *bddVarArr;     
436       
437        mVar = mddGetVarById( mddMgr, mddId );
438        valNum = mVar.values;
439        high = (int) pow( (double) 2, (double) mVar.encode_length ); 
440        assert( (valNum == 1)  || ( (valNum <= high) && (valNum > high/2) ));
441        if ( valNum == high )
442            onvalBdd = bdd_one( mddMgr );
443        else {
444            bddVarArr = mdd_id_to_bdd_array( mddMgr, mddId );
445            onvalBdd = mddIntRetOnvalBdd( mddMgr, valNum, 0, high, 
446                                          0, bddVarArr );
447            mddFreeBddArr( bddVarArr );
448        }
449        return( onvalBdd );
450}               /* mddRetOnvalBdd */   
451
452/************************************************************************/
453static  bdd_t*
454mddIntRetOnvalBdd(
455  mdd_manager *mddMgr,
456  int valNum,
457  int low,
458  int hi,
459  int level,
460  array_t *bddVarArr)
461{
462        int             mid;
463        bdd_t           *curVar, *recBdd;
464        bdd_t           *onvalBdd = NIL(bdd_t); /* initialized for lint */
465
466        mid = (low + hi) / 2;
467        curVar = array_fetch( bdd_t *, bddVarArr, level );
468
469        if      ( valNum > mid ) {
470            recBdd = mddIntRetOnvalBdd( mddMgr, valNum, mid, hi, 
471                                        level+1, bddVarArr );
472            onvalBdd = bdd_or( recBdd, curVar, 1, 0 );
473            bdd_free( recBdd );
474        }
475        else if ( valNum < mid ) {
476            recBdd = mddIntRetOnvalBdd( mddMgr, valNum, low, mid, 
477                                        level+1, bddVarArr );
478            onvalBdd = bdd_and( recBdd, curVar, 1, 0 );
479            bdd_free( recBdd );
480        }
481        else if ( valNum == mid ) 
482            onvalBdd = bdd_not( curVar );
483        return( onvalBdd );
484}               /* mddIntRetOnvalBdd */
485
486/************************************************************************/
487/* Given an array of bdd nodes, frees the array.                        */
488
489static void
490mddFreeBddArr(array_t *bddArr)
491{
492        int     i, arrSize;
493
494        arrSize = array_n( bddArr );
495        for ( i = 0 ; i < arrSize ; i++ ) 
496            bdd_free( array_fetch( bdd_t *, bddArr, i ) );
497        array_free( bddArr );
498}               /* mddFreeBddArr */
499
500array_t  *
501mdd_ret_bvars_of_mvar(mvar_type *mvar_ptr)
502{
503        return mvar_ptr->bvars;
504}
505
506/************************************************************************/
507/* mdd_get_care_set returns the care set of the mdd manager */ 
508
509static mdd_t *mdd_get_care_set(mdd_manager *mdd_mgr)
510{
511    mdd_t *temp;
512    mvar_type mv;
513    mdd_manager *bdd_mgr;
514
515    int mvar_id,i,j,val_j,value;
516    array_t *mvar_list;
517    bdd_t *care_set, *care_val, *care_cube,*bit_j;
518   
519    mvar_list = mdd_ret_mvar_list(mdd_mgr);
520    bdd_mgr = mdd_mgr;
521   
522    care_set = bdd_one(bdd_mgr);
523   
524    for (mvar_id =0; mvar_id < array_n(mvar_list); mvar_id++)
525        {
526            mv = array_fetch(mvar_type, mvar_list, mvar_id);
527            care_val = bdd_zero(bdd_mgr);
528               
529            for (i=0; i< (mv.values); i++)
530                {
531                    value = i;
532                    care_cube = bdd_one(bdd_mgr);
533                    for(j=0; j< mv.encode_length; j++ )
534                        {
535                            bit_j = bdd_get_variable(bdd_mgr,mdd_ret_bvar_id(&mv, j));
536                            val_j = value % 2;
537                            value = value/2;
538                            temp = care_cube;
539                            care_cube = bdd_and(temp,bit_j,1,val_j);
540                            bdd_free(temp);
541                        }
542                    temp = care_val;
543                    care_val = bdd_or(temp,care_cube,1,1);
544                    bdd_free(temp);
545                    bdd_free(care_cube);
546                }
547            temp = care_set;
548            care_set = bdd_and(temp,care_val,1,1);
549            bdd_free(care_val);
550            bdd_free(temp);
551        }
552    return care_set;
553}
554
555/* Corrected mdd_cproject */
556/* returns only valid carepoints */
557
558mdd_t *mdd_cproject(
559  mdd_manager *mgr,
560  mdd_t *T,
561  array_t *mvars)
562{
563    mdd_t *care_set, *new_T, *T_proj;
564     array_t *bdd_vars;
565    int i, j, mv_no;
566    mvar_type mv;
567    bdd_t *temp;
568    array_t *mvar_list = mdd_ret_mvar_list(mgr);
569
570
571    care_set = mdd_get_care_set(mgr);
572    new_T = bdd_and(T,care_set,1,1);
573    bdd_free(care_set);
574
575      if ( mvars == NIL(array_t) ) {
576        T_proj = bdd_dup(T);
577        printf("\nWARNING: Empty Array of Smoothing Variables\n");
578        return T_proj;
579    }
580    else if ( array_n(mvars) == 0) {
581        T_proj = bdd_dup(T);
582        printf("\nWARNING: Empty Array of Smoothing Variables\n");
583        return T_proj;
584    }
585               
586       
587    bdd_vars = array_alloc(bdd_t*, 0);     
588    for (i=0; i<array_n(mvars); i++) {
589        mv_no = array_fetch(int, mvars, i);
590        mv = array_fetch(mvar_type, mvar_list, mv_no);
591        if (mv.status == MDD_BUNDLED) {
592            (void) fprintf(stderr, 
593                        "\nmdd_smooth: bundled variable %s used\n",mv.name);
594            fail("");
595        }
596
597        for (j = 0;j < mv.encode_length; j ++) {
598            temp = bdd_get_variable(mgr, mdd_ret_bvar_id(&mv,j) );
599            array_insert_last(bdd_t *, bdd_vars, temp);
600        }
601    }
602       
603 
604    T_proj = bdd_cproject(new_T,bdd_vars);
605    bdd_free(new_T);
606
607    for (i=0; i<array_n(bdd_vars); i++) {
608        temp = array_fetch(bdd_t *, bdd_vars, i);
609        bdd_free(temp);
610    }
611    array_free(bdd_vars);
612
613   
614    return T_proj;
615}
616
617void
618mdd_print_support(mdd_t *f)
619{
620    mdd_manager *mgr = bdd_get_manager(f);
621    array_t *support_list = mdd_get_support(mgr, f);
622    array_t *mvar_list = mdd_ret_mvar_list(mgr);
623    int nSupports = array_n(support_list);
624    int i, j;
625    mvar_type mv;
626    int id;
627
628    for (i = 0; i < nSupports; i++) {
629        id = array_fetch(int, support_list, i);
630        mv = array_fetch(mvar_type, mvar_list, id);
631        if (id == mv.mvar_id)
632            printf("[%d] = %s\n", i, mv.name);
633        else { /* needs to be checked */
634            for (j = 0; j < array_n(mvar_list); j++) {
635                mv = array_fetch(mvar_type, mvar_list, j);
636                if (id == mv.mvar_id) {
637                    printf(" [%d] = %s\n", i, mv.name);
638                    break;
639                }
640            }
641        }
642    }
643
644    array_free(support_list);
645}
646
647void
648mdd_print_support_to_file(FILE *fout, char *format, mdd_t *f)
649{
650    mdd_manager *mgr = bdd_get_manager(f);
651    array_t *support_list = mdd_get_support(mgr, f);
652    array_t *mvar_list = mdd_ret_mvar_list(mgr);
653    int nSupports = array_n(support_list);
654    int i, j;
655    mvar_type mv;
656    int id;
657
658    for (i = 0; i < nSupports; i++) {
659        id = array_fetch(int, support_list, i);
660        mv = array_fetch(mvar_type, mvar_list, id);
661        if (id == mv.mvar_id)
662            fprintf(fout, format, mv.name);
663        else { /* needs to be checked */
664            for (j = 0; j < array_n(mvar_list); j++) {
665                mv = array_fetch(mvar_type, mvar_list, j);
666                if (id == mv.mvar_id) {
667                    fprintf(fout, format, mv.name);
668                    break;
669                }
670            }
671        }
672    }
673
674    array_free(support_list);
675}
676
677char *
678mdd_read_var_name(mdd_t *f)
679{
680    mdd_manager *mgr;
681    array_t *support_list;
682    array_t *mvar_list;
683    int i, id;
684    mvar_type mv;
685
686    if (bdd_size(f) != 2) {
687        fprintf(stderr,
688          "** mdd error: mdd_read_var_name can be called for a variable\n");
689        return(NIL(char));
690    }
691
692    mgr = bdd_get_manager(f);
693    support_list = mdd_get_support(mgr, f);
694    mvar_list = mdd_ret_mvar_list(mgr);
695
696    id = array_fetch(int, support_list, 0);
697    mv = array_fetch(mvar_type, mvar_list, id);
698    if (id == mv.mvar_id) {
699        array_free(support_list);
700        return(mv.name);
701    } else { /* needs to be checked */
702        for (i = 0; i < array_n(mvar_list); i++) {
703            mv = array_fetch(mvar_type, mvar_list, i);
704            if (id == mv.mvar_id) {
705                array_free(support_list);
706                return(mv.name);
707            }
708        }
709    }
710
711    array_free(support_list);
712    return(NIL(char));
713}
714
715int
716mdd_read_mdd_id(mdd_t *f)
717{
718    mdd_manager *mgr;
719    array_t *support_list;
720    int id;
721
722    if (bdd_size(f) != 2) {
723        fprintf(stderr,
724          "** mdd error: mdd_read_mdd_id can be called for a variable\n");
725        return(0);
726    }
727
728    mgr = bdd_get_manager(f);
729    support_list = mdd_get_support(mgr, f);
730    id = array_fetch(int, support_list, 0);
731    array_free(support_list);
732    return(id);
733}
734
735/**Function********************************************************************
736
737  Synopsis    [Returns an array of BDD ids corresponding to a MDD variable.]
738
739  Description [This function takes an MddId. It returns an array of BDD ids
740  corresponding to the bits.]
741
742  SideEffects []
743
744******************************************************************************/
745array_t *
746mdd_id_to_bdd_id_array(mdd_manager *mddManager, int mddId)
747{
748  array_t     *bddIdArray;
749  mvar_type   mddVar;
750  array_t     *mvar_list;
751  int         i, j;
752
753  mvar_list = mdd_ret_mvar_list(mddManager);
754  mddVar = array_fetch(mvar_type, mvar_list, mddId);
755  bddIdArray = array_alloc(int, mddVar.encode_length);
756 
757  for (i=0; i<mddVar.encode_length; i++){
758    j = mdd_ret_bvar_id(&mddVar, i);
759    array_insert_last(int, bddIdArray, j);
760  }
761  return bddIdArray;
762}
763
764/**Function********************************************************************
765
766  Synopsis    [Returns an array of Bdd_t's corresponding to a Mdd variable.]
767
768  Description [This function takes an MddId. It returns an array of bdd_t's
769  corresponding to the bits.]
770
771  SideEffects []
772
773******************************************************************************/
774array_t *
775mdd_id_to_bdd_array(mdd_manager *mddManager, int mddId)
776{
777  array_t       *bddArray;
778  mvar_type     mddVar;
779  int           i, id;
780 
781  mddVar = mddGetVarById(mddManager, mddId);
782  bddArray = array_alloc(bdd_t*, mddVar.encode_length);
783 
784  for (i = 0; i < mddVar.encode_length; i++) {
785    id = mdd_ret_bvar_id(&mddVar, i);
786    array_insert_last(bdd_t*, bddArray, bdd_get_variable(mddManager, id));
787  }
788  return bddArray;
789}
790
791
792/**Function********************************************************************
793
794  Synopsis    [Returns an array of binary vars(bdd_t *) for a given mdd
795  id array.]
796
797  Description []
798
799  SideEffects []
800
801******************************************************************************/
802array_t *
803mdd_id_array_to_bdd_array(mdd_manager *mddManager, array_t *mddIdArray)
804{
805  array_t       *bddArray;
806  int           i, j;
807  int           id, size;
808  mvar_type     mddVar;
809
810  bddArray = array_alloc(bdd_t*, 0);
811  size = array_n(mddIdArray);
812
813  for (i = 0; i < size; i++) {
814    id = array_fetch(int, mddIdArray, i);
815    mddVar = mddGetVarById(mddManager, id);
816    for (j = 0; j < mddVar.encode_length; j++) {
817      id = mdd_ret_bvar_id(&mddVar, j);
818      array_insert_last(bdd_t *, bddArray, bdd_get_variable(mddManager, id));
819    }
820  }
821  return bddArray;
822}
823
824/**Function********************************************************************
825
826  Synopsis    [Returns an array of bddId's corresponding to an array of Mdd
827  ids.]
828
829  Description [This function takes an array of MddId's. For each MddId it
830  returns an array of bddId's corresponding to the bits. These arrays of bddId's
831  are concatenated together and returned.]
832
833  SideEffects []
834
835******************************************************************************/
836array_t *
837mdd_id_array_to_bdd_id_array(mdd_manager *mddManager, array_t *mddIdArray)
838{
839  array_t *bddIdArray;
840  int i;
841
842  bddIdArray = array_alloc(int, 0);
843  for (i=0; i<array_n(mddIdArray); i++){
844    int mddId;
845    array_t *tmpBddIdArray;
846    mddId = array_fetch(int, mddIdArray, i);
847    tmpBddIdArray = mdd_id_to_bdd_id_array(mddManager, mddId);
848    array_append(bddIdArray, tmpBddIdArray);
849    array_free(tmpBddIdArray);
850  }
851  return bddIdArray;
852}
853
854
855/**Function********************************************************************
856
857  Synopsis    [Returns a bdd cube from a given mdd id array.]
858
859  Description []
860
861  SideEffects []
862
863******************************************************************************/
864mdd_t *
865mdd_id_array_to_bdd_cube(mdd_manager *mddManager, array_t *mddIdArray)
866{
867  int           i, j;
868  int           id, size;
869  mvar_type     mddVar;
870  mdd_t         *cube, *var, *tmp;
871  int           nVars;
872  char          *vars;
873
874  size = array_n(mddIdArray);
875  nVars = bdd_num_vars(mddManager);
876  vars = ALLOC(char, sizeof(char) * nVars);
877  memset(vars, 0, sizeof(char) * nVars);
878
879  for (i = 0; i < size; i++) {
880    id = array_fetch(int, mddIdArray, i);
881    mddVar = mddGetVarById(mddManager, id);
882    for (j = 0; j < mddVar.encode_length; j++) {
883      id = mdd_ret_bvar_id(&mddVar, j);
884      vars[bdd_get_level_from_id(mddManager, id)] = 1;
885    }
886  }
887  cube = mdd_one(mddManager);
888  for (i = nVars - 1; i >= 0; i--) {
889    if (vars[i] == 0)
890      continue;
891    id = (int)bdd_get_id_from_level(mddManager, (long)i);
892    var = bdd_get_variable(mddManager, id);
893    tmp = mdd_and(cube, var, 1, 1);
894    mdd_free(cube);
895    mdd_free(var);
896    cube = tmp;
897  }
898  FREE(vars);
899  return cube;
900}
901
902/**Function********************************************************************
903
904  Synopsis    [Returns the number of bdd variables from mdd id array.]
905
906  Description [Returns the number of bdd variables from mdd id array.]
907
908  SideEffects []
909
910******************************************************************************/
911int
912mdd_get_number_of_bdd_vars(mdd_manager *mddManager, array_t *mddIdArray)
913{
914  int i, n;
915
916  n = 0;
917  for (i=0; i<array_n(mddIdArray); i++){
918    int mddId;
919    array_t *tmpBddIdArray;
920    mddId = array_fetch(int, mddIdArray, i);
921    tmpBddIdArray = mdd_id_to_bdd_id_array(mddManager, mddId);
922    n += array_n(tmpBddIdArray);
923    array_free(tmpBddIdArray);
924  }
925  return n;
926}
927
928/**Function********************************************************************
929
930  Synopsis    [Returns the number of bdd support of a mdd.]
931
932  Description [Returns the number of bdd support of a mdd.]
933
934  SideEffects []
935
936******************************************************************************/
937int
938mdd_get_number_of_bdd_support(mdd_manager *mddManager, mdd_t *f)
939{
940    array_t *bvar_list = mdd_ret_bvar_list(mddManager);
941    var_set_t *vset;
942    int i, number = 0;
943
944    vset = bdd_get_support(f);
945    for (i = 0; i < array_n(bvar_list); i++) {
946        if (var_set_get_elt(vset, i) == 1) {
947            number++;
948        }
949    }
950
951    (void) var_set_free(vset);
952    return number;
953}
954
955/**Function********************************************************************
956
957  Synopsis [Given an Mvf representing the functionality of a multi-valued
958  variable, it returns an array of Bdd's representing the characteristic
959  function of the relation of the various bits of the multi-valued variable.]
960
961  Description [Suppose y is a k-valued variable and takes values
962              0,1,..,k-1. Then the input to this function is an array with k
963              Mdds each representing the onset of the respective value of the
964              variable (the ith Mdd representing the onset when y takes the
965              value (i-1). Suppose m bits are needed to encode the k values of
966              y. Then internally y is represented as y_0, y_1, ...,
967              y_(m-1). Now the functionality of each bit of y can be computed
968              by proper boolean operation on the functions representing the
969              onsets of various values of y. For instance if y is a 4-valued
970              variable. To achieve that we do the following:
971              For each bit b{
972                relation = 0;
973                For each value j of the variable{
974                  Ej = Encoding function of the jth value
975                  Fj = Onset function of the jth value
976                  If (b appears in the positive phase in Ej) then
977                     relation += b * Fj
978                  else if (b appears in the negative phase in Ej) then
979                     relation += b'* Fj
980                  else if (b does not appear in Ej) then
981                     relation += Fj
982                }
983              }
984              Note that the above algorithm does not handle the case when a
985              bit appears in both phases in the encoding of any value of the
986              variable. Hence the assumption behind the above algorithm is that
987              the values are encoded as cubes.
988              The case when the encoding are functions can be handled by more
989              complex algorithm. In that case, we will not be able to build the
990              relation for each bit separately. Something to be dealt with in
991              the later work.
992              ]             
993  SideEffects []
994
995******************************************************************************/
996array_t *
997mdd_fn_array_to_bdd_rel_array(
998  mdd_manager *mddManager,
999  int mddId,
1000  array_t *mddFnArray)
1001{
1002  array_t *bddRelationArray, *mddLiteralArray, *valueArray, *bddArray;
1003  mvar_type mddVar;
1004  int i, j, numValues, numEncodingBits;
1005  bdd_t *bdd, *bddRelation, *bddNot;
1006  bdd_t *mddFn, *posCofactor, *negCofactor, *tmpBddRelation;
1007  mdd_t *mddLiteral, *literalRelation;
1008  array_t *mvar_list;
1009 
1010  numValues = array_n(mddFnArray);
1011  /* simple binary case */
1012  if (numValues == 2) {
1013    bdd_t *onRelation, *offRelation;
1014
1015    bddArray = mdd_id_to_bdd_array(mddManager, mddId);
1016    bdd = array_fetch(bdd_t *, bddArray, 0);
1017    array_free(bddArray);
1018    mddFn = array_fetch(mdd_t *, mddFnArray, 0);
1019    offRelation = bdd_and(bdd, mddFn, 0, 1);
1020    mddFn = array_fetch(mdd_t *, mddFnArray, 1);
1021    onRelation = bdd_and(bdd, mddFn, 1, 1);
1022    bdd_free(bdd);
1023    bddRelation = bdd_or(onRelation, offRelation, 1, 1);
1024    bdd_free(onRelation);
1025    bdd_free(offRelation);
1026    bddRelationArray = array_alloc(bdd_t *, 0);
1027    array_insert_last(bdd_t *, bddRelationArray, bddRelation);
1028    return bddRelationArray;
1029  }
1030  mvar_list = mdd_ret_mvar_list(mddManager);
1031  mddVar = array_fetch(mvar_type, mvar_list, mddId);
1032  assert(mddVar.values == numValues);
1033
1034  /*
1035   * The following is to check whether each encoding is cube or not.
1036   * Since Berkeley MDD package always does the cube encoding this checking has
1037   * been turned off currently.
1038   */
1039 
1040  valueArray = array_alloc(int, 1);
1041  mddLiteralArray = array_alloc(mdd_t*, 0);
1042  for (i=0; i<numValues; i++){
1043    array_insert(int, valueArray, 0, i);
1044    /* Form the Mdd corresponding to this value */
1045    mddLiteral = mdd_literal(mddManager, mddId, valueArray);
1046    /* Check if this is a cube */
1047    if (bdd_is_cube(mddLiteral) == FALSE){ 
1048      fprintf(stderr,
1049        "The encoding of the variable %s for the value %d isnot a cube.\n",
1050        mddVar.name, i); 
1051      fprintf(stderr, "It can result in wrong answers.\n");
1052    } 
1053    array_insert_last(mdd_t*, mddLiteralArray, mddLiteral);
1054  }
1055  array_free(valueArray);
1056
1057  bddRelationArray = array_alloc(bdd_t*, 0);
1058  numEncodingBits = mddVar.encode_length;
1059  bddArray = mdd_id_to_bdd_array(mddManager, mddId);
1060  for (i=0; i<numEncodingBits; i++) {
1061    bddRelation = bdd_zero((bdd_manager *)mddManager);
1062    bdd = array_fetch(bdd_t*, bddArray, i);
1063    bddNot = bdd_not(bdd);
1064    for (j=0; j<numValues; j++){
1065      mddLiteral = array_fetch(mdd_t*, mddLiteralArray, j);
1066      mddFn = array_fetch(mdd_t*, mddFnArray, j);
1067      posCofactor = bdd_cofactor(mddLiteral, bdd);
1068      if (bdd_is_tautology(posCofactor, 0)) {
1069        literalRelation = bdd_and(bddNot, mddFn, 1, 1);
1070        bdd_free(posCofactor);
1071      } else {
1072        negCofactor = bdd_cofactor(mddLiteral, bddNot);
1073        if (bdd_is_tautology(negCofactor, 0)) {
1074          literalRelation = bdd_and(bdd, mddFn, 1, 1);
1075        } else {
1076          assert(bdd_equal(posCofactor, negCofactor));
1077          literalRelation = bdd_dup(mddFn);
1078        }
1079        bdd_free(posCofactor);
1080        bdd_free(negCofactor);
1081      }
1082      tmpBddRelation = bdd_or(bddRelation, literalRelation, 1, 1);
1083      bdd_free(literalRelation);
1084      bdd_free(bddRelation);
1085      bddRelation = tmpBddRelation;
1086    }
1087    array_insert_last(bdd_t*, bddRelationArray, bddRelation);
1088    bdd_free(bdd);
1089    bdd_free(bddNot);
1090  }
1091  /* Free stuff */
1092  mdd_array_free(mddLiteralArray);
1093  array_free(bddArray);
1094  return bddRelationArray;
1095}
1096
1097/**Function********************************************************************
1098
1099  Synopsis [Given an Mvf representing the functionality of a multi-valued
1100  variable, it returns an array of Bdd's representing the characteristic
1101  function of the relation of the various bits of the multi-valued variable.]
1102
1103  Description [Suppose y is a k-valued variable and takes values
1104              0,1,..,k-1. Then the input to this function is an array with k
1105              Mdds each representing the onset of the respective value of the
1106              variable (the ith Mdd representing the onset when y takes the
1107              value (i-1). Suppose m bits are needed to encode the k values of
1108              y. Then internally y is represented as y_0, y_1, ...,
1109              y_(m-1). Now the functionality of each bit of y can be computed
1110              by proper boolean operation on the functions representing the
1111              onsets of various values of y. For instance if y is a 4-valued
1112              variable. To achieve that we do the following:
1113              For each bit b{
1114                relation = 0;
1115                For each value j of the variable{
1116                  Ej = Encoding function of the jth value
1117                  Fj = Onset function of the jth value
1118                  If (b appears in the positive phase in Ej) then
1119                     relation += b * Fj
1120                  else if (b appears in the negative phase in Ej) then
1121                     relation += b'* Fj
1122                  else if (b does not appear in Ej) then
1123                     relation += Fj
1124                }
1125              }
1126              Note that the above algorithm does not handle the case when a
1127              bit appears in both phases in the encoding of any value of the
1128              variable. Hence the assumption behind the above algorithm is that
1129              the values are encoded as cubes.
1130              The case when the encoding are functions can be handled by more
1131              complex algorithm. In that case, we will not be able to build the
1132              relation for each bit separately. Something to be dealt with in
1133              the later work.
1134              ]             
1135  SideEffects []
1136
1137******************************************************************************/
1138array_t *
1139mdd_fn_array_to_bdd_fn_array(
1140  mdd_manager *mddManager,
1141  int mddId,
1142  array_t *mddFnArray)
1143{
1144  array_t *bddFunctionArray, *mddLiteralArray, *valueArray, *bddArray;
1145  mvar_type mddVar;
1146  int i, j, numValues, numEncodingBits;
1147  bdd_t *bdd, *bddFunction, *bddNot;
1148  bdd_t *onSet, *offSet, *dcSet, *lower, *upper;
1149  bdd_t *mddFn, *posCofactor, *negCofactor, *tmp;
1150  mdd_t *mddLiteral;
1151  array_t *mvar_list;
1152 
1153  numValues = array_n(mddFnArray);
1154  /* simple binary case */
1155  if (numValues == 2) {
1156    bddFunctionArray = array_alloc(bdd_t *, 0);
1157    mddFn = array_fetch(mdd_t *, mddFnArray, 1);
1158    bddFunction = mdd_dup(mddFn);
1159    array_insert_last(bdd_t *, bddFunctionArray, bddFunction);
1160    return bddFunctionArray;
1161  }
1162  mvar_list = mdd_ret_mvar_list(mddManager);
1163  mddVar = array_fetch(mvar_type, mvar_list, mddId);
1164  assert(mddVar.values == numValues);
1165
1166  /*
1167   * The following is to check whether each encoding is cube or not.
1168   * Since Berkeley MDD package always does the cube encoding this checking has
1169   * been turned off currently.
1170   */
1171 
1172  valueArray = array_alloc(int, 1);
1173  mddLiteralArray = array_alloc(mdd_t*, 0);
1174  for (i=0; i<numValues; i++){
1175    array_insert(int, valueArray, 0, i);
1176    /* Form the Mdd corresponding to this value */
1177    mddLiteral = mdd_literal(mddManager, mddId, valueArray);
1178    /* Check if this is a cube */
1179    if (bdd_is_cube(mddLiteral) == FALSE) {
1180      fprintf(stderr,
1181        "The encoding of the variable %s for the value %d isnot a cube.\n",
1182        mddVar.name, i); 
1183      fprintf(stderr, "It can result in wrong answers.\n");
1184    } 
1185    array_insert_last(mdd_t*, mddLiteralArray, mddLiteral);
1186  }
1187  array_free(valueArray);
1188
1189  bddFunctionArray = array_alloc(bdd_t*, 0);
1190  numEncodingBits = mddVar.encode_length;
1191  bddArray = mdd_id_to_bdd_array(mddManager, mddId);
1192  for (i=0; i<numEncodingBits; i++) {
1193    onSet = bdd_zero((bdd_manager *)mddManager);
1194    offSet = bdd_zero((bdd_manager *)mddManager);
1195    dcSet = bdd_zero((bdd_manager *)mddManager);
1196    bdd = array_fetch(bdd_t*, bddArray, i);
1197    bddNot = bdd_not(bdd);
1198    for (j=0; j<numValues; j++) {
1199      mddLiteral = array_fetch(mdd_t*, mddLiteralArray, j);
1200      posCofactor = bdd_cofactor(mddLiteral, bdd);
1201      mddFn = array_fetch(mdd_t*, mddFnArray, j);
1202
1203      if (bdd_is_tautology(posCofactor, 0)) {
1204        tmp = bdd_or(offSet, mddFn, 1, 1);
1205        bdd_free(offSet);
1206        offSet = tmp;
1207        bdd_free(posCofactor);
1208        continue;
1209      }
1210
1211      negCofactor = bdd_cofactor(mddLiteral, bddNot);
1212      if (bdd_is_tautology(negCofactor, 0)) {
1213        tmp = bdd_or(onSet, mddFn, 1, 1);
1214        bdd_free(onSet);
1215        onSet = tmp;
1216        bdd_free(posCofactor);
1217        bdd_free(negCofactor);
1218        continue;
1219      }
1220
1221      assert(bdd_equal(posCofactor, negCofactor));
1222      bdd_free(posCofactor);
1223      bdd_free(negCofactor);
1224
1225      tmp = bdd_or(dcSet, mddFn, 1, 1);
1226      bdd_free(dcSet);
1227      dcSet = tmp;
1228    }
1229    bdd_free(bdd);
1230    bdd_free(bddNot);
1231    lower = bdd_and(onSet, offSet, 1, 0);
1232    bdd_free(offSet);
1233    upper = bdd_or(onSet, dcSet, 1, 1);
1234    bdd_free(onSet);
1235    bdd_free(dcSet);
1236    bddFunction = bdd_between(lower, upper);
1237    bdd_free(lower);
1238    bdd_free(upper);
1239    array_insert_last(bdd_t*, bddFunctionArray, bddFunction);
1240  }
1241  /* Free stuff */
1242  mdd_array_free(mddLiteralArray);
1243  array_free(bddArray);
1244  return bddFunctionArray;
1245}
1246
1247
1248array_t *
1249mdd_pick_arbitrary_minterms(
1250  mdd_manager   *mddMgr,
1251  mdd_t         *aMdd,
1252  array_t       *mddIdArr,
1253  int           n)
1254{
1255    bdd_t       *onvalBdd, *aOnvalBdd, *onsetBdd, *tmpBdd;
1256    array_t     *bddVarArr;
1257    int         i, arrSize, mddId;
1258    array_t     *mintermArray;
1259
1260    arrSize = array_n( mddIdArr );
1261    onvalBdd = bdd_one( mddMgr );
1262
1263    for ( i = 0 ; i < arrSize ; i++ ) {
1264        mddId = array_fetch( int, mddIdArr, i );
1265        aOnvalBdd = mddRetOnvalBdd( mddMgr, mddId );
1266
1267        tmpBdd = bdd_and( onvalBdd, aOnvalBdd, 1, 1 );
1268        bdd_free( onvalBdd );
1269        bdd_free( aOnvalBdd );
1270        onvalBdd = tmpBdd;
1271    }
1272    onsetBdd = bdd_and( onvalBdd, aMdd, 1, 1 );
1273    bdd_free( onvalBdd );
1274
1275    bddVarArr = mdd_id_array_to_bdd_array(mddMgr, mddIdArr);
1276    mintermArray = bdd_bdd_pick_arbitrary_minterms(onsetBdd, bddVarArr,
1277        array_n(bddVarArr), n);
1278    bdd_free(onsetBdd);
1279    mddFreeBddArr(bddVarArr);
1280    return(mintermArray);
1281}
1282
1283
1284mdd_t *
1285mdd_subset_with_mask_vars(
1286  mdd_manager   *mddMgr,
1287  mdd_t         *aMdd,
1288  array_t       *mddIdArr,
1289  array_t       *maskIdArr)
1290{
1291    bdd_t       *onvalBdd, *aOnvalBdd, *onsetBdd, *tmpBdd;
1292    array_t     *bddVarArr, *maskVarArr;
1293    int         i, arrSize, mddId;
1294    mdd_t       *subset;
1295
1296    arrSize = array_n( mddIdArr );
1297    onvalBdd = bdd_one( mddMgr );
1298
1299    for ( i = 0 ; i < arrSize ; i++ ) {
1300        mddId = array_fetch( int, mddIdArr, i );
1301        aOnvalBdd = mddRetOnvalBdd( mddMgr, mddId );
1302
1303        tmpBdd = bdd_and( onvalBdd, aOnvalBdd, 1, 1 );
1304        bdd_free( onvalBdd );
1305        bdd_free( aOnvalBdd );
1306        onvalBdd = tmpBdd;
1307    }
1308    onsetBdd = bdd_and( onvalBdd, aMdd, 1, 1 );
1309    bdd_free( onvalBdd );
1310
1311    bddVarArr = mdd_id_array_to_bdd_array(mddMgr, mddIdArr);
1312    maskVarArr = mdd_id_array_to_bdd_array(mddMgr, maskIdArr);
1313
1314    subset = bdd_subset_with_mask_vars(onsetBdd, bddVarArr, maskVarArr);
1315    bdd_free(onsetBdd);
1316    mddFreeBddArr(bddVarArr);
1317    mddFreeBddArr(maskVarArr);
1318    return(subset);
1319}
1320
1321
1322/* Internal macro to access the mvar_type structure for each MDD variable. */
1323mvar_type
1324mdd_get_var_by_id(mdd_manager *mddMgr, int id)
1325{
1326    return(mddGetVarById(mddMgr, id));
1327}
1328
1329
1330/* checks whether all support variables of mdd appear in supportIdArray. */
1331int
1332mdd_check_support(
1333  mdd_manager   *mddMgr,
1334  mdd_t         *mdd,
1335  array_t       *supportIdArray)
1336{
1337  int           i, mddId;
1338  st_table      *supportTable = st_init_table(st_numcmp, st_numhash);
1339  array_t       *tmpIdArray;
1340  int           allSupportFlag = 1;
1341
1342  for (i = 0; i < array_n(supportIdArray); i++) {
1343    mddId = array_fetch(int, supportIdArray, i);
1344    st_insert(supportTable, (char *)(long)mddId, NULL);
1345  }
1346
1347  tmpIdArray = mdd_get_support(mddMgr, mdd);
1348  for (i = 0; i < array_n(tmpIdArray); i++) {
1349    mddId = array_fetch(int, tmpIdArray, i);
1350    if (!st_lookup(supportTable, (char *)(long)mddId, NULL)) {
1351      allSupportFlag = 0;
1352      break;
1353    }
1354  }
1355
1356  st_free_table(supportTable);
1357  array_free(tmpIdArray);
1358  return(allSupportFlag);
1359}
1360
1361
1362boolean
1363mdd_equal_mod_care_set_array(mdd_t *aSet, mdd_t *bSet, array_t *careSetArray)
1364{
1365  mdd_t *tmpMdd1, *tmpMdd2;
1366  mdd_t *careSet;
1367  int i;
1368  boolean result;
1369
1370  if (mdd_equal(aSet, bSet))
1371    return 1;
1372
1373  arrayForEachItem(mdd_t *, careSetArray, i, careSet) {
1374    tmpMdd1 = mdd_and(aSet, careSet, 1, 1);
1375    tmpMdd2 = mdd_and(bSet, careSet, 1, 1);
1376
1377    result = mdd_equal(tmpMdd1, tmpMdd2);
1378    mdd_free(tmpMdd1);
1379    mdd_free(tmpMdd2);
1380    if (result == 1)
1381      return 1;
1382  }
1383
1384  return 0;
1385}
1386
1387
1388boolean
1389mdd_lequal_mod_care_set_array(mdd_t *aSet, mdd_t *bSet,
1390                              boolean aPhase, boolean bPhase,
1391                              array_t *careSetArray)
1392{
1393  mdd_t *tmpMdd, *careSet;
1394  int   i, result;
1395
1396  if (mdd_lequal(aSet, bSet, aPhase, bPhase))
1397    return 1;
1398
1399  arrayForEachItem(mdd_t *, careSetArray, i, careSet) {
1400    tmpMdd = mdd_and(aSet, careSet, aPhase, 1);
1401
1402    result = mdd_lequal(tmpMdd, bSet, 1, bPhase);
1403    mdd_free(tmpMdd);
1404    if (result == 1)
1405      return 1;
1406  }
1407
1408  return 0;
1409}
1410
1411
1412/* Return the mdd that represents all valid assignments to the
1413   variables in the support.  Support is an array of mdd_ids. */
1414mdd_t *
1415mdd_range_mdd(
1416  mdd_manager *mgr,
1417  array_t *support
1418  )
1419{
1420  int var, varIndex;      /* iterates over support */
1421  mdd_t *range;
1422
1423  range = mdd_one(mgr);
1424  arrayForEachItem(int, support, varIndex, var){
1425    mdd_t *rangeForVar;
1426    mdd_t *tmp;
1427
1428    rangeForVar = mddRetOnvalBdd(mgr, var);
1429    tmp = mdd_and( rangeForVar, range, 1, 1);
1430    mdd_free(rangeForVar);
1431    mdd_free(range);
1432    range = tmp;
1433  }
1434 
1435  return range;
1436}
1437
1438/*---------------------------------------------------------------------------*/
1439/* Static function prototypes                                                */
1440/*---------------------------------------------------------------------------*/
1441
1442
Note: See TracBrowser for help on using the repository browser.