source: vis_dev/glu-2.3/src/cuBdd/cuddSplit.c @ 27

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

library glu 2.3
File size: 19.1 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                FREE(varSeen);
175                return(S);
176            }
177            result = selectMintermsFromUniverse(manager,varSeen,m);
178            if (result)
179                cuddRef(result);
180            FREE(varSeen);
181        } else {
182            mtable = st_init_table(st_ptrcmp,st_ptrhash);
183            if (mtable == NULL) {
184                (void) fprintf(manager->out,
185                               "Cudd_SplitSet: out-of-memory.\n");
186                FREE(varSeen);
187                manager->errorCode = CUDD_MEMORY_OUT;
188                return(NULL);
189            }
190            /* The nodes of BDD S are annotated by the number of minterms
191            ** in their onset. The node and the number of minterms in its
192            ** onset are stored in mtable.
193            */
194            num = bddAnnotateMintermCount(manager,S,max,mtable);
195            if (m == num) {
196                st_foreach(mtable,cuddStCountfree,NIL(char));
197                st_free_table(mtable);
198                FREE(varSeen);
199                return(S);
200            }
201           
202            result = cuddSplitSetRecur(manager,mtable,varSeen,S,m,max,0);
203            if (result)
204                cuddRef(result);
205            st_foreach(mtable,cuddStCountfree,NULL);
206            st_free_table(mtable);
207            FREE(varSeen);
208        }
209    } while (manager->reordered == 1);
210
211    cuddDeref(result);
212    return(result);
213
214} /* end of Cudd_SplitSet */
215
216
217/*---------------------------------------------------------------------------*/
218/* Definition of internal functions                                          */
219/*---------------------------------------------------------------------------*/
220
221/**Function********************************************************************
222
223  Synopsis    [Implements the recursive step of Cudd_SplitSet.]
224
225  Description [Implements the recursive step of Cudd_SplitSet. The
226  procedure recursively traverses the BDD and checks to see if any
227  node satisfies the minterm requirements as specified by 'n'. At any
228  node X, n is compared to the number of minterms in the onset of X's
229  children. If either of the child nodes have exactly n minterms, then
230  that node is returned; else, if n is greater than the onset of one
231  of the child nodes, that node is retained and the difference in the
232  number of minterms is extracted from the other child. In case n
233  minterms can be extracted from constant 1, the algorithm returns the
234  result with at most log(n) nodes.]
235
236  SideEffects [The array 'varSeen' is updated at every recursive call
237  to set the variables traversed by the procedure.]
238
239  SeeAlso     []
240
241******************************************************************************/
242DdNode*
243cuddSplitSetRecur(
244  DdManager * manager,
245  st_table * mtable,
246  int * varSeen,
247  DdNode * p,
248  double  n,
249  double  max,
250  int  index)
251{
252    DdNode *one, *zero, *N, *Nv;
253    DdNode *Nnv, *q, *r, *v;
254    DdNode *result;
255    double *dummy, numT, numE;
256    int variable, positive;
257 
258    statLine(manager);
259    one = DD_ONE(manager);
260    zero = Cudd_Not(one);
261
262    /* If p is constant, extract n minterms from constant 1.  The procedure by
263    ** construction guarantees that minterms will not be extracted from
264    ** constant 0.
265    */
266    if (Cudd_IsConstant(p)) {
267        q = selectMintermsFromUniverse(manager,varSeen,n);
268        return(q);
269    }
270
271    N = Cudd_Regular(p);
272
273    /* Set variable as seen. */
274    variable = N->index;
275    varSeen[manager->invperm[variable]] = -1;
276
277    Nv = cuddT(N);
278    Nnv = cuddE(N);
279    if (Cudd_IsComplement(p)) {
280        Nv = Cudd_Not(Nv);
281        Nnv = Cudd_Not(Nnv);
282    }
283
284    /* If both the children of 'p' are constants, extract n minterms from a
285    ** constant node.
286    */
287    if (Cudd_IsConstant(Nv) && Cudd_IsConstant(Nnv)) {
288        q = selectMintermsFromUniverse(manager,varSeen,n);
289        if (q == NULL) {
290            return(NULL);
291        }
292        cuddRef(q);
293        r = cuddBddAndRecur(manager,p,q);
294        if (r == NULL) {
295            Cudd_RecursiveDeref(manager,q);
296            return(NULL);
297        }
298        cuddRef(r);
299        Cudd_RecursiveDeref(manager,q);
300        cuddDeref(r);
301        return(r);
302    }
303 
304    /* Lookup the # of minterms in the onset of the node from the table. */
305    if (!Cudd_IsConstant(Nv)) {
306        if (!st_lookup(mtable, Nv, &dummy)) return(NULL);
307        numT = *dummy/(2*(1<<index));
308    } else if (Nv == one) {
309        numT = max/(2*(1<<index));
310    } else {
311        numT = 0;
312    }
313 
314    if (!Cudd_IsConstant(Nnv)) {
315        if (!st_lookup(mtable, Nnv, &dummy)) return(NULL);
316        numE = *dummy/(2*(1<<index));
317    } else if (Nnv == one) {
318        numE = max/(2*(1<<index));
319    } else {
320        numE = 0;
321    }
322
323    v = cuddUniqueInter(manager,variable,one,zero);
324    cuddRef(v);
325
326    /* If perfect match. */
327    if (numT == n) {
328        q = cuddBddAndRecur(manager,v,Nv);
329        if (q == NULL) {
330            Cudd_RecursiveDeref(manager,v);
331            return(NULL);
332        }
333        cuddRef(q);
334        Cudd_RecursiveDeref(manager,v);
335        cuddDeref(q);
336        return(q);
337    }
338    if (numE == n) {
339        q = cuddBddAndRecur(manager,Cudd_Not(v),Nnv);
340        if (q == NULL) {
341            Cudd_RecursiveDeref(manager,v);
342            return(NULL);
343        }
344        cuddRef(q);
345        Cudd_RecursiveDeref(manager,v);
346        cuddDeref(q);
347        return(q);
348    }
349    /* If n is greater than numT, extract the difference from the ELSE child
350    ** and retain the function represented by the THEN branch.
351    */
352    if (numT < n) {
353        q = cuddSplitSetRecur(manager,mtable,varSeen,
354                              Nnv,(n-numT),max,index+1);
355        if (q == NULL) {
356            Cudd_RecursiveDeref(manager,v);
357            return(NULL);
358        }
359        cuddRef(q);
360        r = cuddBddIteRecur(manager,v,Nv,q);
361        if (r == NULL) {
362            Cudd_RecursiveDeref(manager,q);
363            Cudd_RecursiveDeref(manager,v);
364            return(NULL);
365        }
366        cuddRef(r);
367        Cudd_RecursiveDeref(manager,q);
368        Cudd_RecursiveDeref(manager,v);
369        cuddDeref(r);
370        return(r);
371    }
372    /* If n is greater than numE, extract the difference from the THEN child
373    ** and retain the function represented by the ELSE branch.
374    */
375    if (numE < n) {
376        q = cuddSplitSetRecur(manager,mtable,varSeen,
377                              Nv, (n-numE),max,index+1);
378        if (q == NULL) {
379            Cudd_RecursiveDeref(manager,v);
380            return(NULL);
381        }
382        cuddRef(q);
383        r = cuddBddIteRecur(manager,v,q,Nnv);
384        if (r == NULL) {
385            Cudd_RecursiveDeref(manager,q);
386            Cudd_RecursiveDeref(manager,v);
387            return(NULL);
388        }
389        cuddRef(r);
390        Cudd_RecursiveDeref(manager,q);
391        Cudd_RecursiveDeref(manager,v);
392        cuddDeref(r);   
393        return(r);
394    }
395
396    /* None of the above cases; (n < numT and n < numE) and either of
397    ** the Nv, Nnv or both are not constants. If possible extract the
398    ** required minterms the constant branch.
399    */
400    if (Cudd_IsConstant(Nv) && !Cudd_IsConstant(Nnv)) {
401        q = selectMintermsFromUniverse(manager,varSeen,n);
402        if (q == NULL) {
403            Cudd_RecursiveDeref(manager,v);
404            return(NULL);
405        }
406        cuddRef(q);
407        result = cuddBddAndRecur(manager,v,q);
408        if (result == NULL) {
409            Cudd_RecursiveDeref(manager,q);
410            Cudd_RecursiveDeref(manager,v);
411            return(NULL);
412        }
413        cuddRef(result);
414        Cudd_RecursiveDeref(manager,q);
415        Cudd_RecursiveDeref(manager,v);
416        cuddDeref(result);
417        return(result);
418    } else if (!Cudd_IsConstant(Nv) && Cudd_IsConstant(Nnv)) {
419        q = selectMintermsFromUniverse(manager,varSeen,n);
420        if (q == NULL) {
421            Cudd_RecursiveDeref(manager,v);
422            return(NULL);
423        }
424        cuddRef(q);
425        result = cuddBddAndRecur(manager,Cudd_Not(v),q);
426        if (result == NULL) {
427            Cudd_RecursiveDeref(manager,q);
428            Cudd_RecursiveDeref(manager,v);
429            return(NULL);
430        }
431        cuddRef(result);
432        Cudd_RecursiveDeref(manager,q);
433        Cudd_RecursiveDeref(manager,v);
434        cuddDeref(result);
435        return(result);
436    }
437
438    /* Both Nv and Nnv are not constants. So choose the one which
439    ** has fewer minterms in its onset.
440    */
441    positive = 0;
442    if (numT < numE) {
443        q = cuddSplitSetRecur(manager,mtable,varSeen,
444                              Nv,n,max,index+1);
445        positive = 1;
446    } else {
447        q = cuddSplitSetRecur(manager,mtable,varSeen,
448                              Nnv,n,max,index+1);
449    }
450
451    if (q == NULL) {
452        Cudd_RecursiveDeref(manager,v);
453        return(NULL);
454    }
455    cuddRef(q);
456
457    if (positive) {
458        result = cuddBddAndRecur(manager,v,q);
459    } else {
460        result = cuddBddAndRecur(manager,Cudd_Not(v),q);
461    }
462    if (result == NULL) {
463        Cudd_RecursiveDeref(manager,q);
464        Cudd_RecursiveDeref(manager,v);
465        return(NULL);
466    }
467    cuddRef(result);
468    Cudd_RecursiveDeref(manager,q);
469    Cudd_RecursiveDeref(manager,v);
470    cuddDeref(result);
471
472    return(result);
473
474} /* end of cuddSplitSetRecur */
475
476
477/*---------------------------------------------------------------------------*/
478/* Definition of static functions                                            */
479/*---------------------------------------------------------------------------*/
480
481/**Function********************************************************************
482
483  Synopsis [This function prepares an array of variables which have not been
484  encountered so far when traversing the procedure cuddSplitSetRecur.]
485
486  Description [This function prepares an array of variables which have not been
487  encountered so far when traversing the procedure cuddSplitSetRecur. This
488  array is then used to extract the required number of minterms from a constant
489  1. The algorithm guarantees that the size of BDD will be utmost \log(n).]
490
491  SideEffects [None]
492
493******************************************************************************/
494static DdNode *
495selectMintermsFromUniverse(
496  DdManager * manager,
497  int * varSeen,
498  double  n)
499{
500    int numVars;
501    int i, size, j;
502     DdNode *one, *zero, *result;
503    DdNode **vars;
504
505    numVars = 0;
506    size = manager->size;
507    one = DD_ONE(manager);
508    zero = Cudd_Not(one);
509
510    /* Count the number of variables not encountered so far in procedure
511    ** cuddSplitSetRecur.
512    */
513    for (i = size-1; i >= 0; i--) {
514        if(varSeen[i] == 0)
515            numVars++;
516    }
517    vars = ALLOC(DdNode *, numVars);
518    if (!vars) {
519        manager->errorCode = CUDD_MEMORY_OUT;
520        return(NULL);
521    }
522
523    j = 0;
524    for (i = size-1; i >= 0; i--) {
525        if(varSeen[i] == 0) {
526            vars[j] = cuddUniqueInter(manager,manager->perm[i],one,zero);
527            cuddRef(vars[j]);
528            j++;
529        }
530    }
531
532    /* Compute a function which has n minterms and depends on at most
533    ** numVars variables.
534    */
535    result = mintermsFromUniverse(manager,vars,numVars,n, 0);
536    if (result) 
537        cuddRef(result);
538
539    for (i = 0; i < numVars; i++)
540        Cudd_RecursiveDeref(manager,vars[i]);
541    FREE(vars);
542
543    return(result);
544
545} /* end of selectMintermsFromUniverse */
546
547
548/**Function********************************************************************
549
550  Synopsis    [Recursive procedure to extract n mintems from constant 1.]
551
552  Description [Recursive procedure to extract n mintems from constant 1.]
553
554  SideEffects [None]
555
556******************************************************************************/
557static DdNode *
558mintermsFromUniverse(
559  DdManager * manager,
560  DdNode ** vars,
561  int  numVars,
562  double  n,
563  int  index)
564{
565    DdNode *one, *zero;
566    DdNode *q, *result;
567    double max, max2;
568   
569    statLine(manager);
570    one = DD_ONE(manager);
571    zero = Cudd_Not(one);
572
573    max = pow(2.0, (double)numVars);
574    max2 = max / 2.0;
575
576    if (n == max)
577        return(one);
578    if (n == 0.0)
579        return(zero);
580    /* if n == 2^(numVars-1), return a single variable */
581    if (n == max2)
582        return vars[index];
583    else if (n > max2) {
584        /* When n > 2^(numVars-1), a single variable vars[index]
585        ** contains 2^(numVars-1) minterms. The rest are extracted
586        ** from a constant with 1 less variable.
587        */
588        q = mintermsFromUniverse(manager,vars,numVars-1,(n-max2),index+1);
589        if (q == NULL)
590            return(NULL);
591        cuddRef(q);
592        result = cuddBddIteRecur(manager,vars[index],one,q);
593    } else {
594        /* When n < 2^(numVars-1), a literal of variable vars[index]
595        ** is selected. The required n minterms are extracted from a
596        ** constant with 1 less variable.
597        */
598        q = mintermsFromUniverse(manager,vars,numVars-1,n,index+1);
599        if (q == NULL)
600            return(NULL);
601        cuddRef(q);
602        result = cuddBddAndRecur(manager,vars[index],q);
603    }
604   
605    if (result == NULL) {
606        Cudd_RecursiveDeref(manager,q);
607        return(NULL);
608    }
609    cuddRef(result);
610    Cudd_RecursiveDeref(manager,q);
611    cuddDeref(result);
612    return(result);
613
614} /* end of mintermsFromUniverse */
615
616
617/**Function********************************************************************
618
619  Synopsis    [Annotates every node in the BDD node with its minterm count.]
620
621  Description [Annotates every node in the BDD node with its minterm count.
622  In this function, every node and the minterm count represented by it are
623  stored in a hash table.]
624
625  SideEffects [Fills up 'table' with the pair <node,minterm_count>.]
626
627******************************************************************************/
628static double
629bddAnnotateMintermCount(
630  DdManager * manager,
631  DdNode * node,
632  double  max,
633  st_table * table)
634{
635
636    DdNode *N,*Nv,*Nnv;
637    register double min_v,min_nv;
638    register double min_N;
639    double *pmin;
640    double *dummy;
641
642    statLine(manager);
643    N = Cudd_Regular(node);
644    if (cuddIsConstant(N)) {
645        if (node == DD_ONE(manager)) {
646            return(max);
647        } else {
648            return(0.0);
649        }
650    }
651
652    if (st_lookup(table, node, &dummy)) {
653        return(*dummy);
654    }   
655 
656    Nv = cuddT(N);
657    Nnv = cuddE(N);
658    if (N != node) {
659        Nv = Cudd_Not(Nv);
660        Nnv = Cudd_Not(Nnv);
661    }
662
663    /* Recur on the two branches. */
664    min_v  = bddAnnotateMintermCount(manager,Nv,max,table) / 2.0;
665    if (min_v == (double)CUDD_OUT_OF_MEM)
666        return ((double)CUDD_OUT_OF_MEM);
667    min_nv = bddAnnotateMintermCount(manager,Nnv,max,table) / 2.0;
668    if (min_nv == (double)CUDD_OUT_OF_MEM)
669        return ((double)CUDD_OUT_OF_MEM);
670    min_N  = min_v + min_nv;
671
672    pmin = ALLOC(double,1);
673    if (pmin == NULL) {
674        manager->errorCode = CUDD_MEMORY_OUT;
675        return((double)CUDD_OUT_OF_MEM);
676    }
677    *pmin = min_N;
678
679    if (st_insert(table,(char *)node, (char *)pmin) == ST_OUT_OF_MEM) {
680        FREE(pmin);
681        return((double)CUDD_OUT_OF_MEM);
682    }
683   
684    return(min_N);
685
686} /* end of bddAnnotateMintermCount */
Note: See TracBrowser for help on using the repository browser.