source: vis_dev/glu-2.1/src/cuBdd/cuddSplit.c @ 6

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

Ajout de glus pour dev VIS mod
File size: 19.0 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddSplit.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Returns a subset of minterms from a boolean function.]
8
9  Description [External functions included in this modoule:
10                <ul>
11                <li> Cudd_SplitSet()
12                </ul>
13        Internal functions included in this module:
14                <ul>
15                <li> cuddSplitSetRecur()
16                </u>
17        Static functions included in this module:
18                <ul>
19                <li> selectMintermsFromUniverse()
20                <li> mintermsFromUniverse()
21                <li> bddAnnotateMintermCount()
22                </ul> ]
23
24  SeeAlso     []
25
26  Author      [Balakrishna Kumthekar]
27
28  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
29
30  All rights reserved.
31
32  Redistribution and use in source and binary forms, with or without
33  modification, are permitted provided that the following conditions
34  are met:
35
36  Redistributions of source code must retain the above copyright
37  notice, this list of conditions and the following disclaimer.
38
39  Redistributions in binary form must reproduce the above copyright
40  notice, this list of conditions and the following disclaimer in the
41  documentation and/or other materials provided with the distribution.
42
43  Neither the name of the University of Colorado nor the names of its
44  contributors may be used to endorse or promote products derived from
45  this software without specific prior written permission.
46
47  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
48  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
49  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
50  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
51  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
52  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
53  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
54  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
55  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
56  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
57  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
58  POSSIBILITY OF SUCH DAMAGE.]
59
60******************************************************************************/
61
62#include "util.h"
63#include "cuddInt.h"
64
65/*---------------------------------------------------------------------------*/
66/* Constant declarations                                                     */
67/*---------------------------------------------------------------------------*/
68
69/*---------------------------------------------------------------------------*/
70/* Type declarations                                                         */
71/*---------------------------------------------------------------------------*/
72
73
74/*---------------------------------------------------------------------------*/
75/* Structure declarations                                                    */
76/*---------------------------------------------------------------------------*/
77
78
79/*---------------------------------------------------------------------------*/
80/* Variable declarations                                                     */
81/*---------------------------------------------------------------------------*/
82
83
84/*---------------------------------------------------------------------------*/
85/* Macro declarations                                                        */
86/*---------------------------------------------------------------------------*/
87
88
89/**AutomaticStart*************************************************************/
90
91/*---------------------------------------------------------------------------*/
92/* Static function prototypes                                                */
93/*---------------------------------------------------------------------------*/
94
95static DdNode * selectMintermsFromUniverse (DdManager *manager, int *varSeen, double n);
96static DdNode * mintermsFromUniverse (DdManager *manager, DdNode **vars, int numVars, double n, int index);
97static double bddAnnotateMintermCount (DdManager *manager, DdNode *node, double max, st_table *table);
98
99/**AutomaticEnd***************************************************************/
100
101
102/*---------------------------------------------------------------------------*/
103/* Definition of exported functions                                          */
104/*---------------------------------------------------------------------------*/
105
106
107/**Function********************************************************************
108
109  Synopsis    [Returns m minterms from a BDD.]
110
111  Description [Returns <code>m</code> minterms from a BDD whose
112  support has <code>n</code> variables at most.  The procedure tries
113  to create as few extra nodes as possible. The function represented
114  by <code>S</code> depends on at most <code>n</code> of the variables
115  in <code>xVars</code>. Returns a BDD with <code>m</code> minterms
116  of the on-set of S if successful; NULL otherwise.]
117
118  SideEffects [None]
119
120  SeeAlso     []
121
122******************************************************************************/
123DdNode *
124Cudd_SplitSet(
125  DdManager * manager,
126  DdNode * S,
127  DdNode ** xVars,
128  int  n,
129  double  m)
130{
131    DdNode *result;
132    DdNode *zero, *one;
133    double  max, num;
134    st_table *mtable;
135    int *varSeen;
136    int i,index, size;
137
138    size = manager->size;
139    one = DD_ONE(manager);
140    zero = Cudd_Not(one);
141
142    /* Trivial cases. */
143    if (m == 0.0) {
144        return(zero);
145    }
146    if (S == zero) {
147        return(NULL);
148    }
149
150    max = pow(2.0,(double)n);
151    if (m > max)
152        return(NULL);
153
154    do {
155        manager->reordered = 0;
156        /* varSeen is used to mark the variables that are encountered
157        ** while traversing the BDD S.
158        */
159        varSeen = ALLOC(int, size);
160        if (varSeen == NULL) {
161            manager->errorCode = CUDD_MEMORY_OUT;
162            return(NULL);
163        }
164        for (i = 0; i < size; i++) {
165            varSeen[i] = -1;
166        }
167        for (i = 0; i < n; i++) {
168            index = (xVars[i])->index;
169            varSeen[manager->invperm[index]] = 0;
170        }
171
172        if (S == one) {
173            if (m == max) 
174                return(S);
175            result = selectMintermsFromUniverse(manager,varSeen,m);
176            if (result)
177                cuddRef(result);
178            FREE(varSeen);
179        } else {
180            mtable = st_init_table(st_ptrcmp,st_ptrhash);
181            if (mtable == NULL) {
182                (void) fprintf(manager->out,
183                               "Cudd_SplitSet: out-of-memory.\n");
184                FREE(varSeen);
185                manager->errorCode = CUDD_MEMORY_OUT;
186                return(NULL);
187            }
188            /* The nodes of BDD S are annotated by the number of minterms
189            ** in their onset. The node and the number of minterms in its
190            ** onset are stored in mtable.
191            */
192            num = bddAnnotateMintermCount(manager,S,max,mtable);
193            if (m == num) {
194                st_foreach(mtable,cuddStCountfree,NIL(char));
195                st_free_table(mtable);
196                FREE(varSeen);
197                return(S);
198            }
199           
200            result = cuddSplitSetRecur(manager,mtable,varSeen,S,m,max,0);
201            if (result)
202                cuddRef(result);
203            st_foreach(mtable,cuddStCountfree,NULL);
204            st_free_table(mtable);
205            FREE(varSeen);
206        }
207    } while (manager->reordered == 1);
208
209    cuddDeref(result);
210    return(result);
211
212} /* end of Cudd_SplitSet */
213
214
215/*---------------------------------------------------------------------------*/
216/* Definition of internal functions                                          */
217/*---------------------------------------------------------------------------*/
218
219/**Function********************************************************************
220
221  Synopsis    [Implements the recursive step of Cudd_SplitSet.]
222
223  Description [Implements the recursive step of Cudd_SplitSet. The
224  procedure recursively traverses the BDD and checks to see if any
225  node satisfies the minterm requirements as specified by 'n'. At any
226  node X, n is compared to the number of minterms in the onset of X's
227  children. If either of the child nodes have exactly n minterms, then
228  that node is returned; else, if n is greater than the onset of one
229  of the child nodes, that node is retained and the difference in the
230  number of minterms is extracted from the other child. In case n
231  minterms can be extracted from constant 1, the algorithm returns the
232  result with at most log(n) nodes.]
233
234  SideEffects [The array 'varSeen' is updated at every recursive call
235  to set the variables traversed by the procedure.]
236
237  SeeAlso     []
238
239******************************************************************************/
240DdNode*
241cuddSplitSetRecur(
242  DdManager * manager,
243  st_table * mtable,
244  int * varSeen,
245  DdNode * p,
246  double  n,
247  double  max,
248  int  index)
249{
250    DdNode *one, *zero, *N, *Nv;
251    DdNode *Nnv, *q, *r, *v;
252    DdNode *result;
253    double *dummy, numT, numE;
254    int variable, positive;
255 
256    statLine(manager);
257    one = DD_ONE(manager);
258    zero = Cudd_Not(one);
259
260    /* If p is constant, extract n minterms from constant 1.  The procedure by
261    ** construction guarantees that minterms will not be extracted from
262    ** constant 0.
263    */
264    if (Cudd_IsConstant(p)) {
265        q = selectMintermsFromUniverse(manager,varSeen,n);
266        return(q);
267    }
268
269    N = Cudd_Regular(p);
270
271    /* Set variable as seen. */
272    variable = N->index;
273    varSeen[manager->invperm[variable]] = -1;
274
275    Nv = cuddT(N);
276    Nnv = cuddE(N);
277    if (Cudd_IsComplement(p)) {
278        Nv = Cudd_Not(Nv);
279        Nnv = Cudd_Not(Nnv);
280    }
281
282    /* If both the children of 'p' are constants, extract n minterms from a
283    ** constant node.
284    */
285    if (Cudd_IsConstant(Nv) && Cudd_IsConstant(Nnv)) {
286        q = selectMintermsFromUniverse(manager,varSeen,n);
287        if (q == NULL) {
288            return(NULL);
289        }
290        cuddRef(q);
291        r = cuddBddAndRecur(manager,p,q);
292        if (r == NULL) {
293            Cudd_RecursiveDeref(manager,q);
294            return(NULL);
295        }
296        cuddRef(r);
297        Cudd_RecursiveDeref(manager,q);
298        cuddDeref(r);
299        return(r);
300    }
301 
302    /* Lookup the # of minterms in the onset of the node from the table. */
303    if (!Cudd_IsConstant(Nv)) {
304        st_lookup(mtable, Nv, &dummy);
305        numT = *dummy/(2*(1<<index));
306    } else if (Nv == one) {
307        numT = max/(2*(1<<index));
308    } else {
309        numT = 0;
310    }
311 
312    if (!Cudd_IsConstant(Nnv)) {
313        st_lookup(mtable, Nnv, &dummy);
314        numE = *dummy/(2*(1<<index));
315    } else if (Nnv == one) {
316        numE = max/(2*(1<<index));
317    } else {
318        numE = 0;
319    }
320
321    v = cuddUniqueInter(manager,variable,one,zero);
322    cuddRef(v);
323
324    /* If perfect match. */
325    if (numT == n) {
326        q = cuddBddAndRecur(manager,v,Nv);
327        if (q == NULL) {
328            Cudd_RecursiveDeref(manager,v);
329            return(NULL);
330        }
331        cuddRef(q);
332        Cudd_RecursiveDeref(manager,v);
333        cuddDeref(q);
334        return(q);
335    }
336    if (numE == n) {
337        q = cuddBddAndRecur(manager,Cudd_Not(v),Nnv);
338        if (q == NULL) {
339            Cudd_RecursiveDeref(manager,v);
340            return(NULL);
341        }
342        cuddRef(q);
343        Cudd_RecursiveDeref(manager,v);
344        cuddDeref(q);
345        return(q);
346    }
347    /* If n is greater than numT, extract the difference from the ELSE child
348    ** and retain the function represented by the THEN branch.
349    */
350    if (numT < n) {
351        q = cuddSplitSetRecur(manager,mtable,varSeen,
352                              Nnv,(n-numT),max,index+1);
353        if (q == NULL) {
354            Cudd_RecursiveDeref(manager,v);
355            return(NULL);
356        }
357        cuddRef(q);
358        r = cuddBddIteRecur(manager,v,Nv,q);
359        if (r == NULL) {
360            Cudd_RecursiveDeref(manager,q);
361            Cudd_RecursiveDeref(manager,v);
362            return(NULL);
363        }
364        cuddRef(r);
365        Cudd_RecursiveDeref(manager,q);
366        Cudd_RecursiveDeref(manager,v);
367        cuddDeref(r);
368        return(r);
369    }
370    /* If n is greater than numE, extract the difference from the THEN child
371    ** and retain the function represented by the ELSE branch.
372    */
373    if (numE < n) {
374        q = cuddSplitSetRecur(manager,mtable,varSeen,
375                              Nv, (n-numE),max,index+1);
376        if (q == NULL) {
377            Cudd_RecursiveDeref(manager,v);
378            return(NULL);
379        }
380        cuddRef(q);
381        r = cuddBddIteRecur(manager,v,q,Nnv);
382        if (r == NULL) {
383            Cudd_RecursiveDeref(manager,q);
384            Cudd_RecursiveDeref(manager,v);
385            return(NULL);
386        }
387        cuddRef(r);
388        Cudd_RecursiveDeref(manager,q);
389        Cudd_RecursiveDeref(manager,v);
390        cuddDeref(r);   
391        return(r);
392    }
393
394    /* None of the above cases; (n < numT and n < numE) and either of
395    ** the Nv, Nnv or both are not constants. If possible extract the
396    ** required minterms the constant branch.
397    */
398    if (Cudd_IsConstant(Nv) && !Cudd_IsConstant(Nnv)) {
399        q = selectMintermsFromUniverse(manager,varSeen,n);
400        if (q == NULL) {
401            Cudd_RecursiveDeref(manager,v);
402            return(NULL);
403        }
404        cuddRef(q);
405        result = cuddBddAndRecur(manager,v,q);
406        if (result == NULL) {
407            Cudd_RecursiveDeref(manager,q);
408            Cudd_RecursiveDeref(manager,v);
409            return(NULL);
410        }
411        cuddRef(result);
412        Cudd_RecursiveDeref(manager,q);
413        Cudd_RecursiveDeref(manager,v);
414        cuddDeref(result);
415        return(result);
416    } else if (!Cudd_IsConstant(Nv) && Cudd_IsConstant(Nnv)) {
417        q = selectMintermsFromUniverse(manager,varSeen,n);
418        if (q == NULL) {
419            Cudd_RecursiveDeref(manager,v);
420            return(NULL);
421        }
422        cuddRef(q);
423        result = cuddBddAndRecur(manager,Cudd_Not(v),q);
424        if (result == NULL) {
425            Cudd_RecursiveDeref(manager,q);
426            Cudd_RecursiveDeref(manager,v);
427            return(NULL);
428        }
429        cuddRef(result);
430        Cudd_RecursiveDeref(manager,q);
431        Cudd_RecursiveDeref(manager,v);
432        cuddDeref(result);
433        return(result);
434    }
435
436    /* Both Nv and Nnv are not constants. So choose the one which
437    ** has fewer minterms in its onset.
438    */
439    positive = 0;
440    if (numT < numE) {
441        q = cuddSplitSetRecur(manager,mtable,varSeen,
442                              Nv,n,max,index+1);
443        positive = 1;
444    } else {
445        q = cuddSplitSetRecur(manager,mtable,varSeen,
446                              Nnv,n,max,index+1);
447    }
448
449    if (q == NULL) {
450        Cudd_RecursiveDeref(manager,v);
451        return(NULL);
452    }
453    cuddRef(q);
454
455    if (positive) {
456        result = cuddBddAndRecur(manager,v,q);
457    } else {
458        result = cuddBddAndRecur(manager,Cudd_Not(v),q);
459    }
460    if (result == NULL) {
461        Cudd_RecursiveDeref(manager,q);
462        Cudd_RecursiveDeref(manager,v);
463        return(NULL);
464    }
465    cuddRef(result);
466    Cudd_RecursiveDeref(manager,q);
467    Cudd_RecursiveDeref(manager,v);
468    cuddDeref(result);
469
470    return(result);
471
472} /* end of cuddSplitSetRecur */
473
474
475/*---------------------------------------------------------------------------*/
476/* Definition of static functions                                            */
477/*---------------------------------------------------------------------------*/
478
479/**Function********************************************************************
480
481  Synopsis [This function prepares an array of variables which have not been
482  encountered so far when traversing the procedure cuddSplitSetRecur.]
483
484  Description [This function prepares an array of variables which have not been
485  encountered so far when traversing the procedure cuddSplitSetRecur. This
486  array is then used to extract the required number of minterms from a constant
487  1. The algorithm guarantees that the size of BDD will be utmost \log(n).]
488
489  SideEffects [None]
490
491******************************************************************************/
492static DdNode *
493selectMintermsFromUniverse(
494  DdManager * manager,
495  int * varSeen,
496  double  n)
497{
498    int numVars;
499    int i, size, j;
500     DdNode *one, *zero, *result;
501    DdNode **vars;
502
503    numVars = 0;
504    size = manager->size;
505    one = DD_ONE(manager);
506    zero = Cudd_Not(one);
507
508    /* Count the number of variables not encountered so far in procedure
509    ** cuddSplitSetRecur.
510    */
511    for (i = size-1; i >= 0; i--) {
512        if(varSeen[i] == 0)
513            numVars++;
514    }
515    vars = ALLOC(DdNode *, numVars);
516    if (!vars) {
517        manager->errorCode = CUDD_MEMORY_OUT;
518        return(NULL);
519    }
520
521    j = 0;
522    for (i = size-1; i >= 0; i--) {
523        if(varSeen[i] == 0) {
524            vars[j] = cuddUniqueInter(manager,manager->perm[i],one,zero);
525            cuddRef(vars[j]);
526            j++;
527        }
528    }
529
530    /* Compute a function which has n minterms and depends on at most
531    ** numVars variables.
532    */
533    result = mintermsFromUniverse(manager,vars,numVars,n, 0);
534    if (result) 
535        cuddRef(result);
536
537    for (i = 0; i < numVars; i++)
538        Cudd_RecursiveDeref(manager,vars[i]);
539    FREE(vars);
540
541    return(result);
542
543} /* end of selectMintermsFromUniverse */
544
545
546/**Function********************************************************************
547
548  Synopsis    [Recursive procedure to extract n mintems from constant 1.]
549
550  Description [Recursive procedure to extract n mintems from constant 1.]
551
552  SideEffects [None]
553
554******************************************************************************/
555static DdNode *
556mintermsFromUniverse(
557  DdManager * manager,
558  DdNode ** vars,
559  int  numVars,
560  double  n,
561  int  index)
562{
563    DdNode *one, *zero;
564    DdNode *q, *result;
565    double max, max2;
566   
567    statLine(manager);
568    one = DD_ONE(manager);
569    zero = Cudd_Not(one);
570
571    max = pow(2.0, (double)numVars);
572    max2 = max / 2.0;
573
574    if (n == max)
575        return(one);
576    if (n == 0.0)
577        return(zero);
578    /* if n == 2^(numVars-1), return a single variable */
579    if (n == max2)
580        return vars[index];
581    else if (n > max2) {
582        /* When n > 2^(numVars-1), a single variable vars[index]
583        ** contains 2^(numVars-1) minterms. The rest are extracted
584        ** from a constant with 1 less variable.
585        */
586        q = mintermsFromUniverse(manager,vars,numVars-1,(n-max2),index+1);
587        if (q == NULL)
588            return(NULL);
589        cuddRef(q);
590        result = cuddBddIteRecur(manager,vars[index],one,q);
591    } else {
592        /* When n < 2^(numVars-1), a literal of variable vars[index]
593        ** is selected. The required n minterms are extracted from a
594        ** constant with 1 less variable.
595        */
596        q = mintermsFromUniverse(manager,vars,numVars-1,n,index+1);
597        if (q == NULL)
598            return(NULL);
599        cuddRef(q);
600        result = cuddBddAndRecur(manager,vars[index],q);
601    }
602   
603    if (result == NULL) {
604        Cudd_RecursiveDeref(manager,q);
605        return(NULL);
606    }
607    cuddRef(result);
608    Cudd_RecursiveDeref(manager,q);
609    cuddDeref(result);
610    return(result);
611
612} /* end of mintermsFromUniverse */
613
614
615/**Function********************************************************************
616
617  Synopsis    [Annotates every node in the BDD node with its minterm count.]
618
619  Description [Annotates every node in the BDD node with its minterm count.
620  In this function, every node and the minterm count represented by it are
621  stored in a hash table.]
622
623  SideEffects [Fills up 'table' with the pair <node,minterm_count>.]
624
625******************************************************************************/
626static double
627bddAnnotateMintermCount(
628  DdManager * manager,
629  DdNode * node,
630  double  max,
631  st_table * table)
632{
633
634    DdNode *N,*Nv,*Nnv;
635    register double min_v,min_nv;
636    register double min_N;
637    double *pmin;
638    double *dummy;
639
640    statLine(manager);
641    N = Cudd_Regular(node);
642    if (cuddIsConstant(N)) {
643        if (node == DD_ONE(manager)) {
644            return(max);
645        } else {
646            return(0.0);
647        }
648    }
649
650    if (st_lookup(table, node, &dummy)) {
651        return(*dummy);
652    }   
653 
654    Nv = cuddT(N);
655    Nnv = cuddE(N);
656    if (N != node) {
657        Nv = Cudd_Not(Nv);
658        Nnv = Cudd_Not(Nnv);
659    }
660
661    /* Recur on the two branches. */
662    min_v  = bddAnnotateMintermCount(manager,Nv,max,table) / 2.0;
663    if (min_v == (double)CUDD_OUT_OF_MEM)
664        return ((double)CUDD_OUT_OF_MEM);
665    min_nv = bddAnnotateMintermCount(manager,Nnv,max,table) / 2.0;
666    if (min_nv == (double)CUDD_OUT_OF_MEM)
667        return ((double)CUDD_OUT_OF_MEM);
668    min_N  = min_v + min_nv;
669
670    pmin = ALLOC(double,1);
671    if (pmin == NULL) {
672        manager->errorCode = CUDD_MEMORY_OUT;
673        return((double)CUDD_OUT_OF_MEM);
674    }
675    *pmin = min_N;
676
677    if (st_insert(table,(char *)node, (char *)pmin) == ST_OUT_OF_MEM) {
678        FREE(pmin);
679        return((double)CUDD_OUT_OF_MEM);
680    }
681   
682    return(min_N);
683
684} /* end of bddAnnotateMintermCount */
Note: See TracBrowser for help on using the repository browser.