source: vis_dev/glu-2.3/src/cuBdd/cuddApprox.c@ 104

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

library glu 2.3
File size: 66.6 KB
Line 
1/**CFile***********************************************************************
2
3 FileName [cuddApprox.c]
4
5 PackageName [cudd]
6
7 Synopsis [Procedures to approximate a given BDD.]
8
9 Description [External procedures provided by this module:
10 <ul>
11 <li> Cudd_UnderApprox()
12 <li> Cudd_OverApprox()
13 <li> Cudd_RemapUnderApprox()
14 <li> Cudd_RemapOverApprox()
15 <li> Cudd_BiasedUnderApprox()
16 <li> Cudd_BiasedOverApprox()
17 </ul>
18 Internal procedures included in this module:
19 <ul>
20 <li> cuddUnderApprox()
21 <li> cuddRemapUnderApprox()
22 <li> cuddBiasedUnderApprox()
23 </ul>
24 Static procedures included in this module:
25 <ul>
26 <li> gatherInfoAux()
27 <li> gatherInfo()
28 <li> computeSavings()
29 <li> UAmarkNodes()
30 <li> UAbuildSubset()
31 <li> updateRefs()
32 <li> RAmarkNodes()
33 <li> BAmarkNodes()
34 <li> RAbuildSubset()
35 </ul>
36 ]
37
38 SeeAlso [cuddSubsetHB.c cuddSubsetSP.c cuddGenCof.c]
39
40 Author [Fabio Somenzi]
41
42 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
43
44 All rights reserved.
45
46 Redistribution and use in source and binary forms, with or without
47 modification, are permitted provided that the following conditions
48 are met:
49
50 Redistributions of source code must retain the above copyright
51 notice, this list of conditions and the following disclaimer.
52
53 Redistributions in binary form must reproduce the above copyright
54 notice, this list of conditions and the following disclaimer in the
55 documentation and/or other materials provided with the distribution.
56
57 Neither the name of the University of Colorado nor the names of its
58 contributors may be used to endorse or promote products derived from
59 this software without specific prior written permission.
60
61 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
62 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
63 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
64 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
65 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
66 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
67 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
68 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
69 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
70 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
71 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
72 POSSIBILITY OF SUCH DAMAGE.]
73
74******************************************************************************/
75
76#ifdef __STDC__
77#include <float.h>
78#else
79#define DBL_MAX_EXP 1024
80#endif
81#include "util.h"
82#include "cuddInt.h"
83
84/*---------------------------------------------------------------------------*/
85/* Constant declarations */
86/*---------------------------------------------------------------------------*/
87
88#define NOTHING 0
89#define REPLACE_T 1
90#define REPLACE_E 2
91#define REPLACE_N 3
92#define REPLACE_TT 4
93#define REPLACE_TE 5
94
95#define DONT_CARE 0
96#define CARE 1
97#define TOTAL_CARE 2
98#define CARE_ERROR 3
99
100/*---------------------------------------------------------------------------*/
101/* Stucture declarations */
102/*---------------------------------------------------------------------------*/
103
104/*---------------------------------------------------------------------------*/
105/* Type declarations */
106/*---------------------------------------------------------------------------*/
107
108/* Data structure to store the information on each node. It keeps the
109** number of minterms of the function rooted at this node in terms of
110** the number of variables specified by the user; the number of
111** minterms of the complement; the impact of the number of minterms of
112** this function on the number of minterms of the root function; the
113** reference count of the node from within the root function; the
114** reference count of the node from an internal node; and the flag
115** that says whether the node should be replaced and how. */
116typedef struct NodeData {
117 double mintermsP; /* minterms for the regular node */
118 double mintermsN; /* minterms for the complemented node */
119 int functionRef; /* references from within this function */
120 char care; /* node intersects care set */
121 char replace; /* replacement decision */
122 short int parity; /* 1: even; 2: odd; 3: both */
123 DdNode *resultP; /* result for even parity */
124 DdNode *resultN; /* result for odd parity */
125} NodeData;
126
127typedef struct ApproxInfo {
128 DdNode *one; /* one constant */
129 DdNode *zero; /* BDD zero constant */
130 NodeData *page; /* per-node information */
131 st_table *table; /* hash table to access the per-node info */
132 int index; /* index of the current node */
133 double max; /* max number of minterms */
134 int size; /* how many nodes are left */
135 double minterms; /* how many minterms are left */
136} ApproxInfo;
137
138/* Item of the queue used in the levelized traversal of the BDD. */
139#ifdef __osf__
140#pragma pointer_size save
141#pragma pointer_size short
142#endif
143typedef struct GlobalQueueItem {
144 struct GlobalQueueItem *next;
145 struct GlobalQueueItem *cnext;
146 DdNode *node;
147 double impactP;
148 double impactN;
149} GlobalQueueItem;
150
151typedef struct LocalQueueItem {
152 struct LocalQueueItem *next;
153 struct LocalQueueItem *cnext;
154 DdNode *node;
155 int localRef;
156} LocalQueueItem;
157#ifdef __osf__
158#pragma pointer_size restore
159#endif
160
161
162/*---------------------------------------------------------------------------*/
163/* Variable declarations */
164/*---------------------------------------------------------------------------*/
165
166#ifndef lint
167static char rcsid[] DD_UNUSED = "$Id: cuddApprox.c,v 1.27 2009/02/19 16:16:51 fabio Exp $";
168#endif
169
170/*---------------------------------------------------------------------------*/
171/* Macro declarations */
172/*---------------------------------------------------------------------------*/
173
174/**AutomaticStart*************************************************************/
175
176/*---------------------------------------------------------------------------*/
177/* Static function prototypes */
178/*---------------------------------------------------------------------------*/
179
180static void updateParity (DdNode *node, ApproxInfo *info, int newparity);
181static NodeData * gatherInfoAux (DdNode *node, ApproxInfo *info, int parity);
182static ApproxInfo * gatherInfo (DdManager *dd, DdNode *node, int numVars, int parity);
183static int computeSavings (DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue);
184static int updateRefs (DdManager *dd, DdNode *f, DdNode *skip, ApproxInfo *info, DdLevelQueue *queue);
185static int UAmarkNodes (DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, int safe, double quality);
186static DdNode * UAbuildSubset (DdManager *dd, DdNode *node, ApproxInfo *info);
187static int RAmarkNodes (DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, double quality);
188static int BAmarkNodes (DdManager *dd, DdNode *f, ApproxInfo *info, int threshold, double quality1, double quality0);
189static DdNode * RAbuildSubset (DdManager *dd, DdNode *node, ApproxInfo *info);
190static int BAapplyBias (DdManager *dd, DdNode *f, DdNode *b, ApproxInfo *info, DdHashTable *cache);
191
192/**AutomaticEnd***************************************************************/
193
194
195/*---------------------------------------------------------------------------*/
196/* Definition of exported functions */
197/*---------------------------------------------------------------------------*/
198
199/**Function********************************************************************
200
201 Synopsis [Extracts a dense subset from a BDD with Shiple's
202 underapproximation method.]
203
204 Description [Extracts a dense subset from a BDD. This procedure uses
205 a variant of Tom Shiple's underapproximation method. The main
206 difference from the original method is that density is used as cost
207 function. Returns a pointer to the BDD of the subset if
208 successful. NULL if the procedure runs out of memory. The parameter
209 numVars is the maximum number of variables to be used in minterm
210 calculation. The optimal number should be as close as possible to
211 the size of the support of f. However, it is safe to pass the value
212 returned by Cudd_ReadSize for numVars when the number of variables
213 is under 1023. If numVars is larger than 1023, it will cause
214 overflow. If a 0 parameter is passed then the procedure will compute
215 a value which will avoid overflow but will cause underflow with 2046
216 variables or more.]
217
218 SideEffects [None]
219
220 SeeAlso [Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_ReadSize]
221
222******************************************************************************/
223DdNode *
224Cudd_UnderApprox(
225 DdManager * dd /* manager */,
226 DdNode * f /* function to be subset */,
227 int numVars /* number of variables in the support of f */,
228 int threshold /* when to stop approximation */,
229 int safe /* enforce safe approximation */,
230 double quality /* minimum improvement for accepted changes */)
231{
232 DdNode *subset;
233
234 do {
235 dd->reordered = 0;
236 subset = cuddUnderApprox(dd, f, numVars, threshold, safe, quality);
237 } while (dd->reordered == 1);
238
239 return(subset);
240
241} /* end of Cudd_UnderApprox */
242
243
244/**Function********************************************************************
245
246 Synopsis [Extracts a dense superset from a BDD with Shiple's
247 underapproximation method.]
248
249 Description [Extracts a dense superset from a BDD. The procedure is
250 identical to the underapproximation procedure except for the fact that it
251 works on the complement of the given function. Extracting the subset
252 of the complement function is equivalent to extracting the superset
253 of the function.
254 Returns a pointer to the BDD of the superset if successful. NULL if
255 intermediate result causes the procedure to run out of memory. The
256 parameter numVars is the maximum number of variables to be used in
257 minterm calculation. The optimal number
258 should be as close as possible to the size of the support of f.
259 However, it is safe to pass the value returned by Cudd_ReadSize for
260 numVars when the number of variables is under 1023. If numVars is
261 larger than 1023, it will overflow. If a 0 parameter is passed then
262 the procedure will compute a value which will avoid overflow but
263 will cause underflow with 2046 variables or more.]
264
265 SideEffects [None]
266
267 SeeAlso [Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths Cudd_ReadSize]
268
269******************************************************************************/
270DdNode *
271Cudd_OverApprox(
272 DdManager * dd /* manager */,
273 DdNode * f /* function to be superset */,
274 int numVars /* number of variables in the support of f */,
275 int threshold /* when to stop approximation */,
276 int safe /* enforce safe approximation */,
277 double quality /* minimum improvement for accepted changes */)
278{
279 DdNode *subset, *g;
280
281 g = Cudd_Not(f);
282 do {
283 dd->reordered = 0;
284 subset = cuddUnderApprox(dd, g, numVars, threshold, safe, quality);
285 } while (dd->reordered == 1);
286
287 return(Cudd_NotCond(subset, (subset != NULL)));
288
289} /* end of Cudd_OverApprox */
290
291
292/**Function********************************************************************
293
294 Synopsis [Extracts a dense subset from a BDD with the remapping
295 underapproximation method.]
296
297 Description [Extracts a dense subset from a BDD. This procedure uses
298 a remapping technique and density as the cost function.
299 Returns a pointer to the BDD of the subset if
300 successful. NULL if the procedure runs out of memory. The parameter
301 numVars is the maximum number of variables to be used in minterm
302 calculation. The optimal number should be as close as possible to
303 the size of the support of f. However, it is safe to pass the value
304 returned by Cudd_ReadSize for numVars when the number of variables
305 is under 1023. If numVars is larger than 1023, it will cause
306 overflow. If a 0 parameter is passed then the procedure will compute
307 a value which will avoid overflow but will cause underflow with 2046
308 variables or more.]
309
310 SideEffects [None]
311
312 SeeAlso [Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_UnderApprox Cudd_ReadSize]
313
314******************************************************************************/
315DdNode *
316Cudd_RemapUnderApprox(
317 DdManager * dd /* manager */,
318 DdNode * f /* function to be subset */,
319 int numVars /* number of variables in the support of f */,
320 int threshold /* when to stop approximation */,
321 double quality /* minimum improvement for accepted changes */)
322{
323 DdNode *subset;
324
325 do {
326 dd->reordered = 0;
327 subset = cuddRemapUnderApprox(dd, f, numVars, threshold, quality);
328 } while (dd->reordered == 1);
329
330 return(subset);
331
332} /* end of Cudd_RemapUnderApprox */
333
334
335/**Function********************************************************************
336
337 Synopsis [Extracts a dense superset from a BDD with the remapping
338 underapproximation method.]
339
340 Description [Extracts a dense superset from a BDD. The procedure is
341 identical to the underapproximation procedure except for the fact that it
342 works on the complement of the given function. Extracting the subset
343 of the complement function is equivalent to extracting the superset
344 of the function.
345 Returns a pointer to the BDD of the superset if successful. NULL if
346 intermediate result causes the procedure to run out of memory. The
347 parameter numVars is the maximum number of variables to be used in
348 minterm calculation. The optimal number
349 should be as close as possible to the size of the support of f.
350 However, it is safe to pass the value returned by Cudd_ReadSize for
351 numVars when the number of variables is under 1023. If numVars is
352 larger than 1023, it will overflow. If a 0 parameter is passed then
353 the procedure will compute a value which will avoid overflow but
354 will cause underflow with 2046 variables or more.]
355
356 SideEffects [None]
357
358 SeeAlso [Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths Cudd_ReadSize]
359
360******************************************************************************/
361DdNode *
362Cudd_RemapOverApprox(
363 DdManager * dd /* manager */,
364 DdNode * f /* function to be superset */,
365 int numVars /* number of variables in the support of f */,
366 int threshold /* when to stop approximation */,
367 double quality /* minimum improvement for accepted changes */)
368{
369 DdNode *subset, *g;
370
371 g = Cudd_Not(f);
372 do {
373 dd->reordered = 0;
374 subset = cuddRemapUnderApprox(dd, g, numVars, threshold, quality);
375 } while (dd->reordered == 1);
376
377 return(Cudd_NotCond(subset, (subset != NULL)));
378
379} /* end of Cudd_RemapOverApprox */
380
381
382/**Function********************************************************************
383
384 Synopsis [Extracts a dense subset from a BDD with the biased
385 underapproximation method.]
386
387 Description [Extracts a dense subset from a BDD. This procedure uses
388 a biased remapping technique and density as the cost function. The bias
389 is a function. This procedure tries to approximate where the bias is 0
390 and preserve the given function where the bias is 1.
391 Returns a pointer to the BDD of the subset if
392 successful. NULL if the procedure runs out of memory. The parameter
393 numVars is the maximum number of variables to be used in minterm
394 calculation. The optimal number should be as close as possible to
395 the size of the support of f. However, it is safe to pass the value
396 returned by Cudd_ReadSize for numVars when the number of variables
397 is under 1023. If numVars is larger than 1023, it will cause
398 overflow. If a 0 parameter is passed then the procedure will compute
399 a value which will avoid overflow but will cause underflow with 2046
400 variables or more.]
401
402 SideEffects [None]
403
404 SeeAlso [Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_UnderApprox
405 Cudd_RemapUnderApprox Cudd_ReadSize]
406
407******************************************************************************/
408DdNode *
409Cudd_BiasedUnderApprox(
410 DdManager *dd /* manager */,
411 DdNode *f /* function to be subset */,
412 DdNode *b /* bias function */,
413 int numVars /* number of variables in the support of f */,
414 int threshold /* when to stop approximation */,
415 double quality1 /* minimum improvement for accepted changes when b=1 */,
416 double quality0 /* minimum improvement for accepted changes when b=0 */)
417{
418 DdNode *subset;
419
420 do {
421 dd->reordered = 0;
422 subset = cuddBiasedUnderApprox(dd, f, b, numVars, threshold, quality1,
423 quality0);
424 } while (dd->reordered == 1);
425
426 return(subset);
427
428} /* end of Cudd_BiasedUnderApprox */
429
430
431/**Function********************************************************************
432
433 Synopsis [Extracts a dense superset from a BDD with the biased
434 underapproximation method.]
435
436 Description [Extracts a dense superset from a BDD. The procedure is
437 identical to the underapproximation procedure except for the fact that it
438 works on the complement of the given function. Extracting the subset
439 of the complement function is equivalent to extracting the superset
440 of the function.
441 Returns a pointer to the BDD of the superset if successful. NULL if
442 intermediate result causes the procedure to run out of memory. The
443 parameter numVars is the maximum number of variables to be used in
444 minterm calculation. The optimal number
445 should be as close as possible to the size of the support of f.
446 However, it is safe to pass the value returned by Cudd_ReadSize for
447 numVars when the number of variables is under 1023. If numVars is
448 larger than 1023, it will overflow. If a 0 parameter is passed then
449 the procedure will compute a value which will avoid overflow but
450 will cause underflow with 2046 variables or more.]
451
452 SideEffects [None]
453
454 SeeAlso [Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths
455 Cudd_RemapOverApprox Cudd_BiasedUnderApprox Cudd_ReadSize]
456
457******************************************************************************/
458DdNode *
459Cudd_BiasedOverApprox(
460 DdManager *dd /* manager */,
461 DdNode *f /* function to be superset */,
462 DdNode *b /* bias function */,
463 int numVars /* number of variables in the support of f */,
464 int threshold /* when to stop approximation */,
465 double quality1 /* minimum improvement for accepted changes when b=1*/,
466 double quality0 /* minimum improvement for accepted changes when b=0 */)
467{
468 DdNode *subset, *g;
469
470 g = Cudd_Not(f);
471 do {
472 dd->reordered = 0;
473 subset = cuddBiasedUnderApprox(dd, g, b, numVars, threshold, quality1,
474 quality0);
475 } while (dd->reordered == 1);
476
477 return(Cudd_NotCond(subset, (subset != NULL)));
478
479} /* end of Cudd_BiasedOverApprox */
480
481
482/*---------------------------------------------------------------------------*/
483/* Definition of internal functions */
484/*---------------------------------------------------------------------------*/
485
486
487/**Function********************************************************************
488
489 Synopsis [Applies Tom Shiple's underappoximation algorithm.]
490
491 Description [Applies Tom Shiple's underappoximation algorithm. Proceeds
492 in three phases:
493 <ul>
494 <li> collect information on each node in the BDD; this is done via DFS.
495 <li> traverse the BDD in top-down fashion and compute for each node
496 whether its elimination increases density.
497 <li> traverse the BDD via DFS and actually perform the elimination.
498 </ul>
499 Returns the approximated BDD if successful; NULL otherwise.]
500
501 SideEffects [None]
502
503 SeeAlso [Cudd_UnderApprox]
504
505******************************************************************************/
506DdNode *
507cuddUnderApprox(
508 DdManager * dd /* DD manager */,
509 DdNode * f /* current DD */,
510 int numVars /* maximum number of variables */,
511 int threshold /* threshold under which approximation stops */,
512 int safe /* enforce safe approximation */,
513 double quality /* minimum improvement for accepted changes */)
514{
515 ApproxInfo *info;
516 DdNode *subset;
517 int result;
518
519 if (f == NULL) {
520 fprintf(dd->err, "Cannot subset, nil object\n");
521 return(NULL);
522 }
523
524 if (Cudd_IsConstant(f)) {
525 return(f);
526 }
527
528 /* Create table where node data are accessible via a hash table. */
529 info = gatherInfo(dd, f, numVars, safe);
530 if (info == NULL) {
531 (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
532 dd->errorCode = CUDD_MEMORY_OUT;
533 return(NULL);
534 }
535
536 /* Mark nodes that should be replaced by zero. */
537 result = UAmarkNodes(dd, f, info, threshold, safe, quality);
538 if (result == 0) {
539 (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
540 FREE(info->page);
541 st_free_table(info->table);
542 FREE(info);
543 dd->errorCode = CUDD_MEMORY_OUT;
544 return(NULL);
545 }
546
547 /* Build the result. */
548 subset = UAbuildSubset(dd, f, info);
549#if 1
550 if (subset && info->size < Cudd_DagSize(subset))
551 (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
552 info->size, Cudd_DagSize(subset));
553#endif
554 FREE(info->page);
555 st_free_table(info->table);
556 FREE(info);
557
558#ifdef DD_DEBUG
559 if (subset != NULL) {
560 cuddRef(subset);
561#if 0
562 (void) Cudd_DebugCheck(dd);
563 (void) Cudd_CheckKeys(dd);
564#endif
565 if (!Cudd_bddLeq(dd, subset, f)) {
566 (void) fprintf(dd->err, "Wrong subset\n");
567 dd->errorCode = CUDD_INTERNAL_ERROR;
568 }
569 cuddDeref(subset);
570 }
571#endif
572 return(subset);
573
574} /* end of cuddUnderApprox */
575
576
577/**Function********************************************************************
578
579 Synopsis [Applies the remapping underappoximation algorithm.]
580
581 Description [Applies the remapping underappoximation algorithm.
582 Proceeds in three phases:
583 <ul>
584 <li> collect information on each node in the BDD; this is done via DFS.
585 <li> traverse the BDD in top-down fashion and compute for each node
586 whether remapping increases density.
587 <li> traverse the BDD via DFS and actually perform the elimination.
588 </ul>
589 Returns the approximated BDD if successful; NULL otherwise.]
590
591 SideEffects [None]
592
593 SeeAlso [Cudd_RemapUnderApprox]
594
595******************************************************************************/
596DdNode *
597cuddRemapUnderApprox(
598 DdManager * dd /* DD manager */,
599 DdNode * f /* current DD */,
600 int numVars /* maximum number of variables */,
601 int threshold /* threshold under which approximation stops */,
602 double quality /* minimum improvement for accepted changes */)
603{
604 ApproxInfo *info;
605 DdNode *subset;
606 int result;
607
608 if (f == NULL) {
609 fprintf(dd->err, "Cannot subset, nil object\n");
610 dd->errorCode = CUDD_INVALID_ARG;
611 return(NULL);
612 }
613
614 if (Cudd_IsConstant(f)) {
615 return(f);
616 }
617
618 /* Create table where node data are accessible via a hash table. */
619 info = gatherInfo(dd, f, numVars, TRUE);
620 if (info == NULL) {
621 (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
622 dd->errorCode = CUDD_MEMORY_OUT;
623 return(NULL);
624 }
625
626 /* Mark nodes that should be replaced by zero. */
627 result = RAmarkNodes(dd, f, info, threshold, quality);
628 if (result == 0) {
629 (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
630 FREE(info->page);
631 st_free_table(info->table);
632 FREE(info);
633 dd->errorCode = CUDD_MEMORY_OUT;
634 return(NULL);
635 }
636
637 /* Build the result. */
638 subset = RAbuildSubset(dd, f, info);
639#if 1
640 if (subset && info->size < Cudd_DagSize(subset))
641 (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
642 info->size, Cudd_DagSize(subset));
643#endif
644 FREE(info->page);
645 st_free_table(info->table);
646 FREE(info);
647
648#ifdef DD_DEBUG
649 if (subset != NULL) {
650 cuddRef(subset);
651#if 0
652 (void) Cudd_DebugCheck(dd);
653 (void) Cudd_CheckKeys(dd);
654#endif
655 if (!Cudd_bddLeq(dd, subset, f)) {
656 (void) fprintf(dd->err, "Wrong subset\n");
657 }
658 cuddDeref(subset);
659 dd->errorCode = CUDD_INTERNAL_ERROR;
660 }
661#endif
662 return(subset);
663
664} /* end of cuddRemapUnderApprox */
665
666
667/**Function********************************************************************
668
669 Synopsis [Applies the biased remapping underappoximation algorithm.]
670
671 Description [Applies the biased remapping underappoximation algorithm.
672 Proceeds in three phases:
673 <ul>
674 <li> collect information on each node in the BDD; this is done via DFS.
675 <li> traverse the BDD in top-down fashion and compute for each node
676 whether remapping increases density.
677 <li> traverse the BDD via DFS and actually perform the elimination.
678 </ul>
679 Returns the approximated BDD if successful; NULL otherwise.]
680
681 SideEffects [None]
682
683 SeeAlso [Cudd_BiasedUnderApprox]
684
685******************************************************************************/
686DdNode *
687cuddBiasedUnderApprox(
688 DdManager *dd /* DD manager */,
689 DdNode *f /* current DD */,
690 DdNode *b /* bias function */,
691 int numVars /* maximum number of variables */,
692 int threshold /* threshold under which approximation stops */,
693 double quality1 /* minimum improvement for accepted changes when b=1 */,
694 double quality0 /* minimum improvement for accepted changes when b=0 */)
695{
696 ApproxInfo *info;
697 DdNode *subset;
698 int result;
699 DdHashTable *cache;
700
701 if (f == NULL) {
702 fprintf(dd->err, "Cannot subset, nil object\n");
703 dd->errorCode = CUDD_INVALID_ARG;
704 return(NULL);
705 }
706
707 if (Cudd_IsConstant(f)) {
708 return(f);
709 }
710
711 /* Create table where node data are accessible via a hash table. */
712 info = gatherInfo(dd, f, numVars, TRUE);
713 if (info == NULL) {
714 (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
715 dd->errorCode = CUDD_MEMORY_OUT;
716 return(NULL);
717 }
718
719 cache = cuddHashTableInit(dd,2,2);
720 result = BAapplyBias(dd, Cudd_Regular(f), b, info, cache);
721 if (result == CARE_ERROR) {
722 (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
723 cuddHashTableQuit(cache);
724 FREE(info->page);
725 st_free_table(info->table);
726 FREE(info);
727 dd->errorCode = CUDD_MEMORY_OUT;
728 return(NULL);
729 }
730 cuddHashTableQuit(cache);
731
732 /* Mark nodes that should be replaced by zero. */
733 result = BAmarkNodes(dd, f, info, threshold, quality1, quality0);
734 if (result == 0) {
735 (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
736 FREE(info->page);
737 st_free_table(info->table);
738 FREE(info);
739 dd->errorCode = CUDD_MEMORY_OUT;
740 return(NULL);
741 }
742
743 /* Build the result. */
744 subset = RAbuildSubset(dd, f, info);
745#if 1
746 if (subset && info->size < Cudd_DagSize(subset))
747 (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
748 info->size, Cudd_DagSize(subset));
749#endif
750 FREE(info->page);
751 st_free_table(info->table);
752 FREE(info);
753
754#ifdef DD_DEBUG
755 if (subset != NULL) {
756 cuddRef(subset);
757#if 0
758 (void) Cudd_DebugCheck(dd);
759 (void) Cudd_CheckKeys(dd);
760#endif
761 if (!Cudd_bddLeq(dd, subset, f)) {
762 (void) fprintf(dd->err, "Wrong subset\n");
763 }
764 cuddDeref(subset);
765 dd->errorCode = CUDD_INTERNAL_ERROR;
766 }
767#endif
768 return(subset);
769
770} /* end of cuddBiasedUnderApprox */
771
772
773/*---------------------------------------------------------------------------*/
774/* Definition of static functions */
775/*---------------------------------------------------------------------------*/
776
777
778/**Function********************************************************************
779
780 Synopsis [Recursively update the parity of the paths reaching a node.]
781
782 Description [Recursively update the parity of the paths reaching a node.
783 Assumes that node is regular and propagates the invariant.]
784
785 SideEffects [None]
786
787 SeeAlso [gatherInfoAux]
788
789******************************************************************************/
790static void
791updateParity(
792 DdNode * node /* function to analyze */,
793 ApproxInfo * info /* info on BDD */,
794 int newparity /* new parity for node */)
795{
796 NodeData *infoN;
797 DdNode *E;
798
799 if (!st_lookup(info->table, node, &infoN)) return;
800 if ((infoN->parity & newparity) != 0) return;
801 infoN->parity |= (short) newparity;
802 if (Cudd_IsConstant(node)) return;
803 updateParity(cuddT(node),info,newparity);
804 E = cuddE(node);
805 if (Cudd_IsComplement(E)) {
806 updateParity(Cudd_Not(E),info,3-newparity);
807 } else {
808 updateParity(E,info,newparity);
809 }
810 return;
811
812} /* end of updateParity */
813
814
815/**Function********************************************************************
816
817 Synopsis [Recursively counts minterms and computes reference counts
818 of each node in the BDD.]
819
820 Description [Recursively counts minterms and computes reference
821 counts of each node in the BDD. Similar to the cuddCountMintermAux
822 which recursively counts the number of minterms for the dag rooted
823 at each node in terms of the total number of variables (max). It assumes
824 that the node pointer passed to it is regular and it maintains the
825 invariant.]
826
827 SideEffects [None]
828
829 SeeAlso [gatherInfo]
830
831******************************************************************************/
832static NodeData *
833gatherInfoAux(
834 DdNode * node /* function to analyze */,
835 ApproxInfo * info /* info on BDD */,
836 int parity /* gather parity information */)
837{
838 DdNode *N, *Nt, *Ne;
839 NodeData *infoN, *infoT, *infoE;
840
841 N = Cudd_Regular(node);
842
843 /* Check whether entry for this node exists. */
844 if (st_lookup(info->table, N, &infoN)) {
845 if (parity) {
846 /* Update parity and propagate. */
847 updateParity(N, info, 1 + (int) Cudd_IsComplement(node));
848 }
849 return(infoN);
850 }
851
852 /* Compute the cofactors. */
853 Nt = Cudd_NotCond(cuddT(N), N != node);
854 Ne = Cudd_NotCond(cuddE(N), N != node);
855
856 infoT = gatherInfoAux(Nt, info, parity);
857 if (infoT == NULL) return(NULL);
858 infoE = gatherInfoAux(Ne, info, parity);
859 if (infoE == NULL) return(NULL);
860
861 infoT->functionRef++;
862 infoE->functionRef++;
863
864 /* Point to the correct location in the page. */
865 infoN = &(info->page[info->index++]);
866 infoN->parity |= (short) (1 + Cudd_IsComplement(node));
867
868 infoN->mintermsP = infoT->mintermsP/2;
869 infoN->mintermsN = infoT->mintermsN/2;
870 if (Cudd_IsComplement(Ne) ^ Cudd_IsComplement(node)) {
871 infoN->mintermsP += infoE->mintermsN/2;
872 infoN->mintermsN += infoE->mintermsP/2;
873 } else {
874 infoN->mintermsP += infoE->mintermsP/2;
875 infoN->mintermsN += infoE->mintermsN/2;
876 }
877
878 /* Insert entry for the node in the table. */
879 if (st_insert(info->table,(char *)N, (char *)infoN) == ST_OUT_OF_MEM) {
880 return(NULL);
881 }
882 return(infoN);
883
884} /* end of gatherInfoAux */
885
886
887/**Function********************************************************************
888
889 Synopsis [Gathers information about each node.]
890
891 Description [Counts minterms and computes reference counts of each
892 node in the BDD . The minterm count is separately computed for the
893 node and its complement. This is to avoid cancellation
894 errors. Returns a pointer to the data structure holding the
895 information gathered if successful; NULL otherwise.]
896
897 SideEffects [None]
898
899 SeeAlso [cuddUnderApprox gatherInfoAux]
900
901******************************************************************************/
902static ApproxInfo *
903gatherInfo(
904 DdManager * dd /* manager */,
905 DdNode * node /* function to be analyzed */,
906 int numVars /* number of variables node depends on */,
907 int parity /* gather parity information */)
908{
909 ApproxInfo *info;
910 NodeData *infoTop;
911
912 /* If user did not give numVars value, set it to the maximum
913 ** exponent that the pow function can take. The -1 is due to the
914 ** discrepancy in the value that pow takes and the value that
915 ** log gives.
916 */
917 if (numVars == 0) {
918 numVars = DBL_MAX_EXP - 1;
919 }
920
921 info = ALLOC(ApproxInfo,1);
922 if (info == NULL) {
923 dd->errorCode = CUDD_MEMORY_OUT;
924 return(NULL);
925 }
926 info->max = pow(2.0,(double) numVars);
927 info->one = DD_ONE(dd);
928 info->zero = Cudd_Not(info->one);
929 info->size = Cudd_DagSize(node);
930 /* All the information gathered will be stored in a contiguous
931 ** piece of memory, which is allocated here. This can be done
932 ** efficiently because we have counted the number of nodes of the
933 ** BDD. info->index points to the next available entry in the array
934 ** that stores the per-node information. */
935 info->page = ALLOC(NodeData,info->size);
936 if (info->page == NULL) {
937 dd->errorCode = CUDD_MEMORY_OUT;
938 FREE(info);
939 return(NULL);
940 }
941 memset(info->page, 0, info->size * sizeof(NodeData)); /* clear all page */
942 info->table = st_init_table(st_ptrcmp,st_ptrhash);
943 if (info->table == NULL) {
944 FREE(info->page);
945 FREE(info);
946 return(NULL);
947 }
948 /* We visit the DAG in post-order DFS. Hence, the constant node is
949 ** in first position, and the root of the DAG is in last position. */
950
951 /* Info for the constant node: Initialize only fields different from 0. */
952 if (st_insert(info->table, (char *)info->one, (char *)info->page) == ST_OUT_OF_MEM) {
953 FREE(info->page);
954 FREE(info);
955 st_free_table(info->table);
956 return(NULL);
957 }
958 info->page[0].mintermsP = info->max;
959 info->index = 1;
960
961 infoTop = gatherInfoAux(node,info,parity);
962 if (infoTop == NULL) {
963 FREE(info->page);
964 st_free_table(info->table);
965 FREE(info);
966 return(NULL);
967 }
968 if (Cudd_IsComplement(node)) {
969 info->minterms = infoTop->mintermsN;
970 } else {
971 info->minterms = infoTop->mintermsP;
972 }
973
974 infoTop->functionRef = 1;
975 return(info);
976
977} /* end of gatherInfo */
978
979
980/**Function********************************************************************
981
982 Synopsis [Counts the nodes that would be eliminated if a given node
983 were replaced by zero.]
984
985 Description [Counts the nodes that would be eliminated if a given
986 node were replaced by zero. This procedure uses a queue passed by
987 the caller for efficiency: since the queue is left empty at the
988 endof the search, it can be reused as is by the next search. Returns
989 the count (always striclty positive) if successful; 0 otherwise.]
990
991 SideEffects [None]
992
993 SeeAlso [cuddUnderApprox]
994
995******************************************************************************/
996static int
997computeSavings(
998 DdManager * dd,
999 DdNode * f,
1000 DdNode * skip,
1001 ApproxInfo * info,
1002 DdLevelQueue * queue)
1003{
1004 NodeData *infoN;
1005 LocalQueueItem *item;
1006 DdNode *node;
1007 int savings = 0;
1008
1009 node = Cudd_Regular(f);
1010 skip = Cudd_Regular(skip);
1011 /* Insert the given node in the level queue. Its local reference
1012 ** count is set equal to the function reference count so that the
1013 ** search will continue from it when it is retrieved. */
1014 item = (LocalQueueItem *)
1015 cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1016 if (item == NULL)
1017 return(0);
1018 (void) st_lookup(info->table, node, &infoN);
1019 item->localRef = infoN->functionRef;
1020
1021 /* Process the queue. */
1022 while (queue->first != NULL) {
1023 item = (LocalQueueItem *) queue->first;
1024 node = item->node;
1025 cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1026 if (node == skip) continue;
1027 (void) st_lookup(info->table, node, &infoN);
1028 if (item->localRef != infoN->functionRef) {
1029 /* This node is shared. */
1030 continue;
1031 }
1032 savings++;
1033 if (!cuddIsConstant(cuddT(node))) {
1034 item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1035 cuddI(dd,cuddT(node)->index));
1036 if (item == NULL) return(0);
1037 item->localRef++;
1038 }
1039 if (!Cudd_IsConstant(cuddE(node))) {
1040 item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1041 cuddI(dd,Cudd_Regular(cuddE(node))->index));
1042 if (item == NULL) return(0);
1043 item->localRef++;
1044 }
1045 }
1046
1047#ifdef DD_DEBUG
1048 /* At the end of a local search the queue should be empty. */
1049 assert(queue->size == 0);
1050#endif
1051 return(savings);
1052
1053} /* end of computeSavings */
1054
1055
1056/**Function********************************************************************
1057
1058 Synopsis [Update function reference counts.]
1059
1060 Description [Update function reference counts to account for replacement.
1061 Returns the number of nodes saved if successful; 0 otherwise.]
1062
1063 SideEffects [None]
1064
1065 SeeAlso [UAmarkNodes RAmarkNodes]
1066
1067******************************************************************************/
1068static int
1069updateRefs(
1070 DdManager * dd,
1071 DdNode * f,
1072 DdNode * skip,
1073 ApproxInfo * info,
1074 DdLevelQueue * queue)
1075{
1076 NodeData *infoN;
1077 LocalQueueItem *item;
1078 DdNode *node;
1079 int savings = 0;
1080
1081 node = Cudd_Regular(f);
1082 /* Insert the given node in the level queue. Its function reference
1083 ** count is set equal to 0 so that the search will continue from it
1084 ** when it is retrieved. */
1085 item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1086 if (item == NULL)
1087 return(0);
1088 (void) st_lookup(info->table, node, &infoN);
1089 infoN->functionRef = 0;
1090
1091 if (skip != NULL) {
1092 /* Increase the function reference count of the node to be skipped
1093 ** by 1 to account for the node pointing to it that will be created. */
1094 skip = Cudd_Regular(skip);
1095 (void) st_lookup(info->table, skip, &infoN);
1096 infoN->functionRef++;
1097 }
1098
1099 /* Process the queue. */
1100 while (queue->first != NULL) {
1101 item = (LocalQueueItem *) queue->first;
1102 node = item->node;
1103 cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1104 (void) st_lookup(info->table, node, &infoN);
1105 if (infoN->functionRef != 0) {
1106 /* This node is shared or must be skipped. */
1107 continue;
1108 }
1109 savings++;
1110 if (!cuddIsConstant(cuddT(node))) {
1111 item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1112 cuddI(dd,cuddT(node)->index));
1113 if (item == NULL) return(0);
1114 (void) st_lookup(info->table, cuddT(node), &infoN);
1115 infoN->functionRef--;
1116 }
1117 if (!Cudd_IsConstant(cuddE(node))) {
1118 item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1119 cuddI(dd,Cudd_Regular(cuddE(node))->index));
1120 if (item == NULL) return(0);
1121 (void) st_lookup(info->table, Cudd_Regular(cuddE(node)), &infoN);
1122 infoN->functionRef--;
1123 }
1124 }
1125
1126#ifdef DD_DEBUG
1127 /* At the end of a local search the queue should be empty. */
1128 assert(queue->size == 0);
1129#endif
1130 return(savings);
1131
1132} /* end of updateRefs */
1133
1134
1135/**Function********************************************************************
1136
1137 Synopsis [Marks nodes for replacement by zero.]
1138
1139 Description [Marks nodes for replacement by zero. Returns 1 if successful;
1140 0 otherwise.]
1141
1142 SideEffects [None]
1143
1144 SeeAlso [cuddUnderApprox]
1145
1146******************************************************************************/
1147static int
1148UAmarkNodes(
1149 DdManager * dd /* manager */,
1150 DdNode * f /* function to be analyzed */,
1151 ApproxInfo * info /* info on BDD */,
1152 int threshold /* when to stop approximating */,
1153 int safe /* enforce safe approximation */,
1154 double quality /* minimum improvement for accepted changes */)
1155{
1156 DdLevelQueue *queue;
1157 DdLevelQueue *localQueue;
1158 NodeData *infoN;
1159 GlobalQueueItem *item;
1160 DdNode *node;
1161 double numOnset;
1162 double impactP, impactN;
1163 int savings;
1164
1165#if 0
1166 (void) printf("initial size = %d initial minterms = %g\n",
1167 info->size, info->minterms);
1168#endif
1169 queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
1170 if (queue == NULL) {
1171 return(0);
1172 }
1173 localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
1174 dd->initSlots);
1175 if (localQueue == NULL) {
1176 cuddLevelQueueQuit(queue);
1177 return(0);
1178 }
1179 node = Cudd_Regular(f);
1180 item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1181 if (item == NULL) {
1182 cuddLevelQueueQuit(queue);
1183 cuddLevelQueueQuit(localQueue);
1184 return(0);
1185 }
1186 if (Cudd_IsComplement(f)) {
1187 item->impactP = 0.0;
1188 item->impactN = 1.0;
1189 } else {
1190 item->impactP = 1.0;
1191 item->impactN = 0.0;
1192 }
1193 while (queue->first != NULL) {
1194 /* If the size of the subset is below the threshold, quit. */
1195 if (info->size <= threshold)
1196 break;
1197 item = (GlobalQueueItem *) queue->first;
1198 node = item->node;
1199 node = Cudd_Regular(node);
1200 (void) st_lookup(info->table, node, &infoN);
1201 if (safe && infoN->parity == 3) {
1202 cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1203 continue;
1204 }
1205 impactP = item->impactP;
1206 impactN = item->impactN;
1207 numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
1208 savings = computeSavings(dd,node,NULL,info,localQueue);
1209 if (savings == 0) {
1210 cuddLevelQueueQuit(queue);
1211 cuddLevelQueueQuit(localQueue);
1212 return(0);
1213 }
1214 cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1215#if 0
1216 (void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
1217 node, impactP, impactN, numOnset, savings);
1218#endif
1219 if ((1 - numOnset / info->minterms) >
1220 quality * (1 - (double) savings / info->size)) {
1221 infoN->replace = TRUE;
1222 info->size -= savings;
1223 info->minterms -=numOnset;
1224#if 0
1225 (void) printf("replace: new size = %d new minterms = %g\n",
1226 info->size, info->minterms);
1227#endif
1228 savings -= updateRefs(dd,node,NULL,info,localQueue);
1229 assert(savings == 0);
1230 continue;
1231 }
1232 if (!cuddIsConstant(cuddT(node))) {
1233 item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1234 cuddI(dd,cuddT(node)->index));
1235 item->impactP += impactP/2.0;
1236 item->impactN += impactN/2.0;
1237 }
1238 if (!Cudd_IsConstant(cuddE(node))) {
1239 item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1240 cuddI(dd,Cudd_Regular(cuddE(node))->index));
1241 if (Cudd_IsComplement(cuddE(node))) {
1242 item->impactP += impactN/2.0;
1243 item->impactN += impactP/2.0;
1244 } else {
1245 item->impactP += impactP/2.0;
1246 item->impactN += impactN/2.0;
1247 }
1248 }
1249 }
1250
1251 cuddLevelQueueQuit(queue);
1252 cuddLevelQueueQuit(localQueue);
1253 return(1);
1254
1255} /* end of UAmarkNodes */
1256
1257
1258/**Function********************************************************************
1259
1260 Synopsis [Builds the subset BDD.]
1261
1262 Description [Builds the subset BDD. Based on the info table,
1263 replaces selected nodes by zero. Returns a pointer to the result if
1264 successful; NULL otherwise.]
1265
1266 SideEffects [None]
1267
1268 SeeAlso [cuddUnderApprox]
1269
1270******************************************************************************/
1271static DdNode *
1272UAbuildSubset(
1273 DdManager * dd /* DD manager */,
1274 DdNode * node /* current node */,
1275 ApproxInfo * info /* node info */)
1276{
1277
1278 DdNode *Nt, *Ne, *N, *t, *e, *r;
1279 NodeData *infoN;
1280
1281 if (Cudd_IsConstant(node))
1282 return(node);
1283
1284 N = Cudd_Regular(node);
1285
1286 if (st_lookup(info->table, N, &infoN)) {
1287 if (infoN->replace == TRUE) {
1288 return(info->zero);
1289 }
1290 if (N == node ) {
1291 if (infoN->resultP != NULL) {
1292 return(infoN->resultP);
1293 }
1294 } else {
1295 if (infoN->resultN != NULL) {
1296 return(infoN->resultN);
1297 }
1298 }
1299 } else {
1300 (void) fprintf(dd->err,
1301 "Something is wrong, ought to be in info table\n");
1302 dd->errorCode = CUDD_INTERNAL_ERROR;
1303 return(NULL);
1304 }
1305
1306 Nt = Cudd_NotCond(cuddT(N), Cudd_IsComplement(node));
1307 Ne = Cudd_NotCond(cuddE(N), Cudd_IsComplement(node));
1308
1309 t = UAbuildSubset(dd, Nt, info);
1310 if (t == NULL) {
1311 return(NULL);
1312 }
1313 cuddRef(t);
1314
1315 e = UAbuildSubset(dd, Ne, info);
1316 if (e == NULL) {
1317 Cudd_RecursiveDeref(dd,t);
1318 return(NULL);
1319 }
1320 cuddRef(e);
1321
1322 if (Cudd_IsComplement(t)) {
1323 t = Cudd_Not(t);
1324 e = Cudd_Not(e);
1325 r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
1326 if (r == NULL) {
1327 Cudd_RecursiveDeref(dd, e);
1328 Cudd_RecursiveDeref(dd, t);
1329 return(NULL);
1330 }
1331 r = Cudd_Not(r);
1332 } else {
1333 r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
1334 if (r == NULL) {
1335 Cudd_RecursiveDeref(dd, e);
1336 Cudd_RecursiveDeref(dd, t);
1337 return(NULL);
1338 }
1339 }
1340 cuddDeref(t);
1341 cuddDeref(e);
1342
1343 if (N == node) {
1344 infoN->resultP = r;
1345 } else {
1346 infoN->resultN = r;
1347 }
1348
1349 return(r);
1350
1351} /* end of UAbuildSubset */
1352
1353
1354/**Function********************************************************************
1355
1356 Synopsis [Marks nodes for remapping.]
1357
1358 Description [Marks nodes for remapping. Returns 1 if successful; 0
1359 otherwise.]
1360
1361 SideEffects [None]
1362
1363 SeeAlso [cuddRemapUnderApprox]
1364
1365******************************************************************************/
1366static int
1367RAmarkNodes(
1368 DdManager * dd /* manager */,
1369 DdNode * f /* function to be analyzed */,
1370 ApproxInfo * info /* info on BDD */,
1371 int threshold /* when to stop approximating */,
1372 double quality /* minimum improvement for accepted changes */)
1373{
1374 DdLevelQueue *queue;
1375 DdLevelQueue *localQueue;
1376 NodeData *infoN, *infoT, *infoE;
1377 GlobalQueueItem *item;
1378 DdNode *node, *T, *E;
1379 DdNode *shared; /* grandchild shared by the two children of node */
1380 double numOnset;
1381 double impact, impactP, impactN;
1382 double minterms;
1383 int savings;
1384 int replace;
1385
1386#if 0
1387 (void) fprintf(dd->out,"initial size = %d initial minterms = %g\n",
1388 info->size, info->minterms);
1389#endif
1390 queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
1391 if (queue == NULL) {
1392 return(0);
1393 }
1394 localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
1395 dd->initSlots);
1396 if (localQueue == NULL) {
1397 cuddLevelQueueQuit(queue);
1398 return(0);
1399 }
1400 /* Enqueue regular pointer to root and initialize impact. */
1401 node = Cudd_Regular(f);
1402 item = (GlobalQueueItem *)
1403 cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1404 if (item == NULL) {
1405 cuddLevelQueueQuit(queue);
1406 cuddLevelQueueQuit(localQueue);
1407 return(0);
1408 }
1409 if (Cudd_IsComplement(f)) {
1410 item->impactP = 0.0;
1411 item->impactN = 1.0;
1412 } else {
1413 item->impactP = 1.0;
1414 item->impactN = 0.0;
1415 }
1416 /* The nodes retrieved here are guaranteed to be non-terminal.
1417 ** The initial node is not terminal because constant nodes are
1418 ** dealt with in the calling procedure. Subsequent nodes are inserted
1419 ** only if they are not terminal. */
1420 while (queue->first != NULL) {
1421 /* If the size of the subset is below the threshold, quit. */
1422 if (info->size <= threshold)
1423 break;
1424 item = (GlobalQueueItem *) queue->first;
1425 node = item->node;
1426#ifdef DD_DEBUG
1427 assert(item->impactP >= 0 && item->impactP <= 1.0);
1428 assert(item->impactN >= 0 && item->impactN <= 1.0);
1429 assert(!Cudd_IsComplement(node));
1430 assert(!Cudd_IsConstant(node));
1431#endif
1432 if (!st_lookup(info->table, node, &infoN)) {
1433 cuddLevelQueueQuit(queue);
1434 cuddLevelQueueQuit(localQueue);
1435 return(0);
1436 }
1437#ifdef DD_DEBUG
1438 assert(infoN->parity >= 1 && infoN->parity <= 3);
1439#endif
1440 if (infoN->parity == 3) {
1441 /* This node can be reached through paths of different parity.
1442 ** It is not safe to replace it, because remapping will give
1443 ** an incorrect result, while replacement by 0 may cause node
1444 ** splitting. */
1445 cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1446 continue;
1447 }
1448 T = cuddT(node);
1449 E = cuddE(node);
1450 shared = NULL;
1451 impactP = item->impactP;
1452 impactN = item->impactN;
1453 if (Cudd_bddLeq(dd,T,E)) {
1454 /* Here we know that E is regular. */
1455#ifdef DD_DEBUG
1456 assert(!Cudd_IsComplement(E));
1457#endif
1458 (void) st_lookup(info->table, T, &infoT);
1459 (void) st_lookup(info->table, E, &infoE);
1460 if (infoN->parity == 1) {
1461 impact = impactP;
1462 minterms = infoE->mintermsP/2.0 - infoT->mintermsP/2.0;
1463 if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
1464 savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
1465 if (savings == 1) {
1466 cuddLevelQueueQuit(queue);
1467 cuddLevelQueueQuit(localQueue);
1468 return(0);
1469 }
1470 } else {
1471 savings = 1;
1472 }
1473 replace = REPLACE_E;
1474 } else {
1475#ifdef DD_DEBUG
1476 assert(infoN->parity == 2);
1477#endif
1478 impact = impactN;
1479 minterms = infoT->mintermsN/2.0 - infoE->mintermsN/2.0;
1480 if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
1481 savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
1482 if (savings == 1) {
1483 cuddLevelQueueQuit(queue);
1484 cuddLevelQueueQuit(localQueue);
1485 return(0);
1486 }
1487 } else {
1488 savings = 1;
1489 }
1490 replace = REPLACE_T;
1491 }
1492 numOnset = impact * minterms;
1493 } else if (Cudd_bddLeq(dd,E,T)) {
1494 /* Here E may be complemented. */
1495 DdNode *Ereg = Cudd_Regular(E);
1496 (void) st_lookup(info->table, T, &infoT);
1497 (void) st_lookup(info->table, Ereg, &infoE);
1498 if (infoN->parity == 1) {
1499 impact = impactP;
1500 minterms = infoT->mintermsP/2.0 -
1501 ((E == Ereg) ? infoE->mintermsP : infoE->mintermsN)/2.0;
1502 if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
1503 savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
1504 if (savings == 1) {
1505 cuddLevelQueueQuit(queue);
1506 cuddLevelQueueQuit(localQueue);
1507 return(0);
1508 }
1509 } else {
1510 savings = 1;
1511 }
1512 replace = REPLACE_T;
1513 } else {
1514#ifdef DD_DEBUG
1515 assert(infoN->parity == 2);
1516#endif
1517 impact = impactN;
1518 minterms = ((E == Ereg) ? infoE->mintermsN :
1519 infoE->mintermsP)/2.0 - infoT->mintermsN/2.0;
1520 if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
1521 savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
1522 if (savings == 1) {
1523 cuddLevelQueueQuit(queue);
1524 cuddLevelQueueQuit(localQueue);
1525 return(0);
1526 }
1527 } else {
1528 savings = 1;
1529 }
1530 replace = REPLACE_E;
1531 }
1532 numOnset = impact * minterms;
1533 } else {
1534 DdNode *Ereg = Cudd_Regular(E);
1535 DdNode *TT = cuddT(T);
1536 DdNode *ET = Cudd_NotCond(cuddT(Ereg), Cudd_IsComplement(E));
1537 if (T->index == Ereg->index && TT == ET) {
1538 shared = TT;
1539 replace = REPLACE_TT;
1540 } else {
1541 DdNode *TE = cuddE(T);
1542 DdNode *EE = Cudd_NotCond(cuddE(Ereg), Cudd_IsComplement(E));
1543 if (T->index == Ereg->index && TE == EE) {
1544 shared = TE;
1545 replace = REPLACE_TE;
1546 } else {
1547 replace = REPLACE_N;
1548 }
1549 }
1550 numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
1551 savings = computeSavings(dd,node,shared,info,localQueue);
1552 if (shared != NULL) {
1553 NodeData *infoS;
1554 (void) st_lookup(info->table, Cudd_Regular(shared), &infoS);
1555 if (Cudd_IsComplement(shared)) {
1556 numOnset -= (infoS->mintermsN * impactP +
1557 infoS->mintermsP * impactN)/2.0;
1558 } else {
1559 numOnset -= (infoS->mintermsP * impactP +
1560 infoS->mintermsN * impactN)/2.0;
1561 }
1562 savings--;
1563 }
1564 }
1565
1566 cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1567#if 0
1568 if (replace == REPLACE_T || replace == REPLACE_E)
1569 (void) printf("node %p: impact = %g numOnset = %g savings %d\n",
1570 node, impact, numOnset, savings);
1571 else
1572 (void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
1573 node, impactP, impactN, numOnset, savings);
1574#endif
1575 if ((1 - numOnset / info->minterms) >
1576 quality * (1 - (double) savings / info->size)) {
1577 infoN->replace = (char) replace;
1578 info->size -= savings;
1579 info->minterms -=numOnset;
1580#if 0
1581 (void) printf("remap(%d): new size = %d new minterms = %g\n",
1582 replace, info->size, info->minterms);
1583#endif
1584 if (replace == REPLACE_N) {
1585 savings -= updateRefs(dd,node,NULL,info,localQueue);
1586 } else if (replace == REPLACE_T) {
1587 savings -= updateRefs(dd,node,E,info,localQueue);
1588 } else if (replace == REPLACE_E) {
1589 savings -= updateRefs(dd,node,T,info,localQueue);
1590 } else {
1591#ifdef DD_DEBUG
1592 assert(replace == REPLACE_TT || replace == REPLACE_TE);
1593#endif
1594 savings -= updateRefs(dd,node,shared,info,localQueue) - 1;
1595 }
1596 assert(savings == 0);
1597 } else {
1598 replace = NOTHING;
1599 }
1600 if (replace == REPLACE_N) continue;
1601 if ((replace == REPLACE_E || replace == NOTHING) &&
1602 !cuddIsConstant(cuddT(node))) {
1603 item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1604 cuddI(dd,cuddT(node)->index));
1605 if (replace == REPLACE_E) {
1606 item->impactP += impactP;
1607 item->impactN += impactN;
1608 } else {
1609 item->impactP += impactP/2.0;
1610 item->impactN += impactN/2.0;
1611 }
1612 }
1613 if ((replace == REPLACE_T || replace == NOTHING) &&
1614 !Cudd_IsConstant(cuddE(node))) {
1615 item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1616 cuddI(dd,Cudd_Regular(cuddE(node))->index));
1617 if (Cudd_IsComplement(cuddE(node))) {
1618 if (replace == REPLACE_T) {
1619 item->impactP += impactN;
1620 item->impactN += impactP;
1621 } else {
1622 item->impactP += impactN/2.0;
1623 item->impactN += impactP/2.0;
1624 }
1625 } else {
1626 if (replace == REPLACE_T) {
1627 item->impactP += impactP;
1628 item->impactN += impactN;
1629 } else {
1630 item->impactP += impactP/2.0;
1631 item->impactN += impactN/2.0;
1632 }
1633 }
1634 }
1635 if ((replace == REPLACE_TT || replace == REPLACE_TE) &&
1636 !Cudd_IsConstant(shared)) {
1637 item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(shared),
1638 cuddI(dd,Cudd_Regular(shared)->index));
1639 if (Cudd_IsComplement(shared)) {
1640 item->impactP += impactN;
1641 item->impactN += impactP;
1642 } else {
1643 item->impactP += impactP;
1644 item->impactN += impactN;
1645 }
1646 }
1647 }
1648
1649 cuddLevelQueueQuit(queue);
1650 cuddLevelQueueQuit(localQueue);
1651 return(1);
1652
1653} /* end of RAmarkNodes */
1654
1655
1656/**Function********************************************************************
1657
1658 Synopsis [Marks nodes for remapping.]
1659
1660 Description [Marks nodes for remapping. Returns 1 if successful; 0
1661 otherwise.]
1662
1663 SideEffects [None]
1664
1665 SeeAlso [cuddRemapUnderApprox]
1666
1667******************************************************************************/
1668static int
1669BAmarkNodes(
1670 DdManager *dd /* manager */,
1671 DdNode *f /* function to be analyzed */,
1672 ApproxInfo *info /* info on BDD */,
1673 int threshold /* when to stop approximating */,
1674 double quality1 /* minimum improvement for accepted changes when b=1 */,
1675 double quality0 /* minimum improvement for accepted changes when b=0 */)
1676{
1677 DdLevelQueue *queue;
1678 DdLevelQueue *localQueue;
1679 NodeData *infoN, *infoT, *infoE;
1680 GlobalQueueItem *item;
1681 DdNode *node, *T, *E;
1682 DdNode *shared; /* grandchild shared by the two children of node */
1683 double numOnset;
1684 double impact, impactP, impactN;
1685 double minterms;
1686 double quality;
1687 int savings;
1688 int replace;
1689
1690#if 0
1691 (void) fprintf(dd->out,"initial size = %d initial minterms = %g\n",
1692 info->size, info->minterms);
1693#endif
1694 queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
1695 if (queue == NULL) {
1696 return(0);
1697 }
1698 localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
1699 dd->initSlots);
1700 if (localQueue == NULL) {
1701 cuddLevelQueueQuit(queue);
1702 return(0);
1703 }
1704 /* Enqueue regular pointer to root and initialize impact. */
1705 node = Cudd_Regular(f);
1706 item = (GlobalQueueItem *)
1707 cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1708 if (item == NULL) {
1709 cuddLevelQueueQuit(queue);
1710 cuddLevelQueueQuit(localQueue);
1711 return(0);
1712 }
1713 if (Cudd_IsComplement(f)) {
1714 item->impactP = 0.0;
1715 item->impactN = 1.0;
1716 } else {
1717 item->impactP = 1.0;
1718 item->impactN = 0.0;
1719 }
1720 /* The nodes retrieved here are guaranteed to be non-terminal.
1721 ** The initial node is not terminal because constant nodes are
1722 ** dealt with in the calling procedure. Subsequent nodes are inserted
1723 ** only if they are not terminal. */
1724 while (queue->first != NULL) {
1725 /* If the size of the subset is below the threshold, quit. */
1726 if (info->size <= threshold)
1727 break;
1728 item = (GlobalQueueItem *) queue->first;
1729 node = item->node;
1730#ifdef DD_DEBUG
1731 assert(item->impactP >= 0 && item->impactP <= 1.0);
1732 assert(item->impactN >= 0 && item->impactN <= 1.0);
1733 assert(!Cudd_IsComplement(node));
1734 assert(!Cudd_IsConstant(node));
1735#endif
1736 if (!st_lookup(info->table, node, &infoN)) {
1737 cuddLevelQueueQuit(queue);
1738 cuddLevelQueueQuit(localQueue);
1739 return(0);
1740 }
1741 quality = infoN->care ? quality1 : quality0;
1742#ifdef DD_DEBUG
1743 assert(infoN->parity >= 1 && infoN->parity <= 3);
1744#endif
1745 if (infoN->parity == 3) {
1746 /* This node can be reached through paths of different parity.
1747 ** It is not safe to replace it, because remapping will give
1748 ** an incorrect result, while replacement by 0 may cause node
1749 ** splitting. */
1750 cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1751 continue;
1752 }
1753 T = cuddT(node);
1754 E = cuddE(node);
1755 shared = NULL;
1756 impactP = item->impactP;
1757 impactN = item->impactN;
1758 if (Cudd_bddLeq(dd,T,E)) {
1759 /* Here we know that E is regular. */
1760#ifdef DD_DEBUG
1761 assert(!Cudd_IsComplement(E));
1762#endif
1763 (void) st_lookup(info->table, T, &infoT);
1764 (void) st_lookup(info->table, E, &infoE);
1765 if (infoN->parity == 1) {
1766 impact = impactP;
1767 minterms = infoE->mintermsP/2.0 - infoT->mintermsP/2.0;
1768 if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
1769 savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
1770 if (savings == 1) {
1771 cuddLevelQueueQuit(queue);
1772 cuddLevelQueueQuit(localQueue);
1773 return(0);
1774 }
1775 } else {
1776 savings = 1;
1777 }
1778 replace = REPLACE_E;
1779 } else {
1780#ifdef DD_DEBUG
1781 assert(infoN->parity == 2);
1782#endif
1783 impact = impactN;
1784 minterms = infoT->mintermsN/2.0 - infoE->mintermsN/2.0;
1785 if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
1786 savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
1787 if (savings == 1) {
1788 cuddLevelQueueQuit(queue);
1789 cuddLevelQueueQuit(localQueue);
1790 return(0);
1791 }
1792 } else {
1793 savings = 1;
1794 }
1795 replace = REPLACE_T;
1796 }
1797 numOnset = impact * minterms;
1798 } else if (Cudd_bddLeq(dd,E,T)) {
1799 /* Here E may be complemented. */
1800 DdNode *Ereg = Cudd_Regular(E);
1801 (void) st_lookup(info->table, T, &infoT);
1802 (void) st_lookup(info->table, Ereg, &infoE);
1803 if (infoN->parity == 1) {
1804 impact = impactP;
1805 minterms = infoT->mintermsP/2.0 -
1806 ((E == Ereg) ? infoE->mintermsP : infoE->mintermsN)/2.0;
1807 if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
1808 savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
1809 if (savings == 1) {
1810 cuddLevelQueueQuit(queue);
1811 cuddLevelQueueQuit(localQueue);
1812 return(0);
1813 }
1814 } else {
1815 savings = 1;
1816 }
1817 replace = REPLACE_T;
1818 } else {
1819#ifdef DD_DEBUG
1820 assert(infoN->parity == 2);
1821#endif
1822 impact = impactN;
1823 minterms = ((E == Ereg) ? infoE->mintermsN :
1824 infoE->mintermsP)/2.0 - infoT->mintermsN/2.0;
1825 if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
1826 savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
1827 if (savings == 1) {
1828 cuddLevelQueueQuit(queue);
1829 cuddLevelQueueQuit(localQueue);
1830 return(0);
1831 }
1832 } else {
1833 savings = 1;
1834 }
1835 replace = REPLACE_E;
1836 }
1837 numOnset = impact * minterms;
1838 } else {
1839 DdNode *Ereg = Cudd_Regular(E);
1840 DdNode *TT = cuddT(T);
1841 DdNode *ET = Cudd_NotCond(cuddT(Ereg), Cudd_IsComplement(E));
1842 if (T->index == Ereg->index && TT == ET) {
1843 shared = TT;
1844 replace = REPLACE_TT;
1845 } else {
1846 DdNode *TE = cuddE(T);
1847 DdNode *EE = Cudd_NotCond(cuddE(Ereg), Cudd_IsComplement(E));
1848 if (T->index == Ereg->index && TE == EE) {
1849 shared = TE;
1850 replace = REPLACE_TE;
1851 } else {
1852 replace = REPLACE_N;
1853 }
1854 }
1855 numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
1856 savings = computeSavings(dd,node,shared,info,localQueue);
1857 if (shared != NULL) {
1858 NodeData *infoS;
1859 (void) st_lookup(info->table, Cudd_Regular(shared), &infoS);
1860 if (Cudd_IsComplement(shared)) {
1861 numOnset -= (infoS->mintermsN * impactP +
1862 infoS->mintermsP * impactN)/2.0;
1863 } else {
1864 numOnset -= (infoS->mintermsP * impactP +
1865 infoS->mintermsN * impactN)/2.0;
1866 }
1867 savings--;
1868 }
1869 }
1870
1871 cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1872#if 0
1873 if (replace == REPLACE_T || replace == REPLACE_E)
1874 (void) printf("node %p: impact = %g numOnset = %g savings %d\n",
1875 node, impact, numOnset, savings);
1876 else
1877 (void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
1878 node, impactP, impactN, numOnset, savings);
1879#endif
1880 if ((1 - numOnset / info->minterms) >
1881 quality * (1 - (double) savings / info->size)) {
1882 infoN->replace = (char) replace;
1883 info->size -= savings;
1884 info->minterms -=numOnset;
1885#if 0
1886 (void) printf("remap(%d): new size = %d new minterms = %g\n",
1887 replace, info->size, info->minterms);
1888#endif
1889 if (replace == REPLACE_N) {
1890 savings -= updateRefs(dd,node,NULL,info,localQueue);
1891 } else if (replace == REPLACE_T) {
1892 savings -= updateRefs(dd,node,E,info,localQueue);
1893 } else if (replace == REPLACE_E) {
1894 savings -= updateRefs(dd,node,T,info,localQueue);
1895 } else {
1896#ifdef DD_DEBUG
1897 assert(replace == REPLACE_TT || replace == REPLACE_TE);
1898#endif
1899 savings -= updateRefs(dd,node,shared,info,localQueue) - 1;
1900 }
1901 assert(savings == 0);
1902 } else {
1903 replace = NOTHING;
1904 }
1905 if (replace == REPLACE_N) continue;
1906 if ((replace == REPLACE_E || replace == NOTHING) &&
1907 !cuddIsConstant(cuddT(node))) {
1908 item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1909 cuddI(dd,cuddT(node)->index));
1910 if (replace == REPLACE_E) {
1911 item->impactP += impactP;
1912 item->impactN += impactN;
1913 } else {
1914 item->impactP += impactP/2.0;
1915 item->impactN += impactN/2.0;
1916 }
1917 }
1918 if ((replace == REPLACE_T || replace == NOTHING) &&
1919 !Cudd_IsConstant(cuddE(node))) {
1920 item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1921 cuddI(dd,Cudd_Regular(cuddE(node))->index));
1922 if (Cudd_IsComplement(cuddE(node))) {
1923 if (replace == REPLACE_T) {
1924 item->impactP += impactN;
1925 item->impactN += impactP;
1926 } else {
1927 item->impactP += impactN/2.0;
1928 item->impactN += impactP/2.0;
1929 }
1930 } else {
1931 if (replace == REPLACE_T) {
1932 item->impactP += impactP;
1933 item->impactN += impactN;
1934 } else {
1935 item->impactP += impactP/2.0;
1936 item->impactN += impactN/2.0;
1937 }
1938 }
1939 }
1940 if ((replace == REPLACE_TT || replace == REPLACE_TE) &&
1941 !Cudd_IsConstant(shared)) {
1942 item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(shared),
1943 cuddI(dd,Cudd_Regular(shared)->index));
1944 if (Cudd_IsComplement(shared)) {
1945 if (replace == REPLACE_T) {
1946 item->impactP += impactN;
1947 item->impactN += impactP;
1948 } else {
1949 item->impactP += impactN/2.0;
1950 item->impactN += impactP/2.0;
1951 }
1952 } else {
1953 if (replace == REPLACE_T) {
1954 item->impactP += impactP;
1955 item->impactN += impactN;
1956 } else {
1957 item->impactP += impactP/2.0;
1958 item->impactN += impactN/2.0;
1959 }
1960 }
1961 }
1962 }
1963
1964 cuddLevelQueueQuit(queue);
1965 cuddLevelQueueQuit(localQueue);
1966 return(1);
1967
1968} /* end of BAmarkNodes */
1969
1970
1971/**Function********************************************************************
1972
1973 Synopsis [Builds the subset BDD for cuddRemapUnderApprox.]
1974
1975 Description [Builds the subset BDDfor cuddRemapUnderApprox. Based
1976 on the info table, performs remapping or replacement at selected
1977 nodes. Returns a pointer to the result if successful; NULL
1978 otherwise.]
1979
1980 SideEffects [None]
1981
1982 SeeAlso [cuddRemapUnderApprox]
1983
1984******************************************************************************/
1985static DdNode *
1986RAbuildSubset(
1987 DdManager * dd /* DD manager */,
1988 DdNode * node /* current node */,
1989 ApproxInfo * info /* node info */)
1990{
1991 DdNode *Nt, *Ne, *N, *t, *e, *r;
1992 NodeData *infoN;
1993
1994 if (Cudd_IsConstant(node))
1995 return(node);
1996
1997 N = Cudd_Regular(node);
1998
1999 Nt = Cudd_NotCond(cuddT(N), Cudd_IsComplement(node));
2000 Ne = Cudd_NotCond(cuddE(N), Cudd_IsComplement(node));
2001
2002 if (st_lookup(info->table, N, &infoN)) {
2003 if (N == node ) {
2004 if (infoN->resultP != NULL) {
2005 return(infoN->resultP);
2006 }
2007 } else {
2008 if (infoN->resultN != NULL) {
2009 return(infoN->resultN);
2010 }
2011 }
2012 if (infoN->replace == REPLACE_T) {
2013 r = RAbuildSubset(dd, Ne, info);
2014 return(r);
2015 } else if (infoN->replace == REPLACE_E) {
2016 r = RAbuildSubset(dd, Nt, info);
2017 return(r);
2018 } else if (infoN->replace == REPLACE_N) {
2019 return(info->zero);
2020 } else if (infoN->replace == REPLACE_TT) {
2021 DdNode *Ntt = Cudd_NotCond(cuddT(cuddT(N)),
2022 Cudd_IsComplement(node));
2023 int index = cuddT(N)->index;
2024 e = info->zero;
2025 t = RAbuildSubset(dd, Ntt, info);
2026 if (t == NULL) {
2027 return(NULL);
2028 }
2029 cuddRef(t);
2030 if (Cudd_IsComplement(t)) {
2031 t = Cudd_Not(t);
2032 e = Cudd_Not(e);
2033 r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
2034 if (r == NULL) {
2035 Cudd_RecursiveDeref(dd, t);
2036 return(NULL);
2037 }
2038 r = Cudd_Not(r);
2039 } else {
2040 r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
2041 if (r == NULL) {
2042 Cudd_RecursiveDeref(dd, t);
2043 return(NULL);
2044 }
2045 }
2046 cuddDeref(t);
2047 return(r);
2048 } else if (infoN->replace == REPLACE_TE) {
2049 DdNode *Nte = Cudd_NotCond(cuddE(cuddT(N)),
2050 Cudd_IsComplement(node));
2051 int index = cuddT(N)->index;
2052 t = info->one;
2053 e = RAbuildSubset(dd, Nte, info);
2054 if (e == NULL) {
2055 return(NULL);
2056 }
2057 cuddRef(e);
2058 e = Cudd_Not(e);
2059 r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
2060 if (r == NULL) {
2061 Cudd_RecursiveDeref(dd, e);
2062 return(NULL);
2063 }
2064 r =Cudd_Not(r);
2065 cuddDeref(e);
2066 return(r);
2067 }
2068 } else {
2069 (void) fprintf(dd->err,
2070 "Something is wrong, ought to be in info table\n");
2071 dd->errorCode = CUDD_INTERNAL_ERROR;
2072 return(NULL);
2073 }
2074
2075 t = RAbuildSubset(dd, Nt, info);
2076 if (t == NULL) {
2077 return(NULL);
2078 }
2079 cuddRef(t);
2080
2081 e = RAbuildSubset(dd, Ne, info);
2082 if (e == NULL) {
2083 Cudd_RecursiveDeref(dd,t);
2084 return(NULL);
2085 }
2086 cuddRef(e);
2087
2088 if (Cudd_IsComplement(t)) {
2089 t = Cudd_Not(t);
2090 e = Cudd_Not(e);
2091 r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
2092 if (r == NULL) {
2093 Cudd_RecursiveDeref(dd, e);
2094 Cudd_RecursiveDeref(dd, t);
2095 return(NULL);
2096 }
2097 r = Cudd_Not(r);
2098 } else {
2099 r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
2100 if (r == NULL) {
2101 Cudd_RecursiveDeref(dd, e);
2102 Cudd_RecursiveDeref(dd, t);
2103 return(NULL);
2104 }
2105 }
2106 cuddDeref(t);
2107 cuddDeref(e);
2108
2109 if (N == node) {
2110 infoN->resultP = r;
2111 } else {
2112 infoN->resultN = r;
2113 }
2114
2115 return(r);
2116
2117} /* end of RAbuildSubset */
2118
2119
2120/**Function********************************************************************
2121
2122 Synopsis [Finds don't care nodes.]
2123
2124 Description [Finds don't care nodes by traversing f and b in parallel.
2125 Returns the care status of the visited f node if successful; CARE_ERROR
2126 otherwise.]
2127
2128 SideEffects [None]
2129
2130 SeeAlso [cuddBiasedUnderApprox]
2131
2132******************************************************************************/
2133static int
2134BAapplyBias(
2135 DdManager *dd,
2136 DdNode *f,
2137 DdNode *b,
2138 ApproxInfo *info,
2139 DdHashTable *cache)
2140{
2141 DdNode *one, *zero, *res;
2142 DdNode *Ft, *Fe, *B, *Bt, *Be;
2143 unsigned int topf, topb;
2144 NodeData *infoF;
2145 int careT, careE;
2146
2147 one = DD_ONE(dd);
2148 zero = Cudd_Not(one);
2149
2150 if (!st_lookup(info->table, f, &infoF))
2151 return(CARE_ERROR);
2152 if (f == one) return(TOTAL_CARE);
2153 if (b == zero) return(infoF->care);
2154 if (infoF->care == TOTAL_CARE) return(TOTAL_CARE);
2155
2156 if ((f->ref != 1 || Cudd_Regular(b)->ref != 1) &&
2157 (res = cuddHashTableLookup2(cache,f,b)) != NULL) {
2158 if (res->ref == 0) {
2159 cache->manager->dead++;
2160 cache->manager->constants.dead++;
2161 }
2162 return(infoF->care);
2163 }
2164
2165 topf = dd->perm[f->index];
2166 B = Cudd_Regular(b);
2167 topb = cuddI(dd,B->index);
2168 if (topf <= topb) {
2169 Ft = cuddT(f); Fe = cuddE(f);
2170 } else {
2171 Ft = Fe = f;
2172 }
2173 if (topb <= topf) {
2174 /* We know that b is not constant because f is not. */
2175 Bt = cuddT(B); Be = cuddE(B);
2176 if (Cudd_IsComplement(b)) {
2177 Bt = Cudd_Not(Bt);
2178 Be = Cudd_Not(Be);
2179 }
2180 } else {
2181 Bt = Be = b;
2182 }
2183
2184 careT = BAapplyBias(dd, Ft, Bt, info, cache);
2185 if (careT == CARE_ERROR)
2186 return(CARE_ERROR);
2187 careE = BAapplyBias(dd, Cudd_Regular(Fe), Be, info, cache);
2188 if (careE == CARE_ERROR)
2189 return(CARE_ERROR);
2190 if (careT == TOTAL_CARE && careE == TOTAL_CARE) {
2191 infoF->care = TOTAL_CARE;
2192 } else {
2193 infoF->care = CARE;
2194 }
2195
2196 if (f->ref != 1 || Cudd_Regular(b)->ref != 1) {
2197 ptrint fanout = (ptrint) f->ref * Cudd_Regular(b)->ref;
2198 cuddSatDec(fanout);
2199 if (!cuddHashTableInsert2(cache,f,b,one,fanout)) {
2200 return(CARE_ERROR);
2201 }
2202 }
2203 return(infoF->care);
2204
2205} /* end of BAapplyBias */
Note: See TracBrowser for help on using the repository browser.