1 /**CFile***********************************************************************
3 FileName [cuddDecomp.c]
7 Synopsis [Functions for BDD decomposition.]
9 Description [External procedures included in this file:
11 <li> Cudd_bddApproxConjDecomp()
12 <li> Cudd_bddApproxDisjDecomp()
13 <li> Cudd_bddIterConjDecomp()
14 <li> Cudd_bddIterDisjDecomp()
15 <li> Cudd_bddGenConjDecomp()
16 <li> Cudd_bddGenDisjDecomp()
17 <li> Cudd_bddVarConjDecomp()
18 <li> Cudd_bddVarDisjDecomp()
20 Static procedures included in this module:
22 <li> cuddConjunctsAux()
28 Author [Kavita Ravi, Fabio Somenzi]
30 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
34 Redistribution and use in source and binary forms, with or without
35 modification, are permitted provided that the following conditions
38 Redistributions of source code must retain the above copyright
39 notice, this list of conditions and the following disclaimer.
41 Redistributions in binary form must reproduce the above copyright
42 notice, this list of conditions and the following disclaimer in the
43 documentation and/or other materials provided with the distribution.
45 Neither the name of the University of Colorado nor the names of its
46 contributors may be used to endorse or promote products derived from
47 this software without specific prior written permission.
49 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
50 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
51 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
52 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
53 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
54 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
55 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
56 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
57 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
58 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
59 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
60 POSSIBILITY OF SUCH DAMAGE.]
62 ******************************************************************************/
67 /*---------------------------------------------------------------------------*/
68 /* Constant declarations */
69 /*---------------------------------------------------------------------------*/
82 /*---------------------------------------------------------------------------*/
83 /* Stucture declarations */
84 /*---------------------------------------------------------------------------*/
86 /*---------------------------------------------------------------------------*/
87 /* Type declarations */
88 /*---------------------------------------------------------------------------*/
89 typedef struct Conjuncts
{
94 typedef struct NodeStat
{
100 /*---------------------------------------------------------------------------*/
101 /* Variable declarations */
102 /*---------------------------------------------------------------------------*/
105 static char rcsid
[] DD_UNUSED
= "$Id: cuddDecomp.c,v 1.44 2004/08/13 18:04:47 fabio Exp $";
108 static DdNode
*one
, *zero
;
111 /*---------------------------------------------------------------------------*/
112 /* Macro declarations */
113 /*---------------------------------------------------------------------------*/
116 #define FactorsNotStored(factors) ((int)((long)(factors) & 01))
118 #define FactorsComplement(factors) ((Conjuncts *)((long)(factors) | 01))
120 #define FactorsUncomplement(factors) ((Conjuncts *)((long)(factors) ^ 01))
122 /**AutomaticStart*************************************************************/
124 /*---------------------------------------------------------------------------*/
125 /* Static function prototypes */
126 /*---------------------------------------------------------------------------*/
128 static NodeStat
* CreateBotDist (DdNode
* node
, st_table
* distanceTable
);
129 static double CountMinterms (DdNode
* node
, double max
, st_table
* mintermTable
, FILE *fp
);
130 static void ConjunctsFree (DdManager
* dd
, Conjuncts
* factors
);
131 static int PairInTables (DdNode
* g
, DdNode
* h
, st_table
* ghTable
);
132 static Conjuncts
* CheckTablesCacheAndReturn (DdNode
* node
, DdNode
* g
, DdNode
* h
, st_table
* ghTable
, st_table
* cacheTable
);
133 static Conjuncts
* PickOnePair (DdNode
* node
, DdNode
* g1
, DdNode
* h1
, DdNode
* g2
, DdNode
* h2
, st_table
* ghTable
, st_table
* cacheTable
);
134 static Conjuncts
* CheckInTables (DdNode
* node
, DdNode
* g1
, DdNode
* h1
, DdNode
* g2
, DdNode
* h2
, st_table
* ghTable
, st_table
* cacheTable
, int * outOfMem
);
135 static Conjuncts
* ZeroCase (DdManager
* dd
, DdNode
* node
, Conjuncts
* factorsNv
, st_table
* ghTable
, st_table
* cacheTable
, int switched
);
136 static Conjuncts
* BuildConjuncts (DdManager
* dd
, DdNode
* node
, st_table
* distanceTable
, st_table
* cacheTable
, int approxDistance
, int maxLocalRef
, st_table
* ghTable
, st_table
* mintermTable
);
137 static int cuddConjunctsAux (DdManager
* dd
, DdNode
* f
, DdNode
** c1
, DdNode
** c2
);
139 /**AutomaticEnd***************************************************************/
142 /*---------------------------------------------------------------------------*/
143 /* Definition of exported functions */
144 /*---------------------------------------------------------------------------*/
147 /**Function********************************************************************
149 Synopsis [Performs two-way conjunctive decomposition of a BDD.]
151 Description [Performs two-way conjunctive decomposition of a
152 BDD. This procedure owes its name to the use of supersetting to
153 obtain an initial factor of the given function. Returns the number
154 of conjuncts produced, that is, 2 if successful; 1 if no meaningful
155 decomposition was found; 0 otherwise. The conjuncts produced by this
156 procedure tend to be imbalanced.]
158 SideEffects [The factors are returned in an array as side effects.
159 The array is allocated by this function. It is the caller's responsibility
160 to free it. On successful completion, the conjuncts are already
161 referenced. If the function returns 0, the array for the conjuncts is
162 not allocated. If the function returns 1, the only factor equals the
163 function to be decomposed.]
165 SeeAlso [Cudd_bddApproxDisjDecomp Cudd_bddIterConjDecomp
166 Cudd_bddGenConjDecomp Cudd_bddVarConjDecomp Cudd_RemapOverApprox
167 Cudd_bddSqueeze Cudd_bddLICompaction]
169 ******************************************************************************/
171 Cudd_bddApproxConjDecomp(
172 DdManager
* dd
/* manager */,
173 DdNode
* f
/* function to be decomposed */,
174 DdNode
*** conjuncts
/* address of the first factor */)
176 DdNode
*superset1
, *superset2
, *glocal
, *hlocal
;
177 int nvars
= Cudd_SupportSize(dd
,f
);
179 /* Find a tentative first factor by overapproximation and minimization. */
180 superset1
= Cudd_RemapOverApprox(dd
,f
,nvars
,0,1.0);
181 if (superset1
== NULL
) return(0);
183 superset2
= Cudd_bddSqueeze(dd
,f
,superset1
);
184 if (superset2
== NULL
) {
185 Cudd_RecursiveDeref(dd
,superset1
);
189 Cudd_RecursiveDeref(dd
,superset1
);
191 /* Compute the second factor by minimization. */
192 hlocal
= Cudd_bddLICompaction(dd
,f
,superset2
);
193 if (hlocal
== NULL
) {
194 Cudd_RecursiveDeref(dd
,superset2
);
199 /* Refine the first factor by minimization. If h turns out to be f, this
200 ** step guarantees that g will be 1. */
201 glocal
= Cudd_bddLICompaction(dd
,superset2
,hlocal
);
202 if (glocal
== NULL
) {
203 Cudd_RecursiveDeref(dd
,superset2
);
204 Cudd_RecursiveDeref(dd
,hlocal
);
208 Cudd_RecursiveDeref(dd
,superset2
);
210 if (glocal
!= DD_ONE(dd
)) {
211 if (hlocal
!= DD_ONE(dd
)) {
212 *conjuncts
= ALLOC(DdNode
*,2);
213 if (*conjuncts
== NULL
) {
214 Cudd_RecursiveDeref(dd
,glocal
);
215 Cudd_RecursiveDeref(dd
,hlocal
);
216 dd
->errorCode
= CUDD_MEMORY_OUT
;
219 (*conjuncts
)[0] = glocal
;
220 (*conjuncts
)[1] = hlocal
;
223 Cudd_RecursiveDeref(dd
,hlocal
);
224 *conjuncts
= ALLOC(DdNode
*,1);
225 if (*conjuncts
== NULL
) {
226 Cudd_RecursiveDeref(dd
,glocal
);
227 dd
->errorCode
= CUDD_MEMORY_OUT
;
230 (*conjuncts
)[0] = glocal
;
234 Cudd_RecursiveDeref(dd
,glocal
);
235 *conjuncts
= ALLOC(DdNode
*,1);
236 if (*conjuncts
== NULL
) {
237 Cudd_RecursiveDeref(dd
,hlocal
);
238 dd
->errorCode
= CUDD_MEMORY_OUT
;
241 (*conjuncts
)[0] = hlocal
;
245 } /* end of Cudd_bddApproxConjDecomp */
248 /**Function********************************************************************
250 Synopsis [Performs two-way disjunctive decomposition of a BDD.]
252 Description [Performs two-way disjunctive decomposition of a BDD.
253 Returns the number of disjuncts produced, that is, 2 if successful;
254 1 if no meaningful decomposition was found; 0 otherwise. The
255 disjuncts produced by this procedure tend to be imbalanced.]
257 SideEffects [The two disjuncts are returned in an array as side effects.
258 The array is allocated by this function. It is the caller's responsibility
259 to free it. On successful completion, the disjuncts are already
260 referenced. If the function returns 0, the array for the disjuncts is
261 not allocated. If the function returns 1, the only factor equals the
262 function to be decomposed.]
264 SeeAlso [Cudd_bddApproxConjDecomp Cudd_bddIterDisjDecomp
265 Cudd_bddGenDisjDecomp Cudd_bddVarDisjDecomp]
267 ******************************************************************************/
269 Cudd_bddApproxDisjDecomp(
270 DdManager
* dd
/* manager */,
271 DdNode
* f
/* function to be decomposed */,
272 DdNode
*** disjuncts
/* address of the array of the disjuncts */)
276 result
= Cudd_bddApproxConjDecomp(dd
,Cudd_Not(f
),disjuncts
);
277 for (i
= 0; i
< result
; i
++) {
278 (*disjuncts
)[i
] = Cudd_Not((*disjuncts
)[i
]);
282 } /* end of Cudd_bddApproxDisjDecomp */
285 /**Function********************************************************************
287 Synopsis [Performs two-way conjunctive decomposition of a BDD.]
289 Description [Performs two-way conjunctive decomposition of a
290 BDD. This procedure owes its name to the iterated use of
291 supersetting to obtain a factor of the given function. Returns the
292 number of conjuncts produced, that is, 2 if successful; 1 if no
293 meaningful decomposition was found; 0 otherwise. The conjuncts
294 produced by this procedure tend to be imbalanced.]
296 SideEffects [The factors are returned in an array as side effects.
297 The array is allocated by this function. It is the caller's responsibility
298 to free it. On successful completion, the conjuncts are already
299 referenced. If the function returns 0, the array for the conjuncts is
300 not allocated. If the function returns 1, the only factor equals the
301 function to be decomposed.]
303 SeeAlso [Cudd_bddIterDisjDecomp Cudd_bddApproxConjDecomp
304 Cudd_bddGenConjDecomp Cudd_bddVarConjDecomp Cudd_RemapOverApprox
305 Cudd_bddSqueeze Cudd_bddLICompaction]
307 ******************************************************************************/
309 Cudd_bddIterConjDecomp(
310 DdManager
* dd
/* manager */,
311 DdNode
* f
/* function to be decomposed */,
312 DdNode
*** conjuncts
/* address of the array of conjuncts */)
314 DdNode
*superset1
, *superset2
, *old
[2], *res
[2];
315 int sizeOld
, sizeNew
;
316 int nvars
= Cudd_SupportSize(dd
,f
);
322 sizeOld
= Cudd_SharingSize(old
,2);
325 /* Find a tentative first factor by overapproximation and
327 superset1
= Cudd_RemapOverApprox(dd
,old
[1],nvars
,0,1.0);
328 if (superset1
== NULL
) {
329 Cudd_RecursiveDeref(dd
,old
[0]);
330 Cudd_RecursiveDeref(dd
,old
[1]);
334 superset2
= Cudd_bddSqueeze(dd
,old
[1],superset1
);
335 if (superset2
== NULL
) {
336 Cudd_RecursiveDeref(dd
,old
[0]);
337 Cudd_RecursiveDeref(dd
,old
[1]);
338 Cudd_RecursiveDeref(dd
,superset1
);
342 Cudd_RecursiveDeref(dd
,superset1
);
343 res
[0] = Cudd_bddAnd(dd
,old
[0],superset2
);
344 if (res
[0] == NULL
) {
345 Cudd_RecursiveDeref(dd
,superset2
);
346 Cudd_RecursiveDeref(dd
,old
[0]);
347 Cudd_RecursiveDeref(dd
,old
[1]);
351 Cudd_RecursiveDeref(dd
,superset2
);
352 if (res
[0] == old
[0]) {
353 Cudd_RecursiveDeref(dd
,res
[0]);
354 break; /* avoid infinite loop */
357 /* Compute the second factor by minimization. */
358 res
[1] = Cudd_bddLICompaction(dd
,old
[1],res
[0]);
359 if (res
[1] == NULL
) {
360 Cudd_RecursiveDeref(dd
,old
[0]);
361 Cudd_RecursiveDeref(dd
,old
[1]);
366 sizeNew
= Cudd_SharingSize(res
,2);
367 if (sizeNew
<= sizeOld
) {
368 Cudd_RecursiveDeref(dd
,old
[0]);
370 Cudd_RecursiveDeref(dd
,old
[1]);
374 Cudd_RecursiveDeref(dd
,res
[0]);
375 Cudd_RecursiveDeref(dd
,res
[1]);
381 /* Refine the first factor by minimization. If h turns out to
382 ** be f, this step guarantees that g will be 1. */
383 superset1
= Cudd_bddLICompaction(dd
,old
[0],old
[1]);
384 if (superset1
== NULL
) {
385 Cudd_RecursiveDeref(dd
,old
[0]);
386 Cudd_RecursiveDeref(dd
,old
[1]);
390 Cudd_RecursiveDeref(dd
,old
[0]);
393 if (old
[0] != DD_ONE(dd
)) {
394 if (old
[1] != DD_ONE(dd
)) {
395 *conjuncts
= ALLOC(DdNode
*,2);
396 if (*conjuncts
== NULL
) {
397 Cudd_RecursiveDeref(dd
,old
[0]);
398 Cudd_RecursiveDeref(dd
,old
[1]);
399 dd
->errorCode
= CUDD_MEMORY_OUT
;
402 (*conjuncts
)[0] = old
[0];
403 (*conjuncts
)[1] = old
[1];
406 Cudd_RecursiveDeref(dd
,old
[1]);
407 *conjuncts
= ALLOC(DdNode
*,1);
408 if (*conjuncts
== NULL
) {
409 Cudd_RecursiveDeref(dd
,old
[0]);
410 dd
->errorCode
= CUDD_MEMORY_OUT
;
413 (*conjuncts
)[0] = old
[0];
417 Cudd_RecursiveDeref(dd
,old
[0]);
418 *conjuncts
= ALLOC(DdNode
*,1);
419 if (*conjuncts
== NULL
) {
420 Cudd_RecursiveDeref(dd
,old
[1]);
421 dd
->errorCode
= CUDD_MEMORY_OUT
;
424 (*conjuncts
)[0] = old
[1];
428 } /* end of Cudd_bddIterConjDecomp */
431 /**Function********************************************************************
433 Synopsis [Performs two-way disjunctive decomposition of a BDD.]
435 Description [Performs two-way disjunctive decomposition of a BDD.
436 Returns the number of disjuncts produced, that is, 2 if successful;
437 1 if no meaningful decomposition was found; 0 otherwise. The
438 disjuncts produced by this procedure tend to be imbalanced.]
440 SideEffects [The two disjuncts are returned in an array as side effects.
441 The array is allocated by this function. It is the caller's responsibility
442 to free it. On successful completion, the disjuncts are already
443 referenced. If the function returns 0, the array for the disjuncts is
444 not allocated. If the function returns 1, the only factor equals the
445 function to be decomposed.]
447 SeeAlso [Cudd_bddIterConjDecomp Cudd_bddApproxDisjDecomp
448 Cudd_bddGenDisjDecomp Cudd_bddVarDisjDecomp]
450 ******************************************************************************/
452 Cudd_bddIterDisjDecomp(
453 DdManager
* dd
/* manager */,
454 DdNode
* f
/* function to be decomposed */,
455 DdNode
*** disjuncts
/* address of the array of the disjuncts */)
459 result
= Cudd_bddIterConjDecomp(dd
,Cudd_Not(f
),disjuncts
);
460 for (i
= 0; i
< result
; i
++) {
461 (*disjuncts
)[i
] = Cudd_Not((*disjuncts
)[i
]);
465 } /* end of Cudd_bddIterDisjDecomp */
468 /**Function********************************************************************
470 Synopsis [Performs two-way conjunctive decomposition of a BDD.]
472 Description [Performs two-way conjunctive decomposition of a
473 BDD. This procedure owes its name to the fact tht it generalizes the
474 decomposition based on the cofactors with respect to one
475 variable. Returns the number of conjuncts produced, that is, 2 if
476 successful; 1 if no meaningful decomposition was found; 0
477 otherwise. The conjuncts produced by this procedure tend to be
480 SideEffects [The two factors are returned in an array as side effects.
481 The array is allocated by this function. It is the caller's responsibility
482 to free it. On successful completion, the conjuncts are already
483 referenced. If the function returns 0, the array for the conjuncts is
484 not allocated. If the function returns 1, the only factor equals the
485 function to be decomposed.]
487 SeeAlso [Cudd_bddGenDisjDecomp Cudd_bddApproxConjDecomp
488 Cudd_bddIterConjDecomp Cudd_bddVarConjDecomp]
490 ******************************************************************************/
492 Cudd_bddGenConjDecomp(
493 DdManager
* dd
/* manager */,
494 DdNode
* f
/* function to be decomposed */,
495 DdNode
*** conjuncts
/* address of the array of conjuncts */)
498 DdNode
*glocal
, *hlocal
;
501 zero
= Cudd_Not(one
);
505 result
= cuddConjunctsAux(dd
, f
, &glocal
, &hlocal
);
506 } while (dd
->reordered
== 1);
514 *conjuncts
= ALLOC(DdNode
*,2);
515 if (*conjuncts
== NULL
) {
516 Cudd_RecursiveDeref(dd
,glocal
);
517 Cudd_RecursiveDeref(dd
,hlocal
);
518 dd
->errorCode
= CUDD_MEMORY_OUT
;
521 (*conjuncts
)[0] = glocal
;
522 (*conjuncts
)[1] = hlocal
;
525 Cudd_RecursiveDeref(dd
,hlocal
);
526 *conjuncts
= ALLOC(DdNode
*,1);
527 if (*conjuncts
== NULL
) {
528 Cudd_RecursiveDeref(dd
,glocal
);
529 dd
->errorCode
= CUDD_MEMORY_OUT
;
532 (*conjuncts
)[0] = glocal
;
536 Cudd_RecursiveDeref(dd
,glocal
);
537 *conjuncts
= ALLOC(DdNode
*,1);
538 if (*conjuncts
== NULL
) {
539 Cudd_RecursiveDeref(dd
,hlocal
);
540 dd
->errorCode
= CUDD_MEMORY_OUT
;
543 (*conjuncts
)[0] = hlocal
;
547 } /* end of Cudd_bddGenConjDecomp */
550 /**Function********************************************************************
552 Synopsis [Performs two-way disjunctive decomposition of a BDD.]
554 Description [Performs two-way disjunctive decomposition of a BDD.
555 Returns the number of disjuncts produced, that is, 2 if successful;
556 1 if no meaningful decomposition was found; 0 otherwise. The
557 disjuncts produced by this procedure tend to be balanced.]
559 SideEffects [The two disjuncts are returned in an array as side effects.
560 The array is allocated by this function. It is the caller's responsibility
561 to free it. On successful completion, the disjuncts are already
562 referenced. If the function returns 0, the array for the disjuncts is
563 not allocated. If the function returns 1, the only factor equals the
564 function to be decomposed.]
566 SeeAlso [Cudd_bddGenConjDecomp Cudd_bddApproxDisjDecomp
567 Cudd_bddIterDisjDecomp Cudd_bddVarDisjDecomp]
569 ******************************************************************************/
571 Cudd_bddGenDisjDecomp(
572 DdManager
* dd
/* manager */,
573 DdNode
* f
/* function to be decomposed */,
574 DdNode
*** disjuncts
/* address of the array of the disjuncts */)
578 result
= Cudd_bddGenConjDecomp(dd
,Cudd_Not(f
),disjuncts
);
579 for (i
= 0; i
< result
; i
++) {
580 (*disjuncts
)[i
] = Cudd_Not((*disjuncts
)[i
]);
584 } /* end of Cudd_bddGenDisjDecomp */
587 /**Function********************************************************************
589 Synopsis [Performs two-way conjunctive decomposition of a BDD.]
591 Description [Conjunctively decomposes one BDD according to a
592 variable. If <code>f</code> is the function of the BDD and
593 <code>x</code> is the variable, the decomposition is
594 <code>(f+x)(f+x')</code>. The variable is chosen so as to balance
595 the sizes of the two conjuncts and to keep them small. Returns the
596 number of conjuncts produced, that is, 2 if successful; 1 if no
597 meaningful decomposition was found; 0 otherwise.]
599 SideEffects [The two factors are returned in an array as side effects.
600 The array is allocated by this function. It is the caller's responsibility
601 to free it. On successful completion, the conjuncts are already
602 referenced. If the function returns 0, the array for the conjuncts is
603 not allocated. If the function returns 1, the only factor equals the
604 function to be decomposed.]
606 SeeAlso [Cudd_bddVarDisjDecomp Cudd_bddGenConjDecomp
607 Cudd_bddApproxConjDecomp Cudd_bddIterConjDecomp]
609 *****************************************************************************/
611 Cudd_bddVarConjDecomp(
612 DdManager
* dd
/* manager */,
613 DdNode
* f
/* function to be decomposed */,
614 DdNode
*** conjuncts
/* address of the array of conjuncts */)
618 DdNode
*support
, *scan
, *var
, *glocal
, *hlocal
;
620 /* Find best cofactoring variable. */
621 support
= Cudd_Support(dd
,f
);
622 if (support
== NULL
) return(0);
623 if (Cudd_IsConstant(support
)) {
624 *conjuncts
= ALLOC(DdNode
*,1);
625 if (*conjuncts
== NULL
) {
626 dd
->errorCode
= CUDD_MEMORY_OUT
;
630 cuddRef((*conjuncts
)[0]);
637 while (!Cudd_IsConstant(scan
)) {
639 int est1
= Cudd_EstimateCofactor(dd
,f
,i
,1);
640 int est0
= Cudd_EstimateCofactor(dd
,f
,i
,0);
641 /* Minimize the size of the larger of the two cofactors. */
642 int est
= (est1
> est0
) ? est1
: est0
;
650 assert(best
>= 0 && best
< dd
->size
);
652 Cudd_RecursiveDeref(dd
,support
);
654 var
= Cudd_bddIthVar(dd
,best
);
655 glocal
= Cudd_bddOr(dd
,f
,var
);
656 if (glocal
== NULL
) {
660 hlocal
= Cudd_bddOr(dd
,f
,Cudd_Not(var
));
661 if (hlocal
== NULL
) {
662 Cudd_RecursiveDeref(dd
,glocal
);
667 if (glocal
!= DD_ONE(dd
)) {
668 if (hlocal
!= DD_ONE(dd
)) {
669 *conjuncts
= ALLOC(DdNode
*,2);
670 if (*conjuncts
== NULL
) {
671 Cudd_RecursiveDeref(dd
,glocal
);
672 Cudd_RecursiveDeref(dd
,hlocal
);
673 dd
->errorCode
= CUDD_MEMORY_OUT
;
676 (*conjuncts
)[0] = glocal
;
677 (*conjuncts
)[1] = hlocal
;
680 Cudd_RecursiveDeref(dd
,hlocal
);
681 *conjuncts
= ALLOC(DdNode
*,1);
682 if (*conjuncts
== NULL
) {
683 Cudd_RecursiveDeref(dd
,glocal
);
684 dd
->errorCode
= CUDD_MEMORY_OUT
;
687 (*conjuncts
)[0] = glocal
;
691 Cudd_RecursiveDeref(dd
,glocal
);
692 *conjuncts
= ALLOC(DdNode
*,1);
693 if (*conjuncts
== NULL
) {
694 Cudd_RecursiveDeref(dd
,hlocal
);
695 dd
->errorCode
= CUDD_MEMORY_OUT
;
698 (*conjuncts
)[0] = hlocal
;
702 } /* end of Cudd_bddVarConjDecomp */
705 /**Function********************************************************************
707 Synopsis [Performs two-way disjunctive decomposition of a BDD.]
709 Description [Performs two-way disjunctive decomposition of a BDD
710 according to a variable. If <code>f</code> is the function of the
711 BDD and <code>x</code> is the variable, the decomposition is
712 <code>f*x + f*x'</code>. The variable is chosen so as to balance
713 the sizes of the two disjuncts and to keep them small. Returns the
714 number of disjuncts produced, that is, 2 if successful; 1 if no
715 meaningful decomposition was found; 0 otherwise.]
717 SideEffects [The two disjuncts are returned in an array as side effects.
718 The array is allocated by this function. It is the caller's responsibility
719 to free it. On successful completion, the disjuncts are already
720 referenced. If the function returns 0, the array for the disjuncts is
721 not allocated. If the function returns 1, the only factor equals the
722 function to be decomposed.]
724 SeeAlso [Cudd_bddVarConjDecomp Cudd_bddApproxDisjDecomp
725 Cudd_bddIterDisjDecomp Cudd_bddGenDisjDecomp]
727 ******************************************************************************/
729 Cudd_bddVarDisjDecomp(
730 DdManager
* dd
/* manager */,
731 DdNode
* f
/* function to be decomposed */,
732 DdNode
*** disjuncts
/* address of the array of the disjuncts */)
736 result
= Cudd_bddVarConjDecomp(dd
,Cudd_Not(f
),disjuncts
);
737 for (i
= 0; i
< result
; i
++) {
738 (*disjuncts
)[i
] = Cudd_Not((*disjuncts
)[i
]);
742 } /* end of Cudd_bddVarDisjDecomp */
745 /*---------------------------------------------------------------------------*/
746 /* Definition of internal functions */
747 /*---------------------------------------------------------------------------*/
749 /*---------------------------------------------------------------------------*/
750 /* Definition of static functions */
751 /*---------------------------------------------------------------------------*/
754 /**Function********************************************************************
756 Synopsis [Get longest distance of node from constant.]
758 Description [Get longest distance of node from constant. Returns the
759 distance of the root from the constant if successful; CUDD_OUT_OF_MEM
766 ******************************************************************************/
770 st_table
* distanceTable
)
772 DdNode
*N
, *Nv
, *Nnv
;
773 int distance
, distanceNv
, distanceNnv
;
774 NodeStat
*nodeStat
, *nodeStatNv
, *nodeStatNnv
;
777 if (Cudd_IsConstant(node
)) {
782 /* Return the entry in the table if found. */
783 N
= Cudd_Regular(node
);
784 if (st_lookup(distanceTable
, N
, &nodeStat
)) {
785 nodeStat
->localRef
++;
791 Nv
= Cudd_NotCond(Nv
, Cudd_IsComplement(node
));
792 Nnv
= Cudd_NotCond(Nnv
, Cudd_IsComplement(node
));
794 /* Recur on the children. */
795 nodeStatNv
= CreateBotDist(Nv
, distanceTable
);
796 if (nodeStatNv
== NULL
) return(NULL
);
797 distanceNv
= nodeStatNv
->distance
;
799 nodeStatNnv
= CreateBotDist(Nnv
, distanceTable
);
800 if (nodeStatNnv
== NULL
) return(NULL
);
801 distanceNnv
= nodeStatNnv
->distance
;
802 /* Store max distance from constant; note sometimes this distance
805 distance
= (distanceNv
> distanceNnv
) ? (distanceNv
+1) : (distanceNnv
+ 1);
807 nodeStat
= ALLOC(NodeStat
, 1);
808 if (nodeStat
== NULL
) {
811 nodeStat
->distance
= distance
;
812 nodeStat
->localRef
= 1;
814 if (st_insert(distanceTable
, (char *)N
, (char *)nodeStat
) ==
821 } /* end of CreateBotDist */
824 /**Function********************************************************************
826 Synopsis [Count the number of minterms of each node ina a BDD and
827 store it in a hash table.]
835 ******************************************************************************/
840 st_table
* mintermTable
,
843 DdNode
*N
, *Nv
, *Nnv
;
844 double min
, minNv
, minNnv
;
847 N
= Cudd_Regular(node
);
849 if (cuddIsConstant(N
)) {
857 /* Return the entry in the table if found. */
858 if (st_lookup(mintermTable
, node
, &dummy
)) {
865 Nv
= Cudd_NotCond(Nv
, Cudd_IsComplement(node
));
866 Nnv
= Cudd_NotCond(Nnv
, Cudd_IsComplement(node
));
868 /* Recur on the children. */
869 minNv
= CountMinterms(Nv
, max
, mintermTable
, fp
);
870 if (minNv
== -1.0) return(-1.0);
871 minNnv
= CountMinterms(Nnv
, max
, mintermTable
, fp
);
872 if (minNnv
== -1.0) return(-1.0);
873 min
= minNv
/ 2.0 + minNnv
/ 2.0;
877 dummy
= ALLOC(double, 1);
878 if (dummy
== NULL
) return(-1.0);
880 if (st_insert(mintermTable
, (char *)node
, (char *)dummy
) == ST_OUT_OF_MEM
) {
881 (void) fprintf(fp
, "st table insert failed\n");
885 } /* end of CountMinterms */
888 /**Function********************************************************************
890 Synopsis [Free factors structure]
898 ******************************************************************************/
904 Cudd_RecursiveDeref(dd
, factors
->g
);
905 Cudd_RecursiveDeref(dd
, factors
->h
);
909 } /* end of ConjunctsFree */
912 /**Function********************************************************************
914 Synopsis [Check whether the given pair is in the tables.]
916 Description [.Check whether the given pair is in the tables. gTable
917 and hTable are combined.
918 absence in both is indicated by 0,
919 presence in gTable is indicated by 1,
920 presence in hTable by 2 and
921 presence in both by 3.
922 The values returned by this function are PAIR_ST,
923 PAIR_CR, G_ST, G_CR, H_ST, H_CR, BOTH_G, BOTH_H, NONE.
924 PAIR_ST implies g in gTable and h in hTable
925 PAIR_CR implies g in hTable and h in gTable
926 G_ST implies g in gTable and h not in any table
927 G_CR implies g in hTable and h not in any table
928 H_ST implies h in hTable and g not in any table
929 H_CR implies h in gTable and g not in any table
930 BOTH_G implies both in gTable
931 BOTH_H implies both in hTable
932 NONE implies none in table; ]
936 SeeAlso [CheckTablesCacheAndReturn CheckInTables]
938 ******************************************************************************/
945 int valueG
, valueH
, gPresent
, hPresent
;
947 valueG
= valueH
= gPresent
= hPresent
= 0;
949 gPresent
= st_lookup_int(ghTable
, (char *)Cudd_Regular(g
), &valueG
);
950 hPresent
= st_lookup_int(ghTable
, (char *)Cudd_Regular(h
), &valueH
);
952 if (!gPresent
&& !hPresent
) return(NONE
);
955 if (valueG
& 1) return(G_ST
);
956 if (valueG
& 2) return(G_CR
);
959 if (valueH
& 1) return(H_CR
);
960 if (valueH
& 2) return(H_ST
);
963 if ((valueG
& 1) && (valueH
& 2)) return(PAIR_ST
);
964 if ((valueG
& 2) && (valueH
& 1)) return(PAIR_CR
);
972 } /* end of PairInTables */
975 /**Function********************************************************************
977 Synopsis [Check the tables for the existence of pair and return one
978 combination, cache the result.]
980 Description [Check the tables for the existence of pair and return
981 one combination, cache the result. The assumption is that one of the
982 conjuncts is already in the tables.]
984 SideEffects [g and h referenced for the cache]
988 ******************************************************************************/
990 CheckTablesCacheAndReturn(
995 st_table
* cacheTable
)
1003 pairValue
= PairInTables(g
, h
, ghTable
);
1004 assert(pairValue
!= NONE
);
1005 /* if both dont exist in table, we know one exists(either g or h).
1006 * Therefore store the other and proceed
1008 factors
= ALLOC(Conjuncts
, 1);
1009 if (factors
== NULL
) return(NULL
);
1010 if ((pairValue
== BOTH_H
) || (pairValue
== H_ST
)) {
1013 if (st_lookup_int(ghTable
, (char *)Cudd_Regular(g
), &value
)) {
1018 if (st_insert(ghTable
, (char *)Cudd_Regular(g
),
1019 (char *)(long)value
) == ST_OUT_OF_MEM
) {
1025 } else if ((pairValue
== BOTH_G
) || (pairValue
== G_ST
)) {
1028 if (st_lookup_int(ghTable
, (char *)Cudd_Regular(h
), &value
)) {
1033 if (st_insert(ghTable
, (char *)Cudd_Regular(h
),
1034 (char *)(long)value
) == ST_OUT_OF_MEM
) {
1040 } else if (pairValue
== H_CR
) {
1043 if (st_insert(ghTable
, (char *)Cudd_Regular(g
),
1044 (char *)(long)value
) == ST_OUT_OF_MEM
) {
1050 } else if (pairValue
== G_CR
) {
1053 if (st_insert(ghTable
, (char *)Cudd_Regular(h
),
1054 (char *)(long)value
) == ST_OUT_OF_MEM
) {
1060 } else if (pairValue
== PAIR_CR
) {
1061 /* pair exists in table */
1064 } else if (pairValue
== PAIR_ST
) {
1069 /* cache the result for this node */
1070 if (st_insert(cacheTable
, (char *)node
, (char *)factors
) == ST_OUT_OF_MEM
) {
1077 } /* end of CheckTablesCacheAndReturn */
1079 /**Function********************************************************************
1081 Synopsis [Check the tables for the existence of pair and return one
1082 combination, store in cache.]
1084 Description [Check the tables for the existence of pair and return
1085 one combination, store in cache. The pair that has more pointers to
1086 it is picked. An approximation of the number of local pointers is
1087 made by taking the reference count of the pairs sent. ]
1091 SeeAlso [ZeroCase BuildConjuncts]
1093 ******************************************************************************/
1102 st_table
* cacheTable
)
1108 factors
= ALLOC(Conjuncts
, 1);
1109 if (factors
== NULL
) return(NULL
);
1111 /* count the number of pointers to pair 2 */
1113 twoRef
= (Cudd_Regular(g2
))->ref
;
1114 } else if (g2
== one
) {
1115 twoRef
= (Cudd_Regular(h2
))->ref
;
1117 twoRef
= ((Cudd_Regular(g2
))->ref
+ (Cudd_Regular(h2
))->ref
)/2;
1120 /* count the number of pointers to pair 1 */
1122 oneRef
= (Cudd_Regular(g1
))->ref
;
1123 } else if (g1
== one
) {
1124 oneRef
= (Cudd_Regular(h1
))->ref
;
1126 oneRef
= ((Cudd_Regular(g1
))->ref
+ (Cudd_Regular(h1
))->ref
)/2;
1129 /* pick the pair with higher reference count */
1130 if (oneRef
>= twoRef
) {
1139 * Store computed factors in respective tables to encourage
1142 if (factors
->g
!= one
) {
1143 /* insert g in htable */
1145 if (st_lookup_int(ghTable
, (char *)Cudd_Regular(factors
->g
), &value
)) {
1148 if (st_insert(ghTable
, (char *)Cudd_Regular(factors
->g
),
1149 (char *)(long)value
) == ST_OUT_OF_MEM
) {
1156 if (st_insert(ghTable
, (char *)Cudd_Regular(factors
->g
),
1157 (char *)(long)value
) == ST_OUT_OF_MEM
) {
1164 if (factors
->h
!= one
) {
1165 /* insert h in htable */
1167 if (st_lookup_int(ghTable
, (char *)Cudd_Regular(factors
->h
), &value
)) {
1170 if (st_insert(ghTable
, (char *)Cudd_Regular(factors
->h
),
1171 (char *)(long)value
) == ST_OUT_OF_MEM
) {
1178 if (st_insert(ghTable
, (char *)Cudd_Regular(factors
->h
),
1179 (char *)(long)value
) == ST_OUT_OF_MEM
) {
1186 /* Store factors in cache table for later use. */
1187 if (st_insert(cacheTable
, (char *)node
, (char *)factors
) ==
1195 } /* end of PickOnePair */
1198 /**Function********************************************************************
1200 Synopsis [Check if the two pairs exist in the table, If any of the
1201 conjuncts do exist, store in the cache and return the corresponding pair.]
1203 Description [Check if the two pairs exist in the table. If any of
1204 the conjuncts do exist, store in the cache and return the
1205 corresponding pair.]
1209 SeeAlso [ZeroCase BuildConjuncts]
1211 ******************************************************************************/
1220 st_table
* cacheTable
,
1223 int pairValue1
, pairValue2
;
1229 /* check existence of pair in table */
1230 pairValue1
= PairInTables(g1
, h1
, ghTable
);
1231 pairValue2
= PairInTables(g2
, h2
, ghTable
);
1233 /* if none of the 4 exist in the gh tables, return NULL */
1234 if ((pairValue1
== NONE
) && (pairValue2
== NONE
)) {
1238 factors
= ALLOC(Conjuncts
, 1);
1239 if (factors
== NULL
) {
1244 /* pairs that already exist in the table get preference. */
1245 if (pairValue1
== PAIR_ST
) {
1248 } else if (pairValue2
== PAIR_ST
) {
1251 } else if (pairValue1
== PAIR_CR
) {
1254 } else if (pairValue2
== PAIR_CR
) {
1257 } else if (pairValue1
== G_ST
) {
1258 /* g exists in the table, h is not found in either table */
1263 if (st_insert(ghTable
, (char *)Cudd_Regular(h1
),
1264 (char *)(long)value
) == ST_OUT_OF_MEM
) {
1270 } else if (pairValue1
== BOTH_G
) {
1271 /* g and h are found in the g table */
1276 if (st_insert(ghTable
, (char *)Cudd_Regular(h1
),
1277 (char *)(long)value
) == ST_OUT_OF_MEM
) {
1283 } else if (pairValue1
== H_ST
) {
1284 /* h exists in the table, g is not found in either table */
1289 if (st_insert(ghTable
, (char *)Cudd_Regular(g1
),
1290 (char *)(long)value
) == ST_OUT_OF_MEM
) {
1296 } else if (pairValue1
== BOTH_H
) {
1297 /* g and h are found in the h table */
1302 if (st_insert(ghTable
, (char *)Cudd_Regular(g1
),
1303 (char *)(long)value
) == ST_OUT_OF_MEM
) {
1309 } else if (pairValue2
== G_ST
) {
1310 /* g exists in the table, h is not found in either table */
1315 if (st_insert(ghTable
, (char *)Cudd_Regular(h2
),
1316 (char *)(long)value
) == ST_OUT_OF_MEM
) {
1322 } else if (pairValue2
== BOTH_G
) {
1323 /* g and h are found in the g table */
1328 if (st_insert(ghTable
, (char *)Cudd_Regular(h2
),
1329 (char *)(long)value
) == ST_OUT_OF_MEM
) {
1335 } else if (pairValue2
== H_ST
) {
1336 /* h exists in the table, g is not found in either table */
1341 if (st_insert(ghTable
, (char *)Cudd_Regular(g2
),
1342 (char *)(long)value
) == ST_OUT_OF_MEM
) {
1348 } else if (pairValue2
== BOTH_H
) {
1349 /* g and h are found in the h table */
1354 if (st_insert(ghTable
, (char *)Cudd_Regular(g2
),
1355 (char *)(long)value
) == ST_OUT_OF_MEM
) {
1361 } else if (pairValue1
== G_CR
) {
1362 /* g found in h table and h in none */
1367 if (st_insert(ghTable
, (char *)Cudd_Regular(h1
),
1368 (char *)(long)value
) == ST_OUT_OF_MEM
) {
1374 } else if (pairValue1
== H_CR
) {
1375 /* h found in g table and g in none */
1380 if (st_insert(ghTable
, (char *)Cudd_Regular(g1
),
1381 (char *)(long)value
) == ST_OUT_OF_MEM
) {
1387 } else if (pairValue2
== G_CR
) {
1388 /* g found in h table and h in none */
1393 if (st_insert(ghTable
, (char *)Cudd_Regular(h2
),
1394 (char *)(long)value
) == ST_OUT_OF_MEM
) {
1400 } else if (pairValue2
== H_CR
) {
1401 /* h found in g table and g in none */
1406 if (st_insert(ghTable
, (char *)Cudd_Regular(g2
),
1407 (char *)(long)value
) == ST_OUT_OF_MEM
) {
1415 /* Store factors in cache table for later use. */
1416 if (st_insert(cacheTable
, (char *)node
, (char *)factors
) ==
1423 } /* end of CheckInTables */
1427 /**Function********************************************************************
1429 Synopsis [If one child is zero, do explicitly what Restrict does or better]
1431 Description [If one child is zero, do explicitly what Restrict does or better.
1432 First separate a variable and its child in the base case. In case of a cube
1433 times a function, separate the cube and function. As a last resort, look in
1436 SideEffects [Frees the BDDs in factorsNv. factorsNv itself is not freed
1437 because it is freed above.]
1439 SeeAlso [BuildConjuncts]
1441 ******************************************************************************/
1446 Conjuncts
* factorsNv
,
1448 st_table
* cacheTable
,
1452 DdNode
*g
, *h
, *g1
, *g2
, *h1
, *h2
, *x
, *N
, *G
, *H
, *Gv
, *Gnv
;
1458 /* get var at this node */
1459 N
= Cudd_Regular(node
);
1461 x
= dd
->vars
[topid
];
1462 x
= (switched
) ? Cudd_Not(x
): x
;
1465 /* Seprate variable and child */
1466 if (factorsNv
->g
== one
) {
1467 Cudd_RecursiveDeref(dd
, factorsNv
->g
);
1468 factors
= ALLOC(Conjuncts
, 1);
1469 if (factors
== NULL
) {
1470 dd
->errorCode
= CUDD_MEMORY_OUT
;
1471 Cudd_RecursiveDeref(dd
, factorsNv
->h
);
1472 Cudd_RecursiveDeref(dd
, x
);
1476 factors
->h
= factorsNv
->h
;
1477 /* cache the result*/
1478 if (st_insert(cacheTable
, (char *)node
, (char *)factors
) == ST_OUT_OF_MEM
) {
1479 dd
->errorCode
= CUDD_MEMORY_OUT
;
1480 Cudd_RecursiveDeref(dd
, factorsNv
->h
);
1481 Cudd_RecursiveDeref(dd
, x
);
1486 /* store x in g table, the other node is already in the table */
1487 if (st_lookup_int(ghTable
, (char *)Cudd_Regular(x
), &value
)) {
1492 if (st_insert(ghTable
, (char *)Cudd_Regular(x
), (char *)(long)value
) == ST_OUT_OF_MEM
) {
1493 dd
->errorCode
= CUDD_MEMORY_OUT
;
1499 /* Seprate variable and child */
1500 if (factorsNv
->h
== one
) {
1501 Cudd_RecursiveDeref(dd
, factorsNv
->h
);
1502 factors
= ALLOC(Conjuncts
, 1);
1503 if (factors
== NULL
) {
1504 dd
->errorCode
= CUDD_MEMORY_OUT
;
1505 Cudd_RecursiveDeref(dd
, factorsNv
->g
);
1506 Cudd_RecursiveDeref(dd
, x
);
1509 factors
->g
= factorsNv
->g
;
1511 /* cache the result. */
1512 if (st_insert(cacheTable
, (char *)node
, (char *)factors
) == ST_OUT_OF_MEM
) {
1513 dd
->errorCode
= CUDD_MEMORY_OUT
;
1514 Cudd_RecursiveDeref(dd
, factorsNv
->g
);
1515 Cudd_RecursiveDeref(dd
, x
);
1519 /* store x in h table, the other node is already in the table */
1520 if (st_lookup_int(ghTable
, (char *)Cudd_Regular(x
), &value
)) {
1525 if (st_insert(ghTable
, (char *)Cudd_Regular(x
), (char *)(long)value
) == ST_OUT_OF_MEM
) {
1526 dd
->errorCode
= CUDD_MEMORY_OUT
;
1532 G
= Cudd_Regular(factorsNv
->g
);
1535 Gv
= Cudd_NotCond(Gv
, Cudd_IsComplement(node
));
1536 Gnv
= Cudd_NotCond(Gnv
, Cudd_IsComplement(node
));
1537 /* if the child below is a variable */
1538 if ((Gv
== zero
) || (Gnv
== zero
)) {
1540 g
= cuddBddAndRecur(dd
, x
, factorsNv
->g
);
1541 if (g
!= NULL
) cuddRef(g
);
1542 Cudd_RecursiveDeref(dd
, factorsNv
->g
);
1543 Cudd_RecursiveDeref(dd
, x
);
1545 Cudd_RecursiveDeref(dd
, factorsNv
->h
);
1548 /* CheckTablesCacheAndReturn responsible for allocating
1549 * factors structure., g,h referenced for cache store the
1551 factors
= CheckTablesCacheAndReturn(node
,
1556 if (factors
== NULL
) {
1557 dd
->errorCode
= CUDD_MEMORY_OUT
;
1558 Cudd_RecursiveDeref(dd
, g
);
1559 Cudd_RecursiveDeref(dd
, h
);
1564 H
= Cudd_Regular(factorsNv
->h
);
1567 Hv
= Cudd_NotCond(Hv
, Cudd_IsComplement(node
));
1568 Hnv
= Cudd_NotCond(Hnv
, Cudd_IsComplement(node
));
1569 /* if the child below is a variable */
1570 if ((Hv
== zero
) || (Hnv
== zero
)) {
1572 h
= cuddBddAndRecur(dd
, x
, factorsNv
->h
);
1573 if (h
!= NULL
) cuddRef(h
);
1574 Cudd_RecursiveDeref(dd
, factorsNv
->h
);
1575 Cudd_RecursiveDeref(dd
, x
);
1577 Cudd_RecursiveDeref(dd
, factorsNv
->g
);
1580 /* CheckTablesCacheAndReturn responsible for allocating
1581 * factors structure.g,h referenced for table store
1583 factors
= CheckTablesCacheAndReturn(node
,
1588 if (factors
== NULL
) {
1589 dd
->errorCode
= CUDD_MEMORY_OUT
;
1590 Cudd_RecursiveDeref(dd
, g
);
1591 Cudd_RecursiveDeref(dd
, h
);
1596 /* build g1 = x*g; h1 = h */
1597 /* build g2 = g; h2 = x*h */
1598 Cudd_RecursiveDeref(dd
, x
);
1600 g1
= cuddBddAndRecur(dd
, x
, factorsNv
->g
);
1601 if (g1
!= NULL
) cuddRef(g1
);
1603 Cudd_RecursiveDeref(dd
, factorsNv
->g
);
1604 Cudd_RecursiveDeref(dd
, factorsNv
->h
);
1609 h2
= cuddBddAndRecur(dd
, x
, factorsNv
->h
);
1610 if (h2
!= NULL
) cuddRef(h2
);
1612 Cudd_RecursiveDeref(dd
, factorsNv
->h
);
1613 Cudd_RecursiveDeref(dd
, factorsNv
->g
);
1617 /* check whether any pair is in tables */
1618 factors
= CheckInTables(node
, g1
, h1
, g2
, h2
, ghTable
, cacheTable
, &outOfMem
);
1620 dd
->errorCode
= CUDD_MEMORY_OUT
;
1621 Cudd_RecursiveDeref(dd
, g1
);
1622 Cudd_RecursiveDeref(dd
, h1
);
1623 Cudd_RecursiveDeref(dd
, g2
);
1624 Cudd_RecursiveDeref(dd
, h2
);
1627 if (factors
!= NULL
) {
1628 if ((factors
->g
== g1
) || (factors
->g
== h1
)) {
1629 Cudd_RecursiveDeref(dd
, g2
);
1630 Cudd_RecursiveDeref(dd
, h2
);
1632 Cudd_RecursiveDeref(dd
, g1
);
1633 Cudd_RecursiveDeref(dd
, h1
);
1638 /* check for each pair in tables and choose one */
1639 factors
= PickOnePair(node
,g1
, h1
, g2
, h2
, ghTable
, cacheTable
);
1640 if (factors
== NULL
) {
1641 dd
->errorCode
= CUDD_MEMORY_OUT
;
1642 Cudd_RecursiveDeref(dd
, g1
);
1643 Cudd_RecursiveDeref(dd
, h1
);
1644 Cudd_RecursiveDeref(dd
, g2
);
1645 Cudd_RecursiveDeref(dd
, h2
);
1647 /* now free what was created and not used */
1648 if ((factors
->g
== g1
) || (factors
->g
== h1
)) {
1649 Cudd_RecursiveDeref(dd
, g2
);
1650 Cudd_RecursiveDeref(dd
, h2
);
1652 Cudd_RecursiveDeref(dd
, g1
);
1653 Cudd_RecursiveDeref(dd
, h1
);
1658 } /* end of ZeroCase */
1661 /**Function********************************************************************
1663 Synopsis [Builds the conjuncts recursively, bottom up.]
1665 Description [Builds the conjuncts recursively, bottom up. Constants
1666 are returned as (f, f). The cache is checked for previously computed
1667 result. The decomposition points are determined by the local
1668 reference count of this node and the longest distance from the
1669 constant. At the decomposition point, the factors returned are (f,
1670 1). Recur on the two children. The order is determined by the
1671 heavier branch. Combine the factors of the two children and pick the
1672 one that already occurs in the gh table. Occurence in g is indicated
1673 by value 1, occurence in h by 2, occurence in both 3.]
1677 SeeAlso [cuddConjunctsAux]
1679 ******************************************************************************/
1684 st_table
* distanceTable
,
1685 st_table
* cacheTable
,
1689 st_table
* mintermTable
)
1691 int topid
, distance
;
1692 Conjuncts
*factorsNv
, *factorsNnv
, *factors
;
1694 DdNode
*N
, *Nv
, *Nnv
, *temp
, *g1
, *g2
, *h1
, *h2
, *topv
;
1695 double minNv
= 0.0, minNnv
= 0.0;
1696 double *doubleDummy
;
1699 int freeNv
= 0, freeNnv
= 0, freeTemp
;
1703 /* if f is constant, return (f,f) */
1704 if (Cudd_IsConstant(node
)) {
1705 factors
= ALLOC(Conjuncts
, 1);
1706 if (factors
== NULL
) {
1707 dd
->errorCode
= CUDD_MEMORY_OUT
;
1712 return(FactorsComplement(factors
));
1715 /* If result (a pair of conjuncts) in cache, return the factors. */
1716 if (st_lookup(cacheTable
, node
, &dummy
)) {
1721 /* check distance and local reference count of this node */
1722 N
= Cudd_Regular(node
);
1723 if (!st_lookup(distanceTable
, N
, &nodeStat
)) {
1724 (void) fprintf(dd
->err
, "Not in table, Something wrong\n");
1725 dd
->errorCode
= CUDD_INTERNAL_ERROR
;
1728 distance
= nodeStat
->distance
;
1730 /* at or below decomposition point, return (f, 1) */
1731 if (((nodeStat
->localRef
> maxLocalRef
*2/3) &&
1732 (distance
< approxDistance
*2/3)) ||
1733 (distance
<= approxDistance
/4)) {
1734 factors
= ALLOC(Conjuncts
, 1);
1735 if (factors
== NULL
) {
1736 dd
->errorCode
= CUDD_MEMORY_OUT
;
1739 /* alternate assigning (f,1) */
1741 if (st_lookup_int(ghTable
, (char *)Cudd_Regular(node
), &value
)) {
1752 } else if (value
== 1) {
1759 } else if (!lastTimeG
) {
1764 if (st_insert(ghTable
, (char *)Cudd_Regular(node
), (char *)(long)value
) == ST_OUT_OF_MEM
) {
1765 dd
->errorCode
= CUDD_MEMORY_OUT
;
1774 if (st_insert(ghTable
, (char *)Cudd_Regular(node
), (char *)(long)value
) == ST_OUT_OF_MEM
) {
1775 dd
->errorCode
= CUDD_MEMORY_OUT
;
1780 return(FactorsComplement(factors
));
1783 /* get the children and recur */
1786 Nv
= Cudd_NotCond(Nv
, Cudd_IsComplement(node
));
1787 Nnv
= Cudd_NotCond(Nnv
, Cudd_IsComplement(node
));
1789 /* Choose which subproblem to solve first based on the number of
1790 * minterms. We go first where there are more minterms.
1792 if (!Cudd_IsConstant(Nv
)) {
1793 if (!st_lookup(mintermTable
, Nv
, &doubleDummy
)) {
1794 (void) fprintf(dd
->err
, "Not in table: Something wrong\n");
1795 dd
->errorCode
= CUDD_INTERNAL_ERROR
;
1798 minNv
= *doubleDummy
;
1801 if (!Cudd_IsConstant(Nnv
)) {
1802 if (!st_lookup(mintermTable
, Nnv
, &doubleDummy
)) {
1803 (void) fprintf(dd
->err
, "Not in table: Something wrong\n");
1804 dd
->errorCode
= CUDD_INTERNAL_ERROR
;
1807 minNnv
= *doubleDummy
;
1810 if (minNv
< minNnv
) {
1817 /* build gt, ht recursively */
1819 factorsNv
= BuildConjuncts(dd
, Nv
, distanceTable
,
1820 cacheTable
, approxDistance
, maxLocalRef
,
1821 ghTable
, mintermTable
);
1822 if (factorsNv
== NULL
) return(NULL
);
1823 freeNv
= FactorsNotStored(factorsNv
);
1824 factorsNv
= (freeNv
) ? FactorsUncomplement(factorsNv
) : factorsNv
;
1825 cuddRef(factorsNv
->g
);
1826 cuddRef(factorsNv
->h
);
1828 /* Deal with the zero case */
1830 /* is responsible for freeing factorsNv */
1831 factors
= ZeroCase(dd
, node
, factorsNv
, ghTable
,
1832 cacheTable
, switched
);
1833 if (freeNv
) FREE(factorsNv
);
1838 /* build ge, he recursively */
1840 factorsNnv
= BuildConjuncts(dd
, Nnv
, distanceTable
,
1841 cacheTable
, approxDistance
, maxLocalRef
,
1842 ghTable
, mintermTable
);
1843 if (factorsNnv
== NULL
) {
1844 Cudd_RecursiveDeref(dd
, factorsNv
->g
);
1845 Cudd_RecursiveDeref(dd
, factorsNv
->h
);
1846 if (freeNv
) FREE(factorsNv
);
1849 freeNnv
= FactorsNotStored(factorsNnv
);
1850 factorsNnv
= (freeNnv
) ? FactorsUncomplement(factorsNnv
) : factorsNnv
;
1851 cuddRef(factorsNnv
->g
);
1852 cuddRef(factorsNnv
->h
);
1854 /* Deal with the zero case */
1856 /* is responsible for freeing factorsNv */
1857 factors
= ZeroCase(dd
, node
, factorsNnv
, ghTable
,
1858 cacheTable
, switched
);
1859 if (freeNnv
) FREE(factorsNnv
);
1864 /* construct the 2 pairs */
1865 /* g1 = x*gt + x'*ge; h1 = x*ht + x'*he; */
1866 /* g2 = x*gt + x'*he; h2 = x*ht + x'*ge */
1868 factors
= factorsNnv
;
1869 factorsNnv
= factorsNv
;
1870 factorsNv
= factors
;
1876 /* Build the factors for this node. */
1878 topv
= dd
->vars
[topid
];
1880 g1
= cuddBddIteRecur(dd
, topv
, factorsNv
->g
, factorsNnv
->g
);
1882 Cudd_RecursiveDeref(dd
, factorsNv
->g
);
1883 Cudd_RecursiveDeref(dd
, factorsNv
->h
);
1884 Cudd_RecursiveDeref(dd
, factorsNnv
->g
);
1885 Cudd_RecursiveDeref(dd
, factorsNnv
->h
);
1886 if (freeNv
) FREE(factorsNv
);
1887 if (freeNnv
) FREE(factorsNnv
);
1893 h1
= cuddBddIteRecur(dd
, topv
, factorsNv
->h
, factorsNnv
->h
);
1895 Cudd_RecursiveDeref(dd
, factorsNv
->g
);
1896 Cudd_RecursiveDeref(dd
, factorsNv
->h
);
1897 Cudd_RecursiveDeref(dd
, factorsNnv
->g
);
1898 Cudd_RecursiveDeref(dd
, factorsNnv
->h
);
1899 Cudd_RecursiveDeref(dd
, g1
);
1900 if (freeNv
) FREE(factorsNv
);
1901 if (freeNnv
) FREE(factorsNnv
);
1907 g2
= cuddBddIteRecur(dd
, topv
, factorsNv
->g
, factorsNnv
->h
);
1909 Cudd_RecursiveDeref(dd
, factorsNv
->h
);
1910 Cudd_RecursiveDeref(dd
, factorsNv
->g
);
1911 Cudd_RecursiveDeref(dd
, factorsNnv
->g
);
1912 Cudd_RecursiveDeref(dd
, factorsNnv
->h
);
1913 Cudd_RecursiveDeref(dd
, g1
);
1914 Cudd_RecursiveDeref(dd
, h1
);
1915 if (freeNv
) FREE(factorsNv
);
1916 if (freeNnv
) FREE(factorsNnv
);
1920 Cudd_RecursiveDeref(dd
, factorsNv
->g
);
1921 Cudd_RecursiveDeref(dd
, factorsNnv
->h
);
1923 h2
= cuddBddIteRecur(dd
, topv
, factorsNv
->h
, factorsNnv
->g
);
1925 Cudd_RecursiveDeref(dd
, factorsNv
->g
);
1926 Cudd_RecursiveDeref(dd
, factorsNv
->h
);
1927 Cudd_RecursiveDeref(dd
, factorsNnv
->g
);
1928 Cudd_RecursiveDeref(dd
, factorsNnv
->h
);
1929 Cudd_RecursiveDeref(dd
, g1
);
1930 Cudd_RecursiveDeref(dd
, h1
);
1931 Cudd_RecursiveDeref(dd
, g2
);
1932 if (freeNv
) FREE(factorsNv
);
1933 if (freeNnv
) FREE(factorsNnv
);
1937 Cudd_RecursiveDeref(dd
, factorsNv
->h
);
1938 Cudd_RecursiveDeref(dd
, factorsNnv
->g
);
1939 if (freeNv
) FREE(factorsNv
);
1940 if (freeNnv
) FREE(factorsNnv
);
1942 /* check for each pair in tables and choose one */
1943 factors
= CheckInTables(node
, g1
, h1
, g2
, h2
, ghTable
, cacheTable
, &outOfMem
);
1945 dd
->errorCode
= CUDD_MEMORY_OUT
;
1946 Cudd_RecursiveDeref(dd
, g1
);
1947 Cudd_RecursiveDeref(dd
, h1
);
1948 Cudd_RecursiveDeref(dd
, g2
);
1949 Cudd_RecursiveDeref(dd
, h2
);
1952 if (factors
!= NULL
) {
1953 if ((factors
->g
== g1
) || (factors
->g
== h1
)) {
1954 Cudd_RecursiveDeref(dd
, g2
);
1955 Cudd_RecursiveDeref(dd
, h2
);
1957 Cudd_RecursiveDeref(dd
, g1
);
1958 Cudd_RecursiveDeref(dd
, h1
);
1963 /* if not in tables, pick one pair */
1964 factors
= PickOnePair(node
,g1
, h1
, g2
, h2
, ghTable
, cacheTable
);
1965 if (factors
== NULL
) {
1966 dd
->errorCode
= CUDD_MEMORY_OUT
;
1967 Cudd_RecursiveDeref(dd
, g1
);
1968 Cudd_RecursiveDeref(dd
, h1
);
1969 Cudd_RecursiveDeref(dd
, g2
);
1970 Cudd_RecursiveDeref(dd
, h2
);
1972 /* now free what was created and not used */
1973 if ((factors
->g
== g1
) || (factors
->g
== h1
)) {
1974 Cudd_RecursiveDeref(dd
, g2
);
1975 Cudd_RecursiveDeref(dd
, h2
);
1977 Cudd_RecursiveDeref(dd
, g1
);
1978 Cudd_RecursiveDeref(dd
, h1
);
1984 } /* end of BuildConjuncts */
1987 /**Function********************************************************************
1989 Synopsis [Procedure to compute two conjunctive factors of f and place in *c1 and *c2.]
1991 Description [Procedure to compute two conjunctive factors of f and
1992 place in *c1 and *c2. Sets up the required data - table of distances
1993 from the constant and local reference count. Also minterm table. ]
1999 ******************************************************************************/
2007 st_table
*distanceTable
= NULL
;
2008 st_table
*cacheTable
= NULL
;
2009 st_table
*mintermTable
= NULL
;
2010 st_table
*ghTable
= NULL
;
2011 st_generator
*stGen
;
2014 int distance
, approxDistance
;
2015 double max
, minterms
;
2024 /* initialize distances table */
2025 distanceTable
= st_init_table(st_ptrcmp
,st_ptrhash
);
2026 if (distanceTable
== NULL
) goto outOfMem
;
2028 /* make the entry for the constant */
2029 nodeStat
= ALLOC(NodeStat
, 1);
2030 if (nodeStat
== NULL
) goto outOfMem
;
2031 nodeStat
->distance
= 0;
2032 nodeStat
->localRef
= 1;
2033 if (st_insert(distanceTable
, (char *)one
, (char *)nodeStat
) == ST_OUT_OF_MEM
) {
2037 /* Count node distances from constant. */
2038 nodeStat
= CreateBotDist(f
, distanceTable
);
2039 if (nodeStat
== NULL
) goto outOfMem
;
2041 /* set the distance for the decomposition points */
2042 approxDistance
= (DEPTH
< nodeStat
->distance
) ? nodeStat
->distance
: DEPTH
;
2043 distance
= nodeStat
->distance
;
2045 if (distance
< approxDistance
) {
2046 /* Too small to bother. */
2049 cuddRef(*c1
); cuddRef(*c2
);
2050 stGen
= st_init_gen(distanceTable
);
2051 if (stGen
== NULL
) goto outOfMem
;
2052 while(st_gen(stGen
, (char **)&key
, (char **)&value
)) {
2055 st_free_gen(stGen
); stGen
= NULL
;
2056 st_free_table(distanceTable
);
2060 /* record the maximum local reference count */
2062 stGen
= st_init_gen(distanceTable
);
2063 if (stGen
== NULL
) goto outOfMem
;
2064 while(st_gen(stGen
, (char **)&key
, (char **)&value
)) {
2065 nodeStat
= (NodeStat
*)value
;
2066 maxLocalRef
= (nodeStat
->localRef
> maxLocalRef
) ?
2067 nodeStat
->localRef
: maxLocalRef
;
2069 st_free_gen(stGen
); stGen
= NULL
;
2072 /* Count minterms for each node. */
2073 max
= pow(2.0, (double)Cudd_SupportSize(dd
,f
)); /* potential overflow */
2074 mintermTable
= st_init_table(st_ptrcmp
,st_ptrhash
);
2075 if (mintermTable
== NULL
) goto outOfMem
;
2076 minterms
= CountMinterms(f
, max
, mintermTable
, dd
->err
);
2077 if (minterms
== -1.0) goto outOfMem
;
2079 lastTimeG
= Cudd_Random() & 1;
2080 cacheTable
= st_init_table(st_ptrcmp
, st_ptrhash
);
2081 if (cacheTable
== NULL
) goto outOfMem
;
2082 ghTable
= st_init_table(st_ptrcmp
, st_ptrhash
);
2083 if (ghTable
== NULL
) goto outOfMem
;
2085 /* Build conjuncts. */
2086 factors
= BuildConjuncts(dd
, f
, distanceTable
, cacheTable
,
2087 approxDistance
, maxLocalRef
, ghTable
, mintermTable
);
2088 if (factors
== NULL
) goto outOfMem
;
2090 /* free up tables */
2091 stGen
= st_init_gen(distanceTable
);
2092 if (stGen
== NULL
) goto outOfMem
;
2093 while(st_gen(stGen
, (char **)&key
, (char **)&value
)) {
2096 st_free_gen(stGen
); stGen
= NULL
;
2097 st_free_table(distanceTable
); distanceTable
= NULL
;
2098 st_free_table(ghTable
); ghTable
= NULL
;
2100 stGen
= st_init_gen(mintermTable
);
2101 if (stGen
== NULL
) goto outOfMem
;
2102 while(st_gen(stGen
, (char **)&key
, (char **)&value
)) {
2105 st_free_gen(stGen
); stGen
= NULL
;
2106 st_free_table(mintermTable
); mintermTable
= NULL
;
2108 freeFactors
= FactorsNotStored(factors
);
2109 factors
= (freeFactors
) ? FactorsUncomplement(factors
) : factors
;
2110 if (factors
!= NULL
) {
2115 if (freeFactors
) FREE(factors
);
2118 if ((*c1
== f
) && (!Cudd_IsConstant(f
))) {
2121 if ((*c2
== f
) && (!Cudd_IsConstant(f
))) {
2125 if ((*c1
!= one
) && (!Cudd_IsConstant(f
))) {
2126 assert(!Cudd_bddLeq(dd
, *c2
, *c1
));
2128 if ((*c2
!= one
) && (!Cudd_IsConstant(f
))) {
2129 assert(!Cudd_bddLeq(dd
, *c1
, *c2
));
2134 stGen
= st_init_gen(cacheTable
);
2135 if (stGen
== NULL
) goto outOfMem
;
2136 while(st_gen(stGen
, (char **)&key
, (char **)&value
)) {
2137 ConjunctsFree(dd
, (Conjuncts
*)value
);
2139 st_free_gen(stGen
); stGen
= NULL
;
2141 st_free_table(cacheTable
); cacheTable
= NULL
;
2146 if (distanceTable
!= NULL
) {
2147 stGen
= st_init_gen(distanceTable
);
2148 if (stGen
== NULL
) goto outOfMem
;
2149 while(st_gen(stGen
, (char **)&key
, (char **)&value
)) {
2152 st_free_gen(stGen
); stGen
= NULL
;
2153 st_free_table(distanceTable
); distanceTable
= NULL
;
2155 if (mintermTable
!= NULL
) {
2156 stGen
= st_init_gen(mintermTable
);
2157 if (stGen
== NULL
) goto outOfMem
;
2158 while(st_gen(stGen
, (char **)&key
, (char **)&value
)) {
2161 st_free_gen(stGen
); stGen
= NULL
;
2162 st_free_table(mintermTable
); mintermTable
= NULL
;
2164 if (ghTable
!= NULL
) st_free_table(ghTable
);
2165 if (cacheTable
!= NULL
) {
2166 stGen
= st_init_gen(cacheTable
);
2167 if (stGen
== NULL
) goto outOfMem
;
2168 while(st_gen(stGen
, (char **)&key
, (char **)&value
)) {
2169 ConjunctsFree(dd
, (Conjuncts
*)value
);
2171 st_free_gen(stGen
); stGen
= NULL
;
2172 st_free_table(cacheTable
); cacheTable
= NULL
;
2174 dd
->errorCode
= CUDD_MEMORY_OUT
;
2177 } /* end of cuddConjunctsAux */