1 /**CFile***********************************************************************
7 Synopsis [Returns a subset of minterms from a boolean function.]
9 Description [External functions included in this modoule:
13 Internal functions included in this module:
15 <li> cuddSplitSetRecur()
17 Static functions included in this module:
19 <li> selectMintermsFromUniverse()
20 <li> mintermsFromUniverse()
21 <li> bddAnnotateMintermCount()
26 Author [Balakrishna Kumthekar]
28 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
32 Redistribution and use in source and binary forms, with or without
33 modification, are permitted provided that the following conditions
36 Redistributions of source code must retain the above copyright
37 notice, this list of conditions and the following disclaimer.
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.
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.
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.]
60 ******************************************************************************/
65 /*---------------------------------------------------------------------------*/
66 /* Constant declarations */
67 /*---------------------------------------------------------------------------*/
69 /*---------------------------------------------------------------------------*/
70 /* Type declarations */
71 /*---------------------------------------------------------------------------*/
74 /*---------------------------------------------------------------------------*/
75 /* Structure declarations */
76 /*---------------------------------------------------------------------------*/
79 /*---------------------------------------------------------------------------*/
80 /* Variable declarations */
81 /*---------------------------------------------------------------------------*/
84 /*---------------------------------------------------------------------------*/
85 /* Macro declarations */
86 /*---------------------------------------------------------------------------*/
89 /**AutomaticStart*************************************************************/
91 /*---------------------------------------------------------------------------*/
92 /* Static function prototypes */
93 /*---------------------------------------------------------------------------*/
95 static DdNode
* selectMintermsFromUniverse (DdManager
*manager
, int *varSeen
, double n
);
96 static DdNode
* mintermsFromUniverse (DdManager
*manager
, DdNode
**vars
, int numVars
, double n
, int index
);
97 static double bddAnnotateMintermCount (DdManager
*manager
, DdNode
*node
, double max
, st_table
*table
);
99 /**AutomaticEnd***************************************************************/
102 /*---------------------------------------------------------------------------*/
103 /* Definition of exported functions */
104 /*---------------------------------------------------------------------------*/
107 /**Function********************************************************************
109 Synopsis [Returns m minterms from a BDD.]
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.]
122 ******************************************************************************/
138 size
= manager
->size
;
139 one
= DD_ONE(manager
);
140 zero
= Cudd_Not(one
);
150 max
= pow(2.0,(double)n
);
155 manager
->reordered
= 0;
156 /* varSeen is used to mark the variables that are encountered
157 ** while traversing the BDD S.
159 varSeen
= ALLOC(int, size
);
160 if (varSeen
== NULL
) {
161 manager
->errorCode
= CUDD_MEMORY_OUT
;
164 for (i
= 0; i
< size
; i
++) {
167 for (i
= 0; i
< n
; i
++) {
168 index
= (xVars
[i
])->index
;
169 varSeen
[manager
->invperm
[index
]] = 0;
177 result
= selectMintermsFromUniverse(manager
,varSeen
,m
);
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");
187 manager
->errorCode
= CUDD_MEMORY_OUT
;
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.
194 num
= bddAnnotateMintermCount(manager
,S
,max
,mtable
);
196 st_foreach(mtable
,cuddStCountfree
,NIL(char));
197 st_free_table(mtable
);
202 result
= cuddSplitSetRecur(manager
,mtable
,varSeen
,S
,m
,max
,0);
205 st_foreach(mtable
,cuddStCountfree
,NULL
);
206 st_free_table(mtable
);
209 } while (manager
->reordered
== 1);
214 } /* end of Cudd_SplitSet */
217 /*---------------------------------------------------------------------------*/
218 /* Definition of internal functions */
219 /*---------------------------------------------------------------------------*/
221 /**Function********************************************************************
223 Synopsis [Implements the recursive step of Cudd_SplitSet.]
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.]
236 SideEffects [The array 'varSeen' is updated at every recursive call
237 to set the variables traversed by the procedure.]
241 ******************************************************************************/
252 DdNode
*one
, *zero
, *N
, *Nv
;
253 DdNode
*Nnv
, *q
, *r
, *v
;
255 double *dummy
, numT
, numE
;
256 int variable
, positive
;
259 one
= DD_ONE(manager
);
260 zero
= Cudd_Not(one
);
262 /* If p is constant, extract n minterms from constant 1. The procedure by
263 ** construction guarantees that minterms will not be extracted from
266 if (Cudd_IsConstant(p
)) {
267 q
= selectMintermsFromUniverse(manager
,varSeen
,n
);
273 /* Set variable as seen. */
275 varSeen
[manager
->invperm
[variable
]] = -1;
279 if (Cudd_IsComplement(p
)) {
284 /* If both the children of 'p' are constants, extract n minterms from a
287 if (Cudd_IsConstant(Nv
) && Cudd_IsConstant(Nnv
)) {
288 q
= selectMintermsFromUniverse(manager
,varSeen
,n
);
293 r
= cuddBddAndRecur(manager
,p
,q
);
295 Cudd_RecursiveDeref(manager
,q
);
299 Cudd_RecursiveDeref(manager
,q
);
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
));
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
));
323 v
= cuddUniqueInter(manager
,variable
,one
,zero
);
326 /* If perfect match. */
328 q
= cuddBddAndRecur(manager
,v
,Nv
);
330 Cudd_RecursiveDeref(manager
,v
);
334 Cudd_RecursiveDeref(manager
,v
);
339 q
= cuddBddAndRecur(manager
,Cudd_Not(v
),Nnv
);
341 Cudd_RecursiveDeref(manager
,v
);
345 Cudd_RecursiveDeref(manager
,v
);
349 /* If n is greater than numT, extract the difference from the ELSE child
350 ** and retain the function represented by the THEN branch.
353 q
= cuddSplitSetRecur(manager
,mtable
,varSeen
,
354 Nnv
,(n
-numT
),max
,index
+1);
356 Cudd_RecursiveDeref(manager
,v
);
360 r
= cuddBddIteRecur(manager
,v
,Nv
,q
);
362 Cudd_RecursiveDeref(manager
,q
);
363 Cudd_RecursiveDeref(manager
,v
);
367 Cudd_RecursiveDeref(manager
,q
);
368 Cudd_RecursiveDeref(manager
,v
);
372 /* If n is greater than numE, extract the difference from the THEN child
373 ** and retain the function represented by the ELSE branch.
376 q
= cuddSplitSetRecur(manager
,mtable
,varSeen
,
377 Nv
, (n
-numE
),max
,index
+1);
379 Cudd_RecursiveDeref(manager
,v
);
383 r
= cuddBddIteRecur(manager
,v
,q
,Nnv
);
385 Cudd_RecursiveDeref(manager
,q
);
386 Cudd_RecursiveDeref(manager
,v
);
390 Cudd_RecursiveDeref(manager
,q
);
391 Cudd_RecursiveDeref(manager
,v
);
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.
400 if (Cudd_IsConstant(Nv
) && !Cudd_IsConstant(Nnv
)) {
401 q
= selectMintermsFromUniverse(manager
,varSeen
,n
);
403 Cudd_RecursiveDeref(manager
,v
);
407 result
= cuddBddAndRecur(manager
,v
,q
);
408 if (result
== NULL
) {
409 Cudd_RecursiveDeref(manager
,q
);
410 Cudd_RecursiveDeref(manager
,v
);
414 Cudd_RecursiveDeref(manager
,q
);
415 Cudd_RecursiveDeref(manager
,v
);
418 } else if (!Cudd_IsConstant(Nv
) && Cudd_IsConstant(Nnv
)) {
419 q
= selectMintermsFromUniverse(manager
,varSeen
,n
);
421 Cudd_RecursiveDeref(manager
,v
);
425 result
= cuddBddAndRecur(manager
,Cudd_Not(v
),q
);
426 if (result
== NULL
) {
427 Cudd_RecursiveDeref(manager
,q
);
428 Cudd_RecursiveDeref(manager
,v
);
432 Cudd_RecursiveDeref(manager
,q
);
433 Cudd_RecursiveDeref(manager
,v
);
438 /* Both Nv and Nnv are not constants. So choose the one which
439 ** has fewer minterms in its onset.
443 q
= cuddSplitSetRecur(manager
,mtable
,varSeen
,
447 q
= cuddSplitSetRecur(manager
,mtable
,varSeen
,
452 Cudd_RecursiveDeref(manager
,v
);
458 result
= cuddBddAndRecur(manager
,v
,q
);
460 result
= cuddBddAndRecur(manager
,Cudd_Not(v
),q
);
462 if (result
== NULL
) {
463 Cudd_RecursiveDeref(manager
,q
);
464 Cudd_RecursiveDeref(manager
,v
);
468 Cudd_RecursiveDeref(manager
,q
);
469 Cudd_RecursiveDeref(manager
,v
);
474 } /* end of cuddSplitSetRecur */
477 /*---------------------------------------------------------------------------*/
478 /* Definition of static functions */
479 /*---------------------------------------------------------------------------*/
481 /**Function********************************************************************
483 Synopsis [This function prepares an array of variables which have not been
484 encountered so far when traversing the procedure cuddSplitSetRecur.]
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).]
493 ******************************************************************************/
495 selectMintermsFromUniverse(
502 DdNode
*one
, *zero
, *result
;
506 size
= manager
->size
;
507 one
= DD_ONE(manager
);
508 zero
= Cudd_Not(one
);
510 /* Count the number of variables not encountered so far in procedure
511 ** cuddSplitSetRecur.
513 for (i
= size
-1; i
>= 0; i
--) {
517 vars
= ALLOC(DdNode
*, numVars
);
519 manager
->errorCode
= CUDD_MEMORY_OUT
;
524 for (i
= size
-1; i
>= 0; i
--) {
525 if(varSeen
[i
] == 0) {
526 vars
[j
] = cuddUniqueInter(manager
,manager
->perm
[i
],one
,zero
);
532 /* Compute a function which has n minterms and depends on at most
533 ** numVars variables.
535 result
= mintermsFromUniverse(manager
,vars
,numVars
,n
, 0);
539 for (i
= 0; i
< numVars
; i
++)
540 Cudd_RecursiveDeref(manager
,vars
[i
]);
545 } /* end of selectMintermsFromUniverse */
548 /**Function********************************************************************
550 Synopsis [Recursive procedure to extract n mintems from constant 1.]
552 Description [Recursive procedure to extract n mintems from constant 1.]
556 ******************************************************************************/
558 mintermsFromUniverse(
570 one
= DD_ONE(manager
);
571 zero
= Cudd_Not(one
);
573 max
= pow(2.0, (double)numVars
);
580 /* if n == 2^(numVars-1), return a single variable */
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.
588 q
= mintermsFromUniverse(manager
,vars
,numVars
-1,(n
-max2
),index
+1);
592 result
= cuddBddIteRecur(manager
,vars
[index
],one
,q
);
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.
598 q
= mintermsFromUniverse(manager
,vars
,numVars
-1,n
,index
+1);
602 result
= cuddBddAndRecur(manager
,vars
[index
],q
);
605 if (result
== NULL
) {
606 Cudd_RecursiveDeref(manager
,q
);
610 Cudd_RecursiveDeref(manager
,q
);
614 } /* end of mintermsFromUniverse */
617 /**Function********************************************************************
619 Synopsis [Annotates every node in the BDD node with its minterm count.]
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.]
625 SideEffects [Fills up 'table' with the pair <node,minterm_count>.]
627 ******************************************************************************/
629 bddAnnotateMintermCount(
637 register double min_v
,min_nv
;
638 register double min_N
;
643 N
= Cudd_Regular(node
);
644 if (cuddIsConstant(N
)) {
645 if (node
== DD_ONE(manager
)) {
652 if (st_lookup(table
, node
, &dummy
)) {
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
;
672 pmin
= ALLOC(double,1);
674 manager
->errorCode
= CUDD_MEMORY_OUT
;
675 return((double)CUDD_OUT_OF_MEM
);
679 if (st_insert(table
,(char *)node
, (char *)pmin
) == ST_OUT_OF_MEM
) {
681 return((double)CUDD_OUT_OF_MEM
);
686 } /* end of bddAnnotateMintermCount */